%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP134-2.005 : TPTP v9.3.1. Released v1.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n006.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:03 AM UTC 2026
% Result : Satisfiable 4.26s 1.57s
% Output : Saturation 5.60s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u59,axiom,
product(e_5,e_1,e_5) ).
cnf(u62,axiom,
~ product(e_5,e_1,e_4) ).
cnf(u66,axiom,
~ product(e_5,e_1,e_3) ).
cnf(u70,axiom,
~ product(e_5,e_1,e_2) ).
cnf(u74,axiom,
~ product(e_5,e_1,e_1) ).
cnf(u79,axiom,
~ product(e_4,e_1,e_5) ).
cnf(u84,axiom,
product(e_4,e_1,e_4) ).
cnf(u87,axiom,
~ product(e_4,e_1,e_3) ).
cnf(u91,axiom,
~ product(e_4,e_1,e_2) ).
cnf(u95,axiom,
~ product(e_4,e_1,e_1) ).
cnf(u100,axiom,
~ product(e_3,e_1,e_5) ).
cnf(u104,axiom,
~ product(e_3,e_1,e_4) ).
cnf(u109,axiom,
product(e_3,e_1,e_3) ).
cnf(u112,axiom,
~ product(e_3,e_1,e_2) ).
cnf(u116,axiom,
~ product(e_3,e_1,e_1) ).
cnf(u121,axiom,
~ product(e_2,e_1,e_5) ).
cnf(u125,axiom,
~ product(e_2,e_1,e_4) ).
cnf(u129,axiom,
~ product(e_2,e_1,e_3) ).
cnf(u134,axiom,
product(e_2,e_1,e_2) ).
cnf(u137,axiom,
~ product(e_2,e_1,e_1) ).
cnf(u142,axiom,
~ product(e_1,e_1,e_5) ).
cnf(u146,axiom,
~ product(e_1,e_1,e_4) ).
cnf(u150,axiom,
~ product(e_1,e_1,e_3) ).
cnf(u154,axiom,
~ product(e_1,e_1,e_2) ).
cnf(u159,axiom,
product(e_1,e_1,e_1) ).
cnf(u205,axiom,
~ product(e_5,e_2,e_5) ).
cnf(u209,axiom,
~ product(e_5,e_2,e_4) ).
cnf(u218,axiom,
product(e_5,e_2,e_2) ).
cnf(u221,axiom,
~ product(e_5,e_2,e_1) ).
cnf(u226,axiom,
~ product(e_4,e_2,e_5) ).
cnf(u230,axiom,
~ product(e_4,e_2,e_4) ).
cnf(u234,axiom,
~ product(e_4,e_2,e_3) ).
cnf(u238,axiom,
~ product(e_4,e_2,e_2) ).
cnf(u243,axiom,
product(e_4,e_2,e_1) ).
cnf(u247,axiom,
~ product(e_3,e_2,e_5) ).
cnf(u252,axiom,
product(e_3,e_2,e_4) ).
cnf(u255,axiom,
~ product(e_3,e_2,e_3) ).
cnf(u259,axiom,
~ product(e_3,e_2,e_2) ).
cnf(u263,axiom,
~ product(e_3,e_2,e_1) ).
cnf(u268,axiom,
~ product(e_2,e_2,e_5) ).
cnf(u272,axiom,
~ product(e_2,e_2,e_4) ).
cnf(u277,axiom,
product(e_2,e_2,e_3) ).
cnf(u280,axiom,
~ product(e_2,e_2,e_2) ).
cnf(u284,axiom,
~ product(e_2,e_2,e_1) ).
cnf(u290,axiom,
product(e_1,e_2,e_5) ).
cnf(u293,axiom,
~ product(e_1,e_2,e_4) ).
cnf(u297,axiom,
~ product(e_1,e_2,e_3) ).
cnf(u301,axiom,
~ product(e_1,e_2,e_2) ).
cnf(u305,axiom,
~ product(e_1,e_2,e_1) ).
cnf(u471,axiom,
~ product(e_5,e_3,e_5) ).
cnf(u475,axiom,
~ product(e_5,e_3,e_4) ).
cnf(u479,axiom,
~ product(e_5,e_3,e_3) ).
cnf(u483,axiom,
~ product(e_5,e_3,e_2) ).
cnf(u488,axiom,
product(e_5,e_3,e_1) ).
cnf(u496,axiom,
~ product(e_4,e_3,e_4) ).
cnf(u501,axiom,
product(e_4,e_3,e_3) ).
cnf(u504,axiom,
~ product(e_4,e_3,e_2) ).
cnf(u508,axiom,
~ product(e_4,e_3,e_1) ).
cnf(u513,axiom,
~ product(e_3,e_3,e_5) ).
cnf(u517,axiom,
~ product(e_3,e_3,e_4) ).
cnf(u521,axiom,
~ product(e_3,e_3,e_3) ).
cnf(u526,axiom,
product(e_3,e_3,e_2) ).
cnf(u529,axiom,
~ product(e_3,e_3,e_1) ).
cnf(u535,axiom,
product(e_2,e_3,e_5) ).
cnf(u538,axiom,
~ product(e_2,e_3,e_4) ).
cnf(u542,axiom,
~ product(e_2,e_3,e_3) ).
cnf(u546,axiom,
~ product(e_2,e_3,e_2) ).
cnf(u550,axiom,
~ product(e_2,e_3,e_1) ).
cnf(u555,axiom,
~ product(e_1,e_3,e_5) ).
cnf(u560,axiom,
product(e_1,e_3,e_4) ).
cnf(u563,axiom,
~ product(e_1,e_3,e_3) ).
cnf(u567,axiom,
~ product(e_1,e_3,e_2) ).
cnf(u571,axiom,
~ product(e_1,e_3,e_1) ).
cnf(u721,axiom,
~ product(e_5,e_4,e_5) ).
cnf(u725,axiom,
~ product(e_5,e_4,e_4) ).
cnf(u730,axiom,
product(e_5,e_4,e_3) ).
cnf(u733,axiom,
~ product(e_5,e_4,e_2) ).
cnf(u737,axiom,
~ product(e_5,e_4,e_1) ).
cnf(u743,axiom,
product(e_4,e_4,e_5) ).
cnf(u746,axiom,
~ product(e_4,e_4,e_4) ).
cnf(u750,axiom,
~ product(e_4,e_4,e_3) ).
cnf(u754,axiom,
~ product(e_4,e_4,e_2) ).
cnf(u758,axiom,
~ product(e_4,e_4,e_1) ).
cnf(u763,axiom,
~ product(e_3,e_4,e_5) ).
cnf(u767,axiom,
~ product(e_3,e_4,e_4) ).
cnf(u771,axiom,
~ product(e_3,e_4,e_3) ).
cnf(u775,axiom,
~ product(e_3,e_4,e_2) ).
cnf(u780,axiom,
product(e_3,e_4,e_1) ).
cnf(u784,axiom,
~ product(e_2,e_4,e_5) ).
cnf(u789,axiom,
product(e_2,e_4,e_4) ).
cnf(u792,axiom,
~ product(e_2,e_4,e_3) ).
cnf(u796,axiom,
~ product(e_2,e_4,e_2) ).
cnf(u800,axiom,
~ product(e_2,e_4,e_1) ).
cnf(u805,axiom,
~ product(e_1,e_4,e_5) ).
cnf(u809,axiom,
~ product(e_1,e_4,e_4) ).
cnf(u813,axiom,
~ product(e_1,e_4,e_3) ).
cnf(u818,axiom,
product(e_1,e_4,e_2) ).
cnf(u821,axiom,
~ product(e_1,e_4,e_1) ).
cnf(u1000,axiom,
~ product(e_5,e_5,e_5) ).
cnf(u1005,axiom,
product(e_5,e_5,e_4) ).
cnf(u1008,axiom,
~ product(e_5,e_5,e_3) ).
cnf(u1012,axiom,
~ product(e_5,e_5,e_2) ).
cnf(u1016,axiom,
~ product(e_5,e_5,e_1) ).
cnf(u1022,axiom,
~ product(e_1,e_5,e_5) ).
cnf(u1026,axiom,
~ product(e_1,e_5,e_4) ).
cnf(u1031,axiom,
product(e_1,e_5,e_3) ).
cnf(u1034,axiom,
~ product(e_1,e_5,e_2) ).
cnf(u1038,axiom,
~ product(e_1,e_5,e_1) ).
cnf(u1044,negated_conjecture,
product(e_3,e_5,e_5) ).
cnf(u1047,negated_conjecture,
~ product(e_3,e_5,e_4) ).
cnf(u1051,negated_conjecture,
~ product(e_3,e_5,e_2) ).
cnf(u1055,negated_conjecture,
~ product(e_3,e_5,e_1) ).
cnf(u1112,negated_conjecture,
~ product(e_3,e_5,e_3) ).
cnf(u1615,axiom,
~ product(e_4,e_5,e_5) ).
cnf(u1619,axiom,
~ product(e_4,e_5,e_4) ).
cnf(u1623,axiom,
~ product(e_4,e_5,e_3) ).
cnf(u1628,axiom,
product(e_4,e_5,e_2) ).
cnf(u1631,axiom,
~ product(e_4,e_5,e_1) ).
cnf(u1226,negated_conjecture,
( ~ product(e_4,e_2,X0)
| product(X0,e_4,e_2) ) ).
cnf(u421,negated_conjecture,
equalish(e_1,e_1) ).
cnf(u2703,axiom,
~ next(e_5,e_2) ).
cnf(u594,axiom,
( ~ product(e_2,e_1,X0)
| equalish(X0,e_2) ) ).
cnf(u50,axiom,
( ~ group_element(X0)
| product(X0,e_5,e_1)
| product(X0,e_5,e_2)
| product(X0,e_5,e_3)
| product(X0,e_5,e_4)
| product(X0,e_5,e_5) ) ).
cnf(u3652,negated_conjecture,
( ~ product(e_3,e_1,X0)
| product(X0,e_4,e_1) ) ).
cnf(u3411,axiom,
( ~ product(e_5,X0,e_4)
| equalish(X0,e_5) ) ).
cnf(u3413,negated_conjecture,
( ~ product(e_5,e_5,X0)
| product(X0,e_4,e_5) ) ).
cnf(u3381,axiom,
( ~ product(e_4,X0,e_5)
| equalish(X0,e_4) ) ).
cnf(u3382,axiom,
( ~ product(e_4,e_4,X0)
| equalish(X0,e_5) ) ).
cnf(u3502,negated_conjecture,
( ~ product(e_3,e_5,X0)
| product(X0,e_1,e_5) ) ).
cnf(u3501,axiom,
( ~ product(e_5,e_3,X0)
| equalish(X0,e_1) ) ).
cnf(u3562,axiom,
( ~ product(X0,e_4,e_2)
| equalish(X0,e_1) ) ).
cnf(u3509,axiom,
( ~ product(X0,e_5,e_3)
| equalish(X0,e_1) ) ).
cnf(u3454,axiom,
( ~ greater(e_1,X0)
| ~ next(e_1,X0) ) ).
cnf(u3649,axiom,
( ~ product(X0,e_3,e_4)
| equalish(X0,e_1) ) ).
cnf(u3249,axiom,
( ~ product(e_2,e_2,X0)
| equalish(X0,e_3) ) ).
cnf(u1854,axiom,
~ next(e_4,e_2) ).
cnf(u3383,negated_conjecture,
( ~ product(e_4,e_4,X0)
| product(X0,e_5,e_4) ) ).
cnf(u3156,axiom,
~ next(e_3,e_1) ).
cnf(u49,axiom,
( ~ group_element(X0)
| product(X0,e_4,e_1)
| product(X0,e_4,e_2)
| product(X0,e_4,e_3)
| product(X0,e_4,e_4)
| product(X0,e_4,e_5) ) ).
cnf(product_right_cancellation,axiom,
( ~ product(X0,X3,X2)
| ~ product(X0,X1,X2)
| equalish(X1,X3) ) ).
cnf(u3565,negated_conjecture,
( ~ product(e_4,e_1,X0)
| product(X0,e_2,e_1) ) ).
cnf(u46,axiom,
( ~ group_element(X0)
| product(X0,e_1,e_1)
| product(X0,e_1,e_2)
| product(X0,e_1,e_3)
| product(X0,e_1,e_4)
| product(X0,e_1,e_5) ) ).
cnf(u3456,axiom,
( ~ product(e_1,X0,e_1)
| equalish(X0,e_1) ) ).
cnf(qg4,negated_conjecture,
( ~ product(X1,X0,X3)
| ~ product(X0,X1,X2)
| product(X2,X3,X1) ) ).
cnf(e_3_is_not_e_5,axiom,
~ equalish(e_3,e_5) ).
cnf(e_5_is_not_e_3,axiom,
~ equalish(e_5,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(e_2_is_not_e_5,axiom,
~ equalish(e_2,e_5) ).
cnf(element_4,axiom,
group_element(e_4) ).
cnf(u629,negated_conjecture,
( ~ product(e_2,e_5,X0)
| product(X0,e_2,e_5) ) ).
cnf(e_1_is_not_e_3,axiom,
~ equalish(e_1,e_3) ).
cnf(u1223,axiom,
( ~ product(X0,e_4,e_4)
| equalish(X0,e_2) ) ).
cnf(e_1_is_not_e_2,axiom,
~ equalish(e_1,e_2) ).
cnf(u3499,axiom,
( ~ product(X0,e_3,e_1)
| equalish(X0,e_5) ) ).
cnf(u3516,axiom,
( ~ product(e_4,X0,e_2)
| equalish(X0,e_5) ) ).
cnf(e_5_greater_e_1,axiom,
greater(e_5,e_1) ).
cnf(no_redundancy,axiom,
( ~ product(X0,e_1,X1)
| ~ next(X0,X2)
| ~ greater(X1,X2) ) ).
cnf(u3564,axiom,
( ~ product(e_1,e_4,X0)
| equalish(X0,e_2) ) ).
cnf(e_2_then_e_3,axiom,
next(e_2,e_3) ).
cnf(u3515,axiom,
( ~ product(X0,e_5,e_2)
| equalish(X0,e_4) ) ).
cnf(e_1_then_e_2,axiom,
next(e_1,e_2) ).
cnf(u3308,axiom,
( ~ product(e_3,e_3,X0)
| equalish(X0,e_2) ) ).
cnf(u3542,axiom,
( ~ product(e_4,e_2,X0)
| equalish(X0,e_1) ) ).
cnf(u3269,negated_conjecture,
( ~ product(e_3,X0,e_5)
| equalish(X0,e_5) ) ).
cnf(u3594,axiom,
( ~ product(e_3,X0,e_3)
| equalish(X0,e_1) ) ).
cnf(u586,negated_conjecture,
( ~ product(e_5,e_2,X0)
| product(X0,e_1,e_2) ) ).
cnf(u585,negated_conjecture,
( ~ product(e_2,e_5,X0)
| equalish(X0,e_1) ) ).
cnf(u2704,axiom,
~ next(e_5,e_3) ).
cnf(u3412,axiom,
( ~ product(e_5,e_5,X0)
| equalish(X0,e_4) ) ).
cnf(u2705,axiom,
~ next(e_5,e_4) ).
cnf(u3650,axiom,
( ~ product(e_1,X0,e_4)
| equalish(X0,e_3) ) ).
cnf(u3536,negated_conjecture,
( ~ product(e_1,e_4,X0)
| product(X0,e_4,e_4) ) ).
cnf(u3410,axiom,
( ~ product(X0,e_5,e_4)
| equalish(X0,e_5) ) ).
cnf(u3247,axiom,
( ~ product(X0,e_2,e_3)
| equalish(X0,e_2) ) ).
cnf(e_4_then_e_5,axiom,
next(e_4,e_5) ).
cnf(u583,negated_conjecture,
( ~ product(X0,e_5,e_1)
| equalish(X0,e_2) ) ).
cnf(u3510,axiom,
( ~ product(e_1,X0,e_3)
| equalish(X0,e_5) ) ).
cnf(u592,axiom,
( ~ product(X0,e_1,e_2)
| equalish(X0,e_2) ) ).
cnf(u3593,axiom,
( ~ product(X0,e_1,e_3)
| equalish(X0,e_3) ) ).
cnf(u3487,axiom,
( ~ greater(e_5,X0)
| ~ next(e_5,X0) ) ).
cnf(u1853,axiom,
~ next(e_4,e_1) ).
cnf(u3592,axiom,
( ~ greater(e_3,X0)
| ~ next(e_3,X0) ) ).
cnf(e_5_is_not_e_4,axiom,
~ equalish(e_5,e_4) ).
cnf(u3270,negated_conjecture,
( ~ product(e_3,e_5,X0)
| equalish(X0,e_5) ) ).
cnf(u3490,axiom,
( ~ product(e_5,e_1,X0)
| equalish(X0,e_5) ) ).
cnf(u47,axiom,
( ~ group_element(X0)
| product(X0,e_2,e_1)
| product(X0,e_2,e_2)
| product(X0,e_2,e_3)
| product(X0,e_2,e_4)
| product(X0,e_2,e_5) ) ).
cnf(u3342,axiom,
( ~ product(e_2,X0,e_5)
| equalish(X0,e_3) ) ).
cnf(u355,negated_conjecture,
( ~ product(e_2,e_1,X0)
| product(X0,e_5,e_1) ) ).
cnf(e_4_is_not_e_2,axiom,
~ equalish(e_4,e_2) ).
cnf(u3644,axiom,
( ~ product(X0,e_3,e_3)
| equalish(X0,e_4) ) ).
cnf(u3534,axiom,
( ~ product(e_4,X0,e_4)
| equalish(X0,e_1) ) ).
cnf(u3533,axiom,
( ~ product(X0,e_1,e_4)
| equalish(X0,e_4) ) ).
cnf(u3595,axiom,
( ~ product(e_3,e_1,X0)
| equalish(X0,e_3) ) ).
cnf(u3505,axiom,
( ~ product(e_5,X0,e_3)
| equalish(X0,e_4) ) ).
cnf(u1852,axiom,
~ next(e_2,e_1) ).
cnf(u3647,negated_conjecture,
( ~ product(e_3,e_4,X0)
| product(X0,e_3,e_4) ) ).
cnf(u3343,axiom,
( ~ product(e_2,e_3,X0)
| equalish(X0,e_5) ) ).
cnf(u1091,negated_conjecture,
equalish(e_3,e_3) ).
cnf(u3455,axiom,
( ~ product(X0,e_1,e_1)
| equalish(X0,e_1) ) ).
cnf(u3130,axiom,
equalish(e_4,e_4) ).
cnf(u3250,negated_conjecture,
( ~ product(e_2,e_2,X0)
| product(X0,e_3,e_2) ) ).
cnf(e_4_is_not_e_1,axiom,
~ equalish(e_4,e_1) ).
cnf(u3532,axiom,
( ~ greater(e_4,X0)
| ~ next(e_4,X0) ) ).
cnf(u399,negated_conjecture,
product(e_2,e_5,e_1) ).
cnf(u3596,negated_conjecture,
( ~ product(e_1,e_3,X0)
| product(X0,e_3,e_3) ) ).
cnf(e_4_is_not_e_5,axiom,
~ equalish(e_4,e_5) ).
cnf(u420,negated_conjecture,
equalish(e_5,e_5) ).
cnf(e_2_is_not_e_4,axiom,
~ equalish(e_2,e_4) ).
cnf(e_3_is_not_e_2,axiom,
~ equalish(e_3,e_2) ).
cnf(u3540,axiom,
( ~ product(X0,e_2,e_1)
| equalish(X0,e_4) ) ).
cnf(e_3_is_not_e_1,axiom,
~ equalish(e_3,e_1) ).
cnf(element_1,axiom,
group_element(e_1) ).
cnf(e_1_is_not_e_4,axiom,
~ equalish(e_1,e_4) ).
cnf(e_4_greater_e_2,axiom,
greater(e_4,e_2) ).
cnf(u3506,axiom,
( ~ product(e_5,e_4,X0)
| equalish(X0,e_3) ) ).
cnf(e_3_greater_e_2,axiom,
greater(e_3,e_2) ).
cnf(e_4_greater_e_3,axiom,
greater(e_4,e_3) ).
cnf(e_3_then_e_4,axiom,
next(e_3,e_4) ).
cnf(e_2_greater_e_1,axiom,
greater(e_2,e_1) ).
cnf(u3307,axiom,
( ~ product(e_3,X0,e_2)
| equalish(X0,e_3) ) ).
cnf(e_3_greater_e_1,axiom,
greater(e_3,e_1) ).
cnf(u3157,axiom,
~ next(e_3,e_2) ).
cnf(u3658,negated_conjecture,
( ~ product(e_4,e_3,X0)
| product(X0,e_1,e_3) ) ).
cnf(u3309,negated_conjecture,
( ~ product(e_3,e_3,X0)
| product(X0,e_2,e_3) ) ).
cnf(u3500,axiom,
( ~ product(e_5,X0,e_1)
| equalish(X0,e_3) ) ).
cnf(u3344,negated_conjecture,
( ~ product(e_3,e_2,X0)
| product(X0,e_5,e_2) ) ).
cnf(u593,axiom,
( ~ product(e_2,X0,e_2)
| equalish(X0,e_1) ) ).
cnf(u3341,axiom,
( ~ product(X0,e_3,e_5)
| equalish(X0,e_2) ) ).
cnf(u1225,axiom,
( ~ product(e_2,e_4,X0)
| equalish(X0,e_4) ) ).
cnf(u3646,axiom,
( ~ product(e_4,e_3,X0)
| equalish(X0,e_3) ) ).
cnf(u3458,negated_conjecture,
( ~ product(e_1,e_1,X0)
| product(X0,e_1,e_1) ) ).
cnf(u3457,axiom,
( ~ product(e_1,e_1,X0)
| equalish(X0,e_1) ) ).
cnf(u3563,axiom,
( ~ product(e_1,X0,e_2)
| equalish(X0,e_4) ) ).
cnf(u3655,axiom,
( ~ product(X0,e_4,e_1)
| equalish(X0,e_3) ) ).
cnf(u1224,axiom,
( ~ product(e_2,X0,e_4)
| equalish(X0,e_4) ) ).
cnf(u3507,negated_conjecture,
( ~ product(e_4,e_5,X0)
| product(X0,e_3,e_5) ) ).
cnf(u3543,negated_conjecture,
( ~ product(e_2,e_4,X0)
| product(X0,e_1,e_4) ) ).
cnf(u3248,axiom,
( ~ product(e_2,X0,e_3)
| equalish(X0,e_2) ) ).
cnf(u3268,negated_conjecture,
( ~ product(X0,e_5,e_5)
| equalish(X0,e_3) ) ).
cnf(u3651,axiom,
( ~ product(e_1,e_3,X0)
| equalish(X0,e_4) ) ).
cnf(u3518,negated_conjecture,
( ~ product(e_5,e_4,X0)
| product(X0,e_2,e_4) ) ).
cnf(u595,negated_conjecture,
( ~ product(e_1,e_2,X0)
| product(X0,e_2,e_2) ) ).
cnf(u1855,axiom,
~ next(e_4,e_3) ).
cnf(u628,axiom,
( ~ product(e_5,e_2,X0)
| equalish(X0,e_2) ) ).
cnf(u3495,axiom,
( ~ product(e_3,e_2,X0)
| equalish(X0,e_4) ) ).
cnf(u584,negated_conjecture,
( ~ product(e_2,X0,e_1)
| equalish(X0,e_5) ) ).
cnf(u591,axiom,
( ~ greater(e_2,X0)
| ~ next(e_2,X0) ) ).
cnf(u352,axiom,
( ~ product(X0,e_2,e_5)
| equalish(X0,e_1) ) ).
cnf(u3488,axiom,
( ~ product(X0,e_1,e_5)
| equalish(X0,e_5) ) ).
cnf(u3535,axiom,
( ~ product(e_4,e_1,X0)
| equalish(X0,e_4) ) ).
cnf(u3494,axiom,
( ~ product(e_3,X0,e_4)
| equalish(X0,e_2) ) ).
cnf(u48,axiom,
( ~ group_element(X0)
| product(X0,e_3,e_1)
| product(X0,e_3,e_2)
| product(X0,e_3,e_3)
| product(X0,e_3,e_4)
| product(X0,e_3,e_5) ) ).
cnf(product_total_function2,axiom,
( ~ product(X0,X1,X3)
| ~ product(X0,X1,X2)
| equalish(X2,X3) ) ).
cnf(u3517,axiom,
( ~ product(e_4,e_5,X0)
| equalish(X0,e_2) ) ).
cnf(product_total_function1,axiom,
( ~ group_element(X1)
| ~ group_element(X0)
| product(X0,X1,e_1)
| product(X0,X1,e_2)
| product(X0,X1,e_3)
| product(X0,X1,e_4)
| product(X0,X1,e_5) ) ).
cnf(product_left_cancellation,axiom,
( ~ product(X3,X1,X2)
| ~ product(X0,X1,X2)
| equalish(X0,X3) ) ).
cnf(e_4_is_not_e_3,axiom,
~ equalish(e_4,e_3) ).
cnf(e_5_is_not_e_2,axiom,
~ equalish(e_5,e_2) ).
cnf(u2702,axiom,
~ next(e_5,e_1) ).
cnf(e_5_is_not_e_1,axiom,
~ equalish(e_5,e_1) ).
cnf(u3657,axiom,
( ~ product(e_3,e_4,X0)
| equalish(X0,e_1) ) ).
cnf(e_1_is_not_e_5,axiom,
~ equalish(e_1,e_5) ).
cnf(u3491,negated_conjecture,
( ~ product(e_1,e_5,X0)
| product(X0,e_5,e_5) ) ).
cnf(u626,axiom,
( ~ product(X0,e_2,e_2)
| equalish(X0,e_5) ) ).
cnf(e_3_is_not_e_4,axiom,
~ equalish(e_3,e_4) ).
cnf(u353,axiom,
( ~ product(e_1,X0,e_5)
| equalish(X0,e_2) ) ).
cnf(element_3,axiom,
group_element(e_3) ).
cnf(element_2,axiom,
group_element(e_2) ).
cnf(u3496,negated_conjecture,
( ~ product(e_2,e_3,X0)
| product(X0,e_4,e_3) ) ).
cnf(u3489,axiom,
( ~ product(e_5,X0,e_5)
| equalish(X0,e_1) ) ).
cnf(u3511,axiom,
( ~ product(e_1,e_5,X0)
| equalish(X0,e_3) ) ).
cnf(u627,axiom,
( ~ product(e_5,X0,e_2)
| equalish(X0,e_2) ) ).
cnf(u3541,axiom,
( ~ product(e_4,X0,e_1)
| equalish(X0,e_2) ) ).
cnf(u3380,axiom,
( ~ product(X0,e_4,e_5)
| equalish(X0,e_4) ) ).
cnf(u3306,axiom,
( ~ product(X0,e_3,e_2)
| equalish(X0,e_3) ) ).
cnf(u3493,axiom,
( ~ product(X0,e_2,e_4)
| equalish(X0,e_3) ) ).
cnf(element_5,axiom,
group_element(e_5) ).
cnf(e_5_greater_e_2,axiom,
greater(e_5,e_2) ).
cnf(e_5_greater_e_4,axiom,
greater(e_5,e_4) ).
cnf(e_5_greater_e_3,axiom,
greater(e_5,e_3) ).
cnf(u354,axiom,
( ~ product(e_1,e_2,X0)
| equalish(X0,e_5) ) ).
cnf(e_4_greater_e_1,axiom,
greater(e_4,e_1) ).
cnf(u3504,axiom,
( ~ product(X0,e_4,e_3)
| equalish(X0,e_5) ) ).
cnf(u3656,axiom,
( ~ product(e_3,X0,e_1)
| equalish(X0,e_4) ) ).
cnf(u3512,negated_conjecture,
( ~ product(e_5,e_1,X0)
| product(X0,e_3,e_1) ) ).
cnf(u3645,axiom,
( ~ product(e_4,X0,e_3)
| equalish(X0,e_3) ) ).
cnf(u3271,negated_conjecture,
( ~ product(e_5,e_3,X0)
| product(X0,e_5,e_3) ) ).
cnf(u419,negated_conjecture,
equalish(e_2,e_2) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP134-2.005 : TPTP v9.3.1. Released v1.2.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.38 % Computer : n006.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Sun Sep 27 09:31:26 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.42 Running first-order theorem proving
% 0.11/0.42 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
% 4.26/1.57 % (2733023)Input is clausal, will run a generic CNF schedule.
% 4.26/1.57 % (2733032)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2351921288:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 4.26/1.57 % (2733032)Instruction limit reached!
% 4.26/1.57 % (2733032)------------------------------
% 4.26/1.57 % (2733032)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.26/1.57 % (2733032)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.26/1.57 % (2733032)CaDiCaL version: 2.1.3
% 4.26/1.57 % (2733032)Termination reason: Instruction limit
% 4.26/1.57 % (2733032)Termination phase: Saturation
% 4.26/1.57 % (2733032)Time elapsed: 0.033 s
% 4.26/1.57 % (2733032)Peak memory usage: 88 MB
% 4.26/1.57 % (2733032)Instructions burned: 115 (million)
% 4.26/1.57 % (2733028)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=4190714199:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 4.26/1.57 % (2733034)dis-21_1_sil=8000:lcm=predicate:random_seed=26830739: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)
% 4.26/1.57 % (2733031)lrs+10_1_sil=8000:sp=occurrence:random_seed=2746540152:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 4.26/1.57 % (2733029)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2104351831:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 4.26/1.57 % (2733030)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3737275016:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 4.26/1.57 % (2733033)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=455460024:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 4.26/1.57 % (2733031)Instruction limit reached!
% 4.26/1.57 % (2733031)------------------------------
% 4.26/1.57 % (2733031)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.26/1.57 % (2733031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.26/1.57 % (2733031)CaDiCaL version: 2.1.3
% 4.26/1.57 % (2733031)Termination reason: Instruction limit
% 4.26/1.57 % (2733031)Termination phase: Saturation
% 4.26/1.57 % (2733031)Time elapsed: 0.058 s
% 4.26/1.57 % (2733031)Peak memory usage: 88 MB
% 4.26/1.57 % (2733031)Instructions burned: 108 (million)
% 4.26/1.57 % (2733034)Instruction limit reached!
% 4.26/1.57 % (2733034)------------------------------
% 4.26/1.57 % (2733034)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.26/1.57 % (2733034)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.26/1.57 % (2733034)CaDiCaL version: 2.1.3
% 4.26/1.57 % (2733034)Termination reason: Instruction limit
% 4.26/1.57 % (2733034)Termination phase: Saturation
% 4.26/1.57 % (2733034)Time elapsed: 0.076 s
% 4.26/1.57 % (2733034)Peak memory usage: 89 MB
% 4.26/1.57 % (2733034)Instructions burned: 117 (million)
% 4.26/1.57 % (2733036)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=3208171897:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 4.26/1.57 % (2733033)Instruction limit reached!
% 4.26/1.57 % (2733033)------------------------------
% 4.26/1.57 % (2733033)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.26/1.57 % (2733033)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.26/1.57 % (2733033)CaDiCaL version: 2.1.3
% 4.26/1.57 % (2733033)Termination reason: Instruction limit
% 4.26/1.57 % (2733033)Termination phase: Saturation
% 4.26/1.57 % (2733033)Time elapsed: 0.108 s
% 4.26/1.57 % (2733033)Peak memory usage: 89 MB
% 4.26/1.57 % (2733033)Instructions burned: 182 (million)
% 4.26/1.57 % (2733036)Instruction limit reached!
% 4.26/1.57 % (2733036)------------------------------
% 4.26/1.57 % (2733036)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.26/1.57 % (2733036)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.26/1.57 % (2733036)CaDiCaL version: 2.1.3
% 4.26/1.57 % (2733036)Termination reason: Instruction limit
% 4.26/1.57 % (2733036)Termination phase: Saturation
% 4.26/1.57 % (2733036)Time elapsed: 0.041 s
% 4.26/1.57 % (2733036)Peak memory usage: 89 MB
% 4.26/1.57 % (2733036)Instructions burned: 145 (million)
% 4.26/1.57 % (2733043)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=873671579: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)
% 4.26/1.57 % (2733043)Refutation not found, incomplete strategy
% 4.26/1.57 % (2733043)------------------------------
% 4.26/1.57 % (2733043)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.26/1.57 % (2733043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.26/1.57 % (2733043)CaDiCaL version: 2.1.3
% 4.26/1.57 % (2733043)Termination reason: Refutation not found, incomplete strategy
% 4.26/1.57 % (2733043)Time elapsed: 0.002 s
% 4.26/1.57 % (2733043)Peak memory usage: 87 MB
% 4.26/1.57 % (2733043)Instructions burned: 1 (million)
% 4.26/1.57 % (2733045)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3829990716:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 4.26/1.57 % (2733047)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=2551963908:avsq=on:i=194:fgj=on:bd=preordered_2997 on theBenchmark for (2997ds/194Mi)
% 4.26/1.57 % (2733047)Instruction limit reached!
% 4.26/1.57 % (2733047)------------------------------
% 4.26/1.57 % (2733047)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.26/1.57 % (2733047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.26/1.57 % (2733047)CaDiCaL version: 2.1.3
% 4.26/1.57 % (2733047)Termination reason: Instruction limit
% 4.26/1.57 % (2733047)Termination phase: Saturation
% 4.26/1.57 % (2733047)Time elapsed: 0.039 s
% 4.26/1.57 % (2733047)Peak memory usage: 87 MB
% 4.26/1.57 % (2733047)Instructions burned: 197 (million)
% 4.26/1.57 % (2733046)lrs+10_64_to=lpo:sil=8000:random_seed=4127001649:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 4.26/1.57 % (2733046)First to succeed.
% 4.26/1.57 % (2733046)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2733023"
% 4.26/1.57 % (2733045)Instruction limit reached!
% 4.26/1.57 % (2733045)------------------------------
% 4.26/1.57 % (2733045)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.26/1.57 % (2733045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.26/1.57 % (2733045)CaDiCaL version: 2.1.3
% 4.26/1.57 % (2733045)Termination reason: Instruction limit
% 4.26/1.57 % (2733045)Termination phase: Saturation
% 4.26/1.57 % (2733045)Time elapsed: 0.123 s
% 4.26/1.57 % (2733045)Peak memory usage: 88 MB
% 4.26/1.57 % (2733045)Instructions burned: 220 (million)
% 4.26/1.57 % (2733052)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=2188744259:i=157:gtg=all_2996 on theBenchmark for (2996ds/157Mi)
% 4.26/1.57 % (2733052)Instruction limit reached!
% 4.26/1.57 % (2733052)------------------------------
% 4.26/1.57 % (2733052)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.26/1.57 % (2733052)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.26/1.57 % (2733052)CaDiCaL version: 2.1.3
% 4.26/1.57 % (2733052)Termination reason: Instruction limit
% 4.26/1.57 % (2733052)Termination phase: Saturation
% 4.26/1.57 % (2733052)Time elapsed: 0.042 s
% 4.26/1.57 % (2733052)Peak memory usage: 88 MB
% 4.26/1.57 % (2733052)Instructions burned: 158 (million)
% 4.26/1.57 % (2733043)------------------------------
% 4.26/1.57 % (2733043)------------------------------
% 4.26/1.57 % (2733053)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=2897644838:i=3394:sd=4:ss=included:sgt=64_2995 on theBenchmark for (2995ds/3394Mi)
% 4.26/1.57 % (2733055)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=2836533087:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2994 on theBenchmark for (2994ds/106Mi)
% 4.26/1.57 % (2733055)Refutation not found, incomplete strategy
% 4.26/1.57 % (2733055)------------------------------
% 4.26/1.57 % (2733055)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.26/1.57 % (2733055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.26/1.57 % (2733055)CaDiCaL version: 2.1.3
% 4.26/1.57 % (2733055)Termination reason: Refutation not found, incomplete strategy
% 4.26/1.57 % (2733055)Time elapsed: 0.001 s
% 4.26/1.57 % (2733055)Peak memory usage: 87 MB
% 4.26/1.57 % (2733055)Instructions burned: 2 (million)
% 4.26/1.57 % SZS status Satisfiable for theBenchmark
% 4.26/1.57 % SZS output start Saturation.
% See solution above
% 5.60/1.76 % SZS output start Definitions and Model Updates.
% 5.60/1.76 % SZS output end Definitions and Model Updates.
% 5.60/1.76 % (2733046)------------------------------
% 5.60/1.76 % (2733046)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.60/1.76 % (2733046)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.60/1.76 % (2733046)CaDiCaL version: 2.1.3
% 5.60/1.76 % (2733046)Termination reason: Satisfiable
% 5.60/1.76 % (2733046)Time elapsed: 0.065 s
% 5.60/1.76 % (2733046)Peak memory usage: 88 MB
% 5.60/1.76 % (2733046)Instructions burned: 104 (million)
% 5.60/1.76 % (2733046)------------------------------
% 5.60/1.76 % (2733046)------------------------------
% 5.60/1.76 % (2733023)Success in time 0.709 s
% 5.60/1.76 % Vampire exiting
%------------------------------------------------------------------------------