%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP129-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 : n002.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 10:12:59 AM UTC 2026
% Result : Satisfiable 44.97s 7.43s
% Output : Saturation 47.22s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u61,negated_conjecture,
product(e_5,e_5,e_5) ).
cnf(u68,negated_conjecture,
~ product(e_5,e_4,e_5) ).
cnf(u72,negated_conjecture,
( ~ group_element(X0)
| product(X0,e_5,e_1)
| product(e_4,X0,e_4)
| product(e_4,X0,e_3)
| product(e_4,X0,e_2)
| product(e_4,X0,e_1)
| product(X0,e_5,e_2)
| product(X0,e_5,e_4)
| product(X0,e_5,e_3) ) ).
cnf(u76,negated_conjecture,
~ product(e_5,e_3,e_5) ).
cnf(u80,negated_conjecture,
( ~ group_element(X0)
| product(X0,e_5,e_1)
| product(e_3,X0,e_4)
| product(e_3,X0,e_3)
| product(e_3,X0,e_2)
| product(e_3,X0,e_1)
| product(X0,e_5,e_2)
| product(X0,e_5,e_4)
| product(X0,e_5,e_3) ) ).
cnf(u84,negated_conjecture,
~ product(e_5,e_2,e_5) ).
cnf(u88,negated_conjecture,
( ~ group_element(X0)
| product(X0,e_5,e_1)
| product(e_2,X0,e_4)
| product(e_2,X0,e_3)
| product(e_2,X0,e_2)
| product(e_2,X0,e_1)
| product(X0,e_5,e_2)
| product(X0,e_5,e_4)
| product(X0,e_5,e_3) ) ).
cnf(u92,negated_conjecture,
~ product(e_5,e_1,e_5) ).
cnf(u96,negated_conjecture,
( ~ group_element(X0)
| product(X0,e_5,e_1)
| product(e_1,X0,e_4)
| product(e_1,X0,e_3)
| product(e_1,X0,e_2)
| product(e_1,X0,e_1)
| product(X0,e_5,e_2)
| product(X0,e_5,e_4)
| product(X0,e_5,e_3) ) ).
cnf(u107,negated_conjecture,
~ product(e_2,e_5,e_4) ).
cnf(u111,negated_conjecture,
~ product(e_2,e_5,e_3) ).
cnf(u115,negated_conjecture,
~ product(e_2,e_5,e_2) ).
cnf(u120,negated_conjecture,
product(e_2,e_5,e_1) ).
cnf(u131,negated_conjecture,
~ product(e_1,e_5,e_4) ).
cnf(u135,negated_conjecture,
~ product(e_1,e_5,e_3) ).
cnf(u140,negated_conjecture,
product(e_1,e_5,e_2) ).
cnf(u143,negated_conjecture,
~ product(e_1,e_5,e_1) ).
cnf(u156,negated_conjecture,
product(e_3,e_5,e_4) ).
cnf(u159,negated_conjecture,
~ product(e_3,e_5,e_3) ).
cnf(u163,negated_conjecture,
~ product(e_3,e_5,e_2) ).
cnf(u167,negated_conjecture,
~ product(e_3,e_5,e_1) ).
cnf(u187,negated_conjecture,
product(e_5,e_1,e_4) ).
cnf(u190,negated_conjecture,
~ product(e_5,e_1,e_3) ).
cnf(u194,negated_conjecture,
~ product(e_5,e_1,e_2) ).
cnf(u198,negated_conjecture,
~ product(e_5,e_1,e_1) ).
cnf(u211,negated_conjecture,
~ product(e_5,e_2,e_4) ).
cnf(u216,negated_conjecture,
product(e_5,e_2,e_3) ).
cnf(u219,negated_conjecture,
~ product(e_5,e_2,e_2) ).
cnf(u223,negated_conjecture,
~ product(e_5,e_2,e_1) ).
cnf(u285,negated_conjecture,
~ product(e_4,e_5,e_4) ).
cnf(u290,negated_conjecture,
product(e_4,e_5,e_3) ).
cnf(u293,negated_conjecture,
~ product(e_4,e_5,e_2) ).
cnf(u297,negated_conjecture,
~ product(e_4,e_5,e_1) ).
cnf(u310,negated_conjecture,
~ product(e_5,e_4,e_4) ).
cnf(u314,negated_conjecture,
~ product(e_5,e_4,e_3) ).
cnf(u319,negated_conjecture,
product(e_5,e_4,e_2) ).
cnf(u322,negated_conjecture,
~ product(e_5,e_4,e_1) ).
cnf(u378,negated_conjecture,
~ product(e_5,e_5,e_4) ).
cnf(u382,negated_conjecture,
~ product(e_5,e_5,e_3) ).
cnf(u386,negated_conjecture,
~ product(e_5,e_5,e_2) ).
cnf(u390,negated_conjecture,
~ product(e_5,e_5,e_1) ).
cnf(u399,negated_conjecture,
~ product(e_5,e_3,e_4) ).
cnf(u403,negated_conjecture,
~ product(e_5,e_3,e_3) ).
cnf(u407,negated_conjecture,
~ product(e_5,e_3,e_2) ).
cnf(u412,negated_conjecture,
product(e_5,e_3,e_1) ).
cnf(u430,negated_conjecture,
~ product(e_4,e_5,e_5) ).
cnf(u434,negated_conjecture,
~ product(e_2,e_4,e_4) ).
cnf(u438,negated_conjecture,
~ product(e_2,e_4,e_3) ).
cnf(u442,negated_conjecture,
~ product(e_2,e_4,e_2) ).
cnf(u446,negated_conjecture,
~ product(e_2,e_4,e_1) ).
cnf(u458,negated_conjecture,
~ product(e_3,e_5,e_5) ).
cnf(u463,negated_conjecture,
product(e_2,e_3,e_4) ).
cnf(u466,negated_conjecture,
~ product(e_2,e_3,e_3) ).
cnf(u470,negated_conjecture,
~ product(e_2,e_3,e_2) ).
cnf(u474,negated_conjecture,
~ product(e_2,e_3,e_1) ).
cnf(u486,negated_conjecture,
~ product(e_2,e_5,e_5) ).
cnf(u490,negated_conjecture,
~ product(e_2,e_2,e_4) ).
cnf(u494,negated_conjecture,
~ product(e_2,e_2,e_3) ).
cnf(u499,negated_conjecture,
product(e_2,e_2,e_2) ).
cnf(u502,negated_conjecture,
~ product(e_2,e_2,e_1) ).
cnf(u514,negated_conjecture,
~ product(e_1,e_5,e_5) ).
cnf(u518,negated_conjecture,
~ product(e_2,e_1,e_4) ).
cnf(u523,negated_conjecture,
product(e_2,e_1,e_3) ).
cnf(u526,negated_conjecture,
~ product(e_2,e_1,e_2) ).
cnf(u530,negated_conjecture,
~ product(e_2,e_1,e_1) ).
cnf(u547,negated_conjecture,
~ product(e_1,e_4,e_4) ).
cnf(u552,negated_conjecture,
product(e_1,e_4,e_3) ).
cnf(u555,negated_conjecture,
~ product(e_1,e_4,e_2) ).
cnf(u559,negated_conjecture,
~ product(e_1,e_4,e_1) ).
cnf(u678,negated_conjecture,
product(e_4,e_1,e_5) ).
cnf(u714,negated_conjecture,
~ product(e_4,e_3,e_4) ).
cnf(u718,negated_conjecture,
~ product(e_4,e_3,e_3) ).
cnf(u723,negated_conjecture,
product(e_4,e_3,e_2) ).
cnf(u726,negated_conjecture,
~ product(e_4,e_3,e_1) ).
cnf(u808,negated_conjecture,
~ product(e_4,e_2,e_5) ).
cnf(u820,negated_conjecture,
~ product(e_2,e_2,e_5) ).
cnf(u825,negated_conjecture,
product(e_1,e_2,e_4) ).
cnf(u828,negated_conjecture,
~ product(e_1,e_2,e_3) ).
cnf(u832,negated_conjecture,
~ product(e_1,e_2,e_2) ).
cnf(u836,negated_conjecture,
~ product(e_1,e_2,e_1) ).
cnf(u861,negated_conjecture,
~ product(e_4,e_2,e_4) ).
cnf(u865,negated_conjecture,
~ product(e_4,e_2,e_3) ).
cnf(u869,negated_conjecture,
~ product(e_4,e_2,e_2) ).
cnf(u874,negated_conjecture,
product(e_4,e_2,e_1) ).
cnf(u895,negated_conjecture,
~ product(e_3,e_4,e_4) ).
cnf(u899,negated_conjecture,
~ product(e_3,e_4,e_3) ).
cnf(u903,negated_conjecture,
~ product(e_3,e_4,e_2) ).
cnf(u908,negated_conjecture,
product(e_3,e_4,e_1) ).
cnf(u920,negated_conjecture,
product(e_1,e_3,e_5) ).
cnf(u923,negated_conjecture,
~ product(e_4,e_1,e_4) ).
cnf(u927,negated_conjecture,
~ product(e_4,e_1,e_3) ).
cnf(u931,negated_conjecture,
~ product(e_4,e_1,e_2) ).
cnf(u935,negated_conjecture,
~ product(e_4,e_1,e_1) ).
cnf(u950,negated_conjecture,
~ product(e_4,e_4,e_5) ).
cnf(u975,negated_conjecture,
~ product(e_1,e_3,e_4) ).
cnf(u979,negated_conjecture,
~ product(e_1,e_3,e_3) ).
cnf(u983,negated_conjecture,
~ product(e_1,e_3,e_2) ).
cnf(u987,negated_conjecture,
~ product(e_1,e_3,e_1) ).
cnf(u1010,negated_conjecture,
~ product(e_1,e_1,e_5) ).
cnf(u1014,negated_conjecture,
~ product(e_3,e_1,e_4) ).
cnf(u1018,negated_conjecture,
~ product(e_3,e_1,e_3) ).
cnf(u1023,negated_conjecture,
product(e_3,e_1,e_2) ).
cnf(u1026,negated_conjecture,
~ product(e_3,e_1,e_1) ).
cnf(u1038,negated_conjecture,
~ product(e_4,e_3,e_5) ).
cnf(u1066,negated_conjecture,
~ product(e_1,e_2,e_5) ).
cnf(u1070,negated_conjecture,
~ product(e_1,e_1,e_4) ).
cnf(u1074,negated_conjecture,
~ product(e_1,e_1,e_3) ).
cnf(u1078,negated_conjecture,
~ product(e_1,e_1,e_2) ).
cnf(u1083,negated_conjecture,
product(e_1,e_1,e_1) ).
cnf(u1094,negated_conjecture,
~ product(e_2,e_1,e_5) ).
cnf(u1098,negated_conjecture,
~ product(e_3,e_2,e_4) ).
cnf(u1102,negated_conjecture,
~ product(e_3,e_2,e_3) ).
cnf(u1106,negated_conjecture,
~ product(e_3,e_2,e_2) ).
cnf(u1110,negated_conjecture,
~ product(e_3,e_2,e_1) ).
cnf(u1137,negated_conjecture,
~ product(e_2,e_3,e_5) ).
cnf(u1235,negated_conjecture,
product(e_2,e_4,e_5) ).
cnf(u1255,negated_conjecture,
product(e_3,e_2,e_5) ).
cnf(u1516,negated_conjecture,
product(e_4,e_4,e_4) ).
cnf(u1519,negated_conjecture,
~ product(e_4,e_4,e_3) ).
cnf(u1523,negated_conjecture,
~ product(e_4,e_4,e_2) ).
cnf(u1527,negated_conjecture,
~ product(e_4,e_4,e_1) ).
cnf(u1631,negated_conjecture,
~ product(e_3,e_3,e_4) ).
cnf(u1636,negated_conjecture,
product(e_3,e_3,e_3) ).
cnf(u1639,negated_conjecture,
~ product(e_3,e_3,e_2) ).
cnf(u1643,negated_conjecture,
~ product(e_3,e_3,e_1) ).
cnf(u8211,negated_conjecture,
( ~ product(e_3,e_5,X0)
| equalish(X0,e_4) ) ).
cnf(u8101,negated_conjecture,
( ~ product(e_2,e_1,X0)
| equalish(X0,e_3) ) ).
cnf(e_1_is_not_e_2,axiom,
~ equalish(e_1,e_2) ).
cnf(u8087,negated_conjecture,
( ~ product(X0,e_5,e_2)
| product(e_2,X0,e_3) ) ).
cnf(e_3_is_not_e_5,axiom,
~ equalish(e_3,e_5) ).
cnf(u8245,negated_conjecture,
( ~ product(X0,e_4,e_1)
| product(e_1,X0,e_5) ) ).
cnf(e_5_is_not_e_2,axiom,
~ equalish(e_5,e_2) ).
cnf(u8326,negated_conjecture,
( ~ product(e_1,X0,e_1)
| equalish(X0,e_1) ) ).
cnf(u8493,axiom,
( ~ group_element(X1)
| equalish(X0,e_5)
| product(e_1,X1,e_1)
| product(e_1,X1,e_2)
| product(e_1,X1,e_3)
| product(e_1,X1,e_4)
| ~ product(e_1,X1,X0) ) ).
cnf(u8260,negated_conjecture,
( ~ group_element(X0)
| product(X0,e_3,e_1)
| product(X0,e_3,e_2)
| product(X0,e_3,e_3)
| product(X0,e_3,e_4)
| product(e_5,X0,e_4) ) ).
cnf(u8249,negated_conjecture,
( ~ product(e_2,X0,e_5)
| equalish(X0,e_4) ) ).
cnf(u8008,negated_conjecture,
( ~ product(X0,e_4,e_2)
| product(e_2,X0,e_1) ) ).
cnf(u7995,negated_conjecture,
( ~ product(X0,e_3,e_2)
| equalish(X0,e_4) ) ).
cnf(u8132,negated_conjecture,
( ~ product(e_5,e_3,X0)
| equalish(X0,e_1) ) ).
cnf(u8029,negated_conjecture,
( ~ product(X0,e_1,e_2)
| product(e_2,X0,e_4) ) ).
cnf(u8428,negated_conjecture,
( ~ group_element(X0)
| product(X0,e_3,e_1)
| product(X0,e_3,e_2)
| product(X0,e_3,e_3)
| product(X0,e_3,e_4)
| equalish(X0,e_1) ) ).
cnf(u8231,negated_conjecture,
( ~ product(X0,e_5,e_3)
| equalish(X0,e_4) ) ).
cnf(u8521,axiom,
( ~ group_element(X1)
| product(e_5,X0,e_1)
| product(e_5,X0,e_2)
| product(e_5,X0,e_3)
| product(e_5,X0,e_4)
| equalish(X1,X0)
| ~ group_element(X0)
| 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(u8264,negated_conjecture,
( ~ product(e_3,X0,e_5)
| equalish(X0,e_2) ) ).
cnf(u8579,negated_conjecture,
( ~ 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)
| equalish(e_2,X0) ) ).
cnf(e_4_greater_e_1,axiom,
greater(e_4,e_1) ).
cnf(e_2_greater_e_1,axiom,
greater(e_2,e_1) ).
cnf(u8486,axiom,
( ~ group_element(X1)
| equalish(X0,e_4)
| product(e_4,X1,e_1)
| product(e_4,X1,e_2)
| product(e_4,X1,e_3)
| product(e_4,X1,e_4)
| ~ product(X0,X1,e_5) ) ).
cnf(u8195,negated_conjecture,
( ~ group_element(X0)
| equalish(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) ) ).
cnf(element_1,axiom,
group_element(e_1) ).
cnf(e_1_is_not_e_3,axiom,
~ equalish(e_1,e_3) ).
cnf(qg3,negated_conjecture,
( ~ product(X1,X2,X3)
| ~ product(X0,X1,X2)
| product(X2,X0,X3) ) ).
cnf(u8086,negated_conjecture,
( ~ product(e_5,X0,e_3)
| equalish(X0,e_2) ) ).
cnf(u8064,negated_conjecture,
( ~ product(e_5,X0,e_5)
| equalish(X0,e_5) ) ).
cnf(e_4_is_not_e_3,axiom,
~ equalish(e_4,e_3) ).
cnf(u5520,negated_conjecture,
equalish(e_1,e_1) ).
cnf(u8490,axiom,
( ~ product(e_3,X0,e_5)
| ~ group_element(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(X0,X1) ) ).
cnf(u8288,negated_conjecture,
( ~ product(X0,e_3,e_3)
| product(e_3,X0,e_3) ) ).
cnf(u8286,negated_conjecture,
( ~ product(X0,e_3,e_3)
| equalish(X0,e_3) ) ).
cnf(u8250,negated_conjecture,
( ~ product(X0,e_2,e_4)
| product(e_4,X0,e_5) ) ).
cnf(u8620,negated_conjecture,
~ greater(e_3,e_3) ).
cnf(u8114,negated_conjecture,
( ~ product(e_1,e_4,X0)
| equalish(X0,e_3) ) ).
cnf(u8007,negated_conjecture,
( ~ product(e_4,X0,e_1)
| equalish(X0,e_2) ) ).
cnf(u8011,negated_conjecture,
( ~ product(X0,e_4,e_4)
| equalish(X0,e_4) ) ).
cnf(u8135,negated_conjecture,
( ~ product(X0,e_5,e_3)
| product(e_3,X0,e_1) ) ).
cnf(u8159,negated_conjecture,
( ~ group_element(X0)
| product(X0,e_5,e_1)
| product(X0,e_5,e_2)
| product(X0,e_5,e_3)
| product(X0,e_5,e_4)
| product(e_5,X0,e_5) ) ).
cnf(u8219,negated_conjecture,
( ~ product(X0,e_1,e_4)
| equalish(X0,e_5) ) ).
cnf(u8351,negated_conjecture,
( ~ product(e_1,X0,e_5)
| equalish(X0,e_3) ) ).
cnf(u8584,axiom,
( ~ group_element(X1)
| product(e_4,X0,e_1)
| product(e_4,X0,e_2)
| product(e_4,X0,e_3)
| product(e_4,X0,e_4)
| equalish(X1,X0)
| ~ group_element(X0)
| 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(u8575,axiom,
( ~ group_element(X1)
| product(e_2,X0,e_1)
| product(e_2,X0,e_2)
| product(e_2,X0,e_3)
| product(e_2,X0,e_4)
| equalish(X1,X0)
| ~ group_element(X0)
| 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(u8317,negated_conjecture,
( ~ product(X0,e_3,e_4)
| product(e_4,X0,e_1) ) ).
cnf(u8042,negated_conjecture,
( ~ product(X0,e_1,e_2)
| equalish(X0,e_3) ) ).
cnf(e_3_greater_e_1,axiom,
greater(e_3,e_1) ).
cnf(e_3_is_not_e_1,axiom,
~ equalish(e_3,e_1) ).
cnf(u8487,axiom,
( ~ group_element(X1)
| equalish(X0,e_5)
| product(e_5,X1,e_1)
| product(e_5,X1,e_2)
| product(e_5,X1,e_3)
| product(e_5,X1,e_4)
| ~ product(X0,X1,e_5) ) ).
cnf(u8230,negated_conjecture,
( ~ product(e_4,e_5,X0)
| equalish(X0,e_3) ) ).
cnf(element_4,axiom,
group_element(e_4) ).
cnf(u8615,axiom,
( ~ greater(X0,e_4)
| ~ product(e_3,e_1,X0) ) ).
cnf(u46,negated_conjecture,
( ~ product(X2,X1,X0)
| product(X1,X0,e_1)
| product(X1,X0,e_2)
| product(X1,X0,e_3)
| product(X1,X0,e_4)
| ~ group_element(X1)
| ~ group_element(X0)
| product(X0,X2,e_5) ) ).
cnf(u8475,negated_conjecture,
( ~ group_element(X0)
| equalish(X0,e_4)
| 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(u8080,negated_conjecture,
( ~ product(e_1,X0,e_2)
| equalish(X0,e_5) ) ).
cnf(u8243,negated_conjecture,
( ~ product(X0,e_1,e_5)
| equalish(X0,e_4) ) ).
cnf(element_2,axiom,
group_element(e_2) ).
cnf(product_left_cancellation,axiom,
( ~ product(X3,X1,X2)
| ~ product(X0,X1,X2)
| equalish(X0,X3) ) ).
cnf(u8104,negated_conjecture,
( ~ product(X0,e_2,e_1)
| product(e_1,X0,e_3) ) ).
cnf(e_4_is_not_e_2,axiom,
~ equalish(e_4,e_2) ).
cnf(u8244,negated_conjecture,
( ~ product(e_4,X0,e_5)
| equalish(X0,e_1) ) ).
cnf(u8315,negated_conjecture,
( ~ product(X0,e_4,e_1)
| equalish(X0,e_3) ) ).
cnf(u8491,axiom,
( ~ product(e_4,X0,e_5)
| ~ group_element(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)
| equalish(X0,X1) ) ).
cnf(u7997,negated_conjecture,
( ~ product(X0,e_4,e_3)
| product(e_3,X0,e_2) ) ).
cnf(u3669,negated_conjecture,
equalish(e_2,e_2) ).
cnf(u8263,negated_conjecture,
( ~ product(X0,e_2,e_5)
| equalish(X0,e_3) ) ).
cnf(u8129,negated_conjecture,
( ~ product(e_5,X0,e_2)
| equalish(X0,e_4) ) ).
cnf(e_5_greater_e_3,axiom,
greater(e_5,e_3) ).
cnf(u8028,negated_conjecture,
( ~ product(e_1,X0,e_4)
| equalish(X0,e_2) ) ).
cnf(u8208,negated_conjecture,
( ~ product(X0,e_2,e_5)
| product(e_5,X0,e_1) ) ).
cnf(u8325,negated_conjecture,
( ~ product(X0,e_1,e_1)
| equalish(X0,e_1) ) ).
cnf(u8228,negated_conjecture,
( ~ product(X0,e_2,e_3)
| product(e_3,X0,e_4) ) ).
cnf(e_3_then_e_4,axiom,
next(e_3,e_4) ).
cnf(u8483,axiom,
( ~ group_element(X1)
| equalish(X0,e_1)
| product(e_1,X1,e_1)
| product(e_1,X1,e_2)
| product(e_1,X1,e_3)
| product(e_1,X1,e_4)
| ~ product(X0,X1,e_5) ) ).
cnf(u8573,negated_conjecture,
( ~ 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)
| equalish(e_4,X0) ) ).
cnf(u8492,axiom,
( ~ product(e_5,X0,e_5)
| ~ group_element(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)
| equalish(X0,X1) ) ).
cnf(u8212,negated_conjecture,
( ~ product(X0,e_5,e_4)
| equalish(X0,e_3) ) ).
cnf(e_3_is_not_e_2,axiom,
~ equalish(e_3,e_2) ).
cnf(u8316,negated_conjecture,
( ~ product(e_3,X0,e_1)
| equalish(X0,e_4) ) ).
cnf(u8207,negated_conjecture,
( ~ product(e_2,X0,e_1)
| equalish(X0,e_5) ) ).
cnf(u8227,negated_conjecture,
( ~ product(e_2,X0,e_4)
| equalish(X0,e_3) ) ).
cnf(e_1_then_e_2,axiom,
next(e_1,e_2) ).
cnf(u8078,negated_conjecture,
( ~ product(e_1,e_5,X0)
| equalish(X0,e_2) ) ).
cnf(e_2_is_not_e_5,axiom,
~ equalish(e_2,e_5) ).
cnf(u47,axiom,
( ~ group_element(X0)
| 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)
| ~ product(X0,X1,e_5) ) ).
cnf(product_right_cancellation,axiom,
( ~ product(X0,X3,X2)
| ~ product(X0,X1,X2)
| equalish(X1,X3) ) ).
cnf(u8485,axiom,
( ~ group_element(X1)
| equalish(X0,e_3)
| product(e_3,X1,e_1)
| product(e_3,X1,e_2)
| product(e_3,X1,e_3)
| product(e_3,X1,e_4)
| ~ product(X0,X1,e_5) ) ).
cnf(u8116,negated_conjecture,
( ~ product(e_1,X0,e_3)
| equalish(X0,e_4) ) ).
cnf(element_3,axiom,
group_element(e_3) ).
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(u8613,axiom,
( ~ product(e_1,e_1,X0)
| ~ greater(X0,e_2) ) ).
cnf(u8242,negated_conjecture,
( ~ product(e_4,e_1,X0)
| equalish(X0,e_5) ) ).
cnf(u8356,negated_conjecture,
( ~ group_element(X0)
| product(X0,e_4,e_1)
| product(X0,e_4,e_2)
| product(X0,e_4,e_3)
| product(X0,e_4,e_4)
| equalish(X0,e_2) ) ).
cnf(u8103,negated_conjecture,
( ~ product(e_2,X0,e_3)
| equalish(X0,e_1) ) ).
cnf(u8262,negated_conjecture,
( ~ product(e_3,e_2,X0)
| equalish(X0,e_5) ) ).
cnf(u8081,negated_conjecture,
( ~ product(X0,e_1,e_5)
| product(e_5,X0,e_2) ) ).
cnf(u8496,axiom,
( ~ group_element(X1)
| equalish(X0,e_5)
| product(e_4,X1,e_1)
| product(e_4,X1,e_2)
| product(e_4,X1,e_3)
| product(e_4,X1,e_4)
| ~ product(e_4,X1,X0) ) ).
cnf(u8247,negated_conjecture,
( ~ product(e_2,e_4,X0)
| equalish(X0,e_5) ) ).
cnf(u8127,negated_conjecture,
( ~ product(e_5,e_4,X0)
| equalish(X0,e_2) ) ).
cnf(u8041,negated_conjecture,
( ~ product(e_3,e_1,X0)
| equalish(X0,e_2) ) ).
cnf(u8519,negated_conjecture,
( ~ 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)
| equalish(e_5,X0) ) ).
cnf(u8006,negated_conjecture,
( ~ product(X0,e_2,e_1)
| equalish(X0,e_4) ) ).
cnf(u742,negated_conjecture,
equalish(e_5,e_5) ).
cnf(u8010,negated_conjecture,
( ~ product(e_4,e_4,X0)
| equalish(X0,e_4) ) ).
cnf(u8044,negated_conjecture,
( ~ product(X0,e_3,e_1)
| product(e_1,X0,e_2) ) ).
cnf(u8275,negated_conjecture,
( ~ group_element(X0)
| product(X0,e_2,e_1)
| product(X0,e_2,e_2)
| product(X0,e_2,e_3)
| product(X0,e_2,e_4)
| product(e_5,X0,e_1) ) ).
cnf(u8134,negated_conjecture,
( ~ product(e_5,X0,e_1)
| equalish(X0,e_3) ) ).
cnf(u8221,negated_conjecture,
( ~ product(X0,e_5,e_1)
| product(e_1,X0,e_4) ) ).
cnf(u8495,axiom,
( ~ group_element(X1)
| equalish(X0,e_5)
| product(e_3,X1,e_1)
| product(e_3,X1,e_2)
| product(e_3,X1,e_3)
| product(e_3,X1,e_4)
| ~ product(e_3,X1,X0) ) ).
cnf(e_5_greater_e_4,axiom,
greater(e_5,e_4) ).
cnf(e_4_greater_e_3,axiom,
greater(e_4,e_3) ).
cnf(u8349,negated_conjecture,
( ~ product(e_1,e_3,X0)
| equalish(X0,e_5) ) ).
cnf(u8581,axiom,
( ~ group_element(X1)
| product(e_3,X0,e_1)
| product(e_3,X0,e_2)
| product(e_3,X0,e_3)
| product(e_3,X0,e_4)
| equalish(X1,X0)
| ~ group_element(X0)
| product(e_3,X1,e_1)
| product(e_3,X1,e_2)
| product(e_3,X1,e_3)
| product(e_3,X1,e_4) ) ).
cnf(u8324,negated_conjecture,
( ~ product(e_1,e_1,X0)
| equalish(X0,e_1) ) ).
cnf(e_2_is_not_e_4,axiom,
~ equalish(e_2,e_4) ).
cnf(e_2_then_e_3,axiom,
next(e_2,e_3) ).
cnf(e_2_is_not_e_1,axiom,
~ equalish(e_2,e_1) ).
cnf(u52,negated_conjecture,
( ~ group_element(X1)
| product(X0,e_5,e_2)
| product(X0,e_5,e_3)
| product(X0,e_5,e_4)
| ~ group_element(X0)
| product(e_5,X1,e_5)
| product(X1,X0,e_1)
| product(X1,X0,e_2)
| product(X1,X0,e_3)
| product(X1,X0,e_4)
| product(X0,e_5,e_1) ) ).
cnf(e_3_is_not_e_4,axiom,
~ equalish(e_3,e_4) ).
cnf(u8225,negated_conjecture,
( ~ product(e_2,e_3,X0)
| equalish(X0,e_4) ) ).
cnf(product_total_function2,axiom,
( ~ product(X0,X1,X3)
| ~ product(X0,X1,X2)
| equalish(X2,X3) ) ).
cnf(u8079,negated_conjecture,
( ~ product(X0,e_5,e_2)
| equalish(X0,e_1) ) ).
cnf(u8585,negated_conjecture,
( ~ 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)
| equalish(e_3,X0) ) ).
cnf(e_5_is_not_e_4,axiom,
~ equalish(e_5,e_4) ).
cnf(u8117,negated_conjecture,
( ~ product(X0,e_1,e_4)
| product(e_4,X0,e_3) ) ).
cnf(u8484,axiom,
( ~ group_element(X1)
| equalish(X0,e_2)
| product(e_2,X1,e_1)
| product(e_2,X1,e_2)
| product(e_2,X1,e_3)
| product(e_2,X1,e_4)
| ~ product(X0,X1,e_5) ) ).
cnf(u8121,negated_conjecture,
( ~ product(e_2,X0,e_2)
| equalish(X0,e_2) ) ).
cnf(u8013,negated_conjecture,
( ~ product(X0,e_4,e_4)
| product(e_4,X0,e_4) ) ).
cnf(u7996,negated_conjecture,
( ~ product(e_4,X0,e_2)
| equalish(X0,e_3) ) ).
cnf(u8130,negated_conjecture,
( ~ product(X0,e_5,e_4)
| product(e_4,X0,e_2) ) ).
cnf(u8026,negated_conjecture,
( ~ product(e_1,e_2,X0)
| equalish(X0,e_4) ) ).
cnf(u8220,negated_conjecture,
( ~ product(e_5,X0,e_4)
| equalish(X0,e_1) ) ).
cnf(u8128,negated_conjecture,
( ~ product(X0,e_4,e_2)
| equalish(X0,e_5) ) ).
cnf(u8205,negated_conjecture,
( ~ product(e_2,e_5,X0)
| equalish(X0,e_1) ) ).
cnf(e_5_greater_e_2,axiom,
greater(e_5,e_2) ).
cnf(u8578,negated_conjecture,
( ~ group_element(X0)
| equalish(X0,e_3)
| 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(u8084,negated_conjecture,
( ~ product(e_5,e_2,X0)
| equalish(X0,e_3) ) ).
cnf(e_3_greater_e_2,axiom,
greater(e_3,e_2) ).
cnf(no_redundancy,axiom,
( ~ next(X0,X2)
| ~ product(X0,e_1,X1)
| ~ greater(X1,X2) ) ).
cnf(e_4_is_not_e_5,axiom,
~ equalish(e_4,e_5) ).
cnf(u8314,negated_conjecture,
( ~ product(e_3,e_4,X0)
| equalish(X0,e_1) ) ).
cnf(u7169,negated_conjecture,
equalish(e_4,e_4) ).
cnf(u8233,negated_conjecture,
( ~ product(X0,e_4,e_5)
| product(e_5,X0,e_3) ) ).
cnf(u8488,axiom,
( ~ product(e_1,X0,e_5)
| ~ group_element(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)
| equalish(X0,X1) ) ).
cnf(e_2_is_not_e_3,axiom,
~ equalish(e_2,e_3) ).
cnf(u49,axiom,
( ~ group_element(X0)
| 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)
| ~ product(X0,X1,X2) ) ).
cnf(u8616,axiom,
( ~ greater(X0,e_5)
| ~ product(e_4,e_1,X0) ) ).
cnf(e_1_is_not_e_5,axiom,
~ equalish(e_1,e_5) ).
cnf(u8226,negated_conjecture,
( ~ product(X0,e_3,e_4)
| equalish(X0,e_2) ) ).
cnf(u8213,negated_conjecture,
( ~ product(e_3,X0,e_4)
| equalish(X0,e_5) ) ).
cnf(u8248,negated_conjecture,
( ~ product(X0,e_4,e_5)
| equalish(X0,e_2) ) ).
cnf(u8005,negated_conjecture,
( ~ product(e_4,e_2,X0)
| equalish(X0,e_1) ) ).
cnf(u8119,negated_conjecture,
( ~ product(e_2,e_2,X0)
| equalish(X0,e_2) ) ).
cnf(u8352,negated_conjecture,
( ~ product(X0,e_1,e_3)
| product(e_3,X0,e_5) ) ).
cnf(u8133,negated_conjecture,
( ~ product(X0,e_3,e_1)
| equalish(X0,e_5) ) ).
cnf(u8102,negated_conjecture,
( ~ product(X0,e_1,e_3)
| equalish(X0,e_2) ) ).
cnf(u8120,negated_conjecture,
( ~ product(X0,e_2,e_2)
| equalish(X0,e_2) ) ).
cnf(u8360,negated_conjecture,
( ~ group_element(X0)
| product(X0,e_2,e_1)
| product(X0,e_2,e_2)
| product(X0,e_2,e_3)
| product(X0,e_2,e_4)
| equalish(X0,e_3) ) ).
cnf(u8012,negated_conjecture,
( ~ product(e_4,X0,e_4)
| equalish(X0,e_4) ) ).
cnf(u8527,negated_conjecture,
( ~ group_element(X0)
| equalish(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(u8206,negated_conjecture,
( ~ product(X0,e_5,e_1)
| equalish(X0,e_2) ) ).
cnf(u8395,negated_conjecture,
( ~ group_element(X0)
| product(X0,e_1,e_1)
| product(X0,e_1,e_2)
| product(X0,e_1,e_3)
| product(X0,e_1,e_4)
| equalish(X0,e_4) ) ).
cnf(u735,negated_conjecture,
equalish(e_3,e_3) ).
cnf(u8062,negated_conjecture,
( ~ product(e_5,e_5,X0)
| equalish(X0,e_5) ) ).
cnf(u8168,negated_conjecture,
( ~ group_element(X0)
| product(X0,e_1,e_1)
| product(X0,e_1,e_2)
| product(X0,e_1,e_3)
| product(X0,e_1,e_4)
| product(e_5,X0,e_2) ) ).
cnf(u8287,negated_conjecture,
( ~ product(e_3,X0,e_3)
| equalish(X0,e_3) ) ).
cnf(element_5,axiom,
group_element(e_5) ).
cnf(e_4_greater_e_2,axiom,
greater(e_4,e_2) ).
cnf(u8175,negated_conjecture,
( ~ group_element(X0)
| product(X0,e_5,e_1)
| product(X0,e_5,e_2)
| product(X0,e_5,e_3)
| product(X0,e_5,e_4)
| equalish(X0,e_5) ) ).
cnf(e_4_is_not_e_1,axiom,
~ equalish(e_4,e_1) ).
cnf(u8065,negated_conjecture,
( ~ product(X0,e_5,e_5)
| product(e_5,X0,e_5) ) ).
cnf(e_5_greater_e_1,axiom,
greater(e_5,e_1) ).
cnf(u8085,negated_conjecture,
( ~ product(X0,e_2,e_3)
| equalish(X0,e_5) ) ).
cnf(e_5_is_not_e_3,axiom,
~ equalish(e_5,e_3) ).
cnf(u8489,axiom,
( ~ product(e_2,X0,e_5)
| ~ group_element(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)
| equalish(X0,X1) ) ).
cnf(u8327,negated_conjecture,
( ~ product(X0,e_1,e_1)
| product(e_1,X0,e_1) ) ).
cnf(u8232,negated_conjecture,
( ~ product(e_4,X0,e_3)
| equalish(X0,e_5) ) ).
cnf(u8582,negated_conjecture,
( ~ 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)
| equalish(e_1,X0) ) ).
cnf(e_5_is_not_e_1,axiom,
~ equalish(e_5,e_1) ).
cnf(u8617,negated_conjecture,
~ greater(e_1,e_2) ).
cnf(u8115,negated_conjecture,
( ~ product(X0,e_4,e_3)
| equalish(X0,e_1) ) ).
cnf(u8494,axiom,
( ~ group_element(X1)
| equalish(X0,e_5)
| product(e_2,X1,e_1)
| product(e_2,X1,e_2)
| product(e_2,X1,e_3)
| product(e_2,X1,e_4)
| ~ product(e_2,X1,X0) ) ).
cnf(u48,axiom,
( ~ group_element(X2)
| 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)
| ~ product(X0,X1,e_5) ) ).
cnf(u8214,negated_conjecture,
( ~ product(X0,e_3,e_5)
| product(e_5,X0,e_4) ) ).
cnf(u8292,negated_conjecture,
( ~ group_element(X0)
| product(X0,e_4,e_1)
| product(X0,e_4,e_2)
| product(X0,e_4,e_3)
| product(X0,e_4,e_4)
| product(e_5,X0,e_3) ) ).
cnf(u8027,negated_conjecture,
( ~ product(X0,e_2,e_4)
| equalish(X0,e_1) ) ).
cnf(u8622,axiom,
~ product(e_3,e_1,e_5) ).
cnf(u7994,negated_conjecture,
( ~ product(e_4,e_3,X0)
| equalish(X0,e_2) ) ).
cnf(u8482,negated_conjecture,
( ~ group_element(X0)
| equalish(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(u8587,axiom,
( ~ group_element(X1)
| product(e_1,X0,e_1)
| product(e_1,X0,e_2)
| product(e_1,X0,e_3)
| product(e_1,X0,e_4)
| equalish(X1,X0)
| ~ group_element(X0)
| 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(u8122,negated_conjecture,
( ~ product(X0,e_2,e_2)
| product(e_2,X0,e_2) ) ).
cnf(u8614,axiom,
( ~ product(e_2,e_1,X0)
| ~ greater(X0,e_3) ) ).
cnf(u8285,negated_conjecture,
( ~ product(e_3,e_3,X0)
| equalish(X0,e_3) ) ).
cnf(u8350,negated_conjecture,
( ~ product(X0,e_3,e_5)
| equalish(X0,e_1) ) ).
cnf(u8265,negated_conjecture,
( ~ product(X0,e_3,e_2)
| product(e_2,X0,e_5) ) ).
cnf(e_4_then_e_5,axiom,
next(e_4,e_5) ).
cnf(u8043,negated_conjecture,
( ~ product(e_3,X0,e_2)
| equalish(X0,e_1) ) ).
cnf(u8063,negated_conjecture,
( ~ product(X0,e_5,e_5)
| equalish(X0,e_5) ) ).
cnf(u8497,axiom,
( ~ group_element(X1)
| equalish(X0,e_5)
| product(e_5,X1,e_1)
| product(e_5,X1,e_2)
| product(e_5,X1,e_3)
| product(e_5,X1,e_4)
| ~ product(e_5,X1,X0) ) ).
cnf(u8218,negated_conjecture,
( ~ product(e_5,e_1,X0)
| equalish(X0,e_4) ) ).
cnf(e_1_is_not_e_4,axiom,
~ equalish(e_1,e_4) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP129-2.005 : TPTP v9.3.1. Released v1.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.37 % Computer : n002.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Sun Sep 27 09:30:37 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.40 Running first-order theorem proving
% 0.09/0.40 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
% 8.78/2.08 % (3282513)Input is clausal, will run a generic CNF schedule.
% 8.78/2.08 % (3282524)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=196153433:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 8.78/2.08 % (3282520)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1031210181:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 8.78/2.08 % (3282521)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=487525488:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 8.78/2.08 % (3282519)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=2107588263:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 8.78/2.08 % (3282522)lrs+10_1_sil=8000:sp=occurrence:random_seed=2471720503:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 8.78/2.08 % (3282525)dis-21_1_sil=8000:lcm=predicate:random_seed=4243049430:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 8.78/2.08 % (3282523)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1401751240:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 8.78/2.08 % (3282524)Instruction limit reached!
% 8.78/2.08 % (3282524)------------------------------
% 8.78/2.08 % (3282524)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.78/2.08 % (3282524)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.78/2.08 % (3282524)CaDiCaL version: 2.1.3
% 8.78/2.08 % (3282524)Termination reason: Instruction limit
% 8.78/2.08 % (3282524)Termination phase: Saturation
% 8.78/2.08 % (3282524)Time elapsed: 0.059 s
% 8.78/2.08 % (3282524)Peak memory usage: 89 MB
% 8.78/2.08 % (3282524)Instructions burned: 182 (million)
% 8.78/2.08 % (3282522)Instruction limit reached!
% 8.78/2.08 % (3282522)------------------------------
% 8.78/2.08 % (3282522)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.78/2.08 % (3282522)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.78/2.08 % (3282522)CaDiCaL version: 2.1.3
% 8.78/2.08 % (3282522)Termination reason: Instruction limit
% 8.78/2.08 % (3282522)Termination phase: Saturation
% 8.78/2.08 % (3282522)Time elapsed: 0.056 s
% 8.78/2.08 % (3282522)Peak memory usage: 88 MB
% 8.78/2.08 % (3282522)Instructions burned: 109 (million)
% 8.78/2.08 % (3282523)Instruction limit reached!
% 8.78/2.08 % (3282523)------------------------------
% 8.78/2.08 % (3282523)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.78/2.08 % (3282523)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.78/2.08 % (3282523)CaDiCaL version: 2.1.3
% 8.78/2.08 % (3282523)Termination reason: Instruction limit
% 8.78/2.08 % (3282523)Termination phase: Saturation
% 8.78/2.08 % (3282523)Time elapsed: 0.061 s
% 8.78/2.08 % (3282523)Peak memory usage: 88 MB
% 8.78/2.08 % (3282523)Instructions burned: 115 (million)
% 8.78/2.08 % (3282525)Instruction limit reached!
% 8.78/2.08 % (3282525)------------------------------
% 8.78/2.08 % (3282525)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.78/2.08 % (3282525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.78/2.08 % (3282525)CaDiCaL version: 2.1.3
% 8.78/2.08 % (3282525)Termination reason: Instruction limit
% 8.78/2.08 % (3282525)Termination phase: Saturation
% 8.78/2.08 % (3282525)Time elapsed: 0.069 s
% 8.78/2.08 % (3282525)Peak memory usage: 88 MB
% 8.78/2.08 % (3282525)Instructions burned: 118 (million)
% 8.78/2.08 % (3282533)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=218875304:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 8.78/2.08 % (3282533)Instruction limit reached!
% 8.78/2.08 % (3282533)------------------------------
% 8.78/2.08 % (3282533)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.78/2.08 % (3282533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.78/2.08 % (3282533)CaDiCaL version: 2.1.3
% 8.78/2.08 % (3282533)Termination reason: Instruction limit
% 8.78/2.08 % (3282533)Termination phase: Saturation
% 8.78/2.08 % (3282533)Time elapsed: 0.045 s
% 8.78/2.08 % (3282533)Peak memory usage: 89 MB
% 8.78/2.08 % (3282533)Instructions burned: 143 (million)
% 8.78/2.08 % (3282535)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3746104313:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 13.01/2.85 % (3282536)lrs+10_64_to=lpo:sil=8000:random_seed=4023874898:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 13.01/2.85 % (3282534)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2064432205: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)
% 13.01/2.85 % (3282534)Refutation not found, incomplete strategy
% 13.01/2.85 % (3282534)------------------------------
% 13.01/2.85 % (3282534)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.01/2.85 % (3282534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.01/2.85 % (3282534)CaDiCaL version: 2.1.3
% 13.01/2.85 % (3282534)Termination reason: Refutation not found, incomplete strategy
% 13.01/2.85 % (3282534)Time elapsed: 0.001 s
% 13.01/2.85 % (3282534)Peak memory usage: 87 MB
% 13.01/2.85 % (3282534)Instructions burned: 1 (million)
% 13.01/2.85 % (3282538)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3050414463:avsq=on:i=194:fgj=on:bd=preordered_2997 on theBenchmark for (2997ds/194Mi)
% 13.01/2.85 % (3282538)Instruction limit reached!
% 13.01/2.85 % (3282538)------------------------------
% 13.01/2.85 % (3282538)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.01/2.85 % (3282538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.01/2.85 % (3282538)CaDiCaL version: 2.1.3
% 13.01/2.85 % (3282538)Termination reason: Instruction limit
% 13.01/2.85 % (3282538)Termination phase: Saturation
% 13.01/2.85 % (3282538)Time elapsed: 0.040 s
% 13.01/2.85 % (3282538)Peak memory usage: 87 MB
% 13.01/2.85 % (3282538)Instructions burned: 197 (million)
% 13.01/2.85 % (3282536)Instruction limit reached!
% 13.01/2.85 % (3282536)------------------------------
% 13.01/2.85 % (3282536)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.01/2.85 % (3282536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.01/2.85 % (3282536)CaDiCaL version: 2.1.3
% 13.01/2.85 % (3282536)Termination reason: Instruction limit
% 13.01/2.85 % (3282536)Termination phase: Saturation
% 13.01/2.85 % (3282536)Time elapsed: 0.076 s
% 13.01/2.85 % (3282536)Peak memory usage: 88 MB
% 13.01/2.85 % (3282536)Instructions burned: 126 (million)
% 13.01/2.85 % (3282535)Instruction limit reached!
% 13.01/2.85 % (3282535)------------------------------
% 13.01/2.85 % (3282535)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.01/2.85 % (3282535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.01/2.85 % (3282535)CaDiCaL version: 2.1.3
% 13.01/2.85 % (3282535)Termination reason: Instruction limit
% 13.01/2.85 % (3282535)Termination phase: Saturation
% 13.01/2.85 % (3282535)Time elapsed: 0.120 s
% 13.01/2.85 % (3282535)Peak memory usage: 89 MB
% 13.01/2.85 % (3282535)Instructions burned: 219 (million)
% 13.01/2.85 % (3282543)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=859989145:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 13.01/2.85 % (3282543)Instruction limit reached!
% 13.01/2.85 % (3282543)------------------------------
% 13.01/2.85 % (3282543)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.01/2.85 % (3282543)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.01/2.85 % (3282543)CaDiCaL version: 2.1.3
% 13.01/2.85 % (3282543)Termination reason: Instruction limit
% 13.01/2.85 % (3282543)Termination phase: Saturation
% 13.01/2.85 % (3282543)Time elapsed: 0.044 s
% 13.01/2.85 % (3282543)Peak memory usage: 89 MB
% 13.01/2.85 % (3282543)Instructions burned: 159 (million)
% 13.01/2.85 % (3282544)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=2244843945:i=3394:sd=4:ss=included:sgt=64_2995 on theBenchmark for (2995ds/3394Mi)
% 13.01/2.85 % (3282534)------------------------------
% 13.01/2.85 % (3282534)------------------------------
% 13.01/2.85 % (3282545)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=1227106170:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2995 on theBenchmark for (2995ds/106Mi)
% 13.01/2.85 % (3282545)Refutation not found, incomplete strategy
% 13.01/2.85 % (3282545)------------------------------
% 13.01/2.85 % (3282545)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.01/2.85 % (3282545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.50/3.70 % (3282545)CaDiCaL version: 2.1.3
% 20.50/3.70 % (3282545)Termination reason: Refutation not found, incomplete strategy
% 20.50/3.70 % (3282545)Time elapsed: 0.002 s
% 20.50/3.70 % (3282545)Peak memory usage: 87 MB
% 20.50/3.70 % (3282545)Instructions burned: 2 (million)
% 20.50/3.70 % (3282548)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=3968601344:i=107_2994 on theBenchmark for (2994ds/107Mi)
% 20.50/3.70 % (3282548)Instruction limit reached!
% 20.50/3.70 % (3282548)------------------------------
% 20.50/3.70 % (3282548)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.50/3.70 % (3282548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.50/3.70 % (3282548)CaDiCaL version: 2.1.3
% 20.50/3.70 % (3282548)Termination reason: Instruction limit
% 20.50/3.70 % (3282548)Termination phase: Saturation
% 20.50/3.70 % (3282548)Time elapsed: 0.037 s
% 20.50/3.70 % (3282548)Peak memory usage: 88 MB
% 20.50/3.70 % (3282548)Instructions burned: 109 (million)
% 20.50/3.70 % (3282550)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=1222216566:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2993 on theBenchmark for (2993ds/242Mi)
% 20.50/3.70 % (3282520)Refutation not found, incomplete strategy
% 20.50/3.70 % (3282520)------------------------------
% 20.50/3.70 % (3282520)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.50/3.70 % (3282520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.50/3.70 % (3282520)CaDiCaL version: 2.1.3
% 20.50/3.70 % (3282520)Termination reason: Refutation not found, incomplete strategy
% 20.50/3.70 % (3282520)Time elapsed: 0.610 s
% 20.50/3.70 % (3282520)Peak memory usage: 126 MB
% 20.50/3.70 % (3282520)Instructions burned: 905 (million)
% 20.50/3.70 % (3282552)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3190520651:cond=fast:i=5208:av=off_2993 on theBenchmark for (2993ds/5208Mi)
% 20.50/3.70 % (3282545)------------------------------
% 20.50/3.70 % (3282545)------------------------------
% 20.50/3.70 % (3282550)Instruction limit reached!
% 20.50/3.70 % (3282550)------------------------------
% 20.50/3.70 % (3282550)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.50/3.70 % (3282550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.50/3.70 % (3282550)CaDiCaL version: 2.1.3
% 20.50/3.70 % (3282550)Termination reason: Instruction limit
% 20.50/3.70 % (3282550)Termination phase: Saturation
% 20.50/3.70 % (3282550)Time elapsed: 0.129 s
% 20.50/3.70 % (3282550)Peak memory usage: 89 MB
% 20.50/3.70 % (3282550)Instructions burned: 242 (million)
% 20.50/3.70 % (3282555)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=1746426940:i=134:sd=2:doe=on:ss=axioms:sgt=14_2991 on theBenchmark for (2991ds/134Mi)
% 20.50/3.70 % (3282520)------------------------------
% 20.50/3.70 % (3282520)------------------------------
% 20.50/3.70 % (3282556)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=4167637394:i=499:bd=all_2991 on theBenchmark for (2991ds/499Mi)
% 20.50/3.70 % (3282555)Instruction limit reached!
% 20.50/3.70 % (3282555)------------------------------
% 20.50/3.70 % (3282555)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.50/3.70 % (3282555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.50/3.70 % (3282555)CaDiCaL version: 2.1.3
% 20.50/3.70 % (3282555)Termination reason: Instruction limit
% 20.50/3.70 % (3282555)Termination phase: Saturation
% 20.50/3.70 % (3282555)Time elapsed: 0.053 s
% 20.50/3.70 % (3282555)Peak memory usage: 87 MB
% 20.50/3.70 % (3282555)Instructions burned: 134 (million)
% 20.50/3.70 % (3282559)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=3326769633:i=191:fgj=on:bd=all_2989 on theBenchmark for (2989ds/191Mi)
% 20.50/3.70 % (3282560)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3153517650:i=264:kws=precedence:fsr=off_2989 on theBenchmark for (2989ds/264Mi)
% 20.50/3.70 % (3282559)Instruction limit reached!
% 20.50/3.70 % (3282559)------------------------------
% 20.50/3.70 % (3282559)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.50/3.70 % (3282559)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.50/3.70 % (3282559)CaDiCaL version: 2.1.3
% 20.50/3.70 % (3282559)Termination reason: Instruction limit
% 30.77/5.17 % (3282559)Termination phase: Saturation
% 30.77/5.17 % (3282559)Time elapsed: 0.117 s
% 30.77/5.17 % (3282559)Peak memory usage: 88 MB
% 30.77/5.17 % (3282559)Instructions burned: 193 (million)
% 30.77/5.17 % (3282556)Instruction limit reached!
% 30.77/5.17 % (3282556)------------------------------
% 30.77/5.17 % (3282556)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.77/5.17 % (3282556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.77/5.17 % (3282556)CaDiCaL version: 2.1.3
% 30.77/5.17 % (3282556)Termination reason: Instruction limit
% 30.77/5.17 % (3282556)Termination phase: Saturation
% 30.77/5.17 % (3282556)Time elapsed: 0.260 s
% 30.77/5.17 % (3282556)Peak memory usage: 90 MB
% 30.77/5.17 % (3282556)Instructions burned: 500 (million)
% 30.77/5.17 % (3282560)Instruction limit reached!
% 30.77/5.17 % (3282560)------------------------------
% 30.77/5.17 % (3282560)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.77/5.17 % (3282560)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.77/5.17 % (3282560)CaDiCaL version: 2.1.3
% 30.77/5.17 % (3282560)Termination reason: Instruction limit
% 30.77/5.17 % (3282560)Termination phase: Saturation
% 30.77/5.17 % (3282560)Time elapsed: 0.153 s
% 30.77/5.17 % (3282560)Peak memory usage: 89 MB
% 30.77/5.17 % (3282560)Instructions burned: 265 (million)
% 30.77/5.17 % (3282563)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=2321353535:cond=on:i=156:bs=on:gtg=exists_all:er=known_2987 on theBenchmark for (2987ds/156Mi)
% 30.77/5.17 % (3282564)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=3646112247:i=3256:kws=precedence:bd=preordered:av=off_2987 on theBenchmark for (2987ds/3256Mi)
% 30.77/5.17 % (3282565)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=3250530298:i=537:av=off:ss=included_2986 on theBenchmark for (2986ds/537Mi)
% 30.77/5.17 % (3282563)Instruction limit reached!
% 30.77/5.17 % (3282563)------------------------------
% 30.77/5.17 % (3282563)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.77/5.17 % (3282563)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.77/5.17 % (3282563)CaDiCaL version: 2.1.3
% 30.77/5.17 % (3282563)Termination reason: Instruction limit
% 30.77/5.17 % (3282563)Termination phase: Saturation
% 30.77/5.17 % (3282563)Time elapsed: 0.087 s
% 30.77/5.17 % (3282563)Peak memory usage: 88 MB
% 30.77/5.17 % (3282563)Instructions burned: 156 (million)
% 30.77/5.17 % (3282569)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=3076156492:i=180:bd=preordered:av=off_2985 on theBenchmark for (2985ds/180Mi)
% 30.77/5.17 % (3282565)Instruction limit reached!
% 30.77/5.17 % (3282565)------------------------------
% 30.77/5.17 % (3282565)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.77/5.17 % (3282565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.77/5.17 % (3282565)CaDiCaL version: 2.1.3
% 30.77/5.17 % (3282565)Termination reason: Instruction limit
% 30.77/5.17 % (3282565)Termination phase: Saturation
% 30.77/5.17 % (3282565)Time elapsed: 0.196 s
% 30.77/5.17 % (3282565)Peak memory usage: 87 MB
% 30.77/5.17 % (3282565)Instructions burned: 539 (million)
% 30.77/5.17 % (3282569)Instruction limit reached!
% 30.77/5.17 % (3282569)------------------------------
% 30.77/5.17 % (3282569)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.77/5.17 % (3282569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.77/5.17 % (3282569)CaDiCaL version: 2.1.3
% 30.77/5.17 % (3282569)Termination reason: Instruction limit
% 30.77/5.17 % (3282569)Termination phase: Saturation
% 30.77/5.17 % (3282569)Time elapsed: 0.091 s
% 30.77/5.17 % (3282569)Peak memory usage: 87 MB
% 30.77/5.17 % (3282569)Instructions burned: 180 (million)
% 30.77/5.17 % (3282571)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=1033764702:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2983 on theBenchmark for (2983ds/10307Mi)
% 30.77/5.17 % (3282572)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=4153924798:i=412:gtgl=4:gtg=exists_all_2983 on theBenchmark for (2983ds/412Mi)
% 30.77/5.17 % (3282544)Instruction limit reached!
% 30.77/5.17 % (3282544)------------------------------
% 30.77/5.17 % (3282544)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.83/6.78 % (3282544)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.83/6.78 % (3282544)CaDiCaL version: 2.1.3
% 41.83/6.78 % (3282544)Termination reason: Instruction limit
% 41.83/6.78 % (3282544)Termination phase: Saturation
% 41.83/6.78 % (3282544)Time elapsed: 1.456 s
% 41.83/6.78 % (3282544)Peak memory usage: 140 MB
% 41.83/6.78 % (3282544)Instructions burned: 3398 (million)
% 41.83/6.78 % (3282572)Instruction limit reached!
% 41.83/6.78 % (3282572)------------------------------
% 41.83/6.78 % (3282572)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.83/6.78 % (3282572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.83/6.78 % (3282572)CaDiCaL version: 2.1.3
% 41.83/6.78 % (3282572)Termination reason: Instruction limit
% 41.83/6.78 % (3282572)Termination phase: Saturation
% 41.83/6.78 % (3282572)Time elapsed: 0.207 s
% 41.83/6.78 % (3282572)Peak memory usage: 90 MB
% 41.83/6.78 % (3282572)Instructions burned: 412 (million)
% 41.83/6.78 % (3282575)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=3900700721:s2pl=no:i=8478:s2at=4:nm=6_2979 on theBenchmark for (2979ds/8478Mi)
% 41.83/6.78 % (3282576)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=22390591:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2979 on theBenchmark for (2979ds/303Mi)
% 41.83/6.78 % (3282576)Instruction limit reached!
% 41.83/6.78 % (3282576)------------------------------
% 41.83/6.78 % (3282576)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.83/6.78 % (3282576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.83/6.78 % (3282576)CaDiCaL version: 2.1.3
% 41.83/6.78 % (3282576)Termination reason: Instruction limit
% 41.83/6.78 % (3282576)Termination phase: Saturation
% 41.83/6.78 % (3282576)Time elapsed: 0.183 s
% 41.83/6.78 % (3282576)Peak memory usage: 90 MB
% 41.83/6.78 % (3282576)Instructions burned: 304 (million)
% 41.83/6.78 % (3282575)Refutation not found, incomplete strategy
% 41.83/6.78 % (3282575)------------------------------
% 41.83/6.78 % (3282575)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.83/6.78 % (3282575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.83/6.78 % (3282575)CaDiCaL version: 2.1.3
% 41.83/6.78 % (3282575)Termination reason: Refutation not found, incomplete strategy
% 41.83/6.78 % (3282575)Time elapsed: 0.361 s
% 41.83/6.78 % (3282575)Peak memory usage: 128 MB
% 41.83/6.78 % (3282575)Instructions burned: 907 (million)
% 41.83/6.78 % (3282579)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=1826030385:st=4:i=720:sd=3:fsr=off:ss=axioms_2976 on theBenchmark for (2976ds/720Mi)
% 41.83/6.78 % (3282579)Refutation not found, incomplete strategy
% 41.83/6.78 % (3282579)------------------------------
% 41.83/6.78 % (3282579)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.83/6.78 % (3282579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.83/6.78 % (3282579)CaDiCaL version: 2.1.3
% 41.83/6.78 % (3282579)Termination reason: Refutation not found, incomplete strategy
% 41.83/6.78 % (3282579)Time elapsed: 0.001 s
% 41.83/6.78 % (3282579)Peak memory usage: 87 MB
% 41.83/6.78 % (3282579)Instructions burned: 1 (million)
% 41.83/6.78 % (3282575)------------------------------
% 41.83/6.78 % (3282575)------------------------------
% 41.83/6.78 % (3282581)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=3643426037:i=598:bs=on:bd=preordered:av=off:ss=axioms_2973 on theBenchmark for (2973ds/598Mi)
% 41.83/6.78 % (3282579)------------------------------
% 41.83/6.78 % (3282579)------------------------------
% 41.83/6.78 % (3282581)Instruction limit reached!
% 41.83/6.78 % (3282581)------------------------------
% 41.83/6.78 % (3282581)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 41.83/6.78 % (3282581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.83/6.78 % (3282581)CaDiCaL version: 2.1.3
% 41.83/6.78 % (3282581)Termination reason: Instruction limit
% 41.83/6.78 % (3282581)Termination phase: Saturation
% 41.83/6.78 % (3282581)Time elapsed: 0.149 s
% 41.83/6.78 % (3282581)Peak memory usage: 88 MB
% 41.83/6.78 % (3282581)Instructions burned: 599 (million)
% 41.83/6.78 % (3282583)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=902139541:i=2989:sd=3:ss=axioms:sgt=60_2972 on theBenchmark for (2972ds/2989Mi)
% 44.97/7.43 % (3282552)Instruction limit reached!
% 44.97/7.43 % (3282552)------------------------------
% 44.97/7.43 % (3282552)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.97/7.43 % (3282552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.97/7.43 % (3282552)CaDiCaL version: 2.1.3
% 44.97/7.43 % (3282552)Termination reason: Instruction limit
% 44.97/7.43 % (3282552)Termination phase: Saturation
% 44.97/7.43 % (3282552)Time elapsed: 2.144 s
% 44.97/7.43 % (3282552)Peak memory usage: 131 MB
% 44.97/7.43 % (3282552)Instructions burned: 5209 (million)
% 44.97/7.43 % (3282584)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=2038730681:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2971 on theBenchmark for (2971ds/1997Mi)
% 44.97/7.43 % (3282586)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=2423012705:i=2088:bd=preordered:av=off_2970 on theBenchmark for (2970ds/2088Mi)
% 44.97/7.43 % (3282564)Instruction limit reached!
% 44.97/7.43 % (3282564)------------------------------
% 44.97/7.43 % (3282564)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.97/7.43 % (3282564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.97/7.43 % (3282564)CaDiCaL version: 2.1.3
% 44.97/7.43 % (3282564)Termination reason: Instruction limit
% 44.97/7.43 % (3282564)Termination phase: Saturation
% 44.97/7.43 % (3282564)Time elapsed: 1.886 s
% 44.97/7.43 % (3282564)Peak memory usage: 133 MB
% 44.97/7.43 % (3282564)Instructions burned: 3257 (million)
% 44.97/7.43 % (3282589)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=3350195987:i=1098:nicw=on_2967 on theBenchmark for (2967ds/1098Mi)
% 44.97/7.43 % (3282584)Instruction limit reached!
% 44.97/7.43 % (3282584)------------------------------
% 44.97/7.43 % (3282584)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.97/7.43 % (3282584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.97/7.43 % (3282584)CaDiCaL version: 2.1.3
% 44.97/7.43 % (3282584)Termination reason: Instruction limit
% 44.97/7.43 % (3282584)Termination phase: Saturation
% 44.97/7.43 % (3282584)Time elapsed: 0.789 s
% 44.97/7.43 % (3282584)Peak memory usage: 133 MB
% 44.97/7.43 % (3282584)Instructions burned: 1998 (million)
% 44.97/7.43 % (3282591)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=3080464220:i=433:bd=preordered_2962 on theBenchmark for (2962ds/433Mi)
% 44.97/7.43 % (3282591)Refutation not found, incomplete strategy
% 44.97/7.43 % (3282591)------------------------------
% 44.97/7.43 % (3282591)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.97/7.43 % (3282591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.97/7.43 % (3282591)CaDiCaL version: 2.1.3
% 44.97/7.43 % (3282591)Termination reason: Refutation not found, incomplete strategy
% 44.97/7.43 % (3282591)Time elapsed: 0.084 s
% 44.97/7.43 % (3282591)Peak memory usage: 89 MB
% 44.97/7.43 % (3282591)Instructions burned: 258 (million)
% 44.97/7.43 % (3282589)Instruction limit reached!
% 44.97/7.43 % (3282589)------------------------------
% 44.97/7.43 % (3282589)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.97/7.43 % (3282589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.97/7.43 % (3282589)CaDiCaL version: 2.1.3
% 44.97/7.43 % (3282589)Termination reason: Instruction limit
% 44.97/7.43 % (3282589)Termination phase: Saturation
% 44.97/7.43 % (3282589)Time elapsed: 0.587 s
% 44.97/7.43 % (3282589)Peak memory usage: 91 MB
% 44.97/7.43 % (3282589)Instructions burned: 1099 (million)
% 44.97/7.43 % (3282591)------------------------------
% 44.97/7.43 % (3282591)------------------------------
% 44.97/7.43 % (3282593)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=4187706282:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2960 on theBenchmark for (2960ds/2942Mi)
% 44.97/7.43 % (3282594)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=365420663:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2959 on theBenchmark for (2959ds/6922Mi)
% 44.97/7.43 % (3282586)Instruction limit reached!
% 44.97/7.43 % (3282586)------------------------------
% 44.97/7.43 % (3282586)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.97/7.43 % (3282586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.97/7.43 % (3282586)CaDiCaL version: 2.1.3
% 44.97/7.43 % (3282586)Termination reason: Instruction limit
% 44.97/7.43 % (3282586)Termination phase: Saturation
% 44.97/7.43 % (3282586)Time elapsed: 1.293 s
% 44.97/7.43 % (3282586)Peak memory usage: 132 MB
% 44.97/7.43 % (3282586)Instructions burned: 2089 (million)
% 44.97/7.43 % (3282597)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=552648831:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2956 on theBenchmark for (2956ds/596Mi)
% 44.97/7.43 % (3282597)Refutation not found, incomplete strategy
% 44.97/7.43 % (3282597)------------------------------
% 44.97/7.43 % (3282597)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.97/7.43 % (3282597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.97/7.43 % (3282597)CaDiCaL version: 2.1.3
% 44.97/7.43 % (3282597)Termination reason: Refutation not found, incomplete strategy
% 44.97/7.43 % (3282597)Time elapsed: 0.002 s
% 44.97/7.43 % (3282597)Peak memory usage: 88 MB
% 44.97/7.43 % (3282597)Instructions burned: 2 (million)
% 44.97/7.43 % (3282594)Refutation not found, incomplete strategy
% 44.97/7.43 % (3282594)------------------------------
% 44.97/7.43 % (3282594)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.97/7.43 % (3282594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.97/7.43 % (3282594)CaDiCaL version: 2.1.3
% 44.97/7.43 % (3282594)Termination reason: Refutation not found, incomplete strategy
% 44.97/7.43 % (3282594)Time elapsed: 0.348 s
% 44.97/7.43 % (3282594)Peak memory usage: 127 MB
% 44.97/7.43 % (3282594)Instructions burned: 901 (million)
% 44.97/7.43 % (3282594)------------------------------
% 44.97/7.43 % (3282594)------------------------------
% 44.97/7.43 % (3282597)------------------------------
% 44.97/7.43 % (3282597)------------------------------
% 44.97/7.43 % (3282599)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=1808055852:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2953 on theBenchmark for (2953ds/4123Mi)
% 44.97/7.43 % (3282600)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=4153994839:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2952 on theBenchmark for (2952ds/16411Mi)
% 44.97/7.43 % (3282583)Instruction limit reached!
% 44.97/7.43 % (3282583)------------------------------
% 44.97/7.43 % (3282583)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.97/7.43 % (3282583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.97/7.43 % (3282583)CaDiCaL version: 2.1.3
% 44.97/7.43 % (3282583)Termination reason: Instruction limit
% 44.97/7.43 % (3282583)Termination phase: Saturation
% 44.97/7.43 % (3282583)Time elapsed: 1.985 s
% 44.97/7.43 % (3282583)Peak memory usage: 141 MB
% 44.97/7.43 % (3282583)Instructions burned: 2989 (million)
% 44.97/7.43 % (3282603)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=2737225403:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2951 on theBenchmark for (2951ds/1670Mi)
% 44.97/7.43 % (3282593)Instruction limit reached!
% 44.97/7.43 % (3282593)------------------------------
% 44.97/7.43 % (3282593)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.97/7.43 % (3282593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.97/7.43 % (3282593)CaDiCaL version: 2.1.3
% 44.97/7.43 % (3282593)Termination reason: Instruction limit
% 44.97/7.43 % (3282593)Termination phase: Saturation
% 44.97/7.43 % (3282593)Time elapsed: 1.711 s
% 44.97/7.43 % (3282593)Peak memory usage: 134 MB
% 44.97/7.43 % (3282593)Instructions burned: 2943 (million)
% 44.97/7.43 % (3282599)Instruction limit reached!
% 44.97/7.43 % (3282599)------------------------------
% 44.97/7.43 % (3282599)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.97/7.43 % (3282599)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.97/7.43 % (3282599)CaDiCaL version: 2.1.3
% 44.97/7.43 % (3282599)Termination reason: Instruction limit
% 44.97/7.43 % (3282599)Termination phase: Saturation
% 44.97/7.43 % (3282599)Time elapsed: 1.222 s
% 44.97/7.43 % (3282599)Peak memory usage: 135 MB
% 44.97/7.43 % (3282599)Instructions burned: 4127 (million)
% 44.97/7.43 % (3282605)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=2170537602:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2941 on theBenchmark for (2941ds/1722Mi)
% 44.97/7.43 % (3282603)Instruction limit reached!
% 44.97/7.43 % (3282603)------------------------------
% 44.97/7.43 % (3282603)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.97/7.43 % (3282603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.97/7.43 % (3282603)CaDiCaL version: 2.1.3
% 44.97/7.43 % (3282603)Termination reason: Instruction limit
% 44.97/7.43 % (3282603)Termination phase: Saturation
% 44.97/7.43 % (3282603)Time elapsed: 1.001 s
% 44.97/7.43 % (3282603)Peak memory usage: 134 MB
% 44.97/7.43 % (3282603)Instructions burned: 1670 (million)
% 44.97/7.43 % (3282606)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=3197520208:cts=off:cond=on:i=9530:bs=on:fsd=on_2940 on theBenchmark for (2940ds/9530Mi)
% 44.97/7.43 % (3282608)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=3415825333:st=2:i=4495:sd=10:ss=included_2940 on theBenchmark for (2940ds/4495Mi)
% 44.97/7.43 % (3282600)First to succeed.
% 44.97/7.43 % (3282600)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3282513"
% 44.97/7.43 % SZS status Satisfiable for theBenchmark
% 44.97/7.43 % SZS output start Saturation.
% See solution above
% 47.22/7.62 % SZS output start Definitions and Model Updates.
% 47.22/7.62 % SZS output end Definitions and Model Updates.
% 47.22/7.62 % (3282600)------------------------------
% 47.22/7.62 % (3282600)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 47.22/7.62 % (3282600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 47.22/7.62 % (3282600)CaDiCaL version: 2.1.3
% 47.22/7.62 % (3282600)Termination reason: Satisfiable
% 47.22/7.62 % (3282600)Time elapsed: 1.495 s
% 47.22/7.62 % (3282600)Peak memory usage: 137 MB
% 47.22/7.62 % (3282600)Instructions burned: 2073 (million)
% 47.22/7.62 % (3282600)------------------------------
% 47.22/7.62 % (3282600)------------------------------
% 47.22/7.62 % (3282513)Success in time 6.587 s
% 47.22/7.62 % Vampire exiting
%------------------------------------------------------------------------------