%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LCL498+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 : n019.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:51 PM UTC 2026
% Result : Theorem 6.34s 1.48s
% Output : CNFRefutation 6.34s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 33
% Syntax : Number of formulae : 131 ( 26 unt; 17 def)
% Number of atoms : 358 ( 5 equ)
% Maximal formula atoms : 10 ( 2 avg)
% Number of connectives : 400 ( 173 ~; 178 |; 22 &)
% ( 25 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 28 ( 26 usr; 26 prp; 0-2 aty)
% Number of functors : 17 ( 17 usr; 14 con; 0-2 aty)
% Number of variables : 148 ( 132 !; 16 ?)
% 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(f21,axiom,
( cn3
<=> ! [P] : is_a_theorem(implies(implies(not(P),P),P)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f22,axiom,
( r1
<=> ! [P] : is_a_theorem(implies(or(P,P),P)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f23,axiom,
( r2
<=> ! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f24,axiom,
( r3
<=> ! [P,Q] : is_a_theorem(implies(or(P,Q),or(Q,P))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f25,axiom,
( r4
<=> ! [P,Q,R] : is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f26,axiom,
( r5
<=> ! [P,Q,R] : is_a_theorem(implies(implies(Q,R),implies(or(P,Q),or(P,R)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f30,axiom,
( op_implies_or
=> ! [X,Y] : implies(X,Y) = or(not(X),Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f32,axiom,
op_implies_or,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f35,axiom,
modus_ponens,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f36,axiom,
r1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f37,axiom,
r2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f38,axiom,
r3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f39,axiom,
r4,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f40,axiom,
r5,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f45,conjecture,
cn3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f46,negated_conjecture,
~ cn3,
inference(negated_conjecture,[status(cth)],[f45]) ).
fof(f47,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(f48,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)],[f47]) ).
fof(f49,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)],[f48]) ).
fof(f50,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)],[f49]) ).
fof(f51,plain,
! [X0,X1] :
( is_a_theorem(X1)
| ~ is_a_theorem(implies(X0,X1))
| ~ is_a_theorem(X0)
| ~ modus_ponens ),
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f133,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(f134,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)],[f133]) ).
fof(f136,plain,
( ~ is_a_theorem(implies(implies(not(sK43_skl),sK43_skl),sK43_skl))
| cn3 ),
inference(cnf_transformation,[status(thm)],[f134]) ).
fof(f137,plain,
( ( ? [P] : ~ is_a_theorem(implies(or(P,P),P))
| r1 )
& ( ! [P] : is_a_theorem(implies(or(P,P),P))
| ~ r1 ) ),
inference(NNF_transformation,[status(thm)],[f22]) ).
fof(f138,plain,
( ( ~ is_a_theorem(implies(or(sK44_skl,sK44_skl),sK44_skl))
| r1 )
& ( ! [P] : is_a_theorem(implies(or(P,P),P))
| ~ r1 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK44_skl]),skolemize(P,sK44_skl)],[f137]) ).
fof(f139,plain,
! [X0] :
( is_a_theorem(implies(or(X0,X0),X0))
| ~ r1 ),
inference(cnf_transformation,[status(thm)],[f138]) ).
fof(f141,plain,
( ( ? [P,Q] : ~ is_a_theorem(implies(Q,or(P,Q)))
| r2 )
& ( ! [P,Q] : is_a_theorem(implies(Q,or(P,Q)))
| ~ r2 ) ),
inference(NNF_transformation,[status(thm)],[f23]) ).
fof(f142,plain,
( ( ~ is_a_theorem(implies(sK46_skl,or(sK45_skl,sK46_skl)))
| r2 )
& ( ! [P,Q] : is_a_theorem(implies(Q,or(P,Q)))
| ~ r2 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK45_skl,sK46_skl]),skolemize(P,sK45_skl),skolemize(Q,sK46_skl)],[f141]) ).
fof(f143,plain,
! [X0,X1] :
( is_a_theorem(implies(X0,or(X1,X0)))
| ~ r2 ),
inference(cnf_transformation,[status(thm)],[f142]) ).
fof(f145,plain,
( ( ? [P,Q] : ~ is_a_theorem(implies(or(P,Q),or(Q,P)))
| r3 )
& ( ! [P,Q] : is_a_theorem(implies(or(P,Q),or(Q,P)))
| ~ r3 ) ),
inference(NNF_transformation,[status(thm)],[f24]) ).
fof(f146,plain,
( ( ~ is_a_theorem(implies(or(sK47_skl,sK48_skl),or(sK48_skl,sK47_skl)))
| r3 )
& ( ! [P,Q] : is_a_theorem(implies(or(P,Q),or(Q,P)))
| ~ r3 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK47_skl,sK48_skl]),skolemize(P,sK47_skl),skolemize(Q,sK48_skl)],[f145]) ).
fof(f147,plain,
! [X0,X1] :
( is_a_theorem(implies(or(X0,X1),or(X1,X0)))
| ~ r3 ),
inference(cnf_transformation,[status(thm)],[f146]) ).
fof(f149,plain,
( ( ? [P,Q,R] : ~ is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R))))
| r4 )
& ( ! [P,Q,R] : is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R))))
| ~ r4 ) ),
inference(NNF_transformation,[status(thm)],[f25]) ).
fof(f150,plain,
( ( ~ is_a_theorem(implies(or(sK49_skl,or(sK50_skl,sK51_skl)),or(sK50_skl,or(sK49_skl,sK51_skl))))
| r4 )
& ( ! [P,Q,R] : is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R))))
| ~ r4 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK49_skl,sK50_skl,sK51_skl]),skolemize(P,sK49_skl),skolemize(Q,sK50_skl),skolemize(R,sK51_skl)],[f149]) ).
fof(f151,plain,
! [X0,X1,X2] :
( is_a_theorem(implies(or(X0,or(X1,X2)),or(X1,or(X0,X2))))
| ~ r4 ),
inference(cnf_transformation,[status(thm)],[f150]) ).
fof(f153,plain,
( ( ? [P,Q,R] : ~ is_a_theorem(implies(implies(Q,R),implies(or(P,Q),or(P,R))))
| r5 )
& ( ! [P,Q,R] : is_a_theorem(implies(implies(Q,R),implies(or(P,Q),or(P,R))))
| ~ r5 ) ),
inference(NNF_transformation,[status(thm)],[f26]) ).
fof(f154,plain,
( ( ~ is_a_theorem(implies(implies(sK53_skl,sK54_skl),implies(or(sK52_skl,sK53_skl),or(sK52_skl,sK54_skl))))
| r5 )
& ( ! [P,Q,R] : is_a_theorem(implies(implies(Q,R),implies(or(P,Q),or(P,R))))
| ~ r5 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK52_skl,sK53_skl,sK54_skl]),skolemize(P,sK52_skl),skolemize(Q,sK53_skl),skolemize(R,sK54_skl)],[f153]) ).
fof(f155,plain,
! [X0,X1,X2] :
( is_a_theorem(implies(implies(X0,X1),implies(or(X2,X0),or(X2,X1))))
| ~ r5 ),
inference(cnf_transformation,[status(thm)],[f154]) ).
fof(f163,plain,
( ! [X,Y] : implies(X,Y) = or(not(X),Y)
| ~ op_implies_or ),
inference(pre_NNF_transformation,[status(thm)],[f30]) ).
fof(f164,plain,
! [X0,X1] :
( implies(X0,X1) = or(not(X0),X1)
| ~ op_implies_or ),
inference(cnf_transformation,[status(thm)],[f163]) ).
fof(f167,plain,
op_implies_or,
inference(cnf_transformation,[status(thm)],[f32]) ).
fof(f170,plain,
modus_ponens,
inference(cnf_transformation,[status(thm)],[f35]) ).
fof(f171,plain,
r1,
inference(cnf_transformation,[status(thm)],[f36]) ).
fof(f172,plain,
r2,
inference(cnf_transformation,[status(thm)],[f37]) ).
fof(f173,plain,
r3,
inference(cnf_transformation,[status(thm)],[f38]) ).
fof(f174,plain,
r4,
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f175,plain,
r5,
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f180,plain,
~ cn3,
inference(cnf_transformation,[status(thm)],[f46]) ).
fof(f181,definition,
( sQ0_spl
<=> modus_ponens ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f183,plain,
( sQ0_spl
| ~ modus_ponens ),
inference(component_clause,[status(thm)],[f181]) ).
fof(f184,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(f185,plain,
! [X0,X1] :
( ~ sQ1_spl
| is_a_theorem(X1)
| ~ is_a_theorem(implies(X0,X1))
| ~ is_a_theorem(X0) ),
inference(component_clause,[status(thm)],[f184]) ).
fof(f187,plain,
( sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f51,f181,f184]) ).
fof(f229,definition,
! [X0,X1] :
( sQ13_spl
<=> is_a_theorem(implies(X0,implies(X1,X0))) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f230,plain,
! [X0,X1] :
( ~ sQ13_spl
| is_a_theorem(implies(X0,implies(X1,X0))) ),
inference(component_clause,[status(thm)],[f229]) ).
fof(f306,definition,
! [X0,X1] :
( sQ34_spl
<=> is_a_theorem(implies(X0,or(X1,X0))) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f307,plain,
! [X0,X1] :
( ~ sQ34_spl
| is_a_theorem(implies(X0,or(X1,X0))) ),
inference(component_clause,[status(thm)],[f306]) ).
fof(f407,definition,
( sQ61_spl
<=> cn3 ),
introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition]) ).
fof(f408,plain,
( ~ sQ61_spl
| cn3 ),
inference(component_clause,[status(thm)],[f407]) ).
fof(f414,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(f416,plain,
( sQ63_spl
| ~ is_a_theorem(implies(implies(not(sK43_skl),sK43_skl),sK43_skl)) ),
inference(component_clause,[status(thm)],[f414]) ).
fof(f417,plain,
( ~ sQ63_spl
| sQ61_spl ),
inference(split_clause,[status(thm)],[f136,f407,f414]) ).
fof(f418,definition,
( sQ64_spl
<=> r1 ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f420,plain,
( sQ64_spl
| ~ r1 ),
inference(component_clause,[status(thm)],[f418]) ).
fof(f421,definition,
! [X0] :
( sQ65_spl
<=> is_a_theorem(implies(or(X0,X0),X0)) ),
introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition]) ).
fof(f422,plain,
! [X0] :
( ~ sQ65_spl
| is_a_theorem(implies(or(X0,X0),X0)) ),
inference(component_clause,[status(thm)],[f421]) ).
fof(f424,plain,
( sQ65_spl
| ~ sQ64_spl ),
inference(split_clause,[status(thm)],[f139,f418,f421]) ).
fof(f429,definition,
( sQ67_spl
<=> r2 ),
introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition]) ).
fof(f431,plain,
( sQ67_spl
| ~ r2 ),
inference(component_clause,[status(thm)],[f429]) ).
fof(f432,plain,
( sQ34_spl
| ~ sQ67_spl ),
inference(split_clause,[status(thm)],[f143,f429,f306]) ).
fof(f437,definition,
( sQ69_spl
<=> r3 ),
introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition]) ).
fof(f439,plain,
( sQ69_spl
| ~ r3 ),
inference(component_clause,[status(thm)],[f437]) ).
fof(f440,definition,
! [X0,X1] :
( sQ70_spl
<=> is_a_theorem(implies(or(X0,X1),or(X1,X0))) ),
introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition]) ).
fof(f441,plain,
! [X0,X1] :
( ~ sQ70_spl
| is_a_theorem(implies(or(X0,X1),or(X1,X0))) ),
inference(component_clause,[status(thm)],[f440]) ).
fof(f443,plain,
( sQ70_spl
| ~ sQ69_spl ),
inference(split_clause,[status(thm)],[f147,f437,f440]) ).
fof(f448,definition,
( sQ72_spl
<=> r4 ),
introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition]) ).
fof(f450,plain,
( sQ72_spl
| ~ r4 ),
inference(component_clause,[status(thm)],[f448]) ).
fof(f451,definition,
! [X0,X1,X2] :
( sQ73_spl
<=> is_a_theorem(implies(or(X0,or(X1,X2)),or(X1,or(X0,X2)))) ),
introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition]) ).
fof(f452,plain,
! [X0,X1,X2] :
( ~ sQ73_spl
| is_a_theorem(implies(or(X0,or(X1,X2)),or(X1,or(X0,X2)))) ),
inference(component_clause,[status(thm)],[f451]) ).
fof(f454,plain,
( sQ73_spl
| ~ sQ72_spl ),
inference(split_clause,[status(thm)],[f151,f448,f451]) ).
fof(f459,definition,
( sQ75_spl
<=> r5 ),
introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition]) ).
fof(f461,plain,
( sQ75_spl
| ~ r5 ),
inference(component_clause,[status(thm)],[f459]) ).
fof(f462,definition,
! [X0,X1,X2] :
( sQ76_spl
<=> is_a_theorem(implies(implies(X0,X1),implies(or(X2,X0),or(X2,X1)))) ),
introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition]) ).
fof(f463,plain,
! [X0,X1,X2] :
( ~ sQ76_spl
| is_a_theorem(implies(implies(X0,X1),implies(or(X2,X0),or(X2,X1)))) ),
inference(component_clause,[status(thm)],[f462]) ).
fof(f465,plain,
( sQ76_spl
| ~ sQ75_spl ),
inference(split_clause,[status(thm)],[f155,f459,f462]) ).
fof(f491,definition,
( sQ84_spl
<=> op_implies_or ),
introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition]) ).
fof(f493,plain,
( sQ84_spl
| ~ op_implies_or ),
inference(component_clause,[status(thm)],[f491]) ).
fof(f494,definition,
! [X0,X1] :
( sQ85_spl
<=> implies(X0,X1) = or(not(X0),X1) ),
introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition]) ).
fof(f495,plain,
! [X0,X1] :
( ~ sQ85_spl
| implies(X0,X1) = or(not(X0),X1) ),
inference(component_clause,[status(thm)],[f494]) ).
fof(f497,plain,
( sQ85_spl
| ~ sQ84_spl ),
inference(split_clause,[status(thm)],[f164,f491,f494]) ).
fof(f509,plain,
( sQ84_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f493,f167]) ).
fof(f510,plain,
sQ84_spl,
inference(contradiction_clause,[status(thm)],[f509]) ).
fof(f515,plain,
( sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f183,f170]) ).
fof(f516,plain,
sQ0_spl,
inference(contradiction_clause,[status(thm)],[f515]) ).
fof(f521,plain,
( sQ75_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f461,f175]) ).
fof(f522,plain,
sQ75_spl,
inference(contradiction_clause,[status(thm)],[f521]) ).
fof(f530,plain,
( sQ67_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f431,f172]) ).
fof(f531,plain,
sQ67_spl,
inference(contradiction_clause,[status(thm)],[f530]) ).
fof(f532,plain,
! [X0,X1] :
( ~ sQ85_spl
| ~ sQ34_spl
| is_a_theorem(implies(X0,implies(X1,X0))) ),
inference(paramodulation,[status(thm)],[f495,f307]) ).
fof(f535,plain,
( sQ64_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f420,f171]) ).
fof(f536,plain,
sQ64_spl,
inference(contradiction_clause,[status(thm)],[f535]) ).
fof(f541,plain,
! [X0,X1,X2] :
( ~ sQ85_spl
| ~ sQ73_spl
| is_a_theorem(implies(implies(X0,or(X1,X2)),or(X1,or(not(X0),X2)))) ),
inference(paramodulation,[status(thm)],[f495,f452]) ).
fof(f546,plain,
( sQ72_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f450,f174]) ).
fof(f547,plain,
sQ72_spl,
inference(contradiction_clause,[status(thm)],[f546]) ).
fof(f548,plain,
! [X0,X1,X2] :
( ~ sQ85_spl
| ~ sQ73_spl
| is_a_theorem(implies(implies(X0,or(X1,X2)),or(X1,implies(X0,X2)))) ),
inference(forward_demodulation,[status(thm)],[f495,f541]) ).
fof(f554,plain,
( sQ69_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f439,f173]) ).
fof(f555,plain,
sQ69_spl,
inference(contradiction_clause,[status(thm)],[f554]) ).
fof(f580,plain,
( ~ sQ85_spl
| ~ sQ34_spl
| sQ13_spl ),
inference(split_clause,[status(thm)],[f532,f229,f306,f494]) ).
fof(f586,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)],[f185,f416]) ).
fof(f597,plain,
( ~ sQ65_spl
| sQ63_spl
| ~ sQ1_spl
| ~ is_a_theorem(or(implies(implies(not(sK43_skl),sK43_skl),sK43_skl),implies(implies(not(sK43_skl),sK43_skl),sK43_skl))) ),
inference(resolution,[status(thm)],[f586,f422]) ).
fof(f603,plain,
! [X0] :
( ~ sQ1_spl
| ~ sQ65_spl
| sQ63_spl
| ~ is_a_theorem(implies(X0,or(implies(implies(not(sK43_skl),sK43_skl),sK43_skl),implies(implies(not(sK43_skl),sK43_skl),sK43_skl))))
| ~ is_a_theorem(X0) ),
inference(resolution,[status(thm)],[f597,f185]) ).
fof(f651,plain,
( ~ sQ61_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f408,f180]) ).
fof(f652,plain,
~ sQ61_spl,
inference(contradiction_clause,[status(thm)],[f651]) ).
fof(f658,plain,
! [X0] :
( ~ sQ65_spl
| ~ sQ1_spl
| is_a_theorem(X0)
| ~ is_a_theorem(or(X0,X0)) ),
inference(resolution,[status(thm)],[f185,f422]) ).
fof(f692,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ sQ70_spl
| is_a_theorem(or(X1,X0))
| ~ is_a_theorem(or(X0,X1)) ),
inference(resolution,[status(thm)],[f441,f185]) ).
fof(f704,plain,
! [X0,X1,X2] :
( ~ sQ1_spl
| ~ sQ76_spl
| is_a_theorem(implies(or(X2,X0),or(X2,X1)))
| ~ is_a_theorem(implies(X0,X1)) ),
inference(resolution,[status(thm)],[f463,f185]) ).
fof(f813,plain,
! [X0,X1] :
( ~ sQ85_spl
| ~ sQ1_spl
| ~ sQ70_spl
| is_a_theorem(or(X1,not(X0)))
| ~ is_a_theorem(implies(X0,X1)) ),
inference(paramodulation,[status(thm)],[f495,f692]) ).
fof(f1065,plain,
! [X0,X1] :
( ~ sQ13_spl
| ~ sQ85_spl
| ~ sQ1_spl
| ~ sQ70_spl
| is_a_theorem(or(implies(X0,X1),not(X1))) ),
inference(resolution,[status(thm)],[f813,f230]) ).
fof(f1196,plain,
! [X0,X1,X2] :
( ~ sQ1_spl
| ~ sQ85_spl
| ~ sQ73_spl
| is_a_theorem(or(X1,implies(X0,X2)))
| ~ is_a_theorem(implies(X0,or(X1,X2))) ),
inference(resolution,[status(thm)],[f548,f185]) ).
fof(f3252,plain,
! [X0] :
( ~ sQ1_spl
| ~ sQ65_spl
| sQ63_spl
| ~ sQ76_spl
| ~ is_a_theorem(or(implies(implies(not(sK43_skl),sK43_skl),sK43_skl),X0))
| ~ is_a_theorem(implies(X0,implies(implies(not(sK43_skl),sK43_skl),sK43_skl))) ),
inference(resolution,[status(thm)],[f704,f603]) ).
fof(f5307,plain,
! [X0,X1] :
( ~ sQ34_spl
| ~ sQ1_spl
| ~ sQ85_spl
| ~ sQ73_spl
| is_a_theorem(or(X0,implies(X1,X1))) ),
inference(resolution,[status(thm)],[f1196,f307]) ).
fof(f5380,plain,
! [X0] :
( ~ sQ65_spl
| ~ sQ1_spl
| ~ sQ34_spl
| ~ sQ85_spl
| ~ sQ73_spl
| is_a_theorem(implies(X0,X0)) ),
inference(resolution,[status(thm)],[f5307,f658]) ).
fof(f5412,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ sQ85_spl
| ~ sQ73_spl
| ~ sQ65_spl
| ~ sQ34_spl
| is_a_theorem(or(X0,implies(or(X0,X1),X1))) ),
inference(resolution,[status(thm)],[f5380,f1196]) ).
fof(f6023,plain,
! [X0,X1] :
( ~ sQ85_spl
| ~ sQ1_spl
| ~ sQ73_spl
| ~ sQ65_spl
| ~ sQ34_spl
| is_a_theorem(implies(X0,implies(or(not(X0),X1),X1))) ),
inference(paramodulation,[status(thm)],[f495,f5412]) ).
fof(f6025,plain,
! [X0,X1] :
( ~ sQ85_spl
| ~ sQ1_spl
| ~ sQ73_spl
| ~ sQ65_spl
| ~ sQ34_spl
| is_a_theorem(implies(X0,implies(implies(X0,X1),X1))) ),
inference(forward_demodulation,[status(thm)],[f495,f6023]) ).
fof(f6400,plain,
( ~ sQ1_spl
| ~ sQ65_spl
| sQ63_spl
| ~ sQ76_spl
| ~ sQ85_spl
| ~ sQ73_spl
| ~ sQ34_spl
| ~ is_a_theorem(or(implies(implies(not(sK43_skl),sK43_skl),sK43_skl),not(sK43_skl))) ),
inference(resolution,[status(thm)],[f6025,f3252]) ).
fof(f6415,plain,
( ~ sQ1_spl
| ~ sQ65_spl
| sQ63_spl
| ~ sQ76_spl
| ~ sQ85_spl
| ~ sQ73_spl
| ~ sQ34_spl
| ~ sQ13_spl
| ~ sQ70_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f6400,f1065]) ).
fof(f6416,plain,
( ~ sQ1_spl
| ~ sQ65_spl
| sQ63_spl
| ~ sQ76_spl
| ~ sQ85_spl
| ~ sQ73_spl
| ~ sQ34_spl
| ~ sQ13_spl
| ~ sQ70_spl ),
inference(contradiction_clause,[status(thm)],[f6415]) ).
fof(f6417,plain,
$false,
inference(sat_refutation,[status(thm)],[f187,f417,f424,f432,f443,f454,f465,f497,f510,f516,f522,f531,f536,f547,f555,f580,f652,f6416]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL498+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/0.37 % Computer : n019.cluster.edu
% 0.12/0.37 % Model : x86_64 x86_64
% 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.37 % Memory : 8046.5625MB
% 0.12/0.37 % OS : Linux 6.8.0-71-generic
% 0.12/0.37 % CPULimit : 300
% 0.12/0.37 % WCLimit : 300
% 0.12/0.37 % DateTime : Mon Sep 21 00:36:21 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.39 % Drodi V4.1.1
% 6.34/1.48 % Refutation found
% 6.34/1.48 % SZS status Theorem for theBenchmark: Theorem is valid
% 6.34/1.48 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 5.53/1.54 % Elapsed time: 1.146705 seconds
% 5.53/1.54 % CPU time: 8.756064 seconds
% 5.53/1.54 % Total memory used: 238.102 MB
% 5.53/1.54 % Net memory used: 230.587 MB
%------------------------------------------------------------------------------