%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : HWV008-2.001 : TPTP v8.1.0. Bugfixed v2.7.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n019.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:42 EDT 2022
% Result : Unsatisfiable 0.19s 0.46s
% Output : Refutation 0.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 30
% Syntax : Number of clauses : 84 ( 27 unt; 9 nHn; 84 RR)
% Number of literals : 162 ( 0 equ; 78 neg)
% Maximal clause size : 4 ( 1 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 12 ( 11 usr; 1 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 3 con; 0-1 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
( ~ nbit_adder1(u)
| fulladder(f1(u)) ),
file('HWV008-2.001.p',unknown),
[] ).
cnf(3,axiom,
( ~ nbit_adder1(u)
| connection(outc(u),outc(f1(u))) ),
file('HWV008-2.001.p',unknown),
[] ).
cnf(4,axiom,
( ~ nbit_adder1(u)
| connection(ina1(u),in1(f1(u))) ),
file('HWV008-2.001.p',unknown),
[] ).
cnf(5,axiom,
( ~ nbit_adder1(u)
| connection(inb1(u),in2(f1(u))) ),
file('HWV008-2.001.p',unknown),
[] ).
cnf(7,axiom,
nbit_adder1(a),
file('HWV008-2.001.p',unknown),
[] ).
cnf(8,axiom,
zero(ina1(a)),
file('HWV008-2.001.p',unknown),
[] ).
cnf(9,axiom,
zero(inb1(a)),
file('HWV008-2.001.p',unknown),
[] ).
cnf(12,axiom,
one(outc(a)),
file('HWV008-2.001.p',unknown),
[] ).
cnf(13,axiom,
~ abnormal(or1(f1(a))),
file('HWV008-2.001.p',unknown),
[] ).
cnf(14,axiom,
~ abnormal(and2(h1(f1(a)))),
file('HWV008-2.001.p',unknown),
[] ).
cnf(15,axiom,
~ abnormal(and2(h2(f1(a)))),
file('HWV008-2.001.p',unknown),
[] ).
cnf(16,axiom,
( ~ zero(u)
| ~ connection(u,v)
| zero(v) ),
file('HWV008-2.001.p',unknown),
[] ).
cnf(17,axiom,
( ~ one(u)
| ~ connection(u,v)
| one(v) ),
file('HWV008-2.001.p',unknown),
[] ).
cnf(19,axiom,
( ~ one(u)
| ~ connection(v,u)
| one(v) ),
file('HWV008-2.001.p',unknown),
[] ).
cnf(20,axiom,
( ~ one(u)
| ~ zero(u) ),
file('HWV008-2.001.p',unknown),
[] ).
cnf(21,axiom,
( ~ and_ok(u)
| ~ zero(in1(u))
| zero(out1(u)) ),
file('HWV008-2.001.p',unknown),
[] ).
cnf(28,axiom,
( ~ logic_and(u)
| abnormal(u)
| and_ok(u) ),
file('HWV008-2.001.p',unknown),
[] ).
cnf(32,axiom,
( ~ or_ok(u)
| ~ one(out1(u))
| one(in2(u))
| one(in1(u)) ),
file('HWV008-2.001.p',unknown),
[] ).
cnf(36,axiom,
( ~ logic_or(u)
| abnormal(u)
| or_ok(u) ),
file('HWV008-2.001.p',unknown),
[] ).
cnf(44,axiom,
( ~ halfadder(u)
| logic_and(and2(u)) ),
file('HWV008-2.001.p',unknown),
[] ).
cnf(49,axiom,
( ~ halfadder(u)
| connection(in1(u),in1(and2(u))) ),
file('HWV008-2.001.p',unknown),
[] ).
cnf(52,axiom,
( ~ halfadder(u)
| connection(outc(u),out1(and2(u))) ),
file('HWV008-2.001.p',unknown),
[] ).
cnf(56,axiom,
( ~ fulladder(u)
| halfadder(h1(u)) ),
file('HWV008-2.001.p',unknown),
[] ).
cnf(57,axiom,
( ~ fulladder(u)
| halfadder(h2(u)) ),
file('HWV008-2.001.p',unknown),
[] ).
cnf(58,axiom,
( ~ fulladder(u)
| logic_or(or1(u)) ),
file('HWV008-2.001.p',unknown),
[] ).
cnf(60,axiom,
( ~ fulladder(u)
| connection(outc(h1(u)),in2(or1(u))) ),
file('HWV008-2.001.p',unknown),
[] ).
cnf(61,axiom,
( ~ fulladder(u)
| connection(outc(h2(u)),in1(or1(u))) ),
file('HWV008-2.001.p',unknown),
[] ).
cnf(62,axiom,
( ~ fulladder(u)
| connection(in1(u),in1(h2(u))) ),
file('HWV008-2.001.p',unknown),
[] ).
cnf(63,axiom,
( ~ fulladder(u)
| connection(in2(u),in1(h1(u))) ),
file('HWV008-2.001.p',unknown),
[] ).
cnf(66,axiom,
( ~ fulladder(u)
| connection(outc(u),out1(or1(u))) ),
file('HWV008-2.001.p',unknown),
[] ).
cnf(68,plain,
( ~ logic_or(or1(f1(a)))
| or_ok(or1(f1(a))) ),
inference(res,[status(thm),theory(equality)],[36,13]),
[iquote('0:Res:36.2,13.0')] ).
cnf(70,plain,
( ~ logic_and(and2(h2(f1(a))))
| and_ok(and2(h2(f1(a)))) ),
inference(res,[status(thm),theory(equality)],[28,15]),
[iquote('0:Res:28.2,15.0')] ).
cnf(73,plain,
( ~ logic_and(and2(h1(f1(a))))
| and_ok(and2(h1(f1(a)))) ),
inference(res,[status(thm),theory(equality)],[28,14]),
[iquote('0:Res:28.2,14.0')] ).
cnf(127,plain,
( ~ fulladder(f1(a))
| or_ok(or1(f1(a))) ),
inference(sor,[status(thm)],[68,58]),
[iquote('0:SoR:68.0,58.1')] ).
cnf(129,plain,
or_ok(or1(f1(a))),
inference(ssi,[status(thm)],[127,1,7]),
[iquote('0:SSi:127.0,1.0,7.1')] ).
cnf(160,plain,
( ~ fulladder(u)
| ~ one(outc(u))
| one(out1(or1(u))) ),
inference(res,[status(thm),theory(equality)],[66,17]),
[iquote('0:Res:66.1,17.1')] ).
cnf(161,plain,
( ~ halfadder(u)
| ~ one(outc(u))
| one(out1(and2(u))) ),
inference(res,[status(thm),theory(equality)],[52,17]),
[iquote('0:Res:52.1,17.1')] ).
cnf(164,plain,
( ~ nbit_adder1(u)
| ~ one(outc(u))
| one(outc(f1(u))) ),
inference(res,[status(thm),theory(equality)],[3,17]),
[iquote('0:Res:3.1,17.1')] ).
cnf(181,plain,
( ~ nbit_adder1(u)
| ~ zero(inb1(u))
| zero(in2(f1(u))) ),
inference(res,[status(thm),theory(equality)],[5,16]),
[iquote('0:Res:5.1,16.1')] ).
cnf(185,plain,
( ~ nbit_adder1(u)
| ~ zero(ina1(u))
| zero(in1(f1(u))) ),
inference(res,[status(thm),theory(equality)],[4,16]),
[iquote('0:Res:4.1,16.1')] ).
cnf(186,plain,
( ~ fulladder(u)
| ~ zero(in2(u))
| zero(in1(h1(u))) ),
inference(res,[status(thm),theory(equality)],[63,16]),
[iquote('0:Res:63.1,16.1')] ).
cnf(187,plain,
( ~ fulladder(u)
| ~ zero(in1(u))
| zero(in1(h2(u))) ),
inference(res,[status(thm),theory(equality)],[62,16]),
[iquote('0:Res:62.1,16.1')] ).
cnf(188,plain,
( ~ halfadder(u)
| ~ zero(in1(u))
| zero(in1(and2(u))) ),
inference(res,[status(thm),theory(equality)],[49,16]),
[iquote('0:Res:49.1,16.1')] ).
cnf(198,plain,
( ~ fulladder(u)
| ~ one(in1(or1(u)))
| one(outc(h2(u))) ),
inference(res,[status(thm),theory(equality)],[61,19]),
[iquote('0:Res:61.1,19.1')] ).
cnf(202,plain,
( ~ fulladder(u)
| ~ one(in2(or1(u)))
| one(outc(h1(u))) ),
inference(res,[status(thm),theory(equality)],[60,19]),
[iquote('0:Res:60.1,19.1')] ).
cnf(250,plain,
( ~ halfadder(h1(f1(a)))
| and_ok(and2(h1(f1(a)))) ),
inference(sor,[status(thm)],[73,44]),
[iquote('0:SoR:73.0,44.1')] ).
cnf(251,plain,
and_ok(and2(h1(f1(a)))),
inference(ssi,[status(thm)],[250,56,1,7]),
[iquote('0:SSi:250.0,56.0,1.1,7.1')] ).
cnf(255,plain,
( ~ halfadder(h2(f1(a)))
| and_ok(and2(h2(f1(a)))) ),
inference(sor,[status(thm)],[70,44]),
[iquote('0:SoR:70.0,44.1')] ).
cnf(256,plain,
and_ok(and2(h2(f1(a)))),
inference(ssi,[status(thm)],[255,57,1,7]),
[iquote('0:SSi:255.0,57.0,1.1,7.1')] ).
cnf(308,plain,
( ~ nbit_adder1(a)
| one(outc(f1(a))) ),
inference(sor,[status(thm)],[164,12]),
[iquote('0:SoR:164.1,12.0')] ).
cnf(309,plain,
one(outc(f1(a))),
inference(ssi,[status(thm)],[308,7]),
[iquote('0:SSi:308.0,7.0')] ).
cnf(312,plain,
( ~ fulladder(f1(a))
| one(out1(or1(f1(a)))) ),
inference(sor,[status(thm)],[160,309]),
[iquote('0:SoR:160.1,309.0')] ).
cnf(314,plain,
one(out1(or1(f1(a)))),
inference(ssi,[status(thm)],[312,1,7]),
[iquote('0:SSi:312.0,1.0,7.1')] ).
cnf(320,plain,
( ~ or_ok(or1(f1(a)))
| one(in2(or1(f1(a))))
| one(in1(or1(f1(a)))) ),
inference(res,[status(thm),theory(equality)],[314,32]),
[iquote('0:Res:314.0,32.1')] ).
cnf(324,plain,
( one(in2(or1(f1(a))))
| one(in1(or1(f1(a)))) ),
inference(ssi,[status(thm)],[320,129,58,1,7]),
[iquote('0:SSi:320.0,129.0,58.1,1.1,7.0')] ).
cnf(340,plain,
( ~ nbit_adder1(a)
| zero(in2(f1(a))) ),
inference(sor,[status(thm)],[181,9]),
[iquote('0:SoR:181.1,9.0')] ).
cnf(341,plain,
zero(in2(f1(a))),
inference(ssi,[status(thm)],[340,7]),
[iquote('0:SSi:340.0,7.0')] ).
cnf(346,plain,
( ~ nbit_adder1(a)
| zero(in1(f1(a))) ),
inference(sor,[status(thm)],[185,8]),
[iquote('0:SoR:185.1,8.0')] ).
cnf(347,plain,
zero(in1(f1(a))),
inference(ssi,[status(thm)],[346,7]),
[iquote('0:SSi:346.0,7.0')] ).
cnf(350,plain,
( ~ fulladder(f1(a))
| zero(in1(h1(f1(a)))) ),
inference(sor,[status(thm)],[186,341]),
[iquote('0:SoR:186.1,341.0')] ).
cnf(351,plain,
zero(in1(h1(f1(a)))),
inference(ssi,[status(thm)],[350,1,7]),
[iquote('0:SSi:350.0,1.0,7.1')] ).
cnf(355,plain,
( ~ fulladder(f1(a))
| zero(in1(h2(f1(a)))) ),
inference(sor,[status(thm)],[187,347]),
[iquote('0:SoR:187.1,347.0')] ).
cnf(356,plain,
zero(in1(h2(f1(a)))),
inference(ssi,[status(thm)],[355,1,7]),
[iquote('0:SSi:355.0,1.0,7.1')] ).
cnf(357,plain,
( ~ halfadder(h1(f1(a)))
| zero(in1(and2(h1(f1(a))))) ),
inference(sor,[status(thm)],[188,351]),
[iquote('0:SoR:188.1,351.0')] ).
cnf(359,plain,
zero(in1(and2(h1(f1(a))))),
inference(ssi,[status(thm)],[357,56,1,7]),
[iquote('0:SSi:357.0,56.0,1.1,7.1')] ).
cnf(361,plain,
( ~ halfadder(h2(f1(a)))
| zero(in1(and2(h2(f1(a))))) ),
inference(sor,[status(thm)],[188,356]),
[iquote('0:SoR:188.1,356.0')] ).
cnf(364,plain,
zero(in1(and2(h2(f1(a))))),
inference(ssi,[status(thm)],[361,57,1,7]),
[iquote('0:SSi:361.0,57.0,1.1,7.1')] ).
cnf(434,plain,
( ~ fulladder(f1(a))
| one(outc(h2(f1(a))))
| one(in2(or1(f1(a)))) ),
inference(sor,[status(thm)],[198,324]),
[iquote('0:SoR:198.1,324.1')] ).
cnf(436,plain,
( one(outc(h2(f1(a))))
| one(in2(or1(f1(a)))) ),
inference(ssi,[status(thm)],[434,1,7]),
[iquote('0:SSi:434.0,1.0,7.1')] ).
cnf(438,plain,
( ~ halfadder(h2(f1(a)))
| one(out1(and2(h2(f1(a)))))
| one(in2(or1(f1(a)))) ),
inference(sor,[status(thm)],[161,436]),
[iquote('0:SoR:161.1,436.0')] ).
cnf(440,plain,
( one(out1(and2(h2(f1(a)))))
| one(in2(or1(f1(a)))) ),
inference(ssi,[status(thm)],[438,57,1,7]),
[iquote('0:SSi:438.0,57.0,1.1,7.1')] ).
cnf(441,plain,
one(in2(or1(f1(a)))),
inference(spt,[spt(split,[position(s1)])],[440]),
[iquote('1:Spt:440.1')] ).
cnf(447,plain,
( ~ fulladder(f1(a))
| one(outc(h1(f1(a)))) ),
inference(sor,[status(thm)],[202,441]),
[iquote('1:SoR:202.1,441.0')] ).
cnf(448,plain,
one(outc(h1(f1(a)))),
inference(ssi,[status(thm)],[447,1,7]),
[iquote('1:SSi:447.0,1.0,7.1')] ).
cnf(450,plain,
( ~ halfadder(h1(f1(a)))
| one(out1(and2(h1(f1(a))))) ),
inference(sor,[status(thm)],[161,448]),
[iquote('1:SoR:161.1,448.0')] ).
cnf(452,plain,
one(out1(and2(h1(f1(a))))),
inference(ssi,[status(thm)],[450,56,1,7]),
[iquote('1:SSi:450.0,56.0,1.1,7.1')] ).
cnf(454,plain,
( ~ and_ok(and2(h1(f1(a))))
| ~ zero(in1(and2(h1(f1(a))))) ),
inference(ems,[status(thm)],[20,452,21]),
[iquote('1:EmS:20.0,20.1,452.0,21.2')] ).
cnf(466,plain,
~ zero(in1(and2(h1(f1(a))))),
inference(ssi,[status(thm)],[454,251,44,56,1,7]),
[iquote('1:SSi:454.0,251.0,44.1,56.1,1.1,7.0')] ).
cnf(467,plain,
$false,
inference(mrr,[status(thm)],[466,359]),
[iquote('1:MRR:466.0,359.0')] ).
cnf(469,plain,
~ one(in2(or1(f1(a)))),
inference(spt,[spt(split,[position(sa)])],[467,441]),
[iquote('1:Spt:467.0,440.1,441.0')] ).
cnf(470,plain,
one(out1(and2(h2(f1(a))))),
inference(spt,[spt(split,[position(s2)])],[440]),
[iquote('1:Spt:467.0,440.0')] ).
cnf(474,plain,
( ~ and_ok(and2(h2(f1(a))))
| ~ zero(in1(and2(h2(f1(a))))) ),
inference(ems,[status(thm)],[20,470,21]),
[iquote('1:EmS:20.0,20.1,470.0,21.2')] ).
cnf(485,plain,
~ zero(in1(and2(h2(f1(a))))),
inference(ssi,[status(thm)],[474,256,44,57,1,7]),
[iquote('1:SSi:474.0,256.0,44.1,57.1,1.1,7.0')] ).
cnf(486,plain,
$false,
inference(mrr,[status(thm)],[485,364]),
[iquote('1:MRR:485.0,364.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : HWV008-2.001 : TPTP v8.1.0. Bugfixed v2.7.0.
% 0.12/0.13 % Command : run_spass %d %s
% 0.12/0.34 % Computer : n019.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 04:38:39 EDT 2022
% 0.12/0.34 % CPUTime :
% 0.19/0.46
% 0.19/0.46 SPASS V 3.9
% 0.19/0.46 SPASS beiseite: Proof found.
% 0.19/0.46 % SZS status Theorem
% 0.19/0.46 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.46 SPASS derived 330 clauses, backtracked 4 clauses, performed 1 splits and kept 217 clauses.
% 0.19/0.46 SPASS allocated 76047 KBytes.
% 0.19/0.46 SPASS spent 0:00:00.10 on the problem.
% 0.19/0.46 0:00:00.03 for the input.
% 0.19/0.46 0:00:00.00 for the FLOTTER CNF translation.
% 0.19/0.46 0:00:00.01 for inferences.
% 0.19/0.46 0:00:00.00 for the backtracking.
% 0.19/0.46 0:00:00.03 for the reduction.
% 0.19/0.46
% 0.19/0.46
% 0.19/0.46 Here is a proof with depth 10, length 84 :
% 0.19/0.46 % SZS output start Refutation
% See solution above
% 0.19/0.46 Formulae used in the proof : nbit_adder_fulladder1 nbit_adder_connection_outc_outcf1 nbit_adder_connection_ina1_in1f1 nbit_adder_connection_inb1_in2f1 a_isa_1bit_adder ina1_0 inb1_0 outc_0 diagnosis_or1f1 diagnosis_and2h1f1 diagnosis_and2h2f1 value_propagation_zero1 value_propagation_one1 value_propagation_one2 unique_value and_0x_0 and_ok_or_abnormal or_1_11 or_ok_or_abnormal halfadder_and2 halfadder_connection_in1_in1and2 halfadder_connection_outc_out1and2 fulladder_halfadder1 fulladder_halfadder2 fulladder_or1 fulladder_connection_outch1_in2or1 fulladder_connection_outch2_in1or1 fulladder_connection_in1_in1h2 fulladder_connection_in2_in1h1 fulladder_connection_outc_out1or1
% 0.19/0.46
%------------------------------------------------------------------------------