%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SYN036-4 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n012.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:18:45 PM UTC 2026
% Result : Unsatisfiable 0.03s 0.31s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SYN036-4 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.02 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.03/0.30 % Computer : n012.cluster.edu
% 0.03/0.30 % Model : x86_64 x86_64
% 0.03/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.30 % Memory : 8046.5625MB
% 0.03/0.30 % OS : Linux 6.8.0-71-generic
% 0.03/0.30 % CPULimit : 300
% 0.03/0.30 % WCLimit : 300
% 0.03/0.30 % DateTime : Mon Sep 21 10:39:37 UTC 2026
% 0.03/0.30 % CPUTime :
% 0.03/0.30 % Drodi V4.1.1
% 0.03/0.31 % Refutation found
% 0.03/0.31 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.03/0.31 % SZS output start CNFRefutation for theBenchmark
% 0.03/0.31 fof(f1,negated_conjecture,(
% 0.03/0.31 (![Y3,Z3]: (( ~ p(cx)| ~ q(cw)| p(Y3)| q(Z3) ) ))),
% 0.03/0.31 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.03/0.31 fof(f2,negated_conjecture,(
% 0.03/0.31 (![Z4,Y3]: (( ~ p(cx)| ~ q(Z4)| p(Y3)| q(cw) ) ))),
% 0.03/0.31 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.03/0.31 fof(f3,negated_conjecture,(
% 0.03/0.31 (![Y4,Z3]: (( ~ p(Y4)| ~ q(cw)| p(cx)| q(Z3) ) ))),
% 0.03/0.31 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.03/0.31 fof(f4,negated_conjecture,(
% 0.03/0.31 (![Y4,Z4]: (( ~ p(Y4)| ~ q(Z4)| p(cx)| q(cw) ) ))),
% 0.03/0.31 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.03/0.31 fof(f5,negated_conjecture,(
% 0.03/0.31 (![X7,Z3]: (( ~ p(cx)| ~ p(X7)| ~ p(fy5(X7))| ~ q(cw)| q(Z3) ) ))),
% 0.03/0.31 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.03/0.31 fof(f6,negated_conjecture,(
% 0.03/0.31 (![X7,Z4]: (( ~ p(cx)| ~ p(X7)| ~ p(fy5(X7))| ~ q(Z4)| q(cw) ) ))),
% 0.03/0.31 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.03/0.31 fof(f7,negated_conjecture,(
% 0.03/0.31 (![W9,Y3]: (( ~ p(cx)| ~ q(cw)| ~ q(W9)| ~ q(fz5(W9))| p(Y3) ) ))),
% 0.03/0.31 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.03/0.31 fof(f10,negated_conjecture,(
% 0.03/0.31 (![Y1,W3]: (( ~ p(cx)| p(Y1)| q(cw)| q(W3)| q(fz(W3)) ) ))),
% 0.03/0.31 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.03/0.31 fof(f15,negated_conjecture,(
% 0.03/0.31 (![Y2,W3]: (( ~ p(Y2)| p(cx)| q(cw)| q(W3)| q(fz(W3)) ) ))),
% 0.03/0.31 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.03/0.31 fof(f16,negated_conjecture,(
% 0.03/0.31 (![Y4,W9]: (( ~ p(Y4)| ~ q(cw)| ~ q(W9)| ~ q(fz5(W9))| p(cx) ) ))),
% 0.03/0.31 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.03/0.31 fof(f19,negated_conjecture,(
% 0.03/0.31 (![X1,Z1]: (( ~ q(cw)| p(cx)| p(X1)| p(fy(X1))| q(Z1) ) ))),
% 0.03/0.31 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.03/0.31 fof(f20,negated_conjecture,(
% 0.03/0.31 (![Z2,X1]: (( ~ q(Z2)| p(cx)| p(X1)| p(fy(X1))| q(cw) ) ))),
% 0.03/0.31 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.03/0.31 fof(f21,negated_conjecture,(
% 0.03/0.31 (![X1,W3]: (( ~ p(cx)| ~ p(X1)| ~ p(fy(X1))| ~ q(W3)| ~ q(fz(W3))| q(cw) ) ))),
% 0.03/0.31 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.03/0.31 fof(f22,negated_conjecture,(
% 0.03/0.31 (![X1,W3]: (( ~ p(cx)| ~ p(X1)| ~ p(fy(X1))| q(cw)| q(W3)| q(fz(W3)) ) ))),
% 0.03/0.31 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.03/0.31 fof(f23,negated_conjecture,(
% 0.03/0.31 (![X7,W9]: (( ~ p(cx)| ~ p(X7)| ~ p(fy5(X7))| ~ q(cw)| ~ q(W9)| ~ q(fz5(W9)) ) ))),
% 0.03/0.31 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.03/0.31 fof(f30,negated_conjecture,(
% 0.03/0.31 (![W3,X1]: (( ~ q(cw)| ~ q(W3)| ~ q(fz(W3))| p(cx)| p(X1)| p(fy(X1)) ) ))),
% 0.03/0.31 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.03/0.31 fof(f32,negated_conjecture,(
% 0.03/0.31 (![X7,W9]: (( p(cx)| p(X7)| p(fy5(X7))| q(cw)| q(W9)| q(fz5(W9)) ) ))),
% 0.03/0.31 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.03/0.31 fof(f33,plain,(
% 0.03/0.31 ((~p(cx)|~q(cw))|(![Y3]: p(Y3)))|(![Z3]: q(Z3))),
% 0.03/0.31 inference(miniscoping,[status(thm)],[f1])).
% 0.03/0.31 fof(f34,plain,(
% 0.03/0.31 ![X0,X1]: (~p(cx)|~q(cw)|p(X0)|q(X1))),
% 0.03/0.31 inference(cnf_transformation,[status(thm)],[f33])).
% 0.03/0.31 fof(f35,plain,(
% 0.03/0.31 ((~p(cx)|(![Z4]: ~q(Z4)))|(![Y3]: p(Y3)))|q(cw)),
% 0.03/0.31 inference(miniscoping,[status(thm)],[f2])).
% 0.03/0.31 fof(f36,plain,(
% 0.03/0.31 ![X0,X1]: (~p(cx)|~q(X0)|p(X1)|q(cw))),
% 0.03/0.31 inference(cnf_transformation,[status(thm)],[f35])).
% 0.03/0.31 fof(f37,plain,(
% 0.03/0.31 (((![Y4]: ~p(Y4))|~q(cw))|p(cx))|(![Z3]: q(Z3))),
% 0.03/0.31 inference(miniscoping,[status(thm)],[f3])).
% 0.03/0.31 fof(f38,plain,(
% 0.03/0.31 ![X0,X1]: (~p(X0)|~q(cw)|p(cx)|q(X1))),
% 0.03/0.31 inference(cnf_transformation,[status(thm)],[f37])).
% 0.03/0.31 fof(f39,plain,(
% 0.03/0.31 (((![Y4]: ~p(Y4))|(![Z4]: ~q(Z4)))|p(cx))|q(cw)),
% 0.03/0.31 inference(miniscoping,[status(thm)],[f4])).
% 0.03/0.31 fof(f40,plain,(
% 0.03/0.31 ![X0,X1]: (~p(X0)|~q(X1)|p(cx)|q(cw))),
% 0.03/0.31 inference(cnf_transformation,[status(thm)],[f39])).
% 0.03/0.31 fof(f41,plain,(
% 0.03/0.31 ((![X7]: ((~p(cx)|~p(X7))|~p(fy5(X7))))|~q(cw))|(![Z3]: q(Z3))),
% 0.03/0.31 inference(miniscoping,[status(thm)],[f5])).
% 0.03/0.31 fof(f42,plain,(
% 0.03/0.31 ![X0,X1]: (~p(cx)|~p(X0)|~p(fy5(X0))|~q(cw)|q(X1))),
% 0.03/0.31 inference(cnf_transformation,[status(thm)],[f41])).
% 0.03/0.31 fof(f43,plain,(
% 0.03/0.31 ((![X7]: ((~p(cx)|~p(X7))|~p(fy5(X7))))|(![Z4]: ~q(Z4)))|q(cw)),
% 0.03/0.31 inference(miniscoping,[status(thm)],[f6])).
% 0.03/0.31 fof(f44,plain,(
% 0.03/0.31 ![X0,X1]: (~p(cx)|~p(X0)|~p(fy5(X0))|~q(X1)|q(cw))),
% 0.03/0.31 inference(cnf_transformation,[status(thm)],[f43])).
% 0.03/0.31 fof(f45,plain,(
% 0.03/0.31 (![W9]: (((~p(cx)|~q(cw))|~q(W9))|~q(fz5(W9))))|(![Y3]: p(Y3))),
% 0.03/0.31 inference(miniscoping,[status(thm)],[f7])).
% 0.03/0.31 fof(f46,plain,(
% 0.03/0.31 ![X0,X1]: (~p(cx)|~q(cw)|~q(X0)|~q(fz5(X0))|p(X1))),
% 0.03/0.31 inference(cnf_transformation,[status(thm)],[f45])).
% 0.03/0.31 fof(f51,plain,(
% 0.03/0.31 ![W3]: ((((~p(cx)|(![Y1]: p(Y1)))|q(cw))|q(W3))|q(fz(W3)))),
% 0.03/0.31 inference(miniscoping,[status(thm)],[f10])).
% 0.03/0.31 fof(f52,plain,(
% 0.03/0.31 ![X0,X1]: (~p(cx)|p(X0)|q(cw)|q(X1)|q(fz(X1)))),
% 0.03/0.31 inference(cnf_transformation,[status(thm)],[f51])).
% 0.03/0.31 fof(f61,plain,(
% 0.03/0.31 ![W3]: (((((![Y2]: ~p(Y2))|p(cx))|q(cw))|q(W3))|q(fz(W3)))),
% 0.03/0.31 inference(miniscoping,[status(thm)],[f15])).
% 0.03/0.31 fof(f62,plain,(
% 0.03/0.31 ![X0,X1]: (~p(X0)|p(cx)|q(cw)|q(X1)|q(fz(X1)))),
% 0.03/0.31 inference(cnf_transformation,[status(thm)],[f61])).
% 0.03/0.31 fof(f63,plain,(
% 0.03/0.31 (![W9]: ((((![Y4]: ~p(Y4))|~q(cw))|~q(W9))|~q(fz5(W9))))|p(cx)),
% 0.03/0.31 inference(miniscoping,[status(thm)],[f16])).
% 0.03/0.31 fof(f64,plain,(
% 0.03/0.32 ![X0,X1]: (~p(X0)|~q(cw)|~q(X1)|~q(fz5(X1))|p(cx))),
% 0.03/0.32 inference(cnf_transformation,[status(thm)],[f63])).
% 0.03/0.32 fof(f69,plain,(
% 0.03/0.32 (![X1]: (((~q(cw)|p(cx))|p(X1))|p(fy(X1))))|(![Z1]: q(Z1))),
% 0.03/0.32 inference(miniscoping,[status(thm)],[f19])).
% 0.03/0.32 fof(f70,plain,(
% 0.03/0.32 ![X0,X1]: (~q(cw)|p(cx)|p(X0)|p(fy(X0))|q(X1))),
% 0.03/0.32 inference(cnf_transformation,[status(thm)],[f69])).
% 0.03/0.32 fof(f71,plain,(
% 0.03/0.32 (![X1]: ((((![Z2]: ~q(Z2))|p(cx))|p(X1))|p(fy(X1))))|q(cw)),
% 0.03/0.32 inference(miniscoping,[status(thm)],[f20])).
% 0.03/0.32 fof(f72,plain,(
% 0.03/0.32 ![X0,X1]: (~q(X0)|p(cx)|p(X1)|p(fy(X1))|q(cw))),
% 0.03/0.32 inference(cnf_transformation,[status(thm)],[f71])).
% 0.03/0.32 fof(f73,plain,(
% 0.03/0.32 (![W3]: (((![X1]: ((~p(cx)|~p(X1))|~p(fy(X1))))|~q(W3))|~q(fz(W3))))|q(cw)),
% 0.03/0.32 inference(miniscoping,[status(thm)],[f21])).
% 0.03/0.32 fof(f74,plain,(
% 0.03/0.32 ![X0,X1]: (~p(cx)|~p(X0)|~p(fy(X0))|~q(X1)|~q(fz(X1))|q(cw))),
% 0.03/0.32 inference(cnf_transformation,[status(thm)],[f73])).
% 0.03/0.32 fof(f75,plain,(
% 0.03/0.32 ![W3]: ((((![X1]: ((~p(cx)|~p(X1))|~p(fy(X1))))|q(cw))|q(W3))|q(fz(W3)))),
% 0.03/0.32 inference(miniscoping,[status(thm)],[f22])).
% 0.03/0.32 fof(f76,plain,(
% 0.03/0.32 ![X0,X1]: (~p(cx)|~p(X0)|~p(fy(X0))|q(cw)|q(X1)|q(fz(X1)))),
% 0.03/0.32 inference(cnf_transformation,[status(thm)],[f75])).
% 0.03/0.32 fof(f77,plain,(
% 0.03/0.32 ![W9]: ((((![X7]: ((~p(cx)|~p(X7))|~p(fy5(X7))))|~q(cw))|~q(W9))|~q(fz5(W9)))),
% 0.03/0.32 inference(miniscoping,[status(thm)],[f23])).
% 0.03/0.32 fof(f78,plain,(
% 0.03/0.32 ![X0,X1]: (~p(cx)|~p(X0)|~p(fy5(X0))|~q(cw)|~q(X1)|~q(fz5(X1)))),
% 0.03/0.32 inference(cnf_transformation,[status(thm)],[f77])).
% 0.03/0.32 fof(f91,plain,(
% 0.03/0.32 ![X1]: ((((![W3]: ((~q(cw)|~q(W3))|~q(fz(W3))))|p(cx))|p(X1))|p(fy(X1)))),
% 0.03/0.32 inference(miniscoping,[status(thm)],[f30])).
% 0.03/0.32 fof(f92,plain,(
% 0.03/0.32 ![X0,X1]: (~q(cw)|~q(X0)|~q(fz(X0))|p(cx)|p(X1)|p(fy(X1)))),
% 0.03/0.32 inference(cnf_transformation,[status(thm)],[f91])).
% 0.03/0.32 fof(f95,plain,(
% 0.03/0.32 ![W9]: ((((![X7]: ((p(cx)|p(X7))|p(fy5(X7))))|q(cw))|q(W9))|q(fz5(W9)))),
% 0.03/0.32 inference(miniscoping,[status(thm)],[f32])).
% 0.03/0.32 fof(f96,plain,(
% 0.03/0.32 ![X0,X1]: (p(cx)|p(X0)|p(fy5(X0))|q(cw)|q(X1)|q(fz5(X1)))),
% 0.03/0.32 inference(cnf_transformation,[status(thm)],[f95])).
% 0.03/0.32 fof(f97,definition,(
% 0.03/0.32 sQ0_spl <=> (p(cx))),
% 0.03/0.32 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.03/0.32 fof(f100,definition,(
% 0.03/0.32 sQ1_spl <=> (q(cw))),
% 0.03/0.32 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.03/0.32 fof(f103,definition,(
% 0.03/0.32 ![X0]: (sQ2_spl <=> (p(X0)))),
% 0.03/0.32 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.03/0.32 fof(f104,plain,(
% 0.03/0.32 ![X0]: (p(X0)|~sQ2_spl)),
% 0.03/0.32 inference(component_clause,[status(thm)],[f103])).
% 0.03/0.32 fof(f106,definition,(
% 0.03/0.32 ![X1]: (sQ3_spl <=> (q(X1)))),
% 0.03/0.32 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.03/0.32 fof(f107,plain,(
% 0.03/0.32 ![X0]: (q(X0)|~sQ3_spl)),
% 0.03/0.32 inference(component_clause,[status(thm)],[f106])).
% 0.03/0.32 fof(f109,plain,(
% 0.03/0.32 ~sQ0_spl|~sQ1_spl|sQ2_spl|sQ3_spl),
% 0.03/0.32 inference(split_clause,[status(thm)],[f34,f97,f100,f103,f106])).
% 0.03/0.32 fof(f110,definition,(
% 0.03/0.32 ![X0]: (sQ4_spl <=> (~q(X0)))),
% 0.03/0.32 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.03/0.32 fof(f111,plain,(
% 0.03/0.32 ![X0]: (~q(X0)|~sQ4_spl)),
% 0.03/0.32 inference(component_clause,[status(thm)],[f110])).
% 0.03/0.32 fof(f113,plain,(
% 0.03/0.32 ~sQ0_spl|sQ4_spl|sQ2_spl|sQ1_spl),
% 0.03/0.32 inference(split_clause,[status(thm)],[f36,f97,f110,f103,f100])).
% 0.03/0.32 fof(f114,definition,(
% 0.03/0.32 ![X0]: (sQ5_spl <=> (~p(X0)))),
% 0.03/0.32 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.03/0.32 fof(f115,plain,(
% 0.03/0.32 ![X0]: (~p(X0)|~sQ5_spl)),
% 0.03/0.32 inference(component_clause,[status(thm)],[f114])).
% 0.03/0.32 fof(f117,plain,(
% 0.03/0.32 sQ5_spl|~sQ1_spl|sQ0_spl|sQ3_spl),
% 0.03/0.32 inference(split_clause,[status(thm)],[f38,f114,f100,f97,f106])).
% 0.03/0.32 fof(f118,plain,(
% 0.03/0.32 sQ5_spl|sQ4_spl|sQ0_spl|sQ1_spl),
% 0.03/0.32 inference(split_clause,[status(thm)],[f40,f114,f110,f97,f100])).
% 0.03/0.32 fof(f119,definition,(
% 0.03/0.32 ![X0]: (sQ6_spl <=> (~p(X0)|~p(fy5(X0))))),
% 0.03/0.32 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.03/0.32 fof(f120,plain,(
% 0.03/0.32 ![X0]: (~p(X0)|~p(fy5(X0))|~sQ6_spl)),
% 0.03/0.32 inference(component_clause,[status(thm)],[f119])).
% 0.03/0.32 fof(f122,plain,(
% 0.03/0.32 ~sQ0_spl|sQ6_spl|~sQ1_spl|sQ3_spl),
% 0.03/0.32 inference(split_clause,[status(thm)],[f42,f97,f119,f100,f106])).
% 0.03/0.32 fof(f123,plain,(
% 0.03/0.32 ~sQ0_spl|sQ6_spl|sQ4_spl|sQ1_spl),
% 0.03/0.32 inference(split_clause,[status(thm)],[f44,f97,f119,f110,f100])).
% 0.03/0.32 fof(f124,definition,(
% 0.03/0.32 ![X0]: (sQ7_spl <=> (~q(X0)|~q(fz5(X0))))),
% 0.03/0.32 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.03/0.32 fof(f125,plain,(
% 0.03/0.32 ![X0]: (~q(X0)|~q(fz5(X0))|~sQ7_spl)),
% 0.03/0.32 inference(component_clause,[status(thm)],[f124])).
% 0.03/0.32 fof(f127,plain,(
% 0.03/0.32 ~sQ0_spl|~sQ1_spl|sQ7_spl|sQ2_spl),
% 0.03/0.32 inference(split_clause,[status(thm)],[f46,f97,f100,f124,f103])).
% 0.03/0.32 fof(f128,definition,(
% 0.03/0.32 ![X2]: (sQ8_spl <=> (q(X2)|q(fz(X2))))),
% 0.03/0.32 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.03/0.32 fof(f129,plain,(
% 0.03/0.32 ![X0]: (q(X0)|q(fz(X0))|~sQ8_spl)),
% 0.03/0.32 inference(component_clause,[status(thm)],[f128])).
% 0.03/0.32 fof(f132,definition,(
% 0.03/0.32 ![X0]: (sQ9_spl <=> (~q(X0)|~q(fz(X0))))),
% 0.03/0.32 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.03/0.32 fof(f133,plain,(
% 0.03/0.32 ![X0]: (~q(X0)|~q(fz(X0))|~sQ9_spl)),
% 0.03/0.32 inference(component_clause,[status(thm)],[f132])).
% 0.03/0.32 fof(f136,plain,(
% 0.03/0.32 ~sQ0_spl|sQ2_spl|sQ1_spl|sQ8_spl),
% 0.03/0.32 inference(split_clause,[status(thm)],[f52,f97,f103,f100,f128])).
% 0.03/0.32 fof(f137,definition,(
% 0.03/0.32 ![X0]: (sQ10_spl <=> (~p(X0)|~p(fy(X0))))),
% 0.03/0.32 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.03/0.32 fof(f138,plain,(
% 0.03/0.32 ![X0]: (~p(X0)|~p(fy(X0))|~sQ10_spl)),
% 0.03/0.32 inference(component_clause,[status(thm)],[f137])).
% 0.03/0.32 fof(f141,definition,(
% 0.03/0.32 ![X1]: (sQ11_spl <=> (p(X1)|p(fy(X1))))),
% 0.03/0.32 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.03/0.32 fof(f142,plain,(
% 0.03/0.32 ![X0]: (p(X0)|p(fy(X0))|~sQ11_spl)),
% 0.03/0.32 inference(component_clause,[status(thm)],[f141])).
% 0.03/0.32 fof(f149,definition,(
% 0.03/0.32 ![X2]: (sQ13_spl <=> (p(X2)|p(fy5(X2))))),
% 0.03/0.32 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.03/0.32 fof(f150,plain,(
% 0.03/0.32 ![X0]: (p(X0)|p(fy5(X0))|~sQ13_spl)),
% 0.03/0.32 inference(component_clause,[status(thm)],[f149])).
% 0.03/0.32 fof(f153,plain,(
% 0.03/0.32 sQ5_spl|sQ0_spl|sQ1_spl|sQ8_spl),
% 0.03/0.32 inference(split_clause,[status(thm)],[f62,f114,f97,f100,f128])).
% 0.03/0.32 fof(f154,plain,(
% 0.03/0.32 sQ5_spl|~sQ1_spl|sQ7_spl|sQ0_spl),
% 0.03/0.32 inference(split_clause,[status(thm)],[f64,f114,f100,f124,f97])).
% 0.03/0.32 fof(f155,definition,(
% 0.03/0.32 ![X2]: (sQ14_spl <=> (q(X2)|q(fz5(X2))))),
% 0.03/0.32 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.03/0.32 fof(f156,plain,(
% 0.03/0.32 ![X0]: (q(X0)|q(fz5(X0))|~sQ14_spl)),
% 0.03/0.32 inference(component_clause,[status(thm)],[f155])).
% 0.03/0.32 fof(f160,plain,(
% 0.03/0.32 ~sQ1_spl|sQ0_spl|sQ11_spl|sQ3_spl),
% 0.03/0.32 inference(split_clause,[status(thm)],[f70,f100,f97,f141,f106])).
% 0.03/0.32 fof(f161,plain,(
% 0.03/0.32 sQ4_spl|sQ0_spl|sQ11_spl|sQ1_spl),
% 0.03/0.32 inference(split_clause,[status(thm)],[f72,f110,f97,f141,f100])).
% 0.03/0.32 fof(f162,plain,(
% 0.03/0.32 ~sQ0_spl|sQ10_spl|sQ9_spl|sQ1_spl),
% 0.03/0.32 inference(split_clause,[status(thm)],[f74,f97,f137,f132,f100])).
% 0.03/0.32 fof(f163,plain,(
% 0.03/0.32 ~sQ0_spl|sQ10_spl|sQ1_spl|sQ8_spl),
% 0.03/0.32 inference(split_clause,[status(thm)],[f76,f97,f137,f100,f128])).
% 0.03/0.32 fof(f164,plain,(
% 0.03/0.32 ~sQ0_spl|sQ6_spl|~sQ1_spl|sQ7_spl),
% 0.03/0.32 inference(split_clause,[status(thm)],[f78,f97,f119,f100,f124])).
% 0.03/0.32 fof(f171,plain,(
% 0.03/0.32 ~sQ1_spl|sQ9_spl|sQ0_spl|sQ11_spl),
% 0.03/0.32 inference(split_clause,[status(thm)],[f92,f100,f132,f97,f141])).
% 0.03/0.32 fof(f173,plain,(
% 0.03/0.32 sQ0_spl|sQ13_spl|sQ1_spl|sQ14_spl),
% 0.03/0.32 inference(split_clause,[status(thm)],[f96,f97,f149,f100,f155])).
% 0.03/0.32 fof(f174,plain,(
% 0.03/0.32 $false|~sQ3_spl|~sQ4_spl),
% 0.03/0.32 inference(forward_subsumption_resolution,[status(thm)],[f111,f107])).
% 0.03/0.32 fof(f175,plain,(
% 0.03/0.32 ~sQ3_spl|~sQ4_spl),
% 0.03/0.32 inference(contradiction_clause,[status(thm)],[f174])).
% 0.03/0.32 fof(f176,plain,(
% 0.03/0.32 $false|~sQ5_spl|~sQ2_spl),
% 0.03/0.32 inference(forward_subsumption_resolution,[status(thm)],[f104,f115])).
% 0.03/0.32 fof(f177,plain,(
% 0.03/0.32 ~sQ5_spl|~sQ2_spl),
% 0.03/0.32 inference(contradiction_clause,[status(thm)],[f176])).
% 0.03/0.32 fof(f178,plain,(
% 0.03/0.32 ![X0]: (q(fz(X0))|~sQ4_spl|~sQ8_spl)),
% 0.03/0.32 inference(forward_subsumption_resolution,[status(thm)],[f129,f111])).
% 0.03/0.32 fof(f179,plain,(
% 0.03/0.32 $false|~sQ8_spl|~sQ4_spl),
% 0.03/0.32 inference(resolution,[status(thm)],[f178,f111])).
% 0.03/0.32 fof(f180,plain,(
% 0.03/0.32 ~sQ8_spl|~sQ4_spl),
% 0.03/0.32 inference(contradiction_clause,[status(thm)],[f179])).
% 0.03/0.32 fof(f181,plain,(
% 0.03/0.32 ![X0]: (~p(fy(X0))|~sQ2_spl|~sQ10_spl)),
% 0.03/0.32 inference(forward_subsumption_resolution,[status(thm)],[f138,f104])).
% 0.03/0.32 fof(f182,plain,(
% 0.03/0.32 $false|~sQ10_spl|~sQ2_spl),
% 0.03/0.32 inference(resolution,[status(thm)],[f181,f104])).
% 0.03/0.32 fof(f183,plain,(
% 0.03/0.32 ~sQ10_spl|~sQ2_spl),
% 0.03/0.32 inference(contradiction_clause,[status(thm)],[f182])).
% 0.03/0.32 fof(f184,plain,(
% 0.03/0.32 ![X0]: (p(fy5(X0))|~sQ5_spl|~sQ13_spl)),
% 0.03/0.32 inference(forward_subsumption_resolution,[status(thm)],[f150,f115])).
% 0.03/0.32 fof(f185,plain,(
% 0.03/0.32 $false|~sQ13_spl|~sQ5_spl),
% 0.03/0.32 inference(resolution,[status(thm)],[f184,f115])).
% 0.03/0.32 fof(f186,plain,(
% 0.03/0.32 ~sQ13_spl|~sQ5_spl),
% 0.03/0.32 inference(contradiction_clause,[status(thm)],[f185])).
% 0.03/0.32 fof(f187,plain,(
% 0.03/0.32 ![X0]: (~q(fz(X0))|~sQ3_spl|~sQ9_spl)),
% 0.03/0.32 inference(forward_subsumption_resolution,[status(thm)],[f133,f107])).
% 0.03/0.32 fof(f188,plain,(
% 0.03/0.32 $false|~sQ9_spl|~sQ3_spl),
% 0.03/0.32 inference(resolution,[status(thm)],[f187,f107])).
% 0.03/0.32 fof(f189,plain,(
% 0.03/0.32 ~sQ9_spl|~sQ3_spl),
% 0.03/0.32 inference(contradiction_clause,[status(thm)],[f188])).
% 0.03/0.32 fof(f190,plain,(
% 0.03/0.32 ![X0]: (~p(fy5(X0))|~sQ2_spl|~sQ6_spl)),
% 0.03/0.32 inference(forward_subsumption_resolution,[status(thm)],[f120,f104])).
% 0.03/0.32 fof(f191,plain,(
% 0.03/0.32 $false|~sQ6_spl|~sQ2_spl),
% 0.03/0.32 inference(resolution,[status(thm)],[f190,f104])).
% 0.03/0.32 fof(f192,plain,(
% 0.03/0.32 ~sQ6_spl|~sQ2_spl),
% 0.03/0.32 inference(contradiction_clause,[status(thm)],[f191])).
% 0.03/0.32 fof(f193,plain,(
% 0.03/0.32 ![X0]: (p(fy(X0))|~sQ5_spl|~sQ11_spl)),
% 0.03/0.32 inference(backward_subsumption_resolution,[status(thm)],[f142,f115])).
% 0.03/0.32 fof(f194,plain,(
% 0.03/0.32 $false|~sQ5_spl|~sQ11_spl),
% 0.03/0.32 inference(forward_subsumption_resolution,[status(thm)],[f193,f115])).
% 0.03/0.32 fof(f195,plain,(
% 0.03/0.32 ~sQ5_spl|~sQ11_spl),
% 0.03/0.32 inference(contradiction_clause,[status(thm)],[f194])).
% 0.03/0.32 fof(f196,plain,(
% 0.03/0.32 ![X0]: (~q(fz5(X0))|~sQ3_spl|~sQ7_spl)),
% 0.03/0.32 inference(backward_subsumption_resolution,[status(thm)],[f125,f107])).
% 0.03/0.32 fof(f197,plain,(
% 0.03/0.32 $false|~sQ3_spl|~sQ7_spl),
% 0.03/0.32 inference(forward_subsumption_resolution,[status(thm)],[f196,f107])).
% 0.03/0.32 fof(f198,plain,(
% 0.03/0.32 ~sQ3_spl|~sQ7_spl),
% 0.03/0.32 inference(contradiction_clause,[status(thm)],[f197])).
% 0.03/0.32 fof(f199,plain,(
% 0.03/0.32 ![X0]: (q(fz5(X0))|~sQ4_spl|~sQ14_spl)),
% 0.03/0.32 inference(backward_subsumption_resolution,[status(thm)],[f156,f111])).
% 0.03/0.32 fof(f200,plain,(
% 0.03/0.32 $false|~sQ4_spl|~sQ14_spl),
% 0.03/0.32 inference(forward_subsumption_resolution,[status(thm)],[f199,f111])).
% 0.03/0.32 fof(f201,plain,(
% 0.03/0.32 ~sQ4_spl|~sQ14_spl),
% 0.03/0.32 inference(contradiction_clause,[status(thm)],[f200])).
% 0.03/0.32 fof(f202,plain,(
% 0.03/0.32 $false),
% 0.03/0.32 inference(sat_refutation,[status(thm)],[f109,f113,f117,f118,f122,f123,f127,f136,f153,f154,f160,f161,f162,f163,f164,f171,f173,f175,f177,f180,f183,f186,f189,f192,f195,f198,f201])).
% 0.03/0.32 % SZS output end CNFRefutation for theBenchmark.p
% 0.03/0.33 % Elapsed time: 0.026901 seconds
% 0.03/0.33 % CPU time: 0.053085 seconds
% 0.03/0.33 % Total memory used: 13.651 MB
% 0.03/0.33 % Net memory used: 13.478 MB
%------------------------------------------------------------------------------