[]: Open (size=76, cost=0, time=0, max=0, total=1.69277e-05, pending=1)
[0]: Open (size=76, cost=76, time=1.33761, max=0.838371, total=1.40542, pending=1)
[1]: Open (size=76, cost=76, time=1.24648, max=0.838371, total=1.69803, pending=2)
[01]: Open (size=76, cost=76, time=1.46792, max=0.838371, total=1.83808, pending=3)
[11]: Open (size=76, cost=76, time=1.28296, max=0.838371, total=2.41111, pending=4)
[00]: Open (size=76, cost=76, time=1.49797, max=0.838371, total=2.55869, pending=5)
[10]: Open (size=76, cost=76, time=1.34811, max=0.838371, total=3.15624, pending=6)
[110]: Open (size=76, cost=120, time=1.35616, max=0.838371, total=3.49512, pending=7)
[010]: Open (size=76, cost=124, time=1.96979, max=0.838371, total=3.59771, pending=8)
[100]: Open (size=76, cost=124, time=1.65462, max=0.838371, total=4.0921, pending=9)
[000]: Open (size=76, cost=128, time=1.98709, max=0.838371, total=4.74019, pending=10)
[111]: Open (size=76, cost=188, time=1.35352, max=0.838371, total=6.71557, pending=11)
[101]: Open (size=76, cost=236, time=1.37643, max=0.838371, total=6.91657, pending=12)
[011]: Open (size=76, cost=236, time=1.53504, max=0.838371, total=7.12792, pending=13)
[001]: Open (size=76, cost=284, time=1.6019, max=0.838371, total=7.30499, pending=14)
[1100]: Open (size=76, cost=288, time=1.40329, max=0.838371, total=8.10123, pending=15)
[11000]: Open (size=112, cost=196, time=1.4464, max=0.838371, total=8.29123, pending=16)
[110000]: Open (size=112, cost=196, time=1.48476, max=0.838371, total=8.4309, pending=17)
[1100001]: Open (size=193, cost=251, time=1.58256, max=0.838371, total=8.62056, pending=18)
[0100]: Open (size=76, cost=292, time=2.17542, max=0.838371, total=8.76269, pending=19)
[01001]: Open (size=114, cost=198, time=2.38137, max=0.838371, total=9.15935, pending=20)
[010010]: Open (size=114, cost=198, time=2.54521, max=0.838371, total=10.2579, pending=21)
[0100101]: Open (size=195, cost=253, time=2.8203, max=0.838371, total=10.8153, pending=22)
[1000]: Open (size=76, cost=292, time=1.97274, max=0.838371, total=11.8642, pending=23)
[10000]: Open (size=112, cost=196, time=2.11305, max=0.838371, total=12.7617, pending=24)
[100001]: Open (size=114, cost=198, time=2.44516, max=0.838371, total=13.2498, pending=25)
[1000011]: Open (size=195, cost=253, time=2.73509, max=0.838371, total=14.2133, pending=26)
[0000]: Open (size=76, cost=296, time=3.16348, max=1.17639, total=15.6274, pending=27)
[00001]: Open (size=114, cost=198, time=4.42063, max=1.25715, total=17.9843, pending=28)
[000011]: Open (size=116, cost=200, time=5.40529, max=1.25715, total=19.7431, pending=29)
[0000111]: Open (size=197, cost=255, time=6.67393, max=1.26864, total=21.9743, pending=30)
[1110]: Open (size=76, cost=356, time=1.43219, max=0.838371, total=26.0011, pending=31)
[11100]: Open (size=146, cost=306, time=1.58437, max=0.838371, total=30.3591, pending=32)
[111000]: Open (size=146, cost=306, time=1.61766, max=0.838371, total=32.8298, pending=33)
[1110001]: Open (size=272, cost=338, time=1.64249, max=0.838371, total=32.9214, pending=34)
[11000010]: Open (size=193, cost=364, time=1.63108, max=0.838371, total=33.003, pending=35)
[01001010]: Open (size=195, cost=366, time=3.1708, max=0.838371, total=33.2003, pending=36)
[10000110]: Open (size=195, cost=366, time=3.37838, max=0.838371, total=34.6193, pending=37)
[00001110]: Open (size=197, cost=368, time=8.95105, max=2.27712, total=35.6016, pending=38)
[11001]: Open (size=112, cost=390, time=1.50501, max=0.838371, total=40.4806, pending=39)
[10001]: Open (size=112, cost=390, time=2.70806, max=0.838371, total=41.2172, pending=40)
[110000101]: Open (size=189, cost=398, time=1.66514, max=0.838371, total=42.7246, pending=41)
[010010101]: Open (size=191, cost=400, time=3.48069, max=0.838371, total=42.9301, pending=42)
[100001101]: Open (size=191, cost=400, time=3.78808, max=0.838371, total=43.4262, pending=43)
[000011101]: Open (size=193, cost=402, time=11.3489, max=2.39783, total=44.5658, pending=44)
[1010]: Open (size=76, cost=404, time=1.48682, max=0.838371, total=48.9341, pending=45)
[10101]: Open (size=169, cost=301, time=1.70635, max=0.838371, total=49.2601, pending=46)
[101011]: Open (size=169, cost=329, time=5.18837, max=3.38402, total=58.1666, pending=47)
[0110]: Open (size=76, cost=404, time=1.62957, max=0.838371, total=76.1698, pending=47)
[01101]: Open (size=169, cost=301, time=1.83687, max=0.838371, total=76.4658, pending=48)
[011011]: Open (size=169, cost=329, time=4.48568, max=2.64881, total=79.3221, pending=49)
[1100001011]: Open (size=185, cost=422, time=1.69742, max=0.838371, total=97.491, pending=49)
[0100101011]: Open (size=187, cost=424, time=3.73321, max=0.838371, total=98.0939, pending=50)
[1000011011]: Open (size=187, cost=424, time=4.19758, max=0.838371, total=100.83, pending=51)
[11100011]: Open (size=267, cost=425, time=1.67804, max=0.838371, total=103.241, pending=52)
[0000111011]: Open (size=189, cost=426, time=14.4274, max=3.07855, total=103.581, pending=53)
[110001]: Open (size=112, cost=428, time=1.54294, max=0.838371, total=115.807, pending=53)
[110010]: Open (size=112, cost=428, time=1.55829, max=0.838371, total=116.059, pending=53)
[010011]: Open (size=114, cost=432, time=3.31095, max=0.929574, total=116.252, pending=53)
[100011]: Open (size=114, cost=432, time=3.49334, max=0.838371, total=117.721, pending=53)
[010011]: Open (size=220, cost=432, time=4.77095, max=0.929574, total=119.28, pending=53)
[100011]: Open (size=220, cost=432, time=5.04263, max=0.838371, total=119.995, pending=53)
[01000]: Open (size=114, cost=438, time=2.34488, max=0.838371, total=120.695, pending=53)
[00000]: Open (size=114, cost=438, time=4.22344, max=1.17639, total=121.506, pending=54)
[01001010110]: Open (size=163, cost=442, time=4.1522, max=0.838371, total=123.054, pending=55)
[110001]: Open (size=234, cost=443, time=1.78223, max=0.838371, total=123.756, pending=55)
[0000111011]: Open (size=165, cost=444, time=20.8382, max=3.27516, total=123.82, pending=55)
[110010]: Open (size=218, cost=446, time=1.73865, max=0.838371, total=130.288, pending=55)
[010011]: Open (size=220, cost=449, time=5.47788, max=0.929574, total=130.364, pending=55)
[100011]: Open (size=220, cost=449, time=5.73612, max=0.838371, total=131.092, pending=55)
[0010]: Open (size=76, cost=452, time=2.27951, max=0.838371, total=131.927, pending=55)
[00101]: Open (size=191, cost=365, time=3.72972, max=0.838371, total=133.763, pending=56)
[001011]: Open (size=192, cost=340, time=4.55107, max=0.838371, total=135.268, pending=57)
[110001]: Open (size=234, cost=460, time=1.83937, max=0.838371, total=141.533, pending=57)
[110010]: Open (size=218, cost=463, time=1.806, max=0.838371, total=142.228, pending=58)
[010011]: Open (size=220, cost=466, time=6.19611, max=0.929574, total=142.534, pending=59)
[100011]: Open (size=220, cost=466, time=6.56273, max=0.838371, total=144.578, pending=60)
[100000]: Open (size=114, cost=480, time=2.26356, max=0.838371, total=146.359, pending=61)
[010000]: Open (size=114, cost=480, time=2.44285, max=0.838371, total=146.666, pending=61)
[000001]: Open (size=116, cost=484, time=5.00004, max=1.17639, total=146.958, pending=61)
[000010]: Open (size=116, cost=484, time=5.18967, max=1.25715, total=149.192, pending=61)
[11000010110]: Open (size=161, cost=486, time=1.76934, max=0.838371, total=151.732, pending=61)
[10000110110]: Open (size=163, cost=488, time=5.27983, max=0.838371, total=151.972, pending=61)
[11101]: Open (size=146, cost=489, time=5.69484, max=4.14483, total=153.167, pending=61)
[100000]: Open (size=260, cost=491, time=2.55703, max=0.838371, total=161.569, pending=61)
[010000]: Open (size=260, cost=491, time=2.72054, max=0.838371, total=161.688, pending=61)
[000010]: Open (size=264, cost=495, time=7.71675, max=1.25715, total=161.795, pending=61)
[000001]: Open (size=244, cost=497, time=7.2189, max=1.17639, total=162.62, pending=61)
[1100010]: Open (size=235, cost=501, time=1.87129, max=0.838371, total=163.389, pending=61)
[1100100]: Open (size=219, cost=504, time=1.93696, max=0.838371, total=163.581, pending=62)
[0100111]: Open (size=221, cost=506, time=7.2951, max=1.09899, total=164.534, pending=63)
[1000110]: Open (size=221, cost=507, time=7.44444, max=0.881715, total=167.205, pending=64)
[010000]: Open (size=260, cost=512, time=2.81987, max=0.838371, total=169.503, pending=65)
[100000]: Open (size=260, cost=512, time=2.66759, max=0.838371, total=169.772, pending=66)
[011010]: Open (size=170, cost=513, time=2.02797, max=0.838371, total=170.631, pending=67)
[000010]: Open (size=264, cost=516, time=8.53001, max=1.25715, total=176.013, pending=67)
[10100]: Open (size=169, cost=517, time=1.65865, max=0.838371, total=178.07, pending=68)
[01100]: Open (size=169, cost=517, time=1.78031, max=0.838371, total=183.274, pending=68)
[000001]: Open (size=244, cost=518, time=7.97629, max=1.17639, total=185.893, pending=69)
[1100011]: Open (size=235, cost=520, time=2.49196, max=0.838371, total=188.312, pending=70)
[0100110]: Open (size=221, cost=526, time=7.12945, max=0.933335, total=190.213, pending=71)
[1100000]: Open (size=195, cost=526, time=1.56472, max=0.838371, total=192.819, pending=72)
[11101]: Open (size=146, cost=527, time=8.91902, max=4.14483, total=193.071, pending=73)
[111010]: Open (size=285, cost=421, time=12.2599, max=4.14483, total=200.66, pending=74)
[0100100]: Open (size=197, cost=529, time=2.82116, max=0.838371, total=207.488, pending=74)
[1000010]: Open (size=197, cost=529, time=3.10403, max=0.838371, total=208.413, pending=75)
[0000110]: Open (size=199, cost=532, time=6.36161, max=1.25715, total=209.642, pending=76)
[1100101]: Open (size=219, cost=533, time=1.9697, max=0.838371, total=212.559, pending=77)
[1000111]: Open (size=221, cost=536, time=7.45042, max=0.887692, total=213.532, pending=78)
[111000110]: Open (size=267, cost=538, time=1.70591, max=0.838371, total=216.002, pending=79)
[1110001101]: Open (size=240, cost=484, time=1.77513, max=0.838371, total=216.485, pending=80)
[001011]: Open (size=182, cost=541, time=5.63234, max=1.08128, total=216.979, pending=81)
[11000100]: Open (size=236, cost=542, time=1.93646, max=0.838371, total=223.889, pending=81)
[11001000]: Open (size=220, cost=545, time=1.99692, max=0.838371, total=224.381, pending=82)
[01001110]: Open (size=222, cost=547, time=8.59082, max=1.29572, total=224.96, pending=83)
[10001101]: Open (size=222, cost=547, time=8.64078, max=1.19634, total=229.496, pending=84)
[0100001]: Open (size=261, cost=549, time=2.94065, max=0.838371, total=233.213, pending=85)
[01001010110]: Open (size=232, cost=552, time=4.6783, max=0.838371, total=234.281, pending=86)
[010010101100]: Open (size=228, cost=459, time=5.60047, max=0.838371, total=236.942, pending=87)
[010010101101]: Open (size=228, cost=491, time=6.68994, max=1.4812, total=242.72, pending=87)
[010010101100]: Open (size=223, cost=517, time=5.99088, max=0.838371, total=249.971, pending=87)
[0100101011000]: Open (size=169, cost=264, time=7.32709, max=0.838371, total=259.946, pending=88)
[0100101011001]: Open (size=169, cost=279, time=8.64013, max=1.83026, total=260.571, pending=88)
[0100101011000]: Open (size=269, cost=353, time=7.94588, max=0.838371, total=262.32, pending=88)
******* COMPLETION *******
trans(congror2(X10),trans(congror1(X318),ortrue1)) -> trans(congror1(X318),ortrue1)
trans(congror1(X38),congror2(X28)) -> trans(congror2(X28),congror1(X38))
trans(congror2(X24),trans(congror2(X44),X35)) -> trans(congror2(trans(X24,X44)),X35)
trans(congror1(X10),trans(orfalse2,X31)) -> trans(orfalse2,trans(X10,X31))
trans(trans(X10,X20),X30) -> trans(X10,trans(X20,X30))
trans(congror1(X10),orfalse2) -> trans(orfalse2,X10)
trans(orfalse1,X10) -> trans(congror2(X10),orfalse1)
trans(congror2(X10),ortrue1) -> ortrue1
trans(congror1(X10),ortrue2) -> ortrue2
trans(ortrue2,X10) -> ortrue2
trans(X10,refl) -> X10
trans(ortrue1,X10) -> ortrue1
trans(refl,X10) -> X10
congror2(refl) -> refl
congror1(refl) -> refl
trans(congror2(X24),congror2(X44)) -> congror2(trans(X24,X44))
trans(congror1(X18),congror1(X38)) -> congror1(trans(X18,X38))
trans(congror1(X18),trans(congror1(X38),X39)) -> trans(congror1(trans(X18,X38)),X39)
trans(congror1(X38),trans(congror2(X28),X39)) -> trans(congror2(X28),trans(congror1(X38),X39))
**************************
On branch: [0100101011000]
With size, cost: 146, 230
Orientations: 346
Calls to AProVE (all, T, NT, ?): 286, 258, 11, 17
Time (all, branch, AProVE): 262.322, 7.94588, 259.751
Time/call in AProVE (Avg, Min, Max): 0.908219, 5.71958, 0.019882
Time/T-call in AProVE (Avg, Min, Max): 0.640359, 4.21248, 0.838371
All conjectures solved.