Left Termination proof of /tmp/tmprz2ZaB/delete-bbf.pl

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

0 Prolog

↳1 PrologToDTProblemTransformerProof (⇐)

↳2 TRIPLES

↳3 TriplesToPiDPProof (⇐)

↳4 PiDP

↳5 DependencyGraphProof (⇔)

↳6 AND

    ↳7 PiDP

        ↳8 UsableRulesProof (⇔)

        ↳9 PiDP

        ↳10 PiDPToQDPProof (⇔)

        ↳11 QDP

        ↳12 QDPSizeChangeProof (⇔)

        ↳13 YES

    ↳14 PiDP

        ↳15 UsableRulesProof (⇔)

        ↳16 PiDP

        ↳17 PiDPToQDPProof (⇐)

        ↳18 QDP

        ↳19 QDPSizeChangeProof (⇔)

        ↳20 YES

    ↳21 PiDP

        ↳22 UsableRulesProof (⇔)

        ↳23 PiDP

        ↳24 PiDPToQDPProof (⇔)

        ↳25 QDP

        ↳26 QDPSizeChangeProof (⇔)

        ↳27 YES

    ↳28 PiDP

        ↳29 PiDPToQDPProof (⇐)

        ↳30 QDP

        ↳31 QDPSizeChangeProof (⇔)

        ↳32 YES

(0) Obligation:

Clauses:

delete(X, tree(X, void, Right), Right).
delete(X, tree(X, Left, void), Left).
delete(X, tree(X, Left, Right), tree(Y, Left, Right1)) :- delmin(Right, Y, Right1).
delete(X, tree(Y, Left, Right), tree(Y, Left1, Right)) :- ','(less(X, Y), delete(X, Left, Left1)).
delete(X, tree(Y, Left, Right), tree(Y, Left, Right1)) :- ','(less(Y, X), delete(X, Right, Right1)).
delmin(tree(Y, void, Right), Y, Right).
delmin(tree(X, Left, X1), Y, tree(X, Left1, X2)) :- delmin(Left, Y, Left1).
less(0, s(X3)).
less(s(X), s(Y)) :- less(X, Y).

Queries:

delete(g,g,a).

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="1: delete(T1, T2, T3)\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
2 [label="2: delete(T1, T2, T3), SCOPE: 1, CLAUSE: 0 | delete(T1, T2, T3), SCOPE: 1, CLAUSE: 1 | delete(T1, T2, T3), SCOPE: 1, CLAUSE: 2 | delete(T1, T2, T3), SCOPE: 1, CLAUSE: 3 | delete(T1, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
3 [label="3: true | delete(T6, tree(T6, void, T7), T3), SCOPE: 1, CLAUSE: 1 | delete(T6, tree(T6, void, T7), T3), SCOPE: 1, CLAUSE: 2 | delete(T6, tree(T6, void, T7), T3), SCOPE: 1, CLAUSE: 3 | delete(T6, tree(T6, void, T7), T3), SCOPE: 1, CLAUSE: 4\n\nT6 is ground\nT7 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
4 [label="4: delete(T1, T2, T3), SCOPE: 1, CLAUSE: 1 | delete(T1, T2, T3), SCOPE: 1, CLAUSE: 2 | delete(T1, T2, T3), SCOPE: 1, CLAUSE: 3 | delete(T1, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT1 is ground\nT2 is ground\ndelete(T1, T2, T3) !=? delete(X6, tree(X6, void, X7), X7)", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: delete(T6, tree(T6, void, T7), T3), SCOPE: 1, CLAUSE: 1 | delete(T6, tree(T6, void, T7), T3), SCOPE: 1, CLAUSE: 2 | delete(T6, tree(T6, void, T7), T3), SCOPE: 1, CLAUSE: 3 | delete(T6, tree(T6, void, T7), T3), SCOPE: 1, CLAUSE: 4\n\nT6 is ground\nT7 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: true | delete(T9, tree(T9, void, void), T3), SCOPE: 1, CLAUSE: 2 | delete(T9, tree(T9, void, void), T3), SCOPE: 1, CLAUSE: 3 | delete(T9, tree(T9, void, void), T3), SCOPE: 1, CLAUSE: 4\n\nT9 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: delete(T6, tree(T6, void, T7), T3), SCOPE: 1, CLAUSE: 2 | delete(T6, tree(T6, void, T7), T3), SCOPE: 1, CLAUSE: 3 | delete(T6, tree(T6, void, T7), T3), SCOPE: 1, CLAUSE: 4\n\nT6 is ground\nT7 is ground\ndelete(T6, tree(T6, void, T7), T3) !=? delete(X12, tree(X12, X13, void), X13)", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: delete(T9, tree(T9, void, void), T3), SCOPE: 1, CLAUSE: 2 | delete(T9, tree(T9, void, void), T3), SCOPE: 1, CLAUSE: 3 | delete(T9, tree(T9, void, void), T3), SCOPE: 1, CLAUSE: 4\n\nT9 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: delmin(void, T16, T17) | delete(T13, tree(T13, void, void), T3), SCOPE: 1, CLAUSE: 3 | delete(T13, tree(T13, void, void), T3), SCOPE: 1, CLAUSE: 4\n\nT13 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: delete(T9, tree(T9, void, void), T3), SCOPE: 1, CLAUSE: 3 | delete(T9, tree(T9, void, void), T3), SCOPE: 1, CLAUSE: 4\n\nT9 is ground\ndelete(T9, tree(T9, void, void), T3) !=? delete(X21, tree(X21, X22, X23), tree(X24, X22, X25))", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: delmin(void, T16, T17), SCOPE: 2, CLAUSE: 5 | delmin(void, T16, T17), SCOPE: 2, CLAUSE: 6 | ?_2 | delete(T13, tree(T13, void, void), T3), SCOPE: 1, CLAUSE: 3 | delete(T13, tree(T13, void, void), T3), SCOPE: 1, CLAUSE: 4\n\nT13 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: delmin(void, T16, T17), SCOPE: 2, CLAUSE: 6 | ?_2 | delete(T13, tree(T13, void, void), T3), SCOPE: 1, CLAUSE: 3 | delete(T13, tree(T13, void, void), T3), SCOPE: 1, CLAUSE: 4\n\nT13 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: ?_2 | delete(T13, tree(T13, void, void), T3), SCOPE: 1, CLAUSE: 3 | delete(T13, tree(T13, void, void), T3), SCOPE: 1, CLAUSE: 4\n\nT13 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: delete(T13, tree(T13, void, void), T3), SCOPE: 1, CLAUSE: 3 | delete(T13, tree(T13, void, void), T3), SCOPE: 1, CLAUSE: 4\n\nT13 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: delete(T13, tree(T13, void, void), T3), SCOPE: 1, CLAUSE: 3\n\nT13 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: delete(T13, tree(T13, void, void), T3), SCOPE: 1, CLAUSE: 4\n\nT13 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: ','(less(T26, T26), delete(T26, void, T28))\n\nT26 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: less(T26, T26)\n\nT26 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: delete(T26, void, T28)\n\nT26 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: less(T26, T26), SCOPE: 3, CLAUSE: 7 | less(T26, T26), SCOPE: 3, CLAUSE: 8\n\nT26 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: less(T26, T26), SCOPE: 3, CLAUSE: 8\n\nT26 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: less(T33, T33)\n\nT33 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: ','(less(T46, T46), delete(T46, void, T48))\n\nT46 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: ','(less(T52, T52), delete(T52, void, T54)) | delete(T52, tree(T52, void, void), T3), SCOPE: 1, CLAUSE: 4\n\nT52 is ground\ndelete(T52, tree(T52, void, void), T3) !=? delete(X21, tree(X21, X22, X23), tree(X24, X22, X25))", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: delete(T9, tree(T9, void, void), T3), SCOPE: 1, CLAUSE: 4\n\nT9 is ground\ndelete(T9, tree(T9, void, void), T3) !=? delete(X21, tree(X21, X22, X23), tree(X24, X22, X25))\ndelete(T9, tree(T9, void, void), T3) !=? delete(X142, tree(X143, X144, X145), tree(X143, X146, X145))", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: ','(less(T52, T52), delete(T52, void, T54)), SCOPE: 4, CLAUSE: 7 | ','(less(T52, T52), delete(T52, void, T54)), SCOPE: 4, CLAUSE: 8 | ?_4 | delete(T52, tree(T52, void, void), T3), SCOPE: 1, CLAUSE: 4\n\nT52 is ground\ndelete(T52, tree(T52, void, void), T3) !=? delete(X21, tree(X21, X22, X23), tree(X24, X22, X25))", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: ','(less(T52, T52), delete(T52, void, T54)), SCOPE: 4, CLAUSE: 8 | ?_4 | delete(T52, tree(T52, void, void), T3), SCOPE: 1, CLAUSE: 4\n\nT52 is ground\ndelete(T52, tree(T52, void, void), T3) !=? delete(X21, tree(X21, X22, X23), tree(X24, X22, X25))", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: ','(less(T52, T52), delete(T52, void, T54)), SCOPE: 4, CLAUSE: 8\n\nT52 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: ?_4 | delete(T52, tree(T52, void, void), T3), SCOPE: 1, CLAUSE: 4\n\nT52 is ground\ndelete(T52, tree(T52, void, void), T3) !=? delete(X21, tree(X21, X22, X23), tree(X24, X22, X25))", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: ','(less(T59, T59), delete(s(T59), void, T54))\n\nT59 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: less(T59, T59)\n\nT59 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: delete(s(T59), void, T54)\n\nT59 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: delete(T52, tree(T52, void, void), T3), SCOPE: 1, CLAUSE: 4\n\nT52 is ground\ndelete(T52, tree(T52, void, void), T3) !=? delete(X21, tree(X21, X22, X23), tree(X24, X22, X25))", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: ','(less(T73, T73), delete(T73, void, T75))\n\nT73 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: ','(less(T79, T79), delete(T79, void, T81))\n\nT79 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: ','(less(T79, T79), delete(T79, void, T81)), SCOPE: 5, CLAUSE: 7 | ','(less(T79, T79), delete(T79, void, T81)), SCOPE: 5, CLAUSE: 8\n\nT79 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: ','(less(T79, T79), delete(T79, void, T81)), SCOPE: 5, CLAUSE: 8\n\nT79 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: ','(less(T84, T84), delete(s(T84), void, T81))\n\nT84 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: delmin(T91, T94, T95) | delete(T90, tree(T90, void, T91), T3), SCOPE: 1, CLAUSE: 3 | delete(T90, tree(T90, void, T91), T3), SCOPE: 1, CLAUSE: 4\n\nT90 is ground\nT91 is ground\ndelete(T90, tree(T90, void, T91), T3) !=? delete(X12, tree(X12, X13, void), X13)", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: delete(T6, tree(T6, void, T7), T3), SCOPE: 1, CLAUSE: 3 | delete(T6, tree(T6, void, T7), T3), SCOPE: 1, CLAUSE: 4\n\nT6 is ground\nT7 is ground\ndelete(T6, tree(T6, void, T7), T3) !=? delete(X12, tree(X12, X13, void), X13)\ndelete(T6, tree(T6, void, T7), T3) !=? delete(X253, tree(X253, X254, X255), tree(X256, X254, X257))", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: delmin(T91, T94, T95), SCOPE: 6, CLAUSE: 5 | delmin(T91, T94, T95), SCOPE: 6, CLAUSE: 6 | ?_6 | delete(T90, tree(T90, void, T91), T3), SCOPE: 1, CLAUSE: 3 | delete(T90, tree(T90, void, T91), T3), SCOPE: 1, CLAUSE: 4\n\nT90 is ground\nT91 is ground\ndelete(T90, tree(T90, void, T91), T3) !=? delete(X12, tree(X12, X13, void), X13)", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: delmin(T91, T94, T95), SCOPE: 6, CLAUSE: 5\n\nT91 is ground\ndelete(T90, tree(T90, void, T91), T3) !=? delete(X12, tree(X12, X13, void), X13)", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: delmin(T91, T94, T95), SCOPE: 6, CLAUSE: 6 | ?_6 | delete(T90, tree(T90, void, T91), T3), SCOPE: 1, CLAUSE: 3 | delete(T90, tree(T90, void, T91), T3), SCOPE: 1, CLAUSE: 4\n\nT90 is ground\nT91 is ground\ndelete(T90, tree(T90, void, T91), T3) !=? delete(X12, tree(X12, X13, void), X13)", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: delmin(T91, T94, T95), SCOPE: 6, CLAUSE: 6\n\nT91 is ground\ndelete(T90, tree(T90, void, T91), T3) !=? delete(X12, tree(X12, X13, void), X13)", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: ?_6 | delete(T90, tree(T90, void, T91), T3), SCOPE: 1, CLAUSE: 3 | delete(T90, tree(T90, void, T91), T3), SCOPE: 1, CLAUSE: 4\n\nT90 is ground\nT91 is ground\ndelete(T90, tree(T90, void, T91), T3) !=? delete(X12, tree(X12, X13, void), X13)", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: delmin(T131, T136, T137)\n\nT131 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: delmin(T131, T136, T137), SCOPE: 7, CLAUSE: 5 | delmin(T131, T136, T137), SCOPE: 7, CLAUSE: 6\n\nT131 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: delmin(T131, T136, T137), SCOPE: 7, CLAUSE: 5\n\nT131 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: delmin(T131, T136, T137), SCOPE: 7, CLAUSE: 6\n\nT131 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: delmin(T165, T170, T171)\n\nT165 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: delete(T90, tree(T90, void, T91), T3), SCOPE: 1, CLAUSE: 3 | delete(T90, tree(T90, void, T91), T3), SCOPE: 1, CLAUSE: 4\n\nT90 is ground\nT91 is ground\ndelete(T90, tree(T90, void, T91), T3) !=? delete(X12, tree(X12, X13, void), X13)", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: delete(T90, tree(T90, void, T91), T3), SCOPE: 1, CLAUSE: 3\n\nT90 is ground\nT91 is ground\ndelete(T90, tree(T90, void, T91), T3) !=? delete(X12, tree(X12, X13, void), X13)", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: delete(T90, tree(T90, void, T91), T3), SCOPE: 1, CLAUSE: 4\n\nT90 is ground\nT91 is ground\ndelete(T90, tree(T90, void, T91), T3) !=? delete(X12, tree(X12, X13, void), X13)", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: ','(less(T188, T188), delete(T188, void, T191))\n\nT188 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: ','(less(T199, T199), delete(T199, T200, T202))\n\nT199 is ground\nT200 is ground\ndelete(T199, tree(T199, void, T200), T3) !=? delete(X12, tree(X12, X13, void), X13)", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: less(T199, T199)\n\nT199 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: delete(T199, T200, T202)\n\nT199 is ground\nT200 is ground\ndelete(T199, tree(T199, void, T200), T3) !=? delete(X12, tree(X12, X13, void), X13)", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: ','(less(T212, T212), delete(T212, void, T215)) | delete(T212, tree(T212, void, T213), T3), SCOPE: 1, CLAUSE: 4\n\nT212 is ground\nT213 is ground\ndelete(T212, tree(T212, void, T213), T3) !=? delete(X12, tree(X12, X13, void), X13)\ndelete(T212, tree(T212, void, T213), T3) !=? delete(X253, tree(X253, X254, X255), tree(X256, X254, X257))", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: delete(T6, tree(T6, void, T7), T3), SCOPE: 1, CLAUSE: 4\n\nT6 is ground\nT7 is ground\ndelete(T6, tree(T6, void, T7), T3) !=? delete(X12, tree(X12, X13, void), X13)\ndelete(T6, tree(T6, void, T7), T3) !=? delete(X253, tree(X253, X254, X255), tree(X256, X254, X257))\ndelete(T6, tree(T6, void, T7), T3) !=? delete(X426, tree(X427, X428, X429), tree(X427, X430, X429))", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: ','(less(T212, T212), delete(T212, void, T215)), SCOPE: 8, CLAUSE: 7 | ','(less(T212, T212), delete(T212, void, T215)), SCOPE: 8, CLAUSE: 8 | ?_8 | delete(T212, tree(T212, void, T213), T3), SCOPE: 1, CLAUSE: 4\n\nT212 is ground\nT213 is ground\ndelete(T212, tree(T212, void, T213), T3) !=? delete(X12, tree(X12, X13, void), X13)\ndelete(T212, tree(T212, void, T213), T3) !=? delete(X253, tree(X253, X254, X255), tree(X256, X254, X257))", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: ','(less(T212, T212), delete(T212, void, T215)), SCOPE: 8, CLAUSE: 8 | ?_8 | delete(T212, tree(T212, void, T213), T3), SCOPE: 1, CLAUSE: 4\n\nT212 is ground\nT213 is ground\ndelete(T212, tree(T212, void, T213), T3) !=? delete(X12, tree(X12, X13, void), X13)\ndelete(T212, tree(T212, void, T213), T3) !=? delete(X253, tree(X253, X254, X255), tree(X256, X254, X257))", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: ','(less(T212, T212), delete(T212, void, T215)), SCOPE: 8, CLAUSE: 8\n\nT212 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: ?_8 | delete(T212, tree(T212, void, T213), T3), SCOPE: 1, CLAUSE: 4\n\nT212 is ground\nT213 is ground\ndelete(T212, tree(T212, void, T213), T3) !=? delete(X12, tree(X12, X13, void), X13)\ndelete(T212, tree(T212, void, T213), T3) !=? delete(X253, tree(X253, X254, X255), tree(X256, X254, X257))", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: ','(less(T220, T220), delete(s(T220), void, T215))\n\nT220 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: delete(T212, tree(T212, void, T213), T3), SCOPE: 1, CLAUSE: 4\n\nT212 is ground\nT213 is ground\ndelete(T212, tree(T212, void, T213), T3) !=? delete(X12, tree(X12, X13, void), X13)\ndelete(T212, tree(T212, void, T213), T3) !=? delete(X253, tree(X253, X254, X255), tree(X256, X254, X257))", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: ','(less(T228, T228), delete(T228, T229, T231))\n\nT228 is ground\nT229 is ground\ndelete(T228, tree(T228, void, T229), T3) !=? delete(X12, tree(X12, X13, void), X13)", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: ','(less(T236, T236), delete(T236, T237, T239))\n\nT236 is ground\nT237 is ground\ndelete(T236, tree(T236, void, T237), T3) !=? delete(X12, tree(X12, X13, void), X13)", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: ','(less(T236, T236), delete(T236, T237, T239)), SCOPE: 9, CLAUSE: 7 | ','(less(T236, T236), delete(T236, T237, T239)), SCOPE: 9, CLAUSE: 8\n\nT236 is ground\nT237 is ground\ndelete(T236, tree(T236, void, T237), T3) !=? delete(X12, tree(X12, X13, void), X13)", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: ','(less(T236, T236), delete(T236, T237, T239)), SCOPE: 9, CLAUSE: 8\n\nT236 is ground\nT237 is ground\ndelete(T236, tree(T236, void, T237), T3) !=? delete(X12, tree(X12, X13, void), X13)", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: ','(less(T242, T242), delete(s(T242), T237, T239))\n\nT237 is ground\nT242 is ground\ndelete(s(T242), tree(s(T242), void, T237), T3) !=? delete(X12, tree(X12, X13, void), X13)", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: less(T242, T242)\n\nT242 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: delete(s(T242), T237, T239)\n\nT237 is ground\nT242 is ground\ndelete(s(T242), tree(s(T242), void, T237), T3) !=? delete(X12, tree(X12, X13, void), X13)", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: true | delete(T251, tree(T251, T252, void), T3), SCOPE: 1, CLAUSE: 2 | delete(T251, tree(T251, T252, void), T3), SCOPE: 1, CLAUSE: 3 | delete(T251, tree(T251, T252, void), T3), SCOPE: 1, CLAUSE: 4\n\nT251 is ground\nT252 is ground\ndelete(T251, tree(T251, T252, void), T3) !=? delete(X6, tree(X6, void, X7), X7)", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: delete(T1, T2, T3), SCOPE: 1, CLAUSE: 2 | delete(T1, T2, T3), SCOPE: 1, CLAUSE: 3 | delete(T1, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT1 is ground\nT2 is ground\ndelete(T1, T2, T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T1, T2, T3) !=? delete(X515, tree(X515, X516, void), X516)", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: delete(T251, tree(T251, T252, void), T3), SCOPE: 1, CLAUSE: 2 | delete(T251, tree(T251, T252, void), T3), SCOPE: 1, CLAUSE: 3 | delete(T251, tree(T251, T252, void), T3), SCOPE: 1, CLAUSE: 4\n\nT251 is ground\nT252 is ground\ndelete(T251, tree(T251, T252, void), T3) !=? delete(X6, tree(X6, void, X7), X7)", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: delmin(void, T261, T262) | delete(T257, tree(T257, T258, void), T3), SCOPE: 1, CLAUSE: 3 | delete(T257, tree(T257, T258, void), T3), SCOPE: 1, CLAUSE: 4\n\nT257 is ground\nT258 is ground\ndelete(T257, tree(T257, T258, void), T3) !=? delete(X6, tree(X6, void, X7), X7)", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: delete(T251, tree(T251, T252, void), T3), SCOPE: 1, CLAUSE: 3 | delete(T251, tree(T251, T252, void), T3), SCOPE: 1, CLAUSE: 4\n\nT251 is ground\nT252 is ground\ndelete(T251, tree(T251, T252, void), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T251, tree(T251, T252, void), T3) !=? delete(X524, tree(X524, X525, X526), tree(X527, X525, X528))", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: delmin(void, T261, T262), SCOPE: 10, CLAUSE: 5 | delmin(void, T261, T262), SCOPE: 10, CLAUSE: 6 | ?_10 | delete(T257, tree(T257, T258, void), T3), SCOPE: 1, CLAUSE: 3 | delete(T257, tree(T257, T258, void), T3), SCOPE: 1, CLAUSE: 4\n\nT257 is ground\nT258 is ground\ndelete(T257, tree(T257, T258, void), T3) !=? delete(X6, tree(X6, void, X7), X7)", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="100: delmin(void, T261, T262), SCOPE: 10, CLAUSE: 6 | ?_10 | delete(T257, tree(T257, T258, void), T3), SCOPE: 1, CLAUSE: 3 | delete(T257, tree(T257, T258, void), T3), SCOPE: 1, CLAUSE: 4\n\nT257 is ground\nT258 is ground\ndelete(T257, tree(T257, T258, void), T3) !=? delete(X6, tree(X6, void, X7), X7)", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="101: ?_10 | delete(T257, tree(T257, T258, void), T3), SCOPE: 1, CLAUSE: 3 | delete(T257, tree(T257, T258, void), T3), SCOPE: 1, CLAUSE: 4\n\nT257 is ground\nT258 is ground\ndelete(T257, tree(T257, T258, void), T3) !=? delete(X6, tree(X6, void, X7), X7)", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="102: delete(T257, tree(T257, T258, void), T3), SCOPE: 1, CLAUSE: 3 | delete(T257, tree(T257, T258, void), T3), SCOPE: 1, CLAUSE: 4\n\nT257 is ground\nT258 is ground\ndelete(T257, tree(T257, T258, void), T3) !=? delete(X6, tree(X6, void, X7), X7)", fontsize=16, style=filled, fillcolor=lightyellow];
103 [label="103: delete(T257, tree(T257, T258, void), T3), SCOPE: 1, CLAUSE: 3\n\nT257 is ground\nT258 is ground\ndelete(T257, tree(T257, T258, void), T3) !=? delete(X6, tree(X6, void, X7), X7)", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: delete(T257, tree(T257, T258, void), T3), SCOPE: 1, CLAUSE: 4\n\nT257 is ground\nT258 is ground\ndelete(T257, tree(T257, T258, void), T3) !=? delete(X6, tree(X6, void, X7), X7)", fontsize=16, style=filled, fillcolor=lightyellow];
105 [label="105: ','(less(T275, T275), delete(T275, T276, T278))\n\nT275 is ground\nT276 is ground\ndelete(T275, tree(T275, T276, void), T3) !=? delete(X6, tree(X6, void, X7), X7)", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="106: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: less(T275, T275)\n\nT275 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="108: delete(T275, T276, T278)\n\nT275 is ground\nT276 is ground\ndelete(T275, tree(T275, T276, void), T3) !=? delete(X6, tree(X6, void, X7), X7)", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="109: ','(less(T291, T291), delete(T291, void, T294))\n\nT291 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: ','(less(T299, T299), delete(T299, T300, T302)) | delete(T299, tree(T299, T300, void), T3), SCOPE: 1, CLAUSE: 4\n\nT299 is ground\nT300 is ground\ndelete(T299, tree(T299, T300, void), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T299, tree(T299, T300, void), T3) !=? delete(X524, tree(X524, X525, X526), tree(X527, X525, X528))", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: delete(T251, tree(T251, T252, void), T3), SCOPE: 1, CLAUSE: 4\n\nT251 is ground\nT252 is ground\ndelete(T251, tree(T251, T252, void), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T251, tree(T251, T252, void), T3) !=? delete(X524, tree(X524, X525, X526), tree(X527, X525, X528))\ndelete(T251, tree(T251, T252, void), T3) !=? delete(X613, tree(X614, X615, X616), tree(X614, X617, X616))", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: ','(less(T299, T299), delete(T299, T300, T302)), SCOPE: 11, CLAUSE: 7 | ','(less(T299, T299), delete(T299, T300, T302)), SCOPE: 11, CLAUSE: 8 | ?_11 | delete(T299, tree(T299, T300, void), T3), SCOPE: 1, CLAUSE: 4\n\nT299 is ground\nT300 is ground\ndelete(T299, tree(T299, T300, void), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T299, tree(T299, T300, void), T3) !=? delete(X524, tree(X524, X525, X526), tree(X527, X525, X528))", fontsize=16, style=filled, fillcolor=lightyellow];
114 [label="114: ','(less(T299, T299), delete(T299, T300, T302)), SCOPE: 11, CLAUSE: 8 | ?_11 | delete(T299, tree(T299, T300, void), T3), SCOPE: 1, CLAUSE: 4\n\nT299 is ground\nT300 is ground\ndelete(T299, tree(T299, T300, void), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T299, tree(T299, T300, void), T3) !=? delete(X524, tree(X524, X525, X526), tree(X527, X525, X528))", fontsize=16, style=filled, fillcolor=lightyellow];
115 [label="115: ','(less(T299, T299), delete(T299, T300, T302)), SCOPE: 11, CLAUSE: 8\n\nT299 is ground\nT300 is ground\ndelete(T299, tree(T299, T300, void), T3) !=? delete(X6, tree(X6, void, X7), X7)", fontsize=16, style=filled, fillcolor=lightyellow];
116 [label="116: ?_11 | delete(T299, tree(T299, T300, void), T3), SCOPE: 1, CLAUSE: 4\n\nT299 is ground\nT300 is ground\ndelete(T299, tree(T299, T300, void), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T299, tree(T299, T300, void), T3) !=? delete(X524, tree(X524, X525, X526), tree(X527, X525, X528))", fontsize=16, style=filled, fillcolor=lightyellow];
117 [label="117: ','(less(T307, T307), delete(s(T307), T300, T302))\n\nT300 is ground\nT307 is ground\ndelete(s(T307), tree(s(T307), T300, void), T3) !=? delete(X6, tree(X6, void, X7), X7)", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="118: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
119 [label="119: less(T307, T307)\n\nT307 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
120 [label="120: delete(s(T307), T300, T302)\n\nT300 is ground\nT307 is ground\ndelete(s(T307), tree(s(T307), T300, void), T3) !=? delete(X6, tree(X6, void, X7), X7)", fontsize=16, style=filled, fillcolor=lightyellow];
121 [label="121: delete(T299, tree(T299, T300, void), T3), SCOPE: 1, CLAUSE: 4\n\nT299 is ground\nT300 is ground\ndelete(T299, tree(T299, T300, void), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T299, tree(T299, T300, void), T3) !=? delete(X524, tree(X524, X525, X526), tree(X527, X525, X528))", fontsize=16, style=filled, fillcolor=lightyellow];
122 [label="122: ','(less(T320, T320), delete(T320, void, T323))\n\nT320 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
123 [label="123: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
124 [label="124: ','(less(T328, T328), delete(T328, void, T331))\n\nT328 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
125 [label="125: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
126 [label="126: ','(less(T328, T328), delete(T328, void, T331)), SCOPE: 12, CLAUSE: 7 | ','(less(T328, T328), delete(T328, void, T331)), SCOPE: 12, CLAUSE: 8\n\nT328 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
127 [label="127: ','(less(T328, T328), delete(T328, void, T331)), SCOPE: 12, CLAUSE: 8\n\nT328 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
128 [label="128: ','(less(T334, T334), delete(s(T334), void, T331))\n\nT334 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
129 [label="129: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
130 [label="130: delmin(T343, T346, T347) | delete(T341, tree(T341, T342, T343), T3), SCOPE: 1, CLAUSE: 3 | delete(T341, tree(T341, T342, T343), T3), SCOPE: 1, CLAUSE: 4\n\nT341 is ground\nT342 is ground\nT343 is ground\ndelete(T341, tree(T341, T342, T343), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T341, tree(T341, T342, T343), T3) !=? delete(X515, tree(X515, X516, void), X516)", fontsize=16, style=filled, fillcolor=lightyellow];
131 [label="131: delete(T1, T2, T3), SCOPE: 1, CLAUSE: 3 | delete(T1, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT1 is ground\nT2 is ground\ndelete(T1, T2, T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T1, T2, T3) !=? delete(X515, tree(X515, X516, void), X516)\ndelete(T1, T2, T3) !=? delete(X705, tree(X705, X706, X707), tree(X708, X706, X709))", fontsize=16, style=filled, fillcolor=lightyellow];
132 [label="132: delmin(T343, T346, T347), SCOPE: 13, CLAUSE: 5 | delmin(T343, T346, T347), SCOPE: 13, CLAUSE: 6 | ?_13 | delete(T341, tree(T341, T342, T343), T3), SCOPE: 1, CLAUSE: 3 | delete(T341, tree(T341, T342, T343), T3), SCOPE: 1, CLAUSE: 4\n\nT341 is ground\nT342 is ground\nT343 is ground\ndelete(T341, tree(T341, T342, T343), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T341, tree(T341, T342, T343), T3) !=? delete(X515, tree(X515, X516, void), X516)", fontsize=16, style=filled, fillcolor=lightyellow];
133 [label="133: delmin(T343, T346, T347), SCOPE: 13, CLAUSE: 5\n\nT343 is ground\ndelete(T341, tree(T341, T342, T343), T3) !=? delete(X515, tree(X515, X516, void), X516)", fontsize=16, style=filled, fillcolor=lightyellow];
134 [label="134: delmin(T343, T346, T347), SCOPE: 13, CLAUSE: 6 | ?_13 | delete(T341, tree(T341, T342, T343), T3), SCOPE: 1, CLAUSE: 3 | delete(T341, tree(T341, T342, T343), T3), SCOPE: 1, CLAUSE: 4\n\nT341 is ground\nT342 is ground\nT343 is ground\ndelete(T341, tree(T341, T342, T343), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T341, tree(T341, T342, T343), T3) !=? delete(X515, tree(X515, X516, void), X516)", fontsize=16, style=filled, fillcolor=lightyellow];
135 [label="135: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
136 [label="136: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
137 [label="137: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
138 [label="138: delmin(T343, T346, T347), SCOPE: 13, CLAUSE: 6\n\nT343 is ground\ndelete(T341, tree(T341, T342, T343), T3) !=? delete(X515, tree(X515, X516, void), X516)", fontsize=16, style=filled, fillcolor=lightyellow];
139 [label="139: ?_13 | delete(T341, tree(T341, T342, T343), T3), SCOPE: 1, CLAUSE: 3 | delete(T341, tree(T341, T342, T343), T3), SCOPE: 1, CLAUSE: 4\n\nT341 is ground\nT342 is ground\nT343 is ground\ndelete(T341, tree(T341, T342, T343), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T341, tree(T341, T342, T343), T3) !=? delete(X515, tree(X515, X516, void), X516)", fontsize=16, style=filled, fillcolor=lightyellow];
140 [label="140: delmin(T383, T388, T389)\n\nT383 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
141 [label="141: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
142 [label="142: delete(T341, tree(T341, T342, T343), T3), SCOPE: 1, CLAUSE: 3 | delete(T341, tree(T341, T342, T343), T3), SCOPE: 1, CLAUSE: 4\n\nT341 is ground\nT342 is ground\nT343 is ground\ndelete(T341, tree(T341, T342, T343), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T341, tree(T341, T342, T343), T3) !=? delete(X515, tree(X515, X516, void), X516)", fontsize=16, style=filled, fillcolor=lightyellow];
143 [label="143: delete(T341, tree(T341, T342, T343), T3), SCOPE: 1, CLAUSE: 3\n\nT341 is ground\nT342 is ground\nT343 is ground\ndelete(T341, tree(T341, T342, T343), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T341, tree(T341, T342, T343), T3) !=? delete(X515, tree(X515, X516, void), X516)", fontsize=16, style=filled, fillcolor=lightyellow];
144 [label="144: delete(T341, tree(T341, T342, T343), T3), SCOPE: 1, CLAUSE: 4\n\nT341 is ground\nT342 is ground\nT343 is ground\ndelete(T341, tree(T341, T342, T343), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T341, tree(T341, T342, T343), T3) !=? delete(X515, tree(X515, X516, void), X516)", fontsize=16, style=filled, fillcolor=lightyellow];
145 [label="145: ','(less(T410, T410), delete(T410, T411, T414))\n\nT410 is ground\nT411 is ground\ndelete(T410, tree(T410, T411, T412), T3) !=? delete(X6, tree(X6, void, X7), X7)", fontsize=16, style=filled, fillcolor=lightyellow];
146 [label="146: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
147 [label="147: less(T410, T410)\n\nT410 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
148 [label="148: delete(T410, T411, T414)\n\nT410 is ground\nT411 is ground\ndelete(T410, tree(T410, T411, T412), T3) !=? delete(X6, tree(X6, void, X7), X7)", fontsize=16, style=filled, fillcolor=lightyellow];
149 [label="149: ','(less(T429, T429), delete(T429, T431, T433))\n\nT429 is ground\nT431 is ground\ndelete(T429, tree(T429, T430, T431), T3) !=? delete(X515, tree(X515, X516, void), X516)", fontsize=16, style=filled, fillcolor=lightyellow];
150 [label="150: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
151 [label="151: less(T429, T429)\n\nT429 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
152 [label="152: delete(T429, T431, T433)\n\nT429 is ground\nT431 is ground\ndelete(T429, tree(T429, T430, T431), T3) !=? delete(X515, tree(X515, X516, void), X516)", fontsize=16, style=filled, fillcolor=lightyellow];
153 [label="153: ','(less(T445, T446), delete(T445, T447, T450)) | delete(T445, tree(T446, T447, T448), T3), SCOPE: 1, CLAUSE: 4\n\nT445 is ground\nT446 is ground\nT447 is ground\nT448 is ground\ndelete(T445, tree(T446, T447, T448), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T445, tree(T446, T447, T448), T3) !=? delete(X515, tree(X515, X516, void), X516)\ndelete(T445, tree(T446, T447, T448), T3) !=? delete(X705, tree(X705, X706, X707), tree(X708, X706, X709))", fontsize=16, style=filled, fillcolor=lightyellow];
154 [label="154: delete(T1, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT1 is ground\nT2 is ground\ndelete(T1, T2, T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T1, T2, T3) !=? delete(X515, tree(X515, X516, void), X516)\ndelete(T1, T2, T3) !=? delete(X705, tree(X705, X706, X707), tree(X708, X706, X709))\ndelete(T1, T2, T3) !=? delete(X846, tree(X847, X848, X849), tree(X847, X850, X849))", fontsize=16, style=filled, fillcolor=lightyellow];
155 [label="155: ','(less(T445, T446), delete(T445, T447, T450)), SCOPE: 14, CLAUSE: 7 | ','(less(T445, T446), delete(T445, T447, T450)), SCOPE: 14, CLAUSE: 8 | ?_14 | delete(T445, tree(T446, T447, T448), T3), SCOPE: 1, CLAUSE: 4\n\nT445 is ground\nT446 is ground\nT447 is ground\nT448 is ground\ndelete(T445, tree(T446, T447, T448), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T445, tree(T446, T447, T448), T3) !=? delete(X515, tree(X515, X516, void), X516)\ndelete(T445, tree(T446, T447, T448), T3) !=? delete(X705, tree(X705, X706, X707), tree(X708, X706, X709))", fontsize=16, style=filled, fillcolor=lightyellow];
156 [label="156: ','(less(T445, T446), delete(T445, T447, T450)), SCOPE: 14, CLAUSE: 7\n\nT445 is ground\nT446 is ground\nT447 is ground\ndelete(T445, tree(T446, T447, T448), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T445, tree(T446, T447, T448), T3) !=? delete(X515, tree(X515, X516, void), X516)\ndelete(T445, tree(T446, T447, T448), T3) !=? delete(X705, tree(X705, X706, X707), tree(X708, X706, X709))", fontsize=16, style=filled, fillcolor=lightyellow];
157 [label="157: ','(less(T445, T446), delete(T445, T447, T450)), SCOPE: 14, CLAUSE: 8 | ?_14 | delete(T445, tree(T446, T447, T448), T3), SCOPE: 1, CLAUSE: 4\n\nT445 is ground\nT446 is ground\nT447 is ground\nT448 is ground\ndelete(T445, tree(T446, T447, T448), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T445, tree(T446, T447, T448), T3) !=? delete(X515, tree(X515, X516, void), X516)\ndelete(T445, tree(T446, T447, T448), T3) !=? delete(X705, tree(X705, X706, X707), tree(X708, X706, X709))", fontsize=16, style=filled, fillcolor=lightyellow];
158 [label="158: delete(0, T447, T450)\n\nT447 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
159 [label="159: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
160 [label="160: ','(less(T445, T446), delete(T445, T447, T450)), SCOPE: 14, CLAUSE: 8\n\nT445 is ground\nT446 is ground\nT447 is ground\ndelete(T445, tree(T446, T447, T448), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T445, tree(T446, T447, T448), T3) !=? delete(X515, tree(X515, X516, void), X516)\ndelete(T445, tree(T446, T447, T448), T3) !=? delete(X705, tree(X705, X706, X707), tree(X708, X706, X709))", fontsize=16, style=filled, fillcolor=lightyellow];
161 [label="161: ?_14 | delete(T445, tree(T446, T447, T448), T3), SCOPE: 1, CLAUSE: 4\n\nT445 is ground\nT446 is ground\nT447 is ground\nT448 is ground\ndelete(T445, tree(T446, T447, T448), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T445, tree(T446, T447, T448), T3) !=? delete(X515, tree(X515, X516, void), X516)\ndelete(T445, tree(T446, T447, T448), T3) !=? delete(X705, tree(X705, X706, X707), tree(X708, X706, X709))", fontsize=16, style=filled, fillcolor=lightyellow];
162 [label="162: ','(less(T466, T467), delete(s(T466), T447, T450))\n\nT447 is ground\nT466 is ground\nT467 is ground\ndelete(s(T466), tree(s(T467), T447, T448), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(s(T466), tree(s(T467), T447, T448), T3) !=? delete(X515, tree(X515, X516, void), X516)\ndelete(s(T466), tree(s(T467), T447, T448), T3) !=? delete(X705, tree(X705, X706, X707), tree(X708, X706, X709))", fontsize=16, style=filled, fillcolor=lightyellow];
163 [label="163: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
164 [label="164: less(T466, T467)\n\nT466 is ground\nT467 is ground\ndelete(s(T466), tree(s(T467), T447, T448), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(s(T466), tree(s(T467), T447, T448), T3) !=? delete(X515, tree(X515, X516, void), X516)\ndelete(s(T466), tree(s(T467), T447, T448), T3) !=? delete(X705, tree(X705, X706, X707), tree(X708, X706, X709))", fontsize=16, style=filled, fillcolor=lightyellow];
165 [label="165: delete(s(T466), T447, T450)\n\nT447 is ground\nT466 is ground\ndelete(s(T466), tree(s(T467), T447, T448), T3) !=? delete(X6, tree(X6, void, X7), X7)", fontsize=16, style=filled, fillcolor=lightyellow];
166 [label="166: less(T466, T467), SCOPE: 15, CLAUSE: 7 | less(T466, T467), SCOPE: 15, CLAUSE: 8\n\nT466 is ground\nT467 is ground\ndelete(s(T466), tree(s(T467), T447, T448), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(s(T466), tree(s(T467), T447, T448), T3) !=? delete(X515, tree(X515, X516, void), X516)\ndelete(s(T466), tree(s(T467), T447, T448), T3) !=? delete(X705, tree(X705, X706, X707), tree(X708, X706, X709))", fontsize=16, style=filled, fillcolor=lightyellow];
167 [label="167: less(T466, T467), SCOPE: 15, CLAUSE: 7\n\nT466 is ground\nT467 is ground\ndelete(s(T466), tree(s(T467), T447, T448), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(s(T466), tree(s(T467), T447, T448), T3) !=? delete(X515, tree(X515, X516, void), X516)\ndelete(s(T466), tree(s(T467), T447, T448), T3) !=? delete(X705, tree(X705, X706, X707), tree(X708, X706, X709))", fontsize=16, style=filled, fillcolor=lightyellow];
168 [label="168: less(T466, T467), SCOPE: 15, CLAUSE: 8\n\nT466 is ground\nT467 is ground\ndelete(s(T466), tree(s(T467), T447, T448), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(s(T466), tree(s(T467), T447, T448), T3) !=? delete(X515, tree(X515, X516, void), X516)\ndelete(s(T466), tree(s(T467), T447, T448), T3) !=? delete(X705, tree(X705, X706, X707), tree(X708, X706, X709))", fontsize=16, style=filled, fillcolor=lightyellow];
169 [label="169: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
170 [label="170: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
171 [label="171: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
172 [label="172: less(T481, T482)\n\nT481 is ground\nT482 is ground\ndelete(s(s(T481)), tree(s(s(T482)), T447, T448), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(s(s(T481)), tree(s(s(T482)), T447, T448), T3) !=? delete(X515, tree(X515, X516, void), X516)\ndelete(s(s(T481)), tree(s(s(T482)), T447, T448), T3) !=? delete(X705, tree(X705, X706, X707), tree(X708, X706, X709))", fontsize=16, style=filled, fillcolor=lightyellow];
173 [label="173: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
174 [label="174: less(T481, T482), SCOPE: 16, CLAUSE: 7 | less(T481, T482), SCOPE: 16, CLAUSE: 8\n\nT481 is ground\nT482 is ground\ndelete(s(s(T481)), tree(s(s(T482)), T447, T448), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(s(s(T481)), tree(s(s(T482)), T447, T448), T3) !=? delete(X515, tree(X515, X516, void), X516)\ndelete(s(s(T481)), tree(s(s(T482)), T447, T448), T3) !=? delete(X705, tree(X705, X706, X707), tree(X708, X706, X709))", fontsize=16, style=filled, fillcolor=lightyellow];
175 [label="175: less(T481, T482), SCOPE: 16, CLAUSE: 7\n\nT481 is ground\nT482 is ground\ndelete(s(s(T481)), tree(s(s(T482)), T447, T448), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(s(s(T481)), tree(s(s(T482)), T447, T448), T3) !=? delete(X515, tree(X515, X516, void), X516)\ndelete(s(s(T481)), tree(s(s(T482)), T447, T448), T3) !=? delete(X705, tree(X705, X706, X707), tree(X708, X706, X709))", fontsize=16, style=filled, fillcolor=lightyellow];
176 [label="176: less(T481, T482), SCOPE: 16, CLAUSE: 8\n\nT481 is ground\nT482 is ground\ndelete(s(s(T481)), tree(s(s(T482)), T447, T448), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(s(s(T481)), tree(s(s(T482)), T447, T448), T3) !=? delete(X515, tree(X515, X516, void), X516)\ndelete(s(s(T481)), tree(s(s(T482)), T447, T448), T3) !=? delete(X705, tree(X705, X706, X707), tree(X708, X706, X709))", fontsize=16, style=filled, fillcolor=lightyellow];
177 [label="177: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
178 [label="178: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
179 [label="179: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
180 [label="180: less(T494, T495)\n\nT494 is ground\nT495 is ground\ndelete(s(s(s(T494))), tree(s(s(s(T495))), T447, T448), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(s(s(s(T494))), tree(s(s(s(T495))), T447, T448), T3) !=? delete(X515, tree(X515, X516, void), X516)\ndelete(s(s(s(T494))), tree(s(s(s(T495))), T447, T448), T3) !=? delete(X705, tree(X705, X706, X707), tree(X708, X706, X709))", fontsize=16, style=filled, fillcolor=lightyellow];
181 [label="181: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
182 [label="182: less(T494, T495), SCOPE: 17, CLAUSE: 7 | less(T494, T495), SCOPE: 17, CLAUSE: 8\n\nT494 is ground\nT495 is ground\ndelete(s(s(s(T494))), tree(s(s(s(T495))), T447, T448), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(s(s(s(T494))), tree(s(s(s(T495))), T447, T448), T3) !=? delete(X515, tree(X515, X516, void), X516)\ndelete(s(s(s(T494))), tree(s(s(s(T495))), T447, T448), T3) !=? delete(X705, tree(X705, X706, X707), tree(X708, X706, X709))", fontsize=16, style=filled, fillcolor=lightyellow];
183 [label="183: less(T494, T495), SCOPE: 17, CLAUSE: 7\n\nT494 is ground\nT495 is ground\ndelete(s(s(s(T494))), tree(s(s(s(T495))), T447, T448), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(s(s(s(T494))), tree(s(s(s(T495))), T447, T448), T3) !=? delete(X515, tree(X515, X516, void), X516)\ndelete(s(s(s(T494))), tree(s(s(s(T495))), T447, T448), T3) !=? delete(X705, tree(X705, X706, X707), tree(X708, X706, X709))", fontsize=16, style=filled, fillcolor=lightyellow];
184 [label="184: less(T494, T495), SCOPE: 17, CLAUSE: 8\n\nT494 is ground\nT495 is ground\ndelete(s(s(s(T494))), tree(s(s(s(T495))), T447, T448), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(s(s(s(T494))), tree(s(s(s(T495))), T447, T448), T3) !=? delete(X515, tree(X515, X516, void), X516)\ndelete(s(s(s(T494))), tree(s(s(s(T495))), T447, T448), T3) !=? delete(X705, tree(X705, X706, X707), tree(X708, X706, X709))", fontsize=16, style=filled, fillcolor=lightyellow];
185 [label="185: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
186 [label="186: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
187 [label="187: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
188 [label="188: less(T507, T508)\n\nT507 is ground\nT508 is ground\ndelete(s(s(s(s(T507)))), tree(s(s(s(s(T508)))), T447, T448), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(s(s(s(s(T507)))), tree(s(s(s(s(T508)))), T447, T448), T3) !=? delete(X515, tree(X515, X516, void), X516)\ndelete(s(s(s(s(T507)))), tree(s(s(s(s(T508)))), T447, T448), T3) !=? delete(X705, tree(X705, X706, X707), tree(X708, X706, X709))", fontsize=16, style=filled, fillcolor=lightyellow];
189 [label="189: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
190 [label="190: less(T507, T508), SCOPE: 18, CLAUSE: 7 | less(T507, T508), SCOPE: 18, CLAUSE: 8\n\nT507 is ground\nT508 is ground\ndelete(s(s(s(s(T507)))), tree(s(s(s(s(T508)))), T447, T448), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(s(s(s(s(T507)))), tree(s(s(s(s(T508)))), T447, T448), T3) !=? delete(X515, tree(X515, X516, void), X516)\ndelete(s(s(s(s(T507)))), tree(s(s(s(s(T508)))), T447, T448), T3) !=? delete(X705, tree(X705, X706, X707), tree(X708, X706, X709))", fontsize=16, style=filled, fillcolor=lightyellow];
191 [label="191: less(T507, T508), SCOPE: 18, CLAUSE: 7\n\nT507 is ground\nT508 is ground\ndelete(s(s(s(s(T507)))), tree(s(s(s(s(T508)))), T447, T448), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(s(s(s(s(T507)))), tree(s(s(s(s(T508)))), T447, T448), T3) !=? delete(X515, tree(X515, X516, void), X516)\ndelete(s(s(s(s(T507)))), tree(s(s(s(s(T508)))), T447, T448), T3) !=? delete(X705, tree(X705, X706, X707), tree(X708, X706, X709))", fontsize=16, style=filled, fillcolor=lightyellow];
192 [label="192: less(T507, T508), SCOPE: 18, CLAUSE: 8\n\nT507 is ground\nT508 is ground\ndelete(s(s(s(s(T507)))), tree(s(s(s(s(T508)))), T447, T448), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(s(s(s(s(T507)))), tree(s(s(s(s(T508)))), T447, T448), T3) !=? delete(X515, tree(X515, X516, void), X516)\ndelete(s(s(s(s(T507)))), tree(s(s(s(s(T508)))), T447, T448), T3) !=? delete(X705, tree(X705, X706, X707), tree(X708, X706, X709))", fontsize=16, style=filled, fillcolor=lightyellow];
193 [label="193: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
194 [label="194: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
195 [label="195: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
196 [label="196: less(T520, T521)\n\nT520 is ground\nT521 is ground\ndelete(s(s(s(s(s(T520))))), tree(s(s(s(s(s(T521))))), T447, T448), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(s(s(s(s(s(T520))))), tree(s(s(s(s(s(T521))))), T447, T448), T3) !=? delete(X515, tree(X515, X516, void), X516)\ndelete(s(s(s(s(s(T520))))), tree(s(s(s(s(s(T521))))), T447, T448), T3) !=? delete(X705, tree(X705, X706, X707), tree(X708, X706, X709))", fontsize=16, style=filled, fillcolor=lightyellow];
197 [label="197: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
198 [label="198: less(T520, T521), SCOPE: 19, CLAUSE: 7 | less(T520, T521), SCOPE: 19, CLAUSE: 8\n\nT520 is ground\nT521 is ground\ndelete(s(s(s(s(s(T520))))), tree(s(s(s(s(s(T521))))), T447, T448), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(s(s(s(s(s(T520))))), tree(s(s(s(s(s(T521))))), T447, T448), T3) !=? delete(X515, tree(X515, X516, void), X516)\ndelete(s(s(s(s(s(T520))))), tree(s(s(s(s(s(T521))))), T447, T448), T3) !=? delete(X705, tree(X705, X706, X707), tree(X708, X706, X709))", fontsize=16, style=filled, fillcolor=lightyellow];
199 [label="199: less(T520, T521), SCOPE: 19, CLAUSE: 7\n\nT520 is ground\nT521 is ground\ndelete(s(s(s(s(s(T520))))), tree(s(s(s(s(s(T521))))), T447, T448), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(s(s(s(s(s(T520))))), tree(s(s(s(s(s(T521))))), T447, T448), T3) !=? delete(X515, tree(X515, X516, void), X516)\ndelete(s(s(s(s(s(T520))))), tree(s(s(s(s(s(T521))))), T447, T448), T3) !=? delete(X705, tree(X705, X706, X707), tree(X708, X706, X709))", fontsize=16, style=filled, fillcolor=lightyellow];
200 [label="200: less(T520, T521), SCOPE: 19, CLAUSE: 8\n\nT520 is ground\nT521 is ground\ndelete(s(s(s(s(s(T520))))), tree(s(s(s(s(s(T521))))), T447, T448), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(s(s(s(s(s(T520))))), tree(s(s(s(s(s(T521))))), T447, T448), T3) !=? delete(X515, tree(X515, X516, void), X516)\ndelete(s(s(s(s(s(T520))))), tree(s(s(s(s(s(T521))))), T447, T448), T3) !=? delete(X705, tree(X705, X706, X707), tree(X708, X706, X709))", fontsize=16, style=filled, fillcolor=lightyellow];
201 [label="201: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
202 [label="202: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
203 [label="203: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
204 [label="204: less(T533, T534)\n\nT533 is ground\nT534 is ground\ndelete(s(s(s(s(s(s(T533)))))), tree(s(s(s(s(s(s(T534)))))), T447, T448), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(s(s(s(s(s(s(T533)))))), tree(s(s(s(s(s(s(T534)))))), T447, T448), T3) !=? delete(X515, tree(X515, X516, void), X516)\ndelete(s(s(s(s(s(s(T533)))))), tree(s(s(s(s(s(s(T534)))))), T447, T448), T3) !=? delete(X705, tree(X705, X706, X707), tree(X708, X706, X709))", fontsize=16, style=filled, fillcolor=lightyellow];
205 [label="205: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
206 [label="206: less(T533, T534), SCOPE: 20, CLAUSE: 7 | less(T533, T534), SCOPE: 20, CLAUSE: 8\n\nT533 is ground\nT534 is ground\ndelete(s(s(s(s(s(s(T533)))))), tree(s(s(s(s(s(s(T534)))))), T447, T448), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(s(s(s(s(s(s(T533)))))), tree(s(s(s(s(s(s(T534)))))), T447, T448), T3) !=? delete(X515, tree(X515, X516, void), X516)\ndelete(s(s(s(s(s(s(T533)))))), tree(s(s(s(s(s(s(T534)))))), T447, T448), T3) !=? delete(X705, tree(X705, X706, X707), tree(X708, X706, X709))", fontsize=16, style=filled, fillcolor=lightyellow];
207 [label="207: less(T533, T534), SCOPE: 20, CLAUSE: 7\n\nT533 is ground\nT534 is ground\ndelete(s(s(s(s(s(s(T533)))))), tree(s(s(s(s(s(s(T534)))))), T447, T448), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(s(s(s(s(s(s(T533)))))), tree(s(s(s(s(s(s(T534)))))), T447, T448), T3) !=? delete(X515, tree(X515, X516, void), X516)\ndelete(s(s(s(s(s(s(T533)))))), tree(s(s(s(s(s(s(T534)))))), T447, T448), T3) !=? delete(X705, tree(X705, X706, X707), tree(X708, X706, X709))", fontsize=16, style=filled, fillcolor=lightyellow];
208 [label="208: less(T533, T534), SCOPE: 20, CLAUSE: 8\n\nT533 is ground\nT534 is ground\ndelete(s(s(s(s(s(s(T533)))))), tree(s(s(s(s(s(s(T534)))))), T447, T448), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(s(s(s(s(s(s(T533)))))), tree(s(s(s(s(s(s(T534)))))), T447, T448), T3) !=? delete(X515, tree(X515, X516, void), X516)\ndelete(s(s(s(s(s(s(T533)))))), tree(s(s(s(s(s(s(T534)))))), T447, T448), T3) !=? delete(X705, tree(X705, X706, X707), tree(X708, X706, X709))", fontsize=16, style=filled, fillcolor=lightyellow];
209 [label="209: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
210 [label="210: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
211 [label="211: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
212 [label="212: less(T546, T547)\n\nT546 is ground\nT547 is ground\ndelete(s(s(s(s(s(s(s(T546))))))), tree(s(s(s(s(s(s(s(T547))))))), T447, T448), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(s(s(s(s(s(s(s(T546))))))), tree(s(s(s(s(s(s(s(T547))))))), T447, T448), T3) !=? delete(X515, tree(X515, X516, void), X516)\ndelete(s(s(s(s(s(s(s(T546))))))), tree(s(s(s(s(s(s(s(T547))))))), T447, T448), T3) !=? delete(X705, tree(X705, X706, X707), tree(X708, X706, X709))", fontsize=16, style=filled, fillcolor=lightyellow];
213 [label="213: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
214 [label="214: less(T546, T547), SCOPE: 21, CLAUSE: 7 | less(T546, T547), SCOPE: 21, CLAUSE: 8\n\nT546 is ground\nT547 is ground\ndelete(s(s(s(s(s(s(s(T546))))))), tree(s(s(s(s(s(s(s(T547))))))), T447, T448), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(s(s(s(s(s(s(s(T546))))))), tree(s(s(s(s(s(s(s(T547))))))), T447, T448), T3) !=? delete(X515, tree(X515, X516, void), X516)\ndelete(s(s(s(s(s(s(s(T546))))))), tree(s(s(s(s(s(s(s(T547))))))), T447, T448), T3) !=? delete(X705, tree(X705, X706, X707), tree(X708, X706, X709))", fontsize=16, style=filled, fillcolor=lightyellow];
215 [label="215: less(T546, T547), SCOPE: 21, CLAUSE: 7\n\nT546 is ground\nT547 is ground\ndelete(s(s(s(s(s(s(s(T546))))))), tree(s(s(s(s(s(s(s(T547))))))), T447, T448), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(s(s(s(s(s(s(s(T546))))))), tree(s(s(s(s(s(s(s(T547))))))), T447, T448), T3) !=? delete(X515, tree(X515, X516, void), X516)\ndelete(s(s(s(s(s(s(s(T546))))))), tree(s(s(s(s(s(s(s(T547))))))), T447, T448), T3) !=? delete(X705, tree(X705, X706, X707), tree(X708, X706, X709))", fontsize=16, style=filled, fillcolor=lightyellow];
216 [label="216: less(T546, T547), SCOPE: 21, CLAUSE: 8\n\nT546 is ground\nT547 is ground\ndelete(s(s(s(s(s(s(s(T546))))))), tree(s(s(s(s(s(s(s(T547))))))), T447, T448), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(s(s(s(s(s(s(s(T546))))))), tree(s(s(s(s(s(s(s(T547))))))), T447, T448), T3) !=? delete(X515, tree(X515, X516, void), X516)\ndelete(s(s(s(s(s(s(s(T546))))))), tree(s(s(s(s(s(s(s(T547))))))), T447, T448), T3) !=? delete(X705, tree(X705, X706, X707), tree(X708, X706, X709))", fontsize=16, style=filled, fillcolor=lightyellow];
217 [label="217: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
218 [label="218: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
219 [label="219: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
220 [label="220: less(T559, T560)\n\nT559 is ground\nT560 is ground\ndelete(s(s(s(s(s(s(s(s(T559)))))))), tree(s(s(s(s(s(s(s(s(T560)))))))), T447, T448), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(s(s(s(s(s(s(s(s(T559)))))))), tree(s(s(s(s(s(s(s(s(T560)))))))), T447, T448), T3) !=? delete(X515, tree(X515, X516, void), X516)\ndelete(s(s(s(s(s(s(s(s(T559)))))))), tree(s(s(s(s(s(s(s(s(T560)))))))), T447, T448), T3) !=? delete(X705, tree(X705, X706, X707), tree(X708, X706, X709))", fontsize=16, style=filled, fillcolor=lightyellow];
221 [label="221: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
222 [label="222: less(T559, T560)\n\nT559 is ground\nT560 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
223 [label="223: less(T559, T560), SCOPE: 22, CLAUSE: 7 | less(T559, T560), SCOPE: 22, CLAUSE: 8\n\nT559 is ground\nT560 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
224 [label="224: less(T559, T560), SCOPE: 22, CLAUSE: 7\n\nT559 is ground\nT560 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
225 [label="225: less(T559, T560), SCOPE: 22, CLAUSE: 8\n\nT559 is ground\nT560 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
226 [label="226: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
227 [label="227: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
228 [label="228: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
229 [label="229: less(T576, T577)\n\nT576 is ground\nT577 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
230 [label="230: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
231 [label="231: delete(T445, tree(T446, T447, T448), T3), SCOPE: 1, CLAUSE: 4\n\nT445 is ground\nT446 is ground\nT447 is ground\nT448 is ground\ndelete(T445, tree(T446, T447, T448), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T445, tree(T446, T447, T448), T3) !=? delete(X515, tree(X515, X516, void), X516)\ndelete(T445, tree(T446, T447, T448), T3) !=? delete(X705, tree(X705, X706, X707), tree(X708, X706, X709))", fontsize=16, style=filled, fillcolor=lightyellow];
232 [label="232: ','(less(T595, T594), delete(T594, T597, T599))\n\nT594 is ground\nT595 is ground\nT597 is ground\ndelete(T594, tree(T595, T596, T597), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T594, tree(T595, T596, T597), T3) !=? delete(X515, tree(X515, X516, void), X516)\ndelete(T594, tree(T595, T596, T597), T3) !=? delete(X705, tree(X705, X706, X707), tree(X708, X706, X709))", fontsize=16, style=filled, fillcolor=lightyellow];
233 [label="233: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
234 [label="234: less(T595, T594)\n\nT594 is ground\nT595 is ground\ndelete(T594, tree(T595, T596, T597), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T594, tree(T595, T596, T597), T3) !=? delete(X515, tree(X515, X516, void), X516)\ndelete(T594, tree(T595, T596, T597), T3) !=? delete(X705, tree(X705, X706, X707), tree(X708, X706, X709))", fontsize=16, style=filled, fillcolor=lightyellow];
235 [label="235: delete(T594, T597, T599)\n\nT594 is ground\nT597 is ground\ndelete(T594, tree(T595, T596, T597), T3) !=? delete(X515, tree(X515, X516, void), X516)", fontsize=16, style=filled, fillcolor=lightyellow];
236 [label="236: ','(less(T614, T613), delete(T613, T616, T618))\n\nT613 is ground\nT614 is ground\nT616 is ground\ndelete(T613, tree(T614, T615, T616), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T613, tree(T614, T615, T616), T3) !=? delete(X515, tree(X515, X516, void), X516)\ndelete(T613, tree(T614, T615, T616), T3) !=? delete(X705, tree(X705, X706, X707), tree(X708, X706, X709))", fontsize=16, style=filled, fillcolor=lightyellow];
237 [label="237: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
238 [label="238: ','(less(T614, T613), delete(T613, T616, T618)), SCOPE: 23, CLAUSE: 7 | ','(less(T614, T613), delete(T613, T616, T618)), SCOPE: 23, CLAUSE: 8\n\nT613 is ground\nT614 is ground\nT616 is ground\ndelete(T613, tree(T614, T615, T616), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T613, tree(T614, T615, T616), T3) !=? delete(X515, tree(X515, X516, void), X516)\ndelete(T613, tree(T614, T615, T616), T3) !=? delete(X705, tree(X705, X706, X707), tree(X708, X706, X709))", fontsize=16, style=filled, fillcolor=lightyellow];
239 [label="239: ','(less(T614, T613), delete(T613, T616, T618)), SCOPE: 23, CLAUSE: 7\n\nT613 is ground\nT614 is ground\nT616 is ground\ndelete(T613, tree(T614, T615, T616), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T613, tree(T614, T615, T616), T3) !=? delete(X515, tree(X515, X516, void), X516)\ndelete(T613, tree(T614, T615, T616), T3) !=? delete(X705, tree(X705, X706, X707), tree(X708, X706, X709))", fontsize=16, style=filled, fillcolor=lightyellow];
240 [label="240: ','(less(T614, T613), delete(T613, T616, T618)), SCOPE: 23, CLAUSE: 8\n\nT613 is ground\nT614 is ground\nT616 is ground\ndelete(T613, tree(T614, T615, T616), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(T613, tree(T614, T615, T616), T3) !=? delete(X515, tree(X515, X516, void), X516)\ndelete(T613, tree(T614, T615, T616), T3) !=? delete(X705, tree(X705, X706, X707), tree(X708, X706, X709))", fontsize=16, style=filled, fillcolor=lightyellow];
241 [label="241: delete(s(T623), T616, T618)\n\nT616 is ground\nT623 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
242 [label="242: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
243 [label="243: ','(less(T632, T633), delete(s(T633), T616, T618))\n\nT616 is ground\nT632 is ground\nT633 is ground\ndelete(s(T633), tree(s(T632), T615, T616), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(s(T633), tree(s(T632), T615, T616), T3) !=? delete(X515, tree(X515, X516, void), X516)\ndelete(s(T633), tree(s(T632), T615, T616), T3) !=? delete(X705, tree(X705, X706, X707), tree(X708, X706, X709))", fontsize=16, style=filled, fillcolor=lightyellow];
244 [label="244: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
245 [label="245: less(T632, T633)\n\nT632 is ground\nT633 is ground\ndelete(s(T633), tree(s(T632), T615, T616), T3) !=? delete(X6, tree(X6, void, X7), X7)\ndelete(s(T633), tree(s(T632), T615, T616), T3) !=? delete(X515, tree(X515, X516, void), X516)\ndelete(s(T633), tree(s(T632), T615, T616), T3) !=? delete(X705, tree(X705, X706, X707), tree(X708, X706, X709))", fontsize=16, style=filled, fillcolor=lightyellow];
246 [label="246: delete(s(T633), T616, T618)\n\nT616 is ground\nT633 is ground\ndelete(s(T633), tree(s(T632), T615, T616), T3) !=? delete(X515, tree(X515, X516, void), X516)", fontsize=16, style=filled, fillcolor=lightyellow];
247 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 247 [arrowhead = none ];
247 -> 2;

248 [label="EVAL with clause\ndelete(X6, tree(X6, void, X7), X7).\nand substitution\nT1 -> T6\nX6 -> T6\nX7 -> T7\nT2 -> tree(T6, void, T7)\nT3 -> T7", fontsize=14, style = filled, fillcolor = lightblue];
2 -> 248 [arrowhead = none ];
248 -> 3;

249 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
2 -> 249 [arrowhead = none ];
249 -> 4;

250 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
3 -> 250 [arrowhead = none ];
250 -> 5;

251 [label="EVAL with clause\ndelete(X515, tree(X515, X516, void), X516).\nand substitution\nT1 -> T251\nX515 -> T251\nX516 -> T252\nT2 -> tree(T251, T252, void)\nT3 -> T252", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 251 [arrowhead = none ];
251 -> 94;

252 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 252 [arrowhead = none ];
252 -> 95;

253 [label="EVAL with clause\ndelete(X12, tree(X12, X13, void), X13).\nand substitution\nT6 -> T9\nX12 -> T9\nX13 -> void\nT7 -> void\nT3 -> void", fontsize=14, style = filled, fillcolor = lightblue];
5 -> 253 [arrowhead = none ];
253 -> 6;

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

255 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
6 -> 255 [arrowhead = none ];
255 -> 8;

256 [label="EVAL with clause\ndelete(X253, tree(X253, X254, X255), tree(X256, X254, X257)) :- delmin(X255, X256, X257).\nand substitution\nT6 -> T90\nX253 -> T90\nX254 -> void\nT7 -> T91\nX255 -> T91\nX256 -> T94\nX257 -> T95\nT3 -> tree(T94, void, T95)\nT92 -> T94\nT93 -> T95", fontsize=14, style = filled, fillcolor = lightblue];
7 -> 256 [arrowhead = none ];
256 -> 46;

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

258 [label="EVAL with clause\ndelete(X21, tree(X21, X22, X23), tree(X24, X22, X25)) :- delmin(X23, X24, X25).\nand substitution\nT9 -> T13\nX21 -> T13\nX22 -> void\nX23 -> void\nX24 -> T16\nX25 -> T17\nT3 -> tree(T16, void, T17)\nT14 -> T16\nT15 -> T17", fontsize=14, style = filled, fillcolor = lightblue];
8 -> 258 [arrowhead = none ];
258 -> 9;

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

260 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
9 -> 260 [arrowhead = none ];
260 -> 11;

261 [label="EVAL with clause\ndelete(X142, tree(X143, X144, X145), tree(X143, X146, X145)) :- ','(less(X142, X143), delete(X142, X144, X146)).\nand substitution\nT9 -> T52\nX142 -> T52\nX143 -> T52\nX144 -> void\nX145 -> void\nX146 -> T54\nT3 -> tree(T52, T54, void)\nT53 -> T54", fontsize=14, style = filled, fillcolor = lightblue];
10 -> 261 [arrowhead = none ];
261 -> 27;

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

263 [label="BACKTRACK\nfor clause: delmin(tree(Y, void, Right), Y, Right)because of non-unification", fontsize=14, style = filled, fillcolor = white];
11 -> 263 [arrowhead = none ];
263 -> 12;

264 [label="BACKTRACK\nfor clause: delmin(tree(X, Left, X1), Y, tree(X, Left1, X2)) :- delmin(Left, Y, Left1)because of non-unification", fontsize=14, style = filled, fillcolor = white];
12 -> 264 [arrowhead = none ];
264 -> 13;

265 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
13 -> 265 [arrowhead = none ];
265 -> 14;

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

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

268 [label="EVAL with clause\ndelete(X59, tree(X60, X61, X62), tree(X60, X63, X62)) :- ','(less(X59, X60), delete(X59, X61, X63)).\nand substitution\nT13 -> T26\nX59 -> T26\nX60 -> T26\nX61 -> void\nX62 -> void\nX63 -> T28\nT3 -> tree(T26, T28, void)\nT27 -> T28", fontsize=14, style = filled, fillcolor = lightblue];
15 -> 268 [arrowhead = none ];
268 -> 17;

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

270 [label="EVAL with clause\ndelete(X123, tree(X124, X125, X126), tree(X124, X125, X127)) :- ','(less(X124, X123), delete(X123, X126, X127)).\nand substitution\nT13 -> T46\nX123 -> T46\nX124 -> T46\nX125 -> void\nX126 -> void\nX127 -> T48\nT3 -> tree(T46, void, T48)\nT47 -> T48", fontsize=14, style = filled, fillcolor = lightblue];
16 -> 270 [arrowhead = none ];
270 -> 25;

271 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
16 -> 271 [arrowhead = none ];
271 -> 26;

272 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
17 -> 272 [arrowhead = none ];
272 -> 19;

273 [label="SPLIT 2", fontsize=14, style = filled, fillcolor = violet];
17 -> 273 [arrowhead = none ];
273 -> 20;

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

275 [label="INSTANCE with matching:\nT1 -> T26\nT2 -> void\nT3 -> T28", fontsize=14, style = filled, fillcolor = lightgrey];
20 -> 275 [arrowhead = none , style=dashed];
275 -> 1[style=dashed];

276 [label="BACKTRACK\nfor clause: less(0, s(X3))because of non-unification", fontsize=14, style = filled, fillcolor = white];
21 -> 276 [arrowhead = none ];
276 -> 22;

277 [label="EVAL with clause\nless(s(X82), s(X83)) :- less(X82, X83).\nand substitution\nX82 -> T33\nT26 -> s(T33)\nX83 -> T33", fontsize=14, style = filled, fillcolor = lightblue];
22 -> 277 [arrowhead = none ];
277 -> 23;

278 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
22 -> 278 [arrowhead = none ];
278 -> 24;

279 [label="INSTANCE with matching:\nT26 -> T33", fontsize=14, style = filled, fillcolor = lightgrey];
23 -> 279 [arrowhead = none , style=dashed];
279 -> 19[style=dashed];

280 [label="INSTANCE with matching:\nT26 -> T46\nT28 -> T48", fontsize=14, style = filled, fillcolor = lightgrey];
25 -> 280 [arrowhead = none , style=dashed];
280 -> 17[style=dashed];

281 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
27 -> 281 [arrowhead = none ];
281 -> 29;

282 [label="EVAL with clause\ndelete(X225, tree(X226, X227, X228), tree(X226, X227, X229)) :- ','(less(X226, X225), delete(X225, X228, X229)).\nand substitution\nT9 -> T79\nX225 -> T79\nX226 -> T79\nX227 -> void\nX228 -> void\nX229 -> T81\nT3 -> tree(T79, void, T81)\nT80 -> T81", fontsize=14, style = filled, fillcolor = lightblue];
28 -> 282 [arrowhead = none ];
282 -> 40;

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

284 [label="BACKTRACK\nfor clause: less(0, s(X3))because of non-unification", fontsize=14, style = filled, fillcolor = white];
29 -> 284 [arrowhead = none ];
284 -> 30;

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

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

287 [label="EVAL with clause\nless(s(X161), s(X162)) :- less(X161, X162).\nand substitution\nX161 -> T59\nT52 -> s(T59)\nX162 -> T59", fontsize=14, style = filled, fillcolor = lightblue];
31 -> 287 [arrowhead = none ];
287 -> 33;

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

289 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
32 -> 289 [arrowhead = none ];
289 -> 37;

290 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
33 -> 290 [arrowhead = none ];
290 -> 35;

291 [label="SPLIT 2", fontsize=14, style = filled, fillcolor = violet];
33 -> 291 [arrowhead = none ];
291 -> 36;

292 [label="INSTANCE with matching:\nT26 -> T59", fontsize=14, style = filled, fillcolor = lightgrey];
35 -> 292 [arrowhead = none , style=dashed];
292 -> 19[style=dashed];

293 [label="INSTANCE with matching:\nT1 -> s(T59)\nT2 -> void\nT3 -> T54", fontsize=14, style = filled, fillcolor = lightgrey];
36 -> 293 [arrowhead = none , style=dashed];
293 -> 1[style=dashed];

294 [label="EVAL with clause\ndelete(X206, tree(X207, X208, X209), tree(X207, X208, X210)) :- ','(less(X207, X206), delete(X206, X209, X210)).\nand substitution\nT52 -> T73\nX206 -> T73\nX207 -> T73\nX208 -> void\nX209 -> void\nX210 -> T75\nT3 -> tree(T73, void, T75)\nT74 -> T75", fontsize=14, style = filled, fillcolor = lightblue];
37 -> 294 [arrowhead = none ];
294 -> 38;

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

296 [label="INSTANCE with matching:\nT26 -> T73\nT28 -> T75", fontsize=14, style = filled, fillcolor = lightgrey];
38 -> 296 [arrowhead = none , style=dashed];
296 -> 17[style=dashed];

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

298 [label="BACKTRACK\nfor clause: less(0, s(X3))because of non-unification", fontsize=14, style = filled, fillcolor = white];
42 -> 298 [arrowhead = none ];
298 -> 43;

299 [label="EVAL with clause\nless(s(X240), s(X241)) :- less(X240, X241).\nand substitution\nX240 -> T84\nT79 -> s(T84)\nX241 -> T84", fontsize=14, style = filled, fillcolor = lightblue];
43 -> 299 [arrowhead = none ];
299 -> 44;

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

301 [label="INSTANCE with matching:\nT59 -> T84\nT54 -> T81", fontsize=14, style = filled, fillcolor = lightgrey];
44 -> 301 [arrowhead = none , style=dashed];
301 -> 33[style=dashed];

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

303 [label="EVAL with clause\ndelete(X426, tree(X427, X428, X429), tree(X427, X430, X429)) :- ','(less(X426, X427), delete(X426, X428, X430)).\nand substitution\nT6 -> T212\nX426 -> T212\nX427 -> T212\nX428 -> void\nT7 -> T213\nX429 -> T213\nX430 -> T215\nT3 -> tree(T212, T215, T213)\nT214 -> T215", fontsize=14, style = filled, fillcolor = lightblue];
47 -> 303 [arrowhead = none ];
303 -> 75;

304 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
47 -> 304 [arrowhead = none ];
304 -> 76;

305 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
48 -> 305 [arrowhead = none ];
305 -> 49;

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

307 [label="EVAL with clause\ndelmin(tree(X271, void, X272), X271, X272).\nand substitution\nX271 -> T104\nX272 -> T105\nT91 -> tree(T104, void, T105)\nT94 -> T104\nT95 -> T105", fontsize=14, style = filled, fillcolor = lightblue];
49 -> 307 [arrowhead = none ];
307 -> 51;

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

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

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

311 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
51 -> 311 [arrowhead = none ];
311 -> 53;

312 [label="EVAL with clause\ndelmin(tree(X299, X300, X301), X302, tree(X299, X303, X304)) :- delmin(X300, X302, X303).\nand substitution\nX299 -> T130\nX300 -> T131\nX301 -> T132\nT91 -> tree(T130, T131, T132)\nT94 -> T136\nX302 -> T136\nX303 -> T137\nX304 -> T135\nT95 -> tree(T130, T137, T135)\nT133 -> T136\nT134 -> T137", fontsize=14, style = filled, fillcolor = lightblue];
54 -> 312 [arrowhead = none ];
312 -> 56;

313 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
54 -> 313 [arrowhead = none ];
313 -> 57;

314 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
55 -> 314 [arrowhead = none ];
314 -> 66;

315 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
56 -> 315 [arrowhead = none ];
315 -> 58;

316 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
58 -> 316 [arrowhead = none ];
316 -> 59;

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

318 [label="EVAL with clause\ndelmin(tree(X323, void, X324), X323, X324).\nand substitution\nX323 -> T150\nX324 -> T151\nT131 -> tree(T150, void, T151)\nT136 -> T150\nT137 -> T151", fontsize=14, style = filled, fillcolor = lightblue];
59 -> 318 [arrowhead = none ];
318 -> 61;

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

320 [label="EVAL with clause\ndelmin(tree(X339, X340, X341), X342, tree(X339, X343, X344)) :- delmin(X340, X342, X343).\nand substitution\nX339 -> T164\nX340 -> T165\nX341 -> T166\nT131 -> tree(T164, T165, T166)\nT136 -> T170\nX342 -> T170\nX343 -> T171\nX344 -> T169\nT137 -> tree(T164, T171, T169)\nT167 -> T170\nT168 -> T171", fontsize=14, style = filled, fillcolor = lightblue];
60 -> 320 [arrowhead = none ];
320 -> 64;

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

322 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
61 -> 322 [arrowhead = none ];
322 -> 63;

323 [label="INSTANCE with matching:\nT131 -> T165\nT136 -> T170\nT137 -> T171", fontsize=14, style = filled, fillcolor = lightgrey];
64 -> 323 [arrowhead = none , style=dashed];
323 -> 56[style=dashed];

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

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

326 [label="EVAL with clause\ndelete(X375, tree(X376, X377, X378), tree(X376, X379, X378)) :- ','(less(X375, X376), delete(X375, X377, X379)).\nand substitution\nT90 -> T188\nX375 -> T188\nX376 -> T188\nX377 -> void\nT91 -> T189\nX378 -> T189\nX379 -> T191\nT3 -> tree(T188, T191, T189)\nT190 -> T191", fontsize=14, style = filled, fillcolor = lightblue];
67 -> 326 [arrowhead = none ];
326 -> 69;

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

328 [label="EVAL with clause\ndelete(X399, tree(X400, X401, X402), tree(X400, X401, X403)) :- ','(less(X400, X399), delete(X399, X402, X403)).\nand substitution\nT90 -> T199\nX399 -> T199\nX400 -> T199\nX401 -> void\nT91 -> T200\nX402 -> T200\nX403 -> T202\nT3 -> tree(T199, void, T202)\nT201 -> T202", fontsize=14, style = filled, fillcolor = lightblue];
68 -> 328 [arrowhead = none ];
328 -> 71;

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

330 [label="INSTANCE with matching:\nT79 -> T188\nT81 -> T191", fontsize=14, style = filled, fillcolor = lightgrey];
69 -> 330 [arrowhead = none , style=dashed];
330 -> 40[style=dashed];

331 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
71 -> 331 [arrowhead = none ];
331 -> 73;

332 [label="SPLIT 2", fontsize=14, style = filled, fillcolor = violet];
71 -> 332 [arrowhead = none ];
332 -> 74;

333 [label="INSTANCE with matching:\nT59 -> T199", fontsize=14, style = filled, fillcolor = lightgrey];
73 -> 333 [arrowhead = none , style=dashed];
333 -> 35[style=dashed];

334 [label="INSTANCE with matching:\nT1 -> T199\nT2 -> T200\nT3 -> T202", fontsize=14, style = filled, fillcolor = lightgrey];
74 -> 334 [arrowhead = none , style=dashed];
334 -> 1[style=dashed];

335 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
75 -> 335 [arrowhead = none ];
335 -> 77;

336 [label="EVAL with clause\ndelete(X482, tree(X483, X484, X485), tree(X483, X484, X486)) :- ','(less(X483, X482), delete(X482, X485, X486)).\nand substitution\nT6 -> T236\nX482 -> T236\nX483 -> T236\nX484 -> void\nT7 -> T237\nX485 -> T237\nX486 -> T239\nT3 -> tree(T236, void, T239)\nT238 -> T239", fontsize=14, style = filled, fillcolor = lightblue];
76 -> 336 [arrowhead = none ];
336 -> 86;

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

338 [label="BACKTRACK\nfor clause: less(0, s(X3))because of non-unification", fontsize=14, style = filled, fillcolor = white];
77 -> 338 [arrowhead = none ];
338 -> 78;

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

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

341 [label="EVAL with clause\nless(s(X445), s(X446)) :- less(X445, X446).\nand substitution\nX445 -> T220\nT212 -> s(T220)\nX446 -> T220", fontsize=14, style = filled, fillcolor = lightblue];
79 -> 341 [arrowhead = none ];
341 -> 81;

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

343 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
80 -> 343 [arrowhead = none ];
343 -> 83;

344 [label="INSTANCE with matching:\nT59 -> T220\nT54 -> T215", fontsize=14, style = filled, fillcolor = lightgrey];
81 -> 344 [arrowhead = none , style=dashed];
344 -> 33[style=dashed];

345 [label="EVAL with clause\ndelete(X463, tree(X464, X465, X466), tree(X464, X465, X467)) :- ','(less(X464, X463), delete(X463, X466, X467)).\nand substitution\nT212 -> T228\nX463 -> T228\nX464 -> T228\nX465 -> void\nT213 -> T229\nX466 -> T229\nX467 -> T231\nT3 -> tree(T228, void, T231)\nT230 -> T231", fontsize=14, style = filled, fillcolor = lightblue];
83 -> 345 [arrowhead = none ];
345 -> 84;

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

347 [label="INSTANCE with matching:\nT199 -> T228\nT200 -> T229\nT202 -> T231", fontsize=14, style = filled, fillcolor = lightgrey];
84 -> 347 [arrowhead = none , style=dashed];
347 -> 71[style=dashed];

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

349 [label="BACKTRACK\nfor clause: less(0, s(X3))because of non-unification", fontsize=14, style = filled, fillcolor = white];
88 -> 349 [arrowhead = none ];
349 -> 89;

350 [label="EVAL with clause\nless(s(X497), s(X498)) :- less(X497, X498).\nand substitution\nX497 -> T242\nT236 -> s(T242)\nX498 -> T242", fontsize=14, style = filled, fillcolor = lightblue];
89 -> 350 [arrowhead = none ];
350 -> 90;

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

352 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
90 -> 352 [arrowhead = none ];
352 -> 92;

353 [label="SPLIT 2", fontsize=14, style = filled, fillcolor = violet];
90 -> 353 [arrowhead = none ];
353 -> 93;

354 [label="INSTANCE with matching:\nT59 -> T242", fontsize=14, style = filled, fillcolor = lightgrey];
92 -> 354 [arrowhead = none , style=dashed];
354 -> 35[style=dashed];

355 [label="INSTANCE with matching:\nT1 -> s(T242)\nT2 -> T237\nT3 -> T239", fontsize=14, style = filled, fillcolor = lightgrey];
93 -> 355 [arrowhead = none , style=dashed];
355 -> 1[style=dashed];

356 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
94 -> 356 [arrowhead = none ];
356 -> 96;

357 [label="EVAL with clause\ndelete(X705, tree(X705, X706, X707), tree(X708, X706, X709)) :- delmin(X707, X708, X709).\nand substitution\nT1 -> T341\nX705 -> T341\nX706 -> T342\nX707 -> T343\nT2 -> tree(T341, T342, T343)\nX708 -> T346\nX709 -> T347\nT3 -> tree(T346, T342, T347)\nT344 -> T346\nT345 -> T347", fontsize=14, style = filled, fillcolor = lightblue];
95 -> 357 [arrowhead = none ];
357 -> 130;

358 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
95 -> 358 [arrowhead = none ];
358 -> 131;

359 [label="EVAL with clause\ndelete(X524, tree(X524, X525, X526), tree(X527, X525, X528)) :- delmin(X526, X527, X528).\nand substitution\nT251 -> T257\nX524 -> T257\nT252 -> T258\nX525 -> T258\nX526 -> void\nX527 -> T261\nX528 -> T262\nT3 -> tree(T261, T258, T262)\nT259 -> T261\nT260 -> T262", fontsize=14, style = filled, fillcolor = lightblue];
96 -> 359 [arrowhead = none ];
359 -> 97;

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

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

362 [label="EVAL with clause\ndelete(X613, tree(X614, X615, X616), tree(X614, X617, X616)) :- ','(less(X613, X614), delete(X613, X615, X617)).\nand substitution\nT251 -> T299\nX613 -> T299\nX614 -> T299\nT252 -> T300\nX615 -> T300\nX616 -> void\nX617 -> T302\nT3 -> tree(T299, T302, void)\nT301 -> T302", fontsize=14, style = filled, fillcolor = lightblue];
98 -> 362 [arrowhead = none ];
362 -> 111;

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

364 [label="BACKTRACK\nfor clause: delmin(tree(Y, void, Right), Y, Right)because of non-unification", fontsize=14, style = filled, fillcolor = white];
99 -> 364 [arrowhead = none ];
364 -> 100;

365 [label="BACKTRACK\nfor clause: delmin(tree(X, Left, X1), Y, tree(X, Left1, X2)) :- delmin(Left, Y, Left1)because of non-unification", fontsize=14, style = filled, fillcolor = white];
100 -> 365 [arrowhead = none ];
365 -> 101;

366 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
101 -> 366 [arrowhead = none ];
366 -> 102;

367 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
102 -> 367 [arrowhead = none ];
367 -> 103;

368 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
102 -> 368 [arrowhead = none ];
368 -> 104;

369 [label="EVAL with clause\ndelete(X562, tree(X563, X564, X565), tree(X563, X566, X565)) :- ','(less(X562, X563), delete(X562, X564, X566)).\nand substitution\nT257 -> T275\nX562 -> T275\nX563 -> T275\nT258 -> T276\nX564 -> T276\nX565 -> void\nX566 -> T278\nT3 -> tree(T275, T278, void)\nT277 -> T278", fontsize=14, style = filled, fillcolor = lightblue];
103 -> 369 [arrowhead = none ];
369 -> 105;

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

371 [label="EVAL with clause\ndelete(X594, tree(X595, X596, X597), tree(X595, X596, X598)) :- ','(less(X595, X594), delete(X594, X597, X598)).\nand substitution\nT257 -> T291\nX594 -> T291\nX595 -> T291\nT258 -> T292\nX596 -> T292\nX597 -> void\nX598 -> T294\nT3 -> tree(T291, T292, T294)\nT293 -> T294", fontsize=14, style = filled, fillcolor = lightblue];
104 -> 371 [arrowhead = none ];
371 -> 109;

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

373 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
105 -> 373 [arrowhead = none ];
373 -> 107;

374 [label="SPLIT 2", fontsize=14, style = filled, fillcolor = violet];
105 -> 374 [arrowhead = none ];
374 -> 108;

375 [label="INSTANCE with matching:\nT242 -> T275", fontsize=14, style = filled, fillcolor = lightgrey];
107 -> 375 [arrowhead = none , style=dashed];
375 -> 92[style=dashed];

376 [label="INSTANCE with matching:\nT1 -> T275\nT2 -> T276\nT3 -> T278", fontsize=14, style = filled, fillcolor = lightgrey];
108 -> 376 [arrowhead = none , style=dashed];
376 -> 1[style=dashed];

377 [label="INSTANCE with matching:\nT79 -> T291\nT81 -> T294", fontsize=14, style = filled, fillcolor = lightgrey];
109 -> 377 [arrowhead = none , style=dashed];
377 -> 40[style=dashed];

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

379 [label="EVAL with clause\ndelete(X677, tree(X678, X679, X680), tree(X678, X679, X681)) :- ','(less(X678, X677), delete(X677, X680, X681)).\nand substitution\nT251 -> T328\nX677 -> T328\nX678 -> T328\nT252 -> T329\nX679 -> T329\nX680 -> void\nX681 -> T331\nT3 -> tree(T328, T329, T331)\nT330 -> T331", fontsize=14, style = filled, fillcolor = lightblue];
112 -> 379 [arrowhead = none ];
379 -> 124;

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

381 [label="BACKTRACK\nfor clause: less(0, s(X3))because of non-unification", fontsize=14, style = filled, fillcolor = white];
113 -> 381 [arrowhead = none ];
381 -> 114;

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

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

384 [label="EVAL with clause\nless(s(X632), s(X633)) :- less(X632, X633).\nand substitution\nX632 -> T307\nT299 -> s(T307)\nX633 -> T307", fontsize=14, style = filled, fillcolor = lightblue];
115 -> 384 [arrowhead = none ];
384 -> 117;

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

386 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
116 -> 386 [arrowhead = none ];
386 -> 121;

387 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
117 -> 387 [arrowhead = none ];
387 -> 119;

388 [label="SPLIT 2", fontsize=14, style = filled, fillcolor = violet];
117 -> 388 [arrowhead = none ];
388 -> 120;

389 [label="INSTANCE with matching:\nT242 -> T307", fontsize=14, style = filled, fillcolor = lightgrey];
119 -> 389 [arrowhead = none , style=dashed];
389 -> 92[style=dashed];

390 [label="INSTANCE with matching:\nT1 -> s(T307)\nT2 -> T300\nT3 -> T302", fontsize=14, style = filled, fillcolor = lightgrey];
120 -> 390 [arrowhead = none , style=dashed];
390 -> 1[style=dashed];

391 [label="EVAL with clause\ndelete(X658, tree(X659, X660, X661), tree(X659, X660, X662)) :- ','(less(X659, X658), delete(X658, X661, X662)).\nand substitution\nT299 -> T320\nX658 -> T320\nX659 -> T320\nT300 -> T321\nX660 -> T321\nX661 -> void\nX662 -> T323\nT3 -> tree(T320, T321, T323)\nT322 -> T323", fontsize=14, style = filled, fillcolor = lightblue];
121 -> 391 [arrowhead = none ];
391 -> 122;

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

393 [label="INSTANCE with matching:\nT79 -> T320\nT81 -> T323", fontsize=14, style = filled, fillcolor = lightgrey];
122 -> 393 [arrowhead = none , style=dashed];
393 -> 40[style=dashed];

394 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
124 -> 394 [arrowhead = none ];
394 -> 126;

395 [label="BACKTRACK\nfor clause: less(0, s(X3))because of non-unification", fontsize=14, style = filled, fillcolor = white];
126 -> 395 [arrowhead = none ];
395 -> 127;

396 [label="EVAL with clause\nless(s(X692), s(X693)) :- less(X692, X693).\nand substitution\nX692 -> T334\nT328 -> s(T334)\nX693 -> T334", fontsize=14, style = filled, fillcolor = lightblue];
127 -> 396 [arrowhead = none ];
396 -> 128;

397 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
127 -> 397 [arrowhead = none ];
397 -> 129;

398 [label="INSTANCE with matching:\nT220 -> T334\nT215 -> T331", fontsize=14, style = filled, fillcolor = lightgrey];
128 -> 398 [arrowhead = none , style=dashed];
398 -> 81[style=dashed];

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

400 [label="EVAL with clause\ndelete(X846, tree(X847, X848, X849), tree(X847, X850, X849)) :- ','(less(X846, X847), delete(X846, X848, X850)).\nand substitution\nT1 -> T445\nX846 -> T445\nX847 -> T446\nX848 -> T447\nX849 -> T448\nT2 -> tree(T446, T447, T448)\nX850 -> T450\nT3 -> tree(T446, T450, T448)\nT449 -> T450", fontsize=14, style = filled, fillcolor = lightblue];
131 -> 400 [arrowhead = none ];
400 -> 153;

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

402 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
132 -> 402 [arrowhead = none ];
402 -> 133;

403 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
132 -> 403 [arrowhead = none ];
403 -> 134;

404 [label="EVAL with clause\ndelmin(tree(X723, void, X724), X723, X724).\nand substitution\nX723 -> T356\nX724 -> T357\nT343 -> tree(T356, void, T357)\nT346 -> T356\nT347 -> T357", fontsize=14, style = filled, fillcolor = lightblue];
133 -> 404 [arrowhead = none ];
404 -> 135;

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

406 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
134 -> 406 [arrowhead = none ];
406 -> 138;

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

408 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
135 -> 408 [arrowhead = none ];
408 -> 137;

409 [label="EVAL with clause\ndelmin(tree(X751, X752, X753), X754, tree(X751, X755, X756)) :- delmin(X752, X754, X755).\nand substitution\nX751 -> T382\nX752 -> T383\nX753 -> T384\nT343 -> tree(T382, T383, T384)\nT346 -> T388\nX754 -> T388\nX755 -> T389\nX756 -> T387\nT347 -> tree(T382, T389, T387)\nT385 -> T388\nT386 -> T389", fontsize=14, style = filled, fillcolor = lightblue];
138 -> 409 [arrowhead = none ];
409 -> 140;

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

411 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
139 -> 411 [arrowhead = none ];
411 -> 142;

412 [label="INSTANCE with matching:\nT131 -> T383\nT136 -> T388\nT137 -> T389", fontsize=14, style = filled, fillcolor = lightgrey];
140 -> 412 [arrowhead = none , style=dashed];
412 -> 56[style=dashed];

413 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
142 -> 413 [arrowhead = none ];
413 -> 143;

414 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
142 -> 414 [arrowhead = none ];
414 -> 144;

415 [label="EVAL with clause\ndelete(X787, tree(X788, X789, X790), tree(X788, X791, X790)) :- ','(less(X787, X788), delete(X787, X789, X791)).\nand substitution\nT341 -> T410\nX787 -> T410\nX788 -> T410\nT342 -> T411\nX789 -> T411\nT343 -> T412\nX790 -> T412\nX791 -> T414\nT3 -> tree(T410, T414, T412)\nT413 -> T414", fontsize=14, style = filled, fillcolor = lightblue];
143 -> 415 [arrowhead = none ];
415 -> 145;

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

417 [label="EVAL with clause\ndelete(X819, tree(X820, X821, X822), tree(X820, X821, X823)) :- ','(less(X820, X819), delete(X819, X822, X823)).\nand substitution\nT341 -> T429\nX819 -> T429\nX820 -> T429\nT342 -> T430\nX821 -> T430\nT343 -> T431\nX822 -> T431\nX823 -> T433\nT3 -> tree(T429, T430, T433)\nT432 -> T433", fontsize=14, style = filled, fillcolor = lightblue];
144 -> 417 [arrowhead = none ];
417 -> 149;

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

419 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
145 -> 419 [arrowhead = none ];
419 -> 147;

420 [label="SPLIT 2", fontsize=14, style = filled, fillcolor = violet];
145 -> 420 [arrowhead = none ];
420 -> 148;

421 [label="INSTANCE with matching:\nT242 -> T410", fontsize=14, style = filled, fillcolor = lightgrey];
147 -> 421 [arrowhead = none , style=dashed];
421 -> 92[style=dashed];

422 [label="INSTANCE with matching:\nT1 -> T410\nT2 -> T411\nT3 -> T414", fontsize=14, style = filled, fillcolor = lightgrey];
148 -> 422 [arrowhead = none , style=dashed];
422 -> 1[style=dashed];

423 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
149 -> 423 [arrowhead = none ];
423 -> 151;

424 [label="SPLIT 2", fontsize=14, style = filled, fillcolor = violet];
149 -> 424 [arrowhead = none ];
424 -> 152;

425 [label="INSTANCE with matching:\nT242 -> T429", fontsize=14, style = filled, fillcolor = lightgrey];
151 -> 425 [arrowhead = none , style=dashed];
425 -> 92[style=dashed];

426 [label="INSTANCE with matching:\nT1 -> T429\nT2 -> T431\nT3 -> T433", fontsize=14, style = filled, fillcolor = lightgrey];
152 -> 426 [arrowhead = none , style=dashed];
426 -> 1[style=dashed];

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

428 [label="EVAL with clause\ndelete(X1049, tree(X1050, X1051, X1052), tree(X1050, X1051, X1053)) :- ','(less(X1050, X1049), delete(X1049, X1052, X1053)).\nand substitution\nT1 -> T613\nX1049 -> T613\nX1050 -> T614\nX1051 -> T615\nX1052 -> T616\nT2 -> tree(T614, T615, T616)\nX1053 -> T618\nT3 -> tree(T614, T615, T618)\nT617 -> T618", fontsize=14, style = filled, fillcolor = lightblue];
154 -> 428 [arrowhead = none ];
428 -> 236;

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

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

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

432 [label="EVAL with clause\nless(0, s(X860)).\nand substitution\nT445 -> 0\nX860 -> T455\nT446 -> s(T455)", fontsize=14, style = filled, fillcolor = lightblue];
156 -> 432 [arrowhead = none ];
432 -> 158;

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

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

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

436 [label="INSTANCE with matching:\nT1 -> 0\nT2 -> T447\nT3 -> T450", fontsize=14, style = filled, fillcolor = lightgrey];
158 -> 436 [arrowhead = none , style=dashed];
436 -> 1[style=dashed];

437 [label="EVAL with clause\nless(s(X874), s(X875)) :- less(X874, X875).\nand substitution\nX874 -> T466\nT445 -> s(T466)\nX875 -> T467\nT446 -> s(T467)", fontsize=14, style = filled, fillcolor = lightblue];
160 -> 437 [arrowhead = none ];
437 -> 162;

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

439 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
161 -> 439 [arrowhead = none ];
439 -> 231;

440 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
162 -> 440 [arrowhead = none ];
440 -> 164;

441 [label="SPLIT 2", fontsize=14, style = filled, fillcolor = violet];
162 -> 441 [arrowhead = none ];
441 -> 165;

442 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
164 -> 442 [arrowhead = none ];
442 -> 166;

443 [label="INSTANCE with matching:\nT1 -> s(T466)\nT2 -> T447\nT3 -> T450", fontsize=14, style = filled, fillcolor = lightgrey];
165 -> 443 [arrowhead = none , style=dashed];
443 -> 1[style=dashed];

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

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

446 [label="EVAL with clause\nless(0, s(X886)).\nand substitution\nT466 -> 0\nX886 -> T476\nT467 -> s(T476)", fontsize=14, style = filled, fillcolor = lightblue];
167 -> 446 [arrowhead = none ];
446 -> 169;

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

448 [label="EVAL with clause\nless(s(X892), s(X893)) :- less(X892, X893).\nand substitution\nX892 -> T481\nT466 -> s(T481)\nX893 -> T482\nT467 -> s(T482)", fontsize=14, style = filled, fillcolor = lightblue];
168 -> 448 [arrowhead = none ];
448 -> 172;

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

450 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
169 -> 450 [arrowhead = none ];
450 -> 171;

451 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
172 -> 451 [arrowhead = none ];
451 -> 174;

452 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
174 -> 452 [arrowhead = none ];
452 -> 175;

453 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
174 -> 453 [arrowhead = none ];
453 -> 176;

454 [label="EVAL with clause\nless(0, s(X902)).\nand substitution\nT481 -> 0\nX902 -> T489\nT482 -> s(T489)", fontsize=14, style = filled, fillcolor = lightblue];
175 -> 454 [arrowhead = none ];
454 -> 177;

455 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
175 -> 455 [arrowhead = none ];
455 -> 178;

456 [label="EVAL with clause\nless(s(X908), s(X909)) :- less(X908, X909).\nand substitution\nX908 -> T494\nT481 -> s(T494)\nX909 -> T495\nT482 -> s(T495)", fontsize=14, style = filled, fillcolor = lightblue];
176 -> 456 [arrowhead = none ];
456 -> 180;

457 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
176 -> 457 [arrowhead = none ];
457 -> 181;

458 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
177 -> 458 [arrowhead = none ];
458 -> 179;

459 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
180 -> 459 [arrowhead = none ];
459 -> 182;

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

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

462 [label="EVAL with clause\nless(0, s(X918)).\nand substitution\nT494 -> 0\nX918 -> T502\nT495 -> s(T502)", fontsize=14, style = filled, fillcolor = lightblue];
183 -> 462 [arrowhead = none ];
462 -> 185;

463 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
183 -> 463 [arrowhead = none ];
463 -> 186;

464 [label="EVAL with clause\nless(s(X924), s(X925)) :- less(X924, X925).\nand substitution\nX924 -> T507\nT494 -> s(T507)\nX925 -> T508\nT495 -> s(T508)", fontsize=14, style = filled, fillcolor = lightblue];
184 -> 464 [arrowhead = none ];
464 -> 188;

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

466 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
185 -> 466 [arrowhead = none ];
466 -> 187;

467 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
188 -> 467 [arrowhead = none ];
467 -> 190;

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

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

470 [label="EVAL with clause\nless(0, s(X934)).\nand substitution\nT507 -> 0\nX934 -> T515\nT508 -> s(T515)", fontsize=14, style = filled, fillcolor = lightblue];
191 -> 470 [arrowhead = none ];
470 -> 193;

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

472 [label="EVAL with clause\nless(s(X940), s(X941)) :- less(X940, X941).\nand substitution\nX940 -> T520\nT507 -> s(T520)\nX941 -> T521\nT508 -> s(T521)", fontsize=14, style = filled, fillcolor = lightblue];
192 -> 472 [arrowhead = none ];
472 -> 196;

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

474 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
193 -> 474 [arrowhead = none ];
474 -> 195;

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

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

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

478 [label="EVAL with clause\nless(0, s(X950)).\nand substitution\nT520 -> 0\nX950 -> T528\nT521 -> s(T528)", fontsize=14, style = filled, fillcolor = lightblue];
199 -> 478 [arrowhead = none ];
478 -> 201;

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

480 [label="EVAL with clause\nless(s(X956), s(X957)) :- less(X956, X957).\nand substitution\nX956 -> T533\nT520 -> s(T533)\nX957 -> T534\nT521 -> s(T534)", fontsize=14, style = filled, fillcolor = lightblue];
200 -> 480 [arrowhead = none ];
480 -> 204;

481 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
200 -> 481 [arrowhead = none ];
481 -> 205;

482 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
201 -> 482 [arrowhead = none ];
482 -> 203;

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

484 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
206 -> 484 [arrowhead = none ];
484 -> 207;

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

486 [label="EVAL with clause\nless(0, s(X966)).\nand substitution\nT533 -> 0\nX966 -> T541\nT534 -> s(T541)", fontsize=14, style = filled, fillcolor = lightblue];
207 -> 486 [arrowhead = none ];
486 -> 209;

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

488 [label="EVAL with clause\nless(s(X972), s(X973)) :- less(X972, X973).\nand substitution\nX972 -> T546\nT533 -> s(T546)\nX973 -> T547\nT534 -> s(T547)", fontsize=14, style = filled, fillcolor = lightblue];
208 -> 488 [arrowhead = none ];
488 -> 212;

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

490 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
209 -> 490 [arrowhead = none ];
490 -> 211;

491 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
212 -> 491 [arrowhead = none ];
491 -> 214;

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

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

494 [label="EVAL with clause\nless(0, s(X982)).\nand substitution\nT546 -> 0\nX982 -> T554\nT547 -> s(T554)", fontsize=14, style = filled, fillcolor = lightblue];
215 -> 494 [arrowhead = none ];
494 -> 217;

495 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
215 -> 495 [arrowhead = none ];
495 -> 218;

496 [label="EVAL with clause\nless(s(X988), s(X989)) :- less(X988, X989).\nand substitution\nX988 -> T559\nT546 -> s(T559)\nX989 -> T560\nT547 -> s(T560)", fontsize=14, style = filled, fillcolor = lightblue];
216 -> 496 [arrowhead = none ];
496 -> 220;

497 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
216 -> 497 [arrowhead = none ];
497 -> 221;

498 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
217 -> 498 [arrowhead = none ];
498 -> 219;

499 [label="GENERALIZATION\nT563 <-- s(s(s(s(s(s(s(T559)))))))\nT564 <-- s(s(s(s(s(s(s(T560)))))))\n\nNew Knowledge:\nT563 is ground\nT564 is ground", fontsize=14, style = filled, fillcolor = violet];
220 -> 499 [arrowhead = none ];
499 -> 222;

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

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

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

503 [label="EVAL with clause\nless(0, s(X1000)).\nand substitution\nT559 -> 0\nX1000 -> T571\nT560 -> s(T571)", fontsize=14, style = filled, fillcolor = lightblue];
224 -> 503 [arrowhead = none ];
503 -> 226;

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

505 [label="EVAL with clause\nless(s(X1006), s(X1007)) :- less(X1006, X1007).\nand substitution\nX1006 -> T576\nT559 -> s(T576)\nX1007 -> T577\nT560 -> s(T577)", fontsize=14, style = filled, fillcolor = lightblue];
225 -> 505 [arrowhead = none ];
505 -> 229;

506 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
225 -> 506 [arrowhead = none ];
506 -> 230;

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

508 [label="INSTANCE with matching:\nT559 -> T576\nT560 -> T577", fontsize=14, style = filled, fillcolor = lightgrey];
229 -> 508 [arrowhead = none , style=dashed];
508 -> 222[style=dashed];

509 [label="EVAL with clause\ndelete(X1026, tree(X1027, X1028, X1029), tree(X1027, X1028, X1030)) :- ','(less(X1027, X1026), delete(X1026, X1029, X1030)).\nand substitution\nT445 -> T594\nX1026 -> T594\nT446 -> T595\nX1027 -> T595\nT447 -> T596\nX1028 -> T596\nT448 -> T597\nX1029 -> T597\nX1030 -> T599\nT3 -> tree(T595, T596, T599)\nT598 -> T599", fontsize=14, style = filled, fillcolor = lightblue];
231 -> 509 [arrowhead = none ];
509 -> 232;

510 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
231 -> 510 [arrowhead = none ];
510 -> 233;

511 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
232 -> 511 [arrowhead = none ];
511 -> 234;

512 [label="SPLIT 2", fontsize=14, style = filled, fillcolor = violet];
232 -> 512 [arrowhead = none ];
512 -> 235;

513 [label="INSTANCE with matching:\nT559 -> T595\nT560 -> T594", fontsize=14, style = filled, fillcolor = lightgrey];
234 -> 513 [arrowhead = none , style=dashed];
513 -> 222[style=dashed];

514 [label="INSTANCE with matching:\nT1 -> T594\nT2 -> T597\nT3 -> T599", fontsize=14, style = filled, fillcolor = lightgrey];
235 -> 514 [arrowhead = none , style=dashed];
514 -> 1[style=dashed];

515 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
236 -> 515 [arrowhead = none ];
515 -> 238;

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

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

518 [label="EVAL with clause\nless(0, s(X1063)).\nand substitution\nT614 -> 0\nX1063 -> T623\nT613 -> s(T623)", fontsize=14, style = filled, fillcolor = lightblue];
239 -> 518 [arrowhead = none ];
518 -> 241;

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

520 [label="EVAL with clause\nless(s(X1073), s(X1074)) :- less(X1073, X1074).\nand substitution\nX1073 -> T632\nT614 -> s(T632)\nX1074 -> T633\nT613 -> s(T633)", fontsize=14, style = filled, fillcolor = lightblue];
240 -> 520 [arrowhead = none ];
520 -> 243;

521 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
240 -> 521 [arrowhead = none ];
521 -> 244;

522 [label="INSTANCE with matching:\nT1 -> s(T623)\nT2 -> T616\nT3 -> T618", fontsize=14, style = filled, fillcolor = lightgrey];
241 -> 522 [arrowhead = none , style=dashed];
522 -> 1[style=dashed];

523 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
243 -> 523 [arrowhead = none ];
523 -> 245;

524 [label="SPLIT 2", fontsize=14, style = filled, fillcolor = violet];
243 -> 524 [arrowhead = none ];
524 -> 246;

525 [label="INSTANCE with matching:\nT559 -> T632\nT560 -> T633", fontsize=14, style = filled, fillcolor = lightgrey];
245 -> 525 [arrowhead = none , style=dashed];
525 -> 222[style=dashed];

526 [label="INSTANCE with matching:\nT1 -> s(T633)\nT2 -> T616\nT3 -> T618", fontsize=14, style = filled, fillcolor = lightgrey];
246 -> 526 [arrowhead = none , style=dashed];
526 -> 1[style=dashed];

}

(2) Obligation:

Triples:

less19(s(T33)) :- less19(T33).
p17(T26, T28) :- less19(T26).
p17(T26, T28) :- ','(lessc19(T26), delete1(T26, void, T28)).
p33(T59, T54) :- less19(T59).
p33(T59, T54) :- ','(lessc19(T59), delete1(s(T59), void, T54)).
delmin56(tree(T164, T165, T166), T170, tree(T164, T171, T169)) :- delmin56(T165, T170, T171).
p40(s(T84), T81) :- p33(T84, T81).
p71(T199, T200, T202) :- less19(T199).
p71(T199, T200, T202) :- ','(lessc19(T199), delete1(T199, T200, T202)).
less222(s(T576), s(T577)) :- less222(T576, T577).
delete1(T26, tree(T26, void, void), tree(T26, T28, void)) :- p17(T26, T28).
delete1(T46, tree(T46, void, void), tree(T46, void, T48)) :- p17(T46, T48).
delete1(s(T59), tree(s(T59), void, void), tree(s(T59), T54, void)) :- p33(T59, T54).
delete1(T73, tree(T73, void, void), tree(T73, void, T75)) :- p17(T73, T75).
delete1(T79, tree(T79, void, void), tree(T79, void, T81)) :- p40(T79, T81).
delete1(T90, tree(T90, void, tree(T130, T131, T132)), tree(T136, void, tree(T130, T137, T135))) :- delmin56(T131, T136, T137).
delete1(T188, tree(T188, void, T189), tree(T188, T191, T189)) :- p40(T188, T191).
delete1(T199, tree(T199, void, T200), tree(T199, void, T202)) :- p71(T199, T200, T202).
delete1(s(T220), tree(s(T220), void, T213), tree(s(T220), T215, T213)) :- p33(T220, T215).
delete1(T228, tree(T228, void, T229), tree(T228, void, T231)) :- p71(T228, T229, T231).
delete1(s(T242), tree(s(T242), void, T237), tree(s(T242), void, T239)) :- less19(T242).
delete1(s(T242), tree(s(T242), void, T237), tree(s(T242), void, T239)) :- ','(lessc19(T242), delete1(s(T242), T237, T239)).
delete1(T275, tree(T275, T276, void), tree(T275, T278, void)) :- less19(T275).
delete1(T275, tree(T275, T276, void), tree(T275, T278, void)) :- ','(lessc19(T275), delete1(T275, T276, T278)).
delete1(T291, tree(T291, T292, void), tree(T291, T292, T294)) :- p40(T291, T294).
delete1(s(T307), tree(s(T307), T300, void), tree(s(T307), T302, void)) :- less19(T307).
delete1(s(T307), tree(s(T307), T300, void), tree(s(T307), T302, void)) :- ','(lessc19(T307), delete1(s(T307), T300, T302)).
delete1(T320, tree(T320, T321, void), tree(T320, T321, T323)) :- p40(T320, T323).
delete1(s(T334), tree(s(T334), T329, void), tree(s(T334), T329, T331)) :- p33(T334, T331).
delete1(T341, tree(T341, T342, tree(T382, T383, T384)), tree(T388, T342, tree(T382, T389, T387))) :- delmin56(T383, T388, T389).
delete1(T410, tree(T410, T411, T412), tree(T410, T414, T412)) :- less19(T410).
delete1(T410, tree(T410, T411, T412), tree(T410, T414, T412)) :- ','(lessc19(T410), delete1(T410, T411, T414)).
delete1(T429, tree(T429, T430, T431), tree(T429, T430, T433)) :- less19(T429).
delete1(T429, tree(T429, T430, T431), tree(T429, T430, T433)) :- ','(lessc19(T429), delete1(T429, T431, T433)).
delete1(0, tree(s(T455), T447, T448), tree(s(T455), T450, T448)) :- delete1(0, T447, T450).
delete1(s(s(s(s(s(s(s(s(T559)))))))), tree(s(s(s(s(s(s(s(s(T560)))))))), T447, T448), tree(s(s(s(s(s(s(s(s(T560)))))))), T450, T448)) :- less222(T559, T560).
delete1(s(T466), tree(s(T467), T447, T448), tree(s(T467), T450, T448)) :- ','(lessc164(T466, T467), delete1(s(T466), T447, T450)).
delete1(T594, tree(T595, T596, T597), tree(T595, T596, T599)) :- less222(T595, T594).
delete1(T594, tree(T595, T596, T597), tree(T595, T596, T599)) :- ','(lessc222(T595, T594), delete1(T594, T597, T599)).
delete1(s(T623), tree(0, T615, T616), tree(0, T615, T618)) :- delete1(s(T623), T616, T618).
delete1(s(T633), tree(s(T632), T615, T616), tree(s(T632), T615, T618)) :- less222(T632, T633).
delete1(s(T633), tree(s(T632), T615, T616), tree(s(T632), T615, T618)) :- ','(lessc222(T632, T633), delete1(s(T633), T616, T618)).

Clauses:

deletec1(T6, tree(T6, void, T7), T7).
deletec1(T9, tree(T9, void, void), void).
deletec1(T26, tree(T26, void, void), tree(T26, T28, void)) :- qc17(T26, T28).
deletec1(T46, tree(T46, void, void), tree(T46, void, T48)) :- qc17(T46, T48).
deletec1(s(T59), tree(s(T59), void, void), tree(s(T59), T54, void)) :- qc33(T59, T54).
deletec1(T73, tree(T73, void, void), tree(T73, void, T75)) :- qc17(T73, T75).
deletec1(T79, tree(T79, void, void), tree(T79, void, T81)) :- qc40(T79, T81).
deletec1(T90, tree(T90, void, tree(T104, void, T105)), tree(T104, void, T105)).
deletec1(T90, tree(T90, void, tree(T130, T131, T132)), tree(T136, void, tree(T130, T137, T135))) :- delminc56(T131, T136, T137).
deletec1(T188, tree(T188, void, T189), tree(T188, T191, T189)) :- qc40(T188, T191).
deletec1(T199, tree(T199, void, T200), tree(T199, void, T202)) :- qc71(T199, T200, T202).
deletec1(s(T220), tree(s(T220), void, T213), tree(s(T220), T215, T213)) :- qc33(T220, T215).
deletec1(T228, tree(T228, void, T229), tree(T228, void, T231)) :- qc71(T228, T229, T231).
deletec1(s(T242), tree(s(T242), void, T237), tree(s(T242), void, T239)) :- ','(lessc19(T242), deletec1(s(T242), T237, T239)).
deletec1(T251, tree(T251, T252, void), T252).
deletec1(T275, tree(T275, T276, void), tree(T275, T278, void)) :- ','(lessc19(T275), deletec1(T275, T276, T278)).
deletec1(T291, tree(T291, T292, void), tree(T291, T292, T294)) :- qc40(T291, T294).
deletec1(s(T307), tree(s(T307), T300, void), tree(s(T307), T302, void)) :- ','(lessc19(T307), deletec1(s(T307), T300, T302)).
deletec1(T320, tree(T320, T321, void), tree(T320, T321, T323)) :- qc40(T320, T323).
deletec1(s(T334), tree(s(T334), T329, void), tree(s(T334), T329, T331)) :- qc33(T334, T331).
deletec1(T341, tree(T341, T342, tree(T356, void, T357)), tree(T356, T342, T357)).
deletec1(T341, tree(T341, T342, tree(T382, T383, T384)), tree(T388, T342, tree(T382, T389, T387))) :- delminc56(T383, T388, T389).
deletec1(T410, tree(T410, T411, T412), tree(T410, T414, T412)) :- ','(lessc19(T410), deletec1(T410, T411, T414)).
deletec1(T429, tree(T429, T430, T431), tree(T429, T430, T433)) :- ','(lessc19(T429), deletec1(T429, T431, T433)).
deletec1(0, tree(s(T455), T447, T448), tree(s(T455), T450, T448)) :- deletec1(0, T447, T450).
deletec1(s(T466), tree(s(T467), T447, T448), tree(s(T467), T450, T448)) :- ','(lessc164(T466, T467), deletec1(s(T466), T447, T450)).
deletec1(T594, tree(T595, T596, T597), tree(T595, T596, T599)) :- ','(lessc222(T595, T594), deletec1(T594, T597, T599)).
deletec1(s(T623), tree(0, T615, T616), tree(0, T615, T618)) :- deletec1(s(T623), T616, T618).
deletec1(s(T633), tree(s(T632), T615, T616), tree(s(T632), T615, T618)) :- ','(lessc222(T632, T633), deletec1(s(T633), T616, T618)).
lessc19(s(T33)) :- lessc19(T33).
qc17(T26, T28) :- ','(lessc19(T26), deletec1(T26, void, T28)).
qc33(T59, T54) :- ','(lessc19(T59), deletec1(s(T59), void, T54)).
delminc56(tree(T150, void, T151), T150, T151).
delminc56(tree(T164, T165, T166), T170, tree(T164, T171, T169)) :- delminc56(T165, T170, T171).
qc40(s(T84), T81) :- qc33(T84, T81).
qc71(T199, T200, T202) :- ','(lessc19(T199), deletec1(T199, T200, T202)).
lessc222(0, s(T571)).
lessc222(s(T576), s(T577)) :- lessc222(T576, T577).
lessc164(0, s(T476)).
lessc164(s(0), s(s(T489))).
lessc164(s(s(0)), s(s(s(T502)))).
lessc164(s(s(s(0))), s(s(s(s(T515))))).
lessc164(s(s(s(s(0)))), s(s(s(s(s(T528)))))).
lessc164(s(s(s(s(s(0))))), s(s(s(s(s(s(T541))))))).
lessc164(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T554)))))))).
lessc164(s(s(s(s(s(s(s(T559))))))), s(s(s(s(s(s(s(T560)))))))) :- lessc222(T559, T560).

Afs:

delete1(x1, x2, x3) = delete1(x1, x2)

(3) TriplesToPiDPProof (SOUND transformation)

We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
delete1_in: (b,b,f)
p17_in: (b,f)
less19_in: (b)
lessc19_in: (b)
p33_in: (b,f)
p40_in: (b,f)
delmin56_in: (b,f,f)
p71_in: (b,b,f)
less222_in: (b,b)
lessc164_in: (b,b)
lessc222_in: (b,b)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

DELETE1_IN_GGA(T26, tree(T26, void, void), tree(T26, T28, void)) → U14_GGA(T26, T28, p17_in_ga(T26, T28))
DELETE1_IN_GGA(T26, tree(T26, void, void), tree(T26, T28, void)) → P17_IN_GA(T26, T28)
P17_IN_GA(T26, T28) → U2_GA(T26, T28, less19_in_g(T26))
P17_IN_GA(T26, T28) → LESS19_IN_G(T26)
LESS19_IN_G(s(T33)) → U1_G(T33, less19_in_g(T33))
LESS19_IN_G(s(T33)) → LESS19_IN_G(T33)
P17_IN_GA(T26, T28) → U3_GA(T26, T28, lessc19_in_g(T26))
U3_GA(T26, T28, lessc19_out_g(T26)) → U4_GA(T26, T28, delete1_in_gga(T26, void, T28))
U3_GA(T26, T28, lessc19_out_g(T26)) → DELETE1_IN_GGA(T26, void, T28)
DELETE1_IN_GGA(T46, tree(T46, void, void), tree(T46, void, T48)) → U15_GGA(T46, T48, p17_in_ga(T46, T48))
DELETE1_IN_GGA(T46, tree(T46, void, void), tree(T46, void, T48)) → P17_IN_GA(T46, T48)
DELETE1_IN_GGA(s(T59), tree(s(T59), void, void), tree(s(T59), T54, void)) → U16_GGA(T59, T54, p33_in_ga(T59, T54))
DELETE1_IN_GGA(s(T59), tree(s(T59), void, void), tree(s(T59), T54, void)) → P33_IN_GA(T59, T54)
P33_IN_GA(T59, T54) → U5_GA(T59, T54, less19_in_g(T59))
P33_IN_GA(T59, T54) → LESS19_IN_G(T59)
P33_IN_GA(T59, T54) → U6_GA(T59, T54, lessc19_in_g(T59))
U6_GA(T59, T54, lessc19_out_g(T59)) → U7_GA(T59, T54, delete1_in_gga(s(T59), void, T54))
U6_GA(T59, T54, lessc19_out_g(T59)) → DELETE1_IN_GGA(s(T59), void, T54)
DELETE1_IN_GGA(T73, tree(T73, void, void), tree(T73, void, T75)) → U17_GGA(T73, T75, p17_in_ga(T73, T75))
DELETE1_IN_GGA(T79, tree(T79, void, void), tree(T79, void, T81)) → U18_GGA(T79, T81, p40_in_ga(T79, T81))
DELETE1_IN_GGA(T79, tree(T79, void, void), tree(T79, void, T81)) → P40_IN_GA(T79, T81)
P40_IN_GA(s(T84), T81) → U9_GA(T84, T81, p33_in_ga(T84, T81))
P40_IN_GA(s(T84), T81) → P33_IN_GA(T84, T81)
DELETE1_IN_GGA(T90, tree(T90, void, tree(T130, T131, T132)), tree(T136, void, tree(T130, T137, T135))) → U19_GGA(T90, T130, T131, T132, T136, T137, T135, delmin56_in_gaa(T131, T136, T137))
DELETE1_IN_GGA(T90, tree(T90, void, tree(T130, T131, T132)), tree(T136, void, tree(T130, T137, T135))) → DELMIN56_IN_GAA(T131, T136, T137)
DELMIN56_IN_GAA(tree(T164, T165, T166), T170, tree(T164, T171, T169)) → U8_GAA(T164, T165, T166, T170, T171, T169, delmin56_in_gaa(T165, T170, T171))
DELMIN56_IN_GAA(tree(T164, T165, T166), T170, tree(T164, T171, T169)) → DELMIN56_IN_GAA(T165, T170, T171)
DELETE1_IN_GGA(T188, tree(T188, void, T189), tree(T188, T191, T189)) → U20_GGA(T188, T189, T191, p40_in_ga(T188, T191))
DELETE1_IN_GGA(T188, tree(T188, void, T189), tree(T188, T191, T189)) → P40_IN_GA(T188, T191)
DELETE1_IN_GGA(T199, tree(T199, void, T200), tree(T199, void, T202)) → U21_GGA(T199, T200, T202, p71_in_gga(T199, T200, T202))
DELETE1_IN_GGA(T199, tree(T199, void, T200), tree(T199, void, T202)) → P71_IN_GGA(T199, T200, T202)
P71_IN_GGA(T199, T200, T202) → U10_GGA(T199, T200, T202, less19_in_g(T199))
P71_IN_GGA(T199, T200, T202) → LESS19_IN_G(T199)
P71_IN_GGA(T199, T200, T202) → U11_GGA(T199, T200, T202, lessc19_in_g(T199))
U11_GGA(T199, T200, T202, lessc19_out_g(T199)) → U12_GGA(T199, T200, T202, delete1_in_gga(T199, T200, T202))
U11_GGA(T199, T200, T202, lessc19_out_g(T199)) → DELETE1_IN_GGA(T199, T200, T202)
DELETE1_IN_GGA(s(T220), tree(s(T220), void, T213), tree(s(T220), T215, T213)) → U22_GGA(T220, T213, T215, p33_in_ga(T220, T215))
DELETE1_IN_GGA(s(T220), tree(s(T220), void, T213), tree(s(T220), T215, T213)) → P33_IN_GA(T220, T215)
DELETE1_IN_GGA(T228, tree(T228, void, T229), tree(T228, void, T231)) → U23_GGA(T228, T229, T231, p71_in_gga(T228, T229, T231))
DELETE1_IN_GGA(s(T242), tree(s(T242), void, T237), tree(s(T242), void, T239)) → U24_GGA(T242, T237, T239, less19_in_g(T242))
DELETE1_IN_GGA(s(T242), tree(s(T242), void, T237), tree(s(T242), void, T239)) → LESS19_IN_G(T242)
DELETE1_IN_GGA(s(T242), tree(s(T242), void, T237), tree(s(T242), void, T239)) → U25_GGA(T242, T237, T239, lessc19_in_g(T242))
U25_GGA(T242, T237, T239, lessc19_out_g(T242)) → U26_GGA(T242, T237, T239, delete1_in_gga(s(T242), T237, T239))
U25_GGA(T242, T237, T239, lessc19_out_g(T242)) → DELETE1_IN_GGA(s(T242), T237, T239)
DELETE1_IN_GGA(T275, tree(T275, T276, void), tree(T275, T278, void)) → U27_GGA(T275, T276, T278, less19_in_g(T275))
DELETE1_IN_GGA(T275, tree(T275, T276, void), tree(T275, T278, void)) → LESS19_IN_G(T275)
DELETE1_IN_GGA(T275, tree(T275, T276, void), tree(T275, T278, void)) → U28_GGA(T275, T276, T278, lessc19_in_g(T275))
U28_GGA(T275, T276, T278, lessc19_out_g(T275)) → U29_GGA(T275, T276, T278, delete1_in_gga(T275, T276, T278))
U28_GGA(T275, T276, T278, lessc19_out_g(T275)) → DELETE1_IN_GGA(T275, T276, T278)
DELETE1_IN_GGA(T291, tree(T291, T292, void), tree(T291, T292, T294)) → U30_GGA(T291, T292, T294, p40_in_ga(T291, T294))
DELETE1_IN_GGA(T291, tree(T291, T292, void), tree(T291, T292, T294)) → P40_IN_GA(T291, T294)
DELETE1_IN_GGA(s(T307), tree(s(T307), T300, void), tree(s(T307), T302, void)) → U31_GGA(T307, T300, T302, less19_in_g(T307))
DELETE1_IN_GGA(s(T307), tree(s(T307), T300, void), tree(s(T307), T302, void)) → LESS19_IN_G(T307)
DELETE1_IN_GGA(s(T307), tree(s(T307), T300, void), tree(s(T307), T302, void)) → U32_GGA(T307, T300, T302, lessc19_in_g(T307))
U32_GGA(T307, T300, T302, lessc19_out_g(T307)) → U33_GGA(T307, T300, T302, delete1_in_gga(s(T307), T300, T302))
U32_GGA(T307, T300, T302, lessc19_out_g(T307)) → DELETE1_IN_GGA(s(T307), T300, T302)
DELETE1_IN_GGA(T320, tree(T320, T321, void), tree(T320, T321, T323)) → U34_GGA(T320, T321, T323, p40_in_ga(T320, T323))
DELETE1_IN_GGA(s(T334), tree(s(T334), T329, void), tree(s(T334), T329, T331)) → U35_GGA(T334, T329, T331, p33_in_ga(T334, T331))
DELETE1_IN_GGA(s(T334), tree(s(T334), T329, void), tree(s(T334), T329, T331)) → P33_IN_GA(T334, T331)
DELETE1_IN_GGA(T341, tree(T341, T342, tree(T382, T383, T384)), tree(T388, T342, tree(T382, T389, T387))) → U36_GGA(T341, T342, T382, T383, T384, T388, T389, T387, delmin56_in_gaa(T383, T388, T389))
DELETE1_IN_GGA(T341, tree(T341, T342, tree(T382, T383, T384)), tree(T388, T342, tree(T382, T389, T387))) → DELMIN56_IN_GAA(T383, T388, T389)
DELETE1_IN_GGA(T410, tree(T410, T411, T412), tree(T410, T414, T412)) → U37_GGA(T410, T411, T412, T414, less19_in_g(T410))
DELETE1_IN_GGA(T410, tree(T410, T411, T412), tree(T410, T414, T412)) → LESS19_IN_G(T410)
DELETE1_IN_GGA(T410, tree(T410, T411, T412), tree(T410, T414, T412)) → U38_GGA(T410, T411, T412, T414, lessc19_in_g(T410))
U38_GGA(T410, T411, T412, T414, lessc19_out_g(T410)) → U39_GGA(T410, T411, T412, T414, delete1_in_gga(T410, T411, T414))
U38_GGA(T410, T411, T412, T414, lessc19_out_g(T410)) → DELETE1_IN_GGA(T410, T411, T414)
DELETE1_IN_GGA(T429, tree(T429, T430, T431), tree(T429, T430, T433)) → U40_GGA(T429, T430, T431, T433, less19_in_g(T429))
DELETE1_IN_GGA(T429, tree(T429, T430, T431), tree(T429, T430, T433)) → LESS19_IN_G(T429)
DELETE1_IN_GGA(T429, tree(T429, T430, T431), tree(T429, T430, T433)) → U41_GGA(T429, T430, T431, T433, lessc19_in_g(T429))
U41_GGA(T429, T430, T431, T433, lessc19_out_g(T429)) → U42_GGA(T429, T430, T431, T433, delete1_in_gga(T429, T431, T433))
U41_GGA(T429, T430, T431, T433, lessc19_out_g(T429)) → DELETE1_IN_GGA(T429, T431, T433)
DELETE1_IN_GGA(0, tree(s(T455), T447, T448), tree(s(T455), T450, T448)) → U43_GGA(T455, T447, T448, T450, delete1_in_gga(0, T447, T450))
DELETE1_IN_GGA(0, tree(s(T455), T447, T448), tree(s(T455), T450, T448)) → DELETE1_IN_GGA(0, T447, T450)
DELETE1_IN_GGA(s(s(s(s(s(s(s(s(T559)))))))), tree(s(s(s(s(s(s(s(s(T560)))))))), T447, T448), tree(s(s(s(s(s(s(s(s(T560)))))))), T450, T448)) → U44_GGA(T559, T560, T447, T448, T450, less222_in_gg(T559, T560))
DELETE1_IN_GGA(s(s(s(s(s(s(s(s(T559)))))))), tree(s(s(s(s(s(s(s(s(T560)))))))), T447, T448), tree(s(s(s(s(s(s(s(s(T560)))))))), T450, T448)) → LESS222_IN_GG(T559, T560)
LESS222_IN_GG(s(T576), s(T577)) → U13_GG(T576, T577, less222_in_gg(T576, T577))
LESS222_IN_GG(s(T576), s(T577)) → LESS222_IN_GG(T576, T577)
DELETE1_IN_GGA(s(T466), tree(s(T467), T447, T448), tree(s(T467), T450, T448)) → U45_GGA(T466, T467, T447, T448, T450, lessc164_in_gg(T466, T467))
U45_GGA(T466, T467, T447, T448, T450, lessc164_out_gg(T466, T467)) → U46_GGA(T466, T467, T447, T448, T450, delete1_in_gga(s(T466), T447, T450))
U45_GGA(T466, T467, T447, T448, T450, lessc164_out_gg(T466, T467)) → DELETE1_IN_GGA(s(T466), T447, T450)
DELETE1_IN_GGA(T594, tree(T595, T596, T597), tree(T595, T596, T599)) → U47_GGA(T594, T595, T596, T597, T599, less222_in_gg(T595, T594))
DELETE1_IN_GGA(T594, tree(T595, T596, T597), tree(T595, T596, T599)) → LESS222_IN_GG(T595, T594)
DELETE1_IN_GGA(T594, tree(T595, T596, T597), tree(T595, T596, T599)) → U48_GGA(T594, T595, T596, T597, T599, lessc222_in_gg(T595, T594))
U48_GGA(T594, T595, T596, T597, T599, lessc222_out_gg(T595, T594)) → U49_GGA(T594, T595, T596, T597, T599, delete1_in_gga(T594, T597, T599))
U48_GGA(T594, T595, T596, T597, T599, lessc222_out_gg(T595, T594)) → DELETE1_IN_GGA(T594, T597, T599)
DELETE1_IN_GGA(s(T623), tree(0, T615, T616), tree(0, T615, T618)) → U50_GGA(T623, T615, T616, T618, delete1_in_gga(s(T623), T616, T618))
DELETE1_IN_GGA(s(T623), tree(0, T615, T616), tree(0, T615, T618)) → DELETE1_IN_GGA(s(T623), T616, T618)
DELETE1_IN_GGA(s(T633), tree(s(T632), T615, T616), tree(s(T632), T615, T618)) → U51_GGA(T633, T632, T615, T616, T618, less222_in_gg(T632, T633))
DELETE1_IN_GGA(s(T633), tree(s(T632), T615, T616), tree(s(T632), T615, T618)) → LESS222_IN_GG(T632, T633)
DELETE1_IN_GGA(s(T633), tree(s(T632), T615, T616), tree(s(T632), T615, T618)) → U52_GGA(T633, T632, T615, T616, T618, lessc222_in_gg(T632, T633))
U52_GGA(T633, T632, T615, T616, T618, lessc222_out_gg(T632, T633)) → U53_GGA(T633, T632, T615, T616, T618, delete1_in_gga(s(T633), T616, T618))
U52_GGA(T633, T632, T615, T616, T618, lessc222_out_gg(T632, T633)) → DELETE1_IN_GGA(s(T633), T616, T618)

The TRS R consists of the following rules:

lessc19_in_g(s(T33)) → U87_g(T33, lessc19_in_g(T33))
U87_g(T33, lessc19_out_g(T33)) → lessc19_out_g(s(T33))
lessc164_in_gg(0, s(T476)) → lessc164_out_gg(0, s(T476))
lessc164_in_gg(s(0), s(s(T489))) → lessc164_out_gg(s(0), s(s(T489)))
lessc164_in_gg(s(s(0)), s(s(s(T502)))) → lessc164_out_gg(s(s(0)), s(s(s(T502))))
lessc164_in_gg(s(s(s(0))), s(s(s(s(T515))))) → lessc164_out_gg(s(s(s(0))), s(s(s(s(T515)))))
lessc164_in_gg(s(s(s(s(0)))), s(s(s(s(s(T528)))))) → lessc164_out_gg(s(s(s(s(0)))), s(s(s(s(s(T528))))))
lessc164_in_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T541))))))) → lessc164_out_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T541)))))))
lessc164_in_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T554)))))))) → lessc164_out_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T554))))))))
lessc164_in_gg(s(s(s(s(s(s(s(T559))))))), s(s(s(s(s(s(s(T560)))))))) → U97_gg(T559, T560, lessc222_in_gg(T559, T560))
lessc222_in_gg(0, s(T571)) → lessc222_out_gg(0, s(T571))
lessc222_in_gg(s(T576), s(T577)) → U96_gg(T576, T577, lessc222_in_gg(T576, T577))
U96_gg(T576, T577, lessc222_out_gg(T576, T577)) → lessc222_out_gg(s(T576), s(T577))
U97_gg(T559, T560, lessc222_out_gg(T559, T560)) → lessc164_out_gg(s(s(s(s(s(s(s(T559))))))), s(s(s(s(s(s(s(T560))))))))

The argument filtering Pi contains the following mapping:
delete1_in_gga(x1, x2, x3) = delete1_in_gga(x1, x2)
tree(x1, x2, x3) = tree(x1, x2, x3)
void = void
p17_in_ga(x1, x2) = p17_in_ga(x1)
less19_in_g(x1) = less19_in_g(x1)
s(x1) = s(x1)
lessc19_in_g(x1) = lessc19_in_g(x1)
U87_g(x1, x2) = U87_g(x1, x2)
lessc19_out_g(x1) = lessc19_out_g(x1)
p33_in_ga(x1, x2) = p33_in_ga(x1)
p40_in_ga(x1, x2) = p40_in_ga(x1)
delmin56_in_gaa(x1, x2, x3) = delmin56_in_gaa(x1)
p71_in_gga(x1, x2, x3) = p71_in_gga(x1, x2)
0 = 0
less222_in_gg(x1, x2) = less222_in_gg(x1, x2)
lessc164_in_gg(x1, x2) = lessc164_in_gg(x1, x2)
lessc164_out_gg(x1, x2) = lessc164_out_gg(x1, x2)
U97_gg(x1, x2, x3) = U97_gg(x1, x2, x3)
lessc222_in_gg(x1, x2) = lessc222_in_gg(x1, x2)
lessc222_out_gg(x1, x2) = lessc222_out_gg(x1, x2)
U96_gg(x1, x2, x3) = U96_gg(x1, x2, x3)
DELETE1_IN_GGA(x1, x2, x3) = DELETE1_IN_GGA(x1, x2)
U14_GGA(x1, x2, x3) = U14_GGA(x1, x3)
P17_IN_GA(x1, x2) = P17_IN_GA(x1)
U2_GA(x1, x2, x3) = U2_GA(x1, x3)
LESS19_IN_G(x1) = LESS19_IN_G(x1)
U1_G(x1, x2) = U1_G(x1, x2)
U3_GA(x1, x2, x3) = U3_GA(x1, x3)
U4_GA(x1, x2, x3) = U4_GA(x1, x3)
U15_GGA(x1, x2, x3) = U15_GGA(x1, x3)
U16_GGA(x1, x2, x3) = U16_GGA(x1, x3)
P33_IN_GA(x1, x2) = P33_IN_GA(x1)
U5_GA(x1, x2, x3) = U5_GA(x1, x3)
U6_GA(x1, x2, x3) = U6_GA(x1, x3)
U7_GA(x1, x2, x3) = U7_GA(x1, x3)
U17_GGA(x1, x2, x3) = U17_GGA(x1, x3)
U18_GGA(x1, x2, x3) = U18_GGA(x1, x3)
P40_IN_GA(x1, x2) = P40_IN_GA(x1)
U9_GA(x1, x2, x3) = U9_GA(x1, x3)
U19_GGA(x1, x2, x3, x4, x5, x6, x7, x8) = U19_GGA(x1, x2, x3, x4, x8)
DELMIN56_IN_GAA(x1, x2, x3) = DELMIN56_IN_GAA(x1)
U8_GAA(x1, x2, x3, x4, x5, x6, x7) = U8_GAA(x1, x2, x3, x7)
U20_GGA(x1, x2, x3, x4) = U20_GGA(x1, x2, x4)
U21_GGA(x1, x2, x3, x4) = U21_GGA(x1, x2, x4)
P71_IN_GGA(x1, x2, x3) = P71_IN_GGA(x1, x2)
U10_GGA(x1, x2, x3, x4) = U10_GGA(x1, x2, x4)
U11_GGA(x1, x2, x3, x4) = U11_GGA(x1, x2, x4)
U12_GGA(x1, x2, x3, x4) = U12_GGA(x1, x2, x4)
U22_GGA(x1, x2, x3, x4) = U22_GGA(x1, x2, x4)
U23_GGA(x1, x2, x3, x4) = U23_GGA(x1, x2, x4)
U24_GGA(x1, x2, x3, x4) = U24_GGA(x1, x2, x4)
U25_GGA(x1, x2, x3, x4) = U25_GGA(x1, x2, x4)
U26_GGA(x1, x2, x3, x4) = U26_GGA(x1, x2, x4)
U27_GGA(x1, x2, x3, x4) = U27_GGA(x1, x2, x4)
U28_GGA(x1, x2, x3, x4) = U28_GGA(x1, x2, x4)
U29_GGA(x1, x2, x3, x4) = U29_GGA(x1, x2, x4)
U30_GGA(x1, x2, x3, x4) = U30_GGA(x1, x2, x4)
U31_GGA(x1, x2, x3, x4) = U31_GGA(x1, x2, x4)
U32_GGA(x1, x2, x3, x4) = U32_GGA(x1, x2, x4)
U33_GGA(x1, x2, x3, x4) = U33_GGA(x1, x2, x4)
U34_GGA(x1, x2, x3, x4) = U34_GGA(x1, x2, x4)
U35_GGA(x1, x2, x3, x4) = U35_GGA(x1, x2, x4)
U36_GGA(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U36_GGA(x1, x2, x3, x4, x5, x9)
U37_GGA(x1, x2, x3, x4, x5) = U37_GGA(x1, x2, x3, x5)
U38_GGA(x1, x2, x3, x4, x5) = U38_GGA(x1, x2, x3, x5)
U39_GGA(x1, x2, x3, x4, x5) = U39_GGA(x1, x2, x3, x5)
U40_GGA(x1, x2, x3, x4, x5) = U40_GGA(x1, x2, x3, x5)
U41_GGA(x1, x2, x3, x4, x5) = U41_GGA(x1, x2, x3, x5)
U42_GGA(x1, x2, x3, x4, x5) = U42_GGA(x1, x2, x3, x5)
U43_GGA(x1, x2, x3, x4, x5) = U43_GGA(x1, x2, x3, x5)
U44_GGA(x1, x2, x3, x4, x5, x6) = U44_GGA(x1, x2, x3, x4, x6)
LESS222_IN_GG(x1, x2) = LESS222_IN_GG(x1, x2)
U13_GG(x1, x2, x3) = U13_GG(x1, x2, x3)
U45_GGA(x1, x2, x3, x4, x5, x6) = U45_GGA(x1, x2, x3, x4, x6)
U46_GGA(x1, x2, x3, x4, x5, x6) = U46_GGA(x1, x2, x3, x4, x6)
U47_GGA(x1, x2, x3, x4, x5, x6) = U47_GGA(x1, x2, x3, x4, x6)
U48_GGA(x1, x2, x3, x4, x5, x6) = U48_GGA(x1, x2, x3, x4, x6)
U49_GGA(x1, x2, x3, x4, x5, x6) = U49_GGA(x1, x2, x3, x4, x6)
U50_GGA(x1, x2, x3, x4, x5) = U50_GGA(x1, x2, x3, x5)
U51_GGA(x1, x2, x3, x4, x5, x6) = U51_GGA(x1, x2, x3, x4, x6)
U52_GGA(x1, x2, x3, x4, x5, x6) = U52_GGA(x1, x2, x3, x4, x6)
U53_GGA(x1, x2, x3, x4, x5, x6) = U53_GGA(x1, x2, x3, x4, x6)

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

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(4) Obligation:

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

DELETE1_IN_GGA(T26, tree(T26, void, void), tree(T26, T28, void)) → U14_GGA(T26, T28, p17_in_ga(T26, T28))
DELETE1_IN_GGA(T26, tree(T26, void, void), tree(T26, T28, void)) → P17_IN_GA(T26, T28)
P17_IN_GA(T26, T28) → U2_GA(T26, T28, less19_in_g(T26))
P17_IN_GA(T26, T28) → LESS19_IN_G(T26)
LESS19_IN_G(s(T33)) → U1_G(T33, less19_in_g(T33))
LESS19_IN_G(s(T33)) → LESS19_IN_G(T33)
P17_IN_GA(T26, T28) → U3_GA(T26, T28, lessc19_in_g(T26))
U3_GA(T26, T28, lessc19_out_g(T26)) → U4_GA(T26, T28, delete1_in_gga(T26, void, T28))
U3_GA(T26, T28, lessc19_out_g(T26)) → DELETE1_IN_GGA(T26, void, T28)
DELETE1_IN_GGA(T46, tree(T46, void, void), tree(T46, void, T48)) → U15_GGA(T46, T48, p17_in_ga(T46, T48))
DELETE1_IN_GGA(T46, tree(T46, void, void), tree(T46, void, T48)) → P17_IN_GA(T46, T48)
DELETE1_IN_GGA(s(T59), tree(s(T59), void, void), tree(s(T59), T54, void)) → U16_GGA(T59, T54, p33_in_ga(T59, T54))
DELETE1_IN_GGA(s(T59), tree(s(T59), void, void), tree(s(T59), T54, void)) → P33_IN_GA(T59, T54)
P33_IN_GA(T59, T54) → U5_GA(T59, T54, less19_in_g(T59))
P33_IN_GA(T59, T54) → LESS19_IN_G(T59)
P33_IN_GA(T59, T54) → U6_GA(T59, T54, lessc19_in_g(T59))
U6_GA(T59, T54, lessc19_out_g(T59)) → U7_GA(T59, T54, delete1_in_gga(s(T59), void, T54))
U6_GA(T59, T54, lessc19_out_g(T59)) → DELETE1_IN_GGA(s(T59), void, T54)
DELETE1_IN_GGA(T73, tree(T73, void, void), tree(T73, void, T75)) → U17_GGA(T73, T75, p17_in_ga(T73, T75))
DELETE1_IN_GGA(T79, tree(T79, void, void), tree(T79, void, T81)) → U18_GGA(T79, T81, p40_in_ga(T79, T81))
DELETE1_IN_GGA(T79, tree(T79, void, void), tree(T79, void, T81)) → P40_IN_GA(T79, T81)
P40_IN_GA(s(T84), T81) → U9_GA(T84, T81, p33_in_ga(T84, T81))
P40_IN_GA(s(T84), T81) → P33_IN_GA(T84, T81)
DELETE1_IN_GGA(T90, tree(T90, void, tree(T130, T131, T132)), tree(T136, void, tree(T130, T137, T135))) → U19_GGA(T90, T130, T131, T132, T136, T137, T135, delmin56_in_gaa(T131, T136, T137))
DELETE1_IN_GGA(T90, tree(T90, void, tree(T130, T131, T132)), tree(T136, void, tree(T130, T137, T135))) → DELMIN56_IN_GAA(T131, T136, T137)
DELMIN56_IN_GAA(tree(T164, T165, T166), T170, tree(T164, T171, T169)) → U8_GAA(T164, T165, T166, T170, T171, T169, delmin56_in_gaa(T165, T170, T171))
DELMIN56_IN_GAA(tree(T164, T165, T166), T170, tree(T164, T171, T169)) → DELMIN56_IN_GAA(T165, T170, T171)
DELETE1_IN_GGA(T188, tree(T188, void, T189), tree(T188, T191, T189)) → U20_GGA(T188, T189, T191, p40_in_ga(T188, T191))
DELETE1_IN_GGA(T188, tree(T188, void, T189), tree(T188, T191, T189)) → P40_IN_GA(T188, T191)
DELETE1_IN_GGA(T199, tree(T199, void, T200), tree(T199, void, T202)) → U21_GGA(T199, T200, T202, p71_in_gga(T199, T200, T202))
DELETE1_IN_GGA(T199, tree(T199, void, T200), tree(T199, void, T202)) → P71_IN_GGA(T199, T200, T202)
P71_IN_GGA(T199, T200, T202) → U10_GGA(T199, T200, T202, less19_in_g(T199))
P71_IN_GGA(T199, T200, T202) → LESS19_IN_G(T199)
P71_IN_GGA(T199, T200, T202) → U11_GGA(T199, T200, T202, lessc19_in_g(T199))
U11_GGA(T199, T200, T202, lessc19_out_g(T199)) → U12_GGA(T199, T200, T202, delete1_in_gga(T199, T200, T202))
U11_GGA(T199, T200, T202, lessc19_out_g(T199)) → DELETE1_IN_GGA(T199, T200, T202)
DELETE1_IN_GGA(s(T220), tree(s(T220), void, T213), tree(s(T220), T215, T213)) → U22_GGA(T220, T213, T215, p33_in_ga(T220, T215))
DELETE1_IN_GGA(s(T220), tree(s(T220), void, T213), tree(s(T220), T215, T213)) → P33_IN_GA(T220, T215)
DELETE1_IN_GGA(T228, tree(T228, void, T229), tree(T228, void, T231)) → U23_GGA(T228, T229, T231, p71_in_gga(T228, T229, T231))
DELETE1_IN_GGA(s(T242), tree(s(T242), void, T237), tree(s(T242), void, T239)) → U24_GGA(T242, T237, T239, less19_in_g(T242))
DELETE1_IN_GGA(s(T242), tree(s(T242), void, T237), tree(s(T242), void, T239)) → LESS19_IN_G(T242)
DELETE1_IN_GGA(s(T242), tree(s(T242), void, T237), tree(s(T242), void, T239)) → U25_GGA(T242, T237, T239, lessc19_in_g(T242))
U25_GGA(T242, T237, T239, lessc19_out_g(T242)) → U26_GGA(T242, T237, T239, delete1_in_gga(s(T242), T237, T239))
U25_GGA(T242, T237, T239, lessc19_out_g(T242)) → DELETE1_IN_GGA(s(T242), T237, T239)
DELETE1_IN_GGA(T275, tree(T275, T276, void), tree(T275, T278, void)) → U27_GGA(T275, T276, T278, less19_in_g(T275))
DELETE1_IN_GGA(T275, tree(T275, T276, void), tree(T275, T278, void)) → LESS19_IN_G(T275)
DELETE1_IN_GGA(T275, tree(T275, T276, void), tree(T275, T278, void)) → U28_GGA(T275, T276, T278, lessc19_in_g(T275))
U28_GGA(T275, T276, T278, lessc19_out_g(T275)) → U29_GGA(T275, T276, T278, delete1_in_gga(T275, T276, T278))
U28_GGA(T275, T276, T278, lessc19_out_g(T275)) → DELETE1_IN_GGA(T275, T276, T278)
DELETE1_IN_GGA(T291, tree(T291, T292, void), tree(T291, T292, T294)) → U30_GGA(T291, T292, T294, p40_in_ga(T291, T294))
DELETE1_IN_GGA(T291, tree(T291, T292, void), tree(T291, T292, T294)) → P40_IN_GA(T291, T294)
DELETE1_IN_GGA(s(T307), tree(s(T307), T300, void), tree(s(T307), T302, void)) → U31_GGA(T307, T300, T302, less19_in_g(T307))
DELETE1_IN_GGA(s(T307), tree(s(T307), T300, void), tree(s(T307), T302, void)) → LESS19_IN_G(T307)
DELETE1_IN_GGA(s(T307), tree(s(T307), T300, void), tree(s(T307), T302, void)) → U32_GGA(T307, T300, T302, lessc19_in_g(T307))
U32_GGA(T307, T300, T302, lessc19_out_g(T307)) → U33_GGA(T307, T300, T302, delete1_in_gga(s(T307), T300, T302))
U32_GGA(T307, T300, T302, lessc19_out_g(T307)) → DELETE1_IN_GGA(s(T307), T300, T302)
DELETE1_IN_GGA(T320, tree(T320, T321, void), tree(T320, T321, T323)) → U34_GGA(T320, T321, T323, p40_in_ga(T320, T323))
DELETE1_IN_GGA(s(T334), tree(s(T334), T329, void), tree(s(T334), T329, T331)) → U35_GGA(T334, T329, T331, p33_in_ga(T334, T331))
DELETE1_IN_GGA(s(T334), tree(s(T334), T329, void), tree(s(T334), T329, T331)) → P33_IN_GA(T334, T331)
DELETE1_IN_GGA(T341, tree(T341, T342, tree(T382, T383, T384)), tree(T388, T342, tree(T382, T389, T387))) → U36_GGA(T341, T342, T382, T383, T384, T388, T389, T387, delmin56_in_gaa(T383, T388, T389))
DELETE1_IN_GGA(T341, tree(T341, T342, tree(T382, T383, T384)), tree(T388, T342, tree(T382, T389, T387))) → DELMIN56_IN_GAA(T383, T388, T389)
DELETE1_IN_GGA(T410, tree(T410, T411, T412), tree(T410, T414, T412)) → U37_GGA(T410, T411, T412, T414, less19_in_g(T410))
DELETE1_IN_GGA(T410, tree(T410, T411, T412), tree(T410, T414, T412)) → LESS19_IN_G(T410)
DELETE1_IN_GGA(T410, tree(T410, T411, T412), tree(T410, T414, T412)) → U38_GGA(T410, T411, T412, T414, lessc19_in_g(T410))
U38_GGA(T410, T411, T412, T414, lessc19_out_g(T410)) → U39_GGA(T410, T411, T412, T414, delete1_in_gga(T410, T411, T414))
U38_GGA(T410, T411, T412, T414, lessc19_out_g(T410)) → DELETE1_IN_GGA(T410, T411, T414)
DELETE1_IN_GGA(T429, tree(T429, T430, T431), tree(T429, T430, T433)) → U40_GGA(T429, T430, T431, T433, less19_in_g(T429))
DELETE1_IN_GGA(T429, tree(T429, T430, T431), tree(T429, T430, T433)) → LESS19_IN_G(T429)
DELETE1_IN_GGA(T429, tree(T429, T430, T431), tree(T429, T430, T433)) → U41_GGA(T429, T430, T431, T433, lessc19_in_g(T429))
U41_GGA(T429, T430, T431, T433, lessc19_out_g(T429)) → U42_GGA(T429, T430, T431, T433, delete1_in_gga(T429, T431, T433))
U41_GGA(T429, T430, T431, T433, lessc19_out_g(T429)) → DELETE1_IN_GGA(T429, T431, T433)
DELETE1_IN_GGA(0, tree(s(T455), T447, T448), tree(s(T455), T450, T448)) → U43_GGA(T455, T447, T448, T450, delete1_in_gga(0, T447, T450))
DELETE1_IN_GGA(0, tree(s(T455), T447, T448), tree(s(T455), T450, T448)) → DELETE1_IN_GGA(0, T447, T450)
DELETE1_IN_GGA(s(s(s(s(s(s(s(s(T559)))))))), tree(s(s(s(s(s(s(s(s(T560)))))))), T447, T448), tree(s(s(s(s(s(s(s(s(T560)))))))), T450, T448)) → U44_GGA(T559, T560, T447, T448, T450, less222_in_gg(T559, T560))
DELETE1_IN_GGA(s(s(s(s(s(s(s(s(T559)))))))), tree(s(s(s(s(s(s(s(s(T560)))))))), T447, T448), tree(s(s(s(s(s(s(s(s(T560)))))))), T450, T448)) → LESS222_IN_GG(T559, T560)
LESS222_IN_GG(s(T576), s(T577)) → U13_GG(T576, T577, less222_in_gg(T576, T577))
LESS222_IN_GG(s(T576), s(T577)) → LESS222_IN_GG(T576, T577)
DELETE1_IN_GGA(s(T466), tree(s(T467), T447, T448), tree(s(T467), T450, T448)) → U45_GGA(T466, T467, T447, T448, T450, lessc164_in_gg(T466, T467))
U45_GGA(T466, T467, T447, T448, T450, lessc164_out_gg(T466, T467)) → U46_GGA(T466, T467, T447, T448, T450, delete1_in_gga(s(T466), T447, T450))
U45_GGA(T466, T467, T447, T448, T450, lessc164_out_gg(T466, T467)) → DELETE1_IN_GGA(s(T466), T447, T450)
DELETE1_IN_GGA(T594, tree(T595, T596, T597), tree(T595, T596, T599)) → U47_GGA(T594, T595, T596, T597, T599, less222_in_gg(T595, T594))
DELETE1_IN_GGA(T594, tree(T595, T596, T597), tree(T595, T596, T599)) → LESS222_IN_GG(T595, T594)
DELETE1_IN_GGA(T594, tree(T595, T596, T597), tree(T595, T596, T599)) → U48_GGA(T594, T595, T596, T597, T599, lessc222_in_gg(T595, T594))
U48_GGA(T594, T595, T596, T597, T599, lessc222_out_gg(T595, T594)) → U49_GGA(T594, T595, T596, T597, T599, delete1_in_gga(T594, T597, T599))
U48_GGA(T594, T595, T596, T597, T599, lessc222_out_gg(T595, T594)) → DELETE1_IN_GGA(T594, T597, T599)
DELETE1_IN_GGA(s(T623), tree(0, T615, T616), tree(0, T615, T618)) → U50_GGA(T623, T615, T616, T618, delete1_in_gga(s(T623), T616, T618))
DELETE1_IN_GGA(s(T623), tree(0, T615, T616), tree(0, T615, T618)) → DELETE1_IN_GGA(s(T623), T616, T618)
DELETE1_IN_GGA(s(T633), tree(s(T632), T615, T616), tree(s(T632), T615, T618)) → U51_GGA(T633, T632, T615, T616, T618, less222_in_gg(T632, T633))
DELETE1_IN_GGA(s(T633), tree(s(T632), T615, T616), tree(s(T632), T615, T618)) → LESS222_IN_GG(T632, T633)
DELETE1_IN_GGA(s(T633), tree(s(T632), T615, T616), tree(s(T632), T615, T618)) → U52_GGA(T633, T632, T615, T616, T618, lessc222_in_gg(T632, T633))
U52_GGA(T633, T632, T615, T616, T618, lessc222_out_gg(T632, T633)) → U53_GGA(T633, T632, T615, T616, T618, delete1_in_gga(s(T633), T616, T618))
U52_GGA(T633, T632, T615, T616, T618, lessc222_out_gg(T632, T633)) → DELETE1_IN_GGA(s(T633), T616, T618)

The TRS R consists of the following rules:

lessc19_in_g(s(T33)) → U87_g(T33, lessc19_in_g(T33))
U87_g(T33, lessc19_out_g(T33)) → lessc19_out_g(s(T33))
lessc164_in_gg(0, s(T476)) → lessc164_out_gg(0, s(T476))
lessc164_in_gg(s(0), s(s(T489))) → lessc164_out_gg(s(0), s(s(T489)))
lessc164_in_gg(s(s(0)), s(s(s(T502)))) → lessc164_out_gg(s(s(0)), s(s(s(T502))))
lessc164_in_gg(s(s(s(0))), s(s(s(s(T515))))) → lessc164_out_gg(s(s(s(0))), s(s(s(s(T515)))))
lessc164_in_gg(s(s(s(s(0)))), s(s(s(s(s(T528)))))) → lessc164_out_gg(s(s(s(s(0)))), s(s(s(s(s(T528))))))
lessc164_in_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T541))))))) → lessc164_out_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T541)))))))
lessc164_in_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T554)))))))) → lessc164_out_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T554))))))))
lessc164_in_gg(s(s(s(s(s(s(s(T559))))))), s(s(s(s(s(s(s(T560)))))))) → U97_gg(T559, T560, lessc222_in_gg(T559, T560))
lessc222_in_gg(0, s(T571)) → lessc222_out_gg(0, s(T571))
lessc222_in_gg(s(T576), s(T577)) → U96_gg(T576, T577, lessc222_in_gg(T576, T577))
U96_gg(T576, T577, lessc222_out_gg(T576, T577)) → lessc222_out_gg(s(T576), s(T577))
U97_gg(T559, T560, lessc222_out_gg(T559, T560)) → lessc164_out_gg(s(s(s(s(s(s(s(T559))))))), s(s(s(s(s(s(s(T560))))))))

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 4 SCCs with 68 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

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

LESS222_IN_GG(s(T576), s(T577)) → LESS222_IN_GG(T576, T577)

The TRS R consists of the following rules:

lessc19_in_g(s(T33)) → U87_g(T33, lessc19_in_g(T33))
U87_g(T33, lessc19_out_g(T33)) → lessc19_out_g(s(T33))
lessc164_in_gg(0, s(T476)) → lessc164_out_gg(0, s(T476))
lessc164_in_gg(s(0), s(s(T489))) → lessc164_out_gg(s(0), s(s(T489)))
lessc164_in_gg(s(s(0)), s(s(s(T502)))) → lessc164_out_gg(s(s(0)), s(s(s(T502))))
lessc164_in_gg(s(s(s(0))), s(s(s(s(T515))))) → lessc164_out_gg(s(s(s(0))), s(s(s(s(T515)))))
lessc164_in_gg(s(s(s(s(0)))), s(s(s(s(s(T528)))))) → lessc164_out_gg(s(s(s(s(0)))), s(s(s(s(s(T528))))))
lessc164_in_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T541))))))) → lessc164_out_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T541)))))))
lessc164_in_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T554)))))))) → lessc164_out_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T554))))))))
lessc164_in_gg(s(s(s(s(s(s(s(T559))))))), s(s(s(s(s(s(s(T560)))))))) → U97_gg(T559, T560, lessc222_in_gg(T559, T560))
lessc222_in_gg(0, s(T571)) → lessc222_out_gg(0, s(T571))
lessc222_in_gg(s(T576), s(T577)) → U96_gg(T576, T577, lessc222_in_gg(T576, T577))
U96_gg(T576, T577, lessc222_out_gg(T576, T577)) → lessc222_out_gg(s(T576), s(T577))
U97_gg(T559, T560, lessc222_out_gg(T559, T560)) → lessc164_out_gg(s(s(s(s(s(s(s(T559))))))), s(s(s(s(s(s(s(T560))))))))

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

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

LESS222_IN_GG(s(T576), s(T577)) → LESS222_IN_GG(T576, T577)

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

(10) PiDPToQDPProof (EQUIVALENT 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:

LESS222_IN_GG(s(T576), s(T577)) → LESS222_IN_GG(T576, T577)

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:

LESS222_IN_GG(s(T576), s(T577)) → LESS222_IN_GG(T576, T577)
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:

DELMIN56_IN_GAA(tree(T164, T165, T166), T170, tree(T164, T171, T169)) → DELMIN56_IN_GAA(T165, T170, T171)

The TRS R consists of the following rules:

lessc19_in_g(s(T33)) → U87_g(T33, lessc19_in_g(T33))
U87_g(T33, lessc19_out_g(T33)) → lessc19_out_g(s(T33))
lessc164_in_gg(0, s(T476)) → lessc164_out_gg(0, s(T476))
lessc164_in_gg(s(0), s(s(T489))) → lessc164_out_gg(s(0), s(s(T489)))
lessc164_in_gg(s(s(0)), s(s(s(T502)))) → lessc164_out_gg(s(s(0)), s(s(s(T502))))
lessc164_in_gg(s(s(s(0))), s(s(s(s(T515))))) → lessc164_out_gg(s(s(s(0))), s(s(s(s(T515)))))
lessc164_in_gg(s(s(s(s(0)))), s(s(s(s(s(T528)))))) → lessc164_out_gg(s(s(s(s(0)))), s(s(s(s(s(T528))))))
lessc164_in_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T541))))))) → lessc164_out_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T541)))))))
lessc164_in_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T554)))))))) → lessc164_out_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T554))))))))
lessc164_in_gg(s(s(s(s(s(s(s(T559))))))), s(s(s(s(s(s(s(T560)))))))) → U97_gg(T559, T560, lessc222_in_gg(T559, T560))
lessc222_in_gg(0, s(T571)) → lessc222_out_gg(0, s(T571))
lessc222_in_gg(s(T576), s(T577)) → U96_gg(T576, T577, lessc222_in_gg(T576, T577))
U96_gg(T576, T577, lessc222_out_gg(T576, T577)) → lessc222_out_gg(s(T576), s(T577))
U97_gg(T559, T560, lessc222_out_gg(T559, T560)) → lessc164_out_gg(s(s(s(s(s(s(s(T559))))))), s(s(s(s(s(s(s(T560))))))))

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3) = tree(x1, x2, x3)
s(x1) = s(x1)
lessc19_in_g(x1) = lessc19_in_g(x1)
U87_g(x1, x2) = U87_g(x1, x2)
lessc19_out_g(x1) = lessc19_out_g(x1)
0 = 0
lessc164_in_gg(x1, x2) = lessc164_in_gg(x1, x2)
lessc164_out_gg(x1, x2) = lessc164_out_gg(x1, x2)
U97_gg(x1, x2, x3) = U97_gg(x1, x2, x3)
lessc222_in_gg(x1, x2) = lessc222_in_gg(x1, x2)
lessc222_out_gg(x1, x2) = lessc222_out_gg(x1, x2)
U96_gg(x1, x2, x3) = U96_gg(x1, x2, x3)
DELMIN56_IN_GAA(x1, x2, x3) = DELMIN56_IN_GAA(x1)

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:

DELMIN56_IN_GAA(tree(T164, T165, T166), T170, tree(T164, T171, T169)) → DELMIN56_IN_GAA(T165, T170, T171)

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

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:

DELMIN56_IN_GAA(tree(T164, T165, T166)) → DELMIN56_IN_GAA(T165)

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

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

DELMIN56_IN_GAA(tree(T164, T165, T166)) → DELMIN56_IN_GAA(T165)
The graph contains the following edges 1 > 1

(20) YES

(21) Obligation:

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

LESS19_IN_G(s(T33)) → LESS19_IN_G(T33)

The TRS R consists of the following rules:

lessc19_in_g(s(T33)) → U87_g(T33, lessc19_in_g(T33))
U87_g(T33, lessc19_out_g(T33)) → lessc19_out_g(s(T33))
lessc164_in_gg(0, s(T476)) → lessc164_out_gg(0, s(T476))
lessc164_in_gg(s(0), s(s(T489))) → lessc164_out_gg(s(0), s(s(T489)))
lessc164_in_gg(s(s(0)), s(s(s(T502)))) → lessc164_out_gg(s(s(0)), s(s(s(T502))))
lessc164_in_gg(s(s(s(0))), s(s(s(s(T515))))) → lessc164_out_gg(s(s(s(0))), s(s(s(s(T515)))))
lessc164_in_gg(s(s(s(s(0)))), s(s(s(s(s(T528)))))) → lessc164_out_gg(s(s(s(s(0)))), s(s(s(s(s(T528))))))
lessc164_in_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T541))))))) → lessc164_out_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T541)))))))
lessc164_in_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T554)))))))) → lessc164_out_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T554))))))))
lessc164_in_gg(s(s(s(s(s(s(s(T559))))))), s(s(s(s(s(s(s(T560)))))))) → U97_gg(T559, T560, lessc222_in_gg(T559, T560))
lessc222_in_gg(0, s(T571)) → lessc222_out_gg(0, s(T571))
lessc222_in_gg(s(T576), s(T577)) → U96_gg(T576, T577, lessc222_in_gg(T576, T577))
U96_gg(T576, T577, lessc222_out_gg(T576, T577)) → lessc222_out_gg(s(T576), s(T577))
U97_gg(T559, T560, lessc222_out_gg(T559, T560)) → lessc164_out_gg(s(s(s(s(s(s(s(T559))))))), s(s(s(s(s(s(s(T560))))))))

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

(22) UsableRulesProof (EQUIVALENT transformation)

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

(23) Obligation:

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

LESS19_IN_G(s(T33)) → LESS19_IN_G(T33)

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

(24) PiDPToQDPProof (EQUIVALENT transformation)

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

(25) Obligation:

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

LESS19_IN_G(s(T33)) → LESS19_IN_G(T33)

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

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

LESS19_IN_G(s(T33)) → LESS19_IN_G(T33)
The graph contains the following edges 1 > 1

(27) YES

(28) Obligation:

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

DELETE1_IN_GGA(T199, tree(T199, void, T200), tree(T199, void, T202)) → P71_IN_GGA(T199, T200, T202)
P71_IN_GGA(T199, T200, T202) → U11_GGA(T199, T200, T202, lessc19_in_g(T199))
U11_GGA(T199, T200, T202, lessc19_out_g(T199)) → DELETE1_IN_GGA(T199, T200, T202)
DELETE1_IN_GGA(s(T242), tree(s(T242), void, T237), tree(s(T242), void, T239)) → U25_GGA(T242, T237, T239, lessc19_in_g(T242))
U25_GGA(T242, T237, T239, lessc19_out_g(T242)) → DELETE1_IN_GGA(s(T242), T237, T239)
DELETE1_IN_GGA(T275, tree(T275, T276, void), tree(T275, T278, void)) → U28_GGA(T275, T276, T278, lessc19_in_g(T275))
U28_GGA(T275, T276, T278, lessc19_out_g(T275)) → DELETE1_IN_GGA(T275, T276, T278)
DELETE1_IN_GGA(s(T307), tree(s(T307), T300, void), tree(s(T307), T302, void)) → U32_GGA(T307, T300, T302, lessc19_in_g(T307))
U32_GGA(T307, T300, T302, lessc19_out_g(T307)) → DELETE1_IN_GGA(s(T307), T300, T302)
DELETE1_IN_GGA(T410, tree(T410, T411, T412), tree(T410, T414, T412)) → U38_GGA(T410, T411, T412, T414, lessc19_in_g(T410))
U38_GGA(T410, T411, T412, T414, lessc19_out_g(T410)) → DELETE1_IN_GGA(T410, T411, T414)
DELETE1_IN_GGA(T429, tree(T429, T430, T431), tree(T429, T430, T433)) → U41_GGA(T429, T430, T431, T433, lessc19_in_g(T429))
U41_GGA(T429, T430, T431, T433, lessc19_out_g(T429)) → DELETE1_IN_GGA(T429, T431, T433)
DELETE1_IN_GGA(0, tree(s(T455), T447, T448), tree(s(T455), T450, T448)) → DELETE1_IN_GGA(0, T447, T450)
DELETE1_IN_GGA(T594, tree(T595, T596, T597), tree(T595, T596, T599)) → U48_GGA(T594, T595, T596, T597, T599, lessc222_in_gg(T595, T594))
U48_GGA(T594, T595, T596, T597, T599, lessc222_out_gg(T595, T594)) → DELETE1_IN_GGA(T594, T597, T599)
DELETE1_IN_GGA(s(T466), tree(s(T467), T447, T448), tree(s(T467), T450, T448)) → U45_GGA(T466, T467, T447, T448, T450, lessc164_in_gg(T466, T467))
U45_GGA(T466, T467, T447, T448, T450, lessc164_out_gg(T466, T467)) → DELETE1_IN_GGA(s(T466), T447, T450)
DELETE1_IN_GGA(s(T623), tree(0, T615, T616), tree(0, T615, T618)) → DELETE1_IN_GGA(s(T623), T616, T618)
DELETE1_IN_GGA(s(T633), tree(s(T632), T615, T616), tree(s(T632), T615, T618)) → U52_GGA(T633, T632, T615, T616, T618, lessc222_in_gg(T632, T633))
U52_GGA(T633, T632, T615, T616, T618, lessc222_out_gg(T632, T633)) → DELETE1_IN_GGA(s(T633), T616, T618)

The TRS R consists of the following rules:

lessc19_in_g(s(T33)) → U87_g(T33, lessc19_in_g(T33))
U87_g(T33, lessc19_out_g(T33)) → lessc19_out_g(s(T33))
lessc164_in_gg(0, s(T476)) → lessc164_out_gg(0, s(T476))
lessc164_in_gg(s(0), s(s(T489))) → lessc164_out_gg(s(0), s(s(T489)))
lessc164_in_gg(s(s(0)), s(s(s(T502)))) → lessc164_out_gg(s(s(0)), s(s(s(T502))))
lessc164_in_gg(s(s(s(0))), s(s(s(s(T515))))) → lessc164_out_gg(s(s(s(0))), s(s(s(s(T515)))))
lessc164_in_gg(s(s(s(s(0)))), s(s(s(s(s(T528)))))) → lessc164_out_gg(s(s(s(s(0)))), s(s(s(s(s(T528))))))
lessc164_in_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T541))))))) → lessc164_out_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T541)))))))
lessc164_in_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T554)))))))) → lessc164_out_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T554))))))))
lessc164_in_gg(s(s(s(s(s(s(s(T559))))))), s(s(s(s(s(s(s(T560)))))))) → U97_gg(T559, T560, lessc222_in_gg(T559, T560))
lessc222_in_gg(0, s(T571)) → lessc222_out_gg(0, s(T571))
lessc222_in_gg(s(T576), s(T577)) → U96_gg(T576, T577, lessc222_in_gg(T576, T577))
U96_gg(T576, T577, lessc222_out_gg(T576, T577)) → lessc222_out_gg(s(T576), s(T577))
U97_gg(T559, T560, lessc222_out_gg(T559, T560)) → lessc164_out_gg(s(s(s(s(s(s(s(T559))))))), s(s(s(s(s(s(s(T560))))))))

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3) = tree(x1, x2, x3)
void = void
s(x1) = s(x1)
lessc19_in_g(x1) = lessc19_in_g(x1)
U87_g(x1, x2) = U87_g(x1, x2)
lessc19_out_g(x1) = lessc19_out_g(x1)
0 = 0
lessc164_in_gg(x1, x2) = lessc164_in_gg(x1, x2)
lessc164_out_gg(x1, x2) = lessc164_out_gg(x1, x2)
U97_gg(x1, x2, x3) = U97_gg(x1, x2, x3)
lessc222_in_gg(x1, x2) = lessc222_in_gg(x1, x2)
lessc222_out_gg(x1, x2) = lessc222_out_gg(x1, x2)
U96_gg(x1, x2, x3) = U96_gg(x1, x2, x3)
DELETE1_IN_GGA(x1, x2, x3) = DELETE1_IN_GGA(x1, x2)
P71_IN_GGA(x1, x2, x3) = P71_IN_GGA(x1, x2)
U11_GGA(x1, x2, x3, x4) = U11_GGA(x1, x2, x4)
U25_GGA(x1, x2, x3, x4) = U25_GGA(x1, x2, x4)
U28_GGA(x1, x2, x3, x4) = U28_GGA(x1, x2, x4)
U32_GGA(x1, x2, x3, x4) = U32_GGA(x1, x2, x4)
U38_GGA(x1, x2, x3, x4, x5) = U38_GGA(x1, x2, x3, x5)
U41_GGA(x1, x2, x3, x4, x5) = U41_GGA(x1, x2, x3, x5)
U45_GGA(x1, x2, x3, x4, x5, x6) = U45_GGA(x1, x2, x3, x4, x6)
U48_GGA(x1, x2, x3, x4, x5, x6) = U48_GGA(x1, x2, x3, x4, x6)
U52_GGA(x1, x2, x3, x4, x5, x6) = U52_GGA(x1, x2, x3, x4, x6)

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

(29) PiDPToQDPProof (SOUND transformation)

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

(30) Obligation:

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

DELETE1_IN_GGA(T199, tree(T199, void, T200)) → P71_IN_GGA(T199, T200)
P71_IN_GGA(T199, T200) → U11_GGA(T199, T200, lessc19_in_g(T199))
U11_GGA(T199, T200, lessc19_out_g(T199)) → DELETE1_IN_GGA(T199, T200)
DELETE1_IN_GGA(s(T242), tree(s(T242), void, T237)) → U25_GGA(T242, T237, lessc19_in_g(T242))
U25_GGA(T242, T237, lessc19_out_g(T242)) → DELETE1_IN_GGA(s(T242), T237)
DELETE1_IN_GGA(T275, tree(T275, T276, void)) → U28_GGA(T275, T276, lessc19_in_g(T275))
U28_GGA(T275, T276, lessc19_out_g(T275)) → DELETE1_IN_GGA(T275, T276)
DELETE1_IN_GGA(s(T307), tree(s(T307), T300, void)) → U32_GGA(T307, T300, lessc19_in_g(T307))
U32_GGA(T307, T300, lessc19_out_g(T307)) → DELETE1_IN_GGA(s(T307), T300)
DELETE1_IN_GGA(T410, tree(T410, T411, T412)) → U38_GGA(T410, T411, T412, lessc19_in_g(T410))
U38_GGA(T410, T411, T412, lessc19_out_g(T410)) → DELETE1_IN_GGA(T410, T411)
DELETE1_IN_GGA(T429, tree(T429, T430, T431)) → U41_GGA(T429, T430, T431, lessc19_in_g(T429))
U41_GGA(T429, T430, T431, lessc19_out_g(T429)) → DELETE1_IN_GGA(T429, T431)
DELETE1_IN_GGA(0, tree(s(T455), T447, T448)) → DELETE1_IN_GGA(0, T447)
DELETE1_IN_GGA(T594, tree(T595, T596, T597)) → U48_GGA(T594, T595, T596, T597, lessc222_in_gg(T595, T594))
U48_GGA(T594, T595, T596, T597, lessc222_out_gg(T595, T594)) → DELETE1_IN_GGA(T594, T597)
DELETE1_IN_GGA(s(T466), tree(s(T467), T447, T448)) → U45_GGA(T466, T467, T447, T448, lessc164_in_gg(T466, T467))
U45_GGA(T466, T467, T447, T448, lessc164_out_gg(T466, T467)) → DELETE1_IN_GGA(s(T466), T447)
DELETE1_IN_GGA(s(T623), tree(0, T615, T616)) → DELETE1_IN_GGA(s(T623), T616)
DELETE1_IN_GGA(s(T633), tree(s(T632), T615, T616)) → U52_GGA(T633, T632, T615, T616, lessc222_in_gg(T632, T633))
U52_GGA(T633, T632, T615, T616, lessc222_out_gg(T632, T633)) → DELETE1_IN_GGA(s(T633), T616)

The TRS R consists of the following rules:

lessc19_in_g(s(T33)) → U87_g(T33, lessc19_in_g(T33))
U87_g(T33, lessc19_out_g(T33)) → lessc19_out_g(s(T33))
lessc164_in_gg(0, s(T476)) → lessc164_out_gg(0, s(T476))
lessc164_in_gg(s(0), s(s(T489))) → lessc164_out_gg(s(0), s(s(T489)))
lessc164_in_gg(s(s(0)), s(s(s(T502)))) → lessc164_out_gg(s(s(0)), s(s(s(T502))))
lessc164_in_gg(s(s(s(0))), s(s(s(s(T515))))) → lessc164_out_gg(s(s(s(0))), s(s(s(s(T515)))))
lessc164_in_gg(s(s(s(s(0)))), s(s(s(s(s(T528)))))) → lessc164_out_gg(s(s(s(s(0)))), s(s(s(s(s(T528))))))
lessc164_in_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T541))))))) → lessc164_out_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T541)))))))
lessc164_in_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T554)))))))) → lessc164_out_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T554))))))))
lessc164_in_gg(s(s(s(s(s(s(s(T559))))))), s(s(s(s(s(s(s(T560)))))))) → U97_gg(T559, T560, lessc222_in_gg(T559, T560))
lessc222_in_gg(0, s(T571)) → lessc222_out_gg(0, s(T571))
lessc222_in_gg(s(T576), s(T577)) → U96_gg(T576, T577, lessc222_in_gg(T576, T577))
U96_gg(T576, T577, lessc222_out_gg(T576, T577)) → lessc222_out_gg(s(T576), s(T577))
U97_gg(T559, T560, lessc222_out_gg(T559, T560)) → lessc164_out_gg(s(s(s(s(s(s(s(T559))))))), s(s(s(s(s(s(s(T560))))))))

The set Q consists of the following terms:

lessc19_in_g(x0)
U87_g(x0, x1)
lessc164_in_gg(x0, x1)
lessc222_in_gg(x0, x1)
U96_gg(x0, x1, x2)
U97_gg(x0, x1, x2)

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

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

P71_IN_GGA(T199, T200) → U11_GGA(T199, T200, lessc19_in_g(T199))
The graph contains the following edges 1 >= 1, 2 >= 2
U11_GGA(T199, T200, lessc19_out_g(T199)) → DELETE1_IN_GGA(T199, T200)
The graph contains the following edges 1 >= 1, 3 > 1, 2 >= 2
DELETE1_IN_GGA(T199, tree(T199, void, T200)) → P71_IN_GGA(T199, T200)
The graph contains the following edges 1 >= 1, 2 > 1, 2 > 2
DELETE1_IN_GGA(s(T623), tree(0, T615, T616)) → DELETE1_IN_GGA(s(T623), T616)
The graph contains the following edges 1 >= 1, 2 > 2
DELETE1_IN_GGA(0, tree(s(T455), T447, T448)) → DELETE1_IN_GGA(0, T447)
The graph contains the following edges 1 >= 1, 2 > 2
U25_GGA(T242, T237, lessc19_out_g(T242)) → DELETE1_IN_GGA(s(T242), T237)
The graph contains the following edges 2 >= 2
DELETE1_IN_GGA(s(T242), tree(s(T242), void, T237)) → U25_GGA(T242, T237, lessc19_in_g(T242))
The graph contains the following edges 1 > 1, 2 > 1, 2 > 2
U28_GGA(T275, T276, lessc19_out_g(T275)) → DELETE1_IN_GGA(T275, T276)
The graph contains the following edges 1 >= 1, 3 > 1, 2 >= 2
DELETE1_IN_GGA(T275, tree(T275, T276, void)) → U28_GGA(T275, T276, lessc19_in_g(T275))
The graph contains the following edges 1 >= 1, 2 > 1, 2 > 2
U32_GGA(T307, T300, lessc19_out_g(T307)) → DELETE1_IN_GGA(s(T307), T300)
The graph contains the following edges 2 >= 2
DELETE1_IN_GGA(s(T307), tree(s(T307), T300, void)) → U32_GGA(T307, T300, lessc19_in_g(T307))
The graph contains the following edges 1 > 1, 2 > 1, 2 > 2
U38_GGA(T410, T411, T412, lessc19_out_g(T410)) → DELETE1_IN_GGA(T410, T411)
The graph contains the following edges 1 >= 1, 4 > 1, 2 >= 2
DELETE1_IN_GGA(T410, tree(T410, T411, T412)) → U38_GGA(T410, T411, T412, lessc19_in_g(T410))
The graph contains the following edges 1 >= 1, 2 > 1, 2 > 2, 2 > 3
U41_GGA(T429, T430, T431, lessc19_out_g(T429)) → DELETE1_IN_GGA(T429, T431)
The graph contains the following edges 1 >= 1, 4 > 1, 3 >= 2
DELETE1_IN_GGA(T429, tree(T429, T430, T431)) → U41_GGA(T429, T430, T431, lessc19_in_g(T429))
The graph contains the following edges 1 >= 1, 2 > 1, 2 > 2, 2 > 3
U48_GGA(T594, T595, T596, T597, lessc222_out_gg(T595, T594)) → DELETE1_IN_GGA(T594, T597)
The graph contains the following edges 1 >= 1, 5 > 1, 4 >= 2
DELETE1_IN_GGA(T594, tree(T595, T596, T597)) → U48_GGA(T594, T595, T596, T597, lessc222_in_gg(T595, T594))
The graph contains the following edges 1 >= 1, 2 > 2, 2 > 3, 2 > 4
U45_GGA(T466, T467, T447, T448, lessc164_out_gg(T466, T467)) → DELETE1_IN_GGA(s(T466), T447)
The graph contains the following edges 3 >= 2
U52_GGA(T633, T632, T615, T616, lessc222_out_gg(T632, T633)) → DELETE1_IN_GGA(s(T633), T616)
The graph contains the following edges 4 >= 2
DELETE1_IN_GGA(s(T466), tree(s(T467), T447, T448)) → U45_GGA(T466, T467, T447, T448, lessc164_in_gg(T466, T467))
The graph contains the following edges 1 > 1, 2 > 2, 2 > 3, 2 > 4
DELETE1_IN_GGA(s(T633), tree(s(T632), T615, T616)) → U52_GGA(T633, T632, T615, T616, lessc222_in_gg(T632, T633))
The graph contains the following edges 1 > 1, 2 > 2, 2 > 3, 2 > 4

(0) Obligation:

(1) PrologToDTProblemTransformerProof (SOUND transformation)

(2) Obligation:

(3) TriplesToPiDPProof (SOUND transformation)

(4) Obligation:

(5) DependencyGraphProof (EQUIVALENT transformation)

(6) Complex Obligation (AND)

(7) Obligation:

(8) UsableRulesProof (EQUIVALENT transformation)

(9) Obligation:

(10) PiDPToQDPProof (EQUIVALENT transformation)

(11) Obligation:

(12) QDPSizeChangeProof (EQUIVALENT transformation)

(13) YES

(14) Obligation:

(15) UsableRulesProof (EQUIVALENT transformation)

(16) Obligation:

(17) PiDPToQDPProof (SOUND transformation)

(18) Obligation:

(19) QDPSizeChangeProof (EQUIVALENT transformation)

(20) YES

(21) Obligation:

(22) UsableRulesProof (EQUIVALENT transformation)

(23) Obligation:

(24) PiDPToQDPProof (EQUIVALENT transformation)

(25) Obligation:

(26) QDPSizeChangeProof (EQUIVALENT transformation)

(27) YES

(28) Obligation:

(29) PiDPToQDPProof (SOUND transformation)

(30) Obligation:

(31) QDPSizeChangeProof (EQUIVALENT transformation)

(32) YES