%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP127-3.004 : TPTP v9.3.1. Released v1.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n012.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:19 PM UTC 2026
% Result : Unsatisfiable 94.07s 73.92s
% Output : Proof 94.07s
% Verified :
% SZS Type : Refutation
% Derivation depth : 45
% Number of leaves : 15
% Syntax : Number of formulae : 169 ( 39 unt; 0 def)
% Number of atoms : 726 ( 0 equ)
% Maximal formula atoms : 9 ( 4 avg)
% Number of connectives : 651 ( 94 ~; 557 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 5 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-3 aty)
% Number of functors : 4 ( 4 usr; 4 con; 0-0 aty)
% Number of variables : 105 ( 0 sgn 38 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f37,axiom,
( product(X,Y,e_4)
| 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(f37_nnf,plain,
! [X,Y] :
( product(X,Y,e_4)
| 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)],[f37]) ).
fof(f37_sk,plain,
! [X,Y] :
( product(X,Y,e_4)
| 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)],[f37_nnf]) ).
cnf(c37,plain,
( product(X0,X1,e_4)
| 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)],[f37_sk]) ).
cnf(f24,axiom,
group_element(e_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_4) ).
fof(f24_nnf,plain,
group_element(e_4),
inference(nnf_transformation,[status(thm)],[f24]) ).
cnf(c24,plain,
group_element(e_4),
inference(cnf_transformation,[status(esa)],[f24_nnf]) ).
cnf(p68,plain,
( product(e_4,X0,e_4)
| product(e_4,X0,e_3)
| product(e_4,X0,e_2)
| product(e_4,X0,e_1)
| ~ group_element(X0) ),
inference(resolution,[status(thm)],[c37,c24]) ).
cnf(f22,axiom,
group_element(e_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_2) ).
fof(f22_nnf,plain,
group_element(e_2),
inference(nnf_transformation,[status(thm)],[f22]) ).
cnf(c22,plain,
group_element(e_2),
inference(cnf_transformation,[status(esa)],[f22_nnf]) ).
cnf(p145,plain,
( product(e_4,e_2,e_4)
| product(e_4,e_2,e_3)
| product(e_4,e_2,e_2)
| product(e_4,e_2,e_1) ),
inference(resolution,[status(thm)],[p68,c22]) ).
cnf(f42,negated_conjecture,
( product(Z2,Y,X)
| ~ product(Z1,Y,Z2)
| ~ product(Y,X,Z1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qg3) ).
fof(f42_nnf,plain,
! [Y,X,Z1,Z2] :
( product(Z2,Y,X)
| ~ product(Z1,Y,Z2)
| ~ product(Y,X,Z1) ),
inference(nnf_transformation,[status(thm)],[f42]) ).
fof(f42_sk,plain,
! [Y,X,Z1,Z2] :
( product(Z2,Y,X)
| ~ product(Z1,Y,Z2)
| ~ product(Y,X,Z1) ),
inference(skolemisation,[status(esa)],[f42_nnf]) ).
cnf(c42,plain,
( product(X3,X0,X1)
| ~ product(X2,X0,X3)
| ~ product(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f42_sk]) ).
cnf(p575,plain,
( product(X0,e_4,e_2)
| ~ product(e_4,e_4,X0)
| product(e_4,e_2,e_3)
| product(e_4,e_2,e_2)
| product(e_4,e_2,e_1) ),
inference(resolution,[status(thm)],[p145,c42]) ).
cnf(f41,axiom,
product(X,X,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_idempotence) ).
fof(f41_nnf,plain,
! [X] : product(X,X,X),
inference(nnf_transformation,[status(thm)],[f41]) ).
fof(f41_sk,plain,
! [X] : product(X,X,X),
inference(skolemisation,[status(esa)],[f41_nnf]) ).
cnf(c41,plain,
product(X0,X0,X0),
inference(cnf_transformation,[status(esa)],[f41_sk]) ).
cnf(p611,plain,
( product(e_4,e_4,e_2)
| product(e_4,e_2,e_3)
| product(e_4,e_2,e_2)
| product(e_4,e_2,e_1) ),
inference(resolution,[status(thm)],[p575,c41]) ).
cnf(f38,axiom,
( equalish(W,Z)
| ~ product(X,Y,Z)
| ~ product(X,Y,W) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_total_function2) ).
fof(f38_nnf,plain,
! [X,Y,W,Z] :
( equalish(W,Z)
| ~ product(X,Y,Z)
| ~ product(X,Y,W) ),
inference(nnf_transformation,[status(thm)],[f38]) ).
fof(f38_sk,plain,
! [X,Y,W,Z] :
( equalish(W,Z)
| ~ product(X,Y,Z)
| ~ product(X,Y,W) ),
inference(skolemisation,[status(esa)],[f38_nnf]) ).
cnf(c38,plain,
( equalish(X2,X3)
| ~ product(X0,X1,X3)
| ~ product(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f38_sk]) ).
cnf(p617,plain,
( equalish(e_2,X0)
| ~ product(e_4,e_4,X0)
| product(e_4,e_2,e_3)
| product(e_4,e_2,e_2)
| product(e_4,e_2,e_1) ),
inference(resolution,[status(thm)],[p611,c38]) ).
cnf(p634,plain,
( equalish(e_2,e_4)
| product(e_4,e_2,e_3)
| product(e_4,e_2,e_2)
| product(e_4,e_2,e_1) ),
inference(resolution,[status(thm)],[p617,c41]) ).
cnf(p66,plain,
( product(e_2,X0,e_4)
| 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)],[c37,c22]) ).
cnf(f23,axiom,
group_element(e_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_3) ).
fof(f23_nnf,plain,
group_element(e_3),
inference(nnf_transformation,[status(thm)],[f23]) ).
cnf(c23,plain,
group_element(e_3),
inference(cnf_transformation,[status(esa)],[f23_nnf]) ).
cnf(p122,plain,
( product(e_2,e_3,e_4)
| 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)],[p66,c23]) ).
cnf(p147,plain,
( product(X0,e_2,e_3)
| ~ product(e_4,e_2,X0)
| 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)],[p122,c42]) ).
cnf(p641,plain,
( product(e_3,e_2,e_3)
| product(e_2,e_3,e_3)
| product(e_2,e_3,e_2)
| product(e_2,e_3,e_1)
| equalish(e_2,e_4)
| product(e_4,e_2,e_2)
| product(e_4,e_2,e_1) ),
inference(resolution,[status(thm)],[p634,p147]) ).
cnf(f40,axiom,
( equalish(W,Z)
| ~ product(Z,Y,X)
| ~ product(W,Y,X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_left_cancellation) ).
fof(f40_nnf,plain,
! [W,Y,X,Z] :
( equalish(W,Z)
| ~ product(Z,Y,X)
| ~ product(W,Y,X) ),
inference(nnf_transformation,[status(thm)],[f40]) ).
fof(f40_sk,plain,
! [W,Y,X,Z] :
( equalish(W,Z)
| ~ product(Z,Y,X)
| ~ product(W,Y,X) ),
inference(skolemisation,[status(esa)],[f40_nnf]) ).
cnf(c40,plain,
( equalish(X0,X3)
| ~ product(X3,X1,X2)
| ~ product(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f40_sk]) ).
cnf(p69,plain,
( equalish(X1,X0)
| ~ product(X0,X1,X1) ),
inference(resolution,[status(thm)],[c40,c41]) ).
cnf(p1549,plain,
( equalish(e_2,e_4)
| product(e_3,e_2,e_3)
| product(e_2,e_3,e_3)
| product(e_2,e_3,e_2)
| product(e_2,e_3,e_1)
| equalish(e_2,e_4)
| product(e_4,e_2,e_1) ),
inference(resolution,[status(thm)],[p641,p69]) ).
cnf(p1559,plain,
( product(e_3,e_2,e_3)
| product(e_2,e_3,e_3)
| product(e_2,e_3,e_2)
| product(e_2,e_3,e_1)
| equalish(e_2,e_4)
| product(e_4,e_2,e_1) ),
inference(factoring,[status(thm)],[p1549]) ).
cnf(p1565,plain,
( product(e_1,e_2,e_3)
| product(e_2,e_3,e_3)
| product(e_2,e_3,e_2)
| product(e_2,e_3,e_1)
| product(e_3,e_2,e_3)
| product(e_2,e_3,e_3)
| product(e_2,e_3,e_2)
| product(e_2,e_3,e_1)
| equalish(e_2,e_4) ),
inference(resolution,[status(thm)],[p1559,p147]) ).
cnf(p16505,plain,
( product(e_1,e_2,e_3)
| product(e_2,e_3,e_3)
| product(e_2,e_3,e_2)
| product(e_3,e_2,e_3)
| product(e_2,e_3,e_3)
| product(e_2,e_3,e_2)
| product(e_2,e_3,e_1)
| equalish(e_2,e_4) ),
inference(factoring,[status(thm)],[p1565]) ).
cnf(p28234,plain,
( product(e_1,e_2,e_3)
| product(e_2,e_3,e_3)
| product(e_3,e_2,e_3)
| product(e_2,e_3,e_3)
| product(e_2,e_3,e_2)
| product(e_2,e_3,e_1)
| equalish(e_2,e_4) ),
inference(factoring,[status(thm)],[p16505]) ).
cnf(p28236,plain,
( product(e_1,e_2,e_3)
| product(e_3,e_2,e_3)
| product(e_2,e_3,e_3)
| product(e_2,e_3,e_2)
| product(e_2,e_3,e_1)
| equalish(e_2,e_4) ),
inference(factoring,[status(thm)],[p28234]) ).
cnf(f39,axiom,
( equalish(W,Z)
| ~ product(X,Z,Y)
| ~ product(X,W,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_right_cancellation) ).
fof(f39_nnf,plain,
! [X,W,Y,Z] :
( equalish(W,Z)
| ~ product(X,Z,Y)
| ~ product(X,W,Y) ),
inference(nnf_transformation,[status(thm)],[f39]) ).
fof(f39_sk,plain,
! [X,W,Y,Z] :
( equalish(W,Z)
| ~ product(X,Z,Y)
| ~ product(X,W,Y) ),
inference(skolemisation,[status(esa)],[f39_nnf]) ).
cnf(c39,plain,
( equalish(X1,X3)
| ~ product(X0,X3,X2)
| ~ product(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f39_sk]) ).
cnf(p63,plain,
( equalish(X0,X1)
| ~ product(X0,X1,X0) ),
inference(resolution,[status(thm)],[c39,c41]) ).
cnf(p28256,plain,
( equalish(e_3,e_2)
| product(e_1,e_2,e_3)
| product(e_2,e_3,e_3)
| product(e_2,e_3,e_2)
| product(e_2,e_3,e_1)
| equalish(e_2,e_4) ),
inference(resolution,[status(thm)],[p28236,p63]) ).
cnf(p28298,plain,
( equalish(e_3,e_2)
| equalish(e_3,e_2)
| product(e_1,e_2,e_3)
| product(e_2,e_3,e_2)
| product(e_2,e_3,e_1)
| equalish(e_2,e_4) ),
inference(resolution,[status(thm)],[p28256,p69]) ).
cnf(p28344,plain,
( equalish(e_3,e_2)
| product(e_1,e_2,e_3)
| product(e_2,e_3,e_2)
| product(e_2,e_3,e_1)
| equalish(e_2,e_4) ),
inference(factoring,[status(thm)],[p28298]) ).
cnf(p28347,plain,
( equalish(e_3,X0)
| ~ product(e_2,X0,e_2)
| equalish(e_3,e_2)
| product(e_1,e_2,e_3)
| product(e_2,e_3,e_1)
| equalish(e_2,e_4) ),
inference(resolution,[status(thm)],[p28344,c39]) ).
cnf(p28603,plain,
( equalish(e_3,e_2)
| equalish(e_3,e_2)
| product(e_1,e_2,e_3)
| product(e_2,e_3,e_1)
| equalish(e_2,e_4) ),
inference(resolution,[status(thm)],[p28347,c41]) ).
cnf(p28604,plain,
( equalish(e_3,e_2)
| product(e_1,e_2,e_3)
| product(e_2,e_3,e_1)
| equalish(e_2,e_4) ),
inference(factoring,[status(thm)],[p28603]) ).
cnf(p28608,plain,
( equalish(e_2,X0)
| ~ product(X0,e_3,e_1)
| equalish(e_3,e_2)
| product(e_1,e_2,e_3)
| equalish(e_2,e_4) ),
inference(resolution,[status(thm)],[p28604,c40]) ).
cnf(p28724,plain,
( ~ product(e_4,e_3,e_1)
| equalish(e_3,e_2)
| product(e_1,e_2,e_3)
| equalish(e_2,e_4) ),
inference(factoring,[status(thm)],[p28608]) ).
cnf(p123,plain,
( product(e_2,e_4,e_4)
| product(e_2,e_4,e_3)
| product(e_2,e_4,e_2)
| product(e_2,e_4,e_1) ),
inference(resolution,[status(thm)],[p66,c24]) ).
cnf(p154,plain,
( equalish(e_2,X0)
| ~ product(X0,e_4,e_4)
| product(e_2,e_4,e_3)
| product(e_2,e_4,e_2)
| product(e_2,e_4,e_1) ),
inference(resolution,[status(thm)],[p123,c40]) ).
cnf(p659,plain,
( equalish(e_2,e_4)
| product(e_2,e_4,e_3)
| product(e_2,e_4,e_2)
| product(e_2,e_4,e_1) ),
inference(resolution,[status(thm)],[p154,c41]) ).
cnf(p146,plain,
( product(e_4,e_3,e_4)
| product(e_4,e_3,e_3)
| product(e_4,e_3,e_2)
| product(e_4,e_3,e_1) ),
inference(resolution,[status(thm)],[p68,c23]) ).
cnf(p595,plain,
( product(X0,e_4,e_3)
| ~ product(e_4,e_4,X0)
| product(e_4,e_3,e_3)
| product(e_4,e_3,e_2)
| product(e_4,e_3,e_1) ),
inference(resolution,[status(thm)],[p146,c42]) ).
cnf(p664,plain,
( product(e_4,e_4,e_3)
| product(e_4,e_3,e_3)
| product(e_4,e_3,e_2)
| product(e_4,e_3,e_1) ),
inference(resolution,[status(thm)],[p595,c41]) ).
cnf(p669,plain,
( equalish(e_3,X0)
| ~ product(e_4,e_4,X0)
| product(e_4,e_3,e_3)
| product(e_4,e_3,e_2)
| product(e_4,e_3,e_1) ),
inference(resolution,[status(thm)],[p664,c38]) ).
cnf(p707,plain,
( equalish(e_3,e_4)
| product(e_4,e_3,e_3)
| product(e_4,e_3,e_2)
| product(e_4,e_3,e_1) ),
inference(resolution,[status(thm)],[p669,c41]) ).
cnf(p714,plain,
( equalish(e_3,e_4)
| equalish(e_3,e_4)
| product(e_4,e_3,e_2)
| product(e_4,e_3,e_1) ),
inference(resolution,[status(thm)],[p707,p69]) ).
cnf(p723,plain,
( equalish(e_3,e_4)
| product(e_4,e_3,e_2)
| product(e_4,e_3,e_1) ),
inference(factoring,[status(thm)],[p714]) ).
cnf(p724,plain,
( product(X0,e_4,e_3)
| ~ product(e_2,e_4,X0)
| equalish(e_3,e_4)
| product(e_4,e_3,e_1) ),
inference(resolution,[status(thm)],[p723,c42]) ).
cnf(p4366,plain,
( product(e_3,e_4,e_3)
| equalish(e_3,e_4)
| product(e_4,e_3,e_1)
| equalish(e_2,e_4)
| product(e_2,e_4,e_2)
| product(e_2,e_4,e_1) ),
inference(resolution,[status(thm)],[p659,p724]) ).
cnf(p28777,plain,
( product(e_3,e_4,e_3)
| equalish(e_3,e_4)
| equalish(e_2,e_4)
| product(e_2,e_4,e_2)
| product(e_2,e_4,e_1)
| equalish(e_3,e_2)
| product(e_1,e_2,e_3)
| equalish(e_2,e_4) ),
inference(resolution,[status(thm)],[p28724,p4366]) ).
cnf(p32240,plain,
( product(e_3,e_4,e_3)
| equalish(e_3,e_4)
| product(e_2,e_4,e_2)
| product(e_2,e_4,e_1)
| equalish(e_3,e_2)
| product(e_1,e_2,e_3)
| equalish(e_2,e_4) ),
inference(factoring,[status(thm)],[p28777]) ).
cnf(p32255,plain,
( equalish(e_3,e_4)
| equalish(e_3,e_4)
| product(e_2,e_4,e_2)
| product(e_2,e_4,e_1)
| equalish(e_3,e_2)
| product(e_1,e_2,e_3)
| equalish(e_2,e_4) ),
inference(resolution,[status(thm)],[p32240,p63]) ).
cnf(p32277,plain,
( equalish(e_3,e_4)
| product(e_2,e_4,e_2)
| product(e_2,e_4,e_1)
| equalish(e_3,e_2)
| product(e_1,e_2,e_3)
| equalish(e_2,e_4) ),
inference(factoring,[status(thm)],[p32255]) ).
cnf(p32281,plain,
( equalish(e_2,e_4)
| equalish(e_3,e_4)
| product(e_2,e_4,e_1)
| equalish(e_3,e_2)
| product(e_1,e_2,e_3)
| equalish(e_2,e_4) ),
inference(resolution,[status(thm)],[p32277,p63]) ).
cnf(p32329,plain,
( equalish(e_3,e_4)
| product(e_2,e_4,e_1)
| equalish(e_3,e_2)
| product(e_1,e_2,e_3)
| equalish(e_2,e_4) ),
inference(factoring,[status(thm)],[p32281]) ).
cnf(p28607,plain,
( equalish(e_3,X0)
| ~ product(e_2,X0,e_1)
| equalish(e_3,e_2)
| product(e_1,e_2,e_3)
| equalish(e_2,e_4) ),
inference(resolution,[status(thm)],[p28604,c39]) ).
cnf(p32380,plain,
( equalish(e_3,e_4)
| equalish(e_3,e_2)
| product(e_1,e_2,e_3)
| equalish(e_2,e_4)
| equalish(e_3,e_4)
| equalish(e_3,e_2)
| product(e_1,e_2,e_3)
| equalish(e_2,e_4) ),
inference(resolution,[status(thm)],[p32329,p28607]) ).
cnf(p32513,plain,
( equalish(e_3,e_4)
| equalish(e_3,e_2)
| equalish(e_2,e_4)
| equalish(e_3,e_4)
| equalish(e_3,e_2)
| product(e_1,e_2,e_3)
| equalish(e_2,e_4) ),
inference(factoring,[status(thm)],[p32380]) ).
cnf(p32516,plain,
( equalish(e_3,e_4)
| equalish(e_3,e_2)
| equalish(e_3,e_4)
| equalish(e_3,e_2)
| product(e_1,e_2,e_3)
| equalish(e_2,e_4) ),
inference(factoring,[status(thm)],[p32513]) ).
cnf(p32519,plain,
( equalish(e_3,e_4)
| equalish(e_3,e_4)
| equalish(e_3,e_2)
| product(e_1,e_2,e_3)
| equalish(e_2,e_4) ),
inference(factoring,[status(thm)],[p32516]) ).
cnf(p32521,plain,
( equalish(e_3,e_4)
| equalish(e_3,e_2)
| product(e_1,e_2,e_3)
| equalish(e_2,e_4) ),
inference(factoring,[status(thm)],[p32519]) ).
cnf(p67,plain,
( product(e_3,X0,e_4)
| 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)],[c37,c23]) ).
cnf(p135,plain,
( product(e_3,e_4,e_4)
| product(e_3,e_4,e_3)
| product(e_3,e_4,e_2)
| product(e_3,e_4,e_1) ),
inference(resolution,[status(thm)],[p67,c24]) ).
cnf(p484,plain,
( equalish(e_4,e_3)
| product(e_3,e_4,e_3)
| product(e_3,e_4,e_2)
| product(e_3,e_4,e_1) ),
inference(resolution,[status(thm)],[p135,p69]) ).
cnf(p2256,plain,
( product(X0,e_3,e_4)
| ~ product(e_3,e_3,X0)
| equalish(e_4,e_3)
| product(e_3,e_4,e_2)
| product(e_3,e_4,e_1) ),
inference(resolution,[status(thm)],[p484,c42]) ).
cnf(p2272,plain,
( product(e_3,e_3,e_4)
| equalish(e_4,e_3)
| product(e_3,e_4,e_2)
| product(e_3,e_4,e_1) ),
inference(resolution,[status(thm)],[p2256,c41]) ).
cnf(p2275,plain,
( product(X0,e_3,e_4)
| ~ product(e_2,e_3,X0)
| product(e_3,e_3,e_4)
| equalish(e_4,e_3)
| product(e_3,e_4,e_1) ),
inference(resolution,[status(thm)],[p2272,c42]) ).
cnf(p2313,plain,
( product(e_2,e_3,e_3)
| product(e_2,e_3,e_2)
| product(e_2,e_3,e_1)
| product(e_4,e_3,e_4)
| product(e_3,e_3,e_4)
| equalish(e_4,e_3)
| product(e_3,e_4,e_1) ),
inference(resolution,[status(thm)],[p2275,p122]) ).
cnf(p4634,plain,
( equalish(e_4,e_3)
| product(e_2,e_3,e_3)
| product(e_2,e_3,e_2)
| product(e_2,e_3,e_1)
| product(e_3,e_3,e_4)
| equalish(e_4,e_3)
| product(e_3,e_4,e_1) ),
inference(resolution,[status(thm)],[p2313,p63]) ).
cnf(p4648,plain,
( product(e_2,e_3,e_3)
| product(e_2,e_3,e_2)
| product(e_2,e_3,e_1)
| product(e_3,e_3,e_4)
| equalish(e_4,e_3)
| product(e_3,e_4,e_1) ),
inference(factoring,[status(thm)],[p4634]) ).
cnf(p134,plain,
( product(e_3,e_2,e_4)
| product(e_3,e_2,e_3)
| product(e_3,e_2,e_2)
| product(e_3,e_2,e_1) ),
inference(resolution,[status(thm)],[p67,c22]) ).
cnf(p155,plain,
( equalish(e_4,e_2)
| product(e_2,e_4,e_3)
| product(e_2,e_4,e_2)
| product(e_2,e_4,e_1) ),
inference(resolution,[status(thm)],[p123,p69]) ).
cnf(p159,plain,
( product(X0,e_2,e_4)
| ~ product(e_3,e_2,X0)
| equalish(e_4,e_2)
| product(e_2,e_4,e_2)
| product(e_2,e_4,e_1) ),
inference(resolution,[status(thm)],[p155,c42]) ).
cnf(p457,plain,
( product(e_4,e_2,e_4)
| equalish(e_4,e_2)
| product(e_2,e_4,e_2)
| product(e_2,e_4,e_1)
| product(e_3,e_2,e_3)
| product(e_3,e_2,e_2)
| product(e_3,e_2,e_1) ),
inference(resolution,[status(thm)],[p134,p159]) ).
cnf(p464,plain,
( equalish(e_4,e_2)
| equalish(e_4,e_2)
| product(e_2,e_4,e_2)
| product(e_2,e_4,e_1)
| product(e_3,e_2,e_3)
| product(e_3,e_2,e_2)
| product(e_3,e_2,e_1) ),
inference(resolution,[status(thm)],[p457,p63]) ).
cnf(p471,plain,
( equalish(e_4,e_2)
| product(e_2,e_4,e_2)
| product(e_2,e_4,e_1)
| product(e_3,e_2,e_3)
| product(e_3,e_2,e_2)
| product(e_3,e_2,e_1) ),
inference(factoring,[status(thm)],[p464]) ).
cnf(p474,plain,
( equalish(e_2,X0)
| ~ product(e_3,X0,e_3)
| equalish(e_4,e_2)
| product(e_2,e_4,e_2)
| product(e_2,e_4,e_1)
| product(e_3,e_2,e_2)
| product(e_3,e_2,e_1) ),
inference(resolution,[status(thm)],[p471,c39]) ).
cnf(p526,plain,
( equalish(e_2,e_3)
| equalish(e_4,e_2)
| product(e_2,e_4,e_2)
| product(e_2,e_4,e_1)
| product(e_3,e_2,e_2)
| product(e_3,e_2,e_1) ),
inference(resolution,[status(thm)],[p474,c41]) ).
cnf(p534,plain,
( equalish(e_2,e_3)
| equalish(e_2,e_3)
| equalish(e_4,e_2)
| product(e_2,e_4,e_2)
| product(e_2,e_4,e_1)
| product(e_3,e_2,e_1) ),
inference(resolution,[status(thm)],[p526,p69]) ).
cnf(p537,plain,
( equalish(e_2,e_3)
| equalish(e_4,e_2)
| product(e_2,e_4,e_2)
| product(e_2,e_4,e_1)
| product(e_3,e_2,e_1) ),
inference(factoring,[status(thm)],[p534]) ).
cnf(p542,plain,
( product(e_1,e_2,e_4)
| equalish(e_4,e_2)
| product(e_2,e_4,e_2)
| product(e_2,e_4,e_1)
| equalish(e_2,e_3)
| equalish(e_4,e_2)
| product(e_2,e_4,e_2)
| product(e_2,e_4,e_1) ),
inference(resolution,[status(thm)],[p537,p159]) ).
cnf(p2523,plain,
( product(e_1,e_2,e_4)
| equalish(e_4,e_2)
| product(e_2,e_4,e_2)
| equalish(e_2,e_3)
| equalish(e_4,e_2)
| product(e_2,e_4,e_2)
| product(e_2,e_4,e_1) ),
inference(factoring,[status(thm)],[p542]) ).
cnf(p2638,plain,
( product(e_1,e_2,e_4)
| equalish(e_4,e_2)
| equalish(e_2,e_3)
| equalish(e_4,e_2)
| product(e_2,e_4,e_2)
| product(e_2,e_4,e_1) ),
inference(factoring,[status(thm)],[p2523]) ).
cnf(p2640,plain,
( product(e_1,e_2,e_4)
| equalish(e_2,e_3)
| equalish(e_4,e_2)
| product(e_2,e_4,e_2)
| product(e_2,e_4,e_1) ),
inference(factoring,[status(thm)],[p2638]) ).
cnf(p2643,plain,
( equalish(e_4,X0)
| ~ product(e_2,X0,e_2)
| product(e_1,e_2,e_4)
| equalish(e_2,e_3)
| equalish(e_4,e_2)
| product(e_2,e_4,e_1) ),
inference(resolution,[status(thm)],[p2640,c39]) ).
cnf(p2692,plain,
( equalish(e_4,e_2)
| product(e_1,e_2,e_4)
| equalish(e_2,e_3)
| equalish(e_4,e_2)
| product(e_2,e_4,e_1) ),
inference(resolution,[status(thm)],[p2643,c41]) ).
cnf(p2693,plain,
( product(e_1,e_2,e_4)
| equalish(e_2,e_3)
| equalish(e_4,e_2)
| product(e_2,e_4,e_1) ),
inference(factoring,[status(thm)],[p2692]) ).
cnf(p2697,plain,
( equalish(e_2,X0)
| ~ product(X0,e_4,e_1)
| product(e_1,e_2,e_4)
| equalish(e_2,e_3)
| equalish(e_4,e_2) ),
inference(resolution,[status(thm)],[p2693,c40]) ).
cnf(p2708,plain,
( ~ product(e_3,e_4,e_1)
| product(e_1,e_2,e_4)
| equalish(e_2,e_3)
| equalish(e_4,e_2) ),
inference(factoring,[status(thm)],[p2697]) ).
cnf(p4665,plain,
( product(e_1,e_2,e_4)
| equalish(e_2,e_3)
| equalish(e_4,e_2)
| product(e_2,e_3,e_3)
| product(e_2,e_3,e_2)
| product(e_2,e_3,e_1)
| product(e_3,e_3,e_4)
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[p4648,p2708]) ).
cnf(p60,plain,
( equalish(X0,X1)
| ~ product(X0,X0,X1) ),
inference(resolution,[status(thm)],[c38,c41]) ).
cnf(p9701,plain,
( equalish(e_3,e_4)
| product(e_1,e_2,e_4)
| equalish(e_2,e_3)
| equalish(e_4,e_2)
| product(e_2,e_3,e_3)
| product(e_2,e_3,e_2)
| product(e_2,e_3,e_1)
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[p4665,p60]) ).
cnf(p9715,plain,
( equalish(e_3,e_2)
| equalish(e_3,e_4)
| product(e_1,e_2,e_4)
| equalish(e_2,e_3)
| equalish(e_4,e_2)
| product(e_2,e_3,e_2)
| product(e_2,e_3,e_1)
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[p9701,p69]) ).
cnf(p9722,plain,
( equalish(e_2,e_3)
| equalish(e_3,e_2)
| equalish(e_3,e_4)
| product(e_1,e_2,e_4)
| equalish(e_2,e_3)
| equalish(e_4,e_2)
| product(e_2,e_3,e_1)
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[p9715,p63]) ).
cnf(p9757,plain,
( equalish(e_3,e_2)
| equalish(e_3,e_4)
| product(e_1,e_2,e_4)
| equalish(e_2,e_3)
| equalish(e_4,e_2)
| product(e_2,e_3,e_1)
| equalish(e_4,e_3) ),
inference(factoring,[status(thm)],[p9722]) ).
cnf(p9760,plain,
( equalish(e_3,X0)
| ~ product(e_2,X0,e_1)
| equalish(e_3,e_2)
| equalish(e_3,e_4)
| product(e_1,e_2,e_4)
| equalish(e_2,e_3)
| equalish(e_4,e_2)
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[p9757,c39]) ).
cnf(p9781,plain,
( ~ product(e_2,e_4,e_1)
| equalish(e_3,e_2)
| equalish(e_3,e_4)
| product(e_1,e_2,e_4)
| equalish(e_2,e_3)
| equalish(e_4,e_2)
| equalish(e_4,e_3) ),
inference(factoring,[status(thm)],[p9760]) ).
cnf(p475,plain,
( equalish(e_3,e_2)
| equalish(e_4,e_2)
| product(e_2,e_4,e_2)
| product(e_2,e_4,e_1)
| product(e_3,e_2,e_2)
| product(e_3,e_2,e_1) ),
inference(resolution,[status(thm)],[p471,p63]) ).
cnf(p489,plain,
( equalish(e_3,X0)
| ~ product(X0,e_2,e_2)
| equalish(e_3,e_2)
| equalish(e_4,e_2)
| product(e_2,e_4,e_2)
| product(e_2,e_4,e_1)
| product(e_3,e_2,e_1) ),
inference(resolution,[status(thm)],[p475,c40]) ).
cnf(p512,plain,
( equalish(e_3,e_2)
| equalish(e_3,e_2)
| equalish(e_4,e_2)
| product(e_2,e_4,e_2)
| product(e_2,e_4,e_1)
| product(e_3,e_2,e_1) ),
inference(resolution,[status(thm)],[p489,c41]) ).
cnf(p513,plain,
( equalish(e_3,e_2)
| equalish(e_4,e_2)
| product(e_2,e_4,e_2)
| product(e_2,e_4,e_1)
| product(e_3,e_2,e_1) ),
inference(factoring,[status(thm)],[p512]) ).
cnf(p521,plain,
( product(e_1,e_2,e_4)
| equalish(e_4,e_2)
| product(e_2,e_4,e_2)
| product(e_2,e_4,e_1)
| equalish(e_3,e_2)
| equalish(e_4,e_2)
| product(e_2,e_4,e_2)
| product(e_2,e_4,e_1) ),
inference(resolution,[status(thm)],[p513,p159]) ).
cnf(p2413,plain,
( product(e_1,e_2,e_4)
| equalish(e_4,e_2)
| product(e_2,e_4,e_2)
| equalish(e_3,e_2)
| equalish(e_4,e_2)
| product(e_2,e_4,e_2)
| product(e_2,e_4,e_1) ),
inference(factoring,[status(thm)],[p521]) ).
cnf(p2432,plain,
( product(e_1,e_2,e_4)
| equalish(e_4,e_2)
| equalish(e_3,e_2)
| equalish(e_4,e_2)
| product(e_2,e_4,e_2)
| product(e_2,e_4,e_1) ),
inference(factoring,[status(thm)],[p2413]) ).
cnf(p2434,plain,
( product(e_1,e_2,e_4)
| equalish(e_3,e_2)
| equalish(e_4,e_2)
| product(e_2,e_4,e_2)
| product(e_2,e_4,e_1) ),
inference(factoring,[status(thm)],[p2432]) ).
cnf(p2437,plain,
( equalish(e_4,X0)
| ~ product(e_2,X0,e_2)
| product(e_1,e_2,e_4)
| equalish(e_3,e_2)
| equalish(e_4,e_2)
| product(e_2,e_4,e_1) ),
inference(resolution,[status(thm)],[p2434,c39]) ).
cnf(p2494,plain,
( equalish(e_4,e_2)
| product(e_1,e_2,e_4)
| equalish(e_3,e_2)
| equalish(e_4,e_2)
| product(e_2,e_4,e_1) ),
inference(resolution,[status(thm)],[p2437,c41]) ).
cnf(p2495,plain,
( product(e_1,e_2,e_4)
| equalish(e_3,e_2)
| equalish(e_4,e_2)
| product(e_2,e_4,e_1) ),
inference(factoring,[status(thm)],[p2494]) ).
cnf(p9790,plain,
( product(e_1,e_2,e_4)
| equalish(e_3,e_2)
| equalish(e_4,e_2)
| equalish(e_3,e_2)
| equalish(e_3,e_4)
| product(e_1,e_2,e_4)
| equalish(e_2,e_3)
| equalish(e_4,e_2)
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[p9781,p2495]) ).
cnf(p16893,plain,
( equalish(e_3,e_2)
| equalish(e_4,e_2)
| equalish(e_3,e_2)
| equalish(e_3,e_4)
| product(e_1,e_2,e_4)
| equalish(e_2,e_3)
| equalish(e_4,e_2)
| equalish(e_4,e_3) ),
inference(factoring,[status(thm)],[p9790]) ).
cnf(p16906,plain,
( equalish(e_3,e_2)
| equalish(e_3,e_2)
| equalish(e_3,e_4)
| product(e_1,e_2,e_4)
| equalish(e_2,e_3)
| equalish(e_4,e_2)
| equalish(e_4,e_3) ),
inference(factoring,[status(thm)],[p16893]) ).
cnf(p16908,plain,
( equalish(e_3,e_2)
| equalish(e_3,e_4)
| product(e_1,e_2,e_4)
| equalish(e_2,e_3)
| equalish(e_4,e_2)
| equalish(e_4,e_3) ),
inference(factoring,[status(thm)],[p16906]) ).
cnf(p16910,plain,
( equalish(e_4,X0)
| ~ product(e_1,e_2,X0)
| equalish(e_3,e_2)
| equalish(e_3,e_4)
| equalish(e_2,e_3)
| equalish(e_4,e_2)
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[p16908,c38]) ).
cnf(p16926,plain,
( ~ product(e_1,e_2,e_3)
| equalish(e_3,e_2)
| equalish(e_3,e_4)
| equalish(e_2,e_3)
| equalish(e_4,e_2)
| equalish(e_4,e_3) ),
inference(factoring,[status(thm)],[p16910]) ).
cnf(p32550,plain,
( equalish(e_3,e_2)
| equalish(e_3,e_4)
| equalish(e_2,e_3)
| equalish(e_4,e_2)
| equalish(e_4,e_3)
| equalish(e_3,e_4)
| equalish(e_3,e_2)
| equalish(e_2,e_4) ),
inference(resolution,[status(thm)],[p32521,p16926]) ).
cnf(p33641,plain,
( equalish(e_3,e_4)
| equalish(e_2,e_3)
| equalish(e_4,e_2)
| equalish(e_4,e_3)
| equalish(e_3,e_4)
| equalish(e_3,e_2)
| equalish(e_2,e_4) ),
inference(factoring,[status(thm)],[p32550]) ).
cnf(p33643,plain,
( equalish(e_2,e_3)
| equalish(e_4,e_2)
| equalish(e_4,e_3)
| equalish(e_3,e_4)
| equalish(e_3,e_2)
| equalish(e_2,e_4) ),
inference(factoring,[status(thm)],[p33641]) ).
cnf(f36,axiom,
~ equalish(e_4,e_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_4_is_not_e_3) ).
fof(f36_nnf,plain,
~ equalish(e_4,e_3),
inference(nnf_transformation,[status(thm)],[f36]) ).
fof(f36_sk,plain,
~ equalish(e_4,e_3),
inference(skolemisation,[status(esa)],[f36_nnf]) ).
cnf(c36,plain,
~ equalish(e_4,e_3),
inference(cnf_transformation,[status(esa)],[f36_sk]) ).
cnf(p33644,plain,
( equalish(e_2,e_3)
| equalish(e_4,e_2)
| equalish(e_3,e_4)
| equalish(e_3,e_2)
| equalish(e_2,e_4) ),
inference(resolution,[status(thm)],[p33643,c36]) ).
cnf(f35,axiom,
~ equalish(e_4,e_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_4_is_not_e_2) ).
fof(f35_nnf,plain,
~ equalish(e_4,e_2),
inference(nnf_transformation,[status(thm)],[f35]) ).
fof(f35_sk,plain,
~ equalish(e_4,e_2),
inference(skolemisation,[status(esa)],[f35_nnf]) ).
cnf(c35,plain,
~ equalish(e_4,e_2),
inference(cnf_transformation,[status(esa)],[f35_sk]) ).
cnf(p33645,plain,
( equalish(e_2,e_3)
| equalish(e_3,e_4)
| equalish(e_3,e_2)
| equalish(e_2,e_4) ),
inference(resolution,[status(thm)],[p33644,c35]) ).
cnf(f33,axiom,
~ equalish(e_3,e_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_3_is_not_e_4) ).
fof(f33_nnf,plain,
~ equalish(e_3,e_4),
inference(nnf_transformation,[status(thm)],[f33]) ).
fof(f33_sk,plain,
~ equalish(e_3,e_4),
inference(skolemisation,[status(esa)],[f33_nnf]) ).
cnf(c33,plain,
~ equalish(e_3,e_4),
inference(cnf_transformation,[status(esa)],[f33_sk]) ).
cnf(p33656,plain,
( equalish(e_2,e_3)
| equalish(e_3,e_2)
| equalish(e_2,e_4) ),
inference(resolution,[status(thm)],[p33645,c33]) ).
cnf(f32,axiom,
~ equalish(e_3,e_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_3_is_not_e_2) ).
fof(f32_nnf,plain,
~ equalish(e_3,e_2),
inference(nnf_transformation,[status(thm)],[f32]) ).
fof(f32_sk,plain,
~ equalish(e_3,e_2),
inference(skolemisation,[status(esa)],[f32_nnf]) ).
cnf(c32,plain,
~ equalish(e_3,e_2),
inference(cnf_transformation,[status(esa)],[f32_sk]) ).
cnf(p33657,plain,
( equalish(e_2,e_3)
| equalish(e_2,e_4) ),
inference(resolution,[status(thm)],[p33656,c32]) ).
cnf(f30,axiom,
~ equalish(e_2,e_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_2_is_not_e_4) ).
fof(f30_nnf,plain,
~ equalish(e_2,e_4),
inference(nnf_transformation,[status(thm)],[f30]) ).
fof(f30_sk,plain,
~ equalish(e_2,e_4),
inference(skolemisation,[status(esa)],[f30_nnf]) ).
cnf(c30,plain,
~ equalish(e_2,e_4),
inference(cnf_transformation,[status(esa)],[f30_sk]) ).
cnf(p33658,plain,
equalish(e_2,e_3),
inference(resolution,[status(thm)],[p33657,c30]) ).
cnf(f29,axiom,
~ equalish(e_2,e_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_2_is_not_e_3) ).
fof(f29_nnf,plain,
~ equalish(e_2,e_3),
inference(nnf_transformation,[status(thm)],[f29]) ).
fof(f29_sk,plain,
~ equalish(e_2,e_3),
inference(skolemisation,[status(esa)],[f29_nnf]) ).
cnf(c29,plain,
~ equalish(e_2,e_3),
inference(cnf_transformation,[status(esa)],[f29_sk]) ).
cnf(p33659,plain,
$false,
inference(resolution,[status(thm)],[p33658,c29]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : GRP127-3.004 : TPTP v9.3.1. Released v1.2.0.
% 0.00/0.02 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.05/5.31 % Computer : n012.cluster.edu
% 0.05/5.31 % Model : x86_64 x86_64
% 0.05/5.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.05/5.31 % Memory : 8046.5625MB
% 0.05/5.31 % OS : Linux 6.8.0-71-generic
% 0.05/5.31 % CPULimit : 300
% 0.05/5.31 % WCLimit : 300
% 0.05/5.31 % DateTime : Wed Sep 23 13:43:07 UTC 2026
% 0.05/5.31 % CPUTime :
% 0.05/5.31 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 94.07/73.92 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 94.07/73.92 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------