%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP654+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 : 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:27:51 PM UTC 2026
% Result : Theorem 35.96s 5.00s
% Output : Proof 35.96s
% Verified :
% SZS Type : Refutation
% Derivation depth : 141
% Number of leaves : 7
% Syntax : Number of formulae : 336 ( 331 unt; 0 def)
% Number of atoms : 341 ( 340 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 14 ( 9 ~; 3 |; 2 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 1 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 2 con; 0-4 aty)
% Number of variables : 784 ( 2 sgn 37 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f5,conjecture,
? [X0] :
! [X1] :
( mult(X0,X1) = X1
& mult(X1,X0) = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals) ).
fof(f5_neg,negated_conjecture,
~ ? [X0] :
! [X1] :
( mult(X0,X1) = X1
& mult(X1,X0) = X1 ),
inference(negated_conjecture,[status(cth)],[f5]) ).
fof(f5_nnf,plain,
! [X0] :
? [X1] :
( mult(X0,X1) != X1
| mult(X1,X0) != X1 ),
inference(nnf_transformation,[status(thm)],[f5_neg]) ).
fof(f5_sk,plain,
! [X0] :
( mult(X0,sk0(X0)) != sk0(X0)
| mult(sk0(X0),X0) != sk0(X0) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0])],[f5_nnf]) ).
cnf(c5,plain,
( mult(X0,sk0(X0)) != sk0(X0)
| mult(sk0(X0),X0) != sk0(X0) ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(t6,plain,
ifeq(mult(sk0(X1),X1),sk0(X1),ifeq(mult(X1,sk0(X1)),sk0(X1),false,true),true) = true,
inference(equality_encoding,[status(esa)],[c5]) ).
cnf(t22,plain,
ifeq(mult(sk0(X1),X1),sk0(X1),ifeq(mult(X1,sk0(X1)),sk0(X1),false,true),true) = true,
inference(orient,[status(thm)],[t6]) ).
fof(f3,axiom,
! [B,A] : rd(mult(A,B),B) = A,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',f04) ).
fof(f3_nnf,plain,
! [B,A] : rd(mult(A,B),B) = A,
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [A,B] : rd(mult(A,B),B) = A,
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
rd(mult(X1,X0),X0) = X1,
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(t4,plain,
rd(mult(X1,X2),X2) = X1,
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(t10,plain,
rd(mult(X1,X2),X2) = X1,
inference(orient,[status(thm)],[t4]) ).
fof(f4,axiom,
! [C,B,A] : mult(A,mult(B,mult(A,C))) = mult(mult(mult(A,B),A),C),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',f05) ).
fof(f4_nnf,plain,
! [C,B,A] : mult(A,mult(B,mult(A,C))) = mult(mult(mult(A,B),A),C),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [A,B,C] : mult(A,mult(B,mult(A,C))) = mult(mult(mult(A,B),A),C),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c4,plain,
mult(X2,mult(X1,mult(X2,X0))) = mult(mult(mult(X2,X1),X2),X0),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(t5,plain,
mult(mult(mult(X1,X2),X1),X3) = mult(X1,mult(X2,mult(X1,X3))),
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(t14,plain,
mult(mult(mult(X1,X2),X1),X3) = mult(X1,mult(X2,mult(X1,X3))),
inference(orient,[status(thm)],[t5]) ).
cnf(t19,plain,
mult(mult(X1,X2),X1) = rd(mult(X1,mult(X2,mult(X1,X3))),X3),
inference(cp,[status(thm)],[t10,t14]) ).
cnf(t59,plain,
rd(mult(X1,mult(X2,mult(X1,X3))),X3) = mult(mult(X1,X2),X1),
inference(orient,[status(thm)],[t19]) ).
fof(f2,axiom,
! [B,A] : mult(rd(A,B),B) = A,
file('/export/starexec/sandbox/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(t3,plain,
mult(rd(X1,X2),X2) = X1,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t8,plain,
mult(rd(X1,X2),X2) = X1,
inference(orient,[status(thm)],[t3]) ).
cnf(t63,plain,
mult(mult(X1,rd(X2,mult(X1,X3))),X1) = rd(mult(X1,X2),X3),
inference(cp,[status(thm)],[t59,t8]) ).
cnf(t599,plain,
mult(mult(X1,rd(X2,mult(X1,X3))),X1) = rd(mult(X1,X2),X3),
inference(orient,[status(thm)],[t63]) ).
fof(f0,axiom,
! [B,A] : mult(A,ld(A,B)) = B,
file('/export/starexec/sandbox/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(t2,plain,
mult(X1,ld(X1,X2)) = X2,
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t7,plain,
mult(X1,ld(X1,X2)) = X2,
inference(orient,[status(thm)],[t2]) ).
cnf(t607,plain,
rd(mult(X1,X2),ld(X1,X3)) = mult(mult(X1,rd(X2,X3)),X1),
inference(cp,[status(thm)],[t599,t7]) ).
cnf(t734,plain,
mult(mult(X1,rd(X2,X3)),X1) = rd(mult(X1,X2),ld(X1,X3)),
inference(orient,[status(thm)],[t607]) ).
cnf(t757,plain,
mult(X1,rd(X2,X3)) = rd(rd(mult(X1,X2),ld(X1,X3)),X1),
inference(cp,[status(thm)],[t10,t734]) ).
cnf(t1679,plain,
rd(rd(mult(X1,X2),ld(X1,X3)),X1) = mult(X1,rd(X2,X3)),
inference(orient,[status(thm)],[t757]) ).
fof(f1,axiom,
! [B,A] : ld(A,mult(A,B)) = B,
file('/export/starexec/sandbox/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(t1,plain,
ld(X1,mult(X1,X2)) = X2,
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(t12,plain,
ld(X1,mult(X1,X2)) = X2,
inference(orient,[status(thm)],[t1]) ).
cnf(t1711,plain,
mult(X1,rd(X2,mult(X1,X3))) = rd(rd(mult(X1,X2),X3),X1),
inference(cp,[status(thm)],[t1679,t12]) ).
cnf(t1833,plain,
mult(X1,rd(X2,mult(X1,X3))) = rd(rd(mult(X1,X2),X3),X1),
inference(orient,[status(thm)],[t1711]) ).
cnf(t11,plain,
X1 = rd(X2,ld(X1,X2)),
inference(cp,[status(thm)],[t10,t7]) ).
cnf(t24,plain,
rd(X1,ld(X2,X1)) = X2,
inference(orient,[status(thm)],[t11]) ).
cnf(t16,plain,
mult(X1,mult(ld(X1,X2),mult(X1,X3))) = mult(mult(X2,X1),X3),
inference(cp,[status(thm)],[t14,t7]) ).
cnf(t26,plain,
mult(X1,mult(ld(X1,X2),mult(X1,X3))) = mult(mult(X2,X1),X3),
inference(orient,[status(thm)],[t16]) ).
cnf(t29,plain,
mult(mult(X1,X2),ld(X2,X3)) = mult(X2,mult(ld(X2,X1),X3)),
inference(cp,[status(thm)],[t26,t7]) ).
cnf(t36,plain,
mult(mult(X1,X2),ld(X2,X3)) = mult(X2,mult(ld(X2,X1),X3)),
inference(orient,[status(thm)],[t29]) ).
cnf(t40,plain,
mult(X1,mult(ld(X1,rd(X2,X1)),X3)) = mult(X2,ld(X1,X3)),
inference(cp,[status(thm)],[t36,t8]) ).
cnf(t70,plain,
mult(X1,mult(ld(X1,rd(X2,X1)),X3)) = mult(X2,ld(X1,X3)),
inference(orient,[status(thm)],[t40]) ).
cnf(t77,plain,
mult(ld(X1,rd(X2,X1)),X3) = ld(X1,mult(X2,ld(X1,X3))),
inference(cp,[status(thm)],[t12,t70]) ).
cnf(t86,plain,
ld(X1,mult(X2,ld(X1,X3))) = mult(ld(X1,rd(X2,X1)),X3),
inference(orient,[status(thm)],[t77]) ).
cnf(t87,plain,
mult(ld(X1,rd(X1,X1)),X2) = ld(X1,X2),
inference(cp,[status(thm)],[t86,t12]) ).
cnf(t98,plain,
mult(ld(X1,rd(X1,X1)),X2) = ld(X1,X2),
inference(orient,[status(thm)],[t87]) ).
cnf(t104,plain,
ld(X1,rd(X1,X1)) = rd(ld(X1,X2),X2),
inference(cp,[status(thm)],[t10,t98]) ).
cnf(t132,plain,
ld(X1,rd(X1,X1)) = rd(ld(X1,X2),X2),
inference(orient,[status(thm)],[t104]) ).
cnf(t133,plain,
rd(X1,X1) = mult(X1,rd(ld(X1,X2),X2)),
inference(cp,[status(thm)],[t7,t132]) ).
cnf(t149,plain,
mult(X1,rd(ld(X1,X2),X2)) = rd(X1,X1),
inference(orient,[status(thm)],[t133]) ).
cnf(t152,plain,
rd(X1,X1) = mult(X1,rd(X2,mult(X1,X2))),
inference(cp,[status(thm)],[t149,t12]) ).
cnf(t223,plain,
mult(X1,rd(X2,mult(X1,X2))) = rd(X1,X1),
inference(orient,[status(thm)],[t152]) ).
cnf(t235,plain,
X1 = rd(rd(X1,X1),rd(X2,mult(X1,X2))),
inference(cp,[status(thm)],[t10,t223]) ).
cnf(t346,plain,
rd(rd(X1,X1),rd(X2,mult(X1,X2))) = X1,
inference(orient,[status(thm)],[t235]) ).
cnf(t357,plain,
mult(rd(X1,X1),ld(rd(X2,mult(X1,X2)),X3)) = mult(rd(X2,mult(X1,X2)),mult(ld(rd(X2,mult(X1,X2)),X1),X3)),
inference(cp,[status(thm)],[t70,t346]) ).
cnf(t145,plain,
ld(X1,X2) = mult(ld(X1,rd(X1,X1)),X2),
inference(cp,[status(thm)],[t8,t132]) ).
cnf(t70886,plain,
ld(X1,X2) = mult(rd(ld(X1,true),true),X2),
inference(step,[status(thm)],[t145,t132]) ).
cnf(t165,plain,
mult(rd(ld(X1,true),true),X2) = ld(X1,X2),
inference(orient,[status(thm)],[t70886]) ).
cnf(t13,plain,
X1 = ld(rd(X2,X1),X2),
inference(cp,[status(thm)],[t12,t8]) ).
cnf(t25,plain,
ld(rd(X1,X2),X1) = X2,
inference(orient,[status(thm)],[t13]) ).
cnf(t170,plain,
ld(rd(true,X1),X2) = mult(rd(X1,true),X2),
inference(cp,[status(thm)],[t165,t25]) ).
cnf(t182,plain,
ld(rd(true,X1),X2) = mult(rd(X1,true),X2),
inference(orient,[status(thm)],[t170]) ).
cnf(t99,plain,
ld(X1,ld(ld(X1,rd(X1,X1)),X2)) = X2,
inference(cp,[status(thm)],[t98,t7]) ).
cnf(t113,plain,
ld(X1,ld(ld(X1,rd(X1,X1)),X2)) = X2,
inference(orient,[status(thm)],[t99]) ).
cnf(t116,plain,
ld(ld(X1,rd(X1,X1)),X2) = mult(X1,X2),
inference(cp,[status(thm)],[t7,t113]) ).
cnf(t122,plain,
ld(ld(X1,rd(X1,X1)),X2) = mult(X1,X2),
inference(orient,[status(thm)],[t116]) ).
cnf(t147,plain,
ld(ld(X1,rd(X1,X1)),X2) = mult(X1,X2),
inference(rw,[status(thm)],[t122]) ).
cnf(t70887,plain,
ld(rd(ld(X1,true),true),X2) = mult(X1,X2),
inference(step,[status(thm)],[t147,t132]) ).
cnf(t195,plain,
ld(rd(ld(X1,true),true),X2) = mult(X1,X2),
inference(orient,[status(thm)],[t70887]) ).
cnf(t199,plain,
mult(rd(true,X1),X2) = ld(rd(X1,true),X2),
inference(cp,[status(thm)],[t195,t25]) ).
cnf(t208,plain,
ld(rd(X1,true),X2) = mult(rd(true,X1),X2),
inference(orient,[status(thm)],[t199]) ).
cnf(t213,plain,
mult(rd(true,mult(X1,true)),X2) = ld(X1,X2),
inference(cp,[status(thm)],[t208,t10]) ).
cnf(t253,plain,
mult(rd(true,mult(X1,true)),X2) = ld(X1,X2),
inference(orient,[status(thm)],[t213]) ).
cnf(t260,plain,
rd(true,mult(X1,true)) = rd(ld(X1,X2),X2),
inference(cp,[status(thm)],[t10,t253]) ).
cnf(t270,plain,
rd(ld(X1,X2),X2) = rd(true,mult(X1,true)),
inference(orient,[status(thm)],[t260]) ).
cnf(t274,plain,
rd(true,mult(rd(X1,X2),true)) = rd(X2,X1),
inference(cp,[status(thm)],[t270,t25]) ).
cnf(t293,plain,
rd(true,mult(rd(X1,X2),true)) = rd(X2,X1),
inference(orient,[status(thm)],[t274]) ).
cnf(t296,plain,
mult(rd(mult(rd(X1,X2),true),true),X3) = ld(rd(X2,X1),X3),
inference(cp,[status(thm)],[t182,t293]) ).
cnf(t70889,plain,
mult(rd(X1,X2),X3) = ld(rd(X2,X1),X3),
inference(step,[status(thm)],[t296,t10]) ).
cnf(t303,plain,
ld(rd(X1,X2),X3) = mult(rd(X2,X1),X3),
inference(orient,[status(thm)],[t70889]) ).
cnf(t70891,plain,
mult(rd(X1,X1),mult(rd(mult(X1,X2),X2),X3)) = mult(rd(X2,mult(X1,X2)),mult(ld(rd(X2,mult(X1,X2)),X1),X3)),
inference(step,[status(thm)],[t357,t303]) ).
cnf(t70892,plain,
mult(rd(X1,X1),mult(X1,X3)) = mult(rd(X2,mult(X1,X2)),mult(ld(rd(X2,mult(X1,X2)),X1),X3)),
inference(step,[status(thm)],[t70891,t10]) ).
cnf(t308,plain,
mult(rd(X1,mult(X2,X1)),X3) = ld(X2,X3),
inference(cp,[status(thm)],[t303,t10]) ).
cnf(t326,plain,
mult(rd(X1,mult(X2,X1)),X3) = ld(X2,X3),
inference(orient,[status(thm)],[t308]) ).
cnf(t70893,plain,
mult(rd(X1,X1),mult(X1,X3)) = ld(X1,mult(ld(rd(X2,mult(X1,X2)),X1),X3)),
inference(step,[status(thm)],[t70892,t326]) ).
cnf(t70894,plain,
mult(rd(X1,X1),mult(X1,X3)) = ld(X1,mult(mult(rd(mult(X1,X2),X2),X1),X3)),
inference(step,[status(thm)],[t70893,t303]) ).
cnf(t32,plain,
mult(ld(X1,X2),mult(X1,X3)) = ld(X1,mult(mult(X2,X1),X3)),
inference(cp,[status(thm)],[t12,t26]) ).
cnf(t48,plain,
ld(X1,mult(mult(X2,X1),X3)) = mult(ld(X1,X2),mult(X1,X3)),
inference(orient,[status(thm)],[t32]) ).
cnf(t70895,plain,
mult(rd(X1,X1),mult(X1,X3)) = mult(ld(X1,rd(mult(X1,X2),X2)),mult(X1,X3)),
inference(step,[status(thm)],[t70894,t48]) ).
cnf(t70896,plain,
mult(rd(X1,X1),mult(X1,X3)) = mult(ld(X1,X1),mult(X1,X3)),
inference(step,[status(thm)],[t70895,t10]) ).
cnf(t395,plain,
mult(ld(X1,X1),mult(X1,X2)) = mult(rd(X1,X1),mult(X1,X2)),
inference(orient,[status(thm)],[t70896]) ).
cnf(t410,plain,
ld(X1,X1) = rd(mult(rd(X1,X1),mult(X1,X2)),mult(X1,X2)),
inference(cp,[status(thm)],[t10,t395]) ).
cnf(t70897,plain,
ld(X1,X1) = rd(X1,X1),
inference(step,[status(thm)],[t410,t10]) ).
cnf(t421,plain,
ld(X1,X1) = rd(X1,X1),
inference(orient,[status(thm)],[t70897]) ).
cnf(t426,plain,
X1 = rd(X1,rd(X1,X1)),
inference(cp,[status(thm)],[t24,t421]) ).
cnf(t445,plain,
rd(X1,rd(X1,X1)) = X1,
inference(orient,[status(thm)],[t426]) ).
cnf(t742,plain,
rd(mult(X1,X2),ld(X1,rd(X2,X2))) = mult(mult(X1,X2),X1),
inference(cp,[status(thm)],[t734,t445]) ).
cnf(t1586,plain,
rd(mult(X1,X2),ld(X1,rd(X2,X2))) = mult(mult(X1,X2),X1),
inference(orient,[status(thm)],[t742]) ).
cnf(t1605,plain,
mult(mult(rd(X1,X2),X2),rd(X1,X2)) = rd(X1,ld(rd(X1,X2),rd(X2,X2))),
inference(cp,[status(thm)],[t1586,t8]) ).
cnf(t70952,plain,
mult(X1,rd(X1,X2)) = rd(X1,ld(rd(X1,X2),rd(X2,X2))),
inference(step,[status(thm)],[t1605,t8]) ).
cnf(t70953,plain,
mult(X1,rd(X1,X2)) = rd(X1,mult(rd(X2,X1),rd(X2,X2))),
inference(step,[status(thm)],[t70952,t303]) ).
cnf(t2899,plain,
rd(X1,mult(rd(X2,X1),rd(X2,X2))) = mult(X1,rd(X1,X2)),
inference(orient,[status(thm)],[t70953]) ).
cnf(t2930,plain,
rd(rd(mult(rd(X1,X2),X2),rd(X1,X1)),rd(X1,X2)) = mult(rd(X1,X2),mult(X2,rd(X2,X1))),
inference(cp,[status(thm)],[t1833,t2899]) ).
cnf(t70958,plain,
rd(rd(X1,rd(X1,X1)),rd(X1,X2)) = mult(rd(X1,X2),mult(X2,rd(X2,X1))),
inference(step,[status(thm)],[t2930,t8]) ).
cnf(t70959,plain,
rd(X1,rd(X1,X2)) = mult(rd(X1,X2),mult(X2,rd(X2,X1))),
inference(step,[status(thm)],[t70958,t445]) ).
cnf(t3687,plain,
mult(rd(X1,X2),mult(X2,rd(X2,X1))) = rd(X1,rd(X1,X2)),
inference(orient,[status(thm)],[t70959]) ).
cnf(t343,plain,
mult(mult(rd(X1,mult(X2,X1)),X3),rd(X1,mult(X2,X1))) = rd(ld(X2,mult(X3,mult(rd(X1,mult(X2,X1)),Y3))),Y3),
inference(cp,[status(thm)],[t59,t326]) ).
cnf(t70907,plain,
mult(ld(X2,X3),rd(X1,mult(X2,X1))) = rd(ld(X2,mult(X3,mult(rd(X1,mult(X2,X1)),Y3))),Y3),
inference(step,[status(thm)],[t343,t326]) ).
cnf(t70908,plain,
mult(ld(X2,X3),rd(X1,mult(X2,X1))) = rd(ld(X2,mult(X3,ld(X2,Y3))),Y3),
inference(step,[status(thm)],[t70907,t326]) ).
cnf(t70909,plain,
mult(ld(X2,X3),rd(X1,mult(X2,X1))) = rd(mult(ld(X2,rd(X3,X2)),Y3),Y3),
inference(step,[status(thm)],[t70908,t86]) ).
cnf(t70910,plain,
mult(ld(X2,X3),rd(X1,mult(X2,X1))) = ld(X2,rd(X3,X2)),
inference(step,[status(thm)],[t70909,t10]) ).
cnf(t822,plain,
mult(ld(X1,X2),rd(X3,mult(X1,X3))) = ld(X1,rd(X2,X1)),
inference(orient,[status(thm)],[t70910]) ).
cnf(t858,plain,
mult(X1,ld(X2,rd(X3,mult(X2,X3)))) = mult(X2,ld(X2,rd(rd(X1,X2),X2))),
inference(cp,[status(thm)],[t70,t822]) ).
cnf(t427,plain,
mult(ld(X1,rd(X2,X1)),X1) = ld(X1,mult(X2,rd(X1,X1))),
inference(cp,[status(thm)],[t86,t421]) ).
cnf(t499,plain,
ld(X1,mult(X2,rd(X1,X1))) = mult(ld(X1,rd(X2,X1)),X1),
inference(orient,[status(thm)],[t427]) ).
cnf(t231,plain,
rd(rd(X1,X2),rd(X1,X2)) = mult(rd(X1,X2),rd(X2,X1)),
inference(cp,[status(thm)],[t223,t8]) ).
cnf(t375,plain,
mult(rd(X1,X2),rd(X2,X1)) = rd(rd(X1,X2),rd(X1,X2)),
inference(orient,[status(thm)],[t231]) ).
cnf(t502,plain,
mult(ld(X1,rd(rd(X1,X1),X1)),X1) = ld(X1,rd(rd(X1,X1),rd(X1,X1))),
inference(cp,[status(thm)],[t499,t375]) ).
cnf(t424,plain,
rd(true,mult(X1,true)) = rd(rd(X1,X1),X1),
inference(cp,[status(thm)],[t270,t421]) ).
cnf(t453,plain,
rd(rd(X1,X1),X1) = rd(true,mult(X1,true)),
inference(orient,[status(thm)],[t424]) ).
cnf(t70913,plain,
mult(ld(X1,rd(true,mult(X1,true))),X1) = ld(X1,rd(rd(X1,X1),rd(X1,X1))),
inference(step,[status(thm)],[t502,t453]) ).
cnf(t425,plain,
mult(X1,mult(ld(X1,X2),X1)) = mult(mult(X2,X1),rd(X1,X1)),
inference(cp,[status(thm)],[t36,t421]) ).
cnf(t456,plain,
mult(mult(X1,X2),rd(X2,X2)) = mult(X2,mult(ld(X2,X1),X2)),
inference(orient,[status(thm)],[t425]) ).
cnf(t423,plain,
X1 = mult(X1,rd(X1,X1)),
inference(cp,[status(thm)],[t7,t421]) ).
cnf(t429,plain,
mult(X1,rd(X1,X1)) = X1,
inference(orient,[status(thm)],[t423]) ).
cnf(t458,plain,
mult(rd(X1,X1),mult(ld(rd(X1,X1),X1),rd(X1,X1))) = mult(X1,rd(rd(X1,X1),rd(X1,X1))),
inference(cp,[status(thm)],[t456,t429]) ).
cnf(t70898,plain,
mult(rd(X1,X1),mult(mult(rd(X1,X1),X1),rd(X1,X1))) = mult(X1,rd(rd(X1,X1),rd(X1,X1))),
inference(step,[status(thm)],[t458,t303]) ).
cnf(t70899,plain,
mult(rd(X1,X1),mult(X1,rd(X1,X1))) = mult(X1,rd(rd(X1,X1),rd(X1,X1))),
inference(step,[status(thm)],[t70898,t8]) ).
cnf(t70900,plain,
mult(rd(X1,X1),X1) = mult(X1,rd(rd(X1,X1),rd(X1,X1))),
inference(step,[status(thm)],[t70899,t429]) ).
cnf(t70901,plain,
X1 = mult(X1,rd(rd(X1,X1),rd(X1,X1))),
inference(step,[status(thm)],[t70900,t8]) ).
cnf(t479,plain,
mult(X1,rd(rd(X1,X1),rd(X1,X1))) = X1,
inference(orient,[status(thm)],[t70901]) ).
cnf(t484,plain,
rd(rd(X1,X1),rd(X1,X1)) = ld(X1,X1),
inference(cp,[status(thm)],[t12,t479]) ).
cnf(t70902,plain,
rd(rd(X1,X1),rd(X1,X1)) = rd(X1,X1),
inference(step,[status(thm)],[t484,t421]) ).
cnf(t497,plain,
rd(rd(X1,X1),rd(X1,X1)) = rd(X1,X1),
inference(orient,[status(thm)],[t70902]) ).
cnf(t70914,plain,
mult(ld(X1,rd(true,mult(X1,true))),X1) = ld(X1,rd(X1,X1)),
inference(step,[status(thm)],[t70913,t497]) ).
cnf(t70888,plain,
ld(X1,rd(X1,X1)) = rd(true,mult(X1,true)),
inference(step,[status(thm)],[t132,t270]) ).
cnf(t277,plain,
ld(X1,rd(X1,X1)) = rd(true,mult(X1,true)),
inference(rw,[status(thm)],[t70888]) ).
cnf(t278,plain,
ld(X1,rd(X1,X1)) = rd(true,mult(X1,true)),
inference(orient,[status(thm)],[t277]) ).
cnf(t70915,plain,
mult(ld(X1,rd(true,mult(X1,true))),X1) = rd(true,mult(X1,true)),
inference(step,[status(thm)],[t70914,t278]) ).
cnf(t1092,plain,
mult(ld(X1,rd(true,mult(X1,true))),X1) = rd(true,mult(X1,true)),
inference(orient,[status(thm)],[t70915]) ).
cnf(t1101,plain,
rd(true,mult(rd(X1,mult(X2,X1)),true)) = mult(ld(rd(X1,mult(X2,X1)),rd(true,ld(X2,true))),rd(X1,mult(X2,X1))),
inference(cp,[status(thm)],[t1092,t326]) ).
cnf(t70916,plain,
rd(mult(X2,X1),X1) = mult(ld(rd(X1,mult(X2,X1)),rd(true,ld(X2,true))),rd(X1,mult(X2,X1))),
inference(step,[status(thm)],[t1101,t293]) ).
cnf(t70917,plain,
X2 = mult(ld(rd(X1,mult(X2,X1)),rd(true,ld(X2,true))),rd(X1,mult(X2,X1))),
inference(step,[status(thm)],[t70916,t10]) ).
cnf(t70918,plain,
X2 = mult(mult(rd(mult(X2,X1),X1),rd(true,ld(X2,true))),rd(X1,mult(X2,X1))),
inference(step,[status(thm)],[t70917,t303]) ).
cnf(t70919,plain,
X2 = mult(mult(X2,rd(true,ld(X2,true))),rd(X1,mult(X2,X1))),
inference(step,[status(thm)],[t70918,t10]) ).
cnf(t70920,plain,
X2 = mult(mult(X2,X2),rd(X1,mult(X2,X1))),
inference(step,[status(thm)],[t70919,t24]) ).
cnf(t1126,plain,
mult(mult(X1,X1),rd(X2,mult(X1,X2))) = X1,
inference(orient,[status(thm)],[t70920]) ).
cnf(t1156,plain,
mult(X1,X1) = rd(X1,rd(X2,mult(X1,X2))),
inference(cp,[status(thm)],[t10,t1126]) ).
cnf(t1172,plain,
rd(X1,rd(X2,mult(X1,X2))) = mult(X1,X1),
inference(orient,[status(thm)],[t1156]) ).
cnf(t1194,plain,
mult(rd(X1,mult(X2,X1)),rd(X1,mult(X2,X1))) = rd(rd(X1,mult(X2,X1)),rd(X3,ld(X2,X3))),
inference(cp,[status(thm)],[t1172,t326]) ).
cnf(t70921,plain,
ld(X2,rd(X1,mult(X2,X1))) = rd(rd(X1,mult(X2,X1)),rd(X3,ld(X2,X3))),
inference(step,[status(thm)],[t1194,t326]) ).
cnf(t70922,plain,
ld(X2,rd(X1,mult(X2,X1))) = rd(rd(X1,mult(X2,X1)),X2),
inference(step,[status(thm)],[t70921,t24]) ).
cnf(t1269,plain,
ld(X1,rd(X2,mult(X1,X2))) = rd(rd(X2,mult(X1,X2)),X1),
inference(orient,[status(thm)],[t70922]) ).
cnf(t1155,plain,
rd(X1,mult(X2,X1)) = ld(mult(X2,X2),X2),
inference(cp,[status(thm)],[t12,t1126]) ).
cnf(t1298,plain,
rd(X1,mult(X2,X1)) = ld(mult(X2,X2),X2),
inference(orient,[status(thm)],[t1155]) ).
cnf(t1336,plain,
rd(true,mult(mult(X1,X1),true)) = rd(rd(X2,mult(X1,X2)),X1),
inference(cp,[status(thm)],[t270,t1298]) ).
cnf(t1343,plain,
rd(rd(X1,mult(X2,X1)),X2) = rd(true,mult(mult(X2,X2),true)),
inference(orient,[status(thm)],[t1336]) ).
cnf(t70923,plain,
ld(X1,rd(X2,mult(X1,X2))) = rd(true,mult(mult(X1,X1),true)),
inference(step,[status(thm)],[t1269,t1343]) ).
cnf(t1344,plain,
ld(X1,rd(X2,mult(X1,X2))) = rd(true,mult(mult(X1,X1),true)),
inference(orient,[status(thm)],[t70923]) ).
cnf(t70936,plain,
mult(X1,rd(true,mult(mult(X2,X2),true))) = mult(X2,ld(X2,rd(rd(X1,X2),X2))),
inference(step,[status(thm)],[t858,t1344]) ).
cnf(t70937,plain,
mult(X1,rd(true,mult(mult(X2,X2),true))) = rd(rd(X1,X2),X2),
inference(step,[status(thm)],[t70936,t7]) ).
cnf(t2068,plain,
mult(X1,rd(true,mult(mult(X2,X2),true))) = rd(rd(X1,X2),X2),
inference(orient,[status(thm)],[t70937]) ).
cnf(t217,plain,
rd(X1,true) = rd(X2,mult(rd(true,X1),X2)),
inference(cp,[status(thm)],[t24,t208]) ).
cnf(t285,plain,
rd(X1,mult(rd(true,X2),X1)) = rd(X2,true),
inference(orient,[status(thm)],[t217]) ).
cnf(t299,plain,
rd(mult(rd(X1,X2),true),true) = rd(X3,mult(rd(X2,X1),X3)),
inference(cp,[status(thm)],[t285,t293]) ).
cnf(t70890,plain,
rd(X1,X2) = rd(X3,mult(rd(X2,X1),X3)),
inference(step,[status(thm)],[t299,t10]) ).
cnf(t316,plain,
rd(X1,mult(rd(X2,X3),X1)) = rd(X3,X2),
inference(orient,[status(thm)],[t70890]) ).
cnf(t321,plain,
rd(X1,mult(X2,X1)) = rd(X3,mult(X2,X3)),
inference(cp,[status(thm)],[t316,t10]) ).
cnf(t551,plain,
rd(X1,mult(X2,X1)) = rd(X3,mult(X2,X3)),
inference(orient,[status(thm)],[t321]) ).
cnf(t2077,plain,
rd(rd(X1,X2),X2) = mult(X1,rd(X3,mult(mult(X2,X2),X3))),
inference(cp,[status(thm)],[t2068,t551]) ).
cnf(t3105,plain,
mult(X1,rd(X2,mult(mult(X3,X3),X2))) = rd(rd(X1,X3),X3),
inference(orient,[status(thm)],[t2077]) ).
cnf(t3717,plain,
rd(mult(mult(X1,X1),X2),rd(mult(mult(X1,X1),X2),X2)) = mult(rd(mult(mult(X1,X1),X2),X2),rd(rd(X2,X1),X1)),
inference(cp,[status(thm)],[t3687,t3105]) ).
cnf(t71050,plain,
rd(mult(mult(X1,X1),X2),mult(X1,X1)) = mult(rd(mult(mult(X1,X1),X2),X2),rd(rd(X2,X1),X1)),
inference(step,[status(thm)],[t3717,t10]) ).
cnf(t71051,plain,
rd(mult(mult(X1,X1),X2),mult(X1,X1)) = mult(mult(X1,X1),rd(rd(X2,X1),X1)),
inference(step,[status(thm)],[t71050,t10]) ).
cnf(t12044,plain,
mult(mult(X1,X1),rd(rd(X2,X1),X1)) = rd(mult(mult(X1,X1),X2),mult(X1,X1)),
inference(orient,[status(thm)],[t71051]) ).
cnf(t12113,plain,
rd(mult(mult(X1,X1),mult(X2,X1)),mult(X1,X1)) = mult(mult(X1,X1),rd(X2,X1)),
inference(cp,[status(thm)],[t12044,t10]) ).
cnf(t54156,plain,
rd(mult(mult(X1,X1),mult(X2,X1)),mult(X1,X1)) = mult(mult(X1,X1),rd(X2,X1)),
inference(orient,[status(thm)],[t12113]) ).
cnf(t43,plain,
ld(X1,X2) = ld(mult(X3,X1),mult(X1,mult(ld(X1,X3),X2))),
inference(cp,[status(thm)],[t12,t36]) ).
cnf(t4556,plain,
ld(mult(X1,X2),mult(X2,mult(ld(X2,X1),X3))) = ld(X2,X3),
inference(orient,[status(thm)],[t43]) ).
cnf(t4609,plain,
ld(X1,ld(ld(X1,X2),X3)) = ld(mult(X2,X1),mult(X1,X3)),
inference(cp,[status(thm)],[t4556,t7]) ).
cnf(t4648,plain,
ld(mult(X1,X2),mult(X2,X3)) = ld(X2,ld(ld(X2,X1),X3)),
inference(orient,[status(thm)],[t4609]) ).
cnf(t4721,plain,
ld(rd(X1,X2),ld(ld(rd(X1,X2),X3),X2)) = ld(mult(X3,rd(X1,X2)),X1),
inference(cp,[status(thm)],[t4648,t8]) ).
cnf(t71238,plain,
mult(rd(X2,X1),ld(ld(rd(X1,X2),X3),X2)) = ld(mult(X3,rd(X1,X2)),X1),
inference(step,[status(thm)],[t4721,t303]) ).
cnf(t71239,plain,
mult(rd(X2,X1),ld(mult(rd(X2,X1),X3),X2)) = ld(mult(X3,rd(X1,X2)),X1),
inference(step,[status(thm)],[t71238,t303]) ).
cnf(t48040,plain,
mult(rd(X1,X2),ld(mult(rd(X1,X2),X3),X1)) = ld(mult(X3,rd(X2,X1)),X2),
inference(orient,[status(thm)],[t71239]) ).
cnf(t55,plain,
mult(ld(X1,rd(X2,X1)),mult(X1,X3)) = ld(X1,mult(X2,X3)),
inference(cp,[status(thm)],[t48,t8]) ).
cnf(t565,plain,
mult(ld(X1,rd(X2,X1)),mult(X1,X3)) = ld(X1,mult(X2,X3)),
inference(orient,[status(thm)],[t55]) ).
cnf(t588,plain,
ld(X1,rd(X2,X1)) = rd(ld(X1,mult(X2,X3)),mult(X1,X3)),
inference(cp,[status(thm)],[t10,t565]) ).
cnf(t1427,plain,
rd(ld(X1,mult(X2,X3)),mult(X1,X3)) = ld(X1,rd(X2,X1)),
inference(orient,[status(thm)],[t588]) ).
cnf(t1438,plain,
ld(X1,rd(X2,X1)) = rd(ld(X1,X2),mult(X1,rd(X2,X2))),
inference(cp,[status(thm)],[t1427,t429]) ).
cnf(t2639,plain,
rd(ld(X1,X2),mult(X1,rd(X2,X2))) = ld(X1,rd(X2,X1)),
inference(orient,[status(thm)],[t1438]) ).
cnf(t2646,plain,
ld(X1,rd(mult(X1,X2),X1)) = rd(X2,mult(X1,rd(mult(X1,X2),mult(X1,X2)))),
inference(cp,[status(thm)],[t2639,t12]) ).
cnf(t15,plain,
mult(X1,mult(X2,mult(X1,ld(mult(mult(X1,X2),X1),X3)))) = X3,
inference(cp,[status(thm)],[t14,t7]) ).
cnf(t639,plain,
mult(X1,mult(X2,mult(X1,ld(mult(mult(X1,X2),X1),X3)))) = X3,
inference(orient,[status(thm)],[t15]) ).
cnf(t2096,plain,
rd(true,mult(mult(X1,X1),true)) = ld(X2,rd(rd(X2,X1),X1)),
inference(cp,[status(thm)],[t12,t2068]) ).
cnf(t2141,plain,
ld(X1,rd(rd(X1,X2),X2)) = rd(true,mult(mult(X2,X2),true)),
inference(orient,[status(thm)],[t2096]) ).
cnf(t2153,plain,
rd(true,mult(mult(X1,X1),true)) = ld(mult(X2,X1),rd(X2,X1)),
inference(cp,[status(thm)],[t2141,t10]) ).
cnf(t2198,plain,
ld(mult(X1,X2),rd(X1,X2)) = rd(true,mult(mult(X2,X2),true)),
inference(orient,[status(thm)],[t2153]) ).
cnf(t2252,plain,
rd(mult(X1,X2),X1) = mult(X1,mult(X2,mult(X1,rd(true,mult(mult(X1,X1),true))))),
inference(cp,[status(thm)],[t639,t2198]) ).
cnf(t70955,plain,
rd(mult(X1,X2),X1) = mult(X1,mult(X2,rd(rd(X1,X1),X1))),
inference(step,[status(thm)],[t2252,t2068]) ).
cnf(t70956,plain,
rd(mult(X1,X2),X1) = mult(X1,mult(X2,rd(true,mult(X1,true)))),
inference(step,[status(thm)],[t70955,t453]) ).
cnf(t3236,plain,
mult(X1,mult(X2,rd(true,mult(X1,true)))) = rd(mult(X1,X2),X1),
inference(orient,[status(thm)],[t70956]) ).
cnf(t3264,plain,
mult(X1,rd(true,mult(X2,true))) = ld(X2,rd(mult(X2,X1),X2)),
inference(cp,[status(thm)],[t12,t3236]) ).
cnf(t3307,plain,
ld(X1,rd(mult(X1,X2),X1)) = mult(X2,rd(true,mult(X1,true))),
inference(orient,[status(thm)],[t3264]) ).
cnf(t71187,plain,
mult(X2,rd(true,mult(X1,true))) = rd(X2,mult(X1,rd(mult(X1,X2),mult(X1,X2)))),
inference(step,[status(thm)],[t2646,t3307]) ).
cnf(t71188,plain,
mult(X2,rd(true,mult(X1,true))) = rd(X2,rd(rd(mult(X1,mult(X1,X2)),X2),X1)),
inference(step,[status(thm)],[t71187,t1833]) ).
cnf(t38030,plain,
rd(X1,rd(rd(mult(X2,mult(X2,X1)),X1),X2)) = mult(X1,rd(true,mult(X2,true))),
inference(orient,[status(thm)],[t71188]) ).
cnf(t306,plain,
mult(rd(X1,X2),mult(rd(X2,X1),X3)) = X3,
inference(cp,[status(thm)],[t303,t12]) ).
cnf(t358,plain,
mult(rd(X1,X2),mult(rd(X2,X1),X3)) = X3,
inference(orient,[status(thm)],[t306]) ).
cnf(t38053,plain,
mult(X1,rd(true,mult(rd(X2,X2),true))) = rd(X1,rd(rd(X1,X1),rd(X2,X2))),
inference(cp,[status(thm)],[t38030,t358]) ).
cnf(t71189,plain,
mult(X1,rd(X2,X2)) = rd(X1,rd(rd(X1,X1),rd(X2,X2))),
inference(step,[status(thm)],[t38053,t293]) ).
cnf(t38241,plain,
rd(X1,rd(rd(X1,X1),rd(X2,X2))) = mult(X1,rd(X2,X2)),
inference(orient,[status(thm)],[t71189]) ).
cnf(t38268,plain,
X1 = mult(mult(X1,rd(X2,X2)),rd(rd(X1,X1),rd(X2,X2))),
inference(cp,[status(thm)],[t8,t38241]) ).
cnf(t38366,plain,
mult(mult(X1,rd(X2,X2)),rd(rd(X1,X1),rd(X2,X2))) = X1,
inference(orient,[status(thm)],[t38268]) ).
cnf(t38425,plain,
rd(rd(X1,X1),rd(X2,X2)) = ld(mult(X1,rd(X2,X2)),X1),
inference(cp,[status(thm)],[t12,t38366]) ).
cnf(t38550,plain,
ld(mult(X1,rd(X2,X2)),X1) = rd(rd(X1,X1),rd(X2,X2)),
inference(orient,[status(thm)],[t38425]) ).
cnf(t38594,plain,
rd(true,mult(mult(X1,rd(X2,X2)),true)) = rd(rd(rd(X1,X1),rd(X2,X2)),X1),
inference(cp,[status(thm)],[t270,t38550]) ).
cnf(t38697,plain,
rd(rd(rd(X1,X1),rd(X2,X2)),X1) = rd(true,mult(mult(X1,rd(X2,X2)),true)),
inference(orient,[status(thm)],[t38594]) ).
cnf(t844,plain,
ld(rd(X1,mult(X2,X1)),rd(X3,rd(X1,mult(X2,X1)))) = mult(ld(rd(X1,mult(X2,X1)),X3),rd(Y3,ld(X2,Y3))),
inference(cp,[status(thm)],[t822,t326]) ).
cnf(t70931,plain,
mult(rd(mult(X2,X1),X1),rd(X3,rd(X1,mult(X2,X1)))) = mult(ld(rd(X1,mult(X2,X1)),X3),rd(Y3,ld(X2,Y3))),
inference(step,[status(thm)],[t844,t303]) ).
cnf(t70932,plain,
mult(X2,rd(X3,rd(X1,mult(X2,X1)))) = mult(ld(rd(X1,mult(X2,X1)),X3),rd(Y3,ld(X2,Y3))),
inference(step,[status(thm)],[t70931,t10]) ).
cnf(t70933,plain,
mult(X2,rd(X3,rd(X1,mult(X2,X1)))) = mult(mult(rd(mult(X2,X1),X1),X3),rd(Y3,ld(X2,Y3))),
inference(step,[status(thm)],[t70932,t303]) ).
cnf(t70934,plain,
mult(X2,rd(X3,rd(X1,mult(X2,X1)))) = mult(mult(X2,X3),rd(Y3,ld(X2,Y3))),
inference(step,[status(thm)],[t70933,t10]) ).
cnf(t70935,plain,
mult(X2,rd(X3,rd(X1,mult(X2,X1)))) = mult(mult(X2,X3),X2),
inference(step,[status(thm)],[t70934,t24]) ).
cnf(t1994,plain,
mult(X1,rd(X2,rd(X3,mult(X1,X3)))) = mult(mult(X1,X2),X1),
inference(orient,[status(thm)],[t70935]) ).
cnf(t2033,plain,
rd(X1,rd(X2,mult(X3,X2))) = ld(X3,mult(mult(X3,X1),X3)),
inference(cp,[status(thm)],[t12,t1994]) ).
cnf(t22035,plain,
rd(X1,rd(X2,mult(X3,X2))) = ld(X3,mult(mult(X3,X1),X3)),
inference(orient,[status(thm)],[t2033]) ).
cnf(t38700,plain,
rd(true,mult(mult(rd(X1,mult(X2,X1)),rd(X3,X3)),true)) = ld(X2,mult(mult(X2,rd(rd(rd(X1,mult(X2,X1)),rd(X1,mult(X2,X1))),rd(X3,X3))),X2)),
inference(cp,[status(thm)],[t38697,t22035]) ).
cnf(t71190,plain,
rd(true,mult(ld(X2,rd(X3,X3)),true)) = ld(X2,mult(mult(X2,rd(rd(rd(X1,mult(X2,X1)),rd(X1,mult(X2,X1))),rd(X3,X3))),X2)),
inference(step,[status(thm)],[t38700,t326]) ).
cnf(t71191,plain,
rd(true,mult(ld(X2,rd(X3,X3)),true)) = rd(rd(rd(rd(X1,mult(X2,X1)),rd(X1,mult(X2,X1))),rd(X3,X3)),rd(true,mult(X2,true))),
inference(step,[status(thm)],[t71190,t22035]) ).
cnf(t1685,plain,
mult(X1,rd(ld(X1,X2),X3)) = rd(rd(X2,ld(X1,X3)),X1),
inference(cp,[status(thm)],[t1679,t7]) ).
cnf(t1776,plain,
mult(X1,rd(ld(X1,X2),X3)) = rd(rd(X2,ld(X1,X3)),X1),
inference(orient,[status(thm)],[t1685]) ).
cnf(t1781,plain,
rd(rd(X1,ld(rd(X2,mult(X3,X2)),Y3)),rd(X2,mult(X3,X2))) = ld(X3,rd(ld(rd(X2,mult(X3,X2)),X1),Y3)),
inference(cp,[status(thm)],[t1776,t326]) ).
cnf(t71165,plain,
rd(rd(X1,mult(rd(mult(X3,X2),X2),Y3)),rd(X2,mult(X3,X2))) = ld(X3,rd(ld(rd(X2,mult(X3,X2)),X1),Y3)),
inference(step,[status(thm)],[t1781,t303]) ).
cnf(t71166,plain,
rd(rd(X1,mult(X3,Y3)),rd(X2,mult(X3,X2))) = ld(X3,rd(ld(rd(X2,mult(X3,X2)),X1),Y3)),
inference(step,[status(thm)],[t71165,t10]) ).
cnf(t71167,plain,
rd(rd(X1,mult(X3,Y3)),rd(X2,mult(X3,X2))) = ld(X3,rd(mult(rd(mult(X3,X2),X2),X1),Y3)),
inference(step,[status(thm)],[t71166,t303]) ).
cnf(t71168,plain,
rd(rd(X1,mult(X3,Y3)),rd(X2,mult(X3,X2))) = ld(X3,rd(mult(X3,X1),Y3)),
inference(step,[status(thm)],[t71167,t10]) ).
cnf(t30813,plain,
rd(rd(X1,mult(X2,X3)),rd(Y3,mult(X2,Y3))) = ld(X2,rd(mult(X2,X1),X3)),
inference(orient,[status(thm)],[t71168]) ).
cnf(t71192,plain,
rd(true,mult(ld(X2,rd(X3,X3)),true)) = rd(rd(ld(X2,rd(mult(X2,X1),X1)),rd(X3,X3)),rd(true,mult(X2,true))),
inference(step,[status(thm)],[t71191,t30813]) ).
cnf(t1836,plain,
rd(rd(mult(rd(X1,mult(X2,X1)),X3),Y3),rd(X1,mult(X2,X1))) = ld(X2,rd(X3,mult(rd(X1,mult(X2,X1)),Y3))),
inference(cp,[status(thm)],[t1833,t326]) ).
cnf(t71170,plain,
rd(rd(ld(X2,X3),Y3),rd(X1,mult(X2,X1))) = ld(X2,rd(X3,mult(rd(X1,mult(X2,X1)),Y3))),
inference(step,[status(thm)],[t1836,t326]) ).
cnf(t71171,plain,
rd(rd(ld(X2,X3),Y3),rd(X1,mult(X2,X1))) = ld(X2,rd(X3,ld(X2,Y3))),
inference(step,[status(thm)],[t71170,t326]) ).
cnf(t31416,plain,
rd(rd(ld(X1,X2),X3),rd(Y3,mult(X1,Y3))) = ld(X1,rd(X2,ld(X1,X3))),
inference(orient,[status(thm)],[t71171]) ).
cnf(t71193,plain,
rd(true,mult(ld(X2,rd(X3,X3)),true)) = ld(X2,rd(rd(mult(X2,X1),X1),ld(X2,rd(X3,X3)))),
inference(step,[status(thm)],[t71192,t31416]) ).
cnf(t71194,plain,
rd(true,mult(ld(X2,rd(X3,X3)),true)) = ld(X2,rd(X2,ld(X2,rd(X3,X3)))),
inference(step,[status(thm)],[t71193,t10]) ).
cnf(t38794,plain,
ld(X1,rd(X1,ld(X1,rd(X2,X2)))) = rd(true,mult(ld(X1,rd(X2,X2)),true)),
inference(orient,[status(thm)],[t71194]) ).
cnf(t4674,plain,
ld(rd(X1,mult(X2,X1)),ld(ld(rd(X1,mult(X2,X1)),ld(X2,X3)),Y3)) = ld(ld(X2,rd(X3,X2)),mult(rd(X1,mult(X2,X1)),Y3)),
inference(cp,[status(thm)],[t4648,t822]) ).
cnf(t70968,plain,
mult(rd(mult(X2,X1),X1),ld(ld(rd(X1,mult(X2,X1)),ld(X2,X3)),Y3)) = ld(ld(X2,rd(X3,X2)),mult(rd(X1,mult(X2,X1)),Y3)),
inference(step,[status(thm)],[t4674,t303]) ).
cnf(t70969,plain,
mult(X2,ld(ld(rd(X1,mult(X2,X1)),ld(X2,X3)),Y3)) = ld(ld(X2,rd(X3,X2)),mult(rd(X1,mult(X2,X1)),Y3)),
inference(step,[status(thm)],[t70968,t10]) ).
cnf(t70970,plain,
mult(X2,ld(mult(rd(mult(X2,X1),X1),ld(X2,X3)),Y3)) = ld(ld(X2,rd(X3,X2)),mult(rd(X1,mult(X2,X1)),Y3)),
inference(step,[status(thm)],[t70969,t303]) ).
cnf(t70971,plain,
mult(X2,ld(mult(X2,ld(X2,X3)),Y3)) = ld(ld(X2,rd(X3,X2)),mult(rd(X1,mult(X2,X1)),Y3)),
inference(step,[status(thm)],[t70970,t10]) ).
cnf(t70972,plain,
mult(X2,ld(X3,Y3)) = ld(ld(X2,rd(X3,X2)),mult(rd(X1,mult(X2,X1)),Y3)),
inference(step,[status(thm)],[t70971,t7]) ).
cnf(t70973,plain,
mult(X2,ld(X3,Y3)) = ld(ld(X2,rd(X3,X2)),ld(X2,Y3)),
inference(step,[status(thm)],[t70972,t326]) ).
cnf(t4871,plain,
ld(ld(X1,rd(X2,X1)),ld(X1,X3)) = mult(X1,ld(X2,X3)),
inference(orient,[status(thm)],[t70973]) ).
cnf(t4899,plain,
mult(X1,ld(mult(X2,X1),X3)) = ld(ld(X1,X2),ld(X1,X3)),
inference(cp,[status(thm)],[t4871,t10]) ).
cnf(t4945,plain,
ld(ld(X1,X2),ld(X1,X3)) = mult(X1,ld(mult(X2,X1),X3)),
inference(orient,[status(thm)],[t4899]) ).
cnf(t4946,plain,
mult(X1,ld(mult(X2,X1),X2)) = rd(ld(X1,X2),ld(X1,X2)),
inference(cp,[status(thm)],[t4945,t421]) ).
cnf(t5001,plain,
mult(X1,ld(mult(X2,X1),X2)) = rd(ld(X1,X2),ld(X1,X2)),
inference(orient,[status(thm)],[t4946]) ).
cnf(t5050,plain,
ld(mult(X1,X2),X1) = ld(X2,rd(ld(X2,X1),ld(X2,X1))),
inference(cp,[status(thm)],[t12,t5001]) ).
cnf(t5475,plain,
ld(X1,rd(ld(X1,X2),ld(X1,X2))) = ld(mult(X2,X1),X2),
inference(orient,[status(thm)],[t5050]) ).
cnf(t38806,plain,
rd(true,mult(ld(X1,rd(ld(X1,X2),ld(X1,X2))),true)) = ld(X1,rd(X1,ld(mult(X2,X1),X2))),
inference(cp,[status(thm)],[t38794,t5475]) ).
cnf(t71195,plain,
rd(true,mult(ld(mult(X2,X1),X2),true)) = ld(X1,rd(X1,ld(mult(X2,X1),X2))),
inference(step,[status(thm)],[t38806,t5475]) ).
cnf(t38918,plain,
ld(X1,rd(X1,ld(mult(X2,X1),X2))) = rd(true,mult(ld(mult(X2,X1),X2),true)),
inference(orient,[status(thm)],[t71195]) ).
cnf(t39017,plain,
rd(X1,ld(mult(X2,X1),X2)) = mult(X1,rd(true,mult(ld(mult(X2,X1),X2),true))),
inference(cp,[status(thm)],[t7,t38918]) ).
cnf(t69535,plain,
mult(X1,rd(true,mult(ld(mult(X2,X1),X2),true))) = rd(X1,ld(mult(X2,X1),X2)),
inference(orient,[status(thm)],[t39017]) ).
cnf(t69603,plain,
rd(rd(rd(X1,X1),rd(X2,X2)),ld(mult(mult(X1,rd(X2,X2)),rd(rd(X1,X1),rd(X2,X2))),mult(X1,rd(X2,X2)))) = mult(rd(rd(X1,X1),rd(X2,X2)),rd(true,mult(ld(X1,mult(X1,rd(X2,X2))),true))),
inference(cp,[status(thm)],[t69535,t38366]) ).
cnf(t71365,plain,
rd(rd(rd(X1,X1),rd(X2,X2)),ld(X1,mult(X1,rd(X2,X2)))) = mult(rd(rd(X1,X1),rd(X2,X2)),rd(true,mult(ld(X1,mult(X1,rd(X2,X2))),true))),
inference(step,[status(thm)],[t69603,t38366]) ).
cnf(t71366,plain,
rd(rd(rd(X1,X1),rd(X2,X2)),rd(X2,X2)) = mult(rd(rd(X1,X1),rd(X2,X2)),rd(true,mult(ld(X1,mult(X1,rd(X2,X2))),true))),
inference(step,[status(thm)],[t71365,t12]) ).
cnf(t3135,plain,
rd(rd(X1,rd(X2,X2)),rd(X2,X2)) = mult(X1,rd(X3,mult(rd(rd(X2,X2),rd(X2,X2)),X3))),
inference(cp,[status(thm)],[t3105,t375]) ).
cnf(t70960,plain,
rd(rd(X1,rd(X2,X2)),rd(X2,X2)) = mult(X1,rd(rd(X2,X2),rd(X2,X2))),
inference(step,[status(thm)],[t3135,t316]) ).
cnf(t70961,plain,
rd(rd(X1,rd(X2,X2)),rd(X2,X2)) = mult(X1,rd(X2,X2)),
inference(step,[status(thm)],[t70960,t497]) ).
cnf(t3952,plain,
rd(rd(X1,rd(X2,X2)),rd(X2,X2)) = mult(X1,rd(X2,X2)),
inference(orient,[status(thm)],[t70961]) ).
cnf(t71367,plain,
mult(rd(X1,X1),rd(X2,X2)) = mult(rd(rd(X1,X1),rd(X2,X2)),rd(true,mult(ld(X1,mult(X1,rd(X2,X2))),true))),
inference(step,[status(thm)],[t71366,t3952]) ).
cnf(t71368,plain,
mult(rd(X1,X1),rd(X2,X2)) = mult(rd(rd(X1,X1),rd(X2,X2)),rd(true,mult(rd(X2,X2),true))),
inference(step,[status(thm)],[t71367,t12]) ).
cnf(t71369,plain,
mult(rd(X1,X1),rd(X2,X2)) = mult(rd(rd(X1,X1),rd(X2,X2)),rd(X2,X2)),
inference(step,[status(thm)],[t71368,t293]) ).
cnf(t71370,plain,
mult(rd(X1,X1),rd(X2,X2)) = rd(X1,X1),
inference(step,[status(thm)],[t71369,t8]) ).
cnf(t69922,plain,
mult(rd(X1,X1),rd(X2,X2)) = rd(X1,X1),
inference(orient,[status(thm)],[t71370]) ).
cnf(t70055,plain,
ld(mult(rd(X1,X1),rd(X2,X2)),X2) = mult(rd(X2,X2),ld(rd(X2,X2),X2)),
inference(cp,[status(thm)],[t48040,t69922]) ).
cnf(t71373,plain,
ld(rd(X1,X1),X2) = mult(rd(X2,X2),ld(rd(X2,X2),X2)),
inference(step,[status(thm)],[t70055,t69922]) ).
cnf(t71374,plain,
mult(rd(X1,X1),X2) = mult(rd(X2,X2),ld(rd(X2,X2),X2)),
inference(step,[status(thm)],[t71373,t303]) ).
cnf(t71375,plain,
mult(rd(X1,X1),X2) = X2,
inference(step,[status(thm)],[t71374,t7]) ).
cnf(t70130,plain,
mult(rd(X1,X1),X2) = X2,
inference(orient,[status(thm)],[t71375]) ).
cnf(t70194,plain,
mult(mult(rd(X1,X1),rd(X1,X1)),rd(X2,rd(X1,X1))) = rd(mult(rd(X1,X1),mult(X2,rd(X1,X1))),mult(rd(X1,X1),rd(X1,X1))),
inference(cp,[status(thm)],[t54156,t70130]) ).
cnf(t71439,plain,
mult(rd(rd(X1,X1),rd(X1,X1)),rd(X2,rd(X1,X1))) = rd(mult(rd(X1,X1),mult(X2,rd(X1,X1))),mult(rd(X1,X1),rd(X1,X1))),
inference(step,[status(thm)],[t70194,t375]) ).
cnf(t71440,plain,
mult(rd(X1,X1),rd(X2,rd(X1,X1))) = rd(mult(rd(X1,X1),mult(X2,rd(X1,X1))),mult(rd(X1,X1),rd(X1,X1))),
inference(step,[status(thm)],[t71439,t497]) ).
cnf(t829,plain,
ld(rd(X1,X2),rd(X3,rd(X1,X2))) = mult(mult(rd(X2,X1),X3),rd(Y3,mult(rd(X1,X2),Y3))),
inference(cp,[status(thm)],[t822,t303]) ).
cnf(t71010,plain,
mult(rd(X2,X1),rd(X3,rd(X1,X2))) = mult(mult(rd(X2,X1),X3),rd(Y3,mult(rd(X1,X2),Y3))),
inference(step,[status(thm)],[t829,t303]) ).
cnf(t71011,plain,
mult(rd(X2,X1),rd(X3,rd(X1,X2))) = mult(mult(rd(X2,X1),X3),rd(X2,X1)),
inference(step,[status(thm)],[t71010,t316]) ).
cnf(t68,plain,
mult(mult(rd(X1,X2),X3),rd(X1,X2)) = rd(mult(rd(X1,X2),mult(X3,X1)),X2),
inference(cp,[status(thm)],[t59,t8]) ).
cnf(t8667,plain,
mult(mult(rd(X1,X2),X3),rd(X1,X2)) = rd(mult(rd(X1,X2),mult(X3,X1)),X2),
inference(orient,[status(thm)],[t68]) ).
cnf(t71012,plain,
mult(rd(X2,X1),rd(X3,rd(X1,X2))) = rd(mult(rd(X2,X1),mult(X3,X2)),X1),
inference(step,[status(thm)],[t71011,t8667]) ).
cnf(t9305,plain,
mult(rd(X1,X2),rd(X3,rd(X2,X1))) = rd(mult(rd(X1,X2),mult(X3,X1)),X2),
inference(orient,[status(thm)],[t71012]) ).
cnf(t743,plain,
rd(mult(X1,X2),ld(X1,ld(X3,X2))) = mult(mult(X1,X3),X1),
inference(cp,[status(thm)],[t734,t24]) ).
cnf(t1628,plain,
rd(mult(X1,X2),ld(X1,ld(X3,X2))) = mult(mult(X1,X3),X1),
inference(orient,[status(thm)],[t743]) ).
cnf(t1648,plain,
mult(mult(rd(X1,X2),X3),rd(X1,X2)) = rd(X1,ld(rd(X1,X2),ld(X3,X2))),
inference(cp,[status(thm)],[t1628,t8]) ).
cnf(t71021,plain,
rd(mult(rd(X1,X2),mult(X3,X1)),X2) = rd(X1,ld(rd(X1,X2),ld(X3,X2))),
inference(step,[status(thm)],[t1648,t8667]) ).
cnf(t71022,plain,
rd(mult(rd(X1,X2),mult(X3,X1)),X2) = rd(X1,mult(rd(X2,X1),ld(X3,X2))),
inference(step,[status(thm)],[t71021,t303]) ).
cnf(t10101,plain,
rd(mult(rd(X1,X2),mult(X3,X1)),X2) = rd(X1,mult(rd(X2,X1),ld(X3,X2))),
inference(orient,[status(thm)],[t71022]) ).
cnf(t71025,plain,
mult(rd(X1,X2),rd(X3,rd(X2,X1))) = rd(X1,mult(rd(X2,X1),ld(X3,X2))),
inference(step,[status(thm)],[t9305,t10101]) ).
cnf(t10104,plain,
mult(rd(X1,X2),rd(X3,rd(X2,X1))) = rd(X1,mult(rd(X2,X1),ld(X3,X2))),
inference(orient,[status(thm)],[t71025]) ).
cnf(t71441,plain,
rd(X1,mult(rd(X1,X1),ld(X2,X1))) = rd(mult(rd(X1,X1),mult(X2,rd(X1,X1))),mult(rd(X1,X1),rd(X1,X1))),
inference(step,[status(thm)],[t71440,t10104]) ).
cnf(t71442,plain,
rd(X1,ld(X2,X1)) = rd(mult(rd(X1,X1),mult(X2,rd(X1,X1))),mult(rd(X1,X1),rd(X1,X1))),
inference(step,[status(thm)],[t71441,t70130]) ).
cnf(t71443,plain,
X2 = rd(mult(rd(X1,X1),mult(X2,rd(X1,X1))),mult(rd(X1,X1),rd(X1,X1))),
inference(step,[status(thm)],[t71442,t24]) ).
cnf(t3727,plain,
rd(mult(rd(X1,X2),X3),rd(mult(rd(X1,X2),X3),X3)) = mult(rd(mult(rd(X1,X2),X3),X3),mult(X3,rd(X2,X1))),
inference(cp,[status(thm)],[t3687,t316]) ).
cnf(t71052,plain,
rd(mult(rd(X1,X2),X3),rd(X1,X2)) = mult(rd(mult(rd(X1,X2),X3),X3),mult(X3,rd(X2,X1))),
inference(step,[status(thm)],[t3727,t10]) ).
cnf(t71053,plain,
rd(mult(rd(X1,X2),X3),rd(X1,X2)) = mult(rd(X1,X2),mult(X3,rd(X2,X1))),
inference(step,[status(thm)],[t71052,t10]) ).
cnf(t12191,plain,
mult(rd(X1,X2),mult(X3,rd(X2,X1))) = rd(mult(rd(X1,X2),X3),rd(X1,X2)),
inference(orient,[status(thm)],[t71053]) ).
cnf(t71444,plain,
X2 = rd(rd(mult(rd(X1,X1),X2),rd(X1,X1)),mult(rd(X1,X1),rd(X1,X1))),
inference(step,[status(thm)],[t71443,t12191]) ).
cnf(t71445,plain,
X2 = rd(rd(X2,rd(X1,X1)),mult(rd(X1,X1),rd(X1,X1))),
inference(step,[status(thm)],[t71444,t70130]) ).
cnf(t71446,plain,
X2 = rd(rd(X2,rd(X1,X1)),rd(rd(X1,X1),rd(X1,X1))),
inference(step,[status(thm)],[t71445,t375]) ).
cnf(t71447,plain,
X2 = rd(rd(X2,rd(X1,X1)),rd(X1,X1)),
inference(step,[status(thm)],[t71446,t497]) ).
cnf(t71448,plain,
X2 = mult(X2,rd(X1,X1)),
inference(step,[status(thm)],[t71447,t3952]) ).
cnf(t70633,plain,
mult(X1,rd(X2,X2)) = X1,
inference(orient,[status(thm)],[t71448]) ).
cnf(t70734,plain,
true = ifeq(sk0(rd(X1,X1)),sk0(rd(X1,X1)),ifeq(mult(rd(X1,X1),sk0(rd(X1,X1))),sk0(rd(X1,X1)),false,true),true),
inference(cp,[status(thm)],[t22,t70633]) ).
cnf(t0,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t9,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t0]) ).
cnf(t71467,plain,
true = ifeq(mult(rd(X1,X1),sk0(rd(X1,X1))),sk0(rd(X1,X1)),false,true),
inference(step,[status(thm)],[t70734,t9]) ).
cnf(t71468,plain,
true = ifeq(sk0(rd(X1,X1)),sk0(rd(X1,X1)),false,true),
inference(step,[status(thm)],[t71467,t70130]) ).
cnf(t71469,plain,
true = false,
inference(step,[status(thm)],[t71468,t9]) ).
cnf(t70883,plain,
false = true,
inference(orient,[status(thm)],[t71469]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c5]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t70883]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : GRP654+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.02 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.02/0.29 % Computer : n012.cluster.edu
% 0.02/0.29 % Model : x86_64 x86_64
% 0.02/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.02/0.29 % Memory : 8046.5625MB
% 0.02/0.29 % OS : Linux 6.8.0-71-generic
% 0.02/0.29 % CPULimit : 300
% 0.02/0.29 % WCLimit : 300
% 0.02/0.29 % DateTime : Wed Sep 23 15:29:50 UTC 2026
% 0.02/0.30 % CPUTime :
% 0.02/0.30 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 35.96/5.00 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 35.96/5.00 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------