%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT340+2 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n011.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:47:06 AM UTC 2026
% Result : Theorem 11.21s 4.32s
% Output : Refutation 23.66s
% Verified :
% SZS Type : Refutation
% Derivation depth : 37
% Number of leaves : 55
% Syntax : Number of formulae : 397 ( 47 unt; 16 def)
% Number of atoms : 1852 ( 152 equ)
% Maximal formula atoms : 15 ( 4 avg)
% Number of connectives : 2463 (1008 ~;1198 |; 186 &)
% ( 23 <=>; 48 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 6 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 44 ( 42 usr; 16 prp; 0-3 aty)
% Number of functors : 20 ( 20 usr; 1 con; 0-3 aty)
% Number of variables : 438 ( 2 sgn 436 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f18,axiom,
! [X0,X1] : r1_tarski(X0,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',reflexivity_r1_tarski) ).
fof(f58,axiom,
! [X0,X1] : k3_xboole_0(X0,X0) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',idempotence_k3_xboole_0) ).
fof(f144,axiom,
! [X0] : k2_tarski(X0,X0) = k1_tarski(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t69_enumset1) ).
fof(f366,axiom,
! [X0,X1] :
( ( ~ v1_xboole_0(X0)
=> ( m1_subset_1(X1,X0)
<=> r2_hidden(X1,X0) ) )
& ( v1_xboole_0(X0)
=> ( m1_subset_1(X1,X0)
<=> v1_xboole_0(X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d2_subset_1) ).
fof(f368,axiom,
! [X0] : k2_subset_1(X0) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d4_subset_1) ).
fof(f450,axiom,
! [X0] : m1_subset_1(k2_subset_1(X0),k1_zfmisc_1(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k2_subset_1) ).
fof(f460,axiom,
! [X0,X1,X2] :
( ( m1_subset_1(X1,k1_zfmisc_1(X0))
& m1_subset_1(X2,k1_zfmisc_1(X0)) )
=> k5_subset_1(X0,X1,X2) = k3_xboole_0(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k5_subset_1) ).
fof(f488,axiom,
! [X0,X1] : k1_setfam_1(k2_tarski(X0,X1)) = k3_xboole_0(X0,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t12_setfam_1) ).
fof(f561,axiom,
! [X0,X1] :
( r2_hidden(X0,X1)
=> m1_subset_1(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t1_subset) ).
fof(f563,axiom,
! [X0,X1] :
( m1_subset_1(X0,k1_zfmisc_1(X1))
<=> r1_tarski(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t3_subset) ).
fof(f3570,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_struct_0(X0) )
=> ~ v1_xboole_0(u1_struct_0(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_struct_0) ).
fof(f3582,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& l1_struct_0(X0)
& m1_subset_1(X1,u1_struct_0(X0)) )
=> m1_subset_1(k1_struct_0(X0,X1),k1_zfmisc_1(u1_struct_0(X0))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k1_struct_0) ).
fof(f3583,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& l1_struct_0(X0)
& m1_subset_1(X1,u1_struct_0(X0)) )
=> k1_struct_0(X0,X1) = k1_tarski(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k1_struct_0) ).
fof(f3602,axiom,
! [X0] :
( l3_lattices(X0)
=> ( ( ~ v3_struct_0(X0)
& v10_lattices(X0) )
=> ( ~ v3_struct_0(X0)
& v4_lattices(X0)
& v5_lattices(X0)
& v6_lattices(X0)
& v7_lattices(X0)
& v8_lattices(X0)
& v9_lattices(X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc1_lattices) ).
fof(f3661,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v4_lattices(X0)
& l2_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( m1_subset_1(X2,u1_struct_0(X0))
=> ( ( r1_lattices(X0,X1,X2)
& r1_lattices(X0,X2,X1) )
=> X1 = X2 ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t26_lattices) ).
fof(f3676,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v13_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> r3_lattices(X0,k5_lattices(X0),X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t41_lattices) ).
fof(f3692,axiom,
! [X0] :
( l2_lattices(X0)
=> l1_struct_0(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l2_lattices) ).
fof(f3694,axiom,
! [X0] :
( l3_lattices(X0)
=> ( l1_lattices(X0)
& l2_lattices(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l3_lattices) ).
fof(f3700,axiom,
! [X0,X1,X2] :
( ( ~ v3_struct_0(X0)
& v6_lattices(X0)
& v8_lattices(X0)
& v9_lattices(X0)
& l3_lattices(X0)
& m1_subset_1(X1,u1_struct_0(X0))
& m1_subset_1(X2,u1_struct_0(X0)) )
=> ( r3_lattices(X0,X1,X2)
<=> r1_lattices(X0,X1,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_r3_lattices) ).
fof(f3709,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_lattices(X0) )
=> m1_subset_1(k5_lattices(X0),u1_struct_0(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k5_lattices) ).
fof(f3710,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l2_lattices(X0) )
=> m1_subset_1(k6_lattices(X0),u1_struct_0(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k6_lattices) ).
fof(f3740,axiom,
! [X0] :
( l1_struct_0(X0)
=> k2_pre_topc(X0) = u1_struct_0(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d3_pre_topc) ).
fof(f3806,axiom,
! [X0] :
( l1_struct_0(X0)
=> m1_subset_1(k2_pre_topc(X0),k1_zfmisc_1(u1_struct_0(X0))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k2_pre_topc) ).
fof(f4042,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> m1_filter_0(u1_struct_0(X0),X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t15_filter_0) ).
fof(f4127,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_filter_0(X1,X0)
=> ( ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m1_filter_0) ).
fof(f4262,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_filter_0(X1,X0)
=> ! [X2] :
( m1_filter_0(X2,X0)
=> m1_filter_0(k5_subset_1(u1_struct_0(X0),X1,X2),X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t1_filter_1) ).
fof(f4423,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v4_lattice3(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ! [X2] :
( r2_hidden(X1,X2)
=> ( r3_lattices(X0,X1,k15_lattice3(X0,X2))
& r3_lattices(X0,k16_lattice3(X0,X2),X1) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t38_lattice3) ).
fof(f4428,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v4_lattice3(X0)
& l3_lattices(X0) )
=> ! [X1] :
( m1_subset_1(X1,u1_struct_0(X0))
=> ( k15_lattice3(X0,k1_struct_0(X0,X1)) = X1
& k16_lattice3(X0,k1_struct_0(X0,X1)) = X1 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t43_lattice3) ).
fof(f4430,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v4_lattice3(X0)
& l3_lattices(X0) )
=> ! [X1,X2] :
( r1_tarski(X1,X2)
=> ( r3_lattices(X0,k15_lattice3(X0,X1),k15_lattice3(X0,X2))
& r3_lattices(X0,k16_lattice3(X0,X2),k16_lattice3(X0,X1)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t46_lattice3) ).
fof(f4433,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v4_lattice3(X0)
& l3_lattices(X0) )
=> ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v14_lattices(X0)
& l3_lattices(X0)
& k6_lattices(X0) = k15_lattice3(X0,u1_struct_0(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t51_lattice3) ).
fof(f4457,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& l3_lattices(X0) )
=> m1_subset_1(k15_lattice3(X0,X1),u1_struct_0(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k15_lattice3) ).
fof(f4458,axiom,
! [X0,X1] :
( ( ~ v3_struct_0(X0)
& l3_lattices(X0) )
=> m1_subset_1(k16_lattice3(X0,X1),u1_struct_0(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k16_lattice3) ).
fof(f5331,axiom,
! [X0] :
( ( ~ v3_conlat_1(X0)
& l2_conlat_1(X0) )
=> ( ~ v3_struct_0(k11_conlat_1(X0))
& v10_lattices(k11_conlat_1(X0))
& l3_lattices(k11_conlat_1(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t46_conlat_1) ).
fof(f5334,axiom,
! [X0] :
( ( ~ v3_conlat_1(X0)
& l2_conlat_1(X0) )
=> ( ~ v3_struct_0(k11_conlat_1(X0))
& v10_lattices(k11_conlat_1(X0))
& v4_lattice3(k11_conlat_1(X0))
& l3_lattices(k11_conlat_1(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t48_conlat_1) ).
fof(f5466,axiom,
! [X0] :
( ( ~ v3_conlat_1(X0)
& l2_conlat_1(X0) )
=> ( ~ v3_struct_0(k11_conlat_1(X0))
& v3_lattices(k11_conlat_1(X0))
& v4_lattices(k11_conlat_1(X0))
& v5_lattices(k11_conlat_1(X0))
& v6_lattices(k11_conlat_1(X0))
& v7_lattices(k11_conlat_1(X0))
& v8_lattices(k11_conlat_1(X0))
& v9_lattices(k11_conlat_1(X0))
& v10_lattices(k11_conlat_1(X0))
& v13_lattices(k11_conlat_1(X0))
& v14_lattices(k11_conlat_1(X0))
& v15_lattices(k11_conlat_1(X0))
& v4_lattice3(k11_conlat_1(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_conlat_2) ).
fof(f5467,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(f5471,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(f5472,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(f5474,conjecture,
! [X0] :
( ( ~ v3_conlat_1(X0)
& l2_conlat_1(X0) )
=> ( k3_conlat_2(X0,k2_subset_1(u1_struct_0(k11_conlat_1(X0)))) = k5_conlat_1(X0)
& k2_conlat_2(X0,k2_subset_1(u1_struct_0(k11_conlat_1(X0)))) = k6_conlat_1(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t6_conlat_2) ).
fof(f5475,negated_conjecture,
~ ! [X0] :
( ( ~ v3_conlat_1(X0)
& l2_conlat_1(X0) )
=> ( k3_conlat_2(X0,k2_subset_1(u1_struct_0(k11_conlat_1(X0)))) = k5_conlat_1(X0)
& k2_conlat_2(X0,k2_subset_1(u1_struct_0(k11_conlat_1(X0)))) = k6_conlat_1(X0) ) ),
inference(negated_conjecture,[status(cth)],[f5474]) ).
fof(f5481,plain,
! [X0] : r1_tarski(X0,X0),
inference(rectify,[],[f18]) ).
fof(f5512,plain,
! [X0] : k3_xboole_0(X0,X0) = X0,
inference(rectify,[],[f58]) ).
fof(f5542,plain,
? [X0] :
( ( k5_conlat_1(X0) != k3_conlat_2(X0,k2_subset_1(u1_struct_0(k11_conlat_1(X0))))
| k6_conlat_1(X0) != k2_conlat_2(X0,k2_subset_1(u1_struct_0(k11_conlat_1(X0)))) )
& ~ v3_conlat_1(X0)
& l2_conlat_1(X0) ),
inference(ennf_transformation,[],[f5475]) ).
fof(f5543,plain,
? [X0] :
( ( k5_conlat_1(X0) != k3_conlat_2(X0,k2_subset_1(u1_struct_0(k11_conlat_1(X0))))
| k6_conlat_1(X0) != k2_conlat_2(X0,k2_subset_1(u1_struct_0(k11_conlat_1(X0)))) )
& ~ v3_conlat_1(X0)
& l2_conlat_1(X0) ),
inference(flattening,[],[f5542]) ).
fof(f5556,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,[],[f5467]) ).
fof(f5557,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,[],[f5556]) ).
fof(f5558,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,[],[f5466]) ).
fof(f5559,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,[],[f5558]) ).
fof(f5562,plain,
! [X0] :
( ( ~ v3_struct_0(k11_conlat_1(X0))
& v10_lattices(k11_conlat_1(X0))
& v4_lattice3(k11_conlat_1(X0))
& l3_lattices(k11_conlat_1(X0)) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(ennf_transformation,[],[f5334]) ).
fof(f5563,plain,
! [X0] :
( ( ~ v3_struct_0(k11_conlat_1(X0))
& v10_lattices(k11_conlat_1(X0))
& v4_lattice3(k11_conlat_1(X0))
& l3_lattices(k11_conlat_1(X0)) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(flattening,[],[f5562]) ).
fof(f5564,plain,
! [X0] :
( ( ~ v3_struct_0(k11_conlat_1(X0))
& v10_lattices(k11_conlat_1(X0))
& l3_lattices(k11_conlat_1(X0)) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(ennf_transformation,[],[f5331]) ).
fof(f5565,plain,
! [X0] :
( ( ~ v3_struct_0(k11_conlat_1(X0))
& v10_lattices(k11_conlat_1(X0))
& l3_lattices(k11_conlat_1(X0)) )
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(flattening,[],[f5564]) ).
fof(f5596,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,[],[f5471]) ).
fof(f5597,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,[],[f5596]) ).
fof(f5600,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,[],[f5472]) ).
fof(f5601,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,[],[f5600]) ).
fof(f5614,plain,
! [X0,X1] :
( m1_subset_1(X0,X1)
| ~ r2_hidden(X0,X1) ),
inference(ennf_transformation,[],[f561]) ).
fof(f5627,plain,
! [X0,X1] :
( ( ( m1_subset_1(X1,X0)
<=> r2_hidden(X1,X0) )
| v1_xboole_0(X0) )
& ( ( m1_subset_1(X1,X0)
<=> v1_xboole_0(X1) )
| ~ v1_xboole_0(X0) ) ),
inference(ennf_transformation,[],[f366]) ).
fof(f5885,plain,
! [X0,X1] :
( m1_subset_1(k15_lattice3(X0,X1),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f4457]) ).
fof(f5886,plain,
! [X0,X1] :
( m1_subset_1(k15_lattice3(X0,X1),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f5885]) ).
fof(f5887,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v14_lattices(X0)
& l3_lattices(X0)
& k6_lattices(X0) = k15_lattice3(X0,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v4_lattice3(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f4433]) ).
fof(f5888,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v10_lattices(X0)
& v14_lattices(X0)
& l3_lattices(X0)
& k6_lattices(X0) = k15_lattice3(X0,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v4_lattice3(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f5887]) ).
fof(f5893,plain,
! [X0] :
( ! [X1,X2] :
( ( r3_lattices(X0,k15_lattice3(X0,X1),k15_lattice3(X0,X2))
& r3_lattices(X0,k16_lattice3(X0,X2),k16_lattice3(X0,X1)) )
| ~ r1_tarski(X1,X2) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v4_lattice3(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f4430]) ).
fof(f5894,plain,
! [X0] :
( ! [X1,X2] :
( ( r3_lattices(X0,k15_lattice3(X0,X1),k15_lattice3(X0,X2))
& r3_lattices(X0,k16_lattice3(X0,X2),k16_lattice3(X0,X1)) )
| ~ r1_tarski(X1,X2) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v4_lattice3(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f5893]) ).
fof(f5897,plain,
! [X0] :
( ! [X1] :
( ( k15_lattice3(X0,k1_struct_0(X0,X1)) = X1
& k16_lattice3(X0,k1_struct_0(X0,X1)) = X1 )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v4_lattice3(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f4428]) ).
fof(f5898,plain,
! [X0] :
( ! [X1] :
( ( k15_lattice3(X0,k1_struct_0(X0,X1)) = X1
& k16_lattice3(X0,k1_struct_0(X0,X1)) = X1 )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v4_lattice3(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f5897]) ).
fof(f5901,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( r3_lattices(X0,X1,k15_lattice3(X0,X2))
& r3_lattices(X0,k16_lattice3(X0,X2),X1) )
| ~ r2_hidden(X1,X2) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v4_lattice3(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f4423]) ).
fof(f5902,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( r3_lattices(X0,X1,k15_lattice3(X0,X2))
& r3_lattices(X0,k16_lattice3(X0,X2),X1) )
| ~ r2_hidden(X1,X2) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v4_lattice3(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f5901]) ).
fof(f5905,plain,
! [X0,X1] :
( m1_subset_1(k16_lattice3(X0,X1),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f4458]) ).
fof(f5906,plain,
! [X0,X1] :
( m1_subset_1(k16_lattice3(X0,X1),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f5905]) ).
fof(f5931,plain,
! [X0] :
( m1_subset_1(k5_lattices(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_lattices(X0) ),
inference(ennf_transformation,[],[f3709]) ).
fof(f5932,plain,
! [X0] :
( m1_subset_1(k5_lattices(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_lattices(X0) ),
inference(flattening,[],[f5931]) ).
fof(f5937,plain,
! [X0] :
( ! [X1] :
( r3_lattices(X0,k5_lattices(X0),X1)
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v13_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f3676]) ).
fof(f5938,plain,
! [X0] :
( ! [X1] :
( r3_lattices(X0,k5_lattices(X0),X1)
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v13_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f5937]) ).
fof(f5959,plain,
! [X0] :
( m1_subset_1(k6_lattices(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l2_lattices(X0) ),
inference(ennf_transformation,[],[f3710]) ).
fof(f5960,plain,
! [X0] :
( m1_subset_1(k6_lattices(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l2_lattices(X0) ),
inference(flattening,[],[f5959]) ).
fof(f5994,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( X1 = X2
| ~ r1_lattices(X0,X1,X2)
| ~ r1_lattices(X0,X2,X1)
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v4_lattices(X0)
| ~ l2_lattices(X0) ),
inference(ennf_transformation,[],[f3661]) ).
fof(f5995,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( X1 = X2
| ~ r1_lattices(X0,X1,X2)
| ~ r1_lattices(X0,X2,X1)
| ~ m1_subset_1(X2,u1_struct_0(X0)) )
| ~ m1_subset_1(X1,u1_struct_0(X0)) )
| v3_struct_0(X0)
| ~ v4_lattices(X0)
| ~ l2_lattices(X0) ),
inference(flattening,[],[f5994]) ).
fof(f6002,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v4_lattices(X0)
& v5_lattices(X0)
& v6_lattices(X0)
& v7_lattices(X0)
& v8_lattices(X0)
& v9_lattices(X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f3602]) ).
fof(f6003,plain,
! [X0] :
( ( ~ v3_struct_0(X0)
& v4_lattices(X0)
& v5_lattices(X0)
& v6_lattices(X0)
& v7_lattices(X0)
& v8_lattices(X0)
& v9_lattices(X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f6002]) ).
fof(f6016,plain,
! [X0,X1,X2] :
( ( r3_lattices(X0,X1,X2)
<=> r1_lattices(X0,X1,X2) )
| v3_struct_0(X0)
| ~ v6_lattices(X0)
| ~ v8_lattices(X0)
| ~ v9_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f3700]) ).
fof(f6017,plain,
! [X0,X1,X2] :
( ( r3_lattices(X0,X1,X2)
<=> r1_lattices(X0,X1,X2) )
| v3_struct_0(X0)
| ~ v6_lattices(X0)
| ~ v8_lattices(X0)
| ~ v9_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(flattening,[],[f6016]) ).
fof(f6514,plain,
! [X0] :
( m1_subset_1(k2_pre_topc(X0),k1_zfmisc_1(u1_struct_0(X0)))
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f3806]) ).
fof(f6523,plain,
! [X0] :
( k2_pre_topc(X0) = u1_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f3740]) ).
fof(f6609,plain,
! [X0] :
( l1_struct_0(X0)
| ~ l2_lattices(X0) ),
inference(ennf_transformation,[],[f3692]) ).
fof(f6613,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(ennf_transformation,[],[f3570]) ).
fof(f6614,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(flattening,[],[f6613]) ).
fof(f6659,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( m1_filter_0(k5_subset_1(u1_struct_0(X0),X1,X2),X0)
| ~ m1_filter_0(X2,X0) )
| ~ m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f4262]) ).
fof(f6660,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( m1_filter_0(k5_subset_1(u1_struct_0(X0),X1,X2),X0)
| ~ m1_filter_0(X2,X0) )
| ~ m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f6659]) ).
fof(f6665,plain,
! [X0,X1,X2] :
( k5_subset_1(X0,X1,X2) = k3_xboole_0(X1,X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f460]) ).
fof(f6666,plain,
! [X0,X1,X2] :
( k5_subset_1(X0,X1,X2) = k3_xboole_0(X1,X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(flattening,[],[f6665]) ).
fof(f7141,plain,
! [X0,X1] :
( k1_struct_0(X0,X1) = k1_tarski(X1)
| v3_struct_0(X0)
| ~ l1_struct_0(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f3583]) ).
fof(f7142,plain,
! [X0,X1] :
( k1_struct_0(X0,X1) = k1_tarski(X1)
| v3_struct_0(X0)
| ~ l1_struct_0(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(flattening,[],[f7141]) ).
fof(f7143,plain,
! [X0,X1] :
( m1_subset_1(k1_struct_0(X0,X1),k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ l1_struct_0(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(ennf_transformation,[],[f3582]) ).
fof(f7144,plain,
! [X0,X1] :
( m1_subset_1(k1_struct_0(X0,X1),k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ l1_struct_0(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(flattening,[],[f7143]) ).
fof(f7306,plain,
! [X0] :
( ( l1_lattices(X0)
& l2_lattices(X0) )
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f3694]) ).
fof(f7378,plain,
! [X0] :
( ! [X1] :
( ( ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f4127]) ).
fof(f7379,plain,
! [X0] :
( ! [X1] :
( ( ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0))) )
| ~ m1_filter_0(X1,X0) )
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f7378]) ).
fof(f7380,plain,
! [X0] :
( m1_filter_0(u1_struct_0(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(ennf_transformation,[],[f4042]) ).
fof(f7381,plain,
! [X0] :
( m1_filter_0(u1_struct_0(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(flattening,[],[f7380]) ).
fof(f8071,definition,
! [X0] :
( ( ~ v3_struct_0(k11_conlat_1(X0))
& v3_lattices(k11_conlat_1(X0))
& v4_lattices(k11_conlat_1(X0))
& v5_lattices(k11_conlat_1(X0))
& v6_lattices(k11_conlat_1(X0))
& v7_lattices(k11_conlat_1(X0))
& v8_lattices(k11_conlat_1(X0))
& v9_lattices(k11_conlat_1(X0))
& v10_lattices(k11_conlat_1(X0))
& v13_lattices(k11_conlat_1(X0))
& v14_lattices(k11_conlat_1(X0))
& v15_lattices(k11_conlat_1(X0))
& v4_lattice3(k11_conlat_1(X0)) )
| ~ sP0(X0) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f8072,plain,
! [X0] :
( sP0(X0)
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(definition_folding,[],[f5559,f8071]) ).
fof(f8197,plain,
( ( k5_conlat_1(sK74) != k3_conlat_2(sK74,k2_subset_1(u1_struct_0(k11_conlat_1(sK74))))
| k6_conlat_1(sK74) != k2_conlat_2(sK74,k2_subset_1(u1_struct_0(k11_conlat_1(sK74)))) )
& ~ v3_conlat_1(sK74)
& l2_conlat_1(sK74) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK74]),skolemize(X0,sK74)],[f5543]) ).
fof(f8203,plain,
! [X0] :
( ( ~ v3_struct_0(k11_conlat_1(X0))
& v3_lattices(k11_conlat_1(X0))
& v4_lattices(k11_conlat_1(X0))
& v5_lattices(k11_conlat_1(X0))
& v6_lattices(k11_conlat_1(X0))
& v7_lattices(k11_conlat_1(X0))
& v8_lattices(k11_conlat_1(X0))
& v9_lattices(k11_conlat_1(X0))
& v10_lattices(k11_conlat_1(X0))
& v13_lattices(k11_conlat_1(X0))
& v14_lattices(k11_conlat_1(X0))
& v15_lattices(k11_conlat_1(X0))
& v4_lattice3(k11_conlat_1(X0)) )
| ~ sP0(X0) ),
inference(nnf_transformation,[],[f8071]) ).
fof(f8222,plain,
! [X0,X1] :
( ( ( ( m1_subset_1(X1,X0)
| ~ r2_hidden(X1,X0) )
& ( r2_hidden(X1,X0)
| ~ m1_subset_1(X1,X0) ) )
| v1_xboole_0(X0) )
& ( ( ( m1_subset_1(X1,X0)
| ~ v1_xboole_0(X1) )
& ( v1_xboole_0(X1)
| ~ m1_subset_1(X1,X0) ) )
| ~ v1_xboole_0(X0) ) ),
inference(nnf_transformation,[],[f5627]) ).
fof(f8248,plain,
! [X0,X1] :
( ( m1_subset_1(X0,k1_zfmisc_1(X1))
| ~ r1_tarski(X0,X1) )
& ( r1_tarski(X0,X1)
| ~ m1_subset_1(X0,k1_zfmisc_1(X1)) ) ),
inference(nnf_transformation,[],[f563]) ).
fof(f8369,plain,
! [X0,X1,X2] :
( ( ( r3_lattices(X0,X1,X2)
| ~ r1_lattices(X0,X1,X2) )
& ( r1_lattices(X0,X1,X2)
| ~ r3_lattices(X0,X1,X2) ) )
| v3_struct_0(X0)
| ~ v6_lattices(X0)
| ~ v8_lattices(X0)
| ~ v9_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(nnf_transformation,[],[f6017]) ).
fof(f9165,plain,
l2_conlat_1(sK74),
inference(cnf_transformation,[],[f8197]) ).
fof(f9166,plain,
~ v3_conlat_1(sK74),
inference(cnf_transformation,[],[f8197]) ).
fof(f9167,plain,
( k5_conlat_1(sK74) != k3_conlat_2(sK74,k2_subset_1(u1_struct_0(k11_conlat_1(sK74))))
| k6_conlat_1(sK74) != k2_conlat_2(sK74,k2_subset_1(u1_struct_0(k11_conlat_1(sK74)))) ),
inference(cnf_transformation,[],[f8197]) ).
fof(f9172,plain,
! [X0] : m1_subset_1(k2_subset_1(X0),k1_zfmisc_1(X0)),
inference(cnf_transformation,[],[f450]) ).
fof(f9179,plain,
! [X0] : k2_subset_1(X0) = X0,
inference(cnf_transformation,[],[f368]) ).
fof(f9190,plain,
! [X0] :
( ~ l2_conlat_1(X0)
| v3_conlat_1(X0)
| k5_conlat_1(X0) = k6_lattices(k11_conlat_1(X0)) ),
inference(cnf_transformation,[],[f5557]) ).
fof(f9191,plain,
! [X0] :
( ~ l2_conlat_1(X0)
| v3_conlat_1(X0)
| k6_conlat_1(X0) = k5_lattices(k11_conlat_1(X0)) ),
inference(cnf_transformation,[],[f5557]) ).
fof(f9195,plain,
! [X0] :
( v13_lattices(k11_conlat_1(X0))
| ~ sP0(X0) ),
inference(cnf_transformation,[],[f8203]) ).
fof(f9205,plain,
! [X0] :
( ~ l2_conlat_1(X0)
| v3_conlat_1(X0)
| sP0(X0) ),
inference(cnf_transformation,[],[f8072]) ).
fof(f9210,plain,
! [X0] :
( v4_lattice3(k11_conlat_1(X0))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f5563]) ).
fof(f9213,plain,
! [X0] :
( l3_lattices(k11_conlat_1(X0))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f5565]) ).
fof(f9214,plain,
! [X0] :
( v10_lattices(k11_conlat_1(X0))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f5565]) ).
fof(f9215,plain,
! [X0] :
( ~ v3_struct_0(k11_conlat_1(X0))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[],[f5565]) ).
fof(f9272,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,[],[f5597]) ).
fof(f9276,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,[],[f5601]) ).
fof(f9288,plain,
! [X0,X1] :
( ~ r2_hidden(X0,X1)
| m1_subset_1(X0,X1) ),
inference(cnf_transformation,[],[f5614]) ).
fof(f9306,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,X0)
| r2_hidden(X1,X0)
| v1_xboole_0(X0) ),
inference(cnf_transformation,[],[f8222]) ).
fof(f9432,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(X1))
| r1_tarski(X0,X1) ),
inference(cnf_transformation,[],[f8248]) ).
fof(f9629,plain,
! [X0] : r1_tarski(X0,X0),
inference(cnf_transformation,[],[f5481]) ).
fof(f9702,plain,
! [X0,X1] :
( m1_subset_1(k15_lattice3(X0,X1),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f5886]) ).
fof(f9703,plain,
! [X0] :
( ~ v4_lattice3(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| k6_lattices(X0) = k15_lattice3(X0,u1_struct_0(X0))
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f5888]) ).
fof(f9716,plain,
! [X2,X0,X1] :
( r3_lattices(X0,k16_lattice3(X0,X2),k16_lattice3(X0,X1))
| ~ r1_tarski(X1,X2)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v4_lattice3(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f5894]) ).
fof(f9717,plain,
! [X2,X0,X1] :
( r3_lattices(X0,k15_lattice3(X0,X1),k15_lattice3(X0,X2))
| ~ r1_tarski(X1,X2)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v4_lattice3(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f5894]) ).
fof(f9720,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,u1_struct_0(X0))
| k16_lattice3(X0,k1_struct_0(X0,X1)) = X1
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v4_lattice3(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f5898]) ).
fof(f9724,plain,
! [X2,X0,X1] :
( r3_lattices(X0,X1,k15_lattice3(X0,X2))
| ~ r2_hidden(X1,X2)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v4_lattice3(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f5902]) ).
fof(f9730,plain,
! [X0,X1] :
( m1_subset_1(k16_lattice3(X0,X1),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f5906]) ).
fof(f9752,plain,
! [X0] :
( m1_subset_1(k5_lattices(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_lattices(X0) ),
inference(cnf_transformation,[],[f5932]) ).
fof(f9756,plain,
! [X0,X1] :
( r3_lattices(X0,k5_lattices(X0),X1)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v13_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f5938]) ).
fof(f9774,plain,
! [X0] :
( m1_subset_1(k6_lattices(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l2_lattices(X0) ),
inference(cnf_transformation,[],[f5960]) ).
fof(f9912,plain,
! [X2,X0,X1] :
( ~ r1_lattices(X0,X2,X1)
| ~ r1_lattices(X0,X1,X2)
| X1 = X2
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v4_lattices(X0)
| ~ l2_lattices(X0) ),
inference(cnf_transformation,[],[f5995]) ).
fof(f9926,plain,
! [X0] :
( v9_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f6003]) ).
fof(f9927,plain,
! [X0] :
( v8_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f6003]) ).
fof(f9929,plain,
! [X0] :
( v6_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f6003]) ).
fof(f9931,plain,
! [X0] :
( v4_lattices(X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f6003]) ).
fof(f9943,plain,
! [X2,X0,X1] :
( ~ r3_lattices(X0,X1,X2)
| r1_lattices(X0,X1,X2)
| v3_struct_0(X0)
| ~ v6_lattices(X0)
| ~ v8_lattices(X0)
| ~ v9_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f8369]) ).
fof(f10734,plain,
! [X0] : k1_tarski(X0) = k2_tarski(X0,X0),
inference(cnf_transformation,[],[f144]) ).
fof(f10815,plain,
! [X0] :
( m1_subset_1(k2_pre_topc(X0),k1_zfmisc_1(u1_struct_0(X0)))
| ~ l1_struct_0(X0) ),
inference(cnf_transformation,[],[f6514]) ).
fof(f10822,plain,
! [X0] :
( ~ l1_struct_0(X0)
| u1_struct_0(X0) = k2_pre_topc(X0) ),
inference(cnf_transformation,[],[f6523]) ).
fof(f10931,plain,
! [X0] :
( ~ l2_lattices(X0)
| l1_struct_0(X0) ),
inference(cnf_transformation,[],[f6609]) ).
fof(f10937,plain,
! [X0] :
( ~ v1_xboole_0(u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0) ),
inference(cnf_transformation,[],[f6614]) ).
fof(f11011,plain,
! [X2,X0,X1] :
( m1_filter_0(k5_subset_1(u1_struct_0(X0),X1,X2),X0)
| ~ m1_filter_0(X2,X0)
| ~ m1_filter_0(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f6660]) ).
fof(f11014,plain,
! [X2,X0,X1] :
( k5_subset_1(X0,X1,X2) = k3_xboole_0(X1,X2)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| ~ m1_subset_1(X2,k1_zfmisc_1(X0)) ),
inference(cnf_transformation,[],[f6666]) ).
fof(f11422,plain,
! [X0,X1] : k3_xboole_0(X0,X1) = k1_setfam_1(k2_tarski(X0,X1)),
inference(cnf_transformation,[],[f488]) ).
fof(f11857,plain,
! [X0,X1] :
( k1_tarski(X1) = k1_struct_0(X0,X1)
| v3_struct_0(X0)
| ~ l1_struct_0(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f7142]) ).
fof(f11858,plain,
! [X0,X1] :
( m1_subset_1(k1_struct_0(X0,X1),k1_zfmisc_1(u1_struct_0(X0)))
| v3_struct_0(X0)
| ~ l1_struct_0(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0)) ),
inference(cnf_transformation,[],[f7144]) ).
fof(f12061,plain,
! [X0] :
( ~ l3_lattices(X0)
| l2_lattices(X0) ),
inference(cnf_transformation,[],[f7306]) ).
fof(f12062,plain,
! [X0] :
( ~ l3_lattices(X0)
| l1_lattices(X0) ),
inference(cnf_transformation,[],[f7306]) ).
fof(f12136,plain,
! [X0,X1] :
( m1_subset_1(X1,k1_zfmisc_1(u1_struct_0(X0)))
| ~ m1_filter_0(X1,X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f7379]) ).
fof(f12138,plain,
! [X0] :
( m1_filter_0(u1_struct_0(X0),X0)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[],[f7381]) ).
fof(f13094,plain,
! [X0] : k3_xboole_0(X0,X0) = X0,
inference(cnf_transformation,[],[f5512]) ).
fof(f13438,plain,
! [X2,X0,X1] :
( ~ m1_subset_1(X2,k1_zfmisc_1(X0))
| ~ m1_subset_1(X1,k1_zfmisc_1(X0))
| k5_subset_1(X0,X1,X2) = k1_setfam_1(k2_tarski(X1,X2)) ),
inference(definition_unfolding,[],[f11014,f11422]) ).
fof(f13465,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l1_struct_0(X0)
| k1_struct_0(X0,X1) = k2_tarski(X1,X1) ),
inference(definition_unfolding,[],[f11857,f10734]) ).
fof(f13595,plain,
! [X0] : k1_setfam_1(k2_tarski(X0,X0)) = X0,
inference(definition_unfolding,[],[f13094,f11422]) ).
fof(f14063,plain,
! [X0] : m1_subset_1(X0,k1_zfmisc_1(X0)),
inference(forward_demodulation,[],[f9172,f9179]) ).
fof(f14066,plain,
( k5_conlat_1(sK74) != k3_conlat_2(sK74,u1_struct_0(k11_conlat_1(sK74)))
| k6_conlat_1(sK74) != k2_conlat_2(sK74,k2_subset_1(u1_struct_0(k11_conlat_1(sK74)))) ),
inference(forward_demodulation,[],[f9167,f9179]) ).
fof(f14091,plain,
( k6_conlat_1(sK74) != k2_conlat_2(sK74,u1_struct_0(k11_conlat_1(sK74)))
| k5_conlat_1(sK74) != k3_conlat_2(sK74,u1_struct_0(k11_conlat_1(sK74))) ),
inference(forward_demodulation,[],[f14066,f9179]) ).
fof(f14106,definition,
( spl609_9
<=> k5_conlat_1(sK74) = k3_conlat_2(sK74,u1_struct_0(k11_conlat_1(sK74))) ),
introduced(definition,[new_symbols(definition,[spl609_9])],[avatar_definition]) ).
fof(f14110,definition,
( spl609_10
<=> k6_conlat_1(sK74) = k2_conlat_2(sK74,u1_struct_0(k11_conlat_1(sK74))) ),
introduced(definition,[new_symbols(definition,[spl609_10])],[avatar_definition]) ).
fof(f14112,plain,
( k6_conlat_1(sK74) != k2_conlat_2(sK74,u1_struct_0(k11_conlat_1(sK74)))
| spl609_10 ),
inference(avatar_component_clause,[],[f14110]) ).
fof(f14113,plain,
( ~ spl609_9
| ~ spl609_10 ),
inference(avatar_split_clause,[],[f14091,f14110,f14106]) ).
fof(f14119,plain,
( v3_conlat_1(sK74)
| k5_conlat_1(sK74) = k6_lattices(k11_conlat_1(sK74)) ),
inference(resolution,[],[f9165,f9190]) ).
fof(f14120,plain,
( v3_conlat_1(sK74)
| k6_conlat_1(sK74) = k5_lattices(k11_conlat_1(sK74)) ),
inference(resolution,[],[f9165,f9191]) ).
fof(f14121,plain,
k6_conlat_1(sK74) = k5_lattices(k11_conlat_1(sK74)),
inference(forward_subsumption_resolution,[],[f14120,f9166]) ).
fof(f14122,plain,
k5_conlat_1(sK74) = k6_lattices(k11_conlat_1(sK74)),
inference(forward_subsumption_resolution,[],[f14119,f9166]) ).
fof(f14131,plain,
( v3_conlat_1(sK74)
| sP0(sK74) ),
inference(resolution,[],[f9205,f9165]) ).
fof(f14132,plain,
sP0(sK74),
inference(forward_subsumption_resolution,[],[f14131,f9166]) ).
fof(f14178,definition,
( spl609_11
<=> l3_lattices(k11_conlat_1(sK74)) ),
introduced(definition,[new_symbols(definition,[spl609_11])],[avatar_definition]) ).
fof(f14179,plain,
( l3_lattices(k11_conlat_1(sK74))
| ~ spl609_11 ),
inference(avatar_component_clause,[],[f14178]) ).
fof(f14180,plain,
( ~ l3_lattices(k11_conlat_1(sK74))
| spl609_11 ),
inference(avatar_component_clause,[],[f14178]) ).
fof(f14182,definition,
( spl609_12
<=> v3_struct_0(k11_conlat_1(sK74)) ),
introduced(definition,[new_symbols(definition,[spl609_12])],[avatar_definition]) ).
fof(f14183,plain,
( ~ v3_struct_0(k11_conlat_1(sK74))
| spl609_12 ),
inference(avatar_component_clause,[],[f14182]) ).
fof(f14184,plain,
( v3_struct_0(k11_conlat_1(sK74))
| ~ spl609_12 ),
inference(avatar_component_clause,[],[f14182]) ).
fof(f14189,plain,
( v3_conlat_1(sK74)
| ~ l2_conlat_1(sK74)
| spl609_11 ),
inference(resolution,[],[f14180,f9213]) ).
fof(f14190,plain,
( ~ l2_conlat_1(sK74)
| spl609_11 ),
inference(forward_subsumption_resolution,[],[f14189,f9166]) ).
fof(f14191,plain,
( $false
| spl609_11 ),
inference(forward_subsumption_resolution,[],[f14190,f9165]) ).
fof(f14192,plain,
spl609_11,
inference(avatar_contradiction_clause,[],[f14191]) ).
fof(f14193,plain,
( v3_conlat_1(sK74)
| ~ l2_conlat_1(sK74)
| ~ spl609_12 ),
inference(resolution,[],[f14184,f9215]) ).
fof(f14194,plain,
( ~ l2_conlat_1(sK74)
| ~ spl609_12 ),
inference(forward_subsumption_resolution,[],[f14193,f9166]) ).
fof(f14195,plain,
( $false
| ~ spl609_12 ),
inference(forward_subsumption_resolution,[],[f14194,f9165]) ).
fof(f14196,plain,
~ spl609_12,
inference(avatar_contradiction_clause,[],[f14195]) ).
fof(f14210,definition,
( spl609_16
<=> v1_xboole_0(u1_struct_0(k11_conlat_1(sK74))) ),
introduced(definition,[new_symbols(definition,[spl609_16])],[avatar_definition]) ).
fof(f14211,plain,
( v1_xboole_0(u1_struct_0(k11_conlat_1(sK74)))
| ~ spl609_16 ),
inference(avatar_component_clause,[],[f14210]) ).
fof(f14329,plain,
( m1_subset_1(k6_conlat_1(sK74),u1_struct_0(k11_conlat_1(sK74)))
| v3_struct_0(k11_conlat_1(sK74))
| ~ l1_lattices(k11_conlat_1(sK74)) ),
inference(superposition,[],[f9752,f14121]) ).
fof(f14340,plain,
( m1_subset_1(k6_conlat_1(sK74),u1_struct_0(k11_conlat_1(sK74)))
| ~ l1_lattices(k11_conlat_1(sK74))
| spl609_12 ),
inference(forward_subsumption_resolution,[],[f14329,f14183]) ).
fof(f14346,definition,
( spl609_24
<=> l1_lattices(k11_conlat_1(sK74)) ),
introduced(definition,[new_symbols(definition,[spl609_24])],[avatar_definition]) ).
fof(f14348,plain,
( ~ l1_lattices(k11_conlat_1(sK74))
| spl609_24 ),
inference(avatar_component_clause,[],[f14346]) ).
fof(f14350,definition,
( spl609_25
<=> m1_subset_1(k6_conlat_1(sK74),u1_struct_0(k11_conlat_1(sK74))) ),
introduced(definition,[new_symbols(definition,[spl609_25])],[avatar_definition]) ).
fof(f14352,plain,
( m1_subset_1(k6_conlat_1(sK74),u1_struct_0(k11_conlat_1(sK74)))
| ~ spl609_25 ),
inference(avatar_component_clause,[],[f14350]) ).
fof(f14353,plain,
( ~ spl609_24
| spl609_25
| spl609_12 ),
inference(avatar_split_clause,[],[f14340,f14182,f14350,f14346]) ).
fof(f14365,plain,
! [X0] :
( l2_lattices(k11_conlat_1(X0))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(resolution,[],[f12061,f9213]) ).
fof(f14366,plain,
( l2_lattices(k11_conlat_1(sK74))
| ~ spl609_11 ),
inference(resolution,[],[f12061,f14179]) ).
fof(f14367,plain,
( l1_struct_0(k11_conlat_1(sK74))
| ~ spl609_11 ),
inference(resolution,[],[f10931,f14366]) ).
fof(f14368,plain,
! [X0] :
( l1_struct_0(k11_conlat_1(X0))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(resolution,[],[f10931,f14365]) ).
fof(f14370,plain,
( u1_struct_0(k11_conlat_1(sK74)) = k2_pre_topc(k11_conlat_1(sK74))
| ~ spl609_11 ),
inference(resolution,[],[f14367,f10822]) ).
fof(f14379,definition,
( spl609_27
<=> v10_lattices(k11_conlat_1(sK74)) ),
introduced(definition,[new_symbols(definition,[spl609_27])],[avatar_definition]) ).
fof(f14380,plain,
( v10_lattices(k11_conlat_1(sK74))
| ~ spl609_27 ),
inference(avatar_component_clause,[],[f14379]) ).
fof(f14381,plain,
( ~ v10_lattices(k11_conlat_1(sK74))
| spl609_27 ),
inference(avatar_component_clause,[],[f14379]) ).
fof(f14392,plain,
( v3_conlat_1(sK74)
| ~ l2_conlat_1(sK74)
| spl609_27 ),
inference(resolution,[],[f14381,f9214]) ).
fof(f14393,plain,
( ~ l2_conlat_1(sK74)
| spl609_27 ),
inference(forward_subsumption_resolution,[],[f14392,f9166]) ).
fof(f14400,plain,
( $false
| spl609_27 ),
inference(forward_subsumption_resolution,[],[f14393,f9165]) ).
fof(f14401,plain,
spl609_27,
inference(avatar_contradiction_clause,[],[f14400]) ).
fof(f14407,definition,
( spl609_29
<=> v13_lattices(k11_conlat_1(sK74)) ),
introduced(definition,[new_symbols(definition,[spl609_29])],[avatar_definition]) ).
fof(f14408,plain,
( v13_lattices(k11_conlat_1(sK74))
| ~ spl609_29 ),
inference(avatar_component_clause,[],[f14407]) ).
fof(f14409,plain,
( ~ v13_lattices(k11_conlat_1(sK74))
| spl609_29 ),
inference(avatar_component_clause,[],[f14407]) ).
fof(f14414,plain,
( ~ sP0(sK74)
| spl609_29 ),
inference(resolution,[],[f14409,f9195]) ).
fof(f14415,plain,
( $false
| spl609_29 ),
inference(forward_subsumption_resolution,[],[f14414,f14132]) ).
fof(f14416,plain,
spl609_29,
inference(avatar_contradiction_clause,[],[f14415]) ).
fof(f14472,plain,
( m1_subset_1(k5_conlat_1(sK74),u1_struct_0(k11_conlat_1(sK74)))
| v3_struct_0(k11_conlat_1(sK74))
| ~ l2_lattices(k11_conlat_1(sK74)) ),
inference(superposition,[],[f9774,f14122]) ).
fof(f14484,plain,
( m1_subset_1(k5_conlat_1(sK74),u1_struct_0(k11_conlat_1(sK74)))
| ~ l2_lattices(k11_conlat_1(sK74))
| spl609_12 ),
inference(forward_subsumption_resolution,[],[f14472,f14183]) ).
fof(f14490,plain,
( m1_subset_1(k5_conlat_1(sK74),u1_struct_0(k11_conlat_1(sK74)))
| ~ spl609_11
| spl609_12 ),
inference(forward_subsumption_resolution,[],[f14484,f14366]) ).
fof(f14500,plain,
( r2_hidden(k5_conlat_1(sK74),u1_struct_0(k11_conlat_1(sK74)))
| v1_xboole_0(u1_struct_0(k11_conlat_1(sK74)))
| ~ spl609_11
| spl609_12 ),
inference(resolution,[],[f14490,f9306]) ).
fof(f14502,definition,
( spl609_33
<=> r2_hidden(k5_conlat_1(sK74),u1_struct_0(k11_conlat_1(sK74))) ),
introduced(definition,[new_symbols(definition,[spl609_33])],[avatar_definition]) ).
fof(f14504,plain,
( r2_hidden(k5_conlat_1(sK74),u1_struct_0(k11_conlat_1(sK74)))
| ~ spl609_33 ),
inference(avatar_component_clause,[],[f14502]) ).
fof(f14505,plain,
( spl609_16
| spl609_33
| ~ spl609_11
| spl609_12 ),
inference(avatar_split_clause,[],[f14500,f14182,f14178,f14502,f14210]) ).
fof(f14538,plain,
( v3_struct_0(k11_conlat_1(sK74))
| ~ l1_struct_0(k11_conlat_1(sK74))
| ~ spl609_16 ),
inference(resolution,[],[f14211,f10937]) ).
fof(f14539,plain,
( ~ l1_struct_0(k11_conlat_1(sK74))
| spl609_12
| ~ spl609_16 ),
inference(forward_subsumption_resolution,[],[f14538,f14183]) ).
fof(f14540,plain,
( $false
| ~ spl609_11
| spl609_12
| ~ spl609_16 ),
inference(forward_subsumption_resolution,[],[f14539,f14367]) ).
fof(f14541,plain,
( ~ spl609_11
| spl609_12
| ~ spl609_16 ),
inference(avatar_contradiction_clause,[],[f14540]) ).
fof(f14549,plain,
! [X2,X0,X1] :
( r1_lattices(X0,X1,k15_lattice3(X0,X2))
| v3_struct_0(X0)
| ~ v6_lattices(X0)
| ~ v8_lattices(X0)
| ~ v9_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(k15_lattice3(X0,X2),u1_struct_0(X0))
| ~ r2_hidden(X1,X2)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v4_lattice3(X0)
| ~ l3_lattices(X0) ),
inference(resolution,[],[f9943,f9724]) ).
fof(f14551,plain,
! [X0,X1] :
( r1_lattices(X0,k5_lattices(X0),X1)
| v3_struct_0(X0)
| ~ v6_lattices(X0)
| ~ v8_lattices(X0)
| ~ v9_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(k5_lattices(X0),u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v13_lattices(X0)
| ~ l3_lattices(X0) ),
inference(resolution,[],[f9943,f9756]) ).
fof(f14552,plain,
! [X2,X0,X1] :
( r1_lattices(X0,k15_lattice3(X0,X1),k15_lattice3(X0,X2))
| v3_struct_0(X0)
| ~ v6_lattices(X0)
| ~ v8_lattices(X0)
| ~ v9_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(k15_lattice3(X0,X1),u1_struct_0(X0))
| ~ m1_subset_1(k15_lattice3(X0,X2),u1_struct_0(X0))
| ~ r1_tarski(X1,X2)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v4_lattice3(X0)
| ~ l3_lattices(X0) ),
inference(resolution,[],[f9943,f9717]) ).
fof(f14554,plain,
! [X2,X0,X1] :
( r1_lattices(X0,k16_lattice3(X0,X1),k16_lattice3(X0,X2))
| v3_struct_0(X0)
| ~ v6_lattices(X0)
| ~ v8_lattices(X0)
| ~ v9_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(k16_lattice3(X0,X1),u1_struct_0(X0))
| ~ m1_subset_1(k16_lattice3(X0,X2),u1_struct_0(X0))
| ~ r1_tarski(X2,X1)
| v3_struct_0(X0)
| ~ v10_lattices(X0)
| ~ v4_lattice3(X0)
| ~ l3_lattices(X0) ),
inference(resolution,[],[f9943,f9716]) ).
fof(f14559,plain,
! [X2,X0,X1] :
( r1_lattices(X0,k16_lattice3(X0,X1),k16_lattice3(X0,X2))
| v3_struct_0(X0)
| ~ v6_lattices(X0)
| ~ v8_lattices(X0)
| ~ v9_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(k16_lattice3(X0,X1),u1_struct_0(X0))
| ~ m1_subset_1(k16_lattice3(X0,X2),u1_struct_0(X0))
| ~ r1_tarski(X2,X1)
| ~ v10_lattices(X0)
| ~ v4_lattice3(X0) ),
inference(duplicate_literal_removal,[],[f14554]) ).
fof(f14561,plain,
! [X2,X0,X1] :
( r1_lattices(X0,k15_lattice3(X0,X1),k15_lattice3(X0,X2))
| v3_struct_0(X0)
| ~ v6_lattices(X0)
| ~ v8_lattices(X0)
| ~ v9_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(k15_lattice3(X0,X1),u1_struct_0(X0))
| ~ m1_subset_1(k15_lattice3(X0,X2),u1_struct_0(X0))
| ~ r1_tarski(X1,X2)
| ~ v10_lattices(X0)
| ~ v4_lattice3(X0) ),
inference(duplicate_literal_removal,[],[f14552]) ).
fof(f14562,plain,
! [X0,X1] :
( r1_lattices(X0,k5_lattices(X0),X1)
| v3_struct_0(X0)
| ~ v6_lattices(X0)
| ~ v8_lattices(X0)
| ~ v9_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(k5_lattices(X0),u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ v10_lattices(X0)
| ~ v13_lattices(X0) ),
inference(duplicate_literal_removal,[],[f14551]) ).
fof(f14564,plain,
! [X2,X0,X1] :
( r1_lattices(X0,X1,k15_lattice3(X0,X2))
| v3_struct_0(X0)
| ~ v6_lattices(X0)
| ~ v8_lattices(X0)
| ~ v9_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(k15_lattice3(X0,X2),u1_struct_0(X0))
| ~ r2_hidden(X1,X2)
| ~ v10_lattices(X0)
| ~ v4_lattice3(X0) ),
inference(duplicate_literal_removal,[],[f14549]) ).
fof(f14567,plain,
! [X2,X0,X1] :
( r1_lattices(X0,k16_lattice3(X0,X1),k16_lattice3(X0,X2))
| v3_struct_0(X0)
| ~ v8_lattices(X0)
| ~ v9_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(k16_lattice3(X0,X1),u1_struct_0(X0))
| ~ m1_subset_1(k16_lattice3(X0,X2),u1_struct_0(X0))
| ~ r1_tarski(X2,X1)
| ~ v10_lattices(X0)
| ~ v4_lattice3(X0) ),
inference(forward_subsumption_resolution,[],[f14559,f9929]) ).
fof(f14569,plain,
! [X2,X0,X1] :
( r1_lattices(X0,k15_lattice3(X0,X1),k15_lattice3(X0,X2))
| v3_struct_0(X0)
| ~ v8_lattices(X0)
| ~ v9_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(k15_lattice3(X0,X1),u1_struct_0(X0))
| ~ m1_subset_1(k15_lattice3(X0,X2),u1_struct_0(X0))
| ~ r1_tarski(X1,X2)
| ~ v10_lattices(X0)
| ~ v4_lattice3(X0) ),
inference(forward_subsumption_resolution,[],[f14561,f9929]) ).
fof(f14570,plain,
! [X0,X1] :
( r1_lattices(X0,k5_lattices(X0),X1)
| v3_struct_0(X0)
| ~ v8_lattices(X0)
| ~ v9_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(k5_lattices(X0),u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ v10_lattices(X0)
| ~ v13_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f14562,f9929]) ).
fof(f14572,plain,
! [X2,X0,X1] :
( r1_lattices(X0,X1,k15_lattice3(X0,X2))
| v3_struct_0(X0)
| ~ v8_lattices(X0)
| ~ v9_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(k15_lattice3(X0,X2),u1_struct_0(X0))
| ~ r2_hidden(X1,X2)
| ~ v10_lattices(X0)
| ~ v4_lattice3(X0) ),
inference(forward_subsumption_resolution,[],[f14564,f9929]) ).
fof(f14575,plain,
! [X2,X0,X1] :
( r1_lattices(X0,k16_lattice3(X0,X1),k16_lattice3(X0,X2))
| v3_struct_0(X0)
| ~ v9_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(k16_lattice3(X0,X1),u1_struct_0(X0))
| ~ m1_subset_1(k16_lattice3(X0,X2),u1_struct_0(X0))
| ~ r1_tarski(X2,X1)
| ~ v10_lattices(X0)
| ~ v4_lattice3(X0) ),
inference(forward_subsumption_resolution,[],[f14567,f9927]) ).
fof(f14577,plain,
! [X2,X0,X1] :
( r1_lattices(X0,k15_lattice3(X0,X1),k15_lattice3(X0,X2))
| v3_struct_0(X0)
| ~ v9_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(k15_lattice3(X0,X1),u1_struct_0(X0))
| ~ m1_subset_1(k15_lattice3(X0,X2),u1_struct_0(X0))
| ~ r1_tarski(X1,X2)
| ~ v10_lattices(X0)
| ~ v4_lattice3(X0) ),
inference(forward_subsumption_resolution,[],[f14569,f9927]) ).
fof(f14578,plain,
! [X0,X1] :
( r1_lattices(X0,k5_lattices(X0),X1)
| v3_struct_0(X0)
| ~ v9_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(k5_lattices(X0),u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ v10_lattices(X0)
| ~ v13_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f14570,f9927]) ).
fof(f14580,plain,
! [X2,X0,X1] :
( r1_lattices(X0,X1,k15_lattice3(X0,X2))
| v3_struct_0(X0)
| ~ v9_lattices(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(k15_lattice3(X0,X2),u1_struct_0(X0))
| ~ r2_hidden(X1,X2)
| ~ v10_lattices(X0)
| ~ v4_lattice3(X0) ),
inference(forward_subsumption_resolution,[],[f14572,f9927]) ).
fof(f14594,definition,
( spl609_37
<=> ! [X0] :
( r1_lattices(k11_conlat_1(sK74),k6_conlat_1(sK74),X0)
| ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK74))) ) ),
introduced(definition,[new_symbols(definition,[spl609_37])],[avatar_definition]) ).
fof(f14595,plain,
( ! [X0] :
( r1_lattices(k11_conlat_1(sK74),k6_conlat_1(sK74),X0)
| ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK74))) )
| ~ spl609_37 ),
inference(avatar_component_clause,[],[f14594]) ).
fof(f14598,plain,
! [X2,X0,X1] :
( r1_lattices(X0,k16_lattice3(X0,X1),k16_lattice3(X0,X2))
| v3_struct_0(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(k16_lattice3(X0,X1),u1_struct_0(X0))
| ~ m1_subset_1(k16_lattice3(X0,X2),u1_struct_0(X0))
| ~ r1_tarski(X2,X1)
| ~ v10_lattices(X0)
| ~ v4_lattice3(X0) ),
inference(forward_subsumption_resolution,[],[f14575,f9926]) ).
fof(f14600,plain,
! [X2,X0,X1] :
( r1_lattices(X0,k15_lattice3(X0,X1),k15_lattice3(X0,X2))
| v3_struct_0(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(k15_lattice3(X0,X1),u1_struct_0(X0))
| ~ m1_subset_1(k15_lattice3(X0,X2),u1_struct_0(X0))
| ~ r1_tarski(X1,X2)
| ~ v10_lattices(X0)
| ~ v4_lattice3(X0) ),
inference(forward_subsumption_resolution,[],[f14577,f9926]) ).
fof(f14601,plain,
! [X0,X1] :
( ~ m1_subset_1(k5_lattices(X0),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0)
| r1_lattices(X0,k5_lattices(X0),X1)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ v10_lattices(X0)
| ~ v13_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f14578,f9926]) ).
fof(f14603,plain,
! [X2,X0,X1] :
( r1_lattices(X0,X1,k15_lattice3(X0,X2))
| v3_struct_0(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ m1_subset_1(k15_lattice3(X0,X2),u1_struct_0(X0))
| ~ r2_hidden(X1,X2)
| ~ v10_lattices(X0)
| ~ v4_lattice3(X0) ),
inference(forward_subsumption_resolution,[],[f14580,f9926]) ).
fof(f14608,plain,
! [X2,X0,X1] :
( r1_lattices(X0,k16_lattice3(X0,X1),k16_lattice3(X0,X2))
| v3_struct_0(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(k16_lattice3(X0,X2),u1_struct_0(X0))
| ~ r1_tarski(X2,X1)
| ~ v10_lattices(X0)
| ~ v4_lattice3(X0) ),
inference(forward_subsumption_resolution,[],[f14598,f9730]) ).
fof(f14610,plain,
! [X2,X0,X1] :
( r1_lattices(X0,k15_lattice3(X0,X1),k15_lattice3(X0,X2))
| v3_struct_0(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(k15_lattice3(X0,X2),u1_struct_0(X0))
| ~ r1_tarski(X1,X2)
| ~ v10_lattices(X0)
| ~ v4_lattice3(X0) ),
inference(forward_subsumption_resolution,[],[f14600,f9702]) ).
fof(f14611,plain,
! [X2,X0,X1] :
( r1_lattices(X0,X1,k15_lattice3(X0,X2))
| v3_struct_0(X0)
| ~ l3_lattices(X0)
| ~ m1_subset_1(X1,u1_struct_0(X0))
| ~ r2_hidden(X1,X2)
| ~ v10_lattices(X0)
| ~ v4_lattice3(X0) ),
inference(forward_subsumption_resolution,[],[f14603,f9702]) ).
fof(f14612,plain,
! [X2,X0,X1] :
( r1_lattices(X0,k16_lattice3(X0,X1),k16_lattice3(X0,X2))
| v3_struct_0(X0)
| ~ l3_lattices(X0)
| ~ r1_tarski(X2,X1)
| ~ v10_lattices(X0)
| ~ v4_lattice3(X0) ),
inference(forward_subsumption_resolution,[],[f14608,f9730]) ).
fof(f14613,plain,
! [X2,X0,X1] :
( r1_lattices(X0,k15_lattice3(X0,X1),k15_lattice3(X0,X2))
| v3_struct_0(X0)
| ~ l3_lattices(X0)
| ~ r1_tarski(X1,X2)
| ~ v10_lattices(X0)
| ~ v4_lattice3(X0) ),
inference(forward_subsumption_resolution,[],[f14610,f9702]) ).
fof(f14616,plain,
! [X0,X1] :
( ~ m1_subset_1(X0,k1_zfmisc_1(X1))
| k1_setfam_1(k2_tarski(X0,X1)) = k5_subset_1(X1,X0,X1) ),
inference(resolution,[],[f13438,f14063]) ).
fof(f14673,plain,
! [X0,X1] :
( ~ m1_filter_0(X0,k11_conlat_1(X1))
| v3_struct_0(k11_conlat_1(X1))
| ~ v10_lattices(k11_conlat_1(X1))
| ~ l3_lattices(k11_conlat_1(X1))
| k3_conlat_2(X1,X0) = k15_lattice3(k11_conlat_1(X1),X0)
| v3_conlat_1(X1)
| ~ l2_conlat_1(X1) ),
inference(resolution,[],[f12136,f9276]) ).
fof(f14687,plain,
! [X0,X1] :
( ~ m1_filter_0(X0,k11_conlat_1(X1))
| v3_struct_0(k11_conlat_1(X1))
| ~ v10_lattices(k11_conlat_1(X1))
| k3_conlat_2(X1,X0) = k15_lattice3(k11_conlat_1(X1),X0)
| v3_conlat_1(X1)
| ~ l2_conlat_1(X1) ),
inference(forward_subsumption_resolution,[],[f14673,f9213]) ).
fof(f14699,plain,
! [X0,X1] :
( ~ m1_filter_0(X0,k11_conlat_1(X1))
| ~ v10_lattices(k11_conlat_1(X1))
| k3_conlat_2(X1,X0) = k15_lattice3(k11_conlat_1(X1),X0)
| v3_conlat_1(X1)
| ~ l2_conlat_1(X1) ),
inference(forward_subsumption_resolution,[],[f14687,f9215]) ).
fof(f14711,plain,
! [X0,X1] :
( ~ m1_filter_0(X0,k11_conlat_1(X1))
| k3_conlat_2(X1,X0) = k15_lattice3(k11_conlat_1(X1),X0)
| v3_conlat_1(X1)
| ~ l2_conlat_1(X1) ),
inference(forward_subsumption_resolution,[],[f14699,f9214]) ).
fof(f14746,plain,
( l1_lattices(k11_conlat_1(sK74))
| ~ spl609_11 ),
inference(resolution,[],[f12062,f14179]) ).
fof(f14747,plain,
( $false
| ~ spl609_11
| spl609_24 ),
inference(forward_subsumption_resolution,[],[f14746,f14348]) ).
fof(f14748,plain,
( ~ spl609_11
| spl609_24 ),
inference(avatar_contradiction_clause,[],[f14747]) ).
fof(f14755,plain,
( v3_struct_0(k11_conlat_1(sK74))
| ~ l1_struct_0(k11_conlat_1(sK74))
| k1_struct_0(k11_conlat_1(sK74),k6_conlat_1(sK74)) = k2_tarski(k6_conlat_1(sK74),k6_conlat_1(sK74))
| ~ spl609_25 ),
inference(resolution,[],[f14352,f13465]) ).
fof(f14758,plain,
( ~ l1_struct_0(k11_conlat_1(sK74))
| k1_struct_0(k11_conlat_1(sK74),k6_conlat_1(sK74)) = k2_tarski(k6_conlat_1(sK74),k6_conlat_1(sK74))
| spl609_12
| ~ spl609_25 ),
inference(forward_subsumption_resolution,[],[f14755,f14183]) ).
fof(f14764,plain,
( k1_struct_0(k11_conlat_1(sK74),k6_conlat_1(sK74)) = k2_tarski(k6_conlat_1(sK74),k6_conlat_1(sK74))
| ~ spl609_11
| spl609_12
| ~ spl609_25 ),
inference(forward_subsumption_resolution,[],[f14758,f14367]) ).
fof(f14913,plain,
( k6_conlat_1(sK74) = k16_lattice3(k11_conlat_1(sK74),k1_struct_0(k11_conlat_1(sK74),k6_conlat_1(sK74)))
| v3_struct_0(k11_conlat_1(sK74))
| ~ v10_lattices(k11_conlat_1(sK74))
| ~ v4_lattice3(k11_conlat_1(sK74))
| ~ l3_lattices(k11_conlat_1(sK74))
| ~ spl609_25 ),
inference(resolution,[],[f9720,f14352]) ).
fof(f14920,plain,
( k6_conlat_1(sK74) = k16_lattice3(k11_conlat_1(sK74),k1_struct_0(k11_conlat_1(sK74),k6_conlat_1(sK74)))
| ~ v10_lattices(k11_conlat_1(sK74))
| ~ v4_lattice3(k11_conlat_1(sK74))
| ~ l3_lattices(k11_conlat_1(sK74))
| spl609_12
| ~ spl609_25 ),
inference(forward_subsumption_resolution,[],[f14913,f14183]) ).
fof(f14924,plain,
( k6_conlat_1(sK74) = k16_lattice3(k11_conlat_1(sK74),k1_struct_0(k11_conlat_1(sK74),k6_conlat_1(sK74)))
| ~ v4_lattice3(k11_conlat_1(sK74))
| ~ l3_lattices(k11_conlat_1(sK74))
| spl609_12
| ~ spl609_25
| ~ spl609_27 ),
inference(forward_subsumption_resolution,[],[f14920,f14380]) ).
fof(f14926,plain,
( k6_conlat_1(sK74) = k16_lattice3(k11_conlat_1(sK74),k1_struct_0(k11_conlat_1(sK74),k6_conlat_1(sK74)))
| ~ v4_lattice3(k11_conlat_1(sK74))
| ~ spl609_11
| spl609_12
| ~ spl609_25
| ~ spl609_27 ),
inference(forward_subsumption_resolution,[],[f14924,f14179]) ).
fof(f14928,plain,
( k6_conlat_1(sK74) = k16_lattice3(k11_conlat_1(sK74),k2_tarski(k6_conlat_1(sK74),k6_conlat_1(sK74)))
| ~ v4_lattice3(k11_conlat_1(sK74))
| ~ spl609_11
| spl609_12
| ~ spl609_25
| ~ spl609_27 ),
inference(forward_demodulation,[],[f14926,f14764]) ).
fof(f14931,definition,
( spl609_41
<=> v4_lattice3(k11_conlat_1(sK74)) ),
introduced(definition,[new_symbols(definition,[spl609_41])],[avatar_definition]) ).
fof(f14932,plain,
( v4_lattice3(k11_conlat_1(sK74))
| ~ spl609_41 ),
inference(avatar_component_clause,[],[f14931]) ).
fof(f14933,plain,
( ~ v4_lattice3(k11_conlat_1(sK74))
| spl609_41 ),
inference(avatar_component_clause,[],[f14931]) ).
fof(f14935,definition,
( spl609_42
<=> k6_conlat_1(sK74) = k16_lattice3(k11_conlat_1(sK74),k2_tarski(k6_conlat_1(sK74),k6_conlat_1(sK74))) ),
introduced(definition,[new_symbols(definition,[spl609_42])],[avatar_definition]) ).
fof(f14937,plain,
( k6_conlat_1(sK74) = k16_lattice3(k11_conlat_1(sK74),k2_tarski(k6_conlat_1(sK74),k6_conlat_1(sK74)))
| ~ spl609_42 ),
inference(avatar_component_clause,[],[f14935]) ).
fof(f14938,plain,
( ~ spl609_41
| spl609_42
| ~ spl609_11
| spl609_12
| ~ spl609_25
| ~ spl609_27 ),
inference(avatar_split_clause,[],[f14928,f14379,f14350,f14182,f14178,f14935,f14931]) ).
fof(f14946,plain,
( v3_conlat_1(sK74)
| ~ l2_conlat_1(sK74)
| spl609_41 ),
inference(resolution,[],[f14933,f9210]) ).
fof(f14947,plain,
( ~ l2_conlat_1(sK74)
| spl609_41 ),
inference(forward_subsumption_resolution,[],[f14946,f9166]) ).
fof(f14952,plain,
( $false
| spl609_41 ),
inference(forward_subsumption_resolution,[],[f14947,f9165]) ).
fof(f14953,plain,
spl609_41,
inference(avatar_contradiction_clause,[],[f14952]) ).
fof(f15076,plain,
( v3_struct_0(k11_conlat_1(sK74))
| ~ v10_lattices(k11_conlat_1(sK74))
| k6_lattices(k11_conlat_1(sK74)) = k15_lattice3(k11_conlat_1(sK74),u1_struct_0(k11_conlat_1(sK74)))
| ~ l3_lattices(k11_conlat_1(sK74))
| ~ spl609_41 ),
inference(resolution,[],[f9703,f14932]) ).
fof(f15077,plain,
( ~ v10_lattices(k11_conlat_1(sK74))
| k6_lattices(k11_conlat_1(sK74)) = k15_lattice3(k11_conlat_1(sK74),u1_struct_0(k11_conlat_1(sK74)))
| ~ l3_lattices(k11_conlat_1(sK74))
| spl609_12
| ~ spl609_41 ),
inference(forward_subsumption_resolution,[],[f15076,f14183]) ).
fof(f15081,plain,
( k6_lattices(k11_conlat_1(sK74)) = k15_lattice3(k11_conlat_1(sK74),u1_struct_0(k11_conlat_1(sK74)))
| ~ l3_lattices(k11_conlat_1(sK74))
| spl609_12
| ~ spl609_27
| ~ spl609_41 ),
inference(forward_subsumption_resolution,[],[f15077,f14380]) ).
fof(f15085,plain,
( k6_lattices(k11_conlat_1(sK74)) = k15_lattice3(k11_conlat_1(sK74),u1_struct_0(k11_conlat_1(sK74)))
| ~ spl609_11
| spl609_12
| ~ spl609_27
| ~ spl609_41 ),
inference(forward_subsumption_resolution,[],[f15081,f14179]) ).
fof(f15087,plain,
( k5_conlat_1(sK74) = k15_lattice3(k11_conlat_1(sK74),u1_struct_0(k11_conlat_1(sK74)))
| ~ spl609_11
| spl609_12
| ~ spl609_27
| ~ spl609_41 ),
inference(forward_demodulation,[],[f15085,f14122]) ).
fof(f15233,plain,
! [X2,X0,X1] :
( ~ m1_filter_0(X0,k11_conlat_1(X1))
| ~ m1_filter_0(X2,k11_conlat_1(X1))
| v3_struct_0(k11_conlat_1(X1))
| ~ v10_lattices(k11_conlat_1(X1))
| ~ l3_lattices(k11_conlat_1(X1))
| k3_conlat_2(X1,k5_subset_1(u1_struct_0(k11_conlat_1(X1)),X2,X0)) = k15_lattice3(k11_conlat_1(X1),k5_subset_1(u1_struct_0(k11_conlat_1(X1)),X2,X0))
| v3_conlat_1(X1)
| ~ l2_conlat_1(X1) ),
inference(resolution,[],[f11011,f14711]) ).
fof(f15237,plain,
! [X2,X0,X1] :
( ~ m1_filter_0(X0,k11_conlat_1(X1))
| ~ m1_filter_0(X2,k11_conlat_1(X1))
| v3_struct_0(k11_conlat_1(X1))
| ~ v10_lattices(k11_conlat_1(X1))
| k3_conlat_2(X1,k5_subset_1(u1_struct_0(k11_conlat_1(X1)),X2,X0)) = k15_lattice3(k11_conlat_1(X1),k5_subset_1(u1_struct_0(k11_conlat_1(X1)),X2,X0))
| v3_conlat_1(X1)
| ~ l2_conlat_1(X1) ),
inference(forward_subsumption_resolution,[],[f15233,f9213]) ).
fof(f15239,plain,
! [X2,X0,X1] :
( ~ m1_filter_0(X0,k11_conlat_1(X1))
| ~ m1_filter_0(X2,k11_conlat_1(X1))
| ~ v10_lattices(k11_conlat_1(X1))
| k3_conlat_2(X1,k5_subset_1(u1_struct_0(k11_conlat_1(X1)),X2,X0)) = k15_lattice3(k11_conlat_1(X1),k5_subset_1(u1_struct_0(k11_conlat_1(X1)),X2,X0))
| v3_conlat_1(X1)
| ~ l2_conlat_1(X1) ),
inference(forward_subsumption_resolution,[],[f15237,f9215]) ).
fof(f15241,plain,
! [X2,X0,X1] :
( ~ m1_filter_0(X2,k11_conlat_1(X1))
| ~ m1_filter_0(X0,k11_conlat_1(X1))
| k3_conlat_2(X1,k5_subset_1(u1_struct_0(k11_conlat_1(X1)),X2,X0)) = k15_lattice3(k11_conlat_1(X1),k5_subset_1(u1_struct_0(k11_conlat_1(X1)),X2,X0))
| v3_conlat_1(X1)
| ~ l2_conlat_1(X1) ),
inference(forward_subsumption_resolution,[],[f15239,f9214]) ).
fof(f15243,plain,
! [X0,X1] :
( ~ m1_filter_0(X0,k11_conlat_1(X1))
| k3_conlat_2(X1,k5_subset_1(u1_struct_0(k11_conlat_1(X1)),u1_struct_0(k11_conlat_1(X1)),X0)) = k15_lattice3(k11_conlat_1(X1),k5_subset_1(u1_struct_0(k11_conlat_1(X1)),u1_struct_0(k11_conlat_1(X1)),X0))
| v3_conlat_1(X1)
| ~ l2_conlat_1(X1)
| v3_struct_0(k11_conlat_1(X1))
| ~ v10_lattices(k11_conlat_1(X1))
| ~ l3_lattices(k11_conlat_1(X1)) ),
inference(resolution,[],[f15241,f12138]) ).
fof(f15246,plain,
! [X0,X1] :
( ~ m1_filter_0(X0,k11_conlat_1(X1))
| k3_conlat_2(X1,k5_subset_1(u1_struct_0(k11_conlat_1(X1)),u1_struct_0(k11_conlat_1(X1)),X0)) = k15_lattice3(k11_conlat_1(X1),k5_subset_1(u1_struct_0(k11_conlat_1(X1)),u1_struct_0(k11_conlat_1(X1)),X0))
| v3_conlat_1(X1)
| ~ l2_conlat_1(X1)
| v3_struct_0(k11_conlat_1(X1))
| ~ v10_lattices(k11_conlat_1(X1)) ),
inference(forward_subsumption_resolution,[],[f15243,f9213]) ).
fof(f15248,plain,
! [X0,X1] :
( ~ m1_filter_0(X0,k11_conlat_1(X1))
| k3_conlat_2(X1,k5_subset_1(u1_struct_0(k11_conlat_1(X1)),u1_struct_0(k11_conlat_1(X1)),X0)) = k15_lattice3(k11_conlat_1(X1),k5_subset_1(u1_struct_0(k11_conlat_1(X1)),u1_struct_0(k11_conlat_1(X1)),X0))
| v3_conlat_1(X1)
| ~ l2_conlat_1(X1)
| ~ v10_lattices(k11_conlat_1(X1)) ),
inference(forward_subsumption_resolution,[],[f15246,f9215]) ).
fof(f15250,plain,
! [X0,X1] :
( ~ m1_filter_0(X0,k11_conlat_1(X1))
| k3_conlat_2(X1,k5_subset_1(u1_struct_0(k11_conlat_1(X1)),u1_struct_0(k11_conlat_1(X1)),X0)) = k15_lattice3(k11_conlat_1(X1),k5_subset_1(u1_struct_0(k11_conlat_1(X1)),u1_struct_0(k11_conlat_1(X1)),X0))
| v3_conlat_1(X1)
| ~ l2_conlat_1(X1) ),
inference(forward_subsumption_resolution,[],[f15248,f9214]) ).
fof(f15251,plain,
! [X0] :
( k3_conlat_2(X0,k5_subset_1(u1_struct_0(k11_conlat_1(X0)),u1_struct_0(k11_conlat_1(X0)),u1_struct_0(k11_conlat_1(X0)))) = k15_lattice3(k11_conlat_1(X0),k5_subset_1(u1_struct_0(k11_conlat_1(X0)),u1_struct_0(k11_conlat_1(X0)),u1_struct_0(k11_conlat_1(X0))))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0)
| v3_struct_0(k11_conlat_1(X0))
| ~ v10_lattices(k11_conlat_1(X0))
| ~ l3_lattices(k11_conlat_1(X0)) ),
inference(resolution,[],[f15250,f12138]) ).
fof(f15254,plain,
! [X0] :
( k3_conlat_2(X0,k5_subset_1(u1_struct_0(k11_conlat_1(X0)),u1_struct_0(k11_conlat_1(X0)),u1_struct_0(k11_conlat_1(X0)))) = k15_lattice3(k11_conlat_1(X0),k5_subset_1(u1_struct_0(k11_conlat_1(X0)),u1_struct_0(k11_conlat_1(X0)),u1_struct_0(k11_conlat_1(X0))))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0)
| v3_struct_0(k11_conlat_1(X0))
| ~ v10_lattices(k11_conlat_1(X0)) ),
inference(forward_subsumption_resolution,[],[f15251,f9213]) ).
fof(f15256,plain,
! [X0] :
( k3_conlat_2(X0,k5_subset_1(u1_struct_0(k11_conlat_1(X0)),u1_struct_0(k11_conlat_1(X0)),u1_struct_0(k11_conlat_1(X0)))) = k15_lattice3(k11_conlat_1(X0),k5_subset_1(u1_struct_0(k11_conlat_1(X0)),u1_struct_0(k11_conlat_1(X0)),u1_struct_0(k11_conlat_1(X0))))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0)
| ~ v10_lattices(k11_conlat_1(X0)) ),
inference(forward_subsumption_resolution,[],[f15254,f9215]) ).
fof(f15258,plain,
! [X0] :
( ~ l2_conlat_1(X0)
| v3_conlat_1(X0)
| k3_conlat_2(X0,k5_subset_1(u1_struct_0(k11_conlat_1(X0)),u1_struct_0(k11_conlat_1(X0)),u1_struct_0(k11_conlat_1(X0)))) = k15_lattice3(k11_conlat_1(X0),k5_subset_1(u1_struct_0(k11_conlat_1(X0)),u1_struct_0(k11_conlat_1(X0)),u1_struct_0(k11_conlat_1(X0)))) ),
inference(forward_subsumption_resolution,[],[f15256,f9214]) ).
fof(f15259,plain,
( v3_conlat_1(sK74)
| k3_conlat_2(sK74,k5_subset_1(u1_struct_0(k11_conlat_1(sK74)),u1_struct_0(k11_conlat_1(sK74)),u1_struct_0(k11_conlat_1(sK74)))) = k15_lattice3(k11_conlat_1(sK74),k5_subset_1(u1_struct_0(k11_conlat_1(sK74)),u1_struct_0(k11_conlat_1(sK74)),u1_struct_0(k11_conlat_1(sK74)))) ),
inference(resolution,[],[f15258,f9165]) ).
fof(f15260,plain,
k3_conlat_2(sK74,k5_subset_1(u1_struct_0(k11_conlat_1(sK74)),u1_struct_0(k11_conlat_1(sK74)),u1_struct_0(k11_conlat_1(sK74)))) = k15_lattice3(k11_conlat_1(sK74),k5_subset_1(u1_struct_0(k11_conlat_1(sK74)),u1_struct_0(k11_conlat_1(sK74)),u1_struct_0(k11_conlat_1(sK74)))),
inference(forward_subsumption_resolution,[],[f15259,f9166]) ).
fof(f15556,plain,
! [X0] : k1_setfam_1(k2_tarski(X0,X0)) = k5_subset_1(X0,X0,X0),
inference(resolution,[],[f14616,f14063]) ).
fof(f15565,plain,
! [X0] : k5_subset_1(X0,X0,X0) = X0,
inference(forward_demodulation,[],[f15556,f13595]) ).
fof(f15757,plain,
! [X2,X0,X1] :
( v3_struct_0(X0)
| ~ l3_lattices(X0)
| ~ r1_tarski(X1,X2)
| ~ v10_lattices(X0)
| ~ v4_lattice3(X0)
| ~ r1_lattices(X0,k16_lattice3(X0,X1),k16_lattice3(X0,X2))
| k16_lattice3(X0,X2) = k16_lattice3(X0,X1)
| ~ m1_subset_1(k16_lattice3(X0,X2),u1_struct_0(X0))
| ~ m1_subset_1(k16_lattice3(X0,X1),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v4_lattices(X0)
| ~ l2_lattices(X0) ),
inference(resolution,[],[f14612,f9912]) ).
fof(f15762,plain,
! [X2,X0,X1] :
( v3_struct_0(X0)
| ~ l3_lattices(X0)
| ~ r1_tarski(X1,X2)
| ~ v10_lattices(X0)
| ~ v4_lattice3(X0)
| ~ r1_lattices(X0,k16_lattice3(X0,X1),k16_lattice3(X0,X2))
| k16_lattice3(X0,X2) = k16_lattice3(X0,X1)
| ~ m1_subset_1(k16_lattice3(X0,X2),u1_struct_0(X0))
| ~ m1_subset_1(k16_lattice3(X0,X1),u1_struct_0(X0))
| ~ v4_lattices(X0)
| ~ l2_lattices(X0) ),
inference(duplicate_literal_removal,[],[f15757]) ).
fof(f15769,plain,
! [X2,X0,X1] :
( v3_struct_0(X0)
| ~ l3_lattices(X0)
| ~ r1_tarski(X1,X2)
| ~ v10_lattices(X0)
| ~ v4_lattice3(X0)
| ~ r1_lattices(X0,k16_lattice3(X0,X1),k16_lattice3(X0,X2))
| k16_lattice3(X0,X2) = k16_lattice3(X0,X1)
| ~ m1_subset_1(k16_lattice3(X0,X2),u1_struct_0(X0))
| ~ m1_subset_1(k16_lattice3(X0,X1),u1_struct_0(X0))
| ~ l2_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f15762,f9931]) ).
fof(f15775,plain,
! [X2,X0,X1] :
( v3_struct_0(X0)
| ~ l3_lattices(X0)
| ~ r1_tarski(X1,X2)
| ~ v10_lattices(X0)
| ~ v4_lattice3(X0)
| ~ r1_lattices(X0,k16_lattice3(X0,X1),k16_lattice3(X0,X2))
| k16_lattice3(X0,X2) = k16_lattice3(X0,X1)
| ~ m1_subset_1(k16_lattice3(X0,X1),u1_struct_0(X0))
| ~ l2_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f15769,f9730]) ).
fof(f15781,plain,
! [X2,X0,X1] :
( v3_struct_0(X0)
| ~ l3_lattices(X0)
| ~ r1_tarski(X1,X2)
| ~ v10_lattices(X0)
| ~ v4_lattice3(X0)
| ~ r1_lattices(X0,k16_lattice3(X0,X1),k16_lattice3(X0,X2))
| k16_lattice3(X0,X2) = k16_lattice3(X0,X1)
| ~ l2_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f15775,f9730]) ).
fof(f15787,plain,
! [X2,X0,X1] :
( ~ r1_lattices(X0,k16_lattice3(X0,X1),k16_lattice3(X0,X2))
| ~ l3_lattices(X0)
| ~ r1_tarski(X1,X2)
| ~ v10_lattices(X0)
| ~ v4_lattice3(X0)
| v3_struct_0(X0)
| k16_lattice3(X0,X2) = k16_lattice3(X0,X1) ),
inference(forward_subsumption_resolution,[],[f15781,f12061]) ).
fof(f15791,plain,
( ! [X0] :
( ~ r1_lattices(k11_conlat_1(sK74),k6_conlat_1(sK74),k16_lattice3(k11_conlat_1(sK74),X0))
| ~ l3_lattices(k11_conlat_1(sK74))
| ~ r1_tarski(k2_tarski(k6_conlat_1(sK74),k6_conlat_1(sK74)),X0)
| ~ v10_lattices(k11_conlat_1(sK74))
| ~ v4_lattice3(k11_conlat_1(sK74))
| v3_struct_0(k11_conlat_1(sK74))
| k6_conlat_1(sK74) = k16_lattice3(k11_conlat_1(sK74),X0) )
| ~ spl609_42 ),
inference(superposition,[],[f15787,f14937]) ).
fof(f15800,plain,
( ! [X0] :
( ~ r1_lattices(k11_conlat_1(sK74),k6_conlat_1(sK74),k16_lattice3(k11_conlat_1(sK74),X0))
| ~ r1_tarski(k2_tarski(k6_conlat_1(sK74),k6_conlat_1(sK74)),X0)
| ~ v10_lattices(k11_conlat_1(sK74))
| ~ v4_lattice3(k11_conlat_1(sK74))
| v3_struct_0(k11_conlat_1(sK74))
| k6_conlat_1(sK74) = k16_lattice3(k11_conlat_1(sK74),X0) )
| ~ spl609_11
| ~ spl609_42 ),
inference(forward_subsumption_resolution,[],[f15791,f14179]) ).
fof(f15805,plain,
( ! [X0] :
( ~ r1_lattices(k11_conlat_1(sK74),k6_conlat_1(sK74),k16_lattice3(k11_conlat_1(sK74),X0))
| ~ r1_tarski(k2_tarski(k6_conlat_1(sK74),k6_conlat_1(sK74)),X0)
| ~ v4_lattice3(k11_conlat_1(sK74))
| v3_struct_0(k11_conlat_1(sK74))
| k6_conlat_1(sK74) = k16_lattice3(k11_conlat_1(sK74),X0) )
| ~ spl609_11
| ~ spl609_27
| ~ spl609_42 ),
inference(forward_subsumption_resolution,[],[f15800,f14380]) ).
fof(f15809,plain,
( ! [X0] :
( ~ r1_lattices(k11_conlat_1(sK74),k6_conlat_1(sK74),k16_lattice3(k11_conlat_1(sK74),X0))
| ~ r1_tarski(k2_tarski(k6_conlat_1(sK74),k6_conlat_1(sK74)),X0)
| v3_struct_0(k11_conlat_1(sK74))
| k6_conlat_1(sK74) = k16_lattice3(k11_conlat_1(sK74),X0) )
| ~ spl609_11
| ~ spl609_27
| ~ spl609_41
| ~ spl609_42 ),
inference(forward_subsumption_resolution,[],[f15805,f14932]) ).
fof(f15813,plain,
( ! [X0] :
( ~ r1_lattices(k11_conlat_1(sK74),k6_conlat_1(sK74),k16_lattice3(k11_conlat_1(sK74),X0))
| ~ r1_tarski(k2_tarski(k6_conlat_1(sK74),k6_conlat_1(sK74)),X0)
| k6_conlat_1(sK74) = k16_lattice3(k11_conlat_1(sK74),X0) )
| ~ spl609_11
| spl609_12
| ~ spl609_27
| ~ spl609_41
| ~ spl609_42 ),
inference(forward_subsumption_resolution,[],[f15809,f14183]) ).
fof(f16051,plain,
( m1_subset_1(k2_tarski(k6_conlat_1(sK74),k6_conlat_1(sK74)),k1_zfmisc_1(u1_struct_0(k11_conlat_1(sK74))))
| v3_struct_0(k11_conlat_1(sK74))
| ~ l1_struct_0(k11_conlat_1(sK74))
| ~ m1_subset_1(k6_conlat_1(sK74),u1_struct_0(k11_conlat_1(sK74)))
| ~ spl609_11
| spl609_12
| ~ spl609_25 ),
inference(superposition,[],[f11858,f14764]) ).
fof(f16052,plain,
( m1_subset_1(k2_tarski(k6_conlat_1(sK74),k6_conlat_1(sK74)),k1_zfmisc_1(u1_struct_0(k11_conlat_1(sK74))))
| ~ l1_struct_0(k11_conlat_1(sK74))
| ~ m1_subset_1(k6_conlat_1(sK74),u1_struct_0(k11_conlat_1(sK74)))
| ~ spl609_11
| spl609_12
| ~ spl609_25 ),
inference(forward_subsumption_resolution,[],[f16051,f14183]) ).
fof(f16060,plain,
( m1_subset_1(k2_tarski(k6_conlat_1(sK74),k6_conlat_1(sK74)),k1_zfmisc_1(u1_struct_0(k11_conlat_1(sK74))))
| ~ m1_subset_1(k6_conlat_1(sK74),u1_struct_0(k11_conlat_1(sK74)))
| ~ spl609_11
| spl609_12
| ~ spl609_25 ),
inference(forward_subsumption_resolution,[],[f16052,f14367]) ).
fof(f16068,plain,
( m1_subset_1(k2_tarski(k6_conlat_1(sK74),k6_conlat_1(sK74)),k1_zfmisc_1(u1_struct_0(k11_conlat_1(sK74))))
| ~ spl609_11
| spl609_12
| ~ spl609_25 ),
inference(forward_subsumption_resolution,[],[f16060,f14352]) ).
fof(f16078,definition,
( spl609_64
<=> m1_subset_1(k2_tarski(k6_conlat_1(sK74),k6_conlat_1(sK74)),k1_zfmisc_1(u1_struct_0(k11_conlat_1(sK74)))) ),
introduced(definition,[new_symbols(definition,[spl609_64])],[avatar_definition]) ).
fof(f16080,plain,
( m1_subset_1(k2_tarski(k6_conlat_1(sK74),k6_conlat_1(sK74)),k1_zfmisc_1(u1_struct_0(k11_conlat_1(sK74))))
| ~ spl609_64 ),
inference(avatar_component_clause,[],[f16078]) ).
fof(f16088,plain,
( spl609_64
| ~ spl609_11
| spl609_12
| ~ spl609_25 ),
inference(avatar_split_clause,[],[f16068,f14350,f14182,f14178,f16078]) ).
fof(f16102,plain,
( r1_tarski(k2_tarski(k6_conlat_1(sK74),k6_conlat_1(sK74)),u1_struct_0(k11_conlat_1(sK74)))
| ~ spl609_64 ),
inference(resolution,[],[f16080,f9432]) ).
fof(f16172,plain,
! [X0] :
( ~ m1_subset_1(k6_conlat_1(sK74),u1_struct_0(k11_conlat_1(sK74)))
| v3_struct_0(k11_conlat_1(sK74))
| ~ l3_lattices(k11_conlat_1(sK74))
| r1_lattices(k11_conlat_1(sK74),k6_conlat_1(sK74),X0)
| ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK74)))
| ~ v10_lattices(k11_conlat_1(sK74))
| ~ v13_lattices(k11_conlat_1(sK74)) ),
inference(superposition,[],[f14601,f14121]) ).
fof(f16175,plain,
( ! [X0] :
( v3_struct_0(k11_conlat_1(sK74))
| ~ l3_lattices(k11_conlat_1(sK74))
| r1_lattices(k11_conlat_1(sK74),k6_conlat_1(sK74),X0)
| ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK74)))
| ~ v10_lattices(k11_conlat_1(sK74))
| ~ v13_lattices(k11_conlat_1(sK74)) )
| ~ spl609_25 ),
inference(forward_subsumption_resolution,[],[f16172,f14352]) ).
fof(f16177,plain,
( ! [X0] :
( ~ l3_lattices(k11_conlat_1(sK74))
| r1_lattices(k11_conlat_1(sK74),k6_conlat_1(sK74),X0)
| ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK74)))
| ~ v10_lattices(k11_conlat_1(sK74))
| ~ v13_lattices(k11_conlat_1(sK74)) )
| spl609_12
| ~ spl609_25 ),
inference(forward_subsumption_resolution,[],[f16175,f14183]) ).
fof(f16178,plain,
( ! [X0] :
( r1_lattices(k11_conlat_1(sK74),k6_conlat_1(sK74),X0)
| ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK74)))
| ~ v10_lattices(k11_conlat_1(sK74))
| ~ v13_lattices(k11_conlat_1(sK74)) )
| ~ spl609_11
| spl609_12
| ~ spl609_25 ),
inference(forward_subsumption_resolution,[],[f16177,f14179]) ).
fof(f16179,plain,
( ! [X0] :
( r1_lattices(k11_conlat_1(sK74),k6_conlat_1(sK74),X0)
| ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK74)))
| ~ v13_lattices(k11_conlat_1(sK74)) )
| ~ spl609_11
| spl609_12
| ~ spl609_25
| ~ spl609_27 ),
inference(forward_subsumption_resolution,[],[f16178,f14380]) ).
fof(f16180,plain,
( ! [X0] :
( r1_lattices(k11_conlat_1(sK74),k6_conlat_1(sK74),X0)
| ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK74))) )
| ~ spl609_11
| spl609_12
| ~ spl609_25
| ~ spl609_27
| ~ spl609_29 ),
inference(forward_subsumption_resolution,[],[f16179,f14408]) ).
fof(f16181,plain,
( spl609_37
| ~ spl609_11
| spl609_12
| ~ spl609_25
| ~ spl609_27
| ~ spl609_29 ),
inference(avatar_split_clause,[],[f16180,f14407,f14379,f14350,f14182,f14178,f14594]) ).
fof(f16182,plain,
( ! [X0] :
( ~ m1_subset_1(k16_lattice3(k11_conlat_1(sK74),X0),u1_struct_0(k11_conlat_1(sK74)))
| ~ r1_tarski(k2_tarski(k6_conlat_1(sK74),k6_conlat_1(sK74)),X0)
| k6_conlat_1(sK74) = k16_lattice3(k11_conlat_1(sK74),X0) )
| ~ spl609_11
| spl609_12
| ~ spl609_27
| ~ spl609_37
| ~ spl609_41
| ~ spl609_42 ),
inference(resolution,[],[f14595,f15813]) ).
fof(f16211,plain,
( ! [X0] :
( ~ r1_tarski(k2_tarski(k6_conlat_1(sK74),k6_conlat_1(sK74)),X0)
| k6_conlat_1(sK74) = k16_lattice3(k11_conlat_1(sK74),X0)
| v3_struct_0(k11_conlat_1(sK74))
| ~ l3_lattices(k11_conlat_1(sK74)) )
| ~ spl609_11
| spl609_12
| ~ spl609_27
| ~ spl609_37
| ~ spl609_41
| ~ spl609_42 ),
inference(resolution,[],[f16182,f9730]) ).
fof(f16213,plain,
( ! [X0] :
( ~ r1_tarski(k2_tarski(k6_conlat_1(sK74),k6_conlat_1(sK74)),X0)
| k6_conlat_1(sK74) = k16_lattice3(k11_conlat_1(sK74),X0)
| ~ l3_lattices(k11_conlat_1(sK74)) )
| ~ spl609_11
| spl609_12
| ~ spl609_27
| ~ spl609_37
| ~ spl609_41
| ~ spl609_42 ),
inference(forward_subsumption_resolution,[],[f16211,f14183]) ).
fof(f16214,plain,
( ! [X0] :
( ~ r1_tarski(k2_tarski(k6_conlat_1(sK74),k6_conlat_1(sK74)),X0)
| k6_conlat_1(sK74) = k16_lattice3(k11_conlat_1(sK74),X0) )
| ~ spl609_11
| spl609_12
| ~ spl609_27
| ~ spl609_37
| ~ spl609_41
| ~ spl609_42 ),
inference(forward_subsumption_resolution,[],[f16213,f14179]) ).
fof(f16215,plain,
( k6_conlat_1(sK74) = k16_lattice3(k11_conlat_1(sK74),u1_struct_0(k11_conlat_1(sK74)))
| ~ spl609_11
| spl609_12
| ~ spl609_27
| ~ spl609_37
| ~ spl609_41
| ~ spl609_42
| ~ spl609_64 ),
inference(resolution,[],[f16214,f16102]) ).
fof(f17199,plain,
! [X0] :
( r1_lattices(k11_conlat_1(sK74),X0,k3_conlat_2(sK74,k5_subset_1(u1_struct_0(k11_conlat_1(sK74)),u1_struct_0(k11_conlat_1(sK74)),u1_struct_0(k11_conlat_1(sK74)))))
| v3_struct_0(k11_conlat_1(sK74))
| ~ l3_lattices(k11_conlat_1(sK74))
| ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK74)))
| ~ r2_hidden(X0,k5_subset_1(u1_struct_0(k11_conlat_1(sK74)),u1_struct_0(k11_conlat_1(sK74)),u1_struct_0(k11_conlat_1(sK74))))
| ~ v10_lattices(k11_conlat_1(sK74))
| ~ v4_lattice3(k11_conlat_1(sK74)) ),
inference(superposition,[],[f14611,f15260]) ).
fof(f17205,plain,
( ! [X0] :
( r1_lattices(k11_conlat_1(sK74),X0,k3_conlat_2(sK74,k5_subset_1(u1_struct_0(k11_conlat_1(sK74)),u1_struct_0(k11_conlat_1(sK74)),u1_struct_0(k11_conlat_1(sK74)))))
| ~ l3_lattices(k11_conlat_1(sK74))
| ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK74)))
| ~ r2_hidden(X0,k5_subset_1(u1_struct_0(k11_conlat_1(sK74)),u1_struct_0(k11_conlat_1(sK74)),u1_struct_0(k11_conlat_1(sK74))))
| ~ v10_lattices(k11_conlat_1(sK74))
| ~ v4_lattice3(k11_conlat_1(sK74)) )
| spl609_12 ),
inference(forward_subsumption_resolution,[],[f17199,f14183]) ).
fof(f17212,plain,
( ! [X0] :
( r1_lattices(k11_conlat_1(sK74),X0,k3_conlat_2(sK74,k5_subset_1(u1_struct_0(k11_conlat_1(sK74)),u1_struct_0(k11_conlat_1(sK74)),u1_struct_0(k11_conlat_1(sK74)))))
| ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK74)))
| ~ r2_hidden(X0,k5_subset_1(u1_struct_0(k11_conlat_1(sK74)),u1_struct_0(k11_conlat_1(sK74)),u1_struct_0(k11_conlat_1(sK74))))
| ~ v10_lattices(k11_conlat_1(sK74))
| ~ v4_lattice3(k11_conlat_1(sK74)) )
| ~ spl609_11
| spl609_12 ),
inference(forward_subsumption_resolution,[],[f17205,f14179]) ).
fof(f17219,plain,
( ! [X0] :
( r1_lattices(k11_conlat_1(sK74),X0,k3_conlat_2(sK74,k5_subset_1(u1_struct_0(k11_conlat_1(sK74)),u1_struct_0(k11_conlat_1(sK74)),u1_struct_0(k11_conlat_1(sK74)))))
| ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK74)))
| ~ r2_hidden(X0,k5_subset_1(u1_struct_0(k11_conlat_1(sK74)),u1_struct_0(k11_conlat_1(sK74)),u1_struct_0(k11_conlat_1(sK74))))
| ~ v4_lattice3(k11_conlat_1(sK74)) )
| ~ spl609_11
| spl609_12
| ~ spl609_27 ),
inference(forward_subsumption_resolution,[],[f17212,f14380]) ).
fof(f17226,plain,
( ! [X0] :
( r1_lattices(k11_conlat_1(sK74),X0,k3_conlat_2(sK74,k5_subset_1(u1_struct_0(k11_conlat_1(sK74)),u1_struct_0(k11_conlat_1(sK74)),u1_struct_0(k11_conlat_1(sK74)))))
| ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK74)))
| ~ r2_hidden(X0,k5_subset_1(u1_struct_0(k11_conlat_1(sK74)),u1_struct_0(k11_conlat_1(sK74)),u1_struct_0(k11_conlat_1(sK74)))) )
| ~ spl609_11
| spl609_12
| ~ spl609_27
| ~ spl609_41 ),
inference(forward_subsumption_resolution,[],[f17219,f14932]) ).
fof(f17231,plain,
( ! [X0] :
( r1_lattices(k11_conlat_1(sK74),X0,k3_conlat_2(sK74,u1_struct_0(k11_conlat_1(sK74))))
| ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK74)))
| ~ r2_hidden(X0,k5_subset_1(u1_struct_0(k11_conlat_1(sK74)),u1_struct_0(k11_conlat_1(sK74)),u1_struct_0(k11_conlat_1(sK74)))) )
| ~ spl609_11
| spl609_12
| ~ spl609_27
| ~ spl609_41 ),
inference(forward_demodulation,[],[f17226,f15565]) ).
fof(f17233,plain,
( ! [X0] :
( ~ r2_hidden(X0,u1_struct_0(k11_conlat_1(sK74)))
| r1_lattices(k11_conlat_1(sK74),X0,k3_conlat_2(sK74,u1_struct_0(k11_conlat_1(sK74))))
| ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK74))) )
| ~ spl609_11
| spl609_12
| ~ spl609_27
| ~ spl609_41 ),
inference(forward_demodulation,[],[f17231,f15565]) ).
fof(f17234,plain,
( ! [X0] :
( r1_lattices(k11_conlat_1(sK74),X0,k3_conlat_2(sK74,u1_struct_0(k11_conlat_1(sK74))))
| ~ r2_hidden(X0,u1_struct_0(k11_conlat_1(sK74))) )
| ~ spl609_11
| spl609_12
| ~ spl609_27
| ~ spl609_41 ),
inference(forward_subsumption_resolution,[],[f17233,f9288]) ).
fof(f17684,plain,
! [X2,X0,X1] :
( v3_struct_0(X0)
| ~ l3_lattices(X0)
| ~ r1_tarski(X1,X2)
| ~ v10_lattices(X0)
| ~ v4_lattice3(X0)
| ~ r1_lattices(X0,k15_lattice3(X0,X2),k15_lattice3(X0,X1))
| k15_lattice3(X0,X1) = k15_lattice3(X0,X2)
| ~ m1_subset_1(k15_lattice3(X0,X1),u1_struct_0(X0))
| ~ m1_subset_1(k15_lattice3(X0,X2),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ v4_lattices(X0)
| ~ l2_lattices(X0) ),
inference(resolution,[],[f14613,f9912]) ).
fof(f17695,plain,
! [X2,X0,X1] :
( v3_struct_0(X0)
| ~ l3_lattices(X0)
| ~ r1_tarski(X1,X2)
| ~ v10_lattices(X0)
| ~ v4_lattice3(X0)
| ~ r1_lattices(X0,k15_lattice3(X0,X2),k15_lattice3(X0,X1))
| k15_lattice3(X0,X1) = k15_lattice3(X0,X2)
| ~ m1_subset_1(k15_lattice3(X0,X1),u1_struct_0(X0))
| ~ m1_subset_1(k15_lattice3(X0,X2),u1_struct_0(X0))
| ~ v4_lattices(X0)
| ~ l2_lattices(X0) ),
inference(duplicate_literal_removal,[],[f17684]) ).
fof(f17709,plain,
! [X2,X0,X1] :
( v3_struct_0(X0)
| ~ l3_lattices(X0)
| ~ r1_tarski(X1,X2)
| ~ v10_lattices(X0)
| ~ v4_lattice3(X0)
| ~ r1_lattices(X0,k15_lattice3(X0,X2),k15_lattice3(X0,X1))
| k15_lattice3(X0,X1) = k15_lattice3(X0,X2)
| ~ m1_subset_1(k15_lattice3(X0,X1),u1_struct_0(X0))
| ~ m1_subset_1(k15_lattice3(X0,X2),u1_struct_0(X0))
| ~ l2_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f17695,f9931]) ).
fof(f17722,plain,
! [X2,X0,X1] :
( v3_struct_0(X0)
| ~ l3_lattices(X0)
| ~ r1_tarski(X1,X2)
| ~ v10_lattices(X0)
| ~ v4_lattice3(X0)
| ~ r1_lattices(X0,k15_lattice3(X0,X2),k15_lattice3(X0,X1))
| k15_lattice3(X0,X1) = k15_lattice3(X0,X2)
| ~ m1_subset_1(k15_lattice3(X0,X2),u1_struct_0(X0))
| ~ l2_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f17709,f9702]) ).
fof(f17734,plain,
! [X2,X0,X1] :
( v3_struct_0(X0)
| ~ l3_lattices(X0)
| ~ r1_tarski(X1,X2)
| ~ v10_lattices(X0)
| ~ v4_lattice3(X0)
| ~ r1_lattices(X0,k15_lattice3(X0,X2),k15_lattice3(X0,X1))
| k15_lattice3(X0,X1) = k15_lattice3(X0,X2)
| ~ l2_lattices(X0) ),
inference(forward_subsumption_resolution,[],[f17722,f9702]) ).
fof(f17746,plain,
! [X2,X0,X1] :
( ~ r1_lattices(X0,k15_lattice3(X0,X2),k15_lattice3(X0,X1))
| ~ l3_lattices(X0)
| ~ r1_tarski(X1,X2)
| ~ v10_lattices(X0)
| ~ v4_lattice3(X0)
| v3_struct_0(X0)
| k15_lattice3(X0,X1) = k15_lattice3(X0,X2) ),
inference(forward_subsumption_resolution,[],[f17734,f12061]) ).
fof(f17761,plain,
( ! [X0] :
( ~ r1_lattices(k11_conlat_1(sK74),k5_conlat_1(sK74),k15_lattice3(k11_conlat_1(sK74),X0))
| ~ l3_lattices(k11_conlat_1(sK74))
| ~ r1_tarski(X0,u1_struct_0(k11_conlat_1(sK74)))
| ~ v10_lattices(k11_conlat_1(sK74))
| ~ v4_lattice3(k11_conlat_1(sK74))
| v3_struct_0(k11_conlat_1(sK74))
| k5_conlat_1(sK74) = k15_lattice3(k11_conlat_1(sK74),X0) )
| ~ spl609_11
| spl609_12
| ~ spl609_27
| ~ spl609_41 ),
inference(superposition,[],[f17746,f15087]) ).
fof(f17774,plain,
( ! [X0] :
( ~ r1_lattices(k11_conlat_1(sK74),k5_conlat_1(sK74),k15_lattice3(k11_conlat_1(sK74),X0))
| ~ r1_tarski(X0,u1_struct_0(k11_conlat_1(sK74)))
| ~ v10_lattices(k11_conlat_1(sK74))
| ~ v4_lattice3(k11_conlat_1(sK74))
| v3_struct_0(k11_conlat_1(sK74))
| k5_conlat_1(sK74) = k15_lattice3(k11_conlat_1(sK74),X0) )
| ~ spl609_11
| spl609_12
| ~ spl609_27
| ~ spl609_41 ),
inference(forward_subsumption_resolution,[],[f17761,f14179]) ).
fof(f17784,plain,
( ! [X0] :
( ~ r1_lattices(k11_conlat_1(sK74),k5_conlat_1(sK74),k15_lattice3(k11_conlat_1(sK74),X0))
| ~ r1_tarski(X0,u1_struct_0(k11_conlat_1(sK74)))
| ~ v4_lattice3(k11_conlat_1(sK74))
| v3_struct_0(k11_conlat_1(sK74))
| k5_conlat_1(sK74) = k15_lattice3(k11_conlat_1(sK74),X0) )
| ~ spl609_11
| spl609_12
| ~ spl609_27
| ~ spl609_41 ),
inference(forward_subsumption_resolution,[],[f17774,f14380]) ).
fof(f17794,plain,
( ! [X0] :
( ~ r1_lattices(k11_conlat_1(sK74),k5_conlat_1(sK74),k15_lattice3(k11_conlat_1(sK74),X0))
| ~ r1_tarski(X0,u1_struct_0(k11_conlat_1(sK74)))
| v3_struct_0(k11_conlat_1(sK74))
| k5_conlat_1(sK74) = k15_lattice3(k11_conlat_1(sK74),X0) )
| ~ spl609_11
| spl609_12
| ~ spl609_27
| ~ spl609_41 ),
inference(forward_subsumption_resolution,[],[f17784,f14932]) ).
fof(f17804,plain,
( ! [X0] :
( ~ r1_lattices(k11_conlat_1(sK74),k5_conlat_1(sK74),k15_lattice3(k11_conlat_1(sK74),X0))
| ~ r1_tarski(X0,u1_struct_0(k11_conlat_1(sK74)))
| k5_conlat_1(sK74) = k15_lattice3(k11_conlat_1(sK74),X0) )
| ~ spl609_11
| spl609_12
| ~ spl609_27
| ~ spl609_41 ),
inference(forward_subsumption_resolution,[],[f17794,f14183]) ).
fof(f18301,plain,
( ~ r1_lattices(k11_conlat_1(sK74),k5_conlat_1(sK74),k3_conlat_2(sK74,k5_subset_1(u1_struct_0(k11_conlat_1(sK74)),u1_struct_0(k11_conlat_1(sK74)),u1_struct_0(k11_conlat_1(sK74)))))
| ~ r1_tarski(k5_subset_1(u1_struct_0(k11_conlat_1(sK74)),u1_struct_0(k11_conlat_1(sK74)),u1_struct_0(k11_conlat_1(sK74))),u1_struct_0(k11_conlat_1(sK74)))
| k5_conlat_1(sK74) = k3_conlat_2(sK74,k5_subset_1(u1_struct_0(k11_conlat_1(sK74)),u1_struct_0(k11_conlat_1(sK74)),u1_struct_0(k11_conlat_1(sK74))))
| ~ spl609_11
| spl609_12
| ~ spl609_27
| ~ spl609_41 ),
inference(superposition,[],[f17804,f15260]) ).
fof(f18302,plain,
( ~ r1_lattices(k11_conlat_1(sK74),k5_conlat_1(sK74),k3_conlat_2(sK74,u1_struct_0(k11_conlat_1(sK74))))
| ~ r1_tarski(k5_subset_1(u1_struct_0(k11_conlat_1(sK74)),u1_struct_0(k11_conlat_1(sK74)),u1_struct_0(k11_conlat_1(sK74))),u1_struct_0(k11_conlat_1(sK74)))
| k5_conlat_1(sK74) = k3_conlat_2(sK74,k5_subset_1(u1_struct_0(k11_conlat_1(sK74)),u1_struct_0(k11_conlat_1(sK74)),u1_struct_0(k11_conlat_1(sK74))))
| ~ spl609_11
| spl609_12
| ~ spl609_27
| ~ spl609_41 ),
inference(forward_demodulation,[],[f18301,f15565]) ).
fof(f18304,plain,
( ~ r1_tarski(u1_struct_0(k11_conlat_1(sK74)),u1_struct_0(k11_conlat_1(sK74)))
| ~ r1_lattices(k11_conlat_1(sK74),k5_conlat_1(sK74),k3_conlat_2(sK74,u1_struct_0(k11_conlat_1(sK74))))
| k5_conlat_1(sK74) = k3_conlat_2(sK74,k5_subset_1(u1_struct_0(k11_conlat_1(sK74)),u1_struct_0(k11_conlat_1(sK74)),u1_struct_0(k11_conlat_1(sK74))))
| ~ spl609_11
| spl609_12
| ~ spl609_27
| ~ spl609_41 ),
inference(forward_demodulation,[],[f18302,f15565]) ).
fof(f18306,plain,
( ~ r1_lattices(k11_conlat_1(sK74),k5_conlat_1(sK74),k3_conlat_2(sK74,u1_struct_0(k11_conlat_1(sK74))))
| k5_conlat_1(sK74) = k3_conlat_2(sK74,k5_subset_1(u1_struct_0(k11_conlat_1(sK74)),u1_struct_0(k11_conlat_1(sK74)),u1_struct_0(k11_conlat_1(sK74))))
| ~ spl609_11
| spl609_12
| ~ spl609_27
| ~ spl609_41 ),
inference(forward_subsumption_resolution,[],[f18304,f9629]) ).
fof(f18308,plain,
( k5_conlat_1(sK74) = k3_conlat_2(sK74,u1_struct_0(k11_conlat_1(sK74)))
| ~ r1_lattices(k11_conlat_1(sK74),k5_conlat_1(sK74),k3_conlat_2(sK74,u1_struct_0(k11_conlat_1(sK74))))
| ~ spl609_11
| spl609_12
| ~ spl609_27
| ~ spl609_41 ),
inference(forward_demodulation,[],[f18306,f15565]) ).
fof(f18311,definition,
( spl609_115
<=> r1_lattices(k11_conlat_1(sK74),k5_conlat_1(sK74),k3_conlat_2(sK74,u1_struct_0(k11_conlat_1(sK74)))) ),
introduced(definition,[new_symbols(definition,[spl609_115])],[avatar_definition]) ).
fof(f18313,plain,
( ~ r1_lattices(k11_conlat_1(sK74),k5_conlat_1(sK74),k3_conlat_2(sK74,u1_struct_0(k11_conlat_1(sK74))))
| spl609_115 ),
inference(avatar_component_clause,[],[f18311]) ).
fof(f18314,plain,
( ~ spl609_115
| spl609_9
| ~ spl609_11
| spl609_12
| ~ spl609_27
| ~ spl609_41 ),
inference(avatar_split_clause,[],[f18308,f14931,f14379,f14182,f14178,f14106,f18311]) ).
fof(f20141,plain,
! [X0] :
( ~ l1_struct_0(k11_conlat_1(X0))
| k16_lattice3(k11_conlat_1(X0),k2_pre_topc(k11_conlat_1(X0))) = k2_conlat_2(X0,k2_pre_topc(k11_conlat_1(X0)))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(resolution,[],[f10815,f9272]) ).
fof(f20173,plain,
! [X0] :
( ~ l2_conlat_1(X0)
| v3_conlat_1(X0)
| k16_lattice3(k11_conlat_1(X0),k2_pre_topc(k11_conlat_1(X0))) = k2_conlat_2(X0,k2_pre_topc(k11_conlat_1(X0))) ),
inference(forward_subsumption_resolution,[],[f20141,f14368]) ).
fof(f20180,plain,
( v3_conlat_1(sK74)
| k2_conlat_2(sK74,k2_pre_topc(k11_conlat_1(sK74))) = k16_lattice3(k11_conlat_1(sK74),k2_pre_topc(k11_conlat_1(sK74))) ),
inference(resolution,[],[f20173,f9165]) ).
fof(f20181,plain,
k2_conlat_2(sK74,k2_pre_topc(k11_conlat_1(sK74))) = k16_lattice3(k11_conlat_1(sK74),k2_pre_topc(k11_conlat_1(sK74))),
inference(forward_subsumption_resolution,[],[f20180,f9166]) ).
fof(f20182,plain,
( k2_conlat_2(sK74,u1_struct_0(k11_conlat_1(sK74))) = k16_lattice3(k11_conlat_1(sK74),u1_struct_0(k11_conlat_1(sK74)))
| ~ spl609_11 ),
inference(forward_demodulation,[],[f20181,f14370]) ).
fof(f20183,plain,
( k6_conlat_1(sK74) = k2_conlat_2(sK74,u1_struct_0(k11_conlat_1(sK74)))
| ~ spl609_11
| spl609_12
| ~ spl609_27
| ~ spl609_37
| ~ spl609_41
| ~ spl609_42
| ~ spl609_64 ),
inference(forward_demodulation,[],[f20182,f16215]) ).
fof(f20184,plain,
( $false
| spl609_10
| ~ spl609_11
| spl609_12
| ~ spl609_27
| ~ spl609_37
| ~ spl609_41
| ~ spl609_42
| ~ spl609_64 ),
inference(forward_subsumption_resolution,[],[f20183,f14112]) ).
fof(f20185,plain,
( spl609_10
| ~ spl609_11
| spl609_12
| ~ spl609_27
| ~ spl609_37
| ~ spl609_41
| ~ spl609_42
| ~ spl609_64 ),
inference(avatar_contradiction_clause,[],[f20184]) ).
fof(f20214,plain,
( ~ r2_hidden(k5_conlat_1(sK74),u1_struct_0(k11_conlat_1(sK74)))
| ~ spl609_11
| spl609_12
| ~ spl609_27
| ~ spl609_41
| spl609_115 ),
inference(resolution,[],[f18313,f17234]) ).
fof(f20215,plain,
( $false
| ~ spl609_11
| spl609_12
| ~ spl609_27
| ~ spl609_33
| ~ spl609_41
| spl609_115 ),
inference(forward_subsumption_resolution,[],[f20214,f14504]) ).
fof(f20216,plain,
( ~ spl609_11
| spl609_12
| ~ spl609_27
| ~ spl609_33
| ~ spl609_41
| spl609_115 ),
inference(avatar_contradiction_clause,[],[f20215]) ).
cnf(s8,plain,
( ~ spl609_9
| ~ spl609_10 ),
inference(sat_conversion,[],[f14113]) ).
cnf(s11,plain,
spl609_11,
inference(sat_conversion,[],[f14192]) ).
cnf(s12,plain,
~ spl609_12,
inference(sat_conversion,[],[f14196]) ).
cnf(s18,plain,
( spl609_12
| ~ spl609_24
| spl609_25 ),
inference(sat_conversion,[],[f14353]) ).
cnf(s24,plain,
spl609_27,
inference(sat_conversion,[],[f14401]) ).
cnf(s26,plain,
spl609_29,
inference(sat_conversion,[],[f14416]) ).
cnf(s28,plain,
( ~ spl609_11
| spl609_12
| spl609_16
| spl609_33 ),
inference(sat_conversion,[],[f14505]) ).
cnf(s29,plain,
( ~ spl609_11
| spl609_12
| ~ spl609_16 ),
inference(sat_conversion,[],[f14541]) ).
cnf(s32,plain,
( ~ spl609_11
| spl609_24 ),
inference(sat_conversion,[],[f14748]) ).
cnf(s35,plain,
( ~ spl609_11
| spl609_12
| ~ spl609_25
| ~ spl609_27
| ~ spl609_41
| spl609_42 ),
inference(sat_conversion,[],[f14938]) ).
cnf(s39,plain,
spl609_41,
inference(sat_conversion,[],[f14953]) ).
cnf(s55,plain,
( ~ spl609_11
| spl609_12
| ~ spl609_25
| spl609_64 ),
inference(sat_conversion,[],[f16088]) ).
cnf(s58,plain,
( ~ spl609_11
| spl609_12
| ~ spl609_25
| ~ spl609_27
| ~ spl609_29
| spl609_37 ),
inference(sat_conversion,[],[f16181]) ).
cnf(s106,plain,
( spl609_9
| ~ spl609_11
| spl609_12
| ~ spl609_27
| ~ spl609_41
| ~ spl609_115 ),
inference(sat_conversion,[],[f18314]) ).
cnf(s177,plain,
( spl609_10
| ~ spl609_11
| spl609_12
| ~ spl609_27
| ~ spl609_37
| ~ spl609_41
| ~ spl609_42
| ~ spl609_64 ),
inference(sat_conversion,[],[f20185]) ).
cnf(s180,plain,
( ~ spl609_11
| spl609_12
| ~ spl609_27
| ~ spl609_33
| ~ spl609_41
| spl609_115 ),
inference(sat_conversion,[],[f20216]) ).
cnf(s185,plain,
( ~ spl609_11
| spl609_12
| ~ spl609_25
| ~ spl609_27
| spl609_42 ),
inference(rat,[],[s35,s39]) ).
cnf(s194,plain,
spl609_24,
inference(rat,[],[s32,s11]) ).
cnf(s195,plain,
~ spl609_16,
inference(rat,[],[s29,s12,s11]) ).
cnf(s199,plain,
spl609_25,
inference(rat,[],[s18,s12,s194]) ).
cnf(s200,plain,
spl609_33,
inference(rat,[],[s28,s11,s12,s195]) ).
cnf(s202,plain,
spl609_37,
inference(rat,[],[s58,s11,s26,s24,s12,s199]) ).
cnf(s203,plain,
spl609_64,
inference(rat,[],[s55,s11,s12,s199]) ).
cnf(s204,plain,
spl609_42,
inference(rat,[],[s185,s11,s24,s12,s199]) ).
cnf(s205,plain,
spl609_115,
inference(rat,[],[s180,s11,s39,s12,s24,s200]) ).
cnf(s208,plain,
spl609_10,
inference(rat,[],[s177,s203,s204,s39,s11,s24,s12,s202]) ).
cnf(s211,plain,
spl609_9,
inference(rat,[],[s106,s11,s39,s24,s12,s205]) ).
cnf(s216,plain,
$false,
inference(rat,[],[s8,s208,s211]) ).
fof(f20217,plain,
$false,
inference(avatar_sat_refutation,[],[s216]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT340+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.38 % Computer : n011.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Sun Sep 27 14:48:16 UTC 2026
% 0.10/0.39 % CPUTime :
% 0.10/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.42 Running first-order theorem proving
% 0.10/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 11.83/2.85 % (2505076)Detected formulas, will run a generic FOF schedule.
% 11.83/2.85 % (2505085)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=391484874:i=119:av=off:ss=axioms_2997 on theBenchmark for (2997ds/119Mi)
% 11.83/2.85 % (2505084)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=937923301:i=109:sd=1:ins=1:gsp=on:ss=axioms_2997 on theBenchmark for (2997ds/109Mi)
% 11.83/2.85 % (2505086)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3285877738:s2a=on:i=139:gtg=position_2997 on theBenchmark for (2997ds/139Mi)
% 11.83/2.85 % (2505082)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=3187456196:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2997 on theBenchmark for (2997ds/134677Mi)
% 11.83/2.85 % (2505083)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=334497197:i=141695:sd=1:nm=32:gsp=on:ss=included_2997 on theBenchmark for (2997ds/141695Mi)
% 11.83/2.85 % (2505081)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=3731345945:i=141193_2997 on theBenchmark for (2997ds/141193Mi)
% 11.83/2.85 % (2505085)Instruction limit reached!
% 11.83/2.85 % (2505085)------------------------------
% 11.83/2.85 % (2505085)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.83/2.85 % (2505085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.83/2.85 % (2505085)CaDiCaL version: 2.1.3
% 11.83/2.85 % (2505085)Termination reason: Instruction limit
% 11.83/2.85 % (2505085)Termination phase: Property scanning
% 11.83/2.85 % (2505085)Time elapsed: 0.045 s
% 11.83/2.85 % (2505085)Peak memory usage: 95 MB
% 11.83/2.85 % (2505085)Instructions burned: 122 (million)
% 11.83/2.85 % (2505087)dis-21_1_sil=8000:lcm=predicate:random_seed=1247207883:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2997 on theBenchmark for (2997ds/129Mi)
% 11.83/2.85 % (2505084)Refutation not found, incomplete strategy
% 11.83/2.85 % (2505084)------------------------------
% 11.83/2.85 % (2505084)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.83/2.85 % (2505084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.83/2.85 % (2505084)CaDiCaL version: 2.1.3
% 11.83/2.85 % (2505084)Termination reason: Refutation not found, incomplete strategy
% 11.83/2.85 % (2505084)Time elapsed: 0.025 s
% 11.83/2.85 % (2505084)Peak memory usage: 95 MB
% 11.83/2.85 % (2505084)Instructions burned: 29 (million)
% 11.83/2.85 % (2505086)Instruction limit reached!
% 11.83/2.85 % (2505086)------------------------------
% 11.83/2.85 % (2505086)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.83/2.85 % (2505086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.83/2.85 % (2505086)CaDiCaL version: 2.1.3
% 11.83/2.85 % (2505086)Termination reason: Instruction limit
% 11.83/2.85 % (2505086)Termination phase: Preprocessing 2
% 11.83/2.85 % (2505086)Time elapsed: 0.086 s
% 11.83/2.85 % (2505086)Peak memory usage: 93 MB
% 11.83/2.85 % (2505086)Instructions burned: 140 (million)
% 11.83/2.85 % (2505087)Instruction limit reached!
% 11.83/2.85 % (2505087)------------------------------
% 11.83/2.85 % (2505087)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.83/2.85 % (2505087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.83/2.85 % (2505087)CaDiCaL version: 2.1.3
% 11.83/2.85 % (2505087)Termination reason: Instruction limit
% 11.83/2.85 % (2505087)Termination phase: Preprocessing 3
% 11.83/2.85 % (2505087)Time elapsed: 0.099 s
% 11.83/2.85 % (2505087)Peak memory usage: 96 MB
% 11.83/2.85 % (2505087)Instructions burned: 130 (million)
% 11.83/2.85 % (2505094)lrs+10_1_sil=8000:sp=occurrence:random_seed=1662086515:i=285:sd=3:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/285Mi)
% 11.83/2.85 % (2505094)Instruction limit reached!
% 11.83/2.85 % (2505094)------------------------------
% 11.83/2.85 % (2505094)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.83/2.85 % (2505094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.83/2.85 % (2505094)CaDiCaL version: 2.1.3
% 11.83/2.85 % (2505094)Termination reason: Instruction limit
% 11.83/2.85 % (2505094)Termination phase: Saturation
% 11.83/2.85 % (2505094)Time elapsed: 0.103 s
% 11.83/2.85 % (2505094)Peak memory usage: 99 MB
% 11.83/2.85 % (2505094)Instructions burned: 287 (million)
% 20.05/3.92 % (2505096)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3094318351:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/157Mi)
% 20.05/3.92 % (2505084)------------------------------
% 20.05/3.92 % (2505084)------------------------------
% 20.05/3.92 % (2505097)lrs+1011_1_sil=32000:sp=occurrence:random_seed=932575741:i=325:sd=1:ss=axioms:sgt=32_2994 on theBenchmark for (2994ds/325Mi)
% 20.05/3.92 % (2505096)Refutation not found, incomplete strategy
% 20.05/3.92 % (2505096)------------------------------
% 20.05/3.92 % (2505096)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.05/3.92 % (2505096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.05/3.92 % (2505096)CaDiCaL version: 2.1.3
% 20.05/3.92 % (2505096)Termination reason: Refutation not found, incomplete strategy
% 20.05/3.92 % (2505096)Time elapsed: 0.051 s
% 20.05/3.92 % (2505096)Peak memory usage: 95 MB
% 20.05/3.92 % (2505096)Instructions burned: 88 (million)
% 20.05/3.92 % (2505099)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=2396523239:s2a=on:i=248:s2at=1.23:gtg=position_2993 on theBenchmark for (2993ds/248Mi)
% 20.05/3.92 % (2505102)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=903841434:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2993 on theBenchmark for (2993ds/294Mi)
% 20.05/3.92 % (2505099)Instruction limit reached!
% 20.05/3.92 % (2505099)------------------------------
% 20.05/3.92 % (2505099)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.05/3.92 % (2505099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.05/3.92 % (2505099)CaDiCaL version: 2.1.3
% 20.05/3.92 % (2505099)Termination reason: Instruction limit
% 20.05/3.92 % (2505099)Termination phase: Preprocessing 3
% 20.05/3.92 % (2505099)Time elapsed: 0.087 s
% 20.05/3.92 % (2505099)Peak memory usage: 100 MB
% 20.05/3.92 % (2505099)Instructions burned: 248 (million)
% 20.05/3.92 % (2505097)Instruction limit reached!
% 20.05/3.92 % (2505097)------------------------------
% 20.05/3.92 % (2505097)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.05/3.92 % (2505097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.05/3.92 % (2505097)CaDiCaL version: 2.1.3
% 20.05/3.92 % (2505097)Termination reason: Instruction limit
% 20.05/3.92 % (2505097)Termination phase: Saturation
% 20.05/3.92 % (2505097)Time elapsed: 0.181 s
% 20.05/3.92 % (2505097)Peak memory usage: 98 MB
% 20.05/3.92 % (2505097)Instructions burned: 325 (million)
% 20.05/3.92 % (2505096)------------------------------
% 20.05/3.92 % (2505096)------------------------------
% 20.05/3.92 % (2505105)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3564662078:i=2350_2991 on theBenchmark for (2991ds/2350Mi)
% 20.05/3.92 % (2505102)Instruction limit reached!
% 20.05/3.92 % (2505102)------------------------------
% 20.05/3.92 % (2505102)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.05/3.92 % (2505102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.05/3.92 % (2505102)CaDiCaL version: 2.1.3
% 20.05/3.92 % (2505102)Termination reason: Instruction limit
% 20.05/3.92 % (2505102)Termination phase: Saturation
% 20.05/3.92 % (2505102)Time elapsed: 0.175 s
% 20.05/3.92 % (2505102)Peak memory usage: 97 MB
% 20.05/3.92 % (2505102)Instructions burned: 295 (million)
% 20.05/3.92 % (2505106)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2384153526:cts=off:i=113:fsr=off:ss=included:sgt=4_2991 on theBenchmark for (2991ds/113Mi)
% 20.05/3.92 % (2505106)Instruction limit reached!
% 20.05/3.92 % (2505106)------------------------------
% 20.05/3.92 % (2505106)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.05/3.92 % (2505106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.05/3.92 % (2505106)CaDiCaL version: 2.1.3
% 20.05/3.92 % (2505106)Termination reason: Instruction limit
% 20.05/3.92 % (2505106)Termination phase: Property scanning
% 20.05/3.92 % (2505106)Time elapsed: 0.075 s
% 20.05/3.92 % (2505106)Peak memory usage: 95 MB
% 20.05/3.92 % (2505106)Instructions burned: 115 (million)
% 20.05/3.92 % (2505108)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2822956289:i=127:av=off:fsr=off:sup=off_2990 on theBenchmark for (2990ds/127Mi)
% 20.05/3.92 % (2505109)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1745809422:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2989 on theBenchmark for (2989ds/114Mi)
% 20.05/3.92 % (2505108)Instruction limit reached!
% 11.21/4.32 % (2505108)------------------------------
% 11.21/4.32 % (2505108)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.21/4.32 % (2505108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.21/4.32 % (2505108)CaDiCaL version: 2.1.3
% 11.21/4.32 % (2505108)Termination reason: Instruction limit
% 11.21/4.32 % (2505108)Termination phase: Preprocessing 3
% 11.21/4.32 % (2505108)Time elapsed: 0.090 s
% 11.21/4.32 % (2505108)Peak memory usage: 99 MB
% 11.21/4.32 % (2505108)Instructions burned: 127 (million)
% 11.21/4.32 % (2505109)Instruction limit reached!
% 11.21/4.32 % (2505109)------------------------------
% 11.21/4.32 % (2505109)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.21/4.32 % (2505109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.21/4.32 % (2505109)CaDiCaL version: 2.1.3
% 11.21/4.32 % (2505109)Termination reason: Instruction limit
% 11.21/4.32 % (2505109)Termination phase: Property scanning
% 11.21/4.32 % (2505109)Time elapsed: 0.050 s
% 11.21/4.32 % (2505109)Peak memory usage: 91 MB
% 11.21/4.32 % (2505109)Instructions burned: 114 (million)
% 11.21/4.32 % (2505111)lrs+10_1_sil=8000:sp=occurrence:random_seed=3083791492:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2989 on theBenchmark for (2989ds/907Mi)
% 11.21/4.32 % (2505114)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2927048373:i=437:sd=1:aac=none:ss=included_2988 on theBenchmark for (2988ds/437Mi)
% 11.21/4.32 % (2505115)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=4190711948:i=5202:ss=axioms:sgt=16_2987 on theBenchmark for (2987ds/5202Mi)
% 11.21/4.32 % (2505114)Refutation not found, incomplete strategy
% 11.21/4.32 % (2505114)------------------------------
% 11.21/4.32 % (2505114)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.21/4.32 % (2505114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.21/4.32 % (2505114)CaDiCaL version: 2.1.3
% 11.21/4.32 % (2505114)Termination reason: Refutation not found, incomplete strategy
% 11.21/4.32 % (2505114)Time elapsed: 0.034 s
% 11.21/4.32 % (2505114)Peak memory usage: 95 MB
% 11.21/4.32 % (2505114)Instructions burned: 43 (million)
% 11.21/4.32 % (2505114)------------------------------
% 11.21/4.32 % (2505114)------------------------------
% 11.21/4.32 % (2505111)Instruction limit reached!
% 11.21/4.32 % (2505111)------------------------------
% 11.21/4.32 % (2505111)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.21/4.32 % (2505111)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.21/4.32 % (2505111)CaDiCaL version: 2.1.3
% 11.21/4.32 % (2505111)Termination reason: Instruction limit
% 11.21/4.32 % (2505111)Termination phase: Saturation
% 11.21/4.32 % (2505111)Time elapsed: 0.515 s
% 11.21/4.32 % (2505111)Peak memory usage: 110 MB
% 11.21/4.32 % (2505111)Instructions burned: 907 (million)
% 11.21/4.32 % (2505119)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=562710245:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2983 on theBenchmark for (2983ds/134Mi)
% 11.21/4.32 % (2505105)Instruction limit reached!
% 11.21/4.32 % (2505105)------------------------------
% 11.21/4.32 % (2505105)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.21/4.32 % (2505105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.21/4.32 % (2505105)CaDiCaL version: 2.1.3
% 11.21/4.32 % (2505105)Termination reason: Instruction limit
% 11.21/4.32 % (2505105)Termination phase: Saturation
% 11.21/4.32 % (2505105)Time elapsed: 0.912 s
% 11.21/4.32 % (2505105)Peak memory usage: 211 MB
% 11.21/4.32 % (2505105)Instructions burned: 2350 (million)
% 11.21/4.32 % (2505119)Instruction limit reached!
% 11.21/4.32 % (2505119)------------------------------
% 11.21/4.32 % (2505119)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.21/4.32 % (2505119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.21/4.32 % (2505119)CaDiCaL version: 2.1.3
% 11.21/4.32 % (2505119)Termination reason: Instruction limit
% 11.21/4.32 % (2505119)Termination phase: Saturation
% 11.21/4.32 % (2505119)Time elapsed: 0.088 s
% 11.21/4.32 % (2505119)Peak memory usage: 97 MB
% 11.21/4.32 % (2505119)Instructions burned: 135 (million)
% 11.21/4.32 % (2505120)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2706844020:st=8:i=592:sd=3:ep=RST:ss=axioms_2982 on theBenchmark for (2982ds/592Mi)
% 11.21/4.32 % (2505122)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1912949029:st=3:i=13193:sd=3:ss=axioms_2981 on theBenchmark for (2981ds/13193Mi)
% 11.21/4.32 % (2505124)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=943421143:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2980 on theBenchmark for (2980ds/125Mi)
% 11.21/4.32 % (2505124)Instruction limit reached!
% 11.21/4.32 % (2505124)------------------------------
% 11.21/4.32 % (2505124)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.21/4.32 % (2505124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.21/4.32 % (2505124)CaDiCaL version: 2.1.3
% 11.21/4.32 % (2505124)Termination reason: Instruction limit
% 11.21/4.32 % (2505124)Termination phase: Preprocessing 2
% 11.21/4.32 % (2505124)Time elapsed: 0.081 s
% 11.21/4.32 % (2505124)Peak memory usage: 92 MB
% 11.21/4.32 % (2505124)Instructions burned: 125 (million)
% 11.21/4.32 % (2505120)Instruction limit reached!
% 11.21/4.32 % (2505120)------------------------------
% 11.21/4.32 % (2505120)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.21/4.32 % (2505120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.21/4.32 % (2505120)CaDiCaL version: 2.1.3
% 11.21/4.32 % (2505120)Termination reason: Instruction limit
% 11.21/4.32 % (2505120)Termination phase: Saturation
% 11.21/4.32 % (2505120)Time elapsed: 0.313 s
% 11.21/4.32 % (2505120)Peak memory usage: 107 MB
% 11.21/4.32 % (2505120)Instructions burned: 594 (million)
% 11.21/4.32 % (2505127)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=730426608:i=134:gtgl=5:slsql=off:gtg=exists_sym_2977 on theBenchmark for (2977ds/134Mi)
% 11.21/4.32 % (2505128)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2837758125:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2977 on theBenchmark for (2977ds/141Mi)
% 11.21/4.32 % (2505128)Refutation not found, incomplete strategy
% 11.21/4.32 % (2505128)------------------------------
% 11.21/4.32 % (2505128)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.21/4.32 % (2505128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.21/4.32 % (2505128)CaDiCaL version: 2.1.3
% 11.21/4.32 % (2505128)Termination reason: Refutation not found, incomplete strategy
% 11.21/4.32 % (2505128)Time elapsed: 0.023 s
% 11.21/4.32 % (2505128)Peak memory usage: 95 MB
% 11.21/4.32 % (2505128)Instructions burned: 27 (million)
% 11.21/4.32 % (2505127)Instruction limit reached!
% 11.21/4.32 % (2505127)------------------------------
% 11.21/4.32 % (2505127)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.21/4.32 % (2505127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.21/4.32 % (2505127)CaDiCaL version: 2.1.3
% 11.21/4.32 % (2505127)Termination reason: Instruction limit
% 11.21/4.32 % (2505127)Termination phase: SInE selection
% 11.21/4.32 % (2505127)Time elapsed: 0.061 s
% 11.21/4.32 % (2505127)Peak memory usage: 91 MB
% 11.21/4.32 % (2505127)Instructions burned: 134 (million)
% 11.21/4.32 % (2505131)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3154073534:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2975 on theBenchmark for (2975ds/431Mi)
% 11.21/4.32 % (2505131)Refutation not found, incomplete strategy
% 11.21/4.32 % (2505131)------------------------------
% 11.21/4.32 % (2505131)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.21/4.32 % (2505131)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.21/4.32 % (2505131)CaDiCaL version: 2.1.3
% 11.21/4.32 % (2505131)Termination reason: Refutation not found, incomplete strategy
% 11.21/4.32 % (2505131)Time elapsed: 0.027 s
% 11.21/4.32 % (2505131)Peak memory usage: 95 MB
% 11.21/4.32 % (2505131)Instructions burned: 31 (million)
% 11.21/4.32 % (2505128)------------------------------
% 11.21/4.32 % (2505128)------------------------------
% 11.21/4.32 % (2505133)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=3793298793:i=6060:aac=none:ins=25_2973 on theBenchmark for (2973ds/6060Mi)
% 11.21/4.32 % (2505131)------------------------------
% 11.21/4.32 % (2505131)------------------------------
% 11.21/4.32 % (2505135)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=2207560146:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2971 on theBenchmark for (2971ds/150Mi)
% 11.21/4.32 % (2505135)Instruction limit reached!
% 11.21/4.32 % (2505135)------------------------------
% 11.21/4.32 % (2505135)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.21/4.32 % (2505135)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.21/4.32 % (2505135)CaDiCaL version: 2.1.3
% 11.21/4.32 % (2505135)Termination reason: Instruction limit
% 11.21/4.32 % (2505135)Termination phase: Preprocessing 3
% 11.21/4.32 % (2505135)Time elapsed: 0.106 s
% 11.21/4.32 % (2505135)Peak memory usage: 99 MB
% 11.21/4.32 % (2505135)Instructions burned: 150 (million)
% 11.21/4.32 % (2505122)First to succeed.
% 11.21/4.32 % (2505122)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2505076"
% 11.21/4.32 % (2505137)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1135205161:i=14155:bd=all_2968 on theBenchmark for (2968ds/14155Mi)
% 11.21/4.32 % (2505122)Refutation found. Thanks to Tanya!
% 11.21/4.32 % SZS status Theorem for theBenchmark
% 11.21/4.32 % SZS output start Proof for theBenchmark
% See solution above
% 23.66/4.52 % (2505122)------------------------------
% 23.66/4.52 % (2505122)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.66/4.52 % (2505122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.66/4.52 % (2505122)CaDiCaL version: 2.1.3
% 23.66/4.52 % (2505122)Termination reason: Refutation
% 23.66/4.52 % (2505122)Time elapsed: 1.275 s
% 23.66/4.52 % (2505122)Peak memory usage: 190 MB
% 23.66/4.52 % (2505122)Instructions burned: 3645 (million)
% 23.66/4.52 % (2505122)------------------------------
% 23.66/4.52 % (2505122)------------------------------
% 23.66/4.52 % (2505076)Success in time 3.461 s
% 23.66/4.52 % Vampire exiting
%------------------------------------------------------------------------------