%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : HWV008-1.001 : TPTP v8.1.0. Released v2.1.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n021.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 1.00s 1.21s
% Output : Refutation 1.06s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 29
% Syntax : Number of clauses : 90 ( 19 unt; 5 nHn; 90 RR)
% Number of literals : 199 ( 0 equ; 117 neg)
% Maximal clause size : 5 ( 2 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 6 ( 5 usr; 1 prp; 0-2 aty)
% Number of functors : 24 ( 24 usr; 16 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
( ~ type(u,nbit_adder(n1))
| type(v__dfg(n1,u),fulladder) ),
file('HWV008-1.001.p',unknown),
[] ).
cnf(3,axiom,
( ~ type(u,nbit_adder(n1))
| connection(out(c,u),out(c,v__dfg(n1,u))) ),
file('HWV008-1.001.p',unknown),
[] ).
cnf(4,axiom,
( ~ type(u,nbit_adder(n1))
| connection(in(a1,u),in(n1,v__dfg(n1,u))) ),
file('HWV008-1.001.p',unknown),
[] ).
cnf(5,axiom,
( ~ type(u,nbit_adder(n1))
| connection(in(b1,u),in(n2,v__dfg(n1,u))) ),
file('HWV008-1.001.p',unknown),
[] ).
cnf(7,axiom,
type(a,nbit_adder(n1)),
file('HWV008-1.001.p',unknown),
[] ).
cnf(8,axiom,
value(in(a1,a),n0),
file('HWV008-1.001.p',unknown),
[] ).
cnf(9,axiom,
value(in(b1,a),n0),
file('HWV008-1.001.p',unknown),
[] ).
cnf(12,axiom,
value(out(c,a),n1),
file('HWV008-1.001.p',unknown),
[] ).
cnf(13,axiom,
~ mode(or1(v__dfg(n1,a)),abnormal),
file('HWV008-1.001.p',unknown),
[] ).
cnf(14,axiom,
~ mode(and2(h1(v__dfg(n1,a))),abnormal),
file('HWV008-1.001.p',unknown),
[] ).
cnf(15,axiom,
~ mode(and2(h2(v__dfg(n1,a))),abnormal),
file('HWV008-1.001.p',unknown),
[] ).
cnf(16,axiom,
( ~ value(u,v)
| ~ connection(u,w)
| value(w,v) ),
file('HWV008-1.001.p',unknown),
[] ).
cnf(17,axiom,
( ~ value(u,v)
| ~ connection(w,u)
| value(w,v) ),
file('HWV008-1.001.p',unknown),
[] ).
cnf(18,axiom,
( ~ value(u,v)
| ~ value(u,w)
| equal_value(w,v) ),
file('HWV008-1.001.p',unknown),
[] ).
cnf(19,axiom,
~ equal_value(n0,n1),
file('HWV008-1.001.p',unknown),
[] ).
cnf(22,axiom,
( ~ type(u,v)
| mode(u,abnormal)
| mode(u,ok) ),
file('HWV008-1.001.p',unknown),
[] ).
cnf(23,axiom,
( ~ type(u,and__dfg)
| ~ mode(u,ok)
| ~ value(in(v,u),n0)
| value(out(n1,u),n0) ),
file('HWV008-1.001.p',unknown),
[] ).
cnf(30,axiom,
( ~ type(u,or__dfg)
| ~ mode(u,ok)
| ~ value(out(n1,u),n1)
| value(in(n1,u),n1)
| value(in(n2,u),n1) ),
file('HWV008-1.001.p',unknown),
[] ).
cnf(38,axiom,
( ~ type(u,halfadder)
| type(and2(u),and__dfg) ),
file('HWV008-1.001.p',unknown),
[] ).
cnf(43,axiom,
( ~ type(u,halfadder)
| connection(in(n1,u),in(n1,and2(u))) ),
file('HWV008-1.001.p',unknown),
[] ).
cnf(46,axiom,
( ~ type(u,halfadder)
| connection(out(c,u),out(n1,and2(u))) ),
file('HWV008-1.001.p',unknown),
[] ).
cnf(50,axiom,
( ~ type(u,fulladder)
| type(h1(u),halfadder) ),
file('HWV008-1.001.p',unknown),
[] ).
cnf(51,axiom,
( ~ type(u,fulladder)
| type(h2(u),halfadder) ),
file('HWV008-1.001.p',unknown),
[] ).
cnf(52,axiom,
( ~ type(u,fulladder)
| type(or1(u),or__dfg) ),
file('HWV008-1.001.p',unknown),
[] ).
cnf(54,axiom,
( ~ type(u,fulladder)
| connection(out(c,h1(u)),in(n2,or1(u))) ),
file('HWV008-1.001.p',unknown),
[] ).
cnf(55,axiom,
( ~ type(u,fulladder)
| connection(out(c,h2(u)),in(n1,or1(u))) ),
file('HWV008-1.001.p',unknown),
[] ).
cnf(56,axiom,
( ~ type(u,fulladder)
| connection(in(n1,u),in(n1,h2(u))) ),
file('HWV008-1.001.p',unknown),
[] ).
cnf(57,axiom,
( ~ type(u,fulladder)
| connection(in(n2,u),in(n1,h1(u))) ),
file('HWV008-1.001.p',unknown),
[] ).
cnf(60,axiom,
( ~ type(u,fulladder)
| connection(out(c,u),out(n1,or1(u))) ),
file('HWV008-1.001.p',unknown),
[] ).
cnf(62,plain,
( ~ type(and2(h2(v__dfg(n1,a))),u)
| mode(and2(h2(v__dfg(n1,a))),ok) ),
inference(res,[status(thm),theory(equality)],[22,15]),
[iquote('0:Res:22.2,15.0')] ).
cnf(63,plain,
( ~ type(and2(h1(v__dfg(n1,a))),u)
| mode(and2(h1(v__dfg(n1,a))),ok) ),
inference(res,[status(thm),theory(equality)],[22,14]),
[iquote('0:Res:22.2,14.0')] ).
cnf(66,plain,
( ~ type(u,fulladder)
| mode(or1(u),abnormal)
| mode(or1(u),ok) ),
inference(res,[status(thm),theory(equality)],[52,22]),
[iquote('0:Res:52.1,22.0')] ).
cnf(87,plain,
( ~ connection(out(c,a),u)
| value(u,n1) ),
inference(res,[status(thm),theory(equality)],[12,16]),
[iquote('0:Res:12.0,16.0')] ).
cnf(90,plain,
( ~ connection(in(b1,a),u)
| value(u,n0) ),
inference(res,[status(thm),theory(equality)],[9,16]),
[iquote('0:Res:9.0,16.0')] ).
cnf(91,plain,
( ~ connection(in(a1,a),u)
| value(u,n0) ),
inference(res,[status(thm),theory(equality)],[8,16]),
[iquote('0:Res:8.0,16.0')] ).
cnf(108,plain,
( ~ type(v__dfg(n1,a),fulladder)
| mode(or1(v__dfg(n1,a)),ok) ),
inference(res,[status(thm),theory(equality)],[66,13]),
[iquote('0:Res:66.1,13.0')] ).
cnf(119,plain,
( ~ type(a,nbit_adder(n1))
| value(in(n2,v__dfg(n1,a)),n0) ),
inference(res,[status(thm),theory(equality)],[5,90]),
[iquote('0:Res:5.1,90.0')] ).
cnf(120,plain,
value(in(n2,v__dfg(n1,a)),n0),
inference(mrr,[status(thm)],[119,7]),
[iquote('0:MRR:119.0,7.0')] ).
cnf(121,plain,
( ~ connection(in(n2,v__dfg(n1,a)),u)
| value(u,n0) ),
inference(res,[status(thm),theory(equality)],[120,16]),
[iquote('0:Res:120.0,16.0')] ).
cnf(124,plain,
( ~ type(v__dfg(n1,a),fulladder)
| value(in(n1,h1(v__dfg(n1,a))),n0) ),
inference(res,[status(thm),theory(equality)],[57,121]),
[iquote('0:Res:57.1,121.0')] ).
cnf(129,plain,
( ~ type(a,nbit_adder(n1))
| value(in(n1,v__dfg(n1,a)),n0) ),
inference(res,[status(thm),theory(equality)],[4,91]),
[iquote('0:Res:4.1,91.0')] ).
cnf(130,plain,
value(in(n1,v__dfg(n1,a)),n0),
inference(mrr,[status(thm)],[129,7]),
[iquote('0:MRR:129.0,7.0')] ).
cnf(131,plain,
( ~ connection(in(n1,v__dfg(n1,a)),u)
| value(u,n0) ),
inference(res,[status(thm),theory(equality)],[130,16]),
[iquote('0:Res:130.0,16.0')] ).
cnf(134,plain,
( ~ type(v__dfg(n1,a),fulladder)
| value(in(n1,h2(v__dfg(n1,a))),n0) ),
inference(res,[status(thm),theory(equality)],[56,131]),
[iquote('0:Res:56.1,131.0')] ).
cnf(157,plain,
( ~ type(a,nbit_adder(n1))
| value(out(c,v__dfg(n1,a)),n1) ),
inference(res,[status(thm),theory(equality)],[3,87]),
[iquote('0:Res:3.1,87.0')] ).
cnf(158,plain,
value(out(c,v__dfg(n1,a)),n1),
inference(mrr,[status(thm)],[157,7]),
[iquote('0:MRR:157.0,7.0')] ).
cnf(159,plain,
( ~ connection(out(c,v__dfg(n1,a)),u)
| value(u,n1) ),
inference(res,[status(thm),theory(equality)],[158,16]),
[iquote('0:Res:158.0,16.0')] ).
cnf(162,plain,
( ~ type(v__dfg(n1,a),fulladder)
| value(out(n1,or1(v__dfg(n1,a))),n1) ),
inference(res,[status(thm),theory(equality)],[60,159]),
[iquote('0:Res:60.1,159.0')] ).
cnf(171,plain,
( ~ type(v__dfg(n1,a),fulladder)
| ~ connection(in(n1,h1(v__dfg(n1,a))),u)
| value(u,n0) ),
inference(res,[status(thm),theory(equality)],[124,16]),
[iquote('0:Res:124.1,16.0')] ).
cnf(184,plain,
( ~ type(v__dfg(n1,a),fulladder)
| ~ connection(in(n1,h2(v__dfg(n1,a))),u)
| value(u,n0) ),
inference(res,[status(thm),theory(equality)],[134,16]),
[iquote('0:Res:134.1,16.0')] ).
cnf(361,plain,
( ~ type(v__dfg(n1,a),fulladder)
| ~ type(or1(v__dfg(n1,a)),or__dfg)
| ~ mode(or1(v__dfg(n1,a)),ok)
| value(in(n1,or1(v__dfg(n1,a))),n1)
| value(in(n2,or1(v__dfg(n1,a))),n1) ),
inference(res,[status(thm),theory(equality)],[162,30]),
[iquote('0:Res:162.1,30.2')] ).
cnf(367,plain,
( ~ type(v__dfg(n1,a),fulladder)
| value(in(n1,or1(v__dfg(n1,a))),n1)
| value(in(n2,or1(v__dfg(n1,a))),n1) ),
inference(mrr,[status(thm)],[361,52,108]),
[iquote('0:MRR:361.1,361.2,52.1,108.1')] ).
cnf(836,plain,
( ~ type(h1(v__dfg(n1,a)),halfadder)
| ~ type(v__dfg(n1,a),fulladder)
| value(in(n1,and2(h1(v__dfg(n1,a)))),n0) ),
inference(res,[status(thm),theory(equality)],[43,171]),
[iquote('0:Res:43.1,171.1')] ).
cnf(839,plain,
( ~ type(v__dfg(n1,a),fulladder)
| value(in(n1,and2(h1(v__dfg(n1,a)))),n0) ),
inference(mrr,[status(thm)],[836,50]),
[iquote('0:MRR:836.0,50.1')] ).
cnf(850,plain,
( ~ type(v__dfg(n1,a),fulladder)
| ~ type(and2(h1(v__dfg(n1,a))),and__dfg)
| ~ mode(and2(h1(v__dfg(n1,a))),ok)
| value(out(n1,and2(h1(v__dfg(n1,a)))),n0) ),
inference(res,[status(thm),theory(equality)],[839,23]),
[iquote('0:Res:839.1,23.2')] ).
cnf(854,plain,
( ~ type(v__dfg(n1,a),fulladder)
| ~ type(and2(h1(v__dfg(n1,a))),and__dfg)
| value(out(n1,and2(h1(v__dfg(n1,a)))),n0) ),
inference(mrr,[status(thm)],[850,63]),
[iquote('0:MRR:850.2,63.1')] ).
cnf(937,plain,
( ~ type(h2(v__dfg(n1,a)),halfadder)
| ~ type(v__dfg(n1,a),fulladder)
| value(in(n1,and2(h2(v__dfg(n1,a)))),n0) ),
inference(res,[status(thm),theory(equality)],[43,184]),
[iquote('0:Res:43.1,184.1')] ).
cnf(940,plain,
( ~ type(v__dfg(n1,a),fulladder)
| value(in(n1,and2(h2(v__dfg(n1,a)))),n0) ),
inference(mrr,[status(thm)],[937,51]),
[iquote('0:MRR:937.0,51.1')] ).
cnf(951,plain,
( ~ type(v__dfg(n1,a),fulladder)
| ~ type(and2(h2(v__dfg(n1,a))),and__dfg)
| ~ mode(and2(h2(v__dfg(n1,a))),ok)
| value(out(n1,and2(h2(v__dfg(n1,a)))),n0) ),
inference(res,[status(thm),theory(equality)],[940,23]),
[iquote('0:Res:940.1,23.2')] ).
cnf(955,plain,
( ~ type(v__dfg(n1,a),fulladder)
| ~ type(and2(h2(v__dfg(n1,a))),and__dfg)
| value(out(n1,and2(h2(v__dfg(n1,a)))),n0) ),
inference(mrr,[status(thm)],[951,62]),
[iquote('0:MRR:951.2,62.1')] ).
cnf(2347,plain,
value(in(n2,or1(v__dfg(n1,a))),n1),
inference(spt,[spt(split,[position(s1)])],[367]),
[iquote('1:Spt:367.2')] ).
cnf(2350,plain,
( ~ connection(u,in(n2,or1(v__dfg(n1,a))))
| value(u,n1) ),
inference(res,[status(thm),theory(equality)],[2347,17]),
[iquote('1:Res:2347.0,17.0')] ).
cnf(2356,plain,
( ~ type(v__dfg(n1,a),fulladder)
| value(out(c,h1(v__dfg(n1,a))),n1) ),
inference(res,[status(thm),theory(equality)],[54,2350]),
[iquote('1:Res:54.1,2350.0')] ).
cnf(2359,plain,
( ~ type(v__dfg(n1,a),fulladder)
| ~ connection(out(c,h1(v__dfg(n1,a))),u)
| value(u,n1) ),
inference(res,[status(thm),theory(equality)],[2356,16]),
[iquote('1:Res:2356.1,16.0')] ).
cnf(2408,plain,
( ~ type(h1(v__dfg(n1,a)),halfadder)
| ~ type(v__dfg(n1,a),fulladder)
| value(out(n1,and2(h1(v__dfg(n1,a)))),n1) ),
inference(res,[status(thm),theory(equality)],[46,2359]),
[iquote('1:Res:46.1,2359.1')] ).
cnf(2412,plain,
( ~ type(v__dfg(n1,a),fulladder)
| value(out(n1,and2(h1(v__dfg(n1,a)))),n1) ),
inference(mrr,[status(thm)],[2408,50]),
[iquote('1:MRR:2408.0,50.1')] ).
cnf(2423,plain,
( ~ type(v__dfg(n1,a),fulladder)
| ~ value(out(n1,and2(h1(v__dfg(n1,a)))),u)
| equal_value(u,n1) ),
inference(res,[status(thm),theory(equality)],[2412,18]),
[iquote('1:Res:2412.1,18.0')] ).
cnf(3326,plain,
( ~ type(v__dfg(n1,a),fulladder)
| ~ type(and2(h1(v__dfg(n1,a))),and__dfg)
| ~ type(v__dfg(n1,a),fulladder)
| equal_value(n0,n1) ),
inference(res,[status(thm),theory(equality)],[854,2423]),
[iquote('1:Res:854.2,2423.1')] ).
cnf(3334,plain,
( ~ type(and2(h1(v__dfg(n1,a))),and__dfg)
| ~ type(v__dfg(n1,a),fulladder)
| equal_value(n0,n1) ),
inference(obv,[status(thm),theory(equality)],[3326]),
[iquote('1:Obv:3326.0')] ).
cnf(3335,plain,
( ~ type(and2(h1(v__dfg(n1,a))),and__dfg)
| ~ type(v__dfg(n1,a),fulladder) ),
inference(mrr,[status(thm)],[3334,19]),
[iquote('1:MRR:3334.2,19.0')] ).
cnf(3341,plain,
( ~ type(h1(v__dfg(n1,a)),halfadder)
| ~ type(v__dfg(n1,a),fulladder) ),
inference(res,[status(thm),theory(equality)],[38,3335]),
[iquote('1:Res:38.1,3335.0')] ).
cnf(3342,plain,
~ type(v__dfg(n1,a),fulladder),
inference(mrr,[status(thm)],[3341,50]),
[iquote('1:MRR:3341.0,50.1')] ).
cnf(3343,plain,
~ type(a,nbit_adder(n1)),
inference(res,[status(thm),theory(equality)],[1,3342]),
[iquote('1:Res:1.1,3342.0')] ).
cnf(3344,plain,
$false,
inference(mrr,[status(thm)],[3343,7]),
[iquote('1:MRR:3343.0,7.0')] ).
cnf(3345,plain,
~ value(in(n2,or1(v__dfg(n1,a))),n1),
inference(spt,[spt(split,[position(sa)])],[3344,2347]),
[iquote('1:Spt:3344.0,367.2,2347.0')] ).
cnf(3346,plain,
( ~ type(v__dfg(n1,a),fulladder)
| value(in(n1,or1(v__dfg(n1,a))),n1) ),
inference(spt,[spt(split,[position(s2)])],[367]),
[iquote('1:Spt:3344.0,367.0,367.1')] ).
cnf(3360,plain,
( ~ type(v__dfg(n1,a),fulladder)
| ~ connection(u,in(n1,or1(v__dfg(n1,a))))
| value(u,n1) ),
inference(res,[status(thm),theory(equality)],[3346,17]),
[iquote('1:Res:3346.1,17.0')] ).
cnf(3499,plain,
( ~ type(v__dfg(n1,a),fulladder)
| ~ type(v__dfg(n1,a),fulladder)
| value(out(c,h2(v__dfg(n1,a))),n1) ),
inference(res,[status(thm),theory(equality)],[55,3360]),
[iquote('1:Res:55.1,3360.1')] ).
cnf(3501,plain,
( ~ type(v__dfg(n1,a),fulladder)
| value(out(c,h2(v__dfg(n1,a))),n1) ),
inference(obv,[status(thm),theory(equality)],[3499]),
[iquote('1:Obv:3499.0')] ).
cnf(3502,plain,
( ~ type(v__dfg(n1,a),fulladder)
| ~ connection(out(c,h2(v__dfg(n1,a))),u)
| value(u,n1) ),
inference(res,[status(thm),theory(equality)],[3501,16]),
[iquote('1:Res:3501.1,16.0')] ).
cnf(3508,plain,
( ~ type(h2(v__dfg(n1,a)),halfadder)
| ~ type(v__dfg(n1,a),fulladder)
| value(out(n1,and2(h2(v__dfg(n1,a)))),n1) ),
inference(res,[status(thm),theory(equality)],[46,3502]),
[iquote('1:Res:46.1,3502.1')] ).
cnf(3512,plain,
( ~ type(v__dfg(n1,a),fulladder)
| value(out(n1,and2(h2(v__dfg(n1,a)))),n1) ),
inference(mrr,[status(thm)],[3508,51]),
[iquote('1:MRR:3508.0,51.1')] ).
cnf(3523,plain,
( ~ type(v__dfg(n1,a),fulladder)
| ~ value(out(n1,and2(h2(v__dfg(n1,a)))),u)
| equal_value(u,n1) ),
inference(res,[status(thm),theory(equality)],[3512,18]),
[iquote('1:Res:3512.1,18.0')] ).
cnf(3877,plain,
( ~ type(v__dfg(n1,a),fulladder)
| ~ type(and2(h2(v__dfg(n1,a))),and__dfg)
| ~ type(v__dfg(n1,a),fulladder)
| equal_value(n0,n1) ),
inference(res,[status(thm),theory(equality)],[955,3523]),
[iquote('1:Res:955.2,3523.1')] ).
cnf(3885,plain,
( ~ type(and2(h2(v__dfg(n1,a))),and__dfg)
| ~ type(v__dfg(n1,a),fulladder)
| equal_value(n0,n1) ),
inference(obv,[status(thm),theory(equality)],[3877]),
[iquote('1:Obv:3877.0')] ).
cnf(3886,plain,
( ~ type(and2(h2(v__dfg(n1,a))),and__dfg)
| ~ type(v__dfg(n1,a),fulladder) ),
inference(mrr,[status(thm)],[3885,19]),
[iquote('1:MRR:3885.2,19.0')] ).
cnf(3889,plain,
( ~ type(h2(v__dfg(n1,a)),halfadder)
| ~ type(v__dfg(n1,a),fulladder) ),
inference(res,[status(thm),theory(equality)],[38,3886]),
[iquote('1:Res:38.1,3886.0')] ).
cnf(3890,plain,
~ type(v__dfg(n1,a),fulladder),
inference(mrr,[status(thm)],[3889,51]),
[iquote('1:MRR:3889.0,51.1')] ).
cnf(3891,plain,
~ type(a,nbit_adder(n1)),
inference(res,[status(thm),theory(equality)],[1,3890]),
[iquote('1:Res:1.1,3890.0')] ).
cnf(3892,plain,
$false,
inference(mrr,[status(thm)],[3891,7]),
[iquote('1:MRR:3891.0,7.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : HWV008-1.001 : TPTP v8.1.0. Released v2.1.0.
% 0.03/0.14 % Command : run_spass %d %s
% 0.13/0.35 % Computer : n021.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 600
% 0.13/0.35 % DateTime : Fri Jun 17 03:07:00 EDT 2022
% 0.13/0.35 % CPUTime :
% 1.00/1.21
% 1.00/1.21 SPASS V 3.9
% 1.00/1.21 SPASS beiseite: Proof found.
% 1.00/1.21 % SZS status Theorem
% 1.00/1.21 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.00/1.21 SPASS derived 3000 clauses, backtracked 197 clauses, performed 3 splits and kept 2259 clauses.
% 1.00/1.21 SPASS allocated 67592 KBytes.
% 1.00/1.21 SPASS spent 0:00:00.85 on the problem.
% 1.00/1.21 0:00:00.04 for the input.
% 1.00/1.21 0:00:00.00 for the FLOTTER CNF translation.
% 1.00/1.21 0:00:00.07 for inferences.
% 1.00/1.21 0:00:00.03 for the backtracking.
% 1.00/1.21 0:00:00.63 for the reduction.
% 1.00/1.21
% 1.00/1.21
% 1.00/1.21 Here is a proof with depth 14, length 90 :
% 1.00/1.21 % SZS output start Refutation
% See solution above
% 1.06/1.23 Formulae used in the proof : nbit_adder_fulladder1 nbit_adder_connection_outc_outcv1 nbit_adder_connection_ina1_in1v1 nbit_adder_connection_inb1_in2v1 a_isa_1bit_adder ina1_0 inb1_0 outc_0 diagnosis_or1v1 diagnosis_and2h1v1 diagnosis_and2h2v1 value_propagation1 value_propagation2 unique_value equal_value1 ok_or_abnormal and_0x_0 or_1_11 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
% 1.06/1.23
%------------------------------------------------------------------------------