%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LAT345+1 : 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 : n013.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:46 PM UTC 2026
% Result : Theorem 13.71s 2.27s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LAT345+1 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.44 % Computer : n013.cluster.edu
% 0.18/0.44 % Model : x86_64 x86_64
% 0.18/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.44 % Memory : 8046.5625MB
% 0.18/0.44 % OS : Linux 6.8.0-71-generic
% 0.18/0.44 % CPULimit : 300
% 0.18/0.44 % WCLimit : 300
% 0.18/0.44 % DateTime : Sun Sep 20 23:43:35 UTC 2026
% 0.18/0.44 % CPUTime :
% 0.18/0.46 % Drodi V4.1.1
% 13.71/2.27 % Refutation found
% 13.71/2.27 % SZS status Theorem for theBenchmark: Theorem is valid
% 13.71/2.27 % SZS output start CNFRefutation for theBenchmark
% 13.71/2.27 fof(f1,conjecture,(
% 13.71/2.27 (! [A] :( ( ~ v3_conlat_1(A)& v4_conlat_1(A)& l2_conlat_1(A) )=> (! [B] :( ( v6_conlat_1(B,A)& ~ v7_conlat_1(B,A)& v9_conlat_1(B,A)& l3_conlat_1(B,A) )=> k9_conlat_2(k7_conlat_2(A),k9_conlat_2(A,B)) = B ) )) )),
% 13.71/2.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 13.71/2.27 fof(f2,negated_conjecture,(
% 13.71/2.27 ~((! [A] :( ( ~ v3_conlat_1(A)& v4_conlat_1(A)& l2_conlat_1(A) )=> (! [B] :( ( v6_conlat_1(B,A)& ~ v7_conlat_1(B,A)& v9_conlat_1(B,A)& l3_conlat_1(B,A) )=> k9_conlat_2(k7_conlat_2(A),k9_conlat_2(A,B)) = B ) )) ))),
% 13.71/2.27 inference(negated_conjecture,[status(cth)],[f1])).
% 13.71/2.27 fof(f3,axiom,(
% 13.71/2.27 (! [A] :( l2_conlat_1(A)=> ( v4_conlat_1(A)=> A = g2_conlat_1(u1_conlat_1(A),u2_conlat_1(A),u3_conlat_1(A)) ) ) )),
% 13.71/2.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 13.71/2.27 fof(f4,axiom,(
% 13.71/2.27 (! [A,B] :( ( l1_conlat_1(A)& l3_conlat_1(B,A) )=> ( v6_conlat_1(B,A)=> B = g3_conlat_1(A,u4_conlat_1(A,B),u5_conlat_1(A,B)) ) ) )),
% 13.71/2.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 13.71/2.27 fof(f6,axiom,(
% 13.71/2.27 (! [A,B,C] :( m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B)))=> v1_relat_1(C) ) )),
% 13.71/2.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 13.71/2.27 fof(f8,axiom,(
% 13.71/2.27 (! [A] :( ( ~ v3_conlat_1(A)& l2_conlat_1(A) )=> k7_conlat_2(A) = g2_conlat_1(u2_conlat_1(A),u1_conlat_1(A),k6_relset_1(u1_conlat_1(A),u2_conlat_1(A),u3_conlat_1(A))) ) )),
% 13.71/2.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 13.71/2.27 fof(f9,axiom,(
% 13.71/2.27 (! [A] :( ( ~ v3_conlat_1(A)& l2_conlat_1(A) )=> (! [B] :( l3_conlat_1(B,A)=> (! [C] :( ( v6_conlat_1(C,k7_conlat_2(A))& l3_conlat_1(C,k7_conlat_2(A)) )=> ( C = k8_conlat_2(A,B)<=> ( u4_conlat_1(k7_conlat_2(A),C) = u5_conlat_1(A,B)& u5_conlat_1(k7_conlat_2(A),C) = u4_conlat_1(A,B) ) ) ) )) )) )),
% 13.71/2.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 13.71/2.27 fof(f10,axiom,(
% 13.71/2.27 (! [A,B,C] :( m1_relset_1(C,A,B)=> ( v4_conlat_1(g2_conlat_1(A,B,C))& l2_conlat_1(g2_conlat_1(A,B,C)) ) ) )),
% 13.71/2.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 13.71/2.27 fof(f16,axiom,(
% 13.71/2.27 (! [A,B,C] :( m1_relset_1(C,A,B)=> m2_relset_1(k6_relset_1(A,B,C),B,A) ) )),
% 13.71/2.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 13.71/2.27 fof(f17,axiom,(
% 13.71/2.27 (! [A] :( ( ~ v3_conlat_1(A)& l2_conlat_1(A) )=> ( ~ v3_conlat_1(k7_conlat_2(A))& v4_conlat_1(k7_conlat_2(A))& l2_conlat_1(k7_conlat_2(A)) ) ) )),
% 13.71/2.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 13.71/2.27 fof(f18,axiom,(
% 13.71/2.27 (! [A,B] :( ( ~ v3_conlat_1(A)& l2_conlat_1(A)& l3_conlat_1(B,A) )=> ( v6_conlat_1(k8_conlat_2(A,B),k7_conlat_2(A))& l3_conlat_1(k8_conlat_2(A,B),k7_conlat_2(A)) ) ) )),
% 13.71/2.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 13.71/2.27 fof(f19,axiom,(
% 13.71/2.27 (! [A,B] :( ( ~ v3_conlat_1(A)& l2_conlat_1(A)& ~ v7_conlat_1(B,A)& v9_conlat_1(B,A)& l3_conlat_1(B,A) )=> ( v6_conlat_1(k9_conlat_2(A,B),k7_conlat_2(A))& ~ v7_conlat_1(k9_conlat_2(A,B),k7_conlat_2(A))& v9_conlat_1(k9_conlat_2(A,B),k7_conlat_2(A))& l3_conlat_1(k9_conlat_2(A,B),k7_conlat_2(A)) ) ) )),
% 13.71/2.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 13.71/2.27 fof(f21,axiom,(
% 13.71/2.27 (! [A] :( l2_conlat_1(A)=> l1_conlat_1(A) ) )),
% 13.71/2.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 13.71/2.27 fof(f25,axiom,(
% 13.71/2.27 (! [A,B,C] :( m2_relset_1(C,A,B)=> m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))) ) )),
% 13.71/2.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 13.71/2.27 fof(f28,axiom,(
% 13.71/2.27 (! [A] :( l2_conlat_1(A)=> m2_relset_1(u3_conlat_1(A),u1_conlat_1(A),u2_conlat_1(A)) ) )),
% 13.71/2.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 13.71/2.27 fof(f42,axiom,(
% 13.71/2.27 (! [A,B,C] :( m1_relset_1(C,A,B)=> (! [D,E,F] :( g2_conlat_1(A,B,C) = g2_conlat_1(D,E,F)=> ( A = D& B = E& C = F ) ) )) )),
% 13.71/2.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 13.71/2.27 fof(f44,axiom,(
% 13.71/2.27 (! [A] :( v1_relat_1(A)=> k4_relat_1(k4_relat_1(A)) = A ) )),
% 13.71/2.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 13.71/2.27 fof(f59,axiom,(
% 13.71/2.27 (! [A,B,C] :( m1_relset_1(C,A,B)=> k6_relset_1(A,B,C) = k4_relat_1(C) ) )),
% 13.71/2.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 13.71/2.27 fof(f60,axiom,(
% 13.71/2.27 (! [A,B] :( ( ~ v3_conlat_1(A)& l2_conlat_1(A)& ~ v7_conlat_1(B,A)& v9_conlat_1(B,A)& l3_conlat_1(B,A) )=> k9_conlat_2(A,B) = k8_conlat_2(A,B) ) )),
% 13.71/2.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 13.71/2.27 fof(f61,axiom,(
% 13.71/2.27 (! [A,B,C] :( m2_relset_1(C,A,B)<=> m1_relset_1(C,A,B) ) )),
% 13.71/2.27 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 13.71/2.27 fof(f71,plain,(
% 13.71/2.27 (?[A]: (((~v3_conlat_1(A)&v4_conlat_1(A))&l2_conlat_1(A))&(?[B]: ((((v6_conlat_1(B,A)&~v7_conlat_1(B,A))&v9_conlat_1(B,A))&l3_conlat_1(B,A))&~k9_conlat_2(k7_conlat_2(A),k9_conlat_2(A,B))=B))))),
% 13.71/2.27 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 13.71/2.27 fof(f72,plain,(
% 13.71/2.27 (((~v3_conlat_1(sK0_skl)&v4_conlat_1(sK0_skl))&l2_conlat_1(sK0_skl))&((((v6_conlat_1(sK1_skl,sK0_skl)&~v7_conlat_1(sK1_skl,sK0_skl))&v9_conlat_1(sK1_skl,sK0_skl))&l3_conlat_1(sK1_skl,sK0_skl))&~k9_conlat_2(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl))=sK1_skl))),
% 13.71/2.27 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(A,sK0_skl),skolemize(B,sK1_skl)],[f71])).
% 13.71/2.27 fof(f73,plain,(
% 13.71/2.27 ~v3_conlat_1(sK0_skl)),
% 13.71/2.27 inference(cnf_transformation,[status(thm)],[f72])).
% 13.71/2.27 fof(f74,plain,(
% 13.71/2.27 v4_conlat_1(sK0_skl)),
% 13.71/2.27 inference(cnf_transformation,[status(thm)],[f72])).
% 13.71/2.27 fof(f75,plain,(
% 13.71/2.27 l2_conlat_1(sK0_skl)),
% 13.71/2.27 inference(cnf_transformation,[status(thm)],[f72])).
% 13.71/2.27 fof(f76,plain,(
% 13.71/2.27 v6_conlat_1(sK1_skl,sK0_skl)),
% 13.71/2.27 inference(cnf_transformation,[status(thm)],[f72])).
% 13.71/2.27 fof(f77,plain,(
% 13.71/2.27 ~v7_conlat_1(sK1_skl,sK0_skl)),
% 13.71/2.27 inference(cnf_transformation,[status(thm)],[f72])).
% 13.71/2.27 fof(f78,plain,(
% 13.71/2.27 v9_conlat_1(sK1_skl,sK0_skl)),
% 13.71/2.27 inference(cnf_transformation,[status(thm)],[f72])).
% 13.71/2.27 fof(f79,plain,(
% 13.71/2.27 l3_conlat_1(sK1_skl,sK0_skl)),
% 13.71/2.27 inference(cnf_transformation,[status(thm)],[f72])).
% 13.71/2.27 fof(f80,plain,(
% 13.71/2.27 ~k9_conlat_2(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl))=sK1_skl),
% 13.71/2.27 inference(cnf_transformation,[status(thm)],[f72])).
% 13.71/2.27 fof(f81,plain,(
% 13.71/2.27 ![A]: (~l2_conlat_1(A)|(~v4_conlat_1(A)|A=g2_conlat_1(u1_conlat_1(A),u2_conlat_1(A),u3_conlat_1(A))))),
% 13.71/2.27 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 13.71/2.27 fof(f82,plain,(
% 13.71/2.27 ![X0]: (~l2_conlat_1(X0)|~v4_conlat_1(X0)|X0=g2_conlat_1(u1_conlat_1(X0),u2_conlat_1(X0),u3_conlat_1(X0)))),
% 13.71/2.27 inference(cnf_transformation,[status(thm)],[f81])).
% 13.71/2.27 fof(f83,plain,(
% 13.71/2.27 ![A,B]: ((~l1_conlat_1(A)|~l3_conlat_1(B,A))|(~v6_conlat_1(B,A)|B=g3_conlat_1(A,u4_conlat_1(A,B),u5_conlat_1(A,B))))),
% 13.71/2.27 inference(pre_NNF_transformation,[status(thm)],[f4])).
% 13.71/2.27 fof(f84,plain,(
% 13.71/2.27 ![X0,X1]: (~l1_conlat_1(X0)|~l3_conlat_1(X1,X0)|~v6_conlat_1(X1,X0)|X1=g3_conlat_1(X0,u4_conlat_1(X0,X1),u5_conlat_1(X0,X1)))),
% 13.71/2.27 inference(cnf_transformation,[status(thm)],[f83])).
% 13.71/2.27 fof(f87,plain,(
% 13.71/2.27 ![A,B,C]: (~m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B)))|v1_relat_1(C))),
% 13.71/2.27 inference(pre_NNF_transformation,[status(thm)],[f6])).
% 13.71/2.27 fof(f88,plain,(
% 13.71/2.27 ![C]: ((![A,B]: ~m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))))|v1_relat_1(C))),
% 13.71/2.27 inference(miniscoping,[status(thm)],[f87])).
% 13.71/2.27 fof(f89,plain,(
% 13.71/2.27 ![X0,X1,X2]: (~m1_subset_1(X0,k1_zfmisc_1(k2_zfmisc_1(X1,X2)))|v1_relat_1(X0))),
% 13.71/2.27 inference(cnf_transformation,[status(thm)],[f88])).
% 13.71/2.27 fof(f92,plain,(
% 13.71/2.27 ![A]: ((v3_conlat_1(A)|~l2_conlat_1(A))|k7_conlat_2(A)=g2_conlat_1(u2_conlat_1(A),u1_conlat_1(A),k6_relset_1(u1_conlat_1(A),u2_conlat_1(A),u3_conlat_1(A))))),
% 13.71/2.27 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 13.71/2.27 fof(f93,plain,(
% 13.71/2.27 ![X0]: (v3_conlat_1(X0)|~l2_conlat_1(X0)|k7_conlat_2(X0)=g2_conlat_1(u2_conlat_1(X0),u1_conlat_1(X0),k6_relset_1(u1_conlat_1(X0),u2_conlat_1(X0),u3_conlat_1(X0))))),
% 13.71/2.27 inference(cnf_transformation,[status(thm)],[f92])).
% 13.71/2.27 fof(f94,plain,(
% 13.71/2.27 ![A]: ((v3_conlat_1(A)|~l2_conlat_1(A))|(![B]: (~l3_conlat_1(B,A)|(![C]: ((~v6_conlat_1(C,k7_conlat_2(A))|~l3_conlat_1(C,k7_conlat_2(A)))|(C=k8_conlat_2(A,B)<=>(u4_conlat_1(k7_conlat_2(A),C)=u5_conlat_1(A,B)&u5_conlat_1(k7_conlat_2(A),C)=u4_conlat_1(A,B))))))))),
% 13.71/2.27 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 13.71/2.27 fof(f95,plain,(
% 13.71/2.27 ![A]: ((v3_conlat_1(A)|~l2_conlat_1(A))|(![B]: (~l3_conlat_1(B,A)|(![C]: ((~v6_conlat_1(C,k7_conlat_2(A))|~l3_conlat_1(C,k7_conlat_2(A)))|((~C=k8_conlat_2(A,B)|(u4_conlat_1(k7_conlat_2(A),C)=u5_conlat_1(A,B)&u5_conlat_1(k7_conlat_2(A),C)=u4_conlat_1(A,B)))&(C=k8_conlat_2(A,B)|(~u4_conlat_1(k7_conlat_2(A),C)=u5_conlat_1(A,B)|~u5_conlat_1(k7_conlat_2(A),C)=u4_conlat_1(A,B)))))))))),
% 13.71/2.27 inference(NNF_transformation,[status(thm)],[f94])).
% 13.71/2.27 fof(f96,plain,(
% 13.71/2.27 ![X0,X1,X2]: (v3_conlat_1(X0)|~l2_conlat_1(X0)|~l3_conlat_1(X1,X0)|~v6_conlat_1(X2,k7_conlat_2(X0))|~l3_conlat_1(X2,k7_conlat_2(X0))|~X2=k8_conlat_2(X0,X1)|u4_conlat_1(k7_conlat_2(X0),X2)=u5_conlat_1(X0,X1))),
% 13.71/2.27 inference(cnf_transformation,[status(thm)],[f95])).
% 13.71/2.27 fof(f97,plain,(
% 13.71/2.27 ![X0,X1,X2]: (v3_conlat_1(X0)|~l2_conlat_1(X0)|~l3_conlat_1(X1,X0)|~v6_conlat_1(X2,k7_conlat_2(X0))|~l3_conlat_1(X2,k7_conlat_2(X0))|~X2=k8_conlat_2(X0,X1)|u5_conlat_1(k7_conlat_2(X0),X2)=u4_conlat_1(X0,X1))),
% 13.71/2.27 inference(cnf_transformation,[status(thm)],[f95])).
% 13.71/2.27 fof(f99,plain,(
% 13.71/2.27 ![A,B,C]: (~m1_relset_1(C,A,B)|(v4_conlat_1(g2_conlat_1(A,B,C))&l2_conlat_1(g2_conlat_1(A,B,C))))),
% 13.71/2.27 inference(pre_NNF_transformation,[status(thm)],[f10])).
% 13.71/2.27 fof(f101,plain,(
% 13.71/2.27 ![X0,X1,X2]: (~m1_relset_1(X0,X1,X2)|l2_conlat_1(g2_conlat_1(X1,X2,X0)))),
% 13.71/2.27 inference(cnf_transformation,[status(thm)],[f99])).
% 13.71/2.27 fof(f107,plain,(
% 13.71/2.27 ![A,B,C]: (~m1_relset_1(C,A,B)|m2_relset_1(k6_relset_1(A,B,C),B,A))),
% 13.71/2.27 inference(pre_NNF_transformation,[status(thm)],[f16])).
% 13.71/2.27 fof(f108,plain,(
% 13.71/2.27 ![X0,X1,X2]: (~m1_relset_1(X0,X1,X2)|m2_relset_1(k6_relset_1(X1,X2,X0),X2,X1))),
% 13.71/2.27 inference(cnf_transformation,[status(thm)],[f107])).
% 13.71/2.27 fof(f109,plain,(
% 13.71/2.27 ![A]: ((v3_conlat_1(A)|~l2_conlat_1(A))|((~v3_conlat_1(k7_conlat_2(A))&v4_conlat_1(k7_conlat_2(A)))&l2_conlat_1(k7_conlat_2(A))))),
% 13.71/2.27 inference(pre_NNF_transformation,[status(thm)],[f17])).
% 13.71/2.27 fof(f110,plain,(
% 13.71/2.27 ![X0]: (v3_conlat_1(X0)|~l2_conlat_1(X0)|~v3_conlat_1(k7_conlat_2(X0)))),
% 13.71/2.27 inference(cnf_transformation,[status(thm)],[f109])).
% 13.71/2.27 fof(f111,plain,(
% 13.71/2.27 ![X0]: (v3_conlat_1(X0)|~l2_conlat_1(X0)|v4_conlat_1(k7_conlat_2(X0)))),
% 13.71/2.27 inference(cnf_transformation,[status(thm)],[f109])).
% 13.71/2.27 fof(f112,plain,(
% 13.71/2.27 ![X0]: (v3_conlat_1(X0)|~l2_conlat_1(X0)|l2_conlat_1(k7_conlat_2(X0)))),
% 13.71/2.27 inference(cnf_transformation,[status(thm)],[f109])).
% 13.71/2.27 fof(f113,plain,(
% 13.71/2.27 ![A,B]: (((v3_conlat_1(A)|~l2_conlat_1(A))|~l3_conlat_1(B,A))|(v6_conlat_1(k8_conlat_2(A,B),k7_conlat_2(A))&l3_conlat_1(k8_conlat_2(A,B),k7_conlat_2(A))))),
% 13.71/2.27 inference(pre_NNF_transformation,[status(thm)],[f18])).
% 13.71/2.27 fof(f114,plain,(
% 13.71/2.27 ![X0,X1]: (v3_conlat_1(X0)|~l2_conlat_1(X0)|~l3_conlat_1(X1,X0)|v6_conlat_1(k8_conlat_2(X0,X1),k7_conlat_2(X0)))),
% 13.71/2.27 inference(cnf_transformation,[status(thm)],[f113])).
% 13.71/2.27 fof(f115,plain,(
% 13.71/2.27 ![X0,X1]: (v3_conlat_1(X0)|~l2_conlat_1(X0)|~l3_conlat_1(X1,X0)|l3_conlat_1(k8_conlat_2(X0,X1),k7_conlat_2(X0)))),
% 13.71/2.27 inference(cnf_transformation,[status(thm)],[f113])).
% 13.71/2.27 fof(f116,plain,(
% 13.71/2.27 ![A,B]: (((((v3_conlat_1(A)|~l2_conlat_1(A))|v7_conlat_1(B,A))|~v9_conlat_1(B,A))|~l3_conlat_1(B,A))|(((v6_conlat_1(k9_conlat_2(A,B),k7_conlat_2(A))&~v7_conlat_1(k9_conlat_2(A,B),k7_conlat_2(A)))&v9_conlat_1(k9_conlat_2(A,B),k7_conlat_2(A)))&l3_conlat_1(k9_conlat_2(A,B),k7_conlat_2(A))))),
% 13.71/2.27 inference(pre_NNF_transformation,[status(thm)],[f19])).
% 13.71/2.27 fof(f118,plain,(
% 13.71/2.27 ![X0,X1]: (v3_conlat_1(X0)|~l2_conlat_1(X0)|v7_conlat_1(X1,X0)|~v9_conlat_1(X1,X0)|~l3_conlat_1(X1,X0)|~v7_conlat_1(k9_conlat_2(X0,X1),k7_conlat_2(X0)))),
% 13.71/2.27 inference(cnf_transformation,[status(thm)],[f116])).
% 13.71/2.27 fof(f119,plain,(
% 13.71/2.27 ![X0,X1]: (v3_conlat_1(X0)|~l2_conlat_1(X0)|v7_conlat_1(X1,X0)|~v9_conlat_1(X1,X0)|~l3_conlat_1(X1,X0)|v9_conlat_1(k9_conlat_2(X0,X1),k7_conlat_2(X0)))),
% 13.71/2.27 inference(cnf_transformation,[status(thm)],[f116])).
% 13.71/2.27 fof(f120,plain,(
% 13.71/2.27 ![X0,X1]: (v3_conlat_1(X0)|~l2_conlat_1(X0)|v7_conlat_1(X1,X0)|~v9_conlat_1(X1,X0)|~l3_conlat_1(X1,X0)|l3_conlat_1(k9_conlat_2(X0,X1),k7_conlat_2(X0)))),
% 13.71/2.27 inference(cnf_transformation,[status(thm)],[f116])).
% 13.71/2.27 fof(f121,plain,(
% 13.71/2.27 ![A]: (~l2_conlat_1(A)|l1_conlat_1(A))),
% 13.71/2.27 inference(pre_NNF_transformation,[status(thm)],[f21])).
% 13.71/2.27 fof(f122,plain,(
% 13.71/2.27 ![X0]: (~l2_conlat_1(X0)|l1_conlat_1(X0))),
% 13.71/2.27 inference(cnf_transformation,[status(thm)],[f121])).
% 13.71/2.27 fof(f123,plain,(
% 13.71/2.27 ![A,B,C]: (~m2_relset_1(C,A,B)|m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))))),
% 13.71/2.27 inference(pre_NNF_transformation,[status(thm)],[f25])).
% 13.71/2.27 fof(f124,plain,(
% 13.71/2.27 ![X0,X1,X2]: (~m2_relset_1(X0,X1,X2)|m1_subset_1(X0,k1_zfmisc_1(k2_zfmisc_1(X1,X2))))),
% 13.71/2.27 inference(cnf_transformation,[status(thm)],[f123])).
% 13.71/2.27 fof(f125,plain,(
% 13.71/2.27 ![A]: (~l2_conlat_1(A)|m2_relset_1(u3_conlat_1(A),u1_conlat_1(A),u2_conlat_1(A)))),
% 13.71/2.27 inference(pre_NNF_transformation,[status(thm)],[f28])).
% 13.71/2.27 fof(f126,plain,(
% 13.71/2.27 ![X0]: (~l2_conlat_1(X0)|m2_relset_1(u3_conlat_1(X0),u1_conlat_1(X0),u2_conlat_1(X0)))),
% 13.71/2.27 inference(cnf_transformation,[status(thm)],[f125])).
% 13.71/2.27 fof(f152,plain,(
% 13.71/2.27 ![A,B,C]: (~m1_relset_1(C,A,B)|(![D,E,F]: (~g2_conlat_1(A,B,C)=g2_conlat_1(D,E,F)|((A=D&B=E)&C=F))))),
% 13.71/2.27 inference(pre_NNF_transformation,[status(thm)],[f42])).
% 13.71/2.27 fof(f153,plain,(
% 13.71/2.27 ![X0,X1,X2,X3,X4,X5]: (~m1_relset_1(X0,X1,X2)|~g2_conlat_1(X1,X2,X0)=g2_conlat_1(X3,X4,X5)|X1=X3)),
% 13.71/2.27 inference(cnf_transformation,[status(thm)],[f152])).
% 13.71/2.27 fof(f154,plain,(
% 13.71/2.27 ![X0,X1,X2,X3,X4,X5]: (~m1_relset_1(X0,X1,X2)|~g2_conlat_1(X1,X2,X0)=g2_conlat_1(X3,X4,X5)|X2=X4)),
% 13.71/2.27 inference(cnf_transformation,[status(thm)],[f152])).
% 13.71/2.27 fof(f155,plain,(
% 13.71/2.27 ![X0,X1,X2,X3,X4,X5]: (~m1_relset_1(X0,X1,X2)|~g2_conlat_1(X1,X2,X0)=g2_conlat_1(X3,X4,X5)|X0=X5)),
% 13.71/2.27 inference(cnf_transformation,[status(thm)],[f152])).
% 13.71/2.27 fof(f160,plain,(
% 13.71/2.27 ![A]: (~v1_relat_1(A)|k4_relat_1(k4_relat_1(A))=A)),
% 13.71/2.27 inference(pre_NNF_transformation,[status(thm)],[f44])).
% 13.71/2.27 fof(f161,plain,(
% 13.71/2.27 ![X0]: (~v1_relat_1(X0)|k4_relat_1(k4_relat_1(X0))=X0)),
% 13.71/2.27 inference(cnf_transformation,[status(thm)],[f160])).
% 13.71/2.27 fof(f215,plain,(
% 13.71/2.27 ![A,B,C]: (~m1_relset_1(C,A,B)|k6_relset_1(A,B,C)=k4_relat_1(C))),
% 13.71/2.27 inference(pre_NNF_transformation,[status(thm)],[f59])).
% 13.71/2.27 fof(f216,plain,(
% 13.71/2.27 ![X0,X1,X2]: (~m1_relset_1(X0,X1,X2)|k6_relset_1(X1,X2,X0)=k4_relat_1(X0))),
% 13.71/2.27 inference(cnf_transformation,[status(thm)],[f215])).
% 13.71/2.27 fof(f217,plain,(
% 13.71/2.27 ![A,B]: (((((v3_conlat_1(A)|~l2_conlat_1(A))|v7_conlat_1(B,A))|~v9_conlat_1(B,A))|~l3_conlat_1(B,A))|k9_conlat_2(A,B)=k8_conlat_2(A,B))),
% 13.71/2.27 inference(pre_NNF_transformation,[status(thm)],[f60])).
% 13.71/2.27 fof(f218,plain,(
% 13.71/2.27 ![X0,X1]: (v3_conlat_1(X0)|~l2_conlat_1(X0)|v7_conlat_1(X1,X0)|~v9_conlat_1(X1,X0)|~l3_conlat_1(X1,X0)|k9_conlat_2(X0,X1)=k8_conlat_2(X0,X1))),
% 13.71/2.27 inference(cnf_transformation,[status(thm)],[f217])).
% 13.71/2.27 fof(f219,plain,(
% 13.71/2.27 ![A,B,C]: ((~m2_relset_1(C,A,B)|m1_relset_1(C,A,B))&(m2_relset_1(C,A,B)|~m1_relset_1(C,A,B)))),
% 13.71/2.27 inference(NNF_transformation,[status(thm)],[f61])).
% 13.71/2.27 fof(f220,plain,(
% 13.71/2.27 (![A,B,C]: (~m2_relset_1(C,A,B)|m1_relset_1(C,A,B)))&(![A,B,C]: (m2_relset_1(C,A,B)|~m1_relset_1(C,A,B)))),
% 13.71/2.27 inference(miniscoping,[status(thm)],[f219])).
% 13.71/2.27 fof(f221,plain,(
% 13.71/2.27 ![X0,X1,X2]: (~m2_relset_1(X0,X1,X2)|m1_relset_1(X0,X1,X2))),
% 13.71/2.27 inference(cnf_transformation,[status(thm)],[f220])).
% 13.71/2.27 fof(f247,plain,(
% 13.71/2.27 ![X0,X1]: (v3_conlat_1(X0)|~l2_conlat_1(X0)|~l3_conlat_1(X1,X0)|~v6_conlat_1(k8_conlat_2(X0,X1),k7_conlat_2(X0))|~l3_conlat_1(k8_conlat_2(X0,X1),k7_conlat_2(X0))|u4_conlat_1(k7_conlat_2(X0),k8_conlat_2(X0,X1))=u5_conlat_1(X0,X1))),
% 13.71/2.27 inference(destructive_equality_resolution,[status(thm)],[f96])).
% 13.71/2.27 fof(f248,plain,(
% 13.71/2.27 ![X0,X1]: (v3_conlat_1(X0)|~l2_conlat_1(X0)|~l3_conlat_1(X1,X0)|~v6_conlat_1(k8_conlat_2(X0,X1),k7_conlat_2(X0))|~l3_conlat_1(k8_conlat_2(X0,X1),k7_conlat_2(X0))|u5_conlat_1(k7_conlat_2(X0),k8_conlat_2(X0,X1))=u4_conlat_1(X0,X1))),
% 13.71/2.27 inference(destructive_equality_resolution,[status(thm)],[f97])).
% 13.71/2.27 fof(f249,plain,(
% 13.71/2.27 ![X0,X1]: (v3_conlat_1(X0)|~l2_conlat_1(X0)|~l3_conlat_1(X1,X0)|~l3_conlat_1(k8_conlat_2(X0,X1),k7_conlat_2(X0))|u5_conlat_1(k7_conlat_2(X0),k8_conlat_2(X0,X1))=u4_conlat_1(X0,X1))),
% 13.71/2.27 inference(backward_subsumption_resolution,[status(thm)],[f248,f114])).
% 13.71/2.27 fof(f250,plain,(
% 13.71/2.27 ![X0,X1]: (v3_conlat_1(X0)|~l2_conlat_1(X0)|~l3_conlat_1(X1,X0)|~l3_conlat_1(k8_conlat_2(X0,X1),k7_conlat_2(X0))|u4_conlat_1(k7_conlat_2(X0),k8_conlat_2(X0,X1))=u5_conlat_1(X0,X1))),
% 13.71/2.27 inference(backward_subsumption_resolution,[status(thm)],[f247,f114])).
% 13.71/2.27 fof(f251,plain,(
% 13.71/2.27 ![X0,X1]: (v3_conlat_1(X0)|~l2_conlat_1(X0)|~l3_conlat_1(X1,X0)|u5_conlat_1(k7_conlat_2(X0),k8_conlat_2(X0,X1))=u4_conlat_1(X0,X1))),
% 13.71/2.27 inference(forward_subsumption_resolution,[status(thm)],[f249,f115])).
% 13.71/2.27 fof(f252,plain,(
% 13.71/2.27 ![X0,X1]: (v3_conlat_1(X0)|~l2_conlat_1(X0)|~l3_conlat_1(X1,X0)|u4_conlat_1(k7_conlat_2(X0),k8_conlat_2(X0,X1))=u5_conlat_1(X0,X1))),
% 13.71/2.27 inference(forward_subsumption_resolution,[status(thm)],[f250,f115])).
% 13.71/2.27 fof(f255,plain,(
% 13.71/2.27 ![X0]: (~v4_conlat_1(k7_conlat_2(X0))|k7_conlat_2(X0)=g2_conlat_1(u1_conlat_1(k7_conlat_2(X0)),u2_conlat_1(k7_conlat_2(X0)),u3_conlat_1(k7_conlat_2(X0)))|v3_conlat_1(X0)|~l2_conlat_1(X0))),
% 13.71/2.27 inference(resolution,[status(thm)],[f82,f112])).
% 13.71/2.27 fof(f256,plain,(
% 13.71/2.27 ~v4_conlat_1(sK0_skl)|sK0_skl=g2_conlat_1(u1_conlat_1(sK0_skl),u2_conlat_1(sK0_skl),u3_conlat_1(sK0_skl))),
% 13.71/2.27 inference(resolution,[status(thm)],[f82,f75])).
% 13.71/2.27 fof(f258,plain,(
% 13.71/2.27 ![X0]: (k7_conlat_2(X0)=g2_conlat_1(u1_conlat_1(k7_conlat_2(X0)),u2_conlat_1(k7_conlat_2(X0)),u3_conlat_1(k7_conlat_2(X0)))|v3_conlat_1(X0)|~l2_conlat_1(X0))),
% 13.71/2.27 inference(forward_subsumption_resolution,[status(thm)],[f255,f111])).
% 13.71/2.27 fof(f259,plain,(
% 13.71/2.27 sK0_skl=g2_conlat_1(u1_conlat_1(sK0_skl),u2_conlat_1(sK0_skl),u3_conlat_1(sK0_skl))),
% 13.71/2.27 inference(forward_subsumption_resolution,[status(thm)],[f256,f74])).
% 13.71/2.27 fof(f263,plain,(
% 13.71/2.27 k7_conlat_2(sK0_skl)=g2_conlat_1(u1_conlat_1(k7_conlat_2(sK0_skl)),u2_conlat_1(k7_conlat_2(sK0_skl)),u3_conlat_1(k7_conlat_2(sK0_skl)))|v3_conlat_1(sK0_skl)),
% 13.71/2.27 inference(resolution,[status(thm)],[f258,f75])).
% 13.71/2.27 fof(f265,plain,(
% 13.71/2.27 k7_conlat_2(sK0_skl)=g2_conlat_1(u1_conlat_1(k7_conlat_2(sK0_skl)),u2_conlat_1(k7_conlat_2(sK0_skl)),u3_conlat_1(k7_conlat_2(sK0_skl)))),
% 13.71/2.27 inference(forward_subsumption_resolution,[status(thm)],[f263,f73])).
% 13.71/2.27 fof(f270,plain,(
% 13.71/2.27 ![X0,X1]: (v3_conlat_1(k7_conlat_2(X0))|~l2_conlat_1(k7_conlat_2(X0))|v7_conlat_1(k9_conlat_2(X0,X1),k7_conlat_2(X0))|~v9_conlat_1(k9_conlat_2(X0,X1),k7_conlat_2(X0))|k9_conlat_2(k7_conlat_2(X0),k9_conlat_2(X0,X1))=k8_conlat_2(k7_conlat_2(X0),k9_conlat_2(X0,X1))|v3_conlat_1(X0)|~l2_conlat_1(X0)|v7_conlat_1(X1,X0)|~v9_conlat_1(X1,X0)|~l3_conlat_1(X1,X0))),
% 13.71/2.27 inference(resolution,[status(thm)],[f218,f120])).
% 13.71/2.27 fof(f271,plain,(
% 13.71/2.27 v3_conlat_1(sK0_skl)|~l2_conlat_1(sK0_skl)|v7_conlat_1(sK1_skl,sK0_skl)|~v9_conlat_1(sK1_skl,sK0_skl)|k9_conlat_2(sK0_skl,sK1_skl)=k8_conlat_2(sK0_skl,sK1_skl)),
% 13.71/2.27 inference(resolution,[status(thm)],[f218,f79])).
% 13.71/2.27 fof(f272,plain,(
% 13.71/2.27 ![X0,X1]: (~l2_conlat_1(k7_conlat_2(X0))|v7_conlat_1(k9_conlat_2(X0,X1),k7_conlat_2(X0))|~v9_conlat_1(k9_conlat_2(X0,X1),k7_conlat_2(X0))|k9_conlat_2(k7_conlat_2(X0),k9_conlat_2(X0,X1))=k8_conlat_2(k7_conlat_2(X0),k9_conlat_2(X0,X1))|v3_conlat_1(X0)|~l2_conlat_1(X0)|v7_conlat_1(X1,X0)|~v9_conlat_1(X1,X0)|~l3_conlat_1(X1,X0))),
% 13.71/2.27 inference(forward_subsumption_resolution,[status(thm)],[f270,f110])).
% 13.71/2.27 fof(f273,plain,(
% 13.71/2.27 ~l2_conlat_1(sK0_skl)|v7_conlat_1(sK1_skl,sK0_skl)|~v9_conlat_1(sK1_skl,sK0_skl)|k9_conlat_2(sK0_skl,sK1_skl)=k8_conlat_2(sK0_skl,sK1_skl)),
% 13.71/2.27 inference(forward_subsumption_resolution,[status(thm)],[f271,f73])).
% 13.71/2.27 fof(f274,plain,(
% 13.71/2.27 v7_conlat_1(sK1_skl,sK0_skl)|~v9_conlat_1(sK1_skl,sK0_skl)|k9_conlat_2(sK0_skl,sK1_skl)=k8_conlat_2(sK0_skl,sK1_skl)),
% 13.71/2.27 inference(resolution,[status(thm)],[f273,f75])).
% 13.71/2.27 fof(f275,plain,(
% 13.71/2.27 ~v9_conlat_1(sK1_skl,sK0_skl)|k9_conlat_2(sK0_skl,sK1_skl)=k8_conlat_2(sK0_skl,sK1_skl)),
% 13.71/2.27 inference(forward_subsumption_resolution,[status(thm)],[f274,f77])).
% 13.71/2.27 fof(f276,plain,(
% 13.71/2.27 k9_conlat_2(sK0_skl,sK1_skl)=k8_conlat_2(sK0_skl,sK1_skl)),
% 13.71/2.27 inference(resolution,[status(thm)],[f275,f78])).
% 13.71/2.27 fof(f285,plain,(
% 13.71/2.27 ![X0,X1]: (v7_conlat_1(k9_conlat_2(X0,X1),k7_conlat_2(X0))|~v9_conlat_1(k9_conlat_2(X0,X1),k7_conlat_2(X0))|k9_conlat_2(k7_conlat_2(X0),k9_conlat_2(X0,X1))=k8_conlat_2(k7_conlat_2(X0),k9_conlat_2(X0,X1))|v3_conlat_1(X0)|~l2_conlat_1(X0)|v7_conlat_1(X1,X0)|~v9_conlat_1(X1,X0)|~l3_conlat_1(X1,X0)|v3_conlat_1(X0)|~l2_conlat_1(X0))),
% 13.71/2.27 inference(resolution,[status(thm)],[f272,f112])).
% 13.71/2.27 fof(f286,plain,(
% 13.71/2.27 ![X0,X1]: (v7_conlat_1(k9_conlat_2(X0,X1),k7_conlat_2(X0))|~v9_conlat_1(k9_conlat_2(X0,X1),k7_conlat_2(X0))|k9_conlat_2(k7_conlat_2(X0),k9_conlat_2(X0,X1))=k8_conlat_2(k7_conlat_2(X0),k9_conlat_2(X0,X1))|v3_conlat_1(X0)|~l2_conlat_1(X0)|v7_conlat_1(X1,X0)|~v9_conlat_1(X1,X0)|~l3_conlat_1(X1,X0))),
% 13.71/2.27 inference(duplicate_literals_removal,[status(thm)],[f285])).
% 13.71/2.27 fof(f287,plain,(
% 13.71/2.27 ![X0,X1]: (~v9_conlat_1(k9_conlat_2(X0,X1),k7_conlat_2(X0))|k9_conlat_2(k7_conlat_2(X0),k9_conlat_2(X0,X1))=k8_conlat_2(k7_conlat_2(X0),k9_conlat_2(X0,X1))|v3_conlat_1(X0)|~l2_conlat_1(X0)|v7_conlat_1(X1,X0)|~v9_conlat_1(X1,X0)|~l3_conlat_1(X1,X0))),
% 13.71/2.27 inference(forward_subsumption_resolution,[status(thm)],[f286,f118])).
% 13.71/2.27 fof(f310,plain,(
% 13.71/2.27 ![X0,X1]: (k9_conlat_2(k7_conlat_2(X0),k9_conlat_2(X0,X1))=k8_conlat_2(k7_conlat_2(X0),k9_conlat_2(X0,X1))|v3_conlat_1(X0)|~l2_conlat_1(X0)|v7_conlat_1(X1,X0)|~v9_conlat_1(X1,X0)|~l3_conlat_1(X1,X0)|v3_conlat_1(X0)|~l2_conlat_1(X0)|v7_conlat_1(X1,X0)|~v9_conlat_1(X1,X0)|~l3_conlat_1(X1,X0))),
% 13.71/2.27 inference(resolution,[status(thm)],[f287,f119])).
% 13.71/2.27 fof(f311,plain,(
% 13.71/2.27 ![X0,X1]: (k9_conlat_2(k7_conlat_2(X0),k9_conlat_2(X0,X1))=k8_conlat_2(k7_conlat_2(X0),k9_conlat_2(X0,X1))|v3_conlat_1(X0)|~l2_conlat_1(X0)|v7_conlat_1(X1,X0)|~v9_conlat_1(X1,X0)|~l3_conlat_1(X1,X0))),
% 13.71/2.27 inference(duplicate_literals_removal,[status(thm)],[f310])).
% 13.71/2.27 fof(f313,plain,(
% 13.71/2.27 k9_conlat_2(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl))=k8_conlat_2(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl))|v3_conlat_1(sK0_skl)|~l2_conlat_1(sK0_skl)|v7_conlat_1(sK1_skl,sK0_skl)|~v9_conlat_1(sK1_skl,sK0_skl)),
% 13.71/2.27 inference(resolution,[status(thm)],[f311,f79])).
% 13.71/2.27 fof(f315,plain,(
% 13.71/2.27 k9_conlat_2(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl))=k8_conlat_2(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl))|~l2_conlat_1(sK0_skl)|v7_conlat_1(sK1_skl,sK0_skl)|~v9_conlat_1(sK1_skl,sK0_skl)),
% 13.71/2.27 inference(forward_subsumption_resolution,[status(thm)],[f313,f73])).
% 13.71/2.27 fof(f318,plain,(
% 13.71/2.27 ![X0,X1]: (~l2_conlat_1(X0)|~l3_conlat_1(X1,X0)|~v6_conlat_1(X1,X0)|X1=g3_conlat_1(X0,u4_conlat_1(X0,X1),u5_conlat_1(X0,X1)))),
% 13.71/2.27 inference(resolution,[status(thm)],[f122,f84])).
% 13.71/2.27 fof(f346,plain,(
% 13.71/2.27 ![X0]: (v3_conlat_1(k7_conlat_2(X0))|k7_conlat_2(k7_conlat_2(X0))=g2_conlat_1(u2_conlat_1(k7_conlat_2(X0)),u1_conlat_1(k7_conlat_2(X0)),k6_relset_1(u1_conlat_1(k7_conlat_2(X0)),u2_conlat_1(k7_conlat_2(X0)),u3_conlat_1(k7_conlat_2(X0))))|v3_conlat_1(X0)|~l2_conlat_1(X0))),
% 13.71/2.27 inference(resolution,[status(thm)],[f93,f112])).
% 13.71/2.27 fof(f347,plain,(
% 13.71/2.27 v3_conlat_1(sK0_skl)|k7_conlat_2(sK0_skl)=g2_conlat_1(u2_conlat_1(sK0_skl),u1_conlat_1(sK0_skl),k6_relset_1(u1_conlat_1(sK0_skl),u2_conlat_1(sK0_skl),u3_conlat_1(sK0_skl)))),
% 13.71/2.27 inference(resolution,[status(thm)],[f93,f75])).
% 13.71/2.27 fof(f349,plain,(
% 13.71/2.27 ![X0]: (k7_conlat_2(k7_conlat_2(X0))=g2_conlat_1(u2_conlat_1(k7_conlat_2(X0)),u1_conlat_1(k7_conlat_2(X0)),k6_relset_1(u1_conlat_1(k7_conlat_2(X0)),u2_conlat_1(k7_conlat_2(X0)),u3_conlat_1(k7_conlat_2(X0))))|v3_conlat_1(X0)|~l2_conlat_1(X0))),
% 13.71/2.27 inference(forward_subsumption_resolution,[status(thm)],[f346,f110])).
% 13.71/2.27 fof(f350,plain,(
% 13.71/2.27 k7_conlat_2(sK0_skl)=g2_conlat_1(u2_conlat_1(sK0_skl),u1_conlat_1(sK0_skl),k6_relset_1(u1_conlat_1(sK0_skl),u2_conlat_1(sK0_skl),u3_conlat_1(sK0_skl)))),
% 13.71/2.27 inference(forward_subsumption_resolution,[status(thm)],[f347,f73])).
% 13.71/2.27 fof(f352,plain,(
% 13.71/2.27 k9_conlat_2(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl))=k8_conlat_2(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl))|v7_conlat_1(sK1_skl,sK0_skl)|~v9_conlat_1(sK1_skl,sK0_skl)),
% 13.71/2.27 inference(resolution,[status(thm)],[f315,f75])).
% 13.71/2.27 fof(f353,plain,(
% 13.71/2.27 k9_conlat_2(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl))=k8_conlat_2(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl))|~v9_conlat_1(sK1_skl,sK0_skl)),
% 13.71/2.27 inference(forward_subsumption_resolution,[status(thm)],[f352,f77])).
% 13.71/2.27 fof(f354,plain,(
% 13.71/2.27 k9_conlat_2(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl))=k8_conlat_2(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl))),
% 13.71/2.27 inference(resolution,[status(thm)],[f353,f78])).
% 13.71/2.27 fof(f362,plain,(
% 13.71/2.27 k7_conlat_2(k7_conlat_2(sK0_skl))=g2_conlat_1(u2_conlat_1(k7_conlat_2(sK0_skl)),u1_conlat_1(k7_conlat_2(sK0_skl)),k6_relset_1(u1_conlat_1(k7_conlat_2(sK0_skl)),u2_conlat_1(k7_conlat_2(sK0_skl)),u3_conlat_1(k7_conlat_2(sK0_skl))))|v3_conlat_1(sK0_skl)),
% 13.71/2.27 inference(resolution,[status(thm)],[f349,f75])).
% 13.71/2.27 fof(f365,plain,(
% 13.71/2.27 k7_conlat_2(k7_conlat_2(sK0_skl))=g2_conlat_1(u2_conlat_1(k7_conlat_2(sK0_skl)),u1_conlat_1(k7_conlat_2(sK0_skl)),k6_relset_1(u1_conlat_1(k7_conlat_2(sK0_skl)),u2_conlat_1(k7_conlat_2(sK0_skl)),u3_conlat_1(k7_conlat_2(sK0_skl))))),
% 13.71/2.27 inference(forward_subsumption_resolution,[status(thm)],[f362,f73])).
% 13.71/2.27 fof(f408,plain,(
% 13.71/2.27 ![X0,X1,X2]: (~m1_relset_1(X0,X1,X2)|m1_relset_1(k6_relset_1(X1,X2,X0),X2,X1))),
% 13.71/2.27 inference(resolution,[status(thm)],[f108,f221])).
% 13.71/2.27 fof(f467,plain,(
% 13.71/2.27 v3_conlat_1(k7_conlat_2(sK0_skl))|~l2_conlat_1(k7_conlat_2(sK0_skl))|~l3_conlat_1(k9_conlat_2(sK0_skl,sK1_skl),k7_conlat_2(sK0_skl))|v6_conlat_1(k9_conlat_2(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl)),k7_conlat_2(k7_conlat_2(sK0_skl)))),
% 13.71/2.27 inference(paramodulation,[status(thm)],[f354,f114])).
% 13.71/2.27 fof(f472,plain,(
% 13.71/2.27 v3_conlat_1(k7_conlat_2(sK0_skl))|~l2_conlat_1(k7_conlat_2(sK0_skl))|~l3_conlat_1(k9_conlat_2(sK0_skl,sK1_skl),k7_conlat_2(sK0_skl))|l3_conlat_1(k9_conlat_2(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl)),k7_conlat_2(k7_conlat_2(sK0_skl)))),
% 13.71/2.27 inference(paramodulation,[status(thm)],[f354,f115])).
% 13.71/2.27 fof(f473,plain,(
% 13.71/2.27 v3_conlat_1(sK0_skl)|~l2_conlat_1(sK0_skl)|~l3_conlat_1(sK1_skl,sK0_skl)|l3_conlat_1(k9_conlat_2(sK0_skl,sK1_skl),k7_conlat_2(sK0_skl))),
% 13.71/2.27 inference(paramodulation,[status(thm)],[f276,f115])).
% 13.71/2.27 fof(f476,plain,(
% 13.71/2.27 ~l2_conlat_1(sK0_skl)|~l3_conlat_1(sK1_skl,sK0_skl)|l3_conlat_1(k9_conlat_2(sK0_skl,sK1_skl),k7_conlat_2(sK0_skl))),
% 13.71/2.27 inference(forward_subsumption_resolution,[status(thm)],[f473,f73])).
% 13.71/2.27 fof(f477,plain,(
% 13.71/2.27 ![X0,X1,X2]: (~m2_relset_1(X0,X1,X2)|v1_relat_1(X0))),
% 13.71/2.27 inference(resolution,[status(thm)],[f124,f89])).
% 13.71/2.27 fof(f481,plain,(
% 13.71/2.27 ~l3_conlat_1(sK1_skl,sK0_skl)|l3_conlat_1(k9_conlat_2(sK0_skl,sK1_skl),k7_conlat_2(sK0_skl))),
% 13.71/2.27 inference(resolution,[status(thm)],[f476,f75])).
% 13.71/2.27 fof(f482,plain,(
% 13.71/2.27 v3_conlat_1(k7_conlat_2(sK0_skl))|~l2_conlat_1(k7_conlat_2(sK0_skl))|l3_conlat_1(k9_conlat_2(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl)),k7_conlat_2(k7_conlat_2(sK0_skl)))),
% 13.71/2.27 inference(backward_subsumption_resolution,[status(thm)],[f472,f484])).
% 13.71/2.27 fof(f483,plain,(
% 13.71/2.27 v3_conlat_1(k7_conlat_2(sK0_skl))|~l2_conlat_1(k7_conlat_2(sK0_skl))|v6_conlat_1(k9_conlat_2(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl)),k7_conlat_2(k7_conlat_2(sK0_skl)))),
% 13.71/2.27 inference(backward_subsumption_resolution,[status(thm)],[f467,f484])).
% 13.71/2.27 fof(f484,plain,(
% 13.71/2.27 l3_conlat_1(k9_conlat_2(sK0_skl,sK1_skl),k7_conlat_2(sK0_skl))),
% 13.71/2.27 inference(forward_subsumption_resolution,[status(thm)],[f481,f79])).
% 13.71/2.27 fof(f487,plain,(
% 13.71/2.27 v3_conlat_1(k7_conlat_2(sK0_skl))|l3_conlat_1(k9_conlat_2(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl)),k7_conlat_2(k7_conlat_2(sK0_skl)))|v3_conlat_1(sK0_skl)|~l2_conlat_1(sK0_skl)),
% 13.71/2.27 inference(resolution,[status(thm)],[f482,f112])).
% 13.71/2.27 fof(f488,plain,(
% 13.71/2.27 l3_conlat_1(k9_conlat_2(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl)),k7_conlat_2(k7_conlat_2(sK0_skl)))|v3_conlat_1(sK0_skl)|~l2_conlat_1(sK0_skl)),
% 13.71/2.27 inference(forward_subsumption_resolution,[status(thm)],[f487,f110])).
% 13.71/2.27 fof(f489,plain,(
% 13.71/2.27 l3_conlat_1(k9_conlat_2(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl)),k7_conlat_2(k7_conlat_2(sK0_skl)))|v3_conlat_1(sK0_skl)),
% 13.71/2.27 inference(resolution,[status(thm)],[f488,f75])).
% 13.71/2.27 fof(f490,plain,(
% 13.71/2.27 l3_conlat_1(k9_conlat_2(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl)),k7_conlat_2(k7_conlat_2(sK0_skl)))),
% 13.71/2.27 inference(forward_subsumption_resolution,[status(thm)],[f489,f73])).
% 13.71/2.27 fof(f551,plain,(
% 13.71/2.27 ![X0]: (~l2_conlat_1(X0)|v1_relat_1(u3_conlat_1(X0)))),
% 13.71/2.27 inference(resolution,[status(thm)],[f126,f477])).
% 13.71/2.27 fof(f552,plain,(
% 13.71/2.27 ![X0]: (~l2_conlat_1(X0)|m1_relset_1(u3_conlat_1(X0),u1_conlat_1(X0),u2_conlat_1(X0)))),
% 13.71/2.27 inference(resolution,[status(thm)],[f126,f221])).
% 13.71/2.27 fof(f629,plain,(
% 13.71/2.27 ![X0]: (~l2_conlat_1(X0)|k4_relat_1(k4_relat_1(u3_conlat_1(X0)))=u3_conlat_1(X0))),
% 13.71/2.27 inference(resolution,[status(thm)],[f551,f161])).
% 13.71/2.27 fof(f775,plain,(
% 13.71/2.27 k4_relat_1(k4_relat_1(u3_conlat_1(sK0_skl)))=u3_conlat_1(sK0_skl)),
% 13.71/2.27 inference(resolution,[status(thm)],[f629,f75])).
% 13.71/2.27 fof(f919,plain,(
% 13.71/2.27 m1_relset_1(u3_conlat_1(sK0_skl),u1_conlat_1(sK0_skl),u2_conlat_1(sK0_skl))),
% 13.71/2.27 inference(resolution,[status(thm)],[f552,f75])).
% 13.71/2.27 fof(f958,plain,(
% 13.71/2.27 m1_relset_1(k6_relset_1(u1_conlat_1(sK0_skl),u2_conlat_1(sK0_skl),u3_conlat_1(sK0_skl)),u2_conlat_1(sK0_skl),u1_conlat_1(sK0_skl))),
% 13.71/2.27 inference(resolution,[status(thm)],[f919,f408])).
% 13.71/2.27 fof(f962,plain,(
% 13.71/2.27 k6_relset_1(u1_conlat_1(sK0_skl),u2_conlat_1(sK0_skl),u3_conlat_1(sK0_skl))=k4_relat_1(u3_conlat_1(sK0_skl))),
% 13.71/2.27 inference(resolution,[status(thm)],[f919,f216])).
% 13.71/2.27 fof(f969,plain,(
% 13.71/2.27 k7_conlat_2(sK0_skl)=g2_conlat_1(u2_conlat_1(sK0_skl),u1_conlat_1(sK0_skl),k4_relat_1(u3_conlat_1(sK0_skl)))),
% 13.71/2.27 inference(backward_demodulation,[status(thm)],[f962,f350])).
% 13.71/2.27 fof(f970,plain,(
% 13.71/2.27 m1_relset_1(k4_relat_1(u3_conlat_1(sK0_skl)),u2_conlat_1(sK0_skl),u1_conlat_1(sK0_skl))),
% 13.71/2.27 inference(backward_demodulation,[status(thm)],[f962,f958])).
% 13.71/2.27 fof(f1033,plain,(
% 13.71/2.27 ![X0,X1,X2]: (~g2_conlat_1(u2_conlat_1(sK0_skl),u1_conlat_1(sK0_skl),k4_relat_1(u3_conlat_1(sK0_skl)))=g2_conlat_1(X0,X1,X2)|u1_conlat_1(sK0_skl)=X1)),
% 13.71/2.27 inference(resolution,[status(thm)],[f970,f154])).
% 13.71/2.27 fof(f1037,plain,(
% 13.71/2.27 l2_conlat_1(g2_conlat_1(u2_conlat_1(sK0_skl),u1_conlat_1(sK0_skl),k4_relat_1(u3_conlat_1(sK0_skl))))),
% 13.71/2.27 inference(resolution,[status(thm)],[f970,f101])).
% 13.71/2.27 fof(f1039,plain,(
% 13.71/2.27 ![X0,X1,X2]: (~k7_conlat_2(sK0_skl)=g2_conlat_1(X0,X1,X2)|u1_conlat_1(sK0_skl)=X1)),
% 13.71/2.27 inference(forward_demodulation,[status(thm)],[f969,f1033])).
% 13.71/2.27 fof(f1044,plain,(
% 13.71/2.27 v3_conlat_1(k7_conlat_2(sK0_skl))|v6_conlat_1(k9_conlat_2(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl)),k7_conlat_2(k7_conlat_2(sK0_skl)))),
% 13.71/2.27 inference(backward_subsumption_resolution,[status(thm)],[f483,f1051])).
% 13.71/2.27 fof(f1051,plain,(
% 13.71/2.27 l2_conlat_1(k7_conlat_2(sK0_skl))),
% 13.71/2.27 inference(forward_demodulation,[status(thm)],[f969,f1037])).
% 13.71/2.27 fof(f1052,plain,(
% 13.71/2.27 m1_relset_1(u3_conlat_1(k7_conlat_2(sK0_skl)),u1_conlat_1(k7_conlat_2(sK0_skl)),u2_conlat_1(k7_conlat_2(sK0_skl)))),
% 13.71/2.27 inference(resolution,[status(thm)],[f1051,f552])).
% 13.71/2.27 fof(f1073,plain,(
% 13.71/2.27 u1_conlat_1(sK0_skl)=u2_conlat_1(k7_conlat_2(sK0_skl))),
% 13.71/2.27 inference(resolution,[status(thm)],[f1039,f265])).
% 13.71/2.27 fof(f1092,plain,(
% 13.71/2.27 k7_conlat_2(k7_conlat_2(sK0_skl))=g2_conlat_1(u2_conlat_1(k7_conlat_2(sK0_skl)),u1_conlat_1(k7_conlat_2(sK0_skl)),k6_relset_1(u1_conlat_1(k7_conlat_2(sK0_skl)),u1_conlat_1(sK0_skl),u3_conlat_1(k7_conlat_2(sK0_skl))))),
% 13.71/2.27 inference(backward_demodulation,[status(thm)],[f1073,f365])).
% 13.71/2.27 fof(f1093,plain,(
% 13.71/2.27 k7_conlat_2(sK0_skl)=g2_conlat_1(u1_conlat_1(k7_conlat_2(sK0_skl)),u1_conlat_1(sK0_skl),u3_conlat_1(k7_conlat_2(sK0_skl)))),
% 13.71/2.27 inference(backward_demodulation,[status(thm)],[f1073,f265])).
% 13.71/2.27 fof(f1094,plain,(
% 13.71/2.27 m1_relset_1(u3_conlat_1(k7_conlat_2(sK0_skl)),u1_conlat_1(k7_conlat_2(sK0_skl)),u1_conlat_1(sK0_skl))),
% 13.71/2.27 inference(backward_demodulation,[status(thm)],[f1073,f1052])).
% 13.71/2.27 fof(f1099,plain,(
% 13.71/2.27 k7_conlat_2(k7_conlat_2(sK0_skl))=g2_conlat_1(u1_conlat_1(sK0_skl),u1_conlat_1(k7_conlat_2(sK0_skl)),k6_relset_1(u1_conlat_1(k7_conlat_2(sK0_skl)),u1_conlat_1(sK0_skl),u3_conlat_1(k7_conlat_2(sK0_skl))))),
% 13.71/2.27 inference(forward_demodulation,[status(thm)],[f1073,f1092])).
% 13.71/2.27 fof(f1294,plain,(
% 13.71/2.27 ![X0,X1]: (v3_conlat_1(k7_conlat_2(X0))|~l3_conlat_1(X1,k7_conlat_2(X0))|u5_conlat_1(k7_conlat_2(k7_conlat_2(X0)),k8_conlat_2(k7_conlat_2(X0),X1))=u4_conlat_1(k7_conlat_2(X0),X1)|v3_conlat_1(X0)|~l2_conlat_1(X0))),
% 13.71/2.27 inference(resolution,[status(thm)],[f251,f112])).
% 13.71/2.27 fof(f1295,plain,(
% 13.71/2.27 ![X0]: (v3_conlat_1(sK0_skl)|~l3_conlat_1(X0,sK0_skl)|u5_conlat_1(k7_conlat_2(sK0_skl),k8_conlat_2(sK0_skl,X0))=u4_conlat_1(sK0_skl,X0))),
% 13.71/2.27 inference(resolution,[status(thm)],[f251,f75])).
% 13.71/2.27 fof(f1297,plain,(
% 13.71/2.27 ![X0,X1]: (~l3_conlat_1(X0,k7_conlat_2(X1))|u5_conlat_1(k7_conlat_2(k7_conlat_2(X1)),k8_conlat_2(k7_conlat_2(X1),X0))=u4_conlat_1(k7_conlat_2(X1),X0)|v3_conlat_1(X1)|~l2_conlat_1(X1))),
% 13.71/2.27 inference(forward_subsumption_resolution,[status(thm)],[f1294,f110])).
% 13.71/2.27 fof(f1298,plain,(
% 13.71/2.27 ![X0]: (~l3_conlat_1(X0,sK0_skl)|u5_conlat_1(k7_conlat_2(sK0_skl),k8_conlat_2(sK0_skl,X0))=u4_conlat_1(sK0_skl,X0))),
% 13.71/2.27 inference(forward_subsumption_resolution,[status(thm)],[f1295,f73])).
% 13.71/2.27 fof(f1307,plain,(
% 13.71/2.27 ![X0,X1]: (v3_conlat_1(k7_conlat_2(X0))|~l3_conlat_1(X1,k7_conlat_2(X0))|u4_conlat_1(k7_conlat_2(k7_conlat_2(X0)),k8_conlat_2(k7_conlat_2(X0),X1))=u5_conlat_1(k7_conlat_2(X0),X1)|v3_conlat_1(X0)|~l2_conlat_1(X0))),
% 13.71/2.27 inference(resolution,[status(thm)],[f252,f112])).
% 13.71/2.27 fof(f1308,plain,(
% 13.71/2.27 ![X0]: (v3_conlat_1(sK0_skl)|~l3_conlat_1(X0,sK0_skl)|u4_conlat_1(k7_conlat_2(sK0_skl),k8_conlat_2(sK0_skl,X0))=u5_conlat_1(sK0_skl,X0))),
% 13.71/2.27 inference(resolution,[status(thm)],[f252,f75])).
% 13.71/2.27 fof(f1310,plain,(
% 13.71/2.27 ![X0,X1]: (~l3_conlat_1(X0,k7_conlat_2(X1))|u4_conlat_1(k7_conlat_2(k7_conlat_2(X1)),k8_conlat_2(k7_conlat_2(X1),X0))=u5_conlat_1(k7_conlat_2(X1),X0)|v3_conlat_1(X1)|~l2_conlat_1(X1))),
% 13.71/2.27 inference(forward_subsumption_resolution,[status(thm)],[f1307,f110])).
% 13.71/2.27 fof(f1311,plain,(
% 13.71/2.27 ![X0]: (~l3_conlat_1(X0,sK0_skl)|u4_conlat_1(k7_conlat_2(sK0_skl),k8_conlat_2(sK0_skl,X0))=u5_conlat_1(sK0_skl,X0))),
% 13.71/2.27 inference(forward_subsumption_resolution,[status(thm)],[f1308,f73])).
% 13.71/2.27 fof(f1333,plain,(
% 13.71/2.27 u5_conlat_1(k7_conlat_2(sK0_skl),k8_conlat_2(sK0_skl,sK1_skl))=u4_conlat_1(sK0_skl,sK1_skl)),
% 13.71/2.27 inference(resolution,[status(thm)],[f1298,f79])).
% 13.71/2.27 fof(f1340,plain,(
% 13.71/2.27 u5_conlat_1(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl))=u4_conlat_1(sK0_skl,sK1_skl)),
% 13.71/2.27 inference(forward_demodulation,[status(thm)],[f276,f1333])).
% 13.71/2.27 fof(f1368,plain,(
% 13.71/2.27 ![X0]: (~l3_conlat_1(X0,k7_conlat_2(sK0_skl))|u5_conlat_1(k7_conlat_2(k7_conlat_2(sK0_skl)),k8_conlat_2(k7_conlat_2(sK0_skl),X0))=u4_conlat_1(k7_conlat_2(sK0_skl),X0)|v3_conlat_1(sK0_skl))),
% 13.71/2.27 inference(resolution,[status(thm)],[f1297,f75])).
% 13.71/2.27 fof(f1371,plain,(
% 13.71/2.27 ![X0]: (~l3_conlat_1(X0,k7_conlat_2(sK0_skl))|u5_conlat_1(k7_conlat_2(k7_conlat_2(sK0_skl)),k8_conlat_2(k7_conlat_2(sK0_skl),X0))=u4_conlat_1(k7_conlat_2(sK0_skl),X0))),
% 13.71/2.27 inference(forward_subsumption_resolution,[status(thm)],[f1368,f73])).
% 13.71/2.27 fof(f1381,plain,(
% 13.71/2.27 ![X0]: (~l3_conlat_1(X0,k7_conlat_2(sK0_skl))|u4_conlat_1(k7_conlat_2(k7_conlat_2(sK0_skl)),k8_conlat_2(k7_conlat_2(sK0_skl),X0))=u5_conlat_1(k7_conlat_2(sK0_skl),X0)|v3_conlat_1(sK0_skl))),
% 13.71/2.27 inference(resolution,[status(thm)],[f1310,f75])).
% 13.71/2.27 fof(f1384,plain,(
% 13.71/2.27 ![X0]: (~l3_conlat_1(X0,k7_conlat_2(sK0_skl))|u4_conlat_1(k7_conlat_2(k7_conlat_2(sK0_skl)),k8_conlat_2(k7_conlat_2(sK0_skl),X0))=u5_conlat_1(k7_conlat_2(sK0_skl),X0))),
% 13.71/2.27 inference(forward_subsumption_resolution,[status(thm)],[f1381,f73])).
% 13.71/2.27 fof(f1462,plain,(
% 13.71/2.27 ![X0,X1,X2]: (~g2_conlat_1(u1_conlat_1(k7_conlat_2(sK0_skl)),u1_conlat_1(sK0_skl),u3_conlat_1(k7_conlat_2(sK0_skl)))=g2_conlat_1(X0,X1,X2)|u3_conlat_1(k7_conlat_2(sK0_skl))=X2)),
% 13.71/2.27 inference(resolution,[status(thm)],[f1094,f155])).
% 13.71/2.27 fof(f1464,plain,(
% 13.71/2.27 ![X0,X1,X2]: (~g2_conlat_1(u1_conlat_1(k7_conlat_2(sK0_skl)),u1_conlat_1(sK0_skl),u3_conlat_1(k7_conlat_2(sK0_skl)))=g2_conlat_1(X0,X1,X2)|u1_conlat_1(k7_conlat_2(sK0_skl))=X0)),
% 13.71/2.27 inference(resolution,[status(thm)],[f1094,f153])).
% 13.71/2.27 fof(f1465,plain,(
% 13.71/2.27 k6_relset_1(u1_conlat_1(k7_conlat_2(sK0_skl)),u1_conlat_1(sK0_skl),u3_conlat_1(k7_conlat_2(sK0_skl)))=k4_relat_1(u3_conlat_1(k7_conlat_2(sK0_skl)))),
% 13.71/2.27 inference(resolution,[status(thm)],[f1094,f216])).
% 13.71/2.27 fof(f1469,plain,(
% 13.71/2.27 ![X0,X1,X2]: (~k7_conlat_2(sK0_skl)=g2_conlat_1(X0,X1,X2)|u3_conlat_1(k7_conlat_2(sK0_skl))=X2)),
% 13.71/2.29 inference(forward_demodulation,[status(thm)],[f1093,f1462])).
% 13.71/2.29 fof(f1471,plain,(
% 13.71/2.29 ![X0,X1,X2]: (~k7_conlat_2(sK0_skl)=g2_conlat_1(X0,X1,X2)|u1_conlat_1(k7_conlat_2(sK0_skl))=X0)),
% 13.71/2.29 inference(forward_demodulation,[status(thm)],[f1093,f1464])).
% 13.71/2.29 fof(f1472,plain,(
% 13.71/2.29 k7_conlat_2(k7_conlat_2(sK0_skl))=g2_conlat_1(u1_conlat_1(sK0_skl),u1_conlat_1(k7_conlat_2(sK0_skl)),k4_relat_1(u3_conlat_1(k7_conlat_2(sK0_skl))))),
% 13.71/2.29 inference(backward_demodulation,[status(thm)],[f1465,f1099])).
% 13.71/2.29 fof(f1486,plain,(
% 13.71/2.29 u4_conlat_1(k7_conlat_2(sK0_skl),k8_conlat_2(sK0_skl,sK1_skl))=u5_conlat_1(sK0_skl,sK1_skl)),
% 13.71/2.29 inference(resolution,[status(thm)],[f1311,f79])).
% 13.71/2.29 fof(f1493,plain,(
% 13.71/2.29 u4_conlat_1(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl))=u5_conlat_1(sK0_skl,sK1_skl)),
% 13.71/2.29 inference(forward_demodulation,[status(thm)],[f276,f1486])).
% 13.71/2.29 fof(f1496,plain,(
% 13.71/2.29 u3_conlat_1(k7_conlat_2(sK0_skl))=k4_relat_1(u3_conlat_1(sK0_skl))),
% 13.71/2.29 inference(resolution,[status(thm)],[f1469,f969])).
% 13.71/2.29 fof(f1520,plain,(
% 13.71/2.29 k7_conlat_2(sK0_skl)=g2_conlat_1(u2_conlat_1(sK0_skl),u1_conlat_1(sK0_skl),u3_conlat_1(k7_conlat_2(sK0_skl)))),
% 13.71/2.29 inference(backward_demodulation,[status(thm)],[f1496,f969])).
% 13.71/2.29 fof(f1521,plain,(
% 13.71/2.29 k4_relat_1(u3_conlat_1(k7_conlat_2(sK0_skl)))=u3_conlat_1(sK0_skl)),
% 13.71/2.29 inference(backward_demodulation,[status(thm)],[f1496,f775])).
% 13.71/2.29 fof(f1547,plain,(
% 13.71/2.29 k7_conlat_2(k7_conlat_2(sK0_skl))=g2_conlat_1(u1_conlat_1(sK0_skl),u1_conlat_1(k7_conlat_2(sK0_skl)),u3_conlat_1(sK0_skl))),
% 13.71/2.29 inference(backward_demodulation,[status(thm)],[f1521,f1472])).
% 13.71/2.29 fof(f1609,plain,(
% 13.71/2.29 u1_conlat_1(k7_conlat_2(sK0_skl))=u2_conlat_1(sK0_skl)),
% 13.71/2.29 inference(resolution,[status(thm)],[f1520,f1471])).
% 13.71/2.29 fof(f1652,plain,(
% 13.71/2.29 k7_conlat_2(k7_conlat_2(sK0_skl))=g2_conlat_1(u1_conlat_1(sK0_skl),u2_conlat_1(sK0_skl),u3_conlat_1(sK0_skl))),
% 13.71/2.29 inference(backward_demodulation,[status(thm)],[f1609,f1547])).
% 13.71/2.29 fof(f1676,plain,(
% 13.71/2.29 l3_conlat_1(k9_conlat_2(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl)),sK0_skl)),
% 13.71/2.29 inference(backward_demodulation,[status(thm)],[f1793,f490])).
% 13.71/2.29 fof(f1703,plain,(
% 13.71/2.29 ![X0]: (~l3_conlat_1(X0,k7_conlat_2(sK0_skl))|u4_conlat_1(sK0_skl,k8_conlat_2(k7_conlat_2(sK0_skl),X0))=u5_conlat_1(k7_conlat_2(sK0_skl),X0))),
% 13.71/2.29 inference(backward_demodulation,[status(thm)],[f1793,f1384])).
% 13.71/2.29 fof(f1705,plain,(
% 13.71/2.29 ![X0]: (~l3_conlat_1(X0,k7_conlat_2(sK0_skl))|u5_conlat_1(sK0_skl,k8_conlat_2(k7_conlat_2(sK0_skl),X0))=u4_conlat_1(k7_conlat_2(sK0_skl),X0))),
% 13.71/2.29 inference(backward_demodulation,[status(thm)],[f1793,f1371])).
% 13.71/2.29 fof(f1768,plain,(
% 13.71/2.29 v3_conlat_1(k7_conlat_2(sK0_skl))|v6_conlat_1(k9_conlat_2(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl)),sK0_skl)),
% 13.71/2.29 inference(backward_demodulation,[status(thm)],[f1793,f1044])).
% 13.71/2.29 fof(f1793,plain,(
% 13.71/2.29 k7_conlat_2(k7_conlat_2(sK0_skl))=sK0_skl),
% 13.71/2.29 inference(forward_demodulation,[status(thm)],[f259,f1652])).
% 13.71/2.29 fof(f2315,plain,(
% 13.71/2.29 ~l2_conlat_1(sK0_skl)|~l3_conlat_1(sK1_skl,sK0_skl)|sK1_skl=g3_conlat_1(sK0_skl,u4_conlat_1(sK0_skl,sK1_skl),u5_conlat_1(sK0_skl,sK1_skl))),
% 13.71/2.29 inference(resolution,[status(thm)],[f318,f76])).
% 13.71/2.29 fof(f2327,plain,(
% 13.71/2.29 ~l3_conlat_1(sK1_skl,sK0_skl)|sK1_skl=g3_conlat_1(sK0_skl,u4_conlat_1(sK0_skl,sK1_skl),u5_conlat_1(sK0_skl,sK1_skl))),
% 13.71/2.29 inference(forward_subsumption_resolution,[status(thm)],[f2315,f75])).
% 13.71/2.29 fof(f2338,plain,(
% 13.71/2.29 sK1_skl=g3_conlat_1(sK0_skl,u4_conlat_1(sK0_skl,sK1_skl),u5_conlat_1(sK0_skl,sK1_skl))),
% 13.71/2.29 inference(resolution,[status(thm)],[f2327,f79])).
% 13.71/2.29 fof(f4204,plain,(
% 13.71/2.29 u4_conlat_1(sK0_skl,k8_conlat_2(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl)))=u5_conlat_1(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl))),
% 13.71/2.29 inference(resolution,[status(thm)],[f1703,f484])).
% 13.71/2.29 fof(f4216,plain,(
% 13.71/2.29 u4_conlat_1(sK0_skl,k9_conlat_2(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl)))=u5_conlat_1(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl))),
% 13.71/2.29 inference(forward_demodulation,[status(thm)],[f354,f4204])).
% 13.71/2.29 fof(f4218,plain,(
% 13.71/2.29 u4_conlat_1(sK0_skl,k9_conlat_2(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl)))=u4_conlat_1(sK0_skl,sK1_skl)),
% 13.71/2.29 inference(forward_demodulation,[status(thm)],[f1340,f4216])).
% 13.71/2.29 fof(f4291,plain,(
% 13.71/2.29 u5_conlat_1(sK0_skl,k8_conlat_2(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl)))=u4_conlat_1(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl))),
% 13.71/2.29 inference(resolution,[status(thm)],[f1705,f484])).
% 13.71/2.29 fof(f4303,plain,(
% 13.71/2.29 u5_conlat_1(sK0_skl,k9_conlat_2(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl)))=u4_conlat_1(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl))),
% 13.71/2.29 inference(forward_demodulation,[status(thm)],[f354,f4291])).
% 13.71/2.29 fof(f4305,plain,(
% 13.71/2.29 u5_conlat_1(sK0_skl,k9_conlat_2(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl)))=u5_conlat_1(sK0_skl,sK1_skl)),
% 13.71/2.29 inference(forward_demodulation,[status(thm)],[f1493,f4303])).
% 13.71/2.29 fof(f4453,plain,(
% 13.71/2.29 v3_conlat_1(k7_conlat_2(sK0_skl))|~l2_conlat_1(sK0_skl)|~l3_conlat_1(k9_conlat_2(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl)),sK0_skl)|k9_conlat_2(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl))=g3_conlat_1(sK0_skl,u4_conlat_1(sK0_skl,k9_conlat_2(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl))),u5_conlat_1(sK0_skl,k9_conlat_2(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl))))),
% 8.32/2.33 inference(resolution,[status(thm)],[f1768,f318])).
% 8.32/2.33 fof(f4454,plain,(
% 8.32/2.33 v3_conlat_1(k7_conlat_2(sK0_skl))|~l2_conlat_1(sK0_skl)|~l3_conlat_1(k9_conlat_2(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl)),sK0_skl)|k9_conlat_2(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl))=g3_conlat_1(sK0_skl,u4_conlat_1(sK0_skl,sK1_skl),u5_conlat_1(sK0_skl,k9_conlat_2(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl))))),
% 8.32/2.33 inference(forward_demodulation,[status(thm)],[f4218,f4453])).
% 8.32/2.33 fof(f4455,plain,(
% 8.32/2.33 v3_conlat_1(k7_conlat_2(sK0_skl))|~l2_conlat_1(sK0_skl)|~l3_conlat_1(k9_conlat_2(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl)),sK0_skl)|k9_conlat_2(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl))=g3_conlat_1(sK0_skl,u4_conlat_1(sK0_skl,sK1_skl),u5_conlat_1(sK0_skl,sK1_skl))),
% 8.32/2.33 inference(forward_demodulation,[status(thm)],[f4305,f4454])).
% 8.32/2.33 fof(f4456,plain,(
% 8.32/2.33 v3_conlat_1(k7_conlat_2(sK0_skl))|~l2_conlat_1(sK0_skl)|~l3_conlat_1(k9_conlat_2(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl)),sK0_skl)|k9_conlat_2(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl))=sK1_skl),
% 8.32/2.33 inference(forward_demodulation,[status(thm)],[f2338,f4455])).
% 8.32/2.33 fof(f4457,plain,(
% 8.32/2.33 v3_conlat_1(k7_conlat_2(sK0_skl))|~l3_conlat_1(k9_conlat_2(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl)),sK0_skl)|k9_conlat_2(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl))=sK1_skl),
% 8.32/2.33 inference(forward_subsumption_resolution,[status(thm)],[f4456,f75])).
% 8.32/2.33 fof(f4458,plain,(
% 8.32/2.33 v3_conlat_1(k7_conlat_2(sK0_skl))|k9_conlat_2(k7_conlat_2(sK0_skl),k9_conlat_2(sK0_skl,sK1_skl))=sK1_skl),
% 8.32/2.33 inference(resolution,[status(thm)],[f4457,f1676])).
% 8.32/2.33 fof(f4459,plain,(
% 8.32/2.33 v3_conlat_1(k7_conlat_2(sK0_skl))),
% 8.32/2.33 inference(forward_subsumption_resolution,[status(thm)],[f4458,f80])).
% 8.32/2.33 fof(f4460,plain,(
% 8.32/2.33 v3_conlat_1(sK0_skl)|~l2_conlat_1(sK0_skl)),
% 8.32/2.33 inference(resolution,[status(thm)],[f4459,f110])).
% 8.32/2.33 fof(f4463,plain,(
% 8.32/2.33 ~l2_conlat_1(sK0_skl)),
% 8.32/2.33 inference(forward_subsumption_resolution,[status(thm)],[f4460,f73])).
% 8.32/2.33 fof(f4464,plain,(
% 8.32/2.33 $false),
% 8.32/2.33 inference(backward_subsumption_resolution,[status(thm)],[f75,f4463])).
% 8.32/2.33 % SZS output end CNFRefutation for theBenchmark.p
% 8.32/2.35 % Elapsed time: 1.888292 seconds
% 8.32/2.35 % CPU time: 14.577326 seconds
% 8.32/2.35 % Total memory used: 249.564 MB
% 8.32/2.35 % Net memory used: 244.360 MB
%------------------------------------------------------------------------------