%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : HWV008-2.002 : TPTP v8.1.0. Bugfixed v2.7.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n006.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:43 EDT 2022
% Result : Unsatisfiable 0.19s 0.48s
% 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(2,axiom,
( ~ nbit_adder2(u)
| fulladder(f2(u)) ),
file('HWV008-2.002.p',unknown),
[] ).
cnf(5,axiom,
( ~ nbit_adder2(u)
| connection(outc(u),outc(f2(u))) ),
file('HWV008-2.002.p',unknown),
[] ).
cnf(8,axiom,
( ~ nbit_adder2(u)
| connection(ina2(u),in1(f2(u))) ),
file('HWV008-2.002.p',unknown),
[] ).
cnf(9,axiom,
( ~ nbit_adder2(u)
| connection(inb2(u),in2(f2(u))) ),
file('HWV008-2.002.p',unknown),
[] ).
cnf(12,axiom,
nbit_adder2(a),
file('HWV008-2.002.p',unknown),
[] ).
cnf(14,axiom,
zero(ina2(a)),
file('HWV008-2.002.p',unknown),
[] ).
cnf(16,axiom,
zero(inb2(a)),
file('HWV008-2.002.p',unknown),
[] ).
cnf(20,axiom,
one(outc(a)),
file('HWV008-2.002.p',unknown),
[] ).
cnf(21,axiom,
~ abnormal(or1(f2(a))),
file('HWV008-2.002.p',unknown),
[] ).
cnf(22,axiom,
~ abnormal(and2(h1(f2(a)))),
file('HWV008-2.002.p',unknown),
[] ).
cnf(23,axiom,
~ abnormal(and2(h2(f2(a)))),
file('HWV008-2.002.p',unknown),
[] ).
cnf(24,axiom,
( ~ zero(u)
| ~ connection(u,v)
| zero(v) ),
file('HWV008-2.002.p',unknown),
[] ).
cnf(25,axiom,
( ~ one(u)
| ~ connection(u,v)
| one(v) ),
file('HWV008-2.002.p',unknown),
[] ).
cnf(27,axiom,
( ~ one(u)
| ~ connection(v,u)
| one(v) ),
file('HWV008-2.002.p',unknown),
[] ).
cnf(28,axiom,
( ~ one(u)
| ~ zero(u) ),
file('HWV008-2.002.p',unknown),
[] ).
cnf(29,axiom,
( ~ and_ok(u)
| ~ zero(in1(u))
| zero(out1(u)) ),
file('HWV008-2.002.p',unknown),
[] ).
cnf(36,axiom,
( ~ logic_and(u)
| abnormal(u)
| and_ok(u) ),
file('HWV008-2.002.p',unknown),
[] ).
cnf(40,axiom,
( ~ or_ok(u)
| ~ one(out1(u))
| one(in2(u))
| one(in1(u)) ),
file('HWV008-2.002.p',unknown),
[] ).
cnf(44,axiom,
( ~ logic_or(u)
| abnormal(u)
| or_ok(u) ),
file('HWV008-2.002.p',unknown),
[] ).
cnf(52,axiom,
( ~ halfadder(u)
| logic_and(and2(u)) ),
file('HWV008-2.002.p',unknown),
[] ).
cnf(57,axiom,
( ~ halfadder(u)
| connection(in1(u),in1(and2(u))) ),
file('HWV008-2.002.p',unknown),
[] ).
cnf(60,axiom,
( ~ halfadder(u)
| connection(outc(u),out1(and2(u))) ),
file('HWV008-2.002.p',unknown),
[] ).
cnf(64,axiom,
( ~ fulladder(u)
| halfadder(h1(u)) ),
file('HWV008-2.002.p',unknown),
[] ).
cnf(65,axiom,
( ~ fulladder(u)
| halfadder(h2(u)) ),
file('HWV008-2.002.p',unknown),
[] ).
cnf(66,axiom,
( ~ fulladder(u)
| logic_or(or1(u)) ),
file('HWV008-2.002.p',unknown),
[] ).
cnf(68,axiom,
( ~ fulladder(u)
| connection(outc(h1(u)),in2(or1(u))) ),
file('HWV008-2.002.p',unknown),
[] ).
cnf(69,axiom,
( ~ fulladder(u)
| connection(outc(h2(u)),in1(or1(u))) ),
file('HWV008-2.002.p',unknown),
[] ).
cnf(70,axiom,
( ~ fulladder(u)
| connection(in1(u),in1(h2(u))) ),
file('HWV008-2.002.p',unknown),
[] ).
cnf(71,axiom,
( ~ fulladder(u)
| connection(in2(u),in1(h1(u))) ),
file('HWV008-2.002.p',unknown),
[] ).
cnf(74,axiom,
( ~ fulladder(u)
| connection(outc(u),out1(or1(u))) ),
file('HWV008-2.002.p',unknown),
[] ).
cnf(76,plain,
( ~ logic_or(or1(f2(a)))
| or_ok(or1(f2(a))) ),
inference(res,[status(thm),theory(equality)],[44,21]),
[iquote('0:Res:44.2,21.0')] ).
cnf(78,plain,
( ~ logic_and(and2(h2(f2(a))))
| and_ok(and2(h2(f2(a)))) ),
inference(res,[status(thm),theory(equality)],[36,23]),
[iquote('0:Res:36.2,23.0')] ).
cnf(81,plain,
( ~ logic_and(and2(h1(f2(a))))
| and_ok(and2(h1(f2(a)))) ),
inference(res,[status(thm),theory(equality)],[36,22]),
[iquote('0:Res:36.2,22.0')] ).
cnf(139,plain,
( ~ fulladder(f2(a))
| or_ok(or1(f2(a))) ),
inference(sor,[status(thm)],[76,66]),
[iquote('0:SoR:76.0,66.1')] ).
cnf(141,plain,
or_ok(or1(f2(a))),
inference(ssi,[status(thm)],[139,2,12]),
[iquote('0:SSi:139.0,2.0,12.1')] ).
cnf(176,plain,
( ~ fulladder(u)
| ~ one(outc(u))
| one(out1(or1(u))) ),
inference(res,[status(thm),theory(equality)],[74,25]),
[iquote('0:Res:74.1,25.1')] ).
cnf(177,plain,
( ~ halfadder(u)
| ~ one(outc(u))
| one(out1(and2(u))) ),
inference(res,[status(thm),theory(equality)],[60,25]),
[iquote('0:Res:60.1,25.1')] ).
cnf(181,plain,
( ~ nbit_adder2(u)
| ~ one(outc(u))
| one(outc(f2(u))) ),
inference(res,[status(thm),theory(equality)],[5,25]),
[iquote('0:Res:5.1,25.1')] ).
cnf(202,plain,
( ~ nbit_adder2(u)
| ~ zero(inb2(u))
| zero(in2(f2(u))) ),
inference(res,[status(thm),theory(equality)],[9,24]),
[iquote('0:Res:9.1,24.1')] ).
cnf(207,plain,
( ~ nbit_adder2(u)
| ~ zero(ina2(u))
| zero(in1(f2(u))) ),
inference(res,[status(thm),theory(equality)],[8,24]),
[iquote('0:Res:8.1,24.1')] ).
cnf(209,plain,
( ~ fulladder(u)
| ~ zero(in2(u))
| zero(in1(h1(u))) ),
inference(res,[status(thm),theory(equality)],[71,24]),
[iquote('0:Res:71.1,24.1')] ).
cnf(210,plain,
( ~ fulladder(u)
| ~ zero(in1(u))
| zero(in1(h2(u))) ),
inference(res,[status(thm),theory(equality)],[70,24]),
[iquote('0:Res:70.1,24.1')] ).
cnf(211,plain,
( ~ halfadder(u)
| ~ zero(in1(u))
| zero(in1(and2(u))) ),
inference(res,[status(thm),theory(equality)],[57,24]),
[iquote('0:Res:57.1,24.1')] ).
cnf(226,plain,
( ~ fulladder(u)
| ~ one(in1(or1(u)))
| one(outc(h2(u))) ),
inference(res,[status(thm),theory(equality)],[69,27]),
[iquote('0:Res:69.1,27.1')] ).
cnf(230,plain,
( ~ fulladder(u)
| ~ one(in2(or1(u)))
| one(outc(h1(u))) ),
inference(res,[status(thm),theory(equality)],[68,27]),
[iquote('0:Res:68.1,27.1')] ).
cnf(278,plain,
( ~ halfadder(h1(f2(a)))
| and_ok(and2(h1(f2(a)))) ),
inference(sor,[status(thm)],[81,52]),
[iquote('0:SoR:81.0,52.1')] ).
cnf(279,plain,
and_ok(and2(h1(f2(a)))),
inference(ssi,[status(thm)],[278,64,2,12]),
[iquote('0:SSi:278.0,64.0,2.1,12.1')] ).
cnf(286,plain,
( ~ halfadder(h2(f2(a)))
| and_ok(and2(h2(f2(a)))) ),
inference(sor,[status(thm)],[78,52]),
[iquote('0:SoR:78.0,52.1')] ).
cnf(287,plain,
and_ok(and2(h2(f2(a)))),
inference(ssi,[status(thm)],[286,65,2,12]),
[iquote('0:SSi:286.0,65.0,2.1,12.1')] ).
cnf(345,plain,
( ~ nbit_adder2(a)
| one(outc(f2(a))) ),
inference(sor,[status(thm)],[181,20]),
[iquote('0:SoR:181.1,20.0')] ).
cnf(346,plain,
one(outc(f2(a))),
inference(ssi,[status(thm)],[345,12]),
[iquote('0:SSi:345.0,12.0')] ).
cnf(349,plain,
( ~ fulladder(f2(a))
| one(out1(or1(f2(a)))) ),
inference(sor,[status(thm)],[176,346]),
[iquote('0:SoR:176.1,346.0')] ).
cnf(351,plain,
one(out1(or1(f2(a)))),
inference(ssi,[status(thm)],[349,2,12]),
[iquote('0:SSi:349.0,2.0,12.1')] ).
cnf(357,plain,
( ~ or_ok(or1(f2(a)))
| one(in2(or1(f2(a))))
| one(in1(or1(f2(a)))) ),
inference(res,[status(thm),theory(equality)],[351,40]),
[iquote('0:Res:351.0,40.1')] ).
cnf(361,plain,
( one(in2(or1(f2(a))))
| one(in1(or1(f2(a)))) ),
inference(ssi,[status(thm)],[357,141,66,2,12]),
[iquote('0:SSi:357.0,141.0,66.1,2.1,12.0')] ).
cnf(383,plain,
( ~ nbit_adder2(a)
| zero(in2(f2(a))) ),
inference(sor,[status(thm)],[202,16]),
[iquote('0:SoR:202.1,16.0')] ).
cnf(384,plain,
zero(in2(f2(a))),
inference(ssi,[status(thm)],[383,12]),
[iquote('0:SSi:383.0,12.0')] ).
cnf(394,plain,
( ~ nbit_adder2(a)
| zero(in1(f2(a))) ),
inference(sor,[status(thm)],[207,14]),
[iquote('0:SoR:207.1,14.0')] ).
cnf(395,plain,
zero(in1(f2(a))),
inference(ssi,[status(thm)],[394,12]),
[iquote('0:SSi:394.0,12.0')] ).
cnf(403,plain,
( ~ fulladder(f2(a))
| zero(in1(h1(f2(a)))) ),
inference(sor,[status(thm)],[209,384]),
[iquote('0:SoR:209.1,384.0')] ).
cnf(405,plain,
zero(in1(h1(f2(a)))),
inference(ssi,[status(thm)],[403,2,12]),
[iquote('0:SSi:403.0,2.0,12.1')] ).
cnf(410,plain,
( ~ fulladder(f2(a))
| zero(in1(h2(f2(a)))) ),
inference(sor,[status(thm)],[210,395]),
[iquote('0:SoR:210.1,395.0')] ).
cnf(412,plain,
zero(in1(h2(f2(a)))),
inference(ssi,[status(thm)],[410,2,12]),
[iquote('0:SSi:410.0,2.0,12.1')] ).
cnf(422,plain,
( ~ halfadder(h2(f2(a)))
| zero(in1(and2(h2(f2(a))))) ),
inference(sor,[status(thm)],[211,412]),
[iquote('0:SoR:211.1,412.0')] ).
cnf(424,plain,
( ~ halfadder(h1(f2(a)))
| zero(in1(and2(h1(f2(a))))) ),
inference(sor,[status(thm)],[211,405]),
[iquote('0:SoR:211.1,405.0')] ).
cnf(428,plain,
zero(in1(and2(h2(f2(a))))),
inference(ssi,[status(thm)],[422,65,2,12]),
[iquote('0:SSi:422.0,65.0,2.1,12.1')] ).
cnf(430,plain,
zero(in1(and2(h1(f2(a))))),
inference(ssi,[status(thm)],[424,64,2,12]),
[iquote('0:SSi:424.0,64.0,2.1,12.1')] ).
cnf(533,plain,
( ~ fulladder(f2(a))
| one(outc(h2(f2(a))))
| one(in2(or1(f2(a)))) ),
inference(sor,[status(thm)],[226,361]),
[iquote('0:SoR:226.1,361.1')] ).
cnf(535,plain,
( one(outc(h2(f2(a))))
| one(in2(or1(f2(a)))) ),
inference(ssi,[status(thm)],[533,2,12]),
[iquote('0:SSi:533.0,2.0,12.1')] ).
cnf(537,plain,
( ~ halfadder(h2(f2(a)))
| one(out1(and2(h2(f2(a)))))
| one(in2(or1(f2(a)))) ),
inference(sor,[status(thm)],[177,535]),
[iquote('0:SoR:177.1,535.0')] ).
cnf(539,plain,
( one(out1(and2(h2(f2(a)))))
| one(in2(or1(f2(a)))) ),
inference(ssi,[status(thm)],[537,65,2,12]),
[iquote('0:SSi:537.0,65.0,2.1,12.1')] ).
cnf(540,plain,
one(in2(or1(f2(a)))),
inference(spt,[spt(split,[position(s1)])],[539]),
[iquote('1:Spt:539.1')] ).
cnf(546,plain,
( ~ fulladder(f2(a))
| one(outc(h1(f2(a)))) ),
inference(sor,[status(thm)],[230,540]),
[iquote('1:SoR:230.1,540.0')] ).
cnf(547,plain,
one(outc(h1(f2(a)))),
inference(ssi,[status(thm)],[546,2,12]),
[iquote('1:SSi:546.0,2.0,12.1')] ).
cnf(549,plain,
( ~ halfadder(h1(f2(a)))
| one(out1(and2(h1(f2(a))))) ),
inference(sor,[status(thm)],[177,547]),
[iquote('1:SoR:177.1,547.0')] ).
cnf(551,plain,
one(out1(and2(h1(f2(a))))),
inference(ssi,[status(thm)],[549,64,2,12]),
[iquote('1:SSi:549.0,64.0,2.1,12.1')] ).
cnf(553,plain,
( ~ and_ok(and2(h1(f2(a))))
| ~ zero(in1(and2(h1(f2(a))))) ),
inference(ems,[status(thm)],[28,551,29]),
[iquote('1:EmS:28.0,28.1,551.0,29.2')] ).
cnf(564,plain,
~ zero(in1(and2(h1(f2(a))))),
inference(ssi,[status(thm)],[553,279,52,64,2,12]),
[iquote('1:SSi:553.0,279.0,52.1,64.1,2.1,12.0')] ).
cnf(565,plain,
$false,
inference(mrr,[status(thm)],[564,430]),
[iquote('1:MRR:564.0,430.0')] ).
cnf(566,plain,
~ one(in2(or1(f2(a)))),
inference(spt,[spt(split,[position(sa)])],[565,540]),
[iquote('1:Spt:565.0,539.1,540.0')] ).
cnf(567,plain,
one(out1(and2(h2(f2(a))))),
inference(spt,[spt(split,[position(s2)])],[539]),
[iquote('1:Spt:565.0,539.0')] ).
cnf(571,plain,
( ~ and_ok(and2(h2(f2(a))))
| ~ zero(in1(and2(h2(f2(a))))) ),
inference(ems,[status(thm)],[28,567,29]),
[iquote('1:EmS:28.0,28.1,567.0,29.2')] ).
cnf(582,plain,
~ zero(in1(and2(h2(f2(a))))),
inference(ssi,[status(thm)],[571,287,52,65,2,12]),
[iquote('1:SSi:571.0,287.0,52.1,65.1,2.1,12.0')] ).
cnf(583,plain,
$false,
inference(mrr,[status(thm)],[582,428]),
[iquote('1:MRR:582.0,428.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : HWV008-2.002 : TPTP v8.1.0. Bugfixed v2.7.0.
% 0.07/0.13 % Command : run_spass %d %s
% 0.13/0.34 % Computer : n006.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 600
% 0.13/0.34 % DateTime : Fri Jun 17 01:39:56 EDT 2022
% 0.13/0.34 % CPUTime :
% 0.19/0.48
% 0.19/0.48 SPASS V 3.9
% 0.19/0.48 SPASS beiseite: Proof found.
% 0.19/0.48 % SZS status Theorem
% 0.19/0.48 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.48 SPASS derived 408 clauses, backtracked 4 clauses, performed 1 splits and kept 246 clauses.
% 0.19/0.48 SPASS allocated 76153 KBytes.
% 0.19/0.48 SPASS spent 0:00:00.12 on the problem.
% 0.19/0.48 0:00:00.04 for the input.
% 0.19/0.48 0:00:00.00 for the FLOTTER CNF translation.
% 0.19/0.48 0:00:00.01 for inferences.
% 0.19/0.48 0:00:00.00 for the backtracking.
% 0.19/0.48 0:00:00.04 for the reduction.
% 0.19/0.48
% 0.19/0.48
% 0.19/0.48 Here is a proof with depth 10, length 84 :
% 0.19/0.48 % SZS output start Refutation
% See solution above
% 0.19/0.48 Formulae used in the proof : nbit_adder_fulladder2 nbit_adder_connection_outc_outcf1 nbit_adder_connection_ina2_in1f2 nbit_adder_connection_inb2_in2f2 a_isa_2bit_adder ina2_0 inb2_0 outc_1 diagnosis_or1f2a diagnosis_and2h1f2a diagnosis_and2h2f2a 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.48
%------------------------------------------------------------------------------