%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP683+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/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:28:02 PM UTC 2026
% Result : Theorem 5.67s 6.30s
% Output : Proof 0.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 88
% Number of leaves : 9
% Syntax : Number of formulae : 220 ( 215 unt; 0 def)
% Number of atoms : 225 ( 224 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 19 ( 14 ~; 3 |; 2 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 1 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 5 con; 0-4 aty)
% Number of variables : 510 ( 2 sgn 54 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f4,axiom,
! [D,C,B,A] : ld(ld(A,B),mult(ld(A,B),mult(C,D))) = mult(ld(A,mult(A,C)),D),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',f05) ).
fof(f4_nnf,plain,
! [D,C,B,A] : ld(ld(A,B),mult(ld(A,B),mult(C,D))) = mult(ld(A,mult(A,C)),D),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [A,B,C,D] : ld(ld(A,B),mult(ld(A,B),mult(C,D))) = mult(ld(A,mult(A,C)),D),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c4,plain,
ld(ld(X3,X2),mult(ld(X3,X2),mult(X1,X0))) = mult(ld(X3,mult(X3,X1)),X0),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(t6,plain,
ld(ld(X1,X2),mult(ld(X1,X2),mult(X3,X4))) = mult(ld(X1,mult(X1,X3)),X4),
inference(equality_encoding,[status(esa)],[c4]) ).
fof(f2,axiom,
! [B,A] : mult(A,ld(A,B)) = ld(A,mult(A,B)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',f03) ).
fof(f2_nnf,plain,
! [B,A] : mult(A,ld(A,B)) = ld(A,mult(A,B)),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [A,B] : mult(A,ld(A,B)) = ld(A,mult(A,B)),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
mult(X1,ld(X1,X0)) = ld(X1,mult(X1,X0)),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(t3,plain,
mult(X1,ld(X1,X2)) = ld(X1,mult(X1,X2)),
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t12,plain,
ld(X1,mult(X1,X2)) = mult(X1,ld(X1,X2)),
inference(orient,[status(thm)],[t3]) ).
cnf(t1756,plain,
mult(ld(X1,X2),ld(ld(X1,X2),mult(X3,X4))) = mult(ld(X1,mult(X1,X3)),X4),
inference(step,[status(thm)],[t6,t12]) ).
cnf(t1757,plain,
mult(ld(X1,X2),ld(ld(X1,X2),mult(X3,X4))) = mult(mult(X1,ld(X1,X3)),X4),
inference(step,[status(thm)],[t1756,t12]) ).
cnf(t19,plain,
mult(ld(X1,X2),ld(ld(X1,X2),mult(X3,X4))) = mult(mult(X1,ld(X1,X3)),X4),
inference(orient,[status(thm)],[t1757]) ).
cnf(t20,plain,
mult(mult(X1,ld(X1,X2)),X3) = mult(mult(X1,ld(X1,X4)),ld(ld(X1,mult(X1,X4)),mult(X2,X3))),
inference(cp,[status(thm)],[t19,t12]) ).
cnf(t1800,plain,
mult(mult(X1,ld(X1,X2)),X3) = mult(mult(X1,ld(X1,X4)),ld(mult(X1,ld(X1,X4)),mult(X2,X3))),
inference(step,[status(thm)],[t20,t12]) ).
cnf(t625,plain,
mult(mult(X1,ld(X1,X2)),ld(mult(X1,ld(X1,X2)),mult(X3,X4))) = mult(mult(X1,ld(X1,X3)),X4),
inference(orient,[status(thm)],[t1800]) ).
fof(f0,axiom,
! [A] : ld(A,mult(A,A)) = A,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',f01) ).
fof(f0_nnf,plain,
! [A] : ld(A,mult(A,A)) = A,
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [A] : ld(A,mult(A,A)) = A,
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
ld(X0,mult(X0,X0)) = X0,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t1,plain,
ld(X1,mult(X1,X1)) = X1,
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t9,plain,
ld(X1,mult(X1,X1)) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t1755,plain,
mult(X1,ld(X1,X1)) = X1,
inference(step,[status(thm)],[t9,t12]) ).
cnf(t13,plain,
mult(X1,ld(X1,X1)) = X1,
inference(rw,[status(thm)],[t1755]) ).
cnf(t37,plain,
mult(X1,ld(X1,X1)) = X1,
inference(orient,[status(thm)],[t13]) ).
cnf(t39,plain,
mult(X1,ld(X1,ld(X1,X1))) = ld(X1,X1),
inference(cp,[status(thm)],[t12,t37]) ).
fof(f6,axiom,
! [B,A] : ld(A,mult(A,ld(B,B))) = rd(mult(rd(A,A),B),B),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',f07) ).
fof(f6_nnf,plain,
! [B,A] : ld(A,mult(A,ld(B,B))) = rd(mult(rd(A,A),B),B),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [A,B] : ld(A,mult(A,ld(B,B))) = rd(mult(rd(A,A),B),B),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c6,plain,
ld(X1,mult(X1,ld(X0,X0))) = rd(mult(rd(X1,X1),X0),X0),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(t5,plain,
rd(mult(rd(X1,X1),X2),X2) = ld(X1,mult(X1,ld(X2,X2))),
inference(equality_encoding,[status(esa)],[c6]) ).
cnf(t1758,plain,
rd(mult(rd(X1,X1),X2),X2) = mult(X1,ld(X1,ld(X2,X2))),
inference(step,[status(thm)],[t5,t12]) ).
cnf(t32,plain,
mult(X1,ld(X1,ld(X2,X2))) = rd(mult(rd(X1,X1),X2),X2),
inference(orient,[status(thm)],[t1758]) ).
cnf(t1760,plain,
rd(mult(rd(X1,X1),X1),X1) = ld(X1,X1),
inference(step,[status(thm)],[t39,t32]) ).
fof(f3,axiom,
! [B,A] : mult(rd(A,B),B) = rd(mult(A,B),B),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',f04) ).
fof(f3_nnf,plain,
! [B,A] : mult(rd(A,B),B) = rd(mult(A,B),B),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [A,B] : mult(rd(A,B),B) = rd(mult(A,B),B),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
mult(rd(X1,X0),X0) = rd(mult(X1,X0),X0),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(t4,plain,
rd(mult(X1,X2),X2) = mult(rd(X1,X2),X2),
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(t26,plain,
mult(rd(X1,X2),X2) = rd(mult(X1,X2),X2),
inference(orient,[status(thm)],[t4]) ).
cnf(t1761,plain,
rd(rd(mult(X1,X1),X1),X1) = ld(X1,X1),
inference(step,[status(thm)],[t1760,t26]) ).
fof(f1,axiom,
! [A] : rd(mult(A,A),A) = A,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',f02) ).
fof(f1_nnf,plain,
! [A] : rd(mult(A,A),A) = A,
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [A] : rd(mult(A,A),A) = A,
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
rd(mult(X0,X0),X0) = X0,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(t2,plain,
rd(mult(X1,X1),X1) = X1,
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(t10,plain,
rd(mult(X1,X1),X1) = X1,
inference(orient,[status(thm)],[t2]) ).
cnf(t1762,plain,
rd(X1,X1) = ld(X1,X1),
inference(step,[status(thm)],[t1761,t10]) ).
cnf(t42,plain,
ld(X1,X1) = rd(X1,X1),
inference(orient,[status(thm)],[t1762]) ).
cnf(t629,plain,
mult(mult(X1,ld(X1,X2)),X3) = mult(mult(X1,rd(X1,X1)),ld(mult(X1,ld(X1,X1)),mult(X2,X3))),
inference(cp,[status(thm)],[t625,t42]) ).
cnf(t1763,plain,
mult(X1,rd(X1,X1)) = X1,
inference(step,[status(thm)],[t37,t42]) ).
cnf(t45,plain,
mult(X1,rd(X1,X1)) = X1,
inference(rw,[status(thm)],[t1763]) ).
cnf(t47,plain,
mult(X1,rd(X1,X1)) = X1,
inference(orient,[status(thm)],[t45]) ).
cnf(t1801,plain,
mult(mult(X1,ld(X1,X2)),X3) = mult(X1,ld(mult(X1,ld(X1,X1)),mult(X2,X3))),
inference(step,[status(thm)],[t629,t47]) ).
cnf(t1802,plain,
mult(mult(X1,ld(X1,X2)),X3) = mult(X1,ld(mult(X1,rd(X1,X1)),mult(X2,X3))),
inference(step,[status(thm)],[t1801,t42]) ).
cnf(t1803,plain,
mult(mult(X1,ld(X1,X2)),X3) = mult(X1,ld(X1,mult(X2,X3))),
inference(step,[status(thm)],[t1802,t47]) ).
cnf(t680,plain,
mult(mult(X1,ld(X1,X2)),X3) = mult(X1,ld(X1,mult(X2,X3))),
inference(orient,[status(thm)],[t1803]) ).
cnf(t693,plain,
mult(X1,ld(X1,mult(X1,X2))) = mult(mult(X1,rd(X1,X1)),X2),
inference(cp,[status(thm)],[t680,t42]) ).
cnf(t1810,plain,
mult(X1,mult(X1,ld(X1,X2))) = mult(mult(X1,rd(X1,X1)),X2),
inference(step,[status(thm)],[t693,t12]) ).
cnf(t1811,plain,
mult(X1,mult(X1,ld(X1,X2))) = mult(X1,X2),
inference(step,[status(thm)],[t1810,t47]) ).
cnf(t731,plain,
mult(X1,mult(X1,ld(X1,X2))) = mult(X1,X2),
inference(orient,[status(thm)],[t1811]) ).
cnf(t1764,plain,
mult(X1,ld(X1,rd(X2,X2))) = rd(mult(rd(X1,X1),X2),X2),
inference(step,[status(thm)],[t32,t42]) ).
cnf(t46,plain,
mult(X1,ld(X1,rd(X2,X2))) = rd(mult(rd(X1,X1),X2),X2),
inference(rw,[status(thm)],[t1764]) ).
cnf(t90,plain,
mult(X1,ld(X1,rd(X2,X2))) = rd(mult(rd(X1,X1),X2),X2),
inference(orient,[status(thm)],[t46]) ).
fof(f5,axiom,
! [D,C,B,A] : rd(mult(mult(A,B),rd(C,D)),rd(C,D)) = mult(A,rd(mult(B,D),D)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',f06) ).
fof(f5_nnf,plain,
! [D,C,B,A] : rd(mult(mult(A,B),rd(C,D)),rd(C,D)) = mult(A,rd(mult(B,D),D)),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [A,B,C,D] : rd(mult(mult(A,B),rd(C,D)),rd(C,D)) = mult(A,rd(mult(B,D),D)),
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c5,plain,
rd(mult(mult(X3,X2),rd(X1,X0)),rd(X1,X0)) = mult(X3,rd(mult(X2,X0),X0)),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(t7,plain,
rd(mult(mult(X1,X2),rd(X3,X4)),rd(X3,X4)) = mult(X1,rd(mult(X2,X4),X4)),
inference(equality_encoding,[status(esa)],[c5]) ).
cnf(t14,plain,
rd(mult(mult(X1,X2),rd(X3,X4)),rd(X3,X4)) = mult(X1,rd(mult(X2,X4),X4)),
inference(orient,[status(thm)],[t7]) ).
cnf(t15,plain,
mult(X1,rd(mult(X2,X3),X3)) = rd(mult(mult(X1,X2),X3),rd(mult(X3,X3),X3)),
inference(cp,[status(thm)],[t14,t10]) ).
cnf(t1766,plain,
mult(X1,rd(mult(X2,X3),X3)) = rd(mult(mult(X1,X2),X3),X3),
inference(step,[status(thm)],[t15,t10]) ).
cnf(t61,plain,
mult(X1,rd(mult(X2,X3),X3)) = rd(mult(mult(X1,X2),X3),X3),
inference(orient,[status(thm)],[t1766]) ).
cnf(t1767,plain,
rd(mult(mult(X1,X2),rd(X3,X4)),rd(X3,X4)) = rd(mult(mult(X1,X2),X4),X4),
inference(step,[status(thm)],[t14,t61]) ).
cnf(t62,plain,
rd(mult(mult(X1,X2),rd(X3,X4)),rd(X3,X4)) = rd(mult(mult(X1,X2),X4),X4),
inference(orient,[status(thm)],[t1767]) ).
cnf(t91,plain,
rd(mult(rd(rd(X1,X1),rd(X1,X1)),X1),X1) = mult(rd(X1,X1),rd(rd(X1,X1),rd(X1,X1))),
inference(cp,[status(thm)],[t90,t42]) ).
cnf(t1771,plain,
rd(mult(rd(rd(X1,X1),rd(X1,X1)),X1),X1) = rd(X1,X1),
inference(step,[status(thm)],[t91,t47]) ).
cnf(t113,plain,
rd(mult(rd(rd(X1,X1),rd(X1,X1)),X1),X1) = rd(X1,X1),
inference(orient,[status(thm)],[t1771]) ).
cnf(t115,plain,
rd(mult(mult(rd(rd(X1,X1),rd(X1,X1)),X1),X1),X1) = mult(rd(X1,X1),X1),
inference(cp,[status(thm)],[t26,t113]) ).
cnf(t65,plain,
rd(mult(mult(X1,X2),X2),X2) = mult(X1,X2),
inference(cp,[status(thm)],[t61,t10]) ).
cnf(t79,plain,
rd(mult(mult(X1,X2),X2),X2) = mult(X1,X2),
inference(orient,[status(thm)],[t65]) ).
cnf(t1772,plain,
mult(rd(rd(X1,X1),rd(X1,X1)),X1) = mult(rd(X1,X1),X1),
inference(step,[status(thm)],[t115,t79]) ).
cnf(t1773,plain,
mult(rd(rd(X1,X1),rd(X1,X1)),X1) = rd(mult(X1,X1),X1),
inference(step,[status(thm)],[t1772,t26]) ).
cnf(t1774,plain,
mult(rd(rd(X1,X1),rd(X1,X1)),X1) = X1,
inference(step,[status(thm)],[t1773,t10]) ).
cnf(t119,plain,
mult(rd(rd(X1,X1),rd(X1,X1)),X1) = X1,
inference(orient,[status(thm)],[t1774]) ).
cnf(t122,plain,
rd(mult(mult(rd(rd(X1,X1),rd(X1,X1)),X1),X2),X2) = rd(mult(X1,rd(X3,X2)),rd(X3,X2)),
inference(cp,[status(thm)],[t62,t119]) ).
cnf(t1777,plain,
rd(mult(X1,X2),X2) = rd(mult(X1,rd(X3,X2)),rd(X3,X2)),
inference(step,[status(thm)],[t122,t119]) ).
cnf(t132,plain,
rd(mult(X1,rd(X2,X3)),rd(X2,X3)) = rd(mult(X1,X3),X3),
inference(orient,[status(thm)],[t1777]) ).
cnf(t43,plain,
mult(mult(X1,ld(X1,X2)),X3) = mult(rd(X1,X1),ld(ld(X1,X1),mult(X2,X3))),
inference(cp,[status(thm)],[t19,t42]) ).
cnf(t1785,plain,
mult(mult(X1,ld(X1,X2)),X3) = mult(rd(X1,X1),ld(rd(X1,X1),mult(X2,X3))),
inference(step,[status(thm)],[t43,t42]) ).
cnf(t343,plain,
mult(rd(X1,X1),ld(rd(X1,X1),mult(X2,X3))) = mult(mult(X1,ld(X1,X2)),X3),
inference(orient,[status(thm)],[t1785]) ).
cnf(t136,plain,
rd(mult(rd(X1,rd(X2,X3)),X3),X3) = rd(rd(mult(X1,rd(X2,X3)),rd(X2,X3)),rd(X2,X3)),
inference(cp,[status(thm)],[t132,t26]) ).
cnf(t80,plain,
mult(X1,rd(X2,X3)) = rd(mult(mult(X1,rd(X2,X3)),X3),X3),
inference(cp,[status(thm)],[t79,t62]) ).
cnf(t97,plain,
rd(mult(mult(X1,rd(X2,X3)),X3),X3) = mult(X1,rd(X2,X3)),
inference(orient,[status(thm)],[t80]) ).
cnf(t125,plain,
mult(rd(rd(rd(X1,X2),rd(X1,X2)),rd(rd(X1,X2),rd(X1,X2))),rd(X1,X2)) = rd(mult(rd(X1,X2),X2),X2),
inference(cp,[status(thm)],[t97,t119]) ).
cnf(t1775,plain,
rd(X1,X2) = rd(mult(rd(X1,X2),X2),X2),
inference(step,[status(thm)],[t125,t119]) ).
cnf(t1776,plain,
rd(X1,X2) = rd(rd(mult(X1,X2),X2),X2),
inference(step,[status(thm)],[t1775,t26]) ).
cnf(t126,plain,
rd(rd(mult(X1,X2),X2),X2) = rd(X1,X2),
inference(orient,[status(thm)],[t1776]) ).
cnf(t1778,plain,
rd(mult(rd(X1,rd(X2,X3)),X3),X3) = rd(X1,rd(X2,X3)),
inference(step,[status(thm)],[t136,t126]) ).
cnf(t149,plain,
rd(mult(rd(X1,rd(X2,X3)),X3),X3) = rd(X1,rd(X2,X3)),
inference(orient,[status(thm)],[t1778]) ).
cnf(t151,plain,
rd(rd(X1,X1),rd(X1,X1)) = rd(X1,X1),
inference(cp,[status(thm)],[t149,t119]) ).
cnf(t162,plain,
rd(rd(X1,X1),rd(X1,X1)) = rd(X1,X1),
inference(orient,[status(thm)],[t151]) ).
cnf(t163,plain,
rd(X1,X1) = mult(rd(X1,X1),rd(X1,X1)),
inference(cp,[status(thm)],[t47,t162]) ).
cnf(t165,plain,
mult(rd(X1,X1),rd(X1,X1)) = rd(X1,X1),
inference(orient,[status(thm)],[t163]) ).
cnf(t358,plain,
mult(mult(X1,ld(X1,rd(X2,X2))),rd(X2,X2)) = mult(rd(X1,X1),ld(rd(X1,X1),rd(X2,X2))),
inference(cp,[status(thm)],[t343,t165]) ).
cnf(t1786,plain,
mult(rd(mult(rd(X1,X1),X2),X2),rd(X2,X2)) = mult(rd(X1,X1),ld(rd(X1,X1),rd(X2,X2))),
inference(step,[status(thm)],[t358,t90]) ).
cnf(t144,plain,
rd(mult(mult(X1,rd(X2,X3)),rd(X2,X3)),rd(X2,X3)) = mult(rd(mult(X1,X3),X3),rd(X2,X3)),
inference(cp,[status(thm)],[t26,t132]) ).
cnf(t1780,plain,
rd(mult(mult(X1,rd(X2,X3)),X3),X3) = mult(rd(mult(X1,X3),X3),rd(X2,X3)),
inference(step,[status(thm)],[t144,t62]) ).
cnf(t1781,plain,
mult(X1,rd(X2,X3)) = mult(rd(mult(X1,X3),X3),rd(X2,X3)),
inference(step,[status(thm)],[t1780,t97]) ).
cnf(t184,plain,
mult(rd(mult(X1,X2),X2),rd(X3,X2)) = mult(X1,rd(X3,X2)),
inference(orient,[status(thm)],[t1781]) ).
cnf(t1787,plain,
mult(rd(X1,X1),rd(X2,X2)) = mult(rd(X1,X1),ld(rd(X1,X1),rd(X2,X2))),
inference(step,[status(thm)],[t1786,t184]) ).
cnf(t1788,plain,
mult(rd(X1,X1),rd(X2,X2)) = rd(mult(rd(rd(X1,X1),rd(X1,X1)),X2),X2),
inference(step,[status(thm)],[t1787,t90]) ).
cnf(t1789,plain,
mult(rd(X1,X1),rd(X2,X2)) = rd(mult(rd(X1,X1),X2),X2),
inference(step,[status(thm)],[t1788,t162]) ).
cnf(t379,plain,
mult(rd(X1,X1),rd(X2,X2)) = rd(mult(rd(X1,X1),X2),X2),
inference(orient,[status(thm)],[t1789]) ).
cnf(t393,plain,
rd(mult(rd(X1,X1),X2),X2) = rd(rd(mult(rd(X1,X1),X2),X2),rd(X2,X2)),
inference(cp,[status(thm)],[t132,t379]) ).
cnf(t145,plain,
rd(X1,rd(X2,X3)) = rd(rd(mult(X1,X3),X3),rd(X2,X3)),
inference(cp,[status(thm)],[t126,t132]) ).
cnf(t201,plain,
rd(rd(mult(X1,X2),X2),rd(X3,X2)) = rd(X1,rd(X3,X2)),
inference(orient,[status(thm)],[t145]) ).
cnf(t1790,plain,
rd(mult(rd(X1,X1),X2),X2) = rd(rd(X1,X1),rd(X2,X2)),
inference(step,[status(thm)],[t393,t201]) ).
cnf(t400,plain,
rd(mult(rd(X1,X1),X2),X2) = rd(rd(X1,X1),rd(X2,X2)),
inference(orient,[status(thm)],[t1790]) ).
cnf(t1791,plain,
mult(X1,ld(X1,rd(X2,X2))) = rd(rd(X1,X1),rd(X2,X2)),
inference(step,[status(thm)],[t90,t400]) ).
cnf(t401,plain,
mult(X1,ld(X1,rd(X2,X2))) = rd(rd(X1,X1),rd(X2,X2)),
inference(orient,[status(thm)],[t1791]) ).
cnf(t733,plain,
mult(X1,rd(X2,X2)) = mult(X1,rd(rd(X1,X1),rd(X2,X2))),
inference(cp,[status(thm)],[t731,t401]) ).
cnf(t394,plain,
rd(mult(mult(X1,rd(X2,X2)),rd(X3,X3)),rd(X3,X3)) = mult(X1,rd(rd(mult(rd(X2,X2),X3),X3),rd(X3,X3))),
inference(cp,[status(thm)],[t61,t379]) ).
cnf(t1797,plain,
rd(mult(mult(X1,rd(X2,X2)),X3),X3) = mult(X1,rd(rd(mult(rd(X2,X2),X3),X3),rd(X3,X3))),
inference(step,[status(thm)],[t394,t62]) ).
cnf(t1798,plain,
rd(mult(mult(X1,rd(X2,X2)),X3),X3) = mult(X1,rd(rd(X2,X2),rd(X3,X3))),
inference(step,[status(thm)],[t1797,t201]) ).
cnf(t455,plain,
mult(X1,rd(rd(X2,X2),rd(X3,X3))) = rd(mult(mult(X1,rd(X2,X2)),X3),X3),
inference(orient,[status(thm)],[t1798]) ).
cnf(t1815,plain,
mult(X1,rd(X2,X2)) = rd(mult(mult(X1,rd(X1,X1)),X2),X2),
inference(step,[status(thm)],[t733,t455]) ).
cnf(t1816,plain,
mult(X1,rd(X2,X2)) = rd(mult(X1,X2),X2),
inference(step,[status(thm)],[t1815,t47]) ).
cnf(t763,plain,
mult(X1,rd(X2,X2)) = rd(mult(X1,X2),X2),
inference(orient,[status(thm)],[t1816]) ).
cnf(t767,plain,
rd(mult(rd(X1,rd(X2,X2)),X2),X2) = rd(mult(X1,rd(X2,X2)),rd(X2,X2)),
inference(cp,[status(thm)],[t763,t26]) ).
cnf(t1819,plain,
rd(X1,rd(X2,X2)) = rd(mult(X1,rd(X2,X2)),rd(X2,X2)),
inference(step,[status(thm)],[t767,t149]) ).
cnf(t1820,plain,
rd(X1,rd(X2,X2)) = rd(mult(X1,X2),X2),
inference(step,[status(thm)],[t1819,t132]) ).
cnf(t794,plain,
rd(mult(X1,X2),X2) = rd(X1,rd(X2,X2)),
inference(orient,[status(thm)],[t1820]) ).
cnf(t1821,plain,
mult(rd(X1,X2),X2) = rd(X1,rd(X2,X2)),
inference(step,[status(thm)],[t26,t794]) ).
cnf(t795,plain,
mult(rd(X1,X2),X2) = rd(X1,rd(X2,X2)),
inference(orient,[status(thm)],[t1821]) ).
cnf(t811,plain,
rd(mult(X1,X2),rd(X2,X2)) = mult(rd(X1,rd(X2,X2)),X2),
inference(cp,[status(thm)],[t795,t794]) ).
cnf(t1839,plain,
rd(mult(X1,X2),rd(X2,X2)) = mult(X1,X2),
inference(step,[status(thm)],[t79,t794]) ).
cnf(t820,plain,
rd(mult(X1,X2),rd(X2,X2)) = mult(X1,X2),
inference(rw,[status(thm)],[t1839]) ).
cnf(t837,plain,
rd(mult(X1,X2),rd(X2,X2)) = mult(X1,X2),
inference(orient,[status(thm)],[t820]) ).
cnf(t1857,plain,
mult(X1,X2) = mult(rd(X1,rd(X2,X2)),X2),
inference(step,[status(thm)],[t811,t837]) ).
cnf(t861,plain,
mult(rd(X1,rd(X2,X2)),X2) = mult(X1,X2),
inference(orient,[status(thm)],[t1857]) ).
cnf(t140,plain,
rd(mult(X1,X2),X2) = rd(mult(X1,mult(X3,X2)),rd(mult(mult(X3,X2),X2),X2)),
inference(cp,[status(thm)],[t132,t79]) ).
cnf(t1779,plain,
rd(mult(X1,X2),X2) = rd(mult(X1,mult(X3,X2)),mult(X3,X2)),
inference(step,[status(thm)],[t140,t79]) ).
cnf(t167,plain,
rd(mult(X1,mult(X2,X3)),mult(X2,X3)) = rd(mult(X1,X3),X3),
inference(orient,[status(thm)],[t1779]) ).
cnf(t1835,plain,
rd(X1,rd(mult(X2,X3),mult(X2,X3))) = rd(mult(X1,X3),X3),
inference(step,[status(thm)],[t167,t794]) ).
cnf(t1836,plain,
rd(X1,rd(mult(X2,X3),mult(X2,X3))) = rd(X1,rd(X3,X3)),
inference(step,[status(thm)],[t1835,t794]) ).
cnf(t818,plain,
rd(X1,rd(mult(X2,X3),mult(X2,X3))) = rd(X1,rd(X3,X3)),
inference(rw,[status(thm)],[t1836]) ).
cnf(t917,plain,
rd(X1,rd(mult(X2,X3),mult(X2,X3))) = rd(X1,rd(X3,X3)),
inference(orient,[status(thm)],[t818]) ).
cnf(t696,plain,
mult(X1,ld(X1,mult(mult(X1,X2),X3))) = mult(mult(X1,mult(X1,ld(X1,X2))),X3),
inference(cp,[status(thm)],[t680,t12]) ).
cnf(t1887,plain,
mult(X1,ld(X1,mult(mult(X1,X2),X3))) = mult(mult(X1,X2),X3),
inference(step,[status(thm)],[t696,t731]) ).
cnf(t1558,plain,
mult(X1,ld(X1,mult(mult(X1,X2),X3))) = mult(mult(X1,X2),X3),
inference(orient,[status(thm)],[t1887]) ).
cnf(t1582,plain,
rd(X1,rd(ld(X2,mult(mult(X2,X3),X4)),ld(X2,mult(mult(X2,X3),X4)))) = rd(X1,rd(mult(X2,ld(X2,mult(mult(X2,X3),X4))),mult(mult(X2,X3),X4))),
inference(cp,[status(thm)],[t917,t1558]) ).
cnf(t922,plain,
rd(X1,rd(mult(X2,ld(X2,X3)),mult(X2,ld(X2,X3)))) = rd(X1,rd(mult(X2,X3),mult(X2,mult(X2,ld(X2,X3))))),
inference(cp,[status(thm)],[t917,t731]) ).
cnf(t1859,plain,
rd(X1,rd(ld(X2,X3),ld(X2,X3))) = rd(X1,rd(mult(X2,X3),mult(X2,mult(X2,ld(X2,X3))))),
inference(step,[status(thm)],[t922,t917]) ).
cnf(t1860,plain,
rd(X1,rd(ld(X2,X3),ld(X2,X3))) = rd(X1,rd(mult(X2,X3),mult(X2,X3))),
inference(step,[status(thm)],[t1859,t731]) ).
cnf(t1861,plain,
rd(X1,rd(ld(X2,X3),ld(X2,X3))) = rd(X1,rd(X3,X3)),
inference(step,[status(thm)],[t1860,t917]) ).
cnf(t1057,plain,
rd(X1,rd(ld(X2,X3),ld(X2,X3))) = rd(X1,rd(X3,X3)),
inference(orient,[status(thm)],[t1861]) ).
cnf(t1888,plain,
rd(X1,rd(mult(mult(X2,X3),X4),mult(mult(X2,X3),X4))) = rd(X1,rd(mult(X2,ld(X2,mult(mult(X2,X3),X4))),mult(mult(X2,X3),X4))),
inference(step,[status(thm)],[t1582,t1057]) ).
cnf(t1889,plain,
rd(X1,rd(X4,X4)) = rd(X1,rd(mult(X2,ld(X2,mult(mult(X2,X3),X4))),mult(mult(X2,X3),X4))),
inference(step,[status(thm)],[t1888,t917]) ).
cnf(t690,plain,
mult(X1,ld(X1,mult(rd(X2,X2),X3))) = mult(rd(rd(X1,X1),rd(X2,X2)),X3),
inference(cp,[status(thm)],[t680,t401]) ).
cnf(t1272,plain,
mult(rd(rd(X1,X1),rd(X2,X2)),X3) = mult(X1,ld(X1,mult(rd(X2,X2),X3))),
inference(orient,[status(thm)],[t690]) ).
cnf(t1273,plain,
mult(X1,ld(X1,mult(rd(X2,X2),X2))) = mult(rd(X1,X1),X2),
inference(cp,[status(thm)],[t1272,t861]) ).
cnf(t1864,plain,
mult(X1,ld(X1,rd(X2,rd(X2,X2)))) = mult(rd(X1,X1),X2),
inference(step,[status(thm)],[t1273,t795]) ).
cnf(t82,plain,
mult(X1,rd(X1,X1)) = rd(mult(X1,rd(X1,X1)),rd(X1,X1)),
inference(cp,[status(thm)],[t79,t47]) ).
cnf(t1769,plain,
X1 = rd(mult(X1,rd(X1,X1)),rd(X1,X1)),
inference(step,[status(thm)],[t82,t47]) ).
cnf(t1770,plain,
X1 = rd(X1,rd(X1,X1)),
inference(step,[status(thm)],[t1769,t47]) ).
cnf(t89,plain,
rd(X1,rd(X1,X1)) = X1,
inference(orient,[status(thm)],[t1770]) ).
cnf(t1865,plain,
mult(X1,ld(X1,X2)) = mult(rd(X1,X1),X2),
inference(step,[status(thm)],[t1864,t89]) ).
cnf(t1309,plain,
mult(rd(X1,X1),X2) = mult(X1,ld(X1,X2)),
inference(orient,[status(thm)],[t1865]) ).
cnf(t1324,plain,
rd(rd(X1,X1),rd(X2,X2)) = rd(mult(X1,ld(X1,X2)),X2),
inference(cp,[status(thm)],[t794,t1309]) ).
cnf(t1337,plain,
rd(mult(X1,ld(X1,X2)),X2) = rd(rd(X1,X1),rd(X2,X2)),
inference(orient,[status(thm)],[t1324]) ).
cnf(t1890,plain,
rd(X1,rd(X4,X4)) = rd(X1,rd(rd(X2,X2),rd(mult(mult(X2,X3),X4),mult(mult(X2,X3),X4)))),
inference(step,[status(thm)],[t1889,t1337]) ).
cnf(t1891,plain,
rd(X1,rd(X4,X4)) = rd(X1,rd(rd(X2,X2),rd(X4,X4))),
inference(step,[status(thm)],[t1890,t917]) ).
cnf(t1585,plain,
rd(X1,rd(rd(X2,X2),rd(X3,X3))) = rd(X1,rd(X3,X3)),
inference(orient,[status(thm)],[t1891]) ).
cnf(t1594,plain,
rd(mult(X1,rd(rd(X2,X2),rd(X3,X3))),rd(X3,X3)) = rd(X1,rd(rd(rd(X2,X2),rd(X3,X3)),rd(rd(X2,X2),rd(X3,X3)))),
inference(cp,[status(thm)],[t1585,t794]) ).
cnf(t1817,plain,
mult(X1,rd(rd(X2,X2),rd(X3,X3))) = rd(mult(rd(mult(X1,X2),X2),X3),X3),
inference(step,[status(thm)],[t455,t763]) ).
cnf(t764,plain,
mult(X1,rd(rd(X2,X2),rd(X3,X3))) = rd(mult(rd(mult(X1,X2),X2),X3),X3),
inference(orient,[status(thm)],[t1817]) ).
cnf(t1823,plain,
mult(X1,rd(rd(X2,X2),rd(X3,X3))) = rd(rd(mult(X1,X2),X2),rd(X3,X3)),
inference(step,[status(thm)],[t764,t794]) ).
cnf(t1824,plain,
mult(X1,rd(rd(X2,X2),rd(X3,X3))) = rd(rd(X1,rd(X2,X2)),rd(X3,X3)),
inference(step,[status(thm)],[t1823,t794]) ).
cnf(t797,plain,
mult(X1,rd(rd(X2,X2),rd(X3,X3))) = rd(rd(X1,rd(X2,X2)),rd(X3,X3)),
inference(orient,[status(thm)],[t1824]) ).
cnf(t1892,plain,
rd(rd(rd(X1,rd(X2,X2)),rd(X3,X3)),rd(X3,X3)) = rd(X1,rd(rd(rd(X2,X2),rd(X3,X3)),rd(rd(X2,X2),rd(X3,X3)))),
inference(step,[status(thm)],[t1594,t797]) ).
cnf(t1846,plain,
rd(rd(X1,rd(X2,X3)),rd(X3,X3)) = rd(X1,rd(X2,X3)),
inference(step,[status(thm)],[t149,t794]) ).
cnf(t825,plain,
rd(rd(X1,rd(X2,X3)),rd(X3,X3)) = rd(X1,rd(X2,X3)),
inference(rw,[status(thm)],[t1846]) ).
cnf(t1024,plain,
rd(rd(X1,rd(X2,X3)),rd(X3,X3)) = rd(X1,rd(X2,X3)),
inference(orient,[status(thm)],[t825]) ).
cnf(t1893,plain,
rd(rd(X1,rd(X2,X2)),rd(X3,X3)) = rd(X1,rd(rd(rd(X2,X2),rd(X3,X3)),rd(rd(X2,X2),rd(X3,X3)))),
inference(step,[status(thm)],[t1892,t1024]) ).
cnf(t1837,plain,
rd(X1,rd(rd(X2,X3),rd(X2,X3))) = rd(mult(X1,X3),X3),
inference(step,[status(thm)],[t132,t794]) ).
cnf(t1838,plain,
rd(X1,rd(rd(X2,X3),rd(X2,X3))) = rd(X1,rd(X3,X3)),
inference(step,[status(thm)],[t1837,t794]) ).
cnf(t819,plain,
rd(X1,rd(rd(X2,X3),rd(X2,X3))) = rd(X1,rd(X3,X3)),
inference(rw,[status(thm)],[t1838]) ).
cnf(t963,plain,
rd(X1,rd(rd(X2,X3),rd(X2,X3))) = rd(X1,rd(X3,X3)),
inference(orient,[status(thm)],[t819]) ).
cnf(t1894,plain,
rd(rd(X1,rd(X2,X2)),rd(X3,X3)) = rd(X1,rd(rd(X3,X3),rd(X3,X3))),
inference(step,[status(thm)],[t1893,t963]) ).
cnf(t1895,plain,
rd(rd(X1,rd(X2,X2)),rd(X3,X3)) = rd(X1,rd(X3,X3)),
inference(step,[status(thm)],[t1894,t963]) ).
cnf(t1642,plain,
rd(rd(X1,rd(X2,X2)),rd(X3,X3)) = rd(X1,rd(X3,X3)),
inference(orient,[status(thm)],[t1895]) ).
cnf(t1670,plain,
mult(rd(X1,rd(X2,X2)),X3) = mult(rd(X1,rd(X3,X3)),X3),
inference(cp,[status(thm)],[t861,t1642]) ).
cnf(t1896,plain,
mult(rd(X1,rd(X2,X2)),X3) = mult(X1,X3),
inference(step,[status(thm)],[t1670,t861]) ).
cnf(t1678,plain,
mult(rd(X1,rd(X2,X2)),X3) = mult(X1,X3),
inference(orient,[status(thm)],[t1896]) ).
cnf(t0,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t11,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t0]) ).
cnf(t1685,plain,
mult(mult(X1,ld(X1,rd(X2,X2))),X3) = mult(rd(rd(X1,X1),rd(rd(X2,X2),rd(X2,X2))),X3),
inference(cp,[status(thm)],[t1678,t1337]) ).
cnf(t1900,plain,
mult(X1,ld(X1,mult(rd(X2,X2),X3))) = mult(rd(rd(X1,X1),rd(rd(X2,X2),rd(X2,X2))),X3),
inference(step,[status(thm)],[t1685,t680]) ).
cnf(t1901,plain,
mult(X1,ld(X1,mult(X2,ld(X2,X3)))) = mult(rd(rd(X1,X1),rd(rd(X2,X2),rd(X2,X2))),X3),
inference(step,[status(thm)],[t1900,t1309]) ).
cnf(t1902,plain,
mult(X1,ld(X1,mult(X2,ld(X2,X3)))) = mult(rd(X1,X1),X3),
inference(step,[status(thm)],[t1901,t1678]) ).
cnf(t1903,plain,
mult(X1,ld(X1,mult(X2,ld(X2,X3)))) = mult(X1,ld(X1,X3)),
inference(step,[status(thm)],[t1902,t1309]) ).
cnf(t1725,plain,
mult(X1,ld(X1,mult(X2,ld(X2,X3)))) = mult(X1,ld(X1,X3)),
inference(orient,[status(thm)],[t1903]) ).
cnf(t1739,plain,
mult(X1,mult(X2,ld(X2,X3))) = mult(X1,mult(X1,ld(X1,X3))),
inference(cp,[status(thm)],[t731,t1725]) ).
cnf(t1904,plain,
mult(X1,mult(X2,ld(X2,X3))) = mult(X1,X3),
inference(step,[status(thm)],[t1739,t731]) ).
cnf(t1747,plain,
mult(X1,mult(X2,ld(X2,X3))) = mult(X1,X3),
inference(orient,[status(thm)],[t1904]) ).
fof(f7,conjecture,
! [X3,X4,X5] :
( mult(rd(mult(X3,X4),X4),X5) = mult(X3,X5)
& mult(X3,ld(X4,mult(X4,X5))) = mult(X3,X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals) ).
fof(f7_neg,negated_conjecture,
~ ! [X3,X4,X5] :
( mult(rd(mult(X3,X4),X4),X5) = mult(X3,X5)
& mult(X3,ld(X4,mult(X4,X5))) = mult(X3,X5) ),
inference(negated_conjecture,[status(cth)],[f7]) ).
fof(f7_nnf,plain,
? [X3,X4,X5] :
( mult(rd(mult(X3,X4),X4),X5) != mult(X3,X5)
| mult(X3,ld(X4,mult(X4,X5))) != mult(X3,X5) ),
inference(nnf_transformation,[status(thm)],[f7_neg]) ).
fof(f7_sk,plain,
( mult(rd(mult(sk0,sk1),sk1),sk2) != mult(sk0,sk2)
| mult(sk0,ld(sk1,mult(sk1,sk2))) != mult(sk0,sk2) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0,sk1,sk2])],[f7_nnf]) ).
cnf(c7,plain,
( mult(rd(mult(sk0,sk1),sk1),sk2) != mult(sk0,sk2)
| mult(sk0,ld(sk1,mult(sk1,sk2))) != mult(sk0,sk2) ),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c7]) ).
cnf(g0_0,plain,
true != ifeq(mult(sk0,mult(sk1,ld(sk1,sk2))),mult(sk0,sk2),ifeq(mult(rd(mult(sk0,sk1),sk1),sk2),mult(sk0,sk2),false,true),true),
inference(rw,[status(thm)],[goal_0]) ).
cnf(g0_1,plain,
true != ifeq(mult(sk0,mult(sk1,ld(sk1,sk2))),mult(sk0,sk2),ifeq(mult(rd(sk0,rd(sk1,sk1)),sk2),mult(sk0,sk2),false,true),true),
inference(rw,[status(thm)],[g0_0,t794]) ).
cnf(g0_2,plain,
true != ifeq(mult(sk0,mult(sk1,ld(sk1,sk2))),mult(sk0,sk2),ifeq(mult(sk0,sk2),mult(sk0,sk2),false,true),true),
inference(rw,[status(thm)],[g0_1,t1678]) ).
cnf(g0_3,plain,
true != ifeq(mult(sk0,mult(sk1,ld(sk1,sk2))),mult(sk0,sk2),false,true),
inference(rw,[status(thm)],[g0_2,t11]) ).
cnf(g0_4,plain,
true != ifeq(mult(sk0,sk2),mult(sk0,sk2),false,true),
inference(rw,[status(thm)],[g0_3,t1747]) ).
cnf(g0_5,plain,
true != false,
inference(rw,[status(thm)],[g0_4,t11]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_5]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP683+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/5.37 % Computer : n003.cluster.edu
% 0.09/5.37 % Model : x86_64 x86_64
% 0.09/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.37 % Memory : 8046.5625MB
% 0.09/5.37 % OS : Linux 6.8.0-71-generic
% 0.09/5.37 % CPULimit : 300
% 0.09/5.37 % WCLimit : 300
% 0.09/5.37 % DateTime : Wed Sep 23 15:43:24 UTC 2026
% 0.09/5.37 % CPUTime :
% 0.09/5.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 5.67/6.30 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.67/6.30 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------