%------------------------------------------------------------------------------
% File : Geo-III---2018C
% Problem : GRA170-1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : geo -tptp_input -nonempty -inputfile %s
% Computer : n009.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue May 5 06:27:34 PM UTC 2026
% Result : Unsatisfiable 11.96s 12.13s
% Output : Refutation 11.96s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : GRA170-1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.12 % Command : geo -tptp_input -nonempty -inputfile %s
% 0.16/0.34 % Computer : n009.cluster.edu
% 0.16/0.34 % Model : x86_64 x86_64
% 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.34 % Memory : 8042.1875MB
% 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.34 % CPULimit : 300
% 0.16/0.34 % WCLimit : 300
% 0.16/0.34 % DateTime : Tue May 5 00:54:25 EDT 2026
% 0.16/0.34 % CPUTime :
% 11.96/12.13 GeoParameters:
% 11.96/12.13
% 11.96/12.13 tptp_input = 1
% 11.96/12.13 tptp_output = 0
% 11.96/12.13 nonempty = 1
% 11.96/12.13 inputfile = /export/starexec/sandbox/benchmark/theBenchmark.p
% 11.96/12.13 includepath = /export/starexec/sandbox/solver/bin/../../benchmark/
% 11.96/12.13
% 11.96/12.13
% 11.96/12.13 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 11.96/12.13 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 11.96/12.13
% 11.96/12.13 RuleSystem INPUT:
% 11.96/12.13
% 11.96/12.13 Initial Rules:
% 11.96/12.13 #0: input, references = 10, size of lhs = 2:
% 11.96/12.13 P_z-{F}(V0), P_s-{F}(V1,V0) | FALSE
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 #1: input, references = 10, size of lhs = 4:
% 11.96/12.13 P_z-{F}(V0), P_s-{F}(V1,V4), P_s-{F}(V2,V4), V1 == V2 | FALSE
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 #2: input, references = 3, size of lhs = 2:
% 11.96/12.13 P_z-{F}(V0), r-{F}(V1,V1) | FALSE
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 #3: input, references = 3, size of lhs = 2:
% 11.96/12.13 P_z-{F}(V0), b-{F}(V1,V1) | FALSE
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 #4: input, references = 35, size of lhs = 4:
% 11.96/12.13 P_z-{F}(V0), #-{F} V1, #-{F} V2, V1 == V2 | r-{T}(V1,V2), b-{T}(V1,V2)
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 #5: input, references = 27, size of lhs = 4:
% 11.96/12.13 P_z-{F}(V0), r-{F}(V1,V2), r-{F}(V3,V1), r-{F}(V3,V2) | FALSE
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 #6: input, references = 12, size of lhs = 7:
% 11.96/12.13 P_z-{F}(V0), b-{F}(V1,V2), b-{F}(V1,V3), b-{F}(V3,V2), b-{F}(V1,V4), b-{F}(V2,V5), b-{F}(V5,V4) | FALSE
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 #7: input, references = 16, size of lhs = 1:
% 11.96/12.13 #-{F} V0 | EXISTS V1: P_s-{T}(V0,V1)
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 #8: input, references = 4, size of lhs = 0:
% 11.96/12.13 FALSE | EXISTS V0: P_z-{T}(V0)
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 number of initial rules = 9
% 11.96/12.13
% 11.96/12.13 Simplifiers:
% 11.96/12.13 #9: unsound, references = 3, size of lhs = 3:
% 11.96/12.13 P_s-{F}(V0,V1), P_s-{F}(V0,V3), V1 == V3 | FALSE
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 #10: unsound, references = 3, size of lhs = 3:
% 11.96/12.13 P_z-{F}(V0), P_z-{F}(V1), V0 == V1 | FALSE
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 number of simplifiers = 2
% 11.96/12.13
% 11.96/12.13 Learnt:
% 11.96/12.13 #13: mergings( V0 == V3; #11 ), references = 23, size of lhs = 7:
% 11.96/12.13 P_z-{F}(V0), b-{F}(V1,V2), b-{F}(V1,V3), V3 == V2, b-{F}(V1,V4), b-{F}(V2,V5), b-{F}(V5,V4) | r-{T}(V3,V2)
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 #16: mergings( V0 == V3; #14 ), references = 11, size of lhs = 7:
% 11.96/12.13 P_z-{F}(V0), b-{F}(V1,V2), b-{F}(V1,V3), b-{F}(V3,V2), b-{F}(V1,V4), b-{F}(V5,V4), V2 == V5 | r-{T}(V2,V5)
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 #24: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6; #19 ), references = 15, size of lhs = 12:
% 11.96/12.13 P_z-{F}(V0), b-{F}(V1,V2), b-{F}(V1,V3), b-{F}(V2,V4), b-{F}(V4,V3), b-{F}(V1,V5), b-{F}(V5,V6), V1 == V6, V6 == V2, b-{F}(V7,V6), V6 == V7, r-{F}(V7,V2) | r-{T}(V1,V6)
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 #29: mergings( V0 == V3, V3 == V4; #26 ), references = 8, size of lhs = 9:
% 11.96/12.13 P_z-{F}(V0), b-{F}(V1,V2), b-{F}(V1,V3), b-{F}(V2,V4), b-{F}(V4,V3), r-{F}(V5,V2), r-{F}(V5,V6), V1 == V6, V6 == V2 | r-{T}(V1,V6)
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 #36: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6; #31 ), references = 9, size of lhs = 11:
% 11.96/12.13 P_z-{F}(V0), r-{F}(V1,V2), b-{F}(V2,V3), b-{F}(V3,V4), r-{F}(V1,V5), b-{F}(V5,V2), b-{F}(V5,V4), #-{F} V6, V1 == V6, V6 == V2, V5 == V6 | b-{T}(V1,V6)
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 #41: mergings( V0 == V3, V3 == V4; #38 ), references = 5, size of lhs = 9:
% 11.96/12.13 P_z-{F}(V0), b-{F}(V1,V2), b-{F}(V1,V3), V3 == V2, b-{F}(V1,V4), b-{F}(V5,V4), V2 == V5, r-{F}(V6,V3), r-{F}(V6,V2) | r-{T}(V2,V5)
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 #44: mergings( V0 == V3; #42 ), references = 15, size of lhs = 4:
% 11.96/12.13 P_z-{F}(V0), r-{F}(V1,V2), r-{F}(V3,V2), V3 == V1 | b-{T}(V3,V1)
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 #60: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10; #51 ), references = 1, size of lhs = 35:
% 11.96/12.13 P_z-{F}(V0), b-{F}(V1,V2), b-{F}(V3,V2), V2 == V3, r-{F}(V3,V4), V2 == V4, b-{F}(V4,V5), V5 == V1, V5 == V2, b-{F}(V5,V4), b-{F}(V5,V6), b-{F}(V6,V5), b-{F}(V1,V7), V5 == V7, V7 == V6, V2 == V7, b-{F}(V8,V7), V7 == V8, r-{F}(V8,V6), b-{F}(V9,V7), b-{F}(V9,V2), b-{F}(V9,V10), b-{F}(V11,V10), V7 == V11, b-{F}(V12,V7), b-{F}(V12,V2), b-{F}(V13,V2), b-{F}(V13,V7), b-{F}(V13,V14), r-{F}(V11,V15), V15 == V2, V7 == V15, r-{F}(V15,V16), V2 == V16, b-{F}(V16,V14) | r-{T}(V5,V1)
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 #77: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10; #68 ), references = 1, size of lhs = 28:
% 11.96/12.13 P_z-{F}(V0), b-{F}(V1,V2), b-{F}(V1,V3), V3 == V2, b-{F}(V1,V4), r-{F}(V5,V2), V3 == V5, r-{F}(V5,V6), V2 == V6, b-{F}(V6,V4), b-{F}(V6,V2), r-{F}(V6,V7), V2 == V7, b-{F}(V7,V8), V8 == V2, b-{F}(V8,V7), b-{F}(V9,V3), b-{F}(V9,V10), V10 == V3, V10 == V2, b-{F}(V11,V10), b-{F}(V11,V2), b-{F}(V11,V12), b-{F}(V6,V12), b-{F}(V9,V13), V5 == V13, V13 == V6, V2 == V13 | r-{T}(V8,V2)
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 #90: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8; #83 ), references = 3, size of lhs = 29:
% 11.96/12.13 P_z-{F}(V0), r-{F}(V1,V2), b-{F}(V2,V3), b-{F}(V3,V2), r-{F}(V1,V4), V4 == V2, r-{F}(V5,V4), b-{F}(V5,V6), b-{F}(V7,V6), b-{F}(V7,V8), V8 == V2, V8 == V4, V8 == V5, b-{F}(V7,V9), V8 == V9, V9 == V4, V9 == V2, b-{F}(V5,V9), b-{F}(V10,V9), V9 == V10, r-{F}(V10,V2), b-{F}(V2,V11), b-{F}(V11,V2), b-{F}(V12,V4), V12 == V9, r-{F}(V12,V8), b-{F}(V12,V13), b-{F}(V4,V14), b-{F}(V14,V13) | r-{T}(V8,V2)
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 #119: 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; #97 ), references = 2, size of lhs = 73:
% 11.96/12.13 P_z-{F}(V0), b-{F}(V1,V2), b-{F}(V1,V3), V3 == V2, b-{F}(V1,V4), b-{F}(V5,V3), b-{F}(V5,V6), V6 == V3, V6 == V2, b-{F}(V7,V6), b-{F}(V7,V2), b-{F}(V7,V8), b-{F}(V5,V9), V2 == V9, b-{F}(V10,V2), b-{F}(V10,V11), b-{F}(V12,V11), V2 == V12, r-{F}(V12,V13), V2 == V13, r-{F}(V14,V13), r-{F}(V14,V15), V13 == V15, V2 == V15, b-{F}(V15,V16), b-{F}(V16,V15), b-{F}(V10,V17), V2 == V17, V17 == V13, V17 == V15, b-{F}(V12,V17), b-{F}(V18,V17), V17 == V18, r-{F}(V18,V15), b-{F}(V15,V19), b-{F}(V19,V15), b-{F}(V20,V13), V20 == V2, V3 == V20, V20 == V9, V20 == V17, r-{F}(V20,V21), V2 == V21, V9 == V21, b-{F}(V21,V4), b-{F}(V21,V2), b-{F}(V21,V8), r-{F}(V21,V22), V2 == V22, b-{F}(V22,V23), V23 == V2, b-{F}(V23,V22), b-{F}(V20,V23), b-{F}(V20,V24), b-{F}(V13,V25), b-{F}(V25,V24), r-{F}(V26,V15), V2 == V26, b-{F}(V26,V27), b-{F}(V28,V27), b-{F}(V28,V2), b-{F}(V28,V29), V29 == V2, V29 == V23, V20 == V29, b-{F}(V26,V30), r-{F}(V20,V31), V31 == V29, b-{F}(V31,V2), b-{F}(V31,V30), b-{F}(V20,V32), b-{F}(V23,V33), b-{F}(V33,V32) | b-{T}(V20,V2)
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 #183: 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; #134 ), references = 1, size of lhs = 38:
% 11.96/12.13 P_z-{F}(V0), r-{F}(V1,V2), r-{F}(V2,V3), r-{F}(V3,V2), b-{F}(V1,V4), V4 == V2, r-{F}(V2,V4), r-{F}(V5,V4), r-{F}(V5,V6), V6 == V4, r-{F}(V6,V2), r-{F}(V2,V6), b-{F}(V6,V4), b-{F}(V6,V7), b-{F}(V6,V8), b-{F}(V6,V9), r-{F}(V10,V6), r-{F}(V10,V4), b-{F}(V1,V11), b-{F}(V6,V11), #-{F} V12, V12 == V6, V3 == V12, V12 == V2, V12 == V4, #-{F} V13, V13 == V3, V12 == V13, V4 == V13, V2 == V13, V13 == V6, #-{F} V14, V1 == V14, V12 == V14, V14 == V2, V13 == V14, V14 == V4, V6 == V14 | r-{T}(V4,V6)
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 #236: 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; #185 ), references = 2, size of lhs = 31:
% 11.96/12.13 P_z-{F}(V0), r-{F}(V1,V2), r-{F}(V1,V3), V3 == V2, r-{F}(V3,V4), V2 == V4, r-{F}(V4,V2), r-{F}(V4,V3), r-{F}(V4,V5), r-{F}(V5,V4), r-{F}(V6,V3), r-{F}(V6,V2), r-{F}(V7,V2), r-{F}(V7,V3), #-{F} V8, V8 == V3, V5 == V8, V8 == V4, V8 == V2, #-{F} V9, V9 == V5, V8 == V9, V2 == V9, V4 == V9, V9 == V3, #-{F} V10, V8 == V10, V10 == V4, V9 == V10, V10 == V2, V3 == V10 | r-{T}(V3,V2)
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 #290: 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 == V49, V49 == V50, V50 == V51, V51 == V52, V52 == V53; #238 ), references = 1, size of lhs = 27:
% 11.96/12.13 P_z-{F}(V0), r-{F}(V1,V2), r-{F}(V1,V3), V3 == V2, r-{F}(V3,V4), V2 == V4, r-{F}(V4,V2), r-{F}(V4,V3), r-{F}(V4,V5), r-{F}(V5,V4), r-{F}(V6,V3), r-{F}(V6,V2), r-{F}(V7,V2), r-{F}(V7,V3), r-{F}(V8,V3), r-{F}(V8,V2), #-{F} V9, #-{F} V10, V10 == V5, V2 == V10, V4 == V10, V10 == V3, #-{F} V11, V11 == V4, V10 == V11, V11 == V2, V3 == V11 | P_s-{T}(V9,V3), P_s-{T}(V9,V5), P_s-{T}(V9,V4), P_s-{T}(V9,V2), P_s-{T}(V9,V10), P_s-{T}(V9,V11)
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 #348: 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 == V47, V47 == V48, V48 == V49, V49 == V50, V50 == V51, V51 == V54, V54 == V56, V56 == V63, V63 == V65, V65 == V67; #291 ), references = 1, size of lhs = 29:
% 11.96/12.13 P_z-{F}(V0), r-{F}(V1,V0), r-{F}(V1,V2), V0 == V2, r-{F}(V0,V3), V2 == V3, r-{F}(V3,V2), r-{F}(V3,V0), r-{F}(V4,V0), r-{F}(V4,V2), r-{F}(V5,V2), r-{F}(V5,V0), r-{F}(V6,V0), r-{F}(V6,V2), P_s-{F}(V7,V3), P_s-{F}(V8,V2), P_s-{F}(V9,V10), V2 == V10, V3 == V10, V10 == V0, #-{F} V11, V7 == V11, V8 == V11, V9 == V11, #-{F} V12, V12 == V3, V10 == V12, V12 == V2, V0 == V12 | P_s-{T}(V11,V12)
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 #409: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10, V10 == V11, V11 == V12, V12 == V13, V13 == V14, V14 == V15, V15 == V16, V16 == V17, V17 == V18, V18 == V19, V19 == V20, V20 == V21, V21 == V22, V22 == V23, V23 == V24, V24 == V25, V25 == V26, V26 == V27, V27 == V28, V28 == V29, V29 == V30, V30 == V31, V31 == V32, V32 == V33, V33 == V34, V34 == V35, V35 == V36, V36 == V37, V37 == V38, V38 == V39, V39 == V40, V40 == V41, V41 == V42, V42 == V43, V43 == V44, V44 == V45, V45 == V46, V46 == V47, V47 == V48, V48 == V49, V49 == V50, V50 == V51, V51 == V52, V52 == V53, V53 == V54, V54 == V55, V55 == V56, V56 == V57, V57 == V59, V59 == V61, V61 == V62; #350 ), references = 7, size of lhs = 21:
% 11.96/12.13 P_z-{F}(V0), r-{F}(V0,V1), r-{F}(V1,V0), P_s-{F}(V2,V1), P_s-{F}(V3,V4), V0 == V4, V4 == V1, P_s-{F}(V5,V6), V4 == V6, V1 == V6, V6 == V0, P_s-{F}(V7,V8), V8 == V1, V6 == V8, V8 == V4, V0 == V8, #-{F} V9, V2 == V9, V3 == V9, V5 == V9, V7 == V9 | b-{T}(V1,V4)
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 #422: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8; #415 ), references = 5, size of lhs = 17:
% 11.96/12.13 P_z-{F}(V0), r-{F}(V1,V2), b-{F}(V1,V3), b-{F}(V4,V3), b-{F}(V4,V5), V5 == V2, V5 == V1, b-{F}(V4,V6), V6 == V5, b-{F}(V7,V5), b-{F}(V7,V8), V8 == V5, V6 == V8, b-{F}(V7,V9), b-{F}(V1,V9), b-{F}(V10,V8), b-{F}(V10,V6) | b-{T}(V5,V2)
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 #426: mergings( V2 == V3; #424 ), references = 1, size of lhs = 27:
% 11.96/12.13 P_z-{F}(V0), r-{F}(V1,V2), r-{F}(V1,V3), V3 == V2, r-{F}(V3,V4), V2 == V4, r-{F}(V4,V2), r-{F}(V4,V3), r-{F}(V4,V5), r-{F}(V5,V4), r-{F}(V6,V3), r-{F}(V6,V2), r-{F}(V7,V2), r-{F}(V7,V3), r-{F}(V3,V8), r-{F}(V8,V2), #-{F} V9, #-{F} V10, V10 == V5, V2 == V10, V4 == V10, V10 == V3, #-{F} V11, V11 == V4, V10 == V11, V11 == V2, V3 == V11 | P_s-{T}(V9,V3), P_s-{T}(V9,V5), P_s-{T}(V9,V4), P_s-{T}(V9,V2), P_s-{T}(V9,V10), P_s-{T}(V9,V11)
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 #434: mergings( V0 == V1, V1 == V13, V13 == V15, V15 == V17, V17 == V19, V19 == V21; #427 ), references = 1, size of lhs = 35:
% 11.96/12.13 P_z-{F}(V0), r-{F}(V1,V2), r-{F}(V1,V3), V3 == V2, r-{F}(V3,V4), V2 == V4, r-{F}(V4,V2), r-{F}(V4,V3), r-{F}(V4,V5), r-{F}(V5,V4), r-{F}(V6,V3), r-{F}(V6,V2), r-{F}(V7,V2), r-{F}(V7,V3), r-{F}(V3,V8), r-{F}(V8,V2), P_s-{F}(V9,V3), P_s-{F}(V10,V5), P_s-{F}(V11,V2), P_s-{F}(V12,V13), V13 == V5, V2 == V13, V4 == V13, V13 == V3, P_s-{F}(V14,V15), V15 == V4, V13 == V15, V15 == V2, V3 == V15, #-{F} V16, V9 == V16, V10 == V16, V11 == V16, V12 == V16, V14 == V16 | P_s-{T}(V16,V4)
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 #445: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V1; #436 ), references = 3, size of lhs = 26:
% 11.96/12.13 P_z-{F}(V0), r-{F}(V0,V1), r-{F}(V1,V0), r-{F}(V0,V2), r-{F}(V2,V0), P_s-{F}(V3,V2), P_s-{F}(V4,V1), P_s-{F}(V5,V6), V6 == V0, V2 == V6, P_s-{F}(V7,V8), V8 == V1, V6 == V8, V0 == V8, V8 == V2, P_s-{F}(V9,V10), V10 == V0, V8 == V10, V10 == V6, V2 == V10, #-{F} V11, V3 == V11, V4 == V11, V5 == V11, V7 == V11, V9 == V11 | b-{T}(V0,V6)
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 #550: 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 == V49, V49 == V50, V50 == V51, V51 == V52, V52 == V53, V53 == V54, V54 == V55, V55 == V57, V57 == V58, V58 == V60, V60 == V61, V61 == V62, V62 == V63, V63 == V65, V65 == 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 == V84, V84 == V89, V89 == V90, V90 == V91, V91 == V92; #466 ), references = 1, size of lhs = 42:
% 11.96/12.13 P_z-{F}(V0), r-{F}(V0,V1), r-{F}(V1,V0), P_s-{F}(V2,V1), P_s-{F}(V3,V1), P_s-{F}(V4,V1), r-{F}(V0,V5), r-{F}(V5,V0), r-{F}(V0,V6), r-{F}(V6,V0), P_s-{F}(V7,V6), P_s-{F}(V8,V5), P_s-{F}(V9,V10), V10 == V0, V6 == V10, V10 == V1, P_s-{F}(V11,V10), P_s-{F}(V12,V13), V10 == V13, V1 == V13, V13 == V0, P_s-{F}(V14,V15), V15 == V0, V15 == V1, V10 == V15, P_s-{F}(V16,V17), V15 == V17, V1 == V17, V17 == V0, P_s-{F}(V18,V19), V1 == V19, V19 == V0, P_s-{F}(V20,V21), V21 == V1, V19 == V21, V0 == V21, P_s-{F}(V22,V23), V23 == V5, V10 == V23, V0 == V23, V23 == V6, #-{F} V24 | P_s-{T}(V24,V1), P_s-{T}(V24,V13), P_s-{T}(V24,V10), P_s-{T}(V24,V0), P_s-{T}(V24,V17), P_s-{T}(V24,V15), P_s-{T}(V24,V19), P_s-{T}(V24,V21), P_s-{T}(V24,V23), P_s-{T}(V24,V6), P_s-{T}(V24,V2), P_s-{T}(V24,V9), P_s-{T}(V24,V12), P_s-{T}(V24,V24), P_s-{T}(V24,V3), P_s-{T}(V24,V14), P_s-{T}(V24,V16), P_s-{T}(V24,V4), P_s-{T}(V24,V18), P_s-{T}(V24,V20), P_s-{T}(V24,V7), P_s-{T}(V24,V8), P_s-{T}(V24,V11), P_s-{T}(V24,V22)
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 #633: 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 == V49, V49 == V50, V50 == V51, V51 == V52, V52 == V53, V53 == V54, V54 == V55, V55 == V57, V57 == V58, V58 == V60, V60 == V61, V61 == V62, V62 == V63, V63 == V65, V65 == 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 == V88, V88 == V89, V89 == V90, V90 == V91, V91 == V92; #467 ), references = 1, size of lhs = 42:
% 11.96/12.13 P_z-{F}(V0), r-{F}(V0,V1), r-{F}(V1,V0), P_s-{F}(V2,V1), P_s-{F}(V3,V1), P_s-{F}(V4,V1), r-{F}(V0,V5), r-{F}(V5,V0), r-{F}(V0,V6), r-{F}(V6,V0), P_s-{F}(V7,V6), P_s-{F}(V8,V5), P_s-{F}(V9,V10), V10 == V0, V6 == V10, V10 == V1, P_s-{F}(V11,V10), P_s-{F}(V12,V13), V10 == V13, V1 == V13, V13 == V0, P_s-{F}(V14,V15), V15 == V0, V15 == V1, V10 == V15, P_s-{F}(V16,V17), V15 == V17, V1 == V17, V17 == V0, P_s-{F}(V18,V19), V1 == V19, V19 == V0, P_s-{F}(V20,V21), V21 == V1, V19 == V21, V0 == V21, P_s-{F}(V22,V23), V23 == V5, V10 == V23, V0 == V23, V23 == V6, #-{F} V24 | P_s-{T}(V24,V1), P_s-{T}(V24,V13), P_s-{T}(V24,V10), P_s-{T}(V24,V0), P_s-{T}(V24,V17), P_s-{T}(V24,V15), P_s-{T}(V24,V19), P_s-{T}(V24,V21), P_s-{T}(V24,V23), P_s-{T}(V24,V6), P_s-{T}(V24,V2), P_s-{T}(V24,V9), P_s-{T}(V24,V12), P_s-{T}(V24,V24), P_s-{T}(V24,V3), P_s-{T}(V24,V14), P_s-{T}(V24,V16), P_s-{T}(V24,V4), P_s-{T}(V24,V18), P_s-{T}(V24,V20), P_s-{T}(V24,V7), P_s-{T}(V24,V8), P_s-{T}(V24,V11), P_s-{T}(V24,V22)
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 #741: 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 == V47, V47 == V48, V48 == V49, V49 == V50, V50 == V51, V51 == V52, V52 == V55, V55 == V53, V53 == V56, V56 == V58, V58 == V59, V59 == V60, V60 == V61, V61 == V63, V63 == 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 == V87, V87 == V88, V88 == V89, V89 == V90, V90 == V107, V107 == V109, V109 == V111, V111 == V113, V113 == V115, V115 == V117, V117 == V119, V119 == V121, V121 == V123, V123 == V57, V57 == V125, V125 == V127, V127 == V129, V129 == V62, V62 == V131, V131 == V133, V133 == V64, V64 == V135, V135 == V137, V137 == V85, V54 == V84, V85 == V86, V84 == V83, V86 == V139; #634 ), references = 1, size of lhs = 65:
% 11.96/12.13 P_z-{F}(V0), r-{F}(V0,V1), r-{F}(V1,V0), P_s-{F}(V0,V1), P_s-{F}(V2,V1), P_s-{F}(V3,V1), P_s-{F}(V4,V5), V0 == V5, V5 == V1, P_s-{F}(V6,V5), P_s-{F}(V7,V8), V1 == V8, V8 == V0, P_s-{F}(V9,V8), P_s-{F}(V10,V9), P_s-{F}(V11,V12), V12 == V0, V12 == V1, V12 == V8, V12 == V5, P_s-{F}(V13,V12), P_s-{F}(V14,V13), P_s-{F}(V15,V12), P_s-{F}(V16,V15), P_s-{F}(V17,V18), V1 == V18, V18 == V0, P_s-{F}(V19,V18), P_s-{F}(V20,V19), P_s-{F}(V21,V22), V22 == V0, V22 == V1, V12 == V22, V22 == V18, P_s-{F}(V23,V22), P_s-{F}(V24,V23), P_s-{F}(V25,V26), V1 == V26, V26 == V0, P_s-{F}(V27,V26), P_s-{F}(V28,V27), P_s-{F}(V29,V30), V30 == V1, V26 == V30, V0 == V30, P_s-{F}(V31,V30), P_s-{F}(V32,V31), P_s-{F}(V33,V34), V2 == V34, V7 == V34, V11 == V34, V17 == V34, V21 == V34, V25 == V34, V29 == V34, V6 == V34, V3 == V34, V14 == V34, V10 == V34, V33 == V34, V24 == V34, V20 == V34, V28 == V34, V32 == V34, V16 == V34 | P_s-{T}(V34,V4)
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 #846: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10, V10 == V11, V11 == V12, V12 == V13, V13 == V14, V14 == V15, V15 == V16, V16 == V17, V17 == V18, V18 == V19, V19 == V20, V20 == V21, V21 == V22, V22 == V23, V23 == V24, V24 == V25, V25 == V26, V26 == V27, V27 == V28, V28 == V29, V29 == V30, V30 == V31, V31 == V32, V32 == V33, V33 == V34, V34 == V35, V35 == V36, V36 == V37, V37 == V38, V38 == V39, V39 == V40, V40 == V41, V41 == V42, V42 == V43, V43 == V44, V44 == V45, V45 == V46, V46 == V47, V47 == V48, V48 == V49, V49 == V50, V50 == V51, V51 == V52, V52 == V53, V53 == V54, V54 == V55, V55 == V56, V56 == V57, V57 == V58, V58 == V59, V59 == V60, V60 == V61, V61 == V62, V62 == V63, V63 == V64, V64 == V65, V65 == V66, V66 == V67, V67 == V68, V68 == V69, V69 == V70, V70 == V71, V71 == V72, V72 == V73, V73 == V74, V74 == V75, V75 == V76, V76 == V1, V1 == V77, V77 == V78, V78 == V79, V79 == V80, V80 == V81, V81 == V83, V83 == V84, V84 == V85, V85 == V86, V86 == V87, V87 == V88, V88 == V89, V89 == V90, V90 == 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; #743 ), references = 1, size of lhs = 67:
% 11.96/12.13 P_z-{F}(V0), P_s-{F}(V0,V1), V0 == V1, r-{F}(V1,V0), P_s-{F}(V2,V1), P_s-{F}(V3,V1), P_s-{F}(V4,V5), V0 == V5, V5 == V1, P_s-{F}(V6,V5), P_s-{F}(V7,V6), P_s-{F}(V8,V9), V1 == V9, V9 == V0, P_s-{F}(V10,V9), P_s-{F}(V11,V10), P_s-{F}(V12,V13), V13 == V0, V13 == V1, V13 == V9, V13 == V5, P_s-{F}(V14,V13), P_s-{F}(V15,V14), P_s-{F}(V16,V13), P_s-{F}(V17,V16), P_s-{F}(V18,V19), V1 == V19, V19 == V0, P_s-{F}(V20,V19), P_s-{F}(V21,V20), P_s-{F}(V22,V23), V23 == V0, V23 == V1, V13 == V23, V23 == V19, P_s-{F}(V24,V23), P_s-{F}(V25,V24), P_s-{F}(V26,V27), V1 == V27, V27 == V0, P_s-{F}(V28,V27), P_s-{F}(V29,V28), P_s-{F}(V30,V31), V31 == V1, V27 == V31, V0 == V31, P_s-{F}(V32,V31), P_s-{F}(V33,V32), P_s-{F}(V34,V35), V2 == V35, V8 == V35, V12 == V35, V18 == V35, V22 == V35, V26 == V35, V30 == V35, V4 == V35, V3 == V35, V15 == V35, V11 == V35, V34 == V35, V25 == V35, V21 == V35, V29 == V35, V33 == V35, V17 == V35, V7 == V35 | b-{T}(V0,V1)
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 #849: mergings( V0 == V3; #847 ), references = 12, size of lhs = 4:
% 11.96/12.13 P_z-{F}(V0), r-{F}(V1,V2), r-{F}(V1,V3), V2 == V3 | b-{T}(V2,V3)
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 #857: mergings( V2 == V3, V3 == V4, V4 == V5; #853 ), references = 1, size of lhs = 33:
% 11.96/12.13 P_z-{F}(V0), r-{F}(V1,V2), b-{F}(V2,V3), b-{F}(V3,V4), r-{F}(V1,V5), b-{F}(V5,V2), b-{F}(V5,V4), r-{F}(V1,V6), r-{F}(V7,V6), r-{F}(V7,V8), V6 == V8, r-{F}(V1,V8), b-{F}(V8,V9), b-{F}(V9,V8), b-{F}(V1,V10), V10 == V8, V10 == V6, V10 == V1, b-{F}(V8,V11), b-{F}(V11,V8), b-{F}(V12,V6), r-{F}(V12,V10), b-{F}(V12,V13), b-{F}(V6,V14), b-{F}(V14,V13), r-{F}(V15,V8), V10 == V15, b-{F}(V16,V15), b-{F}(V16,V17), b-{F}(V17,V10), b-{F}(V16,V18), b-{F}(V18,V17), #-{F} V19 | P_s-{T}(V19,V2), P_s-{T}(V19,V5), P_s-{T}(V19,V10), P_s-{T}(V19,V6), P_s-{T}(V19,V8), P_s-{T}(V19,V1), P_s-{T}(V19,V12)
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 #868: mergings( V0 == V1, V1 == V2, V2 == V3, V3 == V5, V5 == V23, V23 == V25, V25 == V9, V9 == V27, V27 == V29; #858 ), references = 2, size of lhs = 40:
% 11.96/12.13 P_z-{F}(V0), b-{F}(V0,V1), b-{F}(V1,V2), r-{F}(V3,V0), r-{F}(V3,V4), V0 == V4, b-{F}(V4,V5), b-{F}(V5,V4), b-{F}(V4,V6), b-{F}(V6,V4), b-{F}(V7,V0), r-{F}(V7,V8), V8 == V4, V8 == V0, b-{F}(V7,V9), b-{F}(V0,V10), b-{F}(V10,V9), P_s-{F}(V11,V8), P_s-{F}(V12,V4), r-{F}(V13,V0), V8 == V13, r-{F}(V13,V4), b-{F}(V13,V8), r-{F}(V13,V14), b-{F}(V14,V0), b-{F}(V14,V2), P_s-{F}(V15,V14), P_s-{F}(V16,V13), r-{F}(V17,V4), V8 == V17, b-{F}(V18,V17), b-{F}(V18,V19), b-{F}(V19,V8), b-{F}(V18,V20), b-{F}(V20,V19), #-{F} V21, V15 == V21, V11 == V21, V12 == V21, V16 == V21 | P_s-{T}(V21,V7)
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 #884: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10, V10 == V11, V11 == V16, V16 == V18, V18 == V19; #871 ), references = 1, size of lhs = 42:
% 11.96/12.13 P_z-{F}(V0), b-{F}(V0,V1), b-{F}(V1,V0), r-{F}(V2,V0), r-{F}(V2,V3), V0 == V3, b-{F}(V3,V4), b-{F}(V4,V3), b-{F}(V3,V5), b-{F}(V5,V3), P_s-{F}(V6,V3), b-{F}(V1,V7), b-{F}(V7,V1), r-{F}(V8,V7), b-{F}(V8,V9), V1 == V9, V9 == V7, V9 == V3, V9 == V0, V9 == V8, P_s-{F}(V10,V9), P_s-{F}(V11,V1), P_s-{F}(V12,V1), b-{F}(V13,V1), b-{F}(V13,V14), V9 == V14, r-{F}(V14,V3), b-{F}(V13,V15), V1 == V15, b-{F}(V15,V9), r-{F}(V16,V0), V9 == V16, r-{F}(V16,V3), b-{F}(V16,V9), r-{F}(V16,V1), P_s-{F}(V17,V16), #-{F} V18, V12 == V18, V10 == V18, V6 == V18, V17 == V18, V11 == V18 | r-{T}(V1,V15)
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 #894: mergings( V2 == V3, V3 == V4, V4 == V5, V5 == V6; #889 ), references = 1, size of lhs = 37:
% 11.96/12.13 P_z-{F}(V0), b-{F}(V1,V2), b-{F}(V1,V3), b-{F}(V2,V4), b-{F}(V4,V3), b-{F}(V1,V5), r-{F}(V5,V2), r-{F}(V5,V6), b-{F}(V6,V7), b-{F}(V7,V8), r-{F}(V5,V9), b-{F}(V9,V6), b-{F}(V9,V8), r-{F}(V1,V10), V10 == V5, b-{F}(V5,V10), r-{F}(V5,V11), V10 == V11, r-{F}(V12,V11), r-{F}(V12,V13), V11 == V13, V10 == V13, r-{F}(V5,V13), b-{F}(V13,V14), b-{F}(V14,V13), b-{F}(V13,V15), b-{F}(V15,V13), b-{F}(V16,V11), r-{F}(V16,V10), b-{F}(V16,V17), b-{F}(V11,V18), b-{F}(V18,V17), b-{F}(V5,V19), b-{F}(V20,V19), V10 == V20, r-{F}(V20,V13), #-{F} V21 | P_s-{T}(V21,V6), P_s-{T}(V21,V9), P_s-{T}(V21,V1), P_s-{T}(V21,V2), P_s-{T}(V21,V10), P_s-{T}(V21,V11), P_s-{T}(V21,V13), P_s-{T}(V21,V5), P_s-{T}(V21,V16)
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 #905: mergings( V0 == V1, V1 == V2, V2 == V3, V3 == V4, V4 == V26, V26 == V28, V28 == V30, V30 == V32, V32 == V34; #895 ), references = 1, size of lhs = 47:
% 11.96/12.13 P_z-{F}(V0), b-{F}(V1,V2), b-{F}(V1,V3), b-{F}(V2,V4), b-{F}(V4,V3), b-{F}(V1,V5), r-{F}(V5,V2), r-{F}(V5,V6), b-{F}(V6,V7), b-{F}(V7,V8), r-{F}(V5,V9), b-{F}(V9,V6), b-{F}(V9,V8), r-{F}(V1,V10), V10 == V5, b-{F}(V5,V10), r-{F}(V5,V11), V10 == V11, r-{F}(V12,V11), r-{F}(V12,V13), V11 == V13, V10 == V13, r-{F}(V5,V13), b-{F}(V13,V14), b-{F}(V14,V13), b-{F}(V13,V15), b-{F}(V15,V13), b-{F}(V16,V11), r-{F}(V16,V10), b-{F}(V16,V17), b-{F}(V11,V18), b-{F}(V18,V17), b-{F}(V5,V19), b-{F}(V20,V19), V10 == V20, r-{F}(V20,V13), P_s-{F}(V21,V9), P_s-{F}(V22,V2), P_s-{F}(V23,V10), P_s-{F}(V24,V11), P_s-{F}(V25,V5), #-{F} V26, V21 == V26, V22 == V26, V23 == V26, V24 == V26, V25 == V26 | P_s-{T}(V26,V6), P_s-{T}(V26,V1), P_s-{T}(V26,V13), P_s-{T}(V26,V16)
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 #919: mergings( V0 == V1, V1 == V2, V2 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V15, V15 == V10, V10 == V22; #906 ), references = 1, size of lhs = 46:
% 11.96/12.13 P_z-{F}(V0), b-{F}(V0,V1), b-{F}(V1,V2), b-{F}(V0,V3), b-{F}(V0,V4), b-{F}(V3,V5), b-{F}(V5,V4), b-{F}(V0,V6), r-{F}(V6,V3), r-{F}(V6,V0), r-{F}(V6,V7), b-{F}(V7,V0), b-{F}(V7,V2), r-{F}(V0,V8), V8 == V6, V8 == V0, b-{F}(V6,V8), r-{F}(V6,V9), V8 == V9, V9 == V0, r-{F}(V10,V9), r-{F}(V10,V0), b-{F}(V0,V11), b-{F}(V11,V0), b-{F}(V0,V12), b-{F}(V12,V0), b-{F}(V13,V9), r-{F}(V13,V8), b-{F}(V13,V14), b-{F}(V9,V15), b-{F}(V15,V14), b-{F}(V6,V16), b-{F}(V17,V16), V8 == V17, r-{F}(V17,V0), P_s-{F}(V18,V7), P_s-{F}(V19,V3), P_s-{F}(V20,V8), P_s-{F}(V21,V9), P_s-{F}(V22,V6), #-{F} V23, V18 == V23, V19 == V23, V20 == V23, V21 == V23, V22 == V23 | P_s-{T}(V23,V13)
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 #942: 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; #925 ), references = 8, size of lhs = 22:
% 11.96/12.13 P_z-{F}(V0), b-{F}(V0,V1), b-{F}(V0,V2), b-{F}(V0,V3), b-{F}(V0,V4), r-{F}(V4,V0), P_s-{F}(V5,V4), P_s-{F}(V6,V7), V4 == V7, V7 == V0, P_s-{F}(V8,V7), P_s-{F}(V9,V7), P_s-{F}(V10,V11), V11 == V7, V11 == V0, V11 == V4, #-{F} V12, V8 == V12, V9 == V12, V10 == V12, V6 == V12, V5 == V12 | b-{T}(V4,V7)
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 #952: mergings( V0 == V3, V3 == V4, V4 == V5; #947 ), references = 6, size of lhs = 11:
% 11.96/12.13 P_z-{F}(V0), b-{F}(V1,V2), b-{F}(V2,V3), V1 == V3, b-{F}(V1,V4), b-{F}(V1,V5), V3 == V5, b-{F}(V5,V3), r-{F}(V5,V6), V3 == V6, b-{F}(V6,V4) | r-{T}(V1,V3)
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 #956: mergings( V0 == V3, V3 == V4, V4 == V5; #948 ), references = 1, size of lhs = 12:
% 11.96/12.13 P_z-{F}(V0), b-{F}(V1,V2), b-{F}(V2,V3), V1 == V3, b-{F}(V1,V4), b-{F}(V1,V5), b-{F}(V5,V3), b-{F}(V6,V3), V3 == V6, r-{F}(V6,V7), V3 == V7, b-{F}(V7,V4) | r-{T}(V1,V3)
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 #1099: 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 == V49, V49 == V50, V50 == V51, V51 == V52, V52 == V53, V53 == V54, V54 == V55, V55 == V56, V56 == V57, V57 == V58, V58 == V59, V59 == V60, V60 == V61, V61 == V62, V62 == V63, V63 == V64, V64 == V65, V65 == V66, V66 == V67, V67 == V68, V68 == V69, V69 == V70, V70 == V71, V71 == V72, V72 == V73, V73 == V74, V74 == V75, V75 == V76, V76 == V77, V77 == V78, V78 == V79, V79 == V80, V80 == V81, V81 == V82, V82 == V83, V83 == V84, V84 == V85, V85 == V86, V86 == V87, V87 == V88, V88 == V89, V89 == V90, V90 == 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, V120 == V121, V121 == V122, V122 == V124, V124 == V126, V126 == V127, V127 == V128, V128 == V129, V129 == V130, V130 == V131, V131 == V132, V132 == V133; #971 ), references = 1, size of lhs = 40:
% 11.96/12.13 P_z-{F}(V0), P_s-{F}(V0,V1), V0 == V1, r-{F}(V1,V0), P_s-{F}(V2,V1), P_s-{F}(V3,V1), P_s-{F}(V4,V1), P_s-{F}(V5,V1), P_s-{F}(V6,V7), V0 == V7, V7 == V1, P_s-{F}(V8,V7), P_s-{F}(V9,V8), P_s-{F}(V10,V11), V1 == V11, V11 == V0, P_s-{F}(V12,V11), P_s-{F}(V13,V12), P_s-{F}(V14,V15), P_s-{F}(V16,V15), P_s-{F}(V17,V15), P_s-{F}(V18,V15), P_s-{F}(V19,V20), V20 == V0, V20 == V1, P_s-{F}(V21,V20), P_s-{F}(V22,V21), P_s-{F}(V23,V24), V1 == V24, V24 == V0, P_s-{F}(V25,V24), P_s-{F}(V26,V25), P_s-{F}(V27,V28), V28 == V1, V28 == V0, P_s-{F}(V29,V28), P_s-{F}(V30,V28), P_s-{F}(V31,V32), V32 == V0, V32 == V1 | P_s-{T}(V15,V0), P_s-{T}(V15,V1), P_s-{T}(V15,V11), P_s-{T}(V15,V7), P_s-{T}(V15,V20), P_s-{T}(V15,V24), P_s-{T}(V15,V2), P_s-{T}(V15,V10), P_s-{T}(V15,V15), P_s-{T}(V15,V19), P_s-{T}(V15,V23), P_s-{T}(V15,V6), P_s-{T}(V15,V3), P_s-{T}(V15,V14), P_s-{T}(V15,V13), P_s-{T}(V15,V22), P_s-{T}(V15,V17), P_s-{T}(V15,V26), P_s-{T}(V15,V18), P_s-{T}(V15,V16), P_s-{T}(V15,V9), P_s-{T}(V15,V28), P_s-{T}(V15,V32), P_s-{T}(V15,V29), P_s-{T}(V15,V30), P_s-{T}(V15,V27), P_s-{T}(V15,V4), P_s-{T}(V15,V31), P_s-{T}(V15,V5)
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 #1226: 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 == V49, V49 == V50, V50 == V51, V51 == V52, V52 == V53, V53 == V54, V54 == V55, V55 == V56, V56 == V57, V57 == V58, V58 == V59, V59 == V60, V60 == V61, V61 == V62, V62 == V63, V63 == V64, V64 == V65, V65 == V66, V66 == V67, V67 == V68, V68 == V69, V69 == V70, V70 == V71, V71 == V72, V72 == V73, V73 == V74, V74 == V75, V75 == V76, V76 == V77, V77 == V78, V78 == V79, V79 == V80, V80 == V81, V81 == V82, V82 == V83, V83 == V84, V84 == V85, V85 == V86, V86 == V87, V87 == V88, V88 == V89, V89 == V90, V90 == 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, V120 == V121, V121 == V122, V122 == V124, V124 == V126, V126 == V127, V127 == V128, V128 == V129, V129 == V130, V130 == V131, V131 == V132, V132 == V133; #972 ), references = 1, size of lhs = 40:
% 11.96/12.13 P_z-{F}(V0), P_s-{F}(V0,V1), V0 == V1, r-{F}(V1,V0), P_s-{F}(V2,V1), P_s-{F}(V3,V1), P_s-{F}(V4,V1), P_s-{F}(V5,V1), P_s-{F}(V6,V7), V0 == V7, V7 == V1, P_s-{F}(V8,V7), P_s-{F}(V9,V8), P_s-{F}(V10,V11), V1 == V11, V11 == V0, P_s-{F}(V12,V11), P_s-{F}(V13,V12), P_s-{F}(V14,V15), P_s-{F}(V16,V15), P_s-{F}(V17,V15), P_s-{F}(V18,V15), P_s-{F}(V19,V20), V20 == V0, V20 == V1, P_s-{F}(V21,V20), P_s-{F}(V22,V21), P_s-{F}(V23,V24), V1 == V24, V24 == V0, P_s-{F}(V25,V24), P_s-{F}(V26,V25), P_s-{F}(V27,V28), V28 == V1, V28 == V0, P_s-{F}(V29,V28), P_s-{F}(V30,V28), P_s-{F}(V31,V32), V32 == V0, V32 == V1 | P_s-{T}(V15,V0), P_s-{T}(V15,V1), P_s-{T}(V15,V11), P_s-{T}(V15,V7), P_s-{T}(V15,V20), P_s-{T}(V15,V24), P_s-{T}(V15,V2), P_s-{T}(V15,V10), P_s-{T}(V15,V15), P_s-{T}(V15,V19), P_s-{T}(V15,V23), P_s-{T}(V15,V6), P_s-{T}(V15,V3), P_s-{T}(V15,V14), P_s-{T}(V15,V13), P_s-{T}(V15,V22), P_s-{T}(V15,V17), P_s-{T}(V15,V26), P_s-{T}(V15,V18), P_s-{T}(V15,V16), P_s-{T}(V15,V9), P_s-{T}(V15,V28), P_s-{T}(V15,V32), P_s-{T}(V15,V29), P_s-{T}(V15,V30), P_s-{T}(V15,V27), P_s-{T}(V15,V4), P_s-{T}(V15,V31), P_s-{T}(V15,V5)
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 #1374: 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 == V47, V47 == V48, V48 == V49, V49 == V50, V50 == V51, V51 == V52, V52 == V53, V53 == V54, V54 == V55, V55 == V56, V56 == V57, V57 == V58, V58 == V59, V59 == V60, V60 == V61, V61 == V62, V62 == V63, V63 == V64, V64 == V65, V65 == V66, V66 == V67, V67 == V68, V68 == V69, V69 == V70, V70 == V71, V71 == V72, V72 == V73, V73 == V74, V74 == V75, V75 == V76, V76 == V77, V77 == V78, V78 == V79, V79 == V80, V80 == V81, V81 == V82, V82 == V83, V83 == V84, V84 == V85, V85 == V86, V86 == V87, V87 == V88, V88 == 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, V120 == V122, V122 == V124, V124 == V125, V125 == V126, V126 == V127, V127 == V128, V128 == V129, V129 == V130, V130 == V131, V131 == V159, V159 == V161, V161 == V163, V163 == V165, V165 == V167, V167 == V169, V169 == V171, V171 == V173, V173 == V175, V175 == V177, V177 == V179, V179 == V181, V181 == V183, V183 == V185, V185 == V187, V187 == V189, V189 == V191, V191 == V193, V193 == V195, V195 == V197; #1227 ), references = 1, size of lhs = 80:
% 11.96/12.13 P_z-{F}(V0), P_s-{F}(V0,V1), V0 == V1, r-{F}(V1,V0), P_s-{F}(V2,V1), P_s-{F}(V3,V1), P_s-{F}(V4,V1), P_s-{F}(V5,V1), P_s-{F}(V6,V1), P_s-{F}(V7,V8), P_s-{F}(V8,V9), V0 == V9, V9 == V1, P_s-{F}(V10,V9), P_s-{F}(V11,V9), P_s-{F}(V12,V11), P_s-{F}(V13,V14), P_s-{F}(V14,V15), V1 == V15, V15 == V0, P_s-{F}(V16,V15), P_s-{F}(V17,V15), P_s-{F}(V18,V17), P_s-{F}(V19,V20), P_s-{F}(V20,V21), V21 == V0, V21 == V1, P_s-{F}(V22,V21), P_s-{F}(V23,V21), P_s-{F}(V24,V23), P_s-{F}(V25,V26), P_s-{F}(V26,V27), V1 == V27, V27 == V0, P_s-{F}(V28,V27), P_s-{F}(V29,V27), P_s-{F}(V30,V29), P_s-{F}(V31,V32), V6 == V32, V16 == V32, V10 == V32, V22 == V32, V28 == V32, V18 == V32, V31 == V32, V24 == V32, V30 == V32, V12 == V32, P_s-{F}(V33,V32), P_s-{F}(V34,V33), V34 == V32, P_s-{F}(V35,V32), P_s-{F}(V36,V35), V36 == V32, P_s-{F}(V37,V32), P_s-{F}(V38,V37), V38 == V32, P_s-{F}(V39,V32), P_s-{F}(V40,V39), V40 == V32, P_s-{F}(V41,V42), V42 == V1, V42 == V0, V41 == V32, P_s-{F}(V43,V42), P_s-{F}(V44,V43), V44 == V32, P_s-{F}(V45,V42), P_s-{F}(V46,V45), V46 == V32, P_s-{F}(V47,V42), P_s-{F}(V48,V47), V48 == V32, P_s-{F}(V49,V50), V50 == V0, V50 == V1, V49 == V32, P_s-{F}(V51,V50), P_s-{F}(V52,V51), V52 == V32 | P_s-{T}(V32,V0), P_s-{T}(V32,V2), P_s-{T}(V32,V3), P_s-{T}(V32,V13), P_s-{T}(V32,V19), P_s-{T}(V32,V25), P_s-{T}(V32,V7), P_s-{T}(V32,V4), P_s-{T}(V32,V5)
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 #1536: 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 == V47, V47 == V48, V48 == V49, V49 == V50, V50 == V51, V51 == V52, V52 == V53, V53 == V54, V54 == V55, V55 == V56, V56 == V57, V57 == V58, V58 == V59, V59 == V60, V60 == V61, V61 == V62, V62 == V63, V63 == V64, V64 == V65, V65 == V66, V66 == V67, V67 == V68, V68 == V69, V69 == V70, V70 == V71, V71 == V72, V72 == V73, V73 == V74, V74 == V75, V75 == V76, V76 == V77, V77 == V78, V78 == V79, V79 == V80, V80 == V81, V81 == V82, V82 == V83, V83 == V84, V84 == V85, V85 == V86, V86 == V87, V87 == V88, V88 == 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, V120 == V122, V122 == V124, V124 == V125, V125 == V126, V126 == V127, V127 == V128, V128 == V129, V129 == V130, V130 == V131, V131 == V132, V132 == V134, V134 == V135, V135 == V136, V136 == V137, V137 == V138, V138 == V139, V139 == V140, V140 == V141, V141 == V142, V142 == V143, V143 == V144, V144 == V145, V145 == V146, V146 == V147, V147 == V148, V148 == V149, V149 == V150, V150 == V151, V151 == V152, V152 == V90, V90 == V91, V91 == V159, V89 == V160, V159 == V165, V160 == V166, V161 == V167, V165 == V171, V166 == V172, V167 == V173, V171 == V153, V172 == V154, V173 == V155, V153 == V121; #1375 ), references = 1, size of lhs = 64:
% 11.96/12.13 P_z-{F}(V0), P_s-{F}(V0,V1), V0 == V1, r-{F}(V1,V0), P_s-{F}(V2,V1), P_s-{F}(V3,V1), P_s-{F}(V1,V4), V0 == V4, V4 == V1, P_s-{F}(V5,V4), P_s-{F}(V6,V4), P_s-{F}(V7,V4), P_s-{F}(V8,V4), P_s-{F}(V9,V4), P_s-{F}(V10,V9), P_s-{F}(V11,V4), P_s-{F}(V12,V11), P_s-{F}(V13,V4), P_s-{F}(V14,V13), P_s-{F}(V15,V4), P_s-{F}(V16,V15), P_s-{F}(V17,V18), V3 == V18, V5 == V18, V8 == V18, V6 == V18, V7 == V18, V12 == V18, V17 == V18, V14 == V18, V16 == V18, V10 == V18, P_s-{F}(V19,V18), P_s-{F}(V20,V19), V20 == V18, P_s-{F}(V21,V18), P_s-{F}(V22,V21), V22 == V18, P_s-{F}(V23,V18), P_s-{F}(V24,V23), V24 == V18, P_s-{F}(V25,V18), P_s-{F}(V26,V25), V26 == V18, P_s-{F}(V27,V28), V28 == V1, V28 == V0, V27 == V18, P_s-{F}(V29,V28), P_s-{F}(V30,V29), V30 == V18, P_s-{F}(V31,V28), P_s-{F}(V32,V31), V32 == V18, P_s-{F}(V33,V28), P_s-{F}(V34,V33), V34 == V18, P_s-{F}(V35,V36), V36 == V0, V36 == V1, V35 == V18, P_s-{F}(V37,V36), P_s-{F}(V38,V37), V38 == V18 | P_s-{T}(V18,V2)
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 #1701: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10, V10 == V11, V11 == V12, V12 == V13, V13 == V14, V14 == V15, V15 == V16, V16 == V17, V17 == V18, V18 == V19, V19 == V20, V20 == V21, V21 == V22, V22 == V23, V23 == V24, V24 == V25, V25 == V26, V26 == V27, V27 == V28, V28 == V29, V29 == V30, V30 == V31, V31 == V32, V32 == V33, V33 == V34, V34 == V35, V35 == V36, V36 == V37, V37 == V38, V38 == V39, V39 == V40, V40 == V41, V41 == V42, V42 == V43, V43 == V44, V44 == V45, V45 == V46, V46 == V47, V47 == V48, V48 == V49, V49 == V50, V50 == V51, V51 == V52, V52 == V53, V53 == V54, V54 == V55, V55 == V56, V56 == V57, V57 == V58, V58 == V59, V59 == V60, V60 == V61, V61 == V62, V62 == V63, V63 == V64, V64 == V65, V65 == V66, V66 == V67, V67 == V68, V68 == V69, V69 == V70, V70 == V71, V71 == V72, V72 == V73, V73 == V74, V74 == V75, V75 == V76, V76 == V77, V77 == V78, V78 == 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, 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, V120 == V2, V2 == V121, V121 == V122, V122 == V123, V123 == V124, V124 == V125, V125 == V126, V126 == V127, V127 == V128, V128 == V129, V129 == 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 == V146, V146 == V147, V147 == V148, V148 == V149, V149 == V150, V150 == V151, V151 == V152, V1 == V153, V152 == V156, V153 == V157, V154 == V158, V156 == V160, V157 == V161, V158 == V162, V160 == V164, V161 == V165, V162 == V166, V164 == V168, V168 == V169; #1538 ), references = 2, size of lhs = 62:
% 11.96/12.13 P_z-{F}(V0), P_s-{F}(V0,V1), V0 == V1, P_s-{F}(V2,V1), P_s-{F}(V1,V3), V0 == V3, V3 == V1, P_s-{F}(V4,V3), P_s-{F}(V5,V3), P_s-{F}(V6,V3), P_s-{F}(V7,V3), P_s-{F}(V8,V3), P_s-{F}(V9,V8), P_s-{F}(V10,V3), P_s-{F}(V11,V10), P_s-{F}(V12,V3), P_s-{F}(V13,V12), P_s-{F}(V14,V3), P_s-{F}(V15,V14), P_s-{F}(V16,V17), V2 == V17, V4 == V17, V7 == V17, V5 == V17, V6 == V17, V11 == V17, V16 == V17, V13 == V17, V15 == V17, V9 == V17, P_s-{F}(V18,V17), P_s-{F}(V19,V18), V19 == V17, P_s-{F}(V20,V17), P_s-{F}(V21,V20), V21 == V17, P_s-{F}(V22,V17), P_s-{F}(V23,V22), V23 == V17, P_s-{F}(V24,V17), P_s-{F}(V25,V24), V25 == V17, P_s-{F}(V26,V27), V27 == V1, V27 == V0, V26 == V17, P_s-{F}(V28,V27), P_s-{F}(V29,V28), V29 == V17, P_s-{F}(V30,V27), P_s-{F}(V31,V30), V31 == V17, P_s-{F}(V32,V27), P_s-{F}(V33,V32), V33 == V17, P_s-{F}(V34,V35), V35 == V0, V35 == V1, V34 == V17, P_s-{F}(V36,V35), P_s-{F}(V37,V36), V37 == V17 | b-{T}(V1,V0)
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 #1720: mergings( V0 == V7, V7 == V2, V2 == V12, V12 == V13, V13 == V14; #1713 ), references = 1, size of lhs = 47:
% 11.96/12.13 P_z-{F}(V0), b-{F}(V0,V1), b-{F}(V0,V2), b-{F}(V0,V3), b-{F}(V0,V4), V4 == V0, P_s-{F}(V5,V4), b-{F}(V0,V6), b-{F}(V0,V7), b-{F}(V0,V8), P_s-{F}(V9,V4), b-{F}(V10,V4), b-{F}(V10,V11), b-{F}(V0,V11), r-{F}(V10,V12), V4 == V12, V12 == V0, P_s-{F}(V13,V12), P_s-{F}(V14,V12), P_s-{F}(V15,V12), P_s-{F}(V16,V17), V10 == V17, V17 == V4, V17 == V0, V17 == V12, P_s-{F}(V18,V17), P_s-{F}(V19,V17), P_s-{F}(V20,V21), V21 == V17, V21 == V0, V21 == V4, P_s-{F}(V22,V23), V23 == V12, V23 == V0, V23 == V4, #-{F} V24, V18 == V24, V19 == V24, V20 == V24, V16 == V24, V5 == V24, #-{F} V25, V14 == V25, V15 == V25, V22 == V25, V13 == V25, V9 == V25 | b-{T}(V4,V0)
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 #1727: mergings( V0 == V7, V7 == V2, V2 == V12, V12 == V13, V13 == V14, V14 == V15; #1714 ), references = 1, size of lhs = 51:
% 11.96/12.13 P_z-{F}(V0), b-{F}(V0,V1), b-{F}(V0,V2), b-{F}(V0,V3), b-{F}(V0,V4), V4 == V0, P_s-{F}(V5,V4), b-{F}(V0,V6), b-{F}(V0,V7), b-{F}(V0,V8), P_s-{F}(V9,V4), b-{F}(V10,V4), b-{F}(V10,V11), b-{F}(V0,V11), r-{F}(V10,V12), V4 == V12, V12 == V0, P_s-{F}(V13,V12), P_s-{F}(V14,V12), P_s-{F}(V15,V12), b-{F}(V12,V16), r-{F}(V16,V12), b-{F}(V16,V4), P_s-{F}(V17,V18), V10 == V18, V18 == V4, V18 == V0, V18 == V12, V18 == V16, P_s-{F}(V19,V18), P_s-{F}(V20,V18), P_s-{F}(V21,V22), V22 == V18, V22 == V0, V22 == V4, P_s-{F}(V23,V24), V24 == V12, V24 == V0, V24 == V4, #-{F} V25, V19 == V25, V20 == V25, V21 == V25, V17 == V25, V5 == V25, #-{F} V26, V14 == V26, V15 == V26, V23 == V26, V13 == V26, V9 == V26 | b-{T}(V4,V0)
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 #1730: mergings( V0 == V3; #1728 ), references = 1, size of lhs = 5:
% 11.96/12.13 P_z-{F}(V0), b-{F}(V1,V2), b-{F}(V2,V3), V3 == V1, b-{F}(V3,V2) | r-{T}(V3,V1)
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 #1739: mergings( V0 == V1, V1 == V5, V5 == V6, V6 == V7; #1734 ), references = 1, size of lhs = 33:
% 11.96/12.13 P_z-{F}(V0), b-{F}(V0,V1), b-{F}(V1,V0), r-{F}(V2,V1), b-{F}(V2,V0), b-{F}(V2,V3), r-{F}(V0,V4), b-{F}(V4,V3), r-{F}(V5,V0), V0 == V5, P_s-{F}(V6,V5), P_s-{F}(V7,V5), P_s-{F}(V8,V9), V5 == V9, V9 == V1, V2 == V9, V9 == V0, V9 == V4, P_s-{F}(V10,V11), V9 == V11, V0 == V11, V11 == V5, P_s-{F}(V12,V13), V13 == V0, V11 == V13, V13 == V9, V5 == V13, #-{F} V14, V6 == V14, V7 == V14, V8 == V14, V10 == V14, V12 == V14 | b-{T}(V0,V5)
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 #1754: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V8, V8 == V9, V9 == V10, V10 == V15, V15 == V16, V16 == V17; #1744 ), references = 1, size of lhs = 44:
% 11.96/12.13 P_z-{F}(V0), b-{F}(V0,V1), b-{F}(V1,V2), b-{F}(V3,V2), b-{F}(V3,V0), b-{F}(V0,V4), b-{F}(V4,V0), r-{F}(V5,V4), b-{F}(V5,V0), b-{F}(V5,V6), r-{F}(V0,V7), b-{F}(V7,V6), b-{F}(V0,V8), b-{F}(V8,V0), b-{F}(V3,V9), b-{F}(V10,V9), r-{F}(V10,V8), P_s-{F}(V11,V12), V3 == V12, V0 == V12, V12 == V8, V12 == V10, P_s-{F}(V13,V12), P_s-{F}(V14,V15), V12 == V15, V15 == V4, V5 == V15, V15 == V0, V15 == V7, P_s-{F}(V16,V17), V15 == V17, V0 == V17, V17 == V12, P_s-{F}(V18,V19), V19 == V0, V17 == V19, V19 == V15, V12 == V19, #-{F} V20, V11 == V20, V13 == V20, V14 == V20, V16 == V20, V18 == V20 | r-{T}(V3,V12)
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 #1776: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10, V10 == V1, V1 == V17, V17 == V18, V18 == V19, V19 == V23, V23 == V24, V24 == V25, V25 == V28, V28 == V29; #1758 ), references = 1, size of lhs = 74:
% 11.96/12.13 P_z-{F}(V0), r-{F}(V0,V1), V1 == V0, P_s-{F}(V2,V1), P_s-{F}(V3,V1), P_s-{F}(V4,V1), b-{F}(V5,V0), r-{F}(V5,V6), V6 == V0, V6 == V1, P_s-{F}(V7,V6), P_s-{F}(V8,V6), b-{F}(V5,V9), r-{F}(V0,V10), b-{F}(V10,V9), r-{F}(V11,V6), b-{F}(V11,V12), r-{F}(V0,V13), b-{F}(V13,V0), b-{F}(V13,V12), r-{F}(V13,V6), P_s-{F}(V14,V15), V15 == V6, V15 == V0, V15 == V1, P_s-{F}(V16,V15), P_s-{F}(V17,V15), P_s-{F}(V18,V19), V19 == V15, V19 == V0, V19 == V6, P_s-{F}(V20,V21), V21 == V1, V21 == V0, V21 == V6, P_s-{F}(V22,V23), V13 == V23, V23 == V11, V0 == V23, V23 == V6, P_s-{F}(V24,V23), P_s-{F}(V25,V26), V23 == V26, V26 == V6, V5 == V26, V26 == V0, V26 == V10, P_s-{F}(V27,V28), V26 == V28, V0 == V28, V28 == V23, P_s-{F}(V29,V30), V30 == V0, V28 == V30, V30 == V26, V23 == V30, #-{F} V31, V16 == V31, V17 == V31, V18 == V31, V14 == V31, V7 == V31, #-{F} V32, V3 == V32, V4 == V32, V20 == V32, V2 == V32, V8 == V32, #-{F} V33, V22 == V33, V24 == V33, V25 == V33, V27 == V33, V29 == V33 | r-{T}(V0,V6)
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 #1797: mergings( V2 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10, V10 == V11, V11 == V16, V16 == V17, V17 == V18, V18 == V25, V25 == V26, V26 == V27, V27 == V30, V30 == V31, V31 == V33; #1778 ), references = 1, size of lhs = 40:
% 11.96/12.13 P_z-{F}(V0), r-{F}(V0,V1), V1 == V0, P_s-{F}(V2,V1), P_s-{F}(V3,V1), P_s-{F}(V4,V1), b-{F}(V5,V0), r-{F}(V5,V6), V6 == V0, V6 == V1, P_s-{F}(V7,V6), P_s-{F}(V8,V6), b-{F}(V5,V9), r-{F}(V0,V10), b-{F}(V10,V9), r-{F}(V11,V6), b-{F}(V11,V12), r-{F}(V0,V13), b-{F}(V13,V0), b-{F}(V13,V12), r-{F}(V13,V6), r-{F}(V0,V14), r-{F}(V14,V6), P_s-{F}(V15,V16), V16 == V0, V16 == V6, P_s-{F}(V17,V18), V13 == V18, V18 == V11, V0 == V18, V18 == V6, P_s-{F}(V19,V18), P_s-{F}(V20,V21), V0 == V21, V21 == V18, P_s-{F}(V22,V23), V23 == V0, V21 == V23, V18 == V23, #-{F} V24 | P_s-{T}(V24,V6), P_s-{T}(V24,V0), P_s-{T}(V24,V1), P_s-{T}(V24,V16), P_s-{T}(V24,V18), P_s-{T}(V24,V5), P_s-{T}(V24,V10), P_s-{T}(V24,V21), P_s-{T}(V24,V23), P_s-{T}(V24,V24), P_s-{T}(V24,V15), P_s-{T}(V24,V7), P_s-{T}(V24,V3), P_s-{T}(V24,V4), P_s-{T}(V24,V2), P_s-{T}(V24,V8), P_s-{T}(V24,V17), P_s-{T}(V24,V19), P_s-{T}(V24,V20), P_s-{T}(V24,V22)
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 #1832: mergings( V0 == V1, V1 == V2, V2 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V14, V14 == V15, V15 == V16, V16 == V23, V23 == V24, V24 == V25, V25 == V28, V28 == V29, V29 == V31, V31 == V43, V43 == V45, V45 == V47, V47 == V49, V49 == V51, V51 == V53, V53 == V55, V55 == V57, V57 == V59, V59 == V61, V61 == V63, V63 == V65, V65 == V67, V67 == V69, V69 == V71; #1798 ), references = 1, size of lhs = 69:
% 11.96/12.13 P_z-{F}(V0), r-{F}(V0,V1), V1 == V0, P_s-{F}(V2,V1), P_s-{F}(V3,V1), P_s-{F}(V4,V1), r-{F}(V0,V5), b-{F}(V5,V6), r-{F}(V0,V7), b-{F}(V7,V0), b-{F}(V7,V8), b-{F}(V9,V8), r-{F}(V9,V10), V10 == V0, V10 == V1, r-{F}(V7,V10), r-{F}(V0,V11), r-{F}(V11,V10), P_s-{F}(V12,V10), P_s-{F}(V13,V1), P_s-{F}(V14,V5), b-{F}(V15,V0), r-{F}(V15,V10), b-{F}(V15,V6), P_s-{F}(V16,V15), P_s-{F}(V17,V10), P_s-{F}(V18,V17), P_s-{F}(V19,V10), P_s-{F}(V20,V19), P_s-{F}(V21,V22), V22 == V0, P_s-{F}(V23,V22), P_s-{F}(V24,V25), V25 == V0, V25 == V10, P_s-{F}(V26,V25), P_s-{F}(V27,V26), P_s-{F}(V28,V29), V7 == V29, V29 == V9, V0 == V29, V29 == V10, V29 == V22, P_s-{F}(V30,V29), P_s-{F}(V31,V30), P_s-{F}(V32,V29), P_s-{F}(V33,V32), P_s-{F}(V34,V35), V0 == V35, V35 == V29, V35 == V22, P_s-{F}(V36,V35), P_s-{F}(V37,V36), P_s-{F}(V38,V39), V12 == V39, V13 == V39, V24 == V39, V28 == V39, V16 == V39, V14 == V39, V34 == V39, V23 == V39, V38 == V39, V27 == V39, V18 == V39, V20 == V39, V31 == V39, V33 == V39, V37 == V39 | P_s-{T}(V39,V0), P_s-{T}(V39,V3), P_s-{T}(V39,V4), P_s-{T}(V39,V2), P_s-{T}(V39,V21)
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 #1870: mergings( V0 == V1, V1 == V2, V2 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V14, V14 == V15, V15 == V16, V16 == V19, V19 == V20, V20 == V21, V21 == V22, V22 == V23, V23 == V28, V28 == V30, V30 == V32, V32 == V34, V34 == V35, V35 == V36, V36 == V37, V37 == V39, V39 == V40, V40 == V41, V41 == V42, V42 == V43, V43 == V44, V44 == V45, V45 == V46, V46 == V47, V47 == V9, V9 == V12, V12 == V13, V13 == V11; #1833 ), references = 1, size of lhs = 67:
% 11.96/12.13 P_z-{F}(V0), r-{F}(V0,V1), V1 == V0, P_s-{F}(V0,V1), r-{F}(V0,V2), b-{F}(V2,V3), r-{F}(V0,V4), b-{F}(V4,V0), b-{F}(V4,V5), b-{F}(V6,V5), r-{F}(V6,V7), V7 == V0, V7 == V1, r-{F}(V4,V7), r-{F}(V0,V8), r-{F}(V8,V7), P_s-{F}(V9,V7), P_s-{F}(V10,V1), P_s-{F}(V11,V2), b-{F}(V12,V0), r-{F}(V12,V7), b-{F}(V12,V3), P_s-{F}(V13,V12), P_s-{F}(V14,V7), P_s-{F}(V15,V14), P_s-{F}(V16,V7), P_s-{F}(V17,V16), P_s-{F}(V18,V19), V19 == V0, P_s-{F}(V20,V19), P_s-{F}(V21,V22), V22 == V0, V22 == V7, P_s-{F}(V23,V22), P_s-{F}(V24,V23), P_s-{F}(V25,V26), V4 == V26, V26 == V6, V0 == V26, V26 == V7, V26 == V19, P_s-{F}(V27,V26), P_s-{F}(V28,V27), P_s-{F}(V29,V26), P_s-{F}(V30,V29), P_s-{F}(V31,V32), V0 == V32, V32 == V26, V32 == V19, P_s-{F}(V33,V32), P_s-{F}(V34,V33), P_s-{F}(V35,V36), V9 == V36, V10 == V36, V21 == V36, V25 == V36, V13 == V36, V11 == V36, V31 == V36, V20 == V36, V35 == V36, V24 == V36, V15 == V36, V17 == V36, V28 == V36, V30 == V36, V34 == V36 | P_s-{T}(V36,V18)
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 #1912: 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 == V44, V44 == V45, V45 == V46, V46 == V47, V37 == V48; #1872 ), references = 2, size of lhs = 58:
% 11.96/12.13 P_z-{F}(V0), r-{F}(V0,V1), V1 == V0, P_s-{F}(V0,V1), r-{F}(V0,V2), b-{F}(V2,V3), r-{F}(V0,V4), b-{F}(V4,V0), b-{F}(V4,V3), b-{F}(V4,V5), P_s-{F}(V6,V1), P_s-{F}(V7,V2), P_s-{F}(V8,V1), P_s-{F}(V9,V4), P_s-{F}(V10,V11), V4 == V11, V11 == V0, V11 == V1, P_s-{F}(V12,V11), P_s-{F}(V13,V12), P_s-{F}(V14,V11), P_s-{F}(V15,V14), P_s-{F}(V16,V17), V17 == V0, V17 == V11, P_s-{F}(V18,V17), P_s-{F}(V19,V18), P_s-{F}(V20,V21), V21 == V4, V0 == V21, V21 == V11, V21 == V1, 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), V0 == V27, V27 == V21, V27 == V1, P_s-{F}(V28,V27), P_s-{F}(V29,V28), P_s-{F}(V30,V31), V10 == V31, V6 == V31, V16 == V31, V20 == V31, V9 == V31, V7 == V31, V26 == V31, V8 == V31, V30 == V31, V19 == V31, V13 == V31, V15 == V31, V23 == V31, V25 == V31, V29 == V31 | b-{T}(V4,V11)
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 #1922: mergings( V0 == V3, V3 == V4, V4 == V5; #1917 ), references = 2, size of lhs = 10:
% 11.96/12.13 P_z-{F}(V0), b-{F}(V1,V2), b-{F}(V1,V3), V2 == V3, b-{F}(V1,V4), b-{F}(V5,V2), b-{F}(V5,V3), r-{F}(V3,V6), V2 == V6, b-{F}(V6,V4) | r-{T}(V3,V2)
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 #1926: mergings( V0 == V3, V3 == V4, V4 == V5; #1918 ), references = 1, size of lhs = 10:
% 11.96/12.13 P_z-{F}(V0), b-{F}(V1,V2), b-{F}(V1,V3), V2 == V3, b-{F}(V1,V4), b-{F}(V5,V3), b-{F}(V5,V2), r-{F}(V3,V6), V2 == V6, b-{F}(V6,V4) | r-{T}(V3,V2)
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 #1983: 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 == V44, V44 == V45, V45 == V46, V46 == V47, V37 == V48, V47 == V51, V48 == V52, V51 == V61, V61 == V62, V62 == V63, V63 == V64, V64 == V65, V65 == V66, V66 == V67, V67 == V68; #1933 ), references = 1, size of lhs = 66:
% 11.96/12.13 P_z-{F}(V0), r-{F}(V0,V1), b-{F}(V1,V2), r-{F}(V0,V3), b-{F}(V3,V0), b-{F}(V3,V2), b-{F}(V3,V4), P_s-{F}(V5,V1), P_s-{F}(V6,V3), r-{F}(V0,V7), V7 == V0, P_s-{F}(V0,V7), P_s-{F}(V8,V7), P_s-{F}(V9,V7), r-{F}(V0,V10), b-{F}(V10,V11), r-{F}(V0,V12), b-{F}(V12,V0), b-{F}(V12,V11), b-{F}(V12,V13), P_s-{F}(V14,V7), P_s-{F}(V15,V10), P_s-{F}(V16,V7), P_s-{F}(V17,V12), b-{F}(V12,V18), b-{F}(V12,V19), b-{F}(V3,V19), r-{F}(V19,V3), b-{F}(V3,V20), r-{F}(V19,V21), b-{F}(V21,V20), r-{F}(V19,V22), b-{F}(V22,V18), P_s-{F}(V23,V24), V24 == V0, V24 == V7, V24 == V19, V24 == V21, V24 == V3, 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), P_s-{F}(V31,V30), P_s-{F}(V32,V30), P_s-{F}(V33,V30), P_s-{F}(V34,V30), P_s-{F}(V35,V30), P_s-{F}(V36,V37), V0 == V37, V37 == V7, P_s-{F}(V38,V37), P_s-{F}(V39,V38), P_s-{F}(V40,V41), V41 == V0, P_s-{F}(V42,V41), P_s-{F}(V43,V42), P_s-{F}(V44,V45), V45 == V12, V0 == V45, V45 == V7, P_s-{F}(V46,V45), P_s-{F}(V47,V46), P_s-{F}(V48,V45), P_s-{F}(V49,V48) | P_s-{T}(V30,V0), P_s-{T}(V30,V24), P_s-{T}(V30,V3), P_s-{T}(V30,V7), P_s-{T}(V30,V37), P_s-{T}(V30,V23), P_s-{T}(V30,V8), P_s-{T}(V30,V30), P_s-{T}(V30,V6), P_s-{T}(V30,V5), P_s-{T}(V30,V36), P_s-{T}(V30,V9), P_s-{T}(V30,V29), P_s-{T}(V30,V26), P_s-{T}(V30,V28), P_s-{T}(V30,V31), P_s-{T}(V30,V32), P_s-{T}(V30,V39), P_s-{T}(V30,V12), P_s-{T}(V30,V19), P_s-{T}(V30,V22), P_s-{T}(V30,V41), P_s-{T}(V30,V45), P_s-{T}(V30,V14), P_s-{T}(V30,V40), P_s-{T}(V30,V44), P_s-{T}(V30,V17), P_s-{T}(V30,V15), P_s-{T}(V30,V16), P_s-{T}(V30,V43), P_s-{T}(V30,V33), P_s-{T}(V30,V34), P_s-{T}(V30,V47), P_s-{T}(V30,V49), P_s-{T}(V30,V35)
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 #2054: 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 == V42, V42 == V43, V43 == V44, V44 == V45, V35 == V46, V45 == V49, V46 == V50, V49 == V59, V59 == V60, V60 == V61, V61 == V62, V62 == V63, V63 == V64, V64 == V65, V65 == V66, V66 == V99, V99 == V101, V101 == V103, V103 == V105, V105 == V107, V107 == V109, V109 == V111, V111 == V113, V113 == V115, V115 == V117, V117 == V119, V119 == V121, V121 == V123, V123 == V125, V125 == V127, V127 == V129, V129 == V131, V131 == V133, V133 == V135, V135 == V137; #1984 ), references = 1, size of lhs = 106:
% 11.96/12.13 P_z-{F}(V0), r-{F}(V0,V1), b-{F}(V1,V2), r-{F}(V0,V3), b-{F}(V3,V0), b-{F}(V3,V2), b-{F}(V3,V4), P_s-{F}(V5,V1), P_s-{F}(V6,V3), r-{F}(V0,V7), V7 == V0, P_s-{F}(V0,V7), P_s-{F}(V8,V7), P_s-{F}(V9,V7), r-{F}(V0,V10), b-{F}(V10,V11), r-{F}(V0,V12), b-{F}(V12,V0), b-{F}(V12,V11), b-{F}(V12,V13), P_s-{F}(V14,V7), P_s-{F}(V15,V10), P_s-{F}(V16,V7), P_s-{F}(V17,V12), b-{F}(V12,V18), b-{F}(V12,V19), b-{F}(V3,V19), r-{F}(V19,V3), b-{F}(V3,V20), r-{F}(V19,V21), b-{F}(V21,V20), r-{F}(V19,V22), b-{F}(V22,V18), P_s-{F}(V23,V3), P_s-{F}(V24,V7), P_s-{F}(V25,V12), P_s-{F}(V26,V7), P_s-{F}(V27,V22), P_s-{F}(V28,V29), P_s-{F}(V29,V30), V30 == V0, V30 == V7, V30 == V19, V30 == V21, V30 == V3, P_s-{F}(V31,V30), P_s-{F}(V32,V30), P_s-{F}(V33,V32), P_s-{F}(V34,V30), P_s-{F}(V35,V34), P_s-{F}(V36,V37), P_s-{F}(V37,V38), V0 == V38, V38 == V7, P_s-{F}(V39,V38), P_s-{F}(V40,V38), P_s-{F}(V41,V40), P_s-{F}(V42,V43), P_s-{F}(V43,V44), V44 == V0, P_s-{F}(V45,V44), P_s-{F}(V46,V44), P_s-{F}(V47,V46), P_s-{F}(V48,V49), P_s-{F}(V49,V50), V50 == V12, V0 == V50, V50 == V7, P_s-{F}(V51,V50), P_s-{F}(V52,V50), P_s-{F}(V53,V52), P_s-{F}(V54,V50), P_s-{F}(V55,V54), P_s-{F}(V56,V57), V31 == V57, V23 == V57, V24 == V57, V39 == V57, V33 == V57, V56 == V57, V41 == V57, V25 == V57, V26 == V57, V27 == V57, V45 == V57, V51 == V57, V47 == V57, V53 == V57, P_s-{F}(V58,V57), P_s-{F}(V59,V58), V59 == V57, P_s-{F}(V60,V57), P_s-{F}(V61,V60), V61 == V57, P_s-{F}(V62,V57), P_s-{F}(V63,V62), V63 == V57, P_s-{F}(V64,V57), P_s-{F}(V65,V64), V65 == V57, P_s-{F}(V66,V57), P_s-{F}(V67,V66), V67 == V57, P_s-{F}(V68,V57), P_s-{F}(V69,V68), V69 == V57 | P_s-{T}(V57,V0), P_s-{T}(V57,V8), P_s-{T}(V57,V6), P_s-{T}(V57,V5), P_s-{T}(V57,V9), P_s-{T}(V57,V28), P_s-{T}(V57,V35), P_s-{T}(V57,V36), P_s-{T}(V57,V19), P_s-{T}(V57,V14), P_s-{T}(V57,V17), P_s-{T}(V57,V15), P_s-{T}(V57,V16), P_s-{T}(V57,V42), P_s-{T}(V57,V48), P_s-{T}(V57,V55)
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 #2151: 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 == V42, V42 == V43, V43 == V44, V44 == V45, V35 == V46, V45 == V59, V59 == V60, V60 == V61, V61 == V62, V62 == V63, V63 == V64, V64 == V65, V65 == V66, V66 == V72, V72 == V73, V73 == V75, V75 == V77, V77 == V78, V78 == V79, V79 == V80, V80 == V81, V81 == V82, V82 == V83, V83 == V84, V84 == V86, V86 == V88, V88 == V90, V90 == V91, V91 == V92, V92 == V93, V93 == V94, V94 == V95, V95 == V96, V96 == V34, V34 == V68, V68 == V40, V40 == V48, V46 == V38, V48 == V41, V38 == V36, V41 == V47, V47 == V97, V36 == V98, V97 == V104, V98 == V103, V104 == V105, V103 == V106, V99 == V107, V105 == V49, V106 == V50, V49 == V55, V55 == V58, V50 == V53, V58 == V56, V53 == V51, V56 == V57, V57 == V111, V51 == V112, V107 == V113, V111 == V117, V112 == V118, V113 == V119; #2055 ), references = 1, size of lhs = 71:
% 11.96/12.13 P_z-{F}(V0), r-{F}(V0,V1), b-{F}(V1,V2), r-{F}(V0,V3), b-{F}(V3,V4), P_s-{F}(V5,V3), r-{F}(V0,V6), V6 == V0, b-{F}(V6,V2), b-{F}(V6,V4), b-{F}(V6,V0), P_s-{F}(V0,V6), P_s-{F}(V7,V6), b-{F}(V6,V8), b-{F}(V6,V9), P_s-{F}(V10,V6), b-{F}(V6,V11), b-{F}(V6,V12), P_s-{F}(V13,V6), P_s-{F}(V14,V6), P_s-{F}(V6,V15), V15 == V1, V0 == V15, V15 == V6, P_s-{F}(V16,V15), P_s-{F}(V17,V15), P_s-{F}(V18,V15), P_s-{F}(V19,V15), P_s-{F}(V20,V15), P_s-{F}(V21,V20), P_s-{F}(V22,V15), P_s-{F}(V23,V22), P_s-{F}(V24,V15), P_s-{F}(V25,V24), P_s-{F}(V26,V15), P_s-{F}(V27,V26), P_s-{F}(V28,V15), P_s-{F}(V29,V28), P_s-{F}(V30,V31), V16 == V31, V10 == V31, V7 == V31, V17 == V31, V21 == V31, V30 == V31, V23 == V31, V13 == V31, V14 == V31, V5 == V31, V18 == V31, V19 == V31, V25 == V31, V27 == 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,V31), P_s-{F}(V37,V36), V37 == V31, P_s-{F}(V38,V31), P_s-{F}(V39,V38), V39 == V31, P_s-{F}(V40,V31), P_s-{F}(V41,V40), V41 == V31, P_s-{F}(V42,V31), P_s-{F}(V43,V42), V43 == V31 | P_s-{T}(V31,V29)
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 #2245: 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, V2 == V41, V40 == V42, V42 == V43, V43 == V44, V44 == V45, V45 == V46, V46 == V47, V47 == V48, V48 == V49, V49 == V50, V50 == V51, V51 == V52, V52 == V54, V54 == V55, V55 == V56, V56 == V57, V57 == V58, V58 == V59, V59 == V60, V60 == V61, V61 == V62, V62 == V63, V63 == V64, V64 == V65, V65 == V66, V66 == V67, V67 == V68, V68 == V69, V69 == V70, V70 == V77, V77 == V78, V78 == V79, V79 == V80, V80 == V81, V41 == V82, V81 == V85, V82 == V86, V85 == V87, V86 == V88, V83 == V89, V87 == V1, V1 == V95, V95 == V96, V96 == V97, V97 == V98, V98 == V99, V88 == V100, V89 == V101, V99 == V103, V100 == V104, V101 == V105, V103 == V107, V104 == V108; #2153 ), references = 2, size of lhs = 63:
% 11.96/12.13 P_z-{F}(V0), P_s-{F}(V0,V1), V1 == V0, b-{F}(V1,V0), P_s-{F}(V2,V1), b-{F}(V1,V3), b-{F}(V1,V4), b-{F}(V1,V5), P_s-{F}(V6,V1), P_s-{F}(V7,V1), b-{F}(V1,V8), b-{F}(V1,V9), b-{F}(V1,V10), P_s-{F}(V11,V1), P_s-{F}(V12,V1), P_s-{F}(V1,V13), V0 == V13, V13 == V1, P_s-{F}(V14,V13), P_s-{F}(V15,V13), P_s-{F}(V16,V13), P_s-{F}(V17,V13), P_s-{F}(V18,V13), P_s-{F}(V19,V18), P_s-{F}(V20,V13), P_s-{F}(V21,V20), P_s-{F}(V22,V13), P_s-{F}(V23,V22), P_s-{F}(V24,V13), P_s-{F}(V25,V24), P_s-{F}(V26,V27), V14 == V27, V6 == V27, V2 == V27, V15 == V27, V19 == V27, V26 == V27, V21 == V27, V11 == V27, V12 == V27, V7 == V27, V16 == V27, V17 == V27, V23 == 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,V27), P_s-{F}(V33,V32), V33 == V27, P_s-{F}(V34,V27), P_s-{F}(V35,V34), V35 == V27, P_s-{F}(V36,V27), P_s-{F}(V37,V36), V37 == V27, P_s-{F}(V38,V27), P_s-{F}(V39,V38), V39 == V27 | b-{T}(V0,V1)
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 #2270: mergings( V2 == V5, V5 == V10, V10 == V11, V11 == V13, V13 == V14, V14 == V15, V15 == V16; #2261 ), references = 1, size of lhs = 46:
% 11.96/12.13 P_z-{F}(V0), r-{F}(V0,V1), r-{F}(V1,V0), r-{F}(V0,V2), r-{F}(V2,V0), P_s-{F}(V3,V2), P_s-{F}(V4,V1), r-{F}(V0,V5), r-{F}(V5,V0), P_s-{F}(V6,V5), P_s-{F}(V7,V5), r-{F}(V5,V8), b-{F}(V9,V8), b-{F}(V9,V0), b-{F}(V9,V5), b-{F}(V9,V10), r-{F}(V5,V10), b-{F}(V9,V11), b-{F}(V10,V12), b-{F}(V12,V11), b-{F}(V9,V13), b-{F}(V8,V14), b-{F}(V14,V13), P_s-{F}(V15,V16), V5 == V16, V16 == V0, P_s-{F}(V17,V18), V18 == V5, V16 == V18, V0 == V18, P_s-{F}(V19,V20), V2 == V20, V0 == V20, V9 == V20, V20 == V8, V20 == V5, P_s-{F}(V21,V20), P_s-{F}(V22,V23), V23 == V0, V23 == V20, V2 == V23, P_s-{F}(V24,V25), V25 == V5, V25 == V20, V0 == V25, #-{F} V26 | P_s-{T}(V26,V0), P_s-{T}(V26,V9), P_s-{T}(V26,V10), P_s-{T}(V26,V5), P_s-{T}(V26,V16), P_s-{T}(V26,V18), P_s-{T}(V26,V20), P_s-{T}(V26,V1), P_s-{T}(V26,V2), P_s-{T}(V26,V23), P_s-{T}(V26,V25), P_s-{T}(V26,V6), P_s-{T}(V26,V26), P_s-{T}(V26,V15), P_s-{T}(V26,V17), P_s-{T}(V26,V3), P_s-{T}(V26,V4), P_s-{T}(V26,V19), P_s-{T}(V26,V22), P_s-{T}(V26,V7), P_s-{T}(V26,V21), P_s-{T}(V26,V24)
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 #2296: mergings( V0 == V3, V3 == V8, V8 == V9, V9 == V11, V11 == V12, V12 == V13, V13 == V14, V14 == V34, V34 == V36, V36 == V38, V38 == V40, V40 == V42, V42 == V44, V44 == V46, V46 == V48, V48 == V50, V50 == V52, V52 == V54, V54 == V56, V56 == V58, V58 == V60, V60 == V62, V62 == V64, V64 == V66; #2271 ), references = 1, size of lhs = 79:
% 11.96/12.13 P_z-{F}(V0), r-{F}(V0,V1), r-{F}(V1,V0), r-{F}(V0,V2), r-{F}(V2,V0), r-{F}(V0,V3), r-{F}(V3,V0), r-{F}(V3,V4), r-{F}(V3,V5), b-{F}(V5,V6), b-{F}(V6,V7), b-{F}(V4,V8), b-{F}(V8,V9), P_s-{F}(V10,V3), P_s-{F}(V11,V1), P_s-{F}(V12,V2), P_s-{F}(V13,V3), P_s-{F}(V14,V13), P_s-{F}(V15,V2), P_s-{F}(V16,V15), P_s-{F}(V17,V1), P_s-{F}(V18,V17), P_s-{F}(V19,V3), P_s-{F}(V20,V19), b-{F}(V21,V4), b-{F}(V21,V0), b-{F}(V21,V3), b-{F}(V21,V5), b-{F}(V21,V7), b-{F}(V21,V9), P_s-{F}(V22,V21), P_s-{F}(V23,V24), V24 == V3, V0 == V24, P_s-{F}(V25,V24), P_s-{F}(V26,V27), V27 == V0, V2 == V27, P_s-{F}(V28,V27), P_s-{F}(V29,V30), V30 == V3, V0 == V30, P_s-{F}(V31,V30), P_s-{F}(V32,V33), V3 == V33, V33 == V0, V33 == V24, P_s-{F}(V34,V33), P_s-{F}(V35,V34), P_s-{F}(V36,V37), V2 == V37, V0 == V37, V21 == V37, V37 == V4, V37 == V3, V27 == V37, V30 == V37, P_s-{F}(V38,V37), P_s-{F}(V39,V38), P_s-{F}(V40,V37), P_s-{F}(V41,V40), P_s-{F}(V42,V43), V22 == V43, V10 == V43, V32 == V43, V25 == V43, V36 == V43, V11 == V43, V12 == V43, V28 == V43, V31 == V43, V14 == V43, V42 == V43, V35 == V43, V16 == V43, V18 == V43, V39 == V43, V20 == V43, V41 == V43 | P_s-{T}(V43,V0), P_s-{T}(V43,V5), P_s-{T}(V43,V23), P_s-{T}(V43,V26), P_s-{T}(V43,V29)
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 #2326: mergings( V5 == V7, V7 == V8, V8 == V9, V9 == V10, V10 == V17, V17 == V18, V18 == V20, V20 == V21, V21 == V22, V22 == V23, V23 == V25, V25 == V27, V27 == V28, V28 == V29, V29 == V30, V30 == V31, V31 == V32, V32 == V33, V33 == V34, V34 == V35, V35 == V36, V36 == V0, V0 == V6, V6 == V12, V12 == V2, V2 == V47, V47 == V50, V48 == V51; #2297 ), references = 1, size of lhs = 75:
% 11.96/12.13 P_z-{F}(V0), r-{F}(V0,V1), r-{F}(V1,V0), r-{F}(V1,V2), b-{F}(V0,V3), b-{F}(V3,V4), b-{F}(V2,V5), b-{F}(V5,V6), P_s-{F}(V7,V1), r-{F}(V0,V8), r-{F}(V8,V0), r-{F}(V0,V9), r-{F}(V9,V0), P_s-{F}(V10,V8), P_s-{F}(V11,V9), P_s-{F}(V0,V12), V12 == V1, V12 == V0, V9 == V12, P_s-{F}(V13,V12), P_s-{F}(V14,V12), P_s-{F}(V15,V1), P_s-{F}(V16,V15), P_s-{F}(V17,V9), P_s-{F}(V18,V17), P_s-{F}(V19,V8), P_s-{F}(V20,V19), P_s-{F}(V21,V1), P_s-{F}(V22,V21), b-{F}(V23,V2), b-{F}(V23,V1), b-{F}(V23,V0), b-{F}(V23,V4), b-{F}(V23,V6), P_s-{F}(V24,V23), P_s-{F}(V25,V26), V26 == V1, V0 == V26, P_s-{F}(V27,V26), P_s-{F}(V28,V29), V1 == V29, V29 == V0, V29 == V12, P_s-{F}(V30,V29), P_s-{F}(V31,V30), P_s-{F}(V32,V33), V9 == V33, V0 == V33, V23 == V33, V33 == V2, V33 == V1, V12 == V33, V26 == V33, P_s-{F}(V34,V33), P_s-{F}(V35,V34), P_s-{F}(V36,V33), P_s-{F}(V37,V36), P_s-{F}(V38,V39), V24 == V39, V7 == V39, V28 == V39, V13 == V39, V32 == V39, V10 == V39, V11 == V39, V14 == V39, V27 == V39, V16 == V39, V38 == V39, V31 == V39, V18 == V39, V20 == V39, V35 == V39, V22 == V39, V37 == V39 | P_s-{T}(V39,V25)
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 #2358: 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 == V26, V26 == V1, V1 == V34, V34 == V37, V35 == V38, V37 == V40, V38 == V41; #2328 ), references = 1, size of lhs = 65:
% 11.96/12.13 P_z-{F}(V0), b-{F}(V0,V1), b-{F}(V1,V2), P_s-{F}(V0,V3), V0 == V3, P_s-{F}(V4,V3), P_s-{F}(V5,V3), P_s-{F}(V6,V3), b-{F}(V7,V0), b-{F}(V7,V2), b-{F}(V7,V8), b-{F}(V8,V9), b-{F}(V9,V10), b-{F}(V7,V10), b-{F}(V7,V11), V0 == V11, V3 == V11, r-{F}(V11,V8), r-{F}(V11,V0), P_s-{F}(V12,V11), P_s-{F}(V13,V11), P_s-{F}(V14,V11), P_s-{F}(V15,V7), P_s-{F}(V16,V11), P_s-{F}(V17,V16), P_s-{F}(V18,V11), P_s-{F}(V19,V18), P_s-{F}(V20,V11), P_s-{F}(V21,V20), P_s-{F}(V22,V11), P_s-{F}(V23,V22), P_s-{F}(V24,V25), V11 == V25, V25 == V0, V25 == V3, P_s-{F}(V26,V25), P_s-{F}(V27,V26), P_s-{F}(V28,V29), V0 == V29, V7 == V29, V29 == V8, V29 == V11, V3 == V29, P_s-{F}(V30,V29), P_s-{F}(V31,V30), P_s-{F}(V32,V29), P_s-{F}(V33,V32), P_s-{F}(V34,V35), V15 == V35, V12 == V35, V24 == V35, V4 == V35, V28 == V35, V13 == V35, V14 == V35, V5 == V35, V6 == V35, V17 == V35, V34 == V35, V27 == V35, V19 == V35, V21 == V35, V31 == V35, V23 == V35, V33 == V35 | b-{T}(V0,V11)
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 #2401: 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 == V30, V28 == V31, V30 == V33, V31 == V34, V33 == V36, V36 == V41; #2368 ), references = 3, size of lhs = 80:
% 11.96/12.13 P_z-{F}(V0), P_s-{F}(V0,V1), V0 == V1, P_s-{F}(V2,V1), P_s-{F}(V3,V1), P_s-{F}(V4,V1), b-{F}(V0,V5), b-{F}(V5,V6), b-{F}(V0,V7), b-{F}(V7,V8), b-{F}(V0,V9), V9 == V0, b-{F}(V9,V6), b-{F}(V9,V8), b-{F}(V9,V0), b-{F}(V0,V10), b-{F}(V10,V11), b-{F}(V9,V11), P_s-{F}(V12,V9), P_s-{F}(V13,V9), P_s-{F}(V14,V9), P_s-{F}(V15,V9), P_s-{F}(V16,V17), V0 == V17, V1 == V17, V17 == V9, P_s-{F}(V18,V17), P_s-{F}(V19,V17), P_s-{F}(V20,V17), P_s-{F}(V21,V17), P_s-{F}(V22,V21), P_s-{F}(V23,V17), P_s-{F}(V24,V23), P_s-{F}(V25,V17), P_s-{F}(V26,V25), P_s-{F}(V27,V17), P_s-{F}(V28,V27), P_s-{F}(V29,V30), V17 == V30, V30 == V0, V30 == V1, P_s-{F}(V31,V30), P_s-{F}(V32,V31), P_s-{F}(V33,V34), V9 == V34, V34 == V0, V34 == V17, V1 == V34, P_s-{F}(V35,V34), P_s-{F}(V36,V35), P_s-{F}(V37,V34), P_s-{F}(V38,V37), P_s-{F}(V39,V40), V12 == V40, V16 == V40, V29 == V40, V2 == V40, V33 == V40, V18 == V40, V19 == V40, V3 == V40, V4 == V40, V22 == V40, V39 == V40, V32 == V40, V24 == V40, V26 == V40, V36 == V40, V28 == V40, V38 == V40, P_s-{F}(V41,V42), V42 == V9, V42 == V0, V42 == V17, #-{F} V43, V14 == V43, V15 == V43, V41 == V43, V13 == V43, V20 == V43 | r-{T}(V9,V17)
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 #2436: 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 == V30, V28 == V31, V30 == V33, V31 == V34, V33 == V36, V36 == V37, V37 == V38, V38 == V39, V39 == V48; #2369 ), references = 1, size of lhs = 100:
% 11.96/12.13 P_z-{F}(V0), P_s-{F}(V0,V1), V0 == V1, P_s-{F}(V2,V1), P_s-{F}(V3,V1), P_s-{F}(V4,V1), b-{F}(V0,V5), b-{F}(V5,V6), b-{F}(V0,V7), b-{F}(V7,V8), b-{F}(V0,V9), b-{F}(V9,V10), b-{F}(V0,V11), b-{F}(V11,V12), b-{F}(V0,V13), V0 == V13, b-{F}(V13,V10), b-{F}(V13,V0), b-{F}(V13,V14), b-{F}(V14,V13), b-{F}(V13,V15), b-{F}(V15,V13), P_s-{F}(V16,V13), b-{F}(V0,V17), b-{F}(V17,V18), b-{F}(V13,V18), P_s-{F}(V19,V13), b-{F}(V0,V20), b-{F}(V20,V6), b-{F}(V20,V8), b-{F}(V20,V12), b-{F}(V20,V0), b-{F}(V0,V21), b-{F}(V21,V22), b-{F}(V20,V22), b-{F}(V0,V23), b-{F}(V23,V24), b-{F}(V20,V24), P_s-{F}(V25,V20), P_s-{F}(V26,V20), P_s-{F}(V27,V28), V20 == V28, V0 == V28, V1 == V28, V28 == V13, P_s-{F}(V29,V28), P_s-{F}(V30,V28), P_s-{F}(V31,V28), P_s-{F}(V32,V28), P_s-{F}(V33,V32), P_s-{F}(V34,V28), P_s-{F}(V35,V34), P_s-{F}(V36,V28), P_s-{F}(V37,V36), P_s-{F}(V38,V28), P_s-{F}(V39,V38), P_s-{F}(V40,V41), V28 == V41, V41 == V0, V41 == V1, P_s-{F}(V42,V41), P_s-{F}(V43,V42), P_s-{F}(V44,V45), V20 == V45, V45 == V0, V45 == V28, V1 == V45, P_s-{F}(V46,V45), P_s-{F}(V47,V46), P_s-{F}(V48,V45), P_s-{F}(V49,V48), P_s-{F}(V50,V51), V25 == V51, V27 == V51, V40 == V51, V2 == V51, V44 == V51, V29 == V51, V30 == V51, V3 == V51, V4 == V51, V33 == V51, V50 == V51, V43 == V51, V35 == V51, V37 == V51, V47 == V51, V39 == V51, V49 == V51, P_s-{F}(V52,V53), V20 == V53, V53 == V13, V53 == V0, V53 == V28, #-{F} V54, V19 == V54, V52 == V54, V16 == V54, V31 == V54, V26 == V54 | r-{T}(V20,V28)
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 #2442: mergings( V2 == V18, V18 == V19; #2439 ), references = 1, size of lhs = 54:
% 11.96/12.13 P_z-{F}(V0), P_s-{F}(V0,V1), V0 == V1, P_s-{F}(V2,V1), P_s-{F}(V3,V1), P_s-{F}(V4,V1), b-{F}(V0,V5), b-{F}(V5,V6), b-{F}(V0,V7), b-{F}(V7,V8), b-{F}(V0,V9), V9 == V0, b-{F}(V9,V6), b-{F}(V9,V8), b-{F}(V9,V0), b-{F}(V0,V10), b-{F}(V10,V11), b-{F}(V9,V11), P_s-{F}(V12,V9), P_s-{F}(V13,V9), P_s-{F}(V14,V9), P_s-{F}(V15,V9), r-{F}(V9,V16), b-{F}(V16,V17), b-{F}(V17,V18), r-{F}(V9,V19), b-{F}(V19,V16), b-{F}(V19,V18), P_s-{F}(V20,V21), P_s-{F}(V22,V21), P_s-{F}(V23,V21), P_s-{F}(V24,V21), P_s-{F}(V25,V26), V26 == V0, V26 == V1, P_s-{F}(V27,V26), P_s-{F}(V28,V27), P_s-{F}(V29,V30), V9 == V30, V30 == V0, V1 == V30, P_s-{F}(V31,V30), P_s-{F}(V32,V31), P_s-{F}(V33,V30), P_s-{F}(V34,V33), P_s-{F}(V35,V36), V36 == V9, V36 == V0, #-{F} V37, V14 == V37, V15 == V37, V35 == V37, V13 == V37, V21 == V37 | P_s-{T}(V21,V0), P_s-{T}(V21,V1), P_s-{T}(V21,V9), P_s-{T}(V21,V16), P_s-{T}(V21,V19), P_s-{T}(V21,V26), P_s-{T}(V21,V30), P_s-{T}(V21,V12), P_s-{T}(V21,V21), P_s-{T}(V21,V25), P_s-{T}(V21,V2), P_s-{T}(V21,V29), P_s-{T}(V21,V3), P_s-{T}(V21,V4), P_s-{T}(V21,V20), P_s-{T}(V21,V28), P_s-{T}(V21,V22), P_s-{T}(V21,V23), P_s-{T}(V21,V32), P_s-{T}(V21,V24), P_s-{T}(V21,V34), P_s-{T}(V21,V36)
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 #2471: mergings( V16 == V17, V17 == V0, V0 == V40, V40 == V42, V42 == V44, V44 == V46, V46 == V48, V48 == V50, V50 == V12, V1 == V9, V12 == V52, V52 == V54, V54 == V2, V2 == V56, V56 == V3, V3 == V4, V4 == V58, V58 == V30, V9 == V29, V30 == V60, V60 == V62, V62 == V34, V29 == V33, V28 == V32, V34 == V64, V64 == V36, V33 == V35; #2443 ), references = 1, size of lhs = 67:
% 11.96/12.13 P_z-{F}(V0), b-{F}(V0,V1), b-{F}(V1,V2), b-{F}(V0,V3), b-{F}(V3,V4), b-{F}(V0,V5), V5 == V0, b-{F}(V5,V2), b-{F}(V5,V4), b-{F}(V5,V0), P_s-{F}(V0,V5), b-{F}(V0,V6), b-{F}(V6,V7), b-{F}(V5,V7), P_s-{F}(V8,V5), P_s-{F}(V9,V5), P_s-{F}(V10,V5), r-{F}(V5,V11), b-{F}(V11,V12), b-{F}(V12,V13), r-{F}(V5,V14), b-{F}(V14,V11), b-{F}(V14,V13), P_s-{F}(V15,V5), P_s-{F}(V16,V5), P_s-{F}(V17,V11), P_s-{F}(V18,V14), P_s-{F}(V5,V19), V19 == V0, V5 == V19, P_s-{F}(V20,V19), P_s-{F}(V21,V19), P_s-{F}(V22,V19), P_s-{F}(V23,V22), P_s-{F}(V24,V19), P_s-{F}(V25,V24), P_s-{F}(V26,V27), V27 == V5, V27 == V0, P_s-{F}(V28,V29), V15 == V29, V16 == V29, V17 == V29, V18 == V29, V20 == V29, V21 == V29, V28 == V29, V23 == V29, V25 == V29, P_s-{F}(V30,V29), P_s-{F}(V31,V30), V31 == V29, P_s-{F}(V32,V29), P_s-{F}(V33,V32), V33 == V29, P_s-{F}(V34,V29), P_s-{F}(V35,V34), V35 == V29, P_s-{F}(V36,V29), P_s-{F}(V37,V36), V37 == V29, #-{F} V38, V9 == V38, V10 == V38, V26 == V38, V8 == V38, V29 == V38 | P_s-{T}(V29,V27)
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 #2543: 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 == V30, V28 == V31, V30 == V33, V31 == V34, V33 == V36, V36 == V41, V41 == V49, V34 == V50, V49 == V64, V64 == V65, V65 == V66, V66 == V67, V67 == V68, V50 == V69, V68 == V79, V79 == V81, V81 == V83, V83 == V84, V84 == V85, V85 == V86, V86 == V87, V69 == V42, V87 == V88, V88 == V89, V89 == V90, V90 == V91, V91 == V92, V92 == V93, V93 == V94, V94 == V95, V42 == V96, V95 == V99, V99 == V100, V100 == V101, V96 == V102, V97 == V103, V101 == V105, V105 == V106, V102 == V107, V106 == V108; #2477 ), references = 1, size of lhs = 110:
% 11.96/12.13 P_z-{F}(V0), b-{F}(V0,V1), b-{F}(V1,V2), b-{F}(V0,V3), b-{F}(V3,V4), b-{F}(V0,V5), b-{F}(V5,V6), b-{F}(V0,V7), b-{F}(V7,V8), b-{F}(V0,V9), b-{F}(V9,V10), b-{F}(V0,V11), b-{F}(V11,V12), b-{F}(V0,V13), V0 == V13, b-{F}(V13,V2), b-{F}(V13,V4), b-{F}(V13,V6), b-{F}(V13,V8), b-{F}(V13,V10), b-{F}(V13,V12), b-{F}(V13,V0), P_s-{F}(V0,V13), P_s-{F}(V14,V13), P_s-{F}(V15,V13), P_s-{F}(V16,V13), P_s-{F}(V17,V13), P_s-{F}(V18,V13), P_s-{F}(V19,V13), P_s-{F}(V20,V13), P_s-{F}(V21,V13), P_s-{F}(V22,V13), P_s-{F}(V23,V13), P_s-{F}(V24,V13), P_s-{F}(V25,V13), P_s-{F}(V26,V13), P_s-{F}(V27,V13), b-{F}(V0,V28), b-{F}(V28,V29), b-{F}(V13,V29), b-{F}(V0,V30), b-{F}(V30,V31), b-{F}(V13,V31), b-{F}(V0,V32), b-{F}(V32,V33), b-{F}(V13,V33), P_s-{F}(V34,V13), P_s-{F}(V35,V13), P_s-{F}(V36,V13), P_s-{F}(V37,V13), P_s-{F}(V38,V13), P_s-{F}(V13,V39), V39 == V0, V13 == V39, P_s-{F}(V40,V39), P_s-{F}(V41,V39), 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), V0 == V47, V47 == V13, 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,V52), P_s-{F}(V54,V47), P_s-{F}(V55,V54), P_s-{F}(V56,V47), P_s-{F}(V57,V56), P_s-{F}(V58,V47), P_s-{F}(V59,V58), P_s-{F}(V60,V61), P_s-{F}(V62,V61), P_s-{F}(V63,V61), P_s-{F}(V64,V61), P_s-{F}(V65,V61), P_s-{F}(V66,V61), P_s-{F}(V67,V61), P_s-{F}(V68,V61), P_s-{F}(V69,V61), P_s-{F}(V70,V61), P_s-{F}(V71,V61), P_s-{F}(V72,V73), V73 == V0, V73 == V13, P_s-{F}(V74,V73), P_s-{F}(V75,V74), P_s-{F}(V76,V77), V77 == V0, V13 == V77, P_s-{F}(V78,V77), P_s-{F}(V79,V78), P_s-{F}(V80,V77), P_s-{F}(V81,V80), P_s-{F}(V82,V83), V83 == V13, V83 == V0, P_s-{F}(V84,V85), V85 == V13, V85 == V0, P_s-{F}(V86,V85), #-{F} V87, V35 == V87, V36 == V87, V84 == V87, V34 == V87 | P_s-{T}(V61,V47), P_s-{T}(V61,V0), P_s-{T}(V61,V13), P_s-{T}(V61,V17), P_s-{T}(V61,V46), P_s-{T}(V61,V61), P_s-{T}(V61,V14), P_s-{T}(V61,V48), P_s-{T}(V61,V49), P_s-{T}(V61,V15), P_s-{T}(V61,V16), P_s-{T}(V61,V53), P_s-{T}(V61,V60), P_s-{T}(V61,V55), P_s-{T}(V61,V57), P_s-{T}(V61,V62), P_s-{T}(V61,V59), P_s-{T}(V61,V63), P_s-{T}(V61,V73), P_s-{T}(V61,V77), P_s-{T}(V61,V24), P_s-{T}(V61,V72), P_s-{T}(V61,V21), P_s-{T}(V61,V76), P_s-{T}(V61,V22), P_s-{T}(V61,V23), P_s-{T}(V61,V64), P_s-{T}(V61,V75), P_s-{T}(V61,V65), P_s-{T}(V61,V66), P_s-{T}(V61,V79), P_s-{T}(V61,V67), P_s-{T}(V61,V81), P_s-{T}(V61,V83), P_s-{T}(V61,V37), P_s-{T}(V61,V38), P_s-{T}(V61,V51), P_s-{T}(V61,V40), P_s-{T}(V61,V41), P_s-{T}(V61,V43), P_s-{T}(V61,V45), P_s-{T}(V61,V86), P_s-{T}(V61,V68), P_s-{T}(V61,V69), P_s-{T}(V61,V70), P_s-{T}(V61,V71), P_s-{T}(V61,V19), P_s-{T}(V61,V20), P_s-{T}(V61,V18), P_s-{T}(V61,V50), P_s-{T}(V61,V26), P_s-{T}(V61,V27), P_s-{T}(V61,V82), P_s-{T}(V61,V25), P_s-{T}(V61,V87)
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 #2679: 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 == V28, V26 == V29, V28 == V31, V29 == V32, V31 == V39, V39 == V62, V62 == V63, V63 == V64, V64 == V65, V65 == V66, V32 == V67, V66 == V34, V34 == V47, V48 == V67, V47 == V77, V77 == V79, V79 == V81, V81 == V82, V82 == V83, V83 == V84, V84 == V85, V67 == V40, V85 == V86, V86 == V87, V87 == V88, V88 == V89, V89 == V90, V90 == V91, V91 == V92, V92 == V93, V40 == V94, V93 == V97, V97 == V98, V98 == V99, V94 == V100, V95 == V101, V99 == V103, V103 == V104, V100 == V105, V104 == V106, V106 == V153, V153 == V155, V155 == V157, V157 == V159, V159 == V161, V161 == V43, V43 == V163, V163 == V165, V165 == V27, V27 == V167, V167 == V169, V169 == V30, V30 == V33, V33 == V118, V105 == V117, V101 == V112, V118 == V171, V171 == V120, V117 == V119, V120 == V122, V119 == V121, V122 == V173, V173 == V124, V121 == V123, V124 == V175, V175 == V177, V177 == V179, V179 == V181, V181 == V58, V58 == V183, V183 == V49, V49 == V185, V185 == V50, V50 == V51, V51 == V187, V187 == V140, V123 == V139, V112 == V138, V140 == V189, V189 == V191, V191 == V144, V139 == V143, V138 == V142, V144 == V193, V193 == V146, V143 == V145, V146 == V195, V195 == V78, V78 == V80, V80 == V197, V197 == V199, V199 == V201, V201 == V108, V145 == V107, V108 == V110, V107 == V109, V110 == V203, V203 == V205, V205 == V207, V207 == V209, V209 == V211, V211 == V45, V45 == V46, V46 == V44, V44 == V213, V213 == V60, V60 == V61, V61 == V215, V215 == V59; #2544 ), references = 2, size of lhs = 134:
% 11.96/12.13 P_z-{F}(V0), b-{F}(V0,V1), b-{F}(V1,V2), b-{F}(V0,V3), b-{F}(V3,V4), b-{F}(V0,V5), b-{F}(V5,V6), b-{F}(V0,V7), V0 == V7, b-{F}(V7,V2), b-{F}(V7,V4), b-{F}(V7,V6), b-{F}(V7,V0), P_s-{F}(V0,V7), b-{F}(V0,V8), b-{F}(V8,V9), b-{F}(V7,V9), b-{F}(V0,V10), b-{F}(V10,V11), b-{F}(V7,V11), b-{F}(V0,V12), b-{F}(V12,V13), b-{F}(V7,V13), b-{F}(V0,V14), b-{F}(V14,V15), b-{F}(V7,V15), b-{F}(V0,V16), b-{F}(V16,V17), b-{F}(V7,V17), b-{F}(V0,V18), b-{F}(V18,V19), b-{F}(V7,V19), P_s-{F}(V20,V7), P_s-{F}(V21,V7), P_s-{F}(V22,V7), P_s-{F}(V23,V7), P_s-{F}(V24,V7), P_s-{F}(V25,V7), P_s-{F}(V26,V7), P_s-{F}(V27,V7), P_s-{F}(V7,V28), V28 == V0, V7 == V28, P_s-{F}(V29,V28), P_s-{F}(V30,V28), P_s-{F}(V31,V28), P_s-{F}(V32,V28), P_s-{F}(V33,V32), P_s-{F}(V34,V28), P_s-{F}(V35,V34), P_s-{F}(V36,V28), P_s-{F}(V37,V36), P_s-{F}(V38,V28), P_s-{F}(V39,V38), P_s-{F}(V40,V28), P_s-{F}(V41,V40), P_s-{F}(V42,V28), P_s-{F}(V43,V42), P_s-{F}(V44,V28), P_s-{F}(V45,V44), P_s-{F}(V46,V28), P_s-{F}(V47,V46), P_s-{F}(V48,V28), P_s-{F}(V49,V48), P_s-{F}(V50,V51), V51 == V7, V51 == V0, P_s-{F}(V52,V51), P_s-{F}(V53,V52), P_s-{F}(V54,V55), V29 == V55, V23 == V55, V24 == V55, V25 == V55, V26 == V55, V37 == V55, V54 == V55, V39 == V55, V41 == V55, V27 == V55, V30 == V55, V31 == V55, V47 == V55, V49 == V55, V45 == V55, V33 == V55, V35 == V55, V53 == V55, V43 == V55, P_s-{F}(V56,V55), P_s-{F}(V57,V56), V57 == V55, P_s-{F}(V58,V55), P_s-{F}(V59,V58), V59 == V55, P_s-{F}(V60,V55), P_s-{F}(V61,V60), V61 == V55, P_s-{F}(V62,V55), P_s-{F}(V63,V62), V63 == V55, P_s-{F}(V64,V55), P_s-{F}(V65,V64), V65 == V55, P_s-{F}(V66,V55), P_s-{F}(V67,V66), V67 == V55, P_s-{F}(V68,V55), P_s-{F}(V69,V68), V69 == V55, P_s-{F}(V70,V55), P_s-{F}(V71,V70), V71 == V55, P_s-{F}(V72,V55), P_s-{F}(V73,V72), V73 == V55, P_s-{F}(V74,V55), P_s-{F}(V75,V74), V75 == V55, P_s-{F}(V76,V55), P_s-{F}(V77,V76), V77 == V55, P_s-{F}(V78,V79), V79 == V7, V79 == V0, V78 == V55, P_s-{F}(V80,V79), P_s-{F}(V81,V80), V81 == V55, #-{F} V82, V21 == V82, V22 == V82, V50 == V82, V20 == V82 | P_s-{T}(V55,V82)
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 #2688: mergings( V2 == V17; #2686 ), references = 1, size of lhs = 61:
% 11.96/12.13 P_z-{F}(V0), P_s-{F}(V0,V1), V0 == V1, 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,V0), P_s-{T}(V1,V1), P_s-{T}(V1,V2), P_s-{T}(V1,V17), P_s-{T}(V1,V18), P_s-{T}(V1,V19), P_s-{T}(V1,V16), P_s-{T}(V1,V33), P_s-{T}(V1,V34), P_s-{T}(V1,V35), P_s-{T}(V1,V36), P_s-{T}(V1,V37), P_s-{T}(V1,V38), P_s-{T}(V1,V39), P_s-{T}(V1,V40), P_s-{T}(V1,V4), P_s-{T}(V1,V3), P_s-{T}(V1,V20), P_s-{T}(V1,V21), P_s-{T}(V1,V6), P_s-{T}(V1,V7), P_s-{T}(V1,V5), P_s-{T}(V1,V22), P_s-{T}(V1,V23), P_s-{T}(V1,V41), P_s-{T}(V1,V42), P_s-{T}(V1,V43), P_s-{T}(V1,V44), P_s-{T}(V1,V45), P_s-{T}(V1,V46), P_s-{T}(V1,V11), P_s-{T}(V1,V12), P_s-{T}(V1,V13), P_s-{T}(V1,V14), P_s-{T}(V1,V26), P_s-{T}(V1,V27), P_s-{T}(V1,V28), P_s-{T}(V1,V15), P_s-{T}(V1,V31), P_s-{T}(V1,V32), P_s-{T}(V1,V30), P_s-{T}(V1,V24), P_s-{T}(V1,V25), P_s-{T}(V1,V47), P_s-{T}(V1,V29), P_s-{T}(V1,V48), P_s-{T}(V1,V49), P_s-{T}(V1,V50), P_s-{T}(V1,V51), P_s-{T}(V1,V52), P_s-{T}(V1,V53), P_s-{T}(V1,V54), P_s-{T}(V1,V55), P_s-{T}(V1,V56), P_s-{T}(V1,V57), P_s-{T}(V1,V58), P_s-{T}(V1,V59), P_s-{T}(V1,V9), P_s-{T}(V1,V10), P_s-{T}(V1,V8)
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 #2749: mergings( V16 == V0, V0 == V2, V2 == V18, V18 == V19, V19 == V20, V20 == V17, V17 == V34, V34 == V35, V35 == V36, V36 == V37, V37 == V38, V38 == V39, V39 == V40, V40 == V41, V41 == V4, V4 == V3, V3 == V21, V21 == V22, V22 == V6, V6 == V7, V7 == V5, V5 == V23, V23 == V24, V24 == V42, V42 == V43, V43 == V44, V44 == V45, V45 == V46, V46 == V47, V47 == V11, V11 == V12, V12 == V13, V13 == V14, V14 == V27, V27 == V28, V28 == V29, V29 == V15, V15 == V32, V32 == V33, V33 == V31, V31 == V25, V25 == V26, V26 == V48, V48 == V30, V30 == V49, V49 == V50, V50 == V51, V51 == V52, V52 == V53, V53 == V54, V54 == V55, V55 == V56, V56 == V57, V57 == V58, V58 == V59, V59 == V60, V60 == V9, V9 == V10, V10 == V8; #2689 ), references = 1, size of lhs = 3:
% 11.96/12.13 P_z-{F}(V0), P_s-{F}(V0,V1), V0 == V1 | P_s-{T}(V1,V1)
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 #2754: mergings( V2 == V0, V0 == V3; #2751 ), references = 1, size of lhs = 1:
% 11.96/12.13 P_z-{F}(V0) | P_s-{T}(V0,V0)
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 #2757: exists( #8, #2755 ), references = 1, size of lhs = 0:
% 11.96/12.13 FALSE | FALSE
% 11.96/12.13 (used 0 times, uses = {})
% 11.96/12.13
% 11.96/12.13 number of learnt formulas = 69
% 11.96/12.13
% 11.96/12.13
% 11.96/12.13 % SZS output end Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 11.96/12.13
% 11.96/12.13 randbase = 1
%------------------------------------------------------------------------------