%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : GRP664-12 : TPTP v9.2.1. Released v8.1.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 : n005.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 100.53s 67.78s
% Output : CNFRefutation 101.85s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 19
% Syntax : Number of clauses : 267 ( 259 unt; 0 nHn; 8 RR)
% Number of literals : 276 ( 275 equ; 12 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 4 ( 1 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 : 421 ( 18 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(goal2,negated_conjecture,
mult(mult(x2,x3),mult(x1,x0)) != mult(x2,mult(x3,mult(x1,x0))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goal2) ).
cnf(f08,axiom,
mult(mult(X1,X2),X3) = mult(mult(X1,X3),ld(X3,mult(X2,X3))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f08) ).
cnf(f07,axiom,
mult(X1,mult(X2,X3)) = mult(rd(mult(X1,X2),X1),mult(X1,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f07) ).
cnf(f04,axiom,
rd(mult(X1,X2),X2) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f04) ).
cnf(f03,axiom,
mult(rd(X1,X2),X2) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f03) ).
cnf(f01,axiom,
mult(X1,ld(X1,X2)) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f01) ).
cnf(f02,axiom,
ld(X1,mult(X1,X2)) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f02) ).
cnf(f06,axiom,
mult(unit,X1) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f06) ).
cnf(f05,axiom,
mult(X1,unit) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',f05) ).
cnf(goal1,negated_conjecture,
mult(x0,x1) = unit,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goal1) ).
cnf(i_0_10,negated_conjecture,
mult(mult(x2,x3),mult(x1,x0)) != mult(x2,mult(x3,mult(x1,x0))),
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_57,plain,
X1 = mult(rd(X1,X2),X2),
inference(scs_inference,[],[i_0_14,i_0_21]) ).
cnf(i_0_58,plain,
X1 = mult(X2,ld(X2,X1)),
inference(scs_inference,[],[i_0_15,i_0_21]) ).
cnf(i_0_59,plain,
X1 = ld(X2,mult(X2,X1)),
inference(scs_inference,[],[i_0_16,i_0_21]) ).
cnf(i_0_60,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_61,plain,
X1 = mult(unit,X1),
inference(scs_inference,[],[i_0_17,i_0_21]) ).
cnf(i_0_62,plain,
X1 = mult(X1,unit),
inference(scs_inference,[],[i_0_18,i_0_21]) ).
cnf(i_0_171,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_174,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_177,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_180,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_194,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_197,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_200,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_203,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_206,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_209,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_212,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_218,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_224,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_227,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_230,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_233,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_236,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_239,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_242,plain,
rd(mult(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_13]) ).
cnf(i_0_245,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_248,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_251,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_254,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_257,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_260,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_263,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_266,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_277,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_280,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_283,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_286,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_289,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_292,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_295,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_301,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_307,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_310,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_312,plain,
mult(rd(mult(X1,X2),X3),X3) = unit,
inference(scs_inference,[],[i_0_14,i_0_19,i_0_22]) ).
cnf(i_0_313,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_314,plain,
unit = mult(rd(mult(X1,X2),X3),X3),
inference(scs_inference,[],[i_0_14,i_0_19,i_0_22,i_0_21]) ).
cnf(i_0_316,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_319,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_322,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_325,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_328,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_331,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_334,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_337,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_340,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_343,plain,
mult(rd(X1,X2),X2) = X1,
inference(rename_variables,[],[i_0_14]) ).
cnf(i_0_346,plain,
mult(X1,ld(X1,X2)) = X2,
inference(rename_variables,[],[i_0_15]) ).
cnf(i_0_349,plain,
mult(X1,ld(X1,X2)) = X2,
inference(rename_variables,[],[i_0_15]) ).
cnf(i_0_352,plain,
mult(X1,ld(X1,X2)) = X2,
inference(rename_variables,[],[i_0_15]) ).
cnf(i_0_355,plain,
mult(X1,ld(X1,X2)) = X2,
inference(rename_variables,[],[i_0_15]) ).
cnf(i_0_358,plain,
mult(X1,ld(X1,X2)) = X2,
inference(rename_variables,[],[i_0_15]) ).
cnf(i_0_361,plain,
mult(X1,ld(X1,X2)) = X2,
inference(rename_variables,[],[i_0_15]) ).
cnf(i_0_364,plain,
mult(X1,ld(X1,X2)) = X2,
inference(rename_variables,[],[i_0_15]) ).
cnf(i_0_367,plain,
mult(X1,ld(X1,X2)) = X2,
inference(rename_variables,[],[i_0_15]) ).
cnf(i_0_370,plain,
mult(X1,ld(X1,X2)) = X2,
inference(rename_variables,[],[i_0_15]) ).
cnf(i_0_378,plain,
mult(X1,ld(X1,X2)) = X2,
inference(rename_variables,[],[i_0_15]) ).
cnf(i_0_381,plain,
mult(X1,ld(X1,X2)) = X2,
inference(rename_variables,[],[i_0_15]) ).
cnf(i_0_384,plain,
mult(X1,ld(X1,X2)) = X2,
inference(rename_variables,[],[i_0_15]) ).
cnf(i_0_387,plain,
mult(X1,ld(X1,X2)) = X2,
inference(rename_variables,[],[i_0_15]) ).
cnf(i_0_390,plain,
mult(X1,ld(X1,X2)) = X2,
inference(rename_variables,[],[i_0_15]) ).
cnf(i_0_393,plain,
mult(X1,ld(X1,X2)) = X2,
inference(rename_variables,[],[i_0_15]) ).
cnf(i_0_399,plain,
mult(X1,ld(X1,X2)) = X2,
inference(rename_variables,[],[i_0_15]) ).
cnf(i_0_405,plain,
mult(X1,ld(X1,X2)) = X2,
inference(rename_variables,[],[i_0_15]) ).
cnf(i_0_408,plain,
mult(X1,ld(X1,X2)) = X2,
inference(rename_variables,[],[i_0_15]) ).
cnf(i_0_410,plain,
mult(X1,ld(X1,mult(X2,X3))) = unit,
inference(scs_inference,[],[i_0_15,i_0_19,i_0_22]) ).
cnf(i_0_411,plain,
mult(X1,ld(X1,X2)) = X2,
inference(rename_variables,[],[i_0_15]) ).
cnf(i_0_412,plain,
unit = mult(X1,ld(X1,mult(X2,X3))),
inference(scs_inference,[],[i_0_15,i_0_19,i_0_22,i_0_21]) ).
cnf(i_0_414,plain,
mult(X1,ld(X1,X2)) = X2,
inference(rename_variables,[],[i_0_15]) ).
cnf(i_0_417,plain,
mult(X1,ld(X1,X2)) = X2,
inference(rename_variables,[],[i_0_15]) ).
cnf(i_0_420,plain,
mult(X1,ld(X1,X2)) = X2,
inference(rename_variables,[],[i_0_15]) ).
cnf(i_0_423,plain,
mult(X1,ld(X1,X2)) = X2,
inference(rename_variables,[],[i_0_15]) ).
cnf(i_0_426,plain,
mult(X1,ld(X1,X2)) = X2,
inference(rename_variables,[],[i_0_15]) ).
cnf(i_0_429,plain,
mult(X1,ld(X1,X2)) = X2,
inference(rename_variables,[],[i_0_15]) ).
cnf(i_0_432,plain,
mult(X1,ld(X1,X2)) = X2,
inference(rename_variables,[],[i_0_15]) ).
cnf(i_0_435,plain,
mult(X1,ld(X1,X2)) = X2,
inference(rename_variables,[],[i_0_15]) ).
cnf(i_0_438,plain,
mult(X1,ld(X1,X2)) = X2,
inference(rename_variables,[],[i_0_15]) ).
cnf(i_0_441,plain,
ld(X1,mult(X1,X2)) = X2,
inference(rename_variables,[],[i_0_16]) ).
cnf(i_0_444,plain,
ld(X1,mult(X1,X2)) = X2,
inference(rename_variables,[],[i_0_16]) ).
cnf(i_0_447,plain,
ld(X1,mult(X1,X2)) = X2,
inference(rename_variables,[],[i_0_16]) ).
cnf(i_0_450,plain,
ld(X1,mult(X1,X2)) = X2,
inference(rename_variables,[],[i_0_16]) ).
cnf(i_0_453,plain,
ld(X1,mult(X1,X2)) = X2,
inference(rename_variables,[],[i_0_16]) ).
cnf(i_0_456,plain,
ld(X1,mult(X1,X2)) = X2,
inference(rename_variables,[],[i_0_16]) ).
cnf(i_0_459,plain,
ld(X1,mult(X1,X2)) = X2,
inference(rename_variables,[],[i_0_16]) ).
cnf(i_0_462,plain,
ld(X1,mult(X1,X2)) = X2,
inference(rename_variables,[],[i_0_16]) ).
cnf(i_0_465,plain,
ld(X1,mult(X1,X2)) = X2,
inference(rename_variables,[],[i_0_16]) ).
cnf(i_0_468,plain,
ld(X1,mult(X1,X2)) = X2,
inference(rename_variables,[],[i_0_16]) ).
cnf(i_0_471,plain,
ld(X1,mult(X1,X2)) = X2,
inference(rename_variables,[],[i_0_16]) ).
cnf(i_0_476,plain,
ld(X1,mult(X1,X2)) = X2,
inference(rename_variables,[],[i_0_16]) ).
cnf(i_0_479,plain,
ld(X1,mult(X1,X2)) = X2,
inference(rename_variables,[],[i_0_16]) ).
cnf(i_0_482,plain,
ld(X1,mult(X1,X2)) = X2,
inference(rename_variables,[],[i_0_16]) ).
cnf(i_0_485,plain,
ld(X1,mult(X1,X2)) = X2,
inference(rename_variables,[],[i_0_16]) ).
cnf(i_0_488,plain,
ld(X1,mult(X1,X2)) = X2,
inference(rename_variables,[],[i_0_16]) ).
cnf(i_0_491,plain,
ld(X1,mult(X1,X2)) = X2,
inference(rename_variables,[],[i_0_16]) ).
cnf(i_0_497,plain,
ld(X1,mult(X1,X2)) = X2,
inference(rename_variables,[],[i_0_16]) ).
cnf(i_0_503,plain,
ld(X1,mult(X1,X2)) = X2,
inference(rename_variables,[],[i_0_16]) ).
cnf(i_0_506,plain,
ld(X1,mult(X1,X2)) = X2,
inference(rename_variables,[],[i_0_16]) ).
cnf(i_0_508,plain,
ld(X1,mult(X1,mult(X2,X3))) = unit,
inference(scs_inference,[],[i_0_16,i_0_19,i_0_22]) ).
cnf(i_0_509,plain,
ld(X1,mult(X1,X2)) = X2,
inference(rename_variables,[],[i_0_16]) ).
cnf(i_0_510,plain,
unit = ld(X1,mult(X1,mult(X2,X3))),
inference(scs_inference,[],[i_0_16,i_0_19,i_0_22,i_0_21]) ).
cnf(i_0_512,plain,
ld(X1,mult(X1,X2)) = X2,
inference(rename_variables,[],[i_0_16]) ).
cnf(i_0_515,plain,
ld(X1,mult(X1,X2)) = X2,
inference(rename_variables,[],[i_0_16]) ).
cnf(i_0_518,plain,
ld(X1,mult(X1,X2)) = X2,
inference(rename_variables,[],[i_0_16]) ).
cnf(i_0_521,plain,
ld(X1,mult(X1,X2)) = X2,
inference(rename_variables,[],[i_0_16]) ).
cnf(i_0_524,plain,
ld(X1,mult(X1,X2)) = X2,
inference(rename_variables,[],[i_0_16]) ).
cnf(i_0_527,plain,
ld(X1,mult(X1,X2)) = X2,
inference(rename_variables,[],[i_0_16]) ).
cnf(i_0_530,plain,
ld(X1,mult(X1,X2)) = X2,
inference(rename_variables,[],[i_0_16]) ).
cnf(i_0_533,plain,
ld(X1,mult(X1,X2)) = X2,
inference(rename_variables,[],[i_0_16]) ).
cnf(i_0_536,plain,
ld(X1,mult(X1,X2)) = X2,
inference(rename_variables,[],[i_0_16]) ).
cnf(i_0_539,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_542,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_545,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_548,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_551,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_554,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_557,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_560,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_563,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_566,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_569,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_572,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_575,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_578,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_581,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_584,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_587,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_590,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_593,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_596,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_599,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_602,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_605,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_608,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_611,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_614,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_617,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_620,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_623,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_626,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_629,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_632,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_635,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_638,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_641,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_644,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_647,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_650,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_653,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_656,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_659,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_662,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_665,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_668,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_671,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_674,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_677,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_680,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_683,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_686,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_689,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_692,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_695,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_698,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_701,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_704,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_707,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_710,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_713,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_716,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_719,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_722,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_725,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_728,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_731,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_734,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_737,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_740,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_743,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_746,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_749,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_752,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_755,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_758,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_761,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_764,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_770,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_773,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_776,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_779,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_782,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_785,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_788,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_791,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_794,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_797,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_800,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_803,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_806,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_809,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_812,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_815,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_818,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_821,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_824,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_827,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_830,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_833,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_836,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_839,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_842,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_845,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_848,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_851,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_854,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_857,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_860,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_863,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_866,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_869,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(i_0_872,plain,
mult(unit,X1) = X1,
inference(rename_variables,[],[i_0_17]) ).
cnf(c_0_32,negated_conjecture,
mult(mult(x2,x3),mult(x1,x0)) != mult(x2,mult(x3,mult(x1,x0))),
i_0_10 ).
cnf(c_0_33,plain,
unit = mult(X1,X2),
i_0_29 ).
cnf(c_0_34,negated_conjecture,
$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)],[c_0_32,c_0_33]),c_0_33]),c_0_33]),c_0_33]),c_0_33]),c_0_33])]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : GRP664-12 : TPTP v9.2.1. Released v8.1.0.
% 0.00/0.12 % 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.14/0.33 % Computer : n005.cluster.edu
% 0.14/0.33 % Model : x86_64 x86_64
% 0.14/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.33 % Memory : 8042.1875MB
% 0.14/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.33 % CPULimit : 300
% 0.14/0.33 % WCLimit : 300
% 0.14/0.33 % DateTime : Mon May 4 19:00:30 EDT 2026
% 0.14/0.33 % CPUTime :
% 0.14/0.34 % start to proof: theBenchmark
% 100.53/67.78 % Version : CSE_E---1.7
% 100.53/67.78 % Problem : theBenchmark.p
% 100.53/67.78 % SZS status Unsatisfiable for theBenchmark.p
% 100.53/67.78 % SZS output start CNFRefutation
% See solution above
% 101.85/69.09 % Total time : 67.426s
%------------------------------------------------------------------------------