%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT312+2 : 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 : n013.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:48 AM UTC 2026
% Result : Theorem 19.38s 3.79s
% Output : Refutation 20.66s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 38
% Syntax : Number of formulae : 295 ( 52 unt; 16 def)
% Number of atoms : 1259 ( 171 equ)
% Maximal formula atoms : 16 ( 4 avg)
% Number of connectives : 1562 ( 598 ~; 738 |; 165 &)
% ( 17 <=>; 44 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 6 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 30 ( 28 usr; 11 prp; 0-3 aty)
% Number of functors : 24 ( 24 usr; 8 con; 0-3 aty)
% Number of variables : 284 ( 0 sgn 275 !; 9 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f38,axiom,
! [X0,X1] :
( X0 = X1
<=> ( r1_tarski(X0,X1)
& r1_tarski(X1,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d10_xboole_0) ).
fof(f1867,axiom,
! [X0,X1] :
( ( ~ v1_xboole_0(X0)
& m1_subset_1(X1,X0) )
=> m1_subset_1(k6_domain_1(X0,X1),k1_zfmisc_1(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k6_domain_1) ).
fof(f2455,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> m1_filter_0(u1_struct_0(X0),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t15_filter_0) ).
fof(f2473,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( ( ~ v1_xboole_0(X2)
& m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
=> ( X2 = k6_domain_1(u1_struct_0(X0),X1)
=> k3_filter_0(X0,X2) = k2_filter_0(X0,X1) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t30_filter_0) ).
fof(f2540,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_filter_0(X1,X0)
=> ( ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m1_filter_0) ).
fof(f2564,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(f2569,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(f2597,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(f2669,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(f2857,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_lattice4(X1,X0)
=> m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m2_lattice4) ).
fof(f2874,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(f2878,axiom,
! [X0,X1,X2] :
( ( ~ v1_xboole_0(X0)
& m1_subset_1(X1,k1_zfmisc_1(X0))
& m1_subset_1(X2,k1_zfmisc_1(X0)) )
=> ( r1_filter_2(X0,X1,X2)
<=> X1 = X2 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_r1_filter_2) ).
fof(f2882,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0)
& m1_subset_1(X1,u1_struct_0(X0)) )
=> k2_filter_2(X0,X1) = k2_filter_0(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k2_filter_2) ).
fof(f2884,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0)
& ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
=> k3_filter_2(X0,X1) = k3_filter_0(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k3_filter_2) ).
fof(f2909,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0)
& ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
=> m2_filter_2(k19_filter_2(X0,X1),X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k19_filter_2) ).
fof(f2937,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> k5_filter_2(X0,X1) = X1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d4_filter_2) ).
fof(f2943,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
=> k7_filter_2(X0,X1) = X1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d6_filter_2) ).
fof(f2957,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ( k18_filter_2(X0,X1) = k2_filter_2(k1_lattice2(X0),k5_filter_2(X0,X1))
& k18_filter_2(k1_lattice2(X0),k5_filter_2(X0,X1)) = k2_filter_2(X0,X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t30_filter_2) ).
fof(f2965,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( ( ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
=> ! [X2] :
( m2_filter_2(X2,X0)
=> ( X2 = k19_filter_2(X0,X1)
<=> ( r1_tarski(X1,X2)
& ! [X3] :
( m2_filter_2(X3,X0)
=> ( r1_tarski(X1,X3)
=> r1_tarski(X2,X3) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d11_filter_2) ).
fof(f2967,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( ( ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
=> ! [X2] :
( ( ~ v1_xboole_0(X2)
& m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(k1_lattice2(X0)))) )
=> ( k3_filter_2(k1_lattice2(X0),k7_filter_2(X0,X1)) = k19_filter_2(X0,X1)
& k3_filter_2(X0,X1) = k19_filter_2(k1_lattice2(X0),k7_filter_2(X0,X1))
& k3_filter_2(X0,k8_filter_2(X0,X2)) = k19_filter_2(k1_lattice2(X0),X2)
& k3_filter_2(k1_lattice2(X0),X2) = k19_filter_2(X0,k8_filter_2(X0,X2)) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t37_filter_2) ).
fof(f2968,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m2_filter_2(X1,X0)
=> r1_filter_2(u1_struct_0(X0),k19_filter_2(X0,X1),X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t38_filter_2) ).
fof(f2971,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( ( ~ v1_xboole_0(X2)
& m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
=> ( r1_filter_2(u1_struct_0(X0),X2,k6_domain_1(u1_struct_0(X0),X1))
=> r1_filter_2(u1_struct_0(X0),k19_filter_2(X0,X2),k18_filter_2(X0,X1)) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t41_filter_2) ).
fof(f2972,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( ( ~ v1_xboole_0(X2)
& m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
=> ( r1_filter_2(u1_struct_0(X0),X2,k6_domain_1(u1_struct_0(X0),X1))
=> r1_filter_2(u1_struct_0(X0),k19_filter_2(X0,X2),k18_filter_2(X0,X1)) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f2971]) ).
fof(f4770,plain,
! [X0,X1] :
( m1_subset_1(k6_domain_1(X0,X1),k1_zfmisc_1(X0))
| v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0) ),
inference(ennf_transformation,[],[f1867]) ).
fof(f4771,plain,
! [X0,X1] :
( m1_subset_1(k6_domain_1(X0,X1),k1_zfmisc_1(X0))
| v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0) ),
inference(flattening,[],[f4770]) ).
fof(f5468,plain,
! [X0] :
( m1_filter_0(u1_struct_0(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2455]) ).
fof(f5469,plain,
! [X0] :
( m1_filter_0(u1_struct_0(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f5468]) ).
fof(f5494,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( k3_filter_0(X0,X2) = k2_filter_0(X0,X1)
| k6_domain_1(u1_struct_0(X0),X1) != X2
| v1_xboole_0(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2473]) ).
fof(f5495,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( k3_filter_0(X0,X2) = k2_filter_0(X0,X1)
| k6_domain_1(u1_struct_0(X0),X1) != X2
| v1_xboole_0(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f5494]) ).
fof(f5612,plain,
! [X0] :
( ! [X1] :
( ( ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2540]) ).
fof(f5613,plain,
! [X0] :
( ! [X1] :
( ( ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f5612]) ).
fof(f5660,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2564]) ).
fof(f5661,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f5660]) ).
fof(f5670,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,[],[f2569]) ).
fof(f5671,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,[],[f5670]) ).
fof(f5711,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,[],[f2597]) ).
fof(f5712,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,[],[f5711]) ).
fof(f5847,plain,
! [X0] :
( ( v3_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) )
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2669]) ).
fof(f6026,plain,
! [X0] :
( ! [X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m2_lattice4(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2857]) ).
fof(f6027,plain,
! [X0] :
( ! [X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m2_lattice4(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f6026]) ).
fof(f6060,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,[],[f2874]) ).
fof(f6061,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,[],[f6060]) ).
fof(f6068,plain,
! [X0,X1,X2] :
( ( r1_filter_2(X0,X1,X2)
<=> X1 = X2 )
| v1_xboole_0(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f2878]) ).
fof(f6069,plain,
! [X0,X1,X2] :
( ( r1_filter_2(X0,X1,X2)
<=> X1 = X2 )
| v1_xboole_0(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(flattening,[],[f6068]) ).
fof(f6076,plain,
! [X0,X1] :
( k2_filter_2(X0,X1) = k2_filter_0(X0,X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f2882]) ).
fof(f6077,plain,
! [X0,X1] :
( k2_filter_2(X0,X1) = k2_filter_0(X0,X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(flattening,[],[f6076]) ).
fof(f6080,plain,
! [X0,X1] :
( k3_filter_2(X0,X1) = k3_filter_0(X0,X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ),
inference(ennf_transformation,[],[f2884]) ).
fof(f6081,plain,
! [X0,X1] :
( k3_filter_2(X0,X1) = k3_filter_0(X0,X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ),
inference(flattening,[],[f6080]) ).
fof(f6130,plain,
! [X0,X1] :
( m2_filter_2(k19_filter_2(X0,X1),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ),
inference(ennf_transformation,[],[f2909]) ).
fof(f6131,plain,
! [X0,X1] :
( m2_filter_2(k19_filter_2(X0,X1),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ),
inference(flattening,[],[f6130]) ).
fof(f6183,plain,
! [X0] :
( ! [X1] :
( k5_filter_2(X0,X1) = X1
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2937]) ).
fof(f6184,plain,
! [X0] :
( ! [X1] :
( k5_filter_2(X0,X1) = X1
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f6183]) ).
fof(f6195,plain,
! [X0] :
( ! [X1] :
( k7_filter_2(X0,X1) = X1
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2943]) ).
fof(f6196,plain,
! [X0] :
( ! [X1] :
( k7_filter_2(X0,X1) = X1
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f6195]) ).
fof(f6223,plain,
! [X0] :
( ! [X1] :
( ( k18_filter_2(X0,X1) = k2_filter_2(k1_lattice2(X0),k5_filter_2(X0,X1))
& k18_filter_2(k1_lattice2(X0),k5_filter_2(X0,X1)) = k2_filter_2(X0,X1) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2957]) ).
fof(f6224,plain,
! [X0] :
( ! [X1] :
( ( k18_filter_2(X0,X1) = k2_filter_2(k1_lattice2(X0),k5_filter_2(X0,X1))
& k18_filter_2(k1_lattice2(X0),k5_filter_2(X0,X1)) = k2_filter_2(X0,X1) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f6223]) ).
fof(f6239,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( X2 = k19_filter_2(X0,X1)
<=> ( r1_tarski(X1,X2)
& ! [X3] :
( r1_tarski(X2,X3)
| ~ r1_tarski(X1,X3)
| ~ m2_filter_2(X3,X0) ) ) )
| ~ m2_filter_2(X2,X0) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2965]) ).
fof(f6240,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( X2 = k19_filter_2(X0,X1)
<=> ( r1_tarski(X1,X2)
& ! [X3] :
( r1_tarski(X2,X3)
| ~ r1_tarski(X1,X3)
| ~ m2_filter_2(X3,X0) ) ) )
| ~ m2_filter_2(X2,X0) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f6239]) ).
fof(f6243,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( k3_filter_2(k1_lattice2(X0),k7_filter_2(X0,X1)) = k19_filter_2(X0,X1)
& k3_filter_2(X0,X1) = k19_filter_2(k1_lattice2(X0),k7_filter_2(X0,X1))
& k3_filter_2(X0,k8_filter_2(X0,X2)) = k19_filter_2(k1_lattice2(X0),X2)
& k3_filter_2(k1_lattice2(X0),X2) = k19_filter_2(X0,k8_filter_2(X0,X2)) )
| v1_xboole_0(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(k1_lattice2(X0)))) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2967]) ).
fof(f6244,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( k3_filter_2(k1_lattice2(X0),k7_filter_2(X0,X1)) = k19_filter_2(X0,X1)
& k3_filter_2(X0,X1) = k19_filter_2(k1_lattice2(X0),k7_filter_2(X0,X1))
& k3_filter_2(X0,k8_filter_2(X0,X2)) = k19_filter_2(k1_lattice2(X0),X2)
& k3_filter_2(k1_lattice2(X0),X2) = k19_filter_2(X0,k8_filter_2(X0,X2)) )
| v1_xboole_0(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(k1_lattice2(X0)))) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f6243]) ).
fof(f6245,plain,
! [X0] :
( ! [X1] :
( r1_filter_2(u1_struct_0(X0),k19_filter_2(X0,X1),X1)
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f2968]) ).
fof(f6246,plain,
! [X0] :
( ! [X1] :
( r1_filter_2(u1_struct_0(X0),k19_filter_2(X0,X1),X1)
| ~ m2_filter_2(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f6245]) ).
fof(f6251,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ~ r1_filter_2(u1_struct_0(X0),k19_filter_2(X0,X2),k18_filter_2(X0,X1))
& r1_filter_2(u1_struct_0(X0),X2,k6_domain_1(u1_struct_0(X0),X1))
& ~ v1_xboole_0(X2)
& m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
& m1_subset_1(X1,u1_struct_0(X0)) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(ennf_transformation,[],[f2972]) ).
fof(f6252,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ~ r1_filter_2(u1_struct_0(X0),k19_filter_2(X0,X2),k18_filter_2(X0,X1))
& r1_filter_2(u1_struct_0(X0),X2,k6_domain_1(u1_struct_0(X0),X1))
& ~ v1_xboole_0(X2)
& m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0))) )
& m1_subset_1(X1,u1_struct_0(X0)) )
& ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) ),
inference(flattening,[],[f6251]) ).
fof(f6427,definition,
! [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)) )
| ~ sP112(X0) ),
introduced(definition,[new_symbols(definition,[sP112])],[predicate_definition_introduction]) ).
fof(f6428,plain,
! [X0] :
( sP112(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(definition_folding,[],[f5671,f6427]) ).
fof(f6497,plain,
! [X0,X1] :
( ( X0 = X1
| ~ r1_tarski(X0,X1)
| ~ r1_tarski(X1,X0) )
& ( ( r1_tarski(X0,X1)
& r1_tarski(X1,X0) )
| X0 != X1 ) ),
inference(nnf_transformation,[],[f38]) ).
fof(f6498,plain,
! [X0,X1] :
( ( X0 = X1
| ~ r1_tarski(X0,X1)
| ~ r1_tarski(X1,X0) )
& ( ( r1_tarski(X0,X1)
& r1_tarski(X1,X0) )
| X0 != X1 ) ),
inference(flattening,[],[f6497]) ).
fof(f7829,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)) )
| ~ sP112(X0) ),
inference(nnf_transformation,[],[f6427]) ).
fof(f7957,plain,
! [X0,X1,X2] :
( ( ( r1_filter_2(X0,X1,X2)
| X1 != X2 )
& ( X1 = X2
| ~ r1_filter_2(X0,X1,X2) ) )
| v1_xboole_0(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(nnf_transformation,[],[f6069]) ).
fof(f7992,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( X2 = k19_filter_2(X0,X1)
| ~ r1_tarski(X1,X2)
| ? [X3] :
( ~ r1_tarski(X2,X3)
& r1_tarski(X1,X3)
& m2_filter_2(X3,X0) ) )
& ( ( r1_tarski(X1,X2)
& ! [X3] :
( r1_tarski(X2,X3)
| ~ r1_tarski(X1,X3)
| ~ m2_filter_2(X3,X0) ) )
| k19_filter_2(X0,X1) != X2 ) )
| ~ m2_filter_2(X2,X0) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f6240]) ).
fof(f7993,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( X2 = k19_filter_2(X0,X1)
| ~ r1_tarski(X1,X2)
| ? [X3] :
( ~ r1_tarski(X2,X3)
& r1_tarski(X1,X3)
& m2_filter_2(X3,X0) ) )
& ( ( r1_tarski(X1,X2)
& ! [X3] :
( r1_tarski(X2,X3)
| ~ r1_tarski(X1,X3)
| ~ m2_filter_2(X3,X0) ) )
| k19_filter_2(X0,X1) != X2 ) )
| ~ m2_filter_2(X2,X0) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f7992]) ).
fof(f7994,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( X2 = k19_filter_2(X0,X1)
| ~ r1_tarski(X1,X2)
| ? [X3] :
( ~ r1_tarski(X2,X3)
& r1_tarski(X1,X3)
& m2_filter_2(X3,X0) ) )
& ( ( r1_tarski(X1,X2)
& ! [X4] :
( r1_tarski(X2,X4)
| ~ r1_tarski(X1,X4)
| ~ m2_filter_2(X4,X0) ) )
| k19_filter_2(X0,X1) != X2 ) )
| ~ m2_filter_2(X2,X0) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(rectify,[],[f7993]) ).
fof(f7995,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( X2 = k19_filter_2(X0,X1)
| ~ r1_tarski(X1,X2)
| ( ~ r1_tarski(X2,sK1070(X0,X1,X2))
& r1_tarski(X1,sK1070(X0,X1,X2))
& m2_filter_2(sK1070(X0,X1,X2),X0) ) )
& ( ( r1_tarski(X1,X2)
& ! [X4] :
( r1_tarski(X2,X4)
| ~ r1_tarski(X1,X4)
| ~ m2_filter_2(X4,X0) ) )
| k19_filter_2(X0,X1) != X2 ) )
| ~ m2_filter_2(X2,X0) )
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1070]),skolemize(X3,sK1070(X0,X1,X2))],[f7994]) ).
fof(f7996,plain,
( ~ r1_filter_2(u1_struct_0(sK1071),k19_filter_2(sK1071,sK1073),k18_filter_2(sK1071,sK1072))
& r1_filter_2(u1_struct_0(sK1071),sK1073,k6_domain_1(u1_struct_0(sK1071),sK1072))
& ~ v1_xboole_0(sK1073)
& m1_subset_1(sK1073,k1_zfmisc_1(u1_struct_0(sK1071)))
& m1_subset_1(sK1072,u1_struct_0(sK1071))
& ~ v3_struct_0(sK1071)
& v10_lattices(sK1071)
& l3_lattices(sK1071) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1071,sK1072,sK1073]),skolemize(X0,sK1071),skolemize(X1,sK1072),skolemize(X2,sK1073)],[f6252]) ).
fof(f8077,plain,
! [X0,X1] :
( r1_tarski(X1,X0)
| X0 != X1 ),
inference(cnf_transformation,[],[f6498]) ).
fof(f10912,plain,
! [X0,X1] :
( m1_subset_1(k6_domain_1(X0,X1),k1_zfmisc_1(X0))
| v1_xboole_0(X0)
| ~ m1_subset_1(X1,X0) ),
inference(cnf_transformation,[],[f4771]) ).
fof(f12478,plain,
! [X0] :
( m1_filter_0(u1_struct_0(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f5469]) ).
fof(f12507,plain,
! [X2,X0,X1] :
( k2_filter_0(X0,X1) = k3_filter_0(X0,X2)
| k6_domain_1(u1_struct_0(X0),X1) != X2
| v1_xboole_0(X2)
| ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f5495]) ).
fof(f12644,plain,
! [X0,X1] :
( ~ m1_filter_0(X1,X0)
| ~ v1_xboole_0(X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f5613]) ).
fof(f12692,plain,
! [X0] :
( ~ v3_struct_0(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f5661]) ).
fof(f12713,plain,
! [X0] :
( v10_lattices(k1_lattice2(X0))
| ~ sP112(X0) ),
inference(cnf_transformation,[],[f7829]) ).
fof(f12722,plain,
! [X0] :
( ~ v10_lattices(X0)
| v3_struct_0(X0)
| sP112(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f6428]) ).
fof(f12839,plain,
! [X0] :
( ~ l3_lattices(X0)
| v3_struct_0(X0)
| u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0)) ),
inference(cnf_transformation,[],[f5712]) ).
fof(f12960,plain,
! [X0] :
( l3_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f5847]) ).
fof(f13222,plain,
! [X0,X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f6027]) ).
fof(f13255,plain,
! [X0,X1] :
( ~ m2_filter_2(X1,X0)
| m2_lattice4(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f6061]) ).
fof(f13256,plain,
! [X0,X1] :
( ~ m2_filter_2(X1,X0)
| ~ v1_xboole_0(X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f6061]) ).
fof(f13260,plain,
! [X2,X0,X1] :
( ~ r1_filter_2(X0,X1,X2)
| X1 = X2
| v1_xboole_0(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(cnf_transformation,[],[f7957]) ).
fof(f13265,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| k2_filter_0(X0,X1) = k2_filter_2(X0,X1) ),
inference(cnf_transformation,[],[f6077]) ).
fof(f13267,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| v1_xboole_0(X1)
| k3_filter_0(X0,X1) = k3_filter_2(X0,X1) ),
inference(cnf_transformation,[],[f6081]) ).
fof(f13294,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| v1_xboole_0(X1)
| m2_filter_2(k19_filter_2(X0,X1),X0) ),
inference(cnf_transformation,[],[f6131]) ).
fof(f13354,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,u1_struct_0(X0))
| k5_filter_2(X0,X1) = X1
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f6184]) ).
fof(f13368,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| k7_filter_2(X0,X1) = X1
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f6196]) ).
fof(f13398,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,u1_struct_0(X0))
| k18_filter_2(X0,X1) = k2_filter_2(k1_lattice2(X0),k5_filter_2(X0,X1))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f6224]) ).
fof(f13421,plain,
! [X2,X0,X1] :
( r1_tarski(X1,sK1070(X0,X1,X2))
| ~ r1_tarski(X1,X2)
| k19_filter_2(X0,X1) = X2
| ~ m2_filter_2(X2,X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f7995]) ).
fof(f13422,plain,
! [X2,X0,X1] :
( ~ r1_tarski(X2,sK1070(X0,X1,X2))
| ~ r1_tarski(X1,X2)
| k19_filter_2(X0,X1) = X2
| ~ m2_filter_2(X2,X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f7995]) ).
fof(f13428,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,k1_zfmisc_1(u1_struct_0(k1_lattice2(X0))))
| v1_xboole_0(X2)
| k19_filter_2(X0,X1) = k3_filter_2(k1_lattice2(X0),k7_filter_2(X0,X1))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f6244]) ).
fof(f13429,plain,
! [X0,X1] :
( r1_filter_2(u1_struct_0(X0),k19_filter_2(X0,X1),X1)
| ~ m2_filter_2(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f6246]) ).
fof(f13433,plain,
l3_lattices(sK1071),
inference(cnf_transformation,[],[f7996]) ).
fof(f13434,plain,
v10_lattices(sK1071),
inference(cnf_transformation,[],[f7996]) ).
fof(f13435,plain,
~ v3_struct_0(sK1071),
inference(cnf_transformation,[],[f7996]) ).
fof(f13436,plain,
m1_subset_1(sK1072,u1_struct_0(sK1071)),
inference(cnf_transformation,[],[f7996]) ).
fof(f13437,plain,
m1_subset_1(sK1073,k1_zfmisc_1(u1_struct_0(sK1071))),
inference(cnf_transformation,[],[f7996]) ).
fof(f13438,plain,
~ v1_xboole_0(sK1073),
inference(cnf_transformation,[],[f7996]) ).
fof(f13439,plain,
r1_filter_2(u1_struct_0(sK1071),sK1073,k6_domain_1(u1_struct_0(sK1071),sK1072)),
inference(cnf_transformation,[],[f7996]) ).
fof(f13440,plain,
~ r1_filter_2(u1_struct_0(sK1071),k19_filter_2(sK1071,sK1073),k18_filter_2(sK1071,sK1072)),
inference(cnf_transformation,[],[f7996]) ).
fof(f14810,plain,
! [X1] : r1_tarski(X1,X1),
inference(equality_resolution,[],[f8077]) ).
fof(f15283,plain,
! [X0,X1] :
( ~ m1_subset_1(k6_domain_1(u1_struct_0(X0),X1),k1_zfmisc_1(u1_struct_0(X0)))
| v1_xboole_0(k6_domain_1(u1_struct_0(X0),X1))
| k2_filter_0(X0,X1) = k3_filter_0(X0,k6_domain_1(u1_struct_0(X0),X1))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(equality_resolution,[],[f12507]) ).
fof(f15364,definition,
sF1074 = u1_struct_0(sK1071),
introduced(definition,[new_symbols(definition,[sF1074])],[function_definition]) ).
fof(f15365,plain,
u1_struct_0(sK1071) = sF1074,
inference(reorient_equations,[],[f15364]) ).
fof(f15366,definition,
sF1075 = k19_filter_2(sK1071,sK1073),
introduced(definition,[new_symbols(definition,[sF1075])],[function_definition]) ).
fof(f15367,plain,
k19_filter_2(sK1071,sK1073) = sF1075,
inference(reorient_equations,[],[f15366]) ).
fof(f15368,definition,
sF1076 = k18_filter_2(sK1071,sK1072),
introduced(definition,[new_symbols(definition,[sF1076])],[function_definition]) ).
fof(f15369,plain,
k18_filter_2(sK1071,sK1072) = sF1076,
inference(reorient_equations,[],[f15368]) ).
fof(f15370,plain,
~ r1_filter_2(sF1074,sF1075,sF1076),
inference(definition_folding,[],[f13440,f15369,f15367,f15365]) ).
fof(f15371,definition,
sF1077 = k6_domain_1(sF1074,sK1072),
introduced(definition,[new_symbols(definition,[sF1077])],[function_definition]) ).
fof(f15372,plain,
k6_domain_1(sF1074,sK1072) = sF1077,
inference(reorient_equations,[],[f15371]) ).
fof(f15373,plain,
r1_filter_2(sF1074,sK1073,sF1077),
inference(definition_folding,[],[f13439,f15372,f15365,f15365]) ).
fof(f15374,definition,
sF1078 = k1_zfmisc_1(sF1074),
introduced(definition,[new_symbols(definition,[sF1078])],[function_definition]) ).
fof(f15375,plain,
k1_zfmisc_1(sF1074) = sF1078,
inference(reorient_equations,[],[f15374]) ).
fof(f15376,plain,
m1_subset_1(sK1073,sF1078),
inference(definition_folding,[],[f13437,f15375,f15365]) ).
fof(f15377,plain,
m1_subset_1(sK1072,sF1074),
inference(definition_folding,[],[f13436,f15365]) ).
fof(f17930,plain,
( m1_subset_1(sF1077,k1_zfmisc_1(sF1074))
| v1_xboole_0(sF1074)
| ~ m1_subset_1(sK1072,sF1074) ),
inference(superposition,[],[f10912,f15372]) ).
fof(f17940,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF1074))
| v3_struct_0(sK1071)
| ~ v10_lattices(sK1071)
| ~ l3_lattices(sK1071)
| v1_xboole_0(X0)
| m2_filter_2(k19_filter_2(sK1071,X0),sK1071) ),
inference(superposition,[],[f13294,f15365]) ).
fof(f17941,plain,
! [X0] :
( r1_filter_2(sF1074,k19_filter_2(sK1071,X0),X0)
| ~ m2_filter_2(X0,sK1071)
| v3_struct_0(sK1071)
| ~ v10_lattices(sK1071)
| ~ l3_lattices(sK1071) ),
inference(superposition,[],[f13429,f15365]) ).
fof(f17942,plain,
! [X0] :
( r1_filter_2(sF1074,k19_filter_2(sK1071,X0),X0)
| ~ m2_filter_2(X0,sK1071)
| ~ v10_lattices(sK1071)
| ~ l3_lattices(sK1071) ),
inference(forward_subsumption_resolution,[],[f17941,f13435]) ).
fof(f17943,plain,
! [X0] :
( r1_filter_2(sF1074,k19_filter_2(sK1071,X0),X0)
| ~ m2_filter_2(X0,sK1071)
| ~ l3_lattices(sK1071) ),
inference(forward_subsumption_resolution,[],[f17942,f13434]) ).
fof(f17944,plain,
! [X0] :
( r1_filter_2(sF1074,k19_filter_2(sK1071,X0),X0)
| ~ m2_filter_2(X0,sK1071) ),
inference(forward_subsumption_resolution,[],[f17943,f13433]) ).
fof(f17950,plain,
! [X0] :
( m1_subset_1(k6_domain_1(sF1074,X0),sF1078)
| v1_xboole_0(sF1074)
| ~ m1_subset_1(X0,sF1074) ),
inference(superposition,[],[f10912,f15375]) ).
fof(f17952,plain,
( sK1073 = sF1077
| v1_xboole_0(sF1074)
| ~ m1_subset_1(sK1073,k1_zfmisc_1(sF1074))
| ~ m1_subset_1(sF1077,k1_zfmisc_1(sF1074)) ),
inference(resolution,[],[f13260,f15373]) ).
fof(f17962,plain,
( v3_struct_0(sK1071)
| u1_struct_0(sK1071) = u1_struct_0(k1_lattice2(sK1071)) ),
inference(resolution,[],[f12839,f13433]) ).
fof(f17963,plain,
u1_struct_0(sK1071) = u1_struct_0(k1_lattice2(sK1071)),
inference(forward_subsumption_resolution,[],[f17962,f13435]) ).
fof(f17964,plain,
sF1074 = u1_struct_0(k1_lattice2(sK1071)),
inference(forward_demodulation,[],[f17963,f15365]) ).
fof(f17966,plain,
! [X0] :
( ~ m1_subset_1(k6_domain_1(sF1074,X0),k1_zfmisc_1(sF1074))
| v1_xboole_0(k6_domain_1(sF1074,X0))
| k2_filter_0(k1_lattice2(sK1071),X0) = k3_filter_0(k1_lattice2(sK1071),k6_domain_1(sF1074,X0))
| ~ m1_subset_1(X0,sF1074)
| v3_struct_0(k1_lattice2(sK1071))
| ~ v10_lattices(k1_lattice2(sK1071))
| ~ l3_lattices(k1_lattice2(sK1071)) ),
inference(superposition,[],[f15283,f17964]) ).
fof(f17970,definition,
( spl1079_343
<=> l3_lattices(k1_lattice2(sK1071)) ),
introduced(definition,[new_symbols(definition,[spl1079_343])],[avatar_definition]) ).
fof(f17971,plain,
( l3_lattices(k1_lattice2(sK1071))
| ~ spl1079_343 ),
inference(avatar_component_clause,[],[f17970]) ).
fof(f17972,plain,
( ~ l3_lattices(k1_lattice2(sK1071))
| spl1079_343 ),
inference(avatar_component_clause,[],[f17970]) ).
fof(f17974,definition,
( spl1079_344
<=> v10_lattices(k1_lattice2(sK1071)) ),
introduced(definition,[new_symbols(definition,[spl1079_344])],[avatar_definition]) ).
fof(f17975,plain,
( v10_lattices(k1_lattice2(sK1071))
| ~ spl1079_344 ),
inference(avatar_component_clause,[],[f17974]) ).
fof(f17976,plain,
( ~ v10_lattices(k1_lattice2(sK1071))
| spl1079_344 ),
inference(avatar_component_clause,[],[f17974]) ).
fof(f17978,definition,
( spl1079_345
<=> v3_struct_0(k1_lattice2(sK1071)) ),
introduced(definition,[new_symbols(definition,[spl1079_345])],[avatar_definition]) ).
fof(f17979,plain,
( ~ v3_struct_0(k1_lattice2(sK1071))
| spl1079_345 ),
inference(avatar_component_clause,[],[f17978]) ).
fof(f17980,plain,
( v3_struct_0(k1_lattice2(sK1071))
| ~ spl1079_345 ),
inference(avatar_component_clause,[],[f17978]) ).
fof(f18005,plain,
! [X0] :
( ~ m1_subset_1(X0,sF1074)
| k18_filter_2(sK1071,X0) = k2_filter_2(k1_lattice2(sK1071),k5_filter_2(sK1071,X0))
| v3_struct_0(sK1071)
| ~ v10_lattices(sK1071)
| ~ l3_lattices(sK1071) ),
inference(superposition,[],[f13398,f15365]) ).
fof(f18007,plain,
! [X0] :
( ~ m1_subset_1(X0,sF1074)
| k18_filter_2(sK1071,X0) = k2_filter_2(k1_lattice2(sK1071),k5_filter_2(sK1071,X0))
| ~ v10_lattices(sK1071)
| ~ l3_lattices(sK1071) ),
inference(forward_subsumption_resolution,[],[f18005,f13435]) ).
fof(f18008,plain,
! [X0] :
( ~ m1_subset_1(X0,sF1074)
| k18_filter_2(sK1071,X0) = k2_filter_2(k1_lattice2(sK1071),k5_filter_2(sK1071,X0))
| ~ l3_lattices(sK1071) ),
inference(forward_subsumption_resolution,[],[f18007,f13434]) ).
fof(f18009,plain,
! [X0] :
( ~ m1_subset_1(X0,sF1074)
| k18_filter_2(sK1071,X0) = k2_filter_2(k1_lattice2(sK1071),k5_filter_2(sK1071,X0)) ),
inference(forward_subsumption_resolution,[],[f18008,f13433]) ).
fof(f18010,plain,
k18_filter_2(sK1071,sK1072) = k2_filter_2(k1_lattice2(sK1071),k5_filter_2(sK1071,sK1072)),
inference(resolution,[],[f18009,f15377]) ).
fof(f18011,plain,
sF1076 = k2_filter_2(k1_lattice2(sK1071),k5_filter_2(sK1071,sK1072)),
inference(forward_demodulation,[],[f18010,f15369]) ).
fof(f18092,plain,
( m1_filter_0(sF1074,sK1071)
| v3_struct_0(sK1071)
| ~ v10_lattices(sK1071)
| ~ l3_lattices(sK1071) ),
inference(superposition,[],[f12478,f15365]) ).
fof(f18094,plain,
( m1_filter_0(sF1074,sK1071)
| ~ v10_lattices(sK1071)
| ~ l3_lattices(sK1071) ),
inference(forward_subsumption_resolution,[],[f18092,f13435]) ).
fof(f18096,plain,
( m1_filter_0(sF1074,sK1071)
| ~ l3_lattices(sK1071) ),
inference(forward_subsumption_resolution,[],[f18094,f13434]) ).
fof(f18098,plain,
m1_filter_0(sF1074,sK1071),
inference(forward_subsumption_resolution,[],[f18096,f13433]) ).
fof(f18112,plain,
! [X0,X1] :
( ~ r1_tarski(X0,X0)
| k19_filter_2(X1,X0) = X0
| ~ m2_filter_2(X0,X1)
| v1_xboole_0(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(X1)))
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1)
| ~ r1_tarski(X0,X0)
| k19_filter_2(X1,X0) = X0
| ~ m2_filter_2(X0,X1)
| v1_xboole_0(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(X1)))
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) ),
inference(resolution,[],[f13421,f13422]) ).
fof(f18113,plain,
! [X0,X1] :
( ~ r1_tarski(X0,X0)
| k19_filter_2(X1,X0) = X0
| ~ m2_filter_2(X0,X1)
| v1_xboole_0(X0)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(X1)))
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) ),
inference(duplicate_literal_removal,[],[f18112]) ).
fof(f18114,plain,
! [X0,X1] :
( ~ r1_tarski(X0,X0)
| k19_filter_2(X1,X0) = X0
| ~ m2_filter_2(X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(X1)))
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) ),
inference(forward_subsumption_resolution,[],[f18113,f13256]) ).
fof(f18115,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(X1)))
| ~ m2_filter_2(X0,X1)
| k19_filter_2(X1,X0) = X0
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) ),
inference(forward_subsumption_resolution,[],[f18114,f14810]) ).
fof(f18116,plain,
! [X0,X1] :
( ~ m2_filter_2(X0,X1)
| k19_filter_2(X1,X0) = X0
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1)
| ~ m2_lattice4(X0,X1)
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) ),
inference(resolution,[],[f18115,f13222]) ).
fof(f18122,plain,
! [X0,X1] :
( ~ m2_filter_2(X0,X1)
| k19_filter_2(X1,X0) = X0
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1)
| ~ m2_lattice4(X0,X1) ),
inference(duplicate_literal_removal,[],[f18116]) ).
fof(f18124,plain,
! [X0,X1] :
( ~ m2_filter_2(X0,X1)
| k19_filter_2(X1,X0) = X0
| v3_struct_0(X1)
| ~ v10_lattices(X1)
| ~ l3_lattices(X1) ),
inference(forward_subsumption_resolution,[],[f18122,f13255]) ).
fof(f18169,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF1074))
| v3_struct_0(k1_lattice2(sK1071))
| ~ v10_lattices(k1_lattice2(sK1071))
| ~ l3_lattices(k1_lattice2(sK1071))
| v1_xboole_0(X0)
| k3_filter_0(k1_lattice2(sK1071),X0) = k3_filter_2(k1_lattice2(sK1071),X0) ),
inference(superposition,[],[f13267,f17964]) ).
fof(f18184,definition,
( spl1079_356
<=> m2_filter_2(sF1075,sK1071) ),
introduced(definition,[new_symbols(definition,[spl1079_356])],[avatar_definition]) ).
fof(f18185,plain,
( m2_filter_2(sF1075,sK1071)
| ~ spl1079_356 ),
inference(avatar_component_clause,[],[f18184]) ).
fof(f18186,plain,
( ~ m2_filter_2(sF1075,sK1071)
| spl1079_356 ),
inference(avatar_component_clause,[],[f18184]) ).
fof(f18203,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF1074))
| k7_filter_2(sK1071,X0) = X0
| v3_struct_0(sK1071)
| ~ v10_lattices(sK1071)
| ~ l3_lattices(sK1071) ),
inference(superposition,[],[f13368,f15365]) ).
fof(f18207,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF1074))
| k7_filter_2(sK1071,X0) = X0
| ~ v10_lattices(sK1071)
| ~ l3_lattices(sK1071) ),
inference(forward_subsumption_resolution,[],[f18203,f13435]) ).
fof(f18208,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF1074))
| k7_filter_2(sK1071,X0) = X0
| ~ l3_lattices(sK1071) ),
inference(forward_subsumption_resolution,[],[f18207,f13434]) ).
fof(f18209,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF1074))
| k7_filter_2(sK1071,X0) = X0 ),
inference(forward_subsumption_resolution,[],[f18208,f13433]) ).
fof(f18210,plain,
! [X0] :
( ~ m1_subset_1(X0,sF1078)
| k7_filter_2(sK1071,X0) = X0 ),
inference(forward_demodulation,[],[f18209,f15375]) ).
fof(f18211,plain,
sK1073 = k7_filter_2(sK1071,sK1073),
inference(resolution,[],[f18210,f15376]) ).
fof(f18233,definition,
( spl1079_361
<=> m1_subset_1(sF1077,sF1078) ),
introduced(definition,[new_symbols(definition,[spl1079_361])],[avatar_definition]) ).
fof(f18234,plain,
( m1_subset_1(sF1077,sF1078)
| ~ spl1079_361 ),
inference(avatar_component_clause,[],[f18233]) ).
fof(f18235,plain,
( ~ m1_subset_1(sF1077,sF1078)
| spl1079_361 ),
inference(avatar_component_clause,[],[f18233]) ).
fof(f18290,plain,
( ~ l3_lattices(sK1071)
| spl1079_343 ),
inference(resolution,[],[f12960,f17972]) ).
fof(f18292,plain,
( $false
| spl1079_343 ),
inference(forward_subsumption_resolution,[],[f18290,f13433]) ).
fof(f18293,plain,
spl1079_343,
inference(avatar_contradiction_clause,[],[f18292]) ).
fof(f18301,plain,
( v3_struct_0(sK1071)
| ~ l3_lattices(sK1071)
| ~ spl1079_345 ),
inference(resolution,[],[f17980,f12692]) ).
fof(f18302,plain,
( ~ l3_lattices(sK1071)
| ~ spl1079_345 ),
inference(forward_subsumption_resolution,[],[f18301,f13435]) ).
fof(f18303,plain,
( $false
| ~ spl1079_345 ),
inference(forward_subsumption_resolution,[],[f18302,f13433]) ).
fof(f18304,plain,
~ spl1079_345,
inference(avatar_contradiction_clause,[],[f18303]) ).
fof(f18366,plain,
! [X0] :
( ~ m1_subset_1(X0,sF1074)
| v3_struct_0(k1_lattice2(sK1071))
| ~ v10_lattices(k1_lattice2(sK1071))
| ~ l3_lattices(k1_lattice2(sK1071))
| k2_filter_0(k1_lattice2(sK1071),X0) = k2_filter_2(k1_lattice2(sK1071),X0) ),
inference(superposition,[],[f13265,f17964]) ).
fof(f18381,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF1074))
| v1_xboole_0(X0)
| k19_filter_2(sK1071,X1) = k3_filter_2(k1_lattice2(sK1071),k7_filter_2(sK1071,X1))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK1071)))
| v3_struct_0(sK1071)
| ~ v10_lattices(sK1071)
| ~ l3_lattices(sK1071) ),
inference(superposition,[],[f13428,f17964]) ).
fof(f18385,plain,
( ~ v1_xboole_0(sF1074)
| v3_struct_0(sK1071)
| ~ v10_lattices(sK1071)
| ~ l3_lattices(sK1071) ),
inference(resolution,[],[f12644,f18098]) ).
fof(f18397,plain,
( m1_subset_1(sF1077,k1_zfmisc_1(sF1074))
| v1_xboole_0(sF1074) ),
inference(forward_subsumption_resolution,[],[f17930,f15377]) ).
fof(f18398,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF1074))
| ~ v10_lattices(sK1071)
| ~ l3_lattices(sK1071)
| v1_xboole_0(X0)
| m2_filter_2(k19_filter_2(sK1071,X0),sK1071) ),
inference(forward_subsumption_resolution,[],[f17940,f13435]) ).
fof(f18402,definition,
( spl1079_367
<=> v1_xboole_0(sF1074) ),
introduced(definition,[new_symbols(definition,[spl1079_367])],[avatar_definition]) ).
fof(f18403,plain,
( ~ v1_xboole_0(sF1074)
| spl1079_367 ),
inference(avatar_component_clause,[],[f18402]) ).
fof(f18406,definition,
( spl1079_368
<=> ! [X0] :
( m1_subset_1(k6_domain_1(sF1074,X0),sF1078)
| ~ m1_subset_1(X0,sF1074) ) ),
introduced(definition,[new_symbols(definition,[spl1079_368])],[avatar_definition]) ).
fof(f18407,plain,
( ! [X0] :
( m1_subset_1(k6_domain_1(sF1074,X0),sF1078)
| ~ m1_subset_1(X0,sF1074) )
| ~ spl1079_368 ),
inference(avatar_component_clause,[],[f18406]) ).
fof(f18408,plain,
( spl1079_367
| spl1079_368 ),
inference(avatar_split_clause,[],[f17950,f18406,f18402]) ).
fof(f18414,plain,
( ~ m1_subset_1(sK1073,sF1078)
| sK1073 = sF1077
| v1_xboole_0(sF1074)
| ~ m1_subset_1(sF1077,k1_zfmisc_1(sF1074)) ),
inference(forward_demodulation,[],[f17952,f15375]) ).
fof(f18447,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF1074))
| v1_xboole_0(X0)
| k19_filter_2(sK1071,X1) = k3_filter_2(k1_lattice2(sK1071),k7_filter_2(sK1071,X1))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK1071)))
| ~ v10_lattices(sK1071)
| ~ l3_lattices(sK1071) ),
inference(forward_subsumption_resolution,[],[f18381,f13435]) ).
fof(f18450,plain,
( ~ v1_xboole_0(sF1074)
| ~ v10_lattices(sK1071)
| ~ l3_lattices(sK1071) ),
inference(forward_subsumption_resolution,[],[f18385,f13435]) ).
fof(f18452,plain,
( m1_subset_1(sF1077,sF1078)
| v1_xboole_0(sF1074) ),
inference(forward_demodulation,[],[f18397,f15375]) ).
fof(f18453,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF1074))
| ~ l3_lattices(sK1071)
| v1_xboole_0(X0)
| m2_filter_2(k19_filter_2(sK1071,X0),sK1071) ),
inference(forward_subsumption_resolution,[],[f18398,f13434]) ).
fof(f18457,plain,
( sK1073 = sF1077
| v1_xboole_0(sF1074)
| ~ m1_subset_1(sF1077,k1_zfmisc_1(sF1074)) ),
inference(forward_subsumption_resolution,[],[f18414,f15376]) ).
fof(f18482,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF1074))
| v1_xboole_0(X0)
| k19_filter_2(sK1071,X1) = k3_filter_2(k1_lattice2(sK1071),k7_filter_2(sK1071,X1))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK1071)))
| ~ l3_lattices(sK1071) ),
inference(forward_subsumption_resolution,[],[f18447,f13434]) ).
fof(f18485,plain,
( ~ v1_xboole_0(sF1074)
| ~ l3_lattices(sK1071) ),
inference(forward_subsumption_resolution,[],[f18450,f13434]) ).
fof(f18487,plain,
( v1_xboole_0(sF1074)
| spl1079_361 ),
inference(forward_subsumption_resolution,[],[f18452,f18235]) ).
fof(f18488,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF1074))
| v1_xboole_0(X0)
| m2_filter_2(k19_filter_2(sK1071,X0),sK1071) ),
inference(forward_subsumption_resolution,[],[f18453,f13433]) ).
fof(f18494,plain,
( ~ m1_subset_1(sF1077,sF1078)
| sK1073 = sF1077
| v1_xboole_0(sF1074) ),
inference(forward_demodulation,[],[f18457,f15375]) ).
fof(f18510,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF1074))
| v1_xboole_0(X0)
| k19_filter_2(sK1071,X1) = k3_filter_2(k1_lattice2(sK1071),k7_filter_2(sK1071,X1))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK1071))) ),
inference(forward_subsumption_resolution,[],[f18482,f13433]) ).
fof(f18512,plain,
~ v1_xboole_0(sF1074),
inference(forward_subsumption_resolution,[],[f18485,f13433]) ).
fof(f18513,plain,
( spl1079_367
| spl1079_361 ),
inference(avatar_split_clause,[],[f18487,f18233,f18402]) ).
fof(f18514,plain,
! [X0] :
( m2_filter_2(k19_filter_2(sK1071,X0),sK1071)
| v1_xboole_0(X0)
| ~ m1_subset_1(X0,sF1078) ),
inference(forward_demodulation,[],[f18488,f15375]) ).
fof(f18523,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,sF1078)
| v1_xboole_0(X0)
| k19_filter_2(sK1071,X1) = k3_filter_2(k1_lattice2(sK1071),k7_filter_2(sK1071,X1))
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(sK1071))) ),
inference(forward_demodulation,[],[f18510,f15375]) ).
fof(f18524,plain,
~ spl1079_367,
inference(avatar_split_clause,[],[f18512,f18402]) ).
fof(f18528,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(sF1074))
| ~ m1_subset_1(X0,sF1078)
| v1_xboole_0(X0)
| k19_filter_2(sK1071,X1) = k3_filter_2(k1_lattice2(sK1071),k7_filter_2(sK1071,X1))
| v1_xboole_0(X1) ),
inference(forward_demodulation,[],[f18523,f15365]) ).
fof(f18532,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,sF1078)
| ~ m1_subset_1(X0,sF1078)
| v1_xboole_0(X0)
| k19_filter_2(sK1071,X1) = k3_filter_2(k1_lattice2(sK1071),k7_filter_2(sK1071,X1))
| v1_xboole_0(X1) ),
inference(forward_demodulation,[],[f18528,f15375]) ).
fof(f18537,definition,
( spl1079_379
<=> ! [X0] :
( ~ m1_subset_1(X0,sF1078)
| v1_xboole_0(X0) ) ),
introduced(definition,[new_symbols(definition,[spl1079_379])],[avatar_definition]) ).
fof(f18538,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF1078)
| v1_xboole_0(X0) )
| ~ spl1079_379 ),
inference(avatar_component_clause,[],[f18537]) ).
fof(f18540,definition,
( spl1079_380
<=> ! [X1] :
( ~ m1_subset_1(X1,sF1078)
| v1_xboole_0(X1)
| k19_filter_2(sK1071,X1) = k3_filter_2(k1_lattice2(sK1071),k7_filter_2(sK1071,X1)) ) ),
introduced(definition,[new_symbols(definition,[spl1079_380])],[avatar_definition]) ).
fof(f18541,plain,
( ! [X1] :
( ~ m1_subset_1(X1,sF1078)
| v1_xboole_0(X1)
| k19_filter_2(sK1071,X1) = k3_filter_2(k1_lattice2(sK1071),k7_filter_2(sK1071,X1)) )
| ~ spl1079_380 ),
inference(avatar_component_clause,[],[f18540]) ).
fof(f18542,plain,
( spl1079_379
| spl1079_380 ),
inference(avatar_split_clause,[],[f18532,f18540,f18537]) ).
fof(f18547,plain,
( sK1073 = sF1077
| v1_xboole_0(sF1074)
| ~ spl1079_361 ),
inference(forward_subsumption_resolution,[],[f18494,f18234]) ).
fof(f18550,plain,
( sK1073 = sF1077
| ~ spl1079_361
| spl1079_367 ),
inference(forward_subsumption_resolution,[],[f18547,f18403]) ).
fof(f18553,plain,
( v1_xboole_0(sK1073)
| ~ spl1079_379 ),
inference(resolution,[],[f18538,f15376]) ).
fof(f18557,plain,
( $false
| ~ spl1079_379 ),
inference(forward_subsumption_resolution,[],[f18553,f13438]) ).
fof(f18558,plain,
~ spl1079_379,
inference(avatar_contradiction_clause,[],[f18557]) ).
fof(f18573,plain,
( m2_filter_2(sF1075,sK1071)
| v1_xboole_0(sK1073)
| ~ m1_subset_1(sK1073,sF1078) ),
inference(superposition,[],[f18514,f15367]) ).
fof(f18578,plain,
( v1_xboole_0(sK1073)
| ~ m1_subset_1(sK1073,sF1078)
| spl1079_356 ),
inference(forward_subsumption_resolution,[],[f18573,f18186]) ).
fof(f18583,plain,
( ~ m1_subset_1(sK1073,sF1078)
| spl1079_356 ),
inference(forward_subsumption_resolution,[],[f18578,f13438]) ).
fof(f18588,plain,
( $false
| spl1079_356 ),
inference(forward_subsumption_resolution,[],[f18583,f15376]) ).
fof(f18589,plain,
spl1079_356,
inference(avatar_contradiction_clause,[],[f18588]) ).
fof(f18662,plain,
( v1_xboole_0(sK1073)
| k19_filter_2(sK1071,sK1073) = k3_filter_2(k1_lattice2(sK1071),k7_filter_2(sK1071,sK1073))
| ~ spl1079_380 ),
inference(resolution,[],[f18541,f15376]) ).
fof(f18665,plain,
( k19_filter_2(sK1071,sK1073) = k3_filter_2(k1_lattice2(sK1071),k7_filter_2(sK1071,sK1073))
| ~ spl1079_380 ),
inference(forward_subsumption_resolution,[],[f18662,f13438]) ).
fof(f18667,plain,
( k19_filter_2(sK1071,sK1073) = k3_filter_2(k1_lattice2(sK1071),sK1073)
| ~ spl1079_380 ),
inference(forward_demodulation,[],[f18665,f18211]) ).
fof(f18669,plain,
( sF1075 = k3_filter_2(k1_lattice2(sK1071),sK1073)
| ~ spl1079_380 ),
inference(forward_demodulation,[],[f18667,f15367]) ).
fof(f18673,plain,
( sF1075 = k19_filter_2(sK1071,sF1075)
| v3_struct_0(sK1071)
| ~ v10_lattices(sK1071)
| ~ l3_lattices(sK1071)
| ~ spl1079_356 ),
inference(resolution,[],[f18185,f18124]) ).
fof(f18674,plain,
( sF1075 = k19_filter_2(sK1071,sF1075)
| ~ v10_lattices(sK1071)
| ~ l3_lattices(sK1071)
| ~ spl1079_356 ),
inference(forward_subsumption_resolution,[],[f18673,f13435]) ).
fof(f18677,definition,
( spl1079_382
<=> sF1075 = k19_filter_2(sK1071,sF1075) ),
introduced(definition,[new_symbols(definition,[spl1079_382])],[avatar_definition]) ).
fof(f18679,plain,
( sF1075 = k19_filter_2(sK1071,sF1075)
| ~ spl1079_382 ),
inference(avatar_component_clause,[],[f18677]) ).
fof(f18685,plain,
( sF1075 = k19_filter_2(sK1071,sF1075)
| ~ l3_lattices(sK1071)
| ~ spl1079_356 ),
inference(forward_subsumption_resolution,[],[f18674,f13434]) ).
fof(f18687,plain,
( sF1075 = k19_filter_2(sK1071,sF1075)
| ~ spl1079_356 ),
inference(forward_subsumption_resolution,[],[f18685,f13433]) ).
fof(f18689,plain,
( spl1079_382
| ~ spl1079_356 ),
inference(avatar_split_clause,[],[f18687,f18184,f18677]) ).
fof(f18743,plain,
( r1_filter_2(sF1074,sF1075,sF1075)
| ~ m2_filter_2(sF1075,sK1071)
| ~ spl1079_382 ),
inference(superposition,[],[f17944,f18679]) ).
fof(f18751,plain,
( r1_filter_2(sF1074,sF1075,sF1075)
| ~ spl1079_356
| ~ spl1079_382 ),
inference(forward_subsumption_resolution,[],[f18743,f18185]) ).
fof(f18834,plain,
( v3_struct_0(sK1071)
| sP112(sK1071)
| ~ l3_lattices(sK1071) ),
inference(resolution,[],[f12722,f13434]) ).
fof(f18835,plain,
( sP112(sK1071)
| ~ l3_lattices(sK1071) ),
inference(forward_subsumption_resolution,[],[f18834,f13435]) ).
fof(f18836,plain,
sP112(sK1071),
inference(forward_subsumption_resolution,[],[f18835,f13433]) ).
fof(f19080,plain,
! [X0] :
( ~ m1_subset_1(X0,sF1074)
| k5_filter_2(sK1071,X0) = X0
| v3_struct_0(sK1071)
| ~ v10_lattices(sK1071)
| ~ l3_lattices(sK1071) ),
inference(superposition,[],[f13354,f15365]) ).
fof(f19082,plain,
! [X0] :
( ~ m1_subset_1(X0,sF1074)
| k5_filter_2(sK1071,X0) = X0
| ~ v10_lattices(sK1071)
| ~ l3_lattices(sK1071) ),
inference(forward_subsumption_resolution,[],[f19080,f13435]) ).
fof(f19083,plain,
! [X0] :
( ~ m1_subset_1(X0,sF1074)
| k5_filter_2(sK1071,X0) = X0
| ~ l3_lattices(sK1071) ),
inference(forward_subsumption_resolution,[],[f19082,f13434]) ).
fof(f19084,plain,
! [X0] :
( ~ m1_subset_1(X0,sF1074)
| k5_filter_2(sK1071,X0) = X0 ),
inference(forward_subsumption_resolution,[],[f19083,f13433]) ).
fof(f19085,plain,
sK1072 = k5_filter_2(sK1071,sK1072),
inference(resolution,[],[f19084,f15377]) ).
fof(f19086,plain,
sF1076 = k2_filter_2(k1_lattice2(sK1071),sK1072),
inference(superposition,[],[f18011,f19085]) ).
fof(f20072,plain,
( ~ sP112(sK1071)
| spl1079_344 ),
inference(resolution,[],[f12713,f17976]) ).
fof(f20081,plain,
( $false
| spl1079_344 ),
inference(forward_subsumption_resolution,[],[f20072,f18836]) ).
fof(f20082,plain,
spl1079_344,
inference(avatar_contradiction_clause,[],[f20081]) ).
fof(f20090,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF1074))
| ~ v10_lattices(k1_lattice2(sK1071))
| ~ l3_lattices(k1_lattice2(sK1071))
| v1_xboole_0(X0)
| k3_filter_0(k1_lattice2(sK1071),X0) = k3_filter_2(k1_lattice2(sK1071),X0) )
| spl1079_345 ),
inference(forward_subsumption_resolution,[],[f18169,f17979]) ).
fof(f20094,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF1074)
| ~ v10_lattices(k1_lattice2(sK1071))
| ~ l3_lattices(k1_lattice2(sK1071))
| k2_filter_0(k1_lattice2(sK1071),X0) = k2_filter_2(k1_lattice2(sK1071),X0) )
| spl1079_345 ),
inference(forward_subsumption_resolution,[],[f18366,f17979]) ).
fof(f20096,plain,
( ! [X0] :
( ~ m1_subset_1(k6_domain_1(sF1074,X0),k1_zfmisc_1(sF1074))
| v1_xboole_0(k6_domain_1(sF1074,X0))
| k2_filter_0(k1_lattice2(sK1071),X0) = k3_filter_0(k1_lattice2(sK1071),k6_domain_1(sF1074,X0))
| ~ m1_subset_1(X0,sF1074)
| ~ v10_lattices(k1_lattice2(sK1071))
| ~ l3_lattices(k1_lattice2(sK1071)) )
| spl1079_345 ),
inference(forward_subsumption_resolution,[],[f17966,f17979]) ).
fof(f20121,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF1074))
| ~ l3_lattices(k1_lattice2(sK1071))
| v1_xboole_0(X0)
| k3_filter_0(k1_lattice2(sK1071),X0) = k3_filter_2(k1_lattice2(sK1071),X0) )
| ~ spl1079_344
| spl1079_345 ),
inference(forward_subsumption_resolution,[],[f20090,f17975]) ).
fof(f20125,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF1074)
| ~ l3_lattices(k1_lattice2(sK1071))
| k2_filter_0(k1_lattice2(sK1071),X0) = k2_filter_2(k1_lattice2(sK1071),X0) )
| ~ spl1079_344
| spl1079_345 ),
inference(forward_subsumption_resolution,[],[f20094,f17975]) ).
fof(f20127,plain,
( ! [X0] :
( ~ m1_subset_1(k6_domain_1(sF1074,X0),k1_zfmisc_1(sF1074))
| v1_xboole_0(k6_domain_1(sF1074,X0))
| k2_filter_0(k1_lattice2(sK1071),X0) = k3_filter_0(k1_lattice2(sK1071),k6_domain_1(sF1074,X0))
| ~ m1_subset_1(X0,sF1074)
| ~ l3_lattices(k1_lattice2(sK1071)) )
| ~ spl1079_344
| spl1079_345 ),
inference(forward_subsumption_resolution,[],[f20096,f17975]) ).
fof(f20152,plain,
( ! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(sF1074))
| v1_xboole_0(X0)
| k3_filter_0(k1_lattice2(sK1071),X0) = k3_filter_2(k1_lattice2(sK1071),X0) )
| ~ spl1079_343
| ~ spl1079_344
| spl1079_345 ),
inference(forward_subsumption_resolution,[],[f20121,f17971]) ).
fof(f20156,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF1074)
| k2_filter_0(k1_lattice2(sK1071),X0) = k2_filter_2(k1_lattice2(sK1071),X0) )
| ~ spl1079_343
| ~ spl1079_344
| spl1079_345 ),
inference(forward_subsumption_resolution,[],[f20125,f17971]) ).
fof(f20158,plain,
( ! [X0] :
( ~ m1_subset_1(k6_domain_1(sF1074,X0),k1_zfmisc_1(sF1074))
| v1_xboole_0(k6_domain_1(sF1074,X0))
| k2_filter_0(k1_lattice2(sK1071),X0) = k3_filter_0(k1_lattice2(sK1071),k6_domain_1(sF1074,X0))
| ~ m1_subset_1(X0,sF1074) )
| ~ spl1079_343
| ~ spl1079_344
| spl1079_345 ),
inference(forward_subsumption_resolution,[],[f20127,f17971]) ).
fof(f20198,plain,
( ! [X0] :
( ~ m1_subset_1(X0,sF1078)
| v1_xboole_0(X0)
| k3_filter_0(k1_lattice2(sK1071),X0) = k3_filter_2(k1_lattice2(sK1071),X0) )
| ~ spl1079_343
| ~ spl1079_344
| spl1079_345 ),
inference(forward_demodulation,[],[f20152,f15375]) ).
fof(f20201,plain,
( ! [X0] :
( ~ m1_subset_1(k6_domain_1(sF1074,X0),sF1078)
| v1_xboole_0(k6_domain_1(sF1074,X0))
| k2_filter_0(k1_lattice2(sK1071),X0) = k3_filter_0(k1_lattice2(sK1071),k6_domain_1(sF1074,X0))
| ~ m1_subset_1(X0,sF1074) )
| ~ spl1079_343
| ~ spl1079_344
| spl1079_345 ),
inference(forward_demodulation,[],[f20158,f15375]) ).
fof(f20232,plain,
( ! [X0] :
( v1_xboole_0(k6_domain_1(sF1074,X0))
| k2_filter_0(k1_lattice2(sK1071),X0) = k3_filter_0(k1_lattice2(sK1071),k6_domain_1(sF1074,X0))
| ~ m1_subset_1(X0,sF1074) )
| ~ spl1079_343
| ~ spl1079_344
| spl1079_345
| ~ spl1079_368 ),
inference(forward_subsumption_resolution,[],[f20201,f18407]) ).
fof(f20258,plain,
( v1_xboole_0(sK1073)
| k3_filter_2(k1_lattice2(sK1071),sK1073) = k3_filter_0(k1_lattice2(sK1071),sK1073)
| ~ spl1079_343
| ~ spl1079_344
| spl1079_345 ),
inference(resolution,[],[f20198,f15376]) ).
fof(f20267,plain,
( k3_filter_2(k1_lattice2(sK1071),sK1073) = k3_filter_0(k1_lattice2(sK1071),sK1073)
| ~ spl1079_343
| ~ spl1079_344
| spl1079_345 ),
inference(forward_subsumption_resolution,[],[f20258,f13438]) ).
fof(f20274,plain,
( sF1075 = k3_filter_0(k1_lattice2(sK1071),sK1073)
| ~ spl1079_343
| ~ spl1079_344
| spl1079_345
| ~ spl1079_380 ),
inference(forward_demodulation,[],[f20267,f18669]) ).
fof(f20313,plain,
( v1_xboole_0(sF1077)
| k3_filter_0(k1_lattice2(sK1071),sF1077) = k2_filter_0(k1_lattice2(sK1071),sK1072)
| ~ m1_subset_1(sK1072,sF1074)
| ~ spl1079_343
| ~ spl1079_344
| spl1079_345
| ~ spl1079_368 ),
inference(superposition,[],[f20232,f15372]) ).
fof(f20314,plain,
( v1_xboole_0(sF1077)
| k3_filter_0(k1_lattice2(sK1071),sF1077) = k2_filter_0(k1_lattice2(sK1071),sK1072)
| ~ spl1079_343
| ~ spl1079_344
| spl1079_345
| ~ spl1079_368 ),
inference(forward_subsumption_resolution,[],[f20313,f15377]) ).
fof(f20315,plain,
( v1_xboole_0(sK1073)
| k3_filter_0(k1_lattice2(sK1071),sF1077) = k2_filter_0(k1_lattice2(sK1071),sK1072)
| ~ spl1079_343
| ~ spl1079_344
| spl1079_345
| ~ spl1079_361
| spl1079_367
| ~ spl1079_368 ),
inference(forward_demodulation,[],[f20314,f18550]) ).
fof(f20316,plain,
( k3_filter_0(k1_lattice2(sK1071),sF1077) = k2_filter_0(k1_lattice2(sK1071),sK1072)
| ~ spl1079_343
| ~ spl1079_344
| spl1079_345
| ~ spl1079_361
| spl1079_367
| ~ spl1079_368 ),
inference(forward_subsumption_resolution,[],[f20315,f13438]) ).
fof(f20317,plain,
( k3_filter_0(k1_lattice2(sK1071),sK1073) = k2_filter_0(k1_lattice2(sK1071),sK1072)
| ~ spl1079_343
| ~ spl1079_344
| spl1079_345
| ~ spl1079_361
| spl1079_367
| ~ spl1079_368 ),
inference(forward_demodulation,[],[f20316,f18550]) ).
fof(f20318,plain,
( sF1075 = k2_filter_0(k1_lattice2(sK1071),sK1072)
| ~ spl1079_343
| ~ spl1079_344
| spl1079_345
| ~ spl1079_361
| spl1079_367
| ~ spl1079_368
| ~ spl1079_380 ),
inference(forward_demodulation,[],[f20317,f20274]) ).
fof(f20514,plain,
( k2_filter_2(k1_lattice2(sK1071),sK1072) = k2_filter_0(k1_lattice2(sK1071),sK1072)
| ~ spl1079_343
| ~ spl1079_344
| spl1079_345 ),
inference(resolution,[],[f20156,f15377]) ).
fof(f20515,plain,
( sF1075 = k2_filter_2(k1_lattice2(sK1071),sK1072)
| ~ spl1079_343
| ~ spl1079_344
| spl1079_345
| ~ spl1079_361
| spl1079_367
| ~ spl1079_368
| ~ spl1079_380 ),
inference(forward_demodulation,[],[f20514,f20318]) ).
fof(f20516,plain,
( sF1075 = sF1076
| ~ spl1079_343
| ~ spl1079_344
| spl1079_345
| ~ spl1079_361
| spl1079_367
| ~ spl1079_368
| ~ spl1079_380 ),
inference(forward_demodulation,[],[f20515,f19086]) ).
fof(f20517,plain,
( ~ r1_filter_2(sF1074,sF1075,sF1075)
| ~ spl1079_343
| ~ spl1079_344
| spl1079_345
| ~ spl1079_361
| spl1079_367
| ~ spl1079_368
| ~ spl1079_380 ),
inference(superposition,[],[f15370,f20516]) ).
fof(f20542,plain,
( $false
| ~ spl1079_343
| ~ spl1079_344
| spl1079_345
| ~ spl1079_356
| ~ spl1079_361
| spl1079_367
| ~ spl1079_368
| ~ spl1079_380
| ~ spl1079_382 ),
inference(forward_subsumption_resolution,[],[f20517,f18751]) ).
fof(f20543,plain,
( ~ spl1079_343
| ~ spl1079_344
| spl1079_345
| ~ spl1079_356
| ~ spl1079_361
| spl1079_367
| ~ spl1079_368
| ~ spl1079_380
| ~ spl1079_382 ),
inference(avatar_contradiction_clause,[],[f20542]) ).
cnf(s305,plain,
spl1079_343,
inference(sat_conversion,[],[f18293]) ).
cnf(s307,plain,
~ spl1079_345,
inference(sat_conversion,[],[f18304]) ).
cnf(s311,plain,
( spl1079_367
| spl1079_368 ),
inference(sat_conversion,[],[f18408]) ).
cnf(s321,plain,
( spl1079_361
| spl1079_367 ),
inference(sat_conversion,[],[f18513]) ).
cnf(s322,plain,
~ spl1079_367,
inference(sat_conversion,[],[f18524]) ).
cnf(s323,plain,
( spl1079_379
| spl1079_380 ),
inference(sat_conversion,[],[f18542]) ).
cnf(s325,plain,
~ spl1079_379,
inference(sat_conversion,[],[f18558]) ).
cnf(s326,plain,
spl1079_356,
inference(sat_conversion,[],[f18589]) ).
cnf(s329,plain,
( ~ spl1079_356
| spl1079_382 ),
inference(sat_conversion,[],[f18689]) ).
cnf(s387,plain,
spl1079_344,
inference(sat_conversion,[],[f20082]) ).
cnf(s403,plain,
( ~ spl1079_343
| ~ spl1079_344
| spl1079_345
| ~ spl1079_356
| ~ spl1079_361
| spl1079_367
| ~ spl1079_368
| ~ spl1079_380
| ~ spl1079_382 ),
inference(sat_conversion,[],[f20543]) ).
cnf(s406,plain,
spl1079_382,
inference(rat,[],[s329,s326]) ).
cnf(s410,plain,
spl1079_380,
inference(rat,[],[s323,s325]) ).
cnf(s412,plain,
spl1079_361,
inference(rat,[],[s321,s322]) ).
cnf(s418,plain,
spl1079_368,
inference(rat,[],[s311,s322]) ).
cnf(s420,plain,
~ spl1079_343,
inference(rat,[],[s403,s406,s410,s418,s322,s412,s326,s387,s307]) ).
cnf(s421,plain,
$false,
inference(rat,[],[s305,s420]) ).
fof(f20544,plain,
$false,
inference(avatar_sat_refutation,[],[s421]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT312+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.37 % Computer : n013.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Sun Sep 27 14:29:22 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.41 Running first-order theorem proving
% 0.11/0.41 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
% 15.92/3.14 % (281794)Detected formulas, will run a generic FOF schedule.
% 15.92/3.14 % (281801)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=3257924810:i=141695:sd=1:nm=32:gsp=on:ss=included_2998 on theBenchmark for (2998ds/141695Mi)
% 15.92/3.14 % (281802)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=799086571:i=109:sd=1:ins=1:gsp=on:ss=axioms_2998 on theBenchmark for (2998ds/109Mi)
% 15.92/3.14 % (281799)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=1932635930:i=141193_2998 on theBenchmark for (2998ds/141193Mi)
% 15.92/3.14 % (281804)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=311981182:s2a=on:i=139:gtg=position_2998 on theBenchmark for (2998ds/139Mi)
% 15.92/3.14 % (281803)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1932286015:i=119:av=off:ss=axioms_2998 on theBenchmark for (2998ds/119Mi)
% 15.92/3.14 % (281805)dis-21_1_sil=8000:lcm=predicate:random_seed=900119688:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2998 on theBenchmark for (2998ds/129Mi)
% 15.92/3.14 % (281800)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=2089314148:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2998 on theBenchmark for (2998ds/134677Mi)
% 15.92/3.14 % (281802)Instruction limit reached!
% 15.92/3.14 % (281802)------------------------------
% 15.92/3.14 % (281802)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.92/3.14 % (281802)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.92/3.14 % (281802)CaDiCaL version: 2.1.3
% 15.92/3.14 % (281802)Termination reason: Instruction limit
% 15.92/3.14 % (281802)Termination phase: Saturation
% 15.92/3.14 % (281802)Time elapsed: 0.068 s
% 15.92/3.14 % (281802)Peak memory usage: 92 MB
% 15.92/3.14 % (281802)Instructions burned: 110 (million)
% 15.92/3.14 % (281805)Instruction limit reached!
% 15.92/3.14 % (281805)------------------------------
% 15.92/3.14 % (281805)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.92/3.14 % (281805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.92/3.14 % (281805)CaDiCaL version: 2.1.3
% 15.92/3.14 % (281805)Termination reason: Instruction limit
% 15.92/3.14 % (281805)Termination phase: Property scanning
% 15.92/3.14 % (281805)Time elapsed: 0.076 s
% 15.92/3.14 % (281805)Peak memory usage: 92 MB
% 15.92/3.14 % (281805)Instructions burned: 130 (million)
% 15.92/3.14 % (281803)Instruction limit reached!
% 15.92/3.14 % (281803)------------------------------
% 15.92/3.14 % (281803)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.92/3.14 % (281803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.92/3.14 % (281803)CaDiCaL version: 2.1.3
% 15.92/3.14 % (281803)Termination reason: Instruction limit
% 15.92/3.14 % (281803)Termination phase: Saturation
% 15.92/3.14 % (281803)Time elapsed: 0.076 s
% 15.92/3.14 % (281803)Peak memory usage: 92 MB
% 15.92/3.14 % (281803)Instructions burned: 119 (million)
% 15.92/3.14 % (281804)Instruction limit reached!
% 15.92/3.14 % (281804)------------------------------
% 15.92/3.14 % (281804)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.92/3.14 % (281804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.92/3.14 % (281804)CaDiCaL version: 2.1.3
% 15.92/3.14 % (281804)Termination reason: Instruction limit
% 15.92/3.14 % (281804)Termination phase: Property scanning
% 15.92/3.14 % (281804)Time elapsed: 0.084 s
% 15.92/3.14 % (281804)Peak memory usage: 94 MB
% 15.92/3.14 % (281804)Instructions burned: 141 (million)
% 15.92/3.14 % (281813)lrs+10_1_sil=8000:sp=occurrence:random_seed=2369659635:i=285:sd=3:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/285Mi)
% 15.92/3.14 % (281815)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1319040124:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi)
% 15.92/3.14 % (281814)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3734341879:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/157Mi)
% 15.92/3.14 % (281816)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=518684414:s2a=on:i=248:s2at=1.23:gtg=position_2996 on theBenchmark for (2996ds/248Mi)
% 15.92/3.14 % (281814)Instruction limit reached!
% 15.92/3.14 % (281814)------------------------------
% 19.38/3.79 % (281814)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.38/3.79 % (281814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.38/3.79 % (281814)CaDiCaL version: 2.1.3
% 19.38/3.79 % (281814)Termination reason: Instruction limit
% 19.38/3.79 % (281814)Termination phase: Saturation
% 19.38/3.79 % (281814)Time elapsed: 0.087 s
% 19.38/3.79 % (281814)Peak memory usage: 92 MB
% 19.38/3.79 % (281814)Instructions burned: 158 (million)
% 19.38/3.79 % (281816)Instruction limit reached!
% 19.38/3.79 % (281816)------------------------------
% 19.38/3.79 % (281816)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.38/3.79 % (281816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.38/3.79 % (281816)CaDiCaL version: 2.1.3
% 19.38/3.79 % (281816)Termination reason: Instruction limit
% 19.38/3.79 % (281816)Termination phase: Saturation
% 19.38/3.79 % (281816)Time elapsed: 0.137 s
% 19.38/3.79 % (281816)Peak memory usage: 97 MB
% 19.38/3.79 % (281816)Instructions burned: 249 (million)
% 19.38/3.79 % (281813)Instruction limit reached!
% 19.38/3.79 % (281813)------------------------------
% 19.38/3.79 % (281813)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.38/3.79 % (281813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.38/3.79 % (281813)CaDiCaL version: 2.1.3
% 19.38/3.79 % (281813)Termination reason: Instruction limit
% 19.38/3.79 % (281813)Termination phase: Saturation
% 19.38/3.79 % (281813)Time elapsed: 0.191 s
% 19.38/3.79 % (281813)Peak memory usage: 95 MB
% 19.38/3.79 % (281813)Instructions burned: 285 (million)
% 19.38/3.79 % (281815)Instruction limit reached!
% 19.38/3.79 % (281815)------------------------------
% 19.38/3.79 % (281815)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.38/3.79 % (281815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.38/3.79 % (281815)CaDiCaL version: 2.1.3
% 19.38/3.79 % (281815)Termination reason: Instruction limit
% 19.38/3.79 % (281815)Termination phase: Saturation
% 19.38/3.79 % (281815)Time elapsed: 0.204 s
% 19.38/3.79 % (281815)Peak memory usage: 93 MB
% 19.38/3.79 % (281815)Instructions burned: 326 (million)
% 19.38/3.79 % (281821)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=833842345:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2993 on theBenchmark for (2993ds/294Mi)
% 19.38/3.79 % (281822)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=4059118936:i=2350_2993 on theBenchmark for (2993ds/2350Mi)
% 19.38/3.79 % (281823)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=4096474737:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi)
% 19.38/3.79 % (281824)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1076037548:i=127:av=off:fsr=off:sup=off_2992 on theBenchmark for (2992ds/127Mi)
% 19.38/3.79 % (281823)Instruction limit reached!
% 19.38/3.79 % (281823)------------------------------
% 19.38/3.79 % (281823)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.38/3.79 % (281823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.38/3.79 % (281823)CaDiCaL version: 2.1.3
% 19.38/3.79 % (281823)Termination reason: Instruction limit
% 19.38/3.79 % (281823)Termination phase: Saturation
% 19.38/3.79 % (281823)Time elapsed: 0.064 s
% 19.38/3.79 % (281823)Peak memory usage: 93 MB
% 19.38/3.79 % (281823)Instructions burned: 114 (million)
% 19.38/3.79 % (281821)Instruction limit reached!
% 19.38/3.79 % (281821)------------------------------
% 19.38/3.79 % (281821)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.38/3.79 % (281821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.38/3.79 % (281821)CaDiCaL version: 2.1.3
% 19.38/3.79 % (281821)Termination reason: Instruction limit
% 19.38/3.79 % (281821)Termination phase: Saturation
% 19.38/3.79 % (281821)Time elapsed: 0.165 s
% 19.38/3.79 % (281821)Peak memory usage: 95 MB
% 19.38/3.79 % (281821)Instructions burned: 294 (million)
% 19.38/3.79 % (281824)Instruction limit reached!
% 19.38/3.79 % (281824)------------------------------
% 19.38/3.79 % (281824)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.38/3.79 % (281824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.38/3.79 % (281824)CaDiCaL version: 2.1.3
% 19.38/3.79 % (281824)Termination reason: Instruction limit
% 19.38/3.79 % (281824)Termination phase: Property scanning
% 19.38/3.79 % (281824)Time elapsed: 0.075 s
% 19.38/3.79 % (281824)Peak memory usage: 94 MB
% 19.38/3.79 % (281824)Instructions burned: 127 (million)
% 19.38/3.79 % (281829)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=449511205:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2990 on theBenchmark for (2990ds/114Mi)
% 19.38/3.79 % (281830)lrs+10_1_sil=8000:sp=occurrence:random_seed=350745624:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2990 on theBenchmark for (2990ds/907Mi)
% 19.38/3.79 % (281831)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3732779521:i=437:sd=1:aac=none:ss=included_2990 on theBenchmark for (2990ds/437Mi)
% 19.38/3.79 % (281829)Instruction limit reached!
% 19.38/3.79 % (281829)------------------------------
% 19.38/3.79 % (281829)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.38/3.79 % (281829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.38/3.79 % (281829)CaDiCaL version: 2.1.3
% 19.38/3.79 % (281829)Termination reason: Instruction limit
% 19.38/3.79 % (281829)Termination phase: Property scanning
% 19.38/3.79 % (281829)Time elapsed: 0.058 s
% 19.38/3.79 % (281829)Peak memory usage: 90 MB
% 19.38/3.79 % (281829)Instructions burned: 115 (million)
% 19.38/3.79 % (281835)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=382544708:i=5202:ss=axioms:sgt=16_2988 on theBenchmark for (2988ds/5202Mi)
% 19.38/3.79 % (281831)Instruction limit reached!
% 19.38/3.79 % (281831)------------------------------
% 19.38/3.79 % (281831)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.38/3.79 % (281831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.38/3.79 % (281831)CaDiCaL version: 2.1.3
% 19.38/3.79 % (281831)Termination reason: Instruction limit
% 19.38/3.79 % (281831)Termination phase: Saturation
% 19.38/3.79 % (281831)Time elapsed: 0.249 s
% 19.38/3.79 % (281831)Peak memory usage: 95 MB
% 19.38/3.79 % (281831)Instructions burned: 438 (million)
% 19.38/3.79 % (281837)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2104649258:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2986 on theBenchmark for (2986ds/134Mi)
% 19.38/3.79 % (281837)Instruction limit reached!
% 19.38/3.79 % (281837)------------------------------
% 19.38/3.79 % (281837)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.38/3.79 % (281837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.38/3.79 % (281837)CaDiCaL version: 2.1.3
% 19.38/3.79 % (281837)Termination reason: Instruction limit
% 19.38/3.79 % (281837)Termination phase: Saturation
% 19.38/3.79 % (281837)Time elapsed: 0.081 s
% 19.38/3.79 % (281837)Peak memory usage: 94 MB
% 19.38/3.79 % (281837)Instructions burned: 134 (million)
% 19.38/3.79 % (281830)Instruction limit reached!
% 19.38/3.79 % (281830)------------------------------
% 19.38/3.79 % (281830)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.38/3.79 % (281830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.38/3.79 % (281830)CaDiCaL version: 2.1.3
% 19.38/3.79 % (281830)Termination reason: Instruction limit
% 19.38/3.79 % (281830)Termination phase: Saturation
% 19.38/3.79 % (281830)Time elapsed: 0.601 s
% 19.38/3.79 % (281830)Peak memory usage: 103 MB
% 19.38/3.79 % (281830)Instructions burned: 907 (million)
% 19.38/3.79 % (281839)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=691262187:st=8:i=592:sd=3:ep=RST:ss=axioms_2983 on theBenchmark for (2983ds/592Mi)
% 19.38/3.79 % (281840)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2275227493:st=3:i=13193:sd=3:ss=axioms_2983 on theBenchmark for (2983ds/13193Mi)
% 19.38/3.79 % (281839)Instruction limit reached!
% 19.38/3.79 % (281839)------------------------------
% 19.38/3.79 % (281839)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.38/3.79 % (281839)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.38/3.79 % (281839)CaDiCaL version: 2.1.3
% 19.38/3.79 % (281839)Termination reason: Instruction limit
% 19.38/3.79 % (281839)Termination phase: Saturation
% 19.38/3.79 % (281839)Time elapsed: 0.301 s
% 19.38/3.79 % (281839)Peak memory usage: 102 MB
% 19.38/3.79 % (281839)Instructions burned: 592 (million)
% 19.38/3.79 % (281843)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=2211349156:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2978 on theBenchmark for (2978ds/125Mi)
% 19.38/3.79 % (281822)Instruction limit reached!
% 19.38/3.79 % (281822)------------------------------
% 19.38/3.79 % (281822)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.38/3.79 % (281822)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.38/3.79 % (281822)CaDiCaL version: 2.1.3
% 19.38/3.79 % (281822)Termination reason: Instruction limit
% 19.38/3.79 % (281822)Termination phase: Saturation
% 19.38/3.79 % (281822)Time elapsed: 1.483 s
% 19.38/3.79 % (281822)Peak memory usage: 212 MB
% 19.38/3.79 % (281822)Instructions burned: 2351 (million)
% 19.38/3.79 % (281843)Instruction limit reached!
% 19.38/3.79 % (281843)------------------------------
% 19.38/3.79 % (281843)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.38/3.79 % (281843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.38/3.79 % (281843)CaDiCaL version: 2.1.3
% 19.38/3.79 % (281843)Termination reason: Instruction limit
% 19.38/3.79 % (281843)Termination phase: Saturation
% 19.38/3.79 % (281843)Time elapsed: 0.069 s
% 19.38/3.79 % (281843)Peak memory usage: 93 MB
% 19.38/3.79 % (281843)Instructions burned: 127 (million)
% 19.38/3.79 % (281845)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2571365190:i=134:gtgl=5:slsql=off:gtg=exists_sym_2976 on theBenchmark for (2976ds/134Mi)
% 19.38/3.79 % (281846)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3095350873:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2976 on theBenchmark for (2976ds/141Mi)
% 19.38/3.79 % (281845)Instruction limit reached!
% 19.38/3.79 % (281845)------------------------------
% 19.38/3.79 % (281845)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.38/3.79 % (281845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.38/3.79 % (281845)CaDiCaL version: 2.1.3
% 19.38/3.79 % (281845)Termination reason: Instruction limit
% 19.38/3.79 % (281845)Termination phase: Preprocessing 3
% 19.38/3.79 % (281845)Time elapsed: 0.077 s
% 19.38/3.79 % (281845)Peak memory usage: 92 MB
% 19.38/3.79 % (281845)Instructions burned: 135 (million)
% 19.38/3.79 % (281846)Instruction limit reached!
% 19.38/3.79 % (281846)------------------------------
% 19.38/3.79 % (281846)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.38/3.79 % (281846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.38/3.79 % (281846)CaDiCaL version: 2.1.3
% 19.38/3.79 % (281846)Termination reason: Instruction limit
% 19.38/3.79 % (281846)Termination phase: Saturation
% 19.38/3.79 % (281846)Time elapsed: 0.095 s
% 19.38/3.79 % (281846)Peak memory usage: 93 MB
% 19.38/3.79 % (281846)Instructions burned: 141 (million)
% 19.38/3.79 % (281799)First to succeed.
% 19.38/3.79 % (281799)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-281794"
% 19.38/3.79 % (281849)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=178323198:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2974 on theBenchmark for (2974ds/431Mi)
% 19.38/3.79 % (281850)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=580542368:i=6060:aac=none:ins=25_2974 on theBenchmark for (2974ds/6060Mi)
% 19.38/3.79 % (281799)Refutation found. Thanks to Tanya!
% 19.38/3.79 % SZS status Theorem for theBenchmark
% 19.38/3.79 % SZS output start Proof for theBenchmark
% See solution above
% 20.66/3.98 % (281799)------------------------------
% 20.66/3.98 % (281799)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.66/3.98 % (281799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.66/3.98 % (281799)CaDiCaL version: 2.1.3
% 20.66/3.98 % (281799)Termination reason: Refutation
% 20.66/3.98 % (281799)Time elapsed: 2.369 s
% 20.66/3.98 % (281799)Peak memory usage: 217 MB
% 20.66/3.98 % (281799)Instructions burned: 3875 (million)
% 20.66/3.98 % (281799)------------------------------
% 20.66/3.98 % (281799)------------------------------
% 20.66/3.98 % (281794)Success in time 2.935 s
% 20.66/3.98 % Vampire exiting
%------------------------------------------------------------------------------