%------------------------------------------------------------------------------
% File : Geo-III---2018C
% Problem : HWV008-2.002 : TPTP v8.1.0. Bugfixed v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : geo -tptp_input -nonempty -inputfile %s
% Computer : n022.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 : 300s
% DateTime : Sat Jul 23 06:04:48 EDT 2022
% Result : Unsatisfiable 20.35s 20.53s
% Output : Refutation 20.35s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : HWV008-2.002 : TPTP v8.1.0. Bugfixed v2.7.0.
% 0.07/0.12 % Command : geo -tptp_input -nonempty -inputfile %s
% 0.12/0.33 % Computer : n022.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Fri Jul 22 17:14:51 EDT 2022
% 0.12/0.33 % CPUTime :
% 20.35/20.53 GeoParameters:
% 20.35/20.53
% 20.35/20.53 tptp_input = 1
% 20.35/20.53 tptp_output = 0
% 20.35/20.53 nonempty = 1
% 20.35/20.53 inputfile = /export/starexec/sandbox/benchmark/theBenchmark.p
% 20.35/20.53 includepath = /export/starexec/sandbox/solver/bin/../../benchmark/
% 20.35/20.53
% 20.35/20.53
% 20.35/20.53 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 20.35/20.53 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 20.35/20.53
% 20.35/20.53 RuleSystem INPUT:
% 20.35/20.53
% 20.35/20.53 Initial Rules:
% 20.35/20.53 #0: input, references = 82, size of lhs = 2:
% 20.35/20.53 connection-{F}(V1,V0), zero-{F}(V1) | zero-{T}(V0)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #1: input, references = 28, size of lhs = 2:
% 20.35/20.53 connection-{F}(V1,V0), one-{F}(V1) | one-{T}(V0)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2: input, references = 45, size of lhs = 2:
% 20.35/20.53 zero-{F}(V0), connection-{F}(V1,V0) | zero-{T}(V1)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #3: input, references = 13, size of lhs = 2:
% 20.35/20.53 one-{F}(V0), connection-{F}(V1,V0) | one-{T}(V1)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #4: input, references = 33, size of lhs = 2:
% 20.35/20.53 zero-{F}(V0), one-{F}(V0) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #5: input, references = 18, size of lhs = 4:
% 20.35/20.53 P_in1-{F}(V0,V1), P_out1-{F}(V0,V2), and_ok-{F}(V0), zero-{F}(V1) | zero-{T}(V2)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #6: input, references = 3, size of lhs = 4:
% 20.35/20.53 P_in2-{F}(V0,V1), P_out1-{F}(V0,V2), and_ok-{F}(V0), zero-{F}(V1) | zero-{T}(V2)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #7: input, references = 3, size of lhs = 6:
% 20.35/20.53 P_in1-{F}(V0,V1), P_in2-{F}(V0,V2), P_out1-{F}(V0,V3), and_ok-{F}(V0), one-{F}(V1), one-{F}(V2) | one-{T}(V3)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #8: input, references = 3, size of lhs = 5:
% 20.35/20.53 P_out1-{F}(V0,V1), P_in1-{F}(V0,V2), P_in2-{F}(V0,V3), and_ok-{F}(V0), zero-{F}(V1) | zero-{T}(V2), zero-{T}(V3)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #9: input, references = 3, size of lhs = 4:
% 20.35/20.53 P_out1-{F}(V0,V1), P_in1-{F}(V0,V2), and_ok-{F}(V0), one-{F}(V1) | one-{T}(V2)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #10: input, references = 6, size of lhs = 4:
% 20.35/20.53 P_out1-{F}(V0,V1), P_in2-{F}(V0,V2), and_ok-{F}(V0), one-{F}(V1) | one-{T}(V2)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #11: input, references = 3, size of lhs = 2:
% 20.35/20.53 and_ok-{F}(V0), abnormal-{F}(V0) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #12: input, references = 6, size of lhs = 1:
% 20.35/20.53 logic_and-{F}(V0) | and_ok-{T}(V0), abnormal-{T}(V0)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #13: input, references = 5, size of lhs = 4:
% 20.35/20.53 P_in1-{F}(V0,V1), P_out1-{F}(V0,V2), or_ok-{F}(V0), one-{F}(V1) | one-{T}(V2)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #14: input, references = 3, size of lhs = 4:
% 20.35/20.53 P_in2-{F}(V0,V1), P_out1-{F}(V0,V2), or_ok-{F}(V0), one-{F}(V1) | one-{T}(V2)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #15: input, references = 12, size of lhs = 6:
% 20.35/20.53 P_in1-{F}(V0,V1), P_in2-{F}(V0,V2), P_out1-{F}(V0,V3), or_ok-{F}(V0), zero-{F}(V1), zero-{F}(V2) | zero-{T}(V3)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #16: input, references = 3, size of lhs = 5:
% 20.35/20.53 P_out1-{F}(V0,V1), P_in1-{F}(V0,V2), P_in2-{F}(V0,V3), or_ok-{F}(V0), one-{F}(V1) | one-{T}(V2), one-{T}(V3)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #17: input, references = 3, size of lhs = 4:
% 20.35/20.53 P_out1-{F}(V0,V1), P_in1-{F}(V0,V2), or_ok-{F}(V0), zero-{F}(V1) | zero-{T}(V2)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #18: input, references = 3, size of lhs = 4:
% 20.35/20.53 P_out1-{F}(V0,V1), P_in2-{F}(V0,V2), or_ok-{F}(V0), zero-{F}(V1) | zero-{T}(V2)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #19: input, references = 3, size of lhs = 2:
% 20.35/20.53 or_ok-{F}(V0), abnormal-{F}(V0) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #20: input, references = 6, size of lhs = 1:
% 20.35/20.53 logic_or-{F}(V0) | or_ok-{T}(V0), abnormal-{T}(V0)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #21: input, references = 10, size of lhs = 4:
% 20.35/20.53 P_in1-{F}(V0,V1), P_out1-{F}(V0,V2), not_ok-{F}(V0), zero-{F}(V1) | one-{T}(V2)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #22: input, references = 3, size of lhs = 4:
% 20.35/20.53 P_in1-{F}(V0,V1), P_out1-{F}(V0,V2), not_ok-{F}(V0), one-{F}(V1) | zero-{T}(V2)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #23: input, references = 3, size of lhs = 4:
% 20.35/20.53 P_out1-{F}(V0,V1), P_in1-{F}(V0,V2), not_ok-{F}(V0), zero-{F}(V1) | one-{T}(V2)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #24: input, references = 3, size of lhs = 4:
% 20.35/20.53 P_out1-{F}(V0,V1), P_in1-{F}(V0,V2), not_ok-{F}(V0), one-{F}(V1) | zero-{T}(V2)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #25: input, references = 3, size of lhs = 2:
% 20.35/20.53 not_ok-{F}(V0), abnormal-{F}(V0) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #26: input, references = 5, size of lhs = 1:
% 20.35/20.53 logic_not-{F}(V0) | not_ok-{T}(V0), abnormal-{T}(V0)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #27: input, references = 3, size of lhs = 2:
% 20.35/20.53 P_and1-{F}(V0,V1), halfadder-{F}(V0) | logic_and-{T}(V1)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #28: input, references = 9, size of lhs = 2:
% 20.35/20.53 P_and2-{F}(V0,V1), halfadder-{F}(V0) | logic_and-{T}(V1)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #29: input, references = 3, size of lhs = 2:
% 20.35/20.53 P_not1-{F}(V0,V1), halfadder-{F}(V0) | logic_not-{T}(V1)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #30: input, references = 3, size of lhs = 2:
% 20.35/20.53 P_or1-{F}(V0,V1), halfadder-{F}(V0) | logic_or-{T}(V1)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #31: input, references = 3, size of lhs = 4:
% 20.35/20.53 P_in1-{F}(V0,V1), P_or1-{F}(V0,V2), P_in1-{F}(V2,V3), halfadder-{F}(V0) | connection-{T}(V1,V3)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #32: input, references = 5, size of lhs = 4:
% 20.35/20.53 P_in2-{F}(V0,V1), P_or1-{F}(V0,V2), P_in2-{F}(V2,V3), halfadder-{F}(V0) | connection-{T}(V1,V3)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #33: input, references = 20, size of lhs = 4:
% 20.35/20.53 P_in1-{F}(V0,V1), P_and2-{F}(V0,V2), P_in1-{F}(V2,V3), halfadder-{F}(V0) | connection-{T}(V1,V3)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #34: input, references = 3, size of lhs = 4:
% 20.35/20.53 P_in2-{F}(V0,V1), P_and2-{F}(V0,V2), P_in2-{F}(V2,V3), halfadder-{F}(V0) | connection-{T}(V1,V3)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #35: input, references = 12, size of lhs = 4:
% 20.35/20.53 P_outs-{F}(V0,V1), P_and1-{F}(V0,V2), P_out1-{F}(V2,V3), halfadder-{F}(V0) | connection-{T}(V1,V3)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #36: input, references = 17, size of lhs = 4:
% 20.35/20.53 P_outc-{F}(V0,V1), P_and2-{F}(V0,V2), P_out1-{F}(V2,V3), halfadder-{F}(V0) | connection-{T}(V1,V3)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #37: input, references = 6, size of lhs = 5:
% 20.35/20.53 P_or1-{F}(V0,V1), P_out1-{F}(V1,V2), P_and1-{F}(V0,V3), P_in1-{F}(V3,V4), halfadder-{F}(V0) | connection-{T}(V2,V4)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #38: input, references = 9, size of lhs = 5:
% 20.35/20.53 P_and2-{F}(V0,V1), P_out1-{F}(V1,V2), P_not1-{F}(V0,V3), P_in1-{F}(V3,V4), halfadder-{F}(V0) | connection-{T}(V2,V4)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #39: input, references = 4, size of lhs = 5:
% 20.35/20.53 P_not1-{F}(V0,V1), P_out1-{F}(V1,V2), P_and1-{F}(V0,V3), P_in2-{F}(V3,V4), halfadder-{F}(V0) | connection-{T}(V2,V4)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #40: input, references = 4, size of lhs = 2:
% 20.35/20.53 P_h1-{F}(V0,V1), fulladder-{F}(V0) | halfadder-{T}(V1)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #41: input, references = 5, size of lhs = 2:
% 20.35/20.53 P_h2-{F}(V0,V1), fulladder-{F}(V0) | halfadder-{T}(V1)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #42: input, references = 4, size of lhs = 2:
% 20.35/20.53 P_or1-{F}(V0,V1), fulladder-{F}(V0) | logic_or-{T}(V1)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #43: input, references = 11, size of lhs = 5:
% 20.35/20.53 P_h1-{F}(V0,V1), P_outs-{F}(V1,V2), P_h2-{F}(V0,V3), P_in2-{F}(V3,V4), fulladder-{F}(V0) | connection-{T}(V2,V4)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #44: input, references = 13, size of lhs = 5:
% 20.35/20.53 P_h1-{F}(V0,V1), P_outc-{F}(V1,V2), P_or1-{F}(V0,V3), P_in2-{F}(V3,V4), fulladder-{F}(V0) | connection-{T}(V2,V4)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #45: input, references = 6, size of lhs = 5:
% 20.35/20.53 P_h2-{F}(V0,V1), P_outc-{F}(V1,V2), P_or1-{F}(V0,V3), P_in1-{F}(V3,V4), fulladder-{F}(V0) | connection-{T}(V2,V4)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #46: input, references = 10, size of lhs = 4:
% 20.35/20.53 P_in1-{F}(V0,V1), P_h2-{F}(V0,V2), P_in1-{F}(V2,V3), fulladder-{F}(V0) | connection-{T}(V1,V3)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #47: input, references = 12, size of lhs = 4:
% 20.35/20.53 P_in2-{F}(V0,V1), P_h1-{F}(V0,V2), P_in1-{F}(V2,V3), fulladder-{F}(V0) | connection-{T}(V1,V3)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #48: input, references = 15, size of lhs = 4:
% 20.35/20.53 P_inc-{F}(V0,V1), P_h1-{F}(V0,V2), P_in2-{F}(V2,V3), fulladder-{F}(V0) | connection-{T}(V1,V3)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #49: input, references = 9, size of lhs = 4:
% 20.35/20.53 P_outs-{F}(V0,V1), P_h2-{F}(V0,V2), P_outs-{F}(V2,V3), fulladder-{F}(V0) | connection-{T}(V1,V3)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #50: input, references = 17, size of lhs = 4:
% 20.35/20.53 P_outc-{F}(V0,V1), P_or1-{F}(V0,V2), P_out1-{F}(V2,V3), fulladder-{F}(V0) | connection-{T}(V1,V3)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #51: input, references = 3, size of lhs = 2:
% 20.35/20.53 P_f1-{F}(V0,V1), nbit_adder2-{F}(V0) | fulladder-{T}(V1)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #52: input, references = 4, size of lhs = 2:
% 20.35/20.53 P_f2-{F}(V0,V1), nbit_adder2-{F}(V0) | fulladder-{T}(V1)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #53: input, references = 4, size of lhs = 4:
% 20.35/20.53 P_out1-{F}(V0,V1), P_f1-{F}(V0,V2), P_out1-{F}(V2,V3), nbit_adder2-{F}(V0) | connection-{T}(V1,V3)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #54: input, references = 3, size of lhs = 4:
% 20.35/20.53 P_out2-{F}(V0,V1), P_f2-{F}(V0,V2), P_out1-{F}(V2,V3), nbit_adder2-{F}(V0) | connection-{T}(V1,V3)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #55: input, references = 5, size of lhs = 4:
% 20.35/20.53 P_outc-{F}(V0,V1), P_f2-{F}(V0,V2), P_outc-{F}(V2,V3), nbit_adder2-{F}(V0) | connection-{T}(V1,V3)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #56: input, references = 9, size of lhs = 4:
% 20.35/20.53 P_ina1-{F}(V0,V1), P_f1-{F}(V0,V2), P_in1-{F}(V2,V3), nbit_adder2-{F}(V0) | connection-{T}(V1,V3)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #57: input, references = 5, size of lhs = 4:
% 20.35/20.53 P_inb1-{F}(V0,V1), P_f1-{F}(V0,V2), P_in2-{F}(V2,V3), nbit_adder2-{F}(V0) | connection-{T}(V1,V3)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #58: input, references = 4, size of lhs = 4:
% 20.35/20.53 P_ina2-{F}(V0,V1), P_f2-{F}(V0,V2), P_in1-{F}(V2,V3), nbit_adder2-{F}(V0) | connection-{T}(V1,V3)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #59: input, references = 4, size of lhs = 4:
% 20.35/20.53 P_inb2-{F}(V0,V1), P_f2-{F}(V0,V2), P_in2-{F}(V2,V3), nbit_adder2-{F}(V0) | connection-{T}(V1,V3)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #60: input, references = 12, size of lhs = 5:
% 20.35/20.53 P_f1-{F}(V0,V1), P_outc-{F}(V1,V2), P_f2-{F}(V0,V3), P_inc-{F}(V3,V4), nbit_adder2-{F}(V0) | connection-{T}(V2,V4)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #61: input, references = 8, size of lhs = 4:
% 20.35/20.53 P_inc-{F}(V0,V1), P_f1-{F}(V0,V2), P_inc-{F}(V2,V3), nbit_adder2-{F}(V0) | connection-{T}(V1,V3)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #62: input, references = 4, size of lhs = 1:
% 20.35/20.53 P_a-{F}(V0) | nbit_adder2-{T}(V0)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #63: input, references = 6, size of lhs = 2:
% 20.35/20.53 P_a-{F}(V0), P_ina1-{F}(V0,V1) | zero-{T}(V1)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #64: input, references = 4, size of lhs = 3:
% 20.35/20.53 P_a-{F}(V0), P_ina1-{F}(V0,V1), P_ina2-{F}(V0,V2) | zero-{T}(V2)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #65: input, references = 7, size of lhs = 4:
% 20.35/20.53 P_a-{F}(V0), P_ina1-{F}(V0,V1), P_ina2-{F}(V0,V2), P_inb1-{F}(V0,V3) | zero-{T}(V3)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #66: input, references = 4, size of lhs = 5:
% 20.35/20.53 P_a-{F}(V0), P_ina1-{F}(V0,V1), P_ina2-{F}(V0,V2), P_inb1-{F}(V0,V3), P_inb2-{F}(V0,V4) | zero-{T}(V4)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #67: input, references = 6, size of lhs = 6:
% 20.35/20.53 P_a-{F}(V0), P_ina1-{F}(V0,V1), P_ina2-{F}(V0,V2), P_inb1-{F}(V0,V3), P_inb2-{F}(V0,V4), P_inc-{F}(V0,V5) | zero-{T}(V5)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #68: input, references = 6, size of lhs = 7:
% 20.35/20.53 P_a-{F}(V0), P_ina1-{F}(V0,V1), P_ina2-{F}(V0,V2), P_inb1-{F}(V0,V3), P_inb2-{F}(V0,V4), P_inc-{F}(V0,V5), P_out1-{F}(V0,V6) | zero-{T}(V6)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #69: input, references = 9, size of lhs = 8:
% 20.35/20.53 P_a-{F}(V0), P_ina1-{F}(V0,V1), P_ina2-{F}(V0,V2), P_inb1-{F}(V0,V3), P_inb2-{F}(V0,V4), P_inc-{F}(V0,V5), P_out1-{F}(V0,V6), P_out2-{F}(V0,V7) | zero-{T}(V7)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #70: input, references = 11, size of lhs = 9:
% 20.35/20.53 P_a-{F}(V0), P_ina1-{F}(V0,V1), P_ina2-{F}(V0,V2), P_inb1-{F}(V0,V3), P_inb2-{F}(V0,V4), P_inc-{F}(V0,V5), P_out1-{F}(V0,V6), P_out2-{F}(V0,V7), P_outc-{F}(V0,V8) | one-{T}(V8)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #71: input, references = 3, size of lhs = 12:
% 20.35/20.53 P_a-{F}(V0), P_ina1-{F}(V0,V1), P_ina2-{F}(V0,V2), P_inb1-{F}(V0,V3), P_inb2-{F}(V0,V4), P_inc-{F}(V0,V5), P_out1-{F}(V0,V6), P_out2-{F}(V0,V7), P_outc-{F}(V0,V8), P_f2-{F}(V0,V9), P_or1-{F}(V9,V10), abnormal-{F}(V10) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #72: input, references = 3, size of lhs = 14:
% 20.35/20.53 P_a-{F}(V0), P_ina1-{F}(V0,V1), P_ina2-{F}(V0,V2), P_inb1-{F}(V0,V3), P_inb2-{F}(V0,V4), P_inc-{F}(V0,V5), P_out1-{F}(V0,V6), P_out2-{F}(V0,V7), P_outc-{F}(V0,V8), P_f2-{F}(V0,V9), P_or1-{F}(V9,V10), P_h1-{F}(V9,V11), P_and2-{F}(V11,V12), abnormal-{F}(V12) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #73: input, references = 3, size of lhs = 16:
% 20.35/20.53 P_a-{F}(V0), P_ina1-{F}(V0,V1), P_ina2-{F}(V0,V2), P_inb1-{F}(V0,V3), P_inb2-{F}(V0,V4), P_inc-{F}(V0,V5), P_out1-{F}(V0,V6), P_out2-{F}(V0,V7), P_outc-{F}(V0,V8), P_f2-{F}(V0,V9), P_or1-{F}(V9,V10), P_h1-{F}(V9,V11), P_and2-{F}(V11,V12), P_h2-{F}(V9,V13), P_and2-{F}(V13,V14), abnormal-{F}(V14) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #74: input, references = 32, size of lhs = 1:
% 20.35/20.53 #-{F} V0 | EXISTS V1: P_in1-{T}(V0,V1)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #75: input, references = 22, size of lhs = 1:
% 20.35/20.53 #-{F} V0 | EXISTS V1: P_out1-{T}(V0,V1)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #76: input, references = 19, size of lhs = 1:
% 20.35/20.53 #-{F} V0 | EXISTS V1: P_in2-{T}(V0,V1)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #77: input, references = 3, size of lhs = 1:
% 20.35/20.53 #-{F} V0 | EXISTS V1: P_and1-{T}(V0,V1)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #78: input, references = 8, size of lhs = 1:
% 20.35/20.53 #-{F} V0 | EXISTS V1: P_and2-{T}(V0,V1)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #79: input, references = 3, size of lhs = 1:
% 20.35/20.53 #-{F} V0 | EXISTS V1: P_not1-{T}(V0,V1)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #80: input, references = 4, size of lhs = 1:
% 20.35/20.53 #-{F} V0 | EXISTS V1: P_or1-{T}(V0,V1)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #81: input, references = 9, size of lhs = 1:
% 20.35/20.53 #-{F} V0 | EXISTS V1: P_outs-{T}(V0,V1)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #82: input, references = 18, size of lhs = 1:
% 20.35/20.53 #-{F} V0 | EXISTS V1: P_outc-{T}(V0,V1)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #83: input, references = 4, size of lhs = 1:
% 20.35/20.53 #-{F} V0 | EXISTS V1: P_h1-{T}(V0,V1)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #84: input, references = 5, size of lhs = 1:
% 20.35/20.53 #-{F} V0 | EXISTS V1: P_h2-{T}(V0,V1)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #85: input, references = 11, size of lhs = 1:
% 20.35/20.53 #-{F} V0 | EXISTS V1: P_inc-{T}(V0,V1)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #86: input, references = 3, size of lhs = 1:
% 20.35/20.53 #-{F} V0 | EXISTS V1: P_f1-{T}(V0,V1)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #87: input, references = 4, size of lhs = 1:
% 20.35/20.53 #-{F} V0 | EXISTS V1: P_f2-{T}(V0,V1)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #88: input, references = 9, size of lhs = 1:
% 20.35/20.53 #-{F} V0 | EXISTS V1: P_out2-{T}(V0,V1)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #89: input, references = 11, size of lhs = 1:
% 20.35/20.53 #-{F} V0 | EXISTS V1: P_ina1-{T}(V0,V1)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #90: input, references = 11, size of lhs = 1:
% 20.35/20.53 #-{F} V0 | EXISTS V1: P_inb1-{T}(V0,V1)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #91: input, references = 13, size of lhs = 1:
% 20.35/20.53 #-{F} V0 | EXISTS V1: P_ina2-{T}(V0,V1)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #92: input, references = 11, size of lhs = 1:
% 20.35/20.53 #-{F} V0 | EXISTS V1: P_inb2-{T}(V0,V1)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #93: input, references = 4, size of lhs = 0:
% 20.35/20.53 FALSE | EXISTS V0: P_a-{T}(V0)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 number of initial rules = 94
% 20.35/20.53
% 20.35/20.53 Simplifiers:
% 20.35/20.53 #94: unsound, references = 3, size of lhs = 3:
% 20.35/20.53 nbit_adder2-{F}(V0), nbit_adder2-{F}(V1), V0 == V1 | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #95: unsound, references = 3, size of lhs = 3:
% 20.35/20.53 P_in1-{F}(V0,V1), P_in1-{F}(V0,V3), V1 == V3 | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #96: unsound, references = 3, size of lhs = 3:
% 20.35/20.53 P_out1-{F}(V0,V1), P_out1-{F}(V0,V3), V1 == V3 | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #97: unsound, references = 3, size of lhs = 3:
% 20.35/20.53 P_in2-{F}(V0,V1), P_in2-{F}(V0,V3), V1 == V3 | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #98: unsound, references = 3, size of lhs = 3:
% 20.35/20.53 P_and1-{F}(V0,V1), P_and1-{F}(V0,V3), V1 == V3 | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #99: unsound, references = 3, size of lhs = 3:
% 20.35/20.53 P_and2-{F}(V0,V1), P_and2-{F}(V0,V3), V1 == V3 | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #100: unsound, references = 3, size of lhs = 3:
% 20.35/20.53 P_not1-{F}(V0,V1), P_not1-{F}(V0,V3), V1 == V3 | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #101: unsound, references = 3, size of lhs = 3:
% 20.35/20.53 P_or1-{F}(V0,V1), P_or1-{F}(V0,V3), V1 == V3 | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #102: unsound, references = 3, size of lhs = 3:
% 20.35/20.53 P_outs-{F}(V0,V1), P_outs-{F}(V0,V3), V1 == V3 | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #103: unsound, references = 3, size of lhs = 3:
% 20.35/20.53 P_outc-{F}(V0,V1), P_outc-{F}(V0,V3), V1 == V3 | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #104: unsound, references = 3, size of lhs = 3:
% 20.35/20.53 P_h1-{F}(V0,V1), P_h1-{F}(V0,V3), V1 == V3 | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #105: unsound, references = 3, size of lhs = 3:
% 20.35/20.53 P_h2-{F}(V0,V1), P_h2-{F}(V0,V3), V1 == V3 | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #106: unsound, references = 3, size of lhs = 3:
% 20.35/20.53 P_inc-{F}(V0,V1), P_inc-{F}(V0,V3), V1 == V3 | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #107: unsound, references = 3, size of lhs = 3:
% 20.35/20.53 P_f1-{F}(V0,V1), P_f1-{F}(V0,V3), V1 == V3 | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #108: unsound, references = 3, size of lhs = 3:
% 20.35/20.53 P_f2-{F}(V0,V1), P_f2-{F}(V0,V3), V1 == V3 | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #109: unsound, references = 3, size of lhs = 3:
% 20.35/20.53 P_out2-{F}(V0,V1), P_out2-{F}(V0,V3), V1 == V3 | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #110: unsound, references = 3, size of lhs = 3:
% 20.35/20.53 P_ina1-{F}(V0,V1), P_ina1-{F}(V0,V3), V1 == V3 | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #111: unsound, references = 3, size of lhs = 3:
% 20.35/20.53 P_inb1-{F}(V0,V1), P_inb1-{F}(V0,V3), V1 == V3 | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #112: unsound, references = 3, size of lhs = 3:
% 20.35/20.53 P_ina2-{F}(V0,V1), P_ina2-{F}(V0,V3), V1 == V3 | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #113: unsound, references = 3, size of lhs = 3:
% 20.35/20.53 P_inb2-{F}(V0,V1), P_inb2-{F}(V0,V3), V1 == V3 | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #114: unsound, references = 3, size of lhs = 3:
% 20.35/20.53 P_a-{F}(V0), P_a-{F}(V1), V0 == V1 | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 number of simplifiers = 21
% 20.35/20.53
% 20.35/20.53 Learnt:
% 20.35/20.53 #117: exists( #92, #115 ), references = 1, size of lhs = 9:
% 20.35/20.53 P_a-{F}(V0), P_ina1-{F}(V0,V1), P_ina2-{F}(V0,V2), P_inb1-{F}(V0,V3), P_inc-{F}(V0,V4), P_out1-{F}(V0,V5), P_out2-{F}(V0,V6), P_outc-{F}(V0,V7), zero-{F}(V7) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #119: exists( #91, #116 ), references = 5, size of lhs = 8:
% 20.35/20.53 P_a-{F}(V0), P_ina1-{F}(V0,V1), P_inb1-{F}(V0,V2), P_inc-{F}(V0,V3), P_out1-{F}(V0,V4), P_out2-{F}(V0,V5), P_outc-{F}(V0,V6), zero-{F}(V6) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #121: exists( #90, #118 ), references = 8, size of lhs = 7:
% 20.35/20.53 P_a-{F}(V0), P_ina1-{F}(V0,V1), P_inc-{F}(V0,V2), P_out1-{F}(V0,V3), P_out2-{F}(V0,V4), P_outc-{F}(V0,V5), zero-{F}(V5) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #127: exists( #89, #125 ), references = 1, size of lhs = 8:
% 20.35/20.53 nbit_adder2-{F}(V0), P_a-{F}(V0), P_f1-{F}(V0,V1), P_in1-{F}(V1,V2), P_outc-{F}(V0,V2), P_inc-{F}(V0,V3), P_out1-{F}(V0,V4), P_out2-{F}(V0,V5) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #129: exists( #88, #126 ), references = 1, size of lhs = 7:
% 20.35/20.53 nbit_adder2-{F}(V0), P_a-{F}(V0), P_f1-{F}(V0,V1), P_in1-{F}(V1,V2), P_outc-{F}(V0,V2), P_inc-{F}(V0,V3), P_out1-{F}(V0,V4) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #144: mergings( V0 == V7, V6 == V10, V5 == V9, V2 == V8; #137 ), references = 1, size of lhs = 8:
% 20.35/20.53 P_a-{F}(V0), P_ina2-{F}(V0,V1), P_inb1-{F}(V0,V2), P_outc-{F}(V0,V3), P_out1-{F}(V0,V3), P_ina1-{F}(V0,V4), P_inc-{F}(V0,V5), P_out2-{F}(V0,V6) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #150: mergings( V0 == V7, V6 == V11, V5 == V10, V2 == V8, V4 == V9; #138 ), references = 1, size of lhs = 8:
% 20.35/20.53 P_a-{F}(V0), P_ina2-{F}(V0,V1), P_outc-{F}(V0,V2), P_out1-{F}(V0,V2), P_ina1-{F}(V0,V3), P_inb1-{F}(V0,V4), P_inc-{F}(V0,V5), P_out2-{F}(V0,V6) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #156: mergings( V6 == V11, V5 == V10, V2 == V7, V4 == V9, V3 == V8; #139 ), references = 1, size of lhs = 8:
% 20.35/20.53 P_a-{F}(V0), P_outc-{F}(V0,V1), P_out1-{F}(V0,V1), P_ina1-{F}(V0,V2), P_ina2-{F}(V0,V3), P_inb1-{F}(V0,V4), P_inc-{F}(V0,V5), P_out2-{F}(V0,V6) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #164: mergings( V0 == V6, V5 == V9, V4 == V8, V2 == V7; #157 ), references = 1, size of lhs = 7:
% 20.35/20.53 P_a-{F}(V0), P_inb1-{F}(V0,V1), P_outc-{F}(V0,V2), P_out1-{F}(V0,V2), P_ina1-{F}(V0,V3), P_inc-{F}(V0,V4), P_out2-{F}(V0,V5) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #172: mergings( V4 == V7, V3 == V6, V2 == V5; #167 ), references = 1, size of lhs = 6:
% 20.35/20.53 P_a-{F}(V0), P_outc-{F}(V0,V1), P_out1-{F}(V0,V1), P_ina1-{F}(V0,V2), P_inc-{F}(V0,V3), P_out2-{F}(V0,V4) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #179: mergings( V3 == V5, V2 == V4; #174 ), references = 1, size of lhs = 5:
% 20.35/20.53 P_a-{F}(V0), P_outc-{F}(V0,V1), P_out1-{F}(V0,V1), P_inc-{F}(V0,V2), P_out2-{F}(V0,V3) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #185: mergings( V3 == V5, V2 == V4; #180 ), references = 1, size of lhs = 4:
% 20.35/20.53 P_a-{F}(V0), P_outc-{F}(V0,V1), P_out1-{F}(V0,V1), P_inc-{F}(V0,V2) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #190: mergings( V2 == V3; #186 ), references = 1, size of lhs = 3:
% 20.35/20.53 P_a-{F}(V0), P_outc-{F}(V0,V1), P_out1-{F}(V0,V1) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #198: exists( #89, #196 ), references = 1, size of lhs = 9:
% 20.35/20.53 nbit_adder2-{F}(V0), P_a-{F}(V0), P_f1-{F}(V0,V1), P_in1-{F}(V1,V2), P_inc-{F}(V0,V3), P_out1-{F}(V0,V4), P_out2-{F}(V0,V5), P_outc-{F}(V0,V6), connection-{F}(V6,V2) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #200: exists( #88, #197 ), references = 1, size of lhs = 8:
% 20.35/20.53 nbit_adder2-{F}(V0), P_a-{F}(V0), P_f1-{F}(V0,V1), P_in1-{F}(V1,V2), P_inc-{F}(V0,V3), P_out1-{F}(V0,V4), P_outc-{F}(V0,V5), connection-{F}(V5,V2) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #237: mergings( V0 == V8, V6 == V11, V5 == V10, V7 == V12, V2 == V9; #229 ), references = 1, size of lhs = 9:
% 20.35/20.53 P_a-{F}(V0), P_ina2-{F}(V0,V1), P_inb1-{F}(V0,V2), P_ina1-{F}(V0,V3), P_inc-{F}(V0,V4), P_out1-{F}(V0,V5), P_out2-{F}(V0,V6), P_outc-{F}(V0,V7), connection-{F}(V7,V6) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #244: mergings( V0 == V8, V6 == V12, V5 == V11, V7 == V13, V2 == V9, V4 == V10; #230 ), references = 1, size of lhs = 9:
% 20.35/20.53 P_a-{F}(V0), P_ina2-{F}(V0,V1), P_ina1-{F}(V0,V2), P_inb1-{F}(V0,V3), P_inc-{F}(V0,V4), P_out1-{F}(V0,V5), P_out2-{F}(V0,V6), P_outc-{F}(V0,V7), connection-{F}(V7,V6) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #251: mergings( V6 == V12, V5 == V11, V7 == V13, V2 == V8, V4 == V10, V3 == V9; #231 ), references = 1, size of lhs = 9:
% 20.35/20.53 P_a-{F}(V0), P_ina1-{F}(V0,V1), P_ina2-{F}(V0,V2), P_inb1-{F}(V0,V3), P_inc-{F}(V0,V4), P_out1-{F}(V0,V5), P_out2-{F}(V0,V6), P_outc-{F}(V0,V7), connection-{F}(V7,V6) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #260: mergings( V0 == V7, V5 == V10, V4 == V9, V6 == V11, V2 == V8; #252 ), references = 1, size of lhs = 8:
% 20.35/20.53 P_a-{F}(V0), P_inb1-{F}(V0,V1), P_ina1-{F}(V0,V2), P_inc-{F}(V0,V3), P_out1-{F}(V0,V4), P_out2-{F}(V0,V5), P_outc-{F}(V0,V6), connection-{F}(V6,V5) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #266: mergings( V5 == V10, V4 == V9, V6 == V11, V2 == V7, V3 == V8; #254 ), references = 1, size of lhs = 8:
% 20.35/20.53 P_a-{F}(V0), P_ina1-{F}(V0,V1), P_inb1-{F}(V0,V2), P_inc-{F}(V0,V3), P_out1-{F}(V0,V4), P_out2-{F}(V0,V5), P_outc-{F}(V0,V6), connection-{F}(V6,V5) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #273: mergings( V0 == V7, V5 == V11, V4 == V10, V6 == V12, V2 == V8, V3 == V9; #253 ), references = 1, size of lhs = 8:
% 20.35/20.53 P_a-{F}(V0), P_ina1-{F}(V0,V1), P_inb1-{F}(V0,V2), P_inc-{F}(V0,V3), P_out1-{F}(V0,V4), P_out2-{F}(V0,V5), P_outc-{F}(V0,V6), connection-{F}(V6,V5) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #281: mergings( V4 == V8, V3 == V7, V5 == V9, V2 == V6; #275 ), references = 1, size of lhs = 7:
% 20.35/20.53 P_a-{F}(V0), P_ina1-{F}(V0,V1), P_inc-{F}(V0,V2), P_out1-{F}(V0,V3), P_out2-{F}(V0,V4), P_outc-{F}(V0,V5), connection-{F}(V5,V4) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #289: mergings( V3 == V6, V2 == V5, V4 == V7; #283 ), references = 1, size of lhs = 6:
% 20.35/20.53 P_a-{F}(V0), P_inc-{F}(V0,V1), P_out1-{F}(V0,V2), P_out2-{F}(V0,V3), P_outc-{F}(V0,V4), connection-{F}(V4,V3) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #316: mergings( V0 == V8, V6 == V11, V5 == V10, V7 == V12, V2 == V9; #308 ), references = 1, size of lhs = 8:
% 20.35/20.53 P_a-{F}(V0), P_ina2-{F}(V0,V1), P_inb1-{F}(V0,V2), P_outc-{F}(V0,V3), P_out2-{F}(V0,V3), P_ina1-{F}(V0,V4), P_inc-{F}(V0,V5), P_out1-{F}(V0,V6) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #323: mergings( V0 == V8, V6 == V12, V5 == V11, V7 == V13, V2 == V9, V4 == V10; #309 ), references = 1, size of lhs = 8:
% 20.35/20.53 P_a-{F}(V0), P_ina2-{F}(V0,V1), P_outc-{F}(V0,V2), P_out2-{F}(V0,V2), P_ina1-{F}(V0,V3), P_inb1-{F}(V0,V4), P_inc-{F}(V0,V5), P_out1-{F}(V0,V6) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #330: mergings( V6 == V12, V5 == V11, V7 == V13, V2 == V8, V4 == V10, V3 == V9; #310 ), references = 1, size of lhs = 8:
% 20.35/20.53 P_a-{F}(V0), P_outc-{F}(V0,V1), P_out2-{F}(V0,V1), P_ina1-{F}(V0,V2), P_ina2-{F}(V0,V3), P_inb1-{F}(V0,V4), P_inc-{F}(V0,V5), P_out1-{F}(V0,V6) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #339: mergings( V0 == V7, V5 == V10, V4 == V9, V6 == V11, V2 == V8; #331 ), references = 1, size of lhs = 7:
% 20.35/20.53 P_a-{F}(V0), P_inb1-{F}(V0,V1), P_outc-{F}(V0,V2), P_out2-{F}(V0,V2), P_ina1-{F}(V0,V3), P_inc-{F}(V0,V4), P_out1-{F}(V0,V5) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #348: mergings( V4 == V8, V3 == V7, V5 == V9, V2 == V6; #342 ), references = 1, size of lhs = 6:
% 20.35/20.53 P_a-{F}(V0), P_outc-{F}(V0,V1), P_out2-{F}(V0,V1), P_ina1-{F}(V0,V2), P_inc-{F}(V0,V3), P_out1-{F}(V0,V4) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #356: mergings( V3 == V6, V2 == V5, V4 == V7; #350 ), references = 1, size of lhs = 5:
% 20.35/20.53 P_a-{F}(V0), P_outc-{F}(V0,V1), P_out2-{F}(V0,V1), P_inc-{F}(V0,V2), P_out1-{F}(V0,V3) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #388: exists( #81, #386 ), references = 2, size of lhs = 9:
% 20.35/20.53 fulladder-{F}(V0), P_outs-{F}(V0,V1), one-{F}(V1), P_h2-{F}(V0,V2), fulladder-{F}(V3), P_h1-{F}(V3,V2), P_h2-{F}(V3,V4), P_in2-{F}(V4,V5), zero-{F}(V5) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #394: exists( #76, #392 ), references = 3, size of lhs = 11:
% 20.35/20.53 fulladder-{F}(V0), P_inc-{F}(V0,V1), zero-{F}(V1), P_h1-{F}(V0,V2), fulladder-{F}(V3), P_outs-{F}(V3,V4), one-{F}(V4), P_h2-{F}(V3,V5), fulladder-{F}(V6), P_h1-{F}(V6,V5), P_h2-{F}(V6,V2) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #398: exists( #92, #396 ), references = 1, size of lhs = 19:
% 20.35/20.53 P_a-{F}(V0), P_ina1-{F}(V0,V1), P_ina2-{F}(V0,V2), P_inb1-{F}(V0,V3), P_inc-{F}(V0,V4), P_out1-{F}(V0,V5), P_out2-{F}(V0,V6), P_outc-{F}(V0,V7), connection-{F}(V7,V8), fulladder-{F}(V9), P_inc-{F}(V9,V10), zero-{F}(V10), P_h1-{F}(V9,V11), fulladder-{F}(V12), P_outs-{F}(V12,V8), P_h2-{F}(V12,V13), fulladder-{F}(V14), P_h1-{F}(V14,V13), P_h2-{F}(V14,V11) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #400: exists( #91, #397 ), references = 3, size of lhs = 18:
% 20.35/20.53 P_a-{F}(V0), P_ina1-{F}(V0,V1), P_inb1-{F}(V0,V2), P_inc-{F}(V0,V3), P_out1-{F}(V0,V4), P_out2-{F}(V0,V5), P_outc-{F}(V0,V6), connection-{F}(V6,V7), fulladder-{F}(V8), P_inc-{F}(V8,V9), zero-{F}(V9), P_h1-{F}(V8,V10), fulladder-{F}(V11), P_outs-{F}(V11,V7), P_h2-{F}(V11,V12), fulladder-{F}(V13), P_h1-{F}(V13,V12), P_h2-{F}(V13,V10) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #402: exists( #90, #399 ), references = 4, size of lhs = 17:
% 20.35/20.53 P_a-{F}(V0), P_ina1-{F}(V0,V1), P_inc-{F}(V0,V2), P_out1-{F}(V0,V3), P_out2-{F}(V0,V4), P_outc-{F}(V0,V5), connection-{F}(V5,V6), fulladder-{F}(V7), P_inc-{F}(V7,V8), zero-{F}(V8), P_h1-{F}(V7,V9), fulladder-{F}(V10), P_outs-{F}(V10,V6), P_h2-{F}(V10,V11), fulladder-{F}(V12), P_h1-{F}(V12,V11), P_h2-{F}(V12,V9) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #410: exists( #89, #408 ), references = 1, size of lhs = 18:
% 20.35/20.53 nbit_adder2-{F}(V0), P_a-{F}(V0), P_f1-{F}(V0,V1), P_in1-{F}(V1,V2), P_inc-{F}(V0,V3), P_out1-{F}(V0,V4), P_out2-{F}(V0,V5), P_outc-{F}(V0,V6), connection-{F}(V6,V7), fulladder-{F}(V8), P_inc-{F}(V8,V2), P_h1-{F}(V8,V9), fulladder-{F}(V10), P_outs-{F}(V10,V7), P_h2-{F}(V10,V11), fulladder-{F}(V12), P_h1-{F}(V12,V11), P_h2-{F}(V12,V9) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #412: exists( #88, #409 ), references = 1, size of lhs = 17:
% 20.35/20.53 nbit_adder2-{F}(V0), P_a-{F}(V0), P_f1-{F}(V0,V1), P_in1-{F}(V1,V2), P_inc-{F}(V0,V3), P_out1-{F}(V0,V4), P_outc-{F}(V0,V5), connection-{F}(V5,V6), fulladder-{F}(V7), P_inc-{F}(V7,V2), P_h1-{F}(V7,V8), fulladder-{F}(V9), P_outs-{F}(V9,V6), P_h2-{F}(V9,V10), fulladder-{F}(V11), P_h1-{F}(V11,V10), P_h2-{F}(V11,V8) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #426: mergings( V0 == V4, V2 == V5; #421 ), references = 1, size of lhs = 7:
% 20.35/20.53 P_a-{F}(V0), P_inb1-{F}(V0,V1), P_outc-{F}(V0,V1), P_ina1-{F}(V0,V2), P_inc-{F}(V0,V3), P_out1-{F}(V0,V4), P_out2-{F}(V0,V5) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #451: exists( #82, #449 ), references = 7, size of lhs = 8:
% 20.35/20.53 nbit_adder2-{F}(V0), P_outc-{F}(V0,V1), one-{F}(V1), P_f2-{F}(V0,V2), fulladder-{F}(V2), P_or1-{F}(V2,V3), P_out1-{F}(V3,V4), zero-{F}(V4) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #476: mergings( V2 == V4, V0 == V5; #473 ), references = 2, size of lhs = 7:
% 20.35/20.53 zero-{F}(V0), nbit_adder2-{F}(V1), P_inc-{F}(V1,V0), P_f2-{F}(V1,V2), P_f1-{F}(V1,V2), P_outc-{F}(V2,V3), one-{F}(V3) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #481: mergings( V2 == V5; #479 ), references = 2, size of lhs = 7:
% 20.35/20.53 one-{F}(V0), zero-{F}(V1), nbit_adder2-{F}(V2), P_outc-{F}(V2,V0), P_inc-{F}(V2,V1), P_f2-{F}(V2,V3), P_f1-{F}(V2,V3) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #485: mergings( V9 == V12; #483 ), references = 2, size of lhs = 14:
% 20.35/20.53 P_a-{F}(V0), P_ina1-{F}(V0,V1), P_ina2-{F}(V0,V2), P_inb1-{F}(V0,V3), P_inc-{F}(V0,V4), P_out1-{F}(V0,V5), P_out2-{F}(V0,V6), P_outc-{F}(V0,V7), zero-{F}(V8), nbit_adder2-{F}(V9), P_outc-{F}(V9,V7), P_inc-{F}(V9,V8), P_f2-{F}(V9,V10), P_f1-{F}(V9,V10) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #488: mergings( V8 == V11; #486 ), references = 3, size of lhs = 13:
% 20.35/20.53 P_a-{F}(V0), P_ina1-{F}(V0,V1), P_inb1-{F}(V0,V2), P_inc-{F}(V0,V3), P_out1-{F}(V0,V4), P_out2-{F}(V0,V5), P_outc-{F}(V0,V6), zero-{F}(V7), nbit_adder2-{F}(V8), P_outc-{F}(V8,V6), P_inc-{F}(V8,V7), P_f2-{F}(V8,V9), P_f1-{F}(V8,V9) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #491: mergings( V7 == V10; #489 ), references = 3, size of lhs = 12:
% 20.35/20.53 P_a-{F}(V0), P_ina1-{F}(V0,V1), P_inc-{F}(V0,V2), P_out1-{F}(V0,V3), P_out2-{F}(V0,V4), P_outc-{F}(V0,V5), zero-{F}(V6), nbit_adder2-{F}(V7), P_outc-{F}(V7,V5), P_inc-{F}(V7,V6), P_f2-{F}(V7,V8), P_f1-{F}(V7,V8) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #507: mergings( V0 == V4, V2 == V5; #502 ), references = 1, size of lhs = 12:
% 20.35/20.53 P_a-{F}(V0), P_inb1-{F}(V0,V1), P_ina1-{F}(V0,V2), P_inc-{F}(V0,V3), P_out1-{F}(V0,V4), P_out2-{F}(V0,V5), P_outc-{F}(V0,V6), nbit_adder2-{F}(V7), P_outc-{F}(V7,V6), P_inc-{F}(V7,V1), P_f2-{F}(V7,V8), P_f1-{F}(V7,V8) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #510: mergings( V2 == V4, V3 == V5; #504 ), references = 1, size of lhs = 12:
% 20.35/20.53 P_a-{F}(V0), P_ina1-{F}(V0,V1), P_inb1-{F}(V0,V2), P_inc-{F}(V0,V3), P_out1-{F}(V0,V4), P_out2-{F}(V0,V5), P_outc-{F}(V0,V6), nbit_adder2-{F}(V7), P_outc-{F}(V7,V6), P_inc-{F}(V7,V2), P_f2-{F}(V7,V8), P_f1-{F}(V7,V8) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #514: mergings( V0 == V4, V2 == V5, V3 == V6; #503 ), references = 1, size of lhs = 12:
% 20.35/20.53 P_a-{F}(V0), P_ina1-{F}(V0,V1), P_inb1-{F}(V0,V2), P_inc-{F}(V0,V3), P_out1-{F}(V0,V4), P_out2-{F}(V0,V5), P_outc-{F}(V0,V6), nbit_adder2-{F}(V7), P_outc-{F}(V7,V6), P_inc-{F}(V7,V2), P_f2-{F}(V7,V8), P_f1-{F}(V7,V8) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #525: mergings( V0 == V6, V5 == V8, V2 == V7; #519 ), references = 1, size of lhs = 13:
% 20.35/20.53 P_a-{F}(V0), P_ina2-{F}(V0,V1), P_inb1-{F}(V0,V2), P_ina1-{F}(V0,V3), P_inc-{F}(V0,V4), P_out1-{F}(V0,V5), P_out2-{F}(V0,V6), P_outc-{F}(V0,V7), nbit_adder2-{F}(V8), P_outc-{F}(V8,V7), P_inc-{F}(V8,V4), P_f2-{F}(V8,V9), P_f1-{F}(V8,V9) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #530: mergings( V0 == V6, V5 == V9, V2 == V7, V4 == V8; #520 ), references = 1, size of lhs = 13:
% 20.35/20.53 P_a-{F}(V0), P_ina2-{F}(V0,V1), P_ina1-{F}(V0,V2), P_inb1-{F}(V0,V3), P_inc-{F}(V0,V4), P_out1-{F}(V0,V5), P_out2-{F}(V0,V6), P_outc-{F}(V0,V7), nbit_adder2-{F}(V8), P_outc-{F}(V8,V7), P_inc-{F}(V8,V4), P_f2-{F}(V8,V9), P_f1-{F}(V8,V9) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #535: mergings( V5 == V9, V2 == V6, V4 == V8, V3 == V7; #521 ), references = 1, size of lhs = 13:
% 20.35/20.53 P_a-{F}(V0), P_ina1-{F}(V0,V1), P_ina2-{F}(V0,V2), P_inb1-{F}(V0,V3), P_inc-{F}(V0,V4), P_out1-{F}(V0,V5), P_out2-{F}(V0,V6), P_outc-{F}(V0,V7), nbit_adder2-{F}(V8), P_outc-{F}(V8,V7), P_inc-{F}(V8,V4), P_f2-{F}(V8,V9), P_f1-{F}(V8,V9) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #542: mergings( V0 == V5, V4 == V7, V2 == V6; #536 ), references = 1, size of lhs = 12:
% 20.35/20.53 P_a-{F}(V0), P_inb1-{F}(V0,V1), P_ina1-{F}(V0,V2), P_inc-{F}(V0,V3), P_out1-{F}(V0,V4), P_out2-{F}(V0,V5), P_outc-{F}(V0,V6), nbit_adder2-{F}(V7), P_outc-{F}(V7,V6), P_inc-{F}(V7,V3), P_f2-{F}(V7,V8), P_f1-{F}(V7,V8) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #546: mergings( V4 == V7, V2 == V5, V3 == V6; #538 ), references = 1, size of lhs = 12:
% 20.35/20.53 P_a-{F}(V0), P_ina1-{F}(V0,V1), P_inb1-{F}(V0,V2), P_inc-{F}(V0,V3), P_out1-{F}(V0,V4), P_out2-{F}(V0,V5), P_outc-{F}(V0,V6), nbit_adder2-{F}(V7), P_outc-{F}(V7,V6), P_inc-{F}(V7,V3), P_f2-{F}(V7,V8), P_f1-{F}(V7,V8) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #551: mergings( V0 == V5, V4 == V8, V2 == V6, V3 == V7; #537 ), references = 1, size of lhs = 12:
% 20.35/20.53 P_a-{F}(V0), P_ina1-{F}(V0,V1), P_inb1-{F}(V0,V2), P_inc-{F}(V0,V3), P_out1-{F}(V0,V4), P_out2-{F}(V0,V5), P_outc-{F}(V0,V6), nbit_adder2-{F}(V7), P_outc-{F}(V7,V6), P_inc-{F}(V7,V3), P_f2-{F}(V7,V8), P_f1-{F}(V7,V8) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #557: mergings( V3 == V5, V2 == V4; #553 ), references = 1, size of lhs = 11:
% 20.35/20.53 P_a-{F}(V0), P_ina1-{F}(V0,V1), P_inc-{F}(V0,V2), P_out1-{F}(V0,V3), P_out2-{F}(V0,V4), P_outc-{F}(V0,V5), nbit_adder2-{F}(V6), P_outc-{F}(V6,V5), P_inc-{F}(V6,V2), P_f2-{F}(V6,V7), P_f1-{F}(V6,V7) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #560: mergings( V3 == V5, V2 == V4; #554 ), references = 1, size of lhs = 11:
% 20.35/20.53 P_a-{F}(V0), P_ina1-{F}(V0,V1), P_inc-{F}(V0,V2), P_out1-{F}(V0,V3), P_out2-{F}(V0,V4), P_outc-{F}(V0,V5), nbit_adder2-{F}(V6), P_outc-{F}(V6,V5), P_inc-{F}(V6,V2), P_f2-{F}(V6,V7), P_f1-{F}(V6,V7) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #564: mergings( V0 == V4, V3 == V6, V2 == V5; #552 ), references = 1, size of lhs = 11:
% 20.35/20.53 P_a-{F}(V0), P_ina1-{F}(V0,V1), P_inc-{F}(V0,V2), P_out1-{F}(V0,V3), P_out2-{F}(V0,V4), P_outc-{F}(V0,V5), nbit_adder2-{F}(V6), P_outc-{F}(V6,V5), P_inc-{F}(V6,V2), P_f2-{F}(V6,V7), P_f1-{F}(V6,V7) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #569: mergings( V2 == V3; #565 ), references = 1, size of lhs = 10:
% 20.35/20.53 P_a-{F}(V0), P_inc-{F}(V0,V1), P_out1-{F}(V0,V2), P_out2-{F}(V0,V3), P_outc-{F}(V0,V4), nbit_adder2-{F}(V5), P_outc-{F}(V5,V4), P_inc-{F}(V5,V1), P_f2-{F}(V5,V6), P_f1-{F}(V5,V6) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #571: mergings( V2 == V3; #566 ), references = 1, size of lhs = 10:
% 20.35/20.53 P_a-{F}(V0), P_inc-{F}(V0,V1), P_out1-{F}(V0,V2), P_out2-{F}(V0,V3), P_outc-{F}(V0,V4), nbit_adder2-{F}(V5), P_outc-{F}(V5,V4), P_inc-{F}(V5,V1), P_f2-{F}(V5,V6), P_f1-{F}(V5,V6) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #573: mergings( V2 == V3; #567 ), references = 1, size of lhs = 10:
% 20.35/20.53 P_a-{F}(V0), P_inc-{F}(V0,V1), P_out1-{F}(V0,V2), P_out2-{F}(V0,V3), P_outc-{F}(V0,V4), nbit_adder2-{F}(V5), P_outc-{F}(V5,V4), P_inc-{F}(V5,V1), P_f2-{F}(V5,V6), P_f1-{F}(V5,V6) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #578: mergings( V2 == V3; #574 ), references = 1, size of lhs = 9:
% 20.35/20.53 P_a-{F}(V0), P_inc-{F}(V0,V1), P_out1-{F}(V0,V2), P_outc-{F}(V0,V3), nbit_adder2-{F}(V4), P_outc-{F}(V4,V3), P_inc-{F}(V4,V1), P_f2-{F}(V4,V5), P_f1-{F}(V4,V5) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #580: mergings( V2 == V3; #575 ), references = 1, size of lhs = 9:
% 20.35/20.53 P_a-{F}(V0), P_inc-{F}(V0,V1), P_out1-{F}(V0,V2), P_outc-{F}(V0,V3), nbit_adder2-{F}(V4), P_outc-{F}(V4,V3), P_inc-{F}(V4,V1), P_f2-{F}(V4,V5), P_f1-{F}(V4,V5) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #582: mergings( V2 == V3; #576 ), references = 1, size of lhs = 9:
% 20.35/20.53 P_a-{F}(V0), P_inc-{F}(V0,V1), P_out1-{F}(V0,V2), P_outc-{F}(V0,V3), nbit_adder2-{F}(V4), P_outc-{F}(V4,V3), P_inc-{F}(V4,V1), P_f2-{F}(V4,V5), P_f1-{F}(V4,V5) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #613: mergings( V2 == V4; #610 ), references = 1, size of lhs = 9:
% 20.35/20.53 zero-{F}(V0), nbit_adder2-{F}(V1), P_out1-{F}(V1,V0), P_f1-{F}(V1,V2), P_outc-{F}(V1,V3), one-{F}(V3), P_f2-{F}(V1,V4), fulladder-{F}(V4), P_or1-{F}(V4,V2) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #665: exists( #82, #659 ), references = 1, size of lhs = 18:
% 20.35/20.53 nbit_adder2-{F}(V0), P_f1-{F}(V0,V1), fulladder-{F}(V1), P_f2-{F}(V0,V2), P_inc-{F}(V2,V3), P_or1-{F}(V1,V4), P_out1-{F}(V4,V5), zero-{F}(V5), fulladder-{F}(V6), P_inc-{F}(V6,V3), P_h1-{F}(V6,V7), fulladder-{F}(V8), P_outs-{F}(V8,V9), one-{F}(V9), P_h2-{F}(V8,V10), fulladder-{F}(V11), P_h1-{F}(V11,V10), P_h2-{F}(V11,V7) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #666: exists( #82, #660 ), references = 1, size of lhs = 24:
% 20.35/20.53 nbit_adder2-{F}(V0), P_f1-{F}(V0,V1), fulladder-{F}(V1), P_f2-{F}(V0,V2), P_inc-{F}(V2,V3), P_or1-{F}(V1,V4), P_out1-{F}(V4,V5), zero-{F}(V5), P_a-{F}(V6), P_ina1-{F}(V6,V7), P_inc-{F}(V6,V8), P_out1-{F}(V6,V9), P_out2-{F}(V6,V10), P_outc-{F}(V6,V11), connection-{F}(V11,V12), fulladder-{F}(V13), P_inc-{F}(V13,V3), P_h1-{F}(V13,V14), fulladder-{F}(V15), P_outs-{F}(V15,V12), P_h2-{F}(V15,V16), fulladder-{F}(V17), P_h1-{F}(V17,V16), P_h2-{F}(V17,V14) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #667: exists( #82, #661 ), references = 1, size of lhs = 25:
% 20.35/20.53 nbit_adder2-{F}(V0), P_f1-{F}(V0,V1), fulladder-{F}(V1), P_f2-{F}(V0,V2), P_inc-{F}(V2,V3), P_or1-{F}(V1,V4), P_out1-{F}(V4,V5), zero-{F}(V5), P_a-{F}(V6), P_ina1-{F}(V6,V7), P_inb1-{F}(V6,V8), P_inc-{F}(V6,V9), P_out1-{F}(V6,V10), P_out2-{F}(V6,V11), P_outc-{F}(V6,V12), connection-{F}(V12,V13), fulladder-{F}(V14), P_inc-{F}(V14,V3), P_h1-{F}(V14,V15), fulladder-{F}(V16), P_outs-{F}(V16,V13), P_h2-{F}(V16,V17), fulladder-{F}(V18), P_h1-{F}(V18,V17), P_h2-{F}(V18,V15) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #689: exists( #85, #683 ), references = 2, size of lhs = 13:
% 20.35/20.53 nbit_adder2-{F}(V0), P_inc-{F}(V0,V1), zero-{F}(V1), P_f1-{F}(V0,V2), fulladder-{F}(V2), P_h1-{F}(V2,V3), fulladder-{F}(V4), P_outs-{F}(V4,V5), one-{F}(V5), P_h2-{F}(V4,V6), fulladder-{F}(V7), P_h1-{F}(V7,V6), P_h2-{F}(V7,V3) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #690: exists( #85, #684 ), references = 1, size of lhs = 19:
% 20.35/20.53 nbit_adder2-{F}(V0), P_inc-{F}(V0,V1), zero-{F}(V1), P_f1-{F}(V0,V2), fulladder-{F}(V2), P_a-{F}(V3), P_ina1-{F}(V3,V4), P_inc-{F}(V3,V5), P_out1-{F}(V3,V6), P_out2-{F}(V3,V7), P_outc-{F}(V3,V8), connection-{F}(V8,V9), P_h1-{F}(V2,V10), fulladder-{F}(V11), P_outs-{F}(V11,V9), P_h2-{F}(V11,V12), fulladder-{F}(V13), P_h1-{F}(V13,V12), P_h2-{F}(V13,V10) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #691: exists( #85, #685 ), references = 1, size of lhs = 20:
% 20.35/20.53 nbit_adder2-{F}(V0), P_inc-{F}(V0,V1), zero-{F}(V1), P_f1-{F}(V0,V2), fulladder-{F}(V2), P_a-{F}(V3), P_ina1-{F}(V3,V4), P_inb1-{F}(V3,V5), P_inc-{F}(V3,V6), P_out1-{F}(V3,V7), P_out2-{F}(V3,V8), P_outc-{F}(V3,V9), connection-{F}(V9,V10), P_h1-{F}(V2,V11), fulladder-{F}(V12), P_outs-{F}(V12,V10), P_h2-{F}(V12,V13), fulladder-{F}(V14), P_h1-{F}(V14,V13), P_h2-{F}(V14,V11) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #708: exists( #75, #703 ), references = 3, size of lhs = 11:
% 20.35/20.53 halfadder-{F}(V0), P_and2-{F}(V0,V1), P_not1-{F}(V0,V2), P_in1-{F}(V2,V3), zero-{F}(V3), nbit_adder2-{F}(V4), P_outc-{F}(V4,V5), one-{F}(V5), P_f2-{F}(V4,V6), fulladder-{F}(V6), P_or1-{F}(V6,V1) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #709: exists( #75, #705 ), references = 3, size of lhs = 9:
% 20.35/20.53 fulladder-{F}(V0), P_outc-{F}(V0,V1), one-{F}(V1), P_or1-{F}(V0,V2), halfadder-{F}(V3), P_and2-{F}(V3,V2), P_not1-{F}(V3,V4), P_in1-{F}(V4,V5), zero-{F}(V5) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #768: exists( #81, #766 ), references = 2, size of lhs = 8:
% 20.35/20.53 fulladder-{F}(V0), P_outs-{F}(V0,V1), one-{F}(V1), P_h2-{F}(V0,V2), halfadder-{F}(V2), P_and1-{F}(V2,V3), P_out1-{F}(V3,V4), zero-{F}(V4) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #790: exists( #82, #788 ), references = 3, size of lhs = 10:
% 20.35/20.53 fulladder-{F}(V0), P_h2-{F}(V0,V1), P_or1-{F}(V0,V2), P_in1-{F}(V2,V3), zero-{F}(V3), fulladder-{F}(V4), P_h1-{F}(V4,V1), P_or1-{F}(V4,V5), P_in2-{F}(V5,V6), one-{F}(V6) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #794: exists( #76, #792 ), references = 2, size of lhs = 12:
% 20.35/20.53 fulladder-{F}(V0), P_inc-{F}(V0,V1), one-{F}(V1), P_h1-{F}(V0,V2), fulladder-{F}(V3), P_h2-{F}(V3,V4), P_or1-{F}(V3,V5), P_in1-{F}(V5,V6), zero-{F}(V6), fulladder-{F}(V7), P_h1-{F}(V7,V4), P_or1-{F}(V7,V2) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #826: exists( #81, #822 ), references = 1, size of lhs = 17:
% 20.35/20.53 fulladder-{F}(V0), P_outs-{F}(V0,V1), one-{F}(V1), P_h2-{F}(V0,V2), fulladder-{F}(V3), P_h1-{F}(V3,V2), P_h2-{F}(V3,V4), P_in2-{F}(V4,V5), fulladder-{F}(V6), P_h2-{F}(V6,V7), P_or1-{F}(V6,V8), P_in1-{F}(V8,V9), zero-{F}(V9), fulladder-{F}(V10), P_h1-{F}(V10,V7), P_or1-{F}(V10,V11), P_in2-{F}(V11,V5) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #828: exists( #76, #824 ), references = 2, size of lhs = 15:
% 20.35/20.53 fulladder-{F}(V0), P_outs-{F}(V0,V1), one-{F}(V1), P_h2-{F}(V0,V2), fulladder-{F}(V3), P_h1-{F}(V3,V2), P_h2-{F}(V3,V4), fulladder-{F}(V5), P_h2-{F}(V5,V6), P_or1-{F}(V5,V7), P_in1-{F}(V7,V8), zero-{F}(V8), fulladder-{F}(V9), P_h1-{F}(V9,V6), P_or1-{F}(V9,V4) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #832: exists( #74, #830 ), references = 2, size of lhs = 17:
% 20.35/20.53 fulladder-{F}(V0), P_in2-{F}(V0,V1), zero-{F}(V1), P_h1-{F}(V0,V2), fulladder-{F}(V3), P_outs-{F}(V3,V4), one-{F}(V4), P_h2-{F}(V3,V5), fulladder-{F}(V6), P_h1-{F}(V6,V5), P_h2-{F}(V6,V7), fulladder-{F}(V8), P_or1-{F}(V8,V2), P_h2-{F}(V8,V9), fulladder-{F}(V10), P_h1-{F}(V10,V9), P_or1-{F}(V10,V7) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #877: exists( #81, #875 ), references = 1, size of lhs = 9:
% 20.35/20.53 fulladder-{F}(V0), P_h1-{F}(V0,V1), halfadder-{F}(V1), P_h2-{F}(V0,V2), P_in2-{F}(V2,V3), zero-{F}(V3), P_and1-{F}(V1,V4), P_out1-{F}(V4,V5), one-{F}(V5) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #879: disj( #20, input ), references = 1, size of lhs = 12:
% 20.35/20.53 logic_or-{F}(V0), P_a-{F}(V1), P_ina1-{F}(V1,V2), P_ina2-{F}(V1,V3), P_inb1-{F}(V1,V4), P_inb2-{F}(V1,V5), P_inc-{F}(V1,V6), P_out1-{F}(V1,V7), P_out2-{F}(V1,V8), P_outc-{F}(V1,V9), P_f2-{F}(V1,V10), P_or1-{F}(V10,V0) | or_ok-{T}(V0)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #904: exists( #76, #898 ), references = 3, size of lhs = 9:
% 20.35/20.53 fulladder-{F}(V0), P_inc-{F}(V0,V1), zero-{F}(V1), P_h1-{F}(V0,V2), or_ok-{F}(V2), P_in1-{F}(V2,V3), zero-{F}(V3), P_out1-{F}(V2,V4), one-{F}(V4) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #905: exists( #76, #899 ), references = 1, size of lhs = 14:
% 20.35/20.53 fulladder-{F}(V0), P_inc-{F}(V0,V1), zero-{F}(V1), P_h1-{F}(V0,V2), or_ok-{F}(V2), P_in1-{F}(V2,V3), zero-{F}(V3), P_out1-{F}(V2,V4), P_a-{F}(V5), P_outc-{F}(V5,V4), P_ina1-{F}(V5,V6), P_inc-{F}(V5,V7), P_out1-{F}(V5,V8), P_out2-{F}(V5,V9) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #906: exists( #76, #900 ), references = 1, size of lhs = 15:
% 20.35/20.53 fulladder-{F}(V0), P_inc-{F}(V0,V1), zero-{F}(V1), P_h1-{F}(V0,V2), or_ok-{F}(V2), P_in1-{F}(V2,V3), zero-{F}(V3), P_out1-{F}(V2,V4), P_a-{F}(V5), P_outc-{F}(V5,V4), P_ina1-{F}(V5,V6), P_inb1-{F}(V5,V7), P_inc-{F}(V5,V8), P_out1-{F}(V5,V9), P_out2-{F}(V5,V10) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #910: exists( #75, #908 ), references = 4, size of lhs = 11:
% 20.35/20.53 fulladder-{F}(V0), P_outc-{F}(V0,V1), one-{F}(V1), P_or1-{F}(V0,V2), or_ok-{F}(V2), fulladder-{F}(V3), P_h1-{F}(V3,V2), P_inc-{F}(V3,V4), zero-{F}(V4), P_in1-{F}(V2,V5), zero-{F}(V5) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #914: exists( #74, #912 ), references = 7, size of lhs = 13:
% 20.35/20.53 fulladder-{F}(V0), P_in2-{F}(V0,V1), zero-{F}(V1), P_h1-{F}(V0,V2), or_ok-{F}(V2), fulladder-{F}(V3), P_or1-{F}(V3,V2), P_outc-{F}(V3,V4), one-{F}(V4), fulladder-{F}(V5), P_h1-{F}(V5,V2), P_inc-{F}(V5,V6), zero-{F}(V6) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #938: exists( #82, #936 ), references = 1, size of lhs = 9:
% 20.35/20.53 nbit_adder2-{F}(V0), P_f1-{F}(V0,V1), fulladder-{F}(V1), P_f2-{F}(V0,V2), P_inc-{F}(V2,V3), one-{F}(V3), P_or1-{F}(V1,V4), P_out1-{F}(V4,V5), zero-{F}(V5) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #969: exists( #74, #967 ), references = 1, size of lhs = 14:
% 20.35/20.53 fulladder-{F}(V0), P_in2-{F}(V0,V1), zero-{F}(V1), P_h1-{F}(V0,V2), fulladder-{F}(V3), P_inc-{F}(V3,V4), one-{F}(V4), P_h1-{F}(V3,V5), fulladder-{F}(V6), P_or1-{F}(V6,V2), P_h2-{F}(V6,V7), fulladder-{F}(V8), P_h1-{F}(V8,V7), P_or1-{F}(V8,V5) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #990: disj( #26, input ), references = 1, size of lhs = 16:
% 20.35/20.53 logic_not-{F}(V0), P_a-{F}(V1), P_ina1-{F}(V1,V2), P_ina2-{F}(V1,V3), P_inb1-{F}(V1,V4), P_inb2-{F}(V1,V5), P_inc-{F}(V1,V6), P_out1-{F}(V1,V7), P_out2-{F}(V1,V8), P_outc-{F}(V1,V9), P_f2-{F}(V1,V10), P_or1-{F}(V10,V11), P_h1-{F}(V10,V12), P_and2-{F}(V12,V13), P_h2-{F}(V10,V14), P_and2-{F}(V14,V0) | not_ok-{T}(V0)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #991: disj( #26, input ), references = 3, size of lhs = 2:
% 20.35/20.53 logic_not-{F}(V0), and_ok-{F}(V0) | not_ok-{T}(V0)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #1001: exists( #78, #995 ), references = 1, size of lhs = 19:
% 20.35/20.53 logic_not-{F}(V0), P_a-{F}(V1), P_ina1-{F}(V1,V2), P_ina2-{F}(V1,V3), P_inb1-{F}(V1,V4), P_inb2-{F}(V1,V5), P_inc-{F}(V1,V6), P_out1-{F}(V1,V7), P_out2-{F}(V1,V8), P_outc-{F}(V1,V9), P_f2-{F}(V1,V10), P_or1-{F}(V10,V11), P_h1-{F}(V10,V12), P_h2-{F}(V10,V13), P_and2-{F}(V13,V0), P_in1-{F}(V0,V14), zero-{F}(V14), P_out1-{F}(V0,V15), zero-{F}(V15) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #1002: exists( #78, #996 ), references = 1, size of lhs = 25:
% 20.35/20.53 logic_not-{F}(V0), P_a-{F}(V1), P_ina1-{F}(V1,V2), P_ina2-{F}(V1,V3), P_inb1-{F}(V1,V4), P_inb2-{F}(V1,V5), P_inc-{F}(V1,V6), P_out1-{F}(V1,V7), P_out2-{F}(V1,V8), P_outc-{F}(V1,V9), P_f2-{F}(V1,V10), P_or1-{F}(V10,V11), P_h1-{F}(V10,V12), P_h2-{F}(V10,V13), P_and2-{F}(V13,V0), P_in1-{F}(V0,V14), zero-{F}(V14), P_out1-{F}(V0,V15), fulladder-{F}(V16), P_outs-{F}(V16,V15), P_h2-{F}(V16,V17), halfadder-{F}(V17), P_and1-{F}(V17,V18), P_out1-{F}(V18,V19), zero-{F}(V19) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #1030: exists( #82, #1028 ), references = 4, size of lhs = 20:
% 20.35/20.53 nbit_adder2-{F}(V0), P_f1-{F}(V0,V1), fulladder-{F}(V1), P_f2-{F}(V0,V2), P_inc-{F}(V2,V3), P_or1-{F}(V1,V4), P_out1-{F}(V4,V5), zero-{F}(V5), fulladder-{F}(V6), P_in2-{F}(V6,V7), zero-{F}(V7), P_h1-{F}(V6,V8), or_ok-{F}(V8), fulladder-{F}(V9), P_or1-{F}(V9,V8), P_outc-{F}(V9,V10), one-{F}(V10), fulladder-{F}(V11), P_h1-{F}(V11,V8), P_inc-{F}(V11,V3) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #1114: exists( #81, #1108 ), references = 1, size of lhs = 21:
% 20.35/20.53 fulladder-{F}(V0), P_outs-{F}(V0,V1), zero-{F}(V1), P_h2-{F}(V0,V2), fulladder-{F}(V3), P_h1-{F}(V3,V2), P_h2-{F}(V3,V4), P_in2-{F}(V4,V5), fulladder-{F}(V6), P_in2-{F}(V6,V7), zero-{F}(V7), P_h1-{F}(V6,V8), or_ok-{F}(V8), fulladder-{F}(V9), P_or1-{F}(V9,V8), P_outc-{F}(V9,V10), one-{F}(V10), fulladder-{F}(V11), P_h1-{F}(V11,V8), P_inc-{F}(V11,V12), connection-{F}(V12,V5) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #1115: exists( #81, #1109 ), references = 1, size of lhs = 19:
% 20.35/20.53 fulladder-{F}(V0), P_outs-{F}(V0,V1), zero-{F}(V1), P_h2-{F}(V0,V2), fulladder-{F}(V3), P_h1-{F}(V3,V2), P_h2-{F}(V3,V4), P_in2-{F}(V4,V5), fulladder-{F}(V6), P_outc-{F}(V6,V7), one-{F}(V7), P_or1-{F}(V6,V8), or_ok-{F}(V8), fulladder-{F}(V9), P_h1-{F}(V9,V8), P_inc-{F}(V9,V10), connection-{F}(V10,V5), P_in1-{F}(V8,V11), zero-{F}(V11) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #1116: exists( #81, #1110 ), references = 1, size of lhs = 14:
% 20.35/20.53 fulladder-{F}(V0), P_outs-{F}(V0,V1), zero-{F}(V1), P_h2-{F}(V0,V2), fulladder-{F}(V3), P_h1-{F}(V3,V2), P_h2-{F}(V3,V4), P_in2-{F}(V4,V5), or_ok-{F}(V6), P_in2-{F}(V6,V5), P_in1-{F}(V6,V7), zero-{F}(V7), P_out1-{F}(V6,V8), one-{F}(V8) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #1122: exists( #76, #1117 ), references = 1, size of lhs = 22:
% 20.35/20.53 fulladder-{F}(V0), P_inc-{F}(V0,V1), P_h1-{F}(V0,V2), fulladder-{F}(V3), P_outs-{F}(V3,V4), zero-{F}(V4), P_h2-{F}(V3,V5), fulladder-{F}(V6), P_h1-{F}(V6,V5), P_h2-{F}(V6,V2), fulladder-{F}(V7), P_in2-{F}(V7,V8), zero-{F}(V8), P_h1-{F}(V7,V9), or_ok-{F}(V9), fulladder-{F}(V10), P_or1-{F}(V10,V9), P_outc-{F}(V10,V11), one-{F}(V11), fulladder-{F}(V12), P_h1-{F}(V12,V9), P_inc-{F}(V12,V1) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #1125: mergings( V2 == V9; #1123 ), references = 1, size of lhs = 18:
% 20.35/20.53 fulladder-{F}(V0), P_outs-{F}(V0,V1), zero-{F}(V1), P_h2-{F}(V0,V2), fulladder-{F}(V3), P_h1-{F}(V3,V2), P_h2-{F}(V3,V4), or_ok-{F}(V4), fulladder-{F}(V5), P_h1-{F}(V5,V4), P_in2-{F}(V5,V6), zero-{F}(V6), fulladder-{F}(V7), P_or1-{F}(V7,V4), P_outc-{F}(V7,V8), one-{F}(V8), fulladder-{F}(V9), P_h1-{F}(V9,V4) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #1149: exists( #76, #1147 ), references = 2, size of lhs = 9:
% 20.35/20.53 fulladder-{F}(V0), P_inc-{F}(V0,V1), one-{F}(V1), P_h1-{F}(V0,V2), fulladder-{F}(V3), P_or1-{F}(V3,V2), P_h1-{F}(V3,V4), P_outc-{F}(V4,V5), zero-{F}(V5) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #1184: exists( #74, #1178 ), references = 1, size of lhs = 13:
% 20.35/20.53 fulladder-{F}(V0), P_in1-{F}(V0,V1), zero-{F}(V1), P_h2-{F}(V0,V2), halfadder-{F}(V3), P_not1-{F}(V3,V2), P_and2-{F}(V3,V4), nbit_adder2-{F}(V5), P_outc-{F}(V5,V6), one-{F}(V6), P_f2-{F}(V5,V7), fulladder-{F}(V7), P_or1-{F}(V7,V4) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #1185: exists( #74, #1179 ), references = 2, size of lhs = 11:
% 20.35/20.53 fulladder-{F}(V0), P_in1-{F}(V0,V1), zero-{F}(V1), P_h2-{F}(V0,V2), fulladder-{F}(V3), P_outc-{F}(V3,V4), one-{F}(V4), P_or1-{F}(V3,V5), halfadder-{F}(V6), P_and2-{F}(V6,V5), P_not1-{F}(V6,V2) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #1186: exists( #74, #1180 ), references = 2, size of lhs = 9:
% 20.35/20.53 fulladder-{F}(V0), P_in1-{F}(V0,V1), zero-{F}(V1), P_h2-{F}(V0,V2), halfadder-{F}(V3), P_not1-{F}(V3,V2), P_and2-{F}(V3,V4), P_out1-{F}(V4,V5), one-{F}(V5) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #1224: exists( #76, #1222 ), references = 2, size of lhs = 9:
% 20.35/20.53 halfadder-{F}(V0), P_in2-{F}(V0,V1), one-{F}(V1), P_or1-{F}(V0,V2), fulladder-{F}(V3), P_h2-{F}(V3,V2), P_h1-{F}(V3,V4), P_outs-{F}(V4,V5), zero-{F}(V5) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #1234: exists( #81, #1232 ), references = 1, size of lhs = 11:
% 20.35/20.53 halfadder-{F}(V0), P_and1-{F}(V0,V1), P_out1-{F}(V1,V2), zero-{F}(V2), halfadder-{F}(V3), P_in2-{F}(V3,V4), one-{F}(V4), P_or1-{F}(V3,V5), fulladder-{F}(V6), P_h2-{F}(V6,V5), P_h1-{F}(V6,V0) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #1261: exists( #74, #1256 ), references = 1, size of lhs = 13:
% 20.35/20.53 fulladder-{F}(V0), P_in2-{F}(V0,V1), zero-{F}(V1), P_h1-{F}(V0,V2), halfadder-{F}(V3), P_not1-{F}(V3,V2), P_and2-{F}(V3,V4), nbit_adder2-{F}(V5), P_outc-{F}(V5,V6), one-{F}(V6), P_f2-{F}(V5,V7), fulladder-{F}(V7), P_or1-{F}(V7,V4) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #1262: exists( #74, #1257 ), references = 1, size of lhs = 11:
% 20.35/20.53 fulladder-{F}(V0), P_in2-{F}(V0,V1), zero-{F}(V1), P_h1-{F}(V0,V2), fulladder-{F}(V3), P_outc-{F}(V3,V4), one-{F}(V4), P_or1-{F}(V3,V5), halfadder-{F}(V6), P_and2-{F}(V6,V5), P_not1-{F}(V6,V2) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #1292: exists( #76, #1290 ), references = 1, size of lhs = 8:
% 20.35/20.53 fulladder-{F}(V0), P_inc-{F}(V0,V1), zero-{F}(V1), P_h1-{F}(V0,V2), halfadder-{F}(V3), P_or1-{F}(V3,V2), P_in2-{F}(V3,V4), one-{F}(V4) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #1327: exists( #82, #1323 ), references = 2, size of lhs = 11:
% 20.35/20.53 halfadder-{F}(V0), P_and2-{F}(V0,V1), P_out1-{F}(V1,V2), zero-{F}(V2), fulladder-{F}(V3), P_inc-{F}(V3,V4), one-{F}(V4), P_h1-{F}(V3,V5), fulladder-{F}(V6), P_or1-{F}(V6,V5), P_h1-{F}(V6,V0) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #1331: disj( #12, input ), references = 1, size of lhs = 2:
% 20.35/20.53 logic_and-{F}(V0), or_ok-{F}(V0) | and_ok-{T}(V0)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #1332: disj( #12, input ), references = 1, size of lhs = 12:
% 20.35/20.53 logic_and-{F}(V0), P_a-{F}(V1), P_ina1-{F}(V1,V2), P_ina2-{F}(V1,V3), P_inb1-{F}(V1,V4), P_inb2-{F}(V1,V5), P_inc-{F}(V1,V6), P_out1-{F}(V1,V7), P_out2-{F}(V1,V8), P_outc-{F}(V1,V9), P_f2-{F}(V1,V10), P_or1-{F}(V10,V0) | and_ok-{T}(V0)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #1333: disj( #12, input ), references = 5, size of lhs = 14:
% 20.35/20.53 logic_and-{F}(V0), P_a-{F}(V1), P_ina1-{F}(V1,V2), P_ina2-{F}(V1,V3), P_inb1-{F}(V1,V4), P_inb2-{F}(V1,V5), P_inc-{F}(V1,V6), P_out1-{F}(V1,V7), P_out2-{F}(V1,V8), P_outc-{F}(V1,V9), P_f2-{F}(V1,V10), P_or1-{F}(V10,V11), P_h1-{F}(V10,V12), P_and2-{F}(V12,V0) | and_ok-{T}(V0)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #1362: exists( #75, #1360 ), references = 4, size of lhs = 12:
% 20.35/20.53 and_ok-{F}(V0), P_in1-{F}(V0,V1), zero-{F}(V1), halfadder-{F}(V2), P_and2-{F}(V2,V0), fulladder-{F}(V3), P_inc-{F}(V3,V4), one-{F}(V4), P_h1-{F}(V3,V5), fulladder-{F}(V6), P_or1-{F}(V6,V5), P_h1-{F}(V6,V2) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #1372: exists( #74, #1370 ), references = 1, size of lhs = 14:
% 20.35/20.53 fulladder-{F}(V0), P_in1-{F}(V0,V1), zero-{F}(V1), P_h2-{F}(V0,V2), and_ok-{F}(V2), halfadder-{F}(V3), P_and2-{F}(V3,V2), fulladder-{F}(V4), P_inc-{F}(V4,V5), one-{F}(V5), P_h1-{F}(V4,V6), fulladder-{F}(V7), P_or1-{F}(V7,V6), P_h1-{F}(V7,V3) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #1407: exists( #74, #1405 ), references = 1, size of lhs = 14:
% 20.35/20.53 fulladder-{F}(V0), P_in2-{F}(V0,V1), zero-{F}(V1), P_h1-{F}(V0,V2), and_ok-{F}(V2), halfadder-{F}(V3), P_and2-{F}(V3,V2), fulladder-{F}(V4), P_inc-{F}(V4,V5), one-{F}(V5), P_h1-{F}(V4,V6), fulladder-{F}(V7), P_or1-{F}(V7,V6), P_h1-{F}(V7,V3) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #1438: exists( #76, #1436 ), references = 2, size of lhs = 9:
% 20.35/20.53 fulladder-{F}(V0), P_inc-{F}(V0,V1), zero-{F}(V1), P_h1-{F}(V0,V2), halfadder-{F}(V3), P_and1-{F}(V3,V2), P_not1-{F}(V3,V4), P_out1-{F}(V4,V5), one-{F}(V5) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #1466: disj( #12, #991+#21+#4 ), references = 1, size of lhs = 6:
% 20.35/20.53 logic_and-{F}(V0), logic_not-{F}(V0), P_in1-{F}(V0,V1), zero-{F}(V1), P_out1-{F}(V0,V2), zero-{F}(V2) | abnormal-{T}(V0)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #1467: disj( #12, #991+#21+#1186 ), references = 1, size of lhs = 13:
% 20.35/20.53 logic_and-{F}(V0), logic_not-{F}(V0), P_in1-{F}(V0,V1), zero-{F}(V1), P_out1-{F}(V0,V2), fulladder-{F}(V3), P_in1-{F}(V3,V4), zero-{F}(V4), P_h2-{F}(V3,V5), halfadder-{F}(V6), P_not1-{F}(V6,V5), P_and2-{F}(V6,V7), P_out1-{F}(V7,V2) | abnormal-{T}(V0)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #1513: exists( #74, #1511 ), references = 1, size of lhs = 14:
% 20.35/20.53 halfadder-{F}(V0), P_in1-{F}(V0,V1), zero-{F}(V1), P_and2-{F}(V0,V2), and_ok-{F}(V2), halfadder-{F}(V3), P_and2-{F}(V3,V2), fulladder-{F}(V4), P_inc-{F}(V4,V5), one-{F}(V5), P_h1-{F}(V4,V6), fulladder-{F}(V7), P_or1-{F}(V7,V6), P_h1-{F}(V7,V3) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #1517: exists( #78, #1515 ), references = 2, size of lhs = 22:
% 20.35/20.53 P_a-{F}(V0), P_ina1-{F}(V0,V1), P_ina2-{F}(V0,V2), P_inb1-{F}(V0,V3), P_inb2-{F}(V0,V4), P_inc-{F}(V0,V5), P_out1-{F}(V0,V6), P_out2-{F}(V0,V7), P_outc-{F}(V0,V8), P_f2-{F}(V0,V9), P_or1-{F}(V9,V10), P_h1-{F}(V9,V11), halfadder-{F}(V11), P_in1-{F}(V11,V12), zero-{F}(V12), fulladder-{F}(V13), P_inc-{F}(V13,V14), one-{F}(V14), P_h1-{F}(V13,V15), fulladder-{F}(V16), P_or1-{F}(V16,V15), P_h1-{F}(V16,V11) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #1527: exists( #74, #1525 ), references = 1, size of lhs = 24:
% 20.35/20.53 fulladder-{F}(V0), P_in2-{F}(V0,V1), zero-{F}(V1), P_h1-{F}(V0,V2), halfadder-{F}(V2), P_a-{F}(V3), P_ina1-{F}(V3,V4), P_ina2-{F}(V3,V5), P_inb1-{F}(V3,V6), P_inb2-{F}(V3,V7), P_inc-{F}(V3,V8), P_out1-{F}(V3,V9), P_out2-{F}(V3,V10), P_outc-{F}(V3,V11), P_f2-{F}(V3,V12), P_h1-{F}(V12,V2), P_or1-{F}(V12,V13), fulladder-{F}(V14), P_inc-{F}(V14,V15), one-{F}(V15), P_h1-{F}(V14,V16), fulladder-{F}(V17), P_or1-{F}(V17,V16), P_h1-{F}(V17,V2) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #1533: exists( #85, #1531 ), references = 1, size of lhs = 15:
% 20.35/20.53 nbit_adder2-{F}(V0), P_inc-{F}(V0,V1), zero-{F}(V1), P_f1-{F}(V0,V2), fulladder-{F}(V2), fulladder-{F}(V3), P_in2-{F}(V3,V4), zero-{F}(V4), P_h1-{F}(V3,V5), or_ok-{F}(V5), P_h1-{F}(V2,V5), fulladder-{F}(V6), P_or1-{F}(V6,V5), P_outc-{F}(V6,V7), one-{F}(V7) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #1607: exists( #74, #1604 ), references = 1, size of lhs = 9:
% 20.35/20.53 halfadder-{F}(V0), P_in1-{F}(V0,V1), zero-{F}(V1), P_and2-{F}(V0,V2), halfadder-{F}(V3), P_and1-{F}(V3,V2), P_or1-{F}(V3,V4), P_out1-{F}(V4,V5), one-{F}(V5) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #1669: exists( #76, #1665 ), references = 4, size of lhs = 10:
% 20.35/20.53 fulladder-{F}(V0), P_h1-{F}(V0,V1), P_outc-{F}(V1,V2), zero-{F}(V2), P_or1-{F}(V0,V3), fulladder-{F}(V4), P_h2-{F}(V4,V3), P_h1-{F}(V4,V5), P_outs-{F}(V5,V6), one-{F}(V6) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #1710: exists( #75, #1704 ), references = 2, size of lhs = 18:
% 20.35/20.53 halfadder-{F}(V0), P_outc-{F}(V0,V1), P_and2-{F}(V0,V2), and_ok-{F}(V2), P_in1-{F}(V2,V3), zero-{F}(V3), fulladder-{F}(V4), P_in2-{F}(V4,V5), zero-{F}(V5), P_h1-{F}(V4,V6), or_ok-{F}(V6), fulladder-{F}(V7), P_or1-{F}(V7,V6), P_outc-{F}(V7,V8), one-{F}(V8), fulladder-{F}(V9), P_h1-{F}(V9,V6), P_inc-{F}(V9,V1) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #1711: exists( #75, #1705 ), references = 2, size of lhs = 14:
% 20.35/20.53 halfadder-{F}(V0), P_outc-{F}(V0,V1), P_and2-{F}(V0,V2), and_ok-{F}(V2), P_in1-{F}(V2,V3), zero-{F}(V3), fulladder-{F}(V4), P_inc-{F}(V4,V1), P_h1-{F}(V4,V5), or_ok-{F}(V5), P_in1-{F}(V5,V6), zero-{F}(V6), P_out1-{F}(V5,V7), one-{F}(V7) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #1712: exists( #75, #1706 ), references = 2, size of lhs = 16:
% 20.35/20.53 halfadder-{F}(V0), P_outc-{F}(V0,V1), P_and2-{F}(V0,V2), and_ok-{F}(V2), P_in1-{F}(V2,V3), zero-{F}(V3), fulladder-{F}(V4), P_outc-{F}(V4,V5), one-{F}(V5), P_or1-{F}(V4,V6), or_ok-{F}(V6), fulladder-{F}(V7), P_h1-{F}(V7,V6), P_inc-{F}(V7,V1), P_in1-{F}(V6,V8), zero-{F}(V8) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #1722: exists( #74, #1717 ), references = 1, size of lhs = 18:
% 20.35/20.53 halfadder-{F}(V0), P_in1-{F}(V0,V1), zero-{F}(V1), P_and2-{F}(V0,V2), and_ok-{F}(V2), halfadder-{F}(V3), P_and2-{F}(V3,V2), P_outc-{F}(V3,V4), fulladder-{F}(V5), P_outc-{F}(V5,V6), one-{F}(V6), P_or1-{F}(V5,V7), or_ok-{F}(V7), fulladder-{F}(V8), P_h1-{F}(V8,V7), P_inc-{F}(V8,V4), P_in1-{F}(V7,V9), zero-{F}(V9) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #1723: exists( #74, #1718 ), references = 1, size of lhs = 20:
% 20.35/20.53 halfadder-{F}(V0), P_in1-{F}(V0,V1), zero-{F}(V1), P_and2-{F}(V0,V2), and_ok-{F}(V2), halfadder-{F}(V3), P_and2-{F}(V3,V2), P_outc-{F}(V3,V4), fulladder-{F}(V5), P_in2-{F}(V5,V6), zero-{F}(V6), P_h1-{F}(V5,V7), or_ok-{F}(V7), fulladder-{F}(V8), P_or1-{F}(V8,V7), P_outc-{F}(V8,V9), one-{F}(V9), fulladder-{F}(V10), P_h1-{F}(V10,V7), P_inc-{F}(V10,V4) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #1724: exists( #74, #1716 ), references = 1, size of lhs = 16:
% 20.35/20.53 halfadder-{F}(V0), P_in1-{F}(V0,V1), zero-{F}(V1), P_and2-{F}(V0,V2), and_ok-{F}(V2), halfadder-{F}(V3), P_and2-{F}(V3,V2), P_outc-{F}(V3,V4), fulladder-{F}(V5), P_inc-{F}(V5,V4), P_h1-{F}(V5,V6), or_ok-{F}(V6), P_in1-{F}(V6,V7), zero-{F}(V7), P_out1-{F}(V6,V8), one-{F}(V8) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #1783: disj( #20, #15+#1030 ), references = 1, size of lhs = 25:
% 20.35/20.53 logic_or-{F}(V0), P_in1-{F}(V0,V1), zero-{F}(V1), P_in2-{F}(V0,V2), zero-{F}(V2), P_out1-{F}(V0,V3), nbit_adder2-{F}(V4), P_f1-{F}(V4,V5), fulladder-{F}(V5), P_f2-{F}(V4,V6), P_inc-{F}(V6,V7), P_or1-{F}(V5,V8), P_out1-{F}(V8,V3), fulladder-{F}(V9), P_in2-{F}(V9,V10), zero-{F}(V10), P_h1-{F}(V9,V11), or_ok-{F}(V11), fulladder-{F}(V12), P_or1-{F}(V12,V11), P_outc-{F}(V12,V13), one-{F}(V13), fulladder-{F}(V14), P_h1-{F}(V14,V11), P_inc-{F}(V14,V7) | abnormal-{T}(V0)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #1816: exists( #75, #1814 ), references = 2, size of lhs = 25:
% 20.35/20.53 halfadder-{F}(V0), P_outc-{F}(V0,V1), P_and2-{F}(V0,V2), and_ok-{F}(V2), P_in1-{F}(V2,V3), zero-{F}(V3), nbit_adder2-{F}(V4), P_f1-{F}(V4,V5), fulladder-{F}(V5), P_f2-{F}(V4,V6), P_inc-{F}(V6,V7), P_or1-{F}(V5,V8), P_out1-{F}(V8,V1), fulladder-{F}(V9), P_in2-{F}(V9,V10), zero-{F}(V10), P_h1-{F}(V9,V11), or_ok-{F}(V11), fulladder-{F}(V12), P_or1-{F}(V12,V11), P_outc-{F}(V12,V13), one-{F}(V13), fulladder-{F}(V14), P_h1-{F}(V14,V11), P_inc-{F}(V14,V7) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #1828: exists( #74, #1826 ), references = 1, size of lhs = 27:
% 20.35/20.53 halfadder-{F}(V0), P_in1-{F}(V0,V1), zero-{F}(V1), P_and2-{F}(V0,V2), and_ok-{F}(V2), halfadder-{F}(V3), P_and2-{F}(V3,V2), P_outc-{F}(V3,V4), nbit_adder2-{F}(V5), P_f1-{F}(V5,V6), fulladder-{F}(V6), P_f2-{F}(V5,V7), P_inc-{F}(V7,V8), P_or1-{F}(V6,V9), P_out1-{F}(V9,V4), fulladder-{F}(V10), P_in2-{F}(V10,V11), zero-{F}(V11), P_h1-{F}(V10,V12), or_ok-{F}(V12), fulladder-{F}(V13), P_or1-{F}(V13,V12), P_outc-{F}(V13,V14), one-{F}(V14), fulladder-{F}(V15), P_h1-{F}(V15,V12), P_inc-{F}(V15,V8) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #1918: exists( #75, #1912 ), references = 2, size of lhs = 19:
% 20.35/20.53 halfadder-{F}(V0), P_outc-{F}(V0,V1), P_and2-{F}(V0,V2), and_ok-{F}(V2), P_in1-{F}(V2,V3), zero-{F}(V3), fulladder-{F}(V4), P_in2-{F}(V4,V5), zero-{F}(V5), P_h1-{F}(V4,V6), or_ok-{F}(V6), fulladder-{F}(V7), P_or1-{F}(V7,V6), P_outc-{F}(V7,V8), one-{F}(V8), fulladder-{F}(V9), P_h1-{F}(V9,V6), P_inc-{F}(V9,V10), connection-{F}(V10,V1) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #1919: exists( #75, #1913 ), references = 2, size of lhs = 18:
% 20.35/20.53 halfadder-{F}(V0), P_outc-{F}(V0,V1), P_and2-{F}(V0,V2), and_ok-{F}(V2), P_in1-{F}(V2,V3), zero-{F}(V3), or_ok-{F}(V4), P_in2-{F}(V4,V1), P_in1-{F}(V4,V5), zero-{F}(V5), P_out1-{F}(V4,V6), nbit_adder2-{F}(V7), P_outc-{F}(V7,V8), one-{F}(V8), P_f2-{F}(V7,V9), fulladder-{F}(V9), P_or1-{F}(V9,V10), P_out1-{F}(V10,V6) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #1920: exists( #75, #1914 ), references = 2, size of lhs = 12:
% 20.35/20.53 halfadder-{F}(V0), P_outc-{F}(V0,V1), P_and2-{F}(V0,V2), and_ok-{F}(V2), P_in1-{F}(V2,V3), zero-{F}(V3), or_ok-{F}(V4), P_in2-{F}(V4,V1), P_in1-{F}(V4,V5), zero-{F}(V5), P_out1-{F}(V4,V6), one-{F}(V6) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #1930: exists( #74, #1926 ), references = 1, size of lhs = 21:
% 20.35/20.53 halfadder-{F}(V0), P_in1-{F}(V0,V1), zero-{F}(V1), P_and2-{F}(V0,V2), and_ok-{F}(V2), halfadder-{F}(V3), P_and2-{F}(V3,V2), P_outc-{F}(V3,V4), fulladder-{F}(V5), P_in2-{F}(V5,V6), zero-{F}(V6), P_h1-{F}(V5,V7), or_ok-{F}(V7), fulladder-{F}(V8), P_or1-{F}(V8,V7), P_outc-{F}(V8,V9), one-{F}(V9), fulladder-{F}(V10), P_h1-{F}(V10,V7), P_inc-{F}(V10,V11), connection-{F}(V11,V4) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #1931: exists( #74, #1924 ), references = 1, size of lhs = 20:
% 20.35/20.53 halfadder-{F}(V0), P_in1-{F}(V0,V1), zero-{F}(V1), P_and2-{F}(V0,V2), and_ok-{F}(V2), halfadder-{F}(V3), P_and2-{F}(V3,V2), P_outc-{F}(V3,V4), or_ok-{F}(V5), P_in2-{F}(V5,V4), P_in1-{F}(V5,V6), zero-{F}(V6), P_out1-{F}(V5,V7), nbit_adder2-{F}(V8), P_outc-{F}(V8,V9), one-{F}(V9), P_f2-{F}(V8,V10), fulladder-{F}(V10), P_or1-{F}(V10,V11), P_out1-{F}(V11,V7) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #1932: exists( #74, #1925 ), references = 1, size of lhs = 14:
% 20.35/20.53 halfadder-{F}(V0), P_in1-{F}(V0,V1), zero-{F}(V1), P_and2-{F}(V0,V2), and_ok-{F}(V2), halfadder-{F}(V3), P_and2-{F}(V3,V2), P_outc-{F}(V3,V4), or_ok-{F}(V5), P_in2-{F}(V5,V4), P_in1-{F}(V5,V6), zero-{F}(V6), P_out1-{F}(V5,V7), one-{F}(V7) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #1995: exists( #75, #1993 ), references = 2, size of lhs = 26:
% 20.35/20.53 halfadder-{F}(V0), P_outc-{F}(V0,V1), P_and2-{F}(V0,V2), and_ok-{F}(V2), P_in1-{F}(V2,V3), zero-{F}(V3), connection-{F}(V1,V4), nbit_adder2-{F}(V5), P_f1-{F}(V5,V6), fulladder-{F}(V6), P_f2-{F}(V5,V7), P_inc-{F}(V7,V8), P_or1-{F}(V6,V9), P_out1-{F}(V9,V4), fulladder-{F}(V10), P_in2-{F}(V10,V11), zero-{F}(V11), P_h1-{F}(V10,V12), or_ok-{F}(V12), fulladder-{F}(V13), P_or1-{F}(V13,V12), P_outc-{F}(V13,V14), one-{F}(V14), fulladder-{F}(V15), P_h1-{F}(V15,V12), P_inc-{F}(V15,V8) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2005: exists( #74, #2003 ), references = 1, size of lhs = 28:
% 20.35/20.53 halfadder-{F}(V0), P_in1-{F}(V0,V1), zero-{F}(V1), P_and2-{F}(V0,V2), and_ok-{F}(V2), halfadder-{F}(V3), P_and2-{F}(V3,V2), P_outc-{F}(V3,V4), connection-{F}(V4,V5), nbit_adder2-{F}(V6), P_f1-{F}(V6,V7), fulladder-{F}(V7), P_f2-{F}(V6,V8), P_inc-{F}(V8,V9), P_or1-{F}(V7,V10), P_out1-{F}(V10,V5), fulladder-{F}(V11), P_in2-{F}(V11,V12), zero-{F}(V12), P_h1-{F}(V11,V13), or_ok-{F}(V13), fulladder-{F}(V14), P_or1-{F}(V14,V13), P_outc-{F}(V14,V15), one-{F}(V15), fulladder-{F}(V16), P_h1-{F}(V16,V13), P_inc-{F}(V16,V9) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2088: exists( #75, #2082 ), references = 2, size of lhs = 20:
% 20.35/20.53 halfadder-{F}(V0), P_outc-{F}(V0,V1), P_and2-{F}(V0,V2), and_ok-{F}(V2), P_in1-{F}(V2,V3), zero-{F}(V3), connection-{F}(V1,V4), fulladder-{F}(V5), P_in2-{F}(V5,V6), zero-{F}(V6), P_h1-{F}(V5,V7), or_ok-{F}(V7), fulladder-{F}(V8), P_or1-{F}(V8,V7), P_outc-{F}(V8,V9), one-{F}(V9), fulladder-{F}(V10), P_h1-{F}(V10,V7), P_inc-{F}(V10,V11), connection-{F}(V11,V4) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2089: exists( #75, #2083 ), references = 2, size of lhs = 19:
% 20.35/20.53 halfadder-{F}(V0), P_outc-{F}(V0,V1), P_and2-{F}(V0,V2), and_ok-{F}(V2), P_in1-{F}(V2,V3), zero-{F}(V3), connection-{F}(V1,V4), or_ok-{F}(V5), P_in2-{F}(V5,V4), P_in1-{F}(V5,V6), zero-{F}(V6), P_out1-{F}(V5,V7), nbit_adder2-{F}(V8), P_outc-{F}(V8,V9), one-{F}(V9), P_f2-{F}(V8,V10), fulladder-{F}(V10), P_or1-{F}(V10,V11), P_out1-{F}(V11,V7) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2090: exists( #75, #2084 ), references = 2, size of lhs = 13:
% 20.35/20.53 halfadder-{F}(V0), P_outc-{F}(V0,V1), P_and2-{F}(V0,V2), and_ok-{F}(V2), P_in1-{F}(V2,V3), zero-{F}(V3), connection-{F}(V1,V4), or_ok-{F}(V5), P_in2-{F}(V5,V4), P_in1-{F}(V5,V6), zero-{F}(V6), P_out1-{F}(V5,V7), one-{F}(V7) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2100: exists( #74, #2096 ), references = 1, size of lhs = 22:
% 20.35/20.53 halfadder-{F}(V0), P_in1-{F}(V0,V1), zero-{F}(V1), P_and2-{F}(V0,V2), and_ok-{F}(V2), halfadder-{F}(V3), P_and2-{F}(V3,V2), P_outc-{F}(V3,V4), connection-{F}(V4,V5), fulladder-{F}(V6), P_in2-{F}(V6,V7), zero-{F}(V7), P_h1-{F}(V6,V8), or_ok-{F}(V8), fulladder-{F}(V9), P_or1-{F}(V9,V8), P_outc-{F}(V9,V10), one-{F}(V10), fulladder-{F}(V11), P_h1-{F}(V11,V8), P_inc-{F}(V11,V12), connection-{F}(V12,V5) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2101: exists( #74, #2094 ), references = 1, size of lhs = 21:
% 20.35/20.53 halfadder-{F}(V0), P_in1-{F}(V0,V1), zero-{F}(V1), P_and2-{F}(V0,V2), and_ok-{F}(V2), halfadder-{F}(V3), P_and2-{F}(V3,V2), P_outc-{F}(V3,V4), connection-{F}(V4,V5), or_ok-{F}(V6), P_in2-{F}(V6,V5), P_in1-{F}(V6,V7), zero-{F}(V7), P_out1-{F}(V6,V8), nbit_adder2-{F}(V9), P_outc-{F}(V9,V10), one-{F}(V10), P_f2-{F}(V9,V11), fulladder-{F}(V11), P_or1-{F}(V11,V12), P_out1-{F}(V12,V8) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2102: exists( #74, #2095 ), references = 1, size of lhs = 15:
% 20.35/20.53 halfadder-{F}(V0), P_in1-{F}(V0,V1), zero-{F}(V1), P_and2-{F}(V0,V2), and_ok-{F}(V2), halfadder-{F}(V3), P_and2-{F}(V3,V2), P_outc-{F}(V3,V4), connection-{F}(V4,V5), or_ok-{F}(V6), P_in2-{F}(V6,V5), P_in1-{F}(V6,V7), zero-{F}(V7), P_out1-{F}(V6,V8), one-{F}(V8) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2109: exists( #82, #2103 ), references = 2, size of lhs = 24:
% 20.35/20.53 fulladder-{F}(V0), P_h1-{F}(V0,V1), halfadder-{F}(V1), P_or1-{F}(V0,V2), P_in2-{F}(V2,V3), halfadder-{F}(V4), P_in1-{F}(V4,V5), zero-{F}(V5), P_and2-{F}(V4,V6), and_ok-{F}(V6), P_and2-{F}(V1,V6), fulladder-{F}(V7), P_in2-{F}(V7,V8), zero-{F}(V8), P_h1-{F}(V7,V9), or_ok-{F}(V9), fulladder-{F}(V10), P_or1-{F}(V10,V9), P_outc-{F}(V10,V11), one-{F}(V11), fulladder-{F}(V12), P_h1-{F}(V12,V9), P_inc-{F}(V12,V13), connection-{F}(V13,V3) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2110: exists( #82, #2104 ), references = 2, size of lhs = 23:
% 20.35/20.53 fulladder-{F}(V0), P_h1-{F}(V0,V1), halfadder-{F}(V1), P_or1-{F}(V0,V2), P_in2-{F}(V2,V3), halfadder-{F}(V4), P_in1-{F}(V4,V5), zero-{F}(V5), P_and2-{F}(V4,V6), and_ok-{F}(V6), P_and2-{F}(V1,V6), or_ok-{F}(V7), P_in2-{F}(V7,V3), P_in1-{F}(V7,V8), zero-{F}(V8), P_out1-{F}(V7,V9), nbit_adder2-{F}(V10), P_outc-{F}(V10,V11), one-{F}(V11), P_f2-{F}(V10,V12), fulladder-{F}(V12), P_or1-{F}(V12,V13), P_out1-{F}(V13,V9) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2111: exists( #82, #2105 ), references = 3, size of lhs = 17:
% 20.35/20.53 fulladder-{F}(V0), P_h1-{F}(V0,V1), halfadder-{F}(V1), P_or1-{F}(V0,V2), P_in2-{F}(V2,V3), halfadder-{F}(V4), P_in1-{F}(V4,V5), zero-{F}(V5), P_and2-{F}(V4,V6), and_ok-{F}(V6), P_and2-{F}(V1,V6), or_ok-{F}(V7), P_in2-{F}(V7,V3), P_in1-{F}(V7,V8), zero-{F}(V8), P_out1-{F}(V7,V9), one-{F}(V9) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2124: exists( #78, #2118 ), references = 1, size of lhs = 32:
% 20.35/20.53 P_a-{F}(V0), P_ina1-{F}(V0,V1), P_ina2-{F}(V0,V2), P_inb1-{F}(V0,V3), P_inb2-{F}(V0,V4), P_inc-{F}(V0,V5), P_out1-{F}(V0,V6), P_out2-{F}(V0,V7), P_outc-{F}(V0,V8), P_f2-{F}(V0,V9), P_or1-{F}(V9,V10), P_h1-{F}(V9,V11), halfadder-{F}(V11), fulladder-{F}(V12), P_h1-{F}(V12,V11), P_or1-{F}(V12,V13), P_in2-{F}(V13,V14), P_in1-{F}(V11,V15), zero-{F}(V15), fulladder-{F}(V16), P_in2-{F}(V16,V17), zero-{F}(V17), P_h1-{F}(V16,V18), or_ok-{F}(V18), fulladder-{F}(V19), P_or1-{F}(V19,V18), P_outc-{F}(V19,V20), one-{F}(V20), fulladder-{F}(V21), P_h1-{F}(V21,V18), P_inc-{F}(V21,V22), connection-{F}(V22,V14) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2125: exists( #78, #2119 ), references = 2, size of lhs = 31:
% 20.35/20.53 P_a-{F}(V0), P_ina1-{F}(V0,V1), P_ina2-{F}(V0,V2), P_inb1-{F}(V0,V3), P_inb2-{F}(V0,V4), P_inc-{F}(V0,V5), P_out1-{F}(V0,V6), P_out2-{F}(V0,V7), P_outc-{F}(V0,V8), P_f2-{F}(V0,V9), P_or1-{F}(V9,V10), P_h1-{F}(V9,V11), halfadder-{F}(V11), fulladder-{F}(V12), P_h1-{F}(V12,V11), P_or1-{F}(V12,V13), P_in2-{F}(V13,V14), P_in1-{F}(V11,V15), zero-{F}(V15), or_ok-{F}(V16), P_in2-{F}(V16,V14), P_in1-{F}(V16,V17), zero-{F}(V17), P_out1-{F}(V16,V18), nbit_adder2-{F}(V19), P_outc-{F}(V19,V20), one-{F}(V20), P_f2-{F}(V19,V21), fulladder-{F}(V21), P_or1-{F}(V21,V22), P_out1-{F}(V22,V18) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2126: exists( #78, #2120 ), references = 2, size of lhs = 25:
% 20.35/20.53 P_a-{F}(V0), P_ina1-{F}(V0,V1), P_ina2-{F}(V0,V2), P_inb1-{F}(V0,V3), P_inb2-{F}(V0,V4), P_inc-{F}(V0,V5), P_out1-{F}(V0,V6), P_out2-{F}(V0,V7), P_outc-{F}(V0,V8), P_f2-{F}(V0,V9), P_or1-{F}(V9,V10), P_h1-{F}(V9,V11), halfadder-{F}(V11), fulladder-{F}(V12), P_h1-{F}(V12,V11), P_or1-{F}(V12,V13), P_in2-{F}(V13,V14), P_in1-{F}(V11,V15), zero-{F}(V15), or_ok-{F}(V16), P_in2-{F}(V16,V14), P_in1-{F}(V16,V17), zero-{F}(V17), P_out1-{F}(V16,V18), one-{F}(V18) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2131: exists( #76, #2127 ), references = 2, size of lhs = 33:
% 20.35/20.53 fulladder-{F}(V0), P_inc-{F}(V0,V1), P_h1-{F}(V0,V2), P_a-{F}(V3), P_ina1-{F}(V3,V4), P_ina2-{F}(V3,V5), P_inb1-{F}(V3,V6), P_inb2-{F}(V3,V7), P_inc-{F}(V3,V8), P_out1-{F}(V3,V9), P_out2-{F}(V3,V10), P_outc-{F}(V3,V11), P_f2-{F}(V3,V12), P_or1-{F}(V12,V13), P_h1-{F}(V12,V14), halfadder-{F}(V14), fulladder-{F}(V15), P_h1-{F}(V15,V14), P_or1-{F}(V15,V2), P_in1-{F}(V14,V16), zero-{F}(V16), fulladder-{F}(V17), P_in2-{F}(V17,V18), zero-{F}(V18), P_h1-{F}(V17,V19), or_ok-{F}(V19), fulladder-{F}(V20), P_or1-{F}(V20,V19), P_outc-{F}(V20,V21), one-{F}(V21), fulladder-{F}(V22), P_h1-{F}(V22,V19), P_inc-{F}(V22,V1) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2145: exists( #74, #2143 ), references = 1, size of lhs = 35:
% 20.35/20.53 fulladder-{F}(V0), P_in2-{F}(V0,V1), zero-{F}(V1), P_h1-{F}(V0,V2), halfadder-{F}(V2), fulladder-{F}(V3), P_inc-{F}(V3,V4), P_h1-{F}(V3,V5), P_a-{F}(V6), P_ina1-{F}(V6,V7), P_ina2-{F}(V6,V8), P_inb1-{F}(V6,V9), P_inb2-{F}(V6,V10), P_inc-{F}(V6,V11), P_out1-{F}(V6,V12), P_out2-{F}(V6,V13), P_outc-{F}(V6,V14), P_f2-{F}(V6,V15), P_h1-{F}(V15,V2), P_or1-{F}(V15,V16), fulladder-{F}(V17), P_h1-{F}(V17,V2), P_or1-{F}(V17,V5), fulladder-{F}(V18), P_in2-{F}(V18,V19), zero-{F}(V19), P_h1-{F}(V18,V20), or_ok-{F}(V20), fulladder-{F}(V21), P_or1-{F}(V21,V20), P_outc-{F}(V21,V22), one-{F}(V22), fulladder-{F}(V23), P_h1-{F}(V23,V20), P_inc-{F}(V23,V4) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2148: mergings( V5 == V20; #2146 ), references = 1, size of lhs = 31:
% 20.35/20.53 fulladder-{F}(V0), P_in2-{F}(V0,V1), zero-{F}(V1), P_h1-{F}(V0,V2), halfadder-{F}(V2), P_a-{F}(V3), P_ina1-{F}(V3,V4), P_ina2-{F}(V3,V5), P_inb1-{F}(V3,V6), P_inb2-{F}(V3,V7), P_inc-{F}(V3,V8), P_out1-{F}(V3,V9), P_out2-{F}(V3,V10), P_outc-{F}(V3,V11), P_f2-{F}(V3,V12), P_h1-{F}(V12,V2), P_or1-{F}(V12,V13), fulladder-{F}(V14), P_h1-{F}(V14,V2), P_or1-{F}(V14,V15), or_ok-{F}(V15), fulladder-{F}(V16), P_h1-{F}(V16,V15), P_in2-{F}(V16,V17), zero-{F}(V17), fulladder-{F}(V18), P_or1-{F}(V18,V15), P_outc-{F}(V18,V19), one-{F}(V19), fulladder-{F}(V20), P_h1-{F}(V20,V15) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2168: exists( #82, #2166 ), references = 1, size of lhs = 13:
% 20.35/20.53 nbit_adder2-{F}(V0), P_f1-{F}(V0,V1), P_f2-{F}(V0,V2), P_inc-{F}(V2,V3), zero-{F}(V3), fulladder-{F}(V4), P_h1-{F}(V4,V1), P_or1-{F}(V4,V5), fulladder-{F}(V6), P_h2-{F}(V6,V5), P_h1-{F}(V6,V7), P_outs-{F}(V7,V8), one-{F}(V8) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2177: exists( #75, #2175 ), references = 3, size of lhs = 9:
% 20.35/20.53 and_ok-{F}(V0), P_in1-{F}(V0,V1), zero-{F}(V1), nbit_adder2-{F}(V2), P_outc-{F}(V2,V3), one-{F}(V3), P_f2-{F}(V2,V4), fulladder-{F}(V4), P_or1-{F}(V4,V0) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2187: exists( #74, #2185 ), references = 1, size of lhs = 11:
% 20.35/20.53 fulladder-{F}(V0), P_in1-{F}(V0,V1), zero-{F}(V1), P_h2-{F}(V0,V2), and_ok-{F}(V2), nbit_adder2-{F}(V3), P_outc-{F}(V3,V4), one-{F}(V4), P_f2-{F}(V3,V5), fulladder-{F}(V5), P_or1-{F}(V5,V2) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2206: exists( #76, #2126 ), references = 1, size of lhs = 23:
% 20.35/20.53 P_a-{F}(V0), P_ina1-{F}(V0,V1), P_ina2-{F}(V0,V2), P_inb1-{F}(V0,V3), P_inb2-{F}(V0,V4), P_inc-{F}(V0,V5), P_out1-{F}(V0,V6), P_out2-{F}(V0,V7), P_outc-{F}(V0,V8), P_f2-{F}(V0,V9), P_or1-{F}(V9,V10), P_h1-{F}(V9,V11), halfadder-{F}(V11), fulladder-{F}(V12), P_h1-{F}(V12,V11), P_or1-{F}(V12,V13), or_ok-{F}(V13), P_in1-{F}(V11,V14), zero-{F}(V14), P_in1-{F}(V13,V15), zero-{F}(V15), P_out1-{F}(V13,V16), one-{F}(V16) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2207: exists( #76, #2125 ), references = 1, size of lhs = 29:
% 20.35/20.53 P_a-{F}(V0), P_ina1-{F}(V0,V1), P_ina2-{F}(V0,V2), P_inb1-{F}(V0,V3), P_inb2-{F}(V0,V4), P_inc-{F}(V0,V5), P_out1-{F}(V0,V6), P_out2-{F}(V0,V7), P_outc-{F}(V0,V8), P_f2-{F}(V0,V9), P_or1-{F}(V9,V10), P_h1-{F}(V9,V11), halfadder-{F}(V11), fulladder-{F}(V12), P_h1-{F}(V12,V11), P_or1-{F}(V12,V13), or_ok-{F}(V13), P_in1-{F}(V11,V14), zero-{F}(V14), P_in1-{F}(V13,V15), zero-{F}(V15), P_out1-{F}(V13,V16), nbit_adder2-{F}(V17), P_outc-{F}(V17,V18), one-{F}(V18), P_f2-{F}(V17,V19), fulladder-{F}(V19), P_or1-{F}(V19,V20), P_out1-{F}(V20,V16) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2208: exists( #76, #2111 ), references = 1, size of lhs = 15:
% 20.35/20.53 fulladder-{F}(V0), P_h1-{F}(V0,V1), halfadder-{F}(V1), P_or1-{F}(V0,V2), or_ok-{F}(V2), halfadder-{F}(V3), P_in1-{F}(V3,V4), zero-{F}(V4), P_and2-{F}(V3,V5), and_ok-{F}(V5), P_and2-{F}(V1,V5), P_in1-{F}(V2,V6), zero-{F}(V6), P_out1-{F}(V2,V7), one-{F}(V7) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2210: exists( #75, #2204 ), references = 5, size of lhs = 27:
% 20.35/20.53 P_a-{F}(V0), P_ina1-{F}(V0,V1), P_ina2-{F}(V0,V2), P_inb1-{F}(V0,V3), P_inb2-{F}(V0,V4), P_inc-{F}(V0,V5), P_out1-{F}(V0,V6), P_out2-{F}(V0,V7), P_outc-{F}(V0,V8), P_f2-{F}(V0,V9), P_or1-{F}(V9,V10), P_h1-{F}(V9,V11), halfadder-{F}(V11), fulladder-{F}(V12), P_h1-{F}(V12,V11), P_or1-{F}(V12,V13), or_ok-{F}(V13), P_in1-{F}(V11,V14), zero-{F}(V14), P_in1-{F}(V13,V15), zero-{F}(V15), nbit_adder2-{F}(V16), P_outc-{F}(V16,V17), one-{F}(V17), P_f2-{F}(V16,V18), fulladder-{F}(V18), P_or1-{F}(V18,V13) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2220: exists( #74, #2218 ), references = 1, size of lhs = 29:
% 20.35/20.53 fulladder-{F}(V0), P_in1-{F}(V0,V1), zero-{F}(V1), P_h2-{F}(V0,V2), or_ok-{F}(V2), P_a-{F}(V3), P_ina1-{F}(V3,V4), P_ina2-{F}(V3,V5), P_inb1-{F}(V3,V6), P_inb2-{F}(V3,V7), P_inc-{F}(V3,V8), P_out1-{F}(V3,V9), P_out2-{F}(V3,V10), P_outc-{F}(V3,V11), P_f2-{F}(V3,V12), P_or1-{F}(V12,V13), P_h1-{F}(V12,V14), halfadder-{F}(V14), fulladder-{F}(V15), P_h1-{F}(V15,V14), P_or1-{F}(V15,V2), P_in1-{F}(V14,V16), zero-{F}(V16), nbit_adder2-{F}(V17), P_outc-{F}(V17,V18), one-{F}(V18), P_f2-{F}(V17,V19), fulladder-{F}(V19), P_or1-{F}(V19,V2) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2225: mergings( V2 == V19; #2223 ), references = 1, size of lhs = 30:
% 20.35/20.53 zero-{F}(V0), halfadder-{F}(V1), fulladder-{F}(V2), P_in1-{F}(V2,V3), zero-{F}(V3), P_h2-{F}(V2,V4), or_ok-{F}(V4), P_a-{F}(V5), P_ina1-{F}(V5,V6), P_ina2-{F}(V5,V7), P_inb1-{F}(V5,V8), P_inb2-{F}(V5,V9), P_inc-{F}(V5,V10), P_out1-{F}(V5,V11), P_out2-{F}(V5,V12), P_outc-{F}(V5,V13), P_f2-{F}(V5,V14), P_h1-{F}(V14,V1), P_or1-{F}(V14,V15), fulladder-{F}(V16), P_h1-{F}(V16,V1), P_or1-{F}(V16,V4), nbit_adder2-{F}(V17), P_ina1-{F}(V17,V0), P_f1-{F}(V17,V1), P_outc-{F}(V17,V18), one-{F}(V18), P_f2-{F}(V17,V19), fulladder-{F}(V19), P_or1-{F}(V19,V4) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2243: exists( #76, #2241 ), references = 3, size of lhs = 8:
% 20.35/20.53 nbit_adder2-{F}(V0), P_inb1-{F}(V0,V1), zero-{F}(V1), P_f1-{F}(V0,V2), fulladder-{F}(V3), P_h1-{F}(V3,V2), P_inc-{F}(V3,V4), one-{F}(V4) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2272: exists( #74, #2270 ), references = 1, size of lhs = 30:
% 20.35/20.53 halfadder-{F}(V0), P_and2-{F}(V0,V1), P_out1-{F}(V1,V2), zero-{F}(V2), P_not1-{F}(V0,V3), or_ok-{F}(V3), P_a-{F}(V4), P_ina1-{F}(V4,V5), P_ina2-{F}(V4,V6), P_inb1-{F}(V4,V7), P_inb2-{F}(V4,V8), P_inc-{F}(V4,V9), P_out1-{F}(V4,V10), P_out2-{F}(V4,V11), P_outc-{F}(V4,V12), P_f2-{F}(V4,V13), P_or1-{F}(V13,V14), P_h1-{F}(V13,V15), halfadder-{F}(V15), fulladder-{F}(V16), P_h1-{F}(V16,V15), P_or1-{F}(V16,V3), P_in1-{F}(V15,V17), zero-{F}(V17), nbit_adder2-{F}(V18), P_outc-{F}(V18,V19), one-{F}(V19), P_f2-{F}(V18,V20), fulladder-{F}(V20), P_or1-{F}(V20,V3) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2285: exists( #74, #2283 ), references = 4, size of lhs = 30:
% 20.35/20.53 fulladder-{F}(V0), P_h2-{F}(V0,V1), P_outc-{F}(V1,V2), zero-{F}(V2), P_or1-{F}(V0,V3), or_ok-{F}(V3), P_a-{F}(V4), P_ina1-{F}(V4,V5), P_ina2-{F}(V4,V6), P_inb1-{F}(V4,V7), P_inb2-{F}(V4,V8), P_inc-{F}(V4,V9), P_out1-{F}(V4,V10), P_out2-{F}(V4,V11), P_outc-{F}(V4,V12), P_f2-{F}(V4,V13), P_or1-{F}(V13,V14), P_h1-{F}(V13,V15), halfadder-{F}(V15), fulladder-{F}(V16), P_h1-{F}(V16,V15), P_or1-{F}(V16,V3), P_in1-{F}(V15,V17), zero-{F}(V17), nbit_adder2-{F}(V18), P_outc-{F}(V18,V19), one-{F}(V19), P_f2-{F}(V18,V20), fulladder-{F}(V20), P_or1-{F}(V20,V3) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2291: mergings( V2 == V21, V3 == V23; #2288 ), references = 2, size of lhs = 31:
% 20.35/20.53 zero-{F}(V0), fulladder-{F}(V1), P_h2-{F}(V1,V2), P_or1-{F}(V1,V3), or_ok-{F}(V3), P_a-{F}(V4), P_ina1-{F}(V4,V5), P_ina2-{F}(V4,V6), P_inb1-{F}(V4,V7), P_inb2-{F}(V4,V8), P_inc-{F}(V4,V9), P_out1-{F}(V4,V10), P_out2-{F}(V4,V11), P_outc-{F}(V4,V12), P_f2-{F}(V4,V13), P_or1-{F}(V13,V14), P_h1-{F}(V13,V15), halfadder-{F}(V15), fulladder-{F}(V16), P_h1-{F}(V16,V15), P_or1-{F}(V16,V3), P_in1-{F}(V15,V17), zero-{F}(V17), nbit_adder2-{F}(V18), P_f1-{F}(V18,V2), P_outc-{F}(V18,V19), one-{F}(V19), P_f2-{F}(V18,V20), P_inc-{F}(V20,V0), fulladder-{F}(V20), P_or1-{F}(V20,V3) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2311: mergings( V2 == V23, V0 == V7; #2308 ), references = 2, size of lhs = 35:
% 20.35/20.53 zero-{F}(V0), fulladder-{F}(V1), P_h1-{F}(V1,V2), P_inc-{F}(V1,V3), fulladder-{F}(V4), P_h2-{F}(V4,V2), P_or1-{F}(V4,V5), or_ok-{F}(V5), P_a-{F}(V6), P_ina1-{F}(V6,V7), P_ina2-{F}(V6,V8), P_inb1-{F}(V6,V9), P_inb2-{F}(V6,V10), P_inc-{F}(V6,V11), P_out1-{F}(V6,V12), P_out2-{F}(V6,V13), P_outc-{F}(V6,V14), P_f2-{F}(V6,V15), P_or1-{F}(V15,V16), P_h1-{F}(V15,V17), halfadder-{F}(V17), fulladder-{F}(V18), P_h1-{F}(V18,V17), P_or1-{F}(V18,V5), P_in1-{F}(V17,V19), zero-{F}(V19), nbit_adder2-{F}(V20), P_inb1-{F}(V20,V0), P_f1-{F}(V20,V2), P_outc-{F}(V20,V21), one-{F}(V21), P_f2-{F}(V20,V22), fulladder-{F}(V22), P_or1-{F}(V22,V5), P_inc-{F}(V22,V3) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2317: mergings( V2 == V22, V0 == V6; #2314 ), references = 1, size of lhs = 35:
% 20.35/20.53 zero-{F}(V0), halfadder-{F}(V1), zero-{F}(V2), fulladder-{F}(V3), P_h1-{F}(V3,V1), P_inc-{F}(V3,V4), fulladder-{F}(V5), P_h2-{F}(V5,V1), P_or1-{F}(V5,V6), or_ok-{F}(V6), P_a-{F}(V7), P_ina1-{F}(V7,V8), P_ina2-{F}(V7,V9), P_inb1-{F}(V7,V10), P_inb2-{F}(V7,V11), P_inc-{F}(V7,V12), P_out1-{F}(V7,V13), P_out2-{F}(V7,V14), P_outc-{F}(V7,V15), P_f2-{F}(V7,V16), P_h1-{F}(V16,V1), P_or1-{F}(V16,V17), fulladder-{F}(V18), P_h1-{F}(V18,V1), P_or1-{F}(V18,V6), nbit_adder2-{F}(V19), P_ina1-{F}(V19,V0), P_inb1-{F}(V19,V2), P_f1-{F}(V19,V1), P_outc-{F}(V19,V20), one-{F}(V20), P_f2-{F}(V19,V21), fulladder-{F}(V21), P_or1-{F}(V21,V6), P_inc-{F}(V21,V4) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2321: mergings( V2 == V21, V4 == V6; #2318 ), references = 1, size of lhs = 32:
% 20.35/20.53 zero-{F}(V0), halfadder-{F}(V1), zero-{F}(V2), fulladder-{F}(V3), P_h2-{F}(V3,V1), P_or1-{F}(V3,V4), or_ok-{F}(V4), P_a-{F}(V5), P_ina1-{F}(V5,V6), P_ina2-{F}(V5,V7), P_inb1-{F}(V5,V8), P_inb2-{F}(V5,V9), P_inc-{F}(V5,V10), P_out1-{F}(V5,V11), P_out2-{F}(V5,V12), P_outc-{F}(V5,V13), P_f2-{F}(V5,V14), P_h1-{F}(V14,V1), P_or1-{F}(V14,V15), fulladder-{F}(V16), P_h1-{F}(V16,V1), P_or1-{F}(V16,V4), nbit_adder2-{F}(V17), P_ina1-{F}(V17,V0), P_inb1-{F}(V17,V2), P_f1-{F}(V17,V1), P_outc-{F}(V17,V18), one-{F}(V18), P_f2-{F}(V17,V19), P_h1-{F}(V19,V1), fulladder-{F}(V19), P_or1-{F}(V19,V4) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2337: exists( #74, #2333 ), references = 1, size of lhs = 12:
% 20.35/20.53 halfadder-{F}(V0), P_or1-{F}(V0,V1), P_out1-{F}(V1,V2), zero-{F}(V2), P_and1-{F}(V0,V3), and_ok-{F}(V3), nbit_adder2-{F}(V4), P_outc-{F}(V4,V5), one-{F}(V5), P_f2-{F}(V4,V6), fulladder-{F}(V6), P_or1-{F}(V6,V3) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2338: exists( #74, #2334 ), references = 1, size of lhs = 30:
% 20.35/20.53 halfadder-{F}(V0), P_or1-{F}(V0,V1), P_out1-{F}(V1,V2), zero-{F}(V2), P_and1-{F}(V0,V3), or_ok-{F}(V3), P_a-{F}(V4), P_ina1-{F}(V4,V5), P_ina2-{F}(V4,V6), P_inb1-{F}(V4,V7), P_inb2-{F}(V4,V8), P_inc-{F}(V4,V9), P_out1-{F}(V4,V10), P_out2-{F}(V4,V11), P_outc-{F}(V4,V12), P_f2-{F}(V4,V13), P_or1-{F}(V13,V14), P_h1-{F}(V13,V15), halfadder-{F}(V15), fulladder-{F}(V16), P_h1-{F}(V16,V15), P_or1-{F}(V16,V3), P_in1-{F}(V15,V17), zero-{F}(V17), nbit_adder2-{F}(V18), P_outc-{F}(V18,V19), one-{F}(V19), P_f2-{F}(V18,V20), fulladder-{F}(V20), P_or1-{F}(V20,V3) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2362: exists( #75, #2356 ), references = 1, size of lhs = 10:
% 20.35/20.53 halfadder-{F}(V0), P_outs-{F}(V0,V1), zero-{F}(V1), P_and1-{F}(V0,V2), nbit_adder2-{F}(V3), P_outc-{F}(V3,V4), one-{F}(V4), P_f2-{F}(V3,V5), fulladder-{F}(V5), P_or1-{F}(V5,V2) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2363: exists( #75, #2357 ), references = 1, size of lhs = 7:
% 20.35/20.53 halfadder-{F}(V0), P_outs-{F}(V0,V1), zero-{F}(V1), P_and1-{F}(V0,V2), or_ok-{F}(V2), P_in1-{F}(V2,V3), one-{F}(V3) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2380: exists( #75, #2378 ), references = 1, size of lhs = 15:
% 20.35/20.53 halfadder-{F}(V0), P_outs-{F}(V0,V1), P_and1-{F}(V0,V2), or_ok-{F}(V2), P_in1-{F}(V2,V3), one-{F}(V3), fulladder-{F}(V4), P_h1-{F}(V4,V5), P_outc-{F}(V5,V6), zero-{F}(V6), P_or1-{F}(V4,V7), fulladder-{F}(V8), P_h2-{F}(V8,V7), P_h1-{F}(V8,V9), P_outs-{F}(V9,V1) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2394: exists( #75, #2390 ), references = 1, size of lhs = 16:
% 20.35/20.53 fulladder-{F}(V0), P_outc-{F}(V0,V1), one-{F}(V1), P_or1-{F}(V0,V2), halfadder-{F}(V3), P_and1-{F}(V3,V2), P_outs-{F}(V3,V4), fulladder-{F}(V5), P_h1-{F}(V5,V6), P_outc-{F}(V6,V7), zero-{F}(V7), P_or1-{F}(V5,V8), fulladder-{F}(V9), P_h2-{F}(V9,V8), P_h1-{F}(V9,V10), P_outs-{F}(V10,V4) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2416: exists( #75, #2410 ), references = 1, size of lhs = 19:
% 20.35/20.53 fulladder-{F}(V0), P_outc-{F}(V0,V1), one-{F}(V1), P_or1-{F}(V0,V2), halfadder-{F}(V3), P_and1-{F}(V3,V2), P_outs-{F}(V3,V4), nbit_adder2-{F}(V5), P_inc-{F}(V5,V6), zero-{F}(V6), P_f1-{F}(V5,V7), fulladder-{F}(V7), P_h1-{F}(V7,V8), fulladder-{F}(V9), P_outs-{F}(V9,V4), P_h2-{F}(V9,V10), fulladder-{F}(V11), P_h1-{F}(V11,V10), P_h2-{F}(V11,V8) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2417: exists( #75, #2411 ), references = 1, size of lhs = 23:
% 20.35/20.53 fulladder-{F}(V0), P_outc-{F}(V0,V1), one-{F}(V1), P_or1-{F}(V0,V2), halfadder-{F}(V3), P_and1-{F}(V3,V2), P_outs-{F}(V3,V4), fulladder-{F}(V5), P_in2-{F}(V5,V6), zero-{F}(V6), P_h1-{F}(V5,V7), fulladder-{F}(V8), P_outs-{F}(V8,V4), P_h2-{F}(V8,V9), fulladder-{F}(V10), P_h1-{F}(V10,V9), P_h2-{F}(V10,V11), fulladder-{F}(V12), P_or1-{F}(V12,V7), P_h2-{F}(V12,V13), fulladder-{F}(V14), P_h1-{F}(V14,V13), P_or1-{F}(V14,V11) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2437: exists( #76, #2431 ), references = 2, size of lhs = 8:
% 20.35/20.53 fulladder-{F}(V0), P_h1-{F}(V0,V1), P_outc-{F}(V1,V2), zero-{F}(V2), P_or1-{F}(V0,V3), and_ok-{F}(V3), P_out1-{F}(V3,V4), one-{F}(V4) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2438: exists( #76, #2432 ), references = 2, size of lhs = 14:
% 20.35/20.53 fulladder-{F}(V0), P_h1-{F}(V0,V1), P_outc-{F}(V1,V2), P_or1-{F}(V0,V3), and_ok-{F}(V3), P_out1-{F}(V3,V4), one-{F}(V4), nbit_adder2-{F}(V5), P_inb1-{F}(V5,V6), zero-{F}(V6), P_f1-{F}(V5,V7), fulladder-{F}(V8), P_h1-{F}(V8,V7), P_inc-{F}(V8,V2) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2439: exists( #76, #2433 ), references = 2, size of lhs = 17:
% 20.35/20.53 fulladder-{F}(V0), P_h1-{F}(V0,V1), P_outc-{F}(V1,V2), P_or1-{F}(V0,V3), and_ok-{F}(V3), P_out1-{F}(V3,V4), one-{F}(V4), fulladder-{F}(V5), P_in1-{F}(V5,V6), zero-{F}(V6), P_h2-{F}(V5,V7), fulladder-{F}(V8), P_outc-{F}(V8,V2), P_or1-{F}(V8,V9), halfadder-{F}(V10), P_and2-{F}(V10,V9), P_not1-{F}(V10,V7) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2449: exists( #75, #2443 ), references = 2, size of lhs = 10:
% 20.35/20.53 fulladder-{F}(V0), P_outc-{F}(V0,V1), one-{F}(V1), P_or1-{F}(V0,V2), and_ok-{F}(V2), fulladder-{F}(V3), P_or1-{F}(V3,V2), P_h1-{F}(V3,V4), P_outc-{F}(V4,V5), zero-{F}(V5) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2450: exists( #75, #2444 ), references = 1, size of lhs = 16:
% 20.35/20.53 fulladder-{F}(V0), P_outc-{F}(V0,V1), one-{F}(V1), P_or1-{F}(V0,V2), and_ok-{F}(V2), fulladder-{F}(V3), P_or1-{F}(V3,V2), P_h1-{F}(V3,V4), P_outc-{F}(V4,V5), nbit_adder2-{F}(V6), P_inb1-{F}(V6,V7), zero-{F}(V7), P_f1-{F}(V6,V8), fulladder-{F}(V9), P_h1-{F}(V9,V8), P_inc-{F}(V9,V5) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2451: exists( #75, #2445 ), references = 1, size of lhs = 19:
% 20.35/20.53 fulladder-{F}(V0), P_outc-{F}(V0,V1), one-{F}(V1), P_or1-{F}(V0,V2), and_ok-{F}(V2), fulladder-{F}(V3), P_or1-{F}(V3,V2), P_h1-{F}(V3,V4), P_outc-{F}(V4,V5), fulladder-{F}(V6), P_in1-{F}(V6,V7), zero-{F}(V7), P_h2-{F}(V6,V8), fulladder-{F}(V9), P_outc-{F}(V9,V5), P_or1-{F}(V9,V10), halfadder-{F}(V11), P_and2-{F}(V11,V10), P_not1-{F}(V11,V8) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2453: exists( #82, #2448 ), references = 1, size of lhs = 17:
% 20.35/20.53 fulladder-{F}(V0), P_outc-{F}(V0,V1), one-{F}(V1), P_or1-{F}(V0,V2), and_ok-{F}(V2), fulladder-{F}(V3), P_or1-{F}(V3,V2), P_h1-{F}(V3,V4), fulladder-{F}(V4), fulladder-{F}(V5), P_in1-{F}(V5,V6), zero-{F}(V6), P_h2-{F}(V5,V7), P_or1-{F}(V4,V8), halfadder-{F}(V9), P_and2-{F}(V9,V8), P_not1-{F}(V9,V7) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2457: exists( #82, #2455 ), references = 1, size of lhs = 13:
% 20.35/20.53 nbit_adder2-{F}(V0), P_f1-{F}(V0,V1), P_f2-{F}(V0,V2), P_inc-{F}(V2,V3), zero-{F}(V3), fulladder-{F}(V4), P_outc-{F}(V4,V5), one-{F}(V5), P_or1-{F}(V4,V6), and_ok-{F}(V6), fulladder-{F}(V7), P_or1-{F}(V7,V6), P_h1-{F}(V7,V1) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2486: exists( #82, #2482 ), references = 1, size of lhs = 33:
% 20.35/20.53 fulladder-{F}(V0), P_h1-{F}(V0,V1), P_or1-{F}(V0,V2), P_in2-{F}(V2,V3), zero-{F}(V3), fulladder-{F}(V4), P_h2-{F}(V4,V1), P_or1-{F}(V4,V5), or_ok-{F}(V5), P_a-{F}(V6), P_ina1-{F}(V6,V7), P_ina2-{F}(V6,V8), P_inb1-{F}(V6,V9), P_inb2-{F}(V6,V10), P_inc-{F}(V6,V11), P_out1-{F}(V6,V12), P_out2-{F}(V6,V13), P_outc-{F}(V6,V14), P_f2-{F}(V6,V15), P_or1-{F}(V15,V16), P_h1-{F}(V15,V17), halfadder-{F}(V17), fulladder-{F}(V18), P_h1-{F}(V18,V17), P_or1-{F}(V18,V5), P_in1-{F}(V17,V19), zero-{F}(V19), nbit_adder2-{F}(V20), P_outc-{F}(V20,V21), one-{F}(V21), P_f2-{F}(V20,V22), fulladder-{F}(V22), P_or1-{F}(V22,V5) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2495: exists( #82, #2490 ), references = 3, size of lhs = 32:
% 20.35/20.53 halfadder-{F}(V0), P_and2-{F}(V0,V1), P_out1-{F}(V1,V2), zero-{F}(V2), fulladder-{F}(V3), P_h2-{F}(V3,V0), P_or1-{F}(V3,V4), or_ok-{F}(V4), P_a-{F}(V5), P_ina1-{F}(V5,V6), P_ina2-{F}(V5,V7), P_inb1-{F}(V5,V8), P_inb2-{F}(V5,V9), P_inc-{F}(V5,V10), P_out1-{F}(V5,V11), P_out2-{F}(V5,V12), P_outc-{F}(V5,V13), P_f2-{F}(V5,V14), P_or1-{F}(V14,V15), P_h1-{F}(V14,V16), halfadder-{F}(V16), fulladder-{F}(V17), P_h1-{F}(V17,V16), P_or1-{F}(V17,V4), P_in1-{F}(V16,V18), zero-{F}(V18), nbit_adder2-{F}(V19), P_outc-{F}(V19,V20), one-{F}(V20), P_f2-{F}(V19,V21), fulladder-{F}(V21), P_or1-{F}(V21,V4) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2496: exists( #82, #2492 ), references = 3, size of lhs = 9:
% 20.35/20.53 fulladder-{F}(V0), P_h2-{F}(V0,V1), halfadder-{F}(V1), P_or1-{F}(V0,V2), P_in1-{F}(V2,V3), one-{F}(V3), P_and2-{F}(V1,V4), P_out1-{F}(V4,V5), zero-{F}(V5) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2506: exists( #75, #2501 ), references = 2, size of lhs = 35:
% 20.35/20.53 halfadder-{F}(V0), P_and2-{F}(V0,V1), P_not1-{F}(V0,V2), P_in1-{F}(V2,V3), zero-{F}(V3), halfadder-{F}(V4), P_and2-{F}(V4,V1), fulladder-{F}(V5), P_h2-{F}(V5,V4), P_or1-{F}(V5,V6), or_ok-{F}(V6), P_a-{F}(V7), P_ina1-{F}(V7,V8), P_ina2-{F}(V7,V9), P_inb1-{F}(V7,V10), P_inb2-{F}(V7,V11), P_inc-{F}(V7,V12), P_out1-{F}(V7,V13), P_out2-{F}(V7,V14), P_outc-{F}(V7,V15), P_f2-{F}(V7,V16), P_or1-{F}(V16,V17), P_h1-{F}(V16,V18), halfadder-{F}(V18), fulladder-{F}(V19), P_h1-{F}(V19,V18), P_or1-{F}(V19,V6), P_in1-{F}(V18,V20), zero-{F}(V20), nbit_adder2-{F}(V21), P_outc-{F}(V21,V22), one-{F}(V22), P_f2-{F}(V21,V23), fulladder-{F}(V23), P_or1-{F}(V23,V6) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2507: exists( #75, #2502 ), references = 2, size of lhs = 12:
% 20.35/20.53 halfadder-{F}(V0), P_and2-{F}(V0,V1), P_not1-{F}(V0,V2), P_in1-{F}(V2,V3), zero-{F}(V3), fulladder-{F}(V4), P_h2-{F}(V4,V5), halfadder-{F}(V5), P_and2-{F}(V5,V1), P_or1-{F}(V4,V6), P_in1-{F}(V6,V7), one-{F}(V7) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2514: disj( #26, #21+#4 ), references = 1, size of lhs = 5:
% 20.35/20.53 logic_not-{F}(V0), P_in1-{F}(V0,V1), zero-{F}(V1), P_out1-{F}(V0,V2), zero-{F}(V2) | abnormal-{T}(V0)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2515: disj( #26, #21+#2243 ), references = 1, size of lhs = 11:
% 20.35/20.53 logic_not-{F}(V0), P_in1-{F}(V0,V1), zero-{F}(V1), P_out1-{F}(V0,V2), nbit_adder2-{F}(V3), P_inb1-{F}(V3,V4), zero-{F}(V4), P_f1-{F}(V3,V5), fulladder-{F}(V6), P_h1-{F}(V6,V5), P_inc-{F}(V6,V2) | abnormal-{T}(V0)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2516: disj( #26, #21+#1438 ), references = 1, size of lhs = 12:
% 20.35/20.53 logic_not-{F}(V0), P_in1-{F}(V0,V1), zero-{F}(V1), P_out1-{F}(V0,V2), fulladder-{F}(V3), P_inc-{F}(V3,V4), zero-{F}(V4), P_h1-{F}(V3,V5), halfadder-{F}(V6), P_and1-{F}(V6,V5), P_not1-{F}(V6,V7), P_out1-{F}(V7,V2) | abnormal-{T}(V0)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2530: disj( #20, input ), references = 1, size of lhs = 2:
% 20.35/20.53 logic_or-{F}(V0), and_ok-{F}(V0) | or_ok-{T}(V0)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2539: exists( #74, #2534 ), references = 1, size of lhs = 37:
% 20.35/20.53 halfadder-{F}(V0), P_in1-{F}(V0,V1), zero-{F}(V1), P_and2-{F}(V0,V2), halfadder-{F}(V3), P_not1-{F}(V3,V2), P_and2-{F}(V3,V4), halfadder-{F}(V5), P_and2-{F}(V5,V4), fulladder-{F}(V6), P_h2-{F}(V6,V5), P_or1-{F}(V6,V7), or_ok-{F}(V7), P_a-{F}(V8), P_ina1-{F}(V8,V9), P_ina2-{F}(V8,V10), P_inb1-{F}(V8,V11), P_inb2-{F}(V8,V12), P_inc-{F}(V8,V13), P_out1-{F}(V8,V14), P_out2-{F}(V8,V15), P_outc-{F}(V8,V16), P_f2-{F}(V8,V17), P_or1-{F}(V17,V18), P_h1-{F}(V17,V19), halfadder-{F}(V19), fulladder-{F}(V20), P_h1-{F}(V20,V19), P_or1-{F}(V20,V7), P_in1-{F}(V19,V21), zero-{F}(V21), nbit_adder2-{F}(V22), P_outc-{F}(V22,V23), one-{F}(V23), P_f2-{F}(V22,V24), fulladder-{F}(V24), P_or1-{F}(V24,V7) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2540: exists( #74, #2535 ), references = 1, size of lhs = 14:
% 20.35/20.53 halfadder-{F}(V0), P_in1-{F}(V0,V1), zero-{F}(V1), P_and2-{F}(V0,V2), halfadder-{F}(V3), P_not1-{F}(V3,V2), P_and2-{F}(V3,V4), fulladder-{F}(V5), P_h2-{F}(V5,V6), halfadder-{F}(V6), P_and2-{F}(V6,V4), P_or1-{F}(V5,V7), P_in1-{F}(V7,V8), one-{F}(V8) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2542: disj( #12, input ), references = 1, size of lhs = 16:
% 20.35/20.53 logic_and-{F}(V0), P_a-{F}(V1), P_ina1-{F}(V1,V2), P_ina2-{F}(V1,V3), P_inb1-{F}(V1,V4), P_inb2-{F}(V1,V5), P_inc-{F}(V1,V6), P_out1-{F}(V1,V7), P_out2-{F}(V1,V8), P_outc-{F}(V1,V9), P_f2-{F}(V1,V10), P_or1-{F}(V10,V11), P_h1-{F}(V10,V12), P_and2-{F}(V12,V13), P_h2-{F}(V10,V14), P_and2-{F}(V14,V0) | and_ok-{T}(V0)
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2556: exists( #75, #2552 ), references = 2, size of lhs = 33:
% 20.35/20.53 and_ok-{F}(V0), P_in1-{F}(V0,V1), zero-{F}(V1), halfadder-{F}(V2), P_and2-{F}(V2,V0), fulladder-{F}(V3), P_h2-{F}(V3,V2), P_or1-{F}(V3,V4), or_ok-{F}(V4), P_a-{F}(V5), P_ina1-{F}(V5,V6), P_ina2-{F}(V5,V7), P_inb1-{F}(V5,V8), P_inb2-{F}(V5,V9), P_inc-{F}(V5,V10), P_out1-{F}(V5,V11), P_out2-{F}(V5,V12), P_outc-{F}(V5,V13), P_f2-{F}(V5,V14), P_or1-{F}(V14,V15), P_h1-{F}(V14,V16), halfadder-{F}(V16), fulladder-{F}(V17), P_h1-{F}(V17,V16), P_or1-{F}(V17,V4), P_in1-{F}(V16,V18), zero-{F}(V18), nbit_adder2-{F}(V19), P_outc-{F}(V19,V20), one-{F}(V20), P_f2-{F}(V19,V21), fulladder-{F}(V21), P_or1-{F}(V21,V4) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2557: exists( #75, #2553 ), references = 2, size of lhs = 10:
% 20.35/20.53 and_ok-{F}(V0), P_in1-{F}(V0,V1), zero-{F}(V1), fulladder-{F}(V2), P_h2-{F}(V2,V3), halfadder-{F}(V3), P_and2-{F}(V3,V0), P_or1-{F}(V2,V4), P_in1-{F}(V4,V5), one-{F}(V5) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2566: exists( #74, #2561 ), references = 1, size of lhs = 35:
% 20.35/20.53 halfadder-{F}(V0), P_in1-{F}(V0,V1), zero-{F}(V1), P_and2-{F}(V0,V2), and_ok-{F}(V2), halfadder-{F}(V3), P_and2-{F}(V3,V2), fulladder-{F}(V4), P_h2-{F}(V4,V3), P_or1-{F}(V4,V5), or_ok-{F}(V5), P_a-{F}(V6), P_ina1-{F}(V6,V7), P_ina2-{F}(V6,V8), P_inb1-{F}(V6,V9), P_inb2-{F}(V6,V10), P_inc-{F}(V6,V11), P_out1-{F}(V6,V12), P_out2-{F}(V6,V13), P_outc-{F}(V6,V14), P_f2-{F}(V6,V15), P_or1-{F}(V15,V16), P_h1-{F}(V15,V17), halfadder-{F}(V17), fulladder-{F}(V18), P_h1-{F}(V18,V17), P_or1-{F}(V18,V5), P_in1-{F}(V17,V19), zero-{F}(V19), nbit_adder2-{F}(V20), P_outc-{F}(V20,V21), one-{F}(V21), P_f2-{F}(V20,V22), fulladder-{F}(V22), P_or1-{F}(V22,V5) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2567: exists( #74, #2562 ), references = 1, size of lhs = 12:
% 20.35/20.53 halfadder-{F}(V0), P_in1-{F}(V0,V1), zero-{F}(V1), P_and2-{F}(V0,V2), and_ok-{F}(V2), fulladder-{F}(V3), P_h2-{F}(V3,V4), halfadder-{F}(V4), P_and2-{F}(V4,V2), P_or1-{F}(V3,V5), P_in1-{F}(V5,V6), one-{F}(V6) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2586: mergings( V2 == V18, V8 == V24, V10 == V26, V7 == V23, V11 == V27, V12 == V28, V13 == V29, V9 == V25, V3 == V19, V5 == V21, V4 == V20, V6 == V22; #2572 ), references = 2, size of lhs = 33:
% 20.35/20.53 halfadder-{F}(V0), P_in1-{F}(V0,V1), zero-{F}(V1), fulladder-{F}(V2), P_h2-{F}(V2,V0), P_or1-{F}(V2,V3), or_ok-{F}(V3), P_a-{F}(V4), P_ina1-{F}(V4,V5), P_ina2-{F}(V4,V6), P_inb1-{F}(V4,V7), P_inb2-{F}(V4,V8), P_inc-{F}(V4,V9), P_out1-{F}(V4,V10), P_out2-{F}(V4,V11), P_outc-{F}(V4,V12), P_f2-{F}(V4,V13), P_h2-{F}(V13,V0), P_or1-{F}(V13,V14), P_h1-{F}(V13,V15), halfadder-{F}(V15), P_and2-{F}(V15,V16), fulladder-{F}(V17), P_h1-{F}(V17,V15), P_or1-{F}(V17,V3), P_in1-{F}(V15,V18), zero-{F}(V18), nbit_adder2-{F}(V19), P_outc-{F}(V19,V20), one-{F}(V20), P_f2-{F}(V19,V21), fulladder-{F}(V21), P_or1-{F}(V21,V3) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2587: exists( #78, #2571 ), references = 1, size of lhs = 22:
% 20.35/20.53 P_a-{F}(V0), P_ina1-{F}(V0,V1), P_ina2-{F}(V0,V2), P_inb1-{F}(V0,V3), P_inb2-{F}(V0,V4), P_inc-{F}(V0,V5), P_out1-{F}(V0,V6), P_out2-{F}(V0,V7), P_outc-{F}(V0,V8), P_f2-{F}(V0,V9), P_or1-{F}(V9,V10), P_h1-{F}(V9,V11), P_and2-{F}(V11,V12), P_h2-{F}(V9,V13), halfadder-{F}(V13), P_in1-{F}(V13,V14), zero-{F}(V14), fulladder-{F}(V15), P_h2-{F}(V15,V13), P_or1-{F}(V15,V16), P_in1-{F}(V16,V17), one-{F}(V17) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2600: exists( #74, #2596 ), references = 1, size of lhs = 35:
% 20.35/20.53 fulladder-{F}(V0), P_in1-{F}(V0,V1), zero-{F}(V1), P_h2-{F}(V0,V2), halfadder-{F}(V2), fulladder-{F}(V3), P_h2-{F}(V3,V2), P_or1-{F}(V3,V4), or_ok-{F}(V4), P_a-{F}(V5), P_ina1-{F}(V5,V6), P_ina2-{F}(V5,V7), P_inb1-{F}(V5,V8), P_inb2-{F}(V5,V9), P_inc-{F}(V5,V10), P_out1-{F}(V5,V11), P_out2-{F}(V5,V12), P_outc-{F}(V5,V13), P_f2-{F}(V5,V14), P_h2-{F}(V14,V2), P_or1-{F}(V14,V15), P_h1-{F}(V14,V16), halfadder-{F}(V16), P_and2-{F}(V16,V17), fulladder-{F}(V18), P_h1-{F}(V18,V16), P_or1-{F}(V18,V4), P_in1-{F}(V16,V19), zero-{F}(V19), nbit_adder2-{F}(V20), P_outc-{F}(V20,V21), one-{F}(V21), P_f2-{F}(V20,V22), fulladder-{F}(V22), P_or1-{F}(V22,V4) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2602: exists( #78, #2598 ), references = 3, size of lhs = 34:
% 20.35/20.53 fulladder-{F}(V0), P_in1-{F}(V0,V1), zero-{F}(V1), P_h2-{F}(V0,V2), halfadder-{F}(V2), fulladder-{F}(V3), P_h2-{F}(V3,V2), P_or1-{F}(V3,V4), or_ok-{F}(V4), P_a-{F}(V5), P_ina1-{F}(V5,V6), P_ina2-{F}(V5,V7), P_inb1-{F}(V5,V8), P_inb2-{F}(V5,V9), P_inc-{F}(V5,V10), P_out1-{F}(V5,V11), P_out2-{F}(V5,V12), P_outc-{F}(V5,V13), P_f2-{F}(V5,V14), P_h2-{F}(V14,V2), P_or1-{F}(V14,V15), P_h1-{F}(V14,V16), halfadder-{F}(V16), fulladder-{F}(V17), P_h1-{F}(V17,V16), P_or1-{F}(V17,V4), P_in1-{F}(V16,V18), zero-{F}(V18), nbit_adder2-{F}(V19), P_outc-{F}(V19,V20), one-{F}(V20), P_f2-{F}(V19,V21), fulladder-{F}(V21), P_or1-{F}(V21,V4) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2607: mergings( V2 == V21; #2605 ), references = 1, size of lhs = 35:
% 20.35/20.53 zero-{F}(V0), halfadder-{F}(V1), fulladder-{F}(V2), P_in1-{F}(V2,V3), zero-{F}(V3), P_h2-{F}(V2,V4), halfadder-{F}(V4), fulladder-{F}(V5), P_h2-{F}(V5,V4), P_or1-{F}(V5,V6), or_ok-{F}(V6), P_a-{F}(V7), P_ina1-{F}(V7,V8), P_ina2-{F}(V7,V9), P_inb1-{F}(V7,V10), P_inb2-{F}(V7,V11), P_inc-{F}(V7,V12), P_out1-{F}(V7,V13), P_out2-{F}(V7,V14), P_outc-{F}(V7,V15), P_f2-{F}(V7,V16), P_h2-{F}(V16,V4), P_h1-{F}(V16,V1), P_or1-{F}(V16,V17), fulladder-{F}(V18), P_h1-{F}(V18,V1), P_or1-{F}(V18,V6), nbit_adder2-{F}(V19), P_ina1-{F}(V19,V0), P_f1-{F}(V19,V1), P_outc-{F}(V19,V20), one-{F}(V20), P_f2-{F}(V19,V21), fulladder-{F}(V21), P_or1-{F}(V21,V6) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2612: mergings( V2 == V18, V6 == V16; #2609 ), references = 1, size of lhs = 29:
% 20.35/20.53 zero-{F}(V0), halfadder-{F}(V1), zero-{F}(V2), fulladder-{F}(V3), P_in1-{F}(V3,V2), P_h1-{F}(V3,V1), or_ok-{F}(V4), P_or1-{F}(V3,V4), P_a-{F}(V5), P_f2-{F}(V5,V3), P_ina1-{F}(V5,V6), P_ina2-{F}(V5,V7), P_inb1-{F}(V5,V8), P_inb2-{F}(V5,V9), P_inc-{F}(V5,V10), P_out1-{F}(V5,V11), P_out2-{F}(V5,V12), P_outc-{F}(V5,V13), fulladder-{F}(V14), P_h1-{F}(V14,V1), P_or1-{F}(V14,V4), nbit_adder2-{F}(V15), P_ina1-{F}(V15,V0), P_f1-{F}(V15,V1), P_outc-{F}(V15,V16), one-{F}(V16), P_f2-{F}(V15,V17), fulladder-{F}(V17), P_or1-{F}(V17,V4) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2646: exists( #74, #2640 ), references = 2, size of lhs = 36:
% 20.35/20.53 fulladder-{F}(V0), P_in2-{F}(V0,V1), zero-{F}(V1), P_h1-{F}(V0,V2), halfadder-{F}(V2), fulladder-{F}(V3), P_in1-{F}(V3,V4), zero-{F}(V4), P_h2-{F}(V3,V5), halfadder-{F}(V5), fulladder-{F}(V6), P_h2-{F}(V6,V5), P_or1-{F}(V6,V7), or_ok-{F}(V7), P_a-{F}(V8), P_ina1-{F}(V8,V9), P_ina2-{F}(V8,V10), P_inb1-{F}(V8,V11), P_inb2-{F}(V8,V12), P_inc-{F}(V8,V13), P_out1-{F}(V8,V14), P_out2-{F}(V8,V15), P_outc-{F}(V8,V16), P_f2-{F}(V8,V17), P_h2-{F}(V17,V5), P_h1-{F}(V17,V2), P_or1-{F}(V17,V18), fulladder-{F}(V19), P_h1-{F}(V19,V2), P_or1-{F}(V19,V7), nbit_adder2-{F}(V20), P_outc-{F}(V20,V21), one-{F}(V21), P_f2-{F}(V20,V22), fulladder-{F}(V22), P_or1-{F}(V22,V7) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2650: mergings( V6 == V16; #2648 ), references = 1, size of lhs = 30:
% 20.35/20.53 fulladder-{F}(V0), P_in2-{F}(V0,V1), zero-{F}(V1), P_h1-{F}(V0,V2), halfadder-{F}(V2), zero-{F}(V3), fulladder-{F}(V4), P_in1-{F}(V4,V3), P_h1-{F}(V4,V2), or_ok-{F}(V5), P_or1-{F}(V4,V5), P_a-{F}(V6), P_f2-{F}(V6,V4), P_ina1-{F}(V6,V7), P_ina2-{F}(V6,V8), P_inb1-{F}(V6,V9), P_inb2-{F}(V6,V10), P_inc-{F}(V6,V11), P_out1-{F}(V6,V12), P_out2-{F}(V6,V13), P_outc-{F}(V6,V14), fulladder-{F}(V15), P_h1-{F}(V15,V2), P_or1-{F}(V15,V5), nbit_adder2-{F}(V16), P_outc-{F}(V16,V17), one-{F}(V17), P_f2-{F}(V16,V18), fulladder-{F}(V18), P_or1-{F}(V18,V5) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2654: mergings( V4 == V14; #2652 ), references = 1, size of lhs = 23:
% 20.35/20.53 zero-{F}(V0), zero-{F}(V1), or_ok-{F}(V2), P_a-{F}(V3), P_f2-{F}(V3,V4), P_in2-{F}(V4,V0), P_in1-{F}(V4,V1), fulladder-{F}(V4), P_or1-{F}(V4,V2), P_ina1-{F}(V3,V5), P_ina2-{F}(V3,V6), P_inb1-{F}(V3,V7), P_inb2-{F}(V3,V8), P_inc-{F}(V3,V9), P_out1-{F}(V3,V10), P_out2-{F}(V3,V11), P_outc-{F}(V3,V12), nbit_adder2-{F}(V13), P_outc-{F}(V13,V14), one-{F}(V14), P_f2-{F}(V13,V15), fulladder-{F}(V15), P_or1-{F}(V15,V2) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2667: mergings( V2 == V13, V8 == V19, V10 == V21, V7 == V18, V9 == V20, V3 == V14, V5 == V16, V4 == V15, V6 == V17; #2657 ), references = 2, size of lhs = 19:
% 20.35/20.53 fulladder-{F}(V0), zero-{F}(V1), P_in2-{F}(V0,V1), zero-{F}(V2), P_in1-{F}(V0,V2), P_a-{F}(V3), P_f2-{F}(V3,V0), P_ina1-{F}(V3,V4), P_ina2-{F}(V3,V5), P_inb1-{F}(V3,V6), P_inb2-{F}(V3,V7), P_inc-{F}(V3,V8), P_out1-{F}(V3,V9), P_out2-{F}(V3,V10), P_outc-{F}(V3,V11), nbit_adder2-{F}(V12), P_f2-{F}(V12,V0), P_outc-{F}(V12,V13), one-{F}(V13) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2678: mergings( V2 == V14; #2676 ), references = 2, size of lhs = 19:
% 20.35/20.53 zero-{F}(V0), fulladder-{F}(V1), zero-{F}(V2), P_in1-{F}(V1,V2), P_a-{F}(V3), P_f2-{F}(V3,V1), P_ina1-{F}(V3,V4), P_ina2-{F}(V3,V5), P_inb1-{F}(V3,V6), P_inb2-{F}(V3,V7), P_inc-{F}(V3,V8), P_out1-{F}(V3,V9), P_out2-{F}(V3,V10), P_outc-{F}(V3,V11), nbit_adder2-{F}(V12), P_inb2-{F}(V12,V0), P_f2-{F}(V12,V1), P_outc-{F}(V12,V13), one-{F}(V13) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2683: mergings( V2 == V14; #2681 ), references = 2, size of lhs = 19:
% 20.35/20.53 zero-{F}(V0), fulladder-{F}(V1), zero-{F}(V2), P_a-{F}(V3), P_f2-{F}(V3,V1), P_ina1-{F}(V3,V4), P_ina2-{F}(V3,V5), P_inb1-{F}(V3,V6), P_inb2-{F}(V3,V7), P_inc-{F}(V3,V8), P_out1-{F}(V3,V9), P_out2-{F}(V3,V10), P_outc-{F}(V3,V11), nbit_adder2-{F}(V12), P_ina2-{F}(V12,V0), P_inb2-{F}(V12,V2), P_f2-{F}(V12,V1), P_outc-{F}(V12,V13), one-{F}(V13) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2702: mergings( V9 == V18, V20 == V11, V8 == V17, V10 == V19, V2 == V5, V5 == V14, V4 == V7, V7 == V16, V12 == V3, V3 == V6, V6 == V15; #2690 ), references = 2, size of lhs = 12:
% 20.35/20.53 zero-{F}(V0), fulladder-{F}(V1), P_a-{F}(V2), nbit_adder2-{F}(V2), P_f2-{F}(V2,V1), P_ina2-{F}(V2,V0), P_ina1-{F}(V2,V3), P_inb1-{F}(V2,V4), P_inc-{F}(V2,V5), P_out1-{F}(V2,V6), P_out2-{F}(V2,V7), P_outc-{F}(V2,V8) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2706: mergings( V2 == V4; #2704 ), references = 1, size of lhs = 10:
% 20.35/20.53 fulladder-{F}(V0), P_a-{F}(V1), nbit_adder2-{F}(V1), P_f2-{F}(V1,V0), P_ina1-{F}(V1,V2), P_inb1-{F}(V1,V3), P_inc-{F}(V1,V4), P_out1-{F}(V1,V5), P_out2-{F}(V1,V6), P_outc-{F}(V1,V7) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2709: mergings( V3 == V4; #2707 ), references = 1, size of lhs = 9:
% 20.35/20.53 fulladder-{F}(V0), P_a-{F}(V1), nbit_adder2-{F}(V1), P_f2-{F}(V1,V0), P_ina1-{F}(V1,V2), P_inc-{F}(V1,V3), P_out1-{F}(V1,V4), P_out2-{F}(V1,V5), P_outc-{F}(V1,V6) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2711: exists( #89, #2707 ), references = 1, size of lhs = 8:
% 20.35/20.53 fulladder-{F}(V0), P_a-{F}(V1), nbit_adder2-{F}(V1), P_f2-{F}(V1,V0), P_inc-{F}(V1,V2), P_out1-{F}(V1,V3), P_out2-{F}(V1,V4), P_outc-{F}(V1,V5) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2713: exists( #88, #2710 ), references = 1, size of lhs = 7:
% 20.35/20.53 fulladder-{F}(V0), P_a-{F}(V1), nbit_adder2-{F}(V1), P_f2-{F}(V1,V0), P_inc-{F}(V1,V2), P_out1-{F}(V1,V3), P_outc-{F}(V1,V4) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2716: exists( #87, #2714 ), references = 1, size of lhs = 5:
% 20.35/20.53 P_a-{F}(V0), nbit_adder2-{F}(V0), P_inc-{F}(V0,V1), P_out1-{F}(V0,V2), P_outc-{F}(V0,V3) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2718: exists( #85, #2715 ), references = 1, size of lhs = 4:
% 20.35/20.53 P_a-{F}(V0), nbit_adder2-{F}(V0), P_out1-{F}(V0,V1), P_outc-{F}(V0,V2) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2720: exists( #82, #2717 ), references = 1, size of lhs = 3:
% 20.35/20.53 P_a-{F}(V0), nbit_adder2-{F}(V0), P_out1-{F}(V0,V1) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2722: exists( #75, #2719 ), references = 1, size of lhs = 2:
% 20.35/20.53 P_a-{F}(V0), nbit_adder2-{F}(V0) | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 #2725: exists( #93, #2723 ), references = 1, size of lhs = 0:
% 20.35/20.53 FALSE | FALSE
% 20.35/20.53 (used 0 times, uses = {})
% 20.35/20.53
% 20.35/20.53 number of learnt formulas = 222
% 20.35/20.53
% 20.35/20.53
% 20.35/20.53 % SZS output end Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 20.35/20.53
% 20.35/20.53 randbase = 1
%------------------------------------------------------------------------------