%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LAT295+3 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -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:03:33 PM UTC 2026
% Result : Theorem 1.95s 2.61s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT295+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.07/0.35 % Computer : n002.cluster.edu
% 0.07/0.35 % Model : x86_64 x86_64
% 0.07/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.35 % Memory : 8046.5625MB
% 0.07/0.35 % OS : Linux 6.8.0-71-generic
% 0.07/0.35 % CPULimit : 300
% 0.07/0.35 % WCLimit : 300
% 0.07/0.35 % DateTime : Sun Sep 20 23:31:36 UTC 2026
% 0.12/0.36 % CPUTime :
% 1.78/2.05 % Drodi V4.1.1
% 1.95/2.61 % Refutation found
% 1.95/2.61 % SZS status Theorem for theBenchmark: Theorem is valid
% 1.95/2.61 % SZS output start CNFRefutation for theBenchmark
% 1.95/2.61 fof(f13132,axiom,(
% 1.95/2.61 (! [A] :( ( ~ v3_struct_0(A)& l3_lattices(A) )=> (! [B] :( ( ~ v3_struct_0(B)& l3_lattices(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))=> ( ( C = E& D = F )=> ( k1_lattices(A,C,D) = k1_lattices(B,E,F)& k2_lattices(A,C,D) = k2_lattices(B,E,F)& ( r1_lattices(A,C,D)=> r1_lattices(B,E,F) )& ( r1_lattices(B,E,F)=> r1_lattices(A,C,D) ) ) ) ) )) )) )) )) ) )) )),
% 1.95/2.61 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.95/2.61 fof(f13583,conjecture,(
% 1.95/2.61 (! [A] :( ( ~ v3_struct_0(A)& l3_lattices(A) )=> (! [B] :( ( ~ v3_struct_0(B)& l3_lattices(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))=> ( ( C = E& D = F )=> ( k1_lattices(A,C,D) = k1_lattices(B,E,F)& k2_lattices(A,C,D) = k2_lattices(B,E,F)& ( r1_lattices(A,C,D)=> r1_lattices(B,E,F) )& ( r1_lattices(B,E,F)=> r1_lattices(A,C,D) ) ) ) ) )) )) )) )) ) )) )),
% 1.95/2.61 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 1.95/2.61 fof(f13584,negated_conjecture,(
% 1.95/2.61 ~((! [A] :( ( ~ v3_struct_0(A)& l3_lattices(A) )=> (! [B] :( ( ~ v3_struct_0(B)& l3_lattices(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))=> ( ( C = E& D = F )=> ( k1_lattices(A,C,D) = k1_lattices(B,E,F)& k2_lattices(A,C,D) = k2_lattices(B,E,F)& ( r1_lattices(A,C,D)=> r1_lattices(B,E,F) )& ( r1_lattices(B,E,F)=> r1_lattices(A,C,D) ) ) ) ) )) )) )) )) ) )) ))),
% 1.95/2.61 inference(negated_conjecture,[status(cth)],[f13583])).
% 1.95/2.61 fof(f55595,plain,(
% 1.95/2.61 ![A]: ((v3_struct_0(A)|~l3_lattices(A))|(![B]: ((v3_struct_0(B)|~l3_lattices(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))|((~C=E|~D=F)|(((k1_lattices(A,C,D)=k1_lattices(B,E,F)&k2_lattices(A,C,D)=k2_lattices(B,E,F))&(~r1_lattices(A,C,D)|r1_lattices(B,E,F)))&(~r1_lattices(B,E,F)|r1_lattices(A,C,D))))))))))))))))),
% 1.95/2.61 inference(pre_NNF_transformation,[status(thm)],[f13132])).
% 1.95/2.61 fof(f55596,plain,(
% 1.95/2.61 ![X0,X1,X2,X3,X4,X5]: (v3_struct_0(X0)|~l3_lattices(X0)|v3_struct_0(X1)|~l3_lattices(X1)|~g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))=g3_lattices(u1_struct_0(X1),u2_lattices(X1),u1_lattices(X1))|~m1_subset_1(X2,u1_struct_0(X0))|~m1_subset_1(X3,u1_struct_0(X0))|~m1_subset_1(X4,u1_struct_0(X1))|~m1_subset_1(X5,u1_struct_0(X1))|~X2=X4|~X3=X5|k1_lattices(X0,X2,X3)=k1_lattices(X1,X4,X5))),
% 1.95/2.61 inference(cnf_transformation,[status(thm)],[f55595])).
% 1.95/2.61 fof(f55597,plain,(
% 1.95/2.61 ![X0,X1,X2,X3,X4,X5]: (v3_struct_0(X0)|~l3_lattices(X0)|v3_struct_0(X1)|~l3_lattices(X1)|~g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))=g3_lattices(u1_struct_0(X1),u2_lattices(X1),u1_lattices(X1))|~m1_subset_1(X2,u1_struct_0(X0))|~m1_subset_1(X3,u1_struct_0(X0))|~m1_subset_1(X4,u1_struct_0(X1))|~m1_subset_1(X5,u1_struct_0(X1))|~X2=X4|~X3=X5|k2_lattices(X0,X2,X3)=k2_lattices(X1,X4,X5))),
% 1.95/2.61 inference(cnf_transformation,[status(thm)],[f55595])).
% 1.95/2.61 fof(f55598,plain,(
% 1.95/2.61 ![X0,X1,X2,X3,X4,X5]: (v3_struct_0(X0)|~l3_lattices(X0)|v3_struct_0(X1)|~l3_lattices(X1)|~g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))=g3_lattices(u1_struct_0(X1),u2_lattices(X1),u1_lattices(X1))|~m1_subset_1(X2,u1_struct_0(X0))|~m1_subset_1(X3,u1_struct_0(X0))|~m1_subset_1(X4,u1_struct_0(X1))|~m1_subset_1(X5,u1_struct_0(X1))|~X2=X4|~X3=X5|~r1_lattices(X0,X2,X3)|r1_lattices(X1,X4,X5))),
% 1.95/2.61 inference(cnf_transformation,[status(thm)],[f55595])).
% 1.95/2.61 fof(f57541,plain,(
% 1.95/2.61 (?[A]: ((~v3_struct_0(A)&l3_lattices(A))&(?[B]: ((~v3_struct_0(B)&l3_lattices(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))&((C=E&D=F)&(((~k1_lattices(A,C,D)=k1_lattices(B,E,F)|~k2_lattices(A,C,D)=k2_lattices(B,E,F))|(r1_lattices(A,C,D)&~r1_lattices(B,E,F)))|(r1_lattices(B,E,F)&~r1_lattices(A,C,D)))))))))))))))))),
% 1.95/2.61 inference(pre_NNF_transformation,[status(thm)],[f13584])).
% 1.95/2.61 fof(f57542,definition,(
% 1.95/2.61 ![A,B,C,D,E,F]: (sP322_prd(F,E,D,C,B,A)<=>(r1_lattices(A,C,D)&~r1_lattices(B,E,F)))),
% 1.95/2.61 introduced(definition,[new_symbols(definition,[sP322_prd])],[])).
% 1.95/2.61 fof(f57543,plain,(
% 1.95/2.61 ?[A]: ((~v3_struct_0(A)&l3_lattices(A))&(?[B]: ((~v3_struct_0(B)&l3_lattices(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))&((C=E&D=F)&(((~k1_lattices(A,C,D)=k1_lattices(B,E,F)|~k2_lattices(A,C,D)=k2_lattices(B,E,F))|sP322_prd(F,E,D,C,B,A))|(r1_lattices(B,E,F)&~r1_lattices(A,C,D))))))))))))))))),
% 1.95/2.61 inference(formula_renaming,[status(thm)],[f57541,f57542])).
% 1.95/2.61 fof(f57544,plain,(
% 1.95/2.61 ((~v3_struct_0(sK3966_skl)&l3_lattices(sK3966_skl))&((~v3_struct_0(sK3967_skl)&l3_lattices(sK3967_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))&(m1_subset_1(sK3968_skl,u1_struct_0(sK3966_skl))&(m1_subset_1(sK3969_skl,u1_struct_0(sK3966_skl))&(m1_subset_1(sK3970_skl,u1_struct_0(sK3967_skl))&(m1_subset_1(sK3971_skl,u1_struct_0(sK3967_skl))&((sK3968_skl=sK3970_skl&sK3969_skl=sK3971_skl)&(((~k1_lattices(sK3966_skl,sK3968_skl,sK3969_skl)=k1_lattices(sK3967_skl,sK3970_skl,sK3971_skl)|~k2_lattices(sK3966_skl,sK3968_skl,sK3969_skl)=k2_lattices(sK3967_skl,sK3970_skl,sK3971_skl))|sP322_prd(sK3971_skl,sK3970_skl,sK3969_skl,sK3968_skl,sK3967_skl,sK3966_skl))|(r1_lattices(sK3967_skl,sK3970_skl,sK3971_skl)&~r1_lattices(sK3966_skl,sK3968_skl,sK3969_skl)))))))))))),
% 1.95/2.61 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])).
% 1.95/2.61 fof(f57545,plain,(
% 1.95/2.61 ~v3_struct_0(sK3966_skl)),
% 1.95/2.61 inference(cnf_transformation,[status(thm)],[f57544])).
% 1.95/2.61 fof(f57546,plain,(
% 1.95/2.61 l3_lattices(sK3966_skl)),
% 1.95/2.61 inference(cnf_transformation,[status(thm)],[f57544])).
% 1.95/2.61 fof(f57547,plain,(
% 1.95/2.61 ~v3_struct_0(sK3967_skl)),
% 1.95/2.61 inference(cnf_transformation,[status(thm)],[f57544])).
% 1.95/2.61 fof(f57548,plain,(
% 1.95/2.61 l3_lattices(sK3967_skl)),
% 1.95/2.61 inference(cnf_transformation,[status(thm)],[f57544])).
% 1.95/2.61 fof(f57549,plain,(
% 1.95/2.61 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))),
% 1.95/2.61 inference(cnf_transformation,[status(thm)],[f57544])).
% 1.95/2.61 fof(f57550,plain,(
% 1.95/2.61 m1_subset_1(sK3968_skl,u1_struct_0(sK3966_skl))),
% 1.95/2.61 inference(cnf_transformation,[status(thm)],[f57544])).
% 1.95/2.61 fof(f57551,plain,(
% 1.95/2.61 m1_subset_1(sK3969_skl,u1_struct_0(sK3966_skl))),
% 1.95/2.61 inference(cnf_transformation,[status(thm)],[f57544])).
% 1.95/2.61 fof(f57552,plain,(
% 1.95/2.61 m1_subset_1(sK3970_skl,u1_struct_0(sK3967_skl))),
% 1.95/2.61 inference(cnf_transformation,[status(thm)],[f57544])).
% 1.95/2.61 fof(f57553,plain,(
% 1.95/2.61 m1_subset_1(sK3971_skl,u1_struct_0(sK3967_skl))),
% 1.95/2.61 inference(cnf_transformation,[status(thm)],[f57544])).
% 1.95/2.61 fof(f57554,plain,(
% 1.95/2.61 sK3968_skl=sK3970_skl),
% 1.95/2.61 inference(cnf_transformation,[status(thm)],[f57544])).
% 1.95/2.61 fof(f57555,plain,(
% 1.95/2.61 sK3969_skl=sK3971_skl),
% 1.95/2.61 inference(cnf_transformation,[status(thm)],[f57544])).
% 1.95/2.61 fof(f57556,plain,(
% 1.95/2.61 ~k1_lattices(sK3966_skl,sK3968_skl,sK3969_skl)=k1_lattices(sK3967_skl,sK3970_skl,sK3971_skl)|~k2_lattices(sK3966_skl,sK3968_skl,sK3969_skl)=k2_lattices(sK3967_skl,sK3970_skl,sK3971_skl)|sP322_prd(sK3971_skl,sK3970_skl,sK3969_skl,sK3968_skl,sK3967_skl,sK3966_skl)|r1_lattices(sK3967_skl,sK3970_skl,sK3971_skl)),
% 1.95/2.61 inference(cnf_transformation,[status(thm)],[f57544])).
% 1.95/2.61 fof(f57557,plain,(
% 1.95/2.61 ~k1_lattices(sK3966_skl,sK3968_skl,sK3969_skl)=k1_lattices(sK3967_skl,sK3970_skl,sK3971_skl)|~k2_lattices(sK3966_skl,sK3968_skl,sK3969_skl)=k2_lattices(sK3967_skl,sK3970_skl,sK3971_skl)|sP322_prd(sK3971_skl,sK3970_skl,sK3969_skl,sK3968_skl,sK3967_skl,sK3966_skl)|~r1_lattices(sK3966_skl,sK3968_skl,sK3969_skl)),
% 1.95/2.61 inference(cnf_transformation,[status(thm)],[f57544])).
% 1.95/2.61 fof(f59931,plain,(
% 1.95/2.61 ![A,B,C,D,E,F]: ((~sP322_prd(F,E,D,C,B,A)|(r1_lattices(A,C,D)&~r1_lattices(B,E,F)))&(sP322_prd(F,E,D,C,B,A)|(~r1_lattices(A,C,D)|r1_lattices(B,E,F))))),
% 1.95/2.61 inference(NNF_transformation,[status(thm)],[f57542])).
% 1.95/2.61 fof(f59932,plain,(
% 1.95/2.61 (![A,B,C,D,E,F]: (~sP322_prd(F,E,D,C,B,A)|(r1_lattices(A,C,D)&~r1_lattices(B,E,F))))&(![A,B,C,D,E,F]: (sP322_prd(F,E,D,C,B,A)|(~r1_lattices(A,C,D)|r1_lattices(B,E,F))))),
% 1.95/2.61 inference(miniscoping,[status(thm)],[f59931])).
% 1.95/2.61 fof(f59933,plain,(
% 1.95/2.61 ![X0,X1,X2,X3,X4,X5]: (~sP322_prd(X0,X1,X2,X3,X4,X5)|r1_lattices(X5,X3,X2))),
% 1.95/2.61 inference(cnf_transformation,[status(thm)],[f59932])).
% 1.95/2.61 fof(f59934,plain,(
% 1.95/2.61 ![X0,X1,X2,X3,X4,X5]: (~sP322_prd(X0,X1,X2,X3,X4,X5)|~r1_lattices(X4,X1,X0))),
% 1.95/2.61 inference(cnf_transformation,[status(thm)],[f59932])).
% 1.95/2.61 fof(f63117,plain,(
% 1.95/2.61 ![X0,X1,X2,X3]: (v3_struct_0(X0)|~l3_lattices(X0)|v3_struct_0(X1)|~l3_lattices(X1)|~g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))=g3_lattices(u1_struct_0(X1),u2_lattices(X1),u1_lattices(X1))|~m1_subset_1(X2,u1_struct_0(X0))|~m1_subset_1(X3,u1_struct_0(X0))|~m1_subset_1(X2,u1_struct_0(X1))|~m1_subset_1(X3,u1_struct_0(X1))|k1_lattices(X0,X2,X3)=k1_lattices(X1,X2,X3))),
% 1.95/2.61 inference(destructive_equality_resolution,[status(thm)],[f55596])).
% 1.95/2.61 fof(f63118,plain,(
% 1.95/2.61 ![X0,X1,X2,X3]: (v3_struct_0(X0)|~l3_lattices(X0)|v3_struct_0(X1)|~l3_lattices(X1)|~g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))=g3_lattices(u1_struct_0(X1),u2_lattices(X1),u1_lattices(X1))|~m1_subset_1(X2,u1_struct_0(X0))|~m1_subset_1(X3,u1_struct_0(X0))|~m1_subset_1(X2,u1_struct_0(X1))|~m1_subset_1(X3,u1_struct_0(X1))|k2_lattices(X0,X2,X3)=k2_lattices(X1,X2,X3))),
% 1.95/2.61 inference(destructive_equality_resolution,[status(thm)],[f55597])).
% 1.95/2.61 fof(f63119,plain,(
% 1.95/2.61 ![X0,X1,X2,X3]: (v3_struct_0(X0)|~l3_lattices(X0)|v3_struct_0(X1)|~l3_lattices(X1)|~g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))=g3_lattices(u1_struct_0(X1),u2_lattices(X1),u1_lattices(X1))|~m1_subset_1(X2,u1_struct_0(X0))|~m1_subset_1(X3,u1_struct_0(X0))|~m1_subset_1(X2,u1_struct_0(X1))|~m1_subset_1(X3,u1_struct_0(X1))|~r1_lattices(X0,X2,X3)|r1_lattices(X1,X2,X3))),
% 1.95/2.61 inference(destructive_equality_resolution,[status(thm)],[f55598])).
% 1.95/2.61 fof(f63521,plain,(
% 1.95/2.61 m1_subset_1(sK3968_skl,u1_struct_0(sK3967_skl))),
% 1.95/2.61 inference(forward_demodulation,[status(thm)],[f57554,f57552])).
% 1.95/2.61 fof(f63523,plain,(
% 1.95/2.61 ![X0,X1,X2]: (v3_struct_0(X0)|~l3_lattices(X0)|v3_struct_0(sK3967_skl)|~g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))=g3_lattices(u1_struct_0(sK3967_skl),u2_lattices(sK3967_skl),u1_lattices(sK3967_skl))|~m1_subset_1(X1,u1_struct_0(X0))|~m1_subset_1(X2,u1_struct_0(X0))|~m1_subset_1(X1,u1_struct_0(sK3967_skl))|~m1_subset_1(X2,u1_struct_0(sK3967_skl))|k1_lattices(X0,X1,X2)=k1_lattices(sK3967_skl,X1,X2))),
% 1.95/2.61 inference(resolution,[status(thm)],[f63117,f57548])).
% 1.95/2.61 fof(f63525,plain,(
% 1.95/2.61 ![X0,X1,X2]: (v3_struct_0(X0)|~l3_lattices(X0)|v3_struct_0(sK3967_skl)|~g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))=g3_lattices(u1_struct_0(sK3966_skl),u2_lattices(sK3966_skl),u1_lattices(sK3966_skl))|~m1_subset_1(X1,u1_struct_0(X0))|~m1_subset_1(X2,u1_struct_0(X0))|~m1_subset_1(X1,u1_struct_0(sK3967_skl))|~m1_subset_1(X2,u1_struct_0(sK3967_skl))|k1_lattices(X0,X1,X2)=k1_lattices(sK3967_skl,X1,X2))),
% 1.95/2.61 inference(forward_demodulation,[status(thm)],[f57549,f63523])).
% 1.95/2.61 fof(f63526,plain,(
% 1.95/2.61 ![X0,X1,X2]: (v3_struct_0(X0)|~l3_lattices(X0)|~g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))=g3_lattices(u1_struct_0(sK3966_skl),u2_lattices(sK3966_skl),u1_lattices(sK3966_skl))|~m1_subset_1(X1,u1_struct_0(X0))|~m1_subset_1(X2,u1_struct_0(X0))|~m1_subset_1(X1,u1_struct_0(sK3967_skl))|~m1_subset_1(X2,u1_struct_0(sK3967_skl))|k1_lattices(X0,X1,X2)=k1_lattices(sK3967_skl,X1,X2))),
% 1.95/2.61 inference(forward_subsumption_resolution,[status(thm)],[f63525,f57547])).
% 1.95/2.61 fof(f63529,plain,(
% 1.95/2.61 ![X0,X1,X2]: (v3_struct_0(X0)|~l3_lattices(X0)|v3_struct_0(sK3967_skl)|~g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))=g3_lattices(u1_struct_0(sK3967_skl),u2_lattices(sK3967_skl),u1_lattices(sK3967_skl))|~m1_subset_1(X1,u1_struct_0(X0))|~m1_subset_1(X2,u1_struct_0(X0))|~m1_subset_1(X1,u1_struct_0(sK3967_skl))|~m1_subset_1(X2,u1_struct_0(sK3967_skl))|k2_lattices(X0,X1,X2)=k2_lattices(sK3967_skl,X1,X2))),
% 1.95/2.61 inference(resolution,[status(thm)],[f63118,f57548])).
% 1.95/2.61 fof(f63531,plain,(
% 1.95/2.61 ![X0,X1,X2]: (v3_struct_0(X0)|~l3_lattices(X0)|v3_struct_0(sK3967_skl)|~g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))=g3_lattices(u1_struct_0(sK3966_skl),u2_lattices(sK3966_skl),u1_lattices(sK3966_skl))|~m1_subset_1(X1,u1_struct_0(X0))|~m1_subset_1(X2,u1_struct_0(X0))|~m1_subset_1(X1,u1_struct_0(sK3967_skl))|~m1_subset_1(X2,u1_struct_0(sK3967_skl))|k2_lattices(X0,X1,X2)=k2_lattices(sK3967_skl,X1,X2))),
% 1.95/2.61 inference(forward_demodulation,[status(thm)],[f57549,f63529])).
% 1.95/2.61 fof(f63532,plain,(
% 1.95/2.61 ![X0,X1,X2]: (v3_struct_0(X0)|~l3_lattices(X0)|~g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))=g3_lattices(u1_struct_0(sK3966_skl),u2_lattices(sK3966_skl),u1_lattices(sK3966_skl))|~m1_subset_1(X1,u1_struct_0(X0))|~m1_subset_1(X2,u1_struct_0(X0))|~m1_subset_1(X1,u1_struct_0(sK3967_skl))|~m1_subset_1(X2,u1_struct_0(sK3967_skl))|k2_lattices(X0,X1,X2)=k2_lattices(sK3967_skl,X1,X2))),
% 1.95/2.61 inference(forward_subsumption_resolution,[status(thm)],[f63531,f57547])).
% 1.95/2.61 fof(f63546,plain,(
% 1.95/2.61 m1_subset_1(sK3969_skl,u1_struct_0(sK3967_skl))),
% 1.95/2.61 inference(forward_demodulation,[status(thm)],[f57555,f57553])).
% 1.95/2.61 fof(f63547,plain,(
% 1.95/2.61 ~k1_lattices(sK3966_skl,sK3968_skl,sK3969_skl)=k1_lattices(sK3967_skl,sK3968_skl,sK3971_skl)|~k2_lattices(sK3966_skl,sK3968_skl,sK3969_skl)=k2_lattices(sK3967_skl,sK3970_skl,sK3971_skl)|sP322_prd(sK3971_skl,sK3970_skl,sK3969_skl,sK3968_skl,sK3967_skl,sK3966_skl)|r1_lattices(sK3967_skl,sK3970_skl,sK3971_skl)),
% 1.95/2.61 inference(forward_demodulation,[status(thm)],[f57554,f57556])).
% 1.95/2.61 fof(f63548,plain,(
% 1.95/2.61 ~k1_lattices(sK3966_skl,sK3968_skl,sK3969_skl)=k1_lattices(sK3967_skl,sK3968_skl,sK3969_skl)|~k2_lattices(sK3966_skl,sK3968_skl,sK3969_skl)=k2_lattices(sK3967_skl,sK3970_skl,sK3971_skl)|sP322_prd(sK3971_skl,sK3970_skl,sK3969_skl,sK3968_skl,sK3967_skl,sK3966_skl)|r1_lattices(sK3967_skl,sK3970_skl,sK3971_skl)),
% 1.95/2.61 inference(forward_demodulation,[status(thm)],[f57555,f63547])).
% 1.95/2.61 fof(f63549,plain,(
% 1.95/2.61 ~k1_lattices(sK3966_skl,sK3968_skl,sK3969_skl)=k1_lattices(sK3967_skl,sK3968_skl,sK3969_skl)|~k2_lattices(sK3966_skl,sK3968_skl,sK3969_skl)=k2_lattices(sK3967_skl,sK3968_skl,sK3971_skl)|sP322_prd(sK3971_skl,sK3970_skl,sK3969_skl,sK3968_skl,sK3967_skl,sK3966_skl)|r1_lattices(sK3967_skl,sK3970_skl,sK3971_skl)),
% 1.95/2.61 inference(forward_demodulation,[status(thm)],[f57554,f63548])).
% 1.95/2.61 fof(f63550,plain,(
% 1.95/2.61 ~k1_lattices(sK3966_skl,sK3968_skl,sK3969_skl)=k1_lattices(sK3967_skl,sK3968_skl,sK3969_skl)|~k2_lattices(sK3966_skl,sK3968_skl,sK3969_skl)=k2_lattices(sK3967_skl,sK3968_skl,sK3969_skl)|sP322_prd(sK3971_skl,sK3970_skl,sK3969_skl,sK3968_skl,sK3967_skl,sK3966_skl)|r1_lattices(sK3967_skl,sK3970_skl,sK3971_skl)),
% 1.95/2.61 inference(forward_demodulation,[status(thm)],[f57555,f63549])).
% 1.95/2.61 fof(f63551,plain,(
% 1.95/2.61 ~k1_lattices(sK3966_skl,sK3968_skl,sK3969_skl)=k1_lattices(sK3967_skl,sK3968_skl,sK3969_skl)|~k2_lattices(sK3966_skl,sK3968_skl,sK3969_skl)=k2_lattices(sK3967_skl,sK3968_skl,sK3969_skl)|sP322_prd(sK3969_skl,sK3970_skl,sK3969_skl,sK3968_skl,sK3967_skl,sK3966_skl)|r1_lattices(sK3967_skl,sK3970_skl,sK3971_skl)),
% 1.95/2.61 inference(forward_demodulation,[status(thm)],[f57555,f63550])).
% 1.95/2.61 fof(f63552,plain,(
% 1.95/2.61 ~k1_lattices(sK3966_skl,sK3968_skl,sK3969_skl)=k1_lattices(sK3967_skl,sK3968_skl,sK3969_skl)|~k2_lattices(sK3966_skl,sK3968_skl,sK3969_skl)=k2_lattices(sK3967_skl,sK3968_skl,sK3969_skl)|sP322_prd(sK3969_skl,sK3968_skl,sK3969_skl,sK3968_skl,sK3967_skl,sK3966_skl)|r1_lattices(sK3967_skl,sK3970_skl,sK3971_skl)),
% 1.95/2.61 inference(forward_demodulation,[status(thm)],[f57554,f63551])).
% 1.95/2.61 fof(f63553,plain,(
% 1.95/2.61 ~k1_lattices(sK3966_skl,sK3968_skl,sK3969_skl)=k1_lattices(sK3967_skl,sK3968_skl,sK3969_skl)|~k2_lattices(sK3966_skl,sK3968_skl,sK3969_skl)=k2_lattices(sK3967_skl,sK3968_skl,sK3969_skl)|sP322_prd(sK3969_skl,sK3968_skl,sK3969_skl,sK3968_skl,sK3967_skl,sK3966_skl)|r1_lattices(sK3967_skl,sK3968_skl,sK3971_skl)),
% 1.95/2.61 inference(forward_demodulation,[status(thm)],[f57554,f63552])).
% 1.95/2.61 fof(f63554,plain,(
% 1.95/2.61 ~k1_lattices(sK3966_skl,sK3968_skl,sK3969_skl)=k1_lattices(sK3967_skl,sK3968_skl,sK3969_skl)|~k2_lattices(sK3966_skl,sK3968_skl,sK3969_skl)=k2_lattices(sK3967_skl,sK3968_skl,sK3969_skl)|sP322_prd(sK3969_skl,sK3968_skl,sK3969_skl,sK3968_skl,sK3967_skl,sK3966_skl)|r1_lattices(sK3967_skl,sK3968_skl,sK3969_skl)),
% 1.95/2.61 inference(forward_demodulation,[status(thm)],[f57555,f63553])).
% 1.95/2.61 fof(f63555,plain,(
% 1.95/2.61 ~k1_lattices(sK3966_skl,sK3968_skl,sK3969_skl)=k1_lattices(sK3967_skl,sK3968_skl,sK3971_skl)|~k2_lattices(sK3966_skl,sK3968_skl,sK3969_skl)=k2_lattices(sK3967_skl,sK3970_skl,sK3971_skl)|sP322_prd(sK3971_skl,sK3970_skl,sK3969_skl,sK3968_skl,sK3967_skl,sK3966_skl)|~r1_lattices(sK3966_skl,sK3968_skl,sK3969_skl)),
% 1.95/2.61 inference(forward_demodulation,[status(thm)],[f57554,f57557])).
% 1.95/2.61 fof(f63556,plain,(
% 1.95/2.61 ~k1_lattices(sK3966_skl,sK3968_skl,sK3969_skl)=k1_lattices(sK3967_skl,sK3968_skl,sK3969_skl)|~k2_lattices(sK3966_skl,sK3968_skl,sK3969_skl)=k2_lattices(sK3967_skl,sK3970_skl,sK3971_skl)|sP322_prd(sK3971_skl,sK3970_skl,sK3969_skl,sK3968_skl,sK3967_skl,sK3966_skl)|~r1_lattices(sK3966_skl,sK3968_skl,sK3969_skl)),
% 1.95/2.61 inference(forward_demodulation,[status(thm)],[f57555,f63555])).
% 1.95/2.61 fof(f63557,plain,(
% 1.95/2.61 ~k1_lattices(sK3966_skl,sK3968_skl,sK3969_skl)=k1_lattices(sK3967_skl,sK3968_skl,sK3969_skl)|~k2_lattices(sK3966_skl,sK3968_skl,sK3969_skl)=k2_lattices(sK3967_skl,sK3968_skl,sK3971_skl)|sP322_prd(sK3971_skl,sK3970_skl,sK3969_skl,sK3968_skl,sK3967_skl,sK3966_skl)|~r1_lattices(sK3966_skl,sK3968_skl,sK3969_skl)),
% 1.95/2.61 inference(forward_demodulation,[status(thm)],[f57554,f63556])).
% 1.95/2.61 fof(f63558,plain,(
% 1.95/2.61 ~k1_lattices(sK3966_skl,sK3968_skl,sK3969_skl)=k1_lattices(sK3967_skl,sK3968_skl,sK3969_skl)|~k2_lattices(sK3966_skl,sK3968_skl,sK3969_skl)=k2_lattices(sK3967_skl,sK3968_skl,sK3969_skl)|sP322_prd(sK3971_skl,sK3970_skl,sK3969_skl,sK3968_skl,sK3967_skl,sK3966_skl)|~r1_lattices(sK3966_skl,sK3968_skl,sK3969_skl)),
% 1.95/2.61 inference(forward_demodulation,[status(thm)],[f57555,f63557])).
% 1.95/2.61 fof(f63559,plain,(
% 1.95/2.61 ~k1_lattices(sK3966_skl,sK3968_skl,sK3969_skl)=k1_lattices(sK3967_skl,sK3968_skl,sK3969_skl)|~k2_lattices(sK3966_skl,sK3968_skl,sK3969_skl)=k2_lattices(sK3967_skl,sK3968_skl,sK3969_skl)|sP322_prd(sK3969_skl,sK3970_skl,sK3969_skl,sK3968_skl,sK3967_skl,sK3966_skl)|~r1_lattices(sK3966_skl,sK3968_skl,sK3969_skl)),
% 1.95/2.61 inference(forward_demodulation,[status(thm)],[f57555,f63558])).
% 1.95/2.61 fof(f63560,plain,(
% 1.95/2.61 ~k1_lattices(sK3966_skl,sK3968_skl,sK3969_skl)=k1_lattices(sK3967_skl,sK3968_skl,sK3969_skl)|~k2_lattices(sK3966_skl,sK3968_skl,sK3969_skl)=k2_lattices(sK3967_skl,sK3968_skl,sK3969_skl)|sP322_prd(sK3969_skl,sK3968_skl,sK3969_skl,sK3968_skl,sK3967_skl,sK3966_skl)|~r1_lattices(sK3966_skl,sK3968_skl,sK3969_skl)),
% 1.95/2.61 inference(forward_demodulation,[status(thm)],[f57554,f63559])).
% 1.95/2.61 fof(f63562,plain,(
% 1.95/2.61 r1_lattices(sK3966_skl,sK3968_skl,sK3969_skl)|~k1_lattices(sK3966_skl,sK3968_skl,sK3969_skl)=k1_lattices(sK3967_skl,sK3968_skl,sK3969_skl)|~k2_lattices(sK3966_skl,sK3968_skl,sK3969_skl)=k2_lattices(sK3967_skl,sK3968_skl,sK3969_skl)|r1_lattices(sK3967_skl,sK3968_skl,sK3969_skl)),
% 1.95/2.61 inference(resolution,[status(thm)],[f59933,f63554])).
% 1.95/2.61 fof(f63578,plain,(
% 1.95/2.61 ![X0,X1]: (v3_struct_0(X0)|~l3_lattices(X0)|~g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))=g3_lattices(u1_struct_0(sK3966_skl),u2_lattices(sK3966_skl),u1_lattices(sK3966_skl))|~m1_subset_1(X1,u1_struct_0(X0))|~m1_subset_1(sK3969_skl,u1_struct_0(X0))|~m1_subset_1(X1,u1_struct_0(sK3967_skl))|k1_lattices(X0,X1,sK3969_skl)=k1_lattices(sK3967_skl,X1,sK3969_skl))),
% 1.95/2.61 inference(resolution,[status(thm)],[f63526,f63546])).
% 1.95/2.61 fof(f63581,plain,(
% 1.95/2.61 ![X0]: (v3_struct_0(sK3966_skl)|~l3_lattices(sK3966_skl)|~g3_lattices(u1_struct_0(sK3966_skl),u2_lattices(sK3966_skl),u1_lattices(sK3966_skl))=g3_lattices(u1_struct_0(sK3966_skl),u2_lattices(sK3966_skl),u1_lattices(sK3966_skl))|~m1_subset_1(X0,u1_struct_0(sK3966_skl))|~m1_subset_1(X0,u1_struct_0(sK3967_skl))|k1_lattices(sK3966_skl,X0,sK3969_skl)=k1_lattices(sK3967_skl,X0,sK3969_skl))),
% 1.95/2.61 inference(resolution,[status(thm)],[f63578,f57551])).
% 1.95/2.61 fof(f63582,plain,(
% 1.95/2.61 ![X0]: (v3_struct_0(sK3966_skl)|~l3_lattices(sK3966_skl)|~m1_subset_1(X0,u1_struct_0(sK3966_skl))|~m1_subset_1(X0,u1_struct_0(sK3967_skl))|k1_lattices(sK3966_skl,X0,sK3969_skl)=k1_lattices(sK3967_skl,X0,sK3969_skl))),
% 1.95/2.61 inference(trivial_equality_resolution,[status(thm)],[f63581])).
% 1.95/2.61 fof(f63583,plain,(
% 1.95/2.61 ![X0]: (~l3_lattices(sK3966_skl)|~m1_subset_1(X0,u1_struct_0(sK3966_skl))|~m1_subset_1(X0,u1_struct_0(sK3967_skl))|k1_lattices(sK3966_skl,X0,sK3969_skl)=k1_lattices(sK3967_skl,X0,sK3969_skl))),
% 1.95/2.61 inference(forward_subsumption_resolution,[status(thm)],[f63582,f57545])).
% 1.95/2.61 fof(f63584,plain,(
% 1.95/2.61 ![X0]: (~m1_subset_1(X0,u1_struct_0(sK3966_skl))|~m1_subset_1(X0,u1_struct_0(sK3967_skl))|k1_lattices(sK3966_skl,X0,sK3969_skl)=k1_lattices(sK3967_skl,X0,sK3969_skl))),
% 1.95/2.61 inference(forward_subsumption_resolution,[status(thm)],[f63583,f57546])).
% 1.95/2.61 fof(f63586,plain,(
% 1.95/2.61 ~m1_subset_1(sK3968_skl,u1_struct_0(sK3966_skl))|k1_lattices(sK3966_skl,sK3968_skl,sK3969_skl)=k1_lattices(sK3967_skl,sK3968_skl,sK3969_skl)),
% 1.95/2.61 inference(resolution,[status(thm)],[f63584,f63521])).
% 1.95/2.61 fof(f63588,plain,(
% 1.95/2.61 k1_lattices(sK3966_skl,sK3968_skl,sK3969_skl)=k1_lattices(sK3967_skl,sK3968_skl,sK3969_skl)),
% 1.95/2.61 inference(forward_subsumption_resolution,[status(thm)],[f63586,f57550])).
% 1.95/2.61 fof(f63591,plain,(
% 1.95/2.61 ![X0,X1]: (v3_struct_0(X0)|~l3_lattices(X0)|~g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))=g3_lattices(u1_struct_0(sK3966_skl),u2_lattices(sK3966_skl),u1_lattices(sK3966_skl))|~m1_subset_1(X1,u1_struct_0(X0))|~m1_subset_1(sK3969_skl,u1_struct_0(X0))|~m1_subset_1(X1,u1_struct_0(sK3967_skl))|k2_lattices(X0,X1,sK3969_skl)=k2_lattices(sK3967_skl,X1,sK3969_skl))),
% 1.95/2.61 inference(resolution,[status(thm)],[f63532,f63546])).
% 1.95/2.61 fof(f63629,plain,(
% 1.95/2.61 r1_lattices(sK3966_skl,sK3968_skl,sK3969_skl)|~k1_lattices(sK3966_skl,sK3968_skl,sK3969_skl)=k1_lattices(sK3966_skl,sK3968_skl,sK3969_skl)|~k2_lattices(sK3966_skl,sK3968_skl,sK3969_skl)=k2_lattices(sK3967_skl,sK3968_skl,sK3969_skl)|r1_lattices(sK3967_skl,sK3968_skl,sK3969_skl)),
% 1.95/2.61 inference(backward_demodulation,[status(thm)],[f63588,f63562])).
% 1.95/2.61 fof(f63630,plain,(
% 1.95/2.61 ~k1_lattices(sK3966_skl,sK3968_skl,sK3969_skl)=k1_lattices(sK3966_skl,sK3968_skl,sK3969_skl)|~k2_lattices(sK3966_skl,sK3968_skl,sK3969_skl)=k2_lattices(sK3967_skl,sK3968_skl,sK3969_skl)|sP322_prd(sK3969_skl,sK3968_skl,sK3969_skl,sK3968_skl,sK3967_skl,sK3966_skl)|~r1_lattices(sK3966_skl,sK3968_skl,sK3969_skl)),
% 1.95/2.61 inference(backward_demodulation,[status(thm)],[f63588,f63560])).
% 1.95/2.61 fof(f63632,plain,(
% 1.95/2.61 r1_lattices(sK3966_skl,sK3968_skl,sK3969_skl)|~k2_lattices(sK3966_skl,sK3968_skl,sK3969_skl)=k2_lattices(sK3967_skl,sK3968_skl,sK3969_skl)|r1_lattices(sK3967_skl,sK3968_skl,sK3969_skl)),
% 1.95/2.61 inference(trivial_equality_resolution,[status(thm)],[f63629])).
% 1.95/2.61 fof(f63633,plain,(
% 1.95/2.61 ~k2_lattices(sK3966_skl,sK3968_skl,sK3969_skl)=k2_lattices(sK3967_skl,sK3968_skl,sK3969_skl)|sP322_prd(sK3969_skl,sK3968_skl,sK3969_skl,sK3968_skl,sK3967_skl,sK3966_skl)|~r1_lattices(sK3966_skl,sK3968_skl,sK3969_skl)),
% 1.95/2.61 inference(trivial_equality_resolution,[status(thm)],[f63630])).
% 1.95/2.61 fof(f63653,plain,(
% 1.95/2.61 ![X0]: (v3_struct_0(sK3966_skl)|~l3_lattices(sK3966_skl)|~g3_lattices(u1_struct_0(sK3966_skl),u2_lattices(sK3966_skl),u1_lattices(sK3966_skl))=g3_lattices(u1_struct_0(sK3966_skl),u2_lattices(sK3966_skl),u1_lattices(sK3966_skl))|~m1_subset_1(X0,u1_struct_0(sK3966_skl))|~m1_subset_1(X0,u1_struct_0(sK3967_skl))|k2_lattices(sK3966_skl,X0,sK3969_skl)=k2_lattices(sK3967_skl,X0,sK3969_skl))),
% 1.95/2.61 inference(resolution,[status(thm)],[f63591,f57551])).
% 1.95/2.61 fof(f63654,plain,(
% 1.95/2.61 ![X0]: (v3_struct_0(sK3966_skl)|~l3_lattices(sK3966_skl)|~m1_subset_1(X0,u1_struct_0(sK3966_skl))|~m1_subset_1(X0,u1_struct_0(sK3967_skl))|k2_lattices(sK3966_skl,X0,sK3969_skl)=k2_lattices(sK3967_skl,X0,sK3969_skl))),
% 1.95/2.61 inference(trivial_equality_resolution,[status(thm)],[f63653])).
% 1.95/2.61 fof(f63655,plain,(
% 1.95/2.61 ![X0]: (~l3_lattices(sK3966_skl)|~m1_subset_1(X0,u1_struct_0(sK3966_skl))|~m1_subset_1(X0,u1_struct_0(sK3967_skl))|k2_lattices(sK3966_skl,X0,sK3969_skl)=k2_lattices(sK3967_skl,X0,sK3969_skl))),
% 1.95/2.61 inference(forward_subsumption_resolution,[status(thm)],[f63654,f57545])).
% 1.95/2.61 fof(f63656,plain,(
% 1.95/2.61 ![X0]: (~m1_subset_1(X0,u1_struct_0(sK3966_skl))|~m1_subset_1(X0,u1_struct_0(sK3967_skl))|k2_lattices(sK3966_skl,X0,sK3969_skl)=k2_lattices(sK3967_skl,X0,sK3969_skl))),
% 1.95/2.61 inference(forward_subsumption_resolution,[status(thm)],[f63655,f57546])).
% 1.95/2.61 fof(f63658,plain,(
% 1.95/2.61 ~m1_subset_1(sK3968_skl,u1_struct_0(sK3966_skl))|k2_lattices(sK3966_skl,sK3968_skl,sK3969_skl)=k2_lattices(sK3967_skl,sK3968_skl,sK3969_skl)),
% 1.95/2.61 inference(resolution,[status(thm)],[f63656,f63521])).
% 1.95/2.61 fof(f63660,plain,(
% 1.95/2.61 k2_lattices(sK3966_skl,sK3968_skl,sK3969_skl)=k2_lattices(sK3967_skl,sK3968_skl,sK3969_skl)),
% 1.95/2.61 inference(forward_subsumption_resolution,[status(thm)],[f63658,f57550])).
% 1.95/2.61 fof(f63683,plain,(
% 1.95/2.61 r1_lattices(sK3966_skl,sK3968_skl,sK3969_skl)|~k2_lattices(sK3966_skl,sK3968_skl,sK3969_skl)=k2_lattices(sK3966_skl,sK3968_skl,sK3969_skl)|r1_lattices(sK3967_skl,sK3968_skl,sK3969_skl)),
% 1.95/2.61 inference(backward_demodulation,[status(thm)],[f63660,f63632])).
% 1.95/2.61 fof(f63685,plain,(
% 1.95/2.61 ~k2_lattices(sK3966_skl,sK3968_skl,sK3969_skl)=k2_lattices(sK3966_skl,sK3968_skl,sK3969_skl)|sP322_prd(sK3969_skl,sK3968_skl,sK3969_skl,sK3968_skl,sK3967_skl,sK3966_skl)|~r1_lattices(sK3966_skl,sK3968_skl,sK3969_skl)),
% 1.95/2.61 inference(backward_demodulation,[status(thm)],[f63660,f63633])).
% 1.95/2.61 fof(f63686,plain,(
% 1.95/2.61 r1_lattices(sK3966_skl,sK3968_skl,sK3969_skl)|r1_lattices(sK3967_skl,sK3968_skl,sK3969_skl)),
% 1.95/2.61 inference(trivial_equality_resolution,[status(thm)],[f63683])).
% 1.95/2.61 fof(f63688,plain,(
% 1.95/2.61 sP322_prd(sK3969_skl,sK3968_skl,sK3969_skl,sK3968_skl,sK3967_skl,sK3966_skl)|~r1_lattices(sK3966_skl,sK3968_skl,sK3969_skl)),
% 1.95/2.61 inference(trivial_equality_resolution,[status(thm)],[f63685])).
% 1.95/2.61 fof(f63691,plain,(
% 1.95/2.61 ![X0]: (r1_lattices(sK3966_skl,sK3968_skl,sK3969_skl)|v3_struct_0(sK3967_skl)|~l3_lattices(sK3967_skl)|v3_struct_0(X0)|~l3_lattices(X0)|~g3_lattices(u1_struct_0(sK3967_skl),u2_lattices(sK3967_skl),u1_lattices(sK3967_skl))=g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))|~m1_subset_1(sK3968_skl,u1_struct_0(sK3967_skl))|~m1_subset_1(sK3969_skl,u1_struct_0(sK3967_skl))|~m1_subset_1(sK3968_skl,u1_struct_0(X0))|~m1_subset_1(sK3969_skl,u1_struct_0(X0))|r1_lattices(X0,sK3968_skl,sK3969_skl))),
% 1.95/2.61 inference(resolution,[status(thm)],[f63686,f63119])).
% 1.95/2.61 fof(f63693,plain,(
% 1.95/2.61 ![X0]: (r1_lattices(sK3966_skl,sK3968_skl,sK3969_skl)|v3_struct_0(sK3967_skl)|~l3_lattices(sK3967_skl)|v3_struct_0(X0)|~l3_lattices(X0)|~g3_lattices(u1_struct_0(sK3966_skl),u2_lattices(sK3966_skl),u1_lattices(sK3966_skl))=g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))|~m1_subset_1(sK3968_skl,u1_struct_0(sK3967_skl))|~m1_subset_1(sK3969_skl,u1_struct_0(sK3967_skl))|~m1_subset_1(sK3968_skl,u1_struct_0(X0))|~m1_subset_1(sK3969_skl,u1_struct_0(X0))|r1_lattices(X0,sK3968_skl,sK3969_skl))),
% 1.95/2.61 inference(forward_demodulation,[status(thm)],[f57549,f63691])).
% 1.95/2.61 fof(f63694,plain,(
% 1.95/2.61 ![X0]: (r1_lattices(sK3966_skl,sK3968_skl,sK3969_skl)|~l3_lattices(sK3967_skl)|v3_struct_0(X0)|~l3_lattices(X0)|~g3_lattices(u1_struct_0(sK3966_skl),u2_lattices(sK3966_skl),u1_lattices(sK3966_skl))=g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))|~m1_subset_1(sK3968_skl,u1_struct_0(sK3967_skl))|~m1_subset_1(sK3969_skl,u1_struct_0(sK3967_skl))|~m1_subset_1(sK3968_skl,u1_struct_0(X0))|~m1_subset_1(sK3969_skl,u1_struct_0(X0))|r1_lattices(X0,sK3968_skl,sK3969_skl))),
% 1.95/2.61 inference(forward_subsumption_resolution,[status(thm)],[f63693,f57547])).
% 1.95/2.61 fof(f63717,plain,(
% 1.95/2.61 ![X0]: (r1_lattices(sK3966_skl,sK3968_skl,sK3969_skl)|v3_struct_0(X0)|~l3_lattices(X0)|~g3_lattices(u1_struct_0(sK3966_skl),u2_lattices(sK3966_skl),u1_lattices(sK3966_skl))=g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))|~m1_subset_1(sK3968_skl,u1_struct_0(sK3967_skl))|~m1_subset_1(sK3969_skl,u1_struct_0(sK3967_skl))|~m1_subset_1(sK3968_skl,u1_struct_0(X0))|~m1_subset_1(sK3969_skl,u1_struct_0(X0))|r1_lattices(X0,sK3968_skl,sK3969_skl))),
% 1.95/2.61 inference(forward_subsumption_resolution,[status(thm)],[f63694,f57548])).
% 1.95/2.61 fof(f63718,plain,(
% 1.95/2.61 ![X0]: (r1_lattices(sK3966_skl,sK3968_skl,sK3969_skl)|v3_struct_0(X0)|~l3_lattices(X0)|~g3_lattices(u1_struct_0(sK3966_skl),u2_lattices(sK3966_skl),u1_lattices(sK3966_skl))=g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))|~m1_subset_1(sK3968_skl,u1_struct_0(sK3967_skl))|~m1_subset_1(sK3968_skl,u1_struct_0(X0))|~m1_subset_1(sK3969_skl,u1_struct_0(X0))|r1_lattices(X0,sK3968_skl,sK3969_skl))),
% 1.95/2.61 inference(resolution,[status(thm)],[f63717,f63546])).
% 1.95/2.61 fof(f63719,plain,(
% 1.95/2.61 ![X0]: (r1_lattices(sK3966_skl,sK3968_skl,sK3969_skl)|v3_struct_0(X0)|~l3_lattices(X0)|~g3_lattices(u1_struct_0(sK3966_skl),u2_lattices(sK3966_skl),u1_lattices(sK3966_skl))=g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))|~m1_subset_1(sK3968_skl,u1_struct_0(X0))|~m1_subset_1(sK3969_skl,u1_struct_0(X0))|r1_lattices(X0,sK3968_skl,sK3969_skl))),
% 1.95/2.61 inference(forward_subsumption_resolution,[status(thm)],[f63718,f63521])).
% 1.95/2.61 fof(f63721,plain,(
% 1.95/2.61 r1_lattices(sK3966_skl,sK3968_skl,sK3969_skl)|v3_struct_0(sK3966_skl)|~l3_lattices(sK3966_skl)|~g3_lattices(u1_struct_0(sK3966_skl),u2_lattices(sK3966_skl),u1_lattices(sK3966_skl))=g3_lattices(u1_struct_0(sK3966_skl),u2_lattices(sK3966_skl),u1_lattices(sK3966_skl))|~m1_subset_1(sK3968_skl,u1_struct_0(sK3966_skl))|r1_lattices(sK3966_skl,sK3968_skl,sK3969_skl)),
% 1.95/2.61 inference(resolution,[status(thm)],[f63719,f57551])).
% 1.95/2.61 fof(f63724,plain,(
% 1.95/2.61 r1_lattices(sK3966_skl,sK3968_skl,sK3969_skl)|v3_struct_0(sK3966_skl)|~l3_lattices(sK3966_skl)|~g3_lattices(u1_struct_0(sK3966_skl),u2_lattices(sK3966_skl),u1_lattices(sK3966_skl))=g3_lattices(u1_struct_0(sK3966_skl),u2_lattices(sK3966_skl),u1_lattices(sK3966_skl))|~m1_subset_1(sK3968_skl,u1_struct_0(sK3966_skl))),
% 1.95/2.61 inference(duplicate_literals_removal,[status(thm)],[f63721])).
% 1.95/2.61 fof(f63725,plain,(
% 1.95/2.61 r1_lattices(sK3966_skl,sK3968_skl,sK3969_skl)|v3_struct_0(sK3966_skl)|~l3_lattices(sK3966_skl)|~m1_subset_1(sK3968_skl,u1_struct_0(sK3966_skl))),
% 1.95/2.61 inference(trivial_equality_resolution,[status(thm)],[f63724])).
% 1.95/2.61 fof(f63726,plain,(
% 1.95/2.61 r1_lattices(sK3966_skl,sK3968_skl,sK3969_skl)|~l3_lattices(sK3966_skl)|~m1_subset_1(sK3968_skl,u1_struct_0(sK3966_skl))),
% 1.95/2.61 inference(forward_subsumption_resolution,[status(thm)],[f63725,f57545])).
% 1.95/2.61 fof(f63727,plain,(
% 1.95/2.61 r1_lattices(sK3966_skl,sK3968_skl,sK3969_skl)|~m1_subset_1(sK3968_skl,u1_struct_0(sK3966_skl))),
% 1.95/2.61 inference(forward_subsumption_resolution,[status(thm)],[f63726,f57546])).
% 1.95/2.61 fof(f63728,plain,(
% 1.95/2.61 r1_lattices(sK3966_skl,sK3968_skl,sK3969_skl)),
% 1.95/2.61 inference(resolution,[status(thm)],[f63727,f57550])).
% 1.95/2.61 fof(f63729,plain,(
% 1.95/2.61 sP322_prd(sK3969_skl,sK3968_skl,sK3969_skl,sK3968_skl,sK3967_skl,sK3966_skl)),
% 1.95/2.61 inference(backward_subsumption_resolution,[status(thm)],[f63688,f63728])).
% 1.95/2.61 fof(f63731,plain,(
% 1.95/2.61 ![X0]: (v3_struct_0(sK3966_skl)|~l3_lattices(sK3966_skl)|v3_struct_0(X0)|~l3_lattices(X0)|~g3_lattices(u1_struct_0(sK3966_skl),u2_lattices(sK3966_skl),u1_lattices(sK3966_skl))=g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))|~m1_subset_1(sK3968_skl,u1_struct_0(sK3966_skl))|~m1_subset_1(sK3969_skl,u1_struct_0(sK3966_skl))|~m1_subset_1(sK3968_skl,u1_struct_0(X0))|~m1_subset_1(sK3969_skl,u1_struct_0(X0))|r1_lattices(X0,sK3968_skl,sK3969_skl))),
% 1.95/2.61 inference(resolution,[status(thm)],[f63728,f63119])).
% 1.95/2.61 fof(f63733,plain,(
% 1.97/2.78 ![X0]: (~l3_lattices(sK3966_skl)|v3_struct_0(X0)|~l3_lattices(X0)|~g3_lattices(u1_struct_0(sK3966_skl),u2_lattices(sK3966_skl),u1_lattices(sK3966_skl))=g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))|~m1_subset_1(sK3968_skl,u1_struct_0(sK3966_skl))|~m1_subset_1(sK3969_skl,u1_struct_0(sK3966_skl))|~m1_subset_1(sK3968_skl,u1_struct_0(X0))|~m1_subset_1(sK3969_skl,u1_struct_0(X0))|r1_lattices(X0,sK3968_skl,sK3969_skl))),
% 1.97/2.78 inference(forward_subsumption_resolution,[status(thm)],[f63731,f57545])).
% 1.97/2.78 fof(f63736,plain,(
% 1.97/2.78 ![X0]: (v3_struct_0(X0)|~l3_lattices(X0)|~g3_lattices(u1_struct_0(sK3966_skl),u2_lattices(sK3966_skl),u1_lattices(sK3966_skl))=g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))|~m1_subset_1(sK3968_skl,u1_struct_0(sK3966_skl))|~m1_subset_1(sK3969_skl,u1_struct_0(sK3966_skl))|~m1_subset_1(sK3968_skl,u1_struct_0(X0))|~m1_subset_1(sK3969_skl,u1_struct_0(X0))|r1_lattices(X0,sK3968_skl,sK3969_skl))),
% 1.97/2.78 inference(forward_subsumption_resolution,[status(thm)],[f63733,f57546])).
% 1.97/2.78 fof(f63737,plain,(
% 1.97/2.78 ![X0]: (v3_struct_0(X0)|~l3_lattices(X0)|~g3_lattices(u1_struct_0(sK3966_skl),u2_lattices(sK3966_skl),u1_lattices(sK3966_skl))=g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))|~m1_subset_1(sK3968_skl,u1_struct_0(sK3966_skl))|~m1_subset_1(sK3968_skl,u1_struct_0(X0))|~m1_subset_1(sK3969_skl,u1_struct_0(X0))|r1_lattices(X0,sK3968_skl,sK3969_skl))),
% 1.97/2.78 inference(resolution,[status(thm)],[f63736,f57551])).
% 1.97/2.78 fof(f63738,plain,(
% 1.97/2.78 ![X0]: (v3_struct_0(X0)|~l3_lattices(X0)|~g3_lattices(u1_struct_0(sK3966_skl),u2_lattices(sK3966_skl),u1_lattices(sK3966_skl))=g3_lattices(u1_struct_0(X0),u2_lattices(X0),u1_lattices(X0))|~m1_subset_1(sK3968_skl,u1_struct_0(X0))|~m1_subset_1(sK3969_skl,u1_struct_0(X0))|r1_lattices(X0,sK3968_skl,sK3969_skl))),
% 1.97/2.78 inference(forward_subsumption_resolution,[status(thm)],[f63737,f57550])).
% 1.97/2.78 fof(f63784,plain,(
% 1.97/2.78 v3_struct_0(sK3967_skl)|~l3_lattices(sK3967_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))|~m1_subset_1(sK3968_skl,u1_struct_0(sK3967_skl))|r1_lattices(sK3967_skl,sK3968_skl,sK3969_skl)),
% 1.97/2.78 inference(resolution,[status(thm)],[f63738,f63546])).
% 1.97/2.78 fof(f63786,plain,(
% 1.97/2.78 v3_struct_0(sK3967_skl)|~l3_lattices(sK3967_skl)|~g3_lattices(u1_struct_0(sK3966_skl),u2_lattices(sK3966_skl),u1_lattices(sK3966_skl))=g3_lattices(u1_struct_0(sK3966_skl),u2_lattices(sK3966_skl),u1_lattices(sK3966_skl))|~m1_subset_1(sK3968_skl,u1_struct_0(sK3967_skl))|r1_lattices(sK3967_skl,sK3968_skl,sK3969_skl)),
% 1.97/2.78 inference(forward_demodulation,[status(thm)],[f57549,f63784])).
% 1.97/2.78 fof(f63787,plain,(
% 1.97/2.78 v3_struct_0(sK3967_skl)|~l3_lattices(sK3967_skl)|~m1_subset_1(sK3968_skl,u1_struct_0(sK3967_skl))|r1_lattices(sK3967_skl,sK3968_skl,sK3969_skl)),
% 1.97/2.78 inference(trivial_equality_resolution,[status(thm)],[f63786])).
% 1.97/2.78 fof(f63788,plain,(
% 1.97/2.78 ~l3_lattices(sK3967_skl)|~m1_subset_1(sK3968_skl,u1_struct_0(sK3967_skl))|r1_lattices(sK3967_skl,sK3968_skl,sK3969_skl)),
% 1.97/2.78 inference(forward_subsumption_resolution,[status(thm)],[f63787,f57547])).
% 1.97/2.78 fof(f63790,plain,(
% 1.97/2.78 ~m1_subset_1(sK3968_skl,u1_struct_0(sK3967_skl))|r1_lattices(sK3967_skl,sK3968_skl,sK3969_skl)),
% 1.97/2.78 inference(forward_subsumption_resolution,[status(thm)],[f63788,f57548])).
% 1.97/2.78 fof(f63791,plain,(
% 1.97/2.78 r1_lattices(sK3967_skl,sK3968_skl,sK3969_skl)),
% 1.97/2.78 inference(resolution,[status(thm)],[f63790,f63521])).
% 1.97/2.78 fof(f63794,plain,(
% 1.97/2.78 ![X0,X1,X2]: (~sP322_prd(sK3969_skl,sK3968_skl,X0,X1,sK3967_skl,X2))),
% 1.97/2.78 inference(resolution,[status(thm)],[f63791,f59934])).
% 1.97/2.78 fof(f63797,plain,(
% 1.97/2.78 $false),
% 1.97/2.78 inference(backward_subsumption_resolution,[status(thm)],[f63729,f63794])).
% 1.97/2.78 % SZS output end CNFRefutation for theBenchmark.p
% 1.99/2.90 % Elapsed time: 2.493991 seconds
% 1.99/2.90 % CPU time: 6.292577 seconds
% 1.99/2.90 % Total memory used: 3.798 GB
% 1.99/2.90 % Net memory used: 3.781 GB
%------------------------------------------------------------------------------