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

(0) Obligation:

Clauses:

bin_tree(void).
bin_tree(tree(X1, Left, Right)) :- ','(bin_tree(Left), bin_tree(Right)).

Query: bin_tree(g)

(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: bin_tree(T1)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
3 [label="3: bin_tree(T1), SCOPE: 1, CLAUSE: 0 | bin_tree(T1), SCOPE: 1, CLAUSE: 1\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: true | bin_tree(void), SCOPE: 1, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: bin_tree(T1), SCOPE: 1, CLAUSE: 1\n\nT1 is ground\nbin_tree(T1) !=? bin_tree(void)", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: bin_tree(void), SCOPE: 1, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: ','(bin_tree(T9), bin_tree(T10))\n\nT9 is ground\nT10 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: bin_tree(T9)\n\nT9 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: bin_tree(T10)\n\nT10 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 24 [arrowhead = none ];
24 -> 3;

25 [label="EVAL with clause\nbin_tree(void).\nand substitutionT1 -> void", fontsize=14, style = filled, fillcolor = lightblue];
3 -> 25 [arrowhead = none ];
25 -> 5;

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

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

28 [label="EVAL with clause\nbin_tree(tree(X11, X12, X13)) :- ','(bin_tree(X12), bin_tree(X13)).\nand substitutionX11 -> T8,\nX12 -> T9,\nX13 -> T10,\nT1 -> tree(T8, T9, T10)", fontsize=14, style = filled, fillcolor = lightblue];
8 -> 28 [arrowhead = none ];
28 -> 17;

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

30 [label="BACKTRACK\nfor clause: bin_tree(tree(X1, Left, Right)) :- ','(bin_tree(Left), bin_tree(Right))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
9 -> 30 [arrowhead = none ];
30 -> 12;

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

32 [label="SPLIT 2\nnew knowledge:\nT9 is ground", fontsize=14, style = filled, fillcolor = violet];
17 -> 32 [arrowhead = none ];
32 -> 23;

33 [label="INSTANCE with matching:\nT1 -> T9", fontsize=14, style = filled, fillcolor = lightgrey];
22 -> 33 [arrowhead = none , style=dashed];
33 -> 1[style=dashed];

34 [label="INSTANCE with matching:\nT1 -> T10", fontsize=14, style = filled, fillcolor = lightgrey];
23 -> 34 [arrowhead = none , style=dashed];
34 -> 1[style=dashed];

}

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(void) → f1_out1
f1_in(tree(z0, z1, z2)) → U1(f17_in(z1, z2), tree(z0, z1, z2))
U1(f17_out1, tree(z0, z1, z2)) → f1_out1
f17_in(z0, z1) → U2(f1_in(z0), z0, z1)
U2(f1_out1, z0, z1) → U3(f1_in(z1), z0, z1)
U3(f1_out1, z0, z1) → f17_out1

Tuples:

F1_IN(tree(z0, z1, z2)) → c1(U1'(f17_in(z1, z2), tree(z0, z1, z2)), F17_IN(z1, z2))
F17_IN(z0, z1) → c3(U2'(f1_in(z0), z0, z1), F1_IN(z0))
U2'(f1_out1, z0, z1) → c4(U3'(f1_in(z1), z0, z1), F1_IN(z1))

S tuples:

F1_IN(tree(z0, z1, z2)) → c1(U1'(f17_in(z1, z2), tree(z0, z1, z2)), F17_IN(z1, z2))
F17_IN(z0, z1) → c3(U2'(f1_in(z0), z0, z1), F1_IN(z0))
U2'(f1_out1, z0, z1) → c4(U3'(f1_in(z1), z0, z1), F1_IN(z1))

K tuples:none
Defined Rule Symbols:

f1_in, U1, f17_in, U2, U3

Defined Pair Symbols:

F1_IN, F17_IN, U2'

Compound Symbols:

c1, c3, c4

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

Removed 2 trailing tuple parts

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(void) → f1_out1
f1_in(tree(z0, z1, z2)) → U1(f17_in(z1, z2), tree(z0, z1, z2))
U1(f17_out1, tree(z0, z1, z2)) → f1_out1
f17_in(z0, z1) → U2(f1_in(z0), z0, z1)
U2(f1_out1, z0, z1) → U3(f1_in(z1), z0, z1)
U3(f1_out1, z0, z1) → f17_out1

Tuples:

F17_IN(z0, z1) → c3(U2'(f1_in(z0), z0, z1), F1_IN(z0))
F1_IN(tree(z0, z1, z2)) → c1(F17_IN(z1, z2))
U2'(f1_out1, z0, z1) → c4(F1_IN(z1))

S tuples:

F17_IN(z0, z1) → c3(U2'(f1_in(z0), z0, z1), F1_IN(z0))
F1_IN(tree(z0, z1, z2)) → c1(F17_IN(z1, z2))
U2'(f1_out1, z0, z1) → c4(F1_IN(z1))

K tuples:none
Defined Rule Symbols:

f1_in, U1, f17_in, U2, U3

Defined Pair Symbols:

F17_IN, F1_IN, U2'

Compound Symbols:

c3, c1, c4

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

U2'(f1_out1, z0, z1) → c4(F1_IN(z1))

We considered the (Usable) Rules:

f1_in(void) → f1_out1
f1_in(tree(z0, z1, z2)) → U1(f17_in(z1, z2), tree(z0, z1, z2))
f17_in(z0, z1) → U2(f1_in(z0), z0, z1)
U1(f17_out1, tree(z0, z1, z2)) → f1_out1
U2(f1_out1, z0, z1) → U3(f1_in(z1), z0, z1)
U3(f1_out1, z0, z1) → f17_out1

And the Tuples:

F17_IN(z0, z1) → c3(U2'(f1_in(z0), z0, z1), F1_IN(z0))
F1_IN(tree(z0, z1, z2)) → c1(F17_IN(z1, z2))
U2'(f1_out1, z0, z1) → c4(F1_IN(z1))

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

POL(F17_IN(x₁, x₂)) = [2] + x₁ + x₂   
POL(F1_IN(x₁)) = x₁   
POL(U1(x₁, x₂)) = 0   
POL(U2(x₁, x₂, x₃)) = 0   
POL(U2'(x₁, x₂, x₃)) = [2] + x₃   
POL(U3(x₁, x₂, x₃)) = 0   
POL(c1(x₁)) = x₁   
POL(c3(x₁, x₂)) = x₁ + x₂   
POL(c4(x₁)) = x₁   
POL(f17_in(x₁, x₂)) = 0   
POL(f17_out1) = 0   
POL(f1_in(x₁)) = 0   
POL(f1_out1) = 0   
POL(tree(x₁, x₂, x₃)) = [2] + x₂ + x₃   
POL(void) = 0   

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(void) → f1_out1
f1_in(tree(z0, z1, z2)) → U1(f17_in(z1, z2), tree(z0, z1, z2))
U1(f17_out1, tree(z0, z1, z2)) → f1_out1
f17_in(z0, z1) → U2(f1_in(z0), z0, z1)
U2(f1_out1, z0, z1) → U3(f1_in(z1), z0, z1)
U3(f1_out1, z0, z1) → f17_out1

Tuples:

F17_IN(z0, z1) → c3(U2'(f1_in(z0), z0, z1), F1_IN(z0))
F1_IN(tree(z0, z1, z2)) → c1(F17_IN(z1, z2))
U2'(f1_out1, z0, z1) → c4(F1_IN(z1))

S tuples:

F17_IN(z0, z1) → c3(U2'(f1_in(z0), z0, z1), F1_IN(z0))
F1_IN(tree(z0, z1, z2)) → c1(F17_IN(z1, z2))

K tuples:

U2'(f1_out1, z0, z1) → c4(F1_IN(z1))

Defined Rule Symbols:

f1_in, U1, f17_in, U2, U3

Defined Pair Symbols:

F17_IN, F1_IN, U2'

Compound Symbols:

c3, c1, c4

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

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

F1_IN(tree(z0, z1, z2)) → c1(F17_IN(z1, z2))

We considered the (Usable) Rules:

f1_in(void) → f1_out1
f1_in(tree(z0, z1, z2)) → U1(f17_in(z1, z2), tree(z0, z1, z2))
f17_in(z0, z1) → U2(f1_in(z0), z0, z1)
U1(f17_out1, tree(z0, z1, z2)) → f1_out1
U2(f1_out1, z0, z1) → U3(f1_in(z1), z0, z1)
U3(f1_out1, z0, z1) → f17_out1

And the Tuples:

F17_IN(z0, z1) → c3(U2'(f1_in(z0), z0, z1), F1_IN(z0))
F1_IN(tree(z0, z1, z2)) → c1(F17_IN(z1, z2))
U2'(f1_out1, z0, z1) → c4(F1_IN(z1))

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

POL(F17_IN(x₁, x₂)) = [2]x₁ + [2]x₂   
POL(F1_IN(x₁)) = [2]x₁   
POL(U1(x₁, x₂)) = 0   
POL(U2(x₁, x₂, x₃)) = [3] + [3]x₁ + x₃   
POL(U2'(x₁, x₂, x₃)) = [2]x₃   
POL(U3(x₁, x₂, x₃)) = x₃   
POL(c1(x₁)) = x₁   
POL(c3(x₁, x₂)) = x₁ + x₂   
POL(c4(x₁)) = x₁   
POL(f17_in(x₁, x₂)) = [3] + x₁ + [2]x₂   
POL(f17_out1) = 0   
POL(f1_in(x₁)) = 0   
POL(f1_out1) = [2]   
POL(tree(x₁, x₂, x₃)) = [1] + x₂ + x₃   
POL(void) = 0   

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(void) → f1_out1
f1_in(tree(z0, z1, z2)) → U1(f17_in(z1, z2), tree(z0, z1, z2))
U1(f17_out1, tree(z0, z1, z2)) → f1_out1
f17_in(z0, z1) → U2(f1_in(z0), z0, z1)
U2(f1_out1, z0, z1) → U3(f1_in(z1), z0, z1)
U3(f1_out1, z0, z1) → f17_out1

Tuples:

F17_IN(z0, z1) → c3(U2'(f1_in(z0), z0, z1), F1_IN(z0))
F1_IN(tree(z0, z1, z2)) → c1(F17_IN(z1, z2))
U2'(f1_out1, z0, z1) → c4(F1_IN(z1))

S tuples:

F17_IN(z0, z1) → c3(U2'(f1_in(z0), z0, z1), F1_IN(z0))

K tuples:

U2'(f1_out1, z0, z1) → c4(F1_IN(z1))
F1_IN(tree(z0, z1, z2)) → c1(F17_IN(z1, z2))

Defined Rule Symbols:

f1_in, U1, f17_in, U2, U3

Defined Pair Symbols:

F17_IN, F1_IN, U2'

Compound Symbols:

c3, c1, c4

(9) CdtKnowledgeProof (EQUIVALENT transformation)

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

F17_IN(z0, z1) → c3(U2'(f1_in(z0), z0, z1), F1_IN(z0))
F1_IN(tree(z0, z1, z2)) → c1(F17_IN(z1, z2))
U2'(f1_out1, z0, z1) → c4(F1_IN(z1))

Now S is empty

(10) BOUNDS(O(1), O(1))