%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : GRP697-1 : TPTP v9.2.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n020.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue May 5 04:27:05 PM UTC 2026
% Result : Unsatisfiable 103.39s 67.63s
% Output : CNFRefutation 104.81s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named i_0_408)
% Comments :
%------------------------------------------------------------------------------
cnf(goals,negated_conjecture,
mult(mult(a,b),mult(b,mult(c,b))) != mult(mult(a,mult(b,mult(b,c))),b),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals) ).
cnf(c09,axiom,
mult(mult(X1,X2),X3) = mult(mult(X1,X3),ld(X3,mult(X2,X3))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c09) ).
cnf(c08,axiom,
mult(X1,mult(X2,X3)) = mult(rd(mult(X1,X2),X1),mult(X1,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c08) ).
cnf(c07,axiom,
mult(X1,i(mult(X2,X1))) = i(X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c07) ).
cnf(c04,axiom,
rd(mult(X1,X2),X2) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c04) ).
cnf(c03,axiom,
mult(rd(X1,X2),X2) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c03) ).
cnf(c01,axiom,
mult(X1,ld(X1,X2)) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c01) ).
cnf(c02,axiom,
ld(X1,mult(X1,X2)) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c02) ).
cnf(c10,axiom,
mult(i(X1),X1) = unit,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c10) ).
cnf(c11,axiom,
mult(X1,i(X1)) = unit,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c11) ).
cnf(c06,axiom,
mult(unit,X1) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c06) ).
cnf(c05,axiom,
mult(X1,unit) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c05) ).
cnf(i_0_12,negated_conjecture,
mult(mult(a,b),mult(b,mult(c,b))) != mult(mult(a,mult(b,mult(b,c))),b),
goals,
[final] ).
cnf(i_0_13,axiom,
mult(mult(X1,X2),X3) = mult(mult(X1,X3),ld(X3,mult(X2,X3))),
c09,
[final] ).
cnf(i_0_14,axiom,
mult(X1,mult(X2,X3)) = mult(rd(mult(X1,X2),X1),mult(X1,X3)),
c08,
[final] ).
cnf(i_0_15,axiom,
mult(X1,i(mult(X2,X1))) = i(X2),
c07,
[final] ).
cnf(i_0_16,axiom,
rd(mult(X1,X2),X2) = X1,
c04,
[final] ).
cnf(i_0_17,axiom,
mult(rd(X1,X2),X2) = X1,
c03,
[final] ).
cnf(i_0_18,axiom,
mult(X1,ld(X1,X2)) = X2,
c01,
[final] ).
cnf(i_0_19,axiom,
ld(X1,mult(X1,X2)) = X2,
c02,
[final] ).
cnf(i_0_20,axiom,
mult(i(X1),X1) = unit,
c10,
[final] ).
cnf(i_0_21,axiom,
mult(X1,i(X1)) = unit,
c11,
[final] ).
cnf(i_0_22,axiom,
mult(unit,X1) = X1,
c06,
[final] ).
cnf(i_0_23,axiom,
mult(X1,unit) = X1,
c05,
[final] ).
cnf(i_0_24,axiom,
X1 = X1 ).
cnf(i_0_25,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_26,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_27,axiom,
( X1 != X2
| mult(X1,X3) = mult(X2,X3) ) ).
cnf(i_0_28,axiom,
( X1 != X2
| mult(X3,X1) = mult(X3,X2) ) ).
cnf(i_0_29,axiom,
( X1 != X2
| ld(X1,X3) = ld(X2,X3) ) ).
cnf(i_0_30,axiom,
( X1 != X2
| ld(X3,X1) = ld(X3,X2) ) ).
cnf(i_0_31,axiom,
( X1 != X2
| rd(X1,X3) = rd(X2,X3) ) ).
cnf(i_0_32,axiom,
( X1 != X2
| rd(X3,X1) = rd(X3,X2) ) ).
cnf(i_0_33,axiom,
( X1 != X2
| i(X1) = i(X2) ) ).
cnf(i_0_412,plain,
rd(unit,unit) = rd(mult(mult(rd(unit,X1),X1),X2),X2),
inference(scs_inference,[],[i_0_401,i_0_161,i_0_409,i_0_25,i_0_26]) ).
cnf(i_0_426,plain,
mult(unit,rd(mult(unit,X1),X1)) = mult(unit,mult(unit,mult(rd(unit,mult(X2,X3)),mult(X2,X3)))),
inference(rename_variables,[],[i_0_408]) ).
cnf(i_0_429,plain,
mult(unit,rd(mult(unit,X1),X1)) = mult(unit,mult(unit,mult(rd(unit,mult(X2,X3)),mult(X2,X3)))),
inference(rename_variables,[],[i_0_408]) ).
cnf(i_0_414,plain,
rd(mult(mult(rd(unit,X1),X1),X2),X2) = rd(unit,unit),
inference(scs_inference,[],[i_0_412,i_0_25]) ).
cnf(i_0_415,plain,
mult(mult(i(X1),X1),unit) = rd(unit,unit),
inference(scs_inference,[],[i_0_13,i_0_411,i_0_412,i_0_25,i_0_26]) ).
cnf(i_0_416,plain,
mult(mult(i(X1),unit),ld(unit,mult(X1,unit))) = rd(unit,unit),
inference(rename_variables,[],[i_0_411]) ).
cnf(i_0_652,plain,
i(unit) = rd(unit,unit),
inference(scs_inference,[],[i_0_643,i_0_411,i_0_26]) ).
cnf(i_0_653,plain,
mult(mult(i(X1),unit),ld(unit,mult(X1,unit))) = rd(unit,unit),
inference(rename_variables,[],[i_0_411]) ).
cnf(i_0_654,plain,
rd(unit,unit) = i(unit),
inference(scs_inference,[],[i_0_643,i_0_411,i_0_26,i_0_25]) ).
cnf(i_0_418,plain,
rd(unit,unit) = mult(mult(i(X1),X1),unit),
inference(scs_inference,[],[i_0_415,i_0_25]) ).
cnf(i_0_419,plain,
mult(mult(X1,X2),X3) = mult(mult(mult(X1,X3),ld(X3,mult(X2,X3))),unit),
inference(scs_inference,[],[i_0_13,i_0_322,i_0_415,i_0_25,i_0_26]) ).
cnf(i_0_569,plain,
mult(X1,i(mult(unit,X1))) = rd(unit,unit),
inference(scs_inference,[],[i_0_414,i_0_564,i_0_26]) ).
cnf(i_0_570,plain,
rd(mult(mult(rd(unit,X1),X1),X2),X2) = rd(unit,unit),
inference(rename_variables,[],[i_0_414]) ).
cnf(i_0_571,plain,
rd(unit,unit) = mult(X1,i(mult(unit,X1))),
inference(scs_inference,[],[i_0_414,i_0_564,i_0_26,i_0_25]) ).
cnf(i_0_669,plain,
ld(X1,mult(X1,mult(rd(unit,X2),X2))) = i(unit),
inference(scs_inference,[],[i_0_398,i_0_654,i_0_26]) ).
cnf(i_0_670,plain,
i(unit) = ld(X1,mult(X1,mult(rd(unit,X2),X2))),
inference(scs_inference,[],[i_0_398,i_0_654,i_0_26,i_0_25]) ).
cnf(i_0_752,plain,
mult(i(unit),X1) = mult(rd(unit,unit),X1),
inference(scs_inference,[],[i_0_652,i_0_27]) ).
cnf(i_0_753,plain,
mult(X1,i(unit)) = mult(X1,rd(unit,unit)),
inference(scs_inference,[],[i_0_652,i_0_27,i_0_28]) ).
cnf(i_0_754,plain,
ld(i(unit),X1) = ld(rd(unit,unit),X1),
inference(scs_inference,[],[i_0_652,i_0_27,i_0_28,i_0_29]) ).
cnf(i_0_755,plain,
ld(X1,i(unit)) = ld(X1,rd(unit,unit)),
inference(scs_inference,[],[i_0_652,i_0_27,i_0_28,i_0_29,i_0_30]) ).
cnf(i_0_756,plain,
rd(i(unit),X1) = rd(rd(unit,unit),X1),
inference(scs_inference,[],[i_0_652,i_0_27,i_0_28,i_0_29,i_0_30,i_0_31]) ).
cnf(i_0_757,plain,
rd(X1,i(unit)) = rd(X1,rd(unit,unit)),
inference(scs_inference,[],[i_0_652,i_0_27,i_0_28,i_0_29,i_0_30,i_0_31,i_0_32]) ).
cnf(i_0_758,plain,
i(i(unit)) = i(rd(unit,unit)),
inference(scs_inference,[],[i_0_652,i_0_27,i_0_28,i_0_29,i_0_30,i_0_31,i_0_32,i_0_33]) ).
cnf(i_0_760,plain,
i(unit) = rd(i(unit),unit),
inference(scs_inference,[],[i_0_652,i_0_746,i_0_750,i_0_27,i_0_28,i_0_29,i_0_30,i_0_31,i_0_32,i_0_33,i_0_25,i_0_26]) ).
cnf(i_0_421,plain,
mult(mult(mult(X1,X2),ld(X2,mult(X3,X2))),unit) = mult(mult(X1,X3),X2),
inference(scs_inference,[],[i_0_419,i_0_25]) ).
cnf(i_0_422,plain,
mult(i(X1),X1) = mult(unit,mult(unit,rd(mult(unit,X2),X2))),
inference(scs_inference,[],[i_0_355,i_0_94,i_0_419,i_0_25,i_0_26]) ).
cnf(i_0_664,plain,
mult(rd(mult(X1,ld(X1,unit)),X2),X2) = mult(X3,i(mult(unit,X3))),
inference(scs_inference,[],[i_0_395,i_0_571,i_0_26]) ).
cnf(i_0_665,plain,
mult(X1,i(mult(unit,X1))) = mult(rd(mult(X2,ld(X2,unit)),X3),X3),
inference(scs_inference,[],[i_0_395,i_0_571,i_0_26,i_0_25]) ).
cnf(i_0_671,plain,
mult(X1,i(mult(unit,X1))) = ld(X2,mult(X2,mult(rd(unit,X3),X3))),
inference(scs_inference,[],[i_0_15,i_0_670,i_0_26]) ).
cnf(i_0_673,plain,
ld(X1,mult(X1,mult(rd(unit,X2),X2))) = mult(X3,i(mult(unit,X3))),
inference(scs_inference,[],[i_0_15,i_0_670,i_0_26,i_0_25]) ).
cnf(i_0_677,plain,
i(unit) = rd(mult(unit,X1),X1),
inference(scs_inference,[],[i_0_250,i_0_670,i_0_26]) ).
cnf(i_0_679,plain,
rd(mult(unit,X1),X1) = i(unit),
inference(scs_inference,[],[i_0_250,i_0_670,i_0_26,i_0_25]) ).
cnf(i_0_879,plain,
mult(i(unit),X1) = mult(rd(unit,unit),X1),
inference(rename_variables,[],[i_0_752]) ).
cnf(i_0_899,plain,
mult(X1,i(unit)) = mult(X1,rd(unit,unit)),
inference(rename_variables,[],[i_0_753]) ).
cnf(i_0_920,plain,
ld(i(unit),X1) = ld(rd(unit,unit),X1),
inference(rename_variables,[],[i_0_754]) ).
cnf(i_0_921,plain,
mult(ld(X1,i(unit)),X2) = mult(ld(X1,rd(unit,unit)),X2),
inference(scs_inference,[],[i_0_755,i_0_27]) ).
cnf(i_0_922,plain,
mult(X1,ld(X2,i(unit))) = mult(X1,ld(X2,rd(unit,unit))),
inference(scs_inference,[],[i_0_755,i_0_27,i_0_28]) ).
cnf(i_0_923,plain,
ld(ld(X1,i(unit)),X2) = ld(ld(X1,rd(unit,unit)),X2),
inference(scs_inference,[],[i_0_755,i_0_27,i_0_28,i_0_29]) ).
cnf(i_0_924,plain,
ld(X1,ld(X2,i(unit))) = ld(X1,ld(X2,rd(unit,unit))),
inference(scs_inference,[],[i_0_755,i_0_27,i_0_28,i_0_29,i_0_30]) ).
cnf(i_0_925,plain,
rd(ld(X1,i(unit)),X2) = rd(ld(X1,rd(unit,unit)),X2),
inference(scs_inference,[],[i_0_755,i_0_27,i_0_28,i_0_29,i_0_30,i_0_31]) ).
cnf(i_0_926,plain,
rd(X1,ld(X2,i(unit))) = rd(X1,ld(X2,rd(unit,unit))),
inference(scs_inference,[],[i_0_755,i_0_27,i_0_28,i_0_29,i_0_30,i_0_31,i_0_32]) ).
cnf(i_0_927,plain,
i(ld(X1,i(unit))) = i(ld(X1,rd(unit,unit))),
inference(scs_inference,[],[i_0_755,i_0_27,i_0_28,i_0_29,i_0_30,i_0_31,i_0_32,i_0_33]) ).
cnf(i_0_931,plain,
mult(rd(i(unit),X1),X2) = mult(rd(rd(unit,unit),X1),X2),
inference(scs_inference,[],[i_0_756,i_0_27]) ).
cnf(i_0_932,plain,
mult(X1,rd(i(unit),X2)) = mult(X1,rd(rd(unit,unit),X2)),
inference(scs_inference,[],[i_0_756,i_0_27,i_0_28]) ).
cnf(i_0_933,plain,
ld(rd(i(unit),X1),X2) = ld(rd(rd(unit,unit),X1),X2),
inference(scs_inference,[],[i_0_756,i_0_27,i_0_28,i_0_29]) ).
cnf(i_0_934,plain,
ld(X1,rd(i(unit),X2)) = ld(X1,rd(rd(unit,unit),X2)),
inference(scs_inference,[],[i_0_756,i_0_27,i_0_28,i_0_29,i_0_30]) ).
cnf(i_0_935,plain,
rd(rd(i(unit),X1),X2) = rd(rd(rd(unit,unit),X1),X2),
inference(scs_inference,[],[i_0_756,i_0_27,i_0_28,i_0_29,i_0_30,i_0_31]) ).
cnf(i_0_936,plain,
rd(X1,rd(i(unit),X2)) = rd(X1,rd(rd(unit,unit),X2)),
inference(scs_inference,[],[i_0_756,i_0_27,i_0_28,i_0_29,i_0_30,i_0_31,i_0_32]) ).
cnf(i_0_937,plain,
i(rd(i(unit),X1)) = i(rd(rd(unit,unit),X1)),
inference(scs_inference,[],[i_0_756,i_0_27,i_0_28,i_0_29,i_0_30,i_0_31,i_0_32,i_0_33]) ).
cnf(i_0_940,plain,
rd(i(unit),X1) = rd(rd(unit,unit),X1),
inference(rename_variables,[],[i_0_756]) ).
cnf(i_0_941,plain,
rd(X1,i(unit)) = rd(X1,rd(unit,unit)),
inference(rename_variables,[],[i_0_757]) ).
cnf(i_0_961,plain,
mult(mult(X1,i(mult(unit,X1))),X2) = mult(rd(unit,unit),X2),
inference(scs_inference,[],[i_0_569,i_0_27]) ).
cnf(i_0_962,plain,
mult(X1,mult(X2,i(mult(unit,X2)))) = mult(X1,rd(unit,unit)),
inference(scs_inference,[],[i_0_569,i_0_27,i_0_28]) ).
cnf(i_0_963,plain,
ld(mult(X1,i(mult(unit,X1))),X2) = ld(rd(unit,unit),X2),
inference(scs_inference,[],[i_0_569,i_0_27,i_0_28,i_0_29]) ).
cnf(i_0_964,plain,
ld(X1,mult(X2,i(mult(unit,X2)))) = ld(X1,rd(unit,unit)),
inference(scs_inference,[],[i_0_569,i_0_27,i_0_28,i_0_29,i_0_30]) ).
cnf(i_0_965,plain,
rd(mult(X1,i(mult(unit,X1))),X2) = rd(rd(unit,unit),X2),
inference(scs_inference,[],[i_0_569,i_0_27,i_0_28,i_0_29,i_0_30,i_0_31]) ).
cnf(i_0_966,plain,
rd(X1,mult(X2,i(mult(unit,X2)))) = rd(X1,rd(unit,unit)),
inference(scs_inference,[],[i_0_569,i_0_27,i_0_28,i_0_29,i_0_30,i_0_31,i_0_32]) ).
cnf(i_0_967,plain,
i(mult(X1,i(mult(unit,X1)))) = i(rd(unit,unit)),
inference(scs_inference,[],[i_0_569,i_0_27,i_0_28,i_0_29,i_0_30,i_0_31,i_0_32,i_0_33]) ).
cnf(i_0_1590,plain,
mult(mult(mult(a,b),ld(b,mult(mult(b,mult(b,c)),b))),unit) != mult(mult(a,b),mult(b,mult(c,b))),
inference(scs_inference,[],[i_0_419,i_0_749,i_0_26]) ).
cnf(i_0_1591,plain,
mult(mult(X1,X2),X3) = mult(mult(mult(X1,X3),ld(X3,mult(X2,X3))),unit),
inference(rename_variables,[],[i_0_419]) ).
cnf(i_0_1592,plain,
mult(ld(X1,rd(X2,unit)),X3) = mult(ld(X1,rd(X2,i(unit))),X3),
inference(scs_inference,[],[i_0_834,i_0_419,i_0_749,i_0_26,i_0_27]) ).
cnf(i_0_1593,plain,
mult(X1,ld(X2,rd(X3,unit))) = mult(X1,ld(X2,rd(X3,i(unit)))),
inference(scs_inference,[],[i_0_834,i_0_419,i_0_749,i_0_26,i_0_27,i_0_28]) ).
cnf(i_0_424,plain,
mult(unit,mult(unit,rd(mult(unit,X1),X1))) = mult(i(X2),X2),
inference(scs_inference,[],[i_0_422,i_0_25]) ).
cnf(i_0_425,plain,
rd(unit,unit) = mult(unit,mult(unit,mult(rd(unit,mult(X1,X2)),mult(X1,X2)))),
inference(scs_inference,[],[i_0_408,i_0_392,i_0_422,i_0_25,i_0_26]) ).
cnf(i_0_436,plain,
mult(mult(mult(X1,X2),ld(X2,mult(X3,X2))),unit) = mult(mult(X1,X3),X2),
inference(rename_variables,[],[i_0_421]) ).
cnf(i_0_487,plain,
mult(mult(mult(X1,X2),ld(X2,mult(X3,X2))),unit) = mult(mult(X1,X3),X2),
inference(rename_variables,[],[i_0_421]) ).
cnf(i_0_674,plain,
mult(unit,rd(mult(unit,X1),X1)) = mult(X2,i(mult(unit,X2))),
inference(scs_inference,[],[i_0_673,i_0_244,i_0_26]) ).
cnf(i_0_675,plain,
ld(X1,mult(X1,mult(rd(unit,X2),X2))) = mult(X3,i(mult(unit,X3))),
inference(rename_variables,[],[i_0_673]) ).
cnf(i_0_676,plain,
mult(X1,i(mult(unit,X1))) = mult(unit,rd(mult(unit,X2),X2)),
inference(scs_inference,[],[i_0_673,i_0_244,i_0_26,i_0_25]) ).
cnf(i_0_728,plain,
rd(mult(i(unit),X1),X1) = mult(rd(mult(X2,ld(X2,unit)),X3),X3),
inference(scs_inference,[],[i_0_727,i_0_665,i_0_26]) ).
cnf(i_0_729,plain,
mult(X1,i(mult(unit,X1))) = mult(rd(mult(X2,ld(X2,unit)),X3),X3),
inference(rename_variables,[],[i_0_665]) ).
cnf(i_0_731,plain,
mult(rd(mult(X1,ld(X1,unit)),X2),X2) = rd(mult(i(unit),X3),X3),
inference(scs_inference,[],[i_0_727,i_0_665,i_0_26,i_0_25]) ).
cnf(i_0_771,plain,
mult(rd(mult(unit,X1),X1),X2) = mult(i(unit),X2),
inference(scs_inference,[],[i_0_679,i_0_27]) ).
cnf(i_0_772,plain,
mult(X1,rd(mult(unit,X2),X2)) = mult(X1,i(unit)),
inference(scs_inference,[],[i_0_679,i_0_27,i_0_28]) ).
cnf(i_0_773,plain,
ld(rd(mult(unit,X1),X1),X2) = ld(i(unit),X2),
inference(scs_inference,[],[i_0_679,i_0_27,i_0_28,i_0_29]) ).
cnf(i_0_774,plain,
ld(X1,rd(mult(unit,X2),X2)) = ld(X1,i(unit)),
inference(scs_inference,[],[i_0_679,i_0_27,i_0_28,i_0_29,i_0_30]) ).
cnf(i_0_775,plain,
rd(rd(mult(unit,X1),X1),X2) = rd(i(unit),X2),
inference(scs_inference,[],[i_0_679,i_0_27,i_0_28,i_0_29,i_0_30,i_0_31]) ).
cnf(i_0_776,plain,
rd(X1,rd(mult(unit,X2),X2)) = rd(X1,i(unit)),
inference(scs_inference,[],[i_0_679,i_0_27,i_0_28,i_0_29,i_0_30,i_0_31,i_0_32]) ).
cnf(i_0_777,plain,
i(rd(mult(unit,X1),X1)) = i(i(unit)),
inference(scs_inference,[],[i_0_679,i_0_27,i_0_28,i_0_29,i_0_30,i_0_31,i_0_32,i_0_33]) ).
cnf(i_0_779,plain,
rd(mult(unit,X1),X1) = rd(i(unit),unit),
inference(scs_inference,[],[i_0_679,i_0_760,i_0_769,i_0_27,i_0_28,i_0_29,i_0_30,i_0_31,i_0_32,i_0_33,i_0_25,i_0_26]) ).
cnf(i_0_852,plain,
mult(i(unit),X1) = mult(rd(mult(unit,X2),X2),X1),
inference(scs_inference,[],[i_0_677,i_0_27]) ).
cnf(i_0_853,plain,
mult(X1,i(unit)) = mult(X1,rd(mult(unit,X2),X2)),
inference(scs_inference,[],[i_0_677,i_0_27,i_0_28]) ).
cnf(i_0_854,plain,
ld(i(unit),X1) = ld(rd(mult(unit,X2),X2),X1),
inference(scs_inference,[],[i_0_677,i_0_27,i_0_28,i_0_29]) ).
cnf(i_0_855,plain,
ld(X1,i(unit)) = ld(X1,rd(mult(unit,X2),X2)),
inference(scs_inference,[],[i_0_677,i_0_27,i_0_28,i_0_29,i_0_30]) ).
cnf(i_0_856,plain,
rd(i(unit),X1) = rd(rd(mult(unit,X2),X2),X1),
inference(scs_inference,[],[i_0_677,i_0_27,i_0_28,i_0_29,i_0_30,i_0_31]) ).
cnf(i_0_857,plain,
rd(X1,i(unit)) = rd(X1,rd(mult(unit,X2),X2)),
inference(scs_inference,[],[i_0_677,i_0_27,i_0_28,i_0_29,i_0_30,i_0_31,i_0_32]) ).
cnf(i_0_858,plain,
i(i(unit)) = i(rd(mult(unit,X1),X1)),
inference(scs_inference,[],[i_0_677,i_0_27,i_0_28,i_0_29,i_0_30,i_0_31,i_0_32,i_0_33]) ).
cnf(i_0_1594,plain,
mult(mult(a,b),mult(b,mult(c,b))) != mult(mult(mult(a,b),ld(b,mult(mult(b,mult(b,c)),b))),unit),
inference(scs_inference,[],[i_0_1590,i_0_25]) ).
cnf(i_0_1595,plain,
rd(rd(X1,unit),rd(X2,unit)) = rd(rd(X1,i(unit)),rd(X2,i(unit))),
inference(scs_inference,[],[i_0_835,i_0_836,i_0_1590,i_0_25,i_0_26]) ).
cnf(i_0_427,plain,
mult(unit,mult(unit,mult(rd(unit,mult(X1,X2)),mult(X1,X2)))) = rd(unit,unit),
inference(scs_inference,[],[i_0_425,i_0_25]) ).
cnf(i_0_428,plain,
mult(X1,i(X1)) = mult(unit,mult(unit,mult(rd(unit,mult(X2,X3)),mult(X2,X3)))),
inference(scs_inference,[],[i_0_408,i_0_193,i_0_425,i_0_25,i_0_26]) ).
cnf(i_0_680,plain,
mult(X1,i(mult(unit,X1))) = rd(mult(mult(i(X2),X2),X3),X3),
inference(scs_inference,[],[i_0_676,i_0_309,i_0_26]) ).
cnf(i_0_682,plain,
rd(mult(mult(i(X1),X1),X2),X2) = mult(X3,i(mult(unit,X3))),
inference(scs_inference,[],[i_0_676,i_0_309,i_0_26,i_0_25]) ).
cnf(i_0_686,plain,
mult(X1,i(mult(unit,X1))) = mult(X2,ld(X2,unit)),
inference(scs_inference,[],[i_0_676,i_0_268,i_0_26]) ).
cnf(i_0_688,plain,
mult(X1,ld(X1,unit)) = mult(X2,i(mult(unit,X2))),
inference(scs_inference,[],[i_0_676,i_0_268,i_0_26,i_0_25]) ).
cnf(i_0_952,plain,
mult(rd(mult(unit,X1),X1),X2) = mult(rd(i(unit),unit),X2),
inference(scs_inference,[],[i_0_779,i_0_27]) ).
cnf(i_0_953,plain,
mult(X1,rd(mult(unit,X2),X2)) = mult(X1,rd(i(unit),unit)),
inference(scs_inference,[],[i_0_779,i_0_27,i_0_28]) ).
cnf(i_0_954,plain,
ld(rd(mult(unit,X1),X1),X2) = ld(rd(i(unit),unit),X2),
inference(scs_inference,[],[i_0_779,i_0_27,i_0_28,i_0_29]) ).
cnf(i_0_955,plain,
ld(X1,rd(mult(unit,X2),X2)) = ld(X1,rd(i(unit),unit)),
inference(scs_inference,[],[i_0_779,i_0_27,i_0_28,i_0_29,i_0_30]) ).
cnf(i_0_956,plain,
rd(rd(mult(unit,X1),X1),X2) = rd(rd(i(unit),unit),X2),
inference(scs_inference,[],[i_0_779,i_0_27,i_0_28,i_0_29,i_0_30,i_0_31]) ).
cnf(i_0_957,plain,
rd(X1,rd(mult(unit,X2),X2)) = rd(X1,rd(i(unit),unit)),
inference(scs_inference,[],[i_0_779,i_0_27,i_0_28,i_0_29,i_0_30,i_0_31,i_0_32]) ).
cnf(i_0_958,plain,
i(rd(mult(unit,X1),X1)) = i(rd(i(unit),unit)),
inference(scs_inference,[],[i_0_779,i_0_27,i_0_28,i_0_29,i_0_30,i_0_31,i_0_32,i_0_33]) ).
cnf(i_0_959,plain,
rd(mult(unit,X1),X1) = rd(mult(i(X2),X2),unit),
inference(scs_inference,[],[i_0_779,i_0_846,i_0_27,i_0_28,i_0_29,i_0_30,i_0_31,i_0_32,i_0_33,i_0_26]) ).
cnf(i_0_1000,plain,
mult(X1,rd(mult(unit,X2),X2)) = mult(X1,i(unit)),
inference(rename_variables,[],[i_0_772]) ).
cnf(i_0_1102,plain,
mult(mult(rd(mult(unit,X1),X1),X2),X3) = mult(mult(i(unit),X2),X3),
inference(scs_inference,[],[i_0_771,i_0_27]) ).
cnf(i_0_1103,plain,
mult(X1,mult(rd(mult(unit,X2),X2),X3)) = mult(X1,mult(i(unit),X3)),
inference(scs_inference,[],[i_0_771,i_0_27,i_0_28]) ).
cnf(i_0_1104,plain,
ld(mult(rd(mult(unit,X1),X1),X2),X3) = ld(mult(i(unit),X2),X3),
inference(scs_inference,[],[i_0_771,i_0_27,i_0_28,i_0_29]) ).
cnf(i_0_1105,plain,
ld(X1,mult(rd(mult(unit,X2),X2),X3)) = ld(X1,mult(i(unit),X3)),
inference(scs_inference,[],[i_0_771,i_0_27,i_0_28,i_0_29,i_0_30]) ).
cnf(i_0_1106,plain,
rd(mult(rd(mult(unit,X1),X1),X2),X3) = rd(mult(i(unit),X2),X3),
inference(scs_inference,[],[i_0_771,i_0_27,i_0_28,i_0_29,i_0_30,i_0_31]) ).
cnf(i_0_1107,plain,
rd(X1,mult(rd(mult(unit,X2),X2),X3)) = rd(X1,mult(i(unit),X3)),
inference(scs_inference,[],[i_0_771,i_0_27,i_0_28,i_0_29,i_0_30,i_0_31,i_0_32]) ).
cnf(i_0_1108,plain,
i(mult(rd(mult(unit,X1),X1),X2)) = i(mult(i(unit),X2)),
inference(scs_inference,[],[i_0_771,i_0_27,i_0_28,i_0_29,i_0_30,i_0_31,i_0_32,i_0_33]) ).
cnf(i_0_1112,plain,
mult(ld(rd(mult(unit,X1),X1),X2),X3) = mult(ld(i(unit),X2),X3),
inference(scs_inference,[],[i_0_773,i_0_27]) ).
cnf(i_0_1113,plain,
mult(X1,ld(rd(mult(unit,X2),X2),X3)) = mult(X1,ld(i(unit),X3)),
inference(scs_inference,[],[i_0_773,i_0_27,i_0_28]) ).
cnf(i_0_1114,plain,
ld(ld(rd(mult(unit,X1),X1),X2),X3) = ld(ld(i(unit),X2),X3),
inference(scs_inference,[],[i_0_773,i_0_27,i_0_28,i_0_29]) ).
cnf(i_0_1115,plain,
ld(X1,ld(rd(mult(unit,X2),X2),X3)) = ld(X1,ld(i(unit),X3)),
inference(scs_inference,[],[i_0_773,i_0_27,i_0_28,i_0_29,i_0_30]) ).
cnf(i_0_1116,plain,
rd(ld(rd(mult(unit,X1),X1),X2),X3) = rd(ld(i(unit),X2),X3),
inference(scs_inference,[],[i_0_773,i_0_27,i_0_28,i_0_29,i_0_30,i_0_31]) ).
cnf(i_0_1117,plain,
rd(X1,ld(rd(mult(unit,X2),X2),X3)) = rd(X1,ld(i(unit),X3)),
inference(scs_inference,[],[i_0_773,i_0_27,i_0_28,i_0_29,i_0_30,i_0_31,i_0_32]) ).
cnf(i_0_1118,plain,
i(ld(rd(mult(unit,X1),X1),X2)) = i(ld(i(unit),X2)),
inference(scs_inference,[],[i_0_773,i_0_27,i_0_28,i_0_29,i_0_30,i_0_31,i_0_32,i_0_33]) ).
cnf(i_0_1120,plain,
ld(rd(mult(unit,X1),X1),X2) = ld(i(unit),X2),
inference(rename_variables,[],[i_0_773]) ).
cnf(i_0_1122,plain,
mult(ld(X1,rd(mult(unit,X2),X2)),X3) = mult(ld(X1,i(unit)),X3),
inference(scs_inference,[],[i_0_774,i_0_27]) ).
cnf(i_0_1123,plain,
mult(X1,ld(X2,rd(mult(unit,X3),X3))) = mult(X1,ld(X2,i(unit))),
inference(scs_inference,[],[i_0_774,i_0_27,i_0_28]) ).
cnf(i_0_1124,plain,
ld(ld(X1,rd(mult(unit,X2),X2)),X3) = ld(ld(X1,i(unit)),X3),
inference(scs_inference,[],[i_0_774,i_0_27,i_0_28,i_0_29]) ).
cnf(i_0_1125,plain,
ld(X1,ld(X2,rd(mult(unit,X3),X3))) = ld(X1,ld(X2,i(unit))),
inference(scs_inference,[],[i_0_774,i_0_27,i_0_28,i_0_29,i_0_30]) ).
cnf(i_0_1126,plain,
rd(ld(X1,rd(mult(unit,X2),X2)),X3) = rd(ld(X1,i(unit)),X3),
inference(scs_inference,[],[i_0_774,i_0_27,i_0_28,i_0_29,i_0_30,i_0_31]) ).
cnf(i_0_1127,plain,
rd(X1,ld(X2,rd(mult(unit,X3),X3))) = rd(X1,ld(X2,i(unit))),
inference(scs_inference,[],[i_0_774,i_0_27,i_0_28,i_0_29,i_0_30,i_0_31,i_0_32]) ).
cnf(i_0_1128,plain,
i(ld(X1,rd(mult(unit,X2),X2))) = i(ld(X1,i(unit))),
inference(scs_inference,[],[i_0_774,i_0_27,i_0_28,i_0_29,i_0_30,i_0_31,i_0_32,i_0_33]) ).
cnf(i_0_1130,plain,
mult(i(unit),X1) = mult(rd(mult(unit,X2),X2),X1),
inference(rename_variables,[],[i_0_852]) ).
cnf(i_0_1132,plain,
mult(rd(rd(mult(unit,X1),X1),X2),X3) = mult(rd(i(unit),X2),X3),
inference(scs_inference,[],[i_0_775,i_0_27]) ).
cnf(i_0_1133,plain,
mult(X1,rd(rd(mult(unit,X2),X2),X3)) = mult(X1,rd(i(unit),X3)),
inference(scs_inference,[],[i_0_775,i_0_27,i_0_28]) ).
cnf(i_0_1134,plain,
ld(rd(rd(mult(unit,X1),X1),X2),X3) = ld(rd(i(unit),X2),X3),
inference(scs_inference,[],[i_0_775,i_0_27,i_0_28,i_0_29]) ).
cnf(i_0_1135,plain,
ld(X1,rd(rd(mult(unit,X2),X2),X3)) = ld(X1,rd(i(unit),X3)),
inference(scs_inference,[],[i_0_775,i_0_27,i_0_28,i_0_29,i_0_30]) ).
cnf(i_0_1136,plain,
rd(rd(rd(mult(unit,X1),X1),X2),X3) = rd(rd(i(unit),X2),X3),
inference(scs_inference,[],[i_0_775,i_0_27,i_0_28,i_0_29,i_0_30,i_0_31]) ).
cnf(i_0_1137,plain,
rd(X1,rd(rd(mult(unit,X2),X2),X3)) = rd(X1,rd(i(unit),X3)),
inference(scs_inference,[],[i_0_775,i_0_27,i_0_28,i_0_29,i_0_30,i_0_31,i_0_32]) ).
cnf(i_0_1138,plain,
i(rd(rd(mult(unit,X1),X1),X2)) = i(rd(i(unit),X2)),
inference(scs_inference,[],[i_0_775,i_0_27,i_0_28,i_0_29,i_0_30,i_0_31,i_0_32,i_0_33]) ).
cnf(i_0_1139,plain,
rd(rd(mult(unit,X1),X1),rd(mult(unit,X2),X2)) = rd(i(unit),i(unit)),
inference(scs_inference,[],[i_0_775,i_0_776,i_0_27,i_0_28,i_0_29,i_0_30,i_0_31,i_0_32,i_0_33,i_0_26]) ).
cnf(i_0_1140,plain,
rd(rd(mult(unit,X1),X1),X2) = rd(i(unit),X2),
inference(rename_variables,[],[i_0_775]) ).
cnf(i_0_1141,plain,
rd(X1,rd(mult(unit,X2),X2)) = rd(X1,i(unit)),
inference(rename_variables,[],[i_0_776]) ).
cnf(i_0_1260,plain,
i(rd(mult(unit,X1),X1)) = i(mult(i(X2),X2)),
inference(scs_inference,[],[i_0_732,i_0_777,i_0_848,i_0_27,i_0_28,i_0_29,i_0_30,i_0_31,i_0_32,i_0_33,i_0_26]) ).
cnf(i_0_1439,plain,
mult(a,mult(b,mult(b,c))) != rd(mult(rd(mult(mult(a,b),b),mult(a,b)),mult(mult(a,b),mult(c,b))),b),
inference(scs_inference,[],[i_0_778,i_0_27]) ).
cnf(i_0_1441,plain,
ld(b,mult(mult(b,mult(b,c)),b)) != mult(b,mult(c,b)),
inference(scs_inference,[],[i_0_1210,i_0_778,i_0_27,i_0_28]) ).
cnf(i_0_1442,plain,
rd(mult(rd(mult(mult(a,b),b),mult(a,b)),mult(mult(a,b),mult(c,b))),b) != mult(a,mult(b,mult(b,c))),
inference(scs_inference,[],[i_0_1210,i_0_778,i_0_27,i_0_28,i_0_25]) ).
cnf(i_0_1580,plain,
mult(X1,i(unit)) = mult(X1,rd(mult(unit,X2),X2)),
inference(rename_variables,[],[i_0_853]) ).
cnf(i_0_430,plain,
mult(unit,mult(unit,mult(rd(unit,mult(X1,X2)),mult(X1,X2)))) = mult(X3,i(X3)),
inference(scs_inference,[],[i_0_428,i_0_25]) ).
cnf(i_0_431,plain,
rd(mult(unit,X1),X1) = rd(unit,unit),
inference(scs_inference,[],[i_0_373,i_0_427,i_0_428,i_0_25,i_0_26]) ).
cnf(i_0_432,plain,
mult(unit,mult(unit,mult(rd(unit,mult(X1,X2)),mult(X1,X2)))) = rd(unit,unit),
inference(rename_variables,[],[i_0_427]) ).
cnf(i_0_683,plain,
rd(mult(mult(i(X1),X1),X2),X2) = i(unit),
inference(scs_inference,[],[i_0_15,i_0_682,i_0_26]) ).
cnf(i_0_685,plain,
i(unit) = rd(mult(mult(i(X1),X1),X2),X2),
inference(scs_inference,[],[i_0_15,i_0_682,i_0_26,i_0_25]) ).
cnf(i_0_689,plain,
mult(X1,ld(X1,unit)) = i(unit),
inference(scs_inference,[],[i_0_15,i_0_688,i_0_26]) ).
cnf(i_0_691,plain,
i(unit) = mult(X1,ld(X1,unit)),
inference(scs_inference,[],[i_0_15,i_0_688,i_0_26,i_0_25]) ).
cnf(i_0_704,plain,
mult(X1,i(X1)) = mult(X2,i(mult(unit,X2))),
inference(scs_inference,[],[i_0_688,i_0_205,i_0_26]) ).
cnf(i_0_705,plain,
mult(X1,ld(X1,unit)) = mult(X2,i(mult(unit,X2))),
inference(rename_variables,[],[i_0_688]) ).
cnf(i_0_706,plain,
mult(X1,i(mult(unit,X1))) = mult(X2,i(X2)),
inference(scs_inference,[],[i_0_688,i_0_205,i_0_26,i_0_25]) ).
cnf(i_0_1051,plain,
mult(mult(X1,i(mult(unit,X1))),X2) = mult(mult(X3,ld(X3,unit)),X2),
inference(scs_inference,[],[i_0_686,i_0_27]) ).
cnf(i_0_1052,plain,
mult(X1,mult(X2,i(mult(unit,X2)))) = mult(X1,mult(X3,ld(X3,unit))),
inference(scs_inference,[],[i_0_686,i_0_27,i_0_28]) ).
cnf(i_0_1053,plain,
ld(mult(X1,i(mult(unit,X1))),X2) = ld(mult(X3,ld(X3,unit)),X2),
inference(scs_inference,[],[i_0_686,i_0_27,i_0_28,i_0_29]) ).
cnf(i_0_1054,plain,
ld(X1,mult(X2,i(mult(unit,X2)))) = ld(X1,mult(X3,ld(X3,unit))),
inference(scs_inference,[],[i_0_686,i_0_27,i_0_28,i_0_29,i_0_30]) ).
cnf(i_0_1055,plain,
rd(mult(X1,i(mult(unit,X1))),X2) = rd(mult(X3,ld(X3,unit)),X2),
inference(scs_inference,[],[i_0_686,i_0_27,i_0_28,i_0_29,i_0_30,i_0_31]) ).
cnf(i_0_1056,plain,
rd(X1,mult(X2,i(mult(unit,X2)))) = rd(X1,mult(X3,ld(X3,unit))),
inference(scs_inference,[],[i_0_686,i_0_27,i_0_28,i_0_29,i_0_30,i_0_31,i_0_32]) ).
cnf(i_0_1057,plain,
i(mult(X1,i(mult(unit,X1)))) = i(mult(X2,ld(X2,unit))),
inference(scs_inference,[],[i_0_686,i_0_27,i_0_28,i_0_29,i_0_30,i_0_31,i_0_32,i_0_33]) ).
cnf(i_0_1058,plain,
mult(X1,i(mult(unit,X1))) = mult(i(unit),ld(mult(i(X2),X2),unit)),
inference(scs_inference,[],[i_0_686,i_0_762,i_0_27,i_0_28,i_0_29,i_0_30,i_0_31,i_0_32,i_0_33,i_0_26]) ).
cnf(i_0_1059,plain,
mult(X1,i(mult(unit,X1))) = mult(X2,ld(X2,unit)),
inference(rename_variables,[],[i_0_686]) ).
cnf(i_0_1452,plain,
mult(b,mult(c,b)) != ld(b,mult(mult(b,mult(b,c)),b)),
inference(scs_inference,[],[i_0_814,i_0_1441,i_0_27,i_0_28,i_0_25]) ).
cnf(i_0_1453,plain,
mult(X1,i(mult(ld(unit,X2),X1))) = i(ld(i(unit),X2)),
inference(scs_inference,[],[i_0_15,i_0_814,i_0_816,i_0_1441,i_0_27,i_0_28,i_0_25,i_0_26]) ).
cnf(i_0_1465,plain,
ld(mult(ld(X1,unit),X2),X3) = ld(mult(ld(X1,i(unit)),X2),X3),
inference(scs_inference,[],[i_0_821,i_0_1313,i_0_1442,i_0_26,i_0_29]) ).
cnf(i_0_1466,plain,
ld(X1,mult(ld(X2,unit),X3)) = ld(X1,mult(ld(X2,i(unit)),X3)),
inference(scs_inference,[],[i_0_821,i_0_1313,i_0_1442,i_0_26,i_0_29,i_0_30]) ).
cnf(i_0_1467,plain,
rd(mult(ld(X1,unit),X2),X3) = rd(mult(ld(X1,i(unit)),X2),X3),
inference(scs_inference,[],[i_0_821,i_0_1313,i_0_1442,i_0_26,i_0_29,i_0_30,i_0_31]) ).
cnf(i_0_1468,plain,
rd(X1,mult(ld(X2,unit),X3)) = rd(X1,mult(ld(X2,i(unit)),X3)),
inference(scs_inference,[],[i_0_821,i_0_1313,i_0_1442,i_0_26,i_0_29,i_0_30,i_0_31,i_0_32]) ).
cnf(i_0_1469,plain,
i(mult(ld(X1,unit),X2)) = i(mult(ld(X1,i(unit)),X2)),
inference(scs_inference,[],[i_0_821,i_0_1313,i_0_1442,i_0_26,i_0_29,i_0_30,i_0_31,i_0_32,i_0_33]) ).
cnf(i_0_1473,plain,
ld(b,mult(mult(b,b),ld(b,mult(mult(b,c),b)))) != mult(b,mult(c,b)),
inference(scs_inference,[],[i_0_1206,i_0_1441,i_0_26]) ).
cnf(i_0_1475,plain,
mult(mult(X1,ld(X2,unit)),X3) = mult(mult(X1,ld(X2,i(unit))),X3),
inference(scs_inference,[],[i_0_822,i_0_1206,i_0_1441,i_0_26,i_0_27]) ).
cnf(i_0_1476,plain,
mult(X1,mult(X2,ld(X3,unit))) = mult(X1,mult(X2,ld(X3,i(unit)))),
inference(scs_inference,[],[i_0_822,i_0_1206,i_0_1441,i_0_26,i_0_27,i_0_28]) ).
cnf(i_0_1477,plain,
mult(b,mult(c,b)) != ld(b,mult(mult(b,b),ld(b,mult(mult(b,c),b)))),
inference(scs_inference,[],[i_0_822,i_0_1206,i_0_1441,i_0_26,i_0_27,i_0_28,i_0_25]) ).
cnf(i_0_1502,plain,
ld(rd(mult(X1,X2),X2),X3) = ld(X1,X3),
inference(scs_inference,[],[i_0_16,i_0_1439,i_0_1310,i_0_26,i_0_29]) ).
cnf(i_0_1503,plain,
ld(X1,rd(mult(X2,X3),X3)) = ld(X1,X2),
inference(scs_inference,[],[i_0_16,i_0_1439,i_0_1310,i_0_26,i_0_29,i_0_30]) ).
cnf(i_0_1504,plain,
rd(rd(mult(X1,X2),X2),X3) = rd(X1,X3),
inference(scs_inference,[],[i_0_16,i_0_1439,i_0_1310,i_0_26,i_0_29,i_0_30,i_0_31]) ).
cnf(i_0_1505,plain,
rd(X1,rd(mult(X2,X3),X3)) = rd(X1,X2),
inference(scs_inference,[],[i_0_16,i_0_1439,i_0_1310,i_0_26,i_0_29,i_0_30,i_0_31,i_0_32]) ).
cnf(i_0_1506,plain,
i(rd(mult(X1,X2),X2)) = i(X1),
inference(scs_inference,[],[i_0_16,i_0_1439,i_0_1310,i_0_26,i_0_29,i_0_30,i_0_31,i_0_32,i_0_33]) ).
cnf(i_0_433,plain,
rd(unit,unit) = rd(mult(unit,X1),X1),
inference(scs_inference,[],[i_0_431,i_0_25]) ).
cnf(i_0_434,plain,
mult(mult(mult(i(X1),unit),ld(unit,mult(X1,unit))),unit) = mult(X2,i(X2)),
inference(scs_inference,[],[i_0_421,i_0_190,i_0_431,i_0_25,i_0_26]) ).
cnf(i_0_692,plain,
i(unit) = mult(unit,mult(unit,mult(rd(unit,mult(X1,X2)),mult(X1,X2)))),
inference(scs_inference,[],[i_0_691,i_0_346,i_0_26]) ).
cnf(i_0_694,plain,
mult(unit,mult(unit,mult(rd(unit,mult(X1,X2)),mult(X1,X2)))) = i(unit),
inference(scs_inference,[],[i_0_691,i_0_346,i_0_26,i_0_25]) ).
cnf(i_0_695,plain,
i(unit) = ld(X1,mult(X1,mult(X2,ld(X2,unit)))),
inference(scs_inference,[],[i_0_691,i_0_177,i_0_26]) ).
cnf(i_0_697,plain,
ld(X1,mult(X1,mult(X2,ld(X2,unit)))) = i(unit),
inference(scs_inference,[],[i_0_691,i_0_177,i_0_26,i_0_25]) ).
cnf(i_0_722,plain,
i(unit) = mult(mult(i(X1),X1),unit),
inference(scs_inference,[],[i_0_685,i_0_297,i_0_26]) ).
cnf(i_0_724,plain,
mult(mult(i(X1),X1),unit) = i(unit),
inference(scs_inference,[],[i_0_685,i_0_297,i_0_26,i_0_25]) ).
cnf(i_0_780,plain,
mult(mult(X1,ld(X1,unit)),X2) = mult(i(unit),X2),
inference(scs_inference,[],[i_0_689,i_0_27]) ).
cnf(i_0_781,plain,
mult(X1,mult(X2,ld(X2,unit))) = mult(X1,i(unit)),
inference(scs_inference,[],[i_0_689,i_0_27,i_0_28]) ).
cnf(i_0_782,plain,
ld(mult(X1,ld(X1,unit)),X2) = ld(i(unit),X2),
inference(scs_inference,[],[i_0_689,i_0_27,i_0_28,i_0_29]) ).
cnf(i_0_783,plain,
ld(X1,mult(X2,ld(X2,unit))) = ld(X1,i(unit)),
inference(scs_inference,[],[i_0_689,i_0_27,i_0_28,i_0_29,i_0_30]) ).
cnf(i_0_784,plain,
rd(mult(X1,ld(X1,unit)),X2) = rd(i(unit),X2),
inference(scs_inference,[],[i_0_689,i_0_27,i_0_28,i_0_29,i_0_30,i_0_31]) ).
cnf(i_0_785,plain,
rd(X1,mult(X2,ld(X2,unit))) = rd(X1,i(unit)),
inference(scs_inference,[],[i_0_689,i_0_27,i_0_28,i_0_29,i_0_30,i_0_31,i_0_32]) ).
cnf(i_0_786,plain,
i(mult(X1,ld(X1,unit))) = i(i(unit)),
inference(scs_inference,[],[i_0_689,i_0_27,i_0_28,i_0_29,i_0_30,i_0_31,i_0_32,i_0_33]) ).
cnf(i_0_1339,plain,
mult(mult(X1,i(X1)),X2) = mult(mult(X3,i(mult(unit,X3))),X2),
inference(scs_inference,[],[i_0_704,i_0_27]) ).
cnf(i_0_1340,plain,
mult(X1,mult(X2,i(X2))) = mult(X1,mult(X3,i(mult(unit,X3)))),
inference(scs_inference,[],[i_0_704,i_0_27,i_0_28]) ).
cnf(i_0_1341,plain,
ld(mult(X1,i(X1)),X2) = ld(mult(X3,i(mult(unit,X3))),X2),
inference(scs_inference,[],[i_0_704,i_0_27,i_0_28,i_0_29]) ).
cnf(i_0_1342,plain,
ld(X1,mult(X2,i(X2))) = ld(X1,mult(X3,i(mult(unit,X3)))),
inference(scs_inference,[],[i_0_704,i_0_27,i_0_28,i_0_29,i_0_30]) ).
cnf(i_0_1343,plain,
rd(mult(X1,i(X1)),X2) = rd(mult(X3,i(mult(unit,X3))),X2),
inference(scs_inference,[],[i_0_704,i_0_27,i_0_28,i_0_29,i_0_30,i_0_31]) ).
cnf(i_0_1344,plain,
rd(X1,mult(X2,i(X2))) = rd(X1,mult(X3,i(mult(unit,X3)))),
inference(scs_inference,[],[i_0_704,i_0_27,i_0_28,i_0_29,i_0_30,i_0_31,i_0_32]) ).
cnf(i_0_1345,plain,
i(mult(X1,i(X1))) = i(mult(X2,i(mult(unit,X2)))),
inference(scs_inference,[],[i_0_704,i_0_27,i_0_28,i_0_29,i_0_30,i_0_31,i_0_32,i_0_33]) ).
cnf(i_0_1480,plain,
mult(rd(mult(X1,ld(X1,mult(b,mult(c,b)))),X2),X2) != ld(b,mult(mult(b,mult(b,c)),b)),
inference(scs_inference,[],[i_0_107,i_0_1452,i_0_26]) ).
cnf(i_0_1482,plain,
ld(ld(ld(X1,unit),X2),X3) = ld(ld(ld(X1,i(unit)),X2),X3),
inference(scs_inference,[],[i_0_823,i_0_107,i_0_1452,i_0_26,i_0_29]) ).
cnf(i_0_1483,plain,
ld(X1,ld(ld(X2,unit),X3)) = ld(X1,ld(ld(X2,i(unit)),X3)),
inference(scs_inference,[],[i_0_823,i_0_107,i_0_1452,i_0_26,i_0_29,i_0_30]) ).
cnf(i_0_1484,plain,
rd(ld(ld(X1,unit),X2),X3) = rd(ld(ld(X1,i(unit)),X2),X3),
inference(scs_inference,[],[i_0_823,i_0_107,i_0_1452,i_0_26,i_0_29,i_0_30,i_0_31]) ).
cnf(i_0_1485,plain,
rd(X1,ld(ld(X2,unit),X3)) = rd(X1,ld(ld(X2,i(unit)),X3)),
inference(scs_inference,[],[i_0_823,i_0_107,i_0_1452,i_0_26,i_0_29,i_0_30,i_0_31,i_0_32]) ).
cnf(i_0_1486,plain,
i(ld(ld(X1,unit),X2)) = i(ld(ld(X1,i(unit)),X2)),
inference(scs_inference,[],[i_0_823,i_0_107,i_0_1452,i_0_26,i_0_29,i_0_30,i_0_31,i_0_32,i_0_33]) ).
cnf(i_0_1487,plain,
ld(b,mult(mult(b,mult(b,c)),b)) != mult(rd(mult(X1,ld(X1,mult(b,mult(c,b)))),X2),X2),
inference(scs_inference,[],[i_0_823,i_0_107,i_0_1452,i_0_26,i_0_29,i_0_30,i_0_31,i_0_32,i_0_33,i_0_25]) ).
cnf(i_0_1509,plain,
ld(rd(mult(X1,X2),X2),X3) = ld(X1,X3),
inference(rename_variables,[],[i_0_1502]) ).
cnf(i_0_1512,plain,
mult(rd(mult(rd(mult(b,c),b),mult(b,b)),X1),X1) != ld(b,mult(mult(b,b),ld(b,mult(mult(b,c),b)))),
inference(scs_inference,[],[i_0_1477,i_0_529,i_0_26]) ).
cnf(i_0_1517,plain,
ld(X1,rd(mult(ld(X2,unit),X3),X3)) = ld(X1,ld(X2,i(unit))),
inference(scs_inference,[],[i_0_1503,i_0_824,i_0_26]) ).
cnf(i_0_1518,plain,
ld(X1,rd(mult(X2,X3),X3)) = ld(X1,X2),
inference(rename_variables,[],[i_0_1503]) ).
cnf(i_0_1521,plain,
ld(rd(rd(mult(X1,X2),X2),X3),X4) = ld(rd(X1,X3),X4),
inference(scs_inference,[],[i_0_1504,i_0_1507,i_0_1313,i_0_26,i_0_29]) ).
cnf(i_0_1522,plain,
ld(X1,rd(rd(mult(X2,X3),X3),X4)) = ld(X1,rd(X2,X4)),
inference(scs_inference,[],[i_0_1504,i_0_1507,i_0_1313,i_0_26,i_0_29,i_0_30]) ).
cnf(i_0_1523,plain,
rd(rd(rd(mult(X1,X2),X2),X3),X4) = rd(rd(X1,X3),X4),
inference(scs_inference,[],[i_0_1504,i_0_1507,i_0_1313,i_0_26,i_0_29,i_0_30,i_0_31]) ).
cnf(i_0_1524,plain,
rd(X1,rd(rd(mult(X2,X3),X3),X4)) = rd(X1,rd(X2,X4)),
inference(scs_inference,[],[i_0_1504,i_0_1507,i_0_1313,i_0_26,i_0_29,i_0_30,i_0_31,i_0_32]) ).
cnf(c_0_1469,axiom,
rd(mult(X1,X2),X2) = X1,
i_0_16 ).
cnf(c_0_1470,axiom,
mult(i(X1),X1) = unit,
i_0_20 ).
cnf(c_0_1471,axiom,
mult(X1,i(mult(X2,X1))) = i(X2),
i_0_15 ).
cnf(c_0_1472,plain,
i(X1) = rd(unit,X1),
inference(spm,[status(thm)],[c_0_1469,c_0_1470]) ).
cnf(c_0_1473,axiom,
mult(X1,i(X1)) = unit,
i_0_21 ).
cnf(c_0_1474,plain,
mult(X1,rd(unit,mult(X2,X1))) = rd(unit,X2),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_1471,c_0_1472]),c_0_1472]) ).
cnf(c_0_1475,axiom,
mult(X1,ld(X1,X2)) = X2,
i_0_18 ).
cnf(c_0_1476,axiom,
ld(X1,mult(X1,X2)) = X2,
i_0_19 ).
cnf(c_0_1477,plain,
mult(X1,rd(unit,X1)) = unit,
inference(rw,[status(thm)],[c_0_1473,c_0_1472]) ).
cnf(c_0_1478,axiom,
mult(X1,mult(X2,X3)) = mult(rd(mult(X1,X2),X1),mult(X1,X3)),
i_0_14 ).
cnf(c_0_1479,axiom,
mult(X1,unit) = X1,
i_0_23 ).
cnf(c_0_1480,plain,
mult(ld(X1,X2),rd(unit,X2)) = rd(unit,X1),
inference(spm,[status(thm)],[c_0_1474,c_0_1475]) ).
cnf(c_0_1481,plain,
rd(X1,ld(X2,X1)) = X2,
inference(spm,[status(thm)],[c_0_1469,c_0_1475]) ).
cnf(c_0_1482,plain,
ld(X1,unit) = rd(unit,X1),
inference(spm,[status(thm)],[c_0_1476,c_0_1477]) ).
cnf(c_0_1483,plain,
ld(X1,rd(unit,X2)) = rd(unit,mult(X2,X1)),
inference(spm,[status(thm)],[c_0_1476,c_0_1474]) ).
cnf(c_0_1484,plain,
mult(X1,mult(X2,rd(unit,X1))) = rd(mult(X1,X2),X1),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1478,c_0_1477]),c_0_1479]) ).
cnf(c_0_1485,plain,
mult(rd(unit,mult(X1,X2)),X1) = rd(unit,X2),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1480,c_0_1481]),c_0_1482]),c_0_1483]) ).
cnf(c_0_1486,plain,
rd(unit,mult(rd(unit,X1),X2)) = ld(X2,X1),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1483,c_0_1481]),c_0_1482]) ).
cnf(c_0_1487,plain,
i(unit) = mult(X1,ld(X1,unit)),
i_0_691 ).
cnf(c_0_1488,plain,
i(unit) = rd(unit,unit),
i_0_652 ).
cnf(c_0_1489,axiom,
mult(rd(X1,X2),X2) = X1,
i_0_17 ).
cnf(c_0_1490,plain,
rd(mult(X1,ld(X2,X1)),X1) = mult(X1,rd(unit,X2)),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1484,c_0_1485]),c_0_1486]) ).
cnf(c_0_1491,plain,
i(unit) = rd(mult(unit,X1),X1),
i_0_677 ).
cnf(c_0_1492,axiom,
mult(unit,X1) = X1,
i_0_22 ).
cnf(c_0_1493,plain,
rd(unit,unit) = unit,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_1487,c_0_1475]),c_0_1488]) ).
cnf(c_0_1494,plain,
mult(mult(X1,rd(unit,X2)),X1) = mult(X1,ld(X2,X1)),
inference(spm,[status(thm)],[c_0_1489,c_0_1490]) ).
cnf(c_0_1495,plain,
rd(unit,rd(X1,X2)) = mult(X2,rd(unit,X1)),
inference(spm,[status(thm)],[c_0_1474,c_0_1489]) ).
cnf(c_0_1496,plain,
rd(X1,X1) = unit,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_1491,c_0_1492]),c_0_1488]),c_0_1493]) ).
cnf(c_0_1497,plain,
mult(X1,ld(mult(X2,X1),X1)) = mult(rd(unit,X2),X1),
inference(spm,[status(thm)],[c_0_1494,c_0_1474]) ).
cnf(c_0_1498,plain,
rd(unit,ld(X1,X2)) = mult(rd(unit,X2),X1),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1474,c_0_1480]),c_0_1495]),c_0_1496]),c_0_1479]) ).
cnf(c_0_1499,plain,
rd(unit,mult(X1,rd(unit,X2))) = rd(X2,X1),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1495,c_0_1495]),c_0_1496]),c_0_1479]) ).
cnf(c_0_1500,plain,
mult(ld(X1,X2),X1) = mult(rd(unit,X1),mult(X2,X1)),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1485,c_0_1497]),c_0_1486]),c_0_1498]) ).
cnf(c_0_1501,plain,
mult(X1,ld(mult(X1,ld(X2,X1)),X1)) = X2,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1497,c_0_1494]),c_0_1499]),c_0_1489]) ).
cnf(c_0_1502,plain,
mult(rd(unit,X1),mult(mult(X1,X2),X1)) = mult(X2,X1),
inference(spm,[status(thm)],[c_0_1500,c_0_1476]) ).
cnf(c_0_1503,plain,
ld(rd(X1,X2),X1) = X2,
inference(spm,[status(thm)],[c_0_1476,c_0_1489]) ).
cnf(c_0_1504,plain,
ld(mult(X1,ld(X2,X1)),X1) = ld(X1,X2),
inference(spm,[status(thm)],[c_0_1476,c_0_1501]) ).
cnf(c_0_1505,plain,
ld(mult(mult(X1,X2),X1),X1) = rd(unit,mult(X2,X1)),
inference(spm,[status(thm)],[c_0_1486,c_0_1502]) ).
cnf(c_0_1506,plain,
mult(rd(unit,X1),rd(X1,X2)) = rd(unit,X2),
inference(spm,[status(thm)],[c_0_1498,c_0_1503]) ).
cnf(c_0_1507,plain,
i(unit) = ld(X1,mult(X1,mult(X2,ld(X2,unit)))),
i_0_695 ).
cnf(c_0_1508,plain,
rd(X1,ld(X1,X2)) = mult(X1,ld(X2,X1)),
inference(spm,[status(thm)],[c_0_1481,c_0_1504]) ).
cnf(c_0_1509,plain,
rd(X1,rd(X1,X2)) = mult(X1,rd(X2,X1)),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1505,c_0_1506]),c_0_1483]),c_0_1484]),c_0_1495]),c_0_1499]),c_0_1499]) ).
cnf(c_0_1510,plain,
ld(X1,X1) = unit,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_1507,c_0_1475]),c_0_1479]),c_0_1488]),c_0_1496]) ).
cnf(c_0_1511,plain,
mult(X1,ld(mult(X1,X2),X1)) = rd(X1,X2),
inference(spm,[status(thm)],[c_0_1508,c_0_1476]) ).
cnf(c_0_1512,plain,
ld(mult(X1,rd(X2,X1)),X1) = rd(X1,X2),
inference(spm,[status(thm)],[c_0_1503,c_0_1509]) ).
cnf(c_0_1513,plain,
ld(rd(mult(X1,X2),X1),mult(X1,mult(X2,X3))) = mult(X1,X3),
inference(spm,[status(thm)],[c_0_1476,c_0_1478]) ).
cnf(c_0_1514,plain,
mult(rd(unit,X1),mult(X1,X1)) = X1,
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1500,c_0_1510]),c_0_1492]) ).
cnf(c_0_1515,plain,
rd(X1,rd(X2,X1)) = mult(X1,rd(X1,X2)),
inference(spm,[status(thm)],[c_0_1511,c_0_1512]) ).
cnf(c_0_1516,plain,
ld(mult(X1,X2),X1) = rd(X1,mult(X2,X1)),
inference(spm,[status(thm)],[c_0_1512,c_0_1469]) ).
cnf(c_0_1517,plain,
ld(rd(mult(X1,X2),X1),X1) = mult(X1,rd(unit,X2)),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1513,c_0_1477]),c_0_1479]) ).
cnf(c_0_1518,plain,
mult(X1,rd(ld(X2,X1),X1)) = rd(X1,X2),
inference(spm,[status(thm)],[c_0_1509,c_0_1481]) ).
cnf(c_0_1519,plain,
ld(X1,rd(X1,X2)) = ld(mult(X1,X2),X1),
inference(spm,[status(thm)],[c_0_1504,c_0_1503]) ).
cnf(c_0_1520,axiom,
mult(mult(X1,X2),X3) = mult(mult(X1,X3),ld(X3,mult(X2,X3))),
i_0_13 ).
cnf(c_0_1521,plain,
mult(mult(X1,X1),X1) = mult(X1,mult(X1,X1)),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1497,c_0_1514]),c_0_1476]),c_0_1495]),c_0_1496]),c_0_1479]) ).
cnf(c_0_1522,plain,
rd(rd(unit,X1),X2) = rd(unit,mult(X2,X1)),
inference(spm,[status(thm)],[c_0_1469,c_0_1485]) ).
cnf(c_0_1523,plain,
rd(X1,mult(rd(X1,X2),X1)) = rd(X2,X1),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1503,c_0_1515]),c_0_1516]) ).
cnf(c_0_1524,plain,
ld(rd(X1,X2),X2) = mult(X2,mult(rd(unit,X1),X2)),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1517,c_0_1475]),c_0_1498]) ).
cnf(c_0_1525,plain,
rd(ld(X1,X2),X2) = rd(X2,mult(X1,X2)),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1476,c_0_1518]),c_0_1519]),c_0_1516]) ).
cnf(c_0_1526,plain,
mult(mult(X1,mult(X2,X2)),X2) = mult(mult(X1,X2),mult(X2,X2)),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1520,c_0_1521]),c_0_1476]) ).
cnf(c_0_1527,plain,
mult(rd(unit,mult(X1,X2)),mult(X1,X3)) = mult(X1,mult(rd(unit,mult(X2,X1)),X3)),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1478,c_0_1474]),c_0_1522]) ).
cnf(c_0_1528,plain,
mult(X1,mult(rd(unit,X2),X1)) = mult(rd(X1,X2),X1),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1503,c_0_1523]),c_0_1524]) ).
cnf(c_0_1529,plain,
mult(rd(X1,mult(X2,X1)),X1) = ld(X2,X1),
inference(spm,[status(thm)],[c_0_1489,c_0_1525]) ).
cnf(c_0_1530,plain,
rd(X1,mult(ld(X2,X1),X1)) = ld(X1,X2),
inference(rw,[status(thm)],[c_0_1504,c_0_1516]) ).
cnf(c_0_1531,plain,
mult(ld(X1,X2),X2) = mult(rd(unit,X1),mult(X2,X2)),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1526,c_0_1527]),c_0_1528]),c_0_1529]),c_0_1485]) ).
cnf(c_0_1532,plain,
rd(X1,mult(rd(unit,X2),mult(X1,X1))) = ld(X1,X2),
inference(rw,[status(thm)],[c_0_1530,c_0_1531]) ).
cnf(c_0_1533,plain,
ld(unit,X1) = X1,
inference(spm,[status(thm)],[c_0_1492,c_0_1475]) ).
cnf(c_0_1534,plain,
mult(X1,mult(mult(rd(unit,X1),X2),X1)) = mult(X2,X1),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1524,c_0_1525]),c_0_1503]),c_0_1498]) ).
cnf(c_0_1535,plain,
ld(ld(rd(unit,X1),X2),X1) = rd(unit,X2),
inference(spm,[status(thm)],[c_0_1486,c_0_1475]) ).
cnf(c_0_1536,plain,
rd(X1,mult(X2,mult(X1,X1))) = rd(unit,mult(X2,X1)),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1532,c_0_1532]),c_0_1533]),c_0_1492]),c_0_1479]),c_0_1483]) ).
cnf(c_0_1537,plain,
mult(b,mult(c,b)) != ld(b,mult(mult(b,mult(b,c)),b)),
i_0_1452 ).
cnf(c_0_1538,plain,
ld(X1,mult(X2,X1)) = mult(mult(rd(unit,X1),X2),X1),
inference(spm,[status(thm)],[c_0_1476,c_0_1534]) ).
cnf(c_0_1539,plain,
ld(rd(unit,X1),X2) = rd(X1,rd(unit,X2)),
inference(spm,[status(thm)],[c_0_1481,c_0_1535]) ).
cnf(c_0_1540,plain,
rd(X1,mult(X1,mult(X2,X1))) = rd(unit,mult(X1,X2)),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1536,c_0_1478]),c_0_1489]) ).
cnf(c_0_1541,plain,
mult(mult(rd(unit,b),mult(b,mult(b,c))),b) != mult(b,mult(c,b)),
inference(rw,[status(thm)],[c_0_1537,c_0_1538]) ).
cnf(c_0_1542,plain,
mult(rd(unit,X1),mult(X1,X2)) = mult(X1,mult(rd(unit,X1),X2)),
inference(spm,[status(thm)],[c_0_1478,c_0_1477]) ).
cnf(c_0_1543,plain,
mult(X1,rd(X2,rd(unit,X1))) = mult(mult(X1,X2),X1),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1494,c_0_1481]),c_0_1482]),c_0_1539]) ).
cnf(c_0_1544,plain,
rd(mult(X1,X2),rd(unit,X1)) = mult(X1,mult(X2,X1)),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1503,c_0_1540]),c_0_1539]) ).
cnf(c_0_1545,plain,
mult(mult(b,mult(b,mult(rd(unit,b),c))),b) != mult(b,mult(c,b)),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_1541,c_0_1542]),c_0_1542]) ).
cnf(c_0_1546,plain,
mult(mult(X1,mult(X1,X2)),X1) = mult(X1,mult(X1,mult(X2,X1))),
inference(spm,[status(thm)],[c_0_1543,c_0_1544]) ).
cnf(c_0_1547,plain,
$false,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_1545,c_0_1546]),c_0_1534])]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.09 % Problem : GRP697-1 : TPTP v9.2.1. Released v4.0.0.
% 0.00/0.09 % Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.12/0.29 % Computer : n020.cluster.edu
% 0.12/0.29 % Model : x86_64 x86_64
% 0.12/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.29 % Memory : 8042.1875MB
% 0.12/0.29 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.29 % CPULimit : 300
% 0.12/0.29 % WCLimit : 300
% 0.12/0.29 % DateTime : Mon May 4 19:02:34 EDT 2026
% 0.12/0.29 % CPUTime :
% 0.12/0.30 % start to proof: theBenchmark
% 103.39/67.63 % Version : CSE_E---1.7
% 103.39/67.63 % Problem : theBenchmark.p
% 103.39/67.63 % SZS status Unsatisfiable for theBenchmark.p
% 103.39/67.63 % SZS output start CNFRefutation
% See solution above
% 104.81/69.03 % Total time : 67.163s
%------------------------------------------------------------------------------