%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SYO606+1 : TPTP v9.3.1. Released v7.0.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 03:44:39 PM UTC 2026
% Result : Theorem 0.15s 5.94s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO606+1 : TPTP v9.3.1. Released v7.0.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/5.39 % Computer : n013.cluster.edu
% 0.10/5.39 % Model : x86_64 x86_64
% 0.10/5.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.39 % Memory : 8046.5625MB
% 0.10/5.39 % OS : Linux 6.8.0-71-generic
% 0.10/5.39 % CPULimit : 300
% 0.10/5.39 % WCLimit : 300
% 0.10/5.39 % DateTime : Mon Sep 21 12:03:00 UTC 2026
% 0.10/5.39 % CPUTime :
% 0.15/5.40 % Drodi V4.1.1
% 0.15/5.94 % Refutation found
% 0.15/5.94 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.15/5.94 % SZS output start CNFRefutation for theBenchmark
% 0.15/5.94 fof(f1,conjecture,(
% 0.15/5.94 ( ( (! [A] :( (! [B] : g_false_only(A,B))| (? [B] : h_true_only(A,B) )))& (! [A,B] :(? [C] :( g_false_only(A,B)| h_true_only(A,C) ) )))| ( (? [A] :( ( (? [B] : g_true_only(A,B))& ( ( (? [B] : h_both(A,B))& ~ (? [B] : h_true_only(A,B) ))| (! [B] : h_false_only(A,B) )) )| ( (? [B] : g_both(A,B))& ~ (? [B] : g_true_only(A,B))& (! [B] : h_false_only(A,B) )) ))& (? [A,B] :(! [C] :( ( g_true_only(A,B)& ( h_both(A,C)| h_false_only(A,C) ) )| ( g_both(A,B)& h_false_only(A,C) ) ) )))| ( (? [A] :( (? [B] : g_both(A,B))& ~ (? [B] : g_true_only(A,B))& (? [B] : h_both(A,B))& ~ (? [B] : h_true_only(A,B) )))& ~ (? [A] :( ( (? [B] : g_true_only(A,B))& ( ( (? [B] : h_both(A,B))& ~ (? [B] : h_true_only(A,B) ))| (! [B] : h_false_only(A,B) )) )| ( (? [B] : g_both(A,B))& ~ (? [B] : g_true_only(A,B))& (! [B] : h_false_only(A,B) )) ))& (? [A] :( (? [B] :( (? [C] :( g_both(A,B)& h_both(A,C) ))& ~ (? [C] :( g_false_only(A,B)| h_true_only(A,C) ) )))& ~ (? [B] :(! [C] :( ( g_true_only(A,B)& ( h_both(A,C)| h_false_only(A,C) ) )| ( g_both(A,B)& h_false_only(A,C) ) ) ))))& ~ (? [A,B] :(! [C] :( ( g_true_only(A,B)& ( h_both(A,C)| h_false_only(A,C) ) )| ( g_both(A,B)& h_false_only(A,C) ) ) ))) ) ),
% 0.15/5.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.94 fof(f2,negated_conjecture,(
% 0.15/5.94 ~(( ( (! [A] :( (! [B] : g_false_only(A,B))| (? [B] : h_true_only(A,B) )))& (! [A,B] :(? [C] :( g_false_only(A,B)| h_true_only(A,C) ) )))| ( (? [A] :( ( (? [B] : g_true_only(A,B))& ( ( (? [B] : h_both(A,B))& ~ (? [B] : h_true_only(A,B) ))| (! [B] : h_false_only(A,B) )) )| ( (? [B] : g_both(A,B))& ~ (? [B] : g_true_only(A,B))& (! [B] : h_false_only(A,B) )) ))& (? [A,B] :(! [C] :( ( g_true_only(A,B)& ( h_both(A,C)| h_false_only(A,C) ) )| ( g_both(A,B)& h_false_only(A,C) ) ) )))| ( (? [A] :( (? [B] : g_both(A,B))& ~ (? [B] : g_true_only(A,B))& (? [B] : h_both(A,B))& ~ (? [B] : h_true_only(A,B) )))& ~ (? [A] :( ( (? [B] : g_true_only(A,B))& ( ( (? [B] : h_both(A,B))& ~ (? [B] : h_true_only(A,B) ))| (! [B] : h_false_only(A,B) )) )| ( (? [B] : g_both(A,B))& ~ (? [B] : g_true_only(A,B))& (! [B] : h_false_only(A,B) )) ))& (? [A] :( (? [B] :( (? [C] :( g_both(A,B)& h_both(A,C) ))& ~ (? [C] :( g_false_only(A,B)| h_true_only(A,C) ) )))& ~ (? [B] :(! [C] :( ( g_true_only(A,B)& ( h_both(A,C)| h_false_only(A,C) ) )| ( g_both(A,B)& h_false_only(A,C) ) ) ))))& ~ (? [A,B] :(! [C] :( ( g_true_only(A,B)& ( h_both(A,C)| h_false_only(A,C) ) )| ( g_both(A,B)& h_false_only(A,C) ) ) ))) ) )),
% 0.15/5.94 inference(negated_conjecture,[status(cth)],[f1])).
% 0.15/5.94 fof(f3,axiom,(
% 0.15/5.94 (! [X_2,X_1] :( g_true_only(X_2,X_1)<=> ( g_true(X_2,X_1)& ~ g_false(X_2,X_1) ) ) )),
% 0.15/5.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.94 fof(f4,axiom,(
% 0.15/5.94 (! [X_2,X_1] :( g_both(X_2,X_1)<=> ( g_true(X_2,X_1)& g_false(X_2,X_1) ) ) )),
% 0.15/5.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.94 fof(f5,axiom,(
% 0.15/5.94 (! [X_2,X_1] :( g_false_only(X_2,X_1)<=> ( g_false(X_2,X_1)& ~ g_true(X_2,X_1) ) ) )),
% 0.15/5.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.94 fof(f6,axiom,(
% 0.15/5.94 (! [X_2,X_1] :( g_true_only(X_2,X_1)| g_both(X_2,X_1)| g_false_only(X_2,X_1) ) )),
% 0.15/5.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.94 fof(f7,axiom,(
% 0.15/5.94 (! [X_2,X_1] :( h_true_only(X_2,X_1)<=> ( h_true(X_2,X_1)& ~ h_false(X_2,X_1) ) ) )),
% 0.15/5.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.94 fof(f8,axiom,(
% 0.15/5.94 (! [X_2,X_1] :( h_both(X_2,X_1)<=> ( h_true(X_2,X_1)& h_false(X_2,X_1) ) ) )),
% 0.15/5.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.94 fof(f9,axiom,(
% 0.15/5.94 (! [X_2,X_1] :( h_false_only(X_2,X_1)<=> ( h_false(X_2,X_1)& ~ h_true(X_2,X_1) ) ) )),
% 0.15/5.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.94 fof(f10,axiom,(
% 0.15/5.94 (! [X_2,X_1] :( h_true_only(X_2,X_1)| h_both(X_2,X_1)| h_false_only(X_2,X_1) ) )),
% 0.15/5.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.94 fof(f11,plain,(
% 0.15/5.94 ((((?[A]: ((?[B]: ~g_false_only(A,B))&(![B]: ~h_true_only(A,B))))|(?[A,B]: ![C]: (~g_false_only(A,B)&~h_true_only(A,C))))&((![A]: (((![B]: ~g_true_only(A,B))|(((![B]: ~h_both(A,B))|(?[B]: h_true_only(A,B)))&(?[B]: ~h_false_only(A,B))))&(((![B]: ~g_both(A,B))|(?[B]: g_true_only(A,B)))|(?[B]: ~h_false_only(A,B)))))|(![A,B]: ?[C]: ((~g_true_only(A,B)|(~h_both(A,C)&~h_false_only(A,C)))&(~g_both(A,B)|~h_false_only(A,C))))))&((((![A]: ((((![B]: ~g_both(A,B))|(?[B]: g_true_only(A,B)))|(![B]: ~h_both(A,B)))|(?[B]: h_true_only(A,B))))|(?[A]: (((?[B]: g_true_only(A,B))&(((?[B]: h_both(A,B))&(![B]: ~h_true_only(A,B)))|(![B]: h_false_only(A,B))))|(((?[B]: g_both(A,B))&(![B]: ~g_true_only(A,B)))&(![B]: h_false_only(A,B))))))|(![A]: ((![B]: ((![C]: (~g_both(A,B)|~h_both(A,C)))|(?[C]: (g_false_only(A,B)|h_true_only(A,C)))))|(?[B]: ![C]: ((g_true_only(A,B)&(h_both(A,C)|h_false_only(A,C)))|(g_both(A,B)&h_false_only(A,C)))))))|(?[A,B]: ![C]: ((g_true_only(A,B)&(h_both(A,C)|h_false_only(A,C)))|(g_both(A,B)&h_false_only(A,C))))))),
% 0.15/5.94 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.15/5.94 fof(f12,definition,(
% 0.15/5.94 ![A]: (sP0_prd(A)<=>((?[B]: ~g_false_only(A,B))&(![B]: ~h_true_only(A,B))))),
% 0.15/5.94 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 0.15/5.94 fof(f13,definition,(
% 0.15/5.94 ![A]: (sP1_prd(A)<=>(((![B]: ~g_true_only(A,B))|(((![B]: ~h_both(A,B))|(?[B]: h_true_only(A,B)))&(?[B]: ~h_false_only(A,B))))&(((![B]: ~g_both(A,B))|(?[B]: g_true_only(A,B)))|(?[B]: ~h_false_only(A,B)))))),
% 0.15/5.94 introduced(definition,[new_symbols(definition,[sP1_prd])],[])).
% 0.15/5.94 fof(f14,definition,(
% 0.15/5.94 ![A]: (sP2_prd(A)<=>(((?[B]: g_true_only(A,B))&(((?[B]: h_both(A,B))&(![B]: ~h_true_only(A,B)))|(![B]: h_false_only(A,B))))|(((?[B]: g_both(A,B))&(![B]: ~g_true_only(A,B)))&(![B]: h_false_only(A,B)))))),
% 0.15/5.94 introduced(definition,[new_symbols(definition,[sP2_prd])],[])).
% 0.15/5.94 fof(f15,definition,(
% 0.15/5.94 ![A,B,C]: (sP3_prd(C,B,A)<=>((g_true_only(A,B)&(h_both(A,C)|h_false_only(A,C)))|(g_both(A,B)&h_false_only(A,C))))),
% 0.15/5.94 introduced(definition,[new_symbols(definition,[sP3_prd])],[])).
% 0.15/5.94 fof(f16,definition,(
% 0.15/5.94 ![A,B,C]: (sP4_prd(C,B,A)<=>(g_true_only(A,B)&(h_both(A,C)|h_false_only(A,C))))),
% 0.15/5.94 introduced(definition,[new_symbols(definition,[sP4_prd])],[])).
% 0.15/5.94 fof(f17,plain,(
% 0.15/5.94 (((?[A]: sP0_prd(A))|(?[A,B]: ![C]: (~g_false_only(A,B)&~h_true_only(A,C))))&((![A]: sP1_prd(A))|(![A,B]: ?[C]: ((~g_true_only(A,B)|(~h_both(A,C)&~h_false_only(A,C)))&(~g_both(A,B)|~h_false_only(A,C))))))&((((![A]: ((((![B]: ~g_both(A,B))|(?[B]: g_true_only(A,B)))|(![B]: ~h_both(A,B)))|(?[B]: h_true_only(A,B))))|(?[A]: sP2_prd(A)))|(![A]: ((![B]: ((![C]: (~g_both(A,B)|~h_both(A,C)))|(?[C]: (g_false_only(A,B)|h_true_only(A,C)))))|(?[B]: ![C]: sP3_prd(C,B,A)))))|(?[A,B]: ![C]: (sP4_prd(C,B,A)|(g_both(A,B)&h_false_only(A,C)))))),
% 0.15/5.94 inference(formula_renaming,[status(thm)],[f11,f16,f15,f14,f13,f12])).
% 0.15/5.94 fof(f18,plain,(
% 0.15/5.94 (((?[A]: sP0_prd(A))|(?[A]: ((?[B]: ~g_false_only(A,B))&(![C]: ~h_true_only(A,C)))))&((![A]: sP1_prd(A))|(![A,B]: ?[C]: ((~g_true_only(A,B)|(~h_both(A,C)&~h_false_only(A,C)))&(~g_both(A,B)|~h_false_only(A,C))))))&((((![A]: ((((![B]: ~g_both(A,B))|(?[B]: g_true_only(A,B)))|(![B]: ~h_both(A,B)))|(?[B]: h_true_only(A,B))))|(?[A]: sP2_prd(A)))|(![A]: ((![B]: ((~g_both(A,B)|(![C]: ~h_both(A,C)))|(g_false_only(A,B)|(?[C]: h_true_only(A,C)))))|(?[B]: ![C]: sP3_prd(C,B,A)))))|(?[A,B]: ![C]: (sP4_prd(C,B,A)|(g_both(A,B)&h_false_only(A,C)))))),
% 0.15/5.94 inference(miniscoping,[status(thm)],[f17])).
% 0.15/5.94 fof(f19,plain,(
% 0.15/5.94 ((sP0_prd(sK0_skl)|(~g_false_only(sK1_skl,sK2_skl)&(![C]: ~h_true_only(sK1_skl,C))))&((![A]: sP1_prd(A))|(![A,B]: ((~g_true_only(A,B)|(~h_both(A,sK3_skl(B,A))&~h_false_only(A,sK3_skl(B,A))))&(~g_both(A,B)|~h_false_only(A,sK3_skl(B,A)))))))&((((![A]: ((((![B]: ~g_both(A,B))|g_true_only(A,sK4_skl(A)))|(![B]: ~h_both(A,B)))|h_true_only(A,sK5_skl(A))))|sP2_prd(sK6_skl))|(![A]: ((![B]: ((~g_both(A,B)|(![C]: ~h_both(A,C)))|(g_false_only(A,B)|h_true_only(A,sK7_skl(B,A)))))|![C]: sP3_prd(C,sK8_skl(A),A))))|![C]: (sP4_prd(C,sK10_skl,sK9_skl)|(g_both(sK9_skl,sK10_skl)&h_false_only(sK9_skl,C))))),
% 0.15/5.94 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl,sK3_skl,sK4_skl,sK5_skl,sK6_skl,sK7_skl,sK8_skl,sK9_skl,sK10_skl]),skolemize(A,sK0_skl),skolemize(A,sK1_skl),skolemize(B,sK2_skl),skolemize(C,sK3_skl(B,A)),skolemize(B,sK4_skl(A)),skolemize(B,sK5_skl(A)),skolemize(A,sK6_skl),skolemize(C,sK7_skl(B,A)),skolemize(B,sK8_skl(A)),skolemize(A,sK9_skl),skolemize(B,sK10_skl)],[f18])).
% 0.15/5.94 fof(f20,plain,(
% 0.15/5.94 sP0_prd(sK0_skl)|~g_false_only(sK1_skl,sK2_skl)),
% 0.15/5.94 inference(cnf_transformation,[status(thm)],[f19])).
% 0.15/5.94 fof(f21,plain,(
% 0.15/5.94 ![X0]: (sP0_prd(sK0_skl)|~h_true_only(sK1_skl,X0))),
% 0.15/5.94 inference(cnf_transformation,[status(thm)],[f19])).
% 0.15/5.94 fof(f22,plain,(
% 0.15/5.94 ![X0,X1,X2]: (sP1_prd(X0)|~g_true_only(X1,X2)|~h_both(X1,sK3_skl(X2,X1)))),
% 0.15/5.94 inference(cnf_transformation,[status(thm)],[f19])).
% 0.15/5.94 fof(f23,plain,(
% 0.15/5.94 ![X0,X1,X2]: (sP1_prd(X0)|~g_true_only(X1,X2)|~h_false_only(X1,sK3_skl(X2,X1)))),
% 0.15/5.94 inference(cnf_transformation,[status(thm)],[f19])).
% 0.15/5.94 fof(f24,plain,(
% 0.15/5.94 ![X0,X1,X2]: (sP1_prd(X0)|~g_both(X1,X2)|~h_false_only(X1,sK3_skl(X2,X1)))),
% 0.15/5.94 inference(cnf_transformation,[status(thm)],[f19])).
% 0.15/5.94 fof(f25,plain,(
% 0.15/5.94 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~g_both(X0,X1)|g_true_only(X0,sK4_skl(X0))|~h_both(X0,X2)|h_true_only(X0,sK5_skl(X0))|sP2_prd(sK6_skl)|~g_both(X3,X4)|~h_both(X3,X5)|g_false_only(X3,X4)|h_true_only(X3,sK7_skl(X4,X3))|sP3_prd(X6,sK8_skl(X3),X3)|sP4_prd(X7,sK10_skl,sK9_skl)|g_both(sK9_skl,sK10_skl))),
% 0.15/5.94 inference(cnf_transformation,[status(thm)],[f19])).
% 0.15/5.94 fof(f26,plain,(
% 0.15/5.94 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~g_both(X0,X1)|g_true_only(X0,sK4_skl(X0))|~h_both(X0,X2)|h_true_only(X0,sK5_skl(X0))|sP2_prd(sK6_skl)|~g_both(X3,X4)|~h_both(X3,X5)|g_false_only(X3,X4)|h_true_only(X3,sK7_skl(X4,X3))|sP3_prd(X6,sK8_skl(X3),X3)|sP4_prd(X7,sK10_skl,sK9_skl)|h_false_only(sK9_skl,X7))),
% 0.15/5.94 inference(cnf_transformation,[status(thm)],[f19])).
% 0.15/5.94 fof(f27,plain,(
% 0.15/5.94 ![X_2,X_1]: ((~g_true_only(X_2,X_1)|(g_true(X_2,X_1)&~g_false(X_2,X_1)))&(g_true_only(X_2,X_1)|(~g_true(X_2,X_1)|g_false(X_2,X_1))))),
% 0.15/5.94 inference(NNF_transformation,[status(thm)],[f3])).
% 0.15/5.94 fof(f28,plain,(
% 0.15/5.94 (![X_2,X_1]: (~g_true_only(X_2,X_1)|(g_true(X_2,X_1)&~g_false(X_2,X_1))))&(![X_2,X_1]: (g_true_only(X_2,X_1)|(~g_true(X_2,X_1)|g_false(X_2,X_1))))),
% 0.15/5.94 inference(miniscoping,[status(thm)],[f27])).
% 0.15/5.94 fof(f29,plain,(
% 0.15/5.94 ![X0,X1]: (~g_true_only(X0,X1)|g_true(X0,X1))),
% 0.15/5.94 inference(cnf_transformation,[status(thm)],[f28])).
% 0.15/5.94 fof(f30,plain,(
% 0.15/5.94 ![X0,X1]: (~g_true_only(X0,X1)|~g_false(X0,X1))),
% 0.15/5.94 inference(cnf_transformation,[status(thm)],[f28])).
% 0.15/5.94 fof(f32,plain,(
% 0.15/5.94 ![X_2,X_1]: ((~g_both(X_2,X_1)|(g_true(X_2,X_1)&g_false(X_2,X_1)))&(g_both(X_2,X_1)|(~g_true(X_2,X_1)|~g_false(X_2,X_1))))),
% 0.15/5.94 inference(NNF_transformation,[status(thm)],[f4])).
% 0.15/5.94 fof(f33,plain,(
% 0.15/5.94 (![X_2,X_1]: (~g_both(X_2,X_1)|(g_true(X_2,X_1)&g_false(X_2,X_1))))&(![X_2,X_1]: (g_both(X_2,X_1)|(~g_true(X_2,X_1)|~g_false(X_2,X_1))))),
% 0.15/5.94 inference(miniscoping,[status(thm)],[f32])).
% 0.15/5.94 fof(f34,plain,(
% 0.15/5.94 ![X0,X1]: (~g_both(X0,X1)|g_true(X0,X1))),
% 0.15/5.94 inference(cnf_transformation,[status(thm)],[f33])).
% 0.15/5.94 fof(f37,plain,(
% 0.15/5.94 ![X_2,X_1]: ((~g_false_only(X_2,X_1)|(g_false(X_2,X_1)&~g_true(X_2,X_1)))&(g_false_only(X_2,X_1)|(~g_false(X_2,X_1)|g_true(X_2,X_1))))),
% 0.15/5.94 inference(NNF_transformation,[status(thm)],[f5])).
% 0.15/5.94 fof(f38,plain,(
% 0.15/5.94 (![X_2,X_1]: (~g_false_only(X_2,X_1)|(g_false(X_2,X_1)&~g_true(X_2,X_1))))&(![X_2,X_1]: (g_false_only(X_2,X_1)|(~g_false(X_2,X_1)|g_true(X_2,X_1))))),
% 0.15/5.94 inference(miniscoping,[status(thm)],[f37])).
% 0.15/5.94 fof(f39,plain,(
% 0.15/5.94 ![X0,X1]: (~g_false_only(X0,X1)|g_false(X0,X1))),
% 0.15/5.94 inference(cnf_transformation,[status(thm)],[f38])).
% 0.15/5.94 fof(f40,plain,(
% 0.15/5.94 ![X0,X1]: (~g_false_only(X0,X1)|~g_true(X0,X1))),
% 0.15/5.94 inference(cnf_transformation,[status(thm)],[f38])).
% 0.15/5.94 fof(f42,plain,(
% 0.15/5.94 ![X0,X1]: (g_true_only(X0,X1)|g_both(X0,X1)|g_false_only(X0,X1))),
% 0.15/5.94 inference(cnf_transformation,[status(thm)],[f6])).
% 0.15/5.94 fof(f43,plain,(
% 0.15/5.94 ![X_2,X_1]: ((~h_true_only(X_2,X_1)|(h_true(X_2,X_1)&~h_false(X_2,X_1)))&(h_true_only(X_2,X_1)|(~h_true(X_2,X_1)|h_false(X_2,X_1))))),
% 0.15/5.94 inference(NNF_transformation,[status(thm)],[f7])).
% 0.15/5.94 fof(f44,plain,(
% 0.15/5.94 (![X_2,X_1]: (~h_true_only(X_2,X_1)|(h_true(X_2,X_1)&~h_false(X_2,X_1))))&(![X_2,X_1]: (h_true_only(X_2,X_1)|(~h_true(X_2,X_1)|h_false(X_2,X_1))))),
% 0.15/5.94 inference(miniscoping,[status(thm)],[f43])).
% 0.15/5.94 fof(f46,plain,(
% 0.15/5.94 ![X0,X1]: (~h_true_only(X0,X1)|~h_false(X0,X1))),
% 0.15/5.94 inference(cnf_transformation,[status(thm)],[f44])).
% 0.15/5.94 fof(f48,plain,(
% 0.15/5.94 ![X_2,X_1]: ((~h_both(X_2,X_1)|(h_true(X_2,X_1)&h_false(X_2,X_1)))&(h_both(X_2,X_1)|(~h_true(X_2,X_1)|~h_false(X_2,X_1))))),
% 0.15/5.94 inference(NNF_transformation,[status(thm)],[f8])).
% 0.15/5.94 fof(f49,plain,(
% 0.15/5.94 (![X_2,X_1]: (~h_both(X_2,X_1)|(h_true(X_2,X_1)&h_false(X_2,X_1))))&(![X_2,X_1]: (h_both(X_2,X_1)|(~h_true(X_2,X_1)|~h_false(X_2,X_1))))),
% 0.15/5.94 inference(miniscoping,[status(thm)],[f48])).
% 0.15/5.94 fof(f51,plain,(
% 0.15/5.94 ![X0,X1]: (~h_both(X0,X1)|h_false(X0,X1))),
% 0.15/5.94 inference(cnf_transformation,[status(thm)],[f49])).
% 0.15/5.94 fof(f53,plain,(
% 0.15/5.94 ![X_2,X_1]: ((~h_false_only(X_2,X_1)|(h_false(X_2,X_1)&~h_true(X_2,X_1)))&(h_false_only(X_2,X_1)|(~h_false(X_2,X_1)|h_true(X_2,X_1))))),
% 0.15/5.94 inference(NNF_transformation,[status(thm)],[f9])).
% 0.15/5.94 fof(f54,plain,(
% 0.15/5.94 (![X_2,X_1]: (~h_false_only(X_2,X_1)|(h_false(X_2,X_1)&~h_true(X_2,X_1))))&(![X_2,X_1]: (h_false_only(X_2,X_1)|(~h_false(X_2,X_1)|h_true(X_2,X_1))))),
% 0.15/5.94 inference(miniscoping,[status(thm)],[f53])).
% 0.15/5.94 fof(f55,plain,(
% 0.15/5.94 ![X0,X1]: (~h_false_only(X0,X1)|h_false(X0,X1))),
% 0.15/5.94 inference(cnf_transformation,[status(thm)],[f54])).
% 0.15/5.94 fof(f58,plain,(
% 0.15/5.94 ![X0,X1]: (h_true_only(X0,X1)|h_both(X0,X1)|h_false_only(X0,X1))),
% 0.15/5.94 inference(cnf_transformation,[status(thm)],[f10])).
% 0.15/5.94 fof(f59,plain,(
% 0.15/5.94 ![A]: ((~sP0_prd(A)|((?[B]: ~g_false_only(A,B))&(![B]: ~h_true_only(A,B))))&(sP0_prd(A)|((![B]: g_false_only(A,B))|(?[B]: h_true_only(A,B)))))),
% 0.15/5.94 inference(NNF_transformation,[status(thm)],[f12])).
% 0.15/5.94 fof(f60,plain,(
% 0.15/5.94 (![A]: (~sP0_prd(A)|((?[B]: ~g_false_only(A,B))&(![B]: ~h_true_only(A,B)))))&(![A]: (sP0_prd(A)|((![B]: g_false_only(A,B))|(?[B]: h_true_only(A,B)))))),
% 0.15/5.94 inference(miniscoping,[status(thm)],[f59])).
% 0.15/5.94 fof(f61,plain,(
% 0.15/5.94 (![A]: (~sP0_prd(A)|(~g_false_only(A,sK11_skl(A))&(![B]: ~h_true_only(A,B)))))&(![A]: (sP0_prd(A)|((![B]: g_false_only(A,B))|h_true_only(A,sK12_skl(A)))))),
% 0.15/5.94 inference(skolemize,[status(esa),new_symbols(skolem,[sK11_skl,sK12_skl]),skolemize(B,sK11_skl(A)),skolemize(B,sK12_skl(A))],[f60])).
% 0.15/5.94 fof(f62,plain,(
% 0.15/5.94 ![X0]: (~sP0_prd(X0)|~g_false_only(X0,sK11_skl(X0)))),
% 0.15/5.94 inference(cnf_transformation,[status(thm)],[f61])).
% 0.15/5.94 fof(f63,plain,(
% 0.15/5.94 ![X0,X1]: (~sP0_prd(X0)|~h_true_only(X0,X1))),
% 0.15/5.94 inference(cnf_transformation,[status(thm)],[f61])).
% 0.15/5.94 fof(f64,plain,(
% 0.15/5.94 ![X0,X1]: (sP0_prd(X0)|g_false_only(X0,X1)|h_true_only(X0,sK12_skl(X0)))),
% 0.15/5.94 inference(cnf_transformation,[status(thm)],[f61])).
% 0.15/5.94 fof(f65,definition,(
% 0.15/5.94 ![A]: (sP5_prd(A)<=>((![B]: ~g_true_only(A,B))|(((![B]: ~h_both(A,B))|(?[B]: h_true_only(A,B)))&(?[B]: ~h_false_only(A,B)))))),
% 0.15/5.94 introduced(definition,[new_symbols(definition,[sP5_prd])],[])).
% 0.15/5.94 fof(f66,plain,(
% 0.15/5.94 ![A]: (sP1_prd(A)<=>(sP5_prd(A)&(((![B]: ~g_both(A,B))|(?[B]: g_true_only(A,B)))|(?[B]: ~h_false_only(A,B)))))),
% 0.15/5.94 inference(formula_renaming,[status(thm)],[f13,f65])).
% 0.15/5.94 fof(f67,plain,(
% 0.15/5.94 ![A]: ((~sP1_prd(A)|(sP5_prd(A)&(((![B]: ~g_both(A,B))|(?[B]: g_true_only(A,B)))|(?[B]: ~h_false_only(A,B)))))&(sP1_prd(A)|(~sP5_prd(A)|(((?[B]: g_both(A,B))&(![B]: ~g_true_only(A,B)))&(![B]: h_false_only(A,B))))))),
% 0.15/5.94 inference(NNF_transformation,[status(thm)],[f66])).
% 0.15/5.94 fof(f68,plain,(
% 0.15/5.94 (![A]: (~sP1_prd(A)|(sP5_prd(A)&(((![B]: ~g_both(A,B))|(?[B]: g_true_only(A,B)))|(?[B]: ~h_false_only(A,B))))))&(![A]: (sP1_prd(A)|(~sP5_prd(A)|(((?[B]: g_both(A,B))&(![B]: ~g_true_only(A,B)))&(![B]: h_false_only(A,B))))))),
% 0.15/5.94 inference(miniscoping,[status(thm)],[f67])).
% 0.15/5.94 fof(f69,plain,(
% 0.15/5.94 (![A]: (~sP1_prd(A)|(sP5_prd(A)&(((![B]: ~g_both(A,B))|g_true_only(A,sK13_skl(A)))|~h_false_only(A,sK14_skl(A))))))&(![A]: (sP1_prd(A)|(~sP5_prd(A)|((g_both(A,sK15_skl(A))&(![B]: ~g_true_only(A,B)))&(![B]: h_false_only(A,B))))))),
% 0.15/5.94 inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl,sK14_skl,sK15_skl]),skolemize(B,sK13_skl(A)),skolemize(B,sK14_skl(A)),skolemize(B,sK15_skl(A))],[f68])).
% 0.15/5.94 fof(f70,plain,(
% 0.15/5.94 ![X0]: (~sP1_prd(X0)|sP5_prd(X0))),
% 0.15/5.94 inference(cnf_transformation,[status(thm)],[f69])).
% 0.15/5.94 fof(f71,plain,(
% 0.15/5.94 ![X0,X1]: (~sP1_prd(X0)|~g_both(X0,X1)|g_true_only(X0,sK13_skl(X0))|~h_false_only(X0,sK14_skl(X0)))),
% 0.15/5.94 inference(cnf_transformation,[status(thm)],[f69])).
% 0.15/5.94 fof(f72,plain,(
% 0.15/5.94 ![X0]: (sP1_prd(X0)|~sP5_prd(X0)|g_both(X0,sK15_skl(X0)))),
% 0.15/5.94 inference(cnf_transformation,[status(thm)],[f69])).
% 0.15/5.94 fof(f74,plain,(
% 0.15/5.94 ![X0,X1]: (sP1_prd(X0)|~sP5_prd(X0)|h_false_only(X0,X1))),
% 0.15/5.94 inference(cnf_transformation,[status(thm)],[f69])).
% 0.15/5.94 fof(f75,definition,(
% 0.15/5.94 ![A]: (sP6_prd(A)<=>((?[B]: g_true_only(A,B))&(((?[B]: h_both(A,B))&(![B]: ~h_true_only(A,B)))|(![B]: h_false_only(A,B)))))),
% 0.15/5.94 introduced(definition,[new_symbols(definition,[sP6_prd])],[])).
% 0.15/5.94 fof(f76,plain,(
% 0.15/5.94 ![A]: (sP2_prd(A)<=>(sP6_prd(A)|(((?[B]: g_both(A,B))&(![B]: ~g_true_only(A,B)))&(![B]: h_false_only(A,B)))))),
% 0.15/5.94 inference(formula_renaming,[status(thm)],[f14,f75])).
% 0.15/5.94 fof(f77,plain,(
% 0.15/5.94 ![A]: ((~sP2_prd(A)|(sP6_prd(A)|(((?[B]: g_both(A,B))&(![B]: ~g_true_only(A,B)))&(![B]: h_false_only(A,B)))))&(sP2_prd(A)|(~sP6_prd(A)&(((![B]: ~g_both(A,B))|(?[B]: g_true_only(A,B)))|(?[B]: ~h_false_only(A,B))))))),
% 0.15/5.94 inference(NNF_transformation,[status(thm)],[f76])).
% 0.15/5.94 fof(f78,plain,(
% 0.15/5.94 (![A]: (~sP2_prd(A)|(sP6_prd(A)|(((?[B]: g_both(A,B))&(![B]: ~g_true_only(A,B)))&(![B]: h_false_only(A,B))))))&(![A]: (sP2_prd(A)|(~sP6_prd(A)&(((![B]: ~g_both(A,B))|(?[B]: g_true_only(A,B)))|(?[B]: ~h_false_only(A,B))))))),
% 0.15/5.94 inference(miniscoping,[status(thm)],[f77])).
% 0.15/5.94 fof(f79,plain,(
% 0.15/5.94 (![A]: (~sP2_prd(A)|(sP6_prd(A)|((g_both(A,sK16_skl(A))&(![B]: ~g_true_only(A,B)))&(![B]: h_false_only(A,B))))))&(![A]: (sP2_prd(A)|(~sP6_prd(A)&(((![B]: ~g_both(A,B))|g_true_only(A,sK17_skl(A)))|~h_false_only(A,sK18_skl(A))))))),
% 0.15/5.94 inference(skolemize,[status(esa),new_symbols(skolem,[sK16_skl,sK17_skl,sK18_skl]),skolemize(B,sK16_skl(A)),skolemize(B,sK17_skl(A)),skolemize(B,sK18_skl(A))],[f78])).
% 0.15/5.94 fof(f80,plain,(
% 0.15/5.94 ![X0]: (~sP2_prd(X0)|sP6_prd(X0)|g_both(X0,sK16_skl(X0)))),
% 0.15/5.94 inference(cnf_transformation,[status(thm)],[f79])).
% 0.15/5.94 fof(f82,plain,(
% 0.15/5.94 ![X0,X1]: (~sP2_prd(X0)|sP6_prd(X0)|h_false_only(X0,X1))),
% 0.15/5.94 inference(cnf_transformation,[status(thm)],[f79])).
% 0.15/5.94 fof(f85,plain,(
% 0.15/5.94 ![A,B,C]: ((~sP3_prd(C,B,A)|((g_true_only(A,B)&(h_both(A,C)|h_false_only(A,C)))|(g_both(A,B)&h_false_only(A,C))))&(sP3_prd(C,B,A)|((~g_true_only(A,B)|(~h_both(A,C)&~h_false_only(A,C)))&(~g_both(A,B)|~h_false_only(A,C)))))),
% 0.15/5.94 inference(NNF_transformation,[status(thm)],[f15])).
% 0.15/5.94 fof(f86,plain,(
% 0.15/5.94 (![A,B,C]: (~sP3_prd(C,B,A)|((g_true_only(A,B)&(h_both(A,C)|h_false_only(A,C)))|(g_both(A,B)&h_false_only(A,C)))))&(![A,B,C]: (sP3_prd(C,B,A)|((~g_true_only(A,B)|(~h_both(A,C)&~h_false_only(A,C)))&(~g_both(A,B)|~h_false_only(A,C)))))),
% 0.15/5.94 inference(miniscoping,[status(thm)],[f85])).
% 0.15/5.94 fof(f88,plain,(
% 0.15/5.94 ![X0,X1,X2]: (~sP3_prd(X0,X1,X2)|g_true_only(X2,X1)|h_false_only(X2,X0))),
% 0.15/5.94 inference(cnf_transformation,[status(thm)],[f86])).
% 0.15/5.94 fof(f94,plain,(
% 0.15/5.94 ![A,B,C]: ((~sP4_prd(C,B,A)|(g_true_only(A,B)&(h_both(A,C)|h_false_only(A,C))))&(sP4_prd(C,B,A)|(~g_true_only(A,B)|(~h_both(A,C)&~h_false_only(A,C)))))),
% 0.15/5.94 inference(NNF_transformation,[status(thm)],[f16])).
% 0.15/5.94 fof(f95,plain,(
% 0.15/5.94 (![A,B,C]: (~sP4_prd(C,B,A)|(g_true_only(A,B)&(h_both(A,C)|h_false_only(A,C)))))&(![A,B,C]: (sP4_prd(C,B,A)|(~g_true_only(A,B)|(~h_both(A,C)&~h_false_only(A,C)))))),
% 0.15/5.94 inference(miniscoping,[status(thm)],[f94])).
% 0.15/5.94 fof(f96,plain,(
% 0.15/5.94 ![X0,X1,X2]: (~sP4_prd(X0,X1,X2)|g_true_only(X2,X1))),
% 0.15/5.94 inference(cnf_transformation,[status(thm)],[f95])).
% 0.15/5.94 fof(f97,plain,(
% 0.15/5.94 ![X0,X1,X2]: (~sP4_prd(X0,X1,X2)|h_both(X2,X0)|h_false_only(X2,X0))),
% 0.15/5.94 inference(cnf_transformation,[status(thm)],[f95])).
% 0.15/5.94 fof(f100,plain,(
% 0.15/5.94 ![A]: ((~sP5_prd(A)|((![B]: ~g_true_only(A,B))|(((![B]: ~h_both(A,B))|(?[B]: h_true_only(A,B)))&(?[B]: ~h_false_only(A,B)))))&(sP5_prd(A)|((?[B]: g_true_only(A,B))&(((?[B]: h_both(A,B))&(![B]: ~h_true_only(A,B)))|(![B]: h_false_only(A,B))))))),
% 0.15/5.94 inference(NNF_transformation,[status(thm)],[f65])).
% 0.15/5.94 fof(f101,plain,(
% 0.15/5.94 (![A]: (~sP5_prd(A)|((![B]: ~g_true_only(A,B))|(((![B]: ~h_both(A,B))|(?[B]: h_true_only(A,B)))&(?[B]: ~h_false_only(A,B))))))&(![A]: (sP5_prd(A)|((?[B]: g_true_only(A,B))&(((?[B]: h_both(A,B))&(![B]: ~h_true_only(A,B)))|(![B]: h_false_only(A,B))))))),
% 0.15/5.94 inference(miniscoping,[status(thm)],[f100])).
% 0.15/5.94 fof(f102,plain,(
% 0.15/5.94 (![A]: (~sP5_prd(A)|((![B]: ~g_true_only(A,B))|(((![B]: ~h_both(A,B))|h_true_only(A,sK19_skl(A)))&~h_false_only(A,sK20_skl(A))))))&(![A]: (sP5_prd(A)|(g_true_only(A,sK21_skl(A))&((h_both(A,sK22_skl(A))&(![B]: ~h_true_only(A,B)))|(![B]: h_false_only(A,B))))))),
% 0.15/5.94 inference(skolemize,[status(esa),new_symbols(skolem,[sK19_skl,sK20_skl,sK21_skl,sK22_skl]),skolemize(B,sK19_skl(A)),skolemize(B,sK20_skl(A)),skolemize(B,sK21_skl(A)),skolemize(B,sK22_skl(A))],[f101])).
% 0.15/5.94 fof(f103,plain,(
% 0.15/5.94 ![X0,X1,X2]: (~sP5_prd(X0)|~g_true_only(X0,X1)|~h_both(X0,X2)|h_true_only(X0,sK19_skl(X0)))),
% 0.15/5.94 inference(cnf_transformation,[status(thm)],[f102])).
% 0.15/5.94 fof(f104,plain,(
% 0.15/5.94 ![X0,X1]: (~sP5_prd(X0)|~g_true_only(X0,X1)|~h_false_only(X0,sK20_skl(X0)))),
% 0.15/5.94 inference(cnf_transformation,[status(thm)],[f102])).
% 0.15/5.94 fof(f105,plain,(
% 0.15/5.94 ![X0]: (sP5_prd(X0)|g_true_only(X0,sK21_skl(X0)))),
% 0.15/5.94 inference(cnf_transformation,[status(thm)],[f102])).
% 0.15/5.94 fof(f107,plain,(
% 0.15/5.94 ![X0,X1,X2]: (sP5_prd(X0)|~h_true_only(X0,X1)|h_false_only(X0,X2))),
% 0.15/5.94 inference(cnf_transformation,[status(thm)],[f102])).
% 0.15/5.94 fof(f108,plain,(
% 0.15/5.94 ![A]: ((~sP6_prd(A)|((?[B]: g_true_only(A,B))&(((?[B]: h_both(A,B))&(![B]: ~h_true_only(A,B)))|(![B]: h_false_only(A,B)))))&(sP6_prd(A)|((![B]: ~g_true_only(A,B))|(((![B]: ~h_both(A,B))|(?[B]: h_true_only(A,B)))&(?[B]: ~h_false_only(A,B))))))),
% 0.15/5.94 inference(NNF_transformation,[status(thm)],[f75])).
% 0.15/5.94 fof(f109,plain,(
% 0.15/5.94 (![A]: (~sP6_prd(A)|((?[B]: g_true_only(A,B))&(((?[B]: h_both(A,B))&(![B]: ~h_true_only(A,B)))|(![B]: h_false_only(A,B))))))&(![A]: (sP6_prd(A)|((![B]: ~g_true_only(A,B))|(((![B]: ~h_both(A,B))|(?[B]: h_true_only(A,B)))&(?[B]: ~h_false_only(A,B))))))),
% 0.15/5.94 inference(miniscoping,[status(thm)],[f108])).
% 0.15/5.94 fof(f110,plain,(
% 0.15/5.94 (![A]: (~sP6_prd(A)|(g_true_only(A,sK23_skl(A))&((h_both(A,sK24_skl(A))&(![B]: ~h_true_only(A,B)))|(![B]: h_false_only(A,B))))))&(![A]: (sP6_prd(A)|((![B]: ~g_true_only(A,B))|(((![B]: ~h_both(A,B))|h_true_only(A,sK25_skl(A)))&~h_false_only(A,sK26_skl(A))))))),
% 0.15/5.94 inference(skolemize,[status(esa),new_symbols(skolem,[sK23_skl,sK24_skl,sK25_skl,sK26_skl]),skolemize(B,sK23_skl(A)),skolemize(B,sK24_skl(A)),skolemize(B,sK25_skl(A)),skolemize(B,sK26_skl(A))],[f109])).
% 0.15/5.94 fof(f111,plain,(
% 0.15/5.94 ![X0]: (~sP6_prd(X0)|g_true_only(X0,sK23_skl(X0)))),
% 0.15/5.94 inference(cnf_transformation,[status(thm)],[f110])).
% 0.15/5.94 fof(f112,plain,(
% 0.15/5.94 ![X0,X1]: (~sP6_prd(X0)|h_both(X0,sK24_skl(X0))|h_false_only(X0,X1))),
% 0.15/5.94 inference(cnf_transformation,[status(thm)],[f110])).
% 0.15/5.94 fof(f113,plain,(
% 0.15/5.94 ![X0,X1,X2]: (~sP6_prd(X0)|~h_true_only(X0,X1)|h_false_only(X0,X2))),
% 0.15/5.94 inference(cnf_transformation,[status(thm)],[f110])).
% 0.15/5.94 fof(f117,plain,(
% 0.15/5.94 sP0_prd(sK1_skl)|h_true_only(sK1_skl,sK12_skl(sK1_skl))|sP0_prd(sK0_skl)),
% 0.15/5.94 inference(resolution,[status(thm)],[f64,f20])).
% 0.15/5.94 fof(f119,plain,(
% 0.15/5.94 ![X0,X1]: (sP0_prd(X0)|h_true_only(X0,sK12_skl(X0))|g_false(X0,X1))),
% 0.15/5.94 inference(resolution,[status(thm)],[f64,f39])).
% 0.15/5.94 fof(f122,plain,(
% 0.15/5.94 sP0_prd(sK1_skl)|sP0_prd(sK0_skl)),
% 0.15/5.94 inference(forward_subsumption_resolution,[status(thm)],[f117,f21])).
% 0.15/5.94 fof(f123,plain,(
% 0.15/5.94 g_true_only(sK1_skl,sK2_skl)|g_both(sK1_skl,sK2_skl)|sP0_prd(sK0_skl)),
% 0.15/5.94 inference(resolution,[status(thm)],[f42,f20])).
% 0.15/5.94 fof(f124,plain,(
% 0.15/5.94 ![X0]: (g_true_only(X0,sK11_skl(X0))|g_both(X0,sK11_skl(X0))|~sP0_prd(X0))),
% 0.15/5.94 inference(resolution,[status(thm)],[f42,f62])).
% 0.15/5.94 fof(f127,plain,(
% 0.15/5.94 ![X0]: (h_both(sK1_skl,X0)|h_false_only(sK1_skl,X0)|sP0_prd(sK0_skl))),
% 0.15/5.94 inference(resolution,[status(thm)],[f58,f21])).
% 0.15/5.94 fof(f128,plain,(
% 0.15/5.94 ![X0,X1]: (h_both(X0,X1)|h_false_only(X0,X1)|~sP0_prd(X0))),
% 0.15/5.94 inference(resolution,[status(thm)],[f58,f63])).
% 0.15/5.94 fof(f132,plain,(
% 0.15/5.94 ![X0,X1,X2]: (sP5_prd(X0)|h_false_only(X0,X1)|h_both(X0,X2)|h_false_only(X0,X2))),
% 0.15/5.94 inference(resolution,[status(thm)],[f107,f58])).
% 0.15/5.94 fof(f150,plain,(
% 0.15/5.94 ![X0,X1]: (h_false_only(sK1_skl,X0)|sP0_prd(sK0_skl)|~sP5_prd(sK1_skl)|~g_true_only(sK1_skl,X1)|h_true_only(sK1_skl,sK19_skl(sK1_skl)))),
% 0.15/5.94 inference(resolution,[status(thm)],[f127,f103])).
% 0.15/5.94 fof(f156,plain,(
% 0.15/5.94 ![X0,X1]: (h_false_only(sK1_skl,X0)|sP0_prd(sK0_skl)|~sP5_prd(sK1_skl)|~g_true_only(sK1_skl,X1))),
% 0.15/5.94 inference(forward_subsumption_resolution,[status(thm)],[f150,f21])).
% 0.15/5.94 fof(f196,plain,(
% 0.15/5.94 ![X0,X1]: (sP0_prd(X0)|h_true_only(X0,sK12_skl(X0))|~g_true_only(X0,X1))),
% 0.15/5.94 inference(resolution,[status(thm)],[f119,f30])).
% 0.15/5.94 fof(f198,plain,(
% 0.15/5.94 ![X0,X1,X2,X3,X4,X5]: (g_true_only(sK1_skl,sK2_skl)|sP0_prd(sK0_skl)|g_true_only(sK1_skl,sK4_skl(sK1_skl))|~h_both(sK1_skl,X0)|h_true_only(sK1_skl,sK5_skl(sK1_skl))|sP2_prd(sK6_skl)|~g_both(X1,X2)|~h_both(X1,X3)|g_false_only(X1,X2)|h_true_only(X1,sK7_skl(X2,X1))|sP3_prd(X4,sK8_skl(X1),X1)|sP4_prd(X5,sK10_skl,sK9_skl)|h_false_only(sK9_skl,X5))),
% 0.15/5.94 inference(resolution,[status(thm)],[f123,f26])).
% 0.15/5.94 fof(f199,plain,(
% 0.15/5.94 ![X0,X1,X2,X3,X4,X5]: (g_true_only(sK1_skl,sK2_skl)|sP0_prd(sK0_skl)|g_true_only(sK1_skl,sK4_skl(sK1_skl))|~h_both(sK1_skl,X0)|h_true_only(sK1_skl,sK5_skl(sK1_skl))|sP2_prd(sK6_skl)|~g_both(X1,X2)|~h_both(X1,X3)|g_false_only(X1,X2)|h_true_only(X1,sK7_skl(X2,X1))|sP3_prd(X4,sK8_skl(X1),X1)|sP4_prd(X5,sK10_skl,sK9_skl)|g_both(sK9_skl,sK10_skl))),
% 0.15/5.94 inference(resolution,[status(thm)],[f123,f25])).
% 0.15/5.94 fof(f203,plain,(
% 0.15/5.94 ![X0,X1,X2,X3,X4,X5]: (g_true_only(sK1_skl,sK2_skl)|sP0_prd(sK0_skl)|g_true_only(sK1_skl,sK4_skl(sK1_skl))|~h_both(sK1_skl,X0)|sP2_prd(sK6_skl)|~g_both(X1,X2)|~h_both(X1,X3)|g_false_only(X1,X2)|h_true_only(X1,sK7_skl(X2,X1))|sP3_prd(X4,sK8_skl(X1),X1)|sP4_prd(X5,sK10_skl,sK9_skl)|h_false_only(sK9_skl,X5))),
% 0.15/5.94 inference(forward_subsumption_resolution,[status(thm)],[f198,f21])).
% 0.15/5.94 fof(f204,plain,(
% 0.15/5.94 ![X0,X1,X2,X3,X4,X5]: (g_true_only(sK1_skl,sK2_skl)|sP0_prd(sK0_skl)|g_true_only(sK1_skl,sK4_skl(sK1_skl))|~h_both(sK1_skl,X0)|sP2_prd(sK6_skl)|~g_both(X1,X2)|~h_both(X1,X3)|g_false_only(X1,X2)|h_true_only(X1,sK7_skl(X2,X1))|sP3_prd(X4,sK8_skl(X1),X1)|sP4_prd(X5,sK10_skl,sK9_skl)|g_both(sK9_skl,sK10_skl))),
% 0.15/5.94 inference(forward_subsumption_resolution,[status(thm)],[f199,f21])).
% 0.15/5.94 fof(f210,plain,(
% 0.15/5.94 g_true_only(sK1_skl,sK11_skl(sK1_skl))|g_both(sK1_skl,sK11_skl(sK1_skl))|sP0_prd(sK0_skl)),
% 0.15/5.94 inference(resolution,[status(thm)],[f124,f122])).
% 0.15/5.94 fof(f220,plain,(
% 0.15/5.94 ![X0,X1,X2,X3]: (sP5_prd(X0)|h_false_only(X0,X1)|h_false_only(X0,sK3_skl(X2,X0))|sP1_prd(X3)|~g_true_only(X0,X2))),
% 0.15/5.94 inference(resolution,[status(thm)],[f132,f22])).
% 0.15/5.94 fof(f227,plain,(
% 0.15/5.94 ![X0,X1,X2,X3]: (sP5_prd(X0)|h_false_only(X0,X1)|sP1_prd(X2)|~g_true_only(X0,X3))),
% 0.15/5.94 inference(forward_subsumption_resolution,[status(thm)],[f220,f23])).
% 0.15/5.94 fof(f427,plain,(
% 0.15/5.94 ![X0,X1,X2,X3,X4,X5]: (g_true_only(sK1_skl,sK2_skl)|sP0_prd(sK0_skl)|g_true_only(sK1_skl,sK4_skl(sK1_skl))|sP2_prd(sK6_skl)|~g_both(X0,X1)|~h_both(X0,X2)|g_false_only(X0,X1)|h_true_only(X0,sK7_skl(X1,X0))|sP3_prd(X3,sK8_skl(X0),X0)|sP4_prd(X4,sK10_skl,sK9_skl)|h_false_only(sK9_skl,X4)|h_false_only(sK1_skl,X5)|sP0_prd(sK0_skl))),
% 0.15/5.94 inference(resolution,[status(thm)],[f203,f127])).
% 0.15/5.94 fof(f431,plain,(
% 0.15/5.94 ![X0,X1,X2,X3,X4,X5]: (g_true_only(sK1_skl,sK2_skl)|sP0_prd(sK0_skl)|g_true_only(sK1_skl,sK4_skl(sK1_skl))|sP2_prd(sK6_skl)|~g_both(X0,X1)|~h_both(X0,X2)|g_false_only(X0,X1)|h_true_only(X0,sK7_skl(X1,X0))|sP3_prd(X3,sK8_skl(X0),X0)|sP4_prd(X4,sK10_skl,sK9_skl)|h_false_only(sK9_skl,X4)|h_false_only(sK1_skl,X5))),
% 0.15/5.94 inference(duplicate_literals_removal,[status(thm)],[f427])).
% 0.15/5.94 fof(f440,plain,(
% 0.15/5.94 ![X0,X1,X2,X3,X4,X5]: (g_true_only(sK1_skl,sK2_skl)|sP0_prd(sK0_skl)|g_true_only(sK1_skl,sK4_skl(sK1_skl))|sP2_prd(sK6_skl)|~g_both(X0,X1)|~h_both(X0,X2)|g_false_only(X0,X1)|h_true_only(X0,sK7_skl(X1,X0))|sP3_prd(X3,sK8_skl(X0),X0)|sP4_prd(X4,sK10_skl,sK9_skl)|g_both(sK9_skl,sK10_skl)|h_false_only(sK1_skl,X5)|sP0_prd(sK0_skl))),
% 0.15/5.94 inference(resolution,[status(thm)],[f204,f127])).
% 0.15/5.94 fof(f444,plain,(
% 0.15/5.94 ![X0,X1,X2,X3,X4,X5]: (g_true_only(sK1_skl,sK2_skl)|sP0_prd(sK0_skl)|g_true_only(sK1_skl,sK4_skl(sK1_skl))|sP2_prd(sK6_skl)|~g_both(X0,X1)|~h_both(X0,X2)|g_false_only(X0,X1)|h_true_only(X0,sK7_skl(X1,X0))|sP3_prd(X3,sK8_skl(X0),X0)|sP4_prd(X4,sK10_skl,sK9_skl)|g_both(sK9_skl,sK10_skl)|h_false_only(sK1_skl,X5))),
% 0.15/5.94 inference(duplicate_literals_removal,[status(thm)],[f440])).
% 0.15/5.94 fof(f451,plain,(
% 0.15/5.94 g_true_only(sK1_skl,sK11_skl(sK1_skl))|sP0_prd(sK0_skl)|g_true(sK1_skl,sK11_skl(sK1_skl))),
% 0.15/5.94 inference(resolution,[status(thm)],[f210,f34])).
% 0.15/5.94 fof(f455,plain,(
% 0.15/5.94 sP0_prd(sK0_skl)|g_true(sK1_skl,sK11_skl(sK1_skl))),
% 0.15/5.94 inference(forward_subsumption_resolution,[status(thm)],[f451,f29])).
% 0.15/5.94 fof(f458,plain,(
% 0.15/5.94 sP0_prd(sK0_skl)|~g_false_only(sK1_skl,sK11_skl(sK1_skl))),
% 0.15/5.94 inference(resolution,[status(thm)],[f455,f40])).
% 0.15/5.94 fof(f541,plain,(
% 0.15/5.94 ![X0,X1,X2]: (sP5_prd(X0)|h_false_only(X0,X1)|sP1_prd(X2)|sP5_prd(X0))),
% 0.15/5.94 inference(resolution,[status(thm)],[f227,f105])).
% 0.15/5.94 fof(f542,plain,(
% 0.15/5.94 ![X0,X1,X2]: (sP5_prd(X0)|h_false_only(X0,X1)|sP1_prd(X2))),
% 0.15/5.94 inference(duplicate_literals_removal,[status(thm)],[f541])).
% 0.15/5.94 fof(f851,plain,(
% 0.15/5.94 ![X0,X1]: (sP1_prd(X0)|h_false_only(X0,X1))),
% 0.15/5.94 inference(backward_subsumption_resolution,[status(thm)],[f74,f542])).
% 0.15/5.94 fof(f870,plain,(
% 0.15/5.94 ![X0,X1,X2]: (sP1_prd(X0)|sP1_prd(X1)|~g_both(X0,X2))),
% 0.15/5.94 inference(resolution,[status(thm)],[f851,f24])).
% 0.15/5.94 fof(f871,plain,(
% 0.15/5.94 ![X0,X1,X2]: (sP1_prd(X0)|sP1_prd(X1)|~g_true_only(X0,X2))),
% 0.15/5.94 inference(resolution,[status(thm)],[f851,f23])).
% 0.15/5.94 fof(f907,plain,(
% 0.15/5.94 ![X0,X1]: (sP1_prd(X0)|sP1_prd(X1)|sP5_prd(X0))),
% 0.15/5.94 inference(resolution,[status(thm)],[f871,f105])).
% 0.15/5.94 fof(f908,plain,(
% 0.15/5.94 ![X0,X1]: (sP1_prd(X0)|sP5_prd(X1))),
% 0.15/5.94 inference(forward_subsumption_resolution,[status(thm)],[f907,f70])).
% 0.15/5.94 fof(f1082,plain,(
% 0.15/5.94 ![X0]: (sP5_prd(X0))),
% 0.15/5.94 inference(backward_subsumption_resolution,[status(thm)],[f70,f908])).
% 0.15/5.94 fof(f1084,plain,(
% 0.15/5.94 ![X0]: (sP1_prd(X0)|g_both(X0,sK15_skl(X0)))),
% 0.15/5.94 inference(backward_subsumption_resolution,[status(thm)],[f72,f908])).
% 0.15/5.94 fof(f1085,plain,(
% 0.15/5.94 ![X0,X1]: (h_false_only(sK1_skl,X0)|sP0_prd(sK0_skl)|~g_true_only(sK1_skl,X1))),
% 0.15/5.94 inference(backward_subsumption_resolution,[status(thm)],[f156,f1082])).
% 0.15/5.94 fof(f1086,plain,(
% 0.15/5.94 ![X0,X1]: (~g_true_only(X0,X1)|~h_false_only(X0,sK20_skl(X0)))),
% 0.15/5.94 inference(backward_subsumption_resolution,[status(thm)],[f104,f1082])).
% 0.15/5.94 fof(f1087,plain,(
% 0.15/5.94 ![X0,X1,X2]: (~g_true_only(X0,X1)|~h_both(X0,X2)|h_true_only(X0,sK19_skl(X0)))),
% 0.15/5.94 inference(backward_subsumption_resolution,[status(thm)],[f103,f1082])).
% 0.15/5.94 fof(f1095,plain,(
% 0.15/5.94 ![X0,X1]: (sP1_prd(X0)|sP1_prd(X0)|sP1_prd(X1))),
% 0.15/5.94 inference(resolution,[status(thm)],[f1084,f870])).
% 0.15/5.94 fof(f1101,plain,(
% 0.15/5.94 ![X0,X1]: (sP1_prd(X0)|sP1_prd(X1))),
% 0.15/5.94 inference(duplicate_literals_removal,[status(thm)],[f1095])).
% 0.15/5.94 fof(f1141,plain,(
% 0.15/5.94 ![X0]: (sP1_prd(X0))),
% 0.15/5.94 inference(factoring,[status(thm)],[f1101])).
% 0.15/5.94 fof(f1144,plain,(
% 0.15/5.94 ![X0,X1]: (~g_both(X0,X1)|g_true_only(X0,sK13_skl(X0))|~h_false_only(X0,sK14_skl(X0)))),
% 0.15/5.94 inference(backward_subsumption_resolution,[status(thm)],[f71,f1141])).
% 0.15/5.94 fof(f1148,plain,(
% 0.15/5.94 ![X0,X1,X2,X3,X4,X5]: (sP0_prd(sK0_skl)|g_true_only(sK1_skl,sK4_skl(sK1_skl))|sP2_prd(sK6_skl)|~g_both(X0,X1)|~h_both(X0,X2)|g_false_only(X0,X1)|h_true_only(X0,sK7_skl(X1,X0))|sP3_prd(X3,sK8_skl(X0),X0)|sP4_prd(X4,sK10_skl,sK9_skl)|h_false_only(sK9_skl,X4)|h_false_only(sK1_skl,X5))),
% 0.15/5.94 inference(forward_subsumption_resolution,[status(thm)],[f431,f1085])).
% 0.15/5.94 fof(f1150,plain,(
% 0.15/5.94 ![X0,X1,X2,X3]: (sP0_prd(sK0_skl)|g_true_only(sK1_skl,sK4_skl(sK1_skl))|sP2_prd(sK6_skl)|~h_both(sK1_skl,X0)|g_false_only(sK1_skl,sK2_skl)|h_true_only(sK1_skl,sK7_skl(sK2_skl,sK1_skl))|sP3_prd(X1,sK8_skl(sK1_skl),sK1_skl)|sP4_prd(X2,sK10_skl,sK9_skl)|h_false_only(sK9_skl,X2)|h_false_only(sK1_skl,X3)|g_true_only(sK1_skl,sK2_skl)|sP0_prd(sK0_skl))),
% 0.15/5.94 inference(resolution,[status(thm)],[f1148,f123])).
% 0.15/5.94 fof(f1153,plain,(
% 0.15/5.94 ![X0,X1,X2,X3]: (sP0_prd(sK0_skl)|g_true_only(sK1_skl,sK4_skl(sK1_skl))|sP2_prd(sK6_skl)|~h_both(sK1_skl,X0)|g_false_only(sK1_skl,sK2_skl)|h_true_only(sK1_skl,sK7_skl(sK2_skl,sK1_skl))|sP3_prd(X1,sK8_skl(sK1_skl),sK1_skl)|sP4_prd(X2,sK10_skl,sK9_skl)|h_false_only(sK9_skl,X2)|h_false_only(sK1_skl,X3)|g_true_only(sK1_skl,sK2_skl))),
% 0.15/5.94 inference(duplicate_literals_removal,[status(thm)],[f1150])).
% 0.15/5.94 fof(f1154,plain,(
% 0.15/5.94 ![X0,X1,X2,X3]: (sP0_prd(sK0_skl)|sP2_prd(sK6_skl)|~h_both(sK1_skl,X0)|g_false_only(sK1_skl,sK2_skl)|h_true_only(sK1_skl,sK7_skl(sK2_skl,sK1_skl))|sP3_prd(X1,sK8_skl(sK1_skl),sK1_skl)|sP4_prd(X2,sK10_skl,sK9_skl)|h_false_only(sK9_skl,X2)|h_false_only(sK1_skl,X3)|g_true_only(sK1_skl,sK2_skl))),
% 0.15/5.94 inference(forward_subsumption_resolution,[status(thm)],[f1153,f1085])).
% 0.15/5.94 fof(f1155,plain,(
% 0.15/5.94 ![X0,X1,X2,X3,X4,X5]: (sP0_prd(sK0_skl)|g_true_only(sK1_skl,sK4_skl(sK1_skl))|sP2_prd(sK6_skl)|~g_both(X0,X1)|~h_both(X0,X2)|g_false_only(X0,X1)|h_true_only(X0,sK7_skl(X1,X0))|sP3_prd(X3,sK8_skl(X0),X0)|sP4_prd(X4,sK10_skl,sK9_skl)|g_both(sK9_skl,sK10_skl)|h_false_only(sK1_skl,X5))),
% 0.15/5.94 inference(forward_subsumption_resolution,[status(thm)],[f444,f1085])).
% 0.15/5.94 fof(f1156,plain,(
% 0.15/5.94 ![X0,X1,X2,X3]: (sP0_prd(sK0_skl)|g_true_only(sK1_skl,sK4_skl(sK1_skl))|sP2_prd(sK6_skl)|~h_both(sK1_skl,X0)|g_false_only(sK1_skl,sK11_skl(sK1_skl))|h_true_only(sK1_skl,sK7_skl(sK11_skl(sK1_skl),sK1_skl))|sP3_prd(X1,sK8_skl(sK1_skl),sK1_skl)|sP4_prd(X2,sK10_skl,sK9_skl)|g_both(sK9_skl,sK10_skl)|h_false_only(sK1_skl,X3)|g_true_only(sK1_skl,sK11_skl(sK1_skl))|sP0_prd(sK0_skl))),
% 0.15/5.94 inference(resolution,[status(thm)],[f1155,f210])).
% 0.15/5.94 fof(f1158,plain,(
% 0.15/5.94 ![X0,X1,X2,X3]: (sP0_prd(sK0_skl)|g_true_only(sK1_skl,sK4_skl(sK1_skl))|sP2_prd(sK6_skl)|~h_both(sK1_skl,X0)|g_false_only(sK1_skl,sK11_skl(sK1_skl))|h_true_only(sK1_skl,sK7_skl(sK11_skl(sK1_skl),sK1_skl))|sP3_prd(X1,sK8_skl(sK1_skl),sK1_skl)|sP4_prd(X2,sK10_skl,sK9_skl)|g_both(sK9_skl,sK10_skl)|h_false_only(sK1_skl,X3)|g_true_only(sK1_skl,sK11_skl(sK1_skl)))),
% 0.15/5.94 inference(duplicate_literals_removal,[status(thm)],[f1156])).
% 0.15/5.94 fof(f1159,plain,(
% 0.15/5.94 ![X0,X1,X2,X3]: (sP0_prd(sK0_skl)|sP2_prd(sK6_skl)|~h_both(sK1_skl,X0)|g_false_only(sK1_skl,sK11_skl(sK1_skl))|h_true_only(sK1_skl,sK7_skl(sK11_skl(sK1_skl),sK1_skl))|sP3_prd(X1,sK8_skl(sK1_skl),sK1_skl)|sP4_prd(X2,sK10_skl,sK9_skl)|g_both(sK9_skl,sK10_skl)|h_false_only(sK1_skl,X3)|g_true_only(sK1_skl,sK11_skl(sK1_skl)))),
% 0.15/5.94 inference(forward_subsumption_resolution,[status(thm)],[f1158,f1085])).
% 0.15/5.94 fof(f1170,plain,(
% 0.15/5.94 ![X0,X1,X2,X3]: (sP0_prd(sK0_skl)|sP2_prd(sK6_skl)|~h_both(sK1_skl,X0)|h_true_only(sK1_skl,sK7_skl(sK2_skl,sK1_skl))|sP3_prd(X1,sK8_skl(sK1_skl),sK1_skl)|sP4_prd(X2,sK10_skl,sK9_skl)|h_false_only(sK9_skl,X2)|h_false_only(sK1_skl,X3)|g_true_only(sK1_skl,sK2_skl))),
% 0.15/5.94 inference(forward_subsumption_resolution,[status(thm)],[f1154,f20])).
% 0.15/5.94 fof(f1171,plain,(
% 0.15/5.94 ![X0,X1,X2,X3]: (sP0_prd(sK0_skl)|sP2_prd(sK6_skl)|h_true_only(sK1_skl,sK7_skl(sK2_skl,sK1_skl))|sP3_prd(X0,sK8_skl(sK1_skl),sK1_skl)|sP4_prd(X1,sK10_skl,sK9_skl)|h_false_only(sK9_skl,X1)|h_false_only(sK1_skl,X2)|g_true_only(sK1_skl,sK2_skl)|h_false_only(sK1_skl,X3)|sP0_prd(sK0_skl))),
% 0.15/5.94 inference(resolution,[status(thm)],[f1170,f127])).
% 0.15/5.94 fof(f1172,plain,(
% 0.15/5.94 ![X0,X1,X2,X3]: (sP0_prd(sK0_skl)|sP2_prd(sK6_skl)|h_true_only(sK1_skl,sK7_skl(sK2_skl,sK1_skl))|sP3_prd(X0,sK8_skl(sK1_skl),sK1_skl)|sP4_prd(X1,sK10_skl,sK9_skl)|h_false_only(sK9_skl,X1)|h_false_only(sK1_skl,X2)|g_true_only(sK1_skl,sK2_skl)|h_false_only(sK1_skl,X3))),
% 0.15/5.94 inference(duplicate_literals_removal,[status(thm)],[f1171])).
% 0.15/5.94 fof(f1173,plain,(
% 0.15/5.94 ![X0,X1,X2,X3]: (sP0_prd(sK0_skl)|sP2_prd(sK6_skl)|sP3_prd(X0,sK8_skl(sK1_skl),sK1_skl)|sP4_prd(X1,sK10_skl,sK9_skl)|h_false_only(sK9_skl,X1)|h_false_only(sK1_skl,X2)|g_true_only(sK1_skl,sK2_skl)|h_false_only(sK1_skl,X3))),
% 0.15/5.94 inference(forward_subsumption_resolution,[status(thm)],[f1172,f21])).
% 0.15/5.94 fof(f1174,plain,(
% 0.15/5.94 ![X0,X1,X2,X3]: (sP0_prd(sK0_skl)|sP2_prd(sK6_skl)|~h_both(sK1_skl,X0)|h_true_only(sK1_skl,sK7_skl(sK11_skl(sK1_skl),sK1_skl))|sP3_prd(X1,sK8_skl(sK1_skl),sK1_skl)|sP4_prd(X2,sK10_skl,sK9_skl)|g_both(sK9_skl,sK10_skl)|h_false_only(sK1_skl,X3)|g_true_only(sK1_skl,sK11_skl(sK1_skl)))),
% 0.15/5.94 inference(forward_subsumption_resolution,[status(thm)],[f1159,f458])).
% 0.15/5.94 fof(f1175,plain,(
% 0.15/5.94 ![X0,X1,X2,X3]: (sP0_prd(sK0_skl)|sP2_prd(sK6_skl)|h_true_only(sK1_skl,sK7_skl(sK11_skl(sK1_skl),sK1_skl))|sP3_prd(X0,sK8_skl(sK1_skl),sK1_skl)|sP4_prd(X1,sK10_skl,sK9_skl)|g_both(sK9_skl,sK10_skl)|h_false_only(sK1_skl,X2)|g_true_only(sK1_skl,sK11_skl(sK1_skl))|h_false_only(sK1_skl,X3)|sP0_prd(sK0_skl))),
% 0.15/5.94 inference(resolution,[status(thm)],[f1174,f127])).
% 0.15/5.94 fof(f1176,plain,(
% 0.15/5.94 ![X0,X1,X2,X3]: (sP0_prd(sK0_skl)|sP2_prd(sK6_skl)|h_true_only(sK1_skl,sK7_skl(sK11_skl(sK1_skl),sK1_skl))|sP3_prd(X0,sK8_skl(sK1_skl),sK1_skl)|sP4_prd(X1,sK10_skl,sK9_skl)|g_both(sK9_skl,sK10_skl)|h_false_only(sK1_skl,X2)|g_true_only(sK1_skl,sK11_skl(sK1_skl))|h_false_only(sK1_skl,X3))),
% 0.15/5.94 inference(duplicate_literals_removal,[status(thm)],[f1175])).
% 0.15/5.94 fof(f1177,plain,(
% 0.15/5.94 ![X0,X1,X2,X3]: (sP0_prd(sK0_skl)|sP2_prd(sK6_skl)|sP3_prd(X0,sK8_skl(sK1_skl),sK1_skl)|sP4_prd(X1,sK10_skl,sK9_skl)|g_both(sK9_skl,sK10_skl)|h_false_only(sK1_skl,X2)|g_true_only(sK1_skl,sK11_skl(sK1_skl))|h_false_only(sK1_skl,X3))),
% 0.15/5.94 inference(forward_subsumption_resolution,[status(thm)],[f1176,f21])).
% 0.15/5.94 fof(f1182,plain,(
% 0.15/5.94 ![X0,X1,X2,X3]: (sP0_prd(sK0_skl)|sP2_prd(sK6_skl)|sP3_prd(X0,sK8_skl(sK1_skl),sK1_skl)|sP4_prd(X1,sK10_skl,sK9_skl)|h_false_only(sK9_skl,X1)|h_false_only(sK1_skl,X2)|h_false_only(sK1_skl,X3))),
% 0.15/5.94 inference(forward_subsumption_resolution,[status(thm)],[f1173,f1085])).
% 0.15/5.94 fof(f1184,plain,(
% 0.15/5.94 ![X0,X1,X2,X3]: (sP0_prd(sK0_skl)|sP2_prd(sK6_skl)|sP4_prd(X0,sK10_skl,sK9_skl)|h_false_only(sK9_skl,X0)|h_false_only(sK1_skl,X1)|h_false_only(sK1_skl,X2)|g_true_only(sK1_skl,sK8_skl(sK1_skl))|h_false_only(sK1_skl,X3))),
% 0.15/5.94 inference(resolution,[status(thm)],[f1182,f88])).
% 0.15/5.94 fof(f1222,plain,(
% 0.15/5.94 ![X0,X1,X2,X3]: (sP0_prd(sK0_skl)|sP2_prd(sK6_skl)|sP4_prd(X0,sK10_skl,sK9_skl)|h_false_only(sK9_skl,X0)|h_false_only(sK1_skl,X1)|h_false_only(sK1_skl,X2)|h_false_only(sK1_skl,X3))),
% 0.15/5.94 inference(forward_subsumption_resolution,[status(thm)],[f1184,f1085])).
% 0.15/5.94 fof(f1243,plain,(
% 0.15/5.94 ![X0,X1]: (sP0_prd(sK0_skl)|sP2_prd(sK6_skl)|sP4_prd(X0,sK10_skl,sK9_skl)|h_false_only(sK9_skl,X0)|~g_true_only(sK1_skl,X1))),
% 0.15/5.94 inference(resolution,[status(thm)],[f1222,f1086])).
% 0.15/5.94 fof(f1292,plain,(
% 0.15/5.94 ![X0,X1]: (sP0_prd(sK0_skl)|sP2_prd(sK6_skl)|sP4_prd(X0,sK10_skl,sK9_skl)|h_false_only(sK9_skl,X0)|h_false_only(sK1_skl,X1))),
% 0.15/5.94 inference(factoring,[status(thm)],[f1222])).
% 0.15/5.94 fof(f1325,plain,(
% 0.15/5.94 ![X0,X1]: (sP0_prd(sK0_skl)|sP2_prd(sK6_skl)|sP4_prd(X0,sK10_skl,sK9_skl)|h_false_only(sK9_skl,X0)|~g_both(sK1_skl,X1)|g_true_only(sK1_skl,sK13_skl(sK1_skl)))),
% 0.15/5.94 inference(resolution,[status(thm)],[f1292,f1144])).
% 0.15/5.94 fof(f1337,plain,(
% 0.15/5.94 ![X0,X1]: (sP0_prd(sK0_skl)|sP2_prd(sK6_skl)|sP4_prd(X0,sK10_skl,sK9_skl)|h_false_only(sK9_skl,X0)|~g_both(sK1_skl,X1))),
% 0.15/5.94 inference(forward_subsumption_resolution,[status(thm)],[f1325,f1243])).
% 0.15/5.94 fof(f1444,plain,(
% 0.15/5.94 ![X0,X1,X2,X3]: (sP0_prd(sK0_skl)|sP2_prd(sK6_skl)|sP3_prd(X0,sK8_skl(sK1_skl),sK1_skl)|sP4_prd(X1,sK10_skl,sK9_skl)|g_both(sK9_skl,sK10_skl)|h_false_only(sK1_skl,X2)|h_false_only(sK1_skl,X3))),
% 0.15/5.94 inference(forward_subsumption_resolution,[status(thm)],[f1177,f1085])).
% 0.15/5.94 fof(f1506,plain,(
% 0.15/5.94 ![X0]: (sP0_prd(sK0_skl)|sP2_prd(sK6_skl)|sP4_prd(X0,sK10_skl,sK9_skl)|h_false_only(sK9_skl,X0)|g_true_only(sK1_skl,sK11_skl(sK1_skl))|sP0_prd(sK0_skl))),
% 0.15/5.94 inference(resolution,[status(thm)],[f1337,f210])).
% 0.15/5.94 fof(f1508,plain,(
% 0.15/5.94 ![X0]: (sP0_prd(sK0_skl)|sP2_prd(sK6_skl)|sP4_prd(X0,sK10_skl,sK9_skl)|h_false_only(sK9_skl,X0)|g_true_only(sK1_skl,sK11_skl(sK1_skl)))),
% 0.15/5.94 inference(duplicate_literals_removal,[status(thm)],[f1506])).
% 0.15/5.94 fof(f1509,plain,(
% 0.15/5.94 ![X0]: (sP0_prd(sK0_skl)|sP2_prd(sK6_skl)|sP4_prd(X0,sK10_skl,sK9_skl)|h_false_only(sK9_skl,X0))),
% 0.15/5.94 inference(forward_subsumption_resolution,[status(thm)],[f1508,f1243])).
% 0.15/5.94 fof(f1512,plain,(
% 0.15/5.94 ![X0]: (sP0_prd(sK0_skl)|sP2_prd(sK6_skl)|h_false_only(sK9_skl,X0)|h_both(sK9_skl,X0)|h_false_only(sK9_skl,X0))),
% 0.15/5.94 inference(resolution,[status(thm)],[f1509,f97])).
% 0.15/5.94 fof(f1513,plain,(
% 0.15/5.94 ![X0]: (sP0_prd(sK0_skl)|sP2_prd(sK6_skl)|h_false_only(sK9_skl,X0)|g_true_only(sK9_skl,sK10_skl))),
% 0.15/5.94 inference(resolution,[status(thm)],[f1509,f96])).
% 0.15/5.94 fof(f1514,plain,(
% 0.15/5.94 ![X0]: (sP0_prd(sK0_skl)|sP2_prd(sK6_skl)|h_false_only(sK9_skl,X0)|h_both(sK9_skl,X0))),
% 0.15/5.94 inference(duplicate_literals_removal,[status(thm)],[f1512])).
% 0.15/5.94 fof(f1515,plain,(
% 0.15/5.94 ![X0,X1]: (sP0_prd(sK0_skl)|sP2_prd(sK6_skl)|h_false_only(sK9_skl,X0)|~g_true_only(sK9_skl,X1)|h_true_only(sK9_skl,sK19_skl(sK9_skl)))),
% 0.15/5.94 inference(resolution,[status(thm)],[f1514,f1087])).
% 0.15/5.94 fof(f1519,plain,(
% 0.15/5.94 ![X0]: (sP0_prd(sK0_skl)|sP2_prd(sK6_skl)|h_false_only(sK9_skl,X0)|h_false(sK9_skl,X0))),
% 0.15/5.94 inference(resolution,[status(thm)],[f1514,f51])).
% 0.15/5.94 fof(f1523,plain,(
% 0.15/5.94 ![X0]: (sP0_prd(sK0_skl)|sP2_prd(sK6_skl)|h_false(sK9_skl,X0))),
% 0.15/5.94 inference(forward_subsumption_resolution,[status(thm)],[f1519,f55])).
% 0.15/5.94 fof(f1525,plain,(
% 0.15/5.94 ![X0]: (sP0_prd(sK0_skl)|sP2_prd(sK6_skl)|~h_true_only(sK9_skl,X0))),
% 0.15/5.94 inference(resolution,[status(thm)],[f1523,f46])).
% 0.15/5.94 fof(f1546,plain,(
% 0.15/5.94 ![X0]: (sP0_prd(sK0_skl)|sP2_prd(sK6_skl)|h_false_only(sK9_skl,X0))),
% 0.15/5.94 inference(backward_subsumption_resolution,[status(thm)],[f1513,f1547])).
% 0.15/5.94 fof(f1547,plain,(
% 0.15/5.94 ![X0,X1]: (sP0_prd(sK0_skl)|sP2_prd(sK6_skl)|h_false_only(sK9_skl,X0)|~g_true_only(sK9_skl,X1))),
% 0.15/5.94 inference(forward_subsumption_resolution,[status(thm)],[f1515,f1525])).
% 0.15/5.94 fof(f1548,plain,(
% 0.15/5.94 ![X0]: (sP0_prd(sK0_skl)|sP2_prd(sK6_skl)|~g_both(sK9_skl,X0)|g_true_only(sK9_skl,sK13_skl(sK9_skl)))),
% 0.15/5.94 inference(resolution,[status(thm)],[f1546,f1144])).
% 0.15/5.94 fof(f1549,plain,(
% 0.15/5.94 ![X0]: (sP0_prd(sK0_skl)|sP2_prd(sK6_skl)|~g_true_only(sK9_skl,X0))),
% 0.15/5.94 inference(resolution,[status(thm)],[f1546,f1086])).
% 0.15/5.94 fof(f1557,plain,(
% 0.15/5.94 ![X0,X1,X2,X3]: (sP0_prd(sK0_skl)|sP2_prd(sK6_skl)|sP3_prd(X0,sK8_skl(sK1_skl),sK1_skl)|sP4_prd(X1,sK10_skl,sK9_skl)|h_false_only(sK1_skl,X2)|h_false_only(sK1_skl,X3))),
% 0.15/5.94 inference(backward_subsumption_resolution,[status(thm)],[f1444,f1564])).
% 0.15/5.94 fof(f1564,plain,(
% 0.15/5.94 ![X0]: (sP0_prd(sK0_skl)|sP2_prd(sK6_skl)|~g_both(sK9_skl,X0))),
% 0.15/5.94 inference(forward_subsumption_resolution,[status(thm)],[f1548,f1549])).
% 0.15/5.94 fof(f1585,plain,(
% 0.15/5.94 ![X0,X1,X2,X3]: (sP0_prd(sK0_skl)|sP2_prd(sK6_skl)|sP4_prd(X0,sK10_skl,sK9_skl)|h_false_only(sK1_skl,X1)|h_false_only(sK1_skl,X2)|g_true_only(sK1_skl,sK8_skl(sK1_skl))|h_false_only(sK1_skl,X3))),
% 0.15/5.94 inference(resolution,[status(thm)],[f1557,f88])).
% 0.15/5.94 fof(f1623,plain,(
% 0.15/5.94 ![X0,X1,X2,X3]: (sP0_prd(sK0_skl)|sP2_prd(sK6_skl)|sP4_prd(X0,sK10_skl,sK9_skl)|h_false_only(sK1_skl,X1)|h_false_only(sK1_skl,X2)|h_false_only(sK1_skl,X3))),
% 0.15/5.94 inference(forward_subsumption_resolution,[status(thm)],[f1585,f1085])).
% 0.15/5.94 fof(f1644,plain,(
% 0.15/5.94 ![X0,X1]: (sP0_prd(sK0_skl)|sP2_prd(sK6_skl)|sP4_prd(X0,sK10_skl,sK9_skl)|~g_true_only(sK1_skl,X1))),
% 0.15/5.94 inference(resolution,[status(thm)],[f1623,f1086])).
% 0.15/5.94 fof(f1693,plain,(
% 0.15/5.94 ![X0,X1]: (sP0_prd(sK0_skl)|sP2_prd(sK6_skl)|sP4_prd(X0,sK10_skl,sK9_skl)|h_false_only(sK1_skl,X1))),
% 0.15/5.94 inference(factoring,[status(thm)],[f1623])).
% 0.15/5.94 fof(f1718,plain,(
% 0.15/5.94 ![X0]: (sP0_prd(sK0_skl)|sP2_prd(sK6_skl)|h_false_only(sK1_skl,X0)|g_true_only(sK9_skl,sK10_skl))),
% 0.15/5.94 inference(resolution,[status(thm)],[f1693,f96])).
% 0.15/5.94 fof(f1721,plain,(
% 0.15/5.94 ![X0,X1]: (sP0_prd(sK0_skl)|sP2_prd(sK6_skl)|sP4_prd(X0,sK10_skl,sK9_skl)|~g_both(sK1_skl,X1)|g_true_only(sK1_skl,sK13_skl(sK1_skl)))),
% 0.15/5.94 inference(resolution,[status(thm)],[f1693,f1144])).
% 0.15/5.94 fof(f1730,plain,(
% 0.15/5.94 ![X0]: (sP0_prd(sK0_skl)|sP2_prd(sK6_skl)|h_false_only(sK1_skl,X0))),
% 0.15/5.94 inference(forward_subsumption_resolution,[status(thm)],[f1718,f1549])).
% 0.15/5.94 fof(f1733,plain,(
% 0.15/5.94 ![X0,X1]: (sP0_prd(sK0_skl)|sP2_prd(sK6_skl)|sP4_prd(X0,sK10_skl,sK9_skl)|~g_both(sK1_skl,X1))),
% 0.15/5.94 inference(forward_subsumption_resolution,[status(thm)],[f1721,f1644])).
% 0.15/5.94 fof(f1740,plain,(
% 0.15/5.94 ![X0]: (sP0_prd(sK0_skl)|sP2_prd(sK6_skl)|~g_true_only(sK1_skl,X0))),
% 0.15/5.94 inference(resolution,[status(thm)],[f1730,f1086])).
% 0.15/5.94 fof(f1753,plain,(
% 0.15/5.94 ![X0]: (sP0_prd(sK0_skl)|sP2_prd(sK6_skl)|sP4_prd(X0,sK10_skl,sK9_skl)|g_true_only(sK1_skl,sK11_skl(sK1_skl))|sP0_prd(sK0_skl))),
% 0.15/5.94 inference(resolution,[status(thm)],[f1733,f210])).
% 0.15/5.94 fof(f1755,plain,(
% 0.15/5.94 ![X0]: (sP0_prd(sK0_skl)|sP2_prd(sK6_skl)|sP4_prd(X0,sK10_skl,sK9_skl)|g_true_only(sK1_skl,sK11_skl(sK1_skl)))),
% 0.15/5.94 inference(duplicate_literals_removal,[status(thm)],[f1753])).
% 0.15/5.94 fof(f1756,plain,(
% 0.15/5.94 ![X0]: (sP0_prd(sK0_skl)|sP2_prd(sK6_skl)|sP4_prd(X0,sK10_skl,sK9_skl))),
% 0.15/5.94 inference(forward_subsumption_resolution,[status(thm)],[f1755,f1740])).
% 0.15/5.94 fof(f1760,plain,(
% 0.15/5.94 sP0_prd(sK0_skl)|sP2_prd(sK6_skl)|g_true_only(sK9_skl,sK10_skl)),
% 0.15/5.94 inference(resolution,[status(thm)],[f1756,f96])).
% 0.15/5.94 fof(f1761,plain,(
% 0.15/5.94 sP0_prd(sK0_skl)|sP2_prd(sK6_skl)),
% 0.15/5.94 inference(forward_subsumption_resolution,[status(thm)],[f1760,f1549])).
% 0.15/5.94 fof(f1762,plain,(
% 0.15/5.94 sP2_prd(sK6_skl)|g_true_only(sK0_skl,sK11_skl(sK0_skl))|g_both(sK0_skl,sK11_skl(sK0_skl))),
% 0.15/5.94 inference(resolution,[status(thm)],[f1761,f124])).
% 0.15/5.94 fof(f1763,plain,(
% 0.15/5.94 ![X0]: (sP2_prd(sK6_skl)|h_both(sK0_skl,X0)|h_false_only(sK0_skl,X0))),
% 0.15/5.94 inference(resolution,[status(thm)],[f1761,f128])).
% 0.15/5.94 fof(f1764,plain,(
% 0.15/5.94 ![X0,X1]: (sP2_prd(sK6_skl)|h_false_only(sK0_skl,X0)|~g_true_only(sK0_skl,X1)|h_true_only(sK0_skl,sK19_skl(sK0_skl)))),
% 0.15/5.94 inference(resolution,[status(thm)],[f1763,f1087])).
% 0.15/5.94 fof(f1768,plain,(
% 0.15/5.94 ![X0]: (sP2_prd(sK6_skl)|h_false_only(sK0_skl,X0)|h_false(sK0_skl,X0))),
% 0.15/5.94 inference(resolution,[status(thm)],[f1763,f51])).
% 0.15/5.94 fof(f1772,plain,(
% 0.15/5.94 ![X0]: (sP2_prd(sK6_skl)|h_false(sK0_skl,X0))),
% 0.15/5.94 inference(forward_subsumption_resolution,[status(thm)],[f1768,f55])).
% 0.15/5.94 fof(f1774,plain,(
% 0.15/5.94 ![X0]: (sP2_prd(sK6_skl)|~h_true_only(sK0_skl,X0))),
% 0.15/5.94 inference(resolution,[status(thm)],[f1772,f46])).
% 0.15/5.94 fof(f1782,plain,(
% 0.15/5.94 ![X0,X1,X2,X3,X4,X5]: (sP2_prd(sK6_skl)|g_true_only(sK0_skl,sK11_skl(sK0_skl))|g_true_only(sK0_skl,sK4_skl(sK0_skl))|~h_both(sK0_skl,X0)|h_true_only(sK0_skl,sK5_skl(sK0_skl))|sP2_prd(sK6_skl)|~g_both(X1,X2)|~h_both(X1,X3)|g_false_only(X1,X2)|h_true_only(X1,sK7_skl(X2,X1))|sP3_prd(X4,sK8_skl(X1),X1)|sP4_prd(X5,sK10_skl,sK9_skl)|h_false_only(sK9_skl,X5))),
% 0.15/5.94 inference(resolution,[status(thm)],[f1762,f26])).
% 0.15/5.94 fof(f1783,plain,(
% 0.15/5.94 ![X0,X1,X2,X3,X4,X5]: (sP2_prd(sK6_skl)|g_true_only(sK0_skl,sK11_skl(sK0_skl))|g_true_only(sK0_skl,sK4_skl(sK0_skl))|~h_both(sK0_skl,X0)|h_true_only(sK0_skl,sK5_skl(sK0_skl))|sP2_prd(sK6_skl)|~g_both(X1,X2)|~h_both(X1,X3)|g_false_only(X1,X2)|h_true_only(X1,sK7_skl(X2,X1))|sP3_prd(X4,sK8_skl(X1),X1)|sP4_prd(X5,sK10_skl,sK9_skl)|g_both(sK9_skl,sK10_skl))),
% 0.15/5.94 inference(resolution,[status(thm)],[f1762,f25])).
% 0.15/5.94 fof(f1785,plain,(
% 0.15/5.94 sP2_prd(sK6_skl)|g_true_only(sK0_skl,sK11_skl(sK0_skl))|g_true(sK0_skl,sK11_skl(sK0_skl))),
% 0.15/5.94 inference(resolution,[status(thm)],[f1762,f34])).
% 0.15/5.94 fof(f1787,plain,(
% 0.15/5.94 ![X0,X1,X2,X3,X4,X5]: (sP2_prd(sK6_skl)|g_true_only(sK0_skl,sK11_skl(sK0_skl))|g_true_only(sK0_skl,sK4_skl(sK0_skl))|~h_both(sK0_skl,X0)|h_true_only(sK0_skl,sK5_skl(sK0_skl))|~g_both(X1,X2)|~h_both(X1,X3)|g_false_only(X1,X2)|h_true_only(X1,sK7_skl(X2,X1))|sP3_prd(X4,sK8_skl(X1),X1)|sP4_prd(X5,sK10_skl,sK9_skl)|h_false_only(sK9_skl,X5))),
% 0.15/5.94 inference(duplicate_literals_removal,[status(thm)],[f1782])).
% 0.15/5.94 fof(f1788,plain,(
% 0.15/5.94 ![X0,X1,X2,X3,X4,X5]: (sP2_prd(sK6_skl)|g_true_only(sK0_skl,sK11_skl(sK0_skl))|g_true_only(sK0_skl,sK4_skl(sK0_skl))|~h_both(sK0_skl,X0)|~g_both(X1,X2)|~h_both(X1,X3)|g_false_only(X1,X2)|h_true_only(X1,sK7_skl(X2,X1))|sP3_prd(X4,sK8_skl(X1),X1)|sP4_prd(X5,sK10_skl,sK9_skl)|h_false_only(sK9_skl,X5))),
% 0.15/5.94 inference(forward_subsumption_resolution,[status(thm)],[f1787,f1774])).
% 0.15/5.94 fof(f1789,plain,(
% 0.15/5.94 ![X0,X1,X2,X3,X4,X5]: (sP2_prd(sK6_skl)|g_true_only(sK0_skl,sK11_skl(sK0_skl))|g_true_only(sK0_skl,sK4_skl(sK0_skl))|~h_both(sK0_skl,X0)|h_true_only(sK0_skl,sK5_skl(sK0_skl))|~g_both(X1,X2)|~h_both(X1,X3)|g_false_only(X1,X2)|h_true_only(X1,sK7_skl(X2,X1))|sP3_prd(X4,sK8_skl(X1),X1)|sP4_prd(X5,sK10_skl,sK9_skl)|g_both(sK9_skl,sK10_skl))),
% 0.15/5.94 inference(duplicate_literals_removal,[status(thm)],[f1783])).
% 0.15/5.94 fof(f1790,plain,(
% 0.15/5.94 ![X0,X1,X2,X3,X4,X5]: (sP2_prd(sK6_skl)|g_true_only(sK0_skl,sK11_skl(sK0_skl))|g_true_only(sK0_skl,sK4_skl(sK0_skl))|~h_both(sK0_skl,X0)|~g_both(X1,X2)|~h_both(X1,X3)|g_false_only(X1,X2)|h_true_only(X1,sK7_skl(X2,X1))|sP3_prd(X4,sK8_skl(X1),X1)|sP4_prd(X5,sK10_skl,sK9_skl)|g_both(sK9_skl,sK10_skl))),
% 0.15/5.94 inference(forward_subsumption_resolution,[status(thm)],[f1789,f1774])).
% 0.15/5.94 fof(f1791,plain,(
% 0.15/5.94 sP2_prd(sK6_skl)|g_true(sK0_skl,sK11_skl(sK0_skl))),
% 0.15/5.94 inference(forward_subsumption_resolution,[status(thm)],[f1785,f29])).
% 0.15/5.94 fof(f1795,plain,(
% 0.15/5.94 sP2_prd(sK6_skl)|~g_false_only(sK0_skl,sK11_skl(sK0_skl))),
% 0.15/5.94 inference(resolution,[status(thm)],[f1791,f40])).
% 0.15/5.94 fof(f1799,plain,(
% 0.15/5.94 ![X0,X1]: (sP2_prd(sK6_skl)|h_false_only(sK0_skl,X0)|~g_true_only(sK0_skl,X1))),
% 0.15/5.94 inference(forward_subsumption_resolution,[status(thm)],[f1764,f1774])).
% 0.15/5.94 fof(f1800,plain,(
% 0.15/5.94 ![X0,X1,X2,X3,X4,X5]: (sP2_prd(sK6_skl)|g_true_only(sK0_skl,sK11_skl(sK0_skl))|g_true_only(sK0_skl,sK4_skl(sK0_skl))|~g_both(X0,X1)|~h_both(X0,X2)|g_false_only(X0,X1)|h_true_only(X0,sK7_skl(X1,X0))|sP3_prd(X3,sK8_skl(X0),X0)|sP4_prd(X4,sK10_skl,sK9_skl)|h_false_only(sK9_skl,X4)|sP2_prd(sK6_skl)|h_false_only(sK0_skl,X5))),
% 0.15/5.94 inference(resolution,[status(thm)],[f1788,f1763])).
% 0.15/5.94 fof(f1801,plain,(
% 0.15/5.94 ![X0,X1,X2,X3,X4,X5]: (sP2_prd(sK6_skl)|g_true_only(sK0_skl,sK11_skl(sK0_skl))|g_true_only(sK0_skl,sK4_skl(sK0_skl))|~g_both(X0,X1)|~h_both(X0,X2)|g_false_only(X0,X1)|h_true_only(X0,sK7_skl(X1,X0))|sP3_prd(X3,sK8_skl(X0),X0)|sP4_prd(X4,sK10_skl,sK9_skl)|h_false_only(sK9_skl,X4)|h_false_only(sK0_skl,X5))),
% 0.15/5.94 inference(duplicate_literals_removal,[status(thm)],[f1800])).
% 0.15/5.94 fof(f1802,plain,(
% 0.15/5.94 ![X0,X1,X2,X3,X4,X5]: (sP2_prd(sK6_skl)|g_true_only(sK0_skl,sK4_skl(sK0_skl))|~g_both(X0,X1)|~h_both(X0,X2)|g_false_only(X0,X1)|h_true_only(X0,sK7_skl(X1,X0))|sP3_prd(X3,sK8_skl(X0),X0)|sP4_prd(X4,sK10_skl,sK9_skl)|h_false_only(sK9_skl,X4)|h_false_only(sK0_skl,X5))),
% 0.15/5.94 inference(forward_subsumption_resolution,[status(thm)],[f1801,f1799])).
% 0.15/5.94 fof(f1803,plain,(
% 0.15/5.94 ![X0,X1,X2,X3,X4,X5]: (sP2_prd(sK6_skl)|~g_both(X0,X1)|~h_both(X0,X2)|g_false_only(X0,X1)|h_true_only(X0,sK7_skl(X1,X0))|sP3_prd(X3,sK8_skl(X0),X0)|sP4_prd(X4,sK10_skl,sK9_skl)|h_false_only(sK9_skl,X4)|h_false_only(sK0_skl,X5))),
% 0.15/5.94 inference(forward_subsumption_resolution,[status(thm)],[f1802,f1799])).
% 0.15/5.94 fof(f1804,plain,(
% 0.15/5.94 ![X0,X1,X2,X3]: (sP2_prd(sK6_skl)|~h_both(sK0_skl,X0)|g_false_only(sK0_skl,sK11_skl(sK0_skl))|h_true_only(sK0_skl,sK7_skl(sK11_skl(sK0_skl),sK0_skl))|sP3_prd(X1,sK8_skl(sK0_skl),sK0_skl)|sP4_prd(X2,sK10_skl,sK9_skl)|h_false_only(sK9_skl,X2)|h_false_only(sK0_skl,X3)|sP2_prd(sK6_skl)|g_true_only(sK0_skl,sK11_skl(sK0_skl)))),
% 0.15/5.94 inference(resolution,[status(thm)],[f1803,f1762])).
% 0.15/5.94 fof(f1807,plain,(
% 0.15/5.94 ![X0,X1,X2,X3]: (sP2_prd(sK6_skl)|~h_both(sK0_skl,X0)|g_false_only(sK0_skl,sK11_skl(sK0_skl))|h_true_only(sK0_skl,sK7_skl(sK11_skl(sK0_skl),sK0_skl))|sP3_prd(X1,sK8_skl(sK0_skl),sK0_skl)|sP4_prd(X2,sK10_skl,sK9_skl)|h_false_only(sK9_skl,X2)|h_false_only(sK0_skl,X3)|g_true_only(sK0_skl,sK11_skl(sK0_skl)))),
% 0.15/5.94 inference(duplicate_literals_removal,[status(thm)],[f1804])).
% 0.15/5.94 fof(f1808,plain,(
% 0.15/5.94 ![X0,X1,X2,X3]: (sP2_prd(sK6_skl)|~h_both(sK0_skl,X0)|h_true_only(sK0_skl,sK7_skl(sK11_skl(sK0_skl),sK0_skl))|sP3_prd(X1,sK8_skl(sK0_skl),sK0_skl)|sP4_prd(X2,sK10_skl,sK9_skl)|h_false_only(sK9_skl,X2)|h_false_only(sK0_skl,X3)|g_true_only(sK0_skl,sK11_skl(sK0_skl)))),
% 0.15/5.94 inference(forward_subsumption_resolution,[status(thm)],[f1807,f1795])).
% 0.15/5.94 fof(f1809,plain,(
% 0.15/5.94 ![X0,X1,X2,X3]: (sP2_prd(sK6_skl)|~h_both(sK0_skl,X0)|sP3_prd(X1,sK8_skl(sK0_skl),sK0_skl)|sP4_prd(X2,sK10_skl,sK9_skl)|h_false_only(sK9_skl,X2)|h_false_only(sK0_skl,X3)|g_true_only(sK0_skl,sK11_skl(sK0_skl)))),
% 0.15/5.94 inference(forward_subsumption_resolution,[status(thm)],[f1808,f1774])).
% 0.15/5.94 fof(f1810,plain,(
% 0.15/5.94 ![X0,X1,X2,X3]: (sP2_prd(sK6_skl)|sP3_prd(X0,sK8_skl(sK0_skl),sK0_skl)|sP4_prd(X1,sK10_skl,sK9_skl)|h_false_only(sK9_skl,X1)|h_false_only(sK0_skl,X2)|g_true_only(sK0_skl,sK11_skl(sK0_skl))|sP2_prd(sK6_skl)|h_false_only(sK0_skl,X3))),
% 0.15/5.94 inference(resolution,[status(thm)],[f1809,f1763])).
% 0.15/5.94 fof(f1811,plain,(
% 0.15/5.94 ![X0,X1,X2,X3]: (sP2_prd(sK6_skl)|sP3_prd(X0,sK8_skl(sK0_skl),sK0_skl)|sP4_prd(X1,sK10_skl,sK9_skl)|h_false_only(sK9_skl,X1)|h_false_only(sK0_skl,X2)|g_true_only(sK0_skl,sK11_skl(sK0_skl))|h_false_only(sK0_skl,X3))),
% 0.15/5.94 inference(duplicate_literals_removal,[status(thm)],[f1810])).
% 0.15/5.94 fof(f1812,plain,(
% 0.15/5.94 ![X0,X1,X2,X3]: (sP2_prd(sK6_skl)|sP3_prd(X0,sK8_skl(sK0_skl),sK0_skl)|sP4_prd(X1,sK10_skl,sK9_skl)|h_false_only(sK9_skl,X1)|h_false_only(sK0_skl,X2)|h_false_only(sK0_skl,X3))),
% 0.15/5.94 inference(forward_subsumption_resolution,[status(thm)],[f1811,f1799])).
% 0.15/5.94 fof(f1814,plain,(
% 0.15/5.94 ![X0,X1,X2,X3]: (sP2_prd(sK6_skl)|sP4_prd(X0,sK10_skl,sK9_skl)|h_false_only(sK9_skl,X0)|h_false_only(sK0_skl,X1)|h_false_only(sK0_skl,X2)|g_true_only(sK0_skl,sK8_skl(sK0_skl))|h_false_only(sK0_skl,X3))),
% 0.15/5.94 inference(resolution,[status(thm)],[f1812,f88])).
% 0.15/5.94 fof(f1849,plain,(
% 0.15/5.94 ![X0,X1,X2,X3]: (sP2_prd(sK6_skl)|sP4_prd(X0,sK10_skl,sK9_skl)|h_false_only(sK9_skl,X0)|h_false_only(sK0_skl,X1)|h_false_only(sK0_skl,X2)|h_false_only(sK0_skl,X3))),
% 0.15/5.94 inference(forward_subsumption_resolution,[status(thm)],[f1814,f1799])).
% 0.15/5.94 fof(f1865,plain,(
% 0.15/5.94 ![X0,X1]: (sP2_prd(sK6_skl)|sP4_prd(X0,sK10_skl,sK9_skl)|h_false_only(sK9_skl,X0)|~g_true_only(sK0_skl,X1))),
% 0.15/5.94 inference(resolution,[status(thm)],[f1849,f1086])).
% 0.15/5.94 fof(f1911,plain,(
% 0.15/5.94 ![X0,X1]: (sP2_prd(sK6_skl)|sP4_prd(X0,sK10_skl,sK9_skl)|h_false_only(sK9_skl,X0)|h_false_only(sK0_skl,X1))),
% 0.15/5.94 inference(factoring,[status(thm)],[f1849])).
% 0.15/5.94 fof(f1926,plain,(
% 0.15/5.94 ![X0,X1,X2,X3,X4,X5]: (sP2_prd(sK6_skl)|g_true_only(sK0_skl,sK11_skl(sK0_skl))|g_true_only(sK0_skl,sK4_skl(sK0_skl))|~g_both(X0,X1)|~h_both(X0,X2)|g_false_only(X0,X1)|h_true_only(X0,sK7_skl(X1,X0))|sP3_prd(X3,sK8_skl(X0),X0)|sP4_prd(X4,sK10_skl,sK9_skl)|g_both(sK9_skl,sK10_skl)|sP2_prd(sK6_skl)|h_false_only(sK0_skl,X5))),
% 0.15/5.94 inference(resolution,[status(thm)],[f1790,f1763])).
% 0.15/5.94 fof(f1927,plain,(
% 0.15/5.94 ![X0,X1,X2,X3,X4,X5]: (sP2_prd(sK6_skl)|g_true_only(sK0_skl,sK11_skl(sK0_skl))|g_true_only(sK0_skl,sK4_skl(sK0_skl))|~g_both(X0,X1)|~h_both(X0,X2)|g_false_only(X0,X1)|h_true_only(X0,sK7_skl(X1,X0))|sP3_prd(X3,sK8_skl(X0),X0)|sP4_prd(X4,sK10_skl,sK9_skl)|g_both(sK9_skl,sK10_skl)|h_false_only(sK0_skl,X5))),
% 0.15/5.94 inference(duplicate_literals_removal,[status(thm)],[f1926])).
% 0.15/5.94 fof(f1928,plain,(
% 0.15/5.94 ![X0,X1,X2,X3,X4,X5]: (sP2_prd(sK6_skl)|g_true_only(sK0_skl,sK4_skl(sK0_skl))|~g_both(X0,X1)|~h_both(X0,X2)|g_false_only(X0,X1)|h_true_only(X0,sK7_skl(X1,X0))|sP3_prd(X3,sK8_skl(X0),X0)|sP4_prd(X4,sK10_skl,sK9_skl)|g_both(sK9_skl,sK10_skl)|h_false_only(sK0_skl,X5))),
% 0.15/5.94 inference(forward_subsumption_resolution,[status(thm)],[f1927,f1799])).
% 0.15/5.94 fof(f1929,plain,(
% 0.15/5.94 ![X0,X1,X2,X3,X4,X5]: (sP2_prd(sK6_skl)|~g_both(X0,X1)|~h_both(X0,X2)|g_false_only(X0,X1)|h_true_only(X0,sK7_skl(X1,X0))|sP3_prd(X3,sK8_skl(X0),X0)|sP4_prd(X4,sK10_skl,sK9_skl)|g_both(sK9_skl,sK10_skl)|h_false_only(sK0_skl,X5))),
% 0.15/5.94 inference(forward_subsumption_resolution,[status(thm)],[f1928,f1799])).
% 0.15/5.94 fof(f1930,plain,(
% 0.15/5.94 ![X0,X1,X2,X3]: (sP2_prd(sK6_skl)|~h_both(sK0_skl,X0)|g_false_only(sK0_skl,sK11_skl(sK0_skl))|h_true_only(sK0_skl,sK7_skl(sK11_skl(sK0_skl),sK0_skl))|sP3_prd(X1,sK8_skl(sK0_skl),sK0_skl)|sP4_prd(X2,sK10_skl,sK9_skl)|g_both(sK9_skl,sK10_skl)|h_false_only(sK0_skl,X3)|sP2_prd(sK6_skl)|g_true_only(sK0_skl,sK11_skl(sK0_skl)))),
% 0.15/5.94 inference(resolution,[status(thm)],[f1929,f1762])).
% 0.15/5.94 fof(f1933,plain,(
% 0.15/5.94 ![X0,X1,X2,X3]: (sP2_prd(sK6_skl)|~h_both(sK0_skl,X0)|g_false_only(sK0_skl,sK11_skl(sK0_skl))|h_true_only(sK0_skl,sK7_skl(sK11_skl(sK0_skl),sK0_skl))|sP3_prd(X1,sK8_skl(sK0_skl),sK0_skl)|sP4_prd(X2,sK10_skl,sK9_skl)|g_both(sK9_skl,sK10_skl)|h_false_only(sK0_skl,X3)|g_true_only(sK0_skl,sK11_skl(sK0_skl)))),
% 0.15/5.94 inference(duplicate_literals_removal,[status(thm)],[f1930])).
% 0.15/5.94 fof(f1934,plain,(
% 0.15/5.94 ![X0,X1,X2,X3]: (sP2_prd(sK6_skl)|~h_both(sK0_skl,X0)|h_true_only(sK0_skl,sK7_skl(sK11_skl(sK0_skl),sK0_skl))|sP3_prd(X1,sK8_skl(sK0_skl),sK0_skl)|sP4_prd(X2,sK10_skl,sK9_skl)|g_both(sK9_skl,sK10_skl)|h_false_only(sK0_skl,X3)|g_true_only(sK0_skl,sK11_skl(sK0_skl)))),
% 0.15/5.94 inference(forward_subsumption_resolution,[status(thm)],[f1933,f1795])).
% 0.15/5.94 fof(f1941,plain,(
% 0.15/5.94 ![X0,X1]: (sP2_prd(sK6_skl)|sP4_prd(X0,sK10_skl,sK9_skl)|h_false_only(sK9_skl,X0)|~g_both(sK0_skl,X1)|g_true_only(sK0_skl,sK13_skl(sK0_skl)))),
% 0.15/5.94 inference(resolution,[status(thm)],[f1911,f1144])).
% 0.15/5.94 fof(f1952,plain,(
% 0.15/5.94 ![X0,X1]: (sP2_prd(sK6_skl)|sP4_prd(X0,sK10_skl,sK9_skl)|h_false_only(sK9_skl,X0)|~g_both(sK0_skl,X1))),
% 0.15/5.94 inference(forward_subsumption_resolution,[status(thm)],[f1941,f1865])).
% 0.15/5.94 fof(f1992,plain,(
% 0.15/5.94 ![X0,X1,X2,X3]: (sP2_prd(sK6_skl)|~h_both(sK0_skl,X0)|sP3_prd(X1,sK8_skl(sK0_skl),sK0_skl)|sP4_prd(X2,sK10_skl,sK9_skl)|g_both(sK9_skl,sK10_skl)|h_false_only(sK0_skl,X3)|g_true_only(sK0_skl,sK11_skl(sK0_skl)))),
% 0.15/5.94 inference(forward_subsumption_resolution,[status(thm)],[f1934,f1774])).
% 0.15/5.94 fof(f1993,plain,(
% 0.15/5.94 ![X0,X1,X2,X3]: (sP2_prd(sK6_skl)|sP3_prd(X0,sK8_skl(sK0_skl),sK0_skl)|sP4_prd(X1,sK10_skl,sK9_skl)|g_both(sK9_skl,sK10_skl)|h_false_only(sK0_skl,X2)|g_true_only(sK0_skl,sK11_skl(sK0_skl))|sP2_prd(sK6_skl)|h_false_only(sK0_skl,X3))),
% 0.15/5.94 inference(resolution,[status(thm)],[f1992,f1763])).
% 0.15/5.94 fof(f1994,plain,(
% 0.15/5.94 ![X0,X1,X2,X3]: (sP2_prd(sK6_skl)|sP3_prd(X0,sK8_skl(sK0_skl),sK0_skl)|sP4_prd(X1,sK10_skl,sK9_skl)|g_both(sK9_skl,sK10_skl)|h_false_only(sK0_skl,X2)|g_true_only(sK0_skl,sK11_skl(sK0_skl))|h_false_only(sK0_skl,X3))),
% 0.15/5.94 inference(duplicate_literals_removal,[status(thm)],[f1993])).
% 0.15/5.94 fof(f1995,plain,(
% 0.15/5.94 ![X0,X1,X2,X3]: (sP2_prd(sK6_skl)|sP3_prd(X0,sK8_skl(sK0_skl),sK0_skl)|sP4_prd(X1,sK10_skl,sK9_skl)|g_both(sK9_skl,sK10_skl)|h_false_only(sK0_skl,X2)|h_false_only(sK0_skl,X3))),
% 0.15/5.94 inference(forward_subsumption_resolution,[status(thm)],[f1994,f1799])).
% 0.15/5.94 fof(f2023,plain,(
% 0.15/5.94 ![X0,X1,X2,X3]: (sP2_prd(sK6_skl)|sP4_prd(X0,sK10_skl,sK9_skl)|g_both(sK9_skl,sK10_skl)|h_false_only(sK0_skl,X1)|h_false_only(sK0_skl,X2)|g_true_only(sK0_skl,sK8_skl(sK0_skl))|h_false_only(sK0_skl,X3))),
% 0.15/5.94 inference(resolution,[status(thm)],[f1995,f88])).
% 0.15/5.94 fof(f2058,plain,(
% 0.15/5.94 ![X0,X1,X2,X3]: (sP2_prd(sK6_skl)|sP4_prd(X0,sK10_skl,sK9_skl)|g_both(sK9_skl,sK10_skl)|h_false_only(sK0_skl,X1)|h_false_only(sK0_skl,X2)|h_false_only(sK0_skl,X3))),
% 0.15/5.94 inference(forward_subsumption_resolution,[status(thm)],[f2023,f1799])).
% 0.15/5.94 fof(f2152,plain,(
% 0.15/5.94 ![X0]: (sP2_prd(sK6_skl)|sP4_prd(X0,sK10_skl,sK9_skl)|h_false_only(sK9_skl,X0)|sP2_prd(sK6_skl)|g_true_only(sK0_skl,sK11_skl(sK0_skl)))),
% 0.15/5.94 inference(resolution,[status(thm)],[f1952,f1762])).
% 0.15/5.94 fof(f2153,plain,(
% 0.15/5.94 ![X0]: (sP2_prd(sK6_skl)|sP4_prd(X0,sK10_skl,sK9_skl)|h_false_only(sK9_skl,X0)|g_true_only(sK0_skl,sK11_skl(sK0_skl)))),
% 0.15/5.94 inference(duplicate_literals_removal,[status(thm)],[f2152])).
% 0.15/5.94 fof(f2154,plain,(
% 0.15/5.94 ![X0]: (sP2_prd(sK6_skl)|sP4_prd(X0,sK10_skl,sK9_skl)|h_false_only(sK9_skl,X0))),
% 0.15/5.94 inference(forward_subsumption_resolution,[status(thm)],[f2153,f1865])).
% 0.15/5.94 fof(f2155,plain,(
% 0.15/5.94 ![X0]: (sP2_prd(sK6_skl)|h_false_only(sK9_skl,X0)|h_both(sK9_skl,X0)|h_false_only(sK9_skl,X0))),
% 0.15/5.94 inference(resolution,[status(thm)],[f2154,f97])).
% 0.15/5.94 fof(f2156,plain,(
% 0.15/5.94 ![X0]: (sP2_prd(sK6_skl)|h_false_only(sK9_skl,X0)|g_true_only(sK9_skl,sK10_skl))),
% 0.15/5.94 inference(resolution,[status(thm)],[f2154,f96])).
% 0.15/5.94 fof(f2157,plain,(
% 0.15/5.94 ![X0]: (sP2_prd(sK6_skl)|h_false_only(sK9_skl,X0)|h_both(sK9_skl,X0))),
% 0.15/5.94 inference(duplicate_literals_removal,[status(thm)],[f2155])).
% 0.15/5.94 fof(f2158,plain,(
% 0.15/5.94 ![X0,X1]: (sP2_prd(sK6_skl)|h_false_only(sK9_skl,X0)|~g_true_only(sK9_skl,X1)|h_true_only(sK9_skl,sK19_skl(sK9_skl)))),
% 0.15/5.94 inference(resolution,[status(thm)],[f2157,f1087])).
% 0.15/5.94 fof(f2162,plain,(
% 0.15/5.94 ![X0]: (sP2_prd(sK6_skl)|h_false_only(sK9_skl,X0)|h_false(sK9_skl,X0))),
% 0.15/5.94 inference(resolution,[status(thm)],[f2157,f51])).
% 0.15/5.94 fof(f2166,plain,(
% 0.15/5.94 ![X0]: (sP2_prd(sK6_skl)|h_false(sK9_skl,X0))),
% 0.15/5.94 inference(forward_subsumption_resolution,[status(thm)],[f2162,f55])).
% 0.15/5.94 fof(f2168,plain,(
% 0.15/5.94 ![X0]: (sP2_prd(sK6_skl)|~h_true_only(sK9_skl,X0))),
% 0.15/5.94 inference(resolution,[status(thm)],[f2166,f46])).
% 0.15/5.94 fof(f2189,plain,(
% 0.15/5.94 ![X0]: (sP2_prd(sK6_skl)|h_false_only(sK9_skl,X0))),
% 0.15/5.94 inference(backward_subsumption_resolution,[status(thm)],[f2156,f2190])).
% 0.15/5.94 fof(f2190,plain,(
% 0.15/5.94 ![X0,X1]: (sP2_prd(sK6_skl)|h_false_only(sK9_skl,X0)|~g_true_only(sK9_skl,X1))),
% 0.15/5.94 inference(forward_subsumption_resolution,[status(thm)],[f2158,f2168])).
% 0.15/5.94 fof(f2191,plain,(
% 0.15/5.94 ![X0]: (sP2_prd(sK6_skl)|~g_both(sK9_skl,X0)|g_true_only(sK9_skl,sK13_skl(sK9_skl)))),
% 0.15/5.94 inference(resolution,[status(thm)],[f2189,f1144])).
% 0.15/5.94 fof(f2192,plain,(
% 0.15/5.94 ![X0]: (sP2_prd(sK6_skl)|~g_true_only(sK9_skl,X0))),
% 0.15/5.94 inference(resolution,[status(thm)],[f2189,f1086])).
% 0.15/5.94 fof(f2201,plain,(
% 0.15/5.94 ![X0,X1,X2]: (sP2_prd(sK6_skl)|g_both(sK9_skl,sK10_skl)|h_false_only(sK0_skl,X0)|h_false_only(sK0_skl,X1)|h_false_only(sK0_skl,X2)|g_true_only(sK9_skl,sK10_skl))),
% 0.15/5.94 inference(resolution,[status(thm)],[f2058,f96])).
% 0.15/5.94 fof(f2253,plain,(
% 0.15/5.94 ![X0,X1,X2]: (sP2_prd(sK6_skl)|g_both(sK9_skl,sK10_skl)|h_false_only(sK0_skl,X0)|h_false_only(sK0_skl,X1)|h_false_only(sK0_skl,X2))),
% 0.15/5.94 inference(forward_subsumption_resolution,[status(thm)],[f2201,f2192])).
% 0.15/5.94 fof(f2316,plain,(
% 0.15/5.94 ![X0]: (sP2_prd(sK6_skl)|~g_both(sK9_skl,X0))),
% 0.15/5.94 inference(forward_subsumption_resolution,[status(thm)],[f2191,f2192])).
% 0.15/5.94 fof(f2332,plain,(
% 0.15/5.94 ![X0,X1,X2]: (sP2_prd(sK6_skl)|h_false_only(sK0_skl,X0)|h_false_only(sK0_skl,X1)|h_false_only(sK0_skl,X2))),
% 0.15/5.94 inference(forward_subsumption_resolution,[status(thm)],[f2253,f2316])).
% 0.15/5.94 fof(f2337,plain,(
% 0.15/5.95 ![X0]: (sP2_prd(sK6_skl)|~g_true_only(sK0_skl,X0))),
% 0.15/5.95 inference(resolution,[status(thm)],[f2332,f1086])).
% 0.15/5.95 fof(f2383,plain,(
% 0.15/5.95 ![X0]: (sP2_prd(sK6_skl)|h_false_only(sK0_skl,X0))),
% 0.15/5.95 inference(factoring,[status(thm)],[f2332])).
% 0.15/5.95 fof(f2400,plain,(
% 0.15/5.95 sP2_prd(sK6_skl)|g_both(sK0_skl,sK11_skl(sK0_skl))),
% 0.15/5.95 inference(backward_subsumption_resolution,[status(thm)],[f1762,f2337])).
% 0.15/5.95 fof(f2403,plain,(
% 0.15/5.95 ![X0]: (sP2_prd(sK6_skl)|~g_both(sK0_skl,X0)|g_true_only(sK0_skl,sK13_skl(sK0_skl)))),
% 0.15/5.95 inference(resolution,[status(thm)],[f2383,f1144])).
% 0.15/5.95 fof(f2412,plain,(
% 0.15/5.95 ![X0]: (sP2_prd(sK6_skl)|~g_both(sK0_skl,X0))),
% 0.15/5.95 inference(forward_subsumption_resolution,[status(thm)],[f2403,f2337])).
% 0.15/5.95 fof(f2414,plain,(
% 0.15/5.95 sP2_prd(sK6_skl)),
% 0.15/5.95 inference(forward_subsumption_resolution,[status(thm)],[f2400,f2412])).
% 0.15/5.95 fof(f2415,plain,(
% 0.15/5.95 sP6_prd(sK6_skl)|g_both(sK6_skl,sK16_skl(sK6_skl))),
% 0.15/5.95 inference(resolution,[status(thm)],[f2414,f80])).
% 0.15/5.95 fof(f2416,plain,(
% 0.15/5.95 ![X0]: (sP6_prd(sK6_skl)|h_false_only(sK6_skl,X0))),
% 0.15/5.95 inference(resolution,[status(thm)],[f2414,f82])).
% 0.15/5.95 fof(f2417,plain,(
% 0.15/5.95 ![X0]: (sP6_prd(sK6_skl)|~g_both(sK6_skl,X0)|g_true_only(sK6_skl,sK13_skl(sK6_skl)))),
% 0.15/5.95 inference(resolution,[status(thm)],[f2416,f1144])).
% 0.15/5.95 fof(f2418,plain,(
% 0.15/5.95 ![X0]: (sP6_prd(sK6_skl)|~g_true_only(sK6_skl,X0))),
% 0.15/5.95 inference(resolution,[status(thm)],[f2416,f1086])).
% 0.15/5.95 fof(f2433,plain,(
% 0.15/5.95 sP6_prd(sK6_skl)),
% 0.15/5.95 inference(backward_subsumption_resolution,[status(thm)],[f2415,f2434])).
% 0.15/5.95 fof(f2434,plain,(
% 0.15/5.95 ![X0]: (sP6_prd(sK6_skl)|~g_both(sK6_skl,X0))),
% 0.15/5.95 inference(forward_subsumption_resolution,[status(thm)],[f2417,f2418])).
% 0.15/5.95 fof(f2438,plain,(
% 0.15/5.95 ![X0]: (h_both(sK6_skl,sK24_skl(sK6_skl))|h_false_only(sK6_skl,X0))),
% 0.15/5.95 inference(resolution,[status(thm)],[f2433,f112])).
% 0.15/5.95 fof(f2439,plain,(
% 0.15/5.95 g_true_only(sK6_skl,sK23_skl(sK6_skl))),
% 0.15/5.95 inference(resolution,[status(thm)],[f2433,f111])).
% 0.15/5.95 fof(f2442,plain,(
% 0.15/5.95 sP0_prd(sK6_skl)|h_true_only(sK6_skl,sK12_skl(sK6_skl))),
% 0.15/5.95 inference(resolution,[status(thm)],[f2439,f196])).
% 0.15/5.95 fof(f2454,plain,(
% 0.15/5.95 ![X0]: (sP0_prd(sK6_skl)|~sP6_prd(sK6_skl)|h_false_only(sK6_skl,X0))),
% 0.15/5.95 inference(resolution,[status(thm)],[f2442,f113])).
% 0.15/5.95 fof(f2457,plain,(
% 0.15/5.95 ![X0]: (sP0_prd(sK6_skl)|h_false_only(sK6_skl,X0))),
% 0.15/5.95 inference(forward_subsumption_resolution,[status(thm)],[f2454,f2433])).
% 0.15/5.95 fof(f2459,plain,(
% 0.15/5.95 ![X0]: (sP0_prd(sK6_skl)|~g_true_only(sK6_skl,X0))),
% 0.15/5.95 inference(resolution,[status(thm)],[f2457,f1086])).
% 0.15/5.95 fof(f2469,plain,(
% 0.15/5.95 sP0_prd(sK6_skl)),
% 0.15/5.95 inference(resolution,[status(thm)],[f2459,f2439])).
% 0.15/5.95 fof(f2471,plain,(
% 0.15/5.95 ![X0]: (h_both(sK6_skl,X0)|h_false_only(sK6_skl,X0))),
% 0.15/5.95 inference(resolution,[status(thm)],[f2469,f128])).
% 0.15/5.95 fof(f2494,plain,(
% 0.15/5.95 ![X0]: (h_false_only(sK6_skl,X0)|h_false(sK6_skl,X0))),
% 0.15/5.95 inference(resolution,[status(thm)],[f2471,f51])).
% 0.15/5.95 fof(f2498,plain,(
% 0.15/5.95 ![X0]: (h_false(sK6_skl,X0))),
% 0.15/5.95 inference(forward_subsumption_resolution,[status(thm)],[f2494,f55])).
% 0.15/5.95 fof(f2500,plain,(
% 0.15/5.95 ![X0]: (~h_true_only(sK6_skl,X0))),
% 0.15/5.95 inference(resolution,[status(thm)],[f2498,f46])).
% 0.15/5.95 fof(f2509,plain,(
% 0.15/5.95 ![X0,X1]: (h_false_only(sK6_skl,X0)|~g_true_only(sK6_skl,X1)|h_true_only(sK6_skl,sK19_skl(sK6_skl)))),
% 0.15/5.95 inference(resolution,[status(thm)],[f2438,f1087])).
% 0.15/5.95 fof(f2524,plain,(
% 0.15/5.95 ![X0,X1]: (h_false_only(sK6_skl,X0)|~g_true_only(sK6_skl,X1))),
% 0.15/5.95 inference(forward_subsumption_resolution,[status(thm)],[f2509,f2500])).
% 0.15/5.95 fof(f2525,plain,(
% 0.15/5.95 ![X0]: (h_false_only(sK6_skl,X0))),
% 0.15/5.95 inference(resolution,[status(thm)],[f2524,f2439])).
% 0.15/5.95 fof(f2527,plain,(
% 0.15/5.95 ![X0]: (~g_true_only(sK6_skl,X0))),
% 0.15/5.95 inference(resolution,[status(thm)],[f2525,f1086])).
% 0.15/5.95 fof(f2536,plain,(
% 0.15/5.95 $false),
% 0.15/5.95 inference(backward_subsumption_resolution,[status(thm)],[f2439,f2527])).
% 0.15/5.95 % SZS output end CNFRefutation for theBenchmark.p
% 0.15/5.95 % Elapsed time: 0.549096 seconds
% 0.15/5.95 % CPU time: 4.193242 seconds
% 0.15/5.95 % Total memory used: 51.847 MB
% 0.15/5.95 % Net memory used: 49.055 MB
%------------------------------------------------------------------------------