%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP127-1.005 : TPTP v9.3.1. Released v1.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n013.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:46 AM UTC 2026
% Result : Satisfiable 2.95s 1.61s
% Output : Saturation 5.73s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u52,axiom,
~ product(e_5,e_1,e_5) ).
cnf(u56,axiom,
~ product(e_5,e_1,e_4) ).
cnf(u60,axiom,
~ product(e_5,e_1,e_3) ).
cnf(u65,axiom,
product(e_5,e_1,e_2) ).
cnf(u68,axiom,
~ product(e_5,e_1,e_1) ).
cnf(u73,axiom,
~ product(e_4,e_1,e_5) ).
cnf(u77,axiom,
~ product(e_4,e_1,e_4) ).
cnf(u82,axiom,
product(e_4,e_1,e_3) ).
cnf(u85,axiom,
~ product(e_4,e_1,e_2) ).
cnf(u89,axiom,
~ product(e_4,e_1,e_1) ).
cnf(u95,axiom,
product(e_3,e_1,e_5) ).
cnf(u98,axiom,
~ product(e_3,e_1,e_4) ).
cnf(u102,axiom,
~ product(e_3,e_1,e_3) ).
cnf(u106,axiom,
~ product(e_3,e_1,e_2) ).
cnf(u110,axiom,
~ product(e_3,e_1,e_1) ).
cnf(u115,axiom,
~ product(e_2,e_1,e_5) ).
cnf(u120,axiom,
product(e_2,e_1,e_4) ).
cnf(u123,axiom,
~ product(e_2,e_1,e_3) ).
cnf(u127,axiom,
~ product(e_2,e_1,e_2) ).
cnf(u131,axiom,
~ product(e_2,e_1,e_1) ).
cnf(u210,axiom,
~ product(e_5,e_2,e_5) ).
cnf(u214,axiom,
~ product(e_5,e_2,e_4) ).
cnf(u218,axiom,
~ product(e_5,e_2,e_3) ).
cnf(u222,axiom,
~ product(e_5,e_2,e_2) ).
cnf(u227,axiom,
product(e_5,e_2,e_1) ).
cnf(u232,axiom,
product(e_4,e_2,e_5) ).
cnf(u235,axiom,
~ product(e_4,e_2,e_4) ).
cnf(u239,axiom,
~ product(e_4,e_2,e_3) ).
cnf(u243,axiom,
~ product(e_4,e_2,e_2) ).
cnf(u247,axiom,
~ product(e_4,e_2,e_1) ).
cnf(u252,axiom,
~ product(e_3,e_2,e_5) ).
cnf(u257,axiom,
product(e_3,e_2,e_4) ).
cnf(u260,axiom,
~ product(e_3,e_2,e_3) ).
cnf(u264,axiom,
~ product(e_3,e_2,e_2) ).
cnf(u268,axiom,
~ product(e_3,e_2,e_1) ).
cnf(u273,axiom,
~ product(e_1,e_2,e_5) ).
cnf(u277,axiom,
~ product(e_1,e_2,e_4) ).
cnf(u282,axiom,
product(e_1,e_2,e_3) ).
cnf(u285,axiom,
~ product(e_1,e_2,e_2) ).
cnf(u289,axiom,
~ product(e_1,e_2,e_1) ).
cnf(u447,axiom,
~ product(e_5,e_3,e_5) ).
cnf(u452,axiom,
product(e_5,e_3,e_4) ).
cnf(u455,axiom,
~ product(e_5,e_3,e_3) ).
cnf(u459,axiom,
~ product(e_5,e_3,e_2) ).
cnf(u463,axiom,
~ product(e_5,e_3,e_1) ).
cnf(u468,axiom,
~ product(e_4,e_3,e_5) ).
cnf(u472,axiom,
~ product(e_4,e_3,e_4) ).
cnf(u476,axiom,
~ product(e_4,e_3,e_3) ).
cnf(u480,axiom,
~ product(e_4,e_3,e_2) ).
cnf(u485,axiom,
product(e_4,e_3,e_1) ).
cnf(u490,axiom,
product(e_2,e_3,e_5) ).
cnf(u493,axiom,
~ product(e_2,e_3,e_4) ).
cnf(u497,axiom,
~ product(e_2,e_3,e_3) ).
cnf(u501,axiom,
~ product(e_2,e_3,e_2) ).
cnf(u505,axiom,
~ product(e_2,e_3,e_1) ).
cnf(u510,axiom,
~ product(e_1,e_3,e_5) ).
cnf(u514,axiom,
~ product(e_1,e_3,e_4) ).
cnf(u518,axiom,
~ product(e_1,e_3,e_3) ).
cnf(u523,axiom,
product(e_1,e_3,e_2) ).
cnf(u526,axiom,
~ product(e_1,e_3,e_1) ).
cnf(u732,axiom,
~ product(e_5,e_4,e_5) ).
cnf(u736,axiom,
~ product(e_5,e_4,e_4) ).
cnf(u741,axiom,
product(e_5,e_4,e_3) ).
cnf(u744,axiom,
~ product(e_5,e_4,e_2) ).
cnf(u748,axiom,
~ product(e_5,e_4,e_1) ).
cnf(u753,axiom,
~ product(e_3,e_4,e_5) ).
cnf(u757,axiom,
~ product(e_3,e_4,e_4) ).
cnf(u761,axiom,
~ product(e_3,e_4,e_3) ).
cnf(u766,axiom,
product(e_3,e_4,e_2) ).
cnf(u769,axiom,
~ product(e_3,e_4,e_1) ).
cnf(u774,axiom,
~ product(e_2,e_4,e_5) ).
cnf(u778,axiom,
~ product(e_2,e_4,e_4) ).
cnf(u782,axiom,
~ product(e_2,e_4,e_3) ).
cnf(u786,axiom,
~ product(e_2,e_4,e_2) ).
cnf(u791,axiom,
product(e_2,e_4,e_1) ).
cnf(u796,axiom,
product(e_1,e_4,e_5) ).
cnf(u799,axiom,
~ product(e_1,e_4,e_4) ).
cnf(u803,axiom,
~ product(e_1,e_4,e_3) ).
cnf(u807,axiom,
~ product(e_1,e_4,e_2) ).
cnf(u811,axiom,
~ product(e_1,e_4,e_1) ).
cnf(u979,axiom,
~ product(e_4,e_5,e_5) ).
cnf(u987,axiom,
~ product(e_4,e_5,e_3) ).
cnf(u992,axiom,
product(e_4,e_5,e_2) ).
cnf(u995,axiom,
~ product(e_4,e_5,e_1) ).
cnf(u1000,axiom,
~ product(e_3,e_5,e_5) ).
cnf(u1004,axiom,
~ product(e_3,e_5,e_4) ).
cnf(u1008,axiom,
~ product(e_3,e_5,e_3) ).
cnf(u1012,axiom,
~ product(e_3,e_5,e_2) ).
cnf(u1017,axiom,
product(e_3,e_5,e_1) ).
cnf(u1030,axiom,
product(e_2,e_5,e_3) ).
cnf(u1033,axiom,
~ product(e_2,e_5,e_2) ).
cnf(u1042,axiom,
~ product(e_1,e_5,e_5) ).
cnf(u1047,axiom,
product(e_1,e_5,e_4) ).
cnf(u1245,negated_conjecture,
( ~ product(e_1,X0,e_4)
| product(e_3,e_1,X0) ) ).
cnf(u1244,axiom,
( ~ product(e_4,e_1,X0)
| equalish(X0,e_3) ) ).
cnf(element_3,axiom,
group_element(e_3) ).
cnf(u1382,axiom,
( ~ product(e_4,X0,e_2)
| equalish(X0,e_5) ) ).
cnf(e_5_is_not_e_1,axiom,
~ equalish(e_5,e_1) ).
cnf(u942,axiom,
( ~ product(e_4,X0,e_1)
| equalish(X0,e_3) ) ).
cnf(u1237,axiom,
( ~ product(e_1,X0,e_2)
| equalish(X0,e_3) ) ).
cnf(u40,axiom,
( ~ 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(X0,e_1,e_5) ) ).
cnf(e_1_is_not_e_3,axiom,
~ equalish(e_1,e_3) ).
cnf(u904,axiom,
( ~ product(e_3,X0,e_5)
| equalish(X0,e_1) ) ).
cnf(u932,axiom,
( ~ product(e_5,X0,e_4)
| equalish(X0,e_3) ) ).
cnf(e_2_is_not_e_1,axiom,
~ equalish(e_2,e_1) ).
cnf(u941,axiom,
( ~ product(X0,e_3,e_1)
| equalish(X0,e_4) ) ).
cnf(u933,axiom,
( ~ product(e_5,e_3,X0)
| equalish(X0,e_4) ) ).
cnf(u361,negated_conjecture,
( ~ product(e_2,X0,e_5)
| product(e_1,e_2,X0) ) ).
cnf(e_5_is_not_e_4,axiom,
~ equalish(e_5,e_4) ).
cnf(u914,axiom,
( ~ product(e_1,X0,e_3)
| equalish(X0,e_2) ) ).
cnf(u44,axiom,
( ~ 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(X0,e_5,e_5) ) ).
cnf(u1239,negated_conjecture,
( ~ product(e_3,X0,e_1)
| product(e_2,e_3,X0) ) ).
cnf(u1188,negated_conjecture,
( ~ product(e_2,X0,e_4)
| product(e_5,e_2,X0) ) ).
cnf(u1254,axiom,
( ~ product(e_2,X0,e_1)
| equalish(X0,e_4) ) ).
cnf(u915,axiom,
( ~ product(e_1,e_2,X0)
| equalish(X0,e_3) ) ).
cnf(u1383,axiom,
( ~ product(e_4,e_5,X0)
| equalish(X0,e_2) ) ).
cnf(e_3_is_not_e_1,axiom,
~ equalish(e_3,e_1) ).
cnf(u906,negated_conjecture,
( ~ product(e_1,X0,e_3)
| product(e_5,e_1,X0) ) ).
cnf(u1213,axiom,
( ~ product(e_3,X0,e_4)
| equalish(X0,e_2) ) ).
cnf(element_1,axiom,
group_element(e_1) ).
cnf(product_left_cancellation,axiom,
( ~ product(X3,X1,X2)
| ~ product(X0,X1,X2)
| equalish(X0,X3) ) ).
cnf(u1452,axiom,
( ~ product(e_1,e_5,X0)
| equalish(X0,e_4) ) ).
cnf(u32,negated_conjecture,
( ~ product(X0,X1,X0)
| product(X0,X0,X1) ) ).
cnf(u1429,negated_conjecture,
( ~ product(e_5,X0,e_2)
| product(e_3,e_5,X0) ) ).
cnf(u1345,axiom,
( ~ product(e_1,X0,e_5)
| equalish(X0,e_4) ) ).
cnf(u1256,negated_conjecture,
( ~ product(e_4,X0,e_2)
| product(e_1,e_4,X0) ) ).
cnf(u919,axiom,
( ~ product(X0,e_1,e_2)
| equalish(X0,e_5) ) ).
cnf(element_5,axiom,
group_element(e_5) ).
cnf(u1428,axiom,
( ~ product(e_2,e_5,X0)
| equalish(X0,e_3) ) ).
cnf(e_1_is_not_e_4,axiom,
~ equalish(e_1,e_4) ).
cnf(u36,axiom,
( ~ product(X0,X1,X0)
| equalish(X1,X0) ) ).
cnf(qg3,negated_conjecture,
( ~ product(X2,X0,X3)
| ~ product(X0,X1,X2)
| product(X3,X0,X1) ) ).
cnf(u43,axiom,
( ~ 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(X0,e_4,e_5) ) ).
cnf(u34,axiom,
( ~ product(X0,X0,X1)
| equalish(X1,X0) ) ).
cnf(u1180,axiom,
( ~ product(X0,e_1,e_4)
| equalish(X0,e_2) ) ).
cnf(u1300,negated_conjecture,
( ~ product(e_3,X0,e_2)
| product(e_5,e_3,X0) ) ).
cnf(u1287,axiom,
( ~ product(X0,e_4,e_3)
| equalish(X0,e_5) ) ).
cnf(u1450,axiom,
( ~ product(X0,e_5,e_4)
| equalish(X0,e_1) ) ).
cnf(e_2_is_not_e_4,axiom,
~ equalish(e_2,e_4) ).
cnf(u1384,negated_conjecture,
( ~ product(e_5,X0,e_4)
| product(e_2,e_5,X0) ) ).
cnf(u360,axiom,
( ~ product(e_5,e_2,X0)
| equalish(X0,e_1) ) ).
cnf(u921,axiom,
( ~ product(e_5,e_1,X0)
| equalish(X0,e_2) ) ).
cnf(e_4_is_not_e_2,axiom,
~ equalish(e_4,e_2) ).
cnf(u944,negated_conjecture,
( ~ product(e_3,X0,e_4)
| product(e_1,e_3,X0) ) ).
cnf(u38,axiom,
( ~ product(X0,X1,X1)
| equalish(X0,X1) ) ).
cnf(u1305,negated_conjecture,
( ~ product(e_4,X0,e_3)
| product(e_2,e_4,X0) ) ).
cnf(u1181,axiom,
( ~ product(e_2,X0,e_4)
| equalish(X0,e_1) ) ).
cnf(u1420,axiom,
( ~ product(e_3,X0,e_1)
| equalish(X0,e_5) ) ).
cnf(u359,axiom,
( ~ product(e_5,X0,e_1)
| equalish(X0,e_2) ) ).
cnf(e_5_is_not_e_2,axiom,
~ equalish(e_5,e_2) ).
cnf(u920,axiom,
( ~ product(e_5,X0,e_2)
| equalish(X0,e_1) ) ).
cnf(u943,axiom,
( ~ product(e_4,e_3,X0)
| equalish(X0,e_1) ) ).
cnf(u1344,axiom,
( ~ product(X0,e_4,e_5)
| equalish(X0,e_1) ) ).
cnf(product_total_function1,axiom,
( ~ group_element(X1)
| ~ group_element(X0)
| product(X0,X1,e_1)
| product(X0,X1,e_2)
| product(X0,X1,e_3)
| product(X0,X1,e_4)
| product(X0,X1,e_5) ) ).
cnf(u934,negated_conjecture,
( ~ product(e_3,X0,e_5)
| product(e_4,e_3,X0) ) ).
cnf(u1255,axiom,
( ~ product(e_2,e_4,X0)
| equalish(X0,e_1) ) ).
cnf(u41,axiom,
( ~ 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(X0,e_2,e_5) ) ).
cnf(u1298,axiom,
( ~ product(e_2,X0,e_5)
| equalish(X0,e_3) ) ).
cnf(element_4,axiom,
group_element(e_4) ).
cnf(e_2_is_not_e_3,axiom,
~ equalish(e_2,e_3) ).
cnf(u931,axiom,
( ~ product(X0,e_3,e_4)
| equalish(X0,e_5) ) ).
cnf(element_2,axiom,
group_element(e_2) ).
cnf(product_idempotence,axiom,
product(X0,X0,X0) ).
cnf(u922,negated_conjecture,
( ~ product(e_1,X0,e_5)
| product(e_2,e_1,X0) ) ).
cnf(e_3_is_not_e_5,axiom,
~ equalish(e_3,e_5) ).
cnf(u1297,axiom,
( ~ product(X0,e_3,e_5)
| equalish(X0,e_2) ) ).
cnf(u1346,axiom,
( ~ product(e_1,e_4,X0)
| equalish(X0,e_5) ) ).
cnf(u1289,axiom,
( ~ product(e_5,e_4,X0)
| equalish(X0,e_3) ) ).
cnf(u1302,axiom,
( ~ product(X0,e_4,e_2)
| equalish(X0,e_3) ) ).
cnf(u1236,axiom,
( ~ product(X0,e_3,e_2)
| equalish(X0,e_1) ) ).
cnf(e_1_is_not_e_2,axiom,
~ equalish(e_1,e_2) ).
cnf(u1186,axiom,
( ~ product(e_4,X0,e_5)
| equalish(X0,e_2) ) ).
cnf(u913,axiom,
( ~ product(X0,e_2,e_3)
| equalish(X0,e_1) ) ).
cnf(e_4_is_not_e_5,axiom,
~ equalish(e_4,e_5) ).
cnf(u1290,negated_conjecture,
( ~ product(e_4,X0,e_5)
| product(e_3,e_4,X0) ) ).
cnf(e_5_is_not_e_3,axiom,
~ equalish(e_5,e_3) ).
cnf(u1304,axiom,
( ~ product(e_3,e_4,X0)
| equalish(X0,e_2) ) ).
cnf(u1451,axiom,
( ~ product(e_1,X0,e_4)
| equalish(X0,e_5) ) ).
cnf(u916,negated_conjecture,
( ~ product(e_2,X0,e_1)
| product(e_3,e_2,X0) ) ).
cnf(u1238,axiom,
( ~ product(e_1,e_3,X0)
| equalish(X0,e_2) ) ).
cnf(u1242,axiom,
( ~ product(X0,e_1,e_3)
| equalish(X0,e_4) ) ).
cnf(u1215,negated_conjecture,
( ~ product(e_2,X0,e_3)
| product(e_4,e_2,X0) ) ).
cnf(u358,axiom,
( ~ product(X0,e_2,e_1)
| equalish(X0,e_5) ) ).
cnf(u1253,axiom,
( ~ product(X0,e_4,e_1)
| equalish(X0,e_2) ) ).
cnf(e_1_is_not_e_5,axiom,
~ equalish(e_1,e_5) ).
cnf(u1212,axiom,
( ~ product(X0,e_2,e_4)
| equalish(X0,e_3) ) ).
cnf(product_right_cancellation,axiom,
( ~ product(X0,X3,X2)
| ~ product(X0,X1,X2)
| equalish(X1,X3) ) ).
cnf(u1427,axiom,
( ~ product(e_2,X0,e_3)
| equalish(X0,e_5) ) ).
cnf(u1422,negated_conjecture,
( ~ product(e_5,X0,e_3)
| product(e_1,e_5,X0) ) ).
cnf(u1303,axiom,
( ~ product(e_3,X0,e_2)
| equalish(X0,e_4) ) ).
cnf(u35,axiom,
equalish(X0,X0) ).
cnf(u1214,axiom,
( ~ product(e_3,e_2,X0)
| equalish(X0,e_4) ) ).
cnf(u1182,axiom,
( ~ product(e_2,e_1,X0)
| equalish(X0,e_4) ) ).
cnf(u1421,axiom,
( ~ product(e_3,e_5,X0)
| equalish(X0,e_1) ) ).
cnf(u905,axiom,
( ~ product(e_3,e_1,X0)
| equalish(X0,e_5) ) ).
cnf(e_2_is_not_e_5,axiom,
~ equalish(e_2,e_5) ).
cnf(u1299,axiom,
( ~ product(e_2,e_3,X0)
| equalish(X0,e_5) ) ).
cnf(e_3_is_not_e_4,axiom,
~ equalish(e_3,e_4) ).
cnf(u1426,axiom,
( ~ product(X0,e_5,e_3)
| equalish(X0,e_2) ) ).
cnf(u1288,axiom,
( ~ product(e_5,X0,e_3)
| equalish(X0,e_4) ) ).
cnf(u42,axiom,
( ~ 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(X0,e_3,e_5) ) ).
cnf(u903,axiom,
( ~ product(X0,e_1,e_5)
| equalish(X0,e_3) ) ).
cnf(product_total_function2,axiom,
( ~ product(X0,X1,X3)
| ~ product(X0,X1,X2)
| equalish(X2,X3) ) ).
cnf(u1347,negated_conjecture,
( ~ product(e_4,X0,e_1)
| product(e_5,e_4,X0) ) ).
cnf(e_4_is_not_e_3,axiom,
~ equalish(e_4,e_3) ).
cnf(u1419,axiom,
( ~ product(X0,e_5,e_1)
| equalish(X0,e_3) ) ).
cnf(u1243,axiom,
( ~ product(e_4,X0,e_3)
| equalish(X0,e_1) ) ).
cnf(e_3_is_not_e_2,axiom,
~ equalish(e_3,e_2) ).
cnf(u1381,axiom,
( ~ product(X0,e_5,e_2)
| equalish(X0,e_4) ) ).
cnf(e_4_is_not_e_1,axiom,
~ equalish(e_4,e_1) ).
cnf(u1453,negated_conjecture,
( ~ product(e_5,X0,e_1)
| product(e_4,e_5,X0) ) ).
cnf(u1185,axiom,
( ~ product(X0,e_2,e_5)
| equalish(X0,e_4) ) ).
cnf(u1183,negated_conjecture,
( ~ product(e_1,X0,e_2)
| product(e_4,e_1,X0) ) ).
cnf(u1187,axiom,
( ~ product(e_4,e_2,X0)
| equalish(X0,e_5) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP127-1.005 : TPTP v9.3.1. Released v1.2.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.37 % Computer : n013.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Sun Sep 27 09:25:06 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.43 Running first-order theorem proving
% 0.11/0.43 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
% 2.95/1.61 % (4154714)Input is clausal, will run a generic CNF schedule.
% 2.95/1.61 % (4154719)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=204111495:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 2.95/1.61 % (4154721)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1110745601:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 2.95/1.61 % (4154723)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=553107149:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 2.95/1.61 % (4154724)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=673714649:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 2.95/1.61 % (4154720)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2451468946:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 2.95/1.61 % (4154722)lrs+10_1_sil=8000:sp=occurrence:random_seed=4141185805:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 2.95/1.61 % (4154725)dis-21_1_sil=8000:lcm=predicate:random_seed=1803978748: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)
% 2.95/1.61 % (4154723)Instruction limit reached!
% 2.95/1.61 % (4154723)------------------------------
% 2.95/1.61 % (4154723)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.95/1.61 % (4154723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.95/1.61 % (4154723)CaDiCaL version: 2.1.3
% 2.95/1.61 % (4154723)Termination reason: Instruction limit
% 2.95/1.61 % (4154723)Termination phase: Saturation
% 2.95/1.61 % (4154723)Time elapsed: 0.053 s
% 2.95/1.61 % (4154723)Peak memory usage: 87 MB
% 2.95/1.61 % (4154723)Instructions burned: 115 (million)
% 2.95/1.61 % (4154722)Instruction limit reached!
% 2.95/1.61 % (4154722)------------------------------
% 2.95/1.61 % (4154722)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.95/1.61 % (4154722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.95/1.61 % (4154722)CaDiCaL version: 2.1.3
% 2.95/1.61 % (4154722)Termination reason: Instruction limit
% 2.95/1.61 % (4154722)Termination phase: Saturation
% 2.95/1.61 % (4154722)Time elapsed: 0.060 s
% 2.95/1.61 % (4154722)Peak memory usage: 88 MB
% 2.95/1.61 % (4154722)Instructions burned: 109 (million)
% 2.95/1.61 % (4154725)Instruction limit reached!
% 2.95/1.61 % (4154725)------------------------------
% 2.95/1.61 % (4154725)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.95/1.61 % (4154725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.95/1.61 % (4154725)CaDiCaL version: 2.1.3
% 2.95/1.61 % (4154725)Termination reason: Instruction limit
% 2.95/1.61 % (4154725)Termination phase: Saturation
% 2.95/1.61 % (4154725)Time elapsed: 0.074 s
% 2.95/1.61 % (4154725)Peak memory usage: 89 MB
% 2.95/1.61 % (4154725)Instructions burned: 118 (million)
% 2.95/1.61 % (4154724)Instruction limit reached!
% 2.95/1.61 % (4154724)------------------------------
% 2.95/1.61 % (4154724)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.95/1.61 % (4154724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.95/1.61 % (4154724)CaDiCaL version: 2.1.3
% 2.95/1.61 % (4154724)Termination reason: Instruction limit
% 2.95/1.61 % (4154724)Termination phase: Saturation
% 2.95/1.61 % (4154724)Time elapsed: 0.108 s
% 2.95/1.61 % (4154724)Peak memory usage: 88 MB
% 2.95/1.61 % (4154724)Instructions burned: 180 (million)
% 2.95/1.61 % (4154733)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=2901501440:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 2.95/1.61 % (4154734)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2282768514: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)
% 2.95/1.61 % (4154734)Refutation not found, incomplete strategy
% 2.95/1.61 % (4154734)------------------------------
% 2.95/1.61 % (4154734)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.95/1.61 % (4154734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.95/1.61 % (4154734)CaDiCaL version: 2.1.3
% 2.95/1.61 % (4154734)Termination reason: Refutation not found, incomplete strategy
% 2.95/1.61 % (4154734)Time elapsed: 0.001 s
% 2.95/1.61 % (4154734)Peak memory usage: 87 MB
% 2.95/1.61 % (4154734)Instructions burned: 1 (million)
% 2.95/1.61 % (4154735)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3378060072:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 2.95/1.61 % (4154736)lrs+10_64_to=lpo:sil=8000:random_seed=1836849424:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 2.95/1.61 % (4154733)Instruction limit reached!
% 2.95/1.61 % (4154733)------------------------------
% 2.95/1.61 % (4154733)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.95/1.61 % (4154733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.95/1.61 % (4154733)CaDiCaL version: 2.1.3
% 2.95/1.61 % (4154733)Termination reason: Instruction limit
% 2.95/1.61 % (4154733)Termination phase: Saturation
% 2.95/1.61 % (4154733)Time elapsed: 0.086 s
% 2.95/1.61 % (4154733)Peak memory usage: 88 MB
% 2.95/1.61 % (4154733)Instructions burned: 144 (million)
% 2.95/1.61 % (4154736)First to succeed.
% 2.95/1.61 % (4154736)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-4154714"
% 2.95/1.61 % (4154735)Instruction limit reached!
% 2.95/1.61 % (4154735)------------------------------
% 2.95/1.61 % (4154735)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.95/1.61 % (4154735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.95/1.61 % (4154735)CaDiCaL version: 2.1.3
% 2.95/1.61 % (4154735)Termination reason: Instruction limit
% 2.95/1.61 % (4154735)Termination phase: Saturation
% 2.95/1.61 % (4154735)Time elapsed: 0.115 s
% 2.95/1.61 % (4154735)Peak memory usage: 88 MB
% 2.95/1.61 % (4154735)Instructions burned: 219 (million)
% 2.95/1.61 % (4154720)Refutation not found, incomplete strategy
% 2.95/1.61 % (4154720)------------------------------
% 2.95/1.61 % (4154720)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.95/1.61 % (4154720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.95/1.61 % (4154720)CaDiCaL version: 2.1.3
% 2.95/1.61 % (4154720)Termination reason: Refutation not found, incomplete strategy
% 2.95/1.61 % (4154720)Time elapsed: 0.447 s
% 2.95/1.61 % (4154720)Peak memory usage: 127 MB
% 2.95/1.61 % (4154720)Instructions burned: 918 (million)
% 2.95/1.61 % (4154734)------------------------------
% 2.95/1.61 % (4154734)------------------------------
% 2.95/1.61 % (4154741)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=2558266337:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 2.95/1.61 % SZS status Satisfiable for theBenchmark
% 2.95/1.61 % SZS output start Saturation.
% See solution above
% 5.73/1.71 % SZS output start Definitions and Model Updates.
% 5.73/1.71 % SZS output end Definitions and Model Updates.
% 5.73/1.71 % (4154736)------------------------------
% 5.73/1.71 % (4154736)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.73/1.71 % (4154736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.73/1.71 % (4154736)CaDiCaL version: 2.1.3
% 5.73/1.71 % (4154736)Termination reason: Satisfiable
% 5.73/1.71 % (4154736)Time elapsed: 0.023 s
% 5.73/1.71 % (4154736)Peak memory usage: 88 MB
% 5.73/1.71 % (4154736)Instructions burned: 35 (million)
% 5.73/1.71 % (4154736)------------------------------
% 5.73/1.71 % (4154736)------------------------------
% 5.73/1.71 % (4154714)Success in time 0.738 s
% 5.73/1.71 % Vampire exiting
%------------------------------------------------------------------------------