%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : HWV005-1 : TPTP v9.3.1. Released v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/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:38 PM UTC 2026
% Result : Unsatisfiable 0.15s 5.42s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HWV005-1 : TPTP v9.3.1. Released v2.1.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/5.39 % Computer : n001.cluster.edu
% 0.11/5.39 % Model : x86_64 x86_64
% 0.11/5.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.39 % Memory : 8046.5625MB
% 0.11/5.39 % OS : Linux 6.8.0-71-generic
% 0.11/5.39 % CPULimit : 300
% 0.11/5.39 % WCLimit : 300
% 0.11/5.39 % DateTime : Sun Sep 20 20:52:49 UTC 2026
% 0.11/5.39 % CPUTime :
% 0.15/5.40 % Drodi V4.1.1
% 0.15/5.42 % Refutation found
% 0.15/5.42 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.15/5.42 % SZS output start CNFRefutation for theBenchmark
% 0.15/5.42 fof(f1,axiom,(
% 0.15/5.42 (![P1,P2,V]: (( ~ connection(P1,P2)| ~ value(P1,V)| value(P2,V) ) ))),
% 0.15/5.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.42 fof(f3,axiom,(
% 0.15/5.42 (![P,V1,V2]: (( ~ value(P,V1)| ~ value(P,V2)| equal_value(V1,V2) ) ))),
% 0.15/5.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.42 fof(f4,axiom,(
% 0.15/5.42 ~ equal_value(n0,n1) ),
% 0.15/5.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.42 fof(f5,axiom,(
% 0.15/5.42 ~ equal_value(n1,n0) ),
% 0.15/5.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.42 fof(f7,axiom,(
% 0.15/5.42 (![K,Any]: (( ~ type(K,Any)| mode(K,ok)| mode(K,abnormal) ) ))),
% 0.15/5.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.42 fof(f10,axiom,(
% 0.15/5.42 (![K]: (( ~ mode(K,ok)| ~ type(K,and)| ~ value(out(n1,K),n0)| value(in(n1,K),n0)| value(in(n2,K),n0) ) ))),
% 0.15/5.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.42 fof(f13,axiom,(
% 0.15/5.42 (![K,Any]: (( ~ mode(K,ok)| ~ type(K,or)| ~ value(in(Any,K),n1)| value(out(n1,K),n1) ) ))),
% 0.15/5.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.42 fof(f18,axiom,(
% 0.15/5.42 (![K]: (( ~ mode(K,ok)| ~ type(K,not)| ~ value(in(n1,K),n0)| value(out(n1,K),n1) ) ))),
% 0.15/5.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.42 fof(f22,axiom,(
% 0.15/5.42 (![X]: (( ~ type(X,halfadder)| type(and1(X),and) ) ))),
% 0.15/5.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.42 fof(f24,axiom,(
% 0.15/5.42 (![X]: (( ~ type(X,halfadder)| type(not1(X),not) ) ))),
% 0.15/5.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.42 fof(f25,axiom,(
% 0.15/5.42 (![X]: (( ~ type(X,halfadder)| type(or1(X),or) ) ))),
% 0.15/5.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.42 fof(f26,axiom,(
% 0.15/5.42 (![X]: (( ~ type(X,halfadder)| connection(in(n1,X),in(n1,or1(X))) ) ))),
% 0.15/5.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.42 fof(f30,axiom,(
% 0.15/5.42 (![X]: (( ~ type(X,halfadder)| connection(out(s,X),out(n1,and1(X))) ) ))),
% 0.15/5.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.42 fof(f31,axiom,(
% 0.15/5.42 (![X]: (( ~ type(X,halfadder)| connection(out(c,X),out(n1,and2(X))) ) ))),
% 0.15/5.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.42 fof(f32,axiom,(
% 0.15/5.42 (![X]: (( ~ type(X,halfadder)| connection(out(n1,or1(X)),in(n1,and1(X))) ) ))),
% 0.15/5.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.42 fof(f33,axiom,(
% 0.15/5.42 (![X]: (( ~ type(X,halfadder)| connection(out(n1,and2(X)),in(n1,not1(X))) ) ))),
% 0.15/5.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.42 fof(f34,axiom,(
% 0.15/5.42 (![X]: (( ~ type(X,halfadder)| connection(out(n1,not1(X)),in(n2,and1(X))) ) ))),
% 0.15/5.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.42 fof(f35,hypothesis,(
% 0.15/5.42 type(h,halfadder) ),
% 0.15/5.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.42 fof(f36,hypothesis,(
% 0.15/5.42 value(in(n1,h),n1) ),
% 0.15/5.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.42 fof(f38,hypothesis,(
% 0.15/5.42 value(out(s,h),n0) ),
% 0.15/5.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.42 fof(f39,hypothesis,(
% 0.15/5.42 value(out(c,h),n0) ),
% 0.15/5.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.42 fof(f40,negated_conjecture,(
% 0.15/5.42 ~ mode(and1(h),abnormal) ),
% 0.15/5.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.42 fof(f41,negated_conjecture,(
% 0.15/5.42 ~ mode(not1(h),abnormal) ),
% 0.15/5.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.42 fof(f42,negated_conjecture,(
% 0.15/5.42 ~ mode(or1(h),abnormal) ),
% 0.15/5.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.15/5.42 fof(f43,plain,(
% 0.15/5.42 ![P2,V]: ((![P1]: (~connection(P1,P2)|~value(P1,V)))|value(P2,V))),
% 0.15/5.42 inference(miniscoping,[status(thm)],[f1])).
% 0.15/5.42 fof(f44,plain,(
% 0.15/5.42 ![X0,X1,X2]: (~connection(X0,X1)|~value(X0,X2)|value(X1,X2))),
% 0.15/5.42 inference(cnf_transformation,[status(thm)],[f43])).
% 0.15/5.42 fof(f47,plain,(
% 0.15/5.42 ![V1,V2]: ((![P]: (~value(P,V1)|~value(P,V2)))|equal_value(V1,V2))),
% 0.15/5.42 inference(miniscoping,[status(thm)],[f3])).
% 0.15/5.42 fof(f48,plain,(
% 0.15/5.42 ![X0,X1,X2]: (~value(X0,X1)|~value(X0,X2)|equal_value(X1,X2))),
% 0.15/5.42 inference(cnf_transformation,[status(thm)],[f47])).
% 0.15/5.42 fof(f49,plain,(
% 0.15/5.42 ~equal_value(n0,n1)),
% 0.15/5.42 inference(cnf_transformation,[status(thm)],[f4])).
% 0.15/5.42 fof(f50,plain,(
% 0.15/5.42 ~equal_value(n1,n0)),
% 0.15/5.42 inference(cnf_transformation,[status(thm)],[f5])).
% 0.15/5.42 fof(f52,plain,(
% 0.15/5.42 ![K]: (((![Any]: ~type(K,Any))|mode(K,ok))|mode(K,abnormal))),
% 0.15/5.42 inference(miniscoping,[status(thm)],[f7])).
% 0.15/5.42 fof(f53,plain,(
% 0.15/5.42 ![X0,X1]: (~type(X0,X1)|mode(X0,ok)|mode(X0,abnormal))),
% 0.15/5.42 inference(cnf_transformation,[status(thm)],[f52])).
% 0.15/5.42 fof(f57,plain,(
% 0.15/5.42 ![X0]: (~mode(X0,ok)|~type(X0,and)|~value(out(n1,X0),n0)|value(in(n1,X0),n0)|value(in(n2,X0),n0))),
% 0.15/5.42 inference(cnf_transformation,[status(thm)],[f10])).
% 0.15/5.42 fof(f60,plain,(
% 0.15/5.42 ![K]: (((~mode(K,ok)|~type(K,or))|(![Any]: ~value(in(Any,K),n1)))|value(out(n1,K),n1))),
% 0.15/5.42 inference(miniscoping,[status(thm)],[f13])).
% 0.15/5.42 fof(f61,plain,(
% 0.15/5.42 ![X0,X1]: (~mode(X0,ok)|~type(X0,or)|~value(in(X1,X0),n1)|value(out(n1,X0),n1))),
% 0.15/5.42 inference(cnf_transformation,[status(thm)],[f60])).
% 0.15/5.42 fof(f66,plain,(
% 0.15/5.42 ![X0]: (~mode(X0,ok)|~type(X0,not)|~value(in(n1,X0),n0)|value(out(n1,X0),n1))),
% 0.15/5.42 inference(cnf_transformation,[status(thm)],[f18])).
% 0.15/5.42 fof(f70,plain,(
% 0.15/5.42 ![X0]: (~type(X0,halfadder)|type(and1(X0),and))),
% 0.15/5.42 inference(cnf_transformation,[status(thm)],[f22])).
% 0.15/5.42 fof(f72,plain,(
% 0.15/5.42 ![X0]: (~type(X0,halfadder)|type(not1(X0),not))),
% 0.15/5.42 inference(cnf_transformation,[status(thm)],[f24])).
% 0.15/5.42 fof(f73,plain,(
% 0.15/5.42 ![X0]: (~type(X0,halfadder)|type(or1(X0),or))),
% 0.15/5.42 inference(cnf_transformation,[status(thm)],[f25])).
% 0.15/5.42 fof(f74,plain,(
% 0.15/5.42 ![X0]: (~type(X0,halfadder)|connection(in(n1,X0),in(n1,or1(X0))))),
% 0.15/5.42 inference(cnf_transformation,[status(thm)],[f26])).
% 0.15/5.42 fof(f78,plain,(
% 0.15/5.42 ![X0]: (~type(X0,halfadder)|connection(out(s,X0),out(n1,and1(X0))))),
% 0.15/5.42 inference(cnf_transformation,[status(thm)],[f30])).
% 0.15/5.42 fof(f79,plain,(
% 0.15/5.42 ![X0]: (~type(X0,halfadder)|connection(out(c,X0),out(n1,and2(X0))))),
% 0.15/5.42 inference(cnf_transformation,[status(thm)],[f31])).
% 0.15/5.42 fof(f80,plain,(
% 0.15/5.42 ![X0]: (~type(X0,halfadder)|connection(out(n1,or1(X0)),in(n1,and1(X0))))),
% 0.15/5.42 inference(cnf_transformation,[status(thm)],[f32])).
% 0.15/5.42 fof(f81,plain,(
% 0.15/5.42 ![X0]: (~type(X0,halfadder)|connection(out(n1,and2(X0)),in(n1,not1(X0))))),
% 0.15/5.42 inference(cnf_transformation,[status(thm)],[f33])).
% 0.15/5.42 fof(f82,plain,(
% 0.15/5.42 ![X0]: (~type(X0,halfadder)|connection(out(n1,not1(X0)),in(n2,and1(X0))))),
% 0.15/5.42 inference(cnf_transformation,[status(thm)],[f34])).
% 0.15/5.42 fof(f83,plain,(
% 0.15/5.42 type(h,halfadder)),
% 0.15/5.42 inference(cnf_transformation,[status(thm)],[f35])).
% 0.15/5.42 fof(f84,plain,(
% 0.15/5.42 value(in(n1,h),n1)),
% 0.15/5.42 inference(cnf_transformation,[status(thm)],[f36])).
% 0.15/5.42 fof(f86,plain,(
% 0.15/5.42 value(out(s,h),n0)),
% 0.15/5.42 inference(cnf_transformation,[status(thm)],[f38])).
% 0.15/5.42 fof(f87,plain,(
% 0.15/5.42 value(out(c,h),n0)),
% 0.15/5.42 inference(cnf_transformation,[status(thm)],[f39])).
% 0.15/5.42 fof(f88,plain,(
% 0.15/5.42 ~mode(and1(h),abnormal)),
% 0.15/5.42 inference(cnf_transformation,[status(thm)],[f40])).
% 0.15/5.42 fof(f89,plain,(
% 0.15/5.42 ~mode(not1(h),abnormal)),
% 0.15/5.42 inference(cnf_transformation,[status(thm)],[f41])).
% 0.15/5.42 fof(f90,plain,(
% 0.15/5.42 ~mode(or1(h),abnormal)),
% 0.15/5.42 inference(cnf_transformation,[status(thm)],[f42])).
% 0.15/5.42 fof(f91,plain,(
% 0.15/5.42 type(and1(h),and)),
% 0.15/5.42 inference(resolution,[status(thm)],[f70,f83])).
% 0.15/5.42 fof(f92,plain,(
% 0.15/5.42 type(not1(h),not)),
% 0.15/5.42 inference(resolution,[status(thm)],[f72,f83])).
% 0.15/5.42 fof(f93,plain,(
% 0.15/5.42 type(or1(h),or)),
% 0.15/5.42 inference(resolution,[status(thm)],[f73,f83])).
% 0.15/5.42 fof(f94,plain,(
% 0.15/5.42 connection(in(n1,h),in(n1,or1(h)))),
% 0.15/5.42 inference(resolution,[status(thm)],[f74,f83])).
% 0.15/5.42 fof(f95,plain,(
% 0.15/5.42 mode(and1(h),ok)|mode(and1(h),abnormal)),
% 0.15/5.42 inference(resolution,[status(thm)],[f53,f91])).
% 0.15/5.42 fof(f97,definition,(
% 0.15/5.42 sQ0_spl <=> (mode(and1(h),ok))),
% 0.15/5.42 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.15/5.42 fof(f100,definition,(
% 0.15/5.42 sQ1_spl <=> (mode(and1(h),abnormal))),
% 0.15/5.42 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.15/5.42 fof(f101,plain,(
% 0.15/5.42 mode(and1(h),abnormal)|~sQ1_spl),
% 0.15/5.42 inference(component_clause,[status(thm)],[f100])).
% 0.15/5.42 fof(f103,plain,(
% 0.15/5.42 sQ0_spl|sQ1_spl),
% 0.15/5.42 inference(split_clause,[status(thm)],[f95,f97,f100])).
% 0.15/5.42 fof(f112,plain,(
% 0.15/5.42 connection(out(n1,or1(h)),in(n1,and1(h)))),
% 0.15/5.42 inference(resolution,[status(thm)],[f80,f83])).
% 0.15/5.42 fof(f113,plain,(
% 0.15/5.42 connection(out(n1,and2(h)),in(n1,not1(h)))),
% 0.15/5.42 inference(resolution,[status(thm)],[f81,f83])).
% 0.15/5.42 fof(f114,plain,(
% 0.15/5.42 connection(out(n1,not1(h)),in(n2,and1(h)))),
% 0.15/5.42 inference(resolution,[status(thm)],[f82,f83])).
% 0.15/5.42 fof(f125,plain,(
% 0.15/5.42 mode(not1(h),ok)|mode(not1(h),abnormal)),
% 0.15/5.42 inference(resolution,[status(thm)],[f92,f53])).
% 0.15/5.42 fof(f126,definition,(
% 0.15/5.42 sQ6_spl <=> (mode(not1(h),ok))),
% 0.15/5.42 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.15/5.42 fof(f129,definition,(
% 0.15/5.42 sQ7_spl <=> (mode(not1(h),abnormal))),
% 0.15/5.42 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.15/5.42 fof(f130,plain,(
% 0.15/5.42 mode(not1(h),abnormal)|~sQ7_spl),
% 0.15/5.42 inference(component_clause,[status(thm)],[f129])).
% 0.15/5.42 fof(f132,plain,(
% 0.15/5.42 sQ6_spl|sQ7_spl),
% 0.15/5.42 inference(split_clause,[status(thm)],[f125,f126,f129])).
% 0.15/5.42 fof(f133,plain,(
% 0.15/5.42 $false|~sQ7_spl),
% 0.15/5.42 inference(forward_subsumption_resolution,[status(thm)],[f130,f89])).
% 0.15/5.42 fof(f134,plain,(
% 0.15/5.42 ~sQ7_spl),
% 0.15/5.42 inference(contradiction_clause,[status(thm)],[f133])).
% 0.15/5.42 fof(f135,plain,(
% 0.15/5.42 mode(or1(h),ok)|mode(or1(h),abnormal)),
% 0.15/5.42 inference(resolution,[status(thm)],[f93,f53])).
% 0.15/5.42 fof(f136,definition,(
% 0.15/5.42 sQ8_spl <=> (mode(or1(h),ok))),
% 0.15/5.42 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.15/5.42 fof(f139,definition,(
% 0.15/5.42 sQ9_spl <=> (mode(or1(h),abnormal))),
% 0.15/5.42 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.15/5.42 fof(f140,plain,(
% 0.15/5.42 mode(or1(h),abnormal)|~sQ9_spl),
% 0.15/5.42 inference(component_clause,[status(thm)],[f139])).
% 0.15/5.42 fof(f142,plain,(
% 0.15/5.42 sQ8_spl|sQ9_spl),
% 0.15/5.42 inference(split_clause,[status(thm)],[f135,f136,f139])).
% 0.15/5.42 fof(f143,plain,(
% 0.15/5.42 $false|~sQ9_spl),
% 0.15/5.42 inference(forward_subsumption_resolution,[status(thm)],[f140,f90])).
% 0.15/5.42 fof(f144,plain,(
% 0.15/5.42 ~sQ9_spl),
% 0.15/5.42 inference(contradiction_clause,[status(thm)],[f143])).
% 0.15/5.42 fof(f156,plain,(
% 0.15/5.42 ![X0]: (~value(in(n1,h),X0)|value(in(n1,or1(h)),X0))),
% 0.15/5.42 inference(resolution,[status(thm)],[f94,f44])).
% 0.15/5.42 fof(f160,plain,(
% 0.15/5.42 ![X0]: (~value(out(n1,or1(h)),X0)|value(in(n1,and1(h)),X0))),
% 0.15/5.42 inference(resolution,[status(thm)],[f112,f44])).
% 0.15/5.42 fof(f162,plain,(
% 0.15/5.42 ![X0]: (~value(out(n1,and2(h)),X0)|value(in(n1,not1(h)),X0))),
% 0.15/5.42 inference(resolution,[status(thm)],[f113,f44])).
% 0.15/5.42 fof(f164,plain,(
% 0.15/5.42 ![X0]: (~value(out(n1,not1(h)),X0)|value(in(n2,and1(h)),X0))),
% 0.15/5.42 inference(resolution,[status(thm)],[f114,f44])).
% 0.15/5.42 fof(f167,plain,(
% 0.15/5.42 value(in(n1,or1(h)),n1)),
% 0.15/5.42 inference(resolution,[status(thm)],[f156,f84])).
% 0.15/5.42 fof(f194,plain,(
% 0.15/5.42 ~mode(or1(h),ok)|~type(or1(h),or)|value(out(n1,or1(h)),n1)),
% 0.15/5.42 inference(resolution,[status(thm)],[f61,f167])).
% 0.15/5.42 fof(f196,definition,(
% 0.15/5.42 sQ16_spl <=> (type(or1(h),or))),
% 0.15/5.42 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.15/5.42 fof(f198,plain,(
% 0.15/5.42 ~type(or1(h),or)|sQ16_spl),
% 0.15/5.42 inference(component_clause,[status(thm)],[f196])).
% 0.15/5.42 fof(f199,definition,(
% 0.15/5.42 sQ17_spl <=> (value(out(n1,or1(h)),n1))),
% 0.15/5.42 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.15/5.42 fof(f200,plain,(
% 0.15/5.42 value(out(n1,or1(h)),n1)|~sQ17_spl),
% 0.15/5.42 inference(component_clause,[status(thm)],[f199])).
% 0.15/5.42 fof(f202,plain,(
% 0.15/5.42 ~sQ8_spl|~sQ16_spl|sQ17_spl),
% 0.15/5.42 inference(split_clause,[status(thm)],[f194,f136,f196,f199])).
% 0.15/5.42 fof(f210,plain,(
% 0.15/5.42 $false|sQ16_spl),
% 0.15/5.42 inference(forward_subsumption_resolution,[status(thm)],[f198,f93])).
% 0.15/5.42 fof(f211,plain,(
% 0.15/5.42 sQ16_spl),
% 0.15/5.42 inference(contradiction_clause,[status(thm)],[f210])).
% 0.15/5.42 fof(f212,plain,(
% 0.15/5.42 value(in(n1,and1(h)),n1)|~sQ17_spl),
% 0.15/5.42 inference(resolution,[status(thm)],[f200,f160])).
% 0.15/5.42 fof(f228,plain,(
% 0.15/5.42 ![X0]: (~value(in(n1,and1(h)),X0)|equal_value(n1,X0)|~sQ17_spl)),
% 0.15/5.42 inference(resolution,[status(thm)],[f212,f48])).
% 0.15/5.42 fof(f236,plain,(
% 0.15/5.42 $false|~sQ1_spl),
% 0.15/5.42 inference(forward_subsumption_resolution,[status(thm)],[f101,f88])).
% 0.15/5.42 fof(f237,plain,(
% 0.15/5.42 ~sQ1_spl),
% 0.15/5.42 inference(contradiction_clause,[status(thm)],[f236])).
% 0.15/5.42 fof(f308,plain,(
% 0.15/5.42 connection(out(s,h),out(n1,and1(h)))),
% 0.15/5.42 inference(resolution,[status(thm)],[f78,f83])).
% 0.15/5.42 fof(f309,plain,(
% 0.15/5.42 connection(out(c,h),out(n1,and2(h)))),
% 0.15/5.42 inference(resolution,[status(thm)],[f79,f83])).
% 0.15/5.42 fof(f311,plain,(
% 0.15/5.42 ![X0]: (~value(out(s,h),X0)|value(out(n1,and1(h)),X0))),
% 0.15/5.42 inference(resolution,[status(thm)],[f308,f44])).
% 0.15/5.42 fof(f313,plain,(
% 0.15/5.42 ![X0]: (~value(out(c,h),X0)|value(out(n1,and2(h)),X0))),
% 0.15/5.42 inference(resolution,[status(thm)],[f309,f44])).
% 0.15/5.42 fof(f346,plain,(
% 0.15/5.42 value(out(n1,and1(h)),n0)),
% 0.15/5.42 inference(resolution,[status(thm)],[f311,f86])).
% 0.15/5.42 fof(f347,plain,(
% 0.15/5.42 value(out(n1,and2(h)),n0)),
% 0.15/5.42 inference(resolution,[status(thm)],[f313,f87])).
% 0.15/5.42 fof(f352,plain,(
% 0.15/5.42 ~mode(and1(h),ok)|~type(and1(h),and)|value(in(n1,and1(h)),n0)|value(in(n2,and1(h)),n0)),
% 0.15/5.42 inference(resolution,[status(thm)],[f346,f57])).
% 0.15/5.42 fof(f358,definition,(
% 0.15/5.42 sQ38_spl <=> (value(in(n2,and1(h)),n0))),
% 0.15/5.42 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 0.15/5.42 fof(f359,plain,(
% 0.15/5.42 value(in(n2,and1(h)),n0)|~sQ38_spl),
% 0.15/5.42 inference(component_clause,[status(thm)],[f358])).
% 0.15/5.42 fof(f362,definition,(
% 0.15/5.42 sQ39_spl <=> (value(in(n1,and1(h)),n0))),
% 0.15/5.42 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 0.15/5.42 fof(f363,plain,(
% 0.15/5.42 value(in(n1,and1(h)),n0)|~sQ39_spl),
% 0.15/5.42 inference(component_clause,[status(thm)],[f362])).
% 0.15/5.42 fof(f366,definition,(
% 0.15/5.42 sQ40_spl <=> (type(and1(h),and))),
% 0.15/5.42 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 0.15/5.42 fof(f368,plain,(
% 0.15/5.42 ~type(and1(h),and)|sQ40_spl),
% 0.15/5.42 inference(component_clause,[status(thm)],[f366])).
% 0.15/5.42 fof(f369,plain,(
% 0.15/5.42 ~sQ0_spl|~sQ40_spl|sQ39_spl|sQ38_spl),
% 0.15/5.42 inference(split_clause,[status(thm)],[f352,f97,f366,f362,f358])).
% 0.15/5.42 fof(f371,plain,(
% 0.15/5.42 value(in(n1,not1(h)),n0)),
% 0.15/5.42 inference(resolution,[status(thm)],[f347,f162])).
% 0.15/5.42 fof(f385,plain,(
% 0.15/5.42 ![X0]: (~value(in(n2,and1(h)),X0)|equal_value(n0,X0)|~sQ38_spl)),
% 0.15/5.42 inference(resolution,[status(thm)],[f359,f48])).
% 0.15/5.42 fof(f388,plain,(
% 0.15/5.42 $false|sQ40_spl),
% 0.15/5.42 inference(forward_subsumption_resolution,[status(thm)],[f368,f91])).
% 0.15/5.42 fof(f389,plain,(
% 0.15/5.42 sQ40_spl),
% 0.15/5.42 inference(contradiction_clause,[status(thm)],[f388])).
% 0.15/5.42 fof(f391,plain,(
% 0.15/5.42 ~mode(not1(h),ok)|~type(not1(h),not)|value(out(n1,not1(h)),n1)),
% 0.15/5.42 inference(resolution,[status(thm)],[f371,f66])).
% 0.15/5.42 fof(f394,definition,(
% 0.15/5.42 sQ41_spl <=> (type(not1(h),not))),
% 0.15/5.42 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 0.15/5.42 fof(f396,plain,(
% 0.15/5.42 ~type(not1(h),not)|sQ41_spl),
% 0.15/5.42 inference(component_clause,[status(thm)],[f394])).
% 0.15/5.42 fof(f397,definition,(
% 0.15/5.42 sQ42_spl <=> (value(out(n1,not1(h)),n1))),
% 0.15/5.42 introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 0.15/5.42 fof(f398,plain,(
% 0.15/5.42 value(out(n1,not1(h)),n1)|~sQ42_spl),
% 0.15/5.42 inference(component_clause,[status(thm)],[f397])).
% 0.15/5.42 fof(f400,plain,(
% 0.15/5.42 ~sQ6_spl|~sQ41_spl|sQ42_spl),
% 0.15/5.42 inference(split_clause,[status(thm)],[f391,f126,f394,f397])).
% 0.15/5.42 fof(f408,plain,(
% 0.15/5.42 $false|sQ41_spl),
% 0.15/5.42 inference(forward_subsumption_resolution,[status(thm)],[f396,f92])).
% 0.15/5.42 fof(f409,plain,(
% 0.15/5.42 sQ41_spl),
% 0.15/5.42 inference(contradiction_clause,[status(thm)],[f408])).
% 0.15/5.42 fof(f410,plain,(
% 0.15/5.42 equal_value(n1,n0)|~sQ39_spl|~sQ17_spl),
% 0.15/5.42 inference(resolution,[status(thm)],[f363,f228])).
% 0.15/5.42 fof(f415,plain,(
% 0.15/5.42 $false|~sQ39_spl|~sQ17_spl),
% 0.15/5.42 inference(forward_subsumption_resolution,[status(thm)],[f410,f50])).
% 0.15/5.42 fof(f416,plain,(
% 0.15/5.42 ~sQ39_spl|~sQ17_spl),
% 0.15/5.42 inference(contradiction_clause,[status(thm)],[f415])).
% 0.15/5.42 fof(f417,plain,(
% 0.15/5.42 value(in(n2,and1(h)),n1)|~sQ42_spl),
% 0.15/5.42 inference(resolution,[status(thm)],[f398,f164])).
% 0.15/5.42 fof(f462,plain,(
% 0.15/5.42 equal_value(n0,n1)|~sQ42_spl|~sQ38_spl),
% 0.15/5.42 inference(resolution,[status(thm)],[f417,f385])).
% 0.15/5.42 fof(f467,plain,(
% 0.15/5.42 $false|~sQ42_spl|~sQ38_spl),
% 0.15/5.42 inference(forward_subsumption_resolution,[status(thm)],[f462,f49])).
% 0.15/5.42 fof(f468,plain,(
% 0.15/5.42 ~sQ42_spl|~sQ38_spl),
% 0.15/5.42 inference(contradiction_clause,[status(thm)],[f467])).
% 0.15/5.42 fof(f469,plain,(
% 0.15/5.42 $false),
% 0.15/5.42 inference(sat_refutation,[status(thm)],[f103,f132,f134,f142,f144,f202,f211,f237,f369,f389,f400,f409,f416,f468])).
% 0.15/5.42 % SZS output end CNFRefutation for theBenchmark.p
% 0.15/5.45 % Elapsed time: 0.044154 seconds
% 0.15/5.45 % CPU time: 0.131697 seconds
% 0.15/5.45 % Total memory used: 18.596 MB
% 0.15/5.45 % Net memory used: 18.543 MB
%------------------------------------------------------------------------------