%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP721-1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n026.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:17 PM UTC 2026
% Result : Unsatisfiable 93.99s 13.03s
% Output : CNFRefutation 93.99s
% Verified :
% SZS Type : Refutation
% Derivation depth : 140
% Number of leaves : 7
% Syntax : Number of clauses : 404 ( 404 unt; 0 nHn; 3 RR)
% Number of literals : 404 ( 403 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 : 6 ( 6 usr; 3 con; 0-2 aty)
% Number of variables : 880 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t4,axiom,
mult(X1,ld(X1,X2)) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t8,plain,
mult(X1,ld(X1,X2)) = X2,
inference(orient,[status(thm)],[t4]) ).
cnf(t2,axiom,
ld(X1,mult(X1,X2)) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t12,plain,
ld(X1,mult(X1,X2)) = X2,
inference(orient,[status(thm)],[t2]) ).
cnf(t3,axiom,
mult(X1,X2) = mult(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t15,plain,
mult(X1,X2) = mult(X2,X1),
inference(orient,[status(thm)],[t3]) ).
cnf(t17,plain,
X1 = ld(X2,mult(X1,X2)),
inference(cp,[status(thm)],[t12,t15]) ).
cnf(t52,plain,
ld(X1,mult(X2,X1)) = X2,
inference(orient,[status(thm)],[t17]) ).
cnf(t53,plain,
X1 = ld(ld(X1,X2),X2),
inference(cp,[status(thm)],[t52,t8]) ).
cnf(t62,plain,
ld(ld(X1,X2),X2) = X1,
inference(orient,[status(thm)],[t53]) ).
cnf(t7,axiom,
mult(ld(mult(X1,X2),mult(X1,mult(X2,X3))),ld(mult(X1,X2),mult(X1,mult(X2,X4)))) = ld(mult(X1,X2),mult(X1,mult(X2,mult(X3,X4)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t19,plain,
mult(ld(mult(X1,X2),mult(X1,mult(X2,X3))),ld(mult(X1,X2),mult(X1,mult(X2,X4)))) = ld(mult(X1,X2),mult(X1,mult(X2,mult(X3,X4)))),
inference(orient,[status(thm)],[t7]) ).
cnf(t25,plain,
ld(mult(X1,X2),mult(X1,mult(X2,mult(ld(X2,X3),X4)))) = mult(ld(mult(X1,X2),mult(X1,X3)),ld(mult(X1,X2),mult(X1,mult(X2,X4)))),
inference(cp,[status(thm)],[t19,t8]) ).
cnf(t190617,plain,
ld(mult(X1,X2),mult(X1,mult(X2,mult(X4,ld(X2,X3))))) = mult(ld(mult(X1,X2),mult(X1,X3)),ld(mult(X1,X2),mult(X1,mult(X2,X4)))),
inference(step,[status(thm)],[t25,t15]) ).
cnf(t2034,plain,
mult(ld(mult(X1,X2),mult(X1,X3)),ld(mult(X1,X2),mult(X1,mult(X2,X4)))) = ld(mult(X1,X2),mult(X1,mult(X2,mult(X4,ld(X2,X3))))),
inference(orient,[status(thm)],[t190617]) ).
cnf(t2043,plain,
ld(mult(X1,X2),mult(X1,mult(X2,mult(X3,ld(X2,mult(X1,X2)))))) = mult(X1,ld(mult(X1,X2),mult(X1,mult(X2,X3)))),
inference(cp,[status(thm)],[t2034,t52]) ).
cnf(t190757,plain,
ld(mult(X1,X2),mult(X1,mult(X2,mult(X3,X1)))) = mult(X1,ld(mult(X1,X2),mult(X1,mult(X2,X3)))),
inference(step,[status(thm)],[t2043,t52]) ).
cnf(t190758,plain,
ld(mult(X1,X2),mult(X1,mult(X2,mult(X1,X3)))) = mult(X1,ld(mult(X1,X2),mult(X1,mult(X2,X3)))),
inference(step,[status(thm)],[t190757,t15]) ).
cnf(t5648,plain,
ld(mult(X1,X2),mult(X1,mult(X2,mult(X1,X3)))) = mult(X1,ld(mult(X1,X2),mult(X1,mult(X2,X3)))),
inference(orient,[status(thm)],[t190758]) ).
cnf(t21,plain,
ld(mult(X1,ld(X1,X2)),mult(X1,mult(ld(X1,X2),mult(X3,X4)))) = mult(ld(X2,mult(X1,mult(ld(X1,X2),X3))),ld(mult(X1,ld(X1,X2)),mult(X1,mult(ld(X1,X2),X4)))),
inference(cp,[status(thm)],[t19,t8]) ).
cnf(t190542,plain,
ld(X2,mult(X1,mult(ld(X1,X2),mult(X3,X4)))) = mult(ld(X2,mult(X1,mult(ld(X1,X2),X3))),ld(mult(X1,ld(X1,X2)),mult(X1,mult(ld(X1,X2),X4)))),
inference(step,[status(thm)],[t21,t8]) ).
cnf(t190543,plain,
ld(X2,mult(X1,mult(mult(X3,X4),ld(X1,X2)))) = mult(ld(X2,mult(X1,mult(ld(X1,X2),X3))),ld(mult(X1,ld(X1,X2)),mult(X1,mult(ld(X1,X2),X4)))),
inference(step,[status(thm)],[t190542,t15]) ).
cnf(t190544,plain,
ld(X2,mult(X1,mult(mult(X3,X4),ld(X1,X2)))) = mult(ld(X2,mult(X1,mult(X3,ld(X1,X2)))),ld(mult(X1,ld(X1,X2)),mult(X1,mult(ld(X1,X2),X4)))),
inference(step,[status(thm)],[t190543,t15]) ).
cnf(t190545,plain,
ld(X2,mult(X1,mult(mult(X3,X4),ld(X1,X2)))) = mult(ld(X2,mult(X1,mult(X3,ld(X1,X2)))),ld(X2,mult(X1,mult(ld(X1,X2),X4)))),
inference(step,[status(thm)],[t190544,t8]) ).
cnf(t190546,plain,
ld(X2,mult(X1,mult(mult(X3,X4),ld(X1,X2)))) = mult(ld(X2,mult(X1,mult(X3,ld(X1,X2)))),ld(X2,mult(X1,mult(X4,ld(X1,X2))))),
inference(step,[status(thm)],[t190545,t15]) ).
cnf(t538,plain,
mult(ld(X1,mult(X2,mult(X3,ld(X2,X1)))),ld(X1,mult(X2,mult(X4,ld(X2,X1))))) = ld(X1,mult(X2,mult(mult(X3,X4),ld(X2,X1)))),
inference(orient,[status(thm)],[t190546]) ).
cnf(t543,plain,
ld(X1,mult(X2,mult(mult(X2,X3),ld(X2,X1)))) = mult(ld(X1,mult(X2,X1)),ld(X1,mult(X2,mult(X3,ld(X2,X1))))),
inference(cp,[status(thm)],[t538,t8]) ).
cnf(t190721,plain,
ld(X1,mult(X2,mult(mult(X2,X3),ld(X2,X1)))) = mult(X2,ld(X1,mult(X2,mult(X3,ld(X2,X1))))),
inference(step,[status(thm)],[t543,t52]) ).
cnf(t3429,plain,
ld(X1,mult(X2,mult(mult(X2,X3),ld(X2,X1)))) = mult(X2,ld(X1,mult(X2,mult(X3,ld(X2,X1))))),
inference(orient,[status(thm)],[t190721]) ).
cnf(t0,axiom,
mult(X1,unit) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t9,plain,
mult(X1,unit) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t54,plain,
X1 = ld(unit,X1),
inference(cp,[status(thm)],[t52,t9]) ).
cnf(t59,plain,
ld(unit,X1) = X1,
inference(orient,[status(thm)],[t54]) ).
cnf(t3431,plain,
mult(X1,ld(unit,mult(X1,mult(X2,ld(X1,unit))))) = mult(X1,mult(mult(X1,X2),ld(X1,unit))),
inference(cp,[status(thm)],[t3429,t59]) ).
cnf(t190722,plain,
mult(X1,mult(X1,mult(X2,ld(X1,unit)))) = mult(X1,mult(mult(X1,X2),ld(X1,unit))),
inference(step,[status(thm)],[t3431,t59]) ).
cnf(t3532,plain,
mult(X1,mult(mult(X1,X2),ld(X1,unit))) = mult(X1,mult(X1,mult(X2,ld(X1,unit)))),
inference(orient,[status(thm)],[t190722]) ).
cnf(t3583,plain,
mult(mult(X1,X2),ld(X1,unit)) = ld(X1,mult(X1,mult(X1,mult(X2,ld(X1,unit))))),
inference(cp,[status(thm)],[t12,t3532]) ).
cnf(t190723,plain,
mult(mult(X1,X2),ld(X1,unit)) = mult(X1,mult(X2,ld(X1,unit))),
inference(step,[status(thm)],[t3583,t12]) ).
cnf(t3605,plain,
mult(mult(X1,X2),ld(X1,unit)) = mult(X1,mult(X2,ld(X1,unit))),
inference(orient,[status(thm)],[t190723]) ).
cnf(t3608,plain,
mult(X1,mult(ld(X1,X2),ld(X1,unit))) = mult(X2,ld(X1,unit)),
inference(cp,[status(thm)],[t3605,t8]) ).
cnf(t3674,plain,
mult(X1,mult(ld(X1,X2),ld(X1,unit))) = mult(X2,ld(X1,unit)),
inference(orient,[status(thm)],[t3608]) ).
cnf(t3715,plain,
mult(X1,ld(ld(X2,X1),unit)) = mult(ld(X2,X1),mult(X2,ld(ld(X2,X1),unit))),
inference(cp,[status(thm)],[t3674,t62]) ).
cnf(t4536,plain,
mult(ld(X1,X2),mult(X1,ld(ld(X1,X2),unit))) = mult(X2,ld(ld(X1,X2),unit)),
inference(orient,[status(thm)],[t3715]) ).
cnf(t5699,plain,
mult(X1,ld(mult(X1,ld(X1,X2)),mult(X1,mult(ld(X1,X2),ld(ld(X1,X2),unit))))) = ld(mult(X1,ld(X1,X2)),mult(X1,mult(X2,ld(ld(X1,X2),unit)))),
inference(cp,[status(thm)],[t5648,t4536]) ).
cnf(t190760,plain,
mult(X1,ld(X2,mult(X1,mult(ld(X1,X2),ld(ld(X1,X2),unit))))) = ld(mult(X1,ld(X1,X2)),mult(X1,mult(X2,ld(ld(X1,X2),unit)))),
inference(step,[status(thm)],[t5699,t8]) ).
cnf(t190761,plain,
mult(X1,ld(X2,mult(X1,unit))) = ld(mult(X1,ld(X1,X2)),mult(X1,mult(X2,ld(ld(X1,X2),unit)))),
inference(step,[status(thm)],[t190760,t8]) ).
cnf(t190762,plain,
mult(X1,ld(X2,X1)) = ld(mult(X1,ld(X1,X2)),mult(X1,mult(X2,ld(ld(X1,X2),unit)))),
inference(step,[status(thm)],[t190761,t9]) ).
cnf(t190763,plain,
mult(X1,ld(X2,X1)) = ld(X2,mult(X1,mult(X2,ld(ld(X1,X2),unit)))),
inference(step,[status(thm)],[t190762,t8]) ).
cnf(t5777,plain,
ld(X1,mult(X2,mult(X1,ld(ld(X2,X1),unit)))) = mult(X2,ld(X1,X2)),
inference(orient,[status(thm)],[t190763]) ).
cnf(t5824,plain,
mult(X1,mult(X2,ld(ld(X1,X2),unit))) = mult(X2,mult(X1,ld(X2,X1))),
inference(cp,[status(thm)],[t8,t5777]) ).
cnf(t5869,plain,
mult(X1,mult(X2,ld(ld(X1,X2),unit))) = mult(X2,mult(X1,ld(X2,X1))),
inference(orient,[status(thm)],[t5824]) ).
cnf(t5923,plain,
mult(X1,ld(ld(X2,X1),unit)) = ld(X2,mult(X1,mult(X2,ld(X1,X2)))),
inference(cp,[status(thm)],[t12,t5869]) ).
cnf(t5947,plain,
ld(X1,mult(X2,mult(X1,ld(X2,X1)))) = mult(X2,ld(ld(X1,X2),unit)),
inference(orient,[status(thm)],[t5923]) ).
cnf(t5948,plain,
mult(X1,ld(ld(mult(X1,X2),X1),unit)) = mult(X1,ld(mult(X1,X2),mult(X1,mult(X2,ld(X1,mult(X1,X2)))))),
inference(cp,[status(thm)],[t5947,t3429]) ).
cnf(t190781,plain,
mult(X1,ld(ld(mult(X1,X2),X1),unit)) = mult(X1,ld(mult(X1,X2),mult(X1,mult(X2,X2)))),
inference(step,[status(thm)],[t5948,t12]) ).
cnf(t6620,plain,
mult(X1,ld(mult(X1,X2),mult(X1,mult(X2,X2)))) = mult(X1,ld(ld(mult(X1,X2),X1),unit)),
inference(orient,[status(thm)],[t190781]) ).
cnf(t6678,plain,
ld(mult(X1,X2),mult(X1,mult(X2,X2))) = ld(X1,mult(X1,ld(ld(mult(X1,X2),X1),unit))),
inference(cp,[status(thm)],[t12,t6620]) ).
cnf(t190782,plain,
ld(mult(X1,X2),mult(X1,mult(X2,X2))) = ld(ld(mult(X1,X2),X1),unit),
inference(step,[status(thm)],[t6678,t12]) ).
cnf(t6707,plain,
ld(mult(X1,X2),mult(X1,mult(X2,X2))) = ld(ld(mult(X1,X2),X1),unit),
inference(orient,[status(thm)],[t190782]) ).
cnf(t6713,plain,
ld(ld(mult(X1,ld(X1,X2)),X1),unit) = ld(X2,mult(X1,mult(ld(X1,X2),ld(X1,X2)))),
inference(cp,[status(thm)],[t6707,t8]) ).
cnf(t190783,plain,
ld(ld(X2,X1),unit) = ld(X2,mult(X1,mult(ld(X1,X2),ld(X1,X2)))),
inference(step,[status(thm)],[t6713,t8]) ).
cnf(t6795,plain,
ld(X1,mult(X2,mult(ld(X2,X1),ld(X2,X1)))) = ld(ld(X1,X2),unit),
inference(orient,[status(thm)],[t190783]) ).
cnf(t6898,plain,
mult(X1,mult(ld(X1,X2),ld(X1,X2))) = mult(X2,ld(ld(X2,X1),unit)),
inference(cp,[status(thm)],[t8,t6795]) ).
cnf(t7161,plain,
mult(X1,mult(ld(X1,X2),ld(X1,X2))) = mult(X2,ld(ld(X2,X1),unit)),
inference(orient,[status(thm)],[t6898]) ).
cnf(t7301,plain,
ld(mult(X1,ld(X1,X2)),mult(X1,mult(ld(X1,X2),mult(ld(X1,X2),ld(ld(X1,X2),X3))))) = mult(ld(mult(X1,ld(X1,X2)),mult(X1,X3)),ld(mult(X1,ld(X1,X2)),mult(X2,ld(ld(X2,X1),unit)))),
inference(cp,[status(thm)],[t2034,t7161]) ).
cnf(t190796,plain,
ld(X2,mult(X1,mult(ld(X1,X2),mult(ld(X1,X2),ld(ld(X1,X2),X3))))) = mult(ld(mult(X1,ld(X1,X2)),mult(X1,X3)),ld(mult(X1,ld(X1,X2)),mult(X2,ld(ld(X2,X1),unit)))),
inference(step,[status(thm)],[t7301,t8]) ).
cnf(t190797,plain,
ld(X2,mult(X1,mult(ld(X1,X2),X3))) = mult(ld(mult(X1,ld(X1,X2)),mult(X1,X3)),ld(mult(X1,ld(X1,X2)),mult(X2,ld(ld(X2,X1),unit)))),
inference(step,[status(thm)],[t190796,t8]) ).
cnf(t190798,plain,
ld(X2,mult(X1,mult(X3,ld(X1,X2)))) = mult(ld(mult(X1,ld(X1,X2)),mult(X1,X3)),ld(mult(X1,ld(X1,X2)),mult(X2,ld(ld(X2,X1),unit)))),
inference(step,[status(thm)],[t190797,t15]) ).
cnf(t190799,plain,
ld(X2,mult(X1,mult(X3,ld(X1,X2)))) = mult(ld(X2,mult(X1,X3)),ld(mult(X1,ld(X1,X2)),mult(X2,ld(ld(X2,X1),unit)))),
inference(step,[status(thm)],[t190798,t8]) ).
cnf(t190800,plain,
ld(X2,mult(X1,mult(X3,ld(X1,X2)))) = mult(ld(X2,mult(X1,X3)),ld(X2,mult(X2,ld(ld(X2,X1),unit)))),
inference(step,[status(thm)],[t190799,t8]) ).
cnf(t190801,plain,
ld(X2,mult(X1,mult(X3,ld(X1,X2)))) = mult(ld(X2,mult(X1,X3)),ld(ld(X2,X1),unit)),
inference(step,[status(thm)],[t190800,t12]) ).
cnf(t8279,plain,
mult(ld(X1,mult(X2,X3)),ld(ld(X1,X2),unit)) = ld(X1,mult(X2,mult(X3,ld(X2,X1)))),
inference(orient,[status(thm)],[t190801]) ).
cnf(t8319,plain,
ld(X1,mult(X2,mult(ld(X2,X3),ld(X2,X1)))) = mult(ld(X1,X3),ld(ld(X1,X2),unit)),
inference(cp,[status(thm)],[t8279,t8]) ).
cnf(t190809,plain,
ld(X1,mult(X2,mult(ld(X2,X1),ld(X2,X3)))) = mult(ld(X1,X3),ld(ld(X1,X2),unit)),
inference(step,[status(thm)],[t8319,t15]) ).
cnf(t9347,plain,
ld(X1,mult(X2,mult(ld(X2,X1),ld(X2,X3)))) = mult(ld(X1,X3),ld(ld(X1,X2),unit)),
inference(orient,[status(thm)],[t190809]) ).
cnf(t9351,plain,
mult(ld(X1,unit),ld(ld(X1,X2),unit)) = ld(X1,mult(X1,ld(X2,unit))),
inference(cp,[status(thm)],[t9347,t3674]) ).
cnf(t190810,plain,
mult(ld(X1,unit),ld(ld(X1,X2),unit)) = ld(X2,unit),
inference(step,[status(thm)],[t9351,t12]) ).
cnf(t9552,plain,
mult(ld(X1,unit),ld(ld(X1,X2),unit)) = ld(X2,unit),
inference(orient,[status(thm)],[t190810]) ).
cnf(t9573,plain,
ld(mult(X1,X2),unit) = mult(ld(X1,unit),ld(X2,unit)),
inference(cp,[status(thm)],[t9552,t12]) ).
cnf(t9675,plain,
mult(ld(X1,unit),ld(X2,unit)) = ld(mult(X1,X2),unit),
inference(orient,[status(thm)],[t9573]) ).
cnf(t9696,plain,
ld(mult(ld(X1,unit),X2),unit) = mult(X1,ld(X2,unit)),
inference(cp,[status(thm)],[t9675,t62]) ).
cnf(t190811,plain,
ld(mult(X2,ld(X1,unit)),unit) = mult(X1,ld(X2,unit)),
inference(step,[status(thm)],[t9696,t15]) ).
cnf(t9802,plain,
ld(mult(X1,ld(X2,unit)),unit) = mult(X2,ld(X1,unit)),
inference(orient,[status(thm)],[t190811]) ).
cnf(t9811,plain,
mult(ld(X1,X2),ld(ld(X1,mult(X2,X3)),unit)) = ld(ld(X1,mult(X2,mult(X3,ld(X2,X1)))),unit),
inference(cp,[status(thm)],[t9802,t8279]) ).
cnf(t36927,plain,
ld(ld(X1,mult(X2,mult(X3,ld(X2,X1)))),unit) = mult(ld(X1,X2),ld(ld(X1,mult(X2,X3)),unit)),
inference(orient,[status(thm)],[t9811]) ).
cnf(t36945,plain,
mult(ld(X1,X2),ld(ld(X1,mult(X2,X2)),unit)) = ld(ld(X1,mult(X2,X1)),unit),
inference(cp,[status(thm)],[t36927,t8]) ).
cnf(t191017,plain,
mult(ld(X1,X2),ld(ld(X1,mult(X2,X2)),unit)) = ld(X2,unit),
inference(step,[status(thm)],[t36945,t52]) ).
cnf(t37413,plain,
mult(ld(X1,X2),ld(ld(X1,mult(X2,X2)),unit)) = ld(X2,unit),
inference(orient,[status(thm)],[t191017]) ).
cnf(t37574,plain,
ld(ld(X1,mult(X2,X2)),unit) = ld(ld(X1,X2),ld(X2,unit)),
inference(cp,[status(thm)],[t12,t37413]) ).
cnf(t37661,plain,
ld(ld(X1,mult(X2,X2)),unit) = ld(ld(X1,X2),ld(X2,unit)),
inference(orient,[status(thm)],[t37574]) ).
cnf(t37722,plain,
ld(X1,mult(X2,X2)) = ld(ld(ld(X1,X2),ld(X2,unit)),unit),
inference(cp,[status(thm)],[t62,t37661]) ).
cnf(t9716,plain,
ld(X1,unit) = ld(ld(X2,unit),ld(mult(X1,X2),unit)),
inference(cp,[status(thm)],[t52,t9675]) ).
cnf(t9934,plain,
ld(ld(X1,unit),ld(mult(X2,X1),unit)) = ld(X2,unit),
inference(orient,[status(thm)],[t9716]) ).
cnf(t9954,plain,
ld(X1,unit) = ld(ld(ld(X1,X2),unit),ld(X2,unit)),
inference(cp,[status(thm)],[t9934,t8]) ).
cnf(t10040,plain,
ld(ld(ld(X1,X2),unit),ld(X2,unit)) = ld(X1,unit),
inference(orient,[status(thm)],[t9954]) ).
cnf(t10078,plain,
ld(ld(X1,X2),unit) = ld(ld(X1,unit),ld(X2,unit)),
inference(cp,[status(thm)],[t10040,t62]) ).
cnf(t10146,plain,
ld(ld(X1,unit),ld(X2,unit)) = ld(ld(X1,X2),unit),
inference(orient,[status(thm)],[t10078]) ).
cnf(t10172,plain,
ld(ld(X1,ld(X2,unit)),unit) = ld(ld(X1,unit),X2),
inference(cp,[status(thm)],[t10146,t62]) ).
cnf(t10382,plain,
ld(ld(X1,ld(X2,unit)),unit) = ld(ld(X1,unit),X2),
inference(orient,[status(thm)],[t10172]) ).
cnf(t191024,plain,
ld(X1,mult(X2,X2)) = ld(ld(ld(X1,X2),unit),X2),
inference(step,[status(thm)],[t37722,t10382]) ).
cnf(t38017,plain,
ld(ld(ld(X1,X2),unit),X2) = ld(X1,mult(X2,X2)),
inference(orient,[status(thm)],[t191024]) ).
cnf(t38114,plain,
ld(ld(X1,X2),mult(X2,X2)) = ld(ld(X1,unit),X2),
inference(cp,[status(thm)],[t38017,t62]) ).
cnf(t38305,plain,
ld(ld(X1,X2),mult(X2,X2)) = ld(ld(X1,unit),X2),
inference(orient,[status(thm)],[t38114]) ).
cnf(t38397,plain,
mult(X1,X1) = mult(ld(X2,X1),ld(ld(X2,unit),X1)),
inference(cp,[status(thm)],[t8,t38305]) ).
cnf(t39019,plain,
mult(ld(X1,X2),ld(ld(X1,unit),X2)) = mult(X2,X2),
inference(orient,[status(thm)],[t38397]) ).
cnf(t39102,plain,
mult(ld(X1,unit),ld(X1,unit)) = mult(ld(ld(X2,X1),unit),ld(ld(ld(X2,unit),unit),ld(X1,unit))),
inference(cp,[status(thm)],[t39019,t10146]) ).
cnf(t191058,plain,
ld(mult(X1,X1),unit) = mult(ld(ld(X2,X1),unit),ld(ld(ld(X2,unit),unit),ld(X1,unit))),
inference(step,[status(thm)],[t39102,t9675]) ).
cnf(t57,plain,
ld(mult(X1,X1),mult(X1,mult(X1,mult(X1,X2)))) = mult(X1,ld(mult(X1,X1),mult(X1,mult(X1,X2)))),
inference(cp,[status(thm)],[t19,t52]) ).
cnf(t399,plain,
ld(mult(X1,X1),mult(X1,mult(X1,mult(X1,X2)))) = mult(X1,ld(mult(X1,X1),mult(X1,mult(X1,X2)))),
inference(orient,[status(thm)],[t57]) ).
cnf(t402,plain,
mult(X1,ld(mult(X1,X1),mult(X1,mult(X1,ld(X1,X2))))) = ld(mult(X1,X1),mult(X1,mult(X1,X2))),
inference(cp,[status(thm)],[t399,t8]) ).
cnf(t190533,plain,
mult(X1,ld(mult(X1,X1),mult(X1,X2))) = ld(mult(X1,X1),mult(X1,mult(X1,X2))),
inference(step,[status(thm)],[t402,t8]) ).
cnf(t421,plain,
ld(mult(X1,X1),mult(X1,mult(X1,X2))) = mult(X1,ld(mult(X1,X1),mult(X1,X2))),
inference(orient,[status(thm)],[t190533]) ).
cnf(t424,plain,
mult(X1,ld(mult(X1,X1),mult(X1,ld(X1,X2)))) = ld(mult(X1,X1),mult(X1,X2)),
inference(cp,[status(thm)],[t421,t8]) ).
cnf(t190563,plain,
mult(X1,ld(mult(X1,X1),X2)) = ld(mult(X1,X1),mult(X1,X2)),
inference(step,[status(thm)],[t424,t8]) ).
cnf(t786,plain,
ld(mult(X1,X1),mult(X1,X2)) = mult(X1,ld(mult(X1,X1),X2)),
inference(orient,[status(thm)],[t190563]) ).
cnf(t793,plain,
mult(X1,ld(mult(X1,X1),unit)) = ld(mult(X1,X1),X1),
inference(cp,[status(thm)],[t786,t9]) ).
cnf(t426,plain,
mult(X1,ld(mult(X1,X1),mult(X1,unit))) = ld(mult(X1,X1),mult(X1,X1)),
inference(cp,[status(thm)],[t421,t9]) ).
cnf(t190534,plain,
mult(X1,ld(mult(X1,X1),X1)) = ld(mult(X1,X1),mult(X1,X1)),
inference(step,[status(thm)],[t426,t9]) ).
cnf(t13,plain,
unit = ld(X1,X1),
inference(cp,[status(thm)],[t12,t9]) ).
cnf(t51,plain,
ld(X1,X1) = unit,
inference(orient,[status(thm)],[t13]) ).
cnf(t190535,plain,
mult(X1,ld(mult(X1,X1),X1)) = unit,
inference(step,[status(thm)],[t190534,t51]) ).
cnf(t444,plain,
mult(X1,ld(mult(X1,X1),X1)) = unit,
inference(orient,[status(thm)],[t190535]) ).
cnf(t448,plain,
ld(mult(X1,X1),X1) = ld(X1,unit),
inference(cp,[status(thm)],[t12,t444]) ).
cnf(t464,plain,
ld(mult(X1,X1),X1) = ld(X1,unit),
inference(orient,[status(thm)],[t448]) ).
cnf(t190564,plain,
mult(X1,ld(mult(X1,X1),unit)) = ld(X1,unit),
inference(step,[status(thm)],[t793,t464]) ).
cnf(t819,plain,
mult(X1,ld(mult(X1,X1),unit)) = ld(X1,unit),
inference(orient,[status(thm)],[t190564]) ).
cnf(t826,plain,
ld(mult(X1,X1),unit) = ld(X1,ld(X1,unit)),
inference(cp,[status(thm)],[t12,t819]) ).
cnf(t843,plain,
ld(mult(X1,X1),unit) = ld(X1,ld(X1,unit)),
inference(orient,[status(thm)],[t826]) ).
cnf(t191059,plain,
ld(X1,ld(X1,unit)) = mult(ld(ld(X2,X1),unit),ld(ld(ld(X2,unit),unit),ld(X1,unit))),
inference(step,[status(thm)],[t191058,t843]) ).
cnf(t191060,plain,
ld(X1,ld(X1,unit)) = mult(ld(ld(X2,X1),unit),ld(ld(ld(X2,unit),X1),unit)),
inference(step,[status(thm)],[t191059,t10146]) ).
cnf(t10160,plain,
ld(ld(ld(X1,unit),X2),unit) = ld(X1,ld(X2,unit)),
inference(cp,[status(thm)],[t10146,t62]) ).
cnf(t10229,plain,
ld(ld(ld(X1,unit),X2),unit) = ld(X1,ld(X2,unit)),
inference(orient,[status(thm)],[t10160]) ).
cnf(t191061,plain,
ld(X1,ld(X1,unit)) = mult(ld(ld(X2,X1),unit),ld(X2,ld(X1,unit))),
inference(step,[status(thm)],[t191060,t10229]) ).
cnf(t191062,plain,
ld(X1,ld(X1,unit)) = mult(ld(X2,ld(X1,unit)),ld(ld(X2,X1),unit)),
inference(step,[status(thm)],[t191061,t15]) ).
cnf(t42365,plain,
mult(ld(X1,ld(X2,unit)),ld(ld(X1,X2),unit)) = ld(X2,ld(X2,unit)),
inference(orient,[status(thm)],[t191062]) ).
cnf(t10274,plain,
mult(ld(ld(X1,unit),X2),ld(X3,unit)) = ld(mult(X3,ld(X1,ld(X2,unit))),unit),
inference(cp,[status(thm)],[t9802,t10229]) ).
cnf(t190827,plain,
mult(ld(X3,unit),ld(ld(X1,unit),X2)) = ld(mult(X3,ld(X1,ld(X2,unit))),unit),
inference(step,[status(thm)],[t10274,t15]) ).
cnf(t14020,plain,
ld(mult(X1,ld(X2,ld(X3,unit))),unit) = mult(ld(X1,unit),ld(ld(X2,unit),X3)),
inference(orient,[status(thm)],[t190827]) ).
cnf(t7276,plain,
X1 = ld(mult(ld(X1,X2),ld(X1,X2)),mult(X2,ld(ld(X2,X1),unit))),
inference(cp,[status(thm)],[t52,t7161]) ).
cnf(t28934,plain,
ld(mult(ld(X1,X2),ld(X1,X2)),mult(X2,ld(ld(X2,X1),unit))) = X1,
inference(orient,[status(thm)],[t7276]) ).
cnf(t3435,plain,
mult(X1,ld(X2,mult(X1,mult(ld(X1,X3),ld(X1,X2))))) = ld(X2,mult(X1,mult(X3,ld(X1,X2)))),
inference(cp,[status(thm)],[t3429,t8]) ).
cnf(t191569,plain,
mult(X1,ld(X2,mult(X1,mult(ld(X1,X2),ld(X1,X3))))) = ld(X2,mult(X1,mult(X3,ld(X1,X2)))),
inference(step,[status(thm)],[t3435,t15]) ).
cnf(t191570,plain,
mult(X1,mult(ld(X2,X3),ld(ld(X2,X1),unit))) = ld(X2,mult(X1,mult(X3,ld(X1,X2)))),
inference(step,[status(thm)],[t191569,t9347]) ).
cnf(t123541,plain,
mult(X1,mult(ld(X2,X3),ld(ld(X2,X1),unit))) = ld(X2,mult(X1,mult(X3,ld(X1,X2)))),
inference(orient,[status(thm)],[t191570]) ).
cnf(t124075,plain,
mult(ld(X1,X2),ld(ld(X1,X3),unit)) = ld(X3,ld(X1,mult(X3,mult(X2,ld(X3,X1))))),
inference(cp,[status(thm)],[t12,t123541]) ).
cnf(t124861,plain,
ld(X1,ld(X2,mult(X1,mult(X3,ld(X1,X2))))) = mult(ld(X2,X3),ld(ld(X2,X1),unit)),
inference(orient,[status(thm)],[t124075]) ).
cnf(t124866,plain,
mult(ld(X1,ld(X2,X1)),ld(ld(X1,X2),unit)) = ld(X2,mult(ld(X1,X1),ld(ld(X1,X2),unit))),
inference(cp,[status(thm)],[t124861,t9347]) ).
cnf(t191571,plain,
mult(ld(X1,ld(X2,X1)),ld(ld(X1,X2),unit)) = ld(X2,mult(unit,ld(ld(X1,X2),unit))),
inference(step,[status(thm)],[t124866,t51]) ).
cnf(t5,axiom,
ld(mult(ld(mult(X1,X2),X1),ld(mult(X1,X2),X2)),unit) = f(X1,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t40,plain,
ld(mult(ld(mult(X1,X2),X1),ld(mult(X1,X2),X2)),unit) = f(X1,X2),
inference(orient,[status(thm)],[t5]) ).
cnf(t43,plain,
f(X1,unit) = ld(mult(ld(X1,X1),ld(mult(X1,unit),unit)),unit),
inference(cp,[status(thm)],[t40,t9]) ).
cnf(t190503,plain,
f(X1,unit) = ld(mult(unit,ld(mult(X1,unit),unit)),unit),
inference(step,[status(thm)],[t43,t51]) ).
cnf(t190504,plain,
f(X1,unit) = ld(mult(unit,ld(X1,unit)),unit),
inference(step,[status(thm)],[t190503,t9]) ).
cnf(t82,plain,
ld(mult(unit,ld(X1,unit)),unit) = f(X1,unit),
inference(orient,[status(thm)],[t190504]) ).
cnf(t86,plain,
mult(unit,ld(X1,unit)) = ld(f(X1,unit),unit),
inference(cp,[status(thm)],[t62,t82]) ).
cnf(t83,plain,
f(ld(X1,unit),unit) = ld(mult(unit,X1),unit),
inference(cp,[status(thm)],[t82,t62]) ).
cnf(t190505,plain,
f(ld(X1,unit),unit) = ld(mult(X1,unit),unit),
inference(step,[status(thm)],[t83,t15]) ).
cnf(t190506,plain,
f(ld(X1,unit),unit) = ld(X1,unit),
inference(step,[status(thm)],[t190505,t9]) ).
cnf(t89,plain,
f(ld(X1,unit),unit) = ld(X1,unit),
inference(orient,[status(thm)],[t190506]) ).
cnf(t90,plain,
ld(ld(X1,unit),unit) = f(X1,unit),
inference(cp,[status(thm)],[t89,t62]) ).
cnf(t190507,plain,
X1 = f(X1,unit),
inference(step,[status(thm)],[t90,t62]) ).
cnf(t93,plain,
f(X1,unit) = X1,
inference(orient,[status(thm)],[t190507]) ).
cnf(t190510,plain,
mult(unit,ld(X1,unit)) = ld(X1,unit),
inference(step,[status(thm)],[t86,t93]) ).
cnf(t96,plain,
mult(unit,ld(X1,unit)) = ld(X1,unit),
inference(orient,[status(thm)],[t190510]) ).
cnf(t191572,plain,
mult(ld(X1,ld(X2,X1)),ld(ld(X1,X2),unit)) = ld(X2,ld(ld(X1,X2),unit)),
inference(step,[status(thm)],[t191571,t96]) ).
cnf(t125415,plain,
mult(ld(X1,ld(X2,X1)),ld(ld(X1,X2),unit)) = ld(X2,ld(ld(X1,X2),unit)),
inference(orient,[status(thm)],[t191572]) ).
cnf(t125608,plain,
ld(ld(X1,unit),ld(ld(ld(X2,unit),ld(X1,unit)),unit)) = mult(ld(ld(X2,unit),ld(ld(X1,X2),unit)),ld(ld(ld(X2,unit),ld(X1,unit)),unit)),
inference(cp,[status(thm)],[t125415,t10146]) ).
cnf(t191584,plain,
ld(ld(X1,ld(ld(X2,unit),ld(X1,unit))),unit) = mult(ld(ld(X2,unit),ld(ld(X1,X2),unit)),ld(ld(ld(X2,unit),ld(X1,unit)),unit)),
inference(step,[status(thm)],[t125608,t10146]) ).
cnf(t10260,plain,
ld(ld(X1,ld(ld(X2,unit),X3)),unit) = ld(ld(X1,unit),ld(X2,ld(X3,unit))),
inference(cp,[status(thm)],[t10146,t10229]) ).
cnf(t13437,plain,
ld(ld(X1,ld(ld(X2,unit),X3)),unit) = ld(ld(X1,unit),ld(X2,ld(X3,unit))),
inference(orient,[status(thm)],[t10260]) ).
cnf(t191585,plain,
ld(ld(X1,unit),ld(X2,ld(ld(X1,unit),unit))) = mult(ld(ld(X2,unit),ld(ld(X1,X2),unit)),ld(ld(ld(X2,unit),ld(X1,unit)),unit)),
inference(step,[status(thm)],[t191584,t13437]) ).
cnf(t191586,plain,
ld(ld(X1,unit),ld(X2,X1)) = mult(ld(ld(X2,unit),ld(ld(X1,X2),unit)),ld(ld(ld(X2,unit),ld(X1,unit)),unit)),
inference(step,[status(thm)],[t191585,t62]) ).
cnf(t191587,plain,
ld(ld(X1,unit),ld(X2,X1)) = mult(ld(ld(X2,ld(X1,X2)),unit),ld(ld(ld(X2,unit),ld(X1,unit)),unit)),
inference(step,[status(thm)],[t191586,t10146]) ).
cnf(t191588,plain,
ld(ld(X1,unit),ld(X2,X1)) = ld(mult(ld(X2,ld(X1,X2)),ld(ld(X2,unit),ld(X1,unit))),unit),
inference(step,[status(thm)],[t191587,t9675]) ).
cnf(t10261,plain,
ld(mult(ld(ld(X1,unit),X2),X3),unit) = mult(ld(X1,ld(X2,unit)),ld(X3,unit)),
inference(cp,[status(thm)],[t9675,t10229]) ).
cnf(t190825,plain,
ld(mult(X3,ld(ld(X1,unit),X2)),unit) = mult(ld(X1,ld(X2,unit)),ld(X3,unit)),
inference(step,[status(thm)],[t10261,t15]) ).
cnf(t190826,plain,
ld(mult(X3,ld(ld(X1,unit),X2)),unit) = mult(ld(X3,unit),ld(X1,ld(X2,unit))),
inference(step,[status(thm)],[t190825,t15]) ).
cnf(t13620,plain,
ld(mult(X1,ld(ld(X2,unit),X3)),unit) = mult(ld(X1,unit),ld(X2,ld(X3,unit))),
inference(orient,[status(thm)],[t190826]) ).
cnf(t191589,plain,
ld(ld(X1,unit),ld(X2,X1)) = mult(ld(ld(X2,ld(X1,X2)),unit),ld(X2,ld(ld(X1,unit),unit))),
inference(step,[status(thm)],[t191588,t13620]) ).
cnf(t191590,plain,
ld(ld(X1,unit),ld(X2,X1)) = mult(ld(X2,ld(ld(X1,unit),unit)),ld(ld(X2,ld(X1,X2)),unit)),
inference(step,[status(thm)],[t191589,t15]) ).
cnf(t191591,plain,
ld(ld(X1,unit),ld(X2,X1)) = mult(ld(X2,X1),ld(ld(X2,ld(X1,X2)),unit)),
inference(step,[status(thm)],[t191590,t62]) ).
cnf(t126988,plain,
mult(ld(X1,X2),ld(ld(X1,ld(X2,X1)),unit)) = ld(ld(X2,unit),ld(X1,X2)),
inference(orient,[status(thm)],[t191591]) ).
cnf(t127465,plain,
ld(ld(X1,ld(X2,X1)),unit) = ld(ld(X1,X2),ld(ld(X2,unit),ld(X1,X2))),
inference(cp,[status(thm)],[t12,t126988]) ).
cnf(t129951,plain,
ld(ld(X1,X2),ld(ld(X2,unit),ld(X1,X2))) = ld(ld(X1,ld(X2,X1)),unit),
inference(orient,[status(thm)],[t127465]) ).
cnf(t130558,plain,
ld(ld(X1,unit),ld(X2,X1)) = ld(mult(ld(ld(ld(X1,unit),ld(X2,X1)),ld(X2,X1)),ld(ld(ld(X1,unit),ld(X2,X1)),ld(X2,X1))),mult(ld(X2,X1),ld(ld(ld(X2,ld(X1,X2)),unit),unit))),
inference(cp,[status(thm)],[t28934,t129951]) ).
cnf(t191622,plain,
ld(ld(X1,unit),ld(X2,X1)) = ld(mult(ld(X1,unit),ld(ld(ld(X1,unit),ld(X2,X1)),ld(X2,X1))),mult(ld(X2,X1),ld(ld(ld(X2,ld(X1,X2)),unit),unit))),
inference(step,[status(thm)],[t130558,t62]) ).
cnf(t191623,plain,
ld(ld(X1,unit),ld(X2,X1)) = ld(mult(ld(X1,unit),ld(X1,unit)),mult(ld(X2,X1),ld(ld(ld(X2,ld(X1,X2)),unit),unit))),
inference(step,[status(thm)],[t191622,t62]) ).
cnf(t191624,plain,
ld(ld(X1,unit),ld(X2,X1)) = ld(ld(mult(X1,X1),unit),mult(ld(X2,X1),ld(ld(ld(X2,ld(X1,X2)),unit),unit))),
inference(step,[status(thm)],[t191623,t9675]) ).
cnf(t191625,plain,
ld(ld(X1,unit),ld(X2,X1)) = ld(ld(X1,ld(X1,unit)),mult(ld(X2,X1),ld(ld(ld(X2,ld(X1,X2)),unit),unit))),
inference(step,[status(thm)],[t191624,t843]) ).
cnf(t191626,plain,
ld(ld(X1,unit),ld(X2,X1)) = ld(ld(X1,ld(X1,unit)),mult(ld(X2,X1),ld(X2,ld(X1,X2)))),
inference(step,[status(thm)],[t191625,t62]) ).
cnf(t42,plain,
f(X1,ld(X1,X2)) = ld(mult(ld(X2,X1),ld(mult(X1,ld(X1,X2)),ld(X1,X2))),unit),
inference(cp,[status(thm)],[t40,t8]) ).
cnf(t190512,plain,
f(X1,ld(X1,X2)) = ld(mult(ld(X2,X1),ld(X2,ld(X1,X2))),unit),
inference(step,[status(thm)],[t42,t8]) ).
cnf(t106,plain,
ld(mult(ld(X1,X2),ld(X1,ld(X2,X1))),unit) = f(X2,ld(X2,X1)),
inference(orient,[status(thm)],[t190512]) ).
cnf(t117,plain,
mult(ld(X1,X2),ld(X1,ld(X2,X1))) = ld(f(X2,ld(X2,X1)),unit),
inference(cp,[status(thm)],[t62,t106]) ).
cnf(t127,plain,
mult(ld(X1,X2),ld(X1,ld(X2,X1))) = ld(f(X2,ld(X2,X1)),unit),
inference(orient,[status(thm)],[t117]) ).
cnf(t191627,plain,
ld(ld(X1,unit),ld(X2,X1)) = ld(ld(X1,ld(X1,unit)),ld(f(X1,ld(X1,X2)),unit)),
inference(step,[status(thm)],[t191626,t127]) ).
cnf(t10154,plain,
ld(ld(mult(X1,X1),X2),unit) = ld(ld(X1,ld(X1,unit)),ld(X2,unit)),
inference(cp,[status(thm)],[t10146,t843]) ).
cnf(t11675,plain,
ld(ld(X1,ld(X1,unit)),ld(X2,unit)) = ld(ld(mult(X1,X1),X2),unit),
inference(orient,[status(thm)],[t10154]) ).
cnf(t191628,plain,
ld(ld(X1,unit),ld(X2,X1)) = ld(ld(mult(X1,X1),f(X1,ld(X1,X2))),unit),
inference(step,[status(thm)],[t191627,t11675]) ).
cnf(t131829,plain,
ld(ld(mult(X1,X1),f(X1,ld(X1,X2))),unit) = ld(ld(X1,unit),ld(X2,X1)),
inference(orient,[status(thm)],[t191628]) ).
cnf(t10174,plain,
ld(f(ld(X1,unit),ld(ld(X1,unit),ld(X2,unit))),unit) = mult(ld(ld(X2,X1),unit),ld(ld(X2,unit),ld(ld(X1,unit),ld(X2,unit)))),
inference(cp,[status(thm)],[t127,t10146]) ).
cnf(t190830,plain,
ld(f(ld(X1,unit),ld(ld(X1,X2),unit)),unit) = mult(ld(ld(X2,X1),unit),ld(ld(X2,unit),ld(ld(X1,unit),ld(X2,unit)))),
inference(step,[status(thm)],[t10174,t10146]) ).
cnf(t190831,plain,
ld(f(ld(X1,unit),ld(ld(X1,X2),unit)),unit) = mult(ld(ld(X2,X1),unit),ld(ld(X2,unit),ld(ld(X1,X2),unit))),
inference(step,[status(thm)],[t190830,t10146]) ).
cnf(t190832,plain,
ld(f(ld(X1,unit),ld(ld(X1,X2),unit)),unit) = mult(ld(ld(X2,X1),unit),ld(ld(X2,ld(X1,X2)),unit)),
inference(step,[status(thm)],[t190831,t10146]) ).
cnf(t190833,plain,
ld(f(ld(X1,unit),ld(ld(X1,X2),unit)),unit) = ld(mult(ld(X2,X1),ld(X2,ld(X1,X2))),unit),
inference(step,[status(thm)],[t190832,t9675]) ).
cnf(t190834,plain,
ld(f(ld(X1,unit),ld(ld(X1,X2),unit)),unit) = f(X1,ld(X1,X2)),
inference(step,[status(thm)],[t190833,t106]) ).
cnf(t14395,plain,
ld(f(ld(X1,unit),ld(ld(X1,X2),unit)),unit) = f(X1,ld(X1,X2)),
inference(orient,[status(thm)],[t190834]) ).
cnf(t14434,plain,
f(X1,ld(X1,mult(X1,X2))) = ld(f(ld(X1,unit),ld(X2,unit)),unit),
inference(cp,[status(thm)],[t14395,t12]) ).
cnf(t190835,plain,
f(X1,X2) = ld(f(ld(X1,unit),ld(X2,unit)),unit),
inference(step,[status(thm)],[t14434,t12]) ).
cnf(t14630,plain,
ld(f(ld(X1,unit),ld(X2,unit)),unit) = f(X1,X2),
inference(orient,[status(thm)],[t190835]) ).
cnf(t14660,plain,
f(ld(X1,unit),X2) = ld(f(X1,ld(X2,unit)),unit),
inference(cp,[status(thm)],[t14630,t62]) ).
cnf(t133,plain,
ld(f(ld(X1,X2),ld(ld(X1,X2),X2)),unit) = mult(ld(X2,ld(X1,X2)),ld(X2,X1)),
inference(cp,[status(thm)],[t127,t62]) ).
cnf(t190516,plain,
ld(f(ld(X1,X2),X1),unit) = mult(ld(X2,ld(X1,X2)),ld(X2,X1)),
inference(step,[status(thm)],[t133,t62]) ).
cnf(t190517,plain,
ld(f(ld(X1,X2),X1),unit) = mult(ld(X2,X1),ld(X2,ld(X1,X2))),
inference(step,[status(thm)],[t190516,t15]) ).
cnf(t190518,plain,
ld(f(ld(X1,X2),X1),unit) = ld(f(X1,ld(X1,X2)),unit),
inference(step,[status(thm)],[t190517,t127]) ).
cnf(t143,plain,
ld(f(ld(X1,X2),X1),unit) = ld(f(X1,ld(X1,X2)),unit),
inference(orient,[status(thm)],[t190518]) ).
cnf(t150,plain,
f(ld(X1,X2),X1) = ld(ld(f(X1,ld(X1,X2)),unit),unit),
inference(cp,[status(thm)],[t62,t143]) ).
cnf(t190519,plain,
f(ld(X1,X2),X1) = f(X1,ld(X1,X2)),
inference(step,[status(thm)],[t150,t62]) ).
cnf(t153,plain,
f(ld(X1,X2),X1) = f(X1,ld(X1,X2)),
inference(orient,[status(thm)],[t190519]) ).
cnf(t154,plain,
f(X1,ld(X1,mult(X1,X2))) = f(X2,X1),
inference(cp,[status(thm)],[t153,t12]) ).
cnf(t190520,plain,
f(X1,X2) = f(X2,X1),
inference(step,[status(thm)],[t154,t12]) ).
cnf(t157,plain,
f(X1,X2) = f(X2,X1),
inference(orient,[status(thm)],[t190520]) ).
cnf(t190836,plain,
f(X2,ld(X1,unit)) = ld(f(X1,ld(X2,unit)),unit),
inference(step,[status(thm)],[t14660,t157]) ).
cnf(t14831,plain,
ld(f(X1,ld(X2,unit)),unit) = f(X2,ld(X1,unit)),
inference(orient,[status(thm)],[t190836]) ).
cnf(t14854,plain,
f(ld(X1,ld(X2,unit)),ld(X3,unit)) = ld(f(X3,ld(ld(X1,unit),X2)),unit),
inference(cp,[status(thm)],[t14831,t10382]) ).
cnf(t190844,plain,
f(ld(X3,unit),ld(X1,ld(X2,unit))) = ld(f(X3,ld(ld(X1,unit),X2)),unit),
inference(step,[status(thm)],[t14854,t157]) ).
cnf(t15622,plain,
f(ld(X1,unit),ld(X2,ld(X3,unit))) = ld(f(X1,ld(ld(X2,unit),X3)),unit),
inference(orient,[status(thm)],[t190844]) ).
cnf(t131855,plain,
ld(ld(ld(X1,unit),unit),ld(ld(X2,unit),ld(X1,unit))) = ld(ld(mult(ld(X1,unit),ld(X1,unit)),ld(f(X1,ld(ld(ld(X1,unit),unit),X2)),unit)),unit),
inference(cp,[status(thm)],[t131829,t15622]) ).
cnf(t191629,plain,
ld(X1,ld(ld(X2,unit),ld(X1,unit))) = ld(ld(mult(ld(X1,unit),ld(X1,unit)),ld(f(X1,ld(ld(ld(X1,unit),unit),X2)),unit)),unit),
inference(step,[status(thm)],[t131855,t62]) ).
cnf(t191630,plain,
ld(X1,ld(ld(X2,X1),unit)) = ld(ld(mult(ld(X1,unit),ld(X1,unit)),ld(f(X1,ld(ld(ld(X1,unit),unit),X2)),unit)),unit),
inference(step,[status(thm)],[t191629,t10146]) ).
cnf(t38049,plain,
ld(X1,mult(mult(X2,X1),mult(X2,X1))) = ld(ld(X2,unit),mult(X2,X1)),
inference(cp,[status(thm)],[t38017,t52]) ).
cnf(t191031,plain,
ld(X1,mult(mult(X1,X2),mult(X2,X1))) = ld(ld(X2,unit),mult(X2,X1)),
inference(step,[status(thm)],[t38049,t15]) ).
cnf(t191032,plain,
ld(X1,mult(mult(X1,X2),mult(X1,X2))) = ld(ld(X2,unit),mult(X2,X1)),
inference(step,[status(thm)],[t191031,t15]) ).
cnf(t38048,plain,
ld(X1,mult(mult(X1,X2),mult(X1,X2))) = ld(ld(X2,unit),mult(X1,X2)),
inference(cp,[status(thm)],[t38017,t12]) ).
cnf(t39522,plain,
ld(X1,mult(mult(X1,X2),mult(X1,X2))) = ld(ld(X2,unit),mult(X1,X2)),
inference(orient,[status(thm)],[t38048]) ).
cnf(t191033,plain,
ld(ld(X2,unit),mult(X1,X2)) = ld(ld(X2,unit),mult(X2,X1)),
inference(step,[status(thm)],[t191032,t39522]) ).
cnf(t3733,plain,
mult(ld(X1,X2),ld(X1,unit)) = ld(X1,mult(X2,ld(X1,unit))),
inference(cp,[status(thm)],[t12,t3674]) ).
cnf(t3821,plain,
ld(X1,mult(X2,ld(X1,unit))) = mult(ld(X1,X2),ld(X1,unit)),
inference(orient,[status(thm)],[t3733]) ).
cnf(t3834,plain,
mult(ld(ld(X1,unit),X2),ld(ld(X1,unit),unit)) = ld(ld(X1,unit),mult(X2,X1)),
inference(cp,[status(thm)],[t3821,t62]) ).
cnf(t190724,plain,
mult(ld(ld(X1,unit),X2),X1) = ld(ld(X1,unit),mult(X2,X1)),
inference(step,[status(thm)],[t3834,t62]) ).
cnf(t190725,plain,
mult(X1,ld(ld(X1,unit),X2)) = ld(ld(X1,unit),mult(X2,X1)),
inference(step,[status(thm)],[t190724,t15]) ).
cnf(t190726,plain,
mult(X1,ld(ld(X1,unit),X2)) = ld(ld(X1,unit),mult(X1,X2)),
inference(step,[status(thm)],[t190725,t15]) ).
cnf(t3859,plain,
ld(ld(X1,unit),mult(X1,X2)) = mult(X1,ld(ld(X1,unit),X2)),
inference(orient,[status(thm)],[t190726]) ).
cnf(t191034,plain,
ld(ld(X2,unit),mult(X1,X2)) = mult(X2,ld(ld(X2,unit),X1)),
inference(step,[status(thm)],[t191033,t3859]) ).
cnf(t39819,plain,
ld(ld(X1,unit),mult(X2,X1)) = mult(X1,ld(ld(X1,unit),X2)),
inference(orient,[status(thm)],[t191034]) ).
cnf(t10258,plain,
unit = mult(ld(ld(X1,unit),X2),ld(X1,ld(X2,unit))),
inference(cp,[status(thm)],[t8,t10229]) ).
cnf(t190813,plain,
unit = mult(ld(X1,ld(X2,unit)),ld(ld(X1,unit),X2)),
inference(step,[status(thm)],[t10258,t15]) ).
cnf(t10967,plain,
mult(ld(X1,ld(X2,unit)),ld(ld(X1,unit),X2)) = unit,
inference(orient,[status(thm)],[t190813]) ).
cnf(t10997,plain,
unit = mult(ld(X1,ld(mult(X1,X2),unit)),mult(X1,ld(ld(X1,unit),X2))),
inference(cp,[status(thm)],[t10967,t3859]) ).
cnf(t190977,plain,
unit = mult(mult(X1,ld(ld(X1,unit),X2)),ld(X1,ld(mult(X1,X2),unit))),
inference(step,[status(thm)],[t10997,t15]) ).
cnf(t32049,plain,
mult(mult(X1,ld(ld(X1,unit),X2)),ld(X1,ld(mult(X1,X2),unit))) = unit,
inference(orient,[status(thm)],[t190977]) ).
cnf(t9709,plain,
mult(ld(X1,unit),ld(ld(ld(X1,unit),unit),ld(X2,unit))) = ld(ld(ld(X1,unit),unit),ld(mult(X1,X2),unit)),
inference(cp,[status(thm)],[t3859,t9675]) ).
cnf(t190817,plain,
mult(ld(X1,unit),ld(ld(ld(X1,unit),X2),unit)) = ld(ld(ld(X1,unit),unit),ld(mult(X1,X2),unit)),
inference(step,[status(thm)],[t9709,t10146]) ).
cnf(t190818,plain,
mult(ld(X1,unit),ld(X1,ld(X2,unit))) = ld(ld(ld(X1,unit),unit),ld(mult(X1,X2),unit)),
inference(step,[status(thm)],[t190817,t10229]) ).
cnf(t190819,plain,
mult(ld(X1,unit),ld(X1,ld(X2,unit))) = ld(ld(ld(X1,unit),mult(X1,X2)),unit),
inference(step,[status(thm)],[t190818,t10146]) ).
cnf(t190820,plain,
mult(ld(X1,unit),ld(X1,ld(X2,unit))) = ld(X1,ld(mult(X1,X2),unit)),
inference(step,[status(thm)],[t190819,t10229]) ).
cnf(t11253,plain,
mult(ld(X1,unit),ld(X1,ld(X2,unit))) = ld(X1,ld(mult(X1,X2),unit)),
inference(orient,[status(thm)],[t190820]) ).
cnf(t11297,plain,
ld(X1,ld(mult(X1,ld(ld(X2,unit),X3)),unit)) = mult(ld(X1,unit),ld(X1,ld(X2,ld(X3,unit)))),
inference(cp,[status(thm)],[t11253,t10229]) ).
cnf(t191169,plain,
ld(X1,mult(ld(X1,unit),ld(X2,ld(X3,unit)))) = mult(ld(X1,unit),ld(X1,ld(X2,ld(X3,unit)))),
inference(step,[status(thm)],[t11297,t13620]) ).
cnf(t57683,plain,
ld(X1,mult(ld(X1,unit),ld(X2,ld(X3,unit)))) = mult(ld(X1,unit),ld(X1,ld(X2,ld(X3,unit)))),
inference(orient,[status(thm)],[t191169]) ).
cnf(t135,plain,
ld(X1,X2) = ld(ld(X1,ld(X2,X1)),ld(f(X2,ld(X2,X1)),unit)),
inference(cp,[status(thm)],[t52,t127]) ).
cnf(t255,plain,
ld(ld(X1,ld(X2,X1)),ld(f(X2,ld(X2,X1)),unit)) = ld(X1,X2),
inference(orient,[status(thm)],[t135]) ).
cnf(t57755,plain,
mult(ld(X1,unit),ld(X1,ld(ld(X2,ld(X3,X2)),ld(f(X3,ld(X3,X2)),unit)))) = ld(X1,mult(ld(X1,unit),ld(X2,X3))),
inference(cp,[status(thm)],[t57683,t255]) ).
cnf(t191170,plain,
mult(ld(X1,unit),ld(X1,ld(X2,X3))) = ld(X1,mult(ld(X1,unit),ld(X2,X3))),
inference(step,[status(thm)],[t57755,t255]) ).
cnf(t57972,plain,
ld(X1,mult(ld(X1,unit),ld(X2,X3))) = mult(ld(X1,unit),ld(X1,ld(X2,X3))),
inference(orient,[status(thm)],[t191170]) ).
cnf(t58120,plain,
mult(ld(X1,unit),ld(X2,X3)) = mult(X1,mult(ld(X1,unit),ld(X1,ld(X2,X3)))),
inference(cp,[status(thm)],[t8,t57972]) ).
cnf(t58286,plain,
mult(X1,mult(ld(X1,unit),ld(X1,ld(X2,X3)))) = mult(ld(X1,unit),ld(X2,X3)),
inference(orient,[status(thm)],[t58120]) ).
cnf(t6759,plain,
mult(X1,X2) = ld(ld(ld(mult(X1,X2),X1),unit),mult(X1,mult(X2,X2))),
inference(cp,[status(thm)],[t62,t6707]) ).
cnf(t7670,plain,
ld(ld(ld(mult(X1,X2),X1),unit),mult(X1,mult(X2,X2))) = mult(X1,X2),
inference(orient,[status(thm)],[t6759]) ).
cnf(t58435,plain,
mult(ld(X1,unit),ld(ld(ld(mult(X2,X3),X2),unit),mult(X2,mult(X3,X3)))) = mult(X1,mult(ld(X1,unit),ld(X1,mult(X2,X3)))),
inference(cp,[status(thm)],[t58286,t7670]) ).
cnf(t191171,plain,
mult(ld(X1,unit),mult(X2,X3)) = mult(X1,mult(ld(X1,unit),ld(X1,mult(X2,X3)))),
inference(step,[status(thm)],[t58435,t7670]) ).
cnf(t191172,plain,
mult(mult(X2,X3),ld(X1,unit)) = mult(X1,mult(ld(X1,unit),ld(X1,mult(X2,X3)))),
inference(step,[status(thm)],[t191171,t15]) ).
cnf(t58571,plain,
mult(X1,mult(ld(X1,unit),ld(X1,mult(X2,X3)))) = mult(mult(X2,X3),ld(X1,unit)),
inference(orient,[status(thm)],[t191172]) ).
cnf(t98,plain,
ld(mult(ld(mult(X1,X2),X1),ld(mult(X1,X2),X2)),unit) = mult(unit,f(X1,X2)),
inference(cp,[status(thm)],[t96,t40]) ).
cnf(t190511,plain,
f(X1,X2) = mult(unit,f(X1,X2)),
inference(step,[status(thm)],[t98,t40]) ).
cnf(t101,plain,
mult(unit,f(X1,X2)) = f(X1,X2),
inference(orient,[status(thm)],[t190511]) ).
cnf(t58726,plain,
mult(mult(unit,f(X1,X2)),ld(X3,unit)) = mult(X3,mult(ld(X3,unit),ld(X3,f(X1,X2)))),
inference(cp,[status(thm)],[t58571,t101]) ).
cnf(t191173,plain,
mult(ld(X3,unit),mult(unit,f(X1,X2))) = mult(X3,mult(ld(X3,unit),ld(X3,f(X1,X2)))),
inference(step,[status(thm)],[t58726,t15]) ).
cnf(t191174,plain,
mult(ld(X3,unit),f(X1,X2)) = mult(X3,mult(ld(X3,unit),ld(X3,f(X1,X2)))),
inference(step,[status(thm)],[t191173,t101]) ).
cnf(t58835,plain,
mult(X1,mult(ld(X1,unit),ld(X1,f(X2,X3)))) = mult(ld(X1,unit),f(X2,X3)),
inference(orient,[status(thm)],[t191174]) ).
cnf(t58959,plain,
unit = mult(mult(X1,ld(ld(X1,unit),mult(ld(X1,unit),ld(X1,f(X2,X3))))),ld(X1,ld(mult(ld(X1,unit),f(X2,X3)),unit))),
inference(cp,[status(thm)],[t32049,t58835]) ).
cnf(t191179,plain,
unit = mult(ld(X1,ld(mult(ld(X1,unit),f(X2,X3)),unit)),mult(X1,ld(ld(X1,unit),mult(ld(X1,unit),ld(X1,f(X2,X3)))))),
inference(step,[status(thm)],[t58959,t15]) ).
cnf(t191180,plain,
unit = mult(ld(X1,ld(mult(ld(X1,unit),f(X2,X3)),unit)),mult(X1,ld(X1,f(X2,X3)))),
inference(step,[status(thm)],[t191179,t12]) ).
cnf(t191181,plain,
unit = mult(ld(X1,ld(mult(ld(X1,unit),f(X2,X3)),unit)),f(X2,X3)),
inference(step,[status(thm)],[t191180,t8]) ).
cnf(t191182,plain,
unit = mult(f(X2,X3),ld(X1,ld(mult(ld(X1,unit),f(X2,X3)),unit))),
inference(step,[status(thm)],[t191181,t15]) ).
cnf(t59316,plain,
mult(f(X1,X2),ld(X3,ld(mult(ld(X3,unit),f(X1,X2)),unit))) = unit,
inference(orient,[status(thm)],[t191182]) ).
cnf(t59402,plain,
mult(ld(X1,ld(mult(ld(X1,unit),f(X2,X3)),unit)),ld(ld(ld(X1,ld(mult(ld(X1,unit),f(X2,X3)),unit)),unit),f(X2,X3))) = ld(ld(ld(X1,ld(mult(ld(X1,unit),f(X2,X3)),unit)),unit),unit),
inference(cp,[status(thm)],[t39819,t59316]) ).
cnf(t191183,plain,
mult(ld(X1,ld(mult(ld(X1,unit),f(X2,X3)),unit)),ld(ld(ld(X1,unit),mult(ld(X1,unit),f(X2,X3))),f(X2,X3))) = ld(ld(ld(X1,ld(mult(ld(X1,unit),f(X2,X3)),unit)),unit),unit),
inference(step,[status(thm)],[t59402,t10382]) ).
cnf(t191184,plain,
mult(ld(X1,ld(mult(ld(X1,unit),f(X2,X3)),unit)),ld(f(X2,X3),f(X2,X3))) = ld(ld(ld(X1,ld(mult(ld(X1,unit),f(X2,X3)),unit)),unit),unit),
inference(step,[status(thm)],[t191183,t12]) ).
cnf(t191185,plain,
mult(ld(X1,ld(mult(ld(X1,unit),f(X2,X3)),unit)),unit) = ld(ld(ld(X1,ld(mult(ld(X1,unit),f(X2,X3)),unit)),unit),unit),
inference(step,[status(thm)],[t191184,t51]) ).
cnf(t191186,plain,
ld(X1,ld(mult(ld(X1,unit),f(X2,X3)),unit)) = ld(ld(ld(X1,ld(mult(ld(X1,unit),f(X2,X3)),unit)),unit),unit),
inference(step,[status(thm)],[t191185,t9]) ).
cnf(t10273,plain,
ld(ld(ld(X1,unit),X2),ld(X3,unit)) = ld(ld(ld(X1,ld(X2,unit)),X3),unit),
inference(cp,[status(thm)],[t10229,t10229]) ).
cnf(t13828,plain,
ld(ld(ld(X1,ld(X2,unit)),X3),unit) = ld(ld(ld(X1,unit),X2),ld(X3,unit)),
inference(orient,[status(thm)],[t10273]) ).
cnf(t191187,plain,
ld(X1,ld(mult(ld(X1,unit),f(X2,X3)),unit)) = ld(ld(ld(X1,unit),mult(ld(X1,unit),f(X2,X3))),ld(unit,unit)),
inference(step,[status(thm)],[t191186,t13828]) ).
cnf(t191188,plain,
ld(X1,ld(mult(ld(X1,unit),f(X2,X3)),unit)) = ld(f(X2,X3),ld(unit,unit)),
inference(step,[status(thm)],[t191187,t12]) ).
cnf(t191189,plain,
ld(X1,ld(mult(ld(X1,unit),f(X2,X3)),unit)) = ld(f(X2,X3),unit),
inference(step,[status(thm)],[t191188,t59]) ).
cnf(t59504,plain,
ld(X1,ld(mult(ld(X1,unit),f(X2,X3)),unit)) = ld(f(X2,X3),unit),
inference(orient,[status(thm)],[t191189]) ).
cnf(t59563,plain,
ld(mult(ld(X1,unit),f(X2,X3)),unit) = mult(X1,ld(f(X2,X3),unit)),
inference(cp,[status(thm)],[t8,t59504]) ).
cnf(t59716,plain,
ld(mult(ld(X1,unit),f(X2,X3)),unit) = mult(X1,ld(f(X2,X3),unit)),
inference(orient,[status(thm)],[t59563]) ).
cnf(t63,plain,
mult(ld(mult(X1,X2),X1),ld(mult(X1,X2),X2)) = ld(f(X1,X2),unit),
inference(cp,[status(thm)],[t62,t40]) ).
cnf(t162,plain,
mult(ld(mult(X1,X2),X1),ld(mult(X1,X2),X2)) = ld(f(X1,X2),unit),
inference(orient,[status(thm)],[t63]) ).
cnf(t22,plain,
ld(mult(X1,unit),mult(X1,mult(unit,mult(X2,X3)))) = mult(ld(X1,mult(X1,mult(unit,X2))),ld(mult(X1,unit),mult(X1,mult(unit,X3)))),
inference(cp,[status(thm)],[t19,t9]) ).
cnf(t190489,plain,
ld(X1,mult(X1,mult(unit,mult(X2,X3)))) = mult(ld(X1,mult(X1,mult(unit,X2))),ld(mult(X1,unit),mult(X1,mult(unit,X3)))),
inference(step,[status(thm)],[t22,t9]) ).
cnf(t190490,plain,
mult(unit,mult(X2,X3)) = mult(ld(X1,mult(X1,mult(unit,X2))),ld(mult(X1,unit),mult(X1,mult(unit,X3)))),
inference(step,[status(thm)],[t190489,t12]) ).
cnf(t190491,plain,
mult(unit,mult(X2,X3)) = mult(mult(unit,X2),ld(mult(X1,unit),mult(X1,mult(unit,X3)))),
inference(step,[status(thm)],[t190490,t12]) ).
cnf(t190492,plain,
mult(unit,mult(X2,X3)) = mult(mult(X2,unit),ld(mult(X1,unit),mult(X1,mult(unit,X3)))),
inference(step,[status(thm)],[t190491,t15]) ).
cnf(t190493,plain,
mult(unit,mult(X2,X3)) = mult(X2,ld(mult(X1,unit),mult(X1,mult(unit,X3)))),
inference(step,[status(thm)],[t190492,t9]) ).
cnf(t190494,plain,
mult(unit,mult(X2,X3)) = mult(X2,ld(X1,mult(X1,mult(unit,X3)))),
inference(step,[status(thm)],[t190493,t9]) ).
cnf(t190495,plain,
mult(unit,mult(X2,X3)) = mult(X2,mult(unit,X3)),
inference(step,[status(thm)],[t190494,t12]) ).
cnf(t190496,plain,
mult(unit,mult(X2,X3)) = mult(X2,mult(X3,unit)),
inference(step,[status(thm)],[t190495,t15]) ).
cnf(t190497,plain,
mult(unit,mult(X2,X3)) = mult(X2,X3),
inference(step,[status(thm)],[t190496,t9]) ).
cnf(t65,plain,
mult(unit,mult(X1,X2)) = mult(X1,X2),
inference(orient,[status(thm)],[t190497]) ).
cnf(t165,plain,
ld(f(unit,mult(X1,X2)),unit) = mult(ld(mult(X1,X2),unit),ld(mult(unit,mult(X1,X2)),mult(X1,X2))),
inference(cp,[status(thm)],[t162,t65]) ).
cnf(t190529,plain,
ld(f(unit,mult(X1,X2)),unit) = mult(ld(mult(X1,X2),unit),ld(mult(X1,X2),mult(X1,X2))),
inference(step,[status(thm)],[t165,t65]) ).
cnf(t190530,plain,
ld(f(unit,mult(X1,X2)),unit) = mult(ld(mult(X1,X2),unit),unit),
inference(step,[status(thm)],[t190529,t51]) ).
cnf(t190531,plain,
ld(f(unit,mult(X1,X2)),unit) = ld(mult(X1,X2),unit),
inference(step,[status(thm)],[t190530,t9]) ).
cnf(t205,plain,
ld(f(unit,mult(X1,X2)),unit) = ld(mult(X1,X2),unit),
inference(orient,[status(thm)],[t190531]) ).
cnf(t212,plain,
f(unit,mult(X1,X2)) = ld(ld(mult(X1,X2),unit),unit),
inference(cp,[status(thm)],[t62,t205]) ).
cnf(t190532,plain,
f(unit,mult(X1,X2)) = mult(X1,X2),
inference(step,[status(thm)],[t212,t62]) ).
cnf(t214,plain,
f(unit,mult(X1,X2)) = mult(X1,X2),
inference(orient,[status(thm)],[t190532]) ).
cnf(t791,plain,
mult(X1,ld(mult(X1,X1),ld(X1,X2))) = ld(mult(X1,X1),X2),
inference(cp,[status(thm)],[t786,t8]) ).
cnf(t937,plain,
mult(X1,ld(mult(X1,X1),ld(X1,X2))) = ld(mult(X1,X1),X2),
inference(orient,[status(thm)],[t791]) ).
cnf(t962,plain,
mult(X1,ld(mult(X1,X1),ld(X1,X2))) = mult(unit,ld(mult(X1,X1),X2)),
inference(cp,[status(thm)],[t65,t937]) ).
cnf(t190577,plain,
ld(mult(X1,X1),X2) = mult(unit,ld(mult(X1,X1),X2)),
inference(step,[status(thm)],[t962,t937]) ).
cnf(t993,plain,
mult(unit,ld(mult(X1,X1),X2)) = ld(mult(X1,X1),X2),
inference(orient,[status(thm)],[t190577]) ).
cnf(t964,plain,
ld(mult(X1,X1),ld(X1,X2)) = ld(X1,ld(mult(X1,X1),X2)),
inference(cp,[status(thm)],[t12,t937]) ).
cnf(t1006,plain,
ld(mult(X1,X1),ld(X1,X2)) = ld(X1,ld(mult(X1,X1),X2)),
inference(orient,[status(thm)],[t964]) ).
cnf(t1032,plain,
ld(mult(X1,X1),ld(X1,X2)) = mult(unit,ld(X1,ld(mult(X1,X1),X2))),
inference(cp,[status(thm)],[t993,t1006]) ).
cnf(t190583,plain,
ld(X1,ld(mult(X1,X1),X2)) = mult(unit,ld(X1,ld(mult(X1,X1),X2))),
inference(step,[status(thm)],[t1032,t1006]) ).
cnf(t1112,plain,
mult(unit,ld(X1,ld(mult(X1,X1),X2))) = ld(X1,ld(mult(X1,X1),X2)),
inference(orient,[status(thm)],[t190583]) ).
cnf(t1116,plain,
ld(X1,ld(mult(X1,X1),mult(mult(X1,X1),X2))) = mult(unit,ld(X1,X2)),
inference(cp,[status(thm)],[t1112,t12]) ).
cnf(t190584,plain,
ld(X1,X2) = mult(unit,ld(X1,X2)),
inference(step,[status(thm)],[t1116,t12]) ).
cnf(t1136,plain,
mult(unit,ld(X1,X2)) = ld(X1,X2),
inference(orient,[status(thm)],[t190584]) ).
cnf(t1141,plain,
mult(unit,ld(X1,X2)) = f(unit,ld(X1,X2)),
inference(cp,[status(thm)],[t214,t1136]) ).
cnf(t190585,plain,
ld(X1,X2) = f(unit,ld(X1,X2)),
inference(step,[status(thm)],[t1141,t1136]) ).
cnf(t1150,plain,
f(unit,ld(X1,X2)) = ld(X1,X2),
inference(orient,[status(thm)],[t190585]) ).
cnf(t59778,plain,
mult(X1,ld(f(unit,ld(X2,X3)),unit)) = ld(mult(ld(X1,unit),ld(X2,X3)),unit),
inference(cp,[status(thm)],[t59716,t1150]) ).
cnf(t191190,plain,
mult(X1,ld(ld(X2,X3),unit)) = ld(mult(ld(X1,unit),ld(X2,X3)),unit),
inference(step,[status(thm)],[t59778,t1150]) ).
cnf(t60147,plain,
ld(mult(ld(X1,unit),ld(X2,X3)),unit) = mult(X1,ld(ld(X2,X3),unit)),
inference(orient,[status(thm)],[t191190]) ).
cnf(t60264,plain,
ld(ld(mult(ld(X1,unit),ld(X2,X3)),X4),unit) = ld(mult(X1,ld(ld(X2,X3),unit)),ld(X4,unit)),
inference(cp,[status(thm)],[t10146,t60147]) ).
cnf(t94344,plain,
ld(ld(mult(ld(X1,unit),ld(X2,X3)),X4),unit) = ld(mult(X1,ld(ld(X2,X3),unit)),ld(X4,unit)),
inference(orient,[status(thm)],[t60264]) ).
cnf(t191631,plain,
ld(X1,ld(ld(X2,X1),unit)) = ld(mult(X1,ld(ld(X1,unit),unit)),ld(ld(f(X1,ld(ld(ld(X1,unit),unit),X2)),unit),unit)),
inference(step,[status(thm)],[t191630,t94344]) ).
cnf(t191632,plain,
ld(X1,ld(ld(X2,X1),unit)) = ld(mult(X1,X1),ld(ld(f(X1,ld(ld(ld(X1,unit),unit),X2)),unit),unit)),
inference(step,[status(thm)],[t191631,t62]) ).
cnf(t191633,plain,
ld(X1,ld(ld(X2,X1),unit)) = ld(mult(X1,X1),f(X1,ld(ld(ld(X1,unit),unit),X2))),
inference(step,[status(thm)],[t191632,t62]) ).
cnf(t191634,plain,
ld(X1,ld(ld(X2,X1),unit)) = ld(mult(X1,X1),f(X1,ld(X1,X2))),
inference(step,[status(thm)],[t191633,t62]) ).
cnf(t132678,plain,
ld(mult(X1,X1),f(X1,ld(X1,X2))) = ld(X1,ld(ld(X2,X1),unit)),
inference(orient,[status(thm)],[t191634]) ).
cnf(t132934,plain,
f(X1,ld(X1,X2)) = mult(mult(X1,X1),ld(X1,ld(ld(X2,X1),unit))),
inference(cp,[status(thm)],[t8,t132678]) ).
cnf(t134414,plain,
mult(mult(X1,X1),ld(X1,ld(ld(X2,X1),unit))) = f(X1,ld(X1,X2)),
inference(orient,[status(thm)],[t132934]) ).
cnf(t134656,plain,
f(X1,ld(X1,ld(X2,X1))) = mult(mult(X1,X1),ld(X1,ld(X2,unit))),
inference(cp,[status(thm)],[t134414,t62]) ).
cnf(t134812,plain,
mult(mult(X1,X1),ld(X1,ld(X2,unit))) = f(X1,ld(X1,ld(X2,X1))),
inference(orient,[status(thm)],[t134656]) ).
cnf(t135042,plain,
mult(ld(mult(X1,X1),unit),ld(ld(X1,unit),X2)) = ld(f(X1,ld(X1,ld(X2,X1))),unit),
inference(cp,[status(thm)],[t14020,t134812]) ).
cnf(t191697,plain,
mult(ld(X1,ld(X1,unit)),ld(ld(X1,unit),X2)) = ld(f(X1,ld(X1,ld(X2,X1))),unit),
inference(step,[status(thm)],[t135042,t843]) ).
cnf(t148889,plain,
mult(ld(X1,ld(X1,unit)),ld(ld(X1,unit),X2)) = ld(f(X1,ld(X1,ld(X2,X1))),unit),
inference(orient,[status(thm)],[t191697]) ).
cnf(t127449,plain,
ld(ld(ld(X1,X2),unit),ld(X2,ld(X1,X2))) = mult(ld(X2,ld(X1,X2)),ld(ld(X2,X1),unit)),
inference(cp,[status(thm)],[t126988,t62]) ).
cnf(t191611,plain,
ld(ld(ld(X1,X2),unit),ld(X2,ld(X1,X2))) = ld(X1,ld(ld(X2,X1),unit)),
inference(step,[status(thm)],[t127449,t125415]) ).
cnf(t129280,plain,
ld(ld(ld(X1,X2),unit),ld(X2,ld(X1,X2))) = ld(X1,ld(ld(X2,X1),unit)),
inference(orient,[status(thm)],[t191611]) ).
cnf(t129480,plain,
ld(ld(X1,unit),ld(ld(ld(X2,unit),ld(X1,unit)),unit)) = ld(ld(ld(ld(X1,X2),unit),unit),ld(ld(X2,unit),ld(ld(X1,unit),ld(X2,unit)))),
inference(cp,[status(thm)],[t129280,t10146]) ).
cnf(t191612,plain,
ld(ld(X1,ld(ld(X2,unit),ld(X1,unit))),unit) = ld(ld(ld(ld(X1,X2),unit),unit),ld(ld(X2,unit),ld(ld(X1,unit),ld(X2,unit)))),
inference(step,[status(thm)],[t129480,t10146]) ).
cnf(t191613,plain,
ld(ld(X1,unit),ld(X2,ld(ld(X1,unit),unit))) = ld(ld(ld(ld(X1,X2),unit),unit),ld(ld(X2,unit),ld(ld(X1,unit),ld(X2,unit)))),
inference(step,[status(thm)],[t191612,t13437]) ).
cnf(t191614,plain,
ld(ld(X1,unit),ld(X2,X1)) = ld(ld(ld(ld(X1,X2),unit),unit),ld(ld(X2,unit),ld(ld(X1,unit),ld(X2,unit)))),
inference(step,[status(thm)],[t191613,t62]) ).
cnf(t191615,plain,
ld(ld(X1,unit),ld(X2,X1)) = ld(ld(X1,X2),ld(ld(X2,unit),ld(ld(X1,unit),ld(X2,unit)))),
inference(step,[status(thm)],[t191614,t62]) ).
cnf(t191616,plain,
ld(ld(X1,unit),ld(X2,X1)) = ld(ld(X1,X2),ld(ld(X2,unit),ld(ld(X1,X2),unit))),
inference(step,[status(thm)],[t191615,t10146]) ).
cnf(t191617,plain,
ld(ld(X1,unit),ld(X2,X1)) = ld(ld(X1,X2),ld(ld(X2,ld(X1,X2)),unit)),
inference(step,[status(thm)],[t191616,t10146]) ).
cnf(t130643,plain,
ld(ld(X1,X2),ld(ld(X2,ld(X1,X2)),unit)) = ld(ld(X1,unit),ld(X2,X1)),
inference(orient,[status(thm)],[t191617]) ).
cnf(t131096,plain,
ld(ld(X1,ld(X2,X1)),unit) = mult(ld(X2,X1),ld(ld(X2,unit),ld(X1,X2))),
inference(cp,[status(thm)],[t8,t130643]) ).
cnf(t138093,plain,
mult(ld(X1,X2),ld(ld(X1,unit),ld(X2,X1))) = ld(ld(X2,ld(X1,X2)),unit),
inference(orient,[status(thm)],[t131096]) ).
cnf(t138116,plain,
ld(ld(mult(X1,X2),ld(X1,mult(X1,X2))),unit) = mult(X2,ld(ld(X1,unit),ld(mult(X1,X2),X1))),
inference(cp,[status(thm)],[t138093,t12]) ).
cnf(t191674,plain,
ld(ld(mult(X1,X2),X2),unit) = mult(X2,ld(ld(X1,unit),ld(mult(X1,X2),X1))),
inference(step,[status(thm)],[t138116,t12]) ).
cnf(t141551,plain,
mult(X1,ld(ld(X2,unit),ld(mult(X2,X1),X2))) = ld(ld(mult(X2,X1),X1),unit),
inference(orient,[status(thm)],[t191674]) ).
cnf(t141765,plain,
ld(ld(mult(ld(X1,unit),ld(X2,unit)),ld(X2,unit)),unit) = mult(ld(X2,unit),ld(ld(ld(X1,unit),unit),ld(ld(mult(X1,X2),unit),ld(X1,unit)))),
inference(cp,[status(thm)],[t141551,t9675]) ).
cnf(t191675,plain,
ld(mult(X1,ld(ld(X2,unit),unit)),ld(ld(X2,unit),unit)) = mult(ld(X2,unit),ld(ld(ld(X1,unit),unit),ld(ld(mult(X1,X2),unit),ld(X1,unit)))),
inference(step,[status(thm)],[t141765,t94344]) ).
cnf(t191676,plain,
ld(mult(X1,X2),ld(ld(X2,unit),unit)) = mult(ld(X2,unit),ld(ld(ld(X1,unit),unit),ld(ld(mult(X1,X2),unit),ld(X1,unit)))),
inference(step,[status(thm)],[t191675,t62]) ).
cnf(t191677,plain,
ld(mult(X1,X2),X2) = mult(ld(X2,unit),ld(ld(ld(X1,unit),unit),ld(ld(mult(X1,X2),unit),ld(X1,unit)))),
inference(step,[status(thm)],[t191676,t62]) ).
cnf(t191678,plain,
ld(mult(X1,X2),X2) = mult(ld(X2,unit),ld(X1,ld(ld(mult(X1,X2),unit),ld(X1,unit)))),
inference(step,[status(thm)],[t191677,t62]) ).
cnf(t191679,plain,
ld(mult(X1,X2),X2) = mult(ld(X2,unit),ld(X1,ld(ld(mult(X1,X2),X1),unit))),
inference(step,[status(thm)],[t191678,t10146]) ).
cnf(t132718,plain,
ld(X1,ld(ld(mult(X1,X2),X1),unit)) = ld(mult(X1,X1),f(X1,X2)),
inference(cp,[status(thm)],[t132678,t12]) ).
cnf(t133115,plain,
ld(X1,ld(ld(mult(X1,X2),X1),unit)) = ld(mult(X1,X1),f(X1,X2)),
inference(orient,[status(thm)],[t132718]) ).
cnf(t191680,plain,
ld(mult(X1,X2),X2) = mult(ld(X2,unit),ld(mult(X1,X1),f(X1,X2))),
inference(step,[status(thm)],[t191679,t133115]) ).
cnf(t141969,plain,
mult(ld(X1,unit),ld(mult(X2,X2),f(X2,X1))) = ld(mult(X2,X1),X1),
inference(orient,[status(thm)],[t191680]) ).
cnf(t142117,plain,
ld(mult(X1,X1),f(X1,X2)) = ld(ld(X2,unit),ld(mult(X1,X2),X2)),
inference(cp,[status(thm)],[t12,t141969]) ).
cnf(t184693,plain,
ld(mult(X1,X1),f(X1,X2)) = ld(ld(X2,unit),ld(mult(X1,X2),X2)),
inference(orient,[status(thm)],[t142117]) ).
cnf(t185291,plain,
ld(f(X1,ld(X1,ld(ld(mult(X2,X1),X1),X1))),unit) = mult(ld(X1,ld(X1,unit)),ld(mult(X2,X2),f(X2,X1))),
inference(cp,[status(thm)],[t148889,t184693]) ).
cnf(t191918,plain,
ld(f(X1,ld(X1,mult(X2,X1))),unit) = mult(ld(X1,ld(X1,unit)),ld(mult(X2,X2),f(X2,X1))),
inference(step,[status(thm)],[t185291,t62]) ).
cnf(t191919,plain,
ld(f(X1,ld(X1,mult(X1,X2))),unit) = mult(ld(X1,ld(X1,unit)),ld(mult(X2,X2),f(X2,X1))),
inference(step,[status(thm)],[t191918,t15]) ).
cnf(t191920,plain,
ld(f(X1,X2),unit) = mult(ld(X1,ld(X1,unit)),ld(mult(X2,X2),f(X2,X1))),
inference(step,[status(thm)],[t191919,t12]) ).
cnf(t191921,plain,
ld(f(X1,X2),unit) = mult(ld(X1,ld(X1,unit)),ld(mult(X2,X2),f(X1,X2))),
inference(step,[status(thm)],[t191920,t157]) ).
cnf(t185569,plain,
mult(ld(X1,ld(X1,unit)),ld(mult(X2,X2),f(X1,X2))) = ld(f(X1,X2),unit),
inference(orient,[status(thm)],[t191921]) ).
cnf(t185762,plain,
ld(X1,ld(X1,unit)) = ld(ld(mult(X2,X2),f(X1,X2)),ld(f(X1,X2),unit)),
inference(cp,[status(thm)],[t52,t185569]) ).
cnf(t186443,plain,
ld(ld(mult(X1,X1),f(X2,X1)),ld(f(X2,X1),unit)) = ld(X2,ld(X2,unit)),
inference(orient,[status(thm)],[t185762]) ).
cnf(t186651,plain,
ld(ld(f(X1,X2),unit),ld(ld(f(X1,X2),unit),unit)) = mult(ld(ld(mult(X2,X2),f(X1,X2)),ld(ld(f(X1,X2),unit),unit)),ld(ld(X1,ld(X1,unit)),unit)),
inference(cp,[status(thm)],[t42365,t186443]) ).
cnf(t191935,plain,
ld(ld(f(X1,X2),ld(f(X1,X2),unit)),unit) = mult(ld(ld(mult(X2,X2),f(X1,X2)),ld(ld(f(X1,X2),unit),unit)),ld(ld(X1,ld(X1,unit)),unit)),
inference(step,[status(thm)],[t186651,t10146]) ).
cnf(t191936,plain,
ld(ld(f(X1,X2),unit),f(X1,X2)) = mult(ld(ld(mult(X2,X2),f(X1,X2)),ld(ld(f(X1,X2),unit),unit)),ld(ld(X1,ld(X1,unit)),unit)),
inference(step,[status(thm)],[t191935,t10382]) ).
cnf(t468,plain,
mult(X1,X1) = ld(ld(X1,unit),X1),
inference(cp,[status(thm)],[t62,t464]) ).
cnf(t485,plain,
ld(ld(X1,unit),X1) = mult(X1,X1),
inference(orient,[status(thm)],[t468]) ).
cnf(t191937,plain,
mult(f(X1,X2),f(X1,X2)) = mult(ld(ld(mult(X2,X2),f(X1,X2)),ld(ld(f(X1,X2),unit),unit)),ld(ld(X1,ld(X1,unit)),unit)),
inference(step,[status(thm)],[t191936,t485]) ).
cnf(t191938,plain,
mult(f(X1,X2),f(X1,X2)) = mult(ld(ld(X1,ld(X1,unit)),unit),ld(ld(mult(X2,X2),f(X1,X2)),ld(ld(f(X1,X2),unit),unit))),
inference(step,[status(thm)],[t191937,t15]) ).
cnf(t191939,plain,
mult(f(X1,X2),f(X1,X2)) = mult(ld(ld(X1,unit),X1),ld(ld(mult(X2,X2),f(X1,X2)),ld(ld(f(X1,X2),unit),unit))),
inference(step,[status(thm)],[t191938,t10382]) ).
cnf(t191940,plain,
mult(f(X1,X2),f(X1,X2)) = mult(mult(X1,X1),ld(ld(mult(X2,X2),f(X1,X2)),ld(ld(f(X1,X2),unit),unit))),
inference(step,[status(thm)],[t191939,t485]) ).
cnf(t191941,plain,
mult(f(X1,X2),f(X1,X2)) = mult(mult(X1,X1),ld(ld(mult(X2,X2),f(X1,X2)),f(X1,X2))),
inference(step,[status(thm)],[t191940,t62]) ).
cnf(t191942,plain,
mult(f(X1,X2),f(X1,X2)) = mult(mult(X1,X1),mult(X2,X2)),
inference(step,[status(thm)],[t191941,t62]) ).
cnf(t189733,plain,
mult(f(X1,X2),f(X1,X2)) = mult(mult(X1,X1),mult(X2,X2)),
inference(orient,[status(thm)],[t191942]) ).
cnf(goal_0,negated_conjecture,
mult(mult(a,a),mult(b,b)) != mult(f(a,b),f(a,b)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
mult(mult(a,a),mult(b,b)) != mult(mult(a,a),mult(b,b)),
inference(rw,[status(thm)],[goal_0,t189733]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP721-1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.37 % Computer : n026.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Wed Sep 23 15:53:24 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 93.99/13.03 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 93.99/13.03 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------