[]: Open (size=30, cost=0, time=0, max=0, total=1.00136e-05, pending=1)
[1]: Open (size=30, cost=30, time=0.711899, max=0.656932, total=0.746247, pending=1)
[10]: Open (size=30, cost=30, time=0.79942, max=0.656932, total=0.881953, pending=2)
******* COMPLETION *******
c_union(c_insert(V_a0,V_B0,T_a0),V_C0,T_a0) -> c_insert(V_a0,c_union(V_B0,V_C0,T_a0),T_a0)
c_union(c_Message_Oparts(V_G0),c_Message_Oparts(V_H0),tc_Message_Omsg) -> c_Message_Oparts(c_union(V_G0,V_H0,tc_Message_Omsg))
c_union(c_emptyset,V_y0,T_a0) -> V_y0
**************************
On branch: [10]
With size, cost: 30, 30
Orientations: 6
Calls to AProVE (all, T, NT, ?): 5, 5, 0, 0
Time (all, branch, AProVE): 0.882399, 0.79942, 0.880191
Time/call in AProVE (Avg, Min, Max): 0.176038, 0.656721, 0.0338991
Time/T-call in AProVE (Avg, Min, Max): 0.176038, 0.656721, 0.656932
All conjectures solved.