%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP654-10 : TPTP v9.3.1. Released v8.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n004.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:50 PM UTC 2026
% Result : Unsatisfiable 47.47s 6.46s
% Output : CNFRefutation 47.47s
% Verified :
% SZS Type : Refutation
% Derivation depth : 136
% Number of leaves : 8
% Syntax : Number of clauses : 311 ( 311 unt; 0 nHn; 6 RR)
% Number of literals : 311 ( 310 equ; 3 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 2 con; 0-2 aty)
% Number of variables : 728 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(eg0,negated_conjecture,
tuple(mult(X0,x1(X0)),mult(x1_2(X0),X0)) != tuple(x1(X0),x1_2(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t6,plain,
eq(tuple(mult(X1,x1(X1)),mult(x1_2(X1),X1)),tuple(x1(X1),x1_2(X1))) = efalse,
inference(equality_encoding,[status(esa)],[eg0]) ).
cnf(t22,plain,
eq(tuple(mult(X1,x1(X1)),mult(x1_2(X1),X1)),tuple(x1(X1),x1_2(X1))) = efalse,
inference(orient,[status(thm)],[t6]) ).
cnf(t4,axiom,
rd(mult(X1,X2),X2) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t9,plain,
rd(mult(X1,X2),X2) = X1,
inference(orient,[status(thm)],[t4]) ).
cnf(t5,axiom,
mult(mult(mult(X1,X2),X1),X3) = mult(X1,mult(X2,mult(X1,X3))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t13,plain,
mult(mult(mult(X1,X2),X1),X3) = mult(X1,mult(X2,mult(X1,X3))),
inference(orient,[status(thm)],[t5]) ).
cnf(t18,plain,
mult(mult(X1,X2),X1) = rd(mult(X1,mult(X2,mult(X1,X3))),X3),
inference(cp,[status(thm)],[t9,t13]) ).
cnf(t59,plain,
rd(mult(X1,mult(X2,mult(X1,X3))),X3) = mult(mult(X1,X2),X1),
inference(orient,[status(thm)],[t18]) ).
cnf(t3,axiom,
mult(rd(X1,X2),X2) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
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]) ).
cnf(t2,axiom,
mult(X1,ld(X1,X2)) = X2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
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)],[t9,t734]) ).
cnf(t1679,plain,
rd(rd(mult(X1,X2),ld(X1,X3)),X1) = mult(X1,rd(X2,X3)),
inference(orient,[status(thm)],[t757]) ).
cnf(t1,axiom,
ld(X1,mult(X1,X2)) = X2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t11,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,t11]) ).
cnf(t1833,plain,
mult(X1,rd(X2,mult(X1,X3))) = rd(rd(mult(X1,X2),X3),X1),
inference(orient,[status(thm)],[t1711]) ).
cnf(t10,plain,
X1 = rd(X2,ld(X1,X2)),
inference(cp,[status(thm)],[t9,t7]) ).
cnf(t24,plain,
rd(X1,ld(X2,X1)) = X2,
inference(orient,[status(thm)],[t10]) ).
cnf(t15,plain,
mult(X1,mult(ld(X1,X2),mult(X1,X3))) = mult(mult(X2,X1),X3),
inference(cp,[status(thm)],[t13,t7]) ).
cnf(t26,plain,
mult(X1,mult(ld(X1,X2),mult(X1,X3))) = mult(mult(X2,X1),X3),
inference(orient,[status(thm)],[t15]) ).
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)],[t11,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,t11]) ).
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)],[t9,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,t11]) ).
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)],[t9,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(t70877,plain,
ld(X1,X2) = mult(rd(ld(X1,etrue),etrue),X2),
inference(step,[status(thm)],[t145,t132]) ).
cnf(t165,plain,
mult(rd(ld(X1,etrue),etrue),X2) = ld(X1,X2),
inference(orient,[status(thm)],[t70877]) ).
cnf(t12,plain,
X1 = ld(rd(X2,X1),X2),
inference(cp,[status(thm)],[t11,t8]) ).
cnf(t25,plain,
ld(rd(X1,X2),X1) = X2,
inference(orient,[status(thm)],[t12]) ).
cnf(t170,plain,
ld(rd(etrue,X1),X2) = mult(rd(X1,etrue),X2),
inference(cp,[status(thm)],[t165,t25]) ).
cnf(t182,plain,
ld(rd(etrue,X1),X2) = mult(rd(X1,etrue),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(t70878,plain,
ld(rd(ld(X1,etrue),etrue),X2) = mult(X1,X2),
inference(step,[status(thm)],[t147,t132]) ).
cnf(t195,plain,
ld(rd(ld(X1,etrue),etrue),X2) = mult(X1,X2),
inference(orient,[status(thm)],[t70878]) ).
cnf(t199,plain,
mult(rd(etrue,X1),X2) = ld(rd(X1,etrue),X2),
inference(cp,[status(thm)],[t195,t25]) ).
cnf(t208,plain,
ld(rd(X1,etrue),X2) = mult(rd(etrue,X1),X2),
inference(orient,[status(thm)],[t199]) ).
cnf(t213,plain,
mult(rd(etrue,mult(X1,etrue)),X2) = ld(X1,X2),
inference(cp,[status(thm)],[t208,t9]) ).
cnf(t253,plain,
mult(rd(etrue,mult(X1,etrue)),X2) = ld(X1,X2),
inference(orient,[status(thm)],[t213]) ).
cnf(t260,plain,
rd(etrue,mult(X1,etrue)) = rd(ld(X1,X2),X2),
inference(cp,[status(thm)],[t9,t253]) ).
cnf(t270,plain,
rd(ld(X1,X2),X2) = rd(etrue,mult(X1,etrue)),
inference(orient,[status(thm)],[t260]) ).
cnf(t274,plain,
rd(etrue,mult(rd(X1,X2),etrue)) = rd(X2,X1),
inference(cp,[status(thm)],[t270,t25]) ).
cnf(t293,plain,
rd(etrue,mult(rd(X1,X2),etrue)) = rd(X2,X1),
inference(orient,[status(thm)],[t274]) ).
cnf(t296,plain,
mult(rd(mult(rd(X1,X2),etrue),etrue),X3) = ld(rd(X2,X1),X3),
inference(cp,[status(thm)],[t182,t293]) ).
cnf(t70880,plain,
mult(rd(X1,X2),X3) = ld(rd(X2,X1),X3),
inference(step,[status(thm)],[t296,t9]) ).
cnf(t303,plain,
ld(rd(X1,X2),X3) = mult(rd(X2,X1),X3),
inference(orient,[status(thm)],[t70880]) ).
cnf(t70882,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(t70883,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)],[t70882,t9]) ).
cnf(t308,plain,
mult(rd(X1,mult(X2,X1)),X3) = ld(X2,X3),
inference(cp,[status(thm)],[t303,t9]) ).
cnf(t326,plain,
mult(rd(X1,mult(X2,X1)),X3) = ld(X2,X3),
inference(orient,[status(thm)],[t308]) ).
cnf(t70884,plain,
mult(rd(X1,X1),mult(X1,X3)) = ld(X1,mult(ld(rd(X2,mult(X1,X2)),X1),X3)),
inference(step,[status(thm)],[t70883,t326]) ).
cnf(t70885,plain,
mult(rd(X1,X1),mult(X1,X3)) = ld(X1,mult(mult(rd(mult(X1,X2),X2),X1),X3)),
inference(step,[status(thm)],[t70884,t303]) ).
cnf(t32,plain,
mult(ld(X1,X2),mult(X1,X3)) = ld(X1,mult(mult(X2,X1),X3)),
inference(cp,[status(thm)],[t11,t26]) ).
cnf(t48,plain,
ld(X1,mult(mult(X2,X1),X3)) = mult(ld(X1,X2),mult(X1,X3)),
inference(orient,[status(thm)],[t32]) ).
cnf(t70886,plain,
mult(rd(X1,X1),mult(X1,X3)) = mult(ld(X1,rd(mult(X1,X2),X2)),mult(X1,X3)),
inference(step,[status(thm)],[t70885,t48]) ).
cnf(t70887,plain,
mult(rd(X1,X1),mult(X1,X3)) = mult(ld(X1,X1),mult(X1,X3)),
inference(step,[status(thm)],[t70886,t9]) ).
cnf(t395,plain,
mult(ld(X1,X1),mult(X1,X2)) = mult(rd(X1,X1),mult(X1,X2)),
inference(orient,[status(thm)],[t70887]) ).
cnf(t410,plain,
ld(X1,X1) = rd(mult(rd(X1,X1),mult(X1,X2)),mult(X1,X2)),
inference(cp,[status(thm)],[t9,t395]) ).
cnf(t70888,plain,
ld(X1,X1) = rd(X1,X1),
inference(step,[status(thm)],[t410,t9]) ).
cnf(t421,plain,
ld(X1,X1) = rd(X1,X1),
inference(orient,[status(thm)],[t70888]) ).
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(t70943,plain,
mult(X1,rd(X1,X2)) = rd(X1,ld(rd(X1,X2),rd(X2,X2))),
inference(step,[status(thm)],[t1605,t8]) ).
cnf(t70944,plain,
mult(X1,rd(X1,X2)) = rd(X1,mult(rd(X2,X1),rd(X2,X2))),
inference(step,[status(thm)],[t70943,t303]) ).
cnf(t2899,plain,
rd(X1,mult(rd(X2,X1),rd(X2,X2))) = mult(X1,rd(X1,X2)),
inference(orient,[status(thm)],[t70944]) ).
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(t70949,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(t70950,plain,
rd(X1,rd(X1,X2)) = mult(rd(X1,X2),mult(X2,rd(X2,X1))),
inference(step,[status(thm)],[t70949,t445]) ).
cnf(t3687,plain,
mult(rd(X1,X2),mult(X2,rd(X2,X1))) = rd(X1,rd(X1,X2)),
inference(orient,[status(thm)],[t70950]) ).
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(t70898,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(t70899,plain,
mult(ld(X2,X3),rd(X1,mult(X2,X1))) = rd(ld(X2,mult(X3,ld(X2,Y3))),Y3),
inference(step,[status(thm)],[t70898,t326]) ).
cnf(t70900,plain,
mult(ld(X2,X3),rd(X1,mult(X2,X1))) = rd(mult(ld(X2,rd(X3,X2)),Y3),Y3),
inference(step,[status(thm)],[t70899,t86]) ).
cnf(t70901,plain,
mult(ld(X2,X3),rd(X1,mult(X2,X1))) = ld(X2,rd(X3,X2)),
inference(step,[status(thm)],[t70900,t9]) ).
cnf(t822,plain,
mult(ld(X1,X2),rd(X3,mult(X1,X3))) = ld(X1,rd(X2,X1)),
inference(orient,[status(thm)],[t70901]) ).
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(etrue,mult(X1,etrue)) = rd(rd(X1,X1),X1),
inference(cp,[status(thm)],[t270,t421]) ).
cnf(t453,plain,
rd(rd(X1,X1),X1) = rd(etrue,mult(X1,etrue)),
inference(orient,[status(thm)],[t424]) ).
cnf(t70904,plain,
mult(ld(X1,rd(etrue,mult(X1,etrue))),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(t70889,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(t70890,plain,
mult(rd(X1,X1),mult(X1,rd(X1,X1))) = mult(X1,rd(rd(X1,X1),rd(X1,X1))),
inference(step,[status(thm)],[t70889,t8]) ).
cnf(t70891,plain,
mult(rd(X1,X1),X1) = mult(X1,rd(rd(X1,X1),rd(X1,X1))),
inference(step,[status(thm)],[t70890,t429]) ).
cnf(t70892,plain,
X1 = mult(X1,rd(rd(X1,X1),rd(X1,X1))),
inference(step,[status(thm)],[t70891,t8]) ).
cnf(t479,plain,
mult(X1,rd(rd(X1,X1),rd(X1,X1))) = X1,
inference(orient,[status(thm)],[t70892]) ).
cnf(t484,plain,
rd(rd(X1,X1),rd(X1,X1)) = ld(X1,X1),
inference(cp,[status(thm)],[t11,t479]) ).
cnf(t70893,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)],[t70893]) ).
cnf(t70905,plain,
mult(ld(X1,rd(etrue,mult(X1,etrue))),X1) = ld(X1,rd(X1,X1)),
inference(step,[status(thm)],[t70904,t497]) ).
cnf(t70879,plain,
ld(X1,rd(X1,X1)) = rd(etrue,mult(X1,etrue)),
inference(step,[status(thm)],[t132,t270]) ).
cnf(t277,plain,
ld(X1,rd(X1,X1)) = rd(etrue,mult(X1,etrue)),
inference(rw,[status(thm)],[t70879]) ).
cnf(t278,plain,
ld(X1,rd(X1,X1)) = rd(etrue,mult(X1,etrue)),
inference(orient,[status(thm)],[t277]) ).
cnf(t70906,plain,
mult(ld(X1,rd(etrue,mult(X1,etrue))),X1) = rd(etrue,mult(X1,etrue)),
inference(step,[status(thm)],[t70905,t278]) ).
cnf(t1092,plain,
mult(ld(X1,rd(etrue,mult(X1,etrue))),X1) = rd(etrue,mult(X1,etrue)),
inference(orient,[status(thm)],[t70906]) ).
cnf(t1101,plain,
rd(etrue,mult(rd(X1,mult(X2,X1)),etrue)) = mult(ld(rd(X1,mult(X2,X1)),rd(etrue,ld(X2,etrue))),rd(X1,mult(X2,X1))),
inference(cp,[status(thm)],[t1092,t326]) ).
cnf(t70907,plain,
rd(mult(X2,X1),X1) = mult(ld(rd(X1,mult(X2,X1)),rd(etrue,ld(X2,etrue))),rd(X1,mult(X2,X1))),
inference(step,[status(thm)],[t1101,t293]) ).
cnf(t70908,plain,
X2 = mult(ld(rd(X1,mult(X2,X1)),rd(etrue,ld(X2,etrue))),rd(X1,mult(X2,X1))),
inference(step,[status(thm)],[t70907,t9]) ).
cnf(t70909,plain,
X2 = mult(mult(rd(mult(X2,X1),X1),rd(etrue,ld(X2,etrue))),rd(X1,mult(X2,X1))),
inference(step,[status(thm)],[t70908,t303]) ).
cnf(t70910,plain,
X2 = mult(mult(X2,rd(etrue,ld(X2,etrue))),rd(X1,mult(X2,X1))),
inference(step,[status(thm)],[t70909,t9]) ).
cnf(t70911,plain,
X2 = mult(mult(X2,X2),rd(X1,mult(X2,X1))),
inference(step,[status(thm)],[t70910,t24]) ).
cnf(t1126,plain,
mult(mult(X1,X1),rd(X2,mult(X1,X2))) = X1,
inference(orient,[status(thm)],[t70911]) ).
cnf(t1156,plain,
mult(X1,X1) = rd(X1,rd(X2,mult(X1,X2))),
inference(cp,[status(thm)],[t9,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(t70912,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(t70913,plain,
ld(X2,rd(X1,mult(X2,X1))) = rd(rd(X1,mult(X2,X1)),X2),
inference(step,[status(thm)],[t70912,t24]) ).
cnf(t1269,plain,
ld(X1,rd(X2,mult(X1,X2))) = rd(rd(X2,mult(X1,X2)),X1),
inference(orient,[status(thm)],[t70913]) ).
cnf(t1155,plain,
rd(X1,mult(X2,X1)) = ld(mult(X2,X2),X2),
inference(cp,[status(thm)],[t11,t1126]) ).
cnf(t1298,plain,
rd(X1,mult(X2,X1)) = ld(mult(X2,X2),X2),
inference(orient,[status(thm)],[t1155]) ).
cnf(t1336,plain,
rd(etrue,mult(mult(X1,X1),etrue)) = rd(rd(X2,mult(X1,X2)),X1),
inference(cp,[status(thm)],[t270,t1298]) ).
cnf(t1343,plain,
rd(rd(X1,mult(X2,X1)),X2) = rd(etrue,mult(mult(X2,X2),etrue)),
inference(orient,[status(thm)],[t1336]) ).
cnf(t70914,plain,
ld(X1,rd(X2,mult(X1,X2))) = rd(etrue,mult(mult(X1,X1),etrue)),
inference(step,[status(thm)],[t1269,t1343]) ).
cnf(t1344,plain,
ld(X1,rd(X2,mult(X1,X2))) = rd(etrue,mult(mult(X1,X1),etrue)),
inference(orient,[status(thm)],[t70914]) ).
cnf(t70927,plain,
mult(X1,rd(etrue,mult(mult(X2,X2),etrue))) = mult(X2,ld(X2,rd(rd(X1,X2),X2))),
inference(step,[status(thm)],[t858,t1344]) ).
cnf(t70928,plain,
mult(X1,rd(etrue,mult(mult(X2,X2),etrue))) = rd(rd(X1,X2),X2),
inference(step,[status(thm)],[t70927,t7]) ).
cnf(t2068,plain,
mult(X1,rd(etrue,mult(mult(X2,X2),etrue))) = rd(rd(X1,X2),X2),
inference(orient,[status(thm)],[t70928]) ).
cnf(t217,plain,
rd(X1,etrue) = rd(X2,mult(rd(etrue,X1),X2)),
inference(cp,[status(thm)],[t24,t208]) ).
cnf(t285,plain,
rd(X1,mult(rd(etrue,X2),X1)) = rd(X2,etrue),
inference(orient,[status(thm)],[t217]) ).
cnf(t299,plain,
rd(mult(rd(X1,X2),etrue),etrue) = rd(X3,mult(rd(X2,X1),X3)),
inference(cp,[status(thm)],[t285,t293]) ).
cnf(t70881,plain,
rd(X1,X2) = rd(X3,mult(rd(X2,X1),X3)),
inference(step,[status(thm)],[t299,t9]) ).
cnf(t316,plain,
rd(X1,mult(rd(X2,X3),X1)) = rd(X3,X2),
inference(orient,[status(thm)],[t70881]) ).
cnf(t321,plain,
rd(X1,mult(X2,X1)) = rd(X3,mult(X2,X3)),
inference(cp,[status(thm)],[t316,t9]) ).
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(t71041,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,t9]) ).
cnf(t71042,plain,
rd(mult(mult(X1,X1),X2),mult(X1,X1)) = mult(mult(X1,X1),rd(rd(X2,X1),X1)),
inference(step,[status(thm)],[t71041,t9]) ).
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)],[t71042]) ).
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,t9]) ).
cnf(t54145,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)],[t11,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(t71229,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(t71230,plain,
mult(rd(X2,X1),ld(mult(rd(X2,X1),X3),X2)) = ld(mult(X3,rd(X1,X2)),X1),
inference(step,[status(thm)],[t71229,t303]) ).
cnf(t48029,plain,
mult(rd(X1,X2),ld(mult(rd(X1,X2),X3),X1)) = ld(mult(X3,rd(X2,X1)),X2),
inference(orient,[status(thm)],[t71230]) ).
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)],[t9,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,t11]) ).
cnf(t14,plain,
mult(X1,mult(X2,mult(X1,ld(mult(mult(X1,X2),X1),X3)))) = X3,
inference(cp,[status(thm)],[t13,t7]) ).
cnf(t639,plain,
mult(X1,mult(X2,mult(X1,ld(mult(mult(X1,X2),X1),X3)))) = X3,
inference(orient,[status(thm)],[t14]) ).
cnf(t2096,plain,
rd(etrue,mult(mult(X1,X1),etrue)) = ld(X2,rd(rd(X2,X1),X1)),
inference(cp,[status(thm)],[t11,t2068]) ).
cnf(t2141,plain,
ld(X1,rd(rd(X1,X2),X2)) = rd(etrue,mult(mult(X2,X2),etrue)),
inference(orient,[status(thm)],[t2096]) ).
cnf(t2153,plain,
rd(etrue,mult(mult(X1,X1),etrue)) = ld(mult(X2,X1),rd(X2,X1)),
inference(cp,[status(thm)],[t2141,t9]) ).
cnf(t2198,plain,
ld(mult(X1,X2),rd(X1,X2)) = rd(etrue,mult(mult(X2,X2),etrue)),
inference(orient,[status(thm)],[t2153]) ).
cnf(t2252,plain,
rd(mult(X1,X2),X1) = mult(X1,mult(X2,mult(X1,rd(etrue,mult(mult(X1,X1),etrue))))),
inference(cp,[status(thm)],[t639,t2198]) ).
cnf(t70946,plain,
rd(mult(X1,X2),X1) = mult(X1,mult(X2,rd(rd(X1,X1),X1))),
inference(step,[status(thm)],[t2252,t2068]) ).
cnf(t70947,plain,
rd(mult(X1,X2),X1) = mult(X1,mult(X2,rd(etrue,mult(X1,etrue)))),
inference(step,[status(thm)],[t70946,t453]) ).
cnf(t3236,plain,
mult(X1,mult(X2,rd(etrue,mult(X1,etrue)))) = rd(mult(X1,X2),X1),
inference(orient,[status(thm)],[t70947]) ).
cnf(t3264,plain,
mult(X1,rd(etrue,mult(X2,etrue))) = ld(X2,rd(mult(X2,X1),X2)),
inference(cp,[status(thm)],[t11,t3236]) ).
cnf(t3307,plain,
ld(X1,rd(mult(X1,X2),X1)) = mult(X2,rd(etrue,mult(X1,etrue))),
inference(orient,[status(thm)],[t3264]) ).
cnf(t71178,plain,
mult(X2,rd(etrue,mult(X1,etrue))) = rd(X2,mult(X1,rd(mult(X1,X2),mult(X1,X2)))),
inference(step,[status(thm)],[t2646,t3307]) ).
cnf(t71179,plain,
mult(X2,rd(etrue,mult(X1,etrue))) = rd(X2,rd(rd(mult(X1,mult(X1,X2)),X2),X1)),
inference(step,[status(thm)],[t71178,t1833]) ).
cnf(t38019,plain,
rd(X1,rd(rd(mult(X2,mult(X2,X1)),X1),X2)) = mult(X1,rd(etrue,mult(X2,etrue))),
inference(orient,[status(thm)],[t71179]) ).
cnf(t306,plain,
mult(rd(X1,X2),mult(rd(X2,X1),X3)) = X3,
inference(cp,[status(thm)],[t303,t11]) ).
cnf(t358,plain,
mult(rd(X1,X2),mult(rd(X2,X1),X3)) = X3,
inference(orient,[status(thm)],[t306]) ).
cnf(t38042,plain,
mult(X1,rd(etrue,mult(rd(X2,X2),etrue))) = rd(X1,rd(rd(X1,X1),rd(X2,X2))),
inference(cp,[status(thm)],[t38019,t358]) ).
cnf(t71180,plain,
mult(X1,rd(X2,X2)) = rd(X1,rd(rd(X1,X1),rd(X2,X2))),
inference(step,[status(thm)],[t38042,t293]) ).
cnf(t38230,plain,
rd(X1,rd(rd(X1,X1),rd(X2,X2))) = mult(X1,rd(X2,X2)),
inference(orient,[status(thm)],[t71180]) ).
cnf(t38257,plain,
X1 = mult(mult(X1,rd(X2,X2)),rd(rd(X1,X1),rd(X2,X2))),
inference(cp,[status(thm)],[t8,t38230]) ).
cnf(t38355,plain,
mult(mult(X1,rd(X2,X2)),rd(rd(X1,X1),rd(X2,X2))) = X1,
inference(orient,[status(thm)],[t38257]) ).
cnf(t38414,plain,
rd(rd(X1,X1),rd(X2,X2)) = ld(mult(X1,rd(X2,X2)),X1),
inference(cp,[status(thm)],[t11,t38355]) ).
cnf(t38539,plain,
ld(mult(X1,rd(X2,X2)),X1) = rd(rd(X1,X1),rd(X2,X2)),
inference(orient,[status(thm)],[t38414]) ).
cnf(t38583,plain,
rd(etrue,mult(mult(X1,rd(X2,X2)),etrue)) = rd(rd(rd(X1,X1),rd(X2,X2)),X1),
inference(cp,[status(thm)],[t270,t38539]) ).
cnf(t38686,plain,
rd(rd(rd(X1,X1),rd(X2,X2)),X1) = rd(etrue,mult(mult(X1,rd(X2,X2)),etrue)),
inference(orient,[status(thm)],[t38583]) ).
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(t70922,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(t70923,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)],[t70922,t9]) ).
cnf(t70924,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)],[t70923,t303]) ).
cnf(t70925,plain,
mult(X2,rd(X3,rd(X1,mult(X2,X1)))) = mult(mult(X2,X3),rd(Y3,ld(X2,Y3))),
inference(step,[status(thm)],[t70924,t9]) ).
cnf(t70926,plain,
mult(X2,rd(X3,rd(X1,mult(X2,X1)))) = mult(mult(X2,X3),X2),
inference(step,[status(thm)],[t70925,t24]) ).
cnf(t1994,plain,
mult(X1,rd(X2,rd(X3,mult(X1,X3)))) = mult(mult(X1,X2),X1),
inference(orient,[status(thm)],[t70926]) ).
cnf(t2033,plain,
rd(X1,rd(X2,mult(X3,X2))) = ld(X3,mult(mult(X3,X1),X3)),
inference(cp,[status(thm)],[t11,t1994]) ).
cnf(t22024,plain,
rd(X1,rd(X2,mult(X3,X2))) = ld(X3,mult(mult(X3,X1),X3)),
inference(orient,[status(thm)],[t2033]) ).
cnf(t38689,plain,
rd(etrue,mult(mult(rd(X1,mult(X2,X1)),rd(X3,X3)),etrue)) = 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)],[t38686,t22024]) ).
cnf(t71181,plain,
rd(etrue,mult(ld(X2,rd(X3,X3)),etrue)) = 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)],[t38689,t326]) ).
cnf(t71182,plain,
rd(etrue,mult(ld(X2,rd(X3,X3)),etrue)) = rd(rd(rd(rd(X1,mult(X2,X1)),rd(X1,mult(X2,X1))),rd(X3,X3)),rd(etrue,mult(X2,etrue))),
inference(step,[status(thm)],[t71181,t22024]) ).
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(t71156,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(t71157,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)],[t71156,t9]) ).
cnf(t71158,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)],[t71157,t303]) ).
cnf(t71159,plain,
rd(rd(X1,mult(X3,Y3)),rd(X2,mult(X3,X2))) = ld(X3,rd(mult(X3,X1),Y3)),
inference(step,[status(thm)],[t71158,t9]) ).
cnf(t30802,plain,
rd(rd(X1,mult(X2,X3)),rd(Y3,mult(X2,Y3))) = ld(X2,rd(mult(X2,X1),X3)),
inference(orient,[status(thm)],[t71159]) ).
cnf(t71183,plain,
rd(etrue,mult(ld(X2,rd(X3,X3)),etrue)) = rd(rd(ld(X2,rd(mult(X2,X1),X1)),rd(X3,X3)),rd(etrue,mult(X2,etrue))),
inference(step,[status(thm)],[t71182,t30802]) ).
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(t71161,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(t71162,plain,
rd(rd(ld(X2,X3),Y3),rd(X1,mult(X2,X1))) = ld(X2,rd(X3,ld(X2,Y3))),
inference(step,[status(thm)],[t71161,t326]) ).
cnf(t31405,plain,
rd(rd(ld(X1,X2),X3),rd(Y3,mult(X1,Y3))) = ld(X1,rd(X2,ld(X1,X3))),
inference(orient,[status(thm)],[t71162]) ).
cnf(t71184,plain,
rd(etrue,mult(ld(X2,rd(X3,X3)),etrue)) = ld(X2,rd(rd(mult(X2,X1),X1),ld(X2,rd(X3,X3)))),
inference(step,[status(thm)],[t71183,t31405]) ).
cnf(t71185,plain,
rd(etrue,mult(ld(X2,rd(X3,X3)),etrue)) = ld(X2,rd(X2,ld(X2,rd(X3,X3)))),
inference(step,[status(thm)],[t71184,t9]) ).
cnf(t38783,plain,
ld(X1,rd(X1,ld(X1,rd(X2,X2)))) = rd(etrue,mult(ld(X1,rd(X2,X2)),etrue)),
inference(orient,[status(thm)],[t71185]) ).
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(t70959,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(t70960,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)],[t70959,t9]) ).
cnf(t70961,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)],[t70960,t303]) ).
cnf(t70962,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)],[t70961,t9]) ).
cnf(t70963,plain,
mult(X2,ld(X3,Y3)) = ld(ld(X2,rd(X3,X2)),mult(rd(X1,mult(X2,X1)),Y3)),
inference(step,[status(thm)],[t70962,t7]) ).
cnf(t70964,plain,
mult(X2,ld(X3,Y3)) = ld(ld(X2,rd(X3,X2)),ld(X2,Y3)),
inference(step,[status(thm)],[t70963,t326]) ).
cnf(t4871,plain,
ld(ld(X1,rd(X2,X1)),ld(X1,X3)) = mult(X1,ld(X2,X3)),
inference(orient,[status(thm)],[t70964]) ).
cnf(t4899,plain,
mult(X1,ld(mult(X2,X1),X3)) = ld(ld(X1,X2),ld(X1,X3)),
inference(cp,[status(thm)],[t4871,t9]) ).
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)],[t11,t5001]) ).
cnf(t5475,plain,
ld(X1,rd(ld(X1,X2),ld(X1,X2))) = ld(mult(X2,X1),X2),
inference(orient,[status(thm)],[t5050]) ).
cnf(t38795,plain,
rd(etrue,mult(ld(X1,rd(ld(X1,X2),ld(X1,X2))),etrue)) = ld(X1,rd(X1,ld(mult(X2,X1),X2))),
inference(cp,[status(thm)],[t38783,t5475]) ).
cnf(t71186,plain,
rd(etrue,mult(ld(mult(X2,X1),X2),etrue)) = ld(X1,rd(X1,ld(mult(X2,X1),X2))),
inference(step,[status(thm)],[t38795,t5475]) ).
cnf(t38907,plain,
ld(X1,rd(X1,ld(mult(X2,X1),X2))) = rd(etrue,mult(ld(mult(X2,X1),X2),etrue)),
inference(orient,[status(thm)],[t71186]) ).
cnf(t39006,plain,
rd(X1,ld(mult(X2,X1),X2)) = mult(X1,rd(etrue,mult(ld(mult(X2,X1),X2),etrue))),
inference(cp,[status(thm)],[t7,t38907]) ).
cnf(t69524,plain,
mult(X1,rd(etrue,mult(ld(mult(X2,X1),X2),etrue))) = rd(X1,ld(mult(X2,X1),X2)),
inference(orient,[status(thm)],[t39006]) ).
cnf(t69592,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(etrue,mult(ld(X1,mult(X1,rd(X2,X2))),etrue))),
inference(cp,[status(thm)],[t69524,t38355]) ).
cnf(t71356,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(etrue,mult(ld(X1,mult(X1,rd(X2,X2))),etrue))),
inference(step,[status(thm)],[t69592,t38355]) ).
cnf(t71357,plain,
rd(rd(rd(X1,X1),rd(X2,X2)),rd(X2,X2)) = mult(rd(rd(X1,X1),rd(X2,X2)),rd(etrue,mult(ld(X1,mult(X1,rd(X2,X2))),etrue))),
inference(step,[status(thm)],[t71356,t11]) ).
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(t70951,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(t70952,plain,
rd(rd(X1,rd(X2,X2)),rd(X2,X2)) = mult(X1,rd(X2,X2)),
inference(step,[status(thm)],[t70951,t497]) ).
cnf(t3952,plain,
rd(rd(X1,rd(X2,X2)),rd(X2,X2)) = mult(X1,rd(X2,X2)),
inference(orient,[status(thm)],[t70952]) ).
cnf(t71358,plain,
mult(rd(X1,X1),rd(X2,X2)) = mult(rd(rd(X1,X1),rd(X2,X2)),rd(etrue,mult(ld(X1,mult(X1,rd(X2,X2))),etrue))),
inference(step,[status(thm)],[t71357,t3952]) ).
cnf(t71359,plain,
mult(rd(X1,X1),rd(X2,X2)) = mult(rd(rd(X1,X1),rd(X2,X2)),rd(etrue,mult(rd(X2,X2),etrue))),
inference(step,[status(thm)],[t71358,t11]) ).
cnf(t71360,plain,
mult(rd(X1,X1),rd(X2,X2)) = mult(rd(rd(X1,X1),rd(X2,X2)),rd(X2,X2)),
inference(step,[status(thm)],[t71359,t293]) ).
cnf(t71361,plain,
mult(rd(X1,X1),rd(X2,X2)) = rd(X1,X1),
inference(step,[status(thm)],[t71360,t8]) ).
cnf(t69911,plain,
mult(rd(X1,X1),rd(X2,X2)) = rd(X1,X1),
inference(orient,[status(thm)],[t71361]) ).
cnf(t70044,plain,
ld(mult(rd(X1,X1),rd(X2,X2)),X2) = mult(rd(X2,X2),ld(rd(X2,X2),X2)),
inference(cp,[status(thm)],[t48029,t69911]) ).
cnf(t71364,plain,
ld(rd(X1,X1),X2) = mult(rd(X2,X2),ld(rd(X2,X2),X2)),
inference(step,[status(thm)],[t70044,t69911]) ).
cnf(t71365,plain,
mult(rd(X1,X1),X2) = mult(rd(X2,X2),ld(rd(X2,X2),X2)),
inference(step,[status(thm)],[t71364,t303]) ).
cnf(t71366,plain,
mult(rd(X1,X1),X2) = X2,
inference(step,[status(thm)],[t71365,t7]) ).
cnf(t70119,plain,
mult(rd(X1,X1),X2) = X2,
inference(orient,[status(thm)],[t71366]) ).
cnf(t70183,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)],[t54145,t70119]) ).
cnf(t71430,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)],[t70183,t375]) ).
cnf(t71431,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)],[t71430,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(t71001,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(t71002,plain,
mult(rd(X2,X1),rd(X3,rd(X1,X2))) = mult(mult(rd(X2,X1),X3),rd(X2,X1)),
inference(step,[status(thm)],[t71001,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(t71003,plain,
mult(rd(X2,X1),rd(X3,rd(X1,X2))) = rd(mult(rd(X2,X1),mult(X3,X2)),X1),
inference(step,[status(thm)],[t71002,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)],[t71003]) ).
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(t71012,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(t71013,plain,
rd(mult(rd(X1,X2),mult(X3,X1)),X2) = rd(X1,mult(rd(X2,X1),ld(X3,X2))),
inference(step,[status(thm)],[t71012,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)],[t71013]) ).
cnf(t71016,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)],[t71016]) ).
cnf(t71432,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)],[t71431,t10104]) ).
cnf(t71433,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)],[t71432,t70119]) ).
cnf(t71434,plain,
X2 = rd(mult(rd(X1,X1),mult(X2,rd(X1,X1))),mult(rd(X1,X1),rd(X1,X1))),
inference(step,[status(thm)],[t71433,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(t71043,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,t9]) ).
cnf(t71044,plain,
rd(mult(rd(X1,X2),X3),rd(X1,X2)) = mult(rd(X1,X2),mult(X3,rd(X2,X1))),
inference(step,[status(thm)],[t71043,t9]) ).
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)],[t71044]) ).
cnf(t71435,plain,
X2 = rd(rd(mult(rd(X1,X1),X2),rd(X1,X1)),mult(rd(X1,X1),rd(X1,X1))),
inference(step,[status(thm)],[t71434,t12191]) ).
cnf(t71436,plain,
X2 = rd(rd(X2,rd(X1,X1)),mult(rd(X1,X1),rd(X1,X1))),
inference(step,[status(thm)],[t71435,t70119]) ).
cnf(t71437,plain,
X2 = rd(rd(X2,rd(X1,X1)),rd(rd(X1,X1),rd(X1,X1))),
inference(step,[status(thm)],[t71436,t375]) ).
cnf(t71438,plain,
X2 = rd(rd(X2,rd(X1,X1)),rd(X1,X1)),
inference(step,[status(thm)],[t71437,t497]) ).
cnf(t71439,plain,
X2 = mult(X2,rd(X1,X1)),
inference(step,[status(thm)],[t71438,t3952]) ).
cnf(t70622,plain,
mult(X1,rd(X2,X2)) = X1,
inference(orient,[status(thm)],[t71439]) ).
cnf(t70723,plain,
efalse = eq(tuple(mult(rd(X1,X1),x1(rd(X1,X1))),x1_2(rd(X1,X1))),tuple(x1(rd(X1,X1)),x1_2(rd(X1,X1)))),
inference(cp,[status(thm)],[t22,t70622]) ).
cnf(t71458,plain,
efalse = eq(tuple(x1(rd(X1,X1)),x1_2(rd(X1,X1))),tuple(x1(rd(X1,X1)),x1_2(rd(X1,X1)))),
inference(step,[status(thm)],[t70723,t70119]) ).
cnf(t0,plain,
eq(X1,X1) = etrue,
introduced(definition) ).
cnf(t21,plain,
eq(X1,X1) = etrue,
inference(orient,[status(thm)],[t0]) ).
cnf(t71459,plain,
efalse = etrue,
inference(step,[status(thm)],[t71458,t21]) ).
cnf(t70872,plain,
efalse = etrue,
inference(orient,[status(thm)],[t71459]) ).
cnf(goal_0,negated_conjecture,
etrue != efalse,
introduced(definition) ).
cnf(g0_0,plain,
etrue != etrue,
inference(rw,[status(thm)],[goal_0,t70872]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP654-10 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/0.37 % Computer : n004.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Wed Sep 23 15:29:35 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 47.47/6.46 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 47.47/6.46 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------