%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT340+4 : 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 : n007.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 22.55s 9.77s
% Output : Refutation 52.08s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 34
% Syntax : Number of formulae : 251 ( 39 unt; 9 def)
% Number of atoms : 982 ( 106 equ)
% Maximal formula atoms : 15 ( 3 avg)
% Number of connectives : 1130 ( 399 ~; 487 |; 197 &)
% ( 15 <=>; 32 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 5 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 32 ( 30 usr; 10 prp; 0-3 aty)
% Number of functors : 16 ( 16 usr; 1 con; 0-2 aty)
% Number of variables : 215 ( 0 sgn 213 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f482,axiom,
! [X0] : k2_subset_1(X0) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d4_subset_1) ).
fof(f564,axiom,
! [X0] : m1_subset_1(k2_subset_1(X0),k1_zfmisc_1(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k2_subset_1) ).
fof(f675,axiom,
! [X0,X1] :
( r2_hidden(X0,X1)
=> m1_subset_1(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t1_subset) ).
fof(f21512,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_filter_0(X1,X0)
=> ( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v14_lattices(X0)
& l3_lattices(X0) )
=> r2_hidden(k6_lattices(X0),X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t12_filter_0) ).
fof(f21515,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(f22747,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(f22752,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(f22780,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l3_lattices(X0) )
=> ( u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0))
& u2_lattices(X0) = u1_lattices(k1_lattice2(X0))
& u1_lattices(X0) = u2_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t18_lattice2) ).
fof(f22781,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(f22827,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ( v13_lattices(X0)
<=> v14_lattices(k1_lattice2(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t63_lattice2) ).
fof(f22842,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v13_lattices(X0)
& l3_lattices(X0) )
=> k5_lattices(X0) = k6_lattices(k1_lattice2(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t78_lattice2) ).
fof(f22852,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(f28659,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(f28669,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(f28694,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(f33228,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,X1,k5_lattices(X0))
=> r1_boolealg(X0,X1,k5_lattices(X0)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t25_boolealg) ).
fof(f33294,axiom,
! [X0,X1,X2] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0)
& m1_subset_1(X1,u1_struct_0(X0))
& m1_subset_1(X2,u1_struct_0(X0)) )
=> ( r1_boolealg(X0,X1,X2)
<=> X1 = X2 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_r1_boolealg) ).
fof(f46212,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)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc4_conlat_1) ).
fof(f46213,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))
& v4_lattice3(k11_conlat_1(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc5_conlat_1) ).
fof(f46277,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(f49794,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(f49795,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(f49799,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(f49800,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(f49802,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(f49803,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)],[f49802]) ).
fof(f49946,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,[],[f49794]) ).
fof(f49947,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,[],[f49946]) ).
fof(f49948,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,[],[f49795]) ).
fof(f49949,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,[],[f49948]) ).
fof(f49956,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,[],[f49799]) ).
fof(f49957,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,[],[f49956]) ).
fof(f49958,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,[],[f49800]) ).
fof(f49959,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,[],[f49958]) ).
fof(f49962,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,[],[f49803]) ).
fof(f49963,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,[],[f49962]) ).
fof(f49972,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,[],[f46277]) ).
fof(f49973,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,[],[f49972]) ).
fof(f49974,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))
& v4_lattice3(k11_conlat_1(X0)) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(ennf_transformation,[],[f46213]) ).
fof(f49975,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))
& v4_lattice3(k11_conlat_1(X0)) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(flattening,[],[f49974]) ).
fof(f49976,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)) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(ennf_transformation,[],[f46212]) ).
fof(f49977,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)) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(flattening,[],[f49976]) ).
fof(f50008,plain,
! [X0] :
( ( v3_lattices(k1_lattice2(X0))
& l3_lattices(k1_lattice2(X0)) )
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f22852]) ).
fof(f50013,plain,
! [X0] :
( k5_lattices(X0) = k6_lattices(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v13_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f22842]) ).
fof(f50014,plain,
! [X0] :
( k5_lattices(X0) = k6_lattices(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v13_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f50013]) ).
fof(f50019,plain,
! [X0] :
( ( v13_lattices(X0)
<=> v14_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f22827]) ).
fof(f50020,plain,
! [X0] :
( ( v13_lattices(X0)
<=> v14_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f50019]) ).
fof(f50027,plain,
! [X0] :
( k1_lattice2(k1_lattice2(X0)) = X0
| v3_struct_0(X0)
| ~ v3_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f22781]) ).
fof(f50028,plain,
! [X0] :
( k1_lattice2(k1_lattice2(X0)) = X0
| v3_struct_0(X0)
| ~ v3_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f50027]) ).
fof(f50029,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,[],[f22780]) ).
fof(f50030,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,[],[f50029]) ).
fof(f50032,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,[],[f22752]) ).
fof(f50033,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,[],[f50032]) ).
fof(f50034,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f22747]) ).
fof(f50035,plain,
! [X0] :
( ( ~ v3_struct_0(k1_lattice2(X0))
& v3_lattices(k1_lattice2(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f50034]) ).
fof(f50076,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,[],[f28669]) ).
fof(f50077,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,[],[f50076]) ).
fof(f50088,plain,
! [X0] :
( ! [X1] :
( r2_hidden(k6_lattices(X0),X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v14_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f21512]) ).
fof(f50089,plain,
! [X0] :
( ! [X1] :
( r2_hidden(k6_lattices(X0),X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v14_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f50088]) ).
fof(f50198,plain,
! [X0,X1] :
( m1_subset_1(k16_lattice3(X0,X1),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f28694]) ).
fof(f50199,plain,
! [X0,X1] :
( m1_subset_1(k16_lattice3(X0,X1),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f50198]) ).
fof(f50206,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,[],[f28659]) ).
fof(f50207,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,[],[f50206]) ).
fof(f50261,plain,
! [X0,X1] :
( m1_subset_1(X0,X1)
| ~ r2_hidden(X0,X1) ),
inference(ennf_transformation,[],[f675]) ).
fof(f50411,plain,
! [X0] :
( m1_filter_0(u1_struct_0(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f21515]) ).
fof(f50412,plain,
! [X0] :
( m1_filter_0(u1_struct_0(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f50411]) ).
fof(f56306,plain,
! [X0,X1,X2] :
( ( r1_boolealg(X0,X1,X2)
<=> X1 = X2 )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f33294]) ).
fof(f56307,plain,
! [X0,X1,X2] :
( ( r1_boolealg(X0,X1,X2)
<=> X1 = X2 )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(flattening,[],[f56306]) ).
fof(f56320,plain,
! [X0] :
( ! [X1] :
( r1_boolealg(X0,X1,k5_lattices(X0))
| ~ r3_lattices(X0,X1,k5_lattices(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v13_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f33228]) ).
fof(f56321,plain,
! [X0] :
( ! [X1] :
( r1_boolealg(X0,X1,k5_lattices(X0))
| ~ r3_lattices(X0,X1,k5_lattices(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v13_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f56320]) ).
fof(f59368,plain,
( ( k5_conlat_1(sK56) != k3_conlat_2(sK56,k2_subset_1(u1_struct_0(k11_conlat_1(sK56))))
| k6_conlat_1(sK56) != k2_conlat_2(sK56,k2_subset_1(u1_struct_0(k11_conlat_1(sK56)))) )
& ~ v3_conlat_1(sK56)
& l2_conlat_1(sK56) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK56]),skolemize(X0,sK56)],[f49963]) ).
fof(f59401,plain,
! [X0] :
( ( ( v13_lattices(X0)
| ~ v14_lattices(k1_lattice2(X0)) )
& ( v14_lattices(k1_lattice2(X0))
| ~ v13_lattices(X0) ) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f50020]) ).
fof(f61268,plain,
! [X0,X1,X2] :
( ( ( r1_boolealg(X0,X1,X2)
| X1 != X2 )
& ( X1 = X2
| ~ r1_boolealg(X0,X1,X2) ) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(nnf_transformation,[],[f56307]) ).
fof(f62031,plain,
! [X0] :
( v13_lattices(k11_conlat_1(X0))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f49947]) ).
fof(f62041,plain,
! [X0] :
( ~ l2_conlat_1(X0)
| v3_conlat_1(X0)
| k5_conlat_1(X0) = k6_lattices(k11_conlat_1(X0)) ),
inference(cnf_transformation,[],[f49949]) ).
fof(f62042,plain,
! [X0] :
( ~ l2_conlat_1(X0)
| v3_conlat_1(X0)
| k6_conlat_1(X0) = k5_lattices(k11_conlat_1(X0)) ),
inference(cnf_transformation,[],[f49949]) ).
fof(f62051,plain,
! [X0,X1] :
( ~ l2_conlat_1(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(k11_conlat_1(X0))))
| v3_conlat_1(X0)
| k2_conlat_2(X0,X1) = k16_lattice3(k11_conlat_1(X0),X1) ),
inference(cnf_transformation,[],[f49957]) ).
fof(f62052,plain,
! [X0,X1] :
( ~ l2_conlat_1(X0)
| ~ m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(k11_conlat_1(X0))))
| v3_conlat_1(X0)
| k3_conlat_2(X0,X1) = k15_lattice3(k11_conlat_1(X0),X1) ),
inference(cnf_transformation,[],[f49959]) ).
fof(f62055,plain,
l2_conlat_1(sK56),
inference(cnf_transformation,[],[f59368]) ).
fof(f62056,plain,
~ v3_conlat_1(sK56),
inference(cnf_transformation,[],[f59368]) ).
fof(f62057,plain,
( k5_conlat_1(sK56) != k3_conlat_2(sK56,k2_subset_1(u1_struct_0(k11_conlat_1(sK56))))
| k6_conlat_1(sK56) != k2_conlat_2(sK56,k2_subset_1(u1_struct_0(k11_conlat_1(sK56)))) ),
inference(cnf_transformation,[],[f59368]) ).
fof(f62074,plain,
! [X0] :
( l3_lattices(k11_conlat_1(X0))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f49973]) ).
fof(f62077,plain,
! [X0] :
( v4_lattice3(k11_conlat_1(X0))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f49975]) ).
fof(f62087,plain,
! [X0] :
( v10_lattices(k11_conlat_1(X0))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f49977]) ).
fof(f62094,plain,
! [X0] :
( v3_lattices(k11_conlat_1(X0))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f49977]) ).
fof(f62095,plain,
! [X0] :
( ~ v3_struct_0(k11_conlat_1(X0))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f49977]) ).
fof(f62151,plain,
! [X0] :
( ~ l3_lattices(X0)
| l3_lattices(k1_lattice2(X0)) ),
inference(cnf_transformation,[],[f50008]) ).
fof(f62156,plain,
! [X0] :
( ~ v13_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| k5_lattices(X0) = k6_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f50014]) ).
fof(f62167,plain,
! [X0] :
( ~ v13_lattices(X0)
| v14_lattices(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f59401]) ).
fof(f62173,plain,
! [X0] :
( ~ v3_lattices(X0)
| v3_struct_0(X0)
| k1_lattice2(k1_lattice2(X0)) = X0
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f50028]) ).
fof(f62176,plain,
! [X0] :
( ~ l3_lattices(X0)
| v3_struct_0(X0)
| u1_struct_0(X0) = u1_struct_0(k1_lattice2(X0)) ),
inference(cnf_transformation,[],[f50030]) ).
fof(f62178,plain,
! [X0] :
( ~ v10_lattices(X0)
| v3_struct_0(X0)
| v10_lattices(k1_lattice2(X0))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f50033]) ).
fof(f62188,plain,
! [X0] :
( ~ v3_struct_0(k1_lattice2(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f50035]) ).
fof(f62328,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,[],[f50077]) ).
fof(f62340,plain,
! [X0,X1] :
( r2_hidden(k6_lattices(X0),X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v14_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_filter_0(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f50089]) ).
fof(f62530,plain,
! [X0,X1] :
( ~ l3_lattices(X0)
| v3_struct_0(X0)
| m1_subset_1(k16_lattice3(X0,X1),u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f50199]) ).
fof(f62537,plain,
! [X2,X0,X1] :
( ~ v4_lattice3(X0)
| ~ r2_hidden(X1,X2)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| r3_lattices(X0,k16_lattice3(X0,X2),X1)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f50207]) ).
fof(f62615,plain,
! [X0] : m1_subset_1(k2_subset_1(X0),k1_zfmisc_1(X0)),
inference(cnf_transformation,[],[f564]) ).
fof(f62622,plain,
! [X0] : k2_subset_1(X0) = X0,
inference(cnf_transformation,[],[f482]) ).
fof(f62628,plain,
! [X0,X1] :
( ~ r2_hidden(X0,X1)
| m1_subset_1(X0,X1) ),
inference(cnf_transformation,[],[f50261]) ).
fof(f62913,plain,
! [X0] :
( m1_filter_0(u1_struct_0(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f50412]) ).
fof(f71465,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ r1_boolealg(X0,X1,X2)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| X1 = X2 ),
inference(cnf_transformation,[],[f61268]) ).
fof(f71475,plain,
! [X0,X1] :
( ~ v13_lattices(X0)
| ~ r3_lattices(X0,X1,k5_lattices(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| r1_boolealg(X0,X1,k5_lattices(X0))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f56321]) ).
fof(f78474,plain,
! [X0,X1] :
( ~ v14_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| r2_hidden(k6_lattices(X0),X1)
| ~ l3_lattices(X0)
| ~ m1_filter_0(X1,X0) ),
inference(duplicate_literal_removal,[],[f62340]) ).
fof(f79237,plain,
! [X0] : m1_subset_1(X0,k1_zfmisc_1(X0)),
inference(forward_demodulation,[],[f62615,f62622]) ).
fof(f79307,plain,
( k5_conlat_1(sK56) != k3_conlat_2(sK56,u1_struct_0(k11_conlat_1(sK56)))
| k6_conlat_1(sK56) != k2_conlat_2(sK56,k2_subset_1(u1_struct_0(k11_conlat_1(sK56)))) ),
inference(forward_demodulation,[],[f62057,f62622]) ).
fof(f79476,plain,
( k6_conlat_1(sK56) != k2_conlat_2(sK56,u1_struct_0(k11_conlat_1(sK56)))
| k5_conlat_1(sK56) != k3_conlat_2(sK56,u1_struct_0(k11_conlat_1(sK56))) ),
inference(forward_demodulation,[],[f79307,f62622]) ).
fof(f79544,definition,
( spl1774_70
<=> k5_conlat_1(sK56) = k3_conlat_2(sK56,u1_struct_0(k11_conlat_1(sK56))) ),
introduced(definition,[new_symbols(definition,[spl1774_70])],[avatar_definition]) ).
fof(f79545,plain,
( k5_conlat_1(sK56) != k3_conlat_2(sK56,u1_struct_0(k11_conlat_1(sK56)))
| spl1774_70 ),
inference(avatar_component_clause,[],[f79544]) ).
fof(f79547,definition,
( spl1774_71
<=> k6_conlat_1(sK56) = k2_conlat_2(sK56,u1_struct_0(k11_conlat_1(sK56))) ),
introduced(definition,[new_symbols(definition,[spl1774_71])],[avatar_definition]) ).
fof(f79548,plain,
( k6_conlat_1(sK56) != k2_conlat_2(sK56,u1_struct_0(k11_conlat_1(sK56)))
| spl1774_71 ),
inference(avatar_component_clause,[],[f79547]) ).
fof(f79549,plain,
( ~ spl1774_70
| ~ spl1774_71 ),
inference(avatar_split_clause,[],[f79476,f79547,f79544]) ).
fof(f79596,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(k11_conlat_1(sK56))))
| v3_conlat_1(sK56)
| k3_conlat_2(sK56,X0) = k15_lattice3(k11_conlat_1(sK56),X0) ),
inference(resolution,[],[f62055,f62052]) ).
fof(f79597,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(k11_conlat_1(sK56))))
| v3_conlat_1(sK56)
| k2_conlat_2(sK56,X0) = k16_lattice3(k11_conlat_1(sK56),X0) ),
inference(resolution,[],[f62055,f62051]) ).
fof(f79598,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(k11_conlat_1(sK56))))
| k2_conlat_2(sK56,X0) = k16_lattice3(k11_conlat_1(sK56),X0) ),
inference(forward_subsumption_resolution,[],[f79597,f62056]) ).
fof(f79599,plain,
! [X0] :
( ~ m1_subset_1(X0,k1_zfmisc_1(u1_struct_0(k11_conlat_1(sK56))))
| k3_conlat_2(sK56,X0) = k15_lattice3(k11_conlat_1(sK56),X0) ),
inference(forward_subsumption_resolution,[],[f79596,f62056]) ).
fof(f79600,plain,
( v3_conlat_1(sK56)
| k6_conlat_1(sK56) = k5_lattices(k11_conlat_1(sK56)) ),
inference(resolution,[],[f62042,f62055]) ).
fof(f79601,plain,
k6_conlat_1(sK56) = k5_lattices(k11_conlat_1(sK56)),
inference(forward_subsumption_resolution,[],[f79600,f62056]) ).
fof(f79602,plain,
( v3_conlat_1(sK56)
| k5_conlat_1(sK56) = k6_lattices(k11_conlat_1(sK56)) ),
inference(resolution,[],[f62041,f62055]) ).
fof(f79603,plain,
k5_conlat_1(sK56) = k6_lattices(k11_conlat_1(sK56)),
inference(forward_subsumption_resolution,[],[f79602,f62056]) ).
fof(f79608,plain,
! [X0] :
( v3_struct_0(k11_conlat_1(X0))
| u1_struct_0(k11_conlat_1(X0)) = u1_struct_0(k1_lattice2(k11_conlat_1(X0)))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(resolution,[],[f62176,f62074]) ).
fof(f79609,plain,
! [X0] :
( ~ l2_conlat_1(X0)
| v3_conlat_1(X0)
| u1_struct_0(k11_conlat_1(X0)) = u1_struct_0(k1_lattice2(k11_conlat_1(X0))) ),
inference(forward_subsumption_resolution,[],[f79608,f62095]) ).
fof(f79664,plain,
( v3_conlat_1(sK56)
| u1_struct_0(k11_conlat_1(sK56)) = u1_struct_0(k1_lattice2(k11_conlat_1(sK56))) ),
inference(resolution,[],[f79609,f62055]) ).
fof(f79666,plain,
u1_struct_0(k11_conlat_1(sK56)) = u1_struct_0(k1_lattice2(k11_conlat_1(sK56))),
inference(forward_subsumption_resolution,[],[f79664,f62056]) ).
fof(f79675,definition,
( spl1774_85
<=> v3_struct_0(k1_lattice2(k11_conlat_1(sK56))) ),
introduced(definition,[new_symbols(definition,[spl1774_85])],[avatar_definition]) ).
fof(f79676,plain,
( v3_struct_0(k1_lattice2(k11_conlat_1(sK56)))
| ~ spl1774_85 ),
inference(avatar_component_clause,[],[f79675]) ).
fof(f79681,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,[],[f62173,f62094]) ).
fof(f79682,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,[],[f79681,f62074]) ).
fof(f79683,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,[],[f79682,f62095]) ).
fof(f79684,plain,
( v3_conlat_1(sK56)
| k11_conlat_1(sK56) = k1_lattice2(k1_lattice2(k11_conlat_1(sK56))) ),
inference(resolution,[],[f79683,f62055]) ).
fof(f79686,plain,
k11_conlat_1(sK56) = k1_lattice2(k1_lattice2(k11_conlat_1(sK56))),
inference(forward_subsumption_resolution,[],[f79684,f62056]) ).
fof(f79741,plain,
! [X0,X1] :
( v3_struct_0(k11_conlat_1(X0))
| m1_subset_1(k16_lattice3(k11_conlat_1(X0),X1),u1_struct_0(k11_conlat_1(X0)))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(resolution,[],[f62530,f62074]) ).
fof(f79742,plain,
! [X0,X1] :
( ~ l2_conlat_1(X0)
| v3_conlat_1(X0)
| m1_subset_1(k16_lattice3(k11_conlat_1(X0),X1),u1_struct_0(k11_conlat_1(X0))) ),
inference(forward_subsumption_resolution,[],[f79741,f62095]) ).
fof(f79743,plain,
! [X0] :
( v3_conlat_1(sK56)
| m1_subset_1(k16_lattice3(k11_conlat_1(sK56),X0),u1_struct_0(k11_conlat_1(sK56))) ),
inference(resolution,[],[f79742,f62055]) ).
fof(f79749,plain,
! [X0] : m1_subset_1(k16_lattice3(k11_conlat_1(sK56),X0),u1_struct_0(k11_conlat_1(sK56))),
inference(forward_subsumption_resolution,[],[f79743,f62056]) ).
fof(f79769,definition,
( spl1774_94
<=> v10_lattices(k11_conlat_1(sK56)) ),
introduced(definition,[new_symbols(definition,[spl1774_94])],[avatar_definition]) ).
fof(f79770,plain,
( ~ v10_lattices(k11_conlat_1(sK56))
| spl1774_94 ),
inference(avatar_component_clause,[],[f79769]) ).
fof(f79772,definition,
( spl1774_95
<=> v3_struct_0(k11_conlat_1(sK56)) ),
introduced(definition,[new_symbols(definition,[spl1774_95])],[avatar_definition]) ).
fof(f79773,plain,
( v3_struct_0(k11_conlat_1(sK56))
| ~ spl1774_95 ),
inference(avatar_component_clause,[],[f79772]) ).
fof(f79781,plain,
( v3_conlat_1(sK56)
| ~ l2_conlat_1(sK56)
| spl1774_94 ),
inference(resolution,[],[f79770,f62087]) ).
fof(f79783,plain,
( ~ l2_conlat_1(sK56)
| spl1774_94 ),
inference(forward_subsumption_resolution,[],[f79781,f62056]) ).
fof(f79784,plain,
( $false
| spl1774_94 ),
inference(forward_subsumption_resolution,[],[f79783,f62055]) ).
fof(f79785,plain,
spl1774_94,
inference(avatar_contradiction_clause,[],[f79784]) ).
fof(f79793,plain,
( v3_conlat_1(sK56)
| ~ l2_conlat_1(sK56)
| ~ spl1774_95 ),
inference(resolution,[],[f79773,f62095]) ).
fof(f79795,plain,
( ~ l2_conlat_1(sK56)
| ~ spl1774_95 ),
inference(forward_subsumption_resolution,[],[f79793,f62056]) ).
fof(f79796,plain,
( $false
| ~ spl1774_95 ),
inference(forward_subsumption_resolution,[],[f79795,f62055]) ).
fof(f79797,plain,
~ spl1774_95,
inference(avatar_contradiction_clause,[],[f79796]) ).
fof(f79826,plain,
k3_conlat_2(sK56,u1_struct_0(k11_conlat_1(sK56))) = k15_lattice3(k11_conlat_1(sK56),u1_struct_0(k11_conlat_1(sK56))),
inference(resolution,[],[f79237,f79599]) ).
fof(f79827,plain,
k2_conlat_2(sK56,u1_struct_0(k11_conlat_1(sK56))) = k16_lattice3(k11_conlat_1(sK56),u1_struct_0(k11_conlat_1(sK56))),
inference(resolution,[],[f79237,f79598]) ).
fof(f79838,plain,
m1_subset_1(k2_conlat_2(sK56,u1_struct_0(k11_conlat_1(sK56))),u1_struct_0(k11_conlat_1(sK56))),
inference(superposition,[],[f79749,f79827]) ).
fof(f80209,plain,
! [X0] :
( v3_struct_0(k11_conlat_1(X0))
| ~ v10_lattices(k11_conlat_1(X0))
| k5_lattices(k11_conlat_1(X0)) = k6_lattices(k1_lattice2(k11_conlat_1(X0)))
| ~ l3_lattices(k11_conlat_1(X0))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(resolution,[],[f62156,f62031]) ).
fof(f80210,plain,
! [X0] :
( v3_struct_0(k11_conlat_1(X0))
| ~ v10_lattices(k11_conlat_1(X0))
| k5_lattices(k11_conlat_1(X0)) = k6_lattices(k1_lattice2(k11_conlat_1(X0)))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(forward_subsumption_resolution,[],[f80209,f62074]) ).
fof(f80211,plain,
! [X0] :
( ~ v10_lattices(k11_conlat_1(X0))
| k5_lattices(k11_conlat_1(X0)) = k6_lattices(k1_lattice2(k11_conlat_1(X0)))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(forward_subsumption_resolution,[],[f80210,f62095]) ).
fof(f80212,plain,
! [X0] :
( ~ l2_conlat_1(X0)
| v3_conlat_1(X0)
| k5_lattices(k11_conlat_1(X0)) = k6_lattices(k1_lattice2(k11_conlat_1(X0))) ),
inference(forward_subsumption_resolution,[],[f80211,f62087]) ).
fof(f80213,plain,
( v3_conlat_1(sK56)
| k5_lattices(k11_conlat_1(sK56)) = k6_lattices(k1_lattice2(k11_conlat_1(sK56))) ),
inference(resolution,[],[f80212,f62055]) ).
fof(f80216,plain,
k5_lattices(k11_conlat_1(sK56)) = k6_lattices(k1_lattice2(k11_conlat_1(sK56))),
inference(forward_subsumption_resolution,[],[f80213,f62056]) ).
fof(f80221,plain,
k6_conlat_1(sK56) = k6_lattices(k1_lattice2(k11_conlat_1(sK56))),
inference(forward_demodulation,[],[f80216,f79601]) ).
fof(f80362,plain,
! [X0] :
( ~ l2_conlat_1(X0)
| v3_conlat_1(X0)
| l3_lattices(k1_lattice2(k11_conlat_1(X0))) ),
inference(resolution,[],[f62151,f62074]) ).
fof(f80364,plain,
( v3_conlat_1(sK56)
| l3_lattices(k1_lattice2(k11_conlat_1(sK56))) ),
inference(resolution,[],[f80362,f62055]) ).
fof(f80371,plain,
l3_lattices(k1_lattice2(k11_conlat_1(sK56))),
inference(forward_subsumption_resolution,[],[f80364,f62056]) ).
fof(f80374,plain,
l3_lattices(k1_lattice2(k1_lattice2(k11_conlat_1(sK56)))),
inference(resolution,[],[f80371,f62151]) ).
fof(f80383,plain,
l3_lattices(k11_conlat_1(sK56)),
inference(forward_demodulation,[],[f80374,f79686]) ).
fof(f80909,plain,
( v3_struct_0(k11_conlat_1(sK56))
| ~ l3_lattices(k11_conlat_1(sK56))
| ~ spl1774_85 ),
inference(resolution,[],[f62188,f79676]) ).
fof(f80911,plain,
( v3_struct_0(k11_conlat_1(sK56))
| ~ spl1774_85 ),
inference(forward_subsumption_resolution,[],[f80909,f80383]) ).
fof(f80912,plain,
( spl1774_95
| ~ spl1774_85 ),
inference(avatar_split_clause,[],[f80911,f79675,f79772]) ).
fof(f80919,plain,
( ~ v3_struct_0(k11_conlat_1(sK56))
| spl1774_95 ),
inference(avatar_component_clause,[],[f79772]) ).
fof(f81525,plain,
! [X0,X1] :
( ~ r3_lattices(k11_conlat_1(X0),X1,k5_lattices(k11_conlat_1(X0)))
| ~ m1_subset_1(X1,u1_struct_0(k11_conlat_1(X0)))
| v3_struct_0(k11_conlat_1(X0))
| ~ v10_lattices(k11_conlat_1(X0))
| r1_boolealg(k11_conlat_1(X0),X1,k5_lattices(k11_conlat_1(X0)))
| ~ l3_lattices(k11_conlat_1(X0))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(resolution,[],[f71475,f62031]) ).
fof(f81526,plain,
! [X0,X1] :
( ~ r3_lattices(k11_conlat_1(X0),X1,k5_lattices(k11_conlat_1(X0)))
| ~ m1_subset_1(X1,u1_struct_0(k11_conlat_1(X0)))
| v3_struct_0(k11_conlat_1(X0))
| ~ v10_lattices(k11_conlat_1(X0))
| r1_boolealg(k11_conlat_1(X0),X1,k5_lattices(k11_conlat_1(X0)))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(forward_subsumption_resolution,[],[f81525,f62074]) ).
fof(f81527,plain,
! [X0,X1] :
( ~ r3_lattices(k11_conlat_1(X0),X1,k5_lattices(k11_conlat_1(X0)))
| ~ m1_subset_1(X1,u1_struct_0(k11_conlat_1(X0)))
| ~ v10_lattices(k11_conlat_1(X0))
| r1_boolealg(k11_conlat_1(X0),X1,k5_lattices(k11_conlat_1(X0)))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(forward_subsumption_resolution,[],[f81526,f62095]) ).
fof(f81528,plain,
! [X0,X1] :
( ~ l2_conlat_1(X0)
| ~ m1_subset_1(X1,u1_struct_0(k11_conlat_1(X0)))
| r1_boolealg(k11_conlat_1(X0),X1,k5_lattices(k11_conlat_1(X0)))
| v3_conlat_1(X0)
| ~ r3_lattices(k11_conlat_1(X0),X1,k5_lattices(k11_conlat_1(X0))) ),
inference(forward_subsumption_resolution,[],[f81527,f62087]) ).
fof(f81529,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK56)))
| r1_boolealg(k11_conlat_1(sK56),X0,k5_lattices(k11_conlat_1(sK56)))
| v3_conlat_1(sK56)
| ~ r3_lattices(k11_conlat_1(sK56),X0,k5_lattices(k11_conlat_1(sK56))) ),
inference(resolution,[],[f81528,f62055]) ).
fof(f81532,plain,
! [X0] :
( ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK56)))
| r1_boolealg(k11_conlat_1(sK56),X0,k5_lattices(k11_conlat_1(sK56)))
| ~ r3_lattices(k11_conlat_1(sK56),X0,k5_lattices(k11_conlat_1(sK56))) ),
inference(forward_subsumption_resolution,[],[f81529,f62056]) ).
fof(f81534,plain,
! [X0] :
( r1_boolealg(k11_conlat_1(sK56),X0,k6_conlat_1(sK56))
| ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK56)))
| ~ r3_lattices(k11_conlat_1(sK56),X0,k5_lattices(k11_conlat_1(sK56))) ),
inference(forward_demodulation,[],[f81532,f79601]) ).
fof(f81539,plain,
! [X0] :
( ~ r3_lattices(k11_conlat_1(sK56),X0,k6_conlat_1(sK56))
| r1_boolealg(k11_conlat_1(sK56),X0,k6_conlat_1(sK56))
| ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK56))) ),
inference(forward_demodulation,[],[f81534,f79601]) ).
fof(f81641,plain,
! [X2,X0,X1] :
( ~ r2_hidden(X0,X1)
| ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(X2)))
| v3_struct_0(k11_conlat_1(X2))
| ~ v10_lattices(k11_conlat_1(X2))
| r3_lattices(k11_conlat_1(X2),k16_lattice3(k11_conlat_1(X2),X1),X0)
| ~ l3_lattices(k11_conlat_1(X2))
| v3_conlat_1(X2)
| ~ l2_conlat_1(X2) ),
inference(resolution,[],[f62537,f62077]) ).
fof(f81642,plain,
! [X2,X0,X1] :
( ~ r2_hidden(X0,X1)
| ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(X2)))
| v3_struct_0(k11_conlat_1(X2))
| ~ v10_lattices(k11_conlat_1(X2))
| r3_lattices(k11_conlat_1(X2),k16_lattice3(k11_conlat_1(X2),X1),X0)
| v3_conlat_1(X2)
| ~ l2_conlat_1(X2) ),
inference(forward_subsumption_resolution,[],[f81641,f62074]) ).
fof(f81643,plain,
! [X2,X0,X1] :
( ~ r2_hidden(X0,X1)
| ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(X2)))
| ~ v10_lattices(k11_conlat_1(X2))
| r3_lattices(k11_conlat_1(X2),k16_lattice3(k11_conlat_1(X2),X1),X0)
| v3_conlat_1(X2)
| ~ l2_conlat_1(X2) ),
inference(forward_subsumption_resolution,[],[f81642,f62095]) ).
fof(f81644,plain,
! [X2,X0,X1] :
( ~ l2_conlat_1(X2)
| ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(X2)))
| r3_lattices(k11_conlat_1(X2),k16_lattice3(k11_conlat_1(X2),X1),X0)
| v3_conlat_1(X2)
| ~ r2_hidden(X0,X1) ),
inference(forward_subsumption_resolution,[],[f81643,f62087]) ).
fof(f81645,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK56)))
| r3_lattices(k11_conlat_1(sK56),k16_lattice3(k11_conlat_1(sK56),X1),X0)
| v3_conlat_1(sK56)
| ~ r2_hidden(X0,X1) ),
inference(resolution,[],[f81644,f62055]) ).
fof(f81651,plain,
! [X0,X1] :
( r3_lattices(k11_conlat_1(sK56),k16_lattice3(k11_conlat_1(sK56),X1),X0)
| ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK56)))
| ~ r2_hidden(X0,X1) ),
inference(forward_subsumption_resolution,[],[f81645,f62056]) ).
fof(f81656,plain,
! [X0] :
( r3_lattices(k11_conlat_1(sK56),k2_conlat_2(sK56,u1_struct_0(k11_conlat_1(sK56))),X0)
| ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK56)))
| ~ r2_hidden(X0,u1_struct_0(k11_conlat_1(sK56))) ),
inference(superposition,[],[f81651,f79827]) ).
fof(f81662,plain,
! [X0] :
( r3_lattices(k11_conlat_1(sK56),k2_conlat_2(sK56,u1_struct_0(k11_conlat_1(sK56))),X0)
| ~ r2_hidden(X0,u1_struct_0(k11_conlat_1(sK56))) ),
inference(forward_subsumption_resolution,[],[f81656,f62628]) ).
fof(f81680,plain,
( ~ r2_hidden(k6_conlat_1(sK56),u1_struct_0(k11_conlat_1(sK56)))
| r1_boolealg(k11_conlat_1(sK56),k2_conlat_2(sK56,u1_struct_0(k11_conlat_1(sK56))),k6_conlat_1(sK56))
| ~ m1_subset_1(k2_conlat_2(sK56,u1_struct_0(k11_conlat_1(sK56))),u1_struct_0(k11_conlat_1(sK56))) ),
inference(resolution,[],[f81662,f81539]) ).
fof(f81683,plain,
( ~ r2_hidden(k6_conlat_1(sK56),u1_struct_0(k11_conlat_1(sK56)))
| r1_boolealg(k11_conlat_1(sK56),k2_conlat_2(sK56,u1_struct_0(k11_conlat_1(sK56))),k6_conlat_1(sK56)) ),
inference(forward_subsumption_resolution,[],[f81680,f79838]) ).
fof(f81686,definition,
( spl1774_208
<=> r1_boolealg(k11_conlat_1(sK56),k2_conlat_2(sK56,u1_struct_0(k11_conlat_1(sK56))),k6_conlat_1(sK56)) ),
introduced(definition,[new_symbols(definition,[spl1774_208])],[avatar_definition]) ).
fof(f81687,plain,
( r1_boolealg(k11_conlat_1(sK56),k2_conlat_2(sK56,u1_struct_0(k11_conlat_1(sK56))),k6_conlat_1(sK56))
| ~ spl1774_208 ),
inference(avatar_component_clause,[],[f81686]) ).
fof(f81689,definition,
( spl1774_209
<=> r2_hidden(k6_conlat_1(sK56),u1_struct_0(k11_conlat_1(sK56))) ),
introduced(definition,[new_symbols(definition,[spl1774_209])],[avatar_definition]) ).
fof(f81691,plain,
( spl1774_208
| ~ spl1774_209 ),
inference(avatar_split_clause,[],[f81683,f81689,f81686]) ).
fof(f81939,plain,
! [X0] :
( v3_struct_0(k11_conlat_1(X0))
| ~ v10_lattices(k11_conlat_1(X0))
| k6_lattices(k11_conlat_1(X0)) = k15_lattice3(k11_conlat_1(X0),u1_struct_0(k11_conlat_1(X0)))
| ~ l3_lattices(k11_conlat_1(X0))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(resolution,[],[f62328,f62077]) ).
fof(f81940,plain,
! [X0] :
( v3_struct_0(k11_conlat_1(X0))
| ~ v10_lattices(k11_conlat_1(X0))
| k6_lattices(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) ),
inference(forward_subsumption_resolution,[],[f81939,f62074]) ).
fof(f81941,plain,
! [X0] :
( ~ v10_lattices(k11_conlat_1(X0))
| k6_lattices(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) ),
inference(forward_subsumption_resolution,[],[f81940,f62095]) ).
fof(f81942,plain,
! [X0] :
( ~ l2_conlat_1(X0)
| v3_conlat_1(X0)
| k6_lattices(k11_conlat_1(X0)) = k15_lattice3(k11_conlat_1(X0),u1_struct_0(k11_conlat_1(X0))) ),
inference(forward_subsumption_resolution,[],[f81941,f62087]) ).
fof(f81943,plain,
( v3_conlat_1(sK56)
| k6_lattices(k11_conlat_1(sK56)) = k15_lattice3(k11_conlat_1(sK56),u1_struct_0(k11_conlat_1(sK56))) ),
inference(resolution,[],[f81942,f62055]) ).
fof(f81946,plain,
k6_lattices(k11_conlat_1(sK56)) = k15_lattice3(k11_conlat_1(sK56),u1_struct_0(k11_conlat_1(sK56))),
inference(forward_subsumption_resolution,[],[f81943,f62056]) ).
fof(f81951,plain,
k5_conlat_1(sK56) = k15_lattice3(k11_conlat_1(sK56),u1_struct_0(k11_conlat_1(sK56))),
inference(forward_demodulation,[],[f81946,f79603]) ).
fof(f81953,plain,
k5_conlat_1(sK56) = k3_conlat_2(sK56,u1_struct_0(k11_conlat_1(sK56))),
inference(superposition,[],[f79826,f81951]) ).
fof(f82388,plain,
! [X0] :
( v14_lattices(k1_lattice2(k11_conlat_1(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(resolution,[],[f62167,f62031]) ).
fof(f82389,plain,
! [X0] :
( v14_lattices(k1_lattice2(k11_conlat_1(X0)))
| v3_struct_0(k11_conlat_1(X0))
| ~ v10_lattices(k11_conlat_1(X0))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(forward_subsumption_resolution,[],[f82388,f62074]) ).
fof(f82390,plain,
! [X0] :
( v14_lattices(k1_lattice2(k11_conlat_1(X0)))
| ~ v10_lattices(k11_conlat_1(X0))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(forward_subsumption_resolution,[],[f82389,f62095]) ).
fof(f82391,plain,
! [X0] :
( ~ l2_conlat_1(X0)
| v3_conlat_1(X0)
| v14_lattices(k1_lattice2(k11_conlat_1(X0))) ),
inference(forward_subsumption_resolution,[],[f82390,f62087]) ).
fof(f82392,plain,
( v3_conlat_1(sK56)
| v14_lattices(k1_lattice2(k11_conlat_1(sK56))) ),
inference(resolution,[],[f82391,f62055]) ).
fof(f82398,plain,
v14_lattices(k1_lattice2(k11_conlat_1(sK56))),
inference(forward_subsumption_resolution,[],[f82392,f62056]) ).
fof(f82400,plain,
! [X0] :
( v3_struct_0(k1_lattice2(k11_conlat_1(sK56)))
| ~ v10_lattices(k1_lattice2(k11_conlat_1(sK56)))
| r2_hidden(k6_lattices(k1_lattice2(k11_conlat_1(sK56))),X0)
| ~ l3_lattices(k1_lattice2(k11_conlat_1(sK56)))
| ~ m1_filter_0(X0,k1_lattice2(k11_conlat_1(sK56))) ),
inference(resolution,[],[f82398,f78474]) ).
fof(f88232,plain,
! [X0] :
( v3_struct_0(k11_conlat_1(X0))
| v10_lattices(k1_lattice2(k11_conlat_1(X0)))
| ~ l3_lattices(k11_conlat_1(X0))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(resolution,[],[f62178,f62087]) ).
fof(f88233,plain,
! [X0] :
( v3_struct_0(k11_conlat_1(X0))
| v10_lattices(k1_lattice2(k11_conlat_1(X0)))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(forward_subsumption_resolution,[],[f88232,f62074]) ).
fof(f88234,plain,
! [X0] :
( ~ l2_conlat_1(X0)
| v3_conlat_1(X0)
| v10_lattices(k1_lattice2(k11_conlat_1(X0))) ),
inference(forward_subsumption_resolution,[],[f88233,f62095]) ).
fof(f88236,plain,
( v3_conlat_1(sK56)
| v10_lattices(k1_lattice2(k11_conlat_1(sK56))) ),
inference(resolution,[],[f88234,f62055]) ).
fof(f88240,plain,
v10_lattices(k1_lattice2(k11_conlat_1(sK56))),
inference(forward_subsumption_resolution,[],[f88236,f62056]) ).
fof(f88249,plain,
! [X0] :
( v3_struct_0(k1_lattice2(k11_conlat_1(sK56)))
| ~ v10_lattices(k1_lattice2(k11_conlat_1(sK56)))
| r2_hidden(k6_lattices(k1_lattice2(k11_conlat_1(sK56))),X0)
| ~ m1_filter_0(X0,k1_lattice2(k11_conlat_1(sK56))) ),
inference(forward_subsumption_resolution,[],[f82400,f80371]) ).
fof(f88259,plain,
! [X0] :
( v3_struct_0(k1_lattice2(k11_conlat_1(sK56)))
| r2_hidden(k6_lattices(k1_lattice2(k11_conlat_1(sK56))),X0)
| ~ m1_filter_0(X0,k1_lattice2(k11_conlat_1(sK56))) ),
inference(forward_subsumption_resolution,[],[f88249,f88240]) ).
fof(f88278,plain,
! [X0] :
( r2_hidden(k6_conlat_1(sK56),X0)
| v3_struct_0(k1_lattice2(k11_conlat_1(sK56)))
| ~ m1_filter_0(X0,k1_lattice2(k11_conlat_1(sK56))) ),
inference(forward_demodulation,[],[f88259,f80221]) ).
fof(f88288,definition,
( spl1774_342
<=> ! [X0] :
( r2_hidden(k6_conlat_1(sK56),X0)
| ~ m1_filter_0(X0,k1_lattice2(k11_conlat_1(sK56))) ) ),
introduced(definition,[new_symbols(definition,[spl1774_342])],[avatar_definition]) ).
fof(f88289,plain,
( ! [X0] :
( ~ m1_filter_0(X0,k1_lattice2(k11_conlat_1(sK56)))
| r2_hidden(k6_conlat_1(sK56),X0) )
| ~ spl1774_342 ),
inference(avatar_component_clause,[],[f88288]) ).
fof(f88290,plain,
( spl1774_85
| spl1774_342 ),
inference(avatar_split_clause,[],[f88278,f88288,f79675]) ).
fof(f88372,plain,
( r2_hidden(k6_conlat_1(sK56),u1_struct_0(k1_lattice2(k11_conlat_1(sK56))))
| v3_struct_0(k1_lattice2(k11_conlat_1(sK56)))
| ~ v10_lattices(k1_lattice2(k11_conlat_1(sK56)))
| ~ l3_lattices(k1_lattice2(k11_conlat_1(sK56)))
| ~ spl1774_342 ),
inference(resolution,[],[f88289,f62913]) ).
fof(f88373,plain,
( r2_hidden(k6_conlat_1(sK56),u1_struct_0(k1_lattice2(k11_conlat_1(sK56))))
| v3_struct_0(k1_lattice2(k11_conlat_1(sK56)))
| ~ l3_lattices(k1_lattice2(k11_conlat_1(sK56)))
| ~ spl1774_342 ),
inference(forward_subsumption_resolution,[],[f88372,f88240]) ).
fof(f88374,plain,
( r2_hidden(k6_conlat_1(sK56),u1_struct_0(k1_lattice2(k11_conlat_1(sK56))))
| v3_struct_0(k1_lattice2(k11_conlat_1(sK56)))
| ~ spl1774_342 ),
inference(forward_subsumption_resolution,[],[f88373,f80371]) ).
fof(f88375,plain,
( r2_hidden(k6_conlat_1(sK56),u1_struct_0(k11_conlat_1(sK56)))
| v3_struct_0(k1_lattice2(k11_conlat_1(sK56)))
| ~ spl1774_342 ),
inference(forward_demodulation,[],[f88374,f79666]) ).
fof(f88378,plain,
( r2_hidden(k6_conlat_1(sK56),u1_struct_0(k11_conlat_1(sK56)))
| ~ spl1774_209 ),
inference(avatar_component_clause,[],[f81689]) ).
fof(f88379,plain,
( spl1774_85
| spl1774_209
| ~ spl1774_342 ),
inference(avatar_split_clause,[],[f88375,f88288,f81689,f79675]) ).
fof(f88387,plain,
( m1_subset_1(k6_conlat_1(sK56),u1_struct_0(k11_conlat_1(sK56)))
| ~ spl1774_209 ),
inference(resolution,[],[f88378,f62628]) ).
fof(f88448,plain,
( ! [X0] :
( ~ r1_boolealg(k11_conlat_1(sK56),X0,k6_conlat_1(sK56))
| v3_struct_0(k11_conlat_1(sK56))
| ~ v10_lattices(k11_conlat_1(sK56))
| ~ l3_lattices(k11_conlat_1(sK56))
| ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK56)))
| k6_conlat_1(sK56) = X0 )
| ~ spl1774_209 ),
inference(resolution,[],[f88387,f71465]) ).
fof(f88460,plain,
( ! [X0] :
( ~ r1_boolealg(k11_conlat_1(sK56),X0,k6_conlat_1(sK56))
| ~ v10_lattices(k11_conlat_1(sK56))
| ~ l3_lattices(k11_conlat_1(sK56))
| ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK56)))
| k6_conlat_1(sK56) = X0 )
| spl1774_95
| ~ spl1774_209 ),
inference(forward_subsumption_resolution,[],[f88448,f80919]) ).
fof(f88461,plain,
( ! [X0] :
( ~ r1_boolealg(k11_conlat_1(sK56),X0,k6_conlat_1(sK56))
| ~ v10_lattices(k11_conlat_1(sK56))
| ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK56)))
| k6_conlat_1(sK56) = X0 )
| spl1774_95
| ~ spl1774_209 ),
inference(forward_subsumption_resolution,[],[f88460,f80383]) ).
fof(f88463,definition,
( spl1774_357
<=> ! [X0] :
( ~ r1_boolealg(k11_conlat_1(sK56),X0,k6_conlat_1(sK56))
| k6_conlat_1(sK56) = X0
| ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK56))) ) ),
introduced(definition,[new_symbols(definition,[spl1774_357])],[avatar_definition]) ).
fof(f88464,plain,
( ! [X0] :
( ~ r1_boolealg(k11_conlat_1(sK56),X0,k6_conlat_1(sK56))
| k6_conlat_1(sK56) = X0
| ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK56))) )
| ~ spl1774_357 ),
inference(avatar_component_clause,[],[f88463]) ).
fof(f88465,plain,
( ~ spl1774_94
| spl1774_357
| spl1774_95
| ~ spl1774_209 ),
inference(avatar_split_clause,[],[f88461,f81689,f79772,f88463,f79769]) ).
fof(f88492,plain,
( k6_conlat_1(sK56) = k2_conlat_2(sK56,u1_struct_0(k11_conlat_1(sK56)))
| ~ m1_subset_1(k2_conlat_2(sK56,u1_struct_0(k11_conlat_1(sK56))),u1_struct_0(k11_conlat_1(sK56)))
| ~ spl1774_208
| ~ spl1774_357 ),
inference(resolution,[],[f81687,f88464]) ).
fof(f88499,plain,
( ~ m1_subset_1(k2_conlat_2(sK56,u1_struct_0(k11_conlat_1(sK56))),u1_struct_0(k11_conlat_1(sK56)))
| spl1774_71
| ~ spl1774_208
| ~ spl1774_357 ),
inference(forward_subsumption_resolution,[],[f88492,f79548]) ).
fof(f88502,plain,
( $false
| spl1774_71
| ~ spl1774_208
| ~ spl1774_357 ),
inference(forward_subsumption_resolution,[],[f88499,f79838]) ).
fof(f88503,plain,
( spl1774_71
| ~ spl1774_208
| ~ spl1774_357 ),
inference(avatar_contradiction_clause,[],[f88502]) ).
fof(f88510,plain,
( $false
| spl1774_70 ),
inference(forward_subsumption_resolution,[],[f79545,f81953]) ).
fof(f88511,plain,
spl1774_70,
inference(avatar_contradiction_clause,[],[f88510]) ).
cnf(s58,plain,
( ~ spl1774_70
| ~ spl1774_71 ),
inference(sat_conversion,[],[f79549]) ).
cnf(s80,plain,
spl1774_94,
inference(sat_conversion,[],[f79785]) ).
cnf(s84,plain,
~ spl1774_95,
inference(sat_conversion,[],[f79797]) ).
cnf(s155,plain,
( ~ spl1774_85
| spl1774_95 ),
inference(sat_conversion,[],[f80912]) ).
cnf(s191,plain,
( spl1774_208
| ~ spl1774_209 ),
inference(sat_conversion,[],[f81691]) ).
cnf(s332,plain,
( spl1774_85
| spl1774_342 ),
inference(sat_conversion,[],[f88290]) ).
cnf(s341,plain,
( spl1774_85
| spl1774_209
| ~ spl1774_342 ),
inference(sat_conversion,[],[f88379]) ).
cnf(s352,plain,
( ~ spl1774_94
| spl1774_95
| ~ spl1774_209
| spl1774_357 ),
inference(sat_conversion,[],[f88465]) ).
cnf(s354,plain,
( spl1774_71
| ~ spl1774_208
| ~ spl1774_357 ),
inference(sat_conversion,[],[f88503]) ).
cnf(s356,plain,
spl1774_70,
inference(sat_conversion,[],[f88511]) ).
cnf(s404,plain,
~ spl1774_85,
inference(rat,[],[s155,s84]) ).
cnf(s411,plain,
spl1774_342,
inference(rat,[],[s332,s404]) ).
cnf(s417,plain,
spl1774_209,
inference(rat,[],[s341,s404,s411]) ).
cnf(s430,plain,
spl1774_208,
inference(rat,[],[s191,s417]) ).
cnf(s434,plain,
spl1774_357,
inference(rat,[],[s352,s417,s84,s80]) ).
cnf(s463,plain,
spl1774_71,
inference(rat,[],[s354,s430,s434]) ).
cnf(s546,plain,
$false,
inference(rat,[],[s58,s463,s356]) ).
fof(f88513,plain,
$false,
inference(avatar_sat_refutation,[],[s546]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT340+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.07 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.17/0.41 % Computer : n007.cluster.edu
% 0.17/0.41 % Model : x86_64 x86_64
% 0.17/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.41 % Memory : 8046.5625MB
% 0.17/0.41 % OS : Linux 6.8.0-71-generic
% 0.17/0.41 % CPULimit : 300
% 0.17/0.41 % WCLimit : 300
% 0.17/0.41 % DateTime : Sun Sep 27 14:46:35 UTC 2026
% 0.17/0.41 % CPUTime :
% 0.17/0.41 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.17/0.47 Running first-order theorem proving
% 0.17/0.47 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
% 15.45/4.71 % (1509617)Detected formulas, will run a generic FOF schedule.
% 15.45/4.71 % (1509725)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=3673344195:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2980 on theBenchmark for (2980ds/134677Mi)
% 15.45/4.71 % (1509726)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=4117901747:i=141695:sd=1:nm=32:gsp=on:ss=included_2980 on theBenchmark for (2980ds/141695Mi)
% 15.45/4.71 % (1509724)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=4266916020:i=141193_2980 on theBenchmark for (2980ds/141193Mi)
% 15.45/4.71 % (1509730)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3320082593:i=119:av=off:ss=axioms_2980 on theBenchmark for (2980ds/119Mi)
% 15.45/4.71 % (1509728)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2867633022:i=109:sd=1:ins=1:gsp=on:ss=axioms_2980 on theBenchmark for (2980ds/109Mi)
% 15.45/4.71 % (1509732)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1123600743:s2a=on:i=139:gtg=position_2980 on theBenchmark for (2980ds/139Mi)
% 15.45/4.71 % (1509734)dis-21_1_sil=8000:lcm=predicate:random_seed=206936884:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2980 on theBenchmark for (2980ds/129Mi)
% 15.45/4.71 % (1509732)Instruction limit reached!
% 15.45/4.71 % (1509732)------------------------------
% 15.45/4.71 % (1509732)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.45/4.71 % (1509732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.45/4.71 % (1509732)CaDiCaL version: 2.1.3
% 15.45/4.71 % (1509732)Termination reason: Instruction limit
% 15.45/4.71 % (1509732)Termination phase: Property scanning
% 15.45/4.71 % (1509732)Time elapsed: 0.062 s
% 15.45/4.71 % (1509732)Peak memory usage: 164 MB
% 15.45/4.71 % (1509732)Instructions burned: 139 (million)
% 15.45/4.71 % (1509728)Instruction limit reached!
% 15.45/4.71 % (1509728)------------------------------
% 15.45/4.71 % (1509728)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.45/4.71 % (1509728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.45/4.71 % (1509728)CaDiCaL version: 2.1.3
% 15.45/4.71 % (1509728)Termination reason: Instruction limit
% 15.45/4.71 % (1509728)Termination phase: SInE selection
% 15.45/4.71 % (1509728)Time elapsed: 0.082 s
% 15.45/4.71 % (1509728)Peak memory usage: 163 MB
% 15.45/4.71 % (1509728)Instructions burned: 110 (million)
% 15.45/4.71 % (1509730)Instruction limit reached!
% 15.45/4.71 % (1509730)------------------------------
% 15.45/4.71 % (1509730)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.45/4.71 % (1509730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.45/4.71 % (1509730)CaDiCaL version: 2.1.3
% 15.45/4.71 % (1509730)Termination reason: Instruction limit
% 15.45/4.71 % (1509730)Termination phase: SInE selection
% 15.45/4.71 % (1509730)Time elapsed: 0.090 s
% 15.45/4.71 % (1509730)Peak memory usage: 163 MB
% 15.45/4.71 % (1509730)Instructions burned: 120 (million)
% 15.45/4.71 % (1509734)Instruction limit reached!
% 15.45/4.71 % (1509734)------------------------------
% 15.45/4.71 % (1509734)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.45/4.71 % (1509734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.45/4.71 % (1509734)CaDiCaL version: 2.1.3
% 15.45/4.71 % (1509734)Termination reason: Instruction limit
% 15.45/4.71 % (1509734)Termination phase: SInE selection
% 15.45/4.71 % (1509734)Time elapsed: 0.098 s
% 15.45/4.71 % (1509734)Peak memory usage: 163 MB
% 15.45/4.71 % (1509734)Instructions burned: 130 (million)
% 15.45/4.71 % (1509787)lrs+10_1_sil=8000:sp=occurrence:random_seed=3088534261:i=285:sd=3:ss=axioms:sgt=8_2978 on theBenchmark for (2978ds/285Mi)
% 15.45/4.71 % (1509793)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1974783503:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2978 on theBenchmark for (2978ds/157Mi)
% 15.45/4.71 % (1509794)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2898626390:i=325:sd=1:ss=axioms:sgt=32_2977 on theBenchmark for (2977ds/325Mi)
% 15.45/4.71 % (1509793)Instruction limit reached!
% 15.45/4.71 % (1509793)------------------------------
% 15.45/4.71 % (1509793)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.45/4.71 % (1509793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.32/5.55 % (1509793)CaDiCaL version: 2.1.3
% 21.32/5.55 % (1509793)Termination reason: Instruction limit
% 21.32/5.55 % (1509793)Termination phase: Property scanning
% 21.32/5.55 % (1509793)Time elapsed: 0.073 s
% 21.32/5.55 % (1509793)Peak memory usage: 163 MB
% 21.32/5.55 % (1509793)Instructions burned: 158 (million)
% 21.32/5.55 % (1509795)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=3415513379:s2a=on:i=248:s2at=1.23:gtg=position_2977 on theBenchmark for (2977ds/248Mi)
% 21.32/5.55 % (1509794)Instruction limit reached!
% 21.32/5.55 % (1509794)------------------------------
% 21.32/5.55 % (1509794)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.32/5.55 % (1509794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.32/5.55 % (1509794)CaDiCaL version: 2.1.3
% 21.32/5.55 % (1509794)Termination reason: Instruction limit
% 21.32/5.55 % (1509794)Termination phase: SInE selection
% 21.32/5.55 % (1509794)Time elapsed: 0.135 s
% 21.32/5.55 % (1509794)Peak memory usage: 164 MB
% 21.32/5.55 % (1509794)Instructions burned: 327 (million)
% 21.32/5.55 % (1509795)Instruction limit reached!
% 21.32/5.55 % (1509795)------------------------------
% 21.32/5.55 % (1509795)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.32/5.55 % (1509795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.32/5.55 % (1509795)CaDiCaL version: 2.1.3
% 21.32/5.55 % (1509795)Termination reason: Instruction limit
% 21.32/5.55 % (1509795)Termination phase: Property scanning
% 21.32/5.55 % (1509795)Time elapsed: 0.112 s
% 21.32/5.55 % (1509795)Peak memory usage: 164 MB
% 21.32/5.55 % (1509795)Instructions burned: 250 (million)
% 21.32/5.55 % (1509787)Instruction limit reached!
% 21.32/5.55 % (1509787)------------------------------
% 21.32/5.55 % (1509787)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.32/5.55 % (1509787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.32/5.55 % (1509787)CaDiCaL version: 2.1.3
% 21.32/5.55 % (1509787)Termination reason: Instruction limit
% 21.32/5.55 % (1509787)Termination phase: SInE selection
% 21.32/5.55 % (1509787)Time elapsed: 0.206 s
% 21.32/5.55 % (1509787)Peak memory usage: 164 MB
% 21.32/5.55 % (1509787)Instructions burned: 286 (million)
% 21.32/5.55 % (1509800)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2886853883:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2976 on theBenchmark for (2976ds/294Mi)
% 21.32/5.55 % (1509801)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=13432360:i=2350_2975 on theBenchmark for (2975ds/2350Mi)
% 21.32/5.55 % (1509802)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1108083735:cts=off:i=113:fsr=off:ss=included:sgt=4_2974 on theBenchmark for (2974ds/113Mi)
% 21.32/5.55 % (1509803)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2240057080:i=127:av=off:fsr=off:sup=off_2974 on theBenchmark for (2974ds/127Mi)
% 21.32/5.55 % (1509802)Instruction limit reached!
% 21.32/5.55 % (1509802)------------------------------
% 21.32/5.55 % (1509802)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.32/5.55 % (1509802)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.32/5.55 % (1509802)CaDiCaL version: 2.1.3
% 21.32/5.55 % (1509802)Termination reason: Instruction limit
% 21.32/5.55 % (1509802)Termination phase: SInE selection
% 21.32/5.55 % (1509802)Time elapsed: 0.087 s
% 21.32/5.55 % (1509802)Peak memory usage: 163 MB
% 21.32/5.55 % (1509802)Instructions burned: 114 (million)
% 21.32/5.55 % (1509800)Instruction limit reached!
% 21.32/5.55 % (1509800)------------------------------
% 21.32/5.55 % (1509800)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.32/5.55 % (1509800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.32/5.55 % (1509800)CaDiCaL version: 2.1.3
% 21.32/5.55 % (1509800)Termination reason: Instruction limit
% 21.32/5.55 % (1509800)Termination phase: SInE selection
% 21.32/5.55 % (1509800)Time elapsed: 0.205 s
% 21.32/5.55 % (1509800)Peak memory usage: 164 MB
% 21.32/5.55 % (1509800)Instructions burned: 294 (million)
% 21.32/5.55 % (1509803)Instruction limit reached!
% 21.32/5.55 % (1509803)------------------------------
% 21.32/5.55 % (1509803)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.32/5.55 % (1509803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.32/5.55 % (1509803)CaDiCaL version: 2.1.3
% 22.55/9.77 % (1509803)Termination reason: Instruction limit
% 22.55/9.77 % (1509803)Termination phase: Preprocessing 1
% 22.55/9.77 % (1509803)Time elapsed: 0.097 s
% 22.55/9.77 % (1509803)Peak memory usage: 165 MB
% 22.55/9.77 % (1509803)Instructions burned: 127 (million)
% 22.55/9.77 % (1509808)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=69786549:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2972 on theBenchmark for (2972ds/114Mi)
% 22.55/9.77 % (1509809)lrs+10_1_sil=8000:sp=occurrence:random_seed=802251687:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2972 on theBenchmark for (2972ds/907Mi)
% 22.55/9.77 % (1509810)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1065573151:i=437:sd=1:aac=none:ss=included_2972 on theBenchmark for (2972ds/437Mi)
% 22.55/9.77 % (1509808)Instruction limit reached!
% 22.55/9.77 % (1509808)------------------------------
% 22.55/9.77 % (1509808)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.55/9.77 % (1509808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.55/9.77 % (1509808)CaDiCaL version: 2.1.3
% 22.55/9.77 % (1509808)Termination reason: Instruction limit
% 22.55/9.77 % (1509808)Termination phase: Property scanning
% 22.55/9.77 % (1509808)Time elapsed: 0.055 s
% 22.55/9.77 % (1509808)Peak memory usage: 164 MB
% 22.55/9.77 % (1509808)Instructions burned: 114 (million)
% 22.55/9.77 % (1509814)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=449411:i=5202:ss=axioms:sgt=16_2970 on theBenchmark for (2970ds/5202Mi)
% 22.55/9.77 % (1509810)Refutation not found, incomplete strategy
% 22.55/9.77 % (1509810)------------------------------
% 22.55/9.77 % (1509810)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.55/9.77 % (1509810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.55/9.77 % (1509810)CaDiCaL version: 2.1.3
% 22.55/9.77 % (1509810)Termination reason: Refutation not found, incomplete strategy
% 22.55/9.77 % (1509810)Time elapsed: 0.314 s
% 22.55/9.77 % (1509810)Peak memory usage: 170 MB
% 22.55/9.77 % (1509810)Instructions burned: 405 (million)
% 22.55/9.77 % (1509810)------------------------------
% 22.55/9.77 % (1509810)------------------------------
% 22.55/9.77 % (1509801)Instruction limit reached!
% 22.55/9.77 % (1509801)------------------------------
% 22.55/9.77 % (1509801)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.55/9.77 % (1509801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.55/9.77 % (1509801)CaDiCaL version: 2.1.3
% 22.55/9.77 % (1509801)Termination reason: Instruction limit
% 22.55/9.77 % (1509801)Termination phase: Preprocessing 3
% 22.55/9.77 % (1509801)Time elapsed: 0.951 s
% 22.55/9.77 % (1509801)Peak memory usage: 264 MB
% 22.55/9.77 % (1509801)Instructions burned: 2350 (million)
% 22.55/9.77 % (1509809)Instruction limit reached!
% 22.55/9.77 % (1509809)------------------------------
% 22.55/9.77 % (1509809)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.55/9.77 % (1509809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.55/9.77 % (1509809)CaDiCaL version: 2.1.3
% 22.55/9.77 % (1509809)Termination reason: Instruction limit
% 22.55/9.77 % (1509809)Termination phase: Preprocessing 3
% 22.55/9.77 % (1509809)Time elapsed: 0.679 s
% 22.55/9.77 % (1509809)Peak memory usage: 183 MB
% 22.55/9.77 % (1509809)Instructions burned: 909 (million)
% 22.55/9.77 % (1509817)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=1267011646:st=8:i=592:sd=3:ep=RST:ss=axioms_2964 on theBenchmark for (2964ds/592Mi)
% 22.55/9.77 % (1509816)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=1237232149:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2964 on theBenchmark for (2964ds/134Mi)
% 22.55/9.77 % (1509816)Instruction limit reached!
% 22.55/9.77 % (1509816)------------------------------
% 22.55/9.77 % (1509816)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.55/9.77 % (1509816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.55/9.77 % (1509816)CaDiCaL version: 2.1.3
% 22.55/9.77 % (1509816)Termination reason: Instruction limit
% 22.55/9.77 % (1509816)Termination phase: SInE selection
% 22.55/9.77 % (1509816)Time elapsed: 0.103 s
% 22.55/9.77 % (1509816)Peak memory usage: 163 MB
% 22.55/9.77 % (1509816)Instructions burned: 135 (million)
% 22.55/9.77 % (1509818)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=4069178075:st=3:i=13193:sd=3:ss=axioms_2963 on theBenchmark for (2963ds/13193Mi)
% 22.55/9.77 % (1509817)Instruction limit reached!
% 22.55/9.77 % (1509817)------------------------------
% 22.55/9.77 % (1509817)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.55/9.77 % (1509817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.55/9.77 % (1509817)CaDiCaL version: 2.1.3
% 22.55/9.77 % (1509817)Termination reason: Instruction limit
% 22.55/9.77 % (1509817)Termination phase: Preprocessing 1
% 22.55/9.77 % (1509817)Time elapsed: 0.234 s
% 22.55/9.77 % (1509817)Peak memory usage: 167 MB
% 22.55/9.77 % (1509817)Instructions burned: 594 (million)
% 22.55/9.77 % (1509821)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=3896233434:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2962 on theBenchmark for (2962ds/125Mi)
% 22.55/9.77 % (1509821)Instruction limit reached!
% 22.55/9.77 % (1509821)------------------------------
% 22.55/9.77 % (1509821)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.55/9.77 % (1509821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.55/9.77 % (1509821)CaDiCaL version: 2.1.3
% 22.55/9.77 % (1509821)Termination reason: Instruction limit
% 22.55/9.77 % (1509821)Termination phase: Property scanning
% 22.55/9.77 % (1509821)Time elapsed: 0.061 s
% 22.55/9.77 % (1509821)Peak memory usage: 164 MB
% 22.55/9.77 % (1509821)Instructions burned: 127 (million)
% 22.55/9.77 % (1509823)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2381362789:i=134:gtgl=5:slsql=off:gtg=exists_sym_2960 on theBenchmark for (2960ds/134Mi)
% 22.55/9.77 % (1509823)Instruction limit reached!
% 22.55/9.77 % (1509823)------------------------------
% 22.55/9.77 % (1509823)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.55/9.77 % (1509823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.55/9.77 % (1509823)CaDiCaL version: 2.1.3
% 22.55/9.77 % (1509823)Termination reason: Instruction limit
% 22.55/9.77 % (1509823)Termination phase: Property scanning
% 22.55/9.77 % (1509823)Time elapsed: 0.035 s
% 22.55/9.77 % (1509823)Peak memory usage: 164 MB
% 22.55/9.77 % (1509823)Instructions burned: 138 (million)
% 22.55/9.77 % (1509825)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1352325507:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2959 on theBenchmark for (2959ds/141Mi)
% 22.55/9.77 % (1509827)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1948389270:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2959 on theBenchmark for (2959ds/431Mi)
% 22.55/9.77 % (1509825)Instruction limit reached!
% 22.55/9.77 % (1509825)------------------------------
% 22.55/9.77 % (1509825)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.55/9.77 % (1509825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.55/9.77 % (1509825)CaDiCaL version: 2.1.3
% 22.55/9.77 % (1509825)Termination reason: Instruction limit
% 22.55/9.77 % (1509825)Termination phase: SInE selection
% 22.55/9.77 % (1509825)Time elapsed: 0.111 s
% 22.55/9.77 % (1509825)Peak memory usage: 163 MB
% 22.55/9.77 % (1509825)Instructions burned: 142 (million)
% 22.55/9.77 % (1509827)Refutation not found, incomplete strategy
% 22.55/9.77 % (1509827)------------------------------
% 22.55/9.77 % (1509827)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.55/9.77 % (1509827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.55/9.77 % (1509827)CaDiCaL version: 2.1.3
% 22.55/9.77 % (1509827)Termination reason: Refutation not found, incomplete strategy
% 22.55/9.77 % (1509827)Time elapsed: 0.180 s
% 22.55/9.77 % (1509827)Peak memory usage: 171 MB
% 22.55/9.77 % (1509827)Instructions burned: 389 (million)
% 22.55/9.77 % (1509830)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=2827995619:i=6060:aac=none:ins=25_2956 on theBenchmark for (2956ds/6060Mi)
% 22.55/9.77 % (1509827)------------------------------
% 22.55/9.77 % (1509827)------------------------------
% 22.55/9.77 % (1509832)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=3405186941:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2954 on theBenchmark for (2954ds/150Mi)
% 22.55/9.77 % (1509832)Instruction limit reached!
% 22.55/9.77 % (1509832)------------------------------
% 22.55/9.77 % (1509832)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.55/9.77 % (1509832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.55/9.77 % (1509832)CaDiCaL version: 2.1.3
% 22.55/9.77 % (1509832)Termination reason: Instruction limit
% 22.55/9.77 % (1509832)Termination phase: SInE selection
% 22.55/9.77 % (1509832)Time elapsed: 0.067 s
% 22.55/9.77 % (1509832)Peak memory usage: 163 MB
% 22.55/9.77 % (1509832)Instructions burned: 150 (million)
% 22.55/9.77 % (1509834)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=2947673568:i=14155:bd=all_2952 on theBenchmark for (2952ds/14155Mi)
% 22.55/9.77 % (1509814)Instruction limit reached!
% 22.55/9.77 % (1509814)------------------------------
% 22.55/9.77 % (1509814)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.55/9.77 % (1509814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.55/9.77 % (1509814)CaDiCaL version: 2.1.3
% 22.55/9.77 % (1509814)Termination reason: Instruction limit
% 22.55/9.77 % (1509814)Termination phase: Saturation
% 22.55/9.77 % (1509814)Time elapsed: 3.343 s
% 22.55/9.77 % (1509814)Peak memory usage: 309 MB
% 22.55/9.77 % (1509814)Instructions burned: 5204 (million)
% 22.55/9.77 % (1509837)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=2434431342:i=667:av=off:fsr=off_2934 on theBenchmark for (2934ds/667Mi)
% 22.55/9.77 % (1509837)Instruction limit reached!
% 22.55/9.77 % (1509837)------------------------------
% 22.55/9.77 % (1509837)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.55/9.77 % (1509837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.55/9.77 % (1509837)CaDiCaL version: 2.1.3
% 22.55/9.77 % (1509837)Termination reason: Instruction limit
% 22.55/9.77 % (1509837)Termination phase: Preprocessing 2
% 22.55/9.77 % (1509837)Time elapsed: 0.606 s
% 22.55/9.77 % (1509837)Peak memory usage: 219 MB
% 22.55/9.77 % (1509837)Instructions burned: 667 (million)
% 22.55/9.77 % (1509839)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=4225962724:s2a=on:i=185:s2at=1.8:fdi=4_2926 on theBenchmark for (2926ds/185Mi)
% 22.55/9.77 % (1509839)Instruction limit reached!
% 22.55/9.77 % (1509839)------------------------------
% 22.55/9.77 % (1509839)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.55/9.77 % (1509839)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.55/9.77 % (1509839)CaDiCaL version: 2.1.3
% 22.55/9.77 % (1509839)Termination reason: Instruction limit
% 22.55/9.77 % (1509839)Termination phase: SInE selection
% 22.55/9.77 % (1509839)Time elapsed: 0.146 s
% 22.55/9.77 % (1509839)Peak memory usage: 163 MB
% 22.55/9.77 % (1509839)Instructions burned: 185 (million)
% 22.55/9.77 % (1509841)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=311160473:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2923 on theBenchmark for (2923ds/193Mi)
% 22.55/9.77 % (1509841)Instruction limit reached!
% 22.55/9.77 % (1509841)------------------------------
% 22.55/9.77 % (1509841)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.55/9.77 % (1509841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.55/9.77 % (1509841)CaDiCaL version: 2.1.3
% 22.55/9.77 % (1509841)Termination reason: Instruction limit
% 22.55/9.77 % (1509841)Termination phase: SInE selection
% 22.55/9.77 % (1509841)Time elapsed: 0.152 s
% 22.55/9.77 % (1509841)Peak memory usage: 164 MB
% 22.55/9.77 % (1509841)Instructions burned: 193 (million)
% 22.55/9.77 % (1509843)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=222858639:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2920 on theBenchmark for (2920ds/4850Mi)
% 22.55/9.77 % (1509725)First to succeed.
% 22.55/9.77 % (1509725)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-1509617"
% 22.55/9.77 % (1509725)Refutation found. Thanks to Tanya!
% 22.55/9.77 % SZS status Theorem for theBenchmark
% 22.55/9.77 % SZS output start Proof for theBenchmark
% See solution above
% 52.08/10.02 % (1509725)------------------------------
% 52.08/10.02 % (1509725)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.08/10.02 % (1509725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.08/10.02 % (1509725)CaDiCaL version: 2.1.3
% 52.08/10.02 % (1509725)Termination reason: Refutation
% 52.08/10.02 % (1509725)Time elapsed: 6.487 s
% 52.08/10.02 % (1509725)Peak memory usage: 394 MB
% 52.08/10.02 % (1509725)Instructions burned: 10166 (million)
% 52.08/10.02 % (1509725)------------------------------
% 52.08/10.02 % (1509725)------------------------------
% 52.08/10.02 % (1509617)Success in time 8.977 s
% 52.08/10.02 % Vampire exiting
%------------------------------------------------------------------------------