Left Termination proof of /tmp/tmpN2Dwqd/divremain2.pl

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

0 Prolog

↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 404 ms)

↳2 PiTRS

↳3 DependencyPairsProof (⇔, 39 ms)

↳4 PiDP

↳5 DependencyGraphProof (⇔, 0 ms)

↳6 AND

    ↳7 PiDP

        ↳8 UsableRulesProof (⇔, 0 ms)

        ↳9 PiDP

        ↳10 PiDPToQDPProof (⇒, 0 ms)

        ↳11 QDP

        ↳12 QDPSizeChangeProof (⇔, 0 ms)

        ↳13 YES

    ↳14 PiDP

        ↳15 UsableRulesProof (⇔, 0 ms)

        ↳16 PiDP

        ↳17 PiDPToQDPProof (⇒, 0 ms)

        ↳18 QDP

        ↳19 QDPOrderProof (⇔, 61 ms)

        ↳20 QDP

        ↳21 DependencyGraphProof (⇔, 0 ms)

        ↳22 TRUE

(0) Obligation:

Clauses:

div(X1, 0, X2, X3) :- failure(a).
div(0, Y, 0, 0) :- no(zero(Y)).
div(X, Y, s(Z), R) :- ','(no(zero(X)), ','(no(zero(Y)), ','(minus(X, Y, U), ','(!, div(U, Y, Z, R))))).
div(X, Y, X4, X) :- ','(no(zero(X)), no(zero(Y))).
minus(X, 0, X).
minus(s(X), s(Y), Z) :- minus(X, Y, Z).
failure(b).
zero(0).
no(X) :- ','(X, ','(!, failure(a))).
no(X5).

Query: div(g,g,a,a)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
3 [label="A: div(T1, T2, T3, T4)\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
5 [label="5: div(T1, T2, T3, T4), SCOPE: 1, CLAUSE: 0 | div(T1, T2, T3, T4), SCOPE: 1, CLAUSE: 1 | div(T1, T2, T3, T4), SCOPE: 1, CLAUSE: 2 | div(T1, T2, T3, T4), SCOPE: 1, CLAUSE: 3\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: failure(a) | div(T8, 0, T3, T4), SCOPE: 1, CLAUSE: 1 | div(T8, 0, T3, T4), SCOPE: 1, CLAUSE: 2 | div(T8, 0, T3, T4), SCOPE: 1, CLAUSE: 3\n\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: div(T1, T2, T3, T4), SCOPE: 1, CLAUSE: 1 | div(T1, T2, T3, T4), SCOPE: 1, CLAUSE: 2 | div(T1, T2, T3, T4), SCOPE: 1, CLAUSE: 3\n\nT1 is ground\nT2 is ground\nX9 is free\nX10 is free\nX11 is free\ndiv(T1, T2, T3, T4) !=? div(X9, 0, X10, X11)", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: failure(a), SCOPE: 2, CLAUSE: 6 | ?_2 | div(T8, 0, T3, T4), SCOPE: 1, CLAUSE: 1 | div(T8, 0, T3, T4), SCOPE: 1, CLAUSE: 2 | div(T8, 0, T3, T4), SCOPE: 1, CLAUSE: 3\n\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: ?_2 | div(T8, 0, T3, T4), SCOPE: 1, CLAUSE: 1 | div(T8, 0, T3, T4), SCOPE: 1, CLAUSE: 2 | div(T8, 0, T3, T4), SCOPE: 1, CLAUSE: 3\n\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: div(T8, 0, T3, T4), SCOPE: 1, CLAUSE: 1 | div(T8, 0, T3, T4), SCOPE: 1, CLAUSE: 2 | div(T8, 0, T3, T4), SCOPE: 1, CLAUSE: 3\n\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: no(zero(0)) | div(0, 0, T3, T4), SCOPE: 1, CLAUSE: 2 | div(0, 0, T3, T4), SCOPE: 1, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: div(T8, 0, T3, T4), SCOPE: 1, CLAUSE: 2 | div(T8, 0, T3, T4), SCOPE: 1, CLAUSE: 3\n\nT8 is ground\nX14 is free\ndiv(T8, 0, T3, T4) !=? div(0, X14, 0, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: no(zero(0)), SCOPE: 3, CLAUSE: 8 | no(zero(0)), SCOPE: 3, CLAUSE: 9 | ?_3 | div(0, 0, T3, T4), SCOPE: 1, CLAUSE: 2 | div(0, 0, T3, T4), SCOPE: 1, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: ','(call(zero(0)), ','(!_3, failure(a))) | no(zero(0)), SCOPE: 3, CLAUSE: 9 | ?_3 | div(0, 0, T3, T4), SCOPE: 1, CLAUSE: 2 | div(0, 0, T3, T4), SCOPE: 1, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: ','(zero(0), ','(!_3, failure(a))) | ?_4 | no(zero(0)), SCOPE: 3, CLAUSE: 9 | ?_3 | div(0, 0, T3, T4), SCOPE: 1, CLAUSE: 2 | div(0, 0, T3, T4), SCOPE: 1, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: ','(zero(0), ','(!_3, failure(a))), SCOPE: 5, CLAUSE: 7 | ?_5 | ?_4 | no(zero(0)), SCOPE: 3, CLAUSE: 9 | ?_3 | div(0, 0, T3, T4), SCOPE: 1, CLAUSE: 2 | div(0, 0, T3, T4), SCOPE: 1, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: ','(!_3, failure(a)) | ?_5 | ?_4 | no(zero(0)), SCOPE: 3, CLAUSE: 9 | ?_3 | div(0, 0, T3, T4), SCOPE: 1, CLAUSE: 2 | div(0, 0, T3, T4), SCOPE: 1, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: failure(a) | div(0, 0, T3, T4), SCOPE: 1, CLAUSE: 2 | div(0, 0, T3, T4), SCOPE: 1, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: failure(a), SCOPE: 6, CLAUSE: 6 | ?_6 | div(0, 0, T3, T4), SCOPE: 1, CLAUSE: 2 | div(0, 0, T3, T4), SCOPE: 1, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: ?_6 | div(0, 0, T3, T4), SCOPE: 1, CLAUSE: 2 | div(0, 0, T3, T4), SCOPE: 1, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: div(0, 0, T3, T4), SCOPE: 1, CLAUSE: 2 | div(0, 0, T3, T4), SCOPE: 1, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: div(0, 0, T3, T4), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: div(0, 0, T3, T4), SCOPE: 1, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: ','(no(zero(0)), ','(no(zero(0)), ','(minus(0, 0, X40), ','(!_1, div(X40, 0, T21, T22)))))\n\nX40 is free", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: ','(no(zero(0)), ','(no(zero(0)), ','(minus(0, 0, X40), ','(!_1, div(X40, 0, T21, T22))))), SCOPE: 7, CLAUSE: 8 | ','(no(zero(0)), ','(no(zero(0)), ','(minus(0, 0, X40), ','(!_1, div(X40, 0, T21, T22))))), SCOPE: 7, CLAUSE: 9\n\nX40 is free", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: ','(','(call(zero(0)), ','(!_7, failure(a))), ','(no(zero(0)), ','(minus(0, 0, X40), ','(!_1, div(X40, 0, T21, T22))))) | ','(no(zero(0)), ','(no(zero(0)), ','(minus(0, 0, X40), ','(!_1, div(X40, 0, T21, T22))))), SCOPE: 7, CLAUSE: 9\n\nX40 is free", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: ','(zero(0), ','(','(!_7, failure(a)), ','(no(zero(0)), ','(minus(0, 0, X40), ','(!_1, div(X40, 0, T21, T22)))))) | ?_8 | ','(no(zero(0)), ','(no(zero(0)), ','(minus(0, 0, X40), ','(!_1, div(X40, 0, T21, T22))))), SCOPE: 7, CLAUSE: 9\n\nX40 is free", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: ','(zero(0), ','(','(!_7, failure(a)), ','(no(zero(0)), ','(minus(0, 0, X40), ','(!_1, div(X40, 0, T21, T22)))))), SCOPE: 9, CLAUSE: 7 | ?_9 | ?_8 | ','(no(zero(0)), ','(no(zero(0)), ','(minus(0, 0, X40), ','(!_1, div(X40, 0, T21, T22))))), SCOPE: 7, CLAUSE: 9\n\nX40 is free", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: ','(','(!_7, failure(a)), ','(no(zero(0)), ','(minus(0, 0, X40), ','(!_1, div(X40, 0, T21, T22))))) | ?_9 | ?_8 | ','(no(zero(0)), ','(no(zero(0)), ','(minus(0, 0, X40), ','(!_1, div(X40, 0, T21, T22))))), SCOPE: 7, CLAUSE: 9\n\nX40 is free", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: ','(failure(a), ','(no(zero(0)), ','(minus(0, 0, X40), ','(!_1, div(X40, 0, T21, T22)))))\n\nX40 is free", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: ','(failure(a), ','(no(zero(0)), ','(minus(0, 0, X40), ','(!_1, div(X40, 0, T21, T22))))), SCOPE: 10, CLAUSE: 6\n\nX40 is free", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: ','(no(zero(0)), no(zero(0)))\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: ','(no(zero(0)), no(zero(0))), SCOPE: 11, CLAUSE: 8 | ','(no(zero(0)), no(zero(0))), SCOPE: 11, CLAUSE: 9\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: ','(','(call(zero(0)), ','(!_11, failure(a))), no(zero(0))) | ','(no(zero(0)), no(zero(0))), SCOPE: 11, CLAUSE: 9\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="106: ','(zero(0), ','(','(!_11, failure(a)), no(zero(0)))) | ?_12 | ','(no(zero(0)), no(zero(0))), SCOPE: 11, CLAUSE: 9\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="108: ','(zero(0), ','(','(!_11, failure(a)), no(zero(0)))), SCOPE: 13, CLAUSE: 7 | ?_13 | ?_12 | ','(no(zero(0)), no(zero(0))), SCOPE: 11, CLAUSE: 9\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="109: ','(','(!_11, failure(a)), no(zero(0))) | ?_13 | ?_12 | ','(no(zero(0)), no(zero(0))), SCOPE: 11, CLAUSE: 9\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: ','(failure(a), no(zero(0)))\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: ','(failure(a), no(zero(0))), SCOPE: 14, CLAUSE: 6\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
114 [label="114: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
123 [label="123: div(T8, 0, T3, T4), SCOPE: 1, CLAUSE: 2\n\nT8 is ground\nX14 is free\ndiv(T8, 0, T3, T4) !=? div(0, X14, 0, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
124 [label="124: div(T8, 0, T3, T4), SCOPE: 1, CLAUSE: 3\n\nT8 is ground\nX14 is free\ndiv(T8, 0, T3, T4) !=? div(0, X14, 0, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
128 [label="128: ','(no(zero(T38)), ','(no(zero(0)), ','(minus(T38, 0, X80), ','(!_1, div(X80, 0, T41, T42)))))\n\nT38 is ground\nX14 is free\nX80 is free\ndiv(T38, 0, T3, T4) !=? div(0, X14, 0, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
129 [label="129: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
132 [label="132: ','(no(zero(T38)), ','(no(zero(0)), ','(minus(T38, 0, X80), ','(!_1, div(X80, 0, T41, T42))))), SCOPE: 15, CLAUSE: 8 | ','(no(zero(T38)), ','(no(zero(0)), ','(minus(T38, 0, X80), ','(!_1, div(X80, 0, T41, T42))))), SCOPE: 15, CLAUSE: 9\n\nT38 is ground\nX14 is free\nX80 is free\ndiv(T38, 0, T3, T4) !=? div(0, X14, 0, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
137 [label="137: ','(','(call(zero(T46)), ','(!_15, failure(a))), ','(no(zero(0)), ','(minus(T46, 0, X80), ','(!_1, div(X80, 0, T41, T42))))) | ','(no(zero(T46)), ','(no(zero(0)), ','(minus(T46, 0, X80), ','(!_1, div(X80, 0, T41, T42))))), SCOPE: 15, CLAUSE: 9\n\nT46 is ground\nX14 is free\nX80 is free\ndiv(T46, 0, T3, T4) !=? div(0, X14, 0, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
138 [label="138: ','(zero(T46), ','(','(!_15, failure(a)), ','(no(zero(0)), ','(minus(T46, 0, X80), ','(!_1, div(X80, 0, T41, T42)))))) | ?_16 | ','(no(zero(T46)), ','(no(zero(0)), ','(minus(T46, 0, X80), ','(!_1, div(X80, 0, T41, T42))))), SCOPE: 15, CLAUSE: 9\n\nT46 is ground\nX14 is free\nX80 is free\ndiv(T46, 0, T3, T4) !=? div(0, X14, 0, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
139 [label="139: ','(zero(T46), ','(','(!_15, failure(a)), ','(no(zero(0)), ','(minus(T46, 0, X80), ','(!_1, div(X80, 0, T41, T42)))))), SCOPE: 17, CLAUSE: 7 | ?_17 | ?_16 | ','(no(zero(T46)), ','(no(zero(0)), ','(minus(T46, 0, X80), ','(!_1, div(X80, 0, T41, T42))))), SCOPE: 15, CLAUSE: 9\n\nT46 is ground\nX14 is free\nX80 is free\ndiv(T46, 0, T3, T4) !=? div(0, X14, 0, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
141 [label="141: ','(','(!_15, failure(a)), ','(no(zero(0)), ','(minus(0, 0, X80), ','(!_1, div(X80, 0, T41, T42))))) | ?_17 | ?_16 | ','(no(zero(0)), ','(no(zero(0)), ','(minus(0, 0, X80), ','(!_1, div(X80, 0, T41, T42))))), SCOPE: 15, CLAUSE: 9\n\nX80 is free", fontsize=16, style=filled, fillcolor=lightyellow];
143 [label="143: ?_17 | ?_16 | ','(no(zero(T46)), ','(no(zero(0)), ','(minus(T46, 0, X80), ','(!_1, div(X80, 0, T41, T42))))), SCOPE: 15, CLAUSE: 9\n\nT46 is ground\nX14 is free\nX80 is free\ndiv(T46, 0, T3, T4) !=? div(0, X14, 0, 0)\nzero(T46) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
144 [label="144: ','(failure(a), ','(no(zero(0)), ','(minus(0, 0, X80), ','(!_1, div(X80, 0, T41, T42)))))\n\nX80 is free", fontsize=16, style=filled, fillcolor=lightyellow];
146 [label="146: ','(failure(a), ','(no(zero(0)), ','(minus(0, 0, X80), ','(!_1, div(X80, 0, T41, T42))))), SCOPE: 18, CLAUSE: 6\n\nX80 is free", fontsize=16, style=filled, fillcolor=lightyellow];
147 [label="147: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
148 [label="148: ?_16 | ','(no(zero(T46)), ','(no(zero(0)), ','(minus(T46, 0, X80), ','(!_1, div(X80, 0, T41, T42))))), SCOPE: 15, CLAUSE: 9\n\nT46 is ground\nX14 is free\nX80 is free\ndiv(T46, 0, T3, T4) !=? div(0, X14, 0, 0)\nzero(T46) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
150 [label="150: ','(no(zero(T46)), ','(no(zero(0)), ','(minus(T46, 0, X80), ','(!_1, div(X80, 0, T41, T42))))), SCOPE: 15, CLAUSE: 9\n\nT46 is ground\nX14 is free\nX80 is free\ndiv(T46, 0, T3, T4) !=? div(0, X14, 0, 0)\nzero(T46) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
157 [label="157: ','(no(zero(0)), ','(minus(T50, 0, X80), ','(!_1, div(X80, 0, T41, T42))))\n\nT50 is ground\nX14 is free\nX80 is free\ndiv(T50, 0, T3, T4) !=? div(0, X14, 0, 0)\nzero(T50) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
161 [label="161: ','(no(zero(0)), ','(minus(T50, 0, X80), ','(!_1, div(X80, 0, T41, T42)))), SCOPE: 19, CLAUSE: 8 | ','(no(zero(0)), ','(minus(T50, 0, X80), ','(!_1, div(X80, 0, T41, T42)))), SCOPE: 19, CLAUSE: 9\n\nT50 is ground\nX14 is free\nX80 is free\ndiv(T50, 0, T3, T4) !=? div(0, X14, 0, 0)\nzero(T50) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
168 [label="168: ','(','(call(zero(0)), ','(!_19, failure(a))), ','(minus(T50, 0, X80), ','(!_1, div(X80, 0, T41, T42)))) | ','(no(zero(0)), ','(minus(T50, 0, X80), ','(!_1, div(X80, 0, T41, T42)))), SCOPE: 19, CLAUSE: 9\n\nT50 is ground\nX14 is free\nX80 is free\ndiv(T50, 0, T3, T4) !=? div(0, X14, 0, 0)\nzero(T50) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
169 [label="169: ','(zero(0), ','(','(!_19, failure(a)), ','(minus(T50, 0, X80), ','(!_1, div(X80, 0, T41, T42))))) | ?_20 | ','(no(zero(0)), ','(minus(T50, 0, X80), ','(!_1, div(X80, 0, T41, T42)))), SCOPE: 19, CLAUSE: 9\n\nT50 is ground\nX14 is free\nX80 is free\ndiv(T50, 0, T3, T4) !=? div(0, X14, 0, 0)\nzero(T50) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
170 [label="170: ','(zero(0), ','(','(!_19, failure(a)), ','(minus(T50, 0, X80), ','(!_1, div(X80, 0, T41, T42))))), SCOPE: 21, CLAUSE: 7 | ?_21 | ?_20 | ','(no(zero(0)), ','(minus(T50, 0, X80), ','(!_1, div(X80, 0, T41, T42)))), SCOPE: 19, CLAUSE: 9\n\nT50 is ground\nX14 is free\nX80 is free\ndiv(T50, 0, T3, T4) !=? div(0, X14, 0, 0)\nzero(T50) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
172 [label="172: ','(','(!_19, failure(a)), ','(minus(T50, 0, X80), ','(!_1, div(X80, 0, T41, T42)))) | ?_21 | ?_20 | ','(no(zero(0)), ','(minus(T50, 0, X80), ','(!_1, div(X80, 0, T41, T42)))), SCOPE: 19, CLAUSE: 9\n\nT50 is ground\nX14 is free\nX80 is free\ndiv(T50, 0, T3, T4) !=? div(0, X14, 0, 0)\nzero(T50) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
175 [label="175: ','(failure(a), ','(minus(T50, 0, X80), ','(!_1, div(X80, 0, T41, T42))))\n\nT50 is ground\nX14 is free\nX80 is free\ndiv(T50, 0, T3, T4) !=? div(0, X14, 0, 0)\nzero(T50) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
177 [label="177: ','(failure(a), ','(minus(T50, 0, X80), ','(!_1, div(X80, 0, T41, T42)))), SCOPE: 22, CLAUSE: 6\n\nT50 is ground\nX14 is free\nX80 is free\ndiv(T50, 0, T3, T4) !=? div(0, X14, 0, 0)\nzero(T50) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
179 [label="179: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
184 [label="184: ','(no(zero(T57)), no(zero(0)))\n\nT57 is ground\nX14 is free\ndiv(T57, 0, T3, T4) !=? div(0, X14, 0, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
191 [label="191: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
193 [label="193: ','(no(zero(T57)), no(zero(0))), SCOPE: 23, CLAUSE: 8 | ','(no(zero(T57)), no(zero(0))), SCOPE: 23, CLAUSE: 9\n\nT57 is ground\nX14 is free\ndiv(T57, 0, T3, T4) !=? div(0, X14, 0, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
201 [label="201: ','(','(call(zero(T61)), ','(!_23, failure(a))), no(zero(0))) | ','(no(zero(T61)), no(zero(0))), SCOPE: 23, CLAUSE: 9\n\nT61 is ground\nX14 is free\ndiv(T61, 0, T3, T4) !=? div(0, X14, 0, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
204 [label="204: ','(zero(T61), ','(','(!_23, failure(a)), no(zero(0)))) | ?_24 | ','(no(zero(T61)), no(zero(0))), SCOPE: 23, CLAUSE: 9\n\nT61 is ground\nX14 is free\ndiv(T61, 0, T3, T4) !=? div(0, X14, 0, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
206 [label="206: ','(zero(T61), ','(','(!_23, failure(a)), no(zero(0)))), SCOPE: 25, CLAUSE: 7 | ?_25 | ?_24 | ','(no(zero(T61)), no(zero(0))), SCOPE: 23, CLAUSE: 9\n\nT61 is ground\nX14 is free\ndiv(T61, 0, T3, T4) !=? div(0, X14, 0, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
209 [label="209: ','(','(!_23, failure(a)), no(zero(0))) | ?_25 | ?_24 | ','(no(zero(0)), no(zero(0))), SCOPE: 23, CLAUSE: 9\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
212 [label="212: ?_25 | ?_24 | ','(no(zero(T61)), no(zero(0))), SCOPE: 23, CLAUSE: 9\n\nT61 is ground\nX14 is free\ndiv(T61, 0, T3, T4) !=? div(0, X14, 0, 0)\nzero(T61) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
215 [label="215: ','(failure(a), no(zero(0)))\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
217 [label="217: ','(failure(a), no(zero(0))), SCOPE: 26, CLAUSE: 6\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
218 [label="218: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
222 [label="222: ?_24 | ','(no(zero(T61)), no(zero(0))), SCOPE: 23, CLAUSE: 9\n\nT61 is ground\nX14 is free\ndiv(T61, 0, T3, T4) !=? div(0, X14, 0, 0)\nzero(T61) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
225 [label="225: ','(no(zero(T61)), no(zero(0))), SCOPE: 23, CLAUSE: 9\n\nT61 is ground\nX14 is free\ndiv(T61, 0, T3, T4) !=? div(0, X14, 0, 0)\nzero(T61) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
263 [label="263: no(zero(0))\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
264 [label="264: no(zero(0)), SCOPE: 27, CLAUSE: 8 | no(zero(0)), SCOPE: 27, CLAUSE: 9\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
267 [label="267: ','(call(zero(0)), ','(!_27, failure(a))) | no(zero(0)), SCOPE: 27, CLAUSE: 9\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
269 [label="269: ','(zero(0), ','(!_27, failure(a))) | ?_28 | no(zero(0)), SCOPE: 27, CLAUSE: 9\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
270 [label="270: ','(zero(0), ','(!_27, failure(a))), SCOPE: 29, CLAUSE: 7 | ?_29 | ?_28 | no(zero(0)), SCOPE: 27, CLAUSE: 9\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
272 [label="272: ','(!_27, failure(a)) | ?_29 | ?_28 | no(zero(0)), SCOPE: 27, CLAUSE: 9\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
273 [label="273: failure(a)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
276 [label="276: failure(a), SCOPE: 30, CLAUSE: 6\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
277 [label="277: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
280 [label="280: no(zero(T66)) | div(0, T66, T3, T4), SCOPE: 1, CLAUSE: 2 | div(0, T66, T3, T4), SCOPE: 1, CLAUSE: 3\n\nT66 is ground\nX9 is free\nX10 is free\nX11 is free\ndiv(0, T66, T3, T4) !=? div(X9, 0, X10, X11)", fontsize=16, style=filled, fillcolor=lightyellow];
284 [label="284: div(T1, T2, T3, T4), SCOPE: 1, CLAUSE: 2 | div(T1, T2, T3, T4), SCOPE: 1, CLAUSE: 3\n\nT1 is ground\nT2 is ground\nX9 is free\nX10 is free\nX11 is free\nX114 is free\ndiv(T1, T2, T3, T4) !=? div(X9, 0, X10, X11)\ndiv(T1, T2, T3, T4) !=? div(0, X114, 0, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
285 [label="285: no(zero(T66)), SCOPE: 31, CLAUSE: 8 | no(zero(T66)), SCOPE: 31, CLAUSE: 9 | ?_31 | div(0, T66, T3, T4), SCOPE: 1, CLAUSE: 2 | div(0, T66, T3, T4), SCOPE: 1, CLAUSE: 3\n\nT66 is ground\nX9 is free\nX10 is free\nX11 is free\ndiv(0, T66, T3, T4) !=? div(X9, 0, X10, X11)", fontsize=16, style=filled, fillcolor=lightyellow];
300 [label="300: ','(call(zero(T69)), ','(!_31, failure(a))) | no(zero(T69)), SCOPE: 31, CLAUSE: 9 | ?_31 | div(0, T69, T3, T4), SCOPE: 1, CLAUSE: 2 | div(0, T69, T3, T4), SCOPE: 1, CLAUSE: 3\n\nT69 is ground\nX9 is free\nX10 is free\nX11 is free\ndiv(0, T69, T3, T4) !=? div(X9, 0, X10, X11)", fontsize=16, style=filled, fillcolor=lightyellow];
302 [label="302: ','(zero(T69), ','(!_31, failure(a))) | ?_32 | no(zero(T69)), SCOPE: 31, CLAUSE: 9 | ?_31 | div(0, T69, T3, T4), SCOPE: 1, CLAUSE: 2 | div(0, T69, T3, T4), SCOPE: 1, CLAUSE: 3\n\nT69 is ground\nX9 is free\nX10 is free\nX11 is free\ndiv(0, T69, T3, T4) !=? div(X9, 0, X10, X11)", fontsize=16, style=filled, fillcolor=lightyellow];
304 [label="304: ','(zero(T69), ','(!_31, failure(a))), SCOPE: 33, CLAUSE: 7 | ?_33 | ?_32 | no(zero(T69)), SCOPE: 31, CLAUSE: 9 | ?_31 | div(0, T69, T3, T4), SCOPE: 1, CLAUSE: 2 | div(0, T69, T3, T4), SCOPE: 1, CLAUSE: 3\n\nT69 is ground\nX9 is free\nX10 is free\nX11 is free\ndiv(0, T69, T3, T4) !=? div(X9, 0, X10, X11)", fontsize=16, style=filled, fillcolor=lightyellow];
306 [label="306: ?_33 | ?_32 | no(zero(T69)), SCOPE: 31, CLAUSE: 9 | ?_31 | div(0, T69, T3, T4), SCOPE: 1, CLAUSE: 2 | div(0, T69, T3, T4), SCOPE: 1, CLAUSE: 3\n\nT69 is ground\nX9 is free\nX10 is free\nX11 is free\ndiv(0, T69, T3, T4) !=? div(X9, 0, X10, X11)", fontsize=16, style=filled, fillcolor=lightyellow];
309 [label="309: ?_32 | no(zero(T69)), SCOPE: 31, CLAUSE: 9 | ?_31 | div(0, T69, T3, T4), SCOPE: 1, CLAUSE: 2 | div(0, T69, T3, T4), SCOPE: 1, CLAUSE: 3\n\nT69 is ground\nX9 is free\nX10 is free\nX11 is free\ndiv(0, T69, T3, T4) !=? div(X9, 0, X10, X11)", fontsize=16, style=filled, fillcolor=lightyellow];
311 [label="311: no(zero(T69)), SCOPE: 31, CLAUSE: 9 | ?_31 | div(0, T69, T3, T4), SCOPE: 1, CLAUSE: 2 | div(0, T69, T3, T4), SCOPE: 1, CLAUSE: 3\n\nT69 is ground\nX9 is free\nX10 is free\nX11 is free\ndiv(0, T69, T3, T4) !=? div(X9, 0, X10, X11)", fontsize=16, style=filled, fillcolor=lightyellow];
314 [label="314: true | ?_31 | div(0, T72, T3, T4), SCOPE: 1, CLAUSE: 2 | div(0, T72, T3, T4), SCOPE: 1, CLAUSE: 3\n\nT72 is ground\nX9 is free\nX10 is free\nX11 is free\ndiv(0, T72, T3, T4) !=? div(X9, 0, X10, X11)", fontsize=16, style=filled, fillcolor=lightyellow];
317 [label="317: ?_31 | div(0, T72, T3, T4), SCOPE: 1, CLAUSE: 2 | div(0, T72, T3, T4), SCOPE: 1, CLAUSE: 3\n\nT72 is ground\nX9 is free\nX10 is free\nX11 is free\ndiv(0, T72, T3, T4) !=? div(X9, 0, X10, X11)", fontsize=16, style=filled, fillcolor=lightyellow];
318 [label="318: div(0, T72, T3, T4), SCOPE: 1, CLAUSE: 2 | div(0, T72, T3, T4), SCOPE: 1, CLAUSE: 3\n\nT72 is ground\nX9 is free\nX10 is free\nX11 is free\ndiv(0, T72, T3, T4) !=? div(X9, 0, X10, X11)", fontsize=16, style=filled, fillcolor=lightyellow];
341 [label="341: div(0, T72, T3, T4), SCOPE: 1, CLAUSE: 2\n\nT72 is ground\nX9 is free\nX10 is free\nX11 is free\ndiv(0, T72, T3, T4) !=? div(X9, 0, X10, X11)", fontsize=16, style=filled, fillcolor=lightyellow];
343 [label="343: div(0, T72, T3, T4), SCOPE: 1, CLAUSE: 3\n\nT72 is ground\nX9 is free\nX10 is free\nX11 is free\ndiv(0, T72, T3, T4) !=? div(X9, 0, X10, X11)", fontsize=16, style=filled, fillcolor=lightyellow];
347 [label="347: ','(no(zero(0)), ','(no(zero(T85)), ','(minus(0, T85, X143), ','(!_1, div(X143, T85, T88, T89)))))\n\nT85 is ground\nX9 is free\nX10 is free\nX11 is free\nX143 is free\ndiv(0, T85, T3, T4) !=? div(X9, 0, X10, X11)", fontsize=16, style=filled, fillcolor=lightyellow];
348 [label="348: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
352 [label="352: ','(no(zero(0)), ','(no(zero(T85)), ','(minus(0, T85, X143), ','(!_1, div(X143, T85, T88, T89))))), SCOPE: 34, CLAUSE: 8 | ','(no(zero(0)), ','(no(zero(T85)), ','(minus(0, T85, X143), ','(!_1, div(X143, T85, T88, T89))))), SCOPE: 34, CLAUSE: 9\n\nT85 is ground\nX9 is free\nX10 is free\nX11 is free\nX143 is free\ndiv(0, T85, T3, T4) !=? div(X9, 0, X10, X11)", fontsize=16, style=filled, fillcolor=lightyellow];
368 [label="368: ','(','(call(zero(0)), ','(!_34, failure(a))), ','(no(zero(T85)), ','(minus(0, T85, X143), ','(!_1, div(X143, T85, T88, T89))))) | ','(no(zero(0)), ','(no(zero(T85)), ','(minus(0, T85, X143), ','(!_1, div(X143, T85, T88, T89))))), SCOPE: 34, CLAUSE: 9\n\nT85 is ground\nX9 is free\nX10 is free\nX11 is free\nX143 is free\ndiv(0, T85, T3, T4) !=? div(X9, 0, X10, X11)", fontsize=16, style=filled, fillcolor=lightyellow];
371 [label="371: ','(zero(0), ','(','(!_34, failure(a)), ','(no(zero(T85)), ','(minus(0, T85, X143), ','(!_1, div(X143, T85, T88, T89)))))) | ?_35 | ','(no(zero(0)), ','(no(zero(T85)), ','(minus(0, T85, X143), ','(!_1, div(X143, T85, T88, T89))))), SCOPE: 34, CLAUSE: 9\n\nT85 is ground\nX9 is free\nX10 is free\nX11 is free\nX143 is free\ndiv(0, T85, T3, T4) !=? div(X9, 0, X10, X11)", fontsize=16, style=filled, fillcolor=lightyellow];
372 [label="372: ','(zero(0), ','(','(!_34, failure(a)), ','(no(zero(T85)), ','(minus(0, T85, X143), ','(!_1, div(X143, T85, T88, T89)))))), SCOPE: 36, CLAUSE: 7 | ?_36 | ?_35 | ','(no(zero(0)), ','(no(zero(T85)), ','(minus(0, T85, X143), ','(!_1, div(X143, T85, T88, T89))))), SCOPE: 34, CLAUSE: 9\n\nT85 is ground\nX9 is free\nX10 is free\nX11 is free\nX143 is free\ndiv(0, T85, T3, T4) !=? div(X9, 0, X10, X11)", fontsize=16, style=filled, fillcolor=lightyellow];
375 [label="375: ','(','(!_34, failure(a)), ','(no(zero(T85)), ','(minus(0, T85, X143), ','(!_1, div(X143, T85, T88, T89))))) | ?_36 | ?_35 | ','(no(zero(0)), ','(no(zero(T85)), ','(minus(0, T85, X143), ','(!_1, div(X143, T85, T88, T89))))), SCOPE: 34, CLAUSE: 9\n\nT85 is ground\nX9 is free\nX10 is free\nX11 is free\nX143 is free\ndiv(0, T85, T3, T4) !=? div(X9, 0, X10, X11)", fontsize=16, style=filled, fillcolor=lightyellow];
376 [label="376: ','(failure(a), ','(no(zero(T85)), ','(minus(0, T85, X143), ','(!_1, div(X143, T85, T88, T89)))))\n\nT85 is ground\nX9 is free\nX10 is free\nX11 is free\nX143 is free\ndiv(0, T85, T3, T4) !=? div(X9, 0, X10, X11)", fontsize=16, style=filled, fillcolor=lightyellow];
381 [label="381: ','(failure(a), ','(no(zero(T85)), ','(minus(0, T85, X143), ','(!_1, div(X143, T85, T88, T89))))), SCOPE: 37, CLAUSE: 6\n\nT85 is ground\nX9 is free\nX10 is free\nX11 is free\nX143 is free\ndiv(0, T85, T3, T4) !=? div(X9, 0, X10, X11)", fontsize=16, style=filled, fillcolor=lightyellow];
382 [label="382: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
387 [label="387: ','(no(zero(0)), no(zero(T94)))\n\nT94 is ground\nX9 is free\nX10 is free\nX11 is free\ndiv(0, T94, T3, T4) !=? div(X9, 0, X10, X11)", fontsize=16, style=filled, fillcolor=lightyellow];
399 [label="399: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
401 [label="401: ','(no(zero(0)), no(zero(T94))), SCOPE: 38, CLAUSE: 8 | ','(no(zero(0)), no(zero(T94))), SCOPE: 38, CLAUSE: 9\n\nT94 is ground\nX9 is free\nX10 is free\nX11 is free\ndiv(0, T94, T3, T4) !=? div(X9, 0, X10, X11)", fontsize=16, style=filled, fillcolor=lightyellow];
404 [label="404: ','(','(call(zero(0)), ','(!_38, failure(a))), no(zero(T94))) | ','(no(zero(0)), no(zero(T94))), SCOPE: 38, CLAUSE: 9\n\nT94 is ground\nX9 is free\nX10 is free\nX11 is free\ndiv(0, T94, T3, T4) !=? div(X9, 0, X10, X11)", fontsize=16, style=filled, fillcolor=lightyellow];
406 [label="406: ','(zero(0), ','(','(!_38, failure(a)), no(zero(T94)))) | ?_39 | ','(no(zero(0)), no(zero(T94))), SCOPE: 38, CLAUSE: 9\n\nT94 is ground\nX9 is free\nX10 is free\nX11 is free\ndiv(0, T94, T3, T4) !=? div(X9, 0, X10, X11)", fontsize=16, style=filled, fillcolor=lightyellow];
407 [label="407: ','(zero(0), ','(','(!_38, failure(a)), no(zero(T94)))), SCOPE: 40, CLAUSE: 7 | ?_40 | ?_39 | ','(no(zero(0)), no(zero(T94))), SCOPE: 38, CLAUSE: 9\n\nT94 is ground\nX9 is free\nX10 is free\nX11 is free\ndiv(0, T94, T3, T4) !=? div(X9, 0, X10, X11)", fontsize=16, style=filled, fillcolor=lightyellow];
409 [label="409: ','(','(!_38, failure(a)), no(zero(T94))) | ?_40 | ?_39 | ','(no(zero(0)), no(zero(T94))), SCOPE: 38, CLAUSE: 9\n\nT94 is ground\nX9 is free\nX10 is free\nX11 is free\ndiv(0, T94, T3, T4) !=? div(X9, 0, X10, X11)", fontsize=16, style=filled, fillcolor=lightyellow];
411 [label="411: ','(failure(a), no(zero(T94)))\n\nT94 is ground\nX9 is free\nX10 is free\nX11 is free\ndiv(0, T94, T3, T4) !=? div(X9, 0, X10, X11)", fontsize=16, style=filled, fillcolor=lightyellow];
413 [label="413: ','(failure(a), no(zero(T94))), SCOPE: 41, CLAUSE: 6\n\nT94 is ground\nX9 is free\nX10 is free\nX11 is free\ndiv(0, T94, T3, T4) !=? div(X9, 0, X10, X11)", fontsize=16, style=filled, fillcolor=lightyellow];
414 [label="414: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
421 [label="421: ','(no(zero(T100)), ','(no(zero(T101)), ','(minus(T100, T101, X177), ','(!_1, div(X177, T101, T104, T105))))) | div(T100, T101, T3, T4), SCOPE: 1, CLAUSE: 3\n\nT100 is ground\nT101 is ground\nX9 is free\nX10 is free\nX11 is free\nX114 is free\nX177 is free\ndiv(T100, T101, T3, T4) !=? div(X9, 0, X10, X11)\ndiv(T100, T101, T3, T4) !=? div(0, X114, 0, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
423 [label="423: div(T1, T2, T3, T4), SCOPE: 1, CLAUSE: 3\n\nT1 is ground\nT2 is ground\nX9 is free\nX10 is free\nX11 is free\nX114 is free\nX173 is free\nX174 is free\nX175 is free\nX176 is free\ndiv(T1, T2, T3, T4) !=? div(X9, 0, X10, X11)\ndiv(T1, T2, T3, T4) !=? div(0, X114, 0, 0)\ndiv(T1, T2, T3, T4) !=? div(X173, X174, s(X175), X176)", fontsize=16, style=filled, fillcolor=lightyellow];
424 [label="424: ','(no(zero(T100)), ','(no(zero(T101)), ','(minus(T100, T101, X177), ','(!_1, div(X177, T101, T104, T105))))), SCOPE: 42, CLAUSE: 8 | ','(no(zero(T100)), ','(no(zero(T101)), ','(minus(T100, T101, X177), ','(!_1, div(X177, T101, T104, T105))))), SCOPE: 42, CLAUSE: 9 | ?_42 | div(T100, T101, T3, T4), SCOPE: 1, CLAUSE: 3\n\nT100 is ground\nT101 is ground\nX9 is free\nX10 is free\nX11 is free\nX114 is free\nX177 is free\ndiv(T100, T101, T3, T4) !=? div(X9, 0, X10, X11)\ndiv(T100, T101, T3, T4) !=? div(0, X114, 0, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
427 [label="427: ','(','(call(zero(T108)), ','(!_42, failure(a))), ','(no(zero(T101)), ','(minus(T108, T101, X177), ','(!_1, div(X177, T101, T104, T105))))) | ','(no(zero(T108)), ','(no(zero(T101)), ','(minus(T108, T101, X177), ','(!_1, div(X177, T101, T104, T105))))), SCOPE: 42, CLAUSE: 9 | ?_42 | div(T108, T101, T3, T4), SCOPE: 1, CLAUSE: 3\n\nT101 is ground\nT108 is ground\nX9 is free\nX10 is free\nX11 is free\nX114 is free\nX177 is free\ndiv(T108, T101, T3, T4) !=? div(X9, 0, X10, X11)\ndiv(T108, T101, T3, T4) !=? div(0, X114, 0, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
428 [label="428: ','(zero(T108), ','(','(!_42, failure(a)), ','(no(zero(T101)), ','(minus(T108, T101, X177), ','(!_1, div(X177, T101, T104, T105)))))) | ?_43 | ','(no(zero(T108)), ','(no(zero(T101)), ','(minus(T108, T101, X177), ','(!_1, div(X177, T101, T104, T105))))), SCOPE: 42, CLAUSE: 9 | ?_42 | div(T108, T101, T3, T4), SCOPE: 1, CLAUSE: 3\n\nT101 is ground\nT108 is ground\nX9 is free\nX10 is free\nX11 is free\nX114 is free\nX177 is free\ndiv(T108, T101, T3, T4) !=? div(X9, 0, X10, X11)\ndiv(T108, T101, T3, T4) !=? div(0, X114, 0, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
429 [label="429: ','(zero(T108), ','(','(!_42, failure(a)), ','(no(zero(T101)), ','(minus(T108, T101, X177), ','(!_1, div(X177, T101, T104, T105)))))), SCOPE: 44, CLAUSE: 7 | ?_44 | ?_43 | ','(no(zero(T108)), ','(no(zero(T101)), ','(minus(T108, T101, X177), ','(!_1, div(X177, T101, T104, T105))))), SCOPE: 42, CLAUSE: 9 | ?_42 | div(T108, T101, T3, T4), SCOPE: 1, CLAUSE: 3\n\nT101 is ground\nT108 is ground\nX9 is free\nX10 is free\nX11 is free\nX114 is free\nX177 is free\ndiv(T108, T101, T3, T4) !=? div(X9, 0, X10, X11)\ndiv(T108, T101, T3, T4) !=? div(0, X114, 0, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
430 [label="430: ','(','(!_42, failure(a)), ','(no(zero(T101)), ','(minus(0, T101, X177), ','(!_1, div(X177, T101, T104, T105))))) | ?_44 | ?_43 | ','(no(zero(0)), ','(no(zero(T101)), ','(minus(0, T101, X177), ','(!_1, div(X177, T101, T104, T105))))), SCOPE: 42, CLAUSE: 9 | ?_42 | div(0, T101, T3, T4), SCOPE: 1, CLAUSE: 3\n\nT101 is ground\nX9 is free\nX10 is free\nX11 is free\nX114 is free\nX177 is free\ndiv(0, T101, T3, T4) !=? div(X9, 0, X10, X11)\ndiv(0, T101, T3, T4) !=? div(0, X114, 0, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
432 [label="432: ?_44 | ?_43 | ','(no(zero(T108)), ','(no(zero(T101)), ','(minus(T108, T101, X177), ','(!_1, div(X177, T101, T104, T105))))), SCOPE: 42, CLAUSE: 9 | ?_42 | div(T108, T101, T3, T4), SCOPE: 1, CLAUSE: 3\n\nT101 is ground\nT108 is ground\nX9 is free\nX10 is free\nX11 is free\nX114 is free\nX177 is free\ndiv(T108, T101, T3, T4) !=? div(X9, 0, X10, X11)\ndiv(T108, T101, T3, T4) !=? div(0, X114, 0, 0)\nzero(T108) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
444 [label="444: ','(failure(a), ','(no(zero(T101)), ','(minus(0, T101, X177), ','(!_1, div(X177, T101, T104, T105))))) | div(0, T101, T3, T4), SCOPE: 1, CLAUSE: 3\n\nT101 is ground\nX9 is free\nX10 is free\nX11 is free\nX114 is free\nX177 is free\ndiv(0, T101, T3, T4) !=? div(X9, 0, X10, X11)\ndiv(0, T101, T3, T4) !=? div(0, X114, 0, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
447 [label="447: ','(failure(a), ','(no(zero(T101)), ','(minus(0, T101, X177), ','(!_1, div(X177, T101, T104, T105))))), SCOPE: 45, CLAUSE: 6 | ?_45 | div(0, T101, T3, T4), SCOPE: 1, CLAUSE: 3\n\nT101 is ground\nX9 is free\nX10 is free\nX11 is free\nX114 is free\nX177 is free\ndiv(0, T101, T3, T4) !=? div(X9, 0, X10, X11)\ndiv(0, T101, T3, T4) !=? div(0, X114, 0, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
451 [label="451: ?_45 | div(0, T101, T3, T4), SCOPE: 1, CLAUSE: 3\n\nT101 is ground\nX9 is free\nX10 is free\nX11 is free\nX114 is free\ndiv(0, T101, T3, T4) !=? div(X9, 0, X10, X11)\ndiv(0, T101, T3, T4) !=? div(0, X114, 0, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
452 [label="452: div(0, T101, T3, T4), SCOPE: 1, CLAUSE: 3\n\nT101 is ground\nX9 is free\nX10 is free\nX11 is free\nX114 is free\ndiv(0, T101, T3, T4) !=? div(X9, 0, X10, X11)\ndiv(0, T101, T3, T4) !=? div(0, X114, 0, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
454 [label="454: ','(no(zero(0)), no(zero(T113)))\n\nT113 is ground\nX9 is free\nX10 is free\nX11 is free\nX114 is free\ndiv(0, T113, T3, T4) !=? div(X9, 0, X10, X11)\ndiv(0, T113, T3, T4) !=? div(0, X114, 0, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
456 [label="456: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
457 [label="457: ','(no(zero(0)), no(zero(T113))), SCOPE: 46, CLAUSE: 8 | ','(no(zero(0)), no(zero(T113))), SCOPE: 46, CLAUSE: 9\n\nT113 is ground\nX9 is free\nX10 is free\nX11 is free\nX114 is free\ndiv(0, T113, T3, T4) !=? div(X9, 0, X10, X11)\ndiv(0, T113, T3, T4) !=? div(0, X114, 0, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
467 [label="467: ','(','(call(zero(0)), ','(!_46, failure(a))), no(zero(T113))) | ','(no(zero(0)), no(zero(T113))), SCOPE: 46, CLAUSE: 9\n\nT113 is ground\nX9 is free\nX10 is free\nX11 is free\nX114 is free\ndiv(0, T113, T3, T4) !=? div(X9, 0, X10, X11)\ndiv(0, T113, T3, T4) !=? div(0, X114, 0, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
468 [label="468: ','(zero(0), ','(','(!_46, failure(a)), no(zero(T113)))) | ?_47 | ','(no(zero(0)), no(zero(T113))), SCOPE: 46, CLAUSE: 9\n\nT113 is ground\nX9 is free\nX10 is free\nX11 is free\nX114 is free\ndiv(0, T113, T3, T4) !=? div(X9, 0, X10, X11)\ndiv(0, T113, T3, T4) !=? div(0, X114, 0, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
470 [label="470: ','(zero(0), ','(','(!_46, failure(a)), no(zero(T113)))), SCOPE: 48, CLAUSE: 7 | ?_48 | ?_47 | ','(no(zero(0)), no(zero(T113))), SCOPE: 46, CLAUSE: 9\n\nT113 is ground\nX9 is free\nX10 is free\nX11 is free\nX114 is free\ndiv(0, T113, T3, T4) !=? div(X9, 0, X10, X11)\ndiv(0, T113, T3, T4) !=? div(0, X114, 0, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
473 [label="473: ','(','(!_46, failure(a)), no(zero(T113))) | ?_48 | ?_47 | ','(no(zero(0)), no(zero(T113))), SCOPE: 46, CLAUSE: 9\n\nT113 is ground\nX9 is free\nX10 is free\nX11 is free\nX114 is free\ndiv(0, T113, T3, T4) !=? div(X9, 0, X10, X11)\ndiv(0, T113, T3, T4) !=? div(0, X114, 0, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
474 [label="474: ','(failure(a), no(zero(T113)))\n\nT113 is ground\nX9 is free\nX10 is free\nX11 is free\nX114 is free\ndiv(0, T113, T3, T4) !=? div(X9, 0, X10, X11)\ndiv(0, T113, T3, T4) !=? div(0, X114, 0, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
475 [label="475: ','(failure(a), no(zero(T113))), SCOPE: 49, CLAUSE: 6\n\nT113 is ground\nX9 is free\nX10 is free\nX11 is free\nX114 is free\ndiv(0, T113, T3, T4) !=? div(X9, 0, X10, X11)\ndiv(0, T113, T3, T4) !=? div(0, X114, 0, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
476 [label="476: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
477 [label="477: ?_43 | ','(no(zero(T108)), ','(no(zero(T101)), ','(minus(T108, T101, X177), ','(!_1, div(X177, T101, T104, T105))))), SCOPE: 42, CLAUSE: 9 | ?_42 | div(T108, T101, T3, T4), SCOPE: 1, CLAUSE: 3\n\nT101 is ground\nT108 is ground\nX9 is free\nX10 is free\nX11 is free\nX114 is free\nX177 is free\ndiv(T108, T101, T3, T4) !=? div(X9, 0, X10, X11)\ndiv(T108, T101, T3, T4) !=? div(0, X114, 0, 0)\nzero(T108) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
479 [label="479: ','(no(zero(T108)), ','(no(zero(T101)), ','(minus(T108, T101, X177), ','(!_1, div(X177, T101, T104, T105))))), SCOPE: 42, CLAUSE: 9 | ?_42 | div(T108, T101, T3, T4), SCOPE: 1, CLAUSE: 3\n\nT101 is ground\nT108 is ground\nX9 is free\nX10 is free\nX11 is free\nX114 is free\nX177 is free\ndiv(T108, T101, T3, T4) !=? div(X9, 0, X10, X11)\ndiv(T108, T101, T3, T4) !=? div(0, X114, 0, 0)\nzero(T108) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
484 [label="484: ','(no(zero(T101)), ','(minus(T121, T101, X177), ','(!_1, div(X177, T101, T104, T105)))) | ?_42 | div(T121, T101, T3, T4), SCOPE: 1, CLAUSE: 3\n\nT101 is ground\nT121 is ground\nX9 is free\nX10 is free\nX11 is free\nX114 is free\nX177 is free\ndiv(T121, T101, T3, T4) !=? div(X9, 0, X10, X11)\ndiv(T121, T101, T3, T4) !=? div(0, X114, 0, 0)\nzero(T121) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
485 [label="485: ','(no(zero(T101)), ','(minus(T121, T101, X177), ','(!_1, div(X177, T101, T104, T105)))), SCOPE: 50, CLAUSE: 8 | ','(no(zero(T101)), ','(minus(T121, T101, X177), ','(!_1, div(X177, T101, T104, T105)))), SCOPE: 50, CLAUSE: 9 | ?_50 | ?_42 | div(T121, T101, T3, T4), SCOPE: 1, CLAUSE: 3\n\nT101 is ground\nT121 is ground\nX9 is free\nX10 is free\nX11 is free\nX114 is free\nX177 is free\ndiv(T121, T101, T3, T4) !=? div(X9, 0, X10, X11)\ndiv(T121, T101, T3, T4) !=? div(0, X114, 0, 0)\nzero(T121) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
486 [label="486: ','(','(call(zero(T128)), ','(!_50, failure(a))), ','(minus(T121, T128, X177), ','(!_1, div(X177, T128, T104, T105)))) | ','(no(zero(T128)), ','(minus(T121, T128, X177), ','(!_1, div(X177, T128, T104, T105)))), SCOPE: 50, CLAUSE: 9 | ?_50 | ?_42 | div(T121, T128, T3, T4), SCOPE: 1, CLAUSE: 3\n\nT121 is ground\nT128 is ground\nX9 is free\nX10 is free\nX11 is free\nX114 is free\nX177 is free\ndiv(T121, T128, T3, T4) !=? div(X9, 0, X10, X11)\ndiv(T121, T128, T3, T4) !=? div(0, X114, 0, 0)\nzero(T121) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
487 [label="487: ','(zero(T128), ','(','(!_50, failure(a)), ','(minus(T121, T128, X177), ','(!_1, div(X177, T128, T104, T105))))) | ?_51 | ','(no(zero(T128)), ','(minus(T121, T128, X177), ','(!_1, div(X177, T128, T104, T105)))), SCOPE: 50, CLAUSE: 9 | ?_50 | ?_42 | div(T121, T128, T3, T4), SCOPE: 1, CLAUSE: 3\n\nT121 is ground\nT128 is ground\nX9 is free\nX10 is free\nX11 is free\nX114 is free\nX177 is free\ndiv(T121, T128, T3, T4) !=? div(X9, 0, X10, X11)\ndiv(T121, T128, T3, T4) !=? div(0, X114, 0, 0)\nzero(T121) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
489 [label="489: ','(zero(T128), ','(','(!_50, failure(a)), ','(minus(T121, T128, X177), ','(!_1, div(X177, T128, T104, T105))))), SCOPE: 52, CLAUSE: 7 | ?_52 | ?_51 | ','(no(zero(T128)), ','(minus(T121, T128, X177), ','(!_1, div(X177, T128, T104, T105)))), SCOPE: 50, CLAUSE: 9 | ?_50 | ?_42 | div(T121, T128, T3, T4), SCOPE: 1, CLAUSE: 3\n\nT121 is ground\nT128 is ground\nX9 is free\nX10 is free\nX11 is free\nX114 is free\nX177 is free\ndiv(T121, T128, T3, T4) !=? div(X9, 0, X10, X11)\ndiv(T121, T128, T3, T4) !=? div(0, X114, 0, 0)\nzero(T121) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
493 [label="493: ?_52 | ?_51 | ','(no(zero(T128)), ','(minus(T121, T128, X177), ','(!_1, div(X177, T128, T104, T105)))), SCOPE: 50, CLAUSE: 9 | ?_50 | ?_42 | div(T121, T128, T3, T4), SCOPE: 1, CLAUSE: 3\n\nT121 is ground\nT128 is ground\nX9 is free\nX10 is free\nX11 is free\nX114 is free\nX177 is free\ndiv(T121, T128, T3, T4) !=? div(X9, 0, X10, X11)\ndiv(T121, T128, T3, T4) !=? div(0, X114, 0, 0)\nzero(T121) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
494 [label="494: ?_51 | ','(no(zero(T128)), ','(minus(T121, T128, X177), ','(!_1, div(X177, T128, T104, T105)))), SCOPE: 50, CLAUSE: 9 | ?_50 | ?_42 | div(T121, T128, T3, T4), SCOPE: 1, CLAUSE: 3\n\nT121 is ground\nT128 is ground\nX9 is free\nX10 is free\nX11 is free\nX114 is free\nX177 is free\ndiv(T121, T128, T3, T4) !=? div(X9, 0, X10, X11)\ndiv(T121, T128, T3, T4) !=? div(0, X114, 0, 0)\nzero(T121) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
496 [label="496: ','(no(zero(T128)), ','(minus(T121, T128, X177), ','(!_1, div(X177, T128, T104, T105)))), SCOPE: 50, CLAUSE: 9 | ?_50 | ?_42 | div(T121, T128, T3, T4), SCOPE: 1, CLAUSE: 3\n\nT121 is ground\nT128 is ground\nX9 is free\nX10 is free\nX11 is free\nX114 is free\nX177 is free\ndiv(T121, T128, T3, T4) !=? div(X9, 0, X10, X11)\ndiv(T121, T128, T3, T4) !=? div(0, X114, 0, 0)\nzero(T121) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
515 [label="515: ','(minus(T121, T135, X177), ','(!_1, div(X177, T135, T104, T105))) | ?_50 | ?_42 | div(T121, T135, T3, T4), SCOPE: 1, CLAUSE: 3\n\nT121 is ground\nT135 is ground\nX9 is free\nX10 is free\nX11 is free\nX114 is free\nX177 is free\ndiv(T121, T135, T3, T4) !=? div(X9, 0, X10, X11)\ndiv(T121, T135, T3, T4) !=? div(0, X114, 0, 0)\nzero(T121) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
517 [label="B: ','(minus(T121, T135, X177), ','(!_1, div(X177, T135, T104, T105)))\n\nT121 is ground\nT135 is ground\nX9 is free\nX10 is free\nX11 is free\nX114 is free\nX177 is free\ndiv(T121, T135, T3, T4) !=? div(X9, 0, X10, X11)\ndiv(T121, T135, T3, T4) !=? div(0, X114, 0, 0)\nzero(T121) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
519 [label="519: ?_50 | ?_42 | div(T121, T135, T3, T4), SCOPE: 1, CLAUSE: 3\n\nT121 is ground\nT135 is ground\nX9 is free\nX10 is free\nX11 is free\nX114 is free\ndiv(T121, T135, T3, T4) !=? div(X9, 0, X10, X11)\ndiv(T121, T135, T3, T4) !=? div(0, X114, 0, 0)\nzero(T121) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
533 [label="D: minus(T121, T135, X177)\n\nT121 is ground\nT135 is ground\nX9 is free\nX10 is free\nX11 is free\nX114 is free\nX177 is free\ndiv(T121, T135, T3, T4) !=? div(X9, 0, X10, X11)\ndiv(T121, T135, T3, T4) !=? div(0, X114, 0, 0)\nzero(T121) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
536 [label="E: ','(!_1, div(T144, T135, T104, T105))\n\nT121 is ground\nT135 is ground\nT144 is ground\nX9 is free\nX10 is free\nX11 is free\nX114 is free\ndiv(T121, T135, T3, T4) !=? div(X9, 0, X10, X11)\ndiv(T121, T135, T3, T4) !=? div(0, X114, 0, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
546 [label="546: minus(T121, T135, X177), SCOPE: 53, CLAUSE: 4 | minus(T121, T135, X177), SCOPE: 53, CLAUSE: 5\n\nT121 is ground\nT135 is ground\nX9 is free\nX10 is free\nX11 is free\nX114 is free\nX177 is free\ndiv(T121, T135, T3, T4) !=? div(X9, 0, X10, X11)\ndiv(T121, T135, T3, T4) !=? div(0, X114, 0, 0)\nzero(T121) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
547 [label="547: minus(T121, T135, X177), SCOPE: 53, CLAUSE: 5\n\nT121 is ground\nT135 is ground\nX9 is free\nX10 is free\nX11 is free\nX114 is free\nX177 is free\ndiv(T121, T135, T3, T4) !=? div(X9, 0, X10, X11)\ndiv(T121, T135, T3, T4) !=? div(0, X114, 0, 0)\nzero(T121) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
548 [label="C: minus(T154, T155, X255)\n\nT154 is ground\nT155 is ground\nX255 is free", fontsize=16, style=filled, fillcolor=lightyellow];
549 [label="549: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
553 [label="553: minus(T154, T155, X255), SCOPE: 54, CLAUSE: 4 | minus(T154, T155, X255), SCOPE: 54, CLAUSE: 5\n\nT154 is ground\nT155 is ground\nX255 is free", fontsize=16, style=filled, fillcolor=lightyellow];
555 [label="555: minus(T154, T155, X255), SCOPE: 54, CLAUSE: 4\n\nT154 is ground\nT155 is ground\nX255 is free", fontsize=16, style=filled, fillcolor=lightyellow];
556 [label="556: minus(T154, T155, X255), SCOPE: 54, CLAUSE: 5\n\nT154 is ground\nT155 is ground\nX255 is free", fontsize=16, style=filled, fillcolor=lightyellow];
558 [label="558: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
559 [label="559: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
560 [label="560: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
564 [label="564: minus(T167, T168, X274)\n\nT167 is ground\nT168 is ground\nX274 is free", fontsize=16, style=filled, fillcolor=lightyellow];
565 [label="565: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
566 [label="566: div(T144, T135, T104, T105)\n\nT121 is ground\nT135 is ground\nT144 is ground\nX9 is free\nX10 is free\nX11 is free\nX114 is free\ndiv(T121, T135, T3, T4) !=? div(X9, 0, X10, X11)\ndiv(T121, T135, T3, T4) !=? div(0, X114, 0, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
567 [label="567: ?_42 | div(T121, T135, T3, T4), SCOPE: 1, CLAUSE: 3\n\nT121 is ground\nT135 is ground\nX9 is free\nX10 is free\nX11 is free\nX114 is free\ndiv(T121, T135, T3, T4) !=? div(X9, 0, X10, X11)\ndiv(T121, T135, T3, T4) !=? div(0, X114, 0, 0)\nzero(T121) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
568 [label="568: div(T121, T135, T3, T4), SCOPE: 1, CLAUSE: 3\n\nT121 is ground\nT135 is ground\nX9 is free\nX10 is free\nX11 is free\nX114 is free\ndiv(T121, T135, T3, T4) !=? div(X9, 0, X10, X11)\ndiv(T121, T135, T3, T4) !=? div(0, X114, 0, 0)\nzero(T121) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
569 [label="569: ','(no(zero(T181)), no(zero(T182)))\n\nT181 is ground\nT182 is ground\nX9 is free\nX10 is free\nX11 is free\nX114 is free\ndiv(T181, T182, T3, T4) !=? div(X9, 0, X10, X11)\ndiv(T181, T182, T3, T4) !=? div(0, X114, 0, 0)\nzero(T181) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
570 [label="570: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
571 [label="571: ','(no(zero(T181)), no(zero(T182))), SCOPE: 55, CLAUSE: 8 | ','(no(zero(T181)), no(zero(T182))), SCOPE: 55, CLAUSE: 9\n\nT181 is ground\nT182 is ground\nX9 is free\nX10 is free\nX11 is free\nX114 is free\ndiv(T181, T182, T3, T4) !=? div(X9, 0, X10, X11)\ndiv(T181, T182, T3, T4) !=? div(0, X114, 0, 0)\nzero(T181) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
572 [label="572: ','(','(call(zero(T186)), ','(!_55, failure(a))), no(zero(T182))) | ','(no(zero(T186)), no(zero(T182))), SCOPE: 55, CLAUSE: 9\n\nT182 is ground\nT186 is ground\nX9 is free\nX10 is free\nX11 is free\nX114 is free\ndiv(T186, T182, T3, T4) !=? div(X9, 0, X10, X11)\ndiv(T186, T182, T3, T4) !=? div(0, X114, 0, 0)\nzero(T186) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
573 [label="573: ','(zero(T186), ','(','(!_55, failure(a)), no(zero(T182)))) | ?_56 | ','(no(zero(T186)), no(zero(T182))), SCOPE: 55, CLAUSE: 9\n\nT182 is ground\nT186 is ground\nX9 is free\nX10 is free\nX11 is free\nX114 is free\ndiv(T186, T182, T3, T4) !=? div(X9, 0, X10, X11)\ndiv(T186, T182, T3, T4) !=? div(0, X114, 0, 0)\nzero(T186) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
574 [label="574: ','(zero(T186), ','(','(!_55, failure(a)), no(zero(T182)))), SCOPE: 57, CLAUSE: 7 | ?_57 | ?_56 | ','(no(zero(T186)), no(zero(T182))), SCOPE: 55, CLAUSE: 9\n\nT182 is ground\nT186 is ground\nX9 is free\nX10 is free\nX11 is free\nX114 is free\ndiv(T186, T182, T3, T4) !=? div(X9, 0, X10, X11)\ndiv(T186, T182, T3, T4) !=? div(0, X114, 0, 0)\nzero(T186) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
575 [label="575: ?_57 | ?_56 | ','(no(zero(T186)), no(zero(T182))), SCOPE: 55, CLAUSE: 9\n\nT182 is ground\nT186 is ground\nX9 is free\nX10 is free\nX11 is free\nX114 is free\ndiv(T186, T182, T3, T4) !=? div(X9, 0, X10, X11)\ndiv(T186, T182, T3, T4) !=? div(0, X114, 0, 0)\nzero(T186) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
576 [label="576: ?_56 | ','(no(zero(T186)), no(zero(T182))), SCOPE: 55, CLAUSE: 9\n\nT182 is ground\nT186 is ground\nX9 is free\nX10 is free\nX11 is free\nX114 is free\ndiv(T186, T182, T3, T4) !=? div(X9, 0, X10, X11)\ndiv(T186, T182, T3, T4) !=? div(0, X114, 0, 0)\nzero(T186) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
577 [label="577: ','(no(zero(T186)), no(zero(T182))), SCOPE: 55, CLAUSE: 9\n\nT182 is ground\nT186 is ground\nX9 is free\nX10 is free\nX11 is free\nX114 is free\ndiv(T186, T182, T3, T4) !=? div(X9, 0, X10, X11)\ndiv(T186, T182, T3, T4) !=? div(0, X114, 0, 0)\nzero(T186) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
578 [label="578: no(zero(T182))\n\nT182 is ground\nT189 is ground\nX9 is free\nX10 is free\nX11 is free\nX114 is free\ndiv(T189, T182, T3, T4) !=? div(X9, 0, X10, X11)\ndiv(T189, T182, T3, T4) !=? div(0, X114, 0, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
579 [label="579: no(zero(T182)), SCOPE: 58, CLAUSE: 8 | no(zero(T182)), SCOPE: 58, CLAUSE: 9\n\nT182 is ground\nT189 is ground\nX9 is free\nX10 is free\nX11 is free\nX114 is free\ndiv(T189, T182, T3, T4) !=? div(X9, 0, X10, X11)\ndiv(T189, T182, T3, T4) !=? div(0, X114, 0, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
580 [label="580: ','(call(zero(T192)), ','(!_58, failure(a))) | no(zero(T192)), SCOPE: 58, CLAUSE: 9\n\nT189 is ground\nT192 is ground\nX9 is free\nX10 is free\nX11 is free\nX114 is free\ndiv(T189, T192, T3, T4) !=? div(X9, 0, X10, X11)\ndiv(T189, T192, T3, T4) !=? div(0, X114, 0, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
581 [label="581: ','(zero(T192), ','(!_58, failure(a))) | ?_59 | no(zero(T192)), SCOPE: 58, CLAUSE: 9\n\nT189 is ground\nT192 is ground\nX9 is free\nX10 is free\nX11 is free\nX114 is free\ndiv(T189, T192, T3, T4) !=? div(X9, 0, X10, X11)\ndiv(T189, T192, T3, T4) !=? div(0, X114, 0, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
582 [label="582: ','(zero(T192), ','(!_58, failure(a))), SCOPE: 60, CLAUSE: 7 | ?_60 | ?_59 | no(zero(T192)), SCOPE: 58, CLAUSE: 9\n\nT189 is ground\nT192 is ground\nX9 is free\nX10 is free\nX11 is free\nX114 is free\ndiv(T189, T192, T3, T4) !=? div(X9, 0, X10, X11)\ndiv(T189, T192, T3, T4) !=? div(0, X114, 0, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
583 [label="583: ?_60 | ?_59 | no(zero(T192)), SCOPE: 58, CLAUSE: 9\n\nT189 is ground\nT192 is ground\nX9 is free\nX10 is free\nX11 is free\nX114 is free\ndiv(T189, T192, T3, T4) !=? div(X9, 0, X10, X11)\ndiv(T189, T192, T3, T4) !=? div(0, X114, 0, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
584 [label="584: ?_59 | no(zero(T192)), SCOPE: 58, CLAUSE: 9\n\nT189 is ground\nT192 is ground\nX9 is free\nX10 is free\nX11 is free\nX114 is free\ndiv(T189, T192, T3, T4) !=? div(X9, 0, X10, X11)\ndiv(T189, T192, T3, T4) !=? div(0, X114, 0, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
585 [label="585: no(zero(T192)), SCOPE: 58, CLAUSE: 9\n\nT189 is ground\nT192 is ground\nX9 is free\nX10 is free\nX11 is free\nX114 is free\ndiv(T189, T192, T3, T4) !=? div(X9, 0, X10, X11)\ndiv(T189, T192, T3, T4) !=? div(0, X114, 0, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
586 [label="586: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
587 [label="587: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
588 [label="588: ','(no(zero(T199)), no(zero(T200)))\n\nT199 is ground\nT200 is ground\nX9 is free\nX10 is free\nX11 is free\nX114 is free\nX173 is free\nX174 is free\nX175 is free\nX176 is free\ndiv(T199, T200, T3, T4) !=? div(X9, 0, X10, X11)\ndiv(T199, T200, T3, T4) !=? div(0, X114, 0, 0)\ndiv(T199, T200, T3, T4) !=? div(X173, X174, s(X175), X176)", fontsize=16, style=filled, fillcolor=lightyellow];
589 [label="589: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
590 [label="590: ','(no(zero(T199)), no(zero(T200))), SCOPE: 61, CLAUSE: 8 | ','(no(zero(T199)), no(zero(T200))), SCOPE: 61, CLAUSE: 9\n\nT199 is ground\nT200 is ground\nX9 is free\nX10 is free\nX11 is free\nX114 is free\nX173 is free\nX174 is free\nX175 is free\nX176 is free\ndiv(T199, T200, T3, T4) !=? div(X9, 0, X10, X11)\ndiv(T199, T200, T3, T4) !=? div(0, X114, 0, 0)\ndiv(T199, T200, T3, T4) !=? div(X173, X174, s(X175), X176)", fontsize=16, style=filled, fillcolor=lightyellow];
591 [label="591: ','(','(call(zero(T204)), ','(!_61, failure(a))), no(zero(T200))) | ','(no(zero(T204)), no(zero(T200))), SCOPE: 61, CLAUSE: 9\n\nT200 is ground\nT204 is ground\nX9 is free\nX10 is free\nX11 is free\nX114 is free\nX173 is free\nX174 is free\nX175 is free\nX176 is free\ndiv(T204, T200, T3, T4) !=? div(X9, 0, X10, X11)\ndiv(T204, T200, T3, T4) !=? div(0, X114, 0, 0)\ndiv(T204, T200, T3, T4) !=? div(X173, X174, s(X175), X176)", fontsize=16, style=filled, fillcolor=lightyellow];
592 [label="592: ','(zero(T204), ','(','(!_61, failure(a)), no(zero(T200)))) | ?_62 | ','(no(zero(T204)), no(zero(T200))), SCOPE: 61, CLAUSE: 9\n\nT200 is ground\nT204 is ground\nX9 is free\nX10 is free\nX11 is free\nX114 is free\nX173 is free\nX174 is free\nX175 is free\nX176 is free\ndiv(T204, T200, T3, T4) !=? div(X9, 0, X10, X11)\ndiv(T204, T200, T3, T4) !=? div(0, X114, 0, 0)\ndiv(T204, T200, T3, T4) !=? div(X173, X174, s(X175), X176)", fontsize=16, style=filled, fillcolor=lightyellow];
593 [label="593: ','(zero(T204), ','(','(!_61, failure(a)), no(zero(T200)))), SCOPE: 63, CLAUSE: 7 | ?_63 | ?_62 | ','(no(zero(T204)), no(zero(T200))), SCOPE: 61, CLAUSE: 9\n\nT200 is ground\nT204 is ground\nX9 is free\nX10 is free\nX11 is free\nX114 is free\nX173 is free\nX174 is free\nX175 is free\nX176 is free\ndiv(T204, T200, T3, T4) !=? div(X9, 0, X10, X11)\ndiv(T204, T200, T3, T4) !=? div(0, X114, 0, 0)\ndiv(T204, T200, T3, T4) !=? div(X173, X174, s(X175), X176)", fontsize=16, style=filled, fillcolor=lightyellow];
594 [label="594: ','(','(!_61, failure(a)), no(zero(T200))) | ?_63 | ?_62 | ','(no(zero(0)), no(zero(T200))), SCOPE: 61, CLAUSE: 9\n\nT200 is ground\nX9 is free\nX10 is free\nX11 is free\nX114 is free\nX173 is free\nX174 is free\nX175 is free\nX176 is free\ndiv(0, T200, T3, T4) !=? div(X9, 0, X10, X11)\ndiv(0, T200, T3, T4) !=? div(0, X114, 0, 0)\ndiv(0, T200, T3, T4) !=? div(X173, X174, s(X175), X176)", fontsize=16, style=filled, fillcolor=lightyellow];
595 [label="595: ?_63 | ?_62 | ','(no(zero(T204)), no(zero(T200))), SCOPE: 61, CLAUSE: 9\n\nT200 is ground\nT204 is ground\nX9 is free\nX10 is free\nX11 is free\nX114 is free\nX173 is free\nX174 is free\nX175 is free\nX176 is free\ndiv(T204, T200, T3, T4) !=? div(X9, 0, X10, X11)\ndiv(T204, T200, T3, T4) !=? div(0, X114, 0, 0)\ndiv(T204, T200, T3, T4) !=? div(X173, X174, s(X175), X176)\nzero(T204) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
596 [label="596: ','(failure(a), no(zero(T200)))\n\nT200 is ground\nX9 is free\nX10 is free\nX11 is free\nX114 is free\nX173 is free\nX174 is free\nX175 is free\nX176 is free\ndiv(0, T200, T3, T4) !=? div(X9, 0, X10, X11)\ndiv(0, T200, T3, T4) !=? div(0, X114, 0, 0)\ndiv(0, T200, T3, T4) !=? div(X173, X174, s(X175), X176)", fontsize=16, style=filled, fillcolor=lightyellow];
597 [label="597: ','(failure(a), no(zero(T200))), SCOPE: 64, CLAUSE: 6\n\nT200 is ground\nX9 is free\nX10 is free\nX11 is free\nX114 is free\nX173 is free\nX174 is free\nX175 is free\nX176 is free\ndiv(0, T200, T3, T4) !=? div(X9, 0, X10, X11)\ndiv(0, T200, T3, T4) !=? div(0, X114, 0, 0)\ndiv(0, T200, T3, T4) !=? div(X173, X174, s(X175), X176)", fontsize=16, style=filled, fillcolor=lightyellow];
598 [label="598: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
599 [label="599: ?_62 | ','(no(zero(T204)), no(zero(T200))), SCOPE: 61, CLAUSE: 9\n\nT200 is ground\nT204 is ground\nX9 is free\nX10 is free\nX11 is free\nX114 is free\nX173 is free\nX174 is free\nX175 is free\nX176 is free\ndiv(T204, T200, T3, T4) !=? div(X9, 0, X10, X11)\ndiv(T204, T200, T3, T4) !=? div(0, X114, 0, 0)\ndiv(T204, T200, T3, T4) !=? div(X173, X174, s(X175), X176)\nzero(T204) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
600 [label="600: ','(no(zero(T204)), no(zero(T200))), SCOPE: 61, CLAUSE: 9\n\nT200 is ground\nT204 is ground\nX9 is free\nX10 is free\nX11 is free\nX114 is free\nX173 is free\nX174 is free\nX175 is free\nX176 is free\ndiv(T204, T200, T3, T4) !=? div(X9, 0, X10, X11)\ndiv(T204, T200, T3, T4) !=? div(0, X114, 0, 0)\ndiv(T204, T200, T3, T4) !=? div(X173, X174, s(X175), X176)\nzero(T204) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
601 [label="601: no(zero(T200))\n\nT200 is ground\nT207 is ground\nX9 is free\nX10 is free\nX11 is free\nX114 is free\nX173 is free\nX174 is free\nX175 is free\nX176 is free\ndiv(T207, T200, T3, T4) !=? div(X9, 0, X10, X11)\ndiv(T207, T200, T3, T4) !=? div(0, X114, 0, 0)\ndiv(T207, T200, T3, T4) !=? div(X173, X174, s(X175), X176)", fontsize=16, style=filled, fillcolor=lightyellow];
602 [label="602: no(zero(T200)), SCOPE: 65, CLAUSE: 8 | no(zero(T200)), SCOPE: 65, CLAUSE: 9\n\nT200 is ground\nT207 is ground\nX9 is free\nX10 is free\nX11 is free\nX114 is free\nX173 is free\nX174 is free\nX175 is free\nX176 is free\ndiv(T207, T200, T3, T4) !=? div(X9, 0, X10, X11)\ndiv(T207, T200, T3, T4) !=? div(0, X114, 0, 0)\ndiv(T207, T200, T3, T4) !=? div(X173, X174, s(X175), X176)", fontsize=16, style=filled, fillcolor=lightyellow];
603 [label="603: ','(call(zero(T210)), ','(!_65, failure(a))) | no(zero(T210)), SCOPE: 65, CLAUSE: 9\n\nT207 is ground\nT210 is ground\nX9 is free\nX10 is free\nX11 is free\nX114 is free\nX173 is free\nX174 is free\nX175 is free\nX176 is free\ndiv(T207, T210, T3, T4) !=? div(X9, 0, X10, X11)\ndiv(T207, T210, T3, T4) !=? div(0, X114, 0, 0)\ndiv(T207, T210, T3, T4) !=? div(X173, X174, s(X175), X176)", fontsize=16, style=filled, fillcolor=lightyellow];
604 [label="604: ','(zero(T210), ','(!_65, failure(a))) | ?_66 | no(zero(T210)), SCOPE: 65, CLAUSE: 9\n\nT207 is ground\nT210 is ground\nX9 is free\nX10 is free\nX11 is free\nX114 is free\nX173 is free\nX174 is free\nX175 is free\nX176 is free\ndiv(T207, T210, T3, T4) !=? div(X9, 0, X10, X11)\ndiv(T207, T210, T3, T4) !=? div(0, X114, 0, 0)\ndiv(T207, T210, T3, T4) !=? div(X173, X174, s(X175), X176)", fontsize=16, style=filled, fillcolor=lightyellow];
605 [label="605: ','(zero(T210), ','(!_65, failure(a))), SCOPE: 67, CLAUSE: 7 | ?_67 | ?_66 | no(zero(T210)), SCOPE: 65, CLAUSE: 9\n\nT207 is ground\nT210 is ground\nX9 is free\nX10 is free\nX11 is free\nX114 is free\nX173 is free\nX174 is free\nX175 is free\nX176 is free\ndiv(T207, T210, T3, T4) !=? div(X9, 0, X10, X11)\ndiv(T207, T210, T3, T4) !=? div(0, X114, 0, 0)\ndiv(T207, T210, T3, T4) !=? div(X173, X174, s(X175), X176)", fontsize=16, style=filled, fillcolor=lightyellow];
606 [label="606: ?_67 | ?_66 | no(zero(T210)), SCOPE: 65, CLAUSE: 9\n\nT207 is ground\nT210 is ground\nX9 is free\nX10 is free\nX11 is free\nX114 is free\nX173 is free\nX174 is free\nX175 is free\nX176 is free\ndiv(T207, T210, T3, T4) !=? div(X9, 0, X10, X11)\ndiv(T207, T210, T3, T4) !=? div(0, X114, 0, 0)\ndiv(T207, T210, T3, T4) !=? div(X173, X174, s(X175), X176)", fontsize=16, style=filled, fillcolor=lightyellow];
607 [label="607: ?_66 | no(zero(T210)), SCOPE: 65, CLAUSE: 9\n\nT207 is ground\nT210 is ground\nX9 is free\nX10 is free\nX11 is free\nX114 is free\nX173 is free\nX174 is free\nX175 is free\nX176 is free\ndiv(T207, T210, T3, T4) !=? div(X9, 0, X10, X11)\ndiv(T207, T210, T3, T4) !=? div(0, X114, 0, 0)\ndiv(T207, T210, T3, T4) !=? div(X173, X174, s(X175), X176)", fontsize=16, style=filled, fillcolor=lightyellow];
608 [label="608: no(zero(T210)), SCOPE: 65, CLAUSE: 9\n\nT207 is ground\nT210 is ground\nX9 is free\nX10 is free\nX11 is free\nX114 is free\nX173 is free\nX174 is free\nX175 is free\nX176 is free\ndiv(T207, T210, T3, T4) !=? div(X9, 0, X10, X11)\ndiv(T207, T210, T3, T4) !=? div(0, X114, 0, 0)\ndiv(T207, T210, T3, T4) !=? div(X173, X174, s(X175), X176)", fontsize=16, style=filled, fillcolor=lightyellow];
609 [label="609: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
610 [label="610: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
611 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
3 -> 611 [arrowhead = none ];
611 -> 5;

612 [label="EVAL with clause\ndiv(X9, 0, X10, X11) :- failure(a).\nand substitutionT1 -> T8,\nX9 -> T8,\nT2 -> 0,\nT3 -> T9,\nX10 -> T9,\nT4 -> T10,\nX11 -> T10", fontsize=14, style = filled, fillcolor = lightblue];
5 -> 612 [arrowhead = none ];
612 -> 8;

613 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
5 -> 613 [arrowhead = none ];
613 -> 10;

614 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
8 -> 614 [arrowhead = none ];
614 -> 20;

615 [label="EVAL with clause\ndiv(0, X114, 0, 0) :- no(zero(X114)).\nand substitutionT1 -> 0,\nT2 -> T66,\nX114 -> T66,\nT3 -> 0,\nT4 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
10 -> 615 [arrowhead = none ];
615 -> 280;

616 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
10 -> 616 [arrowhead = none ];
616 -> 284;

617 [label="BACKTRACK\nfor clause: failure(b)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
20 -> 617 [arrowhead = none ];
617 -> 21;

618 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
21 -> 618 [arrowhead = none ];
618 -> 22;

619 [label="EVAL with clause\ndiv(0, X14, 0, 0) :- no(zero(X14)).\nand substitutionT8 -> 0,\nX14 -> 0,\nT3 -> 0,\nT4 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
22 -> 619 [arrowhead = none ];
619 -> 26;

620 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
22 -> 620 [arrowhead = none ];
620 -> 28;

621 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
26 -> 621 [arrowhead = none ];
621 -> 30;

622 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
28 -> 622 [arrowhead = none ];
622 -> 123;

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

624 [label="ONLY EVAL with clause\nno(X17) :- ','(call(X17), ','(!_3, failure(a))).\nand substitutionX17 -> zero(0)", fontsize=14, style = filled, fillcolor = lightblue];
30 -> 624 [arrowhead = none ];
624 -> 32;

625 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
32 -> 625 [arrowhead = none ];
625 -> 33;

626 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
33 -> 626 [arrowhead = none ];
626 -> 37;

627 [label="ONLY EVAL with clause\nzero(0).\nand substitution", fontsize=14, style = filled, fillcolor = lightblue];
37 -> 627 [arrowhead = none ];
627 -> 39;

628 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
39 -> 628 [arrowhead = none ];
628 -> 41;

629 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
41 -> 629 [arrowhead = none ];
629 -> 45;

630 [label="BACKTRACK\nfor clause: failure(b)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
45 -> 630 [arrowhead = none ];
630 -> 48;

631 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
48 -> 631 [arrowhead = none ];
631 -> 51;

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

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

634 [label="EVAL with clause\ndiv(X36, X37, s(X38), X39) :- ','(no(zero(X36)), ','(no(zero(X37)), ','(minus(X36, X37, X40), ','(!_1, div(X40, X37, X38, X39))))).\nand substitutionX36 -> 0,\nX37 -> 0,\nX38 -> T21,\nT3 -> s(T21),\nT4 -> T22,\nX39 -> T22,\nT19 -> T21,\nT20 -> T22", fontsize=14, style = filled, fillcolor = lightblue];
55 -> 634 [arrowhead = none ];
634 -> 61;

635 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
55 -> 635 [arrowhead = none ];
635 -> 62;

636 [label="EVAL with clause\ndiv(X52, X53, X54, X52) :- ','(no(zero(X52)), no(zero(X53))).\nand substitutionX52 -> 0,\nX53 -> 0,\nT3 -> T25,\nX54 -> T25,\nT4 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
56 -> 636 [arrowhead = none ];
636 -> 84;

637 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
56 -> 637 [arrowhead = none ];
637 -> 85;

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

639 [label="ONLY EVAL with clause\nno(X44) :- ','(call(X44), ','(!_7, failure(a))).\nand substitutionX44 -> zero(0)", fontsize=14, style = filled, fillcolor = lightblue];
64 -> 639 [arrowhead = none ];
639 -> 66;

640 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
66 -> 640 [arrowhead = none ];
640 -> 68;

641 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
68 -> 641 [arrowhead = none ];
641 -> 70;

642 [label="ONLY EVAL with clause\nzero(0).\nand substitution", fontsize=14, style = filled, fillcolor = lightblue];
70 -> 642 [arrowhead = none ];
642 -> 73;

643 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
73 -> 643 [arrowhead = none ];
643 -> 74;

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

645 [label="BACKTRACK\nfor clause: failure(b)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
76 -> 645 [arrowhead = none ];
645 -> 78;

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

647 [label="ONLY EVAL with clause\nno(X57) :- ','(call(X57), ','(!_11, failure(a))).\nand substitutionX57 -> zero(0)", fontsize=14, style = filled, fillcolor = lightblue];
86 -> 647 [arrowhead = none ];
647 -> 88;

648 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
88 -> 648 [arrowhead = none ];
648 -> 106;

649 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
106 -> 649 [arrowhead = none ];
649 -> 108;

650 [label="ONLY EVAL with clause\nzero(0).\nand substitution", fontsize=14, style = filled, fillcolor = lightblue];
108 -> 650 [arrowhead = none ];
650 -> 109;

651 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
109 -> 651 [arrowhead = none ];
651 -> 111;

652 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
111 -> 652 [arrowhead = none ];
652 -> 113;

653 [label="BACKTRACK\nfor clause: failure(b)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
113 -> 653 [arrowhead = none ];
653 -> 114;

654 [label="EVAL with clause\ndiv(X76, X77, s(X78), X79) :- ','(no(zero(X76)), ','(no(zero(X77)), ','(minus(X76, X77, X80), ','(!_1, div(X80, X77, X78, X79))))).\nand substitutionT8 -> T38,\nX76 -> T38,\nX77 -> 0,\nX78 -> T41,\nT3 -> s(T41),\nT4 -> T42,\nX79 -> T42,\nT39 -> T41,\nT40 -> T42", fontsize=14, style = filled, fillcolor = lightblue];
123 -> 654 [arrowhead = none ];
654 -> 128;

655 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
123 -> 655 [arrowhead = none ];
655 -> 129;

656 [label="EVAL with clause\ndiv(X101, X102, X103, X101) :- ','(no(zero(X101)), no(zero(X102))).\nand substitutionT8 -> T57,\nX101 -> T57,\nX102 -> 0,\nT3 -> T58,\nX103 -> T58,\nT4 -> T57", fontsize=14, style = filled, fillcolor = lightblue];
124 -> 656 [arrowhead = none ];
656 -> 184;

657 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
124 -> 657 [arrowhead = none ];
657 -> 191;

658 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
128 -> 658 [arrowhead = none ];
658 -> 132;

659 [label="ONLY EVAL with clause\nno(X84) :- ','(call(X84), ','(!_15, failure(a))).\nand substitutionT38 -> T46,\nX84 -> zero(T46)", fontsize=14, style = filled, fillcolor = lightblue];
132 -> 659 [arrowhead = none ];
659 -> 137;

660 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
137 -> 660 [arrowhead = none ];
660 -> 138;

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

662 [label="EVAL with clause\nzero(0).\nand substitutionT46 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
139 -> 662 [arrowhead = none ];
662 -> 141;

663 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
139 -> 663 [arrowhead = none ];
663 -> 143;

664 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
141 -> 664 [arrowhead = none ];
664 -> 144;

665 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
143 -> 665 [arrowhead = none ];
665 -> 148;

666 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
144 -> 666 [arrowhead = none ];
666 -> 146;

667 [label="BACKTRACK\nfor clause: failure(b)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
146 -> 667 [arrowhead = none ];
667 -> 147;

668 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
148 -> 668 [arrowhead = none ];
668 -> 150;

669 [label="ONLY EVAL with clause\nno(X89).\nand substitutionT46 -> T50,\nX89 -> zero(T50)", fontsize=14, style = filled, fillcolor = lightblue];
150 -> 669 [arrowhead = none ];
669 -> 157;

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

671 [label="ONLY EVAL with clause\nno(X93) :- ','(call(X93), ','(!_19, failure(a))).\nand substitutionX93 -> zero(0)", fontsize=14, style = filled, fillcolor = lightblue];
161 -> 671 [arrowhead = none ];
671 -> 168;

672 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
168 -> 672 [arrowhead = none ];
672 -> 169;

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

674 [label="ONLY EVAL with clause\nzero(0).\nand substitution", fontsize=14, style = filled, fillcolor = lightblue];
170 -> 674 [arrowhead = none ];
674 -> 172;

675 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
172 -> 675 [arrowhead = none ];
675 -> 175;

676 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
175 -> 676 [arrowhead = none ];
676 -> 177;

677 [label="BACKTRACK\nfor clause: failure(b)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
177 -> 677 [arrowhead = none ];
677 -> 179;

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

679 [label="ONLY EVAL with clause\nno(X106) :- ','(call(X106), ','(!_23, failure(a))).\nand substitutionT57 -> T61,\nX106 -> zero(T61)", fontsize=14, style = filled, fillcolor = lightblue];
193 -> 679 [arrowhead = none ];
679 -> 201;

680 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
201 -> 680 [arrowhead = none ];
680 -> 204;

681 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
204 -> 681 [arrowhead = none ];
681 -> 206;

682 [label="EVAL with clause\nzero(0).\nand substitutionT61 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
206 -> 682 [arrowhead = none ];
682 -> 209;

683 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
206 -> 683 [arrowhead = none ];
683 -> 212;

684 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
209 -> 684 [arrowhead = none ];
684 -> 215;

685 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
212 -> 685 [arrowhead = none ];
685 -> 222;

686 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
215 -> 686 [arrowhead = none ];
686 -> 217;

687 [label="BACKTRACK\nfor clause: failure(b)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
217 -> 687 [arrowhead = none ];
687 -> 218;

688 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
222 -> 688 [arrowhead = none ];
688 -> 225;

689 [label="ONLY EVAL with clause\nno(X109).\nand substitutionT61 -> T64,\nX109 -> zero(T64)", fontsize=14, style = filled, fillcolor = lightblue];
225 -> 689 [arrowhead = none ];
689 -> 263;

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

691 [label="ONLY EVAL with clause\nno(X112) :- ','(call(X112), ','(!_27, failure(a))).\nand substitutionX112 -> zero(0)", fontsize=14, style = filled, fillcolor = lightblue];
264 -> 691 [arrowhead = none ];
691 -> 267;

692 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
267 -> 692 [arrowhead = none ];
692 -> 269;

693 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
269 -> 693 [arrowhead = none ];
693 -> 270;

694 [label="ONLY EVAL with clause\nzero(0).\nand substitution", fontsize=14, style = filled, fillcolor = lightblue];
270 -> 694 [arrowhead = none ];
694 -> 272;

695 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
272 -> 695 [arrowhead = none ];
695 -> 273;

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

697 [label="BACKTRACK\nfor clause: failure(b)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
276 -> 697 [arrowhead = none ];
697 -> 277;

698 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
280 -> 698 [arrowhead = none ];
698 -> 285;

699 [label="EVAL with clause\ndiv(X173, X174, s(X175), X176) :- ','(no(zero(X173)), ','(no(zero(X174)), ','(minus(X173, X174, X177), ','(!_1, div(X177, X174, X175, X176))))).\nand substitutionT1 -> T100,\nX173 -> T100,\nT2 -> T101,\nX174 -> T101,\nX175 -> T104,\nT3 -> s(T104),\nT4 -> T105,\nX176 -> T105,\nT102 -> T104,\nT103 -> T105", fontsize=14, style = filled, fillcolor = lightblue];
284 -> 699 [arrowhead = none ];
699 -> 421;

700 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
284 -> 700 [arrowhead = none ];
700 -> 423;

701 [label="ONLY EVAL with clause\nno(X117) :- ','(call(X117), ','(!_31, failure(a))).\nand substitutionT66 -> T69,\nX117 -> zero(T69)", fontsize=14, style = filled, fillcolor = lightblue];
285 -> 701 [arrowhead = none ];
701 -> 300;

702 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
300 -> 702 [arrowhead = none ];
702 -> 302;

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

704 [label="BACKTRACK\nfor clause: zero(0)\nwith clash: (div(0, T69, T3, T4), div(X9, 0, X10, X11))", fontsize=14, style = filled, fillcolor = lightgreen];
304 -> 704 [arrowhead = none ];
704 -> 306;

705 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
306 -> 705 [arrowhead = none ];
705 -> 309;

706 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
309 -> 706 [arrowhead = none ];
706 -> 311;

707 [label="ONLY EVAL with clause\nno(X120).\nand substitutionT69 -> T72,\nX120 -> zero(T72)", fontsize=14, style = filled, fillcolor = lightblue];
311 -> 707 [arrowhead = none ];
707 -> 314;

708 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
314 -> 708 [arrowhead = none ];
708 -> 317;

709 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
317 -> 709 [arrowhead = none ];
709 -> 318;

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

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

712 [label="EVAL with clause\ndiv(X139, X140, s(X141), X142) :- ','(no(zero(X139)), ','(no(zero(X140)), ','(minus(X139, X140, X143), ','(!_1, div(X143, X140, X141, X142))))).\nand substitutionX139 -> 0,\nT72 -> T85,\nX140 -> T85,\nX141 -> T88,\nT3 -> s(T88),\nT4 -> T89,\nX142 -> T89,\nT86 -> T88,\nT87 -> T89", fontsize=14, style = filled, fillcolor = lightblue];
341 -> 712 [arrowhead = none ];
712 -> 347;

713 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
341 -> 713 [arrowhead = none ];
713 -> 348;

714 [label="EVAL with clause\ndiv(X163, X164, X165, X163) :- ','(no(zero(X163)), no(zero(X164))).\nand substitutionX163 -> 0,\nT72 -> T94,\nX164 -> T94,\nT3 -> T95,\nX165 -> T95,\nT4 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
343 -> 714 [arrowhead = none ];
714 -> 387;

715 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
343 -> 715 [arrowhead = none ];
715 -> 399;

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

717 [label="ONLY EVAL with clause\nno(X151) :- ','(call(X151), ','(!_34, failure(a))).\nand substitutionX151 -> zero(0)", fontsize=14, style = filled, fillcolor = lightblue];
352 -> 717 [arrowhead = none ];
717 -> 368;

718 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
368 -> 718 [arrowhead = none ];
718 -> 371;

719 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
371 -> 719 [arrowhead = none ];
719 -> 372;

720 [label="ONLY EVAL with clause\nzero(0).\nand substitution", fontsize=14, style = filled, fillcolor = lightblue];
372 -> 720 [arrowhead = none ];
720 -> 375;

721 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
375 -> 721 [arrowhead = none ];
721 -> 376;

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

723 [label="BACKTRACK\nfor clause: failure(b)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
381 -> 723 [arrowhead = none ];
723 -> 382;

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

725 [label="ONLY EVAL with clause\nno(X168) :- ','(call(X168), ','(!_38, failure(a))).\nand substitutionX168 -> zero(0)", fontsize=14, style = filled, fillcolor = lightblue];
401 -> 725 [arrowhead = none ];
725 -> 404;

726 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
404 -> 726 [arrowhead = none ];
726 -> 406;

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

728 [label="ONLY EVAL with clause\nzero(0).\nand substitution", fontsize=14, style = filled, fillcolor = lightblue];
407 -> 728 [arrowhead = none ];
728 -> 409;

729 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
409 -> 729 [arrowhead = none ];
729 -> 411;

730 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
411 -> 730 [arrowhead = none ];
730 -> 413;

731 [label="BACKTRACK\nfor clause: failure(b)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
413 -> 731 [arrowhead = none ];
731 -> 414;

732 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
421 -> 732 [arrowhead = none ];
732 -> 424;

733 [label="EVAL with clause\ndiv(X305, X306, X307, X305) :- ','(no(zero(X305)), no(zero(X306))).\nand substitutionT1 -> T199,\nX305 -> T199,\nT2 -> T200,\nX306 -> T200,\nT3 -> T201,\nX307 -> T201,\nT4 -> T199", fontsize=14, style = filled, fillcolor = lightblue];
423 -> 733 [arrowhead = none ];
733 -> 588;

734 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
423 -> 734 [arrowhead = none ];
734 -> 589;

735 [label="ONLY EVAL with clause\nno(X180) :- ','(call(X180), ','(!_42, failure(a))).\nand substitutionT100 -> T108,\nX180 -> zero(T108)", fontsize=14, style = filled, fillcolor = lightblue];
424 -> 735 [arrowhead = none ];
735 -> 427;

736 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
427 -> 736 [arrowhead = none ];
736 -> 428;

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

738 [label="EVAL with clause\nzero(0).\nand substitutionT108 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
429 -> 738 [arrowhead = none ];
738 -> 430;

739 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
429 -> 739 [arrowhead = none ];
739 -> 432;

740 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
430 -> 740 [arrowhead = none ];
740 -> 444;

741 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
432 -> 741 [arrowhead = none ];
741 -> 477;

742 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
444 -> 742 [arrowhead = none ];
742 -> 447;

743 [label="BACKTRACK\nfor clause: failure(b)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
447 -> 743 [arrowhead = none ];
743 -> 451;

744 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
451 -> 744 [arrowhead = none ];
744 -> 452;

745 [label="EVAL with clause\ndiv(X192, X193, X194, X192) :- ','(no(zero(X192)), no(zero(X193))).\nand substitutionX192 -> 0,\nT101 -> T113,\nX193 -> T113,\nT3 -> T114,\nX194 -> T114,\nT4 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
452 -> 745 [arrowhead = none ];
745 -> 454;

746 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
452 -> 746 [arrowhead = none ];
746 -> 456;

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

748 [label="ONLY EVAL with clause\nno(X197) :- ','(call(X197), ','(!_46, failure(a))).\nand substitutionX197 -> zero(0)", fontsize=14, style = filled, fillcolor = lightblue];
457 -> 748 [arrowhead = none ];
748 -> 467;

749 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
467 -> 749 [arrowhead = none ];
749 -> 468;

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

751 [label="ONLY EVAL with clause\nzero(0).\nand substitution", fontsize=14, style = filled, fillcolor = lightblue];
470 -> 751 [arrowhead = none ];
751 -> 473;

752 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
473 -> 752 [arrowhead = none ];
752 -> 474;

753 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
474 -> 753 [arrowhead = none ];
753 -> 475;

754 [label="BACKTRACK\nfor clause: failure(b)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
475 -> 754 [arrowhead = none ];
754 -> 476;

755 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
477 -> 755 [arrowhead = none ];
755 -> 479;

756 [label="ONLY EVAL with clause\nno(X206).\nand substitutionT108 -> T121,\nX206 -> zero(T121)", fontsize=14, style = filled, fillcolor = lightblue];
479 -> 756 [arrowhead = none ];
756 -> 484;

757 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
484 -> 757 [arrowhead = none ];
757 -> 485;

758 [label="ONLY EVAL with clause\nno(X215) :- ','(call(X215), ','(!_50, failure(a))).\nand substitutionT101 -> T128,\nX215 -> zero(T128)", fontsize=14, style = filled, fillcolor = lightblue];
485 -> 758 [arrowhead = none ];
758 -> 486;

759 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
486 -> 759 [arrowhead = none ];
759 -> 487;

760 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
487 -> 760 [arrowhead = none ];
760 -> 489;

761 [label="BACKTRACK\nfor clause: zero(0)\nwith clash: (div(T121, T128, T3, T4), div(X9, 0, X10, X11))", fontsize=14, style = filled, fillcolor = lightgreen];
489 -> 761 [arrowhead = none ];
761 -> 493;

762 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
493 -> 762 [arrowhead = none ];
762 -> 494;

763 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
494 -> 763 [arrowhead = none ];
763 -> 496;

764 [label="ONLY EVAL with clause\nno(X224).\nand substitutionT128 -> T135,\nX224 -> zero(T135)", fontsize=14, style = filled, fillcolor = lightblue];
496 -> 764 [arrowhead = none ];
764 -> 515;

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

766 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
515 -> 766 [arrowhead = none ];
766 -> 519;

767 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
517 -> 767 [arrowhead = none ];
767 -> 533;

768 [label="SPLIT 2\nnew knowledge:\nT121 is ground\nT135 is ground\nT144 is ground\nreplacements:X177 -> T144", fontsize=14, style = filled, fillcolor = violet];
517 -> 768 [arrowhead = none ];
768 -> 536;

769 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
519 -> 769 [arrowhead = none ];
769 -> 567;

770 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
533 -> 770 [arrowhead = none ];
770 -> 546;

771 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
536 -> 771 [arrowhead = none ];
771 -> 566;

772 [label="BACKTRACK\nfor clause: minus(X, 0, X)\nwith clash: (div(T121, T135, T3, T4), div(X9, 0, X10, X11))", fontsize=14, style = filled, fillcolor = lightgreen];
546 -> 772 [arrowhead = none ];
772 -> 547;

773 [label="EVAL with clause\nminus(s(X252), s(X253), X254) :- minus(X252, X253, X254).\nand substitutionX252 -> T154,\nT121 -> s(T154),\nX253 -> T155,\nT135 -> s(T155),\nX177 -> X255,\nX254 -> X255", fontsize=14, style = filled, fillcolor = lightblue];
547 -> 773 [arrowhead = none ];
773 -> 548;

774 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
547 -> 774 [arrowhead = none ];
774 -> 549;

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

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

777 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
553 -> 777 [arrowhead = none ];
777 -> 556;

778 [label="EVAL with clause\nminus(X262, 0, X262).\nand substitutionT154 -> T162,\nX262 -> T162,\nT155 -> 0,\nX255 -> T162", fontsize=14, style = filled, fillcolor = lightblue];
555 -> 778 [arrowhead = none ];
778 -> 558;

779 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
555 -> 779 [arrowhead = none ];
779 -> 559;

780 [label="EVAL with clause\nminus(s(X271), s(X272), X273) :- minus(X271, X272, X273).\nand substitutionX271 -> T167,\nT154 -> s(T167),\nX272 -> T168,\nT155 -> s(T168),\nX255 -> X274,\nX273 -> X274", fontsize=14, style = filled, fillcolor = lightblue];
556 -> 780 [arrowhead = none ];
780 -> 564;

781 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
556 -> 781 [arrowhead = none ];
781 -> 565;

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

783 [label="INSTANCE with matching:\nT154 -> T167\nT155 -> T168\nX255 -> X274", fontsize=14, style = filled, fillcolor = lightgrey];
564 -> 783 [arrowhead = none , style=dashed];
783 -> 548[style=dashed];

784 [label="INSTANCE with matching:\nT1 -> T144\nT2 -> T135\nT3 -> T104\nT4 -> T105", fontsize=14, style = filled, fillcolor = lightgrey];
566 -> 784 [arrowhead = none , style=dashed];
784 -> 3[style=dashed];

785 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
567 -> 785 [arrowhead = none ];
785 -> 568;

786 [label="EVAL with clause\ndiv(X287, X288, X289, X287) :- ','(no(zero(X287)), no(zero(X288))).\nand substitutionT121 -> T181,\nX287 -> T181,\nT135 -> T182,\nX288 -> T182,\nT3 -> T183,\nX289 -> T183,\nT4 -> T181", fontsize=14, style = filled, fillcolor = lightblue];
568 -> 786 [arrowhead = none ];
786 -> 569;

787 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
568 -> 787 [arrowhead = none ];
787 -> 570;

788 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
569 -> 788 [arrowhead = none ];
788 -> 571;

789 [label="ONLY EVAL with clause\nno(X292) :- ','(call(X292), ','(!_55, failure(a))).\nand substitutionT181 -> T186,\nX292 -> zero(T186)", fontsize=14, style = filled, fillcolor = lightblue];
571 -> 789 [arrowhead = none ];
789 -> 572;

790 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
572 -> 790 [arrowhead = none ];
790 -> 573;

791 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
573 -> 791 [arrowhead = none ];
791 -> 574;

792 [label="BACKTRACK\nfor clause: zero(0)\nwith clash: (zero(T186), zero(0))", fontsize=14, style = filled, fillcolor = lightgreen];
574 -> 792 [arrowhead = none ];
792 -> 575;

793 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
575 -> 793 [arrowhead = none ];
793 -> 576;

794 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
576 -> 794 [arrowhead = none ];
794 -> 577;

795 [label="ONLY EVAL with clause\nno(X295).\nand substitutionT186 -> T189,\nX295 -> zero(T189)", fontsize=14, style = filled, fillcolor = lightblue];
577 -> 795 [arrowhead = none ];
795 -> 578;

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

797 [label="ONLY EVAL with clause\nno(X298) :- ','(call(X298), ','(!_58, failure(a))).\nand substitutionT182 -> T192,\nX298 -> zero(T192)", fontsize=14, style = filled, fillcolor = lightblue];
579 -> 797 [arrowhead = none ];
797 -> 580;

798 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
580 -> 798 [arrowhead = none ];
798 -> 581;

799 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
581 -> 799 [arrowhead = none ];
799 -> 582;

800 [label="BACKTRACK\nfor clause: zero(0)\nwith clash: (div(T189, T192, T3, T4), div(X9, 0, X10, X11))", fontsize=14, style = filled, fillcolor = lightgreen];
582 -> 800 [arrowhead = none ];
800 -> 583;

801 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
583 -> 801 [arrowhead = none ];
801 -> 584;

802 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
584 -> 802 [arrowhead = none ];
802 -> 585;

803 [label="ONLY EVAL with clause\nno(X301).\nand substitutionT192 -> T195,\nX301 -> zero(T195)", fontsize=14, style = filled, fillcolor = lightblue];
585 -> 803 [arrowhead = none ];
803 -> 586;

804 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
586 -> 804 [arrowhead = none ];
804 -> 587;

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

806 [label="ONLY EVAL with clause\nno(X310) :- ','(call(X310), ','(!_61, failure(a))).\nand substitutionT199 -> T204,\nX310 -> zero(T204)", fontsize=14, style = filled, fillcolor = lightblue];
590 -> 806 [arrowhead = none ];
806 -> 591;

807 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
591 -> 807 [arrowhead = none ];
807 -> 592;

808 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
592 -> 808 [arrowhead = none ];
808 -> 593;

809 [label="EVAL with clause\nzero(0).\nand substitutionT204 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
593 -> 809 [arrowhead = none ];
809 -> 594;

810 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
593 -> 810 [arrowhead = none ];
810 -> 595;

811 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
594 -> 811 [arrowhead = none ];
811 -> 596;

812 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
595 -> 812 [arrowhead = none ];
812 -> 599;

813 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
596 -> 813 [arrowhead = none ];
813 -> 597;

814 [label="BACKTRACK\nfor clause: failure(b)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
597 -> 814 [arrowhead = none ];
814 -> 598;

815 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
599 -> 815 [arrowhead = none ];
815 -> 600;

816 [label="ONLY EVAL with clause\nno(X313).\nand substitutionT204 -> T207,\nX313 -> zero(T207)", fontsize=14, style = filled, fillcolor = lightblue];
600 -> 816 [arrowhead = none ];
816 -> 601;

817 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
601 -> 817 [arrowhead = none ];
817 -> 602;

818 [label="ONLY EVAL with clause\nno(X316) :- ','(call(X316), ','(!_65, failure(a))).\nand substitutionT200 -> T210,\nX316 -> zero(T210)", fontsize=14, style = filled, fillcolor = lightblue];
602 -> 818 [arrowhead = none ];
818 -> 603;

819 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
603 -> 819 [arrowhead = none ];
819 -> 604;

820 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
604 -> 820 [arrowhead = none ];
820 -> 605;

821 [label="BACKTRACK\nfor clause: zero(0)\nwith clash: (div(T207, T210, T3, T4), div(X9, 0, X10, X11))", fontsize=14, style = filled, fillcolor = lightgreen];
605 -> 821 [arrowhead = none ];
821 -> 606;

822 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
606 -> 822 [arrowhead = none ];
822 -> 607;

823 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
607 -> 823 [arrowhead = none ];
823 -> 608;

824 [label="ONLY EVAL with clause\nno(X319).\nand substitutionT210 -> T213,\nX319 -> zero(T213)", fontsize=14, style = filled, fillcolor = lightblue];
608 -> 824 [arrowhead = none ];
824 -> 609;

825 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
609 -> 825 [arrowhead = none ];
825 -> 610;

}

(2) Obligation:

Pi-finite rewrite system:
The TRS R consists of the following rules:

divA_in_ggaa(0, T72, 0, 0) → divA_out_ggaa(0, T72, 0, 0)
divA_in_ggaa(T121, T135, s(T104), T105) → U1_ggaa(T121, T135, T104, T105, pB_in_ggaaa(T121, T135, X177, T104, T105))
pB_in_ggaaa(T121, T135, T144, T104, T105) → U5_ggaaa(T121, T135, T144, T104, T105, minusD_in_gga(T121, T135, T144))
minusD_in_gga(s(T154), s(T155), X255) → U3_gga(T154, T155, X255, minusC_in_gga(T154, T155, X255))
minusC_in_gga(T162, 0, T162) → minusC_out_gga(T162, 0, T162)
minusC_in_gga(s(T167), s(T168), X274) → U2_gga(T167, T168, X274, minusC_in_gga(T167, T168, X274))
U2_gga(T167, T168, X274, minusC_out_gga(T167, T168, X274)) → minusC_out_gga(s(T167), s(T168), X274)
U3_gga(T154, T155, X255, minusC_out_gga(T154, T155, X255)) → minusD_out_gga(s(T154), s(T155), X255)
U5_ggaaa(T121, T135, T144, T104, T105, minusD_out_gga(T121, T135, T144)) → U6_ggaaa(T121, T135, T144, T104, T105, pE_in_ggaa(T144, T135, T104, T105))
pE_in_ggaa(T144, T135, T104, T105) → U4_ggaa(T144, T135, T104, T105, divA_in_ggaa(T144, T135, T104, T105))
divA_in_ggaa(T189, T195, T183, T189) → divA_out_ggaa(T189, T195, T183, T189)
U4_ggaa(T144, T135, T104, T105, divA_out_ggaa(T144, T135, T104, T105)) → pE_out_ggaa(T144, T135, T104, T105)
U6_ggaaa(T121, T135, T144, T104, T105, pE_out_ggaa(T144, T135, T104, T105)) → pB_out_ggaaa(T121, T135, T144, T104, T105)
U1_ggaa(T121, T135, T104, T105, pB_out_ggaaa(T121, T135, X177, T104, T105)) → divA_out_ggaa(T121, T135, s(T104), T105)

(3) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

DIVA_IN_GGAA(T121, T135, s(T104), T105) → U1_GGAA(T121, T135, T104, T105, pB_in_ggaaa(T121, T135, X177, T104, T105))
DIVA_IN_GGAA(T121, T135, s(T104), T105) → PB_IN_GGAAA(T121, T135, X177, T104, T105)
PB_IN_GGAAA(T121, T135, T144, T104, T105) → U5_GGAAA(T121, T135, T144, T104, T105, minusD_in_gga(T121, T135, T144))
PB_IN_GGAAA(T121, T135, T144, T104, T105) → MINUSD_IN_GGA(T121, T135, T144)
MINUSD_IN_GGA(s(T154), s(T155), X255) → U3_GGA(T154, T155, X255, minusC_in_gga(T154, T155, X255))
MINUSD_IN_GGA(s(T154), s(T155), X255) → MINUSC_IN_GGA(T154, T155, X255)
MINUSC_IN_GGA(s(T167), s(T168), X274) → U2_GGA(T167, T168, X274, minusC_in_gga(T167, T168, X274))
MINUSC_IN_GGA(s(T167), s(T168), X274) → MINUSC_IN_GGA(T167, T168, X274)
U5_GGAAA(T121, T135, T144, T104, T105, minusD_out_gga(T121, T135, T144)) → U6_GGAAA(T121, T135, T144, T104, T105, pE_in_ggaa(T144, T135, T104, T105))
U5_GGAAA(T121, T135, T144, T104, T105, minusD_out_gga(T121, T135, T144)) → PE_IN_GGAA(T144, T135, T104, T105)
PE_IN_GGAA(T144, T135, T104, T105) → U4_GGAA(T144, T135, T104, T105, divA_in_ggaa(T144, T135, T104, T105))
PE_IN_GGAA(T144, T135, T104, T105) → DIVA_IN_GGAA(T144, T135, T104, T105)

The TRS R consists of the following rules:

divA_in_ggaa(0, T72, 0, 0) → divA_out_ggaa(0, T72, 0, 0)
divA_in_ggaa(T121, T135, s(T104), T105) → U1_ggaa(T121, T135, T104, T105, pB_in_ggaaa(T121, T135, X177, T104, T105))
pB_in_ggaaa(T121, T135, T144, T104, T105) → U5_ggaaa(T121, T135, T144, T104, T105, minusD_in_gga(T121, T135, T144))
minusD_in_gga(s(T154), s(T155), X255) → U3_gga(T154, T155, X255, minusC_in_gga(T154, T155, X255))
minusC_in_gga(T162, 0, T162) → minusC_out_gga(T162, 0, T162)
minusC_in_gga(s(T167), s(T168), X274) → U2_gga(T167, T168, X274, minusC_in_gga(T167, T168, X274))
U2_gga(T167, T168, X274, minusC_out_gga(T167, T168, X274)) → minusC_out_gga(s(T167), s(T168), X274)
U3_gga(T154, T155, X255, minusC_out_gga(T154, T155, X255)) → minusD_out_gga(s(T154), s(T155), X255)
U5_ggaaa(T121, T135, T144, T104, T105, minusD_out_gga(T121, T135, T144)) → U6_ggaaa(T121, T135, T144, T104, T105, pE_in_ggaa(T144, T135, T104, T105))
pE_in_ggaa(T144, T135, T104, T105) → U4_ggaa(T144, T135, T104, T105, divA_in_ggaa(T144, T135, T104, T105))
divA_in_ggaa(T189, T195, T183, T189) → divA_out_ggaa(T189, T195, T183, T189)
U4_ggaa(T144, T135, T104, T105, divA_out_ggaa(T144, T135, T104, T105)) → pE_out_ggaa(T144, T135, T104, T105)
U6_ggaaa(T121, T135, T144, T104, T105, pE_out_ggaa(T144, T135, T104, T105)) → pB_out_ggaaa(T121, T135, T144, T104, T105)
U1_ggaa(T121, T135, T104, T105, pB_out_ggaaa(T121, T135, X177, T104, T105)) → divA_out_ggaa(T121, T135, s(T104), T105)

The argument filtering Pi contains the following mapping:
divA_in_ggaa(x1, x2, x3, x4) = divA_in_ggaa(x1, x2)
0 = 0
divA_out_ggaa(x1, x2, x3, x4) = divA_out_ggaa(x1, x2, x4)
U1_ggaa(x1, x2, x3, x4, x5) = U1_ggaa(x1, x2, x5)
pB_in_ggaaa(x1, x2, x3, x4, x5) = pB_in_ggaaa(x1, x2)
U5_ggaaa(x1, x2, x3, x4, x5, x6) = U5_ggaaa(x1, x2, x6)
minusD_in_gga(x1, x2, x3) = minusD_in_gga(x1, x2)
s(x1) = s(x1)
U3_gga(x1, x2, x3, x4) = U3_gga(x1, x2, x4)
minusC_in_gga(x1, x2, x3) = minusC_in_gga(x1, x2)
minusC_out_gga(x1, x2, x3) = minusC_out_gga(x1, x2, x3)
U2_gga(x1, x2, x3, x4) = U2_gga(x1, x2, x4)
minusD_out_gga(x1, x2, x3) = minusD_out_gga(x1, x2, x3)
U6_ggaaa(x1, x2, x3, x4, x5, x6) = U6_ggaaa(x1, x2, x3, x6)
pE_in_ggaa(x1, x2, x3, x4) = pE_in_ggaa(x1, x2)
U4_ggaa(x1, x2, x3, x4, x5) = U4_ggaa(x1, x2, x5)
pE_out_ggaa(x1, x2, x3, x4) = pE_out_ggaa(x1, x2, x4)
pB_out_ggaaa(x1, x2, x3, x4, x5) = pB_out_ggaaa(x1, x2, x3, x5)
DIVA_IN_GGAA(x1, x2, x3, x4) = DIVA_IN_GGAA(x1, x2)
U1_GGAA(x1, x2, x3, x4, x5) = U1_GGAA(x1, x2, x5)
PB_IN_GGAAA(x1, x2, x3, x4, x5) = PB_IN_GGAAA(x1, x2)
U5_GGAAA(x1, x2, x3, x4, x5, x6) = U5_GGAAA(x1, x2, x6)
MINUSD_IN_GGA(x1, x2, x3) = MINUSD_IN_GGA(x1, x2)
U3_GGA(x1, x2, x3, x4) = U3_GGA(x1, x2, x4)
MINUSC_IN_GGA(x1, x2, x3) = MINUSC_IN_GGA(x1, x2)
U2_GGA(x1, x2, x3, x4) = U2_GGA(x1, x2, x4)
U6_GGAAA(x1, x2, x3, x4, x5, x6) = U6_GGAAA(x1, x2, x3, x6)
PE_IN_GGAA(x1, x2, x3, x4) = PE_IN_GGAA(x1, x2)
U4_GGAA(x1, x2, x3, x4, x5) = U4_GGAA(x1, x2, x5)

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

(4) Obligation:

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

DIVA_IN_GGAA(T121, T135, s(T104), T105) → U1_GGAA(T121, T135, T104, T105, pB_in_ggaaa(T121, T135, X177, T104, T105))
DIVA_IN_GGAA(T121, T135, s(T104), T105) → PB_IN_GGAAA(T121, T135, X177, T104, T105)
PB_IN_GGAAA(T121, T135, T144, T104, T105) → U5_GGAAA(T121, T135, T144, T104, T105, minusD_in_gga(T121, T135, T144))
PB_IN_GGAAA(T121, T135, T144, T104, T105) → MINUSD_IN_GGA(T121, T135, T144)
MINUSD_IN_GGA(s(T154), s(T155), X255) → U3_GGA(T154, T155, X255, minusC_in_gga(T154, T155, X255))
MINUSD_IN_GGA(s(T154), s(T155), X255) → MINUSC_IN_GGA(T154, T155, X255)
MINUSC_IN_GGA(s(T167), s(T168), X274) → U2_GGA(T167, T168, X274, minusC_in_gga(T167, T168, X274))
MINUSC_IN_GGA(s(T167), s(T168), X274) → MINUSC_IN_GGA(T167, T168, X274)
U5_GGAAA(T121, T135, T144, T104, T105, minusD_out_gga(T121, T135, T144)) → U6_GGAAA(T121, T135, T144, T104, T105, pE_in_ggaa(T144, T135, T104, T105))
U5_GGAAA(T121, T135, T144, T104, T105, minusD_out_gga(T121, T135, T144)) → PE_IN_GGAA(T144, T135, T104, T105)
PE_IN_GGAA(T144, T135, T104, T105) → U4_GGAA(T144, T135, T104, T105, divA_in_ggaa(T144, T135, T104, T105))
PE_IN_GGAA(T144, T135, T104, T105) → DIVA_IN_GGAA(T144, T135, T104, T105)

The TRS R consists of the following rules:

divA_in_ggaa(0, T72, 0, 0) → divA_out_ggaa(0, T72, 0, 0)
divA_in_ggaa(T121, T135, s(T104), T105) → U1_ggaa(T121, T135, T104, T105, pB_in_ggaaa(T121, T135, X177, T104, T105))
pB_in_ggaaa(T121, T135, T144, T104, T105) → U5_ggaaa(T121, T135, T144, T104, T105, minusD_in_gga(T121, T135, T144))
minusD_in_gga(s(T154), s(T155), X255) → U3_gga(T154, T155, X255, minusC_in_gga(T154, T155, X255))
minusC_in_gga(T162, 0, T162) → minusC_out_gga(T162, 0, T162)
minusC_in_gga(s(T167), s(T168), X274) → U2_gga(T167, T168, X274, minusC_in_gga(T167, T168, X274))
U2_gga(T167, T168, X274, minusC_out_gga(T167, T168, X274)) → minusC_out_gga(s(T167), s(T168), X274)
U3_gga(T154, T155, X255, minusC_out_gga(T154, T155, X255)) → minusD_out_gga(s(T154), s(T155), X255)
U5_ggaaa(T121, T135, T144, T104, T105, minusD_out_gga(T121, T135, T144)) → U6_ggaaa(T121, T135, T144, T104, T105, pE_in_ggaa(T144, T135, T104, T105))
pE_in_ggaa(T144, T135, T104, T105) → U4_ggaa(T144, T135, T104, T105, divA_in_ggaa(T144, T135, T104, T105))
divA_in_ggaa(T189, T195, T183, T189) → divA_out_ggaa(T189, T195, T183, T189)
U4_ggaa(T144, T135, T104, T105, divA_out_ggaa(T144, T135, T104, T105)) → pE_out_ggaa(T144, T135, T104, T105)
U6_ggaaa(T121, T135, T144, T104, T105, pE_out_ggaa(T144, T135, T104, T105)) → pB_out_ggaaa(T121, T135, T144, T104, T105)
U1_ggaa(T121, T135, T104, T105, pB_out_ggaaa(T121, T135, X177, T104, T105)) → divA_out_ggaa(T121, T135, s(T104), T105)

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 2 SCCs with 7 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

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

MINUSC_IN_GGA(s(T167), s(T168), X274) → MINUSC_IN_GGA(T167, T168, X274)

The TRS R consists of the following rules:

divA_in_ggaa(0, T72, 0, 0) → divA_out_ggaa(0, T72, 0, 0)
divA_in_ggaa(T121, T135, s(T104), T105) → U1_ggaa(T121, T135, T104, T105, pB_in_ggaaa(T121, T135, X177, T104, T105))
pB_in_ggaaa(T121, T135, T144, T104, T105) → U5_ggaaa(T121, T135, T144, T104, T105, minusD_in_gga(T121, T135, T144))
minusD_in_gga(s(T154), s(T155), X255) → U3_gga(T154, T155, X255, minusC_in_gga(T154, T155, X255))
minusC_in_gga(T162, 0, T162) → minusC_out_gga(T162, 0, T162)
minusC_in_gga(s(T167), s(T168), X274) → U2_gga(T167, T168, X274, minusC_in_gga(T167, T168, X274))
U2_gga(T167, T168, X274, minusC_out_gga(T167, T168, X274)) → minusC_out_gga(s(T167), s(T168), X274)
U3_gga(T154, T155, X255, minusC_out_gga(T154, T155, X255)) → minusD_out_gga(s(T154), s(T155), X255)
U5_ggaaa(T121, T135, T144, T104, T105, minusD_out_gga(T121, T135, T144)) → U6_ggaaa(T121, T135, T144, T104, T105, pE_in_ggaa(T144, T135, T104, T105))
pE_in_ggaa(T144, T135, T104, T105) → U4_ggaa(T144, T135, T104, T105, divA_in_ggaa(T144, T135, T104, T105))
divA_in_ggaa(T189, T195, T183, T189) → divA_out_ggaa(T189, T195, T183, T189)
U4_ggaa(T144, T135, T104, T105, divA_out_ggaa(T144, T135, T104, T105)) → pE_out_ggaa(T144, T135, T104, T105)
U6_ggaaa(T121, T135, T144, T104, T105, pE_out_ggaa(T144, T135, T104, T105)) → pB_out_ggaaa(T121, T135, T144, T104, T105)
U1_ggaa(T121, T135, T104, T105, pB_out_ggaaa(T121, T135, X177, T104, T105)) → divA_out_ggaa(T121, T135, s(T104), T105)

(8) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(9) Obligation:

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

MINUSC_IN_GGA(s(T167), s(T168), X274) → MINUSC_IN_GGA(T167, T168, X274)

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

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

(10) PiDPToQDPProof (SOUND transformation)

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

(11) Obligation:

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

MINUSC_IN_GGA(s(T167), s(T168)) → MINUSC_IN_GGA(T167, T168)

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

(12) 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:

MINUSC_IN_GGA(s(T167), s(T168)) → MINUSC_IN_GGA(T167, T168)
The graph contains the following edges 1 > 1, 2 > 2

(13) YES

(14) Obligation:

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

DIVA_IN_GGAA(T121, T135, s(T104), T105) → PB_IN_GGAAA(T121, T135, X177, T104, T105)
PB_IN_GGAAA(T121, T135, T144, T104, T105) → U5_GGAAA(T121, T135, T144, T104, T105, minusD_in_gga(T121, T135, T144))
U5_GGAAA(T121, T135, T144, T104, T105, minusD_out_gga(T121, T135, T144)) → PE_IN_GGAA(T144, T135, T104, T105)
PE_IN_GGAA(T144, T135, T104, T105) → DIVA_IN_GGAA(T144, T135, T104, T105)

The TRS R consists of the following rules:

divA_in_ggaa(0, T72, 0, 0) → divA_out_ggaa(0, T72, 0, 0)
divA_in_ggaa(T121, T135, s(T104), T105) → U1_ggaa(T121, T135, T104, T105, pB_in_ggaaa(T121, T135, X177, T104, T105))
pB_in_ggaaa(T121, T135, T144, T104, T105) → U5_ggaaa(T121, T135, T144, T104, T105, minusD_in_gga(T121, T135, T144))
minusD_in_gga(s(T154), s(T155), X255) → U3_gga(T154, T155, X255, minusC_in_gga(T154, T155, X255))
minusC_in_gga(T162, 0, T162) → minusC_out_gga(T162, 0, T162)
minusC_in_gga(s(T167), s(T168), X274) → U2_gga(T167, T168, X274, minusC_in_gga(T167, T168, X274))
U2_gga(T167, T168, X274, minusC_out_gga(T167, T168, X274)) → minusC_out_gga(s(T167), s(T168), X274)
U3_gga(T154, T155, X255, minusC_out_gga(T154, T155, X255)) → minusD_out_gga(s(T154), s(T155), X255)
U5_ggaaa(T121, T135, T144, T104, T105, minusD_out_gga(T121, T135, T144)) → U6_ggaaa(T121, T135, T144, T104, T105, pE_in_ggaa(T144, T135, T104, T105))
pE_in_ggaa(T144, T135, T104, T105) → U4_ggaa(T144, T135, T104, T105, divA_in_ggaa(T144, T135, T104, T105))
divA_in_ggaa(T189, T195, T183, T189) → divA_out_ggaa(T189, T195, T183, T189)
U4_ggaa(T144, T135, T104, T105, divA_out_ggaa(T144, T135, T104, T105)) → pE_out_ggaa(T144, T135, T104, T105)
U6_ggaaa(T121, T135, T144, T104, T105, pE_out_ggaa(T144, T135, T104, T105)) → pB_out_ggaaa(T121, T135, T144, T104, T105)
U1_ggaa(T121, T135, T104, T105, pB_out_ggaaa(T121, T135, X177, T104, T105)) → divA_out_ggaa(T121, T135, s(T104), T105)

The argument filtering Pi contains the following mapping:
divA_in_ggaa(x1, x2, x3, x4) = divA_in_ggaa(x1, x2)
0 = 0
divA_out_ggaa(x1, x2, x3, x4) = divA_out_ggaa(x1, x2, x4)
U1_ggaa(x1, x2, x3, x4, x5) = U1_ggaa(x1, x2, x5)
pB_in_ggaaa(x1, x2, x3, x4, x5) = pB_in_ggaaa(x1, x2)
U5_ggaaa(x1, x2, x3, x4, x5, x6) = U5_ggaaa(x1, x2, x6)
minusD_in_gga(x1, x2, x3) = minusD_in_gga(x1, x2)
s(x1) = s(x1)
U3_gga(x1, x2, x3, x4) = U3_gga(x1, x2, x4)
minusC_in_gga(x1, x2, x3) = minusC_in_gga(x1, x2)
minusC_out_gga(x1, x2, x3) = minusC_out_gga(x1, x2, x3)
U2_gga(x1, x2, x3, x4) = U2_gga(x1, x2, x4)
minusD_out_gga(x1, x2, x3) = minusD_out_gga(x1, x2, x3)
U6_ggaaa(x1, x2, x3, x4, x5, x6) = U6_ggaaa(x1, x2, x3, x6)
pE_in_ggaa(x1, x2, x3, x4) = pE_in_ggaa(x1, x2)
U4_ggaa(x1, x2, x3, x4, x5) = U4_ggaa(x1, x2, x5)
pE_out_ggaa(x1, x2, x3, x4) = pE_out_ggaa(x1, x2, x4)
pB_out_ggaaa(x1, x2, x3, x4, x5) = pB_out_ggaaa(x1, x2, x3, x5)
DIVA_IN_GGAA(x1, x2, x3, x4) = DIVA_IN_GGAA(x1, x2)
PB_IN_GGAAA(x1, x2, x3, x4, x5) = PB_IN_GGAAA(x1, x2)
U5_GGAAA(x1, x2, x3, x4, x5, x6) = U5_GGAAA(x1, x2, x6)
PE_IN_GGAA(x1, x2, x3, x4) = PE_IN_GGAA(x1, x2)

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

(15) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(16) Obligation:

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

DIVA_IN_GGAA(T121, T135, s(T104), T105) → PB_IN_GGAAA(T121, T135, X177, T104, T105)
PB_IN_GGAAA(T121, T135, T144, T104, T105) → U5_GGAAA(T121, T135, T144, T104, T105, minusD_in_gga(T121, T135, T144))
U5_GGAAA(T121, T135, T144, T104, T105, minusD_out_gga(T121, T135, T144)) → PE_IN_GGAA(T144, T135, T104, T105)
PE_IN_GGAA(T144, T135, T104, T105) → DIVA_IN_GGAA(T144, T135, T104, T105)

The TRS R consists of the following rules:

minusD_in_gga(s(T154), s(T155), X255) → U3_gga(T154, T155, X255, minusC_in_gga(T154, T155, X255))
U3_gga(T154, T155, X255, minusC_out_gga(T154, T155, X255)) → minusD_out_gga(s(T154), s(T155), X255)
minusC_in_gga(T162, 0, T162) → minusC_out_gga(T162, 0, T162)
minusC_in_gga(s(T167), s(T168), X274) → U2_gga(T167, T168, X274, minusC_in_gga(T167, T168, X274))
U2_gga(T167, T168, X274, minusC_out_gga(T167, T168, X274)) → minusC_out_gga(s(T167), s(T168), X274)

The argument filtering Pi contains the following mapping:
0 = 0
minusD_in_gga(x1, x2, x3) = minusD_in_gga(x1, x2)
s(x1) = s(x1)
U3_gga(x1, x2, x3, x4) = U3_gga(x1, x2, x4)
minusC_in_gga(x1, x2, x3) = minusC_in_gga(x1, x2)
minusC_out_gga(x1, x2, x3) = minusC_out_gga(x1, x2, x3)
U2_gga(x1, x2, x3, x4) = U2_gga(x1, x2, x4)
minusD_out_gga(x1, x2, x3) = minusD_out_gga(x1, x2, x3)
DIVA_IN_GGAA(x1, x2, x3, x4) = DIVA_IN_GGAA(x1, x2)
PB_IN_GGAAA(x1, x2, x3, x4, x5) = PB_IN_GGAAA(x1, x2)
U5_GGAAA(x1, x2, x3, x4, x5, x6) = U5_GGAAA(x1, x2, x6)
PE_IN_GGAA(x1, x2, x3, x4) = PE_IN_GGAA(x1, x2)

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

(17) PiDPToQDPProof (SOUND transformation)

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

(18) Obligation:

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

DIVA_IN_GGAA(T121, T135) → PB_IN_GGAAA(T121, T135)
PB_IN_GGAAA(T121, T135) → U5_GGAAA(T121, T135, minusD_in_gga(T121, T135))
U5_GGAAA(T121, T135, minusD_out_gga(T121, T135, T144)) → PE_IN_GGAA(T144, T135)
PE_IN_GGAA(T144, T135) → DIVA_IN_GGAA(T144, T135)

The TRS R consists of the following rules:

minusD_in_gga(s(T154), s(T155)) → U3_gga(T154, T155, minusC_in_gga(T154, T155))
U3_gga(T154, T155, minusC_out_gga(T154, T155, X255)) → minusD_out_gga(s(T154), s(T155), X255)
minusC_in_gga(T162, 0) → minusC_out_gga(T162, 0, T162)
minusC_in_gga(s(T167), s(T168)) → U2_gga(T167, T168, minusC_in_gga(T167, T168))
U2_gga(T167, T168, minusC_out_gga(T167, T168, X274)) → minusC_out_gga(s(T167), s(T168), X274)

The set Q consists of the following terms:

minusD_in_gga(x0, x1)
U3_gga(x0, x1, x2)
minusC_in_gga(x0, x1)
U2_gga(x0, x1, x2)

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

(19) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].

The following pairs can be oriented strictly and are deleted.

PB_IN_GGAAA(T121, T135) → U5_GGAAA(T121, T135, minusD_in_gga(T121, T135))

The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(0) = 0
POL(DIVA_IN_GGAA(x₁, x₂)) = 1 + x₁
POL(PB_IN_GGAAA(x₁, x₂)) = 1 + x₁
POL(PE_IN_GGAA(x₁, x₂)) = 1 + x₁
POL(U2_gga(x₁, x₂, x₃)) = x₃
POL(U3_gga(x₁, x₂, x₃)) = 1 + x₃
POL(U5_GGAAA(x₁, x₂, x₃)) = x₃
POL(minusC_in_gga(x₁, x₂)) = x₁
POL(minusC_out_gga(x₁, x₂, x₃)) = x₃
POL(minusD_in_gga(x₁, x₂)) = x₁
POL(minusD_out_gga(x₁, x₂, x₃)) = 1 + x₃
POL(s(x₁)) = 1 + x₁

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

minusD_in_gga(s(T154), s(T155)) → U3_gga(T154, T155, minusC_in_gga(T154, T155))
minusC_in_gga(T162, 0) → minusC_out_gga(T162, 0, T162)
minusC_in_gga(s(T167), s(T168)) → U2_gga(T167, T168, minusC_in_gga(T167, T168))
U3_gga(T154, T155, minusC_out_gga(T154, T155, X255)) → minusD_out_gga(s(T154), s(T155), X255)
U2_gga(T167, T168, minusC_out_gga(T167, T168, X274)) → minusC_out_gga(s(T167), s(T168), X274)

(20) Obligation:

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

DIVA_IN_GGAA(T121, T135) → PB_IN_GGAAA(T121, T135)
U5_GGAAA(T121, T135, minusD_out_gga(T121, T135, T144)) → PE_IN_GGAA(T144, T135)
PE_IN_GGAA(T144, T135) → DIVA_IN_GGAA(T144, T135)

The TRS R consists of the following rules:

minusD_in_gga(s(T154), s(T155)) → U3_gga(T154, T155, minusC_in_gga(T154, T155))
U3_gga(T154, T155, minusC_out_gga(T154, T155, X255)) → minusD_out_gga(s(T154), s(T155), X255)
minusC_in_gga(T162, 0) → minusC_out_gga(T162, 0, T162)
minusC_in_gga(s(T167), s(T168)) → U2_gga(T167, T168, minusC_in_gga(T167, T168))
U2_gga(T167, T168, minusC_out_gga(T167, T168, X274)) → minusC_out_gga(s(T167), s(T168), X274)

The set Q consists of the following terms:

minusD_in_gga(x0, x1)
U3_gga(x0, x1, x2)
minusC_in_gga(x0, x1)
U2_gga(x0, x1, x2)

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

(21) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 3 less nodes.

(0) Obligation:

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

(2) Obligation:

(3) DependencyPairsProof (EQUIVALENT transformation)

(4) Obligation:

(5) DependencyGraphProof (EQUIVALENT transformation)

(6) Complex Obligation (AND)

(7) Obligation:

(8) UsableRulesProof (EQUIVALENT transformation)

(9) Obligation:

(10) PiDPToQDPProof (SOUND transformation)

(11) Obligation:

(12) QDPSizeChangeProof (EQUIVALENT transformation)

(13) YES

(14) Obligation:

(15) UsableRulesProof (EQUIVALENT transformation)

(16) Obligation:

(17) PiDPToQDPProof (SOUND transformation)

(18) Obligation:

(19) QDPOrderProof (EQUIVALENT transformation)

(20) Obligation:

(21) DependencyGraphProof (EQUIVALENT transformation)

(22) TRUE