%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU369+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 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 : Tue Sep 29 12:48:34 PM UTC 2026
% Result : Theorem 9.37s 2.22s
% Output : Refutation 11.65s
% Verified :
% SZS Type : Refutation
% Derivation depth : 39
% Number of leaves : 16
% Syntax : Number of formulae : 170 ( 32 unt; 3 def)
% Number of atoms : 652 ( 75 equ)
% Maximal formula atoms : 16 ( 3 avg)
% Number of connectives : 835 ( 353 ~; 373 |; 73 &)
% ( 17 <=>; 18 =>; 0 <=; 1 <~>)
% Maximal formula depth : 18 ( 6 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 27 ( 25 usr; 4 prp; 0-3 aty)
% Number of functors : 18 ( 18 usr; 3 con; 0-3 aty)
% Number of variables : 251 ( 0 sgn 236 !; 15 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f94,axiom,
! [X0,X1] :
( ( strict_latt_str(X1)
& latt_str(X1) )
=> ( X1 = boole_lattice(X0)
<=> ( the_carrier(X1) = powerset(X0)
& ! [X2] :
( element(X2,powerset(X0))
=> ! [X3] :
( element(X3,powerset(X0))
=> ( apply_binary(the_L_join(X1),X2,X3) = subset_union2(X0,X2,X3)
& apply_binary(the_L_meet(X1),X2,X3) = subset_intersection2(X0,X2,X3) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d1_lattice3) ).
fof(f128,axiom,
! [X0] : boole_POSet(X0) = poset_of_lattice(boole_lattice(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d2_yellow_1) ).
fof(f131,axiom,
! [X0] :
( ( ~ empty_carrier(X0)
& lattice(X0)
& latt_str(X0) )
=> ! [X1] :
( element(X1,the_carrier(X0))
=> cast_to_el_of_LattPOSet(X0,X1) = X1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d3_lattice3) ).
fof(f140,axiom,
! [X0] :
( ( ~ empty_carrier(X0)
& lattice(X0)
& latt_str(X0) )
=> ! [X1] :
( element(X1,the_carrier(poset_of_lattice(X0)))
=> cast_to_el_of_lattice(X0,X1) = X1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d4_lattice3) ).
fof(f194,axiom,
! [X0] :
( strict_latt_str(boole_lattice(X0))
& latt_str(boole_lattice(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k1_lattice3) ).
fof(f243,axiom,
! [X0,X1] :
( ( ~ empty_carrier(X0)
& lattice(X0)
& latt_str(X0)
& element(X1,the_carrier(poset_of_lattice(X0))) )
=> element(cast_to_el_of_lattice(X0,X1),the_carrier(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k5_lattice3) ).
fof(f347,axiom,
! [X0] :
( ~ empty_carrier(boole_lattice(X0))
& strict_latt_str(boole_lattice(X0))
& join_commutative(boole_lattice(X0))
& join_associative(boole_lattice(X0))
& meet_commutative(boole_lattice(X0))
& meet_associative(boole_lattice(X0))
& meet_absorbing(boole_lattice(X0))
& join_absorbing(boole_lattice(X0))
& lattice(boole_lattice(X0))
& distributive_lattstr(boole_lattice(X0))
& modular_lattstr(boole_lattice(X0))
& lower_bounded_semilattstr(boole_lattice(X0))
& upper_bounded_semilattstr(boole_lattice(X0))
& bounded_lattstr(boole_lattice(X0))
& complemented_lattstr(boole_lattice(X0))
& boolean_lattstr(boole_lattice(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc3_lattice3) ).
fof(f462,axiom,
! [X0] : k1_pcomps_1(X0) = powerset(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k1_pcomps_1) ).
fof(f483,axiom,
! [X0,X1,X2] :
( ( ~ empty_carrier(X0)
& meet_commutative(X0)
& meet_absorbing(X0)
& join_absorbing(X0)
& latt_str(X0)
& element(X1,the_carrier(X0))
& element(X2,the_carrier(X0)) )
=> ( below_refl(X0,X1,X2)
<=> below(X0,X1,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_r3_lattices) ).
fof(f629,axiom,
! [X0,X1] :
( element(X1,the_carrier(boole_lattice(X0)))
=> ! [X2] :
( element(X2,the_carrier(boole_lattice(X0)))
=> ( below(boole_lattice(X0),X1,X2)
<=> subset(X1,X2) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2_lattice3) ).
fof(f634,conjecture,
! [X0,X1] :
( element(X1,the_carrier(boole_POSet(X0)))
=> ! [X2] :
( element(X2,the_carrier(boole_POSet(X0)))
=> ( related_reflexive(boole_POSet(X0),X1,X2)
<=> subset(X1,X2) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2_yellow_1) ).
fof(f635,negated_conjecture,
~ ! [X0,X1] :
( element(X1,the_carrier(boole_POSet(X0)))
=> ! [X2] :
( element(X2,the_carrier(boole_POSet(X0)))
=> ( related_reflexive(boole_POSet(X0),X1,X2)
<=> subset(X1,X2) ) ) ),
inference(negated_conjecture,[status(cth)],[f634]) ).
fof(f663,axiom,
! [X0,X1] :
( element(X0,powerset(X1))
<=> subset(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t3_subset) ).
fof(f733,axiom,
! [X0] :
( ( ~ empty_carrier(X0)
& lattice(X0)
& latt_str(X0) )
=> ! [X1] :
( element(X1,the_carrier(X0))
=> ! [X2] :
( element(X2,the_carrier(X0))
=> ( below_refl(X0,X1,X2)
<=> related_reflexive(poset_of_lattice(X0),cast_to_el_of_LattPOSet(X0,X1),cast_to_el_of_LattPOSet(X0,X2)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t7_lattice3) ).
fof(f937,plain,
! [X0,X1] :
( ( X1 = boole_lattice(X0)
<=> ( the_carrier(X1) = powerset(X0)
& ! [X2] :
( ! [X3] :
( ( apply_binary(the_L_join(X1),X2,X3) = subset_union2(X0,X2,X3)
& apply_binary(the_L_meet(X1),X2,X3) = subset_intersection2(X0,X2,X3) )
| ~ element(X3,powerset(X0)) )
| ~ element(X2,powerset(X0)) ) ) )
| ~ strict_latt_str(X1)
| ~ latt_str(X1) ),
inference(ennf_transformation,[],[f94]) ).
fof(f938,plain,
! [X0,X1] :
( ( X1 = boole_lattice(X0)
<=> ( the_carrier(X1) = powerset(X0)
& ! [X2] :
( ! [X3] :
( ( apply_binary(the_L_join(X1),X2,X3) = subset_union2(X0,X2,X3)
& apply_binary(the_L_meet(X1),X2,X3) = subset_intersection2(X0,X2,X3) )
| ~ element(X3,powerset(X0)) )
| ~ element(X2,powerset(X0)) ) ) )
| ~ strict_latt_str(X1)
| ~ latt_str(X1) ),
inference(flattening,[],[f937]) ).
fof(f976,plain,
! [X0] :
( ! [X1] :
( cast_to_el_of_LattPOSet(X0,X1) = X1
| ~ element(X1,the_carrier(X0)) )
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0) ),
inference(ennf_transformation,[],[f131]) ).
fof(f977,plain,
! [X0] :
( ! [X1] :
( cast_to_el_of_LattPOSet(X0,X1) = X1
| ~ element(X1,the_carrier(X0)) )
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0) ),
inference(flattening,[],[f976]) ).
fof(f987,plain,
! [X0] :
( ! [X1] :
( cast_to_el_of_lattice(X0,X1) = X1
| ~ element(X1,the_carrier(poset_of_lattice(X0))) )
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0) ),
inference(ennf_transformation,[],[f140]) ).
fof(f988,plain,
! [X0] :
( ! [X1] :
( cast_to_el_of_lattice(X0,X1) = X1
| ~ element(X1,the_carrier(poset_of_lattice(X0))) )
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0) ),
inference(flattening,[],[f987]) ).
fof(f1087,plain,
! [X0,X1] :
( element(cast_to_el_of_lattice(X0,X1),the_carrier(X0))
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0)
| ~ element(X1,the_carrier(poset_of_lattice(X0))) ),
inference(ennf_transformation,[],[f243]) ).
fof(f1088,plain,
! [X0,X1] :
( element(cast_to_el_of_lattice(X0,X1),the_carrier(X0))
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0)
| ~ element(X1,the_carrier(poset_of_lattice(X0))) ),
inference(flattening,[],[f1087]) ).
fof(f1315,plain,
! [X0,X1,X2] :
( ( below_refl(X0,X1,X2)
<=> below(X0,X1,X2) )
| empty_carrier(X0)
| ~ meet_commutative(X0)
| ~ meet_absorbing(X0)
| ~ join_absorbing(X0)
| ~ latt_str(X0)
| ~ element(X1,the_carrier(X0))
| ~ element(X2,the_carrier(X0)) ),
inference(ennf_transformation,[],[f483]) ).
fof(f1316,plain,
! [X0,X1,X2] :
( ( below_refl(X0,X1,X2)
<=> below(X0,X1,X2) )
| empty_carrier(X0)
| ~ meet_commutative(X0)
| ~ meet_absorbing(X0)
| ~ join_absorbing(X0)
| ~ latt_str(X0)
| ~ element(X1,the_carrier(X0))
| ~ element(X2,the_carrier(X0)) ),
inference(flattening,[],[f1315]) ).
fof(f1540,plain,
! [X0,X1] :
( ! [X2] :
( ( below(boole_lattice(X0),X1,X2)
<=> subset(X1,X2) )
| ~ element(X2,the_carrier(boole_lattice(X0))) )
| ~ element(X1,the_carrier(boole_lattice(X0))) ),
inference(ennf_transformation,[],[f629]) ).
fof(f1544,plain,
? [X0,X1] :
( ? [X2] :
( ( related_reflexive(boole_POSet(X0),X1,X2)
<~> subset(X1,X2) )
& element(X2,the_carrier(boole_POSet(X0))) )
& element(X1,the_carrier(boole_POSet(X0))) ),
inference(ennf_transformation,[],[f635]) ).
fof(f1672,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( below_refl(X0,X1,X2)
<=> related_reflexive(poset_of_lattice(X0),cast_to_el_of_LattPOSet(X0,X1),cast_to_el_of_LattPOSet(X0,X2)) )
| ~ element(X2,the_carrier(X0)) )
| ~ element(X1,the_carrier(X0)) )
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0) ),
inference(ennf_transformation,[],[f733]) ).
fof(f1673,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( below_refl(X0,X1,X2)
<=> related_reflexive(poset_of_lattice(X0),cast_to_el_of_LattPOSet(X0,X1),cast_to_el_of_LattPOSet(X0,X2)) )
| ~ element(X2,the_carrier(X0)) )
| ~ element(X1,the_carrier(X0)) )
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0) ),
inference(flattening,[],[f1672]) ).
fof(f1836,plain,
! [X0,X1] :
( ( ( X1 = boole_lattice(X0)
| powerset(X0) != the_carrier(X1)
| ? [X2] :
( ? [X3] :
( ( apply_binary(the_L_join(X1),X2,X3) != subset_union2(X0,X2,X3)
| apply_binary(the_L_meet(X1),X2,X3) != subset_intersection2(X0,X2,X3) )
& element(X3,powerset(X0)) )
& element(X2,powerset(X0)) ) )
& ( ( the_carrier(X1) = powerset(X0)
& ! [X2] :
( ! [X3] :
( ( apply_binary(the_L_join(X1),X2,X3) = subset_union2(X0,X2,X3)
& apply_binary(the_L_meet(X1),X2,X3) = subset_intersection2(X0,X2,X3) )
| ~ element(X3,powerset(X0)) )
| ~ element(X2,powerset(X0)) ) )
| boole_lattice(X0) != X1 ) )
| ~ strict_latt_str(X1)
| ~ latt_str(X1) ),
inference(nnf_transformation,[],[f938]) ).
fof(f1837,plain,
! [X0,X1] :
( ( ( X1 = boole_lattice(X0)
| powerset(X0) != the_carrier(X1)
| ? [X2] :
( ? [X3] :
( ( apply_binary(the_L_join(X1),X2,X3) != subset_union2(X0,X2,X3)
| apply_binary(the_L_meet(X1),X2,X3) != subset_intersection2(X0,X2,X3) )
& element(X3,powerset(X0)) )
& element(X2,powerset(X0)) ) )
& ( ( the_carrier(X1) = powerset(X0)
& ! [X2] :
( ! [X3] :
( ( apply_binary(the_L_join(X1),X2,X3) = subset_union2(X0,X2,X3)
& apply_binary(the_L_meet(X1),X2,X3) = subset_intersection2(X0,X2,X3) )
| ~ element(X3,powerset(X0)) )
| ~ element(X2,powerset(X0)) ) )
| boole_lattice(X0) != X1 ) )
| ~ strict_latt_str(X1)
| ~ latt_str(X1) ),
inference(flattening,[],[f1836]) ).
fof(f1838,plain,
! [X0,X1] :
( ( ( X1 = boole_lattice(X0)
| powerset(X0) != the_carrier(X1)
| ? [X2] :
( ? [X3] :
( ( apply_binary(the_L_join(X1),X2,X3) != subset_union2(X0,X2,X3)
| apply_binary(the_L_meet(X1),X2,X3) != subset_intersection2(X0,X2,X3) )
& element(X3,powerset(X0)) )
& element(X2,powerset(X0)) ) )
& ( ( the_carrier(X1) = powerset(X0)
& ! [X4] :
( ! [X5] :
( ( apply_binary(the_L_join(X1),X4,X5) = subset_union2(X0,X4,X5)
& apply_binary(the_L_meet(X1),X4,X5) = subset_intersection2(X0,X4,X5) )
| ~ element(X5,powerset(X0)) )
| ~ element(X4,powerset(X0)) ) )
| boole_lattice(X0) != X1 ) )
| ~ strict_latt_str(X1)
| ~ latt_str(X1) ),
inference(rectify,[],[f1837]) ).
fof(f1839,plain,
! [X0,X1] :
( ( ( X1 = boole_lattice(X0)
| powerset(X0) != the_carrier(X1)
| ( ( apply_binary(the_L_join(X1),sK70(X0,X1),sK71(X0,X1)) != subset_union2(X0,sK70(X0,X1),sK71(X0,X1))
| apply_binary(the_L_meet(X1),sK70(X0,X1),sK71(X0,X1)) != subset_intersection2(X0,sK70(X0,X1),sK71(X0,X1)) )
& element(sK71(X0,X1),powerset(X0))
& element(sK70(X0,X1),powerset(X0)) ) )
& ( ( the_carrier(X1) = powerset(X0)
& ! [X4] :
( ! [X5] :
( ( apply_binary(the_L_join(X1),X4,X5) = subset_union2(X0,X4,X5)
& apply_binary(the_L_meet(X1),X4,X5) = subset_intersection2(X0,X4,X5) )
| ~ element(X5,powerset(X0)) )
| ~ element(X4,powerset(X0)) ) )
| boole_lattice(X0) != X1 ) )
| ~ strict_latt_str(X1)
| ~ latt_str(X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK70,sK71]),skolemize(X2,sK70(X0,X1)),skolemize(X3,sK71(X0,X1))],[f1838]) ).
fof(f2122,plain,
! [X0,X1,X2] :
( ( ( below_refl(X0,X1,X2)
| ~ below(X0,X1,X2) )
& ( below(X0,X1,X2)
| ~ below_refl(X0,X1,X2) ) )
| empty_carrier(X0)
| ~ meet_commutative(X0)
| ~ meet_absorbing(X0)
| ~ join_absorbing(X0)
| ~ latt_str(X0)
| ~ element(X1,the_carrier(X0))
| ~ element(X2,the_carrier(X0)) ),
inference(nnf_transformation,[],[f1316]) ).
fof(f2380,plain,
! [X0,X1] :
( ! [X2] :
( ( ( below(boole_lattice(X0),X1,X2)
| ~ subset(X1,X2) )
& ( subset(X1,X2)
| ~ below(boole_lattice(X0),X1,X2) ) )
| ~ element(X2,the_carrier(boole_lattice(X0))) )
| ~ element(X1,the_carrier(boole_lattice(X0))) ),
inference(nnf_transformation,[],[f1540]) ).
fof(f2383,plain,
? [X0,X1] :
( ? [X2] :
( ( ~ subset(X1,X2)
| ~ related_reflexive(boole_POSet(X0),X1,X2) )
& ( subset(X1,X2)
| related_reflexive(boole_POSet(X0),X1,X2) )
& element(X2,the_carrier(boole_POSet(X0))) )
& element(X1,the_carrier(boole_POSet(X0))) ),
inference(nnf_transformation,[],[f1544]) ).
fof(f2384,plain,
? [X0,X1] :
( ? [X2] :
( ( ~ subset(X1,X2)
| ~ related_reflexive(boole_POSet(X0),X1,X2) )
& ( subset(X1,X2)
| related_reflexive(boole_POSet(X0),X1,X2) )
& element(X2,the_carrier(boole_POSet(X0))) )
& element(X1,the_carrier(boole_POSet(X0))) ),
inference(flattening,[],[f2383]) ).
fof(f2385,plain,
( ( ~ subset(sK520,sK521)
| ~ related_reflexive(boole_POSet(sK519),sK520,sK521) )
& ( subset(sK520,sK521)
| related_reflexive(boole_POSet(sK519),sK520,sK521) )
& element(sK521,the_carrier(boole_POSet(sK519)))
& element(sK520,the_carrier(boole_POSet(sK519))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK519,sK520,sK521]),skolemize(X0,sK519),skolemize(X1,sK520),skolemize(X2,sK521)],[f2384]) ).
fof(f2408,plain,
! [X0,X1] :
( ( element(X0,powerset(X1))
| ~ subset(X0,X1) )
& ( subset(X0,X1)
| ~ element(X0,powerset(X1)) ) ),
inference(nnf_transformation,[],[f663]) ).
fof(f2440,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( below_refl(X0,X1,X2)
| ~ related_reflexive(poset_of_lattice(X0),cast_to_el_of_LattPOSet(X0,X1),cast_to_el_of_LattPOSet(X0,X2)) )
& ( related_reflexive(poset_of_lattice(X0),cast_to_el_of_LattPOSet(X0,X1),cast_to_el_of_LattPOSet(X0,X2))
| ~ below_refl(X0,X1,X2) ) )
| ~ element(X2,the_carrier(X0)) )
| ~ element(X1,the_carrier(X0)) )
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0) ),
inference(nnf_transformation,[],[f1673]) ).
fof(f2740,plain,
! [X0,X1] :
( powerset(X0) = the_carrier(X1)
| boole_lattice(X0) != X1
| ~ strict_latt_str(X1)
| ~ latt_str(X1) ),
inference(cnf_transformation,[],[f1839]) ).
fof(f2878,plain,
! [X0] : boole_POSet(X0) = poset_of_lattice(boole_lattice(X0)),
inference(cnf_transformation,[],[f128]) ).
fof(f2895,plain,
! [X0,X1] :
( ~ lattice(X0)
| ~ element(X1,the_carrier(X0))
| empty_carrier(X0)
| cast_to_el_of_LattPOSet(X0,X1) = X1
| ~ latt_str(X0) ),
inference(cnf_transformation,[],[f977]) ).
fof(f2926,plain,
! [X0,X1] :
( ~ lattice(X0)
| ~ element(X1,the_carrier(poset_of_lattice(X0)))
| empty_carrier(X0)
| cast_to_el_of_lattice(X0,X1) = X1
| ~ latt_str(X0) ),
inference(cnf_transformation,[],[f988]) ).
fof(f3131,plain,
! [X0] : latt_str(boole_lattice(X0)),
inference(cnf_transformation,[],[f194]) ).
fof(f3178,plain,
! [X0,X1] :
( ~ lattice(X0)
| empty_carrier(X0)
| element(cast_to_el_of_lattice(X0,X1),the_carrier(X0))
| ~ latt_str(X0)
| ~ element(X1,the_carrier(poset_of_lattice(X0))) ),
inference(cnf_transformation,[],[f1088]) ).
fof(f3407,plain,
! [X0] : lattice(boole_lattice(X0)),
inference(cnf_transformation,[],[f347]) ).
fof(f3408,plain,
! [X0] : join_absorbing(boole_lattice(X0)),
inference(cnf_transformation,[],[f347]) ).
fof(f3409,plain,
! [X0] : meet_absorbing(boole_lattice(X0)),
inference(cnf_transformation,[],[f347]) ).
fof(f3411,plain,
! [X0] : meet_commutative(boole_lattice(X0)),
inference(cnf_transformation,[],[f347]) ).
fof(f3414,plain,
! [X0] : strict_latt_str(boole_lattice(X0)),
inference(cnf_transformation,[],[f347]) ).
fof(f3415,plain,
! [X0] : ~ empty_carrier(boole_lattice(X0)),
inference(cnf_transformation,[],[f347]) ).
fof(f3826,plain,
! [X0] : powerset(X0) = k1_pcomps_1(X0),
inference(cnf_transformation,[],[f462]) ).
fof(f3850,plain,
! [X2,X0,X1] :
( ~ join_absorbing(X0)
| ~ below_refl(X0,X1,X2)
| empty_carrier(X0)
| ~ meet_commutative(X0)
| ~ meet_absorbing(X0)
| below(X0,X1,X2)
| ~ latt_str(X0)
| ~ element(X1,the_carrier(X0))
| ~ element(X2,the_carrier(X0)) ),
inference(cnf_transformation,[],[f2122]) ).
fof(f3851,plain,
! [X2,X0,X1] :
( ~ join_absorbing(X0)
| ~ below(X0,X1,X2)
| empty_carrier(X0)
| ~ meet_commutative(X0)
| ~ meet_absorbing(X0)
| below_refl(X0,X1,X2)
| ~ latt_str(X0)
| ~ element(X1,the_carrier(X0))
| ~ element(X2,the_carrier(X0)) ),
inference(cnf_transformation,[],[f2122]) ).
fof(f4533,plain,
! [X2,X0,X1] :
( ~ below(boole_lattice(X0),X1,X2)
| subset(X1,X2)
| ~ element(X2,the_carrier(boole_lattice(X0)))
| ~ element(X1,the_carrier(boole_lattice(X0))) ),
inference(cnf_transformation,[],[f2380]) ).
fof(f4534,plain,
! [X2,X0,X1] :
( ~ subset(X1,X2)
| below(boole_lattice(X0),X1,X2)
| ~ element(X2,the_carrier(boole_lattice(X0)))
| ~ element(X1,the_carrier(boole_lattice(X0))) ),
inference(cnf_transformation,[],[f2380]) ).
fof(f4540,plain,
element(sK520,the_carrier(boole_POSet(sK519))),
inference(cnf_transformation,[],[f2385]) ).
fof(f4541,plain,
element(sK521,the_carrier(boole_POSet(sK519))),
inference(cnf_transformation,[],[f2385]) ).
fof(f4542,plain,
( subset(sK520,sK521)
| related_reflexive(boole_POSet(sK519),sK520,sK521) ),
inference(cnf_transformation,[],[f2385]) ).
fof(f4543,plain,
( ~ subset(sK520,sK521)
| ~ related_reflexive(boole_POSet(sK519),sK520,sK521) ),
inference(cnf_transformation,[],[f2385]) ).
fof(f4603,plain,
! [X0,X1] :
( subset(X0,X1)
| ~ element(X0,powerset(X1)) ),
inference(cnf_transformation,[],[f2408]) ).
fof(f4604,plain,
! [X0,X1] :
( element(X0,powerset(X1))
| ~ subset(X0,X1) ),
inference(cnf_transformation,[],[f2408]) ).
fof(f4734,plain,
! [X2,X0,X1] :
( ~ lattice(X0)
| ~ below_refl(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ~ element(X1,the_carrier(X0))
| empty_carrier(X0)
| related_reflexive(poset_of_lattice(X0),cast_to_el_of_LattPOSet(X0,X1),cast_to_el_of_LattPOSet(X0,X2))
| ~ latt_str(X0) ),
inference(cnf_transformation,[],[f2440]) ).
fof(f4735,plain,
! [X2,X0,X1] :
( ~ related_reflexive(poset_of_lattice(X0),cast_to_el_of_LattPOSet(X0,X1),cast_to_el_of_LattPOSet(X0,X2))
| below_refl(X0,X1,X2)
| ~ element(X2,the_carrier(X0))
| ~ element(X1,the_carrier(X0))
| empty_carrier(X0)
| ~ lattice(X0)
| ~ latt_str(X0) ),
inference(cnf_transformation,[],[f2440]) ).
fof(f4846,plain,
! [X0,X1] :
( the_carrier(X1) = k1_pcomps_1(X0)
| boole_lattice(X0) != X1
| ~ strict_latt_str(X1)
| ~ latt_str(X1) ),
inference(definition_unfolding,[],[f2740,f3826]) ).
fof(f5499,plain,
( ~ subset(sK520,sK521)
| ~ related_reflexive(poset_of_lattice(boole_lattice(sK519)),sK520,sK521) ),
inference(definition_unfolding,[],[f4543,f2878]) ).
fof(f5500,plain,
( subset(sK520,sK521)
| related_reflexive(poset_of_lattice(boole_lattice(sK519)),sK520,sK521) ),
inference(definition_unfolding,[],[f4542,f2878]) ).
fof(f5501,plain,
element(sK521,the_carrier(poset_of_lattice(boole_lattice(sK519)))),
inference(definition_unfolding,[],[f4541,f2878]) ).
fof(f5502,plain,
element(sK520,the_carrier(poset_of_lattice(boole_lattice(sK519)))),
inference(definition_unfolding,[],[f4540,f2878]) ).
fof(f5521,plain,
! [X0,X1] :
( element(X0,k1_pcomps_1(X1))
| ~ subset(X0,X1) ),
inference(definition_unfolding,[],[f4604,f3826]) ).
fof(f5522,plain,
! [X0,X1] :
( ~ element(X0,k1_pcomps_1(X1))
| subset(X0,X1) ),
inference(definition_unfolding,[],[f4603,f3826]) ).
fof(f5638,plain,
! [X0] :
( k1_pcomps_1(X0) = the_carrier(boole_lattice(X0))
| ~ strict_latt_str(boole_lattice(X0))
| ~ latt_str(boole_lattice(X0)) ),
inference(equality_resolution,[],[f4846]) ).
fof(f5934,definition,
( spl542_5
<=> related_reflexive(poset_of_lattice(boole_lattice(sK519)),sK520,sK521) ),
introduced(definition,[new_symbols(definition,[spl542_5])],[avatar_definition]) ).
fof(f5935,plain,
( related_reflexive(poset_of_lattice(boole_lattice(sK519)),sK520,sK521)
| ~ spl542_5 ),
inference(avatar_component_clause,[],[f5934]) ).
fof(f5937,definition,
( spl542_6
<=> subset(sK520,sK521) ),
introduced(definition,[new_symbols(definition,[spl542_6])],[avatar_definition]) ).
fof(f5938,plain,
( subset(sK520,sK521)
| ~ spl542_6 ),
inference(avatar_component_clause,[],[f5937]) ).
fof(f5939,plain,
( spl542_5
| spl542_6 ),
inference(avatar_split_clause,[],[f5500,f5937,f5934]) ).
fof(f5940,plain,
( ~ related_reflexive(poset_of_lattice(boole_lattice(sK519)),sK520,sK521)
| spl542_5 ),
inference(avatar_component_clause,[],[f5934]) ).
fof(f5941,plain,
( ~ subset(sK520,sK521)
| spl542_6 ),
inference(avatar_component_clause,[],[f5937]) ).
fof(f5942,plain,
( ~ spl542_5
| ~ spl542_6 ),
inference(avatar_split_clause,[],[f5499,f5937,f5934]) ).
fof(f6288,plain,
! [X0] :
( k1_pcomps_1(X0) = the_carrier(boole_lattice(X0))
| ~ latt_str(boole_lattice(X0)) ),
inference(forward_subsumption_resolution,[],[f5638,f3414]) ).
fof(f6329,plain,
! [X0] : k1_pcomps_1(X0) = the_carrier(boole_lattice(X0)),
inference(forward_subsumption_resolution,[],[f6288,f3131]) ).
fof(f6341,plain,
! [X0,X1] :
( ~ element(X0,the_carrier(boole_lattice(X1)))
| empty_carrier(boole_lattice(X1))
| cast_to_el_of_LattPOSet(boole_lattice(X1),X0) = X0
| ~ latt_str(boole_lattice(X1)) ),
inference(resolution,[],[f3407,f2895]) ).
fof(f6342,plain,
! [X2,X0,X1] :
( ~ below_refl(boole_lattice(X0),X1,X2)
| ~ element(X2,the_carrier(boole_lattice(X0)))
| ~ element(X1,the_carrier(boole_lattice(X0)))
| empty_carrier(boole_lattice(X0))
| related_reflexive(poset_of_lattice(boole_lattice(X0)),cast_to_el_of_LattPOSet(boole_lattice(X0),X1),cast_to_el_of_LattPOSet(boole_lattice(X0),X2))
| ~ latt_str(boole_lattice(X0)) ),
inference(resolution,[],[f3407,f4734]) ).
fof(f6343,plain,
! [X2,X0,X1] :
( ~ below_refl(boole_lattice(X0),X1,X2)
| ~ element(X2,the_carrier(boole_lattice(X0)))
| ~ element(X1,the_carrier(boole_lattice(X0)))
| related_reflexive(poset_of_lattice(boole_lattice(X0)),cast_to_el_of_LattPOSet(boole_lattice(X0),X1),cast_to_el_of_LattPOSet(boole_lattice(X0),X2))
| ~ latt_str(boole_lattice(X0)) ),
inference(forward_subsumption_resolution,[],[f6342,f3415]) ).
fof(f6344,plain,
! [X0,X1] :
( ~ element(X0,the_carrier(boole_lattice(X1)))
| cast_to_el_of_LattPOSet(boole_lattice(X1),X0) = X0
| ~ latt_str(boole_lattice(X1)) ),
inference(forward_subsumption_resolution,[],[f6341,f3415]) ).
fof(f6345,plain,
! [X2,X0,X1] :
( ~ below_refl(boole_lattice(X0),X1,X2)
| ~ element(X2,the_carrier(boole_lattice(X0)))
| ~ element(X1,the_carrier(boole_lattice(X0)))
| related_reflexive(poset_of_lattice(boole_lattice(X0)),cast_to_el_of_LattPOSet(boole_lattice(X0),X1),cast_to_el_of_LattPOSet(boole_lattice(X0),X2)) ),
inference(forward_subsumption_resolution,[],[f6343,f3131]) ).
fof(f6346,plain,
! [X0,X1] :
( ~ element(X0,the_carrier(boole_lattice(X1)))
| cast_to_el_of_LattPOSet(boole_lattice(X1),X0) = X0 ),
inference(forward_subsumption_resolution,[],[f6344,f3131]) ).
fof(f6347,plain,
! [X2,X0,X1] :
( ~ element(X2,k1_pcomps_1(X0))
| ~ below_refl(boole_lattice(X0),X1,X2)
| ~ element(X1,the_carrier(boole_lattice(X0)))
| related_reflexive(poset_of_lattice(boole_lattice(X0)),cast_to_el_of_LattPOSet(boole_lattice(X0),X1),cast_to_el_of_LattPOSet(boole_lattice(X0),X2)) ),
inference(forward_demodulation,[],[f6345,f6329]) ).
fof(f6348,plain,
! [X0,X1] :
( ~ element(X0,k1_pcomps_1(X1))
| cast_to_el_of_LattPOSet(boole_lattice(X1),X0) = X0 ),
inference(forward_demodulation,[],[f6346,f6329]) ).
fof(f6349,plain,
! [X2,X0,X1] :
( ~ element(X2,k1_pcomps_1(X0))
| ~ element(X1,k1_pcomps_1(X0))
| ~ below_refl(boole_lattice(X0),X1,X2)
| related_reflexive(poset_of_lattice(boole_lattice(X0)),cast_to_el_of_LattPOSet(boole_lattice(X0),X1),cast_to_el_of_LattPOSet(boole_lattice(X0),X2)) ),
inference(forward_demodulation,[],[f6347,f6329]) ).
fof(f6390,plain,
! [X2,X0,X1] :
( ~ below_refl(boole_lattice(X0),X1,X2)
| empty_carrier(boole_lattice(X0))
| ~ meet_commutative(boole_lattice(X0))
| ~ meet_absorbing(boole_lattice(X0))
| below(boole_lattice(X0),X1,X2)
| ~ latt_str(boole_lattice(X0))
| ~ element(X1,the_carrier(boole_lattice(X0)))
| ~ element(X2,the_carrier(boole_lattice(X0))) ),
inference(resolution,[],[f3408,f3850]) ).
fof(f6391,plain,
! [X2,X0,X1] :
( ~ below(boole_lattice(X0),X1,X2)
| empty_carrier(boole_lattice(X0))
| ~ meet_commutative(boole_lattice(X0))
| ~ meet_absorbing(boole_lattice(X0))
| below_refl(boole_lattice(X0),X1,X2)
| ~ latt_str(boole_lattice(X0))
| ~ element(X1,the_carrier(boole_lattice(X0)))
| ~ element(X2,the_carrier(boole_lattice(X0))) ),
inference(resolution,[],[f3408,f3851]) ).
fof(f6392,plain,
! [X2,X0,X1] :
( ~ below(boole_lattice(X0),X1,X2)
| ~ meet_commutative(boole_lattice(X0))
| ~ meet_absorbing(boole_lattice(X0))
| below_refl(boole_lattice(X0),X1,X2)
| ~ latt_str(boole_lattice(X0))
| ~ element(X1,the_carrier(boole_lattice(X0)))
| ~ element(X2,the_carrier(boole_lattice(X0))) ),
inference(forward_subsumption_resolution,[],[f6391,f3415]) ).
fof(f6393,plain,
! [X2,X0,X1] :
( ~ below_refl(boole_lattice(X0),X1,X2)
| ~ meet_commutative(boole_lattice(X0))
| ~ meet_absorbing(boole_lattice(X0))
| below(boole_lattice(X0),X1,X2)
| ~ latt_str(boole_lattice(X0))
| ~ element(X1,the_carrier(boole_lattice(X0)))
| ~ element(X2,the_carrier(boole_lattice(X0))) ),
inference(forward_subsumption_resolution,[],[f6390,f3415]) ).
fof(f6394,plain,
! [X2,X0,X1] :
( ~ below(boole_lattice(X0),X1,X2)
| ~ meet_absorbing(boole_lattice(X0))
| below_refl(boole_lattice(X0),X1,X2)
| ~ latt_str(boole_lattice(X0))
| ~ element(X1,the_carrier(boole_lattice(X0)))
| ~ element(X2,the_carrier(boole_lattice(X0))) ),
inference(forward_subsumption_resolution,[],[f6392,f3411]) ).
fof(f6395,plain,
! [X2,X0,X1] :
( ~ below_refl(boole_lattice(X0),X1,X2)
| ~ meet_absorbing(boole_lattice(X0))
| below(boole_lattice(X0),X1,X2)
| ~ latt_str(boole_lattice(X0))
| ~ element(X1,the_carrier(boole_lattice(X0)))
| ~ element(X2,the_carrier(boole_lattice(X0))) ),
inference(forward_subsumption_resolution,[],[f6393,f3411]) ).
fof(f6396,plain,
! [X2,X0,X1] :
( ~ below(boole_lattice(X0),X1,X2)
| below_refl(boole_lattice(X0),X1,X2)
| ~ latt_str(boole_lattice(X0))
| ~ element(X1,the_carrier(boole_lattice(X0)))
| ~ element(X2,the_carrier(boole_lattice(X0))) ),
inference(forward_subsumption_resolution,[],[f6394,f3409]) ).
fof(f6397,plain,
! [X2,X0,X1] :
( ~ below_refl(boole_lattice(X0),X1,X2)
| below(boole_lattice(X0),X1,X2)
| ~ latt_str(boole_lattice(X0))
| ~ element(X1,the_carrier(boole_lattice(X0)))
| ~ element(X2,the_carrier(boole_lattice(X0))) ),
inference(forward_subsumption_resolution,[],[f6395,f3409]) ).
fof(f6398,plain,
! [X2,X0,X1] :
( ~ below(boole_lattice(X0),X1,X2)
| below_refl(boole_lattice(X0),X1,X2)
| ~ element(X1,the_carrier(boole_lattice(X0)))
| ~ element(X2,the_carrier(boole_lattice(X0))) ),
inference(forward_subsumption_resolution,[],[f6396,f3131]) ).
fof(f6399,plain,
! [X2,X0,X1] :
( ~ below_refl(boole_lattice(X0),X1,X2)
| below(boole_lattice(X0),X1,X2)
| ~ element(X1,the_carrier(boole_lattice(X0)))
| ~ element(X2,the_carrier(boole_lattice(X0))) ),
inference(forward_subsumption_resolution,[],[f6397,f3131]) ).
fof(f6400,plain,
! [X2,X0,X1] :
( ~ element(X1,k1_pcomps_1(X0))
| ~ below(boole_lattice(X0),X1,X2)
| below_refl(boole_lattice(X0),X1,X2)
| ~ element(X2,the_carrier(boole_lattice(X0))) ),
inference(forward_demodulation,[],[f6398,f6329]) ).
fof(f6401,plain,
! [X2,X0,X1] :
( ~ element(X1,k1_pcomps_1(X0))
| ~ below_refl(boole_lattice(X0),X1,X2)
| below(boole_lattice(X0),X1,X2)
| ~ element(X2,the_carrier(boole_lattice(X0))) ),
inference(forward_demodulation,[],[f6399,f6329]) ).
fof(f6402,plain,
! [X2,X0,X1] :
( ~ element(X1,k1_pcomps_1(X0))
| ~ element(X2,k1_pcomps_1(X0))
| ~ below(boole_lattice(X0),X1,X2)
| below_refl(boole_lattice(X0),X1,X2) ),
inference(forward_demodulation,[],[f6400,f6329]) ).
fof(f6403,plain,
! [X2,X0,X1] :
( ~ element(X1,k1_pcomps_1(X0))
| ~ element(X2,k1_pcomps_1(X0))
| ~ below_refl(boole_lattice(X0),X1,X2)
| below(boole_lattice(X0),X1,X2) ),
inference(forward_demodulation,[],[f6401,f6329]) ).
fof(f6436,plain,
! [X0,X1] :
( empty_carrier(boole_lattice(X0))
| element(cast_to_el_of_lattice(boole_lattice(X0),X1),the_carrier(boole_lattice(X0)))
| ~ latt_str(boole_lattice(X0))
| ~ element(X1,the_carrier(poset_of_lattice(boole_lattice(X0)))) ),
inference(resolution,[],[f3178,f3407]) ).
fof(f6437,plain,
! [X0,X1] :
( element(cast_to_el_of_lattice(boole_lattice(X0),X1),the_carrier(boole_lattice(X0)))
| ~ latt_str(boole_lattice(X0))
| ~ element(X1,the_carrier(poset_of_lattice(boole_lattice(X0)))) ),
inference(forward_subsumption_resolution,[],[f6436,f3415]) ).
fof(f6438,plain,
! [X0,X1] :
( element(cast_to_el_of_lattice(boole_lattice(X0),X1),the_carrier(boole_lattice(X0)))
| ~ element(X1,the_carrier(poset_of_lattice(boole_lattice(X0)))) ),
inference(forward_subsumption_resolution,[],[f6437,f3131]) ).
fof(f6439,plain,
! [X0,X1] :
( ~ element(X1,the_carrier(poset_of_lattice(boole_lattice(X0))))
| element(cast_to_el_of_lattice(boole_lattice(X0),X1),k1_pcomps_1(X0)) ),
inference(forward_demodulation,[],[f6438,f6329]) ).
fof(f6440,plain,
element(cast_to_el_of_lattice(boole_lattice(sK519),sK521),k1_pcomps_1(sK519)),
inference(resolution,[],[f6439,f5501]) ).
fof(f6441,plain,
element(cast_to_el_of_lattice(boole_lattice(sK519),sK520),k1_pcomps_1(sK519)),
inference(resolution,[],[f6439,f5502]) ).
fof(f6444,plain,
subset(cast_to_el_of_lattice(boole_lattice(sK519),sK520),sK519),
inference(resolution,[],[f6441,f5522]) ).
fof(f6449,plain,
subset(cast_to_el_of_lattice(boole_lattice(sK519),sK521),sK519),
inference(resolution,[],[f6440,f5522]) ).
fof(f6481,plain,
! [X0,X1] :
( ~ subset(X0,X1)
| cast_to_el_of_LattPOSet(boole_lattice(X1),X0) = X0 ),
inference(resolution,[],[f5521,f6348]) ).
fof(f6580,plain,
! [X0,X1] :
( ~ element(X0,the_carrier(poset_of_lattice(boole_lattice(X1))))
| empty_carrier(boole_lattice(X1))
| cast_to_el_of_lattice(boole_lattice(X1),X0) = X0
| ~ latt_str(boole_lattice(X1)) ),
inference(resolution,[],[f2926,f3407]) ).
fof(f6581,plain,
! [X0,X1] :
( ~ element(X0,the_carrier(poset_of_lattice(boole_lattice(X1))))
| cast_to_el_of_lattice(boole_lattice(X1),X0) = X0
| ~ latt_str(boole_lattice(X1)) ),
inference(forward_subsumption_resolution,[],[f6580,f3415]) ).
fof(f6582,plain,
! [X0,X1] :
( ~ element(X0,the_carrier(poset_of_lattice(boole_lattice(X1))))
| cast_to_el_of_lattice(boole_lattice(X1),X0) = X0 ),
inference(forward_subsumption_resolution,[],[f6581,f3131]) ).
fof(f6583,plain,
sK521 = cast_to_el_of_lattice(boole_lattice(sK519),sK521),
inference(resolution,[],[f6582,f5501]) ).
fof(f6584,plain,
sK520 = cast_to_el_of_lattice(boole_lattice(sK519),sK520),
inference(resolution,[],[f6582,f5502]) ).
fof(f6585,plain,
subset(sK520,sK519),
inference(superposition,[],[f6444,f6584]) ).
fof(f6586,plain,
element(sK520,k1_pcomps_1(sK519)),
inference(superposition,[],[f6441,f6584]) ).
fof(f6587,plain,
subset(sK521,sK519),
inference(superposition,[],[f6449,f6583]) ).
fof(f6588,plain,
element(sK521,k1_pcomps_1(sK519)),
inference(superposition,[],[f6440,f6583]) ).
fof(f6590,plain,
sK520 = cast_to_el_of_LattPOSet(boole_lattice(sK519),sK520),
inference(resolution,[],[f6585,f6481]) ).
fof(f6605,plain,
sK521 = cast_to_el_of_LattPOSet(boole_lattice(sK519),sK521),
inference(resolution,[],[f6587,f6481]) ).
fof(f6623,plain,
! [X0] :
( ~ element(X0,k1_pcomps_1(sK519))
| ~ below_refl(boole_lattice(sK519),X0,sK521)
| related_reflexive(poset_of_lattice(boole_lattice(sK519)),cast_to_el_of_LattPOSet(boole_lattice(sK519),X0),cast_to_el_of_LattPOSet(boole_lattice(sK519),sK521)) ),
inference(resolution,[],[f6588,f6349]) ).
fof(f6632,plain,
! [X0] :
( related_reflexive(poset_of_lattice(boole_lattice(sK519)),cast_to_el_of_LattPOSet(boole_lattice(sK519),X0),sK521)
| ~ element(X0,k1_pcomps_1(sK519))
| ~ below_refl(boole_lattice(sK519),X0,sK521) ),
inference(forward_demodulation,[],[f6623,f6605]) ).
fof(f6638,plain,
! [X0] :
( below_refl(boole_lattice(sK519),sK520,X0)
| ~ below(boole_lattice(sK519),sK520,X0)
| ~ element(X0,k1_pcomps_1(sK519)) ),
inference(resolution,[],[f6586,f6402]) ).
fof(f6639,plain,
! [X0] :
( ~ below_refl(boole_lattice(sK519),sK520,X0)
| ~ element(X0,k1_pcomps_1(sK519))
| below(boole_lattice(sK519),sK520,X0) ),
inference(resolution,[],[f6586,f6403]) ).
fof(f6661,plain,
( related_reflexive(poset_of_lattice(boole_lattice(sK519)),sK520,sK521)
| ~ element(sK520,k1_pcomps_1(sK519))
| ~ below_refl(boole_lattice(sK519),sK520,sK521) ),
inference(superposition,[],[f6632,f6590]) ).
fof(f6666,plain,
! [X0] :
( ~ related_reflexive(poset_of_lattice(boole_lattice(sK519)),sK520,cast_to_el_of_LattPOSet(boole_lattice(sK519),X0))
| below_refl(boole_lattice(sK519),sK520,X0)
| ~ element(X0,the_carrier(boole_lattice(sK519)))
| ~ element(sK520,the_carrier(boole_lattice(sK519)))
| empty_carrier(boole_lattice(sK519))
| ~ lattice(boole_lattice(sK519))
| ~ latt_str(boole_lattice(sK519)) ),
inference(superposition,[],[f4735,f6590]) ).
fof(f6667,plain,
! [X0] :
( ~ related_reflexive(poset_of_lattice(boole_lattice(sK519)),sK520,cast_to_el_of_LattPOSet(boole_lattice(sK519),X0))
| below_refl(boole_lattice(sK519),sK520,X0)
| ~ element(X0,the_carrier(boole_lattice(sK519)))
| ~ element(sK520,the_carrier(boole_lattice(sK519)))
| ~ lattice(boole_lattice(sK519))
| ~ latt_str(boole_lattice(sK519)) ),
inference(forward_subsumption_resolution,[],[f6666,f3415]) ).
fof(f6671,plain,
! [X0] :
( ~ related_reflexive(poset_of_lattice(boole_lattice(sK519)),sK520,cast_to_el_of_LattPOSet(boole_lattice(sK519),X0))
| below_refl(boole_lattice(sK519),sK520,X0)
| ~ element(X0,the_carrier(boole_lattice(sK519)))
| ~ element(sK520,the_carrier(boole_lattice(sK519)))
| ~ latt_str(boole_lattice(sK519)) ),
inference(forward_subsumption_resolution,[],[f6667,f3407]) ).
fof(f6675,plain,
! [X0] :
( ~ related_reflexive(poset_of_lattice(boole_lattice(sK519)),sK520,cast_to_el_of_LattPOSet(boole_lattice(sK519),X0))
| below_refl(boole_lattice(sK519),sK520,X0)
| ~ element(X0,the_carrier(boole_lattice(sK519)))
| ~ element(sK520,the_carrier(boole_lattice(sK519))) ),
inference(forward_subsumption_resolution,[],[f6671,f3131]) ).
fof(f6679,plain,
! [X0] :
( ~ element(X0,k1_pcomps_1(sK519))
| ~ related_reflexive(poset_of_lattice(boole_lattice(sK519)),sK520,cast_to_el_of_LattPOSet(boole_lattice(sK519),X0))
| below_refl(boole_lattice(sK519),sK520,X0)
| ~ element(sK520,the_carrier(boole_lattice(sK519))) ),
inference(forward_demodulation,[],[f6675,f6329]) ).
fof(f6683,plain,
! [X0] :
( ~ element(sK520,k1_pcomps_1(sK519))
| ~ element(X0,k1_pcomps_1(sK519))
| ~ related_reflexive(poset_of_lattice(boole_lattice(sK519)),sK520,cast_to_el_of_LattPOSet(boole_lattice(sK519),X0))
| below_refl(boole_lattice(sK519),sK520,X0) ),
inference(forward_demodulation,[],[f6679,f6329]) ).
fof(f6687,plain,
! [X0] :
( ~ related_reflexive(poset_of_lattice(boole_lattice(sK519)),sK520,cast_to_el_of_LattPOSet(boole_lattice(sK519),X0))
| ~ element(X0,k1_pcomps_1(sK519))
| below_refl(boole_lattice(sK519),sK520,X0) ),
inference(forward_subsumption_resolution,[],[f6683,f6586]) ).
fof(f6690,plain,
( ~ related_reflexive(poset_of_lattice(boole_lattice(sK519)),sK520,sK521)
| ~ element(sK521,k1_pcomps_1(sK519))
| below_refl(boole_lattice(sK519),sK520,sK521) ),
inference(superposition,[],[f6687,f6605]) ).
fof(f6702,plain,
( ~ element(sK521,k1_pcomps_1(sK519))
| below_refl(boole_lattice(sK519),sK520,sK521)
| ~ spl542_5 ),
inference(forward_subsumption_resolution,[],[f6690,f5935]) ).
fof(f6714,plain,
( below_refl(boole_lattice(sK519),sK520,sK521)
| ~ spl542_5 ),
inference(forward_subsumption_resolution,[],[f6702,f6588]) ).
fof(f6765,plain,
( ~ element(sK521,k1_pcomps_1(sK519))
| below(boole_lattice(sK519),sK520,sK521)
| ~ spl542_5 ),
inference(resolution,[],[f6639,f6714]) ).
fof(f6768,plain,
( below(boole_lattice(sK519),sK520,sK521)
| ~ spl542_5 ),
inference(forward_subsumption_resolution,[],[f6765,f6588]) ).
fof(f6769,plain,
( subset(sK520,sK521)
| ~ element(sK521,the_carrier(boole_lattice(sK519)))
| ~ element(sK520,the_carrier(boole_lattice(sK519)))
| ~ spl542_5 ),
inference(resolution,[],[f6768,f4533]) ).
fof(f6770,plain,
( ~ element(sK521,the_carrier(boole_lattice(sK519)))
| ~ element(sK520,the_carrier(boole_lattice(sK519)))
| ~ spl542_5
| spl542_6 ),
inference(forward_subsumption_resolution,[],[f6769,f5941]) ).
fof(f6771,plain,
( ~ element(sK521,k1_pcomps_1(sK519))
| ~ element(sK520,the_carrier(boole_lattice(sK519)))
| ~ spl542_5
| spl542_6 ),
inference(forward_demodulation,[],[f6770,f6329]) ).
fof(f6772,plain,
( ~ element(sK520,the_carrier(boole_lattice(sK519)))
| ~ spl542_5
| spl542_6 ),
inference(forward_subsumption_resolution,[],[f6771,f6588]) ).
fof(f6773,plain,
( ~ element(sK520,k1_pcomps_1(sK519))
| ~ spl542_5
| spl542_6 ),
inference(forward_demodulation,[],[f6772,f6329]) ).
fof(f6774,plain,
( $false
| ~ spl542_5
| spl542_6 ),
inference(forward_subsumption_resolution,[],[f6773,f6586]) ).
fof(f6775,plain,
( ~ spl542_5
| spl542_6 ),
inference(avatar_contradiction_clause,[],[f6774]) ).
fof(f6776,plain,
( ~ element(sK520,k1_pcomps_1(sK519))
| ~ below_refl(boole_lattice(sK519),sK520,sK521)
| spl542_5 ),
inference(forward_subsumption_resolution,[],[f6661,f5940]) ).
fof(f6778,plain,
( ~ below_refl(boole_lattice(sK519),sK520,sK521)
| spl542_5 ),
inference(forward_subsumption_resolution,[],[f6776,f6586]) ).
fof(f6780,definition,
( spl542_93
<=> below_refl(boole_lattice(sK519),sK520,sK521) ),
introduced(definition,[new_symbols(definition,[spl542_93])],[avatar_definition]) ).
fof(f6781,plain,
( ~ below_refl(boole_lattice(sK519),sK520,sK521)
| spl542_93 ),
inference(avatar_component_clause,[],[f6780]) ).
fof(f6786,plain,
( ~ spl542_93
| spl542_5 ),
inference(avatar_split_clause,[],[f6778,f5934,f6780]) ).
fof(f6793,plain,
( ! [X0] :
( below(boole_lattice(X0),sK520,sK521)
| ~ element(sK521,the_carrier(boole_lattice(X0)))
| ~ element(sK520,the_carrier(boole_lattice(X0))) )
| ~ spl542_6 ),
inference(resolution,[],[f5938,f4534]) ).
fof(f6794,plain,
( ! [X0] :
( ~ element(sK521,k1_pcomps_1(X0))
| below(boole_lattice(X0),sK520,sK521)
| ~ element(sK520,the_carrier(boole_lattice(X0))) )
| ~ spl542_6 ),
inference(forward_demodulation,[],[f6793,f6329]) ).
fof(f6802,plain,
( ! [X0] :
( below(boole_lattice(X0),sK520,sK521)
| ~ element(sK521,k1_pcomps_1(X0))
| ~ element(sK520,k1_pcomps_1(X0)) )
| ~ spl542_6 ),
inference(forward_demodulation,[],[f6794,f6329]) ).
fof(f6873,plain,
( ~ below(boole_lattice(sK519),sK520,sK521)
| ~ element(sK521,k1_pcomps_1(sK519))
| spl542_93 ),
inference(resolution,[],[f6781,f6638]) ).
fof(f6874,plain,
( ~ below(boole_lattice(sK519),sK520,sK521)
| spl542_93 ),
inference(forward_subsumption_resolution,[],[f6873,f6588]) ).
fof(f6875,plain,
( $false
| ~ spl542_6
| spl542_93 ),
inference(unit_resulting_resolution,[],[f6802,f6586,f6588,f6874]) ).
fof(f6877,plain,
( ~ spl542_6
| spl542_93 ),
inference(avatar_contradiction_clause,[],[f6875]) ).
cnf(s3,plain,
( spl542_5
| spl542_6 ),
inference(sat_conversion,[],[f5939]) ).
cnf(s4,plain,
( ~ spl542_5
| ~ spl542_6 ),
inference(sat_conversion,[],[f5942]) ).
cnf(s85,plain,
( ~ spl542_5
| spl542_6 ),
inference(sat_conversion,[],[f6775]) ).
cnf(s87,plain,
( spl542_5
| ~ spl542_93 ),
inference(sat_conversion,[],[f6786]) ).
cnf(s96,plain,
( ~ spl542_6
| spl542_93 ),
inference(sat_conversion,[],[f6877]) ).
cnf(s102,plain,
spl542_5,
inference(rat,[],[s96,s3,s87]) ).
cnf(s103,plain,
spl542_6,
inference(rat,[],[s85,s102]) ).
cnf(s104,plain,
$false,
inference(rat,[],[s4,s103,s102]) ).
fof(f6881,plain,
$false,
inference(avatar_sat_refutation,[],[s104]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU369+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.38 % Computer : n026.cluster.edu
% 0.13/0.38 % Model : x86_64 x86_64
% 0.13/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.38 % Memory : 8046.5625MB
% 0.13/0.38 % OS : Linux 6.8.0-71-generic
% 0.13/0.38 % CPULimit : 300
% 0.13/0.38 % WCLimit : 300
% 0.13/0.38 % DateTime : Mon Sep 28 05:01:12 UTC 2026
% 0.13/0.38 % CPUTime :
% 0.13/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.42 Running first-order theorem proving
% 0.13/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 9.37/2.22 % (3469948)Detected formulas, will run a generic FOF schedule.
% 9.37/2.22 % (3469957)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=4242625903:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 9.37/2.22 % (3469958)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3192817255:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 9.37/2.22 % (3469959)dis-21_1_sil=8000:lcm=predicate:random_seed=3486767611:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 9.37/2.22 % (3469953)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=3111572348:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 9.37/2.22 % (3469955)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=3470422104:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 9.37/2.22 % (3469954)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=3966218252:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 9.37/2.22 % (3469956)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=4085244089:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 9.37/2.22 % (3469956)Instruction limit reached!
% 9.37/2.22 % (3469956)------------------------------
% 9.37/2.22 % (3469956)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.37/2.22 % (3469956)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.37/2.22 % (3469956)CaDiCaL version: 2.1.3
% 9.37/2.22 % (3469956)Termination reason: Instruction limit
% 9.37/2.22 % (3469956)Termination phase: Property scanning
% 9.37/2.22 % (3469956)Time elapsed: 0.059 s
% 9.37/2.22 % (3469956)Peak memory usage: 90 MB
% 9.37/2.22 % (3469956)Instructions burned: 109 (million)
% 9.37/2.22 % (3469959)Instruction limit reached!
% 9.37/2.22 % (3469959)------------------------------
% 9.37/2.22 % (3469959)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.37/2.22 % (3469959)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.37/2.22 % (3469959)CaDiCaL version: 2.1.3
% 9.37/2.22 % (3469959)Termination reason: Instruction limit
% 9.37/2.22 % (3469959)Termination phase: Saturation
% 9.37/2.22 % (3469959)Time elapsed: 0.066 s
% 9.37/2.22 % (3469959)Peak memory usage: 91 MB
% 9.37/2.22 % (3469959)Instructions burned: 130 (million)
% 9.37/2.22 % (3469957)Instruction limit reached!
% 9.37/2.22 % (3469957)------------------------------
% 9.37/2.22 % (3469957)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.37/2.22 % (3469957)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.37/2.22 % (3469957)CaDiCaL version: 2.1.3
% 9.37/2.22 % (3469957)Termination reason: Instruction limit
% 9.37/2.22 % (3469957)Termination phase: Saturation
% 9.37/2.22 % (3469957)Time elapsed: 0.070 s
% 9.37/2.22 % (3469957)Peak memory usage: 91 MB
% 9.37/2.22 % (3469957)Instructions burned: 120 (million)
% 9.37/2.22 % (3469958)Instruction limit reached!
% 9.37/2.22 % (3469958)------------------------------
% 9.37/2.22 % (3469958)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.37/2.22 % (3469958)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.37/2.22 % (3469958)CaDiCaL version: 2.1.3
% 9.37/2.22 % (3469958)Termination reason: Instruction limit
% 9.37/2.22 % (3469958)Termination phase: Saturation
% 9.37/2.22 % (3469958)Time elapsed: 0.081 s
% 9.37/2.22 % (3469958)Peak memory usage: 92 MB
% 9.37/2.22 % (3469958)Instructions burned: 140 (million)
% 9.37/2.22 % (3469968)lrs+10_1_sil=32000:urr=on:br=off:random_seed=925138142:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 9.37/2.22 % (3469967)lrs+10_1_sil=8000:sp=occurrence:random_seed=685417095:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 9.37/2.22 % (3469970)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=2757425071:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 9.37/2.22 % (3469969)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1459879850:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 9.37/2.22 % (3469968)Instruction limit reached!
% 9.37/2.22 % (3469968)------------------------------
% 9.37/2.22 % (3469968)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.37/2.22 % (3469968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.37/2.22 % (3469968)CaDiCaL version: 2.1.3
% 9.37/2.22 % (3469968)Termination reason: Instruction limit
% 9.37/2.22 % (3469968)Termination phase: Saturation
% 9.37/2.22 % (3469968)Time elapsed: 0.080 s
% 9.37/2.22 % (3469968)Peak memory usage: 90 MB
% 9.37/2.22 % (3469968)Instructions burned: 158 (million)
% 9.37/2.22 % (3469970)Instruction limit reached!
% 9.37/2.22 % (3469970)------------------------------
% 9.37/2.22 % (3469970)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.37/2.22 % (3469970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.37/2.22 % (3469970)CaDiCaL version: 2.1.3
% 9.37/2.22 % (3469970)Termination reason: Instruction limit
% 9.37/2.22 % (3469970)Termination phase: Saturation
% 9.37/2.22 % (3469970)Time elapsed: 0.094 s
% 9.37/2.22 % (3469970)Peak memory usage: 94 MB
% 9.37/2.22 % (3469970)Instructions burned: 248 (million)
% 9.37/2.22 % (3469967)Instruction limit reached!
% 9.37/2.22 % (3469967)------------------------------
% 9.37/2.22 % (3469967)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.37/2.22 % (3469967)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.37/2.22 % (3469967)CaDiCaL version: 2.1.3
% 9.37/2.22 % (3469967)Termination reason: Instruction limit
% 9.37/2.22 % (3469967)Termination phase: Saturation
% 9.37/2.22 % (3469967)Time elapsed: 0.178 s
% 9.37/2.22 % (3469967)Peak memory usage: 95 MB
% 9.37/2.22 % (3469967)Instructions burned: 285 (million)
% 9.37/2.22 % (3469976)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1073285258:i=2350_2995 on theBenchmark for (2995ds/2350Mi)
% 9.37/2.22 % (3469975)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1062997472:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 9.37/2.22 % (3469969)Instruction limit reached!
% 9.37/2.22 % (3469969)------------------------------
% 9.37/2.22 % (3469969)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.37/2.22 % (3469969)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.37/2.22 % (3469969)CaDiCaL version: 2.1.3
% 9.37/2.22 % (3469969)Termination reason: Instruction limit
% 9.37/2.22 % (3469969)Termination phase: Saturation
% 9.37/2.22 % (3469969)Time elapsed: 0.219 s
% 9.37/2.22 % (3469969)Peak memory usage: 95 MB
% 9.37/2.22 % (3469969)Instructions burned: 325 (million)
% 9.37/2.22 % (3469977)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=607146871:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi)
% 9.37/2.22 % (3469980)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1056219724:i=127:av=off:fsr=off:sup=off_2994 on theBenchmark for (2994ds/127Mi)
% 9.37/2.22 % (3469977)Instruction limit reached!
% 9.37/2.22 % (3469977)------------------------------
% 9.37/2.22 % (3469977)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.37/2.22 % (3469977)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.37/2.22 % (3469977)CaDiCaL version: 2.1.3
% 9.37/2.22 % (3469977)Termination reason: Instruction limit
% 9.37/2.22 % (3469977)Termination phase: Saturation
% 9.37/2.22 % (3469977)Time elapsed: 0.064 s
% 9.37/2.22 % (3469977)Peak memory usage: 92 MB
% 9.37/2.22 % (3469977)Instructions burned: 114 (million)
% 9.37/2.22 % (3469975)Instruction limit reached!
% 9.37/2.22 % (3469975)------------------------------
% 9.37/2.22 % (3469975)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.37/2.22 % (3469975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.37/2.22 % (3469975)CaDiCaL version: 2.1.3
% 9.37/2.22 % (3469975)Termination reason: Instruction limit
% 9.37/2.22 % (3469975)Termination phase: Saturation
% 9.37/2.22 % (3469975)Time elapsed: 0.183 s
% 9.37/2.22 % (3469975)Peak memory usage: 94 MB
% 9.37/2.22 % (3469975)Instructions burned: 294 (million)
% 9.37/2.22 % (3469980)Instruction limit reached!
% 9.37/2.22 % (3469980)------------------------------
% 9.37/2.22 % (3469980)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.37/2.22 % (3469980)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.37/2.22 % (3469980)CaDiCaL version: 2.1.3
% 9.37/2.22 % (3469980)Termination reason: Instruction limit
% 9.37/2.22 % (3469980)Termination phase: Property scanning
% 9.37/2.22 % (3469980)Time elapsed: 0.073 s
% 9.37/2.22 % (3469980)Peak memory usage: 91 MB
% 9.37/2.22 % (3469980)Instructions burned: 128 (million)
% 9.37/2.22 % (3469983)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1584778203:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2992 on theBenchmark for (2992ds/114Mi)
% 9.37/2.22 % (3469984)lrs+10_1_sil=8000:sp=occurrence:random_seed=4078807316:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2992 on theBenchmark for (2992ds/907Mi)
% 9.37/2.22 % (3469983)Instruction limit reached!
% 9.37/2.22 % (3469983)------------------------------
% 9.37/2.22 % (3469983)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.37/2.22 % (3469983)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.37/2.22 % (3469983)CaDiCaL version: 2.1.3
% 9.37/2.22 % (3469983)Termination reason: Instruction limit
% 9.37/2.22 % (3469983)Termination phase: Saturation
% 9.37/2.22 % (3469983)Time elapsed: 0.070 s
% 9.37/2.22 % (3469983)Peak memory usage: 90 MB
% 9.37/2.22 % (3469983)Instructions burned: 115 (million)
% 9.37/2.22 % (3469985)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1873034753:i=437:sd=1:aac=none:ss=included_2992 on theBenchmark for (2992ds/437Mi)
% 9.37/2.22 % (3469988)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3438108862:i=5202:ss=axioms:sgt=16_2990 on theBenchmark for (2990ds/5202Mi)
% 9.37/2.22 % (3469985)Instruction limit reached!
% 9.37/2.22 % (3469985)------------------------------
% 9.37/2.22 % (3469985)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.37/2.22 % (3469985)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.37/2.22 % (3469985)CaDiCaL version: 2.1.3
% 9.37/2.22 % (3469985)Termination reason: Instruction limit
% 9.37/2.22 % (3469985)Termination phase: Saturation
% 9.37/2.22 % (3469985)Time elapsed: 0.267 s
% 9.37/2.22 % (3469985)Peak memory usage: 96 MB
% 9.37/2.22 % (3469985)Instructions burned: 438 (million)
% 9.37/2.22 % (3469991)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3264133859:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2987 on theBenchmark for (2987ds/134Mi)
% 9.37/2.22 % (3469954)First to succeed.
% 9.37/2.22 % (3469954)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3469948"
% 9.37/2.22 % (3469976)Also succeeded, but the first one will report.
% 9.37/2.22 % (3469991)Instruction limit reached!
% 9.37/2.22 % (3469991)------------------------------
% 9.37/2.22 % (3469991)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.37/2.22 % (3469991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.37/2.22 % (3469991)CaDiCaL version: 2.1.3
% 9.37/2.22 % (3469991)Termination reason: Instruction limit
% 9.37/2.22 % (3469991)Termination phase: Saturation
% 9.37/2.22 % (3469991)Time elapsed: 0.069 s
% 9.37/2.22 % (3469991)Peak memory usage: 91 MB
% 9.37/2.22 % (3469991)Instructions burned: 136 (million)
% 9.37/2.22 % (3469984)Instruction limit reached!
% 9.37/2.22 % (3469984)------------------------------
% 9.37/2.22 % (3469984)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.37/2.22 % (3469984)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.37/2.22 % (3469984)CaDiCaL version: 2.1.3
% 9.37/2.22 % (3469984)Termination reason: Instruction limit
% 9.37/2.22 % (3469984)Termination phase: Saturation
% 9.37/2.22 % (3469984)Time elapsed: 0.581 s
% 9.37/2.22 % (3469984)Peak memory usage: 105 MB
% 9.37/2.22 % (3469984)Instructions burned: 908 (million)
% 9.37/2.22 % (3469993)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=4004542083:st=8:i=592:sd=3:ep=RST:ss=axioms_2986 on theBenchmark for (2986ds/592Mi)
% 9.37/2.22 % (3469994)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3437743192:st=3:i=13193:sd=3:ss=axioms_2985 on theBenchmark for (2985ds/13193Mi)
% 9.37/2.22 % (3469954)Refutation found. Thanks to Tanya!
% 9.37/2.22 % SZS status Theorem for theBenchmark
% 9.37/2.22 % SZS output start Proof for theBenchmark
% See solution above
% 11.65/2.42 % (3469954)------------------------------
% 11.65/2.42 % (3469954)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.65/2.42 % (3469954)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.65/2.42 % (3469954)CaDiCaL version: 2.1.3
% 11.65/2.42 % (3469954)Termination reason: Refutation
% 11.65/2.42 % (3469954)Time elapsed: 1.184 s
% 11.65/2.42 % (3469954)Peak memory usage: 158 MB
% 11.65/2.42 % (3469954)Instructions burned: 1925 (million)
% 11.65/2.42 % (3469954)------------------------------
% 11.65/2.42 % (3469954)------------------------------
% 11.65/2.42 % (3469948)Success in time 1.601 s
% 11.65/2.42 % Vampire exiting
%------------------------------------------------------------------------------