%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LCL539+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:57 PM UTC 2026
% Result : Theorem 0.21s 10.79s
% Output : CNFRefutation 0.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 44
% Syntax : Number of formulae : 164 ( 32 unt; 24 def)
% Number of atoms : 437 ( 34 equ)
% Maximal formula atoms : 10 ( 2 avg)
% Number of connectives : 470 ( 197 ~; 207 |; 26 &)
% ( 34 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 37 ( 35 usr; 35 prp; 0-2 aty)
% Number of functors : 19 ( 19 usr; 13 con; 0-2 aty)
% Number of variables : 147 ( 132 !; 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/sandbox/benchmark/theBenchmark.p') ).
fof(f2,axiom,
( substitution_of_equivalents
<=> ! [X,Y] :
( is_a_theorem(equiv(X,Y))
=> X = Y ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,axiom,
( and_1
<=> ! [X,Y] : is_a_theorem(implies(and(X,Y),X)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8,axiom,
( and_2
<=> ! [X,Y] : is_a_theorem(implies(and(X,Y),Y)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f9,axiom,
( and_3
<=> ! [X,Y] : is_a_theorem(implies(X,implies(Y,and(X,Y)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f31,axiom,
( op_equiv
=> ! [X,Y] : equiv(X,Y) = and(implies(X,Y),implies(Y,X)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f34,axiom,
op_equiv,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f35,axiom,
modus_ponens,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f40,axiom,
and_1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f41,axiom,
and_2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f42,axiom,
and_3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f49,axiom,
substitution_of_equivalents,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f53,axiom,
( substitution_strict_equiv
<=> ! [X,Y] :
( is_a_theorem(strict_equiv(X,Y))
=> X = Y ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f55,axiom,
( axiom_M
<=> ! [X] : is_a_theorem(implies(necessarily(X),X)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f75,axiom,
( op_strict_implies
=> ! [X,Y] : strict_implies(X,Y) = necessarily(implies(X,Y)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f76,axiom,
( op_strict_equiv
=> ! [X,Y] : strict_equiv(X,Y) = and(strict_implies(X,Y),strict_implies(Y,X)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f80,axiom,
axiom_M,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f86,axiom,
op_strict_implies,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f88,axiom,
op_strict_equiv,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f89,conjecture,
substitution_strict_equiv,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f90,negated_conjecture,
~ substitution_strict_equiv,
inference(negated_conjecture,[status(cth)],[f89]) ).
fof(f91,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(f92,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)],[f91]) ).
fof(f93,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)],[f92]) ).
fof(f94,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)],[f93]) ).
fof(f95,plain,
! [X0,X1] :
( is_a_theorem(X1)
| ~ is_a_theorem(implies(X0,X1))
| ~ is_a_theorem(X0)
| ~ modus_ponens ),
inference(cnf_transformation,[status(thm)],[f94]) ).
fof(f99,plain,
( substitution_of_equivalents
<=> ! [X,Y] :
( X = Y
| ~ is_a_theorem(equiv(X,Y)) ) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f100,plain,
( ( ? [X,Y] :
( X != Y
& is_a_theorem(equiv(X,Y)) )
| substitution_of_equivalents )
& ( ! [X,Y] :
( X = Y
| ~ is_a_theorem(equiv(X,Y)) )
| ~ substitution_of_equivalents ) ),
inference(NNF_transformation,[status(thm)],[f99]) ).
fof(f101,plain,
( ( ( sK2_skl != sK3_skl
& is_a_theorem(equiv(sK2_skl,sK3_skl)) )
| substitution_of_equivalents )
& ( ! [X,Y] :
( X = Y
| ~ is_a_theorem(equiv(X,Y)) )
| ~ substitution_of_equivalents ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2_skl,sK3_skl]),skolemize(X,sK2_skl),skolemize(Y,sK3_skl)],[f100]) ).
fof(f102,plain,
! [X0,X1] :
( X0 = X1
| ~ is_a_theorem(equiv(X0,X1))
| ~ substitution_of_equivalents ),
inference(cnf_transformation,[status(thm)],[f101]) ).
fof(f121,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(f122,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)],[f121]) ).
fof(f123,plain,
! [X0,X1] :
( is_a_theorem(implies(and(X0,X1),X0))
| ~ and_1 ),
inference(cnf_transformation,[status(thm)],[f122]) ).
fof(f125,plain,
( ( ? [X,Y] : ~ is_a_theorem(implies(and(X,Y),Y))
| and_2 )
& ( ! [X,Y] : is_a_theorem(implies(and(X,Y),Y))
| ~ and_2 ) ),
inference(NNF_transformation,[status(thm)],[f8]) ).
fof(f126,plain,
( ( ~ is_a_theorem(implies(and(sK15_skl,sK16_skl),sK16_skl))
| and_2 )
& ( ! [X,Y] : is_a_theorem(implies(and(X,Y),Y))
| ~ and_2 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl,sK16_skl]),skolemize(X,sK15_skl),skolemize(Y,sK16_skl)],[f125]) ).
fof(f127,plain,
! [X0,X1] :
( is_a_theorem(implies(and(X0,X1),X1))
| ~ and_2 ),
inference(cnf_transformation,[status(thm)],[f126]) ).
fof(f129,plain,
( ( ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,and(X,Y))))
| and_3 )
& ( ! [X,Y] : is_a_theorem(implies(X,implies(Y,and(X,Y))))
| ~ and_3 ) ),
inference(NNF_transformation,[status(thm)],[f9]) ).
fof(f130,plain,
( ( ~ is_a_theorem(implies(sK17_skl,implies(sK18_skl,and(sK17_skl,sK18_skl))))
| and_3 )
& ( ! [X,Y] : is_a_theorem(implies(X,implies(Y,and(X,Y))))
| ~ and_3 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK17_skl,sK18_skl]),skolemize(X,sK17_skl),skolemize(Y,sK18_skl)],[f129]) ).
fof(f131,plain,
! [X0,X1] :
( is_a_theorem(implies(X0,implies(X1,and(X0,X1))))
| ~ and_3 ),
inference(cnf_transformation,[status(thm)],[f130]) ).
fof(f209,plain,
( ! [X,Y] : equiv(X,Y) = and(implies(X,Y),implies(Y,X))
| ~ op_equiv ),
inference(pre_NNF_transformation,[status(thm)],[f31]) ).
fof(f210,plain,
! [X0,X1] :
( equiv(X0,X1) = and(implies(X0,X1),implies(X1,X0))
| ~ op_equiv ),
inference(cnf_transformation,[status(thm)],[f209]) ).
fof(f213,plain,
op_equiv,
inference(cnf_transformation,[status(thm)],[f34]) ).
fof(f214,plain,
modus_ponens,
inference(cnf_transformation,[status(thm)],[f35]) ).
fof(f219,plain,
and_1,
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f220,plain,
and_2,
inference(cnf_transformation,[status(thm)],[f41]) ).
fof(f221,plain,
and_3,
inference(cnf_transformation,[status(thm)],[f42]) ).
fof(f228,plain,
substitution_of_equivalents,
inference(cnf_transformation,[status(thm)],[f49]) ).
fof(f250,plain,
( substitution_strict_equiv
<=> ! [X,Y] :
( X = Y
| ~ is_a_theorem(strict_equiv(X,Y)) ) ),
inference(pre_NNF_transformation,[status(thm)],[f53]) ).
fof(f251,plain,
( ( ? [X,Y] :
( X != Y
& is_a_theorem(strict_equiv(X,Y)) )
| substitution_strict_equiv )
& ( ! [X,Y] :
( X = Y
| ~ is_a_theorem(strict_equiv(X,Y)) )
| ~ substitution_strict_equiv ) ),
inference(NNF_transformation,[status(thm)],[f250]) ).
fof(f252,plain,
( ( ( sK60_skl != sK61_skl
& is_a_theorem(strict_equiv(sK60_skl,sK61_skl)) )
| substitution_strict_equiv )
& ( ! [X,Y] :
( X = Y
| ~ is_a_theorem(strict_equiv(X,Y)) )
| ~ substitution_strict_equiv ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK60_skl,sK61_skl]),skolemize(X,sK60_skl),skolemize(Y,sK61_skl)],[f251]) ).
fof(f254,plain,
( is_a_theorem(strict_equiv(sK60_skl,sK61_skl))
| substitution_strict_equiv ),
inference(cnf_transformation,[status(thm)],[f252]) ).
fof(f255,plain,
( sK60_skl != sK61_skl
| substitution_strict_equiv ),
inference(cnf_transformation,[status(thm)],[f252]) ).
fof(f260,plain,
( ( ? [X] : ~ is_a_theorem(implies(necessarily(X),X))
| axiom_M )
& ( ! [X] : is_a_theorem(implies(necessarily(X),X))
| ~ axiom_M ) ),
inference(NNF_transformation,[status(thm)],[f55]) ).
fof(f261,plain,
( ( ~ is_a_theorem(implies(necessarily(sK64_skl),sK64_skl))
| axiom_M )
& ( ! [X] : is_a_theorem(implies(necessarily(X),X))
| ~ axiom_M ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK64_skl]),skolemize(X,sK64_skl)],[f260]) ).
fof(f262,plain,
! [X0] :
( is_a_theorem(implies(necessarily(X0),X0))
| ~ axiom_M ),
inference(cnf_transformation,[status(thm)],[f261]) ).
fof(f336,plain,
( ! [X,Y] : strict_implies(X,Y) = necessarily(implies(X,Y))
| ~ op_strict_implies ),
inference(pre_NNF_transformation,[status(thm)],[f75]) ).
fof(f337,plain,
! [X0,X1] :
( strict_implies(X0,X1) = necessarily(implies(X0,X1))
| ~ op_strict_implies ),
inference(cnf_transformation,[status(thm)],[f336]) ).
fof(f338,plain,
( ! [X,Y] : strict_equiv(X,Y) = and(strict_implies(X,Y),strict_implies(Y,X))
| ~ op_strict_equiv ),
inference(pre_NNF_transformation,[status(thm)],[f76]) ).
fof(f339,plain,
! [X0,X1] :
( strict_equiv(X0,X1) = and(strict_implies(X0,X1),strict_implies(X1,X0))
| ~ op_strict_equiv ),
inference(cnf_transformation,[status(thm)],[f338]) ).
fof(f343,plain,
axiom_M,
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f349,plain,
op_strict_implies,
inference(cnf_transformation,[status(thm)],[f86]) ).
fof(f351,plain,
op_strict_equiv,
inference(cnf_transformation,[status(thm)],[f88]) ).
fof(f352,plain,
~ substitution_strict_equiv,
inference(cnf_transformation,[status(thm)],[f90]) ).
fof(f353,definition,
( sQ0_spl
<=> modus_ponens ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f355,plain,
( sQ0_spl
| ~ modus_ponens ),
inference(component_clause,[status(thm)],[f353]) ).
fof(f356,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(f357,plain,
! [X0,X1] :
( ~ sQ1_spl
| is_a_theorem(X1)
| ~ is_a_theorem(implies(X0,X1))
| ~ is_a_theorem(X0) ),
inference(component_clause,[status(thm)],[f356]) ).
fof(f359,plain,
( sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f95,f353,f356]) ).
fof(f372,definition,
( sQ5_spl
<=> substitution_of_equivalents ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f374,plain,
( sQ5_spl
| ~ substitution_of_equivalents ),
inference(component_clause,[status(thm)],[f372]) ).
fof(f375,definition,
! [X0,X1] :
( sQ6_spl
<=> ( X0 = X1
| ~ is_a_theorem(equiv(X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f376,plain,
! [X0,X1] :
( ~ sQ6_spl
| X0 = X1
| ~ is_a_theorem(equiv(X0,X1)) ),
inference(component_clause,[status(thm)],[f375]) ).
fof(f378,plain,
( sQ6_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f102,f372,f375]) ).
fof(f431,definition,
( sQ21_spl
<=> and_1 ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f433,plain,
( sQ21_spl
| ~ and_1 ),
inference(component_clause,[status(thm)],[f431]) ).
fof(f434,definition,
! [X0,X1] :
( sQ22_spl
<=> is_a_theorem(implies(and(X0,X1),X0)) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f435,plain,
! [X0,X1] :
( ~ sQ22_spl
| is_a_theorem(implies(and(X0,X1),X0)) ),
inference(component_clause,[status(thm)],[f434]) ).
fof(f437,plain,
( sQ22_spl
| ~ sQ21_spl ),
inference(split_clause,[status(thm)],[f123,f431,f434]) ).
fof(f442,definition,
( sQ24_spl
<=> and_2 ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f444,plain,
( sQ24_spl
| ~ and_2 ),
inference(component_clause,[status(thm)],[f442]) ).
fof(f445,definition,
! [X0,X1] :
( sQ25_spl
<=> is_a_theorem(implies(and(X0,X1),X1)) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f446,plain,
! [X0,X1] :
( ~ sQ25_spl
| is_a_theorem(implies(and(X0,X1),X1)) ),
inference(component_clause,[status(thm)],[f445]) ).
fof(f448,plain,
( sQ25_spl
| ~ sQ24_spl ),
inference(split_clause,[status(thm)],[f127,f442,f445]) ).
fof(f453,definition,
( sQ27_spl
<=> and_3 ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f455,plain,
( sQ27_spl
| ~ and_3 ),
inference(component_clause,[status(thm)],[f453]) ).
fof(f456,definition,
! [X0,X1] :
( sQ28_spl
<=> is_a_theorem(implies(X0,implies(X1,and(X0,X1)))) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f457,plain,
! [X0,X1] :
( ~ sQ28_spl
| is_a_theorem(implies(X0,implies(X1,and(X0,X1)))) ),
inference(component_clause,[status(thm)],[f456]) ).
fof(f459,plain,
( sQ28_spl
| ~ sQ27_spl ),
inference(split_clause,[status(thm)],[f131,f453,f456]) ).
fof(f670,definition,
( sQ86_spl
<=> op_equiv ),
introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition]) ).
fof(f672,plain,
( sQ86_spl
| ~ op_equiv ),
inference(component_clause,[status(thm)],[f670]) ).
fof(f673,definition,
! [X0,X1] :
( sQ87_spl
<=> equiv(X0,X1) = and(implies(X0,X1),implies(X1,X0)) ),
introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition]) ).
fof(f674,plain,
! [X0,X1] :
( ~ sQ87_spl
| equiv(X0,X1) = and(implies(X0,X1),implies(X1,X0)) ),
inference(component_clause,[status(thm)],[f673]) ).
fof(f676,plain,
( sQ87_spl
| ~ sQ86_spl ),
inference(split_clause,[status(thm)],[f210,f670,f673]) ).
fof(f714,definition,
! [X0,X1] :
( sQ98_spl
<=> ( is_a_theorem(and(X0,X1))
| ~ is_a_theorem(X1)
| ~ is_a_theorem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ98_spl])],[split_symbol_definition]) ).
fof(f715,plain,
! [X0,X1] :
( ~ sQ98_spl
| is_a_theorem(and(X0,X1))
| ~ is_a_theorem(X1)
| ~ is_a_theorem(X0) ),
inference(component_clause,[status(thm)],[f714]) ).
fof(f730,definition,
( sQ102_spl
<=> substitution_strict_equiv ),
introduced(definition,[new_symbols(definition,[sQ102_spl])],[split_symbol_definition]) ).
fof(f731,plain,
( ~ sQ102_spl
| substitution_strict_equiv ),
inference(component_clause,[status(thm)],[f730]) ).
fof(f737,definition,
( sQ104_spl
<=> is_a_theorem(strict_equiv(sK60_skl,sK61_skl)) ),
introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition]) ).
fof(f738,plain,
( ~ sQ104_spl
| is_a_theorem(strict_equiv(sK60_skl,sK61_skl)) ),
inference(component_clause,[status(thm)],[f737]) ).
fof(f740,plain,
( sQ104_spl
| sQ102_spl ),
inference(split_clause,[status(thm)],[f254,f730,f737]) ).
fof(f741,definition,
( sQ105_spl
<=> sK60_skl = sK61_skl ),
introduced(definition,[new_symbols(definition,[sQ105_spl])],[split_symbol_definition]) ).
fof(f743,plain,
( sQ105_spl
| sK60_skl != sK61_skl ),
inference(component_clause,[status(thm)],[f741]) ).
fof(f744,plain,
( ~ sQ105_spl
| sQ102_spl ),
inference(split_clause,[status(thm)],[f255,f730,f741]) ).
fof(f756,definition,
( sQ109_spl
<=> axiom_M ),
introduced(definition,[new_symbols(definition,[sQ109_spl])],[split_symbol_definition]) ).
fof(f758,plain,
( sQ109_spl
| ~ axiom_M ),
inference(component_clause,[status(thm)],[f756]) ).
fof(f759,definition,
! [X0] :
( sQ110_spl
<=> is_a_theorem(implies(necessarily(X0),X0)) ),
introduced(definition,[new_symbols(definition,[sQ110_spl])],[split_symbol_definition]) ).
fof(f760,plain,
! [X0] :
( ~ sQ110_spl
| is_a_theorem(implies(necessarily(X0),X0)) ),
inference(component_clause,[status(thm)],[f759]) ).
fof(f762,plain,
( sQ110_spl
| ~ sQ109_spl ),
inference(split_clause,[status(thm)],[f262,f756,f759]) ).
fof(f968,definition,
( sQ167_spl
<=> op_strict_implies ),
introduced(definition,[new_symbols(definition,[sQ167_spl])],[split_symbol_definition]) ).
fof(f970,plain,
( sQ167_spl
| ~ op_strict_implies ),
inference(component_clause,[status(thm)],[f968]) ).
fof(f971,definition,
! [X0,X1] :
( sQ168_spl
<=> strict_implies(X0,X1) = necessarily(implies(X0,X1)) ),
introduced(definition,[new_symbols(definition,[sQ168_spl])],[split_symbol_definition]) ).
fof(f972,plain,
! [X0,X1] :
( ~ sQ168_spl
| strict_implies(X0,X1) = necessarily(implies(X0,X1)) ),
inference(component_clause,[status(thm)],[f971]) ).
fof(f974,plain,
( sQ168_spl
| ~ sQ167_spl ),
inference(split_clause,[status(thm)],[f337,f968,f971]) ).
fof(f975,definition,
( sQ169_spl
<=> op_strict_equiv ),
introduced(definition,[new_symbols(definition,[sQ169_spl])],[split_symbol_definition]) ).
fof(f977,plain,
( sQ169_spl
| ~ op_strict_equiv ),
inference(component_clause,[status(thm)],[f975]) ).
fof(f978,definition,
! [X0,X1] :
( sQ170_spl
<=> strict_equiv(X0,X1) = and(strict_implies(X0,X1),strict_implies(X1,X0)) ),
introduced(definition,[new_symbols(definition,[sQ170_spl])],[split_symbol_definition]) ).
fof(f979,plain,
! [X0,X1] :
( ~ sQ170_spl
| strict_equiv(X0,X1) = and(strict_implies(X0,X1),strict_implies(X1,X0)) ),
inference(component_clause,[status(thm)],[f978]) ).
fof(f981,plain,
( sQ170_spl
| ~ sQ169_spl ),
inference(split_clause,[status(thm)],[f339,f975,f978]) ).
fof(f982,plain,
( sQ169_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f977,f351]) ).
fof(f983,plain,
sQ169_spl,
inference(contradiction_clause,[status(thm)],[f982]) ).
fof(f984,plain,
( sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f355,f214]) ).
fof(f985,plain,
sQ0_spl,
inference(contradiction_clause,[status(thm)],[f984]) ).
fof(f988,plain,
( sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f374,f228]) ).
fof(f989,plain,
sQ5_spl,
inference(contradiction_clause,[status(thm)],[f988]) ).
fof(f990,plain,
( sQ167_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f970,f349]) ).
fof(f991,plain,
sQ167_spl,
inference(contradiction_clause,[status(thm)],[f990]) ).
fof(f994,plain,
( sQ86_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f672,f213]) ).
fof(f995,plain,
sQ86_spl,
inference(contradiction_clause,[status(thm)],[f994]) ).
fof(f1022,plain,
( sQ109_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f758,f343]) ).
fof(f1023,plain,
sQ109_spl,
inference(contradiction_clause,[status(thm)],[f1022]) ).
fof(f1024,plain,
! [X0,X1] :
( ~ sQ168_spl
| ~ sQ110_spl
| is_a_theorem(implies(strict_implies(X0,X1),implies(X0,X1))) ),
inference(paramodulation,[status(thm)],[f972,f760]) ).
fof(f1076,plain,
( sQ21_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f433,f219]) ).
fof(f1077,plain,
sQ21_spl,
inference(contradiction_clause,[status(thm)],[f1076]) ).
fof(f1096,plain,
( sQ24_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f444,f220]) ).
fof(f1097,plain,
sQ24_spl,
inference(contradiction_clause,[status(thm)],[f1096]) ).
fof(f1109,plain,
! [X0,X1] :
( ~ sQ25_spl
| ~ sQ1_spl
| is_a_theorem(X1)
| ~ is_a_theorem(and(X0,X1)) ),
inference(resolution,[status(thm)],[f357,f446]) ).
fof(f1110,plain,
! [X0,X1] :
( ~ sQ22_spl
| ~ sQ1_spl
| is_a_theorem(X0)
| ~ is_a_theorem(and(X0,X1)) ),
inference(resolution,[status(thm)],[f357,f435]) ).
fof(f1112,plain,
! [X0,X1] :
( ~ sQ28_spl
| ~ sQ1_spl
| is_a_theorem(implies(X1,and(X0,X1)))
| ~ is_a_theorem(X0) ),
inference(resolution,[status(thm)],[f357,f457]) ).
fof(f1148,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ sQ168_spl
| ~ sQ110_spl
| is_a_theorem(implies(X0,X1))
| ~ is_a_theorem(strict_implies(X0,X1)) ),
inference(resolution,[status(thm)],[f1024,f357]) ).
fof(f1168,plain,
( sQ27_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f455,f221]) ).
fof(f1169,plain,
sQ27_spl,
inference(contradiction_clause,[status(thm)],[f1168]) ).
fof(f1194,plain,
! [X0,X1] :
( ~ sQ170_spl
| ~ sQ22_spl
| ~ sQ1_spl
| is_a_theorem(strict_implies(X0,X1))
| ~ is_a_theorem(strict_equiv(X0,X1)) ),
inference(paramodulation,[status(thm)],[f979,f1110]) ).
fof(f1195,plain,
! [X0,X1] :
( ~ sQ170_spl
| ~ sQ25_spl
| ~ sQ1_spl
| is_a_theorem(strict_implies(X1,X0))
| ~ is_a_theorem(strict_equiv(X0,X1)) ),
inference(paramodulation,[status(thm)],[f979,f1109]) ).
fof(f1390,plain,
! [X0,X1] :
( ~ sQ87_spl
| ~ sQ98_spl
| is_a_theorem(equiv(X0,X1))
| ~ is_a_theorem(implies(X1,X0))
| ~ is_a_theorem(implies(X0,X1)) ),
inference(paramodulation,[status(thm)],[f674,f715]) ).
fof(f1816,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ sQ28_spl
| is_a_theorem(and(X0,X1))
| ~ is_a_theorem(X1)
| ~ is_a_theorem(X0) ),
inference(resolution,[status(thm)],[f1112,f357]) ).
fof(f1820,plain,
( ~ sQ1_spl
| ~ sQ28_spl
| sQ98_spl ),
inference(split_clause,[status(thm)],[f1816,f714,f456,f356]) ).
fof(f1858,plain,
( ~ sQ104_spl
| ~ sQ170_spl
| ~ sQ22_spl
| ~ sQ1_spl
| is_a_theorem(strict_implies(sK60_skl,sK61_skl)) ),
inference(resolution,[status(thm)],[f1194,f738]) ).
fof(f1859,plain,
( ~ sQ1_spl
| ~ sQ168_spl
| ~ sQ110_spl
| ~ sQ104_spl
| ~ sQ170_spl
| ~ sQ22_spl
| is_a_theorem(implies(sK60_skl,sK61_skl)) ),
inference(resolution,[status(thm)],[f1858,f1148]) ).
fof(f1932,plain,
( ~ sQ104_spl
| ~ sQ170_spl
| ~ sQ25_spl
| ~ sQ1_spl
| is_a_theorem(strict_implies(sK61_skl,sK60_skl)) ),
inference(resolution,[status(thm)],[f1195,f738]) ).
fof(f2004,plain,
( ~ sQ1_spl
| ~ sQ168_spl
| ~ sQ110_spl
| ~ sQ104_spl
| ~ sQ170_spl
| ~ sQ25_spl
| is_a_theorem(implies(sK61_skl,sK60_skl)) ),
inference(resolution,[status(thm)],[f1932,f1148]) ).
fof(f3788,plain,
( ~ sQ1_spl
| ~ sQ168_spl
| ~ sQ110_spl
| ~ sQ104_spl
| ~ sQ170_spl
| ~ sQ25_spl
| ~ sQ87_spl
| ~ sQ98_spl
| is_a_theorem(equiv(sK60_skl,sK61_skl))
| ~ is_a_theorem(implies(sK60_skl,sK61_skl)) ),
inference(resolution,[status(thm)],[f1390,f2004]) ).
fof(f3844,definition,
( sQ191_spl
<=> is_a_theorem(implies(sK60_skl,sK61_skl)) ),
introduced(definition,[new_symbols(definition,[sQ191_spl])],[split_symbol_definition]) ).
fof(f3846,plain,
( sQ191_spl
| ~ is_a_theorem(implies(sK60_skl,sK61_skl)) ),
inference(component_clause,[status(thm)],[f3844]) ).
fof(f3847,definition,
( sQ192_spl
<=> is_a_theorem(equiv(sK60_skl,sK61_skl)) ),
introduced(definition,[new_symbols(definition,[sQ192_spl])],[split_symbol_definition]) ).
fof(f3848,plain,
( ~ sQ192_spl
| is_a_theorem(equiv(sK60_skl,sK61_skl)) ),
inference(component_clause,[status(thm)],[f3847]) ).
fof(f3850,plain,
( ~ sQ1_spl
| ~ sQ168_spl
| ~ sQ110_spl
| ~ sQ104_spl
| ~ sQ170_spl
| ~ sQ25_spl
| ~ sQ87_spl
| ~ sQ98_spl
| sQ192_spl
| ~ sQ191_spl ),
inference(split_clause,[status(thm)],[f3788,f3844,f3847,f714,f673,f445,f978,f737,f759,f971,f356]) ).
fof(f3870,plain,
( sQ191_spl
| ~ sQ1_spl
| ~ sQ168_spl
| ~ sQ110_spl
| ~ sQ104_spl
| ~ sQ170_spl
| ~ sQ22_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3846,f1859]) ).
fof(f3871,plain,
( sQ191_spl
| ~ sQ1_spl
| ~ sQ168_spl
| ~ sQ110_spl
| ~ sQ104_spl
| ~ sQ170_spl
| ~ sQ22_spl ),
inference(contradiction_clause,[status(thm)],[f3870]) ).
fof(f3872,plain,
( ~ sQ102_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f731,f352]) ).
fof(f3873,plain,
~ sQ102_spl,
inference(contradiction_clause,[status(thm)],[f3872]) ).
fof(f3915,plain,
( ~ sQ6_spl
| ~ sQ192_spl
| sK60_skl = sK61_skl ),
inference(resolution,[status(thm)],[f3848,f376]) ).
fof(f3918,plain,
( ~ sQ6_spl
| ~ sQ192_spl
| sQ105_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3915,f743]) ).
fof(f3919,plain,
( ~ sQ6_spl
| ~ sQ192_spl
| sQ105_spl ),
inference(contradiction_clause,[status(thm)],[f3918]) ).
fof(f3920,plain,
$false,
inference(sat_refutation,[status(thm)],[f359,f378,f437,f448,f459,f676,f740,f744,f762,f974,f981,f983,f985,f989,f991,f995,f1023,f1077,f1097,f1169,f1820,f3850,f3871,f3873,f3919]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LCL539+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/10.48 % Computer : n019.cluster.edu
% 0.18/10.48 % Model : x86_64 x86_64
% 0.18/10.48 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/10.48 % Memory : 8046.5625MB
% 0.18/10.48 % OS : Linux 6.8.0-71-generic
% 0.18/10.49 % CPULimit : 300
% 0.18/10.49 % WCLimit : 300
% 0.18/10.49 % DateTime : Mon Sep 21 00:38:15 UTC 2026
% 0.18/10.49 % CPUTime :
% 0.21/10.50 % Drodi V4.1.1
% 0.21/10.79 % Refutation found
% 0.21/10.79 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.21/10.79 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.21/10.82 % Elapsed time: 0.310951 seconds
% 0.21/10.82 % CPU time: 2.268414 seconds
% 0.21/10.82 % Total memory used: 139.945 MB
% 0.21/10.82 % Net memory used: 137.139 MB
%------------------------------------------------------------------------------