%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LCL551+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 : n012.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 83.15s 10.87s
% Output : CNFRefutation 42.01s
% Verified :
% SZS Type : Refutation
% Derivation depth : 43
% Number of leaves : 62
% Syntax : Number of formulae : 313 ( 47 unt; 32 def)
% Number of atoms : 1536 ( 82 equ)
% Maximal formula atoms : 17 ( 4 avg)
% Number of connectives : 2344 (1121 ~;1131 |; 37 &)
% ( 46 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 7 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 50 ( 48 usr; 48 prp; 0-2 aty)
% Number of functors : 29 ( 29 usr; 21 con; 0-2 aty)
% Number of variables : 411 ( 388 !; 23 ?)
% Comments :
%------------------------------------------------------------------------------
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(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(f33,axiom,
( modus_ponens_strict_implies
<=> ! [X,Y] :
( ( is_a_theorem(strict_implies(X,Y))
& is_a_theorem(X) )
=> is_a_theorem(Y) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f34,axiom,
( adjunction
<=> ! [X,Y] :
( ( is_a_theorem(Y)
& is_a_theorem(X) )
=> is_a_theorem(and(X,Y)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f35,axiom,
( substitution_strict_equiv
<=> ! [X,Y] :
( is_a_theorem(strict_equiv(X,Y))
=> X = Y ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f45,axiom,
( axiom_m1
<=> ! [X,Y] : is_a_theorem(strict_implies(and(X,Y),and(Y,X))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f46,axiom,
( axiom_m2
<=> ! [X,Y] : is_a_theorem(strict_implies(and(X,Y),X)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f47,axiom,
( axiom_m3
<=> ! [X,Y,Z] : is_a_theorem(strict_implies(and(and(X,Y),Z),and(X,and(Y,Z)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f48,axiom,
( axiom_m4
<=> ! [X] : is_a_theorem(strict_implies(X,and(X,X))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f49,axiom,
( axiom_m5
<=> ! [X,Y,Z] : is_a_theorem(strict_implies(and(strict_implies(X,Y),strict_implies(Y,Z)),strict_implies(X,Z))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f57,axiom,
( op_strict_implies
=> ! [X,Y] : strict_implies(X,Y) = necessarily(implies(X,Y)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f58,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(f60,axiom,
op_or,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f62,axiom,
op_strict_implies,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f63,axiom,
op_equiv,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f64,axiom,
op_strict_equiv,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f65,axiom,
modus_ponens_strict_implies,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f66,axiom,
substitution_strict_equiv,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f67,axiom,
adjunction,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f68,axiom,
axiom_m1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f69,axiom,
axiom_m2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f70,axiom,
axiom_m3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f71,axiom,
axiom_m4,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f72,axiom,
axiom_m5,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f74,axiom,
op_implies_and,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f76,axiom,
substitution_of_equivalents,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f77,conjecture,
modus_tollens,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f78,negated_conjecture,
~ modus_tollens,
inference(negated_conjecture,[status(cth)],[f77]) ).
fof(f87,plain,
( substitution_of_equivalents
<=> ! [X,Y] :
( X = Y
| ~ is_a_theorem(equiv(X,Y)) ) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f88,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)],[f87]) ).
fof(f89,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)],[f88]) ).
fof(f90,plain,
! [X0,X1] :
( X0 = X1
| ~ is_a_theorem(equiv(X0,X1))
| ~ substitution_of_equivalents ),
inference(cnf_transformation,[status(thm)],[f89]) ).
fof(f93,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(f94,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)],[f93]) ).
fof(f96,plain,
( ~ is_a_theorem(implies(implies(not(sK5_skl),not(sK4_skl)),implies(sK4_skl,sK5_skl)))
| modus_tollens ),
inference(cnf_transformation,[status(thm)],[f94]) ).
fof(f189,plain,
( ! [X,Y] : or(X,Y) = not(and(not(X),not(Y)))
| ~ op_or ),
inference(pre_NNF_transformation,[status(thm)],[f27]) ).
fof(f190,plain,
! [X0,X1] :
( or(X0,X1) = not(and(not(X0),not(X1)))
| ~ op_or ),
inference(cnf_transformation,[status(thm)],[f189]) ).
fof(f193,plain,
( ! [X,Y] : implies(X,Y) = not(and(X,not(Y)))
| ~ op_implies_and ),
inference(pre_NNF_transformation,[status(thm)],[f29]) ).
fof(f194,plain,
! [X0,X1] :
( implies(X0,X1) = not(and(X0,not(X1)))
| ~ op_implies_and ),
inference(cnf_transformation,[status(thm)],[f193]) ).
fof(f197,plain,
( ! [X,Y] : equiv(X,Y) = and(implies(X,Y),implies(Y,X))
| ~ op_equiv ),
inference(pre_NNF_transformation,[status(thm)],[f31]) ).
fof(f198,plain,
! [X0,X1] :
( equiv(X0,X1) = and(implies(X0,X1),implies(X1,X0))
| ~ op_equiv ),
inference(cnf_transformation,[status(thm)],[f197]) ).
fof(f205,plain,
( modus_ponens_strict_implies
<=> ! [X,Y] :
( is_a_theorem(Y)
| ~ is_a_theorem(strict_implies(X,Y))
| ~ is_a_theorem(X) ) ),
inference(pre_NNF_transformation,[status(thm)],[f33]) ).
fof(f206,plain,
( ( ? [X,Y] :
( ~ is_a_theorem(Y)
& is_a_theorem(strict_implies(X,Y))
& is_a_theorem(X) )
| modus_ponens_strict_implies )
& ( ! [X,Y] :
( is_a_theorem(Y)
| ~ is_a_theorem(strict_implies(X,Y))
| ~ is_a_theorem(X) )
| ~ modus_ponens_strict_implies ) ),
inference(NNF_transformation,[status(thm)],[f205]) ).
fof(f207,plain,
( ( ? [Y] :
( ~ is_a_theorem(Y)
& ? [X] :
( is_a_theorem(strict_implies(X,Y))
& is_a_theorem(X) ) )
| modus_ponens_strict_implies )
& ( ! [Y] :
( is_a_theorem(Y)
| ! [X] :
( ~ is_a_theorem(strict_implies(X,Y))
| ~ is_a_theorem(X) ) )
| ~ modus_ponens_strict_implies ) ),
inference(miniscoping,[status(thm)],[f206]) ).
fof(f208,plain,
( ( ( ~ is_a_theorem(sK56_skl)
& is_a_theorem(strict_implies(sK57_skl,sK56_skl))
& is_a_theorem(sK57_skl) )
| modus_ponens_strict_implies )
& ( ! [Y] :
( is_a_theorem(Y)
| ! [X] :
( ~ is_a_theorem(strict_implies(X,Y))
| ~ is_a_theorem(X) ) )
| ~ modus_ponens_strict_implies ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK56_skl,sK57_skl]),skolemize(Y,sK56_skl),skolemize(X,sK57_skl)],[f207]) ).
fof(f209,plain,
! [X0,X1] :
( is_a_theorem(X1)
| ~ is_a_theorem(strict_implies(X0,X1))
| ~ is_a_theorem(X0)
| ~ modus_ponens_strict_implies ),
inference(cnf_transformation,[status(thm)],[f208]) ).
fof(f213,plain,
( adjunction
<=> ! [X,Y] :
( is_a_theorem(and(X,Y))
| ~ is_a_theorem(Y)
| ~ is_a_theorem(X) ) ),
inference(pre_NNF_transformation,[status(thm)],[f34]) ).
fof(f214,plain,
( ( ? [X,Y] :
( ~ is_a_theorem(and(X,Y))
& is_a_theorem(Y)
& is_a_theorem(X) )
| adjunction )
& ( ! [X,Y] :
( is_a_theorem(and(X,Y))
| ~ is_a_theorem(Y)
| ~ is_a_theorem(X) )
| ~ adjunction ) ),
inference(NNF_transformation,[status(thm)],[f213]) ).
fof(f215,plain,
( ( ( ~ is_a_theorem(and(sK58_skl,sK59_skl))
& is_a_theorem(sK59_skl)
& is_a_theorem(sK58_skl) )
| adjunction )
& ( ! [X,Y] :
( is_a_theorem(and(X,Y))
| ~ is_a_theorem(Y)
| ~ is_a_theorem(X) )
| ~ adjunction ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK58_skl,sK59_skl]),skolemize(X,sK58_skl),skolemize(Y,sK59_skl)],[f214]) ).
fof(f216,plain,
! [X0,X1] :
( is_a_theorem(and(X0,X1))
| ~ is_a_theorem(X1)
| ~ is_a_theorem(X0)
| ~ adjunction ),
inference(cnf_transformation,[status(thm)],[f215]) ).
fof(f220,plain,
( substitution_strict_equiv
<=> ! [X,Y] :
( X = Y
| ~ is_a_theorem(strict_equiv(X,Y)) ) ),
inference(pre_NNF_transformation,[status(thm)],[f35]) ).
fof(f221,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)],[f220]) ).
fof(f222,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)],[f221]) ).
fof(f223,plain,
! [X0,X1] :
( X0 = X1
| ~ is_a_theorem(strict_equiv(X0,X1))
| ~ substitution_strict_equiv ),
inference(cnf_transformation,[status(thm)],[f222]) ).
fof(f262,plain,
( ( ? [X,Y] : ~ is_a_theorem(strict_implies(and(X,Y),and(Y,X)))
| axiom_m1 )
& ( ! [X,Y] : is_a_theorem(strict_implies(and(X,Y),and(Y,X)))
| ~ axiom_m1 ) ),
inference(NNF_transformation,[status(thm)],[f45]) ).
fof(f263,plain,
( ( ~ is_a_theorem(strict_implies(and(sK76_skl,sK77_skl),and(sK77_skl,sK76_skl)))
| axiom_m1 )
& ( ! [X,Y] : is_a_theorem(strict_implies(and(X,Y),and(Y,X)))
| ~ axiom_m1 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK76_skl,sK77_skl]),skolemize(X,sK76_skl),skolemize(Y,sK77_skl)],[f262]) ).
fof(f264,plain,
! [X0,X1] :
( is_a_theorem(strict_implies(and(X0,X1),and(X1,X0)))
| ~ axiom_m1 ),
inference(cnf_transformation,[status(thm)],[f263]) ).
fof(f266,plain,
( ( ? [X,Y] : ~ is_a_theorem(strict_implies(and(X,Y),X))
| axiom_m2 )
& ( ! [X,Y] : is_a_theorem(strict_implies(and(X,Y),X))
| ~ axiom_m2 ) ),
inference(NNF_transformation,[status(thm)],[f46]) ).
fof(f267,plain,
( ( ~ is_a_theorem(strict_implies(and(sK78_skl,sK79_skl),sK78_skl))
| axiom_m2 )
& ( ! [X,Y] : is_a_theorem(strict_implies(and(X,Y),X))
| ~ axiom_m2 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK78_skl,sK79_skl]),skolemize(X,sK78_skl),skolemize(Y,sK79_skl)],[f266]) ).
fof(f268,plain,
! [X0,X1] :
( is_a_theorem(strict_implies(and(X0,X1),X0))
| ~ axiom_m2 ),
inference(cnf_transformation,[status(thm)],[f267]) ).
fof(f270,plain,
( ( ? [X,Y,Z] : ~ is_a_theorem(strict_implies(and(and(X,Y),Z),and(X,and(Y,Z))))
| axiom_m3 )
& ( ! [X,Y,Z] : is_a_theorem(strict_implies(and(and(X,Y),Z),and(X,and(Y,Z))))
| ~ axiom_m3 ) ),
inference(NNF_transformation,[status(thm)],[f47]) ).
fof(f271,plain,
( ( ~ is_a_theorem(strict_implies(and(and(sK80_skl,sK81_skl),sK82_skl),and(sK80_skl,and(sK81_skl,sK82_skl))))
| axiom_m3 )
& ( ! [X,Y,Z] : is_a_theorem(strict_implies(and(and(X,Y),Z),and(X,and(Y,Z))))
| ~ axiom_m3 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK80_skl,sK81_skl,sK82_skl]),skolemize(X,sK80_skl),skolemize(Y,sK81_skl),skolemize(Z,sK82_skl)],[f270]) ).
fof(f272,plain,
! [X0,X1,X2] :
( is_a_theorem(strict_implies(and(and(X0,X1),X2),and(X0,and(X1,X2))))
| ~ axiom_m3 ),
inference(cnf_transformation,[status(thm)],[f271]) ).
fof(f274,plain,
( ( ? [X] : ~ is_a_theorem(strict_implies(X,and(X,X)))
| axiom_m4 )
& ( ! [X] : is_a_theorem(strict_implies(X,and(X,X)))
| ~ axiom_m4 ) ),
inference(NNF_transformation,[status(thm)],[f48]) ).
fof(f275,plain,
( ( ~ is_a_theorem(strict_implies(sK83_skl,and(sK83_skl,sK83_skl)))
| axiom_m4 )
& ( ! [X] : is_a_theorem(strict_implies(X,and(X,X)))
| ~ axiom_m4 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK83_skl]),skolemize(X,sK83_skl)],[f274]) ).
fof(f276,plain,
! [X0] :
( is_a_theorem(strict_implies(X0,and(X0,X0)))
| ~ axiom_m4 ),
inference(cnf_transformation,[status(thm)],[f275]) ).
fof(f278,plain,
( ( ? [X,Y,Z] : ~ is_a_theorem(strict_implies(and(strict_implies(X,Y),strict_implies(Y,Z)),strict_implies(X,Z)))
| axiom_m5 )
& ( ! [X,Y,Z] : is_a_theorem(strict_implies(and(strict_implies(X,Y),strict_implies(Y,Z)),strict_implies(X,Z)))
| ~ axiom_m5 ) ),
inference(NNF_transformation,[status(thm)],[f49]) ).
fof(f279,plain,
( ( ~ is_a_theorem(strict_implies(and(strict_implies(sK84_skl,sK85_skl),strict_implies(sK85_skl,sK86_skl)),strict_implies(sK84_skl,sK86_skl)))
| axiom_m5 )
& ( ! [X,Y,Z] : is_a_theorem(strict_implies(and(strict_implies(X,Y),strict_implies(Y,Z)),strict_implies(X,Z)))
| ~ axiom_m5 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK84_skl,sK85_skl,sK86_skl]),skolemize(X,sK84_skl),skolemize(Y,sK85_skl),skolemize(Z,sK86_skl)],[f278]) ).
fof(f280,plain,
! [X0,X1,X2] :
( is_a_theorem(strict_implies(and(strict_implies(X0,X1),strict_implies(X1,X2)),strict_implies(X0,X2)))
| ~ axiom_m5 ),
inference(cnf_transformation,[status(thm)],[f279]) ).
fof(f306,plain,
( ! [X,Y] : strict_implies(X,Y) = necessarily(implies(X,Y))
| ~ op_strict_implies ),
inference(pre_NNF_transformation,[status(thm)],[f57]) ).
fof(f307,plain,
! [X0,X1] :
( strict_implies(X0,X1) = necessarily(implies(X0,X1))
| ~ op_strict_implies ),
inference(cnf_transformation,[status(thm)],[f306]) ).
fof(f308,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)],[f58]) ).
fof(f309,plain,
! [X0,X1] :
( strict_equiv(X0,X1) = and(strict_implies(X0,X1),strict_implies(X1,X0))
| ~ op_strict_equiv ),
inference(cnf_transformation,[status(thm)],[f308]) ).
fof(f311,plain,
op_or,
inference(cnf_transformation,[status(thm)],[f60]) ).
fof(f313,plain,
op_strict_implies,
inference(cnf_transformation,[status(thm)],[f62]) ).
fof(f314,plain,
op_equiv,
inference(cnf_transformation,[status(thm)],[f63]) ).
fof(f315,plain,
op_strict_equiv,
inference(cnf_transformation,[status(thm)],[f64]) ).
fof(f316,plain,
modus_ponens_strict_implies,
inference(cnf_transformation,[status(thm)],[f65]) ).
fof(f317,plain,
substitution_strict_equiv,
inference(cnf_transformation,[status(thm)],[f66]) ).
fof(f318,plain,
adjunction,
inference(cnf_transformation,[status(thm)],[f67]) ).
fof(f319,plain,
axiom_m1,
inference(cnf_transformation,[status(thm)],[f68]) ).
fof(f320,plain,
axiom_m2,
inference(cnf_transformation,[status(thm)],[f69]) ).
fof(f321,plain,
axiom_m3,
inference(cnf_transformation,[status(thm)],[f70]) ).
fof(f322,plain,
axiom_m4,
inference(cnf_transformation,[status(thm)],[f71]) ).
fof(f323,plain,
axiom_m5,
inference(cnf_transformation,[status(thm)],[f72]) ).
fof(f325,plain,
op_implies_and,
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f327,plain,
substitution_of_equivalents,
inference(cnf_transformation,[status(thm)],[f76]) ).
fof(f328,plain,
~ modus_tollens,
inference(cnf_transformation,[status(thm)],[f78]) ).
fof(f348,definition,
( sQ5_spl
<=> substitution_of_equivalents ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f350,plain,
( sQ5_spl
| ~ substitution_of_equivalents ),
inference(component_clause,[status(thm)],[f348]) ).
fof(f351,definition,
! [X0,X1] :
( sQ6_spl
<=> ( X0 = X1
| ~ is_a_theorem(equiv(X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f352,plain,
! [X0,X1] :
( ~ sQ6_spl
| X0 = X1
| ~ is_a_theorem(equiv(X0,X1)) ),
inference(component_clause,[status(thm)],[f351]) ).
fof(f354,plain,
( sQ6_spl
| ~ sQ5_spl ),
inference(split_clause,[status(thm)],[f90,f348,f351]) ).
fof(f363,definition,
( sQ9_spl
<=> modus_tollens ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f364,plain,
( ~ sQ9_spl
| modus_tollens ),
inference(component_clause,[status(thm)],[f363]) ).
fof(f370,definition,
( sQ11_spl
<=> is_a_theorem(implies(implies(not(sK5_skl),not(sK4_skl)),implies(sK4_skl,sK5_skl))) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f372,plain,
( sQ11_spl
| ~ is_a_theorem(implies(implies(not(sK5_skl),not(sK4_skl)),implies(sK4_skl,sK5_skl))) ),
inference(component_clause,[status(thm)],[f370]) ).
fof(f373,plain,
( ~ sQ11_spl
| sQ9_spl ),
inference(split_clause,[status(thm)],[f96,f363,f370]) ).
fof(f618,definition,
( sQ78_spl
<=> op_or ),
introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition]) ).
fof(f620,plain,
( sQ78_spl
| ~ op_or ),
inference(component_clause,[status(thm)],[f618]) ).
fof(f621,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(f622,plain,
! [X0,X1] :
( ~ sQ79_spl
| or(X0,X1) = not(and(not(X0),not(X1))) ),
inference(component_clause,[status(thm)],[f621]) ).
fof(f624,plain,
( sQ79_spl
| ~ sQ78_spl ),
inference(split_clause,[status(thm)],[f190,f618,f621]) ).
fof(f632,definition,
( sQ82_spl
<=> op_implies_and ),
introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition]) ).
fof(f634,plain,
( sQ82_spl
| ~ op_implies_and ),
inference(component_clause,[status(thm)],[f632]) ).
fof(f635,definition,
! [X0,X1] :
( sQ83_spl
<=> implies(X0,X1) = not(and(X0,not(X1))) ),
introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition]) ).
fof(f636,plain,
! [X0,X1] :
( ~ sQ83_spl
| implies(X0,X1) = not(and(X0,not(X1))) ),
inference(component_clause,[status(thm)],[f635]) ).
fof(f638,plain,
( sQ83_spl
| ~ sQ82_spl ),
inference(split_clause,[status(thm)],[f194,f632,f635]) ).
fof(f646,definition,
( sQ86_spl
<=> op_equiv ),
introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition]) ).
fof(f648,plain,
( sQ86_spl
| ~ op_equiv ),
inference(component_clause,[status(thm)],[f646]) ).
fof(f649,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(f650,plain,
! [X0,X1] :
( ~ sQ87_spl
| equiv(X0,X1) = and(implies(X0,X1),implies(X1,X0)) ),
inference(component_clause,[status(thm)],[f649]) ).
fof(f652,plain,
( sQ87_spl
| ~ sQ86_spl ),
inference(split_clause,[status(thm)],[f198,f646,f649]) ).
fof(f668,definition,
( sQ92_spl
<=> modus_ponens_strict_implies ),
introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition]) ).
fof(f670,plain,
( sQ92_spl
| ~ modus_ponens_strict_implies ),
inference(component_clause,[status(thm)],[f668]) ).
fof(f671,definition,
! [X0,X1] :
( sQ93_spl
<=> ( is_a_theorem(X1)
| ~ is_a_theorem(strict_implies(X0,X1))
| ~ is_a_theorem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition]) ).
fof(f672,plain,
! [X0,X1] :
( ~ sQ93_spl
| is_a_theorem(X1)
| ~ is_a_theorem(strict_implies(X0,X1))
| ~ is_a_theorem(X0) ),
inference(component_clause,[status(thm)],[f671]) ).
fof(f674,plain,
( sQ93_spl
| ~ sQ92_spl ),
inference(split_clause,[status(thm)],[f209,f668,f671]) ).
fof(f687,definition,
( sQ97_spl
<=> adjunction ),
introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition]) ).
fof(f689,plain,
( sQ97_spl
| ~ adjunction ),
inference(component_clause,[status(thm)],[f687]) ).
fof(f690,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(f691,plain,
! [X0,X1] :
( ~ sQ98_spl
| is_a_theorem(and(X0,X1))
| ~ is_a_theorem(X1)
| ~ is_a_theorem(X0) ),
inference(component_clause,[status(thm)],[f690]) ).
fof(f693,plain,
( sQ98_spl
| ~ sQ97_spl ),
inference(split_clause,[status(thm)],[f216,f687,f690]) ).
fof(f706,definition,
( sQ102_spl
<=> substitution_strict_equiv ),
introduced(definition,[new_symbols(definition,[sQ102_spl])],[split_symbol_definition]) ).
fof(f708,plain,
( sQ102_spl
| ~ substitution_strict_equiv ),
inference(component_clause,[status(thm)],[f706]) ).
fof(f709,definition,
! [X0,X1] :
( sQ103_spl
<=> ( X0 = X1
| ~ is_a_theorem(strict_equiv(X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition]) ).
fof(f710,plain,
! [X0,X1] :
( ~ sQ103_spl
| X0 = X1
| ~ is_a_theorem(strict_equiv(X0,X1)) ),
inference(component_clause,[status(thm)],[f709]) ).
fof(f712,plain,
( sQ103_spl
| ~ sQ102_spl ),
inference(split_clause,[status(thm)],[f223,f706,f709]) ).
fof(f820,definition,
( sQ133_spl
<=> axiom_m1 ),
introduced(definition,[new_symbols(definition,[sQ133_spl])],[split_symbol_definition]) ).
fof(f822,plain,
( sQ133_spl
| ~ axiom_m1 ),
inference(component_clause,[status(thm)],[f820]) ).
fof(f823,definition,
! [X0,X1] :
( sQ134_spl
<=> is_a_theorem(strict_implies(and(X0,X1),and(X1,X0))) ),
introduced(definition,[new_symbols(definition,[sQ134_spl])],[split_symbol_definition]) ).
fof(f824,plain,
! [X0,X1] :
( ~ sQ134_spl
| is_a_theorem(strict_implies(and(X0,X1),and(X1,X0))) ),
inference(component_clause,[status(thm)],[f823]) ).
fof(f826,plain,
( sQ134_spl
| ~ sQ133_spl ),
inference(split_clause,[status(thm)],[f264,f820,f823]) ).
fof(f831,definition,
( sQ136_spl
<=> axiom_m2 ),
introduced(definition,[new_symbols(definition,[sQ136_spl])],[split_symbol_definition]) ).
fof(f833,plain,
( sQ136_spl
| ~ axiom_m2 ),
inference(component_clause,[status(thm)],[f831]) ).
fof(f834,definition,
! [X0,X1] :
( sQ137_spl
<=> is_a_theorem(strict_implies(and(X0,X1),X0)) ),
introduced(definition,[new_symbols(definition,[sQ137_spl])],[split_symbol_definition]) ).
fof(f835,plain,
! [X0,X1] :
( ~ sQ137_spl
| is_a_theorem(strict_implies(and(X0,X1),X0)) ),
inference(component_clause,[status(thm)],[f834]) ).
fof(f837,plain,
( sQ137_spl
| ~ sQ136_spl ),
inference(split_clause,[status(thm)],[f268,f831,f834]) ).
fof(f842,definition,
( sQ139_spl
<=> axiom_m3 ),
introduced(definition,[new_symbols(definition,[sQ139_spl])],[split_symbol_definition]) ).
fof(f844,plain,
( sQ139_spl
| ~ axiom_m3 ),
inference(component_clause,[status(thm)],[f842]) ).
fof(f845,definition,
! [X0,X1,X2] :
( sQ140_spl
<=> is_a_theorem(strict_implies(and(and(X0,X1),X2),and(X0,and(X1,X2)))) ),
introduced(definition,[new_symbols(definition,[sQ140_spl])],[split_symbol_definition]) ).
fof(f846,plain,
! [X0,X1,X2] :
( ~ sQ140_spl
| is_a_theorem(strict_implies(and(and(X0,X1),X2),and(X0,and(X1,X2)))) ),
inference(component_clause,[status(thm)],[f845]) ).
fof(f848,plain,
( sQ140_spl
| ~ sQ139_spl ),
inference(split_clause,[status(thm)],[f272,f842,f845]) ).
fof(f853,definition,
( sQ142_spl
<=> axiom_m4 ),
introduced(definition,[new_symbols(definition,[sQ142_spl])],[split_symbol_definition]) ).
fof(f855,plain,
( sQ142_spl
| ~ axiom_m4 ),
inference(component_clause,[status(thm)],[f853]) ).
fof(f856,definition,
! [X0] :
( sQ143_spl
<=> is_a_theorem(strict_implies(X0,and(X0,X0))) ),
introduced(definition,[new_symbols(definition,[sQ143_spl])],[split_symbol_definition]) ).
fof(f857,plain,
! [X0] :
( ~ sQ143_spl
| is_a_theorem(strict_implies(X0,and(X0,X0))) ),
inference(component_clause,[status(thm)],[f856]) ).
fof(f859,plain,
( sQ143_spl
| ~ sQ142_spl ),
inference(split_clause,[status(thm)],[f276,f853,f856]) ).
fof(f864,definition,
( sQ145_spl
<=> axiom_m5 ),
introduced(definition,[new_symbols(definition,[sQ145_spl])],[split_symbol_definition]) ).
fof(f866,plain,
( sQ145_spl
| ~ axiom_m5 ),
inference(component_clause,[status(thm)],[f864]) ).
fof(f867,definition,
! [X0,X1,X2] :
( sQ146_spl
<=> is_a_theorem(strict_implies(and(strict_implies(X0,X1),strict_implies(X1,X2)),strict_implies(X0,X2))) ),
introduced(definition,[new_symbols(definition,[sQ146_spl])],[split_symbol_definition]) ).
fof(f868,plain,
! [X0,X1,X2] :
( ~ sQ146_spl
| is_a_theorem(strict_implies(and(strict_implies(X0,X1),strict_implies(X1,X2)),strict_implies(X0,X2))) ),
inference(component_clause,[status(thm)],[f867]) ).
fof(f870,plain,
( sQ146_spl
| ~ sQ145_spl ),
inference(split_clause,[status(thm)],[f280,f864,f867]) ).
fof(f944,definition,
( sQ167_spl
<=> op_strict_implies ),
introduced(definition,[new_symbols(definition,[sQ167_spl])],[split_symbol_definition]) ).
fof(f946,plain,
( sQ167_spl
| ~ op_strict_implies ),
inference(component_clause,[status(thm)],[f944]) ).
fof(f947,definition,
! [X0,X1] :
( sQ168_spl
<=> strict_implies(X0,X1) = necessarily(implies(X0,X1)) ),
introduced(definition,[new_symbols(definition,[sQ168_spl])],[split_symbol_definition]) ).
fof(f948,plain,
! [X0,X1] :
( ~ sQ168_spl
| strict_implies(X0,X1) = necessarily(implies(X0,X1)) ),
inference(component_clause,[status(thm)],[f947]) ).
fof(f950,plain,
( sQ168_spl
| ~ sQ167_spl ),
inference(split_clause,[status(thm)],[f307,f944,f947]) ).
fof(f951,definition,
( sQ169_spl
<=> op_strict_equiv ),
introduced(definition,[new_symbols(definition,[sQ169_spl])],[split_symbol_definition]) ).
fof(f953,plain,
( sQ169_spl
| ~ op_strict_equiv ),
inference(component_clause,[status(thm)],[f951]) ).
fof(f954,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(f955,plain,
! [X0,X1] :
( ~ sQ170_spl
| strict_equiv(X0,X1) = and(strict_implies(X0,X1),strict_implies(X1,X0)) ),
inference(component_clause,[status(thm)],[f954]) ).
fof(f957,plain,
( sQ170_spl
| ~ sQ169_spl ),
inference(split_clause,[status(thm)],[f309,f951,f954]) ).
fof(f958,plain,
( sQ169_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f953,f315]) ).
fof(f959,plain,
sQ169_spl,
inference(contradiction_clause,[status(thm)],[f958]) ).
fof(f960,plain,
( sQ97_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f689,f318]) ).
fof(f961,plain,
sQ97_spl,
inference(contradiction_clause,[status(thm)],[f960]) ).
fof(f962,plain,
( sQ92_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f670,f316]) ).
fof(f963,plain,
sQ92_spl,
inference(contradiction_clause,[status(thm)],[f962]) ).
fof(f964,plain,
( sQ102_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f708,f317]) ).
fof(f965,plain,
sQ102_spl,
inference(contradiction_clause,[status(thm)],[f964]) ).
fof(f966,plain,
( sQ5_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f350,f327]) ).
fof(f967,plain,
sQ5_spl,
inference(contradiction_clause,[status(thm)],[f966]) ).
fof(f968,plain,
( sQ167_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f946,f313]) ).
fof(f969,plain,
sQ167_spl,
inference(contradiction_clause,[status(thm)],[f968]) ).
fof(f972,plain,
( sQ86_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f648,f314]) ).
fof(f973,plain,
sQ86_spl,
inference(contradiction_clause,[status(thm)],[f972]) ).
fof(f974,plain,
( sQ82_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f634,f325]) ).
fof(f975,plain,
sQ82_spl,
inference(contradiction_clause,[status(thm)],[f974]) ).
fof(f976,plain,
( sQ78_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f620,f311]) ).
fof(f977,plain,
sQ78_spl,
inference(contradiction_clause,[status(thm)],[f976]) ).
fof(f993,plain,
( sQ142_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f855,f322]) ).
fof(f994,plain,
sQ142_spl,
inference(contradiction_clause,[status(thm)],[f993]) ).
fof(f1027,plain,
( sQ136_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f833,f320]) ).
fof(f1028,plain,
sQ136_spl,
inference(contradiction_clause,[status(thm)],[f1027]) ).
fof(f1043,plain,
( sQ145_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f866,f323]) ).
fof(f1044,plain,
sQ145_spl,
inference(contradiction_clause,[status(thm)],[f1043]) ).
fof(f1077,plain,
( sQ139_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f844,f321]) ).
fof(f1078,plain,
sQ139_spl,
inference(contradiction_clause,[status(thm)],[f1077]) ).
fof(f1081,plain,
( sQ133_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f822,f319]) ).
fof(f1082,plain,
sQ133_spl,
inference(contradiction_clause,[status(thm)],[f1081]) ).
fof(f1119,definition,
! [X1] :
( sQ172_spl
<=> ~ is_a_theorem(X1) ),
introduced(definition,[new_symbols(definition,[sQ172_spl])],[split_symbol_definition]) ).
fof(f1120,plain,
! [X0] :
( ~ sQ172_spl
| ~ is_a_theorem(X0) ),
inference(component_clause,[status(thm)],[f1119]) ).
fof(f1147,plain,
! [X0,X1,X2] :
( ~ sQ83_spl
| implies(X0,and(X1,not(X2))) = not(and(X0,implies(X1,X2))) ),
inference(paramodulation,[status(thm)],[f636,f636]) ).
fof(f1315,plain,
! [X0,X1] :
( ~ sQ93_spl
| ~ sQ134_spl
| is_a_theorem(and(X1,X0))
| ~ is_a_theorem(and(X0,X1)) ),
inference(resolution,[status(thm)],[f824,f672]) ).
fof(f1412,plain,
! [X0,X1] :
( ~ sQ170_spl
| ~ sQ98_spl
| is_a_theorem(strict_equiv(X0,X1))
| ~ is_a_theorem(strict_implies(X1,X0))
| ~ is_a_theorem(strict_implies(X0,X1)) ),
inference(paramodulation,[status(thm)],[f955,f691]) ).
fof(f1414,plain,
! [X0,X1] :
( ~ sQ170_spl
| ~ sQ137_spl
| is_a_theorem(strict_implies(strict_equiv(X0,X1),strict_implies(X0,X1))) ),
inference(paramodulation,[status(thm)],[f955,f835]) ).
fof(f1517,plain,
! [X0] :
( ~ sQ87_spl
| ~ sQ143_spl
| is_a_theorem(strict_implies(implies(X0,X0),equiv(X0,X0))) ),
inference(paramodulation,[status(thm)],[f650,f857]) ).
fof(f1633,plain,
! [X0,X1] :
( ~ sQ79_spl
| ~ sQ83_spl
| or(X0,X1) = implies(not(X0),X1) ),
inference(forward_demodulation,[status(thm)],[f636,f622]) ).
fof(f1679,plain,
! [X0,X1] :
( ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ87_spl
| equiv(not(X0),X1) = and(or(X0,X1),implies(X1,not(X0))) ),
inference(paramodulation,[status(thm)],[f1633,f650]) ).
fof(f1695,plain,
! [X0,X1] :
( ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ168_spl
| strict_implies(not(X0),X1) = necessarily(or(X0,X1)) ),
inference(paramodulation,[status(thm)],[f1633,f948]) ).
fof(f1712,plain,
! [X0,X1] :
( ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ168_spl
| ~ sQ170_spl
| ~ sQ137_spl
| is_a_theorem(strict_implies(strict_equiv(not(X0),X1),necessarily(or(X0,X1)))) ),
inference(paramodulation,[status(thm)],[f1695,f1414]) ).
fof(f1717,plain,
! [X0,X1] :
( ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ168_spl
| ~ sQ170_spl
| strict_equiv(not(X0),X1) = and(necessarily(or(X0,X1)),strict_implies(X1,not(X0))) ),
inference(paramodulation,[status(thm)],[f1695,f955]) ).
fof(f2456,plain,
! [X0,X1] :
( ~ sQ93_spl
| ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ168_spl
| ~ sQ170_spl
| ~ sQ137_spl
| is_a_theorem(necessarily(or(X0,X1)))
| ~ is_a_theorem(strict_equiv(not(X0),X1)) ),
inference(resolution,[status(thm)],[f1712,f672]) ).
fof(f2481,plain,
! [X0,X1,X2] :
( ~ sQ93_spl
| ~ sQ146_spl
| is_a_theorem(strict_implies(X0,X2))
| ~ is_a_theorem(and(strict_implies(X0,X1),strict_implies(X1,X2))) ),
inference(resolution,[status(thm)],[f868,f672]) ).
fof(f2492,plain,
( sQ11_spl
| ~ sQ79_spl
| ~ sQ83_spl
| ~ is_a_theorem(implies(or(sK5_skl,not(sK4_skl)),implies(sK4_skl,sK5_skl))) ),
inference(forward_demodulation,[status(thm)],[f1633,f372]) ).
fof(f2501,plain,
! [X0,X1,X2] :
( ~ sQ93_spl
| ~ sQ140_spl
| is_a_theorem(and(X0,and(X1,X2)))
| ~ is_a_theorem(and(and(X0,X1),X2)) ),
inference(resolution,[status(thm)],[f846,f672]) ).
fof(f2502,plain,
! [X0,X1,X2] :
( ~ sQ87_spl
| ~ sQ140_spl
| is_a_theorem(strict_implies(and(equiv(X0,X1),X2),and(implies(X0,X1),and(implies(X1,X0),X2)))) ),
inference(paramodulation,[status(thm)],[f650,f846]) ).
fof(f2510,plain,
! [X0,X1] :
( ~ sQ83_spl
| ~ sQ87_spl
| ~ sQ143_spl
| is_a_theorem(strict_implies(not(and(and(X0,not(X1)),implies(X0,X1))),equiv(and(X0,not(X1)),and(X0,not(X1))))) ),
inference(paramodulation,[status(thm)],[f1147,f1517]) ).
fof(f2518,plain,
! [X0,X1] :
( ~ sQ83_spl
| ~ sQ87_spl
| ~ sQ143_spl
| ~ sQ79_spl
| ~ sQ168_spl
| is_a_theorem(necessarily(or(and(and(X0,not(X1)),implies(X0,X1)),equiv(and(X0,not(X1)),and(X0,not(X1)))))) ),
inference(forward_demodulation,[status(thm)],[f1695,f2510]) ).
fof(f2530,plain,
! [X0,X1] :
( ~ sQ134_spl
| ~ sQ170_spl
| ~ sQ98_spl
| is_a_theorem(strict_equiv(and(X0,X1),and(X1,X0)))
| ~ is_a_theorem(strict_implies(and(X0,X1),and(X1,X0))) ),
inference(resolution,[status(thm)],[f1412,f824]) ).
fof(f2532,plain,
! [X0] :
( ~ sQ143_spl
| ~ sQ170_spl
| ~ sQ98_spl
| is_a_theorem(strict_equiv(and(X0,X0),X0))
| ~ is_a_theorem(strict_implies(and(X0,X0),X0)) ),
inference(resolution,[status(thm)],[f1412,f857]) ).
fof(f2539,plain,
! [X0,X1] :
( ~ sQ134_spl
| ~ sQ170_spl
| ~ sQ98_spl
| is_a_theorem(strict_equiv(and(X0,X1),and(X1,X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f2530,f824]) ).
fof(f2540,plain,
! [X0] :
( ~ sQ143_spl
| ~ sQ170_spl
| ~ sQ98_spl
| ~ sQ137_spl
| is_a_theorem(strict_equiv(and(X0,X0),X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f2532,f835]) ).
fof(f2545,plain,
! [X0] :
( ~ sQ103_spl
| ~ sQ143_spl
| ~ sQ170_spl
| ~ sQ98_spl
| ~ sQ137_spl
| and(X0,X0) = X0 ),
inference(resolution,[status(thm)],[f2540,f710]) ).
fof(f2550,plain,
! [X0] :
( ~ sQ143_spl
| ~ sQ170_spl
| ~ sQ98_spl
| ~ sQ137_spl
| ~ sQ103_spl
| is_a_theorem(strict_equiv(X0,X0)) ),
inference(backward_demodulation,[status(thm)],[f2545,f2540]) ).
fof(f2554,plain,
! [X0] :
( ~ sQ87_spl
| ~ sQ103_spl
| ~ sQ143_spl
| ~ sQ170_spl
| ~ sQ98_spl
| ~ sQ137_spl
| equiv(X0,X0) = implies(X0,X0) ),
inference(paramodulation,[status(thm)],[f650,f2545]) ).
fof(f2555,plain,
! [X0] :
( ~ sQ170_spl
| ~ sQ103_spl
| ~ sQ143_spl
| ~ sQ98_spl
| ~ sQ137_spl
| strict_equiv(X0,X0) = strict_implies(X0,X0) ),
inference(paramodulation,[status(thm)],[f955,f2545]) ).
fof(f2564,plain,
! [X0] :
( ~ sQ103_spl
| ~ sQ143_spl
| ~ sQ170_spl
| ~ sQ98_spl
| ~ sQ137_spl
| ~ sQ83_spl
| implies(not(X0),X0) = not(not(X0)) ),
inference(paramodulation,[status(thm)],[f2545,f636]) ).
fof(f2566,plain,
! [X0,X1] :
( ~ sQ103_spl
| ~ sQ143_spl
| ~ sQ170_spl
| ~ sQ98_spl
| ~ sQ137_spl
| ~ sQ140_spl
| is_a_theorem(strict_implies(and(X0,X1),and(X0,and(X0,X1)))) ),
inference(paramodulation,[status(thm)],[f2545,f846]) ).
fof(f2578,plain,
! [X0] :
( ~ sQ103_spl
| ~ sQ143_spl
| ~ sQ170_spl
| ~ sQ98_spl
| ~ sQ137_spl
| ~ sQ83_spl
| ~ sQ79_spl
| or(X0,X0) = not(not(X0)) ),
inference(forward_demodulation,[status(thm)],[f1633,f2564]) ).
fof(f2600,plain,
! [X0] :
( ~ sQ87_spl
| ~ sQ103_spl
| ~ sQ143_spl
| ~ sQ170_spl
| ~ sQ98_spl
| ~ sQ137_spl
| ~ sQ168_spl
| strict_implies(X0,X0) = necessarily(equiv(X0,X0)) ),
inference(paramodulation,[status(thm)],[f2554,f948]) ).
fof(f2662,plain,
! [X0] :
( ~ sQ87_spl
| ~ sQ103_spl
| ~ sQ143_spl
| ~ sQ170_spl
| ~ sQ98_spl
| ~ sQ137_spl
| ~ sQ168_spl
| strict_equiv(X0,X0) = necessarily(equiv(X0,X0)) ),
inference(forward_demodulation,[status(thm)],[f2555,f2600]) ).
fof(f2739,plain,
! [X0,X1] :
( ~ sQ103_spl
| ~ sQ134_spl
| ~ sQ170_spl
| ~ sQ98_spl
| and(X0,X1) = and(X1,X0) ),
inference(resolution,[status(thm)],[f2539,f710]) ).
fof(f2773,plain,
! [X0,X1] :
( ~ sQ103_spl
| ~ sQ134_spl
| ~ sQ170_spl
| ~ sQ98_spl
| ~ sQ83_spl
| implies(X0,X1) = not(and(not(X1),X0)) ),
inference(paramodulation,[status(thm)],[f2739,f636]) ).
fof(f2784,plain,
! [X0,X1] :
( ~ sQ103_spl
| ~ sQ134_spl
| ~ sQ170_spl
| ~ sQ98_spl
| ~ sQ137_spl
| is_a_theorem(strict_implies(and(X0,X1),X1)) ),
inference(paramodulation,[status(thm)],[f2739,f835]) ).
fof(f2854,plain,
! [X0,X1] :
( ~ sQ83_spl
| ~ sQ103_spl
| ~ sQ134_spl
| ~ sQ170_spl
| ~ sQ98_spl
| implies(not(X0),X1) = implies(not(X1),X0) ),
inference(paramodulation,[status(thm)],[f636,f2773]) ).
fof(f2877,plain,
! [X0,X1] :
( ~ sQ83_spl
| ~ sQ103_spl
| ~ sQ134_spl
| ~ sQ170_spl
| ~ sQ98_spl
| ~ sQ79_spl
| or(X0,X1) = implies(not(X1),X0) ),
inference(forward_demodulation,[status(thm)],[f1633,f2854]) ).
fof(f2878,plain,
! [X0,X1] :
( ~ sQ83_spl
| ~ sQ103_spl
| ~ sQ134_spl
| ~ sQ170_spl
| ~ sQ98_spl
| ~ sQ79_spl
| or(X0,X1) = or(X1,X0) ),
inference(forward_demodulation,[status(thm)],[f1633,f2877]) ).
fof(f2903,plain,
! [X0,X1] :
( ~ sQ83_spl
| ~ sQ103_spl
| ~ sQ134_spl
| ~ sQ170_spl
| ~ sQ98_spl
| ~ sQ79_spl
| ~ sQ93_spl
| ~ sQ168_spl
| ~ sQ137_spl
| is_a_theorem(necessarily(or(X1,X0)))
| ~ is_a_theorem(strict_equiv(not(X0),X1)) ),
inference(paramodulation,[status(thm)],[f2878,f2456]) ).
fof(f3164,plain,
! [X0,X1] :
( ~ sQ170_spl
| ~ sQ98_spl
| ~ sQ103_spl
| ~ sQ143_spl
| ~ sQ137_spl
| ~ sQ140_spl
| is_a_theorem(strict_equiv(and(X0,and(X0,X1)),and(X0,X1)))
| ~ is_a_theorem(strict_implies(and(X0,and(X0,X1)),and(X0,X1))) ),
inference(resolution,[status(thm)],[f2566,f1412]) ).
fof(f3178,plain,
! [X0,X1] :
( ~ sQ170_spl
| ~ sQ98_spl
| ~ sQ103_spl
| ~ sQ143_spl
| ~ sQ137_spl
| ~ sQ140_spl
| ~ sQ134_spl
| is_a_theorem(strict_equiv(and(X0,and(X0,X1)),and(X0,X1))) ),
inference(forward_subsumption_resolution,[status(thm)],[f3164,f2784]) ).
fof(f3266,plain,
! [X0,X1,X2] :
( ~ sQ93_spl
| ~ sQ134_spl
| ~ sQ146_spl
| ~ is_a_theorem(and(strict_implies(X2,X1),strict_implies(X0,X2)))
| is_a_theorem(strict_implies(X0,X1)) ),
inference(resolution,[status(thm)],[f2481,f1315]) ).
fof(f3274,plain,
! [X0,X1,X2] :
( ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ168_spl
| ~ sQ93_spl
| ~ sQ146_spl
| is_a_theorem(strict_implies(X0,X2))
| ~ is_a_theorem(and(strict_implies(X0,not(X1)),necessarily(or(X1,X2)))) ),
inference(paramodulation,[status(thm)],[f1695,f2481]) ).
fof(f3281,plain,
! [X0,X1] :
( ~ sQ103_spl
| ~ sQ170_spl
| ~ sQ98_spl
| ~ sQ143_spl
| ~ sQ137_spl
| ~ sQ140_spl
| ~ sQ134_spl
| and(X0,and(X0,X1)) = and(X0,X1) ),
inference(resolution,[status(thm)],[f3178,f710]) ).
fof(f3317,plain,
! [X0,X1] :
( ~ sQ103_spl
| ~ sQ134_spl
| ~ sQ170_spl
| ~ sQ98_spl
| ~ sQ143_spl
| ~ sQ137_spl
| ~ sQ140_spl
| and(X0,and(X1,X0)) = and(X0,X1) ),
inference(paramodulation,[status(thm)],[f2739,f3281]) ).
fof(f3321,plain,
! [X0,X1] :
( ~ sQ103_spl
| ~ sQ170_spl
| ~ sQ98_spl
| ~ sQ143_spl
| ~ sQ137_spl
| ~ sQ140_spl
| ~ sQ134_spl
| ~ sQ83_spl
| implies(and(not(X0),X1),X0) = not(and(not(X0),X1)) ),
inference(paramodulation,[status(thm)],[f3281,f2773]) ).
fof(f3342,plain,
! [X0,X1] :
( ~ sQ103_spl
| ~ sQ170_spl
| ~ sQ98_spl
| ~ sQ143_spl
| ~ sQ137_spl
| ~ sQ140_spl
| ~ sQ134_spl
| ~ sQ83_spl
| implies(and(not(X0),X1),X0) = implies(X1,X0) ),
inference(forward_demodulation,[status(thm)],[f2773,f3321]) ).
fof(f3357,plain,
! [X0,X1] :
( ~ sQ103_spl
| ~ sQ134_spl
| ~ sQ170_spl
| ~ sQ98_spl
| ~ sQ143_spl
| ~ sQ137_spl
| ~ sQ140_spl
| ~ sQ83_spl
| implies(and(X0,not(X1)),X1) = not(and(not(X1),X0)) ),
inference(paramodulation,[status(thm)],[f3317,f2773]) ).
fof(f3380,plain,
! [X0,X1] :
( ~ sQ103_spl
| ~ sQ134_spl
| ~ sQ170_spl
| ~ sQ98_spl
| ~ sQ143_spl
| ~ sQ137_spl
| ~ sQ140_spl
| ~ sQ83_spl
| implies(and(X0,not(X1)),X1) = implies(X0,X1) ),
inference(forward_demodulation,[status(thm)],[f2773,f3357]) ).
fof(f3512,plain,
! [X0,X1] :
( ~ sQ103_spl
| ~ sQ170_spl
| ~ sQ98_spl
| ~ sQ143_spl
| ~ sQ137_spl
| ~ sQ140_spl
| ~ sQ134_spl
| ~ sQ83_spl
| ~ sQ168_spl
| strict_implies(and(not(X0),X1),X0) = necessarily(implies(X1,X0)) ),
inference(paramodulation,[status(thm)],[f3342,f948]) ).
fof(f3532,plain,
! [X0,X1] :
( ~ sQ103_spl
| ~ sQ170_spl
| ~ sQ98_spl
| ~ sQ143_spl
| ~ sQ137_spl
| ~ sQ140_spl
| ~ sQ134_spl
| ~ sQ83_spl
| ~ sQ168_spl
| strict_implies(and(not(X0),X1),X0) = strict_implies(X1,X0) ),
inference(forward_demodulation,[status(thm)],[f948,f3512]) ).
fof(f3554,plain,
! [X0,X1] :
( ~ sQ103_spl
| ~ sQ134_spl
| ~ sQ170_spl
| ~ sQ98_spl
| ~ sQ143_spl
| ~ sQ137_spl
| ~ sQ140_spl
| ~ sQ83_spl
| ~ sQ168_spl
| strict_implies(and(X0,not(X1)),X1) = necessarily(implies(X0,X1)) ),
inference(paramodulation,[status(thm)],[f3380,f948]) ).
fof(f3577,plain,
! [X0,X1] :
( ~ sQ103_spl
| ~ sQ134_spl
| ~ sQ170_spl
| ~ sQ98_spl
| ~ sQ143_spl
| ~ sQ137_spl
| ~ sQ140_spl
| ~ sQ83_spl
| ~ sQ168_spl
| strict_implies(and(X0,not(X1)),X1) = strict_implies(X0,X1) ),
inference(forward_demodulation,[status(thm)],[f948,f3554]) ).
fof(f3611,plain,
! [X0,X1,X2] :
( ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ87_spl
| ~ sQ93_spl
| ~ sQ140_spl
| is_a_theorem(and(or(X0,X1),and(implies(X1,not(X0)),X2)))
| ~ is_a_theorem(and(equiv(not(X0),X1),X2)) ),
inference(paramodulation,[status(thm)],[f1679,f2501]) ).
fof(f4463,plain,
! [X0,X1] :
( ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ168_spl
| ~ sQ170_spl
| ~ sQ98_spl
| is_a_theorem(strict_equiv(not(X0),X1))
| ~ is_a_theorem(strict_implies(X1,not(X0)))
| ~ is_a_theorem(necessarily(or(X0,X1))) ),
inference(paramodulation,[status(thm)],[f1717,f691]) ).
fof(f11261,plain,
( ~ sQ83_spl
| ~ sQ87_spl
| ~ sQ143_spl
| ~ sQ79_spl
| ~ sQ168_spl
| ~ sQ172_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f2518,f1120]) ).
fof(f11330,plain,
( ~ sQ83_spl
| ~ sQ87_spl
| ~ sQ143_spl
| ~ sQ79_spl
| ~ sQ168_spl
| ~ sQ172_spl ),
inference(contradiction_clause,[status(thm)],[f11261]) ).
fof(f11442,plain,
! [X0,X1,X2] :
( ~ sQ98_spl
| ~ sQ137_spl
| is_a_theorem(and(X0,strict_implies(and(X1,X2),X1)))
| ~ is_a_theorem(X0) ),
inference(resolution,[status(thm)],[f835,f691]) ).
fof(f12126,plain,
! [X0,X1,X2,X3] :
( ~ sQ98_spl
| ~ sQ140_spl
| is_a_theorem(and(X0,strict_implies(and(and(X1,X2),X3),and(X1,and(X2,X3)))))
| ~ is_a_theorem(X0) ),
inference(resolution,[status(thm)],[f846,f691]) ).
fof(f14738,plain,
! [X0] :
( ~ sQ143_spl
| ~ sQ170_spl
| ~ sQ98_spl
| ~ sQ137_spl
| ~ sQ103_spl
| ~ sQ83_spl
| ~ sQ134_spl
| ~ sQ79_spl
| ~ sQ93_spl
| ~ sQ168_spl
| is_a_theorem(necessarily(or(not(X0),X0))) ),
inference(resolution,[status(thm)],[f2903,f2550]) ).
fof(f14766,plain,
! [X0,X1] :
( ~ sQ98_spl
| ~ sQ143_spl
| ~ sQ170_spl
| ~ sQ137_spl
| ~ sQ103_spl
| ~ sQ83_spl
| ~ sQ134_spl
| ~ sQ79_spl
| ~ sQ93_spl
| ~ sQ168_spl
| is_a_theorem(and(X0,necessarily(or(not(X1),X1))))
| ~ is_a_theorem(X0) ),
inference(resolution,[status(thm)],[f14738,f691]) ).
fof(f21648,plain,
! [X0,X1] :
( ~ sQ98_spl
| ~ sQ143_spl
| ~ sQ170_spl
| ~ sQ137_spl
| ~ sQ103_spl
| ~ sQ83_spl
| ~ sQ134_spl
| ~ sQ79_spl
| ~ sQ93_spl
| ~ sQ168_spl
| ~ sQ146_spl
| ~ is_a_theorem(strict_implies(X0,not(not(X1))))
| is_a_theorem(strict_implies(X0,X1)) ),
inference(resolution,[status(thm)],[f3274,f14766]) ).
fof(f25217,plain,
! [X0,X1] :
( ~ sQ137_spl
| ~ sQ98_spl
| ~ sQ143_spl
| ~ sQ170_spl
| ~ sQ103_spl
| ~ sQ83_spl
| ~ sQ134_spl
| ~ sQ79_spl
| ~ sQ93_spl
| ~ sQ168_spl
| ~ sQ146_spl
| is_a_theorem(strict_implies(and(not(not(X0)),X1),X0)) ),
inference(resolution,[status(thm)],[f21648,f835]) ).
fof(f38760,plain,
! [X0,X1,X2] :
( ~ sQ93_spl
| ~ sQ98_spl
| is_a_theorem(X2)
| ~ is_a_theorem(strict_implies(and(X0,X1),X2))
| ~ is_a_theorem(X1)
| ~ is_a_theorem(X0) ),
inference(resolution,[status(thm)],[f691,f672]) ).
fof(f39329,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ93_spl
| ~ sQ98_spl
| ~ sQ140_spl
| is_a_theorem(X4)
| ~ is_a_theorem(strict_implies(and(X0,strict_implies(and(and(X1,X2),X3),and(X1,and(X2,X3)))),X4))
| ~ is_a_theorem(X0) ),
inference(resolution,[status(thm)],[f12126,f672]) ).
fof(f39599,plain,
! [X0,X1,X2] :
( ~ sQ93_spl
| ~ sQ146_spl
| ~ sQ98_spl
| ~ sQ137_spl
| is_a_theorem(strict_implies(X0,X1))
| ~ is_a_theorem(strict_implies(X0,and(X1,X2))) ),
inference(resolution,[status(thm)],[f11442,f2481]) ).
fof(f39893,plain,
! [X0,X1,X2] :
( ~ sQ87_spl
| ~ sQ140_spl
| ~ sQ93_spl
| ~ sQ98_spl
| is_a_theorem(and(implies(X0,X1),and(implies(X1,X0),X2)))
| ~ is_a_theorem(X2)
| ~ is_a_theorem(equiv(X0,X1)) ),
inference(resolution,[status(thm)],[f38760,f2502]) ).
fof(f42996,plain,
! [X0,X1,X2] :
( ~ sQ98_spl
| ~ sQ137_spl
| ~ sQ93_spl
| ~ sQ134_spl
| ~ sQ146_spl
| ~ is_a_theorem(strict_implies(X0,X2))
| is_a_theorem(strict_implies(and(X0,X1),X2)) ),
inference(resolution,[status(thm)],[f3266,f11442]) ).
fof(f48872,plain,
! [X0,X1,X2] :
( ~ sQ137_spl
| ~ sQ98_spl
| ~ sQ143_spl
| ~ sQ170_spl
| ~ sQ103_spl
| ~ sQ83_spl
| ~ sQ134_spl
| ~ sQ79_spl
| ~ sQ93_spl
| ~ sQ168_spl
| ~ sQ146_spl
| is_a_theorem(strict_implies(and(not(not(and(X0,X1))),X2),X0)) ),
inference(resolution,[status(thm)],[f39599,f25217]) ).
fof(f51957,plain,
! [X0,X1] :
( ~ sQ103_spl
| ~ sQ170_spl
| ~ sQ98_spl
| ~ sQ143_spl
| ~ sQ137_spl
| ~ sQ140_spl
| ~ sQ134_spl
| ~ sQ83_spl
| ~ sQ168_spl
| ~ sQ93_spl
| ~ sQ146_spl
| ~ is_a_theorem(strict_implies(not(X1),X1))
| is_a_theorem(strict_implies(X0,X1)) ),
inference(paramodulation,[status(thm)],[f3532,f42996]) ).
fof(f51992,plain,
! [X0,X1] :
( ~ sQ103_spl
| ~ sQ170_spl
| ~ sQ98_spl
| ~ sQ143_spl
| ~ sQ137_spl
| ~ sQ140_spl
| ~ sQ134_spl
| ~ sQ83_spl
| ~ sQ168_spl
| ~ sQ93_spl
| ~ sQ146_spl
| ~ sQ79_spl
| ~ is_a_theorem(necessarily(or(X1,X1)))
| is_a_theorem(strict_implies(X0,X1)) ),
inference(forward_demodulation,[status(thm)],[f1695,f51957]) ).
fof(f51993,plain,
! [X0,X1] :
( ~ sQ103_spl
| ~ sQ170_spl
| ~ sQ98_spl
| ~ sQ143_spl
| ~ sQ137_spl
| ~ sQ140_spl
| ~ sQ134_spl
| ~ sQ83_spl
| ~ sQ168_spl
| ~ sQ93_spl
| ~ sQ146_spl
| ~ sQ79_spl
| ~ is_a_theorem(necessarily(not(not(X1))))
| is_a_theorem(strict_implies(X0,X1)) ),
inference(forward_demodulation,[status(thm)],[f2578,f51992]) ).
fof(f56542,plain,
! [X0,X1,X2] :
( ~ sQ98_spl
| ~ sQ143_spl
| ~ sQ170_spl
| ~ sQ137_spl
| ~ sQ103_spl
| ~ sQ83_spl
| ~ sQ134_spl
| ~ sQ79_spl
| ~ sQ93_spl
| ~ sQ168_spl
| ~ sQ146_spl
| is_a_theorem(strict_implies(and(not(not(and(not(not(X0)),X1))),X2),X0)) ),
inference(resolution,[status(thm)],[f48872,f21648]) ).
fof(f56596,plain,
! [X0,X1,X2] :
( ~ sQ98_spl
| ~ sQ143_spl
| ~ sQ170_spl
| ~ sQ137_spl
| ~ sQ103_spl
| ~ sQ83_spl
| ~ sQ134_spl
| ~ sQ79_spl
| ~ sQ93_spl
| ~ sQ168_spl
| ~ sQ146_spl
| is_a_theorem(strict_implies(and(not(implies(X0,not(X1))),X2),X1)) ),
inference(forward_demodulation,[status(thm)],[f2773,f56542]) ).
fof(f62754,plain,
! [X0,X1] :
( ~ sQ103_spl
| ~ sQ134_spl
| ~ sQ170_spl
| ~ sQ98_spl
| ~ sQ143_spl
| ~ sQ137_spl
| ~ sQ140_spl
| ~ sQ83_spl
| ~ sQ168_spl
| ~ sQ79_spl
| ~ sQ93_spl
| ~ sQ146_spl
| is_a_theorem(strict_implies(not(implies(X0,not(X1))),X1)) ),
inference(paramodulation,[status(thm)],[f3577,f56596]) ).
fof(f62785,plain,
! [X0,X1] :
( ~ sQ103_spl
| ~ sQ134_spl
| ~ sQ170_spl
| ~ sQ98_spl
| ~ sQ143_spl
| ~ sQ137_spl
| ~ sQ140_spl
| ~ sQ83_spl
| ~ sQ168_spl
| ~ sQ79_spl
| ~ sQ93_spl
| ~ sQ146_spl
| is_a_theorem(necessarily(or(implies(X0,not(X1)),X1))) ),
inference(forward_demodulation,[status(thm)],[f1695,f62754]) ).
fof(f62816,plain,
! [X0,X1] :
( ~ sQ83_spl
| ~ sQ103_spl
| ~ sQ134_spl
| ~ sQ170_spl
| ~ sQ98_spl
| ~ sQ79_spl
| ~ sQ143_spl
| ~ sQ137_spl
| ~ sQ140_spl
| ~ sQ168_spl
| ~ sQ93_spl
| ~ sQ146_spl
| is_a_theorem(necessarily(or(X0,implies(X1,not(X0))))) ),
inference(paramodulation,[status(thm)],[f2878,f62785]) ).
fof(f63128,plain,
! [X0,X1] :
( ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ103_spl
| ~ sQ134_spl
| ~ sQ170_spl
| ~ sQ98_spl
| ~ sQ143_spl
| ~ sQ137_spl
| ~ sQ140_spl
| ~ sQ168_spl
| ~ sQ93_spl
| ~ sQ146_spl
| is_a_theorem(necessarily(or(X0,or(X1,not(X0))))) ),
inference(paramodulation,[status(thm)],[f1633,f62816]) ).
fof(f63278,plain,
! [X0] :
( ~ sQ103_spl
| ~ sQ143_spl
| ~ sQ170_spl
| ~ sQ98_spl
| ~ sQ137_spl
| ~ sQ83_spl
| ~ sQ79_spl
| ~ sQ134_spl
| ~ sQ140_spl
| ~ sQ168_spl
| ~ sQ93_spl
| ~ sQ146_spl
| is_a_theorem(necessarily(or(X0,not(not(not(X0)))))) ),
inference(paramodulation,[status(thm)],[f2578,f63128]) ).
fof(f63582,plain,
! [X0] :
( ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ168_spl
| ~ sQ170_spl
| ~ sQ98_spl
| ~ sQ103_spl
| ~ sQ143_spl
| ~ sQ137_spl
| ~ sQ134_spl
| ~ sQ140_spl
| ~ sQ93_spl
| ~ sQ146_spl
| is_a_theorem(strict_equiv(not(X0),not(not(not(X0)))))
| ~ is_a_theorem(strict_implies(not(not(not(X0))),not(X0))) ),
inference(resolution,[status(thm)],[f63278,f4463]) ).
fof(f63603,plain,
! [X0] :
( ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ168_spl
| ~ sQ170_spl
| ~ sQ98_spl
| ~ sQ103_spl
| ~ sQ143_spl
| ~ sQ137_spl
| ~ sQ134_spl
| ~ sQ140_spl
| ~ sQ93_spl
| ~ sQ146_spl
| is_a_theorem(strict_equiv(not(X0),not(not(not(X0)))))
| ~ is_a_theorem(necessarily(or(not(not(X0)),not(X0)))) ),
inference(forward_demodulation,[status(thm)],[f1695,f63582]) ).
fof(f63604,plain,
! [X0] :
( ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ168_spl
| ~ sQ170_spl
| ~ sQ98_spl
| ~ sQ103_spl
| ~ sQ143_spl
| ~ sQ137_spl
| ~ sQ134_spl
| ~ sQ140_spl
| ~ sQ93_spl
| ~ sQ146_spl
| is_a_theorem(strict_equiv(not(X0),not(not(not(X0))))) ),
inference(forward_subsumption_resolution,[status(thm)],[f63603,f14738]) ).
fof(f65239,plain,
! [X0] :
( ~ sQ103_spl
| ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ168_spl
| ~ sQ170_spl
| ~ sQ98_spl
| ~ sQ143_spl
| ~ sQ137_spl
| ~ sQ134_spl
| ~ sQ140_spl
| ~ sQ93_spl
| ~ sQ146_spl
| not(X0) = not(not(not(X0))) ),
inference(resolution,[status(thm)],[f63604,f710]) ).
fof(f65309,plain,
! [X0,X1] :
( ~ sQ103_spl
| ~ sQ134_spl
| ~ sQ170_spl
| ~ sQ98_spl
| ~ sQ83_spl
| ~ sQ79_spl
| ~ sQ168_spl
| ~ sQ143_spl
| ~ sQ137_spl
| ~ sQ140_spl
| ~ sQ93_spl
| ~ sQ146_spl
| not(and(not(X0),X1)) = not(not(implies(X1,X0))) ),
inference(paramodulation,[status(thm)],[f2773,f65239]) ).
fof(f65552,plain,
! [X0,X1] :
( ~ sQ103_spl
| ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ168_spl
| ~ sQ170_spl
| ~ sQ98_spl
| ~ sQ143_spl
| ~ sQ137_spl
| ~ sQ134_spl
| ~ sQ140_spl
| ~ sQ93_spl
| ~ sQ146_spl
| implies(X0,not(not(X1))) = not(and(not(X1),X0)) ),
inference(paramodulation,[status(thm)],[f65239,f2773]) ).
fof(f65570,plain,
! [X0,X1] :
( ~ sQ103_spl
| ~ sQ134_spl
| ~ sQ170_spl
| ~ sQ98_spl
| ~ sQ83_spl
| ~ sQ79_spl
| ~ sQ168_spl
| ~ sQ143_spl
| ~ sQ137_spl
| ~ sQ140_spl
| ~ sQ93_spl
| ~ sQ146_spl
| implies(X0,X1) = not(not(implies(X0,X1))) ),
inference(forward_demodulation,[status(thm)],[f2773,f65309]) ).
fof(f65722,plain,
! [X0,X1] :
( ~ sQ103_spl
| ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ168_spl
| ~ sQ170_spl
| ~ sQ98_spl
| ~ sQ143_spl
| ~ sQ137_spl
| ~ sQ134_spl
| ~ sQ140_spl
| ~ sQ93_spl
| ~ sQ146_spl
| implies(X0,not(not(X1))) = implies(X0,X1) ),
inference(forward_demodulation,[status(thm)],[f2773,f65552]) ).
fof(f65835,plain,
! [X0] :
( ~ sQ87_spl
| ~ sQ103_spl
| ~ sQ143_spl
| ~ sQ170_spl
| ~ sQ98_spl
| ~ sQ137_spl
| ~ sQ134_spl
| ~ sQ83_spl
| ~ sQ79_spl
| ~ sQ168_spl
| ~ sQ140_spl
| ~ sQ93_spl
| ~ sQ146_spl
| implies(X0,X0) = not(not(equiv(X0,X0))) ),
inference(paramodulation,[status(thm)],[f2554,f65570]) ).
fof(f66097,plain,
! [X0] :
( ~ sQ87_spl
| ~ sQ103_spl
| ~ sQ143_spl
| ~ sQ170_spl
| ~ sQ98_spl
| ~ sQ137_spl
| ~ sQ134_spl
| ~ sQ83_spl
| ~ sQ79_spl
| ~ sQ168_spl
| ~ sQ140_spl
| ~ sQ93_spl
| ~ sQ146_spl
| equiv(X0,X0) = not(not(equiv(X0,X0))) ),
inference(forward_demodulation,[status(thm)],[f2554,f65835]) ).
fof(f66281,plain,
! [X0,X1] :
( ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ103_spl
| ~ sQ168_spl
| ~ sQ170_spl
| ~ sQ98_spl
| ~ sQ143_spl
| ~ sQ137_spl
| ~ sQ134_spl
| ~ sQ140_spl
| ~ sQ93_spl
| ~ sQ146_spl
| or(X0,not(not(X1))) = implies(not(X0),X1) ),
inference(paramodulation,[status(thm)],[f1633,f65722]) ).
fof(f66442,plain,
! [X0,X1] :
( ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ103_spl
| ~ sQ168_spl
| ~ sQ170_spl
| ~ sQ98_spl
| ~ sQ143_spl
| ~ sQ137_spl
| ~ sQ134_spl
| ~ sQ140_spl
| ~ sQ93_spl
| ~ sQ146_spl
| or(X0,not(not(X1))) = or(X0,X1) ),
inference(forward_demodulation,[status(thm)],[f1633,f66281]) ).
fof(f67700,plain,
! [X0,X1] :
( ~ sQ87_spl
| ~ sQ103_spl
| ~ sQ143_spl
| ~ sQ170_spl
| ~ sQ98_spl
| ~ sQ137_spl
| ~ sQ134_spl
| ~ sQ83_spl
| ~ sQ79_spl
| ~ sQ168_spl
| ~ sQ140_spl
| ~ sQ93_spl
| ~ sQ146_spl
| ~ is_a_theorem(necessarily(equiv(X1,X1)))
| is_a_theorem(strict_implies(X0,equiv(X1,X1))) ),
inference(paramodulation,[status(thm)],[f66097,f51993]) ).
fof(f67949,plain,
! [X0,X1] :
( ~ sQ87_spl
| ~ sQ103_spl
| ~ sQ143_spl
| ~ sQ170_spl
| ~ sQ98_spl
| ~ sQ137_spl
| ~ sQ134_spl
| ~ sQ83_spl
| ~ sQ79_spl
| ~ sQ168_spl
| ~ sQ140_spl
| ~ sQ93_spl
| ~ sQ146_spl
| ~ is_a_theorem(strict_equiv(X1,X1))
| is_a_theorem(strict_implies(X0,equiv(X1,X1))) ),
inference(forward_demodulation,[status(thm)],[f2662,f67700]) ).
fof(f67950,plain,
! [X0,X1] :
( ~ sQ87_spl
| ~ sQ103_spl
| ~ sQ143_spl
| ~ sQ170_spl
| ~ sQ98_spl
| ~ sQ137_spl
| ~ sQ134_spl
| ~ sQ83_spl
| ~ sQ79_spl
| ~ sQ168_spl
| ~ sQ140_spl
| ~ sQ93_spl
| ~ sQ146_spl
| is_a_theorem(strict_implies(X0,equiv(X1,X1))) ),
inference(forward_subsumption_resolution,[status(thm)],[f67949,f2550]) ).
fof(f68139,plain,
! [X0,X1] :
( ~ sQ93_spl
| ~ sQ98_spl
| ~ sQ140_spl
| ~ sQ87_spl
| ~ sQ103_spl
| ~ sQ143_spl
| ~ sQ170_spl
| ~ sQ137_spl
| ~ sQ134_spl
| ~ sQ83_spl
| ~ sQ79_spl
| ~ sQ168_spl
| ~ sQ146_spl
| is_a_theorem(equiv(X1,X1))
| ~ is_a_theorem(X0) ),
inference(resolution,[status(thm)],[f67950,f39329]) ).
fof(f68182,definition,
! [X1] :
( sQ283_spl
<=> is_a_theorem(equiv(X1,X1)) ),
introduced(definition,[new_symbols(definition,[sQ283_spl])],[split_symbol_definition]) ).
fof(f68183,plain,
! [X0] :
( ~ sQ283_spl
| is_a_theorem(equiv(X0,X0)) ),
inference(component_clause,[status(thm)],[f68182]) ).
fof(f68187,plain,
( ~ sQ93_spl
| ~ sQ98_spl
| ~ sQ140_spl
| ~ sQ87_spl
| ~ sQ103_spl
| ~ sQ143_spl
| ~ sQ170_spl
| ~ sQ137_spl
| ~ sQ134_spl
| ~ sQ83_spl
| ~ sQ79_spl
| ~ sQ168_spl
| ~ sQ146_spl
| sQ283_spl
| sQ172_spl ),
inference(split_clause,[status(thm)],[f68139,f1119,f68182,f867,f947,f621,f635,f823,f834,f954,f856,f709,f649,f845,f690,f671]) ).
fof(f72161,plain,
( ~ sQ9_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f364,f328]) ).
fof(f72162,plain,
~ sQ9_spl,
inference(contradiction_clause,[status(thm)],[f72161]) ).
fof(f72167,plain,
! [X0,X1] :
( ~ sQ87_spl
| ~ sQ140_spl
| ~ sQ93_spl
| ~ sQ98_spl
| ~ sQ283_spl
| is_a_theorem(and(implies(X1,X1),and(implies(X1,X1),X0)))
| ~ is_a_theorem(X0) ),
inference(resolution,[status(thm)],[f68183,f39893]) ).
fof(f72173,plain,
! [X0,X1] :
( ~ sQ87_spl
| ~ sQ140_spl
| ~ sQ93_spl
| ~ sQ98_spl
| ~ sQ283_spl
| ~ sQ103_spl
| ~ sQ170_spl
| ~ sQ143_spl
| ~ sQ137_spl
| ~ sQ134_spl
| is_a_theorem(and(implies(X1,X1),X0))
| ~ is_a_theorem(X0) ),
inference(forward_demodulation,[status(thm)],[f3281,f72167]) ).
fof(f72174,plain,
! [X0,X1] :
( ~ sQ87_spl
| ~ sQ140_spl
| ~ sQ93_spl
| ~ sQ98_spl
| ~ sQ283_spl
| ~ sQ103_spl
| ~ sQ170_spl
| ~ sQ143_spl
| ~ sQ137_spl
| ~ sQ134_spl
| is_a_theorem(and(equiv(X1,X1),X0))
| ~ is_a_theorem(X0) ),
inference(forward_demodulation,[status(thm)],[f2554,f72173]) ).
fof(f76009,plain,
! [X0,X1] :
( ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ87_spl
| ~ sQ93_spl
| ~ sQ140_spl
| ~ sQ98_spl
| ~ sQ283_spl
| ~ sQ103_spl
| ~ sQ170_spl
| ~ sQ143_spl
| ~ sQ137_spl
| ~ sQ134_spl
| is_a_theorem(and(or(X1,not(X1)),and(implies(not(X1),not(X1)),X0)))
| ~ is_a_theorem(X0) ),
inference(resolution,[status(thm)],[f72174,f3611]) ).
fof(f76044,plain,
! [X0,X1] :
( ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ87_spl
| ~ sQ93_spl
| ~ sQ140_spl
| ~ sQ98_spl
| ~ sQ283_spl
| ~ sQ103_spl
| ~ sQ170_spl
| ~ sQ143_spl
| ~ sQ137_spl
| ~ sQ134_spl
| is_a_theorem(and(or(X1,not(X1)),and(or(X1,not(X1)),X0)))
| ~ is_a_theorem(X0) ),
inference(forward_demodulation,[status(thm)],[f1633,f76009]) ).
fof(f76045,plain,
! [X0,X1] :
( ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ87_spl
| ~ sQ93_spl
| ~ sQ140_spl
| ~ sQ98_spl
| ~ sQ283_spl
| ~ sQ103_spl
| ~ sQ170_spl
| ~ sQ143_spl
| ~ sQ137_spl
| ~ sQ134_spl
| is_a_theorem(and(or(X1,not(X1)),X0))
| ~ is_a_theorem(X0) ),
inference(forward_demodulation,[status(thm)],[f3281,f76044]) ).
fof(f83656,plain,
! [X0,X1] :
( ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ103_spl
| ~ sQ168_spl
| ~ sQ170_spl
| ~ sQ98_spl
| ~ sQ143_spl
| ~ sQ137_spl
| ~ sQ134_spl
| ~ sQ140_spl
| ~ sQ93_spl
| ~ sQ146_spl
| ~ sQ87_spl
| ~ sQ283_spl
| is_a_theorem(and(or(not(X1),X1),X0))
| ~ is_a_theorem(X0) ),
inference(paramodulation,[status(thm)],[f66442,f76045]) ).
fof(f84281,plain,
! [X0] :
( ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ87_spl
| ~ sQ103_spl
| ~ sQ168_spl
| ~ sQ170_spl
| ~ sQ98_spl
| ~ sQ143_spl
| ~ sQ137_spl
| ~ sQ134_spl
| ~ sQ140_spl
| ~ sQ93_spl
| ~ sQ146_spl
| ~ sQ283_spl
| is_a_theorem(equiv(not(not(X0)),X0))
| ~ is_a_theorem(implies(X0,not(not(X0)))) ),
inference(paramodulation,[status(thm)],[f1679,f83656]) ).
fof(f84320,plain,
! [X0] :
( ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ87_spl
| ~ sQ103_spl
| ~ sQ168_spl
| ~ sQ170_spl
| ~ sQ98_spl
| ~ sQ143_spl
| ~ sQ137_spl
| ~ sQ134_spl
| ~ sQ140_spl
| ~ sQ93_spl
| ~ sQ146_spl
| ~ sQ283_spl
| is_a_theorem(equiv(not(not(X0)),X0))
| ~ is_a_theorem(implies(X0,X0)) ),
inference(forward_demodulation,[status(thm)],[f65722,f84281]) ).
fof(f84321,plain,
! [X0] :
( ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ87_spl
| ~ sQ103_spl
| ~ sQ168_spl
| ~ sQ170_spl
| ~ sQ98_spl
| ~ sQ143_spl
| ~ sQ137_spl
| ~ sQ134_spl
| ~ sQ140_spl
| ~ sQ93_spl
| ~ sQ146_spl
| ~ sQ283_spl
| is_a_theorem(equiv(not(not(X0)),X0))
| ~ is_a_theorem(equiv(X0,X0)) ),
inference(forward_demodulation,[status(thm)],[f2554,f84320]) ).
fof(f84322,plain,
! [X0] :
( ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ87_spl
| ~ sQ103_spl
| ~ sQ168_spl
| ~ sQ170_spl
| ~ sQ98_spl
| ~ sQ143_spl
| ~ sQ137_spl
| ~ sQ134_spl
| ~ sQ140_spl
| ~ sQ93_spl
| ~ sQ146_spl
| ~ sQ283_spl
| is_a_theorem(equiv(not(not(X0)),X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f84321,f68183]) ).
fof(f84350,plain,
! [X0] :
( ~ sQ6_spl
| ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ87_spl
| ~ sQ103_spl
| ~ sQ168_spl
| ~ sQ170_spl
| ~ sQ98_spl
| ~ sQ143_spl
| ~ sQ137_spl
| ~ sQ134_spl
| ~ sQ140_spl
| ~ sQ93_spl
| ~ sQ146_spl
| ~ sQ283_spl
| not(not(X0)) = X0 ),
inference(resolution,[status(thm)],[f84322,f352]) ).
fof(f84604,plain,
! [X0,X1] :
( ~ sQ6_spl
| ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ87_spl
| ~ sQ103_spl
| ~ sQ168_spl
| ~ sQ170_spl
| ~ sQ98_spl
| ~ sQ143_spl
| ~ sQ137_spl
| ~ sQ134_spl
| ~ sQ140_spl
| ~ sQ93_spl
| ~ sQ146_spl
| ~ sQ283_spl
| or(not(X0),X1) = implies(X0,X1) ),
inference(paramodulation,[status(thm)],[f84350,f1633]) ).
fof(f85694,plain,
! [X0,X1] :
( ~ sQ83_spl
| ~ sQ103_spl
| ~ sQ134_spl
| ~ sQ170_spl
| ~ sQ98_spl
| ~ sQ79_spl
| ~ sQ6_spl
| ~ sQ87_spl
| ~ sQ168_spl
| ~ sQ143_spl
| ~ sQ137_spl
| ~ sQ140_spl
| ~ sQ93_spl
| ~ sQ146_spl
| ~ sQ283_spl
| or(X0,not(X1)) = implies(X1,X0) ),
inference(paramodulation,[status(thm)],[f2878,f84604]) ).
fof(f87080,plain,
( sQ11_spl
| ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ103_spl
| ~ sQ134_spl
| ~ sQ170_spl
| ~ sQ98_spl
| ~ sQ6_spl
| ~ sQ87_spl
| ~ sQ168_spl
| ~ sQ143_spl
| ~ sQ137_spl
| ~ sQ140_spl
| ~ sQ93_spl
| ~ sQ146_spl
| ~ sQ283_spl
| ~ is_a_theorem(implies(implies(sK4_skl,sK5_skl),implies(sK4_skl,sK5_skl))) ),
inference(backward_demodulation,[status(thm)],[f85694,f2492]) ).
fof(f87210,plain,
( sQ11_spl
| ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ103_spl
| ~ sQ134_spl
| ~ sQ170_spl
| ~ sQ98_spl
| ~ sQ6_spl
| ~ sQ87_spl
| ~ sQ168_spl
| ~ sQ143_spl
| ~ sQ137_spl
| ~ sQ140_spl
| ~ sQ93_spl
| ~ sQ146_spl
| ~ sQ283_spl
| ~ is_a_theorem(equiv(implies(sK4_skl,sK5_skl),implies(sK4_skl,sK5_skl))) ),
inference(forward_demodulation,[status(thm)],[f2554,f87080]) ).
fof(f87211,plain,
( sQ11_spl
| ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ103_spl
| ~ sQ134_spl
| ~ sQ170_spl
| ~ sQ98_spl
| ~ sQ6_spl
| ~ sQ87_spl
| ~ sQ168_spl
| ~ sQ143_spl
| ~ sQ137_spl
| ~ sQ140_spl
| ~ sQ93_spl
| ~ sQ146_spl
| ~ sQ283_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f87210,f68183]) ).
fof(f87212,plain,
( sQ11_spl
| ~ sQ79_spl
| ~ sQ83_spl
| ~ sQ103_spl
| ~ sQ134_spl
| ~ sQ170_spl
| ~ sQ98_spl
| ~ sQ6_spl
| ~ sQ87_spl
| ~ sQ168_spl
| ~ sQ143_spl
| ~ sQ137_spl
| ~ sQ140_spl
| ~ sQ93_spl
| ~ sQ146_spl
| ~ sQ283_spl ),
inference(contradiction_clause,[status(thm)],[f87211]) ).
fof(f87213,plain,
$false,
inference(sat_refutation,[status(thm)],[f354,f373,f624,f638,f652,f674,f693,f712,f826,f837,f848,f859,f870,f950,f957,f959,f961,f963,f965,f967,f969,f973,f975,f977,f994,f1028,f1044,f1078,f1082,f11330,f68187,f72162,f87212]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : LCL551+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% 0.00/0.02 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.03/0.30 % Computer : n012.cluster.edu
% 0.03/0.30 % Model : x86_64 x86_64
% 0.03/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.30 % Memory : 8046.5625MB
% 0.03/0.30 % OS : Linux 6.8.0-71-generic
% 0.03/0.30 % CPULimit : 300
% 0.03/0.30 % WCLimit : 300
% 0.03/0.30 % DateTime : Mon Sep 21 00:37:51 UTC 2026
% 0.03/0.30 % CPUTime :
% 0.03/0.30 % Drodi V4.1.1
% 83.15/10.87 % Refutation found
% 83.15/10.87 % SZS status Theorem for theBenchmark: Theorem is valid
% 83.15/10.87 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 6.08/11.67 % Elapsed time: 11.359352 seconds
% 6.08/11.67 % CPU time: 85.193303 seconds
% 6.08/11.67 % Total memory used: 1.259 GB
% 6.08/11.67 % Net memory used: 1.164 GB
%------------------------------------------------------------------------------