%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : HWV008-2.001 : TPTP v9.3.1. Bugfixed v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n001.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:39 PM UTC 2026
% Result : Unsatisfiable 0.13s 0.40s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HWV008-2.001 : TPTP v9.3.1. Bugfixed v2.7.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.35 % Computer : n001.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Sun Sep 20 20:53:28 UTC 2026
% 0.10/0.35 % CPUTime :
% 0.10/0.36 % Drodi V4.1.1
% 0.13/0.40 % Refutation found
% 0.13/0.40 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.13/0.40 % SZS output start CNFRefutation for theBenchmark
% 0.13/0.40 fof(f1,axiom,(
% 0.13/0.40 (![P1,P2]: (( ~ connection(P1,P2)| ~ zero(P1)| zero(P2) ) ))),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f3,axiom,(
% 0.13/0.40 (![P1,P2]: (( ~ connection(P1,P2)| ~ zero(P2)| zero(P1) ) ))),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f5,axiom,(
% 0.13/0.40 (![P]: (( ~ zero(P)| ~ one(P) ) ))),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f6,axiom,(
% 0.13/0.40 (![K]: (( ~ and_ok(K)| ~ zero(in1(K))| zero(out1(K)) ) ))),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f13,axiom,(
% 0.13/0.40 (![K]: (( ~ logic_and(K)| and_ok(K)| abnormal(K) ) ))),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f16,axiom,(
% 0.13/0.40 (![K]: (( ~ or_ok(K)| ~ zero(in1(K))| ~ zero(in2(K))| zero(out1(K)) ) ))),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f21,axiom,(
% 0.13/0.40 (![K]: (( ~ logic_or(K)| or_ok(K)| abnormal(K) ) ))),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f29,axiom,(
% 0.13/0.40 (![X]: (( ~ halfadder(X)| logic_and(and2(X)) ) ))),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f34,axiom,(
% 0.13/0.40 (![X]: (( ~ halfadder(X)| connection(in1(X),in1(and2(X))) ) ))),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f37,axiom,(
% 0.13/0.40 (![X]: (( ~ halfadder(X)| connection(outc(X),out1(and2(X))) ) ))),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f41,axiom,(
% 0.13/0.40 (![X]: (( ~ fulladder(X)| halfadder(h1(X)) ) ))),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f42,axiom,(
% 0.13/0.40 (![X]: (( ~ fulladder(X)| halfadder(h2(X)) ) ))),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f43,axiom,(
% 0.13/0.40 (![X]: (( ~ fulladder(X)| logic_or(or1(X)) ) ))),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f45,axiom,(
% 0.13/0.40 (![X]: (( ~ fulladder(X)| connection(outc(h1(X)),in2(or1(X))) ) ))),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f46,axiom,(
% 0.13/0.40 (![X]: (( ~ fulladder(X)| connection(outc(h2(X)),in1(or1(X))) ) ))),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f47,axiom,(
% 0.13/0.40 (![X]: (( ~ fulladder(X)| connection(in1(X),in1(h2(X))) ) ))),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f48,axiom,(
% 0.13/0.40 (![X]: (( ~ fulladder(X)| connection(in2(X),in1(h1(X))) ) ))),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f51,axiom,(
% 0.13/0.40 (![X]: (( ~ fulladder(X)| connection(outc(X),out1(or1(X))) ) ))),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f52,axiom,(
% 0.13/0.40 (![X]: (( ~ nbit_adder1(X)| fulladder(f1(X)) ) ))),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f54,axiom,(
% 0.13/0.40 (![X]: (( ~ nbit_adder1(X)| connection(outc(X),outc(f1(X))) ) ))),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f55,axiom,(
% 0.13/0.40 (![X]: (( ~ nbit_adder1(X)| connection(ina1(X),in1(f1(X))) ) ))),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f56,axiom,(
% 0.13/0.40 (![X]: (( ~ nbit_adder1(X)| connection(inb1(X),in2(f1(X))) ) ))),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f58,hypothesis,(
% 0.13/0.40 nbit_adder1(a) ),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f59,hypothesis,(
% 0.13/0.40 zero(ina1(a)) ),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f60,hypothesis,(
% 0.13/0.40 zero(inb1(a)) ),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f63,hypothesis,(
% 0.13/0.40 one(outc(a)) ),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f64,negated_conjecture,(
% 0.13/0.40 ~ abnormal(or1(f1(a))) ),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f65,negated_conjecture,(
% 0.13/0.40 ~ abnormal(and2(h1(f1(a)))) ),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f66,negated_conjecture,(
% 0.13/0.40 ~ abnormal(and2(h2(f1(a)))) ),
% 0.13/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.40 fof(f67,plain,(
% 0.13/0.40 ![P2]: ((![P1]: (~connection(P1,P2)|~zero(P1)))|zero(P2))),
% 0.13/0.40 inference(miniscoping,[status(thm)],[f1])).
% 0.13/0.40 fof(f68,plain,(
% 0.13/0.40 ![X0,X1]: (~connection(X0,X1)|~zero(X0)|zero(X1))),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f67])).
% 0.13/0.40 fof(f71,plain,(
% 0.13/0.40 ![P1]: ((![P2]: (~connection(P1,P2)|~zero(P2)))|zero(P1))),
% 0.13/0.40 inference(miniscoping,[status(thm)],[f3])).
% 0.13/0.40 fof(f72,plain,(
% 0.13/0.40 ![X0,X1]: (~connection(X0,X1)|~zero(X1)|zero(X0))),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f71])).
% 0.13/0.40 fof(f75,plain,(
% 0.13/0.40 ![X0]: (~zero(X0)|~one(X0))),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f5])).
% 0.13/0.40 fof(f76,plain,(
% 0.13/0.40 ![X0]: (~and_ok(X0)|~zero(in1(X0))|zero(out1(X0)))),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f6])).
% 0.13/0.40 fof(f83,plain,(
% 0.13/0.40 ![X0]: (~logic_and(X0)|and_ok(X0)|abnormal(X0))),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f13])).
% 0.13/0.40 fof(f86,plain,(
% 0.13/0.40 ![X0]: (~or_ok(X0)|~zero(in1(X0))|~zero(in2(X0))|zero(out1(X0)))),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f16])).
% 0.13/0.40 fof(f91,plain,(
% 0.13/0.40 ![X0]: (~logic_or(X0)|or_ok(X0)|abnormal(X0))),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f21])).
% 0.13/0.40 fof(f99,plain,(
% 0.13/0.40 ![X0]: (~halfadder(X0)|logic_and(and2(X0)))),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f29])).
% 0.13/0.40 fof(f104,plain,(
% 0.13/0.40 ![X0]: (~halfadder(X0)|connection(in1(X0),in1(and2(X0))))),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f34])).
% 0.13/0.40 fof(f107,plain,(
% 0.13/0.40 ![X0]: (~halfadder(X0)|connection(outc(X0),out1(and2(X0))))),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f37])).
% 0.13/0.40 fof(f111,plain,(
% 0.13/0.40 ![X0]: (~fulladder(X0)|halfadder(h1(X0)))),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f41])).
% 0.13/0.40 fof(f112,plain,(
% 0.13/0.40 ![X0]: (~fulladder(X0)|halfadder(h2(X0)))),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f42])).
% 0.13/0.40 fof(f113,plain,(
% 0.13/0.40 ![X0]: (~fulladder(X0)|logic_or(or1(X0)))),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f43])).
% 0.13/0.40 fof(f115,plain,(
% 0.13/0.40 ![X0]: (~fulladder(X0)|connection(outc(h1(X0)),in2(or1(X0))))),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f45])).
% 0.13/0.40 fof(f116,plain,(
% 0.13/0.40 ![X0]: (~fulladder(X0)|connection(outc(h2(X0)),in1(or1(X0))))),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f46])).
% 0.13/0.40 fof(f117,plain,(
% 0.13/0.40 ![X0]: (~fulladder(X0)|connection(in1(X0),in1(h2(X0))))),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f47])).
% 0.13/0.40 fof(f118,plain,(
% 0.13/0.40 ![X0]: (~fulladder(X0)|connection(in2(X0),in1(h1(X0))))),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f48])).
% 0.13/0.40 fof(f121,plain,(
% 0.13/0.40 ![X0]: (~fulladder(X0)|connection(outc(X0),out1(or1(X0))))),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f51])).
% 0.13/0.40 fof(f122,plain,(
% 0.13/0.40 ![X0]: (~nbit_adder1(X0)|fulladder(f1(X0)))),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f52])).
% 0.13/0.40 fof(f124,plain,(
% 0.13/0.40 ![X0]: (~nbit_adder1(X0)|connection(outc(X0),outc(f1(X0))))),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f54])).
% 0.13/0.40 fof(f125,plain,(
% 0.13/0.40 ![X0]: (~nbit_adder1(X0)|connection(ina1(X0),in1(f1(X0))))),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f55])).
% 0.13/0.40 fof(f126,plain,(
% 0.13/0.40 ![X0]: (~nbit_adder1(X0)|connection(inb1(X0),in2(f1(X0))))),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f56])).
% 0.13/0.40 fof(f128,plain,(
% 0.13/0.40 nbit_adder1(a)),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f58])).
% 0.13/0.40 fof(f129,plain,(
% 0.13/0.40 zero(ina1(a))),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f59])).
% 0.13/0.40 fof(f130,plain,(
% 0.13/0.40 zero(inb1(a))),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f60])).
% 0.13/0.40 fof(f133,plain,(
% 0.13/0.40 one(outc(a))),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f63])).
% 0.13/0.40 fof(f134,plain,(
% 0.13/0.40 ~abnormal(or1(f1(a)))),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f64])).
% 0.13/0.40 fof(f135,plain,(
% 0.13/0.40 ~abnormal(and2(h1(f1(a))))),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f65])).
% 0.13/0.40 fof(f136,plain,(
% 0.13/0.40 ~abnormal(and2(h2(f1(a))))),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f66])).
% 0.13/0.40 fof(f153,plain,(
% 0.13/0.40 ~zero(outc(a))),
% 0.13/0.40 inference(resolution,[status(thm)],[f133,f75])).
% 0.13/0.40 fof(f171,plain,(
% 0.13/0.40 fulladder(f1(a))),
% 0.13/0.40 inference(resolution,[status(thm)],[f122,f128])).
% 0.13/0.40 fof(f172,plain,(
% 0.13/0.40 logic_or(or1(f1(a)))),
% 0.13/0.40 inference(resolution,[status(thm)],[f171,f113])).
% 0.13/0.40 fof(f173,plain,(
% 0.13/0.40 connection(in2(f1(a)),in1(h1(f1(a))))),
% 0.13/0.40 inference(resolution,[status(thm)],[f171,f118])).
% 0.13/0.40 fof(f174,plain,(
% 0.13/0.40 connection(in1(f1(a)),in1(h2(f1(a))))),
% 0.13/0.40 inference(resolution,[status(thm)],[f171,f117])).
% 0.13/0.40 fof(f175,plain,(
% 0.13/0.40 connection(outc(h2(f1(a))),in1(or1(f1(a))))),
% 0.13/0.40 inference(resolution,[status(thm)],[f171,f116])).
% 0.13/0.40 fof(f176,plain,(
% 0.13/0.40 connection(outc(h1(f1(a))),in2(or1(f1(a))))),
% 0.13/0.40 inference(resolution,[status(thm)],[f171,f115])).
% 0.13/0.40 fof(f177,plain,(
% 0.13/0.40 halfadder(h2(f1(a)))),
% 0.13/0.40 inference(resolution,[status(thm)],[f171,f112])).
% 0.13/0.40 fof(f178,plain,(
% 0.13/0.40 halfadder(h1(f1(a)))),
% 0.13/0.40 inference(resolution,[status(thm)],[f171,f111])).
% 0.13/0.40 fof(f181,plain,(
% 0.13/0.40 logic_and(and2(h2(f1(a))))),
% 0.13/0.40 inference(resolution,[status(thm)],[f177,f99])).
% 0.13/0.40 fof(f183,plain,(
% 0.13/0.40 connection(outc(h2(f1(a))),out1(and2(h2(f1(a)))))),
% 0.13/0.40 inference(resolution,[status(thm)],[f177,f107])).
% 0.13/0.40 fof(f185,plain,(
% 0.13/0.40 connection(in1(h2(f1(a))),in1(and2(h2(f1(a)))))),
% 0.13/0.40 inference(resolution,[status(thm)],[f177,f104])).
% 0.13/0.40 fof(f190,plain,(
% 0.13/0.40 logic_and(and2(h1(f1(a))))),
% 0.13/0.40 inference(resolution,[status(thm)],[f178,f99])).
% 0.13/0.40 fof(f192,plain,(
% 0.13/0.40 connection(outc(h1(f1(a))),out1(and2(h1(f1(a)))))),
% 0.13/0.40 inference(resolution,[status(thm)],[f178,f107])).
% 0.13/0.40 fof(f194,plain,(
% 0.13/0.40 connection(in1(h1(f1(a))),in1(and2(h1(f1(a)))))),
% 0.13/0.40 inference(resolution,[status(thm)],[f178,f104])).
% 0.13/0.40 fof(f213,plain,(
% 0.13/0.40 and_ok(and2(h2(f1(a))))|abnormal(and2(h2(f1(a))))),
% 0.13/0.40 inference(resolution,[status(thm)],[f181,f83])).
% 0.13/0.40 fof(f214,definition,(
% 0.13/0.40 sQ11_spl <=> (and_ok(and2(h2(f1(a)))))),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f217,definition,(
% 0.13/0.40 sQ12_spl <=> (abnormal(and2(h2(f1(a)))))),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f218,plain,(
% 0.13/0.40 abnormal(and2(h2(f1(a))))|~sQ12_spl),
% 0.13/0.40 inference(component_clause,[status(thm)],[f217])).
% 0.13/0.40 fof(f220,plain,(
% 0.13/0.40 sQ11_spl|sQ12_spl),
% 0.13/0.40 inference(split_clause,[status(thm)],[f213,f214,f217])).
% 0.13/0.40 fof(f232,plain,(
% 0.13/0.40 ~zero(in2(f1(a)))|zero(in1(h1(f1(a))))),
% 0.13/0.40 inference(resolution,[status(thm)],[f173,f68])).
% 0.13/0.40 fof(f240,definition,(
% 0.13/0.40 sQ17_spl <=> (zero(in1(h1(f1(a)))))),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f243,definition,(
% 0.13/0.40 sQ18_spl <=> (zero(in2(f1(a))))),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f248,plain,(
% 0.13/0.40 ~sQ18_spl|sQ17_spl),
% 0.13/0.40 inference(split_clause,[status(thm)],[f232,f243,f240])).
% 0.13/0.40 fof(f252,plain,(
% 0.13/0.40 ~zero(in1(f1(a)))|zero(in1(h2(f1(a))))),
% 0.13/0.40 inference(resolution,[status(thm)],[f174,f68])).
% 0.13/0.40 fof(f260,definition,(
% 0.13/0.40 sQ21_spl <=> (zero(in1(h2(f1(a)))))),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f263,definition,(
% 0.13/0.40 sQ22_spl <=> (zero(in1(f1(a))))),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f268,plain,(
% 0.13/0.40 ~sQ22_spl|sQ21_spl),
% 0.13/0.40 inference(split_clause,[status(thm)],[f252,f263,f260])).
% 0.13/0.40 fof(f272,plain,(
% 0.13/0.40 ~zero(outc(h2(f1(a))))|zero(in1(or1(f1(a))))),
% 0.13/0.40 inference(resolution,[status(thm)],[f175,f68])).
% 0.13/0.40 fof(f280,definition,(
% 0.13/0.40 sQ25_spl <=> (zero(in1(or1(f1(a)))))),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f283,definition,(
% 0.13/0.40 sQ26_spl <=> (zero(outc(h2(f1(a)))))),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f288,plain,(
% 0.13/0.40 ~sQ26_spl|sQ25_spl),
% 0.13/0.40 inference(split_clause,[status(thm)],[f272,f283,f280])).
% 0.13/0.40 fof(f292,plain,(
% 0.13/0.40 ~zero(outc(h1(f1(a))))|zero(in2(or1(f1(a))))),
% 0.13/0.40 inference(resolution,[status(thm)],[f176,f68])).
% 0.13/0.40 fof(f300,definition,(
% 0.13/0.40 sQ29_spl <=> (zero(in2(or1(f1(a)))))),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f301,plain,(
% 0.13/0.40 zero(in2(or1(f1(a))))|~sQ29_spl),
% 0.13/0.40 inference(component_clause,[status(thm)],[f300])).
% 0.13/0.40 fof(f303,definition,(
% 0.13/0.40 sQ30_spl <=> (zero(outc(h1(f1(a)))))),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f308,plain,(
% 0.13/0.40 ~sQ30_spl|sQ29_spl),
% 0.13/0.40 inference(split_clause,[status(thm)],[f292,f303,f300])).
% 0.13/0.40 fof(f310,plain,(
% 0.13/0.40 ~zero(out1(and2(h2(f1(a)))))|zero(outc(h2(f1(a))))),
% 0.13/0.40 inference(resolution,[status(thm)],[f183,f72])).
% 0.13/0.40 fof(f317,definition,(
% 0.13/0.40 sQ32_spl <=> (zero(out1(and2(h2(f1(a))))))),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f320,plain,(
% 0.13/0.40 ~sQ32_spl|sQ26_spl),
% 0.13/0.40 inference(split_clause,[status(thm)],[f310,f317,f283])).
% 0.13/0.40 fof(f346,plain,(
% 0.13/0.40 ~zero(in1(h2(f1(a))))|zero(in1(and2(h2(f1(a)))))),
% 0.13/0.40 inference(resolution,[status(thm)],[f185,f68])).
% 0.13/0.40 fof(f351,definition,(
% 0.13/0.40 sQ38_spl <=> (zero(in1(and2(h2(f1(a))))))),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f352,plain,(
% 0.13/0.40 zero(in1(and2(h2(f1(a)))))|~sQ38_spl),
% 0.13/0.40 inference(component_clause,[status(thm)],[f351])).
% 0.13/0.40 fof(f356,plain,(
% 0.13/0.40 ~sQ21_spl|sQ38_spl),
% 0.13/0.40 inference(split_clause,[status(thm)],[f346,f260,f351])).
% 0.13/0.40 fof(f401,plain,(
% 0.13/0.40 and_ok(and2(h1(f1(a))))|abnormal(and2(h1(f1(a))))),
% 0.13/0.40 inference(resolution,[status(thm)],[f190,f83])).
% 0.13/0.40 fof(f402,definition,(
% 0.13/0.40 sQ47_spl <=> (and_ok(and2(h1(f1(a)))))),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f405,definition,(
% 0.13/0.40 sQ48_spl <=> (abnormal(and2(h1(f1(a)))))),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f406,plain,(
% 0.13/0.40 abnormal(and2(h1(f1(a))))|~sQ48_spl),
% 0.13/0.40 inference(component_clause,[status(thm)],[f405])).
% 0.13/0.40 fof(f408,plain,(
% 0.13/0.40 sQ47_spl|sQ48_spl),
% 0.13/0.40 inference(split_clause,[status(thm)],[f401,f402,f405])).
% 0.13/0.40 fof(f418,plain,(
% 0.13/0.40 ~zero(out1(and2(h1(f1(a)))))|zero(outc(h1(f1(a))))),
% 0.13/0.40 inference(resolution,[status(thm)],[f192,f72])).
% 0.13/0.40 fof(f425,definition,(
% 0.13/0.40 sQ52_spl <=> (zero(out1(and2(h1(f1(a))))))),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f428,plain,(
% 0.13/0.40 ~sQ52_spl|sQ30_spl),
% 0.13/0.40 inference(split_clause,[status(thm)],[f418,f425,f303])).
% 0.13/0.40 fof(f454,plain,(
% 0.13/0.40 ~zero(in1(h1(f1(a))))|zero(in1(and2(h1(f1(a)))))),
% 0.13/0.40 inference(resolution,[status(thm)],[f194,f68])).
% 0.13/0.40 fof(f459,definition,(
% 0.13/0.40 sQ58_spl <=> (zero(in1(and2(h1(f1(a))))))),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f460,plain,(
% 0.13/0.40 zero(in1(and2(h1(f1(a)))))|~sQ58_spl),
% 0.13/0.40 inference(component_clause,[status(thm)],[f459])).
% 0.13/0.40 fof(f464,plain,(
% 0.13/0.40 ~sQ17_spl|sQ58_spl),
% 0.13/0.40 inference(split_clause,[status(thm)],[f454,f240,f459])).
% 0.13/0.40 fof(f495,plain,(
% 0.13/0.40 or_ok(or1(f1(a)))|abnormal(or1(f1(a)))),
% 0.13/0.40 inference(resolution,[status(thm)],[f172,f91])).
% 0.13/0.40 fof(f496,definition,(
% 0.13/0.40 sQ63_spl <=> (or_ok(or1(f1(a))))),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f499,definition,(
% 0.13/0.40 sQ64_spl <=> (abnormal(or1(f1(a))))),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f500,plain,(
% 0.13/0.40 abnormal(or1(f1(a)))|~sQ64_spl),
% 0.13/0.40 inference(component_clause,[status(thm)],[f499])).
% 0.13/0.40 fof(f502,plain,(
% 0.13/0.40 sQ63_spl|sQ64_spl),
% 0.13/0.40 inference(split_clause,[status(thm)],[f495,f496,f499])).
% 0.13/0.40 fof(f665,plain,(
% 0.13/0.40 connection(outc(f1(a)),out1(or1(f1(a))))),
% 0.13/0.40 inference(resolution,[status(thm)],[f121,f171])).
% 0.13/0.40 fof(f686,plain,(
% 0.13/0.40 connection(outc(a),outc(f1(a)))),
% 0.13/0.40 inference(resolution,[status(thm)],[f124,f128])).
% 0.13/0.40 fof(f687,plain,(
% 0.13/0.40 connection(ina1(a),in1(f1(a)))),
% 0.13/0.40 inference(resolution,[status(thm)],[f125,f128])).
% 0.13/0.40 fof(f688,plain,(
% 0.13/0.40 connection(inb1(a),in2(f1(a)))),
% 0.13/0.40 inference(resolution,[status(thm)],[f126,f128])).
% 0.13/0.40 fof(f691,plain,(
% 0.13/0.40 ~zero(outc(f1(a)))|zero(outc(a))),
% 0.13/0.40 inference(resolution,[status(thm)],[f686,f72])).
% 0.13/0.40 fof(f701,definition,(
% 0.13/0.40 sQ98_spl <=> (zero(outc(f1(a))))),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ98_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f704,definition,(
% 0.13/0.40 sQ99_spl <=> (zero(outc(a)))),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f705,plain,(
% 0.13/0.40 zero(outc(a))|~sQ99_spl),
% 0.13/0.40 inference(component_clause,[status(thm)],[f704])).
% 0.13/0.40 fof(f707,plain,(
% 0.13/0.40 ~sQ98_spl|sQ99_spl),
% 0.13/0.40 inference(split_clause,[status(thm)],[f691,f701,f704])).
% 0.13/0.40 fof(f715,plain,(
% 0.13/0.40 ~zero(ina1(a))|zero(in1(f1(a)))),
% 0.13/0.40 inference(resolution,[status(thm)],[f687,f68])).
% 0.13/0.40 fof(f720,definition,(
% 0.13/0.40 sQ101_spl <=> (zero(ina1(a)))),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f722,plain,(
% 0.13/0.40 ~zero(ina1(a))|sQ101_spl),
% 0.13/0.40 inference(component_clause,[status(thm)],[f720])).
% 0.13/0.40 fof(f725,plain,(
% 0.13/0.40 ~sQ101_spl|sQ22_spl),
% 0.13/0.40 inference(split_clause,[status(thm)],[f715,f720,f263])).
% 0.13/0.40 fof(f726,plain,(
% 0.13/0.40 $false|sQ101_spl),
% 0.13/0.40 inference(forward_subsumption_resolution,[status(thm)],[f722,f129])).
% 0.13/0.40 fof(f727,plain,(
% 0.13/0.40 sQ101_spl),
% 0.13/0.40 inference(contradiction_clause,[status(thm)],[f726])).
% 0.13/0.40 fof(f731,plain,(
% 0.13/0.40 ~zero(inb1(a))|zero(in2(f1(a)))),
% 0.13/0.40 inference(resolution,[status(thm)],[f688,f68])).
% 0.13/0.40 fof(f736,definition,(
% 0.13/0.40 sQ103_spl <=> (zero(inb1(a)))),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f738,plain,(
% 0.13/0.40 ~zero(inb1(a))|sQ103_spl),
% 0.13/0.40 inference(component_clause,[status(thm)],[f736])).
% 0.13/0.40 fof(f741,plain,(
% 0.13/0.40 ~sQ103_spl|sQ18_spl),
% 0.13/0.40 inference(split_clause,[status(thm)],[f731,f736,f243])).
% 0.13/0.40 fof(f742,plain,(
% 0.13/0.40 $false|sQ103_spl),
% 0.13/0.40 inference(forward_subsumption_resolution,[status(thm)],[f738,f130])).
% 0.13/0.40 fof(f743,plain,(
% 0.13/0.40 sQ103_spl),
% 0.13/0.40 inference(contradiction_clause,[status(thm)],[f742])).
% 0.13/0.40 fof(f846,plain,(
% 0.13/0.40 ~and_ok(and2(h2(f1(a))))|zero(out1(and2(h2(f1(a)))))|~sQ38_spl),
% 0.13/0.40 inference(resolution,[status(thm)],[f352,f76])).
% 0.13/0.40 fof(f851,plain,(
% 0.13/0.40 ~sQ11_spl|sQ32_spl|~sQ38_spl),
% 0.13/0.40 inference(split_clause,[status(thm)],[f846,f214,f317,f351])).
% 0.13/0.40 fof(f852,plain,(
% 0.13/0.40 $false|~sQ12_spl),
% 0.13/0.40 inference(forward_subsumption_resolution,[status(thm)],[f218,f136])).
% 0.13/0.40 fof(f853,plain,(
% 0.13/0.40 ~sQ12_spl),
% 0.13/0.40 inference(contradiction_clause,[status(thm)],[f852])).
% 0.13/0.40 fof(f866,definition,(
% 0.13/0.40 sQ125_spl <=> (zero(out1(or1(f1(a)))))),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ125_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f881,plain,(
% 0.13/0.40 ~and_ok(and2(h1(f1(a))))|zero(out1(and2(h1(f1(a)))))|~sQ58_spl),
% 0.13/0.40 inference(resolution,[status(thm)],[f460,f76])).
% 0.13/0.40 fof(f886,plain,(
% 0.13/0.40 ~sQ47_spl|sQ52_spl|~sQ58_spl),
% 0.13/0.40 inference(split_clause,[status(thm)],[f881,f402,f425,f459])).
% 0.13/0.40 fof(f887,plain,(
% 0.13/0.40 $false|~sQ48_spl),
% 0.13/0.40 inference(forward_subsumption_resolution,[status(thm)],[f406,f135])).
% 0.13/0.40 fof(f888,plain,(
% 0.13/0.40 ~sQ48_spl),
% 0.13/0.40 inference(contradiction_clause,[status(thm)],[f887])).
% 0.13/0.40 fof(f897,plain,(
% 0.13/0.40 ~or_ok(or1(f1(a)))|~zero(in1(or1(f1(a))))|zero(out1(or1(f1(a))))|~sQ29_spl),
% 0.13/0.40 inference(resolution,[status(thm)],[f301,f86])).
% 0.13/0.40 fof(f899,plain,(
% 0.13/0.40 ~sQ63_spl|~sQ25_spl|sQ125_spl|~sQ29_spl),
% 0.13/0.40 inference(split_clause,[status(thm)],[f897,f496,f280,f866,f300])).
% 0.13/0.40 fof(f901,plain,(
% 0.13/0.40 $false|~sQ64_spl),
% 0.13/0.40 inference(forward_subsumption_resolution,[status(thm)],[f500,f134])).
% 0.13/0.40 fof(f902,plain,(
% 0.13/0.40 ~sQ64_spl),
% 0.13/0.40 inference(contradiction_clause,[status(thm)],[f901])).
% 0.13/0.40 fof(f1123,plain,(
% 0.13/0.40 ~zero(out1(or1(f1(a))))|zero(outc(f1(a)))),
% 0.13/0.40 inference(resolution,[status(thm)],[f665,f72])).
% 0.13/0.40 fof(f1127,plain,(
% 0.13/0.40 ~sQ125_spl|sQ98_spl),
% 0.13/0.40 inference(split_clause,[status(thm)],[f1123,f866,f701])).
% 0.13/0.40 fof(f1130,plain,(
% 0.13/0.40 $false|~sQ99_spl),
% 0.13/0.40 inference(forward_subsumption_resolution,[status(thm)],[f705,f153])).
% 0.13/0.40 fof(f1131,plain,(
% 0.13/0.40 ~sQ99_spl),
% 0.13/0.40 inference(contradiction_clause,[status(thm)],[f1130])).
% 0.13/0.40 fof(f1132,plain,(
% 0.13/0.40 $false),
% 0.13/0.40 inference(sat_refutation,[status(thm)],[f220,f248,f268,f288,f308,f320,f356,f408,f428,f464,f502,f707,f725,f727,f741,f743,f851,f853,f886,f888,f899,f902,f1127,f1131])).
% 0.13/0.40 % SZS output end CNFRefutation for theBenchmark.p
% 0.13/0.43 % Elapsed time: 0.057425 seconds
% 0.13/0.43 % CPU time: 0.185093 seconds
% 0.13/0.43 % Total memory used: 21.596 MB
% 0.13/0.43 % Net memory used: 21.528 MB
%------------------------------------------------------------------------------