%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LCL470+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n005.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:07:48 PM UTC 2026
% Result : Theorem 12.69s 2.12s
% Output : CNFRefutation 13.48s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 14
% Syntax : Number of formulae : 104 ( 58 unt; 0 def)
% Number of atoms : 191 ( 9 equ)
% Maximal formula atoms : 8 ( 1 avg)
% Number of connectives : 150 ( 63 ~; 60 |; 18 &)
% ( 6 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 10 ( 8 usr; 8 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 10 con; 0-2 aty)
% Number of variables : 227 ( 215 !; 12 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
( modus_ponens
<=> ! [X,Y] :
( ( is_a_theorem(implies(X,Y))
& is_a_theorem(X) )
=> is_a_theorem(Y) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f11,axiom,
( or_2
<=> ! [X,Y] : is_a_theorem(implies(Y,or(X,Y))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f19,axiom,
( cn1
<=> ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(implies(Q,R),implies(P,R)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f20,axiom,
( cn2
<=> ! [P,Q] : is_a_theorem(implies(P,implies(not(P),Q))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f21,axiom,
( cn3
<=> ! [P] : is_a_theorem(implies(implies(not(P),P),P)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f27,axiom,
( op_or
=> ! [X,Y] : or(X,Y) = not(and(not(X),not(Y))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f29,axiom,
( op_implies_and
=> ! [X,Y] : implies(X,Y) = not(and(X,not(Y))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f32,axiom,
op_or,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f35,axiom,
modus_ponens,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f36,axiom,
cn1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f37,axiom,
cn2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f38,axiom,
cn3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f41,axiom,
op_implies_and,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f43,conjecture,
or_2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f44,negated_conjecture,
~ or_2,
inference(negated_conjecture,[status(cth)],[f43]) ).
fof(f45,plain,
( modus_ponens
<=> ! [X,Y] :
( is_a_theorem(Y)
| ~ is_a_theorem(implies(X,Y))
| ~ is_a_theorem(X) ) ),
inference(pre_NNF_transformation,[status(thm)],[f1]) ).
fof(f46,plain,
( ( ? [X,Y] :
( ~ is_a_theorem(Y)
& is_a_theorem(implies(X,Y))
& is_a_theorem(X) )
| modus_ponens )
& ( ! [X,Y] :
( is_a_theorem(Y)
| ~ is_a_theorem(implies(X,Y))
| ~ is_a_theorem(X) )
| ~ modus_ponens ) ),
inference(NNF_transformation,[status(thm)],[f45]) ).
fof(f47,plain,
( ( ? [Y] :
( ~ is_a_theorem(Y)
& ? [X] :
( is_a_theorem(implies(X,Y))
& is_a_theorem(X) ) )
| modus_ponens )
& ( ! [Y] :
( is_a_theorem(Y)
| ! [X] :
( ~ is_a_theorem(implies(X,Y))
| ~ is_a_theorem(X) ) )
| ~ modus_ponens ) ),
inference(miniscoping,[status(thm)],[f46]) ).
fof(f48,plain,
( ( ( ~ is_a_theorem(sK0_skl)
& is_a_theorem(implies(sK1_skl,sK0_skl))
& is_a_theorem(sK1_skl) )
| modus_ponens )
& ( ! [Y] :
( is_a_theorem(Y)
| ! [X] :
( ~ is_a_theorem(implies(X,Y))
| ~ is_a_theorem(X) ) )
| ~ modus_ponens ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(Y,sK0_skl),skolemize(X,sK1_skl)],[f47]) ).
fof(f49,plain,
! [X0,X1] :
( is_a_theorem(X1)
| ~ is_a_theorem(implies(X0,X1))
| ~ is_a_theorem(X0)
| ~ modus_ponens ),
inference(cnf_transformation,[status(thm)],[f48]) ).
fof(f91,plain,
( ( ? [X,Y] : ~ is_a_theorem(implies(Y,or(X,Y)))
| or_2 )
& ( ! [X,Y] : is_a_theorem(implies(Y,or(X,Y)))
| ~ or_2 ) ),
inference(NNF_transformation,[status(thm)],[f11]) ).
fof(f92,plain,
( ( ~ is_a_theorem(implies(sK22_skl,or(sK21_skl,sK22_skl)))
| or_2 )
& ( ! [X,Y] : is_a_theorem(implies(Y,or(X,Y)))
| ~ or_2 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK21_skl,sK22_skl]),skolemize(X,sK21_skl),skolemize(Y,sK22_skl)],[f91]) ).
fof(f94,plain,
( ~ is_a_theorem(implies(sK22_skl,or(sK21_skl,sK22_skl)))
| or_2 ),
inference(cnf_transformation,[status(thm)],[f92]) ).
fof(f123,plain,
( ( ? [P,Q,R] : ~ is_a_theorem(implies(implies(P,Q),implies(implies(Q,R),implies(P,R))))
| cn1 )
& ( ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(implies(Q,R),implies(P,R))))
| ~ cn1 ) ),
inference(NNF_transformation,[status(thm)],[f19]) ).
fof(f124,plain,
( ( ~ is_a_theorem(implies(implies(sK38_skl,sK39_skl),implies(implies(sK39_skl,sK40_skl),implies(sK38_skl,sK40_skl))))
| cn1 )
& ( ! [P,Q,R] : is_a_theorem(implies(implies(P,Q),implies(implies(Q,R),implies(P,R))))
| ~ cn1 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK38_skl,sK39_skl,sK40_skl]),skolemize(P,sK38_skl),skolemize(Q,sK39_skl),skolemize(R,sK40_skl)],[f123]) ).
fof(f125,plain,
! [X0,X1,X2] :
( is_a_theorem(implies(implies(X0,X1),implies(implies(X1,X2),implies(X0,X2))))
| ~ cn1 ),
inference(cnf_transformation,[status(thm)],[f124]) ).
fof(f127,plain,
( ( ? [P,Q] : ~ is_a_theorem(implies(P,implies(not(P),Q)))
| cn2 )
& ( ! [P,Q] : is_a_theorem(implies(P,implies(not(P),Q)))
| ~ cn2 ) ),
inference(NNF_transformation,[status(thm)],[f20]) ).
fof(f128,plain,
( ( ~ is_a_theorem(implies(sK41_skl,implies(not(sK41_skl),sK42_skl)))
| cn2 )
& ( ! [P,Q] : is_a_theorem(implies(P,implies(not(P),Q)))
| ~ cn2 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK41_skl,sK42_skl]),skolemize(P,sK41_skl),skolemize(Q,sK42_skl)],[f127]) ).
fof(f129,plain,
! [X0,X1] :
( is_a_theorem(implies(X0,implies(not(X0),X1)))
| ~ cn2 ),
inference(cnf_transformation,[status(thm)],[f128]) ).
fof(f131,plain,
( ( ? [P] : ~ is_a_theorem(implies(implies(not(P),P),P))
| cn3 )
& ( ! [P] : is_a_theorem(implies(implies(not(P),P),P))
| ~ cn3 ) ),
inference(NNF_transformation,[status(thm)],[f21]) ).
fof(f132,plain,
( ( ~ is_a_theorem(implies(implies(not(sK43_skl),sK43_skl),sK43_skl))
| cn3 )
& ( ! [P] : is_a_theorem(implies(implies(not(P),P),P))
| ~ cn3 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK43_skl]),skolemize(P,sK43_skl)],[f131]) ).
fof(f133,plain,
! [X0] :
( is_a_theorem(implies(implies(not(X0),X0),X0))
| ~ cn3 ),
inference(cnf_transformation,[status(thm)],[f132]) ).
fof(f155,plain,
( ! [X,Y] : or(X,Y) = not(and(not(X),not(Y)))
| ~ op_or ),
inference(pre_NNF_transformation,[status(thm)],[f27]) ).
fof(f156,plain,
! [X0,X1] :
( or(X0,X1) = not(and(not(X0),not(X1)))
| ~ op_or ),
inference(cnf_transformation,[status(thm)],[f155]) ).
fof(f159,plain,
( ! [X,Y] : implies(X,Y) = not(and(X,not(Y)))
| ~ op_implies_and ),
inference(pre_NNF_transformation,[status(thm)],[f29]) ).
fof(f160,plain,
! [X0,X1] :
( implies(X0,X1) = not(and(X0,not(X1)))
| ~ op_implies_and ),
inference(cnf_transformation,[status(thm)],[f159]) ).
fof(f165,plain,
op_or,
inference(cnf_transformation,[status(thm)],[f32]) ).
fof(f168,plain,
modus_ponens,
inference(cnf_transformation,[status(thm)],[f35]) ).
fof(f169,plain,
cn1,
inference(cnf_transformation,[status(thm)],[f36]) ).
fof(f170,plain,
cn2,
inference(cnf_transformation,[status(thm)],[f37]) ).
fof(f171,plain,
cn3,
inference(cnf_transformation,[status(thm)],[f38]) ).
fof(f174,plain,
op_implies_and,
inference(cnf_transformation,[status(thm)],[f41]) ).
fof(f176,plain,
~ or_2,
inference(cnf_transformation,[status(thm)],[f44]) ).
fof(f177,plain,
! [X0,X1] :
( is_a_theorem(X1)
| ~ is_a_theorem(implies(X0,X1))
| ~ is_a_theorem(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f49,f168]) ).
fof(f179,plain,
! [X0,X1] : is_a_theorem(implies(X0,implies(not(X0),X1))),
inference(forward_subsumption_resolution,[status(thm)],[f129,f170]) ).
fof(f182,plain,
! [X0] : is_a_theorem(implies(implies(not(X0),X0),X0)),
inference(forward_subsumption_resolution,[status(thm)],[f133,f171]) ).
fof(f183,plain,
! [X0] :
( is_a_theorem(X0)
| ~ is_a_theorem(implies(not(X0),X0)) ),
inference(resolution,[status(thm)],[f182,f177]) ).
fof(f185,plain,
~ is_a_theorem(implies(sK22_skl,or(sK21_skl,sK22_skl))),
inference(forward_subsumption_resolution,[status(thm)],[f94,f176]) ).
fof(f186,plain,
! [X0,X1] : implies(X0,X1) = not(and(X0,not(X1))),
inference(forward_subsumption_resolution,[status(thm)],[f160,f174]) ).
fof(f191,plain,
! [X0,X1] :
( or(X0,X1) = implies(not(X0),X1)
| ~ op_or ),
inference(forward_demodulation,[status(thm)],[f186,f156]) ).
fof(f194,plain,
! [X0] :
( is_a_theorem(X0)
| ~ is_a_theorem(or(X0,X0)) ),
inference(backward_demodulation,[status(thm)],[f198,f183]) ).
fof(f195,plain,
! [X0] : is_a_theorem(implies(or(X0,X0),X0)),
inference(backward_demodulation,[status(thm)],[f198,f182]) ).
fof(f197,plain,
! [X0,X1] : is_a_theorem(implies(X0,or(X0,X1))),
inference(backward_demodulation,[status(thm)],[f198,f179]) ).
fof(f198,plain,
! [X0,X1] : or(X0,X1) = implies(not(X0),X1),
inference(forward_subsumption_resolution,[status(thm)],[f191,f165]) ).
fof(f343,plain,
! [X0,X1,X2] : is_a_theorem(implies(implies(X0,X1),implies(implies(X1,X2),implies(X0,X2)))),
inference(forward_subsumption_resolution,[status(thm)],[f125,f169]) ).
fof(f344,plain,
! [X0,X1,X2] :
( is_a_theorem(implies(implies(X1,X2),implies(X0,X2)))
| ~ is_a_theorem(implies(X0,X1)) ),
inference(resolution,[status(thm)],[f343,f177]) ).
fof(f346,plain,
! [X0,X1,X2] : is_a_theorem(implies(or(X0,X1),implies(implies(X1,X2),implies(not(X0),X2)))),
inference(paramodulation,[status(thm)],[f198,f343]) ).
fof(f352,plain,
! [X0,X1,X2] : is_a_theorem(implies(or(X0,X1),implies(implies(X1,X2),or(X0,X2)))),
inference(forward_demodulation,[status(thm)],[f198,f346]) ).
fof(f359,plain,
! [X0,X1,X2,X3] : is_a_theorem(implies(implies(implies(implies(X0,X1),implies(X2,X1)),X3),implies(implies(X2,X0),X3))),
inference(resolution,[status(thm)],[f344,f343]) ).
fof(f362,plain,
! [X0,X1] : is_a_theorem(implies(implies(X0,X1),implies(or(X0,X0),X1))),
inference(resolution,[status(thm)],[f344,f195]) ).
fof(f363,plain,
! [X0,X1,X2] : is_a_theorem(implies(implies(or(X0,X1),X2),implies(X0,X2))),
inference(resolution,[status(thm)],[f344,f197]) ).
fof(f364,plain,
! [X0,X1,X2] :
( is_a_theorem(implies(implies(X1,X2),implies(not(X0),X2)))
| ~ is_a_theorem(or(X0,X1)) ),
inference(paramodulation,[status(thm)],[f198,f344]) ).
fof(f366,plain,
! [X0,X1,X2] :
( is_a_theorem(implies(implies(X1,X2),or(X0,X2)))
| ~ is_a_theorem(or(X0,X1)) ),
inference(forward_demodulation,[status(thm)],[f198,f364]) ).
fof(f381,plain,
! [X0,X1,X2] :
( is_a_theorem(implies(X0,X2))
| ~ is_a_theorem(implies(or(X0,X1),X2)) ),
inference(resolution,[status(thm)],[f363,f177]) ).
fof(f385,plain,
! [X0,X1,X2] : is_a_theorem(implies(implies(or(not(X0),X1),X2),or(X0,X2))),
inference(paramodulation,[status(thm)],[f198,f363]) ).
fof(f433,plain,
! [X0] : is_a_theorem(implies(X0,X0)),
inference(resolution,[status(thm)],[f381,f195]) ).
fof(f678,plain,
! [X0,X1,X2] :
( is_a_theorem(or(X0,X2))
| ~ is_a_theorem(implies(or(not(X0),X1),X2)) ),
inference(resolution,[status(thm)],[f385,f177]) ).
fof(f742,plain,
! [X0,X1,X2] : is_a_theorem(implies(X0,implies(implies(X1,X2),or(X0,X2)))),
inference(resolution,[status(thm)],[f352,f381]) ).
fof(f744,plain,
! [X0,X1,X2,X3] : is_a_theorem(implies(implies(implies(implies(X0,X1),or(X2,X1)),X3),implies(or(X2,X0),X3))),
inference(resolution,[status(thm)],[f352,f344]) ).
fof(f760,plain,
! [X0,X1,X2] :
( is_a_theorem(implies(implies(X1,X2),or(X0,X2)))
| ~ is_a_theorem(X0) ),
inference(resolution,[status(thm)],[f742,f177]) ).
fof(f806,plain,
! [X0,X1,X2] : is_a_theorem(implies(implies(X0,X1),or(implies(X2,X2),X1))),
inference(resolution,[status(thm)],[f760,f433]) ).
fof(f861,plain,
! [X0,X1,X2] : is_a_theorem(implies(or(X0,X1),or(implies(X2,X2),X1))),
inference(paramodulation,[status(thm)],[f198,f806]) ).
fof(f908,plain,
! [X0,X1,X2] : is_a_theorem(implies(X0,or(implies(X1,X1),X2))),
inference(resolution,[status(thm)],[f861,f381]) ).
fof(f936,plain,
! [X0,X1,X2,X3] : is_a_theorem(implies(implies(or(implies(X0,X0),X1),X2),implies(X3,X2))),
inference(resolution,[status(thm)],[f908,f344]) ).
fof(f1903,plain,
! [X0,X1,X2,X3] :
( is_a_theorem(implies(X3,X2))
| ~ is_a_theorem(implies(or(implies(X0,X0),X1),X2)) ),
inference(resolution,[status(thm)],[f936,f177]) ).
fof(f2682,plain,
! [X0,X1] : is_a_theorem(implies(X0,implies(X1,X1))),
inference(resolution,[status(thm)],[f1903,f195]) ).
fof(f2705,plain,
! [X0,X1] : is_a_theorem(or(X0,implies(X1,X1))),
inference(resolution,[status(thm)],[f2682,f678]) ).
fof(f2709,plain,
! [X0,X1,X2] : is_a_theorem(implies(implies(implies(X0,X0),X1),implies(X2,X1))),
inference(resolution,[status(thm)],[f2682,f344]) ).
fof(f2725,plain,
! [X0,X1,X2] : is_a_theorem(implies(implies(implies(X0,X0),X1),or(X2,X1))),
inference(resolution,[status(thm)],[f2705,f366]) ).
fof(f2945,plain,
! [X0,X1,X2] :
( is_a_theorem(implies(X2,X1))
| ~ is_a_theorem(implies(implies(X0,X0),X1)) ),
inference(resolution,[status(thm)],[f2709,f177]) ).
fof(f3033,plain,
! [X0,X1] : is_a_theorem(implies(X0,implies(or(X1,X1),X1))),
inference(resolution,[status(thm)],[f2945,f362]) ).
fof(f3062,plain,
! [X0,X1,X2,X3] :
( is_a_theorem(implies(implies(X2,X0),X3))
| ~ is_a_theorem(implies(implies(implies(X0,X1),implies(X2,X1)),X3)) ),
inference(resolution,[status(thm)],[f359,f177]) ).
fof(f3183,plain,
! [X0,X1] : is_a_theorem(or(X0,implies(or(X1,X1),X1))),
inference(resolution,[status(thm)],[f3033,f678]) ).
fof(f3188,plain,
! [X0,X1,X2] : is_a_theorem(implies(implies(implies(or(X0,X0),X0),X1),implies(X2,X1))),
inference(resolution,[status(thm)],[f3033,f344]) ).
fof(f3282,plain,
! [X0,X1,X2] : is_a_theorem(implies(implies(implies(or(X0,X0),X0),X1),or(X2,X1))),
inference(resolution,[status(thm)],[f3183,f366]) ).
fof(f3426,plain,
! [X0,X1,X2,X3] :
( is_a_theorem(implies(or(X2,X0),X3))
| ~ is_a_theorem(implies(implies(implies(X0,X1),or(X2,X1)),X3)) ),
inference(resolution,[status(thm)],[f744,f177]) ).
fof(f21557,plain,
! [X0,X1,X2] : is_a_theorem(implies(implies(X0,or(X1,X1)),or(X2,implies(X0,X1)))),
inference(resolution,[status(thm)],[f3062,f3282]) ).
fof(f21560,plain,
! [X0,X1,X2] : is_a_theorem(implies(implies(X0,or(X1,X1)),implies(X2,implies(X0,X1)))),
inference(resolution,[status(thm)],[f3062,f3188]) ).
fof(f21573,plain,
! [X0,X1,X2] : is_a_theorem(implies(implies(X0,X1),or(X2,implies(X0,X1)))),
inference(resolution,[status(thm)],[f3062,f2725]) ).
fof(f21767,plain,
! [X0,X1,X2] : is_a_theorem(implies(or(X0,X1),or(X2,implies(not(X0),X1)))),
inference(paramodulation,[status(thm)],[f198,f21573]) ).
fof(f21779,plain,
! [X0,X1,X2] : is_a_theorem(implies(or(X0,X1),or(X2,or(X0,X1)))),
inference(forward_demodulation,[status(thm)],[f198,f21767]) ).
fof(f22021,plain,
! [X0,X1,X2] : is_a_theorem(implies(X0,or(X1,or(X0,X2)))),
inference(resolution,[status(thm)],[f21779,f381]) ).
fof(f22072,plain,
! [X0,X1,X2,X3] : is_a_theorem(implies(implies(or(X0,or(X1,X2)),X3),implies(X1,X3))),
inference(resolution,[status(thm)],[f22021,f344]) ).
fof(f27036,plain,
! [X0,X1,X2] : is_a_theorem(implies(or(X0,or(X1,X1)),or(X2,or(X0,X1)))),
inference(resolution,[status(thm)],[f3426,f3282]) ).
fof(f27528,plain,
! [X0,X1,X2] :
( is_a_theorem(or(X2,implies(X0,X1)))
| ~ is_a_theorem(implies(X0,or(X1,X1))) ),
inference(resolution,[status(thm)],[f21557,f177]) ).
fof(f27571,plain,
! [X0,X1,X2] :
( is_a_theorem(implies(X2,implies(X0,X1)))
| ~ is_a_theorem(implies(X0,or(X1,X1))) ),
inference(resolution,[status(thm)],[f21560,f177]) ).
fof(f28675,plain,
! [X0,X1,X2,X3] :
( is_a_theorem(implies(X1,X3))
| ~ is_a_theorem(implies(or(X0,or(X1,X2)),X3)) ),
inference(resolution,[status(thm)],[f22072,f177]) ).
fof(f38946,plain,
! [X0,X1,X2] : is_a_theorem(or(X0,implies(implies(or(not(X1),X2),X1),X1))),
inference(resolution,[status(thm)],[f27528,f385]) ).
fof(f45566,plain,
! [X0,X1] : is_a_theorem(implies(implies(or(not(X0),X1),X0),X0)),
inference(resolution,[status(thm)],[f38946,f194]) ).
fof(f45613,plain,
! [X0,X1] :
( is_a_theorem(X0)
| ~ is_a_theorem(implies(or(not(X0),X1),X0)) ),
inference(resolution,[status(thm)],[f45566,f177]) ).
fof(f53875,plain,
! [X0,X1,X2] : is_a_theorem(implies(X0,or(X1,or(X2,X0)))),
inference(resolution,[status(thm)],[f28675,f27036]) ).
fof(f54167,plain,
! [X0,X1,X2] : is_a_theorem(implies(X0,implies(X1,or(X2,X1)))),
inference(resolution,[status(thm)],[f53875,f27571]) ).
fof(f54940,plain,
! [X0,X1] : is_a_theorem(implies(X0,or(X1,X0))),
inference(resolution,[status(thm)],[f54167,f45613]) ).
fof(f55004,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[f185,f54940]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL470+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n005.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Mon Sep 21 00:34:49 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.39 % Drodi V4.1.1
% 12.69/2.12 % Refutation found
% 12.69/2.12 % SZS status Theorem for theBenchmark: Theorem is valid
% 12.69/2.12 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 13.48/2.19 % Elapsed time: 1.799930 seconds
% 13.48/2.19 % CPU time: 13.905417 seconds
% 13.48/2.19 % Total memory used: 268.690 MB
% 13.48/2.19 % Net memory used: 257.311 MB
%------------------------------------------------------------------------------