%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP703+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n013.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:28:14 PM UTC 2026
% Result : Theorem 4.18s 0.93s
% Output : Proof 4.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 42
% Number of leaves : 14
% Syntax : Number of formulae : 145 ( 140 unt; 0 def)
% Number of atoms : 155 ( 154 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 48 ( 38 ~; 6 |; 4 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 2 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 9 con; 0-4 aty)
% Number of variables : 197 ( 2 sgn 70 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f11,axiom,
! [B,A] : op_e = mult(mult(rd(op_c,mult(A,B)),B),A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f12) ).
fof(f11_nnf,plain,
! [B,A] : op_e = mult(mult(rd(op_c,mult(A,B)),B),A),
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
! [A,B] : op_e = mult(mult(rd(op_c,mult(A,B)),B),A),
inference(skolemisation,[status(esa)],[f11_nnf]) ).
cnf(c11,plain,
op_e = mult(mult(rd(op_c,mult(X1,X0)),X0),X1),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(t11,plain,
mult(mult(rd(op_c,mult(X1,X2)),X2),X1) = op_e,
inference(equality_encoding,[status(esa)],[c11]) ).
cnf(t88,plain,
mult(mult(rd(op_c,mult(X1,X2)),X2),X1) = op_e,
inference(orient,[status(thm)],[t11]) ).
fof(f12,axiom,
! [B,A] : op_f = mult(A,mult(B,ld(mult(A,B),op_c))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f13) ).
fof(f12_nnf,plain,
! [B,A] : op_f = mult(A,mult(B,ld(mult(A,B),op_c))),
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
! [A,B] : op_f = mult(A,mult(B,ld(mult(A,B),op_c))),
inference(skolemisation,[status(esa)],[f12_nnf]) ).
cnf(c12,plain,
op_f = mult(X1,mult(X0,ld(mult(X1,X0),op_c))),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(t8,plain,
mult(X1,mult(X2,ld(mult(X1,X2),op_c))) = op_f,
inference(equality_encoding,[status(esa)],[c12]) ).
cnf(t49,plain,
mult(X1,mult(X2,ld(mult(X1,X2),op_c))) = op_f,
inference(orient,[status(thm)],[t8]) ).
fof(f5,axiom,
! [A] : mult(unit,A) = A,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f06) ).
fof(f5_nnf,plain,
! [A] : mult(unit,A) = A,
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [A] : mult(unit,A) = A,
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c5,plain,
mult(unit,X0) = X0,
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(t1,plain,
mult(unit,X1) = X1,
inference(equality_encoding,[status(esa)],[c5]) ).
cnf(t19,plain,
mult(unit,X1) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t51,plain,
op_f = mult(X1,ld(mult(unit,X1),op_c)),
inference(cp,[status(thm)],[t49,t19]) ).
cnf(t1261,plain,
op_f = mult(X1,ld(X1,op_c)),
inference(step,[status(thm)],[t51,t19]) ).
fof(f0,axiom,
! [B,A] : mult(A,ld(A,B)) = B,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f01) ).
fof(f0_nnf,plain,
! [B,A] : mult(A,ld(A,B)) = B,
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [A,B] : mult(A,ld(A,B)) = B,
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
mult(X1,ld(X1,X0)) = X0,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t5,plain,
mult(X1,ld(X1,X2)) = X2,
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t15,plain,
mult(X1,ld(X1,X2)) = X2,
inference(orient,[status(thm)],[t5]) ).
cnf(t1262,plain,
op_f = op_c,
inference(step,[status(thm)],[t1261,t15]) ).
cnf(t117,plain,
op_c = op_f,
inference(orient,[status(thm)],[t1262]) ).
cnf(t1271,plain,
mult(mult(rd(op_f,mult(X1,X2)),X2),X1) = op_e,
inference(step,[status(thm)],[t88,t117]) ).
cnf(t123,plain,
mult(mult(rd(op_f,mult(X1,X2)),X2),X1) = op_e,
inference(rw,[status(thm)],[t1271]) ).
cnf(t1189,plain,
mult(mult(rd(op_f,mult(X1,X2)),X2),X1) = op_e,
inference(orient,[status(thm)],[t123]) ).
fof(f6,axiom,
! [C,B,A] : mult(A,mult(B,mult(B,C))) = mult(mult(mult(A,B),B),C),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f07) ).
fof(f6_nnf,plain,
! [C,B,A] : mult(A,mult(B,mult(B,C))) = mult(mult(mult(A,B),B),C),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [A,B,C] : mult(A,mult(B,mult(B,C))) = mult(mult(mult(A,B),B),C),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c6,plain,
mult(X2,mult(X1,mult(X1,X0))) = mult(mult(mult(X2,X1),X1),X0),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(t13,plain,
mult(mult(mult(X1,X2),X2),X3) = mult(X1,mult(X2,mult(X2,X3))),
inference(equality_encoding,[status(esa)],[c6]) ).
cnf(t30,plain,
mult(mult(mult(X1,X2),X2),X3) = mult(X1,mult(X2,mult(X2,X3))),
inference(orient,[status(thm)],[t13]) ).
fof(f4,axiom,
! [A] : mult(A,unit) = A,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f05) ).
fof(f4_nnf,plain,
! [A] : mult(A,unit) = A,
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [A] : mult(A,unit) = A,
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c4,plain,
mult(X0,unit) = X0,
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(t0,plain,
mult(X1,unit) = X1,
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(t16,plain,
mult(X1,unit) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t32,plain,
mult(X1,mult(X2,mult(X2,unit))) = mult(mult(X1,X2),X2),
inference(cp,[status(thm)],[t30,t16]) ).
cnf(t1277,plain,
mult(X1,mult(X2,X2)) = mult(mult(X1,X2),X2),
inference(step,[status(thm)],[t32,t16]) ).
cnf(t163,plain,
mult(mult(X1,X2),X2) = mult(X1,mult(X2,X2)),
inference(orient,[status(thm)],[t1277]) ).
cnf(t1190,plain,
op_e = mult(rd(op_f,mult(X1,X1)),mult(X1,X1)),
inference(cp,[status(thm)],[t1189,t163]) ).
fof(f2,axiom,
! [B,A] : mult(rd(A,B),B) = A,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f03) ).
fof(f2_nnf,plain,
! [B,A] : mult(rd(A,B),B) = A,
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [A,B] : mult(rd(A,B),B) = A,
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
mult(rd(X1,X0),X0) = X1,
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(t6,plain,
mult(rd(X1,X2),X2) = X1,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t17,plain,
mult(rd(X1,X2),X2) = X1,
inference(orient,[status(thm)],[t6]) ).
cnf(t1292,plain,
op_e = op_f,
inference(step,[status(thm)],[t1190,t17]) ).
cnf(t1257,plain,
op_e = op_f,
inference(orient,[status(thm)],[t1292]) ).
fof(f10,axiom,
! [A] : op_d = ld(A,mult(op_c,A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f11) ).
fof(f10_nnf,plain,
! [A] : op_d = ld(A,mult(op_c,A)),
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
! [A] : op_d = ld(A,mult(op_c,A)),
inference(skolemisation,[status(esa)],[f10_nnf]) ).
cnf(c10,plain,
op_d = ld(X0,mult(op_c,X0)),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(t4,plain,
ld(X1,mult(op_c,X1)) = op_d,
inference(equality_encoding,[status(esa)],[c10]) ).
cnf(t111,plain,
ld(X1,mult(op_c,X1)) = op_d,
inference(orient,[status(thm)],[t4]) ).
cnf(t1263,plain,
ld(X1,mult(op_f,X1)) = op_d,
inference(step,[status(thm)],[t111,t117]) ).
cnf(t118,plain,
ld(X1,mult(op_f,X1)) = op_d,
inference(rw,[status(thm)],[t1263]) ).
cnf(t130,plain,
ld(X1,mult(op_f,X1)) = op_d,
inference(orient,[status(thm)],[t118]) ).
cnf(t135,plain,
mult(op_f,X1) = mult(X1,op_d),
inference(cp,[status(thm)],[t15,t130]) ).
fof(f1,axiom,
! [B,A] : ld(A,mult(A,B)) = B,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f02) ).
fof(f1_nnf,plain,
! [B,A] : ld(A,mult(A,B)) = B,
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [A,B] : ld(A,mult(A,B)) = B,
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
ld(X1,mult(X1,X0)) = X0,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(t3,plain,
ld(X1,mult(X1,X2)) = X2,
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(t21,plain,
ld(X1,mult(X1,X2)) = X2,
inference(orient,[status(thm)],[t3]) ).
cnf(t131,plain,
op_d = op_f,
inference(cp,[status(thm)],[t130,t21]) ).
cnf(t137,plain,
op_d = op_f,
inference(orient,[status(thm)],[t131]) ).
cnf(t1276,plain,
mult(op_f,X1) = mult(X1,op_f),
inference(step,[status(thm)],[t135,t137]) ).
cnf(t158,plain,
mult(op_f,X1) = mult(X1,op_f),
inference(orient,[status(thm)],[t1276]) ).
fof(f7,axiom,
! [B,A] : mult(op_c,mult(A,B)) = mult(mult(op_c,A),B),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f08) ).
fof(f7_nnf,plain,
! [B,A] : mult(op_c,mult(A,B)) = mult(mult(op_c,A),B),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [A,B] : mult(op_c,mult(A,B)) = mult(mult(op_c,A),B),
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c7,plain,
mult(op_c,mult(X1,X0)) = mult(mult(op_c,X1),X0),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(t12,plain,
mult(op_c,mult(X1,X2)) = mult(mult(op_c,X1),X2),
inference(equality_encoding,[status(esa)],[c7]) ).
cnf(t78,plain,
mult(mult(op_c,X1),X2) = mult(op_c,mult(X1,X2)),
inference(orient,[status(thm)],[t12]) ).
cnf(t1264,plain,
mult(mult(op_f,X1),X2) = mult(op_c,mult(X1,X2)),
inference(step,[status(thm)],[t78,t117]) ).
cnf(t1265,plain,
mult(mult(op_f,X1),X2) = mult(op_f,mult(X1,X2)),
inference(step,[status(thm)],[t1264,t117]) ).
cnf(t119,plain,
mult(mult(op_f,X1),X2) = mult(op_f,mult(X1,X2)),
inference(rw,[status(thm)],[t1265]) ).
cnf(t175,plain,
mult(mult(op_f,X1),X2) = mult(op_f,mult(X1,X2)),
inference(orient,[status(thm)],[t119]) ).
fof(f8,axiom,
! [B,A] : mult(A,mult(B,op_c)) = mult(mult(A,B),op_c),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f09) ).
fof(f8_nnf,plain,
! [B,A] : mult(A,mult(B,op_c)) = mult(mult(A,B),op_c),
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
! [A,B] : mult(A,mult(B,op_c)) = mult(mult(A,B),op_c),
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c8,plain,
mult(X1,mult(X0,op_c)) = mult(mult(X1,X0),op_c),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(t9,plain,
mult(mult(X1,X2),op_c) = mult(X1,mult(X2,op_c)),
inference(equality_encoding,[status(esa)],[c8]) ).
cnf(t40,plain,
mult(mult(X1,X2),op_c) = mult(X1,mult(X2,op_c)),
inference(orient,[status(thm)],[t9]) ).
cnf(t1268,plain,
mult(mult(X1,X2),op_f) = mult(X1,mult(X2,op_c)),
inference(step,[status(thm)],[t40,t117]) ).
cnf(t1269,plain,
mult(mult(X1,X2),op_f) = mult(X1,mult(X2,op_f)),
inference(step,[status(thm)],[t1268,t117]) ).
cnf(t121,plain,
mult(mult(X1,X2),op_f) = mult(X1,mult(X2,op_f)),
inference(rw,[status(thm)],[t1269]) ).
cnf(t1279,plain,
mult(op_f,mult(X1,X2)) = mult(X1,mult(X2,op_f)),
inference(step,[status(thm)],[t121,t158]) ).
cnf(t195,plain,
mult(op_f,mult(X1,X2)) = mult(X1,mult(X2,op_f)),
inference(orient,[status(thm)],[t1279]) ).
cnf(t180,plain,
mult(op_f,mult(X1,X2)) = mult(mult(X1,op_f),X2),
inference(cp,[status(thm)],[t175,t158]) ).
fof(f9,axiom,
! [B,A] : mult(A,mult(op_c,B)) = mult(mult(A,op_c),B),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f10) ).
fof(f9_nnf,plain,
! [B,A] : mult(A,mult(op_c,B)) = mult(mult(A,op_c),B),
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
! [A,B] : mult(A,mult(op_c,B)) = mult(mult(A,op_c),B),
inference(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c9,plain,
mult(X1,mult(op_c,X0)) = mult(mult(X1,op_c),X0),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(t10,plain,
mult(mult(X1,op_c),X2) = mult(X1,mult(op_c,X2)),
inference(equality_encoding,[status(esa)],[c9]) ).
cnf(t65,plain,
mult(mult(X1,op_c),X2) = mult(X1,mult(op_c,X2)),
inference(orient,[status(thm)],[t10]) ).
cnf(t1266,plain,
mult(mult(X1,op_f),X2) = mult(X1,mult(op_c,X2)),
inference(step,[status(thm)],[t65,t117]) ).
cnf(t1267,plain,
mult(mult(X1,op_f),X2) = mult(X1,mult(op_f,X2)),
inference(step,[status(thm)],[t1266,t117]) ).
cnf(t120,plain,
mult(mult(X1,op_f),X2) = mult(X1,mult(op_f,X2)),
inference(rw,[status(thm)],[t1267]) ).
cnf(t184,plain,
mult(mult(X1,op_f),X2) = mult(X1,mult(op_f,X2)),
inference(orient,[status(thm)],[t120]) ).
cnf(t1281,plain,
mult(op_f,mult(X1,X2)) = mult(X1,mult(op_f,X2)),
inference(step,[status(thm)],[t180,t184]) ).
cnf(t245,plain,
mult(op_f,mult(X1,X2)) = mult(X1,mult(op_f,X2)),
inference(orient,[status(thm)],[t1281]) ).
cnf(t2,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t25,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t2]) ).
fof(f13,conjecture,
! [X2,X3] :
( mult(X2,mult(op_e,X3)) = mult(mult(X2,op_e),X3)
& mult(X2,mult(X3,op_e)) = mult(mult(X2,X3),op_e)
& mult(op_e,mult(X2,X3)) = mult(mult(op_e,X2),X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals) ).
fof(f13_neg,negated_conjecture,
~ ! [X2,X3] :
( mult(X2,mult(op_e,X3)) = mult(mult(X2,op_e),X3)
& mult(X2,mult(X3,op_e)) = mult(mult(X2,X3),op_e)
& mult(op_e,mult(X2,X3)) = mult(mult(op_e,X2),X3) ),
inference(negated_conjecture,[status(cth)],[f13]) ).
fof(f13_nnf,plain,
? [X2,X3] :
( mult(X2,mult(op_e,X3)) != mult(mult(X2,op_e),X3)
| mult(X2,mult(X3,op_e)) != mult(mult(X2,X3),op_e)
| mult(op_e,mult(X2,X3)) != mult(mult(op_e,X2),X3) ),
inference(nnf_transformation,[status(thm)],[f13_neg]) ).
fof(f13_sk,plain,
( mult(sk0,mult(op_e,sk1)) != mult(mult(sk0,op_e),sk1)
| mult(sk0,mult(sk1,op_e)) != mult(mult(sk0,sk1),op_e)
| mult(op_e,mult(sk0,sk1)) != mult(mult(op_e,sk0),sk1) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0,sk1])],[f13_nnf]) ).
cnf(c13,plain,
( mult(sk0,mult(op_e,sk1)) != mult(mult(sk0,op_e),sk1)
| mult(sk0,mult(sk1,op_e)) != mult(mult(sk0,sk1),op_e)
| mult(op_e,mult(sk0,sk1)) != mult(mult(op_e,sk0),sk1) ),
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c13]) ).
cnf(g0_0,plain,
true != ifeq(mult(op_e,mult(sk0,sk1)),mult(mult(op_e,sk0),sk1),ifeq(mult(sk0,mult(sk1,op_e)),mult(mult(sk0,sk1),op_e),ifeq(mult(sk0,mult(op_e,sk1)),mult(mult(sk0,op_e),sk1),false,true),true),true),
inference(rw,[status(thm)],[goal_0]) ).
cnf(g0_1,plain,
true != ifeq(mult(op_e,mult(sk0,sk1)),mult(mult(op_e,sk0),sk1),ifeq(mult(sk0,mult(sk1,op_e)),mult(mult(sk0,sk1),op_e),ifeq(mult(sk0,mult(op_e,sk1)),mult(mult(sk0,op_f),sk1),false,true),true),true),
inference(rw,[status(thm)],[g0_0,t1257]) ).
cnf(g0_2,plain,
true != ifeq(mult(op_e,mult(sk0,sk1)),mult(mult(op_e,sk0),sk1),ifeq(mult(sk0,mult(sk1,op_e)),mult(mult(sk0,sk1),op_e),ifeq(mult(sk0,mult(op_e,sk1)),mult(mult(op_f,sk0),sk1),false,true),true),true),
inference(rw,[status(thm)],[g0_1,t158]) ).
cnf(g0_3,plain,
true != ifeq(mult(op_e,mult(sk0,sk1)),mult(mult(op_e,sk0),sk1),ifeq(mult(sk0,mult(sk1,op_e)),mult(mult(sk0,sk1),op_e),ifeq(mult(sk0,mult(op_e,sk1)),mult(op_f,mult(sk0,sk1)),false,true),true),true),
inference(rw,[status(thm)],[g0_2,t175]) ).
cnf(g0_4,plain,
true != ifeq(mult(op_e,mult(sk0,sk1)),mult(mult(op_e,sk0),sk1),ifeq(mult(sk0,mult(sk1,op_e)),mult(mult(sk0,sk1),op_e),ifeq(mult(sk0,mult(op_e,sk1)),mult(mult(sk0,sk1),op_f),false,true),true),true),
inference(rw,[status(thm)],[g0_3,t158]) ).
cnf(g0_5,plain,
true != ifeq(mult(op_e,mult(sk0,sk1)),mult(mult(op_e,sk0),sk1),ifeq(mult(sk0,mult(sk1,op_e)),mult(mult(sk0,sk1),op_e),ifeq(mult(sk0,mult(op_f,sk1)),mult(mult(sk0,sk1),op_f),false,true),true),true),
inference(rw,[status(thm)],[g0_4,t1257]) ).
cnf(g0_6,plain,
true != ifeq(mult(op_e,mult(sk0,sk1)),mult(mult(op_e,sk0),sk1),ifeq(mult(sk0,mult(sk1,op_e)),mult(mult(sk0,sk1),op_e),ifeq(mult(sk0,mult(sk1,op_f)),mult(mult(sk0,sk1),op_f),false,true),true),true),
inference(rw,[status(thm)],[g0_5,t158]) ).
cnf(g0_7,plain,
true != ifeq(mult(op_e,mult(sk0,sk1)),mult(mult(op_e,sk0),sk1),ifeq(mult(sk0,mult(sk1,op_e)),mult(mult(sk0,sk1),op_e),ifeq(mult(sk0,mult(sk1,op_f)),mult(op_f,mult(sk0,sk1)),false,true),true),true),
inference(rw,[status(thm)],[g0_6,t158]) ).
cnf(g0_8,plain,
true != ifeq(mult(op_e,mult(sk0,sk1)),mult(mult(op_e,sk0),sk1),ifeq(mult(sk0,mult(sk1,op_e)),mult(mult(sk0,sk1),op_e),ifeq(mult(sk0,mult(sk1,op_f)),mult(sk0,mult(sk1,op_f)),false,true),true),true),
inference(rw,[status(thm)],[g0_7,t195]) ).
cnf(g0_9,plain,
true != ifeq(mult(op_e,mult(sk0,sk1)),mult(mult(op_e,sk0),sk1),ifeq(mult(sk0,mult(sk1,op_e)),mult(mult(sk0,sk1),op_e),ifeq(mult(sk0,mult(op_f,sk1)),mult(sk0,mult(sk1,op_f)),false,true),true),true),
inference(rw,[status(thm)],[g0_8,t158]) ).
cnf(g0_10,plain,
true != ifeq(mult(op_e,mult(sk0,sk1)),mult(mult(op_e,sk0),sk1),ifeq(mult(sk0,mult(sk1,op_e)),mult(mult(sk0,sk1),op_e),ifeq(mult(sk0,mult(op_f,sk1)),mult(sk0,mult(op_f,sk1)),false,true),true),true),
inference(rw,[status(thm)],[g0_9,t158]) ).
cnf(g0_11,plain,
true != ifeq(mult(op_e,mult(sk0,sk1)),mult(mult(op_e,sk0),sk1),ifeq(mult(sk0,mult(sk1,op_e)),mult(mult(sk0,sk1),op_e),ifeq(mult(op_f,mult(sk0,sk1)),mult(sk0,mult(op_f,sk1)),false,true),true),true),
inference(rw,[status(thm)],[g0_10,t245]) ).
cnf(g0_12,plain,
true != ifeq(mult(op_e,mult(sk0,sk1)),mult(mult(op_e,sk0),sk1),ifeq(mult(sk0,mult(sk1,op_e)),mult(mult(sk0,sk1),op_f),ifeq(mult(op_f,mult(sk0,sk1)),mult(sk0,mult(op_f,sk1)),false,true),true),true),
inference(rw,[status(thm)],[g0_11,t1257]) ).
cnf(g0_13,plain,
true != ifeq(mult(op_e,mult(sk0,sk1)),mult(mult(op_e,sk0),sk1),ifeq(mult(sk0,mult(sk1,op_e)),mult(mult(sk0,sk1),op_f),ifeq(mult(op_f,mult(sk0,sk1)),mult(sk0,mult(sk1,op_f)),false,true),true),true),
inference(rw,[status(thm)],[g0_12,t158]) ).
cnf(g0_14,plain,
true != ifeq(mult(op_e,mult(sk0,sk1)),mult(mult(op_e,sk0),sk1),ifeq(mult(sk0,mult(sk1,op_e)),mult(op_f,mult(sk0,sk1)),ifeq(mult(op_f,mult(sk0,sk1)),mult(sk0,mult(sk1,op_f)),false,true),true),true),
inference(rw,[status(thm)],[g0_13,t158]) ).
cnf(g0_15,plain,
true != ifeq(mult(op_e,mult(sk0,sk1)),mult(mult(op_e,sk0),sk1),ifeq(mult(sk0,mult(sk1,op_e)),mult(op_f,mult(sk0,sk1)),ifeq(mult(sk0,mult(sk1,op_f)),mult(sk0,mult(sk1,op_f)),false,true),true),true),
inference(rw,[status(thm)],[g0_14,t195]) ).
cnf(g0_16,plain,
true != ifeq(mult(op_e,mult(sk0,sk1)),mult(mult(op_e,sk0),sk1),ifeq(mult(sk0,mult(sk1,op_e)),mult(sk0,mult(sk1,op_f)),ifeq(mult(sk0,mult(sk1,op_f)),mult(sk0,mult(sk1,op_f)),false,true),true),true),
inference(rw,[status(thm)],[g0_15,t195]) ).
cnf(g0_17,plain,
true != ifeq(mult(op_e,mult(sk0,sk1)),mult(mult(op_e,sk0),sk1),ifeq(mult(sk0,mult(sk1,op_e)),mult(sk0,mult(sk1,op_f)),false,true),true),
inference(rw,[status(thm)],[g0_16,t25]) ).
cnf(g0_18,plain,
true != ifeq(mult(op_e,mult(sk0,sk1)),mult(mult(op_e,sk0),sk1),ifeq(mult(sk0,mult(sk1,op_f)),mult(sk0,mult(sk1,op_f)),false,true),true),
inference(rw,[status(thm)],[g0_17,t1257]) ).
cnf(g0_19,plain,
true != ifeq(mult(op_e,mult(sk0,sk1)),mult(mult(op_e,sk0),sk1),false,true),
inference(rw,[status(thm)],[g0_18,t25]) ).
cnf(g0_20,plain,
true != ifeq(mult(op_e,mult(sk0,sk1)),mult(mult(op_f,sk0),sk1),false,true),
inference(rw,[status(thm)],[g0_19,t1257]) ).
cnf(g0_21,plain,
true != ifeq(mult(op_e,mult(sk0,sk1)),mult(mult(sk0,op_f),sk1),false,true),
inference(rw,[status(thm)],[g0_20,t158]) ).
cnf(g0_22,plain,
true != ifeq(mult(op_e,mult(sk0,sk1)),mult(sk0,mult(op_f,sk1)),false,true),
inference(rw,[status(thm)],[g0_21,t184]) ).
cnf(g0_23,plain,
true != ifeq(mult(op_e,mult(sk0,sk1)),mult(sk0,mult(sk1,op_f)),false,true),
inference(rw,[status(thm)],[g0_22,t158]) ).
cnf(g0_24,plain,
true != ifeq(mult(op_f,mult(sk0,sk1)),mult(sk0,mult(sk1,op_f)),false,true),
inference(rw,[status(thm)],[g0_23,t1257]) ).
cnf(g0_25,plain,
true != ifeq(mult(sk0,mult(sk1,op_f)),mult(sk0,mult(sk1,op_f)),false,true),
inference(rw,[status(thm)],[g0_24,t195]) ).
cnf(g0_26,plain,
true != false,
inference(rw,[status(thm)],[g0_25,t25]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_26]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP703+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/0.35 % Computer : n013.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.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Wed Sep 23 15:46:05 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 4.18/0.93 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.18/0.93 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------