%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT291+2 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n015.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:46:35 AM UTC 2026
% Result : Theorem 15.14s 3.25s
% Output : Refutation 15.80s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 17
% Syntax : Number of formulae : 128 ( 31 unt; 2 def)
% Number of atoms : 430 ( 86 equ)
% Maximal formula atoms : 9 ( 3 avg)
% Number of connectives : 493 ( 191 ~; 207 |; 77 &)
% ( 2 <=>; 16 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 18 ( 16 usr; 3 prp; 0-2 aty)
% Number of functors : 17 ( 17 usr; 3 con; 0-4 aty)
% Number of variables : 58 ( 0 sgn 56 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f64,axiom,
! [X0] : k4_xboole_0(X0,k1_xboole_0) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t3_boole) ).
fof(f3179,axiom,
np__0 = k1_xboole_0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t51_card_1) ).
fof(f4497,axiom,
! [X0] :
( l3_lattices(X0)
=> ( ( ~ v3_struct_0(X0)
& v17_lattices(X0) )
=> ( ~ v3_struct_0(X0)
& v11_lattices(X0)
& v13_lattices(X0)
& v14_lattices(X0)
& v15_lattices(X0)
& v16_lattices(X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc5_lattices) ).
fof(f4579,axiom,
! [X0] :
( l3_lattices(X0)
=> ( l1_lattices(X0)
& l2_lattices(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l3_lattices) ).
fof(f4595,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(f5607,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(f5640,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l3_lattices(X0) )
=> ( u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0))
& u2_lattices(X0) = u1_lattices(k1_lattice2(X0))
& u1_lattices(X0) = u2_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t18_lattice2) ).
fof(f5702,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(f5712,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(f6355,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& l3_lattices(X0) )
=> k7_lattices(X0,k5_lattices(X0)) = k6_lattices(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t37_lattice4) ).
fof(f6402,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& ~ v3_realset2(X0)
& l3_lattices(X0) )
=> k9_lopclset(X0) = k8_lopclset(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k9_lopclset) ).
fof(f6430,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& ~ v3_realset2(X0)
& l3_lattices(X0) )
=> k7_lopclset(X0) = a_1_1_lopclset(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d5_lopclset) ).
fof(f6448,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& ~ v3_realset2(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> k4_xboole_0(k7_lopclset(X0),k8_funct_2(u1_struct_0(X0),k1_zfmisc_1(k7_lopclset(X0)),k9_lopclset(X0),X1)) = k8_funct_2(u1_struct_0(X0),k1_zfmisc_1(k7_lopclset(X0)),k9_lopclset(X0),k7_lattices(X0,X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t28_lopclset) ).
fof(f6459,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& ~ v3_realset2(X0)
& l3_lattices(X0) )
=> k8_funct_2(u1_struct_0(X0),k1_zfmisc_1(k7_lopclset(X0)),k9_lopclset(X0),k5_lattices(X0)) = k1_xboole_0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t36_lopclset) ).
fof(f6460,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& ~ v3_realset2(X0)
& l3_lattices(X0) )
=> k8_funct_2(u1_struct_0(X0),k1_zfmisc_1(k7_lopclset(X0)),k9_lopclset(X0),k6_lattices(X0)) = k7_lopclset(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t37_lopclset) ).
fof(f6461,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& ~ v3_realset2(X0)
& l3_lattices(X0) )
=> k8_funct_2(u1_struct_0(X0),k1_zfmisc_1(k7_lopclset(X0)),k9_lopclset(X0),k6_lattices(X0)) = k7_lopclset(X0) ),
inference(negated_conjecture,[status(cth)],[f6460]) ).
fof(f6515,plain,
! [X0] :
( k9_lopclset(X0) = k8_lopclset(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f6402]) ).
fof(f6516,plain,
! [X0] :
( k9_lopclset(X0) = k8_lopclset(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f6515]) ).
fof(f6565,plain,
! [X0] :
( k7_lopclset(X0) = a_1_1_lopclset(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f6430]) ).
fof(f6566,plain,
! [X0] :
( k7_lopclset(X0) = a_1_1_lopclset(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f6565]) ).
fof(f6599,plain,
! [X0] :
( ! [X1] :
( k4_xboole_0(k7_lopclset(X0),k8_funct_2(u1_struct_0(X0),k1_zfmisc_1(k7_lopclset(X0)),k9_lopclset(X0),X1)) = k8_funct_2(u1_struct_0(X0),k1_zfmisc_1(k7_lopclset(X0)),k9_lopclset(X0),k7_lattices(X0,X1))
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f6448]) ).
fof(f6600,plain,
! [X0] :
( ! [X1] :
( k4_xboole_0(k7_lopclset(X0),k8_funct_2(u1_struct_0(X0),k1_zfmisc_1(k7_lopclset(X0)),k9_lopclset(X0),X1)) = k8_funct_2(u1_struct_0(X0),k1_zfmisc_1(k7_lopclset(X0)),k9_lopclset(X0),k7_lattices(X0,X1))
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f6599]) ).
fof(f6615,plain,
! [X0] :
( k8_funct_2(u1_struct_0(X0),k1_zfmisc_1(k7_lopclset(X0)),k9_lopclset(X0),k5_lattices(X0)) = k1_xboole_0
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f6459]) ).
fof(f6616,plain,
! [X0] :
( k8_funct_2(u1_struct_0(X0),k1_zfmisc_1(k7_lopclset(X0)),k9_lopclset(X0),k5_lattices(X0)) = k1_xboole_0
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f6615]) ).
fof(f6617,plain,
? [X0] :
( k7_lopclset(X0) != k8_funct_2(u1_struct_0(X0),k1_zfmisc_1(k7_lopclset(X0)),k9_lopclset(X0),k6_lattices(X0))
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& ~ v3_realset2(X0)
& l3_lattices(X0) ),
inference(ennf_transformation,[],[f6461]) ).
fof(f6618,plain,
? [X0] :
( k7_lopclset(X0) != k8_funct_2(u1_struct_0(X0),k1_zfmisc_1(k7_lopclset(X0)),k9_lopclset(X0),k6_lattices(X0))
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& v17_lattices(X0)
& ~ v3_realset2(X0)
& l3_lattices(X0) ),
inference(flattening,[],[f6617]) ).
fof(f6974,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v11_lattices(X0)
& v13_lattices(X0)
& v14_lattices(X0)
& v15_lattices(X0)
& v16_lattices(X0) )
| v3_struct_0(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f4497]) ).
fof(f6975,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v11_lattices(X0)
& v13_lattices(X0)
& v14_lattices(X0)
& v15_lattices(X0)
& v16_lattices(X0) )
| v3_struct_0(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f6974]) ).
fof(f7115,plain,
! [X0] :
( k7_lattices(X0,k5_lattices(X0)) = k6_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f6355]) ).
fof(f7116,plain,
! [X0] :
( k7_lattices(X0,k5_lattices(X0)) = k6_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f7115]) ).
fof(f7407,plain,
! [X0] :
( ( v3_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) )
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f5712]) ).
fof(f7410,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,[],[f5702]) ).
fof(f7411,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,[],[f7410]) ).
fof(f7428,plain,
! [X0] :
( ( u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0))
& u2_lattices(X0) = u1_lattices(k1_lattice2(X0))
& u1_lattices(X0) = u2_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f5640]) ).
fof(f7429,plain,
! [X0] :
( ( u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0))
& u2_lattices(X0) = u1_lattices(k1_lattice2(X0))
& u1_lattices(X0) = u2_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f7428]) ).
fof(f7432,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f5607]) ).
fof(f7433,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f7432]) ).
fof(f7473,plain,
! [X0] :
( m1_subset_1(k6_lattices(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l2_lattices(X0) ),
inference(ennf_transformation,[],[f4595]) ).
fof(f7474,plain,
! [X0] :
( m1_subset_1(k6_lattices(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l2_lattices(X0) ),
inference(flattening,[],[f7473]) ).
fof(f7495,plain,
! [X0] :
( ( l1_lattices(X0)
& l2_lattices(X0) )
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f4579]) ).
fof(f9089,plain,
( k7_lopclset(sK20) != k8_funct_2(u1_struct_0(sK20),k1_zfmisc_1(k7_lopclset(sK20)),k9_lopclset(sK20),k6_lattices(sK20))
& ~ v3_struct_0(sK20)
& v10_lattices(sK20)
& v17_lattices(sK20)
& ~ v3_realset2(sK20)
& l3_lattices(sK20) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK20]),skolemize(X0,sK20)],[f6618]) ).
fof(f9942,plain,
! [X0] :
( v3_realset2(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| k8_lopclset(X0) = k9_lopclset(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f6516]) ).
fof(f9996,plain,
! [X0] :
( v3_realset2(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| k7_lopclset(X0) = a_1_1_lopclset(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f6566]) ).
fof(f10033,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,u1_struct_0(X0))
| k4_xboole_0(k7_lopclset(X0),k8_funct_2(u1_struct_0(X0),k1_zfmisc_1(k7_lopclset(X0)),k9_lopclset(X0),X1)) = k8_funct_2(u1_struct_0(X0),k1_zfmisc_1(k7_lopclset(X0)),k9_lopclset(X0),k7_lattices(X0,X1))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f6600]) ).
fof(f10048,plain,
! [X0] :
( k1_xboole_0 = k8_funct_2(u1_struct_0(X0),k1_zfmisc_1(k7_lopclset(X0)),k9_lopclset(X0),k5_lattices(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| v3_realset2(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f6616]) ).
fof(f10049,plain,
l3_lattices(sK20),
inference(cnf_transformation,[],[f9089]) ).
fof(f10050,plain,
~ v3_realset2(sK20),
inference(cnf_transformation,[],[f9089]) ).
fof(f10051,plain,
v17_lattices(sK20),
inference(cnf_transformation,[],[f9089]) ).
fof(f10052,plain,
v10_lattices(sK20),
inference(cnf_transformation,[],[f9089]) ).
fof(f10053,plain,
~ v3_struct_0(sK20),
inference(cnf_transformation,[],[f9089]) ).
fof(f10054,plain,
k7_lopclset(sK20) != k8_funct_2(u1_struct_0(sK20),k1_zfmisc_1(k7_lopclset(sK20)),k9_lopclset(sK20),k6_lattices(sK20)),
inference(cnf_transformation,[],[f9089]) ).
fof(f10683,plain,
! [X0] :
( ~ v17_lattices(X0)
| v3_struct_0(X0)
| v13_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f6975]) ).
fof(f10925,plain,
! [X0] : k4_xboole_0(X0,k1_xboole_0) = X0,
inference(cnf_transformation,[],[f64]) ).
fof(f10932,plain,
! [X0] :
( ~ v17_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| k6_lattices(X0) = k7_lattices(X0,k5_lattices(X0))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f7116]) ).
fof(f11423,plain,
! [X0] :
( ~ l3_lattices(X0)
| l3_lattices(k1_lattice2(X0)) ),
inference(cnf_transformation,[],[f7407]) ).
fof(f11426,plain,
! [X0] :
( ~ v13_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| k5_lattices(X0) = k6_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f7411]) ).
fof(f11448,plain,
! [X0] :
( ~ l3_lattices(X0)
| v3_struct_0(X0)
| u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0)) ),
inference(cnf_transformation,[],[f7429]) ).
fof(f11459,plain,
! [X0] :
( ~ v3_struct_0(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f7433]) ).
fof(f11535,plain,
! [X0] :
( ~ l2_lattices(X0)
| v3_struct_0(X0)
| m1_subset_1(k6_lattices(X0),u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f7474]) ).
fof(f11558,plain,
! [X0] :
( ~ l3_lattices(X0)
| l2_lattices(X0) ),
inference(cnf_transformation,[],[f7495]) ).
fof(f12713,plain,
k1_xboole_0 = np__0,
inference(cnf_transformation,[],[f3179]) ).
fof(f13549,plain,
! [X0] :
( v3_realset2(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v17_lattices(X0)
| np__0 = k8_funct_2(u1_struct_0(X0),k1_zfmisc_1(k7_lopclset(X0)),k9_lopclset(X0),k5_lattices(X0))
| ~ l3_lattices(X0) ),
inference(definition_unfolding,[],[f10048,f12713]) ).
fof(f13728,plain,
! [X0] : k4_xboole_0(X0,np__0) = X0,
inference(definition_unfolding,[],[f10925,f12713]) ).
fof(f15290,plain,
( v3_struct_0(sK20)
| ~ v10_lattices(sK20)
| ~ v17_lattices(sK20)
| k9_lopclset(sK20) = k8_lopclset(sK20)
| ~ l3_lattices(sK20) ),
inference(resolution,[],[f9942,f10050]) ).
fof(f15291,plain,
( ~ v10_lattices(sK20)
| ~ v17_lattices(sK20)
| k9_lopclset(sK20) = k8_lopclset(sK20)
| ~ l3_lattices(sK20) ),
inference(forward_subsumption_resolution,[],[f15290,f10053]) ).
fof(f15292,plain,
( ~ v17_lattices(sK20)
| k9_lopclset(sK20) = k8_lopclset(sK20)
| ~ l3_lattices(sK20) ),
inference(forward_subsumption_resolution,[],[f15291,f10052]) ).
fof(f15293,plain,
( k9_lopclset(sK20) = k8_lopclset(sK20)
| ~ l3_lattices(sK20) ),
inference(forward_subsumption_resolution,[],[f15292,f10051]) ).
fof(f15294,plain,
k9_lopclset(sK20) = k8_lopclset(sK20),
inference(forward_subsumption_resolution,[],[f15293,f10049]) ).
fof(f15295,plain,
k7_lopclset(sK20) != k8_funct_2(u1_struct_0(sK20),k1_zfmisc_1(k7_lopclset(sK20)),k8_lopclset(sK20),k6_lattices(sK20)),
inference(superposition,[],[f10054,f15294]) ).
fof(f15296,plain,
( v3_struct_0(sK20)
| ~ v10_lattices(sK20)
| ~ v17_lattices(sK20)
| k7_lopclset(sK20) = a_1_1_lopclset(sK20)
| ~ l3_lattices(sK20) ),
inference(resolution,[],[f9996,f10050]) ).
fof(f15297,plain,
( ~ v10_lattices(sK20)
| ~ v17_lattices(sK20)
| k7_lopclset(sK20) = a_1_1_lopclset(sK20)
| ~ l3_lattices(sK20) ),
inference(forward_subsumption_resolution,[],[f15296,f10053]) ).
fof(f15298,plain,
( ~ v17_lattices(sK20)
| k7_lopclset(sK20) = a_1_1_lopclset(sK20)
| ~ l3_lattices(sK20) ),
inference(forward_subsumption_resolution,[],[f15297,f10052]) ).
fof(f15299,plain,
( k7_lopclset(sK20) = a_1_1_lopclset(sK20)
| ~ l3_lattices(sK20) ),
inference(forward_subsumption_resolution,[],[f15298,f10051]) ).
fof(f15300,plain,
k7_lopclset(sK20) = a_1_1_lopclset(sK20),
inference(forward_subsumption_resolution,[],[f15299,f10049]) ).
fof(f15301,plain,
a_1_1_lopclset(sK20) != k8_funct_2(u1_struct_0(sK20),k1_zfmisc_1(a_1_1_lopclset(sK20)),k8_lopclset(sK20),k6_lattices(sK20)),
inference(superposition,[],[f15295,f15300]) ).
fof(f15304,plain,
( v3_struct_0(sK20)
| ~ v10_lattices(sK20)
| ~ v17_lattices(sK20)
| np__0 = k8_funct_2(u1_struct_0(sK20),k1_zfmisc_1(k7_lopclset(sK20)),k9_lopclset(sK20),k5_lattices(sK20))
| ~ l3_lattices(sK20) ),
inference(resolution,[],[f13549,f10050]) ).
fof(f15305,plain,
( ~ v10_lattices(sK20)
| ~ v17_lattices(sK20)
| np__0 = k8_funct_2(u1_struct_0(sK20),k1_zfmisc_1(k7_lopclset(sK20)),k9_lopclset(sK20),k5_lattices(sK20))
| ~ l3_lattices(sK20) ),
inference(forward_subsumption_resolution,[],[f15304,f10053]) ).
fof(f15306,plain,
( ~ v17_lattices(sK20)
| np__0 = k8_funct_2(u1_struct_0(sK20),k1_zfmisc_1(k7_lopclset(sK20)),k9_lopclset(sK20),k5_lattices(sK20))
| ~ l3_lattices(sK20) ),
inference(forward_subsumption_resolution,[],[f15305,f10052]) ).
fof(f15307,plain,
( np__0 = k8_funct_2(u1_struct_0(sK20),k1_zfmisc_1(k7_lopclset(sK20)),k9_lopclset(sK20),k5_lattices(sK20))
| ~ l3_lattices(sK20) ),
inference(forward_subsumption_resolution,[],[f15306,f10051]) ).
fof(f15308,plain,
np__0 = k8_funct_2(u1_struct_0(sK20),k1_zfmisc_1(k7_lopclset(sK20)),k9_lopclset(sK20),k5_lattices(sK20)),
inference(forward_subsumption_resolution,[],[f15307,f10049]) ).
fof(f15309,plain,
np__0 = k8_funct_2(u1_struct_0(sK20),k1_zfmisc_1(k7_lopclset(sK20)),k8_lopclset(sK20),k5_lattices(sK20)),
inference(forward_demodulation,[],[f15308,f15294]) ).
fof(f15310,plain,
np__0 = k8_funct_2(u1_struct_0(sK20),k1_zfmisc_1(a_1_1_lopclset(sK20)),k8_lopclset(sK20),k5_lattices(sK20)),
inference(forward_demodulation,[],[f15309,f15300]) ).
fof(f15364,plain,
( v3_struct_0(sK20)
| u1_struct_0(sK20) = u1_struct_0(k1_lattice2(sK20)) ),
inference(resolution,[],[f11448,f10049]) ).
fof(f15365,plain,
u1_struct_0(sK20) = u1_struct_0(k1_lattice2(sK20)),
inference(forward_subsumption_resolution,[],[f15364,f10053]) ).
fof(f15380,definition,
( spl509_22
<=> v3_struct_0(k1_lattice2(sK20)) ),
introduced(definition,[new_symbols(definition,[spl509_22])],[avatar_definition]) ).
fof(f15381,plain,
( v3_struct_0(k1_lattice2(sK20))
| ~ spl509_22 ),
inference(avatar_component_clause,[],[f15380]) ).
fof(f15433,plain,
( v3_struct_0(sK20)
| ~ v10_lattices(sK20)
| k6_lattices(sK20) = k7_lattices(sK20,k5_lattices(sK20))
| ~ l3_lattices(sK20) ),
inference(resolution,[],[f10932,f10051]) ).
fof(f15434,plain,
( ~ v10_lattices(sK20)
| k6_lattices(sK20) = k7_lattices(sK20,k5_lattices(sK20))
| ~ l3_lattices(sK20) ),
inference(forward_subsumption_resolution,[],[f15433,f10053]) ).
fof(f15435,plain,
( k6_lattices(sK20) = k7_lattices(sK20,k5_lattices(sK20))
| ~ l3_lattices(sK20) ),
inference(forward_subsumption_resolution,[],[f15434,f10052]) ).
fof(f15436,plain,
k6_lattices(sK20) = k7_lattices(sK20,k5_lattices(sK20)),
inference(forward_subsumption_resolution,[],[f15435,f10049]) ).
fof(f15456,plain,
l3_lattices(k1_lattice2(sK20)),
inference(resolution,[],[f11423,f10049]) ).
fof(f15461,plain,
l2_lattices(k1_lattice2(sK20)),
inference(resolution,[],[f15456,f11558]) ).
fof(f15469,plain,
( v3_struct_0(sK20)
| ~ l3_lattices(sK20)
| ~ spl509_22 ),
inference(resolution,[],[f15381,f11459]) ).
fof(f15471,plain,
( ~ l3_lattices(sK20)
| ~ spl509_22 ),
inference(forward_subsumption_resolution,[],[f15469,f10053]) ).
fof(f15472,plain,
( $false
| ~ spl509_22 ),
inference(forward_subsumption_resolution,[],[f15471,f10049]) ).
fof(f15473,plain,
~ spl509_22,
inference(avatar_contradiction_clause,[],[f15472]) ).
fof(f15542,plain,
( v3_struct_0(sK20)
| v13_lattices(sK20)
| ~ l3_lattices(sK20) ),
inference(resolution,[],[f10683,f10051]) ).
fof(f15543,plain,
( v13_lattices(sK20)
| ~ l3_lattices(sK20) ),
inference(forward_subsumption_resolution,[],[f15542,f10053]) ).
fof(f15544,plain,
v13_lattices(sK20),
inference(forward_subsumption_resolution,[],[f15543,f10049]) ).
fof(f15545,plain,
( v3_struct_0(sK20)
| ~ v10_lattices(sK20)
| k5_lattices(sK20) = k6_lattices(k1_lattice2(sK20))
| ~ l3_lattices(sK20) ),
inference(resolution,[],[f15544,f11426]) ).
fof(f15546,plain,
( ~ v10_lattices(sK20)
| k5_lattices(sK20) = k6_lattices(k1_lattice2(sK20))
| ~ l3_lattices(sK20) ),
inference(forward_subsumption_resolution,[],[f15545,f10053]) ).
fof(f15547,plain,
( k5_lattices(sK20) = k6_lattices(k1_lattice2(sK20))
| ~ l3_lattices(sK20) ),
inference(forward_subsumption_resolution,[],[f15546,f10052]) ).
fof(f15548,plain,
k5_lattices(sK20) = k6_lattices(k1_lattice2(sK20)),
inference(forward_subsumption_resolution,[],[f15547,f10049]) ).
fof(f15725,plain,
( v3_struct_0(k1_lattice2(sK20))
| m1_subset_1(k6_lattices(k1_lattice2(sK20)),u1_struct_0(k1_lattice2(sK20))) ),
inference(resolution,[],[f15461,f11535]) ).
fof(f15726,plain,
( m1_subset_1(k6_lattices(k1_lattice2(sK20)),u1_struct_0(sK20))
| v3_struct_0(k1_lattice2(sK20)) ),
inference(forward_demodulation,[],[f15725,f15365]) ).
fof(f15727,plain,
( m1_subset_1(k5_lattices(sK20),u1_struct_0(sK20))
| v3_struct_0(k1_lattice2(sK20)) ),
inference(forward_demodulation,[],[f15726,f15548]) ).
fof(f15729,definition,
( spl509_48
<=> m1_subset_1(k5_lattices(sK20),u1_struct_0(sK20)) ),
introduced(definition,[new_symbols(definition,[spl509_48])],[avatar_definition]) ).
fof(f15730,plain,
( m1_subset_1(k5_lattices(sK20),u1_struct_0(sK20))
| ~ spl509_48 ),
inference(avatar_component_clause,[],[f15729]) ).
fof(f15731,plain,
( spl509_22
| spl509_48 ),
inference(avatar_split_clause,[],[f15727,f15729,f15380]) ).
fof(f15733,plain,
( k4_xboole_0(k7_lopclset(sK20),k8_funct_2(u1_struct_0(sK20),k1_zfmisc_1(k7_lopclset(sK20)),k9_lopclset(sK20),k5_lattices(sK20))) = k8_funct_2(u1_struct_0(sK20),k1_zfmisc_1(k7_lopclset(sK20)),k9_lopclset(sK20),k7_lattices(sK20,k5_lattices(sK20)))
| v3_struct_0(sK20)
| ~ v10_lattices(sK20)
| ~ v17_lattices(sK20)
| v3_realset2(sK20)
| ~ l3_lattices(sK20)
| ~ spl509_48 ),
inference(resolution,[],[f15730,f10033]) ).
fof(f15739,plain,
( k4_xboole_0(k7_lopclset(sK20),k8_funct_2(u1_struct_0(sK20),k1_zfmisc_1(k7_lopclset(sK20)),k9_lopclset(sK20),k5_lattices(sK20))) = k8_funct_2(u1_struct_0(sK20),k1_zfmisc_1(k7_lopclset(sK20)),k9_lopclset(sK20),k7_lattices(sK20,k5_lattices(sK20)))
| ~ v10_lattices(sK20)
| ~ v17_lattices(sK20)
| v3_realset2(sK20)
| ~ l3_lattices(sK20)
| ~ spl509_48 ),
inference(forward_subsumption_resolution,[],[f15733,f10053]) ).
fof(f15741,plain,
( k4_xboole_0(k7_lopclset(sK20),k8_funct_2(u1_struct_0(sK20),k1_zfmisc_1(k7_lopclset(sK20)),k9_lopclset(sK20),k5_lattices(sK20))) = k8_funct_2(u1_struct_0(sK20),k1_zfmisc_1(k7_lopclset(sK20)),k9_lopclset(sK20),k7_lattices(sK20,k5_lattices(sK20)))
| ~ v17_lattices(sK20)
| v3_realset2(sK20)
| ~ l3_lattices(sK20)
| ~ spl509_48 ),
inference(forward_subsumption_resolution,[],[f15739,f10052]) ).
fof(f15742,plain,
( k4_xboole_0(k7_lopclset(sK20),k8_funct_2(u1_struct_0(sK20),k1_zfmisc_1(k7_lopclset(sK20)),k9_lopclset(sK20),k5_lattices(sK20))) = k8_funct_2(u1_struct_0(sK20),k1_zfmisc_1(k7_lopclset(sK20)),k9_lopclset(sK20),k7_lattices(sK20,k5_lattices(sK20)))
| v3_realset2(sK20)
| ~ l3_lattices(sK20)
| ~ spl509_48 ),
inference(forward_subsumption_resolution,[],[f15741,f10051]) ).
fof(f15743,plain,
( k4_xboole_0(k7_lopclset(sK20),k8_funct_2(u1_struct_0(sK20),k1_zfmisc_1(k7_lopclset(sK20)),k9_lopclset(sK20),k5_lattices(sK20))) = k8_funct_2(u1_struct_0(sK20),k1_zfmisc_1(k7_lopclset(sK20)),k9_lopclset(sK20),k7_lattices(sK20,k5_lattices(sK20)))
| ~ l3_lattices(sK20)
| ~ spl509_48 ),
inference(forward_subsumption_resolution,[],[f15742,f10050]) ).
fof(f15744,plain,
( k4_xboole_0(k7_lopclset(sK20),k8_funct_2(u1_struct_0(sK20),k1_zfmisc_1(k7_lopclset(sK20)),k9_lopclset(sK20),k5_lattices(sK20))) = k8_funct_2(u1_struct_0(sK20),k1_zfmisc_1(k7_lopclset(sK20)),k9_lopclset(sK20),k7_lattices(sK20,k5_lattices(sK20)))
| ~ spl509_48 ),
inference(forward_subsumption_resolution,[],[f15743,f10049]) ).
fof(f15745,plain,
( k8_funct_2(u1_struct_0(sK20),k1_zfmisc_1(k7_lopclset(sK20)),k9_lopclset(sK20),k6_lattices(sK20)) = k4_xboole_0(k7_lopclset(sK20),k8_funct_2(u1_struct_0(sK20),k1_zfmisc_1(k7_lopclset(sK20)),k9_lopclset(sK20),k5_lattices(sK20)))
| ~ spl509_48 ),
inference(forward_demodulation,[],[f15744,f15436]) ).
fof(f15746,plain,
( k8_funct_2(u1_struct_0(sK20),k1_zfmisc_1(k7_lopclset(sK20)),k8_lopclset(sK20),k6_lattices(sK20)) = k4_xboole_0(k7_lopclset(sK20),k8_funct_2(u1_struct_0(sK20),k1_zfmisc_1(k7_lopclset(sK20)),k8_lopclset(sK20),k5_lattices(sK20)))
| ~ spl509_48 ),
inference(forward_demodulation,[],[f15745,f15294]) ).
fof(f15747,plain,
( k8_funct_2(u1_struct_0(sK20),k1_zfmisc_1(a_1_1_lopclset(sK20)),k8_lopclset(sK20),k6_lattices(sK20)) = k4_xboole_0(a_1_1_lopclset(sK20),k8_funct_2(u1_struct_0(sK20),k1_zfmisc_1(a_1_1_lopclset(sK20)),k8_lopclset(sK20),k5_lattices(sK20)))
| ~ spl509_48 ),
inference(forward_demodulation,[],[f15746,f15300]) ).
fof(f15748,plain,
( k8_funct_2(u1_struct_0(sK20),k1_zfmisc_1(a_1_1_lopclset(sK20)),k8_lopclset(sK20),k6_lattices(sK20)) = k4_xboole_0(a_1_1_lopclset(sK20),np__0)
| ~ spl509_48 ),
inference(forward_demodulation,[],[f15747,f15310]) ).
fof(f15749,plain,
( a_1_1_lopclset(sK20) = k8_funct_2(u1_struct_0(sK20),k1_zfmisc_1(a_1_1_lopclset(sK20)),k8_lopclset(sK20),k6_lattices(sK20))
| ~ spl509_48 ),
inference(forward_demodulation,[],[f15748,f13728]) ).
fof(f15750,plain,
( $false
| ~ spl509_48 ),
inference(forward_subsumption_resolution,[],[f15749,f15301]) ).
fof(f15751,plain,
~ spl509_48,
inference(avatar_contradiction_clause,[],[f15750]) ).
cnf(s15,plain,
~ spl509_22,
inference(sat_conversion,[],[f15473]) ).
cnf(s34,plain,
( spl509_22
| spl509_48 ),
inference(sat_conversion,[],[f15731]) ).
cnf(s36,plain,
~ spl509_48,
inference(sat_conversion,[],[f15751]) ).
cnf(s37,plain,
spl509_22,
inference(rat,[],[s34,s36]) ).
cnf(s40,plain,
$false,
inference(rat,[],[s15,s37]) ).
fof(f15752,plain,
$false,
inference(avatar_sat_refutation,[],[s40]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT291+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.38 % Computer : n015.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Sun Sep 27 14:20:02 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.42 Running first-order theorem proving
% 0.11/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
% 14.16/3.11 % (1711926)Detected formulas, will run a generic FOF schedule.
% 14.16/3.11 % (1711931)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=1611646018:i=141193_2997 on theBenchmark for (2997ds/141193Mi)
% 14.16/3.11 % (1711936)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3634435555:s2a=on:i=139:gtg=position_2997 on theBenchmark for (2997ds/139Mi)
% 14.16/3.11 % (1711935)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2967761387:i=119:av=off:ss=axioms_2997 on theBenchmark for (2997ds/119Mi)
% 14.16/3.11 % (1711933)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=610498237:i=141695:sd=1:nm=32:gsp=on:ss=included_2997 on theBenchmark for (2997ds/141695Mi)
% 14.16/3.11 % (1711937)dis-21_1_sil=8000:lcm=predicate:random_seed=3758202099:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2997 on theBenchmark for (2997ds/129Mi)
% 14.16/3.11 % (1711932)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=261873982:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2997 on theBenchmark for (2997ds/134677Mi)
% 14.16/3.11 % (1711934)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=546188244:i=109:sd=1:ins=1:gsp=on:ss=axioms_2997 on theBenchmark for (2997ds/109Mi)
% 14.16/3.11 % (1711934)Refutation not found, incomplete strategy
% 14.16/3.11 % (1711934)------------------------------
% 14.16/3.11 % (1711934)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.16/3.11 % (1711934)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.16/3.11 % (1711934)CaDiCaL version: 2.1.3
% 14.16/3.11 % (1711934)Termination reason: Refutation not found, incomplete strategy
% 14.16/3.11 % (1711934)Time elapsed: 0.029 s
% 14.16/3.11 % (1711934)Peak memory usage: 96 MB
% 14.16/3.11 % (1711934)Instructions burned: 37 (million)
% 14.16/3.11 % (1711935)Instruction limit reached!
% 14.16/3.11 % (1711935)------------------------------
% 14.16/3.11 % (1711935)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.16/3.11 % (1711935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.16/3.11 % (1711935)CaDiCaL version: 2.1.3
% 14.16/3.11 % (1711935)Termination reason: Instruction limit
% 14.16/3.11 % (1711935)Termination phase: Saturation
% 14.16/3.11 % (1711935)Time elapsed: 0.082 s
% 14.16/3.11 % (1711935)Peak memory usage: 97 MB
% 14.16/3.11 % (1711935)Instructions burned: 119 (million)
% 14.16/3.11 % (1711936)Instruction limit reached!
% 14.16/3.11 % (1711936)------------------------------
% 14.16/3.11 % (1711936)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.16/3.11 % (1711936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.16/3.11 % (1711936)CaDiCaL version: 2.1.3
% 14.16/3.11 % (1711936)Termination reason: Instruction limit
% 14.16/3.11 % (1711936)Termination phase: Preprocessing 1
% 14.16/3.11 % (1711936)Time elapsed: 0.084 s
% 14.16/3.11 % (1711936)Peak memory usage: 93 MB
% 14.16/3.11 % (1711936)Instructions burned: 139 (million)
% 14.16/3.11 % (1711937)Instruction limit reached!
% 14.16/3.11 % (1711937)------------------------------
% 14.16/3.11 % (1711937)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.16/3.11 % (1711937)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.16/3.11 % (1711937)CaDiCaL version: 2.1.3
% 14.16/3.11 % (1711937)Termination reason: Instruction limit
% 14.16/3.11 % (1711937)Termination phase: Preprocessing 3
% 14.16/3.11 % (1711937)Time elapsed: 0.099 s
% 14.16/3.11 % (1711937)Peak memory usage: 97 MB
% 14.16/3.11 % (1711937)Instructions burned: 130 (million)
% 14.16/3.11 % (1711945)lrs+10_1_sil=8000:sp=occurrence:random_seed=3600619135:i=285:sd=3:ss=axioms:sgt=8_2994 on theBenchmark for (2994ds/285Mi)
% 14.16/3.11 % (1711946)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3776526901:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2994 on theBenchmark for (2994ds/157Mi)
% 14.16/3.11 % (1711947)lrs+1011_1_sil=32000:sp=occurrence:random_seed=127861961:i=325:sd=1:ss=axioms:sgt=32_2994 on theBenchmark for (2994ds/325Mi)
% 14.16/3.11 % (1711934)------------------------------
% 14.16/3.11 % (1711934)------------------------------
% 14.16/3.11 % (1711946)Instruction limit reached!
% 14.16/3.11 % (1711946)------------------------------
% 14.16/3.11 % (1711946)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.14/3.25 % (1711946)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.14/3.25 % (1711946)CaDiCaL version: 2.1.3
% 15.14/3.25 % (1711946)Termination reason: Instruction limit
% 15.14/3.25 % (1711946)Termination phase: Saturation
% 15.14/3.25 % (1711946)Time elapsed: 0.088 s
% 15.14/3.25 % (1711946)Peak memory usage: 97 MB
% 15.14/3.25 % (1711946)Instructions burned: 159 (million)
% 15.14/3.25 % (1711951)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=3609918129:s2a=on:i=248:s2at=1.23:gtg=position_2992 on theBenchmark for (2992ds/248Mi)
% 15.14/3.25 % (1711945)Instruction limit reached!
% 15.14/3.25 % (1711945)------------------------------
% 15.14/3.25 % (1711945)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.14/3.25 % (1711945)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.14/3.25 % (1711945)CaDiCaL version: 2.1.3
% 15.14/3.25 % (1711945)Termination reason: Instruction limit
% 15.14/3.25 % (1711945)Termination phase: Saturation
% 15.14/3.25 % (1711945)Time elapsed: 0.201 s
% 15.14/3.25 % (1711945)Peak memory usage: 100 MB
% 15.14/3.25 % (1711945)Instructions burned: 285 (million)
% 15.14/3.25 % (1711952)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3552667133:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2992 on theBenchmark for (2992ds/294Mi)
% 15.14/3.25 % (1711947)Instruction limit reached!
% 15.14/3.25 % (1711947)------------------------------
% 15.14/3.25 % (1711947)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.14/3.25 % (1711947)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.14/3.25 % (1711947)CaDiCaL version: 2.1.3
% 15.14/3.25 % (1711947)Termination reason: Instruction limit
% 15.14/3.25 % (1711947)Termination phase: Saturation
% 15.14/3.25 % (1711947)Time elapsed: 0.222 s
% 15.14/3.25 % (1711947)Peak memory usage: 99 MB
% 15.14/3.25 % (1711947)Instructions burned: 325 (million)
% 15.14/3.25 % (1711956)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3308407243:i=2350_2991 on theBenchmark for (2991ds/2350Mi)
% 15.14/3.25 % (1711951)Instruction limit reached!
% 15.14/3.25 % (1711951)------------------------------
% 15.14/3.25 % (1711951)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.14/3.25 % (1711951)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.14/3.25 % (1711951)CaDiCaL version: 2.1.3
% 15.14/3.25 % (1711951)Termination reason: Instruction limit
% 15.14/3.25 % (1711951)Termination phase: Preprocessing 3
% 15.14/3.25 % (1711951)Time elapsed: 0.157 s
% 15.14/3.25 % (1711951)Peak memory usage: 101 MB
% 15.14/3.25 % (1711951)Instructions burned: 249 (million)
% 15.14/3.25 % (1711958)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2547117243:cts=off:i=113:fsr=off:ss=included:sgt=4_2991 on theBenchmark for (2991ds/113Mi)
% 15.14/3.25 % (1711952)Instruction limit reached!
% 15.14/3.25 % (1711952)------------------------------
% 15.14/3.25 % (1711952)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.14/3.25 % (1711952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.14/3.25 % (1711952)CaDiCaL version: 2.1.3
% 15.14/3.25 % (1711952)Termination reason: Instruction limit
% 15.14/3.25 % (1711952)Termination phase: Saturation
% 15.14/3.25 % (1711952)Time elapsed: 0.176 s
% 15.14/3.25 % (1711952)Peak memory usage: 101 MB
% 15.14/3.25 % (1711952)Instructions burned: 295 (million)
% 15.14/3.25 % (1711958)Instruction limit reached!
% 15.14/3.25 % (1711958)------------------------------
% 15.14/3.25 % (1711958)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.14/3.25 % (1711958)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.14/3.25 % (1711958)CaDiCaL version: 2.1.3
% 15.14/3.25 % (1711958)Termination reason: Instruction limit
% 15.14/3.25 % (1711958)Termination phase: Property scanning
% 15.14/3.25 % (1711958)Time elapsed: 0.086 s
% 15.14/3.25 % (1711958)Peak memory usage: 96 MB
% 15.14/3.25 % (1711958)Instructions burned: 114 (million)
% 15.14/3.25 % (1711960)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3021790262:i=127:av=off:fsr=off:sup=off_2989 on theBenchmark for (2989ds/127Mi)
% 15.14/3.25 % (1711962)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2573053525:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2989 on theBenchmark for (2989ds/114Mi)
% 15.14/3.25 % (1711962)Instruction limit reached!
% 15.14/3.25 % (1711962)------------------------------
% 15.14/3.25 % (1711962)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.14/3.25 % (1711962)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.14/3.25 % (1711962)CaDiCaL version: 2.1.3
% 15.14/3.25 % (1711962)Termination reason: Instruction limit
% 15.14/3.25 % (1711962)Termination phase: Property scanning
% 15.14/3.25 % (1711962)Time elapsed: 0.049 s
% 15.14/3.25 % (1711962)Peak memory usage: 92 MB
% 15.14/3.25 % (1711962)Instructions burned: 116 (million)
% 15.14/3.25 % (1711960)Instruction limit reached!
% 15.14/3.25 % (1711960)------------------------------
% 15.14/3.25 % (1711960)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.14/3.25 % (1711960)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.14/3.25 % (1711960)CaDiCaL version: 2.1.3
% 15.14/3.25 % (1711960)Termination reason: Instruction limit
% 15.14/3.25 % (1711960)Termination phase: Preprocessing 3
% 15.14/3.25 % (1711960)Time elapsed: 0.092 s
% 15.14/3.25 % (1711960)Peak memory usage: 100 MB
% 15.14/3.25 % (1711960)Instructions burned: 127 (million)
% 15.14/3.25 % (1711963)lrs+10_1_sil=8000:sp=occurrence:random_seed=2442551964:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2988 on theBenchmark for (2988ds/907Mi)
% 15.14/3.25 % (1711966)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2779257851:i=437:sd=1:aac=none:ss=included_2987 on theBenchmark for (2987ds/437Mi)
% 15.14/3.25 % (1711967)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1654705651:i=5202:ss=axioms:sgt=16_2987 on theBenchmark for (2987ds/5202Mi)
% 15.14/3.25 % (1711966)Refutation not found, incomplete strategy
% 15.14/3.25 % (1711966)------------------------------
% 15.14/3.25 % (1711966)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.14/3.25 % (1711966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.14/3.25 % (1711966)CaDiCaL version: 2.1.3
% 15.14/3.25 % (1711966)Termination reason: Refutation not found, incomplete strategy
% 15.14/3.25 % (1711966)Time elapsed: 0.069 s
% 15.14/3.25 % (1711966)Peak memory usage: 98 MB
% 15.14/3.25 % (1711966)Instructions burned: 105 (million)
% 15.14/3.25 % (1711966)------------------------------
% 15.14/3.25 % (1711966)------------------------------
% 15.14/3.25 % (1711963)Instruction limit reached!
% 15.14/3.25 % (1711963)------------------------------
% 15.14/3.25 % (1711963)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.14/3.25 % (1711963)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.14/3.25 % (1711963)CaDiCaL version: 2.1.3
% 15.14/3.25 % (1711963)Termination reason: Instruction limit
% 15.14/3.25 % (1711963)Termination phase: Saturation
% 15.14/3.25 % (1711963)Time elapsed: 0.533 s
% 15.14/3.25 % (1711963)Peak memory usage: 113 MB
% 15.14/3.25 % (1711963)Instructions burned: 908 (million)
% 15.14/3.25 % (1711971)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2065668673:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2983 on theBenchmark for (2983ds/134Mi)
% 15.14/3.25 % (1711971)Instruction limit reached!
% 15.14/3.25 % (1711971)------------------------------
% 15.14/3.25 % (1711971)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.14/3.25 % (1711971)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.14/3.25 % (1711971)CaDiCaL version: 2.1.3
% 15.14/3.25 % (1711971)Termination reason: Instruction limit
% 15.14/3.25 % (1711971)Termination phase: Saturation
% 15.14/3.25 % (1711971)Time elapsed: 0.083 s
% 15.14/3.25 % (1711971)Peak memory usage: 98 MB
% 15.14/3.25 % (1711971)Instructions burned: 136 (million)
% 15.14/3.25 % (1711972)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1889578762:st=8:i=592:sd=3:ep=RST:ss=axioms_2982 on theBenchmark for (2982ds/592Mi)
% 15.14/3.25 % (1711974)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=357956361:st=3:i=13193:sd=3:ss=axioms_2981 on theBenchmark for (2981ds/13193Mi)
% 15.14/3.25 % (1711932)First to succeed.
% 15.14/3.25 % (1711932)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1711926"
% 15.14/3.25 % (1711933)Also succeeded, but the first one will report.
% 15.14/3.25 % (1711972)Instruction limit reached!
% 15.14/3.25 % (1711972)------------------------------
% 15.14/3.25 % (1711972)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.14/3.25 % (1711972)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.14/3.25 % (1711972)CaDiCaL version: 2.1.3
% 15.14/3.25 % (1711972)Termination reason: Instruction limit
% 15.14/3.25 % (1711972)Termination phase: Property scanning
% 15.14/3.25 % (1711972)Time elapsed: 0.326 s
% 15.14/3.25 % (1711972)Peak memory usage: 105 MB
% 15.14/3.25 % (1711972)Instructions burned: 593 (million)
% 15.14/3.25 % (1711977)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=3832058719:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2977 on theBenchmark for (2977ds/125Mi)
% 15.14/3.25 % (1711932)Refutation found. Thanks to Tanya!
% 15.14/3.25 % SZS status Theorem for theBenchmark
% 15.14/3.25 % SZS output start Proof for theBenchmark
% See solution above
% 15.80/3.44 % (1711932)------------------------------
% 15.80/3.44 % (1711932)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.80/3.44 % (1711932)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.80/3.44 % (1711932)CaDiCaL version: 2.1.3
% 15.80/3.44 % (1711932)Termination reason: Refutation
% 15.80/3.44 % (1711932)Time elapsed: 1.661 s
% 15.80/3.44 % (1711932)Peak memory usage: 178 MB
% 15.80/3.44 % (1711932)Instructions burned: 2744 (million)
% 15.80/3.44 % (1711932)------------------------------
% 15.80/3.44 % (1711932)------------------------------
% 15.80/3.44 % (1711926)Success in time 2.391 s
% 15.80/3.44 % Vampire exiting
%------------------------------------------------------------------------------