%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LCL487+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 : 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:50 PM UTC 2026
% Result : Theorem 15.67s 2.45s
% Output : CNFRefutation 15.67s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 41
% Syntax : Number of formulae : 150 ( 29 unt; 22 def)
% Number of atoms : 374 ( 23 equ)
% Maximal formula atoms : 9 ( 2 avg)
% Number of connectives : 387 ( 163 ~; 170 |; 20 &)
% ( 29 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 35 ( 33 usr; 33 prp; 0-2 aty)
% Number of functors : 17 ( 17 usr; 13 con; 0-2 aty)
% Number of variables : 168 ( 153 !; 15 ?)
% 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(f7,axiom,
( and_1
<=> ! [X,Y] : is_a_theorem(implies(and(X,Y),X)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f17,axiom,
( kn2
<=> ! [P,Q] : is_a_theorem(implies(and(P,Q),P)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f23,axiom,
( r2
<=> ! [P,Q] : is_a_theorem(implies(Q,or(P,Q))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f24,axiom,
( r3
<=> ! [P,Q] : is_a_theorem(implies(or(P,Q),or(Q,P))) ),
file('/export/starexec/sandbox2/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/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(f28,axiom,
( op_and
=> ! [X,Y] : and(X,Y) = not(or(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(f30,axiom,
( op_implies_or
=> ! [X,Y] : implies(X,Y) = or(not(X),Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f32,axiom,
op_implies_or,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f33,axiom,
op_and,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f35,axiom,
modus_ponens,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f37,axiom,
r2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f38,axiom,
r3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f40,axiom,
r5,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f42,axiom,
op_or,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f43,axiom,
op_implies_and,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f45,conjecture,
and_1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f46,negated_conjecture,
~ and_1,
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(f77,plain,
( ( ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),X))
| and_1 )
& ( ! [X,Y] : is_a_theorem(implies(and(X,Y),X))
| ~ and_1 ) ),
inference(NNF_transformation,[status(thm)],[f7]) ).
fof(f78,plain,
( ( ~ is_a_theorem(implies(and(sK13_skl,sK14_skl),sK13_skl))
| and_1 )
& ( ! [X,Y] : is_a_theorem(implies(and(X,Y),X))
| ~ and_1 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl,sK14_skl]),skolemize(X,sK13_skl),skolemize(Y,sK14_skl)],[f77]) ).
fof(f80,plain,
( ~ is_a_theorem(implies(and(sK13_skl,sK14_skl),sK13_skl))
| and_1 ),
inference(cnf_transformation,[status(thm)],[f78]) ).
fof(f117,plain,
( ( ? [P,Q] : ~ is_a_theorem(implies(and(P,Q),P))
| kn2 )
& ( ! [P,Q] : is_a_theorem(implies(and(P,Q),P))
| ~ kn2 ) ),
inference(NNF_transformation,[status(thm)],[f17]) ).
fof(f118,plain,
( ( ~ is_a_theorem(implies(and(sK33_skl,sK34_skl),sK33_skl))
| kn2 )
& ( ! [P,Q] : is_a_theorem(implies(and(P,Q),P))
| ~ kn2 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK33_skl,sK34_skl]),skolemize(P,sK33_skl),skolemize(Q,sK34_skl)],[f117]) ).
fof(f119,plain,
! [X0,X1] :
( is_a_theorem(implies(and(X0,X1),X0))
| ~ kn2 ),
inference(cnf_transformation,[status(thm)],[f118]) ).
fof(f120,plain,
( ~ is_a_theorem(implies(and(sK33_skl,sK34_skl),sK33_skl))
| kn2 ),
inference(cnf_transformation,[status(thm)],[f118]) ).
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(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(f157,plain,
( ! [X,Y] : or(X,Y) = not(and(not(X),not(Y)))
| ~ op_or ),
inference(pre_NNF_transformation,[status(thm)],[f27]) ).
fof(f158,plain,
! [X0,X1] :
( or(X0,X1) = not(and(not(X0),not(X1)))
| ~ op_or ),
inference(cnf_transformation,[status(thm)],[f157]) ).
fof(f159,plain,
( ! [X,Y] : and(X,Y) = not(or(not(X),not(Y)))
| ~ op_and ),
inference(pre_NNF_transformation,[status(thm)],[f28]) ).
fof(f160,plain,
! [X0,X1] :
( and(X0,X1) = not(or(not(X0),not(X1)))
| ~ op_and ),
inference(cnf_transformation,[status(thm)],[f159]) ).
fof(f161,plain,
( ! [X,Y] : implies(X,Y) = not(and(X,not(Y)))
| ~ op_implies_and ),
inference(pre_NNF_transformation,[status(thm)],[f29]) ).
fof(f162,plain,
! [X0,X1] :
( implies(X0,X1) = not(and(X0,not(X1)))
| ~ op_implies_and ),
inference(cnf_transformation,[status(thm)],[f161]) ).
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(f168,plain,
op_and,
inference(cnf_transformation,[status(thm)],[f33]) ).
fof(f170,plain,
modus_ponens,
inference(cnf_transformation,[status(thm)],[f35]) ).
fof(f172,plain,
r2,
inference(cnf_transformation,[status(thm)],[f37]) ).
fof(f173,plain,
r3,
inference(cnf_transformation,[status(thm)],[f38]) ).
fof(f175,plain,
r5,
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f177,plain,
op_or,
inference(cnf_transformation,[status(thm)],[f42]) ).
fof(f178,plain,
op_implies_and,
inference(cnf_transformation,[status(thm)],[f43]) ).
fof(f180,plain,
~ and_1,
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(f259,definition,
( sQ21_spl
<=> and_1 ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f260,plain,
( ~ sQ21_spl
| and_1 ),
inference(component_clause,[status(thm)],[f259]) ).
fof(f262,definition,
! [X0,X1] :
( sQ22_spl
<=> is_a_theorem(implies(and(X0,X1),X0)) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f263,plain,
! [X0,X1] :
( ~ sQ22_spl
| is_a_theorem(implies(and(X0,X1),X0)) ),
inference(component_clause,[status(thm)],[f262]) ).
fof(f266,definition,
( sQ23_spl
<=> is_a_theorem(implies(and(sK13_skl,sK14_skl),sK13_skl)) ),
introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition]) ).
fof(f268,plain,
( sQ23_spl
| ~ is_a_theorem(implies(and(sK13_skl,sK14_skl),sK13_skl)) ),
inference(component_clause,[status(thm)],[f266]) ).
fof(f269,plain,
( ~ sQ23_spl
| sQ21_spl ),
inference(split_clause,[status(thm)],[f80,f259,f266]) ).
fof(f295,definition,
! [X0,X1] :
( sQ31_spl
<=> is_a_theorem(implies(X0,or(X0,X1))) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f296,plain,
! [X0,X1] :
( ~ sQ31_spl
| is_a_theorem(implies(X0,or(X0,X1))) ),
inference(component_clause,[status(thm)],[f295]) ).
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(f369,definition,
( sQ51_spl
<=> kn2 ),
introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition]) ).
fof(f372,plain,
( sQ22_spl
| ~ sQ51_spl ),
inference(split_clause,[status(thm)],[f119,f369,f262]) ).
fof(f373,definition,
( sQ52_spl
<=> is_a_theorem(implies(and(sK33_skl,sK34_skl),sK33_skl)) ),
introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition]) ).
fof(f375,plain,
( sQ52_spl
| ~ is_a_theorem(implies(and(sK33_skl,sK34_skl),sK33_skl)) ),
inference(component_clause,[status(thm)],[f373]) ).
fof(f376,plain,
( ~ sQ52_spl
| sQ51_spl ),
inference(split_clause,[status(thm)],[f120,f369,f373]) ).
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(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(f470,definition,
( sQ78_spl
<=> op_or ),
introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition]) ).
fof(f472,plain,
( sQ78_spl
| ~ op_or ),
inference(component_clause,[status(thm)],[f470]) ).
fof(f473,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(f474,plain,
! [X0,X1] :
( ~ sQ79_spl
| or(X0,X1) = not(and(not(X0),not(X1))) ),
inference(component_clause,[status(thm)],[f473]) ).
fof(f476,plain,
( sQ79_spl
| ~ sQ78_spl ),
inference(split_clause,[status(thm)],[f158,f470,f473]) ).
fof(f477,definition,
( sQ80_spl
<=> op_and ),
introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition]) ).
fof(f479,plain,
( sQ80_spl
| ~ op_and ),
inference(component_clause,[status(thm)],[f477]) ).
fof(f480,definition,
! [X0,X1] :
( sQ81_spl
<=> and(X0,X1) = not(or(not(X0),not(X1))) ),
introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition]) ).
fof(f481,plain,
! [X0,X1] :
( ~ sQ81_spl
| and(X0,X1) = not(or(not(X0),not(X1))) ),
inference(component_clause,[status(thm)],[f480]) ).
fof(f483,plain,
( sQ81_spl
| ~ sQ80_spl ),
inference(split_clause,[status(thm)],[f160,f477,f480]) ).
fof(f484,definition,
( sQ82_spl
<=> op_implies_and ),
introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition]) ).
fof(f486,plain,
( sQ82_spl
| ~ op_implies_and ),
inference(component_clause,[status(thm)],[f484]) ).
fof(f487,definition,
! [X0,X1] :
( sQ83_spl
<=> implies(X0,X1) = not(and(X0,not(X1))) ),
introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition]) ).
fof(f488,plain,
! [X0,X1] :
( ~ sQ83_spl
| implies(X0,X1) = not(and(X0,not(X1))) ),
inference(component_clause,[status(thm)],[f487]) ).
fof(f490,plain,
( sQ83_spl
| ~ sQ82_spl ),
inference(split_clause,[status(thm)],[f162,f484,f487]) ).
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(f507,plain,
( sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f183,f170]) ).
fof(f508,plain,
sQ0_spl,
inference(contradiction_clause,[status(thm)],[f507]) ).
fof(f511,plain,
( sQ84_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f493,f167]) ).
fof(f512,plain,
sQ84_spl,
inference(contradiction_clause,[status(thm)],[f511]) ).
fof(f513,plain,
( sQ82_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f486,f178]) ).
fof(f514,plain,
sQ82_spl,
inference(contradiction_clause,[status(thm)],[f513]) ).
fof(f515,plain,
( sQ80_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f479,f168]) ).
fof(f516,plain,
sQ80_spl,
inference(contradiction_clause,[status(thm)],[f515]) ).
fof(f517,plain,
( sQ78_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f472,f177]) ).
fof(f518,plain,
sQ78_spl,
inference(contradiction_clause,[status(thm)],[f517]) ).
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(f529,plain,
( sQ69_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f439,f173]) ).
fof(f530,plain,
sQ69_spl,
inference(contradiction_clause,[status(thm)],[f529]) ).
fof(f533,plain,
( sQ67_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f431,f172]) ).
fof(f534,plain,
sQ67_spl,
inference(contradiction_clause,[status(thm)],[f533]) ).
fof(f565,plain,
( sQ23_spl
| ~ sQ22_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f268,f263]) ).
fof(f566,plain,
( sQ23_spl
| ~ sQ22_spl ),
inference(contradiction_clause,[status(thm)],[f565]) ).
fof(f575,plain,
! [X0,X1] :
( ~ sQ81_spl
| ~ sQ85_spl
| and(X0,X1) = not(implies(X0,not(X1))) ),
inference(forward_demodulation,[status(thm)],[f495,f481]) ).
fof(f580,plain,
! [X0,X1] :
( ~ sQ79_spl
| ~ sQ83_spl
| or(X0,X1) = implies(not(X0),X1) ),
inference(forward_demodulation,[status(thm)],[f488,f474]) ).
fof(f581,plain,
! [X0,X1,X2] :
( ~ sQ81_spl
| ~ sQ85_spl
| ~ sQ79_spl
| ~ sQ83_spl
| or(implies(X0,not(X1)),X2) = implies(and(X0,X1),X2) ),
inference(paramodulation,[status(thm)],[f575,f580]) ).
fof(f589,plain,
! [X0,X1,X2] :
( ~ sQ85_spl
| ~ sQ76_spl
| is_a_theorem(implies(implies(X0,X1),implies(implies(X2,X0),or(not(X2),X1)))) ),
inference(paramodulation,[status(thm)],[f495,f463]) ).
fof(f591,plain,
! [X0,X1,X2] :
( ~ sQ85_spl
| ~ sQ76_spl
| is_a_theorem(implies(implies(X0,X1),implies(implies(X2,X0),implies(X2,X1)))) ),
inference(forward_demodulation,[status(thm)],[f495,f589]) ).
fof(f608,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(f755,plain,
! [X0,X1,X2] :
( ~ sQ81_spl
| ~ sQ85_spl
| ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ1_spl
| ~ sQ70_spl
| is_a_theorem(implies(and(X1,X2),X0))
| ~ is_a_theorem(or(X0,implies(X1,not(X2)))) ),
inference(paramodulation,[status(thm)],[f581,f608]) ).
fof(f1334,plain,
! [X0,X1,X2] :
( ~ sQ1_spl
| ~ sQ70_spl
| is_a_theorem(X2)
| ~ is_a_theorem(implies(implies(or(X0,X1),or(X1,X0)),X2)) ),
inference(resolution,[status(thm)],[f441,f185]) ).
fof(f1384,plain,
! [X0,X1,X2] :
( ~ sQ1_spl
| ~ sQ34_spl
| is_a_theorem(X2)
| ~ is_a_theorem(implies(implies(X0,or(X1,X0)),X2)) ),
inference(resolution,[status(thm)],[f307,f185]) ).
fof(f1873,plain,
! [X0,X1,X2] :
( ~ sQ85_spl
| ~ sQ76_spl
| ~ sQ1_spl
| ~ sQ70_spl
| is_a_theorem(implies(implies(X0,or(X1,X2)),implies(X0,or(X2,X1)))) ),
inference(resolution,[status(thm)],[f1334,f591]) ).
fof(f8790,plain,
( sQ52_spl
| ~ sQ81_spl
| ~ sQ85_spl
| ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ1_spl
| ~ sQ70_spl
| ~ is_a_theorem(or(sK33_skl,implies(sK33_skl,not(sK34_skl)))) ),
inference(resolution,[status(thm)],[f755,f375]) ).
fof(f40650,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ sQ34_spl
| ~ sQ85_spl
| ~ sQ76_spl
| ~ sQ70_spl
| is_a_theorem(implies(X0,or(X0,X1))) ),
inference(resolution,[status(thm)],[f1873,f1384]) ).
fof(f40711,plain,
( ~ sQ1_spl
| ~ sQ34_spl
| ~ sQ85_spl
| ~ sQ76_spl
| ~ sQ70_spl
| sQ31_spl ),
inference(split_clause,[status(thm)],[f40650,f295,f440,f462,f494,f306,f184]) ).
fof(f40759,plain,
! [X0,X1] :
( ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ31_spl
| is_a_theorem(or(X0,or(not(X0),X1))) ),
inference(paramodulation,[status(thm)],[f580,f296]) ).
fof(f40788,plain,
! [X0,X1] :
( ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ31_spl
| ~ sQ85_spl
| is_a_theorem(or(X0,implies(X0,X1))) ),
inference(forward_demodulation,[status(thm)],[f495,f40759]) ).
fof(f40858,plain,
( sQ52_spl
| ~ sQ81_spl
| ~ sQ85_spl
| ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ1_spl
| ~ sQ70_spl
| ~ sQ31_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f8790,f40788]) ).
fof(f40898,plain,
( sQ52_spl
| ~ sQ81_spl
| ~ sQ85_spl
| ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ1_spl
| ~ sQ70_spl
| ~ sQ31_spl ),
inference(contradiction_clause,[status(thm)],[f40858]) ).
fof(f40919,plain,
( ~ sQ21_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f260,f180]) ).
fof(f40920,plain,
~ sQ21_spl,
inference(contradiction_clause,[status(thm)],[f40919]) ).
fof(f40921,plain,
$false,
inference(sat_refutation,[status(thm)],[f187,f269,f372,f376,f432,f443,f465,f476,f483,f490,f497,f508,f512,f514,f516,f518,f522,f530,f534,f566,f40711,f40898,f40920]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : LCL487+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% 0.00/0.05 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.14/0.40 % Computer : n005.cluster.edu
% 0.14/0.40 % Model : x86_64 x86_64
% 0.14/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.40 % Memory : 8046.5625MB
% 0.14/0.40 % OS : Linux 6.8.0-71-generic
% 0.14/0.40 % CPULimit : 300
% 0.14/0.40 % WCLimit : 300
% 0.14/0.40 % DateTime : Mon Sep 21 00:35:32 UTC 2026
% 0.14/0.40 % CPUTime :
% 0.14/0.42 % Drodi V4.1.1
% 15.67/2.45 % Refutation found
% 15.67/2.45 % SZS status Theorem for theBenchmark: Theorem is valid
% 15.67/2.45 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 1.39/2.53 % Elapsed time: 2.105981 seconds
% 1.39/2.53 % CPU time: 16.366516 seconds
% 1.39/2.53 % Total memory used: 318.318 MB
% 1.39/2.53 % Net memory used: 300.358 MB
%------------------------------------------------------------------------------