%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LCL499+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 : n014.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:52 PM UTC 2026
% Result : Theorem 0.12s 0.60s
% Output : CNFRefutation 0.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 25
% Syntax : Number of formulae : 92 ( 20 unt; 13 def)
% Number of atoms : 223 ( 12 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 222 ( 91 ~; 94 |; 16 &)
% ( 18 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 22 ( 20 usr; 20 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 6 con; 0-2 aty)
% Number of variables : 79 ( 71 !; 8 ?)
% 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(f16,axiom,
( kn1
<=> ! [P] : is_a_theorem(implies(P,and(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(f24,axiom,
( r3
<=> ! [P,Q] : is_a_theorem(implies(or(P,Q),or(Q,P))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f28,axiom,
( op_and
=> ! [X,Y] : and(X,Y) = not(or(not(X),not(Y))) ),
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(f33,axiom,
op_and,
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(f38,axiom,
r3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f45,conjecture,
kn1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f46,negated_conjecture,
~ kn1,
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(f113,plain,
( ( ? [P] : ~ is_a_theorem(implies(P,and(P,P)))
| kn1 )
& ( ! [P] : is_a_theorem(implies(P,and(P,P)))
| ~ kn1 ) ),
inference(NNF_transformation,[status(thm)],[f16]) ).
fof(f114,plain,
( ( ~ is_a_theorem(implies(sK32_skl,and(sK32_skl,sK32_skl)))
| kn1 )
& ( ! [P] : is_a_theorem(implies(P,and(P,P)))
| ~ kn1 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK32_skl]),skolemize(P,sK32_skl)],[f113]) ).
fof(f116,plain,
( ~ is_a_theorem(implies(sK32_skl,and(sK32_skl,sK32_skl)))
| kn1 ),
inference(cnf_transformation,[status(thm)],[f114]) ).
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(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(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(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(f171,plain,
r1,
inference(cnf_transformation,[status(thm)],[f36]) ).
fof(f173,plain,
r3,
inference(cnf_transformation,[status(thm)],[f38]) ).
fof(f180,plain,
~ kn1,
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(f358,definition,
( sQ48_spl
<=> kn1 ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f359,plain,
( ~ sQ48_spl
| kn1 ),
inference(component_clause,[status(thm)],[f358]) ).
fof(f361,definition,
! [X0] :
( sQ49_spl
<=> is_a_theorem(implies(X0,and(X0,X0))) ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f362,plain,
! [X0] :
( ~ sQ49_spl
| is_a_theorem(implies(X0,and(X0,X0))) ),
inference(component_clause,[status(thm)],[f361]) ).
fof(f365,definition,
( sQ50_spl
<=> is_a_theorem(implies(sK32_skl,and(sK32_skl,sK32_skl))) ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f367,plain,
( sQ50_spl
| ~ is_a_theorem(implies(sK32_skl,and(sK32_skl,sK32_skl))) ),
inference(component_clause,[status(thm)],[f365]) ).
fof(f368,plain,
( ~ sQ50_spl
| sQ48_spl ),
inference(split_clause,[status(thm)],[f116,f358,f365]) ).
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(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(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(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,
( sQ84_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f493,f167]) ).
fof(f508,plain,
sQ84_spl,
inference(contradiction_clause,[status(thm)],[f507]) ).
fof(f511,plain,
( sQ80_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f479,f168]) ).
fof(f512,plain,
sQ80_spl,
inference(contradiction_clause,[status(thm)],[f511]) ).
fof(f528,plain,
( sQ50_spl
| ~ sQ49_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f367,f362]) ).
fof(f539,plain,
( sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f183,f170]) ).
fof(f540,plain,
sQ0_spl,
inference(contradiction_clause,[status(thm)],[f539]) ).
fof(f543,plain,
! [X0,X1] :
( ~ sQ81_spl
| ~ sQ85_spl
| and(X0,X1) = not(implies(X0,not(X1))) ),
inference(forward_demodulation,[status(thm)],[f495,f481]) ).
fof(f558,plain,
( sQ50_spl
| ~ sQ49_spl ),
inference(contradiction_clause,[status(thm)],[f528]) ).
fof(f574,plain,
( sQ69_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f439,f173]) ).
fof(f575,plain,
sQ69_spl,
inference(contradiction_clause,[status(thm)],[f574]) ).
fof(f576,plain,
( sQ64_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f420,f171]) ).
fof(f577,plain,
sQ64_spl,
inference(contradiction_clause,[status(thm)],[f576]) ).
fof(f595,plain,
! [X0,X1,X2] :
( ~ sQ81_spl
| ~ sQ85_spl
| implies(implies(X0,not(X1)),X2) = or(and(X0,X1),X2) ),
inference(paramodulation,[status(thm)],[f543,f495]) ).
fof(f618,plain,
! [X0,X1] :
( ~ sQ85_spl
| ~ sQ70_spl
| is_a_theorem(implies(or(X0,not(X1)),implies(X1,X0))) ),
inference(paramodulation,[status(thm)],[f495,f441]) ).
fof(f623,plain,
! [X0] :
( ~ sQ85_spl
| ~ sQ65_spl
| is_a_theorem(implies(implies(X0,not(X0)),not(X0))) ),
inference(paramodulation,[status(thm)],[f495,f422]) ).
fof(f624,plain,
! [X0] :
( ~ sQ85_spl
| ~ sQ65_spl
| ~ sQ81_spl
| is_a_theorem(or(and(X0,X0),not(X0))) ),
inference(forward_demodulation,[status(thm)],[f595,f623]) ).
fof(f632,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ sQ85_spl
| ~ sQ65_spl
| ~ sQ81_spl
| is_a_theorem(X1)
| ~ is_a_theorem(implies(or(and(X0,X0),not(X0)),X1)) ),
inference(resolution,[status(thm)],[f624,f185]) ).
fof(f1160,plain,
! [X0] :
( ~ sQ85_spl
| ~ sQ70_spl
| ~ sQ1_spl
| ~ sQ65_spl
| ~ sQ81_spl
| is_a_theorem(implies(X0,and(X0,X0))) ),
inference(resolution,[status(thm)],[f632,f618]) ).
fof(f1174,plain,
( ~ sQ85_spl
| ~ sQ70_spl
| ~ sQ1_spl
| ~ sQ65_spl
| ~ sQ81_spl
| sQ49_spl ),
inference(split_clause,[status(thm)],[f1160,f361,f480,f421,f184,f440,f494]) ).
fof(f1186,plain,
( ~ sQ48_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f359,f180]) ).
fof(f1187,plain,
~ sQ48_spl,
inference(contradiction_clause,[status(thm)],[f1186]) ).
fof(f1188,plain,
$false,
inference(sat_refutation,[status(thm)],[f187,f368,f424,f443,f483,f497,f508,f512,f540,f558,f575,f577,f1174,f1187]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL499+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.55 % Computer : n014.cluster.edu
% 0.09/0.55 % Model : x86_64 x86_64
% 0.09/0.55 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.55 % Memory : 8046.5625MB
% 0.09/0.55 % OS : Linux 6.8.0-71-generic
% 0.09/0.55 % CPULimit : 300
% 0.09/0.55 % WCLimit : 300
% 0.09/0.55 % DateTime : Mon Sep 21 00:36:06 UTC 2026
% 0.09/0.55 % CPUTime :
% 0.12/0.56 % Drodi V4.1.1
% 0.12/0.60 % Refutation found
% 0.12/0.60 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.12/0.60 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.12/0.63 % Elapsed time: 0.069691 seconds
% 0.12/0.63 % CPU time: 0.229805 seconds
% 0.12/0.63 % Total memory used: 86.398 MB
% 0.12/0.63 % Net memory used: 86.178 MB
%------------------------------------------------------------------------------