%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LAT295+4 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n002.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 01:02:36 PM UTC 2026
% Result : Theorem 39.67s 14.49s
% Output : CNFRefutation 42.95s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 39
% Syntax : Number of formulae : 183 ( 24 unt; 37 def)
% Number of atoms : 799 ( 147 equ)
% Maximal formula atoms : 17 ( 4 avg)
% Number of connectives : 1053 ( 437 ~; 486 |; 63 &)
% ( 37 <=>; 30 =>; 0 <=; 0 <~>)
% Maximal formula depth : 23 ( 6 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 43 ( 41 usr; 37 prp; 0-6 aty)
% Number of functors : 12 ( 12 usr; 6 con; 0-3 aty)
% Number of variables : 188 ( 176 !; 12 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f33839,axiom,
! [A] :
( ( l3_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( l3_lattices(B)
& ~ v3_struct_0(B) )
=> ( g3_lattices(u1_struct_0(A),u2_lattices(A),u1_lattices(A)) = g3_lattices(u1_struct_0(B),u2_lattices(B),u1_lattices(B))
=> ! [C] :
( m1_subset_1(C,u1_struct_0(A))
=> ! [D] :
( m1_subset_1(D,u1_struct_0(A))
=> ! [E] :
( m1_subset_1(E,u1_struct_0(B))
=> ! [F] :
( m1_subset_1(F,u1_struct_0(B))
=> ( ( D = F
& C = E )
=> ( ( r1_lattices(B,E,F)
=> r1_lattices(A,C,D) )
& ( r1_lattices(A,C,D)
=> r1_lattices(B,E,F) )
& k2_lattices(A,C,D) = k2_lattices(B,E,F)
& k1_lattices(A,C,D) = k1_lattices(B,E,F) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f34658,conjecture,
! [A] :
( ( l3_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( l3_lattices(B)
& ~ v3_struct_0(B) )
=> ( g3_lattices(u1_struct_0(A),u2_lattices(A),u1_lattices(A)) = g3_lattices(u1_struct_0(B),u2_lattices(B),u1_lattices(B))
=> ! [C] :
( m1_subset_1(C,u1_struct_0(A))
=> ! [D] :
( m1_subset_1(D,u1_struct_0(A))
=> ! [E] :
( m1_subset_1(E,u1_struct_0(B))
=> ! [F] :
( m1_subset_1(F,u1_struct_0(B))
=> ( ( D = F
& C = E )
=> ( ( r1_lattices(B,E,F)
=> r1_lattices(A,C,D) )
& ( r1_lattices(A,C,D)
=> r1_lattices(B,E,F) )
& k2_lattices(A,C,D) = k2_lattices(B,E,F)
& k1_lattices(A,C,D) = k1_lattices(B,E,F) ) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f34659,negated_conjecture,
~ ! [A] :
( ( l3_lattices(A)
& ~ v3_struct_0(A) )
=> ! [B] :
( ( l3_lattices(B)
& ~ v3_struct_0(B) )
=> ( g3_lattices(u1_struct_0(A),u2_lattices(A),u1_lattices(A)) = g3_lattices(u1_struct_0(B),u2_lattices(B),u1_lattices(B))
=> ! [C] :
( m1_subset_1(C,u1_struct_0(A))
=> ! [D] :
( m1_subset_1(D,u1_struct_0(A))
=> ! [E] :
( m1_subset_1(E,u1_struct_0(B))
=> ! [F] :
( m1_subset_1(F,u1_struct_0(B))
=> ( ( D = F
& C = E )
=> ( ( r1_lattices(B,E,F)
=> r1_lattices(A,C,D) )
& ( r1_lattices(A,C,D)
=> r1_lattices(B,E,F) )
& k2_lattices(A,C,D) = k2_lattices(B,E,F)
& k1_lattices(A,C,D) = k1_lattices(B,E,F) ) ) ) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f34658]) ).
fof(f150608,plain,
! [A] :
( ! [B] :
( ! [C] :
( ! [D] :
( ! [E] :
( ! [F] :
( ( ( r1_lattices(A,C,D)
| ~ r1_lattices(B,E,F) )
& ( r1_lattices(B,E,F)
| ~ r1_lattices(A,C,D) )
& k2_lattices(A,C,D) = k2_lattices(B,E,F)
& k1_lattices(A,C,D) = k1_lattices(B,E,F) )
| D != F
| C != E
| ~ m1_subset_1(F,u1_struct_0(B)) )
| ~ m1_subset_1(E,u1_struct_0(B)) )
| ~ m1_subset_1(D,u1_struct_0(A)) )
| ~ m1_subset_1(C,u1_struct_0(A)) )
| g3_lattices(u1_struct_0(A),u2_lattices(A),u1_lattices(A)) != g3_lattices(u1_struct_0(B),u2_lattices(B),u1_lattices(B))
| ~ l3_lattices(B)
| v3_struct_0(B) )
| ~ l3_lattices(A)
| v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f33839]) ).
fof(f150609,plain,
! [X0,X1,X2,X3,X4,X5] :
( k1_lattices(X0,X2,X3) = k1_lattices(X1,X4,X5)
| X3 != X5
| X2 != X4
| ~ m1_subset_1(X5,u1_struct_0(X1))
| ~ m1_subset_1(X4,u1_struct_0(X1))
| ~ m1_subset_1(X3,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) != g3_lattices(u1_struct_0(X1),u2_lattices(X1),u1_lattices(X1))
| ~ l3_lattices(X1)
| v3_struct_0(X1)
| ~ l3_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f150608]) ).
fof(f150610,plain,
! [X0,X1,X2,X3,X4,X5] :
( k2_lattices(X0,X2,X3) = k2_lattices(X1,X4,X5)
| X3 != X5
| X2 != X4
| ~ m1_subset_1(X5,u1_struct_0(X1))
| ~ m1_subset_1(X4,u1_struct_0(X1))
| ~ m1_subset_1(X3,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) != g3_lattices(u1_struct_0(X1),u2_lattices(X1),u1_lattices(X1))
| ~ l3_lattices(X1)
| v3_struct_0(X1)
| ~ l3_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f150608]) ).
fof(f150611,plain,
! [X0,X1,X2,X3,X4,X5] :
( r1_lattices(X1,X4,X5)
| ~ r1_lattices(X0,X2,X3)
| X3 != X5
| X2 != X4
| ~ m1_subset_1(X5,u1_struct_0(X1))
| ~ m1_subset_1(X4,u1_struct_0(X1))
| ~ m1_subset_1(X3,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) != g3_lattices(u1_struct_0(X1),u2_lattices(X1),u1_lattices(X1))
| ~ l3_lattices(X1)
| v3_struct_0(X1)
| ~ l3_lattices(X0)
| v3_struct_0(X0) ),
inference(cnf_transformation,[status(thm)],[f150608]) ).
fof(f153989,plain,
? [A] :
( ? [B] :
( ? [C] :
( ? [D] :
( ? [E] :
( ? [F] :
( ( ( ~ r1_lattices(A,C,D)
& r1_lattices(B,E,F) )
| ( ~ r1_lattices(B,E,F)
& r1_lattices(A,C,D) )
| k2_lattices(A,C,D) != k2_lattices(B,E,F)
| k1_lattices(A,C,D) != k1_lattices(B,E,F) )
& D = F
& C = E
& m1_subset_1(F,u1_struct_0(B)) )
& m1_subset_1(E,u1_struct_0(B)) )
& m1_subset_1(D,u1_struct_0(A)) )
& m1_subset_1(C,u1_struct_0(A)) )
& g3_lattices(u1_struct_0(A),u2_lattices(A),u1_lattices(A)) = g3_lattices(u1_struct_0(B),u2_lattices(B),u1_lattices(B))
& l3_lattices(B)
& ~ v3_struct_0(B) )
& l3_lattices(A)
& ~ v3_struct_0(A) ),
inference(pre_NNF_transformation,[status(thm)],[f34659]) ).
fof(f153990,definition,
! [A,B,C,D,E,F] :
( sP1325_prd(F,E,D,C,B,A)
<=> ( ~ r1_lattices(B,E,F)
& r1_lattices(A,C,D) ) ),
introduced(definition,[new_symbols(definition,[sP1325_prd])],[]) ).
fof(f153991,plain,
? [A] :
( ? [B] :
( ? [C] :
( ? [D] :
( ? [E] :
( ? [F] :
( ( ( ~ r1_lattices(A,C,D)
& r1_lattices(B,E,F) )
| sP1325_prd(F,E,D,C,B,A)
| k2_lattices(A,C,D) != k2_lattices(B,E,F)
| k1_lattices(A,C,D) != k1_lattices(B,E,F) )
& D = F
& C = E
& m1_subset_1(F,u1_struct_0(B)) )
& m1_subset_1(E,u1_struct_0(B)) )
& m1_subset_1(D,u1_struct_0(A)) )
& m1_subset_1(C,u1_struct_0(A)) )
& g3_lattices(u1_struct_0(A),u2_lattices(A),u1_lattices(A)) = g3_lattices(u1_struct_0(B),u2_lattices(B),u1_lattices(B))
& l3_lattices(B)
& ~ v3_struct_0(B) )
& l3_lattices(A)
& ~ v3_struct_0(A) ),
inference(formula_renaming,[status(thm)],[f153989,f153990]) ).
fof(f153992,plain,
( ( ( ~ r1_lattices(sK12109_skl,sK12111_skl,sK12112_skl)
& r1_lattices(sK12110_skl,sK12113_skl,sK12114_skl) )
| sP1325_prd(sK12114_skl,sK12113_skl,sK12112_skl,sK12111_skl,sK12110_skl,sK12109_skl)
| k2_lattices(sK12109_skl,sK12111_skl,sK12112_skl) != k2_lattices(sK12110_skl,sK12113_skl,sK12114_skl)
| k1_lattices(sK12109_skl,sK12111_skl,sK12112_skl) != k1_lattices(sK12110_skl,sK12113_skl,sK12114_skl) )
& sK12112_skl = sK12114_skl
& sK12111_skl = sK12113_skl
& m1_subset_1(sK12114_skl,u1_struct_0(sK12110_skl))
& m1_subset_1(sK12113_skl,u1_struct_0(sK12110_skl))
& m1_subset_1(sK12112_skl,u1_struct_0(sK12109_skl))
& m1_subset_1(sK12111_skl,u1_struct_0(sK12109_skl))
& g3_lattices(u1_struct_0(sK12109_skl),u2_lattices(sK12109_skl),u1_lattices(sK12109_skl)) = g3_lattices(u1_struct_0(sK12110_skl),u2_lattices(sK12110_skl),u1_lattices(sK12110_skl))
& l3_lattices(sK12110_skl)
& ~ v3_struct_0(sK12110_skl)
& l3_lattices(sK12109_skl)
& ~ v3_struct_0(sK12109_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12109_skl,sK12110_skl,sK12111_skl,sK12112_skl,sK12113_skl,sK12114_skl]),skolemize(A,sK12109_skl),skolemize(B,sK12110_skl),skolemize(C,sK12111_skl),skolemize(D,sK12112_skl),skolemize(E,sK12113_skl),skolemize(F,sK12114_skl)],[f153991]) ).
fof(f153993,plain,
~ v3_struct_0(sK12109_skl),
inference(cnf_transformation,[status(thm)],[f153992]) ).
fof(f153994,plain,
l3_lattices(sK12109_skl),
inference(cnf_transformation,[status(thm)],[f153992]) ).
fof(f153995,plain,
~ v3_struct_0(sK12110_skl),
inference(cnf_transformation,[status(thm)],[f153992]) ).
fof(f153996,plain,
l3_lattices(sK12110_skl),
inference(cnf_transformation,[status(thm)],[f153992]) ).
fof(f153997,plain,
g3_lattices(u1_struct_0(sK12109_skl),u2_lattices(sK12109_skl),u1_lattices(sK12109_skl)) = g3_lattices(u1_struct_0(sK12110_skl),u2_lattices(sK12110_skl),u1_lattices(sK12110_skl)),
inference(cnf_transformation,[status(thm)],[f153992]) ).
fof(f153998,plain,
m1_subset_1(sK12111_skl,u1_struct_0(sK12109_skl)),
inference(cnf_transformation,[status(thm)],[f153992]) ).
fof(f153999,plain,
m1_subset_1(sK12112_skl,u1_struct_0(sK12109_skl)),
inference(cnf_transformation,[status(thm)],[f153992]) ).
fof(f154000,plain,
m1_subset_1(sK12113_skl,u1_struct_0(sK12110_skl)),
inference(cnf_transformation,[status(thm)],[f153992]) ).
fof(f154001,plain,
m1_subset_1(sK12114_skl,u1_struct_0(sK12110_skl)),
inference(cnf_transformation,[status(thm)],[f153992]) ).
fof(f154002,plain,
sK12111_skl = sK12113_skl,
inference(cnf_transformation,[status(thm)],[f153992]) ).
fof(f154003,plain,
sK12112_skl = sK12114_skl,
inference(cnf_transformation,[status(thm)],[f153992]) ).
fof(f154004,plain,
( r1_lattices(sK12110_skl,sK12113_skl,sK12114_skl)
| sP1325_prd(sK12114_skl,sK12113_skl,sK12112_skl,sK12111_skl,sK12110_skl,sK12109_skl)
| k2_lattices(sK12109_skl,sK12111_skl,sK12112_skl) != k2_lattices(sK12110_skl,sK12113_skl,sK12114_skl)
| k1_lattices(sK12109_skl,sK12111_skl,sK12112_skl) != k1_lattices(sK12110_skl,sK12113_skl,sK12114_skl) ),
inference(cnf_transformation,[status(thm)],[f153992]) ).
fof(f154005,plain,
( ~ r1_lattices(sK12109_skl,sK12111_skl,sK12112_skl)
| sP1325_prd(sK12114_skl,sK12113_skl,sK12112_skl,sK12111_skl,sK12110_skl,sK12109_skl)
| k2_lattices(sK12109_skl,sK12111_skl,sK12112_skl) != k2_lattices(sK12110_skl,sK12113_skl,sK12114_skl)
| k1_lattices(sK12109_skl,sK12111_skl,sK12112_skl) != k1_lattices(sK12110_skl,sK12113_skl,sK12114_skl) ),
inference(cnf_transformation,[status(thm)],[f153992]) ).
fof(f164089,plain,
! [A,B,C,D,E,F] :
( ( r1_lattices(B,E,F)
| ~ r1_lattices(A,C,D)
| sP1325_prd(F,E,D,C,B,A) )
& ( ( ~ r1_lattices(B,E,F)
& r1_lattices(A,C,D) )
| ~ sP1325_prd(F,E,D,C,B,A) ) ),
inference(NNF_transformation,[status(thm)],[f153990]) ).
fof(f164090,plain,
( ! [A,B,C,D,E,F] :
( r1_lattices(B,E,F)
| ~ r1_lattices(A,C,D)
| sP1325_prd(F,E,D,C,B,A) )
& ! [A,B,C,D,E,F] :
( ( ~ r1_lattices(B,E,F)
& r1_lattices(A,C,D) )
| ~ sP1325_prd(F,E,D,C,B,A) ) ),
inference(miniscoping,[status(thm)],[f164089]) ).
fof(f164091,plain,
! [X0,X1,X2,X3,X4,X5] :
( r1_lattices(X5,X3,X2)
| ~ sP1325_prd(X0,X1,X2,X3,X4,X5) ),
inference(cnf_transformation,[status(thm)],[f164090]) ).
fof(f164092,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ r1_lattices(X4,X1,X0)
| ~ sP1325_prd(X0,X1,X2,X3,X4,X5) ),
inference(cnf_transformation,[status(thm)],[f164090]) ).
fof(f180671,definition,
( sQ2282_spl
<=> k1_lattices(sK12109_skl,sK12111_skl,sK12112_skl) = k1_lattices(sK12110_skl,sK12113_skl,sK12114_skl) ),
introduced(definition,[new_symbols(definition,[sQ2282_spl])],[split_symbol_definition]) ).
fof(f180673,plain,
( sQ2282_spl
| k1_lattices(sK12109_skl,sK12111_skl,sK12112_skl) != k1_lattices(sK12110_skl,sK12113_skl,sK12114_skl) ),
inference(component_clause,[status(thm)],[f180671]) ).
fof(f180674,definition,
( sQ2283_spl
<=> k2_lattices(sK12109_skl,sK12111_skl,sK12112_skl) = k2_lattices(sK12110_skl,sK12113_skl,sK12114_skl) ),
introduced(definition,[new_symbols(definition,[sQ2283_spl])],[split_symbol_definition]) ).
fof(f180676,plain,
( sQ2283_spl
| k2_lattices(sK12109_skl,sK12111_skl,sK12112_skl) != k2_lattices(sK12110_skl,sK12113_skl,sK12114_skl) ),
inference(component_clause,[status(thm)],[f180674]) ).
fof(f180677,definition,
( sQ2284_spl
<=> sP1325_prd(sK12114_skl,sK12113_skl,sK12112_skl,sK12111_skl,sK12110_skl,sK12109_skl) ),
introduced(definition,[new_symbols(definition,[sQ2284_spl])],[split_symbol_definition]) ).
fof(f180678,plain,
( ~ sQ2284_spl
| sP1325_prd(sK12114_skl,sK12113_skl,sK12112_skl,sK12111_skl,sK12110_skl,sK12109_skl) ),
inference(component_clause,[status(thm)],[f180677]) ).
fof(f180680,definition,
( sQ2285_spl
<=> r1_lattices(sK12110_skl,sK12113_skl,sK12114_skl) ),
introduced(definition,[new_symbols(definition,[sQ2285_spl])],[split_symbol_definition]) ).
fof(f180681,plain,
( ~ sQ2285_spl
| r1_lattices(sK12110_skl,sK12113_skl,sK12114_skl) ),
inference(component_clause,[status(thm)],[f180680]) ).
fof(f180683,plain,
( sQ2285_spl
| sQ2284_spl
| ~ sQ2283_spl
| ~ sQ2282_spl ),
inference(split_clause,[status(thm)],[f154004,f180671,f180674,f180677,f180680]) ).
fof(f180684,definition,
( sQ2286_spl
<=> r1_lattices(sK12109_skl,sK12111_skl,sK12112_skl) ),
introduced(definition,[new_symbols(definition,[sQ2286_spl])],[split_symbol_definition]) ).
fof(f180686,plain,
( sQ2286_spl
| ~ r1_lattices(sK12109_skl,sK12111_skl,sK12112_skl) ),
inference(component_clause,[status(thm)],[f180684]) ).
fof(f180687,plain,
( ~ sQ2286_spl
| sQ2284_spl
| ~ sQ2283_spl
| ~ sQ2282_spl ),
inference(split_clause,[status(thm)],[f154005,f180671,f180674,f180677,f180684]) ).
fof(f190800,plain,
! [X0,X1,X2,X3] :
( k1_lattices(X0,X2,X3) = k1_lattices(X1,X2,X3)
| ~ m1_subset_1(X3,u1_struct_0(X1))
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ m1_subset_1(X3,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) != g3_lattices(u1_struct_0(X1),u2_lattices(X1),u1_lattices(X1))
| ~ l3_lattices(X1)
| v3_struct_0(X1)
| ~ l3_lattices(X0)
| v3_struct_0(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f150609]) ).
fof(f190801,plain,
! [X0,X1,X2,X3] :
( k2_lattices(X0,X2,X3) = k2_lattices(X1,X2,X3)
| ~ m1_subset_1(X3,u1_struct_0(X1))
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ m1_subset_1(X3,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) != g3_lattices(u1_struct_0(X1),u2_lattices(X1),u1_lattices(X1))
| ~ l3_lattices(X1)
| v3_struct_0(X1)
| ~ l3_lattices(X0)
| v3_struct_0(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f150610]) ).
fof(f190802,plain,
! [X0,X1,X2,X3] :
( r1_lattices(X1,X2,X3)
| ~ r1_lattices(X0,X2,X3)
| ~ m1_subset_1(X3,u1_struct_0(X1))
| ~ m1_subset_1(X2,u1_struct_0(X1))
| ~ m1_subset_1(X3,u1_struct_0(X0))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) != g3_lattices(u1_struct_0(X1),u2_lattices(X1),u1_lattices(X1))
| ~ l3_lattices(X1)
| v3_struct_0(X1)
| ~ l3_lattices(X0)
| v3_struct_0(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f150611]) ).
fof(f192027,plain,
m1_subset_1(sK12111_skl,u1_struct_0(sK12110_skl)),
inference(forward_demodulation,[status(thm)],[f154002,f154000]) ).
fof(f192028,plain,
m1_subset_1(sK12112_skl,u1_struct_0(sK12110_skl)),
inference(forward_demodulation,[status(thm)],[f154003,f154001]) ).
fof(f192029,plain,
( ~ sQ2285_spl
| r1_lattices(sK12110_skl,sK12111_skl,sK12114_skl) ),
inference(forward_demodulation,[status(thm)],[f154002,f180681]) ).
fof(f192030,plain,
( ~ sQ2285_spl
| r1_lattices(sK12110_skl,sK12111_skl,sK12112_skl) ),
inference(forward_demodulation,[status(thm)],[f154003,f192029]) ).
fof(f192033,plain,
( ~ sQ2284_spl
| sP1325_prd(sK12112_skl,sK12113_skl,sK12112_skl,sK12111_skl,sK12110_skl,sK12109_skl) ),
inference(forward_demodulation,[status(thm)],[f154003,f180678]) ).
fof(f192034,plain,
( ~ sQ2284_spl
| sP1325_prd(sK12112_skl,sK12111_skl,sK12112_skl,sK12111_skl,sK12110_skl,sK12109_skl) ),
inference(forward_demodulation,[status(thm)],[f154002,f192033]) ).
fof(f192035,plain,
( ~ sQ2284_spl
| ~ r1_lattices(sK12110_skl,sK12111_skl,sK12112_skl) ),
inference(resolution,[status(thm)],[f192034,f164092]) ).
fof(f192036,plain,
( ~ sQ2284_spl
| r1_lattices(sK12109_skl,sK12111_skl,sK12112_skl) ),
inference(resolution,[status(thm)],[f192034,f164091]) ).
fof(f192047,plain,
( sQ2283_spl
| k2_lattices(sK12109_skl,sK12111_skl,sK12112_skl) != k2_lattices(sK12110_skl,sK12111_skl,sK12114_skl) ),
inference(forward_demodulation,[status(thm)],[f154002,f180676]) ).
fof(f192048,plain,
( sQ2283_spl
| k2_lattices(sK12109_skl,sK12111_skl,sK12112_skl) != k2_lattices(sK12110_skl,sK12111_skl,sK12112_skl) ),
inference(forward_demodulation,[status(thm)],[f154003,f192047]) ).
fof(f192049,plain,
( sQ2282_spl
| k1_lattices(sK12109_skl,sK12111_skl,sK12112_skl) != k1_lattices(sK12110_skl,sK12111_skl,sK12114_skl) ),
inference(forward_demodulation,[status(thm)],[f154002,f180673]) ).
fof(f192050,plain,
( sQ2282_spl
| k1_lattices(sK12109_skl,sK12111_skl,sK12112_skl) != k1_lattices(sK12110_skl,sK12111_skl,sK12112_skl) ),
inference(forward_demodulation,[status(thm)],[f154003,f192049]) ).
fof(f192051,plain,
! [X0,X1,X2] :
( k1_lattices(X0,X1,X2) = k1_lattices(sK12110_skl,X1,X2)
| ~ m1_subset_1(X2,u1_struct_0(sK12110_skl))
| ~ m1_subset_1(X1,u1_struct_0(sK12110_skl))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) != g3_lattices(u1_struct_0(sK12110_skl),u2_lattices(sK12110_skl),u1_lattices(sK12110_skl))
| v3_struct_0(sK12110_skl)
| ~ l3_lattices(X0)
| v3_struct_0(X0) ),
inference(resolution,[status(thm)],[f190800,f153996]) ).
fof(f192052,plain,
! [X0,X1,X2] :
( k1_lattices(X0,X1,X2) = k1_lattices(sK12109_skl,X1,X2)
| ~ m1_subset_1(X2,u1_struct_0(sK12109_skl))
| ~ m1_subset_1(X1,u1_struct_0(sK12109_skl))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) != g3_lattices(u1_struct_0(sK12109_skl),u2_lattices(sK12109_skl),u1_lattices(sK12109_skl))
| v3_struct_0(sK12109_skl)
| ~ l3_lattices(X0)
| v3_struct_0(X0) ),
inference(resolution,[status(thm)],[f190800,f153994]) ).
fof(f192053,definition,
! [X0,X1,X2] :
( sQ2905_spl
<=> ( k1_lattices(X0,X1,X2) = k1_lattices(sK12110_skl,X1,X2)
| ~ m1_subset_1(X2,u1_struct_0(sK12110_skl))
| ~ m1_subset_1(X1,u1_struct_0(sK12110_skl))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) != g3_lattices(u1_struct_0(sK12110_skl),u2_lattices(sK12110_skl),u1_lattices(sK12110_skl))
| ~ l3_lattices(X0)
| v3_struct_0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ2905_spl])],[split_symbol_definition]) ).
fof(f192054,plain,
! [X0,X1,X2] :
( ~ sQ2905_spl
| k1_lattices(X0,X1,X2) = k1_lattices(sK12110_skl,X1,X2)
| ~ m1_subset_1(X2,u1_struct_0(sK12110_skl))
| ~ m1_subset_1(X1,u1_struct_0(sK12110_skl))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) != g3_lattices(u1_struct_0(sK12110_skl),u2_lattices(sK12110_skl),u1_lattices(sK12110_skl))
| ~ l3_lattices(X0)
| v3_struct_0(X0) ),
inference(component_clause,[status(thm)],[f192053]) ).
fof(f192056,definition,
( sQ2906_spl
<=> v3_struct_0(sK12110_skl) ),
introduced(definition,[new_symbols(definition,[sQ2906_spl])],[split_symbol_definition]) ).
fof(f192057,plain,
( ~ sQ2906_spl
| v3_struct_0(sK12110_skl) ),
inference(component_clause,[status(thm)],[f192056]) ).
fof(f192059,plain,
( sQ2906_spl
| sQ2905_spl ),
inference(split_clause,[status(thm)],[f192051,f192053,f192056]) ).
fof(f192060,definition,
! [X0,X1,X2] :
( sQ2907_spl
<=> ( k1_lattices(X0,X1,X2) = k1_lattices(sK12109_skl,X1,X2)
| ~ m1_subset_1(X2,u1_struct_0(sK12109_skl))
| ~ m1_subset_1(X1,u1_struct_0(sK12109_skl))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) != g3_lattices(u1_struct_0(sK12109_skl),u2_lattices(sK12109_skl),u1_lattices(sK12109_skl))
| ~ l3_lattices(X0)
| v3_struct_0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ2907_spl])],[split_symbol_definition]) ).
fof(f192061,plain,
! [X0,X1,X2] :
( ~ sQ2907_spl
| k1_lattices(X0,X1,X2) = k1_lattices(sK12109_skl,X1,X2)
| ~ m1_subset_1(X2,u1_struct_0(sK12109_skl))
| ~ m1_subset_1(X1,u1_struct_0(sK12109_skl))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) != g3_lattices(u1_struct_0(sK12109_skl),u2_lattices(sK12109_skl),u1_lattices(sK12109_skl))
| ~ l3_lattices(X0)
| v3_struct_0(X0) ),
inference(component_clause,[status(thm)],[f192060]) ).
fof(f192063,definition,
( sQ2908_spl
<=> v3_struct_0(sK12109_skl) ),
introduced(definition,[new_symbols(definition,[sQ2908_spl])],[split_symbol_definition]) ).
fof(f192064,plain,
( ~ sQ2908_spl
| v3_struct_0(sK12109_skl) ),
inference(component_clause,[status(thm)],[f192063]) ).
fof(f192066,plain,
( sQ2908_spl
| sQ2907_spl ),
inference(split_clause,[status(thm)],[f192052,f192060,f192063]) ).
fof(f192067,plain,
! [X0,X1,X2] :
( ~ sQ2905_spl
| k1_lattices(X0,X1,X2) = k1_lattices(sK12110_skl,X1,X2)
| ~ m1_subset_1(X2,u1_struct_0(sK12110_skl))
| ~ m1_subset_1(X1,u1_struct_0(sK12110_skl))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) != g3_lattices(u1_struct_0(sK12109_skl),u2_lattices(sK12109_skl),u1_lattices(sK12109_skl))
| ~ l3_lattices(X0)
| v3_struct_0(X0) ),
inference(forward_demodulation,[status(thm)],[f153997,f192054]) ).
fof(f192068,plain,
( ~ sQ2908_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f192064,f153993]) ).
fof(f192069,plain,
~ sQ2908_spl,
inference(contradiction_clause,[status(thm)],[f192068]) ).
fof(f192070,plain,
( ~ sQ2906_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f192057,f153995]) ).
fof(f192071,plain,
~ sQ2906_spl,
inference(contradiction_clause,[status(thm)],[f192070]) ).
fof(f192072,plain,
! [X0,X1,X2] :
( k2_lattices(X0,X1,X2) = k2_lattices(sK12110_skl,X1,X2)
| ~ m1_subset_1(X2,u1_struct_0(sK12110_skl))
| ~ m1_subset_1(X1,u1_struct_0(sK12110_skl))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) != g3_lattices(u1_struct_0(sK12110_skl),u2_lattices(sK12110_skl),u1_lattices(sK12110_skl))
| v3_struct_0(sK12110_skl)
| ~ l3_lattices(X0)
| v3_struct_0(X0) ),
inference(resolution,[status(thm)],[f190801,f153996]) ).
fof(f192073,plain,
! [X0,X1,X2] :
( k2_lattices(X0,X1,X2) = k2_lattices(sK12109_skl,X1,X2)
| ~ m1_subset_1(X2,u1_struct_0(sK12109_skl))
| ~ m1_subset_1(X1,u1_struct_0(sK12109_skl))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) != g3_lattices(u1_struct_0(sK12109_skl),u2_lattices(sK12109_skl),u1_lattices(sK12109_skl))
| v3_struct_0(sK12109_skl)
| ~ l3_lattices(X0)
| v3_struct_0(X0) ),
inference(resolution,[status(thm)],[f190801,f153994]) ).
fof(f192074,definition,
! [X0,X1,X2] :
( sQ2909_spl
<=> ( k2_lattices(X0,X1,X2) = k2_lattices(sK12110_skl,X1,X2)
| ~ m1_subset_1(X2,u1_struct_0(sK12110_skl))
| ~ m1_subset_1(X1,u1_struct_0(sK12110_skl))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) != g3_lattices(u1_struct_0(sK12110_skl),u2_lattices(sK12110_skl),u1_lattices(sK12110_skl))
| ~ l3_lattices(X0)
| v3_struct_0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ2909_spl])],[split_symbol_definition]) ).
fof(f192075,plain,
! [X0,X1,X2] :
( ~ sQ2909_spl
| k2_lattices(X0,X1,X2) = k2_lattices(sK12110_skl,X1,X2)
| ~ m1_subset_1(X2,u1_struct_0(sK12110_skl))
| ~ m1_subset_1(X1,u1_struct_0(sK12110_skl))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) != g3_lattices(u1_struct_0(sK12110_skl),u2_lattices(sK12110_skl),u1_lattices(sK12110_skl))
| ~ l3_lattices(X0)
| v3_struct_0(X0) ),
inference(component_clause,[status(thm)],[f192074]) ).
fof(f192077,plain,
( sQ2906_spl
| sQ2909_spl ),
inference(split_clause,[status(thm)],[f192072,f192074,f192056]) ).
fof(f192078,definition,
! [X0,X1,X2] :
( sQ2910_spl
<=> ( k2_lattices(X0,X1,X2) = k2_lattices(sK12109_skl,X1,X2)
| ~ m1_subset_1(X2,u1_struct_0(sK12109_skl))
| ~ m1_subset_1(X1,u1_struct_0(sK12109_skl))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) != g3_lattices(u1_struct_0(sK12109_skl),u2_lattices(sK12109_skl),u1_lattices(sK12109_skl))
| ~ l3_lattices(X0)
| v3_struct_0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ2910_spl])],[split_symbol_definition]) ).
fof(f192079,plain,
! [X0,X1,X2] :
( ~ sQ2910_spl
| k2_lattices(X0,X1,X2) = k2_lattices(sK12109_skl,X1,X2)
| ~ m1_subset_1(X2,u1_struct_0(sK12109_skl))
| ~ m1_subset_1(X1,u1_struct_0(sK12109_skl))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) != g3_lattices(u1_struct_0(sK12109_skl),u2_lattices(sK12109_skl),u1_lattices(sK12109_skl))
| ~ l3_lattices(X0)
| v3_struct_0(X0) ),
inference(component_clause,[status(thm)],[f192078]) ).
fof(f192081,plain,
( sQ2908_spl
| sQ2910_spl ),
inference(split_clause,[status(thm)],[f192073,f192078,f192063]) ).
fof(f192082,plain,
! [X0,X1,X2] :
( ~ sQ2909_spl
| k2_lattices(X0,X1,X2) = k2_lattices(sK12110_skl,X1,X2)
| ~ m1_subset_1(X2,u1_struct_0(sK12110_skl))
| ~ m1_subset_1(X1,u1_struct_0(sK12110_skl))
| ~ m1_subset_1(X2,u1_struct_0(X0))
| ~ m1_subset_1(X1,u1_struct_0(X0))
| g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) != g3_lattices(u1_struct_0(sK12109_skl),u2_lattices(sK12109_skl),u1_lattices(sK12109_skl))
| ~ l3_lattices(X0)
| v3_struct_0(X0) ),
inference(forward_demodulation,[status(thm)],[f153997,f192075]) ).
fof(f192095,plain,
! [X0,X1] :
( ~ sQ2907_spl
| k1_lattices(sK12110_skl,X0,X1) = k1_lattices(sK12109_skl,X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(sK12109_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK12109_skl))
| ~ m1_subset_1(X1,u1_struct_0(sK12110_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK12110_skl))
| g3_lattices(u1_struct_0(sK12110_skl),u2_lattices(sK12110_skl),u1_lattices(sK12110_skl)) != g3_lattices(u1_struct_0(sK12109_skl),u2_lattices(sK12109_skl),u1_lattices(sK12109_skl))
| v3_struct_0(sK12110_skl) ),
inference(resolution,[status(thm)],[f192061,f153996]) ).
fof(f192096,plain,
! [X0,X1] :
( ~ sQ2907_spl
| k1_lattices(sK12109_skl,X0,X1) = k1_lattices(sK12109_skl,X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(sK12109_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK12109_skl))
| ~ m1_subset_1(X1,u1_struct_0(sK12109_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK12109_skl))
| g3_lattices(u1_struct_0(sK12109_skl),u2_lattices(sK12109_skl),u1_lattices(sK12109_skl)) != g3_lattices(u1_struct_0(sK12109_skl),u2_lattices(sK12109_skl),u1_lattices(sK12109_skl))
| v3_struct_0(sK12109_skl) ),
inference(resolution,[status(thm)],[f192061,f153994]) ).
fof(f192097,definition,
( sQ2911_spl
<=> g3_lattices(u1_struct_0(sK12110_skl),u2_lattices(sK12110_skl),u1_lattices(sK12110_skl)) = g3_lattices(u1_struct_0(sK12109_skl),u2_lattices(sK12109_skl),u1_lattices(sK12109_skl)) ),
introduced(definition,[new_symbols(definition,[sQ2911_spl])],[split_symbol_definition]) ).
fof(f192099,plain,
( sQ2911_spl
| g3_lattices(u1_struct_0(sK12110_skl),u2_lattices(sK12110_skl),u1_lattices(sK12110_skl)) != g3_lattices(u1_struct_0(sK12109_skl),u2_lattices(sK12109_skl),u1_lattices(sK12109_skl)) ),
inference(component_clause,[status(thm)],[f192097]) ).
fof(f192100,definition,
! [X0,X1] :
( sQ2912_spl
<=> ( k1_lattices(sK12110_skl,X0,X1) = k1_lattices(sK12109_skl,X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(sK12109_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK12109_skl))
| ~ m1_subset_1(X1,u1_struct_0(sK12110_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK12110_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ2912_spl])],[split_symbol_definition]) ).
fof(f192101,plain,
! [X0,X1] :
( ~ sQ2912_spl
| k1_lattices(sK12110_skl,X0,X1) = k1_lattices(sK12109_skl,X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(sK12109_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK12109_skl))
| ~ m1_subset_1(X1,u1_struct_0(sK12110_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK12110_skl)) ),
inference(component_clause,[status(thm)],[f192100]) ).
fof(f192103,plain,
( ~ sQ2907_spl
| sQ2912_spl
| ~ sQ2911_spl
| sQ2906_spl ),
inference(split_clause,[status(thm)],[f192095,f192056,f192097,f192100,f192060]) ).
fof(f192104,definition,
( sQ2913_spl
<=> g3_lattices(u1_struct_0(sK12109_skl),u2_lattices(sK12109_skl),u1_lattices(sK12109_skl)) = g3_lattices(u1_struct_0(sK12109_skl),u2_lattices(sK12109_skl),u1_lattices(sK12109_skl)) ),
introduced(definition,[new_symbols(definition,[sQ2913_spl])],[split_symbol_definition]) ).
fof(f192106,plain,
( sQ2913_spl
| g3_lattices(u1_struct_0(sK12109_skl),u2_lattices(sK12109_skl),u1_lattices(sK12109_skl)) != g3_lattices(u1_struct_0(sK12109_skl),u2_lattices(sK12109_skl),u1_lattices(sK12109_skl)) ),
inference(component_clause,[status(thm)],[f192104]) ).
fof(f192107,definition,
! [X0,X1] :
( sQ2914_spl
<=> ( k1_lattices(sK12109_skl,X0,X1) = k1_lattices(sK12109_skl,X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(sK12109_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK12109_skl))
| ~ m1_subset_1(X1,u1_struct_0(sK12109_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK12109_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ2914_spl])],[split_symbol_definition]) ).
fof(f192110,plain,
( ~ sQ2907_spl
| sQ2914_spl
| ~ sQ2913_spl
| sQ2908_spl ),
inference(split_clause,[status(thm)],[f192096,f192063,f192104,f192107,f192060]) ).
fof(f192111,plain,
( sQ2911_spl
| g3_lattices(u1_struct_0(sK12109_skl),u2_lattices(sK12109_skl),u1_lattices(sK12109_skl)) != g3_lattices(u1_struct_0(sK12109_skl),u2_lattices(sK12109_skl),u1_lattices(sK12109_skl)) ),
inference(forward_demodulation,[status(thm)],[f153997,f192099]) ).
fof(f192112,plain,
( sQ2911_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f192111]) ).
fof(f192113,plain,
sQ2911_spl,
inference(contradiction_clause,[status(thm)],[f192112]) ).
fof(f192114,plain,
( sQ2913_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f192106]) ).
fof(f192115,plain,
sQ2913_spl,
inference(contradiction_clause,[status(thm)],[f192114]) ).
fof(f192116,plain,
! [X0,X1] :
( ~ sQ2905_spl
| k1_lattices(sK12110_skl,X0,X1) = k1_lattices(sK12110_skl,X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(sK12110_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK12110_skl))
| ~ m1_subset_1(X1,u1_struct_0(sK12110_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK12110_skl))
| g3_lattices(u1_struct_0(sK12110_skl),u2_lattices(sK12110_skl),u1_lattices(sK12110_skl)) != g3_lattices(u1_struct_0(sK12109_skl),u2_lattices(sK12109_skl),u1_lattices(sK12109_skl))
| v3_struct_0(sK12110_skl) ),
inference(resolution,[status(thm)],[f192067,f153996]) ).
fof(f192118,definition,
! [X0,X1] :
( sQ2915_spl
<=> ( k1_lattices(sK12110_skl,X0,X1) = k1_lattices(sK12110_skl,X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(sK12110_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK12110_skl))
| ~ m1_subset_1(X1,u1_struct_0(sK12110_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK12110_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ2915_spl])],[split_symbol_definition]) ).
fof(f192121,plain,
( ~ sQ2905_spl
| sQ2915_spl
| ~ sQ2911_spl
| sQ2906_spl ),
inference(split_clause,[status(thm)],[f192116,f192056,f192097,f192118,f192053]) ).
fof(f192123,plain,
! [X0] :
( ~ sQ2912_spl
| k1_lattices(sK12110_skl,X0,sK12112_skl) = k1_lattices(sK12109_skl,X0,sK12112_skl)
| ~ m1_subset_1(sK12112_skl,u1_struct_0(sK12109_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK12109_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK12110_skl)) ),
inference(resolution,[status(thm)],[f192101,f192028]) ).
fof(f192124,plain,
! [X0] :
( ~ sQ2912_spl
| k1_lattices(sK12110_skl,X0,sK12111_skl) = k1_lattices(sK12109_skl,X0,sK12111_skl)
| ~ m1_subset_1(sK12111_skl,u1_struct_0(sK12109_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK12109_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK12110_skl)) ),
inference(resolution,[status(thm)],[f192101,f192027]) ).
fof(f192125,definition,
! [X0] :
( sQ2916_spl
<=> ( k1_lattices(sK12110_skl,X0,sK12112_skl) = k1_lattices(sK12109_skl,X0,sK12112_skl)
| ~ m1_subset_1(X0,u1_struct_0(sK12109_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK12110_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ2916_spl])],[split_symbol_definition]) ).
fof(f192126,plain,
! [X0] :
( ~ sQ2916_spl
| k1_lattices(sK12110_skl,X0,sK12112_skl) = k1_lattices(sK12109_skl,X0,sK12112_skl)
| ~ m1_subset_1(X0,u1_struct_0(sK12109_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK12110_skl)) ),
inference(component_clause,[status(thm)],[f192125]) ).
fof(f192128,definition,
( sQ2917_spl
<=> m1_subset_1(sK12112_skl,u1_struct_0(sK12109_skl)) ),
introduced(definition,[new_symbols(definition,[sQ2917_spl])],[split_symbol_definition]) ).
fof(f192130,plain,
( sQ2917_spl
| ~ m1_subset_1(sK12112_skl,u1_struct_0(sK12109_skl)) ),
inference(component_clause,[status(thm)],[f192128]) ).
fof(f192131,plain,
( ~ sQ2912_spl
| ~ sQ2917_spl
| sQ2916_spl ),
inference(split_clause,[status(thm)],[f192123,f192125,f192128,f192100]) ).
fof(f192132,definition,
! [X0] :
( sQ2918_spl
<=> ( k1_lattices(sK12110_skl,X0,sK12111_skl) = k1_lattices(sK12109_skl,X0,sK12111_skl)
| ~ m1_subset_1(X0,u1_struct_0(sK12109_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK12110_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ2918_spl])],[split_symbol_definition]) ).
fof(f192135,definition,
( sQ2919_spl
<=> m1_subset_1(sK12111_skl,u1_struct_0(sK12109_skl)) ),
introduced(definition,[new_symbols(definition,[sQ2919_spl])],[split_symbol_definition]) ).
fof(f192137,plain,
( sQ2919_spl
| ~ m1_subset_1(sK12111_skl,u1_struct_0(sK12109_skl)) ),
inference(component_clause,[status(thm)],[f192135]) ).
fof(f192138,plain,
( ~ sQ2912_spl
| ~ sQ2919_spl
| sQ2918_spl ),
inference(split_clause,[status(thm)],[f192124,f192132,f192135,f192100]) ).
fof(f192139,plain,
( sQ2919_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f192137,f153998]) ).
fof(f192140,plain,
sQ2919_spl,
inference(contradiction_clause,[status(thm)],[f192139]) ).
fof(f192141,plain,
( sQ2917_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f192130,f153999]) ).
fof(f192142,plain,
sQ2917_spl,
inference(contradiction_clause,[status(thm)],[f192141]) ).
fof(f192143,plain,
( ~ sQ2916_spl
| k1_lattices(sK12110_skl,sK12112_skl,sK12112_skl) = k1_lattices(sK12109_skl,sK12112_skl,sK12112_skl)
| ~ m1_subset_1(sK12112_skl,u1_struct_0(sK12109_skl)) ),
inference(resolution,[status(thm)],[f192126,f192028]) ).
fof(f192144,plain,
( ~ sQ2916_spl
| k1_lattices(sK12110_skl,sK12111_skl,sK12112_skl) = k1_lattices(sK12109_skl,sK12111_skl,sK12112_skl)
| ~ m1_subset_1(sK12111_skl,u1_struct_0(sK12109_skl)) ),
inference(resolution,[status(thm)],[f192126,f192027]) ).
fof(f192145,definition,
( sQ2920_spl
<=> k1_lattices(sK12110_skl,sK12112_skl,sK12112_skl) = k1_lattices(sK12109_skl,sK12112_skl,sK12112_skl) ),
introduced(definition,[new_symbols(definition,[sQ2920_spl])],[split_symbol_definition]) ).
fof(f192148,plain,
( ~ sQ2916_spl
| sQ2920_spl
| ~ sQ2917_spl ),
inference(split_clause,[status(thm)],[f192143,f192128,f192145,f192125]) ).
fof(f192149,definition,
( sQ2921_spl
<=> k1_lattices(sK12110_skl,sK12111_skl,sK12112_skl) = k1_lattices(sK12109_skl,sK12111_skl,sK12112_skl) ),
introduced(definition,[new_symbols(definition,[sQ2921_spl])],[split_symbol_definition]) ).
fof(f192150,plain,
( ~ sQ2921_spl
| k1_lattices(sK12110_skl,sK12111_skl,sK12112_skl) = k1_lattices(sK12109_skl,sK12111_skl,sK12112_skl) ),
inference(component_clause,[status(thm)],[f192149]) ).
fof(f192152,plain,
( ~ sQ2916_spl
| sQ2921_spl
| ~ sQ2919_spl ),
inference(split_clause,[status(thm)],[f192144,f192135,f192149,f192125]) ).
fof(f192153,plain,
( ~ sQ2921_spl
| sQ2282_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f192150,f192050]) ).
fof(f192154,plain,
( ~ sQ2921_spl
| sQ2282_spl ),
inference(contradiction_clause,[status(thm)],[f192153]) ).
fof(f192157,plain,
! [X0,X1] :
( ~ sQ2910_spl
| k2_lattices(sK12110_skl,X0,X1) = k2_lattices(sK12109_skl,X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(sK12109_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK12109_skl))
| ~ m1_subset_1(X1,u1_struct_0(sK12110_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK12110_skl))
| g3_lattices(u1_struct_0(sK12110_skl),u2_lattices(sK12110_skl),u1_lattices(sK12110_skl)) != g3_lattices(u1_struct_0(sK12109_skl),u2_lattices(sK12109_skl),u1_lattices(sK12109_skl))
| v3_struct_0(sK12110_skl) ),
inference(resolution,[status(thm)],[f192079,f153996]) ).
fof(f192158,plain,
! [X0,X1] :
( ~ sQ2910_spl
| k2_lattices(sK12109_skl,X0,X1) = k2_lattices(sK12109_skl,X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(sK12109_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK12109_skl))
| ~ m1_subset_1(X1,u1_struct_0(sK12109_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK12109_skl))
| g3_lattices(u1_struct_0(sK12109_skl),u2_lattices(sK12109_skl),u1_lattices(sK12109_skl)) != g3_lattices(u1_struct_0(sK12109_skl),u2_lattices(sK12109_skl),u1_lattices(sK12109_skl))
| v3_struct_0(sK12109_skl) ),
inference(resolution,[status(thm)],[f192079,f153994]) ).
fof(f192159,definition,
! [X0,X1] :
( sQ2922_spl
<=> ( k2_lattices(sK12110_skl,X0,X1) = k2_lattices(sK12109_skl,X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(sK12109_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK12109_skl))
| ~ m1_subset_1(X1,u1_struct_0(sK12110_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK12110_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ2922_spl])],[split_symbol_definition]) ).
fof(f192160,plain,
! [X0,X1] :
( ~ sQ2922_spl
| k2_lattices(sK12110_skl,X0,X1) = k2_lattices(sK12109_skl,X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(sK12109_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK12109_skl))
| ~ m1_subset_1(X1,u1_struct_0(sK12110_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK12110_skl)) ),
inference(component_clause,[status(thm)],[f192159]) ).
fof(f192162,plain,
( ~ sQ2910_spl
| sQ2922_spl
| ~ sQ2911_spl
| sQ2906_spl ),
inference(split_clause,[status(thm)],[f192157,f192056,f192097,f192159,f192078]) ).
fof(f192163,definition,
! [X0,X1] :
( sQ2923_spl
<=> ( k2_lattices(sK12109_skl,X0,X1) = k2_lattices(sK12109_skl,X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(sK12109_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK12109_skl))
| ~ m1_subset_1(X1,u1_struct_0(sK12109_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK12109_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ2923_spl])],[split_symbol_definition]) ).
fof(f192166,plain,
( ~ sQ2910_spl
| sQ2923_spl
| ~ sQ2913_spl
| sQ2908_spl ),
inference(split_clause,[status(thm)],[f192158,f192063,f192104,f192163,f192078]) ).
fof(f192179,plain,
! [X0,X1] :
( ~ sQ2909_spl
| k2_lattices(sK12110_skl,X0,X1) = k2_lattices(sK12110_skl,X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(sK12110_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK12110_skl))
| ~ m1_subset_1(X1,u1_struct_0(sK12110_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK12110_skl))
| g3_lattices(u1_struct_0(sK12110_skl),u2_lattices(sK12110_skl),u1_lattices(sK12110_skl)) != g3_lattices(u1_struct_0(sK12109_skl),u2_lattices(sK12109_skl),u1_lattices(sK12109_skl))
| v3_struct_0(sK12110_skl) ),
inference(resolution,[status(thm)],[f192082,f153996]) ).
fof(f192181,definition,
! [X0,X1] :
( sQ2924_spl
<=> ( k2_lattices(sK12110_skl,X0,X1) = k2_lattices(sK12110_skl,X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(sK12110_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK12110_skl))
| ~ m1_subset_1(X1,u1_struct_0(sK12110_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK12110_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ2924_spl])],[split_symbol_definition]) ).
fof(f192184,plain,
( ~ sQ2909_spl
| sQ2924_spl
| ~ sQ2911_spl
| sQ2906_spl ),
inference(split_clause,[status(thm)],[f192179,f192056,f192097,f192181,f192074]) ).
fof(f192186,plain,
! [X0] :
( ~ sQ2922_spl
| k2_lattices(sK12110_skl,X0,sK12112_skl) = k2_lattices(sK12109_skl,X0,sK12112_skl)
| ~ m1_subset_1(sK12112_skl,u1_struct_0(sK12109_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK12109_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK12110_skl)) ),
inference(resolution,[status(thm)],[f192160,f192028]) ).
fof(f192187,plain,
! [X0] :
( ~ sQ2922_spl
| k2_lattices(sK12110_skl,X0,sK12111_skl) = k2_lattices(sK12109_skl,X0,sK12111_skl)
| ~ m1_subset_1(sK12111_skl,u1_struct_0(sK12109_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK12109_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK12110_skl)) ),
inference(resolution,[status(thm)],[f192160,f192027]) ).
fof(f192188,definition,
! [X0] :
( sQ2925_spl
<=> ( k2_lattices(sK12110_skl,X0,sK12112_skl) = k2_lattices(sK12109_skl,X0,sK12112_skl)
| ~ m1_subset_1(X0,u1_struct_0(sK12109_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK12110_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ2925_spl])],[split_symbol_definition]) ).
fof(f192189,plain,
! [X0] :
( ~ sQ2925_spl
| k2_lattices(sK12110_skl,X0,sK12112_skl) = k2_lattices(sK12109_skl,X0,sK12112_skl)
| ~ m1_subset_1(X0,u1_struct_0(sK12109_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK12110_skl)) ),
inference(component_clause,[status(thm)],[f192188]) ).
fof(f192191,plain,
( ~ sQ2922_spl
| ~ sQ2917_spl
| sQ2925_spl ),
inference(split_clause,[status(thm)],[f192186,f192188,f192128,f192159]) ).
fof(f192192,definition,
! [X0] :
( sQ2926_spl
<=> ( k2_lattices(sK12110_skl,X0,sK12111_skl) = k2_lattices(sK12109_skl,X0,sK12111_skl)
| ~ m1_subset_1(X0,u1_struct_0(sK12109_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK12110_skl)) ) ),
introduced(definition,[new_symbols(definition,[sQ2926_spl])],[split_symbol_definition]) ).
fof(f192195,plain,
( ~ sQ2922_spl
| ~ sQ2919_spl
| sQ2926_spl ),
inference(split_clause,[status(thm)],[f192187,f192192,f192135,f192159]) ).
fof(f192196,plain,
( ~ sQ2925_spl
| k2_lattices(sK12110_skl,sK12112_skl,sK12112_skl) = k2_lattices(sK12109_skl,sK12112_skl,sK12112_skl)
| ~ m1_subset_1(sK12112_skl,u1_struct_0(sK12109_skl)) ),
inference(resolution,[status(thm)],[f192189,f192028]) ).
fof(f192197,plain,
( ~ sQ2925_spl
| k2_lattices(sK12110_skl,sK12111_skl,sK12112_skl) = k2_lattices(sK12109_skl,sK12111_skl,sK12112_skl)
| ~ m1_subset_1(sK12111_skl,u1_struct_0(sK12109_skl)) ),
inference(resolution,[status(thm)],[f192189,f192027]) ).
fof(f192198,definition,
( sQ2927_spl
<=> k2_lattices(sK12110_skl,sK12112_skl,sK12112_skl) = k2_lattices(sK12109_skl,sK12112_skl,sK12112_skl) ),
introduced(definition,[new_symbols(definition,[sQ2927_spl])],[split_symbol_definition]) ).
fof(f192201,plain,
( ~ sQ2925_spl
| sQ2927_spl
| ~ sQ2917_spl ),
inference(split_clause,[status(thm)],[f192196,f192128,f192198,f192188]) ).
fof(f192202,definition,
( sQ2928_spl
<=> k2_lattices(sK12110_skl,sK12111_skl,sK12112_skl) = k2_lattices(sK12109_skl,sK12111_skl,sK12112_skl) ),
introduced(definition,[new_symbols(definition,[sQ2928_spl])],[split_symbol_definition]) ).
fof(f192203,plain,
( ~ sQ2928_spl
| k2_lattices(sK12110_skl,sK12111_skl,sK12112_skl) = k2_lattices(sK12109_skl,sK12111_skl,sK12112_skl) ),
inference(component_clause,[status(thm)],[f192202]) ).
fof(f192205,plain,
( ~ sQ2925_spl
| sQ2928_spl
| ~ sQ2919_spl ),
inference(split_clause,[status(thm)],[f192197,f192135,f192202,f192188]) ).
fof(f192206,plain,
( ~ sQ2928_spl
| sQ2283_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f192203,f192048]) ).
fof(f192207,plain,
( ~ sQ2928_spl
| sQ2283_spl ),
inference(contradiction_clause,[status(thm)],[f192206]) ).
fof(f192218,plain,
! [X0] :
( ~ sQ2284_spl
| r1_lattices(X0,sK12111_skl,sK12112_skl)
| ~ m1_subset_1(sK12112_skl,u1_struct_0(X0))
| ~ m1_subset_1(sK12111_skl,u1_struct_0(X0))
| ~ m1_subset_1(sK12112_skl,u1_struct_0(sK12109_skl))
| ~ m1_subset_1(sK12111_skl,u1_struct_0(sK12109_skl))
| g3_lattices(u1_struct_0(sK12109_skl),u2_lattices(sK12109_skl),u1_lattices(sK12109_skl)) != g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))
| ~ l3_lattices(X0)
| v3_struct_0(X0)
| ~ l3_lattices(sK12109_skl)
| v3_struct_0(sK12109_skl) ),
inference(resolution,[status(thm)],[f192036,f190802]) ).
fof(f192220,definition,
( sQ2929_spl
<=> l3_lattices(sK12109_skl) ),
introduced(definition,[new_symbols(definition,[sQ2929_spl])],[split_symbol_definition]) ).
fof(f192222,plain,
( sQ2929_spl
| ~ l3_lattices(sK12109_skl) ),
inference(component_clause,[status(thm)],[f192220]) ).
fof(f192223,definition,
! [X0] :
( sQ2930_spl
<=> ( r1_lattices(X0,sK12111_skl,sK12112_skl)
| ~ m1_subset_1(sK12112_skl,u1_struct_0(X0))
| ~ m1_subset_1(sK12111_skl,u1_struct_0(X0))
| g3_lattices(u1_struct_0(sK12109_skl),u2_lattices(sK12109_skl),u1_lattices(sK12109_skl)) != g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))
| ~ l3_lattices(X0)
| v3_struct_0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ2930_spl])],[split_symbol_definition]) ).
fof(f192224,plain,
! [X0] :
( ~ sQ2930_spl
| r1_lattices(X0,sK12111_skl,sK12112_skl)
| ~ m1_subset_1(sK12112_skl,u1_struct_0(X0))
| ~ m1_subset_1(sK12111_skl,u1_struct_0(X0))
| g3_lattices(u1_struct_0(sK12109_skl),u2_lattices(sK12109_skl),u1_lattices(sK12109_skl)) != g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))
| ~ l3_lattices(X0)
| v3_struct_0(X0) ),
inference(component_clause,[status(thm)],[f192223]) ).
fof(f192226,plain,
( ~ sQ2284_spl
| ~ sQ2917_spl
| ~ sQ2919_spl
| sQ2930_spl
| ~ sQ2929_spl
| sQ2908_spl ),
inference(split_clause,[status(thm)],[f192218,f192063,f192220,f192223,f192135,f192128,f180677]) ).
fof(f192227,plain,
( sQ2929_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f192222,f153994]) ).
fof(f192228,plain,
sQ2929_spl,
inference(contradiction_clause,[status(thm)],[f192227]) ).
fof(f192246,definition,
( sQ2933_spl
<=> l3_lattices(sK12110_skl) ),
introduced(definition,[new_symbols(definition,[sQ2933_spl])],[split_symbol_definition]) ).
fof(f192248,plain,
( sQ2933_spl
| ~ l3_lattices(sK12110_skl) ),
inference(component_clause,[status(thm)],[f192246]) ).
fof(f192249,definition,
( sQ2934_spl
<=> m1_subset_1(sK12111_skl,u1_struct_0(sK12110_skl)) ),
introduced(definition,[new_symbols(definition,[sQ2934_spl])],[split_symbol_definition]) ).
fof(f192251,plain,
( sQ2934_spl
| ~ m1_subset_1(sK12111_skl,u1_struct_0(sK12110_skl)) ),
inference(component_clause,[status(thm)],[f192249]) ).
fof(f192252,definition,
( sQ2935_spl
<=> m1_subset_1(sK12112_skl,u1_struct_0(sK12110_skl)) ),
introduced(definition,[new_symbols(definition,[sQ2935_spl])],[split_symbol_definition]) ).
fof(f192254,plain,
( sQ2935_spl
| ~ m1_subset_1(sK12112_skl,u1_struct_0(sK12110_skl)) ),
inference(component_clause,[status(thm)],[f192252]) ).
fof(f192256,plain,
( sQ2935_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f192254,f192028]) ).
fof(f192257,plain,
sQ2935_spl,
inference(contradiction_clause,[status(thm)],[f192256]) ).
fof(f192258,plain,
( sQ2934_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f192251,f192027]) ).
fof(f192259,plain,
sQ2934_spl,
inference(contradiction_clause,[status(thm)],[f192258]) ).
fof(f192260,plain,
( sQ2933_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f192248,f153996]) ).
fof(f192261,plain,
sQ2933_spl,
inference(contradiction_clause,[status(thm)],[f192260]) ).
fof(f192265,plain,
( ~ sQ2284_spl
| ~ sQ2930_spl
| ~ m1_subset_1(sK12112_skl,u1_struct_0(sK12110_skl))
| ~ m1_subset_1(sK12111_skl,u1_struct_0(sK12110_skl))
| g3_lattices(u1_struct_0(sK12109_skl),u2_lattices(sK12109_skl),u1_lattices(sK12109_skl)) != g3_lattices(u1_struct_0(sK12110_skl),u2_lattices(sK12110_skl),u1_lattices(sK12110_skl))
| ~ l3_lattices(sK12110_skl)
| v3_struct_0(sK12110_skl) ),
inference(resolution,[status(thm)],[f192224,f192035]) ).
fof(f192266,plain,
( ~ sQ2284_spl
| ~ sQ2930_spl
| ~ sQ2935_spl
| ~ sQ2934_spl
| ~ sQ2911_spl
| ~ sQ2933_spl
| sQ2906_spl ),
inference(split_clause,[status(thm)],[f192265,f192056,f192246,f192097,f192249,f192252,f192223,f180677]) ).
fof(f192272,plain,
! [X0] :
( sQ2286_spl
| ~ r1_lattices(X0,sK12111_skl,sK12112_skl)
| ~ m1_subset_1(sK12112_skl,u1_struct_0(sK12109_skl))
| ~ m1_subset_1(sK12111_skl,u1_struct_0(sK12109_skl))
| ~ m1_subset_1(sK12112_skl,u1_struct_0(X0))
| ~ m1_subset_1(sK12111_skl,u1_struct_0(X0))
| g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) != g3_lattices(u1_struct_0(sK12109_skl),u2_lattices(sK12109_skl),u1_lattices(sK12109_skl))
| ~ l3_lattices(sK12109_skl)
| v3_struct_0(sK12109_skl)
| ~ l3_lattices(X0)
| v3_struct_0(X0) ),
inference(resolution,[status(thm)],[f180686,f190802]) ).
fof(f192273,definition,
! [X0] :
( sQ2936_spl
<=> ( ~ r1_lattices(X0,sK12111_skl,sK12112_skl)
| ~ m1_subset_1(sK12112_skl,u1_struct_0(X0))
| ~ m1_subset_1(sK12111_skl,u1_struct_0(X0))
| g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) != g3_lattices(u1_struct_0(sK12109_skl),u2_lattices(sK12109_skl),u1_lattices(sK12109_skl))
| ~ l3_lattices(X0)
| v3_struct_0(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ2936_spl])],[split_symbol_definition]) ).
fof(f192274,plain,
! [X0] :
( ~ sQ2936_spl
| ~ r1_lattices(X0,sK12111_skl,sK12112_skl)
| ~ m1_subset_1(sK12112_skl,u1_struct_0(X0))
| ~ m1_subset_1(sK12111_skl,u1_struct_0(X0))
| g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0)) != g3_lattices(u1_struct_0(sK12109_skl),u2_lattices(sK12109_skl),u1_lattices(sK12109_skl))
| ~ l3_lattices(X0)
| v3_struct_0(X0) ),
inference(component_clause,[status(thm)],[f192273]) ).
fof(f192276,plain,
( sQ2286_spl
| ~ sQ2917_spl
| ~ sQ2919_spl
| ~ sQ2929_spl
| sQ2908_spl
| sQ2936_spl ),
inference(split_clause,[status(thm)],[f192272,f192273,f192063,f192220,f192135,f192128,f180684]) ).
fof(f192283,plain,
( ~ sQ2936_spl
| ~ r1_lattices(sK12110_skl,sK12111_skl,sK12112_skl)
| ~ m1_subset_1(sK12111_skl,u1_struct_0(sK12110_skl))
| g3_lattices(u1_struct_0(sK12110_skl),u2_lattices(sK12110_skl),u1_lattices(sK12110_skl)) != g3_lattices(u1_struct_0(sK12109_skl),u2_lattices(sK12109_skl),u1_lattices(sK12109_skl))
| ~ l3_lattices(sK12110_skl)
| v3_struct_0(sK12110_skl) ),
inference(resolution,[status(thm)],[f192274,f192028]) ).
fof(f192285,definition,
( sQ2938_spl
<=> r1_lattices(sK12110_skl,sK12111_skl,sK12112_skl) ),
introduced(definition,[new_symbols(definition,[sQ2938_spl])],[split_symbol_definition]) ).
fof(f192287,plain,
( sQ2938_spl
| ~ r1_lattices(sK12110_skl,sK12111_skl,sK12112_skl) ),
inference(component_clause,[status(thm)],[f192285]) ).
fof(f192288,plain,
( ~ sQ2936_spl
| ~ sQ2938_spl
| ~ sQ2934_spl
| ~ sQ2911_spl
| ~ sQ2933_spl
| sQ2906_spl ),
inference(split_clause,[status(thm)],[f192283,f192056,f192246,f192097,f192249,f192285,f192273]) ).
fof(f192290,plain,
( sQ2938_spl
| ~ sQ2285_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f192287,f192030]) ).
fof(f192291,plain,
( sQ2938_spl
| ~ sQ2285_spl ),
inference(contradiction_clause,[status(thm)],[f192290]) ).
fof(f192292,plain,
$false,
inference(sat_refutation,[status(thm)],[f180683,f180687,f192059,f192066,f192069,f192071,f192077,f192081,f192103,f192110,f192113,f192115,f192121,f192131,f192138,f192140,f192142,f192148,f192152,f192154,f192162,f192166,f192184,f192191,f192195,f192201,f192205,f192207,f192226,f192228,f192257,f192259,f192261,f192266,f192276,f192288,f192291]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LAT295+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.20/0.45 % Computer : n002.cluster.edu
% 0.20/0.45 % Model : x86_64 x86_64
% 0.20/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.20/0.45 % Memory : 8046.5625MB
% 0.20/0.45 % OS : Linux 6.8.0-71-generic
% 0.20/0.45 % CPULimit : 300
% 0.20/0.45 % WCLimit : 300
% 0.20/0.45 % DateTime : Sun Sep 20 23:31:58 UTC 2026
% 0.20/0.46 % CPUTime :
% 10.35/10.64 % Drodi V4.1.1
% 39.67/14.49 % Refutation found
% 39.67/14.49 % SZS status Theorem for theBenchmark: Theorem is valid
% 39.67/14.49 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 11.42/15.68 % Elapsed time: 15.041093 seconds
% 11.42/15.68 % CPU time: 41.359488 seconds
% 11.42/15.68 % Total memory used: 11.075 GB
% 11.42/15.68 % Net memory used: 11.010 GB
%------------------------------------------------------------------------------