%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP134-1.005 : TPTP v9.3.1. Released v1.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n002.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:13:03 AM UTC 2026
% Result : Satisfiable 38.23s 6.27s
% Output : Saturation 38.78s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u49,axiom,
equalish(e_5,e_5) ).
cnf(u64,negated_conjecture,
~ product(e_5,e_5,e_5) ).
cnf(u68,negated_conjecture,
~ product(e_5,e_5,e_1) ).
cnf(u72,negated_conjecture,
~ product(e_5,e_5,e_2) ).
cnf(u76,negated_conjecture,
~ product(e_5,e_5,e_4) ).
cnf(u81,negated_conjecture,
product(e_5,e_5,e_3) ).
cnf(u85,negated_conjecture,
~ product(e_5,e_4,e_4) ).
cnf(u89,negated_conjecture,
~ product(e_5,e_4,e_3) ).
cnf(u93,negated_conjecture,
~ product(e_5,e_4,e_2) ).
cnf(u97,negated_conjecture,
~ product(e_5,e_4,e_1) ).
cnf(u102,negated_conjecture,
product(e_4,e_5,e_1) ).
cnf(u105,negated_conjecture,
~ product(e_4,e_5,e_2) ).
cnf(u109,negated_conjecture,
~ product(e_4,e_5,e_4) ).
cnf(u113,negated_conjecture,
~ product(e_4,e_5,e_3) ).
cnf(u118,negated_conjecture,
~ product(e_5,e_3,e_4) ).
cnf(u122,negated_conjecture,
~ product(e_5,e_3,e_3) ).
cnf(u127,negated_conjecture,
product(e_5,e_3,e_2) ).
cnf(u130,negated_conjecture,
~ product(e_5,e_3,e_1) ).
cnf(u143,negated_conjecture,
product(e_3,e_5,e_4) ).
cnf(u151,negated_conjecture,
~ product(e_5,e_2,e_4) ).
cnf(u164,negated_conjecture,
product(e_5,e_2,e_1) ).
cnf(u172,negated_conjecture,
product(e_2,e_5,e_2) ).
cnf(u179,negated_conjecture,
~ product(e_2,e_5,e_3) ).
cnf(u185,negated_conjecture,
product(e_5,e_1,e_4) ).
cnf(u188,negated_conjecture,
~ product(e_5,e_1,e_3) ).
cnf(u196,negated_conjecture,
~ product(e_5,e_1,e_1) ).
cnf(u200,negated_conjecture,
~ product(e_1,e_5,e_1) ).
cnf(u204,negated_conjecture,
~ product(e_1,e_5,e_2) ).
cnf(u208,negated_conjecture,
~ product(e_1,e_5,e_4) ).
cnf(u212,negated_conjecture,
~ product(e_1,e_5,e_3) ).
cnf(u289,negated_conjecture,
~ product(e_2,e_5,e_5) ).
cnf(u487,negated_conjecture,
~ product(e_4,e_5,e_5) ).
cnf(u742,negated_conjecture,
product(e_1,e_5,e_5) ).
cnf(u977,negated_conjecture,
product(e_4,e_3,e_4) ).
cnf(u1001,negated_conjecture,
~ product(e_2,e_3,e_2) ).
cnf(u1006,negated_conjecture,
product(e_2,e_3,e_1) ).
cnf(u1010,negated_conjecture,
~ product(e_1,e_3,e_4) ).
cnf(u1015,negated_conjecture,
product(e_1,e_3,e_3) ).
cnf(u1018,negated_conjecture,
~ product(e_1,e_3,e_2) ).
cnf(u1022,negated_conjecture,
~ product(e_1,e_3,e_1) ).
cnf(u1046,negated_conjecture,
product(e_3,e_4,e_1) ).
cnf(u1065,negated_conjecture,
~ product(e_3,e_2,e_4) ).
cnf(u1070,negated_conjecture,
product(e_3,e_2,e_3) ).
cnf(u1073,negated_conjecture,
~ product(e_3,e_2,e_2) ).
cnf(u1077,negated_conjecture,
~ product(e_3,e_2,e_1) ).
cnf(u1157,negated_conjecture,
product(e_3,e_1,e_2) ).
cnf(u1160,negated_conjecture,
~ product(e_3,e_1,e_1) ).
cnf(u1221,negated_conjecture,
product(e_4,e_1,e_3) ).
cnf(u1344,negated_conjecture,
~ product(e_2,e_2,e_1) ).
cnf(u1348,negated_conjecture,
~ product(e_2,e_2,e_2) ).
cnf(u1353,negated_conjecture,
product(e_2,e_2,e_4) ).
cnf(u1356,negated_conjecture,
~ product(e_2,e_2,e_3) ).
cnf(u1458,negated_conjecture,
product(e_1,e_1,e_1) ).
cnf(u1461,negated_conjecture,
~ product(e_1,e_1,e_2) ).
cnf(u1469,negated_conjecture,
~ product(e_1,e_1,e_3) ).
cnf(u1646,axiom,
( ~ group_element(X0)
| product(X1,e_3,e_1)
| product(X1,e_3,e_2)
| product(X1,e_3,e_3)
| product(X1,e_3,e_4)
| ~ group_element(X1)
| equalish(X0,e_3)
| product(X1,X0,e_1)
| product(X1,X0,e_2)
| product(X1,X0,e_3)
| product(X1,X0,e_4) ) ).
cnf(element_3,axiom,
group_element(e_3) ).
cnf(u819,negated_conjecture,
( ~ product(e_4,e_5,X0)
| product(X0,e_5,e_5) ) ).
cnf(u476,negated_conjecture,
( ~ product(X0,e_5,e_4)
| equalish(X0,e_3) ) ).
cnf(u928,negated_conjecture,
( ~ product(e_4,e_2,X0)
| product(X0,e_3,e_2) ) ).
cnf(u55,negated_conjecture,
( ~ group_element(X0)
| product(X0,e_5,e_3)
| product(X0,e_5,e_4)
| product(X0,e_5,e_2)
| product(X0,e_5,e_1)
| product(e_5,e_5,X0)
| product(e_5,X0,e_1)
| product(e_5,X0,e_2)
| product(e_5,X0,e_3)
| product(e_5,X0,e_4) ) ).
cnf(u951,negated_conjecture,
( ~ group_element(X0)
| product(X0,e_1,e_1)
| product(X0,e_1,e_2)
| product(X0,e_1,e_3)
| product(X0,e_1,e_4)
| equalish(X0,e_2) ) ).
cnf(e_5_is_not_e_1,axiom,
~ equalish(e_5,e_1) ).
cnf(u965,negated_conjecture,
( ~ group_element(X0)
| equalish(X0,e_3)
| product(e_3,X0,e_1)
| product(e_3,X0,e_2)
| product(e_3,X0,e_3)
| product(e_3,X0,e_4) ) ).
cnf(u1688,axiom,
( ~ group_element(X0)
| product(X0,e_4,e_2)
| product(X0,e_4,e_3)
| product(X0,e_4,e_4)
| product(X0,e_4,e_1)
| product(X0,e_2,e_1)
| product(X0,e_2,e_2)
| product(X0,e_2,e_3)
| product(X0,e_2,e_4) ) ).
cnf(u419,negated_conjecture,
( ~ product(e_5,e_2,X0)
| product(X0,e_2,e_2) ) ).
cnf(u1052,negated_conjecture,
( ~ product(e_3,e_4,X0)
| equalish(X0,e_1) ) ).
cnf(u51,negated_conjecture,
( ~ group_element(X0)
| product(X0,e_1,e_3)
| product(X0,e_1,e_4)
| product(X0,e_1,e_2)
| product(X0,e_1,e_1)
| product(e_5,e_5,X0)
| product(e_1,X0,e_1)
| product(e_1,X0,e_2)
| product(e_1,X0,e_3)
| product(e_1,X0,e_4) ) ).
cnf(u40,axiom,
( ~ group_element(X1)
| equalish(X0,X1)
| product(X2,X1,e_1)
| product(X2,X1,e_2)
| product(X2,X1,e_3)
| product(X2,X1,e_4)
| ~ group_element(X2)
| ~ group_element(X0)
| product(X2,X0,e_1)
| product(X2,X0,e_2)
| product(X2,X0,e_3)
| product(X2,X0,e_4) ) ).
cnf(u1234,negated_conjecture,
( ~ product(e_4,X0,e_3)
| equalish(X0,e_1) ) ).
cnf(u1689,axiom,
( ~ group_element(X0)
| product(X0,e_4,e_2)
| product(X0,e_4,e_3)
| product(X0,e_4,e_4)
| product(X0,e_4,e_1)
| product(X0,e_1,e_1)
| product(X0,e_1,e_2)
| product(X0,e_1,e_3)
| product(X0,e_1,e_4) ) ).
cnf(u817,negated_conjecture,
( ~ product(e_5,X0,e_5)
| equalish(X0,e_4) ) ).
cnf(u1656,axiom,
( ~ group_element(X0)
| product(X0,e_5,e_2)
| product(X0,e_5,e_3)
| product(X0,e_5,e_4)
| product(X0,e_5,e_1)
| product(X0,e_3,e_1)
| product(X0,e_3,e_2)
| product(X0,e_3,e_3)
| product(X0,e_3,e_4) ) ).
cnf(u1235,negated_conjecture,
( ~ product(e_4,e_1,X0)
| equalish(X0,e_3) ) ).
cnf(u1715,axiom,
( ~ group_element(X0)
| product(X0,e_1,e_2)
| product(X0,e_1,e_3)
| product(X0,e_1,e_4)
| product(X0,e_1,e_1)
| product(X0,e_3,e_1)
| product(X0,e_3,e_2)
| product(X0,e_3,e_3)
| product(X0,e_3,e_4) ) ).
cnf(e_1_is_not_e_3,axiom,
~ equalish(e_1,e_3) ).
cnf(u1301,negated_conjecture,
( ~ group_element(X0)
| equalish(X0,e_4)
| product(e_5,X0,e_1)
| product(e_5,X0,e_2)
| product(e_5,X0,e_3)
| product(e_5,X0,e_4) ) ).
cnf(u927,negated_conjecture,
( ~ product(e_2,e_4,X0)
| equalish(X0,e_3) ) ).
cnf(e_2_is_not_e_1,axiom,
~ equalish(e_2,e_1) ).
cnf(u918,negated_conjecture,
( ~ product(X0,e_3,e_2)
| equalish(X0,e_5) ) ).
cnf(u930,negated_conjecture,
product(e_4,e_2,e_5) ).
cnf(u941,negated_conjecture,
( ~ group_element(X0)
| equalish(e_2,X0)
| product(e_4,X0,e_1)
| product(e_4,X0,e_2)
| product(e_4,X0,e_3)
| product(e_4,X0,e_4) ) ).
cnf(u53,negated_conjecture,
( ~ group_element(X0)
| product(X0,e_3,e_3)
| product(X0,e_3,e_4)
| product(X0,e_3,e_2)
| product(X0,e_3,e_1)
| product(e_5,e_5,X0)
| product(e_3,X0,e_1)
| product(e_3,X0,e_2)
| product(e_3,X0,e_3)
| product(e_3,X0,e_4) ) ).
cnf(u418,negated_conjecture,
( ~ product(e_2,e_5,X0)
| equalish(X0,e_2) ) ).
cnf(u1618,axiom,
( ~ group_element(X0)
| product(X1,e_5,e_1)
| product(X1,e_5,e_2)
| product(X1,e_5,e_3)
| product(X1,e_5,e_4)
| ~ group_element(X1)
| product(X0,e_5,e_1)
| product(X0,e_5,e_2)
| product(X0,e_5,e_3)
| product(X0,e_5,e_4)
| equalish(X0,X1) ) ).
cnf(e_5_is_not_e_4,axiom,
~ equalish(e_5,e_4) ).
cnf(u478,negated_conjecture,
( ~ product(e_3,e_5,X0)
| equalish(X0,e_4) ) ).
cnf(u1687,axiom,
( ~ group_element(X0)
| product(X0,e_4,e_2)
| product(X0,e_4,e_3)
| product(X0,e_4,e_4)
| product(X0,e_4,e_1)
| product(X0,e_3,e_1)
| product(X0,e_3,e_2)
| product(X0,e_3,e_3)
| product(X0,e_3,e_4) ) ).
cnf(u654,negated_conjecture,
product(e_3,e_3,e_5) ).
cnf(u1404,negated_conjecture,
( ~ product(e_2,X0,e_4)
| equalish(X0,e_2) ) ).
cnf(u1050,negated_conjecture,
( ~ product(X0,e_4,e_1)
| equalish(X0,e_3) ) ).
cnf(u787,negated_conjecture,
( ~ group_element(X0)
| equalish(e_5,X0)
| product(e_1,X0,e_1)
| product(e_1,X0,e_2)
| product(e_1,X0,e_3)
| product(e_1,X0,e_4) ) ).
cnf(u1051,negated_conjecture,
( ~ product(e_3,X0,e_1)
| equalish(X0,e_4) ) ).
cnf(u32,axiom,
( ~ product(X0,X1,X2)
| equalish(X2,e_5)
| ~ group_element(X1)
| product(X0,X1,e_1)
| product(X0,X1,e_2)
| product(X0,X1,e_3)
| product(X0,X1,e_4)
| ~ group_element(X0) ) ).
cnf(u804,negated_conjecture,
( ~ product(X0,e_2,e_2)
| equalish(X0,e_1) ) ).
cnf(u1209,negated_conjecture,
( ~ product(e_1,e_4,X0)
| equalish(X0,e_4) ) ).
cnf(u700,negated_conjecture,
( ~ product(X0,e_5,e_1)
| equalish(X0,e_4) ) ).
cnf(u799,negated_conjecture,
product(e_1,e_2,e_2) ).
cnf(u833,negated_conjecture,
( ~ group_element(X0)
| equalish(e_1,X0)
| product(e_2,X0,e_1)
| product(e_2,X0,e_2)
| product(e_2,X0,e_3)
| product(e_2,X0,e_4) ) ).
cnf(u790,negated_conjecture,
( ~ group_element(X0)
| product(X0,e_5,e_1)
| product(X0,e_5,e_2)
| product(X0,e_5,e_3)
| product(X0,e_5,e_4)
| equalish(X0,e_1) ) ).
cnf(u915,negated_conjecture,
product(e_2,e_4,e_3) ).
cnf(e_3_is_not_e_1,axiom,
~ equalish(e_3,e_1) ).
cnf(u38,axiom,
( ~ group_element(X2)
| equalish(X0,X1)
| product(X1,X2,e_1)
| product(X1,X2,e_2)
| product(X1,X2,e_3)
| product(X1,X2,e_4)
| ~ group_element(X1)
| product(X0,X2,e_1)
| product(X0,X2,e_2)
| product(X0,X2,e_3)
| product(X0,X2,e_4)
| ~ group_element(X0) ) ).
cnf(u1421,negated_conjecture,
( ~ product(e_4,e_4,X0)
| equalish(X0,e_2) ) ).
cnf(u701,negated_conjecture,
( ~ product(e_4,X0,e_1)
| equalish(X0,e_5) ) ).
cnf(element_1,axiom,
group_element(e_1) ).
cnf(product_left_cancellation,axiom,
( ~ product(X3,X1,X2)
| ~ product(X0,X1,X2)
| equalish(X0,X3) ) ).
cnf(u1735,axiom,
( ~ group_element(X0)
| product(X0,e_3,e_2)
| product(X0,e_3,e_3)
| product(X0,e_3,e_4)
| product(X0,e_3,e_1)
| product(X0,e_2,e_1)
| product(X0,e_2,e_2)
| product(X0,e_2,e_3)
| product(X0,e_2,e_4) ) ).
cnf(u829,negated_conjecture,
( ~ product(e_2,X0,e_5)
| equalish(X0,e_1) ) ).
cnf(u544,negated_conjecture,
( ~ product(X0,e_2,e_1)
| equalish(X0,e_5) ) ).
cnf(u1614,axiom,
( ~ group_element(X0)
| product(X1,e_1,e_1)
| product(X1,e_1,e_2)
| product(X1,e_1,e_3)
| product(X1,e_1,e_4)
| ~ group_element(X1)
| product(X0,e_1,e_1)
| product(X0,e_1,e_2)
| product(X0,e_1,e_3)
| product(X0,e_1,e_4)
| equalish(X0,X1) ) ).
cnf(u1027,negated_conjecture,
( ~ product(X0,e_3,e_4)
| equalish(X0,e_4) ) ).
cnf(u31,negated_conjecture,
( ~ product(X0,X1,X2)
| product(X1,X0,e_1)
| product(X1,X0,e_2)
| product(X1,X0,e_3)
| product(X1,X0,e_4)
| ~ group_element(X1)
| ~ group_element(X0)
| product(X2,e_5,X1) ) ).
cnf(u919,negated_conjecture,
( ~ product(e_5,X0,e_2)
| equalish(X0,e_3) ) ).
cnf(u34,axiom,
( ~ product(X0,X1,e_5)
| equalish(X0,X2)
| ~ group_element(X1)
| product(X2,X1,e_1)
| product(X2,X1,e_2)
| product(X2,X1,e_3)
| product(X2,X1,e_4)
| ~ group_element(X2) ) ).
cnf(u938,negated_conjecture,
( ~ product(e_4,e_2,X0)
| equalish(X0,e_5) ) ).
cnf(u1233,negated_conjecture,
( ~ product(X0,e_1,e_3)
| equalish(X0,e_4) ) ).
cnf(element_5,axiom,
group_element(e_5) ).
cnf(e_1_is_not_e_4,axiom,
~ equalish(e_1,e_4) ).
cnf(u36,negated_conjecture,
( ~ group_element(X1)
| product(X0,X1,e_2)
| product(X0,X1,e_3)
| product(X0,X1,e_4)
| ~ group_element(X0)
| product(X0,X1,e_1)
| product(e_5,e_5,X0)
| product(X1,X0,e_1)
| product(X1,X0,e_2)
| product(X1,X0,e_3)
| product(X1,X0,e_4) ) ).
cnf(u831,negated_conjecture,
( ~ product(e_1,e_2,X0)
| product(X0,e_5,e_2) ) ).
cnf(u416,negated_conjecture,
( ~ product(X0,e_5,e_2)
| equalish(X0,e_2) ) ).
cnf(u664,negated_conjecture,
( ~ product(e_3,e_3,X0)
| product(X0,e_5,e_3) ) ).
cnf(u1521,negated_conjecture,
( ~ product(e_1,X0,e_1)
| equalish(X0,e_1) ) ).
cnf(u546,negated_conjecture,
( ~ product(e_5,e_2,X0)
| equalish(X0,e_1) ) ).
cnf(u782,negated_conjecture,
( ~ product(X0,e_5,e_5)
| equalish(X0,e_1) ) ).
cnf(u1133,negated_conjecture,
( ~ product(X0,e_3,e_1)
| equalish(X0,e_2) ) ).
cnf(u821,negated_conjecture,
( ~ group_element(X0)
| equalish(e_4,X0)
| product(e_5,X0,e_1)
| product(e_5,X0,e_2)
| product(e_5,X0,e_3)
| product(e_5,X0,e_4) ) ).
cnf(u1208,negated_conjecture,
( ~ product(e_1,X0,e_4)
| equalish(X0,e_4) ) ).
cnf(u1202,negated_conjecture,
product(e_1,e_4,e_4) ).
cnf(u1657,axiom,
( ~ group_element(X0)
| product(X0,e_5,e_2)
| product(X0,e_5,e_3)
| product(X0,e_5,e_4)
| product(X0,e_5,e_1)
| product(X0,e_2,e_1)
| product(X0,e_2,e_2)
| product(X0,e_2,e_3)
| product(X0,e_2,e_4) ) ).
cnf(u54,negated_conjecture,
( ~ group_element(X0)
| product(X0,e_4,e_3)
| product(X0,e_4,e_4)
| product(X0,e_4,e_2)
| product(X0,e_4,e_1)
| product(e_5,e_5,X0)
| product(e_4,X0,e_1)
| product(e_4,X0,e_2)
| product(e_4,X0,e_3)
| product(e_4,X0,e_4) ) ).
cnf(u1644,axiom,
( ~ group_element(X0)
| product(X1,e_1,e_1)
| product(X1,e_1,e_2)
| product(X1,e_1,e_3)
| product(X1,e_1,e_4)
| ~ group_element(X1)
| equalish(X0,e_1)
| product(X1,X0,e_1)
| product(X1,X0,e_2)
| product(X1,X0,e_3)
| product(X1,X0,e_4) ) ).
cnf(e_2_is_not_e_4,axiom,
~ equalish(e_2,e_4) ).
cnf(u828,negated_conjecture,
( ~ product(X0,e_1,e_5)
| equalish(X0,e_2) ) ).
cnf(u921,negated_conjecture,
( ~ product(e_3,e_5,X0)
| product(X0,e_2,e_5) ) ).
cnf(e_4_is_not_e_2,axiom,
~ equalish(e_4,e_2) ).
cnf(u663,negated_conjecture,
( ~ product(e_3,e_3,X0)
| equalish(X0,e_5) ) ).
cnf(u1053,negated_conjecture,
( ~ product(e_4,e_3,X0)
| product(X0,e_1,e_3) ) ).
cnf(u1655,axiom,
( ~ group_element(X0)
| product(X0,e_5,e_2)
| product(X0,e_5,e_3)
| product(X0,e_5,e_4)
| product(X0,e_5,e_1)
| product(X0,e_4,e_1)
| product(X0,e_4,e_2)
| product(X0,e_4,e_3)
| product(X0,e_4,e_4) ) ).
cnf(u1244,negated_conjecture,
( ~ product(e_3,e_1,X0)
| equalish(X0,e_2) ) ).
cnf(u1420,negated_conjecture,
( ~ product(e_4,X0,e_2)
| equalish(X0,e_4) ) ).
cnf(u816,negated_conjecture,
( ~ product(X0,e_4,e_5)
| equalish(X0,e_5) ) ).
cnf(e_5_is_not_e_2,axiom,
~ equalish(e_5,e_2) ).
cnf(u644,negated_conjecture,
( ~ product(e_5,X0,e_4)
| equalish(X0,e_1) ) ).
cnf(u52,negated_conjecture,
( ~ group_element(X0)
| product(X0,e_2,e_3)
| product(X0,e_2,e_4)
| product(X0,e_2,e_2)
| product(X0,e_2,e_1)
| product(e_5,e_5,X0)
| product(e_2,X0,e_1)
| product(e_2,X0,e_2)
| product(e_2,X0,e_3)
| product(e_2,X0,e_4) ) ).
cnf(u1236,negated_conjecture,
( ~ product(e_1,e_4,X0)
| product(X0,e_3,e_4) ) ).
cnf(u547,negated_conjecture,
( ~ product(e_2,e_5,X0)
| product(X0,e_1,e_5) ) ).
cnf(product_total_function1,axiom,
( product(X0,X1,e_5)
| ~ group_element(X1)
| product(X0,X1,e_1)
| product(X0,X1,e_2)
| product(X0,X1,e_3)
| product(X0,X1,e_4)
| ~ group_element(X0) ) ).
cnf(u651,negated_conjecture,
equalish(e_3,e_3) ).
cnf(u613,negated_conjecture,
( ~ product(e_5,e_5,X0)
| product(X0,e_3,e_5) ) ).
cnf(u1194,negated_conjecture,
( ~ product(X0,e_3,e_3)
| equalish(X0,e_1) ) ).
cnf(element_4,axiom,
group_element(e_4) ).
cnf(u1195,negated_conjecture,
( ~ product(e_1,X0,e_3)
| equalish(X0,e_3) ) ).
cnf(u820,negated_conjecture,
( ~ group_element(X0)
| product(X0,e_4,e_1)
| product(X0,e_4,e_2)
| product(X0,e_4,e_3)
| product(X0,e_4,e_4)
| equalish(e_5,X0) ) ).
cnf(u1029,negated_conjecture,
( ~ product(e_4,e_3,X0)
| equalish(X0,e_4) ) ).
cnf(e_2_is_not_e_3,axiom,
~ equalish(e_2,e_3) ).
cnf(u1136,negated_conjecture,
( ~ product(e_3,e_2,X0)
| product(X0,e_1,e_2) ) ).
cnf(u1648,axiom,
( ~ group_element(X0)
| product(X1,e_5,e_1)
| product(X1,e_5,e_2)
| product(X1,e_5,e_3)
| product(X1,e_5,e_4)
| ~ group_element(X1)
| equalish(X0,e_5)
| product(X1,X0,e_1)
| product(X1,X0,e_2)
| product(X1,X0,e_3)
| product(X1,X0,e_4) ) ).
cnf(u806,negated_conjecture,
( ~ product(e_1,e_2,X0)
| equalish(X0,e_2) ) ).
cnf(u818,negated_conjecture,
( ~ product(e_5,e_4,X0)
| equalish(X0,e_5) ) ).
cnf(u939,negated_conjecture,
( ~ product(e_2,e_4,X0)
| product(X0,e_5,e_4) ) ).
cnf(u702,negated_conjecture,
( ~ product(e_4,e_5,X0)
| equalish(X0,e_1) ) ).
cnf(element_2,axiom,
group_element(e_2) ).
cnf(qg4,negated_conjecture,
( ~ product(X1,X0,X3)
| ~ product(X0,X1,X2)
| product(X2,X3,X1) ) ).
cnf(u646,negated_conjecture,
( ~ product(e_1,e_5,X0)
| product(X0,e_4,e_5) ) ).
cnf(u925,negated_conjecture,
( ~ product(X0,e_4,e_3)
| equalish(X0,e_2) ) ).
cnf(u937,negated_conjecture,
( ~ product(e_4,X0,e_5)
| equalish(X0,e_2) ) ).
cnf(e_3_is_not_e_5,axiom,
~ equalish(e_3,e_5) ).
cnf(u661,negated_conjecture,
( ~ product(X0,e_3,e_5)
| equalish(X0,e_3) ) ).
cnf(u853,negated_conjecture,
( ~ group_element(X0)
| equalish(X0,e_5)
| product(e_1,X0,e_1)
| product(e_1,X0,e_2)
| product(e_1,X0,e_3)
| product(e_1,X0,e_4) ) ).
cnf(u1128,negated_conjecture,
( ~ product(e_3,X0,e_3)
| equalish(X0,e_2) ) ).
cnf(u1403,negated_conjecture,
( ~ product(X0,e_2,e_4)
| equalish(X0,e_2) ) ).
cnf(u805,negated_conjecture,
( ~ product(e_1,X0,e_2)
| equalish(X0,e_2) ) ).
cnf(u1242,negated_conjecture,
( ~ product(X0,e_1,e_2)
| equalish(X0,e_3) ) ).
cnf(u1414,negated_conjecture,
product(e_4,e_4,e_2) ).
cnf(u808,negated_conjecture,
product(e_5,e_4,e_5) ).
cnf(u692,negated_conjecture,
equalish(e_2,e_2) ).
cnf(u1645,axiom,
( ~ group_element(X0)
| product(X1,e_2,e_1)
| product(X1,e_2,e_2)
| product(X1,e_2,e_3)
| product(X1,e_2,e_4)
| ~ group_element(X1)
| equalish(X0,e_2)
| product(X1,X0,e_1)
| product(X1,X0,e_2)
| product(X1,X0,e_3)
| product(X1,X0,e_4) ) ).
cnf(u1647,axiom,
( ~ group_element(X0)
| product(X1,e_4,e_1)
| product(X1,e_4,e_2)
| product(X1,e_4,e_3)
| product(X1,e_4,e_4)
| ~ group_element(X1)
| equalish(X0,e_4)
| product(X1,X0,e_1)
| product(X1,X0,e_2)
| product(X1,X0,e_3)
| product(X1,X0,e_4) ) ).
cnf(e_1_is_not_e_2,axiom,
~ equalish(e_1,e_2) ).
cnf(u1135,negated_conjecture,
( ~ product(e_2,e_3,X0)
| equalish(X0,e_1) ) ).
cnf(u643,negated_conjecture,
( ~ product(X0,e_1,e_4)
| equalish(X0,e_5) ) ).
cnf(e_4_is_not_e_5,axiom,
~ equalish(e_4,e_5) ).
cnf(u33,axiom,
( ~ product(X0,X1,e_5)
| equalish(X1,X2)
| ~ group_element(X2)
| product(X0,X2,e_1)
| product(X0,X2,e_2)
| product(X0,X2,e_3)
| product(X0,X2,e_4)
| ~ group_element(X0) ) ).
cnf(u920,negated_conjecture,
( ~ product(e_5,e_3,X0)
| equalish(X0,e_2) ) ).
cnf(u709,negated_conjecture,
( ~ group_element(X0)
| product(X0,e_3,e_1)
| product(X0,e_3,e_2)
| product(X0,e_3,e_3)
| product(X0,e_3,e_4)
| equalish(X0,e_3) ) ).
cnf(u1616,axiom,
( ~ group_element(X0)
| product(X1,e_3,e_1)
| product(X1,e_3,e_2)
| product(X1,e_3,e_3)
| product(X1,e_3,e_4)
| ~ group_element(X1)
| product(X0,e_3,e_1)
| product(X0,e_3,e_2)
| product(X0,e_3,e_3)
| product(X0,e_3,e_4)
| equalish(X0,X1) ) ).
cnf(e_5_is_not_e_3,axiom,
~ equalish(e_5,e_3) ).
cnf(u1522,negated_conjecture,
( ~ product(e_1,e_1,X0)
| equalish(X0,e_1) ) ).
cnf(u1129,negated_conjecture,
( ~ product(e_3,e_2,X0)
| equalish(X0,e_3) ) ).
cnf(u784,negated_conjecture,
( ~ product(e_1,e_5,X0)
| equalish(X0,e_5) ) ).
cnf(u668,negated_conjecture,
( ~ group_element(X0)
| equalish(e_3,X0)
| product(e_3,X0,e_1)
| product(e_3,X0,e_2)
| product(e_3,X0,e_3)
| product(e_3,X0,e_4) ) ).
cnf(u1134,negated_conjecture,
( ~ product(e_2,X0,e_1)
| equalish(X0,e_3) ) ).
cnf(u807,negated_conjecture,
( ~ product(e_2,e_1,X0)
| product(X0,e_2,e_1) ) ).
cnf(u1406,negated_conjecture,
( ~ product(e_2,e_2,X0)
| product(X0,e_4,e_2) ) ).
cnf(u703,negated_conjecture,
( ~ product(e_5,e_4,X0)
| product(X0,e_1,e_4) ) ).
cnf(u785,negated_conjecture,
( ~ product(e_5,e_1,X0)
| product(X0,e_5,e_1) ) ).
cnf(u1658,axiom,
( ~ group_element(X0)
| product(X0,e_5,e_2)
| product(X0,e_5,e_3)
| product(X0,e_5,e_4)
| product(X0,e_5,e_1)
| product(X0,e_1,e_1)
| product(X0,e_1,e_2)
| product(X0,e_1,e_3)
| product(X0,e_1,e_4) ) ).
cnf(e_1_is_not_e_5,axiom,
~ equalish(e_1,e_5) ).
cnf(u417,negated_conjecture,
( ~ product(e_2,X0,e_2)
| equalish(X0,e_5) ) ).
cnf(u477,negated_conjecture,
( ~ product(e_3,X0,e_4)
| equalish(X0,e_5) ) ).
cnf(u1617,axiom,
( ~ group_element(X0)
| product(X1,e_4,e_1)
| product(X1,e_4,e_2)
| product(X1,e_4,e_3)
| product(X1,e_4,e_4)
| ~ group_element(X1)
| product(X0,e_4,e_1)
| product(X0,e_4,e_2)
| product(X0,e_4,e_3)
| product(X0,e_4,e_4)
| equalish(X0,X1) ) ).
cnf(product_right_cancellation,axiom,
( ~ product(X0,X3,X2)
| ~ product(X0,X1,X2)
| equalish(X1,X3) ) ).
cnf(u1422,negated_conjecture,
( ~ product(e_4,e_4,X0)
| product(X0,e_2,e_4) ) ).
cnf(u612,negated_conjecture,
( ~ product(e_5,e_5,X0)
| equalish(X0,e_3) ) ).
cnf(u832,negated_conjecture,
( ~ group_element(X0)
| product(X0,e_1,e_1)
| product(X0,e_1,e_2)
| product(X0,e_1,e_3)
| product(X0,e_1,e_4)
| equalish(e_2,X0) ) ).
cnf(u783,negated_conjecture,
( ~ product(e_1,X0,e_5)
| equalish(X0,e_5) ) ).
cnf(u955,negated_conjecture,
( ~ group_element(X0)
| product(X0,e_2,e_1)
| product(X0,e_2,e_2)
| product(X0,e_2,e_3)
| product(X0,e_2,e_4)
| equalish(X0,e_4) ) ).
cnf(u610,negated_conjecture,
( ~ product(X0,e_5,e_3)
| equalish(X0,e_5) ) ).
cnf(u786,negated_conjecture,
( ~ group_element(X0)
| product(X0,e_5,e_1)
| product(X0,e_5,e_2)
| product(X0,e_5,e_3)
| product(X0,e_5,e_4)
| equalish(e_1,X0) ) ).
cnf(u1028,negated_conjecture,
( ~ product(e_4,X0,e_4)
| equalish(X0,e_3) ) ).
cnf(u789,negated_conjecture,
equalish(e_1,e_1) ).
cnf(u1197,negated_conjecture,
( ~ product(e_3,e_1,X0)
| product(X0,e_3,e_1) ) ).
cnf(e_2_is_not_e_5,axiom,
~ equalish(e_2,e_5) ).
cnf(u1127,negated_conjecture,
( ~ product(X0,e_2,e_3)
| equalish(X0,e_3) ) ).
cnf(u926,negated_conjecture,
( ~ product(e_2,X0,e_3)
| equalish(X0,e_4) ) ).
cnf(u1130,negated_conjecture,
( ~ product(e_2,e_3,X0)
| product(X0,e_3,e_3) ) ).
cnf(u848,negated_conjecture,
( ~ group_element(X0)
| product(X0,e_4,e_1)
| product(X0,e_4,e_2)
| product(X0,e_4,e_3)
| product(X0,e_4,e_4)
| equalish(X0,e_5) ) ).
cnf(e_3_is_not_e_4,axiom,
~ equalish(e_3,e_4) ).
cnf(u830,negated_conjecture,
( ~ product(e_2,e_1,X0)
| equalish(X0,e_5) ) ).
cnf(u936,negated_conjecture,
( ~ product(X0,e_2,e_5)
| equalish(X0,e_4) ) ).
cnf(u479,negated_conjecture,
( ~ product(e_5,e_3,X0)
| product(X0,e_4,e_3) ) ).
cnf(u1405,negated_conjecture,
( ~ product(e_2,e_2,X0)
| equalish(X0,e_4) ) ).
cnf(u1311,negated_conjecture,
( ~ group_element(X0)
| equalish(X0,e_2)
| product(e_4,X0,e_1)
| product(e_4,X0,e_2)
| product(e_4,X0,e_3)
| product(e_4,X0,e_4) ) ).
cnf(u1520,negated_conjecture,
( ~ product(X0,e_1,e_1)
| equalish(X0,e_1) ) ).
cnf(u667,negated_conjecture,
( ~ group_element(X0)
| product(X0,e_3,e_1)
| product(X0,e_3,e_2)
| product(X0,e_3,e_3)
| product(X0,e_3,e_4)
| equalish(e_3,X0) ) ).
cnf(u1207,negated_conjecture,
( ~ product(X0,e_4,e_4)
| equalish(X0,e_1) ) ).
cnf(u1245,negated_conjecture,
( ~ product(e_1,e_3,X0)
| product(X0,e_2,e_3) ) ).
cnf(u1308,negated_conjecture,
( ~ group_element(X0)
| equalish(X0,e_1)
| product(e_2,X0,e_1)
| product(e_2,X0,e_2)
| product(e_2,X0,e_3)
| product(e_2,X0,e_4) ) ).
cnf(u1210,negated_conjecture,
( ~ product(e_4,e_1,X0)
| product(X0,e_4,e_1) ) ).
cnf(u1030,negated_conjecture,
( ~ product(e_3,e_4,X0)
| product(X0,e_4,e_4) ) ).
cnf(u1716,axiom,
( ~ group_element(X0)
| product(X0,e_1,e_2)
| product(X0,e_1,e_3)
| product(X0,e_1,e_4)
| product(X0,e_1,e_1)
| product(X0,e_2,e_1)
| product(X0,e_2,e_2)
| product(X0,e_2,e_3)
| product(X0,e_2,e_4) ) ).
cnf(e_4_is_not_e_1,axiom,
~ equalish(e_4,e_1) ).
cnf(e_4_is_not_e_3,axiom,
~ equalish(e_4,e_3) ).
cnf(u1419,negated_conjecture,
( ~ product(X0,e_4,e_2)
| equalish(X0,e_4) ) ).
cnf(u1243,negated_conjecture,
( ~ product(e_3,X0,e_2)
| equalish(X0,e_1) ) ).
cnf(e_3_is_not_e_2,axiom,
~ equalish(e_3,e_2) ).
cnf(product_total_function2,axiom,
( ~ product(X0,X1,X3)
| ~ product(X0,X1,X2)
| equalish(X2,X3) ) ).
cnf(u940,negated_conjecture,
( ~ group_element(X0)
| product(X0,e_2,e_1)
| product(X0,e_2,e_2)
| product(X0,e_2,e_3)
| product(X0,e_2,e_4)
| equalish(e_4,X0) ) ).
cnf(u645,negated_conjecture,
( ~ product(e_5,e_1,X0)
| equalish(X0,e_4) ) ).
cnf(u822,negated_conjecture,
product(e_2,e_1,e_5) ).
cnf(u611,negated_conjecture,
( ~ product(e_5,X0,e_3)
| equalish(X0,e_5) ) ).
cnf(u1615,axiom,
( ~ group_element(X0)
| product(X1,e_2,e_1)
| product(X1,e_2,e_2)
| product(X1,e_2,e_3)
| product(X1,e_2,e_4)
| ~ group_element(X1)
| product(X0,e_2,e_1)
| product(X0,e_2,e_2)
| product(X0,e_2,e_3)
| product(X0,e_2,e_4)
| equalish(X0,X1) ) ).
cnf(u662,negated_conjecture,
( ~ product(e_3,X0,e_5)
| equalish(X0,e_3) ) ).
cnf(u545,negated_conjecture,
( ~ product(e_5,X0,e_1)
| equalish(X0,e_2) ) ).
cnf(u706,negated_conjecture,
equalish(e_4,e_4) ).
cnf(u1196,negated_conjecture,
( ~ product(e_1,e_3,X0)
| equalish(X0,e_3) ) ).
cnf(u1523,negated_conjecture,
( ~ product(e_1,e_1,X0)
| product(X0,e_1,e_1) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP134-1.005 : TPTP v9.3.1. Released v1.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.38 % Computer : n002.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:33:52 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.42 Running first-order theorem proving
% 0.11/0.42 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 8.78/2.06 % (3283406)Input is clausal, will run a generic CNF schedule.
% 8.78/2.06 % (3283415)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1424529952:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 8.78/2.06 % (3283416)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1740955606:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 8.78/2.06 % (3283412)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1645658705:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 8.78/2.06 % (3283411)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=2789094999:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 8.78/2.06 % (3283413)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=982649075:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 8.78/2.06 % (3283417)dis-21_1_sil=8000:lcm=predicate:random_seed=4237518504: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)
% 8.78/2.06 % (3283415)Instruction limit reached!
% 8.78/2.06 % (3283415)------------------------------
% 8.78/2.06 % (3283415)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.78/2.06 % (3283415)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.78/2.06 % (3283415)CaDiCaL version: 2.1.3
% 8.78/2.06 % (3283415)Termination reason: Instruction limit
% 8.78/2.06 % (3283415)Termination phase: Saturation
% 8.78/2.06 % (3283415)Time elapsed: 0.030 s
% 8.78/2.06 % (3283415)Peak memory usage: 88 MB
% 8.78/2.06 % (3283415)Instructions burned: 117 (million)
% 8.78/2.06 % (3283414)lrs+10_1_sil=8000:sp=occurrence:random_seed=946393858:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 8.78/2.06 % (3283414)Instruction limit reached!
% 8.78/2.06 % (3283414)------------------------------
% 8.78/2.06 % (3283414)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.78/2.06 % (3283414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.78/2.06 % (3283414)CaDiCaL version: 2.1.3
% 8.78/2.06 % (3283414)Termination reason: Instruction limit
% 8.78/2.06 % (3283414)Termination phase: Saturation
% 8.78/2.06 % (3283414)Time elapsed: 0.055 s
% 8.78/2.06 % (3283414)Peak memory usage: 88 MB
% 8.78/2.06 % (3283414)Instructions burned: 107 (million)
% 8.78/2.06 % (3283417)Instruction limit reached!
% 8.78/2.06 % (3283417)------------------------------
% 8.78/2.06 % (3283417)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.78/2.06 % (3283417)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.78/2.06 % (3283417)CaDiCaL version: 2.1.3
% 8.78/2.06 % (3283417)Termination reason: Instruction limit
% 8.78/2.06 % (3283417)Termination phase: Saturation
% 8.78/2.06 % (3283417)Time elapsed: 0.075 s
% 8.78/2.06 % (3283417)Peak memory usage: 88 MB
% 8.78/2.06 % (3283417)Instructions burned: 118 (million)
% 8.78/2.06 % (3283425)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=3468149750:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 8.78/2.06 % (3283416)Instruction limit reached!
% 8.78/2.06 % (3283416)------------------------------
% 8.78/2.06 % (3283416)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.78/2.06 % (3283416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.78/2.06 % (3283416)CaDiCaL version: 2.1.3
% 8.78/2.06 % (3283416)Termination reason: Instruction limit
% 8.78/2.06 % (3283416)Termination phase: Saturation
% 8.78/2.06 % (3283416)Time elapsed: 0.106 s
% 8.78/2.06 % (3283416)Peak memory usage: 89 MB
% 8.78/2.06 % (3283416)Instructions burned: 180 (million)
% 8.78/2.06 % (3283425)Instruction limit reached!
% 8.78/2.06 % (3283425)------------------------------
% 8.78/2.06 % (3283425)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.78/2.06 % (3283425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.78/2.06 % (3283425)CaDiCaL version: 2.1.3
% 8.78/2.06 % (3283425)Termination reason: Instruction limit
% 8.78/2.06 % (3283425)Termination phase: Saturation
% 8.78/2.06 % (3283425)Time elapsed: 0.041 s
% 8.78/2.06 % (3283425)Peak memory usage: 88 MB
% 8.78/2.06 % (3283425)Instructions burned: 143 (million)
% 8.78/2.06 % (3283426)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=726594330: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)
% 12.80/2.82 % (3283426)Refutation not found, incomplete strategy
% 12.80/2.82 % (3283426)------------------------------
% 12.80/2.82 % (3283426)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.80/2.82 % (3283426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.80/2.82 % (3283426)CaDiCaL version: 2.1.3
% 12.80/2.82 % (3283426)Termination reason: Refutation not found, incomplete strategy
% 12.80/2.82 % (3283426)Time elapsed: 0.001 s
% 12.80/2.82 % (3283426)Peak memory usage: 87 MB
% 12.80/2.82 % (3283426)Instructions burned: 1 (million)
% 12.80/2.82 % (3283427)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3382988410:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 12.80/2.82 % (3283430)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3410787205:avsq=on:i=194:fgj=on:bd=preordered_2997 on theBenchmark for (2997ds/194Mi)
% 12.80/2.82 % (3283429)lrs+10_64_to=lpo:sil=8000:random_seed=1759805931:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 12.80/2.82 % (3283430)Instruction limit reached!
% 12.80/2.82 % (3283430)------------------------------
% 12.80/2.82 % (3283430)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.80/2.82 % (3283430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.80/2.82 % (3283430)CaDiCaL version: 2.1.3
% 12.80/2.82 % (3283430)Termination reason: Instruction limit
% 12.80/2.82 % (3283430)Termination phase: Saturation
% 12.80/2.82 % (3283430)Time elapsed: 0.038 s
% 12.80/2.82 % (3283430)Peak memory usage: 87 MB
% 12.80/2.82 % (3283430)Instructions burned: 197 (million)
% 12.80/2.82 % (3283427)Instruction limit reached!
% 12.80/2.82 % (3283427)------------------------------
% 12.80/2.82 % (3283427)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.80/2.82 % (3283427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.80/2.82 % (3283427)CaDiCaL version: 2.1.3
% 12.80/2.82 % (3283427)Termination reason: Instruction limit
% 12.80/2.82 % (3283427)Termination phase: Saturation
% 12.80/2.82 % (3283427)Time elapsed: 0.116 s
% 12.80/2.82 % (3283427)Peak memory usage: 88 MB
% 12.80/2.82 % (3283427)Instructions burned: 220 (million)
% 12.80/2.82 % (3283429)Instruction limit reached!
% 12.80/2.82 % (3283429)------------------------------
% 12.80/2.82 % (3283429)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.80/2.82 % (3283429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.80/2.82 % (3283429)CaDiCaL version: 2.1.3
% 12.80/2.82 % (3283429)Termination reason: Instruction limit
% 12.80/2.82 % (3283429)Termination phase: Saturation
% 12.80/2.82 % (3283429)Time elapsed: 0.076 s
% 12.80/2.82 % (3283429)Peak memory usage: 88 MB
% 12.80/2.82 % (3283429)Instructions burned: 127 (million)
% 12.80/2.82 % (3283435)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1287704768:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 12.80/2.82 % (3283435)Instruction limit reached!
% 12.80/2.82 % (3283435)------------------------------
% 12.80/2.82 % (3283435)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.80/2.82 % (3283435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.80/2.82 % (3283435)CaDiCaL version: 2.1.3
% 12.80/2.82 % (3283435)Termination reason: Instruction limit
% 12.80/2.82 % (3283435)Termination phase: Saturation
% 12.80/2.82 % (3283435)Time elapsed: 0.043 s
% 12.80/2.82 % (3283435)Peak memory usage: 88 MB
% 12.80/2.82 % (3283435)Instructions burned: 159 (million)
% 12.80/2.82 % (3283426)------------------------------
% 12.80/2.82 % (3283426)------------------------------
% 12.80/2.82 % (3283436)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3680709308:i=3394:sd=4:ss=included:sgt=64_2995 on theBenchmark for (2995ds/3394Mi)
% 12.80/2.82 % (3283437)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=1996470430:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2995 on theBenchmark for (2995ds/106Mi)
% 12.80/2.82 % (3283437)Refutation not found, incomplete strategy
% 12.80/2.82 % (3283437)------------------------------
% 12.80/2.82 % (3283437)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.80/2.82 % (3283437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.31/3.77 % (3283437)CaDiCaL version: 2.1.3
% 20.31/3.77 % (3283437)Termination reason: Refutation not found, incomplete strategy
% 20.31/3.77 % (3283437)Time elapsed: 0.001 s
% 20.31/3.77 % (3283437)Peak memory usage: 87 MB
% 20.31/3.77 % (3283437)Instructions burned: 1 (million)
% 20.31/3.77 % (3283439)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2259511950:i=107_2994 on theBenchmark for (2994ds/107Mi)
% 20.31/3.77 % (3283439)Instruction limit reached!
% 20.31/3.77 % (3283439)------------------------------
% 20.31/3.77 % (3283439)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.31/3.77 % (3283439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.31/3.77 % (3283439)CaDiCaL version: 2.1.3
% 20.31/3.77 % (3283439)Termination reason: Instruction limit
% 20.31/3.77 % (3283439)Termination phase: Saturation
% 20.31/3.77 % (3283439)Time elapsed: 0.034 s
% 20.31/3.77 % (3283439)Peak memory usage: 88 MB
% 20.31/3.77 % (3283439)Instructions burned: 107 (million)
% 20.31/3.77 % (3283440)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=4087080311:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2994 on theBenchmark for (2994ds/242Mi)
% 20.31/3.77 % (3283412)Refutation not found, incomplete strategy
% 20.31/3.77 % (3283412)------------------------------
% 20.31/3.77 % (3283412)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.31/3.77 % (3283412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.31/3.77 % (3283412)CaDiCaL version: 2.1.3
% 20.31/3.77 % (3283412)Termination reason: Refutation not found, incomplete strategy
% 20.31/3.77 % (3283412)Time elapsed: 0.578 s
% 20.31/3.77 % (3283412)Peak memory usage: 126 MB
% 20.31/3.77 % (3283412)Instructions burned: 863 (million)
% 20.31/3.77 % (3283444)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=1451047657:cond=fast:i=5208:av=off_2993 on theBenchmark for (2993ds/5208Mi)
% 20.31/3.77 % (3283437)------------------------------
% 20.31/3.77 % (3283437)------------------------------
% 20.31/3.77 % (3283440)Instruction limit reached!
% 20.31/3.77 % (3283440)------------------------------
% 20.31/3.77 % (3283440)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.31/3.77 % (3283440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.31/3.77 % (3283440)CaDiCaL version: 2.1.3
% 20.31/3.77 % (3283440)Termination reason: Instruction limit
% 20.31/3.77 % (3283440)Termination phase: Saturation
% 20.31/3.77 % (3283440)Time elapsed: 0.127 s
% 20.31/3.77 % (3283440)Peak memory usage: 88 MB
% 20.31/3.77 % (3283440)Instructions burned: 244 (million)
% 20.31/3.77 % (3283447)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=1965376690:i=134:sd=2:doe=on:ss=axioms:sgt=14_2991 on theBenchmark for (2991ds/134Mi)
% 20.31/3.77 % (3283412)------------------------------
% 20.31/3.77 % (3283412)------------------------------
% 20.31/3.77 % (3283448)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=2001540644:i=499:bd=all_2991 on theBenchmark for (2991ds/499Mi)
% 20.31/3.77 % (3283447)Instruction limit reached!
% 20.31/3.77 % (3283447)------------------------------
% 20.31/3.77 % (3283447)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.31/3.77 % (3283447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.31/3.77 % (3283447)CaDiCaL version: 2.1.3
% 20.31/3.77 % (3283447)Termination reason: Instruction limit
% 20.31/3.77 % (3283447)Termination phase: Saturation
% 20.31/3.77 % (3283447)Time elapsed: 0.051 s
% 20.31/3.77 % (3283447)Peak memory usage: 87 MB
% 20.31/3.77 % (3283447)Instructions burned: 135 (million)
% 20.31/3.77 % (3283451)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=2380892127:i=191:fgj=on:bd=all_2990 on theBenchmark for (2990ds/191Mi)
% 20.31/3.77 % (3283452)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=4059179661:i=264:kws=precedence:fsr=off_2989 on theBenchmark for (2989ds/264Mi)
% 20.31/3.77 % (3283448)Instruction limit reached!
% 20.31/3.77 % (3283448)------------------------------
% 20.31/3.77 % (3283448)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.31/3.77 % (3283448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.31/3.77 % (3283448)CaDiCaL version: 2.1.3
% 20.31/3.77 % (3283448)Termination reason: Instruction limit
% 30.96/5.27 % (3283448)Termination phase: Saturation
% 30.96/5.27 % (3283448)Time elapsed: 0.246 s
% 30.96/5.27 % (3283448)Peak memory usage: 88 MB
% 30.96/5.27 % (3283448)Instructions burned: 501 (million)
% 30.96/5.27 % (3283451)Instruction limit reached!
% 30.96/5.27 % (3283451)------------------------------
% 30.96/5.27 % (3283451)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.96/5.27 % (3283451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.96/5.27 % (3283451)CaDiCaL version: 2.1.3
% 30.96/5.27 % (3283451)Termination reason: Instruction limit
% 30.96/5.27 % (3283451)Termination phase: Saturation
% 30.96/5.27 % (3283451)Time elapsed: 0.107 s
% 30.96/5.27 % (3283451)Peak memory usage: 88 MB
% 30.96/5.27 % (3283451)Instructions burned: 191 (million)
% 30.96/5.27 % (3283452)Instruction limit reached!
% 30.96/5.27 % (3283452)------------------------------
% 30.96/5.27 % (3283452)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.96/5.27 % (3283452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.96/5.27 % (3283452)CaDiCaL version: 2.1.3
% 30.96/5.27 % (3283452)Termination reason: Instruction limit
% 30.96/5.27 % (3283452)Termination phase: Saturation
% 30.96/5.27 % (3283452)Time elapsed: 0.161 s
% 30.96/5.27 % (3283452)Peak memory usage: 89 MB
% 30.96/5.27 % (3283452)Instructions burned: 266 (million)
% 30.96/5.27 % (3283455)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=3612144547:cond=on:i=156:bs=on:gtg=exists_all:er=known_2987 on theBenchmark for (2987ds/156Mi)
% 30.96/5.27 % (3283456)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=2305137234:i=3256:kws=precedence:bd=preordered:av=off_2987 on theBenchmark for (2987ds/3256Mi)
% 30.96/5.27 % (3283457)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=1859999156:i=537:av=off:ss=included_2986 on theBenchmark for (2986ds/537Mi)
% 30.96/5.27 % (3283455)Instruction limit reached!
% 30.96/5.27 % (3283455)------------------------------
% 30.96/5.27 % (3283455)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.96/5.27 % (3283455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.96/5.27 % (3283455)CaDiCaL version: 2.1.3
% 30.96/5.27 % (3283455)Termination reason: Instruction limit
% 30.96/5.27 % (3283455)Termination phase: Saturation
% 30.96/5.27 % (3283455)Time elapsed: 0.088 s
% 30.96/5.27 % (3283455)Peak memory usage: 88 MB
% 30.96/5.27 % (3283455)Instructions burned: 157 (million)
% 30.96/5.27 % (3283461)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=125635620:i=180:bd=preordered:av=off_2985 on theBenchmark for (2985ds/180Mi)
% 30.96/5.27 % (3283457)Instruction limit reached!
% 30.96/5.27 % (3283457)------------------------------
% 30.96/5.27 % (3283457)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.96/5.27 % (3283457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.96/5.27 % (3283457)CaDiCaL version: 2.1.3
% 30.96/5.27 % (3283457)Termination reason: Instruction limit
% 30.96/5.27 % (3283457)Termination phase: Saturation
% 30.96/5.27 % (3283457)Time elapsed: 0.198 s
% 30.96/5.27 % (3283457)Peak memory usage: 88 MB
% 30.96/5.27 % (3283457)Instructions burned: 538 (million)
% 30.96/5.27 % (3283461)Instruction limit reached!
% 30.96/5.27 % (3283461)------------------------------
% 30.96/5.27 % (3283461)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.96/5.27 % (3283461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.96/5.27 % (3283461)CaDiCaL version: 2.1.3
% 30.96/5.27 % (3283461)Termination reason: Instruction limit
% 30.96/5.27 % (3283461)Termination phase: Saturation
% 30.96/5.27 % (3283461)Time elapsed: 0.090 s
% 30.96/5.27 % (3283461)Peak memory usage: 87 MB
% 30.96/5.27 % (3283461)Instructions burned: 181 (million)
% 30.96/5.27 % (3283463)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:sas=cadical:sp=reverse_frequency:bsr=on:alpa=false:sac=on:random_seed=1567340305:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2983 on theBenchmark for (2983ds/10307Mi)
% 30.96/5.27 % (3283464)lrs-1010_1024_to=lpo:sil=8000:tgt=ground:plsq=on:plsqc=1:sas=cadical:plsqr=1,32:sp=arity:lma=off:spb=goal:acc=on:bce=on:nwc=1.2:alpa=false:random_seed=618230578:i=412:gtgl=4:gtg=exists_all_2983 on theBenchmark for (2983ds/412Mi)
% 30.96/5.27 % (3283464)Instruction limit reached!
% 30.96/5.27 % (3283464)------------------------------
% 30.96/5.27 % (3283464)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.23/6.27 % (3283464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.23/6.27 % (3283464)CaDiCaL version: 2.1.3
% 38.23/6.27 % (3283464)Termination reason: Instruction limit
% 38.23/6.27 % (3283464)Termination phase: Saturation
% 38.23/6.27 % (3283464)Time elapsed: 0.209 s
% 38.23/6.27 % (3283464)Peak memory usage: 89 MB
% 38.23/6.27 % (3283464)Instructions burned: 414 (million)
% 38.23/6.27 % (3283436)Instruction limit reached!
% 38.23/6.27 % (3283436)------------------------------
% 38.23/6.27 % (3283436)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.23/6.27 % (3283436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.23/6.27 % (3283436)CaDiCaL version: 2.1.3
% 38.23/6.27 % (3283436)Termination reason: Instruction limit
% 38.23/6.27 % (3283436)Termination phase: Saturation
% 38.23/6.27 % (3283436)Time elapsed: 1.394 s
% 38.23/6.27 % (3283436)Peak memory usage: 138 MB
% 38.23/6.27 % (3283436)Instructions burned: 3395 (million)
% 38.23/6.27 % (3283468)ott-1011_2_sil=32000:bsd=on:sp=reverse_frequency:erd=off:urr=on:rnwc=on:gs=on:s2agt=70:updr=off:lftc=20:random_seed=3409739256:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2980 on theBenchmark for (2980ds/303Mi)
% 38.23/6.27 % (3283467)ott+1002_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:etr=on:spb=units:urr=on:bsr=unit_only:gs=on:s2agt=16:br=off:random_seed=2155864373:s2pl=no:i=8478:s2at=4:nm=6_2980 on theBenchmark for (2980ds/8478Mi)
% 38.23/6.27 % (3283468)Instruction limit reached!
% 38.23/6.27 % (3283468)------------------------------
% 38.23/6.27 % (3283468)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.23/6.27 % (3283468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.23/6.27 % (3283468)CaDiCaL version: 2.1.3
% 38.23/6.27 % (3283468)Termination reason: Instruction limit
% 38.23/6.27 % (3283468)Termination phase: Saturation
% 38.23/6.27 % (3283468)Time elapsed: 0.096 s
% 38.23/6.27 % (3283468)Peak memory usage: 90 MB
% 38.23/6.27 % (3283468)Instructions burned: 303 (million)
% 38.23/6.27 % (3283471)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=160339939:st=4:i=720:sd=3:fsr=off:ss=axioms_2978 on theBenchmark for (2978ds/720Mi)
% 38.23/6.27 % (3283471)Refutation not found, incomplete strategy
% 38.23/6.27 % (3283471)------------------------------
% 38.23/6.27 % (3283471)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.23/6.27 % (3283471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.23/6.27 % (3283471)CaDiCaL version: 2.1.3
% 38.23/6.27 % (3283471)Termination reason: Refutation not found, incomplete strategy
% 38.23/6.27 % (3283471)Time elapsed: 0.001 s
% 38.23/6.27 % (3283471)Peak memory usage: 87 MB
% 38.23/6.27 % (3283471)Instructions burned: 1 (million)
% 38.23/6.27 % (3283471)------------------------------
% 38.23/6.27 % (3283471)------------------------------
% 38.23/6.27 % (3283473)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=285763836:i=598:bs=on:bd=preordered:av=off:ss=axioms_2976 on theBenchmark for (2976ds/598Mi)
% 38.23/6.27 % (3283473)Instruction limit reached!
% 38.23/6.27 % (3283473)------------------------------
% 38.23/6.27 % (3283473)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.23/6.27 % (3283473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.23/6.27 % (3283473)CaDiCaL version: 2.1.3
% 38.23/6.27 % (3283473)Termination reason: Instruction limit
% 38.23/6.27 % (3283473)Termination phase: Saturation
% 38.23/6.27 % (3283473)Time elapsed: 0.150 s
% 38.23/6.27 % (3283473)Peak memory usage: 88 MB
% 38.23/6.27 % (3283473)Instructions burned: 598 (million)
% 38.23/6.27 % (3283467)Refutation not found, incomplete strategy
% 38.23/6.27 % (3283467)------------------------------
% 38.23/6.27 % (3283467)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.23/6.27 % (3283467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.23/6.27 % (3283467)CaDiCaL version: 2.1.3
% 38.23/6.27 % (3283467)Termination reason: Refutation not found, incomplete strategy
% 38.23/6.27 % (3283467)Time elapsed: 0.576 s
% 38.23/6.27 % (3283467)Peak memory usage: 128 MB
% 38.23/6.27 % (3283467)Instructions burned: 862 (million)
% 38.23/6.27 % (3283475)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=1438071878:i=2989:sd=3:ss=axioms:sgt=60_2973 on theBenchmark for (2973ds/2989Mi)
% 38.23/6.27 % (3283467)------------------------------
% 38.23/6.27 % (3283467)------------------------------
% 38.23/6.27 % (3283477)dis+1011_1_ncem=casc2026/models/loop5.pt:sil=8000:tgt=full:npcc=on:bsd=on:sp=const_min:spb=goal_then_units:lcm=predicate:urr=ec_only:s2agt=16:random_seed=479992841:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2970 on theBenchmark for (2970ds/1997Mi)
% 38.23/6.27 % (3283456)Instruction limit reached!
% 38.23/6.27 % (3283456)------------------------------
% 38.23/6.27 % (3283456)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.23/6.27 % (3283456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.23/6.27 % (3283456)CaDiCaL version: 2.1.3
% 38.23/6.27 % (3283456)Termination reason: Instruction limit
% 38.23/6.27 % (3283456)Termination phase: Saturation
% 38.23/6.27 % (3283456)Time elapsed: 1.911 s
% 38.23/6.27 % (3283456)Peak memory usage: 133 MB
% 38.23/6.27 % (3283456)Instructions burned: 3256 (million)
% 38.23/6.27 % (3283444)Instruction limit reached!
% 38.23/6.27 % (3283444)------------------------------
% 38.23/6.27 % (3283444)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.23/6.27 % (3283444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.23/6.27 % (3283444)CaDiCaL version: 2.1.3
% 38.23/6.27 % (3283444)Termination reason: Instruction limit
% 38.23/6.27 % (3283444)Termination phase: Saturation
% 38.23/6.27 % (3283444)Time elapsed: 2.538 s
% 38.23/6.27 % (3283444)Peak memory usage: 134 MB
% 38.23/6.27 % (3283444)Instructions burned: 5209 (million)
% 38.23/6.27 % (3283479)lrs-1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:drc=off:sp=unary_frequency:urr=ec_only:fd=preordered:random_seed=2040909282:i=2088:bd=preordered:av=off_2967 on theBenchmark for (2967ds/2088Mi)
% 38.23/6.27 % (3283480)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=484311705:i=1098:nicw=on_2966 on theBenchmark for (2966ds/1098Mi)
% 38.23/6.27 % (3283475)Instruction limit reached!
% 38.23/6.27 % (3283475)------------------------------
% 38.23/6.27 % (3283475)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.23/6.27 % (3283475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.23/6.27 % (3283475)CaDiCaL version: 2.1.3
% 38.23/6.27 % (3283475)Termination reason: Instruction limit
% 38.23/6.27 % (3283475)Termination phase: Saturation
% 38.23/6.27 % (3283475)Time elapsed: 1.120 s
% 38.23/6.27 % (3283475)Peak memory usage: 142 MB
% 38.23/6.27 % (3283475)Instructions burned: 2990 (million)
% 38.23/6.27 % (3283483)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=952797351:i=433:bd=preordered_2961 on theBenchmark for (2961ds/433Mi)
% 38.23/6.27 % (3283480)Instruction limit reached!
% 38.23/6.27 % (3283480)------------------------------
% 38.23/6.27 % (3283480)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.23/6.27 % (3283480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.23/6.27 % (3283480)CaDiCaL version: 2.1.3
% 38.23/6.27 % (3283480)Termination reason: Instruction limit
% 38.23/6.27 % (3283480)Termination phase: Saturation
% 38.23/6.27 % (3283480)Time elapsed: 0.541 s
% 38.23/6.27 % (3283480)Peak memory usage: 90 MB
% 38.23/6.27 % (3283480)Instructions burned: 1099 (million)
% 38.23/6.27 % (3283483)Refutation not found, incomplete strategy
% 38.23/6.27 % (3283483)------------------------------
% 38.23/6.27 % (3283483)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.23/6.27 % (3283483)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.23/6.27 % (3283483)CaDiCaL version: 2.1.3
% 38.23/6.27 % (3283483)Termination reason: Refutation not found, incomplete strategy
% 38.23/6.27 % (3283483)Time elapsed: 0.055 s
% 38.23/6.27 % (3283483)Peak memory usage: 89 MB
% 38.23/6.27 % (3283483)Instructions burned: 171 (million)
% 38.23/6.27 % (3283485)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=573184766:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2960 on theBenchmark for (2960ds/2942Mi)
% 38.23/6.27 % (3283483)------------------------------
% 38.23/6.27 % (3283483)------------------------------
% 38.23/6.27 % (3283487)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=2242455596:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2958 on theBenchmark for (2958ds/6922Mi)
% 38.23/6.27 % (3283477)Instruction limit reached!
% 38.23/6.27 % (3283477)------------------------------
% 38.23/6.27 % (3283477)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.23/6.27 % (3283477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.23/6.27 % (3283477)CaDiCaL version: 2.1.3
% 38.23/6.27 % (3283477)Termination reason: Instruction limit
% 38.23/6.27 % (3283477)Termination phase: Saturation
% 38.23/6.27 % (3283477)Time elapsed: 1.357 s
% 38.23/6.27 % (3283477)Peak memory usage: 133 MB
% 38.23/6.27 % (3283477)Instructions burned: 1998 (million)
% 38.23/6.27 % (3283489)dis+10_5:1_sil=8000:tgt=full:plsq=on:plsqc=1:plsqr=32,1:urr=on:fd=off:nwc=0.5:br=off:slsqc=3:slsq=on:random_seed=1962680398:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2955 on theBenchmark for (2955ds/596Mi)
% 38.23/6.27 % (3283489)Refutation not found, incomplete strategy
% 38.23/6.27 % (3283489)------------------------------
% 38.23/6.27 % (3283489)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.23/6.27 % (3283489)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.23/6.27 % (3283489)CaDiCaL version: 2.1.3
% 38.23/6.27 % (3283489)Termination reason: Refutation not found, incomplete strategy
% 38.23/6.27 % (3283489)Time elapsed: 0.002 s
% 38.23/6.27 % (3283489)Peak memory usage: 88 MB
% 38.23/6.27 % (3283489)Instructions burned: 1 (million)
% 38.23/6.27 % (3283487)Refutation not found, incomplete strategy
% 38.23/6.27 % (3283487)------------------------------
% 38.23/6.27 % (3283487)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.23/6.27 % (3283487)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.23/6.27 % (3283487)CaDiCaL version: 2.1.3
% 38.23/6.27 % (3283487)Termination reason: Refutation not found, incomplete strategy
% 38.23/6.27 % (3283487)Time elapsed: 0.326 s
% 38.23/6.27 % (3283487)Peak memory usage: 127 MB
% 38.23/6.27 % (3283487)Instructions burned: 862 (million)
% 38.23/6.27 % (3283479)Instruction limit reached!
% 38.23/6.27 % (3283479)------------------------------
% 38.23/6.27 % (3283479)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.23/6.27 % (3283479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.23/6.27 % (3283479)CaDiCaL version: 2.1.3
% 38.23/6.27 % (3283479)Termination reason: Instruction limit
% 38.23/6.27 % (3283479)Termination phase: Saturation
% 38.23/6.27 % (3283479)Time elapsed: 1.306 s
% 38.23/6.27 % (3283479)Peak memory usage: 132 MB
% 38.23/6.27 % (3283479)Instructions burned: 2090 (million)
% 38.23/6.27 % (3283487)------------------------------
% 38.23/6.27 % (3283487)------------------------------
% 38.23/6.27 % (3283489)------------------------------
% 38.23/6.27 % (3283489)------------------------------
% 38.23/6.27 % (3283492)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=1559059989:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2952 on theBenchmark for (2952ds/16411Mi)
% 38.23/6.27 % (3283491)lrs+21_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=non_intro:urr=on:fd=preordered:random_seed=1019205704:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2953 on theBenchmark for (2953ds/4123Mi)
% 38.23/6.27 % (3283494)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=3106958545:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2951 on theBenchmark for (2951ds/1670Mi)
% 38.23/6.27 % (3283492)First to succeed.
% 38.23/6.27 % (3283492)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3283406"
% 38.23/6.27 % SZS status Satisfiable for theBenchmark
% 38.23/6.27 % SZS output start Saturation.
% See solution above
% 38.78/6.37 % SZS output start Definitions and Model Updates.
% 38.78/6.37 % SZS output end Definitions and Model Updates.
% 38.78/6.37 % (3283492)------------------------------
% 38.78/6.37 % (3283492)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 38.78/6.37 % (3283492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 38.78/6.37 % (3283492)CaDiCaL version: 2.1.3
% 38.78/6.37 % (3283492)Termination reason: Satisfiable
% 38.78/6.37 % (3283492)Time elapsed: 0.434 s
% 38.78/6.37 % (3283492)Peak memory usage: 129 MB
% 38.78/6.37 % (3283492)Instructions burned: 1103 (million)
% 38.78/6.37 % (3283492)------------------------------
% 38.78/6.37 % (3283492)------------------------------
% 38.78/6.37 % (3283406)Success in time 5.415 s
% 38.78/6.37 % Vampire exiting
%------------------------------------------------------------------------------