%------------------------------------------------------------------------------
% File : Geo-III---2018C
% Problem : GRA127-1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : geo -tptp_input -nonempty -inputfile %s
% Computer : n027.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:29 PM UTC 2026
% Result : Unsatisfiable 29.24s 29.44s
% Output : Refutation 29.24s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : GRA127-1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.12 % Command : geo -tptp_input -nonempty -inputfile %s
% 0.15/0.33 % Computer : n027.cluster.edu
% 0.15/0.33 % Model : x86_64 x86_64
% 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.33 % Memory : 8042.1875MB
% 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.34 % CPULimit : 300
% 0.15/0.34 % WCLimit : 300
% 0.15/0.34 % DateTime : Mon May 4 22:31:04 EDT 2026
% 0.15/0.34 % CPUTime :
% 29.24/29.44 GeoParameters:
% 29.24/29.44
% 29.24/29.44 tptp_input = 1
% 29.24/29.44 tptp_output = 0
% 29.24/29.44 nonempty = 1
% 29.24/29.44 inputfile = /export/starexec/sandbox/benchmark/theBenchmark.p
% 29.24/29.44 includepath = /export/starexec/sandbox/solver/bin/../../benchmark/
% 29.24/29.44
% 29.24/29.44
% 29.24/29.44 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 29.24/29.44 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 29.24/29.44
% 29.24/29.44 RuleSystem INPUT:
% 29.24/29.44
% 29.24/29.44 Initial Rules:
% 29.24/29.44 #0: input, references = 15, size of lhs = 2:
% 29.24/29.44 P_z-{F}(V0), P_s-{F}(V1,V0) | FALSE
% 29.24/29.44 (used 0 times, uses = {})
% 29.24/29.44
% 29.24/29.44 #1: input, references = 5, size of lhs = 4:
% 29.24/29.44 P_z-{F}(V0), P_s-{F}(V1,V4), P_s-{F}(V2,V4), V1 == V2 | FALSE
% 29.24/29.44 (used 0 times, uses = {})
% 29.24/29.44
% 29.24/29.44 #2: input, references = 3, size of lhs = 2:
% 29.24/29.44 P_z-{F}(V0), r-{F}(V1,V1) | FALSE
% 29.24/29.44 (used 0 times, uses = {})
% 29.24/29.44
% 29.24/29.44 #3: input, references = 3, size of lhs = 2:
% 29.24/29.44 P_z-{F}(V0), b-{F}(V1,V1) | FALSE
% 29.24/29.44 (used 0 times, uses = {})
% 29.24/29.44
% 29.24/29.44 #4: input, references = 25, size of lhs = 4:
% 29.24/29.44 P_z-{F}(V0), #-{F} V1, #-{F} V2, V1 == V2 | r-{T}(V1,V2), b-{T}(V1,V2)
% 29.24/29.44 (used 0 times, uses = {})
% 29.24/29.44
% 29.24/29.44 #5: input, references = 18, size of lhs = 5:
% 29.24/29.44 P_z-{F}(V0), r-{F}(V1,V2), r-{F}(V1,V3), r-{F}(V4,V1), r-{F}(V4,V3) | FALSE
% 29.24/29.44 (used 0 times, uses = {})
% 29.24/29.44
% 29.24/29.44 #6: input, references = 6, size of lhs = 5:
% 29.24/29.44 P_z-{F}(V0), b-{F}(V1,V2), b-{F}(V3,V1), b-{F}(V4,V3), b-{F}(V4,V1) | FALSE
% 29.24/29.44 (used 0 times, uses = {})
% 29.24/29.44
% 29.24/29.44 #7: input, references = 16, size of lhs = 1:
% 29.24/29.44 #-{F} V0 | EXISTS V1: P_s-{T}(V0,V1)
% 29.24/29.44 (used 0 times, uses = {})
% 29.24/29.44
% 29.24/29.44 #8: input, references = 4, size of lhs = 0:
% 29.24/29.44 FALSE | EXISTS V0: P_z-{T}(V0)
% 29.24/29.44 (used 0 times, uses = {})
% 29.24/29.44
% 29.24/29.44 number of initial rules = 9
% 29.24/29.44
% 29.24/29.44 Simplifiers:
% 29.24/29.44 #9: unsound, references = 3, size of lhs = 3:
% 29.24/29.44 P_s-{F}(V0,V1), P_s-{F}(V0,V3), V1 == V3 | FALSE
% 29.24/29.44 (used 0 times, uses = {})
% 29.24/29.44
% 29.24/29.44 #10: unsound, references = 3, size of lhs = 3:
% 29.24/29.44 P_z-{F}(V0), P_z-{F}(V1), V0 == V1 | FALSE
% 29.24/29.44 (used 0 times, uses = {})
% 29.24/29.44
% 29.24/29.44 number of simplifiers = 2
% 29.24/29.44
% 29.24/29.44 Learnt:
% 29.24/29.44 #13: mergings( V0 == V3; #11 ), references = 12, size of lhs = 5:
% 29.24/29.44 P_z-{F}(V0), b-{F}(V1,V2), b-{F}(V1,V3), V2 == V3, b-{F}(V3,V4) | r-{T}(V2,V3)
% 29.24/29.44 (used 0 times, uses = {})
% 29.24/29.44
% 29.24/29.44 #16: mergings( V0 == V3; #14 ), references = 2, size of lhs = 6:
% 29.24/29.44 P_z-{F}(V0), b-{F}(V1,V2), b-{F}(V2,V3), b-{F}(V1,V3), #-{F} V4, V3 == V4 | r-{T}(V3,V4)
% 29.24/29.44 (used 0 times, uses = {})
% 29.24/29.44
% 29.24/29.44 #24: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6; #19 ), references = 15, size of lhs = 9:
% 29.24/29.44 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-{F}(V5,V6) | r-{T}(V3,V2)
% 29.24/29.44 (used 0 times, uses = {})
% 29.24/29.44
% 29.24/29.44 #29: mergings( V0 == V3, V3 == V4; #26 ), references = 9, size of lhs = 9:
% 29.24/29.44 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-{F}(V5,V6) | r-{T}(V1,V4)
% 29.24/29.44 (used 0 times, uses = {})
% 29.24/29.44
% 29.24/29.44 #36: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6; #31 ), references = 6, size of lhs = 10:
% 29.24/29.44 P_z-{F}(V0), r-{F}(V1,V2), V2 == V1, r-{F}(V1,V3), r-{F}(V1,V4), b-{F}(V4,V2), #-{F} V5, V1 == V5, V2 == V5, V4 == V5 | b-{T}(V1,V5)
% 29.24/29.44 (used 0 times, uses = {})
% 29.24/29.44
% 29.24/29.44 #47: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7; #41 ), references = 4, size of lhs = 26:
% 29.24/29.44 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 == V2, V9 == V6, 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)
% 29.24/29.44 (used 0 times, uses = {})
% 29.24/29.44
% 29.24/29.44 #70: 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; #56 ), references = 1, size of lhs = 53:
% 29.24/29.44 P_z-{F}(V0), r-{F}(V1,V2), V2 == V1, r-{F}(V1,V3), r-{F}(V1,V4), b-{F}(V4,V2), b-{F}(V1,V5), b-{F}(V1,V6), V6 == V5, b-{F}(V1,V7), V7 == V6, V7 == V5, b-{F}(V8,V7), b-{F}(V8,V6), b-{F}(V9,V7), b-{F}(V9,V6), b-{F}(V10,V5), b-{F}(V10,V11), V5 == V11, b-{F}(V12,V5), b-{F}(V12,V13), V13 == V5, V13 == V11, b-{F}(V1,V13), b-{F}(V14,V13), b-{F}(V14,V5), b-{F}(V15,V13), b-{F}(V15,V11), b-{F}(V1,V16), V16 == V11, b-{F}(V17,V16), b-{F}(V17,V18), V18 == V16, b-{F}(V19,V18), b-{F}(V19,V16), b-{F}(V20,V16), b-{F}(V20,V21), V21 == V16, V21 == V18, b-{F}(V22,V21), b-{F}(V22,V16), b-{F}(V23,V21), b-{F}(V23,V18), b-{F}(V24,V21), b-{F}(V24,V18), b-{F}(V25,V26), V25 == V5, V5 == V26, V13 == V26, r-{F}(V27,V26), V5 == V27, r-{F}(V27,V28), #-{F} V29 | P_s-{T}(V29,V1), P_s-{T}(V29,V2), P_s-{T}(V29,V4), P_s-{T}(V29,V6), P_s-{T}(V29,V7), P_s-{T}(V29,V13), P_s-{T}(V29,V5), P_s-{T}(V29,V25), P_s-{T}(V29,V16), P_s-{T}(V29,V11), P_s-{T}(V29,V18), P_s-{T}(V29,V21)
% 29.24/29.44 (used 0 times, uses = {})
% 29.24/29.44
% 29.24/29.44 #95: 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 == V43, V43 == V45, V45 == V47, V47 == V49, V49 == V51, V51 == V53, V53 == V55, V55 == V57, V57 == V59, V59 == V61; #71 ), references = 1, size of lhs = 73:
% 29.24/29.44 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), r-{F}(V7,V10), b-{F}(V10,V8), b-{F}(V7,V11), V3 == V11, V2 == V11, b-{F}(V12,V11), b-{F}(V12,V13), V11 == V13, b-{F}(V14,V11), b-{F}(V14,V15), V15 == V11, V15 == V13, b-{F}(V7,V15), b-{F}(V16,V15), b-{F}(V16,V11), b-{F}(V17,V15), b-{F}(V17,V13), b-{F}(V7,V18), V18 == V13, 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 == V18, V23 == V20, 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,V7), P_s-{F}(V28,V8), P_s-{F}(V29,V15), P_s-{F}(V30,V11), P_s-{F}(V31,V18), P_s-{F}(V32,V13), P_s-{F}(V33,V20), P_s-{F}(V34,V23), b-{F}(V35,V36), V35 == V11, V11 == V36, V15 == V36, r-{F}(V37,V36), V11 == V37, r-{F}(V37,V38), #-{F} V39, V27 == V39, V28 == V39, V5 == V39, V6 == V39, V29 == V39, V30 == V39, V31 == V39, V32 == V39, V33 == V39, V34 == V39 | P_s-{T}(V39,V10), P_s-{T}(V39,V35)
% 29.24/29.44 (used 0 times, uses = {})
% 29.24/29.44
% 29.24/29.44 #121: 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 == V33; #96 ), references = 1, size of lhs = 73:
% 29.24/29.44 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), r-{F}(V3,V10), b-{F}(V3,V11), V4 == V11, V6 == V11, b-{F}(V12,V11), b-{F}(V12,V13), V11 == V13, b-{F}(V14,V11), b-{F}(V14,V15), V15 == V11, V15 == V13, b-{F}(V3,V15), b-{F}(V16,V15), b-{F}(V16,V11), b-{F}(V17,V15), b-{F}(V17,V13), b-{F}(V3,V18), V18 == V13, 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 == V18, V23 == V20, 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,V3), P_s-{F}(V28,V15), P_s-{F}(V29,V11), P_s-{F}(V30,V18), P_s-{F}(V31,V13), P_s-{F}(V32,V20), P_s-{F}(V33,V23), b-{F}(V34,V35), V34 == V11, V11 == V35, V15 == V35, r-{F}(V36,V35), V11 == V36, r-{F}(V36,V37), #-{F} V38, V27 == V38, V2 == V38, V8 == V38, V9 == V38, V28 == V38, V29 == V38, V30 == V38, V31 == V38, V32 == V38, V33 == V38 | P_s-{T}(V38,V34)
% 29.24/29.44 (used 0 times, uses = {})
% 29.24/29.44
% 29.24/29.44 #159: 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 == V1; #126 ), references = 1, size of lhs = 45:
% 29.24/29.44 P_z-{F}(V0), r-{F}(V1,V0), r-{F}(V1,V2), r-{F}(V1,V3), r-{F}(V1,V4), V0 == V4, V4 == V1, P_s-{F}(V5,V4), r-{F}(V6,V4), r-{F}(V6,V7), r-{F}(V1,V8), r-{F}(V1,V9), P_s-{F}(V10,V1), P_s-{F}(V11,V12), V1 == V12, V0 == V12, V12 == V4, P_s-{F}(V13,V12), P_s-{F}(V14,V12), P_s-{F}(V15,V16), V1 == V16, V4 == V16, V0 == V16, V12 == V16, P_s-{F}(V17,V16), P_s-{F}(V18,V16), P_s-{F}(V19,V20), V1 == V20, V0 == V20, V20 == V4, V20 == V6, V16 == V20, V12 == V20, P_s-{F}(V21,V20), #-{F} V22, V10 == V22, V5 == V22, V15 == V22, V11 == V22, V13 == V22, V19 == V22, V21 == V22, V17 == V22, V18 == V22, V14 == V22 | r-{T}(V0,V4)
% 29.24/29.44 (used 0 times, uses = {})
% 29.24/29.44
% 29.24/29.44 #195: 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; #161 ), references = 1, size of lhs = 29:
% 29.24/29.44 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}(V4,V5), r-{F}(V6,V0), V2 == V6, r-{F}(V6,V2), r-{F}(V6,V7), r-{F}(V6,V8), r-{F}(V6,V9), r-{F}(V6,V10), P_s-{F}(V11,V6), P_s-{F}(V12,V13), V6 == V13, V2 == V13, V0 == V13, P_s-{F}(V14,V13), P_s-{F}(V15,V13), P_s-{F}(V16,V17), V6 == V17, V0 == V17, V17 == V2, V17 == V4, V13 == V17, P_s-{F}(V18,V17), #-{F} V19 | P_s-{T}(V19,V6), P_s-{T}(V19,V0), P_s-{T}(V19,V2), P_s-{T}(V19,V13), P_s-{T}(V19,V17), P_s-{T}(V19,V11), P_s-{T}(V19,V3), P_s-{T}(V19,V12), P_s-{T}(V19,V19), P_s-{T}(V19,V16), P_s-{T}(V19,V18), P_s-{T}(V19,V14), P_s-{T}(V19,V15)
% 29.24/29.44 (used 0 times, uses = {})
% 29.24/29.44
% 29.24/29.44 #241: 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 == V53, V53 == V55, V55 == V57, V57 == V59, V59 == V61, V61 == V63, V63 == V65, V65 == V67, V67 == V69, V69 == V71, V71 == V73; #196 ), references = 1, size of lhs = 50:
% 29.24/29.44 P_z-{F}(V0), r-{F}(V1,V0), r-{F}(V1,V2), V0 == V2, r-{F}(V3,V2), r-{F}(V3,V4), P_s-{F}(V5,V2), P_s-{F}(V6,V2), P_s-{F}(V7,V6), r-{F}(V8,V0), V2 == V8, r-{F}(V8,V2), r-{F}(V8,V9), r-{F}(V8,V10), r-{F}(V8,V11), r-{F}(V8,V12), P_s-{F}(V13,V8), P_s-{F}(V14,V8), P_s-{F}(V15,V16), V8 == V16, V2 == V16, V0 == 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,V16), P_s-{F}(V22,V21), P_s-{F}(V23,V24), V8 == V24, V0 == V24, V24 == V2, V24 == V3, V16 == V24, P_s-{F}(V25,V24), P_s-{F}(V26,V25), P_s-{F}(V27,V24), P_s-{F}(V28,V27), P_s-{F}(V29,V30), V14 == V30, V5 == V30, V15 == V30, V23 == V30, V7 == V30, V18 == V30, V29 == V30, V26 == V30, V28 == V30, V20 == V30, V22 == V30 | P_s-{T}(V30,V0), P_s-{T}(V30,V13)
% 29.24/29.44 (used 0 times, uses = {})
% 29.24/29.44
% 29.24/29.44 #287: 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 == V33, V33 == V38, V38 == V39, V39 == V41, V41 == V42, V42 == V43, V43 == V44, V44 == V45, V45 == V46, V46 == V47, V47 == V48, V48 == V49, V49 == V32; #242 ), references = 1, size of lhs = 50:
% 29.24/29.44 P_z-{F}(V0), r-{F}(V1,V0), r-{F}(V1,V2), V0 == V2, r-{F}(V3,V2), r-{F}(V3,V4), P_s-{F}(V5,V2), P_s-{F}(V6,V2), P_s-{F}(V7,V6), r-{F}(V8,V0), V2 == V8, r-{F}(V8,V2), r-{F}(V8,V9), r-{F}(V8,V10), r-{F}(V8,V11), r-{F}(V8,V12), P_s-{F}(V13,V8), P_s-{F}(V14,V8), P_s-{F}(V15,V16), V8 == V16, V2 == V16, V0 == 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,V16), P_s-{F}(V22,V21), P_s-{F}(V23,V24), V8 == V24, V0 == V24, V24 == V2, V24 == V3, V16 == V24, P_s-{F}(V25,V24), P_s-{F}(V26,V25), P_s-{F}(V27,V24), P_s-{F}(V28,V27), P_s-{F}(V29,V30), V14 == V30, V5 == V30, V15 == V30, V23 == V30, V7 == V30, V18 == V30, V29 == V30, V26 == V30, V28 == V30, V20 == V30, V22 == V30 | P_s-{T}(V30,V13)
% 29.24/29.44 (used 0 times, uses = {})
% 29.24/29.44
% 29.24/29.44 #336: 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 == V50; #289 ), references = 4, size of lhs = 45:
% 29.24/29.44 P_z-{F}(V0), P_s-{F}(V0,V1), r-{F}(V1,V0), r-{F}(V1,V2), r-{F}(V1,V3), r-{F}(V1,V4), r-{F}(V1,V5), r-{F}(V1,V6), P_s-{F}(V7,V1), P_s-{F}(V8,V9), V0 == V9, V9 == V1, P_s-{F}(V10,V9), P_s-{F}(V11,V10), P_s-{F}(V12,V13), V1 == V13, V9 == V13, V0 == V13, P_s-{F}(V14,V13), P_s-{F}(V15,V14), P_s-{F}(V16,V13), P_s-{F}(V17,V16), P_s-{F}(V18,V13), P_s-{F}(V19,V18), P_s-{F}(V20,V21), V0 == V21, V21 == V9, V21 == V1, V13 == V21, P_s-{F}(V22,V21), P_s-{F}(V23,V22), P_s-{F}(V24,V21), P_s-{F}(V25,V24), P_s-{F}(V26,V27), V7 == V27, V8 == V27, V12 == V27, V20 == V27, V11 == V27, V15 == V27, V26 == V27, V23 == V27, V25 == V27, V17 == V27, V19 == V27 | b-{T}(V1,V9)
% 29.24/29.44 (used 0 times, uses = {})
% 29.24/29.44
% 29.24/29.44 #354: mergings( V2 == V10, V10 == V11, V11 == V12, V12 == V13, V13 == V14, V14 == V15, V15 == V16, V16 == V17; #345 ), references = 1, size of lhs = 71:
% 29.24/29.44 P_z-{F}(V0), P_s-{F}(V0,V1), r-{F}(V1,V0), r-{F}(V1,V2), r-{F}(V1,V3), r-{F}(V1,V4), r-{F}(V1,V5), r-{F}(V1,V6), P_s-{F}(V7,V1), b-{F}(V1,V8), b-{F}(V9,V8), b-{F}(V9,V10), V10 == V8, b-{F}(V11,V10), b-{F}(V11,V8), b-{F}(V12,V8), b-{F}(V12,V13), V13 == V8, V13 == V10, b-{F}(V14,V13), b-{F}(V14,V8), b-{F}(V15,V13), b-{F}(V15,V10), b-{F}(V16,V13), b-{F}(V16,V10), b-{F}(V1,V17), b-{F}(V18,V17), b-{F}(V18,V19), V19 == V17, b-{F}(V1,V19), b-{F}(V1,V20), V8 == V20, V19 == V20, b-{F}(V21,V20), b-{F}(V21,V22), V22 == V20, b-{F}(V1,V23), V23 == V17, b-{F}(V24,V23), b-{F}(V24,V25), V25 == V23, b-{F}(V26,V25), b-{F}(V26,V23), b-{F}(V27,V23), b-{F}(V27,V28), V28 == V23, V28 == V25, b-{F}(V29,V28), b-{F}(V29,V23), b-{F}(V30,V28), b-{F}(V30,V25), b-{F}(V31,V28), b-{F}(V31,V25), P_s-{F}(V32,V33), P_s-{F}(V34,V35), V1 == V35, V0 == V35, P_s-{F}(V36,V35), P_s-{F}(V37,V36), P_s-{F}(V38,V35), P_s-{F}(V39,V38), P_s-{F}(V40,V35), P_s-{F}(V41,V40), P_s-{F}(V42,V43), V0 == V43, V43 == V1, V35 == V43, P_s-{F}(V44,V43), P_s-{F}(V45,V44), P_s-{F}(V46,V43), P_s-{F}(V47,V46) | P_s-{T}(V33,V0), P_s-{T}(V33,V1), P_s-{T}(V33,V8), P_s-{T}(V33,V10), P_s-{T}(V33,V13), P_s-{T}(V33,V20), P_s-{T}(V33,V22), P_s-{T}(V33,V19), P_s-{T}(V33,V23), P_s-{T}(V33,V17), P_s-{T}(V33,V25), P_s-{T}(V33,V28), P_s-{T}(V33,V35), P_s-{T}(V33,V43), P_s-{T}(V33,V7), P_s-{T}(V33,V33), P_s-{T}(V33,V34), P_s-{T}(V33,V42), P_s-{T}(V33,V32), P_s-{T}(V33,V37), P_s-{T}(V33,V45), P_s-{T}(V33,V47), P_s-{T}(V33,V39), P_s-{T}(V33,V41)
% 29.24/29.44 (used 0 times, uses = {})
% 29.24/29.44
% 29.24/29.44 #388: mergings( V8 == V9, V9 == V10, V10 == V11, V11 == V12, V12 == V13, V13 == V14, V14 == V15, V15 == V0, V0 == V56, V56 == V58, V58 == V60, V60 == V62, V62 == V64, V64 == V66, V66 == V68, V68 == V70, V70 == V72, V72 == V74, V74 == V76, V76 == V78, V78 == V80, V80 == V7, V7 == V82, V82 == V84, V84 == V86, V86 == V88, V88 == V45, V1 == V44, V45 == V90, V90 == V92, V92 == V47, V44 == V46; #355 ), references = 1, size of lhs = 105:
% 29.24/29.44 P_z-{F}(V0), P_s-{F}(V0,V1), r-{F}(V1,V0), r-{F}(V1,V2), r-{F}(V1,V3), r-{F}(V1,V4), r-{F}(V1,V5), r-{F}(V1,V6), b-{F}(V1,V7), b-{F}(V8,V7), b-{F}(V8,V9), V9 == V7, b-{F}(V10,V9), b-{F}(V10,V7), b-{F}(V11,V7), b-{F}(V11,V12), V12 == V7, V12 == V9, b-{F}(V13,V12), b-{F}(V13,V7), b-{F}(V14,V12), b-{F}(V14,V9), b-{F}(V15,V12), b-{F}(V15,V9), b-{F}(V1,V16), b-{F}(V17,V16), b-{F}(V17,V18), V18 == V16, b-{F}(V1,V18), b-{F}(V1,V19), V7 == V19, V18 == V19, b-{F}(V20,V19), b-{F}(V20,V21), V21 == V19, b-{F}(V1,V22), V22 == V16, b-{F}(V23,V22), b-{F}(V23,V24), V24 == V22, b-{F}(V25,V24), b-{F}(V25,V22), b-{F}(V26,V22), b-{F}(V26,V27), V27 == V22, V27 == V24, b-{F}(V28,V27), b-{F}(V28,V22), b-{F}(V29,V27), b-{F}(V29,V24), b-{F}(V30,V27), b-{F}(V30,V24), P_s-{F}(V31,V1), P_s-{F}(V32,V7), P_s-{F}(V33,V9), P_s-{F}(V34,V12), P_s-{F}(V35,V19), P_s-{F}(V36,V21), P_s-{F}(V37,V18), P_s-{F}(V38,V22), P_s-{F}(V39,V16), P_s-{F}(V40,V24), P_s-{F}(V41,V27), P_s-{F}(V1,V42), V1 == V42, V0 == V42, P_s-{F}(V43,V42), P_s-{F}(V44,V42), P_s-{F}(V45,V44), P_s-{F}(V46,V42), P_s-{F}(V47,V46), P_s-{F}(V48,V49), V0 == V49, V49 == V1, V42 == 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), V31 == V59, V32 == V59, V33 == V59, V34 == V59, V35 == V59, V36 == V59, V37 == V59, V38 == V59, V39 == V59, V40 == V59, V41 == V59, V43 == V59, V48 == V59, V58 == V59, V45 == V59, V51 == V59, V54 == V59, V57 == V59, P_s-{F}(V60,V59), P_s-{F}(V61,V60), V61 == V59 | P_s-{T}(V59,V47)
% 29.24/29.44 (used 0 times, uses = {})
% 29.24/29.44
% 29.24/29.44 #477: 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 == V47, V47 == V48, V48 == V56, V56 == V63, V63 == V70, V70 == V71, V71 == V72, V72 == V73, V73 == V74, V74 == V75, V75 == V76, V76 == V77, V77 == V78, V78 == V84, V84 == V86, V86 == V87, V87 == V88, V88 == V89, V89 == V90, V90 == V91, V91 == V92, V92 == V93, V93 == V94, V94 == V95, V95 == V96, V96 == V97, V97 == V98, V98 == V99, V99 == V100, V100 == V101, V101 == V102, V102 == V103, V49 == V104, V103 == V107, V107 == V108, V108 == V109, V104 == V110, V109 == V111, V110 == V112; #393 ), references = 1, size of lhs = 105:
% 29.24/29.44 P_z-{F}(V0), P_s-{F}(V0,V1), r-{F}(V1,V0), r-{F}(V1,V2), r-{F}(V1,V3), r-{F}(V1,V4), r-{F}(V1,V5), r-{F}(V1,V6), P_s-{F}(V7,V1), r-{F}(V1,V8), r-{F}(V1,V9), r-{F}(V1,V10), r-{F}(V1,V11), r-{F}(V1,V12), P_s-{F}(V13,V1), r-{F}(V1,V14), r-{F}(V1,V15), r-{F}(V1,V16), r-{F}(V1,V17), r-{F}(V1,V18), P_s-{F}(V19,V1), r-{F}(V1,V20), r-{F}(V1,V21), r-{F}(V1,V22), r-{F}(V1,V23), r-{F}(V1,V24), P_s-{F}(V25,V1), P_s-{F}(V1,V26), V1 == V26, V0 == V26, P_s-{F}(V27,V26), P_s-{F}(V28,V26), P_s-{F}(V29,V28), P_s-{F}(V30,V31), V0 == V31, V31 == V1, P_s-{F}(V32,V31), P_s-{F}(V33,V31), P_s-{F}(V34,V31), P_s-{F}(V35,V31), P_s-{F}(V36,V31), P_s-{F}(V37,V36), P_s-{F}(V38,V39), V1 == V39, V31 == V39, V0 == V39, P_s-{F}(V40,V39), P_s-{F}(V41,V40), P_s-{F}(V42,V39), P_s-{F}(V43,V42), P_s-{F}(V44,V39), P_s-{F}(V45,V44), P_s-{F}(V46,V47), P_s-{F}(V48,V47), P_s-{F}(V49,V47), P_s-{F}(V50,V47), P_s-{F}(V51,V47), P_s-{F}(V52,V47), P_s-{F}(V53,V54), V0 == V54, V54 == V1, V54 == V31, P_s-{F}(V55,V54), P_s-{F}(V56,V54), P_s-{F}(V57,V54), P_s-{F}(V58,V57), P_s-{F}(V59,V60), V1 == V60, V54 == V60, V0 == V60, P_s-{F}(V61,V60), P_s-{F}(V62,V61), P_s-{F}(V63,V60), P_s-{F}(V64,V63), P_s-{F}(V65,V60), P_s-{F}(V66,V65), P_s-{F}(V67,V68), V1 == V68, V0 == V68, P_s-{F}(V69,V68), P_s-{F}(V70,V69), P_s-{F}(V71,V68), P_s-{F}(V72,V71), P_s-{F}(V73,V68), P_s-{F}(V74,V73), P_s-{F}(V75,V76), V0 == V76, V76 == V1, V68 == V76, P_s-{F}(V77,V76), P_s-{F}(V78,V77), P_s-{F}(V79,V76), P_s-{F}(V80,V79), P_s-{F}(V81,V82), V0 == V82, V82 == V1, V26 == V82, P_s-{F}(V83,V82), P_s-{F}(V84,V83), P_s-{F}(V85,V82), P_s-{F}(V86,V85), P_s-{F}(V87,V86), P_s-{F}(V88,V82), P_s-{F}(V89,V88), P_s-{F}(V90,V89) | P_s-{T}(V47,V0), P_s-{T}(V47,V31), P_s-{T}(V47,V1), P_s-{T}(V47,V39), P_s-{T}(V47,V7), P_s-{T}(V47,V30), P_s-{T}(V47,V38), P_s-{T}(V47,V47), P_s-{T}(V47,V37), P_s-{T}(V47,V41), P_s-{T}(V47,V46), P_s-{T}(V47,V48), P_s-{T}(V47,V43), P_s-{T}(V47,V45), P_s-{T}(V47,V54), P_s-{T}(V47,V60), P_s-{T}(V47,V13), P_s-{T}(V47,V53), P_s-{T}(V47,V59), P_s-{T}(V47,V58), P_s-{T}(V47,V62), P_s-{T}(V47,V49), P_s-{T}(V47,V50), P_s-{T}(V47,V64), P_s-{T}(V47,V66), P_s-{T}(V47,V68), P_s-{T}(V47,V76), P_s-{T}(V47,V19), P_s-{T}(V47,V67), P_s-{T}(V47,V75), P_s-{T}(V47,V51), P_s-{T}(V47,V70), P_s-{T}(V47,V78), P_s-{T}(V47,V80), P_s-{T}(V47,V72), P_s-{T}(V47,V74), P_s-{T}(V47,V25), P_s-{T}(V47,V32), P_s-{T}(V47,V55), P_s-{T}(V47,V33), P_s-{T}(V47,V34), P_s-{T}(V47,V35), P_s-{T}(V47,V56), P_s-{T}(V47,V27), P_s-{T}(V47,V81), P_s-{T}(V47,V29), P_s-{T}(V47,V84), P_s-{T}(V47,V87), P_s-{T}(V47,V90), P_s-{T}(V47,V52)
% 29.24/29.44 (used 0 times, uses = {})
% 29.24/29.44
% 29.24/29.44 #597: 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 == V44, V44 == V45, V45 == V46, V46 == V54, V54 == V61, V61 == V68, V68 == V69, V69 == V70, V70 == V71, V71 == V72, V72 == V73, V73 == V74, V74 == V75, V75 == V76, V76 == V82, V82 == V84, V84 == V85, V85 == V86, V86 == V87, V87 == V88, V88 == V89, V89 == V90, V90 == V91, V91 == V92, V92 == V93, V93 == V94, V94 == V95, V95 == V96, V96 == V97, V97 == V98, V98 == V99, V99 == V100, V100 == V101, V47 == V102, V101 == V105, V105 == V106, V106 == V107, V102 == V108, V107 == V109, V108 == V110, V109 == V174, V174 == V176, V176 == V178, V178 == V180, V180 == V182, V182 == V184, V184 == V186, V186 == V188, V188 == V190, V190 == V192, V192 == V194, V194 == V196, V196 == V198, V198 == V200, V200 == V202, V202 == V204, V204 == V206, V206 == 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; #478 ), references = 1, size of lhs = 175:
% 29.24/29.44 P_z-{F}(V0), P_s-{F}(V0,V1), r-{F}(V1,V0), r-{F}(V1,V2), r-{F}(V1,V3), r-{F}(V1,V4), r-{F}(V1,V5), r-{F}(V1,V6), P_s-{F}(V7,V1), r-{F}(V1,V8), r-{F}(V1,V9), r-{F}(V1,V10), r-{F}(V1,V11), r-{F}(V1,V12), P_s-{F}(V13,V1), r-{F}(V1,V14), r-{F}(V1,V15), r-{F}(V1,V16), r-{F}(V1,V17), r-{F}(V1,V18), P_s-{F}(V19,V1), r-{F}(V1,V20), r-{F}(V1,V21), r-{F}(V1,V22), r-{F}(V1,V23), r-{F}(V1,V24), P_s-{F}(V25,V1), P_s-{F}(V1,V26), V1 == V26, V0 == V26, P_s-{F}(V27,V1), P_s-{F}(V28,V26), P_s-{F}(V29,V28), P_s-{F}(V30,V26), P_s-{F}(V31,V30), P_s-{F}(V32,V33), P_s-{F}(V33,V34), V1 == V34, V0 == V34, P_s-{F}(V35,V34), P_s-{F}(V36,V34), P_s-{F}(V37,V36), P_s-{F}(V38,V34), P_s-{F}(V39,V38), P_s-{F}(V40,V34), P_s-{F}(V41,V40), P_s-{F}(V42,V43), P_s-{F}(V43,V44), V0 == V44, V44 == V1, P_s-{F}(V45,V44), P_s-{F}(V46,V44), P_s-{F}(V47,V46), P_s-{F}(V48,V44), P_s-{F}(V49,V48), P_s-{F}(V50,V44), P_s-{F}(V51,V50), P_s-{F}(V52,V53), P_s-{F}(V53,V54), V1 == V54, V0 == V54, P_s-{F}(V55,V54), P_s-{F}(V56,V54), P_s-{F}(V57,V56), P_s-{F}(V58,V54), P_s-{F}(V59,V58), P_s-{F}(V60,V54), P_s-{F}(V61,V60), P_s-{F}(V62,V63), P_s-{F}(V63,V64), P_s-{F}(V64,V65), V0 == V65, V65 == V1, V26 == V65, P_s-{F}(V66,V65), P_s-{F}(V67,V66), P_s-{F}(V68,V65), P_s-{F}(V69,V68), P_s-{F}(V70,V69), P_s-{F}(V71,V65), P_s-{F}(V72,V71), P_s-{F}(V73,V72), P_s-{F}(V74,V75), V0 == V75, V75 == V1, V75 == V34, V44 == V75, P_s-{F}(V76,V75), P_s-{F}(V77,V76), P_s-{F}(V78,V75), P_s-{F}(V79,V78), P_s-{F}(V80,V75), P_s-{F}(V81,V80), P_s-{F}(V82,V75), P_s-{F}(V83,V82), P_s-{F}(V84,V75), P_s-{F}(V85,V84), P_s-{F}(V86,V75), P_s-{F}(V87,V86), P_s-{F}(V88,V87), P_s-{F}(V89,V90), V74 == V90, V27 == V90, V35 == V90, V77 == V90, V37 == V90, V89 == V90, V88 == V90, V45 == V90, V47 == V90, V55 == V90, V57 == V90, V79 == V90, V49 == V90, V81 == V90, V83 == V90, V85 == V90, V51 == V90, V29 == V90, V67 == V90, V70 == V90, P_s-{F}(V91,V90), P_s-{F}(V92,V91), V92 == V90, P_s-{F}(V93,V90), P_s-{F}(V94,V93), V94 == V90, P_s-{F}(V95,V90), P_s-{F}(V96,V95), V96 == V90, P_s-{F}(V97,V90), P_s-{F}(V98,V97), V98 == V90, P_s-{F}(V99,V90), P_s-{F}(V100,V99), V100 == V90, P_s-{F}(V101,V90), P_s-{F}(V102,V101), V102 == V90, P_s-{F}(V103,V104), V1 == V104, V44 == V104, V0 == V104, V103 == V90, P_s-{F}(V105,V104), P_s-{F}(V106,V105), V106 == V90, P_s-{F}(V107,V104), P_s-{F}(V108,V107), P_s-{F}(V109,V108), V109 == V90, P_s-{F}(V110,V104), P_s-{F}(V111,V110), P_s-{F}(V112,V111), V112 == V90, P_s-{F}(V113,V104), P_s-{F}(V114,V113), P_s-{F}(V115,V114), V115 == V90, P_s-{F}(V116,V117), V0 == V117, V117 == V1, V54 == V117, V116 == V90, P_s-{F}(V118,V117), P_s-{F}(V119,V118), V119 == V90, P_s-{F}(V120,V117), P_s-{F}(V121,V120), P_s-{F}(V122,V121), V122 == V90, P_s-{F}(V123,V117), P_s-{F}(V124,V123), P_s-{F}(V125,V124), V125 == V90 | P_s-{T}(V90,V0), P_s-{T}(V90,V7), P_s-{T}(V90,V32), P_s-{T}(V90,V39), P_s-{T}(V90,V41), P_s-{T}(V90,V13), P_s-{T}(V90,V42), P_s-{T}(V90,V19), P_s-{T}(V90,V52), P_s-{T}(V90,V59), P_s-{T}(V90,V61), P_s-{T}(V90,V25), P_s-{T}(V90,V31), P_s-{T}(V90,V62), P_s-{T}(V90,V73)
% 29.24/29.44 (used 0 times, uses = {})
% 29.24/29.44
% 29.24/29.44 #743: 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 == V44, V44 == V46, V46 == V45, V45 == V54, V54 == V61, V61 == V68, V68 == V69, V69 == V70, V70 == V71, V71 == V72, V72 == V73, V73 == V74, V74 == V75, V75 == V76, V76 == V82, V82 == V84, V84 == V85, V85 == V86, V86 == V87, V87 == V88, V88 == V89, V89 == V90, V90 == V91, V91 == V92, V92 == V93, V93 == V94, V94 == V95, V95 == V96, V96 == V97, V97 == V98, V98 == V99, V99 == V100, V100 == V101, V47 == V102, V101 == V104, V104 == V105, V105 == V106, V102 == V107, V106 == V108, V107 == V109, V108 == V110, V110 == V111, V111 == V113, V113 == 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, V126 == V127, V127 == V128, V128 == V129, V129 == V130, V130 == V131, V131 == V132, V132 == V133, V133 == V134, V134 == V135, V135 == V136, V136 == V137, V137 == V138, V138 == V139, V139 == V140, V140 == V141, V141 == V142, V142 == V143, V143 == V144, V144 == V145, V145 == V53, V53 == V150, V109 == V151, V103 == V152, V150 == V157, V151 == V156, V157 == V159, V156 == V158, V159 == V60, V60 == V160, V158 == V161, V152 == V162, V160 == V67, V67 == V170, V161 == V171, V162 == V172, V170 == V177, V171 == V176, V177 == V179, V176 == V178, V179 == V83, V83 == V149, V178 == V148, V149 == V180, V148 == V181, V172 == V182; #598 ), references = 1, size of lhs = 146:
% 29.24/29.44 P_z-{F}(V0), P_s-{F}(V0,V1), r-{F}(V1,V0), r-{F}(V1,V2), r-{F}(V1,V3), r-{F}(V1,V4), r-{F}(V1,V5), r-{F}(V1,V6), r-{F}(V1,V7), r-{F}(V1,V8), r-{F}(V1,V9), r-{F}(V1,V10), r-{F}(V1,V11), r-{F}(V1,V12), r-{F}(V1,V13), r-{F}(V1,V14), r-{F}(V1,V15), r-{F}(V1,V16), r-{F}(V1,V17), r-{F}(V1,V18), r-{F}(V1,V19), r-{F}(V1,V20), r-{F}(V1,V21), P_s-{F}(V22,V1), P_s-{F}(V1,V23), V1 == V23, V0 == V23, P_s-{F}(V24,V23), P_s-{F}(V25,V23), P_s-{F}(V26,V23), P_s-{F}(V23,V27), V0 == V27, V27 == V1, V23 == V27, P_s-{F}(V28,V23), P_s-{F}(V29,V28), P_s-{F}(V30,V23), P_s-{F}(V31,V30), P_s-{F}(V32,V23), P_s-{F}(V33,V32), P_s-{F}(V34,V23), P_s-{F}(V35,V34), P_s-{F}(V36,V23), P_s-{F}(V37,V36), P_s-{F}(V38,V23), P_s-{F}(V39,V38), P_s-{F}(V40,V27), P_s-{F}(V41,V40), P_s-{F}(V42,V27), P_s-{F}(V43,V42), P_s-{F}(V44,V43), P_s-{F}(V45,V27), P_s-{F}(V46,V45), P_s-{F}(V47,V46), P_s-{F}(V48,V49), V0 == V49, V49 == V1, V23 == 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,V49), P_s-{F}(V55,V54), P_s-{F}(V56,V49), P_s-{F}(V57,V56), P_s-{F}(V58,V49), P_s-{F}(V59,V58), P_s-{F}(V60,V49), P_s-{F}(V61,V60), P_s-{F}(V62,V61), P_s-{F}(V63,V64), V48 == V64, V22 == V64, V24 == V64, V51 == V64, V31 == V64, V63 == V64, V62 == V64, V25 == V64, V33 == V64, V26 == V64, V39 == V64, V53 == V64, V35 == V64, V55 == V64, V57 == V64, V59 == V64, V37 == V64, V29 == V64, V41 == V64, V44 == V64, P_s-{F}(V65,V64), P_s-{F}(V66,V65), V66 == V64, P_s-{F}(V67,V64), P_s-{F}(V68,V67), V68 == V64, P_s-{F}(V69,V64), P_s-{F}(V70,V69), V70 == V64, P_s-{F}(V71,V64), P_s-{F}(V72,V71), V72 == V64, P_s-{F}(V73,V64), P_s-{F}(V74,V73), V74 == V64, P_s-{F}(V75,V64), P_s-{F}(V76,V75), V76 == V64, P_s-{F}(V77,V78), V1 == V78, V23 == V78, V0 == V78, V77 == V64, P_s-{F}(V79,V78), P_s-{F}(V80,V79), V80 == V64, P_s-{F}(V81,V78), P_s-{F}(V82,V81), P_s-{F}(V83,V82), V83 == V64, P_s-{F}(V84,V78), P_s-{F}(V85,V84), P_s-{F}(V86,V85), V86 == V64, P_s-{F}(V87,V78), P_s-{F}(V88,V87), P_s-{F}(V89,V88), V89 == V64, P_s-{F}(V90,V91), V0 == V91, V91 == V1, V23 == V91, V90 == V64, P_s-{F}(V92,V91), P_s-{F}(V93,V92), V93 == V64, P_s-{F}(V94,V91), P_s-{F}(V95,V94), P_s-{F}(V96,V95), V96 == V64, P_s-{F}(V97,V91), P_s-{F}(V98,V97), P_s-{F}(V99,V98), V99 == V64 | P_s-{T}(V64,V47)
% 29.24/29.44 (used 0 times, uses = {})
% 29.24/29.44
% 29.24/29.44 #892: 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 == V47, V47 == V49, V49 == V55, V55 == V61, V61 == V67, V67 == V68, V68 == V69, V69 == V70, V70 == V71, V71 == V72, V72 == V73, V73 == V74, V74 == V75, V75 == V81, V81 == V82, V82 == V83, V83 == V84, V84 == V85, V85 == V86, V86 == V87, V87 == V88, V88 == V89, V89 == V90, V90 == V91, V91 == V92, V92 == V93, V93 == V94, V94 == V95, V95 == V96, V96 == V97, V97 == V98, V98 == V99, V48 == V100, V99 == V102, V102 == V103, V103 == V104, V100 == V105, V104 == V106, V105 == V107, V106 == V108, V108 == V109, V109 == V111, V111 == 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, V124 == V125, V125 == V126, V126 == V127, V127 == V128, V128 == V129, V129 == V130, V130 == V131, V131 == V132, V132 == V133, V133 == V134, V134 == V135, V135 == V136, V136 == V137, V137 == V138, V138 == V139, V139 == V140, V140 == V141, V141 == V142, V142 == V143, V143 == V144, V144 == V145, V107 == V146, V101 == V147, V145 == V149, V146 == V150, V149 == V151, V150 == V152, V151 == V153, V153 == V154, V152 == V155, V147 == V156, V154 == V158, V158 == V159, V155 == V160, V156 == V161, V159 == V163, V160 == V164, V163 == V165, V164 == V166, V165 == V167, V167 == V168, V166 == V169, V168 == V170, V169 == V171, V161 == V0, V170 == V172, V171 == V173; #745 ), references = 1, size of lhs = 70:
% 29.24/29.44 P_z-{F}(V0), P_s-{F}(V0,V1), r-{F}(V1,V0), r-{F}(V1,V2), r-{F}(V1,V3), r-{F}(V1,V4), r-{F}(V1,V5), r-{F}(V1,V6), r-{F}(V1,V7), r-{F}(V1,V8), r-{F}(V1,V9), r-{F}(V1,V10), r-{F}(V1,V11), r-{F}(V1,V12), r-{F}(V1,V13), r-{F}(V1,V14), r-{F}(V1,V15), r-{F}(V1,V16), r-{F}(V1,V17), r-{F}(V1,V18), r-{F}(V1,V19), r-{F}(V1,V20), r-{F}(V1,V21), P_s-{F}(V22,V1), P_s-{F}(V1,V23), V1 == V23, V0 == V23, P_s-{F}(V24,V23), P_s-{F}(V25,V23), P_s-{F}(V26,V23), P_s-{F}(V27,V23), P_s-{F}(V28,V23), P_s-{F}(V29,V23), P_s-{F}(V30,V23), P_s-{F}(V31,V23), P_s-{F}(V32,V23), P_s-{F}(V33,V23), P_s-{F}(V34,V23), P_s-{F}(V35,V23), P_s-{F}(V36,V23), P_s-{F}(V37,V23), P_s-{F}(V38,V23), P_s-{F}(V39,V23), P_s-{F}(V40,V23), P_s-{F}(V41,V23), P_s-{F}(V42,V41), P_s-{F}(V43,V23), P_s-{F}(V44,V43), P_s-{F}(V45,V23), P_s-{F}(V46,V45), P_s-{F}(V47,V23), P_s-{F}(V48,V47), P_s-{F}(V49,V23), P_s-{F}(V50,V49), P_s-{F}(V51,V23), P_s-{F}(V52,V51), P_s-{F}(V53,V23), P_s-{F}(V54,V53), P_s-{F}(V55,V23), P_s-{F}(V56,V55), P_s-{F}(V57,V23), P_s-{F}(V58,V57), P_s-{F}(V59,V23), P_s-{F}(V60,V59), P_s-{F}(V61,V23), P_s-{F}(V62,V61), P_s-{F}(V63,V23), P_s-{F}(V64,V63), P_s-{F}(V65,V23), P_s-{F}(V66,V65) | P_s-{T}(V23,V0), P_s-{T}(V23,V1), P_s-{T}(V23,V23), P_s-{T}(V23,V22), P_s-{T}(V23,V24), P_s-{T}(V23,V28), P_s-{T}(V23,V44), P_s-{T}(V23,V56), P_s-{T}(V23,V25), P_s-{T}(V23,V46), P_s-{T}(V23,V26), P_s-{T}(V23,V52), P_s-{T}(V23,V29), P_s-{T}(V23,V48), P_s-{T}(V23,V30), P_s-{T}(V23,V31), P_s-{T}(V23,V32), P_s-{T}(V23,V50), P_s-{T}(V23,V42), P_s-{T}(V23,V27), P_s-{T}(V23,V54), P_s-{T}(V23,V33), P_s-{T}(V23,V34), P_s-{T}(V23,V35), P_s-{T}(V23,V36), P_s-{T}(V23,V37), P_s-{T}(V23,V38), P_s-{T}(V23,V39), P_s-{T}(V23,V58), P_s-{T}(V23,V60), P_s-{T}(V23,V62), P_s-{T}(V23,V40), P_s-{T}(V23,V64), P_s-{T}(V23,V66)
% 29.24/29.44 (used 0 times, uses = {})
% 29.24/29.44
% 29.24/29.44 #1063: 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 == V44, V44 == V45, V45 == V47, V47 == V53, V53 == V59, V59 == V65, V65 == V66, V66 == V67, V67 == V68, V68 == V69, V69 == V70, V70 == V71, V71 == V72, V72 == V73, V73 == V79, V79 == V80, V80 == V81, V81 == V82, V82 == V83, V83 == V84, V84 == V85, V85 == V86, V86 == V87, V87 == V88, V88 == V89, V89 == V90, V90 == V91, V91 == V92, V92 == V93, V93 == V94, V94 == V95, V95 == V96, V96 == V97, V46 == V98, V97 == V100, V100 == V101, V101 == V102, V98 == V103, V102 == V104, V103 == V105, V104 == V106, V106 == V107, V107 == V109, V109 == 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, V122 == V123, V123 == V124, V124 == V125, V125 == V126, V126 == V127, V127 == V128, V128 == V129, V129 == V130, V130 == V131, V131 == V132, V132 == V133, V133 == V134, V134 == V135, V135 == V136, V136 == V137, V137 == V138, V138 == V139, V139 == V140, V140 == V141, V141 == V142, V142 == V143, V105 == V144, V99 == V145, V143 == V147, V144 == V148, V147 == V149, V148 == V150, V149 == V151, V151 == V152, V150 == V153, V145 == V154, V152 == V156, V156 == V157, V153 == V158, V154 == V159, V157 == V161, V158 == V162, V161 == V163, V162 == V164, V163 == V165, V165 == V166, V164 == V167, V166 == V168, V167 == V169, V159 == V170, V168 == V171, V169 == V172, V171 == V213, V213 == V215, V215 == V217, V217 == V219, V219 == V221, V221 == V223, V223 == V225, V225 == V227, V227 == V229, V229 == V231, V231 == V233, V233 == V235, V235 == V237, V237 == V239, V239 == V241, V241 == V243, V243 == V245, V245 == V247, V247 == V249, V249 == V251, V251 == V253, V253 == V255, V255 == V257; #893 ), references = 1, size of lhs = 116:
% 29.24/29.44 P_z-{F}(V0), P_s-{F}(V0,V1), r-{F}(V1,V0), r-{F}(V1,V2), r-{F}(V1,V3), r-{F}(V1,V4), r-{F}(V1,V5), r-{F}(V1,V6), r-{F}(V1,V7), r-{F}(V1,V8), r-{F}(V1,V9), r-{F}(V1,V10), r-{F}(V1,V11), r-{F}(V1,V12), r-{F}(V1,V13), r-{F}(V1,V14), r-{F}(V1,V15), r-{F}(V1,V16), r-{F}(V1,V17), r-{F}(V1,V18), r-{F}(V1,V19), r-{F}(V1,V20), r-{F}(V1,V21), P_s-{F}(V22,V1), P_s-{F}(V1,V23), V1 == V23, V0 == V23, P_s-{F}(V24,V1), V24 == V23, P_s-{F}(V25,V23), V25 == V23, P_s-{F}(V26,V23), V26 == V23, P_s-{F}(V27,V23), V27 == V23, P_s-{F}(V28,V23), V28 == V23, P_s-{F}(V29,V23), V29 == V23, P_s-{F}(V30,V23), P_s-{F}(V31,V30), V31 == V23, P_s-{F}(V32,V23), P_s-{F}(V33,V32), V33 == V23, P_s-{F}(V34,V23), P_s-{F}(V35,V34), V35 == V23, P_s-{F}(V36,V23), P_s-{F}(V37,V36), V37 == V23, P_s-{F}(V38,V23), P_s-{F}(V39,V38), V39 == V23, P_s-{F}(V40,V23), P_s-{F}(V41,V40), V41 == V23, P_s-{F}(V42,V23), P_s-{F}(V43,V42), V43 == V23, P_s-{F}(V44,V23), P_s-{F}(V45,V44), V45 == V23, P_s-{F}(V46,V23), P_s-{F}(V47,V46), V47 == V23, P_s-{F}(V48,V23), P_s-{F}(V49,V48), V49 == V23, P_s-{F}(V50,V23), P_s-{F}(V51,V50), V51 == V23, P_s-{F}(V52,V23), P_s-{F}(V53,V52), V53 == V23, P_s-{F}(V54,V23), P_s-{F}(V55,V54), V55 == V23, P_s-{F}(V56,V23), P_s-{F}(V57,V56), V57 == V23, P_s-{F}(V58,V23), P_s-{F}(V59,V58), V59 == V23, P_s-{F}(V60,V23), P_s-{F}(V61,V60), V61 == V23, P_s-{F}(V62,V23), P_s-{F}(V63,V62), V63 == V23, P_s-{F}(V64,V23), P_s-{F}(V65,V64), P_s-{F}(V66,V23), P_s-{F}(V67,V66), P_s-{F}(V68,V23), P_s-{F}(V69,V68), P_s-{F}(V70,V23), P_s-{F}(V71,V70), P_s-{F}(V72,V23), P_s-{F}(V73,V72), P_s-{F}(V74,V23), P_s-{F}(V75,V74), P_s-{F}(V76,V23), P_s-{F}(V77,V76), P_s-{F}(V78,V23), P_s-{F}(V79,V78), P_s-{F}(V80,V23), P_s-{F}(V81,V80), P_s-{F}(V82,V23), P_s-{F}(V83,V82), P_s-{F}(V84,V23), P_s-{F}(V85,V84), P_s-{F}(V86,V23), P_s-{F}(V87,V86), P_s-{F}(V88,V23), P_s-{F}(V89,V88) | P_s-{T}(V23,V0), P_s-{T}(V23,V22), P_s-{T}(V23,V67), P_s-{T}(V23,V79), P_s-{T}(V23,V69), P_s-{T}(V23,V75), P_s-{T}(V23,V71), P_s-{T}(V23,V73), P_s-{T}(V23,V65), P_s-{T}(V23,V77), P_s-{T}(V23,V81), P_s-{T}(V23,V83), P_s-{T}(V23,V85), P_s-{T}(V23,V87), P_s-{T}(V23,V89)
% 29.24/29.44 (used 0 times, uses = {})
% 29.24/29.44
% 29.24/29.44 #1259: 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 == V44, V44 == V45, V45 == V47, V47 == V53, V53 == V59, V59 == V65, V65 == V66, V66 == V67, V67 == V68, V68 == V69, V69 == V70, V70 == V71, V71 == V72, V72 == V73, V73 == V79, V79 == V80, V80 == V81, V81 == V82, V82 == V83, V83 == V84, V84 == V85, V85 == V86, V86 == V87, V87 == V88, V88 == V89, V89 == V90, V90 == V91, V91 == V92, V92 == V93, V93 == V94, V94 == V95, V95 == V96, V96 == V97, V46 == V98, V97 == V100, V100 == V101, V101 == V102, V98 == V103, V102 == V104, V103 == V105, V104 == V106, V106 == V107, V107 == V109, V109 == 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, V122 == V123, V123 == V124, V124 == V125, V125 == V126, V126 == V127, V127 == V128, V128 == V129, V129 == V130, V130 == V131, V131 == V132, V132 == V133, V133 == V134, V134 == V135, V135 == V136, V136 == V137, V137 == V138, V138 == V139, V139 == V140, V140 == V141, V141 == V142, V142 == V143, V105 == V144, V99 == V145, V143 == V146, V144 == V147, V146 == V148, V147 == V149, V148 == V150, V150 == V151, V149 == V152, V145 == V153, V151 == V154, V154 == V155, V152 == V156, V153 == V157, V155 == V158, V156 == V159, V158 == V160, V159 == V161, V160 == V162, V162 == V163, V161 == V164, V163 == V165, V164 == V166, V157 == V167, V165 == V168, V166 == V169, V168 == V170, V170 == V172, V172 == V174, V174 == V176, V176 == V178, V178 == V180, V180 == V181, V181 == V182, V182 == V183, V183 == V184, V184 == V185, V185 == V186, V186 == V187, V187 == V188, V188 == V189, V189 == V190, V190 == V191, V191 == V192, V192 == V193, V193 == V194, V194 == V195, V195 == V196, V196 == V198, V198 == V108, V108 == V236, V169 == V235, V236 == V248, V235 == V247, V248 == V238, V247 == V237, V238 == V244, V237 == V243, V244 == V240, V243 == V239, V240 == V242, V239 == V241, V242 == V234, V241 == V233, V234 == V246, V233 == V245, V246 == V250, V245 == V249, V250 == V252, V249 == V251, V252 == V254, V251 == V253, V254 == V256, V253 == V255; #1064 ), references = 1, size of lhs = 91:
% 29.24/29.44 P_z-{F}(V0), P_s-{F}(V0,V1), r-{F}(V1,V0), r-{F}(V1,V2), r-{F}(V1,V3), r-{F}(V1,V4), r-{F}(V1,V5), r-{F}(V1,V6), r-{F}(V1,V7), r-{F}(V1,V8), r-{F}(V1,V9), r-{F}(V1,V10), r-{F}(V1,V11), r-{F}(V1,V12), r-{F}(V1,V13), r-{F}(V1,V14), r-{F}(V1,V15), r-{F}(V1,V16), r-{F}(V1,V17), r-{F}(V1,V18), r-{F}(V1,V19), r-{F}(V1,V20), r-{F}(V1,V21), P_s-{F}(V22,V1), P_s-{F}(V1,V23), V1 == V23, V0 == V23, V22 == V23, P_s-{F}(V24,V23), V24 == V23, P_s-{F}(V25,V23), V25 == V23, P_s-{F}(V26,V23), V26 == V23, P_s-{F}(V27,V23), V27 == V23, P_s-{F}(V28,V23), V28 == V23, P_s-{F}(V29,V23), P_s-{F}(V30,V29), V30 == V23, P_s-{F}(V31,V23), P_s-{F}(V32,V31), V32 == V23, P_s-{F}(V33,V23), P_s-{F}(V34,V33), V34 == V23, P_s-{F}(V35,V23), P_s-{F}(V36,V35), V36 == V23, P_s-{F}(V37,V23), P_s-{F}(V38,V37), V38 == V23, P_s-{F}(V39,V23), P_s-{F}(V40,V39), V40 == V23, P_s-{F}(V41,V23), P_s-{F}(V42,V41), V42 == V23, P_s-{F}(V43,V23), P_s-{F}(V44,V43), V44 == V23, P_s-{F}(V45,V23), P_s-{F}(V46,V45), V46 == V23, P_s-{F}(V47,V23), P_s-{F}(V48,V47), V48 == V23, P_s-{F}(V49,V23), P_s-{F}(V50,V49), V50 == V23, P_s-{F}(V51,V23), P_s-{F}(V52,V51), V52 == V23, P_s-{F}(V53,V23), P_s-{F}(V54,V53), V54 == V23, P_s-{F}(V55,V23), P_s-{F}(V56,V55), V56 == V23, P_s-{F}(V57,V23), P_s-{F}(V58,V57), V58 == V23, P_s-{F}(V59,V23), P_s-{F}(V60,V59), V60 == V23, P_s-{F}(V61,V23), P_s-{F}(V62,V61), V62 == V23, P_s-{F}(V63,V23), P_s-{F}(V64,V63) | P_s-{T}(V23,V64)
% 29.24/29.44 (used 0 times, uses = {})
% 29.24/29.44
% 29.24/29.44 #1456: 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 == V2, V2 == 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, V1 == V76, V75 == V78, V78 == V79, V79 == V80, V76 == V81, V80 == V82, V81 == V83, V82 == V84, V84 == V85, V85 == V86, V86 == V87, V87 == V88, V88 == V89, V89 == V90, V90 == V91, V91 == V92, V92 == V93, V93 == V94, V94 == V95, V95 == V96, V96 == 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 == V115, V115 == V116, V116 == V117, V117 == V118, V118 == V119, V119 == V120, V83 == V121, V77 == V122, V120 == V123, V121 == V124, V123 == V125, V124 == V126, V125 == V127, V127 == V128, V126 == V129, V122 == V130, V128 == V131, V131 == V132, V129 == V133, V130 == V134, V132 == V135, V133 == V136, V135 == V137, V136 == V138, V137 == V139, V139 == V140, V138 == V141, V140 == V142, V141 == V143, V134 == V144, V142 == V145, V143 == V146, V145 == V147, V147 == V149, V149 == V151, V151 == V153, V153 == 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 == V175, V175 == V176, V176 == V177, V146 == 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, V199 == V201, V200 == V202; #1261 ), references = 2, size of lhs = 69:
% 29.24/29.44 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)
% 29.24/29.44 (used 0 times, uses = {})
% 29.24/29.44
% 29.24/29.44 #1459: mergings( V0 == V3; #1457 ), references = 7, size of lhs = 5:
% 29.24/29.44 P_z-{F}(V0), r-{F}(V1,V2), r-{F}(V2,V3), r-{F}(V2,V4), V1 == V4 | b-{T}(V1,V4)
% 29.24/29.44 (used 0 times, uses = {})
% 29.24/29.44
% 29.24/29.44 #1466: mergings( V0 == V3, V3 == V4, V4 == V5; #1462 ), references = 2, size of lhs = 16:
% 29.24/29.44 P_z-{F}(V0), b-{F}(V1,V2), r-{F}(V3,V2), r-{F}(V3,V4), r-{F}(V2,V5), V5 == V2, b-{F}(V6,V5), r-{F}(V6,V2), r-{F}(V2,V7), r-{F}(V2,V8), #-{F} V9, V1 == V9, V9 == V2, V9 == V3, V5 == V9, V6 == V9 | r-{T}(V1,V9)
% 29.24/29.44 (used 0 times, uses = {})
% 29.24/29.44
% 29.24/29.44 #1480: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10; #1471 ), references = 2, size of lhs = 31:
% 29.24/29.44 P_z-{F}(V0), b-{F}(V1,V2), r-{F}(V2,V3), r-{F}(V2,V4), V4 == V2, r-{F}(V2,V5), r-{F}(V2,V6), r-{F}(V1,V7), V7 == V1, b-{F}(V2,V7), r-{F}(V8,V4), r-{F}(V8,V9), r-{F}(V4,V10), V10 == V4, b-{F}(V11,V10), r-{F}(V11,V4), r-{F}(V4,V12), r-{F}(V4,V13), r-{F}(V2,V14), #-{F} V15, V15 == V2, V15 == V4, #-{F} V16, V1 == V16, V15 == V16, V16 == V4, V16 == V8, V10 == V16, V11 == V16, V7 == V16, V2 == V16 | b-{T}(V15,V2)
% 29.24/29.44 (used 0 times, uses = {})
% 29.24/29.44
% 29.24/29.44 #1483: mergings( V0 == V3; #1481 ), references = 2, size of lhs = 5:
% 29.24/29.44 P_z-{F}(V0), b-{F}(V1,V2), b-{F}(V2,V3), b-{F}(V4,V2), V4 == V1 | r-{T}(V4,V1)
% 29.24/29.44 (used 0 times, uses = {})
% 29.24/29.44
% 29.24/29.44 #1491: mergings( V2 == V3, V3 == V4, V4 == V5; #1487 ), references = 1, size of lhs = 34:
% 29.24/29.44 P_z-{F}(V0), b-{F}(V1,V2), r-{F}(V2,V3), r-{F}(V2,V4), V4 == V2, r-{F}(V2,V5), r-{F}(V2,V6), r-{F}(V1,V7), V7 == V1, b-{F}(V2,V7), r-{F}(V8,V4), r-{F}(V8,V9), r-{F}(V4,V10), V10 == V4, b-{F}(V11,V10), r-{F}(V11,V4), r-{F}(V4,V12), r-{F}(V4,V13), r-{F}(V2,V14), b-{F}(V15,V2), b-{F}(V2,V16), r-{F}(V15,V17), r-{F}(V15,V18), b-{F}(V2,V18), b-{F}(V18,V19), #-{F} V20, #-{F} V21, V1 == V21, V21 == V4, V21 == V8, V10 == V21, V11 == V21, V7 == V21, V2 == V21 | P_s-{T}(V20,V2), P_s-{T}(V20,V4), P_s-{T}(V20,V15), P_s-{T}(V20,V18), P_s-{T}(V20,V21)
% 29.24/29.44 (used 0 times, uses = {})
% 29.24/29.44
% 29.24/29.44 #1500: mergings( V0 == V1, V1 == V2, V2 == V3, V3 == V25, V25 == V27, V27 == V29, V29 == V31; #1492 ), references = 2, size of lhs = 41:
% 29.24/29.44 P_z-{F}(V0), b-{F}(V1,V2), r-{F}(V2,V3), r-{F}(V2,V4), V4 == V2, r-{F}(V2,V5), r-{F}(V2,V6), r-{F}(V1,V7), V7 == V1, b-{F}(V2,V7), r-{F}(V8,V4), r-{F}(V8,V9), r-{F}(V4,V10), V10 == V4, b-{F}(V11,V10), r-{F}(V11,V4), r-{F}(V4,V12), r-{F}(V4,V13), r-{F}(V2,V14), b-{F}(V2,V15), b-{F}(V2,V16), b-{F}(V16,V17), P_s-{F}(V18,V4), P_s-{F}(V19,V16), b-{F}(V20,V2), r-{F}(V20,V16), r-{F}(V20,V21), P_s-{F}(V22,V20), P_s-{F}(V23,V24), V1 == V24, V24 == V4, V24 == V8, V10 == V24, V11 == V24, V7 == V24, V2 == V24, #-{F} V25, V18 == V25, V22 == V25, V19 == V25, V23 == V25 | P_s-{T}(V25,V2)
% 29.24/29.44 (used 0 times, uses = {})
% 29.24/29.44
% 29.24/29.44 #1525: 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; #1504 ), references = 3, size of lhs = 36:
% 29.24/29.44 P_z-{F}(V0), r-{F}(V0,V1), r-{F}(V0,V2), r-{F}(V0,V3), r-{F}(V0,V4), r-{F}(V0,V5), r-{F}(V0,V6), r-{F}(V0,V7), r-{F}(V0,V8), V8 == V0, b-{F}(V8,V0), r-{F}(V9,V8), r-{F}(V9,V10), P_s-{F}(V11,V8), r-{F}(V12,V8), r-{F}(V12,V13), r-{F}(V0,V14), P_s-{F}(V15,V8), P_s-{F}(V16,V17), V17 == V0, V17 == V8, P_s-{F}(V18,V19), V19 == V8, V19 == V9, V17 == V19, V0 == V19, #-{F} V20, V20 == V8, V20 == V12, V17 == V20, V0 == V20, #-{F} V21, V11 == V21, V15 == V21, V16 == V21, V18 == V21 | b-{T}(V8,V17)
% 29.24/29.44 (used 0 times, uses = {})
% 29.24/29.44
% 29.24/29.44 #1532: mergings( V0 == V3, V3 == V4, V4 == V5; #1528 ), references = 2, size of lhs = 9:
% 29.24/29.44 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), r-{F}(V2,V6), V3 == V6 | r-{T}(V2,V3)
% 29.24/29.44 (used 0 times, uses = {})
% 29.24/29.44
% 29.24/29.44 #1567: 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 == V38, V38 == V53, V53 == V54, V54 == V55, V55 == V56, V56 == V57, V57 == V58, V58 == V59; #1538 ), references = 1, size of lhs = 52:
% 29.24/29.44 P_z-{F}(V0), r-{F}(V0,V1), r-{F}(V0,V2), r-{F}(V0,V3), r-{F}(V0,V4), r-{F}(V0,V5), r-{F}(V0,V6), r-{F}(V0,V7), r-{F}(V0,V8), r-{F}(V0,V9), V9 == V0, b-{F}(V9,V0), r-{F}(V10,V9), r-{F}(V10,V11), P_s-{F}(V12,V9), r-{F}(V13,V9), r-{F}(V13,V14), P_s-{F}(V15,V9), r-{F}(V0,V16), r-{F}(V0,V17), r-{F}(V0,V18), r-{F}(V0,V19), r-{F}(V0,V20), r-{F}(V0,V21), r-{F}(V0,V22), r-{F}(V23,V9), r-{F}(V23,V24), P_s-{F}(V25,V9), r-{F}(V26,V9), r-{F}(V26,V27), r-{F}(V0,V28), P_s-{F}(V29,V9), b-{F}(V9,V30), r-{F}(V30,V31), r-{F}(V30,V32), r-{F}(V30,V33), r-{F}(V30,V34), r-{F}(V30,V35), P_s-{F}(V36,V37), V37 == V0, V37 == V9, V37 == V30, V37 == V32, P_s-{F}(V38,V39), V39 == V9, V39 == V23, V0 == V39, #-{F} V40, #-{F} V41, V41 == V9, V41 == V26, V0 == V41 | P_s-{T}(V40,V9), P_s-{T}(V40,V10), P_s-{T}(V40,V37), P_s-{T}(V40,V0), P_s-{T}(V40,V30), P_s-{T}(V40,V35), P_s-{T}(V40,V39), P_s-{T}(V40,V13), P_s-{T}(V40,V12), P_s-{T}(V40,V15), P_s-{T}(V40,V36), P_s-{T}(V40,V40), P_s-{T}(V40,V41), P_s-{T}(V40,V25), P_s-{T}(V40,V29), P_s-{T}(V40,V38)
% 29.24/29.44 (used 0 times, uses = {})
% 29.24/29.44
% 29.24/29.44 #1611: 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 == V51, V51 == V52, V52 == V53, V53 == V54, V54 == V55, V55 == V56, V56 == V57, V57 == V70, V70 == V29, V29 == V20, V20 == V36, V36 == V58, V58 == V72, V72 == V74, V74 == V76, V76 == V32, V32 == V31, V31 == V35, V35 == V78, V78 == V80, V80 == V82, V82 == V46, V46 == V50; #1568 ), references = 1, size of lhs = 57:
% 29.24/29.44 P_z-{F}(V0), r-{F}(V0,V1), r-{F}(V0,V2), r-{F}(V0,V3), r-{F}(V0,V4), r-{F}(V0,V5), r-{F}(V0,V6), r-{F}(V0,V7), r-{F}(V0,V8), r-{F}(V0,V9), r-{F}(V0,V10), r-{F}(V0,V11), r-{F}(V0,V12), r-{F}(V0,V13), r-{F}(V0,V14), r-{F}(V0,V15), r-{F}(V0,V16), r-{F}(V0,V17), r-{F}(V0,V18), r-{F}(V0,V19), r-{F}(V0,V20), r-{F}(V0,V21), r-{F}(V0,V22), P_s-{F}(V23,V22), r-{F}(V0,V24), V24 == V0, b-{F}(V24,V0), P_s-{F}(V0,V24), r-{F}(V25,V24), r-{F}(V25,V26), r-{F}(V27,V24), r-{F}(V27,V28), P_s-{F}(V29,V24), r-{F}(V0,V30), P_s-{F}(V31,V32), V32 == V24, V32 == V25, V0 == V32, P_s-{F}(V33,V32), P_s-{F}(V34,V35), V35 == V24, V35 == V0, V35 == V19, P_s-{F}(V36,V35), P_s-{F}(V37,V36), P_s-{F}(V38,V39), V29 == V39, V34 == V39, V23 == V39, V33 == V39, V37 == V39, V38 == V39, P_s-{F}(V40,V41), V41 == V24, V41 == V27, V0 == V41, V40 == V39 | P_s-{T}(V39,V31)
% 29.24/29.44 (used 0 times, uses = {})
% 29.24/29.44
% 29.24/29.44 #1654: 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; #1613 ), references = 2, size of lhs = 28:
% 29.24/29.44 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)
% 29.24/29.44 (used 0 times, uses = {})
% 29.24/29.44
% 29.24/29.44 #1661: mergings( V0 == V3, V3 == V4, V4 == V5; #1657 ), references = 1, size of lhs = 15:
% 29.24/29.44 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), r-{F}(V5,V7), #-{F} V8, V5 == V8, V6 == V8, V2 == V8 | r-{T}(V1,V5)
% 29.24/29.44 (used 0 times, uses = {})
% 29.24/29.44
% 29.24/29.44 #1668: mergings( V0 == V3, V3 == V4, V4 == V5; #1664 ), references = 3, size of lhs = 12:
% 29.24/29.44 P_z-{F}(V0), b-{F}(V1,V2), r-{F}(V3,V2), r-{F}(V3,V4), r-{F}(V2,V5), r-{F}(V5,V2), b-{F}(V1,V5), #-{F} V6, V1 == V6, V6 == V2, V6 == V3, V6 == V5 | r-{T}(V1,V6)
% 29.24/29.44 (used 0 times, uses = {})
% 29.24/29.44
% 29.24/29.44 #1683: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V1; #1675 ), references = 2, size of lhs = 40:
% 29.24/29.44 P_z-{F}(V0), b-{F}(V1,V0), r-{F}(V0,V2), V2 == V0, r-{F}(V2,V0), r-{F}(V1,V3), V3 == V1, V3 == V0, V2 == V3, r-{F}(V4,V3), r-{F}(V4,V5), V5 == V0, V5 == V2, V3 == V5, r-{F}(V6,V5), V3 == V6, r-{F}(V6,V7), r-{F}(V2,V8), r-{F}(V2,V9), b-{F}(V0,V10), V10 == V0, V3 == V10, r-{F}(V10,V5), b-{F}(V10,V2), b-{F}(V10,V11), b-{F}(V10,V12), P_s-{F}(V13,V2), P_s-{F}(V14,V10), r-{F}(V10,V15), P_s-{F}(V16,V3), P_s-{F}(V17,V18), V1 == V18, V18 == V2, V3 == V18, V0 == V18, #-{F} V19, V13 == V19, V16 == V19, V14 == V19, V17 == V19 | r-{T}(V0,V3)
% 29.24/29.44 (used 0 times, uses = {})
% 29.24/29.44
% 29.24/29.44 #1701: mergings( V2 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10, V10 == V11, V11 == V34, V34 == V35; #1689 ), references = 1, size of lhs = 46:
% 29.24/29.44 P_z-{F}(V0), b-{F}(V1,V0), r-{F}(V0,V2), V2 == V0, r-{F}(V2,V0), r-{F}(V1,V3), V3 == V1, V2 == V3, V3 == V0, r-{F}(V2,V4), r-{F}(V2,V5), P_s-{F}(V6,V2), P_s-{F}(V7,V3), r-{F}(V0,V8), V8 == V0, V3 == V8, r-{F}(V8,V0), r-{F}(V8,V9), r-{F}(V8,V10), b-{F}(V0,V11), V3 == V11, V11 == V0, b-{F}(V11,V2), b-{F}(V11,V0), r-{F}(V11,V3), b-{F}(V11,V8), b-{F}(V11,V12), r-{F}(V13,V12), r-{F}(V13,V14), r-{F}(V12,V15), r-{F}(V15,V12), b-{F}(V11,V15), b-{F}(V11,V16), b-{F}(V11,V17), P_s-{F}(V18,V11), b-{F}(V11,V19), b-{F}(V11,V20), P_s-{F}(V21,V8), P_s-{F}(V22,V11), r-{F}(V23,V0), V23 == V3, P_s-{F}(V24,V25), V11 == V25, V25 == V8, V0 == V25, #-{F} V26 | P_s-{T}(V26,V12), P_s-{T}(V26,V13), P_s-{T}(V26,V15), P_s-{T}(V26,V2), P_s-{T}(V26,V8), P_s-{T}(V26,V0), P_s-{T}(V26,V3), P_s-{T}(V26,V11), P_s-{T}(V26,V23), P_s-{T}(V26,V1), P_s-{T}(V26,V25), P_s-{T}(V26,V6), P_s-{T}(V26,V7), P_s-{T}(V26,V18), P_s-{T}(V26,V26), P_s-{T}(V26,V21), P_s-{T}(V26,V22), P_s-{T}(V26,V24)
% 29.24/29.44 (used 0 times, uses = {})
% 29.24/29.44
% 29.24/29.44 #1728: mergings( V0 == V1, V1 == V2, V2 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V32, V32 == V33, V33 == 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; #1702 ), references = 1, size of lhs = 73:
% 29.24/29.44 P_z-{F}(V0), r-{F}(V0,V1), V1 == V0, r-{F}(V1,V0), r-{F}(V1,V2), r-{F}(V1,V3), r-{F}(V0,V4), V4 == V0, r-{F}(V4,V0), r-{F}(V4,V5), r-{F}(V4,V6), b-{F}(V0,V7), V7 == V0, b-{F}(V7,V1), b-{F}(V7,V0), b-{F}(V7,V4), r-{F}(V7,V8), V1 == V8, V8 == V0, V8 == V4, V8 == V7, b-{F}(V7,V9), r-{F}(V9,V10), r-{F}(V10,V9), b-{F}(V7,V10), b-{F}(V7,V11), b-{F}(V7,V12), P_s-{F}(V13,V7), b-{F}(V7,V14), b-{F}(V7,V15), P_s-{F}(V16,V7), P_s-{F}(V17,V10), P_s-{F}(V18,V1), P_s-{F}(V19,V4), P_s-{F}(V20,V8), P_s-{F}(V21,V7), b-{F}(V22,V0), V8 == V22, r-{F}(V22,V8), P_s-{F}(V23,V22), P_s-{F}(V24,V1), P_s-{F}(V25,V24), P_s-{F}(V26,V8), P_s-{F}(V27,V26), r-{F}(V28,V9), r-{F}(V28,V29), P_s-{F}(V30,V28), P_s-{F}(V31,V4), P_s-{F}(V32,V31), r-{F}(V33,V0), V33 == V8, P_s-{F}(V34,V33), P_s-{F}(V35,V36), V7 == V36, V36 == V4, V0 == V36, P_s-{F}(V37,V36), P_s-{F}(V38,V37), P_s-{F}(V39,V40), V30 == V40, V17 == V40, V18 == V40, V19 == V40, V20 == V40, V21 == V40, V34 == V40, V23 == V40, V35 == V40, V25 == V40, V27 == V40, V39 == V40, V32 == V40, V38 == V40 | P_s-{T}(V40,V9), P_s-{T}(V40,V0), P_s-{T}(V40,V13), P_s-{T}(V40,V16)
% 29.24/29.44 (used 0 times, uses = {})
% 29.24/29.44
% 29.24/29.44 #1757: mergings( V0 == V1, V1 == V2, V2 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V26, V26 == V27, V27 == V28, V28 == V29, V29 == V31, V31 == V33, V33 == V35, V35 == V37, V37 == V39, V39 == V40, V40 == V41, V41 == V42, V42 == V43, V43 == V44, V44 == V45, V45 == V46, V46 == V18, V18 == V9, V9 == V22; #1729 ), references = 1, size of lhs = 72:
% 29.24/29.44 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), r-{F}(V3,V4), r-{F}(V3,V5), r-{F}(V0,V6), V6 == V0, r-{F}(V6,V0), r-{F}(V6,V7), r-{F}(V6,V8), b-{F}(V0,V9), V9 == V0, b-{F}(V9,V3), b-{F}(V9,V6), b-{F}(V9,V0), b-{F}(V9,V1), P_s-{F}(V0,V9), r-{F}(V9,V10), V3 == V10, V10 == V0, V10 == V6, V10 == V9, b-{F}(V9,V11), b-{F}(V9,V12), b-{F}(V9,V13), b-{F}(V9,V14), P_s-{F}(V15,V9), P_s-{F}(V16,V3), P_s-{F}(V17,V6), P_s-{F}(V18,V10), P_s-{F}(V19,V9), b-{F}(V20,V0), V10 == V20, r-{F}(V20,V10), P_s-{F}(V21,V20), P_s-{F}(V22,V3), P_s-{F}(V23,V22), P_s-{F}(V24,V10), P_s-{F}(V25,V24), r-{F}(V26,V0), r-{F}(V26,V27), P_s-{F}(V28,V26), P_s-{F}(V29,V6), P_s-{F}(V30,V29), r-{F}(V31,V0), V31 == V10, P_s-{F}(V32,V31), P_s-{F}(V33,V34), V9 == V34, V34 == V6, V0 == V34, P_s-{F}(V35,V34), P_s-{F}(V36,V35), P_s-{F}(V37,V38), V28 == V38, V2 == V38, V16 == V38, V17 == V38, V18 == V38, V19 == V38, V32 == V38, V21 == V38, V33 == V38, V23 == V38, V25 == V38, V37 == V38, V30 == V38, V36 == V38 | P_s-{T}(V38,V15)
% 29.24/29.44 (used 0 times, uses = {})
% 29.24/29.44
% 29.24/29.44 #1800: 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 == V49, V49 == V50; #1762 ), references = 4, size of lhs = 58:
% 29.24/29.44 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), b-{F}(V4,V7), b-{F}(V4,V8), P_s-{F}(V9,V4), P_s-{F}(V10,V4), P_s-{F}(V11,V12), V4 == V12, V0 == V12, V12 == V2, P_s-{F}(V13,V12), P_s-{F}(V14,V12), P_s-{F}(V15,V12), P_s-{F}(V16,V12), P_s-{F}(V17,V12), P_s-{F}(V18,V17), P_s-{F}(V19,V12), P_s-{F}(V20,V19), P_s-{F}(V21,V22), V22 == V0, V22 == V4, V12 == V22, P_s-{F}(V23,V22), P_s-{F}(V24,V23), P_s-{F}(V25,V26), V4 == V26, V26 == V12, V0 == V26, P_s-{F}(V27,V26), P_s-{F}(V28,V27), P_s-{F}(V29,V30), V15 == V30, V11 == V30, V13 == V30, V14 == V30, V21 == V30, V9 == V30, V16 == V30, V10 == V30, V25 == V30, V18 == V30, V24 == V30, V29 == V30, V20 == V30, V28 == V30, #-{F} V31, V12 == V31, V0 == V31, V2 == V31 | r-{T}(V4,V12)
% 29.24/29.44 (used 0 times, uses = {})
% 29.24/29.44
% 29.24/29.44 #1815: mergings( V2 == V13, V13 == V14, V14 == V15; #1810 ), references = 1, size of lhs = 40:
% 29.24/29.44 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), b-{F}(V4,V7), b-{F}(V4,V8), P_s-{F}(V9,V4), P_s-{F}(V10,V4), r-{F}(V4,V11), b-{F}(V11,V12), r-{F}(V13,V12), V12 == V13, b-{F}(V13,V14), r-{F}(V15,V14), r-{F}(V15,V16), r-{F}(V14,V17), r-{F}(V17,V14), b-{F}(V13,V17), P_s-{F}(V18,V19), P_s-{F}(V20,V19), P_s-{F}(V21,V22), V22 == V0, V22 == V4, P_s-{F}(V23,V22), P_s-{F}(V24,V23), P_s-{F}(V25,V26), V4 == V26, V0 == V26, P_s-{F}(V27,V26), P_s-{F}(V28,V27), #-{F} V29, V0 == V29, V2 == V29 | P_s-{T}(V19,V4), P_s-{T}(V19,V0), P_s-{T}(V19,V2), P_s-{T}(V19,V13), P_s-{T}(V19,V14), P_s-{T}(V19,V15), P_s-{T}(V19,V17), P_s-{T}(V19,V12), P_s-{T}(V19,V11), P_s-{T}(V19,V22), P_s-{T}(V19,V26), P_s-{T}(V19,V19), P_s-{T}(V19,V21), P_s-{T}(V19,V9), P_s-{T}(V19,V10), P_s-{T}(V19,V25), P_s-{T}(V19,V18), P_s-{T}(V19,V24), P_s-{T}(V19,V20), P_s-{T}(V19,V28), P_s-{T}(V19,V29)
% 29.24/29.44 (used 0 times, uses = {})
% 29.24/29.44
% 29.24/29.44 #1835: mergings( V0 == V11, V11 == V12, V12 == V13, V13 == V33, V33 == V35, V35 == V37, V37 == V39, V39 == V41, V41 == V43, V43 == V45, V45 == V47, V47 == V49, V49 == V51, V51 == V53, V53 == V55, V55 == V57, V57 == V59, V59 == V61; #1816 ), references = 1, size of lhs = 69:
% 29.24/29.44 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), b-{F}(V4,V7), b-{F}(V4,V8), P_s-{F}(V9,V4), P_s-{F}(V10,V4), r-{F}(V4,V11), b-{F}(V11,V12), r-{F}(V13,V12), V12 == V13, b-{F}(V13,V14), r-{F}(V14,V15), r-{F}(V15,V14), b-{F}(V13,V15), P_s-{F}(V16,V4), P_s-{F}(V17,V2), P_s-{F}(V18,V14), P_s-{F}(V19,V15), P_s-{F}(V20,V12), P_s-{F}(V21,V11), r-{F}(V22,V14), r-{F}(V22,V23), P_s-{F}(V24,V22), P_s-{F}(V25,V26), P_s-{F}(V26,V27), V27 == V0, V27 == V4, P_s-{F}(V28,V27), P_s-{F}(V29,V27), P_s-{F}(V30,V29), P_s-{F}(V31,V32), P_s-{F}(V32,V33), V4 == V33, V0 == V33, P_s-{F}(V34,V33), P_s-{F}(V35,V33), P_s-{F}(V36,V35), P_s-{F}(V37,V38), V16 == V38, V17 == V38, V18 == V38, V24 == V38, V19 == V38, V20 == V38, V21 == V38, V28 == V38, V34 == V38, V37 == V38, V30 == V38, V36 == V38, P_s-{F}(V39,V38), P_s-{F}(V40,V39), V40 == V38, P_s-{F}(V41,V38), P_s-{F}(V42,V41), V42 == V38, P_s-{F}(V43,V44), V0 == V44, V2 == V44, V43 == V38 | P_s-{T}(V38,V0), P_s-{T}(V38,V13), P_s-{T}(V38,V9), P_s-{T}(V38,V10), P_s-{T}(V38,V25), P_s-{T}(V38,V31)
% 29.24/29.44 (used 0 times, uses = {})
% 29.24/29.44
% 29.24/29.44 #1860: mergings( V11 == V12, V12 == V13, V13 == V19, V19 == V21, V21 == V23, V23 == V25, V25 == V26, V26 == V28, V28 == V30, V30 == V32, V32 == V33, V33 == V34, V34 == V35, V35 == V36, V36 == V37, V37 == V38, V38 == V39, V39 == V0, V0 == V16, V16 == V9, V9 == V10, V10 == V43, V4 == V44; #1836 ), references = 1, size of lhs = 66:
% 29.24/29.44 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), b-{F}(V4,V7), b-{F}(V4,V8), r-{F}(V4,V9), b-{F}(V9,V10), V10 == V0, r-{F}(V0,V10), P_s-{F}(V11,V4), P_s-{F}(V12,V2), P_s-{F}(V13,V10), P_s-{F}(V14,V9), b-{F}(V0,V15), r-{F}(V15,V16), r-{F}(V16,V15), b-{F}(V0,V16), P_s-{F}(V17,V15), P_s-{F}(V18,V16), P_s-{F}(V4,V19), V19 == V0, V19 == V4, P_s-{F}(V20,V19), r-{F}(V21,V15), r-{F}(V21,V22), P_s-{F}(V23,V21), P_s-{F}(V24,V19), P_s-{F}(V25,V24), P_s-{F}(V26,V27), P_s-{F}(V27,V28), V4 == V28, V0 == V28, P_s-{F}(V29,V28), P_s-{F}(V30,V28), P_s-{F}(V31,V30), P_s-{F}(V32,V33), V11 == V33, V12 == V33, V17 == V33, V23 == V33, V18 == V33, V13 == V33, V14 == V33, V20 == V33, V29 == V33, V32 == V33, V25 == V33, V31 == V33, P_s-{F}(V34,V33), P_s-{F}(V35,V34), V35 == V33, P_s-{F}(V36,V33), P_s-{F}(V37,V36), V37 == V33, P_s-{F}(V38,V39), V0 == V39, V2 == V39, V38 == V33 | P_s-{T}(V33,V26)
% 29.24/29.44 (used 0 times, uses = {})
% 29.24/29.44
% 29.24/29.44 #1895: 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 == V1, V1 == V44, V44 == V45, V45 == V46, V26 == V47, V46 == V50, V47 == V51, V48 == V52; #1865 ), references = 2, size of lhs = 68:
% 29.24/29.44 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), b-{F}(V3,V6), b-{F}(V3,V7), r-{F}(V3,V8), V0 == V8, r-{F}(V9,V8), r-{F}(V9,V10), V8 == V10, V10 == V0, r-{F}(V11,V10), V8 == V11, r-{F}(V11,V12), P_s-{F}(V13,V3), P_s-{F}(V14,V1), P_s-{F}(V15,V10), P_s-{F}(V16,V8), b-{F}(V0,V17), V8 == V17, r-{F}(V17,V8), r-{F}(V17,V10), b-{F}(V17,V18), r-{F}(V17,V19), P_s-{F}(V20,V8), P_s-{F}(V21,V17), P_s-{F}(V3,V22), V3 == V22, V0 == V22, P_s-{F}(V23,V22), P_s-{F}(V24,V22), r-{F}(V25,V8), r-{F}(V25,V26), P_s-{F}(V27,V25), P_s-{F}(V28,V22), P_s-{F}(V29,V28), P_s-{F}(V30,V22), P_s-{F}(V31,V30), P_s-{F}(V32,V33), V13 == V33, V14 == V33, V20 == V33, V27 == V33, V21 == V33, V15 == V33, V16 == V33, V23 == V33, V24 == V33, V32 == V33, V29 == V33, V31 == V33, P_s-{F}(V34,V33), P_s-{F}(V35,V34), V35 == V33, P_s-{F}(V36,V33), P_s-{F}(V37,V36), V37 == V33, P_s-{F}(V38,V39), V0 == V39, V1 == V39, V38 == V33 | r-{T}(V0,V8)
% 29.24/29.44 (used 0 times, uses = {})
% 29.24/29.44
% 29.24/29.44 #1901: mergings( V2 == V13, V13 == V14; #1898 ), references = 1, size of lhs = 35:
% 29.24/29.44 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), b-{F}(V4,V7), b-{F}(V4,V8), P_s-{F}(V9,V4), P_s-{F}(V10,V4), r-{F}(V4,V11), V11 == V4, r-{F}(V4,V12), r-{F}(V4,V13), b-{F}(V13,V11), P_s-{F}(V14,V15), P_s-{F}(V16,V15), P_s-{F}(V17,V18), V18 == V0, V18 == V4, P_s-{F}(V19,V18), P_s-{F}(V20,V19), P_s-{F}(V21,V22), V4 == V22, V0 == V22, P_s-{F}(V23,V22), P_s-{F}(V24,V23), #-{F} V25, V0 == V25, V2 == V25 | P_s-{T}(V15,V4), P_s-{T}(V15,V0), P_s-{T}(V15,V2), P_s-{T}(V15,V11), P_s-{T}(V15,V13), P_s-{T}(V15,V18), P_s-{T}(V15,V22), P_s-{T}(V15,V15), P_s-{T}(V15,V17), P_s-{T}(V15,V9), P_s-{T}(V15,V10), P_s-{T}(V15,V21), P_s-{T}(V15,V14), P_s-{T}(V15,V20), P_s-{T}(V15,V16), P_s-{T}(V15,V24), P_s-{T}(V15,V25)
% 29.24/29.44 (used 0 times, uses = {})
% 29.24/29.44
% 29.24/29.44 #1917: mergings( V0 == V11, V11 == V12, V12 == V28, V28 == V30, V30 == V32, V32 == V34, V34 == V36, V36 == V38, V38 == V40, V40 == V42, V42 == V44, V44 == V46, V46 == V48, V48 == V50; #1902 ), references = 1, size of lhs = 58:
% 29.24/29.44 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), b-{F}(V4,V7), b-{F}(V4,V8), P_s-{F}(V9,V4), P_s-{F}(V10,V4), r-{F}(V4,V11), V11 == V4, r-{F}(V4,V12), r-{F}(V4,V13), b-{F}(V13,V11), P_s-{F}(V14,V4), P_s-{F}(V15,V2), P_s-{F}(V16,V11), P_s-{F}(V17,V13), P_s-{F}(V18,V19), P_s-{F}(V19,V20), V20 == V0, V20 == V4, P_s-{F}(V21,V20), P_s-{F}(V22,V20), P_s-{F}(V23,V22), P_s-{F}(V24,V25), P_s-{F}(V25,V26), V4 == V26, V0 == V26, P_s-{F}(V27,V26), P_s-{F}(V28,V26), P_s-{F}(V29,V28), P_s-{F}(V30,V31), V14 == V31, V15 == V31, V16 == V31, V17 == V31, V21 == V31, V27 == V31, V30 == V31, V23 == V31, V29 == V31, P_s-{F}(V32,V31), P_s-{F}(V33,V32), V33 == V31, P_s-{F}(V34,V31), P_s-{F}(V35,V34), V35 == V31, P_s-{F}(V36,V37), V0 == V37, V2 == V37, V36 == V31 | P_s-{T}(V31,V0), P_s-{T}(V31,V9), P_s-{T}(V31,V10), P_s-{T}(V31,V18), P_s-{T}(V31,V24)
% 29.24/29.44 (used 0 times, uses = {})
% 29.24/29.44
% 29.24/29.44 #1937: mergings( V11 == V12, V12 == V16, V16 == V18, V18 == V20, V20 == V22, V22 == V24, V24 == V25, V25 == V26, V26 == V27, V27 == V28, V28 == V29, V29 == V30, V30 == V31, V31 == V0, V0 == V9, V9 == V10, V10 == V32, V4 == V33; #1918 ), references = 1, size of lhs = 55:
% 29.24/29.44 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), b-{F}(V4,V7), b-{F}(V4,V8), r-{F}(V4,V9), V9 == V4, r-{F}(V4,V10), r-{F}(V4,V11), b-{F}(V11,V9), P_s-{F}(V12,V4), P_s-{F}(V13,V2), P_s-{F}(V14,V9), P_s-{F}(V15,V11), P_s-{F}(V4,V16), V16 == V0, V16 == V4, P_s-{F}(V17,V16), P_s-{F}(V18,V16), P_s-{F}(V19,V18), P_s-{F}(V20,V21), P_s-{F}(V21,V22), V4 == V22, V0 == V22, P_s-{F}(V23,V22), P_s-{F}(V24,V22), P_s-{F}(V25,V24), P_s-{F}(V26,V27), V12 == V27, V13 == V27, V14 == V27, V15 == V27, V17 == V27, V23 == V27, V26 == V27, V19 == V27, V25 == V27, P_s-{F}(V28,V27), P_s-{F}(V29,V28), V29 == V27, P_s-{F}(V30,V27), P_s-{F}(V31,V30), V31 == V27, P_s-{F}(V32,V33), V0 == V33, V2 == V33, V32 == V27 | P_s-{T}(V27,V20)
% 29.24/29.44 (used 0 times, uses = {})
% 29.24/29.44
% 29.24/29.44 #1964: 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 == V34, V34 == V35, V35 == V36, V22 == V37, V36 == V40, V37 == V41, V38 == V42; #1940 ), references = 1, size of lhs = 54:
% 29.24/29.44 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), b-{F}(V4,V7), b-{F}(V4,V8), r-{F}(V4,V9), V9 == V4, r-{F}(V4,V10), r-{F}(V4,V11), V11 == V9, r-{F}(V12,V9), V11 == V12, r-{F}(V12,V13), P_s-{F}(V14,V4), P_s-{F}(V15,V2), P_s-{F}(V16,V9), P_s-{F}(V17,V11), P_s-{F}(V4,V18), V4 == V18, V0 == V18, P_s-{F}(V19,V18), P_s-{F}(V20,V18), P_s-{F}(V21,V18), P_s-{F}(V22,V21), P_s-{F}(V23,V18), P_s-{F}(V24,V23), P_s-{F}(V25,V26), V14 == V26, V15 == V26, V16 == V26, V17 == V26, V19 == V26, V20 == V26, V25 == V26, V22 == V26, V24 == V26, P_s-{F}(V27,V26), P_s-{F}(V28,V27), V28 == V26, P_s-{F}(V29,V26), P_s-{F}(V30,V29), V30 == V26, P_s-{F}(V31,V32), V0 == V32, V2 == V32, V31 == V26 | b-{T}(V11,V12)
% 29.24/29.44 (used 0 times, uses = {})
% 29.24/29.44
% 29.24/29.44 #2067: 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 == V47, V47 == V48, V48 == V50, V50 == 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 == V81, V81 == V82, V82 == V83, V83 == V94, V94 == V95, V41 == V96, V97 == V149, V95 == V99, V96 == V100, V101 == V149, V99 == 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 == V119, V119 == V129, V129 == V130, V130 == V131, V100 == V132, V133 == V149, V131 == V135, V132 == V136, V137 == V149, V135 == V152; #1971 ), references = 1, size of lhs = 135:
% 29.24/29.44 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), b-{F}(V10,V13), b-{F}(V10,V14), P_s-{F}(V15,V10), P_s-{F}(V16,V10), b-{F}(V10,V17), b-{F}(V10,V18), b-{F}(V10,V19), b-{F}(V10,V20), P_s-{F}(V21,V10), P_s-{F}(V22,V10), b-{F}(V10,V23), b-{F}(V10,V24), b-{F}(V10,V25), b-{F}(V10,V26), P_s-{F}(V27,V10), b-{F}(V10,V28), P_s-{F}(V29,V10), b-{F}(V0,V30), b-{F}(V0,V31), b-{F}(V31,V0), b-{F}(V31,V32), b-{F}(V10,V33), b-{F}(V10,V34), b-{F}(V10,V35), b-{F}(V10,V36), P_s-{F}(V37,V10), P_s-{F}(V38,V31), b-{F}(V0,V39), b-{F}(V39,V0), b-{F}(V39,V40), b-{F}(V10,V41), b-{F}(V10,V42), b-{F}(V10,V43), b-{F}(V10,V44), P_s-{F}(V45,V10), P_s-{F}(V46,V39), b-{F}(V10,V47), P_s-{F}(V48,V10), P_s-{F}(V10,V49), V10 == V49, V0 == V49, P_s-{F}(V50,V49), P_s-{F}(V51,V49), P_s-{F}(V52,V49), P_s-{F}(V53,V49), P_s-{F}(V54,V49), P_s-{F}(V55,V49), b-{F}(V0,V56), V56 == V0, P_s-{F}(V57,V56), b-{F}(V56,V58), P_s-{F}(V59,V10), P_s-{F}(V60,V10), P_s-{F}(V61,V49), P_s-{F}(V62,V61), P_s-{F}(V63,V49), P_s-{F}(V64,V63), P_s-{F}(V65,V49), P_s-{F}(V66,V65), P_s-{F}(V67,V49), P_s-{F}(V68,V67), P_s-{F}(V69,V49), P_s-{F}(V70,V69), P_s-{F}(V71,V49), P_s-{F}(V72,V71), P_s-{F}(V73,V74), V74 == V2, V74 == V10, V74 == V0, V56 == V74, P_s-{F}(V75,V74), P_s-{F}(V76,V74), P_s-{F}(V77,V74), P_s-{F}(V78,V74), P_s-{F}(V79,V74), P_s-{F}(V80,V74), P_s-{F}(V81,V74), P_s-{F}(V82,V74), P_s-{F}(V83,V74), P_s-{F}(V84,V74), P_s-{F}(V85,V74), P_s-{F}(V86,V85), P_s-{F}(V87,V74), P_s-{F}(V88,V87), P_s-{F}(V89,V90), P_s-{F}(V91,V90), P_s-{F}(V92,V90), P_s-{F}(V93,V90), P_s-{F}(V94,V90), P_s-{F}(V95,V90), P_s-{F}(V96,V90), P_s-{F}(V97,V90), P_s-{F}(V98,V90), P_s-{F}(V99,V90), P_s-{F}(V100,V101), V101 == V0, V101 == V10, P_s-{F}(V102,V101), P_s-{F}(V103,V102), P_s-{F}(V104,V105), V10 == V105, V0 == V105, P_s-{F}(V106,V105), P_s-{F}(V107,V106), P_s-{F}(V108,V109), V0 == V109, V7 == V109, P_s-{F}(V110,V111), V0 == V111, V39 == V111, P_s-{F}(V112,V113), V0 == V113, V31 == V113, #-{F} V114, V0 == V114, V5 == V114 | P_s-{T}(V90,V0), P_s-{T}(V90,V10), P_s-{T}(V90,V74), P_s-{T}(V90,V77), P_s-{T}(V90,V73), P_s-{T}(V90,V75), P_s-{T}(V90,V76), P_s-{T}(V90,V90), P_s-{T}(V90,V15), P_s-{T}(V90,V78), P_s-{T}(V90,V16), P_s-{T}(V90,V86), P_s-{T}(V90,V89), P_s-{T}(V90,V88), P_s-{T}(V90,V91), P_s-{T}(V90,V5), P_s-{T}(V90,V101), P_s-{T}(V90,V105), P_s-{T}(V90,V100), P_s-{T}(V90,V21), P_s-{T}(V90,V22), P_s-{T}(V90,V104), P_s-{T}(V90,V92), P_s-{T}(V90,V103), P_s-{T}(V90,V93), P_s-{T}(V90,V107), P_s-{T}(V90,V27), P_s-{T}(V90,V9), P_s-{T}(V90,V80), P_s-{T}(V90,V60), P_s-{T}(V90,V29), P_s-{T}(V90,V79), P_s-{T}(V90,V50), P_s-{T}(V90,V51), P_s-{T}(V90,V62), P_s-{T}(V90,V64), P_s-{T}(V90,V94), P_s-{T}(V90,V95), P_s-{T}(V90,V108), P_s-{T}(V90,V45), P_s-{T}(V90,V46), P_s-{T}(V90,V59), P_s-{T}(V90,V48), P_s-{T}(V90,V82), P_s-{T}(V90,V54), P_s-{T}(V90,V55), P_s-{T}(V90,V66), P_s-{T}(V90,V68), P_s-{T}(V90,V96), P_s-{T}(V90,V97), P_s-{T}(V90,V110), P_s-{T}(V90,V37), P_s-{T}(V90,V38), P_s-{T}(V90,V81), P_s-{T}(V90,V52), P_s-{T}(V90,V53), P_s-{T}(V90,V70), P_s-{T}(V90,V72), P_s-{T}(V90,V98), P_s-{T}(V90,V99), P_s-{T}(V90,V112), P_s-{T}(V90,V56), P_s-{T}(V90,V2), P_s-{T}(V90,V114), P_s-{T}(V90,V83), P_s-{T}(V90,V84), P_s-{T}(V90,V57)
% 29.24/29.44 (used 0 times, uses = {})
% 29.24/29.44
% 29.24/29.44 #2205: 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 == V46, V46 == V48, V48 == 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 == V81, V81 == V92, V92 == V93, V39 == V94, V95 == V147, V93 == V97, V94 == V98, V99 == V147, 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 == V127, V127 == V128, V128 == V129, V98 == V130, V131 == V147, V129 == V133, V130 == V134, V135 == V147, V133 == V150, V150 == 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; #2068 ), references = 1, size of lhs = 216:
% 29.24/29.44 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), b-{F}(V10,V13), b-{F}(V10,V14), P_s-{F}(V15,V10), P_s-{F}(V16,V10), b-{F}(V10,V17), b-{F}(V10,V18), b-{F}(V10,V19), b-{F}(V10,V20), P_s-{F}(V21,V10), P_s-{F}(V22,V10), b-{F}(V10,V23), b-{F}(V10,V24), b-{F}(V10,V25), b-{F}(V10,V26), P_s-{F}(V27,V10), b-{F}(V10,V28), P_s-{F}(V29,V10), b-{F}(V0,V30), b-{F}(V0,V31), b-{F}(V31,V0), b-{F}(V31,V32), b-{F}(V10,V33), b-{F}(V10,V34), b-{F}(V10,V35), b-{F}(V10,V36), P_s-{F}(V37,V10), P_s-{F}(V38,V31), b-{F}(V0,V39), b-{F}(V39,V0), b-{F}(V39,V40), b-{F}(V10,V41), b-{F}(V10,V42), b-{F}(V10,V43), b-{F}(V10,V44), P_s-{F}(V45,V10), P_s-{F}(V46,V39), b-{F}(V10,V47), P_s-{F}(V48,V10), P_s-{F}(V10,V49), V10 == V49, V0 == V49, b-{F}(V0,V50), V50 == V0, P_s-{F}(V51,V50), b-{F}(V50,V52), P_s-{F}(V53,V10), P_s-{F}(V54,V10), P_s-{F}(V55,V10), P_s-{F}(V56,V5), P_s-{F}(V57,V50), P_s-{F}(V58,V2), P_s-{F}(V59,V49), P_s-{F}(V60,V59), P_s-{F}(V61,V49), P_s-{F}(V62,V61), P_s-{F}(V63,V49), P_s-{F}(V64,V63), P_s-{F}(V65,V49), P_s-{F}(V66,V65), P_s-{F}(V67,V49), P_s-{F}(V68,V67), P_s-{F}(V69,V49), P_s-{F}(V70,V69), P_s-{F}(V71,V49), P_s-{F}(V72,V71), P_s-{F}(V73,V49), P_s-{F}(V74,V73), P_s-{F}(V75,V49), P_s-{F}(V76,V75), P_s-{F}(V77,V49), P_s-{F}(V78,V77), P_s-{F}(V79,V49), P_s-{F}(V80,V79), P_s-{F}(V81,V49), P_s-{F}(V82,V81), P_s-{F}(V83,V84), P_s-{F}(V84,V85), V85 == V2, V85 == V10, V85 == V0, V50 == V85, P_s-{F}(V86,V85), P_s-{F}(V87,V85), P_s-{F}(V88,V87), P_s-{F}(V89,V85), P_s-{F}(V90,V89), P_s-{F}(V91,V85), P_s-{F}(V92,V91), P_s-{F}(V93,V85), P_s-{F}(V94,V93), P_s-{F}(V95,V85), P_s-{F}(V96,V95), P_s-{F}(V97,V85), P_s-{F}(V98,V97), P_s-{F}(V99,V85), P_s-{F}(V100,V99), P_s-{F}(V101,V85), P_s-{F}(V102,V101), P_s-{F}(V103,V85), P_s-{F}(V104,V103), P_s-{F}(V105,V85), P_s-{F}(V106,V105), P_s-{F}(V107,V85), P_s-{F}(V108,V107), P_s-{F}(V109,V85), P_s-{F}(V110,V109), P_s-{F}(V111,V112), P_s-{F}(V112,V113), V113 == V0, V113 == V10, P_s-{F}(V114,V113), P_s-{F}(V115,V113), P_s-{F}(V116,V115), P_s-{F}(V117,V118), P_s-{F}(V118,V119), V10 == V119, V0 == V119, P_s-{F}(V120,V119), P_s-{F}(V121,V119), P_s-{F}(V122,V121), P_s-{F}(V123,V124), V55 == V124, V86 == V124, V94 == V124, V88 == V124, V90 == V124, V92 == V124, V123 == V124, V96 == V124, V56 == V124, V114 == V124, V120 == V124, V116 == V124, V122 == V124, V100 == V124, V98 == V124, V60 == V124, V62 == V124, V104 == V124, V68 == V124, V70 == V124, V102 == V124, V64 == V124, V66 == V124, V57 == V124, V58 == V124, V106 == V124, V108 == V124, P_s-{F}(V125,V124), P_s-{F}(V126,V125), V126 == V124, P_s-{F}(V127,V124), P_s-{F}(V128,V127), V128 == V124, P_s-{F}(V129,V124), P_s-{F}(V130,V129), V130 == V124, P_s-{F}(V131,V124), P_s-{F}(V132,V131), V132 == V124, P_s-{F}(V133,V124), P_s-{F}(V134,V133), V134 == V124, P_s-{F}(V135,V124), P_s-{F}(V136,V135), V136 == V124, P_s-{F}(V137,V124), P_s-{F}(V138,V137), V138 == V124, P_s-{F}(V139,V124), P_s-{F}(V140,V139), V140 == V124, P_s-{F}(V141,V124), P_s-{F}(V142,V141), V142 == V124, P_s-{F}(V143,V124), P_s-{F}(V144,V143), V144 == V124, P_s-{F}(V145,V146), V145 == V124, P_s-{F}(V146,V147), V0 == V147, V7 == V147, P_s-{F}(V148,V149), V148 == V124, P_s-{F}(V149,V150), V0 == V150, V39 == V150, P_s-{F}(V151,V152), V151 == V124, P_s-{F}(V152,V153), V0 == V153, V31 == V153, P_s-{F}(V154,V155), V0 == V155, V5 == V155, V154 == V124 | P_s-{T}(V124,V0), P_s-{T}(V124,V15), P_s-{T}(V124,V16), P_s-{T}(V124,V83), P_s-{T}(V124,V110), P_s-{T}(V124,V21), P_s-{T}(V124,V22), P_s-{T}(V124,V111), P_s-{T}(V124,V117), P_s-{T}(V124,V27), P_s-{T}(V124,V9), P_s-{T}(V124,V54), P_s-{T}(V124,V29), P_s-{T}(V124,V72), P_s-{T}(V124,V74), P_s-{T}(V124,V45), P_s-{T}(V124,V46), P_s-{T}(V124,V53), P_s-{T}(V124,V48), P_s-{T}(V124,V76), P_s-{T}(V124,V78), P_s-{T}(V124,V37), P_s-{T}(V124,V38), P_s-{T}(V124,V80), P_s-{T}(V124,V82), P_s-{T}(V124,V51)
% 29.24/29.44 (used 0 times, uses = {})
% 29.24/29.44
% 29.24/29.44 #2383: 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 == V45, V45 == V35, V35 == V46, V46 == V48, V48 == 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 == V81, V81 == V92, V92 == V93, V39 == V94, V95 == V143, V93 == V96, V94 == V97, V98 == V143, V96 == 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 == V125, V125 == V126, V126 == V127, V97 == V128, V129 == V143, V127 == V130, V128 == V131, V132 == V143, V130 == V144, V144 == V150, V150 == V152, V152 == V153, V153 == V154, V154 == V155, V155 == V156, V156 == V157, V157 == V158, V158 == V159, V159 == V160, V160 == V161, V161 == 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 == V185, V185 == V186, V186 == V187, V187 == V188, V188 == V190, V190 == V192, V192 == V193, V193 == V194, V194 == V44, V44 == V47, V47 == V219, V131 == V220, V143 == V221, V219 == V246, V220 == V245, V246 == V56, V56 == V57, V57 == V247, V245 == V248, V221 == V249, V247 == V253, V248 == V254, V249 == V255, V253 == V88, V88 == V89, V254 == V82, V89 == V149, V149 == V91, V91 == V208, V82 == V207, V208 == V210, V207 == V209, V210 == V139, V139 == V140, V209 == V133, V140 == V148, V148 == V142, V142 == V212, V133 == V211, V212 == V214, V211 == V213, V214 == V123, V123 == V124, V213 == V117, V124 == V216, V117 == V215, V216 == V218, V215 == V217; #2206 ), references = 2, size of lhs = 170:
% 29.24/29.44 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}(V8,V24), b-{F}(V8,V25), b-{F}(V8,V26), b-{F}(V8,V27), b-{F}(V8,V28), b-{F}(V8,V29), b-{F}(V8,V30), b-{F}(V8,V31), b-{F}(V8,V32), b-{F}(V8,V33), b-{F}(V0,V34), V34 == V0, P_s-{F}(V35,V34), b-{F}(V34,V36), P_s-{F}(V37,V8), P_s-{F}(V38,V5), P_s-{F}(V39,V34), P_s-{F}(V40,V2), P_s-{F}(V8,V41), V41 == V2, V34 == V41, V8 == 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,V45), P_s-{F}(V47,V41), P_s-{F}(V48,V47), P_s-{F}(V49,V41), P_s-{F}(V50,V49), 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), P_s-{F}(V63,V41), P_s-{F}(V64,V63), P_s-{F}(V65,V41), P_s-{F}(V66,V65), P_s-{F}(V67,V41), P_s-{F}(V68,V67), P_s-{F}(V69,V41), P_s-{F}(V70,V69), P_s-{F}(V71,V41), P_s-{F}(V72,V71), P_s-{F}(V73,V41), P_s-{F}(V74,V73), P_s-{F}(V75,V41), P_s-{F}(V76,V75), P_s-{F}(V77,V41), P_s-{F}(V78,V77), P_s-{F}(V79,V41), P_s-{F}(V80,V79), P_s-{F}(V81,V41), P_s-{F}(V82,V81), P_s-{F}(V83,V84), V37 == V84, V42 == V84, V64 == V84, V58 == V84, V60 == V84, V62 == V84, V83 == V84, V66 == V84, V38 == V84, V43 == V84, V44 == V84, V80 == V84, V82 == V84, V70 == V84, V68 == V84, V46 == V84, V48 == V84, V74 == V84, V54 == V84, V56 == V84, V72 == V84, V50 == V84, V52 == V84, V39 == V84, V40 == V84, V76 == V84, V78 == V84, P_s-{F}(V85,V84), P_s-{F}(V86,V85), V86 == V84, P_s-{F}(V87,V84), P_s-{F}(V88,V87), V88 == V84, P_s-{F}(V89,V84), P_s-{F}(V90,V89), V90 == V84, P_s-{F}(V91,V84), P_s-{F}(V92,V91), V92 == V84, P_s-{F}(V93,V84), P_s-{F}(V94,V93), V94 == V84, P_s-{F}(V95,V84), P_s-{F}(V96,V95), V96 == V84, P_s-{F}(V97,V84), P_s-{F}(V98,V97), V98 == V84, P_s-{F}(V99,V84), P_s-{F}(V100,V99), V100 == V84, P_s-{F}(V101,V84), P_s-{F}(V102,V101), V102 == V84, P_s-{F}(V103,V84), P_s-{F}(V104,V103), V104 == V84, P_s-{F}(V105,V106), V105 == V84, P_s-{F}(V106,V107), V0 == V107, V8 == V107, P_s-{F}(V108,V109), V108 == V84, P_s-{F}(V109,V110), V0 == V110, V8 == V110, P_s-{F}(V111,V112), V111 == V84, P_s-{F}(V112,V113), V0 == V113, V8 == V113, P_s-{F}(V114,V115), V0 == V115, V5 == V115, V114 == V84 | P_s-{T}(V84,V35)
% 29.24/29.44 (used 0 times, uses = {})
% 29.24/29.44
% 29.24/29.44 #2392: mergings( V2 == V10; #2390 ), references = 1, size of lhs = 61:
% 29.24/29.44 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-{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,V46), P_s-{T}(V1,V45), 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,V43), P_s-{T}(V1,V44), P_s-{T}(V1,V38), P_s-{T}(V1,V37), P_s-{T}(V1,V26), P_s-{T}(V1,V27), P_s-{T}(V1,V40), P_s-{T}(V1,V30), P_s-{T}(V1,V31), P_s-{T}(V1,V39), P_s-{T}(V1,V28), P_s-{T}(V1,V29), P_s-{T}(V1,V7), P_s-{T}(V1,V8), P_s-{T}(V1,V41), P_s-{T}(V1,V42), P_s-{T}(V1,V47), 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)
% 29.24/29.45 (used 0 times, uses = {})
% 29.24/29.45
% 29.24/29.45 #2453: mergings( V9 == 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 == V47, V47 == V46, V46 == V5, V5 == V36, V36 == V33, V33 == V34, V34 == V35, V35 == V37, V37 == V6, V6 == V44, V44 == V45, V45 == V39, V39 == V38, V38 == V27, V27 == V28, V28 == V41, V41 == V31, V31 == V32, V32 == V40, V40 == V29, V29 == V30, V30 == V7, V7 == V8, V8 == V42, V42 == V43, V43 == 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; #2393 ), references = 1, size of lhs = 3:
% 29.24/29.45 P_z-{F}(V0), P_s-{F}(V0,V1), V1 == V0 | P_s-{T}(V1,V1)
% 29.24/29.45 (used 0 times, uses = {})
% 29.24/29.45
% 29.24/29.45 #2457: mergings( V0 == V2; #2455 ), references = 1, size of lhs = 1:
% 29.24/29.45 P_z-{F}(V0) | P_s-{T}(V0,V0)
% 29.24/29.45 (used 0 times, uses = {})
% 29.24/29.45
% 29.24/29.45 #2460: exists( #8, #2458 ), references = 1, size of lhs = 0:
% 29.24/29.45 FALSE | FALSE
% 29.24/29.45 (used 0 times, uses = {})
% 29.24/29.45
% 29.24/29.45 number of learnt formulas = 56
% 29.24/29.45
% 29.24/29.45
% 29.24/29.45 % SZS output end Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 29.24/29.45
% 29.24/29.45 randbase = 1
%------------------------------------------------------------------------------