%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : LCL533+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n002.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 : Tue Sep 29 11:58:53 AM UTC 2026
% Result : Theorem 1.08s 0.59s
% Output : Refutation 1.08s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 48
% Syntax : Number of formulae : 206 ( 70 unt; 24 def)
% Number of atoms : 469 ( 26 equ)
% Maximal formula atoms : 13 ( 2 avg)
% Number of connectives : 489 ( 226 ~; 213 |; 2 &)
% ( 32 <=>; 16 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 4 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 39 ( 37 usr; 37 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 1 con; 0-2 aty)
% Number of variables : 174 ( 0 sgn 173 !; 1 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
( modus_ponens
<=> ! [X0,X1] :
( ( is_a_theorem(X0)
& is_a_theorem(implies(X0,X1)) )
=> is_a_theorem(X1) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/LCL006+0.ax',modus_ponens) ).
fof(f3,axiom,
( modus_tollens
<=> ! [X0,X1] : is_a_theorem(implies(implies(not(X1),not(X0)),implies(X0,X1))) ),
file('/export/starexec/sandbox2/benchmark/Axioms/LCL006+0.ax',modus_tollens) ).
fof(f6,axiom,
( implies_3
<=> ! [X0,X1,X2] : is_a_theorem(implies(implies(X0,X1),implies(implies(X1,X2),implies(X0,X2)))) ),
file('/export/starexec/sandbox2/benchmark/Axioms/LCL006+0.ax',implies_3) ).
fof(f8,axiom,
( and_2
<=> ! [X0,X1] : is_a_theorem(implies(and(X0,X1),X1)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/LCL006+0.ax',and_2) ).
fof(f12,axiom,
( or_3
<=> ! [X0,X1,X2] : is_a_theorem(implies(implies(X0,X2),implies(implies(X1,X2),implies(or(X0,X1),X2)))) ),
file('/export/starexec/sandbox2/benchmark/Axioms/LCL006+0.ax',or_3) ).
fof(f27,axiom,
( op_or
=> ! [X0,X1] : or(X0,X1) = not(and(not(X0),not(X1))) ),
file('/export/starexec/sandbox2/benchmark/Axioms/LCL006+1.ax',op_or) ).
fof(f29,axiom,
( op_implies_and
=> ! [X0,X1] : implies(X0,X1) = not(and(X0,not(X1))) ),
file('/export/starexec/sandbox2/benchmark/Axioms/LCL006+1.ax',op_implies_and) ).
fof(f32,axiom,
op_or,
file('/export/starexec/sandbox2/benchmark/Axioms/LCL006+2.ax',hilbert_op_or) ).
fof(f33,axiom,
op_implies_and,
file('/export/starexec/sandbox2/benchmark/Axioms/LCL006+2.ax',hilbert_op_implies_and) ).
fof(f35,axiom,
modus_ponens,
file('/export/starexec/sandbox2/benchmark/Axioms/LCL006+2.ax',hilbert_modus_ponens) ).
fof(f36,axiom,
modus_tollens,
file('/export/starexec/sandbox2/benchmark/Axioms/LCL006+2.ax',hilbert_modus_tollens) ).
fof(f39,axiom,
implies_3,
file('/export/starexec/sandbox2/benchmark/Axioms/LCL006+2.ax',hilbert_implies_3) ).
fof(f41,axiom,
and_2,
file('/export/starexec/sandbox2/benchmark/Axioms/LCL006+2.ax',hilbert_and_2) ).
fof(f45,axiom,
or_3,
file('/export/starexec/sandbox2/benchmark/Axioms/LCL006+2.ax',hilbert_or_3) ).
fof(f50,axiom,
( necessitation
<=> ! [X0] :
( is_a_theorem(X0)
=> is_a_theorem(necessarily(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/LCL007+0.ax',necessitation) ).
fof(f55,axiom,
( axiom_M
<=> ! [X0] : is_a_theorem(implies(necessarily(X0),X0)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/LCL007+0.ax',axiom_M) ).
fof(f68,axiom,
( axiom_m6
<=> ! [X0] : is_a_theorem(strict_implies(X0,possibly(X0))) ),
file('/export/starexec/sandbox2/benchmark/Axioms/LCL007+0.ax',axiom_m6) ).
fof(f73,axiom,
( op_possibly
=> ! [X0] : possibly(X0) = not(necessarily(not(X0))) ),
file('/export/starexec/sandbox2/benchmark/Axioms/LCL007+1.ax',op_possibly) ).
fof(f75,axiom,
( op_strict_implies
=> ! [X0,X1] : strict_implies(X0,X1) = necessarily(implies(X0,X1)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/LCL007+1.ax',op_strict_implies) ).
fof(f77,axiom,
op_possibly,
file('/export/starexec/sandbox2/benchmark/Axioms/LCL007+2.ax',km5_op_possibly) ).
fof(f78,axiom,
necessitation,
file('/export/starexec/sandbox2/benchmark/Axioms/LCL007+2.ax',km5_necessitation) ).
fof(f80,axiom,
axiom_M,
file('/export/starexec/sandbox2/benchmark/Axioms/LCL007+2.ax',km5_axiom_M) ).
fof(f85,axiom,
op_strict_implies,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s1_0_op_strict_implies) ).
fof(f88,conjecture,
axiom_m6,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',s1_0_m6s3m9b_axiom_m6) ).
fof(f89,negated_conjecture,
~ axiom_m6,
inference(negated_conjecture,[status(cth)],[f88]) ).
fof(f90,plain,
~ axiom_m6,
inference(flattening,[],[f89]) ).
fof(f91,plain,
( ! [X0] : is_a_theorem(strict_implies(X0,possibly(X0)))
=> axiom_m6 ),
inference(unused_predicate_definition_removal,[],[f68]) ).
fof(f93,plain,
( axiom_M
=> ! [X0] : is_a_theorem(implies(necessarily(X0),X0)) ),
inference(unused_predicate_definition_removal,[],[f55]) ).
fof(f95,plain,
( necessitation
=> ! [X0] :
( is_a_theorem(X0)
=> is_a_theorem(necessarily(X0)) ) ),
inference(unused_predicate_definition_removal,[],[f50]) ).
fof(f99,plain,
( or_3
=> ! [X0,X1,X2] : is_a_theorem(implies(implies(X0,X2),implies(implies(X1,X2),implies(or(X0,X1),X2)))) ),
inference(unused_predicate_definition_removal,[],[f12]) ).
fof(f103,plain,
( and_2
=> ! [X0,X1] : is_a_theorem(implies(and(X0,X1),X1)) ),
inference(unused_predicate_definition_removal,[],[f8]) ).
fof(f105,plain,
( implies_3
=> ! [X0,X1,X2] : is_a_theorem(implies(implies(X0,X1),implies(implies(X1,X2),implies(X0,X2)))) ),
inference(unused_predicate_definition_removal,[],[f6]) ).
fof(f108,plain,
( modus_tollens
=> ! [X0,X1] : is_a_theorem(implies(implies(not(X1),not(X0)),implies(X0,X1))) ),
inference(unused_predicate_definition_removal,[],[f3]) ).
fof(f110,plain,
( modus_ponens
=> ! [X0,X1] :
( ( is_a_theorem(X0)
& is_a_theorem(implies(X0,X1)) )
=> is_a_theorem(X1) ) ),
inference(unused_predicate_definition_removal,[],[f1]) ).
fof(f115,plain,
( ! [X0,X1] :
( is_a_theorem(X1)
| ~ is_a_theorem(X0)
| ~ is_a_theorem(implies(X0,X1)) )
| ~ modus_ponens ),
inference(ennf_transformation,[],[f110]) ).
fof(f116,plain,
( ! [X0,X1] :
( is_a_theorem(X1)
| ~ is_a_theorem(X0)
| ~ is_a_theorem(implies(X0,X1)) )
| ~ modus_ponens ),
inference(flattening,[],[f115]) ).
fof(f118,plain,
( ! [X0,X1] : is_a_theorem(implies(implies(not(X1),not(X0)),implies(X0,X1)))
| ~ modus_tollens ),
inference(ennf_transformation,[],[f108]) ).
fof(f121,plain,
( ! [X0,X1,X2] : is_a_theorem(implies(implies(X0,X1),implies(implies(X1,X2),implies(X0,X2))))
| ~ implies_3 ),
inference(ennf_transformation,[],[f105]) ).
fof(f123,plain,
( ! [X0,X1] : is_a_theorem(implies(and(X0,X1),X1))
| ~ and_2 ),
inference(ennf_transformation,[],[f103]) ).
fof(f127,plain,
( ! [X0,X1,X2] : is_a_theorem(implies(implies(X0,X2),implies(implies(X1,X2),implies(or(X0,X1),X2))))
| ~ or_3 ),
inference(ennf_transformation,[],[f99]) ).
fof(f131,plain,
( ! [X0,X1] : or(X0,X1) = not(and(not(X0),not(X1)))
| ~ op_or ),
inference(ennf_transformation,[],[f27]) ).
fof(f132,plain,
( ! [X0,X1] : implies(X0,X1) = not(and(X0,not(X1)))
| ~ op_implies_and ),
inference(ennf_transformation,[],[f29]) ).
fof(f134,plain,
( ! [X0] :
( is_a_theorem(necessarily(X0))
| ~ is_a_theorem(X0) )
| ~ necessitation ),
inference(ennf_transformation,[],[f95]) ).
fof(f136,plain,
( ! [X0] : is_a_theorem(implies(necessarily(X0),X0))
| ~ axiom_M ),
inference(ennf_transformation,[],[f93]) ).
fof(f138,plain,
( axiom_m6
| ? [X0] : ~ is_a_theorem(strict_implies(X0,possibly(X0))) ),
inference(ennf_transformation,[],[f91]) ).
fof(f139,plain,
( ! [X0] : possibly(X0) = not(necessarily(not(X0)))
| ~ op_possibly ),
inference(ennf_transformation,[],[f73]) ).
fof(f140,plain,
( ! [X0,X1] : strict_implies(X0,X1) = necessarily(implies(X0,X1))
| ~ op_strict_implies ),
inference(ennf_transformation,[],[f75]) ).
fof(f142,plain,
! [X0,X1] :
( ~ modus_ponens
| ~ is_a_theorem(implies(X0,X1))
| ~ is_a_theorem(X0)
| is_a_theorem(X1) ),
inference(cnf_transformation,[],[f116]) ).
fof(f144,plain,
! [X0,X1] :
( ~ modus_tollens
| is_a_theorem(implies(implies(not(X1),not(X0)),implies(X0,X1))) ),
inference(cnf_transformation,[],[f118]) ).
fof(f147,plain,
! [X2,X0,X1] :
( ~ implies_3
| is_a_theorem(implies(implies(X0,X1),implies(implies(X1,X2),implies(X0,X2)))) ),
inference(cnf_transformation,[],[f121]) ).
fof(f149,plain,
! [X0,X1] :
( ~ and_2
| is_a_theorem(implies(and(X0,X1),X1)) ),
inference(cnf_transformation,[],[f123]) ).
fof(f153,plain,
! [X2,X0,X1] :
( ~ or_3
| is_a_theorem(implies(implies(X0,X2),implies(implies(X1,X2),implies(or(X0,X1),X2)))) ),
inference(cnf_transformation,[],[f127]) ).
fof(f157,plain,
! [X0,X1] :
( ~ op_or
| or(X0,X1) = not(and(not(X0),not(X1))) ),
inference(cnf_transformation,[],[f131]) ).
fof(f158,plain,
! [X0,X1] :
( ~ op_implies_and
| implies(X0,X1) = not(and(X0,not(X1))) ),
inference(cnf_transformation,[],[f132]) ).
fof(f160,plain,
op_or,
inference(cnf_transformation,[],[f32]) ).
fof(f161,plain,
op_implies_and,
inference(cnf_transformation,[],[f33]) ).
fof(f163,plain,
modus_ponens,
inference(cnf_transformation,[],[f35]) ).
fof(f164,plain,
modus_tollens,
inference(cnf_transformation,[],[f36]) ).
fof(f167,plain,
implies_3,
inference(cnf_transformation,[],[f39]) ).
fof(f169,plain,
and_2,
inference(cnf_transformation,[],[f41]) ).
fof(f173,plain,
or_3,
inference(cnf_transformation,[],[f45]) ).
fof(f178,plain,
! [X0] :
( ~ necessitation
| ~ is_a_theorem(X0)
| is_a_theorem(necessarily(X0)) ),
inference(cnf_transformation,[],[f134]) ).
fof(f180,plain,
! [X0] :
( ~ axiom_M
| is_a_theorem(implies(necessarily(X0),X0)) ),
inference(cnf_transformation,[],[f136]) ).
fof(f182,plain,
( ~ is_a_theorem(strict_implies(sK0,possibly(sK0)))
| axiom_m6 ),
inference(cnf_transformation,[],[f138]) ).
fof(f183,plain,
! [X0] :
( ~ op_possibly
| possibly(X0) = not(necessarily(not(X0))) ),
inference(cnf_transformation,[],[f139]) ).
fof(f184,plain,
! [X0,X1] :
( ~ op_strict_implies
| strict_implies(X0,X1) = necessarily(implies(X0,X1)) ),
inference(cnf_transformation,[],[f140]) ).
fof(f186,plain,
op_possibly,
inference(cnf_transformation,[],[f77]) ).
fof(f187,plain,
necessitation,
inference(cnf_transformation,[],[f78]) ).
fof(f189,plain,
axiom_M,
inference(cnf_transformation,[],[f80]) ).
fof(f193,plain,
op_strict_implies,
inference(cnf_transformation,[],[f85]) ).
fof(f196,plain,
~ axiom_m6,
inference(cnf_transformation,[],[f90]) ).
fof(f197,plain,
! [X0,X1] :
( ~ modus_ponens
| is_a_theorem(implies(X0,X1))
| is_a_theorem(X0)
| ~ is_a_theorem(X1) ),
inference(consistent_polarity_flipping,[],[f142]) ).
fof(f199,plain,
! [X0,X1] :
( modus_tollens
| ~ is_a_theorem(implies(implies(not(X1),not(X0)),implies(X0,X1))) ),
inference(consistent_polarity_flipping,[],[f144]) ).
fof(f202,plain,
! [X2,X0,X1] :
( ~ implies_3
| ~ is_a_theorem(implies(implies(X0,X1),implies(implies(X1,X2),implies(X0,X2)))) ),
inference(consistent_polarity_flipping,[],[f147]) ).
fof(f204,plain,
! [X0,X1] :
( and_2
| ~ is_a_theorem(implies(and(X0,X1),X1)) ),
inference(consistent_polarity_flipping,[],[f149]) ).
fof(f208,plain,
! [X2,X0,X1] :
( or_3
| ~ is_a_theorem(implies(implies(X0,X2),implies(implies(X1,X2),implies(or(X0,X1),X2)))) ),
inference(consistent_polarity_flipping,[],[f153]) ).
fof(f212,plain,
! [X0,X1] :
( op_implies_and
| implies(X0,X1) = not(and(X0,not(X1))) ),
inference(consistent_polarity_flipping,[],[f158]) ).
fof(f213,plain,
~ op_implies_and,
inference(consistent_polarity_flipping,[],[f161]) ).
fof(f214,plain,
~ modus_tollens,
inference(consistent_polarity_flipping,[],[f164]) ).
fof(f217,plain,
~ and_2,
inference(consistent_polarity_flipping,[],[f169]) ).
fof(f221,plain,
~ or_3,
inference(consistent_polarity_flipping,[],[f173]) ).
fof(f224,plain,
! [X0] :
( ~ necessitation
| is_a_theorem(X0)
| ~ is_a_theorem(necessarily(X0)) ),
inference(consistent_polarity_flipping,[],[f178]) ).
fof(f226,plain,
! [X0] :
( ~ axiom_M
| ~ is_a_theorem(implies(necessarily(X0),X0)) ),
inference(consistent_polarity_flipping,[],[f180]) ).
fof(f228,plain,
( is_a_theorem(strict_implies(sK0,possibly(sK0)))
| axiom_m6 ),
inference(consistent_polarity_flipping,[],[f182]) ).
fof(f229,plain,
! [X0] :
( op_possibly
| possibly(X0) = not(necessarily(not(X0))) ),
inference(consistent_polarity_flipping,[],[f183]) ).
fof(f230,plain,
! [X0,X1] :
( op_strict_implies
| strict_implies(X0,X1) = necessarily(implies(X0,X1)) ),
inference(consistent_polarity_flipping,[],[f184]) ).
fof(f231,plain,
~ op_possibly,
inference(consistent_polarity_flipping,[],[f186]) ).
fof(f235,plain,
~ op_strict_implies,
inference(consistent_polarity_flipping,[],[f193]) ).
fof(f245,definition,
( spl1_3
<=> ! [X0,X1] : strict_implies(X0,X1) = necessarily(implies(X0,X1)) ),
introduced(definition,[new_symbols(definition,[spl1_3])],[avatar_definition]) ).
fof(f246,plain,
( ! [X0,X1] : strict_implies(X0,X1) = necessarily(implies(X0,X1))
| ~ spl1_3 ),
inference(avatar_component_clause,[],[f245]) ).
fof(f248,definition,
( spl1_4
<=> op_strict_implies ),
introduced(definition,[new_symbols(definition,[spl1_4])],[avatar_definition]) ).
fof(f251,plain,
( spl1_3
| spl1_4 ),
inference(avatar_split_clause,[],[f230,f248,f245]) ).
fof(f253,definition,
( spl1_5
<=> ! [X0] : possibly(X0) = not(necessarily(not(X0))) ),
introduced(definition,[new_symbols(definition,[spl1_5])],[avatar_definition]) ).
fof(f254,plain,
( ! [X0] : possibly(X0) = not(necessarily(not(X0)))
| ~ spl1_5 ),
inference(avatar_component_clause,[],[f253]) ).
fof(f256,definition,
( spl1_6
<=> op_possibly ),
introduced(definition,[new_symbols(definition,[spl1_6])],[avatar_definition]) ).
fof(f259,plain,
( spl1_5
| spl1_6 ),
inference(avatar_split_clause,[],[f229,f256,f253]) ).
fof(f261,definition,
( spl1_7
<=> axiom_m6 ),
introduced(definition,[new_symbols(definition,[spl1_7])],[avatar_definition]) ).
fof(f265,definition,
( spl1_8
<=> is_a_theorem(strict_implies(sK0,possibly(sK0))) ),
introduced(definition,[new_symbols(definition,[spl1_8])],[avatar_definition]) ).
fof(f267,plain,
( is_a_theorem(strict_implies(sK0,possibly(sK0)))
| ~ spl1_8 ),
inference(avatar_component_clause,[],[f265]) ).
fof(f268,plain,
( spl1_7
| spl1_8 ),
inference(avatar_split_clause,[],[f228,f265,f261]) ).
fof(f278,definition,
( spl1_11
<=> ! [X0] : ~ is_a_theorem(implies(necessarily(X0),X0)) ),
introduced(definition,[new_symbols(definition,[spl1_11])],[avatar_definition]) ).
fof(f279,plain,
( ! [X0] : ~ is_a_theorem(implies(necessarily(X0),X0))
| ~ spl1_11 ),
inference(avatar_component_clause,[],[f278]) ).
fof(f281,definition,
( spl1_12
<=> axiom_M ),
introduced(definition,[new_symbols(definition,[spl1_12])],[avatar_definition]) ).
fof(f284,plain,
( spl1_11
| ~ spl1_12 ),
inference(avatar_split_clause,[],[f226,f281,f278]) ).
fof(f294,definition,
( spl1_15
<=> ! [X0] :
( is_a_theorem(X0)
| ~ is_a_theorem(necessarily(X0)) ) ),
introduced(definition,[new_symbols(definition,[spl1_15])],[avatar_definition]) ).
fof(f295,plain,
( ! [X0] :
( ~ is_a_theorem(necessarily(X0))
| is_a_theorem(X0) )
| ~ spl1_15 ),
inference(avatar_component_clause,[],[f294]) ).
fof(f297,definition,
( spl1_16
<=> necessitation ),
introduced(definition,[new_symbols(definition,[spl1_16])],[avatar_definition]) ).
fof(f300,plain,
( spl1_15
| ~ spl1_16 ),
inference(avatar_split_clause,[],[f224,f297,f294]) ).
fof(f310,definition,
( spl1_19
<=> ! [X0,X1] : implies(X0,X1) = not(and(X0,not(X1))) ),
introduced(definition,[new_symbols(definition,[spl1_19])],[avatar_definition]) ).
fof(f311,plain,
( ! [X0,X1] : implies(X0,X1) = not(and(X0,not(X1)))
| ~ spl1_19 ),
inference(avatar_component_clause,[],[f310]) ).
fof(f313,definition,
( spl1_20
<=> op_implies_and ),
introduced(definition,[new_symbols(definition,[spl1_20])],[avatar_definition]) ).
fof(f316,plain,
( spl1_19
| spl1_20 ),
inference(avatar_split_clause,[],[f212,f313,f310]) ).
fof(f318,definition,
( spl1_21
<=> ! [X0,X1] : or(X0,X1) = not(and(not(X0),not(X1))) ),
introduced(definition,[new_symbols(definition,[spl1_21])],[avatar_definition]) ).
fof(f319,plain,
( ! [X0,X1] : or(X0,X1) = not(and(not(X0),not(X1)))
| ~ spl1_21 ),
inference(avatar_component_clause,[],[f318]) ).
fof(f321,definition,
( spl1_22
<=> op_or ),
introduced(definition,[new_symbols(definition,[spl1_22])],[avatar_definition]) ).
fof(f324,plain,
( spl1_21
| ~ spl1_22 ),
inference(avatar_split_clause,[],[f157,f321,f318]) ).
fof(f350,definition,
( spl1_29
<=> ! [X2,X0,X1] : ~ is_a_theorem(implies(implies(X0,X2),implies(implies(X1,X2),implies(or(X0,X1),X2)))) ),
introduced(definition,[new_symbols(definition,[spl1_29])],[avatar_definition]) ).
fof(f351,plain,
( ! [X2,X0,X1] : ~ is_a_theorem(implies(implies(X0,X2),implies(implies(X1,X2),implies(or(X0,X1),X2))))
| ~ spl1_29 ),
inference(avatar_component_clause,[],[f350]) ).
fof(f353,definition,
( spl1_30
<=> or_3 ),
introduced(definition,[new_symbols(definition,[spl1_30])],[avatar_definition]) ).
fof(f356,plain,
( spl1_29
| spl1_30 ),
inference(avatar_split_clause,[],[f208,f353,f350]) ).
fof(f382,definition,
( spl1_37
<=> ! [X0,X1] : ~ is_a_theorem(implies(and(X0,X1),X1)) ),
introduced(definition,[new_symbols(definition,[spl1_37])],[avatar_definition]) ).
fof(f383,plain,
( ! [X0,X1] : ~ is_a_theorem(implies(and(X0,X1),X1))
| ~ spl1_37 ),
inference(avatar_component_clause,[],[f382]) ).
fof(f385,definition,
( spl1_38
<=> and_2 ),
introduced(definition,[new_symbols(definition,[spl1_38])],[avatar_definition]) ).
fof(f388,plain,
( spl1_37
| spl1_38 ),
inference(avatar_split_clause,[],[f204,f385,f382]) ).
fof(f398,definition,
( spl1_41
<=> ! [X2,X0,X1] : ~ is_a_theorem(implies(implies(X0,X1),implies(implies(X1,X2),implies(X0,X2)))) ),
introduced(definition,[new_symbols(definition,[spl1_41])],[avatar_definition]) ).
fof(f399,plain,
( ! [X2,X0,X1] : ~ is_a_theorem(implies(implies(X0,X1),implies(implies(X1,X2),implies(X0,X2))))
| ~ spl1_41 ),
inference(avatar_component_clause,[],[f398]) ).
fof(f401,definition,
( spl1_42
<=> implies_3 ),
introduced(definition,[new_symbols(definition,[spl1_42])],[avatar_definition]) ).
fof(f404,plain,
( spl1_41
| ~ spl1_42 ),
inference(avatar_split_clause,[],[f202,f401,f398]) ).
fof(f422,definition,
( spl1_47
<=> ! [X0,X1] : ~ is_a_theorem(implies(implies(not(X1),not(X0)),implies(X0,X1))) ),
introduced(definition,[new_symbols(definition,[spl1_47])],[avatar_definition]) ).
fof(f423,plain,
( ! [X0,X1] : ~ is_a_theorem(implies(implies(not(X1),not(X0)),implies(X0,X1)))
| ~ spl1_47 ),
inference(avatar_component_clause,[],[f422]) ).
fof(f425,definition,
( spl1_48
<=> modus_tollens ),
introduced(definition,[new_symbols(definition,[spl1_48])],[avatar_definition]) ).
fof(f428,plain,
( spl1_47
| spl1_48 ),
inference(avatar_split_clause,[],[f199,f425,f422]) ).
fof(f438,definition,
( spl1_51
<=> ! [X0,X1] :
( is_a_theorem(implies(X0,X1))
| ~ is_a_theorem(X1)
| is_a_theorem(X0) ) ),
introduced(definition,[new_symbols(definition,[spl1_51])],[avatar_definition]) ).
fof(f439,plain,
( ! [X0,X1] :
( is_a_theorem(implies(X0,X1))
| ~ is_a_theorem(X1)
| is_a_theorem(X0) )
| ~ spl1_51 ),
inference(avatar_component_clause,[],[f438]) ).
fof(f441,definition,
( spl1_52
<=> modus_ponens ),
introduced(definition,[new_symbols(definition,[spl1_52])],[avatar_definition]) ).
fof(f444,plain,
( spl1_51
| ~ spl1_52 ),
inference(avatar_split_clause,[],[f197,f441,f438]) ).
fof(f445,plain,
~ spl1_7,
inference(avatar_split_clause,[],[f196,f261]) ).
fof(f446,plain,
spl1_22,
inference(avatar_split_clause,[],[f160,f321]) ).
fof(f448,plain,
spl1_52,
inference(avatar_split_clause,[],[f163,f441]) ).
fof(f450,plain,
spl1_42,
inference(avatar_split_clause,[],[f167,f401]) ).
fof(f453,plain,
spl1_16,
inference(avatar_split_clause,[],[f187,f297]) ).
fof(f454,plain,
spl1_12,
inference(avatar_split_clause,[],[f189,f281]) ).
fof(f456,plain,
~ spl1_20,
inference(avatar_split_clause,[],[f213,f313]) ).
fof(f457,plain,
~ spl1_48,
inference(avatar_split_clause,[],[f214,f425]) ).
fof(f460,plain,
~ spl1_38,
inference(avatar_split_clause,[],[f217,f385]) ).
fof(f464,plain,
~ spl1_30,
inference(avatar_split_clause,[],[f221,f353]) ).
fof(f467,plain,
~ spl1_6,
inference(avatar_split_clause,[],[f231,f256]) ).
fof(f470,plain,
~ spl1_4,
inference(avatar_split_clause,[],[f235,f248]) ).
fof(f472,plain,
( ! [X0,X1] :
( ~ is_a_theorem(strict_implies(X0,X1))
| is_a_theorem(implies(X0,X1)) )
| ~ spl1_3
| ~ spl1_15 ),
inference(superposition,[],[f295,f246]) ).
fof(f491,plain,
( ! [X0,X1] : or(X1,necessarily(not(X0))) = not(and(not(X1),possibly(X0)))
| ~ spl1_5
| ~ spl1_21 ),
inference(superposition,[],[f319,f254]) ).
fof(f494,plain,
( ! [X0,X1] : or(X0,X1) = implies(not(X0),X1)
| ~ spl1_19
| ~ spl1_21 ),
inference(superposition,[],[f319,f311]) ).
fof(f504,plain,
( ! [X0,X1] :
( ~ is_a_theorem(implies(X0,X1))
| is_a_theorem(implies(not(X1),not(X0))) )
| ~ spl1_47
| ~ spl1_51 ),
inference(resolution,[],[f423,f439]) ).
fof(f518,plain,
( is_a_theorem(implies(sK0,possibly(sK0)))
| ~ spl1_3
| ~ spl1_8
| ~ spl1_15 ),
inference(resolution,[],[f472,f267]) ).
fof(f529,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(implies(implies(X0,X1),implies(X2,X1)))
| is_a_theorem(implies(X2,X0)) )
| ~ spl1_41
| ~ spl1_51 ),
inference(resolution,[],[f399,f439]) ).
fof(f530,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(implies(implies(X0,X1),implies(or(X2,X0),X1)))
| is_a_theorem(implies(X2,X1)) )
| ~ spl1_29
| ~ spl1_51 ),
inference(resolution,[],[f351,f439]) ).
fof(f619,plain,
( ! [X0,X1] :
( ~ is_a_theorem(implies(X0,X1))
| is_a_theorem(or(X1,not(X0))) )
| ~ spl1_19
| ~ spl1_21
| ~ spl1_47
| ~ spl1_51 ),
inference(forward_demodulation,[],[f504,f494]) ).
fof(f667,plain,
( ! [X2,X0,X1] : or(and(not(X0),possibly(X1)),X2) = implies(or(X0,necessarily(not(X1))),X2)
| ~ spl1_5
| ~ spl1_19
| ~ spl1_21 ),
inference(superposition,[],[f494,f491]) ).
fof(f780,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(implies(X0,X2))
| is_a_theorem(implies(X0,X1))
| is_a_theorem(implies(X1,X2)) )
| ~ spl1_41
| ~ spl1_51 ),
inference(resolution,[],[f529,f439]) ).
fof(f1035,plain,
( ! [X2,X0,X1] :
( ~ is_a_theorem(implies(or(X0,X2),X1))
| is_a_theorem(implies(X0,X1))
| is_a_theorem(implies(X2,X1)) )
| ~ spl1_29
| ~ spl1_51 ),
inference(resolution,[],[f530,f439]) ).
fof(f2246,plain,
( ! [X0] :
( is_a_theorem(implies(X0,possibly(sK0)))
| is_a_theorem(implies(sK0,X0)) )
| ~ spl1_3
| ~ spl1_8
| ~ spl1_15
| ~ spl1_41
| ~ spl1_51 ),
inference(resolution,[],[f780,f518]) ).
fof(f2274,plain,
( ! [X0] : is_a_theorem(implies(sK0,and(X0,possibly(sK0))))
| ~ spl1_3
| ~ spl1_8
| ~ spl1_15
| ~ spl1_37
| ~ spl1_41
| ~ spl1_51 ),
inference(resolution,[],[f2246,f383]) ).
fof(f2348,plain,
( ! [X0] : is_a_theorem(or(and(X0,possibly(sK0)),not(sK0)))
| ~ spl1_3
| ~ spl1_8
| ~ spl1_15
| ~ spl1_19
| ~ spl1_21
| ~ spl1_37
| ~ spl1_41
| ~ spl1_47
| ~ spl1_51 ),
inference(resolution,[],[f2274,f619]) ).
fof(f4313,plain,
( ! [X0] : is_a_theorem(implies(or(X0,necessarily(not(sK0))),not(sK0)))
| ~ spl1_3
| ~ spl1_5
| ~ spl1_8
| ~ spl1_15
| ~ spl1_19
| ~ spl1_21
| ~ spl1_37
| ~ spl1_41
| ~ spl1_47
| ~ spl1_51 ),
inference(superposition,[],[f2348,f667]) ).
fof(f4520,plain,
( ! [X0] :
( is_a_theorem(implies(X0,not(sK0)))
| is_a_theorem(implies(necessarily(not(sK0)),not(sK0))) )
| ~ spl1_3
| ~ spl1_5
| ~ spl1_8
| ~ spl1_15
| ~ spl1_19
| ~ spl1_21
| ~ spl1_29
| ~ spl1_37
| ~ spl1_41
| ~ spl1_47
| ~ spl1_51 ),
inference(resolution,[],[f4313,f1035]) ).
fof(f4537,plain,
( ! [X0] : is_a_theorem(implies(X0,not(sK0)))
| ~ spl1_3
| ~ spl1_5
| ~ spl1_8
| ~ spl1_11
| ~ spl1_15
| ~ spl1_19
| ~ spl1_21
| ~ spl1_29
| ~ spl1_37
| ~ spl1_41
| ~ spl1_47
| ~ spl1_51 ),
inference(forward_subsumption_resolution,[],[f4520,f279]) ).
fof(f4908,plain,
( $false
| ~ spl1_3
| ~ spl1_5
| ~ spl1_8
| ~ spl1_11
| ~ spl1_15
| ~ spl1_19
| ~ spl1_21
| ~ spl1_29
| ~ spl1_37
| ~ spl1_41
| ~ spl1_47
| ~ spl1_51 ),
inference(resolution,[],[f4537,f383]) ).
fof(f4921,plain,
( ~ spl1_3
| ~ spl1_5
| ~ spl1_8
| ~ spl1_11
| ~ spl1_15
| ~ spl1_19
| ~ spl1_21
| ~ spl1_29
| ~ spl1_37
| ~ spl1_41
| ~ spl1_47
| ~ spl1_51 ),
inference(avatar_contradiction_clause,[],[f4908]) ).
cnf(s2,plain,
( spl1_3
| spl1_4 ),
inference(sat_conversion,[],[f251]) ).
cnf(s3,plain,
( spl1_5
| spl1_6 ),
inference(sat_conversion,[],[f259]) ).
cnf(s4,plain,
( spl1_7
| spl1_8 ),
inference(sat_conversion,[],[f268]) ).
cnf(s6,plain,
( spl1_11
| ~ spl1_12 ),
inference(sat_conversion,[],[f284]) ).
cnf(s8,plain,
( spl1_15
| ~ spl1_16 ),
inference(sat_conversion,[],[f300]) ).
cnf(s10,plain,
( spl1_19
| spl1_20 ),
inference(sat_conversion,[],[f316]) ).
cnf(s11,plain,
( spl1_21
| ~ spl1_22 ),
inference(sat_conversion,[],[f324]) ).
cnf(s15,plain,
( spl1_29
| spl1_30 ),
inference(sat_conversion,[],[f356]) ).
cnf(s19,plain,
( spl1_37
| spl1_38 ),
inference(sat_conversion,[],[f388]) ).
cnf(s21,plain,
( spl1_41
| ~ spl1_42 ),
inference(sat_conversion,[],[f404]) ).
cnf(s24,plain,
( spl1_47
| spl1_48 ),
inference(sat_conversion,[],[f428]) ).
cnf(s26,plain,
( spl1_51
| ~ spl1_52 ),
inference(sat_conversion,[],[f444]) ).
cnf(s27,plain,
~ spl1_7,
inference(sat_conversion,[],[f445]) ).
cnf(s28,plain,
spl1_22,
inference(sat_conversion,[],[f446]) ).
cnf(s30,plain,
spl1_52,
inference(sat_conversion,[],[f448]) ).
cnf(s32,plain,
spl1_42,
inference(sat_conversion,[],[f450]) ).
cnf(s35,plain,
spl1_16,
inference(sat_conversion,[],[f453]) ).
cnf(s36,plain,
spl1_12,
inference(sat_conversion,[],[f454]) ).
cnf(s40,plain,
~ spl1_20,
inference(sat_conversion,[],[f456]) ).
cnf(s41,plain,
~ spl1_48,
inference(sat_conversion,[],[f457]) ).
cnf(s44,plain,
~ spl1_38,
inference(sat_conversion,[],[f460]) ).
cnf(s48,plain,
~ spl1_30,
inference(sat_conversion,[],[f464]) ).
cnf(s51,plain,
~ spl1_6,
inference(sat_conversion,[],[f467]) ).
cnf(s55,plain,
~ spl1_4,
inference(sat_conversion,[],[f470]) ).
cnf(s71,plain,
( ~ spl1_3
| ~ spl1_5
| ~ spl1_8
| ~ spl1_11
| ~ spl1_15
| ~ spl1_19
| ~ spl1_21
| ~ spl1_29
| ~ spl1_37
| ~ spl1_41
| ~ spl1_47
| ~ spl1_51 ),
inference(sat_conversion,[],[f4921]) ).
cnf(s72,plain,
spl1_51,
inference(rat,[],[s26,s30]) ).
cnf(s74,plain,
spl1_47,
inference(rat,[],[s24,s41]) ).
cnf(s77,plain,
spl1_41,
inference(rat,[],[s21,s32]) ).
cnf(s79,plain,
spl1_37,
inference(rat,[],[s19,s44]) ).
cnf(s83,plain,
spl1_29,
inference(rat,[],[s15,s48]) ).
cnf(s87,plain,
spl1_21,
inference(rat,[],[s11,s28]) ).
cnf(s88,plain,
spl1_19,
inference(rat,[],[s10,s40]) ).
cnf(s90,plain,
spl1_15,
inference(rat,[],[s8,s35]) ).
cnf(s92,plain,
spl1_11,
inference(rat,[],[s6,s36]) ).
cnf(s94,plain,
spl1_8,
inference(rat,[],[s4,s27]) ).
cnf(s98,plain,
spl1_5,
inference(rat,[],[s3,s51]) ).
cnf(s99,plain,
~ spl1_3,
inference(rat,[],[s71,s72,s74,s77,s79,s83,s87,s88,s90,s92,s94,s98]) ).
cnf(s100,plain,
$false,
inference(rat,[],[s2,s55,s99]) ).
fof(f4922,plain,
$false,
inference(avatar_sat_refutation,[],[s100]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL533+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.36 % Computer : n002.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sun Sep 27 15:59:36 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.40 Running first-order model finding
% 0.09/0.40 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.08/0.59 % (3708171)Will run a generic schedule for satisfiability detection.
% 1.08/0.59 % (3708182)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2098643336:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 1.08/0.59 % (3708176)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3782666964_2999 on theBenchmark for (2999ds/0Mi)
% 1.08/0.59 % (3708178)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=36810123:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 1.08/0.59 % (3708179)dis+10_1_sil=32000:sp=arity:random_seed=4141574216:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 1.08/0.59 % (3708180)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2496463589:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 1.08/0.59 % TRYING [1]
% 1.08/0.59 % TRYING [2]
% 1.08/0.59 % (3708181)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2861528450:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 1.08/0.59 % TRYING [3]
% 1.08/0.59 % (3708177)% WARNING: option uhcvi not known.
% 1.08/0.59 % TRYING [4]
% 1.08/0.59 % (3708177)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1823543297:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 1.08/0.59 % (3708182)Instruction limit reached!
% 1.08/0.59 % (3708182)------------------------------
% 1.08/0.59 % (3708182)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.08/0.59 % (3708182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.08/0.59 % (3708182)CaDiCaL version: 2.1.3
% 1.08/0.59 % (3708182)Termination reason: Instruction limit
% 1.08/0.59 % (3708182)Termination phase: Saturation
% 1.08/0.59 % (3708182)Time elapsed: 0.064 s
% 1.08/0.59 % (3708182)Peak memory usage: 14 MB
% 1.08/0.59 % (3708182)Instructions burned: 160 (million)
% 1.08/0.59 % (3708179)Instruction limit reached!
% 1.08/0.59 % (3708179)------------------------------
% 1.08/0.59 % (3708179)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.08/0.59 % (3708179)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.08/0.59 % (3708179)CaDiCaL version: 2.1.3
% 1.08/0.59 % (3708179)Termination reason: Instruction limit
% 1.08/0.59 % (3708179)Termination phase: Saturation
% 1.08/0.59 % (3708179)Time elapsed: 0.068 s
% 1.08/0.59 % (3708179)Peak memory usage: 13 MB
% 1.08/0.59 % (3708179)Instructions burned: 103 (million)
% 1.08/0.59 % (3708190)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4257902598:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 1.08/0.59 % TRYING [1]
% 1.08/0.59 % TRYING [2]
% 1.08/0.59 % TRYING [3]
% 1.08/0.59 % (3708180)Instruction limit reached!
% 1.08/0.59 % (3708180)------------------------------
% 1.08/0.59 % (3708180)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.08/0.59 % (3708180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.08/0.59 % (3708180)CaDiCaL version: 2.1.3
% 1.08/0.59 % (3708180)Termination reason: Instruction limit
% 1.08/0.59 % (3708180)Termination phase: Saturation
% 1.08/0.59 % (3708180)Time elapsed: 0.076 s
% 1.08/0.59 % (3708180)Peak memory usage: 13 MB
% 1.08/0.59 % (3708180)Instructions burned: 117 (million)
% 1.08/0.59 % TRYING [4]
% 1.08/0.59 % (3708192)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1019117052:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 1.08/0.59 % TRYING [5]
% 1.08/0.59 % (3708193)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=3808769938:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 1.08/0.59 % (3708181)Instruction limit reached!
% 1.08/0.59 % (3708181)------------------------------
% 1.08/0.59 % (3708181)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.08/0.59 % (3708181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.08/0.59 % (3708181)CaDiCaL version: 2.1.3
% 1.08/0.59 % (3708181)Termination reason: Instruction limit
% 1.08/0.59 % (3708181)Termination phase: Saturation
% 1.08/0.59 % (3708181)Time elapsed: 0.102 s
% 1.08/0.59 % (3708181)Peak memory usage: 14 MB
% 1.08/0.59 % (3708181)Instructions burned: 132 (million)
% 1.08/0.59 % (3708196)ott-21_1_sil=16000:fs=off:random_seed=1565538754:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 1.08/0.59 % (3708177) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3708171-3708177"...
% 1.08/0.59 % (3708177)...printing done.
% 1.08/0.59 % (3708177)Refutation found. Thanks to Tanya!
% 1.08/0.59 % SZS status Theorem for theBenchmark
% 1.08/0.59 % SZS output start Proof for theBenchmark
% See solution above
% 1.08/0.59 % (3708177)------------------------------
% 1.08/0.59 % (3708177)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.08/0.59 % (3708177)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.08/0.59 % (3708177)CaDiCaL version: 2.1.3
% 1.08/0.59 % (3708177)Termination reason: Refutation
% 1.08/0.59 % (3708177)Time elapsed: 0.123 s
% 1.08/0.59 % (3708177)Peak memory usage: 15 MB
% 1.08/0.59 % (3708177)Instructions burned: 195 (million)
% 1.08/0.59 % (3708171)Success in time 0.185 s
% 1.08/0.59 % Vampire exiting
%------------------------------------------------------------------------------