Runtime Complexity of the query pattern
sameleaves(g,g)
w.r.t. the given Prolog program could be shown to be BOUNDS(O(1), O(n^2)).

(0) Obligation:

Clauses:

sameleaves(leaf(L), leaf(L)).
sameleaves(tree(T1, T2), tree(S1, S2)) :- ','(getleave(T1, T2, L, T), ','(getleave(S1, S2, L, S), sameleaves(T, S))).
getleave(leaf(A), C, A, C).
getleave(tree(A, B), C, L, O) :- getleave(A, tree(B, C), L, O).

Query: sameleaves(g,g)

(1) LPReorderTransformerProof (EQUIVALENT transformation)

Reordered facts before rules in definite LP [PROLOG].

(2) Obligation:

Clauses:

sameleaves(leaf(L), leaf(L)).
getleave(leaf(A), C, A, C).
sameleaves(tree(T1, T2), tree(S1, S2)) :- ','(getleave(T1, T2, L, T), ','(getleave(S1, S2, L, S), sameleaves(T, S))).
getleave(tree(A, B), C, L, O) :- getleave(A, tree(B, C), L, O).

Query: sameleaves(g,g)

(3) PrologToCdtProblemTransformerProof (UPPER BOUND (ID) transformation)

Built complexity over-approximating cdt problems from derivation graph.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="1: sameleaves(T3, T4)\n\nT3 is ground\nT4 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
3 [label="3: sameleaves(T3, T4), SCOPE: 1, CLAUSE: 0 | sameleaves(T3, T4), SCOPE: 1, CLAUSE: 2\n\nT3 is ground\nT4 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: true | sameleaves(leaf(T7), leaf(T7)), SCOPE: 1, CLAUSE: 2\n\nT7 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: sameleaves(T3, T4), SCOPE: 1, CLAUSE: 2\n\nT3 is ground\nT4 is ground\nX3 is free\nsameleaves(T3, T4) !=? sameleaves(leaf(X3), leaf(X3))", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: sameleaves(leaf(T7), leaf(T7)), SCOPE: 1, CLAUSE: 2\n\nT7 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: ','(getleave(T16, T17, X23, X24), ','(getleave(T18, T19, X23, X25), sameleaves(X24, X25)))\n\nT16 is ground\nT17 is ground\nT18 is ground\nT19 is ground\nX23 is free\nX24 is free\nX25 is free", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: getleave(T16, T17, X23, X24)\n\nT16 is ground\nT17 is ground\nX23 is free\nX24 is free", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: ','(getleave(T18, T19, T24, X25), sameleaves(T25, X25))\n\nT18 is ground\nT19 is ground\nT24 is ground\nT25 is ground\nX25 is free", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: getleave(T16, T17, X23, X24), SCOPE: 2, CLAUSE: 1 | getleave(T16, T17, X23, X24), SCOPE: 2, CLAUSE: 3\n\nT16 is ground\nT17 is ground\nX23 is free\nX24 is free", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: true | getleave(leaf(T34), T35, X23, X24), SCOPE: 2, CLAUSE: 3\n\nT34 is ground\nT35 is ground\nX23 is free\nX24 is free", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: getleave(T16, T17, X23, X24), SCOPE: 2, CLAUSE: 3\n\nT16 is ground\nT17 is ground\nX23 is free\nX24 is free\nX38 is free\nX39 is free\ngetleave(T16, T17, X23, X24) !=? getleave(leaf(X38), X39, X38, X39)", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: getleave(leaf(T34), T35, X23, X24), SCOPE: 2, CLAUSE: 3\n\nT34 is ground\nT35 is ground\nX23 is free\nX24 is free", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: getleave(T42, tree(T43, T44), X64, X65)\n\nT42 is ground\nT43 is ground\nT44 is ground\nX64 is free\nX65 is free", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: getleave(T18, T19, T24, X25)\n\nT18 is ground\nT19 is ground\nT24 is ground\nX25 is free", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: sameleaves(T25, T55)\n\nT25 is ground\nT55 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: getleave(T18, T19, T24, X25), SCOPE: 3, CLAUSE: 1 | getleave(T18, T19, T24, X25), SCOPE: 3, CLAUSE: 3\n\nT18 is ground\nT19 is ground\nT24 is ground\nX25 is free", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: true | getleave(leaf(T64), T65, T64, X25), SCOPE: 3, CLAUSE: 3\n\nT64 is ground\nT65 is ground\nX25 is free", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: getleave(T18, T19, T24, X25), SCOPE: 3, CLAUSE: 3\n\nT18 is ground\nT19 is ground\nT24 is ground\nX25 is free\nX82 is free\nX83 is free\ngetleave(T18, T19, T24, X25) !=? getleave(leaf(X82), X83, X82, X83)", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: getleave(leaf(T64), T65, T64, X25), SCOPE: 3, CLAUSE: 3\n\nT64 is ground\nT65 is ground\nX25 is free", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: getleave(T74, tree(T75, T76), T77, X106)\n\nT74 is ground\nT75 is ground\nT76 is ground\nT77 is ground\nX106 is free", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 50 [arrowhead = none ];
50 -> 3;

51 [label="EVAL with clause\nsameleaves(leaf(X3), leaf(X3)).\nand substitutionX3 -> T7,\nT3 -> leaf(T7),\nT4 -> leaf(T7)", fontsize=14, style = filled, fillcolor = lightblue];
3 -> 51 [arrowhead = none ];
51 -> 5;

52 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
3 -> 52 [arrowhead = none ];
52 -> 7;

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

54 [label="EVAL with clause\nsameleaves(tree(X19, X20), tree(X21, X22)) :- ','(getleave(X19, X20, X23, X24), ','(getleave(X21, X22, X23, X25), sameleaves(X24, X25))).\nand substitutionX19 -> T16,\nX20 -> T17,\nT3 -> tree(T16, T17),\nX21 -> T18,\nX22 -> T19,\nT4 -> tree(T18, T19)", fontsize=14, style = filled, fillcolor = lightblue];
7 -> 54 [arrowhead = none ];
54 -> 14;

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

56 [label="BACKTRACK\nfor clause: sameleaves(tree(T1, T2), tree(S1, S2)) :- ','(getleave(T1, T2, L, T), ','(getleave(S1, S2, L, S), sameleaves(T, S)))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
8 -> 56 [arrowhead = none ];
56 -> 9;

57 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
14 -> 57 [arrowhead = none ];
57 -> 20;

58 [label="SPLIT 2\nnew knowledge:\nT16 is ground\nT17 is ground\nT24 is ground\nT25 is ground\nreplacements:X23 -> T24,\nX24 -> T25", fontsize=14, style = filled, fillcolor = violet];
14 -> 58 [arrowhead = none ];
58 -> 22;

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

60 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
22 -> 60 [arrowhead = none ];
60 -> 38;

61 [label="SPLIT 2\nnew knowledge:\nT18 is ground\nT19 is ground\nT24 is ground\nT55 is ground\nreplacements:X25 -> T55", fontsize=14, style = filled, fillcolor = violet];
22 -> 61 [arrowhead = none ];
61 -> 39;

62 [label="EVAL with clause\ngetleave(leaf(X38), X39, X38, X39).\nand substitutionX38 -> T34,\nT16 -> leaf(T34),\nT17 -> T35,\nX39 -> T35,\nX23 -> T34,\nX24 -> T35", fontsize=14, style = filled, fillcolor = lightblue];
24 -> 62 [arrowhead = none ];
62 -> 25;

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

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

65 [label="EVAL with clause\ngetleave(tree(X59, X60), X61, X62, X63) :- getleave(X59, tree(X60, X61), X62, X63).\nand substitutionX59 -> T42,\nX60 -> T43,\nT16 -> tree(T42, T43),\nT17 -> T44,\nX61 -> T44,\nX23 -> X64,\nX62 -> X64,\nX24 -> X65,\nX63 -> X65", fontsize=14, style = filled, fillcolor = lightblue];
28 -> 65 [arrowhead = none ];
65 -> 32;

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

67 [label="BACKTRACK\nfor clause: getleave(tree(A, B), C, L, O) :- getleave(A, tree(B, C), L, O)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
29 -> 67 [arrowhead = none ];
67 -> 30;

68 [label="INSTANCE with matching:\nT16 -> T42\nT17 -> tree(T43, T44)\nX23 -> X64\nX24 -> X65", fontsize=14, style = filled, fillcolor = lightgrey];
32 -> 68 [arrowhead = none , style=dashed];
68 -> 20[style=dashed];

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

70 [label="INSTANCE with matching:\nT3 -> T25\nT4 -> T55", fontsize=14, style = filled, fillcolor = lightgrey];
39 -> 70 [arrowhead = none , style=dashed];
70 -> 1[style=dashed];

71 [label="EVAL with clause\ngetleave(leaf(X82), X83, X82, X83).\nand substitutionX82 -> T64,\nT18 -> leaf(T64),\nT19 -> T65,\nX83 -> T65,\nT24 -> T64,\nX25 -> T65", fontsize=14, style = filled, fillcolor = lightblue];
40 -> 71 [arrowhead = none ];
71 -> 42;

72 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
40 -> 72 [arrowhead = none ];
72 -> 44;

73 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
42 -> 73 [arrowhead = none ];
73 -> 45;

74 [label="EVAL with clause\ngetleave(tree(X101, X102), X103, X104, X105) :- getleave(X101, tree(X102, X103), X104, X105).\nand substitutionX101 -> T74,\nX102 -> T75,\nT18 -> tree(T74, T75),\nT19 -> T76,\nX103 -> T76,\nT24 -> T77,\nX104 -> T77,\nX25 -> X106,\nX105 -> X106", fontsize=14, style = filled, fillcolor = lightblue];
44 -> 74 [arrowhead = none ];
74 -> 48;

75 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
44 -> 75 [arrowhead = none ];
75 -> 49;

76 [label="BACKTRACK\nfor clause: getleave(tree(A, B), C, L, O) :- getleave(A, tree(B, C), L, O)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
45 -> 76 [arrowhead = none ];
76 -> 46;

77 [label="INSTANCE with matching:\nT18 -> T74\nT19 -> tree(T75, T76)\nT24 -> T77\nX25 -> X106", fontsize=14, style = filled, fillcolor = lightgrey];
48 -> 77 [arrowhead = none , style=dashed];
77 -> 38[style=dashed];

}

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(leaf(z0), leaf(z0)) → f1_out1
f1_in(tree(z0, z1), tree(z2, z3)) → U1(f14_in(z0, z1, z2, z3), tree(z0, z1), tree(z2, z3))
U1(f14_out1(z0, z1, z2), tree(z3, z4), tree(z5, z6)) → f1_out1
f20_in(leaf(z0), z1) → f20_out1(z0, z1)
f20_in(tree(z0, z1), z2) → U2(f20_in(z0, tree(z1, z2)), tree(z0, z1), z2)
U2(f20_out1(z0, z1), tree(z2, z3), z4) → f20_out1(z0, z1)
f38_in(leaf(z0), z1, z0) → f38_out1(z1)
f38_in(tree(z0, z1), z2, z3) → U3(f38_in(z0, tree(z1, z2), z3), tree(z0, z1), z2, z3)
U3(f38_out1(z0), tree(z1, z2), z3, z4) → f38_out1(z0)
f14_in(z0, z1, z2, z3) → U4(f20_in(z0, z1), z0, z1, z2, z3)
U4(f20_out1(z0, z1), z2, z3, z4, z5) → U5(f22_in(z4, z5, z0, z1), z2, z3, z4, z5, z0, z1)
U5(f22_out1(z0), z1, z2, z3, z4, z5, z6) → f14_out1(z5, z6, z0)
f22_in(z0, z1, z2, z3) → U6(f38_in(z0, z1, z2), z0, z1, z2, z3)
U6(f38_out1(z0), z1, z2, z3, z4) → U7(f1_in(z4, z0), z1, z2, z3, z4, z0)
U7(f1_out1, z0, z1, z2, z3, z4) → f22_out1(z4)

Tuples:

F1_IN(tree(z0, z1), tree(z2, z3)) → c1(U1'(f14_in(z0, z1, z2, z3), tree(z0, z1), tree(z2, z3)), F14_IN(z0, z1, z2, z3))
F20_IN(tree(z0, z1), z2) → c4(U2'(f20_in(z0, tree(z1, z2)), tree(z0, z1), z2), F20_IN(z0, tree(z1, z2)))
F38_IN(tree(z0, z1), z2, z3) → c7(U3'(f38_in(z0, tree(z1, z2), z3), tree(z0, z1), z2, z3), F38_IN(z0, tree(z1, z2), z3))
F14_IN(z0, z1, z2, z3) → c9(U4'(f20_in(z0, z1), z0, z1, z2, z3), F20_IN(z0, z1))
U4'(f20_out1(z0, z1), z2, z3, z4, z5) → c10(U5'(f22_in(z4, z5, z0, z1), z2, z3, z4, z5, z0, z1), F22_IN(z4, z5, z0, z1))
F22_IN(z0, z1, z2, z3) → c12(U6'(f38_in(z0, z1, z2), z0, z1, z2, z3), F38_IN(z0, z1, z2))
U6'(f38_out1(z0), z1, z2, z3, z4) → c13(U7'(f1_in(z4, z0), z1, z2, z3, z4, z0), F1_IN(z4, z0))

S tuples:

F1_IN(tree(z0, z1), tree(z2, z3)) → c1(U1'(f14_in(z0, z1, z2, z3), tree(z0, z1), tree(z2, z3)), F14_IN(z0, z1, z2, z3))
F20_IN(tree(z0, z1), z2) → c4(U2'(f20_in(z0, tree(z1, z2)), tree(z0, z1), z2), F20_IN(z0, tree(z1, z2)))
F38_IN(tree(z0, z1), z2, z3) → c7(U3'(f38_in(z0, tree(z1, z2), z3), tree(z0, z1), z2, z3), F38_IN(z0, tree(z1, z2), z3))
F14_IN(z0, z1, z2, z3) → c9(U4'(f20_in(z0, z1), z0, z1, z2, z3), F20_IN(z0, z1))
U4'(f20_out1(z0, z1), z2, z3, z4, z5) → c10(U5'(f22_in(z4, z5, z0, z1), z2, z3, z4, z5, z0, z1), F22_IN(z4, z5, z0, z1))
F22_IN(z0, z1, z2, z3) → c12(U6'(f38_in(z0, z1, z2), z0, z1, z2, z3), F38_IN(z0, z1, z2))
U6'(f38_out1(z0), z1, z2, z3, z4) → c13(U7'(f1_in(z4, z0), z1, z2, z3, z4, z0), F1_IN(z4, z0))

K tuples:none
Defined Rule Symbols:

f1_in, U1, f20_in, U2, f38_in, U3, f14_in, U4, U5, f22_in, U6, U7

Defined Pair Symbols:

F1_IN, F20_IN, F38_IN, F14_IN, U4', F22_IN, U6'

Compound Symbols:

c1, c4, c7, c9, c10, c12, c13

(5) CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID) transformation)

Removed 5 trailing tuple parts

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(leaf(z0), leaf(z0)) → f1_out1
f1_in(tree(z0, z1), tree(z2, z3)) → U1(f14_in(z0, z1, z2, z3), tree(z0, z1), tree(z2, z3))
U1(f14_out1(z0, z1, z2), tree(z3, z4), tree(z5, z6)) → f1_out1
f20_in(leaf(z0), z1) → f20_out1(z0, z1)
f20_in(tree(z0, z1), z2) → U2(f20_in(z0, tree(z1, z2)), tree(z0, z1), z2)
U2(f20_out1(z0, z1), tree(z2, z3), z4) → f20_out1(z0, z1)
f38_in(leaf(z0), z1, z0) → f38_out1(z1)
f38_in(tree(z0, z1), z2, z3) → U3(f38_in(z0, tree(z1, z2), z3), tree(z0, z1), z2, z3)
U3(f38_out1(z0), tree(z1, z2), z3, z4) → f38_out1(z0)
f14_in(z0, z1, z2, z3) → U4(f20_in(z0, z1), z0, z1, z2, z3)
U4(f20_out1(z0, z1), z2, z3, z4, z5) → U5(f22_in(z4, z5, z0, z1), z2, z3, z4, z5, z0, z1)
U5(f22_out1(z0), z1, z2, z3, z4, z5, z6) → f14_out1(z5, z6, z0)
f22_in(z0, z1, z2, z3) → U6(f38_in(z0, z1, z2), z0, z1, z2, z3)
U6(f38_out1(z0), z1, z2, z3, z4) → U7(f1_in(z4, z0), z1, z2, z3, z4, z0)
U7(f1_out1, z0, z1, z2, z3, z4) → f22_out1(z4)

Tuples:

F14_IN(z0, z1, z2, z3) → c9(U4'(f20_in(z0, z1), z0, z1, z2, z3), F20_IN(z0, z1))
F22_IN(z0, z1, z2, z3) → c12(U6'(f38_in(z0, z1, z2), z0, z1, z2, z3), F38_IN(z0, z1, z2))
F1_IN(tree(z0, z1), tree(z2, z3)) → c1(F14_IN(z0, z1, z2, z3))
F20_IN(tree(z0, z1), z2) → c4(F20_IN(z0, tree(z1, z2)))
F38_IN(tree(z0, z1), z2, z3) → c7(F38_IN(z0, tree(z1, z2), z3))
U4'(f20_out1(z0, z1), z2, z3, z4, z5) → c10(F22_IN(z4, z5, z0, z1))
U6'(f38_out1(z0), z1, z2, z3, z4) → c13(F1_IN(z4, z0))

S tuples:

F14_IN(z0, z1, z2, z3) → c9(U4'(f20_in(z0, z1), z0, z1, z2, z3), F20_IN(z0, z1))
F22_IN(z0, z1, z2, z3) → c12(U6'(f38_in(z0, z1, z2), z0, z1, z2, z3), F38_IN(z0, z1, z2))
F1_IN(tree(z0, z1), tree(z2, z3)) → c1(F14_IN(z0, z1, z2, z3))
F20_IN(tree(z0, z1), z2) → c4(F20_IN(z0, tree(z1, z2)))
F38_IN(tree(z0, z1), z2, z3) → c7(F38_IN(z0, tree(z1, z2), z3))
U4'(f20_out1(z0, z1), z2, z3, z4, z5) → c10(F22_IN(z4, z5, z0, z1))
U6'(f38_out1(z0), z1, z2, z3, z4) → c13(F1_IN(z4, z0))

K tuples:none
Defined Rule Symbols:

f1_in, U1, f20_in, U2, f38_in, U3, f14_in, U4, U5, f22_in, U6, U7

Defined Pair Symbols:

F14_IN, F22_IN, F1_IN, F20_IN, F38_IN, U4', U6'

Compound Symbols:

c9, c12, c1, c4, c7, c10, c13

(7) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

U4'(f20_out1(z0, z1), z2, z3, z4, z5) → c10(F22_IN(z4, z5, z0, z1))

We considered the (Usable) Rules:

f38_in(leaf(z0), z1, z0) → f38_out1(z1)
f38_in(tree(z0, z1), z2, z3) → U3(f38_in(z0, tree(z1, z2), z3), tree(z0, z1), z2, z3)
U3(f38_out1(z0), tree(z1, z2), z3, z4) → f38_out1(z0)
f20_in(leaf(z0), z1) → f20_out1(z0, z1)
f20_in(tree(z0, z1), z2) → U2(f20_in(z0, tree(z1, z2)), tree(z0, z1), z2)
U2(f20_out1(z0, z1), tree(z2, z3), z4) → f20_out1(z0, z1)

And the Tuples:

F14_IN(z0, z1, z2, z3) → c9(U4'(f20_in(z0, z1), z0, z1, z2, z3), F20_IN(z0, z1))
F22_IN(z0, z1, z2, z3) → c12(U6'(f38_in(z0, z1, z2), z0, z1, z2, z3), F38_IN(z0, z1, z2))
F1_IN(tree(z0, z1), tree(z2, z3)) → c1(F14_IN(z0, z1, z2, z3))
F20_IN(tree(z0, z1), z2) → c4(F20_IN(z0, tree(z1, z2)))
F38_IN(tree(z0, z1), z2, z3) → c7(F38_IN(z0, tree(z1, z2), z3))
U4'(f20_out1(z0, z1), z2, z3, z4, z5) → c10(F22_IN(z4, z5, z0, z1))
U6'(f38_out1(z0), z1, z2, z3, z4) → c13(F1_IN(z4, z0))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(F14_IN(x₁, x₂, x₃, x₄)) = [2] + [2]x₁ + [2]x₂   
POL(F1_IN(x₁, x₂)) = [2]x₁   
POL(F20_IN(x₁, x₂)) = 0   
POL(F22_IN(x₁, x₂, x₃, x₄)) = [2]x₃ + [2]x₄   
POL(F38_IN(x₁, x₂, x₃)) = 0   
POL(U2(x₁, x₂, x₃)) = x₁   
POL(U3(x₁, x₂, x₃, x₄)) = [2]x₄   
POL(U4'(x₁, x₂, x₃, x₄, x₅)) = [2] + [2]x₁   
POL(U6'(x₁, x₂, x₃, x₄, x₅)) = [2]x₅   
POL(c1(x₁)) = x₁   
POL(c10(x₁)) = x₁   
POL(c12(x₁, x₂)) = x₁ + x₂   
POL(c13(x₁)) = x₁   
POL(c4(x₁)) = x₁   
POL(c7(x₁)) = x₁   
POL(c9(x₁, x₂)) = x₁ + x₂   
POL(f20_in(x₁, x₂)) = x₁ + x₂   
POL(f20_out1(x₁, x₂)) = [3] + x₁ + x₂   
POL(f38_in(x₁, x₂, x₃)) = [2] + [3]x₃   
POL(f38_out1(x₁)) = 0   
POL(leaf(x₁)) = [3] + x₁   
POL(tree(x₁, x₂)) = [1] + x₁ + x₂   

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(leaf(z0), leaf(z0)) → f1_out1
f1_in(tree(z0, z1), tree(z2, z3)) → U1(f14_in(z0, z1, z2, z3), tree(z0, z1), tree(z2, z3))
U1(f14_out1(z0, z1, z2), tree(z3, z4), tree(z5, z6)) → f1_out1
f20_in(leaf(z0), z1) → f20_out1(z0, z1)
f20_in(tree(z0, z1), z2) → U2(f20_in(z0, tree(z1, z2)), tree(z0, z1), z2)
U2(f20_out1(z0, z1), tree(z2, z3), z4) → f20_out1(z0, z1)
f38_in(leaf(z0), z1, z0) → f38_out1(z1)
f38_in(tree(z0, z1), z2, z3) → U3(f38_in(z0, tree(z1, z2), z3), tree(z0, z1), z2, z3)
U3(f38_out1(z0), tree(z1, z2), z3, z4) → f38_out1(z0)
f14_in(z0, z1, z2, z3) → U4(f20_in(z0, z1), z0, z1, z2, z3)
U4(f20_out1(z0, z1), z2, z3, z4, z5) → U5(f22_in(z4, z5, z0, z1), z2, z3, z4, z5, z0, z1)
U5(f22_out1(z0), z1, z2, z3, z4, z5, z6) → f14_out1(z5, z6, z0)
f22_in(z0, z1, z2, z3) → U6(f38_in(z0, z1, z2), z0, z1, z2, z3)
U6(f38_out1(z0), z1, z2, z3, z4) → U7(f1_in(z4, z0), z1, z2, z3, z4, z0)
U7(f1_out1, z0, z1, z2, z3, z4) → f22_out1(z4)

Tuples:

F14_IN(z0, z1, z2, z3) → c9(U4'(f20_in(z0, z1), z0, z1, z2, z3), F20_IN(z0, z1))
F22_IN(z0, z1, z2, z3) → c12(U6'(f38_in(z0, z1, z2), z0, z1, z2, z3), F38_IN(z0, z1, z2))
F1_IN(tree(z0, z1), tree(z2, z3)) → c1(F14_IN(z0, z1, z2, z3))
F20_IN(tree(z0, z1), z2) → c4(F20_IN(z0, tree(z1, z2)))
F38_IN(tree(z0, z1), z2, z3) → c7(F38_IN(z0, tree(z1, z2), z3))
U4'(f20_out1(z0, z1), z2, z3, z4, z5) → c10(F22_IN(z4, z5, z0, z1))
U6'(f38_out1(z0), z1, z2, z3, z4) → c13(F1_IN(z4, z0))

S tuples:

F14_IN(z0, z1, z2, z3) → c9(U4'(f20_in(z0, z1), z0, z1, z2, z3), F20_IN(z0, z1))
F22_IN(z0, z1, z2, z3) → c12(U6'(f38_in(z0, z1, z2), z0, z1, z2, z3), F38_IN(z0, z1, z2))
F1_IN(tree(z0, z1), tree(z2, z3)) → c1(F14_IN(z0, z1, z2, z3))
F20_IN(tree(z0, z1), z2) → c4(F20_IN(z0, tree(z1, z2)))
F38_IN(tree(z0, z1), z2, z3) → c7(F38_IN(z0, tree(z1, z2), z3))
U6'(f38_out1(z0), z1, z2, z3, z4) → c13(F1_IN(z4, z0))

K tuples:

U4'(f20_out1(z0, z1), z2, z3, z4, z5) → c10(F22_IN(z4, z5, z0, z1))

Defined Rule Symbols:

f1_in, U1, f20_in, U2, f38_in, U3, f14_in, U4, U5, f22_in, U6, U7

Defined Pair Symbols:

F14_IN, F22_IN, F1_IN, F20_IN, F38_IN, U4', U6'

Compound Symbols:

c9, c12, c1, c4, c7, c10, c13

(9) CdtKnowledgeProof (EQUIVALENT transformation)

The following tuples could be moved from S to K by knowledge propagation:

F22_IN(z0, z1, z2, z3) → c12(U6'(f38_in(z0, z1, z2), z0, z1, z2, z3), F38_IN(z0, z1, z2))
U6'(f38_out1(z0), z1, z2, z3, z4) → c13(F1_IN(z4, z0))
U6'(f38_out1(z0), z1, z2, z3, z4) → c13(F1_IN(z4, z0))
F1_IN(tree(z0, z1), tree(z2, z3)) → c1(F14_IN(z0, z1, z2, z3))
F14_IN(z0, z1, z2, z3) → c9(U4'(f20_in(z0, z1), z0, z1, z2, z3), F20_IN(z0, z1))
U4'(f20_out1(z0, z1), z2, z3, z4, z5) → c10(F22_IN(z4, z5, z0, z1))

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(leaf(z0), leaf(z0)) → f1_out1
f1_in(tree(z0, z1), tree(z2, z3)) → U1(f14_in(z0, z1, z2, z3), tree(z0, z1), tree(z2, z3))
U1(f14_out1(z0, z1, z2), tree(z3, z4), tree(z5, z6)) → f1_out1
f20_in(leaf(z0), z1) → f20_out1(z0, z1)
f20_in(tree(z0, z1), z2) → U2(f20_in(z0, tree(z1, z2)), tree(z0, z1), z2)
U2(f20_out1(z0, z1), tree(z2, z3), z4) → f20_out1(z0, z1)
f38_in(leaf(z0), z1, z0) → f38_out1(z1)
f38_in(tree(z0, z1), z2, z3) → U3(f38_in(z0, tree(z1, z2), z3), tree(z0, z1), z2, z3)
U3(f38_out1(z0), tree(z1, z2), z3, z4) → f38_out1(z0)
f14_in(z0, z1, z2, z3) → U4(f20_in(z0, z1), z0, z1, z2, z3)
U4(f20_out1(z0, z1), z2, z3, z4, z5) → U5(f22_in(z4, z5, z0, z1), z2, z3, z4, z5, z0, z1)
U5(f22_out1(z0), z1, z2, z3, z4, z5, z6) → f14_out1(z5, z6, z0)
f22_in(z0, z1, z2, z3) → U6(f38_in(z0, z1, z2), z0, z1, z2, z3)
U6(f38_out1(z0), z1, z2, z3, z4) → U7(f1_in(z4, z0), z1, z2, z3, z4, z0)
U7(f1_out1, z0, z1, z2, z3, z4) → f22_out1(z4)

Tuples:

F14_IN(z0, z1, z2, z3) → c9(U4'(f20_in(z0, z1), z0, z1, z2, z3), F20_IN(z0, z1))
F22_IN(z0, z1, z2, z3) → c12(U6'(f38_in(z0, z1, z2), z0, z1, z2, z3), F38_IN(z0, z1, z2))
F1_IN(tree(z0, z1), tree(z2, z3)) → c1(F14_IN(z0, z1, z2, z3))
F20_IN(tree(z0, z1), z2) → c4(F20_IN(z0, tree(z1, z2)))
F38_IN(tree(z0, z1), z2, z3) → c7(F38_IN(z0, tree(z1, z2), z3))
U4'(f20_out1(z0, z1), z2, z3, z4, z5) → c10(F22_IN(z4, z5, z0, z1))
U6'(f38_out1(z0), z1, z2, z3, z4) → c13(F1_IN(z4, z0))

S tuples:

F20_IN(tree(z0, z1), z2) → c4(F20_IN(z0, tree(z1, z2)))
F38_IN(tree(z0, z1), z2, z3) → c7(F38_IN(z0, tree(z1, z2), z3))

K tuples:

U4'(f20_out1(z0, z1), z2, z3, z4, z5) → c10(F22_IN(z4, z5, z0, z1))
F22_IN(z0, z1, z2, z3) → c12(U6'(f38_in(z0, z1, z2), z0, z1, z2, z3), F38_IN(z0, z1, z2))
U6'(f38_out1(z0), z1, z2, z3, z4) → c13(F1_IN(z4, z0))
F1_IN(tree(z0, z1), tree(z2, z3)) → c1(F14_IN(z0, z1, z2, z3))
F14_IN(z0, z1, z2, z3) → c9(U4'(f20_in(z0, z1), z0, z1, z2, z3), F20_IN(z0, z1))

Defined Rule Symbols:

f1_in, U1, f20_in, U2, f38_in, U3, f14_in, U4, U5, f22_in, U6, U7

Defined Pair Symbols:

F14_IN, F22_IN, F1_IN, F20_IN, F38_IN, U4', U6'

Compound Symbols:

c9, c12, c1, c4, c7, c10, c13

(11) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

F20_IN(tree(z0, z1), z2) → c4(F20_IN(z0, tree(z1, z2)))

We considered the (Usable) Rules:

f38_in(leaf(z0), z1, z0) → f38_out1(z1)
f38_in(tree(z0, z1), z2, z3) → U3(f38_in(z0, tree(z1, z2), z3), tree(z0, z1), z2, z3)
U3(f38_out1(z0), tree(z1, z2), z3, z4) → f38_out1(z0)
f20_in(leaf(z0), z1) → f20_out1(z0, z1)
f20_in(tree(z0, z1), z2) → U2(f20_in(z0, tree(z1, z2)), tree(z0, z1), z2)
U2(f20_out1(z0, z1), tree(z2, z3), z4) → f20_out1(z0, z1)

And the Tuples:

F14_IN(z0, z1, z2, z3) → c9(U4'(f20_in(z0, z1), z0, z1, z2, z3), F20_IN(z0, z1))
F22_IN(z0, z1, z2, z3) → c12(U6'(f38_in(z0, z1, z2), z0, z1, z2, z3), F38_IN(z0, z1, z2))
F1_IN(tree(z0, z1), tree(z2, z3)) → c1(F14_IN(z0, z1, z2, z3))
F20_IN(tree(z0, z1), z2) → c4(F20_IN(z0, tree(z1, z2)))
F38_IN(tree(z0, z1), z2, z3) → c7(F38_IN(z0, tree(z1, z2), z3))
U4'(f20_out1(z0, z1), z2, z3, z4, z5) → c10(F22_IN(z4, z5, z0, z1))
U6'(f38_out1(z0), z1, z2, z3, z4) → c13(F1_IN(z4, z0))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(F14_IN(x₁, x₂, x₃, x₄)) = [1] + x₁ + x₂·x₄ + x₁·x₄ + x₁·x₃ + x₂·x₃   
POL(F1_IN(x₁, x₂)) = x₁·x₂   
POL(F20_IN(x₁, x₂)) = x₁   
POL(F22_IN(x₁, x₂, x₃, x₄)) = x₂·x₄ + x₁·x₄ + x₁·x₃ + x₂·x₃   
POL(F38_IN(x₁, x₂, x₃)) = 0   
POL(U2(x₁, x₂, x₃)) = x₁   
POL(U3(x₁, x₂, x₃, x₄)) = x₁   
POL(U4'(x₁, x₂, x₃, x₄, x₅)) = x₁·x₅ + x₁·x₄   
POL(U6'(x₁, x₂, x₃, x₄, x₅)) = x₁·x₅ + x₁·x₄   
POL(c1(x₁)) = x₁   
POL(c10(x₁)) = x₁   
POL(c12(x₁, x₂)) = x₁ + x₂   
POL(c13(x₁)) = x₁   
POL(c4(x₁)) = x₁   
POL(c7(x₁)) = x₁   
POL(c9(x₁, x₂)) = x₁ + x₂   
POL(f20_in(x₁, x₂)) = x₁ + x₂   
POL(f20_out1(x₁, x₂)) = x₁ + x₂   
POL(f38_in(x₁, x₂, x₃)) = x₁ + x₂   
POL(f38_out1(x₁)) = x₁   
POL(leaf(x₁)) = [1] + x₁   
POL(tree(x₁, x₂)) = [1] + x₁ + x₂   

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(leaf(z0), leaf(z0)) → f1_out1
f1_in(tree(z0, z1), tree(z2, z3)) → U1(f14_in(z0, z1, z2, z3), tree(z0, z1), tree(z2, z3))
U1(f14_out1(z0, z1, z2), tree(z3, z4), tree(z5, z6)) → f1_out1
f20_in(leaf(z0), z1) → f20_out1(z0, z1)
f20_in(tree(z0, z1), z2) → U2(f20_in(z0, tree(z1, z2)), tree(z0, z1), z2)
U2(f20_out1(z0, z1), tree(z2, z3), z4) → f20_out1(z0, z1)
f38_in(leaf(z0), z1, z0) → f38_out1(z1)
f38_in(tree(z0, z1), z2, z3) → U3(f38_in(z0, tree(z1, z2), z3), tree(z0, z1), z2, z3)
U3(f38_out1(z0), tree(z1, z2), z3, z4) → f38_out1(z0)
f14_in(z0, z1, z2, z3) → U4(f20_in(z0, z1), z0, z1, z2, z3)
U4(f20_out1(z0, z1), z2, z3, z4, z5) → U5(f22_in(z4, z5, z0, z1), z2, z3, z4, z5, z0, z1)
U5(f22_out1(z0), z1, z2, z3, z4, z5, z6) → f14_out1(z5, z6, z0)
f22_in(z0, z1, z2, z3) → U6(f38_in(z0, z1, z2), z0, z1, z2, z3)
U6(f38_out1(z0), z1, z2, z3, z4) → U7(f1_in(z4, z0), z1, z2, z3, z4, z0)
U7(f1_out1, z0, z1, z2, z3, z4) → f22_out1(z4)

Tuples:

F14_IN(z0, z1, z2, z3) → c9(U4'(f20_in(z0, z1), z0, z1, z2, z3), F20_IN(z0, z1))
F22_IN(z0, z1, z2, z3) → c12(U6'(f38_in(z0, z1, z2), z0, z1, z2, z3), F38_IN(z0, z1, z2))
F1_IN(tree(z0, z1), tree(z2, z3)) → c1(F14_IN(z0, z1, z2, z3))
F20_IN(tree(z0, z1), z2) → c4(F20_IN(z0, tree(z1, z2)))
F38_IN(tree(z0, z1), z2, z3) → c7(F38_IN(z0, tree(z1, z2), z3))
U4'(f20_out1(z0, z1), z2, z3, z4, z5) → c10(F22_IN(z4, z5, z0, z1))
U6'(f38_out1(z0), z1, z2, z3, z4) → c13(F1_IN(z4, z0))

S tuples:

F38_IN(tree(z0, z1), z2, z3) → c7(F38_IN(z0, tree(z1, z2), z3))

K tuples:

U4'(f20_out1(z0, z1), z2, z3, z4, z5) → c10(F22_IN(z4, z5, z0, z1))
F22_IN(z0, z1, z2, z3) → c12(U6'(f38_in(z0, z1, z2), z0, z1, z2, z3), F38_IN(z0, z1, z2))
U6'(f38_out1(z0), z1, z2, z3, z4) → c13(F1_IN(z4, z0))
F1_IN(tree(z0, z1), tree(z2, z3)) → c1(F14_IN(z0, z1, z2, z3))
F14_IN(z0, z1, z2, z3) → c9(U4'(f20_in(z0, z1), z0, z1, z2, z3), F20_IN(z0, z1))
F20_IN(tree(z0, z1), z2) → c4(F20_IN(z0, tree(z1, z2)))

Defined Rule Symbols:

f1_in, U1, f20_in, U2, f38_in, U3, f14_in, U4, U5, f22_in, U6, U7

Defined Pair Symbols:

F14_IN, F22_IN, F1_IN, F20_IN, F38_IN, U4', U6'

Compound Symbols:

c9, c12, c1, c4, c7, c10, c13

(13) PrologToCdtProblemTransformerProof (UPPER BOUND (ID) transformation)

Built complexity over-approximating cdt problems from derivation graph.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
2 [label="2: sameleaves(T3, T4)\n\nT3 is ground\nT4 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
4 [label="4: sameleaves(T3, T4), SCOPE: 1, CLAUSE: 0 | sameleaves(T3, T4), SCOPE: 1, CLAUSE: 2\n\nT3 is ground\nT4 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: true | sameleaves(leaf(T6), leaf(T6)), SCOPE: 1, CLAUSE: 2\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: sameleaves(T3, T4), SCOPE: 1, CLAUSE: 2\n\nT3 is ground\nT4 is ground\nX2 is free\nsameleaves(T3, T4) !=? sameleaves(leaf(X2), leaf(X2))", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: sameleaves(leaf(T6), leaf(T6)), SCOPE: 1, CLAUSE: 2\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: ','(getleave(T11, T12, X15, X16), ','(getleave(T13, T14, X15, X17), sameleaves(X16, X17)))\n\nT11 is ground\nT12 is ground\nT13 is ground\nT14 is ground\nX15 is free\nX16 is free\nX17 is free", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: ','(getleave(T11, T12, X15, X16), ','(getleave(T13, T14, X15, X17), sameleaves(X16, X17))), SCOPE: 2, CLAUSE: 1 | ','(getleave(T11, T12, X15, X16), ','(getleave(T13, T14, X15, X17), sameleaves(X16, X17))), SCOPE: 2, CLAUSE: 3\n\nT11 is ground\nT12 is ground\nT13 is ground\nT14 is ground\nX15 is free\nX16 is free\nX17 is free", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: ','(getleave(T13, T14, T19, X17), sameleaves(T20, X17)) | ','(getleave(leaf(T19), T20, X15, X16), ','(getleave(T13, T14, X15, X17), sameleaves(X16, X17))), SCOPE: 2, CLAUSE: 3\n\nT13 is ground\nT14 is ground\nT19 is ground\nT20 is ground\nX15 is free\nX16 is free\nX17 is free", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: ','(getleave(T11, T12, X15, X16), ','(getleave(T13, T14, X15, X17), sameleaves(X16, X17))), SCOPE: 2, CLAUSE: 3\n\nT11 is ground\nT12 is ground\nT13 is ground\nT14 is ground\nX15 is free\nX16 is free\nX17 is free\nX22 is free\nX23 is free\ngetleave(T11, T12, X15, X16) !=? getleave(leaf(X22), X23, X22, X23)", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: ','(getleave(T13, T14, T19, X17), sameleaves(T20, X17))\n\nT13 is ground\nT14 is ground\nT19 is ground\nT20 is ground\nX17 is free", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: ','(getleave(leaf(T19), T20, X15, X16), ','(getleave(T13, T14, X15, X17), sameleaves(X16, X17))), SCOPE: 2, CLAUSE: 3\n\nT13 is ground\nT14 is ground\nT19 is ground\nT20 is ground\nX15 is free\nX16 is free\nX17 is free", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: getleave(T13, T14, T19, X17)\n\nT13 is ground\nT14 is ground\nT19 is ground\nX17 is free", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: sameleaves(T20, T29)\n\nT20 is ground\nT29 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: getleave(T13, T14, T19, X17), SCOPE: 3, CLAUSE: 1 | getleave(T13, T14, T19, X17), SCOPE: 3, CLAUSE: 3\n\nT13 is ground\nT14 is ground\nT19 is ground\nX17 is free", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: true | getleave(leaf(T38), T39, T38, X17), SCOPE: 3, CLAUSE: 3\n\nT38 is ground\nT39 is ground\nX17 is free", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: getleave(T13, T14, T19, X17), SCOPE: 3, CLAUSE: 3\n\nT13 is ground\nT14 is ground\nT19 is ground\nX17 is free\nX40 is free\nX41 is free\ngetleave(T13, T14, T19, X17) !=? getleave(leaf(X40), X41, X40, X41)", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: getleave(leaf(T38), T39, T38, X17), SCOPE: 3, CLAUSE: 3\n\nT38 is ground\nT39 is ground\nX17 is free", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: getleave(T48, tree(T49, T50), T51, X64)\n\nT48 is ground\nT49 is ground\nT50 is ground\nT51 is ground\nX64 is free", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: ','(getleave(T66, tree(T67, T68), X95, X96), ','(getleave(T13, T14, X95, X17), sameleaves(X96, X17)))\n\nT13 is ground\nT14 is ground\nT66 is ground\nT67 is ground\nT68 is ground\nX17 is free\nX95 is free\nX96 is free", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
2 -> 52 [arrowhead = none ];
52 -> 4;

53 [label="EVAL with clause\nsameleaves(leaf(X2), leaf(X2)).\nand substitutionX2 -> T6,\nT3 -> leaf(T6),\nT4 -> leaf(T6)", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 53 [arrowhead = none ];
53 -> 6;

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

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

56 [label="EVAL with clause\nsameleaves(tree(X11, X12), tree(X13, X14)) :- ','(getleave(X11, X12, X15, X16), ','(getleave(X13, X14, X15, X17), sameleaves(X16, X17))).\nand substitutionX11 -> T11,\nX12 -> T12,\nT3 -> tree(T11, T12),\nX13 -> T13,\nX14 -> T14,\nT4 -> tree(T13, T14)", fontsize=14, style = filled, fillcolor = lightblue];
10 -> 56 [arrowhead = none ];
56 -> 13;

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

58 [label="BACKTRACK\nfor clause: sameleaves(tree(T1, T2), tree(S1, S2)) :- ','(getleave(T1, T2, L, T), ','(getleave(S1, S2, L, S), sameleaves(T, S)))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
11 -> 58 [arrowhead = none ];
58 -> 12;

59 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
13 -> 59 [arrowhead = none ];
59 -> 17;

60 [label="EVAL with clause\ngetleave(leaf(X22), X23, X22, X23).\nand substitutionX22 -> T19,\nT11 -> leaf(T19),\nT12 -> T20,\nX23 -> T20,\nX15 -> T19,\nX16 -> T20", fontsize=14, style = filled, fillcolor = lightblue];
17 -> 60 [arrowhead = none ];
60 -> 18;

61 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
17 -> 61 [arrowhead = none ];
61 -> 19;

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

63 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
18 -> 63 [arrowhead = none ];
63 -> 23;

64 [label="EVAL with clause\ngetleave(tree(X90, X91), X92, X93, X94) :- getleave(X90, tree(X91, X92), X93, X94).\nand substitutionX90 -> T66,\nX91 -> T67,\nT11 -> tree(T66, T67),\nT12 -> T68,\nX92 -> T68,\nX15 -> X95,\nX93 -> X95,\nX16 -> X96,\nX94 -> X96", fontsize=14, style = filled, fillcolor = lightblue];
19 -> 64 [arrowhead = none ];
64 -> 50;

65 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
19 -> 65 [arrowhead = none ];
65 -> 51;

66 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
21 -> 66 [arrowhead = none ];
66 -> 26;

67 [label="SPLIT 2\nnew knowledge:\nT13 is ground\nT14 is ground\nT19 is ground\nT29 is ground\nreplacements:X17 -> T29", fontsize=14, style = filled, fillcolor = violet];
21 -> 67 [arrowhead = none ];
67 -> 27;

68 [label="BACKTRACK\nfor clause: getleave(tree(A, B), C, L, O) :- getleave(A, tree(B, C), L, O)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
23 -> 68 [arrowhead = none ];
68 -> 47;

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

70 [label="INSTANCE with matching:\nT3 -> T20\nT4 -> T29", fontsize=14, style = filled, fillcolor = lightgrey];
27 -> 70 [arrowhead = none , style=dashed];
70 -> 2[style=dashed];

71 [label="EVAL with clause\ngetleave(leaf(X40), X41, X40, X41).\nand substitutionX40 -> T38,\nT13 -> leaf(T38),\nT14 -> T39,\nX41 -> T39,\nT19 -> T38,\nX17 -> T39", fontsize=14, style = filled, fillcolor = lightblue];
31 -> 71 [arrowhead = none ];
71 -> 34;

72 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
31 -> 72 [arrowhead = none ];
72 -> 35;

73 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
34 -> 73 [arrowhead = none ];
73 -> 36;

74 [label="EVAL with clause\ngetleave(tree(X59, X60), X61, X62, X63) :- getleave(X59, tree(X60, X61), X62, X63).\nand substitutionX59 -> T48,\nX60 -> T49,\nT13 -> tree(T48, T49),\nT14 -> T50,\nX61 -> T50,\nT19 -> T51,\nX62 -> T51,\nX17 -> X64,\nX63 -> X64", fontsize=14, style = filled, fillcolor = lightblue];
35 -> 74 [arrowhead = none ];
74 -> 41;

75 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
35 -> 75 [arrowhead = none ];
75 -> 43;

76 [label="BACKTRACK\nfor clause: getleave(tree(A, B), C, L, O) :- getleave(A, tree(B, C), L, O)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
36 -> 76 [arrowhead = none ];
76 -> 37;

77 [label="INSTANCE with matching:\nT13 -> T48\nT14 -> tree(T49, T50)\nT19 -> T51\nX17 -> X64", fontsize=14, style = filled, fillcolor = lightgrey];
41 -> 77 [arrowhead = none , style=dashed];
77 -> 26[style=dashed];

78 [label="INSTANCE with matching:\nT11 -> T66\nT12 -> tree(T67, T68)\nX15 -> X95\nX16 -> X96", fontsize=14, style = filled, fillcolor = lightgrey];
50 -> 78 [arrowhead = none , style=dashed];
78 -> 13[style=dashed];

}

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(leaf(z0), leaf(z0)) → f2_out1
f2_in(tree(z0, z1), tree(z2, z3)) → U1(f13_in(z0, z1, z2, z3), tree(z0, z1), tree(z2, z3))
U1(f13_out1(z0, z1, z2), tree(z3, z4), tree(z5, z6)) → f2_out1
f13_in(leaf(z0), z1, z2, z3) → U2(f18_in(z2, z3, z0, z1), leaf(z0), z1, z2, z3)
f13_in(tree(z0, z1), z2, z3, z4) → U3(f13_in(z0, tree(z1, z2), z3, z4), tree(z0, z1), z2, z3, z4)
U2(f18_out1(z0), leaf(z1), z2, z3, z4) → f13_out1(z1, z2, z0)
U2(f18_out2(z0, z1, z2), leaf(z3), z4, z5, z6) → f13_out1(z0, z1, z2)
U3(f13_out1(z0, z1, z2), tree(z3, z4), z5, z6, z7) → f13_out1(z0, z1, z2)
f26_in(leaf(z0), z1, z0) → f26_out1(z1)
f26_in(tree(z0, z1), z2, z3) → U4(f26_in(z0, tree(z1, z2), z3), tree(z0, z1), z2, z3)
U4(f26_out1(z0), tree(z1, z2), z3, z4) → f26_out1(z0)
f21_in(z0, z1, z2, z3) → U5(f26_in(z0, z1, z2), z0, z1, z2, z3)
U5(f26_out1(z0), z1, z2, z3, z4) → U6(f2_in(z4, z0), z1, z2, z3, z4, z0)
U6(f2_out1, z0, z1, z2, z3, z4) → f21_out1(z4)
f18_in(z0, z1, z2, z3) → U7(f21_in(z0, z1, z2, z3), f23_in(z2, z3, z0, z1), z0, z1, z2, z3)
U7(f21_out1(z0), z1, z2, z3, z4, z5) → f18_out1(z0)
U7(z0, f23_out1(z1, z2, z3), z4, z5, z6, z7) → f18_out2(z1, z2, z3)

Tuples:

F2_IN(tree(z0, z1), tree(z2, z3)) → c1(U1'(f13_in(z0, z1, z2, z3), tree(z0, z1), tree(z2, z3)), F13_IN(z0, z1, z2, z3))
F13_IN(leaf(z0), z1, z2, z3) → c3(U2'(f18_in(z2, z3, z0, z1), leaf(z0), z1, z2, z3), F18_IN(z2, z3, z0, z1))
F13_IN(tree(z0, z1), z2, z3, z4) → c4(U3'(f13_in(z0, tree(z1, z2), z3, z4), tree(z0, z1), z2, z3, z4), F13_IN(z0, tree(z1, z2), z3, z4))
F26_IN(tree(z0, z1), z2, z3) → c9(U4'(f26_in(z0, tree(z1, z2), z3), tree(z0, z1), z2, z3), F26_IN(z0, tree(z1, z2), z3))
F21_IN(z0, z1, z2, z3) → c11(U5'(f26_in(z0, z1, z2), z0, z1, z2, z3), F26_IN(z0, z1, z2))
U5'(f26_out1(z0), z1, z2, z3, z4) → c12(U6'(f2_in(z4, z0), z1, z2, z3, z4, z0), F2_IN(z4, z0))
F18_IN(z0, z1, z2, z3) → c14(U7'(f21_in(z0, z1, z2, z3), f23_in(z2, z3, z0, z1), z0, z1, z2, z3), F21_IN(z0, z1, z2, z3))

S tuples:

F2_IN(tree(z0, z1), tree(z2, z3)) → c1(U1'(f13_in(z0, z1, z2, z3), tree(z0, z1), tree(z2, z3)), F13_IN(z0, z1, z2, z3))
F13_IN(leaf(z0), z1, z2, z3) → c3(U2'(f18_in(z2, z3, z0, z1), leaf(z0), z1, z2, z3), F18_IN(z2, z3, z0, z1))
F13_IN(tree(z0, z1), z2, z3, z4) → c4(U3'(f13_in(z0, tree(z1, z2), z3, z4), tree(z0, z1), z2, z3, z4), F13_IN(z0, tree(z1, z2), z3, z4))
F26_IN(tree(z0, z1), z2, z3) → c9(U4'(f26_in(z0, tree(z1, z2), z3), tree(z0, z1), z2, z3), F26_IN(z0, tree(z1, z2), z3))
F21_IN(z0, z1, z2, z3) → c11(U5'(f26_in(z0, z1, z2), z0, z1, z2, z3), F26_IN(z0, z1, z2))
U5'(f26_out1(z0), z1, z2, z3, z4) → c12(U6'(f2_in(z4, z0), z1, z2, z3, z4, z0), F2_IN(z4, z0))
F18_IN(z0, z1, z2, z3) → c14(U7'(f21_in(z0, z1, z2, z3), f23_in(z2, z3, z0, z1), z0, z1, z2, z3), F21_IN(z0, z1, z2, z3))

K tuples:none
Defined Rule Symbols:

f2_in, U1, f13_in, U2, U3, f26_in, U4, f21_in, U5, U6, f18_in, U7

Defined Pair Symbols:

F2_IN, F13_IN, F26_IN, F21_IN, U5', F18_IN

Compound Symbols:

c1, c3, c4, c9, c11, c12, c14

(15) CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID) transformation)

Removed 6 trailing tuple parts

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(leaf(z0), leaf(z0)) → f2_out1
f2_in(tree(z0, z1), tree(z2, z3)) → U1(f13_in(z0, z1, z2, z3), tree(z0, z1), tree(z2, z3))
U1(f13_out1(z0, z1, z2), tree(z3, z4), tree(z5, z6)) → f2_out1
f13_in(leaf(z0), z1, z2, z3) → U2(f18_in(z2, z3, z0, z1), leaf(z0), z1, z2, z3)
f13_in(tree(z0, z1), z2, z3, z4) → U3(f13_in(z0, tree(z1, z2), z3, z4), tree(z0, z1), z2, z3, z4)
U2(f18_out1(z0), leaf(z1), z2, z3, z4) → f13_out1(z1, z2, z0)
U2(f18_out2(z0, z1, z2), leaf(z3), z4, z5, z6) → f13_out1(z0, z1, z2)
U3(f13_out1(z0, z1, z2), tree(z3, z4), z5, z6, z7) → f13_out1(z0, z1, z2)
f26_in(leaf(z0), z1, z0) → f26_out1(z1)
f26_in(tree(z0, z1), z2, z3) → U4(f26_in(z0, tree(z1, z2), z3), tree(z0, z1), z2, z3)
U4(f26_out1(z0), tree(z1, z2), z3, z4) → f26_out1(z0)
f21_in(z0, z1, z2, z3) → U5(f26_in(z0, z1, z2), z0, z1, z2, z3)
U5(f26_out1(z0), z1, z2, z3, z4) → U6(f2_in(z4, z0), z1, z2, z3, z4, z0)
U6(f2_out1, z0, z1, z2, z3, z4) → f21_out1(z4)
f18_in(z0, z1, z2, z3) → U7(f21_in(z0, z1, z2, z3), f23_in(z2, z3, z0, z1), z0, z1, z2, z3)
U7(f21_out1(z0), z1, z2, z3, z4, z5) → f18_out1(z0)
U7(z0, f23_out1(z1, z2, z3), z4, z5, z6, z7) → f18_out2(z1, z2, z3)

Tuples:

F21_IN(z0, z1, z2, z3) → c11(U5'(f26_in(z0, z1, z2), z0, z1, z2, z3), F26_IN(z0, z1, z2))
F2_IN(tree(z0, z1), tree(z2, z3)) → c1(F13_IN(z0, z1, z2, z3))
F13_IN(leaf(z0), z1, z2, z3) → c3(F18_IN(z2, z3, z0, z1))
F13_IN(tree(z0, z1), z2, z3, z4) → c4(F13_IN(z0, tree(z1, z2), z3, z4))
F26_IN(tree(z0, z1), z2, z3) → c9(F26_IN(z0, tree(z1, z2), z3))
U5'(f26_out1(z0), z1, z2, z3, z4) → c12(F2_IN(z4, z0))
F18_IN(z0, z1, z2, z3) → c14(F21_IN(z0, z1, z2, z3))

S tuples:

F21_IN(z0, z1, z2, z3) → c11(U5'(f26_in(z0, z1, z2), z0, z1, z2, z3), F26_IN(z0, z1, z2))
F2_IN(tree(z0, z1), tree(z2, z3)) → c1(F13_IN(z0, z1, z2, z3))
F13_IN(leaf(z0), z1, z2, z3) → c3(F18_IN(z2, z3, z0, z1))
F13_IN(tree(z0, z1), z2, z3, z4) → c4(F13_IN(z0, tree(z1, z2), z3, z4))
F26_IN(tree(z0, z1), z2, z3) → c9(F26_IN(z0, tree(z1, z2), z3))
U5'(f26_out1(z0), z1, z2, z3, z4) → c12(F2_IN(z4, z0))
F18_IN(z0, z1, z2, z3) → c14(F21_IN(z0, z1, z2, z3))

K tuples:none
Defined Rule Symbols:

f2_in, U1, f13_in, U2, U3, f26_in, U4, f21_in, U5, U6, f18_in, U7

Defined Pair Symbols:

F21_IN, F2_IN, F13_IN, F26_IN, U5', F18_IN

Compound Symbols:

c11, c1, c3, c4, c9, c12, c14

(17) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

F2_IN(tree(z0, z1), tree(z2, z3)) → c1(F13_IN(z0, z1, z2, z3))
U5'(f26_out1(z0), z1, z2, z3, z4) → c12(F2_IN(z4, z0))

We considered the (Usable) Rules:

f26_in(leaf(z0), z1, z0) → f26_out1(z1)
f26_in(tree(z0, z1), z2, z3) → U4(f26_in(z0, tree(z1, z2), z3), tree(z0, z1), z2, z3)
U4(f26_out1(z0), tree(z1, z2), z3, z4) → f26_out1(z0)

And the Tuples:

F21_IN(z0, z1, z2, z3) → c11(U5'(f26_in(z0, z1, z2), z0, z1, z2, z3), F26_IN(z0, z1, z2))
F2_IN(tree(z0, z1), tree(z2, z3)) → c1(F13_IN(z0, z1, z2, z3))
F13_IN(leaf(z0), z1, z2, z3) → c3(F18_IN(z2, z3, z0, z1))
F13_IN(tree(z0, z1), z2, z3, z4) → c4(F13_IN(z0, tree(z1, z2), z3, z4))
F26_IN(tree(z0, z1), z2, z3) → c9(F26_IN(z0, tree(z1, z2), z3))
U5'(f26_out1(z0), z1, z2, z3, z4) → c12(F2_IN(z4, z0))
F18_IN(z0, z1, z2, z3) → c14(F21_IN(z0, z1, z2, z3))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(F13_IN(x₁, x₂, x₃, x₄)) = [2]x₃ + [2]x₄   
POL(F18_IN(x₁, x₂, x₃, x₄)) = [2]x₁ + [2]x₂   
POL(F21_IN(x₁, x₂, x₃, x₄)) = [2]x₁ + [2]x₂   
POL(F26_IN(x₁, x₂, x₃)) = 0   
POL(F2_IN(x₁, x₂)) = [1] + [2]x₂   
POL(U4(x₁, x₂, x₃, x₄)) = x₁   
POL(U5'(x₁, x₂, x₃, x₄, x₅)) = [2]x₁   
POL(c1(x₁)) = x₁   
POL(c11(x₁, x₂)) = x₁ + x₂   
POL(c12(x₁)) = x₁   
POL(c14(x₁)) = x₁   
POL(c3(x₁)) = x₁   
POL(c4(x₁)) = x₁   
POL(c9(x₁)) = x₁   
POL(f26_in(x₁, x₂, x₃)) = x₁ + x₂   
POL(f26_out1(x₁)) = [2] + x₁   
POL(leaf(x₁)) = [2]   
POL(tree(x₁, x₂)) = x₁ + x₂   

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(leaf(z0), leaf(z0)) → f2_out1
f2_in(tree(z0, z1), tree(z2, z3)) → U1(f13_in(z0, z1, z2, z3), tree(z0, z1), tree(z2, z3))
U1(f13_out1(z0, z1, z2), tree(z3, z4), tree(z5, z6)) → f2_out1
f13_in(leaf(z0), z1, z2, z3) → U2(f18_in(z2, z3, z0, z1), leaf(z0), z1, z2, z3)
f13_in(tree(z0, z1), z2, z3, z4) → U3(f13_in(z0, tree(z1, z2), z3, z4), tree(z0, z1), z2, z3, z4)
U2(f18_out1(z0), leaf(z1), z2, z3, z4) → f13_out1(z1, z2, z0)
U2(f18_out2(z0, z1, z2), leaf(z3), z4, z5, z6) → f13_out1(z0, z1, z2)
U3(f13_out1(z0, z1, z2), tree(z3, z4), z5, z6, z7) → f13_out1(z0, z1, z2)
f26_in(leaf(z0), z1, z0) → f26_out1(z1)
f26_in(tree(z0, z1), z2, z3) → U4(f26_in(z0, tree(z1, z2), z3), tree(z0, z1), z2, z3)
U4(f26_out1(z0), tree(z1, z2), z3, z4) → f26_out1(z0)
f21_in(z0, z1, z2, z3) → U5(f26_in(z0, z1, z2), z0, z1, z2, z3)
U5(f26_out1(z0), z1, z2, z3, z4) → U6(f2_in(z4, z0), z1, z2, z3, z4, z0)
U6(f2_out1, z0, z1, z2, z3, z4) → f21_out1(z4)
f18_in(z0, z1, z2, z3) → U7(f21_in(z0, z1, z2, z3), f23_in(z2, z3, z0, z1), z0, z1, z2, z3)
U7(f21_out1(z0), z1, z2, z3, z4, z5) → f18_out1(z0)
U7(z0, f23_out1(z1, z2, z3), z4, z5, z6, z7) → f18_out2(z1, z2, z3)

Tuples:

F21_IN(z0, z1, z2, z3) → c11(U5'(f26_in(z0, z1, z2), z0, z1, z2, z3), F26_IN(z0, z1, z2))
F2_IN(tree(z0, z1), tree(z2, z3)) → c1(F13_IN(z0, z1, z2, z3))
F13_IN(leaf(z0), z1, z2, z3) → c3(F18_IN(z2, z3, z0, z1))
F13_IN(tree(z0, z1), z2, z3, z4) → c4(F13_IN(z0, tree(z1, z2), z3, z4))
F26_IN(tree(z0, z1), z2, z3) → c9(F26_IN(z0, tree(z1, z2), z3))
U5'(f26_out1(z0), z1, z2, z3, z4) → c12(F2_IN(z4, z0))
F18_IN(z0, z1, z2, z3) → c14(F21_IN(z0, z1, z2, z3))

S tuples:

F21_IN(z0, z1, z2, z3) → c11(U5'(f26_in(z0, z1, z2), z0, z1, z2, z3), F26_IN(z0, z1, z2))
F13_IN(leaf(z0), z1, z2, z3) → c3(F18_IN(z2, z3, z0, z1))
F13_IN(tree(z0, z1), z2, z3, z4) → c4(F13_IN(z0, tree(z1, z2), z3, z4))
F26_IN(tree(z0, z1), z2, z3) → c9(F26_IN(z0, tree(z1, z2), z3))
F18_IN(z0, z1, z2, z3) → c14(F21_IN(z0, z1, z2, z3))

K tuples:

F2_IN(tree(z0, z1), tree(z2, z3)) → c1(F13_IN(z0, z1, z2, z3))
U5'(f26_out1(z0), z1, z2, z3, z4) → c12(F2_IN(z4, z0))

Defined Rule Symbols:

f2_in, U1, f13_in, U2, U3, f26_in, U4, f21_in, U5, U6, f18_in, U7

Defined Pair Symbols:

F21_IN, F2_IN, F13_IN, F26_IN, U5', F18_IN

Compound Symbols:

c11, c1, c3, c4, c9, c12, c14

(19) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

F13_IN(leaf(z0), z1, z2, z3) → c3(F18_IN(z2, z3, z0, z1))

We considered the (Usable) Rules:

f26_in(leaf(z0), z1, z0) → f26_out1(z1)
f26_in(tree(z0, z1), z2, z3) → U4(f26_in(z0, tree(z1, z2), z3), tree(z0, z1), z2, z3)
U4(f26_out1(z0), tree(z1, z2), z3, z4) → f26_out1(z0)

And the Tuples:

F21_IN(z0, z1, z2, z3) → c11(U5'(f26_in(z0, z1, z2), z0, z1, z2, z3), F26_IN(z0, z1, z2))
F2_IN(tree(z0, z1), tree(z2, z3)) → c1(F13_IN(z0, z1, z2, z3))
F13_IN(leaf(z0), z1, z2, z3) → c3(F18_IN(z2, z3, z0, z1))
F13_IN(tree(z0, z1), z2, z3, z4) → c4(F13_IN(z0, tree(z1, z2), z3, z4))
F26_IN(tree(z0, z1), z2, z3) → c9(F26_IN(z0, tree(z1, z2), z3))
U5'(f26_out1(z0), z1, z2, z3, z4) → c12(F2_IN(z4, z0))
F18_IN(z0, z1, z2, z3) → c14(F21_IN(z0, z1, z2, z3))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(F13_IN(x₁, x₂, x₃, x₄)) = x₁ + x₂   
POL(F18_IN(x₁, x₂, x₃, x₄)) = x₄   
POL(F21_IN(x₁, x₂, x₃, x₄)) = x₄   
POL(F26_IN(x₁, x₂, x₃)) = 0   
POL(F2_IN(x₁, x₂)) = x₁   
POL(U4(x₁, x₂, x₃, x₄)) = 0   
POL(U5'(x₁, x₂, x₃, x₄, x₅)) = x₅   
POL(c1(x₁)) = x₁   
POL(c11(x₁, x₂)) = x₁ + x₂   
POL(c12(x₁)) = x₁   
POL(c14(x₁)) = x₁   
POL(c3(x₁)) = x₁   
POL(c4(x₁)) = x₁   
POL(c9(x₁)) = x₁   
POL(f26_in(x₁, x₂, x₃)) = 0   
POL(f26_out1(x₁)) = 0   
POL(leaf(x₁)) = [1] + x₁   
POL(tree(x₁, x₂)) = x₁ + x₂   

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(leaf(z0), leaf(z0)) → f2_out1
f2_in(tree(z0, z1), tree(z2, z3)) → U1(f13_in(z0, z1, z2, z3), tree(z0, z1), tree(z2, z3))
U1(f13_out1(z0, z1, z2), tree(z3, z4), tree(z5, z6)) → f2_out1
f13_in(leaf(z0), z1, z2, z3) → U2(f18_in(z2, z3, z0, z1), leaf(z0), z1, z2, z3)
f13_in(tree(z0, z1), z2, z3, z4) → U3(f13_in(z0, tree(z1, z2), z3, z4), tree(z0, z1), z2, z3, z4)
U2(f18_out1(z0), leaf(z1), z2, z3, z4) → f13_out1(z1, z2, z0)
U2(f18_out2(z0, z1, z2), leaf(z3), z4, z5, z6) → f13_out1(z0, z1, z2)
U3(f13_out1(z0, z1, z2), tree(z3, z4), z5, z6, z7) → f13_out1(z0, z1, z2)
f26_in(leaf(z0), z1, z0) → f26_out1(z1)
f26_in(tree(z0, z1), z2, z3) → U4(f26_in(z0, tree(z1, z2), z3), tree(z0, z1), z2, z3)
U4(f26_out1(z0), tree(z1, z2), z3, z4) → f26_out1(z0)
f21_in(z0, z1, z2, z3) → U5(f26_in(z0, z1, z2), z0, z1, z2, z3)
U5(f26_out1(z0), z1, z2, z3, z4) → U6(f2_in(z4, z0), z1, z2, z3, z4, z0)
U6(f2_out1, z0, z1, z2, z3, z4) → f21_out1(z4)
f18_in(z0, z1, z2, z3) → U7(f21_in(z0, z1, z2, z3), f23_in(z2, z3, z0, z1), z0, z1, z2, z3)
U7(f21_out1(z0), z1, z2, z3, z4, z5) → f18_out1(z0)
U7(z0, f23_out1(z1, z2, z3), z4, z5, z6, z7) → f18_out2(z1, z2, z3)

Tuples:

F21_IN(z0, z1, z2, z3) → c11(U5'(f26_in(z0, z1, z2), z0, z1, z2, z3), F26_IN(z0, z1, z2))
F2_IN(tree(z0, z1), tree(z2, z3)) → c1(F13_IN(z0, z1, z2, z3))
F13_IN(leaf(z0), z1, z2, z3) → c3(F18_IN(z2, z3, z0, z1))
F13_IN(tree(z0, z1), z2, z3, z4) → c4(F13_IN(z0, tree(z1, z2), z3, z4))
F26_IN(tree(z0, z1), z2, z3) → c9(F26_IN(z0, tree(z1, z2), z3))
U5'(f26_out1(z0), z1, z2, z3, z4) → c12(F2_IN(z4, z0))
F18_IN(z0, z1, z2, z3) → c14(F21_IN(z0, z1, z2, z3))

S tuples:

F21_IN(z0, z1, z2, z3) → c11(U5'(f26_in(z0, z1, z2), z0, z1, z2, z3), F26_IN(z0, z1, z2))
F13_IN(tree(z0, z1), z2, z3, z4) → c4(F13_IN(z0, tree(z1, z2), z3, z4))
F26_IN(tree(z0, z1), z2, z3) → c9(F26_IN(z0, tree(z1, z2), z3))
F18_IN(z0, z1, z2, z3) → c14(F21_IN(z0, z1, z2, z3))

K tuples:

F2_IN(tree(z0, z1), tree(z2, z3)) → c1(F13_IN(z0, z1, z2, z3))
U5'(f26_out1(z0), z1, z2, z3, z4) → c12(F2_IN(z4, z0))
F13_IN(leaf(z0), z1, z2, z3) → c3(F18_IN(z2, z3, z0, z1))

Defined Rule Symbols:

f2_in, U1, f13_in, U2, U3, f26_in, U4, f21_in, U5, U6, f18_in, U7

Defined Pair Symbols:

F21_IN, F2_IN, F13_IN, F26_IN, U5', F18_IN

Compound Symbols:

c11, c1, c3, c4, c9, c12, c14

(21) CdtKnowledgeProof (EQUIVALENT transformation)

The following tuples could be moved from S to K by knowledge propagation:

F18_IN(z0, z1, z2, z3) → c14(F21_IN(z0, z1, z2, z3))
F21_IN(z0, z1, z2, z3) → c11(U5'(f26_in(z0, z1, z2), z0, z1, z2, z3), F26_IN(z0, z1, z2))
U5'(f26_out1(z0), z1, z2, z3, z4) → c12(F2_IN(z4, z0))

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(leaf(z0), leaf(z0)) → f2_out1
f2_in(tree(z0, z1), tree(z2, z3)) → U1(f13_in(z0, z1, z2, z3), tree(z0, z1), tree(z2, z3))
U1(f13_out1(z0, z1, z2), tree(z3, z4), tree(z5, z6)) → f2_out1
f13_in(leaf(z0), z1, z2, z3) → U2(f18_in(z2, z3, z0, z1), leaf(z0), z1, z2, z3)
f13_in(tree(z0, z1), z2, z3, z4) → U3(f13_in(z0, tree(z1, z2), z3, z4), tree(z0, z1), z2, z3, z4)
U2(f18_out1(z0), leaf(z1), z2, z3, z4) → f13_out1(z1, z2, z0)
U2(f18_out2(z0, z1, z2), leaf(z3), z4, z5, z6) → f13_out1(z0, z1, z2)
U3(f13_out1(z0, z1, z2), tree(z3, z4), z5, z6, z7) → f13_out1(z0, z1, z2)
f26_in(leaf(z0), z1, z0) → f26_out1(z1)
f26_in(tree(z0, z1), z2, z3) → U4(f26_in(z0, tree(z1, z2), z3), tree(z0, z1), z2, z3)
U4(f26_out1(z0), tree(z1, z2), z3, z4) → f26_out1(z0)
f21_in(z0, z1, z2, z3) → U5(f26_in(z0, z1, z2), z0, z1, z2, z3)
U5(f26_out1(z0), z1, z2, z3, z4) → U6(f2_in(z4, z0), z1, z2, z3, z4, z0)
U6(f2_out1, z0, z1, z2, z3, z4) → f21_out1(z4)
f18_in(z0, z1, z2, z3) → U7(f21_in(z0, z1, z2, z3), f23_in(z2, z3, z0, z1), z0, z1, z2, z3)
U7(f21_out1(z0), z1, z2, z3, z4, z5) → f18_out1(z0)
U7(z0, f23_out1(z1, z2, z3), z4, z5, z6, z7) → f18_out2(z1, z2, z3)

Tuples:

F21_IN(z0, z1, z2, z3) → c11(U5'(f26_in(z0, z1, z2), z0, z1, z2, z3), F26_IN(z0, z1, z2))
F2_IN(tree(z0, z1), tree(z2, z3)) → c1(F13_IN(z0, z1, z2, z3))
F13_IN(leaf(z0), z1, z2, z3) → c3(F18_IN(z2, z3, z0, z1))
F13_IN(tree(z0, z1), z2, z3, z4) → c4(F13_IN(z0, tree(z1, z2), z3, z4))
F26_IN(tree(z0, z1), z2, z3) → c9(F26_IN(z0, tree(z1, z2), z3))
U5'(f26_out1(z0), z1, z2, z3, z4) → c12(F2_IN(z4, z0))
F18_IN(z0, z1, z2, z3) → c14(F21_IN(z0, z1, z2, z3))

S tuples:

F13_IN(tree(z0, z1), z2, z3, z4) → c4(F13_IN(z0, tree(z1, z2), z3, z4))
F26_IN(tree(z0, z1), z2, z3) → c9(F26_IN(z0, tree(z1, z2), z3))

K tuples:

F2_IN(tree(z0, z1), tree(z2, z3)) → c1(F13_IN(z0, z1, z2, z3))
U5'(f26_out1(z0), z1, z2, z3, z4) → c12(F2_IN(z4, z0))
F13_IN(leaf(z0), z1, z2, z3) → c3(F18_IN(z2, z3, z0, z1))
F18_IN(z0, z1, z2, z3) → c14(F21_IN(z0, z1, z2, z3))
F21_IN(z0, z1, z2, z3) → c11(U5'(f26_in(z0, z1, z2), z0, z1, z2, z3), F26_IN(z0, z1, z2))

Defined Rule Symbols:

f2_in, U1, f13_in, U2, U3, f26_in, U4, f21_in, U5, U6, f18_in, U7

Defined Pair Symbols:

F21_IN, F2_IN, F13_IN, F26_IN, U5', F18_IN

Compound Symbols:

c11, c1, c3, c4, c9, c12, c14

(23) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

F13_IN(tree(z0, z1), z2, z3, z4) → c4(F13_IN(z0, tree(z1, z2), z3, z4))

We considered the (Usable) Rules:

f26_in(leaf(z0), z1, z0) → f26_out1(z1)
f26_in(tree(z0, z1), z2, z3) → U4(f26_in(z0, tree(z1, z2), z3), tree(z0, z1), z2, z3)
U4(f26_out1(z0), tree(z1, z2), z3, z4) → f26_out1(z0)

And the Tuples:

F21_IN(z0, z1, z2, z3) → c11(U5'(f26_in(z0, z1, z2), z0, z1, z2, z3), F26_IN(z0, z1, z2))
F2_IN(tree(z0, z1), tree(z2, z3)) → c1(F13_IN(z0, z1, z2, z3))
F13_IN(leaf(z0), z1, z2, z3) → c3(F18_IN(z2, z3, z0, z1))
F13_IN(tree(z0, z1), z2, z3, z4) → c4(F13_IN(z0, tree(z1, z2), z3, z4))
F26_IN(tree(z0, z1), z2, z3) → c9(F26_IN(z0, tree(z1, z2), z3))
U5'(f26_out1(z0), z1, z2, z3, z4) → c12(F2_IN(z4, z0))
F18_IN(z0, z1, z2, z3) → c14(F21_IN(z0, z1, z2, z3))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(F13_IN(x₁, x₂, x₃, x₄)) = x₁ + x₂·x₄ + x₁·x₄ + x₁·x₃ + x₂·x₃   
POL(F18_IN(x₁, x₂, x₃, x₄)) = [1] + x₁ + x₂ + x₃ + x₂·x₄ + x₁·x₄ + x₁·x₃ + x₂·x₃   
POL(F21_IN(x₁, x₂, x₃, x₄)) = x₁ + x₂ + x₂·x₄ + x₁·x₄ + x₁·x₃ + x₂·x₃   
POL(F26_IN(x₁, x₂, x₃)) = 0   
POL(F2_IN(x₁, x₂)) = [1] + x₁ + x₁·x₂   
POL(U4(x₁, x₂, x₃, x₄)) = x₁   
POL(U5'(x₁, x₂, x₃, x₄, x₅)) = x₁ + x₁·x₅ + x₁·x₄   
POL(c1(x₁)) = x₁   
POL(c11(x₁, x₂)) = x₁ + x₂   
POL(c12(x₁)) = x₁   
POL(c14(x₁)) = x₁   
POL(c3(x₁)) = x₁   
POL(c4(x₁)) = x₁   
POL(c9(x₁)) = x₁   
POL(f26_in(x₁, x₂, x₃)) = x₁ + x₂   
POL(f26_out1(x₁)) = [1] + x₁   
POL(leaf(x₁)) = [1] + x₁   
POL(tree(x₁, x₂)) = [1] + x₁ + x₂   

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(leaf(z0), leaf(z0)) → f2_out1
f2_in(tree(z0, z1), tree(z2, z3)) → U1(f13_in(z0, z1, z2, z3), tree(z0, z1), tree(z2, z3))
U1(f13_out1(z0, z1, z2), tree(z3, z4), tree(z5, z6)) → f2_out1
f13_in(leaf(z0), z1, z2, z3) → U2(f18_in(z2, z3, z0, z1), leaf(z0), z1, z2, z3)
f13_in(tree(z0, z1), z2, z3, z4) → U3(f13_in(z0, tree(z1, z2), z3, z4), tree(z0, z1), z2, z3, z4)
U2(f18_out1(z0), leaf(z1), z2, z3, z4) → f13_out1(z1, z2, z0)
U2(f18_out2(z0, z1, z2), leaf(z3), z4, z5, z6) → f13_out1(z0, z1, z2)
U3(f13_out1(z0, z1, z2), tree(z3, z4), z5, z6, z7) → f13_out1(z0, z1, z2)
f26_in(leaf(z0), z1, z0) → f26_out1(z1)
f26_in(tree(z0, z1), z2, z3) → U4(f26_in(z0, tree(z1, z2), z3), tree(z0, z1), z2, z3)
U4(f26_out1(z0), tree(z1, z2), z3, z4) → f26_out1(z0)
f21_in(z0, z1, z2, z3) → U5(f26_in(z0, z1, z2), z0, z1, z2, z3)
U5(f26_out1(z0), z1, z2, z3, z4) → U6(f2_in(z4, z0), z1, z2, z3, z4, z0)
U6(f2_out1, z0, z1, z2, z3, z4) → f21_out1(z4)
f18_in(z0, z1, z2, z3) → U7(f21_in(z0, z1, z2, z3), f23_in(z2, z3, z0, z1), z0, z1, z2, z3)
U7(f21_out1(z0), z1, z2, z3, z4, z5) → f18_out1(z0)
U7(z0, f23_out1(z1, z2, z3), z4, z5, z6, z7) → f18_out2(z1, z2, z3)

Tuples:

F21_IN(z0, z1, z2, z3) → c11(U5'(f26_in(z0, z1, z2), z0, z1, z2, z3), F26_IN(z0, z1, z2))
F2_IN(tree(z0, z1), tree(z2, z3)) → c1(F13_IN(z0, z1, z2, z3))
F13_IN(leaf(z0), z1, z2, z3) → c3(F18_IN(z2, z3, z0, z1))
F13_IN(tree(z0, z1), z2, z3, z4) → c4(F13_IN(z0, tree(z1, z2), z3, z4))
F26_IN(tree(z0, z1), z2, z3) → c9(F26_IN(z0, tree(z1, z2), z3))
U5'(f26_out1(z0), z1, z2, z3, z4) → c12(F2_IN(z4, z0))
F18_IN(z0, z1, z2, z3) → c14(F21_IN(z0, z1, z2, z3))

S tuples:

F26_IN(tree(z0, z1), z2, z3) → c9(F26_IN(z0, tree(z1, z2), z3))

K tuples:

F2_IN(tree(z0, z1), tree(z2, z3)) → c1(F13_IN(z0, z1, z2, z3))
U5'(f26_out1(z0), z1, z2, z3, z4) → c12(F2_IN(z4, z0))
F13_IN(leaf(z0), z1, z2, z3) → c3(F18_IN(z2, z3, z0, z1))
F18_IN(z0, z1, z2, z3) → c14(F21_IN(z0, z1, z2, z3))
F21_IN(z0, z1, z2, z3) → c11(U5'(f26_in(z0, z1, z2), z0, z1, z2, z3), F26_IN(z0, z1, z2))
F13_IN(tree(z0, z1), z2, z3, z4) → c4(F13_IN(z0, tree(z1, z2), z3, z4))

Defined Rule Symbols:

f2_in, U1, f13_in, U2, U3, f26_in, U4, f21_in, U5, U6, f18_in, U7

Defined Pair Symbols:

F21_IN, F2_IN, F13_IN, F26_IN, U5', F18_IN

Compound Symbols:

c11, c1, c3, c4, c9, c12, c14

(25) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

F26_IN(tree(z0, z1), z2, z3) → c9(F26_IN(z0, tree(z1, z2), z3))

We considered the (Usable) Rules:

f26_in(leaf(z0), z1, z0) → f26_out1(z1)
f26_in(tree(z0, z1), z2, z3) → U4(f26_in(z0, tree(z1, z2), z3), tree(z0, z1), z2, z3)
U4(f26_out1(z0), tree(z1, z2), z3, z4) → f26_out1(z0)

And the Tuples:

F21_IN(z0, z1, z2, z3) → c11(U5'(f26_in(z0, z1, z2), z0, z1, z2, z3), F26_IN(z0, z1, z2))
F2_IN(tree(z0, z1), tree(z2, z3)) → c1(F13_IN(z0, z1, z2, z3))
F13_IN(leaf(z0), z1, z2, z3) → c3(F18_IN(z2, z3, z0, z1))
F13_IN(tree(z0, z1), z2, z3, z4) → c4(F13_IN(z0, tree(z1, z2), z3, z4))
F26_IN(tree(z0, z1), z2, z3) → c9(F26_IN(z0, tree(z1, z2), z3))
U5'(f26_out1(z0), z1, z2, z3, z4) → c12(F2_IN(z4, z0))
F18_IN(z0, z1, z2, z3) → c14(F21_IN(z0, z1, z2, z3))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(F13_IN(x₁, x₂, x₃, x₄)) = [1] + x₁ + x₃ + x₂·x₄ + x₁·x₄ + x₁·x₃ + x₂·x₃   
POL(F18_IN(x₁, x₂, x₃, x₄)) = [1] + x₁ + x₂·x₄ + x₁·x₄   
POL(F21_IN(x₁, x₂, x₃, x₄)) = x₁ + x₂·x₄ + x₁·x₄   
POL(F26_IN(x₁, x₂, x₃)) = x₁   
POL(F2_IN(x₁, x₂)) = x₁·x₂   
POL(U4(x₁, x₂, x₃, x₄)) = x₁   
POL(U5'(x₁, x₂, x₃, x₄, x₅)) = x₁·x₅   
POL(c1(x₁)) = x₁   
POL(c11(x₁, x₂)) = x₁ + x₂   
POL(c12(x₁)) = x₁   
POL(c14(x₁)) = x₁   
POL(c3(x₁)) = x₁   
POL(c4(x₁)) = x₁   
POL(c9(x₁)) = x₁   
POL(f26_in(x₁, x₂, x₃)) = x₁ + x₂   
POL(f26_out1(x₁)) = x₁   
POL(leaf(x₁)) = [1] + x₁   
POL(tree(x₁, x₂)) = [1] + x₁ + x₂   

(26) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(leaf(z0), leaf(z0)) → f2_out1
f2_in(tree(z0, z1), tree(z2, z3)) → U1(f13_in(z0, z1, z2, z3), tree(z0, z1), tree(z2, z3))
U1(f13_out1(z0, z1, z2), tree(z3, z4), tree(z5, z6)) → f2_out1
f13_in(leaf(z0), z1, z2, z3) → U2(f18_in(z2, z3, z0, z1), leaf(z0), z1, z2, z3)
f13_in(tree(z0, z1), z2, z3, z4) → U3(f13_in(z0, tree(z1, z2), z3, z4), tree(z0, z1), z2, z3, z4)
U2(f18_out1(z0), leaf(z1), z2, z3, z4) → f13_out1(z1, z2, z0)
U2(f18_out2(z0, z1, z2), leaf(z3), z4, z5, z6) → f13_out1(z0, z1, z2)
U3(f13_out1(z0, z1, z2), tree(z3, z4), z5, z6, z7) → f13_out1(z0, z1, z2)
f26_in(leaf(z0), z1, z0) → f26_out1(z1)
f26_in(tree(z0, z1), z2, z3) → U4(f26_in(z0, tree(z1, z2), z3), tree(z0, z1), z2, z3)
U4(f26_out1(z0), tree(z1, z2), z3, z4) → f26_out1(z0)
f21_in(z0, z1, z2, z3) → U5(f26_in(z0, z1, z2), z0, z1, z2, z3)
U5(f26_out1(z0), z1, z2, z3, z4) → U6(f2_in(z4, z0), z1, z2, z3, z4, z0)
U6(f2_out1, z0, z1, z2, z3, z4) → f21_out1(z4)
f18_in(z0, z1, z2, z3) → U7(f21_in(z0, z1, z2, z3), f23_in(z2, z3, z0, z1), z0, z1, z2, z3)
U7(f21_out1(z0), z1, z2, z3, z4, z5) → f18_out1(z0)
U7(z0, f23_out1(z1, z2, z3), z4, z5, z6, z7) → f18_out2(z1, z2, z3)

Tuples:

F21_IN(z0, z1, z2, z3) → c11(U5'(f26_in(z0, z1, z2), z0, z1, z2, z3), F26_IN(z0, z1, z2))
F2_IN(tree(z0, z1), tree(z2, z3)) → c1(F13_IN(z0, z1, z2, z3))
F13_IN(leaf(z0), z1, z2, z3) → c3(F18_IN(z2, z3, z0, z1))
F13_IN(tree(z0, z1), z2, z3, z4) → c4(F13_IN(z0, tree(z1, z2), z3, z4))
F26_IN(tree(z0, z1), z2, z3) → c9(F26_IN(z0, tree(z1, z2), z3))
U5'(f26_out1(z0), z1, z2, z3, z4) → c12(F2_IN(z4, z0))
F18_IN(z0, z1, z2, z3) → c14(F21_IN(z0, z1, z2, z3))

S tuples:none
K tuples:

F2_IN(tree(z0, z1), tree(z2, z3)) → c1(F13_IN(z0, z1, z2, z3))
U5'(f26_out1(z0), z1, z2, z3, z4) → c12(F2_IN(z4, z0))
F13_IN(leaf(z0), z1, z2, z3) → c3(F18_IN(z2, z3, z0, z1))
F18_IN(z0, z1, z2, z3) → c14(F21_IN(z0, z1, z2, z3))
F21_IN(z0, z1, z2, z3) → c11(U5'(f26_in(z0, z1, z2), z0, z1, z2, z3), F26_IN(z0, z1, z2))
F13_IN(tree(z0, z1), z2, z3, z4) → c4(F13_IN(z0, tree(z1, z2), z3, z4))
F26_IN(tree(z0, z1), z2, z3) → c9(F26_IN(z0, tree(z1, z2), z3))

Defined Rule Symbols:

f2_in, U1, f13_in, U2, U3, f26_in, U4, f21_in, U5, U6, f18_in, U7

Defined Pair Symbols:

F21_IN, F2_IN, F13_IN, F26_IN, U5', F18_IN

Compound Symbols:

c11, c1, c3, c4, c9, c12, c14

(27) SIsEmptyProof (EQUIVALENT transformation)

The set S is empty

(28) BOUNDS(O(1), O(1))