%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LAT295+4 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n018.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 33.07s 13.88s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : LAT295+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.47 % Computer : n018.cluster.edu
% 0.19/0.47 % Model : x86_64 x86_64
% 0.19/0.47 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.47 % Memory : 8046.5625MB
% 0.19/0.47 % OS : Linux 6.8.0-71-generic
% 0.19/0.48 % CPULimit : 300
% 0.19/0.48 % WCLimit : 300
% 0.19/0.48 % DateTime : Sun Sep 20 23:31:22 UTC 2026
% 0.19/0.48 % CPUTime :
% 10.21/10.55 % Drodi V4.1.1
% 33.07/13.88 % Refutation found
% 33.07/13.88 % SZS status Theorem for theBenchmark: Theorem is valid
% 33.07/13.88 % SZS output start CNFRefutation for theBenchmark
% 33.07/13.88 fof(f33839,axiom,(
% 33.07/13.88 (! [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) ) ) ) ) )) )) )) )) ) )) )),
% 33.07/13.88 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 33.07/13.88 fof(f34658,conjecture,(
% 33.07/13.88 (! [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) ) ) ) ) )) )) )) )) ) )) )),
% 33.07/13.88 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 33.07/13.88 fof(f34659,negated_conjecture,(
% 33.07/13.88 ~((! [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) ) ) ) ) )) )) )) )) ) )) ))),
% 33.07/13.88 inference(negated_conjecture,[status(cth)],[f34658])).
% 33.07/13.88 fof(f150608,plain,(
% 33.07/13.88 ![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))))))))))))))))),
% 33.07/13.88 inference(pre_NNF_transformation,[status(thm)],[f33839])).
% 33.07/13.88 fof(f150609,plain,(
% 33.07/13.88 ![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))),
% 33.07/13.88 inference(cnf_transformation,[status(thm)],[f150608])).
% 33.07/13.88 fof(f150610,plain,(
% 33.07/13.88 ![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))),
% 33.07/13.88 inference(cnf_transformation,[status(thm)],[f150608])).
% 33.07/13.88 fof(f150611,plain,(
% 33.07/13.88 ![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))),
% 33.07/13.89 inference(cnf_transformation,[status(thm)],[f150608])).
% 33.07/13.89 fof(f153989,plain,(
% 33.07/13.89 (?[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)))))))))))))))))),
% 33.07/13.89 inference(pre_NNF_transformation,[status(thm)],[f34659])).
% 33.07/13.89 fof(f153990,definition,(
% 33.07/13.89 ![A,B,C,D,E,F]: (sP1325_prd(F,E,D,C,B,A)<=>(r1_lattices(A,C,D)&~r1_lattices(B,E,F)))),
% 33.07/13.89 introduced(definition,[new_symbols(definition,[sP1325_prd])],[])).
% 33.07/13.89 fof(f153991,plain,(
% 33.07/13.89 ?[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))|sP1325_prd(F,E,D,C,B,A))|(r1_lattices(B,E,F)&~r1_lattices(A,C,D))))))))))))))))),
% 33.07/13.89 inference(formula_renaming,[status(thm)],[f153989,f153990])).
% 33.07/13.89 fof(f153992,plain,(
% 33.07/13.89 ((~v3_struct_0(sK12109_skl)&l3_lattices(sK12109_skl))&((~v3_struct_0(sK12110_skl)&l3_lattices(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))&(m1_subset_1(sK12111_skl,u1_struct_0(sK12109_skl))&(m1_subset_1(sK12112_skl,u1_struct_0(sK12109_skl))&(m1_subset_1(sK12113_skl,u1_struct_0(sK12110_skl))&(m1_subset_1(sK12114_skl,u1_struct_0(sK12110_skl))&((sK12111_skl=sK12113_skl&sK12112_skl=sK12114_skl)&(((~k1_lattices(sK12109_skl,sK12111_skl,sK12112_skl)=k1_lattices(sK12110_skl,sK12113_skl,sK12114_skl)|~k2_lattices(sK12109_skl,sK12111_skl,sK12112_skl)=k2_lattices(sK12110_skl,sK12113_skl,sK12114_skl))|sP1325_prd(sK12114_skl,sK12113_skl,sK12112_skl,sK12111_skl,sK12110_skl,sK12109_skl))|(r1_lattices(sK12110_skl,sK12113_skl,sK12114_skl)&~r1_lattices(sK12109_skl,sK12111_skl,sK12112_skl)))))))))))),
% 33.07/13.89 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])).
% 33.07/13.89 fof(f153993,plain,(
% 33.07/13.89 ~v3_struct_0(sK12109_skl)),
% 33.07/13.89 inference(cnf_transformation,[status(thm)],[f153992])).
% 33.07/13.89 fof(f153994,plain,(
% 33.07/13.89 l3_lattices(sK12109_skl)),
% 33.07/13.89 inference(cnf_transformation,[status(thm)],[f153992])).
% 33.07/13.89 fof(f153995,plain,(
% 33.07/13.89 ~v3_struct_0(sK12110_skl)),
% 33.07/13.89 inference(cnf_transformation,[status(thm)],[f153992])).
% 33.07/13.89 fof(f153996,plain,(
% 33.07/13.89 l3_lattices(sK12110_skl)),
% 33.07/13.89 inference(cnf_transformation,[status(thm)],[f153992])).
% 33.07/13.89 fof(f153997,plain,(
% 33.07/13.89 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))),
% 33.07/13.89 inference(cnf_transformation,[status(thm)],[f153992])).
% 33.07/13.89 fof(f153998,plain,(
% 33.07/13.89 m1_subset_1(sK12111_skl,u1_struct_0(sK12109_skl))),
% 33.07/13.89 inference(cnf_transformation,[status(thm)],[f153992])).
% 33.07/13.89 fof(f153999,plain,(
% 33.07/13.89 m1_subset_1(sK12112_skl,u1_struct_0(sK12109_skl))),
% 33.07/13.89 inference(cnf_transformation,[status(thm)],[f153992])).
% 33.07/13.89 fof(f154000,plain,(
% 33.07/13.89 m1_subset_1(sK12113_skl,u1_struct_0(sK12110_skl))),
% 33.07/13.89 inference(cnf_transformation,[status(thm)],[f153992])).
% 33.07/13.89 fof(f154001,plain,(
% 33.07/13.89 m1_subset_1(sK12114_skl,u1_struct_0(sK12110_skl))),
% 33.07/13.89 inference(cnf_transformation,[status(thm)],[f153992])).
% 33.07/13.89 fof(f154002,plain,(
% 33.07/13.89 sK12111_skl=sK12113_skl),
% 33.07/13.89 inference(cnf_transformation,[status(thm)],[f153992])).
% 33.07/13.89 fof(f154003,plain,(
% 33.07/13.89 sK12112_skl=sK12114_skl),
% 33.07/13.89 inference(cnf_transformation,[status(thm)],[f153992])).
% 33.07/13.89 fof(f154004,plain,(
% 33.07/13.89 ~k1_lattices(sK12109_skl,sK12111_skl,sK12112_skl)=k1_lattices(sK12110_skl,sK12113_skl,sK12114_skl)|~k2_lattices(sK12109_skl,sK12111_skl,sK12112_skl)=k2_lattices(sK12110_skl,sK12113_skl,sK12114_skl)|sP1325_prd(sK12114_skl,sK12113_skl,sK12112_skl,sK12111_skl,sK12110_skl,sK12109_skl)|r1_lattices(sK12110_skl,sK12113_skl,sK12114_skl)),
% 33.07/13.89 inference(cnf_transformation,[status(thm)],[f153992])).
% 33.07/13.89 fof(f154005,plain,(
% 33.07/13.89 ~k1_lattices(sK12109_skl,sK12111_skl,sK12112_skl)=k1_lattices(sK12110_skl,sK12113_skl,sK12114_skl)|~k2_lattices(sK12109_skl,sK12111_skl,sK12112_skl)=k2_lattices(sK12110_skl,sK12113_skl,sK12114_skl)|sP1325_prd(sK12114_skl,sK12113_skl,sK12112_skl,sK12111_skl,sK12110_skl,sK12109_skl)|~r1_lattices(sK12109_skl,sK12111_skl,sK12112_skl)),
% 33.07/13.89 inference(cnf_transformation,[status(thm)],[f153992])).
% 33.07/13.89 fof(f164089,plain,(
% 33.07/13.89 ![A,B,C,D,E,F]: ((~sP1325_prd(F,E,D,C,B,A)|(r1_lattices(A,C,D)&~r1_lattices(B,E,F)))&(sP1325_prd(F,E,D,C,B,A)|(~r1_lattices(A,C,D)|r1_lattices(B,E,F))))),
% 33.07/13.89 inference(NNF_transformation,[status(thm)],[f153990])).
% 33.07/13.89 fof(f164090,plain,(
% 33.07/13.89 (![A,B,C,D,E,F]: (~sP1325_prd(F,E,D,C,B,A)|(r1_lattices(A,C,D)&~r1_lattices(B,E,F))))&(![A,B,C,D,E,F]: (sP1325_prd(F,E,D,C,B,A)|(~r1_lattices(A,C,D)|r1_lattices(B,E,F))))),
% 33.07/13.89 inference(miniscoping,[status(thm)],[f164089])).
% 33.07/13.89 fof(f164091,plain,(
% 33.07/13.89 ![X0,X1,X2,X3,X4,X5]: (~sP1325_prd(X0,X1,X2,X3,X4,X5)|r1_lattices(X5,X3,X2))),
% 33.07/13.89 inference(cnf_transformation,[status(thm)],[f164090])).
% 33.07/13.89 fof(f164092,plain,(
% 33.07/13.89 ![X0,X1,X2,X3,X4,X5]: (~sP1325_prd(X0,X1,X2,X3,X4,X5)|~r1_lattices(X4,X1,X0))),
% 33.07/13.89 inference(cnf_transformation,[status(thm)],[f164090])).
% 33.07/13.89 fof(f179767,plain,(
% 33.07/13.89 ![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))),
% 33.07/13.89 inference(destructive_equality_resolution,[status(thm)],[f150609])).
% 33.07/13.89 fof(f179768,plain,(
% 33.07/13.89 ![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))),
% 33.07/13.89 inference(destructive_equality_resolution,[status(thm)],[f150610])).
% 33.07/13.89 fof(f179769,plain,(
% 33.07/13.89 ![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))),
% 33.07/13.89 inference(destructive_equality_resolution,[status(thm)],[f150611])).
% 33.07/13.89 fof(f180886,plain,(
% 33.07/13.89 m1_subset_1(sK12111_skl,u1_struct_0(sK12110_skl))),
% 33.07/13.89 inference(forward_demodulation,[status(thm)],[f154002,f154000])).
% 33.07/13.89 fof(f180887,plain,(
% 33.07/13.89 m1_subset_1(sK12112_skl,u1_struct_0(sK12110_skl))),
% 33.07/13.89 inference(forward_demodulation,[status(thm)],[f154003,f154001])).
% 33.07/13.89 fof(f180892,plain,(
% 33.07/13.89 ~k1_lattices(sK12109_skl,sK12111_skl,sK12112_skl)=k1_lattices(sK12110_skl,sK12111_skl,sK12114_skl)|~k2_lattices(sK12109_skl,sK12111_skl,sK12112_skl)=k2_lattices(sK12110_skl,sK12113_skl,sK12114_skl)|sP1325_prd(sK12114_skl,sK12113_skl,sK12112_skl,sK12111_skl,sK12110_skl,sK12109_skl)|r1_lattices(sK12110_skl,sK12113_skl,sK12114_skl)),
% 33.07/13.89 inference(forward_demodulation,[status(thm)],[f154002,f154004])).
% 33.07/13.89 fof(f180893,plain,(
% 33.07/13.89 ~k1_lattices(sK12109_skl,sK12111_skl,sK12112_skl)=k1_lattices(sK12110_skl,sK12111_skl,sK12112_skl)|~k2_lattices(sK12109_skl,sK12111_skl,sK12112_skl)=k2_lattices(sK12110_skl,sK12113_skl,sK12114_skl)|sP1325_prd(sK12114_skl,sK12113_skl,sK12112_skl,sK12111_skl,sK12110_skl,sK12109_skl)|r1_lattices(sK12110_skl,sK12113_skl,sK12114_skl)),
% 33.07/13.89 inference(forward_demodulation,[status(thm)],[f154003,f180892])).
% 33.07/13.89 fof(f180894,plain,(
% 33.07/13.89 ~k1_lattices(sK12109_skl,sK12111_skl,sK12112_skl)=k1_lattices(sK12110_skl,sK12111_skl,sK12112_skl)|~k2_lattices(sK12109_skl,sK12111_skl,sK12112_skl)=k2_lattices(sK12110_skl,sK12111_skl,sK12114_skl)|sP1325_prd(sK12114_skl,sK12113_skl,sK12112_skl,sK12111_skl,sK12110_skl,sK12109_skl)|r1_lattices(sK12110_skl,sK12113_skl,sK12114_skl)),
% 33.07/13.89 inference(forward_demodulation,[status(thm)],[f154002,f180893])).
% 33.07/13.89 fof(f180895,plain,(
% 33.07/13.89 ~k1_lattices(sK12109_skl,sK12111_skl,sK12112_skl)=k1_lattices(sK12110_skl,sK12111_skl,sK12112_skl)|~k2_lattices(sK12109_skl,sK12111_skl,sK12112_skl)=k2_lattices(sK12110_skl,sK12111_skl,sK12112_skl)|sP1325_prd(sK12114_skl,sK12113_skl,sK12112_skl,sK12111_skl,sK12110_skl,sK12109_skl)|r1_lattices(sK12110_skl,sK12113_skl,sK12114_skl)),
% 33.07/13.89 inference(forward_demodulation,[status(thm)],[f154003,f180894])).
% 33.07/13.89 fof(f180896,plain,(
% 33.07/13.89 ~k1_lattices(sK12109_skl,sK12111_skl,sK12112_skl)=k1_lattices(sK12110_skl,sK12111_skl,sK12112_skl)|~k2_lattices(sK12109_skl,sK12111_skl,sK12112_skl)=k2_lattices(sK12110_skl,sK12111_skl,sK12112_skl)|sP1325_prd(sK12112_skl,sK12113_skl,sK12112_skl,sK12111_skl,sK12110_skl,sK12109_skl)|r1_lattices(sK12110_skl,sK12113_skl,sK12114_skl)),
% 33.07/13.89 inference(forward_demodulation,[status(thm)],[f154003,f180895])).
% 33.07/13.89 fof(f180897,plain,(
% 33.07/13.89 ~k1_lattices(sK12109_skl,sK12111_skl,sK12112_skl)=k1_lattices(sK12110_skl,sK12111_skl,sK12112_skl)|~k2_lattices(sK12109_skl,sK12111_skl,sK12112_skl)=k2_lattices(sK12110_skl,sK12111_skl,sK12112_skl)|sP1325_prd(sK12112_skl,sK12111_skl,sK12112_skl,sK12111_skl,sK12110_skl,sK12109_skl)|r1_lattices(sK12110_skl,sK12113_skl,sK12114_skl)),
% 33.07/13.89 inference(forward_demodulation,[status(thm)],[f154002,f180896])).
% 33.07/13.89 fof(f180898,plain,(
% 33.07/13.89 ~k1_lattices(sK12109_skl,sK12111_skl,sK12112_skl)=k1_lattices(sK12110_skl,sK12111_skl,sK12112_skl)|~k2_lattices(sK12109_skl,sK12111_skl,sK12112_skl)=k2_lattices(sK12110_skl,sK12111_skl,sK12112_skl)|sP1325_prd(sK12112_skl,sK12111_skl,sK12112_skl,sK12111_skl,sK12110_skl,sK12109_skl)|r1_lattices(sK12110_skl,sK12111_skl,sK12114_skl)),
% 33.07/13.89 inference(forward_demodulation,[status(thm)],[f154002,f180897])).
% 33.07/13.89 fof(f180899,plain,(
% 33.07/13.89 ~k1_lattices(sK12109_skl,sK12111_skl,sK12112_skl)=k1_lattices(sK12110_skl,sK12111_skl,sK12112_skl)|~k2_lattices(sK12109_skl,sK12111_skl,sK12112_skl)=k2_lattices(sK12110_skl,sK12111_skl,sK12112_skl)|sP1325_prd(sK12112_skl,sK12111_skl,sK12112_skl,sK12111_skl,sK12110_skl,sK12109_skl)|r1_lattices(sK12110_skl,sK12111_skl,sK12112_skl)),
% 33.07/13.89 inference(forward_demodulation,[status(thm)],[f154003,f180898])).
% 33.07/13.89 fof(f180933,plain,(
% 33.07/13.89 ![X0,X1]: (v3_struct_0(sK12109_skl)|~l3_lattices(sK12109_skl)|v3_struct_0(sK12110_skl)|~l3_lattices(sK12110_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(sK12110_skl))|~m1_subset_1(X1,u1_struct_0(sK12110_skl))|k1_lattices(sK12109_skl,X0,X1)=k1_lattices(sK12110_skl,X0,X1))),
% 33.07/13.89 inference(resolution,[status(thm)],[f179767,f153997])).
% 33.07/13.89 fof(f180938,plain,(
% 33.07/13.89 ![X0,X1]: (~l3_lattices(sK12109_skl)|v3_struct_0(sK12110_skl)|~l3_lattices(sK12110_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(sK12110_skl))|~m1_subset_1(X1,u1_struct_0(sK12110_skl))|k1_lattices(sK12109_skl,X0,X1)=k1_lattices(sK12110_skl,X0,X1))),
% 33.07/13.89 inference(forward_subsumption_resolution,[status(thm)],[f180933,f153993])).
% 33.07/13.89 fof(f180942,plain,(
% 33.07/13.89 ![X0,X1]: (v3_struct_0(sK12110_skl)|~l3_lattices(sK12110_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(sK12110_skl))|~m1_subset_1(X1,u1_struct_0(sK12110_skl))|k1_lattices(sK12109_skl,X0,X1)=k1_lattices(sK12110_skl,X0,X1))),
% 33.07/13.89 inference(forward_subsumption_resolution,[status(thm)],[f180938,f153994])).
% 33.07/13.89 fof(f180943,plain,(
% 33.07/13.89 ![X0]: (v3_struct_0(sK12110_skl)|~l3_lattices(sK12110_skl)|~m1_subset_1(X0,u1_struct_0(sK12109_skl))|~m1_subset_1(sK12112_skl,u1_struct_0(sK12109_skl))|~m1_subset_1(X0,u1_struct_0(sK12110_skl))|k1_lattices(sK12109_skl,X0,sK12112_skl)=k1_lattices(sK12110_skl,X0,sK12112_skl))),
% 33.07/13.89 inference(resolution,[status(thm)],[f180942,f180887])).
% 33.07/13.89 fof(f180945,plain,(
% 33.07/13.89 ![X0]: (~l3_lattices(sK12110_skl)|~m1_subset_1(X0,u1_struct_0(sK12109_skl))|~m1_subset_1(sK12112_skl,u1_struct_0(sK12109_skl))|~m1_subset_1(X0,u1_struct_0(sK12110_skl))|k1_lattices(sK12109_skl,X0,sK12112_skl)=k1_lattices(sK12110_skl,X0,sK12112_skl))),
% 33.07/13.89 inference(forward_subsumption_resolution,[status(thm)],[f180943,f153995])).
% 33.07/13.89 fof(f180956,plain,(
% 33.07/13.89 ![X0,X1]: (v3_struct_0(sK12109_skl)|~l3_lattices(sK12109_skl)|v3_struct_0(sK12110_skl)|~l3_lattices(sK12110_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(sK12110_skl))|~m1_subset_1(X1,u1_struct_0(sK12110_skl))|k2_lattices(sK12109_skl,X0,X1)=k2_lattices(sK12110_skl,X0,X1))),
% 33.07/13.89 inference(resolution,[status(thm)],[f179768,f153997])).
% 33.07/13.89 fof(f180961,plain,(
% 33.07/13.89 ![X0,X1]: (~l3_lattices(sK12109_skl)|v3_struct_0(sK12110_skl)|~l3_lattices(sK12110_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(sK12110_skl))|~m1_subset_1(X1,u1_struct_0(sK12110_skl))|k2_lattices(sK12109_skl,X0,X1)=k2_lattices(sK12110_skl,X0,X1))),
% 33.07/13.89 inference(forward_subsumption_resolution,[status(thm)],[f180956,f153993])).
% 33.07/13.89 fof(f180965,plain,(
% 33.07/13.89 ![X0,X1]: (v3_struct_0(sK12110_skl)|~l3_lattices(sK12110_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(sK12110_skl))|~m1_subset_1(X1,u1_struct_0(sK12110_skl))|k2_lattices(sK12109_skl,X0,X1)=k2_lattices(sK12110_skl,X0,X1))),
% 33.07/13.89 inference(forward_subsumption_resolution,[status(thm)],[f180961,f153994])).
% 33.07/13.89 fof(f180966,plain,(
% 33.07/13.89 ![X0]: (v3_struct_0(sK12110_skl)|~l3_lattices(sK12110_skl)|~m1_subset_1(X0,u1_struct_0(sK12109_skl))|~m1_subset_1(sK12112_skl,u1_struct_0(sK12109_skl))|~m1_subset_1(X0,u1_struct_0(sK12110_skl))|k2_lattices(sK12109_skl,X0,sK12112_skl)=k2_lattices(sK12110_skl,X0,sK12112_skl))),
% 33.07/13.89 inference(resolution,[status(thm)],[f180965,f180887])).
% 33.07/13.89 fof(f180968,plain,(
% 33.07/13.89 ![X0]: (~l3_lattices(sK12110_skl)|~m1_subset_1(X0,u1_struct_0(sK12109_skl))|~m1_subset_1(sK12112_skl,u1_struct_0(sK12109_skl))|~m1_subset_1(X0,u1_struct_0(sK12110_skl))|k2_lattices(sK12109_skl,X0,sK12112_skl)=k2_lattices(sK12110_skl,X0,sK12112_skl))),
% 33.07/13.89 inference(forward_subsumption_resolution,[status(thm)],[f180966,f153995])).
% 33.07/13.89 fof(f180979,plain,(
% 33.07/13.89 ![X0,X1]: (v3_struct_0(sK12109_skl)|~l3_lattices(sK12109_skl)|v3_struct_0(sK12110_skl)|~l3_lattices(sK12110_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(sK12110_skl))|~m1_subset_1(X1,u1_struct_0(sK12110_skl))|~r1_lattices(sK12109_skl,X0,X1)|r1_lattices(sK12110_skl,X0,X1))),
% 33.07/13.89 inference(resolution,[status(thm)],[f179769,f153997])).
% 33.07/13.89 fof(f180980,plain,(
% 33.07/13.89 ![X0,X1]: (v3_struct_0(sK12110_skl)|~l3_lattices(sK12110_skl)|v3_struct_0(sK12109_skl)|~l3_lattices(sK12109_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(sK12109_skl))|~m1_subset_1(X1,u1_struct_0(sK12109_skl))|~r1_lattices(sK12110_skl,X0,X1)|r1_lattices(sK12109_skl,X0,X1))),
% 33.07/13.89 inference(resolution,[status(thm)],[f179769,f153997])).
% 33.07/13.89 fof(f180984,plain,(
% 33.07/13.89 ![X0,X1]: (~l3_lattices(sK12109_skl)|v3_struct_0(sK12110_skl)|~l3_lattices(sK12110_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(sK12110_skl))|~m1_subset_1(X1,u1_struct_0(sK12110_skl))|~r1_lattices(sK12109_skl,X0,X1)|r1_lattices(sK12110_skl,X0,X1))),
% 33.07/13.89 inference(forward_subsumption_resolution,[status(thm)],[f180979,f153993])).
% 33.07/13.89 fof(f180985,plain,(
% 33.07/13.89 ![X0,X1]: (~l3_lattices(sK12110_skl)|v3_struct_0(sK12109_skl)|~l3_lattices(sK12109_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(sK12109_skl))|~m1_subset_1(X1,u1_struct_0(sK12109_skl))|~r1_lattices(sK12110_skl,X0,X1)|r1_lattices(sK12109_skl,X0,X1))),
% 33.07/13.89 inference(forward_subsumption_resolution,[status(thm)],[f180980,f153995])).
% 33.07/13.89 fof(f180988,plain,(
% 33.07/13.89 ![X0,X1]: (v3_struct_0(sK12110_skl)|~l3_lattices(sK12110_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(sK12110_skl))|~m1_subset_1(X1,u1_struct_0(sK12110_skl))|~r1_lattices(sK12109_skl,X0,X1)|r1_lattices(sK12110_skl,X0,X1))),
% 33.07/13.89 inference(forward_subsumption_resolution,[status(thm)],[f180984,f153994])).
% 33.07/13.89 fof(f180989,plain,(
% 33.07/13.89 ![X0]: (v3_struct_0(sK12110_skl)|~l3_lattices(sK12110_skl)|~m1_subset_1(X0,u1_struct_0(sK12109_skl))|~m1_subset_1(X0,u1_struct_0(sK12110_skl))|~m1_subset_1(sK12112_skl,u1_struct_0(sK12110_skl))|~r1_lattices(sK12109_skl,X0,sK12112_skl)|r1_lattices(sK12110_skl,X0,sK12112_skl))),
% 33.07/13.89 inference(resolution,[status(thm)],[f180988,f153999])).
% 33.07/13.89 fof(f180998,plain,(
% 33.07/13.89 ![X0]: (~l3_lattices(sK12110_skl)|~m1_subset_1(X0,u1_struct_0(sK12109_skl))|~m1_subset_1(X0,u1_struct_0(sK12110_skl))|~m1_subset_1(sK12112_skl,u1_struct_0(sK12110_skl))|~r1_lattices(sK12109_skl,X0,sK12112_skl)|r1_lattices(sK12110_skl,X0,sK12112_skl))),
% 33.07/13.89 inference(forward_subsumption_resolution,[status(thm)],[f180989,f153995])).
% 33.07/13.89 fof(f181010,plain,(
% 33.07/13.89 ![X0,X1]: (v3_struct_0(sK12109_skl)|~l3_lattices(sK12109_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(sK12109_skl))|~m1_subset_1(X1,u1_struct_0(sK12109_skl))|~r1_lattices(sK12110_skl,X0,X1)|r1_lattices(sK12109_skl,X0,X1))),
% 33.07/13.89 inference(forward_subsumption_resolution,[status(thm)],[f180985,f153996])).
% 33.07/13.89 fof(f181011,plain,(
% 33.07/13.89 ![X0]: (v3_struct_0(sK12109_skl)|~l3_lattices(sK12109_skl)|~m1_subset_1(X0,u1_struct_0(sK12110_skl))|~m1_subset_1(X0,u1_struct_0(sK12109_skl))|~m1_subset_1(sK12112_skl,u1_struct_0(sK12109_skl))|~r1_lattices(sK12110_skl,X0,sK12112_skl)|r1_lattices(sK12109_skl,X0,sK12112_skl))),
% 33.07/13.89 inference(resolution,[status(thm)],[f181010,f180887])).
% 33.07/13.89 fof(f181013,plain,(
% 33.07/13.89 ![X0]: (~l3_lattices(sK12109_skl)|~m1_subset_1(X0,u1_struct_0(sK12110_skl))|~m1_subset_1(X0,u1_struct_0(sK12109_skl))|~m1_subset_1(sK12112_skl,u1_struct_0(sK12109_skl))|~r1_lattices(sK12110_skl,X0,sK12112_skl)|r1_lattices(sK12109_skl,X0,sK12112_skl))),
% 33.07/13.89 inference(forward_subsumption_resolution,[status(thm)],[f181011,f153993])).
% 33.07/13.89 fof(f181189,plain,(
% 33.07/13.89 ![X0]: (~m1_subset_1(X0,u1_struct_0(sK12109_skl))|~m1_subset_1(sK12112_skl,u1_struct_0(sK12109_skl))|~m1_subset_1(X0,u1_struct_0(sK12110_skl))|k1_lattices(sK12109_skl,X0,sK12112_skl)=k1_lattices(sK12110_skl,X0,sK12112_skl))),
% 33.07/13.89 inference(forward_subsumption_resolution,[status(thm)],[f180945,f153996])).
% 33.07/13.89 fof(f181190,plain,(
% 33.07/13.89 ![X0]: (~m1_subset_1(X0,u1_struct_0(sK12109_skl))|~m1_subset_1(X0,u1_struct_0(sK12110_skl))|k1_lattices(sK12109_skl,X0,sK12112_skl)=k1_lattices(sK12110_skl,X0,sK12112_skl))),
% 33.07/13.89 inference(resolution,[status(thm)],[f181189,f153999])).
% 33.07/13.89 fof(f181191,plain,(
% 33.07/13.89 ~k1_lattices(sK12109_skl,sK12111_skl,sK12112_skl)=k1_lattices(sK12110_skl,sK12111_skl,sK12114_skl)|~k2_lattices(sK12109_skl,sK12111_skl,sK12112_skl)=k2_lattices(sK12110_skl,sK12113_skl,sK12114_skl)|sP1325_prd(sK12114_skl,sK12113_skl,sK12112_skl,sK12111_skl,sK12110_skl,sK12109_skl)|~r1_lattices(sK12109_skl,sK12111_skl,sK12112_skl)),
% 33.07/13.89 inference(forward_demodulation,[status(thm)],[f154002,f154005])).
% 33.07/13.89 fof(f181192,plain,(
% 33.07/13.89 ~k1_lattices(sK12109_skl,sK12111_skl,sK12112_skl)=k1_lattices(sK12110_skl,sK12111_skl,sK12112_skl)|~k2_lattices(sK12109_skl,sK12111_skl,sK12112_skl)=k2_lattices(sK12110_skl,sK12113_skl,sK12114_skl)|sP1325_prd(sK12114_skl,sK12113_skl,sK12112_skl,sK12111_skl,sK12110_skl,sK12109_skl)|~r1_lattices(sK12109_skl,sK12111_skl,sK12112_skl)),
% 33.07/13.89 inference(forward_demodulation,[status(thm)],[f154003,f181191])).
% 33.07/13.89 fof(f181193,plain,(
% 33.07/13.89 ~k1_lattices(sK12109_skl,sK12111_skl,sK12112_skl)=k1_lattices(sK12110_skl,sK12111_skl,sK12112_skl)|~k2_lattices(sK12109_skl,sK12111_skl,sK12112_skl)=k2_lattices(sK12110_skl,sK12111_skl,sK12114_skl)|sP1325_prd(sK12114_skl,sK12113_skl,sK12112_skl,sK12111_skl,sK12110_skl,sK12109_skl)|~r1_lattices(sK12109_skl,sK12111_skl,sK12112_skl)),
% 33.07/13.89 inference(forward_demodulation,[status(thm)],[f154002,f181192])).
% 33.07/13.89 fof(f181194,plain,(
% 33.07/13.89 ~k1_lattices(sK12109_skl,sK12111_skl,sK12112_skl)=k1_lattices(sK12110_skl,sK12111_skl,sK12112_skl)|~k2_lattices(sK12109_skl,sK12111_skl,sK12112_skl)=k2_lattices(sK12110_skl,sK12111_skl,sK12112_skl)|sP1325_prd(sK12114_skl,sK12113_skl,sK12112_skl,sK12111_skl,sK12110_skl,sK12109_skl)|~r1_lattices(sK12109_skl,sK12111_skl,sK12112_skl)),
% 33.07/13.89 inference(forward_demodulation,[status(thm)],[f154003,f181193])).
% 33.07/13.89 fof(f181195,plain,(
% 33.07/13.89 ~k1_lattices(sK12109_skl,sK12111_skl,sK12112_skl)=k1_lattices(sK12110_skl,sK12111_skl,sK12112_skl)|~k2_lattices(sK12109_skl,sK12111_skl,sK12112_skl)=k2_lattices(sK12110_skl,sK12111_skl,sK12112_skl)|sP1325_prd(sK12112_skl,sK12113_skl,sK12112_skl,sK12111_skl,sK12110_skl,sK12109_skl)|~r1_lattices(sK12109_skl,sK12111_skl,sK12112_skl)),
% 33.07/13.89 inference(forward_demodulation,[status(thm)],[f154003,f181194])).
% 33.07/13.89 fof(f181196,plain,(
% 33.07/13.89 ~k1_lattices(sK12109_skl,sK12111_skl,sK12112_skl)=k1_lattices(sK12110_skl,sK12111_skl,sK12112_skl)|~k2_lattices(sK12109_skl,sK12111_skl,sK12112_skl)=k2_lattices(sK12110_skl,sK12111_skl,sK12112_skl)|sP1325_prd(sK12112_skl,sK12111_skl,sK12112_skl,sK12111_skl,sK12110_skl,sK12109_skl)|~r1_lattices(sK12109_skl,sK12111_skl,sK12112_skl)),
% 33.07/13.89 inference(forward_demodulation,[status(thm)],[f154002,f181195])).
% 33.07/13.89 fof(f181198,plain,(
% 33.07/13.89 ~m1_subset_1(sK12111_skl,u1_struct_0(sK12109_skl))|k1_lattices(sK12109_skl,sK12111_skl,sK12112_skl)=k1_lattices(sK12110_skl,sK12111_skl,sK12112_skl)),
% 33.07/13.89 inference(resolution,[status(thm)],[f181190,f180886])).
% 33.07/13.89 fof(f181200,plain,(
% 33.07/13.89 k1_lattices(sK12109_skl,sK12111_skl,sK12112_skl)=k1_lattices(sK12110_skl,sK12111_skl,sK12112_skl)),
% 33.07/13.89 inference(forward_subsumption_resolution,[status(thm)],[f181198,f153998])).
% 33.07/13.89 fof(f181201,plain,(
% 33.07/13.89 ~k1_lattices(sK12109_skl,sK12111_skl,sK12112_skl)=k1_lattices(sK12109_skl,sK12111_skl,sK12112_skl)|~k2_lattices(sK12109_skl,sK12111_skl,sK12112_skl)=k2_lattices(sK12110_skl,sK12111_skl,sK12112_skl)|sP1325_prd(sK12112_skl,sK12111_skl,sK12112_skl,sK12111_skl,sK12110_skl,sK12109_skl)|~r1_lattices(sK12109_skl,sK12111_skl,sK12112_skl)),
% 33.07/13.89 inference(backward_demodulation,[status(thm)],[f181200,f181196])).
% 33.07/13.89 fof(f181202,plain,(
% 33.07/13.89 ~k1_lattices(sK12109_skl,sK12111_skl,sK12112_skl)=k1_lattices(sK12109_skl,sK12111_skl,sK12112_skl)|~k2_lattices(sK12109_skl,sK12111_skl,sK12112_skl)=k2_lattices(sK12110_skl,sK12111_skl,sK12112_skl)|sP1325_prd(sK12112_skl,sK12111_skl,sK12112_skl,sK12111_skl,sK12110_skl,sK12109_skl)|r1_lattices(sK12110_skl,sK12111_skl,sK12112_skl)),
% 33.07/13.89 inference(backward_demodulation,[status(thm)],[f181200,f180899])).
% 33.07/13.89 fof(f181203,plain,(
% 33.07/13.89 ~k2_lattices(sK12109_skl,sK12111_skl,sK12112_skl)=k2_lattices(sK12110_skl,sK12111_skl,sK12112_skl)|sP1325_prd(sK12112_skl,sK12111_skl,sK12112_skl,sK12111_skl,sK12110_skl,sK12109_skl)|~r1_lattices(sK12109_skl,sK12111_skl,sK12112_skl)),
% 33.07/13.89 inference(trivial_equality_resolution,[status(thm)],[f181201])).
% 33.07/13.89 fof(f181204,plain,(
% 33.07/13.89 ~k2_lattices(sK12109_skl,sK12111_skl,sK12112_skl)=k2_lattices(sK12110_skl,sK12111_skl,sK12112_skl)|sP1325_prd(sK12112_skl,sK12111_skl,sK12112_skl,sK12111_skl,sK12110_skl,sK12109_skl)|r1_lattices(sK12110_skl,sK12111_skl,sK12112_skl)),
% 33.07/13.89 inference(trivial_equality_resolution,[status(thm)],[f181202])).
% 33.07/13.89 fof(f181528,plain,(
% 33.07/13.89 ![X0]: (~m1_subset_1(X0,u1_struct_0(sK12109_skl))|~m1_subset_1(sK12112_skl,u1_struct_0(sK12109_skl))|~m1_subset_1(X0,u1_struct_0(sK12110_skl))|k2_lattices(sK12109_skl,X0,sK12112_skl)=k2_lattices(sK12110_skl,X0,sK12112_skl))),
% 33.07/13.89 inference(forward_subsumption_resolution,[status(thm)],[f180968,f153996])).
% 33.07/13.89 fof(f181529,plain,(
% 33.07/13.89 ![X0]: (~m1_subset_1(X0,u1_struct_0(sK12109_skl))|~m1_subset_1(X0,u1_struct_0(sK12110_skl))|k2_lattices(sK12109_skl,X0,sK12112_skl)=k2_lattices(sK12110_skl,X0,sK12112_skl))),
% 33.07/13.89 inference(resolution,[status(thm)],[f181528,f153999])).
% 33.07/13.89 fof(f181531,plain,(
% 33.07/13.89 ~m1_subset_1(sK12111_skl,u1_struct_0(sK12109_skl))|k2_lattices(sK12109_skl,sK12111_skl,sK12112_skl)=k2_lattices(sK12110_skl,sK12111_skl,sK12112_skl)),
% 33.07/13.89 inference(resolution,[status(thm)],[f181529,f180886])).
% 33.07/13.89 fof(f181533,plain,(
% 33.07/13.89 k2_lattices(sK12109_skl,sK12111_skl,sK12112_skl)=k2_lattices(sK12110_skl,sK12111_skl,sK12112_skl)),
% 33.07/13.89 inference(forward_subsumption_resolution,[status(thm)],[f181531,f153998])).
% 33.07/13.89 fof(f181537,plain,(
% 33.07/13.89 ~k2_lattices(sK12109_skl,sK12111_skl,sK12112_skl)=k2_lattices(sK12109_skl,sK12111_skl,sK12112_skl)|sP1325_prd(sK12112_skl,sK12111_skl,sK12112_skl,sK12111_skl,sK12110_skl,sK12109_skl)|r1_lattices(sK12110_skl,sK12111_skl,sK12112_skl)),
% 33.07/13.89 inference(backward_demodulation,[status(thm)],[f181533,f181204])).
% 33.07/13.89 fof(f181538,plain,(
% 33.07/13.89 ~k2_lattices(sK12109_skl,sK12111_skl,sK12112_skl)=k2_lattices(sK12109_skl,sK12111_skl,sK12112_skl)|sP1325_prd(sK12112_skl,sK12111_skl,sK12112_skl,sK12111_skl,sK12110_skl,sK12109_skl)|~r1_lattices(sK12109_skl,sK12111_skl,sK12112_skl)),
% 33.07/13.89 inference(backward_demodulation,[status(thm)],[f181533,f181203])).
% 33.07/13.89 fof(f181540,plain,(
% 33.07/13.89 sP1325_prd(sK12112_skl,sK12111_skl,sK12112_skl,sK12111_skl,sK12110_skl,sK12109_skl)|r1_lattices(sK12110_skl,sK12111_skl,sK12112_skl)),
% 33.07/13.89 inference(trivial_equality_resolution,[status(thm)],[f181537])).
% 33.07/13.89 fof(f181541,plain,(
% 33.07/13.89 sP1325_prd(sK12112_skl,sK12111_skl,sK12112_skl,sK12111_skl,sK12110_skl,sK12109_skl)|~r1_lattices(sK12109_skl,sK12111_skl,sK12112_skl)),
% 33.07/13.89 inference(trivial_equality_resolution,[status(thm)],[f181538])).
% 33.07/13.89 fof(f181558,plain,(
% 33.07/13.89 r1_lattices(sK12110_skl,sK12111_skl,sK12112_skl)|r1_lattices(sK12109_skl,sK12111_skl,sK12112_skl)),
% 33.07/13.89 inference(resolution,[status(thm)],[f181540,f164091])).
% 33.07/13.89 fof(f181678,plain,(
% 33.07/13.89 ![X0]: (~m1_subset_1(X0,u1_struct_0(sK12109_skl))|~m1_subset_1(X0,u1_struct_0(sK12110_skl))|~m1_subset_1(sK12112_skl,u1_struct_0(sK12110_skl))|~r1_lattices(sK12109_skl,X0,sK12112_skl)|r1_lattices(sK12110_skl,X0,sK12112_skl))),
% 33.07/13.89 inference(forward_subsumption_resolution,[status(thm)],[f180998,f153996])).
% 33.07/13.89 fof(f181681,plain,(
% 33.07/13.89 ~m1_subset_1(sK12111_skl,u1_struct_0(sK12109_skl))|~m1_subset_1(sK12112_skl,u1_struct_0(sK12110_skl))|~r1_lattices(sK12109_skl,sK12111_skl,sK12112_skl)|r1_lattices(sK12110_skl,sK12111_skl,sK12112_skl)),
% 33.07/13.89 inference(resolution,[status(thm)],[f181678,f180886])).
% 33.07/13.89 fof(f181684,plain,(
% 33.07/13.89 ~m1_subset_1(sK12112_skl,u1_struct_0(sK12110_skl))|~r1_lattices(sK12109_skl,sK12111_skl,sK12112_skl)|r1_lattices(sK12110_skl,sK12111_skl,sK12112_skl)),
% 33.07/13.89 inference(forward_subsumption_resolution,[status(thm)],[f181681,f153998])).
% 33.07/13.89 fof(f181685,plain,(
% 33.07/13.89 r1_lattices(sK12110_skl,sK12111_skl,sK12112_skl)),
% 33.07/13.89 inference(backward_subsumption_resolution,[status(thm)],[f181558,f181686])).
% 33.07/13.89 fof(f181686,plain,(
% 33.07/13.89 ~r1_lattices(sK12109_skl,sK12111_skl,sK12112_skl)|r1_lattices(sK12110_skl,sK12111_skl,sK12112_skl)),
% 33.07/13.89 inference(forward_subsumption_resolution,[status(thm)],[f181684,f180887])).
% 33.07/13.89 fof(f182192,plain,(
% 33.07/13.89 ![X0]: (~m1_subset_1(X0,u1_struct_0(sK12110_skl))|~m1_subset_1(X0,u1_struct_0(sK12109_skl))|~m1_subset_1(sK12112_skl,u1_struct_0(sK12109_skl))|~r1_lattices(sK12110_skl,X0,sK12112_skl)|r1_lattices(sK12109_skl,X0,sK12112_skl))),
% 33.07/13.89 inference(forward_subsumption_resolution,[status(thm)],[f181013,f153994])).
% 33.07/13.89 fof(f182194,plain,(
% 33.07/13.89 ~m1_subset_1(sK12111_skl,u1_struct_0(sK12110_skl))|~m1_subset_1(sK12111_skl,u1_struct_0(sK12109_skl))|~m1_subset_1(sK12112_skl,u1_struct_0(sK12109_skl))|r1_lattices(sK12109_skl,sK12111_skl,sK12112_skl)),
% 33.07/13.89 inference(resolution,[status(thm)],[f182192,f181685])).
% 33.07/13.89 fof(f182195,plain,(
% 33.07/13.89 ~m1_subset_1(sK12111_skl,u1_struct_0(sK12109_skl))|~m1_subset_1(sK12112_skl,u1_struct_0(sK12109_skl))|r1_lattices(sK12109_skl,sK12111_skl,sK12112_skl)),
% 33.07/13.89 inference(forward_subsumption_resolution,[status(thm)],[f182194,f180886])).
% 33.07/13.89 fof(f182196,plain,(
% 33.07/13.89 ~m1_subset_1(sK12112_skl,u1_struct_0(sK12109_skl))|r1_lattices(sK12109_skl,sK12111_skl,sK12112_skl)),
% 33.07/13.89 inference(forward_subsumption_resolution,[status(thm)],[f182195,f153998])).
% 33.07/13.89 fof(f182197,plain,(
% 33.07/13.89 r1_lattices(sK12109_skl,sK12111_skl,sK12112_skl)),
% 33.07/13.89 inference(resolution,[status(thm)],[f182196,f153999])).
% 33.07/13.89 fof(f182540,plain,(
% 33.07/13.89 sP1325_prd(sK12112_skl,sK12111_skl,sK12112_skl,sK12111_skl,sK12110_skl,sK12109_skl)),
% 37.78/14.18 inference(backward_subsumption_resolution,[status(thm)],[f181541,f182197])).
% 37.78/14.18 fof(f182545,plain,(
% 37.78/14.18 ~r1_lattices(sK12110_skl,sK12111_skl,sK12112_skl)),
% 37.78/14.18 inference(resolution,[status(thm)],[f182540,f164092])).
% 37.78/14.18 fof(f182547,plain,(
% 37.78/14.18 $false),
% 37.78/14.18 inference(forward_subsumption_resolution,[status(thm)],[f182545,f181685])).
% 37.78/14.18 % SZS output end CNFRefutation for theBenchmark.p
% 12.13/15.27 % Elapsed time: 14.464543 seconds
% 12.13/15.27 % CPU time: 37.230798 seconds
% 12.13/15.27 % Total memory used: 11.035 GB
% 12.13/15.27 % Net memory used: 10.978 GB
%------------------------------------------------------------------------------