%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP688-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 : n014.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:03 PM UTC 2026
% Result : Unsatisfiable 24.32s 3.60s
% Output : CNFRefutation 24.32s
% Verified :
% SZS Type : Refutation
% Derivation depth : 151
% Number of leaves : 12
% Syntax : Number of clauses : 581 ( 581 unt; 0 nHn; 183 RR)
% Number of literals : 581 ( 580 equ; 2 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 : 7 ( 7 usr; 3 con; 0-2 aty)
% Number of variables : 731 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t2,axiom,
ld(X1,mult(X1,X2)) = X2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t28,plain,
ld(X1,mult(X1,X2)) = X2,
inference(orient,[status(thm)],[t2]) ).
cnf(t10,axiom,
mult(mult(X1,mult(X2,X1)),X3) = mult(X1,mult(X2,mult(X1,X3))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t33,plain,
mult(mult(X1,mult(X2,X1)),X3) = mult(X1,mult(X2,mult(X1,X3))),
inference(orient,[status(thm)],[t10]) ).
cnf(t5,axiom,
mult(rd(X1,X2),X2) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t20,plain,
mult(rd(X1,X2),X2) = X1,
inference(orient,[status(thm)],[t5]) ).
cnf(t36,plain,
mult(X1,mult(rd(X2,X1),mult(X1,X3))) = mult(mult(X1,X2),X3),
inference(cp,[status(thm)],[t33,t20]) ).
cnf(t3098,plain,
mult(X1,mult(rd(X2,X1),mult(X1,X3))) = mult(mult(X1,X2),X3),
inference(orient,[status(thm)],[t36]) ).
cnf(t3201,plain,
mult(rd(X1,X2),mult(X2,X3)) = ld(X2,mult(mult(X2,X1),X3)),
inference(cp,[status(thm)],[t28,t3098]) ).
cnf(t4776,plain,
ld(X1,mult(mult(X1,X2),X3)) = mult(rd(X2,X1),mult(X1,X3)),
inference(orient,[status(thm)],[t3201]) ).
cnf(t3,axiom,
mult(X1,ld(X1,X2)) = X2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t11,plain,
mult(X1,ld(X1,X2)) = X2,
inference(orient,[status(thm)],[t3]) ).
cnf(t4807,plain,
mult(rd(ld(X1,X2),X1),mult(X1,X3)) = ld(X1,mult(X2,X3)),
inference(cp,[status(thm)],[t4776,t11]) ).
cnf(t16550,plain,
mult(rd(ld(X1,X2),X1),mult(X1,X3)) = ld(X1,mult(X2,X3)),
inference(orient,[status(thm)],[t4807]) ).
cnf(t6,axiom,
rd(mult(X1,X2),X2) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t23,plain,
rd(mult(X1,X2),X2) = X1,
inference(orient,[status(thm)],[t6]) ).
cnf(t24,plain,
X1 = rd(X2,ld(X1,X2)),
inference(cp,[status(thm)],[t23,t11]) ).
cnf(t107,plain,
rd(X1,ld(X2,X1)) = X2,
inference(orient,[status(thm)],[t24]) ).
cnf(t7,axiom,
mult(i(X1),mult(X1,X2)) = X2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t15,plain,
mult(i(X1),mult(X1,X2)) = X2,
inference(orient,[status(thm)],[t7]) ).
cnf(t16,plain,
ld(X1,X2) = mult(i(X1),X2),
inference(cp,[status(thm)],[t15,t11]) ).
cnf(t98,plain,
mult(i(X1),X2) = ld(X1,X2),
inference(orient,[status(thm)],[t16]) ).
cnf(t0,axiom,
mult(X1,unit) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t12,plain,
mult(X1,unit) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t17,plain,
unit = mult(i(X1),X1),
inference(cp,[status(thm)],[t15,t12]) ).
cnf(t73,plain,
mult(i(X1),X1) = unit,
inference(orient,[status(thm)],[t17]) ).
cnf(t79,plain,
X1 = mult(i(i(X1)),unit),
inference(cp,[status(thm)],[t15,t73]) ).
cnf(t19344,plain,
X1 = i(i(X1)),
inference(step,[status(thm)],[t79,t12]) ).
cnf(t81,plain,
i(i(X1)) = X1,
inference(orient,[status(thm)],[t19344]) ).
cnf(t100,plain,
ld(i(X1),X2) = mult(X1,X2),
inference(cp,[status(thm)],[t98,t81]) ).
cnf(t106,plain,
ld(i(X1),X2) = mult(X1,X2),
inference(orient,[status(thm)],[t100]) ).
cnf(t108,plain,
i(X1) = rd(X2,mult(X1,X2)),
inference(cp,[status(thm)],[t107,t106]) ).
cnf(t135,plain,
rd(X1,mult(X2,X1)) = i(X2),
inference(orient,[status(thm)],[t108]) ).
cnf(t8,axiom,
mult(op_c,mult(op_c,mult(op_c,op_c))) = unit,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t44,plain,
mult(op_c,mult(op_c,mult(op_c,op_c))) = unit,
inference(orient,[status(thm)],[t8]) ).
cnf(t136,plain,
i(op_c) = rd(mult(op_c,mult(op_c,op_c)),unit),
inference(cp,[status(thm)],[t135,t44]) ).
cnf(t21,plain,
X1 = rd(X1,unit),
inference(cp,[status(thm)],[t20,t12]) ).
cnf(t60,plain,
rd(X1,unit) = X1,
inference(orient,[status(thm)],[t21]) ).
cnf(t19347,plain,
i(op_c) = mult(op_c,mult(op_c,op_c)),
inference(step,[status(thm)],[t136,t60]) ).
cnf(t138,plain,
mult(op_c,mult(op_c,op_c)) = i(op_c),
inference(orient,[status(thm)],[t19347]) ).
cnf(t16710,plain,
ld(op_c,mult(X1,mult(op_c,op_c))) = mult(rd(ld(op_c,X1),op_c),i(op_c)),
inference(cp,[status(thm)],[t16550,t138]) ).
cnf(t16782,plain,
mult(rd(ld(op_c,X1),op_c),i(op_c)) = ld(op_c,mult(X1,mult(op_c,op_c))),
inference(orient,[status(thm)],[t16710]) ).
cnf(t35,plain,
mult(ld(X1,X2),mult(X1,mult(ld(X1,X2),X3))) = mult(mult(ld(X1,X2),X2),X3),
inference(cp,[status(thm)],[t33,t11]) ).
cnf(t1072,plain,
mult(ld(X1,X2),mult(X1,mult(ld(X1,X2),X3))) = mult(mult(ld(X1,X2),X2),X3),
inference(orient,[status(thm)],[t35]) ).
cnf(t82,plain,
unit = mult(X1,i(X1)),
inference(cp,[status(thm)],[t73,t81]) ).
cnf(t96,plain,
mult(X1,i(X1)) = unit,
inference(orient,[status(thm)],[t82]) ).
cnf(t3158,plain,
mult(mult(X1,X2),i(X1)) = mult(X1,mult(rd(X2,X1),unit)),
inference(cp,[status(thm)],[t3098,t96]) ).
cnf(t19413,plain,
mult(mult(X1,X2),i(X1)) = mult(X1,rd(X2,X1)),
inference(step,[status(thm)],[t3158,t12]) ).
cnf(t3217,plain,
mult(mult(X1,X2),i(X1)) = mult(X1,rd(X2,X1)),
inference(orient,[status(thm)],[t19413]) ).
cnf(t3249,plain,
mult(i(X1),rd(X2,i(X1))) = mult(ld(X1,X2),i(i(X1))),
inference(cp,[status(thm)],[t3217,t98]) ).
cnf(t19417,plain,
ld(X1,rd(X2,i(X1))) = mult(ld(X1,X2),i(i(X1))),
inference(step,[status(thm)],[t3249,t98]) ).
cnf(t19418,plain,
ld(X1,rd(X2,i(X1))) = mult(ld(X1,X2),X1),
inference(step,[status(thm)],[t19417,t81]) ).
cnf(t3381,plain,
ld(X1,rd(X2,i(X1))) = mult(ld(X1,X2),X1),
inference(orient,[status(thm)],[t19418]) ).
cnf(t3407,plain,
rd(X1,i(X2)) = mult(X2,mult(ld(X2,X1),X2)),
inference(cp,[status(thm)],[t11,t3381]) ).
cnf(t4191,plain,
mult(X1,mult(ld(X1,X2),X1)) = rd(X2,i(X1)),
inference(orient,[status(thm)],[t3407]) ).
cnf(t4243,plain,
mult(mult(ld(X1,X2),X2),X1) = mult(ld(X1,X2),rd(X2,i(X1))),
inference(cp,[status(thm)],[t1072,t4191]) ).
cnf(t8825,plain,
mult(ld(X1,X2),rd(X2,i(X1))) = mult(mult(ld(X1,X2),X2),X1),
inference(orient,[status(thm)],[t4243]) ).
cnf(t8862,plain,
mult(mult(ld(i(X1),X2),X2),i(X1)) = mult(mult(X1,X2),rd(X2,i(i(X1)))),
inference(cp,[status(thm)],[t8825,t106]) ).
cnf(t19540,plain,
mult(mult(mult(X1,X2),X2),i(X1)) = mult(mult(X1,X2),rd(X2,i(i(X1)))),
inference(step,[status(thm)],[t8862,t106]) ).
cnf(t19541,plain,
mult(mult(mult(X1,X2),X2),i(X1)) = mult(mult(X1,X2),rd(X2,X1)),
inference(step,[status(thm)],[t19540,t81]) ).
cnf(t9,axiom,
mult(i(X1),i(X2)) = i(mult(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t49,plain,
mult(i(X1),i(X2)) = i(mult(X1,X2)),
inference(orient,[status(thm)],[t9]) ).
cnf(t19345,plain,
ld(X1,i(X2)) = i(mult(X1,X2)),
inference(step,[status(thm)],[t49,t98]) ).
cnf(t105,plain,
ld(X1,i(X2)) = i(mult(X1,X2)),
inference(rw,[status(thm)],[t19345]) ).
cnf(t110,plain,
i(mult(X1,X2)) = ld(X1,i(X2)),
inference(orient,[status(thm)],[t105]) ).
cnf(t117,plain,
ld(mult(X1,X2),X3) = mult(ld(X1,i(X2)),X3),
inference(cp,[status(thm)],[t98,t110]) ).
cnf(t293,plain,
mult(ld(X1,i(X2)),X3) = ld(mult(X1,X2),X3),
inference(orient,[status(thm)],[t117]) ).
cnf(t8829,plain,
mult(mult(ld(X1,i(X2)),i(X2)),X1) = ld(mult(X1,X2),rd(i(X2),i(X1))),
inference(cp,[status(thm)],[t8825,t293]) ).
cnf(t112,plain,
ld(i(X1),i(X2)) = i(ld(X1,X2)),
inference(cp,[status(thm)],[t110,t98]) ).
cnf(t19346,plain,
mult(X1,i(X2)) = i(ld(X1,X2)),
inference(step,[status(thm)],[t112,t106]) ).
cnf(t120,plain,
i(ld(X1,X2)) = mult(X1,i(X2)),
inference(orient,[status(thm)],[t19346]) ).
cnf(t123,plain,
ld(ld(X1,X2),X3) = mult(mult(X1,i(X2)),X3),
inference(cp,[status(thm)],[t98,t120]) ).
cnf(t322,plain,
mult(mult(X1,i(X2)),X3) = ld(ld(X1,X2),X3),
inference(orient,[status(thm)],[t123]) ).
cnf(t19515,plain,
ld(ld(ld(X1,i(X2)),X2),X1) = ld(mult(X1,X2),rd(i(X2),i(X1))),
inference(step,[status(thm)],[t8829,t322]) ).
cnf(t116,plain,
mult(mult(X1,X2),X3) = ld(ld(X1,i(X2)),X3),
inference(cp,[status(thm)],[t106,t110]) ).
cnf(t273,plain,
ld(ld(X1,i(X2)),X3) = mult(mult(X1,X2),X3),
inference(orient,[status(thm)],[t116]) ).
cnf(t19516,plain,
ld(mult(mult(X1,X2),X2),X1) = ld(mult(X1,X2),rd(i(X2),i(X1))),
inference(step,[status(thm)],[t19515,t273]) ).
cnf(t102,plain,
i(X1) = rd(ld(X1,X2),X2),
inference(cp,[status(thm)],[t23,t98]) ).
cnf(t125,plain,
rd(ld(X1,X2),X2) = i(X1),
inference(orient,[status(thm)],[t102]) ).
cnf(t115,plain,
ld(rd(X1,X2),i(X2)) = i(X1),
inference(cp,[status(thm)],[t110,t20]) ).
cnf(t150,plain,
ld(rd(X1,X2),i(X2)) = i(X1),
inference(orient,[status(thm)],[t115]) ).
cnf(t156,plain,
i(rd(X1,X2)) = rd(i(X1),i(X2)),
inference(cp,[status(thm)],[t125,t150]) ).
cnf(t30,plain,
X1 = ld(rd(X2,X1),X2),
inference(cp,[status(thm)],[t28,t20]) ).
cnf(t109,plain,
ld(rd(X1,X2),X1) = X2,
inference(orient,[status(thm)],[t30]) ).
cnf(t127,plain,
i(rd(X1,X2)) = rd(X2,X1),
inference(cp,[status(thm)],[t125,t109]) ).
cnf(t130,plain,
i(rd(X1,X2)) = rd(X2,X1),
inference(orient,[status(thm)],[t127]) ).
cnf(t19348,plain,
rd(X2,X1) = rd(i(X1),i(X2)),
inference(step,[status(thm)],[t156,t130]) ).
cnf(t158,plain,
rd(i(X1),i(X2)) = rd(X2,X1),
inference(orient,[status(thm)],[t19348]) ).
cnf(t19517,plain,
ld(mult(mult(X1,X2),X2),X1) = ld(mult(X1,X2),rd(X1,X2)),
inference(step,[status(thm)],[t19516,t158]) ).
cnf(t8920,plain,
ld(mult(mult(X1,X2),X2),X1) = ld(mult(X1,X2),rd(X1,X2)),
inference(orient,[status(thm)],[t19517]) ).
cnf(t121,plain,
mult(rd(X1,X2),i(X1)) = i(X2),
inference(cp,[status(thm)],[t120,t109]) ).
cnf(t168,plain,
mult(rd(X1,X2),i(X1)) = i(X2),
inference(orient,[status(thm)],[t121]) ).
cnf(t8998,plain,
ld(mult(rd(X1,X2),i(X1)),rd(rd(X1,X2),i(X1))) = ld(mult(i(X2),i(X1)),rd(X1,X2)),
inference(cp,[status(thm)],[t8920,t168]) ).
cnf(t122,plain,
mult(ld(X1,X2),X3) = ld(mult(X1,i(X2)),X3),
inference(cp,[status(thm)],[t106,t120]) ).
cnf(t310,plain,
ld(mult(X1,i(X2)),X3) = mult(ld(X1,X2),X3),
inference(orient,[status(thm)],[t122]) ).
cnf(t19521,plain,
mult(ld(rd(X1,X2),X1),rd(rd(X1,X2),i(X1))) = ld(mult(i(X2),i(X1)),rd(X1,X2)),
inference(step,[status(thm)],[t8998,t310]) ).
cnf(t132,plain,
mult(rd(X1,X2),X3) = ld(rd(X2,X1),X3),
inference(cp,[status(thm)],[t106,t130]) ).
cnf(t210,plain,
ld(rd(X1,X2),X3) = mult(rd(X2,X1),X3),
inference(orient,[status(thm)],[t132]) ).
cnf(t19522,plain,
mult(mult(rd(X2,X1),X1),rd(rd(X1,X2),i(X1))) = ld(mult(i(X2),i(X1)),rd(X1,X2)),
inference(step,[status(thm)],[t19521,t210]) ).
cnf(t19523,plain,
mult(X2,rd(rd(X1,X2),i(X1))) = ld(mult(i(X2),i(X1)),rd(X1,X2)),
inference(step,[status(thm)],[t19522,t20]) ).
cnf(t159,plain,
rd(X1,rd(X2,X3)) = rd(rd(X3,X2),i(X1)),
inference(cp,[status(thm)],[t158,t130]) ).
cnf(t352,plain,
rd(rd(X1,X2),i(X3)) = rd(X3,rd(X2,X1)),
inference(orient,[status(thm)],[t159]) ).
cnf(t19524,plain,
mult(X2,rd(X1,rd(X2,X1))) = ld(mult(i(X2),i(X1)),rd(X1,X2)),
inference(step,[status(thm)],[t19523,t352]) ).
cnf(t19525,plain,
mult(X2,rd(X1,rd(X2,X1))) = mult(ld(i(X2),X1),rd(X1,X2)),
inference(step,[status(thm)],[t19524,t310]) ).
cnf(t19526,plain,
mult(X2,rd(X1,rd(X2,X1))) = mult(mult(X2,X1),rd(X1,X2)),
inference(step,[status(thm)],[t19525,t106]) ).
cnf(t9261,plain,
mult(mult(X1,X2),rd(X2,X1)) = mult(X1,rd(X2,rd(X1,X2))),
inference(orient,[status(thm)],[t19526]) ).
cnf(t19542,plain,
mult(mult(mult(X1,X2),X2),i(X1)) = mult(X1,rd(X2,rd(X1,X2))),
inference(step,[status(thm)],[t19541,t9261]) ).
cnf(t10721,plain,
mult(mult(mult(X1,X2),X2),i(X1)) = mult(X1,rd(X2,rd(X1,X2))),
inference(orient,[status(thm)],[t19542]) ).
cnf(t1,axiom,
mult(unit,X1) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t13,plain,
mult(unit,X1) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t38,plain,
mult(X1,mult(unit,mult(X1,X2))) = mult(mult(X1,X1),X2),
inference(cp,[status(thm)],[t33,t13]) ).
cnf(t19349,plain,
mult(X1,mult(X1,X2)) = mult(mult(X1,X1),X2),
inference(step,[status(thm)],[t38,t13]) ).
cnf(t188,plain,
mult(mult(X1,X1),X2) = mult(X1,mult(X1,X2)),
inference(orient,[status(thm)],[t19349]) ).
cnf(t197,plain,
mult(X1,X1) = rd(mult(X1,mult(X1,X2)),X2),
inference(cp,[status(thm)],[t23,t188]) ).
cnf(t389,plain,
rd(mult(X1,mult(X1,X2)),X2) = mult(X1,X1),
inference(orient,[status(thm)],[t197]) ).
cnf(t400,plain,
mult(X1,X1) = rd(mult(X1,unit),i(X1)),
inference(cp,[status(thm)],[t389,t96]) ).
cnf(t162,plain,
rd(X1,i(X2)) = rd(X2,i(X1)),
inference(cp,[status(thm)],[t158,t81]) ).
cnf(t256,plain,
rd(X1,i(X2)) = rd(X2,i(X1)),
inference(orient,[status(thm)],[t162]) ).
cnf(t19357,plain,
mult(X1,X1) = rd(X1,i(mult(X1,unit))),
inference(step,[status(thm)],[t400,t256]) ).
cnf(t19358,plain,
mult(X1,X1) = rd(X1,ld(X1,i(unit))),
inference(step,[status(thm)],[t19357,t110]) ).
cnf(t74,plain,
unit = i(mult(i(X1),X1)),
inference(cp,[status(thm)],[t73,t49]) ).
cnf(t19343,plain,
unit = i(unit),
inference(step,[status(thm)],[t74,t73]) ).
cnf(t80,plain,
i(unit) = unit,
inference(orient,[status(thm)],[t19343]) ).
cnf(t19359,plain,
mult(X1,X1) = rd(X1,ld(X1,unit)),
inference(step,[status(thm)],[t19358,t80]) ).
cnf(t77,plain,
X1 = ld(i(X1),unit),
inference(cp,[status(thm)],[t28,t73]) ).
cnf(t92,plain,
ld(i(X1),unit) = X1,
inference(orient,[status(thm)],[t77]) ).
cnf(t93,plain,
i(X1) = ld(X1,unit),
inference(cp,[status(thm)],[t92,t81]) ).
cnf(t94,plain,
ld(X1,unit) = i(X1),
inference(orient,[status(thm)],[t93]) ).
cnf(t19360,plain,
mult(X1,X1) = rd(X1,i(X1)),
inference(step,[status(thm)],[t19359,t94]) ).
cnf(t425,plain,
rd(X1,i(X1)) = mult(X1,X1),
inference(orient,[status(thm)],[t19360]) ).
cnf(t430,plain,
mult(mult(X1,X2),mult(X1,X2)) = rd(mult(X1,X2),ld(X1,i(X2))),
inference(cp,[status(thm)],[t425,t110]) ).
cnf(t2359,plain,
rd(mult(X1,X2),ld(X1,i(X2))) = mult(mult(X1,X2),mult(X1,X2)),
inference(orient,[status(thm)],[t430]) ).
cnf(t40,plain,
mult(X1,mult(X2,X1)) = rd(mult(X1,mult(X2,mult(X1,X3))),X3),
inference(cp,[status(thm)],[t23,t33]) ).
cnf(t6188,plain,
rd(mult(X1,mult(X2,mult(X1,X3))),X3) = mult(X1,mult(X2,X1)),
inference(orient,[status(thm)],[t40]) ).
cnf(t170,plain,
i(X1) = mult(rd(ld(X2,X3),X1),mult(X2,i(X3))),
inference(cp,[status(thm)],[t168,t120]) ).
cnf(t1211,plain,
mult(rd(ld(X1,X2),X3),mult(X1,i(X2))) = i(X3),
inference(orient,[status(thm)],[t170]) ).
cnf(t6213,plain,
mult(X1,mult(rd(ld(X1,X2),X3),X1)) = rd(mult(X1,i(X3)),i(X2)),
inference(cp,[status(thm)],[t6188,t1211]) ).
cnf(t3269,plain,
mult(X1,X2) = rd(mult(X1,rd(X2,X1)),i(X1)),
inference(cp,[status(thm)],[t23,t3217]) ).
cnf(t160,plain,
rd(X1,ld(X2,X3)) = rd(mult(X2,i(X3)),i(X1)),
inference(cp,[status(thm)],[t158,t120]) ).
cnf(t631,plain,
rd(mult(X1,i(X2)),i(X3)) = rd(X3,ld(X1,X2)),
inference(orient,[status(thm)],[t160]) ).
cnf(t640,plain,
rd(X1,ld(X2,rd(X3,Y3))) = rd(mult(X2,rd(Y3,X3)),i(X1)),
inference(cp,[status(thm)],[t631,t130]) ).
cnf(t2501,plain,
rd(mult(X1,rd(X2,X3)),i(Y3)) = rd(Y3,ld(X1,rd(X3,X2))),
inference(orient,[status(thm)],[t640]) ).
cnf(t19419,plain,
mult(X1,X2) = rd(X1,ld(X1,rd(X1,X2))),
inference(step,[status(thm)],[t3269,t2501]) ).
cnf(t3482,plain,
rd(X1,ld(X1,rd(X1,X2))) = mult(X1,X2),
inference(orient,[status(thm)],[t19419]) ).
cnf(t3499,plain,
mult(X1,ld(X2,X1)) = rd(X1,ld(X1,X2)),
inference(cp,[status(thm)],[t3482,t107]) ).
cnf(t3578,plain,
mult(X1,ld(X2,X1)) = rd(X1,ld(X1,X2)),
inference(orient,[status(thm)],[t3499]) ).
cnf(t3607,plain,
rd(X1,ld(X1,rd(X2,X3))) = mult(X1,mult(rd(X3,X2),X1)),
inference(cp,[status(thm)],[t3578,t210]) ).
cnf(t5177,plain,
mult(X1,mult(rd(X2,X3),X1)) = rd(X1,ld(X1,rd(X3,X2))),
inference(orient,[status(thm)],[t3607]) ).
cnf(t19826,plain,
rd(X1,ld(X1,rd(X3,ld(X1,X2)))) = rd(mult(X1,i(X3)),i(X2)),
inference(step,[status(thm)],[t6213,t5177]) ).
cnf(t19827,plain,
rd(X1,ld(X1,rd(X3,ld(X1,X2)))) = rd(X2,ld(X1,X3)),
inference(step,[status(thm)],[t19826,t631]) ).
cnf(t18109,plain,
rd(X1,ld(X1,rd(X2,ld(X1,X3)))) = rd(X3,ld(X1,X2)),
inference(orient,[status(thm)],[t19827]) ).
cnf(t18162,plain,
rd(mult(X1,X2),ld(X1,X3)) = rd(X1,ld(X1,rd(X3,X2))),
inference(cp,[status(thm)],[t18109,t28]) ).
cnf(t18290,plain,
rd(mult(X1,X2),ld(X1,X3)) = rd(X1,ld(X1,rd(X3,X2))),
inference(orient,[status(thm)],[t18162]) ).
cnf(t19828,plain,
rd(X1,ld(X1,rd(i(X2),X2))) = mult(mult(X1,X2),mult(X1,X2)),
inference(step,[status(thm)],[t2359,t18290]) ).
cnf(t194,plain,
i(mult(X1,X1)) = rd(X2,mult(X1,mult(X1,X2))),
inference(cp,[status(thm)],[t135,t188]) ).
cnf(t19366,plain,
ld(X1,i(X1)) = rd(X2,mult(X1,mult(X1,X2))),
inference(step,[status(thm)],[t194,t110]) ).
cnf(t427,plain,
mult(i(X1),i(X1)) = rd(i(X1),X1),
inference(cp,[status(thm)],[t425,t158]) ).
cnf(t19361,plain,
ld(X1,i(X1)) = rd(i(X1),X1),
inference(step,[status(thm)],[t427,t98]) ).
cnf(t438,plain,
ld(X1,i(X1)) = rd(i(X1),X1),
inference(orient,[status(thm)],[t19361]) ).
cnf(t19367,plain,
rd(i(X1),X1) = rd(X2,mult(X1,mult(X1,X2))),
inference(step,[status(thm)],[t19366,t438]) ).
cnf(t585,plain,
rd(X1,mult(X2,mult(X2,X1))) = rd(i(X2),X2),
inference(orient,[status(thm)],[t19367]) ).
cnf(t3498,plain,
mult(X1,mult(X2,mult(X2,X1))) = rd(X1,ld(X1,rd(i(X2),X2))),
inference(cp,[status(thm)],[t3482,t585]) ).
cnf(t8278,plain,
rd(X1,ld(X1,rd(i(X2),X2))) = mult(X1,mult(X2,mult(X2,X1))),
inference(orient,[status(thm)],[t3498]) ).
cnf(t19829,plain,
mult(X1,mult(X2,mult(X2,X1))) = mult(mult(X1,X2),mult(X1,X2)),
inference(step,[status(thm)],[t19828,t8278]) ).
cnf(t18526,plain,
mult(X1,mult(X2,mult(X2,X1))) = mult(mult(X1,X2),mult(X1,X2)),
inference(rw,[status(thm)],[t19829]) ).
cnf(t18885,plain,
mult(mult(X1,X2),mult(X1,X2)) = mult(X1,mult(X2,mult(X2,X1))),
inference(orient,[status(thm)],[t18526]) ).
cnf(t3183,plain,
mult(mult(op_c,X1),mult(op_c,op_c)) = mult(op_c,mult(rd(X1,op_c),i(op_c))),
inference(cp,[status(thm)],[t3098,t138]) ).
cnf(t7740,plain,
mult(op_c,mult(rd(X1,op_c),i(op_c))) = mult(mult(op_c,X1),mult(op_c,op_c)),
inference(orient,[status(thm)],[t3183]) ).
cnf(t7756,plain,
ld(op_c,i(mult(rd(X1,op_c),i(op_c)))) = i(mult(mult(op_c,X1),mult(op_c,op_c))),
inference(cp,[status(thm)],[t110,t7740]) ).
cnf(t19496,plain,
ld(op_c,ld(rd(X1,op_c),i(i(op_c)))) = i(mult(mult(op_c,X1),mult(op_c,op_c))),
inference(step,[status(thm)],[t7756,t110]) ).
cnf(t19497,plain,
ld(op_c,mult(rd(op_c,X1),i(i(op_c)))) = i(mult(mult(op_c,X1),mult(op_c,op_c))),
inference(step,[status(thm)],[t19496,t210]) ).
cnf(t19498,plain,
ld(op_c,mult(rd(op_c,X1),op_c)) = i(mult(mult(op_c,X1),mult(op_c,op_c))),
inference(step,[status(thm)],[t19497,t81]) ).
cnf(t19499,plain,
ld(op_c,mult(rd(op_c,X1),op_c)) = ld(mult(op_c,X1),i(mult(op_c,op_c))),
inference(step,[status(thm)],[t19498,t110]) ).
cnf(t19500,plain,
ld(op_c,mult(rd(op_c,X1),op_c)) = ld(mult(op_c,X1),ld(op_c,i(op_c))),
inference(step,[status(thm)],[t19499,t110]) ).
cnf(t141,plain,
mult(op_c,op_c) = ld(op_c,i(op_c)),
inference(cp,[status(thm)],[t28,t138]) ).
cnf(t145,plain,
ld(op_c,i(op_c)) = mult(op_c,op_c),
inference(orient,[status(thm)],[t141]) ).
cnf(t19501,plain,
ld(op_c,mult(rd(op_c,X1),op_c)) = ld(mult(op_c,X1),mult(op_c,op_c)),
inference(step,[status(thm)],[t19500,t145]) ).
cnf(t7777,plain,
ld(mult(op_c,X1),mult(op_c,op_c)) = ld(op_c,mult(rd(op_c,X1),op_c)),
inference(orient,[status(thm)],[t19501]) ).
cnf(t7794,plain,
rd(mult(op_c,op_c),ld(mult(op_c,op_c),mult(op_c,X1))) = mult(mult(op_c,op_c),ld(op_c,mult(rd(op_c,X1),op_c))),
inference(cp,[status(thm)],[t3578,t7777]) ).
cnf(t323,plain,
ld(ld(i(X1),X1),X2) = mult(i(X1),mult(i(X1),X2)),
inference(cp,[status(thm)],[t322,t188]) ).
cnf(t19352,plain,
ld(mult(X1,X1),X2) = mult(i(X1),mult(i(X1),X2)),
inference(step,[status(thm)],[t323,t106]) ).
cnf(t19353,plain,
ld(mult(X1,X1),X2) = ld(X1,mult(i(X1),X2)),
inference(step,[status(thm)],[t19352,t98]) ).
cnf(t19354,plain,
ld(mult(X1,X1),X2) = ld(X1,ld(X1,X2)),
inference(step,[status(thm)],[t19353,t98]) ).
cnf(t337,plain,
ld(mult(X1,X1),X2) = ld(X1,ld(X1,X2)),
inference(orient,[status(thm)],[t19354]) ).
cnf(t19502,plain,
rd(mult(op_c,op_c),ld(op_c,ld(op_c,mult(op_c,X1)))) = mult(mult(op_c,op_c),ld(op_c,mult(rd(op_c,X1),op_c))),
inference(step,[status(thm)],[t7794,t337]) ).
cnf(t277,plain,
mult(mult(op_c,op_c),X1) = ld(mult(op_c,op_c),X1),
inference(cp,[status(thm)],[t273,t145]) ).
cnf(t19351,plain,
mult(op_c,mult(op_c,X1)) = ld(mult(op_c,op_c),X1),
inference(step,[status(thm)],[t277,t188]) ).
cnf(t286,plain,
ld(mult(op_c,op_c),X1) = mult(op_c,mult(op_c,X1)),
inference(orient,[status(thm)],[t19351]) ).
cnf(t19355,plain,
ld(op_c,ld(op_c,X1)) = mult(op_c,mult(op_c,X1)),
inference(step,[status(thm)],[t286,t337]) ).
cnf(t346,plain,
ld(op_c,ld(op_c,X1)) = mult(op_c,mult(op_c,X1)),
inference(rw,[status(thm)],[t19355]) ).
cnf(t347,plain,
ld(op_c,ld(op_c,X1)) = mult(op_c,mult(op_c,X1)),
inference(orient,[status(thm)],[t346]) ).
cnf(t19503,plain,
rd(mult(op_c,op_c),mult(op_c,mult(op_c,mult(op_c,X1)))) = mult(mult(op_c,op_c),ld(op_c,mult(rd(op_c,X1),op_c))),
inference(step,[status(thm)],[t19502,t347]) ).
cnf(t143,plain,
mult(op_c,mult(op_c,mult(op_c,X1))) = mult(i(op_c),X1),
inference(cp,[status(thm)],[t33,t138]) ).
cnf(t19356,plain,
mult(op_c,mult(op_c,mult(op_c,X1))) = ld(op_c,X1),
inference(step,[status(thm)],[t143,t98]) ).
cnf(t383,plain,
mult(op_c,mult(op_c,mult(op_c,X1))) = ld(op_c,X1),
inference(orient,[status(thm)],[t19356]) ).
cnf(t19504,plain,
rd(mult(op_c,op_c),ld(op_c,X1)) = mult(mult(op_c,op_c),ld(op_c,mult(rd(op_c,X1),op_c))),
inference(step,[status(thm)],[t19503,t383]) ).
cnf(t3159,plain,
mult(mult(X1,X2),ld(X1,X3)) = mult(X1,mult(rd(X2,X1),X3)),
inference(cp,[status(thm)],[t3098,t11]) ).
cnf(t4679,plain,
mult(mult(X1,X2),ld(X1,X3)) = mult(X1,mult(rd(X2,X1),X3)),
inference(orient,[status(thm)],[t3159]) ).
cnf(t19505,plain,
rd(mult(op_c,op_c),ld(op_c,X1)) = mult(op_c,mult(rd(op_c,op_c),mult(rd(op_c,X1),op_c))),
inference(step,[status(thm)],[t19504,t4679]) ).
cnf(t27,plain,
unit = rd(X1,X1),
inference(cp,[status(thm)],[t23,t13]) ).
cnf(t61,plain,
rd(X1,X1) = unit,
inference(orient,[status(thm)],[t27]) ).
cnf(t19506,plain,
rd(mult(op_c,op_c),ld(op_c,X1)) = mult(op_c,mult(unit,mult(rd(op_c,X1),op_c))),
inference(step,[status(thm)],[t19505,t61]) ).
cnf(t19507,plain,
rd(mult(op_c,op_c),ld(op_c,X1)) = mult(op_c,mult(rd(op_c,X1),op_c)),
inference(step,[status(thm)],[t19506,t13]) ).
cnf(t19508,plain,
rd(mult(op_c,op_c),ld(op_c,X1)) = rd(op_c,ld(op_c,rd(X1,op_c))),
inference(step,[status(thm)],[t19507,t5177]) ).
cnf(t7828,plain,
rd(mult(op_c,op_c),ld(op_c,X1)) = rd(op_c,ld(op_c,rd(X1,op_c))),
inference(orient,[status(thm)],[t19508]) ).
cnf(t7850,plain,
rd(ld(op_c,X1),mult(op_c,op_c)) = i(rd(op_c,ld(op_c,rd(X1,op_c)))),
inference(cp,[status(thm)],[t130,t7828]) ).
cnf(t19509,plain,
rd(ld(op_c,X1),mult(op_c,op_c)) = rd(ld(op_c,rd(X1,op_c)),op_c),
inference(step,[status(thm)],[t7850,t130]) ).
cnf(t7875,plain,
rd(ld(op_c,rd(X1,op_c)),op_c) = rd(ld(op_c,X1),mult(op_c,op_c)),
inference(orient,[status(thm)],[t19509]) ).
cnf(t42,plain,
mult(mult(X1,mult(X2,X1)),mult(X3,mult(mult(X1,mult(X2,X1)),Y3))) = mult(mult(X1,mult(X2,mult(X1,mult(X3,mult(X1,mult(X2,X1)))))),Y3),
inference(cp,[status(thm)],[t33,t33]) ).
cnf(t19527,plain,
mult(X1,mult(X2,mult(X1,mult(X3,mult(mult(X1,mult(X2,X1)),Y3))))) = mult(mult(X1,mult(X2,mult(X1,mult(X3,mult(X1,mult(X2,X1)))))),Y3),
inference(step,[status(thm)],[t42,t33]) ).
cnf(t19528,plain,
mult(X1,mult(X2,mult(X1,mult(X3,mult(X1,mult(X2,mult(X1,Y3))))))) = mult(mult(X1,mult(X2,mult(X1,mult(X3,mult(X1,mult(X2,X1)))))),Y3),
inference(step,[status(thm)],[t19527,t33]) ).
cnf(t9423,plain,
mult(mult(X1,mult(X2,mult(X1,mult(X3,mult(X1,mult(X2,X1)))))),Y3) = mult(X1,mult(X2,mult(X1,mult(X3,mult(X1,mult(X2,mult(X1,Y3))))))),
inference(orient,[status(thm)],[t19528]) ).
cnf(t4686,plain,
mult(X1,mult(rd(mult(ld(X1,X2),X1),X1),X3)) = mult(rd(X2,i(X1)),ld(X1,X3)),
inference(cp,[status(thm)],[t4679,t4191]) ).
cnf(t19532,plain,
mult(X1,mult(ld(X1,X2),X3)) = mult(rd(X2,i(X1)),ld(X1,X3)),
inference(step,[status(thm)],[t4686,t23]) ).
cnf(t9997,plain,
mult(rd(X1,i(X2)),ld(X2,X3)) = mult(X2,mult(ld(X2,X1),X3)),
inference(orient,[status(thm)],[t19532]) ).
cnf(t10010,plain,
mult(X1,mult(ld(X1,i(X2)),X3)) = mult(rd(X1,X2),ld(X1,X3)),
inference(cp,[status(thm)],[t9997,t158]) ).
cnf(t19533,plain,
mult(X1,ld(mult(X1,X2),X3)) = mult(rd(X1,X2),ld(X1,X3)),
inference(step,[status(thm)],[t10010,t293]) ).
cnf(t10091,plain,
mult(rd(X1,X2),ld(X1,X3)) = mult(X1,ld(mult(X1,X2),X3)),
inference(orient,[status(thm)],[t19533]) ).
cnf(t401,plain,
mult(X1,X1) = rd(mult(X1,X2),ld(X1,X2)),
inference(cp,[status(thm)],[t389,t11]) ).
cnf(t512,plain,
rd(mult(X1,X2),ld(X1,X2)) = mult(X1,X1),
inference(orient,[status(thm)],[t401]) ).
cnf(t519,plain,
mult(i(X1),i(X1)) = rd(ld(X1,X2),ld(i(X1),X2)),
inference(cp,[status(thm)],[t512,t98]) ).
cnf(t19370,plain,
ld(X1,i(X1)) = rd(ld(X1,X2),ld(i(X1),X2)),
inference(step,[status(thm)],[t519,t98]) ).
cnf(t19371,plain,
rd(i(X1),X1) = rd(ld(X1,X2),ld(i(X1),X2)),
inference(step,[status(thm)],[t19370,t438]) ).
cnf(t19372,plain,
rd(i(X1),X1) = rd(ld(X1,X2),mult(X1,X2)),
inference(step,[status(thm)],[t19371,t106]) ).
cnf(t613,plain,
rd(ld(X1,X2),mult(X1,X2)) = rd(i(X1),X1),
inference(orient,[status(thm)],[t19372]) ).
cnf(t4,axiom,
mult(op_d,mult(op_d,op_d)) = unit,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t53,plain,
mult(op_d,mult(op_d,op_d)) = unit,
inference(orient,[status(thm)],[t4]) ).
cnf(t56,plain,
mult(op_d,op_d) = mult(i(op_d),unit),
inference(cp,[status(thm)],[t15,t53]) ).
cnf(t19339,plain,
mult(op_d,op_d) = i(op_d),
inference(step,[status(thm)],[t56,t12]) ).
cnf(t63,plain,
mult(op_d,op_d) = i(op_d),
inference(orient,[status(thm)],[t19339]) ).
cnf(t191,plain,
mult(op_d,mult(op_d,X1)) = mult(i(op_d),X1),
inference(cp,[status(thm)],[t188,t63]) ).
cnf(t19350,plain,
mult(op_d,mult(op_d,X1)) = ld(op_d,X1),
inference(step,[status(thm)],[t191,t98]) ).
cnf(t200,plain,
mult(op_d,mult(op_d,X1)) = ld(op_d,X1),
inference(orient,[status(thm)],[t19350]) ).
cnf(t3186,plain,
mult(mult(op_d,X1),op_d) = mult(op_d,mult(rd(X1,op_d),i(op_d))),
inference(cp,[status(thm)],[t3098,t63]) ).
cnf(t5896,plain,
mult(op_d,mult(rd(X1,op_d),i(op_d))) = mult(mult(op_d,X1),op_d),
inference(orient,[status(thm)],[t3186]) ).
cnf(t5910,plain,
ld(op_d,mult(rd(X1,op_d),i(op_d))) = mult(op_d,mult(mult(op_d,X1),op_d)),
inference(cp,[status(thm)],[t200,t5896]) ).
cnf(t3615,plain,
ld(X1,i(ld(X2,X1))) = i(rd(X1,ld(X1,X2))),
inference(cp,[status(thm)],[t110,t3578]) ).
cnf(t19423,plain,
ld(X1,mult(X2,i(X1))) = i(rd(X1,ld(X1,X2))),
inference(step,[status(thm)],[t3615,t120]) ).
cnf(t19424,plain,
ld(X1,mult(X2,i(X1))) = rd(ld(X1,X2),X1),
inference(step,[status(thm)],[t19423,t130]) ).
cnf(t3686,plain,
ld(X1,mult(X2,i(X1))) = rd(ld(X1,X2),X1),
inference(orient,[status(thm)],[t19424]) ).
cnf(t19448,plain,
rd(ld(op_d,rd(X1,op_d)),op_d) = mult(op_d,mult(mult(op_d,X1),op_d)),
inference(step,[status(thm)],[t5910,t3686]) ).
cnf(t201,plain,
ld(op_d,ld(op_d,X1)) = mult(op_d,X1),
inference(cp,[status(thm)],[t200,t11]) ).
cnf(t207,plain,
ld(op_d,ld(op_d,X1)) = mult(op_d,X1),
inference(orient,[status(thm)],[t201]) ).
cnf(t4223,plain,
rd(ld(op_d,X1),i(op_d)) = mult(op_d,mult(mult(op_d,X1),op_d)),
inference(cp,[status(thm)],[t4191,t207]) ).
cnf(t19438,plain,
rd(op_d,i(ld(op_d,X1))) = mult(op_d,mult(mult(op_d,X1),op_d)),
inference(step,[status(thm)],[t4223,t256]) ).
cnf(t19439,plain,
rd(op_d,mult(op_d,i(X1))) = mult(op_d,mult(mult(op_d,X1),op_d)),
inference(step,[status(thm)],[t19438,t120]) ).
cnf(t4560,plain,
mult(op_d,mult(mult(op_d,X1),op_d)) = rd(op_d,mult(op_d,i(X1))),
inference(orient,[status(thm)],[t19439]) ).
cnf(t19449,plain,
rd(ld(op_d,rd(X1,op_d)),op_d) = rd(op_d,mult(op_d,i(X1))),
inference(step,[status(thm)],[t19448,t4560]) ).
cnf(t5929,plain,
rd(ld(op_d,rd(X1,op_d)),op_d) = rd(op_d,mult(op_d,i(X1))),
inference(orient,[status(thm)],[t19449]) ).
cnf(t3266,plain,
i(mult(X1,X2)) = rd(i(X1),mult(X1,rd(X2,X1))),
inference(cp,[status(thm)],[t135,t3217]) ).
cnf(t19436,plain,
ld(X1,i(X2)) = rd(i(X1),mult(X1,rd(X2,X1))),
inference(step,[status(thm)],[t3266,t110]) ).
cnf(t164,plain,
rd(ld(X1,X2),X3) = rd(i(X3),mult(X1,i(X2))),
inference(cp,[status(thm)],[t158,t120]) ).
cnf(t672,plain,
rd(i(X1),mult(X2,i(X3))) = rd(ld(X2,X3),X1),
inference(orient,[status(thm)],[t164]) ).
cnf(t684,plain,
rd(ld(X1,rd(X2,X3)),Y3) = rd(i(Y3),mult(X1,rd(X3,X2))),
inference(cp,[status(thm)],[t672,t130]) ).
cnf(t2617,plain,
rd(i(X1),mult(X2,rd(X3,Y3))) = rd(ld(X2,rd(Y3,X3)),X1),
inference(orient,[status(thm)],[t684]) ).
cnf(t19437,plain,
ld(X1,i(X2)) = rd(ld(X1,rd(X1,X2)),X1),
inference(step,[status(thm)],[t19436,t2617]) ).
cnf(t4121,plain,
rd(ld(X1,rd(X1,X2)),X1) = ld(X1,i(X2)),
inference(orient,[status(thm)],[t19437]) ).
cnf(t5931,plain,
rd(op_d,mult(op_d,i(ld(op_d,rd(op_d,X1))))) = rd(ld(op_d,ld(op_d,i(X1))),op_d),
inference(cp,[status(thm)],[t5929,t4121]) ).
cnf(t19454,plain,
rd(op_d,mult(op_d,mult(op_d,i(rd(op_d,X1))))) = rd(ld(op_d,ld(op_d,i(X1))),op_d),
inference(step,[status(thm)],[t5931,t120]) ).
cnf(t19455,plain,
rd(op_d,ld(op_d,i(rd(op_d,X1)))) = rd(ld(op_d,ld(op_d,i(X1))),op_d),
inference(step,[status(thm)],[t19454,t200]) ).
cnf(t3497,plain,
mult(X1,mult(X2,X1)) = rd(X1,ld(X1,i(X2))),
inference(cp,[status(thm)],[t3482,t135]) ).
cnf(t3635,plain,
rd(X1,ld(X1,i(X2))) = mult(X1,mult(X2,X1)),
inference(orient,[status(thm)],[t3497]) ).
cnf(t19456,plain,
mult(op_d,mult(rd(op_d,X1),op_d)) = rd(ld(op_d,ld(op_d,i(X1))),op_d),
inference(step,[status(thm)],[t19455,t3635]) ).
cnf(t19457,plain,
rd(op_d,ld(op_d,rd(X1,op_d))) = rd(ld(op_d,ld(op_d,i(X1))),op_d),
inference(step,[status(thm)],[t19456,t5177]) ).
cnf(t19458,plain,
rd(op_d,ld(op_d,rd(X1,op_d))) = rd(mult(op_d,i(X1)),op_d),
inference(step,[status(thm)],[t19457,t207]) ).
cnf(t163,plain,
rd(rd(X1,X2),X3) = rd(i(X3),rd(X2,X1)),
inference(cp,[status(thm)],[t158,t130]) ).
cnf(t370,plain,
rd(i(X1),rd(X2,X3)) = rd(rd(X3,X2),X1),
inference(orient,[status(thm)],[t163]) ).
cnf(t372,plain,
rd(rd(X1,X2),ld(X3,Y3)) = rd(mult(X3,i(Y3)),rd(X2,X1)),
inference(cp,[status(thm)],[t370,t120]) ).
cnf(t2052,plain,
rd(mult(X1,i(X2)),rd(X3,Y3)) = rd(rd(Y3,X3),ld(X1,X2)),
inference(orient,[status(thm)],[t372]) ).
cnf(t65,plain,
op_d = rd(i(op_d),op_d),
inference(cp,[status(thm)],[t23,t63]) ).
cnf(t88,plain,
rd(i(op_d),op_d) = op_d,
inference(orient,[status(thm)],[t65]) ).
cnf(t2075,plain,
rd(rd(op_d,i(op_d)),ld(X1,X2)) = rd(mult(X1,i(X2)),op_d),
inference(cp,[status(thm)],[t2052,t88]) ).
cnf(t64,plain,
op_d = ld(op_d,i(op_d)),
inference(cp,[status(thm)],[t28,t63]) ).
cnf(t87,plain,
ld(op_d,i(op_d)) = op_d,
inference(orient,[status(thm)],[t64]) ).
cnf(t128,plain,
i(op_d) = rd(op_d,i(op_d)),
inference(cp,[status(thm)],[t125,t87]) ).
cnf(t129,plain,
rd(op_d,i(op_d)) = i(op_d),
inference(orient,[status(thm)],[t128]) ).
cnf(t19401,plain,
rd(i(op_d),ld(X1,X2)) = rd(mult(X1,i(X2)),op_d),
inference(step,[status(thm)],[t2075,t129]) ).
cnf(t2126,plain,
rd(mult(X1,i(X2)),op_d) = rd(i(op_d),ld(X1,X2)),
inference(orient,[status(thm)],[t19401]) ).
cnf(t19459,plain,
rd(op_d,ld(op_d,rd(X1,op_d))) = rd(i(op_d),ld(op_d,X1)),
inference(step,[status(thm)],[t19458,t2126]) ).
cnf(t6015,plain,
rd(op_d,ld(op_d,rd(X1,op_d))) = rd(i(op_d),ld(op_d,X1)),
inference(orient,[status(thm)],[t19459]) ).
cnf(t6024,plain,
rd(i(op_d),ld(op_d,mult(X1,op_d))) = rd(op_d,ld(op_d,X1)),
inference(cp,[status(thm)],[t6015,t23]) ).
cnf(t6664,plain,
rd(i(op_d),ld(op_d,mult(X1,op_d))) = rd(op_d,ld(op_d,X1)),
inference(orient,[status(thm)],[t6024]) ).
cnf(t134,plain,
unit = mult(rd(X1,X2),rd(X2,X1)),
inference(cp,[status(thm)],[t96,t130]) ).
cnf(t245,plain,
mult(rd(X1,X2),rd(X2,X1)) = unit,
inference(orient,[status(thm)],[t134]) ).
cnf(t410,plain,
mult(rd(X1,X2),rd(X1,X2)) = rd(mult(rd(X1,X2),unit),rd(X2,X1)),
inference(cp,[status(thm)],[t389,t245]) ).
cnf(t409,plain,
mult(rd(X1,X2),rd(X1,X2)) = rd(mult(rd(X1,X2),X1),X2),
inference(cp,[status(thm)],[t389,t20]) ).
cnf(t888,plain,
mult(rd(X1,X2),rd(X1,X2)) = rd(mult(rd(X1,X2),X1),X2),
inference(orient,[status(thm)],[t409]) ).
cnf(t19374,plain,
rd(mult(rd(X1,X2),X1),X2) = rd(mult(rd(X1,X2),unit),rd(X2,X1)),
inference(step,[status(thm)],[t410,t888]) ).
cnf(t19375,plain,
rd(mult(rd(X1,X2),X1),X2) = rd(rd(X1,X2),rd(X2,X1)),
inference(step,[status(thm)],[t19374,t12]) ).
cnf(t940,plain,
rd(mult(rd(X1,X2),X1),X2) = rd(rd(X1,X2),rd(X2,X1)),
inference(orient,[status(thm)],[t19375]) ).
cnf(t973,plain,
mult(rd(X1,X2),X1) = mult(rd(rd(X1,X2),rd(X2,X1)),X2),
inference(cp,[status(thm)],[t20,t940]) ).
cnf(t522,plain,
mult(rd(X1,X2),rd(X1,X2)) = rd(X1,ld(rd(X1,X2),X2)),
inference(cp,[status(thm)],[t512,t20]) ).
cnf(t19376,plain,
mult(rd(X1,X2),rd(X1,X2)) = rd(rd(X1,X2),rd(X2,X1)),
inference(step,[status(thm)],[t888,t940]) ).
cnf(t941,plain,
mult(rd(X1,X2),rd(X1,X2)) = rd(rd(X1,X2),rd(X2,X1)),
inference(orient,[status(thm)],[t19376]) ).
cnf(t19378,plain,
rd(rd(X1,X2),rd(X2,X1)) = rd(X1,ld(rd(X1,X2),X2)),
inference(step,[status(thm)],[t522,t941]) ).
cnf(t19379,plain,
rd(rd(X1,X2),rd(X2,X1)) = rd(X1,mult(rd(X2,X1),X2)),
inference(step,[status(thm)],[t19378,t210]) ).
cnf(t983,plain,
rd(rd(X1,X2),rd(X2,X1)) = rd(X1,mult(rd(X2,X1),X2)),
inference(orient,[status(thm)],[t19379]) ).
cnf(t19552,plain,
mult(rd(X1,X2),X1) = mult(rd(X1,mult(rd(X2,X1),X2)),X2),
inference(step,[status(thm)],[t973,t983]) ).
cnf(t11463,plain,
mult(rd(X1,mult(rd(X2,X1),X2)),X2) = mult(rd(X1,X2),X1),
inference(orient,[status(thm)],[t19552]) ).
cnf(t405,plain,
mult(op_c,op_c) = rd(mult(op_c,ld(op_c,X1)),mult(op_c,mult(op_c,X1))),
inference(cp,[status(thm)],[t389,t383]) ).
cnf(t19363,plain,
mult(op_c,op_c) = rd(X1,mult(op_c,mult(op_c,X1))),
inference(step,[status(thm)],[t405,t11]) ).
cnf(t536,plain,
rd(X1,mult(op_c,mult(op_c,X1))) = mult(op_c,op_c),
inference(orient,[status(thm)],[t19363]) ).
cnf(t538,plain,
rd(rd(mult(op_c,mult(op_c,X1)),X1),X2) = rd(i(X2),mult(op_c,op_c)),
inference(cp,[status(thm)],[t370,t536]) ).
cnf(t19364,plain,
rd(mult(op_c,op_c),X2) = rd(i(X2),mult(op_c,op_c)),
inference(step,[status(thm)],[t538,t389]) ).
cnf(t540,plain,
rd(i(X1),mult(op_c,op_c)) = rd(mult(op_c,op_c),X1),
inference(orient,[status(thm)],[t19364]) ).
cnf(t551,plain,
i(X1) = mult(rd(mult(op_c,op_c),X1),mult(op_c,op_c)),
inference(cp,[status(thm)],[t20,t540]) ).
cnf(t1038,plain,
mult(rd(mult(op_c,op_c),X1),mult(op_c,op_c)) = i(X1),
inference(orient,[status(thm)],[t551]) ).
cnf(t11470,plain,
mult(rd(X1,mult(op_c,op_c)),X1) = mult(rd(X1,i(X1)),mult(op_c,op_c)),
inference(cp,[status(thm)],[t11463,t1038]) ).
cnf(t19553,plain,
mult(rd(X1,mult(op_c,op_c)),X1) = mult(mult(X1,X1),mult(op_c,op_c)),
inference(step,[status(thm)],[t11470,t425]) ).
cnf(t19554,plain,
mult(rd(X1,mult(op_c,op_c)),X1) = mult(X1,mult(X1,mult(op_c,op_c))),
inference(step,[status(thm)],[t19553,t188]) ).
cnf(t11589,plain,
mult(rd(X1,mult(op_c,op_c)),X1) = mult(X1,mult(X1,mult(op_c,op_c))),
inference(orient,[status(thm)],[t19554]) ).
cnf(t11622,plain,
rd(op_d,ld(op_d,rd(op_d,mult(op_c,op_c)))) = rd(i(op_d),ld(op_d,mult(op_d,mult(op_d,mult(op_c,op_c))))),
inference(cp,[status(thm)],[t6664,t11589]) ).
cnf(t19555,plain,
mult(op_d,mult(op_c,op_c)) = rd(i(op_d),ld(op_d,mult(op_d,mult(op_d,mult(op_c,op_c))))),
inference(step,[status(thm)],[t11622,t3482]) ).
cnf(t19556,plain,
mult(op_d,mult(op_c,op_c)) = rd(i(op_d),mult(op_d,mult(op_c,op_c))),
inference(step,[status(thm)],[t19555,t28]) ).
cnf(t394,plain,
mult(op_c,op_c) = rd(i(op_c),op_c),
inference(cp,[status(thm)],[t389,t138]) ).
cnf(t418,plain,
rd(i(op_c),op_c) = mult(op_c,op_c),
inference(orient,[status(thm)],[t394]) ).
cnf(t2649,plain,
rd(ld(X1,rd(op_c,i(op_c))),X2) = rd(i(X2),mult(X1,mult(op_c,op_c))),
inference(cp,[status(thm)],[t2617,t418]) ).
cnf(t19494,plain,
rd(ld(X1,mult(op_c,op_c)),X2) = rd(i(X2),mult(X1,mult(op_c,op_c))),
inference(step,[status(thm)],[t2649,t425]) ).
cnf(t7651,plain,
rd(i(X1),mult(X2,mult(op_c,op_c))) = rd(ld(X2,mult(op_c,op_c)),X1),
inference(orient,[status(thm)],[t19494]) ).
cnf(t19557,plain,
mult(op_d,mult(op_c,op_c)) = rd(ld(op_d,mult(op_c,op_c)),op_d),
inference(step,[status(thm)],[t19556,t7651]) ).
cnf(t11673,plain,
rd(ld(op_d,mult(op_c,op_c)),op_d) = mult(op_d,mult(op_c,op_c)),
inference(orient,[status(thm)],[t19557]) ).
cnf(t11690,plain,
rd(i(op_d),ld(op_d,ld(op_d,mult(op_c,op_c)))) = rd(op_d,ld(op_d,mult(op_d,mult(op_c,op_c)))),
inference(cp,[status(thm)],[t6015,t11673]) ).
cnf(t19558,plain,
rd(i(op_d),mult(op_d,mult(op_c,op_c))) = rd(op_d,ld(op_d,mult(op_d,mult(op_c,op_c)))),
inference(step,[status(thm)],[t11690,t207]) ).
cnf(t19559,plain,
rd(ld(op_d,mult(op_c,op_c)),op_d) = rd(op_d,ld(op_d,mult(op_d,mult(op_c,op_c)))),
inference(step,[status(thm)],[t19558,t7651]) ).
cnf(t19560,plain,
mult(op_d,mult(op_c,op_c)) = rd(op_d,ld(op_d,mult(op_d,mult(op_c,op_c)))),
inference(step,[status(thm)],[t19559,t11673]) ).
cnf(t19561,plain,
mult(op_d,mult(op_c,op_c)) = rd(op_d,mult(op_c,op_c)),
inference(step,[status(thm)],[t19560,t28]) ).
cnf(t11720,plain,
mult(op_d,mult(op_c,op_c)) = rd(op_d,mult(op_c,op_c)),
inference(orient,[status(thm)],[t19561]) ).
cnf(t11734,plain,
ld(op_d,i(mult(op_c,op_c))) = i(rd(op_d,mult(op_c,op_c))),
inference(cp,[status(thm)],[t110,t11720]) ).
cnf(t19564,plain,
ld(op_d,ld(op_c,i(op_c))) = i(rd(op_d,mult(op_c,op_c))),
inference(step,[status(thm)],[t11734,t110]) ).
cnf(t19565,plain,
ld(op_d,mult(op_c,op_c)) = i(rd(op_d,mult(op_c,op_c))),
inference(step,[status(thm)],[t19564,t145]) ).
cnf(t19566,plain,
ld(op_d,mult(op_c,op_c)) = rd(mult(op_c,op_c),op_d),
inference(step,[status(thm)],[t19565,t130]) ).
cnf(t11765,plain,
ld(op_d,mult(op_c,op_c)) = rd(mult(op_c,op_c),op_d),
inference(orient,[status(thm)],[t19566]) ).
cnf(t11771,plain,
rd(i(op_d),op_d) = rd(rd(mult(op_c,op_c),op_d),mult(op_d,mult(op_c,op_c))),
inference(cp,[status(thm)],[t613,t11765]) ).
cnf(t19614,plain,
op_d = rd(rd(mult(op_c,op_c),op_d),mult(op_d,mult(op_c,op_c))),
inference(step,[status(thm)],[t11771,t88]) ).
cnf(t19615,plain,
op_d = rd(rd(mult(op_c,op_c),op_d),rd(op_d,mult(op_c,op_c))),
inference(step,[status(thm)],[t19614,t11720]) ).
cnf(t19616,plain,
op_d = rd(mult(op_c,op_c),mult(rd(op_d,mult(op_c,op_c)),op_d)),
inference(step,[status(thm)],[t19615,t983]) ).
cnf(t19617,plain,
op_d = rd(mult(op_c,op_c),mult(op_d,mult(op_d,mult(op_c,op_c)))),
inference(step,[status(thm)],[t19616,t11589]) ).
cnf(t19618,plain,
op_d = rd(mult(op_c,op_c),ld(op_d,mult(op_c,op_c))),
inference(step,[status(thm)],[t19617,t200]) ).
cnf(t19619,plain,
op_d = rd(mult(op_c,op_c),rd(mult(op_c,op_c),op_d)),
inference(step,[status(thm)],[t19618,t11765]) ).
cnf(t12250,plain,
rd(mult(op_c,op_c),rd(mult(op_c,op_c),op_d)) = op_d,
inference(orient,[status(thm)],[t19619]) ).
cnf(t12251,plain,
mult(mult(op_c,op_c),ld(mult(mult(op_c,op_c),rd(mult(op_c,op_c),op_d)),X1)) = mult(op_d,ld(mult(op_c,op_c),X1)),
inference(cp,[status(thm)],[t10091,t12250]) ).
cnf(t19625,plain,
mult(op_c,mult(op_c,ld(mult(mult(op_c,op_c),rd(mult(op_c,op_c),op_d)),X1))) = mult(op_d,ld(mult(op_c,op_c),X1)),
inference(step,[status(thm)],[t12251,t188]) ).
cnf(t299,plain,
ld(mult(X1,rd(X2,X3)),Y3) = mult(ld(X1,rd(X3,X2)),Y3),
inference(cp,[status(thm)],[t293,t130]) ).
cnf(t861,plain,
ld(mult(X1,rd(X2,X3)),Y3) = mult(ld(X1,rd(X3,X2)),Y3),
inference(orient,[status(thm)],[t299]) ).
cnf(t19626,plain,
mult(op_c,mult(op_c,mult(ld(mult(op_c,op_c),rd(op_d,mult(op_c,op_c))),X1))) = mult(op_d,ld(mult(op_c,op_c),X1)),
inference(step,[status(thm)],[t19625,t861]) ).
cnf(t19627,plain,
mult(op_c,mult(op_c,mult(ld(op_c,ld(op_c,rd(op_d,mult(op_c,op_c)))),X1))) = mult(op_d,ld(mult(op_c,op_c),X1)),
inference(step,[status(thm)],[t19626,t337]) ).
cnf(t19628,plain,
mult(op_c,mult(op_c,mult(mult(op_c,mult(op_c,rd(op_d,mult(op_c,op_c)))),X1))) = mult(op_d,ld(mult(op_c,op_c),X1)),
inference(step,[status(thm)],[t19627,t347]) ).
cnf(t5912,plain,
ld(op_d,i(mult(rd(X1,op_d),i(op_d)))) = i(mult(mult(op_d,X1),op_d)),
inference(cp,[status(thm)],[t110,t5896]) ).
cnf(t19450,plain,
ld(op_d,ld(rd(X1,op_d),i(i(op_d)))) = i(mult(mult(op_d,X1),op_d)),
inference(step,[status(thm)],[t5912,t110]) ).
cnf(t19451,plain,
ld(op_d,mult(rd(op_d,X1),i(i(op_d)))) = i(mult(mult(op_d,X1),op_d)),
inference(step,[status(thm)],[t19450,t210]) ).
cnf(t66,plain,
op_d = mult(i(op_d),i(op_d)),
inference(cp,[status(thm)],[t15,t63]) ).
cnf(t19341,plain,
op_d = i(mult(op_d,op_d)),
inference(step,[status(thm)],[t66,t49]) ).
cnf(t19342,plain,
op_d = i(i(op_d)),
inference(step,[status(thm)],[t19341,t63]) ).
cnf(t69,plain,
i(i(op_d)) = op_d,
inference(orient,[status(thm)],[t19342]) ).
cnf(t19452,plain,
ld(op_d,mult(rd(op_d,X1),op_d)) = i(mult(mult(op_d,X1),op_d)),
inference(step,[status(thm)],[t19451,t69]) ).
cnf(t19453,plain,
ld(op_d,mult(rd(op_d,X1),op_d)) = ld(mult(op_d,X1),i(op_d)),
inference(step,[status(thm)],[t19452,t110]) ).
cnf(t5980,plain,
ld(op_d,mult(rd(op_d,X1),op_d)) = ld(mult(op_d,X1),i(op_d)),
inference(orient,[status(thm)],[t19453]) ).
cnf(t5937,plain,
rd(op_d,mult(op_d,i(ld(X1,op_d)))) = rd(ld(op_d,i(X1)),op_d),
inference(cp,[status(thm)],[t5929,t125]) ).
cnf(t19485,plain,
rd(op_d,mult(op_d,mult(X1,i(op_d)))) = rd(ld(op_d,i(X1)),op_d),
inference(step,[status(thm)],[t5937,t120]) ).
cnf(t2136,plain,
rd(i(op_d),ld(i(X1),X2)) = rd(ld(X1,i(X2)),op_d),
inference(cp,[status(thm)],[t2126,t98]) ).
cnf(t19403,plain,
rd(i(op_d),mult(X1,X2)) = rd(ld(X1,i(X2)),op_d),
inference(step,[status(thm)],[t2136,t106]) ).
cnf(t2195,plain,
rd(ld(X1,i(X2)),op_d) = rd(i(op_d),mult(X1,X2)),
inference(orient,[status(thm)],[t19403]) ).
cnf(t19486,plain,
rd(op_d,mult(op_d,mult(X1,i(op_d)))) = rd(i(op_d),mult(op_d,X1)),
inference(step,[status(thm)],[t19485,t2195]) ).
cnf(t7093,plain,
rd(op_d,mult(op_d,mult(X1,i(op_d)))) = rd(i(op_d),mult(op_d,X1)),
inference(orient,[status(thm)],[t19486]) ).
cnf(t11656,plain,
rd(i(op_d),mult(op_d,rd(i(op_d),mult(op_c,op_c)))) = rd(op_d,mult(op_d,mult(i(op_d),mult(i(op_d),mult(op_c,op_c))))),
inference(cp,[status(thm)],[t7093,t11589]) ).
cnf(t19571,plain,
rd(ld(op_d,rd(mult(op_c,op_c),i(op_d))),op_d) = rd(op_d,mult(op_d,mult(i(op_d),mult(i(op_d),mult(op_c,op_c))))),
inference(step,[status(thm)],[t11656,t2617]) ).
cnf(t19572,plain,
rd(mult(ld(op_d,mult(op_c,op_c)),op_d),op_d) = rd(op_d,mult(op_d,mult(i(op_d),mult(i(op_d),mult(op_c,op_c))))),
inference(step,[status(thm)],[t19571,t3381]) ).
cnf(t19573,plain,
ld(op_d,mult(op_c,op_c)) = rd(op_d,mult(op_d,mult(i(op_d),mult(i(op_d),mult(op_c,op_c))))),
inference(step,[status(thm)],[t19572,t23]) ).
cnf(t19574,plain,
rd(mult(op_c,op_c),op_d) = rd(op_d,mult(op_d,mult(i(op_d),mult(i(op_d),mult(op_c,op_c))))),
inference(step,[status(thm)],[t19573,t11765]) ).
cnf(t19575,plain,
rd(mult(op_c,op_c),op_d) = rd(op_d,mult(op_d,ld(op_d,mult(i(op_d),mult(op_c,op_c))))),
inference(step,[status(thm)],[t19574,t98]) ).
cnf(t19576,plain,
rd(mult(op_c,op_c),op_d) = rd(op_d,mult(i(op_d),mult(op_c,op_c))),
inference(step,[status(thm)],[t19575,t11]) ).
cnf(t19577,plain,
rd(mult(op_c,op_c),op_d) = rd(op_d,ld(op_d,mult(op_c,op_c))),
inference(step,[status(thm)],[t19576,t98]) ).
cnf(t19578,plain,
rd(mult(op_c,op_c),op_d) = rd(op_d,rd(mult(op_c,op_c),op_d)),
inference(step,[status(thm)],[t19577,t11765]) ).
cnf(t11834,plain,
rd(op_d,rd(mult(op_c,op_c),op_d)) = rd(mult(op_c,op_c),op_d),
inference(orient,[status(thm)],[t19578]) ).
cnf(t11850,plain,
ld(mult(op_d,rd(mult(op_c,op_c),op_d)),i(op_d)) = ld(op_d,mult(rd(mult(op_c,op_c),op_d),op_d)),
inference(cp,[status(thm)],[t5980,t11834]) ).
cnf(t19579,plain,
mult(ld(op_d,rd(op_d,mult(op_c,op_c))),i(op_d)) = ld(op_d,mult(rd(mult(op_c,op_c),op_d),op_d)),
inference(step,[status(thm)],[t11850,t861]) ).
cnf(t3267,plain,
ld(mult(X1,X2),i(i(X1))) = i(mult(X1,rd(X2,X1))),
inference(cp,[status(thm)],[t110,t3217]) ).
cnf(t19414,plain,
ld(mult(X1,X2),X1) = i(mult(X1,rd(X2,X1))),
inference(step,[status(thm)],[t3267,t81]) ).
cnf(t19415,plain,
ld(mult(X1,X2),X1) = ld(X1,i(rd(X2,X1))),
inference(step,[status(thm)],[t19414,t110]) ).
cnf(t19416,plain,
ld(mult(X1,X2),X1) = ld(X1,rd(X1,X2)),
inference(step,[status(thm)],[t19415,t130]) ).
cnf(t3297,plain,
ld(mult(X1,X2),X1) = ld(X1,rd(X1,X2)),
inference(orient,[status(thm)],[t19416]) ).
cnf(t872,plain,
mult(ld(X1,rd(op_c,i(op_c))),X2) = ld(mult(X1,mult(op_c,op_c)),X2),
inference(cp,[status(thm)],[t861,t418]) ).
cnf(t19385,plain,
mult(ld(X1,mult(op_c,op_c)),X2) = ld(mult(X1,mult(op_c,op_c)),X2),
inference(step,[status(thm)],[t872,t425]) ).
cnf(t1122,plain,
ld(mult(X1,mult(op_c,op_c)),X2) = mult(ld(X1,mult(op_c,op_c)),X2),
inference(orient,[status(thm)],[t19385]) ).
cnf(t3299,plain,
ld(X1,rd(X1,mult(op_c,op_c))) = mult(ld(X1,mult(op_c,op_c)),X1),
inference(cp,[status(thm)],[t3297,t1122]) ).
cnf(t4976,plain,
ld(X1,rd(X1,mult(op_c,op_c))) = mult(ld(X1,mult(op_c,op_c)),X1),
inference(orient,[status(thm)],[t3299]) ).
cnf(t19580,plain,
mult(mult(ld(op_d,mult(op_c,op_c)),op_d),i(op_d)) = ld(op_d,mult(rd(mult(op_c,op_c),op_d),op_d)),
inference(step,[status(thm)],[t19579,t4976]) ).
cnf(t19581,plain,
mult(mult(rd(mult(op_c,op_c),op_d),op_d),i(op_d)) = ld(op_d,mult(rd(mult(op_c,op_c),op_d),op_d)),
inference(step,[status(thm)],[t19580,t11765]) ).
cnf(t19582,plain,
mult(mult(op_c,op_c),i(op_d)) = ld(op_d,mult(rd(mult(op_c,op_c),op_d),op_d)),
inference(step,[status(thm)],[t19581,t20]) ).
cnf(t19583,plain,
mult(op_c,mult(op_c,i(op_d))) = ld(op_d,mult(rd(mult(op_c,op_c),op_d),op_d)),
inference(step,[status(thm)],[t19582,t188]) ).
cnf(t19584,plain,
mult(op_c,mult(op_c,i(op_d))) = ld(op_d,mult(op_c,op_c)),
inference(step,[status(thm)],[t19583,t20]) ).
cnf(t19585,plain,
mult(op_c,mult(op_c,i(op_d))) = rd(mult(op_c,op_c),op_d),
inference(step,[status(thm)],[t19584,t11765]) ).
cnf(t11877,plain,
mult(op_c,mult(op_c,i(op_d))) = rd(mult(op_c,op_c),op_d),
inference(orient,[status(thm)],[t19585]) ).
cnf(t11888,plain,
ld(op_c,i(mult(op_c,i(op_d)))) = i(rd(mult(op_c,op_c),op_d)),
inference(cp,[status(thm)],[t110,t11877]) ).
cnf(t19586,plain,
ld(op_c,ld(op_c,i(i(op_d)))) = i(rd(mult(op_c,op_c),op_d)),
inference(step,[status(thm)],[t11888,t110]) ).
cnf(t19587,plain,
mult(op_c,mult(op_c,i(i(op_d)))) = i(rd(mult(op_c,op_c),op_d)),
inference(step,[status(thm)],[t19586,t347]) ).
cnf(t19588,plain,
mult(op_c,mult(op_c,op_d)) = i(rd(mult(op_c,op_c),op_d)),
inference(step,[status(thm)],[t19587,t69]) ).
cnf(t19589,plain,
mult(op_c,mult(op_c,op_d)) = rd(op_d,mult(op_c,op_c)),
inference(step,[status(thm)],[t19588,t130]) ).
cnf(t11925,plain,
mult(op_c,mult(op_c,op_d)) = rd(op_d,mult(op_c,op_c)),
inference(orient,[status(thm)],[t19589]) ).
cnf(t11960,plain,
ld(op_c,op_d) = mult(op_c,rd(op_d,mult(op_c,op_c))),
inference(cp,[status(thm)],[t383,t11925]) ).
cnf(t12063,plain,
mult(op_c,rd(op_d,mult(op_c,op_c))) = ld(op_c,op_d),
inference(orient,[status(thm)],[t11960]) ).
cnf(t19629,plain,
mult(op_c,mult(op_c,mult(mult(op_c,ld(op_c,op_d)),X1))) = mult(op_d,ld(mult(op_c,op_c),X1)),
inference(step,[status(thm)],[t19628,t12063]) ).
cnf(t19630,plain,
mult(op_c,mult(op_c,mult(op_d,X1))) = mult(op_d,ld(mult(op_c,op_c),X1)),
inference(step,[status(thm)],[t19629,t11]) ).
cnf(t19631,plain,
mult(op_c,mult(op_c,mult(op_d,X1))) = mult(op_d,ld(op_c,ld(op_c,X1))),
inference(step,[status(thm)],[t19630,t337]) ).
cnf(t19632,plain,
mult(op_c,mult(op_c,mult(op_d,X1))) = mult(op_d,mult(op_c,mult(op_c,X1))),
inference(step,[status(thm)],[t19631,t347]) ).
cnf(t12454,plain,
mult(op_c,mult(op_c,mult(op_d,X1))) = mult(op_d,mult(op_c,mult(op_c,X1))),
inference(orient,[status(thm)],[t19632]) ).
cnf(t12517,plain,
mult(op_c,mult(op_c,mult(op_c,mult(op_d,mult(op_c,mult(op_c,mult(op_c,X1))))))) = mult(mult(op_c,mult(op_d,mult(op_c,mult(op_c,mult(op_c,mult(op_c,op_c)))))),X1),
inference(cp,[status(thm)],[t9423,t12454]) ).
cnf(t19663,plain,
ld(op_c,mult(op_d,mult(op_c,mult(op_c,mult(op_c,X1))))) = mult(mult(op_c,mult(op_d,mult(op_c,mult(op_c,mult(op_c,mult(op_c,op_c)))))),X1),
inference(step,[status(thm)],[t12517,t383]) ).
cnf(t19664,plain,
ld(op_c,mult(op_d,ld(op_c,X1))) = mult(mult(op_c,mult(op_d,mult(op_c,mult(op_c,mult(op_c,mult(op_c,op_c)))))),X1),
inference(step,[status(thm)],[t19663,t383]) ).
cnf(t103,plain,
mult(i(X1),mult(X2,mult(i(X1),X3))) = mult(ld(X1,mult(X2,i(X1))),X3),
inference(cp,[status(thm)],[t33,t98]) ).
cnf(t19394,plain,
ld(X1,mult(X2,mult(i(X1),X3))) = mult(ld(X1,mult(X2,i(X1))),X3),
inference(step,[status(thm)],[t103,t98]) ).
cnf(t19395,plain,
ld(X1,mult(X2,ld(X1,X3))) = mult(ld(X1,mult(X2,i(X1))),X3),
inference(step,[status(thm)],[t19394,t98]) ).
cnf(t1372,plain,
mult(ld(X1,mult(X2,i(X1))),X3) = ld(X1,mult(X2,ld(X1,X3))),
inference(orient,[status(thm)],[t19395]) ).
cnf(t300,plain,
ld(mult(X1,ld(X2,X3)),Y3) = mult(ld(X1,mult(X2,i(X3))),Y3),
inference(cp,[status(thm)],[t293,t120]) ).
cnf(t1528,plain,
mult(ld(X1,mult(X2,i(X3))),Y3) = ld(mult(X1,ld(X2,X3)),Y3),
inference(orient,[status(thm)],[t300]) ).
cnf(t19396,plain,
ld(mult(X1,ld(X2,X1)),X3) = ld(X1,mult(X2,ld(X1,X3))),
inference(step,[status(thm)],[t1372,t1528]) ).
cnf(t1576,plain,
ld(mult(X1,ld(X2,X1)),X3) = ld(X1,mult(X2,ld(X1,X3))),
inference(rw,[status(thm)],[t19396]) ).
cnf(t1577,plain,
ld(mult(X1,ld(X2,X1)),X3) = ld(X1,mult(X2,ld(X1,X3))),
inference(orient,[status(thm)],[t1576]) ).
cnf(t19420,plain,
ld(rd(X1,ld(X1,X2)),X3) = ld(X1,mult(X2,ld(X1,X3))),
inference(step,[status(thm)],[t1577,t3578]) ).
cnf(t19421,plain,
mult(rd(ld(X1,X2),X1),X3) = ld(X1,mult(X2,ld(X1,X3))),
inference(step,[status(thm)],[t19420,t210]) ).
cnf(t3633,plain,
mult(rd(ld(X1,X2),X1),X3) = ld(X1,mult(X2,ld(X1,X3))),
inference(rw,[status(thm)],[t19421]) ).
cnf(t5328,plain,
ld(X1,mult(X2,ld(X1,X3))) = mult(rd(ld(X1,X2),X1),X3),
inference(orient,[status(thm)],[t3633]) ).
cnf(t19665,plain,
mult(rd(ld(op_c,op_d),op_c),X1) = mult(mult(op_c,mult(op_d,mult(op_c,mult(op_c,mult(op_c,mult(op_c,op_c)))))),X1),
inference(step,[status(thm)],[t19664,t5328]) ).
cnf(t19666,plain,
mult(rd(ld(op_c,op_d),op_c),X1) = mult(mult(op_c,mult(op_d,ld(op_c,mult(op_c,op_c)))),X1),
inference(step,[status(thm)],[t19665,t383]) ).
cnf(t19667,plain,
mult(rd(ld(op_c,op_d),op_c),X1) = mult(mult(op_c,mult(op_d,op_c)),X1),
inference(step,[status(thm)],[t19666,t28]) ).
cnf(t19668,plain,
mult(rd(ld(op_c,op_d),op_c),X1) = mult(op_c,mult(op_d,mult(op_c,X1))),
inference(step,[status(thm)],[t19667,t33]) ).
cnf(t13247,plain,
mult(rd(ld(op_c,op_d),op_c),X1) = mult(op_c,mult(op_d,mult(op_c,X1))),
inference(orient,[status(thm)],[t19668]) ).
cnf(t13273,plain,
ld(rd(ld(op_c,op_d),op_c),ld(rd(ld(op_c,op_d),op_c),X1)) = ld(mult(op_c,mult(op_d,mult(op_c,rd(ld(op_c,op_d),op_c)))),X1),
inference(cp,[status(thm)],[t337,t13247]) ).
cnf(t19673,plain,
mult(rd(op_c,ld(op_c,op_d)),ld(rd(ld(op_c,op_d),op_c),X1)) = ld(mult(op_c,mult(op_d,mult(op_c,rd(ld(op_c,op_d),op_c)))),X1),
inference(step,[status(thm)],[t13273,t210]) ).
cnf(t104,plain,
mult(X1,mult(i(X2),mult(X1,X3))) = mult(mult(X1,ld(X2,X1)),X3),
inference(cp,[status(thm)],[t33,t98]) ).
cnf(t19373,plain,
mult(X1,ld(X2,mult(X1,X3))) = mult(mult(X1,ld(X2,X1)),X3),
inference(step,[status(thm)],[t104,t98]) ).
cnf(t760,plain,
mult(mult(X1,ld(X2,X1)),X3) = mult(X1,ld(X2,mult(X1,X3))),
inference(orient,[status(thm)],[t19373]) ).
cnf(t19422,plain,
mult(rd(X1,ld(X1,X2)),X3) = mult(X1,ld(X2,mult(X1,X3))),
inference(step,[status(thm)],[t760,t3578]) ).
cnf(t3634,plain,
mult(rd(X1,ld(X1,X2)),X3) = mult(X1,ld(X2,mult(X1,X3))),
inference(rw,[status(thm)],[t19422]) ).
cnf(t5427,plain,
mult(rd(X1,ld(X1,X2)),X3) = mult(X1,ld(X2,mult(X1,X3))),
inference(orient,[status(thm)],[t3634]) ).
cnf(t19674,plain,
mult(op_c,ld(op_d,mult(op_c,ld(rd(ld(op_c,op_d),op_c),X1)))) = ld(mult(op_c,mult(op_d,mult(op_c,rd(ld(op_c,op_d),op_c)))),X1),
inference(step,[status(thm)],[t19673,t5427]) ).
cnf(t19675,plain,
mult(op_c,ld(op_d,mult(op_c,mult(rd(op_c,ld(op_c,op_d)),X1)))) = ld(mult(op_c,mult(op_d,mult(op_c,rd(ld(op_c,op_d),op_c)))),X1),
inference(step,[status(thm)],[t19674,t210]) ).
cnf(t19676,plain,
mult(op_c,ld(op_d,mult(op_c,mult(op_c,ld(op_d,mult(op_c,X1)))))) = ld(mult(op_c,mult(op_d,mult(op_c,rd(ld(op_c,op_d),op_c)))),X1),
inference(step,[status(thm)],[t19675,t5427]) ).
cnf(t11733,plain,
i(op_d) = rd(mult(op_c,op_c),rd(op_d,mult(op_c,op_c))),
inference(cp,[status(thm)],[t135,t11720]) ).
cnf(t12359,plain,
rd(mult(op_c,op_c),rd(op_d,mult(op_c,op_c))) = i(op_d),
inference(orient,[status(thm)],[t11733]) ).
cnf(t12360,plain,
mult(mult(op_c,op_c),ld(mult(mult(op_c,op_c),rd(op_d,mult(op_c,op_c))),X1)) = mult(i(op_d),ld(mult(op_c,op_c),X1)),
inference(cp,[status(thm)],[t10091,t12359]) ).
cnf(t19653,plain,
mult(op_c,mult(op_c,ld(mult(mult(op_c,op_c),rd(op_d,mult(op_c,op_c))),X1))) = mult(i(op_d),ld(mult(op_c,op_c),X1)),
inference(step,[status(thm)],[t12360,t188]) ).
cnf(t19654,plain,
mult(op_c,mult(op_c,mult(ld(mult(op_c,op_c),rd(mult(op_c,op_c),op_d)),X1))) = mult(i(op_d),ld(mult(op_c,op_c),X1)),
inference(step,[status(thm)],[t19653,t861]) ).
cnf(t19655,plain,
mult(op_c,mult(op_c,mult(ld(op_c,ld(op_c,rd(mult(op_c,op_c),op_d))),X1))) = mult(i(op_d),ld(mult(op_c,op_c),X1)),
inference(step,[status(thm)],[t19654,t337]) ).
cnf(t19656,plain,
mult(op_c,mult(op_c,mult(mult(op_c,mult(op_c,rd(mult(op_c,op_c),op_d))),X1))) = mult(i(op_d),ld(mult(op_c,op_c),X1)),
inference(step,[status(thm)],[t19655,t347]) ).
cnf(t11915,plain,
ld(op_c,i(op_d)) = mult(op_c,rd(mult(op_c,op_c),op_d)),
inference(cp,[status(thm)],[t383,t11877]) ).
cnf(t12129,plain,
mult(op_c,rd(mult(op_c,op_c),op_d)) = ld(op_c,i(op_d)),
inference(orient,[status(thm)],[t11915]) ).
cnf(t19657,plain,
mult(op_c,mult(op_c,mult(mult(op_c,ld(op_c,i(op_d))),X1))) = mult(i(op_d),ld(mult(op_c,op_c),X1)),
inference(step,[status(thm)],[t19656,t12129]) ).
cnf(t19658,plain,
mult(op_c,mult(op_c,mult(i(op_d),X1))) = mult(i(op_d),ld(mult(op_c,op_c),X1)),
inference(step,[status(thm)],[t19657,t11]) ).
cnf(t19659,plain,
mult(op_c,mult(op_c,ld(op_d,X1))) = mult(i(op_d),ld(mult(op_c,op_c),X1)),
inference(step,[status(thm)],[t19658,t98]) ).
cnf(t19660,plain,
mult(op_c,mult(op_c,ld(op_d,X1))) = ld(op_d,ld(mult(op_c,op_c),X1)),
inference(step,[status(thm)],[t19659,t98]) ).
cnf(t19661,plain,
mult(op_c,mult(op_c,ld(op_d,X1))) = ld(op_d,ld(op_c,ld(op_c,X1))),
inference(step,[status(thm)],[t19660,t337]) ).
cnf(t19662,plain,
mult(op_c,mult(op_c,ld(op_d,X1))) = ld(op_d,mult(op_c,mult(op_c,X1))),
inference(step,[status(thm)],[t19661,t347]) ).
cnf(t13178,plain,
ld(op_d,mult(op_c,mult(op_c,X1))) = mult(op_c,mult(op_c,ld(op_d,X1))),
inference(orient,[status(thm)],[t19662]) ).
cnf(t19677,plain,
mult(op_c,mult(op_c,mult(op_c,ld(op_d,ld(op_d,mult(op_c,X1)))))) = ld(mult(op_c,mult(op_d,mult(op_c,rd(ld(op_c,op_d),op_c)))),X1),
inference(step,[status(thm)],[t19676,t13178]) ).
cnf(t19678,plain,
ld(op_c,ld(op_d,ld(op_d,mult(op_c,X1)))) = ld(mult(op_c,mult(op_d,mult(op_c,rd(ld(op_c,op_d),op_c)))),X1),
inference(step,[status(thm)],[t19677,t383]) ).
cnf(t19679,plain,
ld(op_c,mult(op_d,mult(op_c,X1))) = ld(mult(op_c,mult(op_d,mult(op_c,rd(ld(op_c,op_d),op_c)))),X1),
inference(step,[status(thm)],[t19678,t207]) ).
cnf(t3224,plain,
mult(X1,rd(ld(X1,X2),X1)) = mult(X2,i(X1)),
inference(cp,[status(thm)],[t3217,t11]) ).
cnf(t4065,plain,
mult(X1,rd(ld(X1,X2),X1)) = mult(X2,i(X1)),
inference(orient,[status(thm)],[t3224]) ).
cnf(t19680,plain,
ld(op_c,mult(op_d,mult(op_c,X1))) = ld(mult(op_c,mult(op_d,mult(op_d,i(op_c)))),X1),
inference(step,[status(thm)],[t19679,t4065]) ).
cnf(t19681,plain,
ld(op_c,mult(op_d,mult(op_c,X1))) = ld(mult(op_c,ld(op_d,i(op_c))),X1),
inference(step,[status(thm)],[t19680,t200]) ).
cnf(t3723,plain,
mult(op_c,mult(op_c,mult(X1,i(op_c)))) = ld(op_c,rd(ld(op_c,X1),op_c)),
inference(cp,[status(thm)],[t347,t3686]) ).
cnf(t8715,plain,
mult(op_c,mult(op_c,mult(X1,i(op_c)))) = ld(op_c,rd(ld(op_c,X1),op_c)),
inference(orient,[status(thm)],[t3723]) ).
cnf(t12455,plain,
mult(op_d,mult(op_c,mult(op_c,i(op_c)))) = ld(op_c,rd(ld(op_c,op_d),op_c)),
inference(cp,[status(thm)],[t12454,t8715]) ).
cnf(t19633,plain,
mult(op_d,mult(op_c,unit)) = ld(op_c,rd(ld(op_c,op_d),op_c)),
inference(step,[status(thm)],[t12455,t96]) ).
cnf(t19634,plain,
mult(op_d,op_c) = ld(op_c,rd(ld(op_c,op_d),op_c)),
inference(step,[status(thm)],[t19633,t12]) ).
cnf(t12520,plain,
ld(op_c,rd(ld(op_c,op_d),op_c)) = mult(op_d,op_c),
inference(orient,[status(thm)],[t19634]) ).
cnf(t12529,plain,
mult(op_c,mult(op_c,rd(ld(op_c,op_d),op_c))) = ld(op_c,mult(op_d,op_c)),
inference(cp,[status(thm)],[t347,t12520]) ).
cnf(t19636,plain,
mult(op_c,mult(op_d,i(op_c))) = ld(op_c,mult(op_d,op_c)),
inference(step,[status(thm)],[t12529,t4065]) ).
cnf(t12865,plain,
mult(op_c,mult(op_d,i(op_c))) = ld(op_c,mult(op_d,op_c)),
inference(orient,[status(thm)],[t19636]) ).
cnf(t12876,plain,
ld(op_c,i(mult(op_d,i(op_c)))) = i(ld(op_c,mult(op_d,op_c))),
inference(cp,[status(thm)],[t110,t12865]) ).
cnf(t19640,plain,
ld(op_c,ld(op_d,i(i(op_c)))) = i(ld(op_c,mult(op_d,op_c))),
inference(step,[status(thm)],[t12876,t110]) ).
cnf(t19641,plain,
ld(op_c,ld(op_d,op_c)) = i(ld(op_c,mult(op_d,op_c))),
inference(step,[status(thm)],[t19640,t81]) ).
cnf(t19642,plain,
ld(op_c,ld(op_d,op_c)) = mult(op_c,i(mult(op_d,op_c))),
inference(step,[status(thm)],[t19641,t120]) ).
cnf(t19643,plain,
ld(op_c,ld(op_d,op_c)) = mult(op_c,ld(op_d,i(op_c))),
inference(step,[status(thm)],[t19642,t110]) ).
cnf(t12954,plain,
mult(op_c,ld(op_d,i(op_c))) = ld(op_c,ld(op_d,op_c)),
inference(orient,[status(thm)],[t19643]) ).
cnf(t19682,plain,
ld(op_c,mult(op_d,mult(op_c,X1))) = ld(ld(op_c,ld(op_d,op_c)),X1),
inference(step,[status(thm)],[t19681,t12954]) ).
cnf(t328,plain,
ld(ld(X1,ld(X2,X3)),Y3) = mult(mult(X1,mult(X2,i(X3))),Y3),
inference(cp,[status(thm)],[t322,t120]) ).
cnf(t1901,plain,
mult(mult(X1,mult(X2,i(X3))),Y3) = ld(ld(X1,ld(X2,X3)),Y3),
inference(orient,[status(thm)],[t328]) ).
cnf(t12899,plain,
ld(ld(op_c,ld(op_d,op_c)),X1) = mult(ld(op_c,mult(op_d,op_c)),X1),
inference(cp,[status(thm)],[t1901,t12865]) ).
cnf(t13504,plain,
ld(ld(op_c,ld(op_d,op_c)),X1) = mult(ld(op_c,mult(op_d,op_c)),X1),
inference(orient,[status(thm)],[t12899]) ).
cnf(t19683,plain,
ld(op_c,mult(op_d,mult(op_c,X1))) = mult(ld(op_c,mult(op_d,op_c)),X1),
inference(step,[status(thm)],[t19682,t13504]) ).
cnf(t13683,plain,
ld(op_c,mult(op_d,mult(op_c,X1))) = mult(ld(op_c,mult(op_d,op_c)),X1),
inference(orient,[status(thm)],[t19683]) ).
cnf(t13684,plain,
mult(ld(op_c,mult(op_d,op_c)),op_c) = ld(op_c,rd(op_d,mult(op_c,op_c))),
inference(cp,[status(thm)],[t13683,t11720]) ).
cnf(t11936,plain,
mult(op_c,op_d) = ld(op_c,rd(op_d,mult(op_c,op_c))),
inference(cp,[status(thm)],[t28,t11925]) ).
cnf(t12020,plain,
ld(op_c,rd(op_d,mult(op_c,op_c))) = mult(op_c,op_d),
inference(orient,[status(thm)],[t11936]) ).
cnf(t19684,plain,
mult(ld(op_c,mult(op_d,op_c)),op_c) = mult(op_c,op_d),
inference(step,[status(thm)],[t13684,t12020]) ).
cnf(t13762,plain,
mult(ld(op_c,mult(op_d,op_c)),op_c) = mult(op_c,op_d),
inference(orient,[status(thm)],[t19684]) ).
cnf(t13775,plain,
ld(op_c,mult(op_d,op_c)) = rd(mult(op_c,op_d),op_c),
inference(cp,[status(thm)],[t23,t13762]) ).
cnf(t13851,plain,
ld(op_c,mult(op_d,op_c)) = rd(mult(op_c,op_d),op_c),
inference(orient,[status(thm)],[t13775]) ).
cnf(t13864,plain,
mult(op_c,mult(op_c,mult(op_d,op_c))) = ld(op_c,rd(mult(op_c,op_d),op_c)),
inference(cp,[status(thm)],[t347,t13851]) ).
cnf(t19710,plain,
mult(op_d,mult(op_c,mult(op_c,op_c))) = ld(op_c,rd(mult(op_c,op_d),op_c)),
inference(step,[status(thm)],[t13864,t12454]) ).
cnf(t19711,plain,
mult(op_d,i(op_c)) = ld(op_c,rd(mult(op_c,op_d),op_c)),
inference(step,[status(thm)],[t19710,t138]) ).
cnf(t14094,plain,
ld(op_c,rd(mult(op_c,op_d),op_c)) = mult(op_d,i(op_c)),
inference(orient,[status(thm)],[t19711]) ).
cnf(t14105,plain,
rd(ld(op_c,mult(op_c,op_d)),mult(op_c,op_c)) = rd(mult(op_d,i(op_c)),op_c),
inference(cp,[status(thm)],[t7875,t14094]) ).
cnf(t19712,plain,
rd(op_d,mult(op_c,op_c)) = rd(mult(op_d,i(op_c)),op_c),
inference(step,[status(thm)],[t14105,t28]) ).
cnf(t351,plain,
op_c = rd(ld(op_c,X1),mult(op_c,mult(op_c,X1))),
inference(cp,[status(thm)],[t107,t347]) ).
cnf(t750,plain,
rd(ld(op_c,X1),mult(op_c,mult(op_c,X1))) = op_c,
inference(orient,[status(thm)],[t351]) ).
cnf(t2072,plain,
rd(rd(mult(op_c,mult(op_c,X1)),ld(op_c,X1)),ld(X2,X3)) = rd(mult(X2,i(X3)),op_c),
inference(cp,[status(thm)],[t2052,t750]) ).
cnf(t350,plain,
i(op_c) = rd(mult(op_c,mult(op_c,X1)),ld(op_c,X1)),
inference(cp,[status(thm)],[t125,t347]) ).
cnf(t886,plain,
rd(mult(op_c,mult(op_c,X1)),ld(op_c,X1)) = i(op_c),
inference(orient,[status(thm)],[t350]) ).
cnf(t19400,plain,
rd(i(op_c),ld(X2,X3)) = rd(mult(X2,i(X3)),op_c),
inference(step,[status(thm)],[t2072,t886]) ).
cnf(t2087,plain,
rd(mult(X1,i(X2)),op_c) = rd(i(op_c),ld(X1,X2)),
inference(orient,[status(thm)],[t19400]) ).
cnf(t19713,plain,
rd(op_d,mult(op_c,op_c)) = rd(i(op_c),ld(op_d,op_c)),
inference(step,[status(thm)],[t19712,t2087]) ).
cnf(t14127,plain,
rd(i(op_c),ld(op_d,op_c)) = rd(op_d,mult(op_c,op_c)),
inference(orient,[status(thm)],[t19713]) ).
cnf(t14141,plain,
rd(ld(op_d,op_c),i(op_c)) = i(rd(op_d,mult(op_c,op_c))),
inference(cp,[status(thm)],[t130,t14127]) ).
cnf(t19714,plain,
rd(op_c,i(ld(op_d,op_c))) = i(rd(op_d,mult(op_c,op_c))),
inference(step,[status(thm)],[t14141,t256]) ).
cnf(t19715,plain,
rd(op_c,mult(op_d,i(op_c))) = i(rd(op_d,mult(op_c,op_c))),
inference(step,[status(thm)],[t19714,t120]) ).
cnf(t19716,plain,
rd(op_c,mult(op_d,i(op_c))) = rd(mult(op_c,op_c),op_d),
inference(step,[status(thm)],[t19715,t130]) ).
cnf(t14180,plain,
rd(op_c,mult(op_d,i(op_c))) = rd(mult(op_c,op_c),op_d),
inference(orient,[status(thm)],[t19716]) ).
cnf(t14187,plain,
i(mult(op_d,i(op_c))) = mult(rd(mult(op_c,op_c),op_d),i(op_c)),
inference(cp,[status(thm)],[t168,t14180]) ).
cnf(t19740,plain,
ld(op_d,i(i(op_c))) = mult(rd(mult(op_c,op_c),op_d),i(op_c)),
inference(step,[status(thm)],[t14187,t110]) ).
cnf(t19741,plain,
ld(op_d,op_c) = mult(rd(mult(op_c,op_c),op_d),i(op_c)),
inference(step,[status(thm)],[t19740,t81]) ).
cnf(t14399,plain,
mult(rd(mult(op_c,op_c),op_d),i(op_c)) = ld(op_d,op_c),
inference(orient,[status(thm)],[t19741]) ).
cnf(t18946,plain,
mult(rd(mult(op_c,op_c),op_d),mult(i(op_c),mult(i(op_c),rd(mult(op_c,op_c),op_d)))) = mult(ld(op_d,op_c),mult(rd(mult(op_c,op_c),op_d),i(op_c))),
inference(cp,[status(thm)],[t18885,t14399]) ).
cnf(t19836,plain,
mult(rd(mult(op_c,op_c),op_d),ld(op_c,mult(i(op_c),rd(mult(op_c,op_c),op_d)))) = mult(ld(op_d,op_c),mult(rd(mult(op_c,op_c),op_d),i(op_c))),
inference(step,[status(thm)],[t18946,t98]) ).
cnf(t19837,plain,
mult(rd(mult(op_c,op_c),op_d),ld(op_c,ld(op_c,rd(mult(op_c,op_c),op_d)))) = mult(ld(op_d,op_c),mult(rd(mult(op_c,op_c),op_d),i(op_c))),
inference(step,[status(thm)],[t19836,t98]) ).
cnf(t11889,plain,
mult(op_c,i(op_d)) = ld(op_c,rd(mult(op_c,op_c),op_d)),
inference(cp,[status(thm)],[t28,t11877]) ).
cnf(t12094,plain,
ld(op_c,rd(mult(op_c,op_c),op_d)) = mult(op_c,i(op_d)),
inference(orient,[status(thm)],[t11889]) ).
cnf(t19838,plain,
mult(rd(mult(op_c,op_c),op_d),ld(op_c,mult(op_c,i(op_d)))) = mult(ld(op_d,op_c),mult(rd(mult(op_c,op_c),op_d),i(op_c))),
inference(step,[status(thm)],[t19837,t12094]) ).
cnf(t19839,plain,
mult(rd(mult(op_c,op_c),op_d),i(op_d)) = mult(ld(op_d,op_c),mult(rd(mult(op_c,op_c),op_d),i(op_c))),
inference(step,[status(thm)],[t19838,t28]) ).
cnf(t11623,plain,
ld(mult(op_d,mult(op_c,op_c)),i(op_d)) = ld(op_d,mult(op_d,mult(op_d,mult(op_c,op_c)))),
inference(cp,[status(thm)],[t5980,t11589]) ).
cnf(t19759,plain,
mult(ld(op_d,mult(op_c,op_c)),i(op_d)) = ld(op_d,mult(op_d,mult(op_d,mult(op_c,op_c)))),
inference(step,[status(thm)],[t11623,t1122]) ).
cnf(t19760,plain,
mult(rd(mult(op_c,op_c),op_d),i(op_d)) = ld(op_d,mult(op_d,mult(op_d,mult(op_c,op_c)))),
inference(step,[status(thm)],[t19759,t11765]) ).
cnf(t19761,plain,
mult(rd(mult(op_c,op_c),op_d),i(op_d)) = mult(op_d,mult(op_c,op_c)),
inference(step,[status(thm)],[t19760,t28]) ).
cnf(t19762,plain,
mult(rd(mult(op_c,op_c),op_d),i(op_d)) = rd(op_d,mult(op_c,op_c)),
inference(step,[status(thm)],[t19761,t11720]) ).
cnf(t14667,plain,
mult(rd(mult(op_c,op_c),op_d),i(op_d)) = rd(op_d,mult(op_c,op_c)),
inference(orient,[status(thm)],[t19762]) ).
cnf(t19840,plain,
rd(op_d,mult(op_c,op_c)) = mult(ld(op_d,op_c),mult(rd(mult(op_c,op_c),op_d),i(op_c))),
inference(step,[status(thm)],[t19839,t14667]) ).
cnf(t19841,plain,
rd(op_d,mult(op_c,op_c)) = mult(ld(op_d,op_c),ld(op_d,op_c)),
inference(step,[status(thm)],[t19840,t14399]) ).
cnf(t19157,plain,
mult(ld(op_d,op_c),ld(op_d,op_c)) = rd(op_d,mult(op_c,op_c)),
inference(orient,[status(thm)],[t19841]) ).
cnf(t19176,plain,
mult(ld(op_d,op_c),rd(ld(op_d,op_c),rd(ld(op_d,op_c),ld(op_d,op_c)))) = mult(mult(rd(op_d,mult(op_c,op_c)),ld(op_d,op_c)),i(ld(op_d,op_c))),
inference(cp,[status(thm)],[t10721,t19157]) ).
cnf(t19842,plain,
mult(ld(op_d,op_c),rd(ld(op_d,op_c),unit)) = mult(mult(rd(op_d,mult(op_c,op_c)),ld(op_d,op_c)),i(ld(op_d,op_c))),
inference(step,[status(thm)],[t19176,t61]) ).
cnf(t19843,plain,
mult(ld(op_d,op_c),ld(op_d,op_c)) = mult(mult(rd(op_d,mult(op_c,op_c)),ld(op_d,op_c)),i(ld(op_d,op_c))),
inference(step,[status(thm)],[t19842,t60]) ).
cnf(t19844,plain,
rd(op_d,mult(op_c,op_c)) = mult(mult(rd(op_d,mult(op_c,op_c)),ld(op_d,op_c)),i(ld(op_d,op_c))),
inference(step,[status(thm)],[t19843,t19157]) ).
cnf(t19845,plain,
rd(op_d,mult(op_c,op_c)) = mult(mult(op_d,ld(mult(op_d,mult(op_c,op_c)),op_c)),i(ld(op_d,op_c))),
inference(step,[status(thm)],[t19844,t10091]) ).
cnf(t19846,plain,
rd(op_d,mult(op_c,op_c)) = mult(mult(op_d,mult(ld(op_d,mult(op_c,op_c)),op_c)),i(ld(op_d,op_c))),
inference(step,[status(thm)],[t19845,t1122]) ).
cnf(t19847,plain,
rd(op_d,mult(op_c,op_c)) = mult(mult(op_d,mult(rd(mult(op_c,op_c),op_d),op_c)),i(ld(op_d,op_c))),
inference(step,[status(thm)],[t19846,t11765]) ).
cnf(t13772,plain,
i(ld(op_c,mult(op_d,op_c))) = rd(op_c,mult(op_c,op_d)),
inference(cp,[status(thm)],[t135,t13762]) ).
cnf(t19685,plain,
mult(op_c,i(mult(op_d,op_c))) = rd(op_c,mult(op_c,op_d)),
inference(step,[status(thm)],[t13772,t120]) ).
cnf(t19686,plain,
mult(op_c,ld(op_d,i(op_c))) = rd(op_c,mult(op_c,op_d)),
inference(step,[status(thm)],[t19685,t110]) ).
cnf(t19687,plain,
ld(op_c,ld(op_d,op_c)) = rd(op_c,mult(op_c,op_d)),
inference(step,[status(thm)],[t19686,t12954]) ).
cnf(t13801,plain,
ld(op_c,ld(op_d,op_c)) = rd(op_c,mult(op_c,op_d)),
inference(orient,[status(thm)],[t19687]) ).
cnf(t13814,plain,
mult(op_c,mult(op_c,ld(op_d,op_c))) = ld(op_c,rd(op_c,mult(op_c,op_d))),
inference(cp,[status(thm)],[t347,t13801]) ).
cnf(t19705,plain,
mult(op_c,rd(op_c,ld(op_c,op_d))) = ld(op_c,rd(op_c,mult(op_c,op_d))),
inference(step,[status(thm)],[t13814,t3578]) ).
cnf(t12531,plain,
mult(op_c,i(rd(ld(op_c,op_d),op_c))) = i(mult(op_d,op_c)),
inference(cp,[status(thm)],[t120,t12520]) ).
cnf(t19644,plain,
mult(op_c,rd(op_c,ld(op_c,op_d))) = i(mult(op_d,op_c)),
inference(step,[status(thm)],[t12531,t130]) ).
cnf(t19645,plain,
mult(op_c,rd(op_c,ld(op_c,op_d))) = ld(op_d,i(op_c)),
inference(step,[status(thm)],[t19644,t110]) ).
cnf(t12991,plain,
mult(op_c,rd(op_c,ld(op_c,op_d))) = ld(op_d,i(op_c)),
inference(orient,[status(thm)],[t19645]) ).
cnf(t19706,plain,
ld(op_d,i(op_c)) = ld(op_c,rd(op_c,mult(op_c,op_d))),
inference(step,[status(thm)],[t19705,t12991]) ).
cnf(t11931,plain,
ld(op_c,rd(op_c,mult(op_c,op_d))) = ld(rd(op_d,mult(op_c,op_c)),op_c),
inference(cp,[status(thm)],[t3297,t11925]) ).
cnf(t19624,plain,
ld(op_c,rd(op_c,mult(op_c,op_d))) = mult(rd(mult(op_c,op_c),op_d),op_c),
inference(step,[status(thm)],[t11931,t210]) ).
cnf(t12414,plain,
ld(op_c,rd(op_c,mult(op_c,op_d))) = mult(rd(mult(op_c,op_c),op_d),op_c),
inference(orient,[status(thm)],[t19624]) ).
cnf(t19707,plain,
ld(op_d,i(op_c)) = mult(rd(mult(op_c,op_c),op_d),op_c),
inference(step,[status(thm)],[t19706,t12414]) ).
cnf(t14061,plain,
mult(rd(mult(op_c,op_c),op_d),op_c) = ld(op_d,i(op_c)),
inference(orient,[status(thm)],[t19707]) ).
cnf(t19848,plain,
rd(op_d,mult(op_c,op_c)) = mult(mult(op_d,ld(op_d,i(op_c))),i(ld(op_d,op_c))),
inference(step,[status(thm)],[t19847,t14061]) ).
cnf(t19849,plain,
rd(op_d,mult(op_c,op_c)) = mult(i(op_c),i(ld(op_d,op_c))),
inference(step,[status(thm)],[t19848,t11]) ).
cnf(t19850,plain,
rd(op_d,mult(op_c,op_c)) = ld(op_c,i(ld(op_d,op_c))),
inference(step,[status(thm)],[t19849,t98]) ).
cnf(t19851,plain,
rd(op_d,mult(op_c,op_c)) = ld(op_c,mult(op_d,i(op_c))),
inference(step,[status(thm)],[t19850,t120]) ).
cnf(t19852,plain,
rd(op_d,mult(op_c,op_c)) = rd(ld(op_c,op_d),op_c),
inference(step,[status(thm)],[t19851,t3686]) ).
cnf(t19196,plain,
rd(ld(op_c,op_d),op_c) = rd(op_d,mult(op_c,op_c)),
inference(orient,[status(thm)],[t19852]) ).
cnf(t19217,plain,
ld(op_c,mult(op_d,mult(op_c,op_c))) = mult(rd(op_d,mult(op_c,op_c)),i(op_c)),
inference(cp,[status(thm)],[t16782,t19196]) ).
cnf(t19696,plain,
ld(op_c,mult(op_d,mult(op_c,X1))) = mult(rd(mult(op_c,op_d),op_c),X1),
inference(step,[status(thm)],[t13683,t13851]) ).
cnf(t13854,plain,
ld(op_c,mult(op_d,mult(op_c,X1))) = mult(rd(mult(op_c,op_d),op_c),X1),
inference(orient,[status(thm)],[t19696]) ).
cnf(t19860,plain,
mult(rd(mult(op_c,op_d),op_c),op_c) = mult(rd(op_d,mult(op_c,op_c)),i(op_c)),
inference(step,[status(thm)],[t19217,t13854]) ).
cnf(t19861,plain,
mult(op_c,op_d) = mult(rd(op_d,mult(op_c,op_c)),i(op_c)),
inference(step,[status(thm)],[t19860,t20]) ).
cnf(t13884,plain,
rd(mult(op_d,op_c),i(op_c)) = mult(op_c,mult(rd(mult(op_c,op_d),op_c),op_c)),
inference(cp,[status(thm)],[t4191,t13851]) ).
cnf(t19698,plain,
rd(op_c,i(mult(op_d,op_c))) = mult(op_c,mult(rd(mult(op_c,op_d),op_c),op_c)),
inference(step,[status(thm)],[t13884,t256]) ).
cnf(t19699,plain,
rd(op_c,ld(op_d,i(op_c))) = mult(op_c,mult(rd(mult(op_c,op_d),op_c),op_c)),
inference(step,[status(thm)],[t19698,t110]) ).
cnf(t19700,plain,
rd(op_c,ld(op_d,i(op_c))) = rd(op_c,ld(op_c,rd(op_c,mult(op_c,op_d)))),
inference(step,[status(thm)],[t19699,t5177]) ).
cnf(t19701,plain,
rd(op_c,ld(op_d,i(op_c))) = mult(op_c,mult(op_c,op_d)),
inference(step,[status(thm)],[t19700,t3482]) ).
cnf(t19702,plain,
rd(op_c,ld(op_d,i(op_c))) = rd(op_d,mult(op_c,op_c)),
inference(step,[status(thm)],[t19701,t11925]) ).
cnf(t13895,plain,
rd(op_c,ld(op_d,i(op_c))) = rd(op_d,mult(op_c,op_c)),
inference(orient,[status(thm)],[t19702]) ).
cnf(t13908,plain,
i(ld(op_d,i(op_c))) = mult(rd(op_d,mult(op_c,op_c)),i(op_c)),
inference(cp,[status(thm)],[t168,t13895]) ).
cnf(t19738,plain,
mult(op_d,i(i(op_c))) = mult(rd(op_d,mult(op_c,op_c)),i(op_c)),
inference(step,[status(thm)],[t13908,t120]) ).
cnf(t19739,plain,
mult(op_d,op_c) = mult(rd(op_d,mult(op_c,op_c)),i(op_c)),
inference(step,[status(thm)],[t19738,t81]) ).
cnf(t14370,plain,
mult(rd(op_d,mult(op_c,op_c)),i(op_c)) = mult(op_d,op_c),
inference(orient,[status(thm)],[t19739]) ).
cnf(t19862,plain,
mult(op_c,op_d) = mult(op_d,op_c),
inference(step,[status(thm)],[t19861,t14370]) ).
cnf(t19254,plain,
mult(op_c,op_d) = mult(op_d,op_c),
inference(orient,[status(thm)],[t19862]) ).
cnf(goal_0,negated_conjecture,
mult(op_d,op_c) != mult(op_c,op_d),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
mult(op_d,op_c) != mult(op_d,op_c),
inference(rw,[status(thm)],[goal_0,t19254]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP688-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/0.36 % Computer : n014.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Wed Sep 23 15:42:33 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 24.32/3.60 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 24.32/3.60 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------