Left Termination proof of /tmp/tmpsascCP/quot.pl

Left Termination of the query pattern div_in_3(g, g, a) w.r.t. the given Prolog program could successfully be proven:

0 Prolog

↳1 PrologToDTProblemTransformerProof (⇐)

↳2 TRIPLES

↳3 TriplesToPiDPProof (⇐)

↳4 PiDP

↳5 DependencyGraphProof (⇔)

↳6 AND

    ↳7 PiDP

        ↳8 PiDPToQDPProof (⇐)

        ↳9 QDP

        ↳10 QDPSizeChangeProof (⇔)

        ↳11 YES

    ↳12 PiDP

        ↳13 PiDPToQDPProof (⇐)

        ↳14 QDP

        ↳15 QDPSizeChangeProof (⇔)

        ↳16 YES

    ↳17 PiDP

        ↳18 PiDPToQDPProof (⇐)

        ↳19 QDP

        ↳20 QDPSizeChangeProof (⇔)

        ↳21 YES

    ↳22 PiDP

        ↳23 PiDPToQDPProof (⇐)

        ↳24 QDP

        ↳25 QDPSizeChangeProof (⇔)

        ↳26 YES

    ↳27 PiDP

        ↳28 PiDPToQDPProof (⇐)

        ↳29 QDP

        ↳30 QDPSizeChangeProof (⇔)

        ↳31 YES

    ↳32 PiDP

        ↳33 PiDPToQDPProof (⇐)

        ↳34 QDP

        ↳35 QDPSizeChangeProof (⇔)

        ↳36 YES

    ↳37 PiDP

        ↳38 PiDPToQDPProof (⇐)

        ↳39 QDP

        ↳40 QDPSizeChangeProof (⇔)

        ↳41 YES

    ↳42 PiDP

        ↳43 PiDPToQDPProof (⇐)

        ↳44 QDP

        ↳45 QDPSizeChangeProof (⇔)

        ↳46 YES

(0) Obligation:

Clauses:

div(X, Y, Z) :- quot(X, Y, Y, Z).
quot(0, s(Y), s(Z), 0).
quot(s(X), s(Y), Z, U) :- quot(X, Y, Z, U).
quot(X, 0, s(Z), s(U)) :- quot(X, s(Z), s(Z), U).

Queries:

div(g,g,a).

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="1: div(T1, T2, T3)\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
2 [label="2: div(T1, T2, T3), SCOPE: 1, CLAUSE: 0\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
3 [label="3: quot(T7, T8, T8, T10)\n\nT7 is ground\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
4 [label="4: quot(T7, T8, T8, T10), SCOPE: 2, CLAUSE: 1 | quot(T7, T8, T8, T10), SCOPE: 2, CLAUSE: 2 | quot(T7, T8, T8, T10), SCOPE: 2, CLAUSE: 3\n\nT7 is ground\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: quot(T7, T8, T8, T10), SCOPE: 2, CLAUSE: 1\n\nT7 is ground\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: quot(T7, T8, T8, T10), SCOPE: 2, CLAUSE: 2 | quot(T7, T8, T8, T10), SCOPE: 2, CLAUSE: 3\n\nT7 is ground\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: quot(T7, T8, T8, T10), SCOPE: 2, CLAUSE: 2\n\nT7 is ground\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: quot(T7, T8, T8, T10), SCOPE: 2, CLAUSE: 3\n\nT7 is ground\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: quot(T28, T29, s(T29), T31)\n\nT28 is ground\nT29 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: quot(T28, T29, s(T29), T31), SCOPE: 3, CLAUSE: 1 | quot(T28, T29, s(T29), T31), SCOPE: 3, CLAUSE: 2 | quot(T28, T29, s(T29), T31), SCOPE: 3, CLAUSE: 3\n\nT28 is ground\nT29 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: quot(T28, T29, s(T29), T31), SCOPE: 3, CLAUSE: 1\n\nT28 is ground\nT29 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: quot(T28, T29, s(T29), T31), SCOPE: 3, CLAUSE: 2 | quot(T28, T29, s(T29), T31), SCOPE: 3, CLAUSE: 3\n\nT28 is ground\nT29 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: quot(T28, T29, s(T29), T31), SCOPE: 3, CLAUSE: 2\n\nT28 is ground\nT29 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: quot(T28, T29, s(T29), T31), SCOPE: 3, CLAUSE: 3\n\nT28 is ground\nT29 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: quot(T51, T52, s(s(T52)), T54)\n\nT51 is ground\nT52 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: quot(T51, T52, s(s(T52)), T54), SCOPE: 4, CLAUSE: 1 | quot(T51, T52, s(s(T52)), T54), SCOPE: 4, CLAUSE: 2 | quot(T51, T52, s(s(T52)), T54), SCOPE: 4, CLAUSE: 3\n\nT51 is ground\nT52 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: quot(T51, T52, s(s(T52)), T54), SCOPE: 4, CLAUSE: 1\n\nT51 is ground\nT52 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: quot(T51, T52, s(s(T52)), T54), SCOPE: 4, CLAUSE: 2 | quot(T51, T52, s(s(T52)), T54), SCOPE: 4, CLAUSE: 3\n\nT51 is ground\nT52 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: quot(T51, T52, s(s(T52)), T54), SCOPE: 4, CLAUSE: 2\n\nT51 is ground\nT52 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: quot(T51, T52, s(s(T52)), T54), SCOPE: 4, CLAUSE: 3\n\nT51 is ground\nT52 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: quot(T74, T75, s(s(s(T75))), T77)\n\nT74 is ground\nT75 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: quot(T74, T75, s(s(s(T75))), T77), SCOPE: 5, CLAUSE: 1 | quot(T74, T75, s(s(s(T75))), T77), SCOPE: 5, CLAUSE: 2 | quot(T74, T75, s(s(s(T75))), T77), SCOPE: 5, CLAUSE: 3\n\nT74 is ground\nT75 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: quot(T74, T75, s(s(s(T75))), T77), SCOPE: 5, CLAUSE: 1\n\nT74 is ground\nT75 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: quot(T74, T75, s(s(s(T75))), T77), SCOPE: 5, CLAUSE: 2 | quot(T74, T75, s(s(s(T75))), T77), SCOPE: 5, CLAUSE: 3\n\nT74 is ground\nT75 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: quot(T74, T75, s(s(s(T75))), T77), SCOPE: 5, CLAUSE: 2\n\nT74 is ground\nT75 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: quot(T74, T75, s(s(s(T75))), T77), SCOPE: 5, CLAUSE: 3\n\nT74 is ground\nT75 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: quot(T97, T98, s(s(s(s(T98)))), T100)\n\nT97 is ground\nT98 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: quot(T97, T98, s(s(s(s(T98)))), T100), SCOPE: 6, CLAUSE: 1 | quot(T97, T98, s(s(s(s(T98)))), T100), SCOPE: 6, CLAUSE: 2 | quot(T97, T98, s(s(s(s(T98)))), T100), SCOPE: 6, CLAUSE: 3\n\nT97 is ground\nT98 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: quot(T97, T98, s(s(s(s(T98)))), T100), SCOPE: 6, CLAUSE: 1\n\nT97 is ground\nT98 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: quot(T97, T98, s(s(s(s(T98)))), T100), SCOPE: 6, CLAUSE: 2 | quot(T97, T98, s(s(s(s(T98)))), T100), SCOPE: 6, CLAUSE: 3\n\nT97 is ground\nT98 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: quot(T97, T98, s(s(s(s(T98)))), T100), SCOPE: 6, CLAUSE: 2\n\nT97 is ground\nT98 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: quot(T97, T98, s(s(s(s(T98)))), T100), SCOPE: 6, CLAUSE: 3\n\nT97 is ground\nT98 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: quot(T120, T121, s(s(s(s(s(T121))))), T123)\n\nT120 is ground\nT121 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: quot(T120, T121, s(s(s(s(s(T121))))), T123), SCOPE: 7, CLAUSE: 1 | quot(T120, T121, s(s(s(s(s(T121))))), T123), SCOPE: 7, CLAUSE: 2 | quot(T120, T121, s(s(s(s(s(T121))))), T123), SCOPE: 7, CLAUSE: 3\n\nT120 is ground\nT121 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: quot(T120, T121, s(s(s(s(s(T121))))), T123), SCOPE: 7, CLAUSE: 1\n\nT120 is ground\nT121 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: quot(T120, T121, s(s(s(s(s(T121))))), T123), SCOPE: 7, CLAUSE: 2 | quot(T120, T121, s(s(s(s(s(T121))))), T123), SCOPE: 7, CLAUSE: 3\n\nT120 is ground\nT121 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: quot(T120, T121, s(s(s(s(s(T121))))), T123), SCOPE: 7, CLAUSE: 2\n\nT120 is ground\nT121 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: quot(T120, T121, s(s(s(s(s(T121))))), T123), SCOPE: 7, CLAUSE: 3\n\nT120 is ground\nT121 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: quot(T143, T144, s(s(s(s(s(s(T144)))))), T146)\n\nT143 is ground\nT144 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: quot(T143, T144, s(s(s(s(s(s(T144)))))), T146), SCOPE: 8, CLAUSE: 1 | quot(T143, T144, s(s(s(s(s(s(T144)))))), T146), SCOPE: 8, CLAUSE: 2 | quot(T143, T144, s(s(s(s(s(s(T144)))))), T146), SCOPE: 8, CLAUSE: 3\n\nT143 is ground\nT144 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: quot(T143, T144, s(s(s(s(s(s(T144)))))), T146), SCOPE: 8, CLAUSE: 1\n\nT143 is ground\nT144 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: quot(T143, T144, s(s(s(s(s(s(T144)))))), T146), SCOPE: 8, CLAUSE: 2 | quot(T143, T144, s(s(s(s(s(s(T144)))))), T146), SCOPE: 8, CLAUSE: 3\n\nT143 is ground\nT144 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: quot(T143, T144, s(s(s(s(s(s(T144)))))), T146), SCOPE: 8, CLAUSE: 2\n\nT143 is ground\nT144 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: quot(T143, T144, s(s(s(s(s(s(T144)))))), T146), SCOPE: 8, CLAUSE: 3\n\nT143 is ground\nT144 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: quot(T166, T167, s(s(s(s(s(s(s(T167))))))), T169)\n\nT166 is ground\nT167 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: quot(T166, T167, s(s(s(s(s(s(s(T167))))))), T169), SCOPE: 9, CLAUSE: 1 | quot(T166, T167, s(s(s(s(s(s(s(T167))))))), T169), SCOPE: 9, CLAUSE: 2 | quot(T166, T167, s(s(s(s(s(s(s(T167))))))), T169), SCOPE: 9, CLAUSE: 3\n\nT166 is ground\nT167 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: quot(T166, T167, s(s(s(s(s(s(s(T167))))))), T169), SCOPE: 9, CLAUSE: 1\n\nT166 is ground\nT167 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: quot(T166, T167, s(s(s(s(s(s(s(T167))))))), T169), SCOPE: 9, CLAUSE: 2 | quot(T166, T167, s(s(s(s(s(s(s(T167))))))), T169), SCOPE: 9, CLAUSE: 3\n\nT166 is ground\nT167 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: quot(T166, T167, s(s(s(s(s(s(s(T167))))))), T169), SCOPE: 9, CLAUSE: 2\n\nT166 is ground\nT167 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: quot(T166, T167, s(s(s(s(s(s(s(T167))))))), T169), SCOPE: 9, CLAUSE: 3\n\nT166 is ground\nT167 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: quot(T189, T190, s(s(s(s(s(s(s(s(T190)))))))), T192)\n\nT189 is ground\nT190 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: quot(T189, T190, s(T195), T192)\n\nT189 is ground\nT190 is ground\nT195 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: quot(T189, T190, s(T195), T192), SCOPE: 10, CLAUSE: 1 | quot(T189, T190, s(T195), T192), SCOPE: 10, CLAUSE: 2 | quot(T189, T190, s(T195), T192), SCOPE: 10, CLAUSE: 3\n\nT189 is ground\nT190 is ground\nT195 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: quot(T189, T190, s(T195), T192), SCOPE: 10, CLAUSE: 1\n\nT189 is ground\nT190 is ground\nT195 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: quot(T189, T190, s(T195), T192), SCOPE: 10, CLAUSE: 2 | quot(T189, T190, s(T195), T192), SCOPE: 10, CLAUSE: 3\n\nT189 is ground\nT190 is ground\nT195 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: quot(T189, T190, s(T195), T192), SCOPE: 10, CLAUSE: 2\n\nT189 is ground\nT190 is ground\nT195 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: quot(T189, T190, s(T195), T192), SCOPE: 10, CLAUSE: 3\n\nT189 is ground\nT190 is ground\nT195 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: quot(T226, T227, s(T228), T230)\n\nT226 is ground\nT227 is ground\nT228 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: quot(T241, s(T242), s(T242), T244)\n\nT241 is ground\nT242 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: quot(T251, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))), T253)\n\nT251 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: quot(T251, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))), T253), SCOPE: 11, CLAUSE: 1 | quot(T251, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))), T253), SCOPE: 11, CLAUSE: 2 | quot(T251, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))), T253), SCOPE: 11, CLAUSE: 3\n\nT251 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="100: quot(T251, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))), T253), SCOPE: 11, CLAUSE: 1\n\nT251 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="101: quot(T251, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))), T253), SCOPE: 11, CLAUSE: 2 | quot(T251, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))), T253), SCOPE: 11, CLAUSE: 3\n\nT251 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="102: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
103 [label="103: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
105 [label="105: quot(T251, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))), T253), SCOPE: 11, CLAUSE: 2\n\nT251 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="106: quot(T251, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))), T253), SCOPE: 11, CLAUSE: 3\n\nT251 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: quot(T262, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(0))))))), T264)\n\nT262 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="108: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="109: quot(T262, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(0))))))), T264), SCOPE: 12, CLAUSE: 1 | quot(T262, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(0))))))), T264), SCOPE: 12, CLAUSE: 2 | quot(T262, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(0))))))), T264), SCOPE: 12, CLAUSE: 3\n\nT262 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: quot(T262, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(0))))))), T264), SCOPE: 12, CLAUSE: 1\n\nT262 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: quot(T262, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(0))))))), T264), SCOPE: 12, CLAUSE: 2 | quot(T262, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(0))))))), T264), SCOPE: 12, CLAUSE: 3\n\nT262 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
114 [label="114: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
115 [label="115: quot(T262, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(0))))))), T264), SCOPE: 12, CLAUSE: 2\n\nT262 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
116 [label="116: quot(T262, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(0))))))), T264), SCOPE: 12, CLAUSE: 3\n\nT262 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
117 [label="117: quot(T273, s(s(s(s(s(0))))), s(s(s(s(s(s(s(0))))))), T275)\n\nT273 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="118: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
119 [label="119: quot(T273, s(s(s(s(s(0))))), s(s(s(s(s(s(s(0))))))), T275), SCOPE: 13, CLAUSE: 1 | quot(T273, s(s(s(s(s(0))))), s(s(s(s(s(s(s(0))))))), T275), SCOPE: 13, CLAUSE: 2 | quot(T273, s(s(s(s(s(0))))), s(s(s(s(s(s(s(0))))))), T275), SCOPE: 13, CLAUSE: 3\n\nT273 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
120 [label="120: quot(T273, s(s(s(s(s(0))))), s(s(s(s(s(s(s(0))))))), T275), SCOPE: 13, CLAUSE: 1\n\nT273 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
121 [label="121: quot(T273, s(s(s(s(s(0))))), s(s(s(s(s(s(s(0))))))), T275), SCOPE: 13, CLAUSE: 2 | quot(T273, s(s(s(s(s(0))))), s(s(s(s(s(s(s(0))))))), T275), SCOPE: 13, CLAUSE: 3\n\nT273 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
122 [label="122: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
123 [label="123: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
124 [label="124: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
125 [label="125: quot(T273, s(s(s(s(s(0))))), s(s(s(s(s(s(s(0))))))), T275), SCOPE: 13, CLAUSE: 2\n\nT273 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
126 [label="126: quot(T273, s(s(s(s(s(0))))), s(s(s(s(s(s(s(0))))))), T275), SCOPE: 13, CLAUSE: 3\n\nT273 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
127 [label="127: quot(T284, s(s(s(s(0)))), s(s(s(s(s(s(s(0))))))), T286)\n\nT284 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
128 [label="128: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
129 [label="129: quot(T284, s(s(s(s(0)))), s(s(s(s(s(s(s(0))))))), T286), SCOPE: 14, CLAUSE: 1 | quot(T284, s(s(s(s(0)))), s(s(s(s(s(s(s(0))))))), T286), SCOPE: 14, CLAUSE: 2 | quot(T284, s(s(s(s(0)))), s(s(s(s(s(s(s(0))))))), T286), SCOPE: 14, CLAUSE: 3\n\nT284 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
130 [label="130: quot(T284, s(s(s(s(0)))), s(s(s(s(s(s(s(0))))))), T286), SCOPE: 14, CLAUSE: 1\n\nT284 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
131 [label="131: quot(T284, s(s(s(s(0)))), s(s(s(s(s(s(s(0))))))), T286), SCOPE: 14, CLAUSE: 2 | quot(T284, s(s(s(s(0)))), s(s(s(s(s(s(s(0))))))), T286), SCOPE: 14, CLAUSE: 3\n\nT284 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
132 [label="132: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
133 [label="133: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
134 [label="134: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
135 [label="135: quot(T284, s(s(s(s(0)))), s(s(s(s(s(s(s(0))))))), T286), SCOPE: 14, CLAUSE: 2\n\nT284 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
136 [label="136: quot(T284, s(s(s(s(0)))), s(s(s(s(s(s(s(0))))))), T286), SCOPE: 14, CLAUSE: 3\n\nT284 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
137 [label="137: quot(T295, s(s(s(0))), s(s(s(s(s(s(s(0))))))), T297)\n\nT295 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
138 [label="138: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
139 [label="139: quot(T295, s(s(s(0))), s(s(s(s(s(s(s(0))))))), T297), SCOPE: 15, CLAUSE: 1 | quot(T295, s(s(s(0))), s(s(s(s(s(s(s(0))))))), T297), SCOPE: 15, CLAUSE: 2 | quot(T295, s(s(s(0))), s(s(s(s(s(s(s(0))))))), T297), SCOPE: 15, CLAUSE: 3\n\nT295 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
140 [label="140: quot(T295, s(s(s(0))), s(s(s(s(s(s(s(0))))))), T297), SCOPE: 15, CLAUSE: 1\n\nT295 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
141 [label="141: quot(T295, s(s(s(0))), s(s(s(s(s(s(s(0))))))), T297), SCOPE: 15, CLAUSE: 2 | quot(T295, s(s(s(0))), s(s(s(s(s(s(s(0))))))), T297), SCOPE: 15, CLAUSE: 3\n\nT295 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
142 [label="142: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
143 [label="143: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
144 [label="144: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
145 [label="145: quot(T295, s(s(s(0))), s(s(s(s(s(s(s(0))))))), T297), SCOPE: 15, CLAUSE: 2\n\nT295 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
146 [label="146: quot(T295, s(s(s(0))), s(s(s(s(s(s(s(0))))))), T297), SCOPE: 15, CLAUSE: 3\n\nT295 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
147 [label="147: quot(T306, s(s(0)), s(s(s(s(s(s(s(0))))))), T308)\n\nT306 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
148 [label="148: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
149 [label="149: quot(T306, s(s(0)), s(s(s(s(s(s(s(0))))))), T308), SCOPE: 16, CLAUSE: 1 | quot(T306, s(s(0)), s(s(s(s(s(s(s(0))))))), T308), SCOPE: 16, CLAUSE: 2 | quot(T306, s(s(0)), s(s(s(s(s(s(s(0))))))), T308), SCOPE: 16, CLAUSE: 3\n\nT306 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
150 [label="150: quot(T306, s(s(0)), s(s(s(s(s(s(s(0))))))), T308), SCOPE: 16, CLAUSE: 1\n\nT306 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
151 [label="151: quot(T306, s(s(0)), s(s(s(s(s(s(s(0))))))), T308), SCOPE: 16, CLAUSE: 2 | quot(T306, s(s(0)), s(s(s(s(s(s(s(0))))))), T308), SCOPE: 16, CLAUSE: 3\n\nT306 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
152 [label="152: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
153 [label="153: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
154 [label="154: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
155 [label="155: quot(T306, s(s(0)), s(s(s(s(s(s(s(0))))))), T308), SCOPE: 16, CLAUSE: 2\n\nT306 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
156 [label="156: quot(T306, s(s(0)), s(s(s(s(s(s(s(0))))))), T308), SCOPE: 16, CLAUSE: 3\n\nT306 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
157 [label="157: quot(T317, s(0), s(s(s(s(s(s(s(0))))))), T319)\n\nT317 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
158 [label="158: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
159 [label="159: quot(T317, s(0), s(s(s(s(s(s(s(0))))))), T319), SCOPE: 17, CLAUSE: 1 | quot(T317, s(0), s(s(s(s(s(s(s(0))))))), T319), SCOPE: 17, CLAUSE: 2 | quot(T317, s(0), s(s(s(s(s(s(s(0))))))), T319), SCOPE: 17, CLAUSE: 3\n\nT317 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
160 [label="160: quot(T317, s(0), s(s(s(s(s(s(s(0))))))), T319), SCOPE: 17, CLAUSE: 1\n\nT317 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
161 [label="161: quot(T317, s(0), s(s(s(s(s(s(s(0))))))), T319), SCOPE: 17, CLAUSE: 2 | quot(T317, s(0), s(s(s(s(s(s(s(0))))))), T319), SCOPE: 17, CLAUSE: 3\n\nT317 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
162 [label="162: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
163 [label="163: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
164 [label="164: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
165 [label="165: quot(T317, s(0), s(s(s(s(s(s(s(0))))))), T319), SCOPE: 17, CLAUSE: 2\n\nT317 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
166 [label="166: quot(T317, s(0), s(s(s(s(s(s(s(0))))))), T319), SCOPE: 17, CLAUSE: 3\n\nT317 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
167 [label="167: quot(T328, 0, s(s(s(s(s(s(s(0))))))), T330)\n\nT328 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
168 [label="168: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
169 [label="169: quot(T328, 0, s(s(s(s(s(s(s(0))))))), T330), SCOPE: 18, CLAUSE: 1 | quot(T328, 0, s(s(s(s(s(s(s(0))))))), T330), SCOPE: 18, CLAUSE: 2 | quot(T328, 0, s(s(s(s(s(s(s(0))))))), T330), SCOPE: 18, CLAUSE: 3\n\nT328 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
170 [label="170: quot(T328, 0, s(s(s(s(s(s(s(0))))))), T330), SCOPE: 18, CLAUSE: 2 | quot(T328, 0, s(s(s(s(s(s(s(0))))))), T330), SCOPE: 18, CLAUSE: 3\n\nT328 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
171 [label="171: quot(T328, 0, s(s(s(s(s(s(s(0))))))), T330), SCOPE: 18, CLAUSE: 3\n\nT328 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
172 [label="172: quot(T339, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))), T341)\n\nT339 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
173 [label="173: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
174 [label="174: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
175 [label="175: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
176 [label="176: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
177 [label="177: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
178 [label="178: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
179 [label="179: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
180 [label="180: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
181 [label="181: quot(T353, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))), T355)\n\nT353 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
182 [label="182: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
183 [label="183: quot(T353, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))), T355), SCOPE: 19, CLAUSE: 1 | quot(T353, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))), T355), SCOPE: 19, CLAUSE: 2 | quot(T353, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))), T355), SCOPE: 19, CLAUSE: 3\n\nT353 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
184 [label="184: quot(T353, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))), T355), SCOPE: 19, CLAUSE: 1\n\nT353 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
185 [label="185: quot(T353, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))), T355), SCOPE: 19, CLAUSE: 2 | quot(T353, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))), T355), SCOPE: 19, CLAUSE: 3\n\nT353 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
186 [label="186: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
187 [label="187: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
188 [label="188: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
189 [label="189: quot(T353, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))), T355), SCOPE: 19, CLAUSE: 2\n\nT353 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
190 [label="190: quot(T353, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))), T355), SCOPE: 19, CLAUSE: 3\n\nT353 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
191 [label="191: quot(T364, s(s(s(s(s(0))))), s(s(s(s(s(s(0)))))), T366)\n\nT364 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
192 [label="192: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
193 [label="193: quot(T364, s(s(s(s(s(0))))), s(s(s(s(s(s(0)))))), T366), SCOPE: 20, CLAUSE: 1 | quot(T364, s(s(s(s(s(0))))), s(s(s(s(s(s(0)))))), T366), SCOPE: 20, CLAUSE: 2 | quot(T364, s(s(s(s(s(0))))), s(s(s(s(s(s(0)))))), T366), SCOPE: 20, CLAUSE: 3\n\nT364 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
194 [label="194: quot(T364, s(s(s(s(s(0))))), s(s(s(s(s(s(0)))))), T366), SCOPE: 20, CLAUSE: 1\n\nT364 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
195 [label="195: quot(T364, s(s(s(s(s(0))))), s(s(s(s(s(s(0)))))), T366), SCOPE: 20, CLAUSE: 2 | quot(T364, s(s(s(s(s(0))))), s(s(s(s(s(s(0)))))), T366), SCOPE: 20, CLAUSE: 3\n\nT364 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
196 [label="196: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
197 [label="197: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
198 [label="198: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
199 [label="199: quot(T364, s(s(s(s(s(0))))), s(s(s(s(s(s(0)))))), T366), SCOPE: 20, CLAUSE: 2\n\nT364 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
200 [label="200: quot(T364, s(s(s(s(s(0))))), s(s(s(s(s(s(0)))))), T366), SCOPE: 20, CLAUSE: 3\n\nT364 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
201 [label="201: quot(T375, s(s(s(s(0)))), s(s(s(s(s(s(0)))))), T377)\n\nT375 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
202 [label="202: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
203 [label="203: quot(T375, s(s(s(s(0)))), s(s(s(s(s(s(0)))))), T377), SCOPE: 21, CLAUSE: 1 | quot(T375, s(s(s(s(0)))), s(s(s(s(s(s(0)))))), T377), SCOPE: 21, CLAUSE: 2 | quot(T375, s(s(s(s(0)))), s(s(s(s(s(s(0)))))), T377), SCOPE: 21, CLAUSE: 3\n\nT375 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
204 [label="204: quot(T375, s(s(s(s(0)))), s(s(s(s(s(s(0)))))), T377), SCOPE: 21, CLAUSE: 1\n\nT375 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
205 [label="205: quot(T375, s(s(s(s(0)))), s(s(s(s(s(s(0)))))), T377), SCOPE: 21, CLAUSE: 2 | quot(T375, s(s(s(s(0)))), s(s(s(s(s(s(0)))))), T377), SCOPE: 21, CLAUSE: 3\n\nT375 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
206 [label="206: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
207 [label="207: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
208 [label="208: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
209 [label="209: quot(T375, s(s(s(s(0)))), s(s(s(s(s(s(0)))))), T377), SCOPE: 21, CLAUSE: 2\n\nT375 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
210 [label="210: quot(T375, s(s(s(s(0)))), s(s(s(s(s(s(0)))))), T377), SCOPE: 21, CLAUSE: 3\n\nT375 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
211 [label="211: quot(T386, s(s(s(0))), s(s(s(s(s(s(0)))))), T388)\n\nT386 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
212 [label="212: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
213 [label="213: quot(T386, s(s(s(0))), s(s(s(s(s(s(0)))))), T388), SCOPE: 22, CLAUSE: 1 | quot(T386, s(s(s(0))), s(s(s(s(s(s(0)))))), T388), SCOPE: 22, CLAUSE: 2 | quot(T386, s(s(s(0))), s(s(s(s(s(s(0)))))), T388), SCOPE: 22, CLAUSE: 3\n\nT386 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
214 [label="214: quot(T386, s(s(s(0))), s(s(s(s(s(s(0)))))), T388), SCOPE: 22, CLAUSE: 1\n\nT386 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
215 [label="215: quot(T386, s(s(s(0))), s(s(s(s(s(s(0)))))), T388), SCOPE: 22, CLAUSE: 2 | quot(T386, s(s(s(0))), s(s(s(s(s(s(0)))))), T388), SCOPE: 22, CLAUSE: 3\n\nT386 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
216 [label="216: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
217 [label="217: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
218 [label="218: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
219 [label="219: quot(T386, s(s(s(0))), s(s(s(s(s(s(0)))))), T388), SCOPE: 22, CLAUSE: 2\n\nT386 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
220 [label="220: quot(T386, s(s(s(0))), s(s(s(s(s(s(0)))))), T388), SCOPE: 22, CLAUSE: 3\n\nT386 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
221 [label="221: quot(T397, s(s(0)), s(s(s(s(s(s(0)))))), T399)\n\nT397 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
222 [label="222: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
223 [label="223: quot(T397, s(s(0)), s(s(s(s(s(s(0)))))), T399), SCOPE: 23, CLAUSE: 1 | quot(T397, s(s(0)), s(s(s(s(s(s(0)))))), T399), SCOPE: 23, CLAUSE: 2 | quot(T397, s(s(0)), s(s(s(s(s(s(0)))))), T399), SCOPE: 23, CLAUSE: 3\n\nT397 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
224 [label="224: quot(T397, s(s(0)), s(s(s(s(s(s(0)))))), T399), SCOPE: 23, CLAUSE: 1\n\nT397 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
225 [label="225: quot(T397, s(s(0)), s(s(s(s(s(s(0)))))), T399), SCOPE: 23, CLAUSE: 2 | quot(T397, s(s(0)), s(s(s(s(s(s(0)))))), T399), SCOPE: 23, CLAUSE: 3\n\nT397 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
226 [label="226: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
227 [label="227: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
228 [label="228: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
229 [label="229: quot(T397, s(s(0)), s(s(s(s(s(s(0)))))), T399), SCOPE: 23, CLAUSE: 2\n\nT397 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
230 [label="230: quot(T397, s(s(0)), s(s(s(s(s(s(0)))))), T399), SCOPE: 23, CLAUSE: 3\n\nT397 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
231 [label="231: quot(T408, s(0), s(s(s(s(s(s(0)))))), T410)\n\nT408 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
232 [label="232: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
233 [label="233: quot(T408, s(0), s(s(s(s(s(s(0)))))), T410), SCOPE: 24, CLAUSE: 1 | quot(T408, s(0), s(s(s(s(s(s(0)))))), T410), SCOPE: 24, CLAUSE: 2 | quot(T408, s(0), s(s(s(s(s(s(0)))))), T410), SCOPE: 24, CLAUSE: 3\n\nT408 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
234 [label="234: quot(T408, s(0), s(s(s(s(s(s(0)))))), T410), SCOPE: 24, CLAUSE: 1\n\nT408 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
235 [label="235: quot(T408, s(0), s(s(s(s(s(s(0)))))), T410), SCOPE: 24, CLAUSE: 2 | quot(T408, s(0), s(s(s(s(s(s(0)))))), T410), SCOPE: 24, CLAUSE: 3\n\nT408 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
236 [label="236: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
237 [label="237: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
238 [label="238: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
239 [label="239: quot(T408, s(0), s(s(s(s(s(s(0)))))), T410), SCOPE: 24, CLAUSE: 2\n\nT408 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
240 [label="240: quot(T408, s(0), s(s(s(s(s(s(0)))))), T410), SCOPE: 24, CLAUSE: 3\n\nT408 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
241 [label="241: quot(T419, 0, s(s(s(s(s(s(0)))))), T421)\n\nT419 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
242 [label="242: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
243 [label="243: quot(T419, 0, s(s(s(s(s(s(0)))))), T421), SCOPE: 25, CLAUSE: 1 | quot(T419, 0, s(s(s(s(s(s(0)))))), T421), SCOPE: 25, CLAUSE: 2 | quot(T419, 0, s(s(s(s(s(s(0)))))), T421), SCOPE: 25, CLAUSE: 3\n\nT419 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
244 [label="244: quot(T419, 0, s(s(s(s(s(s(0)))))), T421), SCOPE: 25, CLAUSE: 2 | quot(T419, 0, s(s(s(s(s(s(0)))))), T421), SCOPE: 25, CLAUSE: 3\n\nT419 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
245 [label="245: quot(T419, 0, s(s(s(s(s(s(0)))))), T421), SCOPE: 25, CLAUSE: 3\n\nT419 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
246 [label="246: quot(T430, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))), T432)\n\nT430 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
247 [label="247: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
248 [label="248: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
249 [label="249: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
250 [label="250: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
251 [label="251: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
252 [label="252: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
253 [label="253: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
254 [label="254: quot(T443, s(s(s(s(s(0))))), s(s(s(s(s(0))))), T445)\n\nT443 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
255 [label="255: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
256 [label="256: quot(T443, s(s(s(s(s(0))))), s(s(s(s(s(0))))), T445), SCOPE: 26, CLAUSE: 1 | quot(T443, s(s(s(s(s(0))))), s(s(s(s(s(0))))), T445), SCOPE: 26, CLAUSE: 2 | quot(T443, s(s(s(s(s(0))))), s(s(s(s(s(0))))), T445), SCOPE: 26, CLAUSE: 3\n\nT443 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
257 [label="257: quot(T443, s(s(s(s(s(0))))), s(s(s(s(s(0))))), T445), SCOPE: 26, CLAUSE: 1\n\nT443 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
258 [label="258: quot(T443, s(s(s(s(s(0))))), s(s(s(s(s(0))))), T445), SCOPE: 26, CLAUSE: 2 | quot(T443, s(s(s(s(s(0))))), s(s(s(s(s(0))))), T445), SCOPE: 26, CLAUSE: 3\n\nT443 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
259 [label="259: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
260 [label="260: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
261 [label="261: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
262 [label="262: quot(T443, s(s(s(s(s(0))))), s(s(s(s(s(0))))), T445), SCOPE: 26, CLAUSE: 2\n\nT443 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
263 [label="263: quot(T443, s(s(s(s(s(0))))), s(s(s(s(s(0))))), T445), SCOPE: 26, CLAUSE: 3\n\nT443 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
264 [label="264: quot(T454, s(s(s(s(0)))), s(s(s(s(s(0))))), T456)\n\nT454 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
265 [label="265: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
266 [label="266: quot(T454, s(s(s(s(0)))), s(s(s(s(s(0))))), T456), SCOPE: 27, CLAUSE: 1 | quot(T454, s(s(s(s(0)))), s(s(s(s(s(0))))), T456), SCOPE: 27, CLAUSE: 2 | quot(T454, s(s(s(s(0)))), s(s(s(s(s(0))))), T456), SCOPE: 27, CLAUSE: 3\n\nT454 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
267 [label="267: quot(T454, s(s(s(s(0)))), s(s(s(s(s(0))))), T456), SCOPE: 27, CLAUSE: 1\n\nT454 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
268 [label="268: quot(T454, s(s(s(s(0)))), s(s(s(s(s(0))))), T456), SCOPE: 27, CLAUSE: 2 | quot(T454, s(s(s(s(0)))), s(s(s(s(s(0))))), T456), SCOPE: 27, CLAUSE: 3\n\nT454 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
269 [label="269: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
270 [label="270: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
271 [label="271: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
272 [label="272: quot(T454, s(s(s(s(0)))), s(s(s(s(s(0))))), T456), SCOPE: 27, CLAUSE: 2\n\nT454 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
273 [label="273: quot(T454, s(s(s(s(0)))), s(s(s(s(s(0))))), T456), SCOPE: 27, CLAUSE: 3\n\nT454 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
274 [label="274: quot(T465, s(s(s(0))), s(s(s(s(s(0))))), T467)\n\nT465 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
275 [label="275: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
276 [label="276: quot(T465, s(s(s(0))), s(s(s(s(s(0))))), T467), SCOPE: 28, CLAUSE: 1 | quot(T465, s(s(s(0))), s(s(s(s(s(0))))), T467), SCOPE: 28, CLAUSE: 2 | quot(T465, s(s(s(0))), s(s(s(s(s(0))))), T467), SCOPE: 28, CLAUSE: 3\n\nT465 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
277 [label="277: quot(T465, s(s(s(0))), s(s(s(s(s(0))))), T467), SCOPE: 28, CLAUSE: 1\n\nT465 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
278 [label="278: quot(T465, s(s(s(0))), s(s(s(s(s(0))))), T467), SCOPE: 28, CLAUSE: 2 | quot(T465, s(s(s(0))), s(s(s(s(s(0))))), T467), SCOPE: 28, CLAUSE: 3\n\nT465 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
279 [label="279: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
280 [label="280: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
281 [label="281: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
282 [label="282: quot(T465, s(s(s(0))), s(s(s(s(s(0))))), T467), SCOPE: 28, CLAUSE: 2\n\nT465 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
283 [label="283: quot(T465, s(s(s(0))), s(s(s(s(s(0))))), T467), SCOPE: 28, CLAUSE: 3\n\nT465 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
284 [label="284: quot(T476, s(s(0)), s(s(s(s(s(0))))), T478)\n\nT476 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
285 [label="285: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
286 [label="286: quot(T476, s(s(0)), s(s(s(s(s(0))))), T478), SCOPE: 29, CLAUSE: 1 | quot(T476, s(s(0)), s(s(s(s(s(0))))), T478), SCOPE: 29, CLAUSE: 2 | quot(T476, s(s(0)), s(s(s(s(s(0))))), T478), SCOPE: 29, CLAUSE: 3\n\nT476 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
287 [label="287: quot(T476, s(s(0)), s(s(s(s(s(0))))), T478), SCOPE: 29, CLAUSE: 1\n\nT476 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
288 [label="288: quot(T476, s(s(0)), s(s(s(s(s(0))))), T478), SCOPE: 29, CLAUSE: 2 | quot(T476, s(s(0)), s(s(s(s(s(0))))), T478), SCOPE: 29, CLAUSE: 3\n\nT476 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
289 [label="289: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
290 [label="290: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
291 [label="291: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
292 [label="292: quot(T476, s(s(0)), s(s(s(s(s(0))))), T478), SCOPE: 29, CLAUSE: 2\n\nT476 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
293 [label="293: quot(T476, s(s(0)), s(s(s(s(s(0))))), T478), SCOPE: 29, CLAUSE: 3\n\nT476 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
294 [label="294: quot(T487, s(0), s(s(s(s(s(0))))), T489)\n\nT487 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
295 [label="295: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
296 [label="296: quot(T487, s(0), s(s(s(s(s(0))))), T489), SCOPE: 30, CLAUSE: 1 | quot(T487, s(0), s(s(s(s(s(0))))), T489), SCOPE: 30, CLAUSE: 2 | quot(T487, s(0), s(s(s(s(s(0))))), T489), SCOPE: 30, CLAUSE: 3\n\nT487 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
297 [label="297: quot(T487, s(0), s(s(s(s(s(0))))), T489), SCOPE: 30, CLAUSE: 1\n\nT487 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
298 [label="298: quot(T487, s(0), s(s(s(s(s(0))))), T489), SCOPE: 30, CLAUSE: 2 | quot(T487, s(0), s(s(s(s(s(0))))), T489), SCOPE: 30, CLAUSE: 3\n\nT487 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
299 [label="299: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
300 [label="300: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
301 [label="301: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
302 [label="302: quot(T487, s(0), s(s(s(s(s(0))))), T489), SCOPE: 30, CLAUSE: 2\n\nT487 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
303 [label="303: quot(T487, s(0), s(s(s(s(s(0))))), T489), SCOPE: 30, CLAUSE: 3\n\nT487 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
304 [label="304: quot(T498, 0, s(s(s(s(s(0))))), T500)\n\nT498 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
305 [label="305: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
306 [label="306: quot(T498, 0, s(s(s(s(s(0))))), T500), SCOPE: 31, CLAUSE: 1 | quot(T498, 0, s(s(s(s(s(0))))), T500), SCOPE: 31, CLAUSE: 2 | quot(T498, 0, s(s(s(s(s(0))))), T500), SCOPE: 31, CLAUSE: 3\n\nT498 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
307 [label="307: quot(T498, 0, s(s(s(s(s(0))))), T500), SCOPE: 31, CLAUSE: 2 | quot(T498, 0, s(s(s(s(s(0))))), T500), SCOPE: 31, CLAUSE: 3\n\nT498 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
308 [label="308: quot(T498, 0, s(s(s(s(s(0))))), T500), SCOPE: 31, CLAUSE: 3\n\nT498 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
309 [label="309: quot(T509, s(s(s(s(s(0))))), s(s(s(s(s(0))))), T511)\n\nT509 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
310 [label="310: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
311 [label="311: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
312 [label="312: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
313 [label="313: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
314 [label="314: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
315 [label="315: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
316 [label="316: quot(T521, s(s(s(s(0)))), s(s(s(s(0)))), T523)\n\nT521 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
317 [label="317: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
318 [label="318: quot(T521, s(s(s(s(0)))), s(s(s(s(0)))), T523), SCOPE: 32, CLAUSE: 1 | quot(T521, s(s(s(s(0)))), s(s(s(s(0)))), T523), SCOPE: 32, CLAUSE: 2 | quot(T521, s(s(s(s(0)))), s(s(s(s(0)))), T523), SCOPE: 32, CLAUSE: 3\n\nT521 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
319 [label="319: quot(T521, s(s(s(s(0)))), s(s(s(s(0)))), T523), SCOPE: 32, CLAUSE: 1\n\nT521 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
320 [label="320: quot(T521, s(s(s(s(0)))), s(s(s(s(0)))), T523), SCOPE: 32, CLAUSE: 2 | quot(T521, s(s(s(s(0)))), s(s(s(s(0)))), T523), SCOPE: 32, CLAUSE: 3\n\nT521 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
321 [label="321: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
322 [label="322: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
323 [label="323: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
324 [label="324: quot(T521, s(s(s(s(0)))), s(s(s(s(0)))), T523), SCOPE: 32, CLAUSE: 2\n\nT521 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
325 [label="325: quot(T521, s(s(s(s(0)))), s(s(s(s(0)))), T523), SCOPE: 32, CLAUSE: 3\n\nT521 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
326 [label="326: quot(T532, s(s(s(0))), s(s(s(s(0)))), T534)\n\nT532 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
327 [label="327: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
328 [label="328: quot(T532, s(s(s(0))), s(s(s(s(0)))), T534), SCOPE: 33, CLAUSE: 1 | quot(T532, s(s(s(0))), s(s(s(s(0)))), T534), SCOPE: 33, CLAUSE: 2 | quot(T532, s(s(s(0))), s(s(s(s(0)))), T534), SCOPE: 33, CLAUSE: 3\n\nT532 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
329 [label="329: quot(T532, s(s(s(0))), s(s(s(s(0)))), T534), SCOPE: 33, CLAUSE: 1\n\nT532 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
330 [label="330: quot(T532, s(s(s(0))), s(s(s(s(0)))), T534), SCOPE: 33, CLAUSE: 2 | quot(T532, s(s(s(0))), s(s(s(s(0)))), T534), SCOPE: 33, CLAUSE: 3\n\nT532 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
331 [label="331: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
332 [label="332: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
333 [label="333: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
334 [label="334: quot(T532, s(s(s(0))), s(s(s(s(0)))), T534), SCOPE: 33, CLAUSE: 2\n\nT532 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
335 [label="335: quot(T532, s(s(s(0))), s(s(s(s(0)))), T534), SCOPE: 33, CLAUSE: 3\n\nT532 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
336 [label="336: quot(T543, s(s(0)), s(s(s(s(0)))), T545)\n\nT543 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
337 [label="337: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
338 [label="338: quot(T543, s(s(0)), s(s(s(s(0)))), T545), SCOPE: 34, CLAUSE: 1 | quot(T543, s(s(0)), s(s(s(s(0)))), T545), SCOPE: 34, CLAUSE: 2 | quot(T543, s(s(0)), s(s(s(s(0)))), T545), SCOPE: 34, CLAUSE: 3\n\nT543 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
339 [label="339: quot(T543, s(s(0)), s(s(s(s(0)))), T545), SCOPE: 34, CLAUSE: 1\n\nT543 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
340 [label="340: quot(T543, s(s(0)), s(s(s(s(0)))), T545), SCOPE: 34, CLAUSE: 2 | quot(T543, s(s(0)), s(s(s(s(0)))), T545), SCOPE: 34, CLAUSE: 3\n\nT543 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
341 [label="341: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
342 [label="342: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
343 [label="343: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
344 [label="344: quot(T543, s(s(0)), s(s(s(s(0)))), T545), SCOPE: 34, CLAUSE: 2\n\nT543 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
345 [label="345: quot(T543, s(s(0)), s(s(s(s(0)))), T545), SCOPE: 34, CLAUSE: 3\n\nT543 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
346 [label="346: quot(T554, s(0), s(s(s(s(0)))), T556)\n\nT554 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
347 [label="347: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
348 [label="348: quot(T554, s(0), s(s(s(s(0)))), T556), SCOPE: 35, CLAUSE: 1 | quot(T554, s(0), s(s(s(s(0)))), T556), SCOPE: 35, CLAUSE: 2 | quot(T554, s(0), s(s(s(s(0)))), T556), SCOPE: 35, CLAUSE: 3\n\nT554 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
349 [label="349: quot(T554, s(0), s(s(s(s(0)))), T556), SCOPE: 35, CLAUSE: 1\n\nT554 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
350 [label="350: quot(T554, s(0), s(s(s(s(0)))), T556), SCOPE: 35, CLAUSE: 2 | quot(T554, s(0), s(s(s(s(0)))), T556), SCOPE: 35, CLAUSE: 3\n\nT554 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
351 [label="351: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
352 [label="352: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
353 [label="353: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
354 [label="354: quot(T554, s(0), s(s(s(s(0)))), T556), SCOPE: 35, CLAUSE: 2\n\nT554 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
355 [label="355: quot(T554, s(0), s(s(s(s(0)))), T556), SCOPE: 35, CLAUSE: 3\n\nT554 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
356 [label="356: quot(T565, 0, s(s(s(s(0)))), T567)\n\nT565 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
357 [label="357: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
358 [label="358: quot(T565, 0, s(s(s(s(0)))), T567), SCOPE: 36, CLAUSE: 1 | quot(T565, 0, s(s(s(s(0)))), T567), SCOPE: 36, CLAUSE: 2 | quot(T565, 0, s(s(s(s(0)))), T567), SCOPE: 36, CLAUSE: 3\n\nT565 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
359 [label="359: quot(T565, 0, s(s(s(s(0)))), T567), SCOPE: 36, CLAUSE: 2 | quot(T565, 0, s(s(s(s(0)))), T567), SCOPE: 36, CLAUSE: 3\n\nT565 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
360 [label="360: quot(T565, 0, s(s(s(s(0)))), T567), SCOPE: 36, CLAUSE: 3\n\nT565 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
361 [label="361: quot(T576, s(s(s(s(0)))), s(s(s(s(0)))), T578)\n\nT576 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
362 [label="362: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
363 [label="363: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
364 [label="364: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
365 [label="365: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
366 [label="366: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
367 [label="367: quot(T587, s(s(s(0))), s(s(s(0))), T589)\n\nT587 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
368 [label="368: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
369 [label="369: quot(T587, s(s(s(0))), s(s(s(0))), T589), SCOPE: 37, CLAUSE: 1 | quot(T587, s(s(s(0))), s(s(s(0))), T589), SCOPE: 37, CLAUSE: 2 | quot(T587, s(s(s(0))), s(s(s(0))), T589), SCOPE: 37, CLAUSE: 3\n\nT587 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
370 [label="370: quot(T587, s(s(s(0))), s(s(s(0))), T589), SCOPE: 37, CLAUSE: 1\n\nT587 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
371 [label="371: quot(T587, s(s(s(0))), s(s(s(0))), T589), SCOPE: 37, CLAUSE: 2 | quot(T587, s(s(s(0))), s(s(s(0))), T589), SCOPE: 37, CLAUSE: 3\n\nT587 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
372 [label="372: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
373 [label="373: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
374 [label="374: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
375 [label="375: quot(T587, s(s(s(0))), s(s(s(0))), T589), SCOPE: 37, CLAUSE: 2\n\nT587 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
376 [label="376: quot(T587, s(s(s(0))), s(s(s(0))), T589), SCOPE: 37, CLAUSE: 3\n\nT587 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
377 [label="377: quot(T598, s(s(0)), s(s(s(0))), T600)\n\nT598 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
378 [label="378: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
379 [label="379: quot(T598, s(s(0)), s(s(s(0))), T600), SCOPE: 38, CLAUSE: 1 | quot(T598, s(s(0)), s(s(s(0))), T600), SCOPE: 38, CLAUSE: 2 | quot(T598, s(s(0)), s(s(s(0))), T600), SCOPE: 38, CLAUSE: 3\n\nT598 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
380 [label="380: quot(T598, s(s(0)), s(s(s(0))), T600), SCOPE: 38, CLAUSE: 1\n\nT598 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
381 [label="381: quot(T598, s(s(0)), s(s(s(0))), T600), SCOPE: 38, CLAUSE: 2 | quot(T598, s(s(0)), s(s(s(0))), T600), SCOPE: 38, CLAUSE: 3\n\nT598 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
382 [label="382: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
383 [label="383: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
384 [label="384: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
385 [label="385: quot(T598, s(s(0)), s(s(s(0))), T600), SCOPE: 38, CLAUSE: 2\n\nT598 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
386 [label="386: quot(T598, s(s(0)), s(s(s(0))), T600), SCOPE: 38, CLAUSE: 3\n\nT598 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
387 [label="387: quot(T609, s(0), s(s(s(0))), T611)\n\nT609 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
388 [label="388: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
389 [label="389: quot(T609, s(0), s(s(s(0))), T611), SCOPE: 39, CLAUSE: 1 | quot(T609, s(0), s(s(s(0))), T611), SCOPE: 39, CLAUSE: 2 | quot(T609, s(0), s(s(s(0))), T611), SCOPE: 39, CLAUSE: 3\n\nT609 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
390 [label="390: quot(T609, s(0), s(s(s(0))), T611), SCOPE: 39, CLAUSE: 1\n\nT609 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
391 [label="391: quot(T609, s(0), s(s(s(0))), T611), SCOPE: 39, CLAUSE: 2 | quot(T609, s(0), s(s(s(0))), T611), SCOPE: 39, CLAUSE: 3\n\nT609 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
392 [label="392: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
393 [label="393: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
394 [label="394: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
395 [label="395: quot(T609, s(0), s(s(s(0))), T611), SCOPE: 39, CLAUSE: 2\n\nT609 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
396 [label="396: quot(T609, s(0), s(s(s(0))), T611), SCOPE: 39, CLAUSE: 3\n\nT609 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
397 [label="397: quot(T620, 0, s(s(s(0))), T622)\n\nT620 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
398 [label="398: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
399 [label="399: quot(T620, 0, s(s(s(0))), T622), SCOPE: 40, CLAUSE: 1 | quot(T620, 0, s(s(s(0))), T622), SCOPE: 40, CLAUSE: 2 | quot(T620, 0, s(s(s(0))), T622), SCOPE: 40, CLAUSE: 3\n\nT620 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
400 [label="400: quot(T620, 0, s(s(s(0))), T622), SCOPE: 40, CLAUSE: 2 | quot(T620, 0, s(s(s(0))), T622), SCOPE: 40, CLAUSE: 3\n\nT620 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
401 [label="401: quot(T620, 0, s(s(s(0))), T622), SCOPE: 40, CLAUSE: 3\n\nT620 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
402 [label="402: quot(T631, s(s(s(0))), s(s(s(0))), T633)\n\nT631 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
403 [label="403: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
404 [label="404: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
405 [label="405: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
406 [label="406: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
407 [label="407: quot(T641, s(s(0)), s(s(0)), T643)\n\nT641 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
408 [label="408: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
409 [label="409: quot(T641, s(s(0)), s(s(0)), T643), SCOPE: 41, CLAUSE: 1 | quot(T641, s(s(0)), s(s(0)), T643), SCOPE: 41, CLAUSE: 2 | quot(T641, s(s(0)), s(s(0)), T643), SCOPE: 41, CLAUSE: 3\n\nT641 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
410 [label="410: quot(T641, s(s(0)), s(s(0)), T643), SCOPE: 41, CLAUSE: 1\n\nT641 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
411 [label="411: quot(T641, s(s(0)), s(s(0)), T643), SCOPE: 41, CLAUSE: 2 | quot(T641, s(s(0)), s(s(0)), T643), SCOPE: 41, CLAUSE: 3\n\nT641 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
412 [label="412: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
413 [label="413: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
414 [label="414: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
415 [label="415: quot(T641, s(s(0)), s(s(0)), T643), SCOPE: 41, CLAUSE: 2\n\nT641 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
416 [label="416: quot(T641, s(s(0)), s(s(0)), T643), SCOPE: 41, CLAUSE: 3\n\nT641 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
417 [label="417: quot(T652, s(0), s(s(0)), T654)\n\nT652 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
418 [label="418: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
419 [label="419: quot(T652, s(0), s(s(0)), T654), SCOPE: 42, CLAUSE: 1 | quot(T652, s(0), s(s(0)), T654), SCOPE: 42, CLAUSE: 2 | quot(T652, s(0), s(s(0)), T654), SCOPE: 42, CLAUSE: 3\n\nT652 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
420 [label="420: quot(T652, s(0), s(s(0)), T654), SCOPE: 42, CLAUSE: 1\n\nT652 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
421 [label="421: quot(T652, s(0), s(s(0)), T654), SCOPE: 42, CLAUSE: 2 | quot(T652, s(0), s(s(0)), T654), SCOPE: 42, CLAUSE: 3\n\nT652 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
422 [label="422: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
423 [label="423: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
424 [label="424: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
425 [label="425: quot(T652, s(0), s(s(0)), T654), SCOPE: 42, CLAUSE: 2\n\nT652 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
426 [label="426: quot(T652, s(0), s(s(0)), T654), SCOPE: 42, CLAUSE: 3\n\nT652 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
427 [label="427: quot(T663, 0, s(s(0)), T665)\n\nT663 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
428 [label="428: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
429 [label="429: quot(T663, 0, s(s(0)), T665), SCOPE: 43, CLAUSE: 1 | quot(T663, 0, s(s(0)), T665), SCOPE: 43, CLAUSE: 2 | quot(T663, 0, s(s(0)), T665), SCOPE: 43, CLAUSE: 3\n\nT663 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
430 [label="430: quot(T663, 0, s(s(0)), T665), SCOPE: 43, CLAUSE: 2 | quot(T663, 0, s(s(0)), T665), SCOPE: 43, CLAUSE: 3\n\nT663 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
431 [label="431: quot(T663, 0, s(s(0)), T665), SCOPE: 43, CLAUSE: 3\n\nT663 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
432 [label="432: quot(T674, s(s(0)), s(s(0)), T676)\n\nT674 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
433 [label="433: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
434 [label="434: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
435 [label="435: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
436 [label="436: quot(T683, s(0), s(0), T685)\n\nT683 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
437 [label="437: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
438 [label="438: quot(T683, s(0), s(0), T685), SCOPE: 44, CLAUSE: 1 | quot(T683, s(0), s(0), T685), SCOPE: 44, CLAUSE: 2 | quot(T683, s(0), s(0), T685), SCOPE: 44, CLAUSE: 3\n\nT683 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
439 [label="439: quot(T683, s(0), s(0), T685), SCOPE: 44, CLAUSE: 1\n\nT683 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
440 [label="440: quot(T683, s(0), s(0), T685), SCOPE: 44, CLAUSE: 2 | quot(T683, s(0), s(0), T685), SCOPE: 44, CLAUSE: 3\n\nT683 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
441 [label="441: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
442 [label="442: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
443 [label="443: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
444 [label="444: quot(T683, s(0), s(0), T685), SCOPE: 44, CLAUSE: 2\n\nT683 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
445 [label="445: quot(T683, s(0), s(0), T685), SCOPE: 44, CLAUSE: 3\n\nT683 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
446 [label="446: quot(T694, 0, s(0), T696)\n\nT694 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
447 [label="447: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
448 [label="448: quot(T694, 0, s(0), T696), SCOPE: 45, CLAUSE: 1 | quot(T694, 0, s(0), T696), SCOPE: 45, CLAUSE: 2 | quot(T694, 0, s(0), T696), SCOPE: 45, CLAUSE: 3\n\nT694 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
449 [label="449: quot(T694, 0, s(0), T696), SCOPE: 45, CLAUSE: 2 | quot(T694, 0, s(0), T696), SCOPE: 45, CLAUSE: 3\n\nT694 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
450 [label="450: quot(T694, 0, s(0), T696), SCOPE: 45, CLAUSE: 3\n\nT694 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
451 [label="451: quot(T705, s(0), s(0), T707)\n\nT705 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
452 [label="452: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
453 [label="453: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
454 [label="454: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
455 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 455 [arrowhead = none ];
455 -> 2;

456 [label="ONLY EVAL with clause\ndiv(X4, X5, X6) :- quot(X4, X5, X5, X6).\nand substitution\nT1 -> T7\nX4 -> T7\nT2 -> T8\nX5 -> T8\nT3 -> T10\nX6 -> T10\nT9 -> T10", fontsize=14, style = filled, fillcolor = white];
2 -> 456 [arrowhead = none ];
456 -> 3;

457 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
3 -> 457 [arrowhead = none ];
457 -> 4;

458 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
4 -> 458 [arrowhead = none ];
458 -> 5;

459 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
4 -> 459 [arrowhead = none ];
459 -> 6;

460 [label="EVAL with clause\nquot(0, s(X15), s(X16), 0).\nand substitution\nT7 -> 0\nX15 -> T15\nT8 -> s(T15)\nX16 -> T15\nT10 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
5 -> 460 [arrowhead = none ];
460 -> 7;

461 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
5 -> 461 [arrowhead = none ];
461 -> 8;

462 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
6 -> 462 [arrowhead = none ];
462 -> 10;

463 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
6 -> 463 [arrowhead = none ];
463 -> 11;

464 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
7 -> 464 [arrowhead = none ];
464 -> 9;

465 [label="EVAL with clause\nquot(s(X35), s(X36), X37, X38) :- quot(X35, X36, X37, X38).\nand substitution\nX35 -> T28\nT7 -> s(T28)\nX36 -> T29\nT8 -> s(T29)\nX37 -> s(T29)\nT10 -> T31\nX38 -> T31\nT30 -> T31", fontsize=14, style = filled, fillcolor = lightblue];
10 -> 465 [arrowhead = none ];
465 -> 12;

466 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
10 -> 466 [arrowhead = none ];
466 -> 13;

467 [label="BACKTRACK\nfor clause: quot(X, 0, s(Z), s(U)) :- quot(X, s(Z), s(Z), U)because of non-unification", fontsize=14, style = filled, fillcolor = white];
11 -> 467 [arrowhead = none ];
467 -> 454;

468 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
12 -> 468 [arrowhead = none ];
468 -> 14;

469 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
14 -> 469 [arrowhead = none ];
469 -> 15;

470 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
14 -> 470 [arrowhead = none ];
470 -> 16;

471 [label="EVAL with clause\nquot(0, s(X55), s(X56), 0).\nand substitution\nT28 -> 0\nX55 -> T38\nT29 -> s(T38)\nX56 -> s(T38)\nT31 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
15 -> 471 [arrowhead = none ];
471 -> 17;

472 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
15 -> 472 [arrowhead = none ];
472 -> 18;

473 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
16 -> 473 [arrowhead = none ];
473 -> 20;

474 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
16 -> 474 [arrowhead = none ];
474 -> 21;

475 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
17 -> 475 [arrowhead = none ];
475 -> 19;

476 [label="EVAL with clause\nquot(s(X75), s(X76), X77, X78) :- quot(X75, X76, X77, X78).\nand substitution\nX75 -> T51\nT28 -> s(T51)\nX76 -> T52\nT29 -> s(T52)\nX77 -> s(s(T52))\nT31 -> T54\nX78 -> T54\nT53 -> T54", fontsize=14, style = filled, fillcolor = lightblue];
20 -> 476 [arrowhead = none ];
476 -> 22;

477 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
20 -> 477 [arrowhead = none ];
477 -> 23;

478 [label="EVAL with clause\nquot(X1824, 0, s(X1825), s(X1826)) :- quot(X1824, s(X1825), s(X1825), X1826).\nand substitution\nT28 -> T683\nX1824 -> T683\nT29 -> 0\nX1825 -> 0\nX1826 -> T685\nT31 -> s(T685)\nT684 -> T685", fontsize=14, style = filled, fillcolor = lightblue];
21 -> 478 [arrowhead = none ];
478 -> 436;

479 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
21 -> 479 [arrowhead = none ];
479 -> 437;

480 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
22 -> 480 [arrowhead = none ];
480 -> 24;

481 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
24 -> 481 [arrowhead = none ];
481 -> 25;

482 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
24 -> 482 [arrowhead = none ];
482 -> 26;

483 [label="EVAL with clause\nquot(0, s(X95), s(X96), 0).\nand substitution\nT51 -> 0\nX95 -> T61\nT52 -> s(T61)\nX96 -> s(s(T61))\nT54 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
25 -> 483 [arrowhead = none ];
483 -> 27;

484 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
25 -> 484 [arrowhead = none ];
484 -> 28;

485 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
26 -> 485 [arrowhead = none ];
485 -> 30;

486 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
26 -> 486 [arrowhead = none ];
486 -> 31;

487 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
27 -> 487 [arrowhead = none ];
487 -> 29;

488 [label="EVAL with clause\nquot(s(X115), s(X116), X117, X118) :- quot(X115, X116, X117, X118).\nand substitution\nX115 -> T74\nT51 -> s(T74)\nX116 -> T75\nT52 -> s(T75)\nX117 -> s(s(s(T75)))\nT54 -> T77\nX118 -> T77\nT76 -> T77", fontsize=14, style = filled, fillcolor = lightblue];
30 -> 488 [arrowhead = none ];
488 -> 32;

489 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
30 -> 489 [arrowhead = none ];
489 -> 33;

490 [label="EVAL with clause\nquot(X1693, 0, s(X1694), s(X1695)) :- quot(X1693, s(X1694), s(X1694), X1695).\nand substitution\nT51 -> T641\nX1693 -> T641\nT52 -> 0\nX1694 -> s(0)\nX1695 -> T643\nT54 -> s(T643)\nT642 -> T643", fontsize=14, style = filled, fillcolor = lightblue];
31 -> 490 [arrowhead = none ];
490 -> 407;

491 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
31 -> 491 [arrowhead = none ];
491 -> 408;

492 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
32 -> 492 [arrowhead = none ];
492 -> 34;

493 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
34 -> 493 [arrowhead = none ];
493 -> 35;

494 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
34 -> 494 [arrowhead = none ];
494 -> 36;

495 [label="EVAL with clause\nquot(0, s(X135), s(X136), 0).\nand substitution\nT74 -> 0\nX135 -> T84\nT75 -> s(T84)\nX136 -> s(s(s(T84)))\nT77 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
35 -> 495 [arrowhead = none ];
495 -> 37;

496 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
35 -> 496 [arrowhead = none ];
496 -> 38;

497 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
36 -> 497 [arrowhead = none ];
497 -> 40;

498 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
36 -> 498 [arrowhead = none ];
498 -> 41;

499 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
37 -> 499 [arrowhead = none ];
499 -> 39;

500 [label="EVAL with clause\nquot(s(X155), s(X156), X157, X158) :- quot(X155, X156, X157, X158).\nand substitution\nX155 -> T97\nT74 -> s(T97)\nX156 -> T98\nT75 -> s(T98)\nX157 -> s(s(s(s(T98))))\nT77 -> T100\nX158 -> T100\nT99 -> T100", fontsize=14, style = filled, fillcolor = lightblue];
40 -> 500 [arrowhead = none ];
500 -> 42;

501 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
40 -> 501 [arrowhead = none ];
501 -> 43;

502 [label="EVAL with clause\nquot(X1519, 0, s(X1520), s(X1521)) :- quot(X1519, s(X1520), s(X1520), X1521).\nand substitution\nT74 -> T587\nX1519 -> T587\nT75 -> 0\nX1520 -> s(s(0))\nX1521 -> T589\nT77 -> s(T589)\nT588 -> T589", fontsize=14, style = filled, fillcolor = lightblue];
41 -> 502 [arrowhead = none ];
502 -> 367;

503 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
41 -> 503 [arrowhead = none ];
503 -> 368;

504 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
42 -> 504 [arrowhead = none ];
504 -> 44;

505 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
44 -> 505 [arrowhead = none ];
505 -> 45;

506 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
44 -> 506 [arrowhead = none ];
506 -> 46;

507 [label="EVAL with clause\nquot(0, s(X175), s(X176), 0).\nand substitution\nT97 -> 0\nX175 -> T107\nT98 -> s(T107)\nX176 -> s(s(s(s(T107))))\nT100 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
45 -> 507 [arrowhead = none ];
507 -> 47;

508 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
45 -> 508 [arrowhead = none ];
508 -> 48;

509 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
46 -> 509 [arrowhead = none ];
509 -> 50;

510 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
46 -> 510 [arrowhead = none ];
510 -> 51;

511 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
47 -> 511 [arrowhead = none ];
511 -> 49;

512 [label="EVAL with clause\nquot(s(X195), s(X196), X197, X198) :- quot(X195, X196, X197, X198).\nand substitution\nX195 -> T120\nT97 -> s(T120)\nX196 -> T121\nT98 -> s(T121)\nX197 -> s(s(s(s(s(T121)))))\nT100 -> T123\nX198 -> T123\nT122 -> T123", fontsize=14, style = filled, fillcolor = lightblue];
50 -> 512 [arrowhead = none ];
512 -> 52;

513 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
50 -> 513 [arrowhead = none ];
513 -> 53;

514 [label="EVAL with clause\nquot(X1302, 0, s(X1303), s(X1304)) :- quot(X1302, s(X1303), s(X1303), X1304).\nand substitution\nT97 -> T521\nX1302 -> T521\nT98 -> 0\nX1303 -> s(s(s(0)))\nX1304 -> T523\nT100 -> s(T523)\nT522 -> T523", fontsize=14, style = filled, fillcolor = lightblue];
51 -> 514 [arrowhead = none ];
514 -> 316;

515 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
51 -> 515 [arrowhead = none ];
515 -> 317;

516 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
52 -> 516 [arrowhead = none ];
516 -> 54;

517 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
54 -> 517 [arrowhead = none ];
517 -> 55;

518 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
54 -> 518 [arrowhead = none ];
518 -> 56;

519 [label="EVAL with clause\nquot(0, s(X215), s(X216), 0).\nand substitution\nT120 -> 0\nX215 -> T130\nT121 -> s(T130)\nX216 -> s(s(s(s(s(T130)))))\nT123 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
55 -> 519 [arrowhead = none ];
519 -> 57;

520 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
55 -> 520 [arrowhead = none ];
520 -> 58;

521 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
56 -> 521 [arrowhead = none ];
521 -> 60;

522 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
56 -> 522 [arrowhead = none ];
522 -> 61;

523 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
57 -> 523 [arrowhead = none ];
523 -> 59;

524 [label="EVAL with clause\nquot(s(X235), s(X236), X237, X238) :- quot(X235, X236, X237, X238).\nand substitution\nX235 -> T143\nT120 -> s(T143)\nX236 -> T144\nT121 -> s(T144)\nX237 -> s(s(s(s(s(s(T144))))))\nT123 -> T146\nX238 -> T146\nT145 -> T146", fontsize=14, style = filled, fillcolor = lightblue];
60 -> 524 [arrowhead = none ];
524 -> 62;

525 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
60 -> 525 [arrowhead = none ];
525 -> 63;

526 [label="EVAL with clause\nquot(X1042, 0, s(X1043), s(X1044)) :- quot(X1042, s(X1043), s(X1043), X1044).\nand substitution\nT120 -> T443\nX1042 -> T443\nT121 -> 0\nX1043 -> s(s(s(s(0))))\nX1044 -> T445\nT123 -> s(T445)\nT444 -> T445", fontsize=14, style = filled, fillcolor = lightblue];
61 -> 526 [arrowhead = none ];
526 -> 254;

527 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
61 -> 527 [arrowhead = none ];
527 -> 255;

528 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
62 -> 528 [arrowhead = none ];
528 -> 64;

529 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
64 -> 529 [arrowhead = none ];
529 -> 65;

530 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
64 -> 530 [arrowhead = none ];
530 -> 66;

531 [label="EVAL with clause\nquot(0, s(X255), s(X256), 0).\nand substitution\nT143 -> 0\nX255 -> T153\nT144 -> s(T153)\nX256 -> s(s(s(s(s(s(T153))))))\nT146 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
65 -> 531 [arrowhead = none ];
531 -> 67;

532 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
65 -> 532 [arrowhead = none ];
532 -> 68;

533 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
66 -> 533 [arrowhead = none ];
533 -> 70;

534 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
66 -> 534 [arrowhead = none ];
534 -> 71;

535 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
67 -> 535 [arrowhead = none ];
535 -> 69;

536 [label="EVAL with clause\nquot(s(X275), s(X276), X277, X278) :- quot(X275, X276, X277, X278).\nand substitution\nX275 -> T166\nT143 -> s(T166)\nX276 -> T167\nT144 -> s(T167)\nX277 -> s(s(s(s(s(s(s(T167)))))))\nT146 -> T169\nX278 -> T169\nT168 -> T169", fontsize=14, style = filled, fillcolor = lightblue];
70 -> 536 [arrowhead = none ];
536 -> 72;

537 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
70 -> 537 [arrowhead = none ];
537 -> 73;

538 [label="EVAL with clause\nquot(X739, 0, s(X740), s(X741)) :- quot(X739, s(X740), s(X740), X741).\nand substitution\nT143 -> T353\nX739 -> T353\nT144 -> 0\nX740 -> s(s(s(s(s(0)))))\nX741 -> T355\nT146 -> s(T355)\nT354 -> T355", fontsize=14, style = filled, fillcolor = lightblue];
71 -> 538 [arrowhead = none ];
538 -> 181;

539 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
71 -> 539 [arrowhead = none ];
539 -> 182;

540 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
72 -> 540 [arrowhead = none ];
540 -> 74;

541 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
74 -> 541 [arrowhead = none ];
541 -> 75;

542 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
74 -> 542 [arrowhead = none ];
542 -> 76;

543 [label="EVAL with clause\nquot(0, s(X295), s(X296), 0).\nand substitution\nT166 -> 0\nX295 -> T176\nT167 -> s(T176)\nX296 -> s(s(s(s(s(s(s(T176)))))))\nT169 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
75 -> 543 [arrowhead = none ];
543 -> 77;

544 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
75 -> 544 [arrowhead = none ];
544 -> 78;

545 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
76 -> 545 [arrowhead = none ];
545 -> 80;

546 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
76 -> 546 [arrowhead = none ];
546 -> 81;

547 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
77 -> 547 [arrowhead = none ];
547 -> 79;

548 [label="EVAL with clause\nquot(s(X315), s(X316), X317, X318) :- quot(X315, X316, X317, X318).\nand substitution\nX315 -> T189\nT166 -> s(T189)\nX316 -> T190\nT167 -> s(T190)\nX317 -> s(s(s(s(s(s(s(s(T190))))))))\nT169 -> T192\nX318 -> T192\nT191 -> T192", fontsize=14, style = filled, fillcolor = lightblue];
80 -> 548 [arrowhead = none ];
548 -> 82;

549 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
80 -> 549 [arrowhead = none ];
549 -> 83;

550 [label="EVAL with clause\nquot(X393, 0, s(X394), s(X395)) :- quot(X393, s(X394), s(X394), X395).\nand substitution\nT166 -> T251\nX393 -> T251\nT167 -> 0\nX394 -> s(s(s(s(s(s(0))))))\nX395 -> T253\nT169 -> s(T253)\nT252 -> T253", fontsize=14, style = filled, fillcolor = lightblue];
81 -> 550 [arrowhead = none ];
550 -> 97;

551 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
81 -> 551 [arrowhead = none ];
551 -> 98;

552 [label="GENERALIZATION\nT195 <-- s(s(s(s(s(s(s(T190)))))))\n\nNew Knowledge:\nT195 is ground", fontsize=14, style = filled, fillcolor = violet];
82 -> 552 [arrowhead = none ];
552 -> 84;

553 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
84 -> 553 [arrowhead = none ];
553 -> 85;

554 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
85 -> 554 [arrowhead = none ];
554 -> 86;

555 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
85 -> 555 [arrowhead = none ];
555 -> 87;

556 [label="EVAL with clause\nquot(0, s(X339), s(X340), 0).\nand substitution\nT189 -> 0\nX339 -> T208\nT190 -> s(T208)\nT195 -> T209\nX340 -> T209\nT192 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
86 -> 556 [arrowhead = none ];
556 -> 88;

557 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
86 -> 557 [arrowhead = none ];
557 -> 89;

558 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
87 -> 558 [arrowhead = none ];
558 -> 91;

559 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
87 -> 559 [arrowhead = none ];
559 -> 92;

560 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
88 -> 560 [arrowhead = none ];
560 -> 90;

561 [label="EVAL with clause\nquot(s(X359), s(X360), X361, X362) :- quot(X359, X360, X361, X362).\nand substitution\nX359 -> T226\nT189 -> s(T226)\nX360 -> T227\nT190 -> s(T227)\nT195 -> T228\nX361 -> s(T228)\nT192 -> T230\nX362 -> T230\nT229 -> T230", fontsize=14, style = filled, fillcolor = lightblue];
91 -> 561 [arrowhead = none ];
561 -> 93;

562 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
91 -> 562 [arrowhead = none ];
562 -> 94;

563 [label="EVAL with clause\nquot(X377, 0, s(X378), s(X379)) :- quot(X377, s(X378), s(X378), X379).\nand substitution\nT189 -> T241\nX377 -> T241\nT190 -> 0\nT195 -> T242\nX378 -> T242\nX379 -> T244\nT192 -> s(T244)\nT243 -> T244", fontsize=14, style = filled, fillcolor = lightblue];
92 -> 563 [arrowhead = none ];
563 -> 95;

564 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
92 -> 564 [arrowhead = none ];
564 -> 96;

565 [label="INSTANCE with matching:\nT189 -> T226\nT190 -> T227\nT195 -> T228\nT192 -> T230", fontsize=14, style = filled, fillcolor = lightgrey];
93 -> 565 [arrowhead = none , style=dashed];
565 -> 84[style=dashed];

566 [label="INSTANCE with matching:\nT7 -> T241\nT8 -> s(T242)\nT10 -> T244", fontsize=14, style = filled, fillcolor = lightgrey];
95 -> 566 [arrowhead = none , style=dashed];
566 -> 3[style=dashed];

567 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
97 -> 567 [arrowhead = none ];
567 -> 99;

568 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
99 -> 568 [arrowhead = none ];
568 -> 100;

569 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
99 -> 569 [arrowhead = none ];
569 -> 101;

570 [label="EVAL with clause\nquot(0, s(X411), s(X412), 0).\nand substitution\nT251 -> 0\nX411 -> s(s(s(s(s(s(0))))))\nX412 -> s(s(s(s(s(s(0))))))\nT253 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
100 -> 570 [arrowhead = none ];
570 -> 102;

571 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
100 -> 571 [arrowhead = none ];
571 -> 103;

572 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
101 -> 572 [arrowhead = none ];
572 -> 105;

573 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
101 -> 573 [arrowhead = none ];
573 -> 106;

574 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
102 -> 574 [arrowhead = none ];
574 -> 104;

575 [label="EVAL with clause\nquot(s(X431), s(X432), X433, X434) :- quot(X431, X432, X433, X434).\nand substitution\nX431 -> T262\nT251 -> s(T262)\nX432 -> s(s(s(s(s(s(0))))))\nX433 -> s(s(s(s(s(s(s(0)))))))\nT253 -> T264\nX434 -> T264\nT263 -> T264", fontsize=14, style = filled, fillcolor = lightblue];
105 -> 575 [arrowhead = none ];
575 -> 107;

576 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
105 -> 576 [arrowhead = none ];
576 -> 108;

577 [label="BACKTRACK\nfor clause: quot(X, 0, s(Z), s(U)) :- quot(X, s(Z), s(Z), U)because of non-unification", fontsize=14, style = filled, fillcolor = white];
106 -> 577 [arrowhead = none ];
577 -> 180;

578 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
107 -> 578 [arrowhead = none ];
578 -> 109;

579 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
109 -> 579 [arrowhead = none ];
579 -> 110;

580 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
109 -> 580 [arrowhead = none ];
580 -> 111;

581 [label="EVAL with clause\nquot(0, s(X451), s(X452), 0).\nand substitution\nT262 -> 0\nX451 -> s(s(s(s(s(0)))))\nX452 -> s(s(s(s(s(s(0))))))\nT264 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
110 -> 581 [arrowhead = none ];
581 -> 112;

582 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
110 -> 582 [arrowhead = none ];
582 -> 113;

583 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
111 -> 583 [arrowhead = none ];
583 -> 115;

584 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
111 -> 584 [arrowhead = none ];
584 -> 116;

585 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
112 -> 585 [arrowhead = none ];
585 -> 114;

586 [label="EVAL with clause\nquot(s(X471), s(X472), X473, X474) :- quot(X471, X472, X473, X474).\nand substitution\nX471 -> T273\nT262 -> s(T273)\nX472 -> s(s(s(s(s(0)))))\nX473 -> s(s(s(s(s(s(s(0)))))))\nT264 -> T275\nX474 -> T275\nT274 -> T275", fontsize=14, style = filled, fillcolor = lightblue];
115 -> 586 [arrowhead = none ];
586 -> 117;

587 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
115 -> 587 [arrowhead = none ];
587 -> 118;

588 [label="BACKTRACK\nfor clause: quot(X, 0, s(Z), s(U)) :- quot(X, s(Z), s(Z), U)because of non-unification", fontsize=14, style = filled, fillcolor = white];
116 -> 588 [arrowhead = none ];
588 -> 179;

589 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
117 -> 589 [arrowhead = none ];
589 -> 119;

590 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
119 -> 590 [arrowhead = none ];
590 -> 120;

591 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
119 -> 591 [arrowhead = none ];
591 -> 121;

592 [label="EVAL with clause\nquot(0, s(X491), s(X492), 0).\nand substitution\nT273 -> 0\nX491 -> s(s(s(s(0))))\nX492 -> s(s(s(s(s(s(0))))))\nT275 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
120 -> 592 [arrowhead = none ];
592 -> 122;

593 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
120 -> 593 [arrowhead = none ];
593 -> 123;

594 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
121 -> 594 [arrowhead = none ];
594 -> 125;

595 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
121 -> 595 [arrowhead = none ];
595 -> 126;

596 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
122 -> 596 [arrowhead = none ];
596 -> 124;

597 [label="EVAL with clause\nquot(s(X511), s(X512), X513, X514) :- quot(X511, X512, X513, X514).\nand substitution\nX511 -> T284\nT273 -> s(T284)\nX512 -> s(s(s(s(0))))\nX513 -> s(s(s(s(s(s(s(0)))))))\nT275 -> T286\nX514 -> T286\nT285 -> T286", fontsize=14, style = filled, fillcolor = lightblue];
125 -> 597 [arrowhead = none ];
597 -> 127;

598 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
125 -> 598 [arrowhead = none ];
598 -> 128;

599 [label="BACKTRACK\nfor clause: quot(X, 0, s(Z), s(U)) :- quot(X, s(Z), s(Z), U)because of non-unification", fontsize=14, style = filled, fillcolor = white];
126 -> 599 [arrowhead = none ];
599 -> 178;

600 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
127 -> 600 [arrowhead = none ];
600 -> 129;

601 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
129 -> 601 [arrowhead = none ];
601 -> 130;

602 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
129 -> 602 [arrowhead = none ];
602 -> 131;

603 [label="EVAL with clause\nquot(0, s(X531), s(X532), 0).\nand substitution\nT284 -> 0\nX531 -> s(s(s(0)))\nX532 -> s(s(s(s(s(s(0))))))\nT286 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
130 -> 603 [arrowhead = none ];
603 -> 132;

604 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
130 -> 604 [arrowhead = none ];
604 -> 133;

605 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
131 -> 605 [arrowhead = none ];
605 -> 135;

606 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
131 -> 606 [arrowhead = none ];
606 -> 136;

607 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
132 -> 607 [arrowhead = none ];
607 -> 134;

608 [label="EVAL with clause\nquot(s(X551), s(X552), X553, X554) :- quot(X551, X552, X553, X554).\nand substitution\nX551 -> T295\nT284 -> s(T295)\nX552 -> s(s(s(0)))\nX553 -> s(s(s(s(s(s(s(0)))))))\nT286 -> T297\nX554 -> T297\nT296 -> T297", fontsize=14, style = filled, fillcolor = lightblue];
135 -> 608 [arrowhead = none ];
608 -> 137;

609 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
135 -> 609 [arrowhead = none ];
609 -> 138;

610 [label="BACKTRACK\nfor clause: quot(X, 0, s(Z), s(U)) :- quot(X, s(Z), s(Z), U)because of non-unification", fontsize=14, style = filled, fillcolor = white];
136 -> 610 [arrowhead = none ];
610 -> 177;

611 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
137 -> 611 [arrowhead = none ];
611 -> 139;

612 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
139 -> 612 [arrowhead = none ];
612 -> 140;

613 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
139 -> 613 [arrowhead = none ];
613 -> 141;

614 [label="EVAL with clause\nquot(0, s(X571), s(X572), 0).\nand substitution\nT295 -> 0\nX571 -> s(s(0))\nX572 -> s(s(s(s(s(s(0))))))\nT297 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
140 -> 614 [arrowhead = none ];
614 -> 142;

615 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
140 -> 615 [arrowhead = none ];
615 -> 143;

616 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
141 -> 616 [arrowhead = none ];
616 -> 145;

617 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
141 -> 617 [arrowhead = none ];
617 -> 146;

618 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
142 -> 618 [arrowhead = none ];
618 -> 144;

619 [label="EVAL with clause\nquot(s(X591), s(X592), X593, X594) :- quot(X591, X592, X593, X594).\nand substitution\nX591 -> T306\nT295 -> s(T306)\nX592 -> s(s(0))\nX593 -> s(s(s(s(s(s(s(0)))))))\nT297 -> T308\nX594 -> T308\nT307 -> T308", fontsize=14, style = filled, fillcolor = lightblue];
145 -> 619 [arrowhead = none ];
619 -> 147;

620 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
145 -> 620 [arrowhead = none ];
620 -> 148;

621 [label="BACKTRACK\nfor clause: quot(X, 0, s(Z), s(U)) :- quot(X, s(Z), s(Z), U)because of non-unification", fontsize=14, style = filled, fillcolor = white];
146 -> 621 [arrowhead = none ];
621 -> 176;

622 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
147 -> 622 [arrowhead = none ];
622 -> 149;

623 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
149 -> 623 [arrowhead = none ];
623 -> 150;

624 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
149 -> 624 [arrowhead = none ];
624 -> 151;

625 [label="EVAL with clause\nquot(0, s(X611), s(X612), 0).\nand substitution\nT306 -> 0\nX611 -> s(0)\nX612 -> s(s(s(s(s(s(0))))))\nT308 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
150 -> 625 [arrowhead = none ];
625 -> 152;

626 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
150 -> 626 [arrowhead = none ];
626 -> 153;

627 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
151 -> 627 [arrowhead = none ];
627 -> 155;

628 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
151 -> 628 [arrowhead = none ];
628 -> 156;

629 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
152 -> 629 [arrowhead = none ];
629 -> 154;

630 [label="EVAL with clause\nquot(s(X631), s(X632), X633, X634) :- quot(X631, X632, X633, X634).\nand substitution\nX631 -> T317\nT306 -> s(T317)\nX632 -> s(0)\nX633 -> s(s(s(s(s(s(s(0)))))))\nT308 -> T319\nX634 -> T319\nT318 -> T319", fontsize=14, style = filled, fillcolor = lightblue];
155 -> 630 [arrowhead = none ];
630 -> 157;

631 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
155 -> 631 [arrowhead = none ];
631 -> 158;

632 [label="BACKTRACK\nfor clause: quot(X, 0, s(Z), s(U)) :- quot(X, s(Z), s(Z), U)because of non-unification", fontsize=14, style = filled, fillcolor = white];
156 -> 632 [arrowhead = none ];
632 -> 175;

633 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
157 -> 633 [arrowhead = none ];
633 -> 159;

634 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
159 -> 634 [arrowhead = none ];
634 -> 160;

635 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
159 -> 635 [arrowhead = none ];
635 -> 161;

636 [label="EVAL with clause\nquot(0, s(X651), s(X652), 0).\nand substitution\nT317 -> 0\nX651 -> 0\nX652 -> s(s(s(s(s(s(0))))))\nT319 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
160 -> 636 [arrowhead = none ];
636 -> 162;

637 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
160 -> 637 [arrowhead = none ];
637 -> 163;

638 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
161 -> 638 [arrowhead = none ];
638 -> 165;

639 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
161 -> 639 [arrowhead = none ];
639 -> 166;

640 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
162 -> 640 [arrowhead = none ];
640 -> 164;

641 [label="EVAL with clause\nquot(s(X671), s(X672), X673, X674) :- quot(X671, X672, X673, X674).\nand substitution\nX671 -> T328\nT317 -> s(T328)\nX672 -> 0\nX673 -> s(s(s(s(s(s(s(0)))))))\nT319 -> T330\nX674 -> T330\nT329 -> T330", fontsize=14, style = filled, fillcolor = lightblue];
165 -> 641 [arrowhead = none ];
641 -> 167;

642 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
165 -> 642 [arrowhead = none ];
642 -> 168;

643 [label="BACKTRACK\nfor clause: quot(X, 0, s(Z), s(U)) :- quot(X, s(Z), s(Z), U)because of non-unification", fontsize=14, style = filled, fillcolor = white];
166 -> 643 [arrowhead = none ];
643 -> 174;

644 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
167 -> 644 [arrowhead = none ];
644 -> 169;

645 [label="BACKTRACK\nfor clause: quot(0, s(Y), s(Z), 0)because of non-unification", fontsize=14, style = filled, fillcolor = white];
169 -> 645 [arrowhead = none ];
645 -> 170;

646 [label="BACKTRACK\nfor clause: quot(s(X), s(Y), Z, U) :- quot(X, Y, Z, U)because of non-unification", fontsize=14, style = filled, fillcolor = white];
170 -> 646 [arrowhead = none ];
646 -> 171;

647 [label="EVAL with clause\nquot(X702, 0, s(X703), s(X704)) :- quot(X702, s(X703), s(X703), X704).\nand substitution\nT328 -> T339\nX702 -> T339\nX703 -> s(s(s(s(s(s(0))))))\nX704 -> T341\nT330 -> s(T341)\nT340 -> T341", fontsize=14, style = filled, fillcolor = lightblue];
171 -> 647 [arrowhead = none ];
647 -> 172;

648 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
171 -> 648 [arrowhead = none ];
648 -> 173;

649 [label="INSTANCE with matching:\nT251 -> T339\nT253 -> T341", fontsize=14, style = filled, fillcolor = lightgrey];
172 -> 649 [arrowhead = none , style=dashed];
649 -> 97[style=dashed];

650 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
181 -> 650 [arrowhead = none ];
650 -> 183;

651 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
183 -> 651 [arrowhead = none ];
651 -> 184;

652 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
183 -> 652 [arrowhead = none ];
652 -> 185;

653 [label="EVAL with clause\nquot(0, s(X757), s(X758), 0).\nand substitution\nT353 -> 0\nX757 -> s(s(s(s(s(0)))))\nX758 -> s(s(s(s(s(0)))))\nT355 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
184 -> 653 [arrowhead = none ];
653 -> 186;

654 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
184 -> 654 [arrowhead = none ];
654 -> 187;

655 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
185 -> 655 [arrowhead = none ];
655 -> 189;

656 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
185 -> 656 [arrowhead = none ];
656 -> 190;

657 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
186 -> 657 [arrowhead = none ];
657 -> 188;

658 [label="EVAL with clause\nquot(s(X777), s(X778), X779, X780) :- quot(X777, X778, X779, X780).\nand substitution\nX777 -> T364\nT353 -> s(T364)\nX778 -> s(s(s(s(s(0)))))\nX779 -> s(s(s(s(s(s(0))))))\nT355 -> T366\nX780 -> T366\nT365 -> T366", fontsize=14, style = filled, fillcolor = lightblue];
189 -> 658 [arrowhead = none ];
658 -> 191;

659 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
189 -> 659 [arrowhead = none ];
659 -> 192;

660 [label="BACKTRACK\nfor clause: quot(X, 0, s(Z), s(U)) :- quot(X, s(Z), s(Z), U)because of non-unification", fontsize=14, style = filled, fillcolor = white];
190 -> 660 [arrowhead = none ];
660 -> 253;

661 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
191 -> 661 [arrowhead = none ];
661 -> 193;

662 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
193 -> 662 [arrowhead = none ];
662 -> 194;

663 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
193 -> 663 [arrowhead = none ];
663 -> 195;

664 [label="EVAL with clause\nquot(0, s(X797), s(X798), 0).\nand substitution\nT364 -> 0\nX797 -> s(s(s(s(0))))\nX798 -> s(s(s(s(s(0)))))\nT366 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
194 -> 664 [arrowhead = none ];
664 -> 196;

665 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
194 -> 665 [arrowhead = none ];
665 -> 197;

666 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
195 -> 666 [arrowhead = none ];
666 -> 199;

667 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
195 -> 667 [arrowhead = none ];
667 -> 200;

668 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
196 -> 668 [arrowhead = none ];
668 -> 198;

669 [label="EVAL with clause\nquot(s(X817), s(X818), X819, X820) :- quot(X817, X818, X819, X820).\nand substitution\nX817 -> T375\nT364 -> s(T375)\nX818 -> s(s(s(s(0))))\nX819 -> s(s(s(s(s(s(0))))))\nT366 -> T377\nX820 -> T377\nT376 -> T377", fontsize=14, style = filled, fillcolor = lightblue];
199 -> 669 [arrowhead = none ];
669 -> 201;

670 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
199 -> 670 [arrowhead = none ];
670 -> 202;

671 [label="BACKTRACK\nfor clause: quot(X, 0, s(Z), s(U)) :- quot(X, s(Z), s(Z), U)because of non-unification", fontsize=14, style = filled, fillcolor = white];
200 -> 671 [arrowhead = none ];
671 -> 252;

672 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
201 -> 672 [arrowhead = none ];
672 -> 203;

673 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
203 -> 673 [arrowhead = none ];
673 -> 204;

674 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
203 -> 674 [arrowhead = none ];
674 -> 205;

675 [label="EVAL with clause\nquot(0, s(X837), s(X838), 0).\nand substitution\nT375 -> 0\nX837 -> s(s(s(0)))\nX838 -> s(s(s(s(s(0)))))\nT377 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
204 -> 675 [arrowhead = none ];
675 -> 206;

676 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
204 -> 676 [arrowhead = none ];
676 -> 207;

677 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
205 -> 677 [arrowhead = none ];
677 -> 209;

678 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
205 -> 678 [arrowhead = none ];
678 -> 210;

679 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
206 -> 679 [arrowhead = none ];
679 -> 208;

680 [label="EVAL with clause\nquot(s(X857), s(X858), X859, X860) :- quot(X857, X858, X859, X860).\nand substitution\nX857 -> T386\nT375 -> s(T386)\nX858 -> s(s(s(0)))\nX859 -> s(s(s(s(s(s(0))))))\nT377 -> T388\nX860 -> T388\nT387 -> T388", fontsize=14, style = filled, fillcolor = lightblue];
209 -> 680 [arrowhead = none ];
680 -> 211;

681 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
209 -> 681 [arrowhead = none ];
681 -> 212;

682 [label="BACKTRACK\nfor clause: quot(X, 0, s(Z), s(U)) :- quot(X, s(Z), s(Z), U)because of non-unification", fontsize=14, style = filled, fillcolor = white];
210 -> 682 [arrowhead = none ];
682 -> 251;

683 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
211 -> 683 [arrowhead = none ];
683 -> 213;

684 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
213 -> 684 [arrowhead = none ];
684 -> 214;

685 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
213 -> 685 [arrowhead = none ];
685 -> 215;

686 [label="EVAL with clause\nquot(0, s(X877), s(X878), 0).\nand substitution\nT386 -> 0\nX877 -> s(s(0))\nX878 -> s(s(s(s(s(0)))))\nT388 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
214 -> 686 [arrowhead = none ];
686 -> 216;

687 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
214 -> 687 [arrowhead = none ];
687 -> 217;

688 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
215 -> 688 [arrowhead = none ];
688 -> 219;

689 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
215 -> 689 [arrowhead = none ];
689 -> 220;

690 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
216 -> 690 [arrowhead = none ];
690 -> 218;

691 [label="EVAL with clause\nquot(s(X897), s(X898), X899, X900) :- quot(X897, X898, X899, X900).\nand substitution\nX897 -> T397\nT386 -> s(T397)\nX898 -> s(s(0))\nX899 -> s(s(s(s(s(s(0))))))\nT388 -> T399\nX900 -> T399\nT398 -> T399", fontsize=14, style = filled, fillcolor = lightblue];
219 -> 691 [arrowhead = none ];
691 -> 221;

692 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
219 -> 692 [arrowhead = none ];
692 -> 222;

693 [label="BACKTRACK\nfor clause: quot(X, 0, s(Z), s(U)) :- quot(X, s(Z), s(Z), U)because of non-unification", fontsize=14, style = filled, fillcolor = white];
220 -> 693 [arrowhead = none ];
693 -> 250;

694 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
221 -> 694 [arrowhead = none ];
694 -> 223;

695 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
223 -> 695 [arrowhead = none ];
695 -> 224;

696 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
223 -> 696 [arrowhead = none ];
696 -> 225;

697 [label="EVAL with clause\nquot(0, s(X917), s(X918), 0).\nand substitution\nT397 -> 0\nX917 -> s(0)\nX918 -> s(s(s(s(s(0)))))\nT399 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
224 -> 697 [arrowhead = none ];
697 -> 226;

698 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
224 -> 698 [arrowhead = none ];
698 -> 227;

699 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
225 -> 699 [arrowhead = none ];
699 -> 229;

700 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
225 -> 700 [arrowhead = none ];
700 -> 230;

701 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
226 -> 701 [arrowhead = none ];
701 -> 228;

702 [label="EVAL with clause\nquot(s(X937), s(X938), X939, X940) :- quot(X937, X938, X939, X940).\nand substitution\nX937 -> T408\nT397 -> s(T408)\nX938 -> s(0)\nX939 -> s(s(s(s(s(s(0))))))\nT399 -> T410\nX940 -> T410\nT409 -> T410", fontsize=14, style = filled, fillcolor = lightblue];
229 -> 702 [arrowhead = none ];
702 -> 231;

703 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
229 -> 703 [arrowhead = none ];
703 -> 232;

704 [label="BACKTRACK\nfor clause: quot(X, 0, s(Z), s(U)) :- quot(X, s(Z), s(Z), U)because of non-unification", fontsize=14, style = filled, fillcolor = white];
230 -> 704 [arrowhead = none ];
704 -> 249;

705 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
231 -> 705 [arrowhead = none ];
705 -> 233;

706 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
233 -> 706 [arrowhead = none ];
706 -> 234;

707 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
233 -> 707 [arrowhead = none ];
707 -> 235;

708 [label="EVAL with clause\nquot(0, s(X957), s(X958), 0).\nand substitution\nT408 -> 0\nX957 -> 0\nX958 -> s(s(s(s(s(0)))))\nT410 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
234 -> 708 [arrowhead = none ];
708 -> 236;

709 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
234 -> 709 [arrowhead = none ];
709 -> 237;

710 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
235 -> 710 [arrowhead = none ];
710 -> 239;

711 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
235 -> 711 [arrowhead = none ];
711 -> 240;

712 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
236 -> 712 [arrowhead = none ];
712 -> 238;

713 [label="EVAL with clause\nquot(s(X977), s(X978), X979, X980) :- quot(X977, X978, X979, X980).\nand substitution\nX977 -> T419\nT408 -> s(T419)\nX978 -> 0\nX979 -> s(s(s(s(s(s(0))))))\nT410 -> T421\nX980 -> T421\nT420 -> T421", fontsize=14, style = filled, fillcolor = lightblue];
239 -> 713 [arrowhead = none ];
713 -> 241;

714 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
239 -> 714 [arrowhead = none ];
714 -> 242;

715 [label="BACKTRACK\nfor clause: quot(X, 0, s(Z), s(U)) :- quot(X, s(Z), s(Z), U)because of non-unification", fontsize=14, style = filled, fillcolor = white];
240 -> 715 [arrowhead = none ];
715 -> 248;

716 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
241 -> 716 [arrowhead = none ];
716 -> 243;

717 [label="BACKTRACK\nfor clause: quot(0, s(Y), s(Z), 0)because of non-unification", fontsize=14, style = filled, fillcolor = white];
243 -> 717 [arrowhead = none ];
717 -> 244;

718 [label="BACKTRACK\nfor clause: quot(s(X), s(Y), Z, U) :- quot(X, Y, Z, U)because of non-unification", fontsize=14, style = filled, fillcolor = white];
244 -> 718 [arrowhead = none ];
718 -> 245;

719 [label="EVAL with clause\nquot(X1008, 0, s(X1009), s(X1010)) :- quot(X1008, s(X1009), s(X1009), X1010).\nand substitution\nT419 -> T430\nX1008 -> T430\nX1009 -> s(s(s(s(s(0)))))\nX1010 -> T432\nT421 -> s(T432)\nT431 -> T432", fontsize=14, style = filled, fillcolor = lightblue];
245 -> 719 [arrowhead = none ];
719 -> 246;

720 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
245 -> 720 [arrowhead = none ];
720 -> 247;

721 [label="INSTANCE with matching:\nT353 -> T430\nT355 -> T432", fontsize=14, style = filled, fillcolor = lightgrey];
246 -> 721 [arrowhead = none , style=dashed];
721 -> 181[style=dashed];

722 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
254 -> 722 [arrowhead = none ];
722 -> 256;

723 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
256 -> 723 [arrowhead = none ];
723 -> 257;

724 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
256 -> 724 [arrowhead = none ];
724 -> 258;

725 [label="EVAL with clause\nquot(0, s(X1060), s(X1061), 0).\nand substitution\nT443 -> 0\nX1060 -> s(s(s(s(0))))\nX1061 -> s(s(s(s(0))))\nT445 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
257 -> 725 [arrowhead = none ];
725 -> 259;

726 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
257 -> 726 [arrowhead = none ];
726 -> 260;

727 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
258 -> 727 [arrowhead = none ];
727 -> 262;

728 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
258 -> 728 [arrowhead = none ];
728 -> 263;

729 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
259 -> 729 [arrowhead = none ];
729 -> 261;

730 [label="EVAL with clause\nquot(s(X1080), s(X1081), X1082, X1083) :- quot(X1080, X1081, X1082, X1083).\nand substitution\nX1080 -> T454\nT443 -> s(T454)\nX1081 -> s(s(s(s(0))))\nX1082 -> s(s(s(s(s(0)))))\nT445 -> T456\nX1083 -> T456\nT455 -> T456", fontsize=14, style = filled, fillcolor = lightblue];
262 -> 730 [arrowhead = none ];
730 -> 264;

731 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
262 -> 731 [arrowhead = none ];
731 -> 265;

732 [label="BACKTRACK\nfor clause: quot(X, 0, s(Z), s(U)) :- quot(X, s(Z), s(Z), U)because of non-unification", fontsize=14, style = filled, fillcolor = white];
263 -> 732 [arrowhead = none ];
732 -> 315;

733 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
264 -> 733 [arrowhead = none ];
733 -> 266;

734 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
266 -> 734 [arrowhead = none ];
734 -> 267;

735 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
266 -> 735 [arrowhead = none ];
735 -> 268;

736 [label="EVAL with clause\nquot(0, s(X1100), s(X1101), 0).\nand substitution\nT454 -> 0\nX1100 -> s(s(s(0)))\nX1101 -> s(s(s(s(0))))\nT456 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
267 -> 736 [arrowhead = none ];
736 -> 269;

737 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
267 -> 737 [arrowhead = none ];
737 -> 270;

738 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
268 -> 738 [arrowhead = none ];
738 -> 272;

739 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
268 -> 739 [arrowhead = none ];
739 -> 273;

740 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
269 -> 740 [arrowhead = none ];
740 -> 271;

741 [label="EVAL with clause\nquot(s(X1120), s(X1121), X1122, X1123) :- quot(X1120, X1121, X1122, X1123).\nand substitution\nX1120 -> T465\nT454 -> s(T465)\nX1121 -> s(s(s(0)))\nX1122 -> s(s(s(s(s(0)))))\nT456 -> T467\nX1123 -> T467\nT466 -> T467", fontsize=14, style = filled, fillcolor = lightblue];
272 -> 741 [arrowhead = none ];
741 -> 274;

742 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
272 -> 742 [arrowhead = none ];
742 -> 275;

743 [label="BACKTRACK\nfor clause: quot(X, 0, s(Z), s(U)) :- quot(X, s(Z), s(Z), U)because of non-unification", fontsize=14, style = filled, fillcolor = white];
273 -> 743 [arrowhead = none ];
743 -> 314;

744 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
274 -> 744 [arrowhead = none ];
744 -> 276;

745 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
276 -> 745 [arrowhead = none ];
745 -> 277;

746 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
276 -> 746 [arrowhead = none ];
746 -> 278;

747 [label="EVAL with clause\nquot(0, s(X1140), s(X1141), 0).\nand substitution\nT465 -> 0\nX1140 -> s(s(0))\nX1141 -> s(s(s(s(0))))\nT467 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
277 -> 747 [arrowhead = none ];
747 -> 279;

748 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
277 -> 748 [arrowhead = none ];
748 -> 280;

749 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
278 -> 749 [arrowhead = none ];
749 -> 282;

750 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
278 -> 750 [arrowhead = none ];
750 -> 283;

751 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
279 -> 751 [arrowhead = none ];
751 -> 281;

752 [label="EVAL with clause\nquot(s(X1160), s(X1161), X1162, X1163) :- quot(X1160, X1161, X1162, X1163).\nand substitution\nX1160 -> T476\nT465 -> s(T476)\nX1161 -> s(s(0))\nX1162 -> s(s(s(s(s(0)))))\nT467 -> T478\nX1163 -> T478\nT477 -> T478", fontsize=14, style = filled, fillcolor = lightblue];
282 -> 752 [arrowhead = none ];
752 -> 284;

753 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
282 -> 753 [arrowhead = none ];
753 -> 285;

754 [label="BACKTRACK\nfor clause: quot(X, 0, s(Z), s(U)) :- quot(X, s(Z), s(Z), U)because of non-unification", fontsize=14, style = filled, fillcolor = white];
283 -> 754 [arrowhead = none ];
754 -> 313;

755 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
284 -> 755 [arrowhead = none ];
755 -> 286;

756 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
286 -> 756 [arrowhead = none ];
756 -> 287;

757 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
286 -> 757 [arrowhead = none ];
757 -> 288;

758 [label="EVAL with clause\nquot(0, s(X1180), s(X1181), 0).\nand substitution\nT476 -> 0\nX1180 -> s(0)\nX1181 -> s(s(s(s(0))))\nT478 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
287 -> 758 [arrowhead = none ];
758 -> 289;

759 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
287 -> 759 [arrowhead = none ];
759 -> 290;

760 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
288 -> 760 [arrowhead = none ];
760 -> 292;

761 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
288 -> 761 [arrowhead = none ];
761 -> 293;

762 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
289 -> 762 [arrowhead = none ];
762 -> 291;

763 [label="EVAL with clause\nquot(s(X1200), s(X1201), X1202, X1203) :- quot(X1200, X1201, X1202, X1203).\nand substitution\nX1200 -> T487\nT476 -> s(T487)\nX1201 -> s(0)\nX1202 -> s(s(s(s(s(0)))))\nT478 -> T489\nX1203 -> T489\nT488 -> T489", fontsize=14, style = filled, fillcolor = lightblue];
292 -> 763 [arrowhead = none ];
763 -> 294;

764 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
292 -> 764 [arrowhead = none ];
764 -> 295;

765 [label="BACKTRACK\nfor clause: quot(X, 0, s(Z), s(U)) :- quot(X, s(Z), s(Z), U)because of non-unification", fontsize=14, style = filled, fillcolor = white];
293 -> 765 [arrowhead = none ];
765 -> 312;

766 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
294 -> 766 [arrowhead = none ];
766 -> 296;

767 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
296 -> 767 [arrowhead = none ];
767 -> 297;

768 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
296 -> 768 [arrowhead = none ];
768 -> 298;

769 [label="EVAL with clause\nquot(0, s(X1220), s(X1221), 0).\nand substitution\nT487 -> 0\nX1220 -> 0\nX1221 -> s(s(s(s(0))))\nT489 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
297 -> 769 [arrowhead = none ];
769 -> 299;

770 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
297 -> 770 [arrowhead = none ];
770 -> 300;

771 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
298 -> 771 [arrowhead = none ];
771 -> 302;

772 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
298 -> 772 [arrowhead = none ];
772 -> 303;

773 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
299 -> 773 [arrowhead = none ];
773 -> 301;

774 [label="EVAL with clause\nquot(s(X1240), s(X1241), X1242, X1243) :- quot(X1240, X1241, X1242, X1243).\nand substitution\nX1240 -> T498\nT487 -> s(T498)\nX1241 -> 0\nX1242 -> s(s(s(s(s(0)))))\nT489 -> T500\nX1243 -> T500\nT499 -> T500", fontsize=14, style = filled, fillcolor = lightblue];
302 -> 774 [arrowhead = none ];
774 -> 304;

775 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
302 -> 775 [arrowhead = none ];
775 -> 305;

776 [label="BACKTRACK\nfor clause: quot(X, 0, s(Z), s(U)) :- quot(X, s(Z), s(Z), U)because of non-unification", fontsize=14, style = filled, fillcolor = white];
303 -> 776 [arrowhead = none ];
776 -> 311;

777 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
304 -> 777 [arrowhead = none ];
777 -> 306;

778 [label="BACKTRACK\nfor clause: quot(0, s(Y), s(Z), 0)because of non-unification", fontsize=14, style = filled, fillcolor = white];
306 -> 778 [arrowhead = none ];
778 -> 307;

779 [label="BACKTRACK\nfor clause: quot(s(X), s(Y), Z, U) :- quot(X, Y, Z, U)because of non-unification", fontsize=14, style = filled, fillcolor = white];
307 -> 779 [arrowhead = none ];
779 -> 308;

780 [label="EVAL with clause\nquot(X1271, 0, s(X1272), s(X1273)) :- quot(X1271, s(X1272), s(X1272), X1273).\nand substitution\nT498 -> T509\nX1271 -> T509\nX1272 -> s(s(s(s(0))))\nX1273 -> T511\nT500 -> s(T511)\nT510 -> T511", fontsize=14, style = filled, fillcolor = lightblue];
308 -> 780 [arrowhead = none ];
780 -> 309;

781 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
308 -> 781 [arrowhead = none ];
781 -> 310;

782 [label="INSTANCE with matching:\nT443 -> T509\nT445 -> T511", fontsize=14, style = filled, fillcolor = lightgrey];
309 -> 782 [arrowhead = none , style=dashed];
782 -> 254[style=dashed];

783 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
316 -> 783 [arrowhead = none ];
783 -> 318;

784 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
318 -> 784 [arrowhead = none ];
784 -> 319;

785 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
318 -> 785 [arrowhead = none ];
785 -> 320;

786 [label="EVAL with clause\nquot(0, s(X1320), s(X1321), 0).\nand substitution\nT521 -> 0\nX1320 -> s(s(s(0)))\nX1321 -> s(s(s(0)))\nT523 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
319 -> 786 [arrowhead = none ];
786 -> 321;

787 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
319 -> 787 [arrowhead = none ];
787 -> 322;

788 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
320 -> 788 [arrowhead = none ];
788 -> 324;

789 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
320 -> 789 [arrowhead = none ];
789 -> 325;

790 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
321 -> 790 [arrowhead = none ];
790 -> 323;

791 [label="EVAL with clause\nquot(s(X1340), s(X1341), X1342, X1343) :- quot(X1340, X1341, X1342, X1343).\nand substitution\nX1340 -> T532\nT521 -> s(T532)\nX1341 -> s(s(s(0)))\nX1342 -> s(s(s(s(0))))\nT523 -> T534\nX1343 -> T534\nT533 -> T534", fontsize=14, style = filled, fillcolor = lightblue];
324 -> 791 [arrowhead = none ];
791 -> 326;

792 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
324 -> 792 [arrowhead = none ];
792 -> 327;

793 [label="BACKTRACK\nfor clause: quot(X, 0, s(Z), s(U)) :- quot(X, s(Z), s(Z), U)because of non-unification", fontsize=14, style = filled, fillcolor = white];
325 -> 793 [arrowhead = none ];
793 -> 366;

794 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
326 -> 794 [arrowhead = none ];
794 -> 328;

795 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
328 -> 795 [arrowhead = none ];
795 -> 329;

796 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
328 -> 796 [arrowhead = none ];
796 -> 330;

797 [label="EVAL with clause\nquot(0, s(X1360), s(X1361), 0).\nand substitution\nT532 -> 0\nX1360 -> s(s(0))\nX1361 -> s(s(s(0)))\nT534 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
329 -> 797 [arrowhead = none ];
797 -> 331;

798 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
329 -> 798 [arrowhead = none ];
798 -> 332;

799 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
330 -> 799 [arrowhead = none ];
799 -> 334;

800 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
330 -> 800 [arrowhead = none ];
800 -> 335;

801 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
331 -> 801 [arrowhead = none ];
801 -> 333;

802 [label="EVAL with clause\nquot(s(X1380), s(X1381), X1382, X1383) :- quot(X1380, X1381, X1382, X1383).\nand substitution\nX1380 -> T543\nT532 -> s(T543)\nX1381 -> s(s(0))\nX1382 -> s(s(s(s(0))))\nT534 -> T545\nX1383 -> T545\nT544 -> T545", fontsize=14, style = filled, fillcolor = lightblue];
334 -> 802 [arrowhead = none ];
802 -> 336;

803 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
334 -> 803 [arrowhead = none ];
803 -> 337;

804 [label="BACKTRACK\nfor clause: quot(X, 0, s(Z), s(U)) :- quot(X, s(Z), s(Z), U)because of non-unification", fontsize=14, style = filled, fillcolor = white];
335 -> 804 [arrowhead = none ];
804 -> 365;

805 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
336 -> 805 [arrowhead = none ];
805 -> 338;

806 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
338 -> 806 [arrowhead = none ];
806 -> 339;

807 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
338 -> 807 [arrowhead = none ];
807 -> 340;

808 [label="EVAL with clause\nquot(0, s(X1400), s(X1401), 0).\nand substitution\nT543 -> 0\nX1400 -> s(0)\nX1401 -> s(s(s(0)))\nT545 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
339 -> 808 [arrowhead = none ];
808 -> 341;

809 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
339 -> 809 [arrowhead = none ];
809 -> 342;

810 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
340 -> 810 [arrowhead = none ];
810 -> 344;

811 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
340 -> 811 [arrowhead = none ];
811 -> 345;

812 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
341 -> 812 [arrowhead = none ];
812 -> 343;

813 [label="EVAL with clause\nquot(s(X1420), s(X1421), X1422, X1423) :- quot(X1420, X1421, X1422, X1423).\nand substitution\nX1420 -> T554\nT543 -> s(T554)\nX1421 -> s(0)\nX1422 -> s(s(s(s(0))))\nT545 -> T556\nX1423 -> T556\nT555 -> T556", fontsize=14, style = filled, fillcolor = lightblue];
344 -> 813 [arrowhead = none ];
813 -> 346;

814 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
344 -> 814 [arrowhead = none ];
814 -> 347;

815 [label="BACKTRACK\nfor clause: quot(X, 0, s(Z), s(U)) :- quot(X, s(Z), s(Z), U)because of non-unification", fontsize=14, style = filled, fillcolor = white];
345 -> 815 [arrowhead = none ];
815 -> 364;

816 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
346 -> 816 [arrowhead = none ];
816 -> 348;

817 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
348 -> 817 [arrowhead = none ];
817 -> 349;

818 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
348 -> 818 [arrowhead = none ];
818 -> 350;

819 [label="EVAL with clause\nquot(0, s(X1440), s(X1441), 0).\nand substitution\nT554 -> 0\nX1440 -> 0\nX1441 -> s(s(s(0)))\nT556 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
349 -> 819 [arrowhead = none ];
819 -> 351;

820 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
349 -> 820 [arrowhead = none ];
820 -> 352;

821 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
350 -> 821 [arrowhead = none ];
821 -> 354;

822 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
350 -> 822 [arrowhead = none ];
822 -> 355;

823 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
351 -> 823 [arrowhead = none ];
823 -> 353;

824 [label="EVAL with clause\nquot(s(X1460), s(X1461), X1462, X1463) :- quot(X1460, X1461, X1462, X1463).\nand substitution\nX1460 -> T565\nT554 -> s(T565)\nX1461 -> 0\nX1462 -> s(s(s(s(0))))\nT556 -> T567\nX1463 -> T567\nT566 -> T567", fontsize=14, style = filled, fillcolor = lightblue];
354 -> 824 [arrowhead = none ];
824 -> 356;

825 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
354 -> 825 [arrowhead = none ];
825 -> 357;

826 [label="BACKTRACK\nfor clause: quot(X, 0, s(Z), s(U)) :- quot(X, s(Z), s(Z), U)because of non-unification", fontsize=14, style = filled, fillcolor = white];
355 -> 826 [arrowhead = none ];
826 -> 363;

827 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
356 -> 827 [arrowhead = none ];
827 -> 358;

828 [label="BACKTRACK\nfor clause: quot(0, s(Y), s(Z), 0)because of non-unification", fontsize=14, style = filled, fillcolor = white];
358 -> 828 [arrowhead = none ];
828 -> 359;

829 [label="BACKTRACK\nfor clause: quot(s(X), s(Y), Z, U) :- quot(X, Y, Z, U)because of non-unification", fontsize=14, style = filled, fillcolor = white];
359 -> 829 [arrowhead = none ];
829 -> 360;

830 [label="EVAL with clause\nquot(X1491, 0, s(X1492), s(X1493)) :- quot(X1491, s(X1492), s(X1492), X1493).\nand substitution\nT565 -> T576\nX1491 -> T576\nX1492 -> s(s(s(0)))\nX1493 -> T578\nT567 -> s(T578)\nT577 -> T578", fontsize=14, style = filled, fillcolor = lightblue];
360 -> 830 [arrowhead = none ];
830 -> 361;

831 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
360 -> 831 [arrowhead = none ];
831 -> 362;

832 [label="INSTANCE with matching:\nT521 -> T576\nT523 -> T578", fontsize=14, style = filled, fillcolor = lightgrey];
361 -> 832 [arrowhead = none , style=dashed];
832 -> 316[style=dashed];

833 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
367 -> 833 [arrowhead = none ];
833 -> 369;

834 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
369 -> 834 [arrowhead = none ];
834 -> 370;

835 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
369 -> 835 [arrowhead = none ];
835 -> 371;

836 [label="EVAL with clause\nquot(0, s(X1537), s(X1538), 0).\nand substitution\nT587 -> 0\nX1537 -> s(s(0))\nX1538 -> s(s(0))\nT589 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
370 -> 836 [arrowhead = none ];
836 -> 372;

837 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
370 -> 837 [arrowhead = none ];
837 -> 373;

838 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
371 -> 838 [arrowhead = none ];
838 -> 375;

839 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
371 -> 839 [arrowhead = none ];
839 -> 376;

840 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
372 -> 840 [arrowhead = none ];
840 -> 374;

841 [label="EVAL with clause\nquot(s(X1557), s(X1558), X1559, X1560) :- quot(X1557, X1558, X1559, X1560).\nand substitution\nX1557 -> T598\nT587 -> s(T598)\nX1558 -> s(s(0))\nX1559 -> s(s(s(0)))\nT589 -> T600\nX1560 -> T600\nT599 -> T600", fontsize=14, style = filled, fillcolor = lightblue];
375 -> 841 [arrowhead = none ];
841 -> 377;

842 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
375 -> 842 [arrowhead = none ];
842 -> 378;

843 [label="BACKTRACK\nfor clause: quot(X, 0, s(Z), s(U)) :- quot(X, s(Z), s(Z), U)because of non-unification", fontsize=14, style = filled, fillcolor = white];
376 -> 843 [arrowhead = none ];
843 -> 406;

844 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
377 -> 844 [arrowhead = none ];
844 -> 379;

845 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
379 -> 845 [arrowhead = none ];
845 -> 380;

846 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
379 -> 846 [arrowhead = none ];
846 -> 381;

847 [label="EVAL with clause\nquot(0, s(X1577), s(X1578), 0).\nand substitution\nT598 -> 0\nX1577 -> s(0)\nX1578 -> s(s(0))\nT600 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
380 -> 847 [arrowhead = none ];
847 -> 382;

848 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
380 -> 848 [arrowhead = none ];
848 -> 383;

849 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
381 -> 849 [arrowhead = none ];
849 -> 385;

850 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
381 -> 850 [arrowhead = none ];
850 -> 386;

851 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
382 -> 851 [arrowhead = none ];
851 -> 384;

852 [label="EVAL with clause\nquot(s(X1597), s(X1598), X1599, X1600) :- quot(X1597, X1598, X1599, X1600).\nand substitution\nX1597 -> T609\nT598 -> s(T609)\nX1598 -> s(0)\nX1599 -> s(s(s(0)))\nT600 -> T611\nX1600 -> T611\nT610 -> T611", fontsize=14, style = filled, fillcolor = lightblue];
385 -> 852 [arrowhead = none ];
852 -> 387;

853 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
385 -> 853 [arrowhead = none ];
853 -> 388;

854 [label="BACKTRACK\nfor clause: quot(X, 0, s(Z), s(U)) :- quot(X, s(Z), s(Z), U)because of non-unification", fontsize=14, style = filled, fillcolor = white];
386 -> 854 [arrowhead = none ];
854 -> 405;

855 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
387 -> 855 [arrowhead = none ];
855 -> 389;

856 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
389 -> 856 [arrowhead = none ];
856 -> 390;

857 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
389 -> 857 [arrowhead = none ];
857 -> 391;

858 [label="EVAL with clause\nquot(0, s(X1617), s(X1618), 0).\nand substitution\nT609 -> 0\nX1617 -> 0\nX1618 -> s(s(0))\nT611 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
390 -> 858 [arrowhead = none ];
858 -> 392;

859 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
390 -> 859 [arrowhead = none ];
859 -> 393;

860 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
391 -> 860 [arrowhead = none ];
860 -> 395;

861 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
391 -> 861 [arrowhead = none ];
861 -> 396;

862 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
392 -> 862 [arrowhead = none ];
862 -> 394;

863 [label="EVAL with clause\nquot(s(X1637), s(X1638), X1639, X1640) :- quot(X1637, X1638, X1639, X1640).\nand substitution\nX1637 -> T620\nT609 -> s(T620)\nX1638 -> 0\nX1639 -> s(s(s(0)))\nT611 -> T622\nX1640 -> T622\nT621 -> T622", fontsize=14, style = filled, fillcolor = lightblue];
395 -> 863 [arrowhead = none ];
863 -> 397;

864 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
395 -> 864 [arrowhead = none ];
864 -> 398;

865 [label="BACKTRACK\nfor clause: quot(X, 0, s(Z), s(U)) :- quot(X, s(Z), s(Z), U)because of non-unification", fontsize=14, style = filled, fillcolor = white];
396 -> 865 [arrowhead = none ];
865 -> 404;

866 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
397 -> 866 [arrowhead = none ];
866 -> 399;

867 [label="BACKTRACK\nfor clause: quot(0, s(Y), s(Z), 0)because of non-unification", fontsize=14, style = filled, fillcolor = white];
399 -> 867 [arrowhead = none ];
867 -> 400;

868 [label="BACKTRACK\nfor clause: quot(s(X), s(Y), Z, U) :- quot(X, Y, Z, U)because of non-unification", fontsize=14, style = filled, fillcolor = white];
400 -> 868 [arrowhead = none ];
868 -> 401;

869 [label="EVAL with clause\nquot(X1668, 0, s(X1669), s(X1670)) :- quot(X1668, s(X1669), s(X1669), X1670).\nand substitution\nT620 -> T631\nX1668 -> T631\nX1669 -> s(s(0))\nX1670 -> T633\nT622 -> s(T633)\nT632 -> T633", fontsize=14, style = filled, fillcolor = lightblue];
401 -> 869 [arrowhead = none ];
869 -> 402;

870 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
401 -> 870 [arrowhead = none ];
870 -> 403;

871 [label="INSTANCE with matching:\nT587 -> T631\nT589 -> T633", fontsize=14, style = filled, fillcolor = lightgrey];
402 -> 871 [arrowhead = none , style=dashed];
871 -> 367[style=dashed];

872 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
407 -> 872 [arrowhead = none ];
872 -> 409;

873 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
409 -> 873 [arrowhead = none ];
873 -> 410;

874 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
409 -> 874 [arrowhead = none ];
874 -> 411;

875 [label="EVAL with clause\nquot(0, s(X1711), s(X1712), 0).\nand substitution\nT641 -> 0\nX1711 -> s(0)\nX1712 -> s(0)\nT643 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
410 -> 875 [arrowhead = none ];
875 -> 412;

876 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
410 -> 876 [arrowhead = none ];
876 -> 413;

877 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
411 -> 877 [arrowhead = none ];
877 -> 415;

878 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
411 -> 878 [arrowhead = none ];
878 -> 416;

879 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
412 -> 879 [arrowhead = none ];
879 -> 414;

880 [label="EVAL with clause\nquot(s(X1731), s(X1732), X1733, X1734) :- quot(X1731, X1732, X1733, X1734).\nand substitution\nX1731 -> T652\nT641 -> s(T652)\nX1732 -> s(0)\nX1733 -> s(s(0))\nT643 -> T654\nX1734 -> T654\nT653 -> T654", fontsize=14, style = filled, fillcolor = lightblue];
415 -> 880 [arrowhead = none ];
880 -> 417;

881 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
415 -> 881 [arrowhead = none ];
881 -> 418;

882 [label="BACKTRACK\nfor clause: quot(X, 0, s(Z), s(U)) :- quot(X, s(Z), s(Z), U)because of non-unification", fontsize=14, style = filled, fillcolor = white];
416 -> 882 [arrowhead = none ];
882 -> 435;

883 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
417 -> 883 [arrowhead = none ];
883 -> 419;

884 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
419 -> 884 [arrowhead = none ];
884 -> 420;

885 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
419 -> 885 [arrowhead = none ];
885 -> 421;

886 [label="EVAL with clause\nquot(0, s(X1751), s(X1752), 0).\nand substitution\nT652 -> 0\nX1751 -> 0\nX1752 -> s(0)\nT654 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
420 -> 886 [arrowhead = none ];
886 -> 422;

887 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
420 -> 887 [arrowhead = none ];
887 -> 423;

888 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
421 -> 888 [arrowhead = none ];
888 -> 425;

889 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
421 -> 889 [arrowhead = none ];
889 -> 426;

890 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
422 -> 890 [arrowhead = none ];
890 -> 424;

891 [label="EVAL with clause\nquot(s(X1771), s(X1772), X1773, X1774) :- quot(X1771, X1772, X1773, X1774).\nand substitution\nX1771 -> T663\nT652 -> s(T663)\nX1772 -> 0\nX1773 -> s(s(0))\nT654 -> T665\nX1774 -> T665\nT664 -> T665", fontsize=14, style = filled, fillcolor = lightblue];
425 -> 891 [arrowhead = none ];
891 -> 427;

892 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
425 -> 892 [arrowhead = none ];
892 -> 428;

893 [label="BACKTRACK\nfor clause: quot(X, 0, s(Z), s(U)) :- quot(X, s(Z), s(Z), U)because of non-unification", fontsize=14, style = filled, fillcolor = white];
426 -> 893 [arrowhead = none ];
893 -> 434;

894 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
427 -> 894 [arrowhead = none ];
894 -> 429;

895 [label="BACKTRACK\nfor clause: quot(0, s(Y), s(Z), 0)because of non-unification", fontsize=14, style = filled, fillcolor = white];
429 -> 895 [arrowhead = none ];
895 -> 430;

896 [label="BACKTRACK\nfor clause: quot(s(X), s(Y), Z, U) :- quot(X, Y, Z, U)because of non-unification", fontsize=14, style = filled, fillcolor = white];
430 -> 896 [arrowhead = none ];
896 -> 431;

897 [label="EVAL with clause\nquot(X1802, 0, s(X1803), s(X1804)) :- quot(X1802, s(X1803), s(X1803), X1804).\nand substitution\nT663 -> T674\nX1802 -> T674\nX1803 -> s(0)\nX1804 -> T676\nT665 -> s(T676)\nT675 -> T676", fontsize=14, style = filled, fillcolor = lightblue];
431 -> 897 [arrowhead = none ];
897 -> 432;

898 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
431 -> 898 [arrowhead = none ];
898 -> 433;

899 [label="INSTANCE with matching:\nT641 -> T674\nT643 -> T676", fontsize=14, style = filled, fillcolor = lightgrey];
432 -> 899 [arrowhead = none , style=dashed];
899 -> 407[style=dashed];

900 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
436 -> 900 [arrowhead = none ];
900 -> 438;

901 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
438 -> 901 [arrowhead = none ];
901 -> 439;

902 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
438 -> 902 [arrowhead = none ];
902 -> 440;

903 [label="EVAL with clause\nquot(0, s(X1842), s(X1843), 0).\nand substitution\nT683 -> 0\nX1842 -> 0\nX1843 -> 0\nT685 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
439 -> 903 [arrowhead = none ];
903 -> 441;

904 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
439 -> 904 [arrowhead = none ];
904 -> 442;

905 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
440 -> 905 [arrowhead = none ];
905 -> 444;

906 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
440 -> 906 [arrowhead = none ];
906 -> 445;

907 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
441 -> 907 [arrowhead = none ];
907 -> 443;

908 [label="EVAL with clause\nquot(s(X1862), s(X1863), X1864, X1865) :- quot(X1862, X1863, X1864, X1865).\nand substitution\nX1862 -> T694\nT683 -> s(T694)\nX1863 -> 0\nX1864 -> s(0)\nT685 -> T696\nX1865 -> T696\nT695 -> T696", fontsize=14, style = filled, fillcolor = lightblue];
444 -> 908 [arrowhead = none ];
908 -> 446;

909 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
444 -> 909 [arrowhead = none ];
909 -> 447;

910 [label="BACKTRACK\nfor clause: quot(X, 0, s(Z), s(U)) :- quot(X, s(Z), s(Z), U)because of non-unification", fontsize=14, style = filled, fillcolor = white];
445 -> 910 [arrowhead = none ];
910 -> 453;

911 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
446 -> 911 [arrowhead = none ];
911 -> 448;

912 [label="BACKTRACK\nfor clause: quot(0, s(Y), s(Z), 0)because of non-unification", fontsize=14, style = filled, fillcolor = white];
448 -> 912 [arrowhead = none ];
912 -> 449;

913 [label="BACKTRACK\nfor clause: quot(s(X), s(Y), Z, U) :- quot(X, Y, Z, U)because of non-unification", fontsize=14, style = filled, fillcolor = white];
449 -> 913 [arrowhead = none ];
913 -> 450;

914 [label="EVAL with clause\nquot(X1893, 0, s(X1894), s(X1895)) :- quot(X1893, s(X1894), s(X1894), X1895).\nand substitution\nT694 -> T705\nX1893 -> T705\nX1894 -> 0\nX1895 -> T707\nT696 -> s(T707)\nT706 -> T707", fontsize=14, style = filled, fillcolor = lightblue];
450 -> 914 [arrowhead = none ];
914 -> 451;

915 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
450 -> 915 [arrowhead = none ];
915 -> 452;

916 [label="INSTANCE with matching:\nT683 -> T705\nT685 -> T707", fontsize=14, style = filled, fillcolor = lightgrey];
451 -> 916 [arrowhead = none , style=dashed];
916 -> 436[style=dashed];

}

(2) Obligation:

Triples:

quot84(s(T226), s(T227), T228, T230) :- quot84(T226, T227, T228, T230).
quot84(T241, 0, T242, s(T244)) :- quot3(T241, s(T242), T244).
quot3(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192) :- quot84(T189, T190, s(s(s(s(s(s(s(T190))))))), T192).
quot3(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253)) :- quot97(T251, T253).
quot3(s(s(s(s(s(s(T353)))))), s(s(s(s(s(s(0)))))), s(T355)) :- quot181(T353, T355).
quot3(s(s(s(s(s(T443))))), s(s(s(s(s(0))))), s(T445)) :- quot254(T443, T445).
quot3(s(s(s(s(T521)))), s(s(s(s(0)))), s(T523)) :- quot316(T521, T523).
quot3(s(s(s(T587))), s(s(s(0))), s(T589)) :- quot367(T587, T589).
quot3(s(s(T641)), s(s(0)), s(T643)) :- quot407(T641, T643).
quot3(s(T683), s(0), s(T685)) :- quot436(T683, T685).
quot97(s(s(s(s(s(s(s(T339))))))), s(T341)) :- quot97(T339, T341).
quot181(s(s(s(s(s(s(T430)))))), s(T432)) :- quot181(T430, T432).
quot254(s(s(s(s(s(T509))))), s(T511)) :- quot254(T509, T511).
quot316(s(s(s(s(T576)))), s(T578)) :- quot316(T576, T578).
quot367(s(s(s(T631))), s(T633)) :- quot367(T631, T633).
quot407(s(s(T674)), s(T676)) :- quot407(T674, T676).
quot436(s(T705), s(T707)) :- quot436(T705, T707).
div1(T7, T8, T10) :- quot3(T7, T8, T10).

Clauses:

quotc84(0, s(T208), T209, 0).
quotc84(s(T226), s(T227), T228, T230) :- quotc84(T226, T227, T228, T230).
quotc84(T241, 0, T242, s(T244)) :- quotc3(T241, s(T242), T244).
quotc3(0, s(T15), 0).
quotc3(s(0), s(s(T38)), 0).
quotc3(s(s(0)), s(s(s(T61))), 0).
quotc3(s(s(s(0))), s(s(s(s(T84)))), 0).
quotc3(s(s(s(s(0)))), s(s(s(s(s(T107))))), 0).
quotc3(s(s(s(s(s(0))))), s(s(s(s(s(s(T130)))))), 0).
quotc3(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T153))))))), 0).
quotc3(s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(s(T176)))))))), 0).
quotc3(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192) :- quotc84(T189, T190, s(s(s(s(s(s(s(T190))))))), T192).
quotc3(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253)) :- quotc97(T251, T253).
quotc3(s(s(s(s(s(s(T353)))))), s(s(s(s(s(s(0)))))), s(T355)) :- quotc181(T353, T355).
quotc3(s(s(s(s(s(T443))))), s(s(s(s(s(0))))), s(T445)) :- quotc254(T443, T445).
quotc3(s(s(s(s(T521)))), s(s(s(s(0)))), s(T523)) :- quotc316(T521, T523).
quotc3(s(s(s(T587))), s(s(s(0))), s(T589)) :- quotc367(T587, T589).
quotc3(s(s(T641)), s(s(0)), s(T643)) :- quotc407(T641, T643).
quotc3(s(T683), s(0), s(T685)) :- quotc436(T683, T685).
quotc97(0, 0).
quotc97(s(0), 0).
quotc97(s(s(0)), 0).
quotc97(s(s(s(0))), 0).
quotc97(s(s(s(s(0)))), 0).
quotc97(s(s(s(s(s(0))))), 0).
quotc97(s(s(s(s(s(s(0)))))), 0).
quotc97(s(s(s(s(s(s(s(T339))))))), s(T341)) :- quotc97(T339, T341).
quotc181(0, 0).
quotc181(s(0), 0).
quotc181(s(s(0)), 0).
quotc181(s(s(s(0))), 0).
quotc181(s(s(s(s(0)))), 0).
quotc181(s(s(s(s(s(0))))), 0).
quotc181(s(s(s(s(s(s(T430)))))), s(T432)) :- quotc181(T430, T432).
quotc254(0, 0).
quotc254(s(0), 0).
quotc254(s(s(0)), 0).
quotc254(s(s(s(0))), 0).
quotc254(s(s(s(s(0)))), 0).
quotc254(s(s(s(s(s(T509))))), s(T511)) :- quotc254(T509, T511).
quotc316(0, 0).
quotc316(s(0), 0).
quotc316(s(s(0)), 0).
quotc316(s(s(s(0))), 0).
quotc316(s(s(s(s(T576)))), s(T578)) :- quotc316(T576, T578).
quotc367(0, 0).
quotc367(s(0), 0).
quotc367(s(s(0)), 0).
quotc367(s(s(s(T631))), s(T633)) :- quotc367(T631, T633).
quotc407(0, 0).
quotc407(s(0), 0).
quotc407(s(s(T674)), s(T676)) :- quotc407(T674, T676).
quotc436(0, 0).
quotc436(s(T705), s(T707)) :- quotc436(T705, T707).

Afs:

div1(x1, x2, x3) = div1(x1, x2)

(3) TriplesToPiDPProof (SOUND transformation)

We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
div1_in: (b,b,f)
quot3_in: (b,b,f)
quot84_in: (b,b,b,f)
quot97_in: (b,f)
quot181_in: (b,f)
quot254_in: (b,f)
quot316_in: (b,f)
quot367_in: (b,f)
quot407_in: (b,f)
quot436_in: (b,f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

DIV1_IN_GGA(T7, T8, T10) → U18_GGA(T7, T8, T10, quot3_in_gga(T7, T8, T10))
DIV1_IN_GGA(T7, T8, T10) → QUOT3_IN_GGA(T7, T8, T10)
QUOT3_IN_GGA(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192) → U3_GGA(T189, T190, T192, quot84_in_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192))
QUOT3_IN_GGA(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192) → QUOT84_IN_GGGA(T189, T190, s(s(s(s(s(s(s(T190))))))), T192)
QUOT84_IN_GGGA(s(T226), s(T227), T228, T230) → U1_GGGA(T226, T227, T228, T230, quot84_in_ggga(T226, T227, T228, T230))
QUOT84_IN_GGGA(s(T226), s(T227), T228, T230) → QUOT84_IN_GGGA(T226, T227, T228, T230)
QUOT84_IN_GGGA(T241, 0, T242, s(T244)) → U2_GGGA(T241, T242, T244, quot3_in_gga(T241, s(T242), T244))
QUOT84_IN_GGGA(T241, 0, T242, s(T244)) → QUOT3_IN_GGA(T241, s(T242), T244)
QUOT3_IN_GGA(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253)) → U4_GGA(T251, T253, quot97_in_ga(T251, T253))
QUOT3_IN_GGA(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253)) → QUOT97_IN_GA(T251, T253)
QUOT97_IN_GA(s(s(s(s(s(s(s(T339))))))), s(T341)) → U11_GA(T339, T341, quot97_in_ga(T339, T341))
QUOT97_IN_GA(s(s(s(s(s(s(s(T339))))))), s(T341)) → QUOT97_IN_GA(T339, T341)
QUOT3_IN_GGA(s(s(s(s(s(s(T353)))))), s(s(s(s(s(s(0)))))), s(T355)) → U5_GGA(T353, T355, quot181_in_ga(T353, T355))
QUOT3_IN_GGA(s(s(s(s(s(s(T353)))))), s(s(s(s(s(s(0)))))), s(T355)) → QUOT181_IN_GA(T353, T355)
QUOT181_IN_GA(s(s(s(s(s(s(T430)))))), s(T432)) → U12_GA(T430, T432, quot181_in_ga(T430, T432))
QUOT181_IN_GA(s(s(s(s(s(s(T430)))))), s(T432)) → QUOT181_IN_GA(T430, T432)
QUOT3_IN_GGA(s(s(s(s(s(T443))))), s(s(s(s(s(0))))), s(T445)) → U6_GGA(T443, T445, quot254_in_ga(T443, T445))
QUOT3_IN_GGA(s(s(s(s(s(T443))))), s(s(s(s(s(0))))), s(T445)) → QUOT254_IN_GA(T443, T445)
QUOT254_IN_GA(s(s(s(s(s(T509))))), s(T511)) → U13_GA(T509, T511, quot254_in_ga(T509, T511))
QUOT254_IN_GA(s(s(s(s(s(T509))))), s(T511)) → QUOT254_IN_GA(T509, T511)
QUOT3_IN_GGA(s(s(s(s(T521)))), s(s(s(s(0)))), s(T523)) → U7_GGA(T521, T523, quot316_in_ga(T521, T523))
QUOT3_IN_GGA(s(s(s(s(T521)))), s(s(s(s(0)))), s(T523)) → QUOT316_IN_GA(T521, T523)
QUOT316_IN_GA(s(s(s(s(T576)))), s(T578)) → U14_GA(T576, T578, quot316_in_ga(T576, T578))
QUOT316_IN_GA(s(s(s(s(T576)))), s(T578)) → QUOT316_IN_GA(T576, T578)
QUOT3_IN_GGA(s(s(s(T587))), s(s(s(0))), s(T589)) → U8_GGA(T587, T589, quot367_in_ga(T587, T589))
QUOT3_IN_GGA(s(s(s(T587))), s(s(s(0))), s(T589)) → QUOT367_IN_GA(T587, T589)
QUOT367_IN_GA(s(s(s(T631))), s(T633)) → U15_GA(T631, T633, quot367_in_ga(T631, T633))
QUOT367_IN_GA(s(s(s(T631))), s(T633)) → QUOT367_IN_GA(T631, T633)
QUOT3_IN_GGA(s(s(T641)), s(s(0)), s(T643)) → U9_GGA(T641, T643, quot407_in_ga(T641, T643))
QUOT3_IN_GGA(s(s(T641)), s(s(0)), s(T643)) → QUOT407_IN_GA(T641, T643)
QUOT407_IN_GA(s(s(T674)), s(T676)) → U16_GA(T674, T676, quot407_in_ga(T674, T676))
QUOT407_IN_GA(s(s(T674)), s(T676)) → QUOT407_IN_GA(T674, T676)
QUOT3_IN_GGA(s(T683), s(0), s(T685)) → U10_GGA(T683, T685, quot436_in_ga(T683, T685))
QUOT3_IN_GGA(s(T683), s(0), s(T685)) → QUOT436_IN_GA(T683, T685)
QUOT436_IN_GA(s(T705), s(T707)) → U17_GA(T705, T707, quot436_in_ga(T705, T707))
QUOT436_IN_GA(s(T705), s(T707)) → QUOT436_IN_GA(T705, T707)

R is empty.
The argument filtering Pi contains the following mapping:
quot3_in_gga(x1, x2, x3) = quot3_in_gga(x1, x2)
s(x1) = s(x1)
quot84_in_ggga(x1, x2, x3, x4) = quot84_in_ggga(x1, x2, x3)
0 = 0
quot97_in_ga(x1, x2) = quot97_in_ga(x1)
quot181_in_ga(x1, x2) = quot181_in_ga(x1)
quot254_in_ga(x1, x2) = quot254_in_ga(x1)
quot316_in_ga(x1, x2) = quot316_in_ga(x1)
quot367_in_ga(x1, x2) = quot367_in_ga(x1)
quot407_in_ga(x1, x2) = quot407_in_ga(x1)
quot436_in_ga(x1, x2) = quot436_in_ga(x1)
DIV1_IN_GGA(x1, x2, x3) = DIV1_IN_GGA(x1, x2)
U18_GGA(x1, x2, x3, x4) = U18_GGA(x1, x2, x4)
QUOT3_IN_GGA(x1, x2, x3) = QUOT3_IN_GGA(x1, x2)
U3_GGA(x1, x2, x3, x4) = U3_GGA(x1, x2, x4)
QUOT84_IN_GGGA(x1, x2, x3, x4) = QUOT84_IN_GGGA(x1, x2, x3)
U1_GGGA(x1, x2, x3, x4, x5) = U1_GGGA(x1, x2, x3, x5)
U2_GGGA(x1, x2, x3, x4) = U2_GGGA(x1, x2, x4)
U4_GGA(x1, x2, x3) = U4_GGA(x1, x3)
QUOT97_IN_GA(x1, x2) = QUOT97_IN_GA(x1)
U11_GA(x1, x2, x3) = U11_GA(x1, x3)
U5_GGA(x1, x2, x3) = U5_GGA(x1, x3)
QUOT181_IN_GA(x1, x2) = QUOT181_IN_GA(x1)
U12_GA(x1, x2, x3) = U12_GA(x1, x3)
U6_GGA(x1, x2, x3) = U6_GGA(x1, x3)
QUOT254_IN_GA(x1, x2) = QUOT254_IN_GA(x1)
U13_GA(x1, x2, x3) = U13_GA(x1, x3)
U7_GGA(x1, x2, x3) = U7_GGA(x1, x3)
QUOT316_IN_GA(x1, x2) = QUOT316_IN_GA(x1)
U14_GA(x1, x2, x3) = U14_GA(x1, x3)
U8_GGA(x1, x2, x3) = U8_GGA(x1, x3)
QUOT367_IN_GA(x1, x2) = QUOT367_IN_GA(x1)
U15_GA(x1, x2, x3) = U15_GA(x1, x3)
U9_GGA(x1, x2, x3) = U9_GGA(x1, x3)
QUOT407_IN_GA(x1, x2) = QUOT407_IN_GA(x1)
U16_GA(x1, x2, x3) = U16_GA(x1, x3)
U10_GGA(x1, x2, x3) = U10_GGA(x1, x3)
QUOT436_IN_GA(x1, x2) = QUOT436_IN_GA(x1)
U17_GA(x1, x2, x3) = U17_GA(x1, x3)

We have to consider all (P,R,Pi)-chains

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(4) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

DIV1_IN_GGA(T7, T8, T10) → U18_GGA(T7, T8, T10, quot3_in_gga(T7, T8, T10))
DIV1_IN_GGA(T7, T8, T10) → QUOT3_IN_GGA(T7, T8, T10)
QUOT3_IN_GGA(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192) → U3_GGA(T189, T190, T192, quot84_in_ggga(T189, T190, s(s(s(s(s(s(s(T190))))))), T192))
QUOT3_IN_GGA(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192) → QUOT84_IN_GGGA(T189, T190, s(s(s(s(s(s(s(T190))))))), T192)
QUOT84_IN_GGGA(s(T226), s(T227), T228, T230) → U1_GGGA(T226, T227, T228, T230, quot84_in_ggga(T226, T227, T228, T230))
QUOT84_IN_GGGA(s(T226), s(T227), T228, T230) → QUOT84_IN_GGGA(T226, T227, T228, T230)
QUOT84_IN_GGGA(T241, 0, T242, s(T244)) → U2_GGGA(T241, T242, T244, quot3_in_gga(T241, s(T242), T244))
QUOT84_IN_GGGA(T241, 0, T242, s(T244)) → QUOT3_IN_GGA(T241, s(T242), T244)
QUOT3_IN_GGA(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253)) → U4_GGA(T251, T253, quot97_in_ga(T251, T253))
QUOT3_IN_GGA(s(s(s(s(s(s(s(T251))))))), s(s(s(s(s(s(s(0))))))), s(T253)) → QUOT97_IN_GA(T251, T253)
QUOT97_IN_GA(s(s(s(s(s(s(s(T339))))))), s(T341)) → U11_GA(T339, T341, quot97_in_ga(T339, T341))
QUOT97_IN_GA(s(s(s(s(s(s(s(T339))))))), s(T341)) → QUOT97_IN_GA(T339, T341)
QUOT3_IN_GGA(s(s(s(s(s(s(T353)))))), s(s(s(s(s(s(0)))))), s(T355)) → U5_GGA(T353, T355, quot181_in_ga(T353, T355))
QUOT3_IN_GGA(s(s(s(s(s(s(T353)))))), s(s(s(s(s(s(0)))))), s(T355)) → QUOT181_IN_GA(T353, T355)
QUOT181_IN_GA(s(s(s(s(s(s(T430)))))), s(T432)) → U12_GA(T430, T432, quot181_in_ga(T430, T432))
QUOT181_IN_GA(s(s(s(s(s(s(T430)))))), s(T432)) → QUOT181_IN_GA(T430, T432)
QUOT3_IN_GGA(s(s(s(s(s(T443))))), s(s(s(s(s(0))))), s(T445)) → U6_GGA(T443, T445, quot254_in_ga(T443, T445))
QUOT3_IN_GGA(s(s(s(s(s(T443))))), s(s(s(s(s(0))))), s(T445)) → QUOT254_IN_GA(T443, T445)
QUOT254_IN_GA(s(s(s(s(s(T509))))), s(T511)) → U13_GA(T509, T511, quot254_in_ga(T509, T511))
QUOT254_IN_GA(s(s(s(s(s(T509))))), s(T511)) → QUOT254_IN_GA(T509, T511)
QUOT3_IN_GGA(s(s(s(s(T521)))), s(s(s(s(0)))), s(T523)) → U7_GGA(T521, T523, quot316_in_ga(T521, T523))
QUOT3_IN_GGA(s(s(s(s(T521)))), s(s(s(s(0)))), s(T523)) → QUOT316_IN_GA(T521, T523)
QUOT316_IN_GA(s(s(s(s(T576)))), s(T578)) → U14_GA(T576, T578, quot316_in_ga(T576, T578))
QUOT316_IN_GA(s(s(s(s(T576)))), s(T578)) → QUOT316_IN_GA(T576, T578)
QUOT3_IN_GGA(s(s(s(T587))), s(s(s(0))), s(T589)) → U8_GGA(T587, T589, quot367_in_ga(T587, T589))
QUOT3_IN_GGA(s(s(s(T587))), s(s(s(0))), s(T589)) → QUOT367_IN_GA(T587, T589)
QUOT367_IN_GA(s(s(s(T631))), s(T633)) → U15_GA(T631, T633, quot367_in_ga(T631, T633))
QUOT367_IN_GA(s(s(s(T631))), s(T633)) → QUOT367_IN_GA(T631, T633)
QUOT3_IN_GGA(s(s(T641)), s(s(0)), s(T643)) → U9_GGA(T641, T643, quot407_in_ga(T641, T643))
QUOT3_IN_GGA(s(s(T641)), s(s(0)), s(T643)) → QUOT407_IN_GA(T641, T643)
QUOT407_IN_GA(s(s(T674)), s(T676)) → U16_GA(T674, T676, quot407_in_ga(T674, T676))
QUOT407_IN_GA(s(s(T674)), s(T676)) → QUOT407_IN_GA(T674, T676)
QUOT3_IN_GGA(s(T683), s(0), s(T685)) → U10_GGA(T683, T685, quot436_in_ga(T683, T685))
QUOT3_IN_GGA(s(T683), s(0), s(T685)) → QUOT436_IN_GA(T683, T685)
QUOT436_IN_GA(s(T705), s(T707)) → U17_GA(T705, T707, quot436_in_ga(T705, T707))
QUOT436_IN_GA(s(T705), s(T707)) → QUOT436_IN_GA(T705, T707)

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 8 SCCs with 26 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

QUOT436_IN_GA(s(T705), s(T707)) → QUOT436_IN_GA(T705, T707)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1) = s(x1)
QUOT436_IN_GA(x1, x2) = QUOT436_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(8) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(9) Obligation:

Q DP problem:
The TRS P consists of the following rules:

QUOT436_IN_GA(s(T705)) → QUOT436_IN_GA(T705)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(10) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

QUOT436_IN_GA(s(T705)) → QUOT436_IN_GA(T705)
The graph contains the following edges 1 > 1

(11) YES

(12) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

QUOT407_IN_GA(s(s(T674)), s(T676)) → QUOT407_IN_GA(T674, T676)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1) = s(x1)
QUOT407_IN_GA(x1, x2) = QUOT407_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(13) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(14) Obligation:

Q DP problem:
The TRS P consists of the following rules:

QUOT407_IN_GA(s(s(T674))) → QUOT407_IN_GA(T674)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(15) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

QUOT407_IN_GA(s(s(T674))) → QUOT407_IN_GA(T674)
The graph contains the following edges 1 > 1

(16) YES

(17) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

QUOT367_IN_GA(s(s(s(T631))), s(T633)) → QUOT367_IN_GA(T631, T633)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1) = s(x1)
QUOT367_IN_GA(x1, x2) = QUOT367_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(18) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(19) Obligation:

Q DP problem:
The TRS P consists of the following rules:

QUOT367_IN_GA(s(s(s(T631)))) → QUOT367_IN_GA(T631)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(20) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

QUOT367_IN_GA(s(s(s(T631)))) → QUOT367_IN_GA(T631)
The graph contains the following edges 1 > 1

(21) YES

(22) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

QUOT316_IN_GA(s(s(s(s(T576)))), s(T578)) → QUOT316_IN_GA(T576, T578)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1) = s(x1)
QUOT316_IN_GA(x1, x2) = QUOT316_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(23) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(24) Obligation:

Q DP problem:
The TRS P consists of the following rules:

QUOT316_IN_GA(s(s(s(s(T576))))) → QUOT316_IN_GA(T576)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(25) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

QUOT316_IN_GA(s(s(s(s(T576))))) → QUOT316_IN_GA(T576)
The graph contains the following edges 1 > 1

(26) YES

(27) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

QUOT254_IN_GA(s(s(s(s(s(T509))))), s(T511)) → QUOT254_IN_GA(T509, T511)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1) = s(x1)
QUOT254_IN_GA(x1, x2) = QUOT254_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(28) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(29) Obligation:

Q DP problem:
The TRS P consists of the following rules:

QUOT254_IN_GA(s(s(s(s(s(T509)))))) → QUOT254_IN_GA(T509)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(30) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

QUOT254_IN_GA(s(s(s(s(s(T509)))))) → QUOT254_IN_GA(T509)
The graph contains the following edges 1 > 1

(31) YES

(32) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

QUOT181_IN_GA(s(s(s(s(s(s(T430)))))), s(T432)) → QUOT181_IN_GA(T430, T432)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1) = s(x1)
QUOT181_IN_GA(x1, x2) = QUOT181_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(33) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(34) Obligation:

Q DP problem:
The TRS P consists of the following rules:

QUOT181_IN_GA(s(s(s(s(s(s(T430))))))) → QUOT181_IN_GA(T430)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(35) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

QUOT181_IN_GA(s(s(s(s(s(s(T430))))))) → QUOT181_IN_GA(T430)
The graph contains the following edges 1 > 1

(36) YES

(37) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

QUOT97_IN_GA(s(s(s(s(s(s(s(T339))))))), s(T341)) → QUOT97_IN_GA(T339, T341)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1) = s(x1)
QUOT97_IN_GA(x1, x2) = QUOT97_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(38) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(39) Obligation:

Q DP problem:
The TRS P consists of the following rules:

QUOT97_IN_GA(s(s(s(s(s(s(s(T339)))))))) → QUOT97_IN_GA(T339)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(40) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

QUOT97_IN_GA(s(s(s(s(s(s(s(T339)))))))) → QUOT97_IN_GA(T339)
The graph contains the following edges 1 > 1

(41) YES

(42) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

QUOT3_IN_GGA(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190)))))))), T192) → QUOT84_IN_GGGA(T189, T190, s(s(s(s(s(s(s(T190))))))), T192)
QUOT84_IN_GGGA(s(T226), s(T227), T228, T230) → QUOT84_IN_GGGA(T226, T227, T228, T230)
QUOT84_IN_GGGA(T241, 0, T242, s(T244)) → QUOT3_IN_GGA(T241, s(T242), T244)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1) = s(x1)
0 = 0
QUOT3_IN_GGA(x1, x2, x3) = QUOT3_IN_GGA(x1, x2)
QUOT84_IN_GGGA(x1, x2, x3, x4) = QUOT84_IN_GGGA(x1, x2, x3)

We have to consider all (P,R,Pi)-chains

(43) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(44) Obligation:

Q DP problem:
The TRS P consists of the following rules:

QUOT3_IN_GGA(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190))))))))) → QUOT84_IN_GGGA(T189, T190, s(s(s(s(s(s(s(T190))))))))
QUOT84_IN_GGGA(s(T226), s(T227), T228) → QUOT84_IN_GGGA(T226, T227, T228)
QUOT84_IN_GGGA(T241, 0, T242) → QUOT3_IN_GGA(T241, s(T242))

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(45) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

QUOT84_IN_GGGA(T241, 0, T242) → QUOT3_IN_GGA(T241, s(T242))
The graph contains the following edges 1 >= 1
QUOT84_IN_GGGA(s(T226), s(T227), T228) → QUOT84_IN_GGGA(T226, T227, T228)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3
QUOT3_IN_GGA(s(s(s(s(s(s(s(s(T189)))))))), s(s(s(s(s(s(s(s(T190))))))))) → QUOT84_IN_GGGA(T189, T190, s(s(s(s(s(s(s(T190))))))))
The graph contains the following edges 1 > 1, 2 > 2, 2 > 3

(0) Obligation:

(1) PrologToDTProblemTransformerProof (SOUND transformation)

(2) Obligation:

(3) TriplesToPiDPProof (SOUND transformation)

(4) Obligation:

(5) DependencyGraphProof (EQUIVALENT transformation)

(6) Complex Obligation (AND)

(7) Obligation:

(8) PiDPToQDPProof (SOUND transformation)

(9) Obligation:

(10) QDPSizeChangeProof (EQUIVALENT transformation)

(11) YES

(12) Obligation:

(13) PiDPToQDPProof (SOUND transformation)

(14) Obligation:

(15) QDPSizeChangeProof (EQUIVALENT transformation)

(16) YES

(17) Obligation:

(18) PiDPToQDPProof (SOUND transformation)

(19) Obligation:

(20) QDPSizeChangeProof (EQUIVALENT transformation)

(21) YES

(22) Obligation:

(23) PiDPToQDPProof (SOUND transformation)

(24) Obligation:

(25) QDPSizeChangeProof (EQUIVALENT transformation)

(26) YES

(27) Obligation:

(28) PiDPToQDPProof (SOUND transformation)

(29) Obligation:

(30) QDPSizeChangeProof (EQUIVALENT transformation)

(31) YES

(32) Obligation:

(33) PiDPToQDPProof (SOUND transformation)

(34) Obligation:

(35) QDPSizeChangeProof (EQUIVALENT transformation)

(36) YES

(37) Obligation:

(38) PiDPToQDPProof (SOUND transformation)

(39) Obligation:

(40) QDPSizeChangeProof (EQUIVALENT transformation)

(41) YES

(42) Obligation:

(43) PiDPToQDPProof (SOUND transformation)

(44) Obligation:

(45) QDPSizeChangeProof (EQUIVALENT transformation)

(46) YES