%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : HWV007-2 : TPTP v8.1.0. Bugfixed v2.7.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n028.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 600s
% DateTime : Sat Jul 16 19:14:41 EDT 2022
% Result : Unsatisfiable 0.19s 0.45s
% Output : Refutation 0.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 36
% Number of leaves : 48
% Syntax : Number of clauses : 134 ( 44 unt; 3 nHn; 134 RR)
% Number of literals : 258 ( 0 equ; 136 neg)
% Maximal clause size : 4 ( 1 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 13 ( 12 usr; 1 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 3 con; 0-1 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
fulladder(f),
file('HWV007-2.p',unknown),
[] ).
cnf(2,axiom,
zero(in1(f)),
file('HWV007-2.p',unknown),
[] ).
cnf(3,axiom,
one(in2(f)),
file('HWV007-2.p',unknown),
[] ).
cnf(4,axiom,
one(inc(f)),
file('HWV007-2.p',unknown),
[] ).
cnf(5,axiom,
one(outs(f)),
file('HWV007-2.p',unknown),
[] ).
cnf(6,axiom,
zero(outc(f)),
file('HWV007-2.p',unknown),
[] ).
cnf(7,axiom,
~ abnormal(and2(h1(f))),
file('HWV007-2.p',unknown),
[] ).
cnf(8,axiom,
( ~ abnormal(or1(f))
| ~ abnormal(and1(h1(f))) ),
file('HWV007-2.p',unknown),
[] ).
cnf(9,axiom,
( ~ abnormal(or1(f))
| ~ abnormal(not1(h1(f))) ),
file('HWV007-2.p',unknown),
[] ).
cnf(10,axiom,
( ~ abnormal(or1(f))
| ~ abnormal(and1(h2(f))) ),
file('HWV007-2.p',unknown),
[] ).
cnf(11,axiom,
( ~ abnormal(or1(f))
| ~ abnormal(or1(h2(f))) ),
file('HWV007-2.p',unknown),
[] ).
cnf(12,axiom,
( ~ zero(u)
| ~ connection(u,v)
| zero(v) ),
file('HWV007-2.p',unknown),
[] ).
cnf(13,axiom,
( ~ one(u)
| ~ connection(u,v)
| one(v) ),
file('HWV007-2.p',unknown),
[] ).
cnf(14,axiom,
( ~ zero(u)
| ~ connection(v,u)
| zero(v) ),
file('HWV007-2.p',unknown),
[] ).
cnf(15,axiom,
( ~ one(u)
| ~ connection(v,u)
| one(v) ),
file('HWV007-2.p',unknown),
[] ).
cnf(16,axiom,
( ~ one(u)
| ~ zero(u) ),
file('HWV007-2.p',unknown),
[] ).
cnf(18,axiom,
( ~ and_ok(u)
| ~ zero(in2(u))
| zero(out1(u)) ),
file('HWV007-2.p',unknown),
[] ).
cnf(19,axiom,
( ~ and_ok(u)
| ~ one(in2(u))
| ~ one(in1(u))
| one(out1(u)) ),
file('HWV007-2.p',unknown),
[] ).
cnf(21,axiom,
( ~ and_ok(u)
| ~ one(out1(u))
| one(in1(u)) ),
file('HWV007-2.p',unknown),
[] ).
cnf(24,axiom,
( ~ logic_and(u)
| abnormal(u)
| and_ok(u) ),
file('HWV007-2.p',unknown),
[] ).
cnf(27,axiom,
( ~ or_ok(u)
| ~ zero(in2(u))
| ~ zero(in1(u))
| zero(out1(u)) ),
file('HWV007-2.p',unknown),
[] ).
cnf(30,axiom,
( ~ or_ok(u)
| ~ zero(out1(u))
| zero(in2(u)) ),
file('HWV007-2.p',unknown),
[] ).
cnf(32,axiom,
( ~ logic_or(u)
| abnormal(u)
| or_ok(u) ),
file('HWV007-2.p',unknown),
[] ).
cnf(34,axiom,
( ~ not_ok(u)
| ~ one(in1(u))
| zero(out1(u)) ),
file('HWV007-2.p',unknown),
[] ).
cnf(38,axiom,
( ~ logic_not(u)
| abnormal(u)
| not_ok(u) ),
file('HWV007-2.p',unknown),
[] ).
cnf(39,axiom,
( ~ halfadder(u)
| logic_and(and1(u)) ),
file('HWV007-2.p',unknown),
[] ).
cnf(40,axiom,
( ~ halfadder(u)
| logic_and(and2(u)) ),
file('HWV007-2.p',unknown),
[] ).
cnf(41,axiom,
( ~ halfadder(u)
| logic_not(not1(u)) ),
file('HWV007-2.p',unknown),
[] ).
cnf(42,axiom,
( ~ halfadder(u)
| logic_or(or1(u)) ),
file('HWV007-2.p',unknown),
[] ).
cnf(43,axiom,
( ~ halfadder(u)
| connection(in1(u),in1(or1(u))) ),
file('HWV007-2.p',unknown),
[] ).
cnf(44,axiom,
( ~ halfadder(u)
| connection(in2(u),in2(or1(u))) ),
file('HWV007-2.p',unknown),
[] ).
cnf(45,axiom,
( ~ halfadder(u)
| connection(in1(u),in1(and2(u))) ),
file('HWV007-2.p',unknown),
[] ).
cnf(46,axiom,
( ~ halfadder(u)
| connection(in2(u),in2(and2(u))) ),
file('HWV007-2.p',unknown),
[] ).
cnf(47,axiom,
( ~ halfadder(u)
| connection(outs(u),out1(and1(u))) ),
file('HWV007-2.p',unknown),
[] ).
cnf(48,axiom,
( ~ halfadder(u)
| connection(outc(u),out1(and2(u))) ),
file('HWV007-2.p',unknown),
[] ).
cnf(49,axiom,
( ~ halfadder(u)
| connection(out1(or1(u)),in1(and1(u))) ),
file('HWV007-2.p',unknown),
[] ).
cnf(50,axiom,
( ~ halfadder(u)
| connection(out1(and2(u)),in1(not1(u))) ),
file('HWV007-2.p',unknown),
[] ).
cnf(51,axiom,
( ~ halfadder(u)
| connection(out1(not1(u)),in2(and1(u))) ),
file('HWV007-2.p',unknown),
[] ).
cnf(52,axiom,
( ~ fulladder(u)
| halfadder(h1(u)) ),
file('HWV007-2.p',unknown),
[] ).
cnf(53,axiom,
( ~ fulladder(u)
| halfadder(h2(u)) ),
file('HWV007-2.p',unknown),
[] ).
cnf(54,axiom,
( ~ fulladder(u)
| logic_or(or1(u)) ),
file('HWV007-2.p',unknown),
[] ).
cnf(55,axiom,
( ~ fulladder(u)
| connection(outs(h1(u)),in2(h2(u))) ),
file('HWV007-2.p',unknown),
[] ).
cnf(56,axiom,
( ~ fulladder(u)
| connection(outc(h1(u)),in2(or1(u))) ),
file('HWV007-2.p',unknown),
[] ).
cnf(58,axiom,
( ~ fulladder(u)
| connection(in1(u),in1(h2(u))) ),
file('HWV007-2.p',unknown),
[] ).
cnf(59,axiom,
( ~ fulladder(u)
| connection(in2(u),in1(h1(u))) ),
file('HWV007-2.p',unknown),
[] ).
cnf(60,axiom,
( ~ fulladder(u)
| connection(inc(u),in2(h1(u))) ),
file('HWV007-2.p',unknown),
[] ).
cnf(61,axiom,
( ~ fulladder(u)
| connection(outs(u),outs(h2(u))) ),
file('HWV007-2.p',unknown),
[] ).
cnf(62,axiom,
( ~ fulladder(u)
| connection(outc(u),out1(or1(u))) ),
file('HWV007-2.p',unknown),
[] ).
cnf(63,plain,
( ~ logic_and(and2(h1(f)))
| and_ok(and2(h1(f))) ),
inference(res,[status(thm),theory(equality)],[24,7]),
[iquote('0:Res:24.2,7.0')] ).
cnf(107,plain,
~ abnormal(or1(f)),
inference(spt,[spt(split,[position(s1)])],[10]),
[iquote('1:Spt:10.0')] ).
cnf(110,plain,
( ~ logic_or(or1(f))
| or_ok(or1(f)) ),
inference(res,[status(thm),theory(equality)],[32,107]),
[iquote('1:Res:32.1,107.0')] ).
cnf(112,plain,
or_ok(or1(f)),
inference(ssi,[status(thm)],[110,54,1]),
[iquote('1:SSi:110.0,54.0,1.1')] ).
cnf(118,plain,
( ~ halfadder(h1(f))
| and_ok(and2(h1(f))) ),
inference(sor,[status(thm)],[63,40]),
[iquote('0:SoR:63.0,40.1')] ).
cnf(119,plain,
and_ok(and2(h1(f))),
inference(ssi,[status(thm)],[118,52,1]),
[iquote('0:SSi:118.0,52.0,1.1')] ).
cnf(125,plain,
( ~ halfadder(u)
| ~ zero(out1(and1(u)))
| zero(outs(u)) ),
inference(res,[status(thm),theory(equality)],[47,14]),
[iquote('0:Res:47.1,14.1')] ).
cnf(134,plain,
( ~ fulladder(u)
| ~ zero(outc(u))
| zero(out1(or1(u))) ),
inference(res,[status(thm),theory(equality)],[62,12]),
[iquote('0:Res:62.1,12.1')] ).
cnf(139,plain,
( ~ halfadder(u)
| ~ zero(in2(u))
| zero(in2(or1(u))) ),
inference(res,[status(thm),theory(equality)],[44,12]),
[iquote('0:Res:44.1,12.1')] ).
cnf(141,plain,
( ~ fulladder(u)
| ~ zero(in1(u))
| zero(in1(h2(u))) ),
inference(res,[status(thm),theory(equality)],[58,12]),
[iquote('0:Res:58.1,12.1')] ).
cnf(143,plain,
( ~ halfadder(u)
| ~ zero(in1(u))
| zero(in1(or1(u))) ),
inference(res,[status(thm),theory(equality)],[43,12]),
[iquote('0:Res:43.1,12.1')] ).
cnf(146,plain,
( ~ halfadder(u)
| ~ one(out1(and2(u)))
| one(outc(u)) ),
inference(res,[status(thm),theory(equality)],[48,15]),
[iquote('0:Res:48.1,15.1')] ).
cnf(158,plain,
( ~ halfadder(u)
| ~ one(outs(u))
| one(out1(and1(u))) ),
inference(res,[status(thm),theory(equality)],[47,13]),
[iquote('0:Res:47.1,13.1')] ).
cnf(159,plain,
( ~ fulladder(u)
| ~ one(inc(u))
| one(in2(h1(u))) ),
inference(res,[status(thm),theory(equality)],[60,13]),
[iquote('0:Res:60.1,13.1')] ).
cnf(160,plain,
( ~ halfadder(u)
| ~ one(in2(u))
| one(in2(and2(u))) ),
inference(res,[status(thm),theory(equality)],[46,13]),
[iquote('0:Res:46.1,13.1')] ).
cnf(162,plain,
( ~ fulladder(u)
| ~ one(in2(u))
| one(in1(h1(u))) ),
inference(res,[status(thm),theory(equality)],[59,13]),
[iquote('0:Res:59.1,13.1')] ).
cnf(164,plain,
( ~ halfadder(u)
| ~ one(in1(u))
| one(in1(and2(u))) ),
inference(res,[status(thm),theory(equality)],[45,13]),
[iquote('0:Res:45.1,13.1')] ).
cnf(166,plain,
( ~ fulladder(u)
| ~ one(outs(u))
| one(outs(h2(u))) ),
inference(res,[status(thm),theory(equality)],[61,13]),
[iquote('0:Res:61.1,13.1')] ).
cnf(173,plain,
( ~ fulladder(u)
| ~ one(outc(h1(u)))
| one(in2(or1(u))) ),
inference(res,[status(thm),theory(equality)],[56,13]),
[iquote('0:Res:56.1,13.1')] ).
cnf(178,plain,
( ~ fulladder(u)
| ~ zero(outs(h1(u)))
| zero(in2(h2(u))) ),
inference(res,[status(thm),theory(equality)],[55,12]),
[iquote('0:Res:55.1,12.1')] ).
cnf(182,plain,
( ~ halfadder(u)
| ~ zero(out1(not1(u)))
| zero(in2(and1(u))) ),
inference(res,[status(thm),theory(equality)],[51,12]),
[iquote('0:Res:51.1,12.1')] ).
cnf(185,plain,
( ~ halfadder(u)
| ~ one(out1(and2(u)))
| one(in1(not1(u))) ),
inference(res,[status(thm),theory(equality)],[50,13]),
[iquote('0:Res:50.1,13.1')] ).
cnf(190,plain,
( ~ halfadder(u)
| ~ zero(out1(or1(u)))
| zero(in1(and1(u))) ),
inference(res,[status(thm),theory(equality)],[49,12]),
[iquote('0:Res:49.1,12.1')] ).
cnf(233,plain,
( ~ fulladder(f)
| zero(out1(or1(f))) ),
inference(sor,[status(thm)],[134,6]),
[iquote('0:SoR:134.1,6.0')] ).
cnf(234,plain,
zero(out1(or1(f))),
inference(ssi,[status(thm)],[233,1]),
[iquote('0:SSi:233.0,1.0')] ).
cnf(246,plain,
( ~ fulladder(f)
| zero(in1(h2(f))) ),
inference(sor,[status(thm)],[141,2]),
[iquote('0:SoR:141.1,2.0')] ).
cnf(247,plain,
zero(in1(h2(f))),
inference(ssi,[status(thm)],[246,1]),
[iquote('0:SSi:246.0,1.0')] ).
cnf(269,plain,
( ~ halfadder(h2(f))
| zero(in1(or1(h2(f)))) ),
inference(sor,[status(thm)],[143,247]),
[iquote('0:SoR:143.1,247.0')] ).
cnf(273,plain,
zero(in1(or1(h2(f)))),
inference(ssi,[status(thm)],[269,53,1]),
[iquote('0:SSi:269.0,53.0,1.1')] ).
cnf(281,plain,
( ~ or_ok(or1(h2(f)))
| ~ zero(in2(or1(h2(f))))
| zero(out1(or1(h2(f)))) ),
inference(res,[status(thm),theory(equality)],[273,27]),
[iquote('0:Res:273.0,27.2')] ).
cnf(302,plain,
( ~ fulladder(f)
| one(in2(h1(f))) ),
inference(sor,[status(thm)],[159,4]),
[iquote('0:SoR:159.1,4.0')] ).
cnf(303,plain,
one(in2(h1(f))),
inference(ssi,[status(thm)],[302,1]),
[iquote('0:SSi:302.0,1.0')] ).
cnf(307,plain,
( ~ halfadder(h1(f))
| one(in2(and2(h1(f)))) ),
inference(sor,[status(thm)],[160,303]),
[iquote('0:SoR:160.1,303.0')] ).
cnf(310,plain,
one(in2(and2(h1(f)))),
inference(ssi,[status(thm)],[307,52,1]),
[iquote('0:SSi:307.0,52.0,1.1')] ).
cnf(329,plain,
( ~ fulladder(f)
| one(in1(h1(f))) ),
inference(sor,[status(thm)],[162,3]),
[iquote('0:SoR:162.1,3.0')] ).
cnf(330,plain,
one(in1(h1(f))),
inference(ssi,[status(thm)],[329,1]),
[iquote('0:SSi:329.0,1.0')] ).
cnf(342,plain,
( ~ halfadder(h1(f))
| one(in1(and2(h1(f)))) ),
inference(sor,[status(thm)],[164,330]),
[iquote('0:SoR:164.1,330.0')] ).
cnf(346,plain,
one(in1(and2(h1(f)))),
inference(ssi,[status(thm)],[342,52,1]),
[iquote('0:SSi:342.0,52.0,1.1')] ).
cnf(352,plain,
( ~ and_ok(and2(h1(f)))
| ~ one(in2(and2(h1(f))))
| one(out1(and2(h1(f)))) ),
inference(res,[status(thm),theory(equality)],[346,19]),
[iquote('0:Res:346.0,19.2')] ).
cnf(356,plain,
( ~ one(in2(and2(h1(f))))
| one(out1(and2(h1(f)))) ),
inference(ssi,[status(thm)],[352,119,40,52,1]),
[iquote('0:SSi:352.0,119.0,40.1,52.1,1.0')] ).
cnf(357,plain,
one(out1(and2(h1(f)))),
inference(mrr,[status(thm)],[356,310]),
[iquote('0:MRR:356.0,310.0')] ).
cnf(358,plain,
( ~ halfadder(h1(f))
| one(outc(h1(f))) ),
inference(sor,[status(thm)],[146,357]),
[iquote('0:SoR:146.1,357.0')] ).
cnf(360,plain,
one(outc(h1(f))),
inference(ssi,[status(thm)],[358,52,1]),
[iquote('0:SSi:358.0,52.0,1.1')] ).
cnf(386,plain,
( ~ fulladder(f)
| one(outs(h2(f))) ),
inference(sor,[status(thm)],[166,5]),
[iquote('0:SoR:166.1,5.0')] ).
cnf(387,plain,
one(outs(h2(f))),
inference(ssi,[status(thm)],[386,1]),
[iquote('0:SSi:386.0,1.0')] ).
cnf(389,plain,
( ~ halfadder(h2(f))
| one(out1(and1(h2(f)))) ),
inference(sor,[status(thm)],[158,387]),
[iquote('0:SoR:158.1,387.0')] ).
cnf(391,plain,
one(out1(and1(h2(f)))),
inference(ssi,[status(thm)],[389,53,1]),
[iquote('0:SSi:389.0,53.0,1.1')] ).
cnf(404,plain,
( ~ fulladder(f)
| one(in2(or1(f))) ),
inference(sor,[status(thm)],[173,360]),
[iquote('0:SoR:173.1,360.0')] ).
cnf(405,plain,
one(in2(or1(f))),
inference(ssi,[status(thm)],[404,1]),
[iquote('0:SSi:404.0,1.0')] ).
cnf(406,plain,
( ~ or_ok(or1(f))
| ~ zero(out1(or1(f))) ),
inference(ems,[status(thm)],[16,405,30]),
[iquote('0:EmS:16.0,16.1,405.0,30.2')] ).
cnf(414,plain,
~ zero(out1(or1(f))),
inference(ssi,[status(thm)],[406,112,54,1]),
[iquote('1:SSi:406.0,112.0,54.1,1.0')] ).
cnf(415,plain,
$false,
inference(mrr,[status(thm)],[414,234]),
[iquote('1:MRR:414.0,234.0')] ).
cnf(416,plain,
abnormal(or1(f)),
inference(spt,[spt(split,[position(sa)])],[415,107]),
[iquote('1:Spt:415.0,10.0,107.0')] ).
cnf(417,plain,
~ abnormal(and1(h2(f))),
inference(spt,[spt(split,[position(s2)])],[10]),
[iquote('1:Spt:415.0,10.1')] ).
cnf(418,plain,
~ abnormal(or1(h2(f))),
inference(mrr,[status(thm)],[11,416]),
[iquote('1:MRR:11.0,416.0')] ).
cnf(419,plain,
~ abnormal(not1(h1(f))),
inference(mrr,[status(thm)],[9,416]),
[iquote('1:MRR:9.0,416.0')] ).
cnf(420,plain,
~ abnormal(and1(h1(f))),
inference(mrr,[status(thm)],[8,416]),
[iquote('1:MRR:8.0,416.0')] ).
cnf(422,plain,
( ~ logic_and(and1(h2(f)))
| and_ok(and1(h2(f))) ),
inference(res,[status(thm),theory(equality)],[24,417]),
[iquote('1:Res:24.1,417.0')] ).
cnf(425,plain,
and_ok(and1(h2(f))),
inference(ssi,[status(thm)],[422,39,53,1]),
[iquote('1:SSi:422.0,39.0,53.1,1.1')] ).
cnf(430,plain,
( ~ logic_or(or1(h2(f)))
| or_ok(or1(h2(f))) ),
inference(res,[status(thm),theory(equality)],[32,418]),
[iquote('1:Res:32.1,418.0')] ).
cnf(432,plain,
or_ok(or1(h2(f))),
inference(ssi,[status(thm)],[430,42,53,1]),
[iquote('1:SSi:430.0,42.0,53.1,1.1')] ).
cnf(434,plain,
( ~ zero(in2(or1(h2(f))))
| zero(out1(or1(h2(f)))) ),
inference(mrr,[status(thm)],[281,432]),
[iquote('1:MRR:281.0,432.0')] ).
cnf(440,plain,
( ~ logic_not(not1(h1(f)))
| not_ok(not1(h1(f))) ),
inference(res,[status(thm),theory(equality)],[38,419]),
[iquote('1:Res:38.1,419.0')] ).
cnf(441,plain,
not_ok(not1(h1(f))),
inference(ssi,[status(thm)],[440,41,52,1]),
[iquote('1:SSi:440.0,41.0,52.1,1.1')] ).
cnf(445,plain,
( ~ logic_and(and1(h1(f)))
| and_ok(and1(h1(f))) ),
inference(res,[status(thm),theory(equality)],[24,420]),
[iquote('1:Res:24.1,420.0')] ).
cnf(448,plain,
and_ok(and1(h1(f))),
inference(ssi,[status(thm)],[445,39,52,1]),
[iquote('1:SSi:445.0,39.0,52.1,1.1')] ).
cnf(476,plain,
( ~ halfadder(h1(f))
| one(in1(not1(h1(f)))) ),
inference(sor,[status(thm)],[185,357]),
[iquote('0:SoR:185.1,357.0')] ).
cnf(478,plain,
one(in1(not1(h1(f)))),
inference(ssi,[status(thm)],[476,52,1]),
[iquote('0:SSi:476.0,52.0,1.1')] ).
cnf(487,plain,
( ~ not_ok(not1(h1(f)))
| zero(out1(not1(h1(f)))) ),
inference(res,[status(thm),theory(equality)],[478,34]),
[iquote('0:Res:478.0,34.1')] ).
cnf(488,plain,
zero(out1(not1(h1(f)))),
inference(ssi,[status(thm)],[487,441,41,52,1]),
[iquote('1:SSi:487.0,441.0,41.1,52.1,1.0')] ).
cnf(492,plain,
( ~ halfadder(h1(f))
| zero(in2(and1(h1(f)))) ),
inference(sor,[status(thm)],[182,488]),
[iquote('1:SoR:182.1,488.0')] ).
cnf(493,plain,
zero(in2(and1(h1(f)))),
inference(ssi,[status(thm)],[492,52,1]),
[iquote('1:SSi:492.0,52.0,1.1')] ).
cnf(500,plain,
( ~ and_ok(and1(h1(f)))
| zero(out1(and1(h1(f)))) ),
inference(res,[status(thm),theory(equality)],[493,18]),
[iquote('1:Res:493.0,18.1')] ).
cnf(501,plain,
zero(out1(and1(h1(f)))),
inference(ssi,[status(thm)],[500,448,39,52,1]),
[iquote('1:SSi:500.0,448.0,39.1,52.1,1.0')] ).
cnf(504,plain,
( ~ halfadder(h1(f))
| zero(outs(h1(f))) ),
inference(sor,[status(thm)],[125,501]),
[iquote('1:SoR:125.1,501.0')] ).
cnf(505,plain,
zero(outs(h1(f))),
inference(ssi,[status(thm)],[504,52,1]),
[iquote('1:SSi:504.0,52.0,1.1')] ).
cnf(508,plain,
( ~ fulladder(f)
| zero(in2(h2(f))) ),
inference(sor,[status(thm)],[178,505]),
[iquote('1:SoR:178.1,505.0')] ).
cnf(509,plain,
zero(in2(h2(f))),
inference(ssi,[status(thm)],[508,1]),
[iquote('1:SSi:508.0,1.0')] ).
cnf(512,plain,
( ~ halfadder(h2(f))
| zero(in2(or1(h2(f)))) ),
inference(sor,[status(thm)],[139,509]),
[iquote('1:SoR:139.1,509.0')] ).
cnf(516,plain,
zero(in2(or1(h2(f)))),
inference(ssi,[status(thm)],[512,53,1]),
[iquote('1:SSi:512.0,53.0,1.1')] ).
cnf(517,plain,
zero(out1(or1(h2(f)))),
inference(mrr,[status(thm)],[434,516]),
[iquote('1:MRR:434.0,516.0')] ).
cnf(549,plain,
( ~ halfadder(h2(f))
| zero(in1(and1(h2(f)))) ),
inference(sor,[status(thm)],[190,517]),
[iquote('1:SoR:190.1,517.0')] ).
cnf(551,plain,
zero(in1(and1(h2(f)))),
inference(ssi,[status(thm)],[549,53,1]),
[iquote('1:SSi:549.0,53.0,1.1')] ).
cnf(553,plain,
( ~ and_ok(and1(h2(f)))
| ~ one(out1(and1(h2(f)))) ),
inference(ems,[status(thm)],[16,21,551]),
[iquote('1:EmS:16.0,16.1,21.2,551.0')] ).
cnf(563,plain,
~ one(out1(and1(h2(f)))),
inference(ssi,[status(thm)],[553,425,39,53,1]),
[iquote('1:SSi:553.0,425.0,39.1,53.1,1.0')] ).
cnf(564,plain,
$false,
inference(mrr,[status(thm)],[563,391]),
[iquote('1:MRR:563.0,391.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : HWV007-2 : TPTP v8.1.0. Bugfixed v2.7.0.
% 0.11/0.12 % Command : run_spass %d %s
% 0.12/0.34 % Computer : n028.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 600
% 0.12/0.34 % DateTime : Fri Jun 17 02:45:42 EDT 2022
% 0.12/0.34 % CPUTime :
% 0.19/0.45
% 0.19/0.45 SPASS V 3.9
% 0.19/0.45 SPASS beiseite: Proof found.
% 0.19/0.45 % SZS status Theorem
% 0.19/0.45 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.45 SPASS derived 398 clauses, backtracked 7 clauses, performed 1 splits and kept 207 clauses.
% 0.19/0.45 SPASS allocated 76086 KBytes.
% 0.19/0.45 SPASS spent 0:00:00.10 on the problem.
% 0.19/0.45 0:00:00.04 for the input.
% 0.19/0.45 0:00:00.00 for the FLOTTER CNF translation.
% 0.19/0.45 0:00:00.01 for inferences.
% 0.19/0.45 0:00:00.00 for the backtracking.
% 0.19/0.45 0:00:00.04 for the reduction.
% 0.19/0.45
% 0.19/0.45
% 0.19/0.45 Here is a proof with depth 11, length 134 :
% 0.19/0.45 % SZS output start Refutation
% See solution above
% 0.19/0.46 Formulae used in the proof : f_isa_fulladder in1_1 in2_0 inc_1 outs_1 outc_0 diagnosis_and2h1 diagnosis_or1_and1h1 diagnosis_or1_not1h1 diagnosis_or1_and1h2 diagnosis_or1_or1h2 value_propagation_zero1 value_propagation_one1 value_propagation_zero2 value_propagation_one2 unique_value and_x0_0 and_11_1 and_1_1x and_ok_or_abnormal or_00_0 or_0_01 or_ok_or_abnormal not_1_0_fw not_ok_or_abnormal halfadder_and1 halfadder_and2 halfadder_not1 halfadder_or1 halfadder_connection_in1_in1or1 halfadder_connection_in2_in2or1 halfadder_connection_in1_in1and2 halfadder_connection_in2_in2and2 halfadder_connection_outs_out1and1 halfadder_connection_outc_out1and2 halfadder_connection_out1or1_in1_and1 halfadder_connection_out1and2_in1not1 halfadder_connection_out1not1_in2and1 fulladder_halfadder1 fulladder_halfadder2 fulladder_or1 fulladder_connection_outsh1_in2h2 fulladder_connection_outch1_in2or1 fulladder_connection_in1_in1h2 fulladder_connection_in2_in1h1 fulladder_connection_inc_in2h1 fulladder_connection_outs_outsh2 fulladder_connection_outc_out1or1
% 0.19/0.46
%------------------------------------------------------------------------------