%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP130-1.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 : n011.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:00 AM UTC 2026
% Result : Satisfiable 48.81s 7.94s
% Output : Saturation 0.14s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u51,negated_conjecture,
~ product(e_5,e_5,e_1) ).
cnf(u56,negated_conjecture,
product(e_5,e_5,e_5) ).
cnf(u59,negated_conjecture,
~ product(e_5,e_5,e_2) ).
cnf(u63,negated_conjecture,
~ product(e_5,e_5,e_4) ).
cnf(u67,negated_conjecture,
~ product(e_5,e_5,e_3) ).
cnf(u72,negated_conjecture,
~ product(e_4,e_5,e_1) ).
cnf(u77,negated_conjecture,
product(e_4,e_5,e_2) ).
cnf(u80,negated_conjecture,
~ product(e_4,e_5,e_4) ).
cnf(u84,negated_conjecture,
~ product(e_4,e_5,e_3) ).
cnf(u89,negated_conjecture,
~ product(e_3,e_5,e_1) ).
cnf(u93,negated_conjecture,
~ product(e_3,e_5,e_2) ).
cnf(u98,negated_conjecture,
product(e_3,e_5,e_4) ).
cnf(u101,negated_conjecture,
~ product(e_3,e_5,e_3) ).
cnf(u107,negated_conjecture,
product(e_2,e_5,e_1) ).
cnf(u110,negated_conjecture,
~ product(e_2,e_5,e_2) ).
cnf(u114,negated_conjecture,
~ product(e_2,e_5,e_4) ).
cnf(u118,negated_conjecture,
~ product(e_2,e_5,e_3) ).
cnf(u123,negated_conjecture,
~ product(e_1,e_5,e_1) ).
cnf(u127,negated_conjecture,
~ product(e_1,e_5,e_2) ).
cnf(u131,negated_conjecture,
~ product(e_1,e_5,e_4) ).
cnf(u136,negated_conjecture,
product(e_1,e_5,e_3) ).
cnf(u147,negated_conjecture,
~ product(e_5,e_2,e_4) ).
cnf(u151,negated_conjecture,
~ product(e_5,e_2,e_3) ).
cnf(u155,negated_conjecture,
~ product(e_5,e_2,e_2) ).
cnf(u160,negated_conjecture,
product(e_5,e_2,e_1) ).
cnf(u173,negated_conjecture,
product(e_2,e_1,e_4) ).
cnf(u176,negated_conjecture,
~ product(e_2,e_1,e_3) ).
cnf(u180,negated_conjecture,
~ product(e_2,e_1,e_2) ).
cnf(u184,negated_conjecture,
~ product(e_2,e_1,e_1) ).
cnf(u197,negated_conjecture,
~ product(e_2,e_2,e_4) ).
cnf(u201,negated_conjecture,
~ product(e_2,e_2,e_3) ).
cnf(u206,negated_conjecture,
product(e_2,e_2,e_2) ).
cnf(u209,negated_conjecture,
~ product(e_2,e_2,e_1) ).
cnf(u222,negated_conjecture,
~ product(e_2,e_4,e_4) ).
cnf(u227,negated_conjecture,
product(e_2,e_4,e_3) ).
cnf(u230,negated_conjecture,
~ product(e_2,e_4,e_2) ).
cnf(u234,negated_conjecture,
~ product(e_2,e_4,e_1) ).
cnf(u247,negated_conjecture,
~ product(e_2,e_3,e_4) ).
cnf(u251,negated_conjecture,
~ product(e_2,e_3,e_3) ).
cnf(u255,negated_conjecture,
~ product(e_2,e_3,e_2) ).
cnf(u259,negated_conjecture,
~ product(e_2,e_3,e_1) ).
cnf(u292,negated_conjecture,
~ product(e_1,e_1,e_4) ).
cnf(u296,negated_conjecture,
~ product(e_1,e_1,e_3) ).
cnf(u300,negated_conjecture,
~ product(e_1,e_1,e_2) ).
cnf(u305,negated_conjecture,
product(e_1,e_1,e_1) ).
cnf(u316,negated_conjecture,
~ product(e_5,e_1,e_1) ).
cnf(u320,negated_conjecture,
~ product(e_1,e_4,e_4) ).
cnf(u324,negated_conjecture,
~ product(e_1,e_4,e_3) ).
cnf(u328,negated_conjecture,
~ product(e_1,e_4,e_2) ).
cnf(u332,negated_conjecture,
~ product(e_1,e_4,e_1) ).
cnf(u344,negated_conjecture,
~ product(e_5,e_4,e_1) ).
cnf(u349,negated_conjecture,
product(e_1,e_2,e_4) ).
cnf(u352,negated_conjecture,
~ product(e_1,e_2,e_3) ).
cnf(u356,negated_conjecture,
~ product(e_1,e_2,e_2) ).
cnf(u360,negated_conjecture,
~ product(e_1,e_2,e_1) ).
cnf(u400,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(u411,negated_conjecture,
~ product(e_5,e_3,e_1) ).
cnf(u416,negated_conjecture,
~ product(e_5,e_4,e_4) ).
cnf(u420,negated_conjecture,
~ product(e_5,e_4,e_3) ).
cnf(u425,negated_conjecture,
product(e_5,e_4,e_2) ).
cnf(u446,negated_conjecture,
~ product(e_5,e_3,e_5) ).
cnf(u450,negated_conjecture,
~ product(e_5,e_1,e_4) ).
cnf(u455,negated_conjecture,
product(e_5,e_1,e_3) ).
cnf(u458,negated_conjecture,
~ product(e_5,e_1,e_2) ).
cnf(u487,negated_conjecture,
~ product(e_4,e_4,e_5) ).
cnf(u492,negated_conjecture,
~ product(e_4,e_2,e_5) ).
cnf(u564,negated_conjecture,
~ product(e_5,e_2,e_5) ).
cnf(u595,negated_conjecture,
~ product(e_4,e_1,e_4) ).
cnf(u599,negated_conjecture,
~ product(e_4,e_1,e_3) ).
cnf(u603,negated_conjecture,
~ product(e_4,e_1,e_2) ).
cnf(u607,negated_conjecture,
~ product(e_4,e_1,e_1) ).
cnf(u623,negated_conjecture,
~ product(e_4,e_2,e_4) ).
cnf(u628,negated_conjecture,
product(e_4,e_2,e_3) ).
cnf(u631,negated_conjecture,
~ product(e_4,e_2,e_2) ).
cnf(u635,negated_conjecture,
~ product(e_4,e_2,e_1) ).
cnf(u671,negated_conjecture,
~ product(e_1,e_3,e_4) ).
cnf(u675,negated_conjecture,
~ product(e_1,e_3,e_3) ).
cnf(u680,negated_conjecture,
product(e_1,e_3,e_2) ).
cnf(u683,negated_conjecture,
~ product(e_1,e_3,e_1) ).
cnf(u696,negated_conjecture,
~ product(e_3,e_4,e_4) ).
cnf(u700,negated_conjecture,
~ product(e_3,e_4,e_3) ).
cnf(u704,negated_conjecture,
~ product(e_3,e_4,e_2) ).
cnf(u709,negated_conjecture,
product(e_3,e_4,e_1) ).
cnf(u727,negated_conjecture,
~ product(e_3,e_1,e_4) ).
cnf(u731,negated_conjecture,
~ product(e_3,e_1,e_3) ).
cnf(u736,negated_conjecture,
product(e_3,e_1,e_2) ).
cnf(u739,negated_conjecture,
~ product(e_3,e_1,e_1) ).
cnf(u753,negated_conjecture,
~ product(e_3,e_3,e_4) ).
cnf(u758,negated_conjecture,
product(e_3,e_3,e_3) ).
cnf(u761,negated_conjecture,
~ product(e_3,e_3,e_2) ).
cnf(u774,negated_conjecture,
~ product(e_3,e_2,e_4) ).
cnf(u778,negated_conjecture,
~ product(e_3,e_2,e_3) ).
cnf(u782,negated_conjecture,
~ product(e_3,e_2,e_2) ).
cnf(u842,negated_conjecture,
~ product(e_3,e_3,e_1) ).
cnf(u900,negated_conjecture,
~ product(e_3,e_2,e_1) ).
cnf(u1089,negated_conjecture,
product(e_4,e_4,e_4) ).
cnf(u1092,negated_conjecture,
~ product(e_4,e_4,e_3) ).
cnf(u1096,negated_conjecture,
~ product(e_4,e_4,e_2) ).
cnf(u1100,negated_conjecture,
~ product(e_4,e_4,e_1) ).
cnf(u1164,negated_conjecture,
~ product(e_5,e_4,e_5) ).
cnf(u1345,negated_conjecture,
~ product(e_4,e_3,e_4) ).
cnf(u1349,negated_conjecture,
~ product(e_4,e_3,e_3) ).
cnf(u1353,negated_conjecture,
~ product(e_4,e_3,e_2) ).
cnf(u1358,negated_conjecture,
product(e_4,e_3,e_1) ).
cnf(u12423,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(e_4_is_not_e_5,axiom,
~ equalish(e_4,e_5) ).
cnf(u11845,negated_conjecture,
( ~ product(X0,e_3,e_1)
| equalish(X0,e_4) ) ).
cnf(u12156,negated_conjecture,
( ~ product(X0,e_4,e_4)
| equalish(X0,e_4) ) ).
cnf(u32,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(u38,negated_conjecture,
( ~ group_element(X0)
| product(X0,e_5,e_3)
| product(X0,e_5,e_4)
| product(X0,e_5,e_2)
| product(e_5,e_1,X0)
| 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(u12200,negated_conjecture,
( ~ product(X0,e_2,e_2)
| equalish(X0,e_2) ) ).
cnf(u12206,negated_conjecture,
( ~ product(X0,e_2,e_4)
| equalish(X0,e_1) ) ).
cnf(u11949,negated_conjecture,
( ~ product(X0,e_5,e_5)
| equalish(X0,e_5) ) ).
cnf(u12044,negated_conjecture,
( ~ product(e_1,X0,e_3)
| product(e_2,X0,e_1) ) ).
cnf(u11996,negated_conjecture,
( ~ product(e_5,e_2,X0)
| equalish(X0,e_1) ) ).
cnf(u11994,negated_conjecture,
( ~ product(X0,e_2,e_1)
| equalish(X0,e_5) ) ).
cnf(u1492,negated_conjecture,
equalish(e_4,e_4) ).
cnf(u12123,negated_conjecture,
( ~ group_element(X0)
| 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) ) ).
cnf(u11997,negated_conjecture,
( ~ product(e_5,X0,e_2)
| product(e_1,X0,e_5) ) ).
cnf(u12052,negated_conjecture,
( ~ product(e_4,X0,e_3)
| equalish(X0,e_2) ) ).
cnf(u12400,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(u12249,negated_conjecture,
( ~ product(e_3,X0,e_1)
| product(e_2,X0,e_3) ) ).
cnf(u12353,negated_conjecture,
( ~ product(e_1,X0,e_5)
| equalish(X0,e_4) ) ).
cnf(u12399,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(u12412,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_4,X0) ) ).
cnf(e_1_is_not_e_3,axiom,
~ equalish(e_1,e_3) ).
cnf(u12390,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(u12067,negated_conjecture,
( ~ product(e_3,X0,e_1)
| equalish(X0,e_4) ) ).
cnf(element_5,axiom,
group_element(e_5) ).
cnf(u12396,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(e_3_is_not_e_4,axiom,
~ equalish(e_3,e_4) ).
cnf(u12036,negated_conjecture,
( ~ product(X0,e_5,e_3)
| equalish(X0,e_1) ) ).
cnf(u12111,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(u12201,negated_conjecture,
( ~ product(e_2,X0,e_2)
| equalish(X0,e_2) ) ).
cnf(e_5_is_not_e_1,axiom,
~ equalish(e_5,e_1) ).
cnf(u11665,negated_conjecture,
( ~ product(e_5,e_3,X0)
| equalish(X0,e_4) ) ).
cnf(u12330,negated_conjecture,
( ~ product(e_2,X0,e_3)
| product(e_5,X0,e_2) ) ).
cnf(u12028,negated_conjecture,
( ~ product(e_4,e_5,X0)
| equalish(X0,e_2) ) ).
cnf(u12068,negated_conjecture,
( ~ product(e_3,e_4,X0)
| equalish(X0,e_1) ) ).
cnf(u12389,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(u12247,negated_conjecture,
( ~ product(e_3,X0,e_2)
| equalish(X0,e_1) ) ).
cnf(u12342,negated_conjecture,
( ~ product(e_4,X0,e_1)
| product(e_5,X0,e_4) ) ).
cnf(u12470,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(u12157,negated_conjecture,
( ~ product(e_4,X0,e_4)
| equalish(X0,e_4) ) ).
cnf(u12358,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_1) ) ).
cnf(u12243,negated_conjecture,
( ~ product(e_5,e_1,X0)
| equalish(X0,e_3) ) ).
cnf(u12422,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(u12420,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(u12066,negated_conjecture,
( ~ product(X0,e_4,e_1)
| equalish(X0,e_3) ) ).
cnf(u12443,negated_conjecture,
( ~ product(e_3,e_2,X0)
| equalish(X0,e_5) ) ).
cnf(u12327,negated_conjecture,
( ~ product(X0,e_3,e_5)
| equalish(X0,e_2) ) ).
cnf(u12246,negated_conjecture,
( ~ product(X0,e_1,e_2)
| equalish(X0,e_3) ) ).
cnf(u12324,negated_conjecture,
product(e_2,e_3,e_5) ).
cnf(e_1_is_not_e_2,axiom,
~ equalish(e_1,e_2) ).
cnf(product_left_cancellation,axiom,
( ~ product(X3,X1,X2)
| ~ product(X0,X1,X2)
| equalish(X0,X3) ) ).
cnf(u12424,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(e_4_is_not_e_2,axiom,
~ equalish(e_4,e_2) ).
cnf(e_3_is_not_e_5,axiom,
~ equalish(e_3,e_5) ).
cnf(u34,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(u12398,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(u12238,negated_conjecture,
( ~ product(e_5,e_4,X0)
| equalish(X0,e_2) ) ).
cnf(u12107,negated_conjecture,
( ~ group_element(X0)
| 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) ) ).
cnf(u12393,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(u12237,negated_conjecture,
( ~ product(e_5,X0,e_2)
| equalish(X0,e_4) ) ).
cnf(u12421,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(u12401,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(u12414,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(u12233,negated_conjecture,
( ~ product(e_2,e_1,X0)
| equalish(X0,e_4) ) ).
cnf(u12339,negated_conjecture,
( ~ product(X0,e_1,e_5)
| equalish(X0,e_4) ) ).
cnf(u12510,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(u12227,negated_conjecture,
( ~ product(e_2,X0,e_3)
| equalish(X0,e_4) ) ).
cnf(u914,negated_conjecture,
equalish(e_3,e_3) ).
cnf(u12236,negated_conjecture,
( ~ product(X0,e_4,e_2)
| equalish(X0,e_5) ) ).
cnf(u12023,negated_conjecture,
( ~ product(e_3,e_5,X0)
| equalish(X0,e_4) ) ).
cnf(u12029,negated_conjecture,
( ~ product(e_4,X0,e_5)
| product(e_2,X0,e_4) ) ).
cnf(u12515,negated_conjecture,
( ~ group_element(X0)
| equalish(X0,e_4)
| product(e_1,X0,e_1)
| product(e_1,X0,e_2)
| product(e_1,X0,e_3)
| product(e_1,X0,e_4) ) ).
cnf(e_2_is_not_e_5,axiom,
~ equalish(e_2,e_5) ).
cnf(u41,negated_conjecture,
( ~ group_element(X0)
| product(X0,e_5,e_3)
| product(X0,e_5,e_4)
| product(X0,e_5,e_2)
| product(e_5,e_4,X0)
| 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(u12541,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(element_3,axiom,
group_element(e_3) ).
cnf(qg3,negated_conjecture,
( ~ product(X0,X2,X3)
| ~ product(X0,X1,X2)
| product(X3,X1,X0) ) ).
cnf(element_1,axiom,
group_element(e_1) ).
cnf(u12054,negated_conjecture,
( ~ product(e_4,X0,e_2)
| product(e_3,X0,e_4) ) ).
cnf(product_right_cancellation,axiom,
( ~ product(X0,X3,X2)
| ~ product(X0,X1,X2)
| equalish(X1,X3) ) ).
cnf(u12032,negated_conjecture,
( ~ product(e_2,X0,e_1)
| equalish(X0,e_5) ) ).
cnf(u43,negated_conjecture,
( ~ group_element(X0)
| product(X0,e_5,e_3)
| product(X0,e_5,e_4)
| product(X0,e_5,e_2)
| product(e_5,e_5,X0)
| product(X0,e_5,e_1) ) ).
cnf(u11663,negated_conjecture,
( ~ product(X0,e_3,e_4)
| equalish(X0,e_5) ) ).
cnf(e_4_is_not_e_1,axiom,
~ equalish(e_4,e_1) ).
cnf(u12158,negated_conjecture,
( ~ product(e_4,e_4,X0)
| equalish(X0,e_4) ) ).
cnf(u12340,negated_conjecture,
( ~ product(e_4,X0,e_5)
| equalish(X0,e_1) ) ).
cnf(u12495,negated_conjecture,
( ~ product(e_3,X0,e_5)
| equalish(X0,e_2) ) ).
cnf(u12304,negated_conjecture,
( ~ product(X0,e_1,e_1)
| equalish(X0,e_1) ) ).
cnf(u12468,negated_conjecture,
( ~ product(X0,e_2,e_5)
| equalish(X0,e_3) ) ).
cnf(u12037,negated_conjecture,
( ~ product(e_1,X0,e_3)
| equalish(X0,e_5) ) ).
cnf(u12354,negated_conjecture,
( ~ product(e_1,e_4,X0)
| equalish(X0,e_5) ) ).
cnf(u12336,negated_conjecture,
product(e_4,e_1,e_5) ).
cnf(u12042,negated_conjecture,
( ~ product(e_1,X0,e_2)
| equalish(X0,e_3) ) ).
cnf(u12231,negated_conjecture,
( ~ product(X0,e_1,e_4)
| equalish(X0,e_2) ) ).
cnf(u12388,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(u12021,negated_conjecture,
( ~ product(X0,e_5,e_4)
| equalish(X0,e_3) ) ).
cnf(u12355,negated_conjecture,
( ~ product(e_1,X0,e_4)
| product(e_5,X0,e_1) ) ).
cnf(u12386,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(u11846,negated_conjecture,
( ~ product(e_4,X0,e_1)
| equalish(X0,e_3) ) ).
cnf(u370,negated_conjecture,
equalish(e_5,e_5) ).
cnf(u12394,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_3,X0) ) ).
cnf(e_3_is_not_e_1,axiom,
~ equalish(e_3,e_1) ).
cnf(u12305,negated_conjecture,
( ~ product(e_1,X0,e_1)
| equalish(X0,e_1) ) ).
cnf(u12507,negated_conjecture,
( ~ group_element(X0)
| equalish(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(e_2_is_not_e_4,axiom,
~ equalish(e_2,e_4) ).
cnf(u1929,negated_conjecture,
equalish(e_2,e_2) ).
cnf(product_total_function2,axiom,
( ~ product(X0,X1,X3)
| ~ product(X0,X1,X2)
| equalish(X2,X3) ) ).
cnf(u11664,negated_conjecture,
( ~ product(e_5,X0,e_4)
| equalish(X0,e_3) ) ).
cnf(element_2,axiom,
group_element(e_2) ).
cnf(e_5_is_not_e_4,axiom,
~ equalish(e_5,e_4) ).
cnf(u40,negated_conjecture,
( ~ group_element(X0)
| product(X0,e_5,e_3)
| product(X0,e_5,e_4)
| product(X0,e_5,e_2)
| product(e_5,e_3,X0)
| 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(u31,negated_conjecture,
( ~ product(X1,X2,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(e_5,X2,X1) ) ).
cnf(u12069,negated_conjecture,
( ~ product(e_3,X0,e_4)
| product(e_1,X0,e_3) ) ).
cnf(u11666,negated_conjecture,
( ~ product(e_5,X0,e_3)
| product(e_4,X0,e_5) ) ).
cnf(u12087,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(u12209,negated_conjecture,
( ~ product(e_1,X0,e_2)
| product(e_4,X0,e_1) ) ).
cnf(u12352,negated_conjecture,
( ~ product(X0,e_4,e_5)
| equalish(X0,e_1) ) ).
cnf(u12333,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_2) ) ).
cnf(u12244,negated_conjecture,
( ~ product(e_5,X0,e_1)
| product(e_3,X0,e_5) ) ).
cnf(u12306,negated_conjecture,
( ~ product(e_1,e_1,X0)
| equalish(X0,e_1) ) ).
cnf(u11847,negated_conjecture,
( ~ product(e_4,e_3,X0)
| equalish(X0,e_1) ) ).
cnf(u12031,negated_conjecture,
( ~ product(X0,e_5,e_1)
| equalish(X0,e_2) ) ).
cnf(u11995,negated_conjecture,
( ~ product(e_5,X0,e_1)
| equalish(X0,e_2) ) ).
cnf(u12202,negated_conjecture,
( ~ product(e_2,e_2,X0)
| equalish(X0,e_2) ) ).
cnf(u12208,negated_conjecture,
( ~ product(e_1,e_2,X0)
| equalish(X0,e_4) ) ).
cnf(e_2_is_not_e_3,axiom,
~ equalish(e_2,e_3) ).
cnf(e_1_is_not_e_5,axiom,
~ equalish(e_1,e_5) ).
cnf(u39,negated_conjecture,
( ~ group_element(X0)
| product(X0,e_5,e_3)
| product(X0,e_5,e_4)
| product(X0,e_5,e_2)
| product(e_5,e_2,X0)
| 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(e_3_is_not_e_2,axiom,
~ equalish(e_3,e_2) ).
cnf(u12053,negated_conjecture,
( ~ product(e_4,e_2,X0)
| equalish(X0,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(u11951,negated_conjecture,
( ~ product(e_5,e_5,X0)
| equalish(X0,e_5) ) ).
cnf(u12387,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(e_5_is_not_e_3,axiom,
~ equalish(e_5,e_3) ).
cnf(u12328,negated_conjecture,
( ~ product(e_2,X0,e_5)
| equalish(X0,e_3) ) ).
cnf(u12402,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(u12207,negated_conjecture,
( ~ product(e_1,X0,e_4)
| equalish(X0,e_2) ) ).
cnf(u11950,negated_conjecture,
( ~ product(e_5,X0,e_5)
| equalish(X0,e_5) ) ).
cnf(u12024,negated_conjecture,
( ~ product(e_3,X0,e_5)
| product(e_4,X0,e_3) ) ).
cnf(u12391,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(u33,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(u12242,negated_conjecture,
( ~ product(e_5,X0,e_3)
| equalish(X0,e_1) ) ).
cnf(u12349,negated_conjecture,
product(e_1,e_4,e_5) ).
cnf(u12228,negated_conjecture,
( ~ product(e_2,e_4,X0)
| equalish(X0,e_3) ) ).
cnf(u12226,negated_conjecture,
( ~ product(X0,e_4,e_3)
| equalish(X0,e_2) ) ).
cnf(u12022,negated_conjecture,
( ~ product(e_3,X0,e_4)
| equalish(X0,e_5) ) ).
cnf(u12248,negated_conjecture,
( ~ product(e_3,e_1,X0)
| equalish(X0,e_2) ) ).
cnf(u12341,negated_conjecture,
( ~ product(e_4,e_1,X0)
| equalish(X0,e_5) ) ).
cnf(u12409,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_4_is_not_e_3,axiom,
~ equalish(e_4,e_3) ).
cnf(u12241,negated_conjecture,
( ~ product(X0,e_1,e_3)
| equalish(X0,e_5) ) ).
cnf(u11848,negated_conjecture,
( ~ product(e_4,X0,e_3)
| product(e_1,X0,e_4) ) ).
cnf(u12043,negated_conjecture,
( ~ product(e_1,e_3,X0)
| equalish(X0,e_2) ) ).
cnf(u12329,negated_conjecture,
( ~ product(e_2,e_3,X0)
| equalish(X0,e_5) ) ).
cnf(e_2_is_not_e_1,axiom,
~ equalish(e_2,e_1) ).
cnf(u12026,negated_conjecture,
( ~ product(X0,e_5,e_2)
| equalish(X0,e_4) ) ).
cnf(u12403,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(u12488,negated_conjecture,
product(e_3,e_2,e_5) ).
cnf(e_1_is_not_e_4,axiom,
~ equalish(e_1,e_4) ).
cnf(u12120,negated_conjecture,
( ~ group_element(X0)
| 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) ) ).
cnf(u12411,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(u12490,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(u12345,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(u37,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,X0)
| product(X0,e_5,e_1)
| product(X0,X1,e_1)
| product(X0,X1,e_2)
| product(X0,X1,e_3)
| product(X0,X1,e_4) ) ).
cnf(u12229,negated_conjecture,
( ~ product(e_2,X0,e_4)
| product(e_3,X0,e_2) ) ).
cnf(u12234,negated_conjecture,
( ~ product(e_2,X0,e_1)
| product(e_4,X0,e_2) ) ).
cnf(u12027,negated_conjecture,
( ~ product(e_4,X0,e_2)
| equalish(X0,e_5) ) ).
cnf(u12118,negated_conjecture,
( ~ group_element(X0)
| 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) ) ).
cnf(u12038,negated_conjecture,
( ~ product(e_1,e_5,X0)
| equalish(X0,e_3) ) ).
cnf(u12232,negated_conjecture,
( ~ product(e_2,X0,e_4)
| equalish(X0,e_1) ) ).
cnf(u12034,negated_conjecture,
( ~ product(e_2,X0,e_5)
| product(e_1,X0,e_2) ) ).
cnf(u12041,negated_conjecture,
( ~ product(X0,e_3,e_2)
| equalish(X0,e_1) ) ).
cnf(element_4,axiom,
group_element(e_4) ).
cnf(u12239,negated_conjecture,
( ~ product(e_5,X0,e_4)
| product(e_2,X0,e_5) ) ).
cnf(u12497,negated_conjecture,
( ~ product(e_3,X0,e_2)
| product(e_5,X0,e_3) ) ).
cnf(u12033,negated_conjecture,
( ~ product(e_2,e_5,X0)
| equalish(X0,e_1) ) ).
cnf(u12282,negated_conjecture,
( ~ product(e_3,X0,e_3)
| equalish(X0,e_3) ) ).
cnf(u6514,negated_conjecture,
equalish(e_1,e_1) ).
cnf(u12283,negated_conjecture,
( ~ product(e_3,e_3,X0)
| equalish(X0,e_3) ) ).
cnf(u12039,negated_conjecture,
( ~ product(e_1,X0,e_5)
| product(e_3,X0,e_1) ) ).
cnf(e_5_is_not_e_2,axiom,
~ equalish(e_5,e_2) ).
cnf(u12051,negated_conjecture,
( ~ product(X0,e_2,e_3)
| equalish(X0,e_4) ) ).
cnf(u12281,negated_conjecture,
( ~ product(X0,e_3,e_3)
| equalish(X0,e_3) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP130-1.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.11/0.35 % Computer : n011.cluster.edu
% 0.11/0.35 % Model : x86_64 x86_64
% 0.11/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.35 % Memory : 8046.5625MB
% 0.11/0.35 % OS : Linux 6.8.0-71-generic
% 0.11/0.35 % CPULimit : 300
% 0.11/0.35 % WCLimit : 300
% 0.11/0.35 % DateTime : Sun Sep 27 09:28:15 UTC 2026
% 0.11/0.36 % CPUTime :
% 0.11/0.36 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.39 Running first-order theorem proving
% 0.13/0.39 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.82/2.10 % (2145992)Input is clausal, will run a generic CNF schedule.
% 8.82/2.10 % (2146001)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2750373486:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 8.82/2.10 % (2146001)Instruction limit reached!
% 8.82/2.10 % (2146001)------------------------------
% 8.82/2.10 % (2146001)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.82/2.10 % (2146001)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.82/2.10 % (2146001)CaDiCaL version: 2.1.3
% 8.82/2.10 % (2146001)Termination reason: Instruction limit
% 8.82/2.10 % (2146001)Termination phase: Saturation
% 8.82/2.10 % (2146001)Time elapsed: 0.032 s
% 8.82/2.10 % (2146001)Peak memory usage: 88 MB
% 8.82/2.10 % (2146001)Instructions burned: 118 (million)
% 8.82/2.10 % (2145997)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=3590504709:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 8.82/2.10 % (2145999)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3015228174:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 8.82/2.10 % (2145998)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=224929692:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 8.82/2.10 % (2146003)dis-21_1_sil=8000:lcm=predicate:random_seed=3205307863: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.10 % (2146000)lrs+10_1_sil=8000:sp=occurrence:random_seed=992929248:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 8.82/2.10 % (2146002)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2210441131:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 8.82/2.10 % (2146000)Instruction limit reached!
% 8.82/2.10 % (2146000)------------------------------
% 8.82/2.10 % (2146000)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.82/2.10 % (2146000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.82/2.10 % (2146000)CaDiCaL version: 2.1.3
% 8.82/2.10 % (2146000)Termination reason: Instruction limit
% 8.82/2.10 % (2146000)Termination phase: Saturation
% 8.82/2.10 % (2146000)Time elapsed: 0.056 s
% 8.82/2.10 % (2146000)Peak memory usage: 88 MB
% 8.82/2.10 % (2146000)Instructions burned: 109 (million)
% 8.82/2.10 % (2146003)Instruction limit reached!
% 8.82/2.10 % (2146003)------------------------------
% 8.82/2.10 % (2146003)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.82/2.10 % (2146003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.82/2.10 % (2146003)CaDiCaL version: 2.1.3
% 8.82/2.10 % (2146003)Termination reason: Instruction limit
% 8.82/2.10 % (2146003)Termination phase: Saturation
% 8.82/2.10 % (2146003)Time elapsed: 0.074 s
% 8.82/2.10 % (2146003)Peak memory usage: 88 MB
% 8.82/2.10 % (2146003)Instructions burned: 117 (million)
% 8.82/2.10 % (2146005)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=3415204426:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 8.82/2.10 % (2146002)Instruction limit reached!
% 8.82/2.10 % (2146002)------------------------------
% 8.82/2.10 % (2146002)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.82/2.10 % (2146002)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.82/2.10 % (2146002)CaDiCaL version: 2.1.3
% 8.82/2.10 % (2146002)Termination reason: Instruction limit
% 8.82/2.10 % (2146002)Termination phase: Saturation
% 8.82/2.10 % (2146002)Time elapsed: 0.109 s
% 8.82/2.10 % (2146002)Peak memory usage: 89 MB
% 8.82/2.10 % (2146002)Instructions burned: 180 (million)
% 8.82/2.10 % (2146005)Instruction limit reached!
% 8.82/2.10 % (2146005)------------------------------
% 8.82/2.10 % (2146005)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.82/2.10 % (2146005)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.82/2.10 % (2146005)CaDiCaL version: 2.1.3
% 8.82/2.10 % (2146005)Termination reason: Instruction limit
% 8.82/2.10 % (2146005)Termination phase: Saturation
% 8.82/2.10 % (2146005)Time elapsed: 0.043 s
% 8.82/2.10 % (2146005)Peak memory usage: 88 MB
% 8.82/2.10 % (2146005)Instructions burned: 146 (million)
% 8.82/2.10 % (2146012)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1289808989: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.66/2.97 % (2146012)Refutation not found, incomplete strategy
% 13.66/2.97 % (2146012)------------------------------
% 13.66/2.97 % (2146012)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.66/2.97 % (2146012)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.66/2.97 % (2146012)CaDiCaL version: 2.1.3
% 13.66/2.97 % (2146012)Termination reason: Refutation not found, incomplete strategy
% 13.66/2.97 % (2146012)Time elapsed: 0.002 s
% 13.66/2.97 % (2146012)Peak memory usage: 87 MB
% 13.66/2.97 % (2146012)Instructions burned: 1 (million)
% 13.66/2.97 % (2146013)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=4218425703:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 13.66/2.97 % (2146015)lrs+10_64_to=lpo:sil=8000:random_seed=2662176725:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 13.66/2.97 % (2146016)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=2704707575:avsq=on:i=194:fgj=on:bd=preordered_2996 on theBenchmark for (2996ds/194Mi)
% 13.66/2.97 % (2146016)Instruction limit reached!
% 13.66/2.97 % (2146016)------------------------------
% 13.66/2.97 % (2146016)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.66/2.97 % (2146016)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.66/2.97 % (2146016)CaDiCaL version: 2.1.3
% 13.66/2.97 % (2146016)Termination reason: Instruction limit
% 13.66/2.97 % (2146016)Termination phase: Saturation
% 13.66/2.97 % (2146016)Time elapsed: 0.039 s
% 13.66/2.97 % (2146016)Peak memory usage: 87 MB
% 13.66/2.97 % (2146016)Instructions burned: 201 (million)
% 13.66/2.97 % (2146015)Instruction limit reached!
% 13.66/2.97 % (2146015)------------------------------
% 13.66/2.97 % (2146015)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.66/2.97 % (2146015)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.66/2.97 % (2146015)CaDiCaL version: 2.1.3
% 13.66/2.97 % (2146015)Termination reason: Instruction limit
% 13.66/2.97 % (2146015)Termination phase: Saturation
% 13.66/2.97 % (2146015)Time elapsed: 0.076 s
% 13.66/2.97 % (2146015)Peak memory usage: 88 MB
% 13.66/2.97 % (2146015)Instructions burned: 126 (million)
% 13.66/2.97 % (2146013)Instruction limit reached!
% 13.66/2.97 % (2146013)------------------------------
% 13.66/2.97 % (2146013)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.66/2.97 % (2146013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.66/2.97 % (2146013)CaDiCaL version: 2.1.3
% 13.66/2.97 % (2146013)Termination reason: Instruction limit
% 13.66/2.97 % (2146013)Termination phase: Saturation
% 13.66/2.97 % (2146013)Time elapsed: 0.119 s
% 13.66/2.97 % (2146013)Peak memory usage: 88 MB
% 13.66/2.97 % (2146013)Instructions burned: 220 (million)
% 13.66/2.97 % (2146021)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=2381420447:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 13.66/2.97 % (2146012)------------------------------
% 13.66/2.97 % (2146012)------------------------------
% 13.66/2.97 % (2146021)Instruction limit reached!
% 13.66/2.97 % (2146021)------------------------------
% 13.66/2.97 % (2146021)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.66/2.97 % (2146021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.66/2.97 % (2146021)CaDiCaL version: 2.1.3
% 13.66/2.97 % (2146021)Termination reason: Instruction limit
% 13.66/2.97 % (2146021)Termination phase: Saturation
% 13.66/2.97 % (2146021)Time elapsed: 0.042 s
% 13.66/2.97 % (2146021)Peak memory usage: 88 MB
% 13.66/2.97 % (2146021)Instructions burned: 159 (million)
% 13.66/2.97 % (2146022)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=2029241367:i=3394:sd=4:ss=included:sgt=64_2995 on theBenchmark for (2995ds/3394Mi)
% 13.66/2.97 % (2146023)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=3994542288:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2994 on theBenchmark for (2994ds/106Mi)
% 13.66/2.97 % (2146023)Refutation not found, incomplete strategy
% 13.66/2.97 % (2146023)------------------------------
% 13.66/2.97 % (2146023)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.66/2.97 % (2146023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.05/3.82 % (2146023)CaDiCaL version: 2.1.3
% 21.05/3.82 % (2146023)Termination reason: Refutation not found, incomplete strategy
% 21.05/3.82 % (2146023)Time elapsed: 0.002 s
% 21.05/3.82 % (2146023)Peak memory usage: 87 MB
% 21.05/3.82 % (2146023)Instructions burned: 1 (million)
% 21.05/3.82 % (2146026)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3691558924:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2993 on theBenchmark for (2993ds/242Mi)
% 21.05/3.82 % (2145998)Refutation not found, incomplete strategy
% 21.05/3.82 % (2145998)------------------------------
% 21.05/3.82 % (2145998)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.05/3.82 % (2145998)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.05/3.82 % (2145998)CaDiCaL version: 2.1.3
% 21.05/3.82 % (2145998)Termination reason: Refutation not found, incomplete strategy
% 21.05/3.82 % (2145998)Time elapsed: 0.579 s
% 21.05/3.82 % (2145998)Peak memory usage: 126 MB
% 21.05/3.82 % (2145998)Instructions burned: 858 (million)
% 21.05/3.82 % (2146025)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1407416219:i=107_2993 on theBenchmark for (2993ds/107Mi)
% 21.05/3.82 % (2146026)Instruction limit reached!
% 21.05/3.82 % (2146026)------------------------------
% 21.05/3.82 % (2146026)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.05/3.82 % (2146026)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.05/3.82 % (2146026)CaDiCaL version: 2.1.3
% 21.05/3.82 % (2146026)Termination reason: Instruction limit
% 21.05/3.82 % (2146026)Termination phase: Saturation
% 21.05/3.82 % (2146026)Time elapsed: 0.065 s
% 21.05/3.82 % (2146026)Peak memory usage: 88 MB
% 21.05/3.82 % (2146026)Instructions burned: 244 (million)
% 21.05/3.82 % (2146025)Instruction limit reached!
% 21.05/3.82 % (2146025)------------------------------
% 21.05/3.82 % (2146025)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.05/3.82 % (2146025)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.05/3.82 % (2146025)CaDiCaL version: 2.1.3
% 21.05/3.82 % (2146025)Termination reason: Instruction limit
% 21.05/3.82 % (2146025)Termination phase: Saturation
% 21.05/3.82 % (2146025)Time elapsed: 0.064 s
% 21.05/3.82 % (2146025)Peak memory usage: 88 MB
% 21.05/3.82 % (2146025)Instructions burned: 107 (million)
% 21.05/3.82 % (2146031)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=99266632:cond=fast:i=5208:av=off_2992 on theBenchmark for (2992ds/5208Mi)
% 21.05/3.82 % (2146023)------------------------------
% 21.05/3.82 % (2146023)------------------------------
% 21.05/3.82 % (2145998)------------------------------
% 21.05/3.82 % (2145998)------------------------------
% 21.05/3.82 % (2146032)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=3039347801:i=134:sd=2:doe=on:ss=axioms:sgt=14_2991 on theBenchmark for (2991ds/134Mi)
% 21.05/3.82 % (2146032)Instruction limit reached!
% 21.05/3.82 % (2146032)------------------------------
% 21.05/3.82 % (2146032)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.05/3.82 % (2146032)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.05/3.82 % (2146032)CaDiCaL version: 2.1.3
% 21.05/3.82 % (2146032)Termination reason: Instruction limit
% 21.05/3.82 % (2146032)Termination phase: Saturation
% 21.05/3.82 % (2146032)Time elapsed: 0.052 s
% 21.05/3.82 % (2146032)Peak memory usage: 87 MB
% 21.05/3.82 % (2146032)Instructions burned: 136 (million)
% 21.05/3.82 % (2146034)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=1458338373:i=499:bd=all_2990 on theBenchmark for (2990ds/499Mi)
% 21.05/3.82 % (2146036)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=1222583186:i=191:fgj=on:bd=all_2990 on theBenchmark for (2990ds/191Mi)
% 21.05/3.82 % (2146037)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2407137134:i=264:kws=precedence:fsr=off_2989 on theBenchmark for (2989ds/264Mi)
% 21.05/3.82 % (2146036)Instruction limit reached!
% 21.05/3.82 % (2146036)------------------------------
% 21.05/3.82 % (2146036)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.05/3.82 % (2146036)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.05/3.82 % (2146036)CaDiCaL version: 2.1.3
% 21.05/3.82 % (2146036)Termination reason: Instruction limit
% 32.00/5.39 % (2146036)Termination phase: Saturation
% 32.00/5.39 % (2146036)Time elapsed: 0.114 s
% 32.00/5.39 % (2146036)Peak memory usage: 88 MB
% 32.00/5.39 % (2146036)Instructions burned: 194 (million)
% 32.00/5.39 % (2146034)Instruction limit reached!
% 32.00/5.39 % (2146034)------------------------------
% 32.00/5.39 % (2146034)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.00/5.39 % (2146034)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.00/5.39 % (2146034)CaDiCaL version: 2.1.3
% 32.00/5.39 % (2146034)Termination reason: Instruction limit
% 32.00/5.39 % (2146034)Termination phase: Saturation
% 32.00/5.39 % (2146034)Time elapsed: 0.248 s
% 32.00/5.39 % (2146034)Peak memory usage: 89 MB
% 32.00/5.39 % (2146034)Instructions burned: 500 (million)
% 32.00/5.39 % (2146037)Instruction limit reached!
% 32.00/5.39 % (2146037)------------------------------
% 32.00/5.39 % (2146037)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.00/5.39 % (2146037)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.00/5.39 % (2146037)CaDiCaL version: 2.1.3
% 32.00/5.39 % (2146037)Termination reason: Instruction limit
% 32.00/5.39 % (2146037)Termination phase: Saturation
% 32.00/5.39 % (2146037)Time elapsed: 0.160 s
% 32.00/5.39 % (2146037)Peak memory usage: 90 MB
% 32.00/5.39 % (2146037)Instructions burned: 265 (million)
% 32.00/5.39 % (2146041)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=741794667:cond=on:i=156:bs=on:gtg=exists_all:er=known_2987 on theBenchmark for (2987ds/156Mi)
% 32.00/5.39 % (2146042)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=1459055480:i=3256:kws=precedence:bd=preordered:av=off_2986 on theBenchmark for (2986ds/3256Mi)
% 32.00/5.39 % (2146043)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=1114828507:i=537:av=off:ss=included_2986 on theBenchmark for (2986ds/537Mi)
% 32.00/5.39 % (2146041)Instruction limit reached!
% 32.00/5.39 % (2146041)------------------------------
% 32.00/5.39 % (2146041)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.00/5.39 % (2146041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.00/5.39 % (2146041)CaDiCaL version: 2.1.3
% 32.00/5.39 % (2146041)Termination reason: Instruction limit
% 32.00/5.39 % (2146041)Termination phase: Saturation
% 32.00/5.39 % (2146041)Time elapsed: 0.089 s
% 32.00/5.39 % (2146041)Peak memory usage: 88 MB
% 32.00/5.39 % (2146041)Instructions burned: 156 (million)
% 32.00/5.39 % (2146047)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=2876482857:i=180:bd=preordered:av=off_2984 on theBenchmark for (2984ds/180Mi)
% 32.00/5.39 % (2146043)Instruction limit reached!
% 32.00/5.39 % (2146043)------------------------------
% 32.00/5.39 % (2146043)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.00/5.39 % (2146043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.00/5.39 % (2146043)CaDiCaL version: 2.1.3
% 32.00/5.39 % (2146043)Termination reason: Instruction limit
% 32.00/5.39 % (2146043)Termination phase: Saturation
% 32.00/5.39 % (2146043)Time elapsed: 0.202 s
% 32.00/5.39 % (2146043)Peak memory usage: 88 MB
% 32.00/5.39 % (2146043)Instructions burned: 538 (million)
% 32.00/5.39 % (2146047)Instruction limit reached!
% 32.00/5.39 % (2146047)------------------------------
% 32.00/5.39 % (2146047)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.00/5.39 % (2146047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.00/5.39 % (2146047)CaDiCaL version: 2.1.3
% 32.00/5.39 % (2146047)Termination reason: Instruction limit
% 32.00/5.39 % (2146047)Termination phase: Saturation
% 32.00/5.39 % (2146047)Time elapsed: 0.092 s
% 32.00/5.39 % (2146047)Peak memory usage: 87 MB
% 32.00/5.39 % (2146047)Instructions burned: 181 (million)
% 32.00/5.39 % (2146049)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=3997278288:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2982 on theBenchmark for (2982ds/10307Mi)
% 32.00/5.39 % (2146050)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=2033169163:i=412:gtgl=4:gtg=exists_all_2982 on theBenchmark for (2982ds/412Mi)
% 32.00/5.39 % (2146050)Instruction limit reached!
% 32.00/5.39 % (2146050)------------------------------
% 32.00/5.39 % (2146050)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.27/7.08 % (2146050)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.27/7.08 % (2146050)CaDiCaL version: 2.1.3
% 44.27/7.08 % (2146050)Termination reason: Instruction limit
% 44.27/7.08 % (2146050)Termination phase: Saturation
% 44.27/7.08 % (2146050)Time elapsed: 0.217 s
% 44.27/7.08 % (2146050)Peak memory usage: 91 MB
% 44.27/7.08 % (2146050)Instructions burned: 413 (million)
% 44.27/7.08 % (2146031)Instruction limit reached!
% 44.27/7.08 % (2146031)------------------------------
% 44.27/7.08 % (2146031)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.27/7.08 % (2146031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.27/7.08 % (2146031)CaDiCaL version: 2.1.3
% 44.27/7.08 % (2146031)Termination reason: Instruction limit
% 44.27/7.08 % (2146031)Termination phase: Saturation
% 44.27/7.08 % (2146031)Time elapsed: 1.307 s
% 44.27/7.08 % (2146031)Peak memory usage: 131 MB
% 44.27/7.08 % (2146031)Instructions burned: 5210 (million)
% 44.27/7.08 % (2146053)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=820787120:s2pl=no:i=8478:s2at=4:nm=6_2978 on theBenchmark for (2978ds/8478Mi)
% 44.27/7.08 % (2146054)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=511993618:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2977 on theBenchmark for (2977ds/303Mi)
% 44.27/7.08 % (2146054)Instruction limit reached!
% 44.27/7.08 % (2146054)------------------------------
% 44.27/7.08 % (2146054)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.27/7.08 % (2146054)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.27/7.08 % (2146054)CaDiCaL version: 2.1.3
% 44.27/7.08 % (2146054)Termination reason: Instruction limit
% 44.27/7.08 % (2146054)Termination phase: Saturation
% 44.27/7.08 % (2146054)Time elapsed: 0.096 s
% 44.27/7.08 % (2146054)Peak memory usage: 90 MB
% 44.27/7.08 % (2146054)Instructions burned: 304 (million)
% 44.27/7.08 % (2146057)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=3632410989:st=4:i=720:sd=3:fsr=off:ss=axioms_2975 on theBenchmark for (2975ds/720Mi)
% 44.27/7.08 % (2146057)Refutation not found, incomplete strategy
% 44.27/7.08 % (2146057)------------------------------
% 44.27/7.08 % (2146057)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.27/7.08 % (2146057)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.27/7.08 % (2146057)CaDiCaL version: 2.1.3
% 44.27/7.08 % (2146057)Termination reason: Refutation not found, incomplete strategy
% 44.27/7.08 % (2146057)Time elapsed: 0.001 s
% 44.27/7.08 % (2146057)Peak memory usage: 87 MB
% 44.27/7.08 % (2146057)Instructions burned: 1 (million)
% 44.27/7.08 % (2146057)------------------------------
% 44.27/7.08 % (2146057)------------------------------
% 44.27/7.08 % (2146059)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=1498794610:i=598:bs=on:bd=preordered:av=off:ss=axioms_2972 on theBenchmark for (2972ds/598Mi)
% 44.27/7.08 % (2146022)Instruction limit reached!
% 44.27/7.08 % (2146022)------------------------------
% 44.27/7.08 % (2146022)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.27/7.08 % (2146022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.27/7.08 % (2146022)CaDiCaL version: 2.1.3
% 44.27/7.08 % (2146022)Termination reason: Instruction limit
% 44.27/7.08 % (2146022)Termination phase: Saturation
% 44.27/7.08 % (2146022)Time elapsed: 2.207 s
% 44.27/7.08 % (2146022)Peak memory usage: 140 MB
% 44.27/7.08 % (2146022)Instructions burned: 3395 (million)
% 44.27/7.08 % (2146053)Refutation not found, incomplete strategy
% 44.27/7.08 % (2146053)------------------------------
% 44.27/7.08 % (2146053)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.27/7.08 % (2146053)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.27/7.08 % (2146053)CaDiCaL version: 2.1.3
% 44.27/7.08 % (2146053)Termination reason: Refutation not found, incomplete strategy
% 44.27/7.08 % (2146053)Time elapsed: 0.596 s
% 44.27/7.08 % (2146053)Peak memory usage: 127 MB
% 44.27/7.08 % (2146053)Instructions burned: 859 (million)
% 44.27/7.08 % (2146059)Instruction limit reached!
% 44.27/7.08 % (2146059)------------------------------
% 44.27/7.08 % (2146059)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.81/7.94 % (2146059)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.81/7.94 % (2146059)CaDiCaL version: 2.1.3
% 48.81/7.94 % (2146059)Termination reason: Instruction limit
% 48.81/7.94 % (2146059)Termination phase: Saturation
% 48.81/7.94 % (2146059)Time elapsed: 0.151 s
% 48.81/7.94 % (2146059)Peak memory usage: 88 MB
% 48.81/7.94 % (2146059)Instructions burned: 598 (million)
% 48.81/7.94 % (2146061)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=2380828400:i=2989:sd=3:ss=axioms:sgt=60_2971 on theBenchmark for (2971ds/2989Mi)
% 48.81/7.94 % (2146062)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=3406873426:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2970 on theBenchmark for (2970ds/1997Mi)
% 48.81/7.94 % (2146053)------------------------------
% 48.81/7.94 % (2146053)------------------------------
% 48.81/7.94 % (2146065)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=3250521584:i=2088:bd=preordered:av=off_2968 on theBenchmark for (2968ds/2088Mi)
% 48.81/7.94 % (2146042)Instruction limit reached!
% 48.81/7.94 % (2146042)------------------------------
% 48.81/7.94 % (2146042)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.81/7.94 % (2146042)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.81/7.94 % (2146042)CaDiCaL version: 2.1.3
% 48.81/7.94 % (2146042)Termination reason: Instruction limit
% 48.81/7.94 % (2146042)Termination phase: Saturation
% 48.81/7.94 % (2146042)Time elapsed: 1.893 s
% 48.81/7.94 % (2146042)Peak memory usage: 132 MB
% 48.81/7.94 % (2146042)Instructions burned: 3258 (million)
% 48.81/7.94 % (2146067)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=2147271599:i=1098:nicw=on_2966 on theBenchmark for (2966ds/1098Mi)
% 48.81/7.94 % (2146062)Instruction limit reached!
% 48.81/7.94 % (2146062)------------------------------
% 48.81/7.94 % (2146062)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.81/7.94 % (2146062)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.81/7.94 % (2146062)CaDiCaL version: 2.1.3
% 48.81/7.94 % (2146062)Termination reason: Instruction limit
% 48.81/7.94 % (2146062)Termination phase: Saturation
% 48.81/7.94 % (2146062)Time elapsed: 0.746 s
% 48.81/7.94 % (2146062)Peak memory usage: 133 MB
% 48.81/7.94 % (2146062)Instructions burned: 1999 (million)
% 48.81/7.94 % (2146069)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=3922463292:i=433:bd=preordered_2961 on theBenchmark for (2961ds/433Mi)
% 48.81/7.94 % (2146067)Instruction limit reached!
% 48.81/7.94 % (2146067)------------------------------
% 48.81/7.94 % (2146067)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.81/7.94 % (2146067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.81/7.94 % (2146067)CaDiCaL version: 2.1.3
% 48.81/7.94 % (2146067)Termination reason: Instruction limit
% 48.81/7.94 % (2146067)Termination phase: Saturation
% 48.81/7.94 % (2146067)Time elapsed: 0.516 s
% 48.81/7.94 % (2146067)Peak memory usage: 89 MB
% 48.81/7.94 % (2146067)Instructions burned: 1099 (million)
% 48.81/7.94 % (2146069)Instruction limit reached!
% 48.81/7.94 % (2146069)------------------------------
% 48.81/7.94 % (2146069)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.81/7.94 % (2146069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.81/7.94 % (2146069)CaDiCaL version: 2.1.3
% 48.81/7.94 % (2146069)Termination reason: Instruction limit
% 48.81/7.94 % (2146069)Termination phase: Saturation
% 48.81/7.94 % (2146069)Time elapsed: 0.134 s
% 48.81/7.94 % (2146069)Peak memory usage: 89 MB
% 48.81/7.94 % (2146069)Instructions burned: 436 (million)
% 48.81/7.94 % (2146071)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=138066802:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2959 on theBenchmark for (2959ds/2942Mi)
% 48.81/7.94 % (2146072)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=4250845939:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2958 on theBenchmark for (2958ds/6922Mi)
% 48.81/7.94 % (2146065)Instruction limit reached!
% 48.81/7.94 % (2146065)------------------------------
% 48.81/7.94 % (2146065)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.81/7.94 % (2146065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.81/7.94 % (2146065)CaDiCaL version: 2.1.3
% 48.81/7.94 % (2146065)Termination reason: Instruction limit
% 48.81/7.94 % (2146065)Termination phase: Saturation
% 48.81/7.94 % (2146065)Time elapsed: 1.240 s
% 48.81/7.94 % (2146065)Peak memory usage: 130 MB
% 48.81/7.94 % (2146065)Instructions burned: 2089 (million)
% 48.81/7.94 % (2146072)Refutation not found, incomplete strategy
% 48.81/7.94 % (2146072)------------------------------
% 48.81/7.94 % (2146072)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.81/7.94 % (2146072)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.81/7.94 % (2146072)CaDiCaL version: 2.1.3
% 48.81/7.94 % (2146072)Termination reason: Refutation not found, incomplete strategy
% 48.81/7.94 % (2146072)Time elapsed: 0.340 s
% 48.81/7.94 % (2146072)Peak memory usage: 127 MB
% 48.81/7.94 % (2146072)Instructions burned: 862 (million)
% 48.81/7.94 % (2146075)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=732281629:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2954 on theBenchmark for (2954ds/596Mi)
% 48.81/7.94 % (2146075)Refutation not found, incomplete strategy
% 48.81/7.94 % (2146075)------------------------------
% 48.81/7.94 % (2146075)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.81/7.94 % (2146075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.81/7.94 % (2146075)CaDiCaL version: 2.1.3
% 48.81/7.94 % (2146075)Termination reason: Refutation not found, incomplete strategy
% 48.81/7.94 % (2146075)Time elapsed: 0.001 s
% 48.81/7.94 % (2146075)Peak memory usage: 88 MB
% 48.81/7.94 % (2146075)Instructions burned: 1 (million)
% 48.81/7.94 % (2146075)------------------------------
% 48.81/7.94 % (2146075)------------------------------
% 48.81/7.94 % (2146072)------------------------------
% 48.81/7.94 % (2146072)------------------------------
% 48.81/7.94 % (2146077)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=2421045621:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2951 on theBenchmark for (2951ds/4123Mi)
% 48.81/7.94 % (2146078)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=3630243207:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2951 on theBenchmark for (2951ds/16411Mi)
% 48.81/7.94 % (2146061)Instruction limit reached!
% 48.81/7.94 % (2146061)------------------------------
% 48.81/7.94 % (2146061)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.81/7.94 % (2146061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.81/7.94 % (2146061)CaDiCaL version: 2.1.3
% 48.81/7.94 % (2146061)Termination reason: Instruction limit
% 48.81/7.94 % (2146061)Termination phase: Saturation
% 48.81/7.94 % (2146061)Time elapsed: 2.061 s
% 48.81/7.94 % (2146061)Peak memory usage: 141 MB
% 48.81/7.94 % (2146061)Instructions burned: 2989 (million)
% 48.81/7.94 % (2146081)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=624891438:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2949 on theBenchmark for (2949ds/1670Mi)
% 48.81/7.94 % (2146071)Instruction limit reached!
% 48.81/7.94 % (2146071)------------------------------
% 48.81/7.94 % (2146071)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.81/7.94 % (2146071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.81/7.94 % (2146071)CaDiCaL version: 2.1.3
% 48.81/7.94 % (2146071)Termination reason: Instruction limit
% 48.81/7.94 % (2146071)Termination phase: Saturation
% 48.81/7.94 % (2146071)Time elapsed: 1.515 s
% 48.81/7.94 % (2146071)Peak memory usage: 132 MB
% 48.81/7.94 % (2146071)Instructions burned: 2942 (million)
% 48.81/7.94 % (2146083)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=3178604025:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2942 on theBenchmark for (2942ds/1722Mi)
% 48.81/7.94 % (2146081)Instruction limit reached!
% 48.81/7.94 % (2146081)------------------------------
% 48.81/7.94 % (2146081)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.81/7.94 % (2146081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.81/7.94 % (2146081)CaDiCaL version: 2.1.3
% 48.81/7.94 % (2146081)Termination reason: Instruction limit
% 48.81/7.94 % (2146081)Termination phase: Saturation
% 48.81/7.94 % (2146081)Time elapsed: 0.989 s
% 48.81/7.94 % (2146081)Peak memory usage: 132 MB
% 48.81/7.94 % (2146081)Instructions burned: 1672 (million)
% 48.81/7.94 % (2146077)Instruction limit reached!
% 48.81/7.94 % (2146077)------------------------------
% 48.81/7.94 % (2146077)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.81/7.94 % (2146077)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.81/7.94 % (2146077)CaDiCaL version: 2.1.3
% 48.81/7.94 % (2146077)Termination reason: Instruction limit
% 48.81/7.94 % (2146077)Termination phase: Saturation
% 48.81/7.94 % (2146077)Time elapsed: 1.299 s
% 48.81/7.94 % (2146077)Peak memory usage: 137 MB
% 48.81/7.94 % (2146077)Instructions burned: 4125 (million)
% 48.81/7.94 % (2146086)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=1061816045:st=2:i=4495:sd=10:ss=included_2937 on theBenchmark for (2937ds/4495Mi)
% 48.81/7.94 % (2146085)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=4048051634:cts=off:cond=on:i=9530:bs=on:fsd=on_2937 on theBenchmark for (2937ds/9530Mi)
% 48.81/7.94 % (2146078)First to succeed.
% 48.81/7.94 % (2146078)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2145992"
% 48.81/7.94 % SZS status Satisfiable for theBenchmark
% 48.81/7.94 % SZS output start Saturation.
% See solution above
% 0.14/8.14 % SZS output start Definitions and Model Updates.
% 0.14/8.14 % SZS output end Definitions and Model Updates.
% 0.14/8.14 % (2146078)------------------------------
% 0.14/8.14 % (2146078)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.14/8.14 % (2146078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.14/8.14 % (2146078)CaDiCaL version: 2.1.3
% 0.14/8.14 % (2146078)Termination reason: Satisfiable
% 0.14/8.14 % (2146078)Time elapsed: 1.793 s
% 0.14/8.14 % (2146078)Peak memory usage: 139 MB
% 0.14/8.14 % (2146078)Instructions burned: 2513 (million)
% 0.14/8.14 % (2146078)------------------------------
% 0.14/8.14 % (2146078)------------------------------
% 0.14/8.14 % (2145992)Success in time 7.107 s
% 0.14/8.14 % Vampire exiting
%------------------------------------------------------------------------------