%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LCL453+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/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:07:46 PM UTC 2026
% Result : Theorem 0.15s 5.44s
% Output : CNFRefutation 0.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 33
% Syntax : Number of formulae : 117 ( 29 unt; 17 def)
% Number of atoms : 278 ( 11 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 272 ( 111 ~; 117 |; 18 &)
% ( 23 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 3 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 29 ( 27 usr; 27 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 10 con; 0-2 aty)
% Number of variables : 103 ( 91 !; 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/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,axiom,
( implies_1
<=> ! [X,Y] : is_a_theorem(implies(X,implies(Y,X))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,axiom,
( implies_2
<=> ! [X,Y] : is_a_theorem(implies(implies(X,implies(X,Y)),implies(X,Y))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,axiom,
( or_3
<=> ! [X,Y,Z] : is_a_theorem(implies(implies(X,Z),implies(implies(Y,Z),implies(or(X,Y),Z)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f21,axiom,
( cn3
<=> ! [P] : is_a_theorem(implies(implies(not(P),P),P)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f27,axiom,
( op_or
=> ! [X,Y] : or(X,Y) = not(and(not(X),not(Y))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f29,axiom,
( op_implies_and
=> ! [X,Y] : implies(X,Y) = not(and(X,not(Y))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f32,axiom,
op_or,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f33,axiom,
op_implies_and,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f35,axiom,
modus_ponens,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f36,axiom,
modus_tollens,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f37,axiom,
implies_1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f38,axiom,
implies_2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f42,axiom,
and_3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f45,axiom,
or_3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f53,conjecture,
cn3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f54,negated_conjecture,
~ cn3,
inference(negated_conjecture,[status(cth)],[f53]) ).
fof(f55,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(f56,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)],[f55]) ).
fof(f57,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)],[f56]) ).
fof(f58,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)],[f57]) ).
fof(f59,plain,
! [X0,X1] :
( is_a_theorem(X1)
| ~ is_a_theorem(implies(X0,X1))
| ~ is_a_theorem(X0)
| ~ modus_ponens ),
inference(cnf_transformation,[status(thm)],[f58]) ).
fof(f73,plain,
( ( ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,X)))
| implies_1 )
& ( ! [X,Y] : is_a_theorem(implies(X,implies(Y,X)))
| ~ implies_1 ) ),
inference(NNF_transformation,[status(thm)],[f4]) ).
fof(f74,plain,
( ( ~ is_a_theorem(implies(sK6_skl,implies(sK7_skl,sK6_skl)))
| implies_1 )
& ( ! [X,Y] : is_a_theorem(implies(X,implies(Y,X)))
| ~ implies_1 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl,sK7_skl]),skolemize(X,sK6_skl),skolemize(Y,sK7_skl)],[f73]) ).
fof(f75,plain,
! [X0,X1] :
( is_a_theorem(implies(X0,implies(X1,X0)))
| ~ implies_1 ),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f77,plain,
( ( ? [X,Y] : ~ is_a_theorem(implies(implies(X,implies(X,Y)),implies(X,Y)))
| implies_2 )
& ( ! [X,Y] : is_a_theorem(implies(implies(X,implies(X,Y)),implies(X,Y)))
| ~ implies_2 ) ),
inference(NNF_transformation,[status(thm)],[f5]) ).
fof(f78,plain,
( ( ~ is_a_theorem(implies(implies(sK8_skl,implies(sK8_skl,sK9_skl)),implies(sK8_skl,sK9_skl)))
| implies_2 )
& ( ! [X,Y] : is_a_theorem(implies(implies(X,implies(X,Y)),implies(X,Y)))
| ~ implies_2 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8_skl,sK9_skl]),skolemize(X,sK8_skl),skolemize(Y,sK9_skl)],[f77]) ).
fof(f79,plain,
! [X0,X1] :
( is_a_theorem(implies(implies(X0,implies(X0,X1)),implies(X0,X1)))
| ~ implies_2 ),
inference(cnf_transformation,[status(thm)],[f78]) ).
fof(f105,plain,
( ( ? [X,Y,Z] : ~ is_a_theorem(implies(implies(X,Z),implies(implies(Y,Z),implies(or(X,Y),Z))))
| or_3 )
& ( ! [X,Y,Z] : is_a_theorem(implies(implies(X,Z),implies(implies(Y,Z),implies(or(X,Y),Z))))
| ~ or_3 ) ),
inference(NNF_transformation,[status(thm)],[f12]) ).
fof(f106,plain,
( ( ~ is_a_theorem(implies(implies(sK23_skl,sK25_skl),implies(implies(sK24_skl,sK25_skl),implies(or(sK23_skl,sK24_skl),sK25_skl))))
| or_3 )
& ( ! [X,Y,Z] : is_a_theorem(implies(implies(X,Z),implies(implies(Y,Z),implies(or(X,Y),Z))))
| ~ or_3 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK23_skl,sK24_skl,sK25_skl]),skolemize(X,sK23_skl),skolemize(Y,sK24_skl),skolemize(Z,sK25_skl)],[f105]) ).
fof(f107,plain,
! [X0,X1,X2] :
( is_a_theorem(implies(implies(X0,X1),implies(implies(X2,X1),implies(or(X0,X2),X1))))
| ~ or_3 ),
inference(cnf_transformation,[status(thm)],[f106]) ).
fof(f141,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(f142,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)],[f141]) ).
fof(f144,plain,
( ~ is_a_theorem(implies(implies(not(sK43_skl),sK43_skl),sK43_skl))
| cn3 ),
inference(cnf_transformation,[status(thm)],[f142]) ).
fof(f165,plain,
( ! [X,Y] : or(X,Y) = not(and(not(X),not(Y)))
| ~ op_or ),
inference(pre_NNF_transformation,[status(thm)],[f27]) ).
fof(f166,plain,
! [X0,X1] :
( or(X0,X1) = not(and(not(X0),not(X1)))
| ~ op_or ),
inference(cnf_transformation,[status(thm)],[f165]) ).
fof(f169,plain,
( ! [X,Y] : implies(X,Y) = not(and(X,not(Y)))
| ~ op_implies_and ),
inference(pre_NNF_transformation,[status(thm)],[f29]) ).
fof(f170,plain,
! [X0,X1] :
( implies(X0,X1) = not(and(X0,not(X1)))
| ~ op_implies_and ),
inference(cnf_transformation,[status(thm)],[f169]) ).
fof(f175,plain,
op_or,
inference(cnf_transformation,[status(thm)],[f32]) ).
fof(f176,plain,
op_implies_and,
inference(cnf_transformation,[status(thm)],[f33]) ).
fof(f178,plain,
modus_ponens,
inference(cnf_transformation,[status(thm)],[f35]) ).
fof(f179,plain,
modus_tollens,
inference(cnf_transformation,[status(thm)],[f36]) ).
fof(f180,plain,
implies_1,
inference(cnf_transformation,[status(thm)],[f37]) ).
fof(f181,plain,
implies_2,
inference(cnf_transformation,[status(thm)],[f38]) ).
fof(f185,plain,
and_3,
inference(cnf_transformation,[status(thm)],[f42]) ).
fof(f188,plain,
or_3,
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f196,plain,
~ cn3,
inference(cnf_transformation,[status(thm)],[f54]) ).
fof(f197,definition,
( sQ0_spl
<=> modus_ponens ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f199,plain,
( sQ0_spl
| ~ modus_ponens ),
inference(component_clause,[status(thm)],[f197]) ).
fof(f200,definition,
! [X0,X1] :
( sQ1_spl
<=> ( is_a_theorem(X1)
| ~ is_a_theorem(implies(X0,X1))
| ~ is_a_theorem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f201,plain,
! [X0,X1] :
( ~ sQ1_spl
| is_a_theorem(X1)
| ~ is_a_theorem(implies(X0,X1))
| ~ is_a_theorem(X0) ),
inference(component_clause,[status(thm)],[f200]) ).
fof(f203,plain,
( sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f59,f197,f200]) ).
fof(f231,definition,
( sQ9_spl
<=> modus_tollens ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f233,plain,
( sQ9_spl
| ~ modus_tollens ),
inference(component_clause,[status(thm)],[f231]) ).
fof(f242,definition,
( sQ12_spl
<=> implies_1 ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f244,plain,
( sQ12_spl
| ~ implies_1 ),
inference(component_clause,[status(thm)],[f242]) ).
fof(f245,definition,
! [X0,X1] :
( sQ13_spl
<=> is_a_theorem(implies(X0,implies(X1,X0))) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f246,plain,
! [X0,X1] :
( ~ sQ13_spl
| is_a_theorem(implies(X0,implies(X1,X0))) ),
inference(component_clause,[status(thm)],[f245]) ).
fof(f248,plain,
( sQ13_spl
| ~ sQ12_spl ),
inference(split_clause,[status(thm)],[f75,f242,f245]) ).
fof(f253,definition,
( sQ15_spl
<=> implies_2 ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f255,plain,
( sQ15_spl
| ~ implies_2 ),
inference(component_clause,[status(thm)],[f253]) ).
fof(f256,definition,
! [X0,X1] :
( sQ16_spl
<=> is_a_theorem(implies(implies(X0,implies(X0,X1)),implies(X0,X1))) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f257,plain,
! [X0,X1] :
( ~ sQ16_spl
| is_a_theorem(implies(implies(X0,implies(X0,X1)),implies(X0,X1))) ),
inference(component_clause,[status(thm)],[f256]) ).
fof(f259,plain,
( sQ16_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f79,f253,f256]) ).
fof(f297,definition,
( sQ27_spl
<=> and_3 ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f299,plain,
( sQ27_spl
| ~ and_3 ),
inference(component_clause,[status(thm)],[f297]) ).
fof(f330,definition,
( sQ36_spl
<=> or_3 ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f332,plain,
( sQ36_spl
| ~ or_3 ),
inference(component_clause,[status(thm)],[f330]) ).
fof(f333,definition,
! [X0,X1,X2] :
( sQ37_spl
<=> is_a_theorem(implies(implies(X0,X1),implies(implies(X2,X1),implies(or(X0,X2),X1)))) ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f334,plain,
! [X0,X1,X2] :
( ~ sQ37_spl
| is_a_theorem(implies(implies(X0,X1),implies(implies(X2,X1),implies(or(X0,X2),X1)))) ),
inference(component_clause,[status(thm)],[f333]) ).
fof(f336,plain,
( sQ37_spl
| ~ sQ36_spl ),
inference(split_clause,[status(thm)],[f107,f330,f333]) ).
fof(f423,definition,
( sQ61_spl
<=> cn3 ),
introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition]) ).
fof(f424,plain,
( ~ sQ61_spl
| cn3 ),
inference(component_clause,[status(thm)],[f423]) ).
fof(f430,definition,
( sQ63_spl
<=> is_a_theorem(implies(implies(not(sK43_skl),sK43_skl),sK43_skl)) ),
introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition]) ).
fof(f432,plain,
( sQ63_spl
| ~ is_a_theorem(implies(implies(not(sK43_skl),sK43_skl),sK43_skl)) ),
inference(component_clause,[status(thm)],[f430]) ).
fof(f433,plain,
( ~ sQ63_spl
| sQ61_spl ),
inference(split_clause,[status(thm)],[f144,f423,f430]) ).
fof(f486,definition,
( sQ78_spl
<=> op_or ),
introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition]) ).
fof(f488,plain,
( sQ78_spl
| ~ op_or ),
inference(component_clause,[status(thm)],[f486]) ).
fof(f489,definition,
! [X0,X1] :
( sQ79_spl
<=> or(X0,X1) = not(and(not(X0),not(X1))) ),
introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition]) ).
fof(f490,plain,
! [X0,X1] :
( ~ sQ79_spl
| or(X0,X1) = not(and(not(X0),not(X1))) ),
inference(component_clause,[status(thm)],[f489]) ).
fof(f492,plain,
( sQ79_spl
| ~ sQ78_spl ),
inference(split_clause,[status(thm)],[f166,f486,f489]) ).
fof(f500,definition,
( sQ82_spl
<=> op_implies_and ),
introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition]) ).
fof(f502,plain,
( sQ82_spl
| ~ op_implies_and ),
inference(component_clause,[status(thm)],[f500]) ).
fof(f503,definition,
! [X0,X1] :
( sQ83_spl
<=> implies(X0,X1) = not(and(X0,not(X1))) ),
introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition]) ).
fof(f504,plain,
! [X0,X1] :
( ~ sQ83_spl
| implies(X0,X1) = not(and(X0,not(X1))) ),
inference(component_clause,[status(thm)],[f503]) ).
fof(f506,plain,
( sQ83_spl
| ~ sQ82_spl ),
inference(split_clause,[status(thm)],[f170,f500,f503]) ).
fof(f525,plain,
( sQ82_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f502,f176]) ).
fof(f526,plain,
sQ82_spl,
inference(contradiction_clause,[status(thm)],[f525]) ).
fof(f527,plain,
( sQ78_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f488,f175]) ).
fof(f528,plain,
sQ78_spl,
inference(contradiction_clause,[status(thm)],[f527]) ).
fof(f529,plain,
( sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f199,f178]) ).
fof(f530,plain,
sQ0_spl,
inference(contradiction_clause,[status(thm)],[f529]) ).
fof(f567,plain,
( sQ12_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f244,f180]) ).
fof(f568,plain,
sQ12_spl,
inference(contradiction_clause,[status(thm)],[f567]) ).
fof(f573,plain,
! [X0] :
( sQ63_spl
| ~ sQ1_spl
| ~ is_a_theorem(implies(X0,implies(implies(not(sK43_skl),sK43_skl),sK43_skl)))
| ~ is_a_theorem(X0) ),
inference(resolution,[status(thm)],[f201,f432]) ).
fof(f593,plain,
! [X0,X1] :
( ~ sQ1_spl
| sQ63_spl
| ~ is_a_theorem(implies(X1,implies(X0,implies(implies(not(sK43_skl),sK43_skl),sK43_skl))))
| ~ is_a_theorem(X1)
| ~ is_a_theorem(X0) ),
inference(resolution,[status(thm)],[f573,f201]) ).
fof(f643,plain,
( sQ36_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f332,f188]) ).
fof(f644,plain,
sQ36_spl,
inference(contradiction_clause,[status(thm)],[f643]) ).
fof(f694,plain,
( ~ sQ61_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f424,f196]) ).
fof(f695,plain,
~ sQ61_spl,
inference(contradiction_clause,[status(thm)],[f694]) ).
fof(f698,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ sQ16_spl
| is_a_theorem(implies(X0,X1))
| ~ is_a_theorem(implies(X0,implies(X0,X1))) ),
inference(resolution,[status(thm)],[f257,f201]) ).
fof(f700,plain,
( sQ15_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f255,f181]) ).
fof(f701,plain,
sQ15_spl,
inference(contradiction_clause,[status(thm)],[f700]) ).
fof(f724,plain,
( sQ27_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f299,f185]) ).
fof(f725,plain,
sQ27_spl,
inference(contradiction_clause,[status(thm)],[f724]) ).
fof(f734,plain,
( sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f233,f179]) ).
fof(f735,plain,
sQ9_spl,
inference(contradiction_clause,[status(thm)],[f734]) ).
fof(f739,plain,
! [X0,X1] :
( ~ sQ79_spl
| ~ sQ83_spl
| or(X0,X1) = implies(not(X0),X1) ),
inference(forward_demodulation,[status(thm)],[f504,f490]) ).
fof(f881,plain,
! [X0,X1] :
( ~ sQ1_spl
| sQ63_spl
| ~ sQ79_spl
| ~ sQ83_spl
| ~ is_a_theorem(implies(X1,implies(X0,implies(or(sK43_skl,sK43_skl),sK43_skl))))
| ~ is_a_theorem(X1)
| ~ is_a_theorem(X0) ),
inference(forward_demodulation,[status(thm)],[f739,f593]) ).
fof(f1006,plain,
( ~ sQ1_spl
| sQ63_spl
| ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ37_spl
| ~ is_a_theorem(implies(sK43_skl,sK43_skl))
| ~ is_a_theorem(implies(sK43_skl,sK43_skl)) ),
inference(resolution,[status(thm)],[f334,f881]) ).
fof(f1010,definition,
( sQ103_spl
<=> is_a_theorem(implies(sK43_skl,sK43_skl)) ),
introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition]) ).
fof(f1012,plain,
( sQ103_spl
| ~ is_a_theorem(implies(sK43_skl,sK43_skl)) ),
inference(component_clause,[status(thm)],[f1010]) ).
fof(f1013,plain,
( ~ sQ1_spl
| sQ63_spl
| ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ37_spl
| ~ sQ103_spl ),
inference(split_clause,[status(thm)],[f1006,f1010,f333,f503,f489,f430,f200]) ).
fof(f1060,plain,
! [X0] :
( ~ sQ13_spl
| ~ sQ1_spl
| ~ sQ16_spl
| is_a_theorem(implies(X0,X0)) ),
inference(resolution,[status(thm)],[f698,f246]) ).
fof(f1069,plain,
( sQ103_spl
| ~ sQ13_spl
| ~ sQ1_spl
| ~ sQ16_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f1012,f1060]) ).
fof(f1086,plain,
( sQ103_spl
| ~ sQ13_spl
| ~ sQ1_spl
| ~ sQ16_spl ),
inference(contradiction_clause,[status(thm)],[f1069]) ).
fof(f1087,plain,
$false,
inference(sat_refutation,[status(thm)],[f203,f248,f259,f336,f433,f492,f506,f526,f528,f530,f568,f644,f695,f701,f725,f735,f1013,f1086]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL453+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/5.38 % Computer : n017.cluster.edu
% 0.10/5.38 % Model : x86_64 x86_64
% 0.10/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.38 % Memory : 8046.5625MB
% 0.10/5.38 % OS : Linux 6.8.0-71-generic
% 0.10/5.38 % CPULimit : 300
% 0.10/5.38 % WCLimit : 300
% 0.10/5.38 % DateTime : Mon Sep 21 00:28:47 UTC 2026
% 0.10/5.38 % CPUTime :
% 0.10/5.39 % Drodi V4.1.1
% 0.15/5.44 % Refutation found
% 0.15/5.44 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.15/5.44 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.15/5.48 % Elapsed time: 0.082865 seconds
% 0.15/5.48 % CPU time: 0.366090 seconds
% 0.15/5.48 % Total memory used: 88.254 MB
% 0.15/5.48 % Net memory used: 88.003 MB
%------------------------------------------------------------------------------