Vampire 4.8
Michael Rawson
TU Wien, Austria
Sample solution for NLP042+1
% SZS status CounterSatisfiable for NLP042+1
% SZS output start Saturation.
cnf(u147,negated_conjecture,
woman(sK0,sK1)).
cnf(u151,negated_conjecture,
mia_forename(sK0,sK2)).
cnf(u155,negated_conjecture,
forename(sK0,sK2)).
cnf(u159,negated_conjecture,
shake_beverage(sK0,sK3)).
cnf(u163,negated_conjecture,
event(sK0,sK4)).
cnf(u167,negated_conjecture,
nonreflexive(sK0,sK4)).
cnf(u171,negated_conjecture,
order(sK0,sK4)).
cnf(u175,negated_conjecture,
of(sK0,sK2,sK1)).
cnf(u179,negated_conjecture,
agent(sK0,sK4,sK1)).
cnf(u183,negated_conjecture,
patient(sK0,sK4,sK3)).
cnf(u187,axiom,
~nonhuman(X0,X1) | ~human(X0,X1)).
cnf(u191,axiom,
~nonexistent(X0,X1) | ~existent(X0,X1)).
cnf(u195,axiom,
~nonliving(X0,X1) | ~animate(X0,X1)).
cnf(u199,axiom,
~food(X0,X1) | substance_matter(X0,X1)).
cnf(u203,axiom,
~beverage(X0,X1) | food(X0,X1)).
cnf(u207,axiom,
~shake_beverage(X0,X1) | beverage(X0,X1)).
cnf(u211,axiom,
~relname(X0,X1) | relation(X0,X1)).
cnf(u215,axiom,
~substance_matter(X0,X1) | object(X0,X1)).
cnf(u219,axiom,
~relation(X0,X1) | abstraction(X0,X1)).
cnf(u223,axiom,
forename(X0,X1) | ~mia_forename(X0,X1)).
cnf(u227,axiom,
~act(X0,X1) | event(X0,X1)).
cnf(u231,axiom,
~nonliving(X0,X1) | ~living(X0,X1)).
cnf(u235,axiom,
female(X0,X1) | ~woman(X0,X1)).
cnf(u239,axiom,
act(X0,X1) | ~order(X0,X1)).
cnf(u243,axiom,
human_person(X0,X1) | ~woman(X0,X1)).
cnf(u247,axiom,
event(X0,X1) | ~order(X0,X1)).
cnf(u251,axiom,
animate(X0,X1) | ~human_person(X0,X1)).
cnf(u255,axiom,
living(X0,X1) | ~organism(X0,X1)).
cnf(u259,axiom,
human(X0,X1) | ~human_person(X0,X1)).
cnf(u263,axiom,
organism(X0,X1) | ~human_person(X0,X1)).
cnf(u267,axiom,
entity(X0,X1) | ~organism(X0,X1)).
cnf(u271,axiom,
general(X0,X1) | ~abstraction(X0,X1)).
cnf(u275,axiom,
~abstraction(X0,X1) | nonhuman(X0,X1)).
cnf(u279,axiom,
~eventuality(X0,X1) | nonexistent(X0,X1)).
cnf(u283,axiom,
~object(X0,X1) | nonliving(X0,X1)).
cnf(u287,axiom,
~eventuality(X0,X1) | specific(X0,X1)).
cnf(u291,axiom,
~object(X0,X1) | entity(X0,X1)).
cnf(u295,axiom,
~eventuality(X0,X1) | unisex(X0,X1)).
cnf(u299,axiom,
unisex(X0,X1) | ~abstraction(X0,X1)).
cnf(u303,axiom,
~object(X0,X1) | unisex(X0,X1)).
cnf(u307,axiom,
~specific(X0,X1) | ~general(X0,X1)).
cnf(u311,axiom,
relname(X0,X1) | ~forename(X0,X1)).
cnf(u315,axiom,
existent(X0,X1) | ~entity(X0,X1)).
cnf(u319,axiom,
specific(X0,X1) | ~entity(X0,X1)).
cnf(u323,axiom,
~female(X0,X1) | ~unisex(X0,X1)).
cnf(u327,axiom,
~event(X0,X1) | eventuality(X0,X1)).
cnf(u332,negated_conjecture,
beverage(sK0,sK3)).
cnf(u337,negated_conjecture,
food(sK0,sK3)).
cnf(u342,negated_conjecture,
substance_matter(sK0,sK3)).
cnf(u347,negated_conjecture,
object(sK0,sK3)).
cnf(u353,negated_conjecture,
nonliving(sK0,sK3)).
cnf(u359,negated_conjecture,
~living(sK0,sK3)).
cnf(u365,negated_conjecture,
entity(sK0,sK3)).
cnf(u369,negated_conjecture,
~animate(sK0,sK3)).
cnf(u374,negated_conjecture,
~organism(sK0,sK3)).
cnf(u379,negated_conjecture,
~human_person(sK0,sK3)).
cnf(u385,negated_conjecture,
unisex(sK0,sK3)).
cnf(u389,negated_conjecture,
~woman(sK0,sK3)).
cnf(u398,negated_conjecture,
eventuality(sK0,sK4)).
cnf(u402,axiom,
~nonreflexive(X0,X1) | ~agent(X0,X1,X3) | ~patient(X0,X1,X3)).
cnf(u409,negated_conjecture,
unisex(sK0,sK4)).
cnf(u414,negated_conjecture,
specific(sK0,sK4)).
cnf(u419,negated_conjecture,
nonexistent(sK0,sK4)).
cnf(u423,axiom,
~of(X0,X3,X1) | ~forename(X0,X2) | ~of(X0,X2,X1) | ~forename(X0,X3) | X2 = X3 | ~entity(X0,X1)).
cnf(u428,negated_conjecture,
~general(sK0,sK4)).
cnf(u435,negated_conjecture,
~existent(sK0,sK4)).
cnf(u440,negated_conjecture,
~abstraction(sK0,sK4)).
cnf(u444,axiom,
relation(X0,X1) | ~forename(X0,X1)).
cnf(u448,negated_conjecture,
~entity(sK0,sK4)).
cnf(u454,negated_conjecture,
~organism(sK0,sK4)).
cnf(u459,negated_conjecture,
~human_person(sK0,sK4)).
cnf(u463,axiom,
~general(X0,X1) | ~entity(X0,X1)).
cnf(u468,negated_conjecture,
~woman(sK0,sK4)).
cnf(u473,axiom,
~woman(X0,X1) | ~unisex(X0,X1)).
cnf(u478,negated_conjecture,
~unisex(sK0,sK1)).
cnf(u482,axiom,
~order(X0,X1) | eventuality(X0,X1)).
cnf(u487,negated_conjecture,
~abstraction(sK0,sK1)).
cnf(u492,axiom,
~forename(X0,X1) | abstraction(X0,X1)).
cnf(u498,negated_conjecture,
abstraction(sK0,sK2)).
cnf(u502,negated_conjecture,
~patient(sK0,sK4,X0) | ~agent(sK0,sK4,X0)).
cnf(u507,negated_conjecture,
nonhuman(sK0,sK2)).
cnf(u513,negated_conjecture,
~human(sK0,sK2)).
cnf(u518,negated_conjecture,
~human_person(sK0,sK2)).
cnf(u525,negated_conjecture,
~of(sK0,X0,sK1) | sK2 = X0 | ~forename(sK0,X0)).
cnf(u543,negated_conjecture,
~woman(sK0,sK2)).
cnf(u548,negated_conjecture,
~agent(sK0,sK4,sK3)).
cnf(u552,axiom,
~abstraction(X0,X1) | ~entity(X0,X1)).
cnf(u557,negated_conjecture,
~entity(sK0,sK2)).
cnf(u562,axiom,
~mia_forename(X0,X1) | abstraction(X0,X1)).
cnf(u566,negated_conjecture,
~organism(sK0,sK2)).
% SZS output end Saturation.
Sample solution for SWV017+1
% SZS status Satisfiable for SWV017+1
% SZS output start FiniteModel for SWV017+1
tff(declare_$i,type,$i:$tType).
tff(declare_$i1,type,at:$i).
tff(declare_$i2,type,t:$i).
tff(finite_domain,axiom,
! [X:$i] : (
X = at | X = t
) ).
tff(distinct_domain,axiom,
at != t
).
tff(declare_bool,type,$o:$tType).
tff(declare_bool1,type,fmb_bool_1:$o).
tff(finite_domain,axiom,
! [X:$o] : (
X = fmb_bool_1
) ).
tff(declare_a,type,a:$i).
tff(a_definition,axiom,a = t).
tff(declare_b,type,b:$i).
tff(b_definition,axiom,b = at).
tff(declare_an_a_nonce,type,an_a_nonce:$i).
tff(an_a_nonce_definition,axiom,an_a_nonce = t).
tff(declare_bt,type,bt:$i).
tff(bt_definition,axiom,bt = at).
tff(declare_an_intruder_nonce,type,an_intruder_nonce:$i).
tff(an_intruder_nonce_definition,axiom,an_intruder_nonce = t).
tff(declare_key,type,key: $i * $i > $i).
tff(function_key,axiom,
key(at,at) = t
& key(at,t) = at
& key(t,at) = t
& key(t,t) = t
).
tff(declare_pair,type,pair: $i * $i > $i).
tff(function_pair,axiom,
pair(at,at) = t
& pair(at,t) = t
& pair(t,at) = t
& pair(t,t) = t
).
tff(declare_sent,type,sent: $i * $i * $i > $i).
tff(function_sent,axiom,
sent(at,at,at) = at
& sent(at,at,t) = at
& sent(at,t,at) = at
& sent(at,t,t) = at
& sent(t,at,at) = at
& sent(t,at,t) = at
& sent(t,t,at) = at
& sent(t,t,t) = at
).
tff(declare_quadruple,type,quadruple: $i * $i * $i * $i > $i).
tff(function_quadruple,axiom,
quadruple(at,at,at,at) = at
& quadruple(at,at,at,t) = t
& quadruple(at,at,t,at) = at
& quadruple(at,at,t,t) = at
& quadruple(at,t,at,at) = t
& quadruple(at,t,at,t) = t
& quadruple(at,t,t,at) = at
& quadruple(at,t,t,t) = at
& quadruple(t,at,at,at) = at
& quadruple(t,at,at,t) = at
& quadruple(t,at,t,at) = t
& quadruple(t,at,t,t) = t
& quadruple(t,t,at,at) = t
& quadruple(t,t,at,t) = t
& quadruple(t,t,t,at) = t
& quadruple(t,t,t,t) = t
).
tff(declare_encrypt,type,encrypt: $i * $i > $i).
tff(function_encrypt,axiom,
encrypt(at,at) = at
& encrypt(at,t) = t
& encrypt(t,at) = at
& encrypt(t,t) = t
).
tff(declare_triple,type,triple: $i * $i * $i > $i).
tff(function_triple,axiom,
triple(at,at,at) = at
& triple(at,at,t) = at
& triple(at,t,at) = at
& triple(at,t,t) = at
& triple(t,at,at) = t
& triple(t,at,t) = t
& triple(t,t,at) = t
& triple(t,t,t) = t
).
tff(declare_generate_b_nonce,type,generate_b_nonce: $i > $i).
tff(function_generate_b_nonce,axiom,
generate_b_nonce(at) = t
& generate_b_nonce(t) = t
).
tff(declare_generate_expiration_time,type,generate_expiration_time: $i > $i).
tff(function_generate_expiration_time,axiom,
generate_expiration_time(at) = t
& generate_expiration_time(t) = t
).
tff(declare_generate_key,type,generate_key: $i > $i).
tff(function_generate_key,axiom,
generate_key(at) = at
& generate_key(t) = at
).
tff(declare_generate_intruder_nonce,type,generate_intruder_nonce: $i > $i).
tff(function_generate_intruder_nonce,axiom,
generate_intruder_nonce(at) = at
& generate_intruder_nonce(t) = t
).
tff(declare_a_holds,type,a_holds: $i > $o ).
tff(predicate_a_holds,axiom,
% a_holds(at) undefined in model
% a_holds(t) undefined in model
).
tff(declare_party_of_protocol,type,party_of_protocol: $i > $o ).
tff(predicate_party_of_protocol,axiom,
party_of_protocol(at)
& party_of_protocol(t)
).
tff(declare_message,type,message: $i > $o ).
tff(predicate_message,axiom,
message(at)
& ~message(t)
).
tff(declare_a_stored,type,a_stored: $i > $o ).
tff(predicate_a_stored,axiom,
~a_stored(at)
& a_stored(t)
).
tff(declare_b_holds,type,b_holds: $i > $o ).
tff(predicate_b_holds,axiom,
% b_holds(at) undefined in model
% b_holds(t) undefined in model
).
tff(declare_fresh_to_b,type,fresh_to_b: $i > $o ).
tff(predicate_fresh_to_b,axiom,
~fresh_to_b(at)
& fresh_to_b(t)
).
tff(declare_b_stored,type,b_stored: $i > $o ).
tff(predicate_b_stored,axiom,
% b_stored(at) undefined in model
% b_stored(t) undefined in model
).
tff(declare_a_key,type,a_key: $i > $o ).
tff(predicate_a_key,axiom,
a_key(at)
& ~a_key(t)
).
tff(declare_t_holds,type,t_holds: $i > $o ).
tff(predicate_t_holds,axiom,
t_holds(at)
& t_holds(t)
).
tff(declare_a_nonce,type,a_nonce: $i > $o ).
tff(predicate_a_nonce,axiom,
~a_nonce(at)
& a_nonce(t)
).
tff(declare_intruder_message,type,intruder_message: $i > $o ).
tff(predicate_intruder_message,axiom,
intruder_message(at)
& intruder_message(t)
).
tff(declare_intruder_holds,type,intruder_holds: $i > $o ).
tff(predicate_intruder_holds,axiom,
intruder_holds(at)
& intruder_holds(t)
).
tff(declare_fresh_intruder_nonce,type,fresh_intruder_nonce: $i > $o ).
tff(predicate_fresh_intruder_nonce,axiom,
~fresh_intruder_nonce(at)
& fresh_intruder_nonce(t)
).
% SZS output end FiniteModel for SWV017+1
Vampire 5.0
Michael Rawson
University of Southampton, United Kongdom
Notes regarding saturations
Vampire can testify (counter)-satisfiability of a given problem by finitely saturating the
corresponding preprocessed clause set (using a complete version of a calculus). It then reports
SZS Status Satisfiable.
As supporting evidence, Vampire prints two artefacts:
The saturated clause set itself between SZS output start Saturation and SZS output
end Saturation, and a section of "Definitions and Model Updates".
Among the preprocessing steps used by Vampire in order to transform an arbitrary first-order
problem into the CNF on which saturation starts are some steps (we call them
interferences) which only preserve model existence, but not all models, or which modify
the signature.
Each of these steps comes with a model-theoretic argument of the form: "If you give me a model
of the post-step F, this is what you must do to get a model of pre-step F".
The "Definitions and Model Updates" section lists these transformations in the order in which
they should be applied to the model of the final CNF (that just got saturated) in order to arrive
at a model of the original input problem.
These transformations are implemented in Vampire already to work on finite models found by its
finite model finder, but since the model represented by finite saturations is only implicit, we do
our best to at least report what transformations have been recorded and should be played back.
Here is an explanation for the transformations implemented (so far):
- Eliminated symbols are defined in terms of their original definitions. E.g. for predicates:
for all inputs,
define r(X0,X1) := p(X0,b)
or for functions (constants):
for all inputs,
define a := aa
- Partially eliminated definitions (e.g., when Vampire turns
![X:ta] : (~qq(X) <=> ~(q(X) & (?[X:ta] : q(X))))
into
![X:ta] : (~qq(X) <= ~(q(X) & (?[X:ta] : q(X))))
because all the remaining occurrences of qq are positive.) may require conditional atom flips:
for all groundings,
whenever ? [X1 : ta] : q(X1) & q(X0) is true, set qq(X0) to true
Here "for all groundings" suggests a Herbrand model, but the meaning is the same as "for
all inputs".
- We also have globally flip the polarity of every occurrence of a predicate, e.g.,
'$ki_accessible', which means: "negate the whole truth table for the corresponding
predicate" and complements the optional random_polarities preprocessing step ("As part of
preprocessing, randomly (though consistently) flip polarities of non-equality predicates in
the whole CNF.").
- To complement blocked clause elimination
(https://easychair.org/publications/paper/Bl2v/open)
we may introduce a more complicated version of a conditional flip. E.g.,
for all groundings, until fixed point,
whenever teach(X1,X0,cs) | ~'$ki_accessible'('$ki_local_world',X1) | ~teach('$ki_local_world',X0,psych) | ~'$ki_exists_in_world_$i'('$ki_local_world',X0) is false, set teach(X1,X0,cs) to true
The "until fixed point" bit is necessary and explained in Lemma 4 of the BCE paper.
In a nutshell, this means: if you go over your groundings and flip something, you have to
then restart and go from the beginning again.
In the finite model building version of this (which actually does the changes as described)
we use a do-while loop
(https://github.com/vprover/vampire/blob/0dce69acaa3452831bf8f851485da9266aa02b57/FMB/FiniteModelMultiSorted.cpp#L1093)
Solution for SET014^4
thf(func_def_0, type, in: $i > ($i > $o) > $o).
thf(func_def_2, type, is_a: $i > ($i > $o) > $o).
thf(func_def_3, type, emptyset: $i > $o).
thf(func_def_4, type, unord_pair: $i > $i > $i > $o).
thf(func_def_5, type, singleton: $i > $i > $o).
thf(func_def_6, type, union: ($i > $o) > ($i > $o) > $i > $o).
thf(func_def_7, type, excl_union: ($i > $o) > ($i > $o) > $i > $o).
thf(func_def_8, type, intersection: ($i > $o) > ($i > $o) > $i > $o).
thf(func_def_9, type, setminus: ($i > $o) > ($i > $o) > $i > $o).
thf(func_def_10, type, complement: ($i > $o) > $i > $o).
thf(func_def_11, type, disjoint: ($i > $o) > ($i > $o) > $o).
thf(func_def_12, type, subset: ($i > $o) > ($i > $o) > $o).
thf(func_def_13, type, meets: ($i > $o) > ($i > $o) > $o).
thf(func_def_14, type, misses: ($i > $o) > ($i > $o) > $o).
thf(func_def_28, type, sK0: $i > $o).
thf(func_def_29, type, sK1: $i > $o).
thf(func_def_30, type, sK2: $i > $o).
thf(f113,plain,(
$false),
inference(avatar_sat_refutation,[],[f92,f106,f112])).
thf(f112,plain,(
~spl3_1),
inference(avatar_contradiction_clause,[],[f111])).
thf(f111,plain,(
$false | ~spl3_1),
inference(trivial_inequality_removal,[],[f107])).
thf(f107,plain,(
($true = $false) | ~spl3_1),
inference(superposition,[],[f87,f96])).
thf(f96,plain,(
($false = (sK2 @ sK4))),
inference(trivial_inequality_removal,[],[f94])).
thf(f94,plain,(
($true = $false) | ($false = (sK2 @ sK4))),
inference(superposition,[],[f79,f73])).
thf(f73,plain,(
((sK1 @ sK4) = $false)),
inference(binary_proxy_clausification,[],[f72])).
thf(f72,plain,(
((((sK2 @ sK4) | (sK0 @ sK4)) => (sK1 @ sK4)) = $false)),
inference(beta_eta_normalization,[],[f71])).
thf(f71,plain,(
($false = ((^[Y0 : $i]: (((sK2 @ Y0) | (sK0 @ Y0)) => (sK1 @ Y0))) @ sK4))),
inference(sigma_clausification,[],[f70])).
thf(f70,plain,(
($true != (!! @ $i @ (^[Y0 : $i]: (((sK2 @ Y0) | (sK0 @ Y0)) => (sK1 @ Y0)))))),
inference(beta_eta_normalization,[],[f67])).
thf(f67,plain,(
($true != ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (!! @ $i @ (^[Y2 : $i]: ((Y0 @ Y2) => (Y1 @ Y2))))))) @ ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) | (Y1 @ Y2))))))) @ sK2 @ sK0) @ sK1))),
inference(definition_unfolding,[],[f59,f52,f60])).
thf(f60,plain,(
(union = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) | (Y1 @ Y2))))))))),
inference(cnf_transformation,[],[f28])).
thf(f28,plain,(
(union = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: ((^[Y2 : $i]: ((Y0 @ Y2) | (Y1 @ Y2))))))))),
inference(fool_elimination,[],[f27])).
thf(f27,plain,(
((^[X0 : $i > $o, X1 : $i > $o, X2 : $i] : ((X1 @ X2) | (X0 @ X2))) = union)),
inference(rectify,[],[f6])).
thf(f6,axiom,(
((^[X0 : $i > $o, X2 : $i > $o, X3 : $i] : ((X2 @ X3) | (X0 @ X3))) = union)),
file('Problems/SET/SET014^4.p',union)).
thf(f52,plain,(
(subset = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (!! @ $i @ (^[Y2 : $i]: ((Y0 @ Y2) => (Y1 @ Y2))))))))),
inference(cnf_transformation,[],[f36])).
thf(f36,plain,(
(subset = (^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (!! @ $i @ (^[Y2 : $i]: ((Y0 @ Y2) => (Y1 @ Y2))))))))),
inference(fool_elimination,[],[f35])).
thf(f35,plain,(
(subset = (^[X0 : $i > $o, X1 : $i > $o] : (! [X2] : ((X0 @ X2) => (X1 @ X2)))))),
inference(rectify,[],[f12])).
thf(f12,axiom,(
(subset = (^[X0 : $i > $o, X2 : $i > $o] : (! [X3] : ((X0 @ X3) => (X2 @ X3)))))),
file('Problems/SET/SET014^4.p',subset)).
thf(f59,plain,(
((subset @ (union @ sK2 @ sK0) @ sK1) != $true)),
inference(cnf_transformation,[],[f48])).
thf(f48,plain,(
((subset @ (union @ sK2 @ sK0) @ sK1) != $true) & ($true = (subset @ sK0 @ sK1)) & ($true = (subset @ sK2 @ sK1))),
inference(skolemisation,[status(esa),new_symbols(skolem,[sK0,sK1,sK2])],[f46,f47])).
thf(f47,plain,(
? [X0 : $i > $o,X1 : $i > $o,X2 : $i > $o] : (($true != (subset @ (union @ X2 @ X0) @ X1)) & ($true = (subset @ X0 @ X1)) & ($true = (subset @ X2 @ X1))) => (((subset @ (union @ sK2 @ sK0) @ sK1) != $true) & ($true = (subset @ sK0
@ sK1)) & ($true = (subset @ sK2 @ sK1)))),
introduced(choice_axiom,[])).
thf(f46,plain,(
? [X0 : $i > $o,X1 : $i > $o,X2 : $i > $o] : (($true != (subset @ (union @ X2 @ X0) @ X1)) & ($true = (subset @ X0 @ X1)) & ($true = (subset @ X2 @ X1)))),
inference(flattening,[],[f45])).
thf(f45,plain,(
? [X0 : $i > $o,X1 : $i > $o,X2 : $i > $o] : (($true != (subset @ (union @ X2 @ X0) @ X1)) & (($true = (subset @ X2 @ X1)) & ($true = (subset @ X0 @ X1))))),
inference(ennf_transformation,[],[f30])).
thf(f30,plain,(
~! [X0 : $i > $o,X1 : $i > $o,X2 : $i > $o] : ((($true = (subset @ X2 @ X1)) & ($true = (subset @ X0 @ X1))) => ($true = (subset @ (union @ X2 @ X0) @ X1)))),
inference(fool_elimination,[],[f29])).
thf(f29,plain,(
~! [X0 : $i > $o,X1 : $i > $o,X2 : $i > $o] : (((subset @ X2 @ X1) & (subset @ X0 @ X1)) => (subset @ (union @ X2 @ X0) @ X1))),
inference(rectify,[],[f16])).
thf(f16,negated_conjecture,(
~! [X2 : $i > $o,X4 : $i > $o,X0 : $i > $o] : (((subset @ X0 @ X4) & (subset @ X2 @ X4)) => (subset @ (union @ X0 @ X2) @ X4))),
inference(negated_conjecture,[],[f15])).
thf(f15,conjecture,(
! [X2 : $i > $o,X4 : $i > $o,X0 : $i > $o] : (((subset @ X0 @ X4) & (subset @ X2 @ X4)) => (subset @ (union @ X0 @ X2) @ X4))),
file('Problems/SET/SET014^4.p',thm)).
thf(f79,plain,(
( ! [X1 : $i] : (($true = (sK1 @ X1)) | ((sK2 @ X1) = $false)) )),
inference(binary_proxy_clausification,[],[f78])).
thf(f78,plain,(
( ! [X1 : $i] : (($true = ((sK2 @ X1) => (sK1 @ X1)))) )),
inference(beta_eta_normalization,[],[f77])).
thf(f77,plain,(
( ! [X1 : $i] : (($true = ((^[Y0 : $i]: ((sK2 @ Y0) => (sK1 @ Y0))) @ X1))) )),
inference(pi_clausification,[],[f76])).
thf(f76,plain,(
($true = (!! @ $i @ (^[Y0 : $i]: ((sK2 @ Y0) => (sK1 @ Y0)))))),
inference(beta_eta_normalization,[],[f69])).
thf(f69,plain,(
($true = ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (!! @ $i @ (^[Y2 : $i]: ((Y0 @ Y2) => (Y1 @ Y2))))))) @ sK2 @ sK1))),
inference(definition_unfolding,[],[f57,f52])).
thf(f57,plain,(
($true = (subset @ sK2 @ sK1))),
inference(cnf_transformation,[],[f48])).
thf(f87,plain,(
($true = (sK2 @ sK4)) | ~spl3_1),
inference(avatar_component_clause,[],[f85])).
thf(f85,plain,(
spl3_1 <=> ($true = (sK2 @ sK4))),
introduced(avatar_definition,[new_symbols(naming,[spl3_1])])).
thf(f106,plain,(
~spl3_2),
inference(avatar_contradiction_clause,[],[f105])).
thf(f105,plain,(
$false | ~spl3_2),
inference(trivial_inequality_removal,[],[f101])).
thf(f101,plain,(
($true = $false) | ~spl3_2),
inference(superposition,[],[f100,f91])).
thf(f91,plain,(
($true = (sK0 @ sK4)) | ~spl3_2),
inference(avatar_component_clause,[],[f89])).
thf(f89,plain,(
spl3_2 <=> ($true = (sK0 @ sK4))),
introduced(avatar_definition,[new_symbols(naming,[spl3_2])])).
thf(f100,plain,(
((sK0 @ sK4) = $false)),
inference(trivial_inequality_removal,[],[f97])).
thf(f97,plain,(
($true = $false) | ((sK0 @ sK4) = $false)),
inference(superposition,[],[f83,f73])).
thf(f83,plain,(
( ! [X1 : $i] : (($true = (sK1 @ X1)) | ($false = (sK0 @ X1))) )),
inference(binary_proxy_clausification,[],[f82])).
thf(f82,plain,(
( ! [X1 : $i] : (($true = ((sK0 @ X1) => (sK1 @ X1)))) )),
inference(beta_eta_normalization,[],[f81])).
thf(f81,plain,(
( ! [X1 : $i] : (($true = ((^[Y0 : $i]: ((sK0 @ Y0) => (sK1 @ Y0))) @ X1))) )),
inference(pi_clausification,[],[f80])).
thf(f80,plain,(
($true = (!! @ $i @ (^[Y0 : $i]: ((sK0 @ Y0) => (sK1 @ Y0)))))),
inference(beta_eta_normalization,[],[f68])).
thf(f68,plain,(
($true = ((^[Y0 : $i > $o]: ((^[Y1 : $i > $o]: (!! @ $i @ (^[Y2 : $i]: ((Y0 @ Y2) => (Y1 @ Y2))))))) @ sK0 @ sK1))),
inference(definition_unfolding,[],[f58,f52])).
thf(f58,plain,(
($true = (subset @ sK0 @ sK1))),
inference(cnf_transformation,[],[f48])).
thf(f92,plain,(
spl3_1 | spl3_2),
inference(avatar_split_clause,[],[f75,f89,f85])).
thf(f75,plain,(
($true = (sK2 @ sK4)) | ($true = (sK0 @ sK4))),
inference(binary_proxy_clausification,[],[f74])).
thf(f74,plain,(
($true = ((sK2 @ sK4) | (sK0 @ sK4)))),
inference(binary_proxy_clausification,[],[f72])).
Solution for DAT013_1
% SUCCESS: Derivation has unique formula names
% SUCCESS: All derived formulae have parents and inference information
% WARNING: Took the first false root f43 as the single derivation root
% SUCCESS: Derivation is acyclic
% SUCCESS: Derivation looks like a refutation
% SUCCESS: Negated conjecture f4 is a leaf or CTH from a conjecture
% SUCCESS: Assumptions are propagated
% SUCCESS: Assumptions are discharged
% NOTICE: Took the conjecture f3 as the proved formula
% CPUTIME: 0.06
% SUCCESS: Verified
% SZS status Verified
tff(type_def_5, type, array: $tType).
tff(func_def_0, type, read: (array * $int) > $int).
tff(func_def_1, type, write: (array * $int * $int) > array).
tff(func_def_5, type, sK0: array).
tff(func_def_6, type, sK1: $int).
tff(func_def_7, type, sK2: $int).
tff(func_def_8, type, sK3: $int).
tff(func_def_9, type, -1: $int > $int).
tff(f43,plain,(
$false),
inference(avatar_sat_refutation,[],[f35,f38,f42])).
tff(f42,plain,(
~spl4_1),
inference(avatar_contradiction_clause,[],[f41])).
tff(f41,plain,(
$false | ~spl4_1),
inference(alasca_normalization,[],[f40])).
tff(f40,plain,(
$greater($sum($sum($uminus(sK3),$sum(-2,sK3)),-1),0) | ~spl4_1),
inference(alasca_fourier_motzkin,[],[f30,f20])).
tff(f20,plain,(
$greater($sum(-1(sK1),$sum(sK3,-2)),0)),
inference(alasca_normalization,[],[f16])).
tff(f16,plain,(
~$less(sK3,$sum(sK1,3))),
inference(cnf_transformation,[],[f12])).
tff(f12,plain,(
(~$less(0,read(sK0,sK3)) & ~$less(sK2,sK3) & ~$less(sK3,$sum(sK1,3))) & ! [X4 : $int] : ($less(0,read(sK0,X4)) | $less(sK2,X4) | $less(X4,sK1))),
inference(skolemisation,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3])],[f9,f11,f10])).
tff(f10,plain,(
? [X0 : array,X1 : $int,X2 : $int] : (? [X3 : $int] : (~$less(0,read(X0,X3)) & ~$less(X2,X3) & ~$less(X3,$sum(X1,3))) & ! [X4 : $int] : ($less(0,read(X0,X4)) | $less(X2,X4) | $less(X4,X1))) => (? [X3 : $int] : (~$less(0,read(sK0,X3)) & ~
$less(sK2,X3) & ~$less(X3,$sum(sK1,3))) & ! [X4 : $int] : ($less(0,read(sK0,X4)) | $less(sK2,X4) | $less(X4,sK1)))),
introduced(definition,[],[choice_axiom])).
tff(f11,plain,(
? [X3 : $int] : (~$less(0,read(sK0,X3)) & ~$less(sK2,X3) & ~$less(X3,$sum(sK1,3))) => (~$less(0,read(sK0,sK3)) & ~$less(sK2,sK3) & ~$less(sK3,$sum(sK1,3)))),
introduced(definition,[],[choice_axiom])).
tff(f9,plain,(
? [X0 : array,X1 : $int,X2 : $int] : (? [X3 : $int] : (~$less(0,read(X0,X3)) & ~$less(X2,X3) & ~$less(X3,$sum(X1,3))) & ! [X4 : $int] : ($less(0,read(X0,X4)) | $less(X2,X4) | $less(X4,X1)))),
inference(rectify,[],[f8])).
tff(f8,plain,(
? [X0 : array,X1 : $int,X2 : $int] : (? [X4 : $int] : (~$less(0,read(X0,X4)) & ~$less(X2,X4) & ~$less(X4,$sum(X1,3))) & ! [X3 : $int] : ($less(0,read(X0,X3)) | $less(X2,X3) | $less(X3,X1)))),
inference(flattening,[],[f7])).
tff(f7,plain,(
? [X0 : array,X1 : $int,X2 : $int] : (? [X4 : $int] : (~$less(0,read(X0,X4)) & (~$less(X2,X4) & ~$less(X4,$sum(X1,3)))) & ! [X3 : $int] : ($less(0,read(X0,X3)) | ($less(X2,X3) | $less(X3,X1))))),
inference(ennf_transformation,[],[f5])).
tff(f5,plain,(
~! [X0 : array,X1 : $int,X2 : $int] : (! [X3 : $int] : ((~$less(X2,X3) & ~$less(X3,X1)) => $less(0,read(X0,X3))) => ! [X4 : $int] : ((~$less(X2,X4) & ~$less(X4,$sum(X1,3))) => $less(0,read(X0,X4))))),
inference(theory_normalization,[],[f4])).
tff(f4,negated_conjecture,(
~! [X0 : array,X1 : $int,X2 : $int] : (! [X3 : $int] : (($lesseq(X3,X2) & $lesseq(X1,X3)) => $greater(read(X0,X3),0)) => ! [X4 : $int] : (($lesseq(X4,X2) & $lesseq($sum(X1,3),X4)) => $greater(read(X0,X4),0)))),
inference(negated_conjecture,[status(cth)],[f3])).
tff(f3,conjecture,(
! [X0 : array,X1 : $int,X2 : $int] : (! [X3 : $int] : (($lesseq(X3,X2) & $lesseq(X1,X3)) => $greater(read(X0,X3),0)) => ! [X4 : $int] : (($lesseq(X4,X2) & $lesseq($sum(X1,3),X4)) => $greater(read(X0,X4),0)))),
file('Problems/DAT/DAT013_1.p',unknown)).
tff(f30,plain,(
$greater($sum(sK1,-1(sK3)),0) | ~spl4_1),
inference(avatar_component_clause,[],[f28])).
tff(f28,definition,(
spl4_1 <=> $greater($sum(sK1,-1(sK3)),0)),
introduced(definition,[new_symbols(naming,[spl4_1])],[avatar_definition])).
tff(f38,plain,(
~spl4_2),
inference(avatar_contradiction_clause,[],[f37])).
tff(f37,plain,(
$false | ~spl4_2),
inference(alasca_normalization,[],[f36])).
tff(f36,plain,(
$greater($sum($sum($sum(1,$uminus(sK3)),sK3),-1),0) | ~spl4_2),
inference(alasca_fourier_motzkin,[],[f21,f34])).
tff(f34,plain,(
$greater($sum(-1(sK2),sK3),0) | ~spl4_2),
inference(avatar_component_clause,[],[f32])).
tff(f32,definition,(
spl4_2 <=> $greater($sum(-1(sK2),sK3),0)),
introduced(definition,[new_symbols(naming,[spl4_2])],[avatar_definition])).
tff(f21,plain,(
$greater($sum(sK2,$sum(-1(sK3),1)),0)),
inference(alasca_normalization,[],[f17])).
tff(f17,plain,(
~$less(sK2,sK3)),
inference(cnf_transformation,[],[f12])).
tff(f35,plain,(
spl4_1 | spl4_2),
inference(avatar_split_clause,[],[f26,f32,f28])).
tff(f26,plain,(
$greater($sum(-1(sK2),sK3),0) | $greater($sum(sK1,-1(sK3)),0)),
inference(alasca_normalization,[],[f25])).
tff(f25,plain,(
$greater($sum(sK3,-1(sK2)),0) | $greater($sum(-1(sK3),sK1),0) | $greater($sum(1,-1),0)),
inference(alasca_fourier_motzkin,[],[f19,f22])).
tff(f22,plain,(
$greater($sum(1,-1(read(sK0,sK3))),0)),
inference(alasca_normalization,[],[f18])).
tff(f18,plain,(
~$less(0,read(sK0,sK3))),
inference(cnf_transformation,[],[f12])).
tff(f19,plain,(
( ! [X4 : $int] : ($greater(read(sK0,X4),0) | $greater($sum(X4,-1(sK2)),0) | $greater($sum(-1(X4),sK1),0)) )),
inference(alasca_normalization,[],[f15])).
tff(f15,plain,(
( ! [X4 : $int] : ($less(0,read(sK0,X4)) | $less(sK2,X4) | $less(X4,sK1)) )),
inference(cnf_transformation,[],[f12])).
Saturation for DAT335_2
% (3727607)# SZS output start Saturation.
cnf(u30,negated_conjecture,
'$ki_accessible'('$ki_local_world',X1) | teach(X1,X0,cs) | ~teach('$ki_local_world',X0,psych) | ~'$ki_exists_in_world_$i'('$ki_local_world',X0)).
cnf(u25,axiom,
teach(X0,sue,psych) | '$ki_accessible'('$ki_local_world',X0)).
cnf(u24,axiom,
~'$ki_accessible'(X0,X0)).
cnf(u27,axiom,
teach(X0,sK1(X0),cs) | '$ki_accessible'('$ki_local_world',X0)).
cnf(u16,axiom,
'$ki_exists_in_world_$i'(X0,X1)).
cnf(u26,axiom,
teach(X0,mary,psych) | '$ki_accessible'('$ki_local_world',X0)).
cnf(u29,axiom,
teach(X0,john,math) | '$ki_accessible'('$ki_local_world',X0)).
cnf(u31,negated_conjecture,
teach('$ki_local_world',X0,cs) | ~teach('$ki_local_world',X0,psych) | ~'$ki_exists_in_world_$i'('$ki_local_world',X0)).
% (3727607)# SZS output end Saturation.
% (3727607)# SZS output start Definitions and Model Updates.
globally flip the polarity of every occurrence of predicate "'$ki_accessible'"
% (3727607)# SZS output end Definitions and Model Updates.
Finite Model for DAT335_2
tff('declare_$i1',type,'fmb_$i_1':$i).
tff('finite_domain_$i',axiom,
! [X:$i] : (
X = 'fmb_$i_1'
) ).
tff('declare_$ki_world',type,'$ki_world':$tType).
tff('declare_$ki_world1',type,'fmb_$ki_world_1':'$ki_world').
tff('finite_domain_$ki_world',axiom,
! [X:'$ki_world'] : (
X = 'fmb_$ki_world_1'
) ).
tff('declare_$ki_local_world',type,'$ki_local_world':'$ki_world').
tff('$ki_local_world_definition',axiom,'$ki_local_world' = 'fmb_$ki_world_1').
tff(declare_cs,type,cs:$i).
tff(cs_definition,axiom,cs = 'fmb_$i_1').
tff(declare_sue,type,sue:$i).
tff(sue_definition,axiom,sue = 'fmb_$i_1').
tff(declare_mary,type,mary:$i).
tff(mary_definition,axiom,mary = 'fmb_$i_1').
tff(declare_john,type,john:$i).
tff(john_definition,axiom,john = 'fmb_$i_1').
tff(declare_math,type,math:$i).
tff(math_definition,axiom,math = 'fmb_$i_1').
tff(declare_psych,type,psych:$i).
tff(psych_definition,axiom,psych = 'fmb_$i_1').
tff('declare_$ki_accessible',type,'$ki_accessible': ('$ki_world' * '$ki_world') > $o).
tff('predicate_$ki_accessible',axiom,
'$ki_accessible'('fmb_$ki_world_1','fmb_$ki_world_1')
).
tff(declare_teach,type,teach: ('$ki_world' * $i * $i) > $o).
tff(predicate_teach,axiom,
teach('fmb_$ki_world_1','fmb_$i_1','fmb_$i_1')
).
tff('declare_$ki_exists_in_world_$i',type,'$ki_exists_in_world_$i': ('$ki_world' * $i) > $o).
tff('predicate_$ki_exists_in_world_$i',axiom,
'$ki_exists_in_world_$i'('fmb_$ki_world_1','fmb_$i_1')
).
Saturation for SWW469_10
% # SZS output start Saturation.
cnf(u15,hypothesis,
sK0 != sK1).
cnf(u14,hypothesis,
hoare_1310879719gleton).
% # SZS output end Saturation.
% # SZS output start Definitions and Model Updates.
for all inputs,
define induct_false := $false
for all inputs,
define induct_true := $true
for all groundings,
whenever ? [X0 : state,X1 : state] : X0 != X1 is true, set hoare_1310879719gleton to true
% # SZS output end Definitions and Model Updates.
Finite Model for SWW469_10
tff('declare_$i1',type,'fmb_$i_1':$i).
tff('finite_domain_$i',axiom,
! [X:$i] : (
X = 'fmb_$i_1'
) ).
tff(declare_state,type,state:$tType).
tff(declare_state1,type,fmb_state_1:state).
tff(declare_state2,type,fmb_state_2:state).
tff(finite_domain_state,axiom,
! [X:state] : (
X = fmb_state_1 | X = fmb_state_2
) ).
tff(distinct_domain_state,axiom,
fmb_state_1 != fmb_state_2
).
tff(declare_induct_false,type,induct_false: $o).
tff(induct_false_definition,axiom,~induct_false).
tff(declare_induct_true,type,induct_true: $o).
tff(induct_true_definition,axiom,induct_true).
tff(declare_hoare_1310879719gleton,type,hoare_1310879719gleton: $o).
tff(hoare_1310879719gleton_definition,axiom,hoare_1310879719gleton).
Solution for SEU140+2
% SUCCESS: Derivation has unique formula names
% SUCCESS: All derived formulae have parents and inference information
% WARNING: Took the first false root f1401 as the single derivation root
% SUCCESS: Derivation is acyclic
% SUCCESS: Derivation looks like a refutation
% SUCCESS: Negated conjecture f52 is a leaf or CTH from a conjecture
% SUCCESS: Assumptions are propagated
% SUCCESS: Assumptions are discharged
% NOTICE: Took the conjecture f51 as the proved formula
% CPUTIME: 0.07
% SUCCESS: Verified
% SZS status Verified
fof(f1401,plain,(
$false),
inference(subsumption_resolution,[],[f1400,f210])).
fof(f210,plain,(
~disjoint(sK10,sK12)),
inference(cnf_transformation,[],[f134])).
fof(f134,plain,(
~disjoint(sK10,sK12) & disjoint(sK11,sK12) & subset(sK10,sK11)),
inference(skolemisation,[status(esa),new_symbols(skolem,[sK10,sK11,sK12])],[f88,f133])).
fof(f133,plain,(
? [X0,X1,X2] : (~disjoint(X0,X2) & disjoint(X1,X2) & subset(X0,X1)) => (~disjoint(sK10,sK12) & disjoint(sK11,sK12) & subset(sK10,sK11))),
introduced(definition,[],[choice_axiom])).
fof(f88,plain,(
? [X0,X1,X2] : (~disjoint(X0,X2) & disjoint(X1,X2) & subset(X0,X1))),
inference(flattening,[],[f87])).
fof(f87,plain,(
? [X0,X1,X2] : (~disjoint(X0,X2) & (disjoint(X1,X2) & subset(X0,X1)))),
inference(ennf_transformation,[],[f52])).
fof(f52,negated_conjecture,(
~! [X0,X1,X2] : ((disjoint(X1,X2) & subset(X0,X1)) => disjoint(X0,X2))),
inference(negated_conjecture,[status(cth)],[f51])).
fof(f51,conjecture,(
! [X0,X1,X2] : ((disjoint(X1,X2) & subset(X0,X1)) => disjoint(X0,X2))),
file('Problems/SEU/SEU140+2.p',unknown)).
fof(f1400,plain,(
disjoint(sK10,sK12)),
inference(resolution,[],[f1383,f179])).
fof(f179,plain,(
( ! [X0,X1] : (~disjoint(X0,X1) | disjoint(X1,X0)) )),
inference(cnf_transformation,[],[f72])).
fof(f72,plain,(
! [X0,X1] : (disjoint(X1,X0) | ~disjoint(X0,X1))),
inference(ennf_transformation,[],[f27])).
fof(f27,axiom,(
! [X0,X1] : (disjoint(X0,X1) => disjoint(X1,X0))),
file('Problems/SEU/SEU140+2.p',unknown)).
fof(f1383,plain,(
disjoint(sK12,sK10)),
inference(duplicate_literal_removal,[],[f1380])).
fof(f1380,plain,(
disjoint(sK12,sK10) | disjoint(sK12,sK10)),
inference(resolution,[],[f510,f402])).
fof(f402,plain,(
( ! [X0] : (in(sK8(X0,sK10),sK11) | disjoint(X0,sK10)) )),
inference(resolution,[],[f389,f198])).
fof(f198,plain,(
( ! [X0,X1] : (in(sK8(X0,X1),X1) | disjoint(X0,X1)) )),
inference(cnf_transformation,[],[f130])).
fof(f130,plain,(
! [X0,X1] : ((~disjoint(X0,X1) | ! [X2] : (~in(X2,X1) | ~in(X2,X0))) & ((in(sK8(X0,X1),X1) & in(sK8(X0,X1),X0)) | disjoint(X0,X1)))),
inference(skolemisation,[status(esa),new_symbols(skolem,[sK8])],[f82,f129])).
fof(f129,plain,(
! [X0,X1] : (? [X3] : (in(X3,X1) & in(X3,X0)) => (in(sK8(X0,X1),X1) & in(sK8(X0,X1),X0)))),
introduced(definition,[],[choice_axiom])).
fof(f82,plain,(
! [X0,X1] : ((~disjoint(X0,X1) | ! [X2] : (~in(X2,X1) | ~in(X2,X0))) & (? [X3] : (in(X3,X1) & in(X3,X0)) | disjoint(X0,X1)))),
inference(ennf_transformation,[],[f62])).
fof(f62,plain,(
! [X0,X1] : (~(disjoint(X0,X1) & ? [X2] : (in(X2,X1) & in(X2,X0))) & ~(! [X3] : ~(in(X3,X1) & in(X3,X0)) & ~disjoint(X0,X1)))),
inference(rectify,[],[f43])).
fof(f43,axiom,(
! [X0,X1] : (~(disjoint(X0,X1) & ? [X2] : (in(X2,X1) & in(X2,X0))) & ~(! [X2] : ~(in(X2,X1) & in(X2,X0)) & ~disjoint(X0,X1)))),
file('Problems/SEU/SEU140+2.p',unknown)).
fof(f389,plain,(
( ! [X0] : (~in(X0,sK10) | in(X0,sK11)) )),
inference(superposition,[],[f237,f320])).
fof(f320,plain,(
sK11 = set_union2(sK10,sK11)),
inference(resolution,[],[f180,f208])).
fof(f208,plain,(
subset(sK10,sK11)),
inference(cnf_transformation,[],[f134])).
fof(f180,plain,(
( ! [X0,X1] : (~subset(X0,X1) | set_union2(X0,X1) = X1) )),
inference(cnf_transformation,[],[f73])).
fof(f73,plain,(
! [X0,X1] : (set_union2(X0,X1) = X1 | ~subset(X0,X1))),
inference(ennf_transformation,[],[f28])).
fof(f28,axiom,(
! [X0,X1] : (subset(X0,X1) => set_union2(X0,X1) = X1)),
file('Problems/SEU/SEU140+2.p',unknown)).
fof(f237,plain,(
( ! [X0,X1,X4] : (in(X4,set_union2(X0,X1)) | ~in(X4,X0)) )),
inference(equality_resolution,[],[f145])).
fof(f145,plain,(
( ! [X2,X0,X1,X4] : (in(X4,X2) | ~in(X4,X0) | set_union2(X0,X1) != X2) )),
inference(cnf_transformation,[],[f104])).
fof(f104,plain,(
! [X0,X1,X2] : ((set_union2(X0,X1) = X2 | (((~in(sK1(X0,X1,X2),X1) & ~in(sK1(X0,X1,X2),X0)) | ~in(sK1(X0,X1,X2),X2)) & (in(sK1(X0,X1,X2),X1) | in(sK1(X0,X1,X2),X0) | in(sK1(X0,X1,X2),X2)))) & (! [X4] : ((in(X4,X2) | (~in(X4,X1) & ~in(X4,X0))) & (in(X4,X1) | in(X4,X0) | ~in(X4,X2))) | set_union2(X0,X1) != X2))),
inference(skolemisation,[status(esa),new_symbols(skolem,[sK1])],[f102,f103])).
fof(f103,plain,(
! [X0,X1,X2] : (? [X3] : (((~in(X3,X1) & ~in(X3,X0)) | ~in(X3,X2)) & (in(X3,X1) | in(X3,X0) | in(X3,X2))) => (((~in(sK1(X0,X1,X2),X1) & ~in(sK1(X0,X1,X2),X0)) | ~in(sK1(X0,X1,X2),X2)) & (in(sK1(X0,X1,X2),X1) | in(sK1(X0,X1,X2),X0) | in(sK1(X0,X1,X2),X2))))),
introduced(definition,[],[choice_axiom])).
fof(f102,plain,(
! [X0,X1,X2] : ((set_union2(X0,X1) = X2 | ? [X3] : (((~in(X3,X1) & ~in(X3,X0)) | ~in(X3,X2)) & (in(X3,X1) | in(X3,X0) | in(X3,X2)))) & (! [X4] : ((in(X4,X2) | (~in(X4,X1) & ~in(X4,X0))) & (in(X4,X1) | in(X4,X0) | ~in(X4,X2))) | set_union2(X0,X1) != X2))),
inference(rectify,[],[f101])).
fof(f101,plain,(
! [X0,X1,X2] : ((set_union2(X0,X1) = X2 | ? [X3] : (((~in(X3,X1) & ~in(X3,X0)) | ~in(X3,X2)) & (in(X3,X1) | in(X3,X0) | in(X3,X2)))) & (! [X3] : ((in(X3,X2) | (~in(X3,X1) & ~in(X3,X0))) & (in(X3,X1) | in(X3,X0) | ~in(X3,X2))) | set_union2(X0,X1) != X2))),
inference(flattening,[],[f100])).
fof(f100,plain,(
! [X0,X1,X2] : ((set_union2(X0,X1) = X2 | ? [X3] : (((~in(X3,X1) & ~in(X3,X0)) | ~in(X3,X2)) & ((in(X3,X1) | in(X3,X0)) | in(X3,X2)))) & (! [X3] : ((in(X3,X2) | (~in(X3,X1) & ~in(X3,X0))) & ((in(X3,X1) | in(X3,X0)) | ~in(X3,X2))) | set_union2(X0,X1) != X2))),
inference(nnf_transformation,[],[f7])).
fof(f7,axiom,(
! [X0,X1,X2] : (set_union2(X0,X1) = X2 <=> ! [X3] : (in(X3,X2) <=> (in(X3,X1) | in(X3,X0))))),
file('Problems/SEU/SEU140+2.p',unknown)).
fof(f510,plain,(
( ! [X0] : (~in(sK8(sK12,X0),sK11) | disjoint(sK12,X0)) )),
inference(resolution,[],[f454,f197])).
fof(f197,plain,(
( ! [X0,X1] : (in(sK8(X0,X1),X0) | disjoint(X0,X1)) )),
inference(cnf_transformation,[],[f130])).
fof(f454,plain,(
( ! [X0] : (~in(X0,sK12) | ~in(X0,sK11)) )),
inference(resolution,[],[f199,f271])).
fof(f271,plain,(
disjoint(sK12,sK11)),
inference(resolution,[],[f179,f209])).
fof(f209,plain,(
disjoint(sK11,sK12)),
inference(cnf_transformation,[],[f134])).
fof(f199,plain,(
( ! [X2,X0,X1] : (~disjoint(X0,X1) | ~in(X2,X1) | ~in(X2,X0)) )),
inference(cnf_transformation,[],[f130])).
% SZS output end Proof for SEU140+2
Solution for BOO001-1
% SUCCESS: Derivation has unique formula names
% SUCCESS: All derived formulae have parents and inference information
% WARNING: Took the first false root f295 as the single derivation root
% SUCCESS: Derivation is acyclic
% SUCCESS: Derivation looks like a refutation
% SUCCESS: Negated conjecture f6 is a leaf or CTH from a conjecture
% SUCCESS: Assumptions are propagated
% SUCCESS: Assumptions are discharged
% WARNING: Took the negated conjecture f6 as the proved formula
% CPUTIME: 0.06
% SUCCESS: Verified
% SZS status Verified
fof(f295,plain,(
$false),
inference(trivial_inequality_removal,[],[f289])).
fof(f289,plain,(
a != a),
inference(superposition,[],[f6,f224])).
fof(f224,plain,(
( ! [X0] : (inverse(inverse(X0)) = X0) )),
inference(superposition,[],[f5,f158])).
fof(f158,plain,(
( ! [X0,X1] : (multiply(X1,inverse(X1),X0) = X0) )),
inference(forward_demodulation,[],[f146,f25])).
fof(f25,plain,(
( ! [X2,X0] : (multiply(X0,X2,X0) = X0) )),
inference(forward_demodulation,[],[f22,f3])).
fof(f3,axiom,(
( ! [X2,X3] : (multiply(X2,X2,X3) = X2) )),
file('Problems/BOO/BOO001-1.p',unknown)).
fof(f22,plain,(
( ! [X2,X3,X0,X1] : (multiply(X0,X0,multiply(X1,X2,X3)) = multiply(X0,X2,X0)) )),
inference(forward_demodulation,[],[f13,f3])).
fof(f13,plain,(
( ! [X2,X3,X0,X1] : (multiply(X0,X0,multiply(X1,X2,X3)) = multiply(multiply(X0,X0,X1),X2,X0)) )),
inference(superposition,[],[f1,f3])).
fof(f1,axiom,(
( ! [X2,X3,X0,X1,X4] : (multiply(multiply(X0,X1,X2),X3,multiply(X0,X1,X4)) = multiply(X0,X1,multiply(X2,X3,X4))) )),
file('Problems/BOO/BOO001-1.p',unknown)).
fof(f146,plain,(
( ! [X0,X1] : (multiply(X1,inverse(X1),multiply(X0,X1,X0)) = X0) )),
inference(superposition,[],[f7,f119])).
fof(f119,plain,(
( ! [X3,X0,X1] : (multiply(X3,X1,multiply(X0,inverse(X1),X3)) = X3) )),
inference(forward_demodulation,[],[f118,f88])).
fof(f88,plain,(
( ! [X2,X3,X0,X1,X4] : (multiply(X0,X1,multiply(X2,X3,X0)) = multiply(X0,X1,multiply(X2,X3,multiply(X4,X0,inverse(X1))))) )),
inference(forward_demodulation,[],[f86,f28])).
fof(f28,plain,(
( ! [X2,X3,X0,X1] : (multiply(multiply(X0,X1,X2),X3,X0) = multiply(X0,X1,multiply(X2,X3,X0))) )),
inference(superposition,[],[f1,f25])).
fof(f86,plain,(
( ! [X2,X3,X0,X1,X4] : (multiply(multiply(X0,X1,X2),X3,X0) = multiply(X0,X1,multiply(X2,X3,multiply(X4,X0,inverse(X1))))) )),
inference(superposition,[],[f1,f70])).
fof(f70,plain,(
( ! [X2,X0,X1] : (multiply(X0,X2,multiply(X1,X0,inverse(X2))) = X0) )),
inference(forward_demodulation,[],[f38,f2])).
fof(f2,axiom,(
( ! [X2,X3] : (multiply(X3,X2,X2) = X2) )),
file('Problems/BOO/BOO001-1.p',unknown)).
fof(f38,plain,(
( ! [X2,X0,X1] : (multiply(X1,X0,X0) = multiply(X0,X2,multiply(X1,X0,inverse(X2)))) )),
inference(superposition,[],[f7,f5])).
fof(f118,plain,(
( ! [X2,X3,X0,X1] : (multiply(X3,X1,multiply(X0,inverse(X1),multiply(X2,X3,inverse(X1)))) = X3) )),
inference(superposition,[],[f70,f12])).
fof(f12,plain,(
( ! [X2,X3,X0,X1] : (multiply(X1,X0,multiply(X2,X3,X0)) = multiply(multiply(X1,X0,X2),X3,X0)) )),
inference(superposition,[],[f1,f2])).
fof(f7,plain,(
( ! [X2,X3,X0,X1] : (multiply(X1,X0,multiply(X0,X2,X3)) = multiply(X0,X2,multiply(X1,X0,X3))) )),
inference(superposition,[],[f1,f2])).
fof(f5,axiom,(
( ! [X2,X3] : (multiply(X2,X3,inverse(X3)) = X2) )),
file('Problems/BOO/BOO001-1.p',unknown)).
fof(f6,negated_conjecture,(
a != inverse(inverse(a))),
file('Problems/BOO/BOO001-1.p',unknown)).
Zipperposition 2.1.9999
Jasmin Blanchette
Ludwig-Maximilians-Universität München
Solution for SET014^4
thf(sk__6_type,type,
sk__6: $i ).
thf(sk__4_type,type,
sk__4: $i > $o ).
thf(union_type,type,
union: ( $i > $o ) > ( $i > $o ) > $i > $o ).
thf(sk__3_type,type,
sk__3: $i > $o ).
thf(sk__5_type,type,
sk__5: $i > $o ).
thf(subset_type,type,
subset: ( $i > $o ) > ( $i > $o ) > $o ).
thf(subset,axiom,
( subset
= ( ^ [X: $i > $o,Y: $i > $o] :
! [U: $i] :
( ( X @ U )
=> ( Y @ U ) ) ) ) ).
thf('0',plain,
( subset
= ( ^ [X: $i > $o,Y: $i > $o] :
! [U: $i] :
( ( X @ U )
=> ( Y @ U ) ) ) ),
inference(simplify_rw_rule,[status(thm)],[subset]) ).
thf('1',plain,
( subset
= ( ^ [V_1: $i > $o,V_2: $i > $o] :
! [X4: $i] :
( ( V_1 @ X4 )
=> ( V_2 @ X4 ) ) ) ),
define([status(thm)]) ).
thf(union,axiom,
( union
= ( ^ [X: $i > $o,Y: $i > $o,U: $i] :
( ( X @ U )
| ( Y @ U ) ) ) ) ).
thf('2',plain,
( union
= ( ^ [X: $i > $o,Y: $i > $o,U: $i] :
( ( X @ U )
| ( Y @ U ) ) ) ),
inference(simplify_rw_rule,[status(thm)],[union]) ).
thf('3',plain,
( union
= ( ^ [V_1: $i > $o,V_2: $i > $o,V_3: $i] :
( ( V_1 @ V_3 )
| ( V_2 @ V_3 ) ) ) ),
define([status(thm)]) ).
thf(thm,conjecture,
! [X: $i > $o,Y: $i > $o,A: $i > $o] :
( ( ( subset @ X @ A )
& ( subset @ Y @ A ) )
=> ( subset @ ( union @ X @ Y ) @ A ) ) ).
thf(zf_stmt_0,conjecture,
! [X4: $i > $o,X6: $i > $o,X8: $i > $o] :
( ( ! [X10: $i] :
( ( X4 @ X10 )
=> ( X8 @ X10 ) )
& ! [X12: $i] :
( ( X6 @ X12 )
=> ( X8 @ X12 ) ) )
=> ! [X14: $i] :
( ( ( X4 @ X14 )
| ( X6 @ X14 ) )
=> ( X8 @ X14 ) ) ) ).
thf(zf_stmt_1,negated_conjecture,
~ ! [X4: $i > $o,X6: $i > $o,X8: $i > $o] :
( ( ! [X10: $i] :
( ( X4 @ X10 )
=> ( X8 @ X10 ) )
& ! [X12: $i] :
( ( X6 @ X12 )
=> ( X8 @ X12 ) ) )
=> ! [X14: $i] :
( ( ( X4 @ X14 )
| ( X6 @ X14 ) )
=> ( X8 @ X14 ) ) ),
inference('cnf.neg',[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl2,plain,
~ ( sk__5 @ sk__6 ),
inference(cnf,[status(esa)],[zf_stmt_1]) ).
thf(zip_derived_cl3,plain,
( ( sk__3 @ sk__6 )
| ( sk__4 @ sk__6 ) ),
inference(cnf,[status(esa)],[zf_stmt_1]) ).
thf(zip_derived_cl1,plain,
! [X1: $i] :
( ( sk__5 @ X1 )
| ~ ( sk__4 @ X1 ) ),
inference(cnf,[status(esa)],[zf_stmt_1]) ).
thf(zip_derived_cl5,plain,
( ( sk__3 @ sk__6 )
| ( sk__5 @ sk__6 ) ),
inference('sup-',[status(thm)],[zip_derived_cl3,zip_derived_cl1]) ).
thf(zip_derived_cl2_001,plain,
~ ( sk__5 @ sk__6 ),
inference(cnf,[status(esa)],[zf_stmt_1]) ).
thf(zip_derived_cl8,plain,
sk__3 @ sk__6,
inference(demod,[status(thm)],[zip_derived_cl5,zip_derived_cl2]) ).
thf(zip_derived_cl0,plain,
! [X0: $i] :
( ( sk__5 @ X0 )
| ~ ( sk__3 @ X0 ) ),
inference(cnf,[status(esa)],[zf_stmt_1]) ).
thf(zip_derived_cl12,plain,
sk__5 @ sk__6,
inference('sup-',[status(thm)],[zip_derived_cl8,zip_derived_cl0]) ).
thf(zip_derived_cl16,plain,
$false,
inference(demod,[status(thm)],[zip_derived_cl2,zip_derived_cl12]) ).
Solution for SEU140+2
thf(sk__11_type,type,
sk__11: $i ).
thf(sk__8_type,type,
sk__8: $i > $i > $i ).
thf(sk__10_type,type,
sk__10: $i ).
thf(in_type,type,
in: $i > $i > $o ).
thf(disjoint_type,type,
disjoint: $i > $i > $o ).
thf(empty_set_type,type,
empty_set: $i ).
thf(sk__type,type,
sk_: $i > $i ).
thf(sk__12_type,type,
sk__12: $i ).
thf(subset_type,type,
subset: $i > $i > $o ).
thf(set_intersection2_type,type,
set_intersection2: $i > $i > $i ).
thf(d1_xboole_0,axiom,
! [A: $i] :
( ( A = empty_set )
<=> ! [B: $i] :
~ ( in @ B @ A ) ) ).
thf(zip_derived_cl8,plain,
! [X0: $i] :
( ( X0 = empty_set )
| ( in @ ( sk_ @ X0 ) @ X0 ) ),
inference(cnf,[status(esa)],[d1_xboole_0]) ).
thf(t63_xboole_1,conjecture,
! [A: $i,B: $i,C: $i] :
( ( ( subset @ A @ B )
& ( disjoint @ B @ C ) )
=> ( disjoint @ A @ C ) ) ).
thf(zf_stmt_0,negated_conjecture,
~ ! [A: $i,B: $i,C: $i] :
( ( ( subset @ A @ B )
& ( disjoint @ B @ C ) )
=> ( disjoint @ A @ C ) ),
inference('cnf.neg',[status(esa)],[t63_xboole_1]) ).
thf(zip_derived_cl81,plain,
subset @ sk__10 @ sk__11,
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl80,plain,
disjoint @ sk__11 @ sk__12,
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(d7_xboole_0,axiom,
! [A: $i,B: $i] :
( ( disjoint @ A @ B )
<=> ( ( set_intersection2 @ A @ B )
= empty_set ) ) ).
thf(zip_derived_cl30,plain,
! [X0: $i,X1: $i] :
( ( ( set_intersection2 @ X0 @ X1 )
= empty_set )
| ~ ( disjoint @ X0 @ X1 ) ),
inference(cnf,[status(esa)],[d7_xboole_0]) ).
thf(zip_derived_cl571,plain,
( ( set_intersection2 @ sk__11 @ sk__12 )
= empty_set ),
inference('s_sup-',[status(thm)],[zip_derived_cl80,zip_derived_cl30]) ).
thf(t26_xboole_1,axiom,
! [A: $i,B: $i,C: $i] :
( ( subset @ A @ B )
=> ( subset @ ( set_intersection2 @ A @ C ) @ ( set_intersection2 @ B @ C ) ) ) ).
thf(zip_derived_cl56,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( subset @ X0 @ X1 )
| ( subset @ ( set_intersection2 @ X0 @ X2 ) @ ( set_intersection2 @ X1 @ X2 ) ) ),
inference(cnf,[status(esa)],[t26_xboole_1]) ).
thf(zip_derived_cl765,plain,
! [X0: $i] :
( ~ ( subset @ X0 @ sk__11 )
| ( subset @ ( set_intersection2 @ X0 @ sk__12 ) @ empty_set ) ),
inference('s_sup+',[status(thm)],[zip_derived_cl571,zip_derived_cl56]) ).
thf(t28_xboole_1,axiom,
! [A: $i,B: $i] :
( ( subset @ A @ B )
=> ( ( set_intersection2 @ A @ B )
= A ) ) ).
thf(zip_derived_cl57,plain,
! [X0: $i,X1: $i] :
( ( ( set_intersection2 @ X0 @ X1 )
= X0 )
| ~ ( subset @ X0 @ X1 ) ),
inference(cnf,[status(esa)],[t28_xboole_1]) ).
thf(commutativity_k3_xboole_0,axiom,
! [A: $i,B: $i] :
( ( set_intersection2 @ A @ B )
= ( set_intersection2 @ B @ A ) ) ).
thf(zip_derived_cl3,plain,
! [X0: $i,X1: $i] :
( ( set_intersection2 @ X1 @ X0 )
= ( set_intersection2 @ X0 @ X1 ) ),
inference(cnf,[status(esa)],[commutativity_k3_xboole_0]) ).
thf(t4_xboole_0,axiom,
! [A: $i,B: $i] :
( ~ ( ? [C: $i] : ( in @ C @ ( set_intersection2 @ A @ B ) )
& ( disjoint @ A @ B ) )
& ~ ( ~ ( disjoint @ A @ B )
& ! [C: $i] :
~ ( in @ C @ ( set_intersection2 @ A @ B ) ) ) ) ).
thf(zip_derived_cl77,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( in @ X0 @ ( set_intersection2 @ X1 @ X2 ) )
| ~ ( disjoint @ X1 @ X2 ) ),
inference(cnf,[status(esa)],[t4_xboole_0]) ).
thf(zip_derived_cl417,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( in @ X2 @ ( set_intersection2 @ X1 @ X0 ) )
| ~ ( disjoint @ X0 @ X1 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl3,zip_derived_cl77]) ).
thf(zip_derived_cl644,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ ( subset @ X0 @ X1 )
| ~ ( in @ X2 @ X0 )
| ~ ( disjoint @ X1 @ X0 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl57,zip_derived_cl417]) ).
thf(zip_derived_cl1458,plain,
! [X0: $i,X1: $i] :
( ~ ( subset @ X0 @ sk__11 )
| ~ ( in @ X1 @ ( set_intersection2 @ X0 @ sk__12 ) )
| ~ ( disjoint @ empty_set @ ( set_intersection2 @ X0 @ sk__12 ) ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl765,zip_derived_cl644]) ).
thf(t3_xboole_0,axiom,
! [A: $i,B: $i] :
( ~ ( ? [C: $i] :
( ( in @ C @ B )
& ( in @ C @ A ) )
& ( disjoint @ A @ B ) )
& ~ ( ~ ( disjoint @ A @ B )
& ! [C: $i] :
~ ( ( in @ C @ A )
& ( in @ C @ B ) ) ) ) ).
thf(zip_derived_cl68,plain,
! [X0: $i,X1: $i] :
( ( disjoint @ X0 @ X1 )
| ( in @ ( sk__8 @ X1 @ X0 ) @ X0 ) ),
inference(cnf,[status(esa)],[t3_xboole_0]) ).
thf(zip_derived_cl7,plain,
! [X0: $i,X1: $i] :
( ~ ( in @ X0 @ X1 )
| ( X1 != empty_set ) ),
inference(cnf,[status(esa)],[d1_xboole_0]) ).
thf(zip_derived_cl373,plain,
! [X0: $i] :
~ ( in @ X0 @ empty_set ),
inference(eq_res,[status(thm)],[zip_derived_cl7]) ).
thf(zip_derived_cl862,plain,
! [X0: $i] : ( disjoint @ empty_set @ X0 ),
inference('s_sup-',[status(thm)],[zip_derived_cl68,zip_derived_cl373]) ).
thf(zip_derived_cl1475,plain,
! [X0: $i,X1: $i] :
( ~ ( subset @ X0 @ sk__11 )
| ~ ( in @ X1 @ ( set_intersection2 @ X0 @ sk__12 ) ) ),
inference(demod,[status(thm)],[zip_derived_cl1458,zip_derived_cl862]) ).
thf(zip_derived_cl1484,plain,
! [X0: $i] :
~ ( in @ X0 @ ( set_intersection2 @ sk__10 @ sk__12 ) ),
inference('s_sup-',[status(thm)],[zip_derived_cl81,zip_derived_cl1475]) ).
thf(zip_derived_cl1519,plain,
( ( set_intersection2 @ sk__10 @ sk__12 )
= empty_set ),
inference('s_sup-',[status(thm)],[zip_derived_cl8,zip_derived_cl1484]) ).
thf(zip_derived_cl31,plain,
! [X0: $i,X1: $i] :
( ( disjoint @ X0 @ X1 )
| ( ( set_intersection2 @ X0 @ X1 )
!= empty_set ) ),
inference(cnf,[status(esa)],[d7_xboole_0]) ).
thf(zip_derived_cl79,plain,
~ ( disjoint @ sk__10 @ sk__12 ),
inference(cnf,[status(esa)],[zf_stmt_0]) ).
thf(zip_derived_cl524,plain,
( ( set_intersection2 @ sk__10 @ sk__12 )
!= empty_set ),
inference('s_sup-',[status(thm)],[zip_derived_cl31,zip_derived_cl79]) ).
thf(zip_derived_cl1542,plain,
$false,
inference('simplify_reflect-',[status(thm)],[zip_derived_cl1519,zip_derived_cl524]) ).