%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : LAT339+1 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n002.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:48:30 AM UTC 2026
% Result : Theorem 34.38s 5.36s
% Output : Refutation 34.38s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 32
% Syntax : Number of formulae : 242 ( 28 unt; 9 def)
% Number of atoms : 1041 ( 108 equ)
% Maximal formula atoms : 15 ( 4 avg)
% Number of connectives : 1276 ( 477 ~; 562 |; 180 &)
% ( 17 <=>; 40 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 6 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 45 ( 43 usr; 9 prp; 0-3 aty)
% Number of functors : 19 ( 19 usr; 2 con; 0-3 aty)
% Number of variables : 242 ( 0 sgn 234 !; 8 ?)
% 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/sandbox2/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(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/sandbox2/benchmark/theBenchmark.p',d16_lattice3) ).
fof(f16,axiom,
! [X0] :
( ( ~ v3_conlat_1(X0)
& l2_conlat_1(X0) )
=> ! [X1] :
( ( v6_conlat_1(X1,X0)
& ~ v7_conlat_1(X1,X0)
& v9_conlat_1(X1,X0)
& l3_conlat_1(X1,X0) )
=> k1_conlat_2(X0,X1) = X1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d1_conlat_2) ).
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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/benchmark/theBenchmark.p',dt_k12_conlat_1) ).
fof(f27,axiom,
! [X0,X1] :
( ( ~ v3_conlat_1(X0)
& l2_conlat_1(X0)
& v6_conlat_1(X1,X0)
& ~ v7_conlat_1(X1,X0)
& v9_conlat_1(X1,X0)
& l3_conlat_1(X1,X0) )
=> m1_subset_1(k1_conlat_2(X0,X1),u1_struct_0(k11_conlat_1(X0))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k1_conlat_2) ).
fof(f34,axiom,
! [X0] :
( ( ~ v3_conlat_1(X0)
& l2_conlat_1(X0) )
=> ( v6_conlat_1(k5_conlat_1(X0),X0)
& ~ v7_conlat_1(k5_conlat_1(X0),X0)
& v9_conlat_1(k5_conlat_1(X0),X0)
& v10_conlat_1(k5_conlat_1(X0),X0)
& l3_conlat_1(k5_conlat_1(X0),X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k5_conlat_1) ).
fof(f42,axiom,
! [X0] :
( l2_lattices(X0)
=> l1_struct_0(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l2_lattices) ).
fof(f44,axiom,
! [X0] :
( l3_lattices(X0)
=> ( l1_lattices(X0)
& l2_lattices(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l3_lattices) ).
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/sandbox2/benchmark/theBenchmark.p',fc1_pre_topc) ).
fof(f70,axiom,
v1_xboole_0(k1_xboole_0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_xboole_0) ).
fof(f78,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(f95,axiom,
! [X0] :
? [X1] :
( m1_subset_1(X1,k1_zfmisc_1(X0))
& v1_xboole_0(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc2_subset_1) ).
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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/benchmark/theBenchmark.p',t50_lattice3) ).
fof(f119,axiom,
! [X0] :
( v1_xboole_0(X0)
=> X0 = k1_xboole_0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t6_boole) ).
fof(f120,axiom,
! [X0,X1] :
~ ( r2_hidden(X0,X1)
& v1_xboole_0(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t7_boole) ).
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))
& v3_membered(k1_pre_topc(X0))
& v4_membered(k1_pre_topc(X0)) ) ),
inference(pure_predicate_removal,[],[f67]) ).
fof(f129,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,[],[f128]) ).
fof(f130,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,[],[f129]) ).
fof(f131,plain,
! [X0] :
( l1_struct_0(X0)
=> ( v1_xboole_0(k1_pre_topc(X0))
& v1_membered(k1_pre_topc(X0)) ) ),
inference(pure_predicate_removal,[],[f130]) ).
fof(f132,plain,
! [X0] :
( l1_struct_0(X0)
=> v1_xboole_0(k1_pre_topc(X0)) ),
inference(pure_predicate_removal,[],[f131]) ).
fof(f135,plain,
! [X0] :
( ( ~ v3_conlat_1(X0)
& l2_conlat_1(X0) )
=> ( v6_conlat_1(k5_conlat_1(X0),X0)
& ~ v7_conlat_1(k5_conlat_1(X0),X0)
& v9_conlat_1(k5_conlat_1(X0),X0)
& l3_conlat_1(k5_conlat_1(X0),X0) ) ),
inference(pure_predicate_removal,[],[f34]) ).
fof(f146,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(f147,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,[],[f146]) ).
fof(f167,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(f168,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,[],[f167]) ).
fof(f169,plain,
! [X0] :
( ! [X1] :
( k1_conlat_2(X0,X1) = X1
| ~ v6_conlat_1(X1,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(ennf_transformation,[],[f16]) ).
fof(f170,plain,
! [X0] :
( ! [X1] :
( k1_conlat_2(X0,X1) = X1
| ~ v6_conlat_1(X1,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(flattening,[],[f169]) ).
fof(f173,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(f174,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,[],[f173]) ).
fof(f175,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(f176,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,[],[f175]) ).
fof(f177,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(f178,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,[],[f177]) ).
fof(f183,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(f184,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,[],[f183]) ).
fof(f185,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(f186,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,[],[f185]) ).
fof(f191,plain,
! [X0,X1] :
( m1_subset_1(k1_conlat_2(X0,X1),u1_struct_0(k11_conlat_1(X0)))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0)
| ~ v6_conlat_1(X1,X0)
| v7_conlat_1(X1,X0)
| ~ v9_conlat_1(X1,X0)
| ~ l3_conlat_1(X1,X0) ),
inference(ennf_transformation,[],[f27]) ).
fof(f192,plain,
! [X0,X1] :
( m1_subset_1(k1_conlat_2(X0,X1),u1_struct_0(k11_conlat_1(X0)))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0)
| ~ v6_conlat_1(X1,X0)
| v7_conlat_1(X1,X0)
| ~ v9_conlat_1(X1,X0)
| ~ l3_conlat_1(X1,X0) ),
inference(flattening,[],[f191]) ).
fof(f198,plain,
! [X0] :
( ( v6_conlat_1(k5_conlat_1(X0),X0)
& ~ v7_conlat_1(k5_conlat_1(X0),X0)
& v9_conlat_1(k5_conlat_1(X0),X0)
& l3_conlat_1(k5_conlat_1(X0),X0) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(ennf_transformation,[],[f135]) ).
fof(f199,plain,
! [X0] :
( ( v6_conlat_1(k5_conlat_1(X0),X0)
& ~ v7_conlat_1(k5_conlat_1(X0),X0)
& v9_conlat_1(k5_conlat_1(X0),X0)
& l3_conlat_1(k5_conlat_1(X0),X0) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(flattening,[],[f198]) ).
fof(f208,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l2_lattices(X0) ),
inference(ennf_transformation,[],[f42]) ).
fof(f209,plain,
! [X0] :
( ( l1_lattices(X0)
& l2_lattices(X0) )
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f44]) ).
fof(f222,plain,
! [X0] :
( v1_xboole_0(k1_pre_topc(X0))
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f132]) ).
fof(f239,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,[],[f78]) ).
fof(f240,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,[],[f239]) ).
fof(f273,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(f274,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,[],[f273]) ).
fof(f279,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(f280,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,[],[f279]) ).
fof(f281,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(f282,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,[],[f281]) ).
fof(f284,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(f285,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,[],[f284]) ).
fof(f288,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(f289,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,[],[f288]) ).
fof(f291,plain,
! [X0] :
( X0 = k1_xboole_0
| ~ v1_xboole_0(X0) ),
inference(ennf_transformation,[],[f119]) ).
fof(f292,plain,
! [X0,X1] :
( ~ r2_hidden(X0,X1)
| ~ v1_xboole_0(X1) ),
inference(ennf_transformation,[],[f120]) ).
fof(f298,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))
& v4_lattice3(k11_conlat_1(X0)) )
| ~ sP2(X0) ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f299,plain,
! [X0] :
( sP2(X0)
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(definition_folding,[],[f240,f298]) ).
fof(f300,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)],[f147]) ).
fof(f301,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,[],[f168]) ).
fof(f302,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,[],[f301]) ).
fof(f303,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( r3_lattice3(X0,X1,X2)
| ( ~ r1_lattices(X0,X1,sK4(X0,X1,X2))
& r2_hidden(sK4(X0,X1,X2),X2)
& m1_subset_1(sK4(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,[sK4]),skolemize(X3,sK4(X0,X1,X2))],[f302]) ).
fof(f316,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)) )
| ~ sP2(X0) ),
inference(nnf_transformation,[],[f298]) ).
fof(f332,plain,
! [X0] :
( m1_subset_1(sK28(X0),k1_zfmisc_1(X0))
& v1_xboole_0(sK28(X0)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK28]),skolemize(X1,sK28(X0))],[f95]) ).
fof(f345,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,[],[f282]) ).
fof(f346,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,[],[f345]) ).
fof(f347,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,[],[f346]) ).
fof(f348,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( X1 = k16_lattice3(X0,X2)
| ~ r3_lattice3(X0,X1,X2)
| ( ~ r3_lattices(X0,sK38(X0,X1,X2),X1)
& r3_lattice3(X0,sK38(X0,X1,X2),X2)
& m1_subset_1(sK38(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,[sK38]),skolemize(X3,sK38(X0,X1,X2))],[f347]) ).
fof(f349,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,[],[f285]) ).
fof(f350,plain,
l2_conlat_1(sK3),
inference(cnf_transformation,[],[f300]) ).
fof(f351,plain,
~ v3_conlat_1(sK3),
inference(cnf_transformation,[],[f300]) ).
fof(f352,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,[],[f300]) ).
fof(f381,plain,
! [X2,X0,X1] :
( r2_hidden(sK4(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,[],[f303]) ).
fof(f383,plain,
! [X0,X1] :
( ~ v9_conlat_1(X1,X0)
| ~ v6_conlat_1(X1,X0)
| v7_conlat_1(X1,X0)
| k1_conlat_2(X0,X1) = X1
| ~ l3_conlat_1(X1,X0)
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f170]) ).
fof(f385,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,[],[f174]) ).
fof(f386,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,[],[f176]) ).
fof(f387,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,[],[f178]) ).
fof(f392,plain,
! [X0] :
( l3_lattices(k11_conlat_1(X0))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f184]) ).
fof(f394,plain,
! [X0] :
( ~ v3_struct_0(k11_conlat_1(X0))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f184]) ).
fof(f395,plain,
! [X0,X1] :
( 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(cnf_transformation,[],[f186]) ).
fof(f396,plain,
! [X0,X1] :
( v9_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,[],[f186]) ).
fof(f397,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,[],[f186]) ).
fof(f401,plain,
! [X0,X1] :
( m1_subset_1(k1_conlat_2(X0,X1),u1_struct_0(k11_conlat_1(X0)))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0)
| ~ v6_conlat_1(X1,X0)
| v7_conlat_1(X1,X0)
| ~ v9_conlat_1(X1,X0)
| ~ l3_conlat_1(X1,X0) ),
inference(cnf_transformation,[],[f192]) ).
fof(f409,plain,
! [X0] :
( l3_conlat_1(k5_conlat_1(X0),X0)
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f199]) ).
fof(f410,plain,
! [X0] :
( v9_conlat_1(k5_conlat_1(X0),X0)
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f199]) ).
fof(f411,plain,
! [X0] :
( ~ v7_conlat_1(k5_conlat_1(X0),X0)
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f199]) ).
fof(f412,plain,
! [X0] :
( v6_conlat_1(k5_conlat_1(X0),X0)
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f199]) ).
fof(f421,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l2_lattices(X0) ),
inference(cnf_transformation,[],[f208]) ).
fof(f422,plain,
! [X0] :
( l2_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f209]) ).
fof(f458,plain,
! [X0] :
( v1_xboole_0(k1_pre_topc(X0))
| ~ l1_struct_0(X0) ),
inference(cnf_transformation,[],[f222]) ).
fof(f461,plain,
v1_xboole_0(k1_xboole_0),
inference(cnf_transformation,[],[f70]) ).
fof(f485,plain,
! [X0] :
( v4_lattice3(k11_conlat_1(X0))
| ~ sP2(X0) ),
inference(cnf_transformation,[],[f316]) ).
fof(f486,plain,
! [X0] :
( v10_lattices(k11_conlat_1(X0))
| ~ sP2(X0) ),
inference(cnf_transformation,[],[f316]) ).
fof(f495,plain,
! [X0] :
( sP2(X0)
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f299]) ).
fof(f552,plain,
! [X0] : v1_xboole_0(sK28(X0)),
inference(cnf_transformation,[],[f332]) ).
fof(f553,plain,
! [X0] : m1_subset_1(sK28(X0),k1_zfmisc_1(X0)),
inference(cnf_transformation,[],[f332]) ).
fof(f585,plain,
! [X0] :
( ~ l2_conlat_1(X0)
| v3_conlat_1(X0)
| k6_conlat_1(X0) = k5_lattices(k11_conlat_1(X0)) ),
inference(cnf_transformation,[],[f274]) ).
fof(f591,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,[],[f280]) ).
fof(f594,plain,
! [X2,X0,X1] :
( m1_subset_1(sK38(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,[],[f348]) ).
fof(f596,plain,
! [X2,X0,X1] :
( ~ r3_lattices(X0,sK38(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,[],[f348]) ).
fof(f599,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,[],[f349]) ).
fof(f601,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,[],[f289]) ).
fof(f607,plain,
! [X0] :
( ~ v1_xboole_0(X0)
| k1_xboole_0 = X0 ),
inference(cnf_transformation,[],[f291]) ).
fof(f608,plain,
! [X0,X1] :
( ~ r2_hidden(X0,X1)
| ~ v1_xboole_0(X1) ),
inference(cnf_transformation,[],[f292]) ).
fof(f614,definition,
( spl39_1
<=> k2_conlat_2(sK3,k1_pre_topc(k11_conlat_1(sK3))) = k5_conlat_1(sK3) ),
introduced(definition,[new_symbols(definition,[spl39_1])],[avatar_definition]) ).
fof(f616,plain,
( k2_conlat_2(sK3,k1_pre_topc(k11_conlat_1(sK3))) != k5_conlat_1(sK3)
| spl39_1 ),
inference(avatar_component_clause,[],[f614]) ).
fof(f618,definition,
( spl39_2
<=> k3_conlat_2(sK3,k1_pre_topc(k11_conlat_1(sK3))) = k6_conlat_1(sK3) ),
introduced(definition,[new_symbols(definition,[spl39_2])],[avatar_definition]) ).
fof(f620,plain,
( k3_conlat_2(sK3,k1_pre_topc(k11_conlat_1(sK3))) != k6_conlat_1(sK3)
| spl39_2 ),
inference(avatar_component_clause,[],[f618]) ).
fof(f621,plain,
( ~ spl39_1
| ~ spl39_2 ),
inference(avatar_split_clause,[],[f352,f618,f614]) ).
fof(f622,plain,
! [X0] :
( ~ l1_struct_0(X0)
| k1_pre_topc(X0) = k1_xboole_0 ),
inference(resolution,[],[f607,f458]) ).
fof(f625,plain,
! [X0] : k1_xboole_0 = sK28(X0),
inference(resolution,[],[f607,f552]) ).
fof(f631,plain,
! [X0] :
( ~ l2_lattices(X0)
| k1_pre_topc(X0) = k1_xboole_0 ),
inference(resolution,[],[f622,f421]) ).
fof(f636,plain,
! [X0] :
( ~ l3_lattices(X0)
| k1_pre_topc(X0) = k1_xboole_0 ),
inference(resolution,[],[f631,f422]) ).
fof(f641,plain,
! [X0] :
( ~ l2_conlat_1(X0)
| v3_conlat_1(X0)
| k1_pre_topc(k11_conlat_1(X0)) = k1_xboole_0 ),
inference(resolution,[],[f636,f392]) ).
fof(f739,plain,
( v3_conlat_1(sK3)
| k1_xboole_0 = k1_pre_topc(k11_conlat_1(sK3)) ),
inference(resolution,[],[f641,f350]) ).
fof(f750,plain,
k1_xboole_0 = k1_pre_topc(k11_conlat_1(sK3)),
inference(forward_subsumption_resolution,[],[f739,f351]) ).
fof(f752,plain,
( k6_conlat_1(sK3) != k3_conlat_2(sK3,k1_xboole_0)
| spl39_2 ),
inference(superposition,[],[f620,f750]) ).
fof(f772,definition,
( spl39_9
<=> v3_struct_0(k11_conlat_1(sK3)) ),
introduced(definition,[new_symbols(definition,[spl39_9])],[avatar_definition]) ).
fof(f773,plain,
( ~ v3_struct_0(k11_conlat_1(sK3))
| spl39_9 ),
inference(avatar_component_clause,[],[f772]) ).
fof(f774,plain,
( v3_struct_0(k11_conlat_1(sK3))
| ~ spl39_9 ),
inference(avatar_component_clause,[],[f772]) ).
fof(f776,definition,
( spl39_10
<=> m1_subset_1(k5_conlat_1(sK3),u1_struct_0(k11_conlat_1(sK3))) ),
introduced(definition,[new_symbols(definition,[spl39_10])],[avatar_definition]) ).
fof(f778,plain,
( m1_subset_1(k5_conlat_1(sK3),u1_struct_0(k11_conlat_1(sK3)))
| ~ spl39_10 ),
inference(avatar_component_clause,[],[f776]) ).
fof(f780,plain,
( v3_conlat_1(sK3)
| k6_conlat_1(sK3) = k5_lattices(k11_conlat_1(sK3)) ),
inference(resolution,[],[f585,f350]) ).
fof(f787,plain,
k6_conlat_1(sK3) = k5_lattices(k11_conlat_1(sK3)),
inference(forward_subsumption_resolution,[],[f780,f351]) ).
fof(f802,plain,
( v3_conlat_1(sK3)
| ~ l2_conlat_1(sK3)
| ~ spl39_9 ),
inference(resolution,[],[f774,f394]) ).
fof(f806,plain,
( ~ l2_conlat_1(sK3)
| ~ spl39_9 ),
inference(forward_subsumption_resolution,[],[f802,f351]) ).
fof(f807,plain,
( $false
| ~ spl39_9 ),
inference(forward_subsumption_resolution,[],[f806,f350]) ).
fof(f808,plain,
~ spl39_9,
inference(avatar_contradiction_clause,[],[f807]) ).
fof(f911,plain,
( k5_conlat_1(sK3) = k12_conlat_1(sK3,k5_conlat_1(sK3))
| v3_conlat_1(sK3)
| ~ l2_conlat_1(sK3)
| ~ spl39_10 ),
inference(resolution,[],[f385,f778]) ).
fof(f921,plain,
( k5_conlat_1(sK3) = k12_conlat_1(sK3,k5_conlat_1(sK3))
| ~ l2_conlat_1(sK3)
| ~ spl39_10 ),
inference(forward_subsumption_resolution,[],[f911,f351]) ).
fof(f925,plain,
( k5_conlat_1(sK3) = k12_conlat_1(sK3,k5_conlat_1(sK3))
| ~ spl39_10 ),
inference(forward_subsumption_resolution,[],[f921,f350]) ).
fof(f1153,plain,
! [X2,X0,X1] :
( r3_lattice3(X0,X1,X2)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0)
| ~ v1_xboole_0(X2) ),
inference(resolution,[],[f381,f608]) ).
fof(f1165,plain,
! [X0] :
( k2_conlat_2(X0,sK28(u1_struct_0(k11_conlat_1(X0)))) = k16_lattice3(k11_conlat_1(X0),sK28(u1_struct_0(k11_conlat_1(X0))))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(resolution,[],[f386,f553]) ).
fof(f1170,plain,
! [X0] :
( ~ l2_conlat_1(X0)
| v3_conlat_1(X0)
| k2_conlat_2(X0,k1_xboole_0) = k16_lattice3(k11_conlat_1(X0),k1_xboole_0) ),
inference(forward_demodulation,[],[f1165,f625]) ).
fof(f1177,plain,
! [X0] :
( k3_conlat_2(X0,sK28(u1_struct_0(k11_conlat_1(X0)))) = k15_lattice3(k11_conlat_1(X0),sK28(u1_struct_0(k11_conlat_1(X0))))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(resolution,[],[f387,f553]) ).
fof(f1182,plain,
! [X0] :
( ~ l2_conlat_1(X0)
| v3_conlat_1(X0)
| k15_lattice3(k11_conlat_1(X0),k1_xboole_0) = k3_conlat_2(X0,k1_xboole_0) ),
inference(forward_demodulation,[],[f1177,f625]) ).
fof(f1200,plain,
! [X0] :
( ~ v6_conlat_1(k5_conlat_1(X0),X0)
| v7_conlat_1(k5_conlat_1(X0),X0)
| k5_conlat_1(X0) = k1_conlat_2(X0,k5_conlat_1(X0))
| ~ l3_conlat_1(k5_conlat_1(X0),X0)
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0)
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(resolution,[],[f383,f410]) ).
fof(f1211,plain,
! [X0] :
( ~ v6_conlat_1(k5_conlat_1(X0),X0)
| v7_conlat_1(k5_conlat_1(X0),X0)
| k5_conlat_1(X0) = k1_conlat_2(X0,k5_conlat_1(X0))
| ~ l3_conlat_1(k5_conlat_1(X0),X0)
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(duplicate_literal_removal,[],[f1200]) ).
fof(f1220,plain,
! [X0] :
( v7_conlat_1(k5_conlat_1(X0),X0)
| k5_conlat_1(X0) = k1_conlat_2(X0,k5_conlat_1(X0))
| ~ l3_conlat_1(k5_conlat_1(X0),X0)
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(forward_subsumption_resolution,[],[f1211,f412]) ).
fof(f1229,plain,
! [X0] :
( k5_conlat_1(X0) = k1_conlat_2(X0,k5_conlat_1(X0))
| ~ l3_conlat_1(k5_conlat_1(X0),X0)
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(forward_subsumption_resolution,[],[f1220,f411]) ).
fof(f1236,plain,
! [X0] :
( ~ l2_conlat_1(X0)
| v3_conlat_1(X0)
| k5_conlat_1(X0) = k1_conlat_2(X0,k5_conlat_1(X0)) ),
inference(forward_subsumption_resolution,[],[f1229,f409]) ).
fof(f1264,definition,
( spl39_22
<=> l3_lattices(k11_conlat_1(sK3)) ),
introduced(definition,[new_symbols(definition,[spl39_22])],[avatar_definition]) ).
fof(f1265,plain,
( l3_lattices(k11_conlat_1(sK3))
| ~ spl39_22 ),
inference(avatar_component_clause,[],[f1264]) ).
fof(f1266,plain,
( ~ l3_lattices(k11_conlat_1(sK3))
| spl39_22 ),
inference(avatar_component_clause,[],[f1264]) ).
fof(f1316,definition,
( spl39_26
<=> v10_lattices(k11_conlat_1(sK3)) ),
introduced(definition,[new_symbols(definition,[spl39_26])],[avatar_definition]) ).
fof(f1317,plain,
( ~ v10_lattices(k11_conlat_1(sK3))
| spl39_26 ),
inference(avatar_component_clause,[],[f1316]) ).
fof(f1318,plain,
( v10_lattices(k11_conlat_1(sK3))
| ~ spl39_26 ),
inference(avatar_component_clause,[],[f1316]) ).
fof(f1367,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) )
| ~ spl39_10 ),
inference(superposition,[],[f599,f925]) ).
fof(f1371,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) )
| ~ spl39_10 ),
inference(forward_subsumption_resolution,[],[f1367,f778]) ).
fof(f1375,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) )
| ~ spl39_10 ),
inference(forward_subsumption_resolution,[],[f1371,f351]) ).
fof(f1379,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))) )
| ~ spl39_10 ),
inference(forward_subsumption_resolution,[],[f1375,f350]) ).
fof(f1624,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) )
| ~ spl39_10 ),
inference(resolution,[],[f1379,f591]) ).
fof(f1628,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) )
| ~ spl39_10 ),
inference(forward_subsumption_resolution,[],[f1624,f397]) ).
fof(f1629,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) )
| ~ spl39_10 ),
inference(forward_subsumption_resolution,[],[f1628,f396]) ).
fof(f1630,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) )
| ~ spl39_10 ),
inference(forward_subsumption_resolution,[],[f1629,f395]) ).
fof(f1631,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) )
| ~ spl39_10 ),
inference(forward_subsumption_resolution,[],[f1630,f351]) ).
fof(f1632,plain,
( ! [X0] :
( r3_lattices(k11_conlat_1(sK3),X0,k5_conlat_1(sK3))
| ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK3))) )
| ~ spl39_10 ),
inference(forward_subsumption_resolution,[],[f1631,f350]) ).
fof(f1650,plain,
( ! [X0] :
( ~ m1_subset_1(sK38(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)) )
| ~ spl39_10 ),
inference(resolution,[],[f1632,f596]) ).
fof(f1651,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)) )
| ~ spl39_10 ),
inference(forward_subsumption_resolution,[],[f1650,f594]) ).
fof(f1652,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)) )
| ~ spl39_10 ),
inference(forward_subsumption_resolution,[],[f1651,f778]) ).
fof(f1653,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)) )
| spl39_9
| ~ spl39_10 ),
inference(forward_subsumption_resolution,[],[f1652,f773]) ).
fof(f1654,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)) )
| spl39_9
| ~ spl39_10
| ~ spl39_26 ),
inference(forward_subsumption_resolution,[],[f1653,f1318]) ).
fof(f1655,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)) )
| spl39_9
| ~ spl39_10
| ~ spl39_22
| ~ spl39_26 ),
inference(forward_subsumption_resolution,[],[f1654,f1265]) ).
fof(f1657,definition,
( spl39_70
<=> v4_lattice3(k11_conlat_1(sK3)) ),
introduced(definition,[new_symbols(definition,[spl39_70])],[avatar_definition]) ).
fof(f1658,plain,
( v4_lattice3(k11_conlat_1(sK3))
| ~ spl39_70 ),
inference(avatar_component_clause,[],[f1657]) ).
fof(f1659,plain,
( ~ v4_lattice3(k11_conlat_1(sK3))
| spl39_70 ),
inference(avatar_component_clause,[],[f1657]) ).
fof(f1661,definition,
( spl39_71
<=> ! [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,[spl39_71])],[avatar_definition]) ).
fof(f1662,plain,
( ! [X0] :
( ~ r3_lattice3(k11_conlat_1(sK3),k5_conlat_1(sK3),X0)
| k5_conlat_1(sK3) = k16_lattice3(k11_conlat_1(sK3),X0) )
| ~ spl39_71 ),
inference(avatar_component_clause,[],[f1661]) ).
fof(f1663,plain,
( ~ spl39_70
| spl39_71
| spl39_9
| ~ spl39_10
| ~ spl39_22
| ~ spl39_26 ),
inference(avatar_split_clause,[],[f1655,f1316,f1264,f776,f772,f1661,f1657]) ).
fof(f1677,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))
| ~ spl39_70 ),
inference(resolution,[],[f1658,f601]) ).
fof(f1678,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))
| spl39_9
| ~ spl39_70 ),
inference(forward_subsumption_resolution,[],[f1677,f773]) ).
fof(f1679,plain,
( k5_lattices(k11_conlat_1(sK3)) = k15_lattice3(k11_conlat_1(sK3),k1_xboole_0)
| ~ l3_lattices(k11_conlat_1(sK3))
| spl39_9
| ~ spl39_26
| ~ spl39_70 ),
inference(forward_subsumption_resolution,[],[f1678,f1318]) ).
fof(f1680,plain,
( k5_lattices(k11_conlat_1(sK3)) = k15_lattice3(k11_conlat_1(sK3),k1_xboole_0)
| spl39_9
| ~ spl39_22
| ~ spl39_26
| ~ spl39_70 ),
inference(forward_subsumption_resolution,[],[f1679,f1265]) ).
fof(f1681,plain,
( k6_conlat_1(sK3) = k15_lattice3(k11_conlat_1(sK3),k1_xboole_0)
| spl39_9
| ~ spl39_22
| ~ spl39_26
| ~ spl39_70 ),
inference(forward_demodulation,[],[f1680,f787]) ).
fof(f1726,plain,
( v3_conlat_1(sK3)
| k5_conlat_1(sK3) = k1_conlat_2(sK3,k5_conlat_1(sK3)) ),
inference(resolution,[],[f1236,f350]) ).
fof(f1728,plain,
k5_conlat_1(sK3) = k1_conlat_2(sK3,k5_conlat_1(sK3)),
inference(forward_subsumption_resolution,[],[f1726,f351]) ).
fof(f1766,plain,
( m1_subset_1(k5_conlat_1(sK3),u1_struct_0(k11_conlat_1(sK3)))
| v3_conlat_1(sK3)
| ~ l2_conlat_1(sK3)
| ~ v6_conlat_1(k5_conlat_1(sK3),sK3)
| v7_conlat_1(k5_conlat_1(sK3),sK3)
| ~ v9_conlat_1(k5_conlat_1(sK3),sK3)
| ~ l3_conlat_1(k5_conlat_1(sK3),sK3) ),
inference(superposition,[],[f401,f1728]) ).
fof(f1870,plain,
( v3_conlat_1(sK3)
| k2_conlat_2(sK3,k1_xboole_0) = k16_lattice3(k11_conlat_1(sK3),k1_xboole_0) ),
inference(resolution,[],[f1170,f350]) ).
fof(f1872,plain,
k2_conlat_2(sK3,k1_xboole_0) = k16_lattice3(k11_conlat_1(sK3),k1_xboole_0),
inference(forward_subsumption_resolution,[],[f1870,f351]) ).
fof(f1874,plain,
( v3_conlat_1(sK3)
| k3_conlat_2(sK3,k1_xboole_0) = k15_lattice3(k11_conlat_1(sK3),k1_xboole_0) ),
inference(resolution,[],[f1182,f350]) ).
fof(f1876,plain,
k3_conlat_2(sK3,k1_xboole_0) = k15_lattice3(k11_conlat_1(sK3),k1_xboole_0),
inference(forward_subsumption_resolution,[],[f1874,f351]) ).
fof(f1877,plain,
( k6_conlat_1(sK3) = k3_conlat_2(sK3,k1_xboole_0)
| spl39_9
| ~ spl39_22
| ~ spl39_26
| ~ spl39_70 ),
inference(forward_demodulation,[],[f1876,f1681]) ).
fof(f1878,plain,
( $false
| spl39_2
| spl39_9
| ~ spl39_22
| ~ spl39_26
| ~ spl39_70 ),
inference(forward_subsumption_resolution,[],[f1877,f752]) ).
fof(f1879,plain,
( spl39_2
| spl39_9
| ~ spl39_22
| ~ spl39_26
| ~ spl39_70 ),
inference(avatar_contradiction_clause,[],[f1878]) ).
fof(f1880,plain,
( ~ sP2(sK3)
| spl39_70 ),
inference(resolution,[],[f1659,f485]) ).
fof(f1890,plain,
( v3_conlat_1(sK3)
| ~ l2_conlat_1(sK3)
| spl39_70 ),
inference(resolution,[],[f1880,f495]) ).
fof(f1891,plain,
( ~ l2_conlat_1(sK3)
| spl39_70 ),
inference(forward_subsumption_resolution,[],[f1890,f351]) ).
fof(f1892,plain,
( $false
| spl39_70 ),
inference(forward_subsumption_resolution,[],[f1891,f350]) ).
fof(f1893,plain,
spl39_70,
inference(avatar_contradiction_clause,[],[f1892]) ).
fof(f1902,plain,
( ~ sP2(sK3)
| spl39_26 ),
inference(resolution,[],[f1317,f486]) ).
fof(f1936,plain,
( v3_conlat_1(sK3)
| ~ l2_conlat_1(sK3)
| spl39_26 ),
inference(resolution,[],[f1902,f495]) ).
fof(f1937,plain,
( ~ l2_conlat_1(sK3)
| spl39_26 ),
inference(forward_subsumption_resolution,[],[f1936,f351]) ).
fof(f1938,plain,
( $false
| spl39_26 ),
inference(forward_subsumption_resolution,[],[f1937,f350]) ).
fof(f1939,plain,
spl39_26,
inference(avatar_contradiction_clause,[],[f1938]) ).
fof(f1966,plain,
( v3_conlat_1(sK3)
| ~ l2_conlat_1(sK3)
| spl39_22 ),
inference(resolution,[],[f1266,f392]) ).
fof(f1967,plain,
( ~ l2_conlat_1(sK3)
| spl39_22 ),
inference(forward_subsumption_resolution,[],[f1966,f351]) ).
fof(f1968,plain,
( $false
| spl39_22 ),
inference(forward_subsumption_resolution,[],[f1967,f350]) ).
fof(f1969,plain,
spl39_22,
inference(avatar_contradiction_clause,[],[f1968]) ).
fof(f1970,plain,
( k5_conlat_1(sK3) != k2_conlat_2(sK3,k1_xboole_0)
| spl39_1 ),
inference(forward_demodulation,[],[f616,f750]) ).
fof(f2302,plain,
( ! [X0] :
( ~ m1_subset_1(k5_conlat_1(sK3),u1_struct_0(k11_conlat_1(sK3)))
| v3_struct_0(k11_conlat_1(sK3))
| ~ l3_lattices(k11_conlat_1(sK3))
| ~ v1_xboole_0(X0)
| k5_conlat_1(sK3) = k16_lattice3(k11_conlat_1(sK3),X0) )
| ~ spl39_71 ),
inference(resolution,[],[f1153,f1662]) ).
fof(f2303,plain,
( ! [X0] :
( v3_struct_0(k11_conlat_1(sK3))
| ~ l3_lattices(k11_conlat_1(sK3))
| ~ v1_xboole_0(X0)
| k5_conlat_1(sK3) = k16_lattice3(k11_conlat_1(sK3),X0) )
| ~ spl39_10
| ~ spl39_71 ),
inference(forward_subsumption_resolution,[],[f2302,f778]) ).
fof(f2304,plain,
( ! [X0] :
( ~ l3_lattices(k11_conlat_1(sK3))
| ~ v1_xboole_0(X0)
| k5_conlat_1(sK3) = k16_lattice3(k11_conlat_1(sK3),X0) )
| spl39_9
| ~ spl39_10
| ~ spl39_71 ),
inference(forward_subsumption_resolution,[],[f2303,f773]) ).
fof(f2305,plain,
( ! [X0] :
( ~ v1_xboole_0(X0)
| k5_conlat_1(sK3) = k16_lattice3(k11_conlat_1(sK3),X0) )
| spl39_9
| ~ spl39_10
| ~ spl39_22
| ~ spl39_71 ),
inference(forward_subsumption_resolution,[],[f2304,f1265]) ).
fof(f2359,plain,
( k5_conlat_1(sK3) = k16_lattice3(k11_conlat_1(sK3),k1_xboole_0)
| spl39_9
| ~ spl39_10
| ~ spl39_22
| ~ spl39_71 ),
inference(resolution,[],[f2305,f461]) ).
fof(f2367,plain,
( k5_conlat_1(sK3) = k2_conlat_2(sK3,k1_xboole_0)
| spl39_9
| ~ spl39_10
| ~ spl39_22
| ~ spl39_71 ),
inference(superposition,[],[f2359,f1872]) ).
fof(f2375,plain,
( $false
| spl39_1
| spl39_9
| ~ spl39_10
| ~ spl39_22
| ~ spl39_71 ),
inference(forward_subsumption_resolution,[],[f2367,f1970]) ).
fof(f2376,plain,
( spl39_1
| spl39_9
| ~ spl39_10
| ~ spl39_22
| ~ spl39_71 ),
inference(avatar_contradiction_clause,[],[f2375]) ).
fof(f2387,plain,
( m1_subset_1(k5_conlat_1(sK3),u1_struct_0(k11_conlat_1(sK3)))
| v3_conlat_1(sK3)
| ~ l2_conlat_1(sK3)
| v7_conlat_1(k5_conlat_1(sK3),sK3)
| ~ v9_conlat_1(k5_conlat_1(sK3),sK3)
| ~ l3_conlat_1(k5_conlat_1(sK3),sK3) ),
inference(forward_subsumption_resolution,[],[f1766,f412]) ).
fof(f2394,plain,
( m1_subset_1(k5_conlat_1(sK3),u1_struct_0(k11_conlat_1(sK3)))
| v3_conlat_1(sK3)
| ~ l2_conlat_1(sK3)
| ~ v9_conlat_1(k5_conlat_1(sK3),sK3)
| ~ l3_conlat_1(k5_conlat_1(sK3),sK3) ),
inference(forward_subsumption_resolution,[],[f2387,f411]) ).
fof(f2400,plain,
( m1_subset_1(k5_conlat_1(sK3),u1_struct_0(k11_conlat_1(sK3)))
| v3_conlat_1(sK3)
| ~ l2_conlat_1(sK3)
| ~ l3_conlat_1(k5_conlat_1(sK3),sK3) ),
inference(forward_subsumption_resolution,[],[f2394,f410]) ).
fof(f2402,plain,
( m1_subset_1(k5_conlat_1(sK3),u1_struct_0(k11_conlat_1(sK3)))
| v3_conlat_1(sK3)
| ~ l2_conlat_1(sK3) ),
inference(forward_subsumption_resolution,[],[f2400,f409]) ).
fof(f2404,plain,
( m1_subset_1(k5_conlat_1(sK3),u1_struct_0(k11_conlat_1(sK3)))
| ~ l2_conlat_1(sK3) ),
inference(forward_subsumption_resolution,[],[f2402,f351]) ).
fof(f2406,plain,
m1_subset_1(k5_conlat_1(sK3),u1_struct_0(k11_conlat_1(sK3))),
inference(forward_subsumption_resolution,[],[f2404,f350]) ).
fof(f2408,plain,
spl39_10,
inference(avatar_split_clause,[],[f2406,f776]) ).
cnf(s1,plain,
( ~ spl39_1
| ~ spl39_2 ),
inference(sat_conversion,[],[f621]) ).
cnf(s11,plain,
~ spl39_9,
inference(sat_conversion,[],[f808]) ).
cnf(s33,plain,
( spl39_9
| ~ spl39_10
| ~ spl39_22
| ~ spl39_26
| ~ spl39_70
| spl39_71 ),
inference(sat_conversion,[],[f1663]) ).
cnf(s38,plain,
( spl39_2
| spl39_9
| ~ spl39_22
| ~ spl39_26
| ~ spl39_70 ),
inference(sat_conversion,[],[f1879]) ).
cnf(s39,plain,
spl39_70,
inference(sat_conversion,[],[f1893]) ).
cnf(s40,plain,
spl39_26,
inference(sat_conversion,[],[f1939]) ).
cnf(s47,plain,
spl39_22,
inference(sat_conversion,[],[f1969]) ).
cnf(s64,plain,
( spl39_1
| spl39_9
| ~ spl39_10
| ~ spl39_22
| ~ spl39_71 ),
inference(sat_conversion,[],[f2376]) ).
cnf(s72,plain,
spl39_10,
inference(sat_conversion,[],[f2408]) ).
cnf(s73,plain,
( spl39_1
| spl39_9
| ~ spl39_22
| ~ spl39_71 ),
inference(rat,[],[s64,s72]) ).
cnf(s93,plain,
( spl39_2
| spl39_9 ),
inference(rat,[],[s38,s39,s40,s47]) ).
cnf(s98,plain,
( spl39_9
| spl39_71 ),
inference(rat,[],[s33,s39,s40,s47,s72]) ).
cnf(s109,plain,
spl39_2,
inference(rat,[],[s93,s11]) ).
cnf(s110,plain,
spl39_71,
inference(rat,[],[s98,s11]) ).
cnf(s111,plain,
spl39_1,
inference(rat,[],[s73,s11,s47,s110]) ).
cnf(s113,plain,
$false,
inference(rat,[],[s1,s109,s111]) ).
fof(f2409,plain,
$false,
inference(avatar_sat_refutation,[],[s113]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT339+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.37 % Computer : n002.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sun Sep 27 14:50:21 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.40 Running first-order model finding
% 0.10/0.41 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 15.43/2.68 % (3594827)Will run a generic schedule for satisfiability detection.
% 15.43/2.68 % (3594835)dis+10_1_sil=32000:sp=arity:random_seed=2312468145:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 15.43/2.68 % (3594833)% WARNING: option uhcvi not known.
% 15.43/2.68 % (3594832)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3010755672_2999 on theBenchmark for (2999ds/0Mi)
% 15.43/2.68 % (3594833)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3604298735:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 15.43/2.68 % (3594834)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3684514424:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 15.43/2.68 % (3594836)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1955959835:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 15.43/2.68 % (3594838)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2409913108:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 15.43/2.68 % (3594837)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3283276622:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 15.43/2.68 % TRYING [1]
% 15.43/2.68 % TRYING [2]
% 15.43/2.68 % TRYING [3]
% 15.43/2.68 % (3594835)Instruction limit reached!
% 15.43/2.68 % (3594835)------------------------------
% 15.43/2.68 % (3594835)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.43/2.68 % (3594835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.43/2.68 % (3594835)CaDiCaL version: 2.1.3
% 15.43/2.68 % (3594835)Termination reason: Instruction limit
% 15.43/2.68 % (3594835)Termination phase: Saturation
% 15.43/2.68 % (3594835)Time elapsed: 0.040 s
% 15.43/2.68 % (3594835)Peak memory usage: 13 MB
% 15.43/2.68 % (3594835)Instructions burned: 106 (million)
% 15.43/2.68 % TRYING [4]
% 15.43/2.68 % (3594846)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2890600318:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 15.43/2.68 % TRYING [1]
% 15.43/2.68 % TRYING [2]
% 15.43/2.68 % (3594836)Instruction limit reached!
% 15.43/2.68 % (3594836)------------------------------
% 15.43/2.68 % (3594836)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.43/2.68 % (3594836)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.43/2.68 % (3594836)CaDiCaL version: 2.1.3
% 15.43/2.68 % (3594836)Termination reason: Instruction limit
% 15.43/2.68 % (3594836)Termination phase: Saturation
% 15.43/2.68 % (3594836)Time elapsed: 0.072 s
% 15.43/2.68 % (3594836)Peak memory usage: 13 MB
% 15.43/2.68 % (3594836)Instructions burned: 116 (million)
% 15.43/2.68 % TRYING [3]
% 15.43/2.68 % (3594837)Instruction limit reached!
% 15.43/2.68 % (3594837)------------------------------
% 15.43/2.68 % (3594837)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.43/2.68 % (3594837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.43/2.68 % (3594837)CaDiCaL version: 2.1.3
% 15.43/2.68 % (3594837)Termination reason: Instruction limit
% 15.43/2.68 % (3594837)Termination phase: Saturation
% 15.43/2.68 % (3594837)Time elapsed: 0.078 s
% 15.43/2.68 % (3594837)Peak memory usage: 13 MB
% 15.43/2.68 % (3594837)Instructions burned: 133 (million)
% 15.43/2.68 % (3594848)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3262351500:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 15.43/2.68 % (3594838)Instruction limit reached!
% 15.43/2.68 % (3594838)------------------------------
% 15.43/2.68 % (3594838)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.43/2.68 % (3594838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.43/2.68 % (3594838)CaDiCaL version: 2.1.3
% 15.43/2.68 % (3594838)Termination reason: Instruction limit
% 15.43/2.68 % (3594838)Termination phase: Saturation
% 15.43/2.68 % (3594838)Time elapsed: 0.085 s
% 15.43/2.68 % (3594838)Peak memory usage: 13 MB
% 15.43/2.68 % (3594838)Instructions burned: 159 (million)
% 15.43/2.68 % TRYING [5]
% 15.43/2.68 % (3594849)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=550312786:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 15.43/2.68 % TRYING [4]
% 15.43/2.68 % (3594851)ott-21_1_sil=16000:fs=off:random_seed=882896097:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 15.43/2.68 % (3594848)Instruction limit reached!
% 15.43/2.68 % (3594848)------------------------------
% 15.43/2.68 % (3594848)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.38/5.30 % (3594848)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.38/5.30 % (3594848)CaDiCaL version: 2.1.3
% 34.38/5.30 % (3594848)Termination reason: Instruction limit
% 34.38/5.30 % (3594848)Termination phase: Saturation
% 34.38/5.30 % (3594848)Time elapsed: 0.044 s
% 34.38/5.30 % (3594848)Peak memory usage: 14 MB
% 34.38/5.30 % (3594848)Instructions burned: 133 (million)
% 34.38/5.30 % (3594854)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=770357378:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 34.38/5.30 % (3594851)Instruction limit reached!
% 34.38/5.30 % (3594851)------------------------------
% 34.38/5.30 % (3594851)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.38/5.30 % (3594851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.38/5.30 % (3594851)CaDiCaL version: 2.1.3
% 34.38/5.30 % (3594851)Termination reason: Instruction limit
% 34.38/5.30 % (3594851)Termination phase: Saturation
% 34.38/5.30 % (3594851)Time elapsed: 0.097 s
% 34.38/5.30 % (3594851)Peak memory usage: 13 MB
% 34.38/5.30 % (3594851)Instructions burned: 182 (million)
% 34.38/5.30 % TRYING [6]
% 34.38/5.30 % (3594856)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1909908648:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 34.38/5.30 % TRYING [1]
% 34.38/5.30 % TRYING [2]
% 34.38/5.30 % TRYING [3]
% 34.38/5.30 % TRYING [5]
% 34.38/5.30 % (3594854)Instruction limit reached!
% 34.38/5.30 % (3594854)------------------------------
% 34.38/5.30 % (3594854)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.38/5.30 % (3594854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.38/5.30 % (3594854)CaDiCaL version: 2.1.3
% 34.38/5.30 % (3594854)Termination reason: Instruction limit
% 34.38/5.30 % (3594854)Termination phase: Saturation
% 34.38/5.30 % (3594854)Time elapsed: 0.171 s
% 34.38/5.30 % (3594854)Peak memory usage: 16 MB
% 34.38/5.30 % (3594854)Instructions burned: 479 (million)
% 34.38/5.30 % (3594846)Instruction limit reached!
% 34.38/5.30 % (3594846)------------------------------
% 34.38/5.30 % (3594846)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.38/5.30 % (3594846)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.38/5.30 % (3594846)CaDiCaL version: 2.1.3
% 34.38/5.30 % (3594846)Termination reason: Instruction limit
% 34.38/5.30 % (3594846)Termination phase: Finite model building constraint generation
% 34.38/5.30 % (3594846)Time elapsed: 0.261 s
% 34.38/5.30 % (3594846)Peak memory usage: 31 MB
% 34.38/5.30 % (3594846)Instructions burned: 717 (million)
% 34.38/5.30 % TRYING [4]
% 34.38/5.30 % (3594858)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1807435300:i=1179_2996 on theBenchmark for (2996ds/1179Mi)
% 34.38/5.30 % (3594859)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3209477096:i=889:ins=1_2996 on theBenchmark for (2996ds/889Mi)
% 34.38/5.30 % TRYING [7]
% 34.38/5.30 % TRYING [5]
% 34.38/5.30 % (3594849)Instruction limit reached!
% 34.38/5.30 % (3594849)------------------------------
% 34.38/5.30 % (3594849)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.38/5.30 % (3594849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.38/5.30 % (3594849)CaDiCaL version: 2.1.3
% 34.38/5.30 % (3594849)Termination reason: Instruction limit
% 34.38/5.30 % (3594849)Termination phase: Saturation
% 34.38/5.30 % (3594849)Time elapsed: 0.411 s
% 34.38/5.30 % (3594849)Peak memory usage: 20 MB
% 34.38/5.30 % (3594849)Instructions burned: 684 (million)
% 34.38/5.30 % TRYING [14]
% 34.38/5.30 % (3594862)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=2119446954:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 34.38/5.30 % (3594856)Instruction limit reached!
% 34.38/5.30 % (3594856)------------------------------
% 34.38/5.30 % (3594856)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.38/5.30 % (3594856)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.38/5.30 % (3594856)CaDiCaL version: 2.1.3
% 34.38/5.30 % (3594856)Termination reason: Instruction limit
% 34.38/5.30 % (3594856)Termination phase: Finite model building constraint generation
% 34.38/5.30 % (3594856)Time elapsed: 0.333 s
% 34.38/5.30 % (3594856)Peak memory usage: 24 MB
% 34.38/5.30 % (3594856)Instructions burned: 865 (million)
% 34.38/5.30 % (3594864)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1969339438:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 34.38/5.30 % (3594859)Instruction limit reached!
% 34.38/5.36 % (3594859)------------------------------
% 34.38/5.36 % (3594859)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.38/5.36 % (3594859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.38/5.36 % (3594859)CaDiCaL version: 2.1.3
% 34.38/5.36 % (3594859)Termination reason: Instruction limit
% 34.38/5.36 % (3594859)Termination phase: Finite model building constraint generation
% 34.38/5.36 % (3594859)Time elapsed: 0.337 s
% 34.38/5.36 % (3594859)Peak memory usage: 75 MB
% 34.38/5.36 % (3594859)Instructions burned: 893 (million)
% 34.38/5.36 % (3594858)Instruction limit reached!
% 34.38/5.36 % (3594858)------------------------------
% 34.38/5.36 % (3594858)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.38/5.36 % (3594858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.38/5.36 % (3594858)CaDiCaL version: 2.1.3
% 34.38/5.36 % (3594858)Termination reason: Instruction limit
% 34.38/5.36 % (3594858)Termination phase: Saturation
% 34.38/5.36 % (3594858)Time elapsed: 0.371 s
% 34.38/5.36 % (3594858)Peak memory usage: 26 MB
% 34.38/5.36 % (3594858)Instructions burned: 1182 (million)
% 34.38/5.36 % (3594866)fmb+10_1_sil=64000:random_seed=3331151997:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi)
% 34.38/5.36 % (3594867)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3019143774:i=9515:nm=5_2992 on theBenchmark for (2992ds/9515Mi)
% 34.38/5.36 % TRYING [20]
% 34.38/5.36 % TRYING [1]
% 34.38/5.36 % TRYING [2]
% 34.38/5.36 % TRYING [3]
% 34.38/5.36 % TRYING [4]
% 34.38/5.36 % (3594862)Instruction limit reached!
% 34.38/5.36 % (3594862)------------------------------
% 34.38/5.36 % (3594862)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.38/5.36 % (3594862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.38/5.36 % (3594862)CaDiCaL version: 2.1.3
% 34.38/5.36 % (3594862)Termination reason: Instruction limit
% 34.38/5.36 % (3594862)Termination phase: Saturation
% 34.38/5.36 % (3594862)Time elapsed: 0.362 s
% 34.38/5.36 % (3594862)Peak memory usage: 17 MB
% 34.38/5.36 % (3594862)Instructions burned: 692 (million)
% 34.38/5.36 % (3594870)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=843224836:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 34.38/5.36 % TRYING [8]
% 34.38/5.36 % (3594864)Instruction limit reached!
% 34.38/5.36 % (3594864)------------------------------
% 34.38/5.36 % (3594864)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.38/5.36 % (3594864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.38/5.36 % (3594864)CaDiCaL version: 2.1.3
% 34.38/5.36 % (3594864)Termination reason: Instruction limit
% 34.38/5.36 % (3594864)Termination phase: Saturation
% 34.38/5.36 % (3594864)Time elapsed: 0.475 s
% 34.38/5.36 % (3594864)Peak memory usage: 20 MB
% 34.38/5.36 % (3594864)Instructions burned: 879 (million)
% 34.38/5.36 % (3594872)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2581619696:i=5131_2989 on theBenchmark for (2989ds/5131Mi)
% 34.38/5.36 % (3594870)Instruction limit reached!
% 34.38/5.36 % (3594870)------------------------------
% 34.38/5.36 % (3594870)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.38/5.36 % (3594870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.38/5.36 % (3594870)CaDiCaL version: 2.1.3
% 34.38/5.36 % (3594870)Termination reason: Instruction limit
% 34.38/5.36 % (3594870)Termination phase: Finite model building constraint generation
% 34.38/5.36 % (3594870)Time elapsed: 0.355 s
% 34.38/5.36 % (3594870)Peak memory usage: 70 MB
% 34.38/5.36 % (3594870)Instructions burned: 922 (million)
% 34.38/5.36 % TRYING [8]
% 34.38/5.36 % TRYING [5]
% 34.38/5.36 % (3594874)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=80227160:i=1472:ins=7:fdi=8:gsp=on_2986 on theBenchmark for (2986ds/1472Mi)
% 34.38/5.36 % (3594874)Instruction limit reached!
% 34.38/5.36 % (3594874)------------------------------
% 34.38/5.36 % (3594874)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.38/5.36 % (3594874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.38/5.36 % (3594874)CaDiCaL version: 2.1.3
% 34.38/5.36 % (3594874)Termination reason: Instruction limit
% 34.38/5.36 % (3594874)Termination phase: Saturation
% 34.38/5.36 % (3594874)Time elapsed: 0.907 s
% 34.38/5.36 % (3594874)Peak memory usage: 31 MB
% 34.38/5.36 % (3594874)Instructions burned: 1472 (million)
% 34.38/5.36 % (3594876)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2293062133:i=6324_2977 on theBenchmark for (2977ds/6324Mi)
% 34.38/5.36 % TRYING [77]
% 34.38/5.36 % (3594867)Instruction limit reached!
% 34.38/5.36 % (3594867)------------------------------
% 34.38/5.36 % (3594867)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.38/5.36 % (3594867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.38/5.36 % (3594867)CaDiCaL version: 2.1.3
% 34.38/5.36 % (3594867)Termination reason: Instruction limit
% 34.38/5.36 % (3594867)Termination phase: Finite model building constraint generation
% 34.38/5.36 % (3594867)Time elapsed: 1.814 s
% 34.38/5.36 % (3594867)Peak memory usage: 564 MB
% 34.38/5.36 % (3594867)Instructions burned: 9518 (million)
% 34.38/5.36 % (3594878)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1452634332:fmbsr=2.30978:i=2174_2974 on theBenchmark for (2974ds/2174Mi)
% 34.38/5.36 % TRYING [16]
% 34.38/5.36 % (3594878)Instruction limit reached!
% 34.38/5.36 % (3594878)------------------------------
% 34.38/5.36 % (3594878)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.38/5.36 % (3594878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.38/5.36 % (3594878)CaDiCaL version: 2.1.3
% 34.38/5.36 % (3594878)Termination reason: Instruction limit
% 34.38/5.36 % (3594878)Termination phase: Finite model building constraint generation
% 34.38/5.36 % (3594878)Time elapsed: 0.419 s
% 34.38/5.36 % (3594878)Peak memory usage: 134 MB
% 34.38/5.36 % (3594878)Instructions burned: 2179 (million)
% 34.38/5.36 % (3594880)ott-2_1_sil=16000:newcnf=on:random_seed=1413680895:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2969 on theBenchmark for (2969ds/869Mi)
% 34.38/5.36 % (3594880)Instruction limit reached!
% 34.38/5.36 % (3594880)------------------------------
% 34.38/5.36 % (3594880)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.38/5.36 % (3594880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.38/5.36 % (3594880)CaDiCaL version: 2.1.3
% 34.38/5.36 % (3594880)Termination reason: Instruction limit
% 34.38/5.36 % (3594880)Termination phase: Saturation
% 34.38/5.36 % (3594880)Time elapsed: 0.269 s
% 34.38/5.36 % (3594880)Peak memory usage: 17 MB
% 34.38/5.36 % (3594880)Instructions burned: 873 (million)
% 34.38/5.36 % (3594882)ott+10_1_sil=32000:tgt=ground:random_seed=223929764:i=5114:av=off_2966 on theBenchmark for (2966ds/5114Mi)
% 34.38/5.36 % (3594872)Instruction limit reached!
% 34.38/5.36 % (3594872)------------------------------
% 34.38/5.36 % (3594872)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.38/5.36 % (3594872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.38/5.36 % (3594872)CaDiCaL version: 2.1.3
% 34.38/5.36 % (3594872)Termination reason: Instruction limit
% 34.38/5.36 % (3594872)Termination phase: Saturation
% 34.38/5.36 % (3594872)Time elapsed: 2.862 s
% 34.38/5.36 % (3594872)Peak memory usage: 35 MB
% 34.38/5.36 % (3594872)Instructions burned: 5132 (million)
% 34.38/5.36 % (3594884)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3682760055:i=54282_2960 on theBenchmark for (2960ds/54282Mi)
% 34.38/5.36 % TRYING [1]
% 34.38/5.36 % TRYING [2]
% 34.38/5.36 % TRYING [3]
% 34.38/5.36 % TRYING [4]
% 34.38/5.36 % TRYING [5]
% 34.38/5.36 % TRYING [6]
% 34.38/5.36 % TRYING [7]
% 34.38/5.36 % (3594876)Instruction limit reached!
% 34.38/5.36 % (3594876)------------------------------
% 34.38/5.36 % (3594876)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.38/5.36 % (3594876)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.38/5.36 % (3594876)CaDiCaL version: 2.1.3
% 34.38/5.36 % (3594876)Termination reason: Instruction limit
% 34.38/5.36 % (3594876)Termination phase: Finite model building constraint generation
% 34.38/5.36 % (3594876)Time elapsed: 2.337 s
% 34.38/5.36 % (3594876)Peak memory usage: 524 MB
% 34.38/5.36 % (3594876)Instructions burned: 6324 (million)
% 34.38/5.36 % TRYING [6]
% 34.38/5.36 % (3594886)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3185042922:i=3512:aac=none_2953 on theBenchmark for (2953ds/3512Mi)
% 34.38/5.36 % (3594882)Instruction limit reached!
% 34.38/5.36 % (3594882)------------------------------
% 34.38/5.36 % (3594882)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.38/5.36 % (3594882)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.38/5.36 % (3594882)CaDiCaL version: 2.1.3
% 34.38/5.36 % (3594882)Termination reason: Instruction limit
% 34.38/5.36 % (3594882)Termination phase: Saturation
% 34.38/5.36 % (3594882)Time elapsed: 1.544 s
% 34.38/5.36 % (3594882)Peak memory usage: 47 MB
% 34.38/5.36 % (3594882)Instructions burned: 5114 (million)
% 34.38/5.36 % (3594888)dis+21_1_sil=32000:sas=cadical:random_seed=4175316737:i=3773:amm=off_2951 on theBenchmark for (2951ds/3773Mi)
% 34.38/5.36 % (3594888) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3594827-3594888"...
% 34.38/5.36 % (3594888)...printing done.
% 34.38/5.36 % (3594888)Refutation found. Thanks to Tanya!
% 34.38/5.36 % SZS status Theorem for theBenchmark
% 34.38/5.36 % SZS output start Proof for theBenchmark
% See solution above
% 34.38/5.36 % (3594888)------------------------------
% 34.38/5.36 % (3594888)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.38/5.36 % (3594888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.38/5.36 % (3594888)CaDiCaL version: 2.1.3
% 34.38/5.36 % (3594888)Termination reason: Refutation
% 34.38/5.36 % (3594888)Time elapsed: 0.031 s
% 34.38/5.36 % (3594888)Peak memory usage: 13 MB
% 34.38/5.36 % (3594888)Instructions burned: 88 (million)
% 34.38/5.36 % (3594827)Success in time 4.944 s
% 34.38/5.36 % Vampire exiting
%------------------------------------------------------------------------------