%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP012+5 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n009.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:24:55 PM UTC 2026
% Result : Theorem 8.90s 1.66s
% Output : Proof 8.90s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 1
% Syntax : Number of formulae : 29 ( 23 unt; 0 def)
% Number of atoms : 95 ( 15 equ)
% Maximal formula atoms : 16 ( 3 avg)
% Number of connectives : 90 ( 24 ~; 18 |; 40 &)
% ( 0 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-3 aty)
% Number of functors : 9 ( 9 usr; 6 con; 0-4 aty)
% Number of variables : 110 ( 0 sgn 70 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f0,conjecture,
! [E] :
( ( ! [X] : product(inverse(X),X,E)
& ! [X] : product(X,inverse(X),E)
& ! [X] : product(E,X,X)
& ! [X] : product(X,E,X)
& ! [X,Y,Z,U,V,W] :
( ( product(X,V,W)
& product(Y,Z,V)
& product(X,Y,U) )
=> product(U,Z,W) )
& ! [X,Y,Z,U,V,W] :
( ( product(U,Z,W)
& product(Y,Z,V)
& product(X,Y,U) )
=> product(X,V,W) )
& ! [X,Y] :
? [Z] : product(X,Y,Z) )
=> ! [U,V,W,X] :
( ( product(V,U,X)
& product(inverse(U),inverse(V),W) )
=> product(inverse(W),inverse(X),E) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_distribution) ).
fof(f0_neg,negated_conjecture,
~ ! [E] :
( ( ! [X] : product(inverse(X),X,E)
& ! [X] : product(X,inverse(X),E)
& ! [X] : product(E,X,X)
& ! [X] : product(X,E,X)
& ! [X,Y,Z,U,V,W] :
( ( product(X,V,W)
& product(Y,Z,V)
& product(X,Y,U) )
=> product(U,Z,W) )
& ! [X,Y,Z,U,V,W] :
( ( product(U,Z,W)
& product(Y,Z,V)
& product(X,Y,U) )
=> product(X,V,W) )
& ! [X,Y] :
? [Z] : product(X,Y,Z) )
=> ! [U,V,W,X] :
( ( product(V,U,X)
& product(inverse(U),inverse(V),W) )
=> product(inverse(W),inverse(X),E) ) ),
inference(negated_conjecture,[status(cth)],[f0]) ).
fof(f0_nnf,plain,
? [E] :
( ? [U,V,W,X] :
( ~ product(inverse(W),inverse(X),E)
& product(V,U,X)
& product(inverse(U),inverse(V),W) )
& ! [X] : product(inverse(X),X,E)
& ! [X] : product(X,inverse(X),E)
& ! [X] : product(E,X,X)
& ! [X] : product(X,E,X)
& ! [X,Y,Z,U,V,W] :
( product(U,Z,W)
| ~ product(X,V,W)
| ~ product(Y,Z,V)
| ~ product(X,Y,U) )
& ! [X,Y,Z,U,V,W] :
( product(X,V,W)
| ~ product(U,Z,W)
| ~ product(Y,Z,V)
| ~ product(X,Y,U) )
& ! [X,Y] :
? [Z] : product(X,Y,Z) ),
inference(nnf_transformation,[status(thm)],[f0_neg]) ).
fof(f0_sk,plain,
! [X,Y,U,Z,V,W] :
( ~ product(inverse(sk4),inverse(sk5),sk0)
& product(sk3,sk2,sk5)
& product(inverse(sk2),inverse(sk3),sk4)
& product(inverse(X),X,sk0)
& product(X,inverse(X),sk0)
& product(sk0,X,X)
& product(X,sk0,X)
& ( product(U,Z,W)
| ~ product(X,V,W)
| ~ product(Y,Z,V)
| ~ product(X,Y,U) )
& ( product(X,V,W)
| ~ product(U,Z,W)
| ~ product(Y,Z,V)
| ~ product(X,Y,U) )
& product(X,Y,sk1(X,Y)) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0,sk1,sk2,sk3,sk4,sk5])],[f0_nnf]) ).
cnf(c1,plain,
( product(X1,X5,X6)
| ~ product(X4,X3,X6)
| ~ product(X2,X3,X5)
| ~ product(X1,X2,X4) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(hi1,negated_conjecture,
ifeq(product(X0,X1,X2),true,ifeq(product(X1,X3,X4),true,ifeq(product(X2,X3,X5),true,product(X0,X4,X5),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(c6,plain,
product(inverse(X1),X1,sk0),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(hi6,negated_conjecture,
product(inverse(X0),X0,sk0) = true,
inference(equality_encoding,[status(esa)],[c6]) ).
cnf(c8,plain,
product(sk3,sk2,sk5),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(hi8,negated_conjecture,
product(sk3,sk2,sk5) = true,
inference(equality_encoding,[status(esa)],[c8]) ).
cnf(c4,plain,
product(sk0,X1,X1),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(hi4,negated_conjecture,
product(sk0,X0,X0) = true,
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(h12,plain,
product(inverse(sk3),sk5,sk2) = true,
inference(hyper_resolution,[status(thm)],[hi1,hi6,hi8,hi4]) ).
cnf(c2,plain,
( product(X4,X3,X6)
| ~ product(X1,X5,X6)
| ~ product(X2,X3,X5)
| ~ product(X1,X2,X4) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(hi2,negated_conjecture,
ifeq(product(X0,X1,X2),true,ifeq(product(X1,X3,X4),true,ifeq(product(X0,X4,X5),true,product(X2,X3,X5),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(c7,plain,
product(inverse(sk2),inverse(sk3),sk4),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(hi7,negated_conjecture,
product(inverse(sk2),inverse(sk3),sk4) = true,
inference(equality_encoding,[status(esa)],[c7]) ).
cnf(h227,plain,
product(sk4,sk5,sk0) = true,
inference(hyper_resolution,[status(thm)],[hi2,hi7,h12,hi6]) ).
cnf(c3,plain,
product(X1,sk0,X1),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(hi3,negated_conjecture,
product(X0,sk0,X0) = true,
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(h252,plain,
product(sk0,sk5,inverse(sk4)) = true,
inference(hyper_resolution,[status(thm)],[hi2,hi6,h227,hi3]) ).
cnf(c5,plain,
product(X1,inverse(X1),sk0),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(hi5,negated_conjecture,
product(X0,inverse(X0),sk0) = true,
inference(equality_encoding,[status(esa)],[c5]) ).
cnf(t32,plain,
product(inverse(sk4),inverse(sk5),sk0) = true,
inference(hyper_resolution,[status(thm)],[hi2,h252,hi5,hi4]) ).
cnf(t327,plain,
product(inverse(sk4),inverse(sk5),sk0) = true,
inference(orient,[status(thm)],[t32]) ).
cnf(c9,plain,
~ product(inverse(sk4),inverse(sk5),sk0),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(goal_0,negated_conjecture,
product(inverse(sk4),inverse(sk5),sk0) != true,
inference(equality_encoding,[status(esa)],[c9]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t327]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP012+5 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.11/0.37 % Computer : n009.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Wed Sep 23 13:13:44 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 8.90/1.66 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 8.90/1.66 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------