%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LCL549+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 : n006.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:58 PM UTC 2026
% Result : Theorem 5.68s 1.37s
% Output : CNFRefutation 5.68s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 75
% Syntax : Number of formulae : 287 ( 53 unt; 40 def)
% Number of atoms : 902 ( 46 equ)
% Maximal formula atoms : 16 ( 3 avg)
% Number of connectives : 1113 ( 498 ~; 513 |; 38 &)
% ( 56 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 4 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 61 ( 59 usr; 59 prp; 0-2 aty)
% Number of functors : 28 ( 28 usr; 20 con; 0-2 aty)
% Number of variables : 246 ( 224 !; 22 ?)
% 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(f3,axiom,
( modus_tollens
<=> ! [X,Y] : is_a_theorem(implies(implies(not(Y),not(X)),implies(X,Y))) ),
file('/export/starexec/sandbox/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/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(f10,axiom,
( or_1
<=> ! [X,Y] : is_a_theorem(implies(X,or(X,Y))) ),
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(f27,axiom,
( op_or
=> ! [X,Y] : or(X,Y) = not(and(not(X),not(Y))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f29,axiom,
( op_implies_and
=> ! [X,Y] : implies(X,Y) = not(and(X,not(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(f32,axiom,
op_or,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f33,axiom,
op_implies_and,
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(f36,axiom,
modus_tollens,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f38,axiom,
implies_2,
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(f43,axiom,
or_1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f49,axiom,
substitution_of_equivalents,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f50,axiom,
( necessitation
<=> ! [X] :
( is_a_theorem(X)
=> is_a_theorem(necessarily(X)) ) ),
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(f56,axiom,
( axiom_4
<=> ! [X] : is_a_theorem(implies(necessarily(X),necessarily(necessarily(X)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f57,axiom,
( axiom_B
<=> ! [X] : is_a_theorem(implies(X,necessarily(possibly(X)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f72,axiom,
( axiom_m10
<=> ! [X] : is_a_theorem(strict_implies(possibly(X),necessarily(possibly(X)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f73,axiom,
( op_possibly
=> ! [X] : possibly(X) = not(necessarily(not(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(f77,axiom,
op_possibly,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f78,axiom,
necessitation,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f80,axiom,
axiom_M,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f81,axiom,
axiom_4,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f82,axiom,
axiom_B,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f86,axiom,
op_strict_implies,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f89,conjecture,
axiom_m10,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f90,negated_conjecture,
~ axiom_m10,
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(f105,plain,
( ( ? [X,Y] : ~ is_a_theorem(implies(implies(not(Y),not(X)),implies(X,Y)))
| modus_tollens )
& ( ! [X,Y] : is_a_theorem(implies(implies(not(Y),not(X)),implies(X,Y)))
| ~ modus_tollens ) ),
inference(NNF_transformation,[status(thm)],[f3]) ).
fof(f106,plain,
( ( ~ is_a_theorem(implies(implies(not(sK5_skl),not(sK4_skl)),implies(sK4_skl,sK5_skl)))
| modus_tollens )
& ( ! [X,Y] : is_a_theorem(implies(implies(not(Y),not(X)),implies(X,Y)))
| ~ modus_tollens ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl,sK5_skl]),skolemize(X,sK4_skl),skolemize(Y,sK5_skl)],[f105]) ).
fof(f107,plain,
! [X0,X1] :
( is_a_theorem(implies(implies(not(X0),not(X1)),implies(X1,X0)))
| ~ modus_tollens ),
inference(cnf_transformation,[status(thm)],[f106]) ).
fof(f113,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(f114,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)],[f113]) ).
fof(f115,plain,
! [X0,X1] :
( is_a_theorem(implies(implies(X0,implies(X0,X1)),implies(X0,X1)))
| ~ implies_2 ),
inference(cnf_transformation,[status(thm)],[f114]) ).
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(f133,plain,
( ( ? [X,Y] : ~ is_a_theorem(implies(X,or(X,Y)))
| or_1 )
& ( ! [X,Y] : is_a_theorem(implies(X,or(X,Y)))
| ~ or_1 ) ),
inference(NNF_transformation,[status(thm)],[f10]) ).
fof(f134,plain,
( ( ~ is_a_theorem(implies(sK19_skl,or(sK19_skl,sK20_skl)))
| or_1 )
& ( ! [X,Y] : is_a_theorem(implies(X,or(X,Y)))
| ~ or_1 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK19_skl,sK20_skl]),skolemize(X,sK19_skl),skolemize(Y,sK20_skl)],[f133]) ).
fof(f135,plain,
! [X0,X1] :
( is_a_theorem(implies(X0,or(X0,X1)))
| ~ or_1 ),
inference(cnf_transformation,[status(thm)],[f134]) ).
fof(f181,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(f182,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)],[f181]) ).
fof(f183,plain,
! [X0] :
( is_a_theorem(implies(or(X0,X0),X0))
| ~ r1 ),
inference(cnf_transformation,[status(thm)],[f182]) ).
fof(f184,plain,
( ~ is_a_theorem(implies(or(sK44_skl,sK44_skl),sK44_skl))
| r1 ),
inference(cnf_transformation,[status(thm)],[f182]) ).
fof(f201,plain,
( ! [X,Y] : or(X,Y) = not(and(not(X),not(Y)))
| ~ op_or ),
inference(pre_NNF_transformation,[status(thm)],[f27]) ).
fof(f202,plain,
! [X0,X1] :
( or(X0,X1) = not(and(not(X0),not(X1)))
| ~ op_or ),
inference(cnf_transformation,[status(thm)],[f201]) ).
fof(f205,plain,
( ! [X,Y] : implies(X,Y) = not(and(X,not(Y)))
| ~ op_implies_and ),
inference(pre_NNF_transformation,[status(thm)],[f29]) ).
fof(f206,plain,
! [X0,X1] :
( implies(X0,X1) = not(and(X0,not(X1)))
| ~ op_implies_and ),
inference(cnf_transformation,[status(thm)],[f205]) ).
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(f211,plain,
op_or,
inference(cnf_transformation,[status(thm)],[f32]) ).
fof(f212,plain,
op_implies_and,
inference(cnf_transformation,[status(thm)],[f33]) ).
fof(f213,plain,
op_equiv,
inference(cnf_transformation,[status(thm)],[f34]) ).
fof(f214,plain,
modus_ponens,
inference(cnf_transformation,[status(thm)],[f35]) ).
fof(f215,plain,
modus_tollens,
inference(cnf_transformation,[status(thm)],[f36]) ).
fof(f217,plain,
implies_2,
inference(cnf_transformation,[status(thm)],[f38]) ).
fof(f220,plain,
and_2,
inference(cnf_transformation,[status(thm)],[f41]) ).
fof(f221,plain,
and_3,
inference(cnf_transformation,[status(thm)],[f42]) ).
fof(f222,plain,
or_1,
inference(cnf_transformation,[status(thm)],[f43]) ).
fof(f228,plain,
substitution_of_equivalents,
inference(cnf_transformation,[status(thm)],[f49]) ).
fof(f229,plain,
( necessitation
<=> ! [X] :
( is_a_theorem(necessarily(X))
| ~ is_a_theorem(X) ) ),
inference(pre_NNF_transformation,[status(thm)],[f50]) ).
fof(f230,plain,
( ( ? [X] :
( ~ is_a_theorem(necessarily(X))
& is_a_theorem(X) )
| necessitation )
& ( ! [X] :
( is_a_theorem(necessarily(X))
| ~ is_a_theorem(X) )
| ~ necessitation ) ),
inference(NNF_transformation,[status(thm)],[f229]) ).
fof(f231,plain,
( ( ( ~ is_a_theorem(necessarily(sK55_skl))
& is_a_theorem(sK55_skl) )
| necessitation )
& ( ! [X] :
( is_a_theorem(necessarily(X))
| ~ is_a_theorem(X) )
| ~ necessitation ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK55_skl]),skolemize(X,sK55_skl)],[f230]) ).
fof(f232,plain,
! [X0] :
( is_a_theorem(necessarily(X0))
| ~ is_a_theorem(X0)
| ~ necessitation ),
inference(cnf_transformation,[status(thm)],[f231]) ).
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(f264,plain,
( ( ? [X] : ~ is_a_theorem(implies(necessarily(X),necessarily(necessarily(X))))
| axiom_4 )
& ( ! [X] : is_a_theorem(implies(necessarily(X),necessarily(necessarily(X))))
| ~ axiom_4 ) ),
inference(NNF_transformation,[status(thm)],[f56]) ).
fof(f265,plain,
( ( ~ is_a_theorem(implies(necessarily(sK65_skl),necessarily(necessarily(sK65_skl))))
| axiom_4 )
& ( ! [X] : is_a_theorem(implies(necessarily(X),necessarily(necessarily(X))))
| ~ axiom_4 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK65_skl]),skolemize(X,sK65_skl)],[f264]) ).
fof(f266,plain,
! [X0] :
( is_a_theorem(implies(necessarily(X0),necessarily(necessarily(X0))))
| ~ axiom_4 ),
inference(cnf_transformation,[status(thm)],[f265]) ).
fof(f268,plain,
( ( ? [X] : ~ is_a_theorem(implies(X,necessarily(possibly(X))))
| axiom_B )
& ( ! [X] : is_a_theorem(implies(X,necessarily(possibly(X))))
| ~ axiom_B ) ),
inference(NNF_transformation,[status(thm)],[f57]) ).
fof(f269,plain,
( ( ~ is_a_theorem(implies(sK66_skl,necessarily(possibly(sK66_skl))))
| axiom_B )
& ( ! [X] : is_a_theorem(implies(X,necessarily(possibly(X))))
| ~ axiom_B ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK66_skl]),skolemize(X,sK66_skl)],[f268]) ).
fof(f270,plain,
! [X0] :
( is_a_theorem(implies(X0,necessarily(possibly(X0))))
| ~ axiom_B ),
inference(cnf_transformation,[status(thm)],[f269]) ).
fof(f328,plain,
( ( ? [X] : ~ is_a_theorem(strict_implies(possibly(X),necessarily(possibly(X))))
| axiom_m10 )
& ( ! [X] : is_a_theorem(strict_implies(possibly(X),necessarily(possibly(X))))
| ~ axiom_m10 ) ),
inference(NNF_transformation,[status(thm)],[f72]) ).
fof(f329,plain,
( ( ~ is_a_theorem(strict_implies(possibly(sK93_skl),necessarily(possibly(sK93_skl))))
| axiom_m10 )
& ( ! [X] : is_a_theorem(strict_implies(possibly(X),necessarily(possibly(X))))
| ~ axiom_m10 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK93_skl]),skolemize(X,sK93_skl)],[f328]) ).
fof(f331,plain,
( ~ is_a_theorem(strict_implies(possibly(sK93_skl),necessarily(possibly(sK93_skl))))
| axiom_m10 ),
inference(cnf_transformation,[status(thm)],[f329]) ).
fof(f332,plain,
( ! [X] : possibly(X) = not(necessarily(not(X)))
| ~ op_possibly ),
inference(pre_NNF_transformation,[status(thm)],[f73]) ).
fof(f333,plain,
! [X0] :
( possibly(X0) = not(necessarily(not(X0)))
| ~ op_possibly ),
inference(cnf_transformation,[status(thm)],[f332]) ).
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(f340,plain,
op_possibly,
inference(cnf_transformation,[status(thm)],[f77]) ).
fof(f341,plain,
necessitation,
inference(cnf_transformation,[status(thm)],[f78]) ).
fof(f343,plain,
axiom_M,
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f344,plain,
axiom_4,
inference(cnf_transformation,[status(thm)],[f81]) ).
fof(f345,plain,
axiom_B,
inference(cnf_transformation,[status(thm)],[f82]) ).
fof(f349,plain,
op_strict_implies,
inference(cnf_transformation,[status(thm)],[f86]) ).
fof(f352,plain,
~ axiom_m10,
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(f387,definition,
( sQ9_spl
<=> modus_tollens ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f389,plain,
( sQ9_spl
| ~ modus_tollens ),
inference(component_clause,[status(thm)],[f387]) ).
fof(f390,definition,
! [X0,X1] :
( sQ10_spl
<=> is_a_theorem(implies(implies(not(X0),not(X1)),implies(X1,X0))) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f391,plain,
! [X0,X1] :
( ~ sQ10_spl
| is_a_theorem(implies(implies(not(X0),not(X1)),implies(X1,X0))) ),
inference(component_clause,[status(thm)],[f390]) ).
fof(f393,plain,
( sQ10_spl
| ~ sQ9_spl ),
inference(split_clause,[status(thm)],[f107,f387,f390]) ).
fof(f409,definition,
( sQ15_spl
<=> implies_2 ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f411,plain,
( sQ15_spl
| ~ implies_2 ),
inference(component_clause,[status(thm)],[f409]) ).
fof(f412,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(f413,plain,
! [X0,X1] :
( ~ sQ16_spl
| is_a_theorem(implies(implies(X0,implies(X0,X1)),implies(X0,X1))) ),
inference(component_clause,[status(thm)],[f412]) ).
fof(f415,plain,
( sQ16_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f115,f409,f412]) ).
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(f464,definition,
( sQ30_spl
<=> or_1 ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f466,plain,
( sQ30_spl
| ~ or_1 ),
inference(component_clause,[status(thm)],[f464]) ).
fof(f467,definition,
! [X0,X1] :
( sQ31_spl
<=> is_a_theorem(implies(X0,or(X0,X1))) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f468,plain,
! [X0,X1] :
( ~ sQ31_spl
| is_a_theorem(implies(X0,or(X0,X1))) ),
inference(component_clause,[status(thm)],[f467]) ).
fof(f470,plain,
( sQ31_spl
| ~ sQ30_spl ),
inference(split_clause,[status(thm)],[f135,f464,f467]) ).
fof(f533,definition,
! [X0] :
( sQ49_spl
<=> is_a_theorem(implies(X0,and(X0,X0))) ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f534,plain,
! [X0] :
( ~ sQ49_spl
| is_a_theorem(implies(X0,and(X0,X0))) ),
inference(component_clause,[status(thm)],[f533]) ).
fof(f590,definition,
( sQ64_spl
<=> r1 ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f593,definition,
! [X0] :
( sQ65_spl
<=> is_a_theorem(implies(or(X0,X0),X0)) ),
introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition]) ).
fof(f594,plain,
! [X0] :
( ~ sQ65_spl
| is_a_theorem(implies(or(X0,X0),X0)) ),
inference(component_clause,[status(thm)],[f593]) ).
fof(f596,plain,
( sQ65_spl
| ~ sQ64_spl ),
inference(split_clause,[status(thm)],[f183,f590,f593]) ).
fof(f597,definition,
( sQ66_spl
<=> is_a_theorem(implies(or(sK44_skl,sK44_skl),sK44_skl)) ),
introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition]) ).
fof(f599,plain,
( sQ66_spl
| ~ is_a_theorem(implies(or(sK44_skl,sK44_skl),sK44_skl)) ),
inference(component_clause,[status(thm)],[f597]) ).
fof(f600,plain,
( ~ sQ66_spl
| sQ64_spl ),
inference(split_clause,[status(thm)],[f184,f590,f597]) ).
fof(f642,definition,
( sQ78_spl
<=> op_or ),
introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition]) ).
fof(f644,plain,
( sQ78_spl
| ~ op_or ),
inference(component_clause,[status(thm)],[f642]) ).
fof(f645,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(f646,plain,
! [X0,X1] :
( ~ sQ79_spl
| or(X0,X1) = not(and(not(X0),not(X1))) ),
inference(component_clause,[status(thm)],[f645]) ).
fof(f648,plain,
( sQ79_spl
| ~ sQ78_spl ),
inference(split_clause,[status(thm)],[f202,f642,f645]) ).
fof(f656,definition,
( sQ82_spl
<=> op_implies_and ),
introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition]) ).
fof(f658,plain,
( sQ82_spl
| ~ op_implies_and ),
inference(component_clause,[status(thm)],[f656]) ).
fof(f659,definition,
! [X0,X1] :
( sQ83_spl
<=> implies(X0,X1) = not(and(X0,not(X1))) ),
introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition]) ).
fof(f660,plain,
! [X0,X1] :
( ~ sQ83_spl
| implies(X0,X1) = not(and(X0,not(X1))) ),
inference(component_clause,[status(thm)],[f659]) ).
fof(f662,plain,
( sQ83_spl
| ~ sQ82_spl ),
inference(split_clause,[status(thm)],[f206,f656,f659]) ).
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(f677,definition,
( sQ88_spl
<=> necessitation ),
introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition]) ).
fof(f679,plain,
( sQ88_spl
| ~ necessitation ),
inference(component_clause,[status(thm)],[f677]) ).
fof(f680,definition,
! [X0] :
( sQ89_spl
<=> ( is_a_theorem(necessarily(X0))
| ~ is_a_theorem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition]) ).
fof(f681,plain,
! [X0] :
( ~ sQ89_spl
| is_a_theorem(necessarily(X0))
| ~ is_a_theorem(X0) ),
inference(component_clause,[status(thm)],[f680]) ).
fof(f683,plain,
( sQ89_spl
| ~ sQ88_spl ),
inference(split_clause,[status(thm)],[f232,f677,f680]) ).
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(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(f767,definition,
( sQ112_spl
<=> axiom_4 ),
introduced(definition,[new_symbols(definition,[sQ112_spl])],[split_symbol_definition]) ).
fof(f769,plain,
( sQ112_spl
| ~ axiom_4 ),
inference(component_clause,[status(thm)],[f767]) ).
fof(f770,definition,
! [X0] :
( sQ113_spl
<=> is_a_theorem(implies(necessarily(X0),necessarily(necessarily(X0)))) ),
introduced(definition,[new_symbols(definition,[sQ113_spl])],[split_symbol_definition]) ).
fof(f771,plain,
! [X0] :
( ~ sQ113_spl
| is_a_theorem(implies(necessarily(X0),necessarily(necessarily(X0)))) ),
inference(component_clause,[status(thm)],[f770]) ).
fof(f773,plain,
( sQ113_spl
| ~ sQ112_spl ),
inference(split_clause,[status(thm)],[f266,f767,f770]) ).
fof(f778,definition,
( sQ115_spl
<=> axiom_B ),
introduced(definition,[new_symbols(definition,[sQ115_spl])],[split_symbol_definition]) ).
fof(f780,plain,
( sQ115_spl
| ~ axiom_B ),
inference(component_clause,[status(thm)],[f778]) ).
fof(f781,definition,
! [X0] :
( sQ116_spl
<=> is_a_theorem(implies(X0,necessarily(possibly(X0)))) ),
introduced(definition,[new_symbols(definition,[sQ116_spl])],[split_symbol_definition]) ).
fof(f782,plain,
! [X0] :
( ~ sQ116_spl
| is_a_theorem(implies(X0,necessarily(possibly(X0)))) ),
inference(component_clause,[status(thm)],[f781]) ).
fof(f784,plain,
( sQ116_spl
| ~ sQ115_spl ),
inference(split_clause,[status(thm)],[f270,f778,f781]) ).
fof(f943,definition,
( sQ160_spl
<=> axiom_m10 ),
introduced(definition,[new_symbols(definition,[sQ160_spl])],[split_symbol_definition]) ).
fof(f944,plain,
( ~ sQ160_spl
| axiom_m10 ),
inference(component_clause,[status(thm)],[f943]) ).
fof(f946,definition,
! [X0] :
( sQ161_spl
<=> is_a_theorem(strict_implies(possibly(X0),necessarily(possibly(X0)))) ),
introduced(definition,[new_symbols(definition,[sQ161_spl])],[split_symbol_definition]) ).
fof(f947,plain,
! [X0] :
( ~ sQ161_spl
| is_a_theorem(strict_implies(possibly(X0),necessarily(possibly(X0)))) ),
inference(component_clause,[status(thm)],[f946]) ).
fof(f950,definition,
( sQ162_spl
<=> is_a_theorem(strict_implies(possibly(sK93_skl),necessarily(possibly(sK93_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ162_spl])],[split_symbol_definition]) ).
fof(f952,plain,
( sQ162_spl
| ~ is_a_theorem(strict_implies(possibly(sK93_skl),necessarily(possibly(sK93_skl)))) ),
inference(component_clause,[status(thm)],[f950]) ).
fof(f953,plain,
( ~ sQ162_spl
| sQ160_spl ),
inference(split_clause,[status(thm)],[f331,f943,f950]) ).
fof(f954,definition,
( sQ163_spl
<=> op_possibly ),
introduced(definition,[new_symbols(definition,[sQ163_spl])],[split_symbol_definition]) ).
fof(f956,plain,
( sQ163_spl
| ~ op_possibly ),
inference(component_clause,[status(thm)],[f954]) ).
fof(f957,definition,
! [X0] :
( sQ164_spl
<=> possibly(X0) = not(necessarily(not(X0))) ),
introduced(definition,[new_symbols(definition,[sQ164_spl])],[split_symbol_definition]) ).
fof(f958,plain,
! [X0] :
( ~ sQ164_spl
| possibly(X0) = not(necessarily(not(X0))) ),
inference(component_clause,[status(thm)],[f957]) ).
fof(f960,plain,
( sQ164_spl
| ~ sQ163_spl ),
inference(split_clause,[status(thm)],[f333,f954,f957]) ).
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(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(f986,plain,
( sQ88_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f679,f341]) ).
fof(f987,plain,
sQ88_spl,
inference(contradiction_clause,[status(thm)],[f986]) ).
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(f992,plain,
( sQ163_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f956,f340]) ).
fof(f993,plain,
sQ163_spl,
inference(contradiction_clause,[status(thm)],[f992]) ).
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(f996,plain,
( sQ82_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f658,f212]) ).
fof(f997,plain,
sQ82_spl,
inference(contradiction_clause,[status(thm)],[f996]) ).
fof(f998,plain,
( sQ162_spl
| ~ sQ161_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f952,f947]) ).
fof(f999,plain,
( sQ162_spl
| ~ sQ161_spl ),
inference(contradiction_clause,[status(thm)],[f998]) ).
fof(f1000,plain,
( sQ78_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f644,f211]) ).
fof(f1001,plain,
sQ78_spl,
inference(contradiction_clause,[status(thm)],[f1000]) ).
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(f1025,plain,
! [X0,X1] :
( ~ sQ168_spl
| ~ sQ89_spl
| is_a_theorem(strict_implies(X0,X1))
| ~ is_a_theorem(implies(X0,X1)) ),
inference(paramodulation,[status(thm)],[f972,f681]) ).
fof(f1042,plain,
( sQ115_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f780,f345]) ).
fof(f1043,plain,
sQ115_spl,
inference(contradiction_clause,[status(thm)],[f1042]) ).
fof(f1063,plain,
( sQ112_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f769,f344]) ).
fof(f1064,plain,
sQ112_spl,
inference(contradiction_clause,[status(thm)],[f1063]) ).
fof(f1084,plain,
( sQ30_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f466,f222]) ).
fof(f1085,plain,
sQ30_spl,
inference(contradiction_clause,[status(thm)],[f1084]) ).
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(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(f1153,plain,
! [X0] :
( ~ sQ116_spl
| ~ sQ168_spl
| ~ sQ89_spl
| is_a_theorem(strict_implies(X0,necessarily(possibly(X0)))) ),
inference(resolution,[status(thm)],[f1025,f782]) ).
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(f1174,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)],[f413,f357]) ).
fof(f1176,plain,
( sQ15_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f411,f217]) ).
fof(f1177,plain,
sQ15_spl,
inference(contradiction_clause,[status(thm)],[f1176]) ).
fof(f1181,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ sQ10_spl
| is_a_theorem(implies(X1,X0))
| ~ is_a_theorem(implies(not(X0),not(X1))) ),
inference(resolution,[status(thm)],[f391,f357]) ).
fof(f1187,plain,
( sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f389,f215]) ).
fof(f1188,plain,
sQ9_spl,
inference(contradiction_clause,[status(thm)],[f1187]) ).
fof(f1207,plain,
! [X0,X1] :
( ~ sQ79_spl
| ~ sQ83_spl
| or(X0,X1) = implies(not(X0),X1) ),
inference(forward_demodulation,[status(thm)],[f660,f646]) ).
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(f1694,plain,
! [X0,X1] :
( ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ31_spl
| is_a_theorem(or(X0,or(not(X0),X1))) ),
inference(paramodulation,[status(thm)],[f1207,f468]) ).
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(f2039,plain,
! [X0] :
( ~ sQ28_spl
| ~ sQ1_spl
| ~ sQ16_spl
| is_a_theorem(implies(X0,and(X0,X0))) ),
inference(resolution,[status(thm)],[f1174,f457]) ).
fof(f2047,plain,
( ~ sQ28_spl
| ~ sQ1_spl
| ~ sQ16_spl
| sQ49_spl ),
inference(split_clause,[status(thm)],[f2039,f533,f412,f356,f456]) ).
fof(f2084,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ sQ10_spl
| ~ sQ79_spl
| ~ sQ83_spl
| is_a_theorem(implies(X1,X0))
| ~ is_a_theorem(or(X0,not(X1))) ),
inference(forward_demodulation,[status(thm)],[f1207,f1181]) ).
fof(f3819,plain,
! [X0] :
( ~ sQ113_spl
| ~ sQ87_spl
| ~ sQ98_spl
| is_a_theorem(equiv(necessarily(necessarily(X0)),necessarily(X0)))
| ~ is_a_theorem(implies(necessarily(necessarily(X0)),necessarily(X0))) ),
inference(resolution,[status(thm)],[f1390,f771]) ).
fof(f3829,plain,
! [X0] :
( ~ sQ49_spl
| ~ sQ87_spl
| ~ sQ98_spl
| is_a_theorem(equiv(and(X0,X0),X0))
| ~ is_a_theorem(implies(and(X0,X0),X0)) ),
inference(resolution,[status(thm)],[f1390,f534]) ).
fof(f3865,plain,
! [X0] :
( ~ sQ113_spl
| ~ sQ87_spl
| ~ sQ98_spl
| ~ sQ110_spl
| is_a_theorem(equiv(necessarily(necessarily(X0)),necessarily(X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f3819,f760]) ).
fof(f3868,plain,
! [X0] :
( ~ sQ49_spl
| ~ sQ87_spl
| ~ sQ98_spl
| ~ sQ25_spl
| is_a_theorem(equiv(and(X0,X0),X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f3829,f446]) ).
fof(f3935,plain,
! [X0] :
( ~ sQ6_spl
| ~ sQ49_spl
| ~ sQ87_spl
| ~ sQ98_spl
| ~ sQ25_spl
| and(X0,X0) = X0 ),
inference(resolution,[status(thm)],[f3868,f376]) ).
fof(f4013,plain,
! [X0] :
( ~ sQ6_spl
| ~ sQ49_spl
| ~ sQ87_spl
| ~ sQ98_spl
| ~ sQ25_spl
| ~ sQ83_spl
| implies(not(X0),X0) = not(not(X0)) ),
inference(paramodulation,[status(thm)],[f3935,f660]) ).
fof(f4037,plain,
! [X0] :
( ~ sQ6_spl
| ~ sQ49_spl
| ~ sQ87_spl
| ~ sQ98_spl
| ~ sQ25_spl
| ~ sQ83_spl
| ~ sQ79_spl
| or(X0,X0) = not(not(X0)) ),
inference(forward_demodulation,[status(thm)],[f1207,f4013]) ).
fof(f4345,plain,
( sQ66_spl
| ~ sQ6_spl
| ~ sQ49_spl
| ~ sQ87_spl
| ~ sQ98_spl
| ~ sQ25_spl
| ~ sQ83_spl
| ~ sQ79_spl
| ~ is_a_theorem(implies(not(not(sK44_skl)),sK44_skl)) ),
inference(backward_demodulation,[status(thm)],[f4037,f599]) ).
fof(f4357,plain,
! [X0] :
( ~ sQ6_spl
| ~ sQ49_spl
| ~ sQ87_spl
| ~ sQ98_spl
| ~ sQ25_spl
| ~ sQ83_spl
| ~ sQ79_spl
| ~ sQ31_spl
| is_a_theorem(or(X0,not(not(not(X0))))) ),
inference(paramodulation,[status(thm)],[f4037,f1694]) ).
fof(f4393,plain,
! [X0] :
( ~ sQ6_spl
| ~ sQ49_spl
| ~ sQ87_spl
| ~ sQ98_spl
| ~ sQ25_spl
| ~ sQ83_spl
| ~ sQ79_spl
| ~ sQ31_spl
| is_a_theorem(implies(X0,not(not(X0)))) ),
inference(paramodulation,[status(thm)],[f4037,f468]) ).
fof(f4397,plain,
( sQ66_spl
| ~ sQ6_spl
| ~ sQ49_spl
| ~ sQ87_spl
| ~ sQ98_spl
| ~ sQ25_spl
| ~ sQ83_spl
| ~ sQ79_spl
| ~ is_a_theorem(or(not(sK44_skl),sK44_skl)) ),
inference(forward_demodulation,[status(thm)],[f1207,f4345]) ).
fof(f4732,plain,
! [X0] :
( ~ sQ164_spl
| ~ sQ6_spl
| ~ sQ49_spl
| ~ sQ87_spl
| ~ sQ98_spl
| ~ sQ25_spl
| ~ sQ83_spl
| ~ sQ79_spl
| ~ sQ31_spl
| is_a_theorem(implies(necessarily(not(X0)),not(possibly(X0)))) ),
inference(paramodulation,[status(thm)],[f958,f4393]) ).
fof(f5018,plain,
! [X0] :
( ~ sQ65_spl
| ~ sQ6_spl
| ~ sQ49_spl
| ~ sQ87_spl
| ~ sQ98_spl
| ~ sQ25_spl
| ~ sQ83_spl
| ~ sQ79_spl
| is_a_theorem(implies(not(not(X0)),X0)) ),
inference(forward_demodulation,[status(thm)],[f4037,f594]) ).
fof(f5019,plain,
! [X0] :
( ~ sQ65_spl
| ~ sQ6_spl
| ~ sQ49_spl
| ~ sQ87_spl
| ~ sQ98_spl
| ~ sQ25_spl
| ~ sQ83_spl
| ~ sQ79_spl
| is_a_theorem(or(not(X0),X0)) ),
inference(forward_demodulation,[status(thm)],[f1207,f5018]) ).
fof(f5032,plain,
! [X0] :
( ~ sQ164_spl
| ~ sQ65_spl
| ~ sQ6_spl
| ~ sQ49_spl
| ~ sQ87_spl
| ~ sQ98_spl
| ~ sQ25_spl
| ~ sQ83_spl
| ~ sQ79_spl
| is_a_theorem(or(possibly(X0),necessarily(not(X0)))) ),
inference(paramodulation,[status(thm)],[f958,f5019]) ).
fof(f5147,plain,
! [X0] :
( ~ sQ6_spl
| ~ sQ113_spl
| ~ sQ87_spl
| ~ sQ98_spl
| ~ sQ110_spl
| necessarily(necessarily(X0)) = necessarily(X0) ),
inference(resolution,[status(thm)],[f3865,f376]) ).
fof(f5476,plain,
! [X0] :
( ~ sQ1_spl
| ~ sQ10_spl
| ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ6_spl
| ~ sQ49_spl
| ~ sQ87_spl
| ~ sQ98_spl
| ~ sQ25_spl
| ~ sQ31_spl
| is_a_theorem(implies(not(not(X0)),X0)) ),
inference(resolution,[status(thm)],[f4357,f2084]) ).
fof(f5485,plain,
! [X0] :
( ~ sQ1_spl
| ~ sQ10_spl
| ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ6_spl
| ~ sQ49_spl
| ~ sQ87_spl
| ~ sQ98_spl
| ~ sQ25_spl
| ~ sQ31_spl
| is_a_theorem(or(not(X0),X0)) ),
inference(forward_demodulation,[status(thm)],[f1207,f5476]) ).
fof(f5493,plain,
( sQ66_spl
| ~ sQ6_spl
| ~ sQ49_spl
| ~ sQ87_spl
| ~ sQ98_spl
| ~ sQ25_spl
| ~ sQ83_spl
| ~ sQ79_spl
| ~ sQ1_spl
| ~ sQ10_spl
| ~ sQ31_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f4397,f5485]) ).
fof(f5501,plain,
( sQ66_spl
| ~ sQ6_spl
| ~ sQ49_spl
| ~ sQ87_spl
| ~ sQ98_spl
| ~ sQ25_spl
| ~ sQ83_spl
| ~ sQ79_spl
| ~ sQ1_spl
| ~ sQ10_spl
| ~ sQ31_spl ),
inference(contradiction_clause,[status(thm)],[f5493]) ).
fof(f6528,plain,
! [X0] :
( ~ sQ87_spl
| ~ sQ98_spl
| ~ sQ164_spl
| ~ sQ6_spl
| ~ sQ49_spl
| ~ sQ25_spl
| ~ sQ83_spl
| ~ sQ79_spl
| ~ sQ31_spl
| is_a_theorem(equiv(not(possibly(X0)),necessarily(not(X0))))
| ~ is_a_theorem(implies(not(possibly(X0)),necessarily(not(X0)))) ),
inference(resolution,[status(thm)],[f4732,f1390]) ).
fof(f6536,plain,
! [X0] :
( ~ sQ87_spl
| ~ sQ98_spl
| ~ sQ164_spl
| ~ sQ6_spl
| ~ sQ49_spl
| ~ sQ25_spl
| ~ sQ83_spl
| ~ sQ79_spl
| ~ sQ31_spl
| is_a_theorem(equiv(not(possibly(X0)),necessarily(not(X0))))
| ~ is_a_theorem(or(possibly(X0),necessarily(not(X0)))) ),
inference(forward_demodulation,[status(thm)],[f1207,f6528]) ).
fof(f6537,plain,
! [X0] :
( ~ sQ87_spl
| ~ sQ98_spl
| ~ sQ164_spl
| ~ sQ6_spl
| ~ sQ49_spl
| ~ sQ25_spl
| ~ sQ83_spl
| ~ sQ79_spl
| ~ sQ31_spl
| ~ sQ65_spl
| is_a_theorem(equiv(not(possibly(X0)),necessarily(not(X0)))) ),
inference(forward_subsumption_resolution,[status(thm)],[f6536,f5032]) ).
fof(f7211,plain,
! [X0] :
( ~ sQ6_spl
| ~ sQ87_spl
| ~ sQ98_spl
| ~ sQ164_spl
| ~ sQ49_spl
| ~ sQ25_spl
| ~ sQ83_spl
| ~ sQ79_spl
| ~ sQ31_spl
| ~ sQ65_spl
| not(possibly(X0)) = necessarily(not(X0)) ),
inference(resolution,[status(thm)],[f6537,f376]) ).
fof(f7242,plain,
! [X0] :
( ~ sQ164_spl
| ~ sQ6_spl
| ~ sQ87_spl
| ~ sQ98_spl
| ~ sQ49_spl
| ~ sQ25_spl
| ~ sQ83_spl
| ~ sQ79_spl
| ~ sQ31_spl
| ~ sQ65_spl
| possibly(X0) = not(not(possibly(X0))) ),
inference(backward_demodulation,[status(thm)],[f7211,f958]) ).
fof(f7252,plain,
! [X0] :
( ~ sQ6_spl
| ~ sQ87_spl
| ~ sQ98_spl
| ~ sQ164_spl
| ~ sQ49_spl
| ~ sQ25_spl
| ~ sQ83_spl
| ~ sQ79_spl
| ~ sQ31_spl
| ~ sQ65_spl
| ~ sQ113_spl
| ~ sQ110_spl
| necessarily(not(possibly(X0))) = necessarily(not(X0)) ),
inference(paramodulation,[status(thm)],[f7211,f5147]) ).
fof(f7278,plain,
! [X0] :
( ~ sQ6_spl
| ~ sQ87_spl
| ~ sQ98_spl
| ~ sQ164_spl
| ~ sQ49_spl
| ~ sQ25_spl
| ~ sQ83_spl
| ~ sQ79_spl
| ~ sQ31_spl
| ~ sQ65_spl
| ~ sQ113_spl
| ~ sQ110_spl
| not(possibly(possibly(X0))) = necessarily(not(X0)) ),
inference(forward_demodulation,[status(thm)],[f7211,f7252]) ).
fof(f7279,plain,
! [X0] :
( ~ sQ6_spl
| ~ sQ87_spl
| ~ sQ98_spl
| ~ sQ164_spl
| ~ sQ49_spl
| ~ sQ25_spl
| ~ sQ83_spl
| ~ sQ79_spl
| ~ sQ31_spl
| ~ sQ65_spl
| ~ sQ113_spl
| ~ sQ110_spl
| not(possibly(possibly(X0))) = not(possibly(X0)) ),
inference(forward_demodulation,[status(thm)],[f7211,f7278]) ).
fof(f7571,plain,
! [X0] :
( ~ sQ6_spl
| ~ sQ87_spl
| ~ sQ98_spl
| ~ sQ164_spl
| ~ sQ49_spl
| ~ sQ25_spl
| ~ sQ83_spl
| ~ sQ79_spl
| ~ sQ31_spl
| ~ sQ65_spl
| ~ sQ113_spl
| ~ sQ110_spl
| possibly(possibly(X0)) = not(not(possibly(X0))) ),
inference(paramodulation,[status(thm)],[f7279,f7242]) ).
fof(f7664,plain,
! [X0] :
( ~ sQ6_spl
| ~ sQ87_spl
| ~ sQ98_spl
| ~ sQ164_spl
| ~ sQ49_spl
| ~ sQ25_spl
| ~ sQ83_spl
| ~ sQ79_spl
| ~ sQ31_spl
| ~ sQ65_spl
| ~ sQ113_spl
| ~ sQ110_spl
| possibly(possibly(X0)) = possibly(X0) ),
inference(forward_demodulation,[status(thm)],[f7242,f7571]) ).
fof(f7730,plain,
! [X0] :
( ~ sQ6_spl
| ~ sQ87_spl
| ~ sQ98_spl
| ~ sQ164_spl
| ~ sQ49_spl
| ~ sQ25_spl
| ~ sQ83_spl
| ~ sQ79_spl
| ~ sQ31_spl
| ~ sQ65_spl
| ~ sQ113_spl
| ~ sQ110_spl
| ~ sQ116_spl
| ~ sQ168_spl
| ~ sQ89_spl
| is_a_theorem(strict_implies(possibly(X0),necessarily(possibly(X0)))) ),
inference(paramodulation,[status(thm)],[f7664,f1153]) ).
fof(f7748,plain,
( ~ sQ6_spl
| ~ sQ87_spl
| ~ sQ98_spl
| ~ sQ164_spl
| ~ sQ49_spl
| ~ sQ25_spl
| ~ sQ83_spl
| ~ sQ79_spl
| ~ sQ31_spl
| ~ sQ65_spl
| ~ sQ113_spl
| ~ sQ110_spl
| ~ sQ116_spl
| ~ sQ168_spl
| ~ sQ89_spl
| sQ161_spl ),
inference(split_clause,[status(thm)],[f7730,f946,f680,f971,f781,f759,f770,f593,f467,f645,f659,f445,f533,f957,f714,f673,f375]) ).
fof(f7750,plain,
( ~ sQ160_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f944,f352]) ).
fof(f7751,plain,
~ sQ160_spl,
inference(contradiction_clause,[status(thm)],[f7750]) ).
fof(f7752,plain,
$false,
inference(sat_refutation,[status(thm)],[f359,f378,f393,f415,f448,f459,f470,f596,f600,f648,f662,f676,f683,f762,f773,f784,f953,f960,f974,f985,f987,f989,f991,f993,f995,f997,f999,f1001,f1023,f1043,f1064,f1085,f1097,f1169,f1177,f1188,f1820,f2047,f5501,f7748,f7751]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL549+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.35 % Computer : n006.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Mon Sep 21 00:37:57 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.14/0.36 % Drodi V4.1.1
% 5.68/1.37 % Refutation found
% 5.68/1.37 % SZS status Theorem for theBenchmark: Theorem is valid
% 5.68/1.37 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 5.68/1.41 % Elapsed time: 1.044595 seconds
% 5.68/1.41 % CPU time: 7.865690 seconds
% 5.68/1.41 % Total memory used: 214.240 MB
% 5.68/1.41 % Net memory used: 206.211 MB
%------------------------------------------------------------------------------