[]: Open (size=36, cost=0, time=0, max=0, total=8.10623e-06, pending=1)
[1]: Open (size=36, cost=36, time=0.670031, max=0.643786, total=0.766548, pending=1)
[11]: Open (size=37, cost=37, time=0.714413, max=0.643786, total=0.845526, pending=2)
[0]: Open (size=36, cost=48, time=0.739997, max=0.643786, total=0.898397, pending=2)
[01]: Open (size=36, cost=48, time=0.776174, max=0.643786, total=0.954804, pending=3)
[00]: Open (size=36, cost=92, time=0.759809, max=0.643786, total=1.00398, pending=3)
[10]: Open (size=37, cost=103, time=0.703835, max=0.643786, total=1.02964, pending=3)
[11]: Open (size=37, cost=153, time=0.766418, max=0.643786, total=1.07052, pending=3)
[01]: Open (size=36, cost=196, time=0.82419, max=0.643786, total=1.35525, pending=3)
[11]: Open (size=85, cost=209, time=1.04294, max=0.643786, total=1.59105, pending=3)
[01]: Open (size=94, cost=231, time=1.05358, max=0.643786, total=1.6455, pending=3)
[00]: Open (size=36, cost=278, time=0.784008, max=0.643786, total=1.72964, pending=3)
[000]: Open (size=63, cost=203, time=0.933757, max=0.643786, total=1.90582, pending=4)
[001]: Open (size=63, cost=263, time=0.923161, max=0.643786, total=2.5563, pending=4)
[0011]: Open (size=62, cost=99, time=1.09912, max=0.643786, total=2.82223, pending=5)
[0010]: Open (size=55, cost=230, time=1.11005, max=0.643786, total=2.95531, pending=5)
[10]: Open (size=37, cost=291, time=0.743113, max=0.643786, total=3.34918, pending=5)
[100]: Open (size=65, cost=207, time=0.995768, max=0.643786, total=3.68332, pending=6)
[101]: Open (size=65, cost=247, time=0.992263, max=0.643786, total=3.85435, pending=6)
[100]: Open (size=129, cost=293, time=1.16156, max=0.643786, total=3.92109, pending=6)
[101]: Open (size=149, cost=313, time=1.05298, max=0.643786, total=4.0019, pending=6)
[01]: Open (size=93, cost=334, time=1.13292, max=0.643786, total=4.12301, pending=6)
[0011]: Open (size=42, cost=356, time=1.22917, max=0.643786, total=4.18888, pending=6)
[000]: Open (size=136, cost=368, time=1.28635, max=0.643786, total=4.35525, pending=6)
[0011]: Open (size=204, cost=381, time=1.38046, max=0.643786, total=4.40215, pending=6)
[100]: Open (size=119, cost=389, time=1.23608, max=0.643786, total=4.44835, pending=6)
[0010]: Open (size=156, cost=398, time=1.48795, max=0.643786, total=4.48949, pending=6)
[101]: Open (size=141, cost=443, time=1.16872, max=0.643786, total=4.5301, pending=6)
[0011]: Open (size=201, cost=503, time=1.42295, max=0.643786, total=4.60498, pending=6)
[000]: Open (size=135, cost=522, time=1.32562, max=0.643786, total=4.63193, pending=6)
[0010]: Open (size=156, cost=582, time=1.52102, max=0.643786, total=4.67403, pending=6)
[0011]: Open (size=198, cost=609, time=1.44459, max=0.643786, total=4.79697, pending=6)
[11]: Open (size=85, cost=665, time=1.087, max=0.643786, total=4.85473, pending=6)
[0011]: Open (size=171, cost=762, time=1.48208, max=0.643786, total=4.89266, pending=6)
[01]: Open (size=93, cost=783, time=1.18663, max=0.643786, total=4.98353, pending=6)
[100]: Open (size=107, cost=903, time=1.26604, max=0.643786, total=5.02359, pending=6)
[101]: Open (size=107, cost=905, time=1.23094, max=0.643786, total=5.05777, pending=6)
[0011]: Open (size=158, cost=978, time=1.55969, max=0.643786, total=5.09703, pending=6)
[000]: Open (size=124, cost=1036, time=1.34809, max=0.643786, total=5.1426, pending=6)
[0010]: Open (size=124, cost=1054, time=1.6272, max=0.643786, total=5.20292, pending=6)
[11]: Open (size=85, cost=1135, time=1.10396, max=0.643786, total=5.30395, pending=6)
[0011]: Open (size=152, cost=1208, time=1.59036, max=0.643786, total=5.35695, pending=6)
[01]: Open (size=93, cost=1266, time=1.20758, max=0.643786, total=5.40473, pending=6)
[010]: Open (size=123, cost=171, time=1.2823, max=0.643786, total=5.53991, pending=7)
******* COMPLETION *******
d(X2,d(X1,Y0)) -> d(d(X2,i(Y0)),X1)
d(d(X3,i(Y0)),Y0) -> X3
d(d(X1,Y0),i(Y0)) -> X1
d(Y0,one) -> Y0
d(one,Y0) -> i(Y0)
i(i(Y0)) -> Y0
d(X0,X0) -> one
i(one) -> one
times(X0,Y0) -> d(X0,i(Y0))
i(d(Z1,X0)) -> d(X0,Z1)
**************************
On branch: [010]
With size, cost: 59, 107
Orientations: 156
Calls to AProVE (all, T, NT, ?): 86, 85, 1, 0
Time (all, branch, AProVE): 5.54496, 1.2823, 5.0042
Time/call in AProVE (Avg, Min, Max): 0.0581884, 0.643597, 0.0136709
Time/T-call in AProVE (Avg, Min, Max): 0.0555047, 0.643597, 0.643786
All conjectures solved.