%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : ALG003-1 : TPTP v9.3.1. Bugfixed v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n011.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 12:51:09 PM UTC 2026
% Result : Unsatisfiable 18.07s 2.78s
% Output : Proof 18.07s
% Verified :
% SZS Type : Refutation
% Derivation depth : 38
% Number of leaves : 15
% Syntax : Number of formulae : 127 ( 123 unt; 0 def)
% Number of atoms : 135 ( 134 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 32 ( 24 ~; 8 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 1 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 19 ( 19 usr; 17 con; 0-4 aty)
% Number of variables : 127 ( 2 sgn 16 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(t5,axiom,
sFlat0 = multiply(d,c),
introduced(definition) ).
cnf(t85,plain,
multiply(d,c) = sFlat0,
inference(orient,[status(thm)],[t5]) ).
cnf(t6,axiom,
sFlat1 = multiply(a,multiply(d,c)),
introduced(definition) ).
cnf(t15782,plain,
sFlat1 = multiply(a,sFlat0),
inference(step,[status(thm)],[t6,t85]) ).
cnf(t100,plain,
multiply(a,sFlat0) = sFlat1,
inference(orient,[status(thm)],[t15782]) ).
cnf(t7,axiom,
sFlat2 = multiply(b,e),
introduced(definition) ).
cnf(t61,plain,
multiply(b,e) = sFlat2,
inference(orient,[status(thm)],[t7]) ).
cnf(t8,axiom,
sFlat3 = multiply(multiply(b,e),f),
introduced(definition) ).
cnf(t33,plain,
multiply(multiply(b,e),f) = sFlat3,
inference(orient,[status(thm)],[t8]) ).
cnf(t15777,plain,
multiply(sFlat2,f) = sFlat3,
inference(step,[status(thm)],[t33,t61]) ).
cnf(t68,plain,
multiply(sFlat2,f) = sFlat3,
inference(rw,[status(thm)],[t15777]) ).
cnf(t114,plain,
multiply(sFlat2,f) = sFlat3,
inference(orient,[status(thm)],[t68]) ).
cnf(t9,axiom,
sFlat4 = multiply(multiply(a,multiply(d,c)),multiply(multiply(b,e),f)),
introduced(definition) ).
cnf(t15776,plain,
sFlat4 = multiply(multiply(a,multiply(d,c)),sFlat3),
inference(step,[status(thm)],[t9,t33]) ).
cnf(t54,plain,
multiply(multiply(a,multiply(d,c)),sFlat3) = sFlat4,
inference(orient,[status(thm)],[t15776]) ).
cnf(t15780,plain,
multiply(multiply(a,sFlat0),sFlat3) = sFlat4,
inference(step,[status(thm)],[t54,t85]) ).
cnf(t92,plain,
multiply(multiply(a,sFlat0),sFlat3) = sFlat4,
inference(rw,[status(thm)],[t15780]) ).
cnf(t15783,plain,
multiply(sFlat1,sFlat3) = sFlat4,
inference(step,[status(thm)],[t92,t100]) ).
cnf(t128,plain,
multiply(sFlat1,sFlat3) = sFlat4,
inference(orient,[status(thm)],[t15783]) ).
cnf(f2,axiom,
multiply(multiply(X,Y),multiply(Z,U)) = multiply(multiply(X,Z),multiply(Y,U)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',medial_law) ).
fof(f2_nnf,plain,
! [X,Y,Z,U] : multiply(multiply(X,Y),multiply(Z,U)) = multiply(multiply(X,Z),multiply(Y,U)),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [X,Y,Z,U] : multiply(multiply(X,Y),multiply(Z,U)) = multiply(multiply(X,Z),multiply(Y,U)),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
multiply(multiply(X0,X1),multiply(X2,X3)) = multiply(multiply(X0,X2),multiply(X1,X3)),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(t4,plain,
multiply(multiply(X1,X2),multiply(X3,X4)) = multiply(multiply(X1,X3),multiply(X2,X4)),
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t26,plain,
multiply(multiply(X1,X2),multiply(X3,X4)) = multiply(multiply(X1,X3),multiply(X2,X4)),
inference(orient,[status(thm)],[t4]) ).
cnf(t12,axiom,
sFlat7 = multiply(d,e),
introduced(definition) ).
cnf(t77,plain,
multiply(d,e) = sFlat7,
inference(orient,[status(thm)],[t12]) ).
cnf(t13,axiom,
sFlat8 = multiply(multiply(d,e),f),
introduced(definition) ).
cnf(t40,plain,
multiply(multiply(d,e),f) = sFlat8,
inference(orient,[status(thm)],[t13]) ).
cnf(t15779,plain,
multiply(sFlat7,f) = sFlat8,
inference(step,[status(thm)],[t40,t77]) ).
cnf(t84,plain,
multiply(sFlat7,f) = sFlat8,
inference(rw,[status(thm)],[t15779]) ).
cnf(t121,plain,
multiply(sFlat7,f) = sFlat8,
inference(orient,[status(thm)],[t84]) ).
cnf(t127,plain,
multiply(multiply(X1,sFlat7),multiply(X2,f)) = multiply(multiply(X1,X2),sFlat8),
inference(cp,[status(thm)],[t26,t121]) ).
cnf(t316,plain,
multiply(multiply(X1,sFlat7),multiply(X2,f)) = multiply(multiply(X1,X2),sFlat8),
inference(orient,[status(thm)],[t127]) ).
cnf(t10,axiom,
sFlat5 = multiply(b,c),
introduced(definition) ).
cnf(t69,plain,
multiply(b,c) = sFlat5,
inference(orient,[status(thm)],[t10]) ).
cnf(t11,axiom,
sFlat6 = multiply(a,multiply(b,c)),
introduced(definition) ).
cnf(t15781,plain,
sFlat6 = multiply(a,sFlat5),
inference(step,[status(thm)],[t11,t69]) ).
cnf(t93,plain,
multiply(a,sFlat5) = sFlat6,
inference(orient,[status(thm)],[t15781]) ).
cnf(t14,axiom,
sFlat9 = multiply(multiply(a,multiply(b,c)),multiply(multiply(d,e),f)),
introduced(definition) ).
cnf(t15775,plain,
sFlat9 = multiply(multiply(a,multiply(d,e)),multiply(multiply(b,c),f)),
inference(step,[status(thm)],[t14,t26]) ).
cnf(t47,plain,
multiply(multiply(a,multiply(d,e)),multiply(multiply(b,c),f)) = sFlat9,
inference(orient,[status(thm)],[t15775]) ).
cnf(t15778,plain,
multiply(multiply(a,multiply(d,e)),multiply(sFlat5,f)) = sFlat9,
inference(step,[status(thm)],[t47,t69]) ).
cnf(t76,plain,
multiply(multiply(a,multiply(d,e)),multiply(sFlat5,f)) = sFlat9,
inference(rw,[status(thm)],[t15778]) ).
cnf(t98,plain,
multiply(multiply(a,X1),multiply(sFlat5,X2)) = multiply(sFlat6,multiply(X1,X2)),
inference(cp,[status(thm)],[t26,t93]) ).
cnf(t223,plain,
multiply(multiply(a,X1),multiply(sFlat5,X2)) = multiply(sFlat6,multiply(X1,X2)),
inference(orient,[status(thm)],[t98]) ).
cnf(t15784,plain,
multiply(sFlat6,multiply(multiply(d,e),f)) = sFlat9,
inference(step,[status(thm)],[t76,t223]) ).
cnf(t15785,plain,
multiply(sFlat6,multiply(sFlat7,f)) = sFlat9,
inference(step,[status(thm)],[t15784,t77]) ).
cnf(t15786,plain,
multiply(sFlat6,sFlat8) = sFlat9,
inference(step,[status(thm)],[t15785,t121]) ).
cnf(t882,plain,
multiply(sFlat6,sFlat8) = sFlat9,
inference(orient,[status(thm)],[t15786]) ).
cnf(f0,axiom,
( X = U
| multiply(U,Y) != Z
| multiply(X,Y) != Z ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',left_cancellation) ).
fof(f0_nnf,plain,
! [X,Y,Z,U] :
( X = U
| multiply(U,Y) != Z
| multiply(X,Y) != Z ),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [X,Y,Z,U] :
( X = U
| multiply(U,Y) != Z
| multiply(X,Y) != Z ),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
( X0 = X3
| multiply(X3,X1) != X2
| multiply(X0,X1) != X2 ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t3,plain,
ifeq(multiply(X1,X2),X3,ifeq(multiply(X4,X2),X3,X1,X4),X4) = X4,
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t20,plain,
ifeq(multiply(X1,X2),X3,ifeq(multiply(X4,X2),X3,X1,X4),X4) = X4,
inference(orient,[status(thm)],[t3]) ).
cnf(t1,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t15,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t1]) ).
cnf(t23,plain,
X1 = ifeq(multiply(X2,X3),multiply(X1,X3),X2,X1),
inference(cp,[status(thm)],[t20,t15]) ).
cnf(t759,plain,
ifeq(multiply(X1,X2),multiply(X3,X2),X1,X3) = X3,
inference(orient,[status(thm)],[t23]) ).
cnf(t896,plain,
multiply(multiply(sFlat6,X1),multiply(sFlat8,X2)) = multiply(sFlat9,multiply(X1,X2)),
inference(cp,[status(thm)],[t26,t882]) ).
cnf(t915,plain,
multiply(multiply(sFlat6,X1),multiply(sFlat8,X2)) = multiply(sFlat9,multiply(X1,X2)),
inference(orient,[status(thm)],[t896]) ).
cnf(t66,plain,
multiply(multiply(b,X1),multiply(e,X2)) = multiply(sFlat2,multiply(X1,X2)),
inference(cp,[status(thm)],[t26,t61]) ).
cnf(t135,plain,
multiply(multiply(b,X1),multiply(e,X2)) = multiply(sFlat2,multiply(X1,X2)),
inference(orient,[status(thm)],[t66]) ).
cnf(t136,plain,
multiply(sFlat2,multiply(c,X1)) = multiply(sFlat5,multiply(e,X1)),
inference(cp,[status(thm)],[t135,t69]) ).
cnf(t143,plain,
multiply(sFlat5,multiply(e,X1)) = multiply(sFlat2,multiply(c,X1)),
inference(orient,[status(thm)],[t136]) ).
cnf(t225,plain,
multiply(sFlat6,multiply(X1,multiply(e,X2))) = multiply(multiply(a,X1),multiply(sFlat2,multiply(c,X2))),
inference(cp,[status(thm)],[t223,t143]) ).
cnf(t2890,plain,
multiply(multiply(a,X1),multiply(sFlat2,multiply(c,X2))) = multiply(sFlat6,multiply(X1,multiply(e,X2))),
inference(orient,[status(thm)],[t225]) ).
cnf(t2891,plain,
multiply(sFlat6,multiply(X1,multiply(e,X2))) = multiply(multiply(a,sFlat2),multiply(X1,multiply(c,X2))),
inference(cp,[status(thm)],[t2890,t26]) ).
cnf(t3477,plain,
multiply(multiply(a,sFlat2),multiply(X1,multiply(c,X2))) = multiply(sFlat6,multiply(X1,multiply(e,X2))),
inference(orient,[status(thm)],[t2891]) ).
cnf(t90,plain,
multiply(multiply(d,X1),multiply(c,X2)) = multiply(sFlat0,multiply(X1,X2)),
inference(cp,[status(thm)],[t26,t85]) ).
cnf(t209,plain,
multiply(multiply(d,X1),multiply(c,X2)) = multiply(sFlat0,multiply(X1,X2)),
inference(orient,[status(thm)],[t90]) ).
cnf(t3488,plain,
multiply(sFlat6,multiply(multiply(d,X1),multiply(e,X2))) = multiply(multiply(a,sFlat2),multiply(sFlat0,multiply(X1,X2))),
inference(cp,[status(thm)],[t3477,t209]) ).
cnf(t82,plain,
multiply(multiply(d,X1),multiply(e,X2)) = multiply(sFlat7,multiply(X1,X2)),
inference(cp,[status(thm)],[t26,t77]) ).
cnf(t187,plain,
multiply(multiply(d,X1),multiply(e,X2)) = multiply(sFlat7,multiply(X1,X2)),
inference(orient,[status(thm)],[t82]) ).
cnf(t15816,plain,
multiply(sFlat6,multiply(sFlat7,multiply(X1,X2))) = multiply(multiply(a,sFlat2),multiply(sFlat0,multiply(X1,X2))),
inference(step,[status(thm)],[t3488,t187]) ).
cnf(t105,plain,
multiply(multiply(a,X1),multiply(sFlat0,X2)) = multiply(sFlat1,multiply(X1,X2)),
inference(cp,[status(thm)],[t26,t100]) ).
cnf(t246,plain,
multiply(multiply(a,X1),multiply(sFlat0,X2)) = multiply(sFlat1,multiply(X1,X2)),
inference(orient,[status(thm)],[t105]) ).
cnf(t15817,plain,
multiply(sFlat6,multiply(sFlat7,multiply(X1,X2))) = multiply(sFlat1,multiply(sFlat2,multiply(X1,X2))),
inference(step,[status(thm)],[t15816,t246]) ).
cnf(t3526,plain,
multiply(sFlat6,multiply(sFlat7,multiply(X1,X2))) = multiply(sFlat1,multiply(sFlat2,multiply(X1,X2))),
inference(orient,[status(thm)],[t15817]) ).
cnf(f3,hypothesis,
multiply(an_element,an_element) = an_element,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',idempotent_element) ).
fof(f3_nnf,plain,
multiply(an_element,an_element) = an_element,
inference(nnf_transformation,[status(thm)],[f3]) ).
cnf(c3,plain,
multiply(an_element,an_element) = an_element,
inference(cnf_transformation,[status(esa)],[f3_nnf]) ).
cnf(t0,plain,
multiply(an_element,an_element) = an_element,
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(t107,plain,
multiply(an_element,an_element) = an_element,
inference(orient,[status(thm)],[t0]) ).
cnf(t3531,plain,
multiply(sFlat1,multiply(sFlat2,multiply(an_element,an_element))) = multiply(sFlat6,multiply(sFlat7,an_element)),
inference(cp,[status(thm)],[t3526,t107]) ).
cnf(t15822,plain,
multiply(sFlat1,multiply(sFlat2,an_element)) = multiply(sFlat6,multiply(sFlat7,an_element)),
inference(step,[status(thm)],[t3531,t107]) ).
cnf(t3723,plain,
multiply(sFlat6,multiply(sFlat7,an_element)) = multiply(sFlat1,multiply(sFlat2,an_element)),
inference(orient,[status(thm)],[t15822]) ).
cnf(t3729,plain,
multiply(sFlat9,multiply(multiply(sFlat7,an_element),X1)) = multiply(multiply(sFlat1,multiply(sFlat2,an_element)),multiply(sFlat8,X1)),
inference(cp,[status(thm)],[t915,t3723]) ).
cnf(t15852,plain,
multiply(sFlat9,multiply(multiply(sFlat7,an_element),X1)) = multiply(multiply(sFlat1,sFlat8),multiply(multiply(sFlat2,an_element),X1)),
inference(step,[status(thm)],[t3729,t26]) ).
cnf(t5247,plain,
multiply(multiply(sFlat1,sFlat8),multiply(multiply(sFlat2,an_element),X1)) = multiply(sFlat9,multiply(multiply(sFlat7,an_element),X1)),
inference(orient,[status(thm)],[t15852]) ).
cnf(t119,plain,
multiply(multiply(sFlat2,X1),multiply(f,X2)) = multiply(sFlat3,multiply(X1,X2)),
inference(cp,[status(thm)],[t26,t114]) ).
cnf(t285,plain,
multiply(multiply(sFlat2,X1),multiply(f,X2)) = multiply(sFlat3,multiply(X1,X2)),
inference(orient,[status(thm)],[t119]) ).
cnf(t5248,plain,
multiply(sFlat9,multiply(multiply(sFlat7,an_element),multiply(f,X1))) = multiply(multiply(sFlat1,sFlat8),multiply(sFlat3,multiply(an_element,X1))),
inference(cp,[status(thm)],[t5247,t285]) ).
cnf(t126,plain,
multiply(multiply(sFlat7,X1),multiply(f,X2)) = multiply(sFlat8,multiply(X1,X2)),
inference(cp,[status(thm)],[t26,t121]) ).
cnf(t308,plain,
multiply(multiply(sFlat7,X1),multiply(f,X2)) = multiply(sFlat8,multiply(X1,X2)),
inference(orient,[status(thm)],[t126]) ).
cnf(t15853,plain,
multiply(sFlat9,multiply(sFlat8,multiply(an_element,X1))) = multiply(multiply(sFlat1,sFlat8),multiply(sFlat3,multiply(an_element,X1))),
inference(step,[status(thm)],[t5248,t308]) ).
cnf(t133,plain,
multiply(multiply(sFlat1,X1),multiply(sFlat3,X2)) = multiply(sFlat4,multiply(X1,X2)),
inference(cp,[status(thm)],[t26,t128]) ).
cnf(t324,plain,
multiply(multiply(sFlat1,X1),multiply(sFlat3,X2)) = multiply(sFlat4,multiply(X1,X2)),
inference(orient,[status(thm)],[t133]) ).
cnf(t15854,plain,
multiply(sFlat9,multiply(sFlat8,multiply(an_element,X1))) = multiply(sFlat4,multiply(sFlat8,multiply(an_element,X1))),
inference(step,[status(thm)],[t15853,t324]) ).
cnf(t5291,plain,
multiply(sFlat9,multiply(sFlat8,multiply(an_element,X1))) = multiply(sFlat4,multiply(sFlat8,multiply(an_element,X1))),
inference(orient,[status(thm)],[t15854]) ).
cnf(t5292,plain,
multiply(sFlat4,multiply(sFlat8,multiply(an_element,an_element))) = multiply(sFlat9,multiply(sFlat8,an_element)),
inference(cp,[status(thm)],[t5291,t107]) ).
cnf(t15855,plain,
multiply(sFlat4,multiply(sFlat8,an_element)) = multiply(sFlat9,multiply(sFlat8,an_element)),
inference(step,[status(thm)],[t5292,t107]) ).
cnf(t5327,plain,
multiply(sFlat9,multiply(sFlat8,an_element)) = multiply(sFlat4,multiply(sFlat8,an_element)),
inference(orient,[status(thm)],[t15855]) ).
cnf(t5332,plain,
X1 = ifeq(multiply(sFlat4,multiply(sFlat8,an_element)),multiply(X1,multiply(sFlat8,an_element)),sFlat9,X1),
inference(cp,[status(thm)],[t759,t5327]) ).
cnf(t15586,plain,
ifeq(multiply(sFlat4,multiply(sFlat8,an_element)),multiply(X1,multiply(sFlat8,an_element)),sFlat9,X1) = X1,
inference(orient,[status(thm)],[t5332]) ).
cnf(t15587,plain,
sFlat4 = sFlat9,
inference(cp,[status(thm)],[t15586,t15]) ).
cnf(t15605,plain,
sFlat9 = sFlat4,
inference(orient,[status(thm)],[t15587]) ).
cnf(t15928,plain,
multiply(sFlat6,sFlat8) = sFlat4,
inference(step,[status(thm)],[t882,t15605]) ).
cnf(t15606,plain,
multiply(sFlat6,sFlat8) = sFlat4,
inference(orient,[status(thm)],[t15928]) ).
cnf(f4,negated_conjecture,
multiply(multiply(a,multiply(d,c)),multiply(multiply(b,e),f)) != multiply(multiply(a,multiply(b,c)),multiply(multiply(d,e),f)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this) ).
fof(f4_nnf,plain,
multiply(multiply(a,multiply(d,c)),multiply(multiply(b,e),f)) != multiply(multiply(a,multiply(b,c)),multiply(multiply(d,e),f)),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
multiply(multiply(a,multiply(d,c)),multiply(multiply(b,e),f)) != multiply(multiply(a,multiply(b,c)),multiply(multiply(d,e),f)),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c4,plain,
multiply(multiply(a,multiply(d,c)),multiply(multiply(b,e),f)) != multiply(multiply(a,multiply(b,c)),multiply(multiply(d,e),f)),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(goal_0,negated_conjecture,
multiply(multiply(a,multiply(d,c)),multiply(multiply(b,e),f)) != multiply(multiply(a,multiply(b,c)),multiply(multiply(d,e),f)),
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(g0_0,plain,
multiply(multiply(a,sFlat0),multiply(multiply(b,e),f)) != multiply(multiply(a,multiply(b,c)),multiply(multiply(d,e),f)),
inference(rw,[status(thm)],[goal_0,t85]) ).
cnf(g0_1,plain,
multiply(sFlat1,multiply(multiply(b,e),f)) != multiply(multiply(a,multiply(b,c)),multiply(multiply(d,e),f)),
inference(rw,[status(thm)],[g0_0,t100]) ).
cnf(g0_2,plain,
multiply(sFlat1,multiply(sFlat2,f)) != multiply(multiply(a,multiply(b,c)),multiply(multiply(d,e),f)),
inference(rw,[status(thm)],[g0_1,t61]) ).
cnf(g0_3,plain,
multiply(sFlat1,sFlat3) != multiply(multiply(a,multiply(b,c)),multiply(multiply(d,e),f)),
inference(rw,[status(thm)],[g0_2,t114]) ).
cnf(g0_4,plain,
sFlat4 != multiply(multiply(a,multiply(b,c)),multiply(multiply(d,e),f)),
inference(rw,[status(thm)],[g0_3,t128]) ).
cnf(g0_5,plain,
sFlat4 != multiply(multiply(a,multiply(d,e)),multiply(multiply(b,c),f)),
inference(rw,[status(thm)],[g0_4,t26]) ).
cnf(g0_6,plain,
sFlat4 != multiply(multiply(a,sFlat7),multiply(multiply(b,c),f)),
inference(rw,[status(thm)],[g0_5,t77]) ).
cnf(g0_7,plain,
sFlat4 != multiply(multiply(a,multiply(b,c)),sFlat8),
inference(rw,[status(thm)],[g0_6,t316]) ).
cnf(g0_8,plain,
sFlat4 != multiply(multiply(a,sFlat5),sFlat8),
inference(rw,[status(thm)],[g0_7,t69]) ).
cnf(g0_9,plain,
sFlat4 != multiply(sFlat6,sFlat8),
inference(rw,[status(thm)],[g0_8,t93]) ).
cnf(g0_10,plain,
sFlat4 != sFlat4,
inference(rw,[status(thm)],[g0_9,t15606]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_10]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ALG003-1 : TPTP v9.3.1. Bugfixed v2.5.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.11/0.36 % Computer : n011.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Fri Sep 25 04:30:28 UTC 2026
% 0.11/0.36 % CPUTime :
% 0.11/0.36 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 18.07/2.78 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 18.07/2.78 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------