%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SEU406+4 : 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 : n009.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 02:22:32 PM UTC 2026
% Result : Theorem 134.01s 36.09s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEU406+4 : 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.16/0.42 % Computer : n009.cluster.edu
% 0.16/0.42 % Model : x86_64 x86_64
% 0.16/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.42 % Memory : 8046.5625MB
% 0.16/0.42 % OS : Linux 6.8.0-71-generic
% 0.16/0.42 % CPULimit : 300
% 0.16/0.42 % WCLimit : 300
% 0.16/0.42 % DateTime : Mon Sep 21 06:21:18 UTC 2026
% 0.16/0.42 % CPUTime :
% 21.48/21.70 % Drodi V4.1.1
% 134.01/36.09 % Refutation found
% 134.01/36.09 % SZS status Theorem for theBenchmark: Theorem is valid
% 134.01/36.09 % SZS output start CNFRefutation for theBenchmark
% 134.01/36.09 fof(f30,axiom,(
% 134.01/36.09 (! [A,B,C] :( C = k2_xboole_0(A,B)<=> (! [D] :( r2_hidden(D,C)<=> ( r2_hidden(D,A)| r2_hidden(D,B) ) ) )) )),
% 134.01/36.09 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 134.01/36.09 fof(f32,axiom,(
% 134.01/36.09 (! [A,B,C] :( C = k4_xboole_0(A,B)<=> (! [D] :( r2_hidden(D,C)<=> ( r2_hidden(D,A)& ~ r2_hidden(D,B) ) ) )) )),
% 134.01/36.09 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 134.01/36.09 fof(f62,axiom,(
% 134.01/36.09 (! [A] : k2_xboole_0(A,k1_xboole_0) = A )),
% 134.01/36.09 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 134.01/36.09 fof(f369,axiom,(
% 134.01/36.09 (! [A,B,C] :~ ( k1_tarski(A) = k2_xboole_0(B,C)& B != C& B != k1_xboole_0& C != k1_xboole_0 ) )),
% 134.01/36.09 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 134.01/36.09 fof(f3243,axiom,(
% 134.01/36.09 (! [A,B,C] :( r2_hidden(A,k2_xboole_0(B,k1_tarski(C)))<=> ( r2_hidden(A,B)| A = C ) ) )),
% 134.01/36.09 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 134.01/36.09 fof(f66033,conjecture,(
% 134.01/36.09 (! [A,B,C,D] :~ ( r2_hidden(A,k2_xboole_0(C,D))& r2_hidden(B,k2_xboole_0(C,D))& ~ ( r2_hidden(A,k4_xboole_0(C,D))& r2_hidden(B,k4_xboole_0(C,D)) )& ~ ( r2_hidden(A,D)& r2_hidden(B,D) )& ~ ( r2_hidden(A,k4_xboole_0(C,D))& r2_hidden(B,D) )& ~ ( r2_hidden(A,D)& r2_hidden(B,k4_xboole_0(C,D)) ) ) )),
% 134.01/36.09 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 134.01/36.09 fof(f66034,negated_conjecture,(
% 134.01/36.09 ~((! [A,B,C,D] :~ ( r2_hidden(A,k2_xboole_0(C,D))& r2_hidden(B,k2_xboole_0(C,D))& ~ ( r2_hidden(A,k4_xboole_0(C,D))& r2_hidden(B,k4_xboole_0(C,D)) )& ~ ( r2_hidden(A,D)& r2_hidden(B,D) )& ~ ( r2_hidden(A,k4_xboole_0(C,D))& r2_hidden(B,D) )& ~ ( r2_hidden(A,D)& r2_hidden(B,k4_xboole_0(C,D)) ) ) ))),
% 134.01/36.09 inference(negated_conjecture,[status(cth)],[f66033])).
% 134.01/36.09 fof(f66129,plain,(
% 134.01/36.09 ![A,B,C]: ((~C=k2_xboole_0(A,B)|(![D]: ((~r2_hidden(D,C)|(r2_hidden(D,A)|r2_hidden(D,B)))&(r2_hidden(D,C)|(~r2_hidden(D,A)&~r2_hidden(D,B))))))&(C=k2_xboole_0(A,B)|(?[D]: ((~r2_hidden(D,C)|(~r2_hidden(D,A)&~r2_hidden(D,B)))&(r2_hidden(D,C)|(r2_hidden(D,A)|r2_hidden(D,B)))))))),
% 134.01/36.09 inference(NNF_transformation,[status(thm)],[f30])).
% 134.01/36.09 fof(f66130,plain,(
% 134.01/36.09 (![A,B,C]: (~C=k2_xboole_0(A,B)|((![D]: (~r2_hidden(D,C)|(r2_hidden(D,A)|r2_hidden(D,B))))&(![D]: (r2_hidden(D,C)|(~r2_hidden(D,A)&~r2_hidden(D,B)))))))&(![A,B,C]: (C=k2_xboole_0(A,B)|(?[D]: ((~r2_hidden(D,C)|(~r2_hidden(D,A)&~r2_hidden(D,B)))&(r2_hidden(D,C)|(r2_hidden(D,A)|r2_hidden(D,B)))))))),
% 134.01/36.09 inference(miniscoping,[status(thm)],[f66129])).
% 134.01/36.09 fof(f66131,plain,(
% 134.01/36.09 (![A,B,C]: (~C=k2_xboole_0(A,B)|((![D]: (~r2_hidden(D,C)|(r2_hidden(D,A)|r2_hidden(D,B))))&(![D]: (r2_hidden(D,C)|(~r2_hidden(D,A)&~r2_hidden(D,B)))))))&(![A,B,C]: (C=k2_xboole_0(A,B)|((~r2_hidden(sK23_skl(C,B,A),C)|(~r2_hidden(sK23_skl(C,B,A),A)&~r2_hidden(sK23_skl(C,B,A),B)))&(r2_hidden(sK23_skl(C,B,A),C)|(r2_hidden(sK23_skl(C,B,A),A)|r2_hidden(sK23_skl(C,B,A),B))))))),
% 134.01/36.09 inference(skolemize,[status(esa),new_symbols(skolem,[sK23_skl]),skolemize(D,sK23_skl(C,B,A))],[f66130])).
% 134.01/36.09 fof(f66132,plain,(
% 134.01/36.09 ![X0,X1,X2,X3]: (~X0=k2_xboole_0(X1,X2)|~r2_hidden(X3,X0)|r2_hidden(X3,X1)|r2_hidden(X3,X2))),
% 134.01/36.09 inference(cnf_transformation,[status(thm)],[f66131])).
% 134.01/36.09 fof(f66133,plain,(
% 134.01/36.09 ![X0,X1,X2,X3]: (~X0=k2_xboole_0(X1,X2)|r2_hidden(X3,X0)|~r2_hidden(X3,X1))),
% 134.01/36.09 inference(cnf_transformation,[status(thm)],[f66131])).
% 134.01/36.09 fof(f66147,plain,(
% 134.01/36.09 ![A,B,C]: ((~C=k4_xboole_0(A,B)|(![D]: ((~r2_hidden(D,C)|(r2_hidden(D,A)&~r2_hidden(D,B)))&(r2_hidden(D,C)|(~r2_hidden(D,A)|r2_hidden(D,B))))))&(C=k4_xboole_0(A,B)|(?[D]: ((~r2_hidden(D,C)|(~r2_hidden(D,A)|r2_hidden(D,B)))&(r2_hidden(D,C)|(r2_hidden(D,A)&~r2_hidden(D,B)))))))),
% 134.01/36.09 inference(NNF_transformation,[status(thm)],[f32])).
% 134.01/36.09 fof(f66148,plain,(
% 134.01/36.09 (![A,B,C]: (~C=k4_xboole_0(A,B)|((![D]: (~r2_hidden(D,C)|(r2_hidden(D,A)&~r2_hidden(D,B))))&(![D]: (r2_hidden(D,C)|(~r2_hidden(D,A)|r2_hidden(D,B)))))))&(![A,B,C]: (C=k4_xboole_0(A,B)|(?[D]: ((~r2_hidden(D,C)|(~r2_hidden(D,A)|r2_hidden(D,B)))&(r2_hidden(D,C)|(r2_hidden(D,A)&~r2_hidden(D,B)))))))),
% 134.01/36.09 inference(miniscoping,[status(thm)],[f66147])).
% 134.01/36.09 fof(f66149,plain,(
% 134.01/36.09 (![A,B,C]: (~C=k4_xboole_0(A,B)|((![D]: (~r2_hidden(D,C)|(r2_hidden(D,A)&~r2_hidden(D,B))))&(![D]: (r2_hidden(D,C)|(~r2_hidden(D,A)|r2_hidden(D,B)))))))&(![A,B,C]: (C=k4_xboole_0(A,B)|((~r2_hidden(sK25_skl(C,B,A),C)|(~r2_hidden(sK25_skl(C,B,A),A)|r2_hidden(sK25_skl(C,B,A),B)))&(r2_hidden(sK25_skl(C,B,A),C)|(r2_hidden(sK25_skl(C,B,A),A)&~r2_hidden(sK25_skl(C,B,A),B))))))),
% 134.01/36.09 inference(skolemize,[status(esa),new_symbols(skolem,[sK25_skl]),skolemize(D,sK25_skl(C,B,A))],[f66148])).
% 134.01/36.09 fof(f66152,plain,(
% 134.01/36.09 ![X0,X1,X2,X3]: (~X0=k4_xboole_0(X1,X2)|r2_hidden(X3,X0)|~r2_hidden(X3,X1)|r2_hidden(X3,X2))),
% 134.01/36.09 inference(cnf_transformation,[status(thm)],[f66149])).
% 134.01/36.09 fof(f66247,plain,(
% 134.01/36.09 ![X0]: (k2_xboole_0(X0,k1_xboole_0)=X0)),
% 134.01/36.09 inference(cnf_transformation,[status(thm)],[f62])).
% 134.01/36.09 fof(f66745,plain,(
% 134.01/36.09 ![A,B,C]: (((~k1_tarski(A)=k2_xboole_0(B,C)|B=C)|B=k1_xboole_0)|C=k1_xboole_0)),
% 134.01/36.09 inference(pre_NNF_transformation,[status(thm)],[f369])).
% 134.01/36.09 fof(f66746,plain,(
% 134.01/36.09 ![C]: ((![B]: (((![A]: ~k1_tarski(A)=k2_xboole_0(B,C))|B=C)|B=k1_xboole_0))|C=k1_xboole_0)),
% 134.01/36.09 inference(miniscoping,[status(thm)],[f66745])).
% 134.01/36.09 fof(f66747,plain,(
% 134.01/36.09 ![X0,X1,X2]: (~k1_tarski(X0)=k2_xboole_0(X1,X2)|X1=X2|X1=k1_xboole_0|X2=k1_xboole_0)),
% 134.01/36.09 inference(cnf_transformation,[status(thm)],[f66746])).
% 134.01/36.09 fof(f75238,plain,(
% 134.01/36.09 ![A,B,C]: ((~r2_hidden(A,k2_xboole_0(B,k1_tarski(C)))|(r2_hidden(A,B)|A=C))&(r2_hidden(A,k2_xboole_0(B,k1_tarski(C)))|(~r2_hidden(A,B)&~A=C)))),
% 134.01/36.09 inference(NNF_transformation,[status(thm)],[f3243])).
% 134.01/36.09 fof(f75239,plain,(
% 134.01/36.09 (![A,B,C]: (~r2_hidden(A,k2_xboole_0(B,k1_tarski(C)))|(r2_hidden(A,B)|A=C)))&(![A,B,C]: (r2_hidden(A,k2_xboole_0(B,k1_tarski(C)))|(~r2_hidden(A,B)&~A=C)))),
% 134.01/36.09 inference(miniscoping,[status(thm)],[f75238])).
% 134.01/36.09 fof(f75240,plain,(
% 134.01/36.09 ![X0,X1,X2]: (~r2_hidden(X0,k2_xboole_0(X1,k1_tarski(X2)))|r2_hidden(X0,X1)|X0=X2)),
% 134.01/36.09 inference(cnf_transformation,[status(thm)],[f75239])).
% 134.01/36.09 fof(f310176,plain,(
% 134.01/36.09 (?[A,B,C,D]: (((((r2_hidden(A,k2_xboole_0(C,D))&r2_hidden(B,k2_xboole_0(C,D)))&(~r2_hidden(A,k4_xboole_0(C,D))|~r2_hidden(B,k4_xboole_0(C,D))))&(~r2_hidden(A,D)|~r2_hidden(B,D)))&(~r2_hidden(A,k4_xboole_0(C,D))|~r2_hidden(B,D)))&(~r2_hidden(A,D)|~r2_hidden(B,k4_xboole_0(C,D)))))),
% 134.01/36.09 inference(pre_NNF_transformation,[status(thm)],[f66034])).
% 134.01/36.09 fof(f310177,plain,(
% 134.01/36.09 (((((r2_hidden(sK22356_skl,k2_xboole_0(sK22358_skl,sK22359_skl))&r2_hidden(sK22357_skl,k2_xboole_0(sK22358_skl,sK22359_skl)))&(~r2_hidden(sK22356_skl,k4_xboole_0(sK22358_skl,sK22359_skl))|~r2_hidden(sK22357_skl,k4_xboole_0(sK22358_skl,sK22359_skl))))&(~r2_hidden(sK22356_skl,sK22359_skl)|~r2_hidden(sK22357_skl,sK22359_skl)))&(~r2_hidden(sK22356_skl,k4_xboole_0(sK22358_skl,sK22359_skl))|~r2_hidden(sK22357_skl,sK22359_skl)))&(~r2_hidden(sK22356_skl,sK22359_skl)|~r2_hidden(sK22357_skl,k4_xboole_0(sK22358_skl,sK22359_skl))))),
% 134.01/36.09 inference(skolemize,[status(esa),new_symbols(skolem,[sK22356_skl,sK22357_skl,sK22358_skl,sK22359_skl]),skolemize(A,sK22356_skl),skolemize(B,sK22357_skl),skolemize(C,sK22358_skl),skolemize(D,sK22359_skl)],[f310176])).
% 134.01/36.09 fof(f310178,plain,(
% 134.01/36.09 r2_hidden(sK22356_skl,k2_xboole_0(sK22358_skl,sK22359_skl))),
% 134.01/36.09 inference(cnf_transformation,[status(thm)],[f310177])).
% 134.01/36.09 fof(f310179,plain,(
% 134.01/36.09 r2_hidden(sK22357_skl,k2_xboole_0(sK22358_skl,sK22359_skl))),
% 134.01/36.09 inference(cnf_transformation,[status(thm)],[f310177])).
% 134.01/36.09 fof(f310180,plain,(
% 134.01/36.09 ~r2_hidden(sK22356_skl,k4_xboole_0(sK22358_skl,sK22359_skl))|~r2_hidden(sK22357_skl,k4_xboole_0(sK22358_skl,sK22359_skl))),
% 134.01/36.09 inference(cnf_transformation,[status(thm)],[f310177])).
% 134.01/36.09 fof(f310181,plain,(
% 134.01/36.09 ~r2_hidden(sK22356_skl,sK22359_skl)|~r2_hidden(sK22357_skl,sK22359_skl)),
% 134.01/36.09 inference(cnf_transformation,[status(thm)],[f310177])).
% 134.01/36.09 fof(f310182,plain,(
% 134.01/36.09 ~r2_hidden(sK22356_skl,k4_xboole_0(sK22358_skl,sK22359_skl))|~r2_hidden(sK22357_skl,sK22359_skl)),
% 134.01/36.09 inference(cnf_transformation,[status(thm)],[f310177])).
% 134.01/36.09 fof(f310183,plain,(
% 134.01/36.09 ~r2_hidden(sK22356_skl,sK22359_skl)|~r2_hidden(sK22357_skl,k4_xboole_0(sK22358_skl,sK22359_skl))),
% 134.01/36.09 inference(cnf_transformation,[status(thm)],[f310177])).
% 134.01/36.09 fof(f355638,definition,(
% 134.01/36.09 sQ4292_spl <=> (r2_hidden(sK22356_skl,k4_xboole_0(sK22358_skl,sK22359_skl)))),
% 134.01/36.09 introduced(definition,[new_symbols(definition,[sQ4292_spl])],[split_symbol_definition])).
% 134.01/36.09 fof(f355640,plain,(
% 134.01/36.09 ~r2_hidden(sK22356_skl,k4_xboole_0(sK22358_skl,sK22359_skl))|sQ4292_spl),
% 134.01/36.09 inference(component_clause,[status(thm)],[f355638])).
% 134.01/36.09 fof(f355641,definition,(
% 134.01/36.09 sQ4293_spl <=> (r2_hidden(sK22357_skl,k4_xboole_0(sK22358_skl,sK22359_skl)))),
% 134.01/36.09 introduced(definition,[new_symbols(definition,[sQ4293_spl])],[split_symbol_definition])).
% 134.01/36.09 fof(f355643,plain,(
% 134.01/36.09 ~r2_hidden(sK22357_skl,k4_xboole_0(sK22358_skl,sK22359_skl))|sQ4293_spl),
% 134.01/36.09 inference(component_clause,[status(thm)],[f355641])).
% 134.01/36.09 fof(f355644,plain,(
% 134.01/36.09 ~sQ4292_spl|~sQ4293_spl),
% 134.01/36.09 inference(split_clause,[status(thm)],[f310180,f355638,f355641])).
% 134.01/36.09 fof(f355645,definition,(
% 134.01/36.09 sQ4294_spl <=> (r2_hidden(sK22356_skl,sK22359_skl))),
% 134.01/36.09 introduced(definition,[new_symbols(definition,[sQ4294_spl])],[split_symbol_definition])).
% 134.01/36.09 fof(f355648,definition,(
% 134.01/36.09 sQ4295_spl <=> (r2_hidden(sK22357_skl,sK22359_skl))),
% 134.01/36.09 introduced(definition,[new_symbols(definition,[sQ4295_spl])],[split_symbol_definition])).
% 134.01/36.09 fof(f355651,plain,(
% 134.01/36.09 ~sQ4294_spl|~sQ4295_spl),
% 134.01/36.09 inference(split_clause,[status(thm)],[f310181,f355645,f355648])).
% 134.01/36.09 fof(f355652,plain,(
% 134.01/36.09 ~sQ4292_spl|~sQ4295_spl),
% 134.01/36.09 inference(split_clause,[status(thm)],[f310182,f355638,f355648])).
% 134.01/36.09 fof(f355653,plain,(
% 134.01/36.09 ~sQ4294_spl|~sQ4293_spl),
% 134.01/36.09 inference(split_clause,[status(thm)],[f310183,f355645,f355641])).
% 134.01/36.09 fof(f364186,plain,(
% 134.01/36.09 ![X0,X1,X2]: (~r2_hidden(X0,k2_xboole_0(X1,X2))|r2_hidden(X0,X1)|r2_hidden(X0,X2))),
% 134.01/36.09 inference(destructive_equality_resolution,[status(thm)],[f66132])).
% 134.01/36.09 fof(f364187,plain,(
% 134.01/36.09 ![X0,X1,X2]: (r2_hidden(X0,k2_xboole_0(X1,X2))|~r2_hidden(X0,X1))),
% 134.01/36.09 inference(destructive_equality_resolution,[status(thm)],[f66133])).
% 134.01/36.09 fof(f364194,plain,(
% 134.01/36.09 ![X0,X1,X2]: (r2_hidden(X0,k4_xboole_0(X1,X2))|~r2_hidden(X0,X1)|r2_hidden(X0,X2))),
% 134.01/36.09 inference(destructive_equality_resolution,[status(thm)],[f66152])).
% 134.01/36.09 fof(f382940,plain,(
% 134.01/36.09 r2_hidden(sK22357_skl,sK22358_skl)|r2_hidden(sK22357_skl,sK22359_skl)),
% 134.01/36.09 inference(resolution,[status(thm)],[f364186,f310179])).
% 134.01/36.09 fof(f382941,plain,(
% 134.01/36.09 r2_hidden(sK22356_skl,sK22358_skl)|r2_hidden(sK22356_skl,sK22359_skl)),
% 134.01/36.09 inference(resolution,[status(thm)],[f364186,f310178])).
% 134.01/36.09 fof(f382947,definition,(
% 134.01/36.09 sQ6302_spl <=> (r2_hidden(sK22357_skl,sK22358_skl))),
% 134.01/36.09 introduced(definition,[new_symbols(definition,[sQ6302_spl])],[split_symbol_definition])).
% 134.01/36.09 fof(f382950,plain,(
% 134.01/36.09 sQ6302_spl|sQ4295_spl),
% 134.01/36.09 inference(split_clause,[status(thm)],[f382940,f382947,f355648])).
% 134.01/36.09 fof(f382951,definition,(
% 134.01/36.09 sQ6303_spl <=> (r2_hidden(sK22356_skl,sK22358_skl))),
% 134.01/36.09 introduced(definition,[new_symbols(definition,[sQ6303_spl])],[split_symbol_definition])).
% 134.01/36.09 fof(f382954,plain,(
% 134.01/36.09 sQ6303_spl|sQ4294_spl),
% 134.01/36.09 inference(split_clause,[status(thm)],[f382941,f382951,f355645])).
% 134.01/36.09 fof(f382966,plain,(
% 134.01/36.09 ![X0]: (r2_hidden(sK22357_skl,k4_xboole_0(k2_xboole_0(sK22358_skl,sK22359_skl),X0))|r2_hidden(sK22357_skl,X0))),
% 134.01/36.09 inference(resolution,[status(thm)],[f364194,f310179])).
% 134.01/36.09 fof(f382967,plain,(
% 134.01/36.09 ![X0]: (r2_hidden(sK22356_skl,k4_xboole_0(k2_xboole_0(sK22358_skl,sK22359_skl),X0))|r2_hidden(sK22356_skl,X0))),
% 134.01/36.09 inference(resolution,[status(thm)],[f364194,f310178])).
% 134.01/36.09 fof(f382977,plain,(
% 134.01/36.09 ![X0,X1]: (r2_hidden(sK22357_skl,X0)|r2_hidden(sK22357_skl,k2_xboole_0(k4_xboole_0(k2_xboole_0(sK22358_skl,sK22359_skl),X0),X1)))),
% 134.01/36.09 inference(resolution,[status(thm)],[f382966,f364187])).
% 134.01/36.09 fof(f382981,plain,(
% 134.01/36.09 ![X0,X1]: (r2_hidden(sK22356_skl,X0)|r2_hidden(sK22356_skl,k2_xboole_0(k4_xboole_0(k2_xboole_0(sK22358_skl,sK22359_skl),X0),X1)))),
% 134.01/36.09 inference(resolution,[status(thm)],[f382967,f364187])).
% 134.01/36.09 fof(f382988,plain,(
% 134.01/36.09 ![X0,X1]: (r2_hidden(sK22357_skl,X0)|r2_hidden(sK22357_skl,k4_xboole_0(k2_xboole_0(sK22358_skl,sK22359_skl),X0))|r2_hidden(sK22357_skl,X1))),
% 134.01/36.09 inference(resolution,[status(thm)],[f382977,f364186])).
% 134.01/36.09 fof(f382995,definition,(
% 134.01/36.09 ![X0]: (sQ6304_spl <=> (r2_hidden(sK22357_skl,X0)|r2_hidden(sK22357_skl,k4_xboole_0(k2_xboole_0(sK22358_skl,sK22359_skl),X0))))),
% 134.01/36.09 introduced(definition,[new_symbols(definition,[sQ6304_spl])],[split_symbol_definition])).
% 134.01/36.09 fof(f382998,definition,(
% 134.01/36.09 ![X1]: (sQ6305_spl <=> (r2_hidden(sK22357_skl,X1)))),
% 134.01/36.09 introduced(definition,[new_symbols(definition,[sQ6305_spl])],[split_symbol_definition])).
% 134.01/36.09 fof(f383001,plain,(
% 134.01/36.09 sQ6304_spl|sQ6305_spl),
% 134.01/36.09 inference(split_clause,[status(thm)],[f382988,f382995,f382998])).
% 134.01/36.09 fof(f383006,plain,(
% 134.01/36.09 ![X0,X1]: (r2_hidden(sK22356_skl,X0)|r2_hidden(sK22356_skl,k4_xboole_0(k2_xboole_0(sK22358_skl,sK22359_skl),X0))|r2_hidden(sK22356_skl,X1))),
% 134.01/36.09 inference(resolution,[status(thm)],[f382981,f364186])).
% 134.01/36.09 fof(f383013,definition,(
% 134.01/36.09 ![X0]: (sQ6306_spl <=> (r2_hidden(sK22356_skl,X0)|r2_hidden(sK22356_skl,k4_xboole_0(k2_xboole_0(sK22358_skl,sK22359_skl),X0))))),
% 134.01/36.09 introduced(definition,[new_symbols(definition,[sQ6306_spl])],[split_symbol_definition])).
% 134.01/36.09 fof(f383016,definition,(
% 134.01/36.09 ![X1]: (sQ6307_spl <=> (r2_hidden(sK22356_skl,X1)))),
% 134.01/36.09 introduced(definition,[new_symbols(definition,[sQ6307_spl])],[split_symbol_definition])).
% 134.01/36.09 fof(f383019,plain,(
% 134.01/36.09 sQ6306_spl|sQ6307_spl),
% 134.01/36.09 inference(split_clause,[status(thm)],[f383006,f383013,f383016])).
% 134.01/36.09 fof(f383069,plain,(
% 134.01/36.09 ![X0]: (k1_tarski(X0)=k1_xboole_0|k1_tarski(X0)=k1_xboole_0|k1_xboole_0=k1_xboole_0)),
% 134.01/36.09 inference(resolution,[status(thm)],[f66747,f66247])).
% 134.01/36.09 fof(f383071,plain,(
% 134.01/36.09 ![X0,X1]: (~k1_tarski(X0)=X1|X1=k1_xboole_0|X1=k1_xboole_0|k1_xboole_0=k1_xboole_0)),
% 134.01/36.09 inference(paramodulation,[status(thm)],[f66247,f66747])).
% 134.01/36.09 fof(f383073,definition,(
% 134.01/36.09 ![X0]: (sQ6308_spl <=> (k1_tarski(X0)=k1_xboole_0|k1_tarski(X0)=k1_xboole_0))),
% 134.01/36.09 introduced(definition,[new_symbols(definition,[sQ6308_spl])],[split_symbol_definition])).
% 134.01/36.09 fof(f383076,definition,(
% 134.01/36.09 sQ6309_spl <=> (k1_xboole_0=k1_xboole_0)),
% 134.01/36.09 introduced(definition,[new_symbols(definition,[sQ6309_spl])],[split_symbol_definition])).
% 134.01/36.09 fof(f383079,plain,(
% 134.01/36.09 sQ6308_spl|sQ6309_spl),
% 134.01/36.09 inference(split_clause,[status(thm)],[f383069,f383073,f383076])).
% 134.01/36.09 fof(f383080,definition,(
% 134.01/36.09 ![X0,X1]: (sQ6310_spl <=> (~k1_tarski(X0)=X1|X1=k1_xboole_0|X1=k1_xboole_0))),
% 134.01/36.09 introduced(definition,[new_symbols(definition,[sQ6310_spl])],[split_symbol_definition])).
% 134.01/36.09 fof(f383083,plain,(
% 134.01/36.09 sQ6310_spl|sQ6309_spl),
% 134.01/36.09 inference(split_clause,[status(thm)],[f383071,f383080,f383076])).
% 134.01/36.09 fof(f383304,plain,(
% 134.01/36.09 ![X0,X1]: (r2_hidden(sK22357_skl,k4_xboole_0(k2_xboole_0(sK22358_skl,sK22359_skl),X0))|sK22357_skl=X1|r2_hidden(sK22357_skl,X0))),
% 134.01/36.09 inference(resolution,[status(thm)],[f75240,f382977])).
% 134.01/36.09 fof(f383305,plain,(
% 134.01/36.09 ![X0,X1]: (r2_hidden(sK22356_skl,k4_xboole_0(k2_xboole_0(sK22358_skl,sK22359_skl),X0))|sK22356_skl=X1|r2_hidden(sK22356_skl,X0))),
% 134.01/36.09 inference(resolution,[status(thm)],[f75240,f382981])).
% 134.01/36.09 fof(f383319,definition,(
% 134.01/36.09 ![X1]: (sQ6314_spl <=> (sK22357_skl=X1))),
% 134.01/36.09 introduced(definition,[new_symbols(definition,[sQ6314_spl])],[split_symbol_definition])).
% 134.01/36.09 fof(f383322,plain,(
% 134.01/36.09 sQ6304_spl|sQ6314_spl),
% 134.01/36.09 inference(split_clause,[status(thm)],[f383304,f382995,f383319])).
% 134.01/36.09 fof(f383323,definition,(
% 134.01/36.09 ![X1]: (sQ6315_spl <=> (sK22356_skl=X1))),
% 134.01/36.09 introduced(definition,[new_symbols(definition,[sQ6315_spl])],[split_symbol_definition])).
% 134.01/36.09 fof(f383324,plain,(
% 134.01/36.09 ![X0]: (sK22356_skl=X0|~sQ6315_spl)),
% 134.01/36.09 inference(component_clause,[status(thm)],[f383323])).
% 134.01/36.10 fof(f383326,plain,(
% 134.01/36.10 sQ6306_spl|sQ6315_spl),
% 134.01/36.10 inference(split_clause,[status(thm)],[f383305,f383013,f383323])).
% 134.01/36.10 fof(f384059,plain,(
% 134.01/36.10 ~r2_hidden(sK22356_skl,sK22358_skl)|r2_hidden(sK22356_skl,sK22359_skl)|sQ4292_spl),
% 134.01/36.10 inference(resolution,[status(thm)],[f355640,f364194])).
% 134.01/36.10 fof(f384074,plain,(
% 134.01/36.10 ~sQ6303_spl|sQ4294_spl|sQ4292_spl),
% 134.01/36.10 inference(split_clause,[status(thm)],[f384059,f382951,f355645,f355638])).
% 134.01/36.10 fof(f384075,plain,(
% 134.01/36.10 ~r2_hidden(sK22357_skl,sK22358_skl)|r2_hidden(sK22357_skl,sK22359_skl)|sQ4293_spl),
% 134.01/36.10 inference(resolution,[status(thm)],[f355643,f364194])).
% 134.01/36.10 fof(f384086,plain,(
% 134.01/36.10 ~r2_hidden(sK22356_skl,k4_xboole_0(sK22358_skl,sK22359_skl))|sQ4293_spl|~sQ6315_spl),
% 134.01/36.10 inference(paramodulation,[status(thm)],[f383324,f355643])).
% 134.01/36.10 fof(f384090,plain,(
% 134.01/36.10 ~sQ6302_spl|sQ4295_spl|sQ4293_spl),
% 134.01/36.10 inference(split_clause,[status(thm)],[f384075,f382947,f355648,f355641])).
% 134.01/36.10 fof(f384091,plain,(
% 134.01/36.10 ~sQ4292_spl|sQ4293_spl|~sQ6315_spl),
% 134.01/36.10 inference(split_clause,[status(thm)],[f384086,f355638,f355641,f383323])).
% 87.36/37.49 fof(f384092,plain,(
% 87.36/37.49 $false),
% 87.36/37.49 inference(sat_refutation,[status(thm)],[f355644,f355651,f355652,f355653,f382950,f382954,f383001,f383019,f383079,f383083,f383322,f383326,f384074,f384090,f384091])).
% 87.36/37.49 % SZS output end CNFRefutation for theBenchmark.p
% 25.40/37.76 % Elapsed time: 36.929711 seconds
% 25.40/37.76 % CPU time: 136.517215 seconds
% 25.40/37.76 % Total memory used: 20.744 GB
% 25.40/37.76 % Net memory used: 20.594 GB
%------------------------------------------------------------------------------