%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP752-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 : n005.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:20 PM UTC 2026
% Result : Unsatisfiable 120.61s 17.83s
% Output : CNFRefutation 120.61s
% Verified :
% SZS Type : Refutation
% Derivation depth : 67
% Number of leaves : 8
% Syntax : Number of clauses : 158 ( 158 unt; 0 nHn; 3 RR)
% Number of literals : 158 ( 157 equ; 2 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 : 469 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t4,axiom,
mult(mult(X1,X2),mult(X1,X3)) = mult(mult(X1,X1),mult(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t31,plain,
mult(mult(X1,X2),mult(X1,X3)) = mult(mult(X1,X1),mult(X2,X3)),
inference(orient,[status(thm)],[t4]) ).
cnf(t1,axiom,
mult(X1,ld(X1,X2)) = X2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t7,plain,
mult(X1,ld(X1,X2)) = X2,
inference(orient,[status(thm)],[t1]) ).
cnf(t35,plain,
mult(mult(X1,X1),mult(X2,ld(X1,X3))) = mult(mult(X1,X2),X3),
inference(cp,[status(thm)],[t31,t7]) ).
cnf(t159,plain,
mult(mult(X1,X1),mult(X2,ld(X1,X3))) = mult(mult(X1,X2),X3),
inference(orient,[status(thm)],[t35]) ).
cnf(t0,axiom,
ld(X1,mult(X1,X2)) = X2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t11,plain,
ld(X1,mult(X1,X2)) = X2,
inference(orient,[status(thm)],[t0]) ).
cnf(t2,axiom,
mult(rd(X1,X2),X2) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t8,plain,
mult(rd(X1,X2),X2) = X1,
inference(orient,[status(thm)],[t2]) ).
cnf(t12,plain,
X1 = ld(rd(X2,X1),X2),
inference(cp,[status(thm)],[t11,t8]) ).
cnf(t115,plain,
ld(rd(X1,X2),X1) = X2,
inference(orient,[status(thm)],[t12]) ).
cnf(t3,axiom,
rd(mult(X1,X2),X2) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t9,plain,
rd(mult(X1,X2),X2) = X1,
inference(orient,[status(thm)],[t3]) ).
cnf(t5,axiom,
mult(mult(X1,X2),mult(X3,X3)) = mult(mult(X1,X3),mult(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t13,plain,
mult(mult(X1,X2),mult(X3,X3)) = mult(mult(X1,X3),mult(X2,X3)),
inference(orient,[status(thm)],[t5]) ).
cnf(t14,plain,
mult(mult(X1,X2),mult(ld(X1,X3),X2)) = mult(X3,mult(X2,X2)),
inference(cp,[status(thm)],[t13,t7]) ).
cnf(t116,plain,
mult(mult(X1,X2),mult(ld(X1,X3),X2)) = mult(X3,mult(X2,X2)),
inference(orient,[status(thm)],[t14]) ).
cnf(t127,plain,
mult(X1,mult(X2,X2)) = mult(mult(rd(X1,X3),X2),mult(X3,X2)),
inference(cp,[status(thm)],[t116,t115]) ).
cnf(t214,plain,
mult(mult(rd(X1,X2),X3),mult(X2,X3)) = mult(X1,mult(X3,X3)),
inference(orient,[status(thm)],[t127]) ).
cnf(t223,plain,
mult(X1,mult(X2,X2)) = mult(mult(rd(X1,rd(X3,X2)),X2),X3),
inference(cp,[status(thm)],[t214,t8]) ).
cnf(t390,plain,
mult(mult(rd(X1,rd(X2,X3)),X3),X2) = mult(X1,mult(X3,X3)),
inference(orient,[status(thm)],[t223]) ).
cnf(t395,plain,
mult(rd(X1,rd(X2,X3)),X3) = rd(mult(X1,mult(X3,X3)),X2),
inference(cp,[status(thm)],[t9,t390]) ).
cnf(t405,plain,
mult(rd(X1,rd(X2,X3)),X3) = rd(mult(X1,mult(X3,X3)),X2),
inference(orient,[status(thm)],[t395]) ).
cnf(t411,plain,
rd(X1,rd(X2,X3)) = rd(rd(mult(X1,mult(X3,X3)),X2),X3),
inference(cp,[status(thm)],[t9,t405]) ).
cnf(t562,plain,
rd(rd(mult(X1,mult(X2,X2)),X3),X2) = rd(X1,rd(X3,X2)),
inference(orient,[status(thm)],[t411]) ).
cnf(t566,plain,
rd(rd(X1,mult(X2,X2)),rd(X3,X2)) = rd(rd(X1,X3),X2),
inference(cp,[status(thm)],[t562,t8]) ).
cnf(t810,plain,
rd(rd(X1,mult(X2,X2)),rd(X3,X2)) = rd(rd(X1,X3),X2),
inference(orient,[status(thm)],[t566]) ).
cnf(t824,plain,
rd(X1,mult(X2,X2)) = mult(rd(rd(X1,X3),X2),rd(X3,X2)),
inference(cp,[status(thm)],[t8,t810]) ).
cnf(t830,plain,
mult(rd(rd(X1,X2),X3),rd(X2,X3)) = rd(X1,mult(X3,X3)),
inference(orient,[status(thm)],[t824]) ).
cnf(t838,plain,
rd(mult(X1,X2),mult(X3,X3)) = mult(rd(X1,X3),rd(X2,X3)),
inference(cp,[status(thm)],[t830,t9]) ).
cnf(t861,plain,
mult(rd(X1,X2),rd(X3,X2)) = rd(mult(X1,X3),mult(X2,X2)),
inference(orient,[status(thm)],[t838]) ).
cnf(t876,plain,
rd(mult(X1,mult(X2,X3)),mult(X3,X3)) = mult(rd(X1,X3),X2),
inference(cp,[status(thm)],[t861,t9]) ).
cnf(t965,plain,
rd(mult(X1,mult(X2,X3)),mult(X3,X3)) = mult(rd(X1,X3),X2),
inference(orient,[status(thm)],[t876]) ).
cnf(t32,plain,
mult(mult(X1,X1),mult(ld(X1,X2),X3)) = mult(X2,mult(X1,X3)),
inference(cp,[status(thm)],[t31,t7]) ).
cnf(t140,plain,
mult(mult(X1,X1),mult(ld(X1,X2),X3)) = mult(X2,mult(X1,X3)),
inference(orient,[status(thm)],[t32]) ).
cnf(t969,plain,
mult(rd(mult(X1,X1),X2),ld(X1,X3)) = rd(mult(X3,mult(X1,X2)),mult(X2,X2)),
inference(cp,[status(thm)],[t965,t140]) ).
cnf(t360131,plain,
mult(rd(mult(X1,X1),X2),ld(X1,X3)) = mult(rd(X3,X2),X1),
inference(step,[status(thm)],[t969,t965]) ).
cnf(t1129,plain,
mult(rd(mult(X1,X1),X2),ld(X1,X3)) = mult(rd(X3,X2),X1),
inference(orient,[status(thm)],[t360131]) ).
cnf(t1153,plain,
rd(mult(X1,X1),X2) = rd(mult(rd(X3,X2),X1),ld(X1,X3)),
inference(cp,[status(thm)],[t9,t1129]) ).
cnf(t1624,plain,
rd(mult(rd(X1,X2),X3),ld(X3,X1)) = rd(mult(X3,X3),X2),
inference(orient,[status(thm)],[t1153]) ).
cnf(t1654,plain,
rd(mult(X1,X1),X2) = rd(mult(rd(mult(X1,X3),X2),X1),X3),
inference(cp,[status(thm)],[t1624,t11]) ).
cnf(t2172,plain,
rd(mult(rd(mult(X1,X2),X3),X1),X2) = rd(mult(X1,X1),X3),
inference(orient,[status(thm)],[t1654]) ).
cnf(t1646,plain,
rd(mult(X1,X1),X2) = rd(mult(X3,X1),ld(X1,mult(X3,X2))),
inference(cp,[status(thm)],[t1624,t9]) ).
cnf(t2042,plain,
rd(mult(X1,X2),ld(X2,mult(X1,X3))) = rd(mult(X2,X2),X3),
inference(orient,[status(thm)],[t1646]) ).
cnf(t2179,plain,
rd(mult(X1,X1),ld(X2,mult(X1,X3))) = rd(mult(rd(mult(X2,X2),X3),X1),X2),
inference(cp,[status(thm)],[t2172,t2042]) ).
cnf(t869,plain,
rd(mult(mult(X1,X2),X3),mult(X2,X2)) = mult(X1,rd(X3,X2)),
inference(cp,[status(thm)],[t861,t9]) ).
cnf(t913,plain,
rd(mult(mult(X1,X2),X3),mult(X2,X2)) = mult(X1,rd(X3,X2)),
inference(orient,[status(thm)],[t869]) ).
cnf(t918,plain,
mult(X1,rd(ld(mult(X1,X2),X3),X2)) = rd(X3,mult(X2,X2)),
inference(cp,[status(thm)],[t913,t7]) ).
cnf(t1014,plain,
mult(X1,rd(ld(mult(X1,X2),X3),X2)) = rd(X3,mult(X2,X2)),
inference(orient,[status(thm)],[t918]) ).
cnf(t1043,plain,
rd(ld(mult(X1,X2),X3),X2) = ld(X1,rd(X3,mult(X2,X2))),
inference(cp,[status(thm)],[t11,t1014]) ).
cnf(t1069,plain,
ld(X1,rd(X2,mult(X3,X3))) = rd(ld(mult(X1,X3),X2),X3),
inference(orient,[status(thm)],[t1043]) ).
cnf(t163,plain,
mult(mult(X1,rd(X2,ld(X1,X3))),X3) = mult(mult(X1,X1),X2),
inference(cp,[status(thm)],[t159,t8]) ).
cnf(t347,plain,
mult(mult(X1,rd(X2,ld(X1,X3))),X3) = mult(mult(X1,X1),X2),
inference(orient,[status(thm)],[t163]) ).
cnf(t356,plain,
mult(X1,rd(X2,ld(X1,X3))) = rd(mult(mult(X1,X1),X2),X3),
inference(cp,[status(thm)],[t9,t347]) ).
cnf(t366,plain,
mult(X1,rd(X2,ld(X1,X3))) = rd(mult(mult(X1,X1),X2),X3),
inference(orient,[status(thm)],[t356]) ).
cnf(t373,plain,
rd(X1,ld(X2,X3)) = ld(X2,rd(mult(mult(X2,X2),X1),X3)),
inference(cp,[status(thm)],[t11,t366]) ).
cnf(t535,plain,
ld(X1,rd(mult(mult(X1,X1),X2),X3)) = rd(X2,ld(X1,X3)),
inference(orient,[status(thm)],[t373]) ).
cnf(t1070,plain,
rd(ld(mult(X1,X2),mult(mult(X1,X1),X3)),X2) = rd(X3,ld(X1,mult(X2,X2))),
inference(cp,[status(thm)],[t1069,t535]) ).
cnf(t144,plain,
mult(X1,mult(X2,ld(ld(X2,X1),X3))) = mult(mult(X2,X2),X3),
inference(cp,[status(thm)],[t140,t7]) ).
cnf(t239,plain,
mult(X1,mult(X2,ld(ld(X2,X1),X3))) = mult(mult(X2,X2),X3),
inference(orient,[status(thm)],[t144]) ).
cnf(t248,plain,
mult(X1,ld(ld(X1,X2),X3)) = ld(X2,mult(mult(X1,X1),X3)),
inference(cp,[status(thm)],[t11,t239]) ).
cnf(t264,plain,
ld(X1,mult(mult(X2,X2),X3)) = mult(X2,ld(ld(X2,X1),X3)),
inference(orient,[status(thm)],[t248]) ).
cnf(t360129,plain,
rd(mult(X1,ld(ld(X1,mult(X1,X2)),X3)),X2) = rd(X3,ld(X1,mult(X2,X2))),
inference(step,[status(thm)],[t1070,t264]) ).
cnf(t360130,plain,
rd(mult(X1,ld(X2,X3)),X2) = rd(X3,ld(X1,mult(X2,X2))),
inference(step,[status(thm)],[t360129,t11]) ).
cnf(t1097,plain,
rd(mult(X1,ld(X2,X3)),X2) = rd(X3,ld(X1,mult(X2,X2))),
inference(orient,[status(thm)],[t360130]) ).
cnf(t1109,plain,
rd(mult(X1,X2),ld(X3,mult(X1,X1))) = rd(mult(X3,X2),X1),
inference(cp,[status(thm)],[t1097,t11]) ).
cnf(t1344,plain,
rd(mult(X1,X2),ld(X3,mult(X1,X1))) = rd(mult(X3,X2),X1),
inference(orient,[status(thm)],[t1109]) ).
cnf(t1375,plain,
rd(mult(rd(mult(X1,X1),X2),X3),X1) = rd(mult(X1,X3),X2),
inference(cp,[status(thm)],[t1344,t115]) ).
cnf(t1766,plain,
rd(mult(rd(mult(X1,X1),X2),X3),X1) = rd(mult(X1,X3),X2),
inference(orient,[status(thm)],[t1375]) ).
cnf(t360141,plain,
rd(mult(X1,X1),ld(X2,mult(X1,X3))) = rd(mult(X2,X1),X3),
inference(step,[status(thm)],[t2179,t1766]) ).
cnf(t2667,plain,
rd(mult(X1,X1),ld(X2,mult(X1,X3))) = rd(mult(X2,X1),X3),
inference(orient,[status(thm)],[t360141]) ).
cnf(t6,axiom,
mult(mult(X1,mult(X1,X1)),mult(X2,X3)) = mult(mult(X1,X2),mult(mult(X1,X1),X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t65,plain,
mult(mult(X1,X2),mult(mult(X1,X1),X3)) = mult(mult(X1,mult(X1,X1)),mult(X2,X3)),
inference(orient,[status(thm)],[t6]) ).
cnf(t80,plain,
mult(mult(X1,X1),X2) = ld(mult(X1,X3),mult(mult(X1,mult(X1,X1)),mult(X3,X2))),
inference(cp,[status(thm)],[t11,t65]) ).
cnf(t269,plain,
mult(X1,ld(ld(X1,X2),mult(X3,ld(X1,Y3)))) = ld(X2,mult(mult(X1,X3),Y3)),
inference(cp,[status(thm)],[t264,t159]) ).
cnf(t129414,plain,
mult(X1,ld(ld(X1,X2),mult(X3,ld(X1,Y3)))) = ld(X2,mult(mult(X1,X3),Y3)),
inference(orient,[status(thm)],[t269]) ).
cnf(t129473,plain,
ld(mult(X1,X2),mult(mult(X1,X3),Y3)) = mult(X1,ld(X2,mult(X3,ld(X1,Y3)))),
inference(cp,[status(thm)],[t129414,t11]) ).
cnf(t130020,plain,
ld(mult(X1,X2),mult(mult(X1,X3),Y3)) = mult(X1,ld(X2,mult(X3,ld(X1,Y3)))),
inference(orient,[status(thm)],[t129473]) ).
cnf(t360908,plain,
mult(mult(X1,X1),X2) = mult(X1,ld(X3,mult(mult(X1,X1),ld(X1,mult(X3,X2))))),
inference(step,[status(thm)],[t80,t130020]) ).
cnf(t360909,plain,
mult(mult(X1,X1),X2) = mult(X1,mult(X1,ld(ld(X1,X3),ld(X1,mult(X3,X2))))),
inference(step,[status(thm)],[t360908,t264]) ).
cnf(t229060,plain,
mult(X1,mult(X1,ld(ld(X1,X2),ld(X1,mult(X2,X3))))) = mult(mult(X1,X1),X3),
inference(orient,[status(thm)],[t360909]) ).
cnf(t1385,plain,
ld(X1,mult(X2,X2)) = ld(rd(mult(X1,X3),X2),mult(X2,X3)),
inference(cp,[status(thm)],[t115,t1344]) ).
cnf(t1815,plain,
ld(rd(mult(X1,X2),X3),mult(X3,X2)) = ld(X1,mult(X3,X3)),
inference(orient,[status(thm)],[t1385]) ).
cnf(t1829,plain,
ld(X1,mult(X2,X2)) = ld(rd(X3,X2),mult(X2,ld(X1,X3))),
inference(cp,[status(thm)],[t1815,t7]) ).
cnf(t2435,plain,
ld(rd(X1,X2),mult(X2,ld(X3,X1))) = ld(X3,mult(X2,X2)),
inference(orient,[status(thm)],[t1829]) ).
cnf(t2450,plain,
ld(X1,mult(X2,X2)) = ld(X3,mult(X2,ld(X1,mult(X3,X2)))),
inference(cp,[status(thm)],[t2435,t9]) ).
cnf(t2890,plain,
ld(X1,mult(X2,ld(X3,mult(X1,X2)))) = ld(X3,mult(X2,X2)),
inference(orient,[status(thm)],[t2450]) ).
cnf(t2931,plain,
mult(X1,ld(X2,mult(X3,X1))) = mult(X3,ld(X2,mult(X1,X1))),
inference(cp,[status(thm)],[t7,t2890]) ).
cnf(t119255,plain,
mult(X1,ld(X2,mult(X3,X1))) = mult(X3,ld(X2,mult(X1,X1))),
inference(orient,[status(thm)],[t2931]) ).
cnf(t120012,plain,
ld(X1,mult(X2,X2)) = ld(X3,mult(X2,ld(X1,mult(X3,X2)))),
inference(cp,[status(thm)],[t11,t119255]) ).
cnf(t120746,plain,
ld(X1,mult(X2,ld(X3,mult(X1,X2)))) = ld(X3,mult(X2,X2)),
inference(orient,[status(thm)],[t120012]) ).
cnf(t229243,plain,
mult(mult(X1,X1),ld(X2,mult(X1,X3))) = mult(X1,mult(X1,ld(ld(X1,X3),ld(X2,mult(X3,X3))))),
inference(cp,[status(thm)],[t229060,t120746]) ).
cnf(t1150,plain,
mult(rd(X1,X2),rd(X1,X3)) = mult(rd(mult(rd(X1,X3),rd(X1,X3)),X2),X3),
inference(cp,[status(thm)],[t1129,t115]) ).
cnf(t360132,plain,
mult(rd(X1,X2),rd(X1,X3)) = mult(rd(rd(mult(X1,X1),mult(X3,X3)),X2),X3),
inference(step,[status(thm)],[t1150,t861]) ).
cnf(t230,plain,
mult(rd(X1,X2),X3) = rd(mult(X1,mult(X3,X3)),mult(X2,X3)),
inference(cp,[status(thm)],[t9,t214]) ).
cnf(t421,plain,
rd(mult(X1,mult(X2,X2)),mult(X3,X2)) = mult(rd(X1,X3),X2),
inference(orient,[status(thm)],[t230]) ).
cnf(t424,plain,
mult(rd(rd(X1,mult(X2,X2)),X3),X2) = rd(X1,mult(X3,X2)),
inference(cp,[status(thm)],[t421,t8]) ).
cnf(t583,plain,
mult(rd(rd(X1,mult(X2,X2)),X3),X2) = rd(X1,mult(X3,X2)),
inference(orient,[status(thm)],[t424]) ).
cnf(t360133,plain,
mult(rd(X1,X2),rd(X1,X3)) = rd(mult(X1,X1),mult(X2,X3)),
inference(step,[status(thm)],[t360132,t583]) ).
cnf(t1173,plain,
mult(rd(X1,X2),rd(X1,X3)) = rd(mult(X1,X1),mult(X2,X3)),
inference(orient,[status(thm)],[t360133]) ).
cnf(t10,plain,
X1 = rd(X2,ld(X1,X2)),
inference(cp,[status(thm)],[t9,t7]) ).
cnf(t114,plain,
rd(X1,ld(X2,X1)) = X2,
inference(orient,[status(thm)],[t10]) ).
cnf(t1176,plain,
rd(mult(X1,X1),mult(ld(X2,X1),X3)) = mult(X2,rd(X1,X3)),
inference(cp,[status(thm)],[t1173,t114]) ).
cnf(t1676,plain,
rd(mult(X1,X1),mult(ld(X2,X1),X3)) = mult(X2,rd(X1,X3)),
inference(orient,[status(thm)],[t1176]) ).
cnf(t1704,plain,
mult(ld(X1,X2),X3) = ld(mult(X1,rd(X2,X3)),mult(X2,X2)),
inference(cp,[status(thm)],[t115,t1676]) ).
cnf(t2306,plain,
ld(mult(X1,rd(X2,X3)),mult(X2,X2)) = mult(ld(X1,X2),X3),
inference(orient,[status(thm)],[t1704]) ).
cnf(t2318,plain,
mult(ld(X1,X2),ld(X3,X2)) = ld(mult(X1,X3),mult(X2,X2)),
inference(cp,[status(thm)],[t2306,t114]) ).
cnf(t2369,plain,
ld(mult(X1,X2),mult(X3,X3)) = mult(ld(X1,X3),ld(X2,X3)),
inference(orient,[status(thm)],[t2318]) ).
cnf(t2376,plain,
mult(ld(X1,X2),ld(ld(X1,X3),X2)) = ld(X3,mult(X2,X2)),
inference(cp,[status(thm)],[t2369,t7]) ).
cnf(t2735,plain,
mult(ld(X1,X2),ld(ld(X1,X3),X2)) = ld(X3,mult(X2,X2)),
inference(orient,[status(thm)],[t2376]) ).
cnf(t2777,plain,
ld(ld(X1,X2),X3) = ld(ld(X1,X3),ld(X2,mult(X3,X3))),
inference(cp,[status(thm)],[t11,t2735]) ).
cnf(t3354,plain,
ld(ld(X1,X2),ld(X3,mult(X2,X2))) = ld(ld(X1,X3),X2),
inference(orient,[status(thm)],[t2777]) ).
cnf(t360910,plain,
mult(mult(X1,X1),ld(X2,mult(X1,X3))) = mult(X1,mult(X1,ld(ld(X1,X2),X3))),
inference(step,[status(thm)],[t229243,t3354]) ).
cnf(t229927,plain,
mult(mult(X1,X1),ld(X2,mult(X1,X3))) = mult(X1,mult(X1,ld(ld(X1,X2),X3))),
inference(orient,[status(thm)],[t360910]) ).
cnf(t230282,plain,
ld(X1,mult(X2,X3)) = ld(mult(X2,X2),mult(X2,mult(X2,ld(ld(X2,X1),X3)))),
inference(cp,[status(thm)],[t11,t229927]) ).
cnf(t130202,plain,
mult(X1,ld(X2,mult(X1,ld(X1,mult(ld(X1,X3),Y3))))) = ld(mult(X1,X2),mult(X3,mult(X1,Y3))),
inference(cp,[status(thm)],[t130020,t140]) ).
cnf(t360733,plain,
mult(X1,ld(X2,mult(ld(X1,X3),Y3))) = ld(mult(X1,X2),mult(X3,mult(X1,Y3))),
inference(step,[status(thm)],[t130202,t7]) ).
cnf(t131169,plain,
ld(mult(X1,X2),mult(X3,mult(X1,Y3))) = mult(X1,ld(X2,mult(ld(X1,X3),Y3))),
inference(orient,[status(thm)],[t360733]) ).
cnf(t360911,plain,
ld(X1,mult(X2,X3)) = mult(X2,ld(X2,mult(ld(X2,X2),ld(ld(X2,X1),X3)))),
inference(step,[status(thm)],[t230282,t131169]) ).
cnf(t360912,plain,
ld(X1,mult(X2,X3)) = mult(ld(X2,X2),ld(ld(X2,X1),X3)),
inference(step,[status(thm)],[t360911,t7]) ).
cnf(t230631,plain,
mult(ld(X1,X1),ld(ld(X1,X2),X3)) = ld(X2,mult(X1,X3)),
inference(orient,[status(thm)],[t360912]) ).
cnf(t230790,plain,
ld(mult(X1,X2),mult(X1,X3)) = mult(ld(X1,X1),ld(X2,X3)),
inference(cp,[status(thm)],[t230631,t11]) ).
cnf(t231922,plain,
ld(mult(X1,X2),mult(X1,X3)) = mult(ld(X1,X1),ld(X2,X3)),
inference(orient,[status(thm)],[t230790]) ).
cnf(t232509,plain,
rd(mult(mult(X1,X2),X1),X3) = rd(mult(X1,X1),mult(ld(X1,X1),ld(X2,X3))),
inference(cp,[status(thm)],[t2667,t231922]) ).
cnf(t360914,plain,
rd(mult(mult(X1,X2),X1),X3) = mult(X1,rd(X1,ld(X2,X3))),
inference(step,[status(thm)],[t232509,t1676]) ).
cnf(t233976,plain,
mult(X1,rd(X1,ld(X2,X3))) = rd(mult(mult(X1,X2),X1),X3),
inference(orient,[status(thm)],[t360914]) ).
cnf(t234216,plain,
rd(mult(mult(X1,rd(X2,X3)),X1),X2) = mult(X1,rd(X1,X3)),
inference(cp,[status(thm)],[t233976,t115]) ).
cnf(t1780,plain,
rd(mult(X1,X2),mult(ld(X3,X1),Y3)) = rd(mult(mult(X3,rd(X1,Y3)),X2),X1),
inference(cp,[status(thm)],[t1766,t1676]) ).
cnf(t9696,plain,
rd(mult(mult(X1,rd(X2,X3)),Y3),X2) = rd(mult(X2,Y3),mult(ld(X1,X2),X3)),
inference(orient,[status(thm)],[t1780]) ).
cnf(t360915,plain,
rd(mult(X2,X1),mult(ld(X1,X2),X3)) = mult(X1,rd(X1,X3)),
inference(step,[status(thm)],[t234216,t9696]) ).
cnf(t240453,plain,
rd(mult(X1,X2),mult(ld(X2,X1),X3)) = mult(X2,rd(X2,X3)),
inference(orient,[status(thm)],[t360915]) ).
cnf(t240888,plain,
mult(ld(X1,X2),X3) = ld(mult(X1,rd(X1,X3)),mult(X2,X1)),
inference(cp,[status(thm)],[t115,t240453]) ).
cnf(t2712,plain,
ld(X1,mult(X2,X3)) = ld(rd(mult(X1,X2),X3),mult(X2,X2)),
inference(cp,[status(thm)],[t115,t2667]) ).
cnf(t3108,plain,
ld(rd(mult(X1,X2),X3),mult(X2,X2)) = ld(X1,mult(X2,X3)),
inference(orient,[status(thm)],[t2712]) ).
cnf(t3112,plain,
ld(X1,mult(X2,ld(X3,mult(X1,X1)))) = ld(rd(mult(X3,X2),X1),mult(X2,X2)),
inference(cp,[status(thm)],[t3108,t1344]) ).
cnf(t360142,plain,
ld(X1,mult(X2,ld(X3,mult(X1,X1)))) = ld(X3,mult(X2,X1)),
inference(step,[status(thm)],[t3112,t3108]) ).
cnf(t3486,plain,
ld(X1,mult(X2,ld(X3,mult(X1,X1)))) = ld(X3,mult(X2,X1)),
inference(orient,[status(thm)],[t360142]) ).
cnf(t3505,plain,
ld(rd(mult(X1,X2),X3),mult(Y3,X2)) = ld(X2,mult(Y3,ld(X1,mult(X2,X3)))),
inference(cp,[status(thm)],[t3486,t3108]) ).
cnf(t15677,plain,
ld(rd(mult(X1,X2),X3),mult(Y3,X2)) = ld(X2,mult(Y3,ld(X1,mult(X2,X3)))),
inference(orient,[status(thm)],[t3505]) ).
cnf(t15684,plain,
ld(X1,mult(X2,ld(X1,mult(X1,mult(ld(X3,X1),Y3))))) = ld(mult(X3,rd(X1,Y3)),mult(X2,X1)),
inference(cp,[status(thm)],[t15677,t1676]) ).
cnf(t360231,plain,
ld(X1,mult(X2,mult(ld(X3,X1),Y3))) = ld(mult(X3,rd(X1,Y3)),mult(X2,X1)),
inference(step,[status(thm)],[t15684,t11]) ).
cnf(t18816,plain,
ld(mult(X1,rd(X2,X3)),mult(Y3,X2)) = ld(X2,mult(Y3,mult(ld(X1,X2),X3))),
inference(orient,[status(thm)],[t360231]) ).
cnf(t360934,plain,
mult(ld(X1,X2),X3) = ld(X1,mult(X2,mult(ld(X1,X1),X3))),
inference(step,[status(thm)],[t240888,t18816]) ).
cnf(t261812,plain,
ld(X1,mult(X2,mult(ld(X1,X1),X3))) = mult(ld(X1,X2),X3),
inference(orient,[status(thm)],[t360934]) ).
cnf(t18856,plain,
ld(X1,mult(X2,mult(ld(X3,X1),ld(Y3,X1)))) = ld(mult(X3,Y3),mult(X2,X1)),
inference(cp,[status(thm)],[t18816,t114]) ).
cnf(t212355,plain,
ld(X1,mult(X2,mult(ld(X3,X1),ld(Y3,X1)))) = ld(mult(X3,Y3),mult(X2,X1)),
inference(orient,[status(thm)],[t18856]) ).
cnf(t261813,plain,
mult(ld(X1,X2),ld(X3,X1)) = ld(mult(X1,X3),mult(X2,X1)),
inference(cp,[status(thm)],[t261812,t212355]) ).
cnf(t262426,plain,
ld(mult(X1,X2),mult(X3,X1)) = mult(ld(X1,X3),ld(X2,X1)),
inference(orient,[status(thm)],[t261813]) ).
cnf(t262429,plain,
mult(ld(X1,mult(X1,X2)),ld(X3,X1)) = mult(X1,ld(X3,mult(X2,ld(X1,X1)))),
inference(cp,[status(thm)],[t262426,t130020]) ).
cnf(t360967,plain,
mult(X2,ld(X3,X1)) = mult(X1,ld(X3,mult(X2,ld(X1,X1)))),
inference(step,[status(thm)],[t262429,t11]) ).
cnf(t294928,plain,
mult(X1,ld(X2,mult(X3,ld(X1,X1)))) = mult(X3,ld(X2,X1)),
inference(orient,[status(thm)],[t360967]) ).
cnf(t295453,plain,
mult(mult(X1,X2),mult(X3,ld(X2,X2))) = mult(mult(X1,X1),mult(X3,ld(X1,X2))),
inference(cp,[status(thm)],[t159,t294928]) ).
cnf(t361040,plain,
mult(mult(X1,X2),mult(X3,ld(X2,X2))) = mult(mult(X1,X3),X2),
inference(step,[status(thm)],[t295453,t159]) ).
cnf(t359257,plain,
mult(mult(X1,X2),mult(X3,ld(X2,X2))) = mult(mult(X1,X3),X2),
inference(orient,[status(thm)],[t361040]) ).
cnf(goal_0,negated_conjecture,
mult(mult(a,c),mult(b,ld(c,c))) != mult(mult(a,b),c),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
mult(mult(a,b),c) != mult(mult(a,b),c),
inference(rw,[status(thm)],[goal_0,t359257]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP752-1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/0.36 % Computer : n005.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Wed Sep 23 15:56:17 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 120.61/17.83 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 120.61/17.83 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------