%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP132-2.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 : n012.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:02 AM UTC 2026
% Result : Satisfiable 35.52s 7.51s
% Output : Saturation 44.81s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u68,axiom,
equalish(e_5,e_5) ).
cnf(u81,axiom,
product(e_4,e_1,e_4) ).
cnf(u84,axiom,
~ product(e_4,e_1,e_3) ).
cnf(u88,axiom,
~ product(e_4,e_1,e_2) ).
cnf(u92,axiom,
~ product(e_4,e_1,e_1) ).
cnf(u97,axiom,
~ greater(e_5,e_5) ).
cnf(u104,axiom,
~ product(e_1,e_1,e_4) ).
cnf(u108,axiom,
~ product(e_1,e_1,e_3) ).
cnf(u112,axiom,
~ product(e_1,e_1,e_2) ).
cnf(u117,axiom,
product(e_1,e_1,e_1) ).
cnf(u137,negated_conjecture,
~ product(e_1,e_4,e_4) ).
cnf(u141,negated_conjecture,
~ product(e_1,e_4,e_3) ).
cnf(u145,negated_conjecture,
~ product(e_1,e_4,e_2) ).
cnf(u149,negated_conjecture,
~ product(e_1,e_4,e_1) ).
cnf(u173,negated_conjecture,
~ product(e_1,e_3,e_4) ).
cnf(u177,negated_conjecture,
~ product(e_1,e_3,e_3) ).
cnf(u182,negated_conjecture,
product(e_1,e_3,e_2) ).
cnf(u185,negated_conjecture,
~ product(e_1,e_3,e_1) ).
cnf(u189,negated_conjecture,
( ~ product(X0,X1,e_5)
| equalish(X1,e_3)
| ~ product(e_1,X0,X1) ) ).
cnf(u209,negated_conjecture,
~ product(e_1,e_2,e_4) ).
cnf(u214,negated_conjecture,
product(e_1,e_2,e_3) ).
cnf(u217,negated_conjecture,
~ product(e_1,e_2,e_2) ).
cnf(u221,negated_conjecture,
~ product(e_1,e_2,e_1) ).
cnf(u253,axiom,
~ product(e_3,e_1,e_4) ).
cnf(u258,axiom,
product(e_3,e_1,e_3) ).
cnf(u261,axiom,
~ product(e_3,e_1,e_2) ).
cnf(u265,axiom,
~ product(e_3,e_1,e_1) ).
cnf(u308,negated_conjecture,
~ product(e_4,e_4,e_4) ).
cnf(u312,negated_conjecture,
~ product(e_4,e_4,e_3) ).
cnf(u316,negated_conjecture,
~ product(e_4,e_4,e_2) ).
cnf(u321,negated_conjecture,
product(e_4,e_4,e_1) ).
cnf(u340,negated_conjecture,
~ product(e_4,e_3,e_4) ).
cnf(u345,negated_conjecture,
product(e_4,e_3,e_3) ).
cnf(u348,negated_conjecture,
~ product(e_4,e_3,e_2) ).
cnf(u352,negated_conjecture,
~ product(e_4,e_3,e_1) ).
cnf(u372,negated_conjecture,
~ product(e_4,e_2,e_4) ).
cnf(u376,negated_conjecture,
~ product(e_4,e_2,e_3) ).
cnf(u380,negated_conjecture,
~ product(e_4,e_2,e_2) ).
cnf(u384,negated_conjecture,
~ product(e_4,e_2,e_1) ).
cnf(u442,negated_conjecture,
~ product(e_3,e_4,e_4) ).
cnf(u446,negated_conjecture,
~ product(e_3,e_4,e_3) ).
cnf(u451,negated_conjecture,
product(e_3,e_4,e_2) ).
cnf(u454,negated_conjecture,
~ product(e_3,e_4,e_1) ).
cnf(u486,negated_conjecture,
product(e_3,e_2,e_4) ).
cnf(u489,negated_conjecture,
~ product(e_3,e_2,e_3) ).
cnf(u493,negated_conjecture,
~ product(e_3,e_2,e_2) ).
cnf(u497,negated_conjecture,
~ product(e_3,e_2,e_1) ).
cnf(u676,negated_conjecture,
~ product(e_2,e_3,e_4) ).
cnf(u680,negated_conjecture,
~ product(e_2,e_3,e_3) ).
cnf(u684,negated_conjecture,
~ product(e_2,e_3,e_2) ).
cnf(u688,negated_conjecture,
~ product(e_2,e_3,e_1) ).
cnf(u707,negated_conjecture,
product(e_1,e_5,e_4) ).
cnf(u710,negated_conjecture,
~ product(e_1,e_5,e_3) ).
cnf(u714,negated_conjecture,
~ product(e_1,e_5,e_2) ).
cnf(u718,negated_conjecture,
~ product(e_1,e_5,e_1) ).
cnf(u723,negated_conjecture,
product(e_5,e_5,e_1) ).
cnf(u726,negated_conjecture,
~ product(e_5,e_5,e_4) ).
cnf(u730,negated_conjecture,
~ product(e_5,e_5,e_3) ).
cnf(u734,negated_conjecture,
~ product(e_5,e_5,e_2) ).
cnf(u743,negated_conjecture,
~ product(e_4,e_5,e_1) ).
cnf(u747,negated_conjecture,
~ product(e_4,e_5,e_4) ).
cnf(u751,negated_conjecture,
~ product(e_4,e_5,e_3) ).
cnf(u756,negated_conjecture,
product(e_4,e_5,e_2) ).
cnf(u831,negated_conjecture,
product(e_2,e_4,e_4) ).
cnf(u834,negated_conjecture,
~ product(e_2,e_4,e_3) ).
cnf(u838,negated_conjecture,
~ product(e_2,e_4,e_2) ).
cnf(u842,negated_conjecture,
~ product(e_2,e_4,e_1) ).
cnf(u846,negated_conjecture,
( ~ product(X0,X1,e_5)
| equalish(X1,e_4)
| ~ product(e_4,X0,X1) ) ).
cnf(u1068,negated_conjecture,
~ product(e_2,e_5,e_4) ).
cnf(u1073,negated_conjecture,
product(e_2,e_5,e_3) ).
cnf(u1076,negated_conjecture,
~ product(e_2,e_5,e_2) ).
cnf(u1080,negated_conjecture,
~ product(e_2,e_5,e_1) ).
cnf(u1086,negated_conjecture,
~ product(e_2,e_2,e_4) ).
cnf(u1090,negated_conjecture,
~ product(e_2,e_2,e_3) ).
cnf(u1094,negated_conjecture,
~ product(e_2,e_2,e_2) ).
cnf(u1099,negated_conjecture,
product(e_2,e_2,e_1) ).
cnf(u1103,negated_conjecture,
~ product(e_2,e_1,e_4) ).
cnf(u1107,negated_conjecture,
~ product(e_2,e_1,e_3) ).
cnf(u1112,negated_conjecture,
product(e_2,e_1,e_2) ).
cnf(u1115,negated_conjecture,
~ product(e_2,e_1,e_1) ).
cnf(u1158,negated_conjecture,
~ product(e_5,e_4,e_4) ).
cnf(u1163,negated_conjecture,
product(e_5,e_4,e_3) ).
cnf(u1166,negated_conjecture,
~ product(e_5,e_4,e_2) ).
cnf(u1170,negated_conjecture,
~ product(e_5,e_4,e_1) ).
cnf(u1175,negated_conjecture,
equalish(e_4,e_4) ).
cnf(u1180,negated_conjecture,
~ product(e_3,e_5,e_1) ).
cnf(u1184,negated_conjecture,
~ product(e_3,e_5,e_4) ).
cnf(u1188,negated_conjecture,
~ product(e_3,e_5,e_3) ).
cnf(u1192,negated_conjecture,
~ product(e_3,e_5,e_2) ).
cnf(u1198,negated_conjecture,
( ~ product(X0,X1,e_5)
| equalish(X0,e_2)
| ~ product(e_1,X0,X1) ) ).
cnf(u1241,negated_conjecture,
product(e_5,e_3,e_4) ).
cnf(u1244,negated_conjecture,
~ product(e_5,e_3,e_3) ).
cnf(u1248,negated_conjecture,
~ product(e_5,e_3,e_2) ).
cnf(u1252,negated_conjecture,
~ product(e_5,e_3,e_1) ).
cnf(u1458,negated_conjecture,
~ product(e_5,e_1,e_4) ).
cnf(u1462,negated_conjecture,
~ product(e_5,e_1,e_3) ).
cnf(u1466,negated_conjecture,
~ product(e_5,e_1,e_2) ).
cnf(u1470,negated_conjecture,
~ product(e_5,e_1,e_1) ).
cnf(u1817,negated_conjecture,
~ product(e_5,e_2,e_4) ).
cnf(u1821,negated_conjecture,
~ product(e_5,e_2,e_3) ).
cnf(u1826,negated_conjecture,
product(e_5,e_2,e_2) ).
cnf(u1829,negated_conjecture,
~ product(e_5,e_2,e_1) ).
cnf(u2655,negated_conjecture,
( ~ product(X0,X1,e_5)
| equalish(X0,e_5)
| ~ product(e_5,X0,X1) ) ).
cnf(u2730,negated_conjecture,
~ product(e_3,e_3,e_3) ).
cnf(u2734,negated_conjecture,
~ product(e_3,e_3,e_2) ).
cnf(u2739,negated_conjecture,
product(e_3,e_3,e_1) ).
cnf(u2813,negated_conjecture,
~ product(e_3,e_3,e_4) ).
cnf(u25575,negated_conjecture,
( ~ product(X0,X1,e_5)
| equalish(X1,e_1)
| ~ product(e_5,X0,X1) ) ).
cnf(u44178,negated_conjecture,
( ~ group_element(X0)
| ~ product(X1,X2,e_3)
| equalish(X1,e_2)
| product(X0,e_2,e_1)
| product(X0,e_2,e_2)
| product(X0,e_2,e_3)
| product(X0,e_2,e_4)
| ~ product(X0,X1,X2) ) ).
cnf(u47977,negated_conjecture,
( ~ product(e_5,X0,e_2)
| equalish(X0,e_2) ) ).
cnf(u44172,negated_conjecture,
( ~ product(e_5,e_3,X0)
| ~ product(e_2,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X1,e_5) ) ).
cnf(e_4_is_not_e_1,axiom,
~ equalish(e_4,e_1) ).
cnf(u47358,negated_conjecture,
( ~ product(e_1,X0,X1)
| ~ product(X0,X1,e_1)
| equalish(X0,e_1) ) ).
cnf(u48457,negated_conjecture,
( ~ product(X0,e_5,e_2)
| ~ group_element(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(u47175,negated_conjecture,
( ~ product(X1,X2,e_4)
| ~ product(X0,X1,X2)
| equalish(X2,e_5)
| product(X0,e_1,e_1)
| product(X0,e_1,e_2)
| product(X0,e_1,e_3)
| product(X0,e_1,e_4)
| ~ group_element(X0) ) ).
cnf(u47135,axiom,
( ~ product(X0,e_1,e_3)
| equalish(X0,e_3) ) ).
cnf(u48163,negated_conjecture,
( ~ product(e_3,X0,X1)
| ~ product(X0,X1,e_3)
| equalish(X1,e_1) ) ).
cnf(e_5_is_not_e_2,axiom,
~ equalish(e_5,e_2) ).
cnf(u48439,negated_conjecture,
( ~ product(X0,e_5,e_3)
| equalish(X0,e_5)
| ~ group_element(X0)
| product(e_1,X0,e_1)
| product(e_1,X0,e_2)
| product(e_1,X0,e_3) ) ).
cnf(u47976,negated_conjecture,
( ~ product(e_5,e_2,X0)
| equalish(X0,e_2) ) ).
cnf(u48546,negated_conjecture,
( ~ 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)
| ~ group_element(X0)
| ~ product(X0,e_1,X1)
| product(e_1,X1,e_1)
| product(e_1,X1,e_2)
| product(e_1,X1,e_3)
| product(e_1,X1,e_4) ) ).
cnf(u47626,negated_conjecture,
~ product(e_3,e_1,e_5) ).
cnf(u47341,negated_conjecture,
( ~ product(e_3,X0,X1)
| ~ product(X0,X1,e_2)
| equalish(X1,e_3) ) ).
cnf(u47727,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(u48162,negated_conjecture,
( ~ group_element(X0)
| equalish(X0,e_1)
| ~ group_element(X1)
| product(X0,X1,e_1)
| product(X0,X1,e_2)
| product(X0,X1,e_3)
| product(X0,X1,e_4)
| ~ product(e_4,X0,X1) ) ).
cnf(e_5_is_not_e_3,axiom,
~ equalish(e_5,e_3) ).
cnf(u47173,negated_conjecture,
~ product(e_1,e_1,e_5) ).
cnf(u48722,negated_conjecture,
( ~ product(e_3,e_1,X0)
| ~ group_element(X0)
| product(e_1,X0,e_1)
| product(e_1,X0,e_2)
| product(e_1,X0,e_4)
| equalish(X0,e_2) ) ).
cnf(u47955,negated_conjecture,
( ~ product(X0,e_4,e_4)
| product(X0,e_5,e_1)
| product(X0,e_5,e_2)
| product(X0,e_5,e_3)
| ~ group_element(X0) ) ).
cnf(u48036,negated_conjecture,
( ~ product(e_2,X0,e_1)
| equalish(X0,e_2) ) ).
cnf(u32507,negated_conjecture,
( ~ product(X0,e_5,e_1)
| equalish(X0,e_5) ) ).
cnf(e_4_is_not_e_5,axiom,
~ equalish(e_4,e_5) ).
cnf(u47223,negated_conjecture,
( ~ product(X0,e_2,e_3)
| equalish(X0,e_1) ) ).
cnf(e_5_is_not_e_1,axiom,
~ equalish(e_5,e_1) ).
cnf(u48025,negated_conjecture,
( ~ 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)
| ~ group_element(X0) ) ).
cnf(u48040,negated_conjecture,
( ~ product(e_2,X0,X1)
| ~ product(X0,X1,e_4)
| equalish(X0,e_5) ) ).
cnf(u32510,negated_conjecture,
( ~ product(e_5,X0,e_1)
| equalish(X0,e_5) ) ).
cnf(u48206,negated_conjecture,
( ~ product(e_1,e_4,X0)
| ~ group_element(X0)
| product(e_4,X0,e_1)
| product(e_4,X0,e_2)
| product(e_4,X0,e_4)
| equalish(X0,e_3) ) ).
cnf(e_2_is_not_e_3,axiom,
~ equalish(e_2,e_3) ).
cnf(u48467,negated_conjecture,
( ~ group_element(X2)
| ~ product(X1,X2,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)
| ~ group_element(X0)
| product(X2,X0,e_1)
| product(X2,X0,e_2)
| product(X2,X0,e_3)
| product(X2,X0,e_4)
| equalish(X0,e_5) ) ).
cnf(u48289,negated_conjecture,
( ~ product(e_5,e_1,X0)
| ~ group_element(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(e_2_is_not_e_4,axiom,
~ equalish(e_2,e_4) ).
cnf(u44177,negated_conjecture,
( ~ group_element(X0)
| ~ product(X1,X2,e_3)
| equalish(X2,e_5)
| product(X0,e_2,e_1)
| product(X0,e_2,e_2)
| product(X0,e_2,e_3)
| product(X0,e_2,e_4)
| ~ product(X0,X1,X2) ) ).
cnf(e_1_is_not_e_5,axiom,
~ equalish(e_1,e_5) ).
cnf(u48522,negated_conjecture,
( ~ product(e_5,X0,X1)
| ~ product(X0,X1,e_2)
| equalish(X0,e_3) ) ).
cnf(u47996,negated_conjecture,
( ~ product(e_3,X0,X1)
| ~ product(X0,X1,e_4)
| equalish(X0,e_2) ) ).
cnf(u45539,negated_conjecture,
( ~ product(X0,e_5,e_2)
| equalish(X0,e_4) ) ).
cnf(u47349,negated_conjecture,
( ~ product(X0,e_5,e_2)
| ~ group_element(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(u46544,negated_conjecture,
( ~ product(e_3,e_2,X0)
| ~ product(e_1,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X2,e_2) ) ).
cnf(u32512,negated_conjecture,
( ~ product(X1,X2,e_1)
| ~ product(X0,X1,X2)
| equalish(X2,e_5)
| product(X0,e_5,e_1)
| product(X0,e_5,e_2)
| product(X0,e_5,e_3)
| product(X0,e_5,e_4)
| ~ group_element(X0) ) ).
cnf(u48485,negated_conjecture,
( ~ product(X0,e_4,e_2)
| product(X0,e_3,e_2)
| product(X0,e_3,e_3)
| product(X0,e_3,e_4)
| ~ group_element(X0)
| product(X0,e_3,e_1) ) ).
cnf(u48083,negated_conjecture,
( ~ group_element(X1)
| ~ product(e_5,X1,X0)
| ~ group_element(X0)
| product(X1,X0,e_1)
| product(X1,X0,e_2)
| product(X1,X0,e_3)
| product(X1,X0,e_4)
| equalish(X0,e_1) ) ).
cnf(e_2_is_not_e_1,axiom,
~ equalish(e_2,e_1) ).
cnf(u32508,negated_conjecture,
( ~ product(e_5,e_1,X0)
| ~ product(e_5,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X2,e_1) ) ).
cnf(u47952,negated_conjecture,
( ~ product(e_4,X0,e_1)
| equalish(X0,e_4) ) ).
cnf(u48720,negated_conjecture,
( ~ product(e_3,e_3,X0)
| ~ group_element(X0)
| product(e_3,X0,e_1)
| product(e_3,X0,e_2)
| product(e_3,X0,e_3)
| equalish(X0,e_2) ) ).
cnf(u46542,negated_conjecture,
( ~ product(e_3,e_2,X0)
| ~ product(e_1,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X1,e_3) ) ).
cnf(u48054,negated_conjecture,
( ~ product(X0,e_5,e_3)
| product(X0,e_1,e_1)
| product(X0,e_1,e_2)
| product(X0,e_1,e_4)
| ~ group_element(X0) ) ).
cnf(u48402,negated_conjecture,
( ~ product(X0,e_5,e_4)
| ~ group_element(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(u44174,negated_conjecture,
( ~ product(e_5,e_3,X0)
| ~ product(e_2,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X2,e_3) ) ).
cnf(e_3_is_not_e_2,axiom,
~ equalish(e_3,e_2) ).
cnf(u48473,negated_conjecture,
( ~ 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)
| ~ group_element(X0)
| ~ product(X0,e_5,X1)
| product(e_5,X1,e_2)
| product(e_5,X1,e_3)
| product(e_5,X1,e_4)
| equalish(X1,e_5) ) ).
cnf(u36079,negated_conjecture,
~ product(e_2,e_4,e_5) ).
cnf(e_3_is_not_e_4,axiom,
~ equalish(e_3,e_4) ).
cnf(u47204,negated_conjecture,
( ~ product(e_1,e_2,X0)
| ~ product(e_2,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X1,e_1) ) ).
cnf(u48738,negated_conjecture,
( ~ product(e_3,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)
| ~ group_element(X0) ) ).
cnf(u478,negated_conjecture,
equalish(e_2,e_2) ).
cnf(u48309,negated_conjecture,
( ~ product(e_4,X0,X1)
| ~ product(X0,X1,e_1)
| equalish(X1,e_3) ) ).
cnf(u46777,negated_conjecture,
( ~ product(X0,e_2,e_4)
| equalish(X0,e_3) ) ).
cnf(e_2_is_not_e_5,axiom,
~ equalish(e_2,e_5) ).
cnf(u15767,negated_conjecture,
~ product(e_1,e_5,e_5) ).
cnf(u47945,negated_conjecture,
( ~ group_element(X0)
| product(X0,e_2,e_2)
| product(X0,e_2,e_3)
| product(X0,e_2,e_4)
| product(X0,e_2,e_1)
| equalish(e_4,X0) ) ).
cnf(u47992,negated_conjecture,
( ~ product(X0,e_3,e_3)
| equalish(X0,e_4) ) ).
cnf(u48307,negated_conjecture,
( ~ product(X0,X1,e_5)
| ~ product(e_3,X0,X1)
| equalish(X1,e_2) ) ).
cnf(u48369,negated_conjecture,
( ~ product(e_4,X0,X1)
| ~ product(X0,X1,e_1)
| equalish(X0,e_3) ) ).
cnf(e_3_is_not_e_1,axiom,
~ equalish(e_3,e_1) ).
cnf(u48617,negated_conjecture,
( ~ group_element(X0)
| product(X0,e_2,e_2)
| product(X0,e_2,e_3)
| product(X0,e_2,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(element_3,axiom,
group_element(e_3) ).
cnf(u47224,negated_conjecture,
( ~ product(e_2,e_3,X0)
| ~ product(e_1,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X2,e_3) ) ).
cnf(u48470,negated_conjecture,
( ~ 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)
| ~ group_element(X0)
| ~ product(X0,e_3,X1)
| product(e_3,X1,e_1)
| product(e_3,X1,e_2)
| product(e_3,X1,e_3)
| product(e_3,X1,e_4)
| equalish(X1,e_5) ) ).
cnf(u48495,negated_conjecture,
( ~ product(X0,e_5,e_1)
| product(X0,e_3,e_2)
| product(X0,e_3,e_3)
| product(X0,e_3,e_4)
| ~ group_element(X0)
| product(X0,e_3,e_1) ) ).
cnf(u46605,negated_conjecture,
~ product(e_3,e_4,e_5) ).
cnf(u48225,negated_conjecture,
( ~ product(e_4,X0,X1)
| ~ product(X0,X1,e_4)
| equalish(X0,e_4) ) ).
cnf(u48056,negated_conjecture,
( ~ product(e_1,X0,X1)
| ~ product(X0,X1,e_3)
| equalish(X1,e_4) ) ).
cnf(element_4,axiom,
group_element(e_4) ).
cnf(u47985,negated_conjecture,
( ~ product(X0,e_4,e_2)
| equalish(X0,e_3) ) ).
cnf(u73,negated_conjecture,
( ~ group_element(X3)
| equalish(X1,X3)
| ~ product(X0,X1,X2)
| product(X0,X3,e_1)
| product(X0,X3,e_2)
| product(X0,X3,e_3)
| product(X0,X3,e_4)
| ~ group_element(X0)
| product(X3,e_5,e_1)
| product(X3,e_5,e_2)
| product(X3,e_5,e_3)
| product(X3,e_5,e_4)
| ~ group_element(X2)
| product(X1,X2,e_1)
| product(X1,X2,e_2)
| product(X1,X2,e_3)
| product(X1,X2,e_4)
| ~ group_element(X1) ) ).
cnf(u75,axiom,
( ~ next(X0,X1)
| ~ greater(e_5,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)
| ~ group_element(X0) ) ).
cnf(element_1,axiom,
group_element(e_1) ).
cnf(u48449,negated_conjecture,
( ~ product(e_5,X0,X1)
| ~ product(X0,X1,e_2)
| equalish(X1,e_4) ) ).
cnf(u45542,negated_conjecture,
( ~ product(e_4,X0,e_2)
| equalish(X0,e_5) ) ).
cnf(u72,negated_conjecture,
( ~ group_element(X3)
| equalish(X2,e_5)
| ~ product(X0,X1,X2)
| product(X0,X3,e_1)
| product(X0,X3,e_2)
| product(X0,X3,e_3)
| product(X0,X3,e_4)
| ~ group_element(X0)
| product(X3,e_5,e_1)
| product(X3,e_5,e_2)
| product(X3,e_5,e_3)
| product(X3,e_5,e_4)
| ~ group_element(X2)
| product(X1,X2,e_1)
| product(X1,X2,e_2)
| product(X1,X2,e_3)
| product(X1,X2,e_4)
| ~ group_element(X1) ) ).
cnf(u47994,negated_conjecture,
( ~ product(e_4,e_3,X0)
| equalish(X0,e_3) ) ).
cnf(element_2,axiom,
group_element(e_2) ).
cnf(u48008,negated_conjecture,
( ~ product(e_2,e_4,X0)
| equalish(X0,e_4) ) ).
cnf(u47995,negated_conjecture,
( ~ product(e_4,X0,e_3)
| equalish(X0,e_3) ) ).
cnf(e_1_is_not_e_3,axiom,
~ equalish(e_1,e_3) ).
cnf(u48058,negated_conjecture,
( ~ product(e_4,e_3,X0)
| ~ product(e_5,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X1,e_4) ) ).
cnf(u47134,negated_conjecture,
( ~ product(e_1,e_3,X0)
| ~ product(e_3,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X1,e_1) ) ).
cnf(u47145,negated_conjecture,
( ~ product(e_1,e_1,X0)
| ~ product(e_1,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X2,e_1) ) ).
cnf(u48357,negated_conjecture,
( ~ product(e_1,e_4,X0)
| ~ group_element(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(u48537,negated_conjecture,
( ~ group_element(X0)
| ~ product(X1,X0,X2)
| 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)
| ~ group_element(X2)
| product(X0,X2,e_1)
| product(X0,X2,e_2)
| product(X0,X2,e_3)
| product(X0,X2,e_4)
| equalish(X0,e_3) ) ).
cnf(e_1_is_not_e_4,axiom,
~ equalish(e_1,e_4) ).
cnf(u48059,negated_conjecture,
( ~ product(X0,e_4,e_3)
| equalish(X0,e_5) ) ).
cnf(u48246,negated_conjecture,
( ~ product(X0,e_5,e_2)
| ~ group_element(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(u47726,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(u46546,negated_conjecture,
( ~ product(e_1,X0,e_2)
| equalish(X0,e_3) ) ).
cnf(u48431,negated_conjecture,
( ~ product(X0,e_5,e_4)
| ~ group_element(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(u47986,negated_conjecture,
( ~ product(e_4,e_2,X0)
| ~ product(e_3,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X2,e_2) ) ).
cnf(element_5,axiom,
group_element(e_5) ).
cnf(u47330,negated_conjecture,
( ~ product(e_1,X0,X1)
| ~ product(X0,X1,e_1)
| equalish(X1,e_1) ) ).
cnf(u46945,negated_conjecture,
( ~ product(X0,X1,e_4)
| ~ product(e_1,X0,X1)
| equalish(X1,e_2) ) ).
cnf(e_1_is_not_e_2,axiom,
~ equalish(e_1,e_2) ).
cnf(u48022,axiom,
( ~ product(e_4,e_1,X0)
| equalish(X0,e_4) ) ).
cnf(u45543,negated_conjecture,
( ~ product(X1,X2,e_2)
| ~ product(X0,X1,X2)
| equalish(X2,e_5)
| product(X0,e_4,e_1)
| product(X0,e_4,e_2)
| product(X0,e_4,e_3)
| product(X0,e_4,e_4)
| ~ group_element(X0) ) ).
cnf(u48571,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(e_4_greater_e_2,axiom,
greater(e_4,e_2) ).
cnf(u47206,negated_conjecture,
( ~ product(e_1,e_2,X0)
| ~ product(e_2,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X2,e_2) ) ).
cnf(u48327,negated_conjecture,
( ~ product(e_4,e_3,X0)
| ~ group_element(X0)
| product(e_3,X0,e_1)
| product(e_3,X0,e_3)
| product(e_3,X0,e_4)
| equalish(X0,e_4) ) ).
cnf(u48006,negated_conjecture,
( ~ product(X0,e_4,e_4)
| equalish(X0,e_2) ) ).
cnf(u47439,negated_conjecture,
( ~ product(e_2,X0,X1)
| ~ product(X0,X1,e_3)
| equalish(X0,e_1) ) ).
cnf(u48687,negated_conjecture,
( ~ product(X0,e_5,e_3)
| ~ group_element(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(u48039,negated_conjecture,
( ~ product(X0,e_2,e_2)
| product(X0,e_5,e_1)
| product(X0,e_5,e_3)
| product(X0,e_5,e_4)
| ~ group_element(X0) ) ).
cnf(u48751,axiom,
~ greater(e_3,e_4) ).
cnf(u48055,negated_conjecture,
( ~ product(e_1,X0,X1)
| ~ product(X0,X1,e_3)
| equalish(X0,e_5) ) ).
cnf(e_5_greater_e_2,axiom,
greater(e_5,e_2) ).
cnf(u48034,negated_conjecture,
( ~ product(e_2,e_1,X0)
| ~ product(e_2,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X2,e_1) ) ).
cnf(u48385,negated_conjecture,
( ~ product(e_2,X0,X1)
| ~ product(X0,X1,e_1)
| equalish(X1,e_4) ) ).
cnf(u32509,negated_conjecture,
( ~ product(e_5,e_5,X0)
| equalish(X0,e_1) ) ).
cnf(u48011,negated_conjecture,
( ~ product(X0,e_2,e_4)
| product(X0,e_1,e_1)
| product(X0,e_1,e_2)
| product(X0,e_1,e_3)
| product(X0,e_1,e_4)
| ~ group_element(X0) ) ).
cnf(e_5_greater_e_1,axiom,
greater(e_5,e_1) ).
cnf(u48286,negated_conjecture,
( ~ product(e_5,e_4,X0)
| ~ group_element(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(u47988,negated_conjecture,
( ~ product(e_3,X0,e_2)
| equalish(X0,e_4) ) ).
cnf(u46778,negated_conjecture,
( ~ product(e_2,e_4,X0)
| ~ product(e_3,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X2,e_4) ) ).
cnf(e_3_greater_e_2,axiom,
greater(e_3,e_2) ).
cnf(u47943,negated_conjecture,
( ~ product(e_4,X0,X1)
| equalish(X1,e_5)
| ~ product(X0,X1,e_3) ) ).
cnf(u48359,negated_conjecture,
( ~ product(e_1,e_1,X0)
| ~ group_element(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(u48696,negated_conjecture,
( ~ product(e_4,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)
| ~ group_element(X0) ) ).
cnf(u48205,negated_conjecture,
( ~ product(e_1,e_5,X0)
| ~ group_element(X0)
| product(e_5,X0,e_1)
| product(e_5,X0,e_2)
| product(e_5,X0,e_3)
| equalish(X0,e_3) ) ).
cnf(u47950,negated_conjecture,
( ~ product(e_4,e_1,X0)
| ~ product(e_4,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X2,e_1) ) ).
cnf(u47706,negated_conjecture,
~ product(e_2,e_1,e_5) ).
cnf(e_5_greater_e_4,axiom,
greater(e_5,e_4) ).
cnf(u48173,negated_conjecture,
( ~ product(e_4,X0,X1)
| ~ product(X0,X1,e_4)
| equalish(X1,e_1) ) ).
cnf(u47176,negated_conjecture,
( ~ product(X1,X2,e_4)
| ~ product(X0,X1,X2)
| equalish(X1,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)
| ~ group_element(X0) ) ).
cnf(u47136,negated_conjecture,
( ~ product(e_1,e_3,X0)
| ~ product(e_3,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X2,e_3) ) ).
cnf(no_redundancy,axiom,
( ~ product(X0,e_1,X1)
| ~ next(X0,X2)
| ~ greater(X1,X2) ) ).
cnf(u48035,negated_conjecture,
( ~ product(e_2,e_2,X0)
| equalish(X0,e_1) ) ).
cnf(u48343,negated_conjecture,
( ~ product(e_5,X0,X1)
| ~ product(X0,X1,e_1)
| equalish(X0,e_2) ) ).
cnf(u48007,negated_conjecture,
( ~ product(e_4,e_4,X0)
| ~ product(e_2,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X2,e_4) ) ).
cnf(u47728,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(u71,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(u48721,negated_conjecture,
( ~ product(e_3,e_2,X0)
| ~ group_element(X0)
| product(e_2,X0,e_2)
| product(e_2,X0,e_3)
| product(e_2,X0,e_4)
| equalish(X0,e_2) ) ).
cnf(e_4_greater_e_3,axiom,
greater(e_4,e_3) ).
cnf(u47729,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(u48409,negated_conjecture,
( ~ product(e_2,X0,X1)
| ~ product(X0,X1,e_1)
| equalish(X0,e_4) ) ).
cnf(e_5_greater_e_3,axiom,
greater(e_5,e_3) ).
cnf(u48544,negated_conjecture,
( ~ 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)
| ~ group_element(X0)
| ~ product(X0,e_4,X1)
| product(e_4,X1,e_1)
| product(e_4,X1,e_2)
| product(e_4,X1,e_3)
| product(e_4,X1,e_4) ) ).
cnf(u47974,negated_conjecture,
( ~ product(X0,e_2,e_2)
| equalish(X0,e_5) ) ).
cnf(u48615,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_4,e_1)
| product(X0,e_4,e_2)
| product(X0,e_4,e_3)
| product(X0,e_4,e_4) ) ).
cnf(u48318,negated_conjecture,
( ~ product(X0,e_5,e_1)
| ~ group_element(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(e_2_then_e_3,axiom,
next(e_2,e_3) ).
cnf(u47140,axiom,
( ~ greater(e_1,X0)
| ~ next(e_1,X0) ) ).
cnf(u47225,negated_conjecture,
( ~ product(e_1,e_2,X0)
| equalish(X0,e_3) ) ).
cnf(u48740,negated_conjecture,
( ~ product(e_3,e_1,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)
| ~ group_element(X0) ) ).
cnf(u47226,negated_conjecture,
( ~ product(e_1,X0,e_3)
| equalish(X0,e_2) ) ).
cnf(u48394,negated_conjecture,
( ~ product(X0,e_5,e_1)
| ~ group_element(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(u48048,negated_conjecture,
( ~ product(X0,e_3,e_4)
| equalish(X0,e_5) ) ).
cnf(u48026,negated_conjecture,
( ~ product(X0,e_4,e_1)
| product(X0,e_1,e_2)
| product(X0,e_1,e_3)
| product(X0,e_1,e_4)
| ~ group_element(X0) ) ).
cnf(u44173,negated_conjecture,
( ~ product(X0,e_5,e_3)
| equalish(X0,e_2) ) ).
cnf(e_3_then_e_4,axiom,
next(e_3,e_4) ).
cnf(u47339,negated_conjecture,
( ~ product(X0,e_5,e_1)
| ~ group_element(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(u47964,negated_conjecture,
( ~ product(e_3,e_3,X0)
| equalish(X0,e_1) ) ).
cnf(u48257,negated_conjecture,
( ~ product(X0,e_5,e_1)
| ~ group_element(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(u47725,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(u48356,negated_conjecture,
( ~ product(e_1,e_5,X0)
| ~ group_element(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(u48032,negated_conjecture,
( ~ product(e_2,e_1,X0)
| ~ product(e_2,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X1,e_2) ) ).
cnf(u47766,negated_conjecture,
( ~ 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)
| equalish(e_1,X0) ) ).
cnf(u47975,negated_conjecture,
( ~ product(e_2,e_2,X0)
| ~ product(e_5,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X2,e_2) ) ).
cnf(e_1_then_e_2,axiom,
next(e_1,e_2) ).
cnf(u48476,negated_conjecture,
( ~ 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)
| ~ group_element(X0)
| ~ product(X0,e_1,X1)
| product(e_1,X1,e_1)
| product(e_1,X1,e_2)
| product(e_1,X1,e_3)
| equalish(X1,e_5) ) ).
cnf(u48328,negated_conjecture,
( ~ product(e_4,e_2,X0)
| ~ group_element(X0)
| product(e_2,X0,e_1)
| product(e_2,X0,e_2)
| product(e_2,X0,e_3)
| equalish(X0,e_4) ) ).
cnf(u44176,negated_conjecture,
( ~ product(e_2,X0,e_3)
| equalish(X0,e_5) ) ).
cnf(u48697,negated_conjecture,
( ~ product(e_4,e_2,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)
| ~ group_element(X0) ) ).
cnf(e_3_greater_e_1,axiom,
greater(e_3,e_1) ).
cnf(u48012,negated_conjecture,
( ~ product(X0,e_2,e_4)
| product(X0,e_1,e_1)
| product(X0,e_1,e_2)
| product(X0,e_1,e_3)
| ~ group_element(X0) ) ).
cnf(u48739,negated_conjecture,
( ~ product(e_3,e_2,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)
| ~ group_element(X0) ) ).
cnf(u477,negated_conjecture,
equalish(e_3,e_3) ).
cnf(e_4_greater_e_1,axiom,
greater(e_4,e_1) ).
cnf(u48019,negated_conjecture,
( ~ product(e_1,e_4,X0)
| ~ product(e_4,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X1,e_1) ) ).
cnf(u48288,negated_conjecture,
( ~ product(e_5,e_2,X0)
| ~ group_element(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(u47944,negated_conjecture,
( ~ product(e_4,X0,X1)
| equalish(X0,e_2)
| ~ product(X0,X1,e_3) ) ).
cnf(u48077,negated_conjecture,
( ~ group_element(X1)
| ~ product(e_1,X1,X0)
| ~ group_element(X0)
| product(X1,X0,e_1)
| product(X1,X0,e_2)
| product(X1,X0,e_3)
| product(X1,X0,e_4)
| equalish(X0,e_3) ) ).
cnf(u48023,axiom,
( ~ product(e_4,X0,e_4)
| equalish(X0,e_1) ) ).
cnf(u48248,negated_conjecture,
( ~ product(e_5,X0,X1)
| ~ product(X0,X1,e_1)
| equalish(X1,e_2) ) ).
cnf(e_4_then_e_5,axiom,
next(e_4,e_5) ).
cnf(u48325,negated_conjecture,
( ~ product(e_4,e_5,X0)
| ~ group_element(X0)
| product(e_5,X0,e_1)
| product(e_5,X0,e_2)
| product(e_5,X0,e_4)
| equalish(X0,e_4) ) ).
cnf(u48051,negated_conjecture,
( ~ product(e_5,X0,e_4)
| equalish(X0,e_3) ) ).
cnf(u48005,negated_conjecture,
( ~ product(e_4,e_4,X0)
| ~ product(e_2,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X1,e_4) ) ).
cnf(e_2_greater_e_1,axiom,
greater(e_2,e_1) ).
cnf(u47172,negated_conjecture,
( ~ product(e_1,X0,e_4)
| equalish(X0,e_5) ) ).
cnf(u48021,negated_conjecture,
( ~ product(e_1,e_4,X0)
| ~ product(e_4,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X2,e_4) ) ).
cnf(u48049,negated_conjecture,
( ~ product(e_3,e_4,X0)
| ~ product(e_5,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X2,e_4) ) ).
cnf(u47962,negated_conjecture,
( ~ product(X0,e_3,e_1)
| equalish(X0,e_3) ) ).
cnf(u48737,negated_conjecture,
( ~ product(e_3,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)
| ~ group_element(X0) ) ).
cnf(u47151,negated_conjecture,
( ~ product(X0,e_1,e_1)
| product(X0,e_5,e_2)
| product(X0,e_5,e_3)
| product(X0,e_5,e_4)
| ~ group_element(X0) ) ).
cnf(u48616,negated_conjecture,
( ~ group_element(X0)
| product(X0,e_2,e_2)
| product(X0,e_2,e_4)
| product(X0,e_2,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(u47207,negated_conjecture,
( ~ product(e_2,e_1,X0)
| equalish(X0,e_2) ) ).
cnf(u47402,negated_conjecture,
( ~ product(X0,e_5,e_3)
| ~ group_element(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(u47132,axiom,
( ~ next(e_3,X0)
| ~ greater(e_3,X0) ) ).
cnf(u47098,negated_conjecture,
( ~ product(X0,e_1,e_3)
| product(X0,e_4,e_1)
| product(X0,e_4,e_2)
| product(X0,e_4,e_3)
| product(X0,e_4,e_4)
| ~ group_element(X0) ) ).
cnf(u47968,negated_conjecture,
( ~ product(X0,e_3,e_3)
| product(X0,e_5,e_1)
| product(X0,e_5,e_2)
| product(X0,e_5,e_4)
| ~ group_element(X0) ) ).
cnf(u48171,negated_conjecture,
( ~ product(X0,e_5,e_3)
| ~ group_element(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(u48474,negated_conjecture,
( ~ 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)
| ~ group_element(X0)
| ~ product(X0,e_4,X1)
| product(e_4,X1,e_1)
| product(e_4,X1,e_3)
| product(e_4,X1,e_4)
| equalish(X1,e_5) ) ).
cnf(u48447,negated_conjecture,
( ~ product(X0,e_5,e_3)
| ~ group_element(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(u235,axiom,
equalish(e_1,e_1) ).
cnf(u48161,negated_conjecture,
( ~ product(X0,X1,e_5)
| ~ product(e_4,X0,X1)
| equalish(X0,e_1) ) ).
cnf(u47648,negated_conjecture,
( ~ product(X0,e_3,e_2)
| product(X0,e_1,e_1)
| product(X0,e_1,e_3)
| product(X0,e_1,e_4)
| ~ group_element(X0) ) ).
cnf(u48047,negated_conjecture,
( ~ product(e_3,e_4,X0)
| ~ product(e_5,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X1,e_3) ) ).
cnf(u48569,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(u47963,negated_conjecture,
( ~ product(e_3,e_1,X0)
| ~ product(e_3,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X2,e_1) ) ).
cnf(u47222,negated_conjecture,
( ~ product(e_2,e_3,X0)
| ~ product(e_1,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X1,e_2) ) ).
cnf(u48084,negated_conjecture,
( ~ group_element(X1)
| ~ product(e_4,X1,X0)
| ~ group_element(X0)
| product(X1,X0,e_1)
| product(X1,X0,e_2)
| product(X1,X0,e_3)
| product(X1,X0,e_4)
| equalish(X0,e_4) ) ).
cnf(u48041,negated_conjecture,
( ~ product(e_2,X0,X1)
| ~ product(X0,X1,e_4)
| equalish(X1,e_3) ) ).
cnf(u47138,axiom,
( ~ product(e_3,X0,e_3)
| equalish(X0,e_1) ) ).
cnf(u48719,negated_conjecture,
( ~ product(e_3,e_5,X0)
| ~ group_element(X0)
| product(e_5,X0,e_1)
| product(e_5,X0,e_3)
| product(e_5,X0,e_4)
| equalish(X0,e_2) ) ).
cnf(u48061,negated_conjecture,
( ~ product(e_5,e_4,X0)
| equalish(X0,e_3) ) ).
cnf(u44175,negated_conjecture,
( ~ product(e_2,e_5,X0)
| equalish(X0,e_3) ) ).
cnf(u48679,negated_conjecture,
( ~ product(e_5,X0,X1)
| ~ product(X0,X1,e_3)
| equalish(X1,e_3) ) ).
cnf(u47351,negated_conjecture,
( ~ product(e_3,X0,X1)
| ~ product(X0,X1,e_2)
| equalish(X0,e_1) ) ).
cnf(u48475,negated_conjecture,
( ~ 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)
| ~ group_element(X0)
| ~ product(X0,e_2,X1)
| product(e_2,X1,e_1)
| product(e_2,X1,e_2)
| product(e_2,X1,e_4)
| equalish(X1,e_5) ) ).
cnf(u59,negated_conjecture,
( ~ product(X1,X2,e_5)
| ~ product(X0,X1,X2)
| equalish(X1,X3)
| ~ group_element(X3)
| product(X0,X3,e_1)
| product(X0,X3,e_2)
| product(X0,X3,e_3)
| product(X0,X3,e_4)
| ~ group_element(X0)
| product(X3,e_5,e_1)
| product(X3,e_5,e_2)
| product(X3,e_5,e_3)
| product(X3,e_5,e_4) ) ).
cnf(u48423,negated_conjecture,
( ~ product(X0,e_5,e_4)
| equalish(X0,e_5)
| ~ group_element(X0)
| product(e_2,X0,e_1)
| product(e_2,X0,e_2)
| product(e_2,X0,e_4) ) ).
cnf(u56,negated_conjecture,
( ~ product(X0,e_5,X1)
| ~ product(X2,X3,X4)
| ~ product(X3,X4,X1)
| equalish(X3,X0)
| ~ group_element(X0)
| product(X2,X0,e_1)
| product(X2,X0,e_2)
| product(X2,X0,e_3)
| product(X2,X0,e_4)
| ~ group_element(X2) ) ).
cnf(u47209,negated_conjecture,
( ~ product(X0,e_2,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)
| ~ group_element(X0) ) ).
cnf(u45544,negated_conjecture,
( ~ group_element(X0)
| ~ product(X1,X2,e_2)
| equalish(X1,e_4)
| product(X0,e_4,e_1)
| product(X0,e_4,e_2)
| product(X0,e_4,e_3)
| product(X0,e_4,e_4)
| ~ product(X0,X1,X2) ) ).
cnf(u48060,negated_conjecture,
( ~ product(e_4,e_3,X0)
| ~ product(e_5,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X2,e_3) ) ).
cnf(u47143,negated_conjecture,
( ~ product(e_1,e_1,X0)
| ~ product(e_1,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X1,e_1) ) ).
cnf(u47661,negated_conjecture,
( ~ product(e_3,X0,X1)
| equalish(X0,e_5)
| ~ product(X0,X1,e_1) ) ).
cnf(u47997,negated_conjecture,
( ~ product(e_3,X0,X1)
| ~ product(X0,X1,e_4)
| equalish(X1,e_4) ) ).
cnf(u48752,axiom,
~ greater(e_4,e_5) ).
cnf(u45541,negated_conjecture,
( ~ product(e_4,e_5,X0)
| equalish(X0,e_2) ) ).
cnf(u45538,negated_conjecture,
( ~ product(e_5,e_2,X0)
| ~ product(e_4,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X1,e_5) ) ).
cnf(u47965,negated_conjecture,
( ~ product(e_3,X0,e_1)
| equalish(X0,e_3) ) ).
cnf(u46776,negated_conjecture,
( ~ product(e_2,e_4,X0)
| ~ product(e_3,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X1,e_2) ) ).
cnf(u48642,negated_conjecture,
( ~ 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_5,e_2)
| product(X0,e_5,e_3)
| product(X0,e_5,e_4) ) ).
cnf(u32513,negated_conjecture,
( ~ group_element(X0)
| ~ product(X1,X2,e_1)
| equalish(X1,e_5)
| product(X0,e_5,e_1)
| product(X0,e_5,e_2)
| product(X0,e_5,e_3)
| product(X0,e_5,e_4)
| ~ product(X0,X1,X2) ) ).
cnf(u48033,negated_conjecture,
( ~ product(X0,e_2,e_1)
| equalish(X0,e_2) ) ).
cnf(u48383,negated_conjecture,
( ~ product(X0,X1,e_5)
| ~ product(e_3,X0,X1)
| equalish(X0,e_4) ) ).
cnf(u48505,negated_conjecture,
( ~ product(X0,e_2,e_3)
| product(X0,e_3,e_2)
| product(X0,e_3,e_3)
| product(X0,e_3,e_4)
| ~ group_element(X0)
| product(X0,e_3,e_1) ) ).
cnf(u47168,negated_conjecture,
( ~ product(e_5,e_4,X0)
| ~ product(e_1,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X1,e_5) ) ).
cnf(u48567,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(u47993,negated_conjecture,
( ~ product(e_3,e_3,X0)
| ~ product(e_4,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X2,e_3) ) ).
cnf(u48238,negated_conjecture,
( ~ product(X0,e_5,e_2)
| equalish(X0,e_5)
| ~ group_element(X0)
| product(e_4,X0,e_1)
| product(e_4,X0,e_3)
| product(e_4,X0,e_4) ) ).
cnf(u47948,negated_conjecture,
( ~ product(e_4,e_1,X0)
| ~ product(e_4,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X1,e_4) ) ).
cnf(u47970,negated_conjecture,
( ~ product(e_4,X0,X1)
| ~ product(X0,X1,e_2)
| equalish(X1,e_2) ) ).
cnf(u48326,negated_conjecture,
( ~ product(e_4,e_4,X0)
| ~ group_element(X0)
| product(e_4,X0,e_2)
| product(e_4,X0,e_3)
| product(e_4,X0,e_4)
| equalish(X0,e_4) ) ).
cnf(u47961,negated_conjecture,
( ~ product(e_3,e_1,X0)
| ~ product(e_3,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X1,e_3) ) ).
cnf(u47147,axiom,
( ~ product(e_1,X0,e_1)
| equalish(X0,e_1) ) ).
cnf(u48102,negated_conjecture,
( ~ group_element(X0)
| ~ product(e_1,X0,X1)
| ~ group_element(X1)
| product(X0,X1,e_1)
| product(X0,X1,e_2)
| product(X0,X1,e_3)
| product(X0,X1,e_4)
| equalish(X0,e_2) ) ).
cnf(u47973,negated_conjecture,
( ~ product(e_2,e_2,X0)
| ~ product(e_5,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X1,e_2) ) ).
cnf(u48053,negated_conjecture,
( ~ product(X0,e_5,e_3)
| product(X0,e_1,e_1)
| product(X0,e_1,e_2)
| product(X0,e_1,e_3)
| product(X0,e_1,e_4)
| ~ group_element(X0) ) ).
cnf(u48694,negated_conjecture,
( ~ product(e_4,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)
| ~ group_element(X0) ) ).
cnf(u46543,negated_conjecture,
( ~ product(X0,e_3,e_2)
| equalish(X0,e_1) ) ).
cnf(u48,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(u47201,negated_conjecture,
( ~ greater(e_2,X0)
| ~ next(e_2,X0) ) ).
cnf(u48583,negated_conjecture,
( ~ 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_4) ) ).
cnf(u48181,negated_conjecture,
( ~ product(X0,e_5,e_4)
| ~ group_element(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(u49,negated_conjecture,
( ~ product(X0,e_5,X1)
| ~ product(X2,X3,X4)
| ~ product(X3,X4,X1)
| equalish(X4,e_5)
| ~ group_element(X0)
| product(X2,X0,e_1)
| product(X2,X0,e_2)
| product(X2,X0,e_3)
| product(X2,X0,e_4)
| ~ group_element(X2) ) ).
cnf(u48009,negated_conjecture,
( ~ product(e_2,X0,e_4)
| equalish(X0,e_4) ) ).
cnf(u47969,negated_conjecture,
( ~ product(e_4,X0,X1)
| ~ product(X0,X1,e_2)
| equalish(X0,e_5) ) ).
cnf(u48568,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(u48585,negated_conjecture,
( ~ group_element(X0)
| product(X0,e_5,e_2)
| 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(u45540,negated_conjecture,
( ~ product(e_5,e_2,X0)
| ~ product(e_4,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X2,e_2) ) ).
cnf(u48545,negated_conjecture,
( ~ 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)
| ~ group_element(X0)
| ~ product(X0,e_2,X1)
| product(e_2,X1,e_1)
| product(e_2,X1,e_2)
| product(e_2,X1,e_3)
| product(e_2,X1,e_4) ) ).
cnf(u55,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(u48707,negated_conjecture,
( ~ product(e_5,X0,X1)
| ~ product(X0,X1,e_3)
| equalish(X0,e_4) ) ).
cnf(u48667,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_1,e_1)
| product(X0,e_1,e_2)
| product(X0,e_1,e_3)
| product(X0,e_1,e_4) ) ).
cnf(u46779,negated_conjecture,
( ~ product(e_3,e_2,X0)
| equalish(X0,e_4) ) ).
cnf(u47780,negated_conjecture,
( ~ 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)
| equalish(e_3,X0) ) ).
cnf(u48543,negated_conjecture,
( ~ 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)
| ~ group_element(X0)
| ~ product(X0,e_5,X1)
| product(e_5,X1,e_1)
| product(e_5,X1,e_2)
| product(e_5,X1,e_3)
| product(e_5,X1,e_4) ) ).
cnf(u48384,negated_conjecture,
( ~ group_element(X0)
| equalish(X0,e_4)
| ~ group_element(X1)
| product(X0,X1,e_1)
| product(X0,X1,e_2)
| product(X0,X1,e_3)
| product(X0,X1,e_4)
| ~ product(e_3,X0,X1) ) ).
cnf(u47984,negated_conjecture,
( ~ product(e_4,e_2,X0)
| ~ product(e_3,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X1,e_4) ) ).
cnf(u47949,negated_conjecture,
( ~ product(X0,e_4,e_1)
| equalish(X0,e_4) ) ).
cnf(u52,negated_conjecture,
( ~ product(X1,X2,e_5)
| ~ product(X0,X1,X2)
| equalish(X2,e_5)
| ~ group_element(X3)
| product(X0,X3,e_1)
| product(X0,X3,e_2)
| product(X0,X3,e_3)
| product(X0,X3,e_4)
| ~ group_element(X0)
| product(X3,e_5,e_1)
| product(X3,e_5,e_2)
| product(X3,e_5,e_3)
| product(X3,e_5,e_4) ) ).
cnf(u35725,negated_conjecture,
~ product(e_5,e_5,e_5) ).
cnf(u48218,negated_conjecture,
( ~ product(e_2,X0,X1)
| ~ product(X0,X1,e_2)
| equalish(X0,e_2) ) ).
cnf(u48081,negated_conjecture,
( ~ group_element(X0)
| ~ product(e_5,X0,X1)
| ~ group_element(X1)
| product(X0,X1,e_1)
| product(X0,X1,e_2)
| product(X0,X1,e_3)
| product(X0,X1,e_4)
| equalish(X0,e_5) ) ).
cnf(u47936,negated_conjecture,
( ~ 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)
| equalish(e_2,X0) ) ).
cnf(u47205,negated_conjecture,
( ~ product(X0,e_1,e_2)
| equalish(X0,e_2) ) ).
cnf(u53,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(u47208,negated_conjecture,
( ~ product(e_2,X0,e_2)
| equalish(X0,e_1) ) ).
cnf(u32506,negated_conjecture,
( ~ product(e_5,e_1,X0)
| ~ product(e_5,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X1,e_5) ) ).
cnf(u48183,negated_conjecture,
( ~ product(e_2,X0,X1)
| ~ product(X0,X1,e_2)
| equalish(X1,e_1) ) ).
cnf(product_total_function2,axiom,
( ~ product(X0,X1,X3)
| ~ product(X0,X1,X2)
| equalish(X2,X3) ) ).
cnf(u48013,axiom,
( ~ next(e_4,X0)
| ~ greater(e_4,X0) ) ).
cnf(u48050,negated_conjecture,
( ~ product(e_5,e_3,X0)
| equalish(X0,e_4) ) ).
cnf(u48358,negated_conjecture,
( ~ product(e_1,e_3,X0)
| ~ group_element(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(u47989,negated_conjecture,
( ~ product(X0,e_3,e_4)
| product(X0,e_4,e_1)
| product(X0,e_4,e_2)
| product(X0,e_4,e_3)
| product(X0,e_4,e_4)
| ~ group_element(X0) ) ).
cnf(u47617,negated_conjecture,
( ~ product(X0,e_3,e_2)
| product(X0,e_1,e_1)
| product(X0,e_1,e_2)
| product(X0,e_1,e_3)
| product(X0,e_1,e_4)
| ~ group_element(X0) ) ).
cnf(u47606,negated_conjecture,
( ~ product(e_1,X0,X1)
| equalish(X0,e_4)
| ~ product(X0,X1,e_2) ) ).
cnf(product_right_cancellation,axiom,
( ~ product(X0,X3,X2)
| ~ product(X0,X1,X2)
| equalish(X1,X3) ) ).
cnf(e_5_is_not_e_4,axiom,
~ equalish(e_5,e_4) ).
cnf(u46780,negated_conjecture,
( ~ product(e_3,X0,e_4)
| equalish(X0,e_2) ) ).
cnf(u47137,axiom,
( ~ product(e_3,e_1,X0)
| equalish(X0,e_3) ) ).
cnf(u47987,negated_conjecture,
( ~ product(e_3,e_4,X0)
| equalish(X0,e_2) ) ).
cnf(u48191,negated_conjecture,
( ~ product(X0,e_5,e_2)
| ~ group_element(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(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(u48193,negated_conjecture,
( ~ product(e_3,X0,X1)
| ~ product(X0,X1,e_3)
| equalish(X0,e_3) ) ).
cnf(u48643,negated_conjecture,
( ~ group_element(X0)
| product(X0,e_3,e_2)
| product(X0,e_3,e_3)
| product(X0,e_3,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(u47146,axiom,
( ~ product(e_1,e_1,X0)
| equalish(X0,e_1) ) ).
cnf(qg2_2,negated_conjecture,
( ~ product(X5,X3,X4)
| ~ product(X3,X4,X2)
| ~ product(X5,X0,X1)
| ~ product(X0,X1,X2)
| equalish(X1,X4) ) ).
cnf(u47935,negated_conjecture,
( ~ 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)
| equalish(e_5,X0) ) ).
cnf(u48062,negated_conjecture,
( ~ product(e_5,X0,e_3)
| equalish(X0,e_4) ) ).
cnf(u47,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(u47169,negated_conjecture,
( ~ product(X0,e_5,e_4)
| equalish(X0,e_1) ) ).
cnf(u47394,negated_conjecture,
( ~ product(e_2,X0,X1)
| ~ product(X0,X1,e_3)
| equalish(X1,e_2) ) ).
cnf(u48515,negated_conjecture,
( ~ product(X0,e_1,e_4)
| product(X0,e_3,e_2)
| product(X0,e_3,e_3)
| product(X0,e_3,e_4)
| ~ group_element(X0)
| product(X0,e_3,e_1) ) ).
cnf(u47978,negated_conjecture,
( ~ product(X0,e_5,e_2)
| product(X0,e_4,e_1)
| product(X0,e_4,e_2)
| product(X0,e_4,e_3)
| product(X0,e_4,e_4)
| ~ group_element(X0) ) ).
cnf(product_left_cancellation,axiom,
( ~ product(X3,X1,X2)
| ~ product(X0,X1,X2)
| equalish(X0,X3) ) ).
cnf(u48308,negated_conjecture,
( ~ group_element(X0)
| equalish(X1,e_2)
| ~ group_element(X1)
| product(X0,X1,e_1)
| product(X0,X1,e_2)
| product(X0,X1,e_3)
| product(X0,X1,e_4)
| ~ product(e_3,X0,X1) ) ).
cnf(u47170,negated_conjecture,
( ~ product(e_5,e_4,X0)
| ~ product(e_1,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X2,e_4) ) ).
cnf(u47171,negated_conjecture,
( ~ product(e_1,e_5,X0)
| equalish(X0,e_4) ) ).
cnf(u48570,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(u48207,negated_conjecture,
( ~ product(e_1,e_3,X0)
| ~ group_element(X0)
| product(e_3,X0,e_2)
| product(e_3,X0,e_3)
| product(e_3,X0,e_4)
| equalish(X0,e_3) ) ).
cnf(qg2_1,negated_conjecture,
( ~ product(X5,X3,X4)
| ~ product(X3,X4,X2)
| ~ product(X5,X0,X1)
| ~ product(X0,X1,X2)
| equalish(X0,X3) ) ).
cnf(u48750,negated_conjecture,
~ next(e_2,e_1) ).
cnf(u48020,axiom,
( ~ product(X0,e_1,e_4)
| equalish(X0,e_4) ) ).
cnf(e_4_is_not_e_2,axiom,
~ equalish(e_4,e_2) ).
cnf(u47951,negated_conjecture,
( ~ product(e_4,e_4,X0)
| equalish(X0,e_1) ) ).
cnf(u46545,negated_conjecture,
( ~ product(e_1,e_3,X0)
| equalish(X0,e_2) ) ).
cnf(u48644,negated_conjecture,
( ~ group_element(X0)
| product(X0,e_3,e_3)
| product(X0,e_3,e_4)
| product(X0,e_3,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(u48695,negated_conjecture,
( ~ product(e_4,e_4,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)
| ~ group_element(X0) ) ).
cnf(e_4_is_not_e_3,axiom,
~ equalish(e_4,e_3) ).
cnf(u47005,negated_conjecture,
( ~ product(X0,X1,e_4)
| ~ product(e_1,X0,X1)
| equalish(X0,e_3) ) ).
cnf(u48287,negated_conjecture,
( ~ product(e_5,e_3,X0)
| ~ group_element(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(u48582,negated_conjecture,
( ~ group_element(X0)
| 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(u48584,negated_conjecture,
( ~ 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_3)
| product(X0,e_2,e_4) ) ).
cnf(e_3_is_not_e_5,axiom,
~ equalish(e_3,e_5) ).
cnf(u48208,negated_conjecture,
( ~ product(e_1,e_1,X0)
| ~ group_element(X0)
| product(e_1,X0,e_1)
| product(e_1,X0,e_3)
| product(e_1,X0,e_4)
| equalish(X0,e_3) ) ).
cnf(u47144,axiom,
( ~ product(X0,e_1,e_1)
| equalish(X0,e_1) ) ).
cnf(u47991,negated_conjecture,
( ~ product(e_3,e_3,X0)
| ~ product(e_4,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X1,e_3) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : GRP132-2.005 : TPTP v9.3.1. Released v1.2.0.
% 0.00/0.02 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.04/0.30 % Computer : n012.cluster.edu
% 0.04/0.30 % Model : x86_64 x86_64
% 0.04/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.04/0.30 % Memory : 8046.5625MB
% 0.04/0.30 % OS : Linux 6.8.0-71-generic
% 0.04/0.30 % CPULimit : 300
% 0.04/0.30 % WCLimit : 300
% 0.04/0.30 % DateTime : Sun Sep 27 09:30:34 UTC 2026
% 0.04/0.30 % CPUTime :
% 0.04/0.30 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.04/0.32 Running first-order theorem proving
% 0.04/0.32 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.54/1.29 % (2114033)Input is clausal, will run a generic CNF schedule.
% 4.54/1.29 % (2114038)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=1934715541:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 4.54/1.29 % (2114039)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1124622866:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 4.54/1.29 % (2114040)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=124364552:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 4.54/1.29 % (2114043)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3524403228:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 4.54/1.29 % (2114041)lrs+10_1_sil=8000:sp=occurrence:random_seed=970202835:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 4.54/1.29 % (2114044)dis-21_1_sil=8000:lcm=predicate:random_seed=3688589304: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.54/1.29 % (2114042)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=793265984:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 4.54/1.29 % (2114041)Instruction limit reached!
% 4.54/1.29 % (2114041)------------------------------
% 4.54/1.29 % (2114041)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.54/1.29 % (2114041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.54/1.29 % (2114041)CaDiCaL version: 2.1.3
% 4.54/1.29 % (2114041)Termination reason: Instruction limit
% 4.54/1.29 % (2114041)Termination phase: Saturation
% 4.54/1.29 % (2114041)Time elapsed: 0.028 s
% 4.54/1.29 % (2114041)Peak memory usage: 88 MB
% 4.54/1.29 % (2114041)Instructions burned: 109 (million)
% 4.54/1.29 % (2114042)Instruction limit reached!
% 4.54/1.29 % (2114042)------------------------------
% 4.54/1.29 % (2114042)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.54/1.29 % (2114042)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.54/1.29 % (2114042)CaDiCaL version: 2.1.3
% 4.54/1.29 % (2114042)Termination reason: Instruction limit
% 4.54/1.29 % (2114042)Termination phase: Saturation
% 4.54/1.29 % (2114042)Time elapsed: 0.030 s
% 4.54/1.29 % (2114042)Peak memory usage: 88 MB
% 4.54/1.29 % (2114042)Instructions burned: 115 (million)
% 4.54/1.29 % (2114044)Instruction limit reached!
% 4.54/1.29 % (2114044)------------------------------
% 4.54/1.29 % (2114044)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.54/1.29 % (2114044)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.54/1.29 % (2114044)CaDiCaL version: 2.1.3
% 4.54/1.29 % (2114044)Termination reason: Instruction limit
% 4.54/1.29 % (2114044)Termination phase: Saturation
% 4.54/1.29 % (2114044)Time elapsed: 0.034 s
% 4.54/1.29 % (2114044)Peak memory usage: 89 MB
% 4.54/1.29 % (2114044)Instructions burned: 118 (million)
% 4.54/1.29 % (2114043)Instruction limit reached!
% 4.54/1.29 % (2114043)------------------------------
% 4.54/1.29 % (2114043)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.54/1.29 % (2114043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.54/1.29 % (2114043)CaDiCaL version: 2.1.3
% 4.54/1.29 % (2114043)Termination reason: Instruction limit
% 4.54/1.29 % (2114043)Termination phase: Saturation
% 4.54/1.29 % (2114043)Time elapsed: 0.062 s
% 4.54/1.29 % (2114043)Peak memory usage: 89 MB
% 4.54/1.29 % (2114043)Instructions burned: 181 (million)
% 4.54/1.29 % (2114053)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=4072113912:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2998 on theBenchmark for (2998ds/189Mi)
% 4.54/1.29 % (2114053)Refutation not found, incomplete strategy
% 4.54/1.29 % (2114053)------------------------------
% 4.54/1.29 % (2114053)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.54/1.29 % (2114053)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.54/1.29 % (2114053)CaDiCaL version: 2.1.3
% 4.54/1.29 % (2114053)Termination reason: Refutation not found, incomplete strategy
% 4.54/1.29 % (2114053)Time elapsed: 0.001 s
% 4.54/1.29 % (2114053)Peak memory usage: 87 MB
% 4.54/1.29 % (2114053)Instructions burned: 2 (million)
% 7.22/1.79 % (2114052)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=3066085775:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 7.22/1.79 % (2114054)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1124809602:st=4:i=219:sd=3:ss=axioms_2998 on theBenchmark for (2998ds/219Mi)
% 7.22/1.79 % (2114055)lrs+10_64_to=lpo:sil=8000:random_seed=3312003420:i=126:bd=preordered_2998 on theBenchmark for (2998ds/126Mi)
% 7.22/1.79 % (2114052)Instruction limit reached!
% 7.22/1.79 % (2114052)------------------------------
% 7.22/1.79 % (2114052)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.22/1.79 % (2114052)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.22/1.79 % (2114052)CaDiCaL version: 2.1.3
% 7.22/1.79 % (2114052)Termination reason: Instruction limit
% 7.22/1.79 % (2114052)Termination phase: Saturation
% 7.22/1.79 % (2114052)Time elapsed: 0.038 s
% 7.22/1.79 % (2114052)Peak memory usage: 88 MB
% 7.22/1.79 % (2114052)Instructions burned: 146 (million)
% 7.22/1.79 % (2114054)Instruction limit reached!
% 7.22/1.79 % (2114054)------------------------------
% 7.22/1.79 % (2114054)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.22/1.79 % (2114054)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.22/1.79 % (2114054)CaDiCaL version: 2.1.3
% 7.22/1.79 % (2114054)Termination reason: Instruction limit
% 7.22/1.79 % (2114054)Termination phase: Saturation
% 7.22/1.79 % (2114054)Time elapsed: 0.060 s
% 7.22/1.79 % (2114054)Peak memory usage: 88 MB
% 7.22/1.79 % (2114054)Instructions burned: 220 (million)
% 7.22/1.79 % (2114055)Instruction limit reached!
% 7.22/1.79 % (2114055)------------------------------
% 7.22/1.79 % (2114055)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.22/1.79 % (2114055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.22/1.79 % (2114055)CaDiCaL version: 2.1.3
% 7.22/1.79 % (2114055)Termination reason: Instruction limit
% 7.22/1.79 % (2114055)Termination phase: Saturation
% 7.22/1.79 % (2114055)Time elapsed: 0.055 s
% 7.22/1.79 % (2114055)Peak memory usage: 88 MB
% 7.22/1.79 % (2114055)Instructions burned: 127 (million)
% 7.22/1.79 % (2114060)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=4194022137:avsq=on:i=194:fgj=on:bd=preordered_2997 on theBenchmark for (2997ds/194Mi)
% 7.22/1.79 % (2114053)------------------------------
% 7.22/1.79 % (2114053)------------------------------
% 7.22/1.79 % (2114061)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=2487294567:i=157:gtg=all_2997 on theBenchmark for (2997ds/157Mi)
% 7.22/1.79 % (2114062)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1748748438:i=3394:sd=4:ss=included:sgt=64_2996 on theBenchmark for (2996ds/3394Mi)
% 7.22/1.79 % (2114061)Instruction limit reached!
% 7.22/1.79 % (2114061)------------------------------
% 7.22/1.79 % (2114061)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.22/1.79 % (2114061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.22/1.79 % (2114061)CaDiCaL version: 2.1.3
% 7.22/1.79 % (2114061)Termination reason: Instruction limit
% 7.22/1.79 % (2114061)Termination phase: Saturation
% 7.22/1.79 % (2114061)Time elapsed: 0.040 s
% 7.22/1.79 % (2114061)Peak memory usage: 88 MB
% 7.22/1.79 % (2114061)Instructions burned: 158 (million)
% 7.22/1.79 % (2114060)Instruction limit reached!
% 7.22/1.79 % (2114060)------------------------------
% 7.22/1.79 % (2114060)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.22/1.79 % (2114060)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.22/1.79 % (2114060)CaDiCaL version: 2.1.3
% 7.22/1.79 % (2114060)Termination reason: Instruction limit
% 7.22/1.79 % (2114060)Termination phase: Saturation
% 7.22/1.79 % (2114060)Time elapsed: 0.065 s
% 7.22/1.79 % (2114060)Peak memory usage: 88 MB
% 7.22/1.79 % (2114060)Instructions burned: 197 (million)
% 7.22/1.79 % (2114039)Refutation not found, incomplete strategy
% 7.22/1.79 % (2114039)------------------------------
% 7.22/1.79 % (2114039)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.22/1.79 % (2114039)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.22/1.79 % (2114039)CaDiCaL version: 2.1.3
% 7.22/1.79 % (2114039)Termination reason: Refutation not found, incomplete strategy
% 7.22/1.79 % (2114039)Time elapsed: 0.342 s
% 7.22/1.79 % (2114039)Peak memory usage: 127 MB
% 7.22/1.79 % (2114039)Instructions burned: 906 (million)
% 13.14/2.45 % (2114064)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=4227830961:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2996 on theBenchmark for (2996ds/106Mi)
% 13.14/2.45 % (2114064)Refutation not found, incomplete strategy
% 13.14/2.45 % (2114064)------------------------------
% 13.14/2.45 % (2114064)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.14/2.45 % (2114064)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.14/2.45 % (2114064)CaDiCaL version: 2.1.3
% 13.14/2.45 % (2114064)Termination reason: Refutation not found, incomplete strategy
% 13.14/2.45 % (2114064)Time elapsed: 0.001 s
% 13.14/2.45 % (2114064)Peak memory usage: 87 MB
% 13.14/2.45 % (2114064)Instructions burned: 2 (million)
% 13.14/2.45 % (2114068)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=1959235880:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2995 on theBenchmark for (2995ds/242Mi)
% 13.14/2.45 % (2114067)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1401533333:i=107_2995 on theBenchmark for (2995ds/107Mi)
% 13.14/2.45 % (2114067)Instruction limit reached!
% 13.14/2.45 % (2114067)------------------------------
% 13.14/2.45 % (2114067)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.14/2.45 % (2114067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.14/2.45 % (2114067)CaDiCaL version: 2.1.3
% 13.14/2.45 % (2114067)Termination reason: Instruction limit
% 13.14/2.45 % (2114067)Termination phase: Saturation
% 13.14/2.45 % (2114067)Time elapsed: 0.026 s
% 13.14/2.45 % (2114067)Peak memory usage: 87 MB
% 13.14/2.45 % (2114067)Instructions burned: 107 (million)
% 13.14/2.45 % (2114068)Instruction limit reached!
% 13.14/2.45 % (2114068)------------------------------
% 13.14/2.45 % (2114068)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.14/2.45 % (2114068)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.14/2.45 % (2114068)CaDiCaL version: 2.1.3
% 13.14/2.45 % (2114068)Termination reason: Instruction limit
% 13.14/2.45 % (2114068)Termination phase: Saturation
% 13.14/2.45 % (2114068)Time elapsed: 0.064 s
% 13.14/2.45 % (2114068)Peak memory usage: 88 MB
% 13.14/2.45 % (2114068)Instructions burned: 243 (million)
% 13.14/2.45 % (2114039)------------------------------
% 13.14/2.45 % (2114039)------------------------------
% 13.14/2.45 % (2114064)------------------------------
% 13.14/2.45 % (2114064)------------------------------
% 13.14/2.45 % (2114072)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=1863257814:cond=fast:i=5208:av=off_2994 on theBenchmark for (2994ds/5208Mi)
% 13.14/2.45 % (2114073)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=2928000449:i=134:sd=2:doe=on:ss=axioms:sgt=14_2994 on theBenchmark for (2994ds/134Mi)
% 13.14/2.45 % (2114074)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=532677359:i=499:bd=all_2994 on theBenchmark for (2994ds/499Mi)
% 13.14/2.45 % (2114073)Instruction limit reached!
% 13.14/2.45 % (2114073)------------------------------
% 13.14/2.45 % (2114073)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.14/2.45 % (2114073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.14/2.45 % (2114073)CaDiCaL version: 2.1.3
% 13.14/2.45 % (2114073)Termination reason: Instruction limit
% 13.14/2.45 % (2114073)Termination phase: Saturation
% 13.14/2.45 % (2114073)Time elapsed: 0.044 s
% 13.14/2.45 % (2114073)Peak memory usage: 89 MB
% 13.14/2.45 % (2114073)Instructions burned: 134 (million)
% 13.14/2.45 % (2114075)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=2416253064:i=191:fgj=on:bd=all_2993 on theBenchmark for (2993ds/191Mi)
% 13.14/2.45 % (2114075)Instruction limit reached!
% 13.14/2.45 % (2114075)------------------------------
% 13.14/2.45 % (2114075)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.14/2.45 % (2114075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.14/2.45 % (2114075)CaDiCaL version: 2.1.3
% 13.14/2.45 % (2114075)Termination reason: Instruction limit
% 13.14/2.45 % (2114075)Termination phase: Saturation
% 13.14/2.45 % (2114075)Time elapsed: 0.058 s
% 13.14/2.45 % (2114075)Peak memory usage: 88 MB
% 13.14/2.45 % (2114075)Instructions burned: 192 (million)
% 19.50/3.39 % (2114080)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=4021291991:i=264:kws=precedence:fsr=off_2992 on theBenchmark for (2992ds/264Mi)
% 19.50/3.39 % (2114074)Instruction limit reached!
% 19.50/3.39 % (2114074)------------------------------
% 19.50/3.39 % (2114074)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.50/3.39 % (2114074)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.50/3.39 % (2114074)CaDiCaL version: 2.1.3
% 19.50/3.39 % (2114074)Termination reason: Instruction limit
% 19.50/3.39 % (2114074)Termination phase: Saturation
% 19.50/3.39 % (2114074)Time elapsed: 0.130 s
% 19.50/3.39 % (2114074)Peak memory usage: 89 MB
% 19.50/3.39 % (2114074)Instructions burned: 503 (million)
% 19.50/3.39 % (2114080)Instruction limit reached!
% 19.50/3.39 % (2114080)------------------------------
% 19.50/3.39 % (2114080)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.50/3.39 % (2114080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.50/3.39 % (2114081)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=510315144:cond=on:i=156:bs=on:gtg=exists_all:er=known_2992 on theBenchmark for (2992ds/156Mi)
% 19.50/3.39 % (2114080)CaDiCaL version: 2.1.3
% 19.50/3.39 % (2114080)Termination reason: Instruction limit
% 19.50/3.39 % (2114080)Termination phase: Saturation
% 19.50/3.39 % (2114080)Time elapsed: 0.070 s
% 19.50/3.39 % (2114080)Peak memory usage: 89 MB
% 19.50/3.39 % (2114080)Instructions burned: 267 (million)
% 19.50/3.39 % (2114083)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=2835375866:i=3256:kws=precedence:bd=preordered:av=off_2991 on theBenchmark for (2991ds/3256Mi)
% 19.50/3.39 % (2114081)Instruction limit reached!
% 19.50/3.39 % (2114081)------------------------------
% 19.50/3.39 % (2114081)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.50/3.39 % (2114081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.50/3.39 % (2114081)CaDiCaL version: 2.1.3
% 19.50/3.39 % (2114081)Termination reason: Instruction limit
% 19.50/3.39 % (2114081)Termination phase: Saturation
% 19.50/3.39 % (2114081)Time elapsed: 0.046 s
% 19.50/3.39 % (2114081)Peak memory usage: 88 MB
% 19.50/3.39 % (2114081)Instructions burned: 156 (million)
% 19.50/3.39 % (2114085)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=1290879410:i=537:av=off:ss=included_2991 on theBenchmark for (2991ds/537Mi)
% 19.50/3.39 % (2114087)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=1498434965:i=180:bd=preordered:av=off_2990 on theBenchmark for (2990ds/180Mi)
% 19.50/3.39 % (2114087)Instruction limit reached!
% 19.50/3.39 % (2114087)------------------------------
% 19.50/3.39 % (2114087)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.50/3.39 % (2114087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.50/3.39 % (2114087)CaDiCaL version: 2.1.3
% 19.50/3.39 % (2114087)Termination reason: Instruction limit
% 19.50/3.39 % (2114087)Termination phase: Saturation
% 19.50/3.39 % (2114087)Time elapsed: 0.050 s
% 19.50/3.39 % (2114087)Peak memory usage: 87 MB
% 19.50/3.39 % (2114087)Instructions burned: 183 (million)
% 19.50/3.39 % (2114085)Instruction limit reached!
% 19.50/3.39 % (2114085)------------------------------
% 19.50/3.39 % (2114085)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.50/3.39 % (2114085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.50/3.39 % (2114085)CaDiCaL version: 2.1.3
% 19.50/3.39 % (2114085)Termination reason: Instruction limit
% 19.50/3.39 % (2114085)Termination phase: Saturation
% 19.50/3.39 % (2114085)Time elapsed: 0.119 s
% 19.50/3.39 % (2114085)Peak memory usage: 88 MB
% 19.50/3.39 % (2114085)Instructions burned: 540 (million)
% 19.50/3.39 % (2114090)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=1779032828:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2989 on theBenchmark for (2989ds/10307Mi)
% 19.50/3.39 % (2114091)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=1916311922:i=412:gtgl=4:gtg=exists_all_2989 on theBenchmark for (2989ds/412Mi)
% 19.50/3.39 % (2114091)Instruction limit reached!
% 19.50/3.39 % (2114091)------------------------------
% 19.50/3.39 % (2114091)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.85/4.57 % (2114091)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.85/4.57 % (2114091)CaDiCaL version: 2.1.3
% 27.85/4.57 % (2114091)Termination reason: Instruction limit
% 27.85/4.57 % (2114091)Termination phase: Saturation
% 27.85/4.57 % (2114091)Time elapsed: 0.099 s
% 27.85/4.57 % (2114091)Peak memory usage: 90 MB
% 27.85/4.57 % (2114091)Instructions burned: 415 (million)
% 27.85/4.57 % (2114094)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=2744417761:s2pl=no:i=8478:s2at=4:nm=6_2987 on theBenchmark for (2987ds/8478Mi)
% 27.85/4.57 % (2114062)Instruction limit reached!
% 27.85/4.57 % (2114062)------------------------------
% 27.85/4.57 % (2114062)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.85/4.57 % (2114062)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.85/4.57 % (2114062)CaDiCaL version: 2.1.3
% 27.85/4.57 % (2114062)Termination reason: Instruction limit
% 27.85/4.57 % (2114062)Termination phase: Saturation
% 27.85/4.57 % (2114062)Time elapsed: 1.152 s
% 27.85/4.57 % (2114062)Peak memory usage: 137 MB
% 27.85/4.57 % (2114062)Instructions burned: 3396 (million)
% 27.85/4.57 % (2114096)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=550345634:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2984 on theBenchmark for (2984ds/303Mi)
% 27.85/4.57 % (2114094)Refutation not found, incomplete strategy
% 27.85/4.57 % (2114094)------------------------------
% 27.85/4.57 % (2114094)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.85/4.57 % (2114094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.85/4.57 % (2114094)CaDiCaL version: 2.1.3
% 27.85/4.57 % (2114094)Termination reason: Refutation not found, incomplete strategy
% 27.85/4.57 % (2114094)Time elapsed: 0.326 s
% 27.85/4.57 % (2114094)Peak memory usage: 127 MB
% 27.85/4.57 % (2114094)Instructions burned: 906 (million)
% 27.85/4.57 % (2114096)Instruction limit reached!
% 27.85/4.57 % (2114096)------------------------------
% 27.85/4.57 % (2114096)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.85/4.57 % (2114096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.85/4.57 % (2114096)CaDiCaL version: 2.1.3
% 27.85/4.57 % (2114096)Termination reason: Instruction limit
% 27.85/4.57 % (2114096)Termination phase: Saturation
% 27.85/4.57 % (2114096)Time elapsed: 0.094 s
% 27.85/4.57 % (2114096)Peak memory usage: 90 MB
% 27.85/4.57 % (2114096)Instructions burned: 306 (million)
% 27.85/4.57 % (2114098)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=2194330389:st=4:i=720:sd=3:fsr=off:ss=axioms_2982 on theBenchmark for (2982ds/720Mi)
% 27.85/4.57 % (2114098)Refutation not found, incomplete strategy
% 27.85/4.57 % (2114098)------------------------------
% 27.85/4.57 % (2114098)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.85/4.57 % (2114098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.85/4.57 % (2114098)CaDiCaL version: 2.1.3
% 27.85/4.57 % (2114098)Termination reason: Refutation not found, incomplete strategy
% 27.85/4.57 % (2114098)Time elapsed: 0.001 s
% 27.85/4.57 % (2114098)Peak memory usage: 87 MB
% 27.85/4.57 % (2114098)Instructions burned: 1 (million)
% 27.85/4.57 % (2114094)------------------------------
% 27.85/4.57 % (2114094)------------------------------
% 27.85/4.57 % (2114083)Instruction limit reached!
% 27.85/4.57 % (2114083)------------------------------
% 27.85/4.57 % (2114083)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 27.85/4.57 % (2114083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 27.85/4.57 % (2114083)CaDiCaL version: 2.1.3
% 27.85/4.57 % (2114083)Termination reason: Instruction limit
% 27.85/4.57 % (2114083)Termination phase: Saturation
% 27.85/4.57 % (2114083)Time elapsed: 1.003 s
% 27.85/4.57 % (2114083)Peak memory usage: 133 MB
% 27.85/4.57 % (2114083)Instructions burned: 3259 (million)
% 27.85/4.57 % (2114100)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=4153405676:i=598:bs=on:bd=preordered:av=off:ss=axioms_2981 on theBenchmark for (2981ds/598Mi)
% 27.85/4.57 % (2114100)Refutation not found, incomplete strategy
% 27.85/4.57 % (2114100)------------------------------
% 27.85/4.57 % (2114100)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.24/6.61 % (2114100)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.24/6.61 % (2114100)CaDiCaL version: 2.1.3
% 42.24/6.61 % (2114100)Termination reason: Refutation not found, incomplete strategy
% 42.24/6.61 % (2114100)Time elapsed: 0.0000 s
% 42.24/6.61 % (2114100)Peak memory usage: 86 MB
% 42.24/6.61 % (2114098)------------------------------
% 42.24/6.61 % (2114098)------------------------------
% 42.24/6.61 % (2114101)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=1585909181:i=2989:sd=3:ss=axioms:sgt=60_2980 on theBenchmark for (2980ds/2989Mi)
% 42.24/6.61 % (2114103)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=1650669983:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2980 on theBenchmark for (2980ds/1997Mi)
% 42.24/6.61 % (2114100)------------------------------
% 42.24/6.61 % (2114100)------------------------------
% 42.24/6.61 % (2114106)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=263030968:i=2088:bd=preordered:av=off_2979 on theBenchmark for (2979ds/2088Mi)
% 42.24/6.61 % (2114072)Instruction limit reached!
% 42.24/6.61 % (2114072)------------------------------
% 42.24/6.61 % (2114072)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.24/6.61 % (2114072)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.24/6.61 % (2114072)CaDiCaL version: 2.1.3
% 42.24/6.61 % (2114072)Termination reason: Instruction limit
% 42.24/6.61 % (2114072)Termination phase: Saturation
% 42.24/6.61 % (2114072)Time elapsed: 1.588 s
% 42.24/6.61 % (2114072)Peak memory usage: 137 MB
% 42.24/6.61 % (2114072)Instructions burned: 5209 (million)
% 42.24/6.61 % (2114108)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=1943058929:i=1098:nicw=on_2977 on theBenchmark for (2977ds/1098Mi)
% 42.24/6.61 % (2114108)Instruction limit reached!
% 42.24/6.61 % (2114108)------------------------------
% 42.24/6.61 % (2114108)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.24/6.61 % (2114108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.24/6.61 % (2114108)CaDiCaL version: 2.1.3
% 42.24/6.61 % (2114108)Termination reason: Instruction limit
% 42.24/6.61 % (2114108)Termination phase: Saturation
% 42.24/6.61 % (2114108)Time elapsed: 0.295 s
% 42.24/6.61 % (2114108)Peak memory usage: 90 MB
% 42.24/6.61 % (2114108)Instructions burned: 1101 (million)
% 42.24/6.61 % (2114110)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=3332163089:i=433:bd=preordered_2973 on theBenchmark for (2973ds/433Mi)
% 42.24/6.61 % (2114103)Instruction limit reached!
% 42.24/6.61 % (2114103)------------------------------
% 42.24/6.61 % (2114103)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.24/6.61 % (2114103)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.24/6.61 % (2114103)CaDiCaL version: 2.1.3
% 42.24/6.61 % (2114103)Termination reason: Instruction limit
% 42.24/6.61 % (2114103)Termination phase: Saturation
% 42.24/6.61 % (2114103)Time elapsed: 0.705 s
% 42.24/6.61 % (2114103)Peak memory usage: 133 MB
% 42.24/6.61 % (2114103)Instructions burned: 1999 (million)
% 42.24/6.61 % (2114106)Instruction limit reached!
% 42.24/6.61 % (2114106)------------------------------
% 42.24/6.61 % (2114106)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.24/6.61 % (2114106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.24/6.61 % (2114106)CaDiCaL version: 2.1.3
% 42.24/6.61 % (2114106)Termination reason: Instruction limit
% 42.24/6.61 % (2114106)Termination phase: Saturation
% 42.24/6.61 % (2114106)Time elapsed: 0.662 s
% 42.24/6.61 % (2114106)Peak memory usage: 131 MB
% 42.24/6.61 % (2114106)Instructions burned: 2088 (million)
% 42.24/6.61 % (2114110)Instruction limit reached!
% 42.24/6.61 % (2114110)------------------------------
% 42.24/6.61 % (2114110)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.24/6.61 % (2114110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.24/6.61 % (2114110)CaDiCaL version: 2.1.3
% 42.24/6.61 % (2114110)Termination reason: Instruction limit
% 42.24/6.61 % (2114110)Termination phase: Saturation
% 42.24/6.61 % (2114110)Time elapsed: 0.128 s
% 42.24/6.61 % (2114110)Peak memory usage: 89 MB
% 42.24/6.61 % (2114110)Instructions burned: 433 (million)
% 42.24/6.61 % (2114112)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=1571171935:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2972 on theBenchmark for (2972ds/2942Mi)
% 35.52/7.51 % (2114114)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=343525425:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2971 on theBenchmark for (2971ds/596Mi)
% 35.52/7.51 % (2114113)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=76010551:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2971 on theBenchmark for (2971ds/6922Mi)
% 35.52/7.51 % (2114114)Refutation not found, incomplete strategy
% 35.52/7.51 % (2114114)------------------------------
% 35.52/7.51 % (2114114)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.52/7.51 % (2114114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.52/7.51 % (2114114)CaDiCaL version: 2.1.3
% 35.52/7.51 % (2114114)Termination reason: Refutation not found, incomplete strategy
% 35.52/7.51 % (2114114)Time elapsed: 0.001 s
% 35.52/7.51 % (2114114)Peak memory usage: 87 MB
% 35.52/7.51 % (2114114)Instructions burned: 2 (million)
% 35.52/7.51 % (2114114)------------------------------
% 35.52/7.51 % (2114114)------------------------------
% 35.52/7.51 % (2114101)Instruction limit reached!
% 35.52/7.51 % (2114101)------------------------------
% 35.52/7.51 % (2114101)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.52/7.51 % (2114101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.52/7.51 % (2114101)CaDiCaL version: 2.1.3
% 35.52/7.51 % (2114101)Termination reason: Instruction limit
% 35.52/7.51 % (2114101)Termination phase: Saturation
% 35.52/7.51 % (2114101)Time elapsed: 1.085 s
% 35.52/7.51 % (2114101)Peak memory usage: 140 MB
% 35.52/7.51 % (2114101)Instructions burned: 2990 (million)
% 35.52/7.51 % (2114118)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=1307373141:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2969 on theBenchmark for (2969ds/4123Mi)
% 35.52/7.51 % (2114119)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=269432385:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2968 on theBenchmark for (2968ds/16411Mi)
% 35.52/7.51 % (2114113)Refutation not found, incomplete strategy
% 35.52/7.51 % (2114113)------------------------------
% 35.52/7.51 % (2114113)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.52/7.51 % (2114113)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.52/7.51 % (2114113)CaDiCaL version: 2.1.3
% 35.52/7.51 % (2114113)Termination reason: Refutation not found, incomplete strategy
% 35.52/7.51 % (2114113)Time elapsed: 0.334 s
% 35.52/7.51 % (2114113)Peak memory usage: 127 MB
% 35.52/7.51 % (2114113)Instructions burned: 907 (million)
% 35.52/7.51 % (2114113)------------------------------
% 35.52/7.51 % (2114113)------------------------------
% 35.52/7.51 % (2114122)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=2857276005:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2965 on theBenchmark for (2965ds/1670Mi)
% 35.52/7.51 % (2114112)Instruction limit reached!
% 35.52/7.51 % (2114112)------------------------------
% 35.52/7.51 % (2114112)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.52/7.51 % (2114112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.52/7.51 % (2114112)CaDiCaL version: 2.1.3
% 35.52/7.51 % (2114112)Termination reason: Instruction limit
% 35.52/7.51 % (2114112)Termination phase: Saturation
% 35.52/7.51 % (2114112)Time elapsed: 0.896 s
% 35.52/7.51 % (2114112)Peak memory usage: 134 MB
% 35.52/7.51 % (2114112)Instructions burned: 2942 (million)
% 35.52/7.51 % (2114124)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:prc=on:drc=off:fde=unused:sp=reverse_frequency:updr=off:random_seed=800740244:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2962 on theBenchmark for (2962ds/1722Mi)
% 35.52/7.51 % (2114122)Instruction limit reached!
% 35.52/7.51 % (2114122)------------------------------
% 35.52/7.51 % (2114122)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.52/7.51 % (2114122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.52/7.51 % (2114122)CaDiCaL version: 2.1.3
% 35.52/7.51 % (2114122)Termination reason: Instruction limit
% 35.52/7.51 % (2114122)Termination phase: Saturation
% 35.52/7.51 % (2114122)Time elapsed: 0.528 s
% 35.52/7.51 % (2114122)Peak memory usage: 132 MB
% 35.52/7.51 % (2114122)Instructions burned: 1671 (million)
% 35.52/7.51 % (2114126)ott-1004_1_anc=all_dependent:to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:sas=cadical:sp=const_frequency:acc=on:urr=ec_only:gs=on:s2agt=40:alpa=false:sac=on:random_seed=1381665839:cts=off:cond=on:i=9530:bs=on:fsd=on_2959 on theBenchmark for (2959ds/9530Mi)
% 35.52/7.51 % (2114118)Instruction limit reached!
% 35.52/7.51 % (2114118)------------------------------
% 35.52/7.51 % (2114118)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.52/7.51 % (2114118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.52/7.51 % (2114118)CaDiCaL version: 2.1.3
% 35.52/7.51 % (2114118)Termination reason: Instruction limit
% 35.52/7.51 % (2114118)Termination phase: Saturation
% 35.52/7.51 % (2114118)Time elapsed: 1.264 s
% 35.52/7.51 % (2114118)Peak memory usage: 136 MB
% 35.52/7.51 % (2114118)Instructions burned: 4126 (million)
% 35.52/7.51 % (2114124)Instruction limit reached!
% 35.52/7.51 % (2114124)------------------------------
% 35.52/7.51 % (2114124)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.52/7.51 % (2114124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.52/7.51 % (2114124)CaDiCaL version: 2.1.3
% 35.52/7.51 % (2114124)Termination reason: Instruction limit
% 35.52/7.51 % (2114124)Termination phase: Saturation
% 35.52/7.51 % (2114124)Time elapsed: 0.644 s
% 35.52/7.51 % (2114124)Peak memory usage: 133 MB
% 35.52/7.51 % (2114124)Instructions burned: 1723 (million)
% 35.52/7.51 % (2114128)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=1371384900:st=2:i=4495:sd=10:ss=included_2955 on theBenchmark for (2955ds/4495Mi)
% 35.52/7.51 % (2114129)lrs+1002_1_sfv=off:ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=reverse_arity:spb=non_intro:s2agt=16:random_seed=3602901979:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2954 on theBenchmark for (2954ds/4920Mi)
% 35.52/7.51 % (2114090)Instruction limit reached!
% 35.52/7.51 % (2114090)------------------------------
% 35.52/7.51 % (2114090)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.52/7.51 % (2114090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.52/7.51 % (2114090)CaDiCaL version: 2.1.3
% 35.52/7.51 % (2114090)Termination reason: Instruction limit
% 35.52/7.51 % (2114090)Termination phase: Saturation
% 35.52/7.51 % (2114090)Time elapsed: 3.514 s
% 35.52/7.51 % (2114090)Peak memory usage: 158 MB
% 35.52/7.51 % (2114090)Instructions burned: 10307 (million)
% 35.52/7.51 % (2114132)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:lcm=reverse:bce=on:bsr=unit_only:random_seed=1532751176:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2953 on theBenchmark for (2953ds/2083Mi)
% 35.52/7.51 % (2114132)Instruction limit reached!
% 35.52/7.51 % (2114132)------------------------------
% 35.52/7.51 % (2114132)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.52/7.51 % (2114132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.52/7.51 % (2114132)CaDiCaL version: 2.1.3
% 35.52/7.51 % (2114132)Termination reason: Instruction limit
% 35.52/7.51 % (2114132)Termination phase: Saturation
% 35.52/7.51 % (2114132)Time elapsed: 0.600 s
% 35.52/7.51 % (2114132)Peak memory usage: 130 MB
% 35.52/7.51 % (2114132)Instructions burned: 2087 (million)
% 35.52/7.51 % (2114134)lrs+31_1_to=lpo:ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=weighted_frequency:sos=all:spb=units:lcm=predicate:bsr=on:gs=on:random_seed=3901525473:i=4629:av=off:gsp=on_2946 on theBenchmark for (2946ds/4629Mi)
% 35.52/7.51 % (2114129)Instruction limit reached!
% 35.52/7.51 % (2114129)------------------------------
% 35.52/7.51 % (2114129)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.52/7.51 % (2114129)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.52/7.51 % (2114129)CaDiCaL version: 2.1.3
% 35.52/7.51 % (2114129)Termination reason: Instruction limit
% 35.52/7.51 % (2114129)Termination phase: Saturation
% 35.52/7.51 % (2114129)Time elapsed: 1.428 s
% 35.52/7.51 % (2114129)Peak memory usage: 145 MB
% 35.52/7.51 % (2114129)Instructions burned: 4920 (million)
% 35.52/7.51 % (2114128)Instruction limit reached!
% 35.52/7.51 % (2114128)------------------------------
% 35.52/7.51 % (2114128)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.52/7.51 % (2114128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.52/7.51 % (2114128)CaDiCaL version: 2.1.3
% 35.52/7.51 % (2114128)Termination reason: Instruction limit
% 35.52/7.51 % (2114128)Termination phase: Saturation
% 35.52/7.51 % (2114128)Time elapsed: 1.566 s
% 35.52/7.51 % (2114128)Peak memory usage: 143 MB
% 35.52/7.51 % (2114128)Instructions burned: 4495 (million)
% 35.52/7.51 % (2114136)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=345525680:i=1258:av=off_2939 on theBenchmark for (2939ds/1258Mi)
% 35.52/7.51 % (2114137)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=3944244032:i=7343:av=off:ss=included_2938 on theBenchmark for (2938ds/7343Mi)
% 35.52/7.51 % (2114119)First to succeed.
% 35.52/7.51 % (2114119)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2114033"
% 35.52/7.51 % (2114134)Refutation not found, incomplete strategy
% 35.52/7.51 % (2114134)------------------------------
% 35.52/7.51 % (2114134)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.52/7.51 % (2114134)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.52/7.51 % (2114134)CaDiCaL version: 2.1.3
% 35.52/7.51 % (2114134)Termination reason: Refutation not found, incomplete strategy
% 35.52/7.51 % (2114134)Time elapsed: 0.894 s
% 35.52/7.51 % (2114134)Peak memory usage: 128 MB
% 35.52/7.51 % (2114134)Instructions burned: 942 (million)
% 35.52/7.51 % SZS status Satisfiable for theBenchmark
% 35.52/7.51 % SZS output start Saturation.
% See solution above
% 44.81/7.62 % SZS output start Definitions and Model Updates.
% 44.81/7.62 % SZS output end Definitions and Model Updates.
% 44.81/7.62 % (2114119)------------------------------
% 44.81/7.62 % (2114119)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.81/7.62 % (2114119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.81/7.62 % (2114119)CaDiCaL version: 2.1.3
% 44.81/7.62 % (2114119)Termination reason: Satisfiable
% 44.81/7.62 % (2114119)Time elapsed: 3.042 s
% 44.81/7.62 % (2114119)Peak memory usage: 165 MB
% 44.81/7.62 % (2114119)Instructions burned: 7522 (million)
% 44.81/7.62 % (2114119)------------------------------
% 44.81/7.62 % (2114119)------------------------------
% 44.81/7.62 % (2114033)Success in time 6.992 s
% 44.81/7.62 % Vampire exiting
%------------------------------------------------------------------------------