YES(O(1), O(1)) 0.00/0.54 YES(O(1), O(1)) 0.00/0.55 0.00/0.55 0.00/0.55
0.00/0.55 0.00/0.550 CpxTRS0.00/0.55
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))0.00/0.55
↳2 CdtProblem0.00/0.55
↳3 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))0.00/0.55
↳4 CdtProblem0.00/0.55
↳5 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))0.00/0.55
↳6 CdtProblem0.00/0.55
↳7 SIsEmptyProof (BOTH BOUNDS(ID, ID))0.00/0.55
↳8 BOUNDS(O(1), O(1))0.00/0.55
p(f(f(x))) → q(f(g(x))) 0.00/0.55
p(g(g(x))) → q(g(f(x))) 0.00/0.55
q(f(f(x))) → p(f(g(x))) 0.00/0.55
q(g(g(x))) → p(g(f(x)))
Tuples:
p(f(f(z0))) → q(f(g(z0))) 0.00/0.55
p(g(g(z0))) → q(g(f(z0))) 0.00/0.55
q(f(f(z0))) → p(f(g(z0))) 0.00/0.55
q(g(g(z0))) → p(g(f(z0)))
S tuples:
P(f(f(z0))) → c(Q(f(g(z0)))) 0.00/0.55
P(g(g(z0))) → c1(Q(g(f(z0)))) 0.00/0.55
Q(f(f(z0))) → c2(P(f(g(z0)))) 0.00/0.55
Q(g(g(z0))) → c3(P(g(f(z0))))
K tuples:none
P(f(f(z0))) → c(Q(f(g(z0)))) 0.00/0.55
P(g(g(z0))) → c1(Q(g(f(z0)))) 0.00/0.55
Q(f(f(z0))) → c2(P(f(g(z0)))) 0.00/0.55
Q(g(g(z0))) → c3(P(g(f(z0))))
p, q
P, Q
c, c1, c2, c3
Tuples:
p(f(f(z0))) → q(f(g(z0))) 0.00/0.55
p(g(g(z0))) → q(g(f(z0))) 0.00/0.55
q(f(f(z0))) → p(f(g(z0))) 0.00/0.55
q(g(g(z0))) → p(g(f(z0)))
S tuples:
P(f(f(z0))) → c 0.00/0.55
P(g(g(z0))) → c1 0.00/0.55
Q(f(f(z0))) → c2 0.00/0.55
Q(g(g(z0))) → c3
K tuples:none
P(f(f(z0))) → c 0.00/0.55
P(g(g(z0))) → c1 0.00/0.55
Q(f(f(z0))) → c2 0.00/0.55
Q(g(g(z0))) → c3
p, q
P, Q
c, c1, c2, c3
P(g(g(z0))) → c1 0.00/0.55
Q(g(g(z0))) → c3 0.00/0.55
Q(f(f(z0))) → c2 0.00/0.55
P(f(f(z0))) → c
Tuples:none
p(f(f(z0))) → q(f(g(z0))) 0.00/0.55
p(g(g(z0))) → q(g(f(z0))) 0.00/0.55
q(f(f(z0))) → p(f(g(z0))) 0.00/0.55
q(g(g(z0))) → p(g(f(z0)))
p, q