%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT340+3 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n006.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:06 AM UTC 2026
% Result : Theorem 58.75s 11.40s
% Output : Refutation 66.04s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 45
% Syntax : Number of formulae : 324 ( 33 unt; 17 def)
% Number of atoms : 1408 ( 103 equ)
% Maximal formula atoms : 15 ( 4 avg)
% Number of connectives : 1750 ( 666 ~; 787 |; 236 &)
% ( 22 <=>; 39 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 6 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 44 ( 42 usr; 16 prp; 0-3 aty)
% Number of functors : 15 ( 15 usr; 2 con; 0-2 aty)
% Number of variables : 256 ( 0 sgn 254 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f480,axiom,
! [X0,X1] :
( ( ~ v1_xboole_0(X0)
=> ( m1_subset_1(X1,X0)
<=> r2_hidden(X1,X0) ) )
& ( v1_xboole_0(X0)
=> ( m1_subset_1(X1,X0)
<=> v1_xboole_0(X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d2_subset_1) ).
fof(f482,axiom,
! [X0] : k2_subset_1(X0) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d4_subset_1) ).
fof(f6422,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_struct_0(X0) )
=> ~ v1_xboole_0(u1_struct_0(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_struct_0) ).
fof(f6650,axiom,
! [X0] :
( l3_lattices(X0)
=> ( ( ~ v3_struct_0(X0)
& v10_lattices(X0) )
=> ( ~ v3_struct_0(X0)
& v4_lattices(X0)
& v5_lattices(X0)
& v6_lattices(X0)
& v7_lattices(X0)
& v8_lattices(X0)
& v9_lattices(X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc1_lattices) ).
fof(f6709,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v4_lattices(X0)
& l2_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ( ( r1_lattices(X0,X1,X2)
& r1_lattices(X0,X2,X1) )
=> X1 = X2 ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t26_lattices) ).
fof(f6724,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v13_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> r3_lattices(X0,k5_lattices(X0),X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t41_lattices) ).
fof(f6740,axiom,
! [X0] :
( l2_lattices(X0)
=> l1_struct_0(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l2_lattices) ).
fof(f6742,axiom,
! [X0] :
( l3_lattices(X0)
=> ( l1_lattices(X0)
& l2_lattices(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l3_lattices) ).
fof(f6748,axiom,
! [X0,X1,X2] :
( ( ~ v3_struct_0(X0)
& v6_lattices(X0)
& v8_lattices(X0)
& v9_lattices(X0)
& l3_lattices(X0)
& m1_subset_1(X1,u1_struct_0(X0))
& m1_subset_1(X2,u1_struct_0(X0)) )
=> ( r3_lattices(X0,X1,X2)
<=> r1_lattices(X0,X1,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_r3_lattices) ).
fof(f6757,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_lattices(X0) )
=> m1_subset_1(k5_lattices(X0),u1_struct_0(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k5_lattices) ).
fof(f8588,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> m1_filter_0(u1_struct_0(X0),X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t15_filter_0) ).
fof(f8673,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/sandbox2/benchmark/theBenchmark.p',dt_m1_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/sandbox2/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/sandbox2/benchmark/theBenchmark.p',fc6_lattice2) ).
fof(f9392,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v3_lattices(X0)
& l3_lattices(X0) )
=> k1_lattice2(k1_lattice2(X0)) = X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t19_lattice2) ).
fof(f9463,axiom,
! [X0] :
( l3_lattices(X0)
=> ( v3_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k1_lattice2) ).
fof(f11615,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v4_lattice3(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( r2_hidden(X1,X2)
=> ( r3_lattices(X0,X1,k15_lattice3(X0,X2))
& r3_lattices(X0,k16_lattice3(X0,X2),X1) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t38_lattice3) ).
fof(f11624,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v4_lattice3(X0)
& l3_lattices(X0) )
=> ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v13_lattices(X0)
& l3_lattices(X0)
& k5_lattices(X0) = k15_lattice3(X0,k1_xboole_0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t50_lattice3) ).
fof(f11625,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v4_lattice3(X0)
& l3_lattices(X0) )
=> ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v14_lattices(X0)
& l3_lattices(X0)
& k6_lattices(X0) = k15_lattice3(X0,u1_struct_0(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t51_lattice3) ).
fof(f11650,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& l3_lattices(X0) )
=> m1_subset_1(k16_lattice3(X0,X1),u1_struct_0(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k16_lattice3) ).
fof(f17897,axiom,
! [X0] :
( ( ~ v3_conlat_1(X0)
& l2_conlat_1(X0) )
=> ( ~ v3_struct_0(k11_conlat_1(X0))
& v10_lattices(k11_conlat_1(X0))
& l3_lattices(k11_conlat_1(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t46_conlat_1) ).
fof(f17900,axiom,
! [X0] :
( ( ~ v3_conlat_1(X0)
& l2_conlat_1(X0) )
=> ( ~ v3_struct_0(k11_conlat_1(X0))
& v10_lattices(k11_conlat_1(X0))
& v4_lattice3(k11_conlat_1(X0))
& l3_lattices(k11_conlat_1(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t48_conlat_1) ).
fof(f17929,axiom,
! [X0] :
( ( ~ v3_conlat_1(X0)
& l2_conlat_1(X0) )
=> ( ~ v3_struct_0(k11_conlat_1(X0))
& v3_lattices(k11_conlat_1(X0))
& l3_lattices(k11_conlat_1(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k11_conlat_1) ).
fof(f18293,axiom,
! [X0] :
( ( ~ v3_conlat_1(X0)
& l2_conlat_1(X0) )
=> ( ~ v3_struct_0(k11_conlat_1(X0))
& v3_lattices(k11_conlat_1(X0))
& v4_lattices(k11_conlat_1(X0))
& v5_lattices(k11_conlat_1(X0))
& v6_lattices(k11_conlat_1(X0))
& v7_lattices(k11_conlat_1(X0))
& v8_lattices(k11_conlat_1(X0))
& v9_lattices(k11_conlat_1(X0))
& v10_lattices(k11_conlat_1(X0))
& v13_lattices(k11_conlat_1(X0))
& v14_lattices(k11_conlat_1(X0))
& v15_lattices(k11_conlat_1(X0))
& v4_lattice3(k11_conlat_1(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_conlat_2) ).
fof(f18294,axiom,
! [X0] :
( ( ~ v3_conlat_1(X0)
& l2_conlat_1(X0) )
=> ( k5_lattices(k11_conlat_1(X0)) = k6_conlat_1(X0)
& k6_lattices(k11_conlat_1(X0)) = k5_conlat_1(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t1_conlat_2) ).
fof(f18298,axiom,
! [X0] :
( ( ~ v3_conlat_1(X0)
& l2_conlat_1(X0) )
=> ! [X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(k11_conlat_1(X0))))
=> k2_conlat_2(X0,X1) = k16_lattice3(k11_conlat_1(X0),X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d2_conlat_2) ).
fof(f18299,axiom,
! [X0] :
( ( ~ v3_conlat_1(X0)
& l2_conlat_1(X0) )
=> ! [X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(k11_conlat_1(X0))))
=> k3_conlat_2(X0,X1) = k15_lattice3(k11_conlat_1(X0),X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d3_conlat_2) ).
fof(f18301,conjecture,
! [X0] :
( ( ~ v3_conlat_1(X0)
& l2_conlat_1(X0) )
=> ( k3_conlat_2(X0,k2_subset_1(u1_struct_0(k11_conlat_1(X0)))) = k5_conlat_1(X0)
& k2_conlat_2(X0,k2_subset_1(u1_struct_0(k11_conlat_1(X0)))) = k6_conlat_1(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t6_conlat_2) ).
fof(f18302,negated_conjecture,
~ ! [X0] :
( ( ~ v3_conlat_1(X0)
& l2_conlat_1(X0) )
=> ( k3_conlat_2(X0,k2_subset_1(u1_struct_0(k11_conlat_1(X0)))) = k5_conlat_1(X0)
& k2_conlat_2(X0,k2_subset_1(u1_struct_0(k11_conlat_1(X0)))) = k6_conlat_1(X0) ) ),
inference(negated_conjecture,[status(cth)],[f18301]) ).
fof(f18469,plain,
? [X0] :
( ( k5_conlat_1(X0) != k3_conlat_2(X0,k2_subset_1(u1_struct_0(k11_conlat_1(X0))))
| k6_conlat_1(X0) != k2_conlat_2(X0,k2_subset_1(u1_struct_0(k11_conlat_1(X0)))) )
& ~ v3_conlat_1(X0)
& l2_conlat_1(X0) ),
inference(ennf_transformation,[],[f18302]) ).
fof(f18470,plain,
? [X0] :
( ( k5_conlat_1(X0) != k3_conlat_2(X0,k2_subset_1(u1_struct_0(k11_conlat_1(X0))))
| k6_conlat_1(X0) != k2_conlat_2(X0,k2_subset_1(u1_struct_0(k11_conlat_1(X0)))) )
& ~ v3_conlat_1(X0)
& l2_conlat_1(X0) ),
inference(flattening,[],[f18469]) ).
fof(f18495,plain,
! [X0] :
( ( k5_lattices(k11_conlat_1(X0)) = k6_conlat_1(X0)
& k6_lattices(k11_conlat_1(X0)) = k5_conlat_1(X0) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(ennf_transformation,[],[f18294]) ).
fof(f18496,plain,
! [X0] :
( ( k5_lattices(k11_conlat_1(X0)) = k6_conlat_1(X0)
& k6_lattices(k11_conlat_1(X0)) = k5_conlat_1(X0) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(flattening,[],[f18495]) ).
fof(f18497,plain,
! [X0] :
( ( ~ v3_struct_0(k11_conlat_1(X0))
& v3_lattices(k11_conlat_1(X0))
& v4_lattices(k11_conlat_1(X0))
& v5_lattices(k11_conlat_1(X0))
& v6_lattices(k11_conlat_1(X0))
& v7_lattices(k11_conlat_1(X0))
& v8_lattices(k11_conlat_1(X0))
& v9_lattices(k11_conlat_1(X0))
& v10_lattices(k11_conlat_1(X0))
& v13_lattices(k11_conlat_1(X0))
& v14_lattices(k11_conlat_1(X0))
& v15_lattices(k11_conlat_1(X0))
& v4_lattice3(k11_conlat_1(X0)) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(ennf_transformation,[],[f18293]) ).
fof(f18498,plain,
! [X0] :
( ( ~ v3_struct_0(k11_conlat_1(X0))
& v3_lattices(k11_conlat_1(X0))
& v4_lattices(k11_conlat_1(X0))
& v5_lattices(k11_conlat_1(X0))
& v6_lattices(k11_conlat_1(X0))
& v7_lattices(k11_conlat_1(X0))
& v8_lattices(k11_conlat_1(X0))
& v9_lattices(k11_conlat_1(X0))
& v10_lattices(k11_conlat_1(X0))
& v13_lattices(k11_conlat_1(X0))
& v14_lattices(k11_conlat_1(X0))
& v15_lattices(k11_conlat_1(X0))
& v4_lattice3(k11_conlat_1(X0)) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(flattening,[],[f18497]) ).
fof(f18499,plain,
! [X0] :
( ( ~ v3_struct_0(k11_conlat_1(X0))
& v3_lattices(k11_conlat_1(X0))
& l3_lattices(k11_conlat_1(X0)) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(ennf_transformation,[],[f17929]) ).
fof(f18500,plain,
! [X0] :
( ( ~ v3_struct_0(k11_conlat_1(X0))
& v3_lattices(k11_conlat_1(X0))
& l3_lattices(k11_conlat_1(X0)) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(flattening,[],[f18499]) ).
fof(f18501,plain,
! [X0] :
( ( ~ v3_struct_0(k11_conlat_1(X0))
& v10_lattices(k11_conlat_1(X0))
& v4_lattice3(k11_conlat_1(X0))
& l3_lattices(k11_conlat_1(X0)) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(ennf_transformation,[],[f17900]) ).
fof(f18502,plain,
! [X0] :
( ( ~ v3_struct_0(k11_conlat_1(X0))
& v10_lattices(k11_conlat_1(X0))
& v4_lattice3(k11_conlat_1(X0))
& l3_lattices(k11_conlat_1(X0)) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(flattening,[],[f18501]) ).
fof(f18503,plain,
! [X0] :
( ( ~ v3_struct_0(k11_conlat_1(X0))
& v10_lattices(k11_conlat_1(X0))
& l3_lattices(k11_conlat_1(X0)) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(ennf_transformation,[],[f17897]) ).
fof(f18504,plain,
! [X0] :
( ( ~ v3_struct_0(k11_conlat_1(X0))
& v10_lattices(k11_conlat_1(X0))
& l3_lattices(k11_conlat_1(X0)) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(flattening,[],[f18503]) ).
fof(f18535,plain,
! [X0] :
( ! [X1] :
( k2_conlat_2(X0,X1) = k16_lattice3(k11_conlat_1(X0),X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(k11_conlat_1(X0)))) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(ennf_transformation,[],[f18298]) ).
fof(f18536,plain,
! [X0] :
( ! [X1] :
( k2_conlat_2(X0,X1) = k16_lattice3(k11_conlat_1(X0),X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(k11_conlat_1(X0)))) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(flattening,[],[f18535]) ).
fof(f18539,plain,
! [X0] :
( ! [X1] :
( k3_conlat_2(X0,X1) = k15_lattice3(k11_conlat_1(X0),X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(k11_conlat_1(X0)))) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(ennf_transformation,[],[f18299]) ).
fof(f18540,plain,
! [X0] :
( ! [X1] :
( k3_conlat_2(X0,X1) = k15_lattice3(k11_conlat_1(X0),X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(k11_conlat_1(X0)))) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(flattening,[],[f18539]) ).
fof(f18560,plain,
! [X0,X1] :
( ( ( m1_subset_1(X1,X0)
<=> r2_hidden(X1,X0) )
| v1_xboole_0(X0) )
& ( ( m1_subset_1(X1,X0)
<=> v1_xboole_0(X1) )
| ~ v1_xboole_0(X0) ) ),
inference(ennf_transformation,[],[f480]) ).
fof(f19121,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v14_lattices(X0)
& l3_lattices(X0)
& k6_lattices(X0) = k15_lattice3(X0,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v4_lattice3(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f11625]) ).
fof(f19122,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v14_lattices(X0)
& l3_lattices(X0)
& k6_lattices(X0) = k15_lattice3(X0,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v4_lattice3(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f19121]) ).
fof(f19123,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v13_lattices(X0)
& l3_lattices(X0)
& k5_lattices(X0) = k15_lattice3(X0,k1_xboole_0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v4_lattice3(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f11624]) ).
fof(f19124,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v13_lattices(X0)
& l3_lattices(X0)
& k5_lattices(X0) = k15_lattice3(X0,k1_xboole_0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v4_lattice3(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f19123]) ).
fof(f19133,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( r3_lattices(X0,X1,k15_lattice3(X0,X2))
& r3_lattices(X0,k16_lattice3(X0,X2),X1) )
| ~ r2_hidden(X1,X2) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v4_lattice3(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f11615]) ).
fof(f19134,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( r3_lattices(X0,X1,k15_lattice3(X0,X2))
& r3_lattices(X0,k16_lattice3(X0,X2),X1) )
| ~ r2_hidden(X1,X2) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v4_lattice3(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f19133]) ).
fof(f19135,plain,
! [X0,X1] :
( m1_subset_1(k16_lattice3(X0,X1),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f11650]) ).
fof(f19136,plain,
! [X0,X1] :
( m1_subset_1(k16_lattice3(X0,X1),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f19135]) ).
fof(f19173,plain,
! [X0] :
( m1_subset_1(k5_lattices(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_lattices(X0) ),
inference(ennf_transformation,[],[f6757]) ).
fof(f19174,plain,
! [X0] :
( m1_subset_1(k5_lattices(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_lattices(X0) ),
inference(flattening,[],[f19173]) ).
fof(f19179,plain,
! [X0] :
( ! [X1] :
( r3_lattices(X0,k5_lattices(X0),X1)
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v13_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f6724]) ).
fof(f19180,plain,
! [X0] :
( ! [X1] :
( r3_lattices(X0,k5_lattices(X0),X1)
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v13_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f19179]) ).
fof(f19235,plain,
! [X0] :
( ( v3_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) )
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f9463]) ).
fof(f19236,plain,
! [X0] :
( k1_lattice2(k1_lattice2(X0)) = X0
| v3_struct_0(X0)
| ~ v3_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f9392]) ).
fof(f19237,plain,
! [X0] :
( k1_lattice2(k1_lattice2(X0)) = X0
| v3_struct_0(X0)
| ~ v3_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f19236]) ).
fof(f19238,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(f19239,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,[],[f19238]) ).
fof(f19240,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(f19241,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f19240]) ).
fof(f19268,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( X1 = X2
| ~ r1_lattices(X0,X1,X2)
| ~ r1_lattices(X0,X2,X1)
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v4_lattices(X0)
| ~ l2_lattices(X0) ),
inference(ennf_transformation,[],[f6709]) ).
fof(f19269,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( X1 = X2
| ~ r1_lattices(X0,X1,X2)
| ~ r1_lattices(X0,X2,X1)
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v4_lattices(X0)
| ~ l2_lattices(X0) ),
inference(flattening,[],[f19268]) ).
fof(f19276,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v4_lattices(X0)
& v5_lattices(X0)
& v6_lattices(X0)
& v7_lattices(X0)
& v8_lattices(X0)
& v9_lattices(X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f6650]) ).
fof(f19277,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v4_lattices(X0)
& v5_lattices(X0)
& v6_lattices(X0)
& v7_lattices(X0)
& v8_lattices(X0)
& v9_lattices(X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f19276]) ).
fof(f19298,plain,
! [X0,X1,X2] :
( ( r3_lattices(X0,X1,X2)
<=> r1_lattices(X0,X1,X2) )
| v3_struct_0(X0)
| ~ v6_lattices(X0)
| ~ v8_lattices(X0)
| ~ v9_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f6748]) ).
fof(f19299,plain,
! [X0,X1,X2] :
( ( r3_lattices(X0,X1,X2)
<=> r1_lattices(X0,X1,X2) )
| v3_struct_0(X0)
| ~ v6_lattices(X0)
| ~ v8_lattices(X0)
| ~ v9_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(flattening,[],[f19298]) ).
fof(f19638,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f6422]) ).
fof(f19639,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(flattening,[],[f19638]) ).
fof(f23539,plain,
! [X0] :
( ( l1_lattices(X0)
& l2_lattices(X0) )
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f6742]) ).
fof(f23607,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,[],[f8673]) ).
fof(f23608,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,[],[f23607]) ).
fof(f23609,plain,
! [X0] :
( m1_filter_0(u1_struct_0(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f8588]) ).
fof(f23610,plain,
! [X0] :
( m1_filter_0(u1_struct_0(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f23609]) ).
fof(f23615,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l2_lattices(X0) ),
inference(ennf_transformation,[],[f6740]) ).
fof(f24619,definition,
! [X0] :
( ( ~ v3_struct_0(k11_conlat_1(X0))
& v3_lattices(k11_conlat_1(X0))
& v4_lattices(k11_conlat_1(X0))
& v5_lattices(k11_conlat_1(X0))
& v6_lattices(k11_conlat_1(X0))
& v7_lattices(k11_conlat_1(X0))
& v8_lattices(k11_conlat_1(X0))
& v9_lattices(k11_conlat_1(X0))
& v10_lattices(k11_conlat_1(X0))
& v13_lattices(k11_conlat_1(X0))
& v14_lattices(k11_conlat_1(X0))
& v15_lattices(k11_conlat_1(X0))
& v4_lattice3(k11_conlat_1(X0)) )
| ~ sP0(X0) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f24620,plain,
! [X0] :
( sP0(X0)
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(definition_folding,[],[f18498,f24619]) ).
fof(f24653,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)) )
| ~ sP19(X0) ),
introduced(definition,[new_symbols(definition,[sP19])],[predicate_definition_introduction]) ).
fof(f24654,plain,
! [X0] :
( sP19(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(definition_folding,[],[f19239,f24653]) ).
fof(f24936,plain,
( ( k5_conlat_1(sK187) != k3_conlat_2(sK187,k2_subset_1(u1_struct_0(k11_conlat_1(sK187))))
| k6_conlat_1(sK187) != k2_conlat_2(sK187,k2_subset_1(u1_struct_0(k11_conlat_1(sK187)))) )
& ~ v3_conlat_1(sK187)
& l2_conlat_1(sK187) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK187]),skolemize(X0,sK187)],[f18470]) ).
fof(f24949,plain,
! [X0] :
( ( ~ v3_struct_0(k11_conlat_1(X0))
& v3_lattices(k11_conlat_1(X0))
& v4_lattices(k11_conlat_1(X0))
& v5_lattices(k11_conlat_1(X0))
& v6_lattices(k11_conlat_1(X0))
& v7_lattices(k11_conlat_1(X0))
& v8_lattices(k11_conlat_1(X0))
& v9_lattices(k11_conlat_1(X0))
& v10_lattices(k11_conlat_1(X0))
& v13_lattices(k11_conlat_1(X0))
& v14_lattices(k11_conlat_1(X0))
& v15_lattices(k11_conlat_1(X0))
& v4_lattice3(k11_conlat_1(X0)) )
| ~ sP0(X0) ),
inference(nnf_transformation,[],[f24619]) ).
fof(f24961,plain,
! [X0,X1] :
( ( ( ( m1_subset_1(X1,X0)
| ~ r2_hidden(X1,X0) )
& ( r2_hidden(X1,X0)
| ~ m1_subset_1(X1,X0) ) )
| v1_xboole_0(X0) )
& ( ( ( m1_subset_1(X1,X0)
| ~ v1_xboole_0(X1) )
& ( v1_xboole_0(X1)
| ~ m1_subset_1(X1,X0) ) )
| ~ v1_xboole_0(X0) ) ),
inference(nnf_transformation,[],[f18560]) ).
fof(f25167,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)) )
| ~ sP19(X0) ),
inference(nnf_transformation,[],[f24653]) ).
fof(f25190,plain,
! [X0,X1,X2] :
( ( ( r3_lattices(X0,X1,X2)
| ~ r1_lattices(X0,X1,X2) )
& ( r1_lattices(X0,X1,X2)
| ~ r3_lattices(X0,X1,X2) ) )
| v3_struct_0(X0)
| ~ v6_lattices(X0)
| ~ v8_lattices(X0)
| ~ v9_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(nnf_transformation,[],[f19299]) ).
fof(f27157,plain,
l2_conlat_1(sK187),
inference(cnf_transformation,[],[f24936]) ).
fof(f27158,plain,
~ v3_conlat_1(sK187),
inference(cnf_transformation,[],[f24936]) ).
fof(f27159,plain,
( k5_conlat_1(sK187) != k3_conlat_2(sK187,k2_subset_1(u1_struct_0(k11_conlat_1(sK187))))
| k6_conlat_1(sK187) != k2_conlat_2(sK187,k2_subset_1(u1_struct_0(k11_conlat_1(sK187)))) ),
inference(cnf_transformation,[],[f24936]) ).
fof(f27184,plain,
! [X0] : k2_subset_1(X0) = X0,
inference(cnf_transformation,[],[f482]) ).
fof(f27195,plain,
! [X0] :
( ~ l2_conlat_1(X0)
| v3_conlat_1(X0)
| k5_conlat_1(X0) = k6_lattices(k11_conlat_1(X0)) ),
inference(cnf_transformation,[],[f18496]) ).
fof(f27196,plain,
! [X0] :
( ~ l2_conlat_1(X0)
| v3_conlat_1(X0)
| k6_conlat_1(X0) = k5_lattices(k11_conlat_1(X0)) ),
inference(cnf_transformation,[],[f18496]) ).
fof(f27207,plain,
! [X0] :
( v4_lattices(k11_conlat_1(X0))
| ~ sP0(X0) ),
inference(cnf_transformation,[],[f24949]) ).
fof(f27210,plain,
! [X0] :
( ~ l2_conlat_1(X0)
| v3_conlat_1(X0)
| sP0(X0) ),
inference(cnf_transformation,[],[f24620]) ).
fof(f27212,plain,
! [X0] :
( v3_lattices(k11_conlat_1(X0))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f18500]) ).
fof(f27215,plain,
! [X0] :
( v4_lattice3(k11_conlat_1(X0))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f18502]) ).
fof(f27218,plain,
! [X0] :
( l3_lattices(k11_conlat_1(X0))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f18504]) ).
fof(f27219,plain,
! [X0] :
( v10_lattices(k11_conlat_1(X0))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f18504]) ).
fof(f27220,plain,
! [X0] :
( ~ v3_struct_0(k11_conlat_1(X0))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f18504]) ).
fof(f27277,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(k11_conlat_1(X0))))
| k2_conlat_2(X0,X1) = k16_lattice3(k11_conlat_1(X0),X1)
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f18536]) ).
fof(f27281,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(k11_conlat_1(X0))))
| k3_conlat_2(X0,X1) = k15_lattice3(k11_conlat_1(X0),X1)
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f18540]) ).
fof(f27303,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,X0)
| r2_hidden(X1,X0)
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f24961]) ).
fof(f27997,plain,
! [X0] :
( ~ v4_lattice3(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| k6_lattices(X0) = k15_lattice3(X0,u1_struct_0(X0))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f19122]) ).
fof(f28004,plain,
! [X0] :
( ~ v4_lattice3(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| v13_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f19124]) ).
fof(f28016,plain,
! [X2,X0,X1] :
( r3_lattices(X0,k16_lattice3(X0,X2),X1)
| ~ r2_hidden(X1,X2)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v4_lattice3(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f19134]) ).
fof(f28018,plain,
! [X0,X1] :
( m1_subset_1(k16_lattice3(X0,X1),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f19136]) ).
fof(f28044,plain,
! [X0] :
( m1_subset_1(k5_lattices(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_lattices(X0) ),
inference(cnf_transformation,[],[f19174]) ).
fof(f28048,plain,
! [X0,X1] :
( r3_lattices(X0,k5_lattices(X0),X1)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v13_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f19180]) ).
fof(f28136,plain,
! [X0] :
( l3_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f19235]) ).
fof(f28138,plain,
! [X0] :
( ~ v3_lattices(X0)
| v3_struct_0(X0)
| k1_lattice2(k1_lattice2(X0)) = X0
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f19237]) ).
fof(f28139,plain,
! [X0] :
( v10_lattices(k1_lattice2(X0))
| ~ sP19(X0) ),
inference(cnf_transformation,[],[f25167]) ).
fof(f28148,plain,
! [X0] :
( ~ v10_lattices(X0)
| v3_struct_0(X0)
| sP19(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f24654]) ).
fof(f28150,plain,
! [X0] :
( ~ v3_struct_0(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f19241]) ).
fof(f28302,plain,
! [X2,X0,X1] :
( ~ r1_lattices(X0,X2,X1)
| ~ r1_lattices(X0,X1,X2)
| X1 = X2
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v4_lattices(X0)
| ~ l2_lattices(X0) ),
inference(cnf_transformation,[],[f19269]) ).
fof(f28316,plain,
! [X0] :
( v9_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f19277]) ).
fof(f28317,plain,
! [X0] :
( v8_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f19277]) ).
fof(f28319,plain,
! [X0] :
( v6_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f19277]) ).
fof(f28345,plain,
! [X2,X0,X1] :
( ~ r3_lattices(X0,X1,X2)
| r1_lattices(X0,X1,X2)
| v3_struct_0(X0)
| ~ v6_lattices(X0)
| ~ v8_lattices(X0)
| ~ v9_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f25190]) ).
fof(f28904,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(cnf_transformation,[],[f19639]) ).
fof(f34662,plain,
! [X0] :
( ~ l3_lattices(X0)
| l2_lattices(X0) ),
inference(cnf_transformation,[],[f23539]) ).
fof(f34663,plain,
! [X0] :
( ~ l3_lattices(X0)
| l1_lattices(X0) ),
inference(cnf_transformation,[],[f23539]) ).
fof(f34760,plain,
! [X0,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(cnf_transformation,[],[f23608]) ).
fof(f34762,plain,
! [X0] :
( m1_filter_0(u1_struct_0(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f23610]) ).
fof(f34767,plain,
! [X0] :
( ~ l2_lattices(X0)
| l1_struct_0(X0) ),
inference(cnf_transformation,[],[f23615]) ).
fof(f38557,plain,
( k5_conlat_1(sK187) != k3_conlat_2(sK187,u1_struct_0(k11_conlat_1(sK187)))
| k6_conlat_1(sK187) != k2_conlat_2(sK187,k2_subset_1(u1_struct_0(k11_conlat_1(sK187)))) ),
inference(forward_demodulation,[],[f27159,f27184]) ).
fof(f38675,plain,
( k6_conlat_1(sK187) != k2_conlat_2(sK187,u1_struct_0(k11_conlat_1(sK187)))
| k5_conlat_1(sK187) != k3_conlat_2(sK187,u1_struct_0(k11_conlat_1(sK187))) ),
inference(forward_demodulation,[],[f38557,f27184]) ).
fof(f38708,definition,
( spl1342_23
<=> k5_conlat_1(sK187) = k3_conlat_2(sK187,u1_struct_0(k11_conlat_1(sK187))) ),
introduced(definition,[new_symbols(definition,[spl1342_23])],[avatar_definition]) ).
fof(f38712,definition,
( spl1342_24
<=> k6_conlat_1(sK187) = k2_conlat_2(sK187,u1_struct_0(k11_conlat_1(sK187))) ),
introduced(definition,[new_symbols(definition,[spl1342_24])],[avatar_definition]) ).
fof(f38714,plain,
( k6_conlat_1(sK187) != k2_conlat_2(sK187,u1_struct_0(k11_conlat_1(sK187)))
| spl1342_24 ),
inference(avatar_component_clause,[],[f38712]) ).
fof(f38715,plain,
( ~ spl1342_23
| ~ spl1342_24 ),
inference(avatar_split_clause,[],[f38675,f38712,f38708]) ).
fof(f38732,plain,
( v3_conlat_1(sK187)
| k5_conlat_1(sK187) = k6_lattices(k11_conlat_1(sK187)) ),
inference(resolution,[],[f27157,f27195]) ).
fof(f38733,plain,
( v3_conlat_1(sK187)
| k6_conlat_1(sK187) = k5_lattices(k11_conlat_1(sK187)) ),
inference(resolution,[],[f27157,f27196]) ).
fof(f38734,plain,
k6_conlat_1(sK187) = k5_lattices(k11_conlat_1(sK187)),
inference(forward_subsumption_resolution,[],[f38733,f27158]) ).
fof(f38735,plain,
k5_conlat_1(sK187) = k6_lattices(k11_conlat_1(sK187)),
inference(forward_subsumption_resolution,[],[f38732,f27158]) ).
fof(f38740,plain,
( v3_conlat_1(sK187)
| sP0(sK187) ),
inference(resolution,[],[f27210,f27157]) ).
fof(f38741,plain,
sP0(sK187),
inference(forward_subsumption_resolution,[],[f38740,f27158]) ).
fof(f38760,definition,
( spl1342_26
<=> v3_struct_0(k1_lattice2(k11_conlat_1(sK187))) ),
introduced(definition,[new_symbols(definition,[spl1342_26])],[avatar_definition]) ).
fof(f38761,plain,
( ~ v3_struct_0(k1_lattice2(k11_conlat_1(sK187)))
| spl1342_26 ),
inference(avatar_component_clause,[],[f38760]) ).
fof(f38762,plain,
( v3_struct_0(k1_lattice2(k11_conlat_1(sK187)))
| ~ spl1342_26 ),
inference(avatar_component_clause,[],[f38760]) ).
fof(f38764,definition,
( spl1342_27
<=> v1_xboole_0(u1_struct_0(k11_conlat_1(sK187))) ),
introduced(definition,[new_symbols(definition,[spl1342_27])],[avatar_definition]) ).
fof(f38765,plain,
( v1_xboole_0(u1_struct_0(k11_conlat_1(sK187)))
| ~ spl1342_27 ),
inference(avatar_component_clause,[],[f38764]) ).
fof(f38766,plain,
( ~ v1_xboole_0(u1_struct_0(k11_conlat_1(sK187)))
| spl1342_27 ),
inference(avatar_component_clause,[],[f38764]) ).
fof(f38769,plain,
! [X0] :
( v3_struct_0(k11_conlat_1(X0))
| k11_conlat_1(X0) = k1_lattice2(k1_lattice2(k11_conlat_1(X0)))
| ~ l3_lattices(k11_conlat_1(X0))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(resolution,[],[f28138,f27212]) ).
fof(f38770,plain,
! [X0] :
( v3_struct_0(k11_conlat_1(X0))
| k11_conlat_1(X0) = k1_lattice2(k1_lattice2(k11_conlat_1(X0)))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(forward_subsumption_resolution,[],[f38769,f27218]) ).
fof(f38771,plain,
! [X0] :
( ~ l2_conlat_1(X0)
| v3_conlat_1(X0)
| k11_conlat_1(X0) = k1_lattice2(k1_lattice2(k11_conlat_1(X0))) ),
inference(forward_subsumption_resolution,[],[f38770,f27220]) ).
fof(f38772,plain,
( v3_conlat_1(sK187)
| k11_conlat_1(sK187) = k1_lattice2(k1_lattice2(k11_conlat_1(sK187))) ),
inference(resolution,[],[f38771,f27157]) ).
fof(f38773,plain,
k11_conlat_1(sK187) = k1_lattice2(k1_lattice2(k11_conlat_1(sK187))),
inference(forward_subsumption_resolution,[],[f38772,f27158]) ).
fof(f38777,definition,
( spl1342_28
<=> l3_lattices(k1_lattice2(k11_conlat_1(sK187))) ),
introduced(definition,[new_symbols(definition,[spl1342_28])],[avatar_definition]) ).
fof(f38778,plain,
( l3_lattices(k1_lattice2(k11_conlat_1(sK187)))
| ~ spl1342_28 ),
inference(avatar_component_clause,[],[f38777]) ).
fof(f38779,plain,
( ~ l3_lattices(k1_lattice2(k11_conlat_1(sK187)))
| spl1342_28 ),
inference(avatar_component_clause,[],[f38777]) ).
fof(f38781,definition,
( spl1342_29
<=> l3_lattices(k11_conlat_1(sK187)) ),
introduced(definition,[new_symbols(definition,[spl1342_29])],[avatar_definition]) ).
fof(f38782,plain,
( ~ l3_lattices(k11_conlat_1(sK187))
| spl1342_29 ),
inference(avatar_component_clause,[],[f38781]) ).
fof(f38783,plain,
( l3_lattices(k11_conlat_1(sK187))
| ~ spl1342_29 ),
inference(avatar_component_clause,[],[f38781]) ).
fof(f38786,definition,
( spl1342_30
<=> v3_struct_0(k11_conlat_1(sK187)) ),
introduced(definition,[new_symbols(definition,[spl1342_30])],[avatar_definition]) ).
fof(f38787,plain,
( v3_struct_0(k11_conlat_1(sK187))
| ~ spl1342_30 ),
inference(avatar_component_clause,[],[f38786]) ).
fof(f38788,plain,
( ~ v3_struct_0(k11_conlat_1(sK187))
| spl1342_30 ),
inference(avatar_component_clause,[],[f38786]) ).
fof(f38790,plain,
( ~ l3_lattices(k11_conlat_1(sK187))
| spl1342_28 ),
inference(resolution,[],[f38779,f28136]) ).
fof(f38791,plain,
( ~ spl1342_29
| spl1342_28 ),
inference(avatar_split_clause,[],[f38790,f38777,f38781]) ).
fof(f38792,plain,
( v3_conlat_1(sK187)
| ~ l2_conlat_1(sK187)
| spl1342_29 ),
inference(resolution,[],[f38782,f27218]) ).
fof(f38793,plain,
( ~ l2_conlat_1(sK187)
| spl1342_29 ),
inference(forward_subsumption_resolution,[],[f38792,f27158]) ).
fof(f38794,plain,
( $false
| spl1342_29 ),
inference(forward_subsumption_resolution,[],[f38793,f27157]) ).
fof(f38795,plain,
spl1342_29,
inference(avatar_contradiction_clause,[],[f38794]) ).
fof(f38802,definition,
( spl1342_31
<=> v10_lattices(k1_lattice2(k11_conlat_1(sK187))) ),
introduced(definition,[new_symbols(definition,[spl1342_31])],[avatar_definition]) ).
fof(f38803,plain,
( v10_lattices(k1_lattice2(k11_conlat_1(sK187)))
| ~ spl1342_31 ),
inference(avatar_component_clause,[],[f38802]) ).
fof(f38804,plain,
( ~ v10_lattices(k1_lattice2(k11_conlat_1(sK187)))
| spl1342_31 ),
inference(avatar_component_clause,[],[f38802]) ).
fof(f38850,plain,
! [X0] :
( v3_struct_0(k11_conlat_1(X0))
| sP19(k11_conlat_1(X0))
| ~ l3_lattices(k11_conlat_1(X0))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(resolution,[],[f28148,f27219]) ).
fof(f38851,plain,
! [X0] :
( v3_struct_0(k11_conlat_1(X0))
| sP19(k11_conlat_1(X0))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(forward_subsumption_resolution,[],[f38850,f27218]) ).
fof(f38855,plain,
! [X0] :
( sP19(k11_conlat_1(X0))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(forward_subsumption_resolution,[],[f38851,f27220]) ).
fof(f38931,plain,
( l2_lattices(k11_conlat_1(sK187))
| ~ spl1342_29 ),
inference(resolution,[],[f34662,f38783]) ).
fof(f38935,plain,
( l1_struct_0(k11_conlat_1(sK187))
| ~ spl1342_29 ),
inference(resolution,[],[f38931,f34767]) ).
fof(f39045,plain,
( v3_struct_0(k11_conlat_1(sK187))
| ~ l3_lattices(k11_conlat_1(sK187))
| ~ spl1342_26 ),
inference(resolution,[],[f38762,f28150]) ).
fof(f39046,plain,
( ~ l3_lattices(k11_conlat_1(sK187))
| ~ spl1342_26
| spl1342_30 ),
inference(forward_subsumption_resolution,[],[f39045,f38788]) ).
fof(f39048,plain,
( $false
| ~ spl1342_26
| ~ spl1342_29
| spl1342_30 ),
inference(forward_subsumption_resolution,[],[f39046,f38783]) ).
fof(f39049,plain,
( ~ spl1342_26
| ~ spl1342_29
| spl1342_30 ),
inference(avatar_contradiction_clause,[],[f39048]) ).
fof(f39056,definition,
( spl1342_49
<=> v10_lattices(k11_conlat_1(sK187)) ),
introduced(definition,[new_symbols(definition,[spl1342_49])],[avatar_definition]) ).
fof(f39057,plain,
( v10_lattices(k11_conlat_1(sK187))
| ~ spl1342_49 ),
inference(avatar_component_clause,[],[f39056]) ).
fof(f39063,plain,
( v3_conlat_1(sK187)
| ~ l2_conlat_1(sK187)
| ~ spl1342_30 ),
inference(resolution,[],[f38787,f27220]) ).
fof(f39064,plain,
( ~ l2_conlat_1(sK187)
| ~ spl1342_30 ),
inference(forward_subsumption_resolution,[],[f39063,f27158]) ).
fof(f39071,plain,
( $false
| ~ spl1342_30 ),
inference(forward_subsumption_resolution,[],[f39064,f27157]) ).
fof(f39072,plain,
~ spl1342_30,
inference(avatar_contradiction_clause,[],[f39071]) ).
fof(f39081,plain,
! [X0,X1] :
( ~ m1_filter_0(X0,k11_conlat_1(X1))
| v3_struct_0(k11_conlat_1(X1))
| ~ v10_lattices(k11_conlat_1(X1))
| ~ l3_lattices(k11_conlat_1(X1))
| k16_lattice3(k11_conlat_1(X1),X0) = k2_conlat_2(X1,X0)
| v3_conlat_1(X1)
| ~ l2_conlat_1(X1) ),
inference(resolution,[],[f34760,f27277]) ).
fof(f39085,plain,
! [X0,X1] :
( ~ m1_filter_0(X0,k11_conlat_1(X1))
| v3_struct_0(k11_conlat_1(X1))
| ~ v10_lattices(k11_conlat_1(X1))
| ~ l3_lattices(k11_conlat_1(X1))
| k15_lattice3(k11_conlat_1(X1),X0) = k3_conlat_2(X1,X0)
| v3_conlat_1(X1)
| ~ l2_conlat_1(X1) ),
inference(resolution,[],[f34760,f27281]) ).
fof(f39095,plain,
! [X0,X1] :
( ~ m1_filter_0(X0,k11_conlat_1(X1))
| v3_struct_0(k11_conlat_1(X1))
| ~ v10_lattices(k11_conlat_1(X1))
| k15_lattice3(k11_conlat_1(X1),X0) = k3_conlat_2(X1,X0)
| v3_conlat_1(X1)
| ~ l2_conlat_1(X1) ),
inference(forward_subsumption_resolution,[],[f39085,f27218]) ).
fof(f39099,plain,
! [X0,X1] :
( ~ m1_filter_0(X0,k11_conlat_1(X1))
| v3_struct_0(k11_conlat_1(X1))
| ~ v10_lattices(k11_conlat_1(X1))
| k16_lattice3(k11_conlat_1(X1),X0) = k2_conlat_2(X1,X0)
| v3_conlat_1(X1)
| ~ l2_conlat_1(X1) ),
inference(forward_subsumption_resolution,[],[f39081,f27218]) ).
fof(f39106,plain,
! [X0,X1] :
( ~ m1_filter_0(X0,k11_conlat_1(X1))
| ~ v10_lattices(k11_conlat_1(X1))
| k15_lattice3(k11_conlat_1(X1),X0) = k3_conlat_2(X1,X0)
| v3_conlat_1(X1)
| ~ l2_conlat_1(X1) ),
inference(forward_subsumption_resolution,[],[f39095,f27220]) ).
fof(f39110,plain,
! [X0,X1] :
( ~ m1_filter_0(X0,k11_conlat_1(X1))
| ~ v10_lattices(k11_conlat_1(X1))
| k16_lattice3(k11_conlat_1(X1),X0) = k2_conlat_2(X1,X0)
| v3_conlat_1(X1)
| ~ l2_conlat_1(X1) ),
inference(forward_subsumption_resolution,[],[f39099,f27220]) ).
fof(f39117,plain,
! [X0,X1] :
( ~ m1_filter_0(X0,k11_conlat_1(X1))
| k15_lattice3(k11_conlat_1(X1),X0) = k3_conlat_2(X1,X0)
| v3_conlat_1(X1)
| ~ l2_conlat_1(X1) ),
inference(forward_subsumption_resolution,[],[f39106,f27219]) ).
fof(f39121,plain,
! [X0,X1] :
( ~ m1_filter_0(X0,k11_conlat_1(X1))
| k16_lattice3(k11_conlat_1(X1),X0) = k2_conlat_2(X1,X0)
| v3_conlat_1(X1)
| ~ l2_conlat_1(X1) ),
inference(forward_subsumption_resolution,[],[f39110,f27219]) ).
fof(f39128,plain,
! [X0] :
( k2_conlat_2(X0,u1_struct_0(k11_conlat_1(X0))) = k16_lattice3(k11_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0)
| v3_struct_0(k11_conlat_1(X0))
| ~ v10_lattices(k11_conlat_1(X0))
| ~ l3_lattices(k11_conlat_1(X0)) ),
inference(resolution,[],[f39121,f34762]) ).
fof(f39129,plain,
! [X0] :
( k2_conlat_2(X0,u1_struct_0(k11_conlat_1(X0))) = k16_lattice3(k11_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0)
| v3_struct_0(k11_conlat_1(X0))
| ~ v10_lattices(k11_conlat_1(X0)) ),
inference(forward_subsumption_resolution,[],[f39128,f27218]) ).
fof(f39130,plain,
! [X0] :
( k2_conlat_2(X0,u1_struct_0(k11_conlat_1(X0))) = k16_lattice3(k11_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0)
| ~ v10_lattices(k11_conlat_1(X0)) ),
inference(forward_subsumption_resolution,[],[f39129,f27220]) ).
fof(f39131,plain,
! [X0] :
( ~ l2_conlat_1(X0)
| v3_conlat_1(X0)
| k2_conlat_2(X0,u1_struct_0(k11_conlat_1(X0))) = k16_lattice3(k11_conlat_1(X0),u1_struct_0(k11_conlat_1(X0))) ),
inference(forward_subsumption_resolution,[],[f39130,f27219]) ).
fof(f39133,plain,
( v3_conlat_1(sK187)
| k2_conlat_2(sK187,u1_struct_0(k11_conlat_1(sK187))) = k16_lattice3(k11_conlat_1(sK187),u1_struct_0(k11_conlat_1(sK187))) ),
inference(resolution,[],[f39131,f27157]) ).
fof(f39134,plain,
k2_conlat_2(sK187,u1_struct_0(k11_conlat_1(sK187))) = k16_lattice3(k11_conlat_1(sK187),u1_struct_0(k11_conlat_1(sK187))),
inference(forward_subsumption_resolution,[],[f39133,f27158]) ).
fof(f39139,plain,
! [X0] :
( k3_conlat_2(X0,u1_struct_0(k11_conlat_1(X0))) = k15_lattice3(k11_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0)
| v3_struct_0(k11_conlat_1(X0))
| ~ v10_lattices(k11_conlat_1(X0))
| ~ l3_lattices(k11_conlat_1(X0)) ),
inference(resolution,[],[f39117,f34762]) ).
fof(f39140,plain,
! [X0] :
( k3_conlat_2(X0,u1_struct_0(k11_conlat_1(X0))) = k15_lattice3(k11_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0)
| v3_struct_0(k11_conlat_1(X0))
| ~ v10_lattices(k11_conlat_1(X0)) ),
inference(forward_subsumption_resolution,[],[f39139,f27218]) ).
fof(f39141,plain,
! [X0] :
( k3_conlat_2(X0,u1_struct_0(k11_conlat_1(X0))) = k15_lattice3(k11_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0)
| ~ v10_lattices(k11_conlat_1(X0)) ),
inference(forward_subsumption_resolution,[],[f39140,f27220]) ).
fof(f39142,plain,
! [X0] :
( ~ l2_conlat_1(X0)
| v3_conlat_1(X0)
| k3_conlat_2(X0,u1_struct_0(k11_conlat_1(X0))) = k15_lattice3(k11_conlat_1(X0),u1_struct_0(k11_conlat_1(X0))) ),
inference(forward_subsumption_resolution,[],[f39141,f27219]) ).
fof(f39143,plain,
( v3_conlat_1(sK187)
| k3_conlat_2(sK187,u1_struct_0(k11_conlat_1(sK187))) = k15_lattice3(k11_conlat_1(sK187),u1_struct_0(k11_conlat_1(sK187))) ),
inference(resolution,[],[f39142,f27157]) ).
fof(f39144,plain,
k3_conlat_2(sK187,u1_struct_0(k11_conlat_1(sK187))) = k15_lattice3(k11_conlat_1(sK187),u1_struct_0(k11_conlat_1(sK187))),
inference(forward_subsumption_resolution,[],[f39143,f27158]) ).
fof(f39209,plain,
( v3_struct_0(k11_conlat_1(sK187))
| ~ l1_struct_0(k11_conlat_1(sK187))
| ~ spl1342_27 ),
inference(resolution,[],[f38765,f28904]) ).
fof(f39210,plain,
( ~ l1_struct_0(k11_conlat_1(sK187))
| ~ spl1342_27
| spl1342_30 ),
inference(forward_subsumption_resolution,[],[f39209,f38788]) ).
fof(f39211,plain,
( $false
| ~ spl1342_27
| ~ spl1342_29
| spl1342_30 ),
inference(forward_subsumption_resolution,[],[f39210,f38935]) ).
fof(f39212,plain,
( ~ spl1342_27
| ~ spl1342_29
| spl1342_30 ),
inference(avatar_contradiction_clause,[],[f39211]) ).
fof(f39314,plain,
( ~ sP19(k11_conlat_1(sK187))
| spl1342_31 ),
inference(resolution,[],[f28139,f38804]) ).
fof(f39316,plain,
( v10_lattices(k11_conlat_1(sK187))
| ~ sP19(k1_lattice2(k11_conlat_1(sK187))) ),
inference(superposition,[],[f28139,f38773]) ).
fof(f39318,definition,
( spl1342_53
<=> sP19(k1_lattice2(k11_conlat_1(sK187))) ),
introduced(definition,[new_symbols(definition,[spl1342_53])],[avatar_definition]) ).
fof(f39320,plain,
( ~ sP19(k1_lattice2(k11_conlat_1(sK187)))
| spl1342_53 ),
inference(avatar_component_clause,[],[f39318]) ).
fof(f39321,plain,
( ~ spl1342_53
| spl1342_49 ),
inference(avatar_split_clause,[],[f39316,f39056,f39318]) ).
fof(f39371,plain,
( v3_conlat_1(sK187)
| ~ l2_conlat_1(sK187)
| spl1342_31 ),
inference(resolution,[],[f39314,f38855]) ).
fof(f39372,plain,
( ~ l2_conlat_1(sK187)
| spl1342_31 ),
inference(forward_subsumption_resolution,[],[f39371,f27158]) ).
fof(f39373,plain,
( $false
| spl1342_31 ),
inference(forward_subsumption_resolution,[],[f39372,f27157]) ).
fof(f39374,plain,
spl1342_31,
inference(avatar_contradiction_clause,[],[f39373]) ).
fof(f39392,definition,
( spl1342_55
<=> v13_lattices(k11_conlat_1(sK187)) ),
introduced(definition,[new_symbols(definition,[spl1342_55])],[avatar_definition]) ).
fof(f39393,plain,
( ~ v13_lattices(k11_conlat_1(sK187))
| spl1342_55 ),
inference(avatar_component_clause,[],[f39392]) ).
fof(f39394,plain,
( v13_lattices(k11_conlat_1(sK187))
| ~ spl1342_55 ),
inference(avatar_component_clause,[],[f39392]) ).
fof(f39404,plain,
( v3_struct_0(k1_lattice2(k11_conlat_1(sK187)))
| sP19(k1_lattice2(k11_conlat_1(sK187)))
| ~ l3_lattices(k1_lattice2(k11_conlat_1(sK187)))
| ~ spl1342_31 ),
inference(resolution,[],[f38803,f28148]) ).
fof(f39405,plain,
( sP19(k1_lattice2(k11_conlat_1(sK187)))
| ~ l3_lattices(k1_lattice2(k11_conlat_1(sK187)))
| spl1342_26
| ~ spl1342_31 ),
inference(forward_subsumption_resolution,[],[f39404,f38761]) ).
fof(f39406,plain,
( ~ l3_lattices(k1_lattice2(k11_conlat_1(sK187)))
| spl1342_26
| ~ spl1342_31
| spl1342_53 ),
inference(forward_subsumption_resolution,[],[f39405,f39320]) ).
fof(f39407,plain,
( $false
| spl1342_26
| ~ spl1342_28
| ~ spl1342_31
| spl1342_53 ),
inference(forward_subsumption_resolution,[],[f39406,f38778]) ).
fof(f39408,plain,
( spl1342_26
| ~ spl1342_28
| ~ spl1342_31
| spl1342_53 ),
inference(avatar_contradiction_clause,[],[f39407]) ).
fof(f39521,plain,
! [X0] :
( v3_struct_0(k11_conlat_1(X0))
| ~ v10_lattices(k11_conlat_1(X0))
| v13_lattices(k11_conlat_1(X0))
| ~ l3_lattices(k11_conlat_1(X0))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(resolution,[],[f28004,f27215]) ).
fof(f39522,plain,
! [X0] :
( v3_struct_0(k11_conlat_1(X0))
| ~ v10_lattices(k11_conlat_1(X0))
| v13_lattices(k11_conlat_1(X0))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(forward_subsumption_resolution,[],[f39521,f27218]) ).
fof(f39524,plain,
! [X0] :
( ~ v10_lattices(k11_conlat_1(X0))
| v13_lattices(k11_conlat_1(X0))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(forward_subsumption_resolution,[],[f39522,f27220]) ).
fof(f39526,plain,
! [X0] :
( v13_lattices(k11_conlat_1(X0))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(forward_subsumption_resolution,[],[f39524,f27219]) ).
fof(f39588,plain,
( v3_conlat_1(sK187)
| ~ l2_conlat_1(sK187)
| spl1342_55 ),
inference(resolution,[],[f39393,f39526]) ).
fof(f39592,plain,
( ~ l2_conlat_1(sK187)
| spl1342_55 ),
inference(forward_subsumption_resolution,[],[f39588,f27158]) ).
fof(f39593,plain,
( $false
| spl1342_55 ),
inference(forward_subsumption_resolution,[],[f39592,f27157]) ).
fof(f39594,plain,
spl1342_55,
inference(avatar_contradiction_clause,[],[f39593]) ).
fof(f39714,plain,
( l1_lattices(k11_conlat_1(sK187))
| ~ spl1342_29 ),
inference(resolution,[],[f34663,f38783]) ).
fof(f39871,definition,
( spl1342_63
<=> v4_lattice3(k11_conlat_1(sK187)) ),
introduced(definition,[new_symbols(definition,[spl1342_63])],[avatar_definition]) ).
fof(f39872,plain,
( v4_lattice3(k11_conlat_1(sK187))
| ~ spl1342_63 ),
inference(avatar_component_clause,[],[f39871]) ).
fof(f39873,plain,
( ~ v4_lattice3(k11_conlat_1(sK187))
| spl1342_63 ),
inference(avatar_component_clause,[],[f39871]) ).
fof(f39880,plain,
( v3_conlat_1(sK187)
| ~ l2_conlat_1(sK187)
| spl1342_63 ),
inference(resolution,[],[f39873,f27215]) ).
fof(f39881,plain,
( ~ l2_conlat_1(sK187)
| spl1342_63 ),
inference(forward_subsumption_resolution,[],[f39880,f27158]) ).
fof(f39886,plain,
( $false
| spl1342_63 ),
inference(forward_subsumption_resolution,[],[f39881,f27157]) ).
fof(f39887,plain,
spl1342_63,
inference(avatar_contradiction_clause,[],[f39886]) ).
fof(f39929,plain,
( v3_struct_0(k11_conlat_1(sK187))
| ~ v10_lattices(k11_conlat_1(sK187))
| k6_lattices(k11_conlat_1(sK187)) = k15_lattice3(k11_conlat_1(sK187),u1_struct_0(k11_conlat_1(sK187)))
| ~ l3_lattices(k11_conlat_1(sK187))
| ~ spl1342_63 ),
inference(resolution,[],[f27997,f39872]) ).
fof(f39930,plain,
( ~ v10_lattices(k11_conlat_1(sK187))
| k6_lattices(k11_conlat_1(sK187)) = k15_lattice3(k11_conlat_1(sK187),u1_struct_0(k11_conlat_1(sK187)))
| ~ l3_lattices(k11_conlat_1(sK187))
| spl1342_30
| ~ spl1342_63 ),
inference(forward_subsumption_resolution,[],[f39929,f38788]) ).
fof(f39934,plain,
( k6_lattices(k11_conlat_1(sK187)) = k15_lattice3(k11_conlat_1(sK187),u1_struct_0(k11_conlat_1(sK187)))
| ~ l3_lattices(k11_conlat_1(sK187))
| spl1342_30
| ~ spl1342_49
| ~ spl1342_63 ),
inference(forward_subsumption_resolution,[],[f39930,f39057]) ).
fof(f39938,plain,
( k6_lattices(k11_conlat_1(sK187)) = k15_lattice3(k11_conlat_1(sK187),u1_struct_0(k11_conlat_1(sK187)))
| ~ spl1342_29
| spl1342_30
| ~ spl1342_49
| ~ spl1342_63 ),
inference(forward_subsumption_resolution,[],[f39934,f38783]) ).
fof(f39940,plain,
( k5_conlat_1(sK187) = k15_lattice3(k11_conlat_1(sK187),u1_struct_0(k11_conlat_1(sK187)))
| ~ spl1342_29
| spl1342_30
| ~ spl1342_49
| ~ spl1342_63 ),
inference(forward_demodulation,[],[f39938,f38735]) ).
fof(f39942,plain,
( k5_conlat_1(sK187) = k3_conlat_2(sK187,u1_struct_0(k11_conlat_1(sK187)))
| ~ spl1342_29
| spl1342_30
| ~ spl1342_49
| ~ spl1342_63 ),
inference(superposition,[],[f39144,f39940]) ).
fof(f39954,plain,
( spl1342_23
| ~ spl1342_29
| spl1342_30
| ~ spl1342_49
| ~ spl1342_63 ),
inference(avatar_split_clause,[],[f39942,f39871,f39056,f38786,f38781,f38708]) ).
fof(f40665,plain,
( m1_subset_1(k6_conlat_1(sK187),u1_struct_0(k11_conlat_1(sK187)))
| v3_struct_0(k11_conlat_1(sK187))
| ~ l1_lattices(k11_conlat_1(sK187)) ),
inference(superposition,[],[f28044,f38734]) ).
fof(f40672,plain,
( m1_subset_1(k6_conlat_1(sK187),u1_struct_0(k11_conlat_1(sK187)))
| ~ l1_lattices(k11_conlat_1(sK187))
| spl1342_30 ),
inference(forward_subsumption_resolution,[],[f40665,f38788]) ).
fof(f40685,plain,
( m1_subset_1(k6_conlat_1(sK187),u1_struct_0(k11_conlat_1(sK187)))
| ~ spl1342_29
| spl1342_30 ),
inference(forward_subsumption_resolution,[],[f40672,f39714]) ).
fof(f40702,plain,
( r2_hidden(k6_conlat_1(sK187),u1_struct_0(k11_conlat_1(sK187)))
| v1_xboole_0(u1_struct_0(k11_conlat_1(sK187)))
| ~ spl1342_29
| spl1342_30 ),
inference(resolution,[],[f40685,f27303]) ).
fof(f40703,plain,
( r2_hidden(k6_conlat_1(sK187),u1_struct_0(k11_conlat_1(sK187)))
| spl1342_27
| ~ spl1342_29
| spl1342_30 ),
inference(forward_subsumption_resolution,[],[f40702,f38766]) ).
fof(f42688,plain,
! [X0,X1] :
( r1_lattices(X0,k5_lattices(X0),X1)
| v3_struct_0(X0)
| ~ v6_lattices(X0)
| ~ v8_lattices(X0)
| ~ v9_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(k5_lattices(X0),u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v13_lattices(X0)
| ~ l3_lattices(X0) ),
inference(resolution,[],[f28345,f28048]) ).
fof(f42690,plain,
! [X2,X0,X1] :
( r1_lattices(X0,k16_lattice3(X0,X1),X2)
| v3_struct_0(X0)
| ~ v6_lattices(X0)
| ~ v8_lattices(X0)
| ~ v9_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(k16_lattice3(X0,X1),u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ r2_hidden(X2,X1)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v4_lattice3(X0)
| ~ l3_lattices(X0) ),
inference(resolution,[],[f28345,f28016]) ).
fof(f42703,plain,
! [X2,X0,X1] :
( r1_lattices(X0,k16_lattice3(X0,X1),X2)
| v3_struct_0(X0)
| ~ v6_lattices(X0)
| ~ v8_lattices(X0)
| ~ v9_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(k16_lattice3(X0,X1),u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ r2_hidden(X2,X1)
| ~ v10_lattices(X0)
| ~ v4_lattice3(X0) ),
inference(duplicate_literal_removal,[],[f42690]) ).
fof(f42705,plain,
! [X0,X1] :
( r1_lattices(X0,k5_lattices(X0),X1)
| v3_struct_0(X0)
| ~ v6_lattices(X0)
| ~ v8_lattices(X0)
| ~ v9_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(k5_lattices(X0),u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ v10_lattices(X0)
| ~ v13_lattices(X0) ),
inference(duplicate_literal_removal,[],[f42688]) ).
fof(f42716,plain,
! [X2,X0,X1] :
( r1_lattices(X0,k16_lattice3(X0,X1),X2)
| v3_struct_0(X0)
| ~ v8_lattices(X0)
| ~ v9_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(k16_lattice3(X0,X1),u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ r2_hidden(X2,X1)
| ~ v10_lattices(X0)
| ~ v4_lattice3(X0) ),
inference(forward_subsumption_resolution,[],[f42703,f28319]) ).
fof(f42718,plain,
! [X0,X1] :
( r1_lattices(X0,k5_lattices(X0),X1)
| v3_struct_0(X0)
| ~ v8_lattices(X0)
| ~ v9_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(k5_lattices(X0),u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ v10_lattices(X0)
| ~ v13_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f42705,f28319]) ).
fof(f42729,plain,
! [X2,X0,X1] :
( r1_lattices(X0,k16_lattice3(X0,X1),X2)
| v3_struct_0(X0)
| ~ v9_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(k16_lattice3(X0,X1),u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ r2_hidden(X2,X1)
| ~ v10_lattices(X0)
| ~ v4_lattice3(X0) ),
inference(forward_subsumption_resolution,[],[f42716,f28317]) ).
fof(f42731,plain,
! [X0,X1] :
( r1_lattices(X0,k5_lattices(X0),X1)
| v3_struct_0(X0)
| ~ v9_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(k5_lattices(X0),u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ v10_lattices(X0)
| ~ v13_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f42718,f28317]) ).
fof(f42743,plain,
! [X2,X0,X1] :
( r1_lattices(X0,k16_lattice3(X0,X1),X2)
| v3_struct_0(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(k16_lattice3(X0,X1),u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ r2_hidden(X2,X1)
| ~ v10_lattices(X0)
| ~ v4_lattice3(X0) ),
inference(forward_subsumption_resolution,[],[f42729,f28316]) ).
fof(f42745,plain,
! [X0,X1] :
( ~ m1_subset_1(k5_lattices(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0)
| r1_lattices(X0,k5_lattices(X0),X1)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ v10_lattices(X0)
| ~ v13_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f42731,f28316]) ).
fof(f42774,definition,
( spl1342_162
<=> ! [X0] :
( r1_lattices(k11_conlat_1(sK187),k6_conlat_1(sK187),X0)
| ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK187))) ) ),
introduced(definition,[new_symbols(definition,[spl1342_162])],[avatar_definition]) ).
fof(f42775,plain,
( ! [X0] :
( r1_lattices(k11_conlat_1(sK187),k6_conlat_1(sK187),X0)
| ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK187))) )
| ~ spl1342_162 ),
inference(avatar_component_clause,[],[f42774]) ).
fof(f42778,plain,
! [X2,X0,X1] :
( r1_lattices(X0,k16_lattice3(X0,X1),X2)
| v3_struct_0(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ r2_hidden(X2,X1)
| ~ v10_lattices(X0)
| ~ v4_lattice3(X0) ),
inference(forward_subsumption_resolution,[],[f42743,f28018]) ).
fof(f42852,plain,
! [X0] :
( ~ m1_subset_1(k6_conlat_1(sK187),u1_struct_0(k11_conlat_1(sK187)))
| v3_struct_0(k11_conlat_1(sK187))
| ~ l3_lattices(k11_conlat_1(sK187))
| r1_lattices(k11_conlat_1(sK187),k6_conlat_1(sK187),X0)
| ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK187)))
| ~ v10_lattices(k11_conlat_1(sK187))
| ~ v13_lattices(k11_conlat_1(sK187)) ),
inference(superposition,[],[f42745,f38734]) ).
fof(f42861,plain,
( ! [X0] :
( v3_struct_0(k11_conlat_1(sK187))
| ~ l3_lattices(k11_conlat_1(sK187))
| r1_lattices(k11_conlat_1(sK187),k6_conlat_1(sK187),X0)
| ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK187)))
| ~ v10_lattices(k11_conlat_1(sK187))
| ~ v13_lattices(k11_conlat_1(sK187)) )
| ~ spl1342_29
| spl1342_30 ),
inference(forward_subsumption_resolution,[],[f42852,f40685]) ).
fof(f42865,plain,
( ! [X0] :
( ~ l3_lattices(k11_conlat_1(sK187))
| r1_lattices(k11_conlat_1(sK187),k6_conlat_1(sK187),X0)
| ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK187)))
| ~ v10_lattices(k11_conlat_1(sK187))
| ~ v13_lattices(k11_conlat_1(sK187)) )
| ~ spl1342_29
| spl1342_30 ),
inference(forward_subsumption_resolution,[],[f42861,f38788]) ).
fof(f42868,plain,
( ! [X0] :
( r1_lattices(k11_conlat_1(sK187),k6_conlat_1(sK187),X0)
| ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK187)))
| ~ v10_lattices(k11_conlat_1(sK187))
| ~ v13_lattices(k11_conlat_1(sK187)) )
| ~ spl1342_29
| spl1342_30 ),
inference(forward_subsumption_resolution,[],[f42865,f38783]) ).
fof(f42871,plain,
( ! [X0] :
( r1_lattices(k11_conlat_1(sK187),k6_conlat_1(sK187),X0)
| ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK187)))
| ~ v13_lattices(k11_conlat_1(sK187)) )
| ~ spl1342_29
| spl1342_30
| ~ spl1342_49 ),
inference(forward_subsumption_resolution,[],[f42868,f39057]) ).
fof(f42874,plain,
( ! [X0] :
( r1_lattices(k11_conlat_1(sK187),k6_conlat_1(sK187),X0)
| ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK187))) )
| ~ spl1342_29
| spl1342_30
| ~ spl1342_49
| ~ spl1342_55 ),
inference(forward_subsumption_resolution,[],[f42871,f39394]) ).
fof(f42877,plain,
( spl1342_162
| ~ spl1342_29
| spl1342_30
| ~ spl1342_49
| ~ spl1342_55 ),
inference(avatar_split_clause,[],[f42874,f39392,f39056,f38786,f38781,f42774]) ).
fof(f42882,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK187)))
| ~ r1_lattices(k11_conlat_1(sK187),X0,k6_conlat_1(sK187))
| k6_conlat_1(sK187) = X0
| ~ m1_subset_1(k6_conlat_1(sK187),u1_struct_0(k11_conlat_1(sK187)))
| ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK187)))
| v3_struct_0(k11_conlat_1(sK187))
| ~ v4_lattices(k11_conlat_1(sK187))
| ~ l2_lattices(k11_conlat_1(sK187)) )
| ~ spl1342_162 ),
inference(resolution,[],[f42775,f28302]) ).
fof(f42883,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK187)))
| ~ r1_lattices(k11_conlat_1(sK187),X0,k6_conlat_1(sK187))
| k6_conlat_1(sK187) = X0
| ~ m1_subset_1(k6_conlat_1(sK187),u1_struct_0(k11_conlat_1(sK187)))
| v3_struct_0(k11_conlat_1(sK187))
| ~ v4_lattices(k11_conlat_1(sK187))
| ~ l2_lattices(k11_conlat_1(sK187)) )
| ~ spl1342_162 ),
inference(duplicate_literal_removal,[],[f42882]) ).
fof(f42885,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK187)))
| ~ r1_lattices(k11_conlat_1(sK187),X0,k6_conlat_1(sK187))
| k6_conlat_1(sK187) = X0
| v3_struct_0(k11_conlat_1(sK187))
| ~ v4_lattices(k11_conlat_1(sK187))
| ~ l2_lattices(k11_conlat_1(sK187)) )
| ~ spl1342_29
| spl1342_30
| ~ spl1342_162 ),
inference(forward_subsumption_resolution,[],[f42883,f40685]) ).
fof(f42887,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK187)))
| ~ r1_lattices(k11_conlat_1(sK187),X0,k6_conlat_1(sK187))
| k6_conlat_1(sK187) = X0
| ~ v4_lattices(k11_conlat_1(sK187))
| ~ l2_lattices(k11_conlat_1(sK187)) )
| ~ spl1342_29
| spl1342_30
| ~ spl1342_162 ),
inference(forward_subsumption_resolution,[],[f42885,f38788]) ).
fof(f42889,plain,
( ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK187)))
| ~ r1_lattices(k11_conlat_1(sK187),X0,k6_conlat_1(sK187))
| k6_conlat_1(sK187) = X0
| ~ v4_lattices(k11_conlat_1(sK187)) )
| ~ spl1342_29
| spl1342_30
| ~ spl1342_162 ),
inference(forward_subsumption_resolution,[],[f42887,f38931]) ).
fof(f42892,definition,
( spl1342_170
<=> v4_lattices(k11_conlat_1(sK187)) ),
introduced(definition,[new_symbols(definition,[spl1342_170])],[avatar_definition]) ).
fof(f42894,plain,
( ~ v4_lattices(k11_conlat_1(sK187))
| spl1342_170 ),
inference(avatar_component_clause,[],[f42892]) ).
fof(f42896,definition,
( spl1342_171
<=> ! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK187)))
| k6_conlat_1(sK187) = X0
| ~ r1_lattices(k11_conlat_1(sK187),X0,k6_conlat_1(sK187)) ) ),
introduced(definition,[new_symbols(definition,[spl1342_171])],[avatar_definition]) ).
fof(f42897,plain,
( ! [X0] :
( ~ r1_lattices(k11_conlat_1(sK187),X0,k6_conlat_1(sK187))
| k6_conlat_1(sK187) = X0
| ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK187))) )
| ~ spl1342_171 ),
inference(avatar_component_clause,[],[f42896]) ).
fof(f42898,plain,
( ~ spl1342_170
| spl1342_171
| ~ spl1342_29
| spl1342_30
| ~ spl1342_162 ),
inference(avatar_split_clause,[],[f42889,f42774,f38786,f38781,f42896,f42892]) ).
fof(f42938,plain,
( ~ sP0(sK187)
| spl1342_170 ),
inference(resolution,[],[f42894,f27207]) ).
fof(f42939,plain,
( $false
| spl1342_170 ),
inference(forward_subsumption_resolution,[],[f42938,f38741]) ).
fof(f42940,plain,
spl1342_170,
inference(avatar_contradiction_clause,[],[f42939]) ).
fof(f42942,plain,
( ! [X0] :
( k6_conlat_1(sK187) = k16_lattice3(k11_conlat_1(sK187),X0)
| ~ m1_subset_1(k16_lattice3(k11_conlat_1(sK187),X0),u1_struct_0(k11_conlat_1(sK187)))
| v3_struct_0(k11_conlat_1(sK187))
| ~ l3_lattices(k11_conlat_1(sK187))
| ~ m1_subset_1(k6_conlat_1(sK187),u1_struct_0(k11_conlat_1(sK187)))
| ~ r2_hidden(k6_conlat_1(sK187),X0)
| ~ v10_lattices(k11_conlat_1(sK187))
| ~ v4_lattice3(k11_conlat_1(sK187)) )
| ~ spl1342_171 ),
inference(resolution,[],[f42897,f42778]) ).
fof(f42944,plain,
( ! [X0] :
( k6_conlat_1(sK187) = k16_lattice3(k11_conlat_1(sK187),X0)
| v3_struct_0(k11_conlat_1(sK187))
| ~ l3_lattices(k11_conlat_1(sK187))
| ~ m1_subset_1(k6_conlat_1(sK187),u1_struct_0(k11_conlat_1(sK187)))
| ~ r2_hidden(k6_conlat_1(sK187),X0)
| ~ v10_lattices(k11_conlat_1(sK187))
| ~ v4_lattice3(k11_conlat_1(sK187)) )
| ~ spl1342_171 ),
inference(forward_subsumption_resolution,[],[f42942,f28018]) ).
fof(f42945,plain,
( ! [X0] :
( k6_conlat_1(sK187) = k16_lattice3(k11_conlat_1(sK187),X0)
| ~ l3_lattices(k11_conlat_1(sK187))
| ~ m1_subset_1(k6_conlat_1(sK187),u1_struct_0(k11_conlat_1(sK187)))
| ~ r2_hidden(k6_conlat_1(sK187),X0)
| ~ v10_lattices(k11_conlat_1(sK187))
| ~ v4_lattice3(k11_conlat_1(sK187)) )
| spl1342_30
| ~ spl1342_171 ),
inference(forward_subsumption_resolution,[],[f42944,f38788]) ).
fof(f42946,plain,
( ! [X0] :
( k6_conlat_1(sK187) = k16_lattice3(k11_conlat_1(sK187),X0)
| ~ m1_subset_1(k6_conlat_1(sK187),u1_struct_0(k11_conlat_1(sK187)))
| ~ r2_hidden(k6_conlat_1(sK187),X0)
| ~ v10_lattices(k11_conlat_1(sK187))
| ~ v4_lattice3(k11_conlat_1(sK187)) )
| ~ spl1342_29
| spl1342_30
| ~ spl1342_171 ),
inference(forward_subsumption_resolution,[],[f42945,f38783]) ).
fof(f42947,plain,
( ! [X0] :
( k6_conlat_1(sK187) = k16_lattice3(k11_conlat_1(sK187),X0)
| ~ r2_hidden(k6_conlat_1(sK187),X0)
| ~ v10_lattices(k11_conlat_1(sK187))
| ~ v4_lattice3(k11_conlat_1(sK187)) )
| ~ spl1342_29
| spl1342_30
| ~ spl1342_171 ),
inference(forward_subsumption_resolution,[],[f42946,f40685]) ).
fof(f42948,plain,
( ! [X0] :
( k6_conlat_1(sK187) = k16_lattice3(k11_conlat_1(sK187),X0)
| ~ r2_hidden(k6_conlat_1(sK187),X0)
| ~ v4_lattice3(k11_conlat_1(sK187)) )
| ~ spl1342_29
| spl1342_30
| ~ spl1342_49
| ~ spl1342_171 ),
inference(forward_subsumption_resolution,[],[f42947,f39057]) ).
fof(f42949,plain,
( ! [X0] :
( ~ r2_hidden(k6_conlat_1(sK187),X0)
| k6_conlat_1(sK187) = k16_lattice3(k11_conlat_1(sK187),X0) )
| ~ spl1342_29
| spl1342_30
| ~ spl1342_49
| ~ spl1342_63
| ~ spl1342_171 ),
inference(forward_subsumption_resolution,[],[f42948,f39872]) ).
fof(f42950,plain,
( k6_conlat_1(sK187) = k16_lattice3(k11_conlat_1(sK187),u1_struct_0(k11_conlat_1(sK187)))
| spl1342_27
| ~ spl1342_29
| spl1342_30
| ~ spl1342_49
| ~ spl1342_63
| ~ spl1342_171 ),
inference(resolution,[],[f42949,f40703]) ).
fof(f42962,plain,
( k6_conlat_1(sK187) = k2_conlat_2(sK187,u1_struct_0(k11_conlat_1(sK187)))
| spl1342_27
| ~ spl1342_29
| spl1342_30
| ~ spl1342_49
| ~ spl1342_63
| ~ spl1342_171 ),
inference(superposition,[],[f42950,f39134]) ).
fof(f42980,plain,
( $false
| spl1342_24
| spl1342_27
| ~ spl1342_29
| spl1342_30
| ~ spl1342_49
| ~ spl1342_63
| ~ spl1342_171 ),
inference(forward_subsumption_resolution,[],[f42962,f38714]) ).
fof(f42981,plain,
( spl1342_24
| spl1342_27
| ~ spl1342_29
| spl1342_30
| ~ spl1342_49
| ~ spl1342_63
| ~ spl1342_171 ),
inference(avatar_contradiction_clause,[],[f42980]) ).
cnf(s19,plain,
( ~ spl1342_23
| ~ spl1342_24 ),
inference(sat_conversion,[],[f38715]) ).
cnf(s24,plain,
( spl1342_28
| ~ spl1342_29 ),
inference(sat_conversion,[],[f38791]) ).
cnf(s25,plain,
spl1342_29,
inference(sat_conversion,[],[f38795]) ).
cnf(s35,plain,
( ~ spl1342_26
| ~ spl1342_29
| spl1342_30 ),
inference(sat_conversion,[],[f39049]) ).
cnf(s40,plain,
~ spl1342_30,
inference(sat_conversion,[],[f39072]) ).
cnf(s43,plain,
( ~ spl1342_27
| ~ spl1342_29
| spl1342_30 ),
inference(sat_conversion,[],[f39212]) ).
cnf(s45,plain,
( spl1342_49
| ~ spl1342_53 ),
inference(sat_conversion,[],[f39321]) ).
cnf(s46,plain,
spl1342_31,
inference(sat_conversion,[],[f39374]) ).
cnf(s50,plain,
( spl1342_26
| ~ spl1342_28
| ~ spl1342_31
| spl1342_53 ),
inference(sat_conversion,[],[f39408]) ).
cnf(s55,plain,
spl1342_55,
inference(sat_conversion,[],[f39594]) ).
cnf(s63,plain,
spl1342_63,
inference(sat_conversion,[],[f39887]) ).
cnf(s65,plain,
( spl1342_23
| ~ spl1342_29
| spl1342_30
| ~ spl1342_49
| ~ spl1342_63 ),
inference(sat_conversion,[],[f39954]) ).
cnf(s146,plain,
( ~ spl1342_29
| spl1342_30
| ~ spl1342_49
| ~ spl1342_55
| spl1342_162 ),
inference(sat_conversion,[],[f42877]) ).
cnf(s149,plain,
( ~ spl1342_29
| spl1342_30
| ~ spl1342_162
| ~ spl1342_170
| spl1342_171 ),
inference(sat_conversion,[],[f42898]) ).
cnf(s153,plain,
spl1342_170,
inference(sat_conversion,[],[f42940]) ).
cnf(s156,plain,
( spl1342_24
| spl1342_27
| ~ spl1342_29
| spl1342_30
| ~ spl1342_49
| ~ spl1342_63
| ~ spl1342_171 ),
inference(sat_conversion,[],[f42981]) ).
cnf(s157,plain,
( ~ spl1342_29
| spl1342_30
| ~ spl1342_162
| spl1342_171 ),
inference(rat,[],[s149,s153]) ).
cnf(s162,plain,
( ~ spl1342_26
| ~ spl1342_29 ),
inference(rat,[],[s35,s40]) ).
cnf(s165,plain,
~ spl1342_27,
inference(rat,[],[s43,s40,s25]) ).
cnf(s166,plain,
~ spl1342_26,
inference(rat,[],[s162,s25]) ).
cnf(s168,plain,
spl1342_28,
inference(rat,[],[s24,s25]) ).
cnf(s170,plain,
spl1342_53,
inference(rat,[],[s50,s166,s46,s168]) ).
cnf(s173,plain,
spl1342_49,
inference(rat,[],[s45,s170]) ).
cnf(s174,plain,
spl1342_162,
inference(rat,[],[s146,s25,s55,s40,s173]) ).
cnf(s184,plain,
spl1342_23,
inference(rat,[],[s65,s63,s25,s40,s173]) ).
cnf(s185,plain,
spl1342_171,
inference(rat,[],[s157,s25,s40,s174]) ).
cnf(s191,plain,
spl1342_24,
inference(rat,[],[s156,s173,s63,s165,s40,s25,s185]) ).
cnf(s198,plain,
$false,
inference(rat,[],[s19,s191,s184]) ).
fof(f42992,plain,
$false,
inference(avatar_sat_refutation,[],[s198]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT340+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.15/0.43 % Computer : n006.cluster.edu
% 0.15/0.43 % Model : x86_64 x86_64
% 0.15/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.43 % Memory : 8046.5625MB
% 0.15/0.43 % OS : Linux 6.8.0-71-generic
% 0.15/0.43 % CPULimit : 300
% 0.15/0.43 % WCLimit : 300
% 0.15/0.43 % DateTime : Sun Sep 27 14:47:59 UTC 2026
% 0.15/0.43 % CPUTime :
% 0.15/0.43 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.22/0.49 Running first-order theorem proving
% 0.22/0.49 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 21.76/5.19 % (3058729)Detected formulas, will run a generic FOF schedule.
% 21.76/5.19 % (3058745)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=95925943:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2987 on theBenchmark for (2987ds/134677Mi)
% 21.76/5.19 % (3058750)dis-21_1_sil=8000:lcm=predicate:random_seed=4287771373:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2987 on theBenchmark for (2987ds/129Mi)
% 21.76/5.19 % (3058748)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1961485323:i=119:av=off:ss=axioms_2987 on theBenchmark for (2987ds/119Mi)
% 21.76/5.19 % (3058749)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1087220220:s2a=on:i=139:gtg=position_2987 on theBenchmark for (2987ds/139Mi)
% 21.76/5.19 % (3058747)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1407419277:i=109:sd=1:ins=1:gsp=on:ss=axioms_2987 on theBenchmark for (2987ds/109Mi)
% 21.76/5.19 % (3058746)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=1313872863:i=141695:sd=1:nm=32:gsp=on:ss=included_2987 on theBenchmark for (2987ds/141695Mi)
% 21.76/5.19 % (3058744)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=4080173347:i=141193_2987 on theBenchmark for (2987ds/141193Mi)
% 21.76/5.19 % (3058750)Instruction limit reached!
% 21.76/5.19 % (3058750)------------------------------
% 21.76/5.19 % (3058750)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.76/5.19 % (3058750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.76/5.19 % (3058750)CaDiCaL version: 2.1.3
% 21.76/5.19 % (3058750)Termination reason: Instruction limit
% 21.76/5.19 % (3058750)Termination phase: SInE selection
% 21.76/5.19 % (3058750)Time elapsed: 0.071 s
% 21.76/5.19 % (3058750)Peak memory usage: 111 MB
% 21.76/5.19 % (3058750)Instructions burned: 130 (million)
% 21.76/5.19 % (3058749)Instruction limit reached!
% 21.76/5.19 % (3058749)------------------------------
% 21.76/5.19 % (3058749)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.76/5.19 % (3058749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.76/5.19 % (3058749)CaDiCaL version: 2.1.3
% 21.76/5.19 % (3058749)Termination reason: Instruction limit
% 21.76/5.19 % (3058749)Termination phase: Property scanning
% 21.76/5.19 % (3058749)Time elapsed: 0.110 s
% 21.76/5.19 % (3058749)Peak memory usage: 110 MB
% 21.76/5.19 % (3058749)Instructions burned: 140 (million)
% 21.76/5.19 % (3058747)Instruction limit reached!
% 21.76/5.19 % (3058747)------------------------------
% 21.76/5.19 % (3058747)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.76/5.19 % (3058747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.76/5.19 % (3058747)CaDiCaL version: 2.1.3
% 21.76/5.19 % (3058747)Termination reason: Instruction limit
% 21.76/5.19 % (3058747)Termination phase: Property scanning
% 21.76/5.19 % (3058747)Time elapsed: 0.130 s
% 21.76/5.19 % (3058747)Peak memory usage: 112 MB
% 21.76/5.19 % (3058747)Instructions burned: 109 (million)
% 21.76/5.19 % (3058748)Instruction limit reached!
% 21.76/5.19 % (3058748)------------------------------
% 21.76/5.19 % (3058748)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.76/5.19 % (3058748)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.76/5.19 % (3058748)CaDiCaL version: 2.1.3
% 21.76/5.19 % (3058748)Termination reason: Instruction limit
% 21.76/5.19 % (3058748)Termination phase: Preprocessing 1
% 21.76/5.19 % (3058748)Time elapsed: 0.142 s
% 21.76/5.19 % (3058748)Peak memory usage: 111 MB
% 21.76/5.19 % (3058748)Instructions burned: 119 (million)
% 21.76/5.19 % (3058758)lrs+10_1_sil=8000:sp=occurrence:random_seed=1901577925:i=285:sd=3:ss=axioms:sgt=8_2984 on theBenchmark for (2984ds/285Mi)
% 21.76/5.19 % (3058759)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1457764502:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2983 on theBenchmark for (2983ds/157Mi)
% 21.76/5.19 % (3058759)Instruction limit reached!
% 21.76/5.19 % (3058759)------------------------------
% 21.76/5.19 % (3058759)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.76/5.19 % (3058759)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.76/5.19 % (3058759)CaDiCaL version: 2.1.3
% 21.76/5.19 % (3058759)Termination reason: Instruction limit
% 33.41/6.99 % (3058759)Termination phase: Property scanning
% 33.41/6.99 % (3058759)Time elapsed: 0.072 s
% 33.41/6.99 % (3058759)Peak memory usage: 111 MB
% 33.41/6.99 % (3058759)Instructions burned: 159 (million)
% 33.41/6.99 % (3058760)lrs+1011_1_sil=32000:sp=occurrence:random_seed=416890732:i=325:sd=1:ss=axioms:sgt=32_2983 on theBenchmark for (2983ds/325Mi)
% 33.41/6.99 % (3058761)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=1816611299:s2a=on:i=248:s2at=1.23:gtg=position_2983 on theBenchmark for (2983ds/248Mi)
% 33.41/6.99 % (3058758)Instruction limit reached!
% 33.41/6.99 % (3058758)------------------------------
% 33.41/6.99 % (3058758)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.41/6.99 % (3058758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.41/6.99 % (3058758)CaDiCaL version: 2.1.3
% 33.41/6.99 % (3058758)Termination reason: Instruction limit
% 33.41/6.99 % (3058758)Termination phase: Saturation
% 33.41/6.99 % (3058758)Time elapsed: 0.213 s
% 33.41/6.99 % (3058758)Peak memory usage: 117 MB
% 33.41/6.99 % (3058758)Instructions burned: 286 (million)
% 33.41/6.99 % (3058761)Instruction limit reached!
% 33.41/6.99 % (3058761)------------------------------
% 33.41/6.99 % (3058761)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.41/6.99 % (3058761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.41/6.99 % (3058761)CaDiCaL version: 2.1.3
% 33.41/6.99 % (3058761)Termination reason: Instruction limit
% 33.41/6.99 % (3058761)Termination phase: Property scanning
% 33.41/6.99 % (3058761)Time elapsed: 0.184 s
% 33.41/6.99 % (3058761)Peak memory usage: 110 MB
% 33.41/6.99 % (3058761)Instructions burned: 249 (million)
% 33.41/6.99 % (3058764)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1248324391:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2981 on theBenchmark for (2981ds/294Mi)
% 33.41/6.99 % (3058767)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3169514891:i=2350_2980 on theBenchmark for (2980ds/2350Mi)
% 33.41/6.99 % (3058760)Instruction limit reached!
% 33.41/6.99 % (3058760)------------------------------
% 33.41/6.99 % (3058760)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.41/6.99 % (3058760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.41/6.99 % (3058760)CaDiCaL version: 2.1.3
% 33.41/6.99 % (3058760)Termination reason: Instruction limit
% 33.41/6.99 % (3058760)Termination phase: Saturation
% 33.41/6.99 % (3058760)Time elapsed: 0.342 s
% 33.41/6.99 % (3058760)Peak memory usage: 117 MB
% 33.41/6.99 % (3058760)Instructions burned: 326 (million)
% 33.41/6.99 % (3058768)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1528957025:cts=off:i=113:fsr=off:ss=included:sgt=4_2978 on theBenchmark for (2978ds/113Mi)
% 33.41/6.99 % (3058768)Instruction limit reached!
% 33.41/6.99 % (3058768)------------------------------
% 33.41/6.99 % (3058768)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.41/6.99 % (3058768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.41/6.99 % (3058768)CaDiCaL version: 2.1.3
% 33.41/6.99 % (3058768)Termination reason: Instruction limit
% 33.41/6.99 % (3058768)Termination phase: Preprocessing 1
% 33.41/6.99 % (3058768)Time elapsed: 0.153 s
% 33.41/6.99 % (3058768)Peak memory usage: 111 MB
% 33.41/6.99 % (3058768)Instructions burned: 113 (million)
% 33.41/6.99 % (3058764)Instruction limit reached!
% 33.41/6.99 % (3058764)------------------------------
% 33.41/6.99 % (3058764)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.41/6.99 % (3058764)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.41/6.99 % (3058764)CaDiCaL version: 2.1.3
% 33.41/6.99 % (3058764)Termination reason: Instruction limit
% 33.41/6.99 % (3058764)Termination phase: Saturation
% 33.41/6.99 % (3058764)Time elapsed: 0.309 s
% 33.41/6.99 % (3058764)Peak memory usage: 117 MB
% 33.41/6.99 % (3058764)Instructions burned: 295 (million)
% 33.41/6.99 % (3058771)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3346256615:i=127:av=off:fsr=off:sup=off_2977 on theBenchmark for (2977ds/127Mi)
% 33.41/6.99 % (3058771)Instruction limit reached!
% 33.41/6.99 % (3058771)------------------------------
% 33.41/6.99 % (3058771)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 33.41/6.99 % (3058771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 33.41/6.99 % (3058771)CaDiCaL version: 2.1.3
% 58.75/11.39 % (3058771)Termination reason: Instruction limit
% 58.75/11.39 % (3058771)Termination phase: Preprocessing 1
% 58.75/11.39 % (3058771)Time elapsed: 0.139 s
% 58.75/11.39 % (3058771)Peak memory usage: 111 MB
% 58.75/11.39 % (3058771)Instructions burned: 128 (million)
% 58.75/11.39 % (3058775)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2312483434:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2975 on theBenchmark for (2975ds/114Mi)
% 58.75/11.39 % (3058776)lrs+10_1_sil=8000:sp=occurrence:random_seed=2548644123:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2974 on theBenchmark for (2974ds/907Mi)
% 58.75/11.39 % (3058775)Instruction limit reached!
% 58.75/11.39 % (3058775)------------------------------
% 58.75/11.39 % (3058775)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.75/11.39 % (3058775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.75/11.39 % (3058775)CaDiCaL version: 2.1.3
% 58.75/11.39 % (3058775)Termination reason: Instruction limit
% 58.75/11.39 % (3058775)Termination phase: Property scanning
% 58.75/11.39 % (3058775)Time elapsed: 0.095 s
% 58.75/11.39 % (3058775)Peak memory usage: 111 MB
% 58.75/11.39 % (3058775)Instructions burned: 114 (million)
% 58.75/11.40 % (3058778)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=896280505:i=437:sd=1:aac=none:ss=included_2972 on theBenchmark for (2972ds/437Mi)
% 58.75/11.40 % (3058781)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1270702573:i=5202:ss=axioms:sgt=16_2971 on theBenchmark for (2971ds/5202Mi)
% 58.75/11.40 % (3058778)Refutation not found, incomplete strategy
% 58.75/11.40 % (3058778)------------------------------
% 58.75/11.40 % (3058778)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.75/11.40 % (3058778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.75/11.40 % (3058778)CaDiCaL version: 2.1.3
% 58.75/11.40 % (3058778)Termination reason: Refutation not found, incomplete strategy
% 58.75/11.40 % (3058778)Time elapsed: 0.134 s
% 58.75/11.40 % (3058778)Peak memory usage: 115 MB
% 58.75/11.40 % (3058778)Instructions burned: 132 (million)
% 58.75/11.40 % (3058767)Instruction limit reached!
% 58.75/11.40 % (3058767)------------------------------
% 58.75/11.40 % (3058767)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.75/11.40 % (3058767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.75/11.40 % (3058767)CaDiCaL version: 2.1.3
% 58.75/11.40 % (3058767)Termination reason: Instruction limit
% 58.75/11.40 % (3058767)Termination phase: Saturation
% 58.75/11.40 % (3058767)Time elapsed: 1.172 s
% 58.75/11.40 % (3058767)Peak memory usage: 164 MB
% 58.75/11.40 % (3058767)Instructions burned: 2351 (million)
% 58.75/11.40 % (3058778)------------------------------
% 58.75/11.40 % (3058778)------------------------------
% 58.75/11.40 % (3058776)Instruction limit reached!
% 58.75/11.40 % (3058776)------------------------------
% 58.75/11.40 % (3058776)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.75/11.40 % (3058776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.75/11.40 % (3058776)CaDiCaL version: 2.1.3
% 58.75/11.40 % (3058776)Termination reason: Instruction limit
% 58.75/11.40 % (3058776)Termination phase: Saturation
% 58.75/11.40 % (3058776)Time elapsed: 0.885 s
% 58.75/11.40 % (3058776)Peak memory usage: 131 MB
% 58.75/11.40 % (3058776)Instructions burned: 907 (million)
% 58.75/11.40 % (3058786)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1378260304:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2965 on theBenchmark for (2965ds/134Mi)
% 58.75/11.40 % (3058787)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3767945591:st=8:i=592:sd=3:ep=RST:ss=axioms_2964 on theBenchmark for (2964ds/592Mi)
% 58.75/11.40 % (3058786)Instruction limit reached!
% 58.75/11.40 % (3058786)------------------------------
% 58.75/11.40 % (3058786)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.75/11.40 % (3058786)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.75/11.40 % (3058786)CaDiCaL version: 2.1.3
% 58.75/11.40 % (3058786)Termination reason: Instruction limit
% 58.75/11.40 % (3058786)Termination phase: NewCNF
% 58.75/11.40 % (3058786)Time elapsed: 0.177 s
% 58.75/11.40 % (3058786)Peak memory usage: 113 MB
% 58.75/11.40 % (3058786)Instructions burned: 134 (million)
% 58.75/11.40 % (3058789)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=789645800:st=3:i=13193:sd=3:ss=axioms_2963 on theBenchmark for (2963ds/13193Mi)
% 58.75/11.40 % (3058791)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=3652294360:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2961 on theBenchmark for (2961ds/125Mi)
% 58.75/11.40 % (3058791)Instruction limit reached!
% 58.75/11.40 % (3058791)------------------------------
% 58.75/11.40 % (3058791)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.75/11.40 % (3058791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.75/11.40 % (3058791)CaDiCaL version: 2.1.3
% 58.75/11.40 % (3058791)Termination reason: Instruction limit
% 58.75/11.40 % (3058791)Termination phase: Property scanning
% 58.75/11.40 % (3058791)Time elapsed: 0.111 s
% 58.75/11.40 % (3058791)Peak memory usage: 110 MB
% 58.75/11.40 % (3058791)Instructions burned: 125 (million)
% 58.75/11.40 % (3058794)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1894471991:i=134:gtgl=5:slsql=off:gtg=exists_sym_2957 on theBenchmark for (2957ds/134Mi)
% 58.75/11.40 % (3058787)Instruction limit reached!
% 58.75/11.40 % (3058787)------------------------------
% 58.75/11.40 % (3058787)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.75/11.40 % (3058787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.75/11.40 % (3058787)CaDiCaL version: 2.1.3
% 58.75/11.40 % (3058787)Termination reason: Instruction limit
% 58.75/11.40 % (3058787)Termination phase: Clausification
% 58.75/11.40 % (3058787)Time elapsed: 0.689 s
% 58.75/11.40 % (3058787)Peak memory usage: 133 MB
% 58.75/11.40 % (3058787)Instructions burned: 592 (million)
% 58.75/11.40 % (3058794)Instruction limit reached!
% 58.75/11.40 % (3058794)------------------------------
% 58.75/11.40 % (3058794)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.75/11.40 % (3058794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.75/11.40 % (3058794)CaDiCaL version: 2.1.3
% 58.75/11.40 % (3058794)Termination reason: Instruction limit
% 58.75/11.40 % (3058794)Termination phase: Property scanning
% 58.75/11.40 % (3058794)Time elapsed: 0.113 s
% 58.75/11.40 % (3058794)Peak memory usage: 110 MB
% 58.75/11.40 % (3058794)Instructions burned: 134 (million)
% 58.75/11.40 % (3058796)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=458074490:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2954 on theBenchmark for (2954ds/141Mi)
% 58.75/11.40 % (3058797)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=2111372150:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2953 on theBenchmark for (2953ds/431Mi)
% 58.75/11.40 % (3058796)Refutation not found, incomplete strategy
% 58.75/11.40 % (3058796)------------------------------
% 58.75/11.40 % (3058796)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.75/11.40 % (3058796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.75/11.40 % (3058796)CaDiCaL version: 2.1.3
% 58.75/11.40 % (3058796)Termination reason: Refutation not found, incomplete strategy
% 58.75/11.40 % (3058796)Time elapsed: 0.146 s
% 58.75/11.40 % (3058796)Peak memory usage: 115 MB
% 58.75/11.40 % (3058796)Instructions burned: 114 (million)
% 58.75/11.40 % (3058797)Refutation not found, incomplete strategy
% 58.75/11.40 % (3058797)------------------------------
% 58.75/11.40 % (3058797)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.75/11.40 % (3058797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.75/11.40 % (3058797)CaDiCaL version: 2.1.3
% 58.75/11.40 % (3058797)Termination reason: Refutation not found, incomplete strategy
% 58.75/11.40 % (3058797)Time elapsed: 0.151 s
% 58.75/11.40 % (3058797)Peak memory usage: 116 MB
% 58.75/11.40 % (3058797)Instructions burned: 116 (million)
% 58.75/11.40 % (3058796)------------------------------
% 58.75/11.40 % (3058796)------------------------------
% 58.75/11.40 % (3058797)------------------------------
% 58.75/11.40 % (3058797)------------------------------
% 58.75/11.40 % (3058800)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=512566118:i=6060:aac=none:ins=25_2946 on theBenchmark for (2946ds/6060Mi)
% 58.75/11.40 % (3058801)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=3357285145:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2945 on theBenchmark for (2945ds/150Mi)
% 58.75/11.40 % (3058801)Instruction limit reached!
% 58.75/11.40 % (3058801)------------------------------
% 58.75/11.40 % (3058801)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.75/11.40 % (3058801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.75/11.40 % (3058801)CaDiCaL version: 2.1.3
% 58.75/11.40 % (3058801)Termination reason: Instruction limit
% 58.75/11.40 % (3058801)Termination phase: Preprocessing 1
% 58.75/11.40 % (3058801)Time elapsed: 0.182 s
% 58.75/11.40 % (3058801)Peak memory usage: 111 MB
% 58.75/11.40 % (3058801)Instructions burned: 151 (million)
% 58.75/11.40 % (3058806)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=2636266316:i=14155:bd=all_2940 on theBenchmark for (2940ds/14155Mi)
% 58.75/11.40 % (3058781)Instruction limit reached!
% 58.75/11.40 % (3058781)------------------------------
% 58.75/11.40 % (3058781)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.75/11.40 % (3058781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.75/11.40 % (3058781)CaDiCaL version: 2.1.3
% 58.75/11.40 % (3058781)Termination reason: Instruction limit
% 58.75/11.40 % (3058781)Termination phase: Saturation
% 58.75/11.40 % (3058781)Time elapsed: 6.207 s
% 58.75/11.40 % (3058781)Peak memory usage: 585 MB
% 58.75/11.40 % (3058781)Instructions burned: 5202 (million)
% 58.75/11.40 % (3058814)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=2498795835:i=667:av=off:fsr=off_2905 on theBenchmark for (2905ds/667Mi)
% 58.75/11.40 % (3058789)First to succeed.
% 58.75/11.40 % (3058789)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3058729"
% 58.75/11.40 % (3058789)Refutation found. Thanks to Tanya!
% 58.75/11.40 % SZS status Theorem for theBenchmark
% 58.75/11.40 % SZS output start Proof for theBenchmark
% See solution above
% 66.04/11.69 % (3058789)------------------------------
% 66.04/11.69 % (3058789)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 66.04/11.69 % (3058789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.04/11.69 % (3058789)CaDiCaL version: 2.1.3
% 66.04/11.69 % (3058789)Termination reason: Refutation
% 66.04/11.69 % (3058789)Time elapsed: 5.927 s
% 66.04/11.69 % (3058789)Peak memory usage: 259 MB
% 66.04/11.69 % (3058789)Instructions burned: 5915 (million)
% 66.04/11.69 % (3058789)------------------------------
% 66.04/11.69 % (3058789)------------------------------
% 66.04/11.69 % (3058729)Success in time 10.346 s
% 66.04/11.69 % Vampire exiting
%------------------------------------------------------------------------------