%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP682-11 : TPTP v9.3.1. Released v8.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n015.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:01 PM UTC 2026
% Result : Unsatisfiable 6.72s 1.39s
% Output : CNFRefutation 6.72s
% Verified :
% SZS Type : Refutation
% Derivation depth : 113
% Number of leaves : 8
% Syntax : Number of clauses : 263 ( 263 unt; 0 nHn; 5 RR)
% Number of literals : 263 ( 262 equ; 4 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 3 con; 0-2 aty)
% Number of variables : 633 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t2,axiom,
mult(X1,ld(X1,X2)) = ld(X1,mult(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t14,plain,
ld(X1,mult(X1,X2)) = mult(X1,ld(X1,X2)),
inference(orient,[status(thm)],[t2]) ).
cnf(t3,axiom,
rd(mult(X1,X2),X2) = mult(rd(X1,X2),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t16,plain,
mult(rd(X1,X2),X2) = rd(mult(X1,X2),X2),
inference(orient,[status(thm)],[t3]) ).
cnf(t5,axiom,
ld(ld(X1,X2),mult(ld(X1,X2),mult(X3,X4))) = mult(ld(X1,mult(X1,X3)),X4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t2590,plain,
mult(ld(X1,X2),ld(ld(X1,X2),mult(X3,X4))) = mult(ld(X1,mult(X1,X3)),X4),
inference(step,[status(thm)],[t5,t14]) ).
cnf(t2591,plain,
mult(ld(X1,X2),ld(ld(X1,X2),mult(X3,X4))) = mult(mult(X1,ld(X1,X3)),X4),
inference(step,[status(thm)],[t2590,t14]) ).
cnf(t21,plain,
mult(ld(X1,X2),ld(ld(X1,X2),mult(X3,X4))) = mult(mult(X1,ld(X1,X3)),X4),
inference(orient,[status(thm)],[t2591]) ).
cnf(t22,plain,
mult(mult(X1,ld(X1,X2)),X3) = mult(mult(X1,ld(X1,X4)),ld(ld(X1,mult(X1,X4)),mult(X2,X3))),
inference(cp,[status(thm)],[t21,t14]) ).
cnf(t2634,plain,
mult(mult(X1,ld(X1,X2)),X3) = mult(mult(X1,ld(X1,X4)),ld(mult(X1,ld(X1,X4)),mult(X2,X3))),
inference(step,[status(thm)],[t22,t14]) ).
cnf(t713,plain,
mult(mult(X1,ld(X1,X2)),ld(mult(X1,ld(X1,X2)),mult(X3,X4))) = mult(mult(X1,ld(X1,X3)),X4),
inference(orient,[status(thm)],[t2634]) ).
cnf(t0,axiom,
ld(X1,mult(X1,X1)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t8,plain,
ld(X1,mult(X1,X1)) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t2589,plain,
mult(X1,ld(X1,X1)) = X1,
inference(step,[status(thm)],[t8,t14]) ).
cnf(t15,plain,
mult(X1,ld(X1,X1)) = X1,
inference(rw,[status(thm)],[t2589]) ).
cnf(t33,plain,
mult(X1,ld(X1,X1)) = X1,
inference(orient,[status(thm)],[t15]) ).
cnf(t35,plain,
mult(X1,ld(X1,ld(X1,X1))) = ld(X1,X1),
inference(cp,[status(thm)],[t14,t33]) ).
cnf(t4,axiom,
rd(mult(rd(X1,X1),X2),X2) = ld(X1,mult(X1,ld(X2,X2))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t2592,plain,
rd(mult(rd(X1,X1),X2),X2) = mult(X1,ld(X1,ld(X2,X2))),
inference(step,[status(thm)],[t4,t14]) ).
cnf(t29,plain,
mult(X1,ld(X1,ld(X2,X2))) = rd(mult(rd(X1,X1),X2),X2),
inference(orient,[status(thm)],[t2592]) ).
cnf(t2593,plain,
rd(mult(rd(X1,X1),X1),X1) = ld(X1,X1),
inference(step,[status(thm)],[t35,t29]) ).
cnf(t2594,plain,
rd(rd(mult(X1,X1),X1),X1) = ld(X1,X1),
inference(step,[status(thm)],[t2593,t16]) ).
cnf(t1,axiom,
rd(mult(X1,X1),X1) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t7,plain,
rd(mult(X1,X1),X1) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t2595,plain,
rd(X1,X1) = ld(X1,X1),
inference(step,[status(thm)],[t2594,t7]) ).
cnf(t38,plain,
ld(X1,X1) = rd(X1,X1),
inference(orient,[status(thm)],[t2595]) ).
cnf(t717,plain,
mult(mult(X1,ld(X1,X2)),X3) = mult(mult(X1,rd(X1,X1)),ld(mult(X1,ld(X1,X1)),mult(X2,X3))),
inference(cp,[status(thm)],[t713,t38]) ).
cnf(t2596,plain,
mult(X1,rd(X1,X1)) = X1,
inference(step,[status(thm)],[t33,t38]) ).
cnf(t41,plain,
mult(X1,rd(X1,X1)) = X1,
inference(rw,[status(thm)],[t2596]) ).
cnf(t43,plain,
mult(X1,rd(X1,X1)) = X1,
inference(orient,[status(thm)],[t41]) ).
cnf(t2635,plain,
mult(mult(X1,ld(X1,X2)),X3) = mult(X1,ld(mult(X1,ld(X1,X1)),mult(X2,X3))),
inference(step,[status(thm)],[t717,t43]) ).
cnf(t2636,plain,
mult(mult(X1,ld(X1,X2)),X3) = mult(X1,ld(mult(X1,rd(X1,X1)),mult(X2,X3))),
inference(step,[status(thm)],[t2635,t38]) ).
cnf(t2637,plain,
mult(mult(X1,ld(X1,X2)),X3) = mult(X1,ld(X1,mult(X2,X3))),
inference(step,[status(thm)],[t2636,t43]) ).
cnf(t769,plain,
mult(mult(X1,ld(X1,X2)),X3) = mult(X1,ld(X1,mult(X2,X3))),
inference(orient,[status(thm)],[t2637]) ).
cnf(t782,plain,
mult(X1,ld(X1,mult(X1,X2))) = mult(mult(X1,rd(X1,X1)),X2),
inference(cp,[status(thm)],[t769,t38]) ).
cnf(t2644,plain,
mult(X1,mult(X1,ld(X1,X2))) = mult(mult(X1,rd(X1,X1)),X2),
inference(step,[status(thm)],[t782,t14]) ).
cnf(t2645,plain,
mult(X1,mult(X1,ld(X1,X2))) = mult(X1,X2),
inference(step,[status(thm)],[t2644,t43]) ).
cnf(t822,plain,
mult(X1,mult(X1,ld(X1,X2))) = mult(X1,X2),
inference(orient,[status(thm)],[t2645]) ).
cnf(t2597,plain,
mult(X1,ld(X1,rd(X2,X2))) = rd(mult(rd(X1,X1),X2),X2),
inference(step,[status(thm)],[t29,t38]) ).
cnf(t42,plain,
mult(X1,ld(X1,rd(X2,X2))) = rd(mult(rd(X1,X1),X2),X2),
inference(rw,[status(thm)],[t2597]) ).
cnf(t86,plain,
mult(X1,ld(X1,rd(X2,X2))) = rd(mult(rd(X1,X1),X2),X2),
inference(orient,[status(thm)],[t42]) ).
cnf(t6,axiom,
rd(mult(mult(X1,X2),rd(X3,X4)),rd(X3,X4)) = mult(X1,rd(mult(X2,X4),X4)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t9,plain,
rd(mult(mult(X1,X2),rd(X3,X4)),rd(X3,X4)) = mult(X1,rd(mult(X2,X4),X4)),
inference(orient,[status(thm)],[t6]) ).
cnf(t10,plain,
mult(X1,rd(mult(X2,X3),X3)) = rd(mult(mult(X1,X2),X3),rd(mult(X3,X3),X3)),
inference(cp,[status(thm)],[t9,t7]) ).
cnf(t2599,plain,
mult(X1,rd(mult(X2,X3),X3)) = rd(mult(mult(X1,X2),X3),X3),
inference(step,[status(thm)],[t10,t7]) ).
cnf(t57,plain,
mult(X1,rd(mult(X2,X3),X3)) = rd(mult(mult(X1,X2),X3),X3),
inference(orient,[status(thm)],[t2599]) ).
cnf(t2600,plain,
rd(mult(mult(X1,X2),rd(X3,X4)),rd(X3,X4)) = rd(mult(mult(X1,X2),X4),X4),
inference(step,[status(thm)],[t9,t57]) ).
cnf(t58,plain,
rd(mult(mult(X1,X2),rd(X3,X4)),rd(X3,X4)) = rd(mult(mult(X1,X2),X4),X4),
inference(orient,[status(thm)],[t2600]) ).
cnf(t87,plain,
rd(mult(rd(rd(X1,X1),rd(X1,X1)),X1),X1) = mult(rd(X1,X1),rd(rd(X1,X1),rd(X1,X1))),
inference(cp,[status(thm)],[t86,t38]) ).
cnf(t2604,plain,
rd(mult(rd(rd(X1,X1),rd(X1,X1)),X1),X1) = rd(X1,X1),
inference(step,[status(thm)],[t87,t43]) ).
cnf(t109,plain,
rd(mult(rd(rd(X1,X1),rd(X1,X1)),X1),X1) = rd(X1,X1),
inference(orient,[status(thm)],[t2604]) ).
cnf(t111,plain,
rd(mult(mult(rd(rd(X1,X1),rd(X1,X1)),X1),X1),X1) = mult(rd(X1,X1),X1),
inference(cp,[status(thm)],[t16,t109]) ).
cnf(t61,plain,
rd(mult(mult(X1,X2),X2),X2) = mult(X1,X2),
inference(cp,[status(thm)],[t57,t7]) ).
cnf(t75,plain,
rd(mult(mult(X1,X2),X2),X2) = mult(X1,X2),
inference(orient,[status(thm)],[t61]) ).
cnf(t2605,plain,
mult(rd(rd(X1,X1),rd(X1,X1)),X1) = mult(rd(X1,X1),X1),
inference(step,[status(thm)],[t111,t75]) ).
cnf(t2606,plain,
mult(rd(rd(X1,X1),rd(X1,X1)),X1) = rd(mult(X1,X1),X1),
inference(step,[status(thm)],[t2605,t16]) ).
cnf(t2607,plain,
mult(rd(rd(X1,X1),rd(X1,X1)),X1) = X1,
inference(step,[status(thm)],[t2606,t7]) ).
cnf(t115,plain,
mult(rd(rd(X1,X1),rd(X1,X1)),X1) = X1,
inference(orient,[status(thm)],[t2607]) ).
cnf(t118,plain,
rd(mult(mult(rd(rd(X1,X1),rd(X1,X1)),X1),X2),X2) = rd(mult(X1,rd(X3,X2)),rd(X3,X2)),
inference(cp,[status(thm)],[t58,t115]) ).
cnf(t2610,plain,
rd(mult(X1,X2),X2) = rd(mult(X1,rd(X3,X2)),rd(X3,X2)),
inference(step,[status(thm)],[t118,t115]) ).
cnf(t128,plain,
rd(mult(X1,rd(X2,X3)),rd(X2,X3)) = rd(mult(X1,X3),X3),
inference(orient,[status(thm)],[t2610]) ).
cnf(t39,plain,
mult(mult(X1,ld(X1,X2)),X3) = mult(rd(X1,X1),ld(ld(X1,X1),mult(X2,X3))),
inference(cp,[status(thm)],[t21,t38]) ).
cnf(t2618,plain,
mult(mult(X1,ld(X1,X2)),X3) = mult(rd(X1,X1),ld(rd(X1,X1),mult(X2,X3))),
inference(step,[status(thm)],[t39,t38]) ).
cnf(t339,plain,
mult(rd(X1,X1),ld(rd(X1,X1),mult(X2,X3))) = mult(mult(X1,ld(X1,X2)),X3),
inference(orient,[status(thm)],[t2618]) ).
cnf(t132,plain,
rd(mult(rd(X1,rd(X2,X3)),X3),X3) = rd(rd(mult(X1,rd(X2,X3)),rd(X2,X3)),rd(X2,X3)),
inference(cp,[status(thm)],[t128,t16]) ).
cnf(t76,plain,
mult(X1,rd(X2,X3)) = rd(mult(mult(X1,rd(X2,X3)),X3),X3),
inference(cp,[status(thm)],[t75,t58]) ).
cnf(t93,plain,
rd(mult(mult(X1,rd(X2,X3)),X3),X3) = mult(X1,rd(X2,X3)),
inference(orient,[status(thm)],[t76]) ).
cnf(t121,plain,
mult(rd(rd(rd(X1,X2),rd(X1,X2)),rd(rd(X1,X2),rd(X1,X2))),rd(X1,X2)) = rd(mult(rd(X1,X2),X2),X2),
inference(cp,[status(thm)],[t93,t115]) ).
cnf(t2608,plain,
rd(X1,X2) = rd(mult(rd(X1,X2),X2),X2),
inference(step,[status(thm)],[t121,t115]) ).
cnf(t2609,plain,
rd(X1,X2) = rd(rd(mult(X1,X2),X2),X2),
inference(step,[status(thm)],[t2608,t16]) ).
cnf(t122,plain,
rd(rd(mult(X1,X2),X2),X2) = rd(X1,X2),
inference(orient,[status(thm)],[t2609]) ).
cnf(t2611,plain,
rd(mult(rd(X1,rd(X2,X3)),X3),X3) = rd(X1,rd(X2,X3)),
inference(step,[status(thm)],[t132,t122]) ).
cnf(t145,plain,
rd(mult(rd(X1,rd(X2,X3)),X3),X3) = rd(X1,rd(X2,X3)),
inference(orient,[status(thm)],[t2611]) ).
cnf(t147,plain,
rd(rd(X1,X1),rd(X1,X1)) = rd(X1,X1),
inference(cp,[status(thm)],[t145,t115]) ).
cnf(t158,plain,
rd(rd(X1,X1),rd(X1,X1)) = rd(X1,X1),
inference(orient,[status(thm)],[t147]) ).
cnf(t159,plain,
rd(X1,X1) = mult(rd(X1,X1),rd(X1,X1)),
inference(cp,[status(thm)],[t43,t158]) ).
cnf(t161,plain,
mult(rd(X1,X1),rd(X1,X1)) = rd(X1,X1),
inference(orient,[status(thm)],[t159]) ).
cnf(t353,plain,
mult(mult(X1,ld(X1,rd(X2,X2))),rd(X2,X2)) = mult(rd(X1,X1),ld(rd(X1,X1),rd(X2,X2))),
inference(cp,[status(thm)],[t339,t161]) ).
cnf(t2619,plain,
mult(rd(mult(rd(X1,X1),X2),X2),rd(X2,X2)) = mult(rd(X1,X1),ld(rd(X1,X1),rd(X2,X2))),
inference(step,[status(thm)],[t353,t86]) ).
cnf(t140,plain,
rd(mult(mult(X1,rd(X2,X3)),rd(X2,X3)),rd(X2,X3)) = mult(rd(mult(X1,X3),X3),rd(X2,X3)),
inference(cp,[status(thm)],[t16,t128]) ).
cnf(t2613,plain,
rd(mult(mult(X1,rd(X2,X3)),X3),X3) = mult(rd(mult(X1,X3),X3),rd(X2,X3)),
inference(step,[status(thm)],[t140,t58]) ).
cnf(t2614,plain,
mult(X1,rd(X2,X3)) = mult(rd(mult(X1,X3),X3),rd(X2,X3)),
inference(step,[status(thm)],[t2613,t93]) ).
cnf(t180,plain,
mult(rd(mult(X1,X2),X2),rd(X3,X2)) = mult(X1,rd(X3,X2)),
inference(orient,[status(thm)],[t2614]) ).
cnf(t2620,plain,
mult(rd(X1,X1),rd(X2,X2)) = mult(rd(X1,X1),ld(rd(X1,X1),rd(X2,X2))),
inference(step,[status(thm)],[t2619,t180]) ).
cnf(t2621,plain,
mult(rd(X1,X1),rd(X2,X2)) = rd(mult(rd(rd(X1,X1),rd(X1,X1)),X2),X2),
inference(step,[status(thm)],[t2620,t86]) ).
cnf(t2622,plain,
mult(rd(X1,X1),rd(X2,X2)) = rd(mult(rd(X1,X1),X2),X2),
inference(step,[status(thm)],[t2621,t158]) ).
cnf(t375,plain,
mult(rd(X1,X1),rd(X2,X2)) = rd(mult(rd(X1,X1),X2),X2),
inference(orient,[status(thm)],[t2622]) ).
cnf(t389,plain,
rd(mult(rd(X1,X1),X2),X2) = rd(rd(mult(rd(X1,X1),X2),X2),rd(X2,X2)),
inference(cp,[status(thm)],[t128,t375]) ).
cnf(t141,plain,
rd(X1,rd(X2,X3)) = rd(rd(mult(X1,X3),X3),rd(X2,X3)),
inference(cp,[status(thm)],[t122,t128]) ).
cnf(t197,plain,
rd(rd(mult(X1,X2),X2),rd(X3,X2)) = rd(X1,rd(X3,X2)),
inference(orient,[status(thm)],[t141]) ).
cnf(t2623,plain,
rd(mult(rd(X1,X1),X2),X2) = rd(rd(X1,X1),rd(X2,X2)),
inference(step,[status(thm)],[t389,t197]) ).
cnf(t396,plain,
rd(mult(rd(X1,X1),X2),X2) = rd(rd(X1,X1),rd(X2,X2)),
inference(orient,[status(thm)],[t2623]) ).
cnf(t2624,plain,
mult(X1,ld(X1,rd(X2,X2))) = rd(rd(X1,X1),rd(X2,X2)),
inference(step,[status(thm)],[t86,t396]) ).
cnf(t397,plain,
mult(X1,ld(X1,rd(X2,X2))) = rd(rd(X1,X1),rd(X2,X2)),
inference(orient,[status(thm)],[t2624]) ).
cnf(t824,plain,
mult(X1,rd(X2,X2)) = mult(X1,rd(rd(X1,X1),rd(X2,X2))),
inference(cp,[status(thm)],[t822,t397]) ).
cnf(t390,plain,
rd(mult(mult(X1,rd(X2,X2)),rd(X3,X3)),rd(X3,X3)) = mult(X1,rd(rd(mult(rd(X2,X2),X3),X3),rd(X3,X3))),
inference(cp,[status(thm)],[t57,t375]) ).
cnf(t2630,plain,
rd(mult(mult(X1,rd(X2,X2)),X3),X3) = mult(X1,rd(rd(mult(rd(X2,X2),X3),X3),rd(X3,X3))),
inference(step,[status(thm)],[t390,t58]) ).
cnf(t2631,plain,
rd(mult(mult(X1,rd(X2,X2)),X3),X3) = mult(X1,rd(rd(X2,X2),rd(X3,X3))),
inference(step,[status(thm)],[t2630,t197]) ).
cnf(t451,plain,
mult(X1,rd(rd(X2,X2),rd(X3,X3))) = rd(mult(mult(X1,rd(X2,X2)),X3),X3),
inference(orient,[status(thm)],[t2631]) ).
cnf(t2649,plain,
mult(X1,rd(X2,X2)) = rd(mult(mult(X1,rd(X1,X1)),X2),X2),
inference(step,[status(thm)],[t824,t451]) ).
cnf(t2650,plain,
mult(X1,rd(X2,X2)) = rd(mult(X1,X2),X2),
inference(step,[status(thm)],[t2649,t43]) ).
cnf(t855,plain,
mult(X1,rd(X2,X2)) = rd(mult(X1,X2),X2),
inference(orient,[status(thm)],[t2650]) ).
cnf(t859,plain,
rd(mult(rd(X1,rd(X2,X2)),X2),X2) = rd(mult(X1,rd(X2,X2)),rd(X2,X2)),
inference(cp,[status(thm)],[t855,t16]) ).
cnf(t2653,plain,
rd(X1,rd(X2,X2)) = rd(mult(X1,rd(X2,X2)),rd(X2,X2)),
inference(step,[status(thm)],[t859,t145]) ).
cnf(t2654,plain,
rd(X1,rd(X2,X2)) = rd(mult(X1,X2),X2),
inference(step,[status(thm)],[t2653,t128]) ).
cnf(t888,plain,
rd(mult(X1,X2),X2) = rd(X1,rd(X2,X2)),
inference(orient,[status(thm)],[t2654]) ).
cnf(t2655,plain,
mult(rd(X1,X2),X2) = rd(X1,rd(X2,X2)),
inference(step,[status(thm)],[t16,t888]) ).
cnf(t889,plain,
mult(rd(X1,X2),X2) = rd(X1,rd(X2,X2)),
inference(orient,[status(thm)],[t2655]) ).
cnf(t905,plain,
rd(mult(X1,X2),rd(X2,X2)) = mult(rd(X1,rd(X2,X2)),X2),
inference(cp,[status(thm)],[t889,t888]) ).
cnf(t2673,plain,
rd(mult(X1,X2),rd(X2,X2)) = mult(X1,X2),
inference(step,[status(thm)],[t75,t888]) ).
cnf(t914,plain,
rd(mult(X1,X2),rd(X2,X2)) = mult(X1,X2),
inference(rw,[status(thm)],[t2673]) ).
cnf(t932,plain,
rd(mult(X1,X2),rd(X2,X2)) = mult(X1,X2),
inference(orient,[status(thm)],[t914]) ).
cnf(t2692,plain,
mult(X1,X2) = mult(rd(X1,rd(X2,X2)),X2),
inference(step,[status(thm)],[t905,t932]) ).
cnf(t956,plain,
mult(rd(X1,rd(X2,X2)),X2) = mult(X1,X2),
inference(orient,[status(thm)],[t2692]) ).
cnf(t136,plain,
rd(mult(X1,X2),X2) = rd(mult(X1,mult(X3,X2)),rd(mult(mult(X3,X2),X2),X2)),
inference(cp,[status(thm)],[t128,t75]) ).
cnf(t2612,plain,
rd(mult(X1,X2),X2) = rd(mult(X1,mult(X3,X2)),mult(X3,X2)),
inference(step,[status(thm)],[t136,t75]) ).
cnf(t163,plain,
rd(mult(X1,mult(X2,X3)),mult(X2,X3)) = rd(mult(X1,X3),X3),
inference(orient,[status(thm)],[t2612]) ).
cnf(t2669,plain,
rd(X1,rd(mult(X2,X3),mult(X2,X3))) = rd(mult(X1,X3),X3),
inference(step,[status(thm)],[t163,t888]) ).
cnf(t2670,plain,
rd(X1,rd(mult(X2,X3),mult(X2,X3))) = rd(X1,rd(X3,X3)),
inference(step,[status(thm)],[t2669,t888]) ).
cnf(t912,plain,
rd(X1,rd(mult(X2,X3),mult(X2,X3))) = rd(X1,rd(X3,X3)),
inference(rw,[status(thm)],[t2670]) ).
cnf(t1012,plain,
rd(X1,rd(mult(X2,X3),mult(X2,X3))) = rd(X1,rd(X3,X3)),
inference(orient,[status(thm)],[t912]) ).
cnf(t785,plain,
mult(X1,ld(X1,mult(mult(X1,X2),X3))) = mult(mult(X1,mult(X1,ld(X1,X2))),X3),
inference(cp,[status(thm)],[t769,t14]) ).
cnf(t2722,plain,
mult(X1,ld(X1,mult(mult(X1,X2),X3))) = mult(mult(X1,X2),X3),
inference(step,[status(thm)],[t785,t822]) ).
cnf(t1653,plain,
mult(X1,ld(X1,mult(mult(X1,X2),X3))) = mult(mult(X1,X2),X3),
inference(orient,[status(thm)],[t2722]) ).
cnf(t1677,plain,
rd(X1,rd(ld(X2,mult(mult(X2,X3),X4)),ld(X2,mult(mult(X2,X3),X4)))) = rd(X1,rd(mult(X2,ld(X2,mult(mult(X2,X3),X4))),mult(mult(X2,X3),X4))),
inference(cp,[status(thm)],[t1012,t1653]) ).
cnf(t1017,plain,
rd(X1,rd(mult(X2,ld(X2,X3)),mult(X2,ld(X2,X3)))) = rd(X1,rd(mult(X2,X3),mult(X2,mult(X2,ld(X2,X3))))),
inference(cp,[status(thm)],[t1012,t822]) ).
cnf(t2694,plain,
rd(X1,rd(ld(X2,X3),ld(X2,X3))) = rd(X1,rd(mult(X2,X3),mult(X2,mult(X2,ld(X2,X3))))),
inference(step,[status(thm)],[t1017,t1012]) ).
cnf(t2695,plain,
rd(X1,rd(ld(X2,X3),ld(X2,X3))) = rd(X1,rd(mult(X2,X3),mult(X2,X3))),
inference(step,[status(thm)],[t2694,t822]) ).
cnf(t2696,plain,
rd(X1,rd(ld(X2,X3),ld(X2,X3))) = rd(X1,rd(X3,X3)),
inference(step,[status(thm)],[t2695,t1012]) ).
cnf(t1152,plain,
rd(X1,rd(ld(X2,X3),ld(X2,X3))) = rd(X1,rd(X3,X3)),
inference(orient,[status(thm)],[t2696]) ).
cnf(t2723,plain,
rd(X1,rd(mult(mult(X2,X3),X4),mult(mult(X2,X3),X4))) = rd(X1,rd(mult(X2,ld(X2,mult(mult(X2,X3),X4))),mult(mult(X2,X3),X4))),
inference(step,[status(thm)],[t1677,t1152]) ).
cnf(t2724,plain,
rd(X1,rd(X4,X4)) = rd(X1,rd(mult(X2,ld(X2,mult(mult(X2,X3),X4))),mult(mult(X2,X3),X4))),
inference(step,[status(thm)],[t2723,t1012]) ).
cnf(t779,plain,
mult(X1,ld(X1,mult(rd(X2,X2),X3))) = mult(rd(rd(X1,X1),rd(X2,X2)),X3),
inference(cp,[status(thm)],[t769,t397]) ).
cnf(t1367,plain,
mult(rd(rd(X1,X1),rd(X2,X2)),X3) = mult(X1,ld(X1,mult(rd(X2,X2),X3))),
inference(orient,[status(thm)],[t779]) ).
cnf(t1368,plain,
mult(X1,ld(X1,mult(rd(X2,X2),X2))) = mult(rd(X1,X1),X2),
inference(cp,[status(thm)],[t1367,t956]) ).
cnf(t2699,plain,
mult(X1,ld(X1,rd(X2,rd(X2,X2)))) = mult(rd(X1,X1),X2),
inference(step,[status(thm)],[t1368,t889]) ).
cnf(t78,plain,
mult(X1,rd(X1,X1)) = rd(mult(X1,rd(X1,X1)),rd(X1,X1)),
inference(cp,[status(thm)],[t75,t43]) ).
cnf(t2602,plain,
X1 = rd(mult(X1,rd(X1,X1)),rd(X1,X1)),
inference(step,[status(thm)],[t78,t43]) ).
cnf(t2603,plain,
X1 = rd(X1,rd(X1,X1)),
inference(step,[status(thm)],[t2602,t43]) ).
cnf(t85,plain,
rd(X1,rd(X1,X1)) = X1,
inference(orient,[status(thm)],[t2603]) ).
cnf(t2700,plain,
mult(X1,ld(X1,X2)) = mult(rd(X1,X1),X2),
inference(step,[status(thm)],[t2699,t85]) ).
cnf(t1404,plain,
mult(rd(X1,X1),X2) = mult(X1,ld(X1,X2)),
inference(orient,[status(thm)],[t2700]) ).
cnf(t1419,plain,
rd(rd(X1,X1),rd(X2,X2)) = rd(mult(X1,ld(X1,X2)),X2),
inference(cp,[status(thm)],[t888,t1404]) ).
cnf(t1432,plain,
rd(mult(X1,ld(X1,X2)),X2) = rd(rd(X1,X1),rd(X2,X2)),
inference(orient,[status(thm)],[t1419]) ).
cnf(t2725,plain,
rd(X1,rd(X4,X4)) = rd(X1,rd(rd(X2,X2),rd(mult(mult(X2,X3),X4),mult(mult(X2,X3),X4)))),
inference(step,[status(thm)],[t2724,t1432]) ).
cnf(t2726,plain,
rd(X1,rd(X4,X4)) = rd(X1,rd(rd(X2,X2),rd(X4,X4))),
inference(step,[status(thm)],[t2725,t1012]) ).
cnf(t1680,plain,
rd(X1,rd(rd(X2,X2),rd(X3,X3))) = rd(X1,rd(X3,X3)),
inference(orient,[status(thm)],[t2726]) ).
cnf(t1689,plain,
rd(mult(X1,rd(rd(X2,X2),rd(X3,X3))),rd(X3,X3)) = rd(X1,rd(rd(rd(X2,X2),rd(X3,X3)),rd(rd(X2,X2),rd(X3,X3)))),
inference(cp,[status(thm)],[t1680,t888]) ).
cnf(t2651,plain,
mult(X1,rd(rd(X2,X2),rd(X3,X3))) = rd(mult(rd(mult(X1,X2),X2),X3),X3),
inference(step,[status(thm)],[t451,t855]) ).
cnf(t856,plain,
mult(X1,rd(rd(X2,X2),rd(X3,X3))) = rd(mult(rd(mult(X1,X2),X2),X3),X3),
inference(orient,[status(thm)],[t2651]) ).
cnf(t2657,plain,
mult(X1,rd(rd(X2,X2),rd(X3,X3))) = rd(rd(mult(X1,X2),X2),rd(X3,X3)),
inference(step,[status(thm)],[t856,t888]) ).
cnf(t2658,plain,
mult(X1,rd(rd(X2,X2),rd(X3,X3))) = rd(rd(X1,rd(X2,X2)),rd(X3,X3)),
inference(step,[status(thm)],[t2657,t888]) ).
cnf(t891,plain,
mult(X1,rd(rd(X2,X2),rd(X3,X3))) = rd(rd(X1,rd(X2,X2)),rd(X3,X3)),
inference(orient,[status(thm)],[t2658]) ).
cnf(t2727,plain,
rd(rd(rd(X1,rd(X2,X2)),rd(X3,X3)),rd(X3,X3)) = rd(X1,rd(rd(rd(X2,X2),rd(X3,X3)),rd(rd(X2,X2),rd(X3,X3)))),
inference(step,[status(thm)],[t1689,t891]) ).
cnf(t2680,plain,
rd(rd(X1,rd(X2,X3)),rd(X3,X3)) = rd(X1,rd(X2,X3)),
inference(step,[status(thm)],[t145,t888]) ).
cnf(t919,plain,
rd(rd(X1,rd(X2,X3)),rd(X3,X3)) = rd(X1,rd(X2,X3)),
inference(rw,[status(thm)],[t2680]) ).
cnf(t1119,plain,
rd(rd(X1,rd(X2,X3)),rd(X3,X3)) = rd(X1,rd(X2,X3)),
inference(orient,[status(thm)],[t919]) ).
cnf(t2728,plain,
rd(rd(X1,rd(X2,X2)),rd(X3,X3)) = rd(X1,rd(rd(rd(X2,X2),rd(X3,X3)),rd(rd(X2,X2),rd(X3,X3)))),
inference(step,[status(thm)],[t2727,t1119]) ).
cnf(t2671,plain,
rd(X1,rd(rd(X2,X3),rd(X2,X3))) = rd(mult(X1,X3),X3),
inference(step,[status(thm)],[t128,t888]) ).
cnf(t2672,plain,
rd(X1,rd(rd(X2,X3),rd(X2,X3))) = rd(X1,rd(X3,X3)),
inference(step,[status(thm)],[t2671,t888]) ).
cnf(t913,plain,
rd(X1,rd(rd(X2,X3),rd(X2,X3))) = rd(X1,rd(X3,X3)),
inference(rw,[status(thm)],[t2672]) ).
cnf(t1058,plain,
rd(X1,rd(rd(X2,X3),rd(X2,X3))) = rd(X1,rd(X3,X3)),
inference(orient,[status(thm)],[t913]) ).
cnf(t2729,plain,
rd(rd(X1,rd(X2,X2)),rd(X3,X3)) = rd(X1,rd(rd(X3,X3),rd(X3,X3))),
inference(step,[status(thm)],[t2728,t1058]) ).
cnf(t2730,plain,
rd(rd(X1,rd(X2,X2)),rd(X3,X3)) = rd(X1,rd(X3,X3)),
inference(step,[status(thm)],[t2729,t1058]) ).
cnf(t1737,plain,
rd(rd(X1,rd(X2,X2)),rd(X3,X3)) = rd(X1,rd(X3,X3)),
inference(orient,[status(thm)],[t2730]) ).
cnf(t1765,plain,
mult(rd(X1,rd(X2,X2)),X3) = mult(rd(X1,rd(X3,X3)),X3),
inference(cp,[status(thm)],[t956,t1737]) ).
cnf(t2731,plain,
mult(rd(X1,rd(X2,X2)),X3) = mult(X1,X3),
inference(step,[status(thm)],[t1765,t956]) ).
cnf(t1773,plain,
mult(rd(X1,rd(X2,X2)),X3) = mult(X1,X3),
inference(orient,[status(thm)],[t2731]) ).
cnf(t1780,plain,
mult(mult(X1,ld(X1,rd(X2,X2))),X3) = mult(rd(rd(X1,X1),rd(rd(X2,X2),rd(X2,X2))),X3),
inference(cp,[status(thm)],[t1773,t1432]) ).
cnf(t2735,plain,
mult(X1,ld(X1,mult(rd(X2,X2),X3))) = mult(rd(rd(X1,X1),rd(rd(X2,X2),rd(X2,X2))),X3),
inference(step,[status(thm)],[t1780,t769]) ).
cnf(t2736,plain,
mult(X1,ld(X1,mult(X2,ld(X2,X3)))) = mult(rd(rd(X1,X1),rd(rd(X2,X2),rd(X2,X2))),X3),
inference(step,[status(thm)],[t2735,t1404]) ).
cnf(t2737,plain,
mult(X1,ld(X1,mult(X2,ld(X2,X3)))) = mult(rd(X1,X1),X3),
inference(step,[status(thm)],[t2736,t1773]) ).
cnf(t2738,plain,
mult(X1,ld(X1,mult(X2,ld(X2,X3)))) = mult(X1,ld(X1,X3)),
inference(step,[status(thm)],[t2737,t1404]) ).
cnf(t1820,plain,
mult(X1,ld(X1,mult(X2,ld(X2,X3)))) = mult(X1,ld(X1,X3)),
inference(orient,[status(thm)],[t2738]) ).
cnf(t2638,plain,
mult(ld(X1,X2),ld(ld(X1,X2),mult(X3,X4))) = mult(X1,ld(X1,mult(X3,X4))),
inference(step,[status(thm)],[t21,t769]) ).
cnf(t770,plain,
mult(ld(X1,X2),ld(ld(X1,X2),mult(X3,X4))) = mult(X1,ld(X1,mult(X3,X4))),
inference(orient,[status(thm)],[t2638]) ).
cnf(t1824,plain,
mult(ld(X1,X2),ld(ld(X1,X2),X3)) = mult(X1,ld(X1,mult(X4,ld(X4,X3)))),
inference(cp,[status(thm)],[t1820,t770]) ).
cnf(t2745,plain,
mult(ld(X1,X2),ld(ld(X1,X2),X3)) = mult(X1,ld(X1,X3)),
inference(step,[status(thm)],[t1824,t1820]) ).
cnf(t1934,plain,
mult(ld(X1,X2),ld(ld(X1,X2),X3)) = mult(X1,ld(X1,X3)),
inference(orient,[status(thm)],[t2745]) ).
cnf(t1943,plain,
mult(X1,ld(X1,ld(X1,X2))) = mult(ld(X1,X2),rd(ld(X1,X2),ld(X1,X2))),
inference(cp,[status(thm)],[t1934,t38]) ).
cnf(t2661,plain,
mult(X1,rd(X2,X2)) = rd(X1,rd(X2,X2)),
inference(step,[status(thm)],[t855,t888]) ).
cnf(t893,plain,
mult(X1,rd(X2,X2)) = rd(X1,rd(X2,X2)),
inference(orient,[status(thm)],[t2661]) ).
cnf(t2746,plain,
mult(X1,ld(X1,ld(X1,X2))) = rd(ld(X1,X2),rd(ld(X1,X2),ld(X1,X2))),
inference(step,[status(thm)],[t1943,t893]) ).
cnf(t2747,plain,
mult(X1,ld(X1,ld(X1,X2))) = rd(ld(X1,X2),rd(X2,X2)),
inference(step,[status(thm)],[t2746,t1152]) ).
cnf(t1153,plain,
rd(ld(X1,X2),rd(X2,X2)) = ld(X1,X2),
inference(cp,[status(thm)],[t1152,t85]) ).
cnf(t1193,plain,
rd(ld(X1,X2),rd(X2,X2)) = ld(X1,X2),
inference(orient,[status(thm)],[t1153]) ).
cnf(t2748,plain,
mult(X1,ld(X1,ld(X1,X2))) = ld(X1,X2),
inference(step,[status(thm)],[t2747,t1193]) ).
cnf(t1959,plain,
mult(X1,ld(X1,ld(X1,X2))) = ld(X1,X2),
inference(orient,[status(thm)],[t2748]) ).
cnf(t1834,plain,
mult(X1,mult(X2,ld(X2,X3))) = mult(X1,mult(X1,ld(X1,X3))),
inference(cp,[status(thm)],[t822,t1820]) ).
cnf(t2739,plain,
mult(X1,mult(X2,ld(X2,X3))) = mult(X1,X3),
inference(step,[status(thm)],[t1834,t822]) ).
cnf(t1842,plain,
mult(X1,mult(X2,ld(X2,X3))) = mult(X1,X3),
inference(orient,[status(thm)],[t2739]) ).
cnf(t2701,plain,
mult(rd(rd(X1,X1),rd(X2,X2)),X3) = mult(X1,ld(X1,mult(X2,ld(X2,X3)))),
inference(step,[status(thm)],[t1367,t1404]) ).
cnf(t1405,plain,
mult(rd(rd(X1,X1),rd(X2,X2)),X3) = mult(X1,ld(X1,mult(X2,ld(X2,X3)))),
inference(orient,[status(thm)],[t2701]) ).
cnf(t1410,plain,
mult(rd(X1,X1),ld(rd(X1,X1),X2)) = mult(X1,ld(X1,mult(X1,ld(X1,X2)))),
inference(cp,[status(thm)],[t1404,t1405]) ).
cnf(t2704,plain,
mult(X1,ld(X1,ld(rd(X1,X1),X2))) = mult(X1,ld(X1,mult(X1,ld(X1,X2)))),
inference(step,[status(thm)],[t1410,t1404]) ).
cnf(t2705,plain,
mult(X1,ld(X1,ld(rd(X1,X1),X2))) = mult(X1,mult(X1,ld(X1,ld(X1,X2)))),
inference(step,[status(thm)],[t2704,t14]) ).
cnf(t2706,plain,
mult(X1,ld(X1,ld(rd(X1,X1),X2))) = mult(X1,ld(X1,X2)),
inference(step,[status(thm)],[t2705,t822]) ).
cnf(t1451,plain,
mult(X1,ld(X1,ld(rd(X1,X1),X2))) = mult(X1,ld(X1,X2)),
inference(orient,[status(thm)],[t2706]) ).
cnf(t1844,plain,
mult(X1,ld(rd(X2,X2),X3)) = mult(X1,mult(X2,ld(X2,X3))),
inference(cp,[status(thm)],[t1842,t1451]) ).
cnf(t2742,plain,
mult(X1,ld(rd(X2,X2),X3)) = mult(X1,X3),
inference(step,[status(thm)],[t1844,t1842]) ).
cnf(t1868,plain,
mult(X1,ld(rd(X2,X2),X3)) = mult(X1,X3),
inference(orient,[status(thm)],[t2742]) ).
cnf(t1962,plain,
ld(rd(X1,X1),X2) = mult(rd(X1,X1),ld(rd(X1,X1),X2)),
inference(cp,[status(thm)],[t1959,t1868]) ).
cnf(t2751,plain,
ld(rd(X1,X1),X2) = mult(X1,ld(X1,ld(rd(X1,X1),X2))),
inference(step,[status(thm)],[t1962,t1404]) ).
cnf(t2752,plain,
ld(rd(X1,X1),X2) = mult(X1,ld(X1,X2)),
inference(step,[status(thm)],[t2751,t1451]) ).
cnf(t1972,plain,
ld(rd(X1,X1),X2) = mult(X1,ld(X1,X2)),
inference(orient,[status(thm)],[t2752]) ).
cnf(t1821,plain,
mult(X1,ld(X1,X2)) = mult(mult(X1,X3),ld(mult(X1,X3),X2)),
inference(cp,[status(thm)],[t1820,t1653]) ).
cnf(t1890,plain,
mult(mult(X1,X2),ld(mult(X1,X2),X3)) = mult(X1,ld(X1,X3)),
inference(orient,[status(thm)],[t1821]) ).
cnf(t1899,plain,
mult(X1,ld(X1,X2)) = mult(rd(X1,rd(X3,X3)),ld(mult(X1,rd(X3,X3)),X2)),
inference(cp,[status(thm)],[t1890,t893]) ).
cnf(t2760,plain,
mult(X1,ld(X1,X2)) = mult(X1,ld(mult(X1,rd(X3,X3)),X2)),
inference(step,[status(thm)],[t1899,t1773]) ).
cnf(t2761,plain,
mult(X1,ld(X1,X2)) = mult(X1,ld(rd(X1,rd(X3,X3)),X2)),
inference(step,[status(thm)],[t2760,t893]) ).
cnf(t2033,plain,
mult(X1,ld(rd(X1,rd(X2,X2)),X3)) = mult(X1,ld(X1,X3)),
inference(orient,[status(thm)],[t2761]) ).
cnf(t2039,plain,
mult(X1,ld(X1,ld(rd(X1,rd(X2,X2)),X3))) = ld(X1,mult(X1,ld(X1,X3))),
inference(cp,[status(thm)],[t14,t2033]) ).
cnf(t2781,plain,
mult(X1,ld(X1,ld(rd(X1,rd(X2,X2)),X3))) = mult(X1,ld(X1,ld(X1,X3))),
inference(step,[status(thm)],[t2039,t14]) ).
cnf(t2782,plain,
mult(X1,ld(X1,ld(rd(X1,rd(X2,X2)),X3))) = ld(X1,X3),
inference(step,[status(thm)],[t2781,t1959]) ).
cnf(t2244,plain,
mult(X1,ld(X1,ld(rd(X1,rd(X2,X2)),X3))) = ld(X1,X3),
inference(orient,[status(thm)],[t2782]) ).
cnf(t2246,plain,
ld(rd(X1,rd(X2,X2)),X3) = mult(X1,ld(rd(X1,rd(X2,X2)),ld(rd(rd(X1,rd(X2,X2)),rd(X4,X4)),X3))),
inference(cp,[status(thm)],[t2244,t1773]) ).
cnf(t2783,plain,
ld(rd(X1,rd(X2,X2)),X3) = mult(X1,ld(X1,ld(rd(rd(X1,rd(X2,X2)),rd(X4,X4)),X3))),
inference(step,[status(thm)],[t2246,t2033]) ).
cnf(t2784,plain,
ld(rd(X1,rd(X2,X2)),X3) = mult(X1,ld(X1,ld(rd(X1,rd(X4,X4)),X3))),
inference(step,[status(thm)],[t2783,t1737]) ).
cnf(t2785,plain,
ld(rd(X1,rd(X2,X2)),X3) = ld(X1,X3),
inference(step,[status(thm)],[t2784,t2244]) ).
cnf(t2273,plain,
ld(rd(X1,rd(X2,X2)),X3) = ld(X1,X3),
inference(orient,[status(thm)],[t2785]) ).
cnf(t2274,plain,
ld(X1,rd(X1,rd(X2,X2))) = rd(rd(X1,rd(X2,X2)),rd(X1,rd(X2,X2))),
inference(cp,[status(thm)],[t2273,t38]) ).
cnf(t861,plain,
mult(X1,ld(X1,rd(X2,X2))) = ld(X1,rd(mult(X1,X2),X2)),
inference(cp,[status(thm)],[t14,t855]) ).
cnf(t2689,plain,
rd(rd(X1,X1),rd(X2,X2)) = ld(X1,rd(mult(X1,X2),X2)),
inference(step,[status(thm)],[t861,t397]) ).
cnf(t2690,plain,
rd(rd(X1,X1),rd(X2,X2)) = ld(X1,rd(X1,rd(X2,X2))),
inference(step,[status(thm)],[t2689,t888]) ).
cnf(t942,plain,
ld(X1,rd(X1,rd(X2,X2))) = rd(rd(X1,X1),rd(X2,X2)),
inference(orient,[status(thm)],[t2690]) ).
cnf(t2786,plain,
rd(rd(X1,X1),rd(X2,X2)) = rd(rd(X1,rd(X2,X2)),rd(X1,rd(X2,X2))),
inference(step,[status(thm)],[t2274,t942]) ).
cnf(t2663,plain,
rd(rd(X1,rd(X2,X2)),X2) = rd(X1,X2),
inference(step,[status(thm)],[t122,t888]) ).
cnf(t906,plain,
rd(rd(X1,rd(X2,X2)),X2) = rd(X1,X2),
inference(rw,[status(thm)],[t2663]) ).
cnf(t928,plain,
rd(rd(X1,rd(X2,X2)),X2) = rd(X1,X2),
inference(orient,[status(thm)],[t906]) ).
cnf(t1767,plain,
rd(rd(X1,rd(X2,X2)),X3) = rd(rd(X1,rd(X3,X3)),X3),
inference(cp,[status(thm)],[t928,t1737]) ).
cnf(t2734,plain,
rd(rd(X1,rd(X2,X2)),X3) = rd(X1,X3),
inference(step,[status(thm)],[t1767,t928]) ).
cnf(t1791,plain,
rd(rd(X1,rd(X2,X2)),X3) = rd(X1,X3),
inference(orient,[status(thm)],[t2734]) ).
cnf(t2787,plain,
rd(rd(X1,X1),rd(X2,X2)) = rd(X1,rd(X1,rd(X2,X2))),
inference(step,[status(thm)],[t2786,t1791]) ).
cnf(t2283,plain,
rd(rd(X1,X1),rd(X2,X2)) = rd(X1,rd(X1,rd(X2,X2))),
inference(orient,[status(thm)],[t2787]) ).
cnf(t2792,plain,
rd(mult(X1,ld(X1,X2)),X2) = rd(X1,rd(X1,rd(X2,X2))),
inference(step,[status(thm)],[t1432,t2283]) ).
cnf(t2288,plain,
rd(mult(X1,ld(X1,X2)),X2) = rd(X1,rd(X1,rd(X2,X2))),
inference(orient,[status(thm)],[t2792]) ).
cnf(t19,plain,
mult(rd(X1,X2),ld(rd(X1,X2),X2)) = ld(rd(X1,X2),rd(mult(X1,X2),X2)),
inference(cp,[status(thm)],[t14,t16]) ).
cnf(t257,plain,
ld(rd(X1,X2),rd(mult(X1,X2),X2)) = mult(rd(X1,X2),ld(rd(X1,X2),X2)),
inference(orient,[status(thm)],[t19]) ).
cnf(t2664,plain,
ld(rd(X1,X2),rd(X1,rd(X2,X2))) = mult(rd(X1,X2),ld(rd(X1,X2),X2)),
inference(step,[status(thm)],[t257,t888]) ).
cnf(t907,plain,
ld(rd(X1,X2),rd(X1,rd(X2,X2))) = mult(rd(X1,X2),ld(rd(X1,X2),X2)),
inference(rw,[status(thm)],[t2664]) ).
cnf(t2438,plain,
ld(rd(X1,X2),rd(X1,rd(X2,X2))) = mult(rd(X1,X2),ld(rd(X1,X2),X2)),
inference(orient,[status(thm)],[t907]) ).
cnf(t2484,plain,
rd(rd(X1,X2),rd(rd(X1,X2),rd(rd(X1,rd(X2,X2)),rd(X1,rd(X2,X2))))) = rd(mult(rd(X1,X2),mult(rd(X1,X2),ld(rd(X1,X2),X2))),rd(X1,rd(X2,X2))),
inference(cp,[status(thm)],[t2288,t2438]) ).
cnf(t2815,plain,
rd(rd(X1,X2),rd(rd(X1,X2),rd(rd(X2,X2),rd(X2,X2)))) = rd(mult(rd(X1,X2),mult(rd(X1,X2),ld(rd(X1,X2),X2))),rd(X1,rd(X2,X2))),
inference(step,[status(thm)],[t2484,t1058]) ).
cnf(t2816,plain,
rd(rd(X1,X2),rd(rd(X1,X2),rd(X2,X2))) = rd(mult(rd(X1,X2),mult(rd(X1,X2),ld(rd(X1,X2),X2))),rd(X1,rd(X2,X2))),
inference(step,[status(thm)],[t2815,t1058]) ).
cnf(t902,plain,
rd(rd(X1,X2),rd(X2,X2)) = rd(rd(X1,rd(X2,X2)),X2),
inference(cp,[status(thm)],[t888,t889]) ).
cnf(t2691,plain,
rd(rd(X1,X2),rd(X2,X2)) = rd(X1,X2),
inference(step,[status(thm)],[t902,t928]) ).
cnf(t949,plain,
rd(rd(X1,X2),rd(X2,X2)) = rd(X1,X2),
inference(orient,[status(thm)],[t2691]) ).
cnf(t2817,plain,
rd(rd(X1,X2),rd(X1,X2)) = rd(mult(rd(X1,X2),mult(rd(X1,X2),ld(rd(X1,X2),X2))),rd(X1,rd(X2,X2))),
inference(step,[status(thm)],[t2816,t949]) ).
cnf(t2818,plain,
rd(rd(X1,X2),rd(X1,X2)) = rd(mult(rd(X1,X2),X2),rd(X1,rd(X2,X2))),
inference(step,[status(thm)],[t2817,t1842]) ).
cnf(t2819,plain,
rd(rd(X1,X2),rd(X1,X2)) = rd(rd(X1,rd(X2,X2)),rd(X1,rd(X2,X2))),
inference(step,[status(thm)],[t2818,t889]) ).
cnf(t2820,plain,
rd(rd(X1,X2),rd(X1,X2)) = rd(X1,rd(X1,rd(X2,X2))),
inference(step,[status(thm)],[t2819,t1791]) ).
cnf(t2530,plain,
rd(rd(X1,X2),rd(X1,X2)) = rd(X1,rd(X1,rd(X2,X2))),
inference(orient,[status(thm)],[t2820]) ).
cnf(t2534,plain,
mult(rd(X1,X2),ld(rd(X1,X2),X3)) = ld(rd(X1,rd(X1,rd(X2,X2))),X3),
inference(cp,[status(thm)],[t1972,t2530]) ).
cnf(t2299,plain,
ld(rd(X1,X1),X2) = ld(rd(X1,rd(X1,rd(X3,X3))),X2),
inference(cp,[status(thm)],[t2273,t2283]) ).
cnf(t2794,plain,
mult(X1,ld(X1,X2)) = ld(rd(X1,rd(X1,rd(X3,X3))),X2),
inference(step,[status(thm)],[t2299,t1972]) ).
cnf(t2328,plain,
ld(rd(X1,rd(X1,rd(X2,X2))),X3) = mult(X1,ld(X1,X3)),
inference(orient,[status(thm)],[t2794]) ).
cnf(t2824,plain,
mult(rd(X1,X2),ld(rd(X1,X2),X3)) = mult(X1,ld(X1,X3)),
inference(step,[status(thm)],[t2534,t2328]) ).
cnf(t2566,plain,
mult(rd(X1,X2),ld(rd(X1,X2),X3)) = mult(X1,ld(X1,X3)),
inference(orient,[status(thm)],[t2824]) ).
cnf(goal_0,negated_conjecture,
ld(rd(x0,x1),mult(rd(x0,x1),x2)) != ld(x0,mult(x0,x2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
mult(rd(x0,x1),ld(rd(x0,x1),x2)) != ld(x0,mult(x0,x2)),
inference(rw,[status(thm)],[goal_0,t14]) ).
cnf(g0_1,plain,
mult(x0,ld(x0,x2)) != ld(x0,mult(x0,x2)),
inference(rw,[status(thm)],[g0_0,t2566]) ).
cnf(g0_2,plain,
mult(x0,ld(x0,x2)) != mult(x0,ld(x0,x2)),
inference(rw,[status(thm)],[g0_1,t14]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP682-11 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/0.35 % Computer : n015.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Wed Sep 23 15:44:24 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 6.72/1.39 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.72/1.39 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------