%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT332+3 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n002.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:47:02 AM UTC 2026
% Result : Theorem 26.11s 6.66s
% Output : Refutation 0.30s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 27
% Syntax : Number of formulae : 233 ( 31 unt; 9 def)
% Number of atoms : 945 ( 178 equ)
% Maximal formula atoms : 26 ( 4 avg)
% Number of connectives : 1135 ( 423 ~; 522 |; 151 &)
% ( 15 <=>; 24 =>; 0 <=; 0 <~>)
% Maximal formula depth : 21 ( 5 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 30 ( 28 usr; 10 prp; 0-3 aty)
% Number of functors : 15 ( 15 usr; 1 con; 0-3 aty)
% Number of variables : 143 ( 0 sgn 131 !; 12 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f8589,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> k1_filter_0(X0) = u1_struct_0(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d2_filter_0) ).
fof(f9358,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l3_lattices(X0) )
=> ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_lattice2) ).
fof(f9363,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/sandbox/benchmark/theBenchmark.p',fc6_lattice2) ).
fof(f9391,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/sandbox/benchmark/theBenchmark.p',t18_lattice2) ).
fof(f9463,axiom,
! [X0] :
( l3_lattices(X0)
=> ( v3_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k1_lattice2) ).
fof(f10300,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( ( ~ v3_struct_0(X1)
& v10_lattices(X1)
& l3_lattices(X1) )
=> ( m2_nat_lat(X1,X0)
<=> ( r1_tarski(u1_struct_0(X1),u1_struct_0(X0))
& u2_lattices(X1) = k1_realset1(u2_lattices(X0),u1_struct_0(X1))
& u1_lattices(X1) = k1_realset1(u1_lattices(X0),u1_struct_0(X1)) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d16_nat_lat) ).
fof(f10305,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> m2_nat_lat(X0,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t75_nat_lat) ).
fof(f12269,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> m2_lattice4(u1_struct_0(X0),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t10_lattice4) ).
fof(f13532,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_filter_2(X1,X0)
=> ( ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m2_filter_2) ).
fof(f13537,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> m1_filter_2(k1_filter_2(X0),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k1_filter_2) ).
fof(f13538,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> k1_filter_2(X0) = k1_filter_0(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k1_filter_2) ).
fof(f13565,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> m2_filter_2(k17_filter_2(X0),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k17_filter_2) ).
fof(f13572,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0)
& ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) )
=> m2_nat_lat(k23_filter_2(X0,X1),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k23_filter_2) ).
fof(f13582,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> k1_lattice2(k1_lattice2(X0)) = g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t7_filter_2) ).
fof(f13612,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> k17_filter_2(X0) = u1_struct_0(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d8_filter_2) ).
fof(f13666,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( ( ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) )
=> ! [X2] :
( m2_nat_lat(X2,X0)
=> ( X2 = k23_filter_2(X0,X1)
<=> ? [X3] :
( v1_funct_1(X3)
& v1_funct_2(X3,k2_zfmisc_1(X1,X1),X1)
& m2_relset_1(X3,k2_zfmisc_1(X1,X1),X1)
& ? [X4] :
( v1_funct_1(X4)
& v1_funct_2(X4,k2_zfmisc_1(X1,X1),X1)
& m2_relset_1(X4,k2_zfmisc_1(X1,X1),X1)
& X3 = k1_realset1(u2_lattices(X0),X1)
& X4 = k1_realset1(u1_lattices(X0),X1)
& X2 = g3_lattices(X1,X3,X4) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d16_filter_2) ).
fof(f13668,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_filter_2(X1,X0)
=> k8_filter_0(X0,X1) = k23_filter_2(X0,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t70_filter_2) ).
fof(f13670,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ( k23_filter_2(X0,k17_filter_2(X0)) = g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))
& k23_filter_2(X0,k1_filter_2(X0)) = g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t72_filter_2) ).
fof(f13671,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ( k23_filter_2(X0,k17_filter_2(X0)) = g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))
& k23_filter_2(X0,k1_filter_2(X0)) = g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) ) ),
inference(negated_conjecture,[status(cth)],[f13670]) ).
fof(f13703,plain,
! [X0] :
( ! [X1] :
( ( ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) )
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f13532]) ).
fof(f13704,plain,
! [X0] :
( ! [X1] :
( ( ~ v1_xboole_0(X1)
& m2_lattice4(X1,X0) )
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13703]) ).
fof(f13713,plain,
! [X0] :
( m1_filter_2(k1_filter_2(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f13537]) ).
fof(f13714,plain,
! [X0] :
( m1_filter_2(k1_filter_2(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13713]) ).
fof(f13715,plain,
! [X0] :
( k1_filter_2(X0) = k1_filter_0(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f13538]) ).
fof(f13716,plain,
! [X0] :
( k1_filter_2(X0) = k1_filter_0(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13715]) ).
fof(f13769,plain,
! [X0] :
( m2_filter_2(k17_filter_2(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f13565]) ).
fof(f13770,plain,
! [X0] :
( m2_filter_2(k17_filter_2(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13769]) ).
fof(f13783,plain,
! [X0,X1] :
( m2_nat_lat(k23_filter_2(X0,X1),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0) ),
inference(ennf_transformation,[],[f13572]) ).
fof(f13784,plain,
! [X0,X1] :
( m2_nat_lat(k23_filter_2(X0,X1),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0) ),
inference(flattening,[],[f13783]) ).
fof(f13802,plain,
! [X0] :
( k1_lattice2(k1_lattice2(X0)) = g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f13582]) ).
fof(f13803,plain,
! [X0] :
( k1_lattice2(k1_lattice2(X0)) = g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13802]) ).
fof(f13860,plain,
! [X0] :
( k17_filter_2(X0) = u1_struct_0(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f13612]) ).
fof(f13861,plain,
! [X0] :
( k17_filter_2(X0) = u1_struct_0(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13860]) ).
fof(f13968,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( X2 = k23_filter_2(X0,X1)
<=> ? [X3] :
( v1_funct_1(X3)
& v1_funct_2(X3,k2_zfmisc_1(X1,X1),X1)
& m2_relset_1(X3,k2_zfmisc_1(X1,X1),X1)
& ? [X4] :
( v1_funct_1(X4)
& v1_funct_2(X4,k2_zfmisc_1(X1,X1),X1)
& m2_relset_1(X4,k2_zfmisc_1(X1,X1),X1)
& X3 = k1_realset1(u2_lattices(X0),X1)
& X4 = k1_realset1(u1_lattices(X0),X1)
& X2 = g3_lattices(X1,X3,X4) ) ) )
| ~ m2_nat_lat(X2,X0) )
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f13666]) ).
fof(f13969,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( X2 = k23_filter_2(X0,X1)
<=> ? [X3] :
( v1_funct_1(X3)
& v1_funct_2(X3,k2_zfmisc_1(X1,X1),X1)
& m2_relset_1(X3,k2_zfmisc_1(X1,X1),X1)
& ? [X4] :
( v1_funct_1(X4)
& v1_funct_2(X4,k2_zfmisc_1(X1,X1),X1)
& m2_relset_1(X4,k2_zfmisc_1(X1,X1),X1)
& X3 = k1_realset1(u2_lattices(X0),X1)
& X4 = k1_realset1(u1_lattices(X0),X1)
& X2 = g3_lattices(X1,X3,X4) ) ) )
| ~ m2_nat_lat(X2,X0) )
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13968]) ).
fof(f13972,plain,
! [X0] :
( ! [X1] :
( k8_filter_0(X0,X1) = k23_filter_2(X0,X1)
| ~ m1_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f13668]) ).
fof(f13973,plain,
! [X0] :
( ! [X1] :
( k8_filter_0(X0,X1) = k23_filter_2(X0,X1)
| ~ m1_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13972]) ).
fof(f13976,plain,
? [X0] :
( ( g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) != k23_filter_2(X0,k17_filter_2(X0))
| g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) != k23_filter_2(X0,k1_filter_2(X0)) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(ennf_transformation,[],[f13671]) ).
fof(f13977,plain,
? [X0] :
( ( g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) != k23_filter_2(X0,k17_filter_2(X0))
| g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) != k23_filter_2(X0,k1_filter_2(X0)) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(flattening,[],[f13976]) ).
fof(f13992,plain,
! [X0] :
( m2_lattice4(u1_struct_0(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f12269]) ).
fof(f13993,plain,
! [X0] :
( m2_lattice4(u1_struct_0(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f13992]) ).
fof(f14030,plain,
! [X0] :
( k1_filter_0(X0) = u1_struct_0(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f8589]) ).
fof(f14031,plain,
! [X0] :
( k1_filter_0(X0) = u1_struct_0(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f14030]) ).
fof(f14106,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,[],[f9391]) ).
fof(f14107,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,[],[f14106]) ).
fof(f14113,plain,
! [X0] :
( m2_nat_lat(X0,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f10305]) ).
fof(f14114,plain,
! [X0] :
( m2_nat_lat(X0,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f14113]) ).
fof(f14115,plain,
! [X0] :
( ! [X1] :
( ( m2_nat_lat(X1,X0)
<=> ( r1_tarski(u1_struct_0(X1),u1_struct_0(X0))
& u2_lattices(X1) = k1_realset1(u2_lattices(X0),u1_struct_0(X1))
& u1_lattices(X1) = k1_realset1(u1_lattices(X0),u1_struct_0(X1)) ) )
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f10300]) ).
fof(f14116,plain,
! [X0] :
( ! [X1] :
( ( m2_nat_lat(X1,X0)
<=> ( r1_tarski(u1_struct_0(X1),u1_struct_0(X0))
& u2_lattices(X1) = k1_realset1(u2_lattices(X0),u1_struct_0(X1))
& u1_lattices(X1) = k1_realset1(u1_lattices(X0),u1_struct_0(X1)) ) )
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f14115]) ).
fof(f14119,plain,
! [X0] :
( ( v3_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) )
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f9463]) ).
fof(f14122,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,[],[f9363]) ).
fof(f14123,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,[],[f14122]) ).
fof(f14124,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f9358]) ).
fof(f14125,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f14124]) ).
fof(f16102,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( X2 = k23_filter_2(X0,X1)
| ! [X3] :
( ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(X3,k2_zfmisc_1(X1,X1),X1)
| ! [X4] :
( ~ v1_funct_1(X4)
| ~ v1_funct_2(X4,k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(X4,k2_zfmisc_1(X1,X1),X1)
| k1_realset1(u2_lattices(X0),X1) != X3
| k1_realset1(u1_lattices(X0),X1) != X4
| g3_lattices(X1,X3,X4) != X2 ) ) )
& ( ? [X3] :
( v1_funct_1(X3)
& v1_funct_2(X3,k2_zfmisc_1(X1,X1),X1)
& m2_relset_1(X3,k2_zfmisc_1(X1,X1),X1)
& ? [X4] :
( v1_funct_1(X4)
& v1_funct_2(X4,k2_zfmisc_1(X1,X1),X1)
& m2_relset_1(X4,k2_zfmisc_1(X1,X1),X1)
& X3 = k1_realset1(u2_lattices(X0),X1)
& X4 = k1_realset1(u1_lattices(X0),X1)
& X2 = g3_lattices(X1,X3,X4) ) )
| k23_filter_2(X0,X1) != X2 ) )
| ~ m2_nat_lat(X2,X0) )
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f13969]) ).
fof(f16103,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( X2 = k23_filter_2(X0,X1)
| ! [X3] :
( ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(X3,k2_zfmisc_1(X1,X1),X1)
| ! [X4] :
( ~ v1_funct_1(X4)
| ~ v1_funct_2(X4,k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(X4,k2_zfmisc_1(X1,X1),X1)
| k1_realset1(u2_lattices(X0),X1) != X3
| k1_realset1(u1_lattices(X0),X1) != X4
| g3_lattices(X1,X3,X4) != X2 ) ) )
& ( ? [X5] :
( v1_funct_1(X5)
& v1_funct_2(X5,k2_zfmisc_1(X1,X1),X1)
& m2_relset_1(X5,k2_zfmisc_1(X1,X1),X1)
& ? [X6] :
( v1_funct_1(X6)
& v1_funct_2(X6,k2_zfmisc_1(X1,X1),X1)
& m2_relset_1(X6,k2_zfmisc_1(X1,X1),X1)
& k1_realset1(u2_lattices(X0),X1) = X5
& k1_realset1(u1_lattices(X0),X1) = X6
& g3_lattices(X1,X5,X6) = X2 ) )
| k23_filter_2(X0,X1) != X2 ) )
| ~ m2_nat_lat(X2,X0) )
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(rectify,[],[f16102]) ).
fof(f16104,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( X2 = k23_filter_2(X0,X1)
| ! [X3] :
( ~ v1_funct_1(X3)
| ~ v1_funct_2(X3,k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(X3,k2_zfmisc_1(X1,X1),X1)
| ! [X4] :
( ~ v1_funct_1(X4)
| ~ v1_funct_2(X4,k2_zfmisc_1(X1,X1),X1)
| ~ m2_relset_1(X4,k2_zfmisc_1(X1,X1),X1)
| k1_realset1(u2_lattices(X0),X1) != X3
| k1_realset1(u1_lattices(X0),X1) != X4
| g3_lattices(X1,X3,X4) != X2 ) ) )
& ( ( v1_funct_1(sK35(X0,X1,X2))
& v1_funct_2(sK35(X0,X1,X2),k2_zfmisc_1(X1,X1),X1)
& m2_relset_1(sK35(X0,X1,X2),k2_zfmisc_1(X1,X1),X1)
& v1_funct_1(sK36(X0,X1,X2))
& v1_funct_2(sK36(X0,X1,X2),k2_zfmisc_1(X1,X1),X1)
& m2_relset_1(sK36(X0,X1,X2),k2_zfmisc_1(X1,X1),X1)
& k1_realset1(u2_lattices(X0),X1) = sK35(X0,X1,X2)
& k1_realset1(u1_lattices(X0),X1) = sK36(X0,X1,X2)
& g3_lattices(X1,sK35(X0,X1,X2),sK36(X0,X1,X2)) = X2 )
| k23_filter_2(X0,X1) != X2 ) )
| ~ m2_nat_lat(X2,X0) )
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK35,sK36]),skolemize(X5,sK35(X0,X1,X2)),skolemize(X6,sK36(X0,X1,X2))],[f16103]) ).
fof(f16105,plain,
( ( g3_lattices(u1_struct_0(sK37),u2_lattices(sK37),u1_lattices(sK37)) != k23_filter_2(sK37,k17_filter_2(sK37))
| g3_lattices(u1_struct_0(sK37),u2_lattices(sK37),u1_lattices(sK37)) != k23_filter_2(sK37,k1_filter_2(sK37)) )
& ~ v3_struct_0(sK37)
& v10_lattices(sK37)
& l3_lattices(sK37) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK37]),skolemize(X0,sK37)],[f13977]) ).
fof(f16142,plain,
! [X0] :
( ! [X1] :
( ( ( m2_nat_lat(X1,X0)
| ~ r1_tarski(u1_struct_0(X1),u1_struct_0(X0))
| u2_lattices(X1) != k1_realset1(u2_lattices(X0),u1_struct_0(X1))
| u1_lattices(X1) != k1_realset1(u1_lattices(X0),u1_struct_0(X1)) )
& ( ( r1_tarski(u1_struct_0(X1),u1_struct_0(X0))
& u2_lattices(X1) = k1_realset1(u2_lattices(X0),u1_struct_0(X1))
& u1_lattices(X1) = k1_realset1(u1_lattices(X0),u1_struct_0(X1)) )
| ~ m2_nat_lat(X1,X0) ) )
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f14116]) ).
fof(f16143,plain,
! [X0] :
( ! [X1] :
( ( ( m2_nat_lat(X1,X0)
| ~ r1_tarski(u1_struct_0(X1),u1_struct_0(X0))
| u2_lattices(X1) != k1_realset1(u2_lattices(X0),u1_struct_0(X1))
| u1_lattices(X1) != k1_realset1(u1_lattices(X0),u1_struct_0(X1)) )
& ( ( r1_tarski(u1_struct_0(X1),u1_struct_0(X0))
& u2_lattices(X1) = k1_realset1(u2_lattices(X0),u1_struct_0(X1))
& u1_lattices(X1) = k1_realset1(u1_lattices(X0),u1_struct_0(X1)) )
| ~ m2_nat_lat(X1,X0) ) )
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f16142]) ).
fof(f16903,plain,
! [X0,X1] :
( ~ v10_lattices(X0)
| ~ m2_filter_2(X1,X0)
| v3_struct_0(X0)
| m2_lattice4(X1,X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13704]) ).
fof(f16904,plain,
! [X0,X1] :
( ~ v1_xboole_0(X1)
| ~ m2_filter_2(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13704]) ).
fof(f16910,plain,
! [X0] :
( ~ v10_lattices(X0)
| v3_struct_0(X0)
| m1_filter_2(k1_filter_2(X0),X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13714]) ).
fof(f16911,plain,
! [X0] :
( ~ v10_lattices(X0)
| v3_struct_0(X0)
| k1_filter_0(X0) = k1_filter_2(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13716]) ).
fof(f16940,plain,
! [X0] :
( m2_filter_2(k17_filter_2(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13770]) ).
fof(f16948,plain,
! [X0,X1] :
( ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| v1_xboole_0(X1)
| m2_nat_lat(k23_filter_2(X0,X1),X0) ),
inference(cnf_transformation,[],[f13784]) ).
fof(f16968,plain,
! [X0] :
( ~ v10_lattices(X0)
| v3_struct_0(X0)
| g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) = k1_lattice2(k1_lattice2(X0))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13803]) ).
fof(f17041,plain,
! [X0] :
( ~ v10_lattices(X0)
| v3_struct_0(X0)
| u1_struct_0(X0) = k17_filter_2(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13861]) ).
fof(f17206,plain,
! [X2,X0,X1] :
( g3_lattices(X1,sK35(X0,X1,X2),sK36(X0,X1,X2)) = X2
| k23_filter_2(X0,X1) != X2
| ~ m2_nat_lat(X2,X0)
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f16104]) ).
fof(f17207,plain,
! [X2,X0,X1] :
( k1_realset1(u1_lattices(X0),X1) = sK36(X0,X1,X2)
| k23_filter_2(X0,X1) != X2
| ~ m2_nat_lat(X2,X0)
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f16104]) ).
fof(f17208,plain,
! [X2,X0,X1] :
( k1_realset1(u2_lattices(X0),X1) = sK35(X0,X1,X2)
| k23_filter_2(X0,X1) != X2
| ~ m2_nat_lat(X2,X0)
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f16104]) ).
fof(f17225,plain,
! [X0,X1] :
( ~ m1_filter_2(X1,X0)
| k8_filter_0(X0,X1) = k23_filter_2(X0,X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13973]) ).
fof(f17227,plain,
l3_lattices(sK37),
inference(cnf_transformation,[],[f16105]) ).
fof(f17228,plain,
v10_lattices(sK37),
inference(cnf_transformation,[],[f16105]) ).
fof(f17229,plain,
~ v3_struct_0(sK37),
inference(cnf_transformation,[],[f16105]) ).
fof(f17230,plain,
( g3_lattices(u1_struct_0(sK37),u2_lattices(sK37),u1_lattices(sK37)) != k23_filter_2(sK37,k17_filter_2(sK37))
| g3_lattices(u1_struct_0(sK37),u2_lattices(sK37),u1_lattices(sK37)) != k23_filter_2(sK37,k1_filter_2(sK37)) ),
inference(cnf_transformation,[],[f16105]) ).
fof(f17251,plain,
! [X0] :
( ~ v10_lattices(X0)
| v3_struct_0(X0)
| m2_lattice4(u1_struct_0(X0),X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f13993]) ).
fof(f17289,plain,
! [X0] :
( ~ v10_lattices(X0)
| v3_struct_0(X0)
| u1_struct_0(X0) = k1_filter_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f14031]) ).
fof(f17360,plain,
! [X0] :
( ~ l3_lattices(X0)
| v3_struct_0(X0)
| u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0)) ),
inference(cnf_transformation,[],[f14107]) ).
fof(f17366,plain,
! [X0] :
( ~ v10_lattices(X0)
| v3_struct_0(X0)
| m2_nat_lat(X0,X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f14114]) ).
fof(f17367,plain,
! [X0,X1] :
( ~ m2_nat_lat(X1,X0)
| u1_lattices(X1) = k1_realset1(u1_lattices(X0),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f16143]) ).
fof(f17368,plain,
! [X0,X1] :
( ~ m2_nat_lat(X1,X0)
| u2_lattices(X1) = k1_realset1(u2_lattices(X0),u1_struct_0(X1))
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f16143]) ).
fof(f17381,plain,
! [X0] :
( ~ l3_lattices(X0)
| l3_lattices(k1_lattice2(X0)) ),
inference(cnf_transformation,[],[f14119]) ).
fof(f17384,plain,
! [X0] :
( ~ v10_lattices(X0)
| v3_struct_0(X0)
| v10_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f14123]) ).
fof(f17394,plain,
! [X0] :
( ~ v3_struct_0(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f14125]) ).
fof(f21061,plain,
! [X0,X1] :
( ~ m2_lattice4(X1,X0)
| ~ m2_nat_lat(k23_filter_2(X0,X1),X0)
| v1_xboole_0(X1)
| k1_realset1(u2_lattices(X0),X1) = sK35(X0,X1,k23_filter_2(X0,X1))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(equality_resolution,[],[f17208]) ).
fof(f21062,plain,
! [X0,X1] :
( ~ m2_lattice4(X1,X0)
| ~ m2_nat_lat(k23_filter_2(X0,X1),X0)
| v1_xboole_0(X1)
| k1_realset1(u1_lattices(X0),X1) = sK36(X0,X1,k23_filter_2(X0,X1))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(equality_resolution,[],[f17207]) ).
fof(f21063,plain,
! [X0,X1] :
( ~ m2_nat_lat(k23_filter_2(X0,X1),X0)
| k23_filter_2(X0,X1) = g3_lattices(X1,sK35(X0,X1,k23_filter_2(X0,X1)),sK36(X0,X1,k23_filter_2(X0,X1)))
| v1_xboole_0(X1)
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(equality_resolution,[],[f17206]) ).
fof(f21635,definition,
( spl526_13
<=> g3_lattices(u1_struct_0(sK37),u2_lattices(sK37),u1_lattices(sK37)) = k23_filter_2(sK37,k1_filter_2(sK37)) ),
introduced(definition,[new_symbols(definition,[spl526_13])],[avatar_definition]) ).
fof(f21636,plain,
( g3_lattices(u1_struct_0(sK37),u2_lattices(sK37),u1_lattices(sK37)) != k23_filter_2(sK37,k1_filter_2(sK37))
| spl526_13 ),
inference(avatar_component_clause,[],[f21635]) ).
fof(f21638,definition,
( spl526_14
<=> g3_lattices(u1_struct_0(sK37),u2_lattices(sK37),u1_lattices(sK37)) = k23_filter_2(sK37,k17_filter_2(sK37)) ),
introduced(definition,[new_symbols(definition,[spl526_14])],[avatar_definition]) ).
fof(f21639,plain,
( g3_lattices(u1_struct_0(sK37),u2_lattices(sK37),u1_lattices(sK37)) != k23_filter_2(sK37,k17_filter_2(sK37))
| spl526_14 ),
inference(avatar_component_clause,[],[f21638]) ).
fof(f21640,plain,
( ~ spl526_13
| ~ spl526_14 ),
inference(avatar_split_clause,[],[f17230,f21638,f21635]) ).
fof(f21861,plain,
( v3_struct_0(sK37)
| g3_lattices(u1_struct_0(sK37),u2_lattices(sK37),u1_lattices(sK37)) = k1_lattice2(k1_lattice2(sK37))
| ~ l3_lattices(sK37) ),
inference(resolution,[],[f17228,f16968]) ).
fof(f21862,plain,
( g3_lattices(u1_struct_0(sK37),u2_lattices(sK37),u1_lattices(sK37)) = k1_lattice2(k1_lattice2(sK37))
| ~ l3_lattices(sK37) ),
inference(forward_subsumption_resolution,[],[f21861,f17229]) ).
fof(f21863,plain,
g3_lattices(u1_struct_0(sK37),u2_lattices(sK37),u1_lattices(sK37)) = k1_lattice2(k1_lattice2(sK37)),
inference(forward_subsumption_resolution,[],[f21862,f17227]) ).
fof(f21868,plain,
( k23_filter_2(sK37,k17_filter_2(sK37)) != k1_lattice2(k1_lattice2(sK37))
| spl526_14 ),
inference(superposition,[],[f21639,f21863]) ).
fof(f21869,plain,
( v3_struct_0(sK37)
| u1_struct_0(sK37) = k17_filter_2(sK37)
| ~ l3_lattices(sK37) ),
inference(resolution,[],[f17041,f17228]) ).
fof(f21870,plain,
( u1_struct_0(sK37) = k17_filter_2(sK37)
| ~ l3_lattices(sK37) ),
inference(forward_subsumption_resolution,[],[f21869,f17229]) ).
fof(f21871,plain,
u1_struct_0(sK37) = k17_filter_2(sK37),
inference(forward_subsumption_resolution,[],[f21870,f17227]) ).
fof(f21872,plain,
( k1_lattice2(k1_lattice2(sK37)) != k23_filter_2(sK37,u1_struct_0(sK37))
| spl526_14 ),
inference(superposition,[],[f21868,f21871]) ).
fof(f21873,plain,
( v3_struct_0(sK37)
| u1_struct_0(sK37) = k1_filter_0(sK37)
| ~ l3_lattices(sK37) ),
inference(resolution,[],[f17289,f17228]) ).
fof(f21874,plain,
( u1_struct_0(sK37) = k1_filter_0(sK37)
| ~ l3_lattices(sK37) ),
inference(forward_subsumption_resolution,[],[f21873,f17229]) ).
fof(f21875,plain,
u1_struct_0(sK37) = k1_filter_0(sK37),
inference(forward_subsumption_resolution,[],[f21874,f17227]) ).
fof(f21876,plain,
( v3_struct_0(sK37)
| u1_struct_0(sK37) = u1_struct_0(k1_lattice2(sK37)) ),
inference(resolution,[],[f17360,f17227]) ).
fof(f21877,plain,
u1_struct_0(sK37) = u1_struct_0(k1_lattice2(sK37)),
inference(forward_subsumption_resolution,[],[f21876,f17229]) ).
fof(f21878,plain,
( v3_struct_0(sK37)
| k1_filter_2(sK37) = k1_filter_0(sK37)
| ~ l3_lattices(sK37) ),
inference(resolution,[],[f16911,f17228]) ).
fof(f21879,plain,
( k1_filter_2(sK37) = k1_filter_0(sK37)
| ~ l3_lattices(sK37) ),
inference(forward_subsumption_resolution,[],[f21878,f17229]) ).
fof(f21880,plain,
k1_filter_2(sK37) = k1_filter_0(sK37),
inference(forward_subsumption_resolution,[],[f21879,f17227]) ).
fof(f21881,plain,
u1_struct_0(sK37) = k1_filter_2(sK37),
inference(forward_demodulation,[],[f21880,f21875]) ).
fof(f21890,definition,
( spl526_17
<=> v3_struct_0(k1_lattice2(sK37)) ),
introduced(definition,[new_symbols(definition,[spl526_17])],[avatar_definition]) ).
fof(f21891,plain,
( v3_struct_0(k1_lattice2(sK37))
| ~ spl526_17 ),
inference(avatar_component_clause,[],[f21890]) ).
fof(f21918,plain,
l3_lattices(k1_lattice2(sK37)),
inference(resolution,[],[f17381,f17227]) ).
fof(f21953,plain,
( v3_struct_0(sK37)
| m1_filter_2(k1_filter_2(sK37),sK37)
| ~ l3_lattices(sK37) ),
inference(resolution,[],[f16910,f17228]) ).
fof(f21954,plain,
( m1_filter_2(k1_filter_2(sK37),sK37)
| ~ l3_lattices(sK37) ),
inference(forward_subsumption_resolution,[],[f21953,f17229]) ).
fof(f21955,plain,
m1_filter_2(k1_filter_2(sK37),sK37),
inference(forward_subsumption_resolution,[],[f21954,f17227]) ).
fof(f21956,plain,
m1_filter_2(u1_struct_0(sK37),sK37),
inference(forward_demodulation,[],[f21955,f21881]) ).
fof(f21958,plain,
( k23_filter_2(sK37,u1_struct_0(sK37)) = k8_filter_0(sK37,u1_struct_0(sK37))
| v3_struct_0(sK37)
| ~ v10_lattices(sK37)
| ~ l3_lattices(sK37) ),
inference(resolution,[],[f21956,f17225]) ).
fof(f21959,plain,
( k23_filter_2(sK37,u1_struct_0(sK37)) = k8_filter_0(sK37,u1_struct_0(sK37))
| ~ v10_lattices(sK37)
| ~ l3_lattices(sK37) ),
inference(forward_subsumption_resolution,[],[f21958,f17229]) ).
fof(f21960,plain,
( k23_filter_2(sK37,u1_struct_0(sK37)) = k8_filter_0(sK37,u1_struct_0(sK37))
| ~ l3_lattices(sK37) ),
inference(forward_subsumption_resolution,[],[f21959,f17228]) ).
fof(f21961,plain,
k23_filter_2(sK37,u1_struct_0(sK37)) = k8_filter_0(sK37,u1_struct_0(sK37)),
inference(forward_subsumption_resolution,[],[f21960,f17227]) ).
fof(f21962,plain,
( k1_lattice2(k1_lattice2(sK37)) != k8_filter_0(sK37,u1_struct_0(sK37))
| spl526_14 ),
inference(superposition,[],[f21872,f21961]) ).
fof(f21963,plain,
( ~ m2_nat_lat(k8_filter_0(sK37,u1_struct_0(sK37)),sK37)
| k8_filter_0(sK37,u1_struct_0(sK37)) = g3_lattices(u1_struct_0(sK37),sK35(sK37,u1_struct_0(sK37),k8_filter_0(sK37,u1_struct_0(sK37))),sK36(sK37,u1_struct_0(sK37),k8_filter_0(sK37,u1_struct_0(sK37))))
| v1_xboole_0(u1_struct_0(sK37))
| ~ m2_lattice4(u1_struct_0(sK37),sK37)
| v3_struct_0(sK37)
| ~ v10_lattices(sK37)
| ~ l3_lattices(sK37) ),
inference(superposition,[],[f21063,f21961]) ).
fof(f21964,plain,
( ~ m2_nat_lat(k8_filter_0(sK37,u1_struct_0(sK37)),sK37)
| k8_filter_0(sK37,u1_struct_0(sK37)) = g3_lattices(u1_struct_0(sK37),sK35(sK37,u1_struct_0(sK37),k8_filter_0(sK37,u1_struct_0(sK37))),sK36(sK37,u1_struct_0(sK37),k8_filter_0(sK37,u1_struct_0(sK37))))
| v1_xboole_0(u1_struct_0(sK37))
| v3_struct_0(sK37)
| ~ v10_lattices(sK37)
| ~ l3_lattices(sK37) ),
inference(forward_subsumption_resolution,[],[f21963,f17251]) ).
fof(f21965,plain,
( ~ m2_nat_lat(k8_filter_0(sK37,u1_struct_0(sK37)),sK37)
| k8_filter_0(sK37,u1_struct_0(sK37)) = g3_lattices(u1_struct_0(sK37),sK35(sK37,u1_struct_0(sK37),k8_filter_0(sK37,u1_struct_0(sK37))),sK36(sK37,u1_struct_0(sK37),k8_filter_0(sK37,u1_struct_0(sK37))))
| v1_xboole_0(u1_struct_0(sK37))
| ~ v10_lattices(sK37)
| ~ l3_lattices(sK37) ),
inference(forward_subsumption_resolution,[],[f21964,f17229]) ).
fof(f21966,plain,
( ~ m2_nat_lat(k8_filter_0(sK37,u1_struct_0(sK37)),sK37)
| k8_filter_0(sK37,u1_struct_0(sK37)) = g3_lattices(u1_struct_0(sK37),sK35(sK37,u1_struct_0(sK37),k8_filter_0(sK37,u1_struct_0(sK37))),sK36(sK37,u1_struct_0(sK37),k8_filter_0(sK37,u1_struct_0(sK37))))
| v1_xboole_0(u1_struct_0(sK37))
| ~ l3_lattices(sK37) ),
inference(forward_subsumption_resolution,[],[f21965,f17228]) ).
fof(f21967,plain,
( ~ m2_nat_lat(k8_filter_0(sK37,u1_struct_0(sK37)),sK37)
| k8_filter_0(sK37,u1_struct_0(sK37)) = g3_lattices(u1_struct_0(sK37),sK35(sK37,u1_struct_0(sK37),k8_filter_0(sK37,u1_struct_0(sK37))),sK36(sK37,u1_struct_0(sK37),k8_filter_0(sK37,u1_struct_0(sK37))))
| v1_xboole_0(u1_struct_0(sK37)) ),
inference(forward_subsumption_resolution,[],[f21966,f17227]) ).
fof(f21969,definition,
( spl526_22
<=> v1_xboole_0(u1_struct_0(sK37)) ),
introduced(definition,[new_symbols(definition,[spl526_22])],[avatar_definition]) ).
fof(f21970,plain,
( v1_xboole_0(u1_struct_0(sK37))
| ~ spl526_22 ),
inference(avatar_component_clause,[],[f21969]) ).
fof(f21972,definition,
( spl526_23
<=> k8_filter_0(sK37,u1_struct_0(sK37)) = g3_lattices(u1_struct_0(sK37),sK35(sK37,u1_struct_0(sK37),k8_filter_0(sK37,u1_struct_0(sK37))),sK36(sK37,u1_struct_0(sK37),k8_filter_0(sK37,u1_struct_0(sK37)))) ),
introduced(definition,[new_symbols(definition,[spl526_23])],[avatar_definition]) ).
fof(f21973,plain,
( k8_filter_0(sK37,u1_struct_0(sK37)) = g3_lattices(u1_struct_0(sK37),sK35(sK37,u1_struct_0(sK37),k8_filter_0(sK37,u1_struct_0(sK37))),sK36(sK37,u1_struct_0(sK37),k8_filter_0(sK37,u1_struct_0(sK37))))
| ~ spl526_23 ),
inference(avatar_component_clause,[],[f21972]) ).
fof(f21975,definition,
( spl526_24
<=> m2_nat_lat(k8_filter_0(sK37,u1_struct_0(sK37)),sK37) ),
introduced(definition,[new_symbols(definition,[spl526_24])],[avatar_definition]) ).
fof(f21977,plain,
( spl526_22
| spl526_23
| ~ spl526_24 ),
inference(avatar_split_clause,[],[f21967,f21975,f21972,f21969]) ).
fof(f21994,plain,
( v3_struct_0(sK37)
| ~ l3_lattices(sK37)
| ~ spl526_17 ),
inference(resolution,[],[f17394,f21891]) ).
fof(f21996,plain,
( ~ l3_lattices(sK37)
| ~ spl526_17 ),
inference(forward_subsumption_resolution,[],[f21994,f17229]) ).
fof(f21997,plain,
( $false
| ~ spl526_17 ),
inference(forward_subsumption_resolution,[],[f21996,f17227]) ).
fof(f21998,plain,
~ spl526_17,
inference(avatar_contradiction_clause,[],[f21997]) ).
fof(f22006,plain,
( v3_struct_0(sK37)
| v10_lattices(k1_lattice2(sK37))
| ~ l3_lattices(sK37) ),
inference(resolution,[],[f17384,f17228]) ).
fof(f22008,plain,
( v10_lattices(k1_lattice2(sK37))
| ~ l3_lattices(sK37) ),
inference(forward_subsumption_resolution,[],[f22006,f17229]) ).
fof(f22013,plain,
v10_lattices(k1_lattice2(sK37)),
inference(forward_subsumption_resolution,[],[f22008,f17227]) ).
fof(f22026,plain,
( v3_struct_0(k1_lattice2(sK37))
| u1_struct_0(k1_lattice2(sK37)) = k17_filter_2(k1_lattice2(sK37))
| ~ l3_lattices(k1_lattice2(sK37)) ),
inference(resolution,[],[f22013,f17041]) ).
fof(f22043,plain,
( v3_struct_0(k1_lattice2(sK37))
| u1_struct_0(k1_lattice2(sK37)) = k17_filter_2(k1_lattice2(sK37)) ),
inference(forward_subsumption_resolution,[],[f22026,f21918]) ).
fof(f22061,plain,
( u1_struct_0(sK37) = k17_filter_2(k1_lattice2(sK37))
| v3_struct_0(k1_lattice2(sK37)) ),
inference(forward_demodulation,[],[f22043,f21877]) ).
fof(f22085,definition,
( spl526_30
<=> u1_struct_0(sK37) = k17_filter_2(k1_lattice2(sK37)) ),
introduced(definition,[new_symbols(definition,[spl526_30])],[avatar_definition]) ).
fof(f22086,plain,
( u1_struct_0(sK37) = k17_filter_2(k1_lattice2(sK37))
| ~ spl526_30 ),
inference(avatar_component_clause,[],[f22085]) ).
fof(f22087,plain,
( spl526_17
| spl526_30 ),
inference(avatar_split_clause,[],[f22061,f22085,f21890]) ).
fof(f22122,plain,
( ~ v3_struct_0(k1_lattice2(sK37))
| spl526_17 ),
inference(avatar_component_clause,[],[f21890]) ).
fof(f22124,plain,
( m2_filter_2(u1_struct_0(sK37),k1_lattice2(sK37))
| v3_struct_0(k1_lattice2(sK37))
| ~ v10_lattices(k1_lattice2(sK37))
| ~ l3_lattices(k1_lattice2(sK37))
| ~ spl526_30 ),
inference(superposition,[],[f16940,f22086]) ).
fof(f22125,plain,
( m2_filter_2(u1_struct_0(sK37),k1_lattice2(sK37))
| ~ v10_lattices(k1_lattice2(sK37))
| ~ l3_lattices(k1_lattice2(sK37))
| spl526_17
| ~ spl526_30 ),
inference(forward_subsumption_resolution,[],[f22124,f22122]) ).
fof(f22126,plain,
( m2_filter_2(u1_struct_0(sK37),k1_lattice2(sK37))
| ~ l3_lattices(k1_lattice2(sK37))
| spl526_17
| ~ spl526_30 ),
inference(forward_subsumption_resolution,[],[f22125,f22013]) ).
fof(f22127,plain,
( m2_filter_2(u1_struct_0(sK37),k1_lattice2(sK37))
| spl526_17
| ~ spl526_30 ),
inference(forward_subsumption_resolution,[],[f22126,f21918]) ).
fof(f22197,plain,
( v3_struct_0(sK37)
| m2_nat_lat(sK37,sK37)
| ~ l3_lattices(sK37) ),
inference(resolution,[],[f17366,f17228]) ).
fof(f22200,plain,
( m2_nat_lat(sK37,sK37)
| ~ l3_lattices(sK37) ),
inference(forward_subsumption_resolution,[],[f22197,f17229]) ).
fof(f22202,plain,
m2_nat_lat(sK37,sK37),
inference(forward_subsumption_resolution,[],[f22200,f17227]) ).
fof(f22205,plain,
( u1_lattices(sK37) = k1_realset1(u1_lattices(sK37),u1_struct_0(sK37))
| v3_struct_0(sK37)
| ~ v10_lattices(sK37)
| ~ l3_lattices(sK37)
| v3_struct_0(sK37)
| ~ v10_lattices(sK37)
| ~ l3_lattices(sK37) ),
inference(resolution,[],[f22202,f17367]) ).
fof(f22206,plain,
( u2_lattices(sK37) = k1_realset1(u2_lattices(sK37),u1_struct_0(sK37))
| v3_struct_0(sK37)
| ~ v10_lattices(sK37)
| ~ l3_lattices(sK37)
| v3_struct_0(sK37)
| ~ v10_lattices(sK37)
| ~ l3_lattices(sK37) ),
inference(resolution,[],[f22202,f17368]) ).
fof(f22207,plain,
( u2_lattices(sK37) = k1_realset1(u2_lattices(sK37),u1_struct_0(sK37))
| v3_struct_0(sK37)
| ~ v10_lattices(sK37)
| ~ l3_lattices(sK37) ),
inference(duplicate_literal_removal,[],[f22206]) ).
fof(f22208,plain,
( u1_lattices(sK37) = k1_realset1(u1_lattices(sK37),u1_struct_0(sK37))
| v3_struct_0(sK37)
| ~ v10_lattices(sK37)
| ~ l3_lattices(sK37) ),
inference(duplicate_literal_removal,[],[f22205]) ).
fof(f22209,plain,
( u2_lattices(sK37) = k1_realset1(u2_lattices(sK37),u1_struct_0(sK37))
| ~ v10_lattices(sK37)
| ~ l3_lattices(sK37) ),
inference(forward_subsumption_resolution,[],[f22207,f17229]) ).
fof(f22210,plain,
( u1_lattices(sK37) = k1_realset1(u1_lattices(sK37),u1_struct_0(sK37))
| ~ v10_lattices(sK37)
| ~ l3_lattices(sK37) ),
inference(forward_subsumption_resolution,[],[f22208,f17229]) ).
fof(f22213,plain,
( u2_lattices(sK37) = k1_realset1(u2_lattices(sK37),u1_struct_0(sK37))
| ~ l3_lattices(sK37) ),
inference(forward_subsumption_resolution,[],[f22209,f17228]) ).
fof(f22214,plain,
( u1_lattices(sK37) = k1_realset1(u1_lattices(sK37),u1_struct_0(sK37))
| ~ l3_lattices(sK37) ),
inference(forward_subsumption_resolution,[],[f22210,f17228]) ).
fof(f22217,plain,
u2_lattices(sK37) = k1_realset1(u2_lattices(sK37),u1_struct_0(sK37)),
inference(forward_subsumption_resolution,[],[f22213,f17227]) ).
fof(f22218,plain,
u1_lattices(sK37) = k1_realset1(u1_lattices(sK37),u1_struct_0(sK37)),
inference(forward_subsumption_resolution,[],[f22214,f17227]) ).
fof(f22361,plain,
! [X0] :
( ~ m2_filter_2(X0,sK37)
| v3_struct_0(sK37)
| m2_lattice4(X0,sK37)
| ~ l3_lattices(sK37) ),
inference(resolution,[],[f16903,f17228]) ).
fof(f22364,plain,
! [X0] :
( ~ m2_filter_2(X0,sK37)
| m2_lattice4(X0,sK37)
| ~ l3_lattices(sK37) ),
inference(forward_subsumption_resolution,[],[f22361,f17229]) ).
fof(f22366,plain,
! [X0] :
( ~ m2_filter_2(X0,sK37)
| m2_lattice4(X0,sK37) ),
inference(forward_subsumption_resolution,[],[f22364,f17227]) ).
fof(f22367,plain,
( m2_lattice4(k17_filter_2(sK37),sK37)
| v3_struct_0(sK37)
| ~ v10_lattices(sK37)
| ~ l3_lattices(sK37) ),
inference(resolution,[],[f22366,f16940]) ).
fof(f22370,plain,
( m2_lattice4(k17_filter_2(sK37),sK37)
| ~ v10_lattices(sK37)
| ~ l3_lattices(sK37) ),
inference(forward_subsumption_resolution,[],[f22367,f17229]) ).
fof(f22371,plain,
( m2_lattice4(k17_filter_2(sK37),sK37)
| ~ l3_lattices(sK37) ),
inference(forward_subsumption_resolution,[],[f22370,f17228]) ).
fof(f22372,plain,
m2_lattice4(k17_filter_2(sK37),sK37),
inference(forward_subsumption_resolution,[],[f22371,f17227]) ).
fof(f22373,plain,
m2_lattice4(u1_struct_0(sK37),sK37),
inference(forward_demodulation,[],[f22372,f21871]) ).
fof(f22374,plain,
( v3_struct_0(sK37)
| ~ v10_lattices(sK37)
| ~ l3_lattices(sK37)
| v1_xboole_0(u1_struct_0(sK37))
| m2_nat_lat(k23_filter_2(sK37,u1_struct_0(sK37)),sK37) ),
inference(resolution,[],[f22373,f16948]) ).
fof(f22380,plain,
( ~ m2_nat_lat(k23_filter_2(sK37,u1_struct_0(sK37)),sK37)
| v1_xboole_0(u1_struct_0(sK37))
| sK35(sK37,u1_struct_0(sK37),k23_filter_2(sK37,u1_struct_0(sK37))) = k1_realset1(u2_lattices(sK37),u1_struct_0(sK37))
| v3_struct_0(sK37)
| ~ v10_lattices(sK37)
| ~ l3_lattices(sK37) ),
inference(resolution,[],[f22373,f21061]) ).
fof(f22381,plain,
( ~ m2_nat_lat(k23_filter_2(sK37,u1_struct_0(sK37)),sK37)
| v1_xboole_0(u1_struct_0(sK37))
| sK36(sK37,u1_struct_0(sK37),k23_filter_2(sK37,u1_struct_0(sK37))) = k1_realset1(u1_lattices(sK37),u1_struct_0(sK37))
| v3_struct_0(sK37)
| ~ v10_lattices(sK37)
| ~ l3_lattices(sK37) ),
inference(resolution,[],[f22373,f21062]) ).
fof(f22525,plain,
( $false
| spl526_17
| ~ spl526_22
| ~ spl526_30 ),
inference(unit_resulting_resolution,[],[f16904,f21918,f22013,f22122,f22127,f21970]) ).
fof(f22527,plain,
( spl526_17
| ~ spl526_22
| ~ spl526_30 ),
inference(avatar_contradiction_clause,[],[f22525]) ).
fof(f22537,plain,
( ~ m2_nat_lat(k23_filter_2(sK37,u1_struct_0(sK37)),sK37)
| v1_xboole_0(u1_struct_0(sK37))
| sK36(sK37,u1_struct_0(sK37),k23_filter_2(sK37,u1_struct_0(sK37))) = k1_realset1(u1_lattices(sK37),u1_struct_0(sK37))
| ~ v10_lattices(sK37)
| ~ l3_lattices(sK37) ),
inference(forward_subsumption_resolution,[],[f22381,f17229]) ).
fof(f22538,plain,
( ~ m2_nat_lat(k23_filter_2(sK37,u1_struct_0(sK37)),sK37)
| v1_xboole_0(u1_struct_0(sK37))
| sK35(sK37,u1_struct_0(sK37),k23_filter_2(sK37,u1_struct_0(sK37))) = k1_realset1(u2_lattices(sK37),u1_struct_0(sK37))
| ~ v10_lattices(sK37)
| ~ l3_lattices(sK37) ),
inference(forward_subsumption_resolution,[],[f22380,f17229]) ).
fof(f22543,plain,
( ~ v10_lattices(sK37)
| ~ l3_lattices(sK37)
| v1_xboole_0(u1_struct_0(sK37))
| m2_nat_lat(k23_filter_2(sK37,u1_struct_0(sK37)),sK37) ),
inference(forward_subsumption_resolution,[],[f22374,f17229]) ).
fof(f22562,plain,
( ~ m2_nat_lat(k23_filter_2(sK37,u1_struct_0(sK37)),sK37)
| v1_xboole_0(u1_struct_0(sK37))
| sK36(sK37,u1_struct_0(sK37),k23_filter_2(sK37,u1_struct_0(sK37))) = k1_realset1(u1_lattices(sK37),u1_struct_0(sK37))
| ~ l3_lattices(sK37) ),
inference(forward_subsumption_resolution,[],[f22537,f17228]) ).
fof(f22563,plain,
( ~ m2_nat_lat(k23_filter_2(sK37,u1_struct_0(sK37)),sK37)
| v1_xboole_0(u1_struct_0(sK37))
| sK35(sK37,u1_struct_0(sK37),k23_filter_2(sK37,u1_struct_0(sK37))) = k1_realset1(u2_lattices(sK37),u1_struct_0(sK37))
| ~ l3_lattices(sK37) ),
inference(forward_subsumption_resolution,[],[f22538,f17228]) ).
fof(f22568,plain,
( ~ l3_lattices(sK37)
| v1_xboole_0(u1_struct_0(sK37))
| m2_nat_lat(k23_filter_2(sK37,u1_struct_0(sK37)),sK37) ),
inference(forward_subsumption_resolution,[],[f22543,f17228]) ).
fof(f22575,plain,
( ~ m2_nat_lat(k23_filter_2(sK37,u1_struct_0(sK37)),sK37)
| v1_xboole_0(u1_struct_0(sK37))
| sK36(sK37,u1_struct_0(sK37),k23_filter_2(sK37,u1_struct_0(sK37))) = k1_realset1(u1_lattices(sK37),u1_struct_0(sK37)) ),
inference(forward_subsumption_resolution,[],[f22562,f17227]) ).
fof(f22576,plain,
( ~ m2_nat_lat(k23_filter_2(sK37,u1_struct_0(sK37)),sK37)
| v1_xboole_0(u1_struct_0(sK37))
| sK35(sK37,u1_struct_0(sK37),k23_filter_2(sK37,u1_struct_0(sK37))) = k1_realset1(u2_lattices(sK37),u1_struct_0(sK37)) ),
inference(forward_subsumption_resolution,[],[f22563,f17227]) ).
fof(f22581,plain,
( v1_xboole_0(u1_struct_0(sK37))
| m2_nat_lat(k23_filter_2(sK37,u1_struct_0(sK37)),sK37) ),
inference(forward_subsumption_resolution,[],[f22568,f17227]) ).
fof(f22588,plain,
( ~ m2_nat_lat(k8_filter_0(sK37,u1_struct_0(sK37)),sK37)
| v1_xboole_0(u1_struct_0(sK37))
| sK36(sK37,u1_struct_0(sK37),k23_filter_2(sK37,u1_struct_0(sK37))) = k1_realset1(u1_lattices(sK37),u1_struct_0(sK37)) ),
inference(forward_demodulation,[],[f22575,f21961]) ).
fof(f22589,plain,
( ~ m2_nat_lat(k8_filter_0(sK37,u1_struct_0(sK37)),sK37)
| v1_xboole_0(u1_struct_0(sK37))
| sK35(sK37,u1_struct_0(sK37),k23_filter_2(sK37,u1_struct_0(sK37))) = k1_realset1(u2_lattices(sK37),u1_struct_0(sK37)) ),
inference(forward_demodulation,[],[f22576,f21961]) ).
fof(f22594,plain,
( m2_nat_lat(k8_filter_0(sK37,u1_struct_0(sK37)),sK37)
| v1_xboole_0(u1_struct_0(sK37)) ),
inference(forward_demodulation,[],[f22581,f21961]) ).
fof(f22639,plain,
( u1_lattices(sK37) = sK36(sK37,u1_struct_0(sK37),k23_filter_2(sK37,u1_struct_0(sK37)))
| ~ m2_nat_lat(k8_filter_0(sK37,u1_struct_0(sK37)),sK37)
| v1_xboole_0(u1_struct_0(sK37)) ),
inference(forward_demodulation,[],[f22588,f22218]) ).
fof(f22640,plain,
( u2_lattices(sK37) = sK35(sK37,u1_struct_0(sK37),k23_filter_2(sK37,u1_struct_0(sK37)))
| ~ m2_nat_lat(k8_filter_0(sK37,u1_struct_0(sK37)),sK37)
| v1_xboole_0(u1_struct_0(sK37)) ),
inference(forward_demodulation,[],[f22589,f22217]) ).
fof(f22642,plain,
( spl526_22
| spl526_24 ),
inference(avatar_split_clause,[],[f22594,f21975,f21969]) ).
fof(f22643,plain,
( u1_lattices(sK37) = sK36(sK37,u1_struct_0(sK37),k8_filter_0(sK37,u1_struct_0(sK37)))
| ~ m2_nat_lat(k8_filter_0(sK37,u1_struct_0(sK37)),sK37)
| v1_xboole_0(u1_struct_0(sK37)) ),
inference(forward_demodulation,[],[f22639,f21961]) ).
fof(f22644,plain,
( u2_lattices(sK37) = sK35(sK37,u1_struct_0(sK37),k8_filter_0(sK37,u1_struct_0(sK37)))
| ~ m2_nat_lat(k8_filter_0(sK37,u1_struct_0(sK37)),sK37)
| v1_xboole_0(u1_struct_0(sK37)) ),
inference(forward_demodulation,[],[f22640,f21961]) ).
fof(f22646,definition,
( spl526_60
<=> u1_lattices(sK37) = sK36(sK37,u1_struct_0(sK37),k8_filter_0(sK37,u1_struct_0(sK37))) ),
introduced(definition,[new_symbols(definition,[spl526_60])],[avatar_definition]) ).
fof(f22647,plain,
( u1_lattices(sK37) = sK36(sK37,u1_struct_0(sK37),k8_filter_0(sK37,u1_struct_0(sK37)))
| ~ spl526_60 ),
inference(avatar_component_clause,[],[f22646]) ).
fof(f22648,plain,
( spl526_22
| ~ spl526_24
| spl526_60 ),
inference(avatar_split_clause,[],[f22643,f22646,f21975,f21969]) ).
fof(f22650,definition,
( spl526_61
<=> u2_lattices(sK37) = sK35(sK37,u1_struct_0(sK37),k8_filter_0(sK37,u1_struct_0(sK37))) ),
introduced(definition,[new_symbols(definition,[spl526_61])],[avatar_definition]) ).
fof(f22651,plain,
( u2_lattices(sK37) = sK35(sK37,u1_struct_0(sK37),k8_filter_0(sK37,u1_struct_0(sK37)))
| ~ spl526_61 ),
inference(avatar_component_clause,[],[f22650]) ).
fof(f22652,plain,
( spl526_22
| ~ spl526_24
| spl526_61 ),
inference(avatar_split_clause,[],[f22644,f22650,f21975,f21969]) ).
fof(f23855,plain,
( k8_filter_0(sK37,u1_struct_0(sK37)) = g3_lattices(u1_struct_0(sK37),u2_lattices(sK37),sK36(sK37,u1_struct_0(sK37),k8_filter_0(sK37,u1_struct_0(sK37))))
| ~ spl526_23
| ~ spl526_61 ),
inference(superposition,[],[f21973,f22651]) ).
fof(f23856,plain,
( k8_filter_0(sK37,u1_struct_0(sK37)) = g3_lattices(u1_struct_0(sK37),sK35(sK37,u1_struct_0(sK37),k8_filter_0(sK37,u1_struct_0(sK37))),u1_lattices(sK37))
| ~ spl526_23
| ~ spl526_60 ),
inference(superposition,[],[f21973,f22647]) ).
fof(f23857,plain,
( g3_lattices(u1_struct_0(sK37),u2_lattices(sK37),u1_lattices(sK37)) = k8_filter_0(sK37,u1_struct_0(sK37))
| ~ spl526_23
| ~ spl526_60
| ~ spl526_61 ),
inference(forward_demodulation,[],[f23856,f22651]) ).
fof(f23858,plain,
( g3_lattices(u1_struct_0(sK37),u2_lattices(sK37),u1_lattices(sK37)) = k8_filter_0(sK37,u1_struct_0(sK37))
| ~ spl526_23
| ~ spl526_60
| ~ spl526_61 ),
inference(forward_demodulation,[],[f23855,f22647]) ).
fof(f23859,plain,
( k1_lattice2(k1_lattice2(sK37)) = k8_filter_0(sK37,u1_struct_0(sK37))
| ~ spl526_23
| ~ spl526_60
| ~ spl526_61 ),
inference(forward_demodulation,[],[f23857,f21863]) ).
fof(f23860,plain,
( k1_lattice2(k1_lattice2(sK37)) = k8_filter_0(sK37,u1_struct_0(sK37))
| ~ spl526_23
| ~ spl526_60
| ~ spl526_61 ),
inference(forward_demodulation,[],[f23858,f21863]) ).
fof(f23863,plain,
( $false
| spl526_14
| ~ spl526_23
| ~ spl526_60
| ~ spl526_61 ),
inference(forward_subsumption_resolution,[],[f23860,f21962]) ).
fof(f23864,plain,
( spl526_14
| ~ spl526_23
| ~ spl526_60
| ~ spl526_61 ),
inference(avatar_contradiction_clause,[],[f23863]) ).
fof(f23865,plain,
( g3_lattices(u1_struct_0(sK37),u2_lattices(sK37),u1_lattices(sK37)) != k23_filter_2(sK37,u1_struct_0(sK37))
| spl526_13 ),
inference(forward_demodulation,[],[f21636,f21881]) ).
fof(f23866,plain,
( g3_lattices(u1_struct_0(sK37),u2_lattices(sK37),u1_lattices(sK37)) != k8_filter_0(sK37,u1_struct_0(sK37))
| spl526_13 ),
inference(forward_demodulation,[],[f23865,f21961]) ).
fof(f23867,plain,
( g3_lattices(u1_struct_0(sK37),u2_lattices(sK37),u1_lattices(sK37)) != k1_lattice2(k1_lattice2(sK37))
| spl526_13
| ~ spl526_23
| ~ spl526_60
| ~ spl526_61 ),
inference(forward_demodulation,[],[f23866,f23859]) ).
fof(f23868,plain,
( $false
| spl526_13
| ~ spl526_23
| ~ spl526_60
| ~ spl526_61 ),
inference(forward_subsumption_resolution,[],[f23867,f21863]) ).
fof(f23869,plain,
( spl526_13
| ~ spl526_23
| ~ spl526_60
| ~ spl526_61 ),
inference(avatar_contradiction_clause,[],[f23868]) ).
cnf(s8,plain,
( ~ spl526_13
| ~ spl526_14 ),
inference(sat_conversion,[],[f21640]) ).
cnf(s16,plain,
( spl526_22
| spl526_23
| ~ spl526_24 ),
inference(sat_conversion,[],[f21977]) ).
cnf(s18,plain,
~ spl526_17,
inference(sat_conversion,[],[f21998]) ).
cnf(s26,plain,
( spl526_17
| spl526_30 ),
inference(sat_conversion,[],[f22087]) ).
cnf(s42,plain,
( spl526_17
| ~ spl526_22
| ~ spl526_30 ),
inference(sat_conversion,[],[f22527]) ).
cnf(s59,plain,
( spl526_22
| spl526_24 ),
inference(sat_conversion,[],[f22642]) ).
cnf(s60,plain,
( spl526_22
| ~ spl526_24
| spl526_60 ),
inference(sat_conversion,[],[f22648]) ).
cnf(s61,plain,
( spl526_22
| ~ spl526_24
| spl526_61 ),
inference(sat_conversion,[],[f22652]) ).
cnf(s169,plain,
( spl526_14
| ~ spl526_23
| ~ spl526_60
| ~ spl526_61 ),
inference(sat_conversion,[],[f23864]) ).
cnf(s170,plain,
( spl526_13
| ~ spl526_23
| ~ spl526_60
| ~ spl526_61 ),
inference(sat_conversion,[],[f23869]) ).
cnf(s177,plain,
spl526_30,
inference(rat,[],[s26,s18]) ).
cnf(s182,plain,
~ spl526_22,
inference(rat,[],[s42,s18,s177]) ).
cnf(s185,plain,
spl526_24,
inference(rat,[],[s59,s182]) ).
cnf(s203,plain,
spl526_61,
inference(rat,[],[s61,s182,s185]) ).
cnf(s204,plain,
spl526_60,
inference(rat,[],[s60,s182,s185]) ).
cnf(s248,plain,
spl526_23,
inference(rat,[],[s16,s185,s182]) ).
cnf(s249,plain,
spl526_13,
inference(rat,[],[s170,s203,s204,s248]) ).
cnf(s250,plain,
spl526_14,
inference(rat,[],[s169,s203,s204,s248]) ).
cnf(s308,plain,
$false,
inference(rat,[],[s8,s250,s249]) ).
fof(f23870,plain,
$false,
inference(avatar_sat_refutation,[],[s308]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LAT332+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.09 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.23/0.48 % Computer : n002.cluster.edu
% 0.23/0.48 % Model : x86_64 x86_64
% 0.23/0.48 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.23/0.48 % Memory : 8046.5625MB
% 0.23/0.48 % OS : Linux 6.8.0-71-generic
% 0.23/0.48 % CPULimit : 300
% 0.23/0.48 % WCLimit : 300
% 0.23/0.48 % DateTime : Sun Sep 27 14:45:23 UTC 2026
% 0.23/0.49 % CPUTime :
% 0.23/0.49 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.26/0.55 Running first-order theorem proving
% 0.26/0.55 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 29.42/6.53 % (3593806)Detected formulas, will run a generic FOF schedule.
% 29.42/6.53 % (3593811)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=1051084836:i=141193_2986 on theBenchmark for (2986ds/141193Mi)
% 29.42/6.53 % (3593812)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=2329116802:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2986 on theBenchmark for (2986ds/134677Mi)
% 29.42/6.53 % (3593813)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=3985307590:i=141695:sd=1:nm=32:gsp=on:ss=included_2986 on theBenchmark for (2986ds/141695Mi)
% 29.42/6.53 % (3593815)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2718015012:i=119:av=off:ss=axioms_2986 on theBenchmark for (2986ds/119Mi)
% 29.42/6.53 % (3593814)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3274022259:i=109:sd=1:ins=1:gsp=on:ss=axioms_2986 on theBenchmark for (2986ds/109Mi)
% 29.42/6.53 % (3593817)dis-21_1_sil=8000:lcm=predicate:random_seed=2045075644:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2986 on theBenchmark for (2986ds/129Mi)
% 29.42/6.53 % (3593816)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3695809247:s2a=on:i=139:gtg=position_2986 on theBenchmark for (2986ds/139Mi)
% 29.42/6.53 % (3593814)Refutation not found, incomplete strategy
% 29.42/6.53 % (3593814)------------------------------
% 29.42/6.53 % (3593814)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.42/6.53 % (3593814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.42/6.53 % (3593814)CaDiCaL version: 2.1.3
% 29.42/6.53 % (3593814)Termination reason: Refutation not found, incomplete strategy
% 29.42/6.53 % (3593814)Time elapsed: 0.096 s
% 29.42/6.53 % (3593814)Peak memory usage: 107 MB
% 29.42/6.53 % (3593814)Instructions burned: 79 (million)
% 29.42/6.53 % (3593816)Instruction limit reached!
% 29.42/6.53 % (3593816)------------------------------
% 29.42/6.53 % (3593816)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.42/6.53 % (3593816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.42/6.53 % (3593816)CaDiCaL version: 2.1.3
% 29.42/6.53 % (3593816)Termination reason: Instruction limit
% 29.42/6.53 % (3593816)Termination phase: Property scanning
% 29.42/6.53 % (3593816)Time elapsed: 0.115 s
% 29.42/6.53 % (3593816)Peak memory usage: 102 MB
% 29.42/6.53 % (3593816)Instructions burned: 140 (million)
% 29.42/6.53 % (3593815)Instruction limit reached!
% 29.42/6.53 % (3593815)------------------------------
% 29.42/6.53 % (3593815)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.42/6.53 % (3593815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.42/6.53 % (3593815)CaDiCaL version: 2.1.3
% 29.42/6.53 % (3593815)Termination reason: Instruction limit
% 29.42/6.53 % (3593815)Termination phase: Property scanning
% 29.42/6.53 % (3593815)Time elapsed: 0.144 s
% 29.42/6.53 % (3593815)Peak memory usage: 105 MB
% 29.42/6.53 % (3593815)Instructions burned: 119 (million)
% 29.42/6.53 % (3593817)Instruction limit reached!
% 29.42/6.53 % (3593817)------------------------------
% 29.42/6.53 % (3593817)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.42/6.53 % (3593817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.42/6.53 % (3593817)CaDiCaL version: 2.1.3
% 29.42/6.53 % (3593817)Termination reason: Instruction limit
% 29.42/6.53 % (3593817)Termination phase: Preprocessing 1
% 29.42/6.53 % (3593817)Time elapsed: 0.148 s
% 29.42/6.53 % (3593817)Peak memory usage: 103 MB
% 29.42/6.53 % (3593817)Instructions burned: 129 (million)
% 29.42/6.53 % (3593825)lrs+10_1_sil=8000:sp=occurrence:random_seed=765439927:i=285:sd=3:ss=axioms:sgt=8_2982 on theBenchmark for (2982ds/285Mi)
% 29.42/6.53 % (3593826)lrs+10_1_sil=32000:urr=on:br=off:random_seed=362023559:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2982 on theBenchmark for (2982ds/157Mi)
% 29.42/6.53 % (3593827)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2567606270:i=325:sd=1:ss=axioms:sgt=32_2981 on theBenchmark for (2981ds/325Mi)
% 29.42/6.53 % (3593814)------------------------------
% 29.42/6.53 % (3593814)------------------------------
% 29.42/6.53 % (3593827)Refutation not found, incomplete strategy
% 29.42/6.53 % (3593827)------------------------------
% 29.42/6.53 % (3593827)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.11/6.66 % (3593827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.11/6.66 % (3593827)CaDiCaL version: 2.1.3
% 26.11/6.66 % (3593827)Termination reason: Refutation not found, incomplete strategy
% 26.11/6.66 % (3593827)Time elapsed: 0.099 s
% 26.11/6.66 % (3593827)Peak memory usage: 107 MB
% 26.11/6.66 % (3593827)Instructions burned: 76 (million)
% 26.11/6.66 % (3593826)Instruction limit reached!
% 26.11/6.66 % (3593826)------------------------------
% 26.11/6.66 % (3593826)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.11/6.66 % (3593826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.11/6.66 % (3593826)CaDiCaL version: 2.1.3
% 26.11/6.66 % (3593826)Termination reason: Instruction limit
% 26.11/6.66 % (3593826)Termination phase: Property scanning
% 26.11/6.66 % (3593826)Time elapsed: 0.131 s
% 26.11/6.66 % (3593826)Peak memory usage: 103 MB
% 26.11/6.66 % (3593826)Instructions burned: 158 (million)
% 26.11/6.66 % (3593825)Instruction limit reached!
% 26.11/6.66 % (3593825)------------------------------
% 26.11/6.66 % (3593825)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.11/6.66 % (3593825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.11/6.66 % (3593825)CaDiCaL version: 2.1.3
% 26.11/6.66 % (3593825)Termination reason: Instruction limit
% 26.11/6.66 % (3593825)Termination phase: Saturation
% 26.11/6.66 % (3593825)Time elapsed: 0.322 s
% 26.11/6.66 % (3593825)Peak memory usage: 110 MB
% 26.11/6.66 % (3593825)Instructions burned: 285 (million)
% 26.11/6.66 % (3593831)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=1932755554:s2a=on:i=248:s2at=1.23:gtg=position_2978 on theBenchmark for (2978ds/248Mi)
% 26.11/6.66 % (3593832)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3885962772:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2977 on theBenchmark for (2977ds/294Mi)
% 26.11/6.66 % (3593827)------------------------------
% 26.11/6.66 % (3593827)------------------------------
% 26.11/6.66 % (3593831)Instruction limit reached!
% 26.11/6.66 % (3593831)------------------------------
% 26.11/6.66 % (3593831)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.11/6.66 % (3593831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.11/6.66 % (3593831)CaDiCaL version: 2.1.3
% 26.11/6.66 % (3593831)Termination reason: Instruction limit
% 26.11/6.66 % (3593831)Termination phase: SInE selection
% 26.11/6.66 % (3593831)Time elapsed: 0.225 s
% 26.11/6.66 % (3593831)Peak memory usage: 103 MB
% 26.11/6.66 % (3593831)Instructions burned: 248 (million)
% 26.11/6.66 % (3593833)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3196697342:i=2350_2975 on theBenchmark for (2975ds/2350Mi)
% 26.11/6.66 % (3593832)Instruction limit reached!
% 26.11/6.66 % (3593832)------------------------------
% 26.11/6.66 % (3593832)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.11/6.66 % (3593832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.11/6.66 % (3593832)CaDiCaL version: 2.1.3
% 26.11/6.66 % (3593832)Termination reason: Instruction limit
% 26.11/6.66 % (3593832)Termination phase: Saturation
% 26.11/6.66 % (3593832)Time elapsed: 0.312 s
% 26.11/6.66 % (3593832)Peak memory usage: 110 MB
% 26.11/6.66 % (3593832)Instructions burned: 295 (million)
% 26.11/6.66 % (3593836)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2764207673:cts=off:i=113:fsr=off:ss=included:sgt=4_2973 on theBenchmark for (2973ds/113Mi)
% 26.11/6.66 % (3593837)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1300363330:i=127:av=off:fsr=off:sup=off_2972 on theBenchmark for (2972ds/127Mi)
% 26.11/6.66 % (3593836)Instruction limit reached!
% 26.11/6.66 % (3593836)------------------------------
% 26.11/6.66 % (3593836)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.11/6.66 % (3593836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.11/6.66 % (3593836)CaDiCaL version: 2.1.3
% 26.11/6.66 % (3593836)Termination reason: Instruction limit
% 26.11/6.66 % (3593836)Termination phase: Preprocessing 3
% 26.11/6.66 % (3593836)Time elapsed: 0.148 s
% 26.11/6.66 % (3593836)Peak memory usage: 105 MB
% 26.11/6.66 % (3593836)Instructions burned: 114 (million)
% 26.11/6.66 % (3593839)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1840297810:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2971 on theBenchmark for (2971ds/114Mi)
% 26.11/6.66 % (3593837)Instruction limit reached!
% 26.11/6.66 % (3593837)------------------------------
% 26.11/6.66 % (3593837)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.11/6.66 % (3593837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.11/6.66 % (3593837)CaDiCaL version: 2.1.3
% 26.11/6.66 % (3593837)Termination reason: Instruction limit
% 26.11/6.66 % (3593837)Termination phase: Preprocessing 2
% 26.11/6.66 % (3593837)Time elapsed: 0.169 s
% 26.11/6.66 % (3593837)Peak memory usage: 106 MB
% 26.11/6.66 % (3593837)Instructions burned: 127 (million)
% 26.11/6.66 % (3593839)Instruction limit reached!
% 26.11/6.66 % (3593839)------------------------------
% 26.11/6.66 % (3593839)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.11/6.66 % (3593839)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.11/6.66 % (3593839)CaDiCaL version: 2.1.3
% 26.11/6.66 % (3593839)Termination reason: Instruction limit
% 26.11/6.66 % (3593839)Termination phase: Property scanning
% 26.11/6.66 % (3593839)Time elapsed: 0.097 s
% 26.11/6.66 % (3593839)Peak memory usage: 103 MB
% 26.11/6.66 % (3593839)Instructions burned: 114 (million)
% 26.11/6.66 % (3593842)lrs+10_1_sil=8000:sp=occurrence:random_seed=3843482783:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2968 on theBenchmark for (2968ds/907Mi)
% 26.11/6.66 % (3593844)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=769636525:i=437:sd=1:aac=none:ss=included_2968 on theBenchmark for (2968ds/437Mi)
% 26.11/6.66 % (3593845)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=534593099:i=5202:ss=axioms:sgt=16_2967 on theBenchmark for (2967ds/5202Mi)
% 26.11/6.66 % (3593844)Refutation not found, incomplete strategy
% 26.11/6.66 % (3593844)------------------------------
% 26.11/6.66 % (3593844)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.11/6.66 % (3593844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.11/6.66 % (3593844)CaDiCaL version: 2.1.3
% 26.11/6.66 % (3593844)Termination reason: Refutation not found, incomplete strategy
% 26.11/6.66 % (3593844)Time elapsed: 0.215 s
% 26.11/6.66 % (3593844)Peak memory usage: 109 MB
% 26.11/6.66 % (3593844)Instructions burned: 190 (million)
% 26.11/6.66 % (3593844)------------------------------
% 26.11/6.66 % (3593844)------------------------------
% 26.11/6.66 % (3593842)Instruction limit reached!
% 26.11/6.66 % (3593842)------------------------------
% 26.11/6.66 % (3593842)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.11/6.66 % (3593842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.11/6.66 % (3593842)CaDiCaL version: 2.1.3
% 26.11/6.66 % (3593842)Termination reason: Instruction limit
% 26.11/6.66 % (3593842)Termination phase: Saturation
% 26.11/6.66 % (3593842)Time elapsed: 0.888 s
% 26.11/6.66 % (3593842)Peak memory usage: 121 MB
% 26.11/6.66 % (3593842)Instructions burned: 907 (million)
% 26.11/6.66 % (3593849)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=786907405:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2958 on theBenchmark for (2958ds/134Mi)
% 26.11/6.66 % (3593850)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=466794914:st=8:i=592:sd=3:ep=RST:ss=axioms_2956 on theBenchmark for (2956ds/592Mi)
% 26.11/6.66 % (3593849)Instruction limit reached!
% 26.11/6.66 % (3593849)------------------------------
% 26.11/6.66 % (3593849)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.11/6.66 % (3593849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.11/6.66 % (3593849)CaDiCaL version: 2.1.3
% 26.11/6.66 % (3593849)Termination reason: Instruction limit
% 26.11/6.66 % (3593849)Termination phase: Property scanning
% 26.11/6.66 % (3593849)Time elapsed: 0.160 s
% 26.11/6.66 % (3593849)Peak memory usage: 106 MB
% 26.11/6.66 % (3593849)Instructions burned: 135 (million)
% 26.11/6.66 % (3593812)First to succeed.
% 26.11/6.66 % (3593812)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3593806"
% 26.11/6.66 % (3593853)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2195485894:st=3:i=13193:sd=3:ss=axioms_2953 on theBenchmark for (2953ds/13193Mi)
% 26.11/6.66 % (3593833)Instruction limit reached!
% 26.11/6.66 % (3593833)------------------------------
% 26.11/6.66 % (3593833)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.11/6.66 % (3593833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.11/6.66 % (3593833)CaDiCaL version: 2.1.3
% 26.11/6.66 % (3593833)Termination reason: Instruction limit
% 26.11/6.66 % (3593833)Termination phase: Saturation
% 26.11/6.66 % (3593833)Time elapsed: 2.505 s
% 26.11/6.66 % (3593833)Peak memory usage: 239 MB
% 26.11/6.66 % (3593833)Instructions burned: 2350 (million)
% 26.11/6.66 % (3593850)Instruction limit reached!
% 26.11/6.66 % (3593850)------------------------------
% 26.11/6.66 % (3593850)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.11/6.66 % (3593850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.11/6.66 % (3593850)CaDiCaL version: 2.1.3
% 26.11/6.66 % (3593850)Termination reason: Instruction limit
% 26.11/6.66 % (3593850)Termination phase: Property scanning
% 26.11/6.66 % (3593850)Time elapsed: 0.640 s
% 26.11/6.66 % (3593850)Peak memory usage: 123 MB
% 26.11/6.66 % (3593850)Instructions burned: 592 (million)
% 26.11/6.66 % (3593812)Refutation found. Thanks to Tanya!
% 26.11/6.66 % SZS status Theorem for theBenchmark
% 26.11/6.66 % SZS output start Proof for theBenchmark
% See solution above
% 0.30/7.06 % (3593812)------------------------------
% 0.30/7.06 % (3593812)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.30/7.06 % (3593812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.30/7.06 % (3593812)CaDiCaL version: 2.1.3
% 0.30/7.06 % (3593812)Termination reason: Refutation
% 0.30/7.06 % (3593812)Time elapsed: 3.210 s
% 0.30/7.06 % (3593812)Peak memory usage: 194 MB
% 0.30/7.06 % (3593812)Instructions burned: 3014 (million)
% 0.30/7.06 % (3593812)------------------------------
% 0.30/7.06 % (3593812)------------------------------
% 0.30/7.06 % (3593806)Success in time 5.341 s
% 0.30/7.06 % Vampire exiting
%------------------------------------------------------------------------------