Runtime Complexity proof of /tmp/tmpYJFgFV/palindrome.pl

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

0 Prolog

↳1 LPReorderTransformerProof (⇔, 0 ms)

↳2 Prolog

↳3 PrologToCdtProblemTransformerProof (UPPER BOUND (ID), 376 ms)

↳4 CdtProblem

    ↳5 CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳6 CdtProblem

    ↳7 CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳8 CdtProblem

    ↳9 CdtKnowledgeProof (⇔, 0 ms)

    ↳10 CdtProblem

↳11 PrologToCdtProblemTransformerProof (UPPER BOUND (ID), 355 ms)

↳12 CdtProblem

    ↳13 CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳14 CdtProblem

    ↳15 CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳16 CdtProblem

    ↳17 CdtKnowledgeProof (⇔, 0 ms)

    ↳18 CdtProblem

    ↳19 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))), 281 ms)

    ↳20 CdtProblem

    ↳21 SIsEmptyProof (⇔, 0 ms)

    ↳22 BOUNDS(O(1), O(1))

(0) Obligation:

Clauses:

palindrome(Xs) :- reverse(Xs, Xs).
reverse(X1s, X2s) :- reverse3(X1s, [], X2s).
reverse3(.(X, X1s), X2s, Ys) :- reverse3(X1s, .(X, X2s), Ys).
reverse3([], Xs, Xs).

Query: palindrome(g)

(1) LPReorderTransformerProof (EQUIVALENT transformation)

Reordered facts before rules in definite LP [PROLOG].

(2) Obligation:

Clauses:

reverse3([], Xs, Xs).
palindrome(Xs) :- reverse(Xs, Xs).
reverse(X1s, X2s) :- reverse3(X1s, [], X2s).
reverse3(.(X, X1s), X2s, Ys) :- reverse3(X1s, .(X, X2s), Ys).

Query: palindrome(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: palindrome(T1)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
4 [label="4: palindrome(T1), SCOPE: 1, CLAUSE: 1\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: reverse(T5, T5)\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: reverse(T5, T5), SCOPE: 2, CLAUSE: 2\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: reverse3(T9, [], T9)\n\nT9 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: reverse3(T9, [], T9), SCOPE: 3, CLAUSE: 0 | reverse3(T9, [], T9), SCOPE: 3, CLAUSE: 3\n\nT9 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: true | reverse3([], [], []), SCOPE: 3, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: reverse3(T9, [], T9), SCOPE: 3, CLAUSE: 3\n\nT9 is ground\nX20 is free\nreverse3(T9, [], T9) !=? reverse3([], X20, X20)", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: reverse3([], [], []), SCOPE: 3, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: reverse3(T15, .(T14, []), .(T14, T15))\n\nT14 is ground\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: reverse3(T15, .(T14, []), .(T14, T15)), SCOPE: 4, CLAUSE: 0 | reverse3(T15, .(T14, []), .(T14, T15)), SCOPE: 4, CLAUSE: 3\n\nT14 is ground\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: true | reverse3([], .(T20, []), .(T20, [])), SCOPE: 4, CLAUSE: 3\n\nT20 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: reverse3(T15, .(T14, []), .(T14, T15)), SCOPE: 4, CLAUSE: 3\n\nT14 is ground\nT15 is ground\nX41 is free\nreverse3(T15, .(T14, []), .(T14, T15)) !=? reverse3([], X41, X41)", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: reverse3([], .(T20, []), .(T20, [])), SCOPE: 4, CLAUSE: 3\n\nT20 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: reverse3(T28, .(T27, .(T29, [])), .(T29, .(T27, T28)))\n\nT27 is ground\nT28 is ground\nT29 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: reverse3(T28, .(T27, .(T29, [])), .(T29, .(T27, T28))), SCOPE: 5, CLAUSE: 0 | reverse3(T28, .(T27, .(T29, [])), .(T29, .(T27, T28))), SCOPE: 5, CLAUSE: 3\n\nT27 is ground\nT28 is ground\nT29 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: true | reverse3([], .(T39, .(T39, [])), .(T39, .(T39, []))), SCOPE: 5, CLAUSE: 3\n\nT39 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: reverse3(T28, .(T27, .(T29, [])), .(T29, .(T27, T28))), SCOPE: 5, CLAUSE: 3\n\nT27 is ground\nT28 is ground\nT29 is ground\nX62 is free\nreverse3(T28, .(T27, .(T29, [])), .(T29, .(T27, T28))) !=? reverse3([], X62, X62)", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: reverse3([], .(T39, .(T39, [])), .(T39, .(T39, []))), SCOPE: 5, CLAUSE: 3\n\nT39 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: reverse3(T49, .(T48, .(T50, .(T51, []))), .(T51, .(T50, .(T48, T49))))\n\nT48 is ground\nT49 is ground\nT50 is ground\nT51 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: reverse3(T49, .(T48, .(T50, .(T51, []))), .(T51, .(T50, .(T48, T49)))), SCOPE: 6, CLAUSE: 0 | reverse3(T49, .(T48, .(T50, .(T51, []))), .(T51, .(T50, .(T48, T49)))), SCOPE: 6, CLAUSE: 3\n\nT48 is ground\nT49 is ground\nT50 is ground\nT51 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: true | reverse3([], .(T66, .(T65, .(T66, []))), .(T66, .(T65, .(T66, [])))), SCOPE: 6, CLAUSE: 3\n\nT66 is ground\nT65 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: reverse3(T49, .(T48, .(T50, .(T51, []))), .(T51, .(T50, .(T48, T49)))), SCOPE: 6, CLAUSE: 3\n\nT48 is ground\nT49 is ground\nT50 is ground\nT51 is ground\nX83 is free\nreverse3(T49, .(T48, .(T50, .(T51, []))), .(T51, .(T50, .(T48, T49)))) !=? reverse3([], X83, X83)", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: reverse3([], .(T66, .(T65, .(T66, []))), .(T66, .(T65, .(T66, [])))), SCOPE: 6, CLAUSE: 3\n\nT66 is ground\nT65 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: reverse3(T78, .(T77, .(T79, .(T80, .(T81, [])))), .(T81, .(T80, .(T79, .(T77, T78)))))\n\nT77 is ground\nT78 is ground\nT79 is ground\nT80 is ground\nT81 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: reverse3(T78, .(T77, .(T79, .(T80, .(T81, [])))), .(T81, .(T80, .(T79, .(T77, T78))))), SCOPE: 7, CLAUSE: 0 | reverse3(T78, .(T77, .(T79, .(T80, .(T81, [])))), .(T81, .(T80, .(T79, .(T77, T78))))), SCOPE: 7, CLAUSE: 3\n\nT77 is ground\nT78 is ground\nT79 is ground\nT80 is ground\nT81 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: true | reverse3([], .(T101, .(T100, .(T100, .(T101, [])))), .(T101, .(T100, .(T100, .(T101, []))))), SCOPE: 7, CLAUSE: 3\n\nT101 is ground\nT100 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: reverse3(T78, .(T77, .(T79, .(T80, .(T81, [])))), .(T81, .(T80, .(T79, .(T77, T78))))), SCOPE: 7, CLAUSE: 3\n\nT77 is ground\nT78 is ground\nT79 is ground\nT80 is ground\nT81 is ground\nX104 is free\nreverse3(T78, .(T77, .(T79, .(T80, .(T81, [])))), .(T81, .(T80, .(T79, .(T77, T78))))) !=? reverse3([], X104, X104)", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: reverse3([], .(T101, .(T100, .(T100, .(T101, [])))), .(T101, .(T100, .(T100, .(T101, []))))), SCOPE: 7, CLAUSE: 3\n\nT101 is ground\nT100 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: reverse3(T115, .(T114, .(T116, .(T117, .(T118, .(T119, []))))), .(T119, .(T118, .(T117, .(T116, .(T114, T115))))))\n\nT114 is ground\nT115 is ground\nT116 is ground\nT117 is ground\nT118 is ground\nT119 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: reverse3(T115, .(T114, .(T116, .(T117, .(T118, .(T119, []))))), .(T119, .(T118, .(T117, .(T116, .(T114, T115)))))), SCOPE: 8, CLAUSE: 0 | reverse3(T115, .(T114, .(T116, .(T117, .(T118, .(T119, []))))), .(T119, .(T118, .(T117, .(T116, .(T114, T115)))))), SCOPE: 8, CLAUSE: 3\n\nT114 is ground\nT115 is ground\nT116 is ground\nT117 is ground\nT118 is ground\nT119 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: true | reverse3([], .(T144, .(T143, .(T142, .(T143, .(T144, []))))), .(T144, .(T143, .(T142, .(T143, .(T144, [])))))), SCOPE: 8, CLAUSE: 3\n\nT144 is ground\nT143 is ground\nT142 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: reverse3(T115, .(T114, .(T116, .(T117, .(T118, .(T119, []))))), .(T119, .(T118, .(T117, .(T116, .(T114, T115)))))), SCOPE: 8, CLAUSE: 3\n\nT114 is ground\nT115 is ground\nT116 is ground\nT117 is ground\nT118 is ground\nT119 is ground\nX125 is free\nreverse3(T115, .(T114, .(T116, .(T117, .(T118, .(T119, []))))), .(T119, .(T118, .(T117, .(T116, .(T114, T115)))))) !=? reverse3([], X125, X125)", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: reverse3([], .(T144, .(T143, .(T142, .(T143, .(T144, []))))), .(T144, .(T143, .(T142, .(T143, .(T144, [])))))), SCOPE: 8, CLAUSE: 3\n\nT144 is ground\nT143 is ground\nT142 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: reverse3(T160, .(T159, .(T161, .(T162, .(T163, .(T164, .(T165, [])))))), .(T165, .(T164, .(T163, .(T162, .(T161, .(T159, T160)))))))\n\nT159 is ground\nT160 is ground\nT161 is ground\nT162 is ground\nT163 is ground\nT164 is ground\nT165 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: reverse3(T160, .(T159, .(T161, .(T162, .(T163, .(T164, .(T165, [])))))), .(T165, .(T164, .(T163, .(T162, .(T161, .(T159, T160))))))), SCOPE: 9, CLAUSE: 0 | reverse3(T160, .(T159, .(T161, .(T162, .(T163, .(T164, .(T165, [])))))), .(T165, .(T164, .(T163, .(T162, .(T161, .(T159, T160))))))), SCOPE: 9, CLAUSE: 3\n\nT159 is ground\nT160 is ground\nT161 is ground\nT162 is ground\nT163 is ground\nT164 is ground\nT165 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: true | reverse3([], .(T195, .(T194, .(T193, .(T193, .(T194, .(T195, [])))))), .(T195, .(T194, .(T193, .(T193, .(T194, .(T195, []))))))), SCOPE: 9, CLAUSE: 3\n\nT195 is ground\nT194 is ground\nT193 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: reverse3(T160, .(T159, .(T161, .(T162, .(T163, .(T164, .(T165, [])))))), .(T165, .(T164, .(T163, .(T162, .(T161, .(T159, T160))))))), SCOPE: 9, CLAUSE: 3\n\nT159 is ground\nT160 is ground\nT161 is ground\nT162 is ground\nT163 is ground\nT164 is ground\nT165 is ground\nX146 is free\nreverse3(T160, .(T159, .(T161, .(T162, .(T163, .(T164, .(T165, [])))))), .(T165, .(T164, .(T163, .(T162, .(T161, .(T159, T160))))))) !=? reverse3([], X146, X146)", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="100: reverse3([], .(T195, .(T194, .(T193, .(T193, .(T194, .(T195, [])))))), .(T195, .(T194, .(T193, .(T193, .(T194, .(T195, []))))))), SCOPE: 9, CLAUSE: 3\n\nT195 is ground\nT194 is ground\nT193 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="101: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
105 [label="105: reverse3(T213, .(T212, .(T214, .(T215, .(T216, .(T217, .(T218, .(T219, []))))))), .(T219, .(T218, .(T217, .(T216, .(T215, .(T214, .(T212, T213))))))))\n\nT212 is ground\nT213 is ground\nT214 is ground\nT215 is ground\nT216 is ground\nT217 is ground\nT218 is ground\nT219 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="109: reverse3(T213, .(T212, .(T214, .(T215, .(T216, .(T217, .(T218, .(T219, []))))))), .(T219, .(T218, .(T217, .(T216, .(T215, .(T214, .(T212, T213)))))))), SCOPE: 10, CLAUSE: 0 | reverse3(T213, .(T212, .(T214, .(T215, .(T216, .(T217, .(T218, .(T219, []))))))), .(T219, .(T218, .(T217, .(T216, .(T215, .(T214, .(T212, T213)))))))), SCOPE: 10, CLAUSE: 3\n\nT212 is ground\nT213 is ground\nT214 is ground\nT215 is ground\nT216 is ground\nT217 is ground\nT218 is ground\nT219 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: true | reverse3([], .(T254, .(T253, .(T252, .(T251, .(T252, .(T253, .(T254, []))))))), .(T254, .(T253, .(T252, .(T251, .(T252, .(T253, .(T254, [])))))))), SCOPE: 10, CLAUSE: 3\n\nT254 is ground\nT253 is ground\nT252 is ground\nT251 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: reverse3(T213, .(T212, .(T214, .(T215, .(T216, .(T217, .(T218, .(T219, []))))))), .(T219, .(T218, .(T217, .(T216, .(T215, .(T214, .(T212, T213)))))))), SCOPE: 10, CLAUSE: 3\n\nT212 is ground\nT213 is ground\nT214 is ground\nT215 is ground\nT216 is ground\nT217 is ground\nT218 is ground\nT219 is ground\nX167 is free\nreverse3(T213, .(T212, .(T214, .(T215, .(T216, .(T217, .(T218, .(T219, []))))))), .(T219, .(T218, .(T217, .(T216, .(T215, .(T214, .(T212, T213)))))))) !=? reverse3([], X167, X167)", fontsize=16, style=filled, fillcolor=lightyellow];
114 [label="114: reverse3([], .(T254, .(T253, .(T252, .(T251, .(T252, .(T253, .(T254, []))))))), .(T254, .(T253, .(T252, .(T251, .(T252, .(T253, .(T254, [])))))))), SCOPE: 10, CLAUSE: 3\n\nT254 is ground\nT253 is ground\nT252 is ground\nT251 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
115 [label="115: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
119 [label="119: reverse3(T274, .(T273, .(T275, .(T276, .(T277, .(T278, .(T279, .(T280, .(T281, [])))))))), .(T281, .(T280, .(T279, .(T278, .(T277, .(T276, .(T275, .(T273, T274)))))))))\n\nT273 is ground\nT274 is ground\nT275 is ground\nT276 is ground\nT277 is ground\nT278 is ground\nT279 is ground\nT280 is ground\nT281 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
121 [label="121: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
123 [label="123: reverse3(T274, .(T273, T298), .(T281, T299))\n\nT273 is ground\nT274 is ground\nT281 is ground\nT298 is ground\nT299 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
125 [label="125: reverse3(T274, .(T273, T298), .(T281, T299)), SCOPE: 11, CLAUSE: 0 | reverse3(T274, .(T273, T298), .(T281, T299)), SCOPE: 11, CLAUSE: 3\n\nT273 is ground\nT274 is ground\nT281 is ground\nT298 is ground\nT299 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
127 [label="127: true | reverse3([], .(T308, T309), .(T308, T309)), SCOPE: 11, CLAUSE: 3\n\nT308 is ground\nT309 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
129 [label="129: reverse3(T274, .(T273, T298), .(T281, T299)), SCOPE: 11, CLAUSE: 3\n\nT273 is ground\nT274 is ground\nT281 is ground\nT298 is ground\nT299 is ground\nX190 is free\nreverse3(T274, .(T273, T298), .(T281, T299)) !=? reverse3([], X190, X190)", fontsize=16, style=filled, fillcolor=lightyellow];
130 [label="130: reverse3([], .(T308, T309), .(T308, T309)), SCOPE: 11, CLAUSE: 3\n\nT308 is ground\nT309 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
133 [label="133: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
135 [label="135: reverse3(T323, .(T322, .(T324, T325)), .(T326, T327))\n\nT322 is ground\nT323 is ground\nT324 is ground\nT325 is ground\nT326 is ground\nT327 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
137 [label="137: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
138 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 138 [arrowhead = none ];
138 -> 4;

139 [label="ONLY EVAL with clause\npalindrome(X5) :- reverse(X5, X5).\nand substitutionT1 -> T5,\nX5 -> T5", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 139 [arrowhead = none ];
139 -> 6;

140 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
6 -> 140 [arrowhead = none ];
140 -> 10;

141 [label="ONLY EVAL with clause\nreverse(X14, X15) :- reverse3(X14, [], X15).\nand substitutionT5 -> T9,\nX14 -> T9,\nX15 -> T9", fontsize=14, style = filled, fillcolor = lightblue];
10 -> 141 [arrowhead = none ];
141 -> 12;

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

143 [label="EVAL with clause\nreverse3([], X20, X20).\nand substitutionT9 -> [],\nX20 -> []", fontsize=14, style = filled, fillcolor = lightblue];
14 -> 143 [arrowhead = none ];
143 -> 15;

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

145 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
15 -> 145 [arrowhead = none ];
145 -> 18;

146 [label="EVAL with clause\nreverse3(.(X33, X34), X35, X36) :- reverse3(X34, .(X33, X35), X36).\nand substitutionX33 -> T14,\nX34 -> T15,\nT9 -> .(T14, T15),\nX35 -> [],\nX36 -> .(T14, T15)", fontsize=14, style = filled, fillcolor = lightblue];
17 -> 146 [arrowhead = none ];
146 -> 21;

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

148 [label="BACKTRACK\nfor clause: reverse3(.(X, X1s), X2s, Ys) :- reverse3(X1s, .(X, X2s), Ys)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
18 -> 148 [arrowhead = none ];
148 -> 19;

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

150 [label="EVAL with clause\nreverse3([], X41, X41).\nand substitutionT15 -> [],\nT14 -> T20,\nX41 -> .(T20, [])", fontsize=14, style = filled, fillcolor = lightblue];
25 -> 150 [arrowhead = none ];
150 -> 27;

151 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
25 -> 151 [arrowhead = none ];
151 -> 29;

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

153 [label="EVAL with clause\nreverse3(.(X54, X55), X56, X57) :- reverse3(X55, .(X54, X56), X57).\nand substitutionX54 -> T27,\nX55 -> T28,\nT15 -> .(T27, T28),\nT14 -> T29,\nX56 -> .(T29, []),\nX57 -> .(T29, .(T27, T28))", fontsize=14, style = filled, fillcolor = lightblue];
29 -> 153 [arrowhead = none ];
153 -> 35;

154 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
29 -> 154 [arrowhead = none ];
154 -> 37;

155 [label="BACKTRACK\nfor clause: reverse3(.(X, X1s), X2s, Ys) :- reverse3(X1s, .(X, X2s), Ys)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
31 -> 155 [arrowhead = none ];
155 -> 33;

156 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
35 -> 156 [arrowhead = none ];
156 -> 39;

157 [label="EVAL with clause\nreverse3([], X62, X62).\nand substitutionT28 -> [],\nT27 -> T39,\nT29 -> T39,\nX62 -> .(T39, .(T39, [])),\nT38 -> T39", fontsize=14, style = filled, fillcolor = lightblue];
39 -> 157 [arrowhead = none ];
157 -> 41;

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

159 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
41 -> 159 [arrowhead = none ];
159 -> 44;

160 [label="EVAL with clause\nreverse3(.(X75, X76), X77, X78) :- reverse3(X76, .(X75, X77), X78).\nand substitutionX75 -> T48,\nX76 -> T49,\nT28 -> .(T48, T49),\nT27 -> T50,\nT29 -> T51,\nX77 -> .(T50, .(T51, [])),\nX78 -> .(T51, .(T50, .(T48, T49)))", fontsize=14, style = filled, fillcolor = lightblue];
43 -> 160 [arrowhead = none ];
160 -> 49;

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

162 [label="BACKTRACK\nfor clause: reverse3(.(X, X1s), X2s, Ys) :- reverse3(X1s, .(X, X2s), Ys)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
44 -> 162 [arrowhead = none ];
162 -> 47;

163 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
49 -> 163 [arrowhead = none ];
163 -> 53;

164 [label="EVAL with clause\nreverse3([], X83, X83).\nand substitutionT49 -> [],\nT48 -> T66,\nT50 -> T65,\nT51 -> T66,\nX83 -> .(T66, .(T65, .(T66, []))),\nT64 -> T66", fontsize=14, style = filled, fillcolor = lightblue];
53 -> 164 [arrowhead = none ];
164 -> 55;

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

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

167 [label="EVAL with clause\nreverse3(.(X96, X97), X98, X99) :- reverse3(X97, .(X96, X98), X99).\nand substitutionX96 -> T77,\nX97 -> T78,\nT49 -> .(T77, T78),\nT48 -> T79,\nT50 -> T80,\nT51 -> T81,\nX98 -> .(T79, .(T80, .(T81, []))),\nX99 -> .(T81, .(T80, .(T79, .(T77, T78))))", fontsize=14, style = filled, fillcolor = lightblue];
57 -> 167 [arrowhead = none ];
167 -> 63;

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

169 [label="BACKTRACK\nfor clause: reverse3(.(X, X1s), X2s, Ys) :- reverse3(X1s, .(X, X2s), Ys)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
58 -> 169 [arrowhead = none ];
169 -> 60;

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

171 [label="EVAL with clause\nreverse3([], X104, X104).\nand substitutionT78 -> [],\nT77 -> T101,\nT79 -> T100,\nT80 -> T100,\nT81 -> T101,\nX104 -> .(T101, .(T100, .(T100, .(T101, [])))),\nT98 -> T101,\nT99 -> T100", fontsize=14, style = filled, fillcolor = lightblue];
67 -> 171 [arrowhead = none ];
171 -> 69;

172 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
67 -> 172 [arrowhead = none ];
172 -> 71;

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

174 [label="EVAL with clause\nreverse3(.(X117, X118), X119, X120) :- reverse3(X118, .(X117, X119), X120).\nand substitutionX117 -> T114,\nX118 -> T115,\nT78 -> .(T114, T115),\nT77 -> T116,\nT79 -> T117,\nT80 -> T118,\nT81 -> T119,\nX119 -> .(T116, .(T117, .(T118, .(T119, [])))),\nX120 -> .(T119, .(T118, .(T117, .(T116, .(T114, T115)))))", fontsize=14, style = filled, fillcolor = lightblue];
71 -> 174 [arrowhead = none ];
174 -> 77;

175 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
71 -> 175 [arrowhead = none ];
175 -> 79;

176 [label="BACKTRACK\nfor clause: reverse3(.(X, X1s), X2s, Ys) :- reverse3(X1s, .(X, X2s), Ys)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
72 -> 176 [arrowhead = none ];
176 -> 73;

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

178 [label="EVAL with clause\nreverse3([], X125, X125).\nand substitutionT115 -> [],\nT114 -> T144,\nT116 -> T143,\nT117 -> T142,\nT118 -> T143,\nT119 -> T144,\nX125 -> .(T144, .(T143, .(T142, .(T143, .(T144, []))))),\nT140 -> T144,\nT141 -> T143", fontsize=14, style = filled, fillcolor = lightblue];
81 -> 178 [arrowhead = none ];
178 -> 83;

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

180 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
83 -> 180 [arrowhead = none ];
180 -> 86;

181 [label="EVAL with clause\nreverse3(.(X138, X139), X140, X141) :- reverse3(X139, .(X138, X140), X141).\nand substitutionX138 -> T159,\nX139 -> T160,\nT115 -> .(T159, T160),\nT114 -> T161,\nT116 -> T162,\nT117 -> T163,\nT118 -> T164,\nT119 -> T165,\nX140 -> .(T161, .(T162, .(T163, .(T164, .(T165, []))))),\nX141 -> .(T165, .(T164, .(T163, .(T162, .(T161, .(T159, T160))))))", fontsize=14, style = filled, fillcolor = lightblue];
85 -> 181 [arrowhead = none ];
181 -> 91;

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

183 [label="BACKTRACK\nfor clause: reverse3(.(X, X1s), X2s, Ys) :- reverse3(X1s, .(X, X2s), Ys)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
86 -> 183 [arrowhead = none ];
183 -> 87;

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

185 [label="EVAL with clause\nreverse3([], X146, X146).\nand substitutionT160 -> [],\nT159 -> T195,\nT161 -> T194,\nT162 -> T193,\nT163 -> T193,\nT164 -> T194,\nT165 -> T195,\nX146 -> .(T195, .(T194, .(T193, .(T193, .(T194, .(T195, [])))))),\nT190 -> T195,\nT191 -> T194,\nT192 -> T193", fontsize=14, style = filled, fillcolor = lightblue];
95 -> 185 [arrowhead = none ];
185 -> 97;

186 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
95 -> 186 [arrowhead = none ];
186 -> 99;

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

188 [label="EVAL with clause\nreverse3(.(X159, X160), X161, X162) :- reverse3(X160, .(X159, X161), X162).\nand substitutionX159 -> T212,\nX160 -> T213,\nT160 -> .(T212, T213),\nT159 -> T214,\nT161 -> T215,\nT162 -> T216,\nT163 -> T217,\nT164 -> T218,\nT165 -> T219,\nX161 -> .(T214, .(T215, .(T216, .(T217, .(T218, .(T219, [])))))),\nX162 -> .(T219, .(T218, .(T217, .(T216, .(T215, .(T214, .(T212, T213)))))))", fontsize=14, style = filled, fillcolor = lightblue];
99 -> 188 [arrowhead = none ];
188 -> 105;

189 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
99 -> 189 [arrowhead = none ];
189 -> 107;

190 [label="BACKTRACK\nfor clause: reverse3(.(X, X1s), X2s, Ys) :- reverse3(X1s, .(X, X2s), Ys)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
100 -> 190 [arrowhead = none ];
190 -> 101;

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

192 [label="EVAL with clause\nreverse3([], X167, X167).\nand substitutionT213 -> [],\nT212 -> T254,\nT214 -> T253,\nT215 -> T252,\nT216 -> T251,\nT217 -> T252,\nT218 -> T253,\nT219 -> T254,\nX167 -> .(T254, .(T253, .(T252, .(T251, .(T252, .(T253, .(T254, []))))))),\nT248 -> T254,\nT249 -> T253,\nT250 -> T252", fontsize=14, style = filled, fillcolor = lightblue];
109 -> 192 [arrowhead = none ];
192 -> 111;

193 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
109 -> 193 [arrowhead = none ];
193 -> 113;

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

195 [label="EVAL with clause\nreverse3(.(X180, X181), X182, X183) :- reverse3(X181, .(X180, X182), X183).\nand substitutionX180 -> T273,\nX181 -> T274,\nT213 -> .(T273, T274),\nT212 -> T275,\nT214 -> T276,\nT215 -> T277,\nT216 -> T278,\nT217 -> T279,\nT218 -> T280,\nT219 -> T281,\nX182 -> .(T275, .(T276, .(T277, .(T278, .(T279, .(T280, .(T281, []))))))),\nX183 -> .(T281, .(T280, .(T279, .(T278, .(T277, .(T276, .(T275, .(T273, T274))))))))", fontsize=14, style = filled, fillcolor = lightblue];
113 -> 195 [arrowhead = none ];
195 -> 119;

196 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
113 -> 196 [arrowhead = none ];
196 -> 121;

197 [label="BACKTRACK\nfor clause: reverse3(.(X, X1s), X2s, Ys) :- reverse3(X1s, .(X, X2s), Ys)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
114 -> 197 [arrowhead = none ];
197 -> 115;

198 [label="GENERALIZATION\nT298 <-- .(T275, .(T276, .(T277, .(T278, .(T279, .(T280, .(T281, [])))))))\nT299 <-- .(T280, .(T279, .(T278, .(T277, .(T276, .(T275, .(T273, T274)))))))\n\nNew Knowledge:\nT298 is ground\nT299 is ground", fontsize=14, style = filled, fillcolor = violet];
119 -> 198 [arrowhead = none ];
198 -> 123;

199 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
123 -> 199 [arrowhead = none ];
199 -> 125;

200 [label="EVAL with clause\nreverse3([], X190, X190).\nand substitutionT274 -> [],\nT273 -> T308,\nT298 -> T309,\nX190 -> .(T308, T309),\nT281 -> T308,\nT299 -> T309", fontsize=14, style = filled, fillcolor = lightblue];
125 -> 200 [arrowhead = none ];
200 -> 127;

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

202 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
127 -> 202 [arrowhead = none ];
202 -> 130;

203 [label="EVAL with clause\nreverse3(.(X203, X204), X205, X206) :- reverse3(X204, .(X203, X205), X206).\nand substitutionX203 -> T322,\nX204 -> T323,\nT274 -> .(T322, T323),\nT273 -> T324,\nT298 -> T325,\nX205 -> .(T324, T325),\nT281 -> T326,\nT299 -> T327,\nX206 -> .(T326, T327)", fontsize=14, style = filled, fillcolor = lightblue];
129 -> 203 [arrowhead = none ];
203 -> 135;

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

205 [label="BACKTRACK\nfor clause: reverse3(.(X, X1s), X2s, Ys) :- reverse3(X1s, .(X, X2s), Ys)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
130 -> 205 [arrowhead = none ];
205 -> 133;

206 [label="INSTANCE with matching:\nT274 -> T323\nT273 -> T322\nT298 -> .(T324, T325)\nT281 -> T326\nT299 -> T327", fontsize=14, style = filled, fillcolor = lightgrey];
135 -> 206 [arrowhead = none , style=dashed];
206 -> 123[style=dashed];

}

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in([]) → f1_out1
f1_in(.(z0, [])) → f1_out1
f1_in(.(z0, .(z0, []))) → f1_out1
f1_in(.(z0, .(z1, .(z0, [])))) → f1_out1
f1_in(.(z0, .(z1, .(z1, .(z0, []))))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z1, .(z0, [])))))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z2, .(z1, .(z0, []))))))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z3, .(z2, .(z1, .(z0, [])))))))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → U1(f123_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
U1(f123_out1, .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → f1_out1
f123_in([], z0, z1, z0, z1) → f123_out1
f123_in(.(z0, z1), z2, z3, z4, z5) → U2(f123_in(z1, z0, .(z2, z3), z4, z5), .(z0, z1), z2, z3, z4, z5)
U2(f123_out1, .(z0, z1), z2, z3, z4, z5) → f123_out1

Tuples:

F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c8(U1'(f123_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))), F123_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
F123_IN(.(z0, z1), z2, z3, z4, z5) → c11(U2'(f123_in(z1, z0, .(z2, z3), z4, z5), .(z0, z1), z2, z3, z4, z5), F123_IN(z1, z0, .(z2, z3), z4, z5))

S tuples:

F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c8(U1'(f123_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))), F123_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
F123_IN(.(z0, z1), z2, z3, z4, z5) → c11(U2'(f123_in(z1, z0, .(z2, z3), z4, z5), .(z0, z1), z2, z3, z4, z5), F123_IN(z1, z0, .(z2, z3), z4, z5))

K tuples:none
Defined Rule Symbols:

f1_in, U1, f123_in, U2

Defined Pair Symbols:

F1_IN, F123_IN

Compound Symbols:

c8, c11

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

Split RHS of tuples not part of any SCC

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in([]) → f1_out1
f1_in(.(z0, [])) → f1_out1
f1_in(.(z0, .(z0, []))) → f1_out1
f1_in(.(z0, .(z1, .(z0, [])))) → f1_out1
f1_in(.(z0, .(z1, .(z1, .(z0, []))))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z1, .(z0, [])))))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z2, .(z1, .(z0, []))))))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z3, .(z2, .(z1, .(z0, [])))))))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → U1(f123_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
U1(f123_out1, .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → f1_out1
f123_in([], z0, z1, z0, z1) → f123_out1
f123_in(.(z0, z1), z2, z3, z4, z5) → U2(f123_in(z1, z0, .(z2, z3), z4, z5), .(z0, z1), z2, z3, z4, z5)
U2(f123_out1, .(z0, z1), z2, z3, z4, z5) → f123_out1

Tuples:

F123_IN(.(z0, z1), z2, z3, z4, z5) → c11(U2'(f123_in(z1, z0, .(z2, z3), z4, z5), .(z0, z1), z2, z3, z4, z5), F123_IN(z1, z0, .(z2, z3), z4, z5))
F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(U1'(f123_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))))
F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F123_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))

S tuples:

F123_IN(.(z0, z1), z2, z3, z4, z5) → c11(U2'(f123_in(z1, z0, .(z2, z3), z4, z5), .(z0, z1), z2, z3, z4, z5), F123_IN(z1, z0, .(z2, z3), z4, z5))
F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(U1'(f123_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))))
F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F123_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))

K tuples:none
Defined Rule Symbols:

f1_in, U1, f123_in, U2

Defined Pair Symbols:

F123_IN, F1_IN

Compound Symbols:

c11, c

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

Removed 2 trailing tuple parts

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in([]) → f1_out1
f1_in(.(z0, [])) → f1_out1
f1_in(.(z0, .(z0, []))) → f1_out1
f1_in(.(z0, .(z1, .(z0, [])))) → f1_out1
f1_in(.(z0, .(z1, .(z1, .(z0, []))))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z1, .(z0, [])))))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z2, .(z1, .(z0, []))))))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z3, .(z2, .(z1, .(z0, [])))))))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → U1(f123_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
U1(f123_out1, .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → f1_out1
f123_in([], z0, z1, z0, z1) → f123_out1
f123_in(.(z0, z1), z2, z3, z4, z5) → U2(f123_in(z1, z0, .(z2, z3), z4, z5), .(z0, z1), z2, z3, z4, z5)
U2(f123_out1, .(z0, z1), z2, z3, z4, z5) → f123_out1

Tuples:

F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F123_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
F123_IN(.(z0, z1), z2, z3, z4, z5) → c11(F123_IN(z1, z0, .(z2, z3), z4, z5))
F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c

S tuples:

F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F123_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
F123_IN(.(z0, z1), z2, z3, z4, z5) → c11(F123_IN(z1, z0, .(z2, z3), z4, z5))
F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c

K tuples:none
Defined Rule Symbols:

f1_in, U1, f123_in, U2

Defined Pair Symbols:

F1_IN, F123_IN

Compound Symbols:

c, c11, c

(9) CdtKnowledgeProof (EQUIVALENT transformation)

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

F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F123_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in([]) → f1_out1
f1_in(.(z0, [])) → f1_out1
f1_in(.(z0, .(z0, []))) → f1_out1
f1_in(.(z0, .(z1, .(z0, [])))) → f1_out1
f1_in(.(z0, .(z1, .(z1, .(z0, []))))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z1, .(z0, [])))))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z2, .(z1, .(z0, []))))))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z3, .(z2, .(z1, .(z0, [])))))))) → f1_out1
f1_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → U1(f123_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
U1(f123_out1, .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → f1_out1
f123_in([], z0, z1, z0, z1) → f123_out1
f123_in(.(z0, z1), z2, z3, z4, z5) → U2(f123_in(z1, z0, .(z2, z3), z4, z5), .(z0, z1), z2, z3, z4, z5)
U2(f123_out1, .(z0, z1), z2, z3, z4, z5) → f123_out1

Tuples:

F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F123_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
F123_IN(.(z0, z1), z2, z3, z4, z5) → c11(F123_IN(z1, z0, .(z2, z3), z4, z5))
F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c

S tuples:

F123_IN(.(z0, z1), z2, z3, z4, z5) → c11(F123_IN(z1, z0, .(z2, z3), z4, z5))

K tuples:

F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F123_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
F1_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c

Defined Rule Symbols:

f1_in, U1, f123_in, U2

Defined Pair Symbols:

F1_IN, F123_IN

Compound Symbols:

c, c11, c

(11) 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: palindrome(T1)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
3 [label="3: palindrome(T1), SCOPE: 1, CLAUSE: 1\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: reverse(T3, T3)\n\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: reverse(T3, T3), SCOPE: 2, CLAUSE: 2\n\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: reverse3(T6, [], T6)\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: reverse3(T6, [], T6), SCOPE: 3, CLAUSE: 0 | reverse3(T6, [], T6), SCOPE: 3, CLAUSE: 3\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: true | reverse3([], [], []), SCOPE: 3, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: reverse3(T6, [], T6), SCOPE: 3, CLAUSE: 3\n\nT6 is ground\nX15 is free\nreverse3(T6, [], T6) !=? reverse3([], X15, X15)", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: reverse3([], [], []), SCOPE: 3, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: reverse3(T12, .(T11, []), .(T11, T12))\n\nT11 is ground\nT12 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: reverse3(T12, .(T11, []), .(T11, T12)), SCOPE: 4, CLAUSE: 0 | reverse3(T12, .(T11, []), .(T11, T12)), SCOPE: 4, CLAUSE: 3\n\nT11 is ground\nT12 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: true | reverse3([], .(T17, []), .(T17, [])), SCOPE: 4, CLAUSE: 3\n\nT17 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: reverse3(T12, .(T11, []), .(T11, T12)), SCOPE: 4, CLAUSE: 3\n\nT11 is ground\nT12 is ground\nX36 is free\nreverse3(T12, .(T11, []), .(T11, T12)) !=? reverse3([], X36, X36)", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: reverse3([], .(T17, []), .(T17, [])), SCOPE: 4, CLAUSE: 3\n\nT17 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: reverse3(T25, .(T24, .(T26, [])), .(T26, .(T24, T25)))\n\nT24 is ground\nT25 is ground\nT26 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: reverse3(T25, .(T24, .(T26, [])), .(T26, .(T24, T25))), SCOPE: 5, CLAUSE: 0 | reverse3(T25, .(T24, .(T26, [])), .(T26, .(T24, T25))), SCOPE: 5, CLAUSE: 3\n\nT24 is ground\nT25 is ground\nT26 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: true | reverse3([], .(T36, .(T36, [])), .(T36, .(T36, []))), SCOPE: 5, CLAUSE: 3\n\nT36 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: reverse3(T25, .(T24, .(T26, [])), .(T26, .(T24, T25))), SCOPE: 5, CLAUSE: 3\n\nT24 is ground\nT25 is ground\nT26 is ground\nX57 is free\nreverse3(T25, .(T24, .(T26, [])), .(T26, .(T24, T25))) !=? reverse3([], X57, X57)", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: reverse3([], .(T36, .(T36, [])), .(T36, .(T36, []))), SCOPE: 5, CLAUSE: 3\n\nT36 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: reverse3(T46, .(T45, .(T47, .(T48, []))), .(T48, .(T47, .(T45, T46))))\n\nT45 is ground\nT46 is ground\nT47 is ground\nT48 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: reverse3(T46, .(T45, .(T47, .(T48, []))), .(T48, .(T47, .(T45, T46)))), SCOPE: 6, CLAUSE: 0 | reverse3(T46, .(T45, .(T47, .(T48, []))), .(T48, .(T47, .(T45, T46)))), SCOPE: 6, CLAUSE: 3\n\nT45 is ground\nT46 is ground\nT47 is ground\nT48 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: true | reverse3([], .(T63, .(T62, .(T63, []))), .(T63, .(T62, .(T63, [])))), SCOPE: 6, CLAUSE: 3\n\nT63 is ground\nT62 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: reverse3(T46, .(T45, .(T47, .(T48, []))), .(T48, .(T47, .(T45, T46)))), SCOPE: 6, CLAUSE: 3\n\nT45 is ground\nT46 is ground\nT47 is ground\nT48 is ground\nX78 is free\nreverse3(T46, .(T45, .(T47, .(T48, []))), .(T48, .(T47, .(T45, T46)))) !=? reverse3([], X78, X78)", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: reverse3([], .(T63, .(T62, .(T63, []))), .(T63, .(T62, .(T63, [])))), SCOPE: 6, CLAUSE: 3\n\nT63 is ground\nT62 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: reverse3(T75, .(T74, .(T76, .(T77, .(T78, [])))), .(T78, .(T77, .(T76, .(T74, T75)))))\n\nT74 is ground\nT75 is ground\nT76 is ground\nT77 is ground\nT78 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: reverse3(T75, .(T74, .(T76, .(T77, .(T78, [])))), .(T78, .(T77, .(T76, .(T74, T75))))), SCOPE: 7, CLAUSE: 0 | reverse3(T75, .(T74, .(T76, .(T77, .(T78, [])))), .(T78, .(T77, .(T76, .(T74, T75))))), SCOPE: 7, CLAUSE: 3\n\nT74 is ground\nT75 is ground\nT76 is ground\nT77 is ground\nT78 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: true | reverse3([], .(T98, .(T97, .(T97, .(T98, [])))), .(T98, .(T97, .(T97, .(T98, []))))), SCOPE: 7, CLAUSE: 3\n\nT98 is ground\nT97 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: reverse3(T75, .(T74, .(T76, .(T77, .(T78, [])))), .(T78, .(T77, .(T76, .(T74, T75))))), SCOPE: 7, CLAUSE: 3\n\nT74 is ground\nT75 is ground\nT76 is ground\nT77 is ground\nT78 is ground\nX99 is free\nreverse3(T75, .(T74, .(T76, .(T77, .(T78, [])))), .(T78, .(T77, .(T76, .(T74, T75))))) !=? reverse3([], X99, X99)", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: reverse3([], .(T98, .(T97, .(T97, .(T98, [])))), .(T98, .(T97, .(T97, .(T98, []))))), SCOPE: 7, CLAUSE: 3\n\nT98 is ground\nT97 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: reverse3(T112, .(T111, .(T113, .(T114, .(T115, .(T116, []))))), .(T116, .(T115, .(T114, .(T113, .(T111, T112))))))\n\nT111 is ground\nT112 is ground\nT113 is ground\nT114 is ground\nT115 is ground\nT116 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: reverse3(T112, .(T111, .(T113, .(T114, .(T115, .(T116, []))))), .(T116, .(T115, .(T114, .(T113, .(T111, T112)))))), SCOPE: 8, CLAUSE: 0 | reverse3(T112, .(T111, .(T113, .(T114, .(T115, .(T116, []))))), .(T116, .(T115, .(T114, .(T113, .(T111, T112)))))), SCOPE: 8, CLAUSE: 3\n\nT111 is ground\nT112 is ground\nT113 is ground\nT114 is ground\nT115 is ground\nT116 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: true | reverse3([], .(T141, .(T140, .(T139, .(T140, .(T141, []))))), .(T141, .(T140, .(T139, .(T140, .(T141, [])))))), SCOPE: 8, CLAUSE: 3\n\nT141 is ground\nT140 is ground\nT139 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: reverse3(T112, .(T111, .(T113, .(T114, .(T115, .(T116, []))))), .(T116, .(T115, .(T114, .(T113, .(T111, T112)))))), SCOPE: 8, CLAUSE: 3\n\nT111 is ground\nT112 is ground\nT113 is ground\nT114 is ground\nT115 is ground\nT116 is ground\nX120 is free\nreverse3(T112, .(T111, .(T113, .(T114, .(T115, .(T116, []))))), .(T116, .(T115, .(T114, .(T113, .(T111, T112)))))) !=? reverse3([], X120, X120)", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: reverse3([], .(T141, .(T140, .(T139, .(T140, .(T141, []))))), .(T141, .(T140, .(T139, .(T140, .(T141, [])))))), SCOPE: 8, CLAUSE: 3\n\nT141 is ground\nT140 is ground\nT139 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: reverse3(T157, .(T156, .(T158, .(T159, .(T160, .(T161, .(T162, [])))))), .(T162, .(T161, .(T160, .(T159, .(T158, .(T156, T157)))))))\n\nT156 is ground\nT157 is ground\nT158 is ground\nT159 is ground\nT160 is ground\nT161 is ground\nT162 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: reverse3(T157, .(T156, .(T158, .(T159, .(T160, .(T161, .(T162, [])))))), .(T162, .(T161, .(T160, .(T159, .(T158, .(T156, T157))))))), SCOPE: 9, CLAUSE: 0 | reverse3(T157, .(T156, .(T158, .(T159, .(T160, .(T161, .(T162, [])))))), .(T162, .(T161, .(T160, .(T159, .(T158, .(T156, T157))))))), SCOPE: 9, CLAUSE: 3\n\nT156 is ground\nT157 is ground\nT158 is ground\nT159 is ground\nT160 is ground\nT161 is ground\nT162 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: true | reverse3([], .(T192, .(T191, .(T190, .(T190, .(T191, .(T192, [])))))), .(T192, .(T191, .(T190, .(T190, .(T191, .(T192, []))))))), SCOPE: 9, CLAUSE: 3\n\nT192 is ground\nT191 is ground\nT190 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="102: reverse3(T157, .(T156, .(T158, .(T159, .(T160, .(T161, .(T162, [])))))), .(T162, .(T161, .(T160, .(T159, .(T158, .(T156, T157))))))), SCOPE: 9, CLAUSE: 3\n\nT156 is ground\nT157 is ground\nT158 is ground\nT159 is ground\nT160 is ground\nT161 is ground\nT162 is ground\nX141 is free\nreverse3(T157, .(T156, .(T158, .(T159, .(T160, .(T161, .(T162, [])))))), .(T162, .(T161, .(T160, .(T159, .(T158, .(T156, T157))))))) !=? reverse3([], X141, X141)", fontsize=16, style=filled, fillcolor=lightyellow];
103 [label="103: reverse3([], .(T192, .(T191, .(T190, .(T190, .(T191, .(T192, [])))))), .(T192, .(T191, .(T190, .(T190, .(T191, .(T192, []))))))), SCOPE: 9, CLAUSE: 3\n\nT192 is ground\nT191 is ground\nT190 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="106: reverse3(T210, .(T209, .(T211, .(T212, .(T213, .(T214, .(T215, .(T216, []))))))), .(T216, .(T215, .(T214, .(T213, .(T212, .(T211, .(T209, T210))))))))\n\nT209 is ground\nT210 is ground\nT211 is ground\nT212 is ground\nT213 is ground\nT214 is ground\nT215 is ground\nT216 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="108: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: reverse3(T210, .(T209, .(T211, .(T212, .(T213, .(T214, .(T215, .(T216, []))))))), .(T216, .(T215, .(T214, .(T213, .(T212, .(T211, .(T209, T210)))))))), SCOPE: 10, CLAUSE: 0 | reverse3(T210, .(T209, .(T211, .(T212, .(T213, .(T214, .(T215, .(T216, []))))))), .(T216, .(T215, .(T214, .(T213, .(T212, .(T211, .(T209, T210)))))))), SCOPE: 10, CLAUSE: 3\n\nT209 is ground\nT210 is ground\nT211 is ground\nT212 is ground\nT213 is ground\nT214 is ground\nT215 is ground\nT216 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: true | reverse3([], .(T251, .(T250, .(T249, .(T248, .(T249, .(T250, .(T251, []))))))), .(T251, .(T250, .(T249, .(T248, .(T249, .(T250, .(T251, [])))))))), SCOPE: 10, CLAUSE: 3\n\nT251 is ground\nT250 is ground\nT249 is ground\nT248 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
116 [label="116: reverse3(T210, .(T209, .(T211, .(T212, .(T213, .(T214, .(T215, .(T216, []))))))), .(T216, .(T215, .(T214, .(T213, .(T212, .(T211, .(T209, T210)))))))), SCOPE: 10, CLAUSE: 3\n\nT209 is ground\nT210 is ground\nT211 is ground\nT212 is ground\nT213 is ground\nT214 is ground\nT215 is ground\nT216 is ground\nX162 is free\nreverse3(T210, .(T209, .(T211, .(T212, .(T213, .(T214, .(T215, .(T216, []))))))), .(T216, .(T215, .(T214, .(T213, .(T212, .(T211, .(T209, T210)))))))) !=? reverse3([], X162, X162)", fontsize=16, style=filled, fillcolor=lightyellow];
117 [label="117: reverse3([], .(T251, .(T250, .(T249, .(T248, .(T249, .(T250, .(T251, []))))))), .(T251, .(T250, .(T249, .(T248, .(T249, .(T250, .(T251, [])))))))), SCOPE: 10, CLAUSE: 3\n\nT251 is ground\nT250 is ground\nT249 is ground\nT248 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="118: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
120 [label="120: reverse3(T271, .(T270, .(T272, .(T273, .(T274, .(T275, .(T276, .(T277, .(T278, [])))))))), .(T278, .(T277, .(T276, .(T275, .(T274, .(T273, .(T272, .(T270, T271)))))))))\n\nT270 is ground\nT271 is ground\nT272 is ground\nT273 is ground\nT274 is ground\nT275 is ground\nT276 is ground\nT277 is ground\nT278 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
122 [label="122: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
124 [label="124: reverse3(T271, .(T270, T295), .(T278, T296))\n\nT270 is ground\nT271 is ground\nT278 is ground\nT295 is ground\nT296 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
126 [label="126: reverse3(T271, .(T270, T295), .(T278, T296)), SCOPE: 11, CLAUSE: 0 | reverse3(T271, .(T270, T295), .(T278, T296)), SCOPE: 11, CLAUSE: 3\n\nT270 is ground\nT271 is ground\nT278 is ground\nT295 is ground\nT296 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
128 [label="128: true | reverse3([], .(T305, T306), .(T305, T306)), SCOPE: 11, CLAUSE: 3\n\nT305 is ground\nT306 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
131 [label="131: reverse3(T271, .(T270, T295), .(T278, T296)), SCOPE: 11, CLAUSE: 3\n\nT270 is ground\nT271 is ground\nT278 is ground\nT295 is ground\nT296 is ground\nX185 is free\nreverse3(T271, .(T270, T295), .(T278, T296)) !=? reverse3([], X185, X185)", fontsize=16, style=filled, fillcolor=lightyellow];
132 [label="132: reverse3([], .(T305, T306), .(T305, T306)), SCOPE: 11, CLAUSE: 3\n\nT305 is ground\nT306 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
134 [label="134: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
136 [label="136: reverse3(T320, .(T319, .(T321, T322)), .(T323, T324))\n\nT319 is ground\nT320 is ground\nT321 is ground\nT322 is ground\nT323 is ground\nT324 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
138 [label="138: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
139 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
2 -> 139 [arrowhead = none ];
139 -> 3;

140 [label="ONLY EVAL with clause\npalindrome(X2) :- reverse(X2, X2).\nand substitutionT1 -> T3,\nX2 -> T3", fontsize=14, style = filled, fillcolor = lightblue];
3 -> 140 [arrowhead = none ];
140 -> 5;

141 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
5 -> 141 [arrowhead = none ];
141 -> 7;

142 [label="ONLY EVAL with clause\nreverse(X9, X10) :- reverse3(X9, [], X10).\nand substitutionT3 -> T6,\nX9 -> T6,\nX10 -> T6", fontsize=14, style = filled, fillcolor = lightblue];
7 -> 142 [arrowhead = none ];
142 -> 8;

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

144 [label="EVAL with clause\nreverse3([], X15, X15).\nand substitutionT6 -> [],\nX15 -> []", fontsize=14, style = filled, fillcolor = lightblue];
9 -> 144 [arrowhead = none ];
144 -> 11;

145 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
9 -> 145 [arrowhead = none ];
145 -> 13;

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

147 [label="EVAL with clause\nreverse3(.(X28, X29), X30, X31) :- reverse3(X29, .(X28, X30), X31).\nand substitutionX28 -> T11,\nX29 -> T12,\nT6 -> .(T11, T12),\nX30 -> [],\nX31 -> .(T11, T12)", fontsize=14, style = filled, fillcolor = lightblue];
13 -> 147 [arrowhead = none ];
147 -> 22;

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

149 [label="BACKTRACK\nfor clause: reverse3(.(X, X1s), X2s, Ys) :- reverse3(X1s, .(X, X2s), Ys)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
16 -> 149 [arrowhead = none ];
149 -> 20;

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

151 [label="EVAL with clause\nreverse3([], X36, X36).\nand substitutionT12 -> [],\nT11 -> T17,\nX36 -> .(T17, [])", fontsize=14, style = filled, fillcolor = lightblue];
26 -> 151 [arrowhead = none ];
151 -> 28;

152 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
26 -> 152 [arrowhead = none ];
152 -> 30;

153 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
28 -> 153 [arrowhead = none ];
153 -> 32;

154 [label="EVAL with clause\nreverse3(.(X49, X50), X51, X52) :- reverse3(X50, .(X49, X51), X52).\nand substitutionX49 -> T24,\nX50 -> T25,\nT12 -> .(T24, T25),\nT11 -> T26,\nX51 -> .(T26, []),\nX52 -> .(T26, .(T24, T25))", fontsize=14, style = filled, fillcolor = lightblue];
30 -> 154 [arrowhead = none ];
154 -> 36;

155 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
30 -> 155 [arrowhead = none ];
155 -> 38;

156 [label="BACKTRACK\nfor clause: reverse3(.(X, X1s), X2s, Ys) :- reverse3(X1s, .(X, X2s), Ys)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
32 -> 156 [arrowhead = none ];
156 -> 34;

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

158 [label="EVAL with clause\nreverse3([], X57, X57).\nand substitutionT25 -> [],\nT24 -> T36,\nT26 -> T36,\nX57 -> .(T36, .(T36, [])),\nT35 -> T36", fontsize=14, style = filled, fillcolor = lightblue];
40 -> 158 [arrowhead = none ];
158 -> 42;

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

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

161 [label="EVAL with clause\nreverse3(.(X70, X71), X72, X73) :- reverse3(X71, .(X70, X72), X73).\nand substitutionX70 -> T45,\nX71 -> T46,\nT25 -> .(T45, T46),\nT24 -> T47,\nT26 -> T48,\nX72 -> .(T47, .(T48, [])),\nX73 -> .(T48, .(T47, .(T45, T46)))", fontsize=14, style = filled, fillcolor = lightblue];
45 -> 161 [arrowhead = none ];
161 -> 50;

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

163 [label="BACKTRACK\nfor clause: reverse3(.(X, X1s), X2s, Ys) :- reverse3(X1s, .(X, X2s), Ys)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
46 -> 163 [arrowhead = none ];
163 -> 48;

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

165 [label="EVAL with clause\nreverse3([], X78, X78).\nand substitutionT46 -> [],\nT45 -> T63,\nT47 -> T62,\nT48 -> T63,\nX78 -> .(T63, .(T62, .(T63, []))),\nT61 -> T63", fontsize=14, style = filled, fillcolor = lightblue];
54 -> 165 [arrowhead = none ];
165 -> 56;

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

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

168 [label="EVAL with clause\nreverse3(.(X91, X92), X93, X94) :- reverse3(X92, .(X91, X93), X94).\nand substitutionX91 -> T74,\nX92 -> T75,\nT46 -> .(T74, T75),\nT45 -> T76,\nT47 -> T77,\nT48 -> T78,\nX93 -> .(T76, .(T77, .(T78, []))),\nX94 -> .(T78, .(T77, .(T76, .(T74, T75))))", fontsize=14, style = filled, fillcolor = lightblue];
59 -> 168 [arrowhead = none ];
168 -> 64;

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

170 [label="BACKTRACK\nfor clause: reverse3(.(X, X1s), X2s, Ys) :- reverse3(X1s, .(X, X2s), Ys)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
61 -> 170 [arrowhead = none ];
170 -> 62;

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

172 [label="EVAL with clause\nreverse3([], X99, X99).\nand substitutionT75 -> [],\nT74 -> T98,\nT76 -> T97,\nT77 -> T97,\nT78 -> T98,\nX99 -> .(T98, .(T97, .(T97, .(T98, [])))),\nT95 -> T98,\nT96 -> T97", fontsize=14, style = filled, fillcolor = lightblue];
68 -> 172 [arrowhead = none ];
172 -> 70;

173 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
68 -> 173 [arrowhead = none ];
173 -> 74;

174 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
70 -> 174 [arrowhead = none ];
174 -> 75;

175 [label="EVAL with clause\nreverse3(.(X112, X113), X114, X115) :- reverse3(X113, .(X112, X114), X115).\nand substitutionX112 -> T111,\nX113 -> T112,\nT75 -> .(T111, T112),\nT74 -> T113,\nT76 -> T114,\nT77 -> T115,\nT78 -> T116,\nX114 -> .(T113, .(T114, .(T115, .(T116, [])))),\nX115 -> .(T116, .(T115, .(T114, .(T113, .(T111, T112)))))", fontsize=14, style = filled, fillcolor = lightblue];
74 -> 175 [arrowhead = none ];
175 -> 78;

176 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
74 -> 176 [arrowhead = none ];
176 -> 80;

177 [label="BACKTRACK\nfor clause: reverse3(.(X, X1s), X2s, Ys) :- reverse3(X1s, .(X, X2s), Ys)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
75 -> 177 [arrowhead = none ];
177 -> 76;

178 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
78 -> 178 [arrowhead = none ];
178 -> 82;

179 [label="EVAL with clause\nreverse3([], X120, X120).\nand substitutionT112 -> [],\nT111 -> T141,\nT113 -> T140,\nT114 -> T139,\nT115 -> T140,\nT116 -> T141,\nX120 -> .(T141, .(T140, .(T139, .(T140, .(T141, []))))),\nT137 -> T141,\nT138 -> T140", fontsize=14, style = filled, fillcolor = lightblue];
82 -> 179 [arrowhead = none ];
179 -> 84;

180 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
82 -> 180 [arrowhead = none ];
180 -> 88;

181 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
84 -> 181 [arrowhead = none ];
181 -> 89;

182 [label="EVAL with clause\nreverse3(.(X133, X134), X135, X136) :- reverse3(X134, .(X133, X135), X136).\nand substitutionX133 -> T156,\nX134 -> T157,\nT112 -> .(T156, T157),\nT111 -> T158,\nT113 -> T159,\nT114 -> T160,\nT115 -> T161,\nT116 -> T162,\nX135 -> .(T158, .(T159, .(T160, .(T161, .(T162, []))))),\nX136 -> .(T162, .(T161, .(T160, .(T159, .(T158, .(T156, T157))))))", fontsize=14, style = filled, fillcolor = lightblue];
88 -> 182 [arrowhead = none ];
182 -> 92;

183 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
88 -> 183 [arrowhead = none ];
183 -> 94;

184 [label="BACKTRACK\nfor clause: reverse3(.(X, X1s), X2s, Ys) :- reverse3(X1s, .(X, X2s), Ys)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
89 -> 184 [arrowhead = none ];
184 -> 90;

185 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
92 -> 185 [arrowhead = none ];
185 -> 96;

186 [label="EVAL with clause\nreverse3([], X141, X141).\nand substitutionT157 -> [],\nT156 -> T192,\nT158 -> T191,\nT159 -> T190,\nT160 -> T190,\nT161 -> T191,\nT162 -> T192,\nX141 -> .(T192, .(T191, .(T190, .(T190, .(T191, .(T192, [])))))),\nT187 -> T192,\nT188 -> T191,\nT189 -> T190", fontsize=14, style = filled, fillcolor = lightblue];
96 -> 186 [arrowhead = none ];
186 -> 98;

187 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
96 -> 187 [arrowhead = none ];
187 -> 102;

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

189 [label="EVAL with clause\nreverse3(.(X154, X155), X156, X157) :- reverse3(X155, .(X154, X156), X157).\nand substitutionX154 -> T209,\nX155 -> T210,\nT157 -> .(T209, T210),\nT156 -> T211,\nT158 -> T212,\nT159 -> T213,\nT160 -> T214,\nT161 -> T215,\nT162 -> T216,\nX156 -> .(T211, .(T212, .(T213, .(T214, .(T215, .(T216, [])))))),\nX157 -> .(T216, .(T215, .(T214, .(T213, .(T212, .(T211, .(T209, T210)))))))", fontsize=14, style = filled, fillcolor = lightblue];
102 -> 189 [arrowhead = none ];
189 -> 106;

190 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
102 -> 190 [arrowhead = none ];
190 -> 108;

191 [label="BACKTRACK\nfor clause: reverse3(.(X, X1s), X2s, Ys) :- reverse3(X1s, .(X, X2s), Ys)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
103 -> 191 [arrowhead = none ];
191 -> 104;

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

193 [label="EVAL with clause\nreverse3([], X162, X162).\nand substitutionT210 -> [],\nT209 -> T251,\nT211 -> T250,\nT212 -> T249,\nT213 -> T248,\nT214 -> T249,\nT215 -> T250,\nT216 -> T251,\nX162 -> .(T251, .(T250, .(T249, .(T248, .(T249, .(T250, .(T251, []))))))),\nT245 -> T251,\nT246 -> T250,\nT247 -> T249", fontsize=14, style = filled, fillcolor = lightblue];
110 -> 193 [arrowhead = none ];
193 -> 112;

194 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
110 -> 194 [arrowhead = none ];
194 -> 116;

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

196 [label="EVAL with clause\nreverse3(.(X175, X176), X177, X178) :- reverse3(X176, .(X175, X177), X178).\nand substitutionX175 -> T270,\nX176 -> T271,\nT210 -> .(T270, T271),\nT209 -> T272,\nT211 -> T273,\nT212 -> T274,\nT213 -> T275,\nT214 -> T276,\nT215 -> T277,\nT216 -> T278,\nX177 -> .(T272, .(T273, .(T274, .(T275, .(T276, .(T277, .(T278, []))))))),\nX178 -> .(T278, .(T277, .(T276, .(T275, .(T274, .(T273, .(T272, .(T270, T271))))))))", fontsize=14, style = filled, fillcolor = lightblue];
116 -> 196 [arrowhead = none ];
196 -> 120;

197 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
116 -> 197 [arrowhead = none ];
197 -> 122;

198 [label="BACKTRACK\nfor clause: reverse3(.(X, X1s), X2s, Ys) :- reverse3(X1s, .(X, X2s), Ys)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
117 -> 198 [arrowhead = none ];
198 -> 118;

199 [label="GENERALIZATION\nT295 <-- .(T272, .(T273, .(T274, .(T275, .(T276, .(T277, .(T278, [])))))))\nT296 <-- .(T277, .(T276, .(T275, .(T274, .(T273, .(T272, .(T270, T271)))))))\n\nNew Knowledge:\nT295 is ground\nT296 is ground", fontsize=14, style = filled, fillcolor = violet];
120 -> 199 [arrowhead = none ];
199 -> 124;

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

201 [label="EVAL with clause\nreverse3([], X185, X185).\nand substitutionT271 -> [],\nT270 -> T305,\nT295 -> T306,\nX185 -> .(T305, T306),\nT278 -> T305,\nT296 -> T306", fontsize=14, style = filled, fillcolor = lightblue];
126 -> 201 [arrowhead = none ];
201 -> 128;

202 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
126 -> 202 [arrowhead = none ];
202 -> 131;

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

204 [label="EVAL with clause\nreverse3(.(X198, X199), X200, X201) :- reverse3(X199, .(X198, X200), X201).\nand substitutionX198 -> T319,\nX199 -> T320,\nT271 -> .(T319, T320),\nT270 -> T321,\nT295 -> T322,\nX200 -> .(T321, T322),\nT278 -> T323,\nT296 -> T324,\nX201 -> .(T323, T324)", fontsize=14, style = filled, fillcolor = lightblue];
131 -> 204 [arrowhead = none ];
204 -> 136;

205 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
131 -> 205 [arrowhead = none ];
205 -> 138;

206 [label="BACKTRACK\nfor clause: reverse3(.(X, X1s), X2s, Ys) :- reverse3(X1s, .(X, X2s), Ys)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
132 -> 206 [arrowhead = none ];
206 -> 134;

207 [label="INSTANCE with matching:\nT271 -> T320\nT270 -> T319\nT295 -> .(T321, T322)\nT278 -> T323\nT296 -> T324", fontsize=14, style = filled, fillcolor = lightgrey];
136 -> 207 [arrowhead = none , style=dashed];
207 -> 124[style=dashed];

}

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in([]) → f2_out1
f2_in(.(z0, [])) → f2_out1
f2_in(.(z0, .(z0, []))) → f2_out1
f2_in(.(z0, .(z1, .(z0, [])))) → f2_out1
f2_in(.(z0, .(z1, .(z1, .(z0, []))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z1, .(z0, [])))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z2, .(z1, .(z0, []))))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z3, .(z2, .(z1, .(z0, [])))))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → U1(f124_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
U1(f124_out1, .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → f2_out1
f124_in([], z0, z1, z0, z1) → f124_out1
f124_in(.(z0, z1), z2, z3, z4, z5) → U2(f124_in(z1, z0, .(z2, z3), z4, z5), .(z0, z1), z2, z3, z4, z5)
U2(f124_out1, .(z0, z1), z2, z3, z4, z5) → f124_out1

Tuples:

F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c8(U1'(f124_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))), F124_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
F124_IN(.(z0, z1), z2, z3, z4, z5) → c11(U2'(f124_in(z1, z0, .(z2, z3), z4, z5), .(z0, z1), z2, z3, z4, z5), F124_IN(z1, z0, .(z2, z3), z4, z5))

S tuples:

F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c8(U1'(f124_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))), F124_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
F124_IN(.(z0, z1), z2, z3, z4, z5) → c11(U2'(f124_in(z1, z0, .(z2, z3), z4, z5), .(z0, z1), z2, z3, z4, z5), F124_IN(z1, z0, .(z2, z3), z4, z5))

K tuples:none
Defined Rule Symbols:

f2_in, U1, f124_in, U2

Defined Pair Symbols:

F2_IN, F124_IN

Compound Symbols:

c8, c11

(13) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)

Split RHS of tuples not part of any SCC

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in([]) → f2_out1
f2_in(.(z0, [])) → f2_out1
f2_in(.(z0, .(z0, []))) → f2_out1
f2_in(.(z0, .(z1, .(z0, [])))) → f2_out1
f2_in(.(z0, .(z1, .(z1, .(z0, []))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z1, .(z0, [])))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z2, .(z1, .(z0, []))))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z3, .(z2, .(z1, .(z0, [])))))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → U1(f124_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
U1(f124_out1, .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → f2_out1
f124_in([], z0, z1, z0, z1) → f124_out1
f124_in(.(z0, z1), z2, z3, z4, z5) → U2(f124_in(z1, z0, .(z2, z3), z4, z5), .(z0, z1), z2, z3, z4, z5)
U2(f124_out1, .(z0, z1), z2, z3, z4, z5) → f124_out1

Tuples:

F124_IN(.(z0, z1), z2, z3, z4, z5) → c11(U2'(f124_in(z1, z0, .(z2, z3), z4, z5), .(z0, z1), z2, z3, z4, z5), F124_IN(z1, z0, .(z2, z3), z4, z5))
F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(U1'(f124_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))))
F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F124_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))

S tuples:

F124_IN(.(z0, z1), z2, z3, z4, z5) → c11(U2'(f124_in(z1, z0, .(z2, z3), z4, z5), .(z0, z1), z2, z3, z4, z5), F124_IN(z1, z0, .(z2, z3), z4, z5))
F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(U1'(f124_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))))
F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F124_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))

K tuples:none
Defined Rule Symbols:

f2_in, U1, f124_in, U2

Defined Pair Symbols:

F124_IN, F2_IN

Compound Symbols:

c11, c

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

Removed 2 trailing tuple parts

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in([]) → f2_out1
f2_in(.(z0, [])) → f2_out1
f2_in(.(z0, .(z0, []))) → f2_out1
f2_in(.(z0, .(z1, .(z0, [])))) → f2_out1
f2_in(.(z0, .(z1, .(z1, .(z0, []))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z1, .(z0, [])))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z2, .(z1, .(z0, []))))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z3, .(z2, .(z1, .(z0, [])))))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → U1(f124_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
U1(f124_out1, .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → f2_out1
f124_in([], z0, z1, z0, z1) → f124_out1
f124_in(.(z0, z1), z2, z3, z4, z5) → U2(f124_in(z1, z0, .(z2, z3), z4, z5), .(z0, z1), z2, z3, z4, z5)
U2(f124_out1, .(z0, z1), z2, z3, z4, z5) → f124_out1

Tuples:

F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F124_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
F124_IN(.(z0, z1), z2, z3, z4, z5) → c11(F124_IN(z1, z0, .(z2, z3), z4, z5))
F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c

S tuples:

F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F124_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
F124_IN(.(z0, z1), z2, z3, z4, z5) → c11(F124_IN(z1, z0, .(z2, z3), z4, z5))
F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c

K tuples:none
Defined Rule Symbols:

f2_in, U1, f124_in, U2

Defined Pair Symbols:

F2_IN, F124_IN

Compound Symbols:

c, c11, c

(17) CdtKnowledgeProof (EQUIVALENT transformation)

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

F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F124_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in([]) → f2_out1
f2_in(.(z0, [])) → f2_out1
f2_in(.(z0, .(z0, []))) → f2_out1
f2_in(.(z0, .(z1, .(z0, [])))) → f2_out1
f2_in(.(z0, .(z1, .(z1, .(z0, []))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z1, .(z0, [])))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z2, .(z1, .(z0, []))))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z3, .(z2, .(z1, .(z0, [])))))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → U1(f124_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
U1(f124_out1, .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → f2_out1
f124_in([], z0, z1, z0, z1) → f124_out1
f124_in(.(z0, z1), z2, z3, z4, z5) → U2(f124_in(z1, z0, .(z2, z3), z4, z5), .(z0, z1), z2, z3, z4, z5)
U2(f124_out1, .(z0, z1), z2, z3, z4, z5) → f124_out1

Tuples:

F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F124_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
F124_IN(.(z0, z1), z2, z3, z4, z5) → c11(F124_IN(z1, z0, .(z2, z3), z4, z5))
F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c

S tuples:

F124_IN(.(z0, z1), z2, z3, z4, z5) → c11(F124_IN(z1, z0, .(z2, z3), z4, z5))

K tuples:

F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F124_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c

Defined Rule Symbols:

f2_in, U1, f124_in, U2

Defined Pair Symbols:

F2_IN, F124_IN

Compound Symbols:

c, c11, c

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

F124_IN(.(z0, z1), z2, z3, z4, z5) → c11(F124_IN(z1, z0, .(z2, z3), z4, z5))

We considered the (Usable) Rules:none
And the Tuples:

F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F124_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
F124_IN(.(z0, z1), z2, z3, z4, z5) → c11(F124_IN(z1, z0, .(z2, z3), z4, z5))
F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c

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

POL(.(x₁, x₂)) = [2] + x₁ + x₂
POL(F124_IN(x₁, x₂, x₃, x₄, x₅)) = x₁ + x₄
POL(F2_IN(x₁)) = x₁
POL([]) = 0
POL(c) = 0
POL(c(x₁)) = x₁
POL(c11(x₁)) = x₁

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in([]) → f2_out1
f2_in(.(z0, [])) → f2_out1
f2_in(.(z0, .(z0, []))) → f2_out1
f2_in(.(z0, .(z1, .(z0, [])))) → f2_out1
f2_in(.(z0, .(z1, .(z1, .(z0, []))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z1, .(z0, [])))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z2, .(z1, .(z0, []))))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z3, .(z2, .(z1, .(z0, [])))))))) → f2_out1
f2_in(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → U1(f124_in(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))), .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
U1(f124_out1, .(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → f2_out1
f124_in([], z0, z1, z0, z1) → f124_out1
f124_in(.(z0, z1), z2, z3, z4, z5) → U2(f124_in(z1, z0, .(z2, z3), z4, z5), .(z0, z1), z2, z3, z4, z5)
U2(f124_out1, .(z0, z1), z2, z3, z4, z5) → f124_out1

Tuples:

F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F124_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
F124_IN(.(z0, z1), z2, z3, z4, z5) → c11(F124_IN(z1, z0, .(z2, z3), z4, z5))
F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c

S tuples:none
K tuples:

F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c(F124_IN(z8, z7, .(z6, .(z5, .(z4, .(z3, .(z2, .(z1, .(z0, []))))))), z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8)))))))))
F2_IN(.(z0, .(z1, .(z2, .(z3, .(z4, .(z5, .(z6, .(z7, z8))))))))) → c
F124_IN(.(z0, z1), z2, z3, z4, z5) → c11(F124_IN(z1, z0, .(z2, z3), z4, z5))

Defined Rule Symbols:

f2_in, U1, f124_in, U2

Defined Pair Symbols:

F2_IN, F124_IN

Compound Symbols:

c, c11, c

(21) SIsEmptyProof (EQUIVALENT transformation)

The set S is empty

(0) Obligation:

(1) LPReorderTransformerProof (EQUIVALENT transformation)

(2) Obligation:

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

(4) Obligation:

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

(6) Obligation:

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

(8) Obligation:

(9) CdtKnowledgeProof (EQUIVALENT transformation)

(10) Obligation:

(11) PrologToCdtProblemTransformerProof (UPPER BOUND (ID) transformation)

(12) Obligation:

(13) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)

(14) Obligation:

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

(16) Obligation:

(17) CdtKnowledgeProof (EQUIVALENT transformation)

(18) Obligation:

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

(20) Obligation:

(21) SIsEmptyProof (EQUIVALENT transformation)

(22) BOUNDS(O(1), O(1))