%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LAT338+2 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n003.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 : Thu Sep 24 01:02:49 PM UTC 2026
% Result : Theorem 242.11s 31.62s
% Output : CNFRefutation 242.85s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 84
% Syntax : Number of formulae : 328 ( 86 unt; 53 def)
% Number of atoms : 1065 ( 32 equ)
% Maximal formula atoms : 16 ( 3 avg)
% Number of connectives : 1021 ( 284 ~; 274 |; 399 &)
% ( 53 <=>; 11 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 91 ( 89 usr; 54 prp; 0-2 aty)
% Number of functors : 32 ( 32 usr; 25 con; 0-2 aty)
% Number of variables : 93 ( 73 !; 20 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f26,axiom,
? [A] : ~ v1_xboole_0(A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f466,axiom,
! [A] : m1_subset_1(k8_subset_1(A),A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2450,axiom,
k3_numbers != k1_numbers,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2451,axiom,
k3_numbers != k2_numbers,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2457,axiom,
k5_numbers != k1_numbers,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2458,axiom,
k5_numbers != k2_numbers,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2464,axiom,
k5_numbers = k5_ordinal2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3601,axiom,
? [A] :
( v3_lattices(A)
& ~ v3_struct_0(A)
& l3_lattices(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3606,axiom,
? [A] :
( v10_lattices(A)
& v9_lattices(A)
& v8_lattices(A)
& v7_lattices(A)
& v6_lattices(A)
& v5_lattices(A)
& v4_lattices(A)
& v3_lattices(A)
& ~ v3_struct_0(A)
& l3_lattices(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3607,axiom,
? [A] :
( v14_lattices(A)
& v13_lattices(A)
& v12_lattices(A)
& v11_lattices(A)
& v10_lattices(A)
& v9_lattices(A)
& v8_lattices(A)
& v7_lattices(A)
& v6_lattices(A)
& v5_lattices(A)
& v4_lattices(A)
& v3_lattices(A)
& ~ v3_struct_0(A)
& l3_lattices(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3610,axiom,
? [A] :
( v15_lattices(A)
& v14_lattices(A)
& v13_lattices(A)
& v10_lattices(A)
& v9_lattices(A)
& v8_lattices(A)
& v7_lattices(A)
& v6_lattices(A)
& v5_lattices(A)
& v4_lattices(A)
& v3_lattices(A)
& ~ v3_struct_0(A)
& l3_lattices(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3611,axiom,
? [A] :
( v16_lattices(A)
& v15_lattices(A)
& v14_lattices(A)
& v13_lattices(A)
& v10_lattices(A)
& v9_lattices(A)
& v8_lattices(A)
& v7_lattices(A)
& v6_lattices(A)
& v5_lattices(A)
& v4_lattices(A)
& v3_lattices(A)
& ~ v3_struct_0(A)
& l3_lattices(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3614,axiom,
? [A] :
( v17_lattices(A)
& v16_lattices(A)
& v15_lattices(A)
& v14_lattices(A)
& v13_lattices(A)
& v11_lattices(A)
& v10_lattices(A)
& v9_lattices(A)
& v8_lattices(A)
& v7_lattices(A)
& v6_lattices(A)
& v5_lattices(A)
& v4_lattices(A)
& v3_lattices(A)
& ~ v3_struct_0(A)
& l3_lattices(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3695,axiom,
? [A] : l3_lattices(A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4023,axiom,
? [A] :
( v3_filter_0(A)
& v10_lattices(A)
& v9_lattices(A)
& v8_lattices(A)
& v7_lattices(A)
& v6_lattices(A)
& v5_lattices(A)
& v4_lattices(A)
& v3_lattices(A)
& ~ v3_struct_0(A)
& l3_lattices(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4157,axiom,
? [A] :
( v1_lattice2(A)
& v10_lattices(A)
& v9_lattices(A)
& v8_lattices(A)
& v7_lattices(A)
& v6_lattices(A)
& v5_lattices(A)
& v4_lattices(A)
& ~ v3_struct_0(A)
& l3_lattices(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4160,axiom,
? [A] :
( v1_lattice2(A)
& v3_filter_0(A)
& v13_lattices(A)
& v10_lattices(A)
& v9_lattices(A)
& v8_lattices(A)
& v7_lattices(A)
& v6_lattices(A)
& v5_lattices(A)
& v4_lattices(A)
& v3_lattices(A)
& ~ v3_struct_0(A)
& l3_lattices(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4372,axiom,
? [A] :
( v6_lattice3(A)
& v5_lattice3(A)
& v4_lattice3(A)
& v10_lattices(A)
& v9_lattices(A)
& v8_lattices(A)
& v7_lattices(A)
& v6_lattices(A)
& v5_lattices(A)
& v4_lattices(A)
& v3_lattices(A)
& ~ v3_struct_0(A)
& l3_lattices(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4457,axiom,
! [A,B] :
( ( l3_lattices(A)
& ~ v3_struct_0(A) )
=> m1_subset_1(k15_lattice3(A,B),u1_struct_0(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4458,axiom,
! [A,B] :
( ( l3_lattices(A)
& ~ v3_struct_0(A) )
=> m1_subset_1(k16_lattice3(A,B),u1_struct_0(A)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5251,axiom,
? [A] :
( v4_conlat_1(A)
& ~ v3_conlat_1(A)
& l2_conlat_1(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5332,axiom,
! [A] :
( ( l2_conlat_1(A)
& ~ v3_conlat_1(A) )
=> ! [B] :
( m1_subset_1(B,u1_struct_0(k11_conlat_1(A)))
=> k12_conlat_1(A,B) = B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5363,axiom,
! [A] :
( ( l2_conlat_1(A)
& ~ v3_conlat_1(A) )
=> ( l3_lattices(k11_conlat_1(A))
& v3_lattices(k11_conlat_1(A))
& ~ v3_struct_0(k11_conlat_1(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5364,axiom,
! [A,B] :
( ( m1_subset_1(B,u1_struct_0(k11_conlat_1(A)))
& l2_conlat_1(A)
& ~ v3_conlat_1(A) )
=> ( l3_conlat_1(k12_conlat_1(A,B),A)
& v9_conlat_1(k12_conlat_1(A,B),A)
& ~ v7_conlat_1(k12_conlat_1(A,B),A)
& v6_conlat_1(k12_conlat_1(A,B),A) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5386,axiom,
? [A] :
( v6_group_1(A)
& v15_lattices(A)
& v14_lattices(A)
& v13_lattices(A)
& v10_lattices(A)
& v9_lattices(A)
& v8_lattices(A)
& v7_lattices(A)
& v6_lattices(A)
& v5_lattices(A)
& v4_lattices(A)
& ~ v3_struct_0(A)
& l3_lattices(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5389,axiom,
? [A] :
( v1_lattice6(A)
& v4_lattice3(A)
& v15_lattices(A)
& v14_lattices(A)
& v13_lattices(A)
& v10_lattices(A)
& v9_lattices(A)
& v8_lattices(A)
& v7_lattices(A)
& v6_lattices(A)
& v5_lattices(A)
& v4_lattices(A)
& ~ v3_struct_0(A)
& l3_lattices(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5390,axiom,
? [A] :
( v2_lattice6(A)
& v4_lattice3(A)
& v15_lattices(A)
& v14_lattices(A)
& v13_lattices(A)
& v10_lattices(A)
& v9_lattices(A)
& v8_lattices(A)
& v7_lattices(A)
& v6_lattices(A)
& v5_lattices(A)
& v4_lattices(A)
& ~ v3_struct_0(A)
& l3_lattices(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5393,axiom,
? [A] :
( v3_realset2(A)
& v10_lattices(A)
& v9_lattices(A)
& v8_lattices(A)
& v7_lattices(A)
& v6_lattices(A)
& v5_lattices(A)
& v4_lattices(A)
& v3_lattices(A)
& ~ v3_struct_0(A)
& l3_lattices(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5394,axiom,
? [A] :
( v7_lattice6(A)
& v4_lattice3(A)
& v15_lattices(A)
& v14_lattices(A)
& v13_lattices(A)
& v10_lattices(A)
& v9_lattices(A)
& v8_lattices(A)
& v7_lattices(A)
& v6_lattices(A)
& v5_lattices(A)
& v4_lattices(A)
& ~ v3_struct_0(A)
& l3_lattices(A) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5466,axiom,
! [A] :
( ( l2_conlat_1(A)
& ~ v3_conlat_1(A) )
=> ( v4_lattice3(k11_conlat_1(A))
& v15_lattices(k11_conlat_1(A))
& v14_lattices(k11_conlat_1(A))
& v13_lattices(k11_conlat_1(A))
& v10_lattices(k11_conlat_1(A))
& v9_lattices(k11_conlat_1(A))
& v8_lattices(k11_conlat_1(A))
& v7_lattices(k11_conlat_1(A))
& v6_lattices(k11_conlat_1(A))
& v5_lattices(k11_conlat_1(A))
& v4_lattices(k11_conlat_1(A))
& v3_lattices(k11_conlat_1(A))
& ~ v3_struct_0(k11_conlat_1(A)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5470,conjecture,
! [A] :
( ( l2_conlat_1(A)
& ~ v3_conlat_1(A) )
=> ! [B] :
( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(k11_conlat_1(A))))
=> ( l3_conlat_1(k15_lattice3(k11_conlat_1(A),B),A)
& v9_conlat_1(k15_lattice3(k11_conlat_1(A),B),A)
& ~ v7_conlat_1(k15_lattice3(k11_conlat_1(A),B),A)
& l3_conlat_1(k16_lattice3(k11_conlat_1(A),B),A)
& v9_conlat_1(k16_lattice3(k11_conlat_1(A),B),A)
& ~ v7_conlat_1(k16_lattice3(k11_conlat_1(A),B),A) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f5471,negated_conjecture,
~ ! [A] :
( ( l2_conlat_1(A)
& ~ v3_conlat_1(A) )
=> ! [B] :
( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(k11_conlat_1(A))))
=> ( l3_conlat_1(k15_lattice3(k11_conlat_1(A),B),A)
& v9_conlat_1(k15_lattice3(k11_conlat_1(A),B),A)
& ~ v7_conlat_1(k15_lattice3(k11_conlat_1(A),B),A)
& l3_conlat_1(k16_lattice3(k11_conlat_1(A),B),A)
& v9_conlat_1(k16_lattice3(k11_conlat_1(A),B),A)
& ~ v7_conlat_1(k16_lattice3(k11_conlat_1(A),B),A) ) ) ),
inference(negated_conjecture,[status(cth)],[f5470]) ).
fof(f5553,plain,
~ v1_xboole_0(sK21_skl),
inference(skolemize,[status(esa),new_symbols(skolem,[sK21_skl]),skolemize(A,sK21_skl)],[f26]) ).
fof(f5554,plain,
~ v1_xboole_0(sK21_skl),
inference(cnf_transformation,[status(thm)],[f5553]) ).
fof(f6479,plain,
! [X0] : m1_subset_1(k8_subset_1(X0),X0),
inference(cnf_transformation,[status(thm)],[f466]) ).
fof(f12375,plain,
k3_numbers != k1_numbers,
inference(cnf_transformation,[status(thm)],[f2450]) ).
fof(f12376,plain,
k2_numbers != k3_numbers,
inference(cnf_transformation,[status(thm)],[f2451]) ).
fof(f12382,plain,
k1_numbers != k5_numbers,
inference(cnf_transformation,[status(thm)],[f2457]) ).
fof(f12383,plain,
k2_numbers != k5_numbers,
inference(cnf_transformation,[status(thm)],[f2458]) ).
fof(f12385,plain,
k5_ordinal2 = k5_numbers,
inference(cnf_transformation,[status(thm)],[f2464]) ).
fof(f15675,plain,
( v3_lattices(sK979_skl)
& ~ v3_struct_0(sK979_skl)
& l3_lattices(sK979_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK979_skl]),skolemize(A,sK979_skl)],[f3601]) ).
fof(f15676,plain,
l3_lattices(sK979_skl),
inference(cnf_transformation,[status(thm)],[f15675]) ).
fof(f15702,plain,
( v10_lattices(sK982_skl)
& v9_lattices(sK982_skl)
& v8_lattices(sK982_skl)
& v7_lattices(sK982_skl)
& v6_lattices(sK982_skl)
& v5_lattices(sK982_skl)
& v4_lattices(sK982_skl)
& v3_lattices(sK982_skl)
& ~ v3_struct_0(sK982_skl)
& l3_lattices(sK982_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK982_skl]),skolemize(A,sK982_skl)],[f3606]) ).
fof(f15712,plain,
v10_lattices(sK982_skl),
inference(cnf_transformation,[status(thm)],[f15702]) ).
fof(f15713,plain,
( v14_lattices(sK983_skl)
& v13_lattices(sK983_skl)
& v12_lattices(sK983_skl)
& v11_lattices(sK983_skl)
& v10_lattices(sK983_skl)
& v9_lattices(sK983_skl)
& v8_lattices(sK983_skl)
& v7_lattices(sK983_skl)
& v6_lattices(sK983_skl)
& v5_lattices(sK983_skl)
& v4_lattices(sK983_skl)
& v3_lattices(sK983_skl)
& ~ v3_struct_0(sK983_skl)
& l3_lattices(sK983_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK983_skl]),skolemize(A,sK983_skl)],[f3607]) ).
fof(f15714,plain,
l3_lattices(sK983_skl),
inference(cnf_transformation,[status(thm)],[f15713]) ).
fof(f15735,plain,
( v15_lattices(sK984_skl)
& v14_lattices(sK984_skl)
& v13_lattices(sK984_skl)
& v10_lattices(sK984_skl)
& v9_lattices(sK984_skl)
& v8_lattices(sK984_skl)
& v7_lattices(sK984_skl)
& v6_lattices(sK984_skl)
& v5_lattices(sK984_skl)
& v4_lattices(sK984_skl)
& v3_lattices(sK984_skl)
& ~ v3_struct_0(sK984_skl)
& l3_lattices(sK984_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK984_skl]),skolemize(A,sK984_skl)],[f3610]) ).
fof(f15736,plain,
l3_lattices(sK984_skl),
inference(cnf_transformation,[status(thm)],[f15735]) ).
fof(f15749,plain,
( v16_lattices(sK985_skl)
& v15_lattices(sK985_skl)
& v14_lattices(sK985_skl)
& v13_lattices(sK985_skl)
& v10_lattices(sK985_skl)
& v9_lattices(sK985_skl)
& v8_lattices(sK985_skl)
& v7_lattices(sK985_skl)
& v6_lattices(sK985_skl)
& v5_lattices(sK985_skl)
& v4_lattices(sK985_skl)
& v3_lattices(sK985_skl)
& ~ v3_struct_0(sK985_skl)
& l3_lattices(sK985_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK985_skl]),skolemize(A,sK985_skl)],[f3611]) ).
fof(f15759,plain,
v10_lattices(sK985_skl),
inference(cnf_transformation,[status(thm)],[f15749]) ).
fof(f15774,plain,
( v17_lattices(sK986_skl)
& v16_lattices(sK986_skl)
& v15_lattices(sK986_skl)
& v14_lattices(sK986_skl)
& v13_lattices(sK986_skl)
& v11_lattices(sK986_skl)
& v10_lattices(sK986_skl)
& v9_lattices(sK986_skl)
& v8_lattices(sK986_skl)
& v7_lattices(sK986_skl)
& v6_lattices(sK986_skl)
& v5_lattices(sK986_skl)
& v4_lattices(sK986_skl)
& v3_lattices(sK986_skl)
& ~ v3_struct_0(sK986_skl)
& l3_lattices(sK986_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK986_skl]),skolemize(A,sK986_skl)],[f3614]) ).
fof(f15784,plain,
v10_lattices(sK986_skl),
inference(cnf_transformation,[status(thm)],[f15774]) ).
fof(f16018,plain,
l3_lattices(sK1026_skl),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1026_skl]),skolemize(A,sK1026_skl)],[f3695]) ).
fof(f16019,plain,
l3_lattices(sK1026_skl),
inference(cnf_transformation,[status(thm)],[f16018]) ).
fof(f16682,plain,
( v3_filter_0(sK1079_skl)
& v10_lattices(sK1079_skl)
& v9_lattices(sK1079_skl)
& v8_lattices(sK1079_skl)
& v7_lattices(sK1079_skl)
& v6_lattices(sK1079_skl)
& v5_lattices(sK1079_skl)
& v4_lattices(sK1079_skl)
& v3_lattices(sK1079_skl)
& ~ v3_struct_0(sK1079_skl)
& l3_lattices(sK1079_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1079_skl]),skolemize(A,sK1079_skl)],[f4023]) ).
fof(f16683,plain,
l3_lattices(sK1079_skl),
inference(cnf_transformation,[status(thm)],[f16682]) ).
fof(f17160,plain,
( v1_lattice2(sK1113_skl)
& v10_lattices(sK1113_skl)
& v9_lattices(sK1113_skl)
& v8_lattices(sK1113_skl)
& v7_lattices(sK1113_skl)
& v6_lattices(sK1113_skl)
& v5_lattices(sK1113_skl)
& v4_lattices(sK1113_skl)
& ~ v3_struct_0(sK1113_skl)
& l3_lattices(sK1113_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1113_skl]),skolemize(A,sK1113_skl)],[f4157]) ).
fof(f17161,plain,
l3_lattices(sK1113_skl),
inference(cnf_transformation,[status(thm)],[f17160]) ).
fof(f17192,plain,
( v1_lattice2(sK1114_skl)
& v3_filter_0(sK1114_skl)
& v13_lattices(sK1114_skl)
& v10_lattices(sK1114_skl)
& v9_lattices(sK1114_skl)
& v8_lattices(sK1114_skl)
& v7_lattices(sK1114_skl)
& v6_lattices(sK1114_skl)
& v5_lattices(sK1114_skl)
& v4_lattices(sK1114_skl)
& v3_lattices(sK1114_skl)
& ~ v3_struct_0(sK1114_skl)
& l3_lattices(sK1114_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1114_skl]),skolemize(A,sK1114_skl)],[f4160]) ).
fof(f17202,plain,
v10_lattices(sK1114_skl),
inference(cnf_transformation,[status(thm)],[f17192]) ).
fof(f18018,plain,
( v6_lattice3(sK1177_skl)
& v5_lattice3(sK1177_skl)
& v4_lattice3(sK1177_skl)
& v10_lattices(sK1177_skl)
& v9_lattices(sK1177_skl)
& v8_lattices(sK1177_skl)
& v7_lattices(sK1177_skl)
& v6_lattices(sK1177_skl)
& v5_lattices(sK1177_skl)
& v4_lattices(sK1177_skl)
& v3_lattices(sK1177_skl)
& ~ v3_struct_0(sK1177_skl)
& l3_lattices(sK1177_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1177_skl]),skolemize(A,sK1177_skl)],[f4372]) ).
fof(f18019,plain,
l3_lattices(sK1177_skl),
inference(cnf_transformation,[status(thm)],[f18018]) ).
fof(f18028,plain,
v10_lattices(sK1177_skl),
inference(cnf_transformation,[status(thm)],[f18018]) ).
fof(f18029,plain,
v4_lattice3(sK1177_skl),
inference(cnf_transformation,[status(thm)],[f18018]) ).
fof(f18422,plain,
! [A,B] :
( m1_subset_1(k15_lattice3(A,B),u1_struct_0(A))
| ~ l3_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f4457]) ).
fof(f18423,plain,
! [A] :
( ! [B] : m1_subset_1(k15_lattice3(A,B),u1_struct_0(A))
| ~ l3_lattices(A)
| v3_struct_0(A) ),
inference(miniscoping,[status(thm)],[f18422]) ).
fof(f18424,plain,
! [X0,X1] :
( m1_subset_1(k15_lattice3(X0,X1),u1_struct_0(X0))
| v3_struct_0(X0)
| ~ l3_lattices(X0) ),
inference(cnf_transformation,[status(thm)],[f18423]) ).
fof(f18425,plain,
! [A,B] :
( m1_subset_1(k16_lattice3(A,B),u1_struct_0(A))
| ~ l3_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f4458]) ).
fof(f18426,plain,
! [A] :
( ! [B] : m1_subset_1(k16_lattice3(A,B),u1_struct_0(A))
| ~ l3_lattices(A)
| v3_struct_0(A) ),
inference(miniscoping,[status(thm)],[f18425]) ).
fof(f18427,plain,
! [X0,X1] :
( ~ l3_lattices(X0)
| v3_struct_0(X0)
| m1_subset_1(k16_lattice3(X0,X1),u1_struct_0(X0)) ),
inference(cnf_transformation,[status(thm)],[f18426]) ).
fof(f22276,plain,
( v4_conlat_1(sK1576_skl)
& ~ v3_conlat_1(sK1576_skl)
& l2_conlat_1(sK1576_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1576_skl]),skolemize(A,sK1576_skl)],[f5251]) ).
fof(f22277,plain,
l2_conlat_1(sK1576_skl),
inference(cnf_transformation,[status(thm)],[f22276]) ).
fof(f22278,plain,
~ v3_conlat_1(sK1576_skl),
inference(cnf_transformation,[status(thm)],[f22276]) ).
fof(f22613,plain,
! [A] :
( ! [B] :
( k12_conlat_1(A,B) = B
| ~ m1_subset_1(B,u1_struct_0(k11_conlat_1(A))) )
| ~ l2_conlat_1(A)
| v3_conlat_1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f5332]) ).
fof(f22614,plain,
! [X0,X1] :
( ~ l2_conlat_1(X0)
| k12_conlat_1(X0,X1) = X1
| ~ m1_subset_1(X1,u1_struct_0(k11_conlat_1(X0)))
| v3_conlat_1(X0) ),
inference(cnf_transformation,[status(thm)],[f22613]) ).
fof(f22710,plain,
! [A] :
( ( l3_lattices(k11_conlat_1(A))
& v3_lattices(k11_conlat_1(A))
& ~ v3_struct_0(k11_conlat_1(A)) )
| ~ l2_conlat_1(A)
| v3_conlat_1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f5363]) ).
fof(f22713,plain,
! [X0] :
( l3_lattices(k11_conlat_1(X0))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0) ),
inference(cnf_transformation,[status(thm)],[f22710]) ).
fof(f22714,plain,
! [A,B] :
( ( l3_conlat_1(k12_conlat_1(A,B),A)
& v9_conlat_1(k12_conlat_1(A,B),A)
& ~ v7_conlat_1(k12_conlat_1(A,B),A)
& v6_conlat_1(k12_conlat_1(A,B),A) )
| ~ m1_subset_1(B,u1_struct_0(k11_conlat_1(A)))
| ~ l2_conlat_1(A)
| v3_conlat_1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f5364]) ).
fof(f22716,plain,
! [X0,X1] :
( ~ m1_subset_1(X1,u1_struct_0(k11_conlat_1(X0)))
| v3_conlat_1(X0)
| ~ l2_conlat_1(X0)
| ~ v7_conlat_1(k12_conlat_1(X0,X1),X0) ),
inference(cnf_transformation,[status(thm)],[f22714]) ).
fof(f22717,plain,
! [X0,X1] :
( ~ l2_conlat_1(X0)
| v3_conlat_1(X0)
| ~ m1_subset_1(X1,u1_struct_0(k11_conlat_1(X0)))
| v9_conlat_1(k12_conlat_1(X0,X1),X0) ),
inference(cnf_transformation,[status(thm)],[f22714]) ).
fof(f22718,plain,
! [X0,X1] :
( ~ l2_conlat_1(X0)
| v3_conlat_1(X0)
| ~ m1_subset_1(X1,u1_struct_0(k11_conlat_1(X0)))
| l3_conlat_1(k12_conlat_1(X0,X1),X0) ),
inference(cnf_transformation,[status(thm)],[f22714]) ).
fof(f22810,plain,
( v6_group_1(sK1625_skl)
& v15_lattices(sK1625_skl)
& v14_lattices(sK1625_skl)
& v13_lattices(sK1625_skl)
& v10_lattices(sK1625_skl)
& v9_lattices(sK1625_skl)
& v8_lattices(sK1625_skl)
& v7_lattices(sK1625_skl)
& v6_lattices(sK1625_skl)
& v5_lattices(sK1625_skl)
& v4_lattices(sK1625_skl)
& ~ v3_struct_0(sK1625_skl)
& l3_lattices(sK1625_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1625_skl]),skolemize(A,sK1625_skl)],[f5386]) ).
fof(f22811,plain,
l3_lattices(sK1625_skl),
inference(cnf_transformation,[status(thm)],[f22810]) ).
fof(f22819,plain,
v10_lattices(sK1625_skl),
inference(cnf_transformation,[status(thm)],[f22810]) ).
fof(f22852,plain,
( v1_lattice6(sK1626_skl)
& v4_lattice3(sK1626_skl)
& v15_lattices(sK1626_skl)
& v14_lattices(sK1626_skl)
& v13_lattices(sK1626_skl)
& v10_lattices(sK1626_skl)
& v9_lattices(sK1626_skl)
& v8_lattices(sK1626_skl)
& v7_lattices(sK1626_skl)
& v6_lattices(sK1626_skl)
& v5_lattices(sK1626_skl)
& v4_lattices(sK1626_skl)
& ~ v3_struct_0(sK1626_skl)
& l3_lattices(sK1626_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1626_skl]),skolemize(A,sK1626_skl)],[f5389]) ).
fof(f22853,plain,
l3_lattices(sK1626_skl),
inference(cnf_transformation,[status(thm)],[f22852]) ).
fof(f22861,plain,
v10_lattices(sK1626_skl),
inference(cnf_transformation,[status(thm)],[f22852]) ).
fof(f22865,plain,
v4_lattice3(sK1626_skl),
inference(cnf_transformation,[status(thm)],[f22852]) ).
fof(f22867,plain,
( v2_lattice6(sK1627_skl)
& v4_lattice3(sK1627_skl)
& v15_lattices(sK1627_skl)
& v14_lattices(sK1627_skl)
& v13_lattices(sK1627_skl)
& v10_lattices(sK1627_skl)
& v9_lattices(sK1627_skl)
& v8_lattices(sK1627_skl)
& v7_lattices(sK1627_skl)
& v6_lattices(sK1627_skl)
& v5_lattices(sK1627_skl)
& v4_lattices(sK1627_skl)
& ~ v3_struct_0(sK1627_skl)
& l3_lattices(sK1627_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1627_skl]),skolemize(A,sK1627_skl)],[f5390]) ).
fof(f22868,plain,
l3_lattices(sK1627_skl),
inference(cnf_transformation,[status(thm)],[f22867]) ).
fof(f22876,plain,
v10_lattices(sK1627_skl),
inference(cnf_transformation,[status(thm)],[f22867]) ).
fof(f22880,plain,
v4_lattice3(sK1627_skl),
inference(cnf_transformation,[status(thm)],[f22867]) ).
fof(f22902,plain,
( v3_realset2(sK1628_skl)
& v10_lattices(sK1628_skl)
& v9_lattices(sK1628_skl)
& v8_lattices(sK1628_skl)
& v7_lattices(sK1628_skl)
& v6_lattices(sK1628_skl)
& v5_lattices(sK1628_skl)
& v4_lattices(sK1628_skl)
& v3_lattices(sK1628_skl)
& ~ v3_struct_0(sK1628_skl)
& l3_lattices(sK1628_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1628_skl]),skolemize(A,sK1628_skl)],[f5393]) ).
fof(f22903,plain,
l3_lattices(sK1628_skl),
inference(cnf_transformation,[status(thm)],[f22902]) ).
fof(f22912,plain,
v10_lattices(sK1628_skl),
inference(cnf_transformation,[status(thm)],[f22902]) ).
fof(f22914,plain,
( v7_lattice6(sK1629_skl)
& v4_lattice3(sK1629_skl)
& v15_lattices(sK1629_skl)
& v14_lattices(sK1629_skl)
& v13_lattices(sK1629_skl)
& v10_lattices(sK1629_skl)
& v9_lattices(sK1629_skl)
& v8_lattices(sK1629_skl)
& v7_lattices(sK1629_skl)
& v6_lattices(sK1629_skl)
& v5_lattices(sK1629_skl)
& v4_lattices(sK1629_skl)
& ~ v3_struct_0(sK1629_skl)
& l3_lattices(sK1629_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1629_skl]),skolemize(A,sK1629_skl)],[f5394]) ).
fof(f22915,plain,
l3_lattices(sK1629_skl),
inference(cnf_transformation,[status(thm)],[f22914]) ).
fof(f22923,plain,
v10_lattices(sK1629_skl),
inference(cnf_transformation,[status(thm)],[f22914]) ).
fof(f22927,plain,
v4_lattice3(sK1629_skl),
inference(cnf_transformation,[status(thm)],[f22914]) ).
fof(f23231,plain,
! [A] :
( ( v4_lattice3(k11_conlat_1(A))
& v15_lattices(k11_conlat_1(A))
& v14_lattices(k11_conlat_1(A))
& v13_lattices(k11_conlat_1(A))
& v10_lattices(k11_conlat_1(A))
& v9_lattices(k11_conlat_1(A))
& v8_lattices(k11_conlat_1(A))
& v7_lattices(k11_conlat_1(A))
& v6_lattices(k11_conlat_1(A))
& v5_lattices(k11_conlat_1(A))
& v4_lattices(k11_conlat_1(A))
& v3_lattices(k11_conlat_1(A))
& ~ v3_struct_0(k11_conlat_1(A)) )
| ~ l2_conlat_1(A)
| v3_conlat_1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f5466]) ).
fof(f23232,plain,
! [X0] :
( v3_conlat_1(X0)
| ~ l2_conlat_1(X0)
| ~ v3_struct_0(k11_conlat_1(X0)) ),
inference(cnf_transformation,[status(thm)],[f23231]) ).
fof(f23252,plain,
? [A] :
( ? [B] :
( ( ~ l3_conlat_1(k15_lattice3(k11_conlat_1(A),B),A)
| ~ v9_conlat_1(k15_lattice3(k11_conlat_1(A),B),A)
| v7_conlat_1(k15_lattice3(k11_conlat_1(A),B),A)
| ~ l3_conlat_1(k16_lattice3(k11_conlat_1(A),B),A)
| ~ v9_conlat_1(k16_lattice3(k11_conlat_1(A),B),A)
| v7_conlat_1(k16_lattice3(k11_conlat_1(A),B),A) )
& m1_subset_1(B,k1_zfmisc_1(u1_struct_0(k11_conlat_1(A)))) )
& l2_conlat_1(A)
& ~ v3_conlat_1(A) ),
inference(pre_NNF_transformation,[status(thm)],[f5471]) ).
fof(f23253,plain,
( ( ~ l3_conlat_1(k15_lattice3(k11_conlat_1(sK1656_skl),sK1657_skl),sK1656_skl)
| ~ v9_conlat_1(k15_lattice3(k11_conlat_1(sK1656_skl),sK1657_skl),sK1656_skl)
| v7_conlat_1(k15_lattice3(k11_conlat_1(sK1656_skl),sK1657_skl),sK1656_skl)
| ~ l3_conlat_1(k16_lattice3(k11_conlat_1(sK1656_skl),sK1657_skl),sK1656_skl)
| ~ v9_conlat_1(k16_lattice3(k11_conlat_1(sK1656_skl),sK1657_skl),sK1656_skl)
| v7_conlat_1(k16_lattice3(k11_conlat_1(sK1656_skl),sK1657_skl),sK1656_skl) )
& m1_subset_1(sK1657_skl,k1_zfmisc_1(u1_struct_0(k11_conlat_1(sK1656_skl))))
& l2_conlat_1(sK1656_skl)
& ~ v3_conlat_1(sK1656_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1656_skl,sK1657_skl]),skolemize(A,sK1656_skl),skolemize(B,sK1657_skl)],[f23252]) ).
fof(f23254,plain,
~ v3_conlat_1(sK1656_skl),
inference(cnf_transformation,[status(thm)],[f23253]) ).
fof(f23255,plain,
l2_conlat_1(sK1656_skl),
inference(cnf_transformation,[status(thm)],[f23253]) ).
fof(f23257,plain,
( ~ l3_conlat_1(k15_lattice3(k11_conlat_1(sK1656_skl),sK1657_skl),sK1656_skl)
| ~ v9_conlat_1(k15_lattice3(k11_conlat_1(sK1656_skl),sK1657_skl),sK1656_skl)
| v7_conlat_1(k15_lattice3(k11_conlat_1(sK1656_skl),sK1657_skl),sK1656_skl)
| ~ l3_conlat_1(k16_lattice3(k11_conlat_1(sK1656_skl),sK1657_skl),sK1656_skl)
| ~ v9_conlat_1(k16_lattice3(k11_conlat_1(sK1656_skl),sK1657_skl),sK1656_skl)
| v7_conlat_1(k16_lattice3(k11_conlat_1(sK1656_skl),sK1657_skl),sK1656_skl) ),
inference(cnf_transformation,[status(thm)],[f23253]) ).
fof(f24759,definition,
! [X1] :
( sQ14_spl
<=> v1_xboole_0(X1) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f24760,plain,
! [X0] :
( ~ sQ14_spl
| v1_xboole_0(X0) ),
inference(component_clause,[status(thm)],[f24759]) ).
fof(f26336,definition,
( sQ431_spl
<=> v7_conlat_1(k16_lattice3(k11_conlat_1(sK1656_skl),sK1657_skl),sK1656_skl) ),
introduced(definition,[new_symbols(definition,[sQ431_spl])],[split_symbol_definition]) ).
fof(f26337,plain,
( ~ sQ431_spl
| v7_conlat_1(k16_lattice3(k11_conlat_1(sK1656_skl),sK1657_skl),sK1656_skl) ),
inference(component_clause,[status(thm)],[f26336]) ).
fof(f26339,definition,
( sQ432_spl
<=> v9_conlat_1(k16_lattice3(k11_conlat_1(sK1656_skl),sK1657_skl),sK1656_skl) ),
introduced(definition,[new_symbols(definition,[sQ432_spl])],[split_symbol_definition]) ).
fof(f26341,plain,
( sQ432_spl
| ~ v9_conlat_1(k16_lattice3(k11_conlat_1(sK1656_skl),sK1657_skl),sK1656_skl) ),
inference(component_clause,[status(thm)],[f26339]) ).
fof(f26342,definition,
( sQ433_spl
<=> l3_conlat_1(k16_lattice3(k11_conlat_1(sK1656_skl),sK1657_skl),sK1656_skl) ),
introduced(definition,[new_symbols(definition,[sQ433_spl])],[split_symbol_definition]) ).
fof(f26344,plain,
( sQ433_spl
| ~ l3_conlat_1(k16_lattice3(k11_conlat_1(sK1656_skl),sK1657_skl),sK1656_skl) ),
inference(component_clause,[status(thm)],[f26342]) ).
fof(f26345,definition,
( sQ434_spl
<=> v7_conlat_1(k15_lattice3(k11_conlat_1(sK1656_skl),sK1657_skl),sK1656_skl) ),
introduced(definition,[new_symbols(definition,[sQ434_spl])],[split_symbol_definition]) ).
fof(f26346,plain,
( ~ sQ434_spl
| v7_conlat_1(k15_lattice3(k11_conlat_1(sK1656_skl),sK1657_skl),sK1656_skl) ),
inference(component_clause,[status(thm)],[f26345]) ).
fof(f26348,definition,
( sQ435_spl
<=> v9_conlat_1(k15_lattice3(k11_conlat_1(sK1656_skl),sK1657_skl),sK1656_skl) ),
introduced(definition,[new_symbols(definition,[sQ435_spl])],[split_symbol_definition]) ).
fof(f26350,plain,
( sQ435_spl
| ~ v9_conlat_1(k15_lattice3(k11_conlat_1(sK1656_skl),sK1657_skl),sK1656_skl) ),
inference(component_clause,[status(thm)],[f26348]) ).
fof(f26351,definition,
( sQ436_spl
<=> l3_conlat_1(k15_lattice3(k11_conlat_1(sK1656_skl),sK1657_skl),sK1656_skl) ),
introduced(definition,[new_symbols(definition,[sQ436_spl])],[split_symbol_definition]) ).
fof(f26353,plain,
( sQ436_spl
| ~ l3_conlat_1(k15_lattice3(k11_conlat_1(sK1656_skl),sK1657_skl),sK1656_skl) ),
inference(component_clause,[status(thm)],[f26351]) ).
fof(f26354,plain,
( ~ sQ436_spl
| ~ sQ435_spl
| sQ434_spl
| ~ sQ433_spl
| ~ sQ432_spl
| sQ431_spl ),
inference(split_clause,[status(thm)],[f23257,f26336,f26339,f26342,f26345,f26348,f26351]) ).
fof(f28331,definition,
( sQ582_spl
<=> l2_conlat_1(sK1656_skl) ),
introduced(definition,[new_symbols(definition,[sQ582_spl])],[split_symbol_definition]) ).
fof(f28333,plain,
( sQ582_spl
| ~ l2_conlat_1(sK1656_skl) ),
inference(component_clause,[status(thm)],[f28331]) ).
fof(f28338,plain,
( sQ582_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f28333,f23255]) ).
fof(f28339,plain,
sQ582_spl,
inference(contradiction_clause,[status(thm)],[f28338]) ).
fof(f28353,definition,
( sQ586_spl
<=> v3_struct_0(k11_conlat_1(sK1656_skl)) ),
introduced(definition,[new_symbols(definition,[sQ586_spl])],[split_symbol_definition]) ).
fof(f28354,plain,
( ~ sQ586_spl
| v3_struct_0(k11_conlat_1(sK1656_skl)) ),
inference(component_clause,[status(thm)],[f28353]) ).
fof(f28359,definition,
( sQ588_spl
<=> l3_lattices(k11_conlat_1(sK1656_skl)) ),
introduced(definition,[new_symbols(definition,[sQ588_spl])],[split_symbol_definition]) ).
fof(f28361,plain,
( sQ588_spl
| ~ l3_lattices(k11_conlat_1(sK1656_skl)) ),
inference(component_clause,[status(thm)],[f28359]) ).
fof(f28400,definition,
( sQ596_spl
<=> v3_conlat_1(sK1656_skl) ),
introduced(definition,[new_symbols(definition,[sQ596_spl])],[split_symbol_definition]) ).
fof(f28401,plain,
( ~ sQ596_spl
| v3_conlat_1(sK1656_skl) ),
inference(component_clause,[status(thm)],[f28400]) ).
fof(f28404,plain,
( ~ sQ596_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f28401,f23254]) ).
fof(f28405,plain,
~ sQ596_spl,
inference(contradiction_clause,[status(thm)],[f28404]) ).
fof(f28410,plain,
( sQ588_spl
| v3_conlat_1(sK1656_skl)
| ~ l2_conlat_1(sK1656_skl) ),
inference(resolution,[status(thm)],[f28361,f22713]) ).
fof(f28411,plain,
( sQ588_spl
| sQ596_spl
| ~ sQ582_spl ),
inference(split_clause,[status(thm)],[f28410,f28331,f28400,f28359]) ).
fof(f28417,plain,
( ~ sQ586_spl
| v3_conlat_1(sK1656_skl)
| ~ l2_conlat_1(sK1656_skl) ),
inference(resolution,[status(thm)],[f28354,f23232]) ).
fof(f28418,plain,
( ~ sQ586_spl
| sQ596_spl
| ~ sQ582_spl ),
inference(split_clause,[status(thm)],[f28417,f28331,f28400,f28353]) ).
fof(f29041,definition,
( sQ624_spl
<=> v10_lattices(sK1629_skl) ),
introduced(definition,[new_symbols(definition,[sQ624_spl])],[split_symbol_definition]) ).
fof(f29043,plain,
( sQ624_spl
| ~ v10_lattices(sK1629_skl) ),
inference(component_clause,[status(thm)],[f29041]) ).
fof(f29047,definition,
( sQ626_spl
<=> l3_lattices(sK1629_skl) ),
introduced(definition,[new_symbols(definition,[sQ626_spl])],[split_symbol_definition]) ).
fof(f29049,plain,
( sQ626_spl
| ~ l3_lattices(sK1629_skl) ),
inference(component_clause,[status(thm)],[f29047]) ).
fof(f29111,definition,
( sQ633_spl
<=> l3_lattices(sK1628_skl) ),
introduced(definition,[new_symbols(definition,[sQ633_spl])],[split_symbol_definition]) ).
fof(f29113,plain,
( sQ633_spl
| ~ l3_lattices(sK1628_skl) ),
inference(component_clause,[status(thm)],[f29111]) ).
fof(f29133,definition,
( sQ637_spl
<=> v10_lattices(sK1627_skl) ),
introduced(definition,[new_symbols(definition,[sQ637_spl])],[split_symbol_definition]) ).
fof(f29135,plain,
( sQ637_spl
| ~ v10_lattices(sK1627_skl) ),
inference(component_clause,[status(thm)],[f29133]) ).
fof(f29139,definition,
( sQ639_spl
<=> l3_lattices(sK1627_skl) ),
introduced(definition,[new_symbols(definition,[sQ639_spl])],[split_symbol_definition]) ).
fof(f29141,plain,
( sQ639_spl
| ~ l3_lattices(sK1627_skl) ),
inference(component_clause,[status(thm)],[f29139]) ).
fof(f29169,definition,
( sQ644_spl
<=> v4_lattice3(sK1627_skl) ),
introduced(definition,[new_symbols(definition,[sQ644_spl])],[split_symbol_definition]) ).
fof(f29171,plain,
( sQ644_spl
| ~ v4_lattice3(sK1627_skl) ),
inference(component_clause,[status(thm)],[f29169]) ).
fof(f29174,plain,
( sQ644_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f29171,f22880]) ).
fof(f29175,plain,
sQ644_spl,
inference(contradiction_clause,[status(thm)],[f29174]) ).
fof(f29188,definition,
( sQ647_spl
<=> v4_lattice3(sK1629_skl) ),
introduced(definition,[new_symbols(definition,[sQ647_spl])],[split_symbol_definition]) ).
fof(f29190,plain,
( sQ647_spl
| ~ v4_lattice3(sK1629_skl) ),
inference(component_clause,[status(thm)],[f29188]) ).
fof(f29204,plain,
( sQ647_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f29190,f22927]) ).
fof(f29205,plain,
sQ647_spl,
inference(contradiction_clause,[status(thm)],[f29204]) ).
fof(f29297,definition,
( sQ658_spl
<=> v10_lattices(sK1628_skl) ),
introduced(definition,[new_symbols(definition,[sQ658_spl])],[split_symbol_definition]) ).
fof(f29299,plain,
( sQ658_spl
| ~ v10_lattices(sK1628_skl) ),
inference(component_clause,[status(thm)],[f29297]) ).
fof(f29326,plain,
( sQ658_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f29299,f22912]) ).
fof(f29327,plain,
sQ658_spl,
inference(contradiction_clause,[status(thm)],[f29326]) ).
fof(f29427,plain,
( sQ624_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f29043,f22923]) ).
fof(f29428,plain,
sQ624_spl,
inference(contradiction_clause,[status(thm)],[f29427]) ).
fof(f29437,definition,
( sQ682_spl
<=> l3_lattices(sK1625_skl) ),
introduced(definition,[new_symbols(definition,[sQ682_spl])],[split_symbol_definition]) ).
fof(f29439,plain,
( sQ682_spl
| ~ l3_lattices(sK1625_skl) ),
inference(component_clause,[status(thm)],[f29437]) ).
fof(f29474,definition,
( sQ686_spl
<=> l3_lattices(sK1626_skl) ),
introduced(definition,[new_symbols(definition,[sQ686_spl])],[split_symbol_definition]) ).
fof(f29476,plain,
( sQ686_spl
| ~ l3_lattices(sK1626_skl) ),
inference(component_clause,[status(thm)],[f29474]) ).
fof(f29480,definition,
( sQ688_spl
<=> v4_lattice3(sK1626_skl) ),
introduced(definition,[new_symbols(definition,[sQ688_spl])],[split_symbol_definition]) ).
fof(f29482,plain,
( sQ688_spl
| ~ v4_lattice3(sK1626_skl) ),
inference(component_clause,[status(thm)],[f29480]) ).
fof(f29525,definition,
( sQ696_spl
<=> v10_lattices(sK1625_skl) ),
introduced(definition,[new_symbols(definition,[sQ696_spl])],[split_symbol_definition]) ).
fof(f29527,plain,
( sQ696_spl
| ~ v10_lattices(sK1625_skl) ),
inference(component_clause,[status(thm)],[f29525]) ).
fof(f29551,plain,
( sQ696_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f29527,f22819]) ).
fof(f29552,plain,
sQ696_spl,
inference(contradiction_clause,[status(thm)],[f29551]) ).
fof(f29590,definition,
( sQ708_spl
<=> v10_lattices(sK1626_skl) ),
introduced(definition,[new_symbols(definition,[sQ708_spl])],[split_symbol_definition]) ).
fof(f29592,plain,
( sQ708_spl
| ~ v10_lattices(sK1626_skl) ),
inference(component_clause,[status(thm)],[f29590]) ).
fof(f29616,plain,
( sQ708_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f29592,f22861]) ).
fof(f29617,plain,
sQ708_spl,
inference(contradiction_clause,[status(thm)],[f29616]) ).
fof(f29665,plain,
! [X0] :
( ~ l2_conlat_1(sK1656_skl)
| k12_conlat_1(sK1656_skl,X0) = X0
| ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK1656_skl))) ),
inference(resolution,[status(thm)],[f22614,f23254]) ).
fof(f29666,definition,
! [X0] :
( sQ719_spl
<=> ( k12_conlat_1(sK1656_skl,X0) = X0
| ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK1656_skl))) ) ),
introduced(definition,[new_symbols(definition,[sQ719_spl])],[split_symbol_definition]) ).
fof(f29667,plain,
! [X0] :
( ~ sQ719_spl
| X0 = k12_conlat_1(sK1656_skl,X0)
| ~ m1_subset_1(X0,u1_struct_0(k11_conlat_1(sK1656_skl))) ),
inference(component_clause,[status(thm)],[f29666]) ).
fof(f29669,plain,
( ~ sQ582_spl
| sQ719_spl ),
inference(split_clause,[status(thm)],[f29665,f29666,f28331]) ).
fof(f29677,plain,
( sQ626_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f29049,f22915]) ).
fof(f29678,plain,
sQ626_spl,
inference(contradiction_clause,[status(thm)],[f29677]) ).
fof(f29686,plain,
! [X0] :
( ~ sQ719_spl
| ~ l3_lattices(k11_conlat_1(sK1656_skl))
| v3_struct_0(k11_conlat_1(sK1656_skl))
| k16_lattice3(k11_conlat_1(sK1656_skl),X0) = k12_conlat_1(sK1656_skl,k16_lattice3(k11_conlat_1(sK1656_skl),X0)) ),
inference(resolution,[status(thm)],[f29667,f18427]) ).
fof(f29687,plain,
! [X0] :
( ~ sQ719_spl
| v3_struct_0(k11_conlat_1(sK1656_skl))
| ~ l3_lattices(k11_conlat_1(sK1656_skl))
| k15_lattice3(k11_conlat_1(sK1656_skl),X0) = k12_conlat_1(sK1656_skl,k15_lattice3(k11_conlat_1(sK1656_skl),X0)) ),
inference(resolution,[status(thm)],[f29667,f18424]) ).
fof(f29696,definition,
! [X0] :
( sQ720_spl
<=> k15_lattice3(k11_conlat_1(sK1656_skl),X0) = k12_conlat_1(sK1656_skl,k15_lattice3(k11_conlat_1(sK1656_skl),X0)) ),
introduced(definition,[new_symbols(definition,[sQ720_spl])],[split_symbol_definition]) ).
fof(f29697,plain,
! [X0] :
( ~ sQ720_spl
| k12_conlat_1(sK1656_skl,k15_lattice3(k11_conlat_1(sK1656_skl),X0)) = k15_lattice3(k11_conlat_1(sK1656_skl),X0) ),
inference(component_clause,[status(thm)],[f29696]) ).
fof(f29699,plain,
( ~ sQ719_spl
| sQ586_spl
| ~ sQ588_spl
| sQ720_spl ),
inference(split_clause,[status(thm)],[f29687,f29696,f28359,f28353,f29666]) ).
fof(f29700,definition,
! [X0] :
( sQ721_spl
<=> k16_lattice3(k11_conlat_1(sK1656_skl),X0) = k12_conlat_1(sK1656_skl,k16_lattice3(k11_conlat_1(sK1656_skl),X0)) ),
introduced(definition,[new_symbols(definition,[sQ721_spl])],[split_symbol_definition]) ).
fof(f29701,plain,
! [X0] :
( ~ sQ721_spl
| k16_lattice3(k11_conlat_1(sK1656_skl),X0) = k12_conlat_1(sK1656_skl,k16_lattice3(k11_conlat_1(sK1656_skl),X0)) ),
inference(component_clause,[status(thm)],[f29700]) ).
fof(f29703,plain,
( ~ sQ719_spl
| ~ sQ588_spl
| sQ586_spl
| sQ721_spl ),
inference(split_clause,[status(thm)],[f29686,f29700,f28353,f28359,f29666]) ).
fof(f29721,plain,
! [X0] :
( ~ sQ720_spl
| ~ l2_conlat_1(sK1656_skl)
| v3_conlat_1(sK1656_skl)
| ~ m1_subset_1(k15_lattice3(k11_conlat_1(sK1656_skl),X0),u1_struct_0(k11_conlat_1(sK1656_skl)))
| v9_conlat_1(k15_lattice3(k11_conlat_1(sK1656_skl),X0),sK1656_skl) ),
inference(paramodulation,[status(thm)],[f29697,f22717]) ).
fof(f29722,plain,
! [X0] :
( ~ sQ720_spl
| ~ m1_subset_1(k15_lattice3(k11_conlat_1(sK1656_skl),X0),u1_struct_0(k11_conlat_1(sK1656_skl)))
| v3_conlat_1(sK1656_skl)
| ~ l2_conlat_1(sK1656_skl)
| ~ v7_conlat_1(k15_lattice3(k11_conlat_1(sK1656_skl),X0),sK1656_skl) ),
inference(paramodulation,[status(thm)],[f29697,f22716]) ).
fof(f29723,plain,
! [X0] :
( ~ sQ720_spl
| ~ l2_conlat_1(sK1656_skl)
| v3_conlat_1(sK1656_skl)
| ~ m1_subset_1(k15_lattice3(k11_conlat_1(sK1656_skl),X0),u1_struct_0(k11_conlat_1(sK1656_skl)))
| l3_conlat_1(k15_lattice3(k11_conlat_1(sK1656_skl),X0),sK1656_skl) ),
inference(paramodulation,[status(thm)],[f29697,f22718]) ).
fof(f29725,definition,
! [X0] :
( sQ722_spl
<=> ( ~ m1_subset_1(k15_lattice3(k11_conlat_1(sK1656_skl),X0),u1_struct_0(k11_conlat_1(sK1656_skl)))
| l3_conlat_1(k15_lattice3(k11_conlat_1(sK1656_skl),X0),sK1656_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ722_spl])],[split_symbol_definition]) ).
fof(f29726,plain,
! [X0] :
( ~ sQ722_spl
| ~ m1_subset_1(k15_lattice3(k11_conlat_1(sK1656_skl),X0),u1_struct_0(k11_conlat_1(sK1656_skl)))
| l3_conlat_1(k15_lattice3(k11_conlat_1(sK1656_skl),X0),sK1656_skl) ),
inference(component_clause,[status(thm)],[f29725]) ).
fof(f29728,plain,
( ~ sQ720_spl
| ~ sQ582_spl
| sQ596_spl
| sQ722_spl ),
inference(split_clause,[status(thm)],[f29723,f29725,f28400,f28331,f29696]) ).
fof(f29730,definition,
! [X0] :
( sQ723_spl
<=> ( ~ m1_subset_1(k15_lattice3(k11_conlat_1(sK1656_skl),X0),u1_struct_0(k11_conlat_1(sK1656_skl)))
| ~ v7_conlat_1(k15_lattice3(k11_conlat_1(sK1656_skl),X0),sK1656_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ723_spl])],[split_symbol_definition]) ).
fof(f29731,plain,
! [X0] :
( ~ sQ723_spl
| ~ m1_subset_1(k15_lattice3(k11_conlat_1(sK1656_skl),X0),u1_struct_0(k11_conlat_1(sK1656_skl)))
| ~ v7_conlat_1(k15_lattice3(k11_conlat_1(sK1656_skl),X0),sK1656_skl) ),
inference(component_clause,[status(thm)],[f29730]) ).
fof(f29733,plain,
( ~ sQ720_spl
| sQ596_spl
| ~ sQ582_spl
| sQ723_spl ),
inference(split_clause,[status(thm)],[f29722,f29730,f28331,f28400,f29696]) ).
fof(f29734,definition,
! [X0] :
( sQ724_spl
<=> ( ~ m1_subset_1(k15_lattice3(k11_conlat_1(sK1656_skl),X0),u1_struct_0(k11_conlat_1(sK1656_skl)))
| v9_conlat_1(k15_lattice3(k11_conlat_1(sK1656_skl),X0),sK1656_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ724_spl])],[split_symbol_definition]) ).
fof(f29735,plain,
! [X0] :
( ~ sQ724_spl
| v9_conlat_1(k15_lattice3(k11_conlat_1(sK1656_skl),X0),sK1656_skl)
| ~ m1_subset_1(k15_lattice3(k11_conlat_1(sK1656_skl),X0),u1_struct_0(k11_conlat_1(sK1656_skl))) ),
inference(component_clause,[status(thm)],[f29734]) ).
fof(f29737,plain,
( ~ sQ720_spl
| ~ sQ582_spl
| sQ596_spl
| sQ724_spl ),
inference(split_clause,[status(thm)],[f29721,f29734,f28400,f28331,f29696]) ).
fof(f29777,plain,
! [X0] :
( ~ sQ721_spl
| ~ l2_conlat_1(sK1656_skl)
| v3_conlat_1(sK1656_skl)
| ~ m1_subset_1(k16_lattice3(k11_conlat_1(sK1656_skl),X0),u1_struct_0(k11_conlat_1(sK1656_skl)))
| v9_conlat_1(k16_lattice3(k11_conlat_1(sK1656_skl),X0),sK1656_skl) ),
inference(paramodulation,[status(thm)],[f29701,f22717]) ).
fof(f29778,plain,
! [X0] :
( ~ sQ721_spl
| ~ m1_subset_1(k16_lattice3(k11_conlat_1(sK1656_skl),X0),u1_struct_0(k11_conlat_1(sK1656_skl)))
| v3_conlat_1(sK1656_skl)
| ~ l2_conlat_1(sK1656_skl)
| ~ v7_conlat_1(k16_lattice3(k11_conlat_1(sK1656_skl),X0),sK1656_skl) ),
inference(paramodulation,[status(thm)],[f29701,f22716]) ).
fof(f29779,plain,
! [X0] :
( ~ sQ721_spl
| ~ l2_conlat_1(sK1656_skl)
| v3_conlat_1(sK1656_skl)
| ~ m1_subset_1(k16_lattice3(k11_conlat_1(sK1656_skl),X0),u1_struct_0(k11_conlat_1(sK1656_skl)))
| l3_conlat_1(k16_lattice3(k11_conlat_1(sK1656_skl),X0),sK1656_skl) ),
inference(paramodulation,[status(thm)],[f29701,f22718]) ).
fof(f29780,definition,
! [X0] :
( sQ731_spl
<=> ( ~ m1_subset_1(k16_lattice3(k11_conlat_1(sK1656_skl),X0),u1_struct_0(k11_conlat_1(sK1656_skl)))
| ~ v7_conlat_1(k16_lattice3(k11_conlat_1(sK1656_skl),X0),sK1656_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ731_spl])],[split_symbol_definition]) ).
fof(f29781,plain,
! [X0] :
( ~ sQ731_spl
| ~ m1_subset_1(k16_lattice3(k11_conlat_1(sK1656_skl),X0),u1_struct_0(k11_conlat_1(sK1656_skl)))
| ~ v7_conlat_1(k16_lattice3(k11_conlat_1(sK1656_skl),X0),sK1656_skl) ),
inference(component_clause,[status(thm)],[f29780]) ).
fof(f29783,plain,
( ~ sQ721_spl
| sQ596_spl
| ~ sQ582_spl
| sQ731_spl ),
inference(split_clause,[status(thm)],[f29778,f29780,f28331,f28400,f29700]) ).
fof(f29788,definition,
! [X0] :
( sQ733_spl
<=> ( ~ m1_subset_1(k16_lattice3(k11_conlat_1(sK1656_skl),X0),u1_struct_0(k11_conlat_1(sK1656_skl)))
| v9_conlat_1(k16_lattice3(k11_conlat_1(sK1656_skl),X0),sK1656_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ733_spl])],[split_symbol_definition]) ).
fof(f29789,plain,
! [X0] :
( ~ sQ733_spl
| v9_conlat_1(k16_lattice3(k11_conlat_1(sK1656_skl),X0),sK1656_skl)
| ~ m1_subset_1(k16_lattice3(k11_conlat_1(sK1656_skl),X0),u1_struct_0(k11_conlat_1(sK1656_skl))) ),
inference(component_clause,[status(thm)],[f29788]) ).
fof(f29791,plain,
( ~ sQ721_spl
| ~ sQ582_spl
| sQ596_spl
| sQ733_spl ),
inference(split_clause,[status(thm)],[f29777,f29788,f28400,f28331,f29700]) ).
fof(f29792,definition,
! [X0] :
( sQ734_spl
<=> ( ~ m1_subset_1(k16_lattice3(k11_conlat_1(sK1656_skl),X0),u1_struct_0(k11_conlat_1(sK1656_skl)))
| l3_conlat_1(k16_lattice3(k11_conlat_1(sK1656_skl),X0),sK1656_skl) ) ),
introduced(definition,[new_symbols(definition,[sQ734_spl])],[split_symbol_definition]) ).
fof(f29793,plain,
! [X0] :
( ~ sQ734_spl
| ~ m1_subset_1(k16_lattice3(k11_conlat_1(sK1656_skl),X0),u1_struct_0(k11_conlat_1(sK1656_skl)))
| l3_conlat_1(k16_lattice3(k11_conlat_1(sK1656_skl),X0),sK1656_skl) ),
inference(component_clause,[status(thm)],[f29792]) ).
fof(f29795,plain,
( ~ sQ721_spl
| ~ sQ582_spl
| sQ596_spl
| sQ734_spl ),
inference(split_clause,[status(thm)],[f29779,f29792,f28400,f28331,f29700]) ).
fof(f29822,plain,
( sQ633_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f29113,f22903]) ).
fof(f29823,plain,
sQ633_spl,
inference(contradiction_clause,[status(thm)],[f29822]) ).
fof(f29836,definition,
( sQ740_spl
<=> l2_conlat_1(sK1576_skl) ),
introduced(definition,[new_symbols(definition,[sQ740_spl])],[split_symbol_definition]) ).
fof(f29838,plain,
( sQ740_spl
| ~ l2_conlat_1(sK1576_skl) ),
inference(component_clause,[status(thm)],[f29836]) ).
fof(f29912,definition,
( sQ757_spl
<=> v3_conlat_1(sK1576_skl) ),
introduced(definition,[new_symbols(definition,[sQ757_spl])],[split_symbol_definition]) ).
fof(f29913,plain,
( ~ sQ757_spl
| v3_conlat_1(sK1576_skl) ),
inference(component_clause,[status(thm)],[f29912]) ).
fof(f29916,plain,
( ~ sQ757_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f29913,f22278]) ).
fof(f29917,plain,
~ sQ757_spl,
inference(contradiction_clause,[status(thm)],[f29916]) ).
fof(f29918,plain,
( sQ637_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f29135,f22876]) ).
fof(f29919,plain,
sQ637_spl,
inference(contradiction_clause,[status(thm)],[f29918]) ).
fof(f30033,plain,
( sQ639_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f29141,f22868]) ).
fof(f30034,plain,
sQ639_spl,
inference(contradiction_clause,[status(thm)],[f30033]) ).
fof(f30170,plain,
( sQ740_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f29838,f22277]) ).
fof(f30171,plain,
sQ740_spl,
inference(contradiction_clause,[status(thm)],[f30170]) ).
fof(f30203,plain,
( sQ682_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f29439,f22811]) ).
fof(f30204,plain,
sQ682_spl,
inference(contradiction_clause,[status(thm)],[f30203]) ).
fof(f30306,plain,
( sQ686_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f29476,f22853]) ).
fof(f30307,plain,
sQ686_spl,
inference(contradiction_clause,[status(thm)],[f30306]) ).
fof(f30347,plain,
( sQ688_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f29482,f22865]) ).
fof(f30348,plain,
sQ688_spl,
inference(contradiction_clause,[status(thm)],[f30347]) ).
fof(f30357,plain,
k5_ordinal2 != k1_numbers,
inference(forward_demodulation,[status(thm)],[f12385,f12382]) ).
fof(f30383,plain,
k2_numbers != k5_ordinal2,
inference(forward_demodulation,[status(thm)],[f12385,f12383]) ).
fof(f30428,definition,
( sQ806_spl
<=> k2_numbers = k3_numbers ),
introduced(definition,[new_symbols(definition,[sQ806_spl])],[split_symbol_definition]) ).
fof(f30429,plain,
( ~ sQ806_spl
| k2_numbers = k3_numbers ),
inference(component_clause,[status(thm)],[f30428]) ).
fof(f30432,plain,
( ~ sQ806_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f30429,f12376]) ).
fof(f30433,plain,
~ sQ806_spl,
inference(contradiction_clause,[status(thm)],[f30432]) ).
fof(f30444,definition,
( sQ808_spl
<=> k2_numbers = k5_ordinal2 ),
introduced(definition,[new_symbols(definition,[sQ808_spl])],[split_symbol_definition]) ).
fof(f30445,plain,
( ~ sQ808_spl
| k2_numbers = k5_ordinal2 ),
inference(component_clause,[status(thm)],[f30444]) ).
fof(f30448,plain,
( ~ sQ808_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f30445,f30383]) ).
fof(f30449,plain,
~ sQ808_spl,
inference(contradiction_clause,[status(thm)],[f30448]) ).
fof(f30491,definition,
( sQ812_spl
<=> m1_subset_1(k8_subset_1(u1_struct_0(k11_conlat_1(sK1656_skl))),u1_struct_0(k11_conlat_1(sK1656_skl))) ),
introduced(definition,[new_symbols(definition,[sQ812_spl])],[split_symbol_definition]) ).
fof(f30493,plain,
( sQ812_spl
| ~ m1_subset_1(k8_subset_1(u1_struct_0(k11_conlat_1(sK1656_skl))),u1_struct_0(k11_conlat_1(sK1656_skl))) ),
inference(component_clause,[status(thm)],[f30491]) ).
fof(f30507,plain,
( sQ812_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f30493,f6479]) ).
fof(f30508,plain,
sQ812_spl,
inference(contradiction_clause,[status(thm)],[f30507]) ).
fof(f30562,definition,
( sQ819_spl
<=> k1_numbers = k5_ordinal2 ),
introduced(definition,[new_symbols(definition,[sQ819_spl])],[split_symbol_definition]) ).
fof(f30563,plain,
( ~ sQ819_spl
| k1_numbers = k5_ordinal2 ),
inference(component_clause,[status(thm)],[f30562]) ).
fof(f30566,plain,
( ~ sQ819_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f30563,f30357]) ).
fof(f30567,plain,
~ sQ819_spl,
inference(contradiction_clause,[status(thm)],[f30566]) ).
fof(f30577,definition,
( sQ821_spl
<=> k1_numbers = k3_numbers ),
introduced(definition,[new_symbols(definition,[sQ821_spl])],[split_symbol_definition]) ).
fof(f30578,plain,
( ~ sQ821_spl
| k1_numbers = k3_numbers ),
inference(component_clause,[status(thm)],[f30577]) ).
fof(f30581,plain,
( ~ sQ821_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f30578,f12375]) ).
fof(f30582,plain,
~ sQ821_spl,
inference(contradiction_clause,[status(thm)],[f30581]) ).
fof(f30687,plain,
( ~ sQ14_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f5554,f24760]) ).
fof(f30690,plain,
~ sQ14_spl,
inference(contradiction_clause,[status(thm)],[f30687]) ).
fof(f30731,definition,
( sQ827_spl
<=> l3_lattices(sK1177_skl) ),
introduced(definition,[new_symbols(definition,[sQ827_spl])],[split_symbol_definition]) ).
fof(f30733,plain,
( sQ827_spl
| ~ l3_lattices(sK1177_skl) ),
inference(component_clause,[status(thm)],[f30731]) ).
fof(f30737,definition,
( sQ829_spl
<=> v10_lattices(sK1177_skl) ),
introduced(definition,[new_symbols(definition,[sQ829_spl])],[split_symbol_definition]) ).
fof(f30739,plain,
( sQ829_spl
| ~ v10_lattices(sK1177_skl) ),
inference(component_clause,[status(thm)],[f30737]) ).
fof(f30755,definition,
( sQ833_spl
<=> v4_lattice3(sK1177_skl) ),
introduced(definition,[new_symbols(definition,[sQ833_spl])],[split_symbol_definition]) ).
fof(f30757,plain,
( sQ833_spl
| ~ v4_lattice3(sK1177_skl) ),
inference(component_clause,[status(thm)],[f30755]) ).
fof(f30760,plain,
( sQ833_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f30757,f18029]) ).
fof(f30761,plain,
sQ833_spl,
inference(contradiction_clause,[status(thm)],[f30760]) ).
fof(f30951,definition,
( sQ860_spl
<=> v10_lattices(sK1114_skl) ),
introduced(definition,[new_symbols(definition,[sQ860_spl])],[split_symbol_definition]) ).
fof(f30953,plain,
( sQ860_spl
| ~ v10_lattices(sK1114_skl) ),
inference(component_clause,[status(thm)],[f30951]) ).
fof(f30980,plain,
( sQ860_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f30953,f17202]) ).
fof(f30981,plain,
sQ860_spl,
inference(contradiction_clause,[status(thm)],[f30980]) ).
fof(f31087,definition,
( sQ883_spl
<=> l3_lattices(sK1113_skl) ),
introduced(definition,[new_symbols(definition,[sQ883_spl])],[split_symbol_definition]) ).
fof(f31089,plain,
( sQ883_spl
| ~ l3_lattices(sK1113_skl) ),
inference(component_clause,[status(thm)],[f31087]) ).
fof(f31092,plain,
( sQ883_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f31089,f17161]) ).
fof(f31093,plain,
sQ883_spl,
inference(contradiction_clause,[status(thm)],[f31092]) ).
fof(f31289,definition,
( sQ917_spl
<=> l3_lattices(sK1079_skl) ),
introduced(definition,[new_symbols(definition,[sQ917_spl])],[split_symbol_definition]) ).
fof(f31291,plain,
( sQ917_spl
| ~ l3_lattices(sK1079_skl) ),
inference(component_clause,[status(thm)],[f31289]) ).
fof(f31294,plain,
( sQ917_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f31291,f16683]) ).
fof(f31295,plain,
sQ917_spl,
inference(contradiction_clause,[status(thm)],[f31294]) ).
fof(f31406,plain,
( sQ435_spl
| ~ sQ724_spl
| ~ m1_subset_1(k15_lattice3(k11_conlat_1(sK1656_skl),sK1657_skl),u1_struct_0(k11_conlat_1(sK1656_skl))) ),
inference(resolution,[status(thm)],[f29735,f26350]) ).
fof(f31470,plain,
( sQ435_spl
| ~ sQ724_spl
| v3_struct_0(k11_conlat_1(sK1656_skl))
| ~ l3_lattices(k11_conlat_1(sK1656_skl)) ),
inference(resolution,[status(thm)],[f31406,f18424]) ).
fof(f31479,plain,
( sQ435_spl
| ~ sQ724_spl
| sQ586_spl
| ~ sQ588_spl ),
inference(split_clause,[status(thm)],[f31470,f28359,f28353,f29734,f26348]) ).
fof(f31534,plain,
( ~ sQ434_spl
| ~ sQ723_spl
| ~ m1_subset_1(k15_lattice3(k11_conlat_1(sK1656_skl),sK1657_skl),u1_struct_0(k11_conlat_1(sK1656_skl))) ),
inference(resolution,[status(thm)],[f29731,f26346]) ).
fof(f31623,plain,
( ~ sQ434_spl
| ~ sQ723_spl
| v3_struct_0(k11_conlat_1(sK1656_skl))
| ~ l3_lattices(k11_conlat_1(sK1656_skl)) ),
inference(resolution,[status(thm)],[f31534,f18424]) ).
fof(f31632,plain,
( ~ sQ434_spl
| ~ sQ723_spl
| sQ586_spl
| ~ sQ588_spl ),
inference(split_clause,[status(thm)],[f31623,f28359,f28353,f29730,f26345]) ).
fof(f31685,definition,
( sQ987_spl
<=> l3_lattices(sK983_skl) ),
introduced(definition,[new_symbols(definition,[sQ987_spl])],[split_symbol_definition]) ).
fof(f31687,plain,
( sQ987_spl
| ~ l3_lattices(sK983_skl) ),
inference(component_clause,[status(thm)],[f31685]) ).
fof(f31690,plain,
( sQ987_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f31687,f15714]) ).
fof(f31691,plain,
sQ987_spl,
inference(contradiction_clause,[status(thm)],[f31690]) ).
fof(f31694,definition,
( sQ988_spl
<=> l3_lattices(sK984_skl) ),
introduced(definition,[new_symbols(definition,[sQ988_spl])],[split_symbol_definition]) ).
fof(f31696,plain,
( sQ988_spl
| ~ l3_lattices(sK984_skl) ),
inference(component_clause,[status(thm)],[f31694]) ).
fof(f31699,plain,
( sQ988_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f31696,f15736]) ).
fof(f31700,plain,
sQ988_spl,
inference(contradiction_clause,[status(thm)],[f31699]) ).
fof(f31760,definition,
( sQ999_spl
<=> v10_lattices(sK986_skl) ),
introduced(definition,[new_symbols(definition,[sQ999_spl])],[split_symbol_definition]) ).
fof(f31762,plain,
( sQ999_spl
| ~ v10_lattices(sK986_skl) ),
inference(component_clause,[status(thm)],[f31760]) ).
fof(f31789,plain,
( sQ999_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f31762,f15784]) ).
fof(f31790,plain,
sQ999_spl,
inference(contradiction_clause,[status(thm)],[f31789]) ).
fof(f31824,definition,
( sQ1008_spl
<=> v10_lattices(sK985_skl) ),
introduced(definition,[new_symbols(definition,[sQ1008_spl])],[split_symbol_definition]) ).
fof(f31826,plain,
( sQ1008_spl
| ~ v10_lattices(sK985_skl) ),
inference(component_clause,[status(thm)],[f31824]) ).
fof(f31850,plain,
( sQ1008_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f31826,f15759]) ).
fof(f31851,plain,
sQ1008_spl,
inference(contradiction_clause,[status(thm)],[f31850]) ).
fof(f31852,plain,
( sQ436_spl
| ~ sQ722_spl
| ~ m1_subset_1(k15_lattice3(k11_conlat_1(sK1656_skl),sK1657_skl),u1_struct_0(k11_conlat_1(sK1656_skl))) ),
inference(resolution,[status(thm)],[f29726,f26353]) ).
fof(f31874,definition,
( sQ1017_spl
<=> v10_lattices(sK982_skl) ),
introduced(definition,[new_symbols(definition,[sQ1017_spl])],[split_symbol_definition]) ).
fof(f31876,plain,
( sQ1017_spl
| ~ v10_lattices(sK982_skl) ),
inference(component_clause,[status(thm)],[f31874]) ).
fof(f31900,plain,
( sQ1017_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f31876,f15712]) ).
fof(f31901,plain,
sQ1017_spl,
inference(contradiction_clause,[status(thm)],[f31900]) ).
fof(f32056,plain,
( sQ436_spl
| ~ sQ722_spl
| v3_struct_0(k11_conlat_1(sK1656_skl))
| ~ l3_lattices(k11_conlat_1(sK1656_skl)) ),
inference(resolution,[status(thm)],[f31852,f18424]) ).
fof(f32065,plain,
( sQ436_spl
| ~ sQ722_spl
| sQ586_spl
| ~ sQ588_spl ),
inference(split_clause,[status(thm)],[f32056,f28359,f28353,f29725,f26351]) ).
fof(f32074,definition,
( sQ1057_spl
<=> l3_lattices(sK1026_skl) ),
introduced(definition,[new_symbols(definition,[sQ1057_spl])],[split_symbol_definition]) ).
fof(f32076,plain,
( sQ1057_spl
| ~ l3_lattices(sK1026_skl) ),
inference(component_clause,[status(thm)],[f32074]) ).
fof(f32094,plain,
( sQ1057_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f32076,f16019]) ).
fof(f32095,plain,
sQ1057_spl,
inference(contradiction_clause,[status(thm)],[f32094]) ).
fof(f32150,plain,
( sQ827_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f30733,f18019]) ).
fof(f32151,plain,
sQ827_spl,
inference(contradiction_clause,[status(thm)],[f32150]) ).
fof(f32152,plain,
( sQ433_spl
| ~ sQ734_spl
| ~ m1_subset_1(k16_lattice3(k11_conlat_1(sK1656_skl),sK1657_skl),u1_struct_0(k11_conlat_1(sK1656_skl))) ),
inference(resolution,[status(thm)],[f29793,f26344]) ).
fof(f32164,plain,
( sQ433_spl
| ~ sQ734_spl
| ~ l3_lattices(k11_conlat_1(sK1656_skl))
| v3_struct_0(k11_conlat_1(sK1656_skl)) ),
inference(resolution,[status(thm)],[f32152,f18427]) ).
fof(f32173,plain,
( sQ433_spl
| ~ sQ734_spl
| ~ sQ588_spl
| sQ586_spl ),
inference(split_clause,[status(thm)],[f32164,f28353,f28359,f29792,f26342]) ).
fof(f32209,plain,
( sQ829_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f30739,f18028]) ).
fof(f32210,plain,
sQ829_spl,
inference(contradiction_clause,[status(thm)],[f32209]) ).
fof(f32261,plain,
( sQ432_spl
| ~ sQ733_spl
| ~ m1_subset_1(k16_lattice3(k11_conlat_1(sK1656_skl),sK1657_skl),u1_struct_0(k11_conlat_1(sK1656_skl))) ),
inference(resolution,[status(thm)],[f29789,f26341]) ).
fof(f32346,plain,
( sQ432_spl
| ~ sQ733_spl
| ~ l3_lattices(k11_conlat_1(sK1656_skl))
| v3_struct_0(k11_conlat_1(sK1656_skl)) ),
inference(resolution,[status(thm)],[f32261,f18427]) ).
fof(f32355,plain,
( sQ432_spl
| ~ sQ733_spl
| ~ sQ588_spl
| sQ586_spl ),
inference(split_clause,[status(thm)],[f32346,f28353,f28359,f29788,f26339]) ).
fof(f32381,plain,
( ~ sQ431_spl
| ~ sQ731_spl
| ~ m1_subset_1(k16_lattice3(k11_conlat_1(sK1656_skl),sK1657_skl),u1_struct_0(k11_conlat_1(sK1656_skl))) ),
inference(resolution,[status(thm)],[f29781,f26337]) ).
fof(f32430,definition,
( sQ1101_spl
<=> l3_lattices(sK979_skl) ),
introduced(definition,[new_symbols(definition,[sQ1101_spl])],[split_symbol_definition]) ).
fof(f32432,plain,
( sQ1101_spl
| ~ l3_lattices(sK979_skl) ),
inference(component_clause,[status(thm)],[f32430]) ).
fof(f32450,plain,
( sQ1101_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f32432,f15676]) ).
fof(f32451,plain,
sQ1101_spl,
inference(contradiction_clause,[status(thm)],[f32450]) ).
fof(f32510,plain,
( ~ sQ431_spl
| ~ sQ731_spl
| ~ l3_lattices(k11_conlat_1(sK1656_skl))
| v3_struct_0(k11_conlat_1(sK1656_skl)) ),
inference(resolution,[status(thm)],[f32381,f18427]) ).
fof(f32519,plain,
( ~ sQ431_spl
| ~ sQ731_spl
| ~ sQ588_spl
| sQ586_spl ),
inference(split_clause,[status(thm)],[f32510,f28353,f28359,f29780,f26336]) ).
fof(f32520,plain,
$false,
inference(sat_refutation,[status(thm)],[f26354,f28339,f28405,f28411,f28418,f29175,f29205,f29327,f29428,f29552,f29617,f29669,f29678,f29699,f29703,f29728,f29733,f29737,f29783,f29791,f29795,f29823,f29917,f29919,f30034,f30171,f30204,f30307,f30348,f30433,f30449,f30508,f30567,f30582,f30690,f30761,f30981,f31093,f31295,f31479,f31632,f31691,f31700,f31790,f31851,f31901,f32065,f32095,f32151,f32173,f32210,f32355,f32451,f32519]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT338+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.34 % Computer : n003.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.34 % CPULimit : 300
% 0.08/0.34 % WCLimit : 300
% 0.08/0.34 % DateTime : Sun Sep 20 23:44:01 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.67/0.94 % Drodi V4.1.1
% 242.11/31.62 % Refutation found
% 242.11/31.62 % SZS status Theorem for theBenchmark: Theorem is valid
% 242.11/31.62 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 78.49/31.90 % Elapsed time: 31.523027 seconds
% 78.49/31.90 % CPU time: 243.719109 seconds
% 78.49/31.90 % Total memory used: 1.345 GB
% 78.49/31.90 % Net memory used: 1.280 GB
%------------------------------------------------------------------------------