%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : HWV005-2 : TPTP v9.3.1. Bugfixed v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/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 12:46:38 PM UTC 2026
% Result : Unsatisfiable 0.03s 0.94s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : HWV005-2 : TPTP v9.3.1. Bugfixed v2.7.0.
% 0.00/0.02 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.03/0.91 % Computer : n012.cluster.edu
% 0.03/0.91 % Model : x86_64 x86_64
% 0.03/0.91 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.91 % Memory : 8046.5625MB
% 0.03/0.91 % OS : Linux 6.8.0-71-generic
% 0.03/0.91 % CPULimit : 300
% 0.03/0.91 % WCLimit : 300
% 0.03/0.91 % DateTime : Sun Sep 20 20:46:54 UTC 2026
% 0.03/0.92 % CPUTime :
% 0.03/0.92 % Drodi V4.1.1
% 0.03/0.94 % Refutation found
% 0.03/0.94 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.03/0.94 % SZS output start CNFRefutation for theBenchmark
% 0.03/0.94 fof(f1,axiom,(
% 0.03/0.94 (![P1,P2]: (( ~ connection(P1,P2)| ~ zero(P1)| zero(P2) ) ))),
% 0.03/0.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.94 fof(f2,axiom,(
% 0.03/0.94 (![P1,P2]: (( ~ connection(P1,P2)| ~ one(P1)| one(P2) ) ))),
% 0.03/0.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.94 fof(f5,axiom,(
% 0.03/0.94 (![P]: (( ~ zero(P)| ~ one(P) ) ))),
% 0.03/0.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.94 fof(f9,axiom,(
% 0.03/0.94 (![K]: (( ~ and_ok(K)| ~ zero(out1(K))| zero(in1(K))| zero(in2(K)) ) ))),
% 0.03/0.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.94 fof(f13,axiom,(
% 0.03/0.94 (![K]: (( ~ logic_and(K)| and_ok(K)| abnormal(K) ) ))),
% 0.03/0.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.94 fof(f14,axiom,(
% 0.03/0.94 (![K]: (( ~ or_ok(K)| ~ one(in1(K))| one(out1(K)) ) ))),
% 0.03/0.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.94 fof(f21,axiom,(
% 0.03/0.94 (![K]: (( ~ logic_or(K)| or_ok(K)| abnormal(K) ) ))),
% 0.03/0.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.94 fof(f22,axiom,(
% 0.03/0.94 (![K]: (( ~ not_ok(K)| ~ zero(in1(K))| one(out1(K)) ) ))),
% 0.03/0.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.94 fof(f27,axiom,(
% 0.03/0.94 (![K]: (( ~ logic_not(K)| not_ok(K)| abnormal(K) ) ))),
% 0.03/0.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.94 fof(f28,axiom,(
% 0.03/0.94 (![X]: (( ~ halfadder(X)| logic_and(and1(X)) ) ))),
% 0.03/0.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.94 fof(f30,axiom,(
% 0.03/0.94 (![X]: (( ~ halfadder(X)| logic_not(not1(X)) ) ))),
% 0.03/0.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.94 fof(f31,axiom,(
% 0.03/0.94 (![X]: (( ~ halfadder(X)| logic_or(or1(X)) ) ))),
% 0.03/0.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.94 fof(f32,axiom,(
% 0.03/0.94 (![X]: (( ~ halfadder(X)| connection(in1(X),in1(or1(X))) ) ))),
% 0.03/0.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.94 fof(f36,axiom,(
% 0.03/0.94 (![X]: (( ~ halfadder(X)| connection(outs(X),out1(and1(X))) ) ))),
% 0.03/0.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.94 fof(f37,axiom,(
% 0.03/0.94 (![X]: (( ~ halfadder(X)| connection(outc(X),out1(and2(X))) ) ))),
% 0.03/0.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.94 fof(f38,axiom,(
% 0.03/0.94 (![X]: (( ~ halfadder(X)| connection(out1(or1(X)),in1(and1(X))) ) ))),
% 0.03/0.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.94 fof(f39,axiom,(
% 0.03/0.94 (![X]: (( ~ halfadder(X)| connection(out1(and2(X)),in1(not1(X))) ) ))),
% 0.03/0.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.94 fof(f40,axiom,(
% 0.03/0.94 (![X]: (( ~ halfadder(X)| connection(out1(not1(X)),in2(and1(X))) ) ))),
% 0.03/0.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.94 fof(f41,hypothesis,(
% 0.03/0.94 halfadder(h) ),
% 0.03/0.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.94 fof(f42,hypothesis,(
% 0.03/0.94 one(in1(h)) ),
% 0.03/0.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.94 fof(f44,hypothesis,(
% 0.03/0.94 zero(outs(h)) ),
% 0.03/0.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.94 fof(f45,hypothesis,(
% 0.03/0.94 zero(outc(h)) ),
% 0.03/0.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.94 fof(f46,negated_conjecture,(
% 0.03/0.94 ~ abnormal(and1(h)) ),
% 0.03/0.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.94 fof(f47,negated_conjecture,(
% 0.03/0.94 ~ abnormal(not1(h)) ),
% 0.03/0.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.94 fof(f48,negated_conjecture,(
% 0.03/0.94 ~ abnormal(or1(h)) ),
% 0.03/0.94 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.03/0.94 fof(f49,plain,(
% 0.03/0.94 ![P2]: ((![P1]: (~connection(P1,P2)|~zero(P1)))|zero(P2))),
% 0.03/0.94 inference(miniscoping,[status(thm)],[f1])).
% 0.03/0.94 fof(f50,plain,(
% 0.03/0.94 ![X0,X1]: (~connection(X0,X1)|~zero(X0)|zero(X1))),
% 0.03/0.94 inference(cnf_transformation,[status(thm)],[f49])).
% 0.03/0.94 fof(f51,plain,(
% 0.03/0.94 ![P2]: ((![P1]: (~connection(P1,P2)|~one(P1)))|one(P2))),
% 0.03/0.94 inference(miniscoping,[status(thm)],[f2])).
% 0.03/0.94 fof(f52,plain,(
% 0.03/0.94 ![X0,X1]: (~connection(X0,X1)|~one(X0)|one(X1))),
% 0.03/0.94 inference(cnf_transformation,[status(thm)],[f51])).
% 0.03/0.94 fof(f57,plain,(
% 0.03/0.94 ![X0]: (~zero(X0)|~one(X0))),
% 0.03/0.94 inference(cnf_transformation,[status(thm)],[f5])).
% 0.03/0.94 fof(f61,plain,(
% 0.03/0.94 ![X0]: (~and_ok(X0)|~zero(out1(X0))|zero(in1(X0))|zero(in2(X0)))),
% 0.03/0.94 inference(cnf_transformation,[status(thm)],[f9])).
% 0.03/0.94 fof(f65,plain,(
% 0.03/0.94 ![X0]: (~logic_and(X0)|and_ok(X0)|abnormal(X0))),
% 0.03/0.94 inference(cnf_transformation,[status(thm)],[f13])).
% 0.03/0.94 fof(f66,plain,(
% 0.03/0.94 ![X0]: (~or_ok(X0)|~one(in1(X0))|one(out1(X0)))),
% 0.03/0.94 inference(cnf_transformation,[status(thm)],[f14])).
% 0.03/0.94 fof(f73,plain,(
% 0.03/0.94 ![X0]: (~logic_or(X0)|or_ok(X0)|abnormal(X0))),
% 0.03/0.94 inference(cnf_transformation,[status(thm)],[f21])).
% 0.03/0.94 fof(f74,plain,(
% 0.03/0.94 ![X0]: (~not_ok(X0)|~zero(in1(X0))|one(out1(X0)))),
% 0.03/0.94 inference(cnf_transformation,[status(thm)],[f22])).
% 0.03/0.94 fof(f79,plain,(
% 0.03/0.94 ![X0]: (~logic_not(X0)|not_ok(X0)|abnormal(X0))),
% 0.03/0.94 inference(cnf_transformation,[status(thm)],[f27])).
% 0.03/0.94 fof(f80,plain,(
% 0.03/0.94 ![X0]: (~halfadder(X0)|logic_and(and1(X0)))),
% 0.03/0.94 inference(cnf_transformation,[status(thm)],[f28])).
% 0.03/0.94 fof(f82,plain,(
% 0.03/0.94 ![X0]: (~halfadder(X0)|logic_not(not1(X0)))),
% 0.03/0.94 inference(cnf_transformation,[status(thm)],[f30])).
% 0.03/0.94 fof(f83,plain,(
% 0.03/0.94 ![X0]: (~halfadder(X0)|logic_or(or1(X0)))),
% 0.03/0.94 inference(cnf_transformation,[status(thm)],[f31])).
% 0.03/0.94 fof(f84,plain,(
% 0.03/0.94 ![X0]: (~halfadder(X0)|connection(in1(X0),in1(or1(X0))))),
% 0.03/0.94 inference(cnf_transformation,[status(thm)],[f32])).
% 0.03/0.94 fof(f88,plain,(
% 0.03/0.94 ![X0]: (~halfadder(X0)|connection(outs(X0),out1(and1(X0))))),
% 0.03/0.94 inference(cnf_transformation,[status(thm)],[f36])).
% 0.03/0.94 fof(f89,plain,(
% 0.03/0.94 ![X0]: (~halfadder(X0)|connection(outc(X0),out1(and2(X0))))),
% 0.03/0.94 inference(cnf_transformation,[status(thm)],[f37])).
% 0.03/0.94 fof(f90,plain,(
% 0.03/0.94 ![X0]: (~halfadder(X0)|connection(out1(or1(X0)),in1(and1(X0))))),
% 0.03/0.94 inference(cnf_transformation,[status(thm)],[f38])).
% 0.03/0.94 fof(f91,plain,(
% 0.03/0.94 ![X0]: (~halfadder(X0)|connection(out1(and2(X0)),in1(not1(X0))))),
% 0.03/0.94 inference(cnf_transformation,[status(thm)],[f39])).
% 0.03/0.94 fof(f92,plain,(
% 0.03/0.94 ![X0]: (~halfadder(X0)|connection(out1(not1(X0)),in2(and1(X0))))),
% 0.03/0.94 inference(cnf_transformation,[status(thm)],[f40])).
% 0.03/0.94 fof(f93,plain,(
% 0.03/0.94 halfadder(h)),
% 0.03/0.94 inference(cnf_transformation,[status(thm)],[f41])).
% 0.03/0.94 fof(f94,plain,(
% 0.03/0.94 one(in1(h))),
% 0.03/0.94 inference(cnf_transformation,[status(thm)],[f42])).
% 0.03/0.94 fof(f96,plain,(
% 0.03/0.94 zero(outs(h))),
% 0.03/0.94 inference(cnf_transformation,[status(thm)],[f44])).
% 0.03/0.94 fof(f97,plain,(
% 0.03/0.94 zero(outc(h))),
% 0.03/0.94 inference(cnf_transformation,[status(thm)],[f45])).
% 0.03/0.94 fof(f98,plain,(
% 0.03/0.94 ~abnormal(and1(h))),
% 0.03/0.94 inference(cnf_transformation,[status(thm)],[f46])).
% 0.03/0.94 fof(f99,plain,(
% 0.03/0.94 ~abnormal(not1(h))),
% 0.03/0.94 inference(cnf_transformation,[status(thm)],[f47])).
% 0.03/0.94 fof(f100,plain,(
% 0.03/0.94 ~abnormal(or1(h))),
% 0.03/0.94 inference(cnf_transformation,[status(thm)],[f48])).
% 0.03/0.94 fof(f103,plain,(
% 0.03/0.94 ![X0]: (~connection(outs(h),X0)|zero(X0))),
% 0.03/0.94 inference(resolution,[status(thm)],[f96,f50])).
% 0.03/0.94 fof(f104,plain,(
% 0.03/0.94 ![X0]: (~connection(outc(h),X0)|zero(X0))),
% 0.03/0.94 inference(resolution,[status(thm)],[f97,f50])).
% 0.03/0.94 fof(f105,plain,(
% 0.03/0.94 ![X0]: (~connection(in1(h),X0)|one(X0))),
% 0.03/0.94 inference(resolution,[status(thm)],[f52,f94])).
% 0.03/0.94 fof(f114,definition,(
% 0.03/0.94 sQ1_spl <=> (halfadder(h))),
% 0.03/0.94 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.03/0.94 fof(f116,plain,(
% 0.03/0.94 ~halfadder(h)|sQ1_spl),
% 0.03/0.94 inference(component_clause,[status(thm)],[f114])).
% 0.03/0.94 fof(f120,plain,(
% 0.03/0.94 one(in1(or1(h)))|~halfadder(h)),
% 0.03/0.94 inference(resolution,[status(thm)],[f105,f84])).
% 0.03/0.94 fof(f121,definition,(
% 0.03/0.94 sQ2_spl <=> (one(in1(or1(h))))),
% 0.03/0.94 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.03/0.94 fof(f124,plain,(
% 0.03/0.94 sQ2_spl|~sQ1_spl),
% 0.03/0.94 inference(split_clause,[status(thm)],[f120,f121,f114])).
% 0.03/0.94 fof(f125,plain,(
% 0.03/0.94 $false|sQ1_spl),
% 0.03/0.94 inference(forward_subsumption_resolution,[status(thm)],[f116,f93])).
% 0.03/0.94 fof(f126,plain,(
% 0.03/0.94 sQ1_spl),
% 0.03/0.94 inference(contradiction_clause,[status(thm)],[f125])).
% 0.03/0.94 fof(f146,plain,(
% 0.03/0.94 ![X0]: (and_ok(and1(X0))|abnormal(and1(X0))|~halfadder(X0))),
% 0.03/0.94 inference(resolution,[status(thm)],[f65,f80])).
% 0.03/0.94 fof(f147,plain,(
% 0.03/0.94 ![X0]: (or_ok(or1(X0))|abnormal(or1(X0))|~halfadder(X0))),
% 0.03/0.94 inference(resolution,[status(thm)],[f73,f83])).
% 0.03/0.94 fof(f148,plain,(
% 0.03/0.94 ![X0]: (not_ok(not1(X0))|abnormal(not1(X0))|~halfadder(X0))),
% 0.03/0.94 inference(resolution,[status(thm)],[f79,f82])).
% 0.03/0.94 fof(f168,plain,(
% 0.03/0.94 ~halfadder(h)|zero(out1(and1(h)))),
% 0.03/0.94 inference(resolution,[status(thm)],[f88,f103])).
% 0.03/0.94 fof(f169,definition,(
% 0.03/0.94 sQ8_spl <=> (zero(out1(and1(h))))),
% 0.03/0.94 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.03/0.94 fof(f170,plain,(
% 0.03/0.94 zero(out1(and1(h)))|~sQ8_spl),
% 0.03/0.94 inference(component_clause,[status(thm)],[f169])).
% 0.03/0.94 fof(f172,plain,(
% 0.03/0.94 ~sQ1_spl|sQ8_spl),
% 0.03/0.94 inference(split_clause,[status(thm)],[f168,f114,f169])).
% 0.03/0.94 fof(f194,plain,(
% 0.03/0.94 ~and_ok(and1(h))|zero(in1(and1(h)))|zero(in2(and1(h)))|~sQ8_spl),
% 0.03/0.94 inference(resolution,[status(thm)],[f170,f61])).
% 0.03/0.94 fof(f202,definition,(
% 0.03/0.94 sQ13_spl <=> (one(in1(and1(h))))),
% 0.03/0.94 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.03/0.94 fof(f203,plain,(
% 0.03/0.94 one(in1(and1(h)))|~sQ13_spl),
% 0.03/0.94 inference(component_clause,[status(thm)],[f202])).
% 0.03/0.94 fof(f206,definition,(
% 0.03/0.94 sQ14_spl <=> (and_ok(and1(h)))),
% 0.03/0.94 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.03/0.94 fof(f209,definition,(
% 0.03/0.94 sQ15_spl <=> (zero(in1(and1(h))))),
% 0.03/0.94 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.03/0.94 fof(f210,plain,(
% 0.03/0.94 zero(in1(and1(h)))|~sQ15_spl),
% 0.03/0.94 inference(component_clause,[status(thm)],[f209])).
% 0.03/0.94 fof(f212,definition,(
% 0.03/0.94 sQ16_spl <=> (zero(in2(and1(h))))),
% 0.03/0.94 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.03/0.94 fof(f213,plain,(
% 0.03/0.94 zero(in2(and1(h)))|~sQ16_spl),
% 0.03/0.94 inference(component_clause,[status(thm)],[f212])).
% 0.03/0.94 fof(f215,plain,(
% 0.03/0.94 ~sQ14_spl|sQ15_spl|sQ16_spl|~sQ8_spl),
% 0.03/0.94 inference(split_clause,[status(thm)],[f194,f206,f209,f212,f169])).
% 0.03/0.94 fof(f221,plain,(
% 0.03/0.94 ~halfadder(h)|zero(out1(and2(h)))),
% 0.03/0.94 inference(resolution,[status(thm)],[f89,f104])).
% 0.03/0.94 fof(f222,definition,(
% 0.03/0.94 sQ18_spl <=> (zero(out1(and2(h))))),
% 0.03/0.94 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.03/0.94 fof(f223,plain,(
% 0.03/0.94 zero(out1(and2(h)))|~sQ18_spl),
% 0.03/0.94 inference(component_clause,[status(thm)],[f222])).
% 0.03/0.94 fof(f225,plain,(
% 0.03/0.94 ~sQ1_spl|sQ18_spl),
% 0.03/0.94 inference(split_clause,[status(thm)],[f221,f114,f222])).
% 0.03/0.94 fof(f243,plain,(
% 0.03/0.94 ![X0]: (~connection(out1(and2(h)),X0)|zero(X0)|~sQ18_spl)),
% 0.03/0.94 inference(resolution,[status(thm)],[f223,f50])).
% 0.03/0.94 fof(f278,plain,(
% 0.03/0.94 and_ok(and1(h))|abnormal(and1(h))),
% 0.03/0.94 inference(resolution,[status(thm)],[f146,f93])).
% 0.03/0.94 fof(f279,definition,(
% 0.03/0.94 sQ28_spl <=> (abnormal(and1(h)))),
% 0.03/0.94 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 0.03/0.94 fof(f280,plain,(
% 0.03/0.94 abnormal(and1(h))|~sQ28_spl),
% 0.03/0.94 inference(component_clause,[status(thm)],[f279])).
% 0.03/0.94 fof(f282,plain,(
% 0.03/0.94 sQ14_spl|sQ28_spl),
% 0.03/0.94 inference(split_clause,[status(thm)],[f278,f206,f279])).
% 0.03/0.94 fof(f283,plain,(
% 0.03/0.94 or_ok(or1(h))|abnormal(or1(h))),
% 0.03/0.94 inference(resolution,[status(thm)],[f147,f93])).
% 0.03/0.94 fof(f284,definition,(
% 0.03/0.94 sQ29_spl <=> (or_ok(or1(h)))),
% 0.03/0.94 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 0.03/0.94 fof(f285,plain,(
% 0.03/0.94 or_ok(or1(h))|~sQ29_spl),
% 0.03/0.94 inference(component_clause,[status(thm)],[f284])).
% 0.03/0.94 fof(f287,definition,(
% 0.03/0.94 sQ30_spl <=> (abnormal(or1(h)))),
% 0.03/0.94 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 0.03/0.94 fof(f288,plain,(
% 0.03/0.94 abnormal(or1(h))|~sQ30_spl),
% 0.03/0.94 inference(component_clause,[status(thm)],[f287])).
% 0.03/0.94 fof(f290,plain,(
% 0.03/0.94 sQ29_spl|sQ30_spl),
% 0.03/0.94 inference(split_clause,[status(thm)],[f283,f284,f287])).
% 0.03/0.94 fof(f291,plain,(
% 0.03/0.94 not_ok(not1(h))|abnormal(not1(h))),
% 0.03/0.94 inference(resolution,[status(thm)],[f148,f93])).
% 0.03/0.94 fof(f292,definition,(
% 0.03/0.94 sQ31_spl <=> (not_ok(not1(h)))),
% 0.03/0.94 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.03/0.94 fof(f295,definition,(
% 0.03/0.94 sQ32_spl <=> (abnormal(not1(h)))),
% 0.03/0.94 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.03/0.94 fof(f296,plain,(
% 0.03/0.94 abnormal(not1(h))|~sQ32_spl),
% 0.03/0.94 inference(component_clause,[status(thm)],[f295])).
% 0.03/0.94 fof(f298,plain,(
% 0.03/0.94 sQ31_spl|sQ32_spl),
% 0.03/0.94 inference(split_clause,[status(thm)],[f291,f292,f295])).
% 0.03/0.94 fof(f299,plain,(
% 0.03/0.94 ~one(in1(or1(h)))|one(out1(or1(h)))|~sQ29_spl),
% 0.03/0.94 inference(resolution,[status(thm)],[f285,f66])).
% 0.03/0.94 fof(f301,definition,(
% 0.03/0.94 sQ33_spl <=> (one(out1(or1(h))))),
% 0.03/0.94 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 0.03/0.95 fof(f302,plain,(
% 0.03/0.95 one(out1(or1(h)))|~sQ33_spl),
% 0.03/0.95 inference(component_clause,[status(thm)],[f301])).
% 0.03/0.95 fof(f304,plain,(
% 0.03/0.95 ~sQ2_spl|sQ33_spl|~sQ29_spl),
% 0.03/0.95 inference(split_clause,[status(thm)],[f299,f121,f301,f284])).
% 0.03/0.95 fof(f305,plain,(
% 0.03/0.95 $false|~sQ30_spl),
% 0.03/0.95 inference(forward_subsumption_resolution,[status(thm)],[f288,f100])).
% 0.03/0.95 fof(f306,plain,(
% 0.03/0.95 ~sQ30_spl),
% 0.03/0.95 inference(contradiction_clause,[status(thm)],[f305])).
% 0.03/0.95 fof(f316,plain,(
% 0.03/0.95 $false|~sQ32_spl),
% 0.03/0.95 inference(forward_subsumption_resolution,[status(thm)],[f296,f99])).
% 0.03/0.95 fof(f317,plain,(
% 0.03/0.95 ~sQ32_spl),
% 0.03/0.95 inference(contradiction_clause,[status(thm)],[f316])).
% 0.03/0.95 fof(f329,plain,(
% 0.03/0.95 ![X0]: (~connection(out1(or1(h)),X0)|one(X0)|~sQ33_spl)),
% 0.03/0.95 inference(resolution,[status(thm)],[f302,f52])).
% 0.03/0.95 fof(f347,plain,(
% 0.03/0.95 one(in1(and1(h)))|~halfadder(h)|~sQ33_spl),
% 0.03/0.95 inference(resolution,[status(thm)],[f329,f90])).
% 0.03/0.95 fof(f348,plain,(
% 0.03/0.95 sQ13_spl|~sQ1_spl|~sQ33_spl),
% 0.03/0.95 inference(split_clause,[status(thm)],[f347,f202,f114,f301])).
% 0.03/0.95 fof(f349,plain,(
% 0.03/0.95 zero(in1(not1(h)))|~halfadder(h)|~sQ18_spl),
% 0.03/0.95 inference(resolution,[status(thm)],[f243,f91])).
% 0.03/0.95 fof(f350,definition,(
% 0.03/0.95 sQ40_spl <=> (zero(in1(not1(h))))),
% 0.03/0.95 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 0.03/0.95 fof(f351,plain,(
% 0.03/0.95 zero(in1(not1(h)))|~sQ40_spl),
% 0.03/0.95 inference(component_clause,[status(thm)],[f350])).
% 0.03/0.95 fof(f353,plain,(
% 0.03/0.95 sQ40_spl|~sQ1_spl|~sQ18_spl),
% 0.03/0.95 inference(split_clause,[status(thm)],[f349,f350,f114,f222])).
% 0.03/0.95 fof(f366,plain,(
% 0.03/0.95 ~zero(in1(and1(h)))|~sQ13_spl),
% 0.03/0.95 inference(resolution,[status(thm)],[f203,f57])).
% 0.03/0.95 fof(f367,plain,(
% 0.03/0.95 $false|~sQ15_spl|~sQ13_spl),
% 0.03/0.95 inference(forward_subsumption_resolution,[status(thm)],[f366,f210])).
% 0.03/0.95 fof(f368,plain,(
% 0.03/0.95 ~sQ15_spl|~sQ13_spl),
% 0.03/0.95 inference(contradiction_clause,[status(thm)],[f367])).
% 0.03/0.95 fof(f369,plain,(
% 0.03/0.95 $false|~sQ28_spl),
% 0.03/0.95 inference(forward_subsumption_resolution,[status(thm)],[f280,f98])).
% 0.03/0.95 fof(f370,plain,(
% 0.03/0.95 ~sQ28_spl),
% 0.03/0.95 inference(contradiction_clause,[status(thm)],[f369])).
% 0.03/0.95 fof(f373,plain,(
% 0.03/0.95 ~not_ok(not1(h))|one(out1(not1(h)))|~sQ40_spl),
% 0.03/0.95 inference(resolution,[status(thm)],[f351,f74])).
% 0.03/0.95 fof(f378,definition,(
% 0.03/0.95 sQ41_spl <=> (one(out1(not1(h))))),
% 0.03/0.95 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 0.03/0.95 fof(f379,plain,(
% 0.03/0.95 one(out1(not1(h)))|~sQ41_spl),
% 0.03/0.95 inference(component_clause,[status(thm)],[f378])).
% 0.03/0.95 fof(f381,plain,(
% 0.03/0.95 ~sQ31_spl|sQ41_spl|~sQ40_spl),
% 0.03/0.95 inference(split_clause,[status(thm)],[f373,f292,f378,f350])).
% 0.03/0.95 fof(f415,plain,(
% 0.03/0.95 ![X0]: (~connection(out1(not1(h)),X0)|one(X0)|~sQ41_spl)),
% 0.03/0.95 inference(resolution,[status(thm)],[f379,f52])).
% 0.03/0.95 fof(f473,plain,(
% 0.03/0.95 one(in2(and1(h)))|~halfadder(h)|~sQ41_spl),
% 0.03/0.95 inference(resolution,[status(thm)],[f415,f92])).
% 0.03/0.95 fof(f474,definition,(
% 0.03/0.95 sQ55_spl <=> (one(in2(and1(h))))),
% 0.03/0.95 introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition])).
% 0.03/0.95 fof(f475,plain,(
% 0.03/0.95 one(in2(and1(h)))|~sQ55_spl),
% 0.03/0.95 inference(component_clause,[status(thm)],[f474])).
% 0.03/0.95 fof(f477,plain,(
% 0.03/0.95 sQ55_spl|~sQ1_spl|~sQ41_spl),
% 0.03/0.95 inference(split_clause,[status(thm)],[f473,f474,f114,f378])).
% 0.03/0.95 fof(f482,plain,(
% 0.03/0.95 ~zero(in2(and1(h)))|~sQ55_spl),
% 0.03/0.95 inference(resolution,[status(thm)],[f475,f57])).
% 0.03/0.95 fof(f485,plain,(
% 0.03/0.95 $false|~sQ16_spl|~sQ55_spl),
% 0.03/0.95 inference(forward_subsumption_resolution,[status(thm)],[f482,f213])).
% 0.03/0.95 fof(f486,plain,(
% 0.03/0.95 ~sQ16_spl|~sQ55_spl),
% 0.03/0.95 inference(contradiction_clause,[status(thm)],[f485])).
% 0.03/0.95 fof(f487,plain,(
% 0.03/0.95 $false),
% 0.03/0.95 inference(sat_refutation,[status(thm)],[f124,f126,f172,f215,f225,f282,f290,f298,f304,f306,f317,f348,f353,f368,f370,f381,f477,f486])).
% 0.03/0.95 % SZS output end CNFRefutation for theBenchmark.p
% 0.03/0.96 % Elapsed time: 0.045400 seconds
% 0.03/0.96 % CPU time: 0.117502 seconds
% 0.03/0.96 % Total memory used: 18.379 MB
% 0.03/0.96 % Net memory used: 18.328 MB
%------------------------------------------------------------------------------