%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP123-3.004 : TPTP v9.3.1. Released v1.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : 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:12:39 AM UTC 2026
% Result : Satisfiable 5.26s 1.75s
% Output : Saturation 6.87s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u55,axiom,
~ greater(e_1,e_1) ).
cnf(u58,axiom,
cycle(e_1,e_0) ).
cnf(u73,axiom,
~ cycle(e_3,e_3) ).
cnf(u77,axiom,
~ cycle(e_3,e_2) ).
cnf(u82,axiom,
cycle(e_3,e_1) ).
cnf(u85,axiom,
~ cycle(e_3,e_0) ).
cnf(u90,axiom,
~ cycle(e_2,e_3) ).
cnf(u95,axiom,
cycle(e_2,e_2) ).
cnf(u98,axiom,
~ cycle(e_2,e_1) ).
cnf(u102,axiom,
~ cycle(e_2,e_0) ).
cnf(u107,axiom,
~ cycle(e_1,e_3) ).
cnf(u130,axiom,
( ~ cycle(e_1,X0)
| ~ greater(X0,e_0) ) ).
cnf(u158,axiom,
~ next(e_2,e_4) ).
cnf(u197,axiom,
~ greater(e_1,e_3) ).
cnf(u201,axiom,
~ next(e_1,e_4) ).
cnf(u208,axiom,
~ greater(e_1,e_2) ).
cnf(u218,axiom,
~ next(e_2,e_1) ).
cnf(u232,axiom,
~ next(e_3,e_2) ).
cnf(u240,axiom,
~ next(e_2,e_2) ).
cnf(u265,axiom,
~ greater(e_0,e_3) ).
cnf(u273,axiom,
~ greater(e_3,e_3) ).
cnf(u289,axiom,
~ greater(e_0,e_1) ).
cnf(u311,axiom,
~ next(e_3,e_3) ).
cnf(u348,axiom,
( ~ next(e_0,X0)
| equalish(e_1,X0) ) ).
cnf(u401,axiom,
~ greater(e_0,e_2) ).
cnf(u406,axiom,
~ greater(e_2,e_2) ).
cnf(u419,axiom,
~ product(e_4,e_1,e_4) ).
cnf(u423,axiom,
~ product(e_4,e_1,e_3) ).
cnf(u428,axiom,
product(e_4,e_1,e_2) ).
cnf(u431,axiom,
~ product(e_4,e_1,e_1) ).
cnf(u437,axiom,
product(e_3,e_1,e_4) ).
cnf(u440,axiom,
~ product(e_3,e_1,e_3) ).
cnf(u444,axiom,
~ product(e_3,e_1,e_2) ).
cnf(u448,axiom,
~ product(e_3,e_1,e_1) ).
cnf(u453,axiom,
~ product(e_2,e_1,e_4) ).
cnf(u458,axiom,
product(e_2,e_1,e_3) ).
cnf(u461,axiom,
~ product(e_2,e_1,e_2) ).
cnf(u465,axiom,
~ product(e_2,e_1,e_1) ).
cnf(u500,axiom,
( ~ next(e_4,X1)
| equalish(e_3,X1) ) ).
cnf(u508,axiom,
~ product(e_4,e_2,e_4) ).
cnf(u513,axiom,
product(e_4,e_2,e_3) ).
cnf(u516,axiom,
~ product(e_4,e_2,e_2) ).
cnf(u520,axiom,
~ product(e_4,e_2,e_1) ).
cnf(u525,axiom,
~ product(e_3,e_2,e_4) ).
cnf(u529,axiom,
~ product(e_3,e_2,e_3) ).
cnf(u533,axiom,
~ product(e_3,e_2,e_2) ).
cnf(u538,axiom,
product(e_3,e_2,e_1) ).
cnf(u543,axiom,
product(e_1,e_2,e_4) ).
cnf(u546,axiom,
~ product(e_1,e_2,e_3) ).
cnf(u550,axiom,
~ product(e_1,e_2,e_2) ).
cnf(u554,axiom,
~ product(e_1,e_2,e_1) ).
cnf(u593,axiom,
( ~ next(e_4,X1)
| equalish(e_2,X1) ) ).
cnf(u618,axiom,
( ~ next(e_3,X1)
| equalish(e_4,X1) ) ).
cnf(u792,axiom,
~ product(e_4,e_3,e_4) ).
cnf(u796,axiom,
~ product(e_4,e_3,e_3) ).
cnf(u800,axiom,
~ product(e_4,e_3,e_2) ).
cnf(u805,axiom,
product(e_4,e_3,e_1) ).
cnf(u810,axiom,
product(e_2,e_3,e_4) ).
cnf(u813,axiom,
~ product(e_2,e_3,e_3) ).
cnf(u817,axiom,
~ product(e_2,e_3,e_2) ).
cnf(u821,axiom,
~ product(e_2,e_3,e_1) ).
cnf(u826,axiom,
~ product(e_1,e_3,e_4) ).
cnf(u830,axiom,
~ product(e_1,e_3,e_3) ).
cnf(u835,axiom,
product(e_1,e_3,e_2) ).
cnf(u838,axiom,
~ product(e_1,e_3,e_1) ).
cnf(u1051,axiom,
( ~ next(e_2,X1)
| equalish(e_3,X1) ) ).
cnf(u1063,axiom,
~ product(e_3,e_4,e_4) ).
cnf(u1067,axiom,
~ product(e_3,e_4,e_3) ).
cnf(u1072,axiom,
product(e_3,e_4,e_2) ).
cnf(u1075,axiom,
~ product(e_3,e_4,e_1) ).
cnf(u1080,axiom,
~ product(e_2,e_4,e_4) ).
cnf(u1084,axiom,
~ product(e_2,e_4,e_3) ).
cnf(u1088,axiom,
~ product(e_2,e_4,e_2) ).
cnf(u1093,axiom,
product(e_2,e_4,e_1) ).
cnf(u1097,axiom,
~ product(e_1,e_4,e_4) ).
cnf(u1102,axiom,
product(e_1,e_4,e_3) ).
cnf(u1105,axiom,
~ product(e_1,e_4,e_2) ).
cnf(u1109,axiom,
~ product(e_1,e_4,e_1) ).
cnf(u1941,axiom,
( ~ product(X0,e_2,e_4)
| equalish(X0,e_1) ) ).
cnf(u63,axiom,
( ~ product(X0,X1,X0)
| equalish(X1,X0) ) ).
cnf(u50,axiom,
equalish(e_0,e_0) ).
cnf(u1131,negated_conjecture,
~ product(e_3,e_3,e_4) ).
cnf(u2027,negated_conjecture,
~ product(e_1,e_1,e_4) ).
cnf(u2144,axiom,
( ~ product(e_2,X0,e_1)
| equalish(X0,e_4) ) ).
cnf(u1979,negated_conjecture,
( ~ product(e_2,e_1,X0)
| ~ product(e_1,e_3,X0) ) ).
cnf(u1902,negated_conjecture,
( ~ product(e_4,X1,X2)
| ~ product(e_3,e_2,X0)
| ~ product(X2,X1,X0)
| equalish(X1,e_2) ) ).
cnf(u1803,axiom,
( ~ product(X0,e_1,e_2)
| equalish(X0,e_4) ) ).
cnf(u336,axiom,
( ~ cycle(X1,X2)
| ~ cycle(X0,e_0)
| ~ next(X0,e_3)
| ~ greater(X0,X1)
| ~ greater(X2,e_1) ) ).
cnf(u2021,axiom,
( ~ product(e_1,X0,e_2)
| equalish(X0,e_3) ) ).
cnf(u139,axiom,
( ~ cycle(e_1,X0)
| equalish(X0,e_0) ) ).
cnf(u141,axiom,
( ~ cycle(X0,X1)
| ~ next(X0,e_1)
| ~ greater(X1,e_0)
| ~ next(e_0,X2)
| equalish(X1,X2) ) ).
cnf(u250,axiom,
~ next(e_4,e_1) ).
cnf(u1878,negated_conjecture,
( ~ product(e_2,X0,X1)
| ~ product(X1,X0,e_4)
| equalish(X0,e_1) ) ).
cnf(u1911,negated_conjecture,
( ~ product(e_4,e_4,X0)
| ~ product(e_3,e_2,X0) ) ).
cnf(u2188,negated_conjecture,
( ~ product(e_3,X1,X2)
| ~ product(e_2,e_4,X0)
| ~ product(X2,X1,X0)
| equalish(X1,e_4) ) ).
cnf(u1860,negated_conjecture,
( ~ product(e_3,e_1,X0)
| ~ product(e_2,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X2,e_3) ) ).
cnf(u49,axiom,
( ~ cycle(e_4,X0)
| equalish(X0,e_0) ) ).
cnf(u1940,axiom,
( ~ product(e_1,X0,e_4)
| equalish(X0,e_2) ) ).
cnf(u1964,negated_conjecture,
( ~ product(e_1,X0,X1)
| ~ product(X1,X0,e_3)
| equalish(X0,e_2) ) ).
cnf(qg1_1,negated_conjecture,
( ~ product(X5,X4,X3)
| ~ product(X3,X4,X2)
| ~ product(X5,X1,X0)
| ~ product(X0,X1,X2)
| equalish(X0,X3) ) ).
cnf(u46,negated_conjecture,
( ~ product(X3,X2,X1)
| ~ product(X0,X2,X3)
| ~ product(X0,X0,X1)
| equalish(X3,X0) ) ).
cnf(u45,negated_conjecture,
( ~ product(X3,X2,X1)
| ~ product(X0,X2,X3)
| ~ product(X0,X0,X1)
| equalish(X2,X0) ) ).
cnf(e_3_is_not_e_1,axiom,
~ equalish(e_3,e_1) ).
cnf(product_total_function2,axiom,
( ~ product(X0,X1,X3)
| ~ product(X0,X1,X2)
| equalish(X2,X3) ) ).
cnf(e_1_is_not_e_2,axiom,
~ equalish(e_1,e_2) ).
cnf(u2216,axiom,
( ~ product(e_1,e_4,X0)
| equalish(X0,e_3) ) ).
cnf(u2003,axiom,
( ~ product(X0,e_3,e_4)
| equalish(X0,e_2) ) ).
cnf(element_4,axiom,
group_element(e_4) ).
cnf(e_1_is_not_e_4,axiom,
~ equalish(e_1,e_4) ).
cnf(u1863,negated_conjecture,
( ~ product(X0,e_1,e_2)
| ~ product(X0,X0,e_3)
| equalish(e_2,X0) ) ).
cnf(cycle5,axiom,
( ~ cycle(X3,X4)
| ~ cycle(X2,e_0)
| ~ cycle(X0,X1)
| ~ next(X2,X3)
| ~ greater(X2,X0)
| ~ greater(X1,X4) ) ).
cnf(element_1,axiom,
group_element(e_1) ).
cnf(u2185,axiom,
( ~ product(e_3,X0,e_2)
| equalish(X0,e_4) ) ).
cnf(e_4_greater_e_0,axiom,
greater(e_4,e_0) ).
cnf(cycle7,axiom,
( ~ product(X0,e_1,X2)
| ~ cycle(X0,X1)
| ~ greater(X1,e_0)
| ~ next(X0,X3)
| equalish(X2,X3) ) ).
cnf(u2168,negated_conjecture,
( ~ product(e_4,e_3,X0)
| ~ product(e_1,e_4,X0) ) ).
cnf(u1490,negated_conjecture,
~ product(e_2,e_2,e_1) ).
cnf(cycle1,axiom,
( ~ cycle(X0,X2)
| ~ cycle(X0,X1)
| equalish(X1,X2) ) ).
cnf(u1926,negated_conjecture,
( ~ product(X0,e_2,e_3)
| ~ product(X0,X0,e_1)
| equalish(e_3,X0) ) ).
cnf(e_1_then_e_2,axiom,
next(e_1,e_2) ).
cnf(u2189,negated_conjecture,
( ~ product(X0,e_4,e_3)
| ~ product(X0,X0,e_2)
| equalish(e_4,X0) ) ).
cnf(e_0_then_e_1,axiom,
next(e_0,e_1) ).
cnf(u1922,axiom,
( ~ product(X0,e_2,e_1)
| equalish(X0,e_3) ) ).
cnf(u2193,negated_conjecture,
( ~ product(e_2,e_4,X0)
| ~ product(e_1,e_2,X0) ) ).
cnf(u1831,axiom,
( ~ product(e_3,X0,e_4)
| equalish(X0,e_1) ) ).
cnf(u2030,negated_conjecture,
~ product(e_4,e_4,e_2) ).
cnf(u1898,axiom,
( ~ product(e_4,e_2,X0)
| equalish(X0,e_3) ) ).
cnf(u1874,negated_conjecture,
( ~ product(e_2,X0,X1)
| ~ product(X1,X0,e_4)
| equalish(X1,e_3) ) ).
cnf(u2202,negated_conjecture,
( ~ product(e_4,e_1,X0)
| ~ product(e_2,e_4,X0) ) ).
cnf(u1883,axiom,
( ~ cycle(X0,X1)
| ~ next(X0,e_2)
| ~ greater(X1,e_0)
| ~ next(e_2,X2)
| equalish(X1,X2) ) ).
cnf(u2026,negated_conjecture,
( ~ product(X0,e_3,e_1)
| ~ product(X0,X0,e_2)
| equalish(e_1,X0) ) ).
cnf(u2006,negated_conjecture,
( ~ product(X0,e_3,e_2)
| ~ product(X0,X0,e_4)
| equalish(e_3,X0) ) ).
cnf(u410,axiom,
( ~ group_element(X0)
| product(X0,e_2,e_1)
| product(X0,e_2,e_2)
| product(X0,e_2,e_3)
| product(X0,e_2,e_4) ) ).
cnf(u1960,negated_conjecture,
( ~ product(e_1,X0,X1)
| ~ product(X1,X0,e_3)
| equalish(X1,e_4) ) ).
cnf(u1945,negated_conjecture,
( ~ product(X0,e_2,e_1)
| ~ product(X0,X0,e_4)
| equalish(e_1,X0) ) ).
cnf(u1978,negated_conjecture,
( ~ product(X0,e_3,e_4)
| ~ product(X0,X0,e_1)
| equalish(e_4,X0) ) ).
cnf(u412,axiom,
( ~ group_element(X0)
| product(X0,e_4,e_1)
| product(X0,e_4,e_2)
| product(X0,e_4,e_3)
| product(X0,e_4,e_4) ) ).
cnf(u1835,negated_conjecture,
( ~ product(X0,e_1,e_3)
| ~ product(X0,X0,e_4)
| equalish(e_1,X0) ) ).
cnf(u1925,negated_conjecture,
( ~ product(X0,e_2,e_3)
| ~ product(X0,X0,e_1)
| equalish(e_2,X0) ) ).
cnf(u1802,axiom,
( ~ product(e_4,X0,e_2)
| equalish(X0,e_1) ) ).
cnf(u2169,negated_conjecture,
( ~ product(e_3,e_1,X0)
| ~ product(e_1,e_4,X0) ) ).
cnf(u1973,axiom,
( ~ product(e_4,X0,e_1)
| equalish(X0,e_3) ) ).
cnf(u1901,negated_conjecture,
( ~ product(e_4,X1,X2)
| ~ product(e_3,e_2,X0)
| ~ product(X2,X1,X0)
| equalish(X2,e_3) ) ).
cnf(u1921,axiom,
( ~ product(e_3,X0,e_1)
| equalish(X0,e_2) ) ).
cnf(e_3_then_e_4,axiom,
next(e_3,e_4) ).
cnf(u2218,axiom,
( ~ product(X0,e_4,e_3)
| equalish(X0,e_1) ) ).
cnf(u2220,negated_conjecture,
( ~ product(e_3,e_4,X0)
| ~ product(e_1,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X1,e_4) ) ).
cnf(u2020,axiom,
( ~ product(e_1,e_3,X0)
| equalish(X0,e_2) ) ).
cnf(u1972,axiom,
( ~ product(e_4,e_3,X0)
| equalish(X0,e_1) ) ).
cnf(u1830,axiom,
( ~ product(e_3,e_1,X0)
| equalish(X0,e_4) ) ).
cnf(u334,axiom,
( ~ cycle(e_3,X0)
| equalish(X0,e_1) ) ).
cnf(u2217,axiom,
( ~ product(e_1,X0,e_3)
| equalish(X0,e_4) ) ).
cnf(u409,axiom,
( ~ group_element(X0)
| product(X0,e_1,e_1)
| product(X0,e_1,e_2)
| product(X0,e_1,e_3)
| product(X0,e_1,e_4) ) ).
cnf(u2145,axiom,
( ~ product(X0,e_4,e_1)
| equalish(X0,e_2) ) ).
cnf(u2002,axiom,
( ~ product(e_2,X0,e_4)
| equalish(X0,e_3) ) ).
cnf(product_right_cancellation,axiom,
( ~ product(X0,X3,X2)
| ~ product(X0,X1,X2)
| equalish(X1,X3) ) ).
cnf(u1900,axiom,
( ~ product(X0,e_2,e_3)
| equalish(X0,e_4) ) ).
cnf(e_3_is_not_e_4,axiom,
~ equalish(e_3,e_4) ).
cnf(u1981,negated_conjecture,
( ~ product(e_3,e_2,X0)
| ~ product(e_1,e_3,X0) ) ).
cnf(u1815,negated_conjecture,
( ~ product(e_4,e_4,X0)
| ~ product(e_2,e_1,X0) ) ).
cnf(u1934,negated_conjecture,
( ~ product(e_4,e_1,X0)
| ~ product(e_1,e_2,X0) ) ).
cnf(u1943,negated_conjecture,
( ~ product(e_4,e_2,X0)
| ~ product(e_1,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X1,e_2) ) ).
cnf(u2025,negated_conjecture,
( ~ product(X0,e_3,e_1)
| ~ product(X0,X0,e_2)
| equalish(e_3,X0) ) ).
cnf(u1857,axiom,
( ~ product(e_2,e_1,X0)
| equalish(X0,e_3) ) ).
cnf(u2005,negated_conjecture,
( ~ product(e_4,e_3,X0)
| ~ product(e_2,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X1,e_3) ) ).
cnf(u2187,negated_conjecture,
( ~ product(e_3,X1,X2)
| ~ product(e_2,e_4,X0)
| ~ product(X2,X1,X0)
| equalish(X2,e_2) ) ).
cnf(u1977,negated_conjecture,
( ~ product(X0,e_3,e_4)
| ~ product(X0,X0,e_1)
| equalish(e_3,X0) ) ).
cnf(u1882,axiom,
( ~ cycle(e_2,X0)
| equalish(X0,e_2) ) ).
cnf(u2146,negated_conjecture,
( ~ product(e_2,X1,X2)
| ~ product(e_1,e_4,X0)
| ~ product(X2,X1,X0)
| equalish(X2,e_1) ) ).
cnf(u2001,axiom,
( ~ product(e_2,e_3,X0)
| equalish(X0,e_4) ) ).
cnf(u2148,negated_conjecture,
( ~ product(X0,e_4,e_2)
| ~ product(X0,X0,e_1)
| equalish(e_4,X0) ) ).
cnf(u1862,negated_conjecture,
( ~ product(X0,e_1,e_2)
| ~ product(X0,X0,e_3)
| equalish(e_1,X0) ) ).
cnf(u1801,axiom,
( ~ product(e_4,e_1,X0)
| equalish(X0,e_2) ) ).
cnf(u1806,negated_conjecture,
( ~ product(X0,e_1,e_4)
| ~ product(X0,X0,e_2)
| equalish(e_1,X0) ) ).
cnf(u1834,negated_conjecture,
( ~ product(e_4,e_1,X0)
| ~ product(e_3,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X1,e_1) ) ).
cnf(e_3_is_not_e_2,axiom,
~ equalish(e_3,e_2) ).
cnf(u2221,negated_conjecture,
( ~ product(X0,e_4,e_1)
| ~ product(X0,X0,e_3)
| equalish(e_4,X0) ) ).
cnf(e_4_is_not_e_2,axiom,
~ equalish(e_4,e_2) ).
cnf(u1895,axiom,
( ~ next(e_1,X0)
| equalish(e_2,X0) ) ).
cnf(e_1_is_not_e_3,axiom,
~ equalish(e_1,e_3) ).
cnf(e_2_is_not_e_3,axiom,
~ equalish(e_2,e_3) ).
cnf(e_2_is_not_e_1,axiom,
~ equalish(e_2,e_1) ).
cnf(u1933,negated_conjecture,
( ~ product(e_3,e_3,X0)
| ~ product(e_1,e_2,X0) ) ).
cnf(u1920,axiom,
( ~ product(e_3,e_2,X0)
| equalish(X0,e_1) ) ).
cnf(cycle2,axiom,
( ~ group_element(X0)
| cycle(X0,e_0)
| cycle(X0,e_1)
| cycle(X0,e_2)
| cycle(X0,e_3) ) ).
cnf(element_2,axiom,
group_element(e_2) ).
cnf(e_3_greater_e_1,axiom,
greater(e_3,e_1) ).
cnf(e_2_greater_e_1,axiom,
greater(e_2,e_1) ).
cnf(e_3_greater_e_2,axiom,
greater(e_3,e_2) ).
cnf(e_2_then_e_3,axiom,
next(e_2,e_3) ).
cnf(u1975,negated_conjecture,
( ~ product(e_4,X1,X2)
| ~ product(e_1,e_3,X0)
| ~ product(X2,X1,X0)
| equalish(X2,e_1) ) ).
cnf(e_2_greater_e_0,axiom,
greater(e_2,e_0) ).
cnf(u164,axiom,
( ~ cycle(X1,X2)
| ~ cycle(X0,e_0)
| ~ next(X0,e_1)
| ~ greater(X0,X1)
| ~ greater(X2,e_0) ) ).
cnf(u2023,negated_conjecture,
( ~ product(e_2,e_3,X0)
| ~ product(e_1,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X2,e_2) ) ).
cnf(e_1_greater_e_0,axiom,
greater(e_1,e_0) ).
cnf(u1859,axiom,
( ~ product(X0,e_1,e_3)
| equalish(X0,e_2) ) ).
cnf(u2024,negated_conjecture,
( ~ product(e_2,e_3,X0)
| ~ product(e_1,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X1,e_3) ) ).
cnf(u1939,axiom,
( ~ product(e_1,e_2,X0)
| equalish(X0,e_4) ) ).
cnf(u2228,negated_conjecture,
( ~ product(e_1,X0,X1)
| ~ product(X1,X0,e_2)
| equalish(X1,e_3) ) ).
cnf(u590,axiom,
~ greater(e_2,e_4) ).
cnf(u1891,axiom,
( ~ cycle(X0,e_0)
| ~ next(X0,e_3)
| ~ greater(X0,e_2) ) ).
cnf(u1804,negated_conjecture,
( ~ product(e_4,X1,X2)
| ~ product(e_2,e_1,X0)
| ~ product(X2,X1,X0)
| equalish(X2,e_2) ) ).
cnf(u1805,negated_conjecture,
( ~ product(e_4,X1,X2)
| ~ product(e_2,e_1,X0)
| ~ product(X2,X1,X0)
| equalish(X1,e_1) ) ).
cnf(u1858,axiom,
( ~ product(e_2,X0,e_3)
| equalish(X0,e_1) ) ).
cnf(u1924,negated_conjecture,
( ~ product(e_3,X1,X2)
| ~ product(e_1,e_2,X0)
| ~ product(X2,X1,X0)
| equalish(X1,e_2) ) ).
cnf(u1990,negated_conjecture,
( ~ product(e_4,e_4,X0)
| ~ product(e_1,e_3,X0) ) ).
cnf(u2143,axiom,
( ~ product(e_2,e_4,X0)
| equalish(X0,e_1) ) ).
cnf(u1128,negated_conjecture,
~ product(e_1,e_1,e_3) ).
cnf(u1905,negated_conjecture,
( ~ product(e_3,e_2,X0)
| ~ product(e_2,e_1,X0) ) ).
cnf(u62,axiom,
equalish(X0,X0) ).
cnf(u2037,negated_conjecture,
( ~ product(e_1,X0,X1)
| ~ product(X1,X0,e_4)
| equalish(X0,e_3) ) ).
cnf(u1942,negated_conjecture,
( ~ product(e_4,e_2,X0)
| ~ product(e_1,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X2,e_4) ) ).
cnf(u2219,negated_conjecture,
( ~ product(e_3,e_4,X0)
| ~ product(e_1,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X2,e_3) ) ).
cnf(u2190,negated_conjecture,
( ~ product(X0,e_4,e_3)
| ~ product(X0,X0,e_2)
| equalish(e_3,X0) ) ).
cnf(u1944,negated_conjecture,
( ~ product(X0,e_2,e_1)
| ~ product(X0,X0,e_4)
| equalish(e_2,X0) ) ).
cnf(u144,axiom,
( ~ cycle(X0,X1)
| ~ next(X0,e_4)
| ~ greater(X1,e_0)
| ~ next(e_0,X2)
| equalish(X1,X2) ) ).
cnf(u2004,negated_conjecture,
( ~ product(e_4,e_3,X0)
| ~ product(e_2,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X2,e_4) ) ).
cnf(u342,axiom,
( ~ cycle(X0,e_0)
| ~ next(X0,e_1)
| ~ greater(X0,e_3) ) ).
cnf(u138,axiom,
~ greater(e_0,e_0) ).
cnf(u1833,negated_conjecture,
( ~ product(e_4,e_1,X0)
| ~ product(e_3,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X2,e_4) ) ).
cnf(u411,axiom,
( ~ group_element(X0)
| product(X0,e_3,e_1)
| product(X0,e_3,e_2)
| product(X0,e_3,e_3)
| product(X0,e_3,e_4) ) ).
cnf(u1846,negated_conjecture,
( ~ product(e_3,X0,X1)
| ~ product(X1,X0,e_2)
| equalish(X0,e_1) ) ).
cnf(u2191,negated_conjecture,
~ product(e_3,e_3,e_1) ).
cnf(u61,axiom,
( ~ product(X0,X0,X1)
| equalish(X1,X0) ) ).
cnf(u2233,negated_conjecture,
( ~ product(e_1,X0,X1)
| ~ product(X1,X0,e_2)
| equalish(X0,e_4) ) ).
cnf(product_idempotence,axiom,
product(X0,X0,X0) ).
cnf(u1903,negated_conjecture,
( ~ product(X0,e_2,e_4)
| ~ product(X0,X0,e_3)
| equalish(e_2,X0) ) ).
cnf(product_left_cancellation,axiom,
( ~ product(X3,X1,X2)
| ~ product(X0,X1,X2)
| equalish(X0,X3) ) ).
cnf(qg1_2,negated_conjecture,
( ~ product(X5,X4,X3)
| ~ product(X3,X4,X2)
| ~ product(X5,X1,X0)
| ~ product(X0,X1,X2)
| equalish(X1,X4) ) ).
cnf(u2226,negated_conjecture,
~ product(e_2,e_2,e_3) ).
cnf(u1976,negated_conjecture,
( ~ product(e_4,X1,X2)
| ~ product(e_1,e_3,X0)
| ~ product(X2,X1,X0)
| equalish(X1,e_3) ) ).
cnf(e_4_is_not_e_1,axiom,
~ equalish(e_4,e_1) ).
cnf(u65,axiom,
( ~ product(X0,X1,X1)
| equalish(X0,X1) ) ).
cnf(product_total_function1,axiom,
( ~ group_element(X1)
| ~ group_element(X0)
| product(X0,X1,e_1)
| product(X0,X1,e_2)
| product(X0,X1,e_3)
| product(X0,X1,e_4) ) ).
cnf(u389,axiom,
~ next(e_4,e_3) ).
cnf(e_4_is_not_e_3,axiom,
~ equalish(e_4,e_3) ).
cnf(element_3,axiom,
group_element(e_3) ).
cnf(u1884,axiom,
( ~ cycle(X1,X2)
| ~ cycle(X0,e_0)
| ~ next(X0,e_2)
| ~ greater(X0,X1)
| ~ greater(X2,e_2) ) ).
cnf(e_2_is_not_e_4,axiom,
~ equalish(e_2,e_4) ).
cnf(cycle4,axiom,
( ~ cycle(X2,X3)
| ~ cycle(X0,X1)
| ~ next(X0,X2)
| ~ greater(X1,e_0)
| ~ next(X3,X4)
| equalish(X1,X4) ) ).
cnf(u949,negated_conjecture,
~ product(e_4,e_4,e_1) ).
cnf(cycle3,axiom,
cycle(e_4,e_0) ).
cnf(u341,axiom,
( ~ cycle(X0,e_0)
| ~ next(X0,e_4)
| ~ greater(X0,e_3) ) ).
cnf(u2167,negated_conjecture,
( ~ product(e_2,e_2,X0)
| ~ product(e_1,e_4,X0) ) ).
cnf(u1836,negated_conjecture,
( ~ product(X0,e_1,e_3)
| ~ product(X0,X0,e_4)
| equalish(e_3,X0) ) ).
cnf(u1053,negated_conjecture,
~ product(e_2,e_2,e_4) ).
cnf(u1807,negated_conjecture,
( ~ product(X0,e_1,e_4)
| ~ product(X0,X0,e_2)
| equalish(e_4,X0) ) ).
cnf(u1056,negated_conjecture,
~ product(e_4,e_4,e_3) ).
cnf(u1894,axiom,
( ~ cycle(X0,e_0)
| ~ next(X0,e_1)
| ~ greater(X0,e_2) ) ).
cnf(u1899,axiom,
( ~ product(e_4,X0,e_3)
| equalish(X0,e_2) ) ).
cnf(u1842,negated_conjecture,
( ~ product(e_3,X0,X1)
| ~ product(X1,X0,e_2)
| equalish(X1,e_4) ) ).
cnf(u2022,axiom,
( ~ product(X0,e_3,e_2)
| equalish(X0,e_1) ) ).
cnf(u623,negated_conjecture,
~ product(e_3,e_3,e_2) ).
cnf(u1861,negated_conjecture,
( ~ product(e_3,e_1,X0)
| ~ product(e_2,X1,X2)
| ~ product(X2,X1,X0)
| equalish(X1,e_1) ) ).
cnf(u1974,axiom,
( ~ product(X0,e_3,e_1)
| equalish(X0,e_4) ) ).
cnf(u2222,negated_conjecture,
( ~ product(X0,e_4,e_1)
| ~ product(X0,X0,e_3)
| equalish(e_1,X0) ) ).
cnf(u1904,negated_conjecture,
( ~ product(X0,e_2,e_4)
| ~ product(X0,X0,e_3)
| equalish(e_4,X0) ) ).
cnf(cycle6,axiom,
( ~ product(X0,e_1,X1)
| ~ cycle(X0,e_0)
| ~ greater(X1,X0) ) ).
cnf(u1893,axiom,
( ~ cycle(X0,e_0)
| ~ next(X0,e_4)
| ~ greater(X0,e_2) ) ).
cnf(e_4_greater_e_1,axiom,
greater(e_4,e_1) ).
cnf(u2201,negated_conjecture,
( ~ product(e_3,e_3,X0)
| ~ product(e_2,e_4,X0) ) ).
cnf(u335,axiom,
( ~ cycle(X0,X1)
| ~ next(X0,e_3)
| ~ greater(X1,e_0)
| ~ next(e_1,X2)
| equalish(X1,X2) ) ).
cnf(e_4_greater_e_3,axiom,
greater(e_4,e_3) ).
cnf(e_4_greater_e_2,axiom,
greater(e_4,e_2) ).
cnf(u2007,negated_conjecture,
( ~ product(X0,e_3,e_2)
| ~ product(X0,X0,e_4)
| equalish(e_2,X0) ) ).
cnf(e_3_greater_e_0,axiom,
greater(e_3,e_0) ).
cnf(u193,axiom,
~ next(e_4,e_4) ).
cnf(u166,axiom,
( ~ cycle(X1,X2)
| ~ cycle(X0,e_0)
| ~ next(X0,e_4)
| ~ greater(X0,X1)
| ~ greater(X2,e_0) ) ).
cnf(u2184,axiom,
( ~ product(e_3,e_4,X0)
| equalish(X0,e_2) ) ).
cnf(u1832,axiom,
( ~ product(X0,e_1,e_4)
| equalish(X0,e_3) ) ).
cnf(u2012,negated_conjecture,
( ~ product(e_2,X0,X1)
| ~ product(X1,X0,e_1)
| equalish(X0,e_3) ) ).
cnf(u2223,negated_conjecture,
~ product(e_1,e_1,e_2) ).
cnf(u2147,negated_conjecture,
( ~ product(e_2,X1,X2)
| ~ product(e_1,e_4,X0)
| ~ product(X2,X1,X0)
| equalish(X1,e_4) ) ).
cnf(u2032,negated_conjecture,
( ~ product(e_1,X0,X1)
| ~ product(X1,X0,e_4)
| equalish(X1,e_2) ) ).
cnf(u2186,axiom,
( ~ product(X0,e_4,e_2)
| equalish(X0,e_3) ) ).
cnf(u2149,negated_conjecture,
( ~ product(X0,e_4,e_2)
| ~ product(X0,X0,e_1)
| equalish(e_2,X0) ) ).
cnf(u2008,negated_conjecture,
( ~ product(e_2,X0,X1)
| ~ product(X1,X0,e_1)
| equalish(X1,e_4) ) ).
cnf(u1923,negated_conjecture,
( ~ product(e_3,X1,X2)
| ~ product(e_1,e_2,X0)
| ~ product(X2,X1,X0)
| equalish(X2,e_1) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP123-3.004 : TPTP v9.3.1. Released v1.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.38 % Computer : n011.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Sun Sep 27 09:20:00 UTC 2026
% 0.10/0.39 % CPUTime :
% 0.10/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.42 Running first-order theorem proving
% 0.10/0.42 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.26/1.75 % (2140269)Input is clausal, will run a generic CNF schedule.
% 5.26/1.75 % (2140278)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2142749652:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 5.26/1.75 % (2140278)Instruction limit reached!
% 5.26/1.75 % (2140278)------------------------------
% 5.26/1.75 % (2140278)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.26/1.75 % (2140278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.26/1.75 % (2140278)CaDiCaL version: 2.1.3
% 5.26/1.75 % (2140278)Termination reason: Instruction limit
% 5.26/1.75 % (2140278)Termination phase: Saturation
% 5.26/1.75 % (2140278)Time elapsed: 0.035 s
% 5.26/1.75 % (2140278)Peak memory usage: 88 MB
% 5.26/1.75 % (2140278)Instructions burned: 115 (million)
% 5.26/1.75 % (2140277)lrs+10_1_sil=8000:sp=occurrence:random_seed=556537234:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 5.26/1.75 % (2140274)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=2380642367:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 5.26/1.75 % (2140275)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1387841047:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 5.26/1.75 % (2140276)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2948150806:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 5.26/1.75 % (2140279)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=676501707:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 5.26/1.75 % (2140280)dis-21_1_sil=8000:lcm=predicate:random_seed=1734429265: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)
% 5.26/1.75 % (2140277)Refutation not found, incomplete strategy
% 5.26/1.75 % (2140277)------------------------------
% 5.26/1.75 % (2140277)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.26/1.75 % (2140277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.26/1.75 % (2140277)CaDiCaL version: 2.1.3
% 5.26/1.75 % (2140277)Termination reason: Refutation not found, incomplete strategy
% 5.26/1.75 % (2140277)Time elapsed: 0.001 s
% 5.26/1.75 % (2140277)Peak memory usage: 86 MB
% 5.26/1.75 % (2140279)Refutation not found, incomplete strategy
% 5.26/1.75 % (2140279)------------------------------
% 5.26/1.75 % (2140279)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.26/1.75 % (2140279)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.26/1.75 % (2140279)CaDiCaL version: 2.1.3
% 5.26/1.75 % (2140279)Termination reason: Refutation not found, incomplete strategy
% 5.26/1.75 % (2140279)Time elapsed: 0.054 s
% 5.26/1.75 % (2140279)Peak memory usage: 88 MB
% 5.26/1.75 % (2140279)Instructions burned: 82 (million)
% 5.26/1.75 % (2140280)Instruction limit reached!
% 5.26/1.75 % (2140280)------------------------------
% 5.26/1.75 % (2140280)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.26/1.75 % (2140280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.26/1.75 % (2140280)CaDiCaL version: 2.1.3
% 5.26/1.75 % (2140280)Termination reason: Instruction limit
% 5.26/1.75 % (2140280)Termination phase: Saturation
% 5.26/1.75 % (2140280)Time elapsed: 0.076 s
% 5.26/1.75 % (2140280)Peak memory usage: 89 MB
% 5.26/1.75 % (2140280)Instructions burned: 118 (million)
% 5.26/1.75 % (2140288)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=1010238332:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 5.26/1.75 % (2140288)Instruction limit reached!
% 5.26/1.75 % (2140288)------------------------------
% 5.26/1.75 % (2140288)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.26/1.75 % (2140288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.26/1.75 % (2140288)CaDiCaL version: 2.1.3
% 5.26/1.75 % (2140288)Termination reason: Instruction limit
% 5.26/1.75 % (2140288)Termination phase: Saturation
% 5.26/1.75 % (2140288)Time elapsed: 0.043 s
% 5.26/1.75 % (2140288)Peak memory usage: 88 MB
% 5.26/1.75 % (2140288)Instructions burned: 145 (million)
% 5.26/1.75 % (2140277)------------------------------
% 5.26/1.75 % (2140277)------------------------------
% 5.26/1.75 % (2140289)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=4102359256: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)
% 5.26/1.75 % (2140289)Refutation not found, incomplete strategy
% 5.26/1.75 % (2140289)------------------------------
% 5.26/1.75 % (2140289)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.26/1.75 % (2140289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.26/1.75 % (2140289)CaDiCaL version: 2.1.3
% 5.26/1.75 % (2140289)Termination reason: Refutation not found, incomplete strategy
% 5.26/1.75 % (2140289)Time elapsed: 0.003 s
% 5.26/1.75 % (2140289)Peak memory usage: 87 MB
% 5.26/1.75 % (2140289)Instructions burned: 3 (million)
% 5.26/1.75 % (2140279)------------------------------
% 5.26/1.75 % (2140279)------------------------------
% 5.26/1.75 % (2140291)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3299930475:st=4:i=219:sd=3:ss=axioms_2996 on theBenchmark for (2996ds/219Mi)
% 5.26/1.75 % (2140291)Instruction limit reached!
% 5.26/1.75 % (2140291)------------------------------
% 5.26/1.75 % (2140291)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.26/1.75 % (2140291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.26/1.75 % (2140291)CaDiCaL version: 2.1.3
% 5.26/1.75 % (2140291)Termination reason: Instruction limit
% 5.26/1.75 % (2140291)Termination phase: Saturation
% 5.26/1.75 % (2140291)Time elapsed: 0.061 s
% 5.26/1.75 % (2140291)Peak memory usage: 88 MB
% 5.26/1.75 % (2140291)Instructions burned: 222 (million)
% 5.26/1.75 % (2140293)lrs+10_64_to=lpo:sil=8000:random_seed=2097774230:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 5.26/1.75 % (2140293)First to succeed.
% 5.26/1.75 % (2140295)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=861746410:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 5.26/1.75 % (2140293)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2140269"
% 5.26/1.75 % (2140296)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=2196066990:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 5.26/1.75 % (2140295)Refutation not found, incomplete strategy
% 5.26/1.75 % (2140295)------------------------------
% 5.26/1.75 % (2140295)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.26/1.75 % (2140295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.26/1.75 % (2140295)CaDiCaL version: 2.1.3
% 5.26/1.75 % (2140295)Termination reason: Refutation not found, incomplete strategy
% 5.26/1.75 % (2140295)Time elapsed: 0.038 s
% 5.26/1.75 % (2140295)Peak memory usage: 88 MB
% 5.26/1.75 % (2140295)Instructions burned: 58 (million)
% 5.26/1.75 % (2140289)------------------------------
% 5.26/1.75 % (2140289)------------------------------
% 5.26/1.75 % (2140296)Instruction limit reached!
% 5.26/1.75 % (2140296)------------------------------
% 5.26/1.75 % (2140296)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.26/1.75 % (2140296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.26/1.75 % (2140296)CaDiCaL version: 2.1.3
% 5.26/1.75 % (2140296)Termination reason: Instruction limit
% 5.26/1.75 % (2140296)Termination phase: Saturation
% 5.26/1.75 % (2140296)Time elapsed: 0.049 s
% 5.26/1.75 % (2140296)Peak memory usage: 88 MB
% 5.26/1.75 % (2140296)Instructions burned: 158 (million)
% 5.26/1.75 % (2140275)Refutation not found, incomplete strategy
% 5.26/1.75 % (2140275)------------------------------
% 5.26/1.75 % (2140275)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.26/1.75 % (2140275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.26/1.75 % (2140275)CaDiCaL version: 2.1.3
% 5.26/1.75 % (2140275)Termination reason: Refutation not found, incomplete strategy
% 5.26/1.75 % (2140275)Time elapsed: 0.624 s
% 5.26/1.75 % (2140275)Peak memory usage: 125 MB
% 5.26/1.75 % (2140275)Instructions burned: 921 (million)
% 5.26/1.75 % (2140301)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=2310772236:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 5.26/1.75 % (2140301)Refutation not found, incomplete strategy
% 5.26/1.75 % (2140301)------------------------------
% 5.26/1.75 % (2140301)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.26/1.75 % (2140301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.26/1.75 % (2140301)CaDiCaL version: 2.1.3
% 5.26/1.75 % (2140301)Termination reason: Refutation not found, incomplete strategy
% 5.26/1.75 % (2140301)Time elapsed: 0.003 s
% 5.26/1.75 % (2140301)Peak memory usage: 88 MB
% 5.26/1.75 % (2140301)Instructions burned: 8 (million)
% 5.26/1.75 % (2140300)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=922642303:i=3394:sd=4:ss=included:sgt=64_2993 on theBenchmark for (2993ds/3394Mi)
% 5.26/1.75 % SZS status Satisfiable for theBenchmark
% 5.26/1.75 % SZS output start Saturation.
% See solution above
% 6.87/1.95 % SZS output start Definitions and Model Updates.
% 6.87/1.95 % SZS output end Definitions and Model Updates.
% 6.87/1.95 % (2140293)------------------------------
% 6.87/1.95 % (2140293)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.87/1.95 % (2140293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.87/1.95 % (2140293)CaDiCaL version: 2.1.3
% 6.87/1.95 % (2140293)Termination reason: Satisfiable
% 6.87/1.95 % (2140293)Time elapsed: 0.039 s
% 6.87/1.95 % (2140293)Peak memory usage: 88 MB
% 6.87/1.95 % (2140293)Instructions burned: 59 (million)
% 6.87/1.95 % (2140293)------------------------------
% 6.87/1.95 % (2140293)------------------------------
% 6.87/1.95 % (2140269)Success in time 0.893 s
% 6.87/1.95 % Vampire exiting
%------------------------------------------------------------------------------