%------------------------------------------------------------------------------
% File : Geo-III---2018C
% Problem : GRA162-1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : geo -tptp_input -nonempty -inputfile %s
% Computer : n015.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:33 PM UTC 2026
% Result : Unsatisfiable 2.15s 2.37s
% Output : Refutation 2.15s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : GRA162-1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.12 % Command : geo -tptp_input -nonempty -inputfile %s
% 0.16/0.33 % Computer : n015.cluster.edu
% 0.16/0.33 % Model : x86_64 x86_64
% 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.33 % Memory : 8042.1875MB
% 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.33 % CPULimit : 300
% 0.16/0.33 % WCLimit : 300
% 0.16/0.33 % DateTime : Tue May 5 00:29:31 EDT 2026
% 0.16/0.33 % CPUTime :
% 2.15/2.37 GeoParameters:
% 2.15/2.37
% 2.15/2.37 tptp_input = 1
% 2.15/2.37 tptp_output = 0
% 2.15/2.37 nonempty = 1
% 2.15/2.37 inputfile = /export/starexec/sandbox2/benchmark/theBenchmark.p
% 2.15/2.37 includepath = /export/starexec/sandbox2/solver/bin/../../benchmark/
% 2.15/2.37
% 2.15/2.37
% 2.15/2.37 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 2.15/2.37 % SZS output start Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 2.15/2.37
% 2.15/2.37 RuleSystem INPUT:
% 2.15/2.37
% 2.15/2.37 Initial Rules:
% 2.15/2.37 #0: input, references = 9, size of lhs = 2:
% 2.15/2.37 P_z-{F}(V0), P_s-{F}(V1,V0) | FALSE
% 2.15/2.37 (used 0 times, uses = {})
% 2.15/2.37
% 2.15/2.37 #1: input, references = 7, size of lhs = 4:
% 2.15/2.37 P_z-{F}(V0), P_s-{F}(V1,V4), P_s-{F}(V2,V4), V1 == V2 | FALSE
% 2.15/2.37 (used 0 times, uses = {})
% 2.15/2.37
% 2.15/2.37 #2: input, references = 3, size of lhs = 2:
% 2.15/2.37 P_z-{F}(V0), r-{F}(V1,V1) | FALSE
% 2.15/2.37 (used 0 times, uses = {})
% 2.15/2.37
% 2.15/2.37 #3: input, references = 3, size of lhs = 2:
% 2.15/2.37 P_z-{F}(V0), b-{F}(V1,V1) | FALSE
% 2.15/2.37 (used 0 times, uses = {})
% 2.15/2.37
% 2.15/2.37 #4: input, references = 12, size of lhs = 4:
% 2.15/2.37 P_z-{F}(V0), #-{F} V1, #-{F} V2, V1 == V2 | r-{T}(V1,V2), b-{T}(V1,V2)
% 2.15/2.37 (used 0 times, uses = {})
% 2.15/2.37
% 2.15/2.37 #5: input, references = 10, size of lhs = 4:
% 2.15/2.37 P_z-{F}(V0), r-{F}(V1,V2), r-{F}(V3,V1), r-{F}(V3,V2) | FALSE
% 2.15/2.37 (used 0 times, uses = {})
% 2.15/2.37
% 2.15/2.37 #6: input, references = 3, size of lhs = 5:
% 2.15/2.37 P_z-{F}(V0), b-{F}(V1,V2), b-{F}(V1,V3), b-{F}(V4,V1), b-{F}(V4,V3) | FALSE
% 2.15/2.37 (used 0 times, uses = {})
% 2.15/2.37
% 2.15/2.37 #7: input, references = 11, size of lhs = 1:
% 2.15/2.37 #-{F} V0 | EXISTS V1: P_s-{T}(V0,V1)
% 2.15/2.37 (used 0 times, uses = {})
% 2.15/2.37
% 2.15/2.37 #8: input, references = 4, size of lhs = 0:
% 2.15/2.37 FALSE | EXISTS V0: P_z-{T}(V0)
% 2.15/2.37 (used 0 times, uses = {})
% 2.15/2.37
% 2.15/2.37 number of initial rules = 9
% 2.15/2.37
% 2.15/2.37 Simplifiers:
% 2.15/2.37 #9: unsound, references = 3, size of lhs = 3:
% 2.15/2.37 P_s-{F}(V0,V1), P_s-{F}(V0,V3), V1 == V3 | FALSE
% 2.15/2.37 (used 0 times, uses = {})
% 2.15/2.37
% 2.15/2.37 #10: unsound, references = 3, size of lhs = 3:
% 2.15/2.37 P_z-{F}(V0), P_z-{F}(V1), V0 == V1 | FALSE
% 2.15/2.37 (used 0 times, uses = {})
% 2.15/2.37
% 2.15/2.37 number of simplifiers = 2
% 2.15/2.37
% 2.15/2.37 Learnt:
% 2.15/2.37 #13: mergings( V0 == V3; #11 ), references = 12, size of lhs = 4:
% 2.15/2.37 P_z-{F}(V0), b-{F}(V1,V2), b-{F}(V1,V3), V2 == V3 | r-{T}(V2,V3)
% 2.15/2.37 (used 0 times, uses = {})
% 2.15/2.37
% 2.15/2.37 #18: mergings( V0 == V3, V3 == V4; #15 ), references = 1, size of lhs = 6:
% 2.15/2.37 P_z-{F}(V0), b-{F}(V1,V2), r-{F}(V3,V2), r-{F}(V3,V4), V1 == V4, V2 == V4 | r-{T}(V1,V4)
% 2.15/2.37 (used 0 times, uses = {})
% 2.15/2.37
% 2.15/2.37 #25: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6; #20 ), references = 3, size of lhs = 8:
% 2.15/2.37 P_z-{F}(V0), r-{F}(V1,V2), r-{F}(V1,V3), b-{F}(V3,V2), #-{F} V4, V1 == V4, V2 == V4, V3 == V4 | b-{T}(V1,V4)
% 2.15/2.37 (used 0 times, uses = {})
% 2.15/2.37
% 2.15/2.37 #44: mergings( V0 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7, V7 == V8, V8 == V9, V9 == V10, V10 == V11, V11 == V12, V12 == V13; #32 ), references = 1, size of lhs = 19:
% 2.15/2.37 P_z-{F}(V0), r-{F}(V1,V2), r-{F}(V1,V3), V3 == V2, #-{F} V4, V1 == V4, V2 == V4, V3 == V4, #-{F} V5, V1 == V5, V2 == V5, V3 == V5, V4 == V5, #-{F} V6, V1 == V6, V2 == V6, V3 == V6, V4 == V6, V5 == V6 | r-{T}(V3,V2)
% 2.15/2.37 (used 0 times, uses = {})
% 2.15/2.37
% 2.15/2.37 #59: 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; #46 ), references = 1, size of lhs = 16:
% 2.15/2.37 P_z-{F}(V0), r-{F}(V1,V2), r-{F}(V1,V3), V3 == V2, r-{F}(V4,V3), r-{F}(V4,V2), #-{F} V5, #-{F} V6, V1 == V6, V2 == V6, V3 == V6, #-{F} V7, V1 == V7, V2 == V7, V3 == V7, V6 == V7 | P_s-{T}(V5,V1), P_s-{T}(V5,V2), P_s-{T}(V5,V3), P_s-{T}(V5,V6), P_s-{T}(V5,V7)
% 2.15/2.37 (used 0 times, uses = {})
% 2.15/2.37
% 2.15/2.37 #77: 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 == V20, V20 == V14, V14 == V22, V22 == V24; #60 ), references = 2, size of lhs = 21:
% 2.15/2.37 P_z-{F}(V0), r-{F}(V1,V0), r-{F}(V1,V2), V2 == V0, P_s-{F}(V3,V2), r-{F}(V4,V0), r-{F}(V4,V2), P_s-{F}(V5,V4), P_s-{F}(V6,V7), V4 == V7, V0 == V7, V2 == V7, #-{F} V8, V5 == V8, V3 == V8, V6 == V8, #-{F} V9, V4 == V9, V0 == V9, V2 == V9, V7 == V9 | P_s-{T}(V8,V9)
% 2.15/2.37 (used 0 times, uses = {})
% 2.15/2.37
% 2.15/2.37 #98: 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 == V20, V20 == V21; #79 ), references = 5, size of lhs = 20:
% 2.15/2.37 P_z-{F}(V0), r-{F}(V1,V0), P_s-{F}(V2,V1), P_s-{F}(V3,V4), V1 == V4, V4 == V0, P_s-{F}(V5,V6), V1 == V6, V0 == V6, V4 == V6, P_s-{F}(V7,V8), V1 == V8, V0 == V8, V4 == V8, V6 == V8, #-{F} V9, V2 == V9, V3 == V9, V5 == V9, V7 == V9 | b-{T}(V1,V4)
% 2.15/2.37 (used 0 times, uses = {})
% 2.15/2.37
% 2.15/2.37 #138: 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; #112 ), references = 1, size of lhs = 28:
% 2.15/2.37 P_z-{F}(V0), r-{F}(V1,V0), P_s-{F}(V2,V1), P_s-{F}(V3,V1), P_s-{F}(V4,V1), P_s-{F}(V5,V6), V1 == V6, V6 == V0, P_s-{F}(V7,V8), V1 == V8, V0 == V8, V6 == V8, P_s-{F}(V9,V10), V1 == V10, V10 == V0, V6 == V10, P_s-{F}(V11,V12), V1 == V12, V0 == V12, V10 == V12, P_s-{F}(V13,V14), V1 == V14, V0 == V14, P_s-{F}(V15,V16), V1 == V16, V0 == V16, V14 == V16, #-{F} V17 | P_s-{T}(V17,V1), P_s-{T}(V17,V0), P_s-{T}(V17,V6), P_s-{T}(V17,V8), P_s-{T}(V17,V10), P_s-{T}(V17,V12), P_s-{T}(V17,V14), P_s-{T}(V17,V16), P_s-{T}(V17,V2), P_s-{T}(V17,V5), P_s-{T}(V17,V7), P_s-{T}(V17,V17), P_s-{T}(V17,V3), P_s-{T}(V17,V9), P_s-{T}(V17,V11), P_s-{T}(V17,V4), P_s-{T}(V17,V13), P_s-{T}(V17,V15)
% 2.15/2.37 (used 0 times, uses = {})
% 2.15/2.37
% 2.15/2.37 #178: 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 == 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, V66 == V68; #139 ), references = 1, size of lhs = 55:
% 2.15/2.37 P_z-{F}(V0), 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), V1 == V7, V7 == V0, P_s-{F}(V8,V7), P_s-{F}(V9,V8), P_s-{F}(V10,V11), V1 == V11, V0 == V11, V7 == V11, P_s-{F}(V12,V11), P_s-{F}(V13,V12), P_s-{F}(V14,V15), V1 == V15, V15 == V0, V7 == V15, P_s-{F}(V16,V15), P_s-{F}(V17,V16), P_s-{F}(V18,V19), V1 == V19, V0 == V19, V15 == V19, P_s-{F}(V20,V19), P_s-{F}(V21,V20), P_s-{F}(V22,V23), V1 == V23, V0 == V23, P_s-{F}(V24,V23), P_s-{F}(V25,V24), P_s-{F}(V26,V27), V1 == V27, V0 == V27, V23 == V27, P_s-{F}(V28,V27), P_s-{F}(V29,V28), P_s-{F}(V30,V31), V5 == V31, V6 == V31, V10 == V31, V14 == V31, V18 == V31, V22 == V31, V26 == V31, V9 == V31, V13 == V31, V30 == V31, V17 == V31, V21 == V31, V25 == V31, V29 == V31 | P_s-{T}(V31,V0), P_s-{T}(V31,V2), P_s-{T}(V31,V3), P_s-{T}(V31,V4)
% 2.15/2.37 (used 0 times, uses = {})
% 2.15/2.37
% 2.15/2.37 #220: 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 == V16, V16 == V17, V17 == V18, V18 == V20, V20 == 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 == V15, V15 == V19, V19 == V21, V21 == V40, V40 == V41; #179 ), references = 1, size of lhs = 54:
% 2.15/2.37 P_z-{F}(V0), P_s-{F}(V0,V1), r-{F}(V1,V0), P_s-{F}(V2,V1), P_s-{F}(V3,V1), P_s-{F}(V4,V5), V1 == V5, V5 == V0, P_s-{F}(V6,V5), P_s-{F}(V7,V6), P_s-{F}(V8,V9), V1 == V9, V0 == V9, V5 == V9, P_s-{F}(V10,V9), P_s-{F}(V11,V10), P_s-{F}(V12,V13), V1 == V13, V13 == V0, V5 == V13, P_s-{F}(V14,V13), P_s-{F}(V15,V14), P_s-{F}(V16,V17), V1 == V17, V0 == V17, V13 == V17, P_s-{F}(V18,V17), P_s-{F}(V19,V18), P_s-{F}(V20,V21), V1 == V21, V0 == V21, P_s-{F}(V22,V21), P_s-{F}(V23,V22), P_s-{F}(V24,V25), V1 == V25, V0 == V25, V21 == V25, P_s-{F}(V26,V25), P_s-{F}(V27,V26), P_s-{F}(V28,V29), V3 == V29, V4 == V29, V8 == V29, V12 == V29, V16 == V29, V20 == V29, V24 == V29, V7 == V29, V11 == V29, V28 == V29, V15 == V29, V19 == V29, V23 == V29, V27 == V29 | P_s-{T}(V29,V2)
% 2.15/2.37 (used 0 times, uses = {})
% 2.15/2.37
% 2.15/2.37 #264: 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 == V44, V44 == V45; #222 ), references = 1, size of lhs = 22:
% 2.15/2.37 P_z-{F}(V0), P_s-{F}(V0,V1), r-{F}(V1,V0), P_s-{F}(V2,V1), P_s-{F}(V3,V4), V1 == V4, V4 == V0, P_s-{F}(V5,V4), P_s-{F}(V6,V5), P_s-{F}(V7,V8), P_s-{F}(V9,V8), P_s-{F}(V10,V8), P_s-{F}(V11,V12), V1 == V12, V0 == V12, P_s-{F}(V13,V12), P_s-{F}(V14,V13), P_s-{F}(V15,V16), V1 == V16, V0 == V16, P_s-{F}(V17,V16), P_s-{F}(V18,V17) | P_s-{T}(V8,V1), P_s-{T}(V8,V0), P_s-{T}(V8,V4), P_s-{T}(V8,V12), P_s-{T}(V8,V16), P_s-{T}(V8,V2), P_s-{T}(V8,V3), P_s-{T}(V8,V8), P_s-{T}(V8,V11), P_s-{T}(V8,V15), P_s-{T}(V8,V6), P_s-{T}(V8,V7), P_s-{T}(V8,V9), P_s-{T}(V8,V14), P_s-{T}(V8,V18), P_s-{T}(V8,V10)
% 2.15/2.37 (used 0 times, uses = {})
% 2.15/2.37
% 2.15/2.37 #318: 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 == V42, V42 == V43, V43 == V60, V60 == V62, V62 == V64, V64 == V66, V66 == V68, V68 == V70, V70 == V72, V72 == V74, V74 == V76, V76 == V78, V78 == V80; #265 ), references = 1, size of lhs = 44:
% 2.15/2.37 P_z-{F}(V0), P_s-{F}(V0,V1), r-{F}(V1,V0), P_s-{F}(V2,V1), P_s-{F}(V3,V1), P_s-{F}(V4,V5), P_s-{F}(V5,V6), V1 == V6, V6 == V0, P_s-{F}(V7,V6), P_s-{F}(V8,V6), P_s-{F}(V9,V8), P_s-{F}(V10,V11), P_s-{F}(V11,V12), V1 == V12, V0 == V12, P_s-{F}(V13,V12), P_s-{F}(V14,V12), P_s-{F}(V15,V14), P_s-{F}(V16,V17), P_s-{F}(V17,V18), V1 == V18, V0 == V18, P_s-{F}(V19,V18), P_s-{F}(V20,V18), P_s-{F}(V21,V20), P_s-{F}(V22,V23), V3 == V23, V7 == V23, V13 == V23, V19 == V23, V9 == V23, V22 == V23, V15 == V23, V21 == V23, P_s-{F}(V24,V23), P_s-{F}(V25,V24), V25 == V23, P_s-{F}(V26,V23), P_s-{F}(V27,V26), V27 == V23, P_s-{F}(V28,V23), P_s-{F}(V29,V28), V29 == V23 | P_s-{T}(V23,V0), P_s-{T}(V23,V2), P_s-{T}(V23,V4), P_s-{T}(V23,V10), P_s-{T}(V23,V16)
% 2.15/2.37 (used 0 times, uses = {})
% 2.15/2.37
% 2.15/2.37 #378: 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 == V39, V39 == V36, V36 == V37, V37 == V38, V38 == V42, V42 == V43, V43 == V44, V44 == V46, V46 == V47, V47 == V48, V48 == V49, V49 == V50, V50 == V51, V51 == V52, V52 == V53, V53 == V54, V54 == V55, V55 == V41, V41 == V56, V40 == V57, V56 == V62, V57 == V63, V58 == V64; #319 ), references = 1, size of lhs = 38:
% 2.15/2.37 P_z-{F}(V0), P_s-{F}(V0,V1), r-{F}(V1,V0), P_s-{F}(V2,V1), P_s-{F}(V1,V3), V1 == V3, V0 == V3, P_s-{F}(V4,V3), P_s-{F}(V5,V3), P_s-{F}(V6,V3), P_s-{F}(V7,V6), P_s-{F}(V8,V3), P_s-{F}(V9,V8), P_s-{F}(V10,V11), P_s-{F}(V11,V12), V1 == V12, V0 == V12, P_s-{F}(V13,V12), P_s-{F}(V14,V12), P_s-{F}(V15,V14), P_s-{F}(V16,V17), V2 == V17, V4 == V17, V5 == V17, V13 == V17, V7 == V17, V16 == V17, V9 == V17, V15 == 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-{T}(V17,V10)
% 2.15/2.37 (used 0 times, uses = {})
% 2.15/2.37
% 2.15/2.37 #441: 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 == V2, V2 == V40, V40 == V41, V41 == V42, V42 == V44, V44 == V45, V45 == V46, V46 == V47, V47 == V48, V48 == V49, V49 == V50, V50 == V51, V51 == V52, V52 == V53, V53 == V54, V54 == V55, V1 == V56, V55 == V59, V56 == V60, V57 == V61, V59 == V63, V60 == V64, V61 == V65; #380 ), references = 2, size of lhs = 34:
% 2.15/2.37 P_z-{F}(V0), P_s-{F}(V0,V1), V1 == V0, P_s-{F}(V2,V1), P_s-{F}(V1,V3), V1 == V3, V0 == V3, P_s-{F}(V4,V3), P_s-{F}(V5,V3), P_s-{F}(V6,V3), P_s-{F}(V7,V3), P_s-{F}(V8,V7), P_s-{F}(V9,V3), P_s-{F}(V10,V9), P_s-{F}(V11,V3), P_s-{F}(V12,V11), P_s-{F}(V13,V14), V2 == V14, V4 == V14, V5 == V14, V6 == V14, V8 == V14, V13 == V14, V10 == V14, V12 == V14, P_s-{F}(V15,V14), P_s-{F}(V16,V15), V16 == V14, P_s-{F}(V17,V14), P_s-{F}(V18,V17), V18 == V14, P_s-{F}(V19,V14), P_s-{F}(V20,V19), V20 == V14 | b-{T}(V1,V0)
% 2.15/2.37 (used 0 times, uses = {})
% 2.15/2.37
% 2.15/2.37 #453: mergings( V2 == V3, V3 == V4, V4 == V5, V5 == V6, V6 == V7; #447 ), references = 1, size of lhs = 21:
% 2.15/2.37 P_z-{F}(V0), r-{F}(V1,V0), P_s-{F}(V2,V1), P_s-{F}(V3,V1), b-{F}(V1,V4), P_s-{F}(V5,V6), V1 == V6, V0 == V6, P_s-{F}(V7,V8), V1 == V8, V0 == V8, V6 == V8, P_s-{F}(V9,V10), V1 == V10, V10 == V0, V4 == V10, P_s-{F}(V11,V12), V1 == V12, V0 == V12, V10 == V12, #-{F} V13 | P_s-{T}(V13,V1), P_s-{T}(V13,V0), P_s-{T}(V13,V4), P_s-{T}(V13,V6), P_s-{T}(V13,V8), P_s-{T}(V13,V10), P_s-{T}(V13,V12), P_s-{T}(V13,V2), P_s-{T}(V13,V13), P_s-{T}(V13,V5), P_s-{T}(V13,V7), P_s-{T}(V13,V3), P_s-{T}(V13,V9), P_s-{T}(V13,V11)
% 2.15/2.37 (used 0 times, uses = {})
% 2.15/2.37
% 2.15/2.37 #471: mergings( V0 == V1, V1 == V2, V2 == V3, V3 == V4, V4 == V5, V5 == V19, V19 == V21, V21 == V23, V23 == V25, V25 == V27, V27 == V29, V29 == V31, V31 == V33, V33 == V35, V35 == V37, V37 == V39; #454 ), references = 1, size of lhs = 42:
% 2.15/2.37 P_z-{F}(V0), r-{F}(V1,V0), b-{F}(V1,V2), P_s-{F}(V3,V1), P_s-{F}(V4,V2), P_s-{F}(V5,V1), P_s-{F}(V6,V5), P_s-{F}(V7,V1), P_s-{F}(V8,V7), P_s-{F}(V9,V10), V1 == V10, V0 == V10, P_s-{F}(V11,V10), P_s-{F}(V12,V13), V1 == V13, V0 == V13, P_s-{F}(V14,V13), P_s-{F}(V15,V16), V1 == V16, V0 == V16, V16 == V10, P_s-{F}(V17,V16), P_s-{F}(V18,V17), P_s-{F}(V19,V20), V1 == V20, V20 == V0, V2 == V20, V20 == V13, P_s-{F}(V21,V20), P_s-{F}(V22,V21), P_s-{F}(V23,V24), V3 == V24, V4 == V24, V15 == V24, V11 == V24, V19 == V24, V14 == V24, V6 == V24, V23 == V24, V18 == V24, V8 == V24, V22 == V24 | P_s-{T}(V24,V0), P_s-{T}(V24,V9), P_s-{T}(V24,V12)
% 2.15/2.37 (used 0 times, uses = {})
% 2.15/2.37
% 2.15/2.37 #490: 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 == V0, V0 == V1, V1 == V25; #472 ), references = 1, size of lhs = 42:
% 2.15/2.37 P_z-{F}(V0), P_s-{F}(V0,V1), V0 == V1, P_s-{F}(V2,V1), r-{F}(V3,V0), V3 == V1, b-{F}(V3,V4), P_s-{F}(V5,V3), P_s-{F}(V6,V4), P_s-{F}(V7,V3), P_s-{F}(V8,V7), P_s-{F}(V9,V3), P_s-{F}(V10,V9), P_s-{F}(V11,V12), V3 == V12, V0 == V12, P_s-{F}(V13,V12), P_s-{F}(V14,V15), V3 == V15, V0 == V15, V15 == V1, P_s-{F}(V16,V15), P_s-{F}(V17,V16), P_s-{F}(V18,V19), V3 == V19, V19 == V0, V4 == V19, V19 == V12, P_s-{F}(V20,V19), P_s-{F}(V21,V20), P_s-{F}(V22,V23), V5 == V23, V6 == V23, V14 == V23, V2 == V23, V18 == V23, V13 == V23, V8 == V23, V22 == V23, V17 == V23, V10 == V23, V21 == V23 | P_s-{T}(V23,V11)
% 2.15/2.37 (used 0 times, uses = {})
% 2.15/2.37
% 2.15/2.37 #513: 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 == V23, V21 == V24; #492 ), references = 2, size of lhs = 39:
% 2.15/2.37 P_z-{F}(V0), P_s-{F}(V0,V1), V0 == V1, P_s-{F}(V2,V1), P_s-{F}(V3,V1), r-{F}(V4,V0), V4 == V1, P_s-{F}(V5,V4), P_s-{F}(V6,V4), P_s-{F}(V7,V6), P_s-{F}(V8,V4), P_s-{F}(V9,V8), P_s-{F}(V10,V11), V4 == V11, P_s-{F}(V12,V13), V4 == V13, V0 == V13, V13 == V1, P_s-{F}(V14,V13), P_s-{F}(V15,V14), P_s-{F}(V16,V17), V4 == V17, V17 == V0, V11 == V17, V17 == V1, P_s-{F}(V18,V17), P_s-{F}(V19,V18), P_s-{F}(V20,V21), V5 == V21, V10 == V21, V12 == V21, V2 == V21, V16 == V21, V3 == V21, V7 == V21, V20 == V21, V15 == V21, V9 == V21, V19 == V21 | r-{T}(V4,V11)
% 2.15/2.37 (used 0 times, uses = {})
% 2.15/2.37
% 2.15/2.37 #517: mergings( V2 == V6; #515 ), references = 1, size of lhs = 13:
% 2.15/2.37 P_z-{F}(V0), r-{F}(V1,V0), r-{F}(V1,V2), V2 == V0, P_s-{F}(V3,V2), r-{F}(V4,V0), r-{F}(V4,V2), P_s-{F}(V5,V4), P_s-{F}(V6,V7), V4 == V7, V0 == V7, V2 == V7, #-{F} V8 | P_s-{T}(V8,V4), P_s-{T}(V8,V0), P_s-{T}(V8,V2), P_s-{T}(V8,V7), P_s-{T}(V8,V5), P_s-{T}(V8,V3), P_s-{T}(V8,V8), P_s-{T}(V8,V6)
% 2.15/2.37 (used 0 times, uses = {})
% 2.15/2.37
% 2.15/2.37 #526: mergings( V0 == V4, V4 == V10, V10 == V12, V12 == V14, V14 == V16, V16 == V18, V18 == V20; #518 ), references = 1, size of lhs = 24:
% 2.15/2.37 P_z-{F}(V0), r-{F}(V1,V0), r-{F}(V1,V2), V2 == V0, P_s-{F}(V3,V2), P_s-{F}(V4,V2), r-{F}(V5,V0), r-{F}(V5,V2), P_s-{F}(V6,V5), P_s-{F}(V7,V5), P_s-{F}(V8,V7), P_s-{F}(V9,V10), V5 == V10, V0 == V10, V2 == V10, P_s-{F}(V11,V10), P_s-{F}(V12,V11), P_s-{F}(V13,V14), V6 == V14, V4 == V14, V9 == V14, V8 == V14, V13 == V14, V12 == V14 | P_s-{T}(V14,V0), P_s-{T}(V14,V3)
% 2.15/2.37 (used 0 times, uses = {})
% 2.15/2.37
% 2.15/2.37 #535: mergings( V4 == V5, V5 == V6, V6 == V8, V8 == V9, V9 == V10, V10 == V11, V11 == V0; #527 ), references = 2, size of lhs = 24:
% 2.15/2.37 P_z-{F}(V0), r-{F}(V1,V0), r-{F}(V1,V2), V2 == V0, P_s-{F}(V3,V2), P_s-{F}(V4,V2), r-{F}(V5,V0), r-{F}(V5,V2), P_s-{F}(V6,V5), P_s-{F}(V7,V5), P_s-{F}(V8,V7), P_s-{F}(V9,V10), V5 == V10, V0 == V10, V2 == V10, P_s-{F}(V11,V10), P_s-{F}(V12,V11), P_s-{F}(V13,V14), V6 == V14, V4 == V14, V9 == V14, V8 == V14, V13 == V14, V12 == V14 | P_s-{T}(V14,V3)
% 2.15/2.37 (used 0 times, uses = {})
% 2.15/2.37
% 2.15/2.37 #570: 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 == V23, V21 == V24, V23 == V26, V26 == V27, V27 == V28, V28 == V29, V29 == V30, V30 == V31, V31 == V32, V32 == V33, V33 == V34, V24 == V35; #539 ), references = 3, size of lhs = 56:
% 2.15/2.37 P_z-{F}(V0), b-{F}(V1,V0), P_s-{F}(V0,V2), V2 == V0, P_s-{F}(V3,V2), P_s-{F}(V4,V2), P_s-{F}(V5,V2), P_s-{F}(V6,V2), P_s-{F}(V7,V8), V1 == V8, V8 == V0, V8 == V2, P_s-{F}(V9,V8), P_s-{F}(V10,V8), P_s-{F}(V11,V10), P_s-{F}(V12,V8), P_s-{F}(V13,V12), P_s-{F}(V14,V8), P_s-{F}(V15,V14), P_s-{F}(V16,V17), V8 == V17, V0 == V17, V17 == V2, P_s-{F}(V18,V17), P_s-{F}(V19,V18), P_s-{F}(V20,V21), V8 == V21, V21 == V0, V21 == V2, P_s-{F}(V22,V21), P_s-{F}(V23,V22), P_s-{F}(V24,V25), V7 == V25, V5 == V25, V16 == V25, V3 == V25, V20 == V25, V4 == V25, V11 == V25, V24 == V25, V19 == V25, V13 == V25, V23 == V25, P_s-{F}(V26,V27), V8 == V27, V0 == V27, V2 == V27, P_s-{F}(V28,V27), P_s-{F}(V29,V28), P_s-{F}(V30,V31), V9 == V31, V6 == V31, V26 == V31, V15 == V31, V30 == V31, V29 == V31 | r-{T}(V1,V8)
% 2.15/2.37 (used 0 times, uses = {})
% 2.15/2.37
% 2.15/2.37 #575: mergings( V0 == V2, V2 == V8; #572 ), references = 1, size of lhs = 58:
% 2.15/2.37 P_z-{F}(V0), P_s-{F}(V0,V1), V1 == V0, P_s-{F}(V2,V1), P_s-{F}(V3,V1), P_s-{F}(V4,V1), P_s-{F}(V5,V1), r-{F}(V6,V7), V7 == V0, r-{F}(V6,V8), V7 == V8, V8 == V0, V8 == V1, P_s-{F}(V9,V8), P_s-{F}(V10,V8), P_s-{F}(V11,V8), P_s-{F}(V12,V11), P_s-{F}(V13,V8), P_s-{F}(V14,V13), P_s-{F}(V15,V8), P_s-{F}(V16,V15), P_s-{F}(V17,V18), V8 == V18, V0 == V18, V18 == V1, P_s-{F}(V19,V18), P_s-{F}(V20,V19), P_s-{F}(V21,V22), V8 == V22, V22 == V0, V22 == V1, P_s-{F}(V23,V22), P_s-{F}(V24,V23), P_s-{F}(V25,V26), V9 == V26, V4 == V26, V17 == V26, V2 == V26, V21 == V26, V3 == V26, V12 == V26, V25 == V26, V20 == V26, V14 == V26, V24 == V26, P_s-{F}(V27,V28), V8 == V28, V0 == V28, V1 == V28, P_s-{F}(V29,V28), P_s-{F}(V30,V29), P_s-{F}(V31,V32), V10 == V32, V5 == V32, V27 == V32, V16 == V32, V31 == V32, V30 == V32 | r-{T}(V7,V0)
% 2.15/2.37 (used 0 times, uses = {})
% 2.15/2.37
% 2.15/2.37 #621: mergings( V48 == V53, 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 == V23, V21 == V24, V23 == V26, V26 == V27, V27 == V28, V28 == V29, V29 == V30, V30 == V31, V31 == V32, V32 == V33, V33 == V35, V24 == V36, V35 == V39, V36 == V40, V39 == V45, V45 == V46, V46 == V47, V40 == V53, V47 == V56, V53 == V57; #581 ), references = 1, size of lhs = 81:
% 2.15/2.37 P_z-{F}(V0), b-{F}(V1,V0), P_s-{F}(V0,V2), V2 == V0, P_s-{F}(V3,V2), P_s-{F}(V4,V2), P_s-{F}(V5,V2), P_s-{F}(V6,V2), P_s-{F}(V7,V2), P_s-{F}(V8,V2), P_s-{F}(V9,V2), P_s-{F}(V10,V2), P_s-{F}(V11,V2), P_s-{F}(V12,V2), P_s-{F}(V13,V2), P_s-{F}(V14,V2), P_s-{F}(V15,V2), P_s-{F}(V16,V2), P_s-{F}(V17,V2), P_s-{F}(V18,V2), P_s-{F}(V19,V20), V1 == V20, V20 == V0, V20 == V2, P_s-{F}(V21,V20), P_s-{F}(V22,V20), P_s-{F}(V23,V20), P_s-{F}(V24,V20), P_s-{F}(V25,V24), P_s-{F}(V26,V20), P_s-{F}(V27,V26), P_s-{F}(V28,V20), P_s-{F}(V29,V28), P_s-{F}(V30,V20), P_s-{F}(V31,V30), P_s-{F}(V32,V20), P_s-{F}(V33,V32), P_s-{F}(V34,V20), P_s-{F}(V35,V34), P_s-{F}(V36,V37), P_s-{F}(V38,V37), P_s-{F}(V39,V37), P_s-{F}(V40,V37), P_s-{F}(V41,V37), P_s-{F}(V42,V37), P_s-{F}(V43,V37), P_s-{F}(V44,V37), P_s-{F}(V45,V37), P_s-{F}(V46,V37), P_s-{F}(V47,V37), P_s-{F}(V48,V37), P_s-{F}(V49,V50), V0 == V50, V50 == V2, P_s-{F}(V51,V50), P_s-{F}(V52,V51), P_s-{F}(V53,V54), V54 == V0, V54 == V2, P_s-{F}(V55,V54), P_s-{F}(V56,V55), P_s-{F}(V57,V58), V0 == V58, V2 == V58, P_s-{F}(V59,V58), P_s-{F}(V60,V59), P_s-{F}(V61,V62), V0 == V62, V62 == V2, P_s-{F}(V63,V62), P_s-{F}(V64,V63), P_s-{F}(V65,V66), V66 == V0, V66 == V2, P_s-{F}(V67,V66), P_s-{F}(V68,V67), P_s-{F}(V69,V70), V0 == V70, V2 == V70, P_s-{F}(V71,V70), P_s-{F}(V72,V71) | P_s-{T}(V37,V20), P_s-{T}(V37,V0), P_s-{T}(V37,V2), P_s-{T}(V37,V19), P_s-{T}(V37,V5), P_s-{T}(V37,V37), P_s-{T}(V37,V3), P_s-{T}(V37,V4), P_s-{T}(V37,V25), P_s-{T}(V37,V36), P_s-{T}(V37,V27), P_s-{T}(V37,V38), P_s-{T}(V37,V21), P_s-{T}(V37,V6), P_s-{T}(V37,V29), P_s-{T}(V37,V39), P_s-{T}(V37,V1), P_s-{T}(V37,V50), P_s-{T}(V37,V54), P_s-{T}(V37,V9), P_s-{T}(V37,V49), P_s-{T}(V37,V7), P_s-{T}(V37,V53), P_s-{T}(V37,V8), P_s-{T}(V37,V40), P_s-{T}(V37,V52), P_s-{T}(V37,V41), P_s-{T}(V37,V56), P_s-{T}(V37,V58), P_s-{T}(V37,V10), P_s-{T}(V37,V57), P_s-{T}(V37,V42), P_s-{T}(V37,V60), P_s-{T}(V37,V62), P_s-{T}(V37,V66), P_s-{T}(V37,V13), P_s-{T}(V37,V61), P_s-{T}(V37,V11), P_s-{T}(V37,V65), P_s-{T}(V37,V12), P_s-{T}(V37,V43), P_s-{T}(V37,V64), P_s-{T}(V37,V44), P_s-{T}(V37,V68), P_s-{T}(V37,V70), P_s-{T}(V37,V14), P_s-{T}(V37,V69), P_s-{T}(V37,V45), P_s-{T}(V37,V72), P_s-{T}(V37,V22), P_s-{T}(V37,V17), P_s-{T}(V37,V15), P_s-{T}(V37,V16), P_s-{T}(V37,V31), P_s-{T}(V37,V46), P_s-{T}(V37,V33), P_s-{T}(V37,V47), P_s-{T}(V37,V23), P_s-{T}(V37,V18), P_s-{T}(V37,V35), P_s-{T}(V37,V48)
% 2.15/2.37 (used 0 times, uses = {})
% 2.15/2.37
% 2.15/2.37 #745: mergings( V46 == V51, 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 == V21, V19 == V22, V21 == V24, V24 == V25, V25 == V26, V26 == V27, V27 == V28, V28 == V29, V29 == V30, V30 == V33, V22 == V34, V33 == V43, V43 == V44, V44 == V54, V34 == V55, V54 == V112, V112 == V31, V31 == V114, V114 == V116, V116 == V118, V118 == V120, V120 == V35, V35 == V122, V122 == V20, V20 == V23, V23 == V64, V55 == V63, V64 == V124, V124 == V66, V63 == V65, V66 == V126, V126 == V128, V128 == V36, V36 == V68, V65 == V67, V68 == V130, V130 == V132, V132 == V37, V67 == V38, V37 == V134, V134 == V45, V38 == V51, V45 == V136, V136 == V138, V138 == V140, V140 == V41, V41 == V142, V142 == V39, V39 == V144, V144 == V40, V40 == V146, V146 == V91, V51 == V90, V59 == V89, V91 == V148, V148 == V95, V90 == V94, V89 == V93, V95 == V150, V150 == V42, V42 == V152, V152 == V154, V154 == V99, V94 == V98, V93 == V97, V99 == V156, V156 == V158, V158 == V49, V49 == V160, V160 == V47, V47 == V162, V162 == V48, V48 == V164, V164 == V103, V98 == V102, V97 == V101, V103 == V166, V166 == V107, V102 == V106, V101 == V105, V107 == V168, V168 == V50, V50 == V170, V170 == V172, V172 == V111, V106 == V110, V105 == V109, V111 == V174, V174 == V176, V176 == V178, V178 == V56, V56 == V52, V52 == V53, V53 == V70, V110 == V69, V70 == V180, V180 == V72, V69 == V71, V72 == V182, V182 == V184, V184 == V57, V57 == V74, V71 == V73; #622 ), references = 2, size of lhs = 104:
% 2.15/2.37 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}(V1,V9), V0 == V9, V1 == V9, P_s-{F}(V10,V9), P_s-{F}(V11,V9), P_s-{F}(V12,V9), P_s-{F}(V13,V9), P_s-{F}(V14,V9), P_s-{F}(V15,V9), P_s-{F}(V16,V9), b-{F}(V17,V0), V17 == V9, P_s-{F}(V18,V17), P_s-{F}(V19,V9), P_s-{F}(V20,V19), P_s-{F}(V21,V9), P_s-{F}(V22,V21), P_s-{F}(V23,V9), P_s-{F}(V24,V23), P_s-{F}(V25,V9), P_s-{F}(V26,V25), P_s-{F}(V27,V9), P_s-{F}(V28,V27), P_s-{F}(V29,V9), P_s-{F}(V30,V29), P_s-{F}(V31,V9), P_s-{F}(V32,V31), P_s-{F}(V33,V9), P_s-{F}(V34,V33), P_s-{F}(V35,V9), P_s-{F}(V36,V35), P_s-{F}(V37,V9), P_s-{F}(V38,V37), P_s-{F}(V39,V40), V10 == V40, V2 == V40, V3 == V40, V4 == V40, V20 == V40, V22 == V40, V18 == V40, V5 == V40, V6 == V40, V11 == V40, V12 == V40, V28 == V40, V30 == V40, V13 == V40, V32 == V40, V14 == V40, V15 == V40, V34 == V40, V36 == V40, V16 == V40, V38 == V40, V7 == V40, V8 == V40, V24 == V40, V26 == V40, P_s-{F}(V41,V40), V41 == V40, P_s-{F}(V42,V40), P_s-{F}(V43,V42), V43 == V40, P_s-{F}(V44,V40), P_s-{F}(V45,V44), V45 == V40, P_s-{F}(V46,V40), P_s-{F}(V47,V46), V47 == V40, P_s-{F}(V48,V40), P_s-{F}(V49,V48), V49 == V40, P_s-{F}(V50,V40), P_s-{F}(V51,V50), V51 == V40, P_s-{F}(V52,V40), P_s-{F}(V53,V52), V53 == V40, P_s-{F}(V54,V40), P_s-{F}(V55,V54), V55 == V40, P_s-{F}(V56,V40), P_s-{F}(V57,V56), V57 == V40, P_s-{F}(V58,V40), P_s-{F}(V59,V58), V59 == V40, P_s-{F}(V60,V40), P_s-{F}(V61,V60), V61 == V40, P_s-{F}(V62,V40), P_s-{F}(V63,V62), V63 == V40 | P_s-{T}(V40,V39)
% 2.15/2.37 (used 0 times, uses = {})
% 2.15/2.37
% 2.15/2.37 #756: mergings( V2 == V11; #754 ), references = 1, size of lhs = 40:
% 2.15/2.37 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-{T}(V1,V1), P_s-{T}(V1,V0), P_s-{T}(V1,V2), P_s-{T}(V1,V11), P_s-{T}(V1,V12), P_s-{T}(V1,V13), P_s-{T}(V1,V24), P_s-{T}(V1,V25), P_s-{T}(V1,V26), P_s-{T}(V1,V3), P_s-{T}(V1,V4), P_s-{T}(V1,V5), P_s-{T}(V1,V14), P_s-{T}(V1,V15), P_s-{T}(V1,V10), P_s-{T}(V1,V6), P_s-{T}(V1,V7), P_s-{T}(V1,V18), P_s-{T}(V1,V19), P_s-{T}(V1,V20), P_s-{T}(V1,V21), P_s-{T}(V1,V22), P_s-{T}(V1,V23), P_s-{T}(V1,V8), P_s-{T}(V1,V9), P_s-{T}(V1,V16), P_s-{T}(V1,V17), P_s-{T}(V1,V27), P_s-{T}(V1,V28), P_s-{T}(V1,V29), P_s-{T}(V1,V30), P_s-{T}(V1,V31), P_s-{T}(V1,V32), 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)
% 2.15/2.37 (used 0 times, uses = {})
% 2.15/2.37
% 2.15/2.37 #796: mergings( V10 == V0, V0 == V2, V2 == V12, V12 == V13, V13 == V14, V14 == V25, V25 == V26, V26 == V27, V27 == V3, V3 == V4, V4 == V5, V5 == V15, V15 == V16, V16 == V11, V11 == V6, V6 == V7, V7 == V19, V19 == V20, V20 == V21, V21 == V22, V22 == V23, V23 == V24, V24 == V8, V8 == V9, V9 == V17, V17 == V18, V18 == V28, V28 == V29, V29 == V30, V30 == V31, V31 == V32, V32 == V33, V33 == V34, V34 == V35, V35 == V36, V36 == V37, V37 == V38, V38 == V39; #757 ), references = 1, size of lhs = 3:
% 2.15/2.37 P_z-{F}(V0), P_s-{F}(V0,V1), V0 == V1 | P_s-{T}(V1,V1)
% 2.15/2.37 (used 0 times, uses = {})
% 2.15/2.37
% 2.15/2.37 #801: mergings( V2 == V0, V0 == V3; #798 ), references = 1, size of lhs = 1:
% 2.15/2.37 P_z-{F}(V0) | P_s-{T}(V0,V0)
% 2.15/2.37 (used 0 times, uses = {})
% 2.15/2.37
% 2.15/2.37 #804: exists( #8, #802 ), references = 1, size of lhs = 0:
% 2.15/2.37 FALSE | FALSE
% 2.15/2.37 (used 0 times, uses = {})
% 2.15/2.37
% 2.15/2.37 number of learnt formulas = 29
% 2.15/2.37
% 2.15/2.37
% 2.15/2.37 % SZS output end Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 2.15/2.37
% 2.15/2.37 randbase = 1
%------------------------------------------------------------------------------