%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LAT295+3 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n008.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 2.15s 3.26s
% Output : CNFRefutation 2.27s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 3
% Syntax : Number of formulae : 103 ( 17 unt; 1 def)
% Number of atoms : 623 ( 101 equ)
% Maximal formula atoms : 17 ( 6 avg)
% Number of connectives : 897 ( 377 ~; 426 |; 63 &)
% ( 1 <=>; 30 =>; 0 <=; 0 <~>)
% Maximal formula depth : 23 ( 8 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-6 aty)
% Number of functors : 12 ( 12 usr; 6 con; 0-3 aty)
% Number of variables : 139 ( 127 !; 12 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f13132,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/sandbox/benchmark/theBenchmark.p') ).
fof(f13583,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/sandbox/benchmark/theBenchmark.p') ).
fof(f13584,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)],[f13583]) ).
fof(f55595,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)],[f13132]) ).
fof(f55596,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)],[f55595]) ).
fof(f55597,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)],[f55595]) ).
fof(f55598,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)],[f55595]) ).
fof(f57541,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)],[f13584]) ).
fof(f57542,definition,
! [A,B,C,D,E,F] :
( sP322_prd(F,E,D,C,B,A)
<=> ( ~ r1_lattices(B,E,F)
& r1_lattices(A,C,D) ) ),
introduced(definition,[new_symbols(definition,[sP322_prd])],[]) ).
fof(f57543,plain,
? [A] :
( ? [B] :
( ? [C] :
( ? [D] :
( ? [E] :
( ? [F] :
( ( ( ~ r1_lattices(A,C,D)
& r1_lattices(B,E,F) )
| sP322_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)],[f57541,f57542]) ).
fof(f57544,plain,
( ( ( ~ r1_lattices(sK3966_skl,sK3968_skl,sK3969_skl)
& r1_lattices(sK3967_skl,sK3970_skl,sK3971_skl) )
| sP322_prd(sK3971_skl,sK3970_skl,sK3969_skl,sK3968_skl,sK3967_skl,sK3966_skl)
| k2_lattices(sK3966_skl,sK3968_skl,sK3969_skl) != k2_lattices(sK3967_skl,sK3970_skl,sK3971_skl)
| k1_lattices(sK3966_skl,sK3968_skl,sK3969_skl) != k1_lattices(sK3967_skl,sK3970_skl,sK3971_skl) )
& sK3969_skl = sK3971_skl
& sK3968_skl = sK3970_skl
& m1_subset_1(sK3971_skl,u1_struct_0(sK3967_skl))
& m1_subset_1(sK3970_skl,u1_struct_0(sK3967_skl))
& m1_subset_1(sK3969_skl,u1_struct_0(sK3966_skl))
& m1_subset_1(sK3968_skl,u1_struct_0(sK3966_skl))
& g3_lattices(u1_struct_0(sK3966_skl),u2_lattices(sK3966_skl),u1_lattices(sK3966_skl)) = g3_lattices(u1_struct_0(sK3967_skl),u2_lattices(sK3967_skl),u1_lattices(sK3967_skl))
& l3_lattices(sK3967_skl)
& ~ v3_struct_0(sK3967_skl)
& l3_lattices(sK3966_skl)
& ~ v3_struct_0(sK3966_skl) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3966_skl,sK3967_skl,sK3968_skl,sK3969_skl,sK3970_skl,sK3971_skl]),skolemize(A,sK3966_skl),skolemize(B,sK3967_skl),skolemize(C,sK3968_skl),skolemize(D,sK3969_skl),skolemize(E,sK3970_skl),skolemize(F,sK3971_skl)],[f57543]) ).
fof(f57545,plain,
~ v3_struct_0(sK3966_skl),
inference(cnf_transformation,[status(thm)],[f57544]) ).
fof(f57546,plain,
l3_lattices(sK3966_skl),
inference(cnf_transformation,[status(thm)],[f57544]) ).
fof(f57547,plain,
~ v3_struct_0(sK3967_skl),
inference(cnf_transformation,[status(thm)],[f57544]) ).
fof(f57548,plain,
l3_lattices(sK3967_skl),
inference(cnf_transformation,[status(thm)],[f57544]) ).
fof(f57549,plain,
g3_lattices(u1_struct_0(sK3966_skl),u2_lattices(sK3966_skl),u1_lattices(sK3966_skl)) = g3_lattices(u1_struct_0(sK3967_skl),u2_lattices(sK3967_skl),u1_lattices(sK3967_skl)),
inference(cnf_transformation,[status(thm)],[f57544]) ).
fof(f57550,plain,
m1_subset_1(sK3968_skl,u1_struct_0(sK3966_skl)),
inference(cnf_transformation,[status(thm)],[f57544]) ).
fof(f57551,plain,
m1_subset_1(sK3969_skl,u1_struct_0(sK3966_skl)),
inference(cnf_transformation,[status(thm)],[f57544]) ).
fof(f57552,plain,
m1_subset_1(sK3970_skl,u1_struct_0(sK3967_skl)),
inference(cnf_transformation,[status(thm)],[f57544]) ).
fof(f57553,plain,
m1_subset_1(sK3971_skl,u1_struct_0(sK3967_skl)),
inference(cnf_transformation,[status(thm)],[f57544]) ).
fof(f57554,plain,
sK3968_skl = sK3970_skl,
inference(cnf_transformation,[status(thm)],[f57544]) ).
fof(f57555,plain,
sK3969_skl = sK3971_skl,
inference(cnf_transformation,[status(thm)],[f57544]) ).
fof(f57556,plain,
( r1_lattices(sK3967_skl,sK3970_skl,sK3971_skl)
| sP322_prd(sK3971_skl,sK3970_skl,sK3969_skl,sK3968_skl,sK3967_skl,sK3966_skl)
| k2_lattices(sK3966_skl,sK3968_skl,sK3969_skl) != k2_lattices(sK3967_skl,sK3970_skl,sK3971_skl)
| k1_lattices(sK3966_skl,sK3968_skl,sK3969_skl) != k1_lattices(sK3967_skl,sK3970_skl,sK3971_skl) ),
inference(cnf_transformation,[status(thm)],[f57544]) ).
fof(f57557,plain,
( ~ r1_lattices(sK3966_skl,sK3968_skl,sK3969_skl)
| sP322_prd(sK3971_skl,sK3970_skl,sK3969_skl,sK3968_skl,sK3967_skl,sK3966_skl)
| k2_lattices(sK3966_skl,sK3968_skl,sK3969_skl) != k2_lattices(sK3967_skl,sK3970_skl,sK3971_skl)
| k1_lattices(sK3966_skl,sK3968_skl,sK3969_skl) != k1_lattices(sK3967_skl,sK3970_skl,sK3971_skl) ),
inference(cnf_transformation,[status(thm)],[f57544]) ).
fof(f59931,plain,
! [A,B,C,D,E,F] :
( ( r1_lattices(B,E,F)
| ~ r1_lattices(A,C,D)
| sP322_prd(F,E,D,C,B,A) )
& ( ( ~ r1_lattices(B,E,F)
& r1_lattices(A,C,D) )
| ~ sP322_prd(F,E,D,C,B,A) ) ),
inference(NNF_transformation,[status(thm)],[f57542]) ).
fof(f59932,plain,
( ! [A,B,C,D,E,F] :
( r1_lattices(B,E,F)
| ~ r1_lattices(A,C,D)
| sP322_prd(F,E,D,C,B,A) )
& ! [A,B,C,D,E,F] :
( ( ~ r1_lattices(B,E,F)
& r1_lattices(A,C,D) )
| ~ sP322_prd(F,E,D,C,B,A) ) ),
inference(miniscoping,[status(thm)],[f59931]) ).
fof(f59933,plain,
! [X0,X1,X2,X3,X4,X5] :
( r1_lattices(X5,X3,X2)
| ~ sP322_prd(X0,X1,X2,X3,X4,X5) ),
inference(cnf_transformation,[status(thm)],[f59932]) ).
fof(f59934,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ r1_lattices(X4,X1,X0)
| ~ sP322_prd(X0,X1,X2,X3,X4,X5) ),
inference(cnf_transformation,[status(thm)],[f59932]) ).
fof(f63117,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)],[f55596]) ).
fof(f63118,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)],[f55597]) ).
fof(f63119,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)],[f55598]) ).
fof(f63506,plain,
m1_subset_1(sK3970_skl,u1_struct_0(sK3966_skl)),
inference(forward_demodulation,[status(thm)],[f57554,f57550]) ).
fof(f63507,plain,
m1_subset_1(sK3971_skl,u1_struct_0(sK3966_skl)),
inference(forward_demodulation,[status(thm)],[f57555,f57551]) ).
fof(f63514,plain,
( r1_lattices(sK3967_skl,sK3970_skl,sK3971_skl)
| sP322_prd(sK3971_skl,sK3970_skl,sK3969_skl,sK3968_skl,sK3967_skl,sK3966_skl)
| k2_lattices(sK3966_skl,sK3968_skl,sK3969_skl) != k2_lattices(sK3967_skl,sK3970_skl,sK3971_skl)
| k1_lattices(sK3966_skl,sK3970_skl,sK3969_skl) != k1_lattices(sK3967_skl,sK3970_skl,sK3971_skl) ),
inference(forward_demodulation,[status(thm)],[f57554,f57556]) ).
fof(f63515,plain,
( r1_lattices(sK3967_skl,sK3970_skl,sK3971_skl)
| sP322_prd(sK3971_skl,sK3970_skl,sK3969_skl,sK3968_skl,sK3967_skl,sK3966_skl)
| k2_lattices(sK3966_skl,sK3968_skl,sK3969_skl) != k2_lattices(sK3967_skl,sK3970_skl,sK3971_skl)
| k1_lattices(sK3966_skl,sK3970_skl,sK3971_skl) != k1_lattices(sK3967_skl,sK3970_skl,sK3971_skl) ),
inference(forward_demodulation,[status(thm)],[f57555,f63514]) ).
fof(f63516,plain,
( r1_lattices(sK3967_skl,sK3970_skl,sK3971_skl)
| sP322_prd(sK3971_skl,sK3970_skl,sK3969_skl,sK3968_skl,sK3967_skl,sK3966_skl)
| k2_lattices(sK3966_skl,sK3970_skl,sK3969_skl) != k2_lattices(sK3967_skl,sK3970_skl,sK3971_skl)
| k1_lattices(sK3966_skl,sK3970_skl,sK3971_skl) != k1_lattices(sK3967_skl,sK3970_skl,sK3971_skl) ),
inference(forward_demodulation,[status(thm)],[f57554,f63515]) ).
fof(f63517,plain,
( r1_lattices(sK3967_skl,sK3970_skl,sK3971_skl)
| sP322_prd(sK3971_skl,sK3970_skl,sK3969_skl,sK3968_skl,sK3967_skl,sK3966_skl)
| k2_lattices(sK3966_skl,sK3970_skl,sK3971_skl) != k2_lattices(sK3967_skl,sK3970_skl,sK3971_skl)
| k1_lattices(sK3966_skl,sK3970_skl,sK3971_skl) != k1_lattices(sK3967_skl,sK3970_skl,sK3971_skl) ),
inference(forward_demodulation,[status(thm)],[f57555,f63516]) ).
fof(f63518,plain,
( r1_lattices(sK3967_skl,sK3970_skl,sK3971_skl)
| sP322_prd(sK3971_skl,sK3970_skl,sK3971_skl,sK3968_skl,sK3967_skl,sK3966_skl)
| k2_lattices(sK3966_skl,sK3970_skl,sK3971_skl) != k2_lattices(sK3967_skl,sK3970_skl,sK3971_skl)
| k1_lattices(sK3966_skl,sK3970_skl,sK3971_skl) != k1_lattices(sK3967_skl,sK3970_skl,sK3971_skl) ),
inference(forward_demodulation,[status(thm)],[f57555,f63517]) ).
fof(f63519,plain,
( r1_lattices(sK3967_skl,sK3970_skl,sK3971_skl)
| sP322_prd(sK3971_skl,sK3970_skl,sK3971_skl,sK3970_skl,sK3967_skl,sK3966_skl)
| k2_lattices(sK3966_skl,sK3970_skl,sK3971_skl) != k2_lattices(sK3967_skl,sK3970_skl,sK3971_skl)
| k1_lattices(sK3966_skl,sK3970_skl,sK3971_skl) != k1_lattices(sK3967_skl,sK3970_skl,sK3971_skl) ),
inference(forward_demodulation,[status(thm)],[f57554,f63518]) ).
fof(f63520,plain,
( ~ r1_lattices(sK3966_skl,sK3968_skl,sK3969_skl)
| sP322_prd(sK3971_skl,sK3970_skl,sK3969_skl,sK3968_skl,sK3967_skl,sK3966_skl)
| k2_lattices(sK3966_skl,sK3968_skl,sK3969_skl) != k2_lattices(sK3967_skl,sK3970_skl,sK3971_skl)
| k1_lattices(sK3966_skl,sK3970_skl,sK3969_skl) != k1_lattices(sK3967_skl,sK3970_skl,sK3971_skl) ),
inference(forward_demodulation,[status(thm)],[f57554,f57557]) ).
fof(f63521,plain,
( ~ r1_lattices(sK3966_skl,sK3968_skl,sK3969_skl)
| sP322_prd(sK3971_skl,sK3970_skl,sK3969_skl,sK3968_skl,sK3967_skl,sK3966_skl)
| k2_lattices(sK3966_skl,sK3968_skl,sK3969_skl) != k2_lattices(sK3967_skl,sK3970_skl,sK3971_skl)
| k1_lattices(sK3966_skl,sK3970_skl,sK3971_skl) != k1_lattices(sK3967_skl,sK3970_skl,sK3971_skl) ),
inference(forward_demodulation,[status(thm)],[f57555,f63520]) ).
fof(f63522,plain,
( ~ r1_lattices(sK3966_skl,sK3968_skl,sK3969_skl)
| sP322_prd(sK3971_skl,sK3970_skl,sK3969_skl,sK3968_skl,sK3967_skl,sK3966_skl)
| k2_lattices(sK3966_skl,sK3970_skl,sK3969_skl) != k2_lattices(sK3967_skl,sK3970_skl,sK3971_skl)
| k1_lattices(sK3966_skl,sK3970_skl,sK3971_skl) != k1_lattices(sK3967_skl,sK3970_skl,sK3971_skl) ),
inference(forward_demodulation,[status(thm)],[f57554,f63521]) ).
fof(f63523,plain,
( ~ r1_lattices(sK3966_skl,sK3968_skl,sK3969_skl)
| sP322_prd(sK3971_skl,sK3970_skl,sK3969_skl,sK3968_skl,sK3967_skl,sK3966_skl)
| k2_lattices(sK3966_skl,sK3970_skl,sK3971_skl) != k2_lattices(sK3967_skl,sK3970_skl,sK3971_skl)
| k1_lattices(sK3966_skl,sK3970_skl,sK3971_skl) != k1_lattices(sK3967_skl,sK3970_skl,sK3971_skl) ),
inference(forward_demodulation,[status(thm)],[f57555,f63522]) ).
fof(f63524,plain,
( ~ r1_lattices(sK3966_skl,sK3968_skl,sK3969_skl)
| sP322_prd(sK3971_skl,sK3970_skl,sK3971_skl,sK3968_skl,sK3967_skl,sK3966_skl)
| k2_lattices(sK3966_skl,sK3970_skl,sK3971_skl) != k2_lattices(sK3967_skl,sK3970_skl,sK3971_skl)
| k1_lattices(sK3966_skl,sK3970_skl,sK3971_skl) != k1_lattices(sK3967_skl,sK3970_skl,sK3971_skl) ),
inference(forward_demodulation,[status(thm)],[f57555,f63523]) ).
fof(f63525,plain,
( ~ r1_lattices(sK3966_skl,sK3968_skl,sK3969_skl)
| sP322_prd(sK3971_skl,sK3970_skl,sK3971_skl,sK3970_skl,sK3967_skl,sK3966_skl)
| k2_lattices(sK3966_skl,sK3970_skl,sK3971_skl) != k2_lattices(sK3967_skl,sK3970_skl,sK3971_skl)
| k1_lattices(sK3966_skl,sK3970_skl,sK3971_skl) != k1_lattices(sK3967_skl,sK3970_skl,sK3971_skl) ),
inference(forward_demodulation,[status(thm)],[f57554,f63524]) ).
fof(f63526,plain,
( ~ r1_lattices(sK3966_skl,sK3970_skl,sK3969_skl)
| sP322_prd(sK3971_skl,sK3970_skl,sK3971_skl,sK3970_skl,sK3967_skl,sK3966_skl)
| k2_lattices(sK3966_skl,sK3970_skl,sK3971_skl) != k2_lattices(sK3967_skl,sK3970_skl,sK3971_skl)
| k1_lattices(sK3966_skl,sK3970_skl,sK3971_skl) != k1_lattices(sK3967_skl,sK3970_skl,sK3971_skl) ),
inference(forward_demodulation,[status(thm)],[f57554,f63525]) ).
fof(f63527,plain,
( ~ r1_lattices(sK3966_skl,sK3970_skl,sK3971_skl)
| sP322_prd(sK3971_skl,sK3970_skl,sK3971_skl,sK3970_skl,sK3967_skl,sK3966_skl)
| k2_lattices(sK3966_skl,sK3970_skl,sK3971_skl) != k2_lattices(sK3967_skl,sK3970_skl,sK3971_skl)
| k1_lattices(sK3966_skl,sK3970_skl,sK3971_skl) != k1_lattices(sK3967_skl,sK3970_skl,sK3971_skl) ),
inference(forward_demodulation,[status(thm)],[f57555,f63526]) ).
fof(f63554,plain,
! [X0,X1] :
( k1_lattices(sK3966_skl,X0,X1) = k1_lattices(sK3967_skl,X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(sK3967_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK3967_skl))
| ~ m1_subset_1(X1,u1_struct_0(sK3966_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK3966_skl))
| ~ l3_lattices(sK3967_skl)
| v3_struct_0(sK3967_skl)
| ~ l3_lattices(sK3966_skl)
| v3_struct_0(sK3966_skl) ),
inference(resolution,[status(thm)],[f63117,f57549]) ).
fof(f63559,plain,
! [X0,X1] :
( k1_lattices(sK3966_skl,X0,X1) = k1_lattices(sK3967_skl,X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(sK3967_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK3967_skl))
| ~ m1_subset_1(X1,u1_struct_0(sK3966_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK3966_skl))
| ~ l3_lattices(sK3967_skl)
| v3_struct_0(sK3967_skl)
| ~ l3_lattices(sK3966_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f63554,f57545]) ).
fof(f63563,plain,
! [X0,X1] :
( k2_lattices(sK3966_skl,X0,X1) = k2_lattices(sK3967_skl,X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(sK3967_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK3967_skl))
| ~ m1_subset_1(X1,u1_struct_0(sK3966_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK3966_skl))
| ~ l3_lattices(sK3967_skl)
| v3_struct_0(sK3967_skl)
| ~ l3_lattices(sK3966_skl)
| v3_struct_0(sK3966_skl) ),
inference(resolution,[status(thm)],[f63118,f57549]) ).
fof(f63564,plain,
! [X0,X1] :
( k2_lattices(sK3967_skl,X0,X1) = k2_lattices(sK3966_skl,X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(sK3966_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK3966_skl))
| ~ m1_subset_1(X1,u1_struct_0(sK3967_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK3967_skl))
| ~ l3_lattices(sK3966_skl)
| v3_struct_0(sK3966_skl)
| ~ l3_lattices(sK3967_skl)
| v3_struct_0(sK3967_skl) ),
inference(resolution,[status(thm)],[f63118,f57549]) ).
fof(f63568,plain,
! [X0,X1] :
( k2_lattices(sK3966_skl,X0,X1) = k2_lattices(sK3967_skl,X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(sK3967_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK3967_skl))
| ~ m1_subset_1(X1,u1_struct_0(sK3966_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK3966_skl))
| ~ l3_lattices(sK3967_skl)
| v3_struct_0(sK3967_skl)
| ~ l3_lattices(sK3966_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f63563,f57545]) ).
fof(f63569,plain,
! [X0,X1] :
( k2_lattices(sK3967_skl,X0,X1) = k2_lattices(sK3966_skl,X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(sK3966_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK3966_skl))
| ~ m1_subset_1(X1,u1_struct_0(sK3967_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK3967_skl))
| ~ l3_lattices(sK3966_skl)
| v3_struct_0(sK3966_skl)
| ~ l3_lattices(sK3967_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f63564,f57547]) ).
fof(f63572,plain,
! [X0,X1] :
( r1_lattices(sK3967_skl,X0,X1)
| ~ r1_lattices(sK3966_skl,X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(sK3967_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK3967_skl))
| ~ m1_subset_1(X1,u1_struct_0(sK3966_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK3966_skl))
| ~ l3_lattices(sK3967_skl)
| v3_struct_0(sK3967_skl)
| ~ l3_lattices(sK3966_skl)
| v3_struct_0(sK3966_skl) ),
inference(resolution,[status(thm)],[f63119,f57549]) ).
fof(f63573,plain,
! [X0,X1] :
( r1_lattices(sK3966_skl,X0,X1)
| ~ r1_lattices(sK3967_skl,X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(sK3966_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK3966_skl))
| ~ m1_subset_1(X1,u1_struct_0(sK3967_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK3967_skl))
| ~ l3_lattices(sK3966_skl)
| v3_struct_0(sK3966_skl)
| ~ l3_lattices(sK3967_skl)
| v3_struct_0(sK3967_skl) ),
inference(resolution,[status(thm)],[f63119,f57549]) ).
fof(f63577,plain,
! [X0,X1] :
( r1_lattices(sK3967_skl,X0,X1)
| ~ r1_lattices(sK3966_skl,X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(sK3967_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK3967_skl))
| ~ m1_subset_1(X1,u1_struct_0(sK3966_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK3966_skl))
| ~ l3_lattices(sK3967_skl)
| v3_struct_0(sK3967_skl)
| ~ l3_lattices(sK3966_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f63572,f57545]) ).
fof(f63578,plain,
! [X0,X1] :
( r1_lattices(sK3966_skl,X0,X1)
| ~ r1_lattices(sK3967_skl,X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(sK3966_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK3966_skl))
| ~ m1_subset_1(X1,u1_struct_0(sK3967_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK3967_skl))
| ~ l3_lattices(sK3966_skl)
| v3_struct_0(sK3966_skl)
| ~ l3_lattices(sK3967_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f63573,f57547]) ).
fof(f63584,plain,
! [X0,X1] :
( k1_lattices(sK3966_skl,X0,X1) = k1_lattices(sK3967_skl,X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(sK3967_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK3967_skl))
| ~ m1_subset_1(X1,u1_struct_0(sK3966_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK3966_skl))
| ~ l3_lattices(sK3967_skl)
| v3_struct_0(sK3967_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f63559,f57546]) ).
fof(f63585,plain,
( ~ r1_lattices(sK3966_skl,sK3970_skl,sK3971_skl)
| sP322_prd(sK3971_skl,sK3970_skl,sK3971_skl,sK3970_skl,sK3967_skl,sK3966_skl)
| k2_lattices(sK3966_skl,sK3970_skl,sK3971_skl) != k2_lattices(sK3967_skl,sK3970_skl,sK3971_skl)
| ~ m1_subset_1(sK3971_skl,u1_struct_0(sK3967_skl))
| ~ m1_subset_1(sK3970_skl,u1_struct_0(sK3967_skl))
| ~ m1_subset_1(sK3971_skl,u1_struct_0(sK3966_skl))
| ~ m1_subset_1(sK3970_skl,u1_struct_0(sK3966_skl))
| ~ l3_lattices(sK3967_skl)
| v3_struct_0(sK3967_skl) ),
inference(resolution,[status(thm)],[f63584,f63527]) ).
fof(f63586,plain,
( r1_lattices(sK3967_skl,sK3970_skl,sK3971_skl)
| sP322_prd(sK3971_skl,sK3970_skl,sK3971_skl,sK3970_skl,sK3967_skl,sK3966_skl)
| k2_lattices(sK3966_skl,sK3970_skl,sK3971_skl) != k2_lattices(sK3967_skl,sK3970_skl,sK3971_skl)
| ~ m1_subset_1(sK3971_skl,u1_struct_0(sK3967_skl))
| ~ m1_subset_1(sK3970_skl,u1_struct_0(sK3967_skl))
| ~ m1_subset_1(sK3971_skl,u1_struct_0(sK3966_skl))
| ~ m1_subset_1(sK3970_skl,u1_struct_0(sK3966_skl))
| ~ l3_lattices(sK3967_skl)
| v3_struct_0(sK3967_skl) ),
inference(resolution,[status(thm)],[f63584,f63519]) ).
fof(f63587,plain,
( ~ r1_lattices(sK3966_skl,sK3970_skl,sK3971_skl)
| sP322_prd(sK3971_skl,sK3970_skl,sK3971_skl,sK3970_skl,sK3967_skl,sK3966_skl)
| k2_lattices(sK3966_skl,sK3970_skl,sK3971_skl) != k2_lattices(sK3967_skl,sK3970_skl,sK3971_skl)
| ~ m1_subset_1(sK3971_skl,u1_struct_0(sK3967_skl))
| ~ m1_subset_1(sK3970_skl,u1_struct_0(sK3967_skl))
| ~ m1_subset_1(sK3971_skl,u1_struct_0(sK3966_skl))
| ~ m1_subset_1(sK3970_skl,u1_struct_0(sK3966_skl))
| ~ l3_lattices(sK3967_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f63585,f57547]) ).
fof(f63588,plain,
( r1_lattices(sK3967_skl,sK3970_skl,sK3971_skl)
| sP322_prd(sK3971_skl,sK3970_skl,sK3971_skl,sK3970_skl,sK3967_skl,sK3966_skl)
| k2_lattices(sK3966_skl,sK3970_skl,sK3971_skl) != k2_lattices(sK3967_skl,sK3970_skl,sK3971_skl)
| ~ m1_subset_1(sK3971_skl,u1_struct_0(sK3967_skl))
| ~ m1_subset_1(sK3970_skl,u1_struct_0(sK3967_skl))
| ~ m1_subset_1(sK3971_skl,u1_struct_0(sK3966_skl))
| ~ m1_subset_1(sK3970_skl,u1_struct_0(sK3966_skl))
| ~ l3_lattices(sK3967_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f63586,f57547]) ).
fof(f63594,plain,
! [X0,X1] :
( k2_lattices(sK3966_skl,X0,X1) = k2_lattices(sK3967_skl,X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(sK3967_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK3967_skl))
| ~ m1_subset_1(X1,u1_struct_0(sK3966_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK3966_skl))
| ~ l3_lattices(sK3967_skl)
| v3_struct_0(sK3967_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f63568,f57546]) ).
fof(f63595,plain,
! [X0,X1] :
( k2_lattices(sK3967_skl,X0,X1) = k2_lattices(sK3966_skl,X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(sK3966_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK3966_skl))
| ~ m1_subset_1(X1,u1_struct_0(sK3967_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK3967_skl))
| ~ l3_lattices(sK3966_skl)
| v3_struct_0(sK3966_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f63569,f57548]) ).
fof(f63596,plain,
! [X0,X1] :
( r1_lattices(sK3967_skl,X0,X1)
| ~ r1_lattices(sK3966_skl,X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(sK3967_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK3967_skl))
| ~ m1_subset_1(X1,u1_struct_0(sK3966_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK3966_skl))
| ~ l3_lattices(sK3967_skl)
| v3_struct_0(sK3967_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f63577,f57546]) ).
fof(f63597,plain,
! [X0] :
( r1_lattices(sK3967_skl,X0,sK3971_skl)
| ~ r1_lattices(sK3966_skl,X0,sK3971_skl)
| ~ m1_subset_1(sK3971_skl,u1_struct_0(sK3967_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK3967_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK3966_skl))
| ~ l3_lattices(sK3967_skl)
| v3_struct_0(sK3967_skl) ),
inference(resolution,[status(thm)],[f63596,f63507]) ).
fof(f63599,plain,
! [X0] :
( r1_lattices(sK3967_skl,X0,sK3971_skl)
| ~ r1_lattices(sK3966_skl,X0,sK3971_skl)
| ~ m1_subset_1(sK3971_skl,u1_struct_0(sK3967_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK3967_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK3966_skl))
| ~ l3_lattices(sK3967_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f63597,f57547]) ).
fof(f63601,plain,
! [X0] :
( r1_lattices(sK3967_skl,X0,sK3971_skl)
| ~ r1_lattices(sK3966_skl,X0,sK3971_skl)
| ~ m1_subset_1(sK3971_skl,u1_struct_0(sK3967_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK3967_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK3966_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f63599,f57548]) ).
fof(f63602,plain,
! [X0] :
( r1_lattices(sK3967_skl,X0,sK3971_skl)
| ~ r1_lattices(sK3966_skl,X0,sK3971_skl)
| ~ m1_subset_1(X0,u1_struct_0(sK3967_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK3966_skl)) ),
inference(resolution,[status(thm)],[f63601,f57553]) ).
fof(f63604,plain,
( r1_lattices(sK3967_skl,sK3970_skl,sK3971_skl)
| ~ r1_lattices(sK3966_skl,sK3970_skl,sK3971_skl)
| ~ m1_subset_1(sK3970_skl,u1_struct_0(sK3967_skl)) ),
inference(resolution,[status(thm)],[f63602,f63506]) ).
fof(f63606,plain,
( r1_lattices(sK3967_skl,sK3970_skl,sK3971_skl)
| ~ r1_lattices(sK3966_skl,sK3970_skl,sK3971_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f63604,f57552]) ).
fof(f63619,plain,
! [X0,X1] :
( r1_lattices(sK3966_skl,X0,X1)
| ~ r1_lattices(sK3967_skl,X0,X1)
| ~ m1_subset_1(X1,u1_struct_0(sK3966_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK3966_skl))
| ~ m1_subset_1(X1,u1_struct_0(sK3967_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK3967_skl))
| ~ l3_lattices(sK3966_skl)
| v3_struct_0(sK3966_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f63578,f57548]) ).
fof(f63620,plain,
! [X0] :
( r1_lattices(sK3966_skl,X0,sK3971_skl)
| ~ r1_lattices(sK3967_skl,X0,sK3971_skl)
| ~ m1_subset_1(sK3971_skl,u1_struct_0(sK3966_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK3966_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK3967_skl))
| ~ l3_lattices(sK3966_skl)
| v3_struct_0(sK3966_skl) ),
inference(resolution,[status(thm)],[f63619,f57553]) ).
fof(f63629,plain,
! [X0] :
( r1_lattices(sK3966_skl,X0,sK3971_skl)
| ~ r1_lattices(sK3967_skl,X0,sK3971_skl)
| ~ m1_subset_1(sK3971_skl,u1_struct_0(sK3966_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK3966_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK3967_skl))
| ~ l3_lattices(sK3966_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f63620,f57545]) ).
fof(f63651,plain,
! [X0] :
( r1_lattices(sK3966_skl,X0,sK3971_skl)
| ~ r1_lattices(sK3967_skl,X0,sK3971_skl)
| ~ m1_subset_1(sK3971_skl,u1_struct_0(sK3966_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK3966_skl))
| ~ m1_subset_1(X0,u1_struct_0(sK3967_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f63629,f57546]) ).
fof(f63654,plain,
( r1_lattices(sK3966_skl,sK3970_skl,sK3971_skl)
| ~ r1_lattices(sK3967_skl,sK3970_skl,sK3971_skl)
| ~ m1_subset_1(sK3971_skl,u1_struct_0(sK3966_skl))
| ~ m1_subset_1(sK3970_skl,u1_struct_0(sK3967_skl)) ),
inference(resolution,[status(thm)],[f63651,f63506]) ).
fof(f63657,plain,
( r1_lattices(sK3966_skl,sK3970_skl,sK3971_skl)
| ~ r1_lattices(sK3967_skl,sK3970_skl,sK3971_skl)
| ~ m1_subset_1(sK3971_skl,u1_struct_0(sK3966_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f63654,f57552]) ).
fof(f63658,plain,
( r1_lattices(sK3966_skl,sK3970_skl,sK3971_skl)
| ~ r1_lattices(sK3967_skl,sK3970_skl,sK3971_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f63657,f63507]) ).
fof(f63727,plain,
( ~ r1_lattices(sK3966_skl,sK3970_skl,sK3971_skl)
| sP322_prd(sK3971_skl,sK3970_skl,sK3971_skl,sK3970_skl,sK3967_skl,sK3966_skl)
| k2_lattices(sK3966_skl,sK3970_skl,sK3971_skl) != k2_lattices(sK3967_skl,sK3970_skl,sK3971_skl)
| ~ m1_subset_1(sK3971_skl,u1_struct_0(sK3967_skl))
| ~ m1_subset_1(sK3970_skl,u1_struct_0(sK3967_skl))
| ~ m1_subset_1(sK3971_skl,u1_struct_0(sK3966_skl))
| ~ m1_subset_1(sK3970_skl,u1_struct_0(sK3966_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f63587,f57548]) ).
fof(f63729,plain,
( ~ m1_subset_1(sK3971_skl,u1_struct_0(sK3966_skl))
| ~ m1_subset_1(sK3970_skl,u1_struct_0(sK3966_skl))
| ~ m1_subset_1(sK3971_skl,u1_struct_0(sK3967_skl))
| ~ m1_subset_1(sK3970_skl,u1_struct_0(sK3967_skl))
| ~ l3_lattices(sK3966_skl)
| v3_struct_0(sK3966_skl)
| ~ r1_lattices(sK3966_skl,sK3970_skl,sK3971_skl)
| sP322_prd(sK3971_skl,sK3970_skl,sK3971_skl,sK3970_skl,sK3967_skl,sK3966_skl)
| ~ m1_subset_1(sK3971_skl,u1_struct_0(sK3967_skl))
| ~ m1_subset_1(sK3970_skl,u1_struct_0(sK3967_skl))
| ~ m1_subset_1(sK3971_skl,u1_struct_0(sK3966_skl))
| ~ m1_subset_1(sK3970_skl,u1_struct_0(sK3966_skl)) ),
inference(resolution,[status(thm)],[f63727,f63595]) ).
fof(f63732,plain,
( ~ l3_lattices(sK3966_skl)
| v3_struct_0(sK3966_skl)
| ~ r1_lattices(sK3966_skl,sK3970_skl,sK3971_skl)
| sP322_prd(sK3971_skl,sK3970_skl,sK3971_skl,sK3970_skl,sK3967_skl,sK3966_skl)
| ~ m1_subset_1(sK3971_skl,u1_struct_0(sK3967_skl))
| ~ m1_subset_1(sK3970_skl,u1_struct_0(sK3967_skl))
| ~ m1_subset_1(sK3971_skl,u1_struct_0(sK3966_skl))
| ~ m1_subset_1(sK3970_skl,u1_struct_0(sK3966_skl)) ),
inference(duplicate_literals_removal,[status(thm)],[f63729]) ).
fof(f63733,plain,
( ~ l3_lattices(sK3966_skl)
| v3_struct_0(sK3966_skl)
| ~ r1_lattices(sK3966_skl,sK3970_skl,sK3971_skl)
| sP322_prd(sK3971_skl,sK3970_skl,sK3971_skl,sK3970_skl,sK3967_skl,sK3966_skl)
| ~ m1_subset_1(sK3971_skl,u1_struct_0(sK3967_skl))
| ~ m1_subset_1(sK3970_skl,u1_struct_0(sK3967_skl))
| ~ m1_subset_1(sK3971_skl,u1_struct_0(sK3966_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f63732,f63506]) ).
fof(f63742,plain,
( ~ l3_lattices(sK3966_skl)
| v3_struct_0(sK3966_skl)
| ~ r1_lattices(sK3966_skl,sK3970_skl,sK3971_skl)
| sP322_prd(sK3971_skl,sK3970_skl,sK3971_skl,sK3970_skl,sK3967_skl,sK3966_skl)
| ~ m1_subset_1(sK3971_skl,u1_struct_0(sK3967_skl))
| ~ m1_subset_1(sK3970_skl,u1_struct_0(sK3967_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f63733,f63507]) ).
fof(f63743,plain,
( ~ r1_lattices(sK3967_skl,sK3970_skl,sK3971_skl)
| ~ l3_lattices(sK3966_skl)
| v3_struct_0(sK3966_skl)
| ~ r1_lattices(sK3966_skl,sK3970_skl,sK3971_skl)
| ~ m1_subset_1(sK3971_skl,u1_struct_0(sK3967_skl))
| ~ m1_subset_1(sK3970_skl,u1_struct_0(sK3967_skl)) ),
inference(resolution,[status(thm)],[f63742,f59934]) ).
fof(f63745,plain,
( ~ r1_lattices(sK3967_skl,sK3970_skl,sK3971_skl)
| ~ l3_lattices(sK3966_skl)
| v3_struct_0(sK3966_skl)
| ~ r1_lattices(sK3966_skl,sK3970_skl,sK3971_skl)
| ~ m1_subset_1(sK3971_skl,u1_struct_0(sK3967_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f63743,f57552]) ).
fof(f63746,plain,
( ~ r1_lattices(sK3967_skl,sK3970_skl,sK3971_skl)
| ~ l3_lattices(sK3966_skl)
| v3_struct_0(sK3966_skl)
| ~ r1_lattices(sK3966_skl,sK3970_skl,sK3971_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f63745,f57553]) ).
fof(f63747,plain,
( r1_lattices(sK3967_skl,sK3970_skl,sK3971_skl)
| sP322_prd(sK3971_skl,sK3970_skl,sK3971_skl,sK3970_skl,sK3967_skl,sK3966_skl)
| k2_lattices(sK3966_skl,sK3970_skl,sK3971_skl) != k2_lattices(sK3967_skl,sK3970_skl,sK3971_skl)
| ~ m1_subset_1(sK3971_skl,u1_struct_0(sK3967_skl))
| ~ m1_subset_1(sK3970_skl,u1_struct_0(sK3967_skl))
| ~ m1_subset_1(sK3971_skl,u1_struct_0(sK3966_skl))
| ~ m1_subset_1(sK3970_skl,u1_struct_0(sK3966_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f63588,f57548]) ).
fof(f63748,plain,
( ~ m1_subset_1(sK3971_skl,u1_struct_0(sK3967_skl))
| ~ m1_subset_1(sK3970_skl,u1_struct_0(sK3967_skl))
| ~ m1_subset_1(sK3971_skl,u1_struct_0(sK3966_skl))
| ~ m1_subset_1(sK3970_skl,u1_struct_0(sK3966_skl))
| ~ l3_lattices(sK3967_skl)
| v3_struct_0(sK3967_skl)
| r1_lattices(sK3967_skl,sK3970_skl,sK3971_skl)
| sP322_prd(sK3971_skl,sK3970_skl,sK3971_skl,sK3970_skl,sK3967_skl,sK3966_skl)
| ~ m1_subset_1(sK3971_skl,u1_struct_0(sK3967_skl))
| ~ m1_subset_1(sK3970_skl,u1_struct_0(sK3967_skl))
| ~ m1_subset_1(sK3971_skl,u1_struct_0(sK3966_skl))
| ~ m1_subset_1(sK3970_skl,u1_struct_0(sK3966_skl)) ),
inference(resolution,[status(thm)],[f63747,f63594]) ).
fof(f63750,plain,
( ~ l3_lattices(sK3967_skl)
| v3_struct_0(sK3967_skl)
| r1_lattices(sK3967_skl,sK3970_skl,sK3971_skl)
| sP322_prd(sK3971_skl,sK3970_skl,sK3971_skl,sK3970_skl,sK3967_skl,sK3966_skl)
| ~ m1_subset_1(sK3971_skl,u1_struct_0(sK3967_skl))
| ~ m1_subset_1(sK3970_skl,u1_struct_0(sK3967_skl))
| ~ m1_subset_1(sK3971_skl,u1_struct_0(sK3966_skl))
| ~ m1_subset_1(sK3970_skl,u1_struct_0(sK3966_skl)) ),
inference(duplicate_literals_removal,[status(thm)],[f63748]) ).
fof(f63751,plain,
( ~ l3_lattices(sK3967_skl)
| v3_struct_0(sK3967_skl)
| r1_lattices(sK3967_skl,sK3970_skl,sK3971_skl)
| sP322_prd(sK3971_skl,sK3970_skl,sK3971_skl,sK3970_skl,sK3967_skl,sK3966_skl)
| ~ m1_subset_1(sK3971_skl,u1_struct_0(sK3967_skl))
| ~ m1_subset_1(sK3970_skl,u1_struct_0(sK3967_skl))
| ~ m1_subset_1(sK3971_skl,u1_struct_0(sK3966_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f63750,f63506]) ).
fof(f63754,plain,
( ~ l3_lattices(sK3967_skl)
| v3_struct_0(sK3967_skl)
| r1_lattices(sK3967_skl,sK3970_skl,sK3971_skl)
| sP322_prd(sK3971_skl,sK3970_skl,sK3971_skl,sK3970_skl,sK3967_skl,sK3966_skl)
| ~ m1_subset_1(sK3971_skl,u1_struct_0(sK3967_skl))
| ~ m1_subset_1(sK3970_skl,u1_struct_0(sK3967_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f63751,f63507]) ).
fof(f63756,plain,
( r1_lattices(sK3966_skl,sK3970_skl,sK3971_skl)
| ~ l3_lattices(sK3967_skl)
| v3_struct_0(sK3967_skl)
| r1_lattices(sK3967_skl,sK3970_skl,sK3971_skl)
| ~ m1_subset_1(sK3971_skl,u1_struct_0(sK3967_skl))
| ~ m1_subset_1(sK3970_skl,u1_struct_0(sK3967_skl)) ),
inference(resolution,[status(thm)],[f63754,f59933]) ).
fof(f63757,plain,
( r1_lattices(sK3966_skl,sK3970_skl,sK3971_skl)
| ~ l3_lattices(sK3967_skl)
| v3_struct_0(sK3967_skl)
| r1_lattices(sK3967_skl,sK3970_skl,sK3971_skl)
| ~ m1_subset_1(sK3971_skl,u1_struct_0(sK3967_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f63756,f57552]) ).
fof(f63758,plain,
( r1_lattices(sK3966_skl,sK3970_skl,sK3971_skl)
| ~ l3_lattices(sK3967_skl)
| v3_struct_0(sK3967_skl)
| r1_lattices(sK3967_skl,sK3970_skl,sK3971_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f63757,f57553]) ).
fof(f63761,plain,
( r1_lattices(sK3967_skl,sK3970_skl,sK3971_skl)
| ~ l3_lattices(sK3967_skl)
| v3_struct_0(sK3967_skl)
| r1_lattices(sK3967_skl,sK3970_skl,sK3971_skl) ),
inference(resolution,[status(thm)],[f63758,f63606]) ).
fof(f63762,plain,
( ~ l3_lattices(sK3967_skl)
| v3_struct_0(sK3967_skl)
| r1_lattices(sK3967_skl,sK3970_skl,sK3971_skl) ),
inference(duplicate_literals_removal,[status(thm)],[f63761]) ).
fof(f63763,plain,
( ~ l3_lattices(sK3967_skl)
| r1_lattices(sK3967_skl,sK3970_skl,sK3971_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f63762,f57547]) ).
fof(f63764,plain,
( ~ l3_lattices(sK3966_skl)
| v3_struct_0(sK3966_skl)
| ~ r1_lattices(sK3966_skl,sK3970_skl,sK3971_skl) ),
inference(backward_subsumption_resolution,[status(thm)],[f63746,f63767]) ).
fof(f63766,plain,
r1_lattices(sK3966_skl,sK3970_skl,sK3971_skl),
inference(backward_subsumption_resolution,[status(thm)],[f63658,f63767]) ).
fof(f63767,plain,
r1_lattices(sK3967_skl,sK3970_skl,sK3971_skl),
inference(forward_subsumption_resolution,[status(thm)],[f63763,f57548]) ).
fof(f63768,plain,
( ~ l3_lattices(sK3966_skl)
| ~ r1_lattices(sK3966_skl,sK3970_skl,sK3971_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f63764,f57545]) ).
fof(f63790,plain,
~ l3_lattices(sK3966_skl),
inference(forward_subsumption_resolution,[status(thm)],[f63768,f63766]) ).
fof(f63791,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[f57546,f63790]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : LAT295+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.14/0.41 % Computer : n008.cluster.edu
% 0.14/0.41 % Model : x86_64 x86_64
% 0.14/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.41 % Memory : 8046.5625MB
% 0.14/0.41 % OS : Linux 6.8.0-71-generic
% 0.14/0.41 % CPULimit : 300
% 0.14/0.41 % WCLimit : 300
% 0.14/0.41 % DateTime : Sun Sep 20 23:29:41 UTC 2026
% 0.14/0.41 % CPUTime :
% 1.89/2.28 % Drodi V4.1.1
% 2.15/3.26 % Refutation found
% 2.15/3.26 % SZS status Theorem for theBenchmark: Theorem is valid
% 2.15/3.26 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 2.27/3.63 % Elapsed time: 3.163208 seconds
% 2.27/3.63 % CPU time: 9.778078 seconds
% 2.27/3.63 % Total memory used: 3.816 GB
% 2.27/3.63 % Net memory used: 3.793 GB
%------------------------------------------------------------------------------