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

(0) Obligation:

Clauses:

fold(X, [], X).
fold(X, Y, Z) :- ','(no(empty(Y)), ','(head(Y, H), ','(tail(Y, T), ','(myop(X, H, V), fold(V, T, Z))))).
myop(a, b, c).
head([], X1).
head(.(H, X2), H).
tail([], []).
tail(.(X3, T), T).
empty([]).
no(X) :- ','(X, ','(!, failure(a))).
no(X4).
failure(b).

Query: fold(g,g,a)

(1) 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: fold(T1, T2, T3)\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
3 [label="3: fold(T1, T2, T3), SCOPE: 1, CLAUSE: 0 | fold(T1, T2, T3), SCOPE: 1, CLAUSE: 1\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: true | fold(T5, [], T3), SCOPE: 1, CLAUSE: 1\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: fold(T1, T2, T3), SCOPE: 1, CLAUSE: 1\n\nT1 is ground\nT2 is ground\nX6 is free\nfold(T1, T2, T3) !=? fold(X6, [], X6)", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: fold(T5, [], T3), SCOPE: 1, CLAUSE: 1\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: ','(no(empty([])), ','(head([], X13), ','(tail([], X14), ','(myop(T8, X13, X15), fold(X15, X14, T10)))))\n\nT8 is ground\nX13 is free\nX14 is free\nX15 is free", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: ','(no(empty([])), ','(head([], X13), ','(tail([], X14), ','(myop(T8, X13, X15), fold(X15, X14, T10))))), SCOPE: 2, CLAUSE: 8 | ','(no(empty([])), ','(head([], X13), ','(tail([], X14), ','(myop(T8, X13, X15), fold(X15, X14, T10))))), SCOPE: 2, CLAUSE: 9\n\nT8 is ground\nX13 is free\nX14 is free\nX15 is free", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: ','(','(call(empty([])), ','(!_2, failure(a))), ','(head([], X13), ','(tail([], X14), ','(myop(T8, X13, X15), fold(X15, X14, T10))))) | ','(no(empty([])), ','(head([], X13), ','(tail([], X14), ','(myop(T8, X13, X15), fold(X15, X14, T10))))), SCOPE: 2, CLAUSE: 9\n\nT8 is ground\nX13 is free\nX14 is free\nX15 is free", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: ','(empty([]), ','(','(!_2, failure(a)), ','(head([], X13), ','(tail([], X14), ','(myop(T8, X13, X15), fold(X15, X14, T10)))))) | ?_3 | ','(no(empty([])), ','(head([], X13), ','(tail([], X14), ','(myop(T8, X13, X15), fold(X15, X14, T10))))), SCOPE: 2, CLAUSE: 9\n\nT8 is ground\nX13 is free\nX14 is free\nX15 is free", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: ','(empty([]), ','(','(!_2, failure(a)), ','(head([], X13), ','(tail([], X14), ','(myop(T8, X13, X15), fold(X15, X14, T10)))))), SCOPE: 4, CLAUSE: 7 | ?_4 | ?_3 | ','(no(empty([])), ','(head([], X13), ','(tail([], X14), ','(myop(T8, X13, X15), fold(X15, X14, T10))))), SCOPE: 2, CLAUSE: 9\n\nT8 is ground\nX13 is free\nX14 is free\nX15 is free", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: ','(','(!_2, failure(a)), ','(head([], X13), ','(tail([], X14), ','(myop(T8, X13, X15), fold(X15, X14, T10))))) | ?_4 | ?_3 | ','(no(empty([])), ','(head([], X13), ','(tail([], X14), ','(myop(T8, X13, X15), fold(X15, X14, T10))))), SCOPE: 2, CLAUSE: 9\n\nT8 is ground\nX13 is free\nX14 is free\nX15 is free", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: ','(failure(a), ','(head([], X13), ','(tail([], X14), ','(myop(T8, X13, X15), fold(X15, X14, T10)))))\n\nT8 is ground\nX13 is free\nX14 is free\nX15 is free", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: ','(failure(a), ','(head([], X13), ','(tail([], X14), ','(myop(T8, X13, X15), fold(X15, X14, T10))))), SCOPE: 5, CLAUSE: 10\n\nT8 is ground\nX13 is free\nX14 is free\nX15 is free", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: ','(no(empty(T16)), ','(head(T16, X27), ','(tail(T16, X28), ','(myop(T15, X27, X29), fold(X29, X28, T18)))))\n\nT15 is ground\nT16 is ground\nX6 is free\nX27 is free\nX28 is free\nX29 is free\nfold(T15, T16, T3) !=? fold(X6, [], X6)", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: ','(no(empty(T16)), ','(head(T16, X27), ','(tail(T16, X28), ','(myop(T15, X27, X29), fold(X29, X28, T18))))), SCOPE: 6, CLAUSE: 8 | ','(no(empty(T16)), ','(head(T16, X27), ','(tail(T16, X28), ','(myop(T15, X27, X29), fold(X29, X28, T18))))), SCOPE: 6, CLAUSE: 9\n\nT15 is ground\nT16 is ground\nX6 is free\nX27 is free\nX28 is free\nX29 is free\nfold(T15, T16, T3) !=? fold(X6, [], X6)", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: ','(','(call(empty(T21)), ','(!_6, failure(a))), ','(head(T21, X27), ','(tail(T21, X28), ','(myop(T15, X27, X29), fold(X29, X28, T18))))) | ','(no(empty(T21)), ','(head(T21, X27), ','(tail(T21, X28), ','(myop(T15, X27, X29), fold(X29, X28, T18))))), SCOPE: 6, CLAUSE: 9\n\nT15 is ground\nT21 is ground\nX6 is free\nX27 is free\nX28 is free\nX29 is free\nfold(T15, T21, T3) !=? fold(X6, [], X6)", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: ','(empty(T21), ','(','(!_6, failure(a)), ','(head(T21, X27), ','(tail(T21, X28), ','(myop(T15, X27, X29), fold(X29, X28, T18)))))) | ?_7 | ','(no(empty(T21)), ','(head(T21, X27), ','(tail(T21, X28), ','(myop(T15, X27, X29), fold(X29, X28, T18))))), SCOPE: 6, CLAUSE: 9\n\nT15 is ground\nT21 is ground\nX6 is free\nX27 is free\nX28 is free\nX29 is free\nfold(T15, T21, T3) !=? fold(X6, [], X6)", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: ','(empty(T21), ','(','(!_6, failure(a)), ','(head(T21, X27), ','(tail(T21, X28), ','(myop(T15, X27, X29), fold(X29, X28, T18)))))), SCOPE: 8, CLAUSE: 7 | ?_8 | ?_7 | ','(no(empty(T21)), ','(head(T21, X27), ','(tail(T21, X28), ','(myop(T15, X27, X29), fold(X29, X28, T18))))), SCOPE: 6, CLAUSE: 9\n\nT15 is ground\nT21 is ground\nX6 is free\nX27 is free\nX28 is free\nX29 is free\nfold(T15, T21, T3) !=? fold(X6, [], X6)", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: ','(','(!_6, failure(a)), ','(head([], X27), ','(tail([], X28), ','(myop(T15, X27, X29), fold(X29, X28, T18))))) | ?_8 | ?_7 | ','(no(empty([])), ','(head([], X27), ','(tail([], X28), ','(myop(T15, X27, X29), fold(X29, X28, T18))))), SCOPE: 6, CLAUSE: 9\n\nT15 is ground\nX6 is free\nX27 is free\nX28 is free\nX29 is free\nfold(T15, [], T3) !=? fold(X6, [], X6)", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: ?_8 | ?_7 | ','(no(empty(T21)), ','(head(T21, X27), ','(tail(T21, X28), ','(myop(T15, X27, X29), fold(X29, X28, T18))))), SCOPE: 6, CLAUSE: 9\n\nT15 is ground\nT21 is ground\nX6 is free\nX27 is free\nX28 is free\nX29 is free\nfold(T15, T21, T3) !=? fold(X6, [], X6)\nempty(T21) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: ','(failure(a), ','(head([], X27), ','(tail([], X28), ','(myop(T15, X27, X29), fold(X29, X28, T18)))))\n\nT15 is ground\nX6 is free\nX27 is free\nX28 is free\nX29 is free\nfold(T15, [], T3) !=? fold(X6, [], X6)", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: ','(failure(a), ','(head([], X27), ','(tail([], X28), ','(myop(T15, X27, X29), fold(X29, X28, T18))))), SCOPE: 9, CLAUSE: 10\n\nT15 is ground\nX6 is free\nX27 is free\nX28 is free\nX29 is free\nfold(T15, [], T3) !=? fold(X6, [], X6)", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: ?_7 | ','(no(empty(T21)), ','(head(T21, X27), ','(tail(T21, X28), ','(myop(T15, X27, X29), fold(X29, X28, T18))))), SCOPE: 6, CLAUSE: 9\n\nT15 is ground\nT21 is ground\nX6 is free\nX27 is free\nX28 is free\nX29 is free\nfold(T15, T21, T3) !=? fold(X6, [], X6)\nempty(T21) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: ','(no(empty(T21)), ','(head(T21, X27), ','(tail(T21, X28), ','(myop(T15, X27, X29), fold(X29, X28, T18))))), SCOPE: 6, CLAUSE: 9\n\nT15 is ground\nT21 is ground\nX6 is free\nX27 is free\nX28 is free\nX29 is free\nfold(T15, T21, T3) !=? fold(X6, [], X6)\nempty(T21) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: ','(head(T26, X27), ','(tail(T26, X28), ','(myop(T15, X27, X29), fold(X29, X28, T18))))\n\nT15 is ground\nT26 is ground\nX6 is free\nX27 is free\nX28 is free\nX29 is free\nfold(T15, T26, T3) !=? fold(X6, [], X6)\nempty(T26) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: ','(head(T26, X27), ','(tail(T26, X28), ','(myop(T15, X27, X29), fold(X29, X28, T18)))), SCOPE: 10, CLAUSE: 3 | ','(head(T26, X27), ','(tail(T26, X28), ','(myop(T15, X27, X29), fold(X29, X28, T18)))), SCOPE: 10, CLAUSE: 4\n\nT15 is ground\nT26 is ground\nX6 is free\nX27 is free\nX28 is free\nX29 is free\nfold(T15, T26, T3) !=? fold(X6, [], X6)\nempty(T26) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: ','(head(T26, X27), ','(tail(T26, X28), ','(myop(T15, X27, X29), fold(X29, X28, T18)))), SCOPE: 10, CLAUSE: 4\n\nT15 is ground\nT26 is ground\nX6 is free\nX27 is free\nX28 is free\nX29 is free\nfold(T15, T26, T3) !=? fold(X6, [], X6)\nempty(T26) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: ','(tail(.(T32, T33), X28), ','(myop(T15, T32, X29), fold(X29, X28, T18)))\n\nT15 is ground\nT32 is ground\nT33 is ground\nX28 is free\nX29 is free", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: ','(tail(.(T32, T33), X28), ','(myop(T15, T32, X29), fold(X29, X28, T18))), SCOPE: 11, CLAUSE: 5 | ','(tail(.(T32, T33), X28), ','(myop(T15, T32, X29), fold(X29, X28, T18))), SCOPE: 11, CLAUSE: 6\n\nT15 is ground\nT32 is ground\nT33 is ground\nX28 is free\nX29 is free", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: ','(tail(.(T32, T33), X28), ','(myop(T15, T32, X29), fold(X29, X28, T18))), SCOPE: 11, CLAUSE: 6\n\nT15 is ground\nT32 is ground\nT33 is ground\nX28 is free\nX29 is free", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: ','(myop(T15, T41, X29), fold(X29, T42, T18))\n\nT15 is ground\nT41 is ground\nT42 is ground\nX29 is free", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: ','(myop(T15, T41, X29), fold(X29, T42, T18)), SCOPE: 12, CLAUSE: 2\n\nT15 is ground\nT41 is ground\nT42 is ground\nX29 is free", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: fold(c, T42, T18)\n\nT42 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: fold(c, T42, T18), SCOPE: 13, CLAUSE: 0 | fold(c, T42, T18), SCOPE: 13, CLAUSE: 1\n\nT42 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: true | fold(c, [], T18), SCOPE: 13, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: fold(c, T42, T18), SCOPE: 13, CLAUSE: 1\n\nT42 is ground\nX70 is free\nfold(c, T42, T18) !=? fold(X70, [], X70)", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: fold(c, [], T18), SCOPE: 13, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: ','(no(empty([])), ','(head([], X85), ','(tail([], X86), ','(myop(c, X85, X87), fold(X87, X86, T50)))))\n\nX85 is free\nX86 is free\nX87 is free", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: ','(no(empty([])), ','(head([], X85), ','(tail([], X86), ','(myop(c, X85, X87), fold(X87, X86, T50))))), SCOPE: 14, CLAUSE: 8 | ','(no(empty([])), ','(head([], X85), ','(tail([], X86), ','(myop(c, X85, X87), fold(X87, X86, T50))))), SCOPE: 14, CLAUSE: 9\n\nX85 is free\nX86 is free\nX87 is free", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: ','(','(call(empty([])), ','(!_14, failure(a))), ','(head([], X85), ','(tail([], X86), ','(myop(c, X85, X87), fold(X87, X86, T50))))) | ','(no(empty([])), ','(head([], X85), ','(tail([], X86), ','(myop(c, X85, X87), fold(X87, X86, T50))))), SCOPE: 14, CLAUSE: 9\n\nX85 is free\nX86 is free\nX87 is free", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: ','(empty([]), ','(','(!_14, failure(a)), ','(head([], X85), ','(tail([], X86), ','(myop(c, X85, X87), fold(X87, X86, T50)))))) | ?_15 | ','(no(empty([])), ','(head([], X85), ','(tail([], X86), ','(myop(c, X85, X87), fold(X87, X86, T50))))), SCOPE: 14, CLAUSE: 9\n\nX85 is free\nX86 is free\nX87 is free", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: ','(empty([]), ','(','(!_14, failure(a)), ','(head([], X85), ','(tail([], X86), ','(myop(c, X85, X87), fold(X87, X86, T50)))))), SCOPE: 16, CLAUSE: 7 | ?_16 | ?_15 | ','(no(empty([])), ','(head([], X85), ','(tail([], X86), ','(myop(c, X85, X87), fold(X87, X86, T50))))), SCOPE: 14, CLAUSE: 9\n\nX85 is free\nX86 is free\nX87 is free", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: ','(','(!_14, failure(a)), ','(head([], X85), ','(tail([], X86), ','(myop(c, X85, X87), fold(X87, X86, T50))))) | ?_16 | ?_15 | ','(no(empty([])), ','(head([], X85), ','(tail([], X86), ','(myop(c, X85, X87), fold(X87, X86, T50))))), SCOPE: 14, CLAUSE: 9\n\nX85 is free\nX86 is free\nX87 is free", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: ','(failure(a), ','(head([], X85), ','(tail([], X86), ','(myop(c, X85, X87), fold(X87, X86, T50)))))\n\nX85 is free\nX86 is free\nX87 is free", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: ','(failure(a), ','(head([], X85), ','(tail([], X86), ','(myop(c, X85, X87), fold(X87, X86, T50))))), SCOPE: 17, CLAUSE: 10\n\nX85 is free\nX86 is free\nX87 is free", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: ','(no(empty(T59)), ','(head(T59, X109), ','(tail(T59, X110), ','(myop(c, X109, X111), fold(X111, X110, T61)))))\n\nT59 is ground\nX70 is free\nX109 is free\nX110 is free\nX111 is free\nfold(c, T59, T18) !=? fold(X70, [], X70)", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: ','(no(empty(T59)), ','(head(T59, X109), ','(tail(T59, X110), ','(myop(c, X109, X111), fold(X111, X110, T61))))), SCOPE: 18, CLAUSE: 8 | ','(no(empty(T59)), ','(head(T59, X109), ','(tail(T59, X110), ','(myop(c, X109, X111), fold(X111, X110, T61))))), SCOPE: 18, CLAUSE: 9\n\nT59 is ground\nX70 is free\nX109 is free\nX110 is free\nX111 is free\nfold(c, T59, T18) !=? fold(X70, [], X70)", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="101: ','(','(call(empty(T65)), ','(!_18, failure(a))), ','(head(T65, X109), ','(tail(T65, X110), ','(myop(c, X109, X111), fold(X111, X110, T61))))) | ','(no(empty(T65)), ','(head(T65, X109), ','(tail(T65, X110), ','(myop(c, X109, X111), fold(X111, X110, T61))))), SCOPE: 18, CLAUSE: 9\n\nT65 is ground\nX70 is free\nX109 is free\nX110 is free\nX111 is free\nfold(c, T65, T18) !=? fold(X70, [], X70)", fontsize=16, style=filled, fillcolor=lightyellow];
103 [label="103: ','(empty(T65), ','(','(!_18, failure(a)), ','(head(T65, X109), ','(tail(T65, X110), ','(myop(c, X109, X111), fold(X111, X110, T61)))))) | ?_19 | ','(no(empty(T65)), ','(head(T65, X109), ','(tail(T65, X110), ','(myop(c, X109, X111), fold(X111, X110, T61))))), SCOPE: 18, CLAUSE: 9\n\nT65 is ground\nX70 is free\nX109 is free\nX110 is free\nX111 is free\nfold(c, T65, T18) !=? fold(X70, [], X70)", fontsize=16, style=filled, fillcolor=lightyellow];
105 [label="105: ','(empty(T65), ','(','(!_18, failure(a)), ','(head(T65, X109), ','(tail(T65, X110), ','(myop(c, X109, X111), fold(X111, X110, T61)))))), SCOPE: 20, CLAUSE: 7 | ?_20 | ?_19 | ','(no(empty(T65)), ','(head(T65, X109), ','(tail(T65, X110), ','(myop(c, X109, X111), fold(X111, X110, T61))))), SCOPE: 18, CLAUSE: 9\n\nT65 is ground\nX70 is free\nX109 is free\nX110 is free\nX111 is free\nfold(c, T65, T18) !=? fold(X70, [], X70)", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="106: ','(','(!_18, failure(a)), ','(head([], X109), ','(tail([], X110), ','(myop(c, X109, X111), fold(X111, X110, T61))))) | ?_20 | ?_19 | ','(no(empty([])), ','(head([], X109), ','(tail([], X110), ','(myop(c, X109, X111), fold(X111, X110, T61))))), SCOPE: 18, CLAUSE: 9\n\nX109 is free\nX110 is free\nX111 is free", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: ?_20 | ?_19 | ','(no(empty(T65)), ','(head(T65, X109), ','(tail(T65, X110), ','(myop(c, X109, X111), fold(X111, X110, T61))))), SCOPE: 18, CLAUSE: 9\n\nT65 is ground\nX70 is free\nX109 is free\nX110 is free\nX111 is free\nfold(c, T65, T18) !=? fold(X70, [], X70)\nempty(T65) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="108: ','(failure(a), ','(head([], X109), ','(tail([], X110), ','(myop(c, X109, X111), fold(X111, X110, T61)))))\n\nX109 is free\nX110 is free\nX111 is free", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="109: ','(failure(a), ','(head([], X109), ','(tail([], X110), ','(myop(c, X109, X111), fold(X111, X110, T61))))), SCOPE: 21, CLAUSE: 10\n\nX109 is free\nX110 is free\nX111 is free", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: ?_19 | ','(no(empty(T65)), ','(head(T65, X109), ','(tail(T65, X110), ','(myop(c, X109, X111), fold(X111, X110, T61))))), SCOPE: 18, CLAUSE: 9\n\nT65 is ground\nX70 is free\nX109 is free\nX110 is free\nX111 is free\nfold(c, T65, T18) !=? fold(X70, [], X70)\nempty(T65) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: ','(no(empty(T65)), ','(head(T65, X109), ','(tail(T65, X110), ','(myop(c, X109, X111), fold(X111, X110, T61))))), SCOPE: 18, CLAUSE: 9\n\nT65 is ground\nX70 is free\nX109 is free\nX110 is free\nX111 is free\nfold(c, T65, T18) !=? fold(X70, [], X70)\nempty(T65) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: ','(head(T70, X109), ','(tail(T70, X110), ','(myop(c, X109, X111), fold(X111, X110, T61))))\n\nT70 is ground\nX70 is free\nX109 is free\nX110 is free\nX111 is free\nfold(c, T70, T18) !=? fold(X70, [], X70)\nempty(T70) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
114 [label="114: ','(head(T70, X109), ','(tail(T70, X110), ','(myop(c, X109, X111), fold(X111, X110, T61)))), SCOPE: 22, CLAUSE: 3 | ','(head(T70, X109), ','(tail(T70, X110), ','(myop(c, X109, X111), fold(X111, X110, T61)))), SCOPE: 22, CLAUSE: 4\n\nT70 is ground\nX70 is free\nX109 is free\nX110 is free\nX111 is free\nfold(c, T70, T18) !=? fold(X70, [], X70)\nempty(T70) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
115 [label="115: ','(head(T70, X109), ','(tail(T70, X110), ','(myop(c, X109, X111), fold(X111, X110, T61)))), SCOPE: 22, CLAUSE: 4\n\nT70 is ground\nX70 is free\nX109 is free\nX110 is free\nX111 is free\nfold(c, T70, T18) !=? fold(X70, [], X70)\nempty(T70) !=? empty([])", fontsize=16, style=filled, fillcolor=lightyellow];
116 [label="116: ','(tail(.(T76, T77), X110), ','(myop(c, T76, X111), fold(X111, X110, T61)))\n\nT76 is ground\nT77 is ground\nX110 is free\nX111 is free", fontsize=16, style=filled, fillcolor=lightyellow];
117 [label="117: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
119 [label="119: ','(tail(.(T76, T77), X110), ','(myop(c, T76, X111), fold(X111, X110, T61))), SCOPE: 23, CLAUSE: 5 | ','(tail(.(T76, T77), X110), ','(myop(c, T76, X111), fold(X111, X110, T61))), SCOPE: 23, CLAUSE: 6\n\nT76 is ground\nT77 is ground\nX110 is free\nX111 is free", fontsize=16, style=filled, fillcolor=lightyellow];
120 [label="120: ','(tail(.(T76, T77), X110), ','(myop(c, T76, X111), fold(X111, X110, T61))), SCOPE: 23, CLAUSE: 6\n\nT76 is ground\nT77 is ground\nX110 is free\nX111 is free", fontsize=16, style=filled, fillcolor=lightyellow];
122 [label="122: ','(myop(c, T85, X111), fold(X111, T86, T61))\n\nT85 is ground\nT86 is ground\nX111 is free", fontsize=16, style=filled, fillcolor=lightyellow];
124 [label="124: ','(myop(c, T85, X111), fold(X111, T86, T61)), SCOPE: 24, CLAUSE: 2\n\nT85 is ground\nT86 is ground\nX111 is free", fontsize=16, style=filled, fillcolor=lightyellow];
125 [label="125: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
126 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 126 [arrowhead = none ];
126 -> 3;

127 [label="EVAL with clause\nfold(X6, [], X6).\nand substitutionT1 -> T5,\nX6 -> T5,\nT2 -> [],\nT3 -> T5", fontsize=14, style = filled, fillcolor = lightblue];
3 -> 127 [arrowhead = none ];
127 -> 5;

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

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

130 [label="ONLY EVAL with clause\nfold(X24, X25, X26) :- ','(no(empty(X25)), ','(head(X25, X27), ','(tail(X25, X28), ','(myop(X24, X27, X29), fold(X29, X28, X26))))).\nand substitutionT1 -> T15,\nX24 -> T15,\nT2 -> T16,\nX25 -> T16,\nT3 -> T18,\nX26 -> T18,\nT17 -> T18", fontsize=14, style = filled, fillcolor = lightblue];
7 -> 130 [arrowhead = none ];
130 -> 22;

131 [label="ONLY EVAL with clause\nfold(X10, X11, X12) :- ','(no(empty(X11)), ','(head(X11, X13), ','(tail(X11, X14), ','(myop(X10, X13, X15), fold(X15, X14, X12))))).\nand substitutionT5 -> T8,\nX10 -> T8,\nX11 -> [],\nT3 -> T10,\nX12 -> T10,\nT9 -> T10", fontsize=14, style = filled, fillcolor = lightblue];
10 -> 131 [arrowhead = none ];
131 -> 11;

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

133 [label="ONLY EVAL with clause\nno(X18) :- ','(call(X18), ','(!_2, failure(a))).\nand substitutionX18 -> empty([])", fontsize=14, style = filled, fillcolor = lightblue];
12 -> 133 [arrowhead = none ];
133 -> 13;

134 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
13 -> 134 [arrowhead = none ];
134 -> 14;

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

136 [label="ONLY EVAL with clause\nempty([]).\nand substitution", fontsize=14, style = filled, fillcolor = lightblue];
15 -> 136 [arrowhead = none ];
136 -> 16;

137 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
16 -> 137 [arrowhead = none ];
137 -> 17;

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

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

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

141 [label="ONLY EVAL with clause\nno(X32) :- ','(call(X32), ','(!_6, failure(a))).\nand substitutionT16 -> T21,\nX32 -> empty(T21)", fontsize=14, style = filled, fillcolor = lightblue];
24 -> 141 [arrowhead = none ];
141 -> 27;

142 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
27 -> 142 [arrowhead = none ];
142 -> 28;

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

144 [label="EVAL with clause\nempty([]).\nand substitutionT21 -> []", fontsize=14, style = filled, fillcolor = lightblue];
31 -> 144 [arrowhead = none ];
144 -> 33;

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

146 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
33 -> 146 [arrowhead = none ];
146 -> 35;

147 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
34 -> 147 [arrowhead = none ];
147 -> 39;

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

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

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

151 [label="ONLY EVAL with clause\nno(X39).\nand substitutionT21 -> T26,\nX39 -> empty(T26)", fontsize=14, style = filled, fillcolor = lightblue];
40 -> 151 [arrowhead = none ];
151 -> 41;

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

153 [label="BACKTRACK\nfor clause: head([], X1)\nwith clash: (empty(T26), empty([]))", fontsize=14, style = filled, fillcolor = lightgreen];
42 -> 153 [arrowhead = none ];
153 -> 43;

154 [label="EVAL with clause\nhead(.(X48, X49), X48).\nand substitutionX48 -> T32,\nX49 -> T33,\nT26 -> .(T32, T33),\nX27 -> T32", fontsize=14, style = filled, fillcolor = lightblue];
43 -> 154 [arrowhead = none ];
154 -> 45;

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

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

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

158 [label="ONLY EVAL with clause\ntail(.(X60, X61), X61).\nand substitutionT32 -> T41,\nX60 -> T41,\nT33 -> T42,\nX61 -> T42,\nX28 -> T42", fontsize=14, style = filled, fillcolor = lightblue];
49 -> 158 [arrowhead = none ];
158 -> 54;

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

160 [label="EVAL with clause\nmyop(a, b, c).\nand substitutionT15 -> a,\nT41 -> b,\nX29 -> c", fontsize=14, style = filled, fillcolor = lightblue];
57 -> 160 [arrowhead = none ];
160 -> 59;

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

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

163 [label="EVAL with clause\nfold(X70, [], X70).\nand substitutionX70 -> c,\nT42 -> [],\nT18 -> c", fontsize=14, style = filled, fillcolor = lightblue];
67 -> 163 [arrowhead = none ];
163 -> 69;

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

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

166 [label="ONLY EVAL with clause\nfold(X106, X107, X108) :- ','(no(empty(X107)), ','(head(X107, X109), ','(tail(X107, X110), ','(myop(X106, X109, X111), fold(X111, X110, X108))))).\nand substitutionX106 -> c,\nT42 -> T59,\nX107 -> T59,\nT18 -> T61,\nX108 -> T61,\nT60 -> T61", fontsize=14, style = filled, fillcolor = lightblue];
71 -> 166 [arrowhead = none ];
166 -> 94;

167 [label="ONLY EVAL with clause\nfold(X82, X83, X84) :- ','(no(empty(X83)), ','(head(X83, X85), ','(tail(X83, X86), ','(myop(X82, X85, X87), fold(X87, X86, X84))))).\nand substitutionX82 -> c,\nX83 -> [],\nT18 -> T50,\nX84 -> T50,\nT49 -> T50", fontsize=14, style = filled, fillcolor = lightblue];
72 -> 167 [arrowhead = none ];
167 -> 76;

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

169 [label="ONLY EVAL with clause\nno(X92) :- ','(call(X92), ','(!_14, failure(a))).\nand substitutionX92 -> empty([])", fontsize=14, style = filled, fillcolor = lightblue];
78 -> 169 [arrowhead = none ];
169 -> 81;

170 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
81 -> 170 [arrowhead = none ];
170 -> 82;

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

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

173 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
85 -> 173 [arrowhead = none ];
173 -> 87;

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

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

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

177 [label="ONLY EVAL with clause\nno(X116) :- ','(call(X116), ','(!_18, failure(a))).\nand substitutionT59 -> T65,\nX116 -> empty(T65)", fontsize=14, style = filled, fillcolor = lightblue];
96 -> 177 [arrowhead = none ];
177 -> 101;

178 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
101 -> 178 [arrowhead = none ];
178 -> 103;

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

180 [label="EVAL with clause\nempty([]).\nand substitutionT65 -> []", fontsize=14, style = filled, fillcolor = lightblue];
105 -> 180 [arrowhead = none ];
180 -> 106;

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

182 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
106 -> 182 [arrowhead = none ];
182 -> 108;

183 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
107 -> 183 [arrowhead = none ];
183 -> 111;

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

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

186 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
111 -> 186 [arrowhead = none ];
186 -> 112;

187 [label="ONLY EVAL with clause\nno(X123).\nand substitutionT65 -> T70,\nX123 -> empty(T70)", fontsize=14, style = filled, fillcolor = lightblue];
112 -> 187 [arrowhead = none ];
187 -> 113;

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

189 [label="BACKTRACK\nfor clause: head([], X1)\nwith clash: (empty(T70), empty([]))", fontsize=14, style = filled, fillcolor = lightgreen];
114 -> 189 [arrowhead = none ];
189 -> 115;

190 [label="EVAL with clause\nhead(.(X132, X133), X132).\nand substitutionX132 -> T76,\nX133 -> T77,\nT70 -> .(T76, T77),\nX109 -> T76", fontsize=14, style = filled, fillcolor = lightblue];
115 -> 190 [arrowhead = none ];
190 -> 116;

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

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

193 [label="BACKTRACK\nfor clause: tail([], [])because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
119 -> 193 [arrowhead = none ];
193 -> 120;

194 [label="ONLY EVAL with clause\ntail(.(X144, X145), X145).\nand substitutionT76 -> T85,\nX144 -> T85,\nT77 -> T86,\nX145 -> T86,\nX110 -> T86", fontsize=14, style = filled, fillcolor = lightblue];
120 -> 194 [arrowhead = none ];
194 -> 122;

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

196 [label="BACKTRACK\nfor clause: myop(a, b, c)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
124 -> 196 [arrowhead = none ];
196 -> 125;

}

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0, []) → f1_out1(z0)
f1_in(a, .(b, [])) → f1_out1(c)

Tuples:none
S tuples:none
K tuples:none
Defined Rule Symbols:

f1_in

Defined Pair Symbols:none

Compound Symbols:none

(3) SIsEmptyProof (EQUIVALENT transformation)

The set S is empty

(4) BOUNDS(O(1), O(1))