%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP696-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 : n017.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:04 PM UTC 2026
% Result : Unsatisfiable 14.53s 12.53s
% Output : CNFRefutation 14.53s
% Verified :
% SZS Type : Refutation
% Derivation depth : 39
% Number of leaves : 17
% Syntax : Number of clauses : 145 ( 145 unt; 0 nHn; 100 RR)
% Number of literals : 145 ( 144 equ; 9 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 16 ( 16 usr; 12 con; 0-2 aty)
% Number of variables : 81 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t11,axiom,
sFlat0 = mult(a,b),
introduced(definition) ).
cnf(t125,plain,
mult(a,b) = sFlat0,
inference(orient,[status(thm)],[t11]) ).
cnf(t12,axiom,
sFlat1 = mult(mult(a,b),a),
introduced(definition) ).
cnf(t99,plain,
mult(mult(a,b),a) = sFlat1,
inference(orient,[status(thm)],[t12]) ).
cnf(t3355,plain,
mult(sFlat0,a) = sFlat1,
inference(step,[status(thm)],[t99,t125]) ).
cnf(t133,plain,
mult(sFlat0,a) = sFlat1,
inference(rw,[status(thm)],[t3355]) ).
cnf(t176,plain,
mult(sFlat0,a) = sFlat1,
inference(orient,[status(thm)],[t133]) ).
cnf(t13,axiom,
sFlat2 = mult(a,c),
introduced(definition) ).
cnf(t134,plain,
mult(a,c) = sFlat2,
inference(orient,[status(thm)],[t13]) ).
cnf(t14,axiom,
sFlat3 = mult(mult(mult(a,b),a),mult(a,c)),
introduced(definition) ).
cnf(t83,plain,
mult(mult(mult(a,b),a),mult(a,c)) = sFlat3,
inference(orient,[status(thm)],[t14]) ).
cnf(t3352,plain,
mult(sFlat1,mult(a,c)) = sFlat3,
inference(step,[status(thm)],[t83,t99]) ).
cnf(t107,plain,
mult(sFlat1,mult(a,c)) = sFlat3,
inference(rw,[status(thm)],[t3352]) ).
cnf(t3366,plain,
mult(sFlat1,sFlat2) = sFlat3,
inference(step,[status(thm)],[t107,t134]) ).
cnf(t350,plain,
mult(sFlat1,sFlat2) = sFlat3,
inference(orient,[status(thm)],[t3366]) ).
cnf(t15,axiom,
sFlat4 = mult(b,a),
introduced(definition) ).
cnf(t142,plain,
mult(b,a) = sFlat4,
inference(orient,[status(thm)],[t15]) ).
cnf(t16,axiom,
sFlat5 = mult(mult(b,a),a),
introduced(definition) ).
cnf(t108,plain,
mult(mult(b,a),a) = sFlat5,
inference(orient,[status(thm)],[t16]) ).
cnf(t3356,plain,
mult(sFlat4,a) = sFlat5,
inference(step,[status(thm)],[t108,t142]) ).
cnf(t150,plain,
mult(sFlat4,a) = sFlat5,
inference(rw,[status(thm)],[t3356]) ).
cnf(t188,plain,
mult(sFlat4,a) = sFlat5,
inference(orient,[status(thm)],[t150]) ).
cnf(t17,axiom,
sFlat6 = mult(mult(mult(b,a),a),c),
introduced(definition) ).
cnf(t91,plain,
mult(mult(mult(b,a),a),c) = sFlat6,
inference(orient,[status(thm)],[t17]) ).
cnf(t3353,plain,
mult(sFlat5,c) = sFlat6,
inference(step,[status(thm)],[t91,t108]) ).
cnf(t116,plain,
mult(sFlat5,c) = sFlat6,
inference(rw,[status(thm)],[t3353]) ).
cnf(t165,plain,
mult(sFlat5,c) = sFlat6,
inference(orient,[status(thm)],[t116]) ).
cnf(t18,axiom,
sFlat7 = mult(a,mult(mult(mult(b,a),a),c)),
introduced(definition) ).
cnf(t3354,plain,
sFlat7 = mult(a,mult(sFlat5,c)),
inference(step,[status(thm)],[t18,t108]) ).
cnf(t117,plain,
mult(a,mult(sFlat5,c)) = sFlat7,
inference(orient,[status(thm)],[t3354]) ).
cnf(t3357,plain,
mult(a,sFlat6) = sFlat7,
inference(step,[status(thm)],[t117,t165]) ).
cnf(t173,plain,
mult(a,sFlat6) = sFlat7,
inference(rw,[status(thm)],[t3357]) ).
cnf(t198,plain,
mult(a,sFlat6) = sFlat7,
inference(orient,[status(thm)],[t173]) ).
cnf(t7,axiom,
rd(mult(X1,X2),X2) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t25,plain,
rd(mult(X1,X2),X2) = X1,
inference(orient,[status(thm)],[t7]) ).
cnf(t2,axiom,
mult(X1,i(X1)) = unit,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t45,plain,
mult(X1,i(X1)) = unit,
inference(orient,[status(thm)],[t2]) ).
cnf(t48,plain,
X1 = rd(unit,i(X1)),
inference(cp,[status(thm)],[t25,t45]) ).
cnf(t3,axiom,
mult(i(X1),X1) = unit,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t151,plain,
mult(i(X1),X1) = unit,
inference(orient,[status(thm)],[t3]) ).
cnf(t154,plain,
i(X1) = rd(unit,X1),
inference(cp,[status(thm)],[t25,t151]) ).
cnf(t213,plain,
rd(unit,X1) = i(X1),
inference(orient,[status(thm)],[t154]) ).
cnf(t3358,plain,
X1 = i(i(X1)),
inference(step,[status(thm)],[t48,t213]) ).
cnf(t214,plain,
i(i(X1)) = X1,
inference(orient,[status(thm)],[t3358]) ).
cnf(t9,axiom,
mult(mult(X1,X2),ld(X2,mult(X3,X2))) = mult(mult(X1,X3),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t62,plain,
mult(mult(X1,X2),ld(X2,mult(X3,X2))) = mult(mult(X1,X3),X2),
inference(orient,[status(thm)],[t9]) ).
cnf(t157,plain,
mult(mult(i(X1),X2),X1) = mult(unit,ld(X1,mult(X2,X1))),
inference(cp,[status(thm)],[t62,t151]) ).
cnf(t1,axiom,
mult(unit,X1) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t21,plain,
mult(unit,X1) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t3372,plain,
mult(mult(i(X1),X2),X1) = ld(X1,mult(X2,X1)),
inference(step,[status(thm)],[t157,t21]) ).
cnf(t549,plain,
mult(mult(i(X1),X2),X1) = ld(X1,mult(X2,X1)),
inference(orient,[status(thm)],[t3372]) ).
cnf(t8,axiom,
mult(X1,i(mult(X2,X1))) = i(X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t51,plain,
mult(X1,i(mult(X2,X1))) = i(X2),
inference(orient,[status(thm)],[t8]) ).
cnf(t6,axiom,
mult(rd(X1,X2),X2) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t23,plain,
mult(rd(X1,X2),X2) = X1,
inference(orient,[status(thm)],[t6]) ).
cnf(t54,plain,
i(rd(X1,X2)) = mult(X2,i(X1)),
inference(cp,[status(thm)],[t51,t23]) ).
cnf(t396,plain,
i(rd(X1,X2)) = mult(X2,i(X1)),
inference(orient,[status(thm)],[t54]) ).
cnf(t398,plain,
rd(X1,X2) = i(mult(X2,i(X1))),
inference(cp,[status(thm)],[t214,t396]) ).
cnf(t4,axiom,
ld(X1,mult(X1,X2)) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t29,plain,
ld(X1,mult(X1,X2)) = X2,
inference(orient,[status(thm)],[t4]) ).
cnf(t57,plain,
i(mult(X1,X2)) = ld(X2,i(X1)),
inference(cp,[status(thm)],[t29,t51]) ).
cnf(t401,plain,
i(mult(X1,X2)) = ld(X2,i(X1)),
inference(orient,[status(thm)],[t57]) ).
cnf(t3368,plain,
rd(X1,X2) = ld(i(X1),i(X2)),
inference(step,[status(thm)],[t398,t401]) ).
cnf(t408,plain,
ld(i(X1),i(X2)) = rd(X1,X2),
inference(orient,[status(thm)],[t3368]) ).
cnf(t411,plain,
rd(i(X1),X2) = ld(X1,i(X2)),
inference(cp,[status(thm)],[t408,t214]) ).
cnf(t417,plain,
ld(X1,i(X2)) = rd(i(X1),X2),
inference(orient,[status(thm)],[t411]) ).
cnf(t422,plain,
rd(i(X1),i(X2)) = ld(X1,X2),
inference(cp,[status(thm)],[t417,t214]) ).
cnf(t488,plain,
rd(i(X1),i(X2)) = ld(X1,X2),
inference(orient,[status(thm)],[t422]) ).
cnf(t495,plain,
mult(i(X1),i(i(X2))) = i(ld(X2,X1)),
inference(cp,[status(thm)],[t396,t488]) ).
cnf(t3371,plain,
mult(i(X1),X2) = i(ld(X2,X1)),
inference(step,[status(thm)],[t495,t214]) ).
cnf(t504,plain,
i(ld(X1,X2)) = mult(i(X2),X1),
inference(orient,[status(thm)],[t3371]) ).
cnf(t76,plain,
ld(X1,mult(X2,X1)) = ld(mult(X3,X1),mult(mult(X3,X2),X1)),
inference(cp,[status(thm)],[t29,t62]) ).
cnf(t2129,plain,
ld(mult(X1,X2),mult(mult(X1,X3),X2)) = ld(X2,mult(X3,X2)),
inference(orient,[status(thm)],[t76]) ).
cnf(t2236,plain,
ld(X1,mult(i(X2),X1)) = ld(mult(X2,X1),mult(unit,X1)),
inference(cp,[status(thm)],[t2129,t45]) ).
cnf(t3526,plain,
ld(X1,mult(i(X2),X1)) = ld(mult(X2,X1),X1),
inference(step,[status(thm)],[t2236,t21]) ).
cnf(t2348,plain,
ld(X1,mult(i(X2),X1)) = ld(mult(X2,X1),X1),
inference(orient,[status(thm)],[t3526]) ).
cnf(t132,plain,
i(a) = mult(b,i(sFlat0)),
inference(cp,[status(thm)],[t51,t125]) ).
cnf(t215,plain,
mult(b,i(sFlat0)) = i(a),
inference(orient,[status(thm)],[t132]) ).
cnf(t222,plain,
i(b) = mult(i(sFlat0),i(i(a))),
inference(cp,[status(thm)],[t51,t215]) ).
cnf(t3359,plain,
i(b) = mult(i(sFlat0),a),
inference(step,[status(thm)],[t222,t214]) ).
cnf(t274,plain,
mult(i(sFlat0),a) = i(b),
inference(orient,[status(thm)],[t3359]) ).
cnf(t2367,plain,
ld(mult(sFlat0,a),a) = ld(a,i(b)),
inference(cp,[status(thm)],[t2348,t274]) ).
cnf(t3527,plain,
ld(sFlat1,a) = ld(a,i(b)),
inference(step,[status(thm)],[t2367,t176]) ).
cnf(t149,plain,
i(b) = mult(a,i(sFlat4)),
inference(cp,[status(thm)],[t51,t142]) ).
cnf(t231,plain,
mult(a,i(sFlat4)) = i(b),
inference(orient,[status(thm)],[t149]) ).
cnf(t232,plain,
i(sFlat4) = ld(a,i(b)),
inference(cp,[status(thm)],[t29,t231]) ).
cnf(t290,plain,
ld(a,i(b)) = i(sFlat4),
inference(orient,[status(thm)],[t232]) ).
cnf(t3528,plain,
ld(sFlat1,a) = i(sFlat4),
inference(step,[status(thm)],[t3527,t290]) ).
cnf(t2381,plain,
ld(sFlat1,a) = i(sFlat4),
inference(orient,[status(thm)],[t3528]) ).
cnf(t2386,plain,
mult(i(a),sFlat1) = i(i(sFlat4)),
inference(cp,[status(thm)],[t504,t2381]) ).
cnf(t3533,plain,
mult(i(a),sFlat1) = sFlat4,
inference(step,[status(thm)],[t2386,t214]) ).
cnf(t2408,plain,
mult(i(a),sFlat1) = sFlat4,
inference(orient,[status(thm)],[t3533]) ).
cnf(t2419,plain,
ld(a,mult(sFlat1,a)) = mult(sFlat4,a),
inference(cp,[status(thm)],[t549,t2408]) ).
cnf(t3538,plain,
ld(a,mult(sFlat1,a)) = sFlat5,
inference(step,[status(thm)],[t2419,t188]) ).
cnf(t2438,plain,
ld(a,mult(sFlat1,a)) = sFlat5,
inference(orient,[status(thm)],[t3538]) ).
cnf(t2443,plain,
mult(mult(X1,sFlat1),a) = mult(mult(X1,a),sFlat5),
inference(cp,[status(thm)],[t62,t2438]) ).
cnf(t3070,plain,
mult(mult(X1,a),sFlat5) = mult(mult(X1,sFlat1),a),
inference(orient,[status(thm)],[t2443]) ).
cnf(t205,plain,
i(a) = mult(sFlat6,i(sFlat7)),
inference(cp,[status(thm)],[t51,t198]) ).
cnf(t264,plain,
mult(sFlat6,i(sFlat7)) = i(a),
inference(orient,[status(thm)],[t205]) ).
cnf(t271,plain,
i(sFlat6) = mult(i(sFlat7),i(i(a))),
inference(cp,[status(thm)],[t51,t264]) ).
cnf(t3365,plain,
i(sFlat6) = mult(i(sFlat7),a),
inference(step,[status(thm)],[t271,t214]) ).
cnf(t328,plain,
mult(i(sFlat7),a) = i(sFlat6),
inference(orient,[status(thm)],[t3365]) ).
cnf(t3079,plain,
mult(mult(i(sFlat7),sFlat1),a) = mult(i(sFlat6),sFlat5),
inference(cp,[status(thm)],[t3070,t328]) ).
cnf(t172,plain,
i(sFlat5) = mult(c,i(sFlat6)),
inference(cp,[status(thm)],[t51,t165]) ).
cnf(t239,plain,
mult(c,i(sFlat6)) = i(sFlat5),
inference(orient,[status(thm)],[t172]) ).
cnf(t246,plain,
i(c) = mult(i(sFlat6),i(i(sFlat5))),
inference(cp,[status(thm)],[t51,t239]) ).
cnf(t3362,plain,
i(c) = mult(i(sFlat6),sFlat5),
inference(step,[status(thm)],[t246,t214]) ).
cnf(t301,plain,
mult(i(sFlat6),sFlat5) = i(c),
inference(orient,[status(thm)],[t3362]) ).
cnf(t3593,plain,
mult(mult(i(sFlat7),sFlat1),a) = i(c),
inference(step,[status(thm)],[t3079,t301]) ).
cnf(t3268,plain,
mult(mult(i(sFlat7),sFlat1),a) = i(c),
inference(orient,[status(thm)],[t3593]) ).
cnf(t3274,plain,
mult(i(sFlat7),sFlat1) = rd(i(c),a),
inference(cp,[status(thm)],[t25,t3268]) ).
cnf(t141,plain,
i(a) = mult(c,i(sFlat2)),
inference(cp,[status(thm)],[t51,t134]) ).
cnf(t223,plain,
mult(c,i(sFlat2)) = i(a),
inference(orient,[status(thm)],[t141]) ).
cnf(t230,plain,
i(c) = mult(i(sFlat2),i(i(a))),
inference(cp,[status(thm)],[t51,t223]) ).
cnf(t3360,plain,
i(c) = mult(i(sFlat2),a),
inference(step,[status(thm)],[t230,t214]) ).
cnf(t283,plain,
mult(i(sFlat2),a) = i(c),
inference(orient,[status(thm)],[t3360]) ).
cnf(t285,plain,
i(sFlat2) = rd(i(c),a),
inference(cp,[status(thm)],[t25,t283]) ).
cnf(t336,plain,
rd(i(c),a) = i(sFlat2),
inference(orient,[status(thm)],[t285]) ).
cnf(t3594,plain,
mult(i(sFlat7),sFlat1) = i(sFlat2),
inference(step,[status(thm)],[t3274,t336]) ).
cnf(t3281,plain,
mult(i(sFlat7),sFlat1) = i(sFlat2),
inference(orient,[status(thm)],[t3594]) ).
cnf(t3286,plain,
i(sFlat7) = rd(i(sFlat2),sFlat1),
inference(cp,[status(thm)],[t25,t3281]) ).
cnf(t357,plain,
i(sFlat1) = mult(sFlat2,i(sFlat3)),
inference(cp,[status(thm)],[t51,t350]) ).
cnf(t361,plain,
mult(sFlat2,i(sFlat3)) = i(sFlat1),
inference(orient,[status(thm)],[t357]) ).
cnf(t368,plain,
i(sFlat2) = mult(i(sFlat3),i(i(sFlat1))),
inference(cp,[status(thm)],[t51,t361]) ).
cnf(t3367,plain,
i(sFlat2) = mult(i(sFlat3),sFlat1),
inference(step,[status(thm)],[t368,t214]) ).
cnf(t371,plain,
mult(i(sFlat3),sFlat1) = i(sFlat2),
inference(orient,[status(thm)],[t3367]) ).
cnf(t373,plain,
i(sFlat3) = rd(i(sFlat2),sFlat1),
inference(cp,[status(thm)],[t25,t371]) ).
cnf(t378,plain,
rd(i(sFlat2),sFlat1) = i(sFlat3),
inference(orient,[status(thm)],[t373]) ).
cnf(t3595,plain,
i(sFlat7) = i(sFlat3),
inference(step,[status(thm)],[t3286,t378]) ).
cnf(t3295,plain,
i(sFlat7) = i(sFlat3),
inference(orient,[status(thm)],[t3595]) ).
cnf(t3315,plain,
sFlat7 = i(i(sFlat3)),
inference(cp,[status(thm)],[t214,t3295]) ).
cnf(t3611,plain,
sFlat7 = sFlat3,
inference(step,[status(thm)],[t3315,t214]) ).
cnf(t3334,plain,
sFlat7 = sFlat3,
inference(orient,[status(thm)],[t3611]) ).
cnf(t3612,plain,
mult(a,sFlat6) = sFlat3,
inference(step,[status(thm)],[t198,t3334]) ).
cnf(t3335,plain,
mult(a,sFlat6) = sFlat3,
inference(orient,[status(thm)],[t3612]) ).
cnf(goal_0,negated_conjecture,
mult(mult(mult(a,b),a),mult(a,c)) != mult(a,mult(mult(mult(b,a),a),c)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
mult(mult(sFlat0,a),mult(a,c)) != mult(a,mult(mult(mult(b,a),a),c)),
inference(rw,[status(thm)],[goal_0,t125]) ).
cnf(g0_1,plain,
mult(sFlat1,mult(a,c)) != mult(a,mult(mult(mult(b,a),a),c)),
inference(rw,[status(thm)],[g0_0,t176]) ).
cnf(g0_2,plain,
mult(sFlat1,sFlat2) != mult(a,mult(mult(mult(b,a),a),c)),
inference(rw,[status(thm)],[g0_1,t134]) ).
cnf(g0_3,plain,
sFlat3 != mult(a,mult(mult(mult(b,a),a),c)),
inference(rw,[status(thm)],[g0_2,t350]) ).
cnf(g0_4,plain,
sFlat3 != mult(a,mult(mult(sFlat4,a),c)),
inference(rw,[status(thm)],[g0_3,t142]) ).
cnf(g0_5,plain,
sFlat3 != mult(a,mult(sFlat5,c)),
inference(rw,[status(thm)],[g0_4,t188]) ).
cnf(g0_6,plain,
sFlat3 != mult(a,sFlat6),
inference(rw,[status(thm)],[g0_5,t165]) ).
cnf(g0_7,plain,
sFlat3 != sFlat3,
inference(rw,[status(thm)],[g0_6,t3335]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_7]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : GRP696-1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.13/10.61 % Computer : n017.cluster.edu
% 0.13/10.61 % Model : x86_64 x86_64
% 0.13/10.61 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/10.61 % Memory : 8046.5625MB
% 0.13/10.61 % OS : Linux 6.8.0-71-generic
% 0.13/10.61 % CPULimit : 300
% 0.13/10.61 % WCLimit : 300
% 0.13/10.61 % DateTime : Wed Sep 23 15:39:11 UTC 2026
% 0.13/10.61 % CPUTime :
% 0.13/10.61 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 14.53/12.53 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 14.53/12.53 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------