%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LAT376+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 : n006.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:55 PM UTC 2026
% Result : Theorem 0.70s 0.97s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LAT376+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.17/0.42 % Computer : n006.cluster.edu
% 0.17/0.42 % Model : x86_64 x86_64
% 0.17/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.42 % Memory : 8046.5625MB
% 0.17/0.42 % OS : Linux 6.8.0-71-generic
% 0.17/0.42 % CPULimit : 300
% 0.17/0.42 % WCLimit : 300
% 0.17/0.42 % DateTime : Sun Sep 20 23:55:15 UTC 2026
% 0.17/0.42 % CPUTime :
% 0.17/0.44 % Drodi V4.1.1
% 0.70/0.97 % Refutation found
% 0.70/0.97 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.70/0.97 % SZS output start CNFRefutation for theBenchmark
% 0.70/0.97 fof(f1,conjecture,(
% 0.70/0.97 (! [A] :( ~ v2_setfam_1(A)=> r3_yellow20(k5_waybel34(A),k4_waybel34(A),k7_waybel34(A),k9_waybel34(A),k8_waybel34(A)) ) )),
% 0.70/0.97 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.70/0.97 fof(f2,negated_conjecture,(
% 0.70/0.97 ~((! [A] :( ~ v2_setfam_1(A)=> r3_yellow20(k5_waybel34(A),k4_waybel34(A),k7_waybel34(A),k9_waybel34(A),k8_waybel34(A)) ) ))),
% 0.70/0.97 inference(negated_conjecture,[status(cth)],[f1])).
% 0.70/0.97 fof(f29,axiom,(
% 0.70/0.97 (! [A] :( ~ v2_setfam_1(A)=> ~ v1_xboole_0(A) ) )),
% 0.70/0.97 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.70/0.97 fof(f51,axiom,(
% 0.70/0.97 (! [A] :( ~ v1_xboole_0(A)=> ( ~ v3_struct_0(k4_waybel34(A))& v2_altcat_1(k4_waybel34(A))& v6_altcat_1(k4_waybel34(A))& v11_altcat_1(k4_waybel34(A))& v12_altcat_1(k4_waybel34(A))& v2_yellow21(k4_waybel34(A))& l2_altcat_1(k4_waybel34(A)) ) ) )),
% 0.70/0.97 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.70/0.97 fof(f52,axiom,(
% 0.70/0.97 (! [A] :( ~ v1_xboole_0(A)=> ( ~ v3_struct_0(k5_waybel34(A))& v2_altcat_1(k5_waybel34(A))& v6_altcat_1(k5_waybel34(A))& v11_altcat_1(k5_waybel34(A))& v12_altcat_1(k5_waybel34(A))& v2_yellow21(k5_waybel34(A))& l2_altcat_1(k5_waybel34(A)) ) ) )),
% 0.70/0.97 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.70/0.97 fof(f53,axiom,(
% 0.70/0.97 (! [A] :( ~ v2_setfam_1(A)=> ( v9_functor0(k6_waybel34(A),k4_waybel34(A),k5_waybel34(A))& v16_functor0(k6_waybel34(A),k4_waybel34(A),k5_waybel34(A))& m2_functor0(k6_waybel34(A),k4_waybel34(A),k5_waybel34(A)) ) ) )),
% 0.70/0.97 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.70/0.97 fof(f55,axiom,(
% 0.70/0.97 (! [A] :( ~ v1_xboole_0(A)=> ( ~ v3_struct_0(k8_waybel34(A))& v2_altcat_1(k8_waybel34(A))& v6_altcat_1(k8_waybel34(A))& v3_altcat_2(k8_waybel34(A),k4_waybel34(A))& m1_altcat_2(k8_waybel34(A),k4_waybel34(A)) ) ) )),
% 0.70/0.97 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.70/0.97 fof(f56,axiom,(
% 0.70/0.97 (! [A] :( ~ v2_setfam_1(A)=> ( ~ v3_struct_0(k9_waybel34(A))& v2_altcat_1(k9_waybel34(A))& v6_altcat_1(k9_waybel34(A))& v3_altcat_2(k9_waybel34(A),k5_waybel34(A))& m1_altcat_2(k9_waybel34(A),k5_waybel34(A)) ) ) )),
% 0.70/0.97 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.70/0.97 fof(f91,axiom,(
% 0.70/0.97 (! [A] :( ~ v2_setfam_1(A)=> ( ~ v3_struct_0(k4_waybel34(A))& v2_altcat_1(k4_waybel34(A))& v6_altcat_1(k4_waybel34(A))& v9_altcat_1(k4_waybel34(A))& v11_altcat_1(k4_waybel34(A))& v12_altcat_1(k4_waybel34(A))& v1_altcat_2(k4_waybel34(A))& v2_yellow18(k4_waybel34(A))& v3_yellow18(k4_waybel34(A))& v4_yellow18(k4_waybel34(A))& v1_yellow21(k4_waybel34(A))& v2_yellow21(k4_waybel34(A))& v3_yellow21(k4_waybel34(A)) ) ) )),
% 0.70/0.97 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.70/0.97 fof(f93,axiom,(
% 0.70/0.97 (! [A] :( ~ v2_setfam_1(A)=> ( ~ v3_struct_0(k5_waybel34(A))& v2_altcat_1(k5_waybel34(A))& v6_altcat_1(k5_waybel34(A))& v9_altcat_1(k5_waybel34(A))& v11_altcat_1(k5_waybel34(A))& v12_altcat_1(k5_waybel34(A))& v1_altcat_2(k5_waybel34(A))& v2_yellow18(k5_waybel34(A))& v3_yellow18(k5_waybel34(A))& v4_yellow18(k5_waybel34(A))& v1_yellow21(k5_waybel34(A))& v2_yellow21(k5_waybel34(A))& v3_yellow21(k5_waybel34(A)) ) ) )),
% 0.70/0.97 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.70/0.97 fof(f95,axiom,(
% 0.70/0.97 (! [A] :( ~ v2_setfam_1(A)=> ( v6_functor0(k6_waybel34(A),k4_waybel34(A),k5_waybel34(A))& v8_functor0(k6_waybel34(A),k4_waybel34(A),k5_waybel34(A))& v9_functor0(k6_waybel34(A),k4_waybel34(A),k5_waybel34(A))& v11_functor0(k6_waybel34(A),k4_waybel34(A),k5_waybel34(A))& v12_functor0(k6_waybel34(A),k4_waybel34(A),k5_waybel34(A))& v14_functor0(k6_waybel34(A),k4_waybel34(A),k5_waybel34(A))& v16_functor0(k6_waybel34(A),k4_waybel34(A),k5_waybel34(A))& v21_functor0(k6_waybel34(A),k4_waybel34(A),k5_waybel34(A)) ) ) )),
% 0.70/0.97 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.70/0.97 fof(f118,axiom,(
% 0.70/0.97 (! [A] :( ~ v2_setfam_1(A)=> ( k15_functor0(k4_waybel34(A),k5_waybel34(A),k6_waybel34(A)) = k7_waybel34(A)& k15_functor0(k5_waybel34(A),k4_waybel34(A),k7_waybel34(A)) = k6_waybel34(A) ) ) )),
% 0.70/0.97 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.70/0.97 fof(f123,axiom,(
% 0.70/0.97 (! [A] :( ( ~ v3_struct_0(A)& v2_altcat_1(A)& v11_altcat_1(A)& v12_altcat_1(A)& l2_altcat_1(A) )=> (! [B] :( ( ~ v3_struct_0(B)& v2_altcat_1(B)& v11_altcat_1(B)& v12_altcat_1(B)& l2_altcat_1(B) )=> (! [C] :( ( v16_functor0(C,A,B)& m2_functor0(C,A,B) )=> ( v21_functor0(C,A,B)=> (! [D] :( ( ~ v3_struct_0(D)& v2_altcat_1(D)& v3_altcat_2(D,A)& m1_altcat_2(D,A) )=> (! [E] :( ( ~ v3_struct_0(E)& v2_altcat_1(E)& v3_altcat_2(E,B)& m1_altcat_2(E,B) )=> ( r3_yellow20(A,B,C,D,E)=> r3_yellow20(B,A,k15_functor0(A,B,C),E,D) ) ) )) )) ) )) )) )),
% 0.70/0.97 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.70/0.97 fof(f124,axiom,(
% 0.70/0.97 (! [A] :( ~ v2_setfam_1(A)=> r3_yellow20(k4_waybel34(A),k5_waybel34(A),k6_waybel34(A),k8_waybel34(A),k9_waybel34(A)) ) )),
% 0.70/0.97 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.70/0.97 fof(f129,plain,(
% 0.70/0.97 (?[A]: (~v2_setfam_1(A)&~r3_yellow20(k5_waybel34(A),k4_waybel34(A),k7_waybel34(A),k9_waybel34(A),k8_waybel34(A))))),
% 0.70/0.97 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.70/0.97 fof(f130,plain,(
% 0.70/0.97 (~v2_setfam_1(sK0_skl)&~r3_yellow20(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl),k9_waybel34(sK0_skl),k8_waybel34(sK0_skl)))),
% 0.70/0.97 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl]),skolemize(A,sK0_skl)],[f129])).
% 0.70/0.97 fof(f131,plain,(
% 0.70/0.97 ~v2_setfam_1(sK0_skl)),
% 0.70/0.97 inference(cnf_transformation,[status(thm)],[f130])).
% 0.70/0.97 fof(f132,plain,(
% 0.70/0.97 ~r3_yellow20(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl),k9_waybel34(sK0_skl),k8_waybel34(sK0_skl))),
% 0.70/0.97 inference(cnf_transformation,[status(thm)],[f130])).
% 0.70/0.97 fof(f231,plain,(
% 0.70/0.97 ![A]: (v2_setfam_1(A)|~v1_xboole_0(A))),
% 0.70/0.97 inference(pre_NNF_transformation,[status(thm)],[f29])).
% 0.70/0.97 fof(f232,plain,(
% 0.70/0.97 ![X0]: (v2_setfam_1(X0)|~v1_xboole_0(X0))),
% 0.70/0.97 inference(cnf_transformation,[status(thm)],[f231])).
% 0.70/0.97 fof(f318,plain,(
% 0.70/0.97 ![A]: (v1_xboole_0(A)|((((((~v3_struct_0(k4_waybel34(A))&v2_altcat_1(k4_waybel34(A)))&v6_altcat_1(k4_waybel34(A)))&v11_altcat_1(k4_waybel34(A)))&v12_altcat_1(k4_waybel34(A)))&v2_yellow21(k4_waybel34(A)))&l2_altcat_1(k4_waybel34(A))))),
% 0.70/0.97 inference(pre_NNF_transformation,[status(thm)],[f51])).
% 0.70/0.97 fof(f325,plain,(
% 0.70/0.97 ![X0]: (v1_xboole_0(X0)|l2_altcat_1(k4_waybel34(X0)))),
% 0.70/0.97 inference(cnf_transformation,[status(thm)],[f318])).
% 0.70/0.97 fof(f326,plain,(
% 0.70/0.97 ![A]: (v1_xboole_0(A)|((((((~v3_struct_0(k5_waybel34(A))&v2_altcat_1(k5_waybel34(A)))&v6_altcat_1(k5_waybel34(A)))&v11_altcat_1(k5_waybel34(A)))&v12_altcat_1(k5_waybel34(A)))&v2_yellow21(k5_waybel34(A)))&l2_altcat_1(k5_waybel34(A))))),
% 0.70/0.97 inference(pre_NNF_transformation,[status(thm)],[f52])).
% 0.70/0.97 fof(f333,plain,(
% 0.70/0.97 ![X0]: (v1_xboole_0(X0)|l2_altcat_1(k5_waybel34(X0)))),
% 0.70/0.97 inference(cnf_transformation,[status(thm)],[f326])).
% 0.70/0.97 fof(f334,plain,(
% 0.70/0.97 ![A]: (v2_setfam_1(A)|((v9_functor0(k6_waybel34(A),k4_waybel34(A),k5_waybel34(A))&v16_functor0(k6_waybel34(A),k4_waybel34(A),k5_waybel34(A)))&m2_functor0(k6_waybel34(A),k4_waybel34(A),k5_waybel34(A))))),
% 0.70/0.97 inference(pre_NNF_transformation,[status(thm)],[f53])).
% 0.70/0.97 fof(f336,plain,(
% 0.70/0.97 ![X0]: (v2_setfam_1(X0)|v16_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0)))),
% 0.70/0.97 inference(cnf_transformation,[status(thm)],[f334])).
% 0.70/0.97 fof(f337,plain,(
% 0.70/0.97 ![X0]: (v2_setfam_1(X0)|m2_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0)))),
% 0.70/0.97 inference(cnf_transformation,[status(thm)],[f334])).
% 0.70/0.97 fof(f342,plain,(
% 0.70/0.97 ![A]: (v1_xboole_0(A)|((((~v3_struct_0(k8_waybel34(A))&v2_altcat_1(k8_waybel34(A)))&v6_altcat_1(k8_waybel34(A)))&v3_altcat_2(k8_waybel34(A),k4_waybel34(A)))&m1_altcat_2(k8_waybel34(A),k4_waybel34(A))))),
% 0.70/0.97 inference(pre_NNF_transformation,[status(thm)],[f55])).
% 0.70/0.97 fof(f343,plain,(
% 0.70/0.97 ![X0]: (v1_xboole_0(X0)|~v3_struct_0(k8_waybel34(X0)))),
% 0.70/0.97 inference(cnf_transformation,[status(thm)],[f342])).
% 0.70/0.97 fof(f344,plain,(
% 0.70/0.97 ![X0]: (v1_xboole_0(X0)|v2_altcat_1(k8_waybel34(X0)))),
% 0.70/0.97 inference(cnf_transformation,[status(thm)],[f342])).
% 0.70/0.97 fof(f346,plain,(
% 0.70/0.97 ![X0]: (v1_xboole_0(X0)|v3_altcat_2(k8_waybel34(X0),k4_waybel34(X0)))),
% 0.70/0.97 inference(cnf_transformation,[status(thm)],[f342])).
% 0.70/0.97 fof(f347,plain,(
% 0.70/0.97 ![X0]: (v1_xboole_0(X0)|m1_altcat_2(k8_waybel34(X0),k4_waybel34(X0)))),
% 0.70/0.97 inference(cnf_transformation,[status(thm)],[f342])).
% 0.70/0.97 fof(f348,plain,(
% 0.70/0.97 ![A]: (v2_setfam_1(A)|((((~v3_struct_0(k9_waybel34(A))&v2_altcat_1(k9_waybel34(A)))&v6_altcat_1(k9_waybel34(A)))&v3_altcat_2(k9_waybel34(A),k5_waybel34(A)))&m1_altcat_2(k9_waybel34(A),k5_waybel34(A))))),
% 0.70/0.97 inference(pre_NNF_transformation,[status(thm)],[f56])).
% 0.70/0.97 fof(f349,plain,(
% 0.70/0.97 ![X0]: (v2_setfam_1(X0)|~v3_struct_0(k9_waybel34(X0)))),
% 0.70/0.97 inference(cnf_transformation,[status(thm)],[f348])).
% 0.70/0.97 fof(f350,plain,(
% 0.70/0.97 ![X0]: (v2_setfam_1(X0)|v2_altcat_1(k9_waybel34(X0)))),
% 0.70/0.97 inference(cnf_transformation,[status(thm)],[f348])).
% 0.70/0.97 fof(f352,plain,(
% 0.70/0.97 ![X0]: (v2_setfam_1(X0)|v3_altcat_2(k9_waybel34(X0),k5_waybel34(X0)))),
% 0.70/0.97 inference(cnf_transformation,[status(thm)],[f348])).
% 0.70/0.97 fof(f353,plain,(
% 0.70/0.97 ![X0]: (v2_setfam_1(X0)|m1_altcat_2(k9_waybel34(X0),k5_waybel34(X0)))),
% 0.70/0.97 inference(cnf_transformation,[status(thm)],[f348])).
% 0.70/0.97 fof(f422,plain,(
% 0.70/0.97 ![A]: (v2_setfam_1(A)|((((((((((((~v3_struct_0(k4_waybel34(A))&v2_altcat_1(k4_waybel34(A)))&v6_altcat_1(k4_waybel34(A)))&v9_altcat_1(k4_waybel34(A)))&v11_altcat_1(k4_waybel34(A)))&v12_altcat_1(k4_waybel34(A)))&v1_altcat_2(k4_waybel34(A)))&v2_yellow18(k4_waybel34(A)))&v3_yellow18(k4_waybel34(A)))&v4_yellow18(k4_waybel34(A)))&v1_yellow21(k4_waybel34(A)))&v2_yellow21(k4_waybel34(A)))&v3_yellow21(k4_waybel34(A))))),
% 0.70/0.97 inference(pre_NNF_transformation,[status(thm)],[f91])).
% 0.70/0.97 fof(f423,plain,(
% 0.70/0.97 ![X0]: (v2_setfam_1(X0)|~v3_struct_0(k4_waybel34(X0)))),
% 0.70/0.97 inference(cnf_transformation,[status(thm)],[f422])).
% 0.70/0.97 fof(f424,plain,(
% 0.70/0.97 ![X0]: (v2_setfam_1(X0)|v2_altcat_1(k4_waybel34(X0)))),
% 0.70/0.97 inference(cnf_transformation,[status(thm)],[f422])).
% 0.70/0.97 fof(f427,plain,(
% 0.70/0.97 ![X0]: (v2_setfam_1(X0)|v11_altcat_1(k4_waybel34(X0)))),
% 0.70/0.97 inference(cnf_transformation,[status(thm)],[f422])).
% 0.70/0.97 fof(f428,plain,(
% 0.70/0.97 ![X0]: (v2_setfam_1(X0)|v12_altcat_1(k4_waybel34(X0)))),
% 0.70/0.97 inference(cnf_transformation,[status(thm)],[f422])).
% 0.70/0.97 fof(f442,plain,(
% 0.70/0.97 ![A]: (v2_setfam_1(A)|((((((((((((~v3_struct_0(k5_waybel34(A))&v2_altcat_1(k5_waybel34(A)))&v6_altcat_1(k5_waybel34(A)))&v9_altcat_1(k5_waybel34(A)))&v11_altcat_1(k5_waybel34(A)))&v12_altcat_1(k5_waybel34(A)))&v1_altcat_2(k5_waybel34(A)))&v2_yellow18(k5_waybel34(A)))&v3_yellow18(k5_waybel34(A)))&v4_yellow18(k5_waybel34(A)))&v1_yellow21(k5_waybel34(A)))&v2_yellow21(k5_waybel34(A)))&v3_yellow21(k5_waybel34(A))))),
% 0.70/0.97 inference(pre_NNF_transformation,[status(thm)],[f93])).
% 0.70/0.97 fof(f443,plain,(
% 0.70/0.97 ![X0]: (v2_setfam_1(X0)|~v3_struct_0(k5_waybel34(X0)))),
% 0.70/0.97 inference(cnf_transformation,[status(thm)],[f442])).
% 0.70/0.97 fof(f444,plain,(
% 0.70/0.97 ![X0]: (v2_setfam_1(X0)|v2_altcat_1(k5_waybel34(X0)))),
% 0.70/0.97 inference(cnf_transformation,[status(thm)],[f442])).
% 0.70/0.97 fof(f447,plain,(
% 0.70/0.97 ![X0]: (v2_setfam_1(X0)|v11_altcat_1(k5_waybel34(X0)))),
% 0.70/0.97 inference(cnf_transformation,[status(thm)],[f442])).
% 0.70/0.97 fof(f448,plain,(
% 0.70/0.97 ![X0]: (v2_setfam_1(X0)|v12_altcat_1(k5_waybel34(X0)))),
% 0.70/0.97 inference(cnf_transformation,[status(thm)],[f442])).
% 0.70/0.97 fof(f460,plain,(
% 0.70/0.97 ![A]: (v2_setfam_1(A)|(((((((v6_functor0(k6_waybel34(A),k4_waybel34(A),k5_waybel34(A))&v8_functor0(k6_waybel34(A),k4_waybel34(A),k5_waybel34(A)))&v9_functor0(k6_waybel34(A),k4_waybel34(A),k5_waybel34(A)))&v11_functor0(k6_waybel34(A),k4_waybel34(A),k5_waybel34(A)))&v12_functor0(k6_waybel34(A),k4_waybel34(A),k5_waybel34(A)))&v14_functor0(k6_waybel34(A),k4_waybel34(A),k5_waybel34(A)))&v16_functor0(k6_waybel34(A),k4_waybel34(A),k5_waybel34(A)))&v21_functor0(k6_waybel34(A),k4_waybel34(A),k5_waybel34(A))))),
% 0.70/0.97 inference(pre_NNF_transformation,[status(thm)],[f95])).
% 0.70/0.97 fof(f468,plain,(
% 0.70/0.97 ![X0]: (v2_setfam_1(X0)|v21_functor0(k6_waybel34(X0),k4_waybel34(X0),k5_waybel34(X0)))),
% 0.70/0.97 inference(cnf_transformation,[status(thm)],[f460])).
% 0.70/0.97 fof(f576,plain,(
% 0.70/0.97 ![A]: (v2_setfam_1(A)|(k15_functor0(k4_waybel34(A),k5_waybel34(A),k6_waybel34(A))=k7_waybel34(A)&k15_functor0(k5_waybel34(A),k4_waybel34(A),k7_waybel34(A))=k6_waybel34(A)))),
% 0.70/0.97 inference(pre_NNF_transformation,[status(thm)],[f118])).
% 0.70/0.97 fof(f577,plain,(
% 0.70/0.97 ![X0]: (v2_setfam_1(X0)|k15_functor0(k4_waybel34(X0),k5_waybel34(X0),k6_waybel34(X0))=k7_waybel34(X0))),
% 0.70/0.97 inference(cnf_transformation,[status(thm)],[f576])).
% 0.70/0.97 fof(f590,plain,(
% 0.70/0.97 ![A]: (((((v3_struct_0(A)|~v2_altcat_1(A))|~v11_altcat_1(A))|~v12_altcat_1(A))|~l2_altcat_1(A))|(![B]: (((((v3_struct_0(B)|~v2_altcat_1(B))|~v11_altcat_1(B))|~v12_altcat_1(B))|~l2_altcat_1(B))|(![C]: ((~v16_functor0(C,A,B)|~m2_functor0(C,A,B))|(~v21_functor0(C,A,B)|(![D]: ((((v3_struct_0(D)|~v2_altcat_1(D))|~v3_altcat_2(D,A))|~m1_altcat_2(D,A))|(![E]: ((((v3_struct_0(E)|~v2_altcat_1(E))|~v3_altcat_2(E,B))|~m1_altcat_2(E,B))|(~r3_yellow20(A,B,C,D,E)|r3_yellow20(B,A,k15_functor0(A,B,C),E,D))))))))))))),
% 0.70/0.97 inference(pre_NNF_transformation,[status(thm)],[f123])).
% 0.70/0.97 fof(f591,plain,(
% 0.70/0.97 ![X0,X1,X2,X3,X4]: (v3_struct_0(X0)|~v2_altcat_1(X0)|~v11_altcat_1(X0)|~v12_altcat_1(X0)|~l2_altcat_1(X0)|v3_struct_0(X1)|~v2_altcat_1(X1)|~v11_altcat_1(X1)|~v12_altcat_1(X1)|~l2_altcat_1(X1)|~v16_functor0(X2,X0,X1)|~m2_functor0(X2,X0,X1)|~v21_functor0(X2,X0,X1)|v3_struct_0(X3)|~v2_altcat_1(X3)|~v3_altcat_2(X3,X0)|~m1_altcat_2(X3,X0)|v3_struct_0(X4)|~v2_altcat_1(X4)|~v3_altcat_2(X4,X1)|~m1_altcat_2(X4,X1)|~r3_yellow20(X0,X1,X2,X3,X4)|r3_yellow20(X1,X0,k15_functor0(X0,X1,X2),X4,X3))),
% 0.70/0.97 inference(cnf_transformation,[status(thm)],[f590])).
% 0.70/0.97 fof(f592,plain,(
% 0.70/0.97 ![A]: (v2_setfam_1(A)|r3_yellow20(k4_waybel34(A),k5_waybel34(A),k6_waybel34(A),k8_waybel34(A),k9_waybel34(A)))),
% 0.70/0.97 inference(pre_NNF_transformation,[status(thm)],[f124])).
% 0.70/0.97 fof(f593,plain,(
% 0.70/0.97 ![X0]: (v2_setfam_1(X0)|r3_yellow20(k4_waybel34(X0),k5_waybel34(X0),k6_waybel34(X0),k8_waybel34(X0),k9_waybel34(X0)))),
% 0.70/0.97 inference(cnf_transformation,[status(thm)],[f592])).
% 0.70/0.97 fof(f1223,plain,(
% 0.70/0.97 k15_functor0(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl))=k7_waybel34(sK0_skl)),
% 0.70/0.97 inference(resolution,[status(thm)],[f577,f131])).
% 0.70/0.97 fof(f1225,plain,(
% 0.70/0.97 ![X0,X1]: (v3_struct_0(k4_waybel34(sK0_skl))|~v2_altcat_1(k4_waybel34(sK0_skl))|~v11_altcat_1(k4_waybel34(sK0_skl))|~v12_altcat_1(k4_waybel34(sK0_skl))|~l2_altcat_1(k4_waybel34(sK0_skl))|v3_struct_0(k5_waybel34(sK0_skl))|~v2_altcat_1(k5_waybel34(sK0_skl))|~v11_altcat_1(k5_waybel34(sK0_skl))|~v12_altcat_1(k5_waybel34(sK0_skl))|~l2_altcat_1(k5_waybel34(sK0_skl))|~v16_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))|~m2_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))|~v21_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))|v3_struct_0(X0)|~v2_altcat_1(X0)|~v3_altcat_2(X0,k4_waybel34(sK0_skl))|~m1_altcat_2(X0,k4_waybel34(sK0_skl))|v3_struct_0(X1)|~v2_altcat_1(X1)|~v3_altcat_2(X1,k5_waybel34(sK0_skl))|~m1_altcat_2(X1,k5_waybel34(sK0_skl))|~r3_yellow20(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl),X0,X1)|r3_yellow20(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl),X1,X0))),
% 0.70/0.97 inference(paramodulation,[status(thm)],[f1223,f591])).
% 0.70/0.97 fof(f1246,plain,(
% 0.70/0.97 ![X0,X1]: (v3_struct_0(k4_waybel34(sK0_skl))|~v2_altcat_1(k4_waybel34(sK0_skl))|~v11_altcat_1(k4_waybel34(sK0_skl))|~v12_altcat_1(k4_waybel34(sK0_skl))|~l2_altcat_1(k4_waybel34(sK0_skl))|v3_struct_0(k5_waybel34(sK0_skl))|~v2_altcat_1(k5_waybel34(sK0_skl))|~v11_altcat_1(k5_waybel34(sK0_skl))|~v12_altcat_1(k5_waybel34(sK0_skl))|~l2_altcat_1(k5_waybel34(sK0_skl))|~m2_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))|~v21_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))|v3_struct_0(X0)|~v2_altcat_1(X0)|~v3_altcat_2(X0,k4_waybel34(sK0_skl))|~m1_altcat_2(X0,k4_waybel34(sK0_skl))|v3_struct_0(X1)|~v2_altcat_1(X1)|~v3_altcat_2(X1,k5_waybel34(sK0_skl))|~m1_altcat_2(X1,k5_waybel34(sK0_skl))|~r3_yellow20(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl),X0,X1)|r3_yellow20(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl),X1,X0)|v2_setfam_1(sK0_skl))),
% 0.70/0.97 inference(resolution,[status(thm)],[f1225,f336])).
% 0.70/0.97 fof(f1249,plain,(
% 0.70/0.97 ![X0,X1]: (~v2_altcat_1(k4_waybel34(sK0_skl))|~v11_altcat_1(k4_waybel34(sK0_skl))|~v12_altcat_1(k4_waybel34(sK0_skl))|~l2_altcat_1(k4_waybel34(sK0_skl))|v3_struct_0(k5_waybel34(sK0_skl))|~v2_altcat_1(k5_waybel34(sK0_skl))|~v11_altcat_1(k5_waybel34(sK0_skl))|~v12_altcat_1(k5_waybel34(sK0_skl))|~l2_altcat_1(k5_waybel34(sK0_skl))|~m2_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))|~v21_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))|v3_struct_0(X0)|~v2_altcat_1(X0)|~v3_altcat_2(X0,k4_waybel34(sK0_skl))|~m1_altcat_2(X0,k4_waybel34(sK0_skl))|v3_struct_0(X1)|~v2_altcat_1(X1)|~v3_altcat_2(X1,k5_waybel34(sK0_skl))|~m1_altcat_2(X1,k5_waybel34(sK0_skl))|~r3_yellow20(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl),X0,X1)|r3_yellow20(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl),X1,X0)|v2_setfam_1(sK0_skl))),
% 0.70/0.97 inference(forward_subsumption_resolution,[status(thm)],[f1246,f423])).
% 0.70/0.97 fof(f1252,plain,(
% 0.70/0.97 ![X0,X1]: (~v2_altcat_1(k4_waybel34(sK0_skl))|~v11_altcat_1(k4_waybel34(sK0_skl))|~v12_altcat_1(k4_waybel34(sK0_skl))|~l2_altcat_1(k4_waybel34(sK0_skl))|v3_struct_0(k5_waybel34(sK0_skl))|~v2_altcat_1(k5_waybel34(sK0_skl))|~v11_altcat_1(k5_waybel34(sK0_skl))|~v12_altcat_1(k5_waybel34(sK0_skl))|~l2_altcat_1(k5_waybel34(sK0_skl))|~v21_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))|v3_struct_0(X0)|~v2_altcat_1(X0)|~v3_altcat_2(X0,k4_waybel34(sK0_skl))|~m1_altcat_2(X0,k4_waybel34(sK0_skl))|v3_struct_0(X1)|~v2_altcat_1(X1)|~v3_altcat_2(X1,k5_waybel34(sK0_skl))|~m1_altcat_2(X1,k5_waybel34(sK0_skl))|~r3_yellow20(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl),X0,X1)|r3_yellow20(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl),X1,X0)|v2_setfam_1(sK0_skl)|v2_setfam_1(sK0_skl))),
% 0.70/0.97 inference(resolution,[status(thm)],[f1249,f337])).
% 0.70/0.97 fof(f1254,plain,(
% 0.70/0.97 ![X0,X1]: (~v2_altcat_1(k4_waybel34(sK0_skl))|~v11_altcat_1(k4_waybel34(sK0_skl))|~v12_altcat_1(k4_waybel34(sK0_skl))|~l2_altcat_1(k4_waybel34(sK0_skl))|v3_struct_0(k5_waybel34(sK0_skl))|~v2_altcat_1(k5_waybel34(sK0_skl))|~v11_altcat_1(k5_waybel34(sK0_skl))|~v12_altcat_1(k5_waybel34(sK0_skl))|~l2_altcat_1(k5_waybel34(sK0_skl))|~v21_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))|v3_struct_0(X0)|~v2_altcat_1(X0)|~v3_altcat_2(X0,k4_waybel34(sK0_skl))|~m1_altcat_2(X0,k4_waybel34(sK0_skl))|v3_struct_0(X1)|~v2_altcat_1(X1)|~v3_altcat_2(X1,k5_waybel34(sK0_skl))|~m1_altcat_2(X1,k5_waybel34(sK0_skl))|~r3_yellow20(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl),X0,X1)|r3_yellow20(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl),X1,X0)|v2_setfam_1(sK0_skl))),
% 0.70/0.97 inference(duplicate_literals_removal,[status(thm)],[f1252])).
% 0.70/0.97 fof(f1255,plain,(
% 0.70/0.97 ![X0,X1]: (~v11_altcat_1(k4_waybel34(sK0_skl))|~v12_altcat_1(k4_waybel34(sK0_skl))|~l2_altcat_1(k4_waybel34(sK0_skl))|v3_struct_0(k5_waybel34(sK0_skl))|~v2_altcat_1(k5_waybel34(sK0_skl))|~v11_altcat_1(k5_waybel34(sK0_skl))|~v12_altcat_1(k5_waybel34(sK0_skl))|~l2_altcat_1(k5_waybel34(sK0_skl))|~v21_functor0(k6_waybel34(sK0_skl),k4_waybel34(sK0_skl),k5_waybel34(sK0_skl))|v3_struct_0(X0)|~v2_altcat_1(X0)|~v3_altcat_2(X0,k4_waybel34(sK0_skl))|~m1_altcat_2(X0,k4_waybel34(sK0_skl))|v3_struct_0(X1)|~v2_altcat_1(X1)|~v3_altcat_2(X1,k5_waybel34(sK0_skl))|~m1_altcat_2(X1,k5_waybel34(sK0_skl))|~r3_yellow20(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl),X0,X1)|r3_yellow20(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl),X1,X0)|v2_setfam_1(sK0_skl))),
% 0.70/0.97 inference(forward_subsumption_resolution,[status(thm)],[f1254,f424])).
% 0.70/0.97 fof(f1258,plain,(
% 0.70/0.97 ![X0,X1]: (~v11_altcat_1(k4_waybel34(sK0_skl))|~v12_altcat_1(k4_waybel34(sK0_skl))|~l2_altcat_1(k4_waybel34(sK0_skl))|v3_struct_0(k5_waybel34(sK0_skl))|~v2_altcat_1(k5_waybel34(sK0_skl))|~v11_altcat_1(k5_waybel34(sK0_skl))|~v12_altcat_1(k5_waybel34(sK0_skl))|~l2_altcat_1(k5_waybel34(sK0_skl))|v3_struct_0(X0)|~v2_altcat_1(X0)|~v3_altcat_2(X0,k4_waybel34(sK0_skl))|~m1_altcat_2(X0,k4_waybel34(sK0_skl))|v3_struct_0(X1)|~v2_altcat_1(X1)|~v3_altcat_2(X1,k5_waybel34(sK0_skl))|~m1_altcat_2(X1,k5_waybel34(sK0_skl))|~r3_yellow20(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl),X0,X1)|r3_yellow20(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl),X1,X0)|v2_setfam_1(sK0_skl)|v2_setfam_1(sK0_skl))),
% 0.70/0.97 inference(resolution,[status(thm)],[f1255,f468])).
% 0.70/0.97 fof(f1259,plain,(
% 0.70/0.97 ![X0,X1]: (~v11_altcat_1(k4_waybel34(sK0_skl))|~v12_altcat_1(k4_waybel34(sK0_skl))|~l2_altcat_1(k4_waybel34(sK0_skl))|v3_struct_0(k5_waybel34(sK0_skl))|~v2_altcat_1(k5_waybel34(sK0_skl))|~v11_altcat_1(k5_waybel34(sK0_skl))|~v12_altcat_1(k5_waybel34(sK0_skl))|~l2_altcat_1(k5_waybel34(sK0_skl))|v3_struct_0(X0)|~v2_altcat_1(X0)|~v3_altcat_2(X0,k4_waybel34(sK0_skl))|~m1_altcat_2(X0,k4_waybel34(sK0_skl))|v3_struct_0(X1)|~v2_altcat_1(X1)|~v3_altcat_2(X1,k5_waybel34(sK0_skl))|~m1_altcat_2(X1,k5_waybel34(sK0_skl))|~r3_yellow20(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl),X0,X1)|r3_yellow20(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl),X1,X0)|v2_setfam_1(sK0_skl))),
% 0.70/0.97 inference(duplicate_literals_removal,[status(thm)],[f1258])).
% 0.70/0.97 fof(f1260,plain,(
% 0.70/0.97 ![X0,X1]: (~v12_altcat_1(k4_waybel34(sK0_skl))|~l2_altcat_1(k4_waybel34(sK0_skl))|v3_struct_0(k5_waybel34(sK0_skl))|~v2_altcat_1(k5_waybel34(sK0_skl))|~v11_altcat_1(k5_waybel34(sK0_skl))|~v12_altcat_1(k5_waybel34(sK0_skl))|~l2_altcat_1(k5_waybel34(sK0_skl))|v3_struct_0(X0)|~v2_altcat_1(X0)|~v3_altcat_2(X0,k4_waybel34(sK0_skl))|~m1_altcat_2(X0,k4_waybel34(sK0_skl))|v3_struct_0(X1)|~v2_altcat_1(X1)|~v3_altcat_2(X1,k5_waybel34(sK0_skl))|~m1_altcat_2(X1,k5_waybel34(sK0_skl))|~r3_yellow20(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl),X0,X1)|r3_yellow20(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl),X1,X0)|v2_setfam_1(sK0_skl))),
% 0.70/0.97 inference(forward_subsumption_resolution,[status(thm)],[f1259,f427])).
% 0.70/0.97 fof(f1261,plain,(
% 0.70/0.97 ![X0,X1]: (~v12_altcat_1(k4_waybel34(sK0_skl))|v3_struct_0(k5_waybel34(sK0_skl))|~v2_altcat_1(k5_waybel34(sK0_skl))|~v11_altcat_1(k5_waybel34(sK0_skl))|~v12_altcat_1(k5_waybel34(sK0_skl))|~l2_altcat_1(k5_waybel34(sK0_skl))|v3_struct_0(X0)|~v2_altcat_1(X0)|~v3_altcat_2(X0,k4_waybel34(sK0_skl))|~m1_altcat_2(X0,k4_waybel34(sK0_skl))|v3_struct_0(X1)|~v2_altcat_1(X1)|~v3_altcat_2(X1,k5_waybel34(sK0_skl))|~m1_altcat_2(X1,k5_waybel34(sK0_skl))|~r3_yellow20(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl),X0,X1)|r3_yellow20(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl),X1,X0)|v2_setfam_1(sK0_skl)|v1_xboole_0(sK0_skl))),
% 0.70/0.97 inference(resolution,[status(thm)],[f1260,f325])).
% 0.70/0.97 fof(f1262,plain,(
% 0.70/0.97 ![X0,X1]: (v3_struct_0(k5_waybel34(sK0_skl))|~v2_altcat_1(k5_waybel34(sK0_skl))|~v11_altcat_1(k5_waybel34(sK0_skl))|~v12_altcat_1(k5_waybel34(sK0_skl))|~l2_altcat_1(k5_waybel34(sK0_skl))|v3_struct_0(X0)|~v2_altcat_1(X0)|~v3_altcat_2(X0,k4_waybel34(sK0_skl))|~m1_altcat_2(X0,k4_waybel34(sK0_skl))|v3_struct_0(X1)|~v2_altcat_1(X1)|~v3_altcat_2(X1,k5_waybel34(sK0_skl))|~m1_altcat_2(X1,k5_waybel34(sK0_skl))|~r3_yellow20(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl),X0,X1)|r3_yellow20(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl),X1,X0)|v2_setfam_1(sK0_skl)|v1_xboole_0(sK0_skl))),
% 0.70/0.97 inference(forward_subsumption_resolution,[status(thm)],[f1261,f428])).
% 0.70/0.97 fof(f1263,plain,(
% 0.70/0.97 ![X0,X1]: (v3_struct_0(k5_waybel34(sK0_skl))|~v2_altcat_1(k5_waybel34(sK0_skl))|~v11_altcat_1(k5_waybel34(sK0_skl))|~v12_altcat_1(k5_waybel34(sK0_skl))|v3_struct_0(X0)|~v2_altcat_1(X0)|~v3_altcat_2(X0,k4_waybel34(sK0_skl))|~m1_altcat_2(X0,k4_waybel34(sK0_skl))|v3_struct_0(X1)|~v2_altcat_1(X1)|~v3_altcat_2(X1,k5_waybel34(sK0_skl))|~m1_altcat_2(X1,k5_waybel34(sK0_skl))|~r3_yellow20(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl),X0,X1)|r3_yellow20(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl),X1,X0)|v2_setfam_1(sK0_skl)|v1_xboole_0(sK0_skl)|v1_xboole_0(sK0_skl))),
% 0.70/0.97 inference(resolution,[status(thm)],[f1262,f333])).
% 0.70/0.97 fof(f1264,plain,(
% 0.70/0.97 ![X0,X1]: (v3_struct_0(k5_waybel34(sK0_skl))|~v2_altcat_1(k5_waybel34(sK0_skl))|~v11_altcat_1(k5_waybel34(sK0_skl))|~v12_altcat_1(k5_waybel34(sK0_skl))|v3_struct_0(X0)|~v2_altcat_1(X0)|~v3_altcat_2(X0,k4_waybel34(sK0_skl))|~m1_altcat_2(X0,k4_waybel34(sK0_skl))|v3_struct_0(X1)|~v2_altcat_1(X1)|~v3_altcat_2(X1,k5_waybel34(sK0_skl))|~m1_altcat_2(X1,k5_waybel34(sK0_skl))|~r3_yellow20(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl),X0,X1)|r3_yellow20(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl),X1,X0)|v2_setfam_1(sK0_skl)|v1_xboole_0(sK0_skl))),
% 0.70/0.97 inference(duplicate_literals_removal,[status(thm)],[f1263])).
% 0.70/0.97 fof(f1265,plain,(
% 0.70/0.97 ![X0,X1]: (~v2_altcat_1(k5_waybel34(sK0_skl))|~v11_altcat_1(k5_waybel34(sK0_skl))|~v12_altcat_1(k5_waybel34(sK0_skl))|v3_struct_0(X0)|~v2_altcat_1(X0)|~v3_altcat_2(X0,k4_waybel34(sK0_skl))|~m1_altcat_2(X0,k4_waybel34(sK0_skl))|v3_struct_0(X1)|~v2_altcat_1(X1)|~v3_altcat_2(X1,k5_waybel34(sK0_skl))|~m1_altcat_2(X1,k5_waybel34(sK0_skl))|~r3_yellow20(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl),X0,X1)|r3_yellow20(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl),X1,X0)|v2_setfam_1(sK0_skl)|v1_xboole_0(sK0_skl))),
% 0.70/0.97 inference(forward_subsumption_resolution,[status(thm)],[f1264,f443])).
% 0.70/0.97 fof(f1266,plain,(
% 0.70/0.97 ![X0]: (~v2_altcat_1(k5_waybel34(sK0_skl))|~v11_altcat_1(k5_waybel34(sK0_skl))|~v12_altcat_1(k5_waybel34(sK0_skl))|v3_struct_0(k8_waybel34(sK0_skl))|~v2_altcat_1(k8_waybel34(sK0_skl))|~m1_altcat_2(k8_waybel34(sK0_skl),k4_waybel34(sK0_skl))|v3_struct_0(X0)|~v2_altcat_1(X0)|~v3_altcat_2(X0,k5_waybel34(sK0_skl))|~m1_altcat_2(X0,k5_waybel34(sK0_skl))|~r3_yellow20(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl),k8_waybel34(sK0_skl),X0)|r3_yellow20(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl),X0,k8_waybel34(sK0_skl))|v2_setfam_1(sK0_skl)|v1_xboole_0(sK0_skl)|v1_xboole_0(sK0_skl))),
% 0.70/0.97 inference(resolution,[status(thm)],[f1265,f346])).
% 0.70/0.97 fof(f1267,plain,(
% 0.70/0.97 ![X0]: (~v2_altcat_1(k5_waybel34(sK0_skl))|~v11_altcat_1(k5_waybel34(sK0_skl))|~v12_altcat_1(k5_waybel34(sK0_skl))|v3_struct_0(k8_waybel34(sK0_skl))|~v2_altcat_1(k8_waybel34(sK0_skl))|~m1_altcat_2(k8_waybel34(sK0_skl),k4_waybel34(sK0_skl))|v3_struct_0(X0)|~v2_altcat_1(X0)|~v3_altcat_2(X0,k5_waybel34(sK0_skl))|~m1_altcat_2(X0,k5_waybel34(sK0_skl))|~r3_yellow20(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl),k8_waybel34(sK0_skl),X0)|r3_yellow20(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl),X0,k8_waybel34(sK0_skl))|v2_setfam_1(sK0_skl)|v1_xboole_0(sK0_skl))),
% 0.70/0.97 inference(duplicate_literals_removal,[status(thm)],[f1266])).
% 0.70/0.97 fof(f1268,plain,(
% 0.70/0.97 ![X0]: (~v11_altcat_1(k5_waybel34(sK0_skl))|~v12_altcat_1(k5_waybel34(sK0_skl))|v3_struct_0(k8_waybel34(sK0_skl))|~v2_altcat_1(k8_waybel34(sK0_skl))|~m1_altcat_2(k8_waybel34(sK0_skl),k4_waybel34(sK0_skl))|v3_struct_0(X0)|~v2_altcat_1(X0)|~v3_altcat_2(X0,k5_waybel34(sK0_skl))|~m1_altcat_2(X0,k5_waybel34(sK0_skl))|~r3_yellow20(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl),k8_waybel34(sK0_skl),X0)|r3_yellow20(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl),X0,k8_waybel34(sK0_skl))|v2_setfam_1(sK0_skl)|v1_xboole_0(sK0_skl))),
% 0.70/0.97 inference(forward_subsumption_resolution,[status(thm)],[f1267,f444])).
% 0.70/0.97 fof(f1269,plain,(
% 0.70/0.97 ![X0]: (~v11_altcat_1(k5_waybel34(sK0_skl))|~v12_altcat_1(k5_waybel34(sK0_skl))|v3_struct_0(k8_waybel34(sK0_skl))|~v2_altcat_1(k8_waybel34(sK0_skl))|v3_struct_0(X0)|~v2_altcat_1(X0)|~v3_altcat_2(X0,k5_waybel34(sK0_skl))|~m1_altcat_2(X0,k5_waybel34(sK0_skl))|~r3_yellow20(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl),k8_waybel34(sK0_skl),X0)|r3_yellow20(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl),X0,k8_waybel34(sK0_skl))|v2_setfam_1(sK0_skl)|v1_xboole_0(sK0_skl)|v1_xboole_0(sK0_skl))),
% 0.70/0.97 inference(resolution,[status(thm)],[f1268,f347])).
% 0.70/0.97 fof(f1270,plain,(
% 0.70/0.97 ![X0]: (~v11_altcat_1(k5_waybel34(sK0_skl))|~v12_altcat_1(k5_waybel34(sK0_skl))|v3_struct_0(k8_waybel34(sK0_skl))|~v2_altcat_1(k8_waybel34(sK0_skl))|v3_struct_0(X0)|~v2_altcat_1(X0)|~v3_altcat_2(X0,k5_waybel34(sK0_skl))|~m1_altcat_2(X0,k5_waybel34(sK0_skl))|~r3_yellow20(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl),k8_waybel34(sK0_skl),X0)|r3_yellow20(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl),X0,k8_waybel34(sK0_skl))|v2_setfam_1(sK0_skl)|v1_xboole_0(sK0_skl))),
% 0.70/0.97 inference(duplicate_literals_removal,[status(thm)],[f1269])).
% 0.70/0.97 fof(f1271,plain,(
% 0.70/0.97 ![X0]: (~v12_altcat_1(k5_waybel34(sK0_skl))|v3_struct_0(k8_waybel34(sK0_skl))|~v2_altcat_1(k8_waybel34(sK0_skl))|v3_struct_0(X0)|~v2_altcat_1(X0)|~v3_altcat_2(X0,k5_waybel34(sK0_skl))|~m1_altcat_2(X0,k5_waybel34(sK0_skl))|~r3_yellow20(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl),k8_waybel34(sK0_skl),X0)|r3_yellow20(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl),X0,k8_waybel34(sK0_skl))|v2_setfam_1(sK0_skl)|v1_xboole_0(sK0_skl))),
% 0.70/0.97 inference(forward_subsumption_resolution,[status(thm)],[f1270,f447])).
% 0.70/0.97 fof(f1415,plain,(
% 0.70/0.97 ![X0]: (~v12_altcat_1(k5_waybel34(sK0_skl))|v3_struct_0(k8_waybel34(sK0_skl))|v3_struct_0(X0)|~v2_altcat_1(X0)|~v3_altcat_2(X0,k5_waybel34(sK0_skl))|~m1_altcat_2(X0,k5_waybel34(sK0_skl))|~r3_yellow20(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl),k8_waybel34(sK0_skl),X0)|r3_yellow20(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl),X0,k8_waybel34(sK0_skl))|v2_setfam_1(sK0_skl)|v1_xboole_0(sK0_skl)|v1_xboole_0(sK0_skl))),
% 0.70/0.97 inference(resolution,[status(thm)],[f1271,f344])).
% 0.70/0.97 fof(f1416,plain,(
% 0.70/0.97 ![X0]: (~v12_altcat_1(k5_waybel34(sK0_skl))|v3_struct_0(k8_waybel34(sK0_skl))|v3_struct_0(X0)|~v2_altcat_1(X0)|~v3_altcat_2(X0,k5_waybel34(sK0_skl))|~m1_altcat_2(X0,k5_waybel34(sK0_skl))|~r3_yellow20(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl),k8_waybel34(sK0_skl),X0)|r3_yellow20(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl),X0,k8_waybel34(sK0_skl))|v2_setfam_1(sK0_skl)|v1_xboole_0(sK0_skl))),
% 0.70/0.97 inference(duplicate_literals_removal,[status(thm)],[f1415])).
% 0.70/0.97 fof(f1417,plain,(
% 0.70/0.97 ![X0]: (v3_struct_0(k8_waybel34(sK0_skl))|v3_struct_0(X0)|~v2_altcat_1(X0)|~v3_altcat_2(X0,k5_waybel34(sK0_skl))|~m1_altcat_2(X0,k5_waybel34(sK0_skl))|~r3_yellow20(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl),k8_waybel34(sK0_skl),X0)|r3_yellow20(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl),X0,k8_waybel34(sK0_skl))|v2_setfam_1(sK0_skl)|v1_xboole_0(sK0_skl))),
% 0.70/0.97 inference(forward_subsumption_resolution,[status(thm)],[f1416,f448])).
% 0.70/0.97 fof(f1418,plain,(
% 0.70/0.97 v3_struct_0(k8_waybel34(sK0_skl))|v3_struct_0(k9_waybel34(sK0_skl))|~v2_altcat_1(k9_waybel34(sK0_skl))|~m1_altcat_2(k9_waybel34(sK0_skl),k5_waybel34(sK0_skl))|~r3_yellow20(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl),k8_waybel34(sK0_skl),k9_waybel34(sK0_skl))|r3_yellow20(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl),k9_waybel34(sK0_skl),k8_waybel34(sK0_skl))|v2_setfam_1(sK0_skl)|v1_xboole_0(sK0_skl)|v2_setfam_1(sK0_skl)),
% 0.70/0.97 inference(resolution,[status(thm)],[f1417,f352])).
% 0.70/0.97 fof(f1419,plain,(
% 0.70/0.97 v3_struct_0(k8_waybel34(sK0_skl))|v3_struct_0(k9_waybel34(sK0_skl))|~v2_altcat_1(k9_waybel34(sK0_skl))|~m1_altcat_2(k9_waybel34(sK0_skl),k5_waybel34(sK0_skl))|~r3_yellow20(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl),k8_waybel34(sK0_skl),k9_waybel34(sK0_skl))|r3_yellow20(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl),k9_waybel34(sK0_skl),k8_waybel34(sK0_skl))|v2_setfam_1(sK0_skl)|v1_xboole_0(sK0_skl)),
% 0.70/0.97 inference(duplicate_literals_removal,[status(thm)],[f1418])).
% 0.70/0.97 fof(f1420,plain,(
% 0.70/0.97 v3_struct_0(k9_waybel34(sK0_skl))|~v2_altcat_1(k9_waybel34(sK0_skl))|~m1_altcat_2(k9_waybel34(sK0_skl),k5_waybel34(sK0_skl))|~r3_yellow20(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl),k8_waybel34(sK0_skl),k9_waybel34(sK0_skl))|r3_yellow20(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl),k9_waybel34(sK0_skl),k8_waybel34(sK0_skl))|v2_setfam_1(sK0_skl)|v1_xboole_0(sK0_skl)),
% 0.70/0.97 inference(forward_subsumption_resolution,[status(thm)],[f1419,f343])).
% 0.70/0.97 fof(f1421,plain,(
% 0.70/0.97 v3_struct_0(k9_waybel34(sK0_skl))|~v2_altcat_1(k9_waybel34(sK0_skl))|~r3_yellow20(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl),k8_waybel34(sK0_skl),k9_waybel34(sK0_skl))|r3_yellow20(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl),k9_waybel34(sK0_skl),k8_waybel34(sK0_skl))|v2_setfam_1(sK0_skl)|v1_xboole_0(sK0_skl)|v2_setfam_1(sK0_skl)),
% 0.70/0.97 inference(resolution,[status(thm)],[f1420,f353])).
% 0.70/0.97 fof(f1422,plain,(
% 0.70/0.97 v3_struct_0(k9_waybel34(sK0_skl))|~v2_altcat_1(k9_waybel34(sK0_skl))|~r3_yellow20(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl),k8_waybel34(sK0_skl),k9_waybel34(sK0_skl))|r3_yellow20(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl),k9_waybel34(sK0_skl),k8_waybel34(sK0_skl))|v2_setfam_1(sK0_skl)|v1_xboole_0(sK0_skl)),
% 0.70/0.98 inference(duplicate_literals_removal,[status(thm)],[f1421])).
% 0.70/0.98 fof(f1423,plain,(
% 0.70/0.98 ~v2_altcat_1(k9_waybel34(sK0_skl))|~r3_yellow20(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl),k8_waybel34(sK0_skl),k9_waybel34(sK0_skl))|r3_yellow20(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl),k9_waybel34(sK0_skl),k8_waybel34(sK0_skl))|v2_setfam_1(sK0_skl)|v1_xboole_0(sK0_skl)),
% 0.70/0.98 inference(forward_subsumption_resolution,[status(thm)],[f1422,f349])).
% 0.70/0.98 fof(f1424,plain,(
% 0.70/0.98 ~r3_yellow20(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl),k8_waybel34(sK0_skl),k9_waybel34(sK0_skl))|r3_yellow20(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl),k9_waybel34(sK0_skl),k8_waybel34(sK0_skl))|v2_setfam_1(sK0_skl)|v1_xboole_0(sK0_skl)|v2_setfam_1(sK0_skl)),
% 0.70/0.98 inference(resolution,[status(thm)],[f1423,f350])).
% 0.70/0.98 fof(f1425,plain,(
% 0.70/0.98 ~r3_yellow20(k4_waybel34(sK0_skl),k5_waybel34(sK0_skl),k6_waybel34(sK0_skl),k8_waybel34(sK0_skl),k9_waybel34(sK0_skl))|r3_yellow20(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl),k9_waybel34(sK0_skl),k8_waybel34(sK0_skl))|v2_setfam_1(sK0_skl)|v1_xboole_0(sK0_skl)),
% 0.70/0.98 inference(duplicate_literals_removal,[status(thm)],[f1424])).
% 0.70/0.98 fof(f1426,plain,(
% 0.70/0.98 r3_yellow20(k5_waybel34(sK0_skl),k4_waybel34(sK0_skl),k7_waybel34(sK0_skl),k9_waybel34(sK0_skl),k8_waybel34(sK0_skl))|v2_setfam_1(sK0_skl)|v1_xboole_0(sK0_skl)),
% 0.70/0.98 inference(forward_subsumption_resolution,[status(thm)],[f1425,f593])).
% 0.70/0.98 fof(f1427,plain,(
% 0.70/0.98 v2_setfam_1(sK0_skl)|v1_xboole_0(sK0_skl)),
% 0.70/0.98 inference(resolution,[status(thm)],[f1426,f132])).
% 0.70/0.98 fof(f1428,plain,(
% 0.70/0.98 v1_xboole_0(sK0_skl)),
% 0.70/0.98 inference(forward_subsumption_resolution,[status(thm)],[f1427,f131])).
% 0.70/0.98 fof(f1945,plain,(
% 0.70/0.98 v2_setfam_1(sK0_skl)),
% 0.70/0.98 inference(resolution,[status(thm)],[f232,f1428])).
% 0.70/0.98 fof(f1950,plain,(
% 0.70/0.98 $false),
% 0.70/0.98 inference(forward_subsumption_resolution,[status(thm)],[f1945,f131])).
% 0.70/0.98 % SZS output end CNFRefutation for theBenchmark.p
% 0.59/0.99 % Elapsed time: 0.550906 seconds
% 0.59/0.99 % CPU time: 3.968073 seconds
% 0.59/0.99 % Total memory used: 140.017 MB
% 0.59/0.99 % Net memory used: 138.407 MB
%------------------------------------------------------------------------------