[]: Open (size=28, cost=0, time=0, max=0, total=1.40667e-05, pending=1)
[1]: Open (size=28, cost=28, time=1.03959, max=0.922651, total=1.07328, pending=1)
[0]: Open (size=28, cost=58, time=1.03796, max=0.922651, total=1.15034, pending=2)
[10]: Open (size=28, cost=68, time=1.0807, max=0.922651, total=1.23089, pending=3)
[00]: Open (size=28, cost=72, time=1.07169, max=0.922651, total=1.2918, pending=3)
[11]: Open (size=28, cost=124, time=1.07425, max=0.922651, total=1.416, pending=3)
[10]: Open (size=72, cost=128, time=1.1399, max=0.922651, total=1.50434, pending=3)
[01]: Open (size=28, cost=128, time=1.08353, max=0.922651, total=1.58696, pending=4)
[100]: Open (size=62, cost=146, time=1.17998, max=0.922651, total=1.69789, pending=4)
[00]: Open (size=53, cost=153, time=1.19284, max=0.922651, total=2.01159, pending=4)
[01]: Open (size=53, cost=168, time=1.19098, max=0.922651, total=2.06208, pending=4)
[100]: Open (size=97, cost=175, time=1.4876, max=0.922651, total=2.1025, pending=4)
[11]: Open (size=100, cost=185, time=1.15942, max=0.922651, total=2.14268, pending=4)
[00]: Open (size=65, cost=190, time=1.24046, max=0.922651, total=2.18088, pending=4)
[01]: Open (size=65, cost=200, time=1.22868, max=0.922651, total=2.23255, pending=4)
[00]: Open (size=66, cost=281, time=1.28893, max=0.922651, total=2.3167, pending=4)
[101]: Open (size=62, cost=281, time=1.18054, max=0.922651, total=2.37998, pending=4)
[00]: Open (size=90, cost=330, time=1.34645, max=0.922651, total=2.70162, pending=4)
[11]: Open (size=100, cost=336, time=1.19365, max=0.922651, total=2.80172, pending=4)
[100]: Open (size=97, cost=368, time=1.52316, max=0.922651, total=2.87384, pending=5)
[110]: Open (size=81, cost=371, time=1.23176, max=0.922651, total=2.98406, pending=5)
[101]: Open (size=97, cost=373, time=1.49311, max=0.922651, total=3.1185, pending=5)
[110]: Open (size=118, cost=374, time=1.35541, max=0.922651, total=3.20997, pending=5)
[01]: Open (size=77, cost=545, time=1.306, max=0.922651, total=3.44019, pending=5)
[101]: Open (size=97, cost=586, time=1.57213, max=0.922651, total=3.47862, pending=5)
[01]: Open (size=105, cost=619, time=1.33568, max=0.922651, total=3.52251, pending=5)
[00]: Open (size=90, cost=628, time=1.43892, max=0.922651, total=3.65908, pending=5)
[100]: Open (size=86, cost=700, time=1.61492, max=0.922651, total=3.78713, pending=5)
[111]: Open (size=81, cost=748, time=1.21932, max=0.922651, total=4.01163, pending=5)
[01]: Open (size=199, cost=752, time=1.45878, max=0.922651, total=4.11973, pending=5)
[100]: Open (size=154, cost=756, time=1.80295, max=0.922651, total=4.25049, pending=5)
[111]: Open (size=118, cost=758, time=1.30687, max=0.922651, total=4.42305, pending=5)
[100]: Open (size=120, cost=766, time=1.94944, max=0.922651, total=4.51491, pending=5)
[111]: Open (size=90, cost=766, time=1.37724, max=0.922651, total=4.61534, pending=5)
[00]: Open (size=121, cost=804, time=1.53993, max=0.922651, total=4.71526, pending=5)
[110]: Open (size=155, cost=807, time=1.54973, max=0.922651, total=4.77741, pending=5)
[100]: Open (size=119, cost=933, time=2.00326, max=0.922651, total=4.87556, pending=5)
[00]: Open (size=202, cost=996, time=1.58321, max=0.922651, total=4.95418, pending=5)
[101]: Open (size=86, cost=1018, time=1.60296, max=0.922651, total=5.03915, pending=5)
[01]: Open (size=199, cost=1051, time=1.55912, max=0.922651, total=5.12069, pending=5)
[101]: Open (size=154, cost=1075, time=1.65373, max=0.922651, total=5.17059, pending=5)
[01]: Open (size=180, cost=1110, time=1.58744, max=0.922651, total=5.23185, pending=5)
[101]: Open (size=120, cost=1127, time=1.69384, max=0.922651, total=5.2844, pending=5)
[100]: Open (size=123, cost=1173, time=2.04661, max=0.922651, total=5.33694, pending=5)
[111]: Open (size=167, cost=1209, time=1.44606, max=0.922651, total=5.41495, pending=5)
[00]: Open (size=179, cost=1236, time=1.64411, max=0.922651, total=5.46732, pending=5)
[110]: Open (size=155, cost=1252, time=1.60279, max=0.922651, total=5.86635, pending=5)
[01]: Open (size=180, cost=1274, time=1.61305, max=0.922651, total=5.97212, pending=5)
[00]: Open (size=201, cost=1301, time=1.94386, max=0.922651, total=6.05278, pending=5)
[100]: Open (size=219, cost=1372, time=2.08593, max=0.922651, total=6.15687, pending=5)
[101]: Open (size=119, cost=1394, time=1.71445, max=0.922651, total=6.27813, pending=5)
[01]: Open (size=153, cost=1395, time=1.65642, max=0.922651, total=6.34244, pending=5)
[110]: Open (size=204, cost=1587, time=1.64001, max=0.922651, total=6.71657, pending=5)
[01]: Open (size=211, cost=1632, time=1.85024, max=0.922651, total=6.81496, pending=5)
[101]: Open (size=123, cost=1743, time=1.73343, max=0.922651, total=6.93169, pending=5)
[100]: Open (size=176, cost=1791, time=2.15204, max=0.922651, total=6.99523, pending=5)
[1000]: Open (size=235, cost=599, time=2.1973, max=0.922651, total=7.13478, pending=6)
[10001]: Open (size=152, cost=651, time=2.25217, max=0.922651, total=7.24935, pending=7)
[100011]: Open (size=218, cost=353, time=2.46167, max=0.922651, total=7.60039, pending=8)
******* COMPLETION *******
f(f(X1,h(X0)),h(Y0)) -> f(X1,h(f(X0,Y0)))
i(h(X2)) -> h(i(X2))
h(e) -> e
f(f(X3,i(X0)),X0) -> X3
i(e) -> e
f(X0,e) -> X0
f(X0,i(X0)) -> e
f(h(X0),h(Y0)) -> h(f(X0,Y0))
f(X0,f(Y0,Z0)) -> f(f(X0,Y0),Z0)
f(f(X1,X0),i(X0)) -> X1
f(e,X0) -> X0
i(i(X2)) -> X2
f(i(X2),X2) -> e
i(f(Y0,Z0)) -> f(i(Z0),i(Y0))
**************************
On branch: [100011]
With size, cost: 89, 224
Orientations: 194
Calls to AProVE (all, T, NT, ?): 105, 105, 0, 0
Time (all, branch, AProVE): 7.60723, 2.46167, 5.91381
Time/call in AProVE (Avg, Min, Max): 0.056322, 0.922138, 0.0166938
Time/T-call in AProVE (Avg, Min, Max): 0.056322, 0.922138, 0.922651
All conjectures solved.