%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP718-1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n010.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:28:17 PM UTC 2026
% Result : Unsatisfiable 57.95s 13.04s
% Output : CNFRefutation 57.95s
% Verified :
% SZS Type : Refutation
% Derivation depth : 74
% Number of leaves : 18
% Syntax : Number of clauses : 281 ( 281 unt; 0 nHn; 109 RR)
% Number of literals : 281 ( 280 equ; 17 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 11 con; 0-2 aty)
% Number of variables : 325 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t3,axiom,
mult(X1,X2) = mult(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t49,plain,
mult(X1,X2) = mult(X2,X1),
inference(orient,[status(thm)],[t3]) ).
cnf(t10,axiom,
sFlat0 = mult(a,a),
introduced(definition) ).
cnf(t94,plain,
mult(a,a) = sFlat0,
inference(orient,[status(thm)],[t10]) ).
cnf(t12,axiom,
sFlat2 = mult(c,mult(a,a)),
introduced(definition) ).
cnf(t32401,plain,
sFlat2 = mult(c,sFlat0),
inference(step,[status(thm)],[t12,t94]) ).
cnf(t32402,plain,
sFlat2 = mult(sFlat0,c),
inference(step,[status(thm)],[t32401,t49]) ).
cnf(t109,plain,
mult(sFlat0,c) = sFlat2,
inference(orient,[status(thm)],[t32402]) ).
cnf(t9,axiom,
mult(mult(mult(X1,mult(X2,X3)),X1),X2) = mult(mult(X1,X2),mult(X3,mult(X1,X2))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t32388,plain,
mult(X2,mult(mult(X1,mult(X2,X3)),X1)) = mult(mult(X1,X2),mult(X3,mult(X1,X2))),
inference(step,[status(thm)],[t9,t49]) ).
cnf(t32389,plain,
mult(X2,mult(X1,mult(X1,mult(X2,X3)))) = mult(mult(X1,X2),mult(X3,mult(X1,X2))),
inference(step,[status(thm)],[t32388,t49]) ).
cnf(t52,plain,
mult(mult(X1,X2),mult(X3,mult(X1,X2))) = mult(X2,mult(X1,mult(X1,mult(X2,X3)))),
inference(orient,[status(thm)],[t32389]) ).
cnf(t4,axiom,
mult(X1,ld(X1,X2)) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t17,plain,
mult(X1,ld(X1,X2)) = X2,
inference(orient,[status(thm)],[t4]) ).
cnf(t53,plain,
mult(ld(X1,X2),mult(X1,mult(X1,mult(ld(X1,X2),X3)))) = mult(X2,mult(X3,mult(X1,ld(X1,X2)))),
inference(cp,[status(thm)],[t52,t17]) ).
cnf(t8,axiom,
mult(mult(X1,X2),i(X2)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t19,plain,
mult(mult(X1,X2),i(X2)) = X1,
inference(orient,[status(thm)],[t8]) ).
cnf(t5,axiom,
mult(rd(X1,X2),X2) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t33,plain,
mult(rd(X1,X2),X2) = X1,
inference(orient,[status(thm)],[t5]) ).
cnf(t36,plain,
rd(X1,X2) = mult(X1,i(X2)),
inference(cp,[status(thm)],[t19,t33]) ).
cnf(t172,plain,
mult(X1,i(X2)) = rd(X1,X2),
inference(orient,[status(thm)],[t36]) ).
cnf(t175,plain,
rd(X1,X2) = mult(i(X2),X1),
inference(cp,[status(thm)],[t172,t49]) ).
cnf(t7,axiom,
mult(i(X1),mult(X1,X2)) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t26,plain,
mult(i(X1),mult(X1,X2)) = X2,
inference(orient,[status(thm)],[t7]) ).
cnf(t27,plain,
ld(X1,X2) = mult(i(X1),X2),
inference(cp,[status(thm)],[t26,t17]) ).
cnf(t163,plain,
mult(i(X1),X2) = ld(X1,X2),
inference(orient,[status(thm)],[t27]) ).
cnf(t32410,plain,
rd(X1,X2) = ld(X2,X1),
inference(step,[status(thm)],[t175,t163]) ).
cnf(t185,plain,
ld(X1,X2) = rd(X2,X1),
inference(orient,[status(thm)],[t32410]) ).
cnf(t32447,plain,
mult(rd(X2,X1),mult(X1,mult(X1,mult(ld(X1,X2),X3)))) = mult(X2,mult(X3,mult(X1,ld(X1,X2)))),
inference(step,[status(thm)],[t53,t185]) ).
cnf(t32411,plain,
mult(i(X1),X2) = rd(X2,X1),
inference(step,[status(thm)],[t163,t185]) ).
cnf(t186,plain,
mult(i(X1),X2) = rd(X2,X1),
inference(orient,[status(thm)],[t32411]) ).
cnf(t2,axiom,
ld(X1,mult(X1,X2)) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t43,plain,
ld(X1,mult(X1,X2)) = X2,
inference(orient,[status(thm)],[t2]) ).
cnf(t48,plain,
i(X1) = ld(mult(X2,X1),X2),
inference(cp,[status(thm)],[t43,t19]) ).
cnf(t32423,plain,
i(X1) = rd(X2,mult(X2,X1)),
inference(step,[status(thm)],[t48,t185]) ).
cnf(t214,plain,
rd(X1,mult(X1,X2)) = i(X2),
inference(orient,[status(thm)],[t32423]) ).
cnf(t50,plain,
mult(rd(X1,X2),X2) = X1,
inference(rw,[status(thm)],[t33]) ).
cnf(t32422,plain,
mult(X2,rd(X1,X2)) = X1,
inference(step,[status(thm)],[t50,t49]) ).
cnf(t205,plain,
mult(X1,rd(X2,X1)) = X2,
inference(orient,[status(thm)],[t32422]) ).
cnf(t215,plain,
i(rd(X1,X2)) = rd(X2,X1),
inference(cp,[status(thm)],[t214,t205]) ).
cnf(t224,plain,
i(rd(X1,X2)) = rd(X2,X1),
inference(orient,[status(thm)],[t215]) ).
cnf(t230,plain,
rd(X1,rd(X2,X3)) = mult(rd(X3,X2),X1),
inference(cp,[status(thm)],[t186,t224]) ).
cnf(t315,plain,
mult(rd(X1,X2),X3) = rd(X3,rd(X2,X1)),
inference(orient,[status(thm)],[t230]) ).
cnf(t32448,plain,
rd(mult(X1,mult(X1,mult(ld(X1,X2),X3))),rd(X1,X2)) = mult(X2,mult(X3,mult(X1,ld(X1,X2)))),
inference(step,[status(thm)],[t32447,t315]) ).
cnf(t32449,plain,
rd(mult(X1,mult(X1,mult(rd(X2,X1),X3))),rd(X1,X2)) = mult(X2,mult(X3,mult(X1,ld(X1,X2)))),
inference(step,[status(thm)],[t32448,t185]) ).
cnf(t32450,plain,
rd(mult(X1,mult(X1,rd(X3,rd(X1,X2)))),rd(X1,X2)) = mult(X2,mult(X3,mult(X1,ld(X1,X2)))),
inference(step,[status(thm)],[t32449,t315]) ).
cnf(t228,plain,
rd(X1,rd(X2,X3)) = mult(X1,rd(X3,X2)),
inference(cp,[status(thm)],[t172,t224]) ).
cnf(t308,plain,
mult(X1,rd(X2,X3)) = rd(X1,rd(X3,X2)),
inference(orient,[status(thm)],[t228]) ).
cnf(t32451,plain,
rd(mult(X1,rd(X1,rd(rd(X1,X2),X3))),rd(X1,X2)) = mult(X2,mult(X3,mult(X1,ld(X1,X2)))),
inference(step,[status(thm)],[t32450,t308]) ).
cnf(t32452,plain,
rd(rd(X1,rd(rd(rd(X1,X2),X3),X1)),rd(X1,X2)) = mult(X2,mult(X3,mult(X1,ld(X1,X2)))),
inference(step,[status(thm)],[t32451,t308]) ).
cnf(t32453,plain,
rd(rd(X1,rd(rd(rd(X1,X2),X3),X1)),rd(X1,X2)) = mult(X2,mult(X3,mult(X1,rd(X2,X1)))),
inference(step,[status(thm)],[t32452,t185]) ).
cnf(t32454,plain,
rd(rd(X1,rd(rd(rd(X1,X2),X3),X1)),rd(X1,X2)) = mult(X2,mult(X3,rd(X1,rd(X1,X2)))),
inference(step,[status(thm)],[t32453,t308]) ).
cnf(t20,plain,
X1 = mult(X2,i(ld(X1,X2))),
inference(cp,[status(thm)],[t19,t17]) ).
cnf(t32420,plain,
X1 = rd(X2,ld(X1,X2)),
inference(step,[status(thm)],[t20,t172]) ).
cnf(t32421,plain,
X1 = rd(X2,rd(X2,X1)),
inference(step,[status(thm)],[t32420,t185]) ).
cnf(t201,plain,
rd(X1,rd(X1,X2)) = X2,
inference(orient,[status(thm)],[t32421]) ).
cnf(t32455,plain,
rd(rd(X1,rd(rd(rd(X1,X2),X3),X1)),rd(X1,X2)) = mult(X2,mult(X3,X2)),
inference(step,[status(thm)],[t32454,t201]) ).
cnf(t438,plain,
rd(rd(X1,rd(rd(rd(X1,X2),X3),X1)),rd(X1,X2)) = mult(X2,mult(X3,X2)),
inference(orient,[status(thm)],[t32455]) ).
cnf(t6,axiom,
rd(mult(X1,X2),X2) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t37,plain,
rd(mult(X1,X2),X2) = X1,
inference(orient,[status(thm)],[t6]) ).
cnf(t1,axiom,
mult(unit,X1) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t23,plain,
mult(unit,X1) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t41,plain,
unit = rd(X1,X1),
inference(cp,[status(thm)],[t37,t23]) ).
cnf(t115,plain,
rd(X1,X1) = unit,
inference(orient,[status(thm)],[t41]) ).
cnf(t444,plain,
mult(X1,mult(rd(X2,X1),X1)) = rd(rd(X2,rd(unit,X2)),rd(X2,X1)),
inference(cp,[status(thm)],[t438,t115]) ).
cnf(t32475,plain,
mult(X1,rd(X1,rd(X1,X2))) = rd(rd(X2,rd(unit,X2)),rd(X2,X1)),
inference(step,[status(thm)],[t444,t315]) ).
cnf(t32476,plain,
mult(X1,X2) = rd(rd(X2,rd(unit,X2)),rd(X2,X1)),
inference(step,[status(thm)],[t32475,t201]) ).
cnf(t174,plain,
rd(unit,X1) = i(X1),
inference(cp,[status(thm)],[t172,t23]) ).
cnf(t184,plain,
rd(unit,X1) = i(X1),
inference(orient,[status(thm)],[t174]) ).
cnf(t32477,plain,
mult(X1,X2) = rd(rd(X2,i(X2)),rd(X2,X1)),
inference(step,[status(thm)],[t32476,t184]) ).
cnf(t42,plain,
mult(X1,X2) = rd(X1,i(X2)),
inference(cp,[status(thm)],[t37,t19]) ).
cnf(t195,plain,
rd(X1,i(X2)) = mult(X1,X2),
inference(orient,[status(thm)],[t42]) ).
cnf(t32478,plain,
mult(X1,X2) = rd(mult(X2,X2),rd(X2,X1)),
inference(step,[status(thm)],[t32477,t195]) ).
cnf(t664,plain,
rd(mult(X1,X1),rd(X1,X2)) = mult(X2,X1),
inference(orient,[status(thm)],[t32478]) ).
cnf(t40,plain,
i(X1) = rd(X2,mult(X1,X2)),
inference(cp,[status(thm)],[t37,t26]) ).
cnf(t208,plain,
rd(X1,mult(X2,X1)) = i(X2),
inference(orient,[status(thm)],[t40]) ).
cnf(t673,plain,
mult(mult(X1,X2),X2) = rd(mult(X2,X2),i(X1)),
inference(cp,[status(thm)],[t664,t208]) ).
cnf(t32491,plain,
mult(X2,mult(X1,X2)) = rd(mult(X2,X2),i(X1)),
inference(step,[status(thm)],[t673,t49]) ).
cnf(t32492,plain,
mult(X2,mult(X1,X2)) = mult(mult(X2,X2),X1),
inference(step,[status(thm)],[t32491,t195]) ).
cnf(t773,plain,
mult(mult(X1,X1),X2) = mult(X1,mult(X2,X1)),
inference(orient,[status(thm)],[t32492]) ).
cnf(t671,plain,
mult(X1,a) = rd(sFlat0,rd(a,X1)),
inference(cp,[status(thm)],[t664,t94]) ).
cnf(t758,plain,
rd(sFlat0,rd(a,X1)) = mult(X1,a),
inference(orient,[status(thm)],[t671]) ).
cnf(t759,plain,
mult(mult(X1,a),a) = rd(sFlat0,i(X1)),
inference(cp,[status(thm)],[t758,t208]) ).
cnf(t32511,plain,
mult(a,mult(X1,a)) = rd(sFlat0,i(X1)),
inference(step,[status(thm)],[t759,t49]) ).
cnf(t32512,plain,
mult(a,mult(X1,a)) = mult(sFlat0,X1),
inference(step,[status(thm)],[t32511,t195]) ).
cnf(t842,plain,
mult(a,mult(X1,a)) = mult(sFlat0,X1),
inference(orient,[status(thm)],[t32512]) ).
cnf(t11,axiom,
sFlat1 = mult(mult(a,a),b),
introduced(definition) ).
cnf(t32394,plain,
sFlat1 = mult(b,mult(a,a)),
inference(step,[status(thm)],[t11,t49]) ).
cnf(t79,plain,
mult(b,mult(a,a)) = sFlat1,
inference(orient,[status(thm)],[t32394]) ).
cnf(t32398,plain,
mult(b,sFlat0) = sFlat1,
inference(step,[status(thm)],[t79,t94]) ).
cnf(t101,plain,
mult(b,sFlat0) = sFlat1,
inference(rw,[status(thm)],[t32398]) ).
cnf(t32403,plain,
mult(sFlat0,b) = sFlat1,
inference(step,[status(thm)],[t101,t49]) ).
cnf(t121,plain,
mult(sFlat0,b) = sFlat1,
inference(orient,[status(thm)],[t32403]) ).
cnf(t13,axiom,
sFlat3 = mult(mult(mult(a,a),b),mult(c,mult(a,a))),
introduced(definition) ).
cnf(t32390,plain,
sFlat3 = mult(mult(c,mult(a,a)),mult(mult(a,a),b)),
inference(step,[status(thm)],[t13,t49]) ).
cnf(t32391,plain,
sFlat3 = mult(mult(c,mult(a,a)),mult(b,mult(a,a))),
inference(step,[status(thm)],[t32390,t49]) ).
cnf(t65,plain,
mult(mult(c,mult(a,a)),mult(b,mult(a,a))) = sFlat3,
inference(orient,[status(thm)],[t32391]) ).
cnf(t32395,plain,
mult(mult(c,mult(a,a)),sFlat1) = sFlat3,
inference(step,[status(thm)],[t65,t79]) ).
cnf(t86,plain,
mult(mult(c,mult(a,a)),sFlat1) = sFlat3,
inference(rw,[status(thm)],[t32395]) ).
cnf(t32432,plain,
mult(sFlat1,mult(c,mult(a,a))) = sFlat3,
inference(step,[status(thm)],[t86,t49]) ).
cnf(t32433,plain,
mult(sFlat1,mult(c,sFlat0)) = sFlat3,
inference(step,[status(thm)],[t32432,t94]) ).
cnf(t32434,plain,
mult(sFlat1,mult(sFlat0,c)) = sFlat3,
inference(step,[status(thm)],[t32433,t49]) ).
cnf(t32435,plain,
mult(sFlat1,sFlat2) = sFlat3,
inference(step,[status(thm)],[t32434,t109]) ).
cnf(t325,plain,
mult(sFlat1,sFlat2) = sFlat3,
inference(orient,[status(thm)],[t32435]) ).
cnf(t760,plain,
mult(mult(a,X1),a) = rd(sFlat0,i(X1)),
inference(cp,[status(thm)],[t758,t214]) ).
cnf(t32513,plain,
mult(a,mult(a,X1)) = rd(sFlat0,i(X1)),
inference(step,[status(thm)],[t760,t49]) ).
cnf(t32514,plain,
mult(a,mult(a,X1)) = mult(sFlat0,X1),
inference(step,[status(thm)],[t32513,t195]) ).
cnf(t856,plain,
mult(a,mult(a,X1)) = mult(sFlat0,X1),
inference(orient,[status(thm)],[t32514]) ).
cnf(t98,plain,
mult(a,mult(a,mult(a,mult(a,X1)))) = mult(sFlat0,mult(X1,mult(a,a))),
inference(cp,[status(thm)],[t52,t94]) ).
cnf(t32915,plain,
mult(sFlat0,mult(a,mult(a,X1))) = mult(sFlat0,mult(X1,mult(a,a))),
inference(step,[status(thm)],[t98,t856]) ).
cnf(t32916,plain,
mult(sFlat0,mult(sFlat0,X1)) = mult(sFlat0,mult(X1,mult(a,a))),
inference(step,[status(thm)],[t32915,t856]) ).
cnf(t32917,plain,
mult(sFlat0,mult(sFlat0,X1)) = mult(sFlat0,mult(X1,sFlat0)),
inference(step,[status(thm)],[t32916,t94]) ).
cnf(t176,plain,
i(X1) = ld(X2,rd(X2,X1)),
inference(cp,[status(thm)],[t43,t172]) ).
cnf(t32430,plain,
i(X1) = rd(rd(X2,X1),X2),
inference(step,[status(thm)],[t176,t185]) ).
cnf(t262,plain,
rd(rd(X1,X2),X1) = i(X2),
inference(orient,[status(thm)],[t32430]) ).
cnf(t15,axiom,
sFlat5 = mult(mult(b,c),mult(a,a)),
introduced(definition) ).
cnf(t32396,plain,
sFlat5 = mult(mult(c,b),mult(a,a)),
inference(step,[status(thm)],[t15,t49]) ).
cnf(t87,plain,
mult(mult(c,b),mult(a,a)) = sFlat5,
inference(orient,[status(thm)],[t32396]) ).
cnf(t92,plain,
mult(a,mult(a,mult(a,mult(a,mult(c,b))))) = mult(mult(a,a),sFlat5),
inference(cp,[status(thm)],[t52,t87]) ).
cnf(t16,axiom,
sFlat6 = mult(mult(a,a),mult(mult(b,c),mult(a,a))),
introduced(definition) ).
cnf(t32392,plain,
sFlat6 = mult(a,mult(a,mult(a,mult(a,mult(b,c))))),
inference(step,[status(thm)],[t16,t52]) ).
cnf(t32393,plain,
sFlat6 = mult(a,mult(a,mult(a,mult(a,mult(c,b))))),
inference(step,[status(thm)],[t32392,t49]) ).
cnf(t72,plain,
mult(a,mult(a,mult(a,mult(a,mult(c,b))))) = sFlat6,
inference(orient,[status(thm)],[t32393]) ).
cnf(t32424,plain,
sFlat6 = mult(mult(a,a),sFlat5),
inference(step,[status(thm)],[t92,t72]) ).
cnf(t32425,plain,
sFlat6 = mult(sFlat5,mult(a,a)),
inference(step,[status(thm)],[t32424,t49]) ).
cnf(t32426,plain,
sFlat6 = mult(sFlat5,sFlat0),
inference(step,[status(thm)],[t32425,t94]) ).
cnf(t32427,plain,
sFlat6 = mult(sFlat0,sFlat5),
inference(step,[status(thm)],[t32426,t49]) ).
cnf(t231,plain,
mult(sFlat0,sFlat5) = sFlat6,
inference(orient,[status(thm)],[t32427]) ).
cnf(t233,plain,
i(sFlat0) = rd(sFlat5,sFlat6),
inference(cp,[status(thm)],[t208,t231]) ).
cnf(t242,plain,
rd(sFlat5,sFlat6) = i(sFlat0),
inference(orient,[status(thm)],[t233]) ).
cnf(t266,plain,
i(sFlat6) = rd(i(sFlat0),sFlat5),
inference(cp,[status(thm)],[t262,t242]) ).
cnf(t278,plain,
rd(i(sFlat0),sFlat5) = i(sFlat6),
inference(orient,[status(thm)],[t266]) ).
cnf(t691,plain,
mult(sFlat5,i(sFlat0)) = rd(mult(i(sFlat0),i(sFlat0)),i(sFlat6)),
inference(cp,[status(thm)],[t664,t278]) ).
cnf(t32479,plain,
rd(sFlat5,sFlat0) = rd(mult(i(sFlat0),i(sFlat0)),i(sFlat6)),
inference(step,[status(thm)],[t691,t172]) ).
cnf(t32397,plain,
mult(mult(c,b),sFlat0) = sFlat5,
inference(step,[status(thm)],[t87,t94]) ).
cnf(t100,plain,
mult(mult(c,b),sFlat0) = sFlat5,
inference(rw,[status(thm)],[t32397]) ).
cnf(t32428,plain,
mult(sFlat0,mult(c,b)) = sFlat5,
inference(step,[status(thm)],[t100,t49]) ).
cnf(t14,axiom,
sFlat4 = mult(b,c),
introduced(definition) ).
cnf(t32399,plain,
sFlat4 = mult(c,b),
inference(step,[status(thm)],[t14,t49]) ).
cnf(t102,plain,
mult(c,b) = sFlat4,
inference(orient,[status(thm)],[t32399]) ).
cnf(t32429,plain,
mult(sFlat0,sFlat4) = sFlat5,
inference(step,[status(thm)],[t32428,t102]) ).
cnf(t245,plain,
mult(sFlat0,sFlat4) = sFlat5,
inference(orient,[status(thm)],[t32429]) ).
cnf(t248,plain,
sFlat0 = rd(sFlat5,sFlat4),
inference(cp,[status(thm)],[t37,t245]) ).
cnf(t251,plain,
rd(sFlat5,sFlat4) = sFlat0,
inference(orient,[status(thm)],[t248]) ).
cnf(t253,plain,
sFlat4 = rd(sFlat5,sFlat0),
inference(cp,[status(thm)],[t201,t251]) ).
cnf(t258,plain,
rd(sFlat5,sFlat0) = sFlat4,
inference(orient,[status(thm)],[t253]) ).
cnf(t32480,plain,
sFlat4 = rd(mult(i(sFlat0),i(sFlat0)),i(sFlat6)),
inference(step,[status(thm)],[t32479,t258]) ).
cnf(t32481,plain,
sFlat4 = mult(mult(i(sFlat0),i(sFlat0)),sFlat6),
inference(step,[status(thm)],[t32480,t195]) ).
cnf(t32482,plain,
sFlat4 = mult(sFlat6,mult(i(sFlat0),i(sFlat0))),
inference(step,[status(thm)],[t32481,t49]) ).
cnf(t32483,plain,
sFlat4 = mult(sFlat6,rd(i(sFlat0),sFlat0)),
inference(step,[status(thm)],[t32482,t186]) ).
cnf(t32484,plain,
sFlat4 = rd(sFlat6,rd(sFlat0,i(sFlat0))),
inference(step,[status(thm)],[t32483,t308]) ).
cnf(t32485,plain,
sFlat4 = rd(sFlat6,mult(sFlat0,sFlat0)),
inference(step,[status(thm)],[t32484,t195]) ).
cnf(t728,plain,
rd(sFlat6,mult(sFlat0,sFlat0)) = sFlat4,
inference(orient,[status(thm)],[t32485]) ).
cnf(t735,plain,
mult(sFlat0,sFlat0) = rd(sFlat6,sFlat4),
inference(cp,[status(thm)],[t201,t728]) ).
cnf(t738,plain,
mult(sFlat0,sFlat0) = rd(sFlat6,sFlat4),
inference(orient,[status(thm)],[t735]) ).
cnf(t783,plain,
mult(sFlat0,mult(X1,sFlat0)) = mult(rd(sFlat6,sFlat4),X1),
inference(cp,[status(thm)],[t773,t738]) ).
cnf(t32640,plain,
mult(sFlat0,mult(X1,sFlat0)) = rd(X1,rd(sFlat4,sFlat6)),
inference(step,[status(thm)],[t783,t315]) ).
cnf(t2222,plain,
mult(sFlat0,mult(X1,sFlat0)) = rd(X1,rd(sFlat4,sFlat6)),
inference(orient,[status(thm)],[t32640]) ).
cnf(t32918,plain,
mult(sFlat0,mult(sFlat0,X1)) = rd(X1,rd(sFlat4,sFlat6)),
inference(step,[status(thm)],[t32917,t2222]) ).
cnf(t7646,plain,
mult(sFlat0,mult(sFlat0,X1)) = rd(X1,rd(sFlat4,sFlat6)),
inference(orient,[status(thm)],[t32918]) ).
cnf(t203,plain,
X1 = rd(mult(X2,X1),X2),
inference(cp,[status(thm)],[t201,t37]) ).
cnf(t259,plain,
rd(mult(X1,X2),X1) = X2,
inference(orient,[status(thm)],[t203]) ).
cnf(t331,plain,
mult(sFlat2,mult(sFlat1,mult(sFlat1,mult(sFlat2,X1)))) = mult(sFlat3,mult(X1,mult(sFlat1,sFlat2))),
inference(cp,[status(thm)],[t52,t325]) ).
cnf(t34636,plain,
mult(sFlat2,mult(sFlat1,mult(sFlat1,mult(sFlat2,X1)))) = mult(sFlat3,mult(X1,sFlat3)),
inference(step,[status(thm)],[t331,t325]) ).
cnf(t31732,plain,
mult(sFlat2,mult(sFlat1,mult(sFlat1,mult(sFlat2,X1)))) = mult(sFlat3,mult(X1,sFlat3)),
inference(orient,[status(thm)],[t34636]) ).
cnf(t31767,plain,
mult(sFlat1,mult(sFlat1,mult(sFlat2,X1))) = rd(mult(sFlat3,mult(X1,sFlat3)),sFlat2),
inference(cp,[status(thm)],[t259,t31732]) ).
cnf(t31813,plain,
mult(sFlat1,mult(sFlat1,mult(sFlat2,X1))) = rd(mult(sFlat3,mult(X1,sFlat3)),sFlat2),
inference(orient,[status(thm)],[t31767]) ).
cnf(t31827,plain,
rd(mult(sFlat3,mult(i(X1),sFlat3)),sFlat2) = mult(sFlat1,mult(sFlat1,rd(sFlat2,X1))),
inference(cp,[status(thm)],[t31813,t172]) ).
cnf(t34637,plain,
rd(mult(sFlat3,rd(sFlat3,X1)),sFlat2) = mult(sFlat1,mult(sFlat1,rd(sFlat2,X1))),
inference(step,[status(thm)],[t31827,t186]) ).
cnf(t34638,plain,
rd(rd(sFlat3,rd(X1,sFlat3)),sFlat2) = mult(sFlat1,mult(sFlat1,rd(sFlat2,X1))),
inference(step,[status(thm)],[t34637,t308]) ).
cnf(t34639,plain,
rd(rd(sFlat3,rd(X1,sFlat3)),sFlat2) = mult(sFlat1,rd(sFlat1,rd(X1,sFlat2))),
inference(step,[status(thm)],[t34638,t308]) ).
cnf(t34640,plain,
rd(rd(sFlat3,rd(X1,sFlat3)),sFlat2) = rd(sFlat1,rd(rd(X1,sFlat2),sFlat1)),
inference(step,[status(thm)],[t34639,t308]) ).
cnf(t31903,plain,
rd(rd(sFlat3,rd(X1,sFlat3)),sFlat2) = rd(sFlat1,rd(rd(X1,sFlat2),sFlat1)),
inference(orient,[status(thm)],[t34640]) ).
cnf(t169,plain,
mult(X1,mult(i(X2),mult(i(X2),mult(X1,X3)))) = mult(ld(X2,X1),mult(X3,mult(i(X2),X1))),
inference(cp,[status(thm)],[t52,t163]) ).
cnf(t33873,plain,
mult(X1,rd(mult(i(X2),mult(X1,X3)),X2)) = mult(ld(X2,X1),mult(X3,mult(i(X2),X1))),
inference(step,[status(thm)],[t169,t186]) ).
cnf(t33874,plain,
rd(X1,rd(X2,mult(i(X2),mult(X1,X3)))) = mult(ld(X2,X1),mult(X3,mult(i(X2),X1))),
inference(step,[status(thm)],[t33873,t308]) ).
cnf(t33875,plain,
rd(X1,rd(X2,rd(mult(X1,X3),X2))) = mult(ld(X2,X1),mult(X3,mult(i(X2),X1))),
inference(step,[status(thm)],[t33874,t186]) ).
cnf(t33876,plain,
rd(X1,rd(X2,rd(mult(X1,X3),X2))) = mult(rd(X1,X2),mult(X3,mult(i(X2),X1))),
inference(step,[status(thm)],[t33875,t185]) ).
cnf(t33877,plain,
rd(X1,rd(X2,rd(mult(X1,X3),X2))) = rd(mult(X3,mult(i(X2),X1)),rd(X2,X1)),
inference(step,[status(thm)],[t33876,t315]) ).
cnf(t33878,plain,
rd(X1,rd(X2,rd(mult(X1,X3),X2))) = rd(mult(X3,rd(X1,X2)),rd(X2,X1)),
inference(step,[status(thm)],[t33877,t186]) ).
cnf(t33879,plain,
rd(X1,rd(X2,rd(mult(X1,X3),X2))) = rd(rd(X3,rd(X2,X1)),rd(X2,X1)),
inference(step,[status(thm)],[t33878,t308]) ).
cnf(t779,plain,
mult(i(X1),mult(X2,i(X1))) = mult(rd(i(X1),X1),X2),
inference(cp,[status(thm)],[t773,t172]) ).
cnf(t32518,plain,
rd(mult(X2,i(X1)),X1) = mult(rd(i(X1),X1),X2),
inference(step,[status(thm)],[t779,t186]) ).
cnf(t32519,plain,
rd(rd(X2,X1),X1) = mult(rd(i(X1),X1),X2),
inference(step,[status(thm)],[t32518,t172]) ).
cnf(t32520,plain,
rd(rd(X2,X1),X1) = rd(X2,rd(X1,i(X1))),
inference(step,[status(thm)],[t32519,t315]) ).
cnf(t32521,plain,
rd(rd(X2,X1),X1) = rd(X2,mult(X1,X1)),
inference(step,[status(thm)],[t32520,t195]) ).
cnf(t1020,plain,
rd(rd(X1,X2),X2) = rd(X1,mult(X2,X2)),
inference(orient,[status(thm)],[t32521]) ).
cnf(t33880,plain,
rd(X1,rd(X2,rd(mult(X1,X3),X2))) = rd(X3,mult(rd(X2,X1),rd(X2,X1))),
inference(step,[status(thm)],[t33879,t1020]) ).
cnf(t33881,plain,
rd(X1,rd(X2,rd(mult(X1,X3),X2))) = rd(X3,rd(rd(X2,X1),rd(X1,X2))),
inference(step,[status(thm)],[t33880,t315]) ).
cnf(t56,plain,
mult(X1,mult(X2,mult(X2,mult(X1,unit)))) = mult(mult(X2,X1),mult(X2,X1)),
inference(cp,[status(thm)],[t52,t23]) ).
cnf(t0,axiom,
mult(X1,unit) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t18,plain,
mult(X1,unit) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t32436,plain,
mult(X1,mult(X2,mult(X2,X1))) = mult(mult(X2,X1),mult(X2,X1)),
inference(step,[status(thm)],[t56,t18]) ).
cnf(t360,plain,
mult(mult(X1,X2),mult(X1,X2)) = mult(X2,mult(X1,mult(X1,X2))),
inference(orient,[status(thm)],[t32436]) ).
cnf(t365,plain,
mult(X1,mult(i(X2),mult(i(X2),X1))) = mult(rd(X1,X2),mult(i(X2),X1)),
inference(cp,[status(thm)],[t360,t186]) ).
cnf(t32709,plain,
mult(X1,rd(mult(i(X2),X1),X2)) = mult(rd(X1,X2),mult(i(X2),X1)),
inference(step,[status(thm)],[t365,t186]) ).
cnf(t32710,plain,
rd(X1,rd(X2,mult(i(X2),X1))) = mult(rd(X1,X2),mult(i(X2),X1)),
inference(step,[status(thm)],[t32709,t308]) ).
cnf(t32711,plain,
rd(X1,rd(X2,rd(X1,X2))) = mult(rd(X1,X2),mult(i(X2),X1)),
inference(step,[status(thm)],[t32710,t186]) ).
cnf(t32712,plain,
rd(X1,rd(X2,rd(X1,X2))) = rd(mult(i(X2),X1),rd(X2,X1)),
inference(step,[status(thm)],[t32711,t315]) ).
cnf(t32713,plain,
rd(X1,rd(X2,rd(X1,X2))) = rd(rd(X1,X2),rd(X2,X1)),
inference(step,[status(thm)],[t32712,t186]) ).
cnf(t3684,plain,
rd(rd(X1,X2),rd(X2,X1)) = rd(X1,rd(X2,rd(X1,X2))),
inference(orient,[status(thm)],[t32713]) ).
cnf(t33882,plain,
rd(X1,rd(X2,rd(mult(X1,X3),X2))) = rd(X3,rd(X2,rd(X1,rd(X2,X1)))),
inference(step,[status(thm)],[t33881,t3684]) ).
cnf(t20092,plain,
rd(X1,rd(X2,rd(mult(X1,X3),X2))) = rd(X3,rd(X2,rd(X1,rd(X2,X1)))),
inference(orient,[status(thm)],[t33882]) ).
cnf(t761,plain,
mult(rd(a,X1),a) = rd(sFlat0,X1),
inference(cp,[status(thm)],[t758,t201]) ).
cnf(t32515,plain,
rd(a,rd(X1,a)) = rd(sFlat0,X1),
inference(step,[status(thm)],[t761,t315]) ).
cnf(t869,plain,
rd(a,rd(X1,a)) = rd(sFlat0,X1),
inference(orient,[status(thm)],[t32515]) ).
cnf(t20108,plain,
rd(X1,rd(a,rd(X2,rd(a,X2)))) = rd(X2,rd(sFlat0,mult(X2,X1))),
inference(cp,[status(thm)],[t20092,t869]) ).
cnf(t675,plain,
mult(rd(X1,X2),X1) = rd(mult(X1,X1),X2),
inference(cp,[status(thm)],[t664,t201]) ).
cnf(t32493,plain,
rd(X1,rd(X2,X1)) = rd(mult(X1,X1),X2),
inference(step,[status(thm)],[t675,t315]) ).
cnf(t798,plain,
rd(mult(X1,X1),X2) = rd(X1,rd(X2,X1)),
inference(orient,[status(thm)],[t32493]) ).
cnf(t870,plain,
rd(sFlat0,mult(X1,X1)) = rd(a,rd(X1,rd(a,X1))),
inference(cp,[status(thm)],[t869,t798]) ).
cnf(t6763,plain,
rd(a,rd(X1,rd(a,X1))) = rd(sFlat0,mult(X1,X1)),
inference(orient,[status(thm)],[t870]) ).
cnf(t33883,plain,
rd(X1,rd(sFlat0,mult(X2,X2))) = rd(X2,rd(sFlat0,mult(X2,X1))),
inference(step,[status(thm)],[t20108,t6763]) ).
cnf(t20598,plain,
rd(X1,rd(sFlat0,mult(X2,X2))) = rd(X2,rd(sFlat0,mult(X2,X1))),
inference(orient,[status(thm)],[t33883]) ).
cnf(t309,plain,
rd(i(X1),rd(X2,X3)) = rd(rd(X3,X2),X1),
inference(cp,[status(thm)],[t308,t186]) ).
cnf(t351,plain,
rd(i(X1),rd(X2,X3)) = rd(rd(X3,X2),X1),
inference(orient,[status(thm)],[t309]) ).
cnf(t20610,plain,
rd(X1,rd(sFlat0,mult(X1,i(X2)))) = rd(rd(mult(X1,X1),sFlat0),X2),
inference(cp,[status(thm)],[t20598,t351]) ).
cnf(t33884,plain,
rd(X1,rd(sFlat0,rd(X1,X2))) = rd(rd(mult(X1,X1),sFlat0),X2),
inference(step,[status(thm)],[t20610,t172]) ).
cnf(t33885,plain,
rd(X1,rd(sFlat0,rd(X1,X2))) = rd(rd(X1,rd(sFlat0,X1)),X2),
inference(step,[status(thm)],[t33884,t798]) ).
cnf(t20712,plain,
rd(rd(X1,rd(sFlat0,X1)),X2) = rd(X1,rd(sFlat0,rd(X1,X2))),
inference(orient,[status(thm)],[t33885]) ).
cnf(t31904,plain,
rd(sFlat1,rd(rd(sFlat0,sFlat2),sFlat1)) = rd(sFlat3,rd(sFlat0,rd(sFlat3,sFlat2))),
inference(cp,[status(thm)],[t31903,t20712]) ).
cnf(t217,plain,
i(c) = rd(sFlat0,sFlat2),
inference(cp,[status(thm)],[t214,t109]) ).
cnf(t221,plain,
rd(sFlat0,sFlat2) = i(c),
inference(orient,[status(thm)],[t217]) ).
cnf(t34641,plain,
rd(sFlat1,rd(i(c),sFlat1)) = rd(sFlat3,rd(sFlat0,rd(sFlat3,sFlat2))),
inference(step,[status(thm)],[t31904,t221]) ).
cnf(t173,plain,
rd(i(X1),X2) = ld(X1,i(X2)),
inference(cp,[status(thm)],[t172,t163]) ).
cnf(t32431,plain,
rd(i(X1),X2) = rd(i(X2),X1),
inference(step,[status(thm)],[t173,t185]) ).
cnf(t286,plain,
rd(i(X1),X2) = rd(i(X2),X1),
inference(orient,[status(thm)],[t32431]) ).
cnf(t34642,plain,
rd(sFlat1,rd(i(sFlat1),c)) = rd(sFlat3,rd(sFlat0,rd(sFlat3,sFlat2))),
inference(step,[status(thm)],[t34641,t286]) ).
cnf(t310,plain,
rd(X1,rd(i(X2),X3)) = mult(X1,mult(X3,X2)),
inference(cp,[status(thm)],[t308,t195]) ).
cnf(t355,plain,
rd(X1,rd(i(X2),X3)) = mult(X1,mult(X3,X2)),
inference(orient,[status(thm)],[t310]) ).
cnf(t34643,plain,
mult(sFlat1,mult(c,sFlat1)) = rd(sFlat3,rd(sFlat0,rd(sFlat3,sFlat2))),
inference(step,[status(thm)],[t34642,t355]) ).
cnf(t34644,plain,
mult(sFlat1,mult(sFlat1,c)) = rd(sFlat3,rd(sFlat0,rd(sFlat3,sFlat2))),
inference(step,[status(thm)],[t34643,t49]) ).
cnf(t125,plain,
mult(b,mult(sFlat0,mult(sFlat0,mult(b,X1)))) = mult(sFlat1,mult(X1,mult(sFlat0,b))),
inference(cp,[status(thm)],[t52,t121]) ).
cnf(t33550,plain,
mult(b,rd(mult(b,X1),rd(sFlat4,sFlat6))) = mult(sFlat1,mult(X1,mult(sFlat0,b))),
inference(step,[status(thm)],[t125,t7646]) ).
cnf(t33551,plain,
rd(b,rd(rd(sFlat4,sFlat6),mult(b,X1))) = mult(sFlat1,mult(X1,mult(sFlat0,b))),
inference(step,[status(thm)],[t33550,t308]) ).
cnf(t33552,plain,
rd(b,rd(rd(sFlat4,sFlat6),mult(b,X1))) = mult(sFlat1,mult(X1,sFlat1)),
inference(step,[status(thm)],[t33551,t121]) ).
cnf(t15450,plain,
rd(b,rd(rd(sFlat4,sFlat6),mult(b,X1))) = mult(sFlat1,mult(X1,sFlat1)),
inference(orient,[status(thm)],[t33552]) ).
cnf(t15483,plain,
rd(rd(sFlat4,sFlat6),mult(b,X1)) = rd(b,mult(sFlat1,mult(X1,sFlat1))),
inference(cp,[status(thm)],[t201,t15450]) ).
cnf(t15749,plain,
rd(rd(sFlat4,sFlat6),mult(b,X1)) = rd(b,mult(sFlat1,mult(X1,sFlat1))),
inference(orient,[status(thm)],[t15483]) ).
cnf(t15759,plain,
rd(b,mult(sFlat1,mult(X1,sFlat1))) = rd(rd(sFlat4,sFlat6),mult(X1,b)),
inference(cp,[status(thm)],[t15749,t49]) ).
cnf(t16881,plain,
rd(rd(sFlat4,sFlat6),mult(X1,b)) = rd(b,mult(sFlat1,mult(X1,sFlat1))),
inference(orient,[status(thm)],[t15759]) ).
cnf(t16887,plain,
rd(b,mult(sFlat1,mult(c,sFlat1))) = rd(rd(sFlat4,sFlat6),sFlat4),
inference(cp,[status(thm)],[t16881,t102]) ).
cnf(t33671,plain,
rd(b,mult(sFlat1,mult(sFlat1,c))) = rd(rd(sFlat4,sFlat6),sFlat4),
inference(step,[status(thm)],[t16887,t49]) ).
cnf(t33672,plain,
rd(b,mult(sFlat1,mult(sFlat1,c))) = i(sFlat6),
inference(step,[status(thm)],[t33671,t262]) ).
cnf(t16902,plain,
rd(b,mult(sFlat1,mult(sFlat1,c))) = i(sFlat6),
inference(orient,[status(thm)],[t33672]) ).
cnf(t16912,plain,
mult(sFlat1,mult(sFlat1,c)) = rd(b,i(sFlat6)),
inference(cp,[status(thm)],[t201,t16902]) ).
cnf(t33673,plain,
mult(sFlat1,mult(sFlat1,c)) = mult(b,sFlat6),
inference(step,[status(thm)],[t16912,t195]) ).
cnf(t33674,plain,
mult(sFlat1,mult(sFlat1,c)) = mult(sFlat6,b),
inference(step,[status(thm)],[t33673,t49]) ).
cnf(t16916,plain,
mult(sFlat1,mult(sFlat1,c)) = mult(sFlat6,b),
inference(orient,[status(thm)],[t33674]) ).
cnf(t34645,plain,
mult(sFlat6,b) = rd(sFlat3,rd(sFlat0,rd(sFlat3,sFlat2))),
inference(step,[status(thm)],[t34644,t16916]) ).
cnf(t330,plain,
sFlat1 = rd(sFlat3,sFlat2),
inference(cp,[status(thm)],[t37,t325]) ).
cnf(t333,plain,
rd(sFlat3,sFlat2) = sFlat1,
inference(orient,[status(thm)],[t330]) ).
cnf(t34646,plain,
mult(sFlat6,b) = rd(sFlat3,rd(sFlat0,sFlat1)),
inference(step,[status(thm)],[t34645,t333]) ).
cnf(t218,plain,
i(b) = rd(sFlat0,sFlat1),
inference(cp,[status(thm)],[t214,t121]) ).
cnf(t222,plain,
rd(sFlat0,sFlat1) = i(b),
inference(orient,[status(thm)],[t218]) ).
cnf(t34647,plain,
mult(sFlat6,b) = rd(sFlat3,i(b)),
inference(step,[status(thm)],[t34646,t222]) ).
cnf(t34648,plain,
mult(sFlat6,b) = mult(sFlat3,b),
inference(step,[status(thm)],[t34647,t195]) ).
cnf(t31962,plain,
mult(sFlat6,b) = mult(sFlat3,b),
inference(orient,[status(thm)],[t34648]) ).
cnf(t31984,plain,
sFlat6 = rd(mult(sFlat3,b),b),
inference(cp,[status(thm)],[t37,t31962]) ).
cnf(t34668,plain,
sFlat6 = sFlat3,
inference(step,[status(thm)],[t31984,t37]) ).
cnf(t32029,plain,
sFlat6 = sFlat3,
inference(orient,[status(thm)],[t34668]) ).
cnf(t34727,plain,
mult(sFlat0,mult(sFlat0,X1)) = rd(X1,rd(sFlat4,sFlat3)),
inference(step,[status(thm)],[t7646,t32029]) ).
cnf(t32078,plain,
mult(sFlat0,mult(sFlat0,X1)) = rd(X1,rd(sFlat4,sFlat3)),
inference(orient,[status(thm)],[t34727]) ).
cnf(goal_0,negated_conjecture,
mult(mult(mult(a,a),b),mult(c,mult(a,a))) != mult(mult(a,a),mult(mult(b,c),mult(a,a))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
mult(mult(c,mult(a,a)),mult(mult(a,a),b)) != mult(mult(a,a),mult(mult(b,c),mult(a,a))),
inference(rw,[status(thm)],[goal_0,t49]) ).
cnf(g0_1,plain,
mult(mult(c,sFlat0),mult(mult(a,a),b)) != mult(mult(a,a),mult(mult(b,c),mult(a,a))),
inference(rw,[status(thm)],[g0_0,t94]) ).
cnf(g0_2,plain,
mult(mult(sFlat0,c),mult(mult(a,a),b)) != mult(mult(a,a),mult(mult(b,c),mult(a,a))),
inference(rw,[status(thm)],[g0_1,t49]) ).
cnf(g0_3,plain,
mult(sFlat2,mult(mult(a,a),b)) != mult(mult(a,a),mult(mult(b,c),mult(a,a))),
inference(rw,[status(thm)],[g0_2,t109]) ).
cnf(g0_4,plain,
mult(sFlat2,mult(a,mult(b,a))) != mult(mult(a,a),mult(mult(b,c),mult(a,a))),
inference(rw,[status(thm)],[g0_3,t773]) ).
cnf(g0_5,plain,
mult(sFlat2,mult(sFlat0,b)) != mult(mult(a,a),mult(mult(b,c),mult(a,a))),
inference(rw,[status(thm)],[g0_4,t842]) ).
cnf(g0_6,plain,
mult(sFlat2,sFlat1) != mult(mult(a,a),mult(mult(b,c),mult(a,a))),
inference(rw,[status(thm)],[g0_5,t121]) ).
cnf(g0_7,plain,
mult(sFlat1,sFlat2) != mult(mult(a,a),mult(mult(b,c),mult(a,a))),
inference(rw,[status(thm)],[g0_6,t49]) ).
cnf(g0_8,plain,
sFlat3 != mult(mult(a,a),mult(mult(b,c),mult(a,a))),
inference(rw,[status(thm)],[g0_7,t325]) ).
cnf(g0_9,plain,
sFlat3 != mult(a,mult(a,mult(a,mult(a,mult(b,c))))),
inference(rw,[status(thm)],[g0_8,t52]) ).
cnf(g0_10,plain,
sFlat3 != mult(sFlat0,mult(a,mult(a,mult(b,c)))),
inference(rw,[status(thm)],[g0_9,t856]) ).
cnf(g0_11,plain,
sFlat3 != mult(sFlat0,mult(sFlat0,mult(b,c))),
inference(rw,[status(thm)],[g0_10,t856]) ).
cnf(g0_12,plain,
sFlat3 != rd(mult(b,c),rd(sFlat4,sFlat3)),
inference(rw,[status(thm)],[g0_11,t32078]) ).
cnf(g0_13,plain,
sFlat3 != rd(mult(c,b),rd(sFlat4,sFlat3)),
inference(rw,[status(thm)],[g0_12,t49]) ).
cnf(g0_14,plain,
sFlat3 != rd(sFlat4,rd(sFlat4,sFlat3)),
inference(rw,[status(thm)],[g0_13,t102]) ).
cnf(g0_15,plain,
sFlat3 != sFlat3,
inference(rw,[status(thm)],[g0_14,t201]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_15]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP718-1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.08/5.36 % Computer : n010.cluster.edu
% 0.08/5.36 % Model : x86_64 x86_64
% 0.08/5.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/5.36 % Memory : 8046.5625MB
% 0.08/5.36 % OS : Linux 6.8.0-71-generic
% 0.08/5.36 % CPULimit : 300
% 0.08/5.36 % WCLimit : 300
% 0.08/5.36 % DateTime : Wed Sep 23 15:50:17 UTC 2026
% 0.08/5.36 % CPUTime :
% 0.08/5.36 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 57.95/13.04 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 57.95/13.04 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------