%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LCL573+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 : n026.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:08:01 PM UTC 2026
% Result : Theorem 40.69s 5.62s
% Output : CNFRefutation 40.69s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 59
% Syntax : Number of formulae : 272 ( 44 unt; 31 def)
% Number of atoms : 1107 ( 70 equ)
% Maximal formula atoms : 15 ( 4 avg)
% Number of connectives : 1575 ( 740 ~; 749 |; 35 &)
% ( 44 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 6 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 48 ( 46 usr; 46 prp; 0-2 aty)
% Number of functors : 27 ( 27 usr; 19 con; 0-2 aty)
% Number of variables : 319 ( 298 !; 21 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
( op_or
=> ! [X,Y] : or(X,Y) = not(and(not(X),not(Y))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,axiom,
( op_implies_and
=> ! [X,Y] : implies(X,Y) = not(and(X,not(Y))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,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(f8,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(f9,axiom,
( substitution_strict_equiv
<=> ! [X,Y] :
( is_a_theorem(strict_equiv(X,Y))
=> X = Y ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f14,axiom,
( axiom_5
<=> ! [X] : is_a_theorem(implies(possibly(X),necessarily(possibly(X)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f19,axiom,
( axiom_m1
<=> ! [X,Y] : is_a_theorem(strict_implies(and(X,Y),and(Y,X))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f20,axiom,
( axiom_m2
<=> ! [X,Y] : is_a_theorem(strict_implies(and(X,Y),X)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f21,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(f22,axiom,
( axiom_m4
<=> ! [X] : is_a_theorem(strict_implies(X,and(X,X))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f23,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(f28,axiom,
( axiom_m10
<=> ! [X] : is_a_theorem(strict_implies(possibly(X),necessarily(possibly(X)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f31,axiom,
( op_strict_implies
=> ! [X,Y] : strict_implies(X,Y) = necessarily(implies(X,Y)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f32,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(f34,axiom,
op_or,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f36,axiom,
op_strict_implies,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f38,axiom,
op_strict_equiv,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f39,axiom,
modus_ponens_strict_implies,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f40,axiom,
substitution_strict_equiv,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f41,axiom,
adjunction,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f42,axiom,
axiom_m1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f43,axiom,
axiom_m2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f44,axiom,
axiom_m3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f45,axiom,
axiom_m4,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f46,axiom,
axiom_m5,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f47,axiom,
axiom_m10,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f49,axiom,
op_implies_and,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f52,conjecture,
axiom_5,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f53,negated_conjecture,
~ axiom_5,
inference(negated_conjecture,[status(cth)],[f52]) ).
fof(f54,plain,
( ! [X,Y] : or(X,Y) = not(and(not(X),not(Y)))
| ~ op_or ),
inference(pre_NNF_transformation,[status(thm)],[f1]) ).
fof(f55,plain,
! [X0,X1] :
( or(X0,X1) = not(and(not(X0),not(X1)))
| ~ op_or ),
inference(cnf_transformation,[status(thm)],[f54]) ).
fof(f58,plain,
( ! [X,Y] : implies(X,Y) = not(and(X,not(Y)))
| ~ op_implies_and ),
inference(pre_NNF_transformation,[status(thm)],[f3]) ).
fof(f59,plain,
! [X0,X1] :
( implies(X0,X1) = not(and(X0,not(X1)))
| ~ op_implies_and ),
inference(cnf_transformation,[status(thm)],[f58]) ).
fof(f70,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)],[f7]) ).
fof(f71,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)],[f70]) ).
fof(f72,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)],[f71]) ).
fof(f73,plain,
( ( ( ~ is_a_theorem(sK1_skl)
& is_a_theorem(strict_implies(sK2_skl,sK1_skl))
& is_a_theorem(sK2_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,[sK1_skl,sK2_skl]),skolemize(Y,sK1_skl),skolemize(X,sK2_skl)],[f72]) ).
fof(f74,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)],[f73]) ).
fof(f78,plain,
( adjunction
<=> ! [X,Y] :
( is_a_theorem(and(X,Y))
| ~ is_a_theorem(Y)
| ~ is_a_theorem(X) ) ),
inference(pre_NNF_transformation,[status(thm)],[f8]) ).
fof(f79,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)],[f78]) ).
fof(f80,plain,
( ( ( ~ is_a_theorem(and(sK3_skl,sK4_skl))
& is_a_theorem(sK4_skl)
& is_a_theorem(sK3_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,[sK3_skl,sK4_skl]),skolemize(X,sK3_skl),skolemize(Y,sK4_skl)],[f79]) ).
fof(f81,plain,
! [X0,X1] :
( is_a_theorem(and(X0,X1))
| ~ is_a_theorem(X1)
| ~ is_a_theorem(X0)
| ~ adjunction ),
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f85,plain,
( substitution_strict_equiv
<=> ! [X,Y] :
( X = Y
| ~ is_a_theorem(strict_equiv(X,Y)) ) ),
inference(pre_NNF_transformation,[status(thm)],[f9]) ).
fof(f86,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)],[f85]) ).
fof(f87,plain,
( ( ( sK5_skl != sK6_skl
& is_a_theorem(strict_equiv(sK5_skl,sK6_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,[sK5_skl,sK6_skl]),skolemize(X,sK5_skl),skolemize(Y,sK6_skl)],[f86]) ).
fof(f88,plain,
! [X0,X1] :
( X0 = X1
| ~ is_a_theorem(strict_equiv(X0,X1))
| ~ substitution_strict_equiv ),
inference(cnf_transformation,[status(thm)],[f87]) ).
fof(f107,plain,
( ( ? [X] : ~ is_a_theorem(implies(possibly(X),necessarily(possibly(X))))
| axiom_5 )
& ( ! [X] : is_a_theorem(implies(possibly(X),necessarily(possibly(X))))
| ~ axiom_5 ) ),
inference(NNF_transformation,[status(thm)],[f14]) ).
fof(f108,plain,
( ( ~ is_a_theorem(implies(possibly(sK12_skl),necessarily(possibly(sK12_skl))))
| axiom_5 )
& ( ! [X] : is_a_theorem(implies(possibly(X),necessarily(possibly(X))))
| ~ axiom_5 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12_skl]),skolemize(X,sK12_skl)],[f107]) ).
fof(f110,plain,
( ~ is_a_theorem(implies(possibly(sK12_skl),necessarily(possibly(sK12_skl))))
| axiom_5 ),
inference(cnf_transformation,[status(thm)],[f108]) ).
fof(f127,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)],[f19]) ).
fof(f128,plain,
( ( ~ is_a_theorem(strict_implies(and(sK21_skl,sK22_skl),and(sK22_skl,sK21_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,[sK21_skl,sK22_skl]),skolemize(X,sK21_skl),skolemize(Y,sK22_skl)],[f127]) ).
fof(f129,plain,
! [X0,X1] :
( is_a_theorem(strict_implies(and(X0,X1),and(X1,X0)))
| ~ axiom_m1 ),
inference(cnf_transformation,[status(thm)],[f128]) ).
fof(f131,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)],[f20]) ).
fof(f132,plain,
( ( ~ is_a_theorem(strict_implies(and(sK23_skl,sK24_skl),sK23_skl))
| axiom_m2 )
& ( ! [X,Y] : is_a_theorem(strict_implies(and(X,Y),X))
| ~ axiom_m2 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK23_skl,sK24_skl]),skolemize(X,sK23_skl),skolemize(Y,sK24_skl)],[f131]) ).
fof(f133,plain,
! [X0,X1] :
( is_a_theorem(strict_implies(and(X0,X1),X0))
| ~ axiom_m2 ),
inference(cnf_transformation,[status(thm)],[f132]) ).
fof(f135,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)],[f21]) ).
fof(f136,plain,
( ( ~ is_a_theorem(strict_implies(and(and(sK25_skl,sK26_skl),sK27_skl),and(sK25_skl,and(sK26_skl,sK27_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,[sK25_skl,sK26_skl,sK27_skl]),skolemize(X,sK25_skl),skolemize(Y,sK26_skl),skolemize(Z,sK27_skl)],[f135]) ).
fof(f137,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)],[f136]) ).
fof(f139,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)],[f22]) ).
fof(f140,plain,
( ( ~ is_a_theorem(strict_implies(sK28_skl,and(sK28_skl,sK28_skl)))
| axiom_m4 )
& ( ! [X] : is_a_theorem(strict_implies(X,and(X,X)))
| ~ axiom_m4 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK28_skl]),skolemize(X,sK28_skl)],[f139]) ).
fof(f141,plain,
! [X0] :
( is_a_theorem(strict_implies(X0,and(X0,X0)))
| ~ axiom_m4 ),
inference(cnf_transformation,[status(thm)],[f140]) ).
fof(f143,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)],[f23]) ).
fof(f144,plain,
( ( ~ is_a_theorem(strict_implies(and(strict_implies(sK29_skl,sK30_skl),strict_implies(sK30_skl,sK31_skl)),strict_implies(sK29_skl,sK31_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,[sK29_skl,sK30_skl,sK31_skl]),skolemize(X,sK29_skl),skolemize(Y,sK30_skl),skolemize(Z,sK31_skl)],[f143]) ).
fof(f145,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)],[f144]) ).
fof(f163,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)],[f28]) ).
fof(f164,plain,
( ( ~ is_a_theorem(strict_implies(possibly(sK38_skl),necessarily(possibly(sK38_skl))))
| axiom_m10 )
& ( ! [X] : is_a_theorem(strict_implies(possibly(X),necessarily(possibly(X))))
| ~ axiom_m10 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK38_skl]),skolemize(X,sK38_skl)],[f163]) ).
fof(f165,plain,
! [X0] :
( is_a_theorem(strict_implies(possibly(X0),necessarily(possibly(X0))))
| ~ axiom_m10 ),
inference(cnf_transformation,[status(thm)],[f164]) ).
fof(f171,plain,
( ! [X,Y] : strict_implies(X,Y) = necessarily(implies(X,Y))
| ~ op_strict_implies ),
inference(pre_NNF_transformation,[status(thm)],[f31]) ).
fof(f172,plain,
! [X0,X1] :
( strict_implies(X0,X1) = necessarily(implies(X0,X1))
| ~ op_strict_implies ),
inference(cnf_transformation,[status(thm)],[f171]) ).
fof(f173,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)],[f32]) ).
fof(f174,plain,
! [X0,X1] :
( strict_equiv(X0,X1) = and(strict_implies(X0,X1),strict_implies(X1,X0))
| ~ op_strict_equiv ),
inference(cnf_transformation,[status(thm)],[f173]) ).
fof(f176,plain,
op_or,
inference(cnf_transformation,[status(thm)],[f34]) ).
fof(f178,plain,
op_strict_implies,
inference(cnf_transformation,[status(thm)],[f36]) ).
fof(f180,plain,
op_strict_equiv,
inference(cnf_transformation,[status(thm)],[f38]) ).
fof(f181,plain,
modus_ponens_strict_implies,
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f182,plain,
substitution_strict_equiv,
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f183,plain,
adjunction,
inference(cnf_transformation,[status(thm)],[f41]) ).
fof(f184,plain,
axiom_m1,
inference(cnf_transformation,[status(thm)],[f42]) ).
fof(f185,plain,
axiom_m2,
inference(cnf_transformation,[status(thm)],[f43]) ).
fof(f186,plain,
axiom_m3,
inference(cnf_transformation,[status(thm)],[f44]) ).
fof(f187,plain,
axiom_m4,
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f188,plain,
axiom_m5,
inference(cnf_transformation,[status(thm)],[f46]) ).
fof(f189,plain,
axiom_m10,
inference(cnf_transformation,[status(thm)],[f47]) ).
fof(f191,plain,
op_implies_and,
inference(cnf_transformation,[status(thm)],[f49]) ).
fof(f194,plain,
~ axiom_5,
inference(cnf_transformation,[status(thm)],[f53]) ).
fof(f195,definition,
( sQ0_spl
<=> op_or ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f197,plain,
( sQ0_spl
| ~ op_or ),
inference(component_clause,[status(thm)],[f195]) ).
fof(f198,definition,
! [X0,X1] :
( sQ1_spl
<=> or(X0,X1) = not(and(not(X0),not(X1))) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f199,plain,
! [X0,X1] :
( ~ sQ1_spl
| or(X0,X1) = not(and(not(X0),not(X1))) ),
inference(component_clause,[status(thm)],[f198]) ).
fof(f201,plain,
( sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f55,f195,f198]) ).
fof(f209,definition,
( sQ4_spl
<=> op_implies_and ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f211,plain,
( sQ4_spl
| ~ op_implies_and ),
inference(component_clause,[status(thm)],[f209]) ).
fof(f212,definition,
! [X0,X1] :
( sQ5_spl
<=> implies(X0,X1) = not(and(X0,not(X1))) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f213,plain,
! [X0,X1] :
( ~ sQ5_spl
| implies(X0,X1) = not(and(X0,not(X1))) ),
inference(component_clause,[status(thm)],[f212]) ).
fof(f215,plain,
( sQ5_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f59,f209,f212]) ).
fof(f245,definition,
( sQ14_spl
<=> modus_ponens_strict_implies ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f247,plain,
( sQ14_spl
| ~ modus_ponens_strict_implies ),
inference(component_clause,[status(thm)],[f245]) ).
fof(f248,definition,
! [X0,X1] :
( sQ15_spl
<=> ( is_a_theorem(X1)
| ~ is_a_theorem(strict_implies(X0,X1))
| ~ is_a_theorem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f249,plain,
! [X0,X1] :
( ~ sQ15_spl
| is_a_theorem(X1)
| ~ is_a_theorem(strict_implies(X0,X1))
| ~ is_a_theorem(X0) ),
inference(component_clause,[status(thm)],[f248]) ).
fof(f251,plain,
( sQ15_spl
| ~ sQ14_spl ),
inference(split_clause,[status(thm)],[f74,f245,f248]) ).
fof(f264,definition,
( sQ19_spl
<=> adjunction ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f266,plain,
( sQ19_spl
| ~ adjunction ),
inference(component_clause,[status(thm)],[f264]) ).
fof(f267,definition,
! [X0,X1] :
( sQ20_spl
<=> ( is_a_theorem(and(X0,X1))
| ~ is_a_theorem(X1)
| ~ is_a_theorem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f268,plain,
! [X0,X1] :
( ~ sQ20_spl
| is_a_theorem(and(X0,X1))
| ~ is_a_theorem(X1)
| ~ is_a_theorem(X0) ),
inference(component_clause,[status(thm)],[f267]) ).
fof(f270,plain,
( sQ20_spl
| ~ sQ19_spl ),
inference(split_clause,[status(thm)],[f81,f264,f267]) ).
fof(f283,definition,
( sQ24_spl
<=> substitution_strict_equiv ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f285,plain,
( sQ24_spl
| ~ substitution_strict_equiv ),
inference(component_clause,[status(thm)],[f283]) ).
fof(f286,definition,
! [X0,X1] :
( sQ25_spl
<=> ( X0 = X1
| ~ is_a_theorem(strict_equiv(X0,X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f287,plain,
! [X0,X1] :
( ~ sQ25_spl
| X0 = X1
| ~ is_a_theorem(strict_equiv(X0,X1)) ),
inference(component_clause,[status(thm)],[f286]) ).
fof(f289,plain,
( sQ25_spl
| ~ sQ24_spl ),
inference(split_clause,[status(thm)],[f88,f283,f286]) ).
fof(f342,definition,
( sQ40_spl
<=> axiom_5 ),
introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition]) ).
fof(f343,plain,
( ~ sQ40_spl
| axiom_5 ),
inference(component_clause,[status(thm)],[f342]) ).
fof(f345,definition,
! [X0] :
( sQ41_spl
<=> is_a_theorem(implies(possibly(X0),necessarily(possibly(X0)))) ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f346,plain,
! [X0] :
( ~ sQ41_spl
| is_a_theorem(implies(possibly(X0),necessarily(possibly(X0)))) ),
inference(component_clause,[status(thm)],[f345]) ).
fof(f349,definition,
( sQ42_spl
<=> is_a_theorem(implies(possibly(sK12_skl),necessarily(possibly(sK12_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f351,plain,
( sQ42_spl
| ~ is_a_theorem(implies(possibly(sK12_skl),necessarily(possibly(sK12_skl)))) ),
inference(component_clause,[status(thm)],[f349]) ).
fof(f352,plain,
( ~ sQ42_spl
| sQ40_spl ),
inference(split_clause,[status(thm)],[f110,f342,f349]) ).
fof(f397,definition,
( sQ55_spl
<=> axiom_m1 ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f399,plain,
( sQ55_spl
| ~ axiom_m1 ),
inference(component_clause,[status(thm)],[f397]) ).
fof(f400,definition,
! [X0,X1] :
( sQ56_spl
<=> is_a_theorem(strict_implies(and(X0,X1),and(X1,X0))) ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f401,plain,
! [X0,X1] :
( ~ sQ56_spl
| is_a_theorem(strict_implies(and(X0,X1),and(X1,X0))) ),
inference(component_clause,[status(thm)],[f400]) ).
fof(f403,plain,
( sQ56_spl
| ~ sQ55_spl ),
inference(split_clause,[status(thm)],[f129,f397,f400]) ).
fof(f408,definition,
( sQ58_spl
<=> axiom_m2 ),
introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition]) ).
fof(f410,plain,
( sQ58_spl
| ~ axiom_m2 ),
inference(component_clause,[status(thm)],[f408]) ).
fof(f411,definition,
! [X0,X1] :
( sQ59_spl
<=> is_a_theorem(strict_implies(and(X0,X1),X0)) ),
introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition]) ).
fof(f412,plain,
! [X0,X1] :
( ~ sQ59_spl
| is_a_theorem(strict_implies(and(X0,X1),X0)) ),
inference(component_clause,[status(thm)],[f411]) ).
fof(f414,plain,
( sQ59_spl
| ~ sQ58_spl ),
inference(split_clause,[status(thm)],[f133,f408,f411]) ).
fof(f419,definition,
( sQ61_spl
<=> axiom_m3 ),
introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition]) ).
fof(f421,plain,
( sQ61_spl
| ~ axiom_m3 ),
inference(component_clause,[status(thm)],[f419]) ).
fof(f422,definition,
! [X0,X1,X2] :
( sQ62_spl
<=> is_a_theorem(strict_implies(and(and(X0,X1),X2),and(X0,and(X1,X2)))) ),
introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition]) ).
fof(f423,plain,
! [X0,X1,X2] :
( ~ sQ62_spl
| is_a_theorem(strict_implies(and(and(X0,X1),X2),and(X0,and(X1,X2)))) ),
inference(component_clause,[status(thm)],[f422]) ).
fof(f425,plain,
( sQ62_spl
| ~ sQ61_spl ),
inference(split_clause,[status(thm)],[f137,f419,f422]) ).
fof(f430,definition,
( sQ64_spl
<=> axiom_m4 ),
introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition]) ).
fof(f432,plain,
( sQ64_spl
| ~ axiom_m4 ),
inference(component_clause,[status(thm)],[f430]) ).
fof(f433,definition,
! [X0] :
( sQ65_spl
<=> is_a_theorem(strict_implies(X0,and(X0,X0))) ),
introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition]) ).
fof(f434,plain,
! [X0] :
( ~ sQ65_spl
| is_a_theorem(strict_implies(X0,and(X0,X0))) ),
inference(component_clause,[status(thm)],[f433]) ).
fof(f436,plain,
( sQ65_spl
| ~ sQ64_spl ),
inference(split_clause,[status(thm)],[f141,f430,f433]) ).
fof(f441,definition,
( sQ67_spl
<=> axiom_m5 ),
introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition]) ).
fof(f443,plain,
( sQ67_spl
| ~ axiom_m5 ),
inference(component_clause,[status(thm)],[f441]) ).
fof(f444,definition,
! [X0,X1,X2] :
( sQ68_spl
<=> is_a_theorem(strict_implies(and(strict_implies(X0,X1),strict_implies(X1,X2)),strict_implies(X0,X2))) ),
introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition]) ).
fof(f445,plain,
! [X0,X1,X2] :
( ~ sQ68_spl
| is_a_theorem(strict_implies(and(strict_implies(X0,X1),strict_implies(X1,X2)),strict_implies(X0,X2))) ),
inference(component_clause,[status(thm)],[f444]) ).
fof(f447,plain,
( sQ68_spl
| ~ sQ67_spl ),
inference(split_clause,[status(thm)],[f145,f441,f444]) ).
fof(f496,definition,
( sQ82_spl
<=> axiom_m10 ),
introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition]) ).
fof(f498,plain,
( sQ82_spl
| ~ axiom_m10 ),
inference(component_clause,[status(thm)],[f496]) ).
fof(f499,definition,
! [X0] :
( sQ83_spl
<=> is_a_theorem(strict_implies(possibly(X0),necessarily(possibly(X0)))) ),
introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition]) ).
fof(f500,plain,
! [X0] :
( ~ sQ83_spl
| is_a_theorem(strict_implies(possibly(X0),necessarily(possibly(X0)))) ),
inference(component_clause,[status(thm)],[f499]) ).
fof(f502,plain,
( sQ83_spl
| ~ sQ82_spl ),
inference(split_clause,[status(thm)],[f165,f496,f499]) ).
fof(f521,definition,
( sQ89_spl
<=> op_strict_implies ),
introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition]) ).
fof(f523,plain,
( sQ89_spl
| ~ op_strict_implies ),
inference(component_clause,[status(thm)],[f521]) ).
fof(f524,definition,
! [X0,X1] :
( sQ90_spl
<=> strict_implies(X0,X1) = necessarily(implies(X0,X1)) ),
introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition]) ).
fof(f525,plain,
! [X0,X1] :
( ~ sQ90_spl
| strict_implies(X0,X1) = necessarily(implies(X0,X1)) ),
inference(component_clause,[status(thm)],[f524]) ).
fof(f527,plain,
( sQ90_spl
| ~ sQ89_spl ),
inference(split_clause,[status(thm)],[f172,f521,f524]) ).
fof(f528,definition,
( sQ91_spl
<=> op_strict_equiv ),
introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition]) ).
fof(f530,plain,
( sQ91_spl
| ~ op_strict_equiv ),
inference(component_clause,[status(thm)],[f528]) ).
fof(f531,definition,
! [X0,X1] :
( sQ92_spl
<=> strict_equiv(X0,X1) = and(strict_implies(X0,X1),strict_implies(X1,X0)) ),
introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition]) ).
fof(f532,plain,
! [X0,X1] :
( ~ sQ92_spl
| strict_equiv(X0,X1) = and(strict_implies(X0,X1),strict_implies(X1,X0)) ),
inference(component_clause,[status(thm)],[f531]) ).
fof(f534,plain,
( sQ92_spl
| ~ sQ91_spl ),
inference(split_clause,[status(thm)],[f174,f528,f531]) ).
fof(f535,plain,
( sQ91_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f530,f180]) ).
fof(f536,plain,
sQ91_spl,
inference(contradiction_clause,[status(thm)],[f535]) ).
fof(f537,plain,
( sQ19_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f266,f183]) ).
fof(f538,plain,
sQ19_spl,
inference(contradiction_clause,[status(thm)],[f537]) ).
fof(f539,plain,
( sQ14_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f247,f181]) ).
fof(f540,plain,
sQ14_spl,
inference(contradiction_clause,[status(thm)],[f539]) ).
fof(f541,plain,
( sQ24_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f285,f182]) ).
fof(f542,plain,
sQ24_spl,
inference(contradiction_clause,[status(thm)],[f541]) ).
fof(f543,plain,
( sQ89_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f523,f178]) ).
fof(f544,plain,
sQ89_spl,
inference(contradiction_clause,[status(thm)],[f543]) ).
fof(f549,plain,
( sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f211,f191]) ).
fof(f550,plain,
sQ4_spl,
inference(contradiction_clause,[status(thm)],[f549]) ).
fof(f551,plain,
( sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f197,f176]) ).
fof(f552,plain,
sQ0_spl,
inference(contradiction_clause,[status(thm)],[f551]) ).
fof(f555,plain,
( sQ82_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f498,f189]) ).
fof(f556,plain,
sQ82_spl,
inference(contradiction_clause,[status(thm)],[f555]) ).
fof(f570,plain,
( sQ64_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f432,f187]) ).
fof(f571,plain,
sQ64_spl,
inference(contradiction_clause,[status(thm)],[f570]) ).
fof(f575,plain,
( sQ58_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f410,f185]) ).
fof(f576,plain,
sQ58_spl,
inference(contradiction_clause,[status(thm)],[f575]) ).
fof(f578,plain,
! [X0,X1] :
( ~ sQ92_spl
| ~ sQ56_spl
| is_a_theorem(strict_implies(strict_equiv(X0,X1),and(strict_implies(X1,X0),strict_implies(X0,X1)))) ),
inference(paramodulation,[status(thm)],[f532,f401]) ).
fof(f580,plain,
! [X0,X1] :
( ~ sQ92_spl
| ~ sQ56_spl
| is_a_theorem(strict_implies(strict_equiv(X0,X1),strict_equiv(X1,X0))) ),
inference(forward_demodulation,[status(thm)],[f532,f578]) ).
fof(f592,plain,
! [X0,X1] :
( ~ sQ92_spl
| ~ sQ20_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)],[f532,f268]) ).
fof(f598,plain,
! [X0,X1] :
( ~ sQ92_spl
| ~ sQ68_spl
| is_a_theorem(strict_implies(strict_equiv(X0,X1),strict_implies(X0,X0))) ),
inference(paramodulation,[status(thm)],[f532,f445]) ).
fof(f600,plain,
( sQ67_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f443,f188]) ).
fof(f601,plain,
sQ67_spl,
inference(contradiction_clause,[status(thm)],[f600]) ).
fof(f606,plain,
( sQ61_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f421,f186]) ).
fof(f607,plain,
sQ61_spl,
inference(contradiction_clause,[status(thm)],[f606]) ).
fof(f610,plain,
( sQ55_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f399,f184]) ).
fof(f611,plain,
sQ55_spl,
inference(contradiction_clause,[status(thm)],[f610]) ).
fof(f620,definition,
! [X1] :
( sQ94_spl
<=> ~ is_a_theorem(X1) ),
introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition]) ).
fof(f621,plain,
! [X0] :
( ~ sQ94_spl
| ~ is_a_theorem(X0) ),
inference(component_clause,[status(thm)],[f620]) ).
fof(f633,plain,
! [X0,X1] :
( ~ sQ15_spl
| ~ sQ92_spl
| ~ sQ68_spl
| is_a_theorem(strict_implies(X0,X0))
| ~ is_a_theorem(strict_equiv(X0,X1)) ),
inference(resolution,[status(thm)],[f598,f249]) ).
fof(f639,plain,
! [X0,X1] :
( ~ sQ15_spl
| ~ sQ92_spl
| ~ sQ56_spl
| is_a_theorem(strict_equiv(X1,X0))
| ~ is_a_theorem(strict_equiv(X0,X1)) ),
inference(resolution,[status(thm)],[f580,f249]) ).
fof(f653,plain,
! [X0,X1] :
( ~ sQ15_spl
| ~ sQ92_spl
| ~ sQ68_spl
| ~ sQ56_spl
| is_a_theorem(strict_implies(X1,X1))
| ~ is_a_theorem(strict_equiv(X0,X1)) ),
inference(resolution,[status(thm)],[f639,f633]) ).
fof(f678,plain,
( sQ42_spl
| ~ sQ41_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f351,f346]) ).
fof(f679,plain,
( sQ42_spl
| ~ sQ41_spl ),
inference(contradiction_clause,[status(thm)],[f678]) ).
fof(f700,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ sQ5_spl
| or(X0,X1) = implies(not(X0),X1) ),
inference(forward_demodulation,[status(thm)],[f213,f199]) ).
fof(f701,plain,
! [X0,X1,X2] :
( ~ sQ5_spl
| ~ sQ1_spl
| or(and(X0,not(X1)),X2) = implies(implies(X0,X1),X2) ),
inference(paramodulation,[status(thm)],[f213,f700]) ).
fof(f705,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ sQ5_spl
| ~ sQ90_spl
| strict_implies(not(X0),X1) = necessarily(or(X0,X1)) ),
inference(paramodulation,[status(thm)],[f700,f525]) ).
fof(f733,plain,
! [X0,X1,X2] :
( ~ sQ15_spl
| ~ sQ68_spl
| is_a_theorem(strict_implies(X0,X2))
| ~ is_a_theorem(and(strict_implies(X0,X1),strict_implies(X1,X2))) ),
inference(resolution,[status(thm)],[f445,f249]) ).
fof(f791,plain,
! [X0,X1] :
( ~ sQ92_spl
| ~ sQ56_spl
| ~ sQ20_spl
| is_a_theorem(strict_equiv(strict_equiv(X0,X1),strict_equiv(X1,X0)))
| ~ is_a_theorem(strict_implies(strict_equiv(X0,X1),strict_equiv(X1,X0))) ),
inference(resolution,[status(thm)],[f592,f580]) ).
fof(f798,plain,
! [X0,X1] :
( ~ sQ56_spl
| ~ sQ92_spl
| ~ sQ20_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)],[f592,f401]) ).
fof(f800,plain,
! [X0] :
( ~ sQ65_spl
| ~ sQ92_spl
| ~ sQ20_spl
| is_a_theorem(strict_equiv(and(X0,X0),X0))
| ~ is_a_theorem(strict_implies(and(X0,X0),X0)) ),
inference(resolution,[status(thm)],[f592,f434]) ).
fof(f805,plain,
! [X0,X1] :
( ~ sQ25_spl
| ~ sQ92_spl
| ~ sQ20_spl
| X0 = X1
| ~ is_a_theorem(strict_implies(X1,X0))
| ~ is_a_theorem(strict_implies(X0,X1)) ),
inference(resolution,[status(thm)],[f592,f287]) ).
fof(f808,plain,
! [X0,X1] :
( ~ sQ92_spl
| ~ sQ56_spl
| ~ sQ20_spl
| is_a_theorem(strict_equiv(strict_equiv(X0,X1),strict_equiv(X1,X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f791,f580]) ).
fof(f810,plain,
! [X0,X1] :
( ~ sQ56_spl
| ~ sQ92_spl
| ~ sQ20_spl
| is_a_theorem(strict_equiv(and(X0,X1),and(X1,X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f798,f401]) ).
fof(f811,plain,
! [X0] :
( ~ sQ65_spl
| ~ sQ92_spl
| ~ sQ20_spl
| ~ sQ59_spl
| is_a_theorem(strict_equiv(and(X0,X0),X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[f800,f412]) ).
fof(f812,plain,
! [X0] :
( ~ sQ15_spl
| ~ sQ92_spl
| ~ sQ68_spl
| ~ sQ56_spl
| ~ sQ65_spl
| ~ sQ20_spl
| ~ sQ59_spl
| is_a_theorem(strict_implies(X0,X0)) ),
inference(resolution,[status(thm)],[f811,f653]) ).
fof(f816,plain,
! [X0] :
( ~ sQ25_spl
| ~ sQ65_spl
| ~ sQ92_spl
| ~ sQ20_spl
| ~ sQ59_spl
| and(X0,X0) = X0 ),
inference(resolution,[status(thm)],[f811,f287]) ).
fof(f830,plain,
! [X0,X1] :
( ~ sQ25_spl
| ~ sQ65_spl
| ~ sQ92_spl
| ~ sQ20_spl
| ~ sQ59_spl
| ~ sQ5_spl
| ~ sQ1_spl
| or(not(X0),X1) = implies(implies(not(X0),X0),X1) ),
inference(paramodulation,[status(thm)],[f816,f701]) ).
fof(f832,plain,
! [X0] :
( ~ sQ25_spl
| ~ sQ65_spl
| ~ sQ92_spl
| ~ sQ20_spl
| ~ sQ59_spl
| ~ sQ5_spl
| implies(not(X0),X0) = not(not(X0)) ),
inference(paramodulation,[status(thm)],[f816,f213]) ).
fof(f834,plain,
! [X0,X1] :
( ~ sQ25_spl
| ~ sQ65_spl
| ~ sQ92_spl
| ~ sQ20_spl
| ~ sQ59_spl
| ~ sQ62_spl
| is_a_theorem(strict_implies(and(X0,X1),and(X0,and(X0,X1)))) ),
inference(paramodulation,[status(thm)],[f816,f423]) ).
fof(f842,plain,
! [X0,X1] :
( ~ sQ25_spl
| ~ sQ65_spl
| ~ sQ92_spl
| ~ sQ20_spl
| ~ sQ59_spl
| ~ sQ5_spl
| ~ sQ1_spl
| or(not(X0),X1) = implies(or(X0,X0),X1) ),
inference(forward_demodulation,[status(thm)],[f700,f830]) ).
fof(f843,plain,
! [X0] :
( ~ sQ25_spl
| ~ sQ65_spl
| ~ sQ92_spl
| ~ sQ20_spl
| ~ sQ59_spl
| ~ sQ5_spl
| ~ sQ1_spl
| or(X0,X0) = not(not(X0)) ),
inference(forward_demodulation,[status(thm)],[f700,f832]) ).
fof(f880,plain,
! [X0,X1] :
( ~ sQ25_spl
| ~ sQ65_spl
| ~ sQ92_spl
| ~ sQ20_spl
| ~ sQ59_spl
| ~ sQ5_spl
| ~ sQ1_spl
| ~ sQ90_spl
| strict_implies(or(X0,X0),X1) = necessarily(or(not(X0),X1)) ),
inference(paramodulation,[status(thm)],[f842,f525]) ).
fof(f883,plain,
! [X0,X1] :
( ~ sQ25_spl
| ~ sQ65_spl
| ~ sQ92_spl
| ~ sQ20_spl
| ~ sQ59_spl
| ~ sQ5_spl
| ~ sQ1_spl
| ~ sQ90_spl
| strict_implies(or(X0,X0),X1) = strict_implies(not(not(X0)),X1) ),
inference(forward_demodulation,[status(thm)],[f705,f880]) ).
fof(f959,plain,
! [X0,X1] :
( ~ sQ25_spl
| ~ sQ92_spl
| ~ sQ56_spl
| ~ sQ20_spl
| strict_equiv(X0,X1) = strict_equiv(X1,X0) ),
inference(resolution,[status(thm)],[f808,f287]) ).
fof(f1007,plain,
! [X0,X1] :
( ~ sQ25_spl
| ~ sQ56_spl
| ~ sQ92_spl
| ~ sQ20_spl
| and(X0,X1) = and(X1,X0) ),
inference(resolution,[status(thm)],[f810,f287]) ).
fof(f1043,plain,
! [X0,X1] :
( ~ sQ25_spl
| ~ sQ56_spl
| ~ sQ92_spl
| ~ sQ20_spl
| ~ sQ5_spl
| implies(X0,X1) = not(and(not(X1),X0)) ),
inference(paramodulation,[status(thm)],[f1007,f213]) ).
fof(f1054,plain,
! [X0,X1] :
( ~ sQ25_spl
| ~ sQ56_spl
| ~ sQ92_spl
| ~ sQ20_spl
| ~ sQ59_spl
| is_a_theorem(strict_implies(and(X0,X1),X1)) ),
inference(paramodulation,[status(thm)],[f1007,f412]) ).
fof(f1228,plain,
! [X0,X1,X2] :
( ~ sQ20_spl
| ~ sQ15_spl
| ~ sQ68_spl
| ~ is_a_theorem(strict_implies(X2,X1))
| ~ is_a_theorem(strict_implies(X0,X2))
| is_a_theorem(strict_implies(X0,X1)) ),
inference(resolution,[status(thm)],[f733,f268]) ).
fof(f1254,plain,
! [X0,X1] :
( ~ sQ5_spl
| ~ sQ25_spl
| ~ sQ56_spl
| ~ sQ92_spl
| ~ sQ20_spl
| implies(not(X0),X1) = implies(not(X1),X0) ),
inference(paramodulation,[status(thm)],[f213,f1043]) ).
fof(f1281,plain,
! [X0,X1] :
( ~ sQ5_spl
| ~ sQ25_spl
| ~ sQ56_spl
| ~ sQ92_spl
| ~ sQ20_spl
| ~ sQ1_spl
| or(X0,X1) = implies(not(X1),X0) ),
inference(forward_demodulation,[status(thm)],[f700,f1254]) ).
fof(f1282,plain,
! [X0,X1] :
( ~ sQ5_spl
| ~ sQ25_spl
| ~ sQ56_spl
| ~ sQ92_spl
| ~ sQ20_spl
| ~ sQ1_spl
| or(X0,X1) = or(X1,X0) ),
inference(forward_demodulation,[status(thm)],[f700,f1281]) ).
fof(f1307,plain,
! [X0,X1] :
( ~ sQ5_spl
| ~ sQ25_spl
| ~ sQ56_spl
| ~ sQ92_spl
| ~ sQ20_spl
| ~ sQ1_spl
| ~ sQ90_spl
| strict_implies(not(X0),X1) = necessarily(or(X1,X0)) ),
inference(paramodulation,[status(thm)],[f1282,f705]) ).
fof(f1314,plain,
! [X0,X1] :
( ~ sQ5_spl
| ~ sQ25_spl
| ~ sQ56_spl
| ~ sQ92_spl
| ~ sQ20_spl
| ~ sQ1_spl
| ~ sQ90_spl
| strict_implies(not(X0),X1) = strict_implies(not(X1),X0) ),
inference(forward_demodulation,[status(thm)],[f705,f1307]) ).
fof(f1341,plain,
! [X0] :
( ~ sQ5_spl
| ~ sQ25_spl
| ~ sQ56_spl
| ~ sQ92_spl
| ~ sQ20_spl
| ~ sQ1_spl
| ~ sQ90_spl
| ~ sQ15_spl
| ~ sQ68_spl
| ~ sQ65_spl
| ~ sQ59_spl
| is_a_theorem(strict_implies(not(not(X0)),X0)) ),
inference(paramodulation,[status(thm)],[f1314,f812]) ).
fof(f1374,plain,
! [X0] :
( ~ sQ25_spl
| ~ sQ65_spl
| ~ sQ92_spl
| ~ sQ20_spl
| ~ sQ59_spl
| ~ sQ5_spl
| ~ sQ1_spl
| ~ sQ56_spl
| ~ sQ90_spl
| ~ sQ15_spl
| ~ sQ68_spl
| is_a_theorem(strict_implies(or(X0,X0),X0)) ),
inference(paramodulation,[status(thm)],[f843,f1341]) ).
fof(f1375,plain,
! [X0] :
( ~ sQ25_spl
| ~ sQ65_spl
| ~ sQ92_spl
| ~ sQ20_spl
| ~ sQ59_spl
| ~ sQ5_spl
| ~ sQ1_spl
| ~ sQ56_spl
| ~ sQ90_spl
| ~ sQ15_spl
| ~ sQ68_spl
| is_a_theorem(strict_implies(not(or(X0,X0)),not(X0))) ),
inference(paramodulation,[status(thm)],[f843,f1341]) ).
fof(f1680,plain,
! [X0] :
( ~ sQ25_spl
| ~ sQ65_spl
| ~ sQ92_spl
| ~ sQ20_spl
| ~ sQ59_spl
| ~ sQ5_spl
| ~ sQ1_spl
| ~ sQ56_spl
| ~ sQ90_spl
| ~ sQ15_spl
| ~ sQ68_spl
| X0 = or(X0,X0)
| ~ is_a_theorem(strict_implies(X0,or(X0,X0))) ),
inference(resolution,[status(thm)],[f805,f1374]) ).
fof(f1701,plain,
! [X0,X1] :
( ~ sQ25_spl
| ~ sQ56_spl
| ~ sQ92_spl
| ~ sQ20_spl
| ~ sQ59_spl
| X0 = and(X1,X0)
| ~ is_a_theorem(strict_implies(X0,and(X1,X0))) ),
inference(resolution,[status(thm)],[f805,f1054]) ).
fof(f1702,plain,
! [X0,X1] :
( ~ sQ59_spl
| ~ sQ25_spl
| ~ sQ92_spl
| ~ sQ20_spl
| X0 = and(X0,X1)
| ~ is_a_theorem(strict_implies(X0,and(X0,X1))) ),
inference(resolution,[status(thm)],[f805,f412]) ).
fof(f2195,plain,
! [X0,X1] :
( ~ sQ25_spl
| ~ sQ56_spl
| ~ sQ92_spl
| ~ sQ20_spl
| ~ sQ59_spl
| X0 = and(X0,X1)
| ~ is_a_theorem(strict_implies(X0,and(X1,X0))) ),
inference(paramodulation,[status(thm)],[f1007,f1702]) ).
fof(f2499,plain,
! [X0,X1] :
( ~ sQ25_spl
| ~ sQ56_spl
| ~ sQ92_spl
| ~ sQ20_spl
| ~ sQ59_spl
| ~ sQ65_spl
| ~ sQ62_spl
| and(X0,X1) = and(and(X0,X1),X0) ),
inference(resolution,[status(thm)],[f834,f2195]) ).
fof(f2500,plain,
! [X0,X1] :
( ~ sQ25_spl
| ~ sQ56_spl
| ~ sQ92_spl
| ~ sQ20_spl
| ~ sQ59_spl
| ~ sQ65_spl
| ~ sQ62_spl
| and(X0,X1) = and(X0,and(X0,X1)) ),
inference(resolution,[status(thm)],[f834,f1701]) ).
fof(f2562,plain,
! [X0,X1] :
( ~ sQ25_spl
| ~ sQ56_spl
| ~ sQ92_spl
| ~ sQ20_spl
| ~ sQ59_spl
| ~ sQ65_spl
| ~ sQ62_spl
| ~ sQ5_spl
| implies(and(not(X0),X1),X0) = not(and(not(X0),X1)) ),
inference(paramodulation,[status(thm)],[f2499,f213]) ).
fof(f2592,plain,
! [X0,X1] :
( ~ sQ25_spl
| ~ sQ56_spl
| ~ sQ92_spl
| ~ sQ20_spl
| ~ sQ59_spl
| ~ sQ65_spl
| ~ sQ62_spl
| ~ sQ5_spl
| implies(and(not(X0),X1),X0) = implies(X1,X0) ),
inference(forward_demodulation,[status(thm)],[f1043,f2562]) ).
fof(f2608,plain,
! [X0,X1] :
( ~ sQ25_spl
| ~ sQ56_spl
| ~ sQ92_spl
| ~ sQ20_spl
| ~ sQ59_spl
| ~ sQ65_spl
| ~ sQ62_spl
| and(X0,X1) = and(X0,and(X1,X0)) ),
inference(paramodulation,[status(thm)],[f1007,f2500]) ).
fof(f4205,plain,
! [X0,X1] :
( ~ sQ25_spl
| ~ sQ56_spl
| ~ sQ92_spl
| ~ sQ20_spl
| ~ sQ59_spl
| ~ sQ65_spl
| ~ sQ62_spl
| ~ sQ5_spl
| ~ sQ90_spl
| strict_implies(and(not(X0),X1),X0) = necessarily(implies(X1,X0)) ),
inference(paramodulation,[status(thm)],[f2592,f525]) ).
fof(f4237,plain,
! [X0,X1] :
( ~ sQ25_spl
| ~ sQ56_spl
| ~ sQ92_spl
| ~ sQ20_spl
| ~ sQ59_spl
| ~ sQ65_spl
| ~ sQ62_spl
| ~ sQ5_spl
| ~ sQ90_spl
| strict_implies(and(not(X0),X1),X0) = strict_implies(X1,X0) ),
inference(forward_demodulation,[status(thm)],[f525,f4205]) ).
fof(f4238,plain,
! [X0,X1] :
( ~ sQ25_spl
| ~ sQ56_spl
| ~ sQ92_spl
| ~ sQ20_spl
| ~ sQ59_spl
| ~ sQ65_spl
| ~ sQ62_spl
| ~ sQ5_spl
| ~ sQ90_spl
| strict_implies(and(not(X0),X1),X0) = strict_implies(and(X1,not(X0)),X0) ),
inference(paramodulation,[status(thm)],[f2608,f4237]) ).
fof(f4291,plain,
! [X0,X1] :
( ~ sQ25_spl
| ~ sQ56_spl
| ~ sQ92_spl
| ~ sQ20_spl
| ~ sQ59_spl
| ~ sQ65_spl
| ~ sQ62_spl
| ~ sQ5_spl
| ~ sQ90_spl
| strict_implies(X0,X1) = strict_implies(and(X0,not(X1)),X1) ),
inference(forward_demodulation,[status(thm)],[f4237,f4238]) ).
fof(f6162,plain,
! [X0] :
( ~ sQ25_spl
| ~ sQ65_spl
| ~ sQ92_spl
| ~ sQ20_spl
| ~ sQ59_spl
| ~ sQ5_spl
| ~ sQ1_spl
| ~ sQ90_spl
| ~ sQ15_spl
| ~ sQ68_spl
| ~ sQ56_spl
| is_a_theorem(strict_implies(not(not(X0)),or(X0,X0))) ),
inference(paramodulation,[status(thm)],[f883,f812]) ).
fof(f6213,plain,
! [X0] :
( ~ sQ25_spl
| ~ sQ65_spl
| ~ sQ92_spl
| ~ sQ20_spl
| ~ sQ59_spl
| ~ sQ5_spl
| ~ sQ1_spl
| ~ sQ90_spl
| ~ sQ15_spl
| ~ sQ68_spl
| ~ sQ56_spl
| is_a_theorem(strict_implies(or(X0,X0),not(not(X0)))) ),
inference(paramodulation,[status(thm)],[f883,f812]) ).
fof(f6291,plain,
! [X0] :
( ~ sQ92_spl
| ~ sQ20_spl
| ~ sQ25_spl
| ~ sQ65_spl
| ~ sQ59_spl
| ~ sQ5_spl
| ~ sQ1_spl
| ~ sQ90_spl
| ~ sQ15_spl
| ~ sQ68_spl
| ~ sQ56_spl
| is_a_theorem(strict_equiv(not(not(X0)),or(X0,X0)))
| ~ is_a_theorem(strict_implies(not(not(X0)),or(X0,X0))) ),
inference(resolution,[status(thm)],[f6213,f592]) ).
fof(f6320,plain,
! [X0] :
( ~ sQ92_spl
| ~ sQ20_spl
| ~ sQ25_spl
| ~ sQ65_spl
| ~ sQ59_spl
| ~ sQ5_spl
| ~ sQ1_spl
| ~ sQ90_spl
| ~ sQ15_spl
| ~ sQ68_spl
| ~ sQ56_spl
| is_a_theorem(strict_equiv(not(not(X0)),or(X0,X0))) ),
inference(forward_subsumption_resolution,[status(thm)],[f6291,f6162]) ).
fof(f6989,plain,
! [X0] :
( ~ sQ25_spl
| ~ sQ92_spl
| ~ sQ56_spl
| ~ sQ20_spl
| ~ sQ65_spl
| ~ sQ59_spl
| ~ sQ5_spl
| ~ sQ1_spl
| ~ sQ90_spl
| ~ sQ15_spl
| ~ sQ68_spl
| is_a_theorem(strict_equiv(or(X0,X0),not(not(X0)))) ),
inference(paramodulation,[status(thm)],[f959,f6320]) ).
fof(f8397,plain,
! [X0,X1,X2] :
( ~ sQ25_spl
| ~ sQ56_spl
| ~ sQ92_spl
| ~ sQ20_spl
| ~ sQ59_spl
| ~ sQ15_spl
| ~ sQ68_spl
| ~ is_a_theorem(strict_implies(X1,X2))
| is_a_theorem(strict_implies(and(X0,X1),X2)) ),
inference(resolution,[status(thm)],[f1228,f1054]) ).
fof(f8402,plain,
! [X0,X1] :
( ~ sQ25_spl
| ~ sQ65_spl
| ~ sQ92_spl
| ~ sQ20_spl
| ~ sQ59_spl
| ~ sQ5_spl
| ~ sQ1_spl
| ~ sQ56_spl
| ~ sQ90_spl
| ~ sQ15_spl
| ~ sQ68_spl
| ~ is_a_theorem(strict_implies(X0,or(X1,X1)))
| is_a_theorem(strict_implies(X0,X1)) ),
inference(resolution,[status(thm)],[f1228,f1374]) ).
fof(f8931,plain,
( ~ sQ25_spl
| ~ sQ92_spl
| ~ sQ56_spl
| ~ sQ20_spl
| ~ sQ65_spl
| ~ sQ59_spl
| ~ sQ5_spl
| ~ sQ1_spl
| ~ sQ90_spl
| ~ sQ15_spl
| ~ sQ68_spl
| ~ sQ94_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f6989,f621]) ).
fof(f8974,plain,
( ~ sQ25_spl
| ~ sQ92_spl
| ~ sQ56_spl
| ~ sQ20_spl
| ~ sQ65_spl
| ~ sQ59_spl
| ~ sQ5_spl
| ~ sQ1_spl
| ~ sQ90_spl
| ~ sQ15_spl
| ~ sQ68_spl
| ~ sQ94_spl ),
inference(contradiction_clause,[status(thm)],[f8931]) ).
fof(f14223,plain,
! [X0,X1] :
( ~ sQ25_spl
| ~ sQ56_spl
| ~ sQ92_spl
| ~ sQ20_spl
| ~ sQ59_spl
| ~ sQ65_spl
| ~ sQ62_spl
| ~ sQ5_spl
| ~ sQ90_spl
| ~ sQ15_spl
| ~ sQ68_spl
| ~ is_a_theorem(strict_implies(not(X1),X1))
| is_a_theorem(strict_implies(X0,X1)) ),
inference(paramodulation,[status(thm)],[f4291,f8397]) ).
fof(f14315,plain,
! [X0] :
( ~ sQ5_spl
| ~ sQ25_spl
| ~ sQ56_spl
| ~ sQ92_spl
| ~ sQ20_spl
| ~ sQ1_spl
| ~ sQ90_spl
| ~ sQ15_spl
| ~ sQ68_spl
| ~ sQ65_spl
| ~ sQ59_spl
| is_a_theorem(strict_implies(not(not(or(X0,X0))),X0)) ),
inference(resolution,[status(thm)],[f8402,f1341]) ).
fof(f14592,plain,
! [X0] :
( ~ sQ5_spl
| ~ sQ25_spl
| ~ sQ56_spl
| ~ sQ92_spl
| ~ sQ20_spl
| ~ sQ1_spl
| ~ sQ90_spl
| ~ sQ15_spl
| ~ sQ68_spl
| ~ sQ65_spl
| ~ sQ59_spl
| is_a_theorem(strict_implies(not(X0),not(or(X0,X0)))) ),
inference(paramodulation,[status(thm)],[f1314,f14315]) ).
fof(f14754,plain,
! [X0] :
( ~ sQ25_spl
| ~ sQ92_spl
| ~ sQ20_spl
| ~ sQ5_spl
| ~ sQ56_spl
| ~ sQ1_spl
| ~ sQ90_spl
| ~ sQ15_spl
| ~ sQ68_spl
| ~ sQ65_spl
| ~ sQ59_spl
| not(or(X0,X0)) = not(X0)
| ~ is_a_theorem(strict_implies(not(or(X0,X0)),not(X0))) ),
inference(resolution,[status(thm)],[f14592,f805]) ).
fof(f14793,plain,
! [X0] :
( ~ sQ25_spl
| ~ sQ92_spl
| ~ sQ20_spl
| ~ sQ5_spl
| ~ sQ56_spl
| ~ sQ1_spl
| ~ sQ90_spl
| ~ sQ15_spl
| ~ sQ68_spl
| ~ sQ65_spl
| ~ sQ59_spl
| not(or(X0,X0)) = not(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f14754,f1375]) ).
fof(f14913,plain,
! [X0,X1] :
( ~ sQ25_spl
| ~ sQ92_spl
| ~ sQ20_spl
| ~ sQ5_spl
| ~ sQ56_spl
| ~ sQ1_spl
| ~ sQ90_spl
| ~ sQ15_spl
| ~ sQ68_spl
| ~ sQ65_spl
| ~ sQ59_spl
| implies(X0,or(X1,X1)) = not(and(not(X1),X0)) ),
inference(paramodulation,[status(thm)],[f14793,f1043]) ).
fof(f14977,plain,
! [X0,X1] :
( ~ sQ25_spl
| ~ sQ92_spl
| ~ sQ20_spl
| ~ sQ5_spl
| ~ sQ56_spl
| ~ sQ1_spl
| ~ sQ90_spl
| ~ sQ15_spl
| ~ sQ68_spl
| ~ sQ65_spl
| ~ sQ59_spl
| implies(X0,or(X1,X1)) = implies(X0,X1) ),
inference(forward_demodulation,[status(thm)],[f1043,f14913]) ).
fof(f16083,plain,
! [X0,X1] :
( ~ sQ25_spl
| ~ sQ92_spl
| ~ sQ20_spl
| ~ sQ5_spl
| ~ sQ56_spl
| ~ sQ1_spl
| ~ sQ90_spl
| ~ sQ15_spl
| ~ sQ68_spl
| ~ sQ65_spl
| ~ sQ59_spl
| strict_implies(X0,or(X1,X1)) = necessarily(implies(X0,X1)) ),
inference(paramodulation,[status(thm)],[f14977,f525]) ).
fof(f16149,plain,
! [X0,X1] :
( ~ sQ25_spl
| ~ sQ92_spl
| ~ sQ20_spl
| ~ sQ5_spl
| ~ sQ56_spl
| ~ sQ1_spl
| ~ sQ90_spl
| ~ sQ15_spl
| ~ sQ68_spl
| ~ sQ65_spl
| ~ sQ59_spl
| strict_implies(X0,or(X1,X1)) = strict_implies(X0,X1) ),
inference(forward_demodulation,[status(thm)],[f525,f16083]) ).
fof(f16152,plain,
! [X0] :
( ~ sQ25_spl
| ~ sQ65_spl
| ~ sQ92_spl
| ~ sQ20_spl
| ~ sQ59_spl
| ~ sQ5_spl
| ~ sQ1_spl
| ~ sQ56_spl
| ~ sQ90_spl
| ~ sQ15_spl
| ~ sQ68_spl
| X0 = or(X0,X0)
| ~ is_a_theorem(strict_implies(X0,X0)) ),
inference(backward_demodulation,[status(thm)],[f16149,f1680]) ).
fof(f16249,plain,
! [X0] :
( ~ sQ25_spl
| ~ sQ65_spl
| ~ sQ92_spl
| ~ sQ20_spl
| ~ sQ59_spl
| ~ sQ5_spl
| ~ sQ1_spl
| ~ sQ56_spl
| ~ sQ90_spl
| ~ sQ15_spl
| ~ sQ68_spl
| X0 = or(X0,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f16152,f812]) ).
fof(f16386,plain,
! [X0] :
( ~ sQ25_spl
| ~ sQ65_spl
| ~ sQ92_spl
| ~ sQ20_spl
| ~ sQ59_spl
| ~ sQ5_spl
| ~ sQ1_spl
| ~ sQ56_spl
| ~ sQ90_spl
| ~ sQ15_spl
| ~ sQ68_spl
| strict_implies(not(X0),X0) = necessarily(X0) ),
inference(paramodulation,[status(thm)],[f16249,f705]) ).
fof(f16393,plain,
! [X0,X1] :
( ~ sQ25_spl
| ~ sQ56_spl
| ~ sQ92_spl
| ~ sQ20_spl
| ~ sQ59_spl
| ~ sQ65_spl
| ~ sQ62_spl
| ~ sQ5_spl
| ~ sQ90_spl
| ~ sQ15_spl
| ~ sQ68_spl
| ~ sQ1_spl
| ~ is_a_theorem(necessarily(X1))
| is_a_theorem(strict_implies(X0,X1)) ),
inference(backward_demodulation,[status(thm)],[f16386,f14223]) ).
fof(f17370,plain,
! [X0,X1] :
( ~ sQ15_spl
| ~ sQ25_spl
| ~ sQ56_spl
| ~ sQ92_spl
| ~ sQ20_spl
| ~ sQ59_spl
| ~ sQ65_spl
| ~ sQ62_spl
| ~ sQ5_spl
| ~ sQ90_spl
| ~ sQ68_spl
| ~ sQ1_spl
| is_a_theorem(X0)
| ~ is_a_theorem(X1)
| ~ is_a_theorem(necessarily(X0)) ),
inference(resolution,[status(thm)],[f16393,f249]) ).
fof(f17376,definition,
! [X0] :
( sQ102_spl
<=> ( is_a_theorem(X0)
| ~ is_a_theorem(necessarily(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ102_spl])],[split_symbol_definition]) ).
fof(f17377,plain,
! [X0] :
( ~ sQ102_spl
| is_a_theorem(X0)
| ~ is_a_theorem(necessarily(X0)) ),
inference(component_clause,[status(thm)],[f17376]) ).
fof(f17379,plain,
( ~ sQ15_spl
| ~ sQ25_spl
| ~ sQ56_spl
| ~ sQ92_spl
| ~ sQ20_spl
| ~ sQ59_spl
| ~ sQ65_spl
| ~ sQ62_spl
| ~ sQ5_spl
| ~ sQ90_spl
| ~ sQ68_spl
| ~ sQ1_spl
| sQ94_spl
| sQ102_spl ),
inference(split_clause,[status(thm)],[f17370,f17376,f620,f198,f444,f524,f212,f422,f433,f411,f267,f531,f400,f286,f248]) ).
fof(f17487,plain,
! [X0,X1] :
( ~ sQ90_spl
| ~ sQ102_spl
| is_a_theorem(implies(X0,X1))
| ~ is_a_theorem(strict_implies(X0,X1)) ),
inference(paramodulation,[status(thm)],[f525,f17377]) ).
fof(f19539,plain,
! [X0] :
( ~ sQ83_spl
| ~ sQ90_spl
| ~ sQ102_spl
| is_a_theorem(implies(possibly(X0),necessarily(possibly(X0)))) ),
inference(resolution,[status(thm)],[f17487,f500]) ).
fof(f19578,plain,
( ~ sQ83_spl
| ~ sQ90_spl
| ~ sQ102_spl
| sQ41_spl ),
inference(split_clause,[status(thm)],[f19539,f345,f17376,f524,f499]) ).
fof(f19588,plain,
( ~ sQ40_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f343,f194]) ).
fof(f19589,plain,
~ sQ40_spl,
inference(contradiction_clause,[status(thm)],[f19588]) ).
fof(f19590,plain,
$false,
inference(sat_refutation,[status(thm)],[f201,f215,f251,f270,f289,f352,f403,f414,f425,f436,f447,f502,f527,f534,f536,f538,f540,f542,f544,f550,f552,f556,f571,f576,f601,f607,f611,f679,f8974,f17379,f19578,f19589]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL573+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/0.37 % Computer : n026.cluster.edu
% 0.12/0.37 % Model : x86_64 x86_64
% 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.37 % Memory : 8046.5625MB
% 0.12/0.37 % OS : Linux 6.8.0-71-generic
% 0.12/0.37 % CPULimit : 300
% 0.12/0.37 % WCLimit : 300
% 0.12/0.37 % DateTime : Mon Sep 21 00:42:36 UTC 2026
% 0.12/0.37 % CPUTime :
% 0.12/0.38 % Drodi V4.1.1
% 40.69/5.62 % Refutation found
% 40.69/5.62 % SZS status Theorem for theBenchmark: Theorem is valid
% 40.69/5.62 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 13.12/5.75 % Elapsed time: 5.363057 seconds
% 13.12/5.75 % CPU time: 42.125426 seconds
% 13.12/5.75 % Total memory used: 580.160 MB
% 13.12/5.75 % Net memory used: 559.288 MB
%------------------------------------------------------------------------------