[]: Open (size=44, cost=0, time=0, max=0, total=1.19209e-05, pending=1) [0]: Open (size=60, cost=73, time=1.22279, max=0.804841, total=1.29559, pending=1) [00]: Open (size=55, cost=73, time=1.28423, max=0.804841, total=1.39681, pending=2) ******* COMPLETION ******* eq(X1,s(X0)) -> eq(p(X1),X0) eq(s(X0),Y1) -> eq(X0,p(Y1)) eq(p(X0),p(Y0)) -> eq(X0,Y0) eq(X0,p(X0)) -> false eq(p(X0),X0) -> false eq(X0,X0) -> true p(s(X0)) -> X0 ************************** On branch: [00] With size, cost: 42, 60 Orientations: 20 Calls to AProVE (all, T, NT, ?): 12, 12, 0, 0 Time (all, branch, AProVE): 1.39767, 1.28423, 1.38929 Time/call in AProVE (Avg, Min, Max): 0.115774, 0.804604, 0.031096 Time/T-call in AProVE (Avg, Min, Max): 0.115774, 0.804604, 0.804841 All conjectures solved.