%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : LAT302+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n018.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:48:18 AM UTC 2026
% Result : Theorem 0.18s 0.51s
% Output : Refutation 0.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 28
% Syntax : Number of formulae : 200 ( 32 unt; 13 def)
% Number of atoms : 597 ( 22 equ)
% Maximal formula atoms : 12 ( 2 avg)
% Number of connectives : 655 ( 258 ~; 292 |; 64 &)
% ( 22 <=>; 19 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 35 ( 33 usr; 14 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 1 con; 0-2 aty)
% Number of variables : 87 ( 0 sgn 85 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ( v13_lattices(X0)
=> m2_filter_2(k6_domain_1(u1_struct_0(X0),k5_lattices(X0)),X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t26_filter_2) ).
fof(f2,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ( v13_lattices(X0)
=> m2_filter_2(k6_domain_1(u1_struct_0(X0),k5_lattices(X0)),X0) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f15,axiom,
! [X0] :
( l3_lattices(X0)
=> ( v3_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k1_lattice2) ).
fof(f20,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_lattices(X0) )
=> m1_subset_1(k5_lattices(X0),u1_struct_0(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k5_lattices) ).
fof(f22,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l2_lattices(X0) )
=> m1_subset_1(k6_lattices(X0),u1_struct_0(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k6_lattices) ).
fof(f25,axiom,
! [X0] :
( l2_lattices(X0)
=> l1_struct_0(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l2_lattices) ).
fof(f26,axiom,
! [X0] :
( l3_lattices(X0)
=> ( l1_lattices(X0)
& l2_lattices(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l3_lattices) ).
fof(f48,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l3_lattices(X0) )
=> ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_lattice2) ).
fof(f49,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_struct_0(X0) )
=> ~ v1_xboole_0(u1_struct_0(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_struct_0) ).
fof(f60,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0))
& v4_lattices(k1_lattice2(X0))
& v5_lattices(k1_lattice2(X0))
& v6_lattices(k1_lattice2(X0))
& v7_lattices(k1_lattice2(X0))
& v8_lattices(k1_lattice2(X0))
& v9_lattices(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc6_lattice2) ).
fof(f78,axiom,
! [X0,X1] :
( ( ~ v1_xboole_0(X0)
& m1_subset_1(X1,X0) )
=> k6_domain_1(X0,X1) = k1_tarski(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k6_domain_1) ).
fof(f79,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_filter_2(X1,X0)
<=> m1_filter_0(X1,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_m1_filter_2) ).
fof(f82,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v14_lattices(X0)
& l3_lattices(X0) )
=> m1_filter_0(k6_domain_1(u1_struct_0(X0),k6_lattices(X0)),X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t13_filter_0) ).
fof(f84,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_filter_2(X1,X0)
<=> m1_filter_2(X1,k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t21_filter_2) ).
fof(f89,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ( v13_lattices(X0)
<=> v14_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t63_lattice2) ).
fof(f91,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v13_lattices(X0)
& l3_lattices(X0) )
=> k5_lattices(X0) = k6_lattices(k1_lattice2(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t78_lattice2) ).
fof(f107,plain,
? [X0] :
( ~ m2_filter_2(k6_domain_1(u1_struct_0(X0),k5_lattices(X0)),X0)
& v13_lattices(X0)
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(ennf_transformation,[],[f2]) ).
fof(f108,plain,
? [X0] :
( ~ m2_filter_2(k6_domain_1(u1_struct_0(X0),k5_lattices(X0)),X0)
& v13_lattices(X0)
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(flattening,[],[f107]) ).
fof(f128,plain,
! [X0] :
( ( v3_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) )
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f15]) ).
fof(f129,plain,
! [X0] :
( m1_subset_1(k5_lattices(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_lattices(X0) ),
inference(ennf_transformation,[],[f20]) ).
fof(f130,plain,
! [X0] :
( m1_subset_1(k5_lattices(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_lattices(X0) ),
inference(flattening,[],[f129]) ).
fof(f133,plain,
! [X0] :
( m1_subset_1(k6_lattices(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l2_lattices(X0) ),
inference(ennf_transformation,[],[f22]) ).
fof(f134,plain,
! [X0] :
( m1_subset_1(k6_lattices(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l2_lattices(X0) ),
inference(flattening,[],[f133]) ).
fof(f136,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l2_lattices(X0) ),
inference(ennf_transformation,[],[f25]) ).
fof(f137,plain,
! [X0] :
( ( l1_lattices(X0)
& l2_lattices(X0) )
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f26]) ).
fof(f157,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f48]) ).
fof(f158,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f157]) ).
fof(f159,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f49]) ).
fof(f160,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(flattening,[],[f159]) ).
fof(f173,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0))
& v4_lattices(k1_lattice2(X0))
& v5_lattices(k1_lattice2(X0))
& v6_lattices(k1_lattice2(X0))
& v7_lattices(k1_lattice2(X0))
& v8_lattices(k1_lattice2(X0))
& v9_lattices(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f60]) ).
fof(f174,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0))
& v4_lattices(k1_lattice2(X0))
& v5_lattices(k1_lattice2(X0))
& v6_lattices(k1_lattice2(X0))
& v7_lattices(k1_lattice2(X0))
& v8_lattices(k1_lattice2(X0))
& v9_lattices(k1_lattice2(X0))
& v10_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f173]) ).
fof(f182,plain,
! [X0,X1] :
( k6_domain_1(X0,X1) = k1_tarski(X1)
| v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0) ),
inference(ennf_transformation,[],[f78]) ).
fof(f183,plain,
! [X0,X1] :
( k6_domain_1(X0,X1) = k1_tarski(X1)
| v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0) ),
inference(flattening,[],[f182]) ).
fof(f184,plain,
! [X0] :
( ! [X1] :
( m1_filter_2(X1,X0)
<=> m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f79]) ).
fof(f185,plain,
! [X0] :
( ! [X1] :
( m1_filter_2(X1,X0)
<=> m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f184]) ).
fof(f186,plain,
! [X0] :
( m1_filter_0(k6_domain_1(u1_struct_0(X0),k6_lattices(X0)),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v14_lattices(X0)
| ~ l3_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f82]) ).
fof(f187,plain,
! [X0] :
( m1_filter_0(k6_domain_1(u1_struct_0(X0),k6_lattices(X0)),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v14_lattices(X0)
| ~ l3_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f186]) ).
fof(f189,plain,
! [X0] :
( ! [X1] :
( m2_filter_2(X1,X0)
<=> m1_filter_2(X1,k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f84]) ).
fof(f190,plain,
! [X0] :
( ! [X1] :
( m2_filter_2(X1,X0)
<=> m1_filter_2(X1,k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f189]) ).
fof(f197,plain,
! [X0] :
( ( v13_lattices(X0)
<=> v14_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f89]) ).
fof(f198,plain,
! [X0] :
( ( v13_lattices(X0)
<=> v14_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f197]) ).
fof(f200,plain,
! [X0] :
( k5_lattices(X0) = k6_lattices(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v13_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f91]) ).
fof(f201,plain,
! [X0] :
( k5_lattices(X0) = k6_lattices(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v13_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f200]) ).
fof(f204,plain,
l3_lattices(sK0),
inference(cnf_transformation,[],[f108]) ).
fof(f205,plain,
v10_lattices(sK0),
inference(cnf_transformation,[],[f108]) ).
fof(f206,plain,
~ v3_struct_0(sK0),
inference(cnf_transformation,[],[f108]) ).
fof(f207,plain,
v13_lattices(sK0),
inference(cnf_transformation,[],[f108]) ).
fof(f208,plain,
~ m2_filter_2(k6_domain_1(u1_struct_0(sK0),k5_lattices(sK0)),sK0),
inference(cnf_transformation,[],[f108]) ).
fof(f227,plain,
! [X0] :
( ~ l3_lattices(X0)
| l3_lattices(k1_lattice2(X0)) ),
inference(cnf_transformation,[],[f128]) ).
fof(f229,plain,
! [X0] :
( ~ l1_lattices(X0)
| v3_struct_0(X0)
| m1_subset_1(k5_lattices(X0),u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f130]) ).
fof(f231,plain,
! [X0] :
( ~ l2_lattices(X0)
| v3_struct_0(X0)
| m1_subset_1(k6_lattices(X0),u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f134]) ).
fof(f233,plain,
! [X0] :
( ~ l2_lattices(X0)
| l1_struct_0(X0) ),
inference(cnf_transformation,[],[f136]) ).
fof(f234,plain,
! [X0] :
( ~ l3_lattices(X0)
| l2_lattices(X0) ),
inference(cnf_transformation,[],[f137]) ).
fof(f235,plain,
! [X0] :
( ~ l3_lattices(X0)
| l1_lattices(X0) ),
inference(cnf_transformation,[],[f137]) ).
fof(f262,plain,
! [X0] :
( ~ l3_lattices(X0)
| v3_struct_0(X0)
| ~ v3_struct_0(k1_lattice2(X0)) ),
inference(cnf_transformation,[],[f158]) ).
fof(f263,plain,
! [X0] :
( ~ l1_struct_0(X0)
| v3_struct_0(X0)
| ~ v1_xboole_0(u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f160]) ).
fof(f284,plain,
! [X0] :
( ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| v10_lattices(k1_lattice2(X0)) ),
inference(cnf_transformation,[],[f174]) ).
fof(f347,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,X0)
| v1_xboole_0(X0)
| k6_domain_1(X0,X1) = k1_tarski(X1) ),
inference(cnf_transformation,[],[f183]) ).
fof(f348,plain,
! [X0,X1] :
( ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ~ m1_filter_0(X1,X0)
| m1_filter_2(X1,X0) ),
inference(cnf_transformation,[],[f185]) ).
fof(f353,plain,
! [X0] :
( ~ l3_lattices(X0)
| ~ v14_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| m1_filter_0(k6_domain_1(u1_struct_0(X0),k6_lattices(X0)),X0) ),
inference(cnf_transformation,[],[f187]) ).
fof(f355,plain,
! [X0,X1] :
( ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| ~ m1_filter_2(X1,k1_lattice2(X0))
| m2_filter_2(X1,X0) ),
inference(cnf_transformation,[],[f190]) ).
fof(f362,plain,
! [X0] :
( ~ l3_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| v14_lattices(k1_lattice2(X0))
| ~ v13_lattices(X0) ),
inference(cnf_transformation,[],[f198]) ).
fof(f364,plain,
! [X0] :
( ~ l3_lattices(X0)
| ~ v13_lattices(X0)
| ~ v10_lattices(X0)
| v3_struct_0(X0)
| k5_lattices(X0) = k6_lattices(k1_lattice2(X0)) ),
inference(cnf_transformation,[],[f201]) ).
fof(f367,plain,
m2_filter_2(k6_domain_1(u1_struct_0(sK0),k5_lattices(sK0)),sK0),
inference(consistent_polarity_flipping,[],[f208]) ).
fof(f368,plain,
~ v13_lattices(sK0),
inference(consistent_polarity_flipping,[],[f207]) ).
fof(f369,plain,
v3_struct_0(sK0),
inference(consistent_polarity_flipping,[],[f206]) ).
fof(f370,plain,
~ l3_lattices(sK0),
inference(consistent_polarity_flipping,[],[f204]) ).
fof(f388,plain,
! [X0] :
( ~ l3_lattices(k1_lattice2(X0))
| l3_lattices(X0) ),
inference(consistent_polarity_flipping,[],[f227]) ).
fof(f389,plain,
! [X0] :
( m1_subset_1(k5_lattices(X0),u1_struct_0(X0))
| ~ v3_struct_0(X0)
| l1_lattices(X0) ),
inference(consistent_polarity_flipping,[],[f229]) ).
fof(f390,plain,
! [X0] :
( m1_subset_1(k6_lattices(X0),u1_struct_0(X0))
| ~ v3_struct_0(X0)
| l2_lattices(X0) ),
inference(consistent_polarity_flipping,[],[f231]) ).
fof(f392,plain,
! [X0] :
( l1_struct_0(X0)
| l2_lattices(X0) ),
inference(consistent_polarity_flipping,[],[f233]) ).
fof(f393,plain,
! [X0] :
( ~ l1_lattices(X0)
| l3_lattices(X0) ),
inference(consistent_polarity_flipping,[],[f235]) ).
fof(f394,plain,
! [X0] :
( ~ l2_lattices(X0)
| l3_lattices(X0) ),
inference(consistent_polarity_flipping,[],[f234]) ).
fof(f415,plain,
! [X0] :
( v3_struct_0(k1_lattice2(X0))
| ~ v3_struct_0(X0)
| l3_lattices(X0) ),
inference(consistent_polarity_flipping,[],[f262]) ).
fof(f417,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| ~ v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(consistent_polarity_flipping,[],[f263]) ).
fof(f440,plain,
! [X0] :
( v10_lattices(k1_lattice2(X0))
| ~ v10_lattices(X0)
| ~ v3_struct_0(X0)
| l3_lattices(X0) ),
inference(consistent_polarity_flipping,[],[f284]) ).
fof(f471,plain,
! [X0,X1] :
( ~ m1_filter_2(X1,X0)
| ~ v10_lattices(X0)
| ~ v3_struct_0(X0)
| ~ m1_filter_0(X1,X0)
| l3_lattices(X0) ),
inference(consistent_polarity_flipping,[],[f348]) ).
fof(f472,plain,
! [X0] :
( m1_filter_0(k6_domain_1(u1_struct_0(X0),k6_lattices(X0)),X0)
| v14_lattices(X0)
| ~ v10_lattices(X0)
| ~ v3_struct_0(X0)
| l3_lattices(X0) ),
inference(consistent_polarity_flipping,[],[f353]) ).
fof(f474,plain,
! [X0,X1] :
( ~ m2_filter_2(X1,X0)
| ~ v10_lattices(X0)
| ~ v3_struct_0(X0)
| m1_filter_2(X1,k1_lattice2(X0))
| l3_lattices(X0) ),
inference(consistent_polarity_flipping,[],[f355]) ).
fof(f475,plain,
! [X0] :
( ~ v14_lattices(k1_lattice2(X0))
| ~ v10_lattices(X0)
| ~ v3_struct_0(X0)
| l3_lattices(X0)
| v13_lattices(X0) ),
inference(consistent_polarity_flipping,[],[f362]) ).
fof(f477,plain,
! [X0] :
( v13_lattices(X0)
| l3_lattices(X0)
| ~ v10_lattices(X0)
| ~ v3_struct_0(X0)
| k5_lattices(X0) = k6_lattices(k1_lattice2(X0)) ),
inference(consistent_polarity_flipping,[],[f364]) ).
fof(f535,plain,
! [X0] :
( v1_xboole_0(u1_struct_0(X0))
| k6_domain_1(u1_struct_0(X0),k5_lattices(X0)) = k1_tarski(k5_lattices(X0))
| ~ v3_struct_0(X0)
| l1_lattices(X0) ),
inference(resolution,[],[f347,f389]) ).
fof(f589,plain,
( ~ v10_lattices(sK0)
| ~ v3_struct_0(sK0)
| m1_filter_2(k6_domain_1(u1_struct_0(sK0),k5_lattices(sK0)),k1_lattice2(sK0))
| l3_lattices(sK0) ),
inference(resolution,[],[f474,f367]) ).
fof(f592,plain,
( ~ v3_struct_0(sK0)
| m1_filter_2(k6_domain_1(u1_struct_0(sK0),k5_lattices(sK0)),k1_lattice2(sK0))
| l3_lattices(sK0) ),
inference(forward_subsumption_resolution,[],[f589,f205]) ).
fof(f593,plain,
( m1_filter_2(k6_domain_1(u1_struct_0(sK0),k5_lattices(sK0)),k1_lattice2(sK0))
| l3_lattices(sK0) ),
inference(forward_subsumption_resolution,[],[f592,f369]) ).
fof(f594,plain,
m1_filter_2(k6_domain_1(u1_struct_0(sK0),k5_lattices(sK0)),k1_lattice2(sK0)),
inference(forward_subsumption_resolution,[],[f593,f370]) ).
fof(f604,plain,
( l3_lattices(sK0)
| ~ v10_lattices(sK0)
| ~ v3_struct_0(sK0)
| k5_lattices(sK0) = k6_lattices(k1_lattice2(sK0)) ),
inference(resolution,[],[f477,f368]) ).
fof(f611,plain,
( ~ v10_lattices(sK0)
| ~ v3_struct_0(sK0)
| k5_lattices(sK0) = k6_lattices(k1_lattice2(sK0)) ),
inference(forward_subsumption_resolution,[],[f604,f370]) ).
fof(f613,plain,
( ~ v3_struct_0(sK0)
| k5_lattices(sK0) = k6_lattices(k1_lattice2(sK0)) ),
inference(forward_subsumption_resolution,[],[f611,f205]) ).
fof(f615,plain,
k5_lattices(sK0) = k6_lattices(k1_lattice2(sK0)),
inference(forward_subsumption_resolution,[],[f613,f369]) ).
fof(f618,plain,
( m1_filter_0(k6_domain_1(u1_struct_0(k1_lattice2(sK0)),k5_lattices(sK0)),k1_lattice2(sK0))
| v14_lattices(k1_lattice2(sK0))
| ~ v10_lattices(k1_lattice2(sK0))
| ~ v3_struct_0(k1_lattice2(sK0))
| l3_lattices(k1_lattice2(sK0)) ),
inference(superposition,[],[f472,f615]) ).
fof(f619,plain,
( m1_subset_1(k5_lattices(sK0),u1_struct_0(k1_lattice2(sK0)))
| ~ v3_struct_0(k1_lattice2(sK0))
| l2_lattices(k1_lattice2(sK0)) ),
inference(superposition,[],[f390,f615]) ).
fof(f621,definition,
( spl28_1
<=> l2_lattices(k1_lattice2(sK0)) ),
introduced(definition,[new_symbols(definition,[spl28_1])],[avatar_definition]) ).
fof(f622,plain,
( ~ l2_lattices(k1_lattice2(sK0))
| spl28_1 ),
inference(avatar_component_clause,[],[f621]) ).
fof(f623,plain,
( l2_lattices(k1_lattice2(sK0))
| ~ spl28_1 ),
inference(avatar_component_clause,[],[f621]) ).
fof(f625,definition,
( spl28_2
<=> v3_struct_0(k1_lattice2(sK0)) ),
introduced(definition,[new_symbols(definition,[spl28_2])],[avatar_definition]) ).
fof(f626,plain,
( v3_struct_0(k1_lattice2(sK0))
| ~ spl28_2 ),
inference(avatar_component_clause,[],[f625]) ).
fof(f627,plain,
( ~ v3_struct_0(k1_lattice2(sK0))
| spl28_2 ),
inference(avatar_component_clause,[],[f625]) ).
fof(f629,definition,
( spl28_3
<=> m1_subset_1(k5_lattices(sK0),u1_struct_0(k1_lattice2(sK0))) ),
introduced(definition,[new_symbols(definition,[spl28_3])],[avatar_definition]) ).
fof(f631,plain,
( m1_subset_1(k5_lattices(sK0),u1_struct_0(k1_lattice2(sK0)))
| ~ spl28_3 ),
inference(avatar_component_clause,[],[f629]) ).
fof(f632,plain,
( spl28_1
| ~ spl28_2
| spl28_3 ),
inference(avatar_split_clause,[],[f619,f629,f625,f621]) ).
fof(f634,definition,
( spl28_4
<=> l3_lattices(k1_lattice2(sK0)) ),
introduced(definition,[new_symbols(definition,[spl28_4])],[avatar_definition]) ).
fof(f635,plain,
( ~ l3_lattices(k1_lattice2(sK0))
| spl28_4 ),
inference(avatar_component_clause,[],[f634]) ).
fof(f636,plain,
( l3_lattices(k1_lattice2(sK0))
| ~ spl28_4 ),
inference(avatar_component_clause,[],[f634]) ).
fof(f638,definition,
( spl28_5
<=> v10_lattices(k1_lattice2(sK0)) ),
introduced(definition,[new_symbols(definition,[spl28_5])],[avatar_definition]) ).
fof(f639,plain,
( v10_lattices(k1_lattice2(sK0))
| ~ spl28_5 ),
inference(avatar_component_clause,[],[f638]) ).
fof(f640,plain,
( ~ v10_lattices(k1_lattice2(sK0))
| spl28_5 ),
inference(avatar_component_clause,[],[f638]) ).
fof(f642,definition,
( spl28_6
<=> v14_lattices(k1_lattice2(sK0)) ),
introduced(definition,[new_symbols(definition,[spl28_6])],[avatar_definition]) ).
fof(f644,plain,
( v14_lattices(k1_lattice2(sK0))
| ~ spl28_6 ),
inference(avatar_component_clause,[],[f642]) ).
fof(f646,definition,
( spl28_7
<=> m1_filter_0(k6_domain_1(u1_struct_0(k1_lattice2(sK0)),k5_lattices(sK0)),k1_lattice2(sK0)) ),
introduced(definition,[new_symbols(definition,[spl28_7])],[avatar_definition]) ).
fof(f648,plain,
( m1_filter_0(k6_domain_1(u1_struct_0(k1_lattice2(sK0)),k5_lattices(sK0)),k1_lattice2(sK0))
| ~ spl28_7 ),
inference(avatar_component_clause,[],[f646]) ).
fof(f649,plain,
( spl28_4
| ~ spl28_2
| ~ spl28_5
| spl28_6
| spl28_7 ),
inference(avatar_split_clause,[],[f618,f646,f642,f638,f625,f634]) ).
fof(f650,plain,
( ~ v3_struct_0(sK0)
| l3_lattices(sK0)
| spl28_2 ),
inference(resolution,[],[f627,f415]) ).
fof(f651,plain,
( l3_lattices(sK0)
| spl28_2 ),
inference(forward_subsumption_resolution,[],[f650,f369]) ).
fof(f652,plain,
( $false
| spl28_2 ),
inference(forward_subsumption_resolution,[],[f651,f370]) ).
fof(f653,plain,
spl28_2,
inference(avatar_contradiction_clause,[],[f652]) ).
fof(f654,plain,
( ~ v10_lattices(sK0)
| ~ v3_struct_0(sK0)
| l3_lattices(sK0)
| spl28_5 ),
inference(resolution,[],[f640,f440]) ).
fof(f655,plain,
( ~ v3_struct_0(sK0)
| l3_lattices(sK0)
| spl28_5 ),
inference(forward_subsumption_resolution,[],[f654,f205]) ).
fof(f656,plain,
( l3_lattices(sK0)
| spl28_5 ),
inference(forward_subsumption_resolution,[],[f655,f369]) ).
fof(f657,plain,
( $false
| spl28_5 ),
inference(forward_subsumption_resolution,[],[f656,f370]) ).
fof(f658,plain,
spl28_5,
inference(avatar_contradiction_clause,[],[f657]) ).
fof(f672,plain,
( ~ v10_lattices(sK0)
| ~ v3_struct_0(sK0)
| l3_lattices(sK0)
| v13_lattices(sK0)
| ~ spl28_6 ),
inference(resolution,[],[f644,f475]) ).
fof(f675,plain,
( ~ v3_struct_0(sK0)
| l3_lattices(sK0)
| v13_lattices(sK0)
| ~ spl28_6 ),
inference(forward_subsumption_resolution,[],[f672,f205]) ).
fof(f681,plain,
( l3_lattices(sK0)
| v13_lattices(sK0)
| ~ spl28_6 ),
inference(forward_subsumption_resolution,[],[f675,f369]) ).
fof(f682,plain,
( v13_lattices(sK0)
| ~ spl28_6 ),
inference(forward_subsumption_resolution,[],[f681,f370]) ).
fof(f683,plain,
( $false
| ~ spl28_6 ),
inference(forward_subsumption_resolution,[],[f682,f368]) ).
fof(f684,plain,
~ spl28_6,
inference(avatar_contradiction_clause,[],[f683]) ).
fof(f690,plain,
( ~ v10_lattices(k1_lattice2(sK0))
| ~ v3_struct_0(k1_lattice2(sK0))
| ~ m1_filter_0(k6_domain_1(u1_struct_0(sK0),k5_lattices(sK0)),k1_lattice2(sK0))
| l3_lattices(k1_lattice2(sK0)) ),
inference(resolution,[],[f594,f471]) ).
fof(f691,plain,
( ~ v3_struct_0(k1_lattice2(sK0))
| ~ m1_filter_0(k6_domain_1(u1_struct_0(sK0),k5_lattices(sK0)),k1_lattice2(sK0))
| l3_lattices(k1_lattice2(sK0))
| ~ spl28_5 ),
inference(forward_subsumption_resolution,[],[f690,f639]) ).
fof(f692,plain,
( ~ m1_filter_0(k6_domain_1(u1_struct_0(sK0),k5_lattices(sK0)),k1_lattice2(sK0))
| l3_lattices(k1_lattice2(sK0))
| ~ spl28_2
| ~ spl28_5 ),
inference(forward_subsumption_resolution,[],[f691,f626]) ).
fof(f694,definition,
( spl28_9
<=> m1_filter_0(k6_domain_1(u1_struct_0(sK0),k5_lattices(sK0)),k1_lattice2(sK0)) ),
introduced(definition,[new_symbols(definition,[spl28_9])],[avatar_definition]) ).
fof(f696,plain,
( ~ m1_filter_0(k6_domain_1(u1_struct_0(sK0),k5_lattices(sK0)),k1_lattice2(sK0))
| spl28_9 ),
inference(avatar_component_clause,[],[f694]) ).
fof(f697,plain,
( spl28_4
| ~ spl28_9
| ~ spl28_2
| ~ spl28_5 ),
inference(avatar_split_clause,[],[f692,f638,f625,f694,f634]) ).
fof(f730,plain,
( l3_lattices(sK0)
| ~ spl28_4 ),
inference(resolution,[],[f636,f388]) ).
fof(f731,plain,
( $false
| ~ spl28_4 ),
inference(forward_subsumption_resolution,[],[f730,f370]) ).
fof(f732,plain,
~ spl28_4,
inference(avatar_contradiction_clause,[],[f731]) ).
fof(f756,definition,
( spl28_17
<=> v1_xboole_0(u1_struct_0(k1_lattice2(sK0))) ),
introduced(definition,[new_symbols(definition,[spl28_17])],[avatar_definition]) ).
fof(f757,plain,
( ~ v1_xboole_0(u1_struct_0(k1_lattice2(sK0)))
| spl28_17 ),
inference(avatar_component_clause,[],[f756]) ).
fof(f758,plain,
( v1_xboole_0(u1_struct_0(k1_lattice2(sK0)))
| ~ spl28_17 ),
inference(avatar_component_clause,[],[f756]) ).
fof(f769,definition,
( spl28_20
<=> k6_domain_1(u1_struct_0(k1_lattice2(sK0)),k5_lattices(sK0)) = k1_tarski(k5_lattices(sK0)) ),
introduced(definition,[new_symbols(definition,[spl28_20])],[avatar_definition]) ).
fof(f771,plain,
( k6_domain_1(u1_struct_0(k1_lattice2(sK0)),k5_lattices(sK0)) = k1_tarski(k5_lattices(sK0))
| ~ spl28_20 ),
inference(avatar_component_clause,[],[f769]) ).
fof(f773,plain,
( l3_lattices(k1_lattice2(sK0))
| ~ spl28_1 ),
inference(resolution,[],[f623,f394]) ).
fof(f774,plain,
( $false
| ~ spl28_1
| spl28_4 ),
inference(forward_subsumption_resolution,[],[f773,f635]) ).
fof(f775,plain,
( ~ spl28_1
| spl28_4 ),
inference(avatar_contradiction_clause,[],[f774]) ).
fof(f778,plain,
( ~ v3_struct_0(k1_lattice2(sK0))
| ~ l1_struct_0(k1_lattice2(sK0))
| ~ spl28_17 ),
inference(resolution,[],[f758,f417]) ).
fof(f784,plain,
( ~ l1_struct_0(k1_lattice2(sK0))
| ~ spl28_2
| ~ spl28_17 ),
inference(forward_subsumption_resolution,[],[f778,f626]) ).
fof(f814,plain,
( l2_lattices(k1_lattice2(sK0))
| ~ spl28_2
| ~ spl28_17 ),
inference(resolution,[],[f784,f392]) ).
fof(f816,plain,
( $false
| spl28_1
| ~ spl28_2
| ~ spl28_17 ),
inference(forward_subsumption_resolution,[],[f814,f622]) ).
fof(f817,plain,
( spl28_1
| ~ spl28_2
| ~ spl28_17 ),
inference(avatar_contradiction_clause,[],[f816]) ).
fof(f875,plain,
( v1_xboole_0(u1_struct_0(k1_lattice2(sK0)))
| k6_domain_1(u1_struct_0(k1_lattice2(sK0)),k5_lattices(sK0)) = k1_tarski(k5_lattices(sK0))
| ~ spl28_3 ),
inference(resolution,[],[f631,f347]) ).
fof(f878,plain,
( k6_domain_1(u1_struct_0(k1_lattice2(sK0)),k5_lattices(sK0)) = k1_tarski(k5_lattices(sK0))
| ~ spl28_3
| spl28_17 ),
inference(forward_subsumption_resolution,[],[f875,f757]) ).
fof(f880,plain,
( spl28_20
| ~ spl28_3
| spl28_17 ),
inference(avatar_split_clause,[],[f878,f756,f629,f769]) ).
fof(f919,plain,
( m1_filter_0(k1_tarski(k5_lattices(sK0)),k1_lattice2(sK0))
| ~ spl28_7
| ~ spl28_20 ),
inference(superposition,[],[f648,f771]) ).
fof(f1279,definition,
( spl28_48
<=> v1_xboole_0(u1_struct_0(sK0)) ),
introduced(definition,[new_symbols(definition,[spl28_48])],[avatar_definition]) ).
fof(f1280,plain,
( ~ v1_xboole_0(u1_struct_0(sK0))
| spl28_48 ),
inference(avatar_component_clause,[],[f1279]) ).
fof(f1281,plain,
( v1_xboole_0(u1_struct_0(sK0))
| ~ spl28_48 ),
inference(avatar_component_clause,[],[f1279]) ).
fof(f1301,plain,
( ~ v3_struct_0(sK0)
| ~ l1_struct_0(sK0)
| ~ spl28_48 ),
inference(resolution,[],[f1281,f417]) ).
fof(f1308,plain,
( ~ l1_struct_0(sK0)
| ~ spl28_48 ),
inference(forward_subsumption_resolution,[],[f1301,f369]) ).
fof(f1309,plain,
( l2_lattices(sK0)
| ~ spl28_48 ),
inference(resolution,[],[f1308,f392]) ).
fof(f1325,plain,
( l3_lattices(sK0)
| ~ spl28_48 ),
inference(resolution,[],[f1309,f394]) ).
fof(f1326,plain,
( $false
| ~ spl28_48 ),
inference(forward_subsumption_resolution,[],[f1325,f370]) ).
fof(f1327,plain,
~ spl28_48,
inference(avatar_contradiction_clause,[],[f1326]) ).
fof(f1332,plain,
( k6_domain_1(u1_struct_0(sK0),k5_lattices(sK0)) = k1_tarski(k5_lattices(sK0))
| ~ v3_struct_0(sK0)
| l1_lattices(sK0)
| spl28_48 ),
inference(resolution,[],[f1280,f535]) ).
fof(f1335,plain,
( k6_domain_1(u1_struct_0(sK0),k5_lattices(sK0)) = k1_tarski(k5_lattices(sK0))
| l1_lattices(sK0)
| spl28_48 ),
inference(forward_subsumption_resolution,[],[f1332,f369]) ).
fof(f1338,definition,
( spl28_55
<=> l1_lattices(sK0) ),
introduced(definition,[new_symbols(definition,[spl28_55])],[avatar_definition]) ).
fof(f1340,plain,
( l1_lattices(sK0)
| ~ spl28_55 ),
inference(avatar_component_clause,[],[f1338]) ).
fof(f1342,definition,
( spl28_56
<=> k6_domain_1(u1_struct_0(sK0),k5_lattices(sK0)) = k1_tarski(k5_lattices(sK0)) ),
introduced(definition,[new_symbols(definition,[spl28_56])],[avatar_definition]) ).
fof(f1344,plain,
( k6_domain_1(u1_struct_0(sK0),k5_lattices(sK0)) = k1_tarski(k5_lattices(sK0))
| ~ spl28_56 ),
inference(avatar_component_clause,[],[f1342]) ).
fof(f1345,plain,
( spl28_55
| spl28_56
| spl28_48 ),
inference(avatar_split_clause,[],[f1335,f1279,f1342,f1338]) ).
fof(f1358,plain,
( l3_lattices(sK0)
| ~ spl28_55 ),
inference(resolution,[],[f1340,f393]) ).
fof(f1359,plain,
( $false
| ~ spl28_55 ),
inference(forward_subsumption_resolution,[],[f1358,f370]) ).
fof(f1360,plain,
~ spl28_55,
inference(avatar_contradiction_clause,[],[f1359]) ).
fof(f1455,plain,
( ~ m1_filter_0(k1_tarski(k5_lattices(sK0)),k1_lattice2(sK0))
| spl28_9
| ~ spl28_56 ),
inference(superposition,[],[f696,f1344]) ).
fof(f1460,plain,
( $false
| ~ spl28_7
| spl28_9
| ~ spl28_20
| ~ spl28_56 ),
inference(forward_subsumption_resolution,[],[f1455,f919]) ).
fof(f1461,plain,
( ~ spl28_7
| spl28_9
| ~ spl28_20
| ~ spl28_56 ),
inference(avatar_contradiction_clause,[],[f1460]) ).
cnf(s1,plain,
( spl28_1
| ~ spl28_2
| spl28_3 ),
inference(sat_conversion,[],[f632]) ).
cnf(s2,plain,
( ~ spl28_2
| spl28_4
| ~ spl28_5
| spl28_6
| spl28_7 ),
inference(sat_conversion,[],[f649]) ).
cnf(s3,plain,
spl28_2,
inference(sat_conversion,[],[f653]) ).
cnf(s4,plain,
spl28_5,
inference(sat_conversion,[],[f658]) ).
cnf(s6,plain,
~ spl28_6,
inference(sat_conversion,[],[f684]) ).
cnf(s7,plain,
( ~ spl28_2
| spl28_4
| ~ spl28_5
| ~ spl28_9 ),
inference(sat_conversion,[],[f697]) ).
cnf(s10,plain,
~ spl28_4,
inference(sat_conversion,[],[f732]) ).
cnf(s13,plain,
( ~ spl28_1
| spl28_4 ),
inference(sat_conversion,[],[f775]) ).
cnf(s16,plain,
( spl28_1
| ~ spl28_2
| ~ spl28_17 ),
inference(sat_conversion,[],[f817]) ).
cnf(s18,plain,
( ~ spl28_3
| spl28_17
| spl28_20 ),
inference(sat_conversion,[],[f880]) ).
cnf(s46,plain,
~ spl28_48,
inference(sat_conversion,[],[f1327]) ).
cnf(s47,plain,
( spl28_48
| spl28_55
| spl28_56 ),
inference(sat_conversion,[],[f1345]) ).
cnf(s49,plain,
~ spl28_55,
inference(sat_conversion,[],[f1360]) ).
cnf(s52,plain,
( ~ spl28_7
| spl28_9
| ~ spl28_20
| ~ spl28_56 ),
inference(sat_conversion,[],[f1461]) ).
cnf(s55,plain,
( spl28_48
| spl28_56 ),
inference(rat,[],[s47,s49]) ).
cnf(s57,plain,
spl28_56,
inference(rat,[],[s55,s46]) ).
cnf(s71,plain,
~ spl28_1,
inference(rat,[],[s13,s10]) ).
cnf(s74,plain,
( ~ spl28_2
| ~ spl28_5
| ~ spl28_9 ),
inference(rat,[],[s7,s10]) ).
cnf(s75,plain,
~ spl28_17,
inference(rat,[],[s16,s71,s3]) ).
cnf(s76,plain,
~ spl28_9,
inference(rat,[],[s74,s4,s3]) ).
cnf(s78,plain,
spl28_7,
inference(rat,[],[s2,s6,s4,s10,s3]) ).
cnf(s79,plain,
~ spl28_20,
inference(rat,[],[s52,s57,s76,s78]) ).
cnf(s80,plain,
~ spl28_3,
inference(rat,[],[s18,s75,s79]) ).
cnf(s81,plain,
$false,
inference(rat,[],[s1,s80,s3,s71]) ).
fof(f1471,plain,
$false,
inference(avatar_sat_refutation,[],[s81]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT302+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.39 % Computer : n018.cluster.edu
% 0.11/0.39 % Model : x86_64 x86_64
% 0.11/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.39 % Memory : 8046.5625MB
% 0.11/0.39 % OS : Linux 6.8.0-71-generic
% 0.11/0.39 % CPULimit : 300
% 0.11/0.39 % WCLimit : 300
% 0.11/0.39 % DateTime : Sun Sep 27 14:25:39 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.43 Running first-order model finding
% 0.11/0.43 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.51 % (2408618)Will run a generic schedule for satisfiability detection.
% 0.18/0.51 % (2408627)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1967749912:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.18/0.51 % (2408624)% WARNING: option uhcvi not known.
% 0.18/0.51 % (2408624)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3634751536:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.18/0.51 % (2408623)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=68414294_2999 on theBenchmark for (2999ds/0Mi)
% 0.18/0.51 % (2408625)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2843867297:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.18/0.51 % (2408626)dis+10_1_sil=32000:sp=arity:random_seed=3102600466:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.18/0.51 % (2408628)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=4226291862:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.18/0.51 % (2408629)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1266043402:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.18/0.51 % TRYING [1]
% 0.18/0.51 % TRYING [2]
% 0.18/0.51 % TRYING [3]
% 0.18/0.51 % TRYING [4]
% 0.18/0.51 % (2408624) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2408618-2408624"...
% 0.18/0.51 % (2408626) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2408618-2408626"...
% 0.18/0.51 % (2408624)...printing done.
% 0.18/0.51 % (2408627)Instruction limit reached!
% 0.18/0.51 % (2408627)------------------------------
% 0.18/0.51 % (2408627)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.18/0.51 % (2408627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/0.51 % (2408627)CaDiCaL version: 2.1.3
% 0.18/0.51 % (2408627)Termination reason: Instruction limit
% 0.18/0.51 % (2408627)Termination phase: Saturation
% 0.18/0.51 % (2408627)Time elapsed: 0.044 s
% 0.18/0.51 % (2408627)Peak memory usage: 13 MB
% 0.18/0.51 % (2408627)Instructions burned: 119 (million)
% 0.18/0.51 % (2408626)...printing done.
% 0.18/0.51 % (2408624)Refutation found. Thanks to Tanya!
% 0.18/0.51 % SZS status Theorem for theBenchmark
% 0.18/0.51 % SZS output start Proof for theBenchmark
% See solution above
% 0.18/0.51 % (2408624)------------------------------
% 0.18/0.51 % (2408624)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.18/0.51 % (2408624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/0.51 % (2408624)CaDiCaL version: 2.1.3
% 0.18/0.51 % (2408624)Termination reason: Refutation
% 0.18/0.51 % (2408624)Time elapsed: 0.035 s
% 0.18/0.51 % (2408624)Peak memory usage: 13 MB
% 0.18/0.51 % (2408624)Instructions burned: 48 (million)
% 0.18/0.51 % (2408618)Success in time 0.077 s
% 0.18/0.51 % Vampire exiting
%------------------------------------------------------------------------------