%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : GRP664-11 : TPTP v9.2.1. Released v8.1.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n001.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:26:48 PM UTC 2026
% Result : Unsatisfiable 73.27s 57.22s
% Output : CNFRefutation 75.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 19
% Syntax : Number of clauses : 271 ( 263 unt; 0 nHn; 10 RR)
% Number of literals : 280 ( 279 equ; 14 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 5 con; 0-2 aty)
% Number of variables : 605 ( 28 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(goal2,negated_conjecture,
mult(mult(x2,mult(x1,x0)),x3) != mult(x2,mult(mult(x1,x0),x3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goal2) ).
cnf(f08,axiom,
mult(mult(X1,X2),X3) = mult(mult(X1,X3),ld(X3,mult(X2,X3))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',f08) ).
cnf(f07,axiom,
mult(X1,mult(X2,X3)) = mult(rd(mult(X1,X2),X1),mult(X1,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',f07) ).
cnf(f04,axiom,
rd(mult(X1,X2),X2) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',f04) ).
cnf(f03,axiom,
mult(rd(X1,X2),X2) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',f03) ).
cnf(f01,axiom,
mult(X1,ld(X1,X2)) = X2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',f01) ).
cnf(f02,axiom,
ld(X1,mult(X1,X2)) = X2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',f02) ).
cnf(f06,axiom,
mult(unit,X1) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',f06) ).
cnf(f05,axiom,
mult(X1,unit) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',f05) ).
cnf(goal1,negated_conjecture,
mult(x0,x1) = unit,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goal1) ).
cnf(i_0_10,negated_conjecture,
mult(mult(x2,mult(x1,x0)),x3) != mult(x2,mult(mult(x1,x0),x3)),
goal2,
[final] ).
cnf(i_0_11,axiom,
mult(mult(X1,X2),X3) = mult(mult(X1,X3),ld(X3,mult(X2,X3))),
f08,
[final] ).
cnf(i_0_12,axiom,
mult(X1,mult(X2,X3)) = mult(rd(mult(X1,X2),X1),mult(X1,X3)),
f07,
[final] ).
cnf(i_0_13,axiom,
rd(mult(X1,X2),X2) = X1,
f04,
[final] ).
cnf(i_0_14,axiom,
mult(rd(X1,X2),X2) = X1,
f03,
[final] ).
cnf(i_0_15,axiom,
mult(X1,ld(X1,X2)) = X2,
f01,
[final] ).
cnf(i_0_16,axiom,
ld(X1,mult(X1,X2)) = X2,
f02,
[final] ).
cnf(i_0_17,axiom,
mult(unit,X1) = X1,
f06,
[final] ).
cnf(i_0_18,axiom,
mult(X1,unit) = X1,
f05,
[final] ).
cnf(i_0_19,negated_conjecture,
mult(x0,x1) = unit,
goal1,
[final] ).
cnf(i_0_20,axiom,
X1 = X1 ).
cnf(i_0_21,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_22,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_23,axiom,
( X1 != X2
| mult(X1,X3) = mult(X2,X3) ) ).
cnf(i_0_24,axiom,
( X1 != X2
| mult(X3,X1) = mult(X3,X2) ) ).
cnf(i_0_25,axiom,
( X1 != X2
| ld(X1,X3) = ld(X2,X3) ) ).
cnf(i_0_26,axiom,
( X1 != X2
| ld(X3,X1) = ld(X3,X2) ) ).
cnf(i_0_27,axiom,
( X1 != X2
| rd(X1,X3) = rd(X2,X3) ) ).
cnf(i_0_28,axiom,
( X1 != X2
| rd(X3,X1) = rd(X3,X2) ) ).
cnf(i_0_29,plain,
unit = mult(X1,X2),
inference(scs_inference,[],[i_0_19,i_0_21]) ).
cnf(i_0_30,plain,
mult(unit,mult(X1,X2)) = unit,
inference(scs_inference,[],[i_0_19,i_0_17,i_0_21,i_0_22]) ).
cnf(i_0_31,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_34,plain,
mult(X1,unit) = X1,
inference(rename_variables,[],[i_0_18]) ).
cnf(i_0_37,plain,
mult(rd(mult(X1,X2),X1),mult(X1,X3)) = mult(X1,mult(X2,X3)),
inference(scs_inference,[],[i_0_12,i_0_21]) ).
cnf(i_0_42,plain,
X1 = rd(mult(X1,X2),X2),
inference(scs_inference,[],[i_0_13,i_0_21]) ).
cnf(i_0_60,plain,
X1 = mult(rd(X1,X2),X2),
inference(scs_inference,[],[i_0_14,i_0_21]) ).
cnf(i_0_77,plain,
X1 = mult(X2,ld(X2,X1)),
inference(scs_inference,[],[i_0_15,i_0_21]) ).
cnf(i_0_79,plain,
X1 = ld(X2,mult(X2,X1)),
inference(scs_inference,[],[i_0_16,i_0_21]) ).
cnf(i_0_115,plain,
mult(mult(X1,X2),ld(X2,mult(X3,X2))) = mult(mult(X1,X3),X2),
inference(scs_inference,[],[i_0_11,i_0_21]) ).
cnf(i_0_116,plain,
X1 = mult(unit,X1),
inference(scs_inference,[],[i_0_17,i_0_21]) ).
cnf(i_0_124,plain,
X1 = mult(X1,unit),
inference(scs_inference,[],[i_0_18,i_0_21]) ).
cnf(i_0_408,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_411,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_414,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_417,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_420,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_423,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_426,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_429,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_432,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_435,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_438,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_441,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_444,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_447,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_450,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_453,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_456,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_459,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_462,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_465,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_468,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_471,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_474,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_477,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_480,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_483,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_486,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_489,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_492,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_495,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_498,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_501,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_504,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_507,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_510,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_513,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_516,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_519,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_522,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_530,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_536,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_542,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_545,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_548,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_551,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_554,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_557,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_560,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_563,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_569,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_575,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_578,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_581,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_584,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_587,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_590,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_593,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_596,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_599,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_602,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_605,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_608,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_611,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_614,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_617,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_620,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_623,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_626,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_629,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_632,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_635,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_638,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_641,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_644,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_647,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_650,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_653,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_656,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_665,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_668,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_671,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_674,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_677,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_680,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_683,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_686,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_689,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_692,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_695,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_698,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_701,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_704,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_707,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_710,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_713,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_716,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_719,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_722,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_725,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_728,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_731,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_734,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_737,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_740,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_743,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_746,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_749,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_752,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_755,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_758,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_761,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_764,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_767,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_770,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_773,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_776,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_779,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_782,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_785,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_788,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_791,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_794,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_797,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_800,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_808,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_814,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_817,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_820,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_823,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_826,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_829,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_832,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_838,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_844,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_847,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_850,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_853,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_856,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_859,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_862,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_865,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_868,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_871,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_874,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_877,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_880,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_882,plain,
mult(mult(X1,mult(X2,X3)),X4) != mult(rd(mult(X1,mult(mult(X2,X3),X4)),X5),X5),
inference(scs_inference,[],[i_0_14,i_0_10,i_0_22]) ).
cnf(i_0_883,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_884,plain,
mult(X1,mult(X2,X3)) != rd(mult(X1,mult(mult(X2,X3),X4)),X4),
inference(scs_inference,[],[i_0_14,i_0_10,i_0_22,i_0_23]) ).
cnf(i_0_1300,plain,
mult(X1,mult(X2,X3)) = mult(X1,unit),
inference(scs_inference,[],[i_0_19,i_0_24]) ).
cnf(i_0_1301,plain,
ld(mult(X1,X2),X3) = ld(unit,X3),
inference(scs_inference,[],[i_0_19,i_0_24,i_0_25]) ).
cnf(i_0_1302,plain,
ld(X1,mult(X2,X3)) = ld(X1,unit),
inference(scs_inference,[],[i_0_19,i_0_24,i_0_25,i_0_26]) ).
cnf(i_0_1303,plain,
rd(mult(X1,X2),X3) = rd(unit,X3),
inference(scs_inference,[],[i_0_19,i_0_24,i_0_25,i_0_26,i_0_27]) ).
cnf(i_0_1304,plain,
rd(X1,mult(X2,X3)) = rd(X1,unit),
inference(scs_inference,[],[i_0_19,i_0_24,i_0_25,i_0_26,i_0_27,i_0_28]) ).
cnf(i_0_1305,plain,
mult(mult(X1,X2),X3) = mult(unit,X3),
inference(scs_inference,[],[i_0_19,i_0_24,i_0_25,i_0_26,i_0_27,i_0_28,i_0_23]) ).
cnf(i_0_1398,plain,
mult(X1,mult(mult(X2,X3),X4)) = mult(X1,mult(mult(X2,X4),ld(X4,mult(X3,X4)))),
inference(scs_inference,[],[i_0_11,i_0_24]) ).
cnf(i_0_1399,plain,
ld(mult(mult(X1,X2),X3),X4) = ld(mult(mult(X1,X3),ld(X3,mult(X2,X3))),X4),
inference(scs_inference,[],[i_0_11,i_0_24,i_0_25]) ).
cnf(i_0_1400,plain,
ld(X1,mult(mult(X2,X3),X4)) = ld(X1,mult(mult(X2,X4),ld(X4,mult(X3,X4)))),
inference(scs_inference,[],[i_0_11,i_0_24,i_0_25,i_0_26]) ).
cnf(i_0_1401,plain,
rd(mult(mult(X1,X2),X3),X4) = rd(mult(mult(X1,X3),ld(X3,mult(X2,X3))),X4),
inference(scs_inference,[],[i_0_11,i_0_24,i_0_25,i_0_26,i_0_27]) ).
cnf(i_0_1402,plain,
rd(X1,mult(mult(X2,X3),X4)) = rd(X1,mult(mult(X2,X4),ld(X4,mult(X3,X4)))),
inference(scs_inference,[],[i_0_11,i_0_24,i_0_25,i_0_26,i_0_27,i_0_28]) ).
cnf(i_0_1403,plain,
mult(mult(mult(X1,X2),X3),X4) = mult(mult(mult(X1,X3),ld(X3,mult(X2,X3))),X4),
inference(scs_inference,[],[i_0_11,i_0_24,i_0_25,i_0_26,i_0_27,i_0_28,i_0_23]) ).
cnf(i_0_1405,plain,
mult(mult(X1,X2),X3) = mult(mult(X1,X3),ld(X3,mult(X2,X3))),
inference(rename_variables,[],[i_0_11]) ).
cnf(i_0_1414,plain,
mult(mult(X1,X2),X3) = mult(mult(X1,X3),ld(X3,mult(X2,X3))),
inference(rename_variables,[],[i_0_11]) ).
cnf(i_0_1423,plain,
mult(mult(X1,X2),X3) = mult(mult(X1,X3),ld(X3,mult(X2,X3))),
inference(rename_variables,[],[i_0_11]) ).
cnf(i_0_1432,plain,
mult(mult(X1,X2),X3) = mult(mult(X1,X3),ld(X3,mult(X2,X3))),
inference(rename_variables,[],[i_0_11]) ).
cnf(i_0_1450,plain,
mult(mult(X1,X2),X3) = mult(mult(X1,X3),ld(X3,mult(X2,X3))),
inference(rename_variables,[],[i_0_11]) ).
cnf(i_0_1459,plain,
mult(mult(X1,X2),X3) = mult(mult(X1,X3),ld(X3,mult(X2,X3))),
inference(rename_variables,[],[i_0_11]) ).
cnf(i_0_1468,plain,
mult(mult(X1,X2),X3) = mult(mult(X1,X3),ld(X3,mult(X2,X3))),
inference(rename_variables,[],[i_0_11]) ).
cnf(i_0_1477,plain,
mult(mult(X1,X2),X3) = mult(mult(X1,X3),ld(X3,mult(X2,X3))),
inference(rename_variables,[],[i_0_11]) ).
cnf(i_0_1486,plain,
mult(mult(X1,X2),X3) = mult(mult(X1,X3),ld(X3,mult(X2,X3))),
inference(rename_variables,[],[i_0_11]) ).
cnf(i_0_1495,plain,
mult(mult(X1,X2),X3) = mult(mult(X1,X3),ld(X3,mult(X2,X3))),
inference(rename_variables,[],[i_0_11]) ).
cnf(i_0_1497,plain,
mult(X1,mult(X2,mult(X3,X4))) = mult(X1,mult(rd(mult(X2,X3),X2),mult(X2,X4))),
inference(scs_inference,[],[i_0_12,i_0_24]) ).
cnf(i_0_1498,plain,
ld(mult(X1,mult(X2,X3)),X4) = ld(mult(rd(mult(X1,X2),X1),mult(X1,X3)),X4),
inference(scs_inference,[],[i_0_12,i_0_24,i_0_25]) ).
cnf(i_0_1499,plain,
ld(X1,mult(X2,mult(X3,X4))) = ld(X1,mult(rd(mult(X2,X3),X2),mult(X2,X4))),
inference(scs_inference,[],[i_0_12,i_0_24,i_0_25,i_0_26]) ).
cnf(i_0_1500,plain,
rd(mult(X1,mult(X2,X3)),X4) = rd(mult(rd(mult(X1,X2),X1),mult(X1,X3)),X4),
inference(scs_inference,[],[i_0_12,i_0_24,i_0_25,i_0_26,i_0_27]) ).
cnf(i_0_1501,plain,
rd(X1,mult(X2,mult(X3,X4))) = rd(X1,mult(rd(mult(X2,X3),X2),mult(X2,X4))),
inference(scs_inference,[],[i_0_12,i_0_24,i_0_25,i_0_26,i_0_27,i_0_28]) ).
cnf(i_0_1502,plain,
mult(mult(X1,mult(X2,X3)),X4) = mult(mult(rd(mult(X1,X2),X1),mult(X1,X3)),X4),
inference(scs_inference,[],[i_0_12,i_0_24,i_0_25,i_0_26,i_0_27,i_0_28,i_0_23]) ).
cnf(i_0_1505,plain,
mult(X1,mult(X2,X3)) = mult(rd(mult(X1,X2),X1),mult(X1,X3)),
inference(rename_variables,[],[i_0_12]) ).
cnf(i_0_1531,plain,
mult(X1,mult(X2,X3)) = mult(rd(mult(X1,X2),X1),mult(X1,X3)),
inference(rename_variables,[],[i_0_12]) ).
cnf(i_0_1577,plain,
mult(X1,mult(X2,X3)) = mult(rd(mult(X1,X2),X1),mult(X1,X3)),
inference(rename_variables,[],[i_0_12]) ).
cnf(i_0_1596,plain,
mult(X1,rd(mult(X2,X3),X3)) = mult(X1,X2),
inference(scs_inference,[],[i_0_13,i_0_24]) ).
cnf(i_0_1597,plain,
ld(rd(mult(X1,X2),X2),X3) = ld(X1,X3),
inference(scs_inference,[],[i_0_13,i_0_24,i_0_25]) ).
cnf(i_0_1598,plain,
ld(X1,rd(mult(X2,X3),X3)) = ld(X1,X2),
inference(scs_inference,[],[i_0_13,i_0_24,i_0_25,i_0_26]) ).
cnf(i_0_1599,plain,
rd(rd(mult(X1,X2),X2),X3) = rd(X1,X3),
inference(scs_inference,[],[i_0_13,i_0_24,i_0_25,i_0_26,i_0_27]) ).
cnf(i_0_1600,plain,
rd(X1,rd(mult(X2,X3),X3)) = rd(X1,X2),
inference(scs_inference,[],[i_0_13,i_0_24,i_0_25,i_0_26,i_0_27,i_0_28]) ).
cnf(i_0_1601,plain,
mult(rd(mult(X1,X2),X2),X3) = mult(X1,X3),
inference(scs_inference,[],[i_0_13,i_0_24,i_0_25,i_0_26,i_0_27,i_0_28,i_0_23]) ).
cnf(i_0_1612,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_1630,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_1647,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_1664,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_1672,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_1685,plain,
mult(X1,mult(rd(X2,X3),X3)) = mult(X1,X2),
inference(scs_inference,[],[i_0_14,i_0_24]) ).
cnf(i_0_1686,plain,
ld(mult(rd(X1,X2),X2),X3) = ld(X1,X3),
inference(scs_inference,[],[i_0_14,i_0_24,i_0_25]) ).
cnf(i_0_1687,plain,
ld(X1,mult(rd(X2,X3),X3)) = ld(X1,X2),
inference(scs_inference,[],[i_0_14,i_0_24,i_0_25,i_0_26]) ).
cnf(i_0_1688,plain,
rd(mult(rd(X1,X2),X2),X3) = rd(X1,X3),
inference(scs_inference,[],[i_0_14,i_0_24,i_0_25,i_0_26,i_0_27]) ).
cnf(i_0_1689,plain,
rd(X1,mult(rd(X2,X3),X3)) = rd(X1,X2),
inference(scs_inference,[],[i_0_14,i_0_24,i_0_25,i_0_26,i_0_27,i_0_28]) ).
cnf(i_0_1690,plain,
mult(mult(rd(X1,X2),X2),X3) = mult(X1,X3),
inference(scs_inference,[],[i_0_14,i_0_24,i_0_25,i_0_26,i_0_27,i_0_28,i_0_23]) ).
cnf(i_0_1758,plain,
mult(X1,ld(X1,X2)) = X2,
inference(rename_variables,[],[i_0_15]) ).
cnf(i_0_1767,plain,
mult(X1,ld(X1,X2)) = X2,
inference(rename_variables,[],[i_0_15]) ).
cnf(i_0_1774,plain,
mult(X1,ld(X1,X2)) = X2,
inference(rename_variables,[],[i_0_15]) ).
cnf(i_0_1780,plain,
mult(X1,ld(X1,X2)) = X2,
inference(rename_variables,[],[i_0_15]) ).
cnf(i_0_1782,plain,
ld(ld(X1,mult(X1,X2)),X3) = ld(X2,X3),
inference(scs_inference,[],[i_0_16,i_0_25]) ).
cnf(i_0_1783,plain,
ld(X1,ld(X2,mult(X2,X3))) = ld(X1,X3),
inference(scs_inference,[],[i_0_16,i_0_25,i_0_26]) ).
cnf(i_0_1784,plain,
rd(ld(X1,mult(X1,X2)),X3) = rd(X2,X3),
inference(scs_inference,[],[i_0_16,i_0_25,i_0_26,i_0_27]) ).
cnf(i_0_1785,plain,
rd(X1,ld(X2,mult(X2,X3))) = rd(X1,X3),
inference(scs_inference,[],[i_0_16,i_0_25,i_0_26,i_0_27,i_0_28]) ).
cnf(i_0_1787,plain,
ld(X1,mult(X1,X2)) = X2,
inference(rename_variables,[],[i_0_16]) ).
cnf(i_0_1789,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_32,plain,
unit = mult(unit,mult(X1,X2)),
inference(scs_inference,[],[i_0_30,i_0_21]) ).
cnf(i_0_33,plain,
mult(mult(unit,mult(X1,X2)),unit) = unit,
inference(scs_inference,[],[i_0_30,i_0_18,i_0_21,i_0_22]) ).
cnf(i_0_41,plain,
mult(rd(mult(X1,X2),X1),mult(X1,X3)) = mult(X1,mult(X2,X3)),
inference(rename_variables,[],[i_0_37]) ).
cnf(i_0_43,plain,
mult(rd(mult(unit,X1),unit),mult(unit,X2)) = unit,
inference(scs_inference,[],[i_0_37,i_0_30,i_0_13,i_0_21,i_0_22]) ).
cnf(i_0_44,plain,
mult(rd(mult(X1,X2),X1),mult(X1,X3)) = mult(X1,mult(X2,X3)),
inference(rename_variables,[],[i_0_37]) ).
cnf(i_0_47,plain,
X1 = rd(mult(X1,X2),X2),
inference(rename_variables,[],[i_0_42]) ).
cnf(i_0_52,plain,
X1 = rd(mult(X1,X2),X2),
inference(rename_variables,[],[i_0_42]) ).
cnf(i_0_65,plain,
X1 = mult(rd(X1,X2),X2),
inference(rename_variables,[],[i_0_60]) ).
cnf(i_0_80,plain,
X1 = mult(rd(mult(X2,ld(X2,X1)),X3),X3),
inference(scs_inference,[],[i_0_77,i_0_60,i_0_16,i_0_21,i_0_22]) ).
cnf(i_0_81,plain,
X1 = mult(rd(X1,X2),X2),
inference(rename_variables,[],[i_0_60]) ).
cnf(i_0_84,plain,
X1 = mult(X2,ld(X2,X1)),
inference(rename_variables,[],[i_0_77]) ).
cnf(i_0_87,plain,
X1 = ld(X2,mult(X2,X1)),
inference(rename_variables,[],[i_0_79]) ).
cnf(i_0_108,plain,
mult(rd(mult(X1,X2),X1),mult(X1,X3)) = mult(X1,mult(X2,X3)),
inference(rename_variables,[],[i_0_37]) ).
cnf(i_0_118,plain,
mult(mult(X1,X2),ld(X2,mult(X3,X2))) = mult(mult(X1,X3),X2),
inference(rename_variables,[],[i_0_115]) ).
cnf(i_0_121,plain,
mult(mult(X1,X2),ld(X2,mult(X3,X2))) = mult(mult(X1,X3),X2),
inference(rename_variables,[],[i_0_115]) ).
cnf(i_0_127,plain,
X1 = mult(X1,unit),
inference(rename_variables,[],[i_0_124]) ).
cnf(i_0_147,plain,
X1 = mult(unit,X1),
inference(rename_variables,[],[i_0_116]) ).
cnf(i_0_169,plain,
mult(X1,X2) = mult(unit,unit),
inference(scs_inference,[],[i_0_19,i_0_116,i_0_22]) ).
cnf(i_0_170,plain,
X1 = mult(unit,X1),
inference(rename_variables,[],[i_0_116]) ).
cnf(i_0_171,plain,
mult(unit,unit) = mult(X1,X2),
inference(scs_inference,[],[i_0_19,i_0_116,i_0_22,i_0_21]) ).
cnf(c_0_885,plain,
mult(mult(X1,mult(X2,X3)),X4) != mult(rd(mult(X1,mult(mult(X2,X3),X4)),X5),X5),
i_0_882 ).
cnf(c_0_886,plain,
unit = mult(X1,X2),
i_0_29 ).
cnf(c_0_887,plain,
$false,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_885,c_0_886]),c_0_886]),c_0_886]),c_0_886]),c_0_886]),c_0_886]),c_0_886])]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : GRP664-11 : TPTP v9.2.1. Released v8.1.0.
% 0.00/0.12 % Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.16/0.34 % Computer : n001.cluster.edu
% 0.16/0.34 % Model : x86_64 x86_64
% 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.34 % Memory : 8042.1875MB
% 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.34 % CPULimit : 300
% 0.16/0.34 % WCLimit : 300
% 0.16/0.34 % DateTime : Mon May 4 19:01:03 EDT 2026
% 0.16/0.34 % CPUTime :
% 0.16/0.35 % start to proof: theBenchmark
% 73.27/57.22 % Version : CSE_E---1.7
% 73.27/57.22 % Problem : theBenchmark.p
% 73.27/57.22 % SZS status Unsatisfiable for theBenchmark.p
% 73.27/57.22 % SZS output start CNFRefutation
% See solution above
% 75.15/59.18 % Total time : 56.869s
%------------------------------------------------------------------------------