[]: Open (size=25, cost=0, time=0, max=0, total=1.50204e-05, pending=1) [0]: Open (size=25, cost=25, time=0.734764, max=0.595381, total=0.763944, pending=1) [00]: Open (size=25, cost=25, time=1.15633, max=0.595381, total=1.22289, pending=2) ******* COMPLETION ******* times(X0,s(Y0)) -> plus(times(X0,Y0),X0) plus(X0,s(Y0)) -> s(plus(X0,Y0)) times(X0,null) -> null plus(X0,null) -> X0 ************************** On branch: [00] With size, cost: 25, 25 Orientations: 8 Calls to AProVE (all, T, NT, ?): 6, 6, 0, 0 Time (all, branch, AProVE): 1.22334, 1.15633, 1.22081 Time/call in AProVE (Avg, Min, Max): 0.203468, 0.595022, 0.0285609 Time/T-call in AProVE (Avg, Min, Max): 0.203468, 0.595022, 0.595381 All conjectures solved.