%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT339+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n015.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:47:05 AM UTC 2026
% Result : Theorem 8.69s 2.13s
% Output : Refutation 9.58s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 39
% Syntax : Number of formulae : 281 ( 36 unt; 16 def)
% Number of atoms : 1137 ( 94 equ)
% Maximal formula atoms : 15 ( 4 avg)
% Number of connectives : 1388 ( 532 ~; 613 |; 179 &)
% ( 24 <=>; 40 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 53 ( 51 usr; 16 prp; 0-3 aty)
% Number of functors : 17 ( 17 usr; 2 con; 0-3 aty)
% Number of variables : 228 ( 0 sgn 221 !; 7 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
! [X0] :
( ( ~ v3_conlat_1(X0)
& l2_conlat_1(X0) )
=> ( k3_conlat_2(X0,k1_pre_topc(k11_conlat_1(X0))) = k6_conlat_1(X0)
& k2_conlat_2(X0,k1_pre_topc(k11_conlat_1(X0))) = k5_conlat_1(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t5_conlat_2) ).
fof(f2,negated_conjecture,
~ ! [X0] :
( ( ~ v3_conlat_1(X0)
& l2_conlat_1(X0) )
=> ( k3_conlat_2(X0,k1_pre_topc(k11_conlat_1(X0))) = k6_conlat_1(X0)
& k2_conlat_2(X0,k1_pre_topc(k11_conlat_1(X0))) = k5_conlat_1(X0) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f10,axiom,
! [X0] :
( l3_lattices(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) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc2_lattices) ).
fof(f15,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( r3_lattice3(X0,X1,X2)
<=> ! [X3] :
( m1_subset_1(X3,u1_struct_0(X0))
=> ( r2_hidden(X3,X2)
=> r1_lattices(X0,X1,X3) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d16_lattice3) ).
fof(f18,axiom,
! [X0] :
( ( ~ v3_conlat_1(X0)
& l2_conlat_1(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(k11_conlat_1(X0)))
=> k12_conlat_1(X0,X1) = X1 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d24_conlat_1) ).
fof(f19,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/sandbox/benchmark/theBenchmark.p',d2_conlat_2) ).
fof(f20,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/sandbox/benchmark/theBenchmark.p',d3_conlat_2) ).
fof(f23,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/sandbox/benchmark/theBenchmark.p',dt_k11_conlat_1) ).
fof(f24,axiom,
! [X0,X1] :
( ( ~ v3_conlat_1(X0)
& l2_conlat_1(X0)
& m1_subset_1(X1,u1_struct_0(k11_conlat_1(X0))) )
=> ( v6_conlat_1(k12_conlat_1(X0,X1),X0)
& ~ v7_conlat_1(k12_conlat_1(X0,X1),X0)
& v9_conlat_1(k12_conlat_1(X0,X1),X0)
& l3_conlat_1(k12_conlat_1(X0,X1),X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k12_conlat_1) ).
fof(f28,axiom,
! [X0] :
( l1_struct_0(X0)
=> m1_subset_1(k1_pre_topc(X0),k1_zfmisc_1(u1_struct_0(X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k1_pre_topc) ).
fof(f37,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l2_lattices(X0) )
=> m1_subset_1(k6_lattices(X0),u1_struct_0(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k6_lattices) ).
fof(f39,axiom,
! [X0] :
( l1_lattices(X0)
=> l1_struct_0(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_l1_lattices) ).
fof(f42,axiom,
! [X0] :
( l2_lattices(X0)
=> l1_struct_0(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_l2_lattices) ).
fof(f44,axiom,
! [X0] :
( l3_lattices(X0)
=> ( l1_lattices(X0)
& l2_lattices(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_l3_lattices) ).
fof(f66,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/sandbox/benchmark/theBenchmark.p',fc1_conlat_2) ).
fof(f67,axiom,
! [X0] :
( l1_struct_0(X0)
=> ( v1_xboole_0(k1_pre_topc(X0))
& v1_membered(k1_pre_topc(X0))
& v2_membered(k1_pre_topc(X0))
& v3_membered(k1_pre_topc(X0))
& v4_membered(k1_pre_topc(X0))
& v5_membered(k1_pre_topc(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_pre_topc) ).
fof(f70,axiom,
v1_xboole_0(k1_xboole_0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_xboole_0) ).
fof(f108,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/sandbox/benchmark/theBenchmark.p',t1_conlat_2) ).
fof(f112,axiom,
! [X0] :
( ( ~ v3_conlat_1(X0)
& l2_conlat_1(X0) )
=> ! [X1] :
( ( ~ v7_conlat_1(X1,X0)
& v9_conlat_1(X1,X0)
& l3_conlat_1(X1,X0) )
=> ( r2_conlat_1(X0,X1,k5_conlat_1(X0))
& r2_conlat_1(X0,k6_conlat_1(X0),X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t34_conlat_1) ).
fof(f113,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] :
( X1 = k16_lattice3(X0,X2)
<=> ( r3_lattice3(X0,X1,X2)
& ! [X3] :
( m1_subset_1(X3,u1_struct_0(X0))
=> ( r3_lattice3(X0,X3,X2)
=> r3_lattices(X0,X3,X1) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t34_lattice3) ).
fof(f115,axiom,
! [X0] :
( ( ~ v3_conlat_1(X0)
& l2_conlat_1(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(k11_conlat_1(X0)))
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(k11_conlat_1(X0)))
=> ( r3_lattices(k11_conlat_1(X0),X1,X2)
<=> r2_conlat_1(X0,k12_conlat_1(X0,X1),k12_conlat_1(X0,X2)) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t47_conlat_1) ).
fof(f117,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/sandbox/benchmark/theBenchmark.p',t50_lattice3) ).
fof(f119,axiom,
! [X0] :
( v1_xboole_0(X0)
=> X0 = k1_xboole_0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t6_boole) ).
fof(f120,axiom,
! [X0,X1] :
~ ( r2_hidden(X0,X1)
& v1_xboole_0(X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t7_boole) ).
fof(f126,plain,
! [X0] :
( l1_struct_0(X0)
=> ( v1_xboole_0(k1_pre_topc(X0))
& v1_membered(k1_pre_topc(X0))
& v2_membered(k1_pre_topc(X0))
& v3_membered(k1_pre_topc(X0))
& v4_membered(k1_pre_topc(X0)) ) ),
inference(pure_predicate_removal,[],[f67]) ).
fof(f127,plain,
! [X0] :
( l1_struct_0(X0)
=> ( v1_xboole_0(k1_pre_topc(X0))
& v1_membered(k1_pre_topc(X0))
& v2_membered(k1_pre_topc(X0))
& v3_membered(k1_pre_topc(X0)) ) ),
inference(pure_predicate_removal,[],[f126]) ).
fof(f128,plain,
! [X0] :
( l1_struct_0(X0)
=> ( v1_xboole_0(k1_pre_topc(X0))
& v1_membered(k1_pre_topc(X0))
& v2_membered(k1_pre_topc(X0)) ) ),
inference(pure_predicate_removal,[],[f127]) ).
fof(f129,plain,
! [X0] :
( l1_struct_0(X0)
=> ( v1_xboole_0(k1_pre_topc(X0))
& v1_membered(k1_pre_topc(X0)) ) ),
inference(pure_predicate_removal,[],[f128]) ).
fof(f130,plain,
! [X0] :
( l1_struct_0(X0)
=> v1_xboole_0(k1_pre_topc(X0)) ),
inference(pure_predicate_removal,[],[f129]) ).
fof(f142,plain,
? [X0] :
( ( k3_conlat_2(X0,k1_pre_topc(k11_conlat_1(X0))) != k6_conlat_1(X0)
| k2_conlat_2(X0,k1_pre_topc(k11_conlat_1(X0))) != k5_conlat_1(X0) )
& ~ v3_conlat_1(X0)
& l2_conlat_1(X0) ),
inference(ennf_transformation,[],[f2]) ).
fof(f143,plain,
? [X0] :
( ( k3_conlat_2(X0,k1_pre_topc(k11_conlat_1(X0))) != k6_conlat_1(X0)
| k2_conlat_2(X0,k1_pre_topc(k11_conlat_1(X0))) != k5_conlat_1(X0) )
& ~ v3_conlat_1(X0)
& l2_conlat_1(X0) ),
inference(flattening,[],[f142]) ).
fof(f145,plain,
! [X0] :
( v1_xboole_0(k1_pre_topc(X0))
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f130]) ).
fof(f146,plain,
! [X0] :
( m1_subset_1(k1_pre_topc(X0),k1_zfmisc_1(u1_struct_0(X0)))
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f28]) ).
fof(f149,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,[],[f20]) ).
fof(f150,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,[],[f149]) ).
fof(f151,plain,
! [X0] :
( ! [X1] :
( ( r2_conlat_1(X0,X1,k5_conlat_1(X0))
& r2_conlat_1(X0,k6_conlat_1(X0),X1) )
| v7_conlat_1(X1,X0)
| ~ v9_conlat_1(X1,X0)
| ~ l3_conlat_1(X1,X0) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(ennf_transformation,[],[f112]) ).
fof(f152,plain,
! [X0] :
( ! [X1] :
( ( r2_conlat_1(X0,X1,k5_conlat_1(X0))
& r2_conlat_1(X0,k6_conlat_1(X0),X1) )
| v7_conlat_1(X1,X0)
| ~ v9_conlat_1(X1,X0)
| ~ l3_conlat_1(X1,X0) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(flattening,[],[f151]) ).
fof(f153,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,[],[f108]) ).
fof(f154,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,[],[f153]) ).
fof(f159,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,[],[f19]) ).
fof(f160,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,[],[f159]) ).
fof(f168,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l2_lattices(X0) ),
inference(ennf_transformation,[],[f42]) ).
fof(f169,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l1_lattices(X0) ),
inference(ennf_transformation,[],[f39]) ).
fof(f182,plain,
! [X0,X1] :
( ( v6_conlat_1(k12_conlat_1(X0,X1),X0)
& ~ v7_conlat_1(k12_conlat_1(X0,X1),X0)
& v9_conlat_1(k12_conlat_1(X0,X1),X0)
& l3_conlat_1(k12_conlat_1(X0,X1),X0) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0)
| ~ m1_subset_1(X1,u1_struct_0(k11_conlat_1(X0))) ),
inference(ennf_transformation,[],[f24]) ).
fof(f183,plain,
! [X0,X1] :
( ( v6_conlat_1(k12_conlat_1(X0,X1),X0)
& ~ v7_conlat_1(k12_conlat_1(X0,X1),X0)
& v9_conlat_1(k12_conlat_1(X0,X1),X0)
& l3_conlat_1(k12_conlat_1(X0,X1),X0) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0)
| ~ m1_subset_1(X1,u1_struct_0(k11_conlat_1(X0))) ),
inference(flattening,[],[f182]) ).
fof(f186,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,[],[f117]) ).
fof(f187,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,[],[f186]) ).
fof(f192,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( r3_lattices(k11_conlat_1(X0),X1,X2)
<=> r2_conlat_1(X0,k12_conlat_1(X0,X1),k12_conlat_1(X0,X2)) )
| ~ m1_subset_1(X2,u1_struct_0(k11_conlat_1(X0))) )
| ~ m1_subset_1(X1,u1_struct_0(k11_conlat_1(X0))) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(ennf_transformation,[],[f115]) ).
fof(f193,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( r3_lattices(k11_conlat_1(X0),X1,X2)
<=> r2_conlat_1(X0,k12_conlat_1(X0,X1),k12_conlat_1(X0,X2)) )
| ~ m1_subset_1(X2,u1_struct_0(k11_conlat_1(X0))) )
| ~ m1_subset_1(X1,u1_struct_0(k11_conlat_1(X0))) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(flattening,[],[f192]) ).
fof(f196,plain,
! [X0] :
( m1_subset_1(k6_lattices(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l2_lattices(X0) ),
inference(ennf_transformation,[],[f37]) ).
fof(f197,plain,
! [X0] :
( m1_subset_1(k6_lattices(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l2_lattices(X0) ),
inference(flattening,[],[f196]) ).
fof(f199,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( X1 = k16_lattice3(X0,X2)
<=> ( r3_lattice3(X0,X1,X2)
& ! [X3] :
( r3_lattices(X0,X3,X1)
| ~ r3_lattice3(X0,X3,X2)
| ~ m1_subset_1(X3,u1_struct_0(X0)) ) ) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v4_lattice3(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f113]) ).
fof(f200,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( X1 = k16_lattice3(X0,X2)
<=> ( r3_lattice3(X0,X1,X2)
& ! [X3] :
( r3_lattices(X0,X3,X1)
| ~ r3_lattice3(X0,X3,X2)
| ~ m1_subset_1(X3,u1_struct_0(X0)) ) ) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v4_lattice3(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f199]) ).
fof(f208,plain,
! [X0] :
( ( l1_lattices(X0)
& l2_lattices(X0) )
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f44]) ).
fof(f216,plain,
! [X0] :
( ! [X1] :
( k12_conlat_1(X0,X1) = X1
| ~ m1_subset_1(X1,u1_struct_0(k11_conlat_1(X0))) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(ennf_transformation,[],[f18]) ).
fof(f217,plain,
! [X0] :
( ! [X1] :
( k12_conlat_1(X0,X1) = X1
| ~ m1_subset_1(X1,u1_struct_0(k11_conlat_1(X0))) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(flattening,[],[f216]) ).
fof(f222,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,[],[f66]) ).
fof(f223,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,[],[f222]) ).
fof(f224,plain,
! [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)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f10]) ).
fof(f225,plain,
! [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)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f224]) ).
fof(f232,plain,
! [X0] :
( X0 = k1_xboole_0
| ~ v1_xboole_0(X0) ),
inference(ennf_transformation,[],[f119]) ).
fof(f239,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( r3_lattice3(X0,X1,X2)
<=> ! [X3] :
( r1_lattices(X0,X1,X3)
| ~ r2_hidden(X3,X2)
| ~ m1_subset_1(X3,u1_struct_0(X0)) ) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f15]) ).
fof(f240,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( r3_lattice3(X0,X1,X2)
<=> ! [X3] :
( r1_lattices(X0,X1,X3)
| ~ r2_hidden(X3,X2)
| ~ m1_subset_1(X3,u1_struct_0(X0)) ) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f239]) ).
fof(f258,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,[],[f23]) ).
fof(f259,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,[],[f258]) ).
fof(f260,plain,
! [X0,X1] :
( ~ r2_hidden(X0,X1)
| ~ v1_xboole_0(X1) ),
inference(ennf_transformation,[],[f120]) ).
fof(f273,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)) )
| ~ sP2(X0) ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f274,plain,
! [X0] :
( sP2(X0)
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(definition_folding,[],[f223,f273]) ).
fof(f275,plain,
( ( k3_conlat_2(sK3,k1_pre_topc(k11_conlat_1(sK3))) != k6_conlat_1(sK3)
| k2_conlat_2(sK3,k1_pre_topc(k11_conlat_1(sK3))) != k5_conlat_1(sK3) )
& ~ v3_conlat_1(sK3)
& l2_conlat_1(sK3) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(X0,sK3)],[f143]) ).
fof(f290,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( r3_lattices(k11_conlat_1(X0),X1,X2)
| ~ r2_conlat_1(X0,k12_conlat_1(X0,X1),k12_conlat_1(X0,X2)) )
& ( r2_conlat_1(X0,k12_conlat_1(X0,X1),k12_conlat_1(X0,X2))
| ~ r3_lattices(k11_conlat_1(X0),X1,X2) ) )
| ~ m1_subset_1(X2,u1_struct_0(k11_conlat_1(X0))) )
| ~ m1_subset_1(X1,u1_struct_0(k11_conlat_1(X0))) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(nnf_transformation,[],[f193]) ).
fof(f292,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( X1 = k16_lattice3(X0,X2)
| ~ r3_lattice3(X0,X1,X2)
| ? [X3] :
( ~ r3_lattices(X0,X3,X1)
& r3_lattice3(X0,X3,X2)
& m1_subset_1(X3,u1_struct_0(X0)) ) )
& ( ( r3_lattice3(X0,X1,X2)
& ! [X3] :
( r3_lattices(X0,X3,X1)
| ~ r3_lattice3(X0,X3,X2)
| ~ m1_subset_1(X3,u1_struct_0(X0)) ) )
| k16_lattice3(X0,X2) != X1 ) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v4_lattice3(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f200]) ).
fof(f293,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( X1 = k16_lattice3(X0,X2)
| ~ r3_lattice3(X0,X1,X2)
| ? [X3] :
( ~ r3_lattices(X0,X3,X1)
& r3_lattice3(X0,X3,X2)
& m1_subset_1(X3,u1_struct_0(X0)) ) )
& ( ( r3_lattice3(X0,X1,X2)
& ! [X3] :
( r3_lattices(X0,X3,X1)
| ~ r3_lattice3(X0,X3,X2)
| ~ m1_subset_1(X3,u1_struct_0(X0)) ) )
| k16_lattice3(X0,X2) != X1 ) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v4_lattice3(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f292]) ).
fof(f294,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( X1 = k16_lattice3(X0,X2)
| ~ r3_lattice3(X0,X1,X2)
| ? [X3] :
( ~ r3_lattices(X0,X3,X1)
& r3_lattice3(X0,X3,X2)
& m1_subset_1(X3,u1_struct_0(X0)) ) )
& ( ( r3_lattice3(X0,X1,X2)
& ! [X4] :
( r3_lattices(X0,X4,X1)
| ~ r3_lattice3(X0,X4,X2)
| ~ m1_subset_1(X4,u1_struct_0(X0)) ) )
| k16_lattice3(X0,X2) != X1 ) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v4_lattice3(X0)
| ~ l3_lattices(X0) ),
inference(rectify,[],[f293]) ).
fof(f295,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( X1 = k16_lattice3(X0,X2)
| ~ r3_lattice3(X0,X1,X2)
| ( ~ r3_lattices(X0,sK19(X0,X1,X2),X1)
& r3_lattice3(X0,sK19(X0,X1,X2),X2)
& m1_subset_1(sK19(X0,X1,X2),u1_struct_0(X0)) ) )
& ( ( r3_lattice3(X0,X1,X2)
& ! [X4] :
( r3_lattices(X0,X4,X1)
| ~ r3_lattice3(X0,X4,X2)
| ~ m1_subset_1(X4,u1_struct_0(X0)) ) )
| k16_lattice3(X0,X2) != X1 ) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v4_lattice3(X0)
| ~ l3_lattices(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK19]),skolemize(X3,sK19(X0,X1,X2))],[f294]) ).
fof(f305,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)) )
| ~ sP2(X0) ),
inference(nnf_transformation,[],[f273]) ).
fof(f310,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( r3_lattice3(X0,X1,X2)
| ? [X3] :
( ~ r1_lattices(X0,X1,X3)
& r2_hidden(X3,X2)
& m1_subset_1(X3,u1_struct_0(X0)) ) )
& ( ! [X3] :
( r1_lattices(X0,X1,X3)
| ~ r2_hidden(X3,X2)
| ~ m1_subset_1(X3,u1_struct_0(X0)) )
| ~ r3_lattice3(X0,X1,X2) ) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(nnf_transformation,[],[f240]) ).
fof(f311,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( r3_lattice3(X0,X1,X2)
| ? [X3] :
( ~ r1_lattices(X0,X1,X3)
& r2_hidden(X3,X2)
& m1_subset_1(X3,u1_struct_0(X0)) ) )
& ( ! [X4] :
( r1_lattices(X0,X1,X4)
| ~ r2_hidden(X4,X2)
| ~ m1_subset_1(X4,u1_struct_0(X0)) )
| ~ r3_lattice3(X0,X1,X2) ) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(rectify,[],[f310]) ).
fof(f312,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( r3_lattice3(X0,X1,X2)
| ( ~ r1_lattices(X0,X1,sK28(X0,X1,X2))
& r2_hidden(sK28(X0,X1,X2),X2)
& m1_subset_1(sK28(X0,X1,X2),u1_struct_0(X0)) ) )
& ( ! [X4] :
( r1_lattices(X0,X1,X4)
| ~ r2_hidden(X4,X2)
| ~ m1_subset_1(X4,u1_struct_0(X0)) )
| ~ r3_lattice3(X0,X1,X2) ) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK28]),skolemize(X3,sK28(X0,X1,X2))],[f311]) ).
fof(f322,plain,
l2_conlat_1(sK3),
inference(cnf_transformation,[],[f275]) ).
fof(f323,plain,
~ v3_conlat_1(sK3),
inference(cnf_transformation,[],[f275]) ).
fof(f324,plain,
( k3_conlat_2(sK3,k1_pre_topc(k11_conlat_1(sK3))) != k6_conlat_1(sK3)
| k2_conlat_2(sK3,k1_pre_topc(k11_conlat_1(sK3))) != k5_conlat_1(sK3) ),
inference(cnf_transformation,[],[f275]) ).
fof(f326,plain,
! [X0] :
( v1_xboole_0(k1_pre_topc(X0))
| ~ l1_struct_0(X0) ),
inference(cnf_transformation,[],[f145]) ).
fof(f327,plain,
! [X0] :
( m1_subset_1(k1_pre_topc(X0),k1_zfmisc_1(u1_struct_0(X0)))
| ~ l1_struct_0(X0) ),
inference(cnf_transformation,[],[f146]) ).
fof(f332,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,[],[f150]) ).
fof(f334,plain,
! [X0,X1] :
( r2_conlat_1(X0,X1,k5_conlat_1(X0))
| v7_conlat_1(X1,X0)
| ~ v9_conlat_1(X1,X0)
| ~ l3_conlat_1(X1,X0)
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f152]) ).
fof(f335,plain,
! [X0] :
( ~ l2_conlat_1(X0)
| v3_conlat_1(X0)
| k5_conlat_1(X0) = k6_lattices(k11_conlat_1(X0)) ),
inference(cnf_transformation,[],[f154]) ).
fof(f336,plain,
! [X0] :
( ~ l2_conlat_1(X0)
| v3_conlat_1(X0)
| k6_conlat_1(X0) = k5_lattices(k11_conlat_1(X0)) ),
inference(cnf_transformation,[],[f154]) ).
fof(f344,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,[],[f160]) ).
fof(f362,plain,
! [X0] :
( ~ l2_lattices(X0)
| l1_struct_0(X0) ),
inference(cnf_transformation,[],[f168]) ).
fof(f363,plain,
! [X0] :
( ~ l1_lattices(X0)
| l1_struct_0(X0) ),
inference(cnf_transformation,[],[f169]) ).
fof(f384,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,u1_struct_0(k11_conlat_1(X0)))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0)
| l3_conlat_1(k12_conlat_1(X0,X1),X0) ),
inference(cnf_transformation,[],[f183]) ).
fof(f385,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,u1_struct_0(k11_conlat_1(X0)))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0)
| v9_conlat_1(k12_conlat_1(X0,X1),X0) ),
inference(cnf_transformation,[],[f183]) ).
fof(f386,plain,
! [X0,X1] :
( ~ v7_conlat_1(k12_conlat_1(X0,X1),X0)
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0)
| ~ m1_subset_1(X1,u1_struct_0(k11_conlat_1(X0))) ),
inference(cnf_transformation,[],[f183]) ).
fof(f389,plain,
! [X0] :
( ~ v4_lattice3(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| k5_lattices(X0) = k15_lattice3(X0,k1_xboole_0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f187]) ).
fof(f397,plain,
! [X2,X0,X1] :
( ~ r2_conlat_1(X0,k12_conlat_1(X0,X1),k12_conlat_1(X0,X2))
| r3_lattices(k11_conlat_1(X0),X1,X2)
| ~ m1_subset_1(X2,u1_struct_0(k11_conlat_1(X0)))
| ~ m1_subset_1(X1,u1_struct_0(k11_conlat_1(X0)))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f290]) ).
fof(f399,plain,
! [X0] :
( m1_subset_1(k6_lattices(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l2_lattices(X0) ),
inference(cnf_transformation,[],[f197]) ).
fof(f404,plain,
! [X2,X0,X1] :
( m1_subset_1(sK19(X0,X1,X2),u1_struct_0(X0))
| ~ r3_lattice3(X0,X1,X2)
| k16_lattice3(X0,X2) = X1
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v4_lattice3(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f295]) ).
fof(f406,plain,
! [X2,X0,X1] :
( ~ r3_lattices(X0,sK19(X0,X1,X2),X1)
| ~ r3_lattice3(X0,X1,X2)
| k16_lattice3(X0,X2) = X1
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v4_lattice3(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f295]) ).
fof(f418,plain,
! [X0] :
( ~ l3_lattices(X0)
| l2_lattices(X0) ),
inference(cnf_transformation,[],[f208]) ).
fof(f419,plain,
! [X0] :
( ~ l3_lattices(X0)
| l1_lattices(X0) ),
inference(cnf_transformation,[],[f208]) ).
fof(f433,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,u1_struct_0(k11_conlat_1(X0)))
| k12_conlat_1(X0,X1) = X1
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f217]) ).
fof(f479,plain,
! [X0] :
( v4_lattice3(k11_conlat_1(X0))
| ~ sP2(X0) ),
inference(cnf_transformation,[],[f305]) ).
fof(f484,plain,
! [X0] :
( v9_lattices(k11_conlat_1(X0))
| ~ sP2(X0) ),
inference(cnf_transformation,[],[f305]) ).
fof(f485,plain,
! [X0] :
( v8_lattices(k11_conlat_1(X0))
| ~ sP2(X0) ),
inference(cnf_transformation,[],[f305]) ).
fof(f486,plain,
! [X0] :
( v7_lattices(k11_conlat_1(X0))
| ~ sP2(X0) ),
inference(cnf_transformation,[],[f305]) ).
fof(f487,plain,
! [X0] :
( v6_lattices(k11_conlat_1(X0))
| ~ sP2(X0) ),
inference(cnf_transformation,[],[f305]) ).
fof(f488,plain,
! [X0] :
( v5_lattices(k11_conlat_1(X0))
| ~ sP2(X0) ),
inference(cnf_transformation,[],[f305]) ).
fof(f489,plain,
! [X0] :
( v4_lattices(k11_conlat_1(X0))
| ~ sP2(X0) ),
inference(cnf_transformation,[],[f305]) ).
fof(f492,plain,
! [X0] :
( ~ l2_conlat_1(X0)
| v3_conlat_1(X0)
| sP2(X0) ),
inference(cnf_transformation,[],[f274]) ).
fof(f493,plain,
! [X0] :
( ~ v9_lattices(X0)
| v3_struct_0(X0)
| ~ v4_lattices(X0)
| ~ v5_lattices(X0)
| ~ v6_lattices(X0)
| ~ v7_lattices(X0)
| ~ v8_lattices(X0)
| v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f225]) ).
fof(f507,plain,
! [X0] :
( ~ v1_xboole_0(X0)
| k1_xboole_0 = X0 ),
inference(cnf_transformation,[],[f232]) ).
fof(f508,plain,
v1_xboole_0(k1_xboole_0),
inference(cnf_transformation,[],[f70]) ).
fof(f518,plain,
! [X2,X0,X1] :
( r2_hidden(sK28(X0,X1,X2),X2)
| r3_lattice3(X0,X1,X2)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f312]) ).
fof(f552,plain,
! [X0] :
( l3_lattices(k11_conlat_1(X0))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f259]) ).
fof(f554,plain,
! [X0] :
( ~ v3_struct_0(k11_conlat_1(X0))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f259]) ).
fof(f555,plain,
! [X0,X1] :
( ~ r2_hidden(X0,X1)
| ~ v1_xboole_0(X1) ),
inference(cnf_transformation,[],[f260]) ).
fof(f570,definition,
( spl36_1
<=> k2_conlat_2(sK3,k1_pre_topc(k11_conlat_1(sK3))) = k5_conlat_1(sK3) ),
introduced(definition,[new_symbols(definition,[spl36_1])],[avatar_definition]) ).
fof(f572,plain,
( k2_conlat_2(sK3,k1_pre_topc(k11_conlat_1(sK3))) != k5_conlat_1(sK3)
| spl36_1 ),
inference(avatar_component_clause,[],[f570]) ).
fof(f574,definition,
( spl36_2
<=> k3_conlat_2(sK3,k1_pre_topc(k11_conlat_1(sK3))) = k6_conlat_1(sK3) ),
introduced(definition,[new_symbols(definition,[spl36_2])],[avatar_definition]) ).
fof(f576,plain,
( k3_conlat_2(sK3,k1_pre_topc(k11_conlat_1(sK3))) != k6_conlat_1(sK3)
| spl36_2 ),
inference(avatar_component_clause,[],[f574]) ).
fof(f577,plain,
( ~ spl36_1
| ~ spl36_2 ),
inference(avatar_split_clause,[],[f324,f574,f570]) ).
fof(f602,plain,
! [X0] :
( ~ l1_struct_0(X0)
| k1_pre_topc(X0) = k1_xboole_0 ),
inference(resolution,[],[f507,f326]) ).
fof(f629,plain,
( v3_conlat_1(sK3)
| sP2(sK3) ),
inference(resolution,[],[f492,f322]) ).
fof(f631,plain,
sP2(sK3),
inference(forward_subsumption_resolution,[],[f629,f323]) ).
fof(f650,plain,
! [X0] :
( l1_lattices(k11_conlat_1(X0))
| ~ l2_conlat_1(X0)
| v3_conlat_1(X0) ),
inference(resolution,[],[f552,f419]) ).
fof(f651,plain,
! [X0] :
( l2_lattices(k11_conlat_1(X0))
| ~ l2_conlat_1(X0)
| v3_conlat_1(X0) ),
inference(resolution,[],[f552,f418]) ).
fof(f667,plain,
! [X0] :
( l1_struct_0(k11_conlat_1(X0))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(resolution,[],[f650,f363]) ).
fof(f747,plain,
( v3_conlat_1(sK3)
| k5_conlat_1(sK3) = k6_lattices(k11_conlat_1(sK3)) ),
inference(resolution,[],[f335,f322]) ).
fof(f749,plain,
k5_conlat_1(sK3) = k6_lattices(k11_conlat_1(sK3)),
inference(forward_subsumption_resolution,[],[f747,f323]) ).
fof(f750,plain,
( m1_subset_1(k5_conlat_1(sK3),u1_struct_0(k11_conlat_1(sK3)))
| v3_struct_0(k11_conlat_1(sK3))
| ~ l2_lattices(k11_conlat_1(sK3)) ),
inference(superposition,[],[f399,f749]) ).
fof(f752,definition,
( spl36_8
<=> l2_lattices(k11_conlat_1(sK3)) ),
introduced(definition,[new_symbols(definition,[spl36_8])],[avatar_definition]) ).
fof(f753,plain,
( l2_lattices(k11_conlat_1(sK3))
| ~ spl36_8 ),
inference(avatar_component_clause,[],[f752]) ).
fof(f754,plain,
( ~ l2_lattices(k11_conlat_1(sK3))
| spl36_8 ),
inference(avatar_component_clause,[],[f752]) ).
fof(f756,definition,
( spl36_9
<=> v3_struct_0(k11_conlat_1(sK3)) ),
introduced(definition,[new_symbols(definition,[spl36_9])],[avatar_definition]) ).
fof(f757,plain,
( ~ v3_struct_0(k11_conlat_1(sK3))
| spl36_9 ),
inference(avatar_component_clause,[],[f756]) ).
fof(f758,plain,
( v3_struct_0(k11_conlat_1(sK3))
| ~ spl36_9 ),
inference(avatar_component_clause,[],[f756]) ).
fof(f760,definition,
( spl36_10
<=> m1_subset_1(k5_conlat_1(sK3),u1_struct_0(k11_conlat_1(sK3))) ),
introduced(definition,[new_symbols(definition,[spl36_10])],[avatar_definition]) ).
fof(f762,plain,
( m1_subset_1(k5_conlat_1(sK3),u1_struct_0(k11_conlat_1(sK3)))
| ~ spl36_10 ),
inference(avatar_component_clause,[],[f760]) ).
fof(f763,plain,
( ~ spl36_8
| spl36_9
| spl36_10 ),
inference(avatar_split_clause,[],[f750,f760,f756,f752]) ).
fof(f764,plain,
( v3_conlat_1(sK3)
| k6_conlat_1(sK3) = k5_lattices(k11_conlat_1(sK3)) ),
inference(resolution,[],[f336,f322]) ).
fof(f766,plain,
k6_conlat_1(sK3) = k5_lattices(k11_conlat_1(sK3)),
inference(forward_subsumption_resolution,[],[f764,f323]) ).
fof(f767,plain,
( ~ l2_conlat_1(sK3)
| v3_conlat_1(sK3)
| spl36_8 ),
inference(resolution,[],[f754,f651]) ).
fof(f768,plain,
( v3_conlat_1(sK3)
| spl36_8 ),
inference(forward_subsumption_resolution,[],[f767,f322]) ).
fof(f769,plain,
( $false
| spl36_8 ),
inference(forward_subsumption_resolution,[],[f768,f323]) ).
fof(f770,plain,
spl36_8,
inference(avatar_contradiction_clause,[],[f769]) ).
fof(f774,plain,
( l1_struct_0(k11_conlat_1(sK3))
| ~ spl36_8 ),
inference(resolution,[],[f753,f362]) ).
fof(f779,plain,
( v3_conlat_1(sK3)
| ~ l2_conlat_1(sK3)
| ~ spl36_9 ),
inference(resolution,[],[f758,f554]) ).
fof(f789,plain,
( ~ l2_conlat_1(sK3)
| ~ spl36_9 ),
inference(forward_subsumption_resolution,[],[f779,f323]) ).
fof(f790,plain,
( $false
| ~ spl36_9 ),
inference(forward_subsumption_resolution,[],[f789,f322]) ).
fof(f791,plain,
~ spl36_9,
inference(avatar_contradiction_clause,[],[f790]) ).
fof(f794,plain,
( k1_xboole_0 = k1_pre_topc(k11_conlat_1(sK3))
| ~ spl36_8 ),
inference(resolution,[],[f774,f602]) ).
fof(f797,plain,
( k5_conlat_1(sK3) != k2_conlat_2(sK3,k1_xboole_0)
| spl36_1
| ~ spl36_8 ),
inference(superposition,[],[f572,f794]) ).
fof(f966,plain,
( k5_conlat_1(sK3) = k12_conlat_1(sK3,k5_conlat_1(sK3))
| v3_conlat_1(sK3)
| ~ l2_conlat_1(sK3)
| ~ spl36_10 ),
inference(resolution,[],[f433,f762]) ).
fof(f976,plain,
( k5_conlat_1(sK3) = k12_conlat_1(sK3,k5_conlat_1(sK3))
| ~ l2_conlat_1(sK3)
| ~ spl36_10 ),
inference(forward_subsumption_resolution,[],[f966,f323]) ).
fof(f982,plain,
( k5_conlat_1(sK3) = k12_conlat_1(sK3,k5_conlat_1(sK3))
| ~ spl36_10 ),
inference(forward_subsumption_resolution,[],[f976,f322]) ).
fof(f1111,plain,
! [X0] :
( k3_conlat_2(X0,k1_pre_topc(k11_conlat_1(X0))) = k15_lattice3(k11_conlat_1(X0),k1_pre_topc(k11_conlat_1(X0)))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0)
| ~ l1_struct_0(k11_conlat_1(X0)) ),
inference(resolution,[],[f332,f327]) ).
fof(f1119,plain,
! [X0] :
( ~ l2_conlat_1(X0)
| v3_conlat_1(X0)
| k3_conlat_2(X0,k1_pre_topc(k11_conlat_1(X0))) = k15_lattice3(k11_conlat_1(X0),k1_pre_topc(k11_conlat_1(X0))) ),
inference(forward_subsumption_resolution,[],[f1111,f667]) ).
fof(f1154,plain,
! [X0] :
( k2_conlat_2(X0,k1_pre_topc(k11_conlat_1(X0))) = k16_lattice3(k11_conlat_1(X0),k1_pre_topc(k11_conlat_1(X0)))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0)
| ~ l1_struct_0(k11_conlat_1(X0)) ),
inference(resolution,[],[f344,f327]) ).
fof(f1162,plain,
! [X0] :
( ~ l2_conlat_1(X0)
| v3_conlat_1(X0)
| k2_conlat_2(X0,k1_pre_topc(k11_conlat_1(X0))) = k16_lattice3(k11_conlat_1(X0),k1_pre_topc(k11_conlat_1(X0))) ),
inference(forward_subsumption_resolution,[],[f1154,f667]) ).
fof(f1186,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X1,u1_struct_0(X0))
| r3_lattice3(X0,X1,X2)
| v3_struct_0(X0)
| ~ l3_lattices(X0)
| ~ v1_xboole_0(X2) ),
inference(resolution,[],[f518,f555]) ).
fof(f1393,plain,
( ! [X0] :
( ~ r2_conlat_1(sK3,k12_conlat_1(sK3,X0),k5_conlat_1(sK3))
| r3_lattices(k11_conlat_1(sK3),X0,k5_conlat_1(sK3))
| ~ m1_subset_1(k5_conlat_1(sK3),u1_struct_0(k11_conlat_1(sK3)))
| ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK3)))
| v3_conlat_1(sK3)
| ~ l2_conlat_1(sK3) )
| ~ spl36_10 ),
inference(superposition,[],[f397,f982]) ).
fof(f1397,plain,
( ! [X0] :
( ~ r2_conlat_1(sK3,k12_conlat_1(sK3,X0),k5_conlat_1(sK3))
| r3_lattices(k11_conlat_1(sK3),X0,k5_conlat_1(sK3))
| ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK3)))
| v3_conlat_1(sK3)
| ~ l2_conlat_1(sK3) )
| ~ spl36_10 ),
inference(forward_subsumption_resolution,[],[f1393,f762]) ).
fof(f1401,plain,
( ! [X0] :
( ~ r2_conlat_1(sK3,k12_conlat_1(sK3,X0),k5_conlat_1(sK3))
| r3_lattices(k11_conlat_1(sK3),X0,k5_conlat_1(sK3))
| ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK3)))
| ~ l2_conlat_1(sK3) )
| ~ spl36_10 ),
inference(forward_subsumption_resolution,[],[f1397,f323]) ).
fof(f1405,plain,
( ! [X0] :
( ~ r2_conlat_1(sK3,k12_conlat_1(sK3,X0),k5_conlat_1(sK3))
| r3_lattices(k11_conlat_1(sK3),X0,k5_conlat_1(sK3))
| ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK3))) )
| ~ spl36_10 ),
inference(forward_subsumption_resolution,[],[f1401,f322]) ).
fof(f1533,definition,
( spl36_27
<=> l3_lattices(k11_conlat_1(sK3)) ),
introduced(definition,[new_symbols(definition,[spl36_27])],[avatar_definition]) ).
fof(f1534,plain,
( l3_lattices(k11_conlat_1(sK3))
| ~ spl36_27 ),
inference(avatar_component_clause,[],[f1533]) ).
fof(f1535,plain,
( ~ l3_lattices(k11_conlat_1(sK3))
| spl36_27 ),
inference(avatar_component_clause,[],[f1533]) ).
fof(f1537,definition,
( spl36_28
<=> v9_lattices(k11_conlat_1(sK3)) ),
introduced(definition,[new_symbols(definition,[spl36_28])],[avatar_definition]) ).
fof(f1538,plain,
( v9_lattices(k11_conlat_1(sK3))
| ~ spl36_28 ),
inference(avatar_component_clause,[],[f1537]) ).
fof(f1539,plain,
( ~ v9_lattices(k11_conlat_1(sK3))
| spl36_28 ),
inference(avatar_component_clause,[],[f1537]) ).
fof(f1541,definition,
( spl36_29
<=> v8_lattices(k11_conlat_1(sK3)) ),
introduced(definition,[new_symbols(definition,[spl36_29])],[avatar_definition]) ).
fof(f1542,plain,
( v8_lattices(k11_conlat_1(sK3))
| ~ spl36_29 ),
inference(avatar_component_clause,[],[f1541]) ).
fof(f1543,plain,
( ~ v8_lattices(k11_conlat_1(sK3))
| spl36_29 ),
inference(avatar_component_clause,[],[f1541]) ).
fof(f1545,definition,
( spl36_30
<=> v6_lattices(k11_conlat_1(sK3)) ),
introduced(definition,[new_symbols(definition,[spl36_30])],[avatar_definition]) ).
fof(f1546,plain,
( v6_lattices(k11_conlat_1(sK3))
| ~ spl36_30 ),
inference(avatar_component_clause,[],[f1545]) ).
fof(f1547,plain,
( ~ v6_lattices(k11_conlat_1(sK3))
| spl36_30 ),
inference(avatar_component_clause,[],[f1545]) ).
fof(f1554,plain,
( v3_conlat_1(sK3)
| ~ l2_conlat_1(sK3)
| spl36_27 ),
inference(resolution,[],[f1535,f552]) ).
fof(f1555,plain,
( ~ l2_conlat_1(sK3)
| spl36_27 ),
inference(forward_subsumption_resolution,[],[f1554,f323]) ).
fof(f1556,plain,
( $false
| spl36_27 ),
inference(forward_subsumption_resolution,[],[f1555,f322]) ).
fof(f1557,plain,
spl36_27,
inference(avatar_contradiction_clause,[],[f1556]) ).
fof(f1566,plain,
( ~ sP2(sK3)
| spl36_28 ),
inference(resolution,[],[f1539,f484]) ).
fof(f1573,plain,
( $false
| spl36_28 ),
inference(forward_subsumption_resolution,[],[f1566,f631]) ).
fof(f1574,plain,
spl36_28,
inference(avatar_contradiction_clause,[],[f1573]) ).
fof(f1576,plain,
( v3_struct_0(k11_conlat_1(sK3))
| ~ v4_lattices(k11_conlat_1(sK3))
| ~ v5_lattices(k11_conlat_1(sK3))
| ~ v6_lattices(k11_conlat_1(sK3))
| ~ v7_lattices(k11_conlat_1(sK3))
| ~ v8_lattices(k11_conlat_1(sK3))
| v10_lattices(k11_conlat_1(sK3))
| ~ l3_lattices(k11_conlat_1(sK3))
| ~ spl36_28 ),
inference(resolution,[],[f1538,f493]) ).
fof(f1578,plain,
( ~ sP2(sK3)
| spl36_29 ),
inference(resolution,[],[f1543,f485]) ).
fof(f1585,plain,
( $false
| spl36_29 ),
inference(forward_subsumption_resolution,[],[f1578,f631]) ).
fof(f1586,plain,
spl36_29,
inference(avatar_contradiction_clause,[],[f1585]) ).
fof(f1671,plain,
( ~ sP2(sK3)
| spl36_30 ),
inference(resolution,[],[f1547,f487]) ).
fof(f1678,plain,
( $false
| spl36_30 ),
inference(forward_subsumption_resolution,[],[f1671,f631]) ).
fof(f1679,plain,
spl36_30,
inference(avatar_contradiction_clause,[],[f1678]) ).
fof(f1680,plain,
( ~ v4_lattices(k11_conlat_1(sK3))
| ~ v5_lattices(k11_conlat_1(sK3))
| ~ v6_lattices(k11_conlat_1(sK3))
| ~ v7_lattices(k11_conlat_1(sK3))
| ~ v8_lattices(k11_conlat_1(sK3))
| v10_lattices(k11_conlat_1(sK3))
| ~ l3_lattices(k11_conlat_1(sK3))
| spl36_9
| ~ spl36_28 ),
inference(forward_subsumption_resolution,[],[f1576,f757]) ).
fof(f1681,plain,
( ~ v4_lattices(k11_conlat_1(sK3))
| ~ v5_lattices(k11_conlat_1(sK3))
| ~ v7_lattices(k11_conlat_1(sK3))
| ~ v8_lattices(k11_conlat_1(sK3))
| v10_lattices(k11_conlat_1(sK3))
| ~ l3_lattices(k11_conlat_1(sK3))
| spl36_9
| ~ spl36_28
| ~ spl36_30 ),
inference(forward_subsumption_resolution,[],[f1680,f1546]) ).
fof(f1682,plain,
( ~ v4_lattices(k11_conlat_1(sK3))
| ~ v5_lattices(k11_conlat_1(sK3))
| ~ v7_lattices(k11_conlat_1(sK3))
| v10_lattices(k11_conlat_1(sK3))
| ~ l3_lattices(k11_conlat_1(sK3))
| spl36_9
| ~ spl36_28
| ~ spl36_29
| ~ spl36_30 ),
inference(forward_subsumption_resolution,[],[f1681,f1542]) ).
fof(f1683,plain,
( ~ v4_lattices(k11_conlat_1(sK3))
| ~ v5_lattices(k11_conlat_1(sK3))
| ~ v7_lattices(k11_conlat_1(sK3))
| v10_lattices(k11_conlat_1(sK3))
| spl36_9
| ~ spl36_27
| ~ spl36_28
| ~ spl36_29
| ~ spl36_30 ),
inference(forward_subsumption_resolution,[],[f1682,f1534]) ).
fof(f1685,definition,
( spl36_50
<=> v10_lattices(k11_conlat_1(sK3)) ),
introduced(definition,[new_symbols(definition,[spl36_50])],[avatar_definition]) ).
fof(f1687,plain,
( v10_lattices(k11_conlat_1(sK3))
| ~ spl36_50 ),
inference(avatar_component_clause,[],[f1685]) ).
fof(f1689,definition,
( spl36_51
<=> v7_lattices(k11_conlat_1(sK3)) ),
introduced(definition,[new_symbols(definition,[spl36_51])],[avatar_definition]) ).
fof(f1691,plain,
( ~ v7_lattices(k11_conlat_1(sK3))
| spl36_51 ),
inference(avatar_component_clause,[],[f1689]) ).
fof(f1693,definition,
( spl36_52
<=> v5_lattices(k11_conlat_1(sK3)) ),
introduced(definition,[new_symbols(definition,[spl36_52])],[avatar_definition]) ).
fof(f1695,plain,
( ~ v5_lattices(k11_conlat_1(sK3))
| spl36_52 ),
inference(avatar_component_clause,[],[f1693]) ).
fof(f1697,definition,
( spl36_53
<=> v4_lattices(k11_conlat_1(sK3)) ),
introduced(definition,[new_symbols(definition,[spl36_53])],[avatar_definition]) ).
fof(f1699,plain,
( ~ v4_lattices(k11_conlat_1(sK3))
| spl36_53 ),
inference(avatar_component_clause,[],[f1697]) ).
fof(f1700,plain,
( spl36_50
| ~ spl36_51
| ~ spl36_52
| ~ spl36_53
| spl36_9
| ~ spl36_27
| ~ spl36_28
| ~ spl36_29
| ~ spl36_30 ),
inference(avatar_split_clause,[],[f1683,f1545,f1541,f1537,f1533,f756,f1697,f1693,f1689,f1685]) ).
fof(f1788,plain,
( ~ sP2(sK3)
| spl36_51 ),
inference(resolution,[],[f1691,f486]) ).
fof(f1795,plain,
( $false
| spl36_51 ),
inference(forward_subsumption_resolution,[],[f1788,f631]) ).
fof(f1796,plain,
spl36_51,
inference(avatar_contradiction_clause,[],[f1795]) ).
fof(f1817,plain,
( ~ sP2(sK3)
| spl36_52 ),
inference(resolution,[],[f1695,f488]) ).
fof(f1824,plain,
( $false
| spl36_52 ),
inference(forward_subsumption_resolution,[],[f1817,f631]) ).
fof(f1825,plain,
spl36_52,
inference(avatar_contradiction_clause,[],[f1824]) ).
fof(f1850,plain,
( ~ sP2(sK3)
| spl36_53 ),
inference(resolution,[],[f1699,f489]) ).
fof(f1857,plain,
( $false
| spl36_53 ),
inference(forward_subsumption_resolution,[],[f1850,f631]) ).
fof(f1858,plain,
spl36_53,
inference(avatar_contradiction_clause,[],[f1857]) ).
fof(f1887,plain,
( ! [X0] :
( r3_lattices(k11_conlat_1(sK3),X0,k5_conlat_1(sK3))
| ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK3)))
| v7_conlat_1(k12_conlat_1(sK3,X0),sK3)
| ~ v9_conlat_1(k12_conlat_1(sK3,X0),sK3)
| ~ l3_conlat_1(k12_conlat_1(sK3,X0),sK3)
| v3_conlat_1(sK3)
| ~ l2_conlat_1(sK3) )
| ~ spl36_10 ),
inference(resolution,[],[f1405,f334]) ).
fof(f1893,plain,
( ! [X0] :
( r3_lattices(k11_conlat_1(sK3),X0,k5_conlat_1(sK3))
| ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK3)))
| ~ v9_conlat_1(k12_conlat_1(sK3,X0),sK3)
| ~ l3_conlat_1(k12_conlat_1(sK3,X0),sK3)
| v3_conlat_1(sK3)
| ~ l2_conlat_1(sK3) )
| ~ spl36_10 ),
inference(forward_subsumption_resolution,[],[f1887,f386]) ).
fof(f1896,plain,
( ! [X0] :
( r3_lattices(k11_conlat_1(sK3),X0,k5_conlat_1(sK3))
| ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK3)))
| ~ l3_conlat_1(k12_conlat_1(sK3,X0),sK3)
| v3_conlat_1(sK3)
| ~ l2_conlat_1(sK3) )
| ~ spl36_10 ),
inference(forward_subsumption_resolution,[],[f1893,f385]) ).
fof(f1899,plain,
( ! [X0] :
( r3_lattices(k11_conlat_1(sK3),X0,k5_conlat_1(sK3))
| ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK3)))
| v3_conlat_1(sK3)
| ~ l2_conlat_1(sK3) )
| ~ spl36_10 ),
inference(forward_subsumption_resolution,[],[f1896,f384]) ).
fof(f1900,plain,
( ! [X0] :
( r3_lattices(k11_conlat_1(sK3),X0,k5_conlat_1(sK3))
| ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK3)))
| ~ l2_conlat_1(sK3) )
| ~ spl36_10 ),
inference(forward_subsumption_resolution,[],[f1899,f323]) ).
fof(f1901,plain,
( ! [X0] :
( r3_lattices(k11_conlat_1(sK3),X0,k5_conlat_1(sK3))
| ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK3))) )
| ~ spl36_10 ),
inference(forward_subsumption_resolution,[],[f1900,f322]) ).
fof(f1957,plain,
( ! [X0] :
( ~ m1_subset_1(sK19(k11_conlat_1(sK3),k5_conlat_1(sK3),X0),u1_struct_0(k11_conlat_1(sK3)))
| ~ r3_lattice3(k11_conlat_1(sK3),k5_conlat_1(sK3),X0)
| k5_conlat_1(sK3) = k16_lattice3(k11_conlat_1(sK3),X0)
| ~ m1_subset_1(k5_conlat_1(sK3),u1_struct_0(k11_conlat_1(sK3)))
| v3_struct_0(k11_conlat_1(sK3))
| ~ v10_lattices(k11_conlat_1(sK3))
| ~ v4_lattice3(k11_conlat_1(sK3))
| ~ l3_lattices(k11_conlat_1(sK3)) )
| ~ spl36_10 ),
inference(resolution,[],[f1901,f406]) ).
fof(f1959,plain,
( ! [X0] :
( ~ r3_lattice3(k11_conlat_1(sK3),k5_conlat_1(sK3),X0)
| k5_conlat_1(sK3) = k16_lattice3(k11_conlat_1(sK3),X0)
| ~ m1_subset_1(k5_conlat_1(sK3),u1_struct_0(k11_conlat_1(sK3)))
| v3_struct_0(k11_conlat_1(sK3))
| ~ v10_lattices(k11_conlat_1(sK3))
| ~ v4_lattice3(k11_conlat_1(sK3))
| ~ l3_lattices(k11_conlat_1(sK3)) )
| ~ spl36_10 ),
inference(forward_subsumption_resolution,[],[f1957,f404]) ).
fof(f1961,plain,
( ! [X0] :
( ~ r3_lattice3(k11_conlat_1(sK3),k5_conlat_1(sK3),X0)
| k5_conlat_1(sK3) = k16_lattice3(k11_conlat_1(sK3),X0)
| v3_struct_0(k11_conlat_1(sK3))
| ~ v10_lattices(k11_conlat_1(sK3))
| ~ v4_lattice3(k11_conlat_1(sK3))
| ~ l3_lattices(k11_conlat_1(sK3)) )
| ~ spl36_10 ),
inference(forward_subsumption_resolution,[],[f1959,f762]) ).
fof(f1963,plain,
( ! [X0] :
( ~ r3_lattice3(k11_conlat_1(sK3),k5_conlat_1(sK3),X0)
| k5_conlat_1(sK3) = k16_lattice3(k11_conlat_1(sK3),X0)
| ~ v10_lattices(k11_conlat_1(sK3))
| ~ v4_lattice3(k11_conlat_1(sK3))
| ~ l3_lattices(k11_conlat_1(sK3)) )
| spl36_9
| ~ spl36_10 ),
inference(forward_subsumption_resolution,[],[f1961,f757]) ).
fof(f1965,plain,
( ! [X0] :
( ~ r3_lattice3(k11_conlat_1(sK3),k5_conlat_1(sK3),X0)
| k5_conlat_1(sK3) = k16_lattice3(k11_conlat_1(sK3),X0)
| ~ v4_lattice3(k11_conlat_1(sK3))
| ~ l3_lattices(k11_conlat_1(sK3)) )
| spl36_9
| ~ spl36_10
| ~ spl36_50 ),
inference(forward_subsumption_resolution,[],[f1963,f1687]) ).
fof(f1967,plain,
( ! [X0] :
( ~ r3_lattice3(k11_conlat_1(sK3),k5_conlat_1(sK3),X0)
| k5_conlat_1(sK3) = k16_lattice3(k11_conlat_1(sK3),X0)
| ~ v4_lattice3(k11_conlat_1(sK3)) )
| spl36_9
| ~ spl36_10
| ~ spl36_27
| ~ spl36_50 ),
inference(forward_subsumption_resolution,[],[f1965,f1534]) ).
fof(f1970,definition,
( spl36_72
<=> v4_lattice3(k11_conlat_1(sK3)) ),
introduced(definition,[new_symbols(definition,[spl36_72])],[avatar_definition]) ).
fof(f1971,plain,
( v4_lattice3(k11_conlat_1(sK3))
| ~ spl36_72 ),
inference(avatar_component_clause,[],[f1970]) ).
fof(f1972,plain,
( ~ v4_lattice3(k11_conlat_1(sK3))
| spl36_72 ),
inference(avatar_component_clause,[],[f1970]) ).
fof(f1974,definition,
( spl36_73
<=> ! [X0] :
( ~ r3_lattice3(k11_conlat_1(sK3),k5_conlat_1(sK3),X0)
| k5_conlat_1(sK3) = k16_lattice3(k11_conlat_1(sK3),X0) ) ),
introduced(definition,[new_symbols(definition,[spl36_73])],[avatar_definition]) ).
fof(f1975,plain,
( ! [X0] :
( ~ r3_lattice3(k11_conlat_1(sK3),k5_conlat_1(sK3),X0)
| k5_conlat_1(sK3) = k16_lattice3(k11_conlat_1(sK3),X0) )
| ~ spl36_73 ),
inference(avatar_component_clause,[],[f1974]) ).
fof(f1976,plain,
( ~ spl36_72
| spl36_73
| spl36_9
| ~ spl36_10
| ~ spl36_27
| ~ spl36_50 ),
inference(avatar_split_clause,[],[f1967,f1685,f1533,f760,f756,f1974,f1970]) ).
fof(f1978,plain,
( ~ sP2(sK3)
| spl36_72 ),
inference(resolution,[],[f1972,f479]) ).
fof(f1982,plain,
( $false
| spl36_72 ),
inference(forward_subsumption_resolution,[],[f1978,f631]) ).
fof(f1983,plain,
spl36_72,
inference(avatar_contradiction_clause,[],[f1982]) ).
fof(f1989,plain,
( v3_struct_0(k11_conlat_1(sK3))
| ~ v10_lattices(k11_conlat_1(sK3))
| k5_lattices(k11_conlat_1(sK3)) = k15_lattice3(k11_conlat_1(sK3),k1_xboole_0)
| ~ l3_lattices(k11_conlat_1(sK3))
| ~ spl36_72 ),
inference(resolution,[],[f1971,f389]) ).
fof(f1991,plain,
( ~ v10_lattices(k11_conlat_1(sK3))
| k5_lattices(k11_conlat_1(sK3)) = k15_lattice3(k11_conlat_1(sK3),k1_xboole_0)
| ~ l3_lattices(k11_conlat_1(sK3))
| spl36_9
| ~ spl36_72 ),
inference(forward_subsumption_resolution,[],[f1989,f757]) ).
fof(f1992,plain,
( k5_lattices(k11_conlat_1(sK3)) = k15_lattice3(k11_conlat_1(sK3),k1_xboole_0)
| ~ l3_lattices(k11_conlat_1(sK3))
| spl36_9
| ~ spl36_50
| ~ spl36_72 ),
inference(forward_subsumption_resolution,[],[f1991,f1687]) ).
fof(f1993,plain,
( k5_lattices(k11_conlat_1(sK3)) = k15_lattice3(k11_conlat_1(sK3),k1_xboole_0)
| spl36_9
| ~ spl36_27
| ~ spl36_50
| ~ spl36_72 ),
inference(forward_subsumption_resolution,[],[f1992,f1534]) ).
fof(f1994,plain,
( k6_conlat_1(sK3) = k15_lattice3(k11_conlat_1(sK3),k1_xboole_0)
| spl36_9
| ~ spl36_27
| ~ spl36_50
| ~ spl36_72 ),
inference(forward_demodulation,[],[f1993,f766]) ).
fof(f2442,plain,
( ! [X0] :
( r3_lattice3(k11_conlat_1(sK3),k5_conlat_1(sK3),X0)
| v3_struct_0(k11_conlat_1(sK3))
| ~ l3_lattices(k11_conlat_1(sK3))
| ~ v1_xboole_0(X0) )
| ~ spl36_10 ),
inference(resolution,[],[f1186,f762]) ).
fof(f2470,plain,
( ! [X0] :
( r3_lattice3(k11_conlat_1(sK3),k5_conlat_1(sK3),X0)
| ~ l3_lattices(k11_conlat_1(sK3))
| ~ v1_xboole_0(X0) )
| spl36_9
| ~ spl36_10 ),
inference(forward_subsumption_resolution,[],[f2442,f757]) ).
fof(f2476,plain,
( ! [X0] :
( r3_lattice3(k11_conlat_1(sK3),k5_conlat_1(sK3),X0)
| ~ v1_xboole_0(X0) )
| spl36_9
| ~ spl36_10
| ~ spl36_27 ),
inference(forward_subsumption_resolution,[],[f2470,f1534]) ).
fof(f2495,plain,
( ! [X0] :
( ~ v1_xboole_0(X0)
| k5_conlat_1(sK3) = k16_lattice3(k11_conlat_1(sK3),X0) )
| spl36_9
| ~ spl36_10
| ~ spl36_27
| ~ spl36_73 ),
inference(resolution,[],[f2476,f1975]) ).
fof(f2527,plain,
( v3_conlat_1(sK3)
| k3_conlat_2(sK3,k1_pre_topc(k11_conlat_1(sK3))) = k15_lattice3(k11_conlat_1(sK3),k1_pre_topc(k11_conlat_1(sK3))) ),
inference(resolution,[],[f1119,f322]) ).
fof(f2529,plain,
k3_conlat_2(sK3,k1_pre_topc(k11_conlat_1(sK3))) = k15_lattice3(k11_conlat_1(sK3),k1_pre_topc(k11_conlat_1(sK3))),
inference(forward_subsumption_resolution,[],[f2527,f323]) ).
fof(f2530,plain,
( k3_conlat_2(sK3,k1_xboole_0) = k15_lattice3(k11_conlat_1(sK3),k1_xboole_0)
| ~ spl36_8 ),
inference(forward_demodulation,[],[f2529,f794]) ).
fof(f2531,plain,
( k6_conlat_1(sK3) = k3_conlat_2(sK3,k1_xboole_0)
| ~ spl36_8
| spl36_9
| ~ spl36_27
| ~ spl36_50
| ~ spl36_72 ),
inference(forward_demodulation,[],[f2530,f1994]) ).
fof(f2537,plain,
( v3_conlat_1(sK3)
| k2_conlat_2(sK3,k1_pre_topc(k11_conlat_1(sK3))) = k16_lattice3(k11_conlat_1(sK3),k1_pre_topc(k11_conlat_1(sK3))) ),
inference(resolution,[],[f1162,f322]) ).
fof(f2539,plain,
k2_conlat_2(sK3,k1_pre_topc(k11_conlat_1(sK3))) = k16_lattice3(k11_conlat_1(sK3),k1_pre_topc(k11_conlat_1(sK3))),
inference(forward_subsumption_resolution,[],[f2537,f323]) ).
fof(f2540,plain,
( k2_conlat_2(sK3,k1_xboole_0) = k16_lattice3(k11_conlat_1(sK3),k1_xboole_0)
| ~ spl36_8 ),
inference(forward_demodulation,[],[f2539,f794]) ).
fof(f2905,plain,
( k5_conlat_1(sK3) = k16_lattice3(k11_conlat_1(sK3),k1_xboole_0)
| spl36_9
| ~ spl36_10
| ~ spl36_27
| ~ spl36_73 ),
inference(resolution,[],[f2495,f508]) ).
fof(f2916,plain,
( k5_conlat_1(sK3) = k2_conlat_2(sK3,k1_xboole_0)
| ~ spl36_8
| spl36_9
| ~ spl36_10
| ~ spl36_27
| ~ spl36_73 ),
inference(superposition,[],[f2905,f2540]) ).
fof(f2932,plain,
( $false
| spl36_1
| ~ spl36_8
| spl36_9
| ~ spl36_10
| ~ spl36_27
| ~ spl36_73 ),
inference(forward_subsumption_resolution,[],[f2916,f797]) ).
fof(f2933,plain,
( spl36_1
| ~ spl36_8
| spl36_9
| ~ spl36_10
| ~ spl36_27
| ~ spl36_73 ),
inference(avatar_contradiction_clause,[],[f2932]) ).
fof(f2938,plain,
( k6_conlat_1(sK3) != k3_conlat_2(sK3,k1_xboole_0)
| spl36_2
| ~ spl36_8 ),
inference(forward_demodulation,[],[f576,f794]) ).
fof(f2939,plain,
( $false
| spl36_2
| ~ spl36_8
| spl36_9
| ~ spl36_27
| ~ spl36_50
| ~ spl36_72 ),
inference(forward_subsumption_resolution,[],[f2938,f2531]) ).
fof(f2940,plain,
( spl36_2
| ~ spl36_8
| spl36_9
| ~ spl36_27
| ~ spl36_50
| ~ spl36_72 ),
inference(avatar_contradiction_clause,[],[f2939]) ).
cnf(s1,plain,
( ~ spl36_1
| ~ spl36_2 ),
inference(sat_conversion,[],[f577]) ).
cnf(s9,plain,
( ~ spl36_8
| spl36_9
| spl36_10 ),
inference(sat_conversion,[],[f763]) ).
cnf(s10,plain,
spl36_8,
inference(sat_conversion,[],[f770]) ).
cnf(s14,plain,
~ spl36_9,
inference(sat_conversion,[],[f791]) ).
cnf(s29,plain,
spl36_27,
inference(sat_conversion,[],[f1557]) ).
cnf(s32,plain,
spl36_28,
inference(sat_conversion,[],[f1574]) ).
cnf(s35,plain,
spl36_29,
inference(sat_conversion,[],[f1586]) ).
cnf(s44,plain,
spl36_30,
inference(sat_conversion,[],[f1679]) ).
cnf(s45,plain,
( spl36_9
| ~ spl36_27
| ~ spl36_28
| ~ spl36_29
| ~ spl36_30
| spl36_50
| ~ spl36_51
| ~ spl36_52
| ~ spl36_53 ),
inference(sat_conversion,[],[f1700]) ).
cnf(s54,plain,
spl36_51,
inference(sat_conversion,[],[f1796]) ).
cnf(s57,plain,
spl36_52,
inference(sat_conversion,[],[f1825]) ).
cnf(s60,plain,
spl36_53,
inference(sat_conversion,[],[f1858]) ).
cnf(s66,plain,
( spl36_9
| ~ spl36_10
| ~ spl36_27
| ~ spl36_50
| ~ spl36_72
| spl36_73 ),
inference(sat_conversion,[],[f1976]) ).
cnf(s68,plain,
spl36_72,
inference(sat_conversion,[],[f1983]) ).
cnf(s87,plain,
( spl36_1
| ~ spl36_8
| spl36_9
| ~ spl36_10
| ~ spl36_27
| ~ spl36_73 ),
inference(sat_conversion,[],[f2933]) ).
cnf(s88,plain,
( spl36_2
| ~ spl36_8
| spl36_9
| ~ spl36_27
| ~ spl36_50
| ~ spl36_72 ),
inference(sat_conversion,[],[f2940]) ).
cnf(s89,plain,
( spl36_9
| ~ spl36_10
| ~ spl36_27
| ~ spl36_50
| spl36_73 ),
inference(rat,[],[s66,s68]) ).
cnf(s92,plain,
( spl36_9
| ~ spl36_27
| ~ spl36_28
| ~ spl36_29
| ~ spl36_30
| spl36_50 ),
inference(rat,[],[s45,s60,s57,s54]) ).
cnf(s96,plain,
spl36_50,
inference(rat,[],[s92,s29,s44,s35,s32,s14]) ).
cnf(s100,plain,
spl36_2,
inference(rat,[],[s88,s68,s96,s29,s14,s10]) ).
cnf(s102,plain,
spl36_10,
inference(rat,[],[s9,s14,s10]) ).
cnf(s103,plain,
spl36_73,
inference(rat,[],[s89,s96,s14,s29,s102]) ).
cnf(s107,plain,
spl36_1,
inference(rat,[],[s87,s103,s29,s10,s14,s102]) ).
cnf(s109,plain,
$false,
inference(rat,[],[s1,s100,s107]) ).
fof(f2941,plain,
$false,
inference(avatar_sat_refutation,[],[s109]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT339+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.38 % Computer : n015.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Sun Sep 27 14:51:00 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.42 Running first-order theorem proving
% 0.12/0.42 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 8.69/2.13 % (1737798)Detected formulas, will run a generic FOF schedule.
% 8.69/2.13 % (1737914)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1197072027:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 8.69/2.13 % (1737914)Refutation not found, incomplete strategy
% 8.69/2.13 % (1737914)------------------------------
% 8.69/2.13 % (1737914)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.69/2.13 % (1737914)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.69/2.13 % (1737914)CaDiCaL version: 2.1.3
% 8.69/2.13 % (1737914)Termination reason: Refutation not found, incomplete strategy
% 8.69/2.13 % (1737914)Time elapsed: 0.001 s
% 8.69/2.13 % (1737914)Peak memory usage: 88 MB
% 8.69/2.13 % (1737914)Instructions burned: 1 (million)
% 8.69/2.13 % (1737911)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=3653102625:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 8.69/2.13 % (1737915)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=337165912:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 8.69/2.13 % (1737915)Refutation not found, incomplete strategy
% 8.69/2.13 % (1737915)------------------------------
% 8.69/2.13 % (1737915)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.69/2.13 % (1737915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.69/2.13 % (1737915)CaDiCaL version: 2.1.3
% 8.69/2.13 % (1737915)Termination reason: Refutation not found, incomplete strategy
% 8.69/2.13 % (1737915)Time elapsed: 0.003 s
% 8.69/2.13 % (1737915)Peak memory usage: 88 MB
% 8.69/2.13 % (1737915)Instructions burned: 2 (million)
% 8.69/2.13 % (1737910)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=3860228288:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 8.69/2.13 % (1737912)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=3150776337:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 8.69/2.13 % (1737918)dis-21_1_sil=8000:lcm=predicate:random_seed=1851314773:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 8.69/2.13 % (1737916)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2602816865:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 8.69/2.13 % (1737918)Instruction limit reached!
% 8.69/2.13 % (1737918)------------------------------
% 8.69/2.13 % (1737918)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.69/2.13 % (1737918)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.69/2.13 % (1737918)CaDiCaL version: 2.1.3
% 8.69/2.13 % (1737918)Termination reason: Instruction limit
% 8.69/2.13 % (1737918)Termination phase: Saturation
% 8.69/2.13 % (1737918)Time elapsed: 0.074 s
% 8.69/2.13 % (1737918)Peak memory usage: 91 MB
% 8.69/2.13 % (1737918)Instructions burned: 132 (million)
% 8.69/2.13 % (1737914)------------------------------
% 8.69/2.13 % (1737914)------------------------------
% 8.69/2.13 % (1737916)Instruction limit reached!
% 8.69/2.13 % (1737916)------------------------------
% 8.69/2.13 % (1737916)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.69/2.13 % (1737916)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.69/2.13 % (1737916)CaDiCaL version: 2.1.3
% 8.69/2.13 % (1737916)Termination reason: Instruction limit
% 8.69/2.13 % (1737916)Termination phase: Saturation
% 8.69/2.13 % (1737916)Time elapsed: 0.102 s
% 8.69/2.13 % (1737916)Peak memory usage: 90 MB
% 8.69/2.13 % (1737916)Instructions burned: 140 (million)
% 8.69/2.13 % (1737980)lrs+10_1_sil=32000:urr=on:br=off:random_seed=4210951405:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 8.69/2.13 % (1737980)Refutation not found, incomplete strategy
% 8.69/2.13 % (1737980)------------------------------
% 8.69/2.13 % (1737980)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.69/2.13 % (1737980)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.69/2.13 % (1737980)CaDiCaL version: 2.1.3
% 8.69/2.13 % (1737980)Termination reason: Refutation not found, incomplete strategy
% 8.69/2.13 % (1737980)Time elapsed: 0.001 s
% 8.69/2.13 % (1737980)Peak memory usage: 89 MB
% 8.69/2.13 % (1737980)Instructions burned: 2 (million)
% 8.69/2.13 % (1737974)lrs+10_1_sil=8000:sp=occurrence:random_seed=4017867276:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 8.69/2.13 % (1737915)------------------------------
% 8.69/2.13 % (1737915)------------------------------
% 8.69/2.13 % (1737982)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1278226206:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 8.69/2.13 % (1737980)------------------------------
% 8.69/2.13 % (1737980)------------------------------
% 8.69/2.13 % (1737974)Instruction limit reached!
% 8.69/2.13 % (1737974)------------------------------
% 8.69/2.13 % (1737974)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.69/2.13 % (1737974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.69/2.13 % (1737974)CaDiCaL version: 2.1.3
% 8.69/2.13 % (1737974)Termination reason: Instruction limit
% 8.69/2.13 % (1737974)Termination phase: Saturation
% 8.69/2.13 % (1737974)Time elapsed: 0.165 s
% 8.69/2.13 % (1737974)Peak memory usage: 91 MB
% 8.69/2.13 % (1737974)Instructions burned: 286 (million)
% 8.69/2.13 % (1738015)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=2619595799:s2a=on:i=248:s2at=1.23:gtg=position_2996 on theBenchmark for (2996ds/248Mi)
% 8.69/2.13 % (1738040)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=308995320:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 8.69/2.13 % (1738040)Refutation not found, incomplete strategy
% 8.69/2.13 % (1738040)------------------------------
% 8.69/2.13 % (1738040)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.69/2.13 % (1738040)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.69/2.13 % (1738040)CaDiCaL version: 2.1.3
% 8.69/2.13 % (1738040)Termination reason: Refutation not found, incomplete strategy
% 8.69/2.13 % (1738040)Time elapsed: 0.003 s
% 8.69/2.13 % (1738040)Peak memory usage: 89 MB
% 8.69/2.13 % (1738040)Instructions burned: 7 (million)
% 8.69/2.13 % (1737982)Instruction limit reached!
% 8.69/2.13 % (1737982)------------------------------
% 8.69/2.13 % (1737982)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.69/2.13 % (1737982)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.69/2.13 % (1737982)CaDiCaL version: 2.1.3
% 8.69/2.13 % (1737982)Termination reason: Instruction limit
% 8.69/2.13 % (1737982)Termination phase: Saturation
% 8.69/2.13 % (1737982)Time elapsed: 0.197 s
% 8.69/2.13 % (1737982)Peak memory usage: 92 MB
% 8.69/2.13 % (1737982)Instructions burned: 326 (million)
% 8.69/2.13 % (1738049)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3564344377:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 8.69/2.13 % (1738015)Instruction limit reached!
% 8.69/2.13 % (1738015)------------------------------
% 8.69/2.13 % (1738015)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.69/2.13 % (1738015)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.69/2.13 % (1738015)CaDiCaL version: 2.1.3
% 8.69/2.13 % (1738015)Termination reason: Instruction limit
% 8.69/2.13 % (1738015)Termination phase: Saturation
% 8.69/2.13 % (1738015)Time elapsed: 0.154 s
% 8.69/2.13 % (1738015)Peak memory usage: 93 MB
% 8.69/2.13 % (1738015)Instructions burned: 249 (million)
% 8.69/2.13 % (1738040)------------------------------
% 8.69/2.13 % (1738040)------------------------------
% 8.69/2.13 % (1738070)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2946900625:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi)
% 8.69/2.13 % (1738089)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2515085444:i=127:av=off:fsr=off:sup=off_2993 on theBenchmark for (2993ds/127Mi)
% 8.69/2.13 % (1738103)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3947690755:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2992 on theBenchmark for (2992ds/114Mi)
% 8.69/2.13 % (1738070)Instruction limit reached!
% 8.69/2.13 % (1738070)------------------------------
% 8.69/2.13 % (1738070)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.69/2.13 % (1738070)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.69/2.13 % (1738070)CaDiCaL version: 2.1.3
% 8.69/2.13 % (1738070)Termination reason: Instruction limit
% 8.69/2.13 % (1738070)Termination phase: Saturation
% 8.69/2.13 % (1738070)Time elapsed: 0.076 s
% 8.69/2.13 % (1738103)Refutation not found, incomplete strategy
% 8.69/2.13 % (1738103)------------------------------
% 8.69/2.13 % (1738103)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.69/2.13 % (1738070)Peak memory usage: 91 MB
% 8.69/2.13 % (1738070)Instructions burned: 113 (million)
% 8.69/2.13 % (1738103)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.69/2.13 % (1738103)CaDiCaL version: 2.1.3
% 8.69/2.13 % (1738103)Termination reason: Refutation not found, incomplete strategy
% 8.69/2.13 % (1738103)Time elapsed: 0.001 s
% 8.69/2.13 % (1738103)Peak memory usage: 88 MB
% 8.69/2.13 % (1738103)Instructions burned: 2 (million)
% 8.69/2.13 % (1738089)Instruction limit reached!
% 8.69/2.13 % (1738089)------------------------------
% 8.69/2.13 % (1738089)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.69/2.13 % (1738089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.69/2.13 % (1738089)CaDiCaL version: 2.1.3
% 8.69/2.13 % (1738089)Termination reason: Instruction limit
% 8.69/2.13 % (1738089)Termination phase: Saturation
% 8.69/2.13 % (1738089)Time elapsed: 0.069 s
% 8.69/2.13 % (1738089)Peak memory usage: 89 MB
% 8.69/2.13 % (1738089)Instructions burned: 128 (million)
% 8.69/2.13 % (1738127)lrs+10_1_sil=8000:sp=occurrence:random_seed=784429256:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2991 on theBenchmark for (2991ds/907Mi)
% 8.69/2.13 % (1738103)------------------------------
% 8.69/2.13 % (1738103)------------------------------
% 8.69/2.13 % (1738141)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=303498027:i=437:sd=1:aac=none:ss=included_2991 on theBenchmark for (2991ds/437Mi)
% 8.69/2.13 % (1738127)First to succeed.
% 8.69/2.13 % (1738141)Refutation not found, incomplete strategy
% 8.69/2.13 % (1738141)------------------------------
% 8.69/2.13 % (1738141)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.69/2.13 % (1738141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.69/2.13 % (1738141)CaDiCaL version: 2.1.3
% 8.69/2.13 % (1738141)Termination reason: Refutation not found, incomplete strategy
% 8.69/2.13 % (1738141)Time elapsed: 0.007 s
% 8.69/2.13 % (1738141)Peak memory usage: 89 MB
% 8.69/2.13 % (1738141)Instructions burned: 11 (million)
% 8.69/2.13 % (1738127)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1737798"
% 8.69/2.13 % (1738167)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2049940001:i=5202:ss=axioms:sgt=16_2990 on theBenchmark for (2990ds/5202Mi)
% 8.69/2.13 % (1738141)------------------------------
% 8.69/2.13 % (1738141)------------------------------
% 8.69/2.13 % (1738127)Refutation found. Thanks to Tanya!
% 8.69/2.13 % SZS status Theorem for theBenchmark
% 8.69/2.13 % SZS output start Proof for theBenchmark
% See solution above
% 9.58/2.32 % (1738127)------------------------------
% 9.58/2.32 % (1738127)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.58/2.32 % (1738127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.58/2.32 % (1738127)CaDiCaL version: 2.1.3
% 9.58/2.32 % (1738127)Termination reason: Refutation
% 9.58/2.32 % (1738127)Time elapsed: 0.065 s
% 9.58/2.32 % (1738127)Peak memory usage: 91 MB
% 9.58/2.32 % (1738127)Instructions burned: 97 (million)
% 9.58/2.32 % (1738127)------------------------------
% 9.58/2.32 % (1738127)------------------------------
% 9.58/2.32 % (1737798)Success in time 1.278 s
% 9.58/2.32 % Vampire exiting
%------------------------------------------------------------------------------