%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP124-6.005 : TPTP v9.3.1. Released v1.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n019.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 10:12:42 AM UTC 2026
% Result : Satisfiable 4.36s 1.58s
% Output : Saturation 5.68s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u63,axiom,
~ product1(e_5,e_1,e_5) ).
cnf(u68,axiom,
product1(e_5,e_1,e_4) ).
cnf(u71,axiom,
~ product1(e_5,e_1,e_3) ).
cnf(u75,axiom,
~ product1(e_5,e_1,e_2) ).
cnf(u79,axiom,
~ product1(e_5,e_1,e_1) ).
cnf(u85,axiom,
product1(e_4,e_1,e_5) ).
cnf(u88,axiom,
~ product1(e_4,e_1,e_4) ).
cnf(u92,axiom,
~ product1(e_4,e_1,e_3) ).
cnf(u96,axiom,
~ product1(e_4,e_1,e_2) ).
cnf(u100,axiom,
~ product1(e_4,e_1,e_1) ).
cnf(u105,axiom,
~ product1(e_3,e_1,e_5) ).
cnf(u109,axiom,
~ product1(e_3,e_1,e_4) ).
cnf(u113,axiom,
~ product1(e_3,e_1,e_3) ).
cnf(u118,axiom,
product1(e_3,e_1,e_2) ).
cnf(u121,axiom,
~ product1(e_3,e_1,e_1) ).
cnf(u126,axiom,
~ product1(e_2,e_1,e_5) ).
cnf(u130,axiom,
~ product1(e_2,e_1,e_4) ).
cnf(u135,axiom,
product1(e_2,e_1,e_3) ).
cnf(u138,axiom,
~ product1(e_2,e_1,e_2) ).
cnf(u142,axiom,
~ product1(e_2,e_1,e_1) ).
cnf(u245,axiom,
~ product1(e_5,e_2,e_5) ).
cnf(u249,axiom,
~ product1(e_5,e_2,e_4) ).
cnf(u253,axiom,
~ product1(e_5,e_2,e_3) ).
cnf(u257,axiom,
~ product1(e_5,e_2,e_2) ).
cnf(u262,axiom,
product1(e_5,e_2,e_1) ).
cnf(u266,axiom,
~ product1(e_4,e_2,e_5) ).
cnf(u270,axiom,
~ product1(e_4,e_2,e_4) ).
cnf(u275,axiom,
product1(e_4,e_2,e_3) ).
cnf(u278,axiom,
~ product1(e_4,e_2,e_2) ).
cnf(u282,axiom,
~ product1(e_4,e_2,e_1) ).
cnf(u287,axiom,
~ product1(e_3,e_2,e_5) ).
cnf(u292,axiom,
product1(e_3,e_2,e_4) ).
cnf(u295,axiom,
~ product1(e_3,e_2,e_3) ).
cnf(u299,axiom,
~ product1(e_3,e_2,e_2) ).
cnf(u303,axiom,
~ product1(e_3,e_2,e_1) ).
cnf(u309,axiom,
product1(e_1,e_2,e_5) ).
cnf(u312,axiom,
~ product1(e_1,e_2,e_4) ).
cnf(u316,axiom,
~ product1(e_1,e_2,e_3) ).
cnf(u320,axiom,
~ product1(e_1,e_2,e_2) ).
cnf(u324,axiom,
~ product1(e_1,e_2,e_1) ).
cnf(u435,axiom,
~ product1(e_5,e_3,e_5) ).
cnf(u439,axiom,
~ product1(e_5,e_3,e_4) ).
cnf(u443,axiom,
~ product1(e_5,e_3,e_3) ).
cnf(u448,axiom,
product1(e_5,e_3,e_2) ).
cnf(u451,axiom,
~ product1(e_5,e_3,e_1) ).
cnf(u456,axiom,
~ product1(e_4,e_3,e_5) ).
cnf(u460,axiom,
~ product1(e_4,e_3,e_4) ).
cnf(u464,axiom,
~ product1(e_4,e_3,e_3) ).
cnf(u468,axiom,
~ product1(e_4,e_3,e_2) ).
cnf(u473,axiom,
product1(e_4,e_3,e_1) ).
cnf(u478,axiom,
product1(e_2,e_3,e_5) ).
cnf(u481,axiom,
~ product1(e_2,e_3,e_4) ).
cnf(u485,axiom,
~ product1(e_2,e_3,e_3) ).
cnf(u489,axiom,
~ product1(e_2,e_3,e_2) ).
cnf(u493,axiom,
~ product1(e_2,e_3,e_1) ).
cnf(u498,axiom,
~ product1(e_1,e_3,e_5) ).
cnf(u503,axiom,
product1(e_1,e_3,e_4) ).
cnf(u506,axiom,
~ product1(e_1,e_3,e_3) ).
cnf(u510,axiom,
~ product1(e_1,e_3,e_2) ).
cnf(u514,axiom,
~ product1(e_1,e_3,e_1) ).
cnf(u665,axiom,
~ product1(e_5,e_4,e_5) ).
cnf(u669,axiom,
~ product1(e_5,e_4,e_4) ).
cnf(u674,axiom,
product1(e_5,e_4,e_3) ).
cnf(u677,axiom,
~ product1(e_5,e_4,e_2) ).
cnf(u681,axiom,
~ product1(e_5,e_4,e_1) ).
cnf(u687,axiom,
product1(e_3,e_4,e_5) ).
cnf(u690,axiom,
~ product1(e_3,e_4,e_4) ).
cnf(u694,axiom,
~ product1(e_3,e_4,e_3) ).
cnf(u698,axiom,
~ product1(e_3,e_4,e_2) ).
cnf(u702,axiom,
~ product1(e_3,e_4,e_1) ).
cnf(u707,axiom,
~ product1(e_2,e_4,e_5) ).
cnf(u711,axiom,
~ product1(e_2,e_4,e_4) ).
cnf(u715,axiom,
~ product1(e_2,e_4,e_3) ).
cnf(u719,axiom,
~ product1(e_2,e_4,e_2) ).
cnf(u724,axiom,
product1(e_2,e_4,e_1) ).
cnf(u728,axiom,
~ product1(e_1,e_4,e_5) ).
cnf(u732,axiom,
~ product1(e_1,e_4,e_4) ).
cnf(u736,axiom,
~ product1(e_1,e_4,e_3) ).
cnf(u741,axiom,
product1(e_1,e_4,e_2) ).
cnf(u744,axiom,
~ product1(e_1,e_4,e_1) ).
cnf(u905,axiom,
~ product1(e_4,e_5,e_5) ).
cnf(u909,axiom,
~ product1(e_4,e_5,e_4) ).
cnf(u913,axiom,
~ product1(e_4,e_5,e_3) ).
cnf(u918,axiom,
product1(e_4,e_5,e_2) ).
cnf(u921,axiom,
~ product1(e_4,e_5,e_1) ).
cnf(u926,axiom,
~ product1(e_3,e_5,e_5) ).
cnf(u930,axiom,
~ product1(e_3,e_5,e_4) ).
cnf(u943,axiom,
product1(e_3,e_5,e_1) ).
cnf(u947,axiom,
~ product1(e_2,e_5,e_5) ).
cnf(u952,axiom,
product1(e_2,e_5,e_4) ).
cnf(u955,axiom,
~ product1(e_2,e_5,e_3) ).
cnf(u959,axiom,
~ product1(e_2,e_5,e_2) ).
cnf(u963,axiom,
~ product1(e_2,e_5,e_1) ).
cnf(u968,axiom,
~ product1(e_1,e_5,e_5) ).
cnf(u972,axiom,
~ product1(e_1,e_5,e_4) ).
cnf(u977,axiom,
product1(e_1,e_5,e_3) ).
cnf(u980,axiom,
~ product1(e_1,e_5,e_2) ).
cnf(u984,axiom,
~ product1(e_1,e_5,e_1) ).
cnf(u1153,axiom,
~ product2(e_4,e_1,e_5) ).
cnf(u1161,axiom,
~ product2(e_4,e_1,e_3) ).
cnf(u1166,axiom,
product2(e_4,e_1,e_2) ).
cnf(u1174,axiom,
~ product2(e_3,e_1,e_5) ).
cnf(u1179,axiom,
product2(e_3,e_1,e_4) ).
cnf(u1186,axiom,
~ product2(e_3,e_1,e_2) ).
cnf(u1196,axiom,
product2(e_2,e_1,e_5) ).
cnf(u1199,axiom,
~ product2(e_2,e_1,e_4) ).
cnf(u1203,axiom,
~ product2(e_2,e_1,e_3) ).
cnf(u1232,axiom,
~ product2(e_5,e_1,e_4) ).
cnf(u1237,axiom,
product2(e_5,e_1,e_3) ).
cnf(u1388,axiom,
~ product2(e_4,e_2,e_5) ).
cnf(u1396,axiom,
~ product2(e_4,e_2,e_3) ).
cnf(u1405,axiom,
product2(e_4,e_2,e_1) ).
cnf(u1410,axiom,
product2(e_3,e_2,e_5) ).
cnf(u1413,axiom,
~ product2(e_3,e_2,e_4) ).
cnf(u1425,axiom,
~ product2(e_3,e_2,e_1) ).
cnf(u1593,axiom,
~ product2(e_5,e_3,e_4) ).
cnf(u1597,axiom,
~ product2(e_5,e_3,e_3) ).
cnf(u1601,axiom,
~ product2(e_5,e_3,e_2) ).
cnf(u1606,axiom,
product2(e_5,e_3,e_1) ).
cnf(u1611,axiom,
product2(e_4,e_3,e_5) ).
cnf(u1622,axiom,
~ product2(e_4,e_3,e_2) ).
cnf(u1626,axiom,
~ product2(e_4,e_3,e_1) ).
cnf(u1716,axiom,
~ product2(e_1,e_2,e_4) ).
cnf(u1721,axiom,
product2(e_1,e_2,e_3) ).
cnf(u1740,axiom,
~ product2(e_2,e_3,e_5) ).
cnf(u1745,axiom,
product2(e_2,e_3,e_4) ).
cnf(u1756,axiom,
~ product2(e_2,e_3,e_1) ).
cnf(u1843,axiom,
product2(e_5,e_4,e_2) ).
cnf(u1846,axiom,
~ product2(e_5,e_4,e_1) ).
cnf(u1851,axiom,
~ product2(e_3,e_4,e_5) ).
cnf(u1855,axiom,
~ product2(e_3,e_4,e_4) ).
cnf(u1868,axiom,
product2(e_3,e_4,e_1) ).
cnf(u1873,axiom,
product2(e_1,e_4,e_5) ).
cnf(u1880,axiom,
~ product2(e_1,e_4,e_3) ).
cnf(u1884,axiom,
~ product2(e_1,e_4,e_2) ).
cnf(u1973,axiom,
~ product2(e_1,e_3,e_5) ).
cnf(u1977,axiom,
~ product2(e_1,e_3,e_4) ).
cnf(u1986,axiom,
product2(e_1,e_3,e_2) ).
cnf(u2106,axiom,
~ product2(e_4,e_5,e_5) ).
cnf(u2115,axiom,
product2(e_4,e_5,e_3) ).
cnf(u2118,axiom,
~ product2(e_4,e_5,e_2) ).
cnf(u2122,axiom,
~ product2(e_4,e_5,e_1) ).
cnf(u2131,axiom,
~ product2(e_3,e_5,e_4) ).
cnf(u2140,axiom,
product2(e_3,e_5,e_2) ).
cnf(u2148,axiom,
~ product2(e_2,e_5,e_5) ).
cnf(u2156,axiom,
~ product2(e_2,e_5,e_3) ).
cnf(u2165,axiom,
product2(e_2,e_5,e_1) ).
cnf(u2169,axiom,
~ product2(e_1,e_5,e_5) ).
cnf(u2174,axiom,
product2(e_1,e_5,e_4) ).
cnf(u2177,axiom,
~ product2(e_1,e_5,e_3) ).
cnf(u2181,axiom,
~ product2(e_1,e_5,e_2) ).
cnf(u2088,axiom,
( ~ product1(e_1,X0,e_5)
| equalish(X0,e_2) ) ).
cnf(u2885,axiom,
( ~ product2(e_3,e_2,X0)
| equalish(X0,e_5) ) ).
cnf(u1324,axiom,
( ~ product1(e_4,X0,e_3)
| equalish(X0,e_2) ) ).
cnf(u2304,negated_conjecture,
( ~ product1(e_1,X0,e_3)
| product2(e_2,X0,e_1) ) ).
cnf(u2041,axiom,
( ~ product1(X0,e_1,e_4)
| equalish(X0,e_5) ) ).
cnf(u2328,axiom,
( ~ product1(X0,e_4,e_1)
| equalish(X0,e_2) ) ).
cnf(u52,axiom,
( ~ group_element(X0)
| product1(X0,e_2,e_1)
| product1(X0,e_2,e_2)
| product1(X0,e_2,e_3)
| product1(X0,e_2,e_4)
| product1(X0,e_2,e_5) ) ).
cnf(u2322,axiom,
( ~ product1(X0,e_3,e_5)
| equalish(X0,e_2) ) ).
cnf(u2302,axiom,
( ~ product1(e_3,X0,e_2)
| equalish(X0,e_1) ) ).
cnf(u2296,axiom,
( ~ product1(e_4,e_1,X0)
| equalish(X0,e_5) ) ).
cnf(u2192,negated_conjecture,
( ~ product1(e_3,X0,e_1)
| product2(e_4,X0,e_3) ) ).
cnf(u2295,axiom,
( ~ product1(e_4,X0,e_5)
| equalish(X0,e_1) ) ).
cnf(u2676,axiom,
( ~ product2(e_3,e_4,X0)
| equalish(X0,e_1) ) ).
cnf(u2679,axiom,
( ~ product2(e_1,e_4,X0)
| equalish(X0,e_5) ) ).
cnf(u49,axiom,
( ~ product2(X0,X1,X1)
| equalish(X0,X1) ) ).
cnf(u2560,axiom,
( ~ product1(e_1,e_5,X0)
| equalish(X0,e_3) ) ).
cnf(u43,axiom,
( ~ product1(X0,X1,X1)
| equalish(X0,X1) ) ).
cnf(u45,axiom,
( ~ product2(X0,X0,X1)
| equalish(X1,X0) ) ).
cnf(u1732,negated_conjecture,
( ~ product2(X0,e_2,e_4)
| equalish(X0,e_5) ) ).
cnf(product2_total_function2,axiom,
( ~ product2(X0,X1,X3)
| ~ product2(X0,X1,X2)
| equalish(X2,X3) ) ).
cnf(u39,axiom,
( ~ product1(X0,X0,X1)
| equalish(X1,X0) ) ).
cnf(u2473,axiom,
( ~ product1(X0,e_1,e_3)
| equalish(X0,e_2) ) ).
cnf(u2677,axiom,
( ~ product2(X0,e_4,e_5)
| equalish(X0,e_1) ) ).
cnf(product1_total_function1,axiom,
( ~ group_element(X1)
| ~ group_element(X0)
| product1(X0,X1,e_1)
| product1(X0,X1,e_2)
| product1(X0,X1,e_3)
| product1(X0,X1,e_4)
| product1(X0,X1,e_5) ) ).
cnf(u2090,negated_conjecture,
( ~ product1(e_2,X0,e_1)
| product2(e_5,X0,e_2) ) ).
cnf(e_5_is_not_e_4,axiom,
~ equalish(e_5,e_4) ).
cnf(u2044,negated_conjecture,
( ~ product1(e_1,X0,e_5)
| product2(e_4,X0,e_1) ) ).
cnf(product1_right_cancellation,axiom,
( ~ product1(X0,X3,X2)
| ~ product1(X0,X1,X2)
| equalish(X1,X3) ) ).
cnf(e_4_is_not_e_2,axiom,
~ equalish(e_4,e_2) ).
cnf(u2533,axiom,
( ~ product1(e_5,X0,e_3)
| equalish(X0,e_4) ) ).
cnf(e_5_is_not_e_1,axiom,
~ equalish(e_5,e_1) ).
cnf(e_1_is_not_e_4,axiom,
~ equalish(e_1,e_4) ).
cnf(e_4_is_not_e_5,axiom,
~ equalish(e_4,e_5) ).
cnf(u2489,axiom,
( ~ product1(X0,e_3,e_2)
| equalish(X0,e_5) ) ).
cnf(u1323,axiom,
( ~ product1(X0,e_2,e_3)
| equalish(X0,e_4) ) ).
cnf(e_3_is_not_e_2,axiom,
~ equalish(e_3,e_2) ).
cnf(u2483,axiom,
( ~ product1(e_3,X0,e_4)
| equalish(X0,e_2) ) ).
cnf(element_2,axiom,
group_element(e_2) ).
cnf(element_1,axiom,
group_element(e_1) ).
cnf(u2485,negated_conjecture,
( ~ product1(e_2,X0,e_3)
| product2(e_4,X0,e_2) ) ).
cnf(u2502,axiom,
( ~ product1(X0,e_4,e_2)
| equalish(X0,e_1) ) ).
cnf(u2696,axiom,
( ~ product2(e_1,X0,e_2)
| equalish(X0,e_3) ) ).
cnf(u2654,axiom,
( ~ product2(e_2,X0,e_4)
| equalish(X0,e_3) ) ).
cnf(u2330,axiom,
( ~ product1(e_2,e_4,X0)
| equalish(X0,e_1) ) ).
cnf(u2089,axiom,
( ~ product1(e_1,e_2,X0)
| equalish(X0,e_5) ) ).
cnf(u2480,negated_conjecture,
( ~ product1(e_2,X0,e_5)
| product2(e_1,X0,e_2) ) ).
cnf(u2705,axiom,
( ~ product2(e_4,X0,e_3)
| equalish(X0,e_5) ) ).
cnf(u2474,axiom,
( ~ product1(e_2,X0,e_3)
| equalish(X0,e_1) ) ).
cnf(u2632,axiom,
( ~ product2(X0,e_3,e_5)
| equalish(X0,e_4) ) ).
cnf(u2294,axiom,
( ~ product1(X0,e_1,e_5)
| equalish(X0,e_4) ) ).
cnf(u2547,negated_conjecture,
( ~ product1(e_5,X0,e_3)
| product2(e_1,X0,e_5) ) ).
cnf(u2476,negated_conjecture,
( ~ product1(e_1,X0,e_2)
| product2(e_3,X0,e_1) ) ).
cnf(u208,axiom,
( ~ group_element(X0)
| product2(X0,e_4,e_1)
| product2(X0,e_4,e_2)
| product2(X0,e_4,e_3)
| product2(X0,e_4,e_4)
| product2(X0,e_4,e_5) ) ).
cnf(u2247,axiom,
( ~ product1(e_4,e_5,X0)
| equalish(X0,e_2) ) ).
cnf(u1326,negated_conjecture,
( ~ product1(e_2,X0,e_4)
| product2(e_3,X0,e_2) ) ).
cnf(u2606,axiom,
( ~ product2(e_4,X0,e_1)
| equalish(X0,e_2) ) ).
cnf(u2660,axiom,
( ~ product2(e_5,X0,e_2)
| equalish(X0,e_4) ) ).
cnf(u2561,negated_conjecture,
( ~ product1(e_5,X0,e_1)
| product2(e_3,X0,e_5) ) ).
cnf(u2559,axiom,
( ~ product1(e_1,X0,e_3)
| equalish(X0,e_5) ) ).
cnf(u2704,axiom,
( ~ product2(X0,e_5,e_3)
| equalish(X0,e_4) ) ).
cnf(u2545,axiom,
( ~ product1(e_3,X0,e_1)
| equalish(X0,e_5) ) ).
cnf(element_4,axiom,
group_element(e_4) ).
cnf(u2580,axiom,
( ~ product2(e_2,e_1,X0)
| equalish(X0,e_5) ) ).
cnf(u2494,axiom,
( ~ product1(X0,e_3,e_1)
| equalish(X0,e_4) ) ).
cnf(u2741,axiom,
( ~ product2(e_1,X0,e_4)
| equalish(X0,e_5) ) ).
cnf(u2324,axiom,
( ~ product1(e_2,e_3,X0)
| equalish(X0,e_5) ) ).
cnf(u2596,axiom,
( ~ product2(X0,e_1,e_3)
| equalish(X0,e_5) ) ).
cnf(u51,axiom,
( ~ group_element(X0)
| product1(X0,e_1,e_1)
| product1(X0,e_1,e_2)
| product1(X0,e_1,e_3)
| product1(X0,e_1,e_4)
| product1(X0,e_1,e_5) ) ).
cnf(u2534,axiom,
( ~ product1(e_5,e_4,X0)
| equalish(X0,e_3) ) ).
cnf(u54,axiom,
( ~ group_element(X0)
| product1(X0,e_4,e_1)
| product1(X0,e_4,e_2)
| product1(X0,e_4,e_3)
| product1(X0,e_4,e_4)
| product1(X0,e_4,e_5) ) ).
cnf(u53,axiom,
( ~ group_element(X0)
| product1(X0,e_3,e_1)
| product1(X0,e_3,e_2)
| product1(X0,e_3,e_3)
| product1(X0,e_3,e_4)
| product1(X0,e_3,e_5) ) ).
cnf(u40,axiom,
equalish(X0,X0) ).
cnf(u2674,axiom,
( ~ product2(X0,e_4,e_1)
| equalish(X0,e_3) ) ).
cnf(u47,axiom,
( ~ product2(X0,X1,X0)
| equalish(X1,X0) ) ).
cnf(u2718,axiom,
( ~ product2(e_3,e_5,X0)
| equalish(X0,e_2) ) ).
cnf(product2_left_cancellation,axiom,
( ~ product2(X3,X1,X2)
| ~ product2(X0,X1,X2)
| equalish(X0,X3) ) ).
cnf(u2558,axiom,
( ~ product1(X0,e_5,e_3)
| equalish(X0,e_1) ) ).
cnf(u2697,axiom,
( ~ product2(e_1,e_3,X0)
| equalish(X0,e_2) ) ).
cnf(u2884,axiom,
( ~ product2(e_3,X0,e_5)
| equalish(X0,e_2) ) ).
cnf(u1127,negated_conjecture,
product2(e_2,e_4,e_3) ).
cnf(u2733,axiom,
( ~ product2(e_2,e_5,X0)
| equalish(X0,e_1) ) ).
cnf(u2649,axiom,
( ~ product2(e_1,e_2,X0)
| equalish(X0,e_3) ) ).
cnf(u2554,negated_conjecture,
( ~ product1(e_5,X0,e_2)
| product2(e_4,X0,e_5) ) ).
cnf(u2731,axiom,
( ~ product2(X0,e_5,e_1)
| equalish(X0,e_2) ) ).
cnf(u2742,axiom,
( ~ product2(e_1,e_5,X0)
| equalish(X0,e_4) ) ).
cnf(u2475,axiom,
( ~ product1(e_2,e_1,X0)
| equalish(X0,e_3) ) ).
cnf(u2634,axiom,
( ~ product2(e_4,e_3,X0)
| equalish(X0,e_5) ) ).
cnf(u2477,axiom,
( ~ product1(X0,e_2,e_1)
| equalish(X0,e_5) ) ).
cnf(u1780,axiom,
( ~ product1(e_3,X0,e_5)
| equalish(X0,e_4) ) ).
cnf(u2504,axiom,
( ~ product1(e_1,e_4,X0)
| equalish(X0,e_2) ) ).
cnf(u2189,axiom,
( ~ product1(X0,e_3,e_4)
| equalish(X0,e_1) ) ).
cnf(qg2a,negated_conjecture,
( ~ product1(X2,X0,X3)
| ~ product1(X0,X1,X2)
| product2(X3,X1,X0) ) ).
cnf(u2497,negated_conjecture,
( ~ product1(e_3,X0,e_4)
| product2(e_1,X0,e_3) ) ).
cnf(u1325,axiom,
( ~ product1(e_4,e_2,X0)
| equalish(X0,e_3) ) ).
cnf(u2246,axiom,
( ~ product1(e_4,X0,e_2)
| equalish(X0,e_5) ) ).
cnf(u2597,axiom,
( ~ product2(e_5,X0,e_3)
| equalish(X0,e_1) ) ).
cnf(product2_right_cancellation,axiom,
( ~ product2(X0,X3,X2)
| ~ product2(X0,X1,X2)
| equalish(X1,X3) ) ).
cnf(u2647,axiom,
( ~ product2(X0,e_2,e_3)
| equalish(X0,e_1) ) ).
cnf(u2248,negated_conjecture,
( ~ product1(e_5,X0,e_4)
| product2(e_2,X0,e_5) ) ).
cnf(product1_total_function2,axiom,
( ~ product1(X0,X1,X3)
| ~ product1(X0,X1,X2)
| equalish(X2,X3) ) ).
cnf(u2717,axiom,
( ~ product2(e_3,X0,e_2)
| equalish(X0,e_5) ) ).
cnf(product1_idempotence,axiom,
product1(X0,X0,X0) ).
cnf(product1_left_cancellation,axiom,
( ~ product1(X3,X1,X2)
| ~ product1(X0,X1,X2)
| equalish(X0,X3) ) ).
cnf(u2535,negated_conjecture,
( ~ product1(e_4,X0,e_5)
| product2(e_3,X0,e_4) ) ).
cnf(e_3_is_not_e_4,axiom,
~ equalish(e_3,e_4) ).
cnf(u209,axiom,
( ~ group_element(X0)
| product2(X0,e_5,e_1)
| product2(X0,e_5,e_2)
| product2(X0,e_5,e_3)
| product2(X0,e_5,e_4)
| product2(X0,e_5,e_5) ) ).
cnf(e_5_is_not_e_2,axiom,
~ equalish(e_5,e_2) ).
cnf(e_2_is_not_e_1,axiom,
~ equalish(e_2,e_1) ).
cnf(e_1_is_not_e_5,axiom,
~ equalish(e_1,e_5) ).
cnf(u2578,axiom,
( ~ product2(X0,e_1,e_5)
| equalish(X0,e_2) ) ).
cnf(e_2_is_not_e_4,axiom,
~ equalish(e_2,e_4) ).
cnf(element_3,axiom,
group_element(e_3) ).
cnf(e_1_is_not_e_2,axiom,
~ equalish(e_1,e_2) ).
cnf(element_5,axiom,
group_element(e_5) ).
cnf(u1779,axiom,
( ~ product1(X0,e_4,e_5)
| equalish(X0,e_3) ) ).
cnf(u2883,axiom,
( ~ product2(X0,e_2,e_5)
| equalish(X0,e_3) ) ).
cnf(u2467,negated_conjecture,
( ~ product2(X0,e_4,e_3)
| equalish(X0,e_2) ) ).
cnf(u2191,axiom,
( ~ product1(e_1,e_3,X0)
| equalish(X0,e_4) ) ).
cnf(u2653,axiom,
( ~ product2(X0,e_3,e_4)
| equalish(X0,e_2) ) ).
cnf(u2043,axiom,
( ~ product1(e_5,e_1,X0)
| equalish(X0,e_4) ) ).
cnf(u2579,axiom,
( ~ product2(e_2,X0,e_5)
| equalish(X0,e_1) ) ).
cnf(u2574,axiom,
( ~ product2(e_3,e_1,X0)
| equalish(X0,e_4) ) ).
cnf(u1782,negated_conjecture,
( ~ product1(e_4,X0,e_3)
| product2(e_5,X0,e_4) ) ).
cnf(u2568,axiom,
( ~ product2(e_4,e_1,X0)
| equalish(X0,e_2) ) ).
cnf(u1781,axiom,
( ~ product1(e_3,e_4,X0)
| equalish(X0,e_5) ) ).
cnf(u2605,axiom,
( ~ product2(X0,e_2,e_1)
| equalish(X0,e_4) ) ).
cnf(u2551,axiom,
( ~ product1(X0,e_5,e_4)
| equalish(X0,e_2) ) ).
cnf(u2566,axiom,
( ~ product2(X0,e_1,e_2)
| equalish(X0,e_4) ) ).
cnf(u206,axiom,
( ~ group_element(X0)
| product2(X0,e_2,e_1)
| product2(X0,e_2,e_2)
| product2(X0,e_2,e_3)
| product2(X0,e_2,e_4)
| product2(X0,e_2,e_5) ) ).
cnf(u205,axiom,
( ~ group_element(X0)
| product2(X0,e_1,e_1)
| product2(X0,e_1,e_2)
| product2(X0,e_1,e_3)
| product2(X0,e_1,e_4)
| product2(X0,e_1,e_5) ) ).
cnf(u2655,axiom,
( ~ product2(e_2,e_3,X0)
| equalish(X0,e_4) ) ).
cnf(u2479,axiom,
( ~ product1(e_5,e_2,X0)
| equalish(X0,e_1) ) ).
cnf(u2740,axiom,
( ~ product2(X0,e_5,e_4)
| equalish(X0,e_1) ) ).
cnf(u2190,axiom,
( ~ product1(e_1,X0,e_4)
| equalish(X0,e_3) ) ).
cnf(u2331,negated_conjecture,
( ~ product1(e_4,X0,e_2)
| product2(e_1,X0,e_4) ) ).
cnf(u2607,axiom,
( ~ product2(e_4,e_2,X0)
| equalish(X0,e_1) ) ).
cnf(u2532,axiom,
( ~ product1(X0,e_4,e_3)
| equalish(X0,e_5) ) ).
cnf(u2468,negated_conjecture,
( ~ product2(e_2,X0,e_3)
| equalish(X0,e_4) ) ).
cnf(u2297,negated_conjecture,
( ~ product1(e_1,X0,e_4)
| product2(e_5,X0,e_1) ) ).
cnf(u2495,axiom,
( ~ product1(e_4,X0,e_1)
| equalish(X0,e_3) ) ).
cnf(u2544,axiom,
( ~ product1(X0,e_5,e_1)
| equalish(X0,e_3) ) ).
cnf(u2484,axiom,
( ~ product1(e_3,e_2,X0)
| equalish(X0,e_4) ) ).
cnf(u2478,axiom,
( ~ product1(e_5,X0,e_1)
| equalish(X0,e_2) ) ).
cnf(u2630,axiom,
( ~ product2(e_5,X0,e_1)
| equalish(X0,e_3) ) ).
cnf(u2087,axiom,
( ~ product1(X0,e_2,e_5)
| equalish(X0,e_1) ) ).
cnf(u55,axiom,
( ~ group_element(X0)
| product1(X0,e_5,e_1)
| product1(X0,e_5,e_2)
| product1(X0,e_5,e_3)
| product1(X0,e_5,e_4)
| product1(X0,e_5,e_5) ) ).
cnf(u2553,axiom,
( ~ product1(e_2,e_5,X0)
| equalish(X0,e_4) ) ).
cnf(u2706,axiom,
( ~ product2(e_4,e_5,X0)
| equalish(X0,e_3) ) ).
cnf(u41,axiom,
( ~ product1(X0,X1,X0)
| equalish(X1,X0) ) ).
cnf(product2_idempotence,axiom,
product2(X0,X0,X0) ).
cnf(u37,negated_conjecture,
( ~ product1(X0,X1,X0)
| product2(X0,X1,X0) ) ).
cnf(e_5_is_not_e_3,axiom,
~ equalish(e_5,e_3) ).
cnf(u2552,axiom,
( ~ product1(e_2,X0,e_4)
| equalish(X0,e_5) ) ).
cnf(product2_total_function1,axiom,
( ~ group_element(X1)
| ~ group_element(X0)
| product2(X0,X1,e_1)
| product2(X0,X1,e_2)
| product2(X0,X1,e_3)
| product2(X0,X1,e_4)
| product2(X0,X1,e_5) ) ).
cnf(e_4_is_not_e_1,axiom,
~ equalish(e_4,e_1) ).
cnf(e_3_is_not_e_5,axiom,
~ equalish(e_3,e_5) ).
cnf(u2546,axiom,
( ~ product1(e_3,e_5,X0)
| equalish(X0,e_1) ) ).
cnf(u2629,axiom,
( ~ product2(X0,e_3,e_1)
| equalish(X0,e_5) ) ).
cnf(u1734,negated_conjecture,
( ~ product2(e_5,e_2,X0)
| equalish(X0,e_4) ) ).
cnf(u2329,axiom,
( ~ product1(e_2,X0,e_1)
| equalish(X0,e_4) ) ).
cnf(u1733,negated_conjecture,
( ~ product2(e_5,X0,e_4)
| equalish(X0,e_2) ) ).
cnf(u2323,axiom,
( ~ product1(e_2,X0,e_5)
| equalish(X0,e_3) ) ).
cnf(u2567,axiom,
( ~ product2(e_4,X0,e_2)
| equalish(X0,e_1) ) ).
cnf(u2325,negated_conjecture,
( ~ product1(e_3,X0,e_2)
| product2(e_5,X0,e_3) ) ).
cnf(u2633,axiom,
( ~ product2(e_4,X0,e_5)
| equalish(X0,e_3) ) ).
cnf(u2598,axiom,
( ~ product2(e_5,e_1,X0)
| equalish(X0,e_3) ) ).
cnf(u2675,axiom,
( ~ product2(e_3,X0,e_1)
| equalish(X0,e_4) ) ).
cnf(u2042,axiom,
( ~ product1(e_5,X0,e_4)
| equalish(X0,e_1) ) ).
cnf(u2695,axiom,
( ~ product2(X0,e_3,e_2)
| equalish(X0,e_1) ) ).
cnf(u2572,axiom,
( ~ product2(X0,e_1,e_4)
| equalish(X0,e_3) ) ).
cnf(u2659,axiom,
( ~ product2(X0,e_4,e_2)
| equalish(X0,e_5) ) ).
cnf(u2482,axiom,
( ~ product1(X0,e_2,e_4)
| equalish(X0,e_3) ) ).
cnf(u2490,axiom,
( ~ product1(e_5,X0,e_2)
| equalish(X0,e_3) ) ).
cnf(u2648,axiom,
( ~ product2(e_1,X0,e_3)
| equalish(X0,e_2) ) ).
cnf(u2732,axiom,
( ~ product2(e_2,X0,e_1)
| equalish(X0,e_5) ) ).
cnf(u2503,axiom,
( ~ product1(e_1,X0,e_2)
| equalish(X0,e_4) ) ).
cnf(u2301,axiom,
( ~ product1(X0,e_1,e_2)
| equalish(X0,e_3) ) ).
cnf(u2492,negated_conjecture,
( ~ product1(e_3,X0,e_5)
| product2(e_2,X0,e_3) ) ).
cnf(u2303,axiom,
( ~ product1(e_3,e_1,X0)
| equalish(X0,e_2) ) ).
cnf(u844,negated_conjecture,
product2(e_5,e_2,e_4) ).
cnf(u2491,axiom,
( ~ product1(e_5,e_3,X0)
| equalish(X0,e_2) ) ).
cnf(u2573,axiom,
( ~ product2(e_3,X0,e_4)
| equalish(X0,e_1) ) ).
cnf(u2496,axiom,
( ~ product1(e_4,e_3,X0)
| equalish(X0,e_1) ) ).
cnf(u2245,axiom,
( ~ product1(X0,e_5,e_2)
| equalish(X0,e_4) ) ).
cnf(e_4_is_not_e_3,axiom,
~ equalish(e_4,e_3) ).
cnf(u2631,axiom,
( ~ product2(e_5,e_3,X0)
| equalish(X0,e_1) ) ).
cnf(e_2_is_not_e_3,axiom,
~ equalish(e_2,e_3) ).
cnf(u2469,negated_conjecture,
( ~ product2(e_2,e_4,X0)
| equalish(X0,e_3) ) ).
cnf(e_3_is_not_e_1,axiom,
~ equalish(e_3,e_1) ).
cnf(u207,axiom,
( ~ group_element(X0)
| product2(X0,e_3,e_1)
| product2(X0,e_3,e_2)
| product2(X0,e_3,e_3)
| product2(X0,e_3,e_4)
| product2(X0,e_3,e_5) ) ).
cnf(e_2_is_not_e_5,axiom,
~ equalish(e_2,e_5) ).
cnf(e_1_is_not_e_3,axiom,
~ equalish(e_1,e_3) ).
cnf(u2678,axiom,
( ~ product2(e_1,X0,e_5)
| equalish(X0,e_4) ) ).
cnf(u2505,negated_conjecture,
( ~ product1(e_4,X0,e_1)
| product2(e_2,X0,e_4) ) ).
cnf(u2661,axiom,
( ~ product2(e_5,e_4,X0)
| equalish(X0,e_2) ) ).
cnf(u2716,axiom,
( ~ product2(X0,e_5,e_2)
| equalish(X0,e_3) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP124-6.005 : TPTP v9.3.1. Released v1.2.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.38 % Computer : n019.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Sun Sep 27 09:21:49 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.41 Running first-order theorem proving
% 0.11/0.41 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.36/1.58 % (2828006)Input is clausal, will run a generic CNF schedule.
% 4.36/1.58 % (2828015)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1367673928:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 4.36/1.58 % (2828015)Instruction limit reached!
% 4.36/1.58 % (2828015)------------------------------
% 4.36/1.58 % (2828015)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.36/1.58 % (2828015)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.36/1.58 % (2828015)CaDiCaL version: 2.1.3
% 4.36/1.58 % (2828015)Termination reason: Instruction limit
% 4.36/1.58 % (2828015)Termination phase: Saturation
% 4.36/1.58 % (2828015)Time elapsed: 0.033 s
% 4.36/1.58 % (2828015)Peak memory usage: 88 MB
% 4.36/1.58 % (2828015)Instructions burned: 117 (million)
% 4.36/1.58 % (2828014)lrs+10_1_sil=8000:sp=occurrence:random_seed=992762559:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 4.36/1.58 % (2828013)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=541284953:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 4.36/1.58 % (2828011)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=943822796:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 4.36/1.58 % (2828012)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=920037527:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 4.36/1.58 % (2828016)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=602392247:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 4.36/1.58 % (2828017)dis-21_1_sil=8000:lcm=predicate:random_seed=553669300:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 4.36/1.58 % (2828014)Instruction limit reached!
% 4.36/1.58 % (2828014)------------------------------
% 4.36/1.58 % (2828014)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.36/1.58 % (2828014)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.36/1.58 % (2828014)CaDiCaL version: 2.1.3
% 4.36/1.58 % (2828014)Termination reason: Instruction limit
% 4.36/1.58 % (2828014)Termination phase: Saturation
% 4.36/1.58 % (2828014)Time elapsed: 0.059 s
% 4.36/1.58 % (2828014)Peak memory usage: 88 MB
% 4.36/1.58 % (2828014)Instructions burned: 107 (million)
% 4.36/1.58 % (2828017)Instruction limit reached!
% 4.36/1.58 % (2828017)------------------------------
% 4.36/1.58 % (2828017)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.36/1.58 % (2828017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.36/1.58 % (2828017)CaDiCaL version: 2.1.3
% 4.36/1.58 % (2828017)Termination reason: Instruction limit
% 4.36/1.58 % (2828017)Termination phase: Saturation
% 4.36/1.58 % (2828017)Time elapsed: 0.071 s
% 4.36/1.58 % (2828017)Peak memory usage: 89 MB
% 4.36/1.58 % (2828017)Instructions burned: 118 (million)
% 4.36/1.58 % (2828019)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=1551855348:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 4.36/1.58 % (2828016)Instruction limit reached!
% 4.36/1.58 % (2828016)------------------------------
% 4.36/1.58 % (2828016)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.36/1.58 % (2828016)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.36/1.58 % (2828016)CaDiCaL version: 2.1.3
% 4.36/1.58 % (2828016)Termination reason: Instruction limit
% 4.36/1.58 % (2828016)Termination phase: Saturation
% 4.36/1.58 % (2828016)Time elapsed: 0.106 s
% 4.36/1.58 % (2828016)Peak memory usage: 89 MB
% 4.36/1.58 % (2828016)Instructions burned: 180 (million)
% 4.36/1.58 % (2828019)Instruction limit reached!
% 4.36/1.58 % (2828019)------------------------------
% 4.36/1.58 % (2828019)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.36/1.58 % (2828019)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.36/1.58 % (2828019)CaDiCaL version: 2.1.3
% 4.36/1.58 % (2828019)Termination reason: Instruction limit
% 4.36/1.58 % (2828019)Termination phase: Saturation
% 4.36/1.58 % (2828019)Time elapsed: 0.046 s
% 4.36/1.58 % (2828019)Peak memory usage: 89 MB
% 4.36/1.58 % (2828019)Instructions burned: 145 (million)
% 4.36/1.58 % (2828026)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=547368530:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 4.36/1.58 % (2828026)Refutation not found, incomplete strategy
% 4.36/1.58 % (2828026)------------------------------
% 4.36/1.58 % (2828026)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.36/1.58 % (2828026)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.36/1.58 % (2828026)CaDiCaL version: 2.1.3
% 4.36/1.58 % (2828026)Termination reason: Refutation not found, incomplete strategy
% 4.36/1.58 % (2828026)Time elapsed: 0.002 s
% 4.36/1.58 % (2828026)Peak memory usage: 87 MB
% 4.36/1.58 % (2828026)Instructions burned: 1 (million)
% 4.36/1.58 % (2828027)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3590480945:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 4.36/1.58 % (2828029)lrs+10_64_to=lpo:sil=8000:random_seed=3317017207:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 4.36/1.58 % (2828030)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3117587953:avsq=on:i=194:fgj=on:bd=preordered_2996 on theBenchmark for (2996ds/194Mi)
% 4.36/1.58 % (2828029)First to succeed.
% 4.36/1.58 % (2828029)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2828006"
% 4.36/1.58 % (2828030)Instruction limit reached!
% 4.36/1.58 % (2828030)------------------------------
% 4.36/1.58 % (2828030)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.36/1.58 % (2828030)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.36/1.58 % (2828030)CaDiCaL version: 2.1.3
% 4.36/1.58 % (2828030)Termination reason: Instruction limit
% 4.36/1.58 % (2828030)Termination phase: Saturation
% 4.36/1.58 % (2828030)Time elapsed: 0.064 s
% 4.36/1.58 % (2828030)Peak memory usage: 89 MB
% 4.36/1.58 % (2828030)Instructions burned: 195 (million)
% 4.36/1.58 % (2828027)Instruction limit reached!
% 4.36/1.58 % (2828027)------------------------------
% 4.36/1.58 % (2828027)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.36/1.58 % (2828027)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.36/1.58 % (2828027)CaDiCaL version: 2.1.3
% 4.36/1.58 % (2828027)Termination reason: Instruction limit
% 4.36/1.58 % (2828027)Termination phase: Saturation
% 4.36/1.58 % (2828027)Time elapsed: 0.120 s
% 4.36/1.58 % (2828027)Peak memory usage: 88 MB
% 4.36/1.58 % (2828027)Instructions burned: 219 (million)
% 4.36/1.58 % (2828026)------------------------------
% 4.36/1.58 % (2828026)------------------------------
% 4.36/1.58 % (2828035)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=3021024902:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 4.36/1.58 % (2828035)Instruction limit reached!
% 4.36/1.58 % (2828035)------------------------------
% 4.36/1.58 % (2828035)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.36/1.58 % (2828035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.36/1.58 % (2828035)CaDiCaL version: 2.1.3
% 4.36/1.58 % (2828035)Termination reason: Instruction limit
% 4.36/1.58 % (2828035)Termination phase: Saturation
% 4.36/1.58 % (2828035)Time elapsed: 0.046 s
% 4.36/1.58 % (2828035)Peak memory usage: 89 MB
% 4.36/1.58 % (2828035)Instructions burned: 159 (million)
% 4.36/1.58 % (2828036)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1506866307:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi)
% 4.36/1.58 % SZS status Satisfiable for theBenchmark
% 4.36/1.58 % SZS output start Saturation.
% See solution above
% 5.68/1.78 % SZS output start Definitions and Model Updates.
% 5.68/1.78 % SZS output end Definitions and Model Updates.
% 5.68/1.78 % (2828029)------------------------------
% 5.68/1.78 % (2828029)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.68/1.78 % (2828029)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.68/1.78 % (2828029)CaDiCaL version: 2.1.3
% 5.68/1.78 % (2828029)Termination reason: Satisfiable
% 5.68/1.78 % (2828029)Time elapsed: 0.045 s
% 5.68/1.78 % (2828029)Peak memory usage: 88 MB
% 5.68/1.78 % (2828029)Instructions burned: 73 (million)
% 5.68/1.78 % (2828029)------------------------------
% 5.68/1.78 % (2828029)------------------------------
% 5.68/1.78 % (2828006)Success in time 0.721 s
% 5.68/1.78 % Vampire exiting
%------------------------------------------------------------------------------