%------------------------------------------------------------------------------
% File : Geo-III---2018C
% Problem : GRA166-1 : TPTP v9.3.0. Released v9.3.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 : Tue May 5 06:27:34 PM UTC 2026
% Result : Unsatisfiable 21.25s 21.48s
% Output : Refutation 21.25s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : GRA166-1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.12 % Command : geo -tptp_input -nonempty -inputfile %s
% 0.17/0.33 % Computer : n022.cluster.edu
% 0.17/0.33 % Model : x86_64 x86_64
% 0.17/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.33 % Memory : 8042.1875MB
% 0.17/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.17/0.33 % CPULimit : 300
% 0.17/0.33 % WCLimit : 300
% 0.17/0.33 % DateTime : Tue May 5 00:41:35 EDT 2026
% 0.17/0.33 % CPUTime :
% 21.25/21.48 GeoParameters:
% 21.25/21.48
% 21.25/21.48 tptp_input = 1
% 21.25/21.48 tptp_output = 0
% 21.25/21.48 nonempty = 1
% 21.25/21.48 inputfile = /export/starexec/sandbox/benchmark/theBenchmark.p
% 21.25/21.48 includepath = /export/starexec/sandbox/solver/bin/../../benchmark/
% 21.25/21.48
% 21.25/21.48
% 21.25/21.48 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 21.25/21.48 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 21.25/21.48
% 21.25/21.48 RuleSystem INPUT:
% 21.25/21.48
% 21.25/21.48 Initial Rules:
% 21.25/21.48 #0: input, references = 13, size of lhs = 2:
% 21.25/21.48 P_z-{F}(V0), P_s-{F}(V1,V0) | FALSE
% 21.25/21.48 (used 0 times, uses = {})
% 21.25/21.48
% 21.25/21.48 #1: input, references = 7, size of lhs = 4:
% 21.25/21.48 P_z-{F}(V0), P_s-{F}(V1,V4), P_s-{F}(V2,V4), V1 == V2 | FALSE
% 21.25/21.48 (used 0 times, uses = {})
% 21.25/21.48
% 21.25/21.48 #2: input, references = 3, size of lhs = 2:
% 21.25/21.48 P_z-{F}(V0), r-{F}(V1,V1) | FALSE
% 21.25/21.48 (used 0 times, uses = {})
% 21.25/21.48
% 21.25/21.48 #3: input, references = 3, size of lhs = 2:
% 21.25/21.48 P_z-{F}(V0), b-{F}(V1,V1) | FALSE
% 21.25/21.48 (used 0 times, uses = {})
% 21.25/21.48
% 21.25/21.48 #4: input, references = 25, size of lhs = 4:
% 21.25/21.48 P_z-{F}(V0), #-{F} V1, #-{F} V2, V1 == V2 | r-{T}(V1,V2), b-{T}(V1,V2)
% 21.25/21.48 (used 0 times, uses = {})
% 21.25/21.48
% 21.25/21.48 #5: input, references = 18, size of lhs = 4:
% 21.25/21.48 P_z-{F}(V0), r-{F}(V1,V2), r-{F}(V3,V1), r-{F}(V3,V2) | FALSE
% 21.25/21.48 (used 0 times, uses = {})
% 21.25/21.48
% 21.25/21.48 #6: input, references = 6, size of lhs = 7:
% 21.25/21.48 P_z-{F}(V0), b-{F}(V1,V2), b-{F}(V3,V1), b-{F}(V3,V2), b-{F}(V2,V4), b-{F}(V1,V5), b-{F}(V5,V4) | FALSE
% 21.25/21.48 (used 0 times, uses = {})
% 21.25/21.48
% 21.25/21.48 #7: input, references = 16, size of lhs = 1:
% 21.25/21.48 #-{F} V0 | EXISTS V1: P_s-{T}(V0,V1)
% 21.25/21.48 (used 0 times, uses = {})
% 21.25/21.48
% 21.25/21.48 #8: input, references = 4, size of lhs = 0:
% 21.25/21.48 FALSE | EXISTS V0: P_z-{T}(V0)
% 21.25/21.48 (used 0 times, uses = {})
% 21.25/21.48
% 21.25/21.48 number of initial rules = 9
% 21.25/21.48
% 21.25/21.48 Simplifiers:
% 21.25/21.48 #9: unsound, references = 3, size of lhs = 3:
% 21.25/21.48 P_s-{F}(V0,V1), P_s-{F}(V0,V3), V1 == V3 | FALSE
% 21.25/21.48 (used 0 times, uses = {})
% 21.25/21.48
% 21.25/21.48 #10: unsound, references = 3, size of lhs = 3:
% 21.25/21.48 P_z-{F}(V0), P_z-{F}(V1), V0 == V1 | FALSE
% 21.25/21.48 (used 0 times, uses = {})
% 21.25/21.48
% 21.25/21.48 number of simplifiers = 2
% 21.25/21.48
% 21.25/21.48 Learnt:
% 21.25/21.48 #13: mergings( V0 == V3; #11 ), references = 12, size of lhs = 5:
% 21.25/21.48 P_z-{F}(V0), b-{F}(V1,V2), b-{F}(V1,V3), V2 == V3, b-{F}(V3,V4) | r-{T}(V2,V3)
% 21.25/21.48 (used 0 times, uses = {})
% 21.25/21.48
% 21.25/21.48 #16: mergings( V0 == V3; #14 ), references = 2, size of lhs = 6:
% 21.25/21.48 P_z-{F}(V0), b-{F}(V1,V2), b-{F}(V1,V3), b-{F}(V2,V3), #-{F} V4, V3 == V4 | r-{T}(V3,V4)
% 21.25/21.48 (used 0 times, uses = {})
% 21.25/21.48
% 21.25/21.48 #24: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6; #19 ), references = 14, size of lhs = 8:
% 21.25/21.48 P_z-{F}(V0), b-{F}(V1,V2), b-{F}(V1,V3), V2 == V3, b-{F}(V4,V2), b-{F}(V4,V3), r-{F}(V5,V3), V2 == V5 | r-{T}(V3,V2)
% 21.25/21.48 (used 0 times, uses = {})
% 21.25/21.48
% 21.25/21.48 #29: mergings( V0 == V3, V3 == V4; #26 ), references = 9, size of lhs = 8:
% 21.25/21.48 P_z-{F}(V0), b-{F}(V1,V2), r-{F}(V3,V2), r-{F}(V3,V4), V1 == V4, V2 == V4, r-{F}(V5,V4), V2 == V5 | r-{T}(V1,V4)
% 21.25/21.48 (used 0 times, uses = {})
% 21.25/21.48
% 21.25/21.48 #36: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6; #31 ), references = 6, size of lhs = 9:
% 21.25/21.48 P_z-{F}(V0), r-{F}(V1,V2), V2 == V1, r-{F}(V1,V3), b-{F}(V3,V2), #-{F} V4, V1 == V4, V2 == V4, V3 == V4 | b-{T}(V1,V4)
% 21.25/21.48 (used 0 times, uses = {})
% 21.25/21.48
% 21.25/21.48 #47: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7; #41 ), references = 4, size of lhs = 26:
% 21.25/21.48 P_z-{F}(V0), b-{F}(V1,V2), b-{F}(V1,V3), V2 == V3, b-{F}(V4,V2), b-{F}(V4,V3), b-{F}(V5,V2), b-{F}(V5,V6), V6 == V2, V6 == V3, b-{F}(V7,V6), b-{F}(V7,V2), b-{F}(V8,V2), b-{F}(V8,V9), V9 == V6, V9 == V2, V9 == V3, b-{F}(V10,V9), b-{F}(V10,V2), b-{F}(V11,V9), b-{F}(V11,V6), b-{F}(V12,V9), b-{F}(V12,V6), #-{F} V13, V13 == V3, V2 == V13 | b-{T}(V13,V3)
% 21.25/21.48 (used 0 times, uses = {})
% 21.25/21.48
% 21.25/21.48 #68: mergings( V2 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10, V10 == V11, V11 == V12, V12 == V13, V13 == V14; #55 ), references = 1, size of lhs = 50:
% 21.25/21.48 P_z-{F}(V0), r-{F}(V1,V2), V2 == V1, r-{F}(V1,V3), b-{F}(V3,V2), b-{F}(V1,V4), b-{F}(V1,V5), V5 == V4, b-{F}(V1,V6), V6 == V5, V6 == V4, b-{F}(V7,V6), b-{F}(V7,V5), b-{F}(V8,V6), b-{F}(V8,V5), b-{F}(V9,V4), b-{F}(V9,V10), V4 == V10, b-{F}(V11,V4), b-{F}(V11,V12), V12 == V4, V12 == V10, b-{F}(V13,V12), b-{F}(V13,V4), b-{F}(V14,V12), b-{F}(V14,V10), b-{F}(V1,V15), V15 == V10, b-{F}(V16,V15), b-{F}(V16,V17), V17 == V15, b-{F}(V18,V17), b-{F}(V18,V15), b-{F}(V19,V15), b-{F}(V19,V20), V20 == V17, V20 == V15, b-{F}(V21,V20), b-{F}(V21,V15), b-{F}(V22,V20), b-{F}(V22,V17), b-{F}(V23,V20), b-{F}(V23,V17), b-{F}(V24,V25), V24 == V4, V4 == V25, V12 == V25, r-{F}(V26,V25), V4 == V26, #-{F} V27 | P_s-{T}(V27,V1), P_s-{T}(V27,V2), P_s-{T}(V27,V3), P_s-{T}(V27,V4), P_s-{T}(V27,V5), P_s-{T}(V27,V6), P_s-{T}(V27,V24), P_s-{T}(V27,V15), P_s-{T}(V27,V10), P_s-{T}(V27,V17), P_s-{T}(V27,V20)
% 21.25/21.48 (used 0 times, uses = {})
% 21.25/21.48
% 21.25/21.48 #91: mergings( V0 == V1, V1 == V2, V2 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10, V10 == V11, V11 == V12, V12 == V40, V40 == V42, V42 == V44, V44 == V46, V46 == V48, V48 == V50, V50 == V52, V52 == V54, V54 == V56; #69 ), references = 1, size of lhs = 68:
% 21.25/21.48 P_z-{F}(V0), b-{F}(V1,V2), b-{F}(V1,V3), V2 == V3, b-{F}(V4,V2), b-{F}(V4,V3), P_s-{F}(V5,V3), P_s-{F}(V6,V2), b-{F}(V7,V3), b-{F}(V7,V2), r-{F}(V7,V8), V8 == V7, r-{F}(V7,V9), b-{F}(V9,V8), b-{F}(V7,V10), V3 == V10, V2 == V10, b-{F}(V11,V10), b-{F}(V11,V12), V10 == V12, b-{F}(V13,V10), b-{F}(V13,V14), V14 == V10, V14 == V12, b-{F}(V15,V14), b-{F}(V15,V10), b-{F}(V16,V14), b-{F}(V16,V12), b-{F}(V7,V17), V17 == V12, b-{F}(V18,V17), b-{F}(V18,V19), V19 == V17, b-{F}(V20,V19), b-{F}(V20,V17), b-{F}(V21,V17), b-{F}(V21,V22), V22 == V19, V22 == V17, b-{F}(V23,V22), b-{F}(V23,V17), b-{F}(V24,V22), b-{F}(V24,V19), b-{F}(V25,V22), b-{F}(V25,V19), P_s-{F}(V26,V7), P_s-{F}(V27,V8), P_s-{F}(V28,V10), P_s-{F}(V29,V17), P_s-{F}(V30,V12), P_s-{F}(V31,V19), P_s-{F}(V32,V22), b-{F}(V33,V34), V33 == V10, V10 == V34, V14 == V34, r-{F}(V35,V34), V10 == V35, #-{F} V36, V26 == V36, V27 == V36, V28 == V36, V5 == V36, V6 == V36, V29 == V36, V30 == V36, V31 == V36, V32 == V36 | P_s-{T}(V36,V9), P_s-{T}(V36,V33)
% 21.25/21.48 (used 0 times, uses = {})
% 21.25/21.48
% 21.25/21.48 #115: mergings( V0 == V1, V1 == V2, V2 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10, V10 == V11, V11 == V12, V12 == V13, V13 == V14, V14 == V15, V15 == V16, V16 == V17, V17 == V18, V18 == V19, V19 == V20, V20 == V21, V21 == V30; #92 ), references = 1, size of lhs = 68:
% 21.25/21.48 P_z-{F}(V0), b-{F}(V0,V1), P_s-{F}(V2,V1), r-{F}(V3,V1), V1 == V3, r-{F}(V3,V0), b-{F}(V3,V4), b-{F}(V5,V4), b-{F}(V5,V6), V6 == V4, b-{F}(V3,V6), b-{F}(V7,V6), b-{F}(V7,V4), P_s-{F}(V8,V4), P_s-{F}(V9,V6), b-{F}(V3,V10), V4 == V10, V6 == V10, b-{F}(V11,V10), b-{F}(V11,V12), V10 == V12, b-{F}(V13,V10), b-{F}(V13,V14), V14 == V10, V14 == V12, b-{F}(V15,V14), b-{F}(V15,V10), b-{F}(V16,V14), b-{F}(V16,V12), b-{F}(V3,V17), V17 == V12, b-{F}(V18,V17), b-{F}(V18,V19), V19 == V17, b-{F}(V20,V19), b-{F}(V20,V17), b-{F}(V21,V17), b-{F}(V21,V22), V22 == V19, V22 == V17, b-{F}(V23,V22), b-{F}(V23,V17), b-{F}(V24,V22), b-{F}(V24,V19), b-{F}(V25,V22), b-{F}(V25,V19), P_s-{F}(V26,V3), P_s-{F}(V27,V10), P_s-{F}(V28,V17), P_s-{F}(V29,V12), P_s-{F}(V30,V19), P_s-{F}(V31,V22), b-{F}(V32,V33), V32 == V10, V10 == V33, V14 == V33, r-{F}(V34,V33), V10 == V34, #-{F} V35, V26 == V35, V2 == V35, V27 == V35, V8 == V35, V9 == V35, V28 == V35, V29 == V35, V30 == V35, V31 == V35 | P_s-{T}(V35,V32)
% 21.25/21.48 (used 0 times, uses = {})
% 21.25/21.48
% 21.25/21.48 #151: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10, V10 == V11, V11 == V12, V12 == V13, V13 == V14, V14 == V15, V15 == V16, V16 == V17, V17 == V18, V18 == V19, V19 == V20, V20 == V21, V21 == V22, V22 == V23, V23 == V24, V24 == V25, V25 == V26, V26 == V27, V27 == V28, V28 == V29, V29 == V30, V30 == V31, V31 == V1; #120 ), references = 1, size of lhs = 38:
% 21.25/21.48 P_z-{F}(V0), r-{F}(V1,V0), r-{F}(V1,V2), V0 == V2, V2 == V1, P_s-{F}(V3,V2), r-{F}(V4,V2), P_s-{F}(V5,V1), P_s-{F}(V6,V7), V1 == V7, V0 == V7, V7 == V2, P_s-{F}(V8,V7), P_s-{F}(V9,V10), V1 == V10, V2 == V10, V0 == V10, V7 == V10, P_s-{F}(V11,V10), P_s-{F}(V12,V10), P_s-{F}(V13,V14), V1 == V14, V0 == V14, V14 == V2, V14 == V4, V10 == V14, V7 == V14, P_s-{F}(V15,V14), #-{F} V16, V5 == V16, V3 == V16, V13 == V16, V9 == V16, V6 == V16, V15 == V16, V11 == V16, V12 == V16, V8 == V16 | r-{T}(V0,V2)
% 21.25/21.48 (used 0 times, uses = {})
% 21.25/21.48
% 21.25/21.48 #185: mergings( V2 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10, V10 == V11, V11 == V12, V12 == V13, V13 == V14, V14 == V15, V15 == V16, V16 == V17, V17 == V18, V18 == V19, V19 == V20, V20 == V21, V21 == V22, V22 == V23, V23 == V24, V24 == V25, V25 == V26, V26 == V27, V27 == V28, V28 == V29, V29 == V30, V30 == V31, V31 == V32, V32 == V33; #153 ), references = 1, size of lhs = 24:
% 21.25/21.48 P_z-{F}(V0), r-{F}(V1,V0), r-{F}(V1,V2), V0 == V2, P_s-{F}(V3,V2), r-{F}(V4,V2), r-{F}(V5,V0), V2 == V5, r-{F}(V5,V2), P_s-{F}(V6,V5), P_s-{F}(V7,V8), V5 == V8, V2 == V8, V0 == V8, P_s-{F}(V9,V8), P_s-{F}(V10,V8), P_s-{F}(V11,V12), V5 == V12, V0 == V12, V12 == V2, V12 == V4, V8 == V12, P_s-{F}(V13,V12), #-{F} V14 | P_s-{T}(V14,V5), P_s-{T}(V14,V0), P_s-{T}(V14,V2), P_s-{T}(V14,V8), P_s-{T}(V14,V12), P_s-{T}(V14,V6), P_s-{T}(V14,V3), P_s-{T}(V14,V11), P_s-{T}(V14,V7), P_s-{T}(V14,V14), P_s-{T}(V14,V13), P_s-{T}(V14,V9), P_s-{T}(V14,V10)
% 21.25/21.48 (used 0 times, uses = {})
% 21.25/21.48
% 21.25/21.48 #229: mergings( V0 == V1, V1 == V2, V2 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10, V10 == V11, V11 == V12, V12 == V13, V13 == V14, V14 == V15, V15 == V16, V16 == V17, V17 == V18, V18 == V19, V19 == V20, V20 == V21, V21 == V22, V22 == V23, V23 == V24, V24 == V25, V25 == V26, V26 == V27, V27 == V28, V28 == V29, V29 == V30, V30 == V31, V31 == V46, V46 == V48, V48 == V50, V50 == V52, V52 == V54, V54 == V56, V56 == V58, V58 == V60, V60 == V62, V62 == V64, V64 == V66; #186 ), references = 1, size of lhs = 45:
% 21.25/21.48 P_z-{F}(V0), r-{F}(V1,V0), r-{F}(V1,V2), V0 == V2, r-{F}(V3,V2), P_s-{F}(V4,V2), P_s-{F}(V5,V2), P_s-{F}(V6,V5), r-{F}(V7,V0), V2 == V7, r-{F}(V7,V2), P_s-{F}(V8,V7), P_s-{F}(V9,V7), P_s-{F}(V10,V11), V7 == V11, V2 == V11, V0 == V11, P_s-{F}(V12,V11), P_s-{F}(V13,V12), P_s-{F}(V14,V11), P_s-{F}(V15,V14), P_s-{F}(V16,V11), P_s-{F}(V17,V16), P_s-{F}(V18,V19), V7 == V19, V0 == V19, V19 == V2, V19 == V3, V11 == V19, P_s-{F}(V20,V19), P_s-{F}(V21,V20), P_s-{F}(V22,V19), P_s-{F}(V23,V22), P_s-{F}(V24,V25), V9 == V25, V4 == V25, V10 == V25, V18 == V25, V6 == V25, V21 == V25, V13 == V25, V24 == V25, V23 == V25, V15 == V25, V17 == V25 | P_s-{T}(V25,V0), P_s-{T}(V25,V8)
% 21.25/21.48 (used 0 times, uses = {})
% 21.25/21.48
% 21.25/21.48 #273: mergings( V0 == V1, V1 == V2, V2 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10, V10 == V11, V11 == V12, V12 == V13, V13 == V14, V14 == V15, V15 == V16, V16 == V17, V17 == V18, V18 == V19, V19 == V20, V20 == V21, V21 == V22, V22 == V23, V23 == V24, V24 == V25, V25 == V26, V26 == V27, V27 == V28, V28 == V29, V29 == V31, V31 == V35, V35 == V36, V36 == V38, V38 == V39, V39 == V40, V40 == V41, V41 == V42, V42 == V43, V43 == V44, V44 == V45, V45 == V46, V46 == V30; #230 ), references = 1, size of lhs = 45:
% 21.25/21.48 P_z-{F}(V0), r-{F}(V1,V0), r-{F}(V1,V2), V0 == V2, r-{F}(V3,V2), P_s-{F}(V4,V2), P_s-{F}(V5,V2), P_s-{F}(V6,V5), r-{F}(V7,V0), V2 == V7, r-{F}(V7,V2), P_s-{F}(V8,V7), P_s-{F}(V9,V7), P_s-{F}(V10,V11), V7 == V11, V2 == V11, V0 == V11, P_s-{F}(V12,V11), P_s-{F}(V13,V12), P_s-{F}(V14,V11), P_s-{F}(V15,V14), P_s-{F}(V16,V11), P_s-{F}(V17,V16), P_s-{F}(V18,V19), V7 == V19, V0 == V19, V19 == V2, V19 == V3, V11 == V19, P_s-{F}(V20,V19), P_s-{F}(V21,V20), P_s-{F}(V22,V19), P_s-{F}(V23,V22), P_s-{F}(V24,V25), V9 == V25, V4 == V25, V10 == V25, V18 == V25, V6 == V25, V21 == V25, V13 == V25, V24 == V25, V23 == V25, V15 == V25, V17 == V25 | P_s-{T}(V25,V8)
% 21.25/21.48 (used 0 times, uses = {})
% 21.25/21.48
% 21.25/21.48 #320: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10, V10 == V11, V11 == V12, V12 == V13, V13 == V14, V14 == V15, V15 == V16, V16 == V17, V17 == V18, V18 == V19, V19 == V20, V20 == V21, V21 == V22, V22 == V23, V23 == V24, V24 == V25, V25 == V26, V26 == V27, V27 == V28, V28 == V29, V29 == V30, V30 == V31, V31 == V32, V32 == V33, V33 == V34, V34 == V35, V35 == V36, V36 == V37, V37 == V38, V38 == V39, V39 == V40, V40 == V41, V41 == V42, V42 == V43, V43 == V44, V44 == V45, V45 == V47; #275 ), references = 4, size of lhs = 40:
% 21.25/21.48 P_z-{F}(V0), P_s-{F}(V0,V1), r-{F}(V1,V0), P_s-{F}(V2,V1), P_s-{F}(V3,V4), V0 == V4, V4 == V1, P_s-{F}(V5,V4), P_s-{F}(V6,V5), P_s-{F}(V7,V8), V1 == V8, V4 == V8, V0 == V8, P_s-{F}(V9,V8), P_s-{F}(V10,V9), P_s-{F}(V11,V8), P_s-{F}(V12,V11), P_s-{F}(V13,V8), P_s-{F}(V14,V13), P_s-{F}(V15,V16), V0 == V16, V16 == V4, V16 == V1, V8 == V16, P_s-{F}(V17,V16), P_s-{F}(V18,V17), P_s-{F}(V19,V16), P_s-{F}(V20,V19), P_s-{F}(V21,V22), V2 == V22, V3 == V22, V7 == V22, V15 == V22, V6 == V22, V18 == V22, V10 == V22, V21 == V22, V20 == V22, V12 == V22, V14 == V22 | b-{T}(V1,V4)
% 21.25/21.48 (used 0 times, uses = {})
% 21.25/21.48
% 21.25/21.48 #338: mergings( V2 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10, V10 == V11, V11 == V12; #329 ), references = 1, size of lhs = 66:
% 21.25/21.48 P_z-{F}(V0), P_s-{F}(V0,V1), r-{F}(V1,V0), P_s-{F}(V2,V1), b-{F}(V1,V3), b-{F}(V4,V3), b-{F}(V4,V5), V5 == V3, b-{F}(V6,V5), b-{F}(V6,V3), b-{F}(V7,V3), b-{F}(V7,V8), V8 == V5, V8 == V3, b-{F}(V9,V8), b-{F}(V9,V3), b-{F}(V10,V8), b-{F}(V10,V5), b-{F}(V11,V8), b-{F}(V11,V5), b-{F}(V1,V12), b-{F}(V13,V12), b-{F}(V13,V14), V14 == V12, b-{F}(V1,V14), b-{F}(V1,V15), V3 == V15, V14 == V15, b-{F}(V16,V15), b-{F}(V16,V17), V17 == V15, b-{F}(V1,V18), V18 == V12, b-{F}(V19,V18), b-{F}(V19,V20), V20 == V18, b-{F}(V21,V20), b-{F}(V21,V18), b-{F}(V22,V18), b-{F}(V22,V23), V23 == V20, V23 == V18, b-{F}(V24,V23), b-{F}(V24,V18), b-{F}(V25,V23), b-{F}(V25,V20), b-{F}(V26,V23), b-{F}(V26,V20), P_s-{F}(V27,V28), P_s-{F}(V29,V30), V1 == V30, V0 == V30, P_s-{F}(V31,V30), P_s-{F}(V32,V31), P_s-{F}(V33,V30), P_s-{F}(V34,V33), P_s-{F}(V35,V30), P_s-{F}(V36,V35), P_s-{F}(V37,V38), V0 == V38, V38 == V1, V30 == V38, P_s-{F}(V39,V38), P_s-{F}(V40,V39), P_s-{F}(V41,V38), P_s-{F}(V42,V41) | P_s-{T}(V28,V0), P_s-{T}(V28,V1), P_s-{T}(V28,V3), P_s-{T}(V28,V5), P_s-{T}(V28,V8), P_s-{T}(V28,V15), P_s-{T}(V28,V17), P_s-{T}(V28,V14), P_s-{T}(V28,V18), P_s-{T}(V28,V12), P_s-{T}(V28,V20), P_s-{T}(V28,V23), P_s-{T}(V28,V30), P_s-{T}(V28,V38), P_s-{T}(V28,V2), P_s-{T}(V28,V28), P_s-{T}(V28,V29), P_s-{T}(V28,V37), P_s-{T}(V28,V27), P_s-{T}(V28,V40), P_s-{T}(V28,V32), P_s-{T}(V28,V42), P_s-{T}(V28,V34), P_s-{T}(V28,V36)
% 21.25/21.48 (used 0 times, uses = {})
% 21.25/21.48
% 21.25/21.48 #367: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10, V10 == V51, V51 == V53, V53 == V55, V55 == V57, V57 == V59, V59 == V61, V61 == V63, V63 == V65, V65 == V67, V67 == V69, V69 == V71, V71 == V73, V73 == V75, V75 == V77, V77 == V79, V79 == V81, V81 == V83, V83 == V85, V85 == V87; #339 ), references = 1, size of lhs = 104:
% 21.25/21.48 P_z-{F}(V0), P_s-{F}(V0,V1), r-{F}(V1,V0), P_s-{F}(V2,V1), b-{F}(V1,V3), b-{F}(V4,V3), b-{F}(V4,V5), V5 == V3, b-{F}(V6,V5), b-{F}(V6,V3), b-{F}(V7,V3), b-{F}(V7,V8), V8 == V5, V8 == V3, b-{F}(V9,V8), b-{F}(V9,V3), b-{F}(V10,V8), b-{F}(V10,V5), b-{F}(V11,V8), b-{F}(V11,V5), b-{F}(V1,V12), b-{F}(V13,V12), b-{F}(V13,V14), V14 == V12, b-{F}(V1,V14), b-{F}(V1,V15), V3 == V15, V14 == V15, b-{F}(V16,V15), b-{F}(V16,V17), V17 == V15, b-{F}(V1,V18), V18 == V12, b-{F}(V19,V18), b-{F}(V19,V20), V20 == V18, b-{F}(V21,V20), b-{F}(V21,V18), b-{F}(V22,V18), b-{F}(V22,V23), V23 == V20, V23 == V18, b-{F}(V24,V23), b-{F}(V24,V18), b-{F}(V25,V23), b-{F}(V25,V20), b-{F}(V26,V23), b-{F}(V26,V20), P_s-{F}(V27,V1), P_s-{F}(V28,V3), P_s-{F}(V29,V5), P_s-{F}(V30,V8), P_s-{F}(V31,V15), P_s-{F}(V32,V17), P_s-{F}(V33,V14), P_s-{F}(V34,V18), P_s-{F}(V35,V12), P_s-{F}(V36,V20), P_s-{F}(V37,V23), P_s-{F}(V38,V39), P_s-{F}(V39,V40), V1 == V40, V0 == V40, P_s-{F}(V41,V40), P_s-{F}(V42,V40), P_s-{F}(V43,V42), P_s-{F}(V44,V40), P_s-{F}(V45,V44), P_s-{F}(V46,V40), P_s-{F}(V47,V46), P_s-{F}(V48,V49), V0 == V49, V49 == V1, V40 == V49, P_s-{F}(V50,V49), P_s-{F}(V51,V50), P_s-{F}(V52,V49), P_s-{F}(V53,V52), P_s-{F}(V54,V53), P_s-{F}(V55,V49), P_s-{F}(V56,V55), P_s-{F}(V57,V56), P_s-{F}(V58,V59), V27 == V59, V28 == V59, V29 == V59, V30 == V59, V31 == V59, V32 == V59, V33 == V59, V34 == V59, V35 == V59, V36 == V59, V37 == V59, V41 == V59, V48 == V59, V58 == V59, V43 == V59, V51 == V59, V54 == V59, V57 == V59, P_s-{F}(V60,V59), P_s-{F}(V61,V60), V61 == V59 | P_s-{T}(V59,V0), P_s-{T}(V59,V2), P_s-{T}(V59,V38), P_s-{T}(V59,V45), P_s-{T}(V59,V47)
% 21.25/21.48 (used 0 times, uses = {})
% 21.25/21.48
% 21.25/21.48 #401: mergings( V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10, V10 == V35, V35 == V37, V37 == V39, V39 == V41, V41 == V43, V43 == V45, V45 == V47, V47 == V49, V49 == V51, V51 == V53, V53 == V55, V55 == V57, V57 == V58, V58 == V59, V59 == V60, V60 == V61, V61 == V62, V62 == V63, V63 == V64, V64 == V0, V0 == V2, V2 == V65, V1 == V66, V65 == V72, V66 == V71; #368 ), references = 1, size of lhs = 100:
% 21.25/21.48 P_z-{F}(V0), P_s-{F}(V0,V1), r-{F}(V1,V0), b-{F}(V1,V2), b-{F}(V3,V2), b-{F}(V3,V4), V4 == V2, b-{F}(V5,V4), b-{F}(V5,V2), b-{F}(V6,V2), b-{F}(V6,V7), V7 == V4, V7 == V2, b-{F}(V8,V7), b-{F}(V8,V2), b-{F}(V9,V7), b-{F}(V9,V4), b-{F}(V10,V7), b-{F}(V10,V4), b-{F}(V1,V11), b-{F}(V12,V11), b-{F}(V12,V13), V13 == V11, b-{F}(V1,V13), b-{F}(V1,V14), V2 == V14, V13 == V14, b-{F}(V15,V14), b-{F}(V15,V16), V16 == V14, b-{F}(V1,V17), V17 == V11, b-{F}(V18,V17), b-{F}(V18,V19), V19 == V17, b-{F}(V20,V19), b-{F}(V20,V17), b-{F}(V21,V17), b-{F}(V21,V22), V22 == V19, V22 == V17, b-{F}(V23,V22), b-{F}(V23,V17), b-{F}(V24,V22), b-{F}(V24,V19), b-{F}(V25,V22), b-{F}(V25,V19), P_s-{F}(V26,V1), P_s-{F}(V27,V2), P_s-{F}(V28,V4), P_s-{F}(V29,V7), P_s-{F}(V30,V14), P_s-{F}(V31,V16), P_s-{F}(V32,V13), P_s-{F}(V33,V17), P_s-{F}(V34,V11), P_s-{F}(V35,V19), P_s-{F}(V36,V22), P_s-{F}(V1,V37), V1 == V37, V0 == V37, P_s-{F}(V38,V37), P_s-{F}(V39,V37), P_s-{F}(V40,V39), P_s-{F}(V41,V37), P_s-{F}(V42,V41), P_s-{F}(V43,V44), V0 == V44, V44 == V1, V37 == V44, P_s-{F}(V45,V44), P_s-{F}(V46,V45), P_s-{F}(V47,V44), P_s-{F}(V48,V47), P_s-{F}(V49,V48), P_s-{F}(V50,V44), P_s-{F}(V51,V50), P_s-{F}(V52,V51), P_s-{F}(V53,V54), V26 == V54, V27 == V54, V28 == V54, V29 == V54, V30 == V54, V31 == V54, V32 == V54, V33 == V54, V34 == V54, V35 == V54, V36 == V54, V38 == V54, V43 == V54, V53 == V54, V40 == V54, V46 == V54, V49 == V54, V52 == V54, P_s-{F}(V55,V54), P_s-{F}(V56,V55), V56 == V54 | P_s-{T}(V54,V42)
% 21.25/21.48 (used 0 times, uses = {})
% 21.25/21.48
% 21.25/21.48 #488: mergings( V2 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10, V10 == V11, V11 == V12, V12 == V13, V13 == V14, V14 == V15, V15 == V16, V16 == V17, V17 == V18, V18 == V19, V19 == V20, V20 == V21, V21 == V22, V22 == V23, V23 == V24, V24 == V25, V25 == V26, V26 == V27, V27 == V28, V28 == V29, V29 == V30, V30 == V31, V31 == V32, V32 == V33, V33 == V34, V34 == V35, V35 == V36, V36 == V37, V37 == V38, V38 == V39, V39 == V40, V40 == V41, V41 == V42, V42 == V43, V43 == V44, V44 == V45, V45 == V46, V46 == V49, V49 == V51, V51 == V53, V53 == V54, V54 == V55, V55 == V56, V56 == V57, V57 == V58, V58 == V59, V59 == V60, V60 == V61, V61 == V62, V62 == V63, V63 == V64, V64 == V65, V65 == V66, V66 == V67, V67 == V68, V68 == V69, V69 == V70, V70 == V71, V71 == V72, V72 == V73, V73 == V74, V74 == V75, V75 == V76, V76 == V77, V77 == V78, V78 == V79, V79 == V80, V80 == V82, V82 == V83, V47 == V84, V83 == V87, V84 == V88, V87 == V89, V88 == V90; #406 ), references = 1, size of lhs = 85:
% 21.25/21.48 P_z-{F}(V0), P_s-{F}(V0,V1), r-{F}(V1,V0), P_s-{F}(V2,V1), P_s-{F}(V3,V1), P_s-{F}(V4,V1), P_s-{F}(V5,V1), P_s-{F}(V1,V6), V1 == V6, V0 == V6, P_s-{F}(V7,V6), P_s-{F}(V8,V6), P_s-{F}(V9,V8), P_s-{F}(V10,V11), V0 == V11, V11 == V1, P_s-{F}(V12,V11), P_s-{F}(V13,V11), P_s-{F}(V14,V11), P_s-{F}(V15,V11), P_s-{F}(V16,V11), P_s-{F}(V17,V16), P_s-{F}(V18,V19), V1 == V19, V11 == V19, V0 == V19, P_s-{F}(V20,V19), P_s-{F}(V21,V20), P_s-{F}(V22,V19), P_s-{F}(V23,V22), P_s-{F}(V24,V19), P_s-{F}(V25,V24), P_s-{F}(V26,V27), P_s-{F}(V28,V27), P_s-{F}(V29,V27), P_s-{F}(V30,V27), P_s-{F}(V31,V27), P_s-{F}(V32,V27), P_s-{F}(V33,V34), V0 == V34, V34 == V1, V34 == V11, P_s-{F}(V35,V34), P_s-{F}(V36,V34), P_s-{F}(V37,V34), P_s-{F}(V38,V37), P_s-{F}(V39,V40), V1 == V40, V34 == V40, V0 == V40, P_s-{F}(V41,V40), P_s-{F}(V42,V41), P_s-{F}(V43,V40), P_s-{F}(V44,V43), P_s-{F}(V45,V40), P_s-{F}(V46,V45), P_s-{F}(V47,V48), V1 == V48, V0 == V48, P_s-{F}(V49,V48), P_s-{F}(V50,V49), P_s-{F}(V51,V48), P_s-{F}(V52,V51), P_s-{F}(V53,V48), P_s-{F}(V54,V53), P_s-{F}(V55,V56), V0 == V56, V56 == V1, V48 == V56, P_s-{F}(V57,V56), P_s-{F}(V58,V57), P_s-{F}(V59,V56), P_s-{F}(V60,V59), P_s-{F}(V61,V62), V0 == V62, V62 == V1, V6 == V62, P_s-{F}(V63,V62), P_s-{F}(V64,V63), P_s-{F}(V65,V62), P_s-{F}(V66,V65), P_s-{F}(V67,V66), P_s-{F}(V68,V62), P_s-{F}(V69,V68), P_s-{F}(V70,V69) | P_s-{T}(V27,V0), P_s-{T}(V27,V11), P_s-{T}(V27,V1), P_s-{T}(V27,V19), P_s-{T}(V27,V2), P_s-{T}(V27,V10), P_s-{T}(V27,V18), P_s-{T}(V27,V27), P_s-{T}(V27,V17), P_s-{T}(V27,V26), P_s-{T}(V27,V21), P_s-{T}(V27,V28), P_s-{T}(V27,V23), P_s-{T}(V27,V25), P_s-{T}(V27,V34), P_s-{T}(V27,V40), P_s-{T}(V27,V3), P_s-{T}(V27,V33), P_s-{T}(V27,V39), P_s-{T}(V27,V38), P_s-{T}(V27,V29), P_s-{T}(V27,V42), P_s-{T}(V27,V30), P_s-{T}(V27,V44), P_s-{T}(V27,V46), P_s-{T}(V27,V48), P_s-{T}(V27,V56), P_s-{T}(V27,V4), P_s-{T}(V27,V47), P_s-{T}(V27,V55), P_s-{T}(V27,V31), P_s-{T}(V27,V58), P_s-{T}(V27,V50), P_s-{T}(V27,V60), P_s-{T}(V27,V52), P_s-{T}(V27,V54), P_s-{T}(V27,V5), P_s-{T}(V27,V12), P_s-{T}(V27,V35), P_s-{T}(V27,V13), P_s-{T}(V27,V14), P_s-{T}(V27,V15), P_s-{T}(V27,V36), P_s-{T}(V27,V7), P_s-{T}(V27,V61), P_s-{T}(V27,V9), P_s-{T}(V27,V64), P_s-{T}(V27,V67), P_s-{T}(V27,V70), P_s-{T}(V27,V32)
% 21.25/21.48 (used 0 times, uses = {})
% 21.25/21.48
% 21.25/21.48 #634: mergings( V0 == V1, V1 == V2, V2 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10, V10 == V11, V11 == V12, V12 == V13, V13 == V14, V14 == V15, V15 == V16, V16 == V17, V17 == V18, V18 == V19, V19 == V20, V20 == V21, V21 == V22, V22 == V23, V23 == V24, V24 == V25, V25 == V26, V26 == V27, V27 == V28, V28 == V29, V29 == V30, V30 == V31, V31 == V32, V32 == V33, V33 == V34, V34 == V35, V35 == V36, V36 == V37, V37 == V38, V38 == V39, V39 == V40, V40 == V41, V41 == V42, V42 == V44, V44 == V43, V43 == V47, V47 == V49, V49 == V51, V51 == V52, V52 == V53, V53 == V54, V54 == V55, V55 == V56, V56 == V57, V57 == V58, V58 == V59, V59 == V60, V60 == V61, V61 == V62, V62 == V63, V63 == V64, V64 == V65, V65 == V66, V66 == V67, V67 == V68, V68 == V69, V69 == V70, V70 == V71, V71 == V72, V72 == V73, V73 == V74, V74 == V75, V75 == V76, V76 == V77, V77 == V78, V78 == V80, V80 == V81, V45 == V82, V81 == V85, V82 == V86, V85 == V87, V86 == V88, V87 == V152, V152 == V154, V154 == V156, V156 == V46, V46 == V158, V158 == V160, V160 == V162, V162 == V164, V164 == V166, V166 == V102, V88 == V101, V83 == V100, V102 == V168, V168 == V104, V101 == V103, V104 == V106, V103 == V105, V106 == V170, V170 == V172, V172 == V48, V48 == V174, V174 == V176, V176 == V119, V105 == V118, V100 == V115, V119 == V178, V178 == V180, V180 == V182, V182 == V184, V184 == V186, V186 == V188, V188 == V190, V190 == V50, V50 == V192, V192 == V194, V194 == V196, V196 == V198, V198 == V131, V118 == V130, V115 == V129, V131 == V200, V200 == V133, V130 == V132, V133 == V135, V132 == V134, V135 == V79, V79 == V202, V202 == V204, V204 == V206, V206 == V208, V208 == V210, V210 == V212, V212 == V214, V214 == V216, V216 == V90, V134 == V89, V90 == V218, V218 == V148, V89 == V147, V129 == V146, V148 == V151, V147 == V150, V146 == V149; #489 ), references = 1, size of lhs = 121:
% 21.25/21.48 P_z-{F}(V0), P_s-{F}(V0,V1), r-{F}(V1,V0), P_s-{F}(V2,V1), P_s-{F}(V1,V3), V1 == V3, V0 == V3, P_s-{F}(V4,V3), P_s-{F}(V5,V3), P_s-{F}(V6,V3), P_s-{F}(V3,V7), V0 == V7, V7 == V1, V3 == V7, P_s-{F}(V8,V3), P_s-{F}(V9,V8), P_s-{F}(V10,V3), P_s-{F}(V11,V10), P_s-{F}(V12,V3), P_s-{F}(V13,V12), P_s-{F}(V14,V3), P_s-{F}(V15,V14), P_s-{F}(V16,V3), P_s-{F}(V17,V16), P_s-{F}(V18,V3), P_s-{F}(V19,V18), P_s-{F}(V20,V7), P_s-{F}(V21,V20), P_s-{F}(V22,V7), P_s-{F}(V23,V22), P_s-{F}(V24,V23), P_s-{F}(V25,V26), V2 == V26, V4 == V26, V11 == V26, V5 == V26, V13 == V26, V6 == V26, V19 == V26, V15 == V26, V17 == V26, V9 == V26, V21 == V26, V24 == V26, P_s-{F}(V27,V26), V27 == V26, P_s-{F}(V28,V26), P_s-{F}(V29,V28), V29 == V26, P_s-{F}(V30,V26), P_s-{F}(V31,V30), V31 == V26, P_s-{F}(V32,V26), P_s-{F}(V33,V32), V33 == V26, P_s-{F}(V34,V26), P_s-{F}(V35,V34), V35 == V26, P_s-{F}(V36,V26), P_s-{F}(V37,V36), V37 == V26, P_s-{F}(V38,V39), V0 == V39, V39 == V1, V3 == V39, V38 == V26, P_s-{F}(V40,V39), P_s-{F}(V41,V40), V41 == V26, P_s-{F}(V42,V39), P_s-{F}(V43,V42), V43 == V26, P_s-{F}(V44,V39), P_s-{F}(V45,V44), V45 == V26, P_s-{F}(V46,V39), P_s-{F}(V47,V46), V47 == V26, P_s-{F}(V48,V39), P_s-{F}(V49,V48), V49 == V26, P_s-{F}(V50,V39), P_s-{F}(V51,V50), P_s-{F}(V52,V51), V52 == V26, P_s-{F}(V53,V54), V1 == V54, V3 == V54, V0 == V54, V53 == V26, P_s-{F}(V55,V54), P_s-{F}(V56,V55), V56 == V26, P_s-{F}(V57,V54), P_s-{F}(V58,V57), P_s-{F}(V59,V58), V59 == V26, P_s-{F}(V60,V54), P_s-{F}(V61,V60), P_s-{F}(V62,V61), V62 == V26, P_s-{F}(V63,V54), P_s-{F}(V64,V63), P_s-{F}(V65,V64), V65 == V26, P_s-{F}(V66,V67), V0 == V67, V67 == V1, V3 == V67, V66 == V26, P_s-{F}(V68,V67), P_s-{F}(V69,V68), V69 == V26, P_s-{F}(V70,V67), P_s-{F}(V71,V70), P_s-{F}(V72,V71), V72 == V26, P_s-{F}(V73,V67), P_s-{F}(V74,V73), P_s-{F}(V75,V74), V75 == V26 | P_s-{T}(V26,V25)
% 21.25/21.48 (used 0 times, uses = {})
% 21.25/21.48
% 21.25/21.48 #781: mergings( V2 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10, V10 == V11, V11 == V12, V12 == V13, V13 == V14, V14 == V15, V15 == V16, V16 == V17, V17 == V18, V18 == V19, V19 == V20, V20 == V21, V21 == V22, V22 == V23, V23 == V24, V24 == V25, V25 == V26, V26 == V27, V27 == V28, V28 == V29, V29 == V30, V30 == V31, V31 == V32, V32 == V33, V33 == V34, V34 == V35, V35 == V36, V36 == V37, V37 == V38, V38 == V39, V39 == V40, V40 == V41, V41 == V42, V42 == V43, V43 == V44, V44 == V45, V45 == V47, V47 == V48, V48 == V49, V49 == V50, V50 == V51, V51 == V52, V52 == V53, V53 == V54, V54 == V55, V55 == V56, V56 == V57, V57 == V58, V58 == V59, V59 == V60, V60 == V61, V61 == V62, V62 == V63, V63 == V64, V64 == V65, V65 == V66, V66 == V67, V67 == V68, V68 == V69, V69 == V70, V70 == V71, V71 == V72, V72 == V73, V73 == V74, V74 == V75, V75 == V76, V76 == V77, V77 == V78, V78 == V79, V46 == V80, V79 == V82, V80 == V83, V82 == V84, V83 == V85, V84 == V86, V86 == V87, V87 == V89, V89 == V90, V90 == V91, V91 == V92, V92 == V93, V93 == V94, V94 == V95, V95 == V96, V85 == V97, V81 == V98, V96 == V100, V100 == V101, V97 == V102, V101 == V103, V102 == V104, V103 == V105, V105 == V106, V106 == V107, V107 == V108, V108 == V109, V109 == V110, V104 == V111, V98 == V112, V110 == V114, V114 == V115, V115 == V116, V116 == V117, V117 == V118, V118 == V119, V119 == V120, V120 == V121, V121 == V122, V122 == V123, V123 == V124, V124 == V125, V125 == V126, V111 == V127, V112 == V128, V126 == V130, V130 == V131, V127 == V132, V131 == V133, V132 == V134, V133 == V135, V135 == V136, V136 == V137, V137 == V138, V138 == V139, V139 == V140, V140 == V141, V141 == V142, V142 == V143, V143 == V144, V134 == V145, V144 == V146, V146 == V147, V145 == V148, V128 == V0, V147 == V149, V148 == V150, V149 == V151; #636 ), references = 1, size of lhs = 50:
% 21.25/21.48 P_z-{F}(V0), P_s-{F}(V0,V1), r-{F}(V1,V0), P_s-{F}(V2,V1), P_s-{F}(V1,V3), V1 == V3, V0 == V3, P_s-{F}(V4,V3), P_s-{F}(V5,V3), P_s-{F}(V6,V3), P_s-{F}(V7,V3), P_s-{F}(V8,V3), P_s-{F}(V9,V3), P_s-{F}(V10,V3), P_s-{F}(V11,V3), P_s-{F}(V12,V3), P_s-{F}(V13,V3), P_s-{F}(V14,V3), P_s-{F}(V15,V3), P_s-{F}(V16,V3), P_s-{F}(V17,V3), P_s-{F}(V18,V3), P_s-{F}(V19,V3), P_s-{F}(V20,V3), P_s-{F}(V21,V3), P_s-{F}(V22,V21), P_s-{F}(V23,V3), P_s-{F}(V24,V23), P_s-{F}(V25,V3), P_s-{F}(V26,V25), P_s-{F}(V27,V3), P_s-{F}(V28,V27), P_s-{F}(V29,V3), P_s-{F}(V30,V29), P_s-{F}(V31,V3), P_s-{F}(V32,V31), P_s-{F}(V33,V3), P_s-{F}(V34,V33), P_s-{F}(V35,V3), P_s-{F}(V36,V35), P_s-{F}(V37,V3), P_s-{F}(V38,V37), P_s-{F}(V39,V3), P_s-{F}(V40,V39), P_s-{F}(V41,V3), P_s-{F}(V42,V41), P_s-{F}(V43,V3), P_s-{F}(V44,V43), P_s-{F}(V45,V3), P_s-{F}(V46,V45) | P_s-{T}(V3,V0), P_s-{T}(V3,V1), P_s-{T}(V3,V3), P_s-{T}(V3,V2), P_s-{T}(V3,V4), P_s-{T}(V3,V24), P_s-{T}(V3,V5), P_s-{T}(V3,V26), P_s-{T}(V3,V6), P_s-{T}(V3,V32), P_s-{T}(V3,V28), P_s-{T}(V3,V30), P_s-{T}(V3,V22), P_s-{T}(V3,V7), P_s-{T}(V3,V34), P_s-{T}(V3,V8), P_s-{T}(V3,V9), P_s-{T}(V3,V10), P_s-{T}(V3,V11), P_s-{T}(V3,V12), P_s-{T}(V3,V13), P_s-{T}(V3,V14), P_s-{T}(V3,V15), P_s-{T}(V3,V16), P_s-{T}(V3,V17), P_s-{T}(V3,V18), P_s-{T}(V3,V36), P_s-{T}(V3,V19), P_s-{T}(V3,V38), P_s-{T}(V3,V40), P_s-{T}(V3,V42), P_s-{T}(V3,V20), P_s-{T}(V3,V44), P_s-{T}(V3,V46)
% 21.25/21.48 (used 0 times, uses = {})
% 21.25/21.48
% 21.25/21.48 #950: mergings( V0 == V1, V1 == V2, V2 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10, V10 == V11, V11 == V12, V12 == V13, V13 == V14, V14 == V15, V15 == V16, V16 == V17, V17 == V18, V18 == V19, V19 == V20, V20 == V21, V21 == V22, V22 == V23, V23 == V24, V24 == V25, V25 == V26, V26 == V27, V27 == V28, V28 == V29, V29 == V30, V30 == V31, V31 == V32, V32 == V33, V33 == V34, V34 == V35, V35 == V36, V36 == V37, V37 == V38, V38 == V39, V39 == V40, V40 == V41, V41 == V42, V42 == V43, V43 == V45, V45 == V46, V46 == V47, V47 == V48, V48 == V49, V49 == V50, V50 == V51, V51 == V52, V52 == V53, V53 == V54, V54 == V55, V55 == V56, V56 == V57, V57 == V58, V58 == V59, V59 == V60, V60 == V61, V61 == V62, V62 == V63, V63 == V64, V64 == V65, V65 == V66, V66 == V67, V67 == V68, V68 == V69, V69 == V70, V70 == V71, V71 == V72, V72 == V73, V73 == V74, V74 == V75, V75 == V76, V76 == V77, V44 == V78, V77 == V80, V78 == V81, V80 == V82, V81 == V83, V82 == V84, V84 == V85, V85 == V87, V87 == V88, V88 == V89, V89 == V90, V90 == V91, V91 == V92, V92 == V93, V93 == V94, V83 == V95, V79 == V96, V94 == V98, V98 == V99, V95 == V100, V99 == V101, V100 == V102, V101 == V103, V103 == V104, V104 == V105, V105 == V106, V106 == V107, V107 == V108, V102 == V109, V96 == V110, V108 == V112, V112 == V113, V113 == V114, V114 == V115, V115 == V116, V116 == V117, V117 == V118, V118 == V119, V119 == V120, V120 == V121, V121 == V122, V122 == V123, V123 == V124, V109 == V125, V110 == V126, V124 == V128, V128 == V129, V125 == V130, V129 == V131, V130 == V132, V131 == V133, V133 == V134, V134 == V135, V135 == V136, V136 == V137, V137 == V138, V138 == V139, V139 == V140, V140 == V141, V141 == V142, V132 == V143, V142 == V144, V144 == V145, V143 == V146, V126 == V147, V145 == V148, V146 == V149, V148 == V150, V150 == V191, V191 == V193, V193 == V195, V195 == V197, V197 == V199, V199 == V201, V201 == V203, V203 == V205, V205 == V207, V207 == V209, V209 == V211, V211 == V213, V213 == V215, V215 == V217, V217 == V219, V219 == V221, V221 == V223, V223 == V225, V225 == V227, V227 == V229, V229 == V231, V231 == V233, V233 == V235; #782 ), references = 1, size of lhs = 96:
% 21.25/21.48 P_z-{F}(V0), P_s-{F}(V0,V1), r-{F}(V1,V0), P_s-{F}(V2,V1), P_s-{F}(V1,V3), V1 == V3, V0 == V3, P_s-{F}(V4,V1), V4 == V3, P_s-{F}(V5,V3), V5 == V3, P_s-{F}(V6,V3), V6 == V3, P_s-{F}(V7,V3), V7 == V3, P_s-{F}(V8,V3), V8 == V3, P_s-{F}(V9,V3), V9 == V3, P_s-{F}(V10,V3), P_s-{F}(V11,V10), V11 == V3, P_s-{F}(V12,V3), P_s-{F}(V13,V12), V13 == V3, P_s-{F}(V14,V3), P_s-{F}(V15,V14), V15 == V3, P_s-{F}(V16,V3), P_s-{F}(V17,V16), V17 == V3, P_s-{F}(V18,V3), P_s-{F}(V19,V18), V19 == V3, P_s-{F}(V20,V3), P_s-{F}(V21,V20), V21 == V3, P_s-{F}(V22,V3), P_s-{F}(V23,V22), V23 == V3, P_s-{F}(V24,V3), P_s-{F}(V25,V24), V25 == V3, P_s-{F}(V26,V3), P_s-{F}(V27,V26), V27 == V3, P_s-{F}(V28,V3), P_s-{F}(V29,V28), V29 == V3, P_s-{F}(V30,V3), P_s-{F}(V31,V30), V31 == V3, P_s-{F}(V32,V3), P_s-{F}(V33,V32), V33 == V3, P_s-{F}(V34,V3), P_s-{F}(V35,V34), V35 == V3, P_s-{F}(V36,V3), P_s-{F}(V37,V36), V37 == V3, P_s-{F}(V38,V3), P_s-{F}(V39,V38), V39 == V3, P_s-{F}(V40,V3), P_s-{F}(V41,V40), V41 == V3, P_s-{F}(V42,V3), P_s-{F}(V43,V42), V43 == V3, P_s-{F}(V44,V3), P_s-{F}(V45,V44), P_s-{F}(V46,V3), P_s-{F}(V47,V46), P_s-{F}(V48,V3), P_s-{F}(V49,V48), P_s-{F}(V50,V3), P_s-{F}(V51,V50), P_s-{F}(V52,V3), P_s-{F}(V53,V52), P_s-{F}(V54,V3), P_s-{F}(V55,V54), P_s-{F}(V56,V3), P_s-{F}(V57,V56), P_s-{F}(V58,V3), P_s-{F}(V59,V58), P_s-{F}(V60,V3), P_s-{F}(V61,V60), P_s-{F}(V62,V3), P_s-{F}(V63,V62), P_s-{F}(V64,V3), P_s-{F}(V65,V64), P_s-{F}(V66,V3), P_s-{F}(V67,V66), P_s-{F}(V68,V3), P_s-{F}(V69,V68) | P_s-{T}(V3,V0), P_s-{T}(V3,V2), P_s-{T}(V3,V47), P_s-{T}(V3,V49), P_s-{T}(V3,V55), P_s-{T}(V3,V51), P_s-{T}(V3,V53), P_s-{T}(V3,V45), P_s-{T}(V3,V57), P_s-{T}(V3,V59), P_s-{T}(V3,V61), P_s-{T}(V3,V63), P_s-{T}(V3,V65), P_s-{T}(V3,V67), P_s-{T}(V3,V69)
% 21.25/21.48 (used 0 times, uses = {})
% 21.25/21.48
% 21.25/21.48 #1144: mergings( V0 == V1, V1 == V2, V2 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10, V10 == V11, V11 == V12, V12 == V13, V13 == V14, V14 == V15, V15 == V16, V16 == V17, V17 == V18, V18 == V19, V19 == V20, V20 == V21, V21 == V22, V22 == V23, V23 == V24, V24 == V25, V25 == V26, V26 == V27, V27 == V28, V28 == V29, V29 == V30, V30 == V31, V31 == V32, V32 == V33, V33 == V34, V34 == V35, V35 == V36, V36 == V37, V37 == V38, V38 == V39, V39 == V40, V40 == V41, V41 == V42, V42 == V43, V43 == V45, V45 == V46, V46 == V47, V47 == V48, V48 == V49, V49 == V50, V50 == V51, V51 == V52, V52 == V53, V53 == V54, V54 == V55, V55 == V56, V56 == V57, V57 == V58, V58 == V59, V59 == V60, V60 == V61, V61 == V62, V62 == V63, V63 == V64, V64 == V65, V65 == V66, V66 == V67, V67 == V68, V68 == V69, V69 == V70, V70 == V71, V71 == V72, V72 == V73, V73 == V74, V74 == V75, V75 == V76, V76 == V77, V44 == V78, V77 == V80, V78 == V81, V80 == V82, V81 == V83, V82 == V84, V84 == V85, V85 == V87, V87 == V88, V88 == V89, V89 == V90, V90 == V91, V91 == V92, V92 == V93, V93 == V94, V83 == V95, V79 == V96, V94 == V97, V97 == V98, V95 == V99, V98 == V100, V99 == V101, V100 == V102, V102 == V103, V103 == V104, V104 == V105, V105 == V106, V106 == V107, V101 == V108, V96 == V109, V107 == V110, V110 == V111, V111 == V112, V112 == V113, V113 == V114, V114 == V115, V115 == V116, V116 == V117, V117 == V118, V118 == V119, V119 == V120, V120 == V121, V121 == V122, V108 == V123, V109 == V124, V122 == V125, V125 == V126, V123 == V127, V126 == V128, V127 == V129, V128 == V130, V130 == V131, V131 == V132, V132 == V133, V133 == V134, V134 == V135, V135 == V136, V136 == V137, V137 == V138, V138 == V139, V129 == V140, V139 == V141, V141 == V142, V140 == V143, V124 == V144, V142 == V145, V143 == V146, V145 == V147, V147 == V148, V148 == V150, V150 == V152, V152 == V153, V153 == V154, V154 == V155, V155 == V156, V156 == V158, V158 == V159, V159 == V160, V160 == V161, V161 == V162, V162 == V163, V163 == V164, V164 == V166, V166 == V168, V168 == V169, V169 == V170, V170 == V171, V171 == V172, V172 == V173, V173 == V174, V174 == V176, V176 == V86, V86 == V214, V146 == V213, V214 == V216, V213 == V215, V216 == V222, V215 == V221, V222 == V218, V221 == V217, V218 == V220, V217 == V219, V220 == V212, V219 == V211, V212 == V224, V211 == V223, V224 == V226, V223 == V225, V226 == V228, V225 == V227, V228 == V230, V227 == V229, V230 == V232, V229 == V231, V232 == V234, V231 == V233; #951 ), references = 1, size of lhs = 71:
% 21.25/21.48 P_z-{F}(V0), P_s-{F}(V0,V1), r-{F}(V1,V0), P_s-{F}(V2,V1), P_s-{F}(V1,V3), V1 == V3, V0 == V3, V2 == V3, P_s-{F}(V4,V3), V4 == V3, P_s-{F}(V5,V3), V5 == V3, P_s-{F}(V6,V3), V6 == V3, P_s-{F}(V7,V3), V7 == V3, P_s-{F}(V8,V3), V8 == V3, P_s-{F}(V9,V3), P_s-{F}(V10,V9), V10 == V3, P_s-{F}(V11,V3), P_s-{F}(V12,V11), V12 == V3, P_s-{F}(V13,V3), P_s-{F}(V14,V13), V14 == V3, P_s-{F}(V15,V3), P_s-{F}(V16,V15), V16 == V3, P_s-{F}(V17,V3), P_s-{F}(V18,V17), V18 == V3, P_s-{F}(V19,V3), P_s-{F}(V20,V19), V20 == V3, P_s-{F}(V21,V3), P_s-{F}(V22,V21), V22 == V3, P_s-{F}(V23,V3), P_s-{F}(V24,V23), V24 == V3, P_s-{F}(V25,V3), P_s-{F}(V26,V25), V26 == V3, P_s-{F}(V27,V3), P_s-{F}(V28,V27), V28 == V3, P_s-{F}(V29,V3), P_s-{F}(V30,V29), V30 == V3, P_s-{F}(V31,V3), P_s-{F}(V32,V31), V32 == V3, P_s-{F}(V33,V3), P_s-{F}(V34,V33), V34 == V3, P_s-{F}(V35,V3), P_s-{F}(V36,V35), V36 == V3, P_s-{F}(V37,V3), P_s-{F}(V38,V37), V38 == V3, P_s-{F}(V39,V3), P_s-{F}(V40,V39), V40 == V3, P_s-{F}(V41,V3), P_s-{F}(V42,V41), V42 == V3, P_s-{F}(V43,V3), P_s-{F}(V44,V43) | P_s-{T}(V3,V44)
% 21.25/21.48 (used 0 times, uses = {})
% 21.25/21.48
% 21.25/21.48 #1339: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10, V10 == V11, V11 == V12, V12 == V13, V13 == V14, V14 == V15, V15 == V16, V16 == V17, V17 == V18, V18 == V19, V19 == V20, V20 == V21, V21 == V22, V22 == V23, V23 == V24, V24 == V25, V25 == V26, V26 == V27, V27 == V28, V28 == V29, V29 == V30, V30 == V31, V31 == V32, V32 == V33, V33 == V34, V34 == V35, V35 == V36, V36 == V37, V37 == V38, V38 == V39, V39 == V40, V40 == V41, V41 == V42, V42 == V43, V43 == V44, V44 == V45, V45 == V46, V46 == V47, V47 == V48, V48 == V49, V49 == V50, V50 == V51, V51 == V52, V52 == V53, V53 == V54, V54 == V55, V55 == V56, V56 == V57, V57 == V58, V58 == V59, V59 == V60, V60 == V61, V61 == V62, V62 == V63, V63 == V64, V64 == V65, V65 == V66, V66 == V67, V67 == V68, V68 == V69, V69 == V70, V70 == V71, V71 == V72, V72 == V73, V73 == V2, V2 == V74, V74 == V75, V1 == V76, V75 == V78, V76 == V79, V78 == V80, V79 == V81, V80 == V82, V82 == V83, V83 == V84, V84 == V85, V85 == V86, V86 == V87, V87 == V88, V88 == V89, V89 == V90, V90 == V91, V81 == V92, V77 == V93, V91 == V94, V94 == V95, V92 == V96, V95 == V97, V96 == V98, V97 == V99, V99 == V100, V100 == V101, V101 == V102, V102 == V103, V103 == V104, V98 == V105, V93 == V106, V104 == V107, V107 == V108, V108 == V109, V109 == V110, V110 == V111, V111 == V112, V112 == V113, V113 == V114, V114 == V115, V115 == V116, V116 == V117, V117 == V118, V118 == V119, V105 == V120, V106 == V121, V119 == V122, V122 == V123, V120 == V124, V123 == V125, V124 == V126, V125 == V127, V127 == V128, V128 == V129, V129 == V130, V130 == V131, V131 == V132, V132 == V133, V133 == V134, V134 == V135, V135 == V136, V126 == V137, V136 == V138, V138 == V139, V137 == V140, V121 == V141, V139 == V142, V140 == V143, V142 == V144, V144 == V145, V145 == V147, V147 == V149, V149 == V150, V150 == V151, V151 == V152, V152 == V153, V153 == V155, V155 == V156, V156 == V157, V157 == V158, V158 == V159, V159 == V160, V160 == V161, V161 == V163, V163 == V165, V165 == V166, V166 == V167, V167 == V168, V168 == V169, V169 == V170, V170 == V171, V171 == V173, V173 == V174, V174 == V175, V143 == V176, V175 == V177, V176 == V178, V177 == V179, V178 == V180, V179 == V181, V180 == V182, V181 == V183, V182 == V184, V183 == V185, V184 == V186, V185 == V187, V186 == V188, V187 == V189, V188 == V190, V189 == V191, V190 == V192, V191 == V193, V192 == V194, V193 == V195, V194 == V196, V195 == V197, V196 == V198, V197 == V199, V198 == V200; #1146 ), references = 2, size of lhs = 69:
% 21.25/21.48 P_z-{F}(V0), P_s-{F}(V0,V1), V1 == V0, P_s-{F}(V2,V1), P_s-{F}(V1,V3), V1 == V3, V0 == V3, V2 == V3, P_s-{F}(V4,V3), V4 == V3, P_s-{F}(V5,V3), V5 == V3, P_s-{F}(V6,V3), V6 == V3, P_s-{F}(V7,V3), V7 == V3, P_s-{F}(V8,V3), V8 == V3, P_s-{F}(V9,V3), P_s-{F}(V10,V9), V10 == V3, P_s-{F}(V11,V3), P_s-{F}(V12,V11), V12 == V3, P_s-{F}(V13,V3), P_s-{F}(V14,V13), V14 == V3, P_s-{F}(V15,V3), P_s-{F}(V16,V15), V16 == V3, P_s-{F}(V17,V3), P_s-{F}(V18,V17), V18 == V3, P_s-{F}(V19,V3), P_s-{F}(V20,V19), V20 == V3, P_s-{F}(V21,V3), P_s-{F}(V22,V21), V22 == V3, P_s-{F}(V23,V3), P_s-{F}(V24,V23), V24 == V3, P_s-{F}(V25,V3), P_s-{F}(V26,V25), V26 == V3, P_s-{F}(V27,V3), P_s-{F}(V28,V27), V28 == V3, P_s-{F}(V29,V3), P_s-{F}(V30,V29), V30 == V3, P_s-{F}(V31,V3), P_s-{F}(V32,V31), V32 == V3, P_s-{F}(V33,V3), P_s-{F}(V34,V33), V34 == V3, P_s-{F}(V35,V3), P_s-{F}(V36,V35), V36 == V3, P_s-{F}(V37,V3), P_s-{F}(V38,V37), V38 == V3, P_s-{F}(V39,V3), P_s-{F}(V40,V39), V40 == V3, P_s-{F}(V41,V3), P_s-{F}(V42,V41), V42 == V3 | b-{T}(V1,V0)
% 21.25/21.48 (used 0 times, uses = {})
% 21.25/21.48
% 21.25/21.48 #1342: mergings( V0 == V3; #1340 ), references = 7, size of lhs = 4:
% 21.25/21.48 P_z-{F}(V0), r-{F}(V1,V2), r-{F}(V2,V3), V1 == V3 | b-{T}(V1,V3)
% 21.25/21.48 (used 0 times, uses = {})
% 21.25/21.48
% 21.25/21.48 #1349: mergings( V0 == V3, V3 == V4, V4 == V5; #1345 ), references = 2, size of lhs = 13:
% 21.25/21.48 P_z-{F}(V0), b-{F}(V1,V2), r-{F}(V3,V2), r-{F}(V2,V4), V4 == V2, b-{F}(V5,V4), r-{F}(V5,V2), #-{F} V6, V1 == V6, V6 == V2, V6 == V3, V4 == V6, V5 == V6 | r-{T}(V1,V6)
% 21.25/21.48 (used 0 times, uses = {})
% 21.25/21.48
% 21.25/21.48 #1363: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10; #1354 ), references = 2, size of lhs = 24:
% 21.25/21.48 P_z-{F}(V0), b-{F}(V1,V2), r-{F}(V2,V3), V3 == V2, r-{F}(V1,V4), V4 == V1, b-{F}(V2,V4), r-{F}(V5,V3), r-{F}(V3,V6), V6 == V3, b-{F}(V7,V6), r-{F}(V7,V3), #-{F} V8, V8 == V2, V8 == V3, #-{F} V9, V1 == V9, V8 == V9, V9 == V3, V9 == V5, V6 == V9, V7 == V9, V4 == V9, V2 == V9 | b-{T}(V8,V2)
% 21.25/21.48 (used 0 times, uses = {})
% 21.25/21.48
% 21.25/21.48 #1366: mergings( V0 == V3; #1364 ), references = 2, size of lhs = 7:
% 21.25/21.48 P_z-{F}(V0), b-{F}(V1,V2), b-{F}(V3,V2), V3 == V1, b-{F}(V2,V4), b-{F}(V1,V5), b-{F}(V5,V4) | r-{T}(V3,V1)
% 21.25/21.48 (used 0 times, uses = {})
% 21.25/21.48
% 21.25/21.48 #1374: mergings( V2 == V3, V3 == V4, V4 == V5; #1370 ), references = 1, size of lhs = 30:
% 21.25/21.48 P_z-{F}(V0), b-{F}(V1,V2), r-{F}(V2,V3), V3 == V2, r-{F}(V1,V4), V4 == V1, b-{F}(V2,V4), r-{F}(V5,V3), r-{F}(V3,V6), V6 == V3, b-{F}(V7,V6), r-{F}(V7,V3), b-{F}(V8,V2), b-{F}(V2,V9), b-{F}(V8,V10), b-{F}(V10,V9), r-{F}(V8,V11), b-{F}(V11,V2), b-{F}(V2,V12), b-{F}(V11,V13), b-{F}(V13,V12), #-{F} V14, #-{F} V15, V1 == V15, V15 == V3, V15 == V5, V6 == V15, V7 == V15, V4 == V15, V2 == V15 | P_s-{T}(V14,V2), P_s-{T}(V14,V3), P_s-{T}(V14,V8), P_s-{T}(V14,V11), P_s-{T}(V14,V15)
% 21.25/21.48 (used 0 times, uses = {})
% 21.25/21.48
% 21.25/21.48 #1383: mergings( V0 == V1, V1 == V2, V2 == V3, V3 == V19, V19 == V21, V21 == V23, V23 == V25; #1375 ), references = 2, size of lhs = 37:
% 21.25/21.48 P_z-{F}(V0), b-{F}(V1,V2), r-{F}(V2,V3), V3 == V2, r-{F}(V1,V4), V4 == V1, b-{F}(V2,V4), r-{F}(V5,V3), r-{F}(V3,V6), V6 == V3, b-{F}(V7,V6), r-{F}(V7,V3), b-{F}(V2,V8), b-{F}(V2,V9), P_s-{F}(V10,V3), b-{F}(V11,V2), b-{F}(V11,V12), b-{F}(V12,V8), r-{F}(V11,V13), b-{F}(V13,V2), b-{F}(V13,V14), b-{F}(V14,V9), P_s-{F}(V15,V11), P_s-{F}(V16,V13), P_s-{F}(V17,V18), V1 == V18, V18 == V3, V18 == V5, V6 == V18, V7 == V18, V4 == V18, V2 == V18, #-{F} V19, V10 == V19, V15 == V19, V16 == V19, V17 == V19 | P_s-{T}(V19,V2)
% 21.25/21.48 (used 0 times, uses = {})
% 21.25/21.48
% 21.25/21.48 #1408: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10, V10 == V11, V11 == V12, V12 == V13, V13 == V14, V14 == V15, V15 == V16, V16 == V17, V17 == V18, V18 == V19, V19 == V20, V20 == V21, V21 == V22; #1387 ), references = 3, size of lhs = 26:
% 21.25/21.48 P_z-{F}(V0), r-{F}(V0,V1), V1 == V0, b-{F}(V1,V0), r-{F}(V2,V1), r-{F}(V3,V1), P_s-{F}(V4,V1), P_s-{F}(V5,V1), P_s-{F}(V6,V7), V7 == V0, V7 == V1, P_s-{F}(V8,V9), V9 == V1, V9 == V3, V7 == V9, V0 == V9, #-{F} V10, V10 == V1, V10 == V2, V7 == V10, V0 == V10, #-{F} V11, V4 == V11, V5 == V11, V6 == V11, V8 == V11 | b-{T}(V1,V7)
% 21.25/21.48 (used 0 times, uses = {})
% 21.25/21.48
% 21.25/21.48 #1415: mergings( V0 == V3, V3 == V4, V4 == V5; #1411 ), references = 2, size of lhs = 8:
% 21.25/21.48 P_z-{F}(V0), b-{F}(V1,V2), b-{F}(V1,V3), V3 == V2, b-{F}(V4,V3), b-{F}(V4,V2), r-{F}(V2,V5), V3 == V5 | r-{T}(V2,V3)
% 21.25/21.48 (used 0 times, uses = {})
% 21.25/21.48
% 21.25/21.48 #1450: mergings( V2 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10, V10 == V11, V11 == V12, V12 == V13, V13 == V14, V14 == V15, V15 == V16, V16 == V17, V17 == V18, V18 == V19, V19 == V20, V20 == V21, V21 == V22, V22 == V28, V28 == V33, V33 == V34, V34 == V35, V35 == V36, V36 == V37, V37 == V38, V38 == V39; #1421 ), references = 1, size of lhs = 29:
% 21.25/21.48 P_z-{F}(V0), r-{F}(V0,V1), V1 == V0, b-{F}(V1,V0), r-{F}(V2,V1), r-{F}(V3,V1), P_s-{F}(V4,V1), P_s-{F}(V5,V1), r-{F}(V6,V1), r-{F}(V7,V1), P_s-{F}(V8,V1), P_s-{F}(V9,V1), b-{F}(V1,V10), r-{F}(V10,V11), r-{F}(V10,V12), P_s-{F}(V13,V14), V14 == V0, V14 == V1, V14 == V10, V14 == V11, P_s-{F}(V15,V16), V16 == V1, V16 == V7, V0 == V16, #-{F} V17, #-{F} V18, V18 == V1, V18 == V6, V0 == V18 | P_s-{T}(V17,V1), P_s-{T}(V17,V3), P_s-{T}(V17,V14), P_s-{T}(V17,V0), P_s-{T}(V17,V10), P_s-{T}(V17,V12), P_s-{T}(V17,V16), P_s-{T}(V17,V2), P_s-{T}(V17,V4), P_s-{T}(V17,V5), P_s-{T}(V17,V13), P_s-{T}(V17,V17), P_s-{T}(V17,V18), P_s-{T}(V17,V8), P_s-{T}(V17,V9), P_s-{T}(V17,V15)
% 21.25/21.48 (used 0 times, uses = {})
% 21.25/21.48
% 21.25/21.48 #1494: mergings( V0 == V1, V1 == V2, V2 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10, V10 == V11, V11 == V12, V12 == V13, V13 == V14, V14 == V15, V15 == V16, V16 == V17, V17 == V18, V18 == V19, V19 == V31, V31 == V32, V32 == V33, V33 == V34, V34 == V35, V35 == V36, V36 == V37, V37 == V47, V47 == V23, V23 == V20, V20 == V26, V26 == V38, V38 == V49, V49 == V51, V51 == V53, V53 == V22, V22 == V24, V24 == V25, V25 == V55, V55 == V57, V57 == V59, V59 == V29, V29 == V30; #1451 ), references = 1, size of lhs = 34:
% 21.25/21.48 P_z-{F}(V0), r-{F}(V0,V1), r-{F}(V0,V2), P_s-{F}(V3,V2), r-{F}(V0,V4), V4 == V0, b-{F}(V4,V0), P_s-{F}(V0,V4), r-{F}(V5,V4), r-{F}(V6,V4), P_s-{F}(V7,V4), P_s-{F}(V8,V9), V9 == V4, V9 == V6, V0 == V9, P_s-{F}(V10,V9), P_s-{F}(V11,V12), V12 == V4, V12 == V0, V12 == V1, P_s-{F}(V13,V12), P_s-{F}(V14,V13), P_s-{F}(V15,V16), V7 == V16, V11 == V16, V3 == V16, V10 == V16, V14 == V16, V15 == V16, P_s-{F}(V17,V18), V18 == V4, V18 == V5, V0 == V18, V17 == V16 | P_s-{T}(V16,V8)
% 21.25/21.48 (used 0 times, uses = {})
% 21.25/21.48
% 21.25/21.48 #1537: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10, V10 == V11, V11 == V12, V12 == V13, V13 == V14, V14 == V15, V15 == V16, V16 == V17, V17 == V18, V18 == V19, V19 == V20, V20 == V21, V21 == V22, V22 == V23, V23 == V24, V24 == V25, V25 == V26, V26 == V27, V27 == V28, V28 == V29, V29 == V30, V30 == V32, V32 == V33, V33 == V35, V35 == V1, V1 == V36, V36 == V37, V37 == V38, V38 == V39, V39 == V40, V40 == V41, V41 == V42, V42 == V43; #1496 ), references = 2, size of lhs = 28:
% 21.25/21.48 P_z-{F}(V0), P_s-{F}(V0,V1), V1 == V0, b-{F}(V1,V0), P_s-{F}(V2,V1), P_s-{F}(V3,V1), P_s-{F}(V4,V5), V5 == V1, V0 == V5, P_s-{F}(V6,V5), P_s-{F}(V7,V6), P_s-{F}(V8,V9), V9 == V0, V9 == V1, P_s-{F}(V10,V9), P_s-{F}(V11,V10), P_s-{F}(V12,V13), V2 == V13, V8 == V13, V3 == V13, V4 == V13, V11 == V13, V12 == V13, V7 == V13, P_s-{F}(V14,V15), V15 == V1, V0 == V15, V14 == V13 | b-{T}(V0,V1)
% 21.25/21.48 (used 0 times, uses = {})
% 21.25/21.48
% 21.25/21.48 #1544: mergings( V0 == V3, V3 == V4, V4 == V5; #1540 ), references = 1, size of lhs = 14:
% 21.25/21.48 P_z-{F}(V0), b-{F}(V1,V2), b-{F}(V2,V3), b-{F}(V1,V4), b-{F}(V4,V5), V1 == V5, V5 == V2, r-{F}(V5,V6), V6 == V5, b-{F}(V2,V6), #-{F} V7, V5 == V7, V6 == V7, V2 == V7 | r-{T}(V1,V5)
% 21.25/21.48 (used 0 times, uses = {})
% 21.25/21.48
% 21.25/21.48 #1551: mergings( V0 == V3, V3 == V4, V4 == V5; #1547 ), references = 3, size of lhs = 12:
% 21.25/21.48 P_z-{F}(V0), b-{F}(V1,V2), r-{F}(V3,V2), b-{F}(V1,V4), r-{F}(V4,V2), r-{F}(V5,V4), #-{F} V6, V1 == V6, V6 == V2, V6 == V3, V6 == V4, V6 == V5 | r-{T}(V1,V6)
% 21.25/21.48 (used 0 times, uses = {})
% 21.25/21.48
% 21.25/21.48 #1566: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V1; #1558 ), references = 2, size of lhs = 39:
% 21.25/21.48 P_z-{F}(V0), b-{F}(V1,V0), r-{F}(V0,V2), V2 == V0, r-{F}(V2,V0), r-{F}(V3,V2), r-{F}(V1,V4), V4 == V1, V4 == V0, V2 == V4, r-{F}(V5,V4), r-{F}(V5,V6), V0 == V6, V6 == V2, V6 == V3, V4 == V6, r-{F}(V7,V6), V4 == V7, P_s-{F}(V8,V2), b-{F}(V0,V9), V9 == V0, V4 == V9, r-{F}(V9,V6), b-{F}(V9,V2), b-{F}(V9,V10), P_s-{F}(V11,V4), r-{F}(V12,V4), b-{F}(V12,V0), P_s-{F}(V13,V12), P_s-{F}(V14,V15), V1 == V15, V15 == V2, V4 == V15, V0 == V15, #-{F} V16, V8 == V16, V13 == V16, V11 == V16, V14 == V16 | r-{T}(V0,V4)
% 21.25/21.48 (used 0 times, uses = {})
% 21.25/21.48
% 21.25/21.48 #1584: mergings( V2 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10, V10 == V11, V11 == V29, V29 == V30; #1572 ), references = 1, size of lhs = 47:
% 21.25/21.48 P_z-{F}(V0), b-{F}(V1,V0), r-{F}(V0,V2), V2 == V0, r-{F}(V2,V0), r-{F}(V3,V2), r-{F}(V1,V4), V4 == V1, V2 == V4, V4 == V0, P_s-{F}(V5,V2), b-{F}(V0,V6), V6 == V0, V4 == V6, b-{F}(V6,V2), r-{F}(V6,V4), b-{F}(V6,V0), b-{F}(V6,V7), r-{F}(V8,V7), b-{F}(V6,V9), r-{F}(V9,V7), r-{F}(V10,V9), b-{F}(V6,V11), P_s-{F}(V12,V4), r-{F}(V0,V13), V13 == V0, V4 == V13, r-{F}(V13,V0), r-{F}(V14,V13), V4 == V14, P_s-{F}(V15,V13), b-{F}(V0,V16), V16 == V0, r-{F}(V16,V4), b-{F}(V16,V13), b-{F}(V16,V17), r-{F}(V18,V0), V18 == V4, P_s-{F}(V19,V6), r-{F}(V20,V4), b-{F}(V20,V0), P_s-{F}(V21,V20), P_s-{F}(V22,V23), V6 == V23, V23 == V13, V0 == V23, #-{F} V24 | P_s-{T}(V24,V7), P_s-{T}(V24,V8), P_s-{T}(V24,V9), P_s-{T}(V24,V10), P_s-{T}(V24,V2), P_s-{T}(V24,V3), P_s-{T}(V24,V6), P_s-{T}(V24,V13), P_s-{T}(V24,V0), P_s-{T}(V24,V4), P_s-{T}(V24,V16), P_s-{T}(V24,V18), P_s-{T}(V24,V1), P_s-{T}(V24,V23), P_s-{T}(V24,V5), P_s-{T}(V24,V21), P_s-{T}(V24,V12), P_s-{T}(V24,V24), P_s-{T}(V24,V15), P_s-{T}(V24,V19), P_s-{T}(V24,V22)
% 21.25/21.48 (used 0 times, uses = {})
% 21.25/21.48
% 21.25/21.48 #1612: mergings( V0 == V1, V1 == V2, V2 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V27, V27 == V28, V28 == V36, V36 == V38, V38 == V40, V40 == V42, V42 == V44, V44 == V46, V46 == V48, V48 == V50, V50 == V52, V52 == V54, V54 == V56, V56 == V58, V58 == V60, V60 == V62, V62 == V64; #1585 ), references = 1, size of lhs = 76:
% 21.25/21.48 P_z-{F}(V0), r-{F}(V0,V1), V1 == V0, r-{F}(V1,V0), r-{F}(V2,V1), b-{F}(V0,V3), V3 == V0, b-{F}(V3,V1), b-{F}(V3,V0), r-{F}(V3,V4), V1 == V4, V4 == V0, V4 == V3, b-{F}(V3,V5), b-{F}(V3,V6), r-{F}(V6,V5), r-{F}(V7,V6), b-{F}(V3,V8), r-{F}(V0,V9), V9 == V0, V4 == V9, r-{F}(V9,V0), r-{F}(V10,V9), V4 == V10, b-{F}(V0,V11), V11 == V0, r-{F}(V11,V4), b-{F}(V11,V9), b-{F}(V11,V12), P_s-{F}(V13,V3), P_s-{F}(V14,V6), P_s-{F}(V15,V1), P_s-{F}(V16,V3), P_s-{F}(V17,V9), P_s-{F}(V18,V4), P_s-{F}(V19,V11), b-{F}(V20,V0), V4 == V20, r-{F}(V20,V4), P_s-{F}(V21,V20), P_s-{F}(V22,V1), P_s-{F}(V23,V22), r-{F}(V24,V5), P_s-{F}(V25,V24), P_s-{F}(V26,V4), P_s-{F}(V27,V26), P_s-{F}(V28,V9), P_s-{F}(V29,V28), r-{F}(V30,V0), V30 == V4, P_s-{F}(V31,V30), r-{F}(V32,V4), b-{F}(V32,V0), P_s-{F}(V33,V32), P_s-{F}(V34,V35), V3 == V35, V35 == V9, V0 == V35, P_s-{F}(V36,V35), P_s-{F}(V37,V36), P_s-{F}(V38,V39), V25 == V39, V14 == V39, V15 == V39, V16 == V39, V17 == V39, V18 == V39, V19 == V39, V31 == V39, V21 == V39, V34 == V39, V23 == V39, V27 == V39, V38 == V39, V29 == V39, V37 == V39 | P_s-{T}(V39,V5), P_s-{T}(V39,V7), P_s-{T}(V39,V2), P_s-{T}(V39,V0), P_s-{T}(V39,V33), P_s-{T}(V39,V13)
% 21.25/21.48 (used 0 times, uses = {})
% 21.25/21.48
% 21.25/21.48 #1644: mergings( V0 == V1, V1 == V2, V2 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V22, V22 == V23, V23 == V25, V25 == V26, V26 == V28, V28 == V30, V30 == V32, V32 == V34, V34 == V36, V36 == V38, V38 == V39, V39 == V40, V40 == V41, V41 == V42, V42 == V43, V43 == V44, V44 == V45, V45 == V14, V14 == V16, V16 == V11, V11 == V9, V9 == V59; #1613 ), references = 1, size of lhs = 74:
% 21.25/21.48 P_z-{F}(V0), r-{F}(V0,V1), r-{F}(V1,V0), P_s-{F}(V2,V1), r-{F}(V0,V3), V3 == V0, r-{F}(V3,V0), b-{F}(V0,V4), V4 == V0, b-{F}(V4,V3), b-{F}(V4,V0), b-{F}(V4,V1), r-{F}(V4,V5), V3 == V5, V5 == V0, V5 == V4, b-{F}(V4,V6), r-{F}(V0,V7), V7 == V0, V5 == V7, r-{F}(V7,V0), r-{F}(V8,V7), V5 == V8, b-{F}(V0,V9), V9 == V0, r-{F}(V9,V5), b-{F}(V9,V7), b-{F}(V9,V10), P_s-{F}(V11,V4), P_s-{F}(V12,V3), P_s-{F}(V13,V4), P_s-{F}(V14,V7), P_s-{F}(V15,V5), P_s-{F}(V16,V9), P_s-{F}(V0,V17), r-{F}(V17,V5), b-{F}(V17,V0), b-{F}(V18,V0), V5 == V18, r-{F}(V18,V5), P_s-{F}(V19,V18), P_s-{F}(V20,V3), P_s-{F}(V21,V20), r-{F}(V22,V0), P_s-{F}(V23,V22), P_s-{F}(V24,V5), P_s-{F}(V25,V24), P_s-{F}(V26,V7), P_s-{F}(V27,V26), r-{F}(V28,V0), V28 == V5, P_s-{F}(V29,V28), P_s-{F}(V30,V31), V4 == V31, V31 == V7, V0 == V31, P_s-{F}(V32,V31), P_s-{F}(V33,V32), P_s-{F}(V34,V35), V23 == V35, V2 == V35, V12 == V35, V13 == V35, V14 == V35, V15 == V35, V16 == V35, V29 == V35, V19 == V35, V30 == V35, V21 == V35, V25 == V35, V34 == V35, V27 == V35, V33 == V35 | P_s-{T}(V35,V11)
% 21.25/21.48 (used 0 times, uses = {})
% 21.25/21.48
% 21.25/21.48 #1688: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10, V10 == V11, V11 == V12, V12 == V13, V13 == V14, V14 == V15, V15 == V16, V16 == V17, V17 == V18, V18 == V19, V19 == V20, V20 == V21, V21 == V22, V22 == V23, V23 == V24, V24 == V25, V25 == V26, V26 == V27, V27 == V28, V28 == V29, V29 == V30, V30 == V31, V31 == V32, V32 == V33, V33 == V34, V34 == V35, V35 == V36, V36 == V37, V37 == V38, V38 == V49, V49 == V50; #1649 ), references = 4, size of lhs = 58:
% 21.25/21.48 P_z-{F}(V0), b-{F}(V0,V1), b-{F}(V0,V2), b-{F}(V2,V0), b-{F}(V2,V3), b-{F}(V0,V4), V4 == V0, b-{F}(V4,V0), P_s-{F}(V0,V4), b-{F}(V4,V5), b-{F}(V4,V6), P_s-{F}(V7,V4), P_s-{F}(V8,V4), P_s-{F}(V9,V4), P_s-{F}(V10,V11), V4 == V11, V0 == V11, V11 == V2, P_s-{F}(V12,V11), P_s-{F}(V13,V11), P_s-{F}(V14,V11), P_s-{F}(V15,V11), P_s-{F}(V16,V11), P_s-{F}(V17,V16), P_s-{F}(V18,V11), P_s-{F}(V19,V18), P_s-{F}(V20,V21), V21 == V0, V21 == V4, V11 == V21, P_s-{F}(V22,V21), P_s-{F}(V23,V22), P_s-{F}(V24,V25), V4 == V25, V25 == V11, V0 == V25, P_s-{F}(V26,V25), P_s-{F}(V27,V26), P_s-{F}(V28,V29), V14 == V29, V10 == V29, V12 == V29, V7 == V29, V13 == V29, V20 == V29, V8 == V29, V15 == V29, V9 == V29, V24 == V29, V17 == V29, V23 == V29, V28 == V29, V19 == V29, V27 == V29, #-{F} V30, V11 == V30, V0 == V30, V2 == V30 | r-{T}(V4,V11)
% 21.25/21.48 (used 0 times, uses = {})
% 21.25/21.48
% 21.25/21.48 #1702: mergings( V2 == V12, V12 == V13, V13 == V14; #1697 ), references = 1, size of lhs = 38:
% 21.25/21.48 P_z-{F}(V0), b-{F}(V0,V1), b-{F}(V0,V2), b-{F}(V2,V0), b-{F}(V2,V3), b-{F}(V0,V4), V4 == V0, b-{F}(V4,V0), P_s-{F}(V0,V4), b-{F}(V4,V5), b-{F}(V4,V6), P_s-{F}(V7,V4), P_s-{F}(V8,V4), P_s-{F}(V9,V4), r-{F}(V4,V10), b-{F}(V10,V11), r-{F}(V12,V11), V11 == V12, b-{F}(V12,V13), r-{F}(V14,V13), b-{F}(V12,V15), r-{F}(V15,V13), r-{F}(V16,V15), P_s-{F}(V17,V18), P_s-{F}(V19,V18), P_s-{F}(V20,V21), V21 == V0, V21 == V4, P_s-{F}(V22,V21), P_s-{F}(V23,V22), P_s-{F}(V24,V25), V4 == V25, V0 == V25, P_s-{F}(V26,V25), P_s-{F}(V27,V26), #-{F} V28, V0 == V28, V2 == V28 | P_s-{T}(V18,V4), P_s-{T}(V18,V0), P_s-{T}(V18,V2), P_s-{T}(V18,V12), P_s-{T}(V18,V13), P_s-{T}(V18,V14), P_s-{T}(V18,V15), P_s-{T}(V18,V16), P_s-{T}(V18,V11), P_s-{T}(V18,V10), P_s-{T}(V18,V21), P_s-{T}(V18,V25), P_s-{T}(V18,V18), P_s-{T}(V18,V7), P_s-{T}(V18,V20), P_s-{T}(V18,V8), P_s-{T}(V18,V9), P_s-{T}(V18,V24), P_s-{T}(V18,V17), P_s-{T}(V18,V23), P_s-{T}(V18,V19), P_s-{T}(V18,V27), P_s-{T}(V18,V28)
% 21.25/21.48 (used 0 times, uses = {})
% 21.25/21.48
% 21.25/21.48 #1731: mergings( V10 == V11, V11 == V12, V12 == V32, V32 == V0, V0 == V34, V34 == V15, V15 == V36, V36 == V38, V38 == V40, V40 == V42, V42 == V44, V44 == V46, V46 == V48, V48 == V50, V50 == V52, V52 == V7, V7 == V54, V54 == V8, V8 == V9, V9 == V56, V56 == V58, V58 == V26, V4 == V25, V26 == V60, V60 == V30, V25 == V29, V24 == V28; #1703 ), references = 1, size of lhs = 60:
% 21.25/21.48 P_z-{F}(V0), b-{F}(V0,V1), b-{F}(V0,V2), b-{F}(V2,V0), b-{F}(V2,V3), b-{F}(V0,V4), V4 == V0, b-{F}(V4,V0), P_s-{F}(V0,V4), b-{F}(V4,V5), b-{F}(V4,V6), r-{F}(V4,V7), b-{F}(V7,V8), V8 == V0, r-{F}(V0,V8), P_s-{F}(V9,V4), P_s-{F}(V10,V2), b-{F}(V0,V11), b-{F}(V0,V12), r-{F}(V12,V11), P_s-{F}(V13,V11), P_s-{F}(V14,V12), P_s-{F}(V15,V8), P_s-{F}(V16,V7), P_s-{F}(V4,V17), V4 == V17, V0 == V17, P_s-{F}(V18,V17), P_s-{F}(V19,V17), r-{F}(V20,V11), P_s-{F}(V21,V20), r-{F}(V22,V12), P_s-{F}(V23,V22), P_s-{F}(V24,V17), P_s-{F}(V25,V24), P_s-{F}(V26,V17), P_s-{F}(V27,V26), P_s-{F}(V28,V29), V9 == V29, V10 == V29, V13 == V29, V21 == V29, V14 == V29, V23 == V29, V15 == V29, V16 == V29, V18 == V29, V19 == V29, V28 == V29, V25 == V29, V27 == V29, P_s-{F}(V30,V29), P_s-{F}(V31,V30), V31 == V29, P_s-{F}(V32,V29), P_s-{F}(V33,V32), V33 == V29, #-{F} V34, V0 == V34, V2 == V34 | P_s-{T}(V29,V34)
% 21.25/21.48 (used 0 times, uses = {})
% 21.25/21.48
% 21.25/21.48 #1768: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V21, V21 == V1, V1 == V23, V23 == V25, V25 == V26, V26 == V28, V28 == V29, V29 == V31, V31 == V33, V33 == V34, V34 == V35, V35 == V36, V36 == V37, V37 == V38, V38 == V39, V39 == V40, V40 == V41, V41 == V42, V12 == V43, V42 == V46, V46 == V47, V43 == V48, V44 == V49, V47 == V51; #1736 ), references = 2, size of lhs = 65:
% 21.25/21.48 P_z-{F}(V0), b-{F}(V0,V1), b-{F}(V1,V0), b-{F}(V1,V2), b-{F}(V0,V3), V3 == V0, b-{F}(V3,V0), P_s-{F}(V0,V3), b-{F}(V3,V4), b-{F}(V3,V5), r-{F}(V3,V6), V0 == V6, r-{F}(V7,V6), r-{F}(V7,V8), V6 == V8, V8 == V0, r-{F}(V9,V8), V6 == V9, P_s-{F}(V10,V3), P_s-{F}(V11,V1), b-{F}(V0,V12), V6 == V12, r-{F}(V12,V8), r-{F}(V12,V6), b-{F}(V12,V13), P_s-{F}(V14,V6), P_s-{F}(V15,V12), P_s-{F}(V16,V8), P_s-{F}(V17,V6), P_s-{F}(V3,V18), V3 == V18, V0 == V18, P_s-{F}(V19,V18), P_s-{F}(V20,V18), P_s-{F}(V21,V6), r-{F}(V22,V6), P_s-{F}(V23,V22), P_s-{F}(V24,V18), P_s-{F}(V25,V24), P_s-{F}(V26,V18), P_s-{F}(V27,V26), P_s-{F}(V28,V29), V10 == V29, V11 == V29, V14 == V29, V23 == V29, V15 == V29, V21 == V29, V16 == V29, V17 == V29, V19 == V29, V20 == V29, V28 == V29, V25 == V29, V27 == V29, P_s-{F}(V30,V29), P_s-{F}(V31,V30), V31 == V29, P_s-{F}(V32,V29), P_s-{F}(V33,V32), V33 == V29, P_s-{F}(V34,V35), V0 == V35, V1 == V35, V34 == V29 | r-{T}(V0,V6)
% 21.25/21.48 (used 0 times, uses = {})
% 21.25/21.48
% 21.25/21.48 #1774: mergings( V2 == V12, V12 == V13; #1771 ), references = 1, size of lhs = 33:
% 21.25/21.48 P_z-{F}(V0), b-{F}(V0,V1), b-{F}(V0,V2), b-{F}(V2,V0), b-{F}(V2,V3), b-{F}(V0,V4), V4 == V0, b-{F}(V4,V0), P_s-{F}(V0,V4), b-{F}(V4,V5), b-{F}(V4,V6), P_s-{F}(V7,V4), P_s-{F}(V8,V4), P_s-{F}(V9,V4), r-{F}(V4,V10), V10 == V4, r-{F}(V4,V11), b-{F}(V11,V10), P_s-{F}(V12,V13), P_s-{F}(V14,V13), P_s-{F}(V15,V16), V16 == V0, V16 == V4, P_s-{F}(V17,V16), P_s-{F}(V18,V17), P_s-{F}(V19,V20), V4 == V20, V0 == V20, P_s-{F}(V21,V20), P_s-{F}(V22,V21), #-{F} V23, V0 == V23, V2 == V23 | P_s-{T}(V13,V4), P_s-{T}(V13,V0), P_s-{T}(V13,V2), P_s-{T}(V13,V10), P_s-{T}(V13,V11), P_s-{T}(V13,V16), P_s-{T}(V13,V20), P_s-{T}(V13,V13), P_s-{T}(V13,V7), P_s-{T}(V13,V15), P_s-{T}(V13,V8), P_s-{T}(V13,V9), P_s-{T}(V13,V19), P_s-{T}(V13,V12), P_s-{T}(V13,V18), P_s-{T}(V13,V14), P_s-{T}(V13,V22), P_s-{T}(V13,V23)
% 21.25/21.48 (used 0 times, uses = {})
% 21.25/21.48
% 21.25/21.48 #1790: mergings( V0 == V10, V10 == V11, V11 == V26, V26 == V28, V28 == V30, V30 == V32, V32 == V34, V34 == V36, V36 == V38, V38 == V40, V40 == V42, V42 == V44, V44 == V46, V46 == V48; #1775 ), references = 1, size of lhs = 56:
% 21.25/21.48 P_z-{F}(V0), b-{F}(V0,V1), b-{F}(V0,V2), b-{F}(V2,V0), b-{F}(V2,V3), b-{F}(V0,V4), V4 == V0, b-{F}(V4,V0), P_s-{F}(V0,V4), b-{F}(V4,V5), b-{F}(V4,V6), P_s-{F}(V7,V4), P_s-{F}(V8,V4), P_s-{F}(V9,V4), r-{F}(V4,V10), V10 == V4, r-{F}(V4,V11), b-{F}(V11,V10), P_s-{F}(V12,V4), P_s-{F}(V13,V2), P_s-{F}(V14,V10), P_s-{F}(V15,V11), P_s-{F}(V16,V17), P_s-{F}(V17,V18), V18 == V0, V18 == V4, P_s-{F}(V19,V18), P_s-{F}(V20,V18), P_s-{F}(V21,V20), P_s-{F}(V22,V23), P_s-{F}(V23,V24), V4 == V24, V0 == V24, P_s-{F}(V25,V24), P_s-{F}(V26,V24), P_s-{F}(V27,V26), P_s-{F}(V28,V29), V12 == V29, V13 == V29, V14 == V29, V15 == V29, V19 == V29, V25 == V29, V28 == V29, V21 == V29, V27 == V29, P_s-{F}(V30,V29), P_s-{F}(V31,V30), V31 == V29, P_s-{F}(V32,V29), P_s-{F}(V33,V32), V33 == V29, P_s-{F}(V34,V35), V0 == V35, V2 == V35, V34 == V29 | P_s-{T}(V29,V0), P_s-{T}(V29,V7), P_s-{T}(V29,V8), P_s-{T}(V29,V9), P_s-{T}(V29,V16), P_s-{T}(V29,V22)
% 21.25/21.48 (used 0 times, uses = {})
% 21.25/21.48
% 21.25/21.48 #1811: mergings( V10 == V11, V11 == V14, V14 == V16, V16 == V18, V18 == V20, V20 == V22, V22 == V23, V23 == V24, V24 == V25, V25 == V26, V26 == V27, V27 == V28, V28 == V29, V29 == V0, V0 == V7, V7 == V8, V8 == V9, V9 == V30, V4 == V31; #1791 ), references = 1, size of lhs = 52:
% 21.25/21.48 P_z-{F}(V0), b-{F}(V0,V1), b-{F}(V0,V2), b-{F}(V2,V0), b-{F}(V2,V3), b-{F}(V0,V4), V4 == V0, b-{F}(V4,V0), P_s-{F}(V0,V4), b-{F}(V4,V5), b-{F}(V4,V6), r-{F}(V4,V7), V7 == V4, r-{F}(V4,V8), b-{F}(V8,V7), P_s-{F}(V9,V4), P_s-{F}(V10,V2), P_s-{F}(V11,V7), P_s-{F}(V12,V8), P_s-{F}(V4,V13), V13 == V0, V13 == V4, P_s-{F}(V14,V13), P_s-{F}(V15,V13), P_s-{F}(V16,V15), P_s-{F}(V17,V18), P_s-{F}(V18,V19), V4 == V19, V0 == V19, P_s-{F}(V20,V19), P_s-{F}(V21,V19), P_s-{F}(V22,V21), P_s-{F}(V23,V24), V9 == V24, V10 == V24, V11 == V24, V12 == V24, V14 == V24, V20 == V24, V23 == V24, V16 == V24, V22 == V24, P_s-{F}(V25,V24), P_s-{F}(V26,V25), V26 == V24, P_s-{F}(V27,V24), P_s-{F}(V28,V27), V28 == V24, P_s-{F}(V29,V30), V0 == V30, V2 == V30, V29 == V24 | P_s-{T}(V24,V17)
% 21.25/21.48 (used 0 times, uses = {})
% 21.25/21.48
% 21.25/21.48 #1839: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10, V10 == V11, V11 == V12, V12 == V13, V13 == V14, V14 == V15, V15 == V16, V16 == V17, V17 == V18, V18 == V30, V30 == V31, V31 == V32, V32 == V33, V22 == V34, V33 == V37, V34 == V38, V35 == V39; #1814 ), references = 1, size of lhs = 50:
% 21.25/21.48 P_z-{F}(V0), b-{F}(V0,V1), b-{F}(V0,V2), b-{F}(V2,V0), b-{F}(V2,V3), b-{F}(V0,V4), V4 == V0, b-{F}(V4,V0), P_s-{F}(V0,V4), b-{F}(V4,V5), b-{F}(V4,V6), r-{F}(V4,V7), V7 == V4, r-{F}(V4,V8), V8 == V7, r-{F}(V9,V7), V8 == V9, P_s-{F}(V10,V4), P_s-{F}(V11,V2), P_s-{F}(V12,V7), P_s-{F}(V13,V8), P_s-{F}(V4,V14), V4 == V14, V0 == V14, P_s-{F}(V15,V14), P_s-{F}(V16,V14), P_s-{F}(V17,V14), P_s-{F}(V18,V17), P_s-{F}(V19,V14), P_s-{F}(V20,V19), P_s-{F}(V21,V22), V10 == V22, V11 == V22, V12 == V22, V13 == V22, V15 == V22, V16 == V22, V21 == V22, V18 == V22, V20 == V22, P_s-{F}(V23,V22), P_s-{F}(V24,V23), V24 == V22, P_s-{F}(V25,V22), P_s-{F}(V26,V25), V26 == V22, P_s-{F}(V27,V28), V0 == V28, V2 == V28, V27 == V22 | b-{T}(V8,V9)
% 21.25/21.48 (used 0 times, uses = {})
% 21.25/21.48
% 21.25/21.48 #1946: mergings( V2 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10, V10 == V11, V11 == V12, V12 == V13, V13 == V14, V14 == V15, V15 == V16, V16 == V17, V17 == V18, V18 == V19, V19 == V20, V20 == V21, V21 == V22, V22 == V23, V23 == V24, V24 == V25, V25 == V26, V26 == V27, V27 == V28, V28 == V29, V29 == V30, V30 == V31, V31 == V32, V32 == V33, V33 == V34, V34 == V35, V35 == V36, V36 == V37, V37 == V38, V38 == V47, V47 == V48, V48 == V50, V50 == V59, V59 == V60, V60 == V61, V61 == V62, V62 == V63, V63 == V64, V64 == V65, V65 == V66, V66 == V67, V67 == V68, V68 == V69, V69 == V70, V70 == V71, V71 == V72, V72 == V73, V73 == V74, V74 == V75, V75 == V76, V76 == V77, V77 == V78, V78 == V87, V87 == V88, V88 == V89, V89 == V90, V90 == V91, V91 == V92, V42 == V93, V94 == V145, V92 == V96, V96 == V97, V93 == V98, V99 == V145, V97 == V101, V101 == V102, V102 == V103, V103 == V104, V104 == V105, V105 == V106, V106 == V107, V107 == V108, V108 == V109, V109 == V110, V110 == V111, V111 == V112, V112 == V113, V113 == V114, V114 == V115, V115 == V116, V116 == V117, V117 == V118, V118 == V126, V126 == V127, V127 == V128, V128 == V129, V98 == V130, V131 == V145, V129 == V133, V130 == V134, V135 == V145, V133 == V148; #1846 ), references = 1, size of lhs = 130:
% 21.25/21.48 P_z-{F}(V0), b-{F}(V0,V1), b-{F}(V0,V2), b-{F}(V2,V0), b-{F}(V2,V3), b-{F}(V0,V4), b-{F}(V0,V5), b-{F}(V5,V0), b-{F}(V5,V6), b-{F}(V0,V7), b-{F}(V7,V0), b-{F}(V7,V8), P_s-{F}(V9,V7), b-{F}(V0,V10), V10 == V0, b-{F}(V10,V0), P_s-{F}(V0,V10), b-{F}(V10,V11), b-{F}(V10,V12), P_s-{F}(V13,V10), P_s-{F}(V14,V10), P_s-{F}(V15,V10), b-{F}(V10,V16), b-{F}(V10,V17), P_s-{F}(V18,V10), P_s-{F}(V19,V10), P_s-{F}(V20,V10), b-{F}(V10,V21), b-{F}(V10,V22), P_s-{F}(V23,V10), b-{F}(V10,V24), P_s-{F}(V25,V10), b-{F}(V0,V26), b-{F}(V0,V27), b-{F}(V27,V0), b-{F}(V27,V28), b-{F}(V10,V29), b-{F}(V10,V30), P_s-{F}(V31,V10), P_s-{F}(V32,V27), b-{F}(V0,V33), b-{F}(V33,V0), b-{F}(V33,V34), b-{F}(V10,V35), b-{F}(V10,V36), P_s-{F}(V37,V10), P_s-{F}(V38,V33), b-{F}(V10,V39), P_s-{F}(V40,V10), P_s-{F}(V10,V41), V10 == V41, V0 == V41, P_s-{F}(V42,V41), P_s-{F}(V43,V41), P_s-{F}(V44,V41), P_s-{F}(V45,V41), P_s-{F}(V46,V41), P_s-{F}(V47,V41), b-{F}(V0,V48), P_s-{F}(V49,V10), P_s-{F}(V50,V10), P_s-{F}(V51,V41), P_s-{F}(V52,V51), P_s-{F}(V53,V41), P_s-{F}(V54,V53), P_s-{F}(V55,V41), P_s-{F}(V56,V55), P_s-{F}(V57,V41), P_s-{F}(V58,V57), P_s-{F}(V59,V41), P_s-{F}(V60,V59), P_s-{F}(V61,V41), P_s-{F}(V62,V61), b-{F}(V63,V0), V63 == V0, P_s-{F}(V64,V63), b-{F}(V63,V65), b-{F}(V65,V48), P_s-{F}(V66,V67), V67 == V2, V67 == V10, V67 == V0, V63 == V67, P_s-{F}(V68,V67), P_s-{F}(V69,V67), P_s-{F}(V70,V67), P_s-{F}(V71,V67), P_s-{F}(V72,V67), P_s-{F}(V73,V67), P_s-{F}(V74,V67), P_s-{F}(V75,V67), P_s-{F}(V76,V67), P_s-{F}(V77,V67), P_s-{F}(V78,V67), P_s-{F}(V79,V67), P_s-{F}(V80,V79), P_s-{F}(V81,V67), P_s-{F}(V82,V81), P_s-{F}(V83,V84), P_s-{F}(V85,V84), P_s-{F}(V86,V84), P_s-{F}(V87,V84), P_s-{F}(V88,V84), P_s-{F}(V89,V84), P_s-{F}(V90,V84), P_s-{F}(V91,V84), P_s-{F}(V92,V84), P_s-{F}(V93,V84), P_s-{F}(V94,V95), V95 == V0, V95 == V10, P_s-{F}(V96,V95), P_s-{F}(V97,V96), P_s-{F}(V98,V99), V10 == V99, V0 == V99, P_s-{F}(V100,V99), P_s-{F}(V101,V100), P_s-{F}(V102,V103), V0 == V103, V7 == V103, P_s-{F}(V104,V105), V0 == V105, V33 == V105, P_s-{F}(V106,V107), V0 == V107, V27 == V107, #-{F} V108, V0 == V108, V5 == V108 | P_s-{T}(V84,V0), P_s-{T}(V84,V10), P_s-{T}(V84,V67), P_s-{T}(V84,V70), P_s-{T}(V84,V66), P_s-{T}(V84,V68), P_s-{T}(V84,V13), P_s-{T}(V84,V69), P_s-{T}(V84,V84), P_s-{T}(V84,V14), P_s-{T}(V84,V71), P_s-{T}(V84,V15), P_s-{T}(V84,V80), P_s-{T}(V84,V83), P_s-{T}(V84,V82), P_s-{T}(V84,V85), P_s-{T}(V84,V5), P_s-{T}(V84,V95), P_s-{T}(V84,V99), P_s-{T}(V84,V18), P_s-{T}(V84,V94), P_s-{T}(V84,V19), P_s-{T}(V84,V20), P_s-{T}(V84,V98), P_s-{T}(V84,V86), P_s-{T}(V84,V97), P_s-{T}(V84,V87), P_s-{T}(V84,V101), P_s-{T}(V84,V23), P_s-{T}(V84,V9), P_s-{T}(V84,V72), P_s-{T}(V84,V50), P_s-{T}(V84,V25), P_s-{T}(V84,V74), P_s-{T}(V84,V73), P_s-{T}(V84,V42), P_s-{T}(V84,V43), P_s-{T}(V84,V52), P_s-{T}(V84,V54), P_s-{T}(V84,V88), P_s-{T}(V84,V89), P_s-{T}(V84,V102), P_s-{T}(V84,V37), P_s-{T}(V84,V38), P_s-{T}(V84,V49), P_s-{T}(V84,V40), P_s-{T}(V84,V76), P_s-{T}(V84,V46), P_s-{T}(V84,V47), P_s-{T}(V84,V56), P_s-{T}(V84,V58), P_s-{T}(V84,V90), P_s-{T}(V84,V91), P_s-{T}(V84,V104), P_s-{T}(V84,V31), P_s-{T}(V84,V32), P_s-{T}(V84,V75), P_s-{T}(V84,V44), P_s-{T}(V84,V45), P_s-{T}(V84,V60), P_s-{T}(V84,V62), P_s-{T}(V84,V92), P_s-{T}(V84,V93), P_s-{T}(V84,V106), P_s-{T}(V84,V63), P_s-{T}(V84,V2), P_s-{T}(V84,V108), P_s-{T}(V84,V77), P_s-{T}(V84,V78), P_s-{T}(V84,V64)
% 21.25/21.48 (used 0 times, uses = {})
% 21.25/21.48
% 21.25/21.48 #2089: mergings( V0 == V1, V1 == V2, V2 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10, V10 == V11, V11 == V12, V12 == V13, V13 == V14, V14 == V15, V15 == V16, V16 == V17, V17 == V18, V18 == V19, V19 == V20, V20 == V21, V21 == V22, V22 == V23, V23 == V24, V24 == V25, V25 == V26, V26 == V27, V27 == V28, V28 == V29, V29 == V30, V30 == V31, V31 == V32, V32 == V33, V33 == V34, V34 == V35, V35 == V36, V36 == V45, V45 == V46, V46 == V48, V48 == V57, V57 == V58, V58 == V59, V59 == V60, V60 == V61, V61 == V62, V62 == V63, V63 == V64, V64 == V65, V65 == V66, V66 == V67, V67 == V68, V68 == V69, V69 == V70, V70 == V71, V71 == V72, V72 == V73, V73 == V74, V74 == V75, V75 == V76, V76 == V85, V85 == V86, V86 == V87, V87 == V88, V88 == V89, V89 == V90, V40 == V91, V92 == V143, V90 == V94, V94 == V95, V91 == V96, V97 == V143, V95 == V99, V99 == V100, V100 == V101, V101 == V102, V102 == V103, V103 == V104, V104 == V105, V105 == V106, V106 == V107, V107 == V108, V108 == V109, V109 == V110, V110 == V111, V111 == V112, V112 == V113, V113 == V114, V114 == V115, V115 == V116, V116 == V124, V124 == V125, V125 == V126, V126 == V127, V96 == V128, V129 == V143, V127 == V131, V128 == V132, V133 == V143, V131 == V146, V146 == V208, V208 == V210, V210 == V212, V212 == V214, V214 == V216, V216 == V218, V218 == V220, V220 == V222, V222 == V224, V224 == V226, V226 == V228, V228 == V230, V230 == V232, V232 == V234, V234 == V236, V236 == V238, V238 == V240, V240 == V242, V242 == V244, V244 == V246, V246 == V248, V248 == V250, V250 == V252, V252 == V254, V254 == V256, V256 == V258, V258 == V260, V260 == V262, V262 == V264, V264 == V266, V266 == V268, V268 == V270, V270 == V272, V272 == V274, V274 == V276, V276 == V278, V278 == V280, V280 == V282, V282 == V284, V284 == V286, V286 == V288, V288 == V290; #1947 ), references = 1, size of lhs = 213:
% 21.25/21.48 P_z-{F}(V0), b-{F}(V0,V1), b-{F}(V0,V2), b-{F}(V2,V0), b-{F}(V2,V3), b-{F}(V0,V4), b-{F}(V0,V5), b-{F}(V5,V0), b-{F}(V5,V6), b-{F}(V0,V7), b-{F}(V7,V0), b-{F}(V7,V8), P_s-{F}(V9,V7), b-{F}(V0,V10), V10 == V0, b-{F}(V10,V0), P_s-{F}(V0,V10), b-{F}(V10,V11), b-{F}(V10,V12), P_s-{F}(V13,V10), P_s-{F}(V14,V10), P_s-{F}(V15,V10), b-{F}(V10,V16), b-{F}(V10,V17), P_s-{F}(V18,V10), P_s-{F}(V19,V10), P_s-{F}(V20,V10), b-{F}(V10,V21), b-{F}(V10,V22), P_s-{F}(V23,V10), b-{F}(V10,V24), P_s-{F}(V25,V10), b-{F}(V0,V26), b-{F}(V0,V27), b-{F}(V27,V0), b-{F}(V27,V28), b-{F}(V10,V29), b-{F}(V10,V30), P_s-{F}(V31,V10), P_s-{F}(V32,V27), b-{F}(V0,V33), b-{F}(V33,V0), b-{F}(V33,V34), b-{F}(V10,V35), b-{F}(V10,V36), P_s-{F}(V37,V10), P_s-{F}(V38,V33), b-{F}(V10,V39), P_s-{F}(V40,V10), P_s-{F}(V10,V41), V10 == V41, V0 == V41, b-{F}(V0,V42), P_s-{F}(V43,V10), P_s-{F}(V44,V10), P_s-{F}(V45,V10), P_s-{F}(V46,V5), P_s-{F}(V47,V2), P_s-{F}(V48,V41), P_s-{F}(V49,V48), P_s-{F}(V50,V41), P_s-{F}(V51,V50), P_s-{F}(V52,V41), P_s-{F}(V53,V52), P_s-{F}(V54,V41), P_s-{F}(V55,V54), P_s-{F}(V56,V41), P_s-{F}(V57,V56), P_s-{F}(V58,V41), P_s-{F}(V59,V58), P_s-{F}(V60,V41), P_s-{F}(V61,V60), P_s-{F}(V62,V41), P_s-{F}(V63,V62), P_s-{F}(V64,V41), P_s-{F}(V65,V64), P_s-{F}(V66,V41), P_s-{F}(V67,V66), P_s-{F}(V68,V41), P_s-{F}(V69,V68), P_s-{F}(V70,V41), P_s-{F}(V71,V70), b-{F}(V72,V42), b-{F}(V73,V0), V73 == V0, b-{F}(V73,V72), P_s-{F}(V74,V73), P_s-{F}(V75,V73), P_s-{F}(V76,V77), P_s-{F}(V77,V78), V78 == V2, V78 == V10, V78 == V0, V73 == V78, P_s-{F}(V79,V78), P_s-{F}(V80,V78), P_s-{F}(V81,V80), P_s-{F}(V82,V78), P_s-{F}(V83,V82), P_s-{F}(V84,V78), P_s-{F}(V85,V84), P_s-{F}(V86,V78), P_s-{F}(V87,V86), P_s-{F}(V88,V78), P_s-{F}(V89,V88), P_s-{F}(V90,V78), P_s-{F}(V91,V90), P_s-{F}(V92,V78), P_s-{F}(V93,V92), P_s-{F}(V94,V78), P_s-{F}(V95,V94), P_s-{F}(V96,V78), P_s-{F}(V97,V96), P_s-{F}(V98,V78), P_s-{F}(V99,V98), P_s-{F}(V100,V78), P_s-{F}(V101,V100), P_s-{F}(V102,V78), P_s-{F}(V103,V102), P_s-{F}(V104,V78), P_s-{F}(V105,V104), P_s-{F}(V106,V107), P_s-{F}(V107,V108), V108 == V0, V108 == V10, P_s-{F}(V109,V108), P_s-{F}(V110,V108), P_s-{F}(V111,V110), P_s-{F}(V112,V113), P_s-{F}(V113,V114), V10 == V114, V0 == V114, P_s-{F}(V115,V114), P_s-{F}(V116,V114), P_s-{F}(V117,V116), P_s-{F}(V118,V119), V45 == V119, V79 == V119, V87 == V119, V81 == V119, V83 == V119, V85 == V119, V118 == V119, V89 == V119, V46 == V119, V109 == V119, V115 == V119, V111 == V119, V117 == V119, V91 == V119, V95 == V119, V93 == V119, V49 == V119, V51 == V119, V99 == V119, V57 == V119, V59 == V119, V97 == V119, V53 == V119, V55 == V119, V75 == V119, V47 == V119, V101 == V119, V103 == V119, P_s-{F}(V120,V119), P_s-{F}(V121,V120), V121 == V119, P_s-{F}(V122,V119), P_s-{F}(V123,V122), V123 == V119, P_s-{F}(V124,V119), P_s-{F}(V125,V124), V125 == V119, P_s-{F}(V126,V119), P_s-{F}(V127,V126), V127 == V119, P_s-{F}(V128,V119), P_s-{F}(V129,V128), V129 == V119, P_s-{F}(V130,V119), P_s-{F}(V131,V130), V131 == V119, P_s-{F}(V132,V119), P_s-{F}(V133,V132), V133 == V119, P_s-{F}(V134,V119), P_s-{F}(V135,V134), V135 == V119, P_s-{F}(V136,V119), P_s-{F}(V137,V136), V137 == V119, P_s-{F}(V138,V119), P_s-{F}(V139,V138), V139 == V119, P_s-{F}(V140,V141), V140 == V119, P_s-{F}(V141,V142), V0 == V142, V7 == V142, P_s-{F}(V143,V144), V143 == V119, P_s-{F}(V144,V145), V0 == V145, V33 == V145, P_s-{F}(V146,V147), V146 == V119, P_s-{F}(V147,V148), V0 == V148, V27 == V148, P_s-{F}(V149,V150), V0 == V150, V5 == V150, V149 == V119 | P_s-{T}(V119,V0), P_s-{T}(V119,V13), P_s-{T}(V119,V14), P_s-{T}(V119,V15), P_s-{T}(V119,V76), P_s-{T}(V119,V105), P_s-{T}(V119,V18), P_s-{T}(V119,V19), P_s-{T}(V119,V20), P_s-{T}(V119,V106), P_s-{T}(V119,V112), P_s-{T}(V119,V23), P_s-{T}(V119,V9), P_s-{T}(V119,V44), P_s-{T}(V119,V25), P_s-{T}(V119,V61), P_s-{T}(V119,V63), P_s-{T}(V119,V37), P_s-{T}(V119,V38), P_s-{T}(V119,V43), P_s-{T}(V119,V40), P_s-{T}(V119,V65), P_s-{T}(V119,V67), P_s-{T}(V119,V31), P_s-{T}(V119,V32), P_s-{T}(V119,V69), P_s-{T}(V119,V71), P_s-{T}(V119,V74)
% 21.25/21.48 (used 0 times, uses = {})
% 21.25/21.48
% 21.25/21.48 #2274: mergings( V0 == V1, V1 == V2, V2 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10, V10 == V11, V11 == V12, V12 == V13, V13 == V14, V14 == V15, V15 == V16, V16 == V17, V17 == V18, V18 == V19, V19 == V20, V20 == V21, V21 == V22, V22 == V23, V23 == V24, V24 == V25, V25 == V26, V26 == V27, V27 == V28, V28 == V29, V29 == V30, V30 == V31, V31 == V32, V32 == V33, V33 == V34, V34 == V35, V35 == V45, V45 == V36, V36 == V46, V46 == V48, V48 == V57, V57 == V58, V58 == V59, V59 == V60, V60 == V61, V61 == V62, V62 == V63, V63 == V64, V64 == V65, V65 == V66, V66 == V67, V67 == V68, V68 == V69, V69 == V70, V70 == V71, V71 == V72, V72 == V73, V73 == V74, V74 == V75, V75 == V76, V76 == V85, V85 == V86, V86 == V87, V87 == V88, V88 == V89, V89 == V90, V40 == V91, V92 == V139, V90 == V93, V93 == V94, V91 == V95, V96 == V139, V94 == V97, V97 == V98, V98 == V99, V99 == V100, V100 == V101, V101 == V102, V102 == V103, V103 == V104, V104 == V105, V105 == V106, V106 == V107, V107 == V108, V108 == V109, V109 == V110, V110 == V111, V111 == V112, V112 == V113, V113 == V114, V114 == V122, V122 == V123, V123 == V124, V124 == V125, V95 == V126, V127 == V139, V125 == V128, V126 == V129, V130 == V139, V128 == V140, V140 == V144, V144 == V146, V146 == V147, V147 == V148, V148 == V149, V149 == V150, V150 == V151, V151 == V152, V152 == V153, V153 == V154, V154 == V155, V155 == V157, V157 == V158, V158 == V159, V159 == V160, V160 == V161, V161 == V162, V162 == V163, V163 == V164, V164 == V165, V165 == V166, V166 == V167, V167 == V168, V168 == V169, V169 == V170, V170 == V171, V171 == V172, V172 == V173, V173 == V174, V174 == V175, V175 == V176, V176 == V177, V177 == V178, V178 == V179, V179 == V180, V180 == V181, V181 == V182, V182 == V183, V183 == V184, V184 == V186, V186 == V187, V187 == V188, V188 == V43, V43 == V44, V44 == V47, V47 == V217, V129 == V218, V139 == V219, V217 == V246, V218 == V245, V246 == V54, V54 == V55, V55 == V56, V56 == V247, V245 == V248, V219 == V249, V247 == V253, V248 == V254, V249 == V255, V253 == V81, V81 == V82, V254 == V77, V82 == V143, V143 == V84, V84 == V202, V77 == V201, V202 == V204, V201 == V203, V204 == V135, V135 == V136, V203 == V131, V136 == V142, V142 == V138, V138 == V206, V131 == V205, V206 == V208, V205 == V207, V208 == V120, V120 == V121, V207 == V116, V121 == V210, V116 == V209, V210 == V212, V209 == V211; #2090 ), references = 2, size of lhs = 165:
% 21.25/21.48 P_z-{F}(V0), b-{F}(V0,V1), b-{F}(V0,V2), b-{F}(V2,V0), b-{F}(V2,V3), b-{F}(V0,V4), b-{F}(V0,V5), b-{F}(V5,V0), b-{F}(V5,V6), b-{F}(V0,V7), b-{F}(V0,V8), V8 == V0, b-{F}(V8,V0), P_s-{F}(V0,V8), b-{F}(V8,V9), b-{F}(V8,V10), b-{F}(V8,V11), b-{F}(V8,V12), b-{F}(V8,V13), b-{F}(V8,V14), b-{F}(V8,V15), b-{F}(V8,V16), b-{F}(V8,V17), b-{F}(V8,V18), b-{F}(V8,V19), b-{F}(V8,V20), b-{F}(V8,V21), b-{F}(V8,V22), b-{F}(V8,V23), b-{F}(V0,V24), P_s-{F}(V25,V8), P_s-{F}(V26,V5), P_s-{F}(V27,V2), P_s-{F}(V8,V28), V28 == V2, V8 == V28, V0 == V28, P_s-{F}(V29,V28), P_s-{F}(V30,V28), P_s-{F}(V31,V28), P_s-{F}(V32,V28), P_s-{F}(V33,V32), P_s-{F}(V34,V28), P_s-{F}(V35,V34), P_s-{F}(V36,V28), P_s-{F}(V37,V36), P_s-{F}(V38,V28), P_s-{F}(V39,V38), P_s-{F}(V40,V28), P_s-{F}(V41,V40), P_s-{F}(V42,V28), P_s-{F}(V43,V42), b-{F}(V44,V24), P_s-{F}(V45,V28), P_s-{F}(V46,V45), P_s-{F}(V47,V28), P_s-{F}(V48,V47), P_s-{F}(V49,V28), P_s-{F}(V50,V49), P_s-{F}(V51,V28), P_s-{F}(V52,V51), P_s-{F}(V53,V28), P_s-{F}(V54,V53), P_s-{F}(V55,V28), P_s-{F}(V56,V55), P_s-{F}(V57,V28), P_s-{F}(V58,V57), P_s-{F}(V59,V28), P_s-{F}(V60,V59), P_s-{F}(V61,V28), P_s-{F}(V62,V61), P_s-{F}(V63,V28), P_s-{F}(V64,V63), P_s-{F}(V65,V28), P_s-{F}(V66,V65), P_s-{F}(V67,V28), P_s-{F}(V68,V67), P_s-{F}(V69,V28), P_s-{F}(V70,V69), P_s-{F}(V71,V28), P_s-{F}(V72,V71), b-{F}(V73,V0), V73 == V0, V73 == V28, b-{F}(V73,V44), P_s-{F}(V74,V73), P_s-{F}(V75,V73), P_s-{F}(V76,V77), V25 == V77, V29 == V77, V52 == V77, V46 == V77, V48 == V77, V50 == V77, V76 == V77, V54 == V77, V26 == V77, V30 == V77, V31 == V77, V70 == V77, V72 == V77, V56 == V77, V60 == V77, V58 == V77, V33 == V77, V35 == V77, V64 == V77, V41 == V77, V43 == V77, V62 == V77, V37 == V77, V39 == V77, V75 == V77, V27 == V77, V66 == V77, V68 == V77, P_s-{F}(V78,V77), P_s-{F}(V79,V78), V79 == V77, P_s-{F}(V80,V77), P_s-{F}(V81,V80), V81 == V77, P_s-{F}(V82,V77), P_s-{F}(V83,V82), V83 == V77, P_s-{F}(V84,V77), P_s-{F}(V85,V84), V85 == V77, P_s-{F}(V86,V77), P_s-{F}(V87,V86), V87 == V77, P_s-{F}(V88,V77), P_s-{F}(V89,V88), V89 == V77, P_s-{F}(V90,V77), P_s-{F}(V91,V90), V91 == V77, P_s-{F}(V92,V77), P_s-{F}(V93,V92), V93 == V77, P_s-{F}(V94,V77), P_s-{F}(V95,V94), V95 == V77, P_s-{F}(V96,V77), P_s-{F}(V97,V96), V97 == V77, P_s-{F}(V98,V99), V98 == V77, P_s-{F}(V99,V100), V0 == V100, V8 == V100, P_s-{F}(V101,V102), V101 == V77, P_s-{F}(V102,V103), V0 == V103, V8 == V103, P_s-{F}(V104,V105), V104 == V77, P_s-{F}(V105,V106), V0 == V106, V8 == V106, P_s-{F}(V107,V108), V0 == V108, V5 == V108, V107 == V77 | P_s-{T}(V77,V74)
% 21.25/21.48 (used 0 times, uses = {})
% 21.25/21.48
% 21.25/21.48 #2283: mergings( V2 == V9; #2281 ), references = 1, size of lhs = 62:
% 21.25/21.48 P_z-{F}(V0), P_s-{F}(V0,V1), V1 == V0, P_s-{F}(V2,V1), P_s-{F}(V3,V1), P_s-{F}(V4,V1), P_s-{F}(V5,V1), P_s-{F}(V6,V1), P_s-{F}(V7,V1), P_s-{F}(V8,V1), P_s-{F}(V9,V1), P_s-{F}(V10,V1), P_s-{F}(V11,V1), P_s-{F}(V12,V1), P_s-{F}(V13,V1), P_s-{F}(V14,V1), P_s-{F}(V15,V1), P_s-{F}(V16,V1), P_s-{F}(V17,V1), P_s-{F}(V18,V1), P_s-{F}(V19,V1), P_s-{F}(V20,V1), P_s-{F}(V21,V1), P_s-{F}(V22,V1), P_s-{F}(V23,V1), P_s-{F}(V24,V1), P_s-{F}(V25,V1), P_s-{F}(V26,V1), P_s-{F}(V27,V1), P_s-{F}(V28,V1), P_s-{F}(V29,V1), P_s-{F}(V30,V1), P_s-{F}(V31,V1), P_s-{F}(V32,V1), P_s-{F}(V33,V1), P_s-{F}(V34,V1), P_s-{F}(V35,V1), P_s-{F}(V36,V1), P_s-{F}(V37,V1), P_s-{F}(V38,V1), P_s-{F}(V39,V1), P_s-{F}(V40,V1), P_s-{F}(V41,V1), P_s-{F}(V42,V1), P_s-{F}(V43,V1), P_s-{F}(V44,V1), P_s-{F}(V45,V1), P_s-{F}(V46,V1), P_s-{F}(V47,V1), P_s-{F}(V48,V1), P_s-{F}(V49,V1), P_s-{F}(V50,V1), P_s-{F}(V51,V1), P_s-{F}(V52,V1), P_s-{F}(V53,V1), P_s-{F}(V54,V1), P_s-{F}(V55,V1), P_s-{F}(V56,V1), P_s-{F}(V57,V1), P_s-{F}(V58,V1), P_s-{F}(V59,V1), P_s-{F}(V60,V1) | P_s-{T}(V1,V1), P_s-{T}(V1,V0), P_s-{T}(V1,V2), P_s-{T}(V1,V9), P_s-{T}(V1,V10), P_s-{T}(V1,V11), P_s-{T}(V1,V12), P_s-{T}(V1,V13), P_s-{T}(V1,V14), P_s-{T}(V1,V15), P_s-{T}(V1,V16), P_s-{T}(V1,V17), P_s-{T}(V1,V18), P_s-{T}(V1,V19), P_s-{T}(V1,V20), P_s-{T}(V1,V21), P_s-{T}(V1,V22), P_s-{T}(V1,V23), P_s-{T}(V1,V24), P_s-{T}(V1,V25), P_s-{T}(V1,V3), P_s-{T}(V1,V4), P_s-{T}(V1,V47), P_s-{T}(V1,V46), P_s-{T}(V1,V5), P_s-{T}(V1,V35), P_s-{T}(V1,V32), P_s-{T}(V1,V33), P_s-{T}(V1,V34), P_s-{T}(V1,V36), P_s-{T}(V1,V6), P_s-{T}(V1,V44), P_s-{T}(V1,V45), P_s-{T}(V1,V37), P_s-{T}(V1,V39), P_s-{T}(V1,V38), P_s-{T}(V1,V26), P_s-{T}(V1,V27), P_s-{T}(V1,V41), P_s-{T}(V1,V30), P_s-{T}(V1,V31), P_s-{T}(V1,V40), P_s-{T}(V1,V28), P_s-{T}(V1,V29), P_s-{T}(V1,V8), P_s-{T}(V1,V7), P_s-{T}(V1,V42), P_s-{T}(V1,V43), P_s-{T}(V1,V48), P_s-{T}(V1,V49), P_s-{T}(V1,V50), P_s-{T}(V1,V51), P_s-{T}(V1,V52), P_s-{T}(V1,V53), P_s-{T}(V1,V54), P_s-{T}(V1,V55), P_s-{T}(V1,V56), P_s-{T}(V1,V57), P_s-{T}(V1,V58), P_s-{T}(V1,V59), P_s-{T}(V1,V60)
% 21.25/21.48 (used 0 times, uses = {})
% 21.25/21.48
% 21.25/21.48 #2345: mergings( V8 == V0, V0 == V2, V2 == V10, V10 == V11, V11 == V12, V12 == V13, V13 == V14, V14 == V15, V15 == V16, V16 == V17, V17 == V18, V18 == V19, V19 == V20, V20 == V21, V21 == V22, V22 == V23, V23 == V24, V24 == V25, V25 == V26, V26 == V3, V3 == V4, V4 == V48, V48 == V47, V47 == V5, V5 == V36, V36 == V33, V33 == V34, V34 == V35, V35 == V37, V37 == V6, V6 == V45, V45 == V46, V46 == V38, V38 == V40, V40 == V39, V39 == V27, V27 == V28, V28 == V42, V42 == V31, V31 == V32, V32 == V41, V41 == V29, V29 == V30, V30 == V9, V9 == V7, V7 == V43, V43 == V44, V44 == V49, V49 == V50, V50 == V51, V51 == V52, V52 == V53, V53 == V54, V54 == V55, V55 == V56, V56 == V57, V57 == V58, V58 == V59, V59 == V60, V60 == V61; #2284 ), references = 1, size of lhs = 3:
% 21.25/21.48 P_z-{F}(V0), P_s-{F}(V0,V1), V1 == V0 | P_s-{T}(V1,V1)
% 21.25/21.48 (used 0 times, uses = {})
% 21.25/21.48
% 21.25/21.48 #2349: mergings( V0 == V2; #2347 ), references = 1, size of lhs = 1:
% 21.25/21.48 P_z-{F}(V0) | P_s-{T}(V0,V0)
% 21.25/21.48 (used 0 times, uses = {})
% 21.25/21.48
% 21.25/21.48 #2352: exists( #8, #2350 ), references = 1, size of lhs = 0:
% 21.25/21.48 FALSE | FALSE
% 21.25/21.48 (used 0 times, uses = {})
% 21.25/21.48
% 21.25/21.48 number of learnt formulas = 55
% 21.25/21.48
% 21.25/21.48
% 21.25/21.48 % SZS output end Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 21.25/21.48
% 21.25/21.48 randbase = 1
%------------------------------------------------------------------------------