%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP131-2.005 : TPTP v9.3.1. Released v1.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n026.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:01 AM UTC 2026
% Result : Satisfiable 72.30s 11.55s
% Output : Saturation 73.22s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u68,axiom,
equalish(e_5,e_5) ).
cnf(u80,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(u113,axiom,
product(e_1,e_1,e_2) ).
cnf(u116,axiom,
~ product(e_1,e_1,e_1) ).
cnf(u158,negated_conjecture,
product(e_3,e_1,e_4) ).
cnf(u161,negated_conjecture,
~ product(e_3,e_1,e_3) ).
cnf(u165,negated_conjecture,
~ product(e_3,e_1,e_2) ).
cnf(u169,negated_conjecture,
~ product(e_3,e_1,e_1) ).
cnf(u219,negated_conjecture,
~ product(e_2,e_1,e_4) ).
cnf(u224,negated_conjecture,
product(e_2,e_1,e_3) ).
cnf(u227,negated_conjecture,
~ product(e_2,e_1,e_2) ).
cnf(u231,negated_conjecture,
~ product(e_2,e_1,e_1) ).
cnf(u334,negated_conjecture,
~ product(e_5,e_5,e_4) ).
cnf(u338,negated_conjecture,
~ product(e_5,e_5,e_3) ).
cnf(u343,negated_conjecture,
product(e_5,e_5,e_2) ).
cnf(u346,negated_conjecture,
~ product(e_5,e_5,e_1) ).
cnf(u354,negated_conjecture,
~ product(e_5,e_4,e_4) ).
cnf(u358,negated_conjecture,
~ product(e_5,e_4,e_3) ).
cnf(u362,negated_conjecture,
~ product(e_5,e_4,e_2) ).
cnf(u366,negated_conjecture,
~ product(e_5,e_4,e_1) ).
cnf(u370,negated_conjecture,
( ~ group_element(X1)
| ~ group_element(X0)
| product(X0,X2,e_4)
| product(X0,X2,e_3)
| product(X0,X2,e_2)
| product(X0,X2,e_1)
| ~ group_element(X2)
| equalish(X0,e_5)
| product(X1,e_4,e_4)
| product(X1,e_4,e_3)
| product(X1,e_4,e_2)
| product(X1,e_4,e_1)
| ~ product(X1,X2,X0) ) ).
cnf(u375,negated_conjecture,
product(e_5,e_3,e_4) ).
cnf(u378,negated_conjecture,
~ product(e_5,e_3,e_3) ).
cnf(u382,negated_conjecture,
~ product(e_5,e_3,e_2) ).
cnf(u386,negated_conjecture,
~ product(e_5,e_3,e_1) ).
cnf(u394,negated_conjecture,
~ product(e_5,e_2,e_4) ).
cnf(u399,negated_conjecture,
product(e_5,e_2,e_3) ).
cnf(u402,negated_conjecture,
~ product(e_5,e_2,e_2) ).
cnf(u406,negated_conjecture,
~ product(e_5,e_2,e_1) ).
cnf(u414,negated_conjecture,
~ product(e_5,e_1,e_4) ).
cnf(u418,negated_conjecture,
~ product(e_5,e_1,e_3) ).
cnf(u422,negated_conjecture,
~ product(e_5,e_1,e_2) ).
cnf(u427,negated_conjecture,
product(e_5,e_1,e_1) ).
cnf(u452,negated_conjecture,
~ product(e_3,e_5,e_4) ).
cnf(u456,negated_conjecture,
~ product(e_3,e_5,e_3) ).
cnf(u460,negated_conjecture,
~ product(e_3,e_5,e_2) ).
cnf(u464,negated_conjecture,
~ product(e_3,e_5,e_1) ).
cnf(u760,negated_conjecture,
~ product(e_1,e_4,e_4) ).
cnf(u764,negated_conjecture,
~ product(e_1,e_4,e_3) ).
cnf(u768,negated_conjecture,
~ product(e_1,e_4,e_2) ).
cnf(u773,negated_conjecture,
product(e_1,e_4,e_1) ).
cnf(u993,negated_conjecture,
~ product(e_1,e_3,e_4) ).
cnf(u997,negated_conjecture,
~ product(e_1,e_3,e_3) ).
cnf(u1001,negated_conjecture,
~ product(e_1,e_3,e_1) ).
cnf(u1033,negated_conjecture,
~ product(e_4,e_2,e_3) ).
cnf(u1038,negated_conjecture,
product(e_4,e_2,e_2) ).
cnf(u1041,negated_conjecture,
~ product(e_4,e_2,e_1) ).
cnf(u1060,negated_conjecture,
~ product(e_1,e_2,e_3) ).
cnf(u1064,negated_conjecture,
~ product(e_1,e_2,e_2) ).
cnf(u1068,negated_conjecture,
~ product(e_1,e_2,e_1) ).
cnf(u1089,negated_conjecture,
~ product(e_3,e_2,e_3) ).
cnf(u1093,negated_conjecture,
~ product(e_3,e_2,e_2) ).
cnf(u1098,negated_conjecture,
product(e_3,e_2,e_1) ).
cnf(u1159,negated_conjecture,
~ product(e_2,e_4,e_4) ).
cnf(u1164,negated_conjecture,
product(e_2,e_4,e_2) ).
cnf(u1167,negated_conjecture,
~ product(e_2,e_4,e_1) ).
cnf(u1262,negated_conjecture,
product(e_2,e_5,e_4) ).
cnf(u1265,negated_conjecture,
~ product(e_2,e_5,e_3) ).
cnf(u1269,negated_conjecture,
~ product(e_2,e_5,e_2) ).
cnf(u1273,negated_conjecture,
~ product(e_2,e_5,e_1) ).
cnf(u1414,negated_conjecture,
~ product(e_4,e_5,e_4) ).
cnf(u1419,negated_conjecture,
product(e_4,e_5,e_1) ).
cnf(u1454,negated_conjecture,
product(e_1,e_5,e_3) ).
cnf(u1457,negated_conjecture,
~ product(e_1,e_5,e_2) ).
cnf(u1461,negated_conjecture,
~ product(e_1,e_5,e_1) ).
cnf(u1548,negated_conjecture,
~ product(e_4,e_3,e_4) ).
cnf(u1553,negated_conjecture,
product(e_4,e_3,e_3) ).
cnf(u1556,negated_conjecture,
~ product(e_4,e_3,e_2) ).
cnf(u1564,negated_conjecture,
~ product(e_4,e_3,e_1) ).
cnf(u1600,negated_conjecture,
~ product(e_3,e_3,e_4) ).
cnf(u1604,negated_conjecture,
~ product(e_3,e_3,e_3) ).
cnf(u1609,negated_conjecture,
product(e_3,e_3,e_2) ).
cnf(u1641,negated_conjecture,
product(e_2,e_3,e_1) ).
cnf(u1644,negated_conjecture,
~ product(e_2,e_3,e_2) ).
cnf(u1648,negated_conjecture,
~ product(e_2,e_3,e_3) ).
cnf(u1652,negated_conjecture,
~ product(e_2,e_3,e_4) ).
cnf(u1898,negated_conjecture,
~ product(e_2,e_2,e_1) ).
cnf(u1902,negated_conjecture,
~ product(e_2,e_2,e_2) ).
cnf(u1906,negated_conjecture,
~ product(e_2,e_2,e_3) ).
cnf(u1910,negated_conjecture,
~ product(e_2,e_2,e_4) ).
cnf(u2143,negated_conjecture,
~ product(e_3,e_4,e_4) ).
cnf(u2147,negated_conjecture,
~ product(e_3,e_4,e_2) ).
cnf(u2151,negated_conjecture,
~ product(e_3,e_4,e_1) ).
cnf(u2163,negated_conjecture,
~ product(e_4,e_4,e_3) ).
cnf(u2168,negated_conjecture,
product(e_4,e_4,e_4) ).
cnf(u2188,negated_conjecture,
product(e_3,e_4,e_3) ).
cnf(u2689,negated_conjecture,
~ product(e_1,e_3,e_2) ).
cnf(u2837,negated_conjecture,
~ product(e_3,e_3,e_1) ).
cnf(u3238,negated_conjecture,
~ product(e_4,e_5,e_2) ).
cnf(u3242,negated_conjecture,
~ product(e_4,e_5,e_3) ).
cnf(u3441,negated_conjecture,
~ product(e_4,e_4,e_1) ).
cnf(u3445,negated_conjecture,
~ product(e_4,e_4,e_2) ).
cnf(u3775,negated_conjecture,
~ product(e_4,e_2,e_4) ).
cnf(u5841,negated_conjecture,
~ product(e_2,e_4,e_3) ).
cnf(u6414,negated_conjecture,
~ product(e_1,e_5,e_4) ).
cnf(u8263,negated_conjecture,
~ product(e_3,e_2,e_4) ).
cnf(u9078,negated_conjecture,
( ~ group_element(X0)
| equalish(e_2,X0)
| product(X0,e_2,e_1)
| product(X0,e_2,e_4)
| product(X0,e_2,e_3)
| product(X0,e_2,e_2) ) ).
cnf(u10922,negated_conjecture,
product(e_1,e_2,e_4) ).
cnf(u15504,negated_conjecture,
( ~ group_element(X2)
| equalish(X0,e_4)
| product(X2,X0,e_4)
| product(X2,X0,e_3)
| product(X2,X0,e_2)
| product(X2,X0,e_1)
| ~ group_element(X0)
| ~ group_element(X1)
| product(X1,e_4,e_4)
| product(X1,e_4,e_3)
| product(X1,e_4,e_2)
| product(X1,e_4,e_1)
| ~ product(X1,X0,X2) ) ).
cnf(u15508,negated_conjecture,
( ~ group_element(X0)
| equalish(e_5,X0)
| product(X0,e_4,e_1)
| product(X0,e_4,e_4)
| product(X0,e_4,e_3)
| product(X0,e_4,e_2) ) ).
cnf(u19263,negated_conjecture,
( ~ group_element(X1)
| ~ product(e_5,X1,X0)
| equalish(X0,e_5)
| ~ group_element(X0)
| product(X0,X1,e_1)
| product(X0,X1,e_2)
| product(X0,X1,e_3)
| product(X0,X1,e_4) ) ).
cnf(u20247,negated_conjecture,
( ~ group_element(X0)
| product(e_4,X0,e_4)
| product(e_4,X0,e_3)
| product(e_4,X0,e_2)
| product(e_4,X0,e_1)
| equalish(X0,e_2)
| product(e_5,X0,e_4)
| product(e_5,X0,e_3)
| product(e_5,X0,e_1)
| product(e_5,X0,e_2) ) ).
cnf(u32916,negated_conjecture,
( ~ product(e_2,X0,e_3)
| product(e_3,X0,e_4)
| equalish(X0,e_4)
| ~ group_element(X0)
| product(e_3,X0,e_1)
| product(e_3,X0,e_2)
| product(e_3,X0,e_3) ) ).
cnf(u35135,negated_conjecture,
( ~ product(e_3,X0,e_2)
| product(e_2,X0,e_4)
| equalish(X0,e_4)
| ~ group_element(X0)
| product(e_2,X0,e_1)
| product(e_2,X0,e_2)
| product(e_2,X0,e_3) ) ).
cnf(u35348,negated_conjecture,
( ~ product(X1,X0,e_5)
| ~ product(e_1,X0,X1)
| equalish(X1,e_3) ) ).
cnf(e_4_is_not_e_5,axiom,
~ equalish(e_4,e_5) ).
cnf(u34721,negated_conjecture,
( ~ product(e_3,e_5,X0)
| ~ product(e_1,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X1,e_5) ) ).
cnf(u37044,axiom,
~ next(e_1,e_1) ).
cnf(u35349,negated_conjecture,
( ~ group_element(X1)
| equalish(X1,e_3)
| ~ group_element(X0)
| product(X1,X0,e_1)
| product(X1,X0,e_2)
| product(X1,X0,e_3)
| product(X1,X0,e_4)
| ~ product(e_1,X0,X1) ) ).
cnf(e_3_is_not_e_5,axiom,
~ equalish(e_3,e_5) ).
cnf(u36391,negated_conjecture,
( ~ group_element(X0)
| product(e_5,X0,e_2)
| product(e_5,X0,e_4)
| product(e_5,X0,e_1)
| 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(u36463,negated_conjecture,
( ~ product(e_4,e_5,X0)
| ~ product(e_2,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X1,e_5) ) ).
cnf(product_left_cancellation,axiom,
( ~ product(X3,X1,X2)
| ~ product(X0,X1,X2)
| equalish(X0,X3) ) ).
cnf(e_3_is_not_e_1,axiom,
~ equalish(e_3,e_1) ).
cnf(u35566,negated_conjecture,
( ~ product(X1,X0,e_5)
| ~ product(e_4,X0,X1)
| equalish(X1,e_2) ) ).
cnf(u34863,negated_conjecture,
( ~ product(e_5,e_1,X0)
| equalish(X0,e_1) ) ).
cnf(e_5_is_not_e_4,axiom,
~ equalish(e_5,e_4) ).
cnf(e_2_is_not_e_1,axiom,
~ equalish(e_2,e_1) ).
cnf(u36960,negated_conjecture,
( ~ product(e_1,X1,X0)
| equalish(X0,e_5)
| ~ product(X0,X1,e_4) ) ).
cnf(u36803,negated_conjecture,
( ~ group_element(X1)
| equalish(X0,e_3)
| ~ group_element(X0)
| product(X1,X0,e_1)
| product(X1,X0,e_2)
| product(X1,X0,e_3)
| product(X1,X0,e_4)
| ~ product(e_2,X0,X1) ) ).
cnf(e_5_greater_e_4,axiom,
greater(e_5,e_4) ).
cnf(u36483,negated_conjecture,
( ~ product(e_1,e_2,X0)
| equalish(X0,e_4) ) ).
cnf(u20664,negated_conjecture,
( ~ group_element(X0)
| product(e_4,X0,e_3)
| product(e_4,X0,e_2)
| product(e_4,X0,e_1)
| equalish(X0,e_2)
| product(e_5,X0,e_4)
| product(e_4,X0,e_4)
| product(e_5,X0,e_1)
| product(e_5,X0,e_2) ) ).
cnf(u36653,negated_conjecture,
( ~ group_element(X1)
| equalish(X0,e_1)
| ~ group_element(X0)
| product(X1,X0,e_1)
| product(X1,X0,e_2)
| product(X1,X0,e_3)
| product(X1,X0,e_4)
| ~ product(e_3,X0,X1) ) ).
cnf(e_5_is_not_e_1,axiom,
~ equalish(e_5,e_1) ).
cnf(e_4_greater_e_2,axiom,
greater(e_4,e_2) ).
cnf(u36925,negated_conjecture,
( ~ product(e_3,X1,X0)
| equalish(X1,e_5)
| ~ product(X0,X1,e_2) ) ).
cnf(u36465,negated_conjecture,
( ~ product(e_2,X0,e_4)
| equalish(X0,e_5) ) ).
cnf(u29668,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(u36457,negated_conjecture,
( ~ product(e_4,X0,e_3)
| equalish(X0,e_3) ) ).
cnf(u29677,axiom,
( ~ group_element(X0)
| product(X0,e_5,e_2)
| product(X0,e_5,e_3)
| product(X0,e_5,e_4)
| product(X0,e_5,e_1)
| product(X0,e_4,e_1)
| product(X0,e_4,e_2)
| product(X0,e_4,e_3)
| product(X0,e_4,e_4) ) ).
cnf(u36722,negated_conjecture,
( ~ product(e_3,X0,X1)
| ~ product(X1,X0,e_4)
| equalish(X1,e_1) ) ).
cnf(u35809,negated_conjecture,
( ~ product(e_1,X0,e_2)
| 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(u36419,negated_conjecture,
( ~ product(e_2,e_4,X0)
| equalish(X0,e_2) ) ).
cnf(e_1_is_not_e_3,axiom,
~ equalish(e_1,e_3) ).
cnf(u37026,negated_conjecture,
( ~ product(e_2,X0,e_5)
| 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(e_4_greater_e_1,axiom,
greater(e_4,e_1) ).
cnf(u35538,negated_conjecture,
( ~ group_element(X1)
| equalish(X0,e_2)
| ~ group_element(X0)
| product(X1,X0,e_1)
| product(X1,X0,e_2)
| product(X1,X0,e_3)
| product(X1,X0,e_4)
| ~ product(e_4,X0,X1) ) ).
cnf(u36852,negated_conjecture,
( ~ product(e_5,X0,e_1)
| equalish(X0,e_3)
| ~ group_element(X0)
| product(e_3,X0,e_1)
| product(e_3,X0,e_3)
| product(e_3,X0,e_4) ) ).
cnf(u36522,negated_conjecture,
( ~ product(e_5,X0,e_2)
| equalish(X0,e_5) ) ).
cnf(element_3,axiom,
group_element(e_3) ).
cnf(u36861,negated_conjecture,
( ~ product(e_3,X0,X1)
| ~ product(X1,X0,e_1)
| equalish(X1,e_2) ) ).
cnf(e_3_then_e_4,axiom,
next(e_3,e_4) ).
cnf(u36424,negated_conjecture,
( ~ product(e_2,e_3,X0)
| ~ product(e_3,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X1,e_3) ) ).
cnf(u36765,negated_conjecture,
( ~ product(e_2,X0,X1)
| ~ product(X1,X0,e_2)
| equalish(X1,e_2) ) ).
cnf(u36432,negated_conjecture,
( ~ product(e_3,e_4,X0)
| equalish(X0,e_3) ) ).
cnf(u36417,negated_conjecture,
( ~ product(X0,e_4,e_2)
| equalish(X0,e_2) ) ).
cnf(u35682,negated_conjecture,
( ~ product(e_4,X1,X0)
| equalish(X1,e_1)
| ~ product(X0,X1,e_1) ) ).
cnf(u35632,negated_conjecture,
( ~ product(e_4,X0,e_1)
| 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(no_redundancy,axiom,
( ~ product(X0,e_1,X1)
| ~ next(X0,X2)
| ~ greater(X1,X2) ) ).
cnf(u29667,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(u37005,negated_conjecture,
( ~ product(e_2,X0,e_5)
| ~ 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(u34713,axiom,
( ~ product(X0,e_1,e_2)
| equalish(X0,e_1) ) ).
cnf(u35807,negated_conjecture,
( ~ product(e_1,X0,e_5)
| 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(u36644,negated_conjecture,
( ~ product(e_5,X0,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(u35567,negated_conjecture,
( ~ group_element(X1)
| equalish(X1,e_2)
| ~ group_element(X0)
| product(X1,X0,e_1)
| product(X1,X0,e_2)
| product(X1,X0,e_3)
| product(X1,X0,e_4)
| ~ product(e_4,X0,X1) ) ).
cnf(u36399,negated_conjecture,
( ~ product(e_3,X0,e_1)
| equalish(X0,e_2) ) ).
cnf(u19885,negated_conjecture,
( ~ product(e_5,e_5,X0)
| equalish(X0,e_5)
| ~ group_element(X0)
| product(X0,e_5,e_1)
| product(X0,e_5,e_2)
| product(X0,e_5,e_3)
| product(X0,e_5,e_4) ) ).
cnf(u211,axiom,
equalish(e_2,e_2) ).
cnf(u36390,negated_conjecture,
( ~ group_element(X0)
| product(e_5,X0,e_2)
| product(e_5,X0,e_3)
| product(e_5,X0,e_4)
| product(e_5,X0,e_1)
| 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(u36442,negated_conjecture,
( ~ product(e_4,e_1,X0)
| ~ product(e_3,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X2,e_4) ) ).
cnf(u36536,negated_conjecture,
( ~ product(e_5,e_3,X0)
| equalish(X0,e_4) ) ).
cnf(u36802,negated_conjecture,
( ~ product(X1,X0,e_5)
| ~ product(e_2,X0,X1)
| equalish(X0,e_3) ) ).
cnf(u34722,negated_conjecture,
( ~ product(e_1,e_5,X0)
| equalish(X0,e_3) ) ).
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(u29678,axiom,
( ~ group_element(X0)
| product(X0,e_5,e_2)
| product(X0,e_5,e_3)
| product(X0,e_5,e_4)
| product(X0,e_5,e_1)
| product(X0,e_3,e_1)
| product(X0,e_3,e_2)
| product(X0,e_3,e_3)
| product(X0,e_3,e_4) ) ).
cnf(u36425,negated_conjecture,
( ~ product(e_3,e_3,X0)
| equalish(X0,e_2) ) ).
cnf(u35273,negated_conjecture,
( ~ product(e_5,X0,e_3)
| ~ 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(u19169,negated_conjecture,
( ~ group_element(X1)
| product(e_3,X0,e_4)
| product(e_3,X0,e_2)
| product(e_3,X0,e_1)
| ~ group_element(X0)
| equalish(X0,e_4)
| product(X1,e_4,e_4)
| product(X1,e_4,e_2)
| product(X1,e_4,e_1)
| ~ product(X1,X0,e_3) ) ).
cnf(u29731,axiom,
( ~ group_element(X0)
| product(X0,e_3,e_2)
| product(X0,e_3,e_3)
| product(X0,e_3,e_4)
| product(X0,e_3,e_1)
| product(X0,e_4,e_1)
| product(X0,e_4,e_2)
| product(X0,e_4,e_3)
| product(X0,e_4,e_4) ) ).
cnf(u36430,negated_conjecture,
( ~ product(X0,e_4,e_3)
| equalish(X0,e_3) ) ).
cnf(u36519,negated_conjecture,
( ~ product(X0,e_5,e_2)
| equalish(X0,e_5) ) ).
cnf(u36897,negated_conjecture,
( ~ group_element(X0)
| product(e_5,X0,e_2)
| equalish(X0,e_1)
| product(e_3,X0,e_1)
| product(e_3,X0,e_2)
| product(e_3,X0,e_3) ) ).
cnf(u34902,negated_conjecture,
( ~ group_element(X0)
| ~ product(X2,X1,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(u36869,negated_conjecture,
( ~ product(e_5,X0,e_1)
| ~ 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(u36880,negated_conjecture,
( ~ product(e_5,X0,e_3)
| ~ group_element(X0)
| product(e_3,X0,e_1)
| product(e_3,X0,e_2)
| product(e_3,X0,e_4) ) ).
cnf(u35509,negated_conjecture,
( ~ product(e_5,X0,X1)
| ~ product(X1,X0,e_2)
| equalish(X1,e_1) ) ).
cnf(u19164,negated_conjecture,
( ~ group_element(X1)
| product(e_4,X0,e_4)
| product(e_4,X0,e_3)
| product(e_4,X0,e_2)
| product(e_4,X0,e_1)
| ~ group_element(X0)
| equalish(X0,e_4)
| product(X1,e_4,e_3)
| product(X1,e_4,e_2)
| product(X1,e_4,e_1)
| ~ product(X1,X0,e_4) ) ).
cnf(u36433,negated_conjecture,
( ~ product(e_3,X0,e_3)
| equalish(X0,e_4) ) ).
cnf(u36431,negated_conjecture,
( ~ product(e_3,e_4,X0)
| ~ product(e_3,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X1,e_4) ) ).
cnf(u34861,negated_conjecture,
( ~ product(X0,e_1,e_1)
| equalish(X0,e_5) ) ).
cnf(u36409,negated_conjecture,
( ~ product(X0,e_1,e_3)
| equalish(X0,e_2) ) ).
cnf(u36475,negated_conjecture,
( ~ product(e_4,X0,e_4)
| equalish(X0,e_4) ) ).
cnf(u36842,negated_conjecture,
( ~ product(e_5,X0,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(u32529,axiom,
( ~ group_element(X0)
| product(X0,e_1,e_2)
| product(X0,e_1,e_3)
| product(X0,e_1,e_4)
| product(X0,e_1,e_1)
| equalish(e_4,X0) ) ).
cnf(u34901,negated_conjecture,
( ~ product(e_5,X0,e_3)
| equalish(X0,e_2) ) ).
cnf(u36854,negated_conjecture,
( ~ product(e_3,X0,X1)
| ~ product(X1,X0,e_3)
| equalish(X0,e_4) ) ).
cnf(u36720,negated_conjecture,
( ~ product(e_5,X0,e_2)
| ~ 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(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(e_5,X3,e_1)
| product(e_5,X3,e_2)
| product(e_5,X3,e_3)
| product(e_5,X3,e_4)
| ~ 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(u34899,negated_conjecture,
( ~ product(e_3,e_2,X0)
| ~ product(e_5,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X1,e_2) ) ).
cnf(u36990,negated_conjecture,
( ~ product(e_2,X0,X1)
| ~ product(X1,X0,e_1)
| equalish(X1,e_4) ) ).
cnf(u36758,negated_conjecture,
( ~ product(e_1,X0,X1)
| ~ product(X1,X0,e_1)
| equalish(X0,e_4) ) ).
cnf(u36464,negated_conjecture,
( ~ product(e_2,e_5,X0)
| equalish(X0,e_4) ) ).
cnf(u49,negated_conjecture,
( ~ product(e_5,X0,X1)
| ~ product(X2,X3,X4)
| ~ product(X4,X3,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(u36732,negated_conjecture,
( ~ product(e_5,X0,X1)
| ~ product(X1,X0,e_4)
| equalish(X0,e_5) ) ).
cnf(u29732,axiom,
( ~ group_element(X0)
| product(X0,e_3,e_2)
| product(X0,e_3,e_3)
| product(X0,e_3,e_4)
| product(X0,e_3,e_1)
| product(X0,e_1,e_1)
| product(X0,e_1,e_2)
| product(X0,e_1,e_3)
| product(X0,e_1,e_4) ) ).
cnf(u35173,negated_conjecture,
( ~ product(e_4,X0,e_2)
| equalish(X0,e_2) ) ).
cnf(u34865,negated_conjecture,
( ~ group_element(X0)
| ~ product(X2,X1,e_1)
| 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)
| ~ product(X0,X1,X2) ) ).
cnf(u36844,negated_conjecture,
( ~ product(e_3,X0,X1)
| ~ product(X1,X0,e_1)
| equalish(X0,e_3) ) ).
cnf(u34897,negated_conjecture,
( ~ product(e_3,e_2,X0)
| ~ product(e_5,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X2,e_3) ) ).
cnf(u36453,negated_conjecture,
( ~ product(e_3,e_3,X0)
| ~ product(e_4,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X2,e_3) ) ).
cnf(u29709,axiom,
( ~ 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)
| 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(u36398,negated_conjecture,
( ~ product(e_3,e_2,X0)
| equalish(X0,e_1) ) ).
cnf(qg1_2,negated_conjecture,
( ~ product(X5,X4,X3)
| ~ product(X3,X4,X2)
| ~ product(X5,X1,X0)
| ~ product(X0,X1,X2)
| equalish(X1,X4) ) ).
cnf(u36661,negated_conjecture,
( ~ group_element(X1)
| equalish(X1,e_4)
| ~ group_element(X0)
| product(X1,X0,e_1)
| product(X1,X0,e_2)
| product(X1,X0,e_3)
| product(X1,X0,e_4)
| ~ product(e_3,X0,X1) ) ).
cnf(u36887,negated_conjecture,
( ~ product(e_3,X0,e_5)
| ~ group_element(X0)
| product(e_5,X0,e_2)
| product(e_5,X0,e_3)
| product(e_5,X0,e_4)
| equalish(X0,e_1) ) ).
cnf(u36397,negated_conjecture,
( ~ product(e_1,e_2,X0)
| ~ product(e_3,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X1,e_2) ) ).
cnf(u29749,axiom,
( ~ group_element(X0)
| product(X0,e_4,e_2)
| product(X0,e_4,e_3)
| product(X0,e_4,e_4)
| product(X0,e_4,e_1)
| product(X0,e_1,e_1)
| product(X0,e_1,e_2)
| product(X0,e_1,e_3)
| product(X0,e_1,e_4) ) ).
cnf(product_total_function2,axiom,
( ~ product(X0,X1,X3)
| ~ product(X0,X1,X2)
| equalish(X2,X3) ) ).
cnf(u29278,negated_conjecture,
( ~ product(e_5,X0,e_4)
| product(e_4,X0,e_3)
| product(e_4,X0,e_2)
| product(e_4,X0,e_1)
| ~ group_element(X0)
| equalish(X0,e_4)
| product(e_4,X0,e_4) ) ).
cnf(u36456,negated_conjecture,
( ~ product(e_4,e_3,X0)
| equalish(X0,e_3) ) ).
cnf(e_2_is_not_e_4,axiom,
~ equalish(e_2,e_4) ).
cnf(u36426,negated_conjecture,
( ~ product(e_3,X0,e_2)
| equalish(X0,e_3) ) ).
cnf(u36538,negated_conjecture,
( ~ group_element(X0)
| ~ product(X2,X1,e_4)
| equalish(X2,e_5)
| product(X0,e_3,e_1)
| product(X0,e_3,e_2)
| product(X0,e_3,e_3)
| product(X0,e_3,e_4)
| ~ product(X0,X1,X2) ) ).
cnf(u35786,negated_conjecture,
( ~ product(e_1,X0,e_4)
| ~ group_element(X0)
| product(e_4,X0,e_2)
| product(e_4,X0,e_3)
| product(e_4,X0,e_4)
| equalish(X0,e_5) ) ).
cnf(e_5_is_not_e_3,axiom,
~ equalish(e_5,e_3) ).
cnf(element_5,axiom,
group_element(e_5) ).
cnf(u36936,negated_conjecture,
( ~ product(e_3,X0,e_5)
| 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(u35265,negated_conjecture,
( ~ product(e_4,X0,X1)
| ~ product(X1,X0,e_3)
| equalish(X1,e_1) ) ).
cnf(u36670,negated_conjecture,
( ~ product(e_4,X0,X1)
| ~ product(X1,X0,e_4)
| equalish(X1,e_4) ) ).
cnf(u36471,negated_conjecture,
( ~ product(e_4,e_4,X0)
| ~ product(e_4,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X2,e_4) ) ).
cnf(e_4_is_not_e_3,axiom,
~ equalish(e_4,e_3) ).
cnf(u36454,negated_conjecture,
( ~ product(X0,e_3,e_3)
| equalish(X0,e_4) ) ).
cnf(u36741,negated_conjecture,
( ~ product(e_5,X0,X1)
| ~ product(X1,X0,e_3)
| equalish(X0,e_3) ) ).
cnf(element_1,axiom,
group_element(e_1) ).
cnf(u36422,negated_conjecture,
( ~ product(e_2,e_3,X0)
| ~ product(e_3,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X2,e_2) ) ).
cnf(u36938,negated_conjecture,
( ~ product(e_3,X0,e_1)
| 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(u8155,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(u37027,negated_conjecture,
( ~ product(e_2,X0,e_4)
| 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(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(u36496,negated_conjecture,
( ~ product(e_2,X0,e_1)
| equalish(X0,e_3) ) ).
cnf(u35630,negated_conjecture,
( ~ product(e_4,X0,e_5)
| 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(e_2_is_not_e_5,axiom,
~ equalish(e_2,e_5) ).
cnf(u36636,negated_conjecture,
( ~ product(e_5,X0,e_3)
| equalish(X0,e_1)
| ~ group_element(X0)
| product(e_1,X0,e_1)
| product(e_1,X0,e_3)
| product(e_1,X0,e_4) ) ).
cnf(u36438,negated_conjecture,
( ~ product(e_1,e_4,X0)
| equalish(X0,e_1) ) ).
cnf(e_5_greater_e_3,axiom,
greater(e_5,e_3) ).
cnf(u36944,negated_conjecture,
( ~ group_element(X0)
| product(e_5,X0,e_2)
| 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(u34828,negated_conjecture,
( ~ product(e_1,e_5,X0)
| ~ product(e_4,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X1,e_5) ) ).
cnf(u36495,negated_conjecture,
( ~ product(e_2,e_3,X0)
| equalish(X0,e_1) ) ).
cnf(u36420,negated_conjecture,
( ~ product(e_2,X0,e_2)
| equalish(X0,e_4) ) ).
cnf(u36628,negated_conjecture,
( ~ product(e_5,X0,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(e_1_is_not_e_5,axiom,
~ equalish(e_1,e_5) ).
cnf(u36712,negated_conjecture,
( ~ product(e_1,X0,X1)
| ~ product(X1,X0,e_2)
| equalish(X1,e_4) ) ).
cnf(e_3_greater_e_2,axiom,
greater(e_3,e_2) ).
cnf(u35449,negated_conjecture,
( ~ product(e_5,X0,X1)
| ~ product(X1,X0,e_2)
| equalish(X0,e_1) ) ).
cnf(u36423,negated_conjecture,
( ~ product(X0,e_3,e_2)
| equalish(X0,e_3) ) ).
cnf(u34864,negated_conjecture,
( ~ product(e_5,X0,e_1)
| equalish(X0,e_1) ) ).
cnf(u36794,negated_conjecture,
( ~ product(e_5,X0,e_1)
| ~ group_element(X0)
| product(e_1,X0,e_2)
| product(e_1,X0,e_3)
| product(e_1,X0,e_4) ) ).
cnf(u8157,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(u36524,negated_conjecture,
( ~ group_element(X0)
| ~ product(X2,X1,e_2)
| 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)
| ~ product(X0,X1,X2) ) ).
cnf(e_1_is_not_e_2,axiom,
~ equalish(e_1,e_2) ).
cnf(u34898,negated_conjecture,
( ~ product(X0,e_2,e_3)
| equalish(X0,e_5) ) ).
cnf(u8154,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(element_2,axiom,
group_element(e_2) ).
cnf(u36537,negated_conjecture,
( ~ product(e_5,X0,e_4)
| equalish(X0,e_3) ) ).
cnf(u35023,negated_conjecture,
( ~ product(e_4,X0,X1)
| ~ product(X1,X0,e_3)
| equalish(X0,e_5) ) ).
cnf(e_3_greater_e_1,axiom,
greater(e_3,e_1) ).
cnf(u19883,negated_conjecture,
( ~ product(e_5,e_3,X0)
| equalish(X0,e_5)
| ~ group_element(X0)
| product(X0,e_3,e_1)
| product(X0,e_3,e_2)
| product(X0,e_3,e_3)
| product(X0,e_3,e_4) ) ).
cnf(u36833,negated_conjecture,
( ~ product(e_4,X0,X1)
| ~ product(X1,X0,e_2)
| equalish(X1,e_3) ) ).
cnf(u35171,negated_conjecture,
( ~ product(e_2,e_2,X0)
| ~ product(e_4,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X1,e_2) ) ).
cnf(u36494,negated_conjecture,
( ~ product(e_1,e_3,X0)
| ~ product(e_2,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X1,e_3) ) ).
cnf(u29669,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(u34826,negated_conjecture,
( ~ product(e_1,e_5,X0)
| ~ product(e_4,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X2,e_1) ) ).
cnf(u35170,negated_conjecture,
( ~ product(X0,e_2,e_2)
| equalish(X0,e_4) ) ).
cnf(u35710,negated_conjecture,
( ~ product(e_2,X1,X0)
| equalish(X0,e_5)
| ~ product(X0,X1,e_3) ) ).
cnf(e_2_then_e_3,axiom,
next(e_2,e_3) ).
cnf(u36889,negated_conjecture,
( ~ product(e_3,X0,e_1)
| ~ group_element(X0)
| product(e_1,X0,e_1)
| product(e_1,X0,e_3)
| product(e_1,X0,e_4)
| equalish(X0,e_1) ) ).
cnf(u35301,negated_conjecture,
( ~ product(X1,X0,e_5)
| ~ product(e_1,X0,X1)
| equalish(X0,e_5) ) ).
cnf(u36446,negated_conjecture,
( ~ product(e_3,X0,e_4)
| equalish(X0,e_1) ) ).
cnf(u34712,negated_conjecture,
( ~ product(e_2,e_1,X0)
| ~ product(e_1,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X2,e_2) ) ).
cnf(u29666,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(u36408,negated_conjecture,
( ~ product(e_3,e_1,X0)
| ~ product(e_2,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X2,e_3) ) ).
cnf(u207,negated_conjecture,
equalish(e_4,e_4) ).
cnf(u34903,negated_conjecture,
( ~ group_element(X0)
| ~ product(X2,X1,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(u37007,negated_conjecture,
( ~ product(e_2,X0,e_3)
| ~ group_element(X0)
| product(e_3,X0,e_1)
| product(e_3,X0,e_3)
| product(e_3,X0,e_4)
| equalish(X0,e_3) ) ).
cnf(u35738,negated_conjecture,
( ~ product(e_4,X1,X0)
| equalish(X0,e_5)
| ~ product(X0,X1,e_1) ) ).
cnf(u35606,negated_conjecture,
( ~ product(e_4,X0,e_5)
| ~ group_element(X0)
| product(e_5,X0,e_1)
| product(e_5,X0,e_2)
| product(e_5,X0,e_4)
| equalish(X0,e_2) ) ).
cnf(u35668,negated_conjecture,
( ~ product(e_2,X1,X0)
| equalish(X1,e_2)
| ~ product(X0,X1,e_3) ) ).
cnf(u36411,negated_conjecture,
( ~ product(e_2,e_1,X0)
| equalish(X0,e_3) ) ).
cnf(u36492,negated_conjecture,
( ~ product(e_1,e_3,X0)
| ~ product(e_2,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X2,e_1) ) ).
cnf(u36482,negated_conjecture,
( ~ product(e_4,e_2,X0)
| ~ product(e_1,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X1,e_2) ) ).
cnf(u30036,negated_conjecture,
~ greater(e_4,e_4) ).
cnf(u210,axiom,
equalish(e_1,e_1) ).
cnf(u36406,negated_conjecture,
( ~ next(e_2,X0)
| ~ greater(e_3,X0) ) ).
cnf(u37015,negated_conjecture,
( ~ group_element(X0)
| product(e_5,X0,e_3)
| equalish(X0,e_3)
| product(e_2,X0,e_2)
| product(e_2,X0,e_3)
| product(e_2,X0,e_4) ) ).
cnf(u37028,negated_conjecture,
( ~ product(e_2,X0,e_3)
| product(e_3,X0,e_1)
| product(e_3,X0,e_2)
| product(e_3,X0,e_3)
| product(e_3,X0,e_4)
| ~ group_element(X0) ) ).
cnf(u8156,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(u29670,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(u36520,negated_conjecture,
( ~ product(e_2,e_5,X0)
| ~ product(e_5,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X1,e_5) ) ).
cnf(u36710,negated_conjecture,
( ~ product(e_5,X0,e_4)
| equalish(X0,e_2)
| ~ group_element(X0)
| product(e_3,X0,e_2)
| product(e_3,X0,e_3)
| product(e_3,X0,e_4) ) ).
cnf(u34719,negated_conjecture,
( ~ product(e_3,e_5,X0)
| ~ product(e_1,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X2,e_3) ) ).
cnf(u36888,negated_conjecture,
( ~ product(e_3,X0,e_2)
| ~ group_element(X0)
| product(e_2,X0,e_1)
| product(e_2,X0,e_2)
| product(e_2,X0,e_4)
| equalish(X0,e_1) ) ).
cnf(u36416,negated_conjecture,
( ~ product(e_2,e_4,X0)
| ~ product(e_2,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X2,e_2) ) ).
cnf(u36988,negated_conjecture,
( ~ product(e_5,X0,e_1)
| equalish(X0,e_5)
| ~ group_element(X0)
| product(e_2,X0,e_1)
| product(e_2,X0,e_2)
| product(e_2,X0,e_3) ) ).
cnf(u36481,negated_conjecture,
( ~ product(X0,e_2,e_4)
| equalish(X0,e_1) ) ).
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(u36412,negated_conjecture,
( ~ product(e_2,X0,e_3)
| equalish(X0,e_1) ) ).
cnf(u19167,negated_conjecture,
( ~ group_element(X1)
| product(e_1,X0,e_4)
| product(e_1,X0,e_3)
| product(e_1,X0,e_2)
| product(e_1,X0,e_1)
| ~ group_element(X0)
| equalish(X0,e_4)
| product(X1,e_4,e_4)
| product(X1,e_4,e_3)
| product(X1,e_4,e_2)
| ~ product(X1,X0,e_1) ) ).
cnf(u36662,negated_conjecture,
( ~ product(e_4,X0,X1)
| ~ product(X1,X0,e_4)
| equalish(X0,e_4) ) ).
cnf(u36437,negated_conjecture,
( ~ product(e_1,e_4,X0)
| ~ product(e_1,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X1,e_4) ) ).
cnf(u36461,negated_conjecture,
( ~ product(e_4,e_5,X0)
| ~ product(e_2,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X2,e_4) ) ).
cnf(u29707,axiom,
( ~ 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)
| 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(u59,negated_conjecture,
( ~ product(X2,X1,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(e_5,X3,e_1)
| product(e_5,X3,e_2)
| product(e_5,X3,e_3)
| product(e_5,X3,e_4) ) ).
cnf(u36393,negated_conjecture,
( ~ product(e_5,X0,X1)
| ~ product(X1,X0,e_1)
| equalish(X0,e_2) ) ).
cnf(u35631,negated_conjecture,
( ~ product(e_4,X0,e_3)
| product(e_3,X0,e_1)
| product(e_3,X0,e_2)
| product(e_3,X0,e_3)
| product(e_3,X0,e_4)
| ~ group_element(X0) ) ).
cnf(u34710,axiom,
( ~ greater(e_2,X0)
| ~ next(e_1,X0) ) ).
cnf(u36826,negated_conjecture,
( ~ product(X1,X0,e_5)
| ~ product(e_2,X0,X1)
| equalish(X1,e_1) ) ).
cnf(u35172,negated_conjecture,
( ~ product(e_4,e_2,X0)
| equalish(X0,e_2) ) ).
cnf(u34563,negated_conjecture,
~ greater(e_3,e_3) ).
cnf(u36974,negated_conjecture,
( ~ product(e_3,X1,X0)
| equalish(X0,e_5)
| ~ product(X0,X1,e_2) ) ).
cnf(u35808,negated_conjecture,
( ~ product(e_1,X0,e_4)
| 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(u36443,negated_conjecture,
( ~ product(X0,e_1,e_4)
| equalish(X0,e_3) ) ).
cnf(u52,negated_conjecture,
( ~ product(X2,X1,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(e_5,X3,e_1)
| product(e_5,X3,e_2)
| product(e_5,X3,e_3)
| product(e_5,X3,e_4) ) ).
cnf(u36785,negated_conjecture,
( ~ product(e_1,X0,X1)
| ~ product(X1,X0,e_1)
| equalish(X1,e_1) ) ).
cnf(u34862,negated_conjecture,
( ~ product(e_1,e_1,X0)
| ~ product(e_5,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X1,e_1) ) ).
cnf(u36980,negated_conjecture,
( ~ product(e_2,X0,X1)
| ~ product(X1,X0,e_1)
| equalish(X0,e_5) ) ).
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(e_4_is_not_e_1,axiom,
~ equalish(e_4,e_1) ).
cnf(u34866,negated_conjecture,
( ~ group_element(X0)
| ~ product(X2,X1,e_1)
| 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)
| ~ product(X0,X1,X2) ) ).
cnf(u29369,negated_conjecture,
( ~ group_element(X0)
| product(e_5,X0,e_2)
| product(e_5,X0,e_1)
| product(e_5,X0,e_3)
| product(e_5,X0,e_4)
| equalish(X0,e_4) ) ).
cnf(u36533,negated_conjecture,
( ~ product(e_4,e_3,X0)
| ~ product(e_5,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X2,e_4) ) ).
cnf(u36937,negated_conjecture,
( ~ product(e_3,X0,e_2)
| 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(qg1_1,negated_conjecture,
( ~ product(X5,X4,X3)
| ~ product(X3,X4,X2)
| ~ product(X5,X1,X0)
| ~ product(X0,X1,X2)
| equalish(X0,X3) ) ).
cnf(u29243,negated_conjecture,
( ~ product(e_5,X0,e_2)
| product(e_2,X0,e_3)
| product(e_2,X0,e_1)
| ~ group_element(X0)
| equalish(X0,e_4)
| product(e_2,X0,e_4) ) ).
cnf(u36410,negated_conjecture,
( ~ product(e_3,e_1,X0)
| ~ product(e_2,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X1,e_1) ) ).
cnf(u36776,negated_conjecture,
( ~ product(e_5,X0,X1)
| ~ product(X1,X0,e_4)
| equalish(X1,e_2) ) ).
cnf(u35032,negated_conjecture,
( ~ product(e_5,X0,e_3)
| equalish(X0,e_5)
| ~ group_element(X0)
| product(e_4,X0,e_2)
| product(e_4,X0,e_3)
| product(e_4,X0,e_4) ) ).
cnf(u36660,negated_conjecture,
( ~ product(X1,X0,e_5)
| ~ product(e_3,X0,X1)
| equalish(X1,e_4) ) ).
cnf(u56,negated_conjecture,
( ~ product(e_5,X0,X1)
| ~ product(X2,X3,X4)
| ~ product(X4,X3,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(u36444,negated_conjecture,
( ~ product(e_4,e_1,X0)
| ~ product(e_3,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X1,e_1) ) ).
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(u35169,negated_conjecture,
( ~ product(e_2,e_2,X0)
| ~ product(e_4,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X2,e_2) ) ).
cnf(e_3_is_not_e_2,axiom,
~ equalish(e_3,e_2) ).
cnf(u29708,axiom,
( ~ 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)
| 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(u27670,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(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(e_2_is_not_e_3,axiom,
~ equalish(e_2,e_3) ).
cnf(u29332,negated_conjecture,
( ~ product(e_5,X0,e_1)
| product(e_1,X0,e_3)
| product(e_1,X0,e_2)
| ~ group_element(X0)
| equalish(X0,e_4)
| product(e_1,X0,e_4) ) ).
cnf(u36440,negated_conjecture,
( ~ next(e_3,X0)
| ~ greater(e_4,X0) ) ).
cnf(e_5_greater_e_2,axiom,
greater(e_5,e_2) ).
cnf(u36610,negated_conjecture,
( ~ product(e_2,X0,X1)
| ~ product(X1,X0,e_4)
| equalish(X0,e_1) ) ).
cnf(u36998,negated_conjecture,
( ~ product(e_5,X0,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(u36618,negated_conjecture,
( ~ product(e_5,X0,e_4)
| equalish(X0,e_1)
| ~ group_element(X0)
| product(e_2,X0,e_1)
| product(e_2,X0,e_2)
| product(e_2,X0,e_4) ) ).
cnf(u19166,negated_conjecture,
( ~ group_element(X1)
| product(e_2,X0,e_4)
| product(e_2,X0,e_3)
| product(e_2,X0,e_2)
| product(e_2,X0,e_1)
| ~ group_element(X0)
| equalish(X0,e_4)
| product(X1,e_4,e_4)
| product(X1,e_4,e_3)
| product(X1,e_4,e_1)
| ~ product(X1,X0,e_2) ) ).
cnf(e_5_is_not_e_2,axiom,
~ equalish(e_5,e_2) ).
cnf(u36429,negated_conjecture,
( ~ product(e_3,e_4,X0)
| ~ product(e_3,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X2,e_3) ) ).
cnf(e_1_is_not_e_4,axiom,
~ equalish(e_1,e_4) ).
cnf(u36700,negated_conjecture,
( ~ product(e_5,X0,e_2)
| equalish(X0,e_2)
| ~ group_element(X0)
| product(e_1,X0,e_1)
| product(e_1,X0,e_2)
| product(e_1,X0,e_3) ) ).
cnf(u36462,negated_conjecture,
( ~ product(X0,e_5,e_4)
| equalish(X0,e_2) ) ).
cnf(e_4_then_e_5,axiom,
next(e_4,e_5) ).
cnf(u34716,axiom,
( ~ product(e_1,X0,e_2)
| equalish(X0,e_1) ) ).
cnf(u19170,negated_conjecture,
( ~ group_element(X1)
| product(e_2,X0,e_4)
| product(e_2,X0,e_3)
| product(e_2,X0,e_1)
| ~ group_element(X0)
| equalish(X0,e_4)
| product(X1,e_4,e_4)
| product(X1,e_4,e_3)
| product(X1,e_4,e_1)
| ~ product(X1,X0,e_2) ) ).
cnf(e_4_is_not_e_2,axiom,
~ equalish(e_4,e_2) ).
cnf(u34829,negated_conjecture,
( ~ product(e_4,e_5,X0)
| equalish(X0,e_1) ) ).
cnf(element_4,axiom,
group_element(e_4) ).
cnf(u36455,negated_conjecture,
( ~ product(e_3,e_3,X0)
| ~ product(e_4,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X1,e_3) ) ).
cnf(u36534,negated_conjecture,
( ~ product(X0,e_3,e_4)
| equalish(X0,e_5) ) ).
cnf(u19882,negated_conjecture,
( ~ product(e_5,e_2,X0)
| equalish(X0,e_5)
| ~ group_element(X0)
| product(X0,e_2,e_1)
| product(X0,e_2,e_2)
| product(X0,e_2,e_3)
| product(X0,e_2,e_4) ) ).
cnf(u36439,negated_conjecture,
( ~ product(e_1,X0,e_1)
| equalish(X0,e_4) ) ).
cnf(e_3_is_not_e_4,axiom,
~ equalish(e_3,e_4) ).
cnf(u36480,negated_conjecture,
( ~ product(e_4,e_2,X0)
| ~ product(e_1,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X2,e_4) ) ).
cnf(e_4_greater_e_3,axiom,
greater(e_4,e_3) ).
cnf(u36778,negated_conjecture,
( ~ product(e_5,X0,X1)
| ~ product(X1,X0,e_3)
| equalish(X1,e_4) ) ).
cnf(u36484,negated_conjecture,
( ~ product(e_1,X0,e_4)
| equalish(X0,e_2) ) ).
cnf(u36539,negated_conjecture,
( ~ group_element(X0)
| ~ product(X2,X1,e_4)
| equalish(X1,e_3)
| product(X0,e_3,e_1)
| product(X0,e_3,e_2)
| product(X0,e_3,e_3)
| product(X0,e_3,e_4)
| ~ product(X0,X1,X2) ) ).
cnf(u8153,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(u36702,negated_conjecture,
( ~ product(e_3,X0,X1)
| ~ product(X1,X0,e_4)
| equalish(X0,e_2) ) ).
cnf(u36435,negated_conjecture,
( ~ product(e_1,e_4,X0)
| ~ product(e_1,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X2,e_1) ) ).
cnf(e_5_greater_e_1,axiom,
greater(e_5,e_1) ).
cnf(u36827,negated_conjecture,
( ~ group_element(X1)
| equalish(X1,e_1)
| ~ group_element(X0)
| product(X1,X0,e_1)
| product(X1,X0,e_2)
| product(X1,X0,e_3)
| product(X1,X0,e_4)
| ~ product(e_2,X0,X1) ) ).
cnf(u36472,negated_conjecture,
( ~ product(X0,e_4,e_4)
| equalish(X0,e_4) ) ).
cnf(u34715,axiom,
( ~ product(e_1,e_1,X0)
| equalish(X0,e_2) ) ).
cnf(u35302,negated_conjecture,
( ~ group_element(X1)
| equalish(X0,e_5)
| ~ group_element(X0)
| product(X1,X0,e_1)
| product(X1,X0,e_2)
| product(X1,X0,e_3)
| product(X1,X0,e_4)
| ~ product(e_1,X0,X1) ) ).
cnf(e_2_greater_e_1,axiom,
greater(e_2,e_1) ).
cnf(u34827,negated_conjecture,
( ~ product(X0,e_5,e_1)
| equalish(X0,e_4) ) ).
cnf(u29679,axiom,
( ~ group_element(X0)
| product(X0,e_5,e_2)
| product(X0,e_5,e_3)
| product(X0,e_5,e_4)
| product(X0,e_5,e_1)
| product(X0,e_2,e_1)
| product(X0,e_2,e_2)
| product(X0,e_2,e_3)
| product(X0,e_2,e_4) ) ).
cnf(u36400,negated_conjecture,
( ~ product(e_1,X0,X1)
| ~ product(X1,X0,e_3)
| equalish(X1,e_2) ) ).
cnf(u36911,negated_conjecture,
( ~ product(e_1,X1,X0)
| equalish(X1,e_3)
| ~ product(X0,X1,e_4) ) ).
cnf(e_1_then_e_2,axiom,
next(e_1,e_2) ).
cnf(u205,negated_conjecture,
equalish(e_3,e_3) ).
cnf(u37006,negated_conjecture,
( ~ product(e_2,X0,e_4)
| ~ 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(u34723,negated_conjecture,
( ~ product(e_1,X0,e_3)
| equalish(X0,e_5) ) ).
cnf(u36535,negated_conjecture,
( ~ product(e_4,e_3,X0)
| ~ product(e_5,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X1,e_3) ) ).
cnf(u37034,negated_conjecture,
( ~ group_element(X0)
| product(e_5,X0,e_3)
| 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(u36396,negated_conjecture,
( ~ product(X0,e_2,e_1)
| equalish(X0,e_3) ) ).
cnf(u29331,negated_conjecture,
( ~ product(e_5,X0,e_1)
| product(e_1,X0,e_3)
| product(e_1,X0,e_2)
| product(e_1,X0,e_1)
| ~ group_element(X0)
| equalish(X0,e_4)
| product(e_1,X0,e_4) ) ).
cnf(u36734,negated_conjecture,
( ~ product(e_2,X0,X1)
| ~ product(X1,X0,e_2)
| equalish(X0,e_4) ) ).
cnf(u34720,negated_conjecture,
( ~ product(X0,e_5,e_3)
| equalish(X0,e_1) ) ).
cnf(u36518,negated_conjecture,
( ~ product(e_2,e_5,X0)
| ~ product(e_5,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X2,e_2) ) ).
cnf(u36392,negated_conjecture,
( ~ product(e_5,X0,X1)
| ~ product(X1,X0,e_1)
| equalish(X1,e_3) ) ).
cnf(u29269,negated_conjecture,
( ~ product(e_5,X0,e_3)
| product(e_3,X0,e_2)
| product(e_3,X0,e_1)
| ~ group_element(X0)
| equalish(X0,e_4)
| product(e_3,X0,e_4) ) ).
cnf(u36525,negated_conjecture,
( ~ group_element(X0)
| ~ product(X2,X1,e_2)
| 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(u36418,negated_conjecture,
( ~ product(e_2,e_4,X0)
| ~ product(e_2,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X1,e_4) ) ).
cnf(u34858,negated_conjecture,
( ~ greater(e_1,X0)
| ~ next(e_5,X0) ) ).
cnf(u36474,negated_conjecture,
( ~ product(e_4,e_4,X0)
| equalish(X0,e_4) ) ).
cnf(u29268,negated_conjecture,
( ~ product(e_5,X0,e_3)
| product(e_3,X0,e_3)
| product(e_3,X0,e_2)
| product(e_3,X0,e_1)
| ~ group_element(X0)
| equalish(X0,e_4)
| product(e_3,X0,e_4) ) ).
cnf(u34714,negated_conjecture,
( ~ product(e_2,e_1,X0)
| ~ product(e_1,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X1,e_1) ) ).
cnf(u29279,negated_conjecture,
( ~ product(e_5,X0,e_4)
| product(e_4,X0,e_2)
| product(e_4,X0,e_1)
| ~ group_element(X0)
| equalish(X0,e_4)
| product(e_4,X0,e_3) ) ).
cnf(u34830,negated_conjecture,
( ~ product(e_4,X0,e_1)
| equalish(X0,e_5) ) ).
cnf(u36692,negated_conjecture,
( ~ product(e_1,X0,X1)
| ~ product(X1,X0,e_2)
| equalish(X0,e_2) ) ).
cnf(u36395,negated_conjecture,
( ~ product(e_1,e_2,X0)
| ~ product(e_3,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X2,e_1) ) ).
cnf(u36620,negated_conjecture,
( ~ product(e_2,X0,X1)
| ~ product(X1,X0,e_4)
| equalish(X1,e_3) ) ).
cnf(u36473,negated_conjecture,
( ~ product(e_4,e_4,X0)
| ~ product(e_4,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X1,e_4) ) ).
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(e_5,X3,e_1)
| product(e_5,X3,e_2)
| product(e_5,X3,e_3)
| product(e_5,X3,e_4)
| ~ 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(u36521,negated_conjecture,
( ~ product(e_5,e_5,X0)
| equalish(X0,e_2) ) ).
cnf(u19881,negated_conjecture,
( ~ product(e_5,e_1,X0)
| equalish(X0,e_5)
| ~ group_element(X0)
| product(X0,e_1,e_1)
| product(X0,e_1,e_2)
| product(X0,e_1,e_3)
| product(X0,e_1,e_4) ) ).
cnf(u27667,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_1,X0) ) ).
cnf(u36730,negated_conjecture,
( ~ product(e_5,X0,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(u36871,negated_conjecture,
( ~ product(e_3,X0,X1)
| ~ product(X1,X0,e_3)
| equalish(X1,e_3) ) ).
cnf(u36652,negated_conjecture,
( ~ product(X1,X0,e_5)
| ~ product(e_3,X0,X1)
| equalish(X0,e_1) ) ).
cnf(u34860,negated_conjecture,
( ~ product(e_1,e_1,X0)
| ~ product(e_5,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X2,e_1) ) ).
cnf(u34900,negated_conjecture,
( ~ product(e_5,e_2,X0)
| equalish(X0,e_3) ) ).
cnf(u36680,negated_conjecture,
( ~ product(e_5,X0,e_4)
| ~ group_element(X0)
| product(e_4,X0,e_1)
| product(e_4,X0,e_2)
| product(e_4,X0,e_3) ) ).
cnf(u36436,negated_conjecture,
( ~ product(X0,e_4,e_1)
| equalish(X0,e_1) ) ).
cnf(u36774,negated_conjecture,
( ~ product(e_5,X0,e_2)
| ~ group_element(X0)
| product(e_2,X0,e_1)
| product(e_2,X0,e_3)
| product(e_2,X0,e_4) ) ).
cnf(u36804,negated_conjecture,
( ~ product(e_4,X0,X1)
| ~ product(X1,X0,e_2)
| equalish(X0,e_3) ) ).
cnf(u29680,axiom,
( ~ group_element(X0)
| product(X0,e_5,e_2)
| product(X0,e_5,e_3)
| product(X0,e_5,e_4)
| product(X0,e_5,e_1)
| product(X0,e_1,e_1)
| product(X0,e_1,e_2)
| product(X0,e_1,e_3)
| product(X0,e_1,e_4) ) ).
cnf(u35537,negated_conjecture,
( ~ product(X1,X0,e_5)
| ~ product(e_4,X0,X1)
| equalish(X0,e_2) ) ).
cnf(u36445,negated_conjecture,
( ~ product(e_3,e_1,X0)
| equalish(X0,e_4) ) ).
cnf(u36813,negated_conjecture,
( ~ product(e_5,X0,e_2)
| equalish(X0,e_3)
| ~ group_element(X0)
| product(e_4,X0,e_1)
| product(e_4,X0,e_2)
| product(e_4,X0,e_4) ) ).
cnf(u36493,negated_conjecture,
( ~ product(X0,e_3,e_1)
| equalish(X0,e_2) ) ).
cnf(product_right_cancellation,axiom,
( ~ product(X0,X3,X2)
| ~ product(X0,X1,X2)
| equalish(X1,X3) ) ).
cnf(u19165,negated_conjecture,
( ~ group_element(X1)
| product(e_3,X0,e_4)
| product(e_3,X0,e_3)
| product(e_3,X0,e_2)
| product(e_3,X0,e_1)
| ~ group_element(X0)
| equalish(X0,e_4)
| product(X1,e_4,e_4)
| product(X1,e_4,e_2)
| product(X1,e_4,e_1)
| ~ product(X1,X0,e_3) ) ).
cnf(u19884,negated_conjecture,
( ~ product(e_5,e_4,X0)
| equalish(X0,e_5)
| ~ group_element(X0)
| product(X0,e_4,e_1)
| product(X0,e_4,e_2)
| product(X0,e_4,e_3)
| product(X0,e_4,e_4) ) ).
cnf(u36401,negated_conjecture,
( ~ product(e_1,X0,X1)
| ~ product(X1,X0,e_3)
| equalish(X0,e_1) ) ).
cnf(u29242,negated_conjecture,
( ~ product(e_5,X0,e_2)
| product(e_2,X0,e_3)
| product(e_2,X0,e_2)
| product(e_2,X0,e_1)
| ~ group_element(X0)
| equalish(X0,e_4)
| product(e_2,X0,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) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP131-2.005 : TPTP v9.3.1. Released v1.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.37 % Computer : n026.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sun Sep 27 09:32:59 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.40 Running first-order theorem proving
% 0.10/0.40 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 8.82/2.08 % (2571512)Input is clausal, will run a generic CNF schedule.
% 8.82/2.08 % (2571517)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=1940571593:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 8.82/2.08 % (2571522)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1464258605:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 8.82/2.08 % (2571519)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1629517949:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 8.82/2.08 % (2571520)lrs+10_1_sil=8000:sp=occurrence:random_seed=438319170:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 8.82/2.08 % (2571518)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=3718702605:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 8.82/2.08 % (2571521)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=138997621:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 8.82/2.08 % (2571523)dis-21_1_sil=8000:lcm=predicate:random_seed=1993209277:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 8.82/2.08 % (2571520)Instruction limit reached!
% 8.82/2.08 % (2571520)------------------------------
% 8.82/2.08 % (2571520)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.82/2.08 % (2571520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.82/2.08 % (2571520)CaDiCaL version: 2.1.3
% 8.82/2.08 % (2571520)Termination reason: Instruction limit
% 8.82/2.08 % (2571520)Termination phase: Saturation
% 8.82/2.08 % (2571520)Time elapsed: 0.053 s
% 8.82/2.08 % (2571520)Peak memory usage: 88 MB
% 8.82/2.08 % (2571520)Instructions burned: 108 (million)
% 8.82/2.08 % (2571521)Instruction limit reached!
% 8.82/2.08 % (2571521)------------------------------
% 8.82/2.08 % (2571521)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.82/2.08 % (2571521)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.82/2.08 % (2571521)CaDiCaL version: 2.1.3
% 8.82/2.08 % (2571521)Termination reason: Instruction limit
% 8.82/2.08 % (2571521)Termination phase: Saturation
% 8.82/2.08 % (2571521)Time elapsed: 0.057 s
% 8.82/2.08 % (2571521)Peak memory usage: 88 MB
% 8.82/2.08 % (2571521)Instructions burned: 114 (million)
% 8.82/2.08 % (2571523)Instruction limit reached!
% 8.82/2.08 % (2571523)------------------------------
% 8.82/2.08 % (2571523)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.82/2.08 % (2571523)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.82/2.08 % (2571523)CaDiCaL version: 2.1.3
% 8.82/2.08 % (2571523)Termination reason: Instruction limit
% 8.82/2.08 % (2571523)Termination phase: Saturation
% 8.82/2.08 % (2571523)Time elapsed: 0.069 s
% 8.82/2.08 % (2571523)Peak memory usage: 89 MB
% 8.82/2.08 % (2571523)Instructions burned: 118 (million)
% 8.82/2.08 % (2571522)Instruction limit reached!
% 8.82/2.08 % (2571522)------------------------------
% 8.82/2.08 % (2571522)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.82/2.08 % (2571522)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.82/2.08 % (2571522)CaDiCaL version: 2.1.3
% 8.82/2.08 % (2571522)Termination reason: Instruction limit
% 8.82/2.08 % (2571522)Termination phase: Saturation
% 8.82/2.08 % (2571522)Time elapsed: 0.122 s
% 8.82/2.08 % (2571522)Peak memory usage: 89 MB
% 8.82/2.08 % (2571522)Instructions burned: 181 (million)
% 8.82/2.08 % (2571531)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=186066220:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 8.82/2.08 % (2571532)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=196456287:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 8.82/2.08 % (2571532)Refutation not found, incomplete strategy
% 8.82/2.08 % (2571532)------------------------------
% 8.82/2.08 % (2571532)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.82/2.08 % (2571532)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.82/2.08 % (2571532)CaDiCaL version: 2.1.3
% 13.60/2.91 % (2571532)Termination reason: Refutation not found, incomplete strategy
% 13.60/2.91 % (2571532)Time elapsed: 0.002 s
% 13.60/2.91 % (2571532)Peak memory usage: 87 MB
% 13.60/2.91 % (2571532)Instructions burned: 2 (million)
% 13.60/2.91 % (2571533)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1204163328:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 13.60/2.91 % (2571534)lrs+10_64_to=lpo:sil=8000:random_seed=1009439842:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 13.60/2.91 % (2571531)Instruction limit reached!
% 13.60/2.91 % (2571531)------------------------------
% 13.60/2.91 % (2571531)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.60/2.91 % (2571531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.60/2.91 % (2571531)CaDiCaL version: 2.1.3
% 13.60/2.91 % (2571531)Termination reason: Instruction limit
% 13.60/2.91 % (2571531)Termination phase: Saturation
% 13.60/2.91 % (2571531)Time elapsed: 0.075 s
% 13.60/2.91 % (2571531)Peak memory usage: 88 MB
% 13.60/2.91 % (2571531)Instructions burned: 144 (million)
% 13.60/2.91 % (2571534)Instruction limit reached!
% 13.60/2.91 % (2571534)------------------------------
% 13.60/2.91 % (2571534)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.60/2.91 % (2571534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.60/2.91 % (2571534)CaDiCaL version: 2.1.3
% 13.60/2.91 % (2571534)Termination reason: Instruction limit
% 13.60/2.91 % (2571534)Termination phase: Saturation
% 13.60/2.91 % (2571534)Time elapsed: 0.074 s
% 13.60/2.91 % (2571534)Peak memory usage: 88 MB
% 13.60/2.91 % (2571534)Instructions burned: 126 (million)
% 13.60/2.91 % (2571533)Instruction limit reached!
% 13.60/2.91 % (2571533)------------------------------
% 13.60/2.91 % (2571533)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.60/2.91 % (2571533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.60/2.91 % (2571533)CaDiCaL version: 2.1.3
% 13.60/2.91 % (2571533)Termination reason: Instruction limit
% 13.60/2.91 % (2571533)Termination phase: Saturation
% 13.60/2.91 % (2571533)Time elapsed: 0.113 s
% 13.60/2.91 % (2571533)Peak memory usage: 88 MB
% 13.60/2.91 % (2571533)Instructions burned: 219 (million)
% 13.60/2.91 % (2571539)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1549331756:avsq=on:i=194:fgj=on:bd=preordered_2996 on theBenchmark for (2996ds/194Mi)
% 13.60/2.91 % (2571532)------------------------------
% 13.60/2.91 % (2571532)------------------------------
% 13.60/2.91 % (2571540)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=3390716850:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 13.60/2.91 % (2571541)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=2934327069:i=3394:sd=4:ss=included:sgt=64_2995 on theBenchmark for (2995ds/3394Mi)
% 13.60/2.91 % (2571539)Instruction limit reached!
% 13.60/2.91 % (2571539)------------------------------
% 13.60/2.91 % (2571539)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.60/2.91 % (2571539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.60/2.91 % (2571539)CaDiCaL version: 2.1.3
% 13.60/2.91 % (2571539)Termination reason: Instruction limit
% 13.60/2.91 % (2571539)Termination phase: Saturation
% 13.60/2.91 % (2571539)Time elapsed: 0.119 s
% 13.60/2.91 % (2571539)Peak memory usage: 88 MB
% 13.60/2.91 % (2571539)Instructions burned: 194 (million)
% 13.60/2.91 % (2571540)Instruction limit reached!
% 13.60/2.91 % (2571540)------------------------------
% 13.60/2.91 % (2571540)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.60/2.91 % (2571540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.60/2.91 % (2571540)CaDiCaL version: 2.1.3
% 13.60/2.91 % (2571540)Termination reason: Instruction limit
% 13.60/2.91 % (2571540)Termination phase: Saturation
% 13.60/2.91 % (2571540)Time elapsed: 0.081 s
% 13.60/2.91 % (2571540)Peak memory usage: 88 MB
% 13.60/2.91 % (2571540)Instructions burned: 158 (million)
% 13.60/2.91 % (2571545)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=796682737:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2994 on theBenchmark for (2994ds/106Mi)
% 13.60/2.91 % (2571545)Refutation not found, incomplete strategy
% 13.60/2.91 % (2571545)------------------------------
% 13.60/2.91 % (2571545)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.60/2.91 % (2571545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.99/4.09 % (2571545)CaDiCaL version: 2.1.3
% 22.99/4.09 % (2571545)Termination reason: Refutation not found, incomplete strategy
% 22.99/4.09 % (2571545)Time elapsed: 0.002 s
% 22.99/4.09 % (2571545)Peak memory usage: 88 MB
% 22.99/4.09 % (2571545)Instructions burned: 2 (million)
% 22.99/4.09 % (2571518)Refutation not found, incomplete strategy
% 22.99/4.09 % (2571518)------------------------------
% 22.99/4.09 % (2571518)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.99/4.09 % (2571518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.99/4.09 % (2571518)CaDiCaL version: 2.1.3
% 22.99/4.09 % (2571518)Termination reason: Refutation not found, incomplete strategy
% 22.99/4.09 % (2571518)Time elapsed: 0.606 s
% 22.99/4.09 % (2571518)Peak memory usage: 127 MB
% 22.99/4.09 % (2571518)Instructions burned: 905 (million)
% 22.99/4.09 % (2571546)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3110147705:i=107_2993 on theBenchmark for (2993ds/107Mi)
% 22.99/4.09 % (2571547)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3998065955:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2993 on theBenchmark for (2993ds/242Mi)
% 22.99/4.09 % (2571546)Instruction limit reached!
% 22.99/4.09 % (2571546)------------------------------
% 22.99/4.09 % (2571546)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.99/4.09 % (2571546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.99/4.09 % (2571546)CaDiCaL version: 2.1.3
% 22.99/4.09 % (2571546)Termination reason: Instruction limit
% 22.99/4.09 % (2571546)Termination phase: Saturation
% 22.99/4.09 % (2571546)Time elapsed: 0.052 s
% 22.99/4.09 % (2571546)Peak memory usage: 87 MB
% 22.99/4.09 % (2571546)Instructions burned: 107 (million)
% 22.99/4.09 % (2571547)Instruction limit reached!
% 22.99/4.09 % (2571547)------------------------------
% 22.99/4.09 % (2571547)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.99/4.09 % (2571547)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.99/4.09 % (2571547)CaDiCaL version: 2.1.3
% 22.99/4.09 % (2571547)Termination reason: Instruction limit
% 22.99/4.09 % (2571547)Termination phase: Saturation
% 22.99/4.09 % (2571547)Time elapsed: 0.121 s
% 22.99/4.09 % (2571547)Peak memory usage: 88 MB
% 22.99/4.09 % (2571547)Instructions burned: 243 (million)
% 22.99/4.09 % (2571545)------------------------------
% 22.99/4.09 % (2571545)------------------------------
% 22.99/4.09 % (2571551)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=534351634:cond=fast:i=5208:av=off_2991 on theBenchmark for (2991ds/5208Mi)
% 22.99/4.09 % (2571518)------------------------------
% 22.99/4.09 % (2571518)------------------------------
% 22.99/4.09 % (2571552)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=3370576878:i=134:sd=2:doe=on:ss=axioms:sgt=14_2990 on theBenchmark for (2990ds/134Mi)
% 22.99/4.09 % (2571553)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=1774791225:i=499:bd=all_2990 on theBenchmark for (2990ds/499Mi)
% 22.99/4.09 % (2571555)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=3254568616:i=191:fgj=on:bd=all_2989 on theBenchmark for (2989ds/191Mi)
% 22.99/4.09 % (2571552)Instruction limit reached!
% 22.99/4.09 % (2571552)------------------------------
% 22.99/4.09 % (2571552)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.99/4.09 % (2571552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.99/4.09 % (2571552)CaDiCaL version: 2.1.3
% 22.99/4.09 % (2571552)Termination reason: Instruction limit
% 22.99/4.09 % (2571552)Termination phase: Saturation
% 22.99/4.09 % (2571552)Time elapsed: 0.082 s
% 22.99/4.09 % (2571552)Peak memory usage: 89 MB
% 22.99/4.09 % (2571552)Instructions burned: 135 (million)
% 22.99/4.09 % (2571555)Instruction limit reached!
% 22.99/4.09 % (2571555)------------------------------
% 22.99/4.09 % (2571555)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.99/4.09 % (2571555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.99/4.09 % (2571555)CaDiCaL version: 2.1.3
% 22.99/4.09 % (2571555)Termination reason: Instruction limit
% 22.99/4.09 % (2571555)Termination phase: Saturation
% 22.99/4.09 % (2571555)Time elapsed: 0.109 s
% 22.99/4.09 % (2571555)Peak memory usage: 88 MB
% 22.99/4.09 % (2571555)Instructions burned: 192 (million)
% 35.16/5.92 % (2571559)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3814028378:i=264:kws=precedence:fsr=off_2988 on theBenchmark for (2988ds/264Mi)
% 35.16/5.92 % (2571553)Instruction limit reached!
% 35.16/5.92 % (2571553)------------------------------
% 35.16/5.92 % (2571553)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.16/5.92 % (2571553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.16/5.92 % (2571553)CaDiCaL version: 2.1.3
% 35.16/5.92 % (2571553)Termination reason: Instruction limit
% 35.16/5.92 % (2571553)Termination phase: Saturation
% 35.16/5.92 % (2571553)Time elapsed: 0.249 s
% 35.16/5.92 % (2571553)Peak memory usage: 89 MB
% 35.16/5.92 % (2571553)Instructions burned: 499 (million)
% 35.16/5.92 % (2571560)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=4018509583:cond=on:i=156:bs=on:gtg=exists_all:er=known_2987 on theBenchmark for (2987ds/156Mi)
% 35.16/5.92 % (2571559)Instruction limit reached!
% 35.16/5.92 % (2571559)------------------------------
% 35.16/5.92 % (2571559)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.16/5.92 % (2571559)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.16/5.92 % (2571559)CaDiCaL version: 2.1.3
% 35.16/5.92 % (2571559)Termination reason: Instruction limit
% 35.16/5.92 % (2571559)Termination phase: Saturation
% 35.16/5.92 % (2571559)Time elapsed: 0.152 s
% 35.16/5.92 % (2571559)Peak memory usage: 90 MB
% 35.16/5.92 % (2571559)Instructions burned: 266 (million)
% 35.16/5.92 % (2571560)Instruction limit reached!
% 35.16/5.92 % (2571560)------------------------------
% 35.16/5.92 % (2571560)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.16/5.92 % (2571560)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.16/5.92 % (2571560)CaDiCaL version: 2.1.3
% 35.16/5.92 % (2571560)Termination reason: Instruction limit
% 35.16/5.92 % (2571560)Termination phase: Saturation
% 35.16/5.92 % (2571560)Time elapsed: 0.086 s
% 35.16/5.92 % (2571560)Peak memory usage: 88 MB
% 35.16/5.92 % (2571560)Instructions burned: 157 (million)
% 35.16/5.92 % (2571562)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=4146814759:i=3256:kws=precedence:bd=preordered:av=off_2986 on theBenchmark for (2986ds/3256Mi)
% 35.16/5.92 % (2571564)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=2367714280:i=537:av=off:ss=included_2985 on theBenchmark for (2985ds/537Mi)
% 35.16/5.92 % (2571565)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=1688397502:i=180:bd=preordered:av=off_2985 on theBenchmark for (2985ds/180Mi)
% 35.16/5.92 % (2571565)Instruction limit reached!
% 35.16/5.92 % (2571565)------------------------------
% 35.16/5.92 % (2571565)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.16/5.92 % (2571565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.16/5.92 % (2571565)CaDiCaL version: 2.1.3
% 35.16/5.92 % (2571565)Termination reason: Instruction limit
% 35.16/5.92 % (2571565)Termination phase: Saturation
% 35.16/5.92 % (2571565)Time elapsed: 0.089 s
% 35.16/5.92 % (2571565)Peak memory usage: 87 MB
% 35.16/5.92 % (2571565)Instructions burned: 180 (million)
% 35.16/5.92 % (2571564)Instruction limit reached!
% 35.16/5.92 % (2571564)------------------------------
% 35.16/5.92 % (2571564)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.16/5.92 % (2571564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.16/5.92 % (2571564)CaDiCaL version: 2.1.3
% 35.16/5.92 % (2571564)Termination reason: Instruction limit
% 35.16/5.92 % (2571564)Termination phase: Saturation
% 35.16/5.92 % (2571564)Time elapsed: 0.222 s
% 35.16/5.92 % (2571564)Peak memory usage: 88 MB
% 35.16/5.92 % (2571564)Instructions burned: 539 (million)
% 35.16/5.92 % (2571569)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=613981119:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2983 on theBenchmark for (2983ds/10307Mi)
% 35.16/5.92 % (2571570)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=2124334369:i=412:gtgl=4:gtg=exists_all_2982 on theBenchmark for (2982ds/412Mi)
% 35.16/5.92 % (2571570)Instruction limit reached!
% 35.16/5.92 % (2571570)------------------------------
% 35.16/5.92 % (2571570)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.80/8.13 % (2571570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.80/8.13 % (2571570)CaDiCaL version: 2.1.3
% 48.80/8.13 % (2571570)Termination reason: Instruction limit
% 48.80/8.13 % (2571570)Termination phase: Saturation
% 48.80/8.13 % (2571570)Time elapsed: 0.190 s
% 48.80/8.13 % (2571570)Peak memory usage: 90 MB
% 48.80/8.13 % (2571570)Instructions burned: 412 (million)
% 48.80/8.13 % (2571573)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=3031499340:s2pl=no:i=8478:s2at=4:nm=6_2979 on theBenchmark for (2979ds/8478Mi)
% 48.80/8.13 % (2571541)Instruction limit reached!
% 48.80/8.13 % (2571541)------------------------------
% 48.80/8.13 % (2571541)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.80/8.13 % (2571541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.80/8.13 % (2571541)CaDiCaL version: 2.1.3
% 48.80/8.13 % (2571541)Termination reason: Instruction limit
% 48.80/8.13 % (2571541)Termination phase: Saturation
% 48.80/8.13 % (2571541)Time elapsed: 1.955 s
% 48.80/8.13 % (2571541)Peak memory usage: 134 MB
% 48.80/8.13 % (2571541)Instructions burned: 3396 (million)
% 48.80/8.13 % (2571575)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=178588020:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2974 on theBenchmark for (2974ds/303Mi)
% 48.80/8.13 % (2571573)Refutation not found, incomplete strategy
% 48.80/8.13 % (2571573)------------------------------
% 48.80/8.13 % (2571573)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.80/8.13 % (2571573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.80/8.13 % (2571573)CaDiCaL version: 2.1.3
% 48.80/8.13 % (2571573)Termination reason: Refutation not found, incomplete strategy
% 48.80/8.13 % (2571573)Time elapsed: 0.591 s
% 48.80/8.13 % (2571573)Peak memory usage: 128 MB
% 48.80/8.13 % (2571573)Instructions burned: 906 (million)
% 48.80/8.13 % (2571575)Instruction limit reached!
% 48.80/8.13 % (2571575)------------------------------
% 48.80/8.13 % (2571575)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.80/8.13 % (2571575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.80/8.13 % (2571575)CaDiCaL version: 2.1.3
% 48.80/8.13 % (2571575)Termination reason: Instruction limit
% 48.80/8.13 % (2571575)Termination phase: Saturation
% 48.80/8.13 % (2571575)Time elapsed: 0.168 s
% 48.80/8.13 % (2571575)Peak memory usage: 90 MB
% 48.80/8.13 % (2571575)Instructions burned: 305 (million)
% 48.80/8.13 % (2571577)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=3021868083:st=4:i=720:sd=3:fsr=off:ss=axioms_2971 on theBenchmark for (2971ds/720Mi)
% 48.80/8.13 % (2571577)Refutation not found, incomplete strategy
% 48.80/8.13 % (2571577)------------------------------
% 48.80/8.13 % (2571577)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.80/8.13 % (2571577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.80/8.13 % (2571577)CaDiCaL version: 2.1.3
% 48.80/8.13 % (2571577)Termination reason: Refutation not found, incomplete strategy
% 48.80/8.13 % (2571577)Time elapsed: 0.001 s
% 48.80/8.13 % (2571577)Peak memory usage: 87 MB
% 48.80/8.13 % (2571577)Instructions burned: 1 (million)
% 48.80/8.13 % (2571573)------------------------------
% 48.80/8.13 % (2571573)------------------------------
% 48.80/8.13 % (2571579)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=2472469024:i=598:bs=on:bd=preordered:av=off:ss=axioms_2969 on theBenchmark for (2969ds/598Mi)
% 48.80/8.13 % (2571579)Refutation not found, incomplete strategy
% 48.80/8.13 % (2571579)------------------------------
% 48.80/8.13 % (2571579)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.80/8.13 % (2571579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.80/8.13 % (2571579)CaDiCaL version: 2.1.3
% 48.80/8.13 % (2571579)Termination reason: Refutation not found, incomplete strategy
% 48.80/8.13 % (2571579)Time elapsed: 0.0000 s
% 48.80/8.13 % (2571579)Peak memory usage: 86 MB
% 48.80/8.13 % (2571577)------------------------------
% 48.80/8.13 % (2571577)------------------------------
% 48.80/8.13 % (2571562)Instruction limit reached!
% 48.80/8.13 % (2571562)------------------------------
% 48.80/8.13 % (2571562)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.48/11.23 % (2571562)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.48/11.23 % (2571562)CaDiCaL version: 2.1.3
% 70.48/11.23 % (2571562)Termination reason: Instruction limit
% 70.48/11.23 % (2571562)Termination phase: Saturation
% 70.48/11.23 % (2571562)Time elapsed: 1.773 s
% 70.48/11.23 % (2571562)Peak memory usage: 134 MB
% 70.48/11.23 % (2571562)Instructions burned: 3258 (million)
% 70.48/11.23 % (2571581)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=4085365987:i=2989:sd=3:ss=axioms:sgt=60_2967 on theBenchmark for (2967ds/2989Mi)
% 70.48/11.23 % (2571582)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=3892557128:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2967 on theBenchmark for (2967ds/1997Mi)
% 70.48/11.23 % (2571579)------------------------------
% 70.48/11.23 % (2571579)------------------------------
% 70.48/11.23 % (2571585)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=3776472642:i=2088:bd=preordered:av=off_2965 on theBenchmark for (2965ds/2088Mi)
% 70.48/11.23 % (2571551)Instruction limit reached!
% 70.48/11.23 % (2571551)------------------------------
% 70.48/11.23 % (2571551)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.48/11.23 % (2571551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.48/11.23 % (2571551)CaDiCaL version: 2.1.3
% 70.48/11.23 % (2571551)Termination reason: Instruction limit
% 70.48/11.23 % (2571551)Termination phase: Saturation
% 70.48/11.23 % (2571551)Time elapsed: 3.048 s
% 70.48/11.23 % (2571551)Peak memory usage: 135 MB
% 70.48/11.23 % (2571551)Instructions burned: 5209 (million)
% 70.48/11.23 % (2571587)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=847617115:i=1098:nicw=on_2959 on theBenchmark for (2959ds/1098Mi)
% 70.48/11.23 % (2571587)Instruction limit reached!
% 70.48/11.23 % (2571587)------------------------------
% 70.48/11.23 % (2571587)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.48/11.23 % (2571587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.48/11.23 % (2571587)CaDiCaL version: 2.1.3
% 70.48/11.23 % (2571587)Termination reason: Instruction limit
% 70.48/11.23 % (2571587)Termination phase: Saturation
% 70.48/11.23 % (2571587)Time elapsed: 0.571 s
% 70.48/11.23 % (2571587)Peak memory usage: 90 MB
% 70.48/11.23 % (2571587)Instructions burned: 1098 (million)
% 70.48/11.23 % (2571582)Instruction limit reached!
% 70.48/11.23 % (2571582)------------------------------
% 70.48/11.23 % (2571582)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.48/11.23 % (2571582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.48/11.23 % (2571582)CaDiCaL version: 2.1.3
% 70.48/11.23 % (2571582)Termination reason: Instruction limit
% 70.48/11.23 % (2571582)Termination phase: Saturation
% 70.48/11.23 % (2571582)Time elapsed: 1.408 s
% 70.48/11.23 % (2571582)Peak memory usage: 133 MB
% 70.48/11.23 % (2571582)Instructions burned: 1998 (million)
% 70.48/11.23 % (2571589)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=3845889789:i=433:bd=preordered_2952 on theBenchmark for (2952ds/433Mi)
% 70.48/11.23 % (2571585)Instruction limit reached!
% 70.48/11.23 % (2571585)------------------------------
% 70.48/11.23 % (2571585)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 70.48/11.23 % (2571585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 70.48/11.23 % (2571585)CaDiCaL version: 2.1.3
% 70.48/11.23 % (2571585)Termination reason: Instruction limit
% 70.48/11.23 % (2571585)Termination phase: Saturation
% 70.48/11.23 % (2571585)Time elapsed: 1.327 s
% 70.48/11.23 % (2571585)Peak memory usage: 133 MB
% 70.48/11.23 % (2571585)Instructions burned: 2088 (million)
% 70.48/11.23 % (2571590)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=3477933070:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2952 on theBenchmark for (2952ds/2942Mi)
% 70.48/11.23 % (2571592)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=1356769152:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2951 on theBenchmark for (2951ds/6922Mi)
% 70.48/11.23 % (2571589)Instruction limit reached!
% 70.48/11.23 % (2571589)------------------------------
% 72.30/11.55 % (2571589)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 72.30/11.55 % (2571589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 72.30/11.55 % (2571589)CaDiCaL version: 2.1.3
% 72.30/11.55 % (2571589)Termination reason: Instruction limit
% 72.30/11.55 % (2571589)Termination phase: Saturation
% 72.30/11.55 % (2571589)Time elapsed: 0.245 s
% 72.30/11.55 % (2571589)Peak memory usage: 89 MB
% 72.30/11.55 % (2571589)Instructions burned: 435 (million)
% 72.30/11.55 % (2571595)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=3654598391:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2949 on theBenchmark for (2949ds/596Mi)
% 72.30/11.55 % (2571595)Refutation not found, incomplete strategy
% 72.30/11.55 % (2571595)------------------------------
% 72.30/11.55 % (2571595)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 72.30/11.55 % (2571595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 72.30/11.55 % (2571595)CaDiCaL version: 2.1.3
% 72.30/11.55 % (2571595)Termination reason: Refutation not found, incomplete strategy
% 72.30/11.55 % (2571595)Time elapsed: 0.002 s
% 72.30/11.55 % (2571595)Peak memory usage: 88 MB
% 72.30/11.55 % (2571595)Instructions burned: 2 (million)
% 72.30/11.55 % (2571581)Instruction limit reached!
% 72.30/11.55 % (2571581)------------------------------
% 72.30/11.55 % (2571581)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 72.30/11.55 % (2571581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 72.30/11.55 % (2571581)CaDiCaL version: 2.1.3
% 72.30/11.55 % (2571581)Termination reason: Instruction limit
% 72.30/11.55 % (2571581)Termination phase: Saturation
% 72.30/11.55 % (2571581)Time elapsed: 1.976 s
% 72.30/11.55 % (2571581)Peak memory usage: 138 MB
% 72.30/11.55 % (2571581)Instructions burned: 2990 (million)
% 72.30/11.55 % (2571595)------------------------------
% 72.30/11.55 % (2571595)------------------------------
% 72.30/11.55 % (2571597)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=2351484555:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2946 on theBenchmark for (2946ds/4123Mi)
% 72.30/11.55 % (2571592)Refutation not found, incomplete strategy
% 72.30/11.55 % (2571592)------------------------------
% 72.30/11.55 % (2571592)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 72.30/11.55 % (2571592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 72.30/11.55 % (2571592)CaDiCaL version: 2.1.3
% 72.30/11.55 % (2571592)Termination reason: Refutation not found, incomplete strategy
% 72.30/11.55 % (2571592)Time elapsed: 1.235 s
% 72.30/11.55 % (2571592)Peak memory usage: 127 MB
% 72.30/11.55 % (2571592)Instructions burned: 901 (million)
% 72.30/11.55 % (2571598)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=1002800555:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2945 on theBenchmark for (2945ds/16411Mi)
% 72.30/11.55 % (2571569)Instruction limit reached!
% 72.30/11.55 % (2571569)------------------------------
% 72.30/11.55 % (2571569)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 72.30/11.55 % (2571569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 72.30/11.55 % (2571569)CaDiCaL version: 2.1.3
% 72.30/11.55 % (2571569)Termination reason: Instruction limit
% 72.30/11.55 % (2571569)Termination phase: Saturation
% 72.30/11.55 % (2571569)Time elapsed: 4.600 s
% 72.30/11.55 % (2571569)Peak memory usage: 136 MB
% 72.30/11.55 % (2571569)Instructions burned: 10309 (million)
% 72.30/11.55 % (2571592)------------------------------
% 72.30/11.55 % (2571592)------------------------------
% 72.30/11.55 % (2571601)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=2326720445:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2935 on theBenchmark for (2935ds/1670Mi)
% 72.30/11.55 % (2571602)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=974303122:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2934 on theBenchmark for (2934ds/1722Mi)
% 72.30/11.55 % (2571590)Instruction limit reached!
% 72.30/11.55 % (2571590)------------------------------
% 72.30/11.55 % (2571590)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 72.30/11.55 % (2571590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 72.30/11.55 % (2571590)CaDiCaL version: 2.1.3
% 72.30/11.55 % (2571590)Termination reason: Instruction limit
% 72.30/11.55 % (2571590)Termination phase: Saturation
% 72.30/11.55 % (2571590)Time elapsed: 2.377 s
% 72.30/11.55 % (2571590)Peak memory usage: 134 MB
% 72.30/11.55 % (2571590)Instructions burned: 2943 (million)
% 72.30/11.55 % (2571605)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=1452612774:cts=off:cond=on:i=9530:bs=on:fsd=on_2926 on theBenchmark for (2926ds/9530Mi)
% 72.30/11.55 % (2571601)Instruction limit reached!
% 72.30/11.55 % (2571601)------------------------------
% 72.30/11.55 % (2571601)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 72.30/11.55 % (2571601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 72.30/11.55 % (2571601)CaDiCaL version: 2.1.3
% 72.30/11.55 % (2571601)Termination reason: Instruction limit
% 72.30/11.55 % (2571601)Termination phase: Saturation
% 72.30/11.55 % (2571601)Time elapsed: 0.980 s
% 72.30/11.55 % (2571601)Peak memory usage: 132 MB
% 72.30/11.55 % (2571601)Instructions burned: 1671 (million)
% 72.30/11.55 % (2571607)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=3858221291:st=2:i=4495:sd=10:ss=included_2924 on theBenchmark for (2924ds/4495Mi)
% 72.30/11.55 % (2571602)Instruction limit reached!
% 72.30/11.55 % (2571602)------------------------------
% 72.30/11.55 % (2571602)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 72.30/11.55 % (2571602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 72.30/11.55 % (2571602)CaDiCaL version: 2.1.3
% 72.30/11.55 % (2571602)Termination reason: Instruction limit
% 72.30/11.55 % (2571602)Termination phase: Saturation
% 72.30/11.55 % (2571602)Time elapsed: 1.170 s
% 72.30/11.55 % (2571602)Peak memory usage: 133 MB
% 72.30/11.55 % (2571602)Instructions burned: 1723 (million)
% 72.30/11.55 % (2571609)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=398581297:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2921 on theBenchmark for (2921ds/4920Mi)
% 72.30/11.55 % (2571597)Instruction limit reached!
% 72.30/11.55 % (2571597)------------------------------
% 72.30/11.55 % (2571597)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 72.30/11.55 % (2571597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 72.30/11.55 % (2571597)CaDiCaL version: 2.1.3
% 72.30/11.55 % (2571597)Termination reason: Instruction limit
% 72.30/11.55 % (2571597)Termination phase: Saturation
% 72.30/11.55 % (2571597)Time elapsed: 2.482 s
% 72.30/11.55 % (2571597)Peak memory usage: 136 MB
% 72.30/11.55 % (2571597)Instructions burned: 4125 (million)
% 72.30/11.55 % (2571611)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=2456241899:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2913 on theBenchmark for (2913ds/2083Mi)
% 72.30/11.55 % (2571611)Instruction limit reached!
% 72.30/11.55 % (2571611)------------------------------
% 72.30/11.55 % (2571611)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 72.30/11.55 % (2571611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 72.30/11.55 % (2571611)CaDiCaL version: 2.1.3
% 72.30/11.55 % (2571611)Termination reason: Instruction limit
% 72.30/11.55 % (2571611)Termination phase: Saturation
% 72.30/11.55 % (2571611)Time elapsed: 1.104 s
% 72.30/11.55 % (2571611)Peak memory usage: 130 MB
% 72.30/11.55 % (2571611)Instructions burned: 2083 (million)
% 72.30/11.55 % (2571613)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=2458442098:i=4629:av=off:gsp=on_2900 on theBenchmark for (2900ds/4629Mi)
% 72.30/11.55 % (2571607)Instruction limit reached!
% 72.30/11.55 % (2571607)------------------------------
% 72.30/11.55 % (2571607)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 72.30/11.55 % (2571607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 72.30/11.55 % (2571607)CaDiCaL version: 2.1.3
% 72.30/11.55 % (2571607)Termination reason: Instruction limit
% 72.30/11.55 % (2571607)Termination phase: Saturation
% 72.30/11.55 % (2571607)Time elapsed: 2.619 s
% 72.30/11.55 % (2571607)Peak memory usage: 138 MB
% 72.30/11.55 % (2571607)Instructions burned: 4496 (million)
% 72.30/11.55 % (2571615)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=2217593250:i=1258:av=off_2897 on theBenchmark for (2897ds/1258Mi)
% 72.30/11.55 % (2571598)First to succeed.
% 72.30/11.55 % (2571598)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2571512"
% 72.30/11.55 % (2571609)Instruction limit reached!
% 72.30/11.55 % (2571609)------------------------------
% 72.30/11.55 % (2571609)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 72.30/11.55 % (2571609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 72.30/11.55 % (2571609)CaDiCaL version: 2.1.3
% 72.30/11.55 % (2571609)Termination reason: Instruction limit
% 72.30/11.55 % (2571609)Termination phase: Saturation
% 72.30/11.55 % (2571609)Time elapsed: 2.700 s
% 72.30/11.55 % (2571609)Peak memory usage: 143 MB
% 72.30/11.55 % (2571609)Instructions burned: 4920 (million)
% 72.30/11.55 % SZS status Satisfiable for theBenchmark
% 72.30/11.55 % SZS output start Saturation.
% See solution above
% 73.22/11.75 % SZS output start Definitions and Model Updates.
% 73.22/11.75 % SZS output end Definitions and Model Updates.
% 73.22/11.75 % (2571598)------------------------------
% 73.22/11.75 % (2571598)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 73.22/11.75 % (2571598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.22/11.75 % (2571598)CaDiCaL version: 2.1.3
% 73.22/11.75 % (2571598)Termination reason: Satisfiable
% 73.22/11.75 % (2571598)Time elapsed: 4.122 s
% 73.22/11.75 % (2571598)Peak memory usage: 152 MB
% 73.22/11.75 % (2571598)Instructions burned: 6207 (million)
% 73.22/11.75 % (2571598)------------------------------
% 73.22/11.75 % (2571598)------------------------------
% 73.22/11.75 % (2571512)Success in time 10.72 s
% 73.22/11.75 % Vampire exiting
%------------------------------------------------------------------------------