%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LCL901+1 : TPTP v9.3.1. Released v5.5.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 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 : Thu Sep 24 01:09:03 PM UTC 2026
% Result : Theorem 18.13s 7.81s
% Output : CNFRefutation 18.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 34
% Number of leaves : 13
% Syntax : Number of formulae : 117 ( 74 unt; 0 def)
% Number of atoms : 172 ( 60 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 108 ( 53 ~; 47 |; 3 &)
% ( 1 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 3 con; 0-2 aty)
% Number of variables : 254 ( 253 !; 1 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [A,B,C] : '+'('+'(A,B),C) = '+'(A,'+'(B,C)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [A,B] : '+'(A,B) = '+'(B,A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,axiom,
! [A] : '+'(A,'0') = A,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [A] : '>='(A,A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [X3,X4] :
( ( '>='(X4,X3)
& '>='(X3,X4) )
=> X3 = X4 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [X5,X6,X7] :
( '>='('+'(X5,X6),X7)
<=> '>='(X6,'==>'(X5,X7)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [A] : '>='(A,'0'),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [X8,X9,X10] :
( '>='(X8,X9)
=> '>='('+'(X8,X10),'+'(X9,X10)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [X11,X12,X13] :
( '>='(X11,X12)
=> '>='('==>'(X12,X13),'==>'(X11,X13)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [X14,X15,X16] :
( '>='(X14,X15)
=> '>='('==>'(X16,X14),'==>'(X16,X15)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f13,axiom,
! [A,B] : '==>'('==>'(A,B),B) = '==>'('==>'(B,A),A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f14,axiom,
! [A] : '+'(A,A) = A,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,conjecture,
! [X17] : '==>'('==>'('==>'(X17,'1'),X17),X17) = '0',
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f16,negated_conjecture,
~ ! [X17] : '==>'('==>'('==>'(X17,'1'),X17),X17) = '0',
inference(negated_conjecture,[status(cth)],[f15]) ).
fof(f17,plain,
! [X0,X1,X2] : '+'('+'(X0,X1),X2) = '+'(X0,'+'(X1,X2)),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f18,plain,
! [X0,X1] : '+'(X0,X1) = '+'(X1,X0),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f19,plain,
! [X0] : '+'(X0,'0') = X0,
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f20,plain,
! [X0] : '>='(X0,X0),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f24,plain,
! [X3,X4] :
( X3 = X4
| ~ '>='(X4,X3)
| ~ '>='(X3,X4) ),
inference(pre_NNF_transformation,[status(thm)],[f6]) ).
fof(f25,plain,
! [X0,X1] :
( X0 = X1
| ~ '>='(X1,X0)
| ~ '>='(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f24]) ).
fof(f26,plain,
! [X5,X6,X7] :
( ( ~ '>='(X6,'==>'(X5,X7))
| '>='('+'(X5,X6),X7) )
& ( '>='(X6,'==>'(X5,X7))
| ~ '>='('+'(X5,X6),X7) ) ),
inference(NNF_transformation,[status(thm)],[f7]) ).
fof(f27,plain,
( ! [X5,X6,X7] :
( ~ '>='(X6,'==>'(X5,X7))
| '>='('+'(X5,X6),X7) )
& ! [X5,X6,X7] :
( '>='(X6,'==>'(X5,X7))
| ~ '>='('+'(X5,X6),X7) ) ),
inference(miniscoping,[status(thm)],[f26]) ).
fof(f28,plain,
! [X0,X1,X2] :
( '>='(X1,'==>'(X0,X2))
| ~ '>='('+'(X0,X1),X2) ),
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f29,plain,
! [X0,X1,X2] :
( ~ '>='(X1,'==>'(X0,X2))
| '>='('+'(X0,X1),X2) ),
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f30,plain,
! [X0] : '>='(X0,'0'),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f31,plain,
! [X8,X9,X10] :
( '>='('+'(X8,X10),'+'(X9,X10))
| ~ '>='(X8,X9) ),
inference(pre_NNF_transformation,[status(thm)],[f9]) ).
fof(f32,plain,
! [X8,X9] :
( ! [X10] : '>='('+'(X8,X10),'+'(X9,X10))
| ~ '>='(X8,X9) ),
inference(miniscoping,[status(thm)],[f31]) ).
fof(f33,plain,
! [X0,X1,X2] :
( '>='('+'(X0,X2),'+'(X1,X2))
| ~ '>='(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f32]) ).
fof(f34,plain,
! [X11,X12,X13] :
( '>='('==>'(X12,X13),'==>'(X11,X13))
| ~ '>='(X11,X12) ),
inference(pre_NNF_transformation,[status(thm)],[f10]) ).
fof(f35,plain,
! [X11,X12] :
( ! [X13] : '>='('==>'(X12,X13),'==>'(X11,X13))
| ~ '>='(X11,X12) ),
inference(miniscoping,[status(thm)],[f34]) ).
fof(f36,plain,
! [X0,X1,X2] :
( '>='('==>'(X1,X2),'==>'(X0,X2))
| ~ '>='(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f35]) ).
fof(f37,plain,
! [X14,X15,X16] :
( '>='('==>'(X16,X14),'==>'(X16,X15))
| ~ '>='(X14,X15) ),
inference(pre_NNF_transformation,[status(thm)],[f11]) ).
fof(f38,plain,
! [X14,X15] :
( ! [X16] : '>='('==>'(X16,X14),'==>'(X16,X15))
| ~ '>='(X14,X15) ),
inference(miniscoping,[status(thm)],[f37]) ).
fof(f39,plain,
! [X0,X1,X2] :
( '>='('==>'(X2,X0),'==>'(X2,X1))
| ~ '>='(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f38]) ).
fof(f41,plain,
! [X0,X1] : '==>'('==>'(X0,X1),X1) = '==>'('==>'(X1,X0),X0),
inference(cnf_transformation,[status(thm)],[f13]) ).
fof(f42,plain,
! [X0] : '+'(X0,X0) = X0,
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f43,plain,
? [X17] : '==>'('==>'('==>'(X17,'1'),X17),X17) != '0',
inference(pre_NNF_transformation,[status(thm)],[f16]) ).
fof(f44,plain,
'==>'('==>'('==>'(sK0_skl,'1'),sK0_skl),sK0_skl) != '0',
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(X17,sK0_skl)],[f43]) ).
fof(f45,plain,
'==>'('==>'('==>'(sK0_skl,'1'),sK0_skl),sK0_skl) != '0',
inference(cnf_transformation,[status(thm)],[f44]) ).
fof(f46,plain,
! [X0,X1] : '>='(X0,'==>'(X1,'0')),
inference(resolution,[status(thm)],[f28,f30]) ).
fof(f48,plain,
! [X0,X1] :
( '>='('0','==>'(X0,X1))
| ~ '>='(X0,X1) ),
inference(paramodulation,[status(thm)],[f19,f28]) ).
fof(f56,plain,
! [X0,X1,X2] :
( '>='('+'(X2,'==>'(X2,X0)),X1)
| ~ '>='(X0,X1) ),
inference(resolution,[status(thm)],[f39,f29]) ).
fof(f63,plain,
! [X0,X1] : '>='(X0,'==>'('==>'('0',X1),X1)),
inference(paramodulation,[status(thm)],[f41,f46]) ).
fof(f82,plain,
! [X0,X1] : '>='('+'('==>'('0',X0),X1),X0),
inference(resolution,[status(thm)],[f63,f29]) ).
fof(f86,plain,
! [X0,X1,X2] : '>='('+'(X0,'+'('==>'('0','==>'(X0,X1)),X2)),X1),
inference(resolution,[status(thm)],[f82,f29]) ).
fof(f88,plain,
! [X0] : '>='('==>'('0',X0),X0),
inference(paramodulation,[status(thm)],[f19,f82]) ).
fof(f117,plain,
! [X0,X1] : '>='(X0,'==>'(X1,'+'(X1,X0))),
inference(resolution,[status(thm)],[f20,f28]) ).
fof(f127,plain,
! [X0] : X0 = '+'('0',X0),
inference(paramodulation,[status(thm)],[f19,f18]) ).
fof(f134,plain,
! [X0,X1] : '>='('+'(X0,'==>'('0',X1)),X1),
inference(paramodulation,[status(thm)],[f18,f82]) ).
fof(f138,plain,
! [X0,X1,X2] :
( '>='(X0,'==>'(X1,X2))
| ~ '>='('+'(X0,X1),X2) ),
inference(paramodulation,[status(thm)],[f18,f28]) ).
fof(f179,plain,
! [X0] :
( X0 = '==>'('0',X0)
| ~ '>='(X0,'==>'('0',X0)) ),
inference(resolution,[status(thm)],[f25,f88]) ).
fof(f180,plain,
! [X0,X1,X2] :
( ~ '>='(X2,X1)
| '==>'(X0,X1) = '==>'(X0,X2)
| ~ '>='('==>'(X0,X1),'==>'(X0,X2)) ),
inference(resolution,[status(thm)],[f25,f39]) ).
fof(f182,plain,
! [X0,X1] :
( ~ '>='(X0,X1)
| '==>'(X0,X1) = '0'
| ~ '>='('==>'(X0,X1),'0') ),
inference(resolution,[status(thm)],[f25,f48]) ).
fof(f188,plain,
! [X0] :
( '0' = X0
| ~ '>='('0',X0) ),
inference(resolution,[status(thm)],[f25,f30]) ).
fof(f190,plain,
! [X0,X1] :
( ~ '>='(X0,X1)
| '==>'(X0,X1) = '0' ),
inference(forward_subsumption_resolution,[status(thm)],[f182,f30]) ).
fof(f324,plain,
! [X0] : '>='(X0,'==>'('0',X0)),
inference(paramodulation,[status(thm)],[f127,f117]) ).
fof(f327,plain,
! [X0,X1] : '>='(X0,'==>'(X1,'+'(X0,X1))),
inference(paramodulation,[status(thm)],[f18,f117]) ).
fof(f334,plain,
! [X0] : X0 = '==>'('0',X0),
inference(backward_subsumption_resolution,[status(thm)],[f179,f324]) ).
fof(f341,plain,
! [X0,X1,X2] : '>='('+'(X0,'+'('==>'(X0,X1),X2)),X1),
inference(backward_demodulation,[status(thm)],[f334,f86]) ).
fof(f349,plain,
! [X0,X1] : '>='('+'(X0,X1),X1),
inference(backward_demodulation,[status(thm)],[f334,f134]) ).
fof(f383,plain,
! [X0,X1] :
( '>='(X1,'==>'(X0,X1))
| ~ '>='(X0,'0') ),
inference(paramodulation,[status(thm)],[f334,f36]) ).
fof(f391,plain,
! [X0,X1] : '>='(X0,'==>'(X1,X0)),
inference(forward_subsumption_resolution,[status(thm)],[f383,f30]) ).
fof(f416,plain,
! [X0,X1,X2] : '+'('+'(X0,X1),X2) = '+'(X1,'+'(X0,X2)),
inference(paramodulation,[status(thm)],[f18,f17]) ).
fof(f418,plain,
! [X0,X1] : '+'(X0,X1) = '+'(X0,'+'(X0,X1)),
inference(paramodulation,[status(thm)],[f42,f17]) ).
fof(f428,plain,
! [X0,X1,X2,X3] :
( '>='(X2,'==>'('+'(X0,X1),X3))
| ~ '>='('+'(X0,'+'(X1,X2)),X3) ),
inference(paramodulation,[status(thm)],[f17,f28]) ).
fof(f456,plain,
! [X0,X1] :
( '>='(X0,'+'(X1,X0))
| ~ '>='(X0,X1) ),
inference(paramodulation,[status(thm)],[f42,f33]) ).
fof(f472,plain,
! [X0,X1] :
( X0 = '+'(X1,X0)
| ~ '>='(X0,'+'(X1,X0)) ),
inference(resolution,[status(thm)],[f349,f25]) ).
fof(f473,plain,
! [X0,X1,X2] : '>='('+'(X0,'+'(X1,X2)),X2),
inference(paramodulation,[status(thm)],[f17,f349]) ).
fof(f487,plain,
! [X0,X1] :
( '==>'(X0,X1) = X1
| ~ '>='('==>'(X0,X1),X1) ),
inference(resolution,[status(thm)],[f391,f25]) ).
fof(f490,plain,
! [X0,X1] : '>='(X0,'==>'('==>'(X0,X1),X1)),
inference(paramodulation,[status(thm)],[f41,f391]) ).
fof(f516,plain,
~ '>='('==>'('==>'(sK0_skl,'1'),sK0_skl),sK0_skl),
inference(resolution,[status(thm)],[f190,f45]) ).
fof(f632,plain,
! [X0,X1,X2] : '>='('+'(X0,X1),'==>'(X2,X1)),
inference(resolution,[status(thm)],[f473,f28]) ).
fof(f641,plain,
! [X0,X1,X2] : '>='('+'('+'(X0,X1),X2),X1),
inference(paramodulation,[status(thm)],[f18,f473]) ).
fof(f655,plain,
! [X0,X1,X2] : '>='('+'(X0,'+'(X1,X2)),X1),
inference(forward_demodulation,[status(thm)],[f17,f641]) ).
fof(f662,plain,
! [X0,X1] : '>='('+'('==>'(X0,X1),X0),X1),
inference(resolution,[status(thm)],[f490,f29]) ).
fof(f758,plain,
! [X0,X1,X2] : '>='('+'(X0,X1),'==>'(X2,X0)),
inference(paramodulation,[status(thm)],[f18,f632]) ).
fof(f889,plain,
! [X0,X1,X2] : '>='(X0,'==>'(X1,'==>'(X2,X1))),
inference(resolution,[status(thm)],[f758,f28]) ).
fof(f914,plain,
! [X0,X1] : '0' = '==>'(X0,'==>'(X1,X0)),
inference(resolution,[status(thm)],[f889,f188]) ).
fof(f1058,plain,
! [X0,X1,X2] :
( '>='('+'(X1,'0'),X2)
| ~ '>='('==>'(X0,X1),X2) ),
inference(paramodulation,[status(thm)],[f914,f56]) ).
fof(f1078,plain,
! [X0,X1,X2] :
( '>='(X1,X2)
| ~ '>='('==>'(X0,X1),X2) ),
inference(forward_demodulation,[status(thm)],[f19,f1058]) ).
fof(f1108,plain,
! [X0,X1] : '+'(X0,X1) = '+'(X0,'+'(X1,X0)),
inference(paramodulation,[status(thm)],[f18,f418]) ).
fof(f1178,plain,
! [X0,X1] :
( '+'(X1,X0) = X0
| ~ '>='('+'(X1,X0),X0)
| ~ '>='(X0,X1) ),
inference(resolution,[status(thm)],[f456,f25]) ).
fof(f1192,plain,
! [X0,X1] :
( '+'(X1,X0) = X0
| ~ '>='(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f1178,f349]) ).
fof(f1201,plain,
! [X0,X1] :
( '+'(X0,X1) = X0
| ~ '>='(X0,X1) ),
inference(paramodulation,[status(thm)],[f18,f1192]) ).
fof(f1298,plain,
! [X0,X1,X2] : '>='(X0,'==>'(X1,'+'('==>'(X2,X0),X1))),
inference(resolution,[status(thm)],[f1078,f327]) ).
fof(f1356,plain,
! [X0,X1] :
( '+'(X0,X1) = X0
| ~ '>='(X0,'+'(X1,X0)) ),
inference(paramodulation,[status(thm)],[f1108,f1201]) ).
fof(f1516,plain,
! [X0,X1,X2] : '>='(X0,'==>'('+'(X1,X2),X1)),
inference(resolution,[status(thm)],[f138,f655]) ).
fof(f1565,plain,
! [X0,X1] :
( ~ '>='('+'('==>'(X0,X1),X0),X1)
| '==>'(X0,X1) = '==>'(X0,'+'('==>'(X0,X1),X0)) ),
inference(resolution,[status(thm)],[f180,f327]) ).
fof(f1584,plain,
! [X0,X1,X2] :
( ~ '>='('==>'(X2,X0),X1)
| '==>'(X0,X1) = '==>'(X0,'==>'(X2,X0))
| ~ '>='('==>'(X0,X1),'0') ),
inference(paramodulation,[status(thm)],[f914,f180]) ).
fof(f1595,plain,
! [X0,X1] : '==>'(X0,X1) = '==>'(X0,'+'('==>'(X0,X1),X0)),
inference(forward_subsumption_resolution,[status(thm)],[f1565,f662]) ).
fof(f1613,plain,
! [X0,X1,X2] :
( ~ '>='('==>'(X2,X0),X1)
| '==>'(X0,X1) = '0'
| ~ '>='('==>'(X0,X1),'0') ),
inference(forward_demodulation,[status(thm)],[f914,f1584]) ).
fof(f1614,plain,
! [X0,X1,X2] :
( ~ '>='('==>'(X2,X0),X1)
| '==>'(X0,X1) = '0' ),
inference(forward_subsumption_resolution,[status(thm)],[f1613,f30]) ).
fof(f1620,plain,
! [X0,X1] : '0' = '==>'('+'(X0,X1),X0),
inference(resolution,[status(thm)],[f1516,f188]) ).
fof(f3011,plain,
! [X0,X1,X2] : '>='(X0,'==>'('+'(X1,'==>'(X1,X2)),X2)),
inference(resolution,[status(thm)],[f341,f428]) ).
fof(f5574,plain,
! [X0,X1,X2] : '>='('+'(X0,X1),'+'('==>'(X2,X1),X0)),
inference(resolution,[status(thm)],[f1298,f29]) ).
fof(f7753,plain,
! [X0,X1,X2] : '==>'(X0,'==>'('+'(X1,'==>'(X1,X2)),X2)) = '0',
inference(resolution,[status(thm)],[f3011,f1614]) ).
fof(f7754,plain,
! [X0,X1,X2] : '==>'(X0,'==>'('+'(X1,'==>'(X1,X2)),X2)) = '==>'('+'(X1,'==>'(X1,X2)),X2),
inference(resolution,[status(thm)],[f3011,f487]) ).
fof(f7798,plain,
! [X0,X1] : '0' = '==>'('+'(X0,'==>'(X0,X1)),X1),
inference(forward_demodulation,[status(thm)],[f7753,f7754]) ).
fof(f7848,plain,
! [X0,X1] : '0' = '==>'('+'('+'(X0,'==>'(X0,X1)),'0'),X1),
inference(paramodulation,[status(thm)],[f7798,f7798]) ).
fof(f7966,plain,
! [X0,X1] : '0' = '==>'('+'('==>'(X0,X1),'+'(X0,'0')),X1),
inference(forward_demodulation,[status(thm)],[f416,f7848]) ).
fof(f7968,plain,
! [X0,X1] : '0' = '==>'('+'('==>'(X0,X1),X0),X1),
inference(forward_demodulation,[status(thm)],[f19,f7966]) ).
fof(f10463,plain,
! [X0,X1] : '>='(X0,'+'('==>'(X1,X0),X0)),
inference(paramodulation,[status(thm)],[f42,f5574]) ).
fof(f10558,plain,
! [X0,X1] : '+'(X0,'==>'(X1,X0)) = X0,
inference(resolution,[status(thm)],[f10463,f1356]) ).
fof(f10559,plain,
! [X0,X1] : X0 = '+'('==>'(X1,X0),X0),
inference(resolution,[status(thm)],[f10463,f472]) ).
fof(f10640,plain,
! [X0,X1] : '+'(X0,'==>'('==>'(X0,X1),X1)) = X0,
inference(paramodulation,[status(thm)],[f41,f10558]) ).
fof(f11302,plain,
! [X0,X1] : '+'('+'('==>'(X0,X1),X0),'==>'('0',X1)) = '+'('==>'(X0,X1),X0),
inference(paramodulation,[status(thm)],[f7968,f10640]) ).
fof(f11453,plain,
! [X0,X1] : '+'(X0,'+'('==>'(X0,X1),'==>'('0',X1))) = '+'('==>'(X0,X1),X0),
inference(forward_demodulation,[status(thm)],[f416,f11302]) ).
fof(f11454,plain,
! [X0,X1] : '+'(X0,'+'('==>'(X0,X1),X1)) = '+'('==>'(X0,X1),X0),
inference(forward_demodulation,[status(thm)],[f334,f11453]) ).
fof(f11522,plain,
! [X0,X1] : '==>'(X0,X1) = '==>'(X0,'+'(X0,X1)),
inference(backward_demodulation,[status(thm)],[f11525,f1595]) ).
fof(f11525,plain,
! [X0,X1] : '+'(X0,X1) = '+'('==>'(X0,X1),X0),
inference(forward_demodulation,[status(thm)],[f10559,f11454]) ).
fof(f12934,plain,
! [X0,X1] : '==>'('==>'(X0,X1),X0) = '==>'('==>'(X0,X1),'+'(X0,X1)),
inference(paramodulation,[status(thm)],[f11525,f11522]) ).
fof(f13048,plain,
! [X0,X1] : '==>'('==>'('+'(X0,X1),X0),X0) = '==>'('==>'(X0,X1),'+'(X0,X1)),
inference(paramodulation,[status(thm)],[f11522,f41]) ).
fof(f13182,plain,
! [X0,X1] : '==>'('0',X0) = '==>'('==>'(X0,X1),'+'(X0,X1)),
inference(forward_demodulation,[status(thm)],[f1620,f13048]) ).
fof(f13183,plain,
! [X0,X1] : '==>'('==>'(X0,X1),X0) = X0,
inference(backward_demodulation,[status(thm)],[f13184,f12934]) ).
fof(f13184,plain,
! [X0,X1] : X0 = '==>'('==>'(X0,X1),'+'(X0,X1)),
inference(forward_demodulation,[status(thm)],[f334,f13182]) ).
fof(f13191,plain,
~ '>='(sK0_skl,sK0_skl),
inference(backward_demodulation,[status(thm)],[f13183,f516]) ).
fof(f13202,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f13191,f20]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL901+1 : TPTP v9.3.1. Released v5.5.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/5.39 % Computer : n017.cluster.edu
% 0.11/5.39 % Model : x86_64 x86_64
% 0.11/5.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.39 % Memory : 8046.5625MB
% 0.11/5.39 % OS : Linux 6.8.0-71-generic
% 0.11/5.39 % CPULimit : 300
% 0.11/5.39 % WCLimit : 300
% 0.11/5.39 % DateTime : Mon Sep 21 01:06:17 UTC 2026
% 0.11/5.39 % CPUTime :
% 0.16/5.41 % Drodi V4.1.1
% 18.13/7.81 % Refutation found
% 18.13/7.81 % SZS status Theorem for theBenchmark: Theorem is valid
% 18.13/7.81 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 12.25/7.87 % Elapsed time: 2.456401 seconds
% 12.25/7.87 % CPU time: 19.038679 seconds
% 12.25/7.87 % Total memory used: 137.643 MB
% 12.25/7.87 % Net memory used: 126.964 MB
%------------------------------------------------------------------------------