%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP132-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 : n014.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 10:13:01 AM UTC 2026
% Result : Satisfiable 65.48s 10.14s
% Output : Saturation 66.31s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u53,axiom,
equalish(e_5,e_5) ).
cnf(u71,axiom,
~ product(e_5,e_1,e_4) ).
cnf(u76,axiom,
product(e_5,e_1,e_3) ).
cnf(u79,axiom,
~ product(e_5,e_1,e_2) ).
cnf(u83,axiom,
~ product(e_5,e_1,e_1) ).
cnf(u91,axiom,
~ product(e_4,e_1,e_4) ).
cnf(u95,axiom,
~ product(e_4,e_1,e_3) ).
cnf(u99,axiom,
~ product(e_4,e_1,e_2) ).
cnf(u103,axiom,
~ product(e_4,e_1,e_1) ).
cnf(u107,axiom,
( ~ group_element(X0)
| equalish(e_4,X0)
| product(X0,e_1,e_1)
| product(X0,e_1,e_4)
| product(X0,e_1,e_3)
| product(X0,e_1,e_2) ) ).
cnf(u111,axiom,
~ product(e_3,e_1,e_4) ).
cnf(u115,axiom,
~ product(e_3,e_1,e_3) ).
cnf(u120,axiom,
product(e_3,e_1,e_2) ).
cnf(u123,axiom,
~ product(e_3,e_1,e_1) ).
cnf(u132,axiom,
product(e_2,e_1,e_4) ).
cnf(u135,axiom,
~ product(e_2,e_1,e_3) ).
cnf(u139,axiom,
~ product(e_2,e_1,e_2) ).
cnf(u143,axiom,
~ product(e_2,e_1,e_1) ).
cnf(u151,axiom,
~ product(e_1,e_1,e_4) ).
cnf(u155,axiom,
~ product(e_1,e_1,e_3) ).
cnf(u159,axiom,
~ product(e_1,e_1,e_2) ).
cnf(u164,axiom,
product(e_1,e_1,e_1) ).
cnf(u327,axiom,
~ product(e_5,e_4,e_4) ).
cnf(u331,axiom,
~ product(e_5,e_4,e_3) ).
cnf(u335,axiom,
~ product(e_5,e_4,e_2) ).
cnf(u339,axiom,
~ product(e_5,e_4,e_1) ).
cnf(u343,axiom,
( ~ group_element(X0)
| equalish(e_5,X0)
| product(X0,e_4,e_1)
| product(X0,e_4,e_4)
| product(X0,e_4,e_3)
| product(X0,e_4,e_2) ) ).
cnf(u347,axiom,
~ product(e_4,e_4,e_4) ).
cnf(u351,axiom,
~ product(e_4,e_4,e_3) ).
cnf(u355,axiom,
~ product(e_4,e_4,e_2) ).
cnf(u360,axiom,
product(e_4,e_4,e_1) ).
cnf(u368,axiom,
product(e_3,e_4,e_4) ).
cnf(u371,axiom,
~ product(e_3,e_4,e_3) ).
cnf(u375,axiom,
~ product(e_3,e_4,e_2) ).
cnf(u379,axiom,
~ product(e_3,e_4,e_1) ).
cnf(u387,axiom,
~ product(e_2,e_4,e_4) ).
cnf(u392,axiom,
product(e_2,e_4,e_3) ).
cnf(u395,axiom,
~ product(e_2,e_4,e_2) ).
cnf(u399,axiom,
~ product(e_2,e_4,e_1) ).
cnf(u407,axiom,
~ product(e_1,e_4,e_4) ).
cnf(u411,axiom,
~ product(e_1,e_4,e_3) ).
cnf(u416,axiom,
product(e_1,e_4,e_2) ).
cnf(u419,axiom,
~ product(e_1,e_4,e_1) ).
cnf(u786,axiom,
product(e_5,e_3,e_4) ).
cnf(u789,axiom,
~ product(e_5,e_3,e_3) ).
cnf(u793,axiom,
~ product(e_5,e_3,e_2) ).
cnf(u797,axiom,
~ product(e_5,e_3,e_1) ).
cnf(u805,axiom,
~ product(e_4,e_3,e_4) ).
cnf(u810,axiom,
product(e_4,e_3,e_3) ).
cnf(u813,axiom,
~ product(e_4,e_3,e_2) ).
cnf(u817,axiom,
~ product(e_4,e_3,e_1) ).
cnf(u825,axiom,
~ product(e_3,e_3,e_4) ).
cnf(u829,axiom,
~ product(e_3,e_3,e_3) ).
cnf(u833,axiom,
~ product(e_3,e_3,e_2) ).
cnf(u838,axiom,
product(e_3,e_3,e_1) ).
cnf(u845,axiom,
~ product(e_2,e_3,e_4) ).
cnf(u849,axiom,
~ product(e_2,e_3,e_3) ).
cnf(u854,axiom,
product(e_2,e_3,e_2) ).
cnf(u857,axiom,
~ product(e_2,e_3,e_1) ).
cnf(u865,axiom,
~ product(e_1,e_3,e_4) ).
cnf(u869,axiom,
~ product(e_1,e_3,e_3) ).
cnf(u873,axiom,
~ product(e_1,e_3,e_2) ).
cnf(u877,axiom,
~ product(e_1,e_3,e_1) ).
cnf(u881,axiom,
( ~ group_element(X0)
| equalish(e_1,X0)
| product(X0,e_3,e_1)
| product(X0,e_3,e_4)
| product(X0,e_3,e_3)
| product(X0,e_3,e_2) ) ).
cnf(u1219,axiom,
~ product(e_5,e_2,e_4) ).
cnf(u1223,axiom,
~ product(e_5,e_2,e_3) ).
cnf(u1228,axiom,
product(e_5,e_2,e_2) ).
cnf(u1231,axiom,
~ product(e_5,e_2,e_1) ).
cnf(u1240,axiom,
product(e_4,e_2,e_4) ).
cnf(u1243,axiom,
~ product(e_4,e_2,e_3) ).
cnf(u1247,axiom,
~ product(e_4,e_2,e_2) ).
cnf(u1251,axiom,
~ product(e_4,e_2,e_1) ).
cnf(u1259,axiom,
~ product(e_3,e_2,e_4) ).
cnf(u1263,axiom,
~ product(e_3,e_2,e_3) ).
cnf(u1267,axiom,
~ product(e_3,e_2,e_2) ).
cnf(u1271,axiom,
~ product(e_3,e_2,e_1) ).
cnf(u1275,axiom,
( ~ group_element(X0)
| equalish(e_3,X0)
| product(X0,e_2,e_1)
| product(X0,e_2,e_4)
| product(X0,e_2,e_3)
| product(X0,e_2,e_2) ) ).
cnf(u1279,axiom,
~ product(e_2,e_2,e_4) ).
cnf(u1283,axiom,
~ product(e_2,e_2,e_3) ).
cnf(u1287,axiom,
~ product(e_2,e_2,e_2) ).
cnf(u1292,axiom,
product(e_2,e_2,e_1) ).
cnf(u1299,axiom,
~ product(e_1,e_2,e_4) ).
cnf(u1304,axiom,
product(e_1,e_2,e_3) ).
cnf(u1307,axiom,
~ product(e_1,e_2,e_2) ).
cnf(u1311,axiom,
~ product(e_1,e_2,e_1) ).
cnf(u1923,axiom,
~ product(e_5,e_5,e_4) ).
cnf(u1927,axiom,
~ product(e_5,e_5,e_3) ).
cnf(u1931,axiom,
~ product(e_5,e_5,e_2) ).
cnf(u1936,axiom,
product(e_5,e_5,e_1) ).
cnf(u1943,axiom,
~ product(e_4,e_5,e_4) ).
cnf(u1947,axiom,
~ product(e_4,e_5,e_3) ).
cnf(u1952,axiom,
product(e_4,e_5,e_2) ).
cnf(u1955,axiom,
~ product(e_4,e_5,e_1) ).
cnf(u1963,axiom,
~ product(e_3,e_5,e_4) ).
cnf(u1968,axiom,
product(e_3,e_5,e_3) ).
cnf(u1971,axiom,
~ product(e_3,e_5,e_2) ).
cnf(u1975,axiom,
~ product(e_3,e_5,e_1) ).
cnf(u1983,axiom,
~ product(e_2,e_5,e_4) ).
cnf(u1987,axiom,
~ product(e_2,e_5,e_3) ).
cnf(u1991,axiom,
~ product(e_2,e_5,e_2) ).
cnf(u1995,axiom,
~ product(e_2,e_5,e_1) ).
cnf(u1999,axiom,
( ~ group_element(X0)
| equalish(e_2,X0)
| product(X0,e_5,e_1)
| product(X0,e_5,e_4)
| product(X0,e_5,e_3)
| product(X0,e_5,e_2) ) ).
cnf(u2004,axiom,
product(e_1,e_5,e_4) ).
cnf(u2007,axiom,
~ product(e_1,e_5,e_3) ).
cnf(u2011,axiom,
~ product(e_1,e_5,e_2) ).
cnf(u2015,axiom,
~ product(e_1,e_5,e_1) ).
cnf(u6613,axiom,
equalish(e_4,e_4) ).
cnf(u27891,axiom,
( ~ product(e_2,X0,e_4)
| equalish(X0,e_1) ) ).
cnf(u33,axiom,
( ~ product(X0,X1,e_5)
| equalish(X1,X2)
| ~ group_element(X2)
| product(X0,X2,e_1)
| product(X0,X2,e_2)
| product(X0,X2,e_3)
| product(X0,X2,e_4)
| ~ group_element(X0) ) ).
cnf(u27417,negated_conjecture,
( ~ product(e_4,e_4,X0)
| ~ product(e_3,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X2,e_4) ) ).
cnf(u27789,axiom,
( ~ product(e_4,e_3,X0)
| equalish(X0,e_3) ) ).
cnf(u28027,negated_conjecture,
( ~ product(X0,X1,e_5)
| ~ product(e_4,X0,X1)
| equalish(X1,e_1) ) ).
cnf(u28001,negated_conjecture,
( ~ group_element(X0)
| equalish(X0,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(e_1,X0,X1) ) ).
cnf(u27991,negated_conjecture,
( ~ product(e_1,X0,X1)
| ~ product(X0,X1,e_1)
| equalish(X1,e_1) ) ).
cnf(u27723,negated_conjecture,
( ~ product(e_5,X0,X1)
| ~ product(X0,X1,e_4)
| equalish(X0,e_3) ) ).
cnf(u28207,negated_conjecture,
( ~ product(X0,e_5,e_1)
| equalish(X0,e_1)
| ~ group_element(X0)
| product(e_1,X0,e_2)
| product(e_1,X0,e_3)
| product(e_1,X0,e_4) ) ).
cnf(u38,negated_conjecture,
( ~ product(X1,X2,e_5)
| ~ product(X0,X1,X2)
| equalish(X2,e_5)
| ~ group_element(X3)
| product(X0,X3,e_1)
| product(X0,X3,e_2)
| product(X0,X3,e_3)
| product(X0,X3,e_4)
| ~ group_element(X0)
| product(X3,e_5,e_1)
| product(X3,e_5,e_2)
| product(X3,e_5,e_3)
| product(X3,e_5,e_4) ) ).
cnf(u27815,negated_conjecture,
( ~ product(X0,X1,e_5)
| ~ product(e_2,X0,X1)
| equalish(X1,e_2) ) ).
cnf(u27934,axiom,
( ~ product(e_1,e_4,X0)
| equalish(X0,e_2) ) ).
cnf(u28395,negated_conjecture,
( ~ product(X0,e_5,e_3)
| ~ group_element(X0)
| product(e_4,X0,e_1)
| product(e_4,X0,e_2)
| product(e_4,X0,e_3)
| product(e_4,X0,e_4) ) ).
cnf(u27476,axiom,
( ~ product(X0,e_5,e_3)
| equalish(X0,e_3) ) ).
cnf(u39,negated_conjecture,
( ~ product(X0,e_5,X1)
| ~ product(X2,X3,X4)
| ~ product(X3,X4,X1)
| equalish(X3,X0)
| ~ group_element(X0)
| product(X2,X0,e_1)
| product(X2,X0,e_2)
| product(X2,X0,e_3)
| product(X2,X0,e_4)
| ~ group_element(X2) ) ).
cnf(u27951,axiom,
( ~ product(X0,e_1,e_1)
| equalish(X0,e_1) ) ).
cnf(u5713,axiom,
( ~ group_element(X0)
| product(X1,e_1,e_1)
| product(X1,e_1,e_2)
| product(X1,e_1,e_3)
| product(X1,e_1,e_4)
| ~ group_element(X1)
| equalish(X0,e_1)
| product(X1,X0,e_1)
| product(X1,X0,e_2)
| product(X1,X0,e_3)
| product(X1,X0,e_4) ) ).
cnf(u27489,negated_conjecture,
( ~ product(e_1,e_3,X0)
| ~ product(e_5,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X1,e_1) ) ).
cnf(u28063,negated_conjecture,
( ~ product(X0,e_5,e_2)
| ~ group_element(X0)
| product(e_1,X0,e_1)
| product(e_1,X0,e_2)
| product(e_1,X0,e_3)
| product(e_1,X0,e_4) ) ).
cnf(u28139,negated_conjecture,
( ~ product(e_2,X0,X1)
| equalish(X1,e_5)
| ~ product(X0,X1,e_1) ) ).
cnf(u27670,negated_conjecture,
( ~ product(e_3,X0,X1)
| ~ product(X0,X1,e_4)
| equalish(X1,e_3) ) ).
cnf(u27477,axiom,
( ~ product(e_3,X0,e_3)
| equalish(X0,e_5) ) ).
cnf(u27707,negated_conjecture,
( ~ product(e_3,X0,X1)
| ~ product(X0,X1,e_3)
| equalish(X0,e_1) ) ).
cnf(product_total_function1,axiom,
( product(X0,X1,e_5)
| ~ group_element(X1)
| product(X0,X1,e_1)
| product(X0,X1,e_2)
| product(X0,X1,e_3)
| product(X0,X1,e_4)
| ~ group_element(X0) ) ).
cnf(u27491,axiom,
( ~ product(X0,e_1,e_3)
| equalish(X0,e_5) ) ).
cnf(u28424,negated_conjecture,
( ~ product(e_5,e_5,X0)
| ~ group_element(X0)
| product(e_5,X0,e_1)
| product(e_5,X0,e_2)
| product(e_5,X0,e_3)
| equalish(X0,e_3) ) ).
cnf(product_total_function2,axiom,
( ~ product(X0,X1,X3)
| ~ product(X0,X1,X2)
| equalish(X2,X3) ) ).
cnf(u27456,negated_conjecture,
( ~ product(e_3,e_1,X0)
| ~ product(e_3,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X2,e_1) ) ).
cnf(e_5_is_not_e_3,axiom,
~ equalish(e_5,e_3) ).
cnf(u28374,negated_conjecture,
( ~ product(X0,e_5,e_3)
| ~ group_element(X0)
| product(e_2,X0,e_1)
| product(e_2,X0,e_2)
| product(e_2,X0,e_3)
| product(e_2,X0,e_4) ) ).
cnf(u27050,axiom,
( ~ product(X0,e_2,e_3)
| equalish(X0,e_1) ) ).
cnf(u28029,negated_conjecture,
( ~ product(e_2,X0,X1)
| ~ product(X0,X1,e_4)
| equalish(X1,e_1) ) ).
cnf(e_5_is_not_e_4,axiom,
~ equalish(e_5,e_4) ).
cnf(u27761,negated_conjecture,
( ~ product(e_4,e_3,X0)
| ~ product(e_2,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X1,e_4) ) ).
cnf(u5755,axiom,
( ~ group_element(X0)
| product(X0,e_5,e_2)
| product(X0,e_5,e_3)
| product(X0,e_5,e_4)
| product(X0,e_5,e_1)
| product(X0,e_4,e_1)
| product(X0,e_4,e_2)
| product(X0,e_4,e_3)
| product(X0,e_4,e_4) ) ).
cnf(qg2_1,negated_conjecture,
( ~ product(X5,X3,X4)
| ~ product(X3,X4,X2)
| ~ product(X5,X0,X1)
| ~ product(X0,X1,X2)
| equalish(X0,X3) ) ).
cnf(u27510,negated_conjecture,
( ~ product(e_5,e_1,X0)
| ~ product(e_5,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X2,e_1) ) ).
cnf(u27899,negated_conjecture,
( ~ product(e_5,X0,X1)
| ~ product(X0,X1,e_1)
| equalish(X0,e_2) ) ).
cnf(u28039,negated_conjecture,
( ~ product(e_2,X0,X1)
| ~ product(X0,X1,e_4)
| equalish(X0,e_2) ) ).
cnf(qg2_2,negated_conjecture,
( ~ product(X5,X3,X4)
| ~ product(X3,X4,X2)
| ~ product(X5,X0,X1)
| ~ product(X0,X1,X2)
| equalish(X1,X4) ) ).
cnf(u28255,negated_conjecture,
( ~ product(X0,e_5,e_4)
| ~ group_element(X0)
| product(e_1,X0,e_1)
| product(e_1,X0,e_2)
| product(e_1,X0,e_3)
| product(e_1,X0,e_4) ) ).
cnf(u27455,negated_conjecture,
( ~ product(e_3,e_1,X0)
| ~ product(e_3,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X1,e_3) ) ).
cnf(u27774,axiom,
( ~ product(e_2,e_3,X0)
| equalish(X0,e_2) ) ).
cnf(product_right_cancellation,axiom,
( ~ product(X0,X3,X2)
| ~ product(X0,X1,X2)
| equalish(X1,X3) ) ).
cnf(u28482,negated_conjecture,
( ~ product(e_5,e_3,X0)
| product(e_3,X0,e_1)
| product(e_3,X0,e_2)
| product(e_3,X0,e_3)
| product(e_3,X0,e_4)
| ~ group_element(X0) ) ).
cnf(u5780,axiom,
( ~ group_element(X0)
| product(X0,e_2,e_2)
| product(X0,e_2,e_3)
| product(X0,e_2,e_4)
| product(X0,e_2,e_1)
| product(X0,e_4,e_1)
| product(X0,e_4,e_2)
| product(X0,e_4,e_3)
| product(X0,e_4,e_4) ) ).
cnf(u5585,axiom,
equalish(e_2,e_2) ).
cnf(u28111,negated_conjecture,
( ~ product(e_4,X0,X1)
| equalish(X1,e_5)
| ~ product(X0,X1,e_4) ) ).
cnf(product_left_cancellation,axiom,
( ~ product(X3,X1,X2)
| ~ product(X0,X1,X2)
| equalish(X0,X3) ) ).
cnf(e_4_is_not_e_1,axiom,
~ equalish(e_4,e_1) ).
cnf(u28195,negated_conjecture,
( ~ product(e_1,X0,X1)
| equalish(X0,e_3)
| ~ product(X0,X1,e_3) ) ).
cnf(u28464,negated_conjecture,
( ~ product(e_4,e_3,X0)
| ~ group_element(X0)
| product(e_3,X0,e_1)
| product(e_3,X0,e_3)
| product(e_3,X0,e_4)
| equalish(X0,e_1) ) ).
cnf(u27052,axiom,
( ~ product(e_1,e_2,X0)
| equalish(X0,e_3) ) ).
cnf(u5715,axiom,
( ~ group_element(X0)
| product(X1,e_3,e_1)
| product(X1,e_3,e_2)
| product(X1,e_3,e_3)
| product(X1,e_3,e_4)
| ~ group_element(X1)
| equalish(X0,e_3)
| product(X1,X0,e_1)
| product(X1,X0,e_2)
| product(X1,X0,e_3)
| product(X1,X0,e_4) ) ).
cnf(u28181,negated_conjecture,
( ~ product(e_4,X0,X1)
| equalish(X0,e_1)
| ~ product(X0,X1,e_4) ) ).
cnf(u27913,negated_conjecture,
( ~ product(e_4,e_1,X0)
| ~ product(e_4,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X2,e_1) ) ).
cnf(u27904,axiom,
( ~ product(X0,e_2,e_1)
| equalish(X0,e_2) ) ).
cnf(e_4_is_not_e_2,axiom,
~ equalish(e_4,e_2) ).
cnf(u27419,axiom,
( ~ product(e_3,X0,e_4)
| equalish(X0,e_4) ) ).
cnf(u27696,negated_conjecture,
( ~ group_element(X0)
| equalish(X0,e_1)
| ~ group_element(X1)
| product(X0,X1,e_1)
| product(X0,X1,e_2)
| product(X0,X1,e_3)
| product(X0,X1,e_4)
| ~ product(e_5,X0,X1) ) ).
cnf(u28332,negated_conjecture,
( ~ product(X0,e_5,e_4)
| ~ group_element(X0)
| product(e_2,X0,e_1)
| product(e_2,X0,e_2)
| product(e_2,X0,e_3)
| product(e_2,X0,e_4) ) ).
cnf(u27890,axiom,
( ~ product(X0,e_1,e_4)
| equalish(X0,e_2) ) ).
cnf(u28463,negated_conjecture,
( ~ product(e_4,e_5,X0)
| ~ group_element(X0)
| product(e_5,X0,e_1)
| product(e_5,X0,e_2)
| product(e_5,X0,e_4)
| equalish(X0,e_1) ) ).
cnf(u27900,negated_conjecture,
( ~ product(e_5,X0,X1)
| ~ product(X0,X1,e_1)
| equalish(X1,e_2) ) ).
cnf(e_3_is_not_e_4,axiom,
~ equalish(e_3,e_4) ).
cnf(u28483,negated_conjecture,
( ~ product(e_5,e_2,X0)
| product(e_2,X0,e_1)
| product(e_2,X0,e_2)
| product(e_2,X0,e_3)
| product(e_2,X0,e_4)
| ~ group_element(X0) ) ).
cnf(u28231,negated_conjecture,
( ~ product(X0,e_5,e_2)
| equalish(X0,e_5)
| ~ group_element(X0)
| product(e_4,X0,e_1)
| product(e_4,X0,e_3)
| product(e_4,X0,e_4) ) ).
cnf(u27687,negated_conjecture,
( ~ product(e_3,X0,X1)
| ~ product(X0,X1,e_2)
| equalish(X1,e_1) ) ).
cnf(e_3_is_not_e_5,axiom,
~ equalish(e_3,e_5) ).
cnf(e_5_is_not_e_1,axiom,
~ equalish(e_5,e_1) ).
cnf(u27914,axiom,
( ~ product(X0,e_4,e_1)
| equalish(X0,e_4) ) ).
cnf(e_5_is_not_e_2,axiom,
~ equalish(e_5,e_2) ).
cnf(u27641,negated_conjecture,
( ~ product(e_5,X0,X1)
| ~ product(X0,X1,e_3)
| equalish(X1,e_1) ) ).
cnf(u28382,negated_conjecture,
( ~ product(X0,e_5,e_2)
| ~ group_element(X0)
| product(e_2,X0,e_1)
| product(e_2,X0,e_2)
| product(e_2,X0,e_3)
| product(e_2,X0,e_4) ) ).
cnf(u5716,axiom,
( ~ group_element(X0)
| product(X1,e_4,e_1)
| product(X1,e_4,e_2)
| product(X1,e_4,e_3)
| product(X1,e_4,e_4)
| ~ group_element(X1)
| equalish(X0,e_4)
| product(X1,X0,e_1)
| product(X1,X0,e_2)
| product(X1,X0,e_3)
| product(X1,X0,e_4) ) ).
cnf(u27420,axiom,
( ~ product(e_3,e_4,X0)
| equalish(X0,e_4) ) ).
cnf(u27474,negated_conjecture,
( ~ product(e_5,e_3,X0)
| ~ product(e_3,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X1,e_5) ) ).
cnf(u27822,negated_conjecture,
( ~ product(e_4,X0,X1)
| ~ product(X0,X1,e_1)
| equalish(X0,e_3) ) ).
cnf(e_4_is_not_e_3,axiom,
~ equalish(e_4,e_3) ).
cnf(u27764,axiom,
( ~ product(e_2,X0,e_3)
| equalish(X0,e_4) ) ).
cnf(u28308,negated_conjecture,
( ~ product(X0,e_5,e_4)
| ~ group_element(X0)
| product(e_5,X0,e_1)
| product(e_5,X0,e_2)
| product(e_5,X0,e_3)
| product(e_5,X0,e_4) ) ).
cnf(u28047,negated_conjecture,
( ~ product(X0,X1,e_5)
| ~ product(e_4,X0,X1)
| equalish(X0,e_4) ) ).
cnf(e_4_is_not_e_5,axiom,
~ equalish(e_4,e_5) ).
cnf(u28480,negated_conjecture,
( ~ product(e_5,e_5,X0)
| product(e_5,X0,e_1)
| product(e_5,X0,e_2)
| product(e_5,X0,e_3)
| product(e_5,X0,e_4)
| ~ group_element(X0) ) ).
cnf(u27941,negated_conjecture,
( ~ product(e_5,e_4,X0)
| ~ product(e_1,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X2,e_4) ) ).
cnf(u27932,axiom,
( ~ product(X0,e_4,e_2)
| equalish(X0,e_1) ) ).
cnf(u27765,axiom,
( ~ product(e_2,e_4,X0)
| equalish(X0,e_3) ) ).
cnf(u27927,negated_conjecture,
( ~ group_element(X0)
| ~ product(X1,X2,e_2)
| equalish(X1,e_4)
| product(X0,e_4,e_1)
| product(X0,e_4,e_2)
| product(X0,e_4,e_3)
| product(X0,e_4,e_4)
| ~ product(X0,X1,X2) ) ).
cnf(u28008,negated_conjecture,
( ~ product(X0,X1,e_5)
| ~ product(e_1,X0,X1)
| equalish(X1,e_4) ) ).
cnf(e_2_is_not_e_1,axiom,
~ equalish(e_2,e_1) ).
cnf(u27894,negated_conjecture,
( ~ product(e_2,e_4,X0)
| ~ product(e_4,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X1,e_2) ) ).
cnf(u27475,negated_conjecture,
( ~ product(e_5,e_3,X0)
| ~ product(e_3,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X2,e_3) ) ).
cnf(u28358,negated_conjecture,
( ~ product(X0,e_5,e_1)
| ~ group_element(X0)
| product(e_4,X0,e_1)
| product(e_4,X0,e_2)
| product(e_4,X0,e_3)
| product(e_4,X0,e_4) ) ).
cnf(e_2_is_not_e_3,axiom,
~ equalish(e_2,e_3) ).
cnf(u27785,negated_conjecture,
( ~ product(e_3,e_3,X0)
| ~ product(e_4,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X1,e_3) ) ).
cnf(e_1_is_not_e_4,axiom,
~ equalish(e_1,e_4) ).
cnf(u27408,negated_conjecture,
( ~ product(X0,e_3,e_2)
| product(X0,e_2,e_2)
| product(X0,e_2,e_3)
| product(X0,e_2,e_4)
| ~ group_element(X0)
| product(X0,e_2,e_1) ) ).
cnf(u27945,negated_conjecture,
( ~ group_element(X0)
| ~ product(X1,X2,e_4)
| equalish(X2,e_5)
| product(X0,e_1,e_1)
| product(X0,e_1,e_2)
| product(X0,e_1,e_3)
| product(X0,e_1,e_4)
| ~ product(X0,X1,X2) ) ).
cnf(u28167,negated_conjecture,
( ~ product(e_5,X0,X1)
| equalish(X0,e_4)
| ~ product(X0,X1,e_2) ) ).
cnf(u27921,negated_conjecture,
( ~ product(e_5,e_2,X0)
| ~ product(e_4,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X1,e_5) ) ).
cnf(e_1_is_not_e_5,axiom,
~ equalish(e_1,e_5) ).
cnf(u27771,negated_conjecture,
( ~ product(e_3,e_2,X0)
| ~ product(e_2,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X2,e_2) ) ).
cnf(u28033,negated_conjecture,
( ~ product(e_2,X0,X1)
| ~ product(X0,X1,e_2)
| equalish(X0,e_1) ) ).
cnf(u28125,negated_conjecture,
( ~ product(e_1,X0,X1)
| equalish(X1,e_5)
| ~ product(X0,X1,e_3) ) ).
cnf(e_3_is_not_e_1,axiom,
~ equalish(e_3,e_1) ).
cnf(u28239,negated_conjecture,
( ~ product(X0,e_5,e_4)
| equalish(X0,e_5)
| ~ group_element(X0)
| product(e_3,X0,e_1)
| product(e_3,X0,e_2)
| product(e_3,X0,e_4) ) ).
cnf(u27479,negated_conjecture,
( ~ group_element(X0)
| ~ product(X1,X2,e_3)
| equalish(X2,e_5)
| product(X0,e_3,e_1)
| product(X0,e_3,e_2)
| product(X0,e_3,e_3)
| product(X0,e_3,e_4)
| ~ product(X0,X1,X2) ) ).
cnf(u28446,negated_conjecture,
( ~ product(e_2,e_2,X0)
| ~ group_element(X0)
| product(e_2,X0,e_2)
| product(e_2,X0,e_3)
| product(e_2,X0,e_4)
| equalish(X0,e_2) ) ).
cnf(e_3_is_not_e_2,axiom,
~ equalish(e_3,e_2) ).
cnf(u28350,negated_conjecture,
( ~ product(X0,e_5,e_1)
| equalish(X0,e_3)
| ~ group_element(X0)
| product(e_4,X0,e_1)
| product(e_4,X0,e_2)
| product(e_4,X0,e_4) ) ).
cnf(e_2_is_not_e_4,axiom,
~ equalish(e_2,e_4) ).
cnf(u27926,negated_conjecture,
( ~ group_element(X0)
| ~ product(X1,X2,e_2)
| equalish(X2,e_5)
| product(X0,e_4,e_1)
| product(X0,e_4,e_2)
| product(X0,e_4,e_3)
| product(X0,e_4,e_4)
| ~ product(X0,X1,X2) ) ).
cnf(u27908,negated_conjecture,
( ~ product(e_3,X0,X1)
| ~ product(X0,X1,e_1)
| equalish(X0,e_4) ) ).
cnf(u12877,negated_conjecture,
( ~ group_element(X1)
| product(X0,e_2,e_1)
| product(X0,e_2,e_2)
| product(X0,e_2,e_3)
| product(X0,e_2,e_4)
| ~ group_element(X0)
| ~ product(X0,e_2,X1)
| product(e_2,X1,e_1)
| product(e_2,X1,e_2)
| product(e_2,X1,e_3)
| product(e_2,X1,e_4)
| equalish(X1,e_5) ) ).
cnf(u27944,axiom,
( ~ product(e_1,e_5,X0)
| equalish(X0,e_4) ) ).
cnf(u28518,negated_conjecture,
( ~ product(e_4,e_5,X0)
| product(e_5,X0,e_1)
| product(e_5,X0,e_2)
| product(e_5,X0,e_3)
| product(e_5,X0,e_4)
| ~ group_element(X0) ) ).
cnf(u12891,negated_conjecture,
( ~ group_element(X1)
| product(X0,e_2,e_1)
| product(X0,e_2,e_2)
| product(X0,e_2,e_3)
| product(X0,e_2,e_4)
| ~ group_element(X0)
| ~ product(X0,e_4,X1)
| product(e_4,X1,e_1)
| product(e_4,X1,e_2)
| product(e_4,X1,e_3)
| product(e_4,X1,e_4) ) ).
cnf(e_2_is_not_e_5,axiom,
~ equalish(e_2,e_5) ).
cnf(u5757,axiom,
( ~ group_element(X0)
| product(X0,e_5,e_2)
| product(X0,e_5,e_3)
| product(X0,e_5,e_4)
| product(X0,e_5,e_1)
| product(X0,e_2,e_1)
| product(X0,e_2,e_2)
| product(X0,e_2,e_3)
| product(X0,e_2,e_4) ) ).
cnf(u27512,axiom,
( ~ product(e_5,X0,e_1)
| equalish(X0,e_5) ) ).
cnf(u28079,negated_conjecture,
( ~ product(X0,e_5,e_1)
| equalish(X0,e_4)
| ~ group_element(X0)
| product(e_3,X0,e_1)
| product(e_3,X0,e_2)
| product(e_3,X0,e_3) ) ).
cnf(element_2,axiom,
group_element(e_2) ).
cnf(u28426,negated_conjecture,
( ~ product(e_5,e_3,X0)
| ~ group_element(X0)
| product(e_3,X0,e_2)
| product(e_3,X0,e_3)
| product(e_3,X0,e_4)
| equalish(X0,e_3) ) ).
cnf(u27490,negated_conjecture,
( ~ product(e_1,e_3,X0)
| ~ product(e_5,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X2,e_3) ) ).
cnf(u27772,axiom,
( ~ product(X0,e_3,e_2)
| equalish(X0,e_2) ) ).
cnf(u307,axiom,
equalish(e_1,e_1) ).
cnf(element_3,axiom,
group_element(e_3) ).
cnf(u28405,negated_conjecture,
( ~ product(e_1,e_1,X0)
| product(e_1,X0,e_1)
| product(e_1,X0,e_2)
| product(e_1,X0,e_3)
| product(e_1,X0,e_4)
| ~ group_element(X0) ) ).
cnf(u27949,negated_conjecture,
( ~ product(e_1,e_1,X0)
| ~ product(e_1,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X1,e_1) ) ).
cnf(u27450,negated_conjecture,
( ~ product(e_2,e_2,X0)
| ~ product(e_5,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X2,e_2) ) ).
cnf(u27912,negated_conjecture,
( ~ product(e_4,e_1,X0)
| ~ product(e_4,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X1,e_4) ) ).
cnf(u27773,axiom,
( ~ product(e_2,X0,e_2)
| equalish(X0,e_3) ) ).
cnf(u27483,negated_conjecture,
( ~ product(e_1,e_2,X0)
| ~ product(e_3,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X2,e_2) ) ).
cnf(u28519,negated_conjecture,
( ~ product(e_4,e_3,X0)
| product(e_3,X0,e_1)
| product(e_3,X0,e_2)
| product(e_3,X0,e_3)
| product(e_3,X0,e_4)
| ~ group_element(X0) ) ).
cnf(u27923,axiom,
( ~ product(X0,e_5,e_2)
| equalish(X0,e_4) ) ).
cnf(element_1,axiom,
group_element(e_1) ).
cnf(u28035,negated_conjecture,
( ~ product(e_1,X0,X1)
| ~ product(X0,X1,e_4)
| equalish(X0,e_4) ) ).
cnf(u28019,negated_conjecture,
( ~ product(e_2,X0,X1)
| ~ product(X0,X1,e_2)
| equalish(X1,e_4) ) ).
cnf(u12920,negated_conjecture,
( ~ product(X0,e_4,e_1)
| product(X0,e_2,e_2)
| product(X0,e_2,e_3)
| product(X0,e_2,e_4)
| ~ group_element(X0)
| product(X0,e_2,e_1) ) ).
cnf(u27051,axiom,
( ~ product(e_1,X0,e_3)
| equalish(X0,e_2) ) ).
cnf(u12892,negated_conjecture,
( ~ group_element(X1)
| product(X0,e_2,e_1)
| product(X0,e_2,e_2)
| product(X0,e_2,e_3)
| product(X0,e_2,e_4)
| ~ group_element(X0)
| ~ product(X0,e_3,X1)
| product(e_3,X1,e_1)
| product(e_3,X1,e_2)
| product(e_3,X1,e_3)
| product(e_3,X1,e_4) ) ).
cnf(u28427,negated_conjecture,
( ~ product(e_5,e_2,X0)
| ~ group_element(X0)
| product(e_2,X0,e_1)
| product(e_2,X0,e_3)
| product(e_2,X0,e_4)
| equalish(X0,e_3) ) ).
cnf(u27513,axiom,
( ~ product(e_5,e_5,X0)
| equalish(X0,e_1) ) ).
cnf(e_1_is_not_e_2,axiom,
~ equalish(e_1,e_2) ).
cnf(u28087,negated_conjecture,
( ~ product(X0,e_5,e_1)
| ~ group_element(X0)
| product(e_3,X0,e_1)
| product(e_3,X0,e_2)
| product(e_3,X0,e_3)
| product(e_3,X0,e_4) ) ).
cnf(u5717,axiom,
( ~ group_element(X0)
| product(X1,e_5,e_1)
| product(X1,e_5,e_2)
| product(X1,e_5,e_3)
| product(X1,e_5,e_4)
| ~ group_element(X1)
| equalish(X0,e_5)
| product(X1,X0,e_1)
| product(X1,X0,e_2)
| product(X1,X0,e_3)
| product(X1,X0,e_4) ) ).
cnf(u28520,negated_conjecture,
( ~ product(e_4,e_2,X0)
| product(e_2,X0,e_1)
| product(e_2,X0,e_2)
| product(e_2,X0,e_3)
| product(e_2,X0,e_4)
| ~ group_element(X0) ) ).
cnf(u27452,axiom,
( ~ product(e_5,X0,e_2)
| equalish(X0,e_2) ) ).
cnf(e_1_is_not_e_3,axiom,
~ equalish(e_1,e_3) ).
cnf(u28276,negated_conjecture,
( ~ product(X0,e_5,e_2)
| equalish(X0,e_1)
| ~ group_element(X0)
| product(e_2,X0,e_1)
| product(e_2,X0,e_2)
| product(e_2,X0,e_3) ) ).
cnf(u27407,negated_conjecture,
( ~ product(X0,e_5,e_4)
| product(X0,e_2,e_2)
| product(X0,e_2,e_3)
| product(X0,e_2,e_4)
| ~ group_element(X0)
| product(X0,e_2,e_1) ) ).
cnf(u27457,axiom,
( ~ product(X0,e_3,e_1)
| equalish(X0,e_3) ) ).
cnf(element_4,axiom,
group_element(e_4) ).
cnf(u28015,negated_conjecture,
( ~ product(e_4,X0,X1)
| ~ product(X0,X1,e_2)
| equalish(X1,e_2) ) ).
cnf(u27480,negated_conjecture,
( ~ group_element(X0)
| ~ product(X1,X2,e_3)
| equalish(X1,e_3)
| product(X0,e_3,e_1)
| product(X0,e_3,e_2)
| product(X0,e_3,e_3)
| product(X0,e_3,e_4)
| ~ product(X0,X1,X2) ) ).
cnf(u27767,negated_conjecture,
( ~ product(e_1,X0,X1)
| ~ product(X0,X1,e_2)
| equalish(X1,e_3) ) ).
cnf(u27766,negated_conjecture,
( ~ product(e_1,X0,X1)
| ~ product(X0,X1,e_2)
| equalish(X0,e_2) ) ).
cnf(element_5,axiom,
group_element(e_5) ).
cnf(u27656,negated_conjecture,
( ~ product(e_3,X0,X1)
| ~ product(X0,X1,e_3)
| equalish(X1,e_2) ) ).
cnf(u309,axiom,
equalish(e_3,e_3) ).
cnf(u28292,negated_conjecture,
( ~ product(X0,e_5,e_2)
| ~ group_element(X0)
| product(e_3,X0,e_1)
| product(e_3,X0,e_2)
| product(e_3,X0,e_3)
| product(e_3,X0,e_4) ) ).
cnf(u27453,axiom,
( ~ product(e_5,e_2,X0)
| equalish(X0,e_2) ) ).
cnf(u28010,negated_conjecture,
( ~ product(e_1,X0,X1)
| ~ product(X0,X1,e_4)
| equalish(X1,e_2) ) ).
cnf(u27952,axiom,
( ~ product(e_1,X0,e_1)
| equalish(X0,e_1) ) ).
cnf(u27925,axiom,
( ~ product(e_4,e_5,X0)
| equalish(X0,e_2) ) ).
cnf(u27916,axiom,
( ~ product(e_4,e_4,X0)
| equalish(X0,e_1) ) ).
cnf(u27896,axiom,
( ~ product(X0,e_2,e_4)
| equalish(X0,e_4) ) ).
cnf(u27459,axiom,
( ~ product(e_3,e_3,X0)
| equalish(X0,e_1) ) ).
cnf(u28444,negated_conjecture,
( ~ product(e_2,e_5,X0)
| ~ group_element(X0)
| product(e_5,X0,e_1)
| product(e_5,X0,e_3)
| product(e_5,X0,e_4)
| equalish(X0,e_2) ) ).
cnf(u27683,negated_conjecture,
( ~ product(e_5,X0,X1)
| ~ product(X0,X1,e_4)
| equalish(X1,e_4) ) ).
cnf(u27786,negated_conjecture,
( ~ product(e_3,e_3,X0)
| ~ product(e_4,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X2,e_3) ) ).
cnf(u28012,negated_conjecture,
( ~ product(e_1,X0,X1)
| ~ product(X0,X1,e_1)
| equalish(X0,e_1) ) ).
cnf(u27820,negated_conjecture,
( ~ product(e_2,X0,X1)
| ~ product(X0,X1,e_3)
| equalish(X1,e_3) ) ).
cnf(u28425,negated_conjecture,
( ~ product(e_5,e_4,X0)
| ~ group_element(X0)
| product(e_4,X0,e_1)
| product(e_4,X0,e_2)
| product(e_4,X0,e_4)
| equalish(X0,e_3) ) ).
cnf(u27905,axiom,
( ~ product(e_2,X0,e_1)
| equalish(X0,e_2) ) ).
cnf(u27897,axiom,
( ~ product(e_4,X0,e_4)
| equalish(X0,e_2) ) ).
cnf(u27449,negated_conjecture,
( ~ product(e_2,e_2,X0)
| ~ product(e_5,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X1,e_2) ) ).
cnf(u12890,negated_conjecture,
( ~ group_element(X1)
| product(X0,e_2,e_1)
| product(X0,e_2,e_2)
| product(X0,e_2,e_3)
| product(X0,e_2,e_4)
| ~ group_element(X0)
| ~ product(X0,e_5,X1)
| product(e_5,X1,e_1)
| product(e_5,X1,e_2)
| product(e_5,X1,e_3)
| product(e_5,X1,e_4) ) ).
cnf(u12505,negated_conjecture,
( ~ group_element(X0)
| ~ product(X1,X0,X2)
| product(X1,e_2,e_1)
| product(X1,e_2,e_2)
| product(X1,e_2,e_3)
| product(X1,e_2,e_4)
| ~ group_element(X1)
| ~ group_element(X2)
| product(X0,X2,e_1)
| product(X0,X2,e_2)
| product(X0,X2,e_3)
| product(X0,X2,e_4)
| equalish(X0,e_2) ) ).
cnf(u27486,axiom,
( ~ product(e_3,e_1,X0)
| equalish(X0,e_2) ) ).
cnf(u27770,negated_conjecture,
( ~ product(e_3,e_2,X0)
| ~ product(e_2,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X1,e_3) ) ).
cnf(u27729,negated_conjecture,
( ~ product(e_3,X0,X1)
| ~ product(X0,X1,e_2)
| equalish(X0,e_3) ) ).
cnf(u27931,negated_conjecture,
( ~ product(e_4,e_2,X0)
| ~ product(e_1,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X2,e_2) ) ).
cnf(u27446,axiom,
( ~ product(e_5,X0,e_4)
| equalish(X0,e_3) ) ).
cnf(u27478,axiom,
( ~ product(e_3,e_5,X0)
| equalish(X0,e_3) ) ).
cnf(u28466,negated_conjecture,
( ~ product(e_4,e_1,X0)
| ~ group_element(X0)
| product(e_1,X0,e_2)
| product(e_1,X0,e_3)
| product(e_1,X0,e_4)
| equalish(X0,e_1) ) ).
cnf(u28324,negated_conjecture,
( ~ product(X0,e_5,e_3)
| equalish(X0,e_2)
| ~ group_element(X0)
| product(e_4,X0,e_1)
| product(e_4,X0,e_2)
| product(e_4,X0,e_3) ) ).
cnf(u27650,negated_conjecture,
( ~ group_element(X0)
| equalish(X1,e_3)
| ~ group_element(X1)
| product(X0,X1,e_1)
| product(X0,X1,e_2)
| product(X0,X1,e_3)
| product(X0,X1,e_4)
| ~ product(e_5,X0,X1) ) ).
cnf(u27946,negated_conjecture,
( ~ group_element(X0)
| ~ product(X1,X2,e_4)
| equalish(X1,e_1)
| product(X0,e_1,e_1)
| product(X0,e_1,e_2)
| product(X0,e_1,e_3)
| product(X0,e_1,e_4)
| ~ product(X0,X1,X2) ) ).
cnf(u28284,negated_conjecture,
( ~ product(X0,e_5,e_3)
| equalish(X0,e_1)
| ~ group_element(X0)
| product(e_3,X0,e_1)
| product(e_3,X0,e_3)
| product(e_3,X0,e_4) ) ).
cnf(u27509,negated_conjecture,
( ~ product(e_5,e_1,X0)
| ~ product(e_5,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X1,e_5) ) ).
cnf(u58,negated_conjecture,
( ~ group_element(X3)
| equalish(X1,X3)
| ~ product(X0,X1,X2)
| product(X0,X3,e_1)
| product(X0,X3,e_2)
| product(X0,X3,e_3)
| product(X0,X3,e_4)
| ~ group_element(X0)
| product(X3,e_5,e_1)
| product(X3,e_5,e_2)
| product(X3,e_5,e_3)
| product(X3,e_5,e_4)
| ~ group_element(X2)
| product(X1,X2,e_1)
| product(X1,X2,e_2)
| product(X1,X2,e_3)
| product(X1,X2,e_4)
| ~ group_element(X1) ) ).
cnf(u28502,negated_conjecture,
( ~ product(e_2,e_2,X0)
| product(e_2,X0,e_1)
| product(e_2,X0,e_2)
| product(e_2,X0,e_3)
| product(e_2,X0,e_4)
| ~ group_element(X0) ) ).
cnf(u27832,negated_conjecture,
( ~ group_element(X0)
| equalish(X0,e_3)
| ~ group_element(X1)
| product(X0,X1,e_1)
| product(X0,X1,e_2)
| product(X0,X1,e_3)
| product(X0,X1,e_4)
| ~ product(e_2,X0,X1) ) ).
cnf(u59,axiom,
( ~ group_element(X0)
| product(X1,e_1,e_1)
| product(X1,e_1,e_2)
| product(X1,e_1,e_3)
| product(X1,e_1,e_4)
| ~ group_element(X1)
| product(X0,e_1,e_1)
| product(X0,e_1,e_2)
| product(X0,e_1,e_3)
| product(X0,e_1,e_4)
| equalish(X0,X1) ) ).
cnf(u28009,negated_conjecture,
( ~ group_element(X0)
| equalish(X1,e_4)
| ~ group_element(X1)
| product(X0,X1,e_1)
| product(X0,X1,e_2)
| product(X0,X1,e_3)
| product(X0,X1,e_4)
| ~ product(e_1,X0,X1) ) ).
cnf(u28000,negated_conjecture,
( ~ product(X0,X1,e_5)
| ~ product(e_1,X0,X1)
| equalish(X0,e_5) ) ).
cnf(u56,axiom,
( ~ group_element(X1)
| equalish(X0,X1)
| product(X2,X1,e_1)
| product(X2,X1,e_2)
| product(X2,X1,e_3)
| product(X2,X1,e_4)
| ~ group_element(X2)
| ~ group_element(X0)
| product(X2,X0,e_1)
| product(X2,X0,e_2)
| product(X2,X0,e_3)
| product(X2,X0,e_4) ) ).
cnf(u27933,axiom,
( ~ product(e_1,X0,e_2)
| equalish(X0,e_4) ) ).
cnf(u5724,axiom,
( ~ group_element(X0)
| product(X0,e_1,e_2)
| product(X0,e_1,e_3)
| product(X0,e_1,e_4)
| product(X0,e_1,e_1)
| product(X0,e_5,e_1)
| product(X0,e_5,e_2)
| product(X0,e_5,e_3)
| product(X0,e_5,e_4) ) ).
cnf(u28300,negated_conjecture,
( ~ product(X0,e_5,e_2)
| ~ group_element(X0)
| product(e_4,X0,e_1)
| product(e_4,X0,e_2)
| product(e_4,X0,e_3)
| product(e_4,X0,e_4) ) ).
cnf(u28403,negated_conjecture,
( ~ product(e_1,e_3,X0)
| product(e_3,X0,e_1)
| product(e_3,X0,e_2)
| product(e_3,X0,e_3)
| product(e_3,X0,e_4)
| ~ group_element(X0) ) ).
cnf(u28215,negated_conjecture,
( ~ product(X0,e_5,e_1)
| ~ group_element(X0)
| product(e_1,X0,e_1)
| product(e_1,X0,e_2)
| product(e_1,X0,e_3)
| product(e_1,X0,e_4) ) ).
cnf(u12893,negated_conjecture,
( ~ group_element(X1)
| product(X0,e_2,e_1)
| product(X0,e_2,e_2)
| product(X0,e_2,e_3)
| product(X0,e_2,e_4)
| ~ group_element(X0)
| ~ product(X0,e_1,X1)
| product(e_1,X1,e_1)
| product(e_1,X1,e_2)
| product(e_1,X1,e_3)
| product(e_1,X1,e_4) ) ).
cnf(u27447,axiom,
( ~ product(e_5,e_3,X0)
| equalish(X0,e_4) ) ).
cnf(u57,negated_conjecture,
( ~ group_element(X3)
| equalish(X2,e_5)
| ~ product(X0,X1,X2)
| product(X0,X3,e_1)
| product(X0,X3,e_2)
| product(X0,X3,e_3)
| product(X0,X3,e_4)
| ~ group_element(X0)
| product(X3,e_5,e_1)
| product(X3,e_5,e_2)
| product(X3,e_5,e_3)
| product(X3,e_5,e_4)
| ~ group_element(X2)
| product(X1,X2,e_1)
| product(X1,X2,e_2)
| product(X1,X2,e_3)
| product(X1,X2,e_4)
| ~ group_element(X1) ) ).
cnf(u28503,negated_conjecture,
( ~ product(e_2,e_1,X0)
| product(e_1,X0,e_1)
| product(e_1,X0,e_2)
| product(e_1,X0,e_3)
| product(e_1,X0,e_4)
| ~ group_element(X0) ) ).
cnf(u62,axiom,
( ~ group_element(X0)
| product(X1,e_4,e_1)
| product(X1,e_4,e_2)
| product(X1,e_4,e_3)
| product(X1,e_4,e_4)
| ~ group_element(X1)
| product(X0,e_4,e_1)
| product(X0,e_4,e_2)
| product(X0,e_4,e_3)
| product(X0,e_4,e_4)
| equalish(X0,X1) ) ).
cnf(u27444,negated_conjecture,
( ~ product(e_3,e_4,X0)
| ~ product(e_5,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X2,e_4) ) ).
cnf(u6005,axiom,
( ~ group_element(X0)
| product(X0,e_1,e_2)
| product(X0,e_1,e_3)
| product(X0,e_1,e_4)
| product(X0,e_1,e_1)
| 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(u28071,negated_conjecture,
( ~ product(X0,e_5,e_1)
| ~ group_element(X0)
| product(e_5,X0,e_1)
| product(e_5,X0,e_2)
| product(e_5,X0,e_3)
| product(e_5,X0,e_4) ) ).
cnf(u27895,negated_conjecture,
( ~ product(e_2,e_4,X0)
| ~ product(e_4,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X2,e_4) ) ).
cnf(u28037,negated_conjecture,
( ~ product(e_4,X0,X1)
| ~ product(X0,X1,e_3)
| equalish(X0,e_2) ) ).
cnf(u63,axiom,
( ~ group_element(X0)
| product(X1,e_5,e_1)
| product(X1,e_5,e_2)
| product(X1,e_5,e_3)
| product(X1,e_5,e_4)
| ~ group_element(X1)
| product(X0,e_5,e_1)
| product(X0,e_5,e_2)
| product(X0,e_5,e_3)
| product(X0,e_5,e_4)
| equalish(X0,X1) ) ).
cnf(u12503,negated_conjecture,
( ~ group_element(X2)
| ~ product(X1,X2,X0)
| product(X1,e_2,e_1)
| product(X1,e_2,e_2)
| product(X1,e_2,e_3)
| product(X1,e_2,e_4)
| ~ group_element(X1)
| ~ group_element(X0)
| product(X2,X0,e_1)
| product(X2,X0,e_2)
| product(X2,X0,e_3)
| product(X2,X0,e_4)
| equalish(X0,e_5) ) ).
cnf(u28031,negated_conjecture,
( ~ product(e_4,X0,X1)
| ~ product(X0,X1,e_3)
| equalish(X1,e_4) ) ).
cnf(u60,axiom,
( ~ group_element(X0)
| product(X1,e_2,e_1)
| product(X1,e_2,e_2)
| product(X1,e_2,e_3)
| product(X1,e_2,e_4)
| ~ group_element(X1)
| product(X0,e_2,e_1)
| product(X0,e_2,e_2)
| product(X0,e_2,e_3)
| product(X0,e_2,e_4)
| equalish(X0,X1) ) ).
cnf(u27922,negated_conjecture,
( ~ product(e_5,e_2,X0)
| ~ product(e_4,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X2,e_2) ) ).
cnf(u27516,negated_conjecture,
( ~ group_element(X0)
| ~ product(X1,X2,e_1)
| equalish(X1,e_5)
| product(X0,e_5,e_1)
| product(X0,e_5,e_2)
| product(X0,e_5,e_3)
| product(X0,e_5,e_4)
| ~ product(X0,X1,X2) ) ).
cnf(u28500,negated_conjecture,
( ~ product(e_2,e_5,X0)
| product(e_5,X0,e_1)
| product(e_5,X0,e_2)
| product(e_5,X0,e_3)
| product(e_5,X0,e_4)
| ~ group_element(X0) ) ).
cnf(u61,axiom,
( ~ group_element(X0)
| product(X1,e_3,e_1)
| product(X1,e_3,e_2)
| product(X1,e_3,e_3)
| product(X1,e_3,e_4)
| ~ group_element(X1)
| product(X0,e_3,e_1)
| product(X0,e_3,e_2)
| product(X0,e_3,e_3)
| product(X0,e_3,e_4)
| equalish(X0,X1) ) ).
cnf(u27445,axiom,
( ~ product(X0,e_3,e_4)
| equalish(X0,e_5) ) ).
cnf(u27844,negated_conjecture,
( ~ product(X0,e_5,e_2)
| equalish(X0,e_2)
| ~ group_element(X0)
| product(e_1,X0,e_1)
| product(e_1,X0,e_2)
| product(e_1,X0,e_4) ) ).
cnf(u27924,axiom,
( ~ product(e_4,X0,e_2)
| equalish(X0,e_5) ) ).
cnf(u27451,axiom,
( ~ product(X0,e_2,e_2)
| equalish(X0,e_5) ) ).
cnf(u27909,negated_conjecture,
( ~ product(e_3,X0,X1)
| ~ product(X0,X1,e_1)
| equalish(X1,e_4) ) ).
cnf(u28028,negated_conjecture,
( ~ group_element(X0)
| equalish(X1,e_1)
| ~ group_element(X1)
| product(X0,X1,e_1)
| product(X0,X1,e_2)
| product(X0,X1,e_3)
| product(X0,X1,e_4)
| ~ product(e_4,X0,X1) ) ).
cnf(u27942,axiom,
( ~ product(X0,e_5,e_4)
| equalish(X0,e_1) ) ).
cnf(u28465,negated_conjecture,
( ~ product(e_4,e_2,X0)
| ~ group_element(X0)
| product(e_2,X0,e_1)
| product(e_2,X0,e_2)
| product(e_2,X0,e_3)
| equalish(X0,e_1) ) ).
cnf(u27898,axiom,
( ~ product(e_4,e_2,X0)
| equalish(X0,e_4) ) ).
cnf(u28501,negated_conjecture,
( ~ product(e_2,e_4,X0)
| product(e_4,X0,e_1)
| product(e_4,X0,e_2)
| product(e_4,X0,e_3)
| product(e_4,X0,e_4)
| ~ group_element(X0) ) ).
cnf(u5727,axiom,
( ~ group_element(X0)
| product(X0,e_1,e_2)
| product(X0,e_1,e_3)
| product(X0,e_1,e_4)
| product(X0,e_1,e_1)
| 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(u28263,negated_conjecture,
( ~ product(X0,e_5,e_4)
| equalish(X0,e_3)
| ~ group_element(X0)
| product(e_5,X0,e_1)
| product(e_5,X0,e_2)
| product(e_5,X0,e_3) ) ).
cnf(u27482,negated_conjecture,
( ~ product(e_1,e_2,X0)
| ~ product(e_3,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X1,e_1) ) ).
cnf(u28048,negated_conjecture,
( ~ group_element(X0)
| equalish(X0,e_4)
| ~ group_element(X1)
| product(X0,X1,e_1)
| product(X0,X1,e_2)
| product(X0,X1,e_3)
| product(X0,X1,e_4)
| ~ product(e_4,X0,X1) ) ).
cnf(u28223,negated_conjecture,
( ~ product(X0,e_5,e_3)
| equalish(X0,e_5)
| ~ group_element(X0)
| product(e_5,X0,e_2)
| product(e_5,X0,e_3)
| product(e_5,X0,e_4) ) ).
cnf(u28017,negated_conjecture,
( ~ product(e_4,X0,X1)
| ~ product(X0,X1,e_2)
| equalish(X0,e_5) ) ).
cnf(u28153,negated_conjecture,
( ~ product(e_2,X0,X1)
| equalish(X0,e_5)
| ~ product(X0,X1,e_1) ) ).
cnf(u27831,negated_conjecture,
( ~ product(X0,X1,e_5)
| ~ product(e_2,X0,X1)
| equalish(X0,e_3) ) ).
cnf(u28404,negated_conjecture,
( ~ product(e_1,e_2,X0)
| product(e_2,X0,e_1)
| product(e_2,X0,e_2)
| product(e_2,X0,e_3)
| product(e_2,X0,e_4)
| ~ group_element(X0) ) ).
cnf(u27915,axiom,
( ~ product(e_4,X0,e_1)
| equalish(X0,e_4) ) ).
cnf(u6011,axiom,
( ~ group_element(X0)
| product(X0,e_3,e_2)
| product(X0,e_3,e_3)
| product(X0,e_3,e_4)
| product(X0,e_3,e_1)
| product(X0,e_4,e_1)
| product(X0,e_4,e_2)
| product(X0,e_4,e_3)
| product(X0,e_4,e_4) ) ).
cnf(u27950,negated_conjecture,
( ~ product(e_1,e_1,X0)
| ~ product(e_1,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X2,e_1) ) ).
cnf(u28481,negated_conjecture,
( ~ product(e_5,e_4,X0)
| product(e_4,X0,e_1)
| product(e_4,X0,e_2)
| product(e_4,X0,e_3)
| product(e_4,X0,e_4)
| ~ group_element(X0) ) ).
cnf(u27492,axiom,
( ~ product(e_5,X0,e_3)
| equalish(X0,e_1) ) ).
cnf(u27484,axiom,
( ~ product(X0,e_1,e_2)
| equalish(X0,e_3) ) ).
cnf(u27762,negated_conjecture,
( ~ product(e_4,e_3,X0)
| ~ product(e_2,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X2,e_3) ) ).
cnf(u27763,axiom,
( ~ product(X0,e_4,e_3)
| equalish(X0,e_2) ) ).
cnf(u27668,negated_conjecture,
( ~ product(e_3,X0,X1)
| ~ product(X0,X1,e_4)
| equalish(X0,e_5) ) ).
cnf(u27903,negated_conjecture,
( ~ product(e_2,e_1,X0)
| ~ product(e_2,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X2,e_1) ) ).
cnf(u27930,negated_conjecture,
( ~ product(e_4,e_2,X0)
| ~ product(e_1,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X1,e_4) ) ).
cnf(u28097,negated_conjecture,
( ~ product(e_5,X0,X1)
| equalish(X1,e_5)
| ~ product(X0,X1,e_2) ) ).
cnf(u12929,negated_conjecture,
( ~ product(X0,e_1,e_3)
| product(X0,e_2,e_2)
| product(X0,e_2,e_3)
| product(X0,e_2,e_4)
| ~ group_element(X0)
| product(X0,e_2,e_1) ) ).
cnf(u27458,axiom,
( ~ product(e_3,X0,e_1)
| equalish(X0,e_3) ) ).
cnf(u5725,axiom,
( ~ group_element(X0)
| product(X0,e_1,e_2)
| product(X0,e_1,e_3)
| product(X0,e_1,e_4)
| product(X0,e_1,e_1)
| 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(u42,negated_conjecture,
( ~ product(X1,X2,e_5)
| ~ product(X0,X1,X2)
| equalish(X1,X3)
| ~ group_element(X3)
| product(X0,X3,e_1)
| product(X0,X3,e_2)
| product(X0,X3,e_3)
| product(X0,X3,e_4)
| ~ group_element(X0)
| product(X3,e_5,e_1)
| product(X3,e_5,e_2)
| product(X3,e_5,e_3)
| product(X3,e_5,e_4) ) ).
cnf(u27493,axiom,
( ~ product(e_5,e_1,X0)
| equalish(X0,e_3) ) ).
cnf(u27835,negated_conjecture,
( ~ product(e_2,X0,X1)
| ~ product(X0,X1,e_3)
| equalish(X0,e_4) ) ).
cnf(u27816,negated_conjecture,
( ~ group_element(X0)
| equalish(X1,e_2)
| ~ group_element(X1)
| product(X0,X1,e_1)
| product(X0,X1,e_2)
| product(X0,X1,e_3)
| product(X0,X1,e_4)
| ~ product(e_2,X0,X1) ) ).
cnf(u27892,axiom,
( ~ product(e_2,e_1,X0)
| equalish(X0,e_4) ) ).
cnf(u27485,axiom,
( ~ product(e_3,X0,e_2)
| equalish(X0,e_1) ) ).
cnf(u27817,negated_conjecture,
( ~ product(e_4,X0,X1)
| ~ product(X0,X1,e_1)
| equalish(X1,e_3) ) ).
cnf(u27418,axiom,
( ~ product(X0,e_4,e_4)
| equalish(X0,e_3) ) ).
cnf(u6008,axiom,
( ~ group_element(X0)
| product(X0,e_2,e_2)
| product(X0,e_2,e_3)
| product(X0,e_2,e_4)
| product(X0,e_2,e_1)
| product(X0,e_3,e_1)
| product(X0,e_3,e_2)
| product(X0,e_3,e_3)
| product(X0,e_3,e_4) ) ).
cnf(u27048,negated_conjecture,
( ~ product(e_2,e_3,X0)
| ~ product(e_1,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X1,e_2) ) ).
cnf(u27953,axiom,
( ~ product(e_1,e_1,X0)
| equalish(X0,e_1) ) ).
cnf(u27649,negated_conjecture,
( ~ product(X0,X1,e_5)
| ~ product(e_5,X0,X1)
| equalish(X1,e_3) ) ).
cnf(u27943,axiom,
( ~ product(e_1,X0,e_4)
| equalish(X0,e_5) ) ).
cnf(u27511,axiom,
( ~ product(X0,e_5,e_1)
| equalish(X0,e_5) ) ).
cnf(u27888,negated_conjecture,
( ~ product(e_1,e_4,X0)
| ~ product(e_2,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X1,e_1) ) ).
cnf(u28055,negated_conjecture,
( ~ product(X0,e_5,e_1)
| equalish(X0,e_2)
| ~ group_element(X0)
| product(e_5,X0,e_1)
| product(e_5,X0,e_3)
| product(e_5,X0,e_4) ) ).
cnf(u28447,negated_conjecture,
( ~ product(e_2,e_1,X0)
| ~ group_element(X0)
| product(e_1,X0,e_1)
| product(e_1,X0,e_2)
| product(e_1,X0,e_4)
| equalish(X0,e_2) ) ).
cnf(u27889,negated_conjecture,
( ~ product(e_1,e_4,X0)
| ~ product(e_2,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X2,e_4) ) ).
cnf(u6360,axiom,
( ~ group_element(X0)
| product(X0,e_5,e_2)
| product(X0,e_5,e_3)
| product(X0,e_5,e_4)
| product(X0,e_5,e_1)
| product(X0,e_3,e_1)
| product(X0,e_3,e_2)
| product(X0,e_3,e_3)
| product(X0,e_3,e_4) ) ).
cnf(u27906,axiom,
( ~ product(e_2,e_2,X0)
| equalish(X0,e_1) ) ).
cnf(u27787,axiom,
( ~ product(X0,e_3,e_3)
| equalish(X0,e_4) ) ).
cnf(u27049,negated_conjecture,
( ~ product(e_2,e_3,X0)
| ~ product(e_1,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X2,e_3) ) ).
cnf(u27940,negated_conjecture,
( ~ product(e_5,e_4,X0)
| ~ product(e_1,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X1,e_5) ) ).
cnf(u44,axiom,
( ~ group_element(X2)
| equalish(X0,X1)
| product(X1,X2,e_1)
| product(X1,X2,e_2)
| product(X1,X2,e_3)
| product(X1,X2,e_4)
| ~ group_element(X1)
| product(X0,X2,e_1)
| product(X0,X2,e_2)
| product(X0,X2,e_3)
| product(X0,X2,e_4)
| ~ group_element(X0) ) ).
cnf(u27902,negated_conjecture,
( ~ product(e_2,e_1,X0)
| ~ product(e_2,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X1,e_2) ) ).
cnf(u28402,negated_conjecture,
( ~ product(e_1,e_4,X0)
| product(e_4,X0,e_1)
| product(e_4,X0,e_2)
| product(e_4,X0,e_3)
| product(e_4,X0,e_4)
| ~ group_element(X0) ) ).
cnf(u28366,negated_conjecture,
( ~ product(X0,e_5,e_4)
| ~ group_element(X0)
| product(e_3,X0,e_1)
| product(e_3,X0,e_2)
| product(e_3,X0,e_3)
| product(e_3,X0,e_4) ) ).
cnf(u27443,negated_conjecture,
( ~ product(e_3,e_4,X0)
| ~ product(e_5,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X1,e_3) ) ).
cnf(u34,axiom,
( ~ product(X0,X1,e_5)
| equalish(X0,X2)
| ~ group_element(X1)
| product(X2,X1,e_1)
| product(X2,X1,e_2)
| product(X2,X1,e_3)
| product(X2,X1,e_4)
| ~ group_element(X2) ) ).
cnf(u28316,negated_conjecture,
( ~ product(X0,e_5,e_3)
| ~ group_element(X0)
| product(e_3,X0,e_1)
| product(e_3,X0,e_2)
| product(e_3,X0,e_3)
| product(e_3,X0,e_4) ) ).
cnf(u27416,negated_conjecture,
( ~ product(e_4,e_4,X0)
| ~ product(e_3,X1,X2)
| ~ product(X1,X2,X0)
| equalish(X1,e_4) ) ).
cnf(u35,negated_conjecture,
( ~ product(X0,e_5,X1)
| ~ product(X2,X3,X4)
| ~ product(X3,X4,X1)
| equalish(X4,e_5)
| ~ group_element(X0)
| product(X2,X0,e_1)
| product(X2,X0,e_2)
| product(X2,X0,e_3)
| product(X2,X0,e_4)
| ~ group_element(X2) ) ).
cnf(u27695,negated_conjecture,
( ~ product(X0,X1,e_5)
| ~ product(e_5,X0,X1)
| equalish(X0,e_1) ) ).
cnf(u27515,negated_conjecture,
( ~ group_element(X0)
| ~ product(X1,X2,e_1)
| equalish(X2,e_5)
| product(X0,e_5,e_1)
| product(X0,e_5,e_2)
| product(X0,e_5,e_3)
| product(X0,e_5,e_4)
| ~ product(X0,X1,X2) ) ).
cnf(u27651,negated_conjecture,
( ~ product(e_5,X0,X1)
| ~ product(X0,X1,e_3)
| equalish(X0,e_5) ) ).
cnf(u32,axiom,
( ~ product(X0,X1,X2)
| equalish(X2,e_5)
| ~ group_element(X1)
| product(X0,X1,e_1)
| product(X0,X1,e_2)
| product(X0,X1,e_3)
| product(X0,X1,e_4)
| ~ group_element(X0) ) ).
cnf(u5714,axiom,
( ~ group_element(X0)
| product(X1,e_2,e_1)
| product(X1,e_2,e_2)
| product(X1,e_2,e_3)
| product(X1,e_2,e_4)
| ~ group_element(X1)
| equalish(X0,e_2)
| product(X1,X0,e_1)
| product(X1,X0,e_2)
| product(X1,X0,e_3)
| product(X1,X0,e_4) ) ).
cnf(u28445,negated_conjecture,
( ~ product(e_2,e_4,X0)
| ~ group_element(X0)
| product(e_4,X0,e_1)
| product(e_4,X0,e_2)
| product(e_4,X0,e_3)
| equalish(X0,e_2) ) ).
cnf(u27788,axiom,
( ~ product(e_4,X0,e_3)
| equalish(X0,e_3) ) ).
cnf(u28521,negated_conjecture,
( ~ product(e_4,e_1,X0)
| product(e_1,X0,e_1)
| product(e_1,X0,e_2)
| product(e_1,X0,e_3)
| product(e_1,X0,e_4)
| ~ group_element(X0) ) ).
cnf(u28247,negated_conjecture,
( ~ product(X0,e_5,e_3)
| ~ group_element(X0)
| product(e_5,X0,e_1)
| product(e_5,X0,e_2)
| product(e_5,X0,e_3)
| product(e_5,X0,e_4) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP132-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.12/0.37 % Computer : n014.cluster.edu
% 0.12/0.37 % Model : x86_64 x86_64
% 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.37 % Memory : 8046.5625MB
% 0.12/0.37 % OS : Linux 6.8.0-71-generic
% 0.12/0.37 % CPULimit : 300
% 0.12/0.37 % WCLimit : 300
% 0.12/0.37 % DateTime : Sun Sep 27 09:30:46 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.41 Running first-order theorem proving
% 0.12/0.41 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.76/2.12 % (545670)Input is clausal, will run a generic CNF schedule.
% 8.76/2.12 % (545679)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1281780645:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 8.76/2.12 % (545679)Instruction limit reached!
% 8.76/2.12 % (545679)------------------------------
% 8.76/2.12 % (545679)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.76/2.12 % (545679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.76/2.12 % (545679)CaDiCaL version: 2.1.3
% 8.76/2.12 % (545679)Termination reason: Instruction limit
% 8.76/2.12 % (545679)Termination phase: Saturation
% 8.76/2.12 % (545679)Time elapsed: 0.031 s
% 8.76/2.12 % (545679)Peak memory usage: 88 MB
% 8.76/2.12 % (545679)Instructions burned: 117 (million)
% 8.76/2.12 % (545676)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=4237491239:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 8.76/2.12 % (545677)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=563221791:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 8.76/2.12 % (545678)lrs+10_1_sil=8000:sp=occurrence:random_seed=2915132977:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 8.76/2.12 % (545675)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=3434256835:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 8.76/2.12 % (545680)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=517076739:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 8.76/2.12 % (545681)dis-21_1_sil=8000:lcm=predicate:random_seed=3332087599: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.76/2.12 % (545678)Instruction limit reached!
% 8.76/2.12 % (545678)------------------------------
% 8.76/2.12 % (545678)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.76/2.12 % (545678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.76/2.12 % (545678)CaDiCaL version: 2.1.3
% 8.76/2.12 % (545678)Termination reason: Instruction limit
% 8.76/2.12 % (545678)Termination phase: Saturation
% 8.76/2.12 % (545678)Time elapsed: 0.050 s
% 8.76/2.12 % (545678)Peak memory usage: 88 MB
% 8.76/2.12 % (545678)Instructions burned: 108 (million)
% 8.76/2.12 % (545681)Instruction limit reached!
% 8.76/2.12 % (545681)------------------------------
% 8.76/2.12 % (545681)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.76/2.12 % (545681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.76/2.12 % (545681)CaDiCaL version: 2.1.3
% 8.76/2.12 % (545681)Termination reason: Instruction limit
% 8.76/2.12 % (545681)Termination phase: Saturation
% 8.76/2.12 % (545681)Time elapsed: 0.065 s
% 8.76/2.12 % (545681)Peak memory usage: 89 MB
% 8.76/2.12 % (545681)Instructions burned: 119 (million)
% 8.76/2.12 % (545683)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=1821589137:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 8.76/2.12 % (545680)Instruction limit reached!
% 8.76/2.12 % (545680)------------------------------
% 8.76/2.12 % (545680)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.76/2.12 % (545680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.76/2.12 % (545680)CaDiCaL version: 2.1.3
% 8.76/2.12 % (545680)Termination reason: Instruction limit
% 8.76/2.12 % (545680)Termination phase: Saturation
% 8.76/2.12 % (545680)Time elapsed: 0.115 s
% 8.76/2.12 % (545680)Peak memory usage: 89 MB
% 8.76/2.12 % (545680)Instructions burned: 181 (million)
% 8.76/2.12 % (545683)Instruction limit reached!
% 8.76/2.12 % (545683)------------------------------
% 8.76/2.12 % (545683)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.76/2.12 % (545683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.76/2.12 % (545683)CaDiCaL version: 2.1.3
% 8.76/2.12 % (545683)Termination reason: Instruction limit
% 8.76/2.12 % (545683)Termination phase: Saturation
% 8.76/2.12 % (545683)Time elapsed: 0.038 s
% 8.76/2.12 % (545683)Peak memory usage: 88 MB
% 8.76/2.12 % (545683)Instructions burned: 146 (million)
% 8.76/2.12 % (545690)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2927854306: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)
% 12.83/2.88 % (545690)Refutation not found, incomplete strategy
% 12.83/2.88 % (545690)------------------------------
% 12.83/2.88 % (545690)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.83/2.88 % (545690)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.83/2.88 % (545690)CaDiCaL version: 2.1.3
% 12.83/2.88 % (545690)Termination reason: Refutation not found, incomplete strategy
% 12.83/2.88 % (545690)Time elapsed: 0.002 s
% 12.83/2.88 % (545690)Peak memory usage: 87 MB
% 12.83/2.88 % (545690)Instructions burned: 2 (million)
% 12.83/2.88 % (545691)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=2930881002:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 12.83/2.88 % (545694)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1728614643:avsq=on:i=194:fgj=on:bd=preordered_2996 on theBenchmark for (2996ds/194Mi)
% 12.83/2.88 % (545693)lrs+10_64_to=lpo:sil=8000:random_seed=1394290574:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 12.83/2.88 % (545694)Instruction limit reached!
% 12.83/2.88 % (545694)------------------------------
% 12.83/2.88 % (545694)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.83/2.88 % (545694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.83/2.88 % (545694)CaDiCaL version: 2.1.3
% 12.83/2.88 % (545694)Termination reason: Instruction limit
% 12.83/2.88 % (545694)Termination phase: Saturation
% 12.83/2.88 % (545694)Time elapsed: 0.062 s
% 12.83/2.88 % (545694)Peak memory usage: 88 MB
% 12.83/2.88 % (545694)Instructions burned: 196 (million)
% 12.83/2.88 % (545693)Instruction limit reached!
% 12.83/2.88 % (545693)------------------------------
% 12.83/2.88 % (545693)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.83/2.88 % (545693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.83/2.88 % (545693)CaDiCaL version: 2.1.3
% 12.83/2.88 % (545693)Termination reason: Instruction limit
% 12.83/2.88 % (545693)Termination phase: Saturation
% 12.83/2.88 % (545693)Time elapsed: 0.073 s
% 12.83/2.88 % (545693)Peak memory usage: 88 MB
% 12.83/2.88 % (545693)Instructions burned: 126 (million)
% 12.83/2.88 % (545691)Instruction limit reached!
% 12.83/2.88 % (545691)------------------------------
% 12.83/2.88 % (545691)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.83/2.88 % (545691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.83/2.88 % (545691)CaDiCaL version: 2.1.3
% 12.83/2.88 % (545691)Termination reason: Instruction limit
% 12.83/2.88 % (545691)Termination phase: Saturation
% 12.83/2.88 % (545691)Time elapsed: 0.114 s
% 12.83/2.88 % (545691)Peak memory usage: 88 MB
% 12.83/2.88 % (545691)Instructions burned: 220 (million)
% 12.83/2.88 % (545699)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1811509880:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 12.83/2.88 % (545690)------------------------------
% 12.83/2.88 % (545690)------------------------------
% 12.83/2.88 % (545699)Instruction limit reached!
% 12.83/2.88 % (545699)------------------------------
% 12.83/2.88 % (545699)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.83/2.88 % (545699)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.83/2.88 % (545699)CaDiCaL version: 2.1.3
% 12.83/2.88 % (545699)Termination reason: Instruction limit
% 12.83/2.88 % (545699)Termination phase: Saturation
% 12.83/2.88 % (545699)Time elapsed: 0.039 s
% 12.83/2.88 % (545699)Peak memory usage: 88 MB
% 12.83/2.88 % (545699)Instructions burned: 159 (million)
% 12.83/2.88 % (545700)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=2000545786:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi)
% 12.83/2.88 % (545701)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=1958816075:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2994 on theBenchmark for (2994ds/106Mi)
% 12.83/2.88 % (545701)Refutation not found, incomplete strategy
% 12.83/2.88 % (545701)------------------------------
% 12.83/2.88 % (545701)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.83/2.88 % (545701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.83/2.88 % (545701)CaDiCaL version: 2.1.3
% 12.83/2.88 % (545701)Termination reason: Refutation not found, incomplete strategy
% 21.50/4.01 % (545701)Time elapsed: 0.002 s
% 21.50/4.01 % (545701)Peak memory usage: 87 MB
% 21.50/4.01 % (545701)Instructions burned: 2 (million)
% 21.50/4.01 % (545676)Refutation not found, incomplete strategy
% 21.50/4.01 % (545676)------------------------------
% 21.50/4.01 % (545676)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.50/4.01 % (545676)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.50/4.01 % (545676)CaDiCaL version: 2.1.3
% 21.50/4.01 % (545676)Termination reason: Refutation not found, incomplete strategy
% 21.50/4.01 % (545676)Time elapsed: 0.584 s
% 21.50/4.01 % (545676)Peak memory usage: 125 MB
% 21.50/4.01 % (545676)Instructions burned: 863 (million)
% 21.50/4.01 % (545704)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=532132062:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2993 on theBenchmark for (2993ds/242Mi)
% 21.50/4.01 % (545703)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2798243969:i=107_2993 on theBenchmark for (2993ds/107Mi)
% 21.50/4.01 % (545703)Instruction limit reached!
% 21.50/4.01 % (545703)------------------------------
% 21.50/4.01 % (545703)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.50/4.01 % (545703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.50/4.01 % (545703)CaDiCaL version: 2.1.3
% 21.50/4.01 % (545703)Termination reason: Instruction limit
% 21.50/4.01 % (545703)Termination phase: Saturation
% 21.50/4.01 % (545703)Time elapsed: 0.050 s
% 21.50/4.01 % (545703)Peak memory usage: 87 MB
% 21.50/4.01 % (545703)Instructions burned: 107 (million)
% 21.50/4.01 % (545704)Instruction limit reached!
% 21.50/4.01 % (545704)------------------------------
% 21.50/4.01 % (545704)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.50/4.01 % (545704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.50/4.01 % (545704)CaDiCaL version: 2.1.3
% 21.50/4.01 % (545704)Termination reason: Instruction limit
% 21.50/4.01 % (545704)Termination phase: Saturation
% 21.50/4.01 % (545704)Time elapsed: 0.061 s
% 21.50/4.01 % (545704)Peak memory usage: 88 MB
% 21.50/4.01 % (545704)Instructions burned: 247 (million)
% 21.50/4.01 % (545701)------------------------------
% 21.50/4.01 % (545701)------------------------------
% 21.50/4.01 % (545710)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=1876333819:i=134:sd=2:doe=on:ss=axioms:sgt=14_2991 on theBenchmark for (2991ds/134Mi)
% 21.50/4.01 % (545709)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3544253738:cond=fast:i=5208:av=off_2991 on theBenchmark for (2991ds/5208Mi)
% 21.50/4.01 % (545710)Instruction limit reached!
% 21.50/4.01 % (545710)------------------------------
% 21.50/4.01 % (545710)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.50/4.01 % (545710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.50/4.01 % (545710)CaDiCaL version: 2.1.3
% 21.50/4.01 % (545710)Termination reason: Instruction limit
% 21.50/4.01 % (545710)Termination phase: Saturation
% 21.50/4.01 % (545710)Time elapsed: 0.043 s
% 21.50/4.01 % (545710)Peak memory usage: 89 MB
% 21.50/4.01 % (545710)Instructions burned: 136 (million)
% 21.50/4.01 % (545676)------------------------------
% 21.50/4.01 % (545676)------------------------------
% 21.50/4.01 % (545711)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=1289546170:i=499:bd=all_2990 on theBenchmark for (2990ds/499Mi)
% 21.50/4.01 % (545714)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=1580835694:i=191:fgj=on:bd=all_2990 on theBenchmark for (2990ds/191Mi)
% 21.50/4.01 % (545714)Instruction limit reached!
% 21.50/4.01 % (545714)------------------------------
% 21.50/4.01 % (545714)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.50/4.01 % (545714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.50/4.01 % (545714)CaDiCaL version: 2.1.3
% 21.50/4.01 % (545714)Termination reason: Instruction limit
% 21.50/4.01 % (545714)Termination phase: Saturation
% 21.50/4.01 % (545714)Time elapsed: 0.054 s
% 21.50/4.01 % (545714)Peak memory usage: 88 MB
% 21.50/4.01 % (545714)Instructions burned: 194 (million)
% 21.50/4.01 % (545715)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2937846400:i=264:kws=precedence:fsr=off_2990 on theBenchmark for (2990ds/264Mi)
% 21.50/4.01 % (545718)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=1041683306:cond=on:i=156:bs=on:gtg=exists_all:er=known_2988 on theBenchmark for (2988ds/156Mi)
% 31.73/5.38 % (545711)Instruction limit reached!
% 31.73/5.38 % (545711)------------------------------
% 31.73/5.38 % (545711)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.73/5.38 % (545711)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.73/5.38 % (545711)CaDiCaL version: 2.1.3
% 31.73/5.38 % (545711)Termination reason: Instruction limit
% 31.73/5.38 % (545711)Termination phase: Saturation
% 31.73/5.38 % (545711)Time elapsed: 0.233 s
% 31.73/5.38 % (545711)Peak memory usage: 89 MB
% 31.73/5.38 % (545711)Instructions burned: 500 (million)
% 31.73/5.38 % (545715)Instruction limit reached!
% 31.73/5.38 % (545715)------------------------------
% 31.73/5.38 % (545715)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.73/5.38 % (545715)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.73/5.38 % (545715)CaDiCaL version: 2.1.3
% 31.73/5.38 % (545715)Termination reason: Instruction limit
% 31.73/5.38 % (545715)Termination phase: Saturation
% 31.73/5.38 % (545715)Time elapsed: 0.128 s
% 31.73/5.38 % (545715)Peak memory usage: 89 MB
% 31.73/5.38 % (545715)Instructions burned: 264 (million)
% 31.73/5.38 % (545718)Instruction limit reached!
% 31.73/5.38 % (545718)------------------------------
% 31.73/5.38 % (545718)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.73/5.38 % (545718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.73/5.38 % (545718)CaDiCaL version: 2.1.3
% 31.73/5.38 % (545718)Termination reason: Instruction limit
% 31.73/5.38 % (545718)Termination phase: Saturation
% 31.73/5.38 % (545718)Time elapsed: 0.047 s
% 31.73/5.38 % (545718)Peak memory usage: 89 MB
% 31.73/5.38 % (545718)Instructions burned: 159 (million)
% 31.73/5.38 % (545723)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=4238246406:i=180:bd=preordered:av=off_2986 on theBenchmark for (2986ds/180Mi)
% 31.73/5.38 % (545722)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=1823675750:i=537:av=off:ss=included_2987 on theBenchmark for (2987ds/537Mi)
% 31.73/5.38 % (545721)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=4210787086:i=3256:kws=precedence:bd=preordered:av=off_2987 on theBenchmark for (2987ds/3256Mi)
% 31.73/5.38 % (545723)Instruction limit reached!
% 31.73/5.38 % (545723)------------------------------
% 31.73/5.38 % (545723)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.73/5.38 % (545723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.73/5.38 % (545723)CaDiCaL version: 2.1.3
% 31.73/5.38 % (545723)Termination reason: Instruction limit
% 31.73/5.38 % (545723)Termination phase: Saturation
% 31.73/5.38 % (545723)Time elapsed: 0.044 s
% 31.73/5.38 % (545723)Peak memory usage: 87 MB
% 31.73/5.38 % (545723)Instructions burned: 181 (million)
% 31.73/5.38 % (545727)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=2560016178:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2985 on theBenchmark for (2985ds/10307Mi)
% 31.73/5.38 % (545722)Instruction limit reached!
% 31.73/5.38 % (545722)------------------------------
% 31.73/5.38 % (545722)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.73/5.38 % (545722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.73/5.38 % (545722)CaDiCaL version: 2.1.3
% 31.73/5.38 % (545722)Termination reason: Instruction limit
% 31.73/5.38 % (545722)Termination phase: Saturation
% 31.73/5.38 % (545722)Time elapsed: 0.241 s
% 31.73/5.38 % (545722)Peak memory usage: 88 MB
% 31.73/5.38 % (545722)Instructions burned: 539 (million)
% 31.73/5.38 % (545729)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=2672141911:i=412:gtgl=4:gtg=exists_all_2983 on theBenchmark for (2983ds/412Mi)
% 31.73/5.38 % (545729)Instruction limit reached!
% 31.73/5.38 % (545729)------------------------------
% 31.73/5.38 % (545729)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.73/5.38 % (545729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.73/5.38 % (545729)CaDiCaL version: 2.1.3
% 31.73/5.38 % (545729)Termination reason: Instruction limit
% 31.73/5.38 % (545729)Termination phase: Saturation
% 42.52/6.94 % (545729)Time elapsed: 0.184 s
% 42.52/6.94 % (545729)Peak memory usage: 90 MB
% 42.52/6.94 % (545729)Instructions burned: 413 (million)
% 42.52/6.94 % (545731)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=2891471473:s2pl=no:i=8478:s2at=4:nm=6_2979 on theBenchmark for (2979ds/8478Mi)
% 42.52/6.94 % (545700)Instruction limit reached!
% 42.52/6.94 % (545700)------------------------------
% 42.52/6.94 % (545700)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.52/6.94 % (545700)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.52/6.94 % (545700)CaDiCaL version: 2.1.3
% 42.52/6.94 % (545700)Termination reason: Instruction limit
% 42.52/6.94 % (545700)Termination phase: Saturation
% 42.52/6.94 % (545700)Time elapsed: 1.711 s
% 42.52/6.94 % (545700)Peak memory usage: 132 MB
% 42.52/6.94 % (545700)Instructions burned: 3395 (million)
% 42.52/6.94 % (545733)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=3828106050:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2976 on theBenchmark for (2976ds/303Mi)
% 42.52/6.94 % (545721)Instruction limit reached!
% 42.52/6.94 % (545721)------------------------------
% 42.52/6.94 % (545721)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.52/6.94 % (545721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.52/6.94 % (545721)CaDiCaL version: 2.1.3
% 42.52/6.94 % (545721)Termination reason: Instruction limit
% 42.52/6.94 % (545721)Termination phase: Saturation
% 42.52/6.94 % (545721)Time elapsed: 1.174 s
% 42.52/6.94 % (545721)Peak memory usage: 132 MB
% 42.52/6.94 % (545721)Instructions burned: 3258 (million)
% 42.52/6.94 % (545733)Instruction limit reached!
% 42.52/6.94 % (545733)------------------------------
% 42.52/6.94 % (545733)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.52/6.94 % (545733)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.52/6.94 % (545733)CaDiCaL version: 2.1.3
% 42.52/6.94 % (545733)Termination reason: Instruction limit
% 42.52/6.94 % (545733)Termination phase: Saturation
% 42.52/6.94 % (545733)Time elapsed: 0.168 s
% 42.52/6.94 % (545733)Peak memory usage: 90 MB
% 42.52/6.94 % (545733)Instructions burned: 305 (million)
% 42.52/6.94 % (545735)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=379709308:st=4:i=720:sd=3:fsr=off:ss=axioms_2973 on theBenchmark for (2973ds/720Mi)
% 42.52/6.94 % (545735)Refutation not found, incomplete strategy
% 42.52/6.94 % (545735)------------------------------
% 42.52/6.94 % (545735)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.52/6.94 % (545735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.52/6.94 % (545735)CaDiCaL version: 2.1.3
% 42.52/6.94 % (545735)Termination reason: Refutation not found, incomplete strategy
% 42.52/6.94 % (545735)Time elapsed: 0.001 s
% 42.52/6.94 % (545735)Peak memory usage: 87 MB
% 42.52/6.94 % (545735)Instructions burned: 1 (million)
% 42.52/6.94 % (545731)Refutation not found, incomplete strategy
% 42.52/6.94 % (545731)------------------------------
% 42.52/6.94 % (545731)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.52/6.94 % (545731)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.52/6.94 % (545731)CaDiCaL version: 2.1.3
% 42.52/6.94 % (545731)Termination reason: Refutation not found, incomplete strategy
% 42.52/6.94 % (545731)Time elapsed: 0.573 s
% 42.52/6.94 % (545731)Peak memory usage: 127 MB
% 42.52/6.94 % (545731)Instructions burned: 863 (million)
% 42.52/6.94 % (545736)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=4115650883:i=598:bs=on:bd=preordered:av=off:ss=axioms_2972 on theBenchmark for (2972ds/598Mi)
% 42.52/6.94 % (545735)------------------------------
% 42.52/6.94 % (545735)------------------------------
% 42.52/6.94 % (545731)------------------------------
% 42.52/6.94 % (545731)------------------------------
% 42.52/6.94 % (545739)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=3478674711:i=2989:sd=3:ss=axioms:sgt=60_2971 on theBenchmark for (2971ds/2989Mi)
% 42.52/6.94 % (545736)Instruction limit reached!
% 42.52/6.94 % (545736)------------------------------
% 42.52/6.94 % (545736)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.52/6.94 % (545736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.04/9.86 % (545736)CaDiCaL version: 2.1.3
% 63.04/9.86 % (545736)Termination reason: Instruction limit
% 63.04/9.86 % (545736)Termination phase: Saturation
% 63.04/9.86 % (545736)Time elapsed: 0.294 s
% 63.04/9.86 % (545736)Peak memory usage: 89 MB
% 63.04/9.86 % (545736)Instructions burned: 599 (million)
% 63.04/9.86 % (545740)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=4117005247:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2969 on theBenchmark for (2969ds/1997Mi)
% 63.04/9.86 % (545742)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=1692694892:i=2088:bd=preordered:av=off_2968 on theBenchmark for (2968ds/2088Mi)
% 63.04/9.86 % (545709)Instruction limit reached!
% 63.04/9.86 % (545709)------------------------------
% 63.04/9.86 % (545709)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.04/9.86 % (545709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.04/9.86 % (545709)CaDiCaL version: 2.1.3
% 63.04/9.86 % (545709)Termination reason: Instruction limit
% 63.04/9.86 % (545709)Termination phase: Saturation
% 63.04/9.86 % (545709)Time elapsed: 2.805 s
% 63.04/9.86 % (545709)Peak memory usage: 131 MB
% 63.04/9.86 % (545709)Instructions burned: 5208 (million)
% 63.04/9.86 % (545745)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=1950418723:i=1098:nicw=on_2962 on theBenchmark for (2962ds/1098Mi)
% 63.04/9.86 % (545739)Instruction limit reached!
% 63.04/9.86 % (545739)------------------------------
% 63.04/9.86 % (545739)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.04/9.86 % (545739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.04/9.86 % (545739)CaDiCaL version: 2.1.3
% 63.04/9.86 % (545739)Termination reason: Instruction limit
% 63.04/9.86 % (545739)Termination phase: Saturation
% 63.04/9.86 % (545739)Time elapsed: 1.016 s
% 63.04/9.86 % (545739)Peak memory usage: 140 MB
% 63.04/9.86 % (545739)Instructions burned: 2989 (million)
% 63.04/9.86 % (545747)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=1807573798:i=433:bd=preordered_2959 on theBenchmark for (2959ds/433Mi)
% 63.04/9.86 % (545747)Instruction limit reached!
% 63.04/9.86 % (545747)------------------------------
% 63.04/9.86 % (545747)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.04/9.86 % (545747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.04/9.86 % (545747)CaDiCaL version: 2.1.3
% 63.04/9.86 % (545747)Termination reason: Instruction limit
% 63.04/9.86 % (545747)Termination phase: Saturation
% 63.04/9.86 % (545747)Time elapsed: 0.126 s
% 63.04/9.86 % (545747)Peak memory usage: 89 MB
% 63.04/9.86 % (545747)Instructions burned: 436 (million)
% 63.04/9.86 % (545745)Instruction limit reached!
% 63.04/9.86 % (545745)------------------------------
% 63.04/9.86 % (545745)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.04/9.86 % (545745)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.04/9.86 % (545745)CaDiCaL version: 2.1.3
% 63.04/9.86 % (545745)Termination reason: Instruction limit
% 63.04/9.86 % (545745)Termination phase: Saturation
% 63.04/9.86 % (545745)Time elapsed: 0.462 s
% 63.04/9.86 % (545745)Peak memory usage: 89 MB
% 63.04/9.86 % (545745)Instructions burned: 1099 (million)
% 63.04/9.86 % (545749)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=414058181:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2956 on theBenchmark for (2956ds/2942Mi)
% 63.04/9.86 % (545740)Instruction limit reached!
% 63.04/9.86 % (545740)------------------------------
% 63.04/9.86 % (545740)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 63.04/9.86 % (545740)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 63.04/9.86 % (545740)CaDiCaL version: 2.1.3
% 63.04/9.86 % (545740)Termination reason: Instruction limit
% 63.04/9.86 % (545740)Termination phase: Saturation
% 63.04/9.86 % (545740)Time elapsed: 1.301 s
% 63.04/9.86 % (545740)Peak memory usage: 134 MB
% 63.04/9.86 % (545740)Instructions burned: 1997 (million)
% 63.04/9.86 % (545742)Instruction limit reached!
% 63.04/9.86 % (545742)------------------------------
% 63.04/9.86 % (545742)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.48/10.14 % (545742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.48/10.14 % (545742)CaDiCaL version: 2.1.3
% 65.48/10.14 % (545742)Termination reason: Instruction limit
% 65.48/10.14 % (545742)Termination phase: Saturation
% 65.48/10.14 % (545742)Time elapsed: 1.205 s
% 65.48/10.14 % (545742)Peak memory usage: 131 MB
% 65.48/10.14 % (545742)Instructions burned: 2089 (million)
% 65.48/10.14 % (545750)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=2820762617:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2955 on theBenchmark for (2955ds/6922Mi)
% 65.48/10.14 % (545752)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=3906702028:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2955 on theBenchmark for (2955ds/596Mi)
% 65.48/10.14 % (545752)Refutation not found, incomplete strategy
% 65.48/10.14 % (545752)------------------------------
% 65.48/10.14 % (545752)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.48/10.14 % (545752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.48/10.14 % (545752)CaDiCaL version: 2.1.3
% 65.48/10.14 % (545752)Termination reason: Refutation not found, incomplete strategy
% 65.48/10.14 % (545752)Time elapsed: 0.002 s
% 65.48/10.14 % (545752)Peak memory usage: 88 MB
% 65.48/10.14 % (545752)Instructions burned: 2 (million)
% 65.48/10.14 % (545753)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=2449038307:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2954 on theBenchmark for (2954ds/4123Mi)
% 65.48/10.14 % (545752)------------------------------
% 65.48/10.14 % (545752)------------------------------
% 65.48/10.14 % (545757)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=826588169:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2951 on theBenchmark for (2951ds/16411Mi)
% 65.48/10.14 % (545750)Refutation not found, incomplete strategy
% 65.48/10.14 % (545750)------------------------------
% 65.48/10.14 % (545750)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.48/10.14 % (545750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.48/10.14 % (545750)CaDiCaL version: 2.1.3
% 65.48/10.14 % (545750)Termination reason: Refutation not found, incomplete strategy
% 65.48/10.14 % (545750)Time elapsed: 0.587 s
% 65.48/10.14 % (545750)Peak memory usage: 127 MB
% 65.48/10.14 % (545750)Instructions burned: 899 (million)
% 65.48/10.14 % (545749)Instruction limit reached!
% 65.48/10.14 % (545749)------------------------------
% 65.48/10.14 % (545749)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.48/10.14 % (545749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.48/10.14 % (545749)CaDiCaL version: 2.1.3
% 65.48/10.14 % (545749)Termination reason: Instruction limit
% 65.48/10.14 % (545749)Termination phase: Saturation
% 65.48/10.14 % (545749)Time elapsed: 0.891 s
% 65.48/10.14 % (545749)Peak memory usage: 132 MB
% 65.48/10.14 % (545749)Instructions burned: 2948 (million)
% 65.48/10.14 % (545750)------------------------------
% 65.48/10.14 % (545750)------------------------------
% 65.48/10.14 % (545759)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=590261176:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2946 on theBenchmark for (2946ds/1670Mi)
% 65.48/10.14 % (545760)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=652335789:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2945 on theBenchmark for (2945ds/1722Mi)
% 65.48/10.14 % (545759)Instruction limit reached!
% 65.48/10.14 % (545759)------------------------------
% 65.48/10.14 % (545759)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.48/10.14 % (545759)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.48/10.14 % (545759)CaDiCaL version: 2.1.3
% 65.48/10.14 % (545759)Termination reason: Instruction limit
% 65.48/10.14 % (545759)Termination phase: Saturation
% 65.48/10.14 % (545759)Time elapsed: 0.521 s
% 65.48/10.14 % (545759)Peak memory usage: 133 MB
% 65.48/10.14 % (545759)Instructions burned: 1673 (million)
% 65.48/10.14 % (545763)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=1260106721:cts=off:cond=on:i=9530:bs=on:fsd=on_2940 on theBenchmark for (2940ds/9530Mi)
% 65.48/10.14 % (545727)Instruction limit reached!
% 65.48/10.14 % (545727)------------------------------
% 65.48/10.14 % (545727)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.48/10.14 % (545727)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.48/10.14 % (545727)CaDiCaL version: 2.1.3
% 65.48/10.14 % (545727)Termination reason: Instruction limit
% 65.48/10.14 % (545727)Termination phase: Saturation
% 65.48/10.14 % (545727)Time elapsed: 5.082 s
% 65.48/10.14 % (545727)Peak memory usage: 140 MB
% 65.48/10.14 % (545727)Instructions burned: 10308 (million)
% 65.48/10.14 % (545760)Instruction limit reached!
% 65.48/10.14 % (545760)------------------------------
% 65.48/10.14 % (545760)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.48/10.14 % (545760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.48/10.14 % (545760)CaDiCaL version: 2.1.3
% 65.48/10.14 % (545760)Termination reason: Instruction limit
% 65.48/10.14 % (545760)Termination phase: Saturation
% 65.48/10.14 % (545760)Time elapsed: 1.177 s
% 65.48/10.14 % (545760)Peak memory usage: 133 MB
% 65.48/10.14 % (545760)Instructions burned: 1724 (million)
% 65.48/10.14 % (545765)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=4198970225:st=2:i=4495:sd=10:ss=included_2933 on theBenchmark for (2933ds/4495Mi)
% 65.48/10.14 % (545766)lrs+1002_1_sfv=off:ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=reverse_arity:spb=non_intro:s2agt=16:random_seed=374191112:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2932 on theBenchmark for (2932ds/4920Mi)
% 65.48/10.14 % (545753)Instruction limit reached!
% 65.48/10.14 % (545753)------------------------------
% 65.48/10.14 % (545753)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.48/10.14 % (545753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.48/10.14 % (545753)CaDiCaL version: 2.1.3
% 65.48/10.14 % (545753)Termination reason: Instruction limit
% 65.48/10.14 % (545753)Termination phase: Saturation
% 65.48/10.14 % (545753)Time elapsed: 2.260 s
% 65.48/10.14 % (545753)Peak memory usage: 134 MB
% 65.48/10.14 % (545753)Instructions burned: 4125 (million)
% 65.48/10.14 % (545769)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:lcm=reverse:bce=on:bsr=unit_only:random_seed=3905973120:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2930 on theBenchmark for (2930ds/2083Mi)
% 65.48/10.14 % (545769)Instruction limit reached!
% 65.48/10.14 % (545769)------------------------------
% 65.48/10.14 % (545769)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.48/10.14 % (545769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.48/10.14 % (545769)CaDiCaL version: 2.1.3
% 65.48/10.14 % (545769)Termination reason: Instruction limit
% 65.48/10.14 % (545769)Termination phase: Saturation
% 65.48/10.14 % (545769)Time elapsed: 1.087 s
% 65.48/10.14 % (545769)Peak memory usage: 130 MB
% 65.48/10.14 % (545769)Instructions burned: 2084 (million)
% 65.48/10.14 % (545771)lrs+31_1_to=lpo:ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=weighted_frequency:sos=all:spb=units:lcm=predicate:bsr=on:gs=on:random_seed=3620184035:i=4629:av=off:gsp=on_2917 on theBenchmark for (2917ds/4629Mi)
% 65.48/10.14 % (545763)Instruction limit reached!
% 65.48/10.14 % (545763)------------------------------
% 65.48/10.14 % (545763)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.48/10.14 % (545763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.48/10.14 % (545763)CaDiCaL version: 2.1.3
% 65.48/10.14 % (545763)Termination reason: Instruction limit
% 65.48/10.14 % (545763)Termination phase: Saturation
% 65.48/10.14 % (545763)Time elapsed: 2.826 s
% 65.48/10.14 % (545763)Peak memory usage: 151 MB
% 65.48/10.14 % (545763)Instructions burned: 9534 (million)
% 65.48/10.14 % (545757)First to succeed.
% 65.48/10.14 % (545771)Refutation not found, incomplete strategy
% 65.48/10.14 % (545771)------------------------------
% 65.48/10.14 % (545771)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.48/10.14 % (545771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.48/10.14 % (545771)CaDiCaL version: 2.1.3
% 65.48/10.14 % (545771)Termination reason: Refutation not found, incomplete strategy
% 65.48/10.14 % (545771)Time elapsed: 0.630 s
% 65.48/10.14 % (545771)Peak memory usage: 128 MB
% 65.48/10.14 % (545771)Instructions burned: 943 (million)
% 65.48/10.14 % (545757)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-545670"
% 65.48/10.14 % (545773)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=1908609249:i=1258:av=off_2910 on theBenchmark for (2910ds/1258Mi)
% 65.48/10.14 % (545765)Instruction limit reached!
% 65.48/10.14 % (545765)------------------------------
% 65.48/10.14 % (545765)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.48/10.14 % (545765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.48/10.14 % (545765)CaDiCaL version: 2.1.3
% 65.48/10.14 % (545765)Termination reason: Instruction limit
% 65.48/10.14 % (545765)Termination phase: Saturation
% 65.48/10.14 % (545765)Time elapsed: 2.196 s
% 65.48/10.14 % (545765)Peak memory usage: 133 MB
% 65.48/10.14 % (545765)Instructions burned: 4498 (million)
% 65.48/10.14 % (545775)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=4035490340:i=7343:av=off:ss=included_2909 on theBenchmark for (2909ds/7343Mi)
% 65.48/10.14 % (545771)------------------------------
% 65.48/10.14 % (545771)------------------------------
% 65.48/10.14 % SZS status Satisfiable for theBenchmark
% 65.48/10.14 % SZS output start Saturation.
% See solution above
% 66.31/10.35 % SZS output start Definitions and Model Updates.
% 66.31/10.35 % SZS output end Definitions and Model Updates.
% 66.31/10.35 % (545757)------------------------------
% 66.31/10.35 % (545757)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 66.31/10.35 % (545757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.31/10.35 % (545757)CaDiCaL version: 2.1.3
% 66.31/10.35 % (545757)Termination reason: Satisfiable
% 66.31/10.35 % (545757)Time elapsed: 3.956 s
% 66.31/10.35 % (545757)Peak memory usage: 152 MB
% 66.31/10.35 % (545757)Instructions burned: 5564 (million)
% 66.31/10.35 % (545757)------------------------------
% 66.31/10.35 % (545757)------------------------------
% 66.31/10.35 % (545670)Success in time 9.293 s
% 66.31/10.35 % Vampire exiting
%------------------------------------------------------------------------------