%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP128-1.003 : TPTP v9.3.1. Released v1.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n003.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 : Fri Sep 25 01:25:20 PM UTC 2026
% Result : Unsatisfiable 14.74s 2.44s
% Output : Proof 14.74s
% Verified :
% SZS Type : Refutation
% Derivation depth : 42
% Number of leaves : 9
% Syntax : Number of formulae : 106 ( 19 unt; 0 def)
% Number of atoms : 367 ( 0 equ)
% Maximal formula atoms : 6 ( 3 avg)
% Number of connectives : 325 ( 64 ~; 261 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-3 aty)
% Number of functors : 3 ( 3 usr; 3 con; 0-0 aty)
% Number of variables : 73 ( 1 sgn 28 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f9,axiom,
( product(X,Y,e_3)
| product(X,Y,e_2)
| product(X,Y,e_1)
| ~ group_element(Y)
| ~ group_element(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_total_function1) ).
fof(f9_nnf,plain,
! [X,Y] :
( product(X,Y,e_3)
| product(X,Y,e_2)
| product(X,Y,e_1)
| ~ group_element(Y)
| ~ group_element(X) ),
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
! [X,Y] :
( product(X,Y,e_3)
| product(X,Y,e_2)
| product(X,Y,e_1)
| ~ group_element(Y)
| ~ group_element(X) ),
inference(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c9,plain,
( product(X0,X1,e_3)
| product(X0,X1,e_2)
| product(X0,X1,e_1)
| ~ group_element(X1)
| ~ group_element(X0) ),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(p17,plain,
( product(X0,X0,e_3)
| product(X0,X0,e_2)
| product(X0,X0,e_1)
| ~ group_element(X0) ),
inference(factoring,[status(thm)],[c9]) ).
cnf(f2,axiom,
group_element(e_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_3) ).
fof(f2_nnf,plain,
group_element(e_3),
inference(nnf_transformation,[status(thm)],[f2]) ).
cnf(c2,plain,
group_element(e_3),
inference(cnf_transformation,[status(esa)],[f2_nnf]) ).
cnf(p24,plain,
( product(e_3,e_3,e_3)
| product(e_3,e_3,e_2)
| product(e_3,e_3,e_1) ),
inference(resolution,[status(thm)],[p17,c2]) ).
cnf(f12,axiom,
( equalish(W,Z)
| ~ product(Z,Y,X)
| ~ product(W,Y,X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_left_cancellation) ).
fof(f12_nnf,plain,
! [W,Y,X,Z] :
( equalish(W,Z)
| ~ product(Z,Y,X)
| ~ product(W,Y,X) ),
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
! [W,Y,X,Z] :
( equalish(W,Z)
| ~ product(Z,Y,X)
| ~ product(W,Y,X) ),
inference(skolemisation,[status(esa)],[f12_nnf]) ).
cnf(c12,plain,
( equalish(X0,X3)
| ~ product(X3,X1,X2)
| ~ product(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(p64,plain,
( equalish(e_3,X0)
| ~ product(X0,e_3,e_3)
| product(e_3,e_3,e_2)
| product(e_3,e_3,e_1) ),
inference(resolution,[status(thm)],[p24,c12]) ).
cnf(f1,axiom,
group_element(e_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_2) ).
fof(f1_nnf,plain,
group_element(e_2),
inference(nnf_transformation,[status(thm)],[f1]) ).
cnf(c1,plain,
group_element(e_2),
inference(cnf_transformation,[status(esa)],[f1_nnf]) ).
cnf(p19,plain,
( product(e_2,X0,e_3)
| product(e_2,X0,e_2)
| product(e_2,X0,e_1)
| ~ group_element(X0) ),
inference(resolution,[status(thm)],[c9,c1]) ).
cnf(p40,plain,
( product(e_2,e_3,e_3)
| product(e_2,e_3,e_2)
| product(e_2,e_3,e_1) ),
inference(resolution,[status(thm)],[p19,c2]) ).
cnf(p176,plain,
( product(e_2,e_3,e_2)
| product(e_2,e_3,e_1)
| equalish(e_3,e_2)
| product(e_3,e_3,e_2)
| product(e_3,e_3,e_1) ),
inference(resolution,[status(thm)],[p64,p40]) ).
cnf(f13,negated_conjecture,
( product(X,Z1,Z2)
| ~ product(Z1,Y,Z2)
| ~ product(X,Y,Z1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qg3) ).
fof(f13_nnf,plain,
! [X,Y,Z1,Z2] :
( product(X,Z1,Z2)
| ~ product(Z1,Y,Z2)
| ~ product(X,Y,Z1) ),
inference(nnf_transformation,[status(thm)],[f13]) ).
fof(f13_sk,plain,
! [X,Y,Z1,Z2] :
( product(X,Z1,Z2)
| ~ product(Z1,Y,Z2)
| ~ product(X,Y,Z1) ),
inference(skolemisation,[status(esa)],[f13_nnf]) ).
cnf(c13,plain,
( product(X0,X2,X3)
| ~ product(X2,X1,X3)
| ~ product(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(p100,plain,
( product(e_2,e_3,X0)
| ~ product(e_3,e_3,X0)
| product(e_2,e_3,e_2)
| product(e_2,e_3,e_1) ),
inference(resolution,[status(thm)],[p40,c13]) ).
cnf(p105,plain,
( ~ product(e_3,e_3,e_2)
| product(e_2,e_3,e_2)
| product(e_2,e_3,e_1) ),
inference(factoring,[status(thm)],[p100]) ).
cnf(p630,plain,
( product(e_2,e_3,e_2)
| product(e_2,e_3,e_1)
| product(e_2,e_3,e_2)
| product(e_2,e_3,e_1)
| equalish(e_3,e_2)
| product(e_3,e_3,e_1) ),
inference(resolution,[status(thm)],[p176,p105]) ).
cnf(p1157,plain,
( product(e_2,e_3,e_2)
| product(e_2,e_3,e_2)
| product(e_2,e_3,e_1)
| equalish(e_3,e_2)
| product(e_3,e_3,e_1) ),
inference(factoring,[status(thm)],[p630]) ).
cnf(p1159,plain,
( product(e_2,e_3,e_2)
| product(e_2,e_3,e_1)
| equalish(e_3,e_2)
| product(e_3,e_3,e_1) ),
inference(factoring,[status(thm)],[p1157]) ).
cnf(p104,plain,
( ~ product(e_3,e_3,e_1)
| product(e_2,e_3,e_2)
| product(e_2,e_3,e_1) ),
inference(factoring,[status(thm)],[p100]) ).
cnf(p1172,plain,
( product(e_2,e_3,e_2)
| product(e_2,e_3,e_1)
| product(e_2,e_3,e_2)
| product(e_2,e_3,e_1)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[p1159,p104]) ).
cnf(p1231,plain,
( product(e_2,e_3,e_2)
| product(e_2,e_3,e_2)
| product(e_2,e_3,e_1)
| equalish(e_3,e_2) ),
inference(factoring,[status(thm)],[p1172]) ).
cnf(p1246,plain,
( product(e_2,e_3,e_2)
| product(e_2,e_3,e_1)
| equalish(e_3,e_2) ),
inference(factoring,[status(thm)],[p1231]) ).
cnf(p14,plain,
( product(X0,X0,X0)
| ~ product(X0,X1,X0) ),
inference(factoring,[status(thm)],[c13]) ).
cnf(p1248,plain,
( product(e_2,e_2,e_2)
| product(e_2,e_3,e_1)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[p1246,p14]) ).
cnf(p1256,plain,
( product(e_2,e_1,X0)
| ~ product(e_1,e_3,X0)
| product(e_2,e_2,e_2)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[p1248,c13]) ).
cnf(f0,axiom,
group_element(e_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_1) ).
fof(f0_nnf,plain,
group_element(e_1),
inference(nnf_transformation,[status(thm)],[f0]) ).
cnf(c0,plain,
group_element(e_1),
inference(cnf_transformation,[status(esa)],[f0_nnf]) ).
cnf(p18,plain,
( product(e_1,X0,e_3)
| product(e_1,X0,e_2)
| product(e_1,X0,e_1)
| ~ group_element(X0) ),
inference(resolution,[status(thm)],[c9,c0]) ).
cnf(p26,plain,
( product(e_1,e_3,e_3)
| product(e_1,e_3,e_2)
| product(e_1,e_3,e_1) ),
inference(resolution,[status(thm)],[p18,c2]) ).
cnf(p175,plain,
( product(e_1,e_3,e_2)
| product(e_1,e_3,e_1)
| equalish(e_3,e_1)
| product(e_3,e_3,e_2)
| product(e_3,e_3,e_1) ),
inference(resolution,[status(thm)],[p64,p26]) ).
cnf(p79,plain,
( product(e_1,e_3,X0)
| ~ product(e_3,e_3,X0)
| product(e_1,e_3,e_2)
| product(e_1,e_3,e_1) ),
inference(resolution,[status(thm)],[p26,c13]) ).
cnf(p85,plain,
( ~ product(e_3,e_3,e_2)
| product(e_1,e_3,e_2)
| product(e_1,e_3,e_1) ),
inference(factoring,[status(thm)],[p79]) ).
cnf(p612,plain,
( product(e_1,e_3,e_2)
| product(e_1,e_3,e_1)
| product(e_1,e_3,e_2)
| product(e_1,e_3,e_1)
| equalish(e_3,e_1)
| product(e_3,e_3,e_1) ),
inference(resolution,[status(thm)],[p175,p85]) ).
cnf(p1021,plain,
( product(e_1,e_3,e_2)
| product(e_1,e_3,e_2)
| product(e_1,e_3,e_1)
| equalish(e_3,e_1)
| product(e_3,e_3,e_1) ),
inference(factoring,[status(thm)],[p612]) ).
cnf(p1030,plain,
( product(e_1,e_3,e_2)
| product(e_1,e_3,e_1)
| equalish(e_3,e_1)
| product(e_3,e_3,e_1) ),
inference(factoring,[status(thm)],[p1021]) ).
cnf(p84,plain,
( ~ product(e_3,e_3,e_1)
| product(e_1,e_3,e_2)
| product(e_1,e_3,e_1) ),
inference(factoring,[status(thm)],[p79]) ).
cnf(p1036,plain,
( product(e_1,e_3,e_2)
| product(e_1,e_3,e_1)
| product(e_1,e_3,e_2)
| product(e_1,e_3,e_1)
| equalish(e_3,e_1) ),
inference(resolution,[status(thm)],[p1030,p84]) ).
cnf(p1074,plain,
( product(e_1,e_3,e_2)
| product(e_1,e_3,e_2)
| product(e_1,e_3,e_1)
| equalish(e_3,e_1) ),
inference(factoring,[status(thm)],[p1036]) ).
cnf(p1078,plain,
( product(e_1,e_3,e_2)
| product(e_1,e_3,e_1)
| equalish(e_3,e_1) ),
inference(factoring,[status(thm)],[p1074]) ).
cnf(p1301,plain,
( product(e_1,e_3,e_1)
| equalish(e_3,e_1)
| product(e_2,e_1,e_2)
| product(e_2,e_2,e_2)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[p1256,p1078]) ).
cnf(f11,axiom,
( equalish(W,Z)
| ~ product(X,Z,Y)
| ~ product(X,W,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_right_cancellation) ).
fof(f11_nnf,plain,
! [X,W,Y,Z] :
( equalish(W,Z)
| ~ product(X,Z,Y)
| ~ product(X,W,Y) ),
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
! [X,W,Y,Z] :
( equalish(W,Z)
| ~ product(X,Z,Y)
| ~ product(X,W,Y) ),
inference(skolemisation,[status(esa)],[f11_nnf]) ).
cnf(c11,plain,
( equalish(X1,X3)
| ~ product(X0,X3,X2)
| ~ product(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(p1250,plain,
( equalish(e_3,X0)
| ~ product(e_2,X0,e_2)
| product(e_2,e_3,e_1)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[p1246,c11]) ).
cnf(p1268,plain,
( ~ product(e_2,e_2,e_2)
| product(e_2,e_3,e_1)
| equalish(e_3,e_2) ),
inference(factoring,[status(thm)],[p1250]) ).
cnf(p1334,plain,
( product(e_2,e_3,e_1)
| equalish(e_3,e_2)
| product(e_1,e_3,e_1)
| equalish(e_3,e_1)
| product(e_2,e_1,e_2)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[p1301,p1268]) ).
cnf(p1434,plain,
( product(e_2,e_3,e_1)
| product(e_1,e_3,e_1)
| equalish(e_3,e_1)
| product(e_2,e_1,e_2)
| equalish(e_3,e_2) ),
inference(factoring,[status(thm)],[p1334]) ).
cnf(p1435,plain,
( product(e_2,e_1,X0)
| ~ product(e_1,e_3,X0)
| product(e_1,e_3,e_1)
| equalish(e_3,e_1)
| product(e_2,e_1,e_2)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[p1434,c13]) ).
cnf(p1594,plain,
( ~ product(e_1,e_3,e_2)
| product(e_1,e_3,e_1)
| equalish(e_3,e_1)
| product(e_2,e_1,e_2)
| equalish(e_3,e_2) ),
inference(factoring,[status(thm)],[p1435]) ).
cnf(p1606,plain,
( product(e_1,e_3,e_1)
| equalish(e_3,e_1)
| product(e_1,e_3,e_1)
| equalish(e_3,e_1)
| product(e_2,e_1,e_2)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[p1594,p1078]) ).
cnf(p1608,plain,
( equalish(e_3,e_1)
| product(e_1,e_3,e_1)
| equalish(e_3,e_1)
| product(e_2,e_1,e_2)
| equalish(e_3,e_2) ),
inference(factoring,[status(thm)],[p1606]) ).
cnf(p1609,plain,
( product(e_1,e_3,e_1)
| equalish(e_3,e_1)
| product(e_2,e_1,e_2)
| equalish(e_3,e_2) ),
inference(factoring,[status(thm)],[p1608]) ).
cnf(p1611,plain,
( product(e_2,e_2,e_2)
| product(e_1,e_3,e_1)
| equalish(e_3,e_1)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[p1609,p14]) ).
cnf(p1633,plain,
( product(e_2,e_3,e_1)
| equalish(e_3,e_2)
| product(e_1,e_3,e_1)
| equalish(e_3,e_1)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[p1611,p1268]) ).
cnf(p1663,plain,
( product(e_2,e_3,e_1)
| product(e_1,e_3,e_1)
| equalish(e_3,e_1)
| equalish(e_3,e_2) ),
inference(factoring,[status(thm)],[p1633]) ).
cnf(p1079,plain,
( product(e_1,e_2,X0)
| ~ product(e_2,e_3,X0)
| product(e_1,e_3,e_1)
| equalish(e_3,e_1) ),
inference(resolution,[status(thm)],[p1078,c13]) ).
cnf(p1669,plain,
( product(e_1,e_2,e_1)
| product(e_1,e_3,e_1)
| equalish(e_3,e_1)
| product(e_1,e_3,e_1)
| equalish(e_3,e_1)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[p1663,p1079]) ).
cnf(p1735,plain,
( product(e_1,e_2,e_1)
| equalish(e_3,e_1)
| product(e_1,e_3,e_1)
| equalish(e_3,e_1)
| equalish(e_3,e_2) ),
inference(factoring,[status(thm)],[p1669]) ).
cnf(p1736,plain,
( product(e_1,e_2,e_1)
| product(e_1,e_3,e_1)
| equalish(e_3,e_1)
| equalish(e_3,e_2) ),
inference(factoring,[status(thm)],[p1735]) ).
cnf(p1738,plain,
( product(e_1,e_1,e_1)
| product(e_1,e_2,e_1)
| equalish(e_3,e_1)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[p1736,p14]) ).
cnf(p1753,plain,
( product(e_1,e_1,e_1)
| product(e_1,e_1,e_1)
| equalish(e_3,e_1)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[p1738,p14]) ).
cnf(p1778,plain,
( product(e_1,e_1,e_1)
| equalish(e_3,e_1)
| equalish(e_3,e_2) ),
inference(factoring,[status(thm)],[p1753]) ).
cnf(p20,plain,
( product(e_3,X0,e_3)
| product(e_3,X0,e_2)
| product(e_3,X0,e_1)
| ~ group_element(X0) ),
inference(resolution,[status(thm)],[c9,c2]) ).
cnf(p47,plain,
( product(e_3,e_1,e_3)
| product(e_3,e_1,e_2)
| product(e_3,e_1,e_1) ),
inference(resolution,[status(thm)],[p20,c0]) ).
cnf(p107,plain,
( product(e_3,e_3,e_3)
| product(e_3,e_1,e_2)
| product(e_3,e_1,e_1) ),
inference(resolution,[status(thm)],[p47,p14]) ).
cnf(p115,plain,
( equalish(e_3,X0)
| ~ product(e_3,X0,e_3)
| product(e_3,e_1,e_2)
| product(e_3,e_1,e_1) ),
inference(resolution,[status(thm)],[p107,c11]) ).
cnf(p127,plain,
( product(e_3,e_1,e_2)
| product(e_3,e_1,e_1)
| equalish(e_3,e_1)
| product(e_3,e_1,e_2)
| product(e_3,e_1,e_1) ),
inference(resolution,[status(thm)],[p115,p47]) ).
cnf(p137,plain,
( product(e_3,e_1,e_2)
| equalish(e_3,e_1)
| product(e_3,e_1,e_2)
| product(e_3,e_1,e_1) ),
inference(factoring,[status(thm)],[p127]) ).
cnf(p139,plain,
( equalish(e_3,e_1)
| product(e_3,e_1,e_2)
| product(e_3,e_1,e_1) ),
inference(factoring,[status(thm)],[p137]) ).
cnf(p143,plain,
( equalish(e_3,X0)
| ~ product(X0,e_1,e_2)
| equalish(e_3,e_1)
| product(e_3,e_1,e_1) ),
inference(resolution,[status(thm)],[p139,c12]) ).
cnf(p1615,plain,
( equalish(e_3,e_2)
| equalish(e_3,e_1)
| product(e_3,e_1,e_1)
| product(e_1,e_3,e_1)
| equalish(e_3,e_1)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[p1609,p143]) ).
cnf(p1699,plain,
( equalish(e_3,e_1)
| product(e_3,e_1,e_1)
| product(e_1,e_3,e_1)
| equalish(e_3,e_1)
| equalish(e_3,e_2) ),
inference(factoring,[status(thm)],[p1615]) ).
cnf(p1701,plain,
( product(e_3,e_1,e_1)
| product(e_1,e_3,e_1)
| equalish(e_3,e_1)
| equalish(e_3,e_2) ),
inference(factoring,[status(thm)],[p1699]) ).
cnf(p1705,plain,
( equalish(e_3,X0)
| ~ product(X0,e_1,e_1)
| product(e_1,e_3,e_1)
| equalish(e_3,e_1)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[p1701,c12]) ).
cnf(p1722,plain,
( ~ product(e_1,e_1,e_1)
| product(e_1,e_3,e_1)
| equalish(e_3,e_1)
| equalish(e_3,e_2) ),
inference(factoring,[status(thm)],[p1705]) ).
cnf(p1785,plain,
( product(e_1,e_3,e_1)
| equalish(e_3,e_1)
| equalish(e_3,e_2)
| equalish(e_3,e_1)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[p1778,p1722]) ).
cnf(p1793,plain,
( product(e_1,e_3,e_1)
| equalish(e_3,e_1)
| equalish(e_3,e_1)
| equalish(e_3,e_2) ),
inference(factoring,[status(thm)],[p1785]) ).
cnf(p1795,plain,
( product(e_1,e_3,e_1)
| equalish(e_3,e_1)
| equalish(e_3,e_2) ),
inference(factoring,[status(thm)],[p1793]) ).
cnf(p1805,plain,
( equalish(e_3,X0)
| ~ product(e_1,X0,e_1)
| equalish(e_3,e_1)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[p1795,c11]) ).
cnf(p1813,plain,
( ~ product(e_1,e_1,e_1)
| equalish(e_3,e_1)
| equalish(e_3,e_2) ),
inference(factoring,[status(thm)],[p1805]) ).
cnf(p1823,plain,
( equalish(e_3,e_1)
| equalish(e_3,e_2)
| equalish(e_3,e_1)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[p1813,p1778]) ).
cnf(p1824,plain,
( equalish(e_3,e_1)
| equalish(e_3,e_1)
| equalish(e_3,e_2) ),
inference(factoring,[status(thm)],[p1823]) ).
cnf(p1826,plain,
( equalish(e_3,e_1)
| equalish(e_3,e_2) ),
inference(factoring,[status(thm)],[p1824]) ).
cnf(f8,axiom,
~ equalish(e_3,e_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_3_is_not_e_2) ).
fof(f8_nnf,plain,
~ equalish(e_3,e_2),
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
~ equalish(e_3,e_2),
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c8,plain,
~ equalish(e_3,e_2),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(p1827,plain,
equalish(e_3,e_1),
inference(resolution,[status(thm)],[p1826,c8]) ).
cnf(f7,axiom,
~ equalish(e_3,e_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_3_is_not_e_1) ).
fof(f7_nnf,plain,
~ equalish(e_3,e_1),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
~ equalish(e_3,e_1),
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c7,plain,
~ equalish(e_3,e_1),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(p1833,plain,
$false,
inference(resolution,[status(thm)],[p1827,c7]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP128-1.003 : TPTP v9.3.1. Released v1.2.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.38 % Computer : n003.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 : Wed Sep 23 13:45:19 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 14.74/2.44 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 14.74/2.44 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------