[]: Open (size=19, cost=0, time=0, max=0, total=1.3113e-05, pending=1) [0]: Open (size=19, cost=19, time=0.672645, max=0.672645, total=0.694717, pending=1) [1]: Open (size=19, cost=19, time=0.021703, max=0.021703, total=0.774536, pending=2) [01]: Open (size=19, cost=19, time=0.713558, max=0.672645, total=0.836618, pending=3) ******* COMPLETION ******* plus(X0,plus(Y0,Z0)) -> plus(plus(X0,Y0),Z0) f(plus(X0,Y0)) -> plus(f(X0),f(Y0)) ************************** On branch: [01] With size, cost: 19, 19 Orientations: 6 Calls to AProVE (all, T, NT, ?): 6, 6, 0, 0 Time (all, branch, AProVE): 0.837112, 0.713558, 0.834183 Time/call in AProVE (Avg, Min, Max): 0.13903, 0.672286, 0.0216651 Time/T-call in AProVE (Avg, Min, Max): 0.13903, 0.672286, 0.672645 All conjectures solved.