%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU345+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:27 PM UTC 2026
% Result : Theorem 7.12s 2.05s
% Output : Refutation 8.86s
% Verified :
% SZS Type : Refutation
% Derivation depth : 31
% Number of leaves : 21
% Syntax : Number of formulae : 150 ( 37 unt; 6 def)
% Number of atoms : 593 ( 177 equ)
% Maximal formula atoms : 14 ( 3 avg)
% Number of connectives : 712 ( 269 ~; 334 |; 80 &)
% ( 14 <=>; 15 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 21 ( 19 usr; 5 prp; 0-2 aty)
% Number of functors : 25 ( 25 usr; 4 con; 0-3 aty)
% Number of variables : 200 ( 0 sgn 181 !; 19 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f50,axiom,
! [X0] :
( ( ~ empty_carrier(X0)
& meet_semilatt_str(X0) )
=> ( lower_bounded_semilattstr(X0)
<=> ? [X1] :
( element(X1,the_carrier(X0))
& ! [X2] :
( element(X2,the_carrier(X0))
=> ( meet(X0,X1,X2) = X1
& meet(X0,X2,X1) = X1 ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d13_lattices) ).
fof(f55,axiom,
! [X0] :
( ( ~ empty_carrier(X0)
& meet_semilatt_str(X0) )
=> ( lower_bounded_semilattstr(X0)
=> ! [X1] :
( element(X1,the_carrier(X0))
=> ( X1 = bottom_of_semilattstr(X0)
<=> ! [X2] :
( element(X2,the_carrier(X0))
=> ( meet(X0,X1,X2) = X1
& meet(X0,X2,X1) = X1 ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d16_lattices) ).
fof(f63,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(f78,axiom,
! [X0] :
( X0 = empty_set
<=> ! [X1] : ~ in(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d1_xboole_0) ).
fof(f143,axiom,
! [X0] :
( strict_latt_str(boole_lattice(X0))
& latt_str(boole_lattice(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k1_lattice3) ).
fof(f178,axiom,
! [X0] :
( ( ~ empty_carrier(X0)
& meet_semilatt_str(X0) )
=> element(bottom_of_semilattstr(X0),the_carrier(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k5_lattices) ).
fof(f198,axiom,
! [X0] :
( latt_str(X0)
=> ( meet_semilatt_str(X0)
& join_semilatt_str(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l3_lattices) ).
fof(f244,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)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc2_lattice3) ).
fof(f316,axiom,
! [X0,X1] :
( ! [X2] :
( in(X2,X0)
=> in(X2,X1) )
=> element(X0,powerset(X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l71_subset_1) ).
fof(f464,axiom,
! [X0,X1] :
( element(X1,the_carrier(boole_lattice(X0)))
=> ! [X2] :
( element(X2,the_carrier(boole_lattice(X0)))
=> ( join(boole_lattice(X0),X1,X2) = set_union2(X1,X2)
& meet(boole_lattice(X0),X1,X2) = set_intersection2(X1,X2) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t1_lattice3) ).
fof(f498,axiom,
! [X0] : set_intersection2(X0,empty_set) = empty_set,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2_boole) ).
fof(f524,axiom,
! [X0] : set_difference(X0,empty_set) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t3_boole) ).
fof(f525,conjecture,
! [X0] :
( lower_bounded_semilattstr(boole_lattice(X0))
& bottom_of_semilattstr(boole_lattice(X0)) = empty_set ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t3_lattice3) ).
fof(f526,negated_conjecture,
~ ! [X0] :
( lower_bounded_semilattstr(boole_lattice(X0))
& bottom_of_semilattstr(boole_lattice(X0)) = empty_set ),
inference(negated_conjecture,[status(cth)],[f525]) ).
fof(f551,axiom,
! [X0,X1] : set_difference(X0,set_difference(X0,X1)) = set_intersection2(X0,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t48_xboole_1) ).
fof(f553,axiom,
! [X0] : set_difference(empty_set,X0) = empty_set,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t4_boole) ).
fof(f730,plain,
! [X0] :
( ( lower_bounded_semilattstr(X0)
<=> ? [X1] :
( element(X1,the_carrier(X0))
& ! [X2] :
( ( meet(X0,X1,X2) = X1
& meet(X0,X2,X1) = X1 )
| ~ element(X2,the_carrier(X0)) ) ) )
| empty_carrier(X0)
| ~ meet_semilatt_str(X0) ),
inference(ennf_transformation,[],[f50]) ).
fof(f731,plain,
! [X0] :
( ( lower_bounded_semilattstr(X0)
<=> ? [X1] :
( element(X1,the_carrier(X0))
& ! [X2] :
( ( meet(X0,X1,X2) = X1
& meet(X0,X2,X1) = X1 )
| ~ element(X2,the_carrier(X0)) ) ) )
| empty_carrier(X0)
| ~ meet_semilatt_str(X0) ),
inference(flattening,[],[f730]) ).
fof(f737,plain,
! [X0] :
( ! [X1] :
( ( X1 = bottom_of_semilattstr(X0)
<=> ! [X2] :
( ( meet(X0,X1,X2) = X1
& meet(X0,X2,X1) = X1 )
| ~ element(X2,the_carrier(X0)) ) )
| ~ element(X1,the_carrier(X0)) )
| ~ lower_bounded_semilattstr(X0)
| empty_carrier(X0)
| ~ meet_semilatt_str(X0) ),
inference(ennf_transformation,[],[f55]) ).
fof(f738,plain,
! [X0] :
( ! [X1] :
( ( X1 = bottom_of_semilattstr(X0)
<=> ! [X2] :
( ( meet(X0,X1,X2) = X1
& meet(X0,X2,X1) = X1 )
| ~ element(X2,the_carrier(X0)) ) )
| ~ element(X1,the_carrier(X0)) )
| ~ lower_bounded_semilattstr(X0)
| empty_carrier(X0)
| ~ meet_semilatt_str(X0) ),
inference(flattening,[],[f737]) ).
fof(f749,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,[],[f63]) ).
fof(f750,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,[],[f749]) ).
fof(f852,plain,
! [X0] :
( element(bottom_of_semilattstr(X0),the_carrier(X0))
| empty_carrier(X0)
| ~ meet_semilatt_str(X0) ),
inference(ennf_transformation,[],[f178]) ).
fof(f853,plain,
! [X0] :
( element(bottom_of_semilattstr(X0),the_carrier(X0))
| empty_carrier(X0)
| ~ meet_semilatt_str(X0) ),
inference(flattening,[],[f852]) ).
fof(f874,plain,
! [X0] :
( ( meet_semilatt_str(X0)
& join_semilatt_str(X0) )
| ~ latt_str(X0) ),
inference(ennf_transformation,[],[f198]) ).
fof(f995,plain,
! [X0,X1] :
( element(X0,powerset(X1))
| ? [X2] :
( ~ in(X2,X1)
& in(X2,X0) ) ),
inference(ennf_transformation,[],[f316]) ).
fof(f1181,plain,
! [X0,X1] :
( ! [X2] :
( ( join(boole_lattice(X0),X1,X2) = set_union2(X1,X2)
& meet(boole_lattice(X0),X1,X2) = set_intersection2(X1,X2) )
| ~ element(X2,the_carrier(boole_lattice(X0))) )
| ~ element(X1,the_carrier(boole_lattice(X0))) ),
inference(ennf_transformation,[],[f464]) ).
fof(f1259,plain,
? [X0] :
( ~ lower_bounded_semilattstr(boole_lattice(X0))
| empty_set != bottom_of_semilattstr(boole_lattice(X0)) ),
inference(ennf_transformation,[],[f526]) ).
fof(f1474,plain,
! [X0] :
( ( ( lower_bounded_semilattstr(X0)
| ! [X1] :
( ~ element(X1,the_carrier(X0))
| ? [X2] :
( ( meet(X0,X1,X2) != X1
| meet(X0,X2,X1) != X1 )
& element(X2,the_carrier(X0)) ) ) )
& ( ? [X1] :
( element(X1,the_carrier(X0))
& ! [X2] :
( ( meet(X0,X1,X2) = X1
& meet(X0,X2,X1) = X1 )
| ~ element(X2,the_carrier(X0)) ) )
| ~ lower_bounded_semilattstr(X0) ) )
| empty_carrier(X0)
| ~ meet_semilatt_str(X0) ),
inference(nnf_transformation,[],[f731]) ).
fof(f1475,plain,
! [X0] :
( ( ( lower_bounded_semilattstr(X0)
| ! [X1] :
( ~ element(X1,the_carrier(X0))
| ? [X2] :
( ( meet(X0,X1,X2) != X1
| meet(X0,X2,X1) != X1 )
& element(X2,the_carrier(X0)) ) ) )
& ( ? [X3] :
( element(X3,the_carrier(X0))
& ! [X4] :
( ( meet(X0,X3,X4) = X3
& meet(X0,X4,X3) = X3 )
| ~ element(X4,the_carrier(X0)) ) )
| ~ lower_bounded_semilattstr(X0) ) )
| empty_carrier(X0)
| ~ meet_semilatt_str(X0) ),
inference(rectify,[],[f1474]) ).
fof(f1476,plain,
! [X0] :
( ( ( lower_bounded_semilattstr(X0)
| ! [X1] :
( ~ element(X1,the_carrier(X0))
| ( ( meet(X0,X1,sK65(X0,X1)) != X1
| meet(X0,sK65(X0,X1),X1) != X1 )
& element(sK65(X0,X1),the_carrier(X0)) ) ) )
& ( ( element(sK66(X0),the_carrier(X0))
& ! [X4] :
( ( sK66(X0) = meet(X0,sK66(X0),X4)
& sK66(X0) = meet(X0,X4,sK66(X0)) )
| ~ element(X4,the_carrier(X0)) ) )
| ~ lower_bounded_semilattstr(X0) ) )
| empty_carrier(X0)
| ~ meet_semilatt_str(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK65,sK66]),skolemize(X2,sK65(X0,X1)),skolemize(X3,sK66(X0))],[f1475]) ).
fof(f1490,plain,
! [X0] :
( ! [X1] :
( ( ( X1 = bottom_of_semilattstr(X0)
| ? [X2] :
( ( meet(X0,X1,X2) != X1
| meet(X0,X2,X1) != X1 )
& element(X2,the_carrier(X0)) ) )
& ( ! [X2] :
( ( meet(X0,X1,X2) = X1
& meet(X0,X2,X1) = X1 )
| ~ element(X2,the_carrier(X0)) )
| bottom_of_semilattstr(X0) != X1 ) )
| ~ element(X1,the_carrier(X0)) )
| ~ lower_bounded_semilattstr(X0)
| empty_carrier(X0)
| ~ meet_semilatt_str(X0) ),
inference(nnf_transformation,[],[f738]) ).
fof(f1491,plain,
! [X0] :
( ! [X1] :
( ( ( X1 = bottom_of_semilattstr(X0)
| ? [X2] :
( ( meet(X0,X1,X2) != X1
| meet(X0,X2,X1) != X1 )
& element(X2,the_carrier(X0)) ) )
& ( ! [X3] :
( ( meet(X0,X1,X3) = X1
& meet(X0,X3,X1) = X1 )
| ~ element(X3,the_carrier(X0)) )
| bottom_of_semilattstr(X0) != X1 ) )
| ~ element(X1,the_carrier(X0)) )
| ~ lower_bounded_semilattstr(X0)
| empty_carrier(X0)
| ~ meet_semilatt_str(X0) ),
inference(rectify,[],[f1490]) ).
fof(f1492,plain,
! [X0] :
( ! [X1] :
( ( ( X1 = bottom_of_semilattstr(X0)
| ( ( meet(X0,X1,sK76(X0,X1)) != X1
| meet(X0,sK76(X0,X1),X1) != X1 )
& element(sK76(X0,X1),the_carrier(X0)) ) )
& ( ! [X3] :
( ( meet(X0,X1,X3) = X1
& meet(X0,X3,X1) = X1 )
| ~ element(X3,the_carrier(X0)) )
| bottom_of_semilattstr(X0) != X1 ) )
| ~ element(X1,the_carrier(X0)) )
| ~ lower_bounded_semilattstr(X0)
| empty_carrier(X0)
| ~ meet_semilatt_str(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK76]),skolemize(X2,sK76(X0,X1))],[f1491]) ).
fof(f1506,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,[],[f750]) ).
fof(f1507,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,[],[f1506]) ).
fof(f1508,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,[],[f1507]) ).
fof(f1509,plain,
! [X0,X1] :
( ( ( X1 = boole_lattice(X0)
| powerset(X0) != the_carrier(X1)
| ( ( apply_binary(the_L_join(X1),sK82(X0,X1),sK83(X0,X1)) != subset_union2(X0,sK82(X0,X1),sK83(X0,X1))
| apply_binary(the_L_meet(X1),sK82(X0,X1),sK83(X0,X1)) != subset_intersection2(X0,sK82(X0,X1),sK83(X0,X1)) )
& element(sK83(X0,X1),powerset(X0))
& element(sK82(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,[sK82,sK83]),skolemize(X2,sK82(X0,X1)),skolemize(X3,sK83(X0,X1))],[f1508]) ).
fof(f1545,plain,
! [X0] :
( ( X0 = empty_set
| ? [X1] : in(X1,X0) )
& ( ! [X1] : ~ in(X1,X0)
| empty_set != X0 ) ),
inference(nnf_transformation,[],[f78]) ).
fof(f1546,plain,
! [X0] :
( ( X0 = empty_set
| ? [X1] : in(X1,X0) )
& ( ! [X2] : ~ in(X2,X0)
| empty_set != X0 ) ),
inference(rectify,[],[f1545]) ).
fof(f1547,plain,
! [X0] :
( ( X0 = empty_set
| in(sK101(X0),X0) )
& ( ! [X2] : ~ in(X2,X0)
| empty_set != X0 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK101]),skolemize(X1,sK101(X0))],[f1546]) ).
fof(f1705,plain,
! [X0,X1] :
( element(X0,powerset(X1))
| ( ~ in(sK185(X0,X1),X1)
& in(sK185(X0,X1),X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK185]),skolemize(X2,sK185(X0,X1))],[f995]) ).
fof(f2042,plain,
( ~ lower_bounded_semilattstr(boole_lattice(sK477))
| empty_set != bottom_of_semilattstr(boole_lattice(sK477)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK477]),skolemize(X0,sK477)],[f1259]) ).
fof(f2198,plain,
! [X0,X1] :
( element(sK65(X0,X1),the_carrier(X0))
| ~ element(X1,the_carrier(X0))
| lower_bounded_semilattstr(X0)
| empty_carrier(X0)
| ~ meet_semilatt_str(X0) ),
inference(cnf_transformation,[],[f1476]) ).
fof(f2199,plain,
! [X0,X1] :
( meet(X0,sK65(X0,X1),X1) != X1
| ~ element(X1,the_carrier(X0))
| meet(X0,X1,sK65(X0,X1)) != X1
| lower_bounded_semilattstr(X0)
| empty_carrier(X0)
| ~ meet_semilatt_str(X0) ),
inference(cnf_transformation,[],[f1476]) ).
fof(f2228,plain,
! [X3,X0,X1] :
( meet(X0,X3,X1) = X1
| ~ element(X3,the_carrier(X0))
| bottom_of_semilattstr(X0) != X1
| ~ element(X1,the_carrier(X0))
| ~ lower_bounded_semilattstr(X0)
| empty_carrier(X0)
| ~ meet_semilatt_str(X0) ),
inference(cnf_transformation,[],[f1492]) ).
fof(f2262,plain,
! [X0,X1] :
( powerset(X0) = the_carrier(X1)
| boole_lattice(X0) != X1
| ~ strict_latt_str(X1)
| ~ latt_str(X1) ),
inference(cnf_transformation,[],[f1509]) ).
fof(f2323,plain,
! [X2,X0] :
( ~ in(X2,X0)
| empty_set != X0 ),
inference(cnf_transformation,[],[f1547]) ).
fof(f2559,plain,
! [X0] : latt_str(boole_lattice(X0)),
inference(cnf_transformation,[],[f143]) ).
fof(f2578,plain,
! [X0] :
( element(bottom_of_semilattstr(X0),the_carrier(X0))
| empty_carrier(X0)
| ~ meet_semilatt_str(X0) ),
inference(cnf_transformation,[],[f853]) ).
fof(f2596,plain,
! [X0] :
( ~ latt_str(X0)
| meet_semilatt_str(X0) ),
inference(cnf_transformation,[],[f874]) ).
fof(f2677,plain,
! [X0] : strict_latt_str(boole_lattice(X0)),
inference(cnf_transformation,[],[f244]) ).
fof(f2678,plain,
! [X0] : ~ empty_carrier(boole_lattice(X0)),
inference(cnf_transformation,[],[f244]) ).
fof(f2837,plain,
! [X0,X1] :
( in(sK185(X0,X1),X0)
| element(X0,powerset(X1)) ),
inference(cnf_transformation,[],[f1705]) ).
fof(f3533,plain,
! [X2,X0,X1] :
( set_intersection2(X1,X2) = meet(boole_lattice(X0),X1,X2)
| ~ element(X2,the_carrier(boole_lattice(X0)))
| ~ element(X1,the_carrier(boole_lattice(X0))) ),
inference(cnf_transformation,[],[f1181]) ).
fof(f3587,plain,
! [X0] : empty_set = set_intersection2(X0,empty_set),
inference(cnf_transformation,[],[f498]) ).
fof(f3633,plain,
! [X0] : set_difference(X0,empty_set) = X0,
inference(cnf_transformation,[],[f524]) ).
fof(f3634,plain,
( ~ lower_bounded_semilattstr(boole_lattice(sK477))
| empty_set != bottom_of_semilattstr(boole_lattice(sK477)) ),
inference(cnf_transformation,[],[f2042]) ).
fof(f3680,plain,
! [X0,X1] : set_intersection2(X0,X1) = set_difference(X0,set_difference(X0,X1)),
inference(cnf_transformation,[],[f551]) ).
fof(f3682,plain,
! [X0] : empty_set = set_difference(empty_set,X0),
inference(cnf_transformation,[],[f553]) ).
fof(f4125,plain,
! [X2,X0,X1] :
( ~ element(X2,the_carrier(boole_lattice(X0)))
| meet(boole_lattice(X0),X1,X2) = set_difference(X1,set_difference(X1,X2))
| ~ element(X1,the_carrier(boole_lattice(X0))) ),
inference(definition_unfolding,[],[f3533,f3680]) ).
fof(f4135,plain,
! [X0] : empty_set = set_difference(X0,set_difference(X0,empty_set)),
inference(definition_unfolding,[],[f3587,f3680]) ).
fof(f4200,plain,
! [X3,X0] :
( bottom_of_semilattstr(X0) = meet(X0,X3,bottom_of_semilattstr(X0))
| ~ element(X3,the_carrier(X0))
| ~ element(bottom_of_semilattstr(X0),the_carrier(X0))
| ~ lower_bounded_semilattstr(X0)
| empty_carrier(X0)
| ~ meet_semilatt_str(X0) ),
inference(equality_resolution,[],[f2228]) ).
fof(f4214,plain,
! [X0] :
( powerset(X0) = the_carrier(boole_lattice(X0))
| ~ strict_latt_str(boole_lattice(X0))
| ~ latt_str(boole_lattice(X0)) ),
inference(equality_resolution,[],[f2262]) ).
fof(f4242,plain,
! [X2] : ~ in(X2,empty_set),
inference(equality_resolution,[],[f2323]) ).
fof(f4430,definition,
sF493 = boole_lattice(sK477),
introduced(definition,[new_symbols(definition,[sF493])],[function_definition]) ).
fof(f4431,plain,
boole_lattice(sK477) = sF493,
inference(reorient_equations,[],[f4430]) ).
fof(f4432,definition,
sF494 = bottom_of_semilattstr(sF493),
introduced(definition,[new_symbols(definition,[sF494])],[function_definition]) ).
fof(f4433,plain,
bottom_of_semilattstr(sF493) = sF494,
inference(reorient_equations,[],[f4432]) ).
fof(f4434,plain,
( ~ lower_bounded_semilattstr(sF493)
| empty_set != sF494 ),
inference(definition_folding,[],[f3634,f4433,f4431,f4431]) ).
fof(f4471,definition,
( spl495_5
<=> empty_set = sF494 ),
introduced(definition,[new_symbols(definition,[spl495_5])],[avatar_definition]) ).
fof(f4473,plain,
( empty_set != sF494
| spl495_5 ),
inference(avatar_component_clause,[],[f4471]) ).
fof(f4475,definition,
( spl495_6
<=> lower_bounded_semilattstr(sF493) ),
introduced(definition,[new_symbols(definition,[spl495_6])],[avatar_definition]) ).
fof(f4476,plain,
( lower_bounded_semilattstr(sF493)
| ~ spl495_6 ),
inference(avatar_component_clause,[],[f4475]) ).
fof(f4477,plain,
( ~ lower_bounded_semilattstr(sF493)
| spl495_6 ),
inference(avatar_component_clause,[],[f4475]) ).
fof(f4478,plain,
( ~ spl495_5
| ~ spl495_6 ),
inference(avatar_split_clause,[],[f4434,f4475,f4471]) ).
fof(f4479,plain,
! [X0] : empty_set = set_difference(X0,X0),
inference(forward_demodulation,[],[f4135,f3633]) ).
fof(f4765,plain,
! [X0] :
( powerset(X0) = the_carrier(boole_lattice(X0))
| ~ latt_str(boole_lattice(X0)) ),
inference(forward_subsumption_resolution,[],[f4214,f2677]) ).
fof(f4767,plain,
! [X3,X0] :
( ~ element(X3,the_carrier(X0))
| bottom_of_semilattstr(X0) = meet(X0,X3,bottom_of_semilattstr(X0))
| ~ lower_bounded_semilattstr(X0)
| empty_carrier(X0)
| ~ meet_semilatt_str(X0) ),
inference(forward_subsumption_resolution,[],[f4200,f2578]) ).
fof(f4783,plain,
! [X0] : powerset(X0) = the_carrier(boole_lattice(X0)),
inference(forward_subsumption_resolution,[],[f4765,f2559]) ).
fof(f4784,plain,
latt_str(sF493),
inference(superposition,[],[f2559,f4431]) ).
fof(f4787,definition,
( spl495_61
<=> meet_semilatt_str(sF493) ),
introduced(definition,[new_symbols(definition,[spl495_61])],[avatar_definition]) ).
fof(f4788,plain,
( meet_semilatt_str(sF493)
| ~ spl495_61 ),
inference(avatar_component_clause,[],[f4787]) ).
fof(f4789,plain,
( ~ meet_semilatt_str(sF493)
| spl495_61 ),
inference(avatar_component_clause,[],[f4787]) ).
fof(f4791,definition,
( spl495_62
<=> empty_carrier(sF493) ),
introduced(definition,[new_symbols(definition,[spl495_62])],[avatar_definition]) ).
fof(f4792,plain,
( ~ empty_carrier(sF493)
| spl495_62 ),
inference(avatar_component_clause,[],[f4791]) ).
fof(f4800,plain,
! [X0,X1] :
( meet(boole_lattice(X0),X1,bottom_of_semilattstr(boole_lattice(X0))) = set_difference(X1,set_difference(X1,bottom_of_semilattstr(boole_lattice(X0))))
| ~ element(X1,the_carrier(boole_lattice(X0)))
| empty_carrier(boole_lattice(X0))
| ~ meet_semilatt_str(boole_lattice(X0)) ),
inference(resolution,[],[f4125,f2578]) ).
fof(f4801,plain,
! [X0,X1] :
( ~ element(X1,the_carrier(sF493))
| set_difference(X1,set_difference(X1,X0)) = meet(sF493,X1,X0)
| ~ element(X0,the_carrier(sF493)) ),
inference(superposition,[],[f4125,f4431]) ).
fof(f4802,plain,
! [X0,X1] :
( meet(boole_lattice(X0),X1,bottom_of_semilattstr(boole_lattice(X0))) = set_difference(X1,set_difference(X1,bottom_of_semilattstr(boole_lattice(X0))))
| ~ element(X1,the_carrier(boole_lattice(X0)))
| ~ meet_semilatt_str(boole_lattice(X0)) ),
inference(forward_subsumption_resolution,[],[f4800,f2678]) ).
fof(f4803,plain,
! [X0,X1] :
( ~ element(X1,powerset(X0))
| meet(boole_lattice(X0),X1,bottom_of_semilattstr(boole_lattice(X0))) = set_difference(X1,set_difference(X1,bottom_of_semilattstr(boole_lattice(X0))))
| ~ meet_semilatt_str(boole_lattice(X0)) ),
inference(forward_demodulation,[],[f4802,f4783]) ).
fof(f4804,plain,
the_carrier(sF493) = powerset(sK477),
inference(superposition,[],[f4783,f4431]) ).
fof(f4805,plain,
! [X2,X0,X1] :
( ~ element(X2,powerset(X0))
| meet(boole_lattice(X0),X2,X1) = set_difference(X2,set_difference(X2,X1))
| ~ element(X1,powerset(X0)) ),
inference(superposition,[],[f4125,f4783]) ).
fof(f4808,plain,
~ empty_carrier(sF493),
inference(superposition,[],[f2678,f4431]) ).
fof(f4809,plain,
~ spl495_62,
inference(avatar_split_clause,[],[f4808,f4791]) ).
fof(f4816,plain,
! [X0] : meet_semilatt_str(boole_lattice(X0)),
inference(resolution,[],[f2596,f2559]) ).
fof(f4817,plain,
meet_semilatt_str(sF493),
inference(resolution,[],[f2596,f4784]) ).
fof(f4818,plain,
( $false
| spl495_61 ),
inference(forward_subsumption_resolution,[],[f4817,f4789]) ).
fof(f4819,plain,
spl495_61,
inference(avatar_contradiction_clause,[],[f4818]) ).
fof(f4835,plain,
! [X0,X1] :
( ~ element(X0,the_carrier(sF493))
| lower_bounded_semilattstr(sF493)
| empty_carrier(sF493)
| ~ meet_semilatt_str(sF493)
| set_difference(sK65(sF493,X0),set_difference(sK65(sF493,X0),X1)) = meet(sF493,sK65(sF493,X0),X1)
| ~ element(X1,the_carrier(sF493)) ),
inference(resolution,[],[f2198,f4801]) ).
fof(f4837,plain,
! [X0] :
( element(sK65(sF493,X0),powerset(sK477))
| ~ element(X0,powerset(sK477))
| lower_bounded_semilattstr(sF493)
| empty_carrier(sF493)
| ~ meet_semilatt_str(sF493) ),
inference(superposition,[],[f2198,f4804]) ).
fof(f4838,plain,
( ! [X0] :
( element(sK65(sF493,X0),powerset(sK477))
| ~ element(X0,powerset(sK477))
| empty_carrier(sF493)
| ~ meet_semilatt_str(sF493) )
| spl495_6 ),
inference(forward_subsumption_resolution,[],[f4837,f4477]) ).
fof(f4840,plain,
( ! [X0,X1] :
( ~ element(X0,the_carrier(sF493))
| empty_carrier(sF493)
| ~ meet_semilatt_str(sF493)
| set_difference(sK65(sF493,X0),set_difference(sK65(sF493,X0),X1)) = meet(sF493,sK65(sF493,X0),X1)
| ~ element(X1,the_carrier(sF493)) )
| spl495_6 ),
inference(forward_subsumption_resolution,[],[f4835,f4477]) ).
fof(f4842,plain,
( ! [X0] :
( element(sK65(sF493,X0),powerset(sK477))
| ~ element(X0,powerset(sK477))
| ~ meet_semilatt_str(sF493) )
| spl495_6
| spl495_62 ),
inference(forward_subsumption_resolution,[],[f4838,f4792]) ).
fof(f4844,plain,
( ! [X0,X1] :
( ~ element(X0,the_carrier(sF493))
| ~ meet_semilatt_str(sF493)
| set_difference(sK65(sF493,X0),set_difference(sK65(sF493,X0),X1)) = meet(sF493,sK65(sF493,X0),X1)
| ~ element(X1,the_carrier(sF493)) )
| spl495_6
| spl495_62 ),
inference(forward_subsumption_resolution,[],[f4840,f4792]) ).
fof(f4846,plain,
( ! [X0] :
( element(sK65(sF493,X0),powerset(sK477))
| ~ element(X0,powerset(sK477)) )
| spl495_6
| ~ spl495_61
| spl495_62 ),
inference(forward_subsumption_resolution,[],[f4842,f4788]) ).
fof(f4847,plain,
( ! [X0,X1] :
( ~ element(X0,the_carrier(sF493))
| set_difference(sK65(sF493,X0),set_difference(sK65(sF493,X0),X1)) = meet(sF493,sK65(sF493,X0),X1)
| ~ element(X1,the_carrier(sF493)) )
| spl495_6
| ~ spl495_61
| spl495_62 ),
inference(forward_subsumption_resolution,[],[f4844,f4788]) ).
fof(f4849,plain,
( ! [X0,X1] :
( ~ element(X0,powerset(sK477))
| set_difference(sK65(sF493,X0),set_difference(sK65(sF493,X0),X1)) = meet(sF493,sK65(sF493,X0),X1)
| ~ element(X1,the_carrier(sF493)) )
| spl495_6
| ~ spl495_61
| spl495_62 ),
inference(forward_demodulation,[],[f4847,f4804]) ).
fof(f4851,plain,
( ! [X0,X1] :
( ~ element(X1,powerset(sK477))
| ~ element(X0,powerset(sK477))
| set_difference(sK65(sF493,X0),set_difference(sK65(sF493,X0),X1)) = meet(sF493,sK65(sF493,X0),X1) )
| spl495_6
| ~ spl495_61
| spl495_62 ),
inference(forward_demodulation,[],[f4849,f4804]) ).
fof(f4880,plain,
! [X0] :
( ~ element(X0,powerset(sK477))
| bottom_of_semilattstr(sF493) = meet(sF493,X0,bottom_of_semilattstr(sF493))
| ~ lower_bounded_semilattstr(sF493)
| empty_carrier(sF493)
| ~ meet_semilatt_str(sF493) ),
inference(superposition,[],[f4767,f4804]) ).
fof(f4977,plain,
! [X0] : element(empty_set,powerset(X0)),
inference(resolution,[],[f2837,f4242]) ).
fof(f5197,plain,
! [X0] :
( meet(boole_lattice(X0),empty_set,bottom_of_semilattstr(boole_lattice(X0))) = set_difference(empty_set,set_difference(empty_set,bottom_of_semilattstr(boole_lattice(X0))))
| ~ meet_semilatt_str(boole_lattice(X0)) ),
inference(resolution,[],[f4977,f4803]) ).
fof(f5198,plain,
! [X0,X1] :
( meet(boole_lattice(X0),empty_set,X1) = set_difference(empty_set,set_difference(empty_set,X1))
| ~ element(X1,powerset(X0)) ),
inference(resolution,[],[f4977,f4805]) ).
fof(f5200,plain,
( ! [X0] :
( ~ element(X0,powerset(sK477))
| set_difference(sK65(sF493,X0),set_difference(sK65(sF493,X0),empty_set)) = meet(sF493,sK65(sF493,X0),empty_set) )
| spl495_6
| ~ spl495_61
| spl495_62 ),
inference(resolution,[],[f4977,f4851]) ).
fof(f5231,plain,
( ! [X0] :
( meet(sF493,sK65(sF493,X0),empty_set) = set_difference(sK65(sF493,X0),sK65(sF493,X0))
| ~ element(X0,powerset(sK477)) )
| spl495_6
| ~ spl495_61
| spl495_62 ),
inference(forward_demodulation,[],[f5200,f3633]) ).
fof(f5233,plain,
! [X0,X1] :
( ~ element(X1,powerset(X0))
| empty_set = meet(boole_lattice(X0),empty_set,X1) ),
inference(forward_demodulation,[],[f5198,f3682]) ).
fof(f5234,plain,
! [X0] : meet(boole_lattice(X0),empty_set,bottom_of_semilattstr(boole_lattice(X0))) = set_difference(empty_set,set_difference(empty_set,bottom_of_semilattstr(boole_lattice(X0)))),
inference(forward_subsumption_resolution,[],[f5197,f4816]) ).
fof(f5237,plain,
( ! [X0] :
( ~ element(X0,powerset(sK477))
| empty_set = meet(sF493,sK65(sF493,X0),empty_set) )
| spl495_6
| ~ spl495_61
| spl495_62 ),
inference(forward_demodulation,[],[f5231,f4479]) ).
fof(f5239,plain,
! [X0] : empty_set = meet(boole_lattice(X0),empty_set,bottom_of_semilattstr(boole_lattice(X0))),
inference(forward_demodulation,[],[f5234,f3682]) ).
fof(f5263,plain,
( empty_set = meet(sF493,sK65(sF493,empty_set),empty_set)
| spl495_6
| ~ spl495_61
| spl495_62 ),
inference(resolution,[],[f5237,f4977]) ).
fof(f5269,plain,
empty_set = meet(sF493,empty_set,bottom_of_semilattstr(sF493)),
inference(superposition,[],[f5239,f4431]) ).
fof(f5272,plain,
empty_set = meet(sF493,empty_set,sF494),
inference(forward_demodulation,[],[f5269,f4433]) ).
fof(f5319,plain,
( empty_set != empty_set
| ~ element(empty_set,the_carrier(sF493))
| empty_set != meet(sF493,empty_set,sK65(sF493,empty_set))
| lower_bounded_semilattstr(sF493)
| empty_carrier(sF493)
| ~ meet_semilatt_str(sF493)
| spl495_6
| ~ spl495_61
| spl495_62 ),
inference(superposition,[],[f2199,f5263]) ).
fof(f5320,plain,
( ~ element(empty_set,the_carrier(sF493))
| empty_set != meet(sF493,empty_set,sK65(sF493,empty_set))
| lower_bounded_semilattstr(sF493)
| empty_carrier(sF493)
| ~ meet_semilatt_str(sF493)
| spl495_6
| ~ spl495_61
| spl495_62 ),
inference(trivial_inequality_removal,[],[f5319]) ).
fof(f5321,plain,
( ~ element(empty_set,the_carrier(sF493))
| empty_set != meet(sF493,empty_set,sK65(sF493,empty_set))
| empty_carrier(sF493)
| ~ meet_semilatt_str(sF493)
| spl495_6
| ~ spl495_61
| spl495_62 ),
inference(forward_subsumption_resolution,[],[f5320,f4477]) ).
fof(f5322,plain,
( ~ element(empty_set,the_carrier(sF493))
| empty_set != meet(sF493,empty_set,sK65(sF493,empty_set))
| ~ meet_semilatt_str(sF493)
| spl495_6
| ~ spl495_61
| spl495_62 ),
inference(forward_subsumption_resolution,[],[f5321,f4792]) ).
fof(f5323,plain,
( ~ element(empty_set,the_carrier(sF493))
| empty_set != meet(sF493,empty_set,sK65(sF493,empty_set))
| spl495_6
| ~ spl495_61
| spl495_62 ),
inference(forward_subsumption_resolution,[],[f5322,f4788]) ).
fof(f5324,plain,
( ~ element(empty_set,powerset(sK477))
| empty_set != meet(sF493,empty_set,sK65(sF493,empty_set))
| spl495_6
| ~ spl495_61
| spl495_62 ),
inference(forward_demodulation,[],[f5323,f4804]) ).
fof(f5325,plain,
( empty_set != meet(sF493,empty_set,sK65(sF493,empty_set))
| spl495_6
| ~ spl495_61
| spl495_62 ),
inference(forward_subsumption_resolution,[],[f5324,f4977]) ).
fof(f5370,plain,
( ! [X0] :
( empty_set = meet(boole_lattice(sK477),empty_set,sK65(sF493,X0))
| ~ element(X0,powerset(sK477)) )
| spl495_6
| ~ spl495_61
| spl495_62 ),
inference(resolution,[],[f5233,f4846]) ).
fof(f5374,plain,
( ! [X0] :
( ~ element(X0,powerset(sK477))
| empty_set = meet(sF493,empty_set,sK65(sF493,X0)) )
| spl495_6
| ~ spl495_61
| spl495_62 ),
inference(forward_demodulation,[],[f5370,f4431]) ).
fof(f5378,plain,
( empty_set = meet(sF493,empty_set,sK65(sF493,empty_set))
| spl495_6
| ~ spl495_61
| spl495_62 ),
inference(resolution,[],[f5374,f4977]) ).
fof(f5384,plain,
( $false
| spl495_6
| ~ spl495_61
| spl495_62 ),
inference(forward_subsumption_resolution,[],[f5378,f5325]) ).
fof(f5385,plain,
( spl495_6
| ~ spl495_61
| spl495_62 ),
inference(avatar_contradiction_clause,[],[f5384]) ).
fof(f5386,plain,
( ! [X0] :
( ~ element(X0,powerset(sK477))
| bottom_of_semilattstr(sF493) = meet(sF493,X0,bottom_of_semilattstr(sF493))
| empty_carrier(sF493)
| ~ meet_semilatt_str(sF493) )
| ~ spl495_6 ),
inference(forward_subsumption_resolution,[],[f4880,f4476]) ).
fof(f5393,plain,
( ! [X0] :
( ~ element(X0,powerset(sK477))
| bottom_of_semilattstr(sF493) = meet(sF493,X0,bottom_of_semilattstr(sF493))
| ~ meet_semilatt_str(sF493) )
| ~ spl495_6
| spl495_62 ),
inference(forward_subsumption_resolution,[],[f5386,f4792]) ).
fof(f5395,plain,
( ! [X0] :
( ~ element(X0,powerset(sK477))
| bottom_of_semilattstr(sF493) = meet(sF493,X0,bottom_of_semilattstr(sF493)) )
| ~ spl495_6
| ~ spl495_61
| spl495_62 ),
inference(forward_subsumption_resolution,[],[f5393,f4788]) ).
fof(f5397,plain,
( ! [X0] :
( ~ element(X0,powerset(sK477))
| sF494 = meet(sF493,X0,sF494) )
| ~ spl495_6
| ~ spl495_61
| spl495_62 ),
inference(forward_demodulation,[],[f5395,f4433]) ).
fof(f5400,plain,
( sF494 = meet(sF493,empty_set,sF494)
| ~ spl495_6
| ~ spl495_61
| spl495_62 ),
inference(resolution,[],[f5397,f4977]) ).
fof(f5405,plain,
( empty_set = sF494
| ~ spl495_6
| ~ spl495_61
| spl495_62 ),
inference(forward_demodulation,[],[f5400,f5272]) ).
fof(f5407,plain,
( $false
| spl495_5
| ~ spl495_6
| ~ spl495_61
| spl495_62 ),
inference(forward_subsumption_resolution,[],[f5405,f4473]) ).
fof(f5408,plain,
( spl495_5
| ~ spl495_6
| ~ spl495_61
| spl495_62 ),
inference(avatar_contradiction_clause,[],[f5407]) ).
cnf(s3,plain,
( ~ spl495_5
| ~ spl495_6 ),
inference(sat_conversion,[],[f4478]) ).
cnf(s51,plain,
~ spl495_62,
inference(sat_conversion,[],[f4809]) ).
cnf(s52,plain,
spl495_61,
inference(sat_conversion,[],[f4819]) ).
cnf(s59,plain,
( spl495_6
| ~ spl495_61
| spl495_62 ),
inference(sat_conversion,[],[f5385]) ).
cnf(s60,plain,
( spl495_5
| ~ spl495_6
| ~ spl495_61
| spl495_62 ),
inference(sat_conversion,[],[f5408]) ).
cnf(s61,plain,
spl495_6,
inference(rat,[],[s59,s52,s51]) ).
cnf(s62,plain,
spl495_5,
inference(rat,[],[s60,s51,s52,s61]) ).
cnf(s64,plain,
$false,
inference(rat,[],[s3,s61,s62]) ).
fof(f5409,plain,
$false,
inference(avatar_sat_refutation,[],[s64]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU345+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.38 % Computer : n026.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.39 % CPULimit : 300
% 0.12/0.39 % WCLimit : 300
% 0.12/0.39 % DateTime : Mon Sep 28 04:52:12 UTC 2026
% 0.12/0.39 % CPUTime :
% 0.12/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.42 Running first-order theorem proving
% 0.12/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
% 7.12/2.05 % (3466442)Detected formulas, will run a generic FOF schedule.
% 7.12/2.05 % (3466447)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=2111647239:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 7.12/2.05 % (3466448)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=3675355633:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 7.12/2.05 % (3466450)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2963741183:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 7.12/2.05 % (3466449)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=1682285099:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 7.12/2.05 % (3466453)dis-21_1_sil=8000:lcm=predicate:random_seed=2457220824: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)
% 7.12/2.05 % (3466451)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2443507587:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 7.12/2.05 % (3466452)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3201542522:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 7.12/2.05 % (3466450)Instruction limit reached!
% 7.12/2.05 % (3466450)------------------------------
% 7.12/2.05 % (3466450)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.12/2.05 % (3466450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.12/2.05 % (3466450)CaDiCaL version: 2.1.3
% 7.12/2.05 % (3466450)Termination reason: Instruction limit
% 7.12/2.05 % (3466450)Termination phase: Saturation
% 7.12/2.05 % (3466450)Time elapsed: 0.060 s
% 7.12/2.05 % (3466450)Peak memory usage: 91 MB
% 7.12/2.05 % (3466450)Instructions burned: 110 (million)
% 7.12/2.05 % (3466453)Instruction limit reached!
% 7.12/2.05 % (3466453)------------------------------
% 7.12/2.05 % (3466453)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.12/2.05 % (3466453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.12/2.05 % (3466453)CaDiCaL version: 2.1.3
% 7.12/2.05 % (3466453)Termination reason: Instruction limit
% 7.12/2.05 % (3466453)Termination phase: Saturation
% 7.12/2.05 % (3466453)Time elapsed: 0.066 s
% 7.12/2.05 % (3466453)Peak memory usage: 91 MB
% 7.12/2.05 % (3466453)Instructions burned: 131 (million)
% 7.12/2.05 % (3466451)Instruction limit reached!
% 7.12/2.05 % (3466451)------------------------------
% 7.12/2.05 % (3466451)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.12/2.05 % (3466451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.12/2.05 % (3466451)CaDiCaL version: 2.1.3
% 7.12/2.05 % (3466451)Termination reason: Instruction limit
% 7.12/2.05 % (3466451)Termination phase: Saturation
% 7.12/2.05 % (3466451)Time elapsed: 0.076 s
% 7.12/2.05 % (3466451)Peak memory usage: 91 MB
% 7.12/2.05 % (3466451)Instructions burned: 120 (million)
% 7.12/2.05 % (3466452)Instruction limit reached!
% 7.12/2.05 % (3466452)------------------------------
% 7.12/2.05 % (3466452)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.12/2.05 % (3466452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.12/2.05 % (3466452)CaDiCaL version: 2.1.3
% 7.12/2.05 % (3466452)Termination reason: Instruction limit
% 7.12/2.05 % (3466452)Termination phase: Saturation
% 7.12/2.05 % (3466452)Time elapsed: 0.089 s
% 7.12/2.05 % (3466452)Peak memory usage: 92 MB
% 7.12/2.05 % (3466452)Instructions burned: 139 (million)
% 7.12/2.05 % (3466461)lrs+10_1_sil=8000:sp=occurrence:random_seed=4121103804:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 7.12/2.05 % (3466462)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2764430999:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 7.12/2.05 % (3466462)Refutation not found, incomplete strategy
% 7.12/2.05 % (3466462)------------------------------
% 7.12/2.05 % (3466462)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.12/2.05 % (3466462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.12/2.05 % (3466462)CaDiCaL version: 2.1.3
% 7.12/2.05 % (3466462)Termination reason: Refutation not found, incomplete strategy
% 7.12/2.05 % (3466462)Time elapsed: 0.008 s
% 7.12/2.05 % (3466462)Peak memory usage: 89 MB
% 7.12/2.05 % (3466462)Instructions burned: 10 (million)
% 7.12/2.05 % (3466463)lrs+1011_1_sil=32000:sp=occurrence:random_seed=881967670:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 7.12/2.05 % (3466464)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=2357766495:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 7.12/2.05 % (3466461)Instruction limit reached!
% 7.12/2.05 % (3466461)------------------------------
% 7.12/2.05 % (3466461)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.12/2.05 % (3466461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.12/2.05 % (3466461)CaDiCaL version: 2.1.3
% 7.12/2.05 % (3466461)Termination reason: Instruction limit
% 7.12/2.05 % (3466461)Termination phase: Saturation
% 7.12/2.05 % (3466461)Time elapsed: 0.182 s
% 7.12/2.05 % (3466461)Peak memory usage: 95 MB
% 7.12/2.05 % (3466461)Instructions burned: 286 (million)
% 7.12/2.05 % (3466464)Instruction limit reached!
% 7.12/2.05 % (3466464)------------------------------
% 7.12/2.05 % (3466464)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.12/2.05 % (3466464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.12/2.05 % (3466464)CaDiCaL version: 2.1.3
% 7.12/2.05 % (3466464)Termination reason: Instruction limit
% 7.12/2.05 % (3466464)Termination phase: Saturation
% 7.12/2.05 % (3466464)Time elapsed: 0.143 s
% 7.12/2.05 % (3466464)Peak memory usage: 94 MB
% 7.12/2.05 % (3466464)Instructions burned: 249 (million)
% 7.12/2.05 % (3466463)Instruction limit reached!
% 7.12/2.05 % (3466463)------------------------------
% 7.12/2.05 % (3466463)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.12/2.05 % (3466463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.12/2.05 % (3466463)CaDiCaL version: 2.1.3
% 7.12/2.05 % (3466463)Termination reason: Instruction limit
% 7.12/2.05 % (3466463)Termination phase: Saturation
% 7.12/2.05 % (3466463)Time elapsed: 0.224 s
% 7.12/2.05 % (3466463)Peak memory usage: 95 MB
% 7.12/2.05 % (3466463)Instructions burned: 326 (million)
% 7.12/2.05 % (3466462)------------------------------
% 7.12/2.05 % (3466462)------------------------------
% 7.12/2.05 % (3466469)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2923730438:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi)
% 7.12/2.05 % (3466470)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3961362978:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 7.12/2.05 % (3466469)Instruction limit reached!
% 7.12/2.05 % (3466469)------------------------------
% 7.12/2.05 % (3466469)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.12/2.05 % (3466469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.12/2.05 % (3466469)CaDiCaL version: 2.1.3
% 7.12/2.05 % (3466469)Termination reason: Instruction limit
% 7.12/2.05 % (3466469)Termination phase: Saturation
% 7.12/2.05 % (3466469)Time elapsed: 0.101 s
% 7.12/2.05 % (3466469)Peak memory usage: 93 MB
% 7.12/2.05 % (3466469)Instructions burned: 296 (million)
% 7.12/2.05 % (3466471)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2790037405:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi)
% 7.12/2.05 % (3466473)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=893720910:i=127:av=off:fsr=off:sup=off_2993 on theBenchmark for (2993ds/127Mi)
% 7.12/2.05 % (3466475)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3117069857:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2992 on theBenchmark for (2992ds/114Mi)
% 7.12/2.05 % (3466471)Instruction limit reached!
% 7.12/2.05 % (3466471)------------------------------
% 7.12/2.05 % (3466471)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.12/2.05 % (3466471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.12/2.05 % (3466471)CaDiCaL version: 2.1.3
% 7.12/2.05 % (3466471)Termination reason: Instruction limit
% 7.12/2.05 % (3466471)Termination phase: Saturation
% 7.12/2.05 % (3466471)Time elapsed: 0.066 s
% 7.12/2.05 % (3466471)Peak memory usage: 91 MB
% 7.12/2.05 % (3466471)Instructions burned: 114 (million)
% 7.12/2.05 % (3466473)Instruction limit reached!
% 7.12/2.05 % (3466473)------------------------------
% 7.12/2.05 % (3466473)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.12/2.05 % (3466473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.12/2.05 % (3466473)CaDiCaL version: 2.1.3
% 7.12/2.05 % (3466473)Termination reason: Instruction limit
% 7.12/2.05 % (3466473)Termination phase: Saturation
% 7.12/2.05 % (3466473)Time elapsed: 0.072 s
% 7.12/2.05 % (3466473)Peak memory usage: 91 MB
% 7.12/2.05 % (3466473)Instructions burned: 127 (million)
% 7.12/2.05 % (3466475)Instruction limit reached!
% 7.12/2.05 % (3466475)------------------------------
% 7.12/2.05 % (3466475)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.12/2.05 % (3466475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.12/2.05 % (3466475)CaDiCaL version: 2.1.3
% 7.12/2.05 % (3466475)Termination reason: Instruction limit
% 7.12/2.05 % (3466475)Termination phase: Saturation
% 7.12/2.05 % (3466475)Time elapsed: 0.036 s
% 7.12/2.05 % (3466475)Peak memory usage: 89 MB
% 7.12/2.05 % (3466475)Instructions burned: 117 (million)
% 7.12/2.05 % (3466447)First to succeed.
% 7.12/2.05 % (3466447)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3466442"
% 7.12/2.05 % (3466481)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=491700545:i=5202:ss=axioms:sgt=16_2991 on theBenchmark for (2991ds/5202Mi)
% 7.12/2.05 % (3466479)lrs+10_1_sil=8000:sp=occurrence:random_seed=2203812542:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2991 on theBenchmark for (2991ds/907Mi)
% 7.12/2.05 % (3466480)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=418879701:i=437:sd=1:aac=none:ss=included_2991 on theBenchmark for (2991ds/437Mi)
% 7.12/2.05 % (3466447)Refutation found. Thanks to Tanya!
% 7.12/2.05 % SZS status Theorem for theBenchmark
% 7.12/2.05 % SZS output start Proof for theBenchmark
% See solution above
% 8.86/2.24 % (3466447)------------------------------
% 8.86/2.24 % (3466447)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.86/2.24 % (3466447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.86/2.24 % (3466447)CaDiCaL version: 2.1.3
% 8.86/2.24 % (3466447)Termination reason: Refutation
% 8.86/2.24 % (3466447)Time elapsed: 0.808 s
% 8.86/2.24 % (3466447)Peak memory usage: 144 MB
% 8.86/2.24 % (3466447)Instructions burned: 1705 (million)
% 8.86/2.24 % (3466447)------------------------------
% 8.86/2.24 % (3466447)------------------------------
% 8.86/2.24 % (3466442)Success in time 1.187 s
% 8.86/2.24 % Vampire exiting
%------------------------------------------------------------------------------