%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP127-4.005 : TPTP v9.3.1. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n001.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:57 AM UTC 2026
% Result : Satisfiable 5.11s 1.46s
% Output : Saturation 6.40s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u60,axiom,
~ product(e_5,e_5,e_1) ).
cnf(u64,axiom,
~ product(e_4,e_5,e_1) ).
cnf(u68,axiom,
~ product(e_3,e_5,e_1) ).
cnf(u73,axiom,
product(e_2,e_5,e_1) ).
cnf(u76,axiom,
~ product(e_1,e_5,e_1) ).
cnf(u81,axiom,
~ product(e_5,e_4,e_1) ).
cnf(u85,axiom,
~ product(e_4,e_4,e_1) ).
cnf(u90,axiom,
product(e_3,e_4,e_1) ).
cnf(u93,axiom,
~ product(e_2,e_4,e_1) ).
cnf(u97,axiom,
~ product(e_1,e_4,e_1) ).
cnf(u103,axiom,
product(e_5,e_3,e_1) ).
cnf(u106,axiom,
~ product(e_4,e_3,e_1) ).
cnf(u110,axiom,
~ product(e_3,e_3,e_1) ).
cnf(u114,axiom,
~ product(e_2,e_3,e_1) ).
cnf(u118,axiom,
~ product(e_1,e_3,e_1) ).
cnf(u123,axiom,
~ product(e_5,e_2,e_1) ).
cnf(u128,axiom,
product(e_4,e_2,e_1) ).
cnf(u131,axiom,
~ product(e_3,e_2,e_1) ).
cnf(u267,axiom,
~ product(e_5,e_5,e_2) ).
cnf(u271,axiom,
~ product(e_4,e_5,e_2) ).
cnf(u276,axiom,
product(e_3,e_5,e_2) ).
cnf(u279,axiom,
~ product(e_2,e_5,e_2) ).
cnf(u283,axiom,
~ product(e_1,e_5,e_2) ).
cnf(u289,axiom,
product(e_5,e_4,e_2) ).
cnf(u292,axiom,
~ product(e_4,e_4,e_2) ).
cnf(u300,axiom,
~ product(e_2,e_4,e_2) ).
cnf(u304,axiom,
~ product(e_1,e_4,e_2) ).
cnf(u309,axiom,
~ product(e_5,e_3,e_2) ).
cnf(u313,axiom,
~ product(e_4,e_3,e_2) ).
cnf(u317,axiom,
~ product(e_3,e_3,e_2) ).
cnf(u321,axiom,
~ product(e_2,e_3,e_2) ).
cnf(u326,axiom,
product(e_1,e_3,e_2) ).
cnf(u330,axiom,
~ product(e_5,e_1,e_2) ).
cnf(u335,axiom,
product(e_4,e_1,e_2) ).
cnf(u573,axiom,
~ product(e_5,e_4,e_3) ).
cnf(u581,axiom,
~ product(e_3,e_4,e_3) ).
cnf(u586,axiom,
product(e_2,e_4,e_3) ).
cnf(u594,axiom,
~ product(e_5,e_2,e_3) ).
cnf(u598,axiom,
~ product(e_4,e_2,e_3) ).
cnf(u602,axiom,
~ product(e_3,e_2,e_3) ).
cnf(u606,axiom,
~ product(e_2,e_2,e_3) ).
cnf(u611,axiom,
product(e_1,e_2,e_3) ).
cnf(u616,axiom,
product(e_5,e_1,e_3) ).
cnf(u619,axiom,
~ product(e_4,e_1,e_3) ).
cnf(u686,axiom,
~ product(e_5,e_5,e_3) ).
cnf(u691,axiom,
product(e_4,e_5,e_3) ).
cnf(u702,axiom,
~ product(e_1,e_5,e_3) ).
cnf(u814,axiom,
~ product(e_5,e_3,e_4) ).
cnf(u827,axiom,
product(e_2,e_3,e_4) ).
cnf(u836,axiom,
product(e_5,e_2,e_4) ).
cnf(u839,axiom,
~ product(e_4,e_2,e_4) ).
cnf(u868,axiom,
~ product(e_4,e_5,e_4) ).
cnf(u876,axiom,
~ product(e_2,e_5,e_4) ).
cnf(u881,axiom,
product(e_1,e_5,e_4) ).
cnf(u943,axiom,
product(e_3,e_1,e_4) ).
cnf(u946,axiom,
~ product(e_2,e_1,e_4) ).
cnf(u1048,axiom,
~ product(e_5,e_3,e_5) ).
cnf(u1053,axiom,
product(e_4,e_3,e_5) ).
cnf(u1078,axiom,
product(e_3,e_2,e_5) ).
cnf(u1085,axiom,
~ product(e_1,e_2,e_5) ).
cnf(u1090,axiom,
~ product(e_5,e_1,e_5) ).
cnf(u1094,axiom,
~ product(e_4,e_1,e_5) ).
cnf(u1103,axiom,
product(e_2,e_1,e_5) ).
cnf(u1009,negated_conjecture,
( ~ product(X0,e_5,e_3)
| product(e_5,e_2,X0) ) ).
cnf(u1483,axiom,
( ~ product(X0,e_5,e_4)
| equalish(X0,e_1) ) ).
cnf(u50,axiom,
( ~ group_element(X0)
| product(e_1,X0,e_3)
| product(e_2,X0,e_3)
| product(e_3,X0,e_3)
| product(e_4,X0,e_3)
| product(e_5,X0,e_3) ) ).
cnf(u1485,axiom,
( ~ product(e_1,e_5,X0)
| equalish(X0,e_4) ) ).
cnf(u1547,axiom,
( ~ product(e_3,X0,e_5)
| equalish(X0,e_2) ) ).
cnf(u755,negated_conjecture,
( ~ product(e_5,e_1,X0)
| product(X0,e_5,e_2) ) ).
cnf(u1005,axiom,
( ~ product(e_3,X0,e_2)
| equalish(X0,e_5) ) ).
cnf(u1158,axiom,
( ~ product(e_2,e_4,X0)
| equalish(X0,e_3) ) ).
cnf(u1157,axiom,
( ~ product(e_2,X0,e_3)
| equalish(X0,e_4) ) ).
cnf(u1348,axiom,
( ~ product(e_5,X0,e_1)
| equalish(X0,e_3) ) ).
cnf(u751,axiom,
( ~ product(X0,e_5,e_1)
| equalish(X0,e_2) ) ).
cnf(u1160,negated_conjecture,
( ~ product(e_4,e_3,X0)
| product(X0,e_4,e_2) ) ).
cnf(u1437,negated_conjecture,
( ~ product(e_2,X0,e_5)
| product(e_4,e_2,X0) ) ).
cnf(u957,negated_conjecture,
( ~ product(e_4,X0,e_1)
| product(e_5,e_4,X0) ) ).
cnf(u1110,axiom,
( ~ product(X0,e_1,e_2)
| equalish(X0,e_4) ) ).
cnf(u1112,axiom,
( ~ product(e_4,e_1,X0)
| equalish(X0,e_2) ) ).
cnf(u1007,negated_conjecture,
( ~ product(e_5,X0,e_3)
| product(e_2,e_5,X0) ) ).
cnf(u406,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(u1535,axiom,
( ~ product(e_4,X0,e_5)
| equalish(X0,e_3) ) ).
cnf(u1538,negated_conjecture,
( ~ product(e_3,e_5,X0)
| product(X0,e_3,e_4) ) ).
cnf(u1495,axiom,
( ~ product(e_3,X0,e_4)
| equalish(X0,e_1) ) ).
cnf(u1537,negated_conjecture,
( ~ product(e_3,X0,e_4)
| product(e_5,e_3,X0) ) ).
cnf(u959,negated_conjecture,
( ~ product(X0,e_4,e_1)
| product(e_4,e_5,X0) ) ).
cnf(u49,axiom,
( ~ group_element(X0)
| product(e_1,X0,e_2)
| product(e_2,X0,e_2)
| product(e_3,X0,e_2)
| product(e_4,X0,e_2)
| product(e_5,X0,e_2) ) ).
cnf(u52,axiom,
( ~ group_element(X0)
| product(e_1,X0,e_5)
| product(e_2,X0,e_5)
| product(e_3,X0,e_5)
| product(e_4,X0,e_5)
| product(e_5,X0,e_5) ) ).
cnf(u43,axiom,
equalish(X0,X0) ).
cnf(u910,negated_conjecture,
( ~ product(e_2,e_1,X0)
| product(X0,e_2,e_4) ) ).
cnf(u46,axiom,
( ~ product(X0,X1,X1)
| equalish(X0,X1) ) ).
cnf(product_right_cancellation,axiom,
( ~ product(X0,X3,X2)
| ~ product(X0,X1,X2)
| equalish(X1,X3) ) ).
cnf(e_5_is_not_e_1,axiom,
~ equalish(e_5,e_1) ).
cnf(e_4_is_not_e_5,axiom,
~ equalish(e_4,e_5) ).
cnf(u1494,axiom,
( ~ product(X0,e_1,e_4)
| equalish(X0,e_3) ) ).
cnf(e_5_is_not_e_3,axiom,
~ equalish(e_5,e_3) ).
cnf(u981,negated_conjecture,
( ~ product(e_4,e_1,X0)
| product(X0,e_4,e_3) ) ).
cnf(e_3_is_not_e_2,axiom,
~ equalish(e_3,e_2) ).
cnf(e_4_is_not_e_1,axiom,
~ equalish(e_4,e_1) ).
cnf(u1496,axiom,
( ~ product(e_3,e_1,X0)
| equalish(X0,e_4) ) ).
cnf(e_3_is_not_e_5,axiom,
~ equalish(e_3,e_5) ).
cnf(element_4,axiom,
group_element(e_4) ).
cnf(e_2_is_not_e_3,axiom,
~ equalish(e_2,e_3) ).
cnf(column_surjectivity,axiom,
( ~ group_element(X1)
| ~ group_element(X0)
| product(X0,e_1,X1)
| product(X0,e_2,X1)
| product(X0,e_3,X1)
| product(X0,e_4,X1)
| product(X0,e_5,X1) ) ).
cnf(row_surjectivity,axiom,
( ~ group_element(X1)
| ~ group_element(X0)
| product(e_1,X0,X1)
| product(e_2,X0,X1)
| product(e_3,X0,X1)
| product(e_4,X0,X1)
| product(e_5,X0,X1) ) ).
cnf(u1423,axiom,
( ~ product(e_2,X0,e_4)
| equalish(X0,e_3) ) ).
cnf(u1422,axiom,
( ~ product(X0,e_3,e_4)
| equalish(X0,e_2) ) ).
cnf(u1008,negated_conjecture,
( ~ product(e_5,e_2,X0)
| product(X0,e_5,e_3) ) ).
cnf(u1612,axiom,
( ~ product(e_2,e_1,X0)
| equalish(X0,e_5) ) ).
cnf(u1394,negated_conjecture,
( ~ product(e_1,X0,e_5)
| product(e_3,e_1,X0) ) ).
cnf(u1424,axiom,
( ~ product(e_2,e_3,X0)
| equalish(X0,e_4) ) ).
cnf(u1380,axiom,
( ~ product(e_1,e_3,X0)
| equalish(X0,e_2) ) ).
cnf(u460,negated_conjecture,
product(e_1,e_4,e_5) ).
cnf(u1004,axiom,
( ~ product(X0,e_5,e_2)
| equalish(X0,e_3) ) ).
cnf(u1382,negated_conjecture,
( ~ product(e_3,e_2,X0)
| product(X0,e_3,e_1) ) ).
cnf(u1313,negated_conjecture,
( ~ product(X0,e_5,e_4)
| product(e_5,e_3,X0) ) ).
cnf(u1351,negated_conjecture,
( ~ product(e_3,e_1,X0)
| product(X0,e_3,e_5) ) ).
cnf(u1551,negated_conjecture,
( ~ product(X0,e_2,e_3)
| product(e_2,e_5,X0) ) ).
cnf(u956,negated_conjecture,
( ~ product(e_1,e_4,X0)
| equalish(X0,e_5) ) ).
cnf(u752,axiom,
( ~ product(e_2,X0,e_1)
| equalish(X0,e_5) ) ).
cnf(u911,negated_conjecture,
( ~ product(X0,e_2,e_4)
| product(e_2,e_1,X0) ) ).
cnf(u198,axiom,
( ~ group_element(X0)
| product(X0,e_1,e_3)
| product(X0,e_2,e_3)
| product(X0,e_3,e_3)
| product(X0,e_4,e_3)
| product(X0,e_5,e_3) ) ).
cnf(qg3_2,negated_conjecture,
( ~ product(X2,X1,X3)
| product(X0,X1,X2)
| ~ product(X1,X3,X0) ) ).
cnf(u197,axiom,
( ~ group_element(X0)
| product(X0,e_1,e_2)
| product(X0,e_2,e_2)
| product(X0,e_3,e_2)
| product(X0,e_4,e_2)
| product(X0,e_5,e_2) ) ).
cnf(u1550,negated_conjecture,
( ~ product(e_2,e_5,X0)
| product(X0,e_2,e_3) ) ).
cnf(u1549,negated_conjecture,
( ~ product(e_2,X0,e_3)
| product(e_5,e_2,X0) ) ).
cnf(u1546,axiom,
( ~ product(X0,e_2,e_5)
| equalish(X0,e_3) ) ).
cnf(u1610,axiom,
( ~ product(X0,e_1,e_5)
| equalish(X0,e_2) ) ).
cnf(u1381,negated_conjecture,
( ~ product(e_3,X0,e_1)
| product(e_2,e_3,X0) ) ).
cnf(u1615,negated_conjecture,
( ~ product(X0,e_1,e_2)
| product(e_1,e_5,X0) ) ).
cnf(u403,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(u51,axiom,
( ~ group_element(X0)
| product(e_1,X0,e_4)
| product(e_2,X0,e_4)
| product(e_3,X0,e_4)
| product(e_4,X0,e_4)
| product(e_5,X0,e_4) ) ).
cnf(u405,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(u980,negated_conjecture,
( ~ product(e_4,X0,e_3)
| product(e_1,e_4,X0) ) ).
cnf(u1350,negated_conjecture,
( ~ product(e_3,X0,e_5)
| product(e_1,e_3,X0) ) ).
cnf(product_idempotence,axiom,
product(X0,X0,X0) ).
cnf(u1115,negated_conjecture,
( ~ product(X0,e_1,e_4)
| product(e_1,e_2,X0) ) ).
cnf(u1161,negated_conjecture,
( ~ product(X0,e_4,e_2)
| product(e_4,e_3,X0) ) ).
cnf(u1352,negated_conjecture,
( ~ product(X0,e_3,e_5)
| product(e_3,e_1,X0) ) ).
cnf(u1276,negated_conjecture,
( ~ product(e_2,e_3,X0)
| product(X0,e_2,e_1) ) ).
cnf(u1308,axiom,
( ~ product(X0,e_5,e_3)
| equalish(X0,e_4) ) ).
cnf(u1536,axiom,
( ~ product(e_4,e_3,X0)
| equalish(X0,e_5) ) ).
cnf(u1114,negated_conjecture,
( ~ product(e_1,e_2,X0)
| product(X0,e_1,e_4) ) ).
cnf(u1272,axiom,
( ~ product(X0,e_2,e_3)
| equalish(X0,e_1) ) ).
cnf(u1113,negated_conjecture,
( ~ product(e_1,X0,e_4)
| product(e_2,e_1,X0) ) ).
cnf(u1393,axiom,
( ~ product(e_5,e_1,X0)
| equalish(X0,e_3) ) ).
cnf(u909,negated_conjecture,
( ~ product(e_2,X0,e_4)
| product(e_1,e_2,X0) ) ).
cnf(u908,axiom,
( ~ product(e_4,e_2,X0)
| equalish(X0,e_1) ) ).
cnf(u1383,negated_conjecture,
( ~ product(X0,e_3,e_1)
| product(e_3,e_2,X0) ) ).
cnf(u1347,axiom,
( ~ product(X0,e_3,e_1)
| equalish(X0,e_5) ) ).
cnf(u1349,axiom,
( ~ product(e_5,e_3,X0)
| equalish(X0,e_1) ) ).
cnf(e_1_is_not_e_2,axiom,
~ equalish(e_1,e_2) ).
cnf(u402,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(product_left_cancellation,axiom,
( ~ product(X3,X1,X2)
| ~ product(X0,X1,X2)
| equalish(X0,X3) ) ).
cnf(u36,negated_conjecture,
( ~ product(X0,X1,X0)
| product(X0,X0,X1) ) ).
cnf(e_5_is_not_e_2,axiom,
~ equalish(e_5,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(e_5_is_not_e_4,axiom,
~ equalish(e_5,e_4) ).
cnf(e_2_is_not_e_4,axiom,
~ equalish(e_2,e_4) ).
cnf(u1498,negated_conjecture,
( ~ product(e_1,e_4,X0)
| product(X0,e_1,e_3) ) ).
cnf(e_4_is_not_e_2,axiom,
~ equalish(e_4,e_2) ).
cnf(u1484,axiom,
( ~ product(e_1,X0,e_4)
| equalish(X0,e_5) ) ).
cnf(element_1,axiom,
group_element(e_1) ).
cnf(element_5,axiom,
group_element(e_5) ).
cnf(u1273,axiom,
( ~ product(e_1,X0,e_3)
| equalish(X0,e_2) ) ).
cnf(e_1_is_not_e_4,axiom,
~ equalish(e_1,e_4) ).
cnf(qg3_1,negated_conjecture,
( ~ product(X3,X0,X1)
| product(X0,X1,X2)
| ~ product(X2,X0,X3) ) ).
cnf(element_2,axiom,
group_element(e_2) ).
cnf(u954,negated_conjecture,
( ~ product(X0,e_4,e_5)
| equalish(X0,e_1) ) ).
cnf(u1436,axiom,
( ~ product(e_5,e_2,X0)
| equalish(X0,e_4) ) ).
cnf(u1611,axiom,
( ~ product(e_2,X0,e_5)
| equalish(X0,e_1) ) ).
cnf(u1426,negated_conjecture,
( ~ product(e_3,e_4,X0)
| product(X0,e_3,e_2) ) ).
cnf(u1028,axiom,
( ~ product(e_5,e_4,X0)
| equalish(X0,e_2) ) ).
cnf(u1499,negated_conjecture,
( ~ product(X0,e_1,e_3)
| product(e_1,e_4,X0) ) ).
cnf(u1534,axiom,
( ~ product(X0,e_3,e_5)
| equalish(X0,e_4) ) ).
cnf(u1435,axiom,
( ~ product(e_5,X0,e_4)
| equalish(X0,e_2) ) ).
cnf(u1378,axiom,
( ~ product(X0,e_3,e_2)
| equalish(X0,e_1) ) ).
cnf(u1031,negated_conjecture,
( ~ product(X0,e_4,e_5)
| product(e_4,e_2,X0) ) ).
cnf(u1497,negated_conjecture,
( ~ product(e_1,X0,e_3)
| product(e_4,e_1,X0) ) ).
cnf(u1311,negated_conjecture,
( ~ product(e_5,X0,e_4)
| product(e_3,e_5,X0) ) ).
cnf(u756,negated_conjecture,
( ~ product(X0,e_5,e_2)
| product(e_5,e_1,X0) ) ).
cnf(u1156,axiom,
( ~ product(X0,e_4,e_3)
| equalish(X0,e_2) ) ).
cnf(u1275,negated_conjecture,
( ~ product(e_2,X0,e_1)
| product(e_3,e_2,X0) ) ).
cnf(u1487,negated_conjecture,
( ~ product(e_5,e_4,X0)
| product(X0,e_5,e_1) ) ).
cnf(u199,axiom,
( ~ group_element(X0)
| product(X0,e_1,e_4)
| product(X0,e_2,e_4)
| product(X0,e_3,e_4)
| product(X0,e_4,e_4)
| product(X0,e_5,e_4) ) ).
cnf(u1310,axiom,
( ~ product(e_4,e_5,X0)
| equalish(X0,e_3) ) ).
cnf(u1427,negated_conjecture,
( ~ product(X0,e_3,e_2)
| product(e_3,e_4,X0) ) ).
cnf(u978,axiom,
( ~ product(e_3,X0,e_1)
| equalish(X0,e_4) ) ).
cnf(u1379,axiom,
( ~ product(e_1,X0,e_2)
| equalish(X0,e_3) ) ).
cnf(u200,axiom,
( ~ group_element(X0)
| product(X0,e_1,e_5)
| product(X0,e_2,e_5)
| product(X0,e_3,e_5)
| product(X0,e_4,e_5)
| product(X0,e_5,e_5) ) ).
cnf(u955,negated_conjecture,
( ~ product(e_1,X0,e_5)
| equalish(X0,e_4) ) ).
cnf(u48,axiom,
( ~ group_element(X0)
| product(e_1,X0,e_1)
| product(e_2,X0,e_1)
| product(e_3,X0,e_1)
| product(e_4,X0,e_1)
| product(e_5,X0,e_1) ) ).
cnf(u906,axiom,
( ~ product(X0,e_2,e_1)
| equalish(X0,e_4) ) ).
cnf(u42,axiom,
( ~ product(X0,X0,X1)
| equalish(X1,X0) ) ).
cnf(u1548,axiom,
( ~ product(e_3,e_2,X0)
| equalish(X0,e_5) ) ).
cnf(product_total_function2,axiom,
( ~ product(X0,X1,X3)
| ~ product(X0,X1,X2)
| equalish(X2,X3) ) ).
cnf(u1539,negated_conjecture,
( ~ product(X0,e_3,e_4)
| product(e_3,e_5,X0) ) ).
cnf(u44,axiom,
( ~ product(X0,X1,X0)
| equalish(X1,X0) ) ).
cnf(qg3,negated_conjecture,
( ~ product(X2,X0,X3)
| ~ product(X0,X1,X2)
| product(X3,X0,X1) ) ).
cnf(u38,negated_conjecture,
( ~ product(X1,X0,X0)
| product(X0,X0,X1) ) ).
cnf(u1277,negated_conjecture,
( ~ product(X0,e_2,e_1)
| product(e_2,e_3,X0) ) ).
cnf(u37,negated_conjecture,
( ~ product(X1,X1,X0)
| product(X0,X1,X1) ) ).
cnf(e_4_is_not_e_3,axiom,
~ equalish(e_4,e_3) ).
cnf(u977,axiom,
( ~ product(X0,e_4,e_1)
| equalish(X0,e_3) ) ).
cnf(u1312,negated_conjecture,
( ~ product(e_5,e_3,X0)
| product(X0,e_5,e_4) ) ).
cnf(u1159,negated_conjecture,
( ~ product(e_4,X0,e_2)
| product(e_3,e_4,X0) ) ).
cnf(e_3_is_not_e_1,axiom,
~ equalish(e_3,e_1) ).
cnf(u1274,axiom,
( ~ product(e_1,e_2,X0)
| equalish(X0,e_3) ) ).
cnf(e_2_is_not_e_5,axiom,
~ equalish(e_2,e_5) ).
cnf(u1439,negated_conjecture,
( ~ product(X0,e_2,e_5)
| product(e_2,e_4,X0) ) ).
cnf(u1486,negated_conjecture,
( ~ product(e_5,X0,e_1)
| product(e_4,e_5,X0) ) ).
cnf(u1425,negated_conjecture,
( ~ product(e_3,X0,e_2)
| product(e_4,e_3,X0) ) ).
cnf(u1488,negated_conjecture,
( ~ product(X0,e_5,e_1)
| product(e_5,e_4,X0) ) ).
cnf(u1111,axiom,
( ~ product(e_4,X0,e_2)
| equalish(X0,e_1) ) ).
cnf(u1391,axiom,
( ~ product(X0,e_1,e_3)
| equalish(X0,e_5) ) ).
cnf(u1438,negated_conjecture,
( ~ product(e_2,e_4,X0)
| product(X0,e_2,e_5) ) ).
cnf(u1396,negated_conjecture,
( ~ product(X0,e_1,e_5)
| product(e_1,e_3,X0) ) ).
cnf(u979,axiom,
( ~ product(e_3,e_4,X0)
| equalish(X0,e_1) ) ).
cnf(u1027,axiom,
( ~ product(e_5,X0,e_2)
| equalish(X0,e_4) ) ).
cnf(u1030,negated_conjecture,
( ~ product(e_4,e_2,X0)
| product(X0,e_4,e_5) ) ).
cnf(u1029,negated_conjecture,
( ~ product(e_4,X0,e_5)
| product(e_2,e_4,X0) ) ).
cnf(u1309,axiom,
( ~ product(e_4,X0,e_3)
| equalish(X0,e_5) ) ).
cnf(u1026,axiom,
( ~ product(X0,e_4,e_2)
| equalish(X0,e_5) ) ).
cnf(u1614,negated_conjecture,
( ~ product(e_1,e_5,X0)
| product(X0,e_1,e_2) ) ).
cnf(u1613,negated_conjecture,
( ~ product(e_1,X0,e_2)
| product(e_5,e_1,X0) ) ).
cnf(e_3_is_not_e_4,axiom,
~ equalish(e_3,e_4) ).
cnf(u404,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(e_1_is_not_e_3,axiom,
~ equalish(e_1,e_3) ).
cnf(u1006,axiom,
( ~ product(e_3,e_5,X0)
| equalish(X0,e_2) ) ).
cnf(u907,axiom,
( ~ product(e_4,X0,e_1)
| equalish(X0,e_2) ) ).
cnf(e_2_is_not_e_1,axiom,
~ equalish(e_2,e_1) ).
cnf(e_1_is_not_e_5,axiom,
~ equalish(e_1,e_5) ).
cnf(element_3,axiom,
group_element(e_3) ).
cnf(u196,axiom,
( ~ group_element(X0)
| product(X0,e_1,e_1)
| product(X0,e_2,e_1)
| product(X0,e_3,e_1)
| product(X0,e_4,e_1)
| product(X0,e_5,e_1) ) ).
cnf(u1395,negated_conjecture,
( ~ product(e_1,e_3,X0)
| product(X0,e_1,e_5) ) ).
cnf(u958,negated_conjecture,
( ~ product(e_4,e_5,X0)
| product(X0,e_4,e_1) ) ).
cnf(u754,negated_conjecture,
( ~ product(e_5,X0,e_2)
| product(e_1,e_5,X0) ) ).
cnf(u753,axiom,
( ~ product(e_2,e_5,X0)
| equalish(X0,e_1) ) ).
cnf(u982,negated_conjecture,
( ~ product(X0,e_4,e_3)
| product(e_4,e_1,X0) ) ).
cnf(u1434,axiom,
( ~ product(X0,e_2,e_4)
| equalish(X0,e_5) ) ).
cnf(u1392,axiom,
( ~ product(e_5,X0,e_3)
| equalish(X0,e_1) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP127-4.005 : TPTP v9.3.1. Bugfixed v1.2.1.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.35 % Computer : n001.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sun Sep 27 09:32:15 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.14/0.39 Running first-order theorem proving
% 0.14/0.39 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.11/1.46 % (3293507)Input is clausal, will run a generic CNF schedule.
% 5.11/1.46 % (3293516)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3599066303:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 5.11/1.46 % (3293517)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=242690510:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 5.11/1.46 % (3293513)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=4107918039:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 5.11/1.46 % (3293514)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=4003175770:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 5.11/1.46 % (3293515)lrs+10_1_sil=8000:sp=occurrence:random_seed=274094192:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 5.11/1.46 % (3293518)dis-21_1_sil=8000:lcm=predicate:random_seed=2993040642: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.11/1.46 % (3293512)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=735797531:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 5.11/1.46 % (3293515)Refutation not found, incomplete strategy
% 5.11/1.46 % (3293515)------------------------------
% 5.11/1.46 % (3293515)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.11/1.46 % (3293515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.11/1.46 % (3293515)CaDiCaL version: 2.1.3
% 5.11/1.46 % (3293515)Termination reason: Refutation not found, incomplete strategy
% 5.11/1.46 % (3293515)Time elapsed: 0.001 s
% 5.11/1.46 % (3293515)Peak memory usage: 87 MB
% 5.11/1.46 % (3293516)Instruction limit reached!
% 5.11/1.46 % (3293516)------------------------------
% 5.11/1.46 % (3293516)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.11/1.46 % (3293516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.11/1.46 % (3293516)CaDiCaL version: 2.1.3
% 5.11/1.46 % (3293516)Termination reason: Instruction limit
% 5.11/1.46 % (3293516)Termination phase: Saturation
% 5.11/1.46 % (3293516)Time elapsed: 0.054 s
% 5.11/1.46 % (3293516)Peak memory usage: 87 MB
% 5.11/1.46 % (3293516)Instructions burned: 115 (million)
% 5.11/1.46 % (3293518)Instruction limit reached!
% 5.11/1.46 % (3293518)------------------------------
% 5.11/1.46 % (3293518)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.11/1.46 % (3293518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.11/1.46 % (3293518)CaDiCaL version: 2.1.3
% 5.11/1.46 % (3293518)Termination reason: Instruction limit
% 5.11/1.46 % (3293518)Termination phase: Saturation
% 5.11/1.46 % (3293518)Time elapsed: 0.071 s
% 5.11/1.46 % (3293518)Peak memory usage: 89 MB
% 5.11/1.46 % (3293518)Instructions burned: 118 (million)
% 5.11/1.46 % (3293517)Instruction limit reached!
% 5.11/1.46 % (3293517)------------------------------
% 5.11/1.46 % (3293517)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.11/1.46 % (3293517)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.11/1.46 % (3293517)CaDiCaL version: 2.1.3
% 5.11/1.46 % (3293517)Termination reason: Instruction limit
% 5.11/1.46 % (3293517)Termination phase: Saturation
% 5.11/1.46 % (3293517)Time elapsed: 0.132 s
% 5.11/1.46 % (3293517)Peak memory usage: 88 MB
% 5.11/1.46 % (3293517)Instructions burned: 181 (million)
% 5.11/1.46 % (3293526)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=3788492438:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 5.11/1.46 % (3293527)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1848512780: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.11/1.46 % (3293527)Refutation not found, incomplete strategy
% 5.11/1.46 % (3293527)------------------------------
% 5.11/1.46 % (3293527)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.11/1.46 % (3293527)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.11/1.46 % (3293527)CaDiCaL version: 2.1.3
% 5.11/1.46 % (3293527)Termination reason: Refutation not found, incomplete strategy
% 5.11/1.46 % (3293527)Time elapsed: 0.002 s
% 5.11/1.46 % (3293527)Peak memory usage: 87 MB
% 5.11/1.46 % (3293527)Instructions burned: 2 (million)
% 5.11/1.46 % (3293515)------------------------------
% 5.11/1.46 % (3293515)------------------------------
% 5.11/1.46 % (3293528)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1040058935:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 5.11/1.46 % (3293526)Instruction limit reached!
% 5.11/1.46 % (3293526)------------------------------
% 5.11/1.46 % (3293526)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.11/1.46 % (3293526)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.11/1.46 % (3293526)CaDiCaL version: 2.1.3
% 5.11/1.46 % (3293526)Termination reason: Instruction limit
% 5.11/1.46 % (3293526)Termination phase: Saturation
% 5.11/1.46 % (3293526)Time elapsed: 0.083 s
% 5.11/1.46 % (3293526)Peak memory usage: 89 MB
% 5.11/1.46 % (3293526)Instructions burned: 143 (million)
% 5.11/1.46 % (3293528)Instruction limit reached!
% 5.11/1.46 % (3293528)------------------------------
% 5.11/1.46 % (3293528)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.11/1.46 % (3293528)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.11/1.46 % (3293528)CaDiCaL version: 2.1.3
% 5.11/1.46 % (3293528)Termination reason: Instruction limit
% 5.11/1.46 % (3293528)Termination phase: Saturation
% 5.11/1.46 % (3293528)Time elapsed: 0.056 s
% 5.11/1.46 % (3293528)Peak memory usage: 88 MB
% 5.11/1.46 % (3293528)Instructions burned: 220 (million)
% 5.11/1.46 % (3293531)lrs+10_64_to=lpo:sil=8000:random_seed=308380376:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 5.11/1.46 % (3293531)First to succeed.
% 5.11/1.46 % (3293531)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3293507"
% 5.11/1.46 % (3293533)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=2033064452:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 5.11/1.46 % (3293527)------------------------------
% 5.11/1.46 % (3293527)------------------------------
% 5.11/1.46 % (3293534)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=3788833942:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 5.11/1.46 % (3293534)Instruction limit reached!
% 5.11/1.46 % (3293534)------------------------------
% 5.11/1.46 % (3293534)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.11/1.46 % (3293534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.11/1.46 % (3293534)CaDiCaL version: 2.1.3
% 5.11/1.46 % (3293534)Termination reason: Instruction limit
% 5.11/1.46 % (3293534)Termination phase: Saturation
% 5.11/1.46 % (3293534)Time elapsed: 0.047 s
% 5.11/1.46 % (3293534)Peak memory usage: 89 MB
% 5.11/1.46 % (3293534)Instructions burned: 160 (million)
% 5.11/1.46 % (3293533)Instruction limit reached!
% 5.11/1.46 % (3293533)------------------------------
% 5.11/1.46 % (3293533)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.11/1.46 % (3293533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.11/1.46 % (3293533)CaDiCaL version: 2.1.3
% 5.11/1.46 % (3293533)Termination reason: Instruction limit
% 5.11/1.46 % (3293533)Termination phase: Saturation
% 5.11/1.46 % (3293533)Time elapsed: 0.094 s
% 5.11/1.46 % (3293533)Peak memory usage: 88 MB
% 5.11/1.46 % (3293533)Instructions burned: 194 (million)
% 5.11/1.46 % (3293513)Refutation not found, incomplete strategy
% 5.11/1.46 % (3293513)------------------------------
% 5.11/1.46 % (3293513)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.11/1.46 % (3293513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.11/1.46 % (3293513)CaDiCaL version: 2.1.3
% 5.11/1.46 % (3293513)Termination reason: Refutation not found, incomplete strategy
% 5.11/1.46 % (3293513)Time elapsed: 0.608 s
% 5.11/1.46 % (3293513)Peak memory usage: 125 MB
% 5.11/1.46 % (3293513)Instructions burned: 917 (million)
% 5.11/1.46 % (3293538)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=2547074557:i=3394:sd=4:ss=included:sgt=64_2993 on theBenchmark for (2993ds/3394Mi)
% 5.11/1.46 % (3293539)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=1198159038:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 5.11/1.46 % (3293539)Refutation not found, incomplete strategy
% 5.11/1.46 % (3293539)------------------------------
% 5.11/1.46 % (3293539)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.11/1.46 % (3293539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.11/1.46 % (3293539)CaDiCaL version: 2.1.3
% 5.11/1.46 % (3293539)Termination reason: Refutation not found, incomplete strategy
% 5.11/1.46 % (3293539)Time elapsed: 0.003 s
% 5.11/1.46 % (3293539)Peak memory usage: 87 MB
% 5.11/1.46 % (3293539)Instructions burned: 10 (million)
% 5.11/1.46 % SZS status Satisfiable for theBenchmark
% 5.11/1.46 % SZS output start Saturation.
% See solution above
% 6.40/1.66 % SZS output start Definitions and Model Updates.
% 6.40/1.66 % SZS output end Definitions and Model Updates.
% 6.40/1.66 % (3293531)------------------------------
% 6.40/1.66 % (3293531)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.40/1.66 % (3293531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.40/1.66 % (3293531)CaDiCaL version: 2.1.3
% 6.40/1.66 % (3293531)Termination reason: Satisfiable
% 6.40/1.66 % (3293531)Time elapsed: 0.028 s
% 6.40/1.66 % (3293531)Peak memory usage: 88 MB
% 6.40/1.66 % (3293531)Instructions burned: 44 (million)
% 6.40/1.66 % (3293531)------------------------------
% 6.40/1.66 % (3293531)------------------------------
% 6.40/1.66 % (3293507)Success in time 0.852 s
% 6.40/1.66 % Vampire exiting
%------------------------------------------------------------------------------