%------------------------------------------------------------------------------
% File : Geo-III---2018C
% Problem : NLP001-1 : TPTP v8.1.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : geo -tptp_input -nonempty -inputfile %s
% Computer : n004.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sat Jul 23 06:10:54 EDT 2022
% Result : Unsatisfiable 71.67s 71.83s
% Output : Refutation 71.67s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : NLP001-1 : TPTP v8.1.0. Released v2.4.0.
% 0.11/0.12 % Command : geo -tptp_input -nonempty -inputfile %s
% 0.12/0.33 % Computer : n004.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Fri Jul 22 20:59:21 EDT 2022
% 0.12/0.33 % CPUTime :
% 71.67/71.83 GeoParameters:
% 71.67/71.83
% 71.67/71.83 tptp_input = 1
% 71.67/71.83 tptp_output = 0
% 71.67/71.83 nonempty = 1
% 71.67/71.83 inputfile = /export/starexec/sandbox/benchmark/theBenchmark.p
% 71.67/71.83 includepath = /export/starexec/sandbox/solver/bin/../../benchmark/
% 71.67/71.83
% 71.67/71.83
% 71.67/71.83 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 71.67/71.83 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 71.67/71.83
% 71.67/71.83 RuleSystem INPUT:
% 71.67/71.83
% 71.67/71.83 Initial Rules:
% 71.67/71.83 #0: input, references = 4, size of lhs = 1:
% 71.67/71.83 P_skc15-{F}(V0) | hollywood-{T}(V0)
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #1: input, references = 4, size of lhs = 2:
% 71.67/71.83 P_skc15-{F}(V0), P_skc14-{F}(V1) | event-{T}(V1)
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #2: input, references = 4, size of lhs = 3:
% 71.67/71.83 P_skc15-{F}(V0), P_skc14-{F}(V1), P_skc13-{F}(V2) | street-{T}(V2)
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #3: input, references = 4, size of lhs = 4:
% 71.67/71.83 P_skc15-{F}(V0), P_skc14-{F}(V1), P_skc13-{F}(V2), P_skc12-{F}(V3) | old-{T}(V3)
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #4: input, references = 4, size of lhs = 5:
% 71.67/71.83 P_skc15-{F}(V0), P_skc14-{F}(V1), P_skc13-{F}(V2), P_skc12-{F}(V3), P_skc11-{F}(V4) | hollywood-{T}(V4)
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #5: input, references = 5, size of lhs = 6:
% 71.67/71.83 P_skc15-{F}(V0), P_skc14-{F}(V1), P_skc13-{F}(V2), P_skc12-{F}(V3), P_skc11-{F}(V4), P_skc10-{F}(V5) | event-{T}(V5)
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #6: input, references = 5, size of lhs = 7:
% 71.67/71.83 P_skc15-{F}(V0), P_skc14-{F}(V1), P_skc13-{F}(V2), P_skc12-{F}(V3), P_skc11-{F}(V4), P_skc10-{F}(V5), P_skc9-{F}(V6) | chevy-{T}(V6)
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #7: input, references = 6, size of lhs = 8:
% 71.67/71.83 P_skc15-{F}(V0), P_skc14-{F}(V1), P_skc13-{F}(V2), P_skc12-{F}(V3), P_skc11-{F}(V4), P_skc10-{F}(V5), P_skc9-{F}(V6), P_skc8-{F}(V7) | lonely-{T}(V7)
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #8: input, references = 6, size of lhs = 8:
% 71.67/71.83 P_skc15-{F}(V0), P_skc14-{F}(V1), P_skc13-{F}(V2), P_skc12-{F}(V3), P_skc11-{F}(V4), P_skc10-{F}(V5), P_skc9-{F}(V6), P_skc8-{F}(V7) | ssSkC0-{T}(), chevy-{T}(V3)
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #9: input, references = 6, size of lhs = 8:
% 71.67/71.83 P_skc15-{F}(V0), P_skc14-{F}(V1), P_skc13-{F}(V2), P_skc12-{F}(V3), P_skc11-{F}(V4), P_skc10-{F}(V5), P_skc9-{F}(V6), P_skc8-{F}(V7) | ssSkC0-{T}(), car-{T}(V3)
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #10: input, references = 6, size of lhs = 8:
% 71.67/71.83 P_skc15-{F}(V0), P_skc14-{F}(V1), P_skc13-{F}(V2), P_skc12-{F}(V3), P_skc11-{F}(V4), P_skc10-{F}(V5), P_skc9-{F}(V6), P_skc8-{F}(V7) | ssSkC0-{T}(), white-{T}(V3)
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #11: input, references = 6, size of lhs = 8:
% 71.67/71.83 P_skc15-{F}(V0), P_skc14-{F}(V1), P_skc13-{F}(V2), P_skc12-{F}(V3), P_skc11-{F}(V4), P_skc10-{F}(V5), P_skc9-{F}(V6), P_skc8-{F}(V7) | ssSkC0-{T}(), dirty-{T}(V3)
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #12: input, references = 5, size of lhs = 8:
% 71.67/71.83 P_skc15-{F}(V0), P_skc14-{F}(V1), P_skc13-{F}(V2), P_skc12-{F}(V3), P_skc11-{F}(V4), P_skc10-{F}(V5), P_skc9-{F}(V6), P_skc8-{F}(V7) | ssSkC0-{T}(), lonely-{T}(V2)
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #13: input, references = 7, size of lhs = 8:
% 71.67/71.83 P_skc15-{F}(V0), P_skc14-{F}(V1), P_skc13-{F}(V2), P_skc12-{F}(V3), P_skc11-{F}(V4), P_skc10-{F}(V5), P_skc9-{F}(V6), P_skc8-{F}(V7) | ssSkC0-{T}(), way-{T}(V2)
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #14: input, references = 7, size of lhs = 8:
% 71.67/71.83 P_skc15-{F}(V0), P_skc14-{F}(V1), P_skc13-{F}(V2), P_skc12-{F}(V3), P_skc11-{F}(V4), P_skc10-{F}(V5), P_skc9-{F}(V6), P_skc8-{F}(V7) | ssSkC0-{T}(), city-{T}(V0)
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #15: input, references = 28, size of lhs = 9:
% 71.67/71.83 P_skc15-{F}(V0), P_skc14-{F}(V1), P_skc13-{F}(V2), P_skc12-{F}(V3), P_skc11-{F}(V4), P_skc10-{F}(V5), P_skc9-{F}(V6), P_skc8-{F}(V7), ssSkC0-{F}() | street-{T}(V7)
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #16: input, references = 32, size of lhs = 9:
% 71.67/71.83 P_skc15-{F}(V0), P_skc14-{F}(V1), P_skc13-{F}(V2), P_skc12-{F}(V3), P_skc11-{F}(V4), P_skc10-{F}(V5), P_skc9-{F}(V6), P_skc8-{F}(V7), ssSkC0-{F}() | way-{T}(V7)
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #17: input, references = 27, size of lhs = 9:
% 71.67/71.83 P_skc15-{F}(V0), P_skc14-{F}(V1), P_skc13-{F}(V2), P_skc12-{F}(V3), P_skc11-{F}(V4), P_skc10-{F}(V5), P_skc9-{F}(V6), P_skc8-{F}(V7), ssSkC0-{F}() | old-{T}(V6)
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #18: input, references = 30, size of lhs = 9:
% 71.67/71.83 P_skc15-{F}(V0), P_skc14-{F}(V1), P_skc13-{F}(V2), P_skc12-{F}(V3), P_skc11-{F}(V4), P_skc10-{F}(V5), P_skc9-{F}(V6), P_skc8-{F}(V7), ssSkC0-{F}() | dirty-{T}(V6)
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #19: input, references = 29, size of lhs = 9:
% 71.67/71.83 P_skc15-{F}(V0), P_skc14-{F}(V1), P_skc13-{F}(V2), P_skc12-{F}(V3), P_skc11-{F}(V4), P_skc10-{F}(V5), P_skc9-{F}(V6), P_skc8-{F}(V7), ssSkC0-{F}() | white-{T}(V6)
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #20: input, references = 28, size of lhs = 9:
% 71.67/71.83 P_skc15-{F}(V0), P_skc14-{F}(V1), P_skc13-{F}(V2), P_skc12-{F}(V3), P_skc11-{F}(V4), P_skc10-{F}(V5), P_skc9-{F}(V6), P_skc8-{F}(V7), ssSkC0-{F}() | car-{T}(V6)
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #21: input, references = 27, size of lhs = 9:
% 71.67/71.83 P_skc15-{F}(V0), P_skc14-{F}(V1), P_skc13-{F}(V2), P_skc12-{F}(V3), P_skc11-{F}(V4), P_skc10-{F}(V5), P_skc9-{F}(V6), P_skc8-{F}(V7), ssSkC0-{F}() | city-{T}(V4)
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #22: input, references = 7, size of lhs = 8:
% 71.67/71.83 P_skc15-{F}(V0), P_skc14-{F}(V1), P_skc13-{F}(V2), P_skc12-{F}(V3), P_skc11-{F}(V4), P_skc10-{F}(V5), P_skc9-{F}(V6), P_skc8-{F}(V7) | ssSkC0-{T}(), barrel-{T}(V1,V3)
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #23: input, references = 7, size of lhs = 8:
% 71.67/71.83 P_skc15-{F}(V0), P_skc14-{F}(V1), P_skc13-{F}(V2), P_skc12-{F}(V3), P_skc11-{F}(V4), P_skc10-{F}(V5), P_skc9-{F}(V6), P_skc8-{F}(V7) | ssSkC0-{T}(), down-{T}(V1,V2)
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #24: input, references = 4, size of lhs = 8:
% 71.67/71.83 P_skc15-{F}(V0), P_skc14-{F}(V1), P_skc13-{F}(V2), P_skc12-{F}(V3), P_skc11-{F}(V4), P_skc10-{F}(V5), P_skc9-{F}(V6), P_skc8-{F}(V7) | ssSkC0-{T}(), in-{T}(V1,V0)
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #25: input, references = 36, size of lhs = 9:
% 71.67/71.83 P_skc15-{F}(V0), P_skc14-{F}(V1), P_skc13-{F}(V2), P_skc12-{F}(V3), P_skc11-{F}(V4), P_skc10-{F}(V5), P_skc9-{F}(V6), P_skc8-{F}(V7), ssSkC0-{F}() | barrel-{T}(V5,V6)
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #26: input, references = 36, size of lhs = 9:
% 71.67/71.83 P_skc15-{F}(V0), P_skc14-{F}(V1), P_skc13-{F}(V2), P_skc12-{F}(V3), P_skc11-{F}(V4), P_skc10-{F}(V5), P_skc9-{F}(V6), P_skc8-{F}(V7), ssSkC0-{F}() | down-{T}(V5,V7)
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #27: input, references = 36, size of lhs = 9:
% 71.67/71.83 P_skc15-{F}(V0), P_skc14-{F}(V1), P_skc13-{F}(V2), P_skc12-{F}(V3), P_skc11-{F}(V4), P_skc10-{F}(V5), P_skc9-{F}(V6), P_skc8-{F}(V7), ssSkC0-{F}() | in-{T}(V5,V4)
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #28: input, references = 4, size of lhs = 22:
% 71.67/71.83 P_skc15-{F}(V0), P_skc14-{F}(V1), P_skc13-{F}(V2), P_skc12-{F}(V3), P_skc11-{F}(V4), P_skc10-{F}(V5), P_skc9-{F}(V6), P_skc8-{F}(V7), old-{F}(V8), dirty-{F}(V8), white-{F}(V8), car-{F}(V8), chevy-{F}(V8), event-{F}(V9), barrel-{F}(V9,V8), in-{F}(V9,V10), city-{F}(V10), hollywood-{F}(V10), street-{F}(V11), way-{F}(V11), lonely-{F}(V11), down-{F}(V9,V11) | ssSkC0-{T}()
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #29: input, references = 37, size of lhs = 23:
% 71.67/71.83 P_skc15-{F}(V0), P_skc14-{F}(V1), P_skc13-{F}(V2), P_skc12-{F}(V3), P_skc11-{F}(V4), P_skc10-{F}(V5), P_skc9-{F}(V6), P_skc8-{F}(V7), ssSkC0-{F}(), chevy-{F}(V8), car-{F}(V8), white-{F}(V8), dirty-{F}(V8), old-{F}(V8), event-{F}(V9), barrel-{F}(V9,V8), in-{F}(V9,V10), city-{F}(V10), hollywood-{F}(V10), lonely-{F}(V11), way-{F}(V11), street-{F}(V11), down-{F}(V9,V11) | FALSE
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #30: input, references = 4, size of lhs = 0:
% 71.67/71.83 FALSE | EXISTS V0: P_skc15-{T}(V0)
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #31: input, references = 4, size of lhs = 0:
% 71.67/71.83 FALSE | EXISTS V0: P_skc14-{T}(V0)
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #32: input, references = 4, size of lhs = 0:
% 71.67/71.83 FALSE | EXISTS V0: P_skc13-{T}(V0)
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #33: input, references = 4, size of lhs = 0:
% 71.67/71.83 FALSE | EXISTS V0: P_skc12-{T}(V0)
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #34: input, references = 4, size of lhs = 0:
% 71.67/71.83 FALSE | EXISTS V0: P_skc11-{T}(V0)
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #35: input, references = 5, size of lhs = 0:
% 71.67/71.83 FALSE | EXISTS V0: P_skc10-{T}(V0)
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #36: input, references = 5, size of lhs = 0:
% 71.67/71.83 FALSE | EXISTS V0: P_skc9-{T}(V0)
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #37: input, references = 6, size of lhs = 0:
% 71.67/71.83 FALSE | EXISTS V0: P_skc8-{T}(V0)
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 number of initial rules = 38
% 71.67/71.83
% 71.67/71.83 Simplifiers:
% 71.67/71.83 #38: unsound, references = 3, size of lhs = 3:
% 71.67/71.83 P_skc15-{F}(V0), P_skc15-{F}(V1), V0 == V1 | FALSE
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #39: unsound, references = 3, size of lhs = 3:
% 71.67/71.83 P_skc14-{F}(V0), P_skc14-{F}(V1), V0 == V1 | FALSE
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #40: unsound, references = 3, size of lhs = 3:
% 71.67/71.83 P_skc13-{F}(V0), P_skc13-{F}(V1), V0 == V1 | FALSE
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #41: unsound, references = 3, size of lhs = 3:
% 71.67/71.83 P_skc12-{F}(V0), P_skc12-{F}(V1), V0 == V1 | FALSE
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #42: unsound, references = 3, size of lhs = 3:
% 71.67/71.83 P_skc11-{F}(V0), P_skc11-{F}(V1), V0 == V1 | FALSE
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #43: unsound, references = 3, size of lhs = 3:
% 71.67/71.83 P_skc10-{F}(V0), P_skc10-{F}(V1), V0 == V1 | FALSE
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #44: unsound, references = 3, size of lhs = 3:
% 71.67/71.83 P_skc9-{F}(V0), P_skc9-{F}(V1), V0 == V1 | FALSE
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #45: unsound, references = 3, size of lhs = 3:
% 71.67/71.83 P_skc8-{F}(V0), P_skc8-{F}(V1), V0 == V1 | FALSE
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 number of simplifiers = 8
% 71.67/71.83
% 71.67/71.83 Learnt:
% 71.67/71.83 #120: mergings( V0 == V8, V8 == V15, V15 == V22, V22 == V29, V29 == V36, V36 == V43, V43 == V50, V50 == V57, V57 == V65, V1 == V9, V9 == V16, V16 == V23, V23 == V30, V30 == V37, V37 == V44, V44 == V51, V51 == V58, V58 == V66, V2 == V10, V10 == V17, V17 == V24, V24 == V31, V31 == V38, V38 == V45, V45 == V52, V52 == V59, V59 == V67, V3 == V11, V11 == V18, V18 == V25, V25 == V32, V32 == V39, V39 == V46, V46 == V53, V53 == V60, V60 == V68, V4 == V12, V12 == V19, V19 == V26, V26 == V33, V33 == V47, V47 == V54, V54 == V61, V61 == V69, V5 == V13, V13 == V20, V20 == V27, V27 == V34, V34 == V40, V40 == V62, V62 == V70, V6 == V14, V14 == V21, V21 == V41, V41 == V48, V48 == V55, V55 == V63, V63 == V71, V7 == V28, V28 == V35, V35 == V42, V42 == V49, V49 == V56, V56 == V64, V64 == V72; #54 ), references = 1, size of lhs = 14:
% 71.67/71.83 chevy-{F}(V0), car-{F}(V0), old-{F}(V0), P_skc9-{F}(V0), lonely-{F}(V1), P_skc8-{F}(V1), hollywood-{F}(V2), P_skc11-{F}(V2), event-{F}(V3), P_skc10-{F}(V3), P_skc15-{F}(V4), P_skc14-{F}(V5), P_skc13-{F}(V6), P_skc12-{F}(V7) | white-{T}(V7)
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #187: mergings( V0 == V8, V8 == V15, V15 == V22, V22 == V29, V29 == V36, V36 == V43, V43 == V50, V50 == V58, V1 == V9, V9 == V16, V16 == V23, V23 == V30, V30 == V37, V37 == V44, V44 == V51, V51 == V59, V2 == V10, V10 == V17, V17 == V24, V24 == V31, V31 == V38, V38 == V45, V45 == V52, V52 == V60, V3 == V11, V11 == V18, V18 == V25, V25 == V32, V32 == V39, V39 == V46, V46 == V53, V53 == V61, V4 == V12, V12 == V19, V19 == V26, V26 == V40, V40 == V47, V47 == V54, V54 == V62, V5 == V13, V13 == V20, V20 == V27, V27 == V33, V33 == V55, V55 == V63, V6 == V14, V14 == V21, V21 == V34, V34 == V41, V41 == V48, V48 == V56, V56 == V64, V7 == V28, V28 == V35, V35 == V42, V42 == V49, V49 == V57, V57 == V65; #128 ), references = 1, size of lhs = 15:
% 71.67/71.83 chevy-{F}(V0), car-{F}(V0), white-{F}(V0), old-{F}(V0), P_skc9-{F}(V0), lonely-{F}(V1), P_skc8-{F}(V1), hollywood-{F}(V2), P_skc11-{F}(V2), event-{F}(V3), P_skc10-{F}(V3), P_skc15-{F}(V4), P_skc14-{F}(V5), P_skc13-{F}(V6), P_skc12-{F}(V7) | dirty-{T}(V7)
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #238: mergings( V0 == V8, V8 == V15, V15 == V22, V22 == V29, V29 == V36, V36 == V44, V1 == V9, V9 == V16, V16 == V23, V23 == V30, V30 == V37, V37 == V45, V2 == V10, V10 == V17, V17 == V24, V24 == V31, V31 == V38, V38 == V46, V3 == V11, V11 == V18, V18 == V25, V25 == V32, V32 == V39, V39 == V47, V4 == V12, V12 == V19, V19 == V26, V26 == V33, V33 == V40, V40 == V48, V5 == V13, V13 == V20, V20 == V41, V41 == V49, V6 == V14, V14 == V21, V21 == V27, V27 == V34, V34 == V42, V42 == V50, V7 == V28, V28 == V35, V35 == V43, V43 == V51; #193 ), references = 1, size of lhs = 17:
% 71.67/71.83 chevy-{F}(V0), car-{F}(V0), white-{F}(V0), dirty-{F}(V0), old-{F}(V0), P_skc9-{F}(V0), lonely-{F}(V1), P_skc8-{F}(V1), city-{F}(V2), hollywood-{F}(V2), P_skc11-{F}(V2), event-{F}(V3), P_skc10-{F}(V3), P_skc15-{F}(V4), P_skc14-{F}(V5), P_skc13-{F}(V6), P_skc12-{F}(V7) | down-{T}(V5,V6)
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #257: mergings( V0 == V8, V8 == V18, V1 == V9, V9 == V19, V2 == V10, V10 == V20, V3 == V11, V11 == V21, V4 == V12, V12 == V22, V5 == V13, V13 == V23, V6 == V14, V14 == V24, V7 == V15, V15 == V25; #240 ), references = 4, size of lhs = 31:
% 71.67/71.83 city-{F}(V0), hollywood-{F}(V0), P_skc15-{F}(V0), event-{F}(V1), P_skc14-{F}(V1), old-{F}(V2), dirty-{F}(V2), white-{F}(V2), car-{F}(V2), chevy-{F}(V2), barrel-{F}(V1,V2), street-{F}(V3), way-{F}(V3), lonely-{F}(V3), down-{F}(V1,V3), P_skc13-{F}(V4), P_skc12-{F}(V5), P_skc11-{F}(V6), P_skc10-{F}(V7), P_skc9-{F}(V8), P_skc8-{F}(V9), chevy-{F}(V10), car-{F}(V10), white-{F}(V10), dirty-{F}(V10), old-{F}(V10), barrel-{F}(V1,V10), lonely-{F}(V11), way-{F}(V11), street-{F}(V11), down-{F}(V1,V11) | ssSkC0-{T}()
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #332: mergings( V0 == V8, V8 == V15, V15 == V24, V24 == V33, V33 == V40, V40 == V47, V47 == V54, V54 == V61, V61 == V69, V1 == V16, V16 == V25, V25 == V34, V34 == V41, V41 == V48, V48 == V55, V55 == V62, V62 == V70, V2 == V9, V9 == V17, V17 == V26, V26 == V35, V35 == V42, V42 == V49, V49 == V56, V56 == V63, V63 == V71, V3 == V10, V10 == V18, V18 == V27, V27 == V36, V36 == V43, V43 == V50, V50 == V57, V57 == V64, V64 == V72, V4 == V11, V11 == V19, V19 == V28, V28 == V37, V37 == V44, V44 == V51, V51 == V58, V58 == V65, V65 == V73, V5 == V12, V12 == V20, V20 == V29, V29 == V38, V38 == V45, V45 == V66, V66 == V74, V6 == V13, V13 == V21, V21 == V30, V30 == V39, V39 == V46, V46 == V52, V52 == V59, V59 == V67, V67 == V75, V7 == V14, V14 == V22, V22 == V31, V31 == V53, V53 == V60, V60 == V68, V68 == V76; #264 ), references = 1, size of lhs = 33:
% 71.67/71.83 chevy-{F}(V0), car-{F}(V0), white-{F}(V0), dirty-{F}(V0), old-{F}(V0), P_skc12-{F}(V0), city-{F}(V1), hollywood-{F}(V1), P_skc15-{F}(V1), event-{F}(V2), P_skc14-{F}(V2), street-{F}(V3), way-{F}(V3), lonely-{F}(V3), down-{F}(V2,V3), lonely-{F}(V4), way-{F}(V4), street-{F}(V4), down-{F}(V2,V4), chevy-{F}(V5), car-{F}(V5), white-{F}(V5), dirty-{F}(V5), old-{F}(V5), P_skc9-{F}(V5), lonely-{F}(V6), P_skc8-{F}(V6), city-{F}(V7), hollywood-{F}(V7), P_skc11-{F}(V7), event-{F}(V8), P_skc10-{F}(V8), P_skc13-{F}(V9) | ssSkC0-{T}()
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #508: mergings( V8 == V15, V15 == V22, V22 == V29, V29 == V36, V36 == V43, V43 == V50, V50 == V58, V58 == V0, V0 == V72, V72 == V80, V80 == V88, V88 == V95, V95 == V102, V102 == V109, V109 == V116, V116 == V123, V123 == V131, V131 == V138, V138 == V145, V145 == V152, V152 == V159, V159 == V166, V1 == V16, V16 == V23, V23 == V30, V30 == V37, V37 == V44, V44 == V51, V51 == V65, V65 == V73, V73 == V81, V81 == V89, V89 == V96, V96 == V103, V103 == V110, V110 == V117, V117 == V124, V124 == V132, V132 == V139, V139 == V146, V146 == V153, V153 == V160, V160 == V167, V2 == V9, V9 == V17, V17 == V24, V24 == V31, V31 == V38, V38 == V45, V45 == V52, V52 == V59, V59 == V66, V66 == V74, V74 == V82, V82 == V90, V90 == V97, V97 == V104, V104 == V111, V111 == V118, V118 == V125, V125 == V133, V133 == V140, V140 == V147, V147 == V154, V154 == V161, V161 == V168, V3 == V10, V10 == V18, V18 == V25, V25 == V32, V32 == V39, V39 == V46, V46 == V53, V53 == V60, V60 == V67, V67 == V75, V75 == V83, V83 == V91, V91 == V98, V98 == V105, V105 == V112, V112 == V119, V119 == V126, V126 == V134, V134 == V141, V141 == V148, V148 == V155, V155 == V162, V162 == V169, V4 == V11, V11 == V19, V19 == V26, V26 == V33, V33 == V40, V40 == V54, V54 == V61, V61 == V166, V166 == V68, V68 == V76, V76 == V84, V84 == V92, V92 == V99, V99 == V106, V106 == V113, V113 == V127, V127 == V135, V135 == V142, V142 == V149, V149 == V156, V156 == V170, V5 == V12, V12 == V20, V20 == V27, V27 == V47, V47 == V55, V55 == V62, V62 == V69, V69 == V77, V77 == V85, V85 == V93, V93 == V100, V100 == V120, V120 == V128, V128 == V136, V136 == V143, V143 == V163, V163 == V171, V6 == V13, V13 == V21, V21 == V28, V28 == V34, V34 == V41, V41 == V48, V48 == V56, V56 == V63, V63 == V70, V70 == V78, V78 == V86, V86 == V94, V94 == V101, V101 == V107, V107 == V114, V114 == V121, V121 == V129, V129 == V137, V137 == V144, V144 == V150, V150 == V157, V157 == V164, V164 == V172, V7 == V14, V14 == V35, V35 == V42, V42 == V49, V49 == V57, V57 == V64, V64 == V71, V71 == V79, V79 == V87, V87 == V108, V108 == V115, V115 == V122, V122 == V130, V130 == V151, V151 == V158, V158 == V165, V165 == V173; #340 ), references = 1, size of lhs = 25:
% 71.67/71.83 lonely-{F}(V0), way-{F}(V0), street-{F}(V0), P_skc13-{F}(V0), chevy-{F}(V1), car-{F}(V1), white-{F}(V1), dirty-{F}(V1), old-{F}(V1), P_skc12-{F}(V1), hollywood-{F}(V2), P_skc15-{F}(V2), P_skc11-{F}(V2), event-{F}(V3), P_skc14-{F}(V3), chevy-{F}(V4), car-{F}(V4), white-{F}(V4), dirty-{F}(V4), old-{F}(V4), P_skc9-{F}(V4), lonely-{F}(V5), P_skc8-{F}(V5), event-{F}(V6), P_skc10-{F}(V6) | ssSkC0-{T}()
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #742: mergings( V0 == V15, V15 == V21, V21 == V28, V28 == V35, V35 == V42, V42 == V49, V49 == V56, V56 == V64, V64 == V71, V71 == V79, V79 == V87, V87 == V95, V95 == V102, V102 == V109, V109 == V116, V116 == V123, V123 == V130, V130 == V138, V138 == V145, V145 == V152, V152 == V159, V159 == V166, V166 == V173, V173 == V181, V181 == V188, V188 == V195, V195 == V202, V202 == V209, V209 == V216, V216 == V224, V1 == V8, V8 == V22, V22 == V29, V29 == V36, V36 == V43, V43 == V50, V50 == V57, V57 == V72, V72 == V80, V80 == V88, V88 == V96, V96 == V103, V103 == V110, V110 == V117, V117 == V124, V124 == V131, V131 == V139, V139 == V146, V146 == V153, V153 == V160, V160 == V167, V167 == V174, V174 == V182, V182 == V189, V189 == V196, V196 == V203, V203 == V210, V210 == V217, V217 == V225, V9 == V2, V2 == V23, V23 == V30, V30 == V37, V37 == V44, V44 == V51, V51 == V58, V58 == V65, V65 == V73, V73 == V81, V81 == V89, V89 == V97, V97 == V104, V104 == V111, V111 == V118, V118 == V125, V125 == V132, V132 == V140, V140 == V147, V147 == V154, V154 == V161, V161 == V168, V168 == V175, V175 == V183, V183 == V190, V190 == V197, V197 == V204, V204 == V211, V211 == V218, V218 == V226, V3 == V10, V10 == V16, V16 == V24, V24 == V31, V31 == V38, V38 == V45, V45 == V52, V52 == V59, V59 == V66, V66 == V74, V74 == V82, V82 == V90, V90 == V98, V98 == V105, V105 == V112, V112 == V119, V119 == V126, V126 == V133, V133 == V141, V141 == V148, V148 == V155, V155 == V162, V162 == V169, V169 == V176, V176 == V184, V184 == V191, V191 == V198, V198 == V205, V205 == V212, V212 == V219, V219 == V227, V4 == V11, V11 == V17, V17 == V25, V25 == V32, V32 == V39, V39 == V46, V46 == V60, V60 == V67, V67 == V224, V224 == V75, V75 == V83, V83 == V91, V91 == V99, V99 == V106, V106 == V113, V113 == V120, V120 == V134, V134 == V142, V142 == V149, V149 == V156, V156 == V163, V163 == V177, V177 == V185, V185 == V192, V192 == V206, V206 == V213, V213 == V220, V220 == V228, V5 == V12, V12 == V18, V18 == V26, V26 == V33, V33 == V53, V53 == V61, V61 == V68, V68 == V76, V76 == V84, V84 == V92, V92 == V100, V100 == V107, V107 == V127, V127 == V135, V135 == V143, V143 == V150, V150 == V170, V170 == V178, V178 == V186, V186 == V193, V193 == V199, V199 == V221, V221 == V229, V6 == V13, V13 == V19, V19 == V27, V27 == V34, V34 == V40, V40 == V47, V47 == V54, V54 == V62, V62 == V69, V69 == V77, V77 == V85, V85 == V93, V93 == V101, V101 == V108, V108 == V114, V114 == V121, V121 == V128, V128 == V136, V136 == V144, V144 == V151, V151 == V157, V157 == V164, V164 == V171, V171 == V179, V179 == V187, V187 == V194, V194 == V200, V200 == V207, V207 == V214, V214 == V222, V222 == V230, V7 == V14, V14 == V20, V20 == V41, V41 == V48, V48 == V55, V55 == V63, V63 == V70, V70 == V78, V78 == V86, V86 == V94, V94 == V115, V115 == V122, V122 == V129, V129 == V137, V137 == V158, V158 == V165, V165 == V172, V172 == V180, V180 == V201, V201 == V208, V208 == V215, V215 == V223, V223 == V231; #516 ), references = 1, size of lhs = 24:
% 71.67/71.83 lonely-{F}(V0), street-{F}(V0), P_skc13-{F}(V0), chevy-{F}(V1), car-{F}(V1), white-{F}(V1), dirty-{F}(V1), old-{F}(V1), P_skc12-{F}(V1), event-{F}(V2), P_skc14-{F}(V2), chevy-{F}(V3), car-{F}(V3), white-{F}(V3), dirty-{F}(V3), old-{F}(V3), P_skc9-{F}(V3), lonely-{F}(V4), P_skc8-{F}(V4), hollywood-{F}(V5), P_skc15-{F}(V5), P_skc11-{F}(V5), event-{F}(V6), P_skc10-{F}(V6) | ssSkC0-{T}()
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #1034: mergings( V0 == V8, V8 == V22, V22 == V28, V28 == V35, V35 == V42, V42 == V49, V49 == V56, V56 == V63, V63 == V71, V71 == V78, V78 == V86, V86 == V94, V94 == V102, V102 == V109, V109 == V116, V116 == V123, V123 == V130, V130 == V137, V137 == V145, V145 == V152, V152 == V159, V159 == V166, V166 == V173, V173 == V180, V180 == V188, V188 == V195, V195 == V202, V202 == V209, V209 == V216, V216 == V223, V223 == V231, V231 == V239, V239 == V246, V246 == V253, V253 == V260, V260 == V267, V267 == V274, V274 == V282, V1 == V9, V9 == V15, V15 == V29, V29 == V36, V36 == V43, V43 == V50, V50 == V57, V57 == V64, V64 == V79, V79 == V87, V87 == V95, V95 == V103, V103 == V110, V110 == V117, V117 == V124, V124 == V131, V131 == V138, V138 == V146, V146 == V153, V153 == V160, V160 == V167, V167 == V174, V174 == V181, V181 == V189, V189 == V196, V196 == V203, V203 == V210, V210 == V217, V217 == V224, V224 == V232, V232 == V240, V240 == V247, V247 == V254, V254 == V261, V261 == V268, V268 == V275, V275 == V283, V16 == V2, V2 == V30, V30 == V37, V37 == V44, V44 == V51, V51 == V58, V58 == V65, V65 == V72, V72 == V80, V80 == V88, V88 == V96, V96 == V104, V104 == V111, V111 == V118, V118 == V125, V125 == V132, V132 == V139, V139 == V147, V147 == V154, V154 == V161, V161 == V168, V168 == V175, V175 == V182, V182 == V190, V190 == V197, V197 == V204, V204 == V211, V211 == V218, V218 == V225, V225 == V233, V233 == V241, V241 == V248, V248 == V255, V255 == V262, V262 == V269, V269 == V276, V276 == V284, V3 == V10, V10 == V17, V17 == V23, V23 == V31, V31 == V38, V38 == V45, V45 == V52, V52 == V59, V59 == V66, V66 == V73, V73 == V81, V81 == V89, V89 == V97, V97 == V105, V105 == V112, V112 == V119, V119 == V126, V126 == V133, V133 == V140, V140 == V148, V148 == V155, V155 == V162, V162 == V169, V169 == V176, V176 == V183, V183 == V191, V191 == V198, V198 == V205, V205 == V212, V212 == V219, V219 == V226, V226 == V234, V234 == V242, V242 == V249, V249 == V256, V256 == V263, V263 == V270, V270 == V277, V277 == V285, V4 == V11, V11 == V18, V18 == V24, V24 == V32, V32 == V39, V39 == V46, V46 == V53, V53 == V67, V67 == V74, V74 == V282, V282 == V82, V82 == V90, V90 == V98, V98 == V106, V106 == V113, V113 == V120, V120 == V127, V127 == V141, V141 == V149, V149 == V156, V156 == V163, V163 == V170, V170 == V184, V184 == V192, V192 == V199, V199 == V213, V213 == V220, V220 == V227, V227 == V235, V235 == V243, V243 == V250, V250 == V264, V264 == V271, V271 == V278, V278 == V286, V5 == V12, V12 == V19, V19 == V25, V25 == V33, V33 == V40, V40 == V60, V60 == V68, V68 == V75, V75 == V83, V83 == V91, V91 == V99, V99 == V107, V107 == V114, V114 == V134, V134 == V142, V142 == V150, V150 == V157, V157 == V177, V177 == V185, V185 == V193, V193 == V200, V200 == V206, V206 == V228, V228 == V236, V236 == V244, V244 == V251, V251 == V257, V257 == V279, V279 == V287, V6 == V13, V13 == V20, V20 == V26, V26 == V34, V34 == V41, V41 == V47, V47 == V54, V54 == V61, V61 == V69, V69 == V76, V76 == V84, V84 == V92, V92 == V100, V100 == V108, V108 == V115, V115 == V121, V121 == V128, V128 == V135, V135 == V143, V143 == V151, V151 == V158, V158 == V164, V164 == V171, V171 == V178, V178 == V186, V186 == V194, V194 == V201, V201 == V207, V207 == V214, V214 == V221, V221 == V229, V229 == V237, V237 == V245, V245 == V252, V252 == V258, V258 == V265, V265 == V272, V272 == V280, V280 == V288, V7 == V14, V14 == V21, V21 == V27, V27 == V48, V48 == V55, V55 == V62, V62 == V70, V70 == V77, V77 == V85, V85 == V93, V93 == V101, V101 == V122, V122 == V129, V129 == V136, V136 == V144, V144 == V165, V165 == V172, V172 == V179, V179 == V187, V187 == V208, V208 == V215, V215 == V222, V222 == V230, V230 == V238, V238 == V259, V259 == V266, V266 == V273, V273 == V281, V281 == V289; #750 ), references = 1, size of lhs = 23:
% 71.67/71.83 street-{F}(V0), P_skc13-{F}(V0), chevy-{F}(V1), car-{F}(V1), white-{F}(V1), dirty-{F}(V1), old-{F}(V1), P_skc12-{F}(V1), event-{F}(V2), P_skc14-{F}(V2), chevy-{F}(V3), car-{F}(V3), white-{F}(V3), dirty-{F}(V3), old-{F}(V3), P_skc9-{F}(V3), lonely-{F}(V4), P_skc8-{F}(V4), hollywood-{F}(V5), P_skc15-{F}(V5), P_skc11-{F}(V5), event-{F}(V6), P_skc10-{F}(V6) | ssSkC0-{T}()
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #1516: mergings( V0 == V8, V8 == V15, V15 == V22, V22 == V29, V29 == V36, V36 == V43, V43 == V50, V50 == V56, V56 == V63, V63 == V71, V71 == V79, V79 == V86, V86 == V93, V93 == V100, V100 == V107, V107 == V114, V114 == V120, V120 == V127, V127 == V135, V135 == V143, V143 == V150, V150 == V164, V164 == V171, V171 == V178, V178 == V185, V185 == V191, V191 == V198, V198 == V205, V205 == V213, V213 == V219, V219 == V227, V227 == V235, V235 == V243, V243 == V250, V250 == V257, V257 == V263, V263 == V270, V270 == V277, V277 == V285, V285 == V292, V292 == V299, V299 == V305, V305 == V312, V312 == V319, V319 == V327, V327 == V334, V334 == V341, V341 == V348, V348 == V354, V354 == V361, V361 == V369, V369 == V377, V377 == V384, V384 == V391, V391 == V398, V398 == V404, V404 == V411, V411 == V419, V419 == V427, V427 == V434, V434 == V441, V441 == V448, V448 == V454, V454 == V461, V461 == V469, V1 == V9, V9 == V16, V16 == V23, V23 == V30, V30 == V37, V37 == V44, V44 == V51, V51 == V57, V57 == V64, V64 == V72, V72 == V80, V80 == V87, V87 == V94, V94 == V101, V101 == V108, V108 == V115, V115 == V121, V121 == V128, V128 == V136, V136 == V144, V144 == V151, V151 == V157, V157 == V172, V172 == V179, V179 == V186, V186 == V192, V192 == V199, V199 == V206, V206 == V220, V220 == V228, V228 == V236, V236 == V244, V244 == V251, V251 == V258, V258 == V264, V264 == V271, V271 == V278, V278 == V286, V286 == V293, V293 == V300, V300 == V306, V306 == V313, V313 == V320, V320 == V328, V328 == V335, V335 == V342, V342 == V349, V349 == V355, V355 == V362, V362 == V370, V370 == V378, V378 == V385, V385 == V392, V392 == V399, V399 == V405, V405 == V412, V412 == V420, V420 == V428, V428 == V435, V435 == V442, V442 == V449, V449 == V455, V455 == V462, V462 == V470, V2 == V10, V10 == V17, V17 == V24, V24 == V31, V31 == V38, V38 == V45, V45 == V52, V52 == V58, V58 == V65, V65 == V73, V73 == V81, V81 == V88, V88 == V95, V95 == V102, V102 == V109, V109 == V116, V116 == V122, V122 == V129, V129 == V137, V137 == V158, V158 == V165, V165 == V173, V173 == V180, V180 == V187, V187 == V193, V193 == V200, V200 == V207, V207 == V214, V214 == V221, V221 == V229, V229 == V237, V237 == V245, V245 == V252, V252 == V259, V259 == V265, V265 == V272, V272 == V279, V279 == V287, V287 == V294, V294 == V301, V301 == V307, V307 == V314, V314 == V321, V321 == V329, V329 == V336, V336 == V343, V343 == V350, V350 == V356, V356 == V363, V363 == V371, V371 == V379, V379 == V386, V386 == V393, V393 == V400, V400 == V406, V406 == V413, V413 == V421, V421 == V429, V429 == V436, V436 == V443, V443 == V450, V450 == V456, V456 == V463, V463 == V471, V18 == V25, V25 == V32, V32 == V39, V39 == V46, V46 == V53, V53 == V59, V59 == V66, V66 == V74, V74 == V89, V89 == V96, V96 == V103, V103 == V110, V110 == V117, V117 == V123, V123 == V130, V130 == V138, V138 == V145, V145 == V152, V152 == V159, V159 == V166, V166 == V174, V174 == V181, V181 == V188, V188 == V194, V194 == V201, V201 == V208, V208 == V3, V3 == V222, V222 == V230, V230 == V238, V238 == V246, V246 == V253, V253 == V260, V260 == V266, V266 == V273, V273 == V280, V280 == V288, V288 == V295, V295 == V302, V302 == V308, V308 == V315, V315 == V322, V322 == V330, V330 == V337, V337 == V344, V344 == V351, V351 == V357, V357 == V364, V364 == V372, V372 == V380, V380 == V387, V387 == V394, V394 == V401, V401 == V407, V407 == V414, V414 == V422, V422 == V430, V430 == V437, V437 == V444, V444 == V451, V451 == V457, V457 == V464, V464 == V472, V4 == V11, V11 == V19, V19 == V26, V26 == V33, V33 == V40, V40 == V54, V54 == V60, V60 == V67, V67 == V75, V75 == V82, V82 == V90, V90 == V97, V97 == V104, V104 == V118, V118 == V124, V124 == V131, V131 == V139, V139 == V146, V146 == V153, V153 == V160, V160 == V167, V167 == V175, V175 == V182, V182 == V189, V189 == V195, V195 == V209, V209 == V215, V215 == V469, V469 == V223, V223 == V231, V231 == V239, V239 == V247, V247 == V254, V254 == V261, V261 == V267, V267 == V281, V281 == V289, V289 == V296, V296 == V303, V303 == V309, V309 == V323, V323 == V331, V331 == V338, V338 == V352, V352 == V358, V358 == V365, V365 == V373, V373 == V381, V381 == V388, V388 == V402, V402 == V408, V408 == V415, V415 == V423, V423 == V431, V431 == V438, V438 == V452, V452 == V458, V458 == V465, V465 == V473, V5 == V12, V12 == V20, V20 == V27, V27 == V34, V34 == V41, V41 == V47, V47 == V68, V68 == V76, V76 == V83, V83 == V91, V91 == V98, V98 == V105, V105 == V111, V111 == V132, V132 == V140, V140 == V147, V147 == V154, V154 == V161, V161 == V168, V168 == V176, V176 == V183, V183 == V202, V202 == V210, V210 == V216, V216 == V224, V224 == V232, V232 == V240, V240 == V248, V248 == V255, V255 == V274, V274 == V282, V282 == V290, V290 == V297, V297 == V316, V316 == V324, V324 == V332, V332 == V339, V339 == V345, V345 == V366, V366 == V374, V374 == V382, V382 == V389, V389 == V395, V395 == V416, V416 == V424, V424 == V432, V432 == V439, V439 == V445, V445 == V466, V466 == V474, V6 == V13, V13 == V21, V21 == V28, V28 == V48, V48 == V61, V61 == V69, V69 == V77, V77 == V84, V84 == V92, V92 == V99, V99 == V112, V112 == V125, V125 == V133, V133 == V141, V141 == V148, V148 == V155, V155 == V162, V162 == V169, V169 == V177, V177 == V184, V184 == V196, V196 == V203, V203 == V211, V211 == V472, V472 == V217, V217 == V225, V225 == V233, V233 == V241, V241 == V249, V249 == V256, V256 == V268, V268 == V275, V275 == V283, V283 == V291, V291 == V298, V298 == V310, V310 == V317, V317 == V325, V325 == V333, V333 == V340, V340 == V346, V346 == V359, V359 == V367, V367 == V375, V375 == V383, V383 == V390, V390 == V396, V396 == V409, V409 == V417, V417 == V425, V425 == V433, V433 == V440, V440 == V446, V446 == V459, V459 == V467, V467 == V475, V7 == V14, V14 == V35, V35 == V42, V42 == V49, V49 == V55, V55 == V62, V62 == V70, V70 == V78, V78 == V85, V85 == V106, V106 == V113, V113 == V119, V119 == V126, V126 == V134, V134 == V142, V142 == V149, V149 == V156, V156 == V163, V163 == V170, V170 == V190, V190 == V197, V197 == V204, V204 == V212, V212 == V218, V218 == V226, V226 == V234, V234 == V242, V242 == V262, V262 == V269, V269 == V276, V276 == V284, V284 == V304, V304 == V311, V311 == V318, V318 == V326, V326 == V347, V347 == V353, V353 == V360, V360 == V368, V368 == V376, V376 == V397, V397 == V403, V403 == V410, V410 == V418, V418 == V426, V426 == V447, V447 == V453, V453 == V460, V460 == V468, V468 == V476; #1044 ), references = 1, size of lhs = 15:
% 71.67/71.83 street-{F}(V0), P_skc13-{F}(V0), chevy-{F}(V1), old-{F}(V1), P_skc12-{F}(V1), P_skc9-{F}(V1), event-{F}(V2), P_skc14-{F}(V2), lonely-{F}(V3), P_skc8-{F}(V3), hollywood-{F}(V4), P_skc15-{F}(V4), P_skc11-{F}(V4), event-{F}(V5), P_skc10-{F}(V5) | ssSkC0-{T}()
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #2021: mergings( V1 == V8, V8 == V14, V14 == V20, V20 == V27, V27 == V34, V34 == V40, V40 == V46, V46 == V52, V52 == V57, V57 == V63, V63 == V70, V70 == V77, V77 == V83, V83 == V90, V90 == V97, V97 == V103, V103 == V109, V109 == V114, V114 == V120, V120 == V127, V127 == V134, V134 == V140, V140 == V152, V152 == V158, V158 == V165, V165 == V172, V172 == V177, V177 == V183, V183 == V189, V189 == V196, V196 == V202, V202 == V209, V209 == V216, V216 == V223, V223 == V230, V230 == V237, V237 == V242, V242 == V248, V248 == V254, V254 == V261, V261 == V268, V268 == V275, V275 == V280, V280 == V286, V286 == V292, V292 == V299, V299 == V306, V306 == V313, V313 == V319, V319 == V324, V324 == V330, V330 == V337, V337 == V344, V344 == V351, V351 == V358, V358 == V364, V364 == V369, V369 == V375, V375 == V382, V382 == V389, V389 == V396, V396 == V403, V403 == V409, V409 == V414, V414 == V420, V420 == V427, V427 == V434, V434 == V441, V441 == V448, V448 == V454, V454 == V460, V460 == V466, V466 == V472, V472 == V478, V478 == V484, V484 == V491, V2 == V9, V9 == V15, V15 == V21, V21 == V28, V28 == V35, V35 == V41, V41 == V47, V47 == V53, V53 == V58, V58 == V64, V64 == V71, V71 == V78, V78 == V84, V84 == V91, V91 == V98, V98 == V104, V104 == V110, V110 == V115, V115 == V121, V121 == V128, V128 == V135, V135 == V141, V141 == V146, V146 == V159, V159 == V166, V166 == V173, V173 == V178, V178 == V184, V184 == V190, V190 == V203, V203 == V210, V210 == V217, V217 == V224, V224 == V231, V231 == V238, V238 == V243, V243 == V249, V249 == V255, V255 == V262, V262 == V269, V269 == V276, V276 == V281, V281 == V287, V287 == V293, V293 == V300, V300 == V307, V307 == V314, V314 == V320, V320 == V325, V325 == V331, V331 == V338, V338 == V345, V345 == V352, V352 == V359, V359 == V365, V365 == V370, V370 == V376, V376 == V383, V383 == V390, V390 == V397, V397 == V404, V404 == V410, V410 == V415, V415 == V421, V421 == V428, V428 == V435, V435 == V442, V442 == V449, V449 == V455, V455 == V461, V461 == V467, V467 == V473, V473 == V479, V479 == V485, V485 == V492, V3 == V10, V10 == V16, V16 == V22, V22 == V29, V29 == V36, V36 == V42, V42 == V48, V48 == V54, V54 == V59, V59 == V65, V65 == V72, V72 == V79, V79 == V85, V85 == V92, V92 == V99, V99 == V105, V105 == V111, V111 == V116, V116 == V122, V122 == V129, V129 == V147, V147 == V153, V153 == V160, V160 == V167, V167 == V174, V174 == V179, V179 == V185, V185 == V191, V191 == V197, V197 == V204, V204 == V211, V211 == V218, V218 == V225, V225 == V232, V232 == V239, V239 == V244, V244 == V250, V250 == V256, V256 == V263, V263 == V270, V270 == V277, V277 == V282, V282 == V288, V288 == V294, V294 == V301, V301 == V308, V308 == V315, V315 == V321, V321 == V326, V326 == V332, V332 == V339, V339 == V346, V346 == V353, V353 == V360, V360 == V366, V366 == V371, V371 == V377, V377 == V384, V384 == V391, V391 == V398, V398 == V405, V405 == V411, V411 == V416, V416 == V422, V422 == V429, V429 == V436, V436 == V443, V443 == V450, V450 == V456, V456 == V462, V462 == V468, V468 == V474, V474 == V480, V480 == V486, V486 == V493, V4 == V23, V23 == V30, V30 == V37, V37 == V43, V43 == V49, V49 == V55, V55 == V60, V60 == V66, V66 == V73, V73 == V86, V86 == V93, V93 == V100, V100 == V106, V106 == V112, V112 == V117, V117 == V123, V123 == V130, V130 == V136, V136 == V142, V142 == V148, V148 == V154, V154 == V161, V161 == V168, V168 == V175, V175 == V180, V180 == V186, V186 == V192, V192 == V198, V198 == V205, V205 == V212, V212 == V219, V219 == V226, V226 == V233, V233 == V240, V240 == V245, V245 == V251, V251 == V257, V257 == V264, V264 == V271, V271 == V278, V278 == V283, V283 == V289, V289 == V295, V295 == V302, V302 == V309, V309 == V316, V316 == V322, V322 == V327, V327 == V333, V333 == V340, V340 == V347, V347 == V354, V354 == V361, V361 == V367, V367 == V372, V372 == V378, V378 == V385, V385 == V392, V392 == V399, V399 == V406, V406 == V412, V412 == V417, V417 == V423, V423 == V430, V430 == V437, V437 == V444, V444 == V451, V451 == V457, V457 == V463, V463 == V469, V469 == V475, V475 == V481, V481 == V487, V487 == V494, V5 == V11, V11 == V17, V17 == V24, V24 == V31, V31 == V38, V38 == V44, V44 == V56, V56 == V61, V61 == V67, V67 == V74, V74 == V80, V80 == V87, V87 == V94, V94 == V101, V101 == V113, V113 == V118, V118 == V124, V124 == V131, V131 == V137, V137 == V143, V143 == V149, V149 == V155, V155 == V162, V162 == V169, V169 == V176, V176 == V181, V181 == V193, V193 == V199, V199 == V491, V491 == V206, V206 == V213, V213 == V220, V220 == V227, V227 == V234, V234 == V241, V241 == V246, V246 == V258, V258 == V265, V265 == V272, V272 == V279, V279 == V284, V284 == V296, V296 == V303, V303 == V310, V310 == V323, V323 == V328, V328 == V334, V334 == V341, V341 == V348, V348 == V355, V355 == V368, V368 == V373, V373 == V379, V379 == V386, V386 == V393, V393 == V400, V400 == V413, V413 == V418, V418 == V424, V424 == V431, V431 == V438, V438 == V445, V445 == V452, V452 == V458, V458 == V464, V464 == V476, V476 == V482, V482 == V488, V488 == V495, V6 == V12, V12 == V18, V18 == V25, V25 == V32, V32 == V39, V39 == V45, V45 == V50, V50 == V68, V68 == V75, V75 == V81, V81 == V88, V88 == V95, V95 == V102, V102 == V107, V107 == V125, V125 == V132, V132 == V138, V138 == V144, V144 == V150, V150 == V156, V156 == V163, V163 == V170, V170 == V187, V187 == V194, V194 == V200, V200 == V207, V207 == V214, V214 == V221, V221 == V228, V228 == V235, V235 == V252, V252 == V259, V259 == V266, V266 == V273, V273 == V290, V290 == V297, V297 == V304, V304 == V311, V311 == V317, V317 == V335, V335 == V342, V342 == V349, V349 == V356, V356 == V362, V362 == V380, V380 == V387, V387 == V394, V394 == V401, V401 == V407, V407 == V425, V425 == V432, V432 == V439, V439 == V446, V446 == V453, V453 == V459, V459 == V465, V465 == V470, V470 == V489, V489 == V496, V7 == V13, V13 == V19, V19 == V26, V26 == V33, V33 == V51, V51 == V62, V62 == V69, V69 == V76, V76 == V82, V82 == V89, V89 == V96, V96 == V108, V108 == V119, V119 == V126, V126 == V133, V133 == V139, V139 == V145, V145 == V151, V151 == V157, V157 == V164, V164 == V171, V171 == V182, V182 == V188, V188 == V195, V195 == V494, V494 == V201, V201 == V208, V208 == V215, V215 == V222, V222 == V229, V229 == V236, V236 == V247, V247 == V253, V253 == V260, V260 == V267, V267 == V274, V274 == V285, V285 == V291, V291 == V298, V298 == V305, V305 == V312, V312 == V318, V318 == V329, V329 == V336, V336 == V343, V343 == V350, V350 == V357, V357 == V363, V363 == V374, V374 == V381, V381 == V388, V388 == V395, V395 == V402, V402 == V408, V408 == V419, V419 == V426, V426 == V433, V433 == V440, V440 == V447, V447 == V471, V471 == V477, V477 == V483, V483 == V490, V490 == V497; #1528 ), references = 1, size of lhs = 13:
% 71.67/71.83 street-{F}(V0), P_skc13-{F}(V0), event-{F}(V1), P_skc14-{F}(V1), chevy-{F}(V2), old-{F}(V2), P_skc12-{F}(V2), P_skc9-{F}(V2), hollywood-{F}(V3), P_skc15-{F}(V3), P_skc11-{F}(V3), event-{F}(V4), P_skc10-{F}(V4) | FALSE
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #2105: mergings( V0 == V8, V8 == V15, V15 == V22, V22 == V29, V29 == V36, V36 == V43, V43 == V50, V50 == V57, V57 == V64, V64 == V72, V1 == V9, V9 == V16, V16 == V23, V23 == V30, V30 == V37, V37 == V44, V44 == V51, V51 == V58, V58 == V65, V65 == V73, V2 == V10, V10 == V17, V17 == V24, V24 == V31, V31 == V38, V38 == V45, V45 == V52, V52 == V59, V59 == V66, V66 == V74, V3 == V11, V11 == V18, V18 == V25, V25 == V32, V32 == V39, V39 == V46, V46 == V53, V53 == V60, V60 == V67, V67 == V75, V4 == V12, V12 == V19, V19 == V26, V26 == V33, V33 == V40, V40 == V54, V54 == V61, V61 == V68, V68 == V76, V5 == V13, V13 == V20, V20 == V27, V27 == V34, V34 == V41, V41 == V47, V47 == V69, V69 == V77, V6 == V14, V14 == V48, V48 == V55, V55 == V62, V62 == V70, V70 == V78, V7 == V21, V21 == V28, V28 == V35, V35 == V42, V42 == V49, V49 == V56, V56 == V63, V63 == V71, V71 == V79; #2032 ), references = 1, size of lhs = 13:
% 71.67/71.83 chevy-{F}(V0), P_skc9-{F}(V0), lonely-{F}(V1), street-{F}(V1), P_skc8-{F}(V1), hollywood-{F}(V2), P_skc11-{F}(V2), event-{F}(V3), P_skc10-{F}(V3), P_skc15-{F}(V4), P_skc14-{F}(V5), P_skc13-{F}(V6), P_skc12-{F}(V7) | chevy-{T}(V7)
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #2188: mergings( V0 == V8, V8 == V15, V15 == V22, V22 == V29, V29 == V36, V36 == V43, V43 == V50, V50 == V57, V57 == V64, V64 == V72, V1 == V9, V9 == V16, V16 == V23, V23 == V30, V30 == V37, V37 == V44, V44 == V51, V51 == V58, V58 == V65, V65 == V73, V2 == V10, V10 == V17, V17 == V24, V24 == V31, V31 == V38, V38 == V45, V45 == V52, V52 == V59, V59 == V66, V66 == V74, V3 == V11, V11 == V18, V18 == V25, V25 == V32, V32 == V39, V39 == V46, V46 == V53, V53 == V60, V60 == V67, V67 == V75, V4 == V12, V12 == V19, V19 == V26, V26 == V33, V33 == V40, V40 == V54, V54 == V61, V61 == V68, V68 == V76, V5 == V13, V13 == V20, V20 == V27, V27 == V34, V34 == V41, V41 == V47, V47 == V69, V69 == V77, V6 == V14, V14 == V48, V48 == V55, V55 == V62, V62 == V70, V70 == V78, V7 == V21, V21 == V28, V28 == V35, V35 == V42, V42 == V49, V49 == V56, V56 == V63, V63 == V71, V71 == V79; #2115 ), references = 1, size of lhs = 13:
% 71.67/71.83 chevy-{F}(V0), P_skc9-{F}(V0), lonely-{F}(V1), street-{F}(V1), P_skc8-{F}(V1), hollywood-{F}(V2), P_skc11-{F}(V2), event-{F}(V3), P_skc10-{F}(V3), P_skc15-{F}(V4), P_skc14-{F}(V5), P_skc13-{F}(V6), P_skc12-{F}(V7) | dirty-{T}(V7)
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #2271: mergings( V0 == V8, V8 == V15, V15 == V22, V22 == V29, V29 == V36, V36 == V43, V43 == V50, V50 == V57, V57 == V64, V64 == V72, V1 == V9, V9 == V16, V16 == V23, V23 == V30, V30 == V37, V37 == V44, V44 == V51, V51 == V58, V58 == V65, V65 == V73, V2 == V10, V10 == V17, V17 == V24, V24 == V31, V31 == V38, V38 == V45, V45 == V52, V52 == V59, V59 == V66, V66 == V74, V3 == V11, V11 == V18, V18 == V25, V25 == V32, V32 == V39, V39 == V46, V46 == V53, V53 == V60, V60 == V67, V67 == V75, V4 == V12, V12 == V19, V19 == V26, V26 == V33, V33 == V40, V40 == V54, V54 == V61, V61 == V68, V68 == V76, V5 == V13, V13 == V20, V20 == V27, V27 == V34, V34 == V41, V41 == V47, V47 == V69, V69 == V77, V6 == V14, V14 == V48, V48 == V55, V55 == V62, V62 == V70, V70 == V78, V7 == V21, V21 == V28, V28 == V35, V35 == V42, V42 == V49, V49 == V56, V56 == V63, V63 == V71, V71 == V79; #2198 ), references = 1, size of lhs = 13:
% 71.67/71.83 chevy-{F}(V0), P_skc9-{F}(V0), lonely-{F}(V1), street-{F}(V1), P_skc8-{F}(V1), hollywood-{F}(V2), P_skc11-{F}(V2), event-{F}(V3), P_skc10-{F}(V3), P_skc15-{F}(V4), P_skc14-{F}(V5), P_skc13-{F}(V6), P_skc12-{F}(V7) | car-{T}(V7)
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #2354: mergings( V0 == V8, V8 == V15, V15 == V22, V22 == V29, V29 == V36, V36 == V43, V43 == V50, V50 == V57, V57 == V64, V64 == V72, V1 == V9, V9 == V16, V16 == V23, V23 == V30, V30 == V37, V37 == V44, V44 == V51, V51 == V58, V58 == V65, V65 == V73, V2 == V10, V10 == V17, V17 == V24, V24 == V31, V31 == V38, V38 == V45, V45 == V52, V52 == V59, V59 == V66, V66 == V74, V3 == V11, V11 == V18, V18 == V25, V25 == V32, V32 == V39, V39 == V46, V46 == V53, V53 == V60, V60 == V67, V67 == V75, V4 == V12, V12 == V19, V19 == V26, V26 == V33, V33 == V40, V40 == V54, V54 == V61, V61 == V68, V68 == V76, V5 == V13, V13 == V20, V20 == V27, V27 == V34, V34 == V41, V41 == V47, V47 == V69, V69 == V77, V6 == V14, V14 == V48, V48 == V55, V55 == V62, V62 == V70, V70 == V78, V7 == V21, V21 == V28, V28 == V35, V35 == V42, V42 == V49, V49 == V56, V56 == V63, V63 == V71, V71 == V79; #2281 ), references = 1, size of lhs = 13:
% 71.67/71.83 chevy-{F}(V0), P_skc9-{F}(V0), lonely-{F}(V1), street-{F}(V1), P_skc8-{F}(V1), hollywood-{F}(V2), P_skc11-{F}(V2), event-{F}(V3), P_skc10-{F}(V3), P_skc15-{F}(V4), P_skc14-{F}(V5), P_skc13-{F}(V6), P_skc12-{F}(V7) | way-{T}(V6)
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #2429: mergings( V0 == V8, V8 == V17, V17 == V24, V24 == V31, V31 == V38, V38 == V45, V45 == V52, V52 == V59, V59 == V67, V1 == V18, V18 == V25, V25 == V32, V32 == V39, V39 == V46, V46 == V53, V53 == V60, V60 == V68, V2 == V10, V10 == V19, V19 == V26, V26 == V33, V33 == V40, V40 == V47, V47 == V54, V54 == V61, V61 == V69, V3 == V11, V11 == V20, V20 == V27, V27 == V34, V34 == V41, V41 == V48, V48 == V55, V55 == V62, V62 == V70, V4 == V12, V12 == V21, V21 == V28, V28 == V35, V35 == V42, V42 == V49, V49 == V56, V56 == V63, V63 == V71, V5 == V13, V13 == V22, V22 == V29, V29 == V36, V36 == V43, V43 == V64, V64 == V72, V6 == V14, V14 == V50, V50 == V57, V57 == V65, V65 == V73, V7 == V15, V15 == V23, V23 == V30, V30 == V37, V37 == V44, V44 == V51, V51 == V58, V58 == V66, V66 == V74; #2363 ), references = 1, size of lhs = 33:
% 71.67/71.83 lonely-{F}(V0), way-{F}(V0), street-{F}(V0), P_skc13-{F}(V0), city-{F}(V1), hollywood-{F}(V1), P_skc15-{F}(V1), event-{F}(V2), P_skc14-{F}(V2), old-{F}(V3), dirty-{F}(V3), white-{F}(V3), car-{F}(V3), chevy-{F}(V3), barrel-{F}(V2,V3), chevy-{F}(V4), car-{F}(V4), white-{F}(V4), dirty-{F}(V4), old-{F}(V4), barrel-{F}(V2,V4), chevy-{F}(V5), P_skc9-{F}(V5), lonely-{F}(V6), way-{F}(V6), street-{F}(V6), P_skc8-{F}(V6), city-{F}(V7), hollywood-{F}(V7), P_skc11-{F}(V7), event-{F}(V8), P_skc10-{F}(V8), P_skc12-{F}(V9) | ssSkC0-{T}()
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #2569: mergings( V0 == V8, V8 == V15, V15 == V22, V22 == V29, V29 == V36, V36 == V43, V43 == V50, V50 == V57, V57 == V64, V64 == V72, V72 == V80, V80 == V87, V87 == V94, V94 == V101, V101 == V108, V108 == V115, V115 == V122, V122 == V130, V1 == V23, V23 == V30, V30 == V37, V37 == V44, V44 == V51, V51 == V58, V58 == V65, V65 == V73, V73 == V81, V81 == V88, V88 == V95, V95 == V102, V102 == V109, V109 == V116, V116 == V123, V123 == V131, V2 == V9, V9 == V16, V16 == V24, V24 == V31, V31 == V38, V38 == V45, V45 == V52, V52 == V59, V59 == V66, V66 == V74, V74 == V82, V82 == V89, V89 == V96, V96 == V103, V103 == V110, V110 == V117, V117 == V124, V124 == V132, V3 == V10, V10 == V17, V17 == V25, V25 == V32, V32 == V39, V39 == V46, V46 == V53, V53 == V60, V60 == V67, V67 == V75, V75 == V83, V83 == V90, V90 == V97, V97 == V104, V104 == V111, V111 == V118, V118 == V125, V125 == V133, V4 == V11, V11 == V18, V18 == V26, V26 == V33, V33 == V40, V40 == V47, V47 == V54, V54 == V61, V61 == V68, V68 == V76, V76 == V84, V84 == V91, V91 == V98, V98 == V105, V105 == V112, V112 == V119, V119 == V126, V126 == V134, V5 == V12, V12 == V19, V19 == V27, V27 == V34, V34 == V41, V41 == V48, V48 == V69, V69 == V77, V77 == V85, V85 == V92, V92 == V99, V99 == V106, V106 == V127, V127 == V135, V6 == V13, V13 == V20, V20 == V55, V55 == V62, V62 == V70, V70 == V78, V78 == V113, V113 == V120, V120 == V128, V128 == V136, V7 == V14, V14 == V21, V21 == V28, V28 == V35, V35 == V42, V42 == V49, V49 == V56, V56 == V63, V63 == V71, V71 == V79, V79 == V86, V86 == V93, V93 == V100, V100 == V107, V107 == V114, V114 == V121, V121 == V129, V129 == V137; #2438 ), references = 1, size of lhs = 26:
% 71.67/71.83 chevy-{F}(V0), car-{F}(V0), white-{F}(V0), dirty-{F}(V0), old-{F}(V0), P_skc12-{F}(V0), lonely-{F}(V1), way-{F}(V1), street-{F}(V1), P_skc13-{F}(V1), city-{F}(V2), hollywood-{F}(V2), P_skc15-{F}(V2), event-{F}(V3), P_skc14-{F}(V3), chevy-{F}(V4), P_skc9-{F}(V4), lonely-{F}(V5), way-{F}(V5), street-{F}(V5), P_skc8-{F}(V5), city-{F}(V6), hollywood-{F}(V6), P_skc11-{F}(V6), event-{F}(V7), P_skc10-{F}(V7) | ssSkC0-{T}()
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #2772: mergings( V8 == V15, V15 == V0, V0 == V29, V29 == V36, V36 == V43, V43 == V50, V50 == V57, V57 == V64, V64 == V71, V71 == V78, V78 == V86, V86 == V93, V93 == V100, V100 == V107, V107 == V114, V114 == V121, V121 == V128, V128 == V135, V135 == V143, V143 == V150, V150 == V157, V157 == V164, V164 == V171, V171 == V178, V178 == V185, V185 == V192, V1 == V22, V22 == V30, V30 == V37, V37 == V44, V44 == V51, V51 == V58, V58 == V65, V65 == V72, V72 == V79, V79 == V87, V87 == V94, V94 == V101, V101 == V108, V108 == V115, V115 == V122, V122 == V129, V129 == V136, V136 == V144, V144 == V151, V151 == V158, V158 == V165, V165 == V172, V172 == V179, V179 == V186, V186 == V193, V2 == V9, V9 == V16, V16 == V23, V23 == V31, V31 == V38, V38 == V45, V45 == V52, V52 == V59, V59 == V66, V66 == V73, V73 == V80, V80 == V88, V88 == V95, V95 == V102, V102 == V109, V109 == V116, V116 == V123, V123 == V130, V130 == V137, V137 == V145, V145 == V152, V152 == V159, V159 == V166, V166 == V173, V173 == V180, V180 == V187, V187 == V194, V3 == V10, V10 == V17, V17 == V24, V24 == V32, V32 == V39, V39 == V46, V46 == V53, V53 == V60, V60 == V67, V67 == V74, V74 == V81, V81 == V89, V89 == V96, V96 == V103, V103 == V110, V110 == V117, V117 == V124, V124 == V131, V131 == V138, V138 == V146, V146 == V153, V153 == V160, V160 == V167, V167 == V174, V174 == V181, V181 == V188, V188 == V195, V4 == V11, V11 == V18, V18 == V192, V192 == V25, V25 == V33, V33 == V40, V40 == V47, V47 == V54, V54 == V61, V61 == V68, V68 == V82, V82 == V90, V90 == V97, V97 == V104, V104 == V111, V111 == V118, V118 == V125, V125 == V139, V139 == V147, V147 == V154, V154 == V161, V161 == V168, V168 == V175, V175 == V182, V182 == V196, V5 == V12, V12 == V19, V19 == V26, V26 == V34, V34 == V41, V41 == V48, V48 == V55, V55 == V75, V75 == V83, V83 == V91, V91 == V98, V98 == V105, V105 == V112, V112 == V132, V132 == V140, V140 == V148, V148 == V155, V155 == V162, V162 == V169, V169 == V189, V189 == V197, V6 == V13, V13 == V20, V20 == V27, V27 == V62, V62 == V69, V69 == V76, V76 == V84, V84 == V119, V119 == V126, V126 == V133, V133 == V141, V141 == V176, V176 == V183, V183 == V190, V190 == V198, V7 == V14, V14 == V21, V21 == V28, V28 == V35, V35 == V42, V42 == V49, V49 == V56, V56 == V63, V63 == V70, V70 == V77, V77 == V85, V85 == V92, V92 == V99, V99 == V106, V106 == V113, V113 == V120, V120 == V127, V127 == V134, V134 == V142, V142 == V149, V149 == V156, V156 == V163, V163 == V170, V170 == V177, V177 == V184, V184 == V191, V191 == V199; #2578 ), references = 1, size of lhs = 23:
% 71.67/71.83 chevy-{F}(V0), car-{F}(V0), white-{F}(V0), dirty-{F}(V0), old-{F}(V0), P_skc12-{F}(V0), lonely-{F}(V1), way-{F}(V1), street-{F}(V1), P_skc13-{F}(V1), hollywood-{F}(V2), P_skc15-{F}(V2), P_skc11-{F}(V2), event-{F}(V3), P_skc14-{F}(V3), chevy-{F}(V4), P_skc9-{F}(V4), lonely-{F}(V5), way-{F}(V5), street-{F}(V5), P_skc8-{F}(V5), event-{F}(V6), P_skc10-{F}(V6) | ssSkC0-{T}()
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #3048: mergings( V0 == V15, V15 == V21, V21 == V28, V28 == V36, V36 == V43, V43 == V50, V50 == V57, V57 == V64, V64 == V71, V71 == V78, V78 == V85, V85 == V93, V93 == V100, V100 == V107, V107 == V114, V114 == V121, V121 == V128, V128 == V135, V135 == V142, V142 == V150, V150 == V157, V157 == V164, V164 == V171, V171 == V178, V178 == V185, V185 == V192, V192 == V199, V199 == V207, V207 == V214, V214 == V221, V221 == V228, V228 == V235, V235 == V242, V242 == V249, V249 == V256, V256 == V264, V1 == V8, V8 == V29, V29 == V37, V37 == V44, V44 == V51, V51 == V58, V58 == V65, V65 == V72, V72 == V79, V79 == V86, V86 == V94, V94 == V101, V101 == V108, V108 == V115, V115 == V122, V122 == V129, V129 == V136, V136 == V143, V143 == V151, V151 == V158, V158 == V165, V165 == V172, V172 == V179, V179 == V186, V186 == V193, V193 == V200, V200 == V208, V208 == V215, V215 == V222, V222 == V229, V229 == V236, V236 == V243, V243 == V250, V250 == V257, V257 == V265, V2 == V9, V9 == V16, V16 == V22, V22 == V30, V30 == V38, V38 == V45, V45 == V52, V52 == V59, V59 == V66, V66 == V73, V73 == V80, V80 == V87, V87 == V95, V95 == V102, V102 == V109, V109 == V116, V116 == V123, V123 == V130, V130 == V137, V137 == V144, V144 == V152, V152 == V159, V159 == V166, V166 == V173, V173 == V180, V180 == V187, V187 == V194, V194 == V201, V201 == V209, V209 == V216, V216 == V223, V223 == V230, V230 == V237, V237 == V244, V244 == V251, V251 == V258, V258 == V266, V10 == V3, V3 == V23, V23 == V31, V31 == V39, V39 == V46, V46 == V53, V53 == V60, V60 == V67, V67 == V74, V74 == V81, V81 == V88, V88 == V96, V96 == V103, V103 == V110, V110 == V117, V117 == V124, V124 == V131, V131 == V138, V138 == V145, V145 == V153, V153 == V160, V160 == V167, V167 == V174, V174 == V181, V181 == V188, V188 == V195, V195 == V202, V202 == V210, V210 == V217, V217 == V224, V224 == V231, V231 == V238, V238 == V245, V245 == V252, V252 == V259, V259 == V267, V4 == V11, V11 == V17, V17 == V24, V24 == V264, V264 == V32, V32 == V40, V40 == V47, V47 == V54, V54 == V61, V61 == V68, V68 == V75, V75 == V89, V89 == V97, V97 == V104, V104 == V111, V111 == V118, V118 == V125, V125 == V132, V132 == V146, V146 == V154, V154 == V161, V161 == V168, V168 == V175, V175 == V182, V182 == V189, V189 == V203, V203 == V211, V211 == V218, V218 == V225, V225 == V232, V232 == V246, V246 == V253, V253 == V260, V260 == V268, V5 == V12, V12 == V18, V18 == V25, V25 == V33, V33 == V41, V41 == V48, V48 == V55, V55 == V62, V62 == V82, V82 == V90, V90 == V98, V98 == V105, V105 == V112, V112 == V119, V119 == V139, V139 == V147, V147 == V155, V155 == V162, V162 == V169, V169 == V176, V176 == V196, V196 == V204, V204 == V212, V212 == V219, V219 == V226, V226 == V233, V233 == V239, V239 == V261, V261 == V269, V6 == V13, V13 == V19, V19 == V26, V26 == V34, V34 == V69, V69 == V76, V76 == V83, V83 == V91, V91 == V126, V126 == V133, V133 == V140, V140 == V148, V148 == V183, V183 == V190, V190 == V197, V197 == V205, V205 == V240, V240 == V247, V247 == V254, V254 == V262, V262 == V270, V7 == V14, V14 == V20, V20 == V27, V27 == V35, V35 == V42, V42 == V49, V49 == V56, V56 == V63, V63 == V70, V70 == V77, V77 == V84, V84 == V92, V92 == V99, V99 == V106, V106 == V113, V113 == V120, V120 == V127, V127 == V134, V134 == V141, V141 == V149, V149 == V156, V156 == V163, V163 == V170, V170 == V177, V177 == V184, V184 == V191, V191 == V198, V198 == V206, V206 == V213, V213 == V220, V220 == V227, V227 == V234, V234 == V241, V241 == V248, V248 == V255, V255 == V263, V263 == V271; #2782 ), references = 1, size of lhs = 22:
% 71.67/71.83 chevy-{F}(V0), car-{F}(V0), dirty-{F}(V0), old-{F}(V0), P_skc12-{F}(V0), lonely-{F}(V1), way-{F}(V1), street-{F}(V1), P_skc13-{F}(V1), event-{F}(V2), P_skc14-{F}(V2), chevy-{F}(V3), P_skc9-{F}(V3), lonely-{F}(V4), way-{F}(V4), street-{F}(V4), P_skc8-{F}(V4), hollywood-{F}(V5), P_skc15-{F}(V5), P_skc11-{F}(V5), event-{F}(V6), P_skc10-{F}(V6) | ssSkC0-{T}()
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #3153: mergings( V0 == V8, V8 == V15, V15 == V22, V22 == V29, V29 == V36, V36 == V43, V43 == V50, V50 == V57, V57 == V64, V64 == V71, V71 == V79, V1 == V9, V9 == V16, V16 == V23, V23 == V30, V30 == V37, V37 == V44, V44 == V51, V51 == V58, V58 == V65, V65 == V72, V72 == V80, V2 == V10, V10 == V17, V17 == V24, V24 == V31, V31 == V38, V38 == V45, V45 == V52, V52 == V59, V59 == V66, V66 == V73, V73 == V81, V3 == V11, V11 == V18, V18 == V25, V25 == V32, V32 == V39, V39 == V46, V46 == V53, V53 == V60, V60 == V67, V67 == V74, V74 == V82, V4 == V12, V12 == V19, V19 == V26, V26 == V33, V33 == V40, V40 == V47, V47 == V61, V61 == V68, V68 == V75, V75 == V83, V5 == V13, V13 == V20, V20 == V27, V27 == V34, V34 == V41, V41 == V48, V48 == V54, V54 == V76, V76 == V84, V6 == V14, V14 == V21, V21 == V55, V55 == V62, V62 == V69, V69 == V77, V77 == V85, V7 == V28, V28 == V35, V35 == V42, V42 == V49, V49 == V56, V56 == V63, V63 == V70, V70 == V78, V78 == V86; #3073 ), references = 2, size of lhs = 12:
% 71.67/71.83 chevy-{F}(V0), P_skc9-{F}(V0), lonely-{F}(V1), P_skc8-{F}(V1), hollywood-{F}(V2), P_skc11-{F}(V2), event-{F}(V3), P_skc10-{F}(V3), P_skc15-{F}(V4), P_skc14-{F}(V5), P_skc13-{F}(V6), P_skc12-{F}(V7) | car-{T}(V7)
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #3244: mergings( V0 == V8, V8 == V15, V15 == V22, V22 == V29, V29 == V36, V36 == V43, V43 == V50, V50 == V57, V57 == V64, V64 == V71, V71 == V79, V1 == V9, V9 == V16, V16 == V23, V23 == V30, V30 == V37, V37 == V44, V44 == V51, V51 == V58, V58 == V65, V65 == V72, V72 == V80, V2 == V10, V10 == V17, V17 == V24, V24 == V31, V31 == V38, V38 == V45, V45 == V52, V52 == V59, V59 == V66, V66 == V73, V73 == V81, V3 == V11, V11 == V18, V18 == V25, V25 == V32, V32 == V39, V39 == V46, V46 == V53, V53 == V60, V60 == V67, V67 == V74, V74 == V82, V4 == V12, V12 == V19, V19 == V26, V26 == V33, V33 == V40, V40 == V47, V47 == V61, V61 == V68, V68 == V75, V75 == V83, V5 == V13, V13 == V20, V20 == V27, V27 == V34, V34 == V41, V41 == V48, V48 == V54, V54 == V76, V76 == V84, V6 == V14, V14 == V21, V21 == V55, V55 == V62, V62 == V69, V69 == V77, V77 == V85, V7 == V28, V28 == V35, V35 == V42, V42 == V49, V49 == V56, V56 == V63, V63 == V70, V70 == V78, V78 == V86; #3164 ), references = 2, size of lhs = 12:
% 71.67/71.83 chevy-{F}(V0), P_skc9-{F}(V0), lonely-{F}(V1), P_skc8-{F}(V1), hollywood-{F}(V2), P_skc11-{F}(V2), event-{F}(V3), P_skc10-{F}(V3), P_skc15-{F}(V4), P_skc14-{F}(V5), P_skc13-{F}(V6), P_skc12-{F}(V7) | white-{T}(V7)
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #3335: mergings( V0 == V8, V8 == V15, V15 == V22, V22 == V29, V29 == V36, V36 == V43, V43 == V50, V50 == V57, V57 == V64, V64 == V71, V71 == V79, V1 == V9, V9 == V16, V16 == V23, V23 == V30, V30 == V37, V37 == V44, V44 == V51, V51 == V58, V58 == V65, V65 == V72, V72 == V80, V2 == V10, V10 == V17, V17 == V24, V24 == V31, V31 == V38, V38 == V45, V45 == V52, V52 == V59, V59 == V66, V66 == V73, V73 == V81, V3 == V11, V11 == V18, V18 == V25, V25 == V32, V32 == V39, V39 == V46, V46 == V53, V53 == V60, V60 == V67, V67 == V74, V74 == V82, V4 == V12, V12 == V19, V19 == V26, V26 == V33, V33 == V40, V40 == V47, V47 == V61, V61 == V68, V68 == V75, V75 == V83, V5 == V13, V13 == V20, V20 == V27, V27 == V34, V34 == V41, V41 == V48, V48 == V54, V54 == V76, V76 == V84, V6 == V14, V14 == V21, V21 == V55, V55 == V62, V62 == V69, V69 == V77, V77 == V85, V7 == V28, V28 == V35, V35 == V42, V42 == V49, V49 == V56, V56 == V63, V63 == V70, V70 == V78, V78 == V86; #3255 ), references = 2, size of lhs = 12:
% 71.67/71.83 chevy-{F}(V0), P_skc9-{F}(V0), lonely-{F}(V1), P_skc8-{F}(V1), hollywood-{F}(V2), P_skc11-{F}(V2), event-{F}(V3), P_skc10-{F}(V3), P_skc15-{F}(V4), P_skc14-{F}(V5), P_skc13-{F}(V6), P_skc12-{F}(V7) | lonely-{T}(V6)
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #3426: mergings( V0 == V8, V8 == V15, V15 == V22, V22 == V29, V29 == V36, V36 == V43, V43 == V50, V50 == V57, V57 == V64, V64 == V71, V71 == V79, V1 == V9, V9 == V16, V16 == V23, V23 == V30, V30 == V37, V37 == V44, V44 == V51, V51 == V58, V58 == V65, V65 == V72, V72 == V80, V2 == V10, V10 == V17, V17 == V24, V24 == V31, V31 == V38, V38 == V45, V45 == V52, V52 == V59, V59 == V66, V66 == V73, V73 == V81, V3 == V11, V11 == V18, V18 == V25, V25 == V32, V32 == V39, V39 == V46, V46 == V53, V53 == V60, V60 == V67, V67 == V74, V74 == V82, V4 == V12, V12 == V19, V19 == V26, V26 == V33, V33 == V40, V40 == V47, V47 == V61, V61 == V68, V68 == V75, V75 == V83, V5 == V13, V13 == V20, V20 == V27, V27 == V34, V34 == V41, V41 == V48, V48 == V54, V54 == V76, V76 == V84, V6 == V14, V14 == V21, V21 == V55, V55 == V62, V62 == V69, V69 == V77, V77 == V85, V7 == V28, V28 == V35, V35 == V42, V42 == V49, V49 == V56, V56 == V63, V63 == V70, V70 == V78, V78 == V86; #3346 ), references = 2, size of lhs = 12:
% 71.67/71.83 chevy-{F}(V0), P_skc9-{F}(V0), lonely-{F}(V1), P_skc8-{F}(V1), hollywood-{F}(V2), P_skc11-{F}(V2), event-{F}(V3), P_skc10-{F}(V3), P_skc15-{F}(V4), P_skc14-{F}(V5), P_skc13-{F}(V6), P_skc12-{F}(V7) | dirty-{T}(V7)
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #3509: mergings( V0 == V8, V8 == V15, V15 == V22, V22 == V29, V29 == V36, V36 == V43, V43 == V50, V50 == V57, V57 == V64, V64 == V72, V1 == V9, V9 == V16, V16 == V23, V23 == V30, V30 == V37, V37 == V44, V44 == V51, V51 == V58, V58 == V65, V65 == V73, V2 == V10, V10 == V17, V17 == V24, V24 == V31, V31 == V38, V38 == V45, V45 == V52, V52 == V59, V59 == V66, V66 == V74, V3 == V11, V11 == V18, V18 == V25, V25 == V32, V32 == V39, V39 == V46, V46 == V53, V53 == V60, V60 == V67, V67 == V75, V4 == V12, V12 == V19, V19 == V26, V26 == V33, V33 == V40, V40 == V47, V47 == V54, V54 == V61, V61 == V68, V68 == V76, V5 == V13, V13 == V20, V20 == V27, V27 == V34, V34 == V41, V41 == V48, V48 == V69, V69 == V77, V6 == V14, V14 == V21, V21 == V55, V55 == V62, V62 == V70, V70 == V78, V7 == V28, V28 == V35, V35 == V42, V42 == V49, V49 == V56, V56 == V63, V63 == V71, V71 == V79; #3436 ), references = 1, size of lhs = 13:
% 71.67/71.83 chevy-{F}(V0), P_skc9-{F}(V0), lonely-{F}(V1), P_skc8-{F}(V1), city-{F}(V2), hollywood-{F}(V2), P_skc11-{F}(V2), event-{F}(V3), P_skc10-{F}(V3), P_skc15-{F}(V4), P_skc14-{F}(V5), P_skc13-{F}(V6), P_skc12-{F}(V7) | barrel-{T}(V5,V7)
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #3592: mergings( V0 == V8, V8 == V15, V15 == V22, V22 == V29, V29 == V36, V36 == V43, V43 == V50, V50 == V57, V57 == V64, V64 == V72, V1 == V9, V9 == V16, V16 == V23, V23 == V30, V30 == V37, V37 == V44, V44 == V51, V51 == V58, V58 == V65, V65 == V73, V2 == V10, V10 == V17, V17 == V24, V24 == V31, V31 == V38, V38 == V45, V45 == V52, V52 == V59, V59 == V66, V66 == V74, V3 == V11, V11 == V18, V18 == V25, V25 == V32, V32 == V39, V39 == V46, V46 == V53, V53 == V60, V60 == V67, V67 == V75, V4 == V12, V12 == V19, V19 == V26, V26 == V33, V33 == V40, V40 == V47, V47 == V54, V54 == V61, V61 == V68, V68 == V76, V5 == V13, V13 == V20, V20 == V27, V27 == V34, V34 == V41, V41 == V48, V48 == V69, V69 == V77, V6 == V14, V14 == V21, V21 == V55, V55 == V62, V62 == V70, V70 == V78, V7 == V28, V28 == V35, V35 == V42, V42 == V49, V49 == V56, V56 == V63, V63 == V71, V71 == V79; #3519 ), references = 1, size of lhs = 13:
% 71.67/71.83 chevy-{F}(V0), P_skc9-{F}(V0), lonely-{F}(V1), P_skc8-{F}(V1), city-{F}(V2), hollywood-{F}(V2), P_skc11-{F}(V2), event-{F}(V3), P_skc10-{F}(V3), P_skc15-{F}(V4), P_skc14-{F}(V5), P_skc13-{F}(V6), P_skc12-{F}(V7) | down-{T}(V5,V6)
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #3841: mergings( V8 == V15, V15 == V22, V22 == V29, V29 == V36, V36 == V43, V43 == V50, V50 == V57, V57 == V64, V64 == V71, V71 == V78, V78 == V86, V86 == V93, V93 == V100, V100 == V107, V107 == V114, V114 == V121, V121 == V128, V128 == V135, V135 == V142, V142 == V149, V149 == V156, V156 == V0, V0 == V171, V171 == V178, V178 == V185, V185 == V192, V192 == V199, V199 == V206, V206 == V213, V213 == V220, V220 == V227, V227 == V234, V1 == V16, V16 == V23, V23 == V30, V30 == V37, V37 == V44, V44 == V51, V51 == V58, V58 == V65, V65 == V72, V72 == V79, V79 == V94, V94 == V101, V101 == V108, V108 == V115, V115 == V122, V122 == V129, V129 == V136, V136 == V143, V143 == V150, V150 == V157, V157 == V164, V164 == V172, V172 == V179, V179 == V186, V186 == V193, V193 == V200, V200 == V207, V207 == V214, V214 == V221, V221 == V228, V228 == V235, V2 == V9, V9 == V17, V17 == V24, V24 == V31, V31 == V38, V38 == V45, V45 == V52, V52 == V59, V59 == V66, V66 == V73, V73 == V80, V80 == V87, V87 == V95, V95 == V102, V102 == V109, V109 == V116, V116 == V123, V123 == V130, V130 == V137, V137 == V144, V144 == V151, V151 == V158, V158 == V165, V165 == V173, V173 == V180, V180 == V187, V187 == V194, V194 == V201, V201 == V208, V208 == V215, V215 == V222, V222 == V229, V229 == V236, V3 == V10, V10 == V18, V18 == V25, V25 == V32, V32 == V39, V39 == V46, V46 == V53, V53 == V60, V60 == V67, V67 == V74, V74 == V81, V81 == V88, V88 == V96, V96 == V103, V103 == V110, V110 == V117, V117 == V124, V124 == V131, V131 == V138, V138 == V145, V145 == V152, V152 == V159, V159 == V166, V166 == V174, V174 == V181, V181 == V188, V188 == V195, V195 == V202, V202 == V209, V209 == V216, V216 == V223, V223 == V230, V230 == V237, V4 == V11, V11 == V19, V19 == V26, V26 == V33, V33 == V40, V40 == V47, V47 == V54, V54 == V61, V61 == V68, V68 == V82, V82 == V89, V89 == V97, V97 == V104, V104 == V111, V111 == V118, V118 == V125, V125 == V132, V132 == V139, V139 == V146, V146 == V160, V160 == V234, V234 == V167, V167 == V175, V175 == V182, V182 == V189, V189 == V196, V196 == V203, V203 == V210, V210 == V217, V217 == V224, V224 == V238, V5 == V12, V12 == V20, V20 == V27, V27 == V34, V34 == V41, V41 == V48, V48 == V55, V55 == V75, V75 == V83, V83 == V90, V90 == V98, V98 == V105, V105 == V112, V112 == V119, V119 == V126, V126 == V133, V133 == V153, V153 == V161, V161 == V168, V168 == V176, V176 == V183, V183 == V190, V190 == V197, V197 == V204, V204 == V211, V211 == V231, V231 == V239, V6 == V13, V13 == V21, V21 == V28, V28 == V62, V62 == V69, V69 == V76, V76 == V84, V84 == V91, V91 == V99, V99 == V106, V106 == V140, V140 == V147, V147 == V154, V154 == V162, V162 == V169, V169 == V177, V177 == V184, V184 == V218, V218 == V225, V225 == V232, V232 == V240, V7 == V14, V14 == V35, V35 == V42, V42 == V49, V49 == V56, V56 == V63, V63 == V70, V70 == V77, V77 == V85, V85 == V92, V92 == V113, V113 == V120, V120 == V127, V127 == V134, V134 == V141, V141 == V148, V148 == V155, V155 == V163, V163 == V170, V170 == V191, V191 == V198, V198 == V205, V205 == V212, V212 == V219, V219 == V226, V226 == V233, V233 == V241; #3605 ), references = 1, size of lhs = 21:
% 71.67/71.83 chevy-{F}(V0), car-{F}(V0), white-{F}(V0), dirty-{F}(V0), old-{F}(V0), P_skc12-{F}(V0), lonely-{F}(V1), way-{F}(V1), street-{F}(V1), P_skc13-{F}(V1), hollywood-{F}(V2), P_skc15-{F}(V2), P_skc11-{F}(V2), event-{F}(V3), P_skc14-{F}(V3), chevy-{F}(V4), P_skc9-{F}(V4), lonely-{F}(V5), P_skc8-{F}(V5), event-{F}(V6), P_skc10-{F}(V6) | ssSkC0-{T}()
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #4175: mergings( V0 == V15, V15 == V22, V22 == V29, V29 == V36, V36 == V43, V43 == V50, V50 == V57, V57 == V64, V64 == V71, V71 == V78, V78 == V85, V85 == V93, V93 == V99, V99 == V106, V106 == V113, V113 == V120, V120 == V127, V127 == V134, V134 == V141, V141 == V148, V148 == V155, V155 == V162, V162 == V170, V170 == V178, V178 == V185, V185 == V192, V192 == V199, V199 == V206, V206 == V213, V213 == V220, V220 == V227, V227 == V234, V234 == V241, V241 == V249, V249 == V256, V256 == V263, V263 == V270, V270 == V277, V277 == V284, V284 == V291, V291 == V298, V298 == V305, V305 == V312, V312 == V320, V1 == V8, V8 == V23, V23 == V30, V30 == V37, V37 == V44, V44 == V51, V51 == V58, V58 == V65, V65 == V72, V72 == V79, V79 == V86, V86 == V100, V100 == V107, V107 == V114, V114 == V121, V121 == V128, V128 == V135, V135 == V142, V142 == V149, V149 == V156, V156 == V163, V163 == V171, V171 == V179, V179 == V186, V186 == V193, V193 == V200, V200 == V207, V207 == V214, V214 == V221, V221 == V228, V228 == V235, V235 == V242, V242 == V250, V250 == V257, V257 == V264, V264 == V271, V271 == V278, V278 == V285, V285 == V292, V292 == V299, V299 == V306, V306 == V313, V313 == V321, V9 == V16, V16 == V24, V24 == V31, V31 == V38, V38 == V45, V45 == V52, V52 == V59, V59 == V66, V66 == V73, V73 == V80, V80 == V87, V87 == V2, V2 == V101, V101 == V108, V108 == V115, V115 == V122, V122 == V129, V129 == V136, V136 == V143, V143 == V150, V150 == V157, V157 == V164, V164 == V172, V172 == V180, V180 == V187, V187 == V194, V194 == V201, V201 == V208, V208 == V215, V215 == V222, V222 == V229, V229 == V236, V236 == V243, V243 == V251, V251 == V258, V258 == V265, V265 == V272, V272 == V279, V279 == V286, V286 == V293, V293 == V300, V300 == V307, V307 == V314, V314 == V322, V3 == V10, V10 == V17, V17 == V25, V25 == V32, V32 == V39, V39 == V46, V46 == V53, V53 == V60, V60 == V67, V67 == V74, V74 == V81, V81 == V88, V88 == V94, V94 == V102, V102 == V109, V109 == V116, V116 == V123, V123 == V130, V130 == V137, V137 == V144, V144 == V151, V151 == V158, V158 == V165, V165 == V173, V173 == V181, V181 == V188, V188 == V195, V195 == V202, V202 == V209, V209 == V216, V216 == V223, V223 == V230, V230 == V237, V237 == V244, V244 == V252, V252 == V259, V259 == V266, V266 == V273, V273 == V280, V280 == V287, V287 == V294, V294 == V301, V301 == V308, V308 == V315, V315 == V323, V4 == V11, V11 == V18, V18 == V26, V26 == V33, V33 == V40, V40 == V47, V47 == V54, V54 == V61, V61 == V68, V68 == V75, V75 == V89, V89 == V95, V95 == V103, V103 == V110, V110 == V117, V117 == V124, V124 == V131, V131 == V138, V138 == V145, V145 == V152, V152 == V166, V166 == V320, V320 == V174, V174 == V182, V182 == V189, V189 == V196, V196 == V203, V203 == V210, V210 == V217, V217 == V224, V224 == V231, V231 == V245, V245 == V253, V253 == V260, V260 == V267, V267 == V274, V274 == V281, V281 == V288, V288 == V302, V302 == V309, V309 == V316, V316 == V324, V5 == V12, V12 == V19, V19 == V27, V27 == V34, V34 == V41, V41 == V48, V48 == V55, V55 == V62, V62 == V82, V82 == V90, V90 == V96, V96 == V104, V104 == V111, V111 == V118, V118 == V125, V125 == V132, V132 == V139, V139 == V159, V159 == V167, V167 == V175, V175 == V183, V183 == V190, V190 == V197, V197 == V204, V204 == V211, V211 == V218, V218 == V238, V238 == V246, V246 == V254, V254 == V261, V261 == V268, V268 == V275, V275 == V282, V282 == V289, V289 == V295, V295 == V317, V317 == V325, V6 == V13, V13 == V20, V20 == V28, V28 == V35, V35 == V69, V69 == V76, V76 == V83, V83 == V91, V91 == V97, V97 == V105, V105 == V112, V112 == V146, V146 == V153, V153 == V160, V160 == V168, V168 == V176, V176 == V184, V184 == V191, V191 == V225, V225 == V232, V232 == V239, V239 == V247, V247 == V255, V255 == V262, V262 == V296, V296 == V303, V303 == V310, V310 == V318, V318 == V326, V7 == V14, V14 == V21, V21 == V42, V42 == V49, V49 == V56, V56 == V63, V63 == V70, V70 == V77, V77 == V84, V84 == V92, V92 == V98, V98 == V119, V119 == V126, V126 == V133, V133 == V140, V140 == V147, V147 == V154, V154 == V161, V161 == V169, V169 == V177, V177 == V198, V198 == V205, V205 == V212, V212 == V219, V219 == V226, V226 == V233, V233 == V240, V240 == V248, V248 == V269, V269 == V276, V276 == V283, V283 == V290, V290 == V297, V297 == V304, V304 == V311, V311 == V319, V319 == V327; #3853 ), references = 1, size of lhs = 20:
% 71.67/71.83 chevy-{F}(V0), car-{F}(V0), white-{F}(V0), dirty-{F}(V0), old-{F}(V0), P_skc12-{F}(V0), lonely-{F}(V1), street-{F}(V1), P_skc13-{F}(V1), event-{F}(V2), P_skc14-{F}(V2), chevy-{F}(V3), P_skc9-{F}(V3), lonely-{F}(V4), P_skc8-{F}(V4), hollywood-{F}(V5), P_skc15-{F}(V5), P_skc11-{F}(V5), event-{F}(V6), P_skc10-{F}(V6) | ssSkC0-{T}()
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #4595: mergings( V0 == V8, V8 == V22, V22 == V28, V28 == V35, V35 == V42, V42 == V49, V49 == V56, V56 == V63, V63 == V70, V70 == V77, V77 == V84, V84 == V91, V91 == V99, V99 == V106, V106 == V113, V113 == V120, V120 == V127, V127 == V134, V134 == V141, V141 == V148, V148 == V155, V155 == V162, V162 == V169, V169 == V177, V177 == V185, V185 == V192, V192 == V199, V199 == V206, V206 == V213, V213 == V220, V220 == V227, V227 == V234, V234 == V241, V241 == V248, V248 == V256, V256 == V263, V263 == V270, V270 == V277, V277 == V284, V284 == V291, V291 == V298, V298 == V305, V305 == V312, V312 == V319, V319 == V327, V327 == V335, V335 == V342, V342 == V349, V349 == V356, V356 == V363, V363 == V370, V370 == V377, V377 == V384, V384 == V391, V391 == V398, V398 == V406, V1 == V9, V9 == V15, V15 == V29, V29 == V36, V36 == V43, V43 == V50, V50 == V57, V57 == V64, V64 == V71, V71 == V78, V78 == V85, V85 == V92, V92 == V107, V107 == V114, V114 == V121, V121 == V128, V128 == V135, V135 == V142, V142 == V149, V149 == V156, V156 == V163, V163 == V170, V170 == V178, V178 == V186, V186 == V193, V193 == V200, V200 == V207, V207 == V214, V214 == V221, V221 == V228, V228 == V235, V235 == V242, V242 == V249, V249 == V257, V257 == V264, V264 == V271, V271 == V278, V278 == V285, V285 == V292, V292 == V299, V299 == V306, V306 == V313, V313 == V320, V320 == V328, V328 == V336, V336 == V343, V343 == V350, V350 == V357, V357 == V364, V364 == V371, V371 == V378, V378 == V385, V385 == V392, V392 == V399, V399 == V407, V2 == V16, V16 == V23, V23 == V30, V30 == V37, V37 == V44, V44 == V51, V51 == V58, V58 == V65, V65 == V72, V72 == V79, V79 == V86, V86 == V93, V93 == V100, V100 == V108, V108 == V115, V115 == V122, V122 == V129, V129 == V136, V136 == V143, V143 == V150, V150 == V157, V157 == V164, V164 == V171, V171 == V179, V179 == V187, V187 == V194, V194 == V201, V201 == V208, V208 == V215, V215 == V222, V222 == V229, V229 == V236, V236 == V243, V243 == V250, V250 == V258, V258 == V265, V265 == V272, V272 == V279, V279 == V286, V286 == V293, V293 == V300, V300 == V307, V307 == V314, V314 == V321, V321 == V329, V329 == V337, V337 == V344, V344 == V351, V351 == V358, V358 == V365, V365 == V372, V372 == V379, V379 == V386, V386 == V393, V393 == V400, V400 == V408, V10 == V17, V17 == V3, V3 == V31, V31 == V38, V38 == V45, V45 == V52, V52 == V59, V59 == V66, V66 == V73, V73 == V80, V80 == V87, V87 == V94, V94 == V101, V101 == V109, V109 == V116, V116 == V123, V123 == V130, V130 == V137, V137 == V144, V144 == V151, V151 == V158, V158 == V165, V165 == V172, V172 == V180, V180 == V188, V188 == V195, V195 == V202, V202 == V209, V209 == V216, V216 == V223, V223 == V230, V230 == V237, V237 == V244, V244 == V251, V251 == V259, V259 == V266, V266 == V273, V273 == V280, V280 == V287, V287 == V294, V294 == V301, V301 == V308, V308 == V315, V315 == V322, V322 == V330, V330 == V338, V338 == V345, V345 == V352, V352 == V359, V359 == V366, V366 == V373, V373 == V380, V380 == V387, V387 == V394, V394 == V401, V401 == V409, V4 == V11, V11 == V18, V18 == V24, V24 == V32, V32 == V39, V39 == V46, V46 == V53, V53 == V60, V60 == V67, V67 == V74, V74 == V81, V81 == V95, V95 == V102, V102 == V110, V110 == V117, V117 == V124, V124 == V131, V131 == V138, V138 == V145, V145 == V152, V152 == V159, V159 == V173, V173 == V406, V406 == V181, V181 == V189, V189 == V196, V196 == V203, V203 == V210, V210 == V217, V217 == V224, V224 == V231, V231 == V238, V238 == V252, V252 == V260, V260 == V267, V267 == V274, V274 == V281, V281 == V288, V288 == V295, V295 == V309, V309 == V316, V316 == V323, V323 == V331, V331 == V339, V339 == V346, V346 == V353, V353 == V360, V360 == V367, V367 == V374, V374 == V388, V388 == V395, V395 == V402, V402 == V410, V5 == V12, V12 == V19, V19 == V25, V25 == V33, V33 == V40, V40 == V47, V47 == V54, V54 == V61, V61 == V68, V68 == V88, V88 == V96, V96 == V103, V103 == V111, V111 == V118, V118 == V125, V125 == V132, V132 == V139, V139 == V146, V146 == V166, V166 == V174, V174 == V182, V182 == V190, V190 == V197, V197 == V204, V204 == V211, V211 == V218, V218 == V225, V225 == V245, V245 == V253, V253 == V261, V261 == V268, V268 == V275, V275 == V282, V282 == V289, V289 == V296, V296 == V302, V302 == V324, V324 == V332, V332 == V340, V340 == V347, V347 == V354, V354 == V361, V361 == V368, V368 == V375, V375 == V381, V381 == V403, V403 == V411, V6 == V13, V13 == V20, V20 == V26, V26 == V34, V34 == V41, V41 == V75, V75 == V82, V82 == V89, V89 == V97, V97 == V104, V104 == V112, V112 == V119, V119 == V153, V153 == V160, V160 == V167, V167 == V175, V175 == V183, V183 == V191, V191 == V198, V198 == V232, V232 == V239, V239 == V246, V246 == V254, V254 == V262, V262 == V269, V269 == V303, V303 == V310, V310 == V317, V317 == V325, V325 == V333, V333 == V341, V341 == V348, V348 == V382, V382 == V389, V389 == V396, V396 == V404, V404 == V412, V7 == V14, V14 == V21, V21 == V27, V27 == V48, V48 == V55, V55 == V62, V62 == V69, V69 == V76, V76 == V83, V83 == V90, V90 == V98, V98 == V105, V105 == V126, V126 == V133, V133 == V140, V140 == V147, V147 == V154, V154 == V161, V161 == V168, V168 == V176, V176 == V184, V184 == V205, V205 == V212, V212 == V219, V219 == V226, V226 == V233, V233 == V240, V240 == V247, V247 == V255, V255 == V276, V276 == V283, V283 == V290, V290 == V297, V297 == V304, V304 == V311, V311 == V318, V318 == V326, V326 == V334, V334 == V355, V355 == V362, V362 == V369, V369 == V376, V376 == V383, V383 == V390, V390 == V397, V397 == V405, V405 == V413; #4187 ), references = 1, size of lhs = 19:
% 71.67/71.83 car-{F}(V0), white-{F}(V0), dirty-{F}(V0), old-{F}(V0), P_skc12-{F}(V0), lonely-{F}(V1), street-{F}(V1), P_skc13-{F}(V1), event-{F}(V2), P_skc14-{F}(V2), chevy-{F}(V3), P_skc9-{F}(V3), lonely-{F}(V4), P_skc8-{F}(V4), hollywood-{F}(V5), P_skc15-{F}(V5), P_skc11-{F}(V5), event-{F}(V6), P_skc10-{F}(V6) | ssSkC0-{T}()
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #5354: mergings( V1 == V8, V8 == V14, V14 == V21, V21 == V28, V28 == V34, V34 == V40, V40 == V46, V46 == V52, V52 == V58, V58 == V64, V64 == V70, V70 == V77, V77 == V84, V84 == V90, V90 == V97, V97 == V104, V104 == V110, V110 == V116, V116 == V122, V122 == V128, V128 == V134, V134 == V140, V140 == V146, V146 == V153, V153 == V160, V160 == V166, V166 == V173, V173 == V180, V180 == V186, V186 == V192, V192 == V198, V198 == V204, V204 == V210, V210 == V216, V216 == V222, V222 == V229, V229 == V236, V236 == V242, V242 == V249, V249 == V256, V256 == V262, V262 == V268, V268 == V274, V274 == V280, V280 == V286, V286 == V292, V292 == V298, V298 == V305, V305 == V312, V312 == V318, V318 == V330, V330 == V336, V336 == V343, V343 == V350, V350 == V356, V356 == V362, V362 == V368, V368 == V374, V374 == V380, V380 == V386, V386 == V392, V392 == V399, V399 == V405, V405 == V412, V412 == V419, V419 == V425, V425 == V431, V431 == V437, V437 == V443, V443 == V449, V449 == V455, V455 == V461, V461 == V468, V468 == V475, V475 == V482, V482 == V489, V489 == V495, V495 == V501, V501 == V507, V507 == V513, V513 == V519, V519 == V525, V525 == V531, V531 == V538, V538 == V545, V545 == V552, V552 == V558, V558 == V564, V564 == V570, V570 == V576, V576 == V582, V582 == V588, V588 == V594, V594 == V601, V601 == V608, V608 == V615, V615 == V622, V622 == V628, V628 == V634, V634 == V640, V640 == V646, V646 == V652, V652 == V658, V658 == V664, V664 == V671, V671 == V678, V678 == V685, V685 == V692, V692 == V698, V698 == V704, V704 == V710, V710 == V716, V716 == V722, V722 == V728, V728 == V734, V734 == V741, V2 == V9, V9 == V15, V15 == V22, V22 == V29, V29 == V35, V35 == V41, V41 == V47, V47 == V53, V53 == V59, V59 == V65, V65 == V71, V71 == V78, V78 == V85, V85 == V91, V91 == V98, V98 == V105, V105 == V111, V111 == V117, V117 == V123, V123 == V129, V129 == V135, V135 == V141, V141 == V147, V147 == V154, V154 == V161, V161 == V167, V167 == V174, V174 == V181, V181 == V187, V187 == V193, V193 == V199, V199 == V205, V205 == V211, V211 == V217, V217 == V223, V223 == V230, V230 == V237, V237 == V243, V243 == V250, V250 == V257, V257 == V263, V263 == V269, V269 == V275, V275 == V281, V281 == V287, V287 == V293, V293 == V299, V299 == V306, V306 == V313, V313 == V319, V319 == V324, V324 == V337, V337 == V344, V344 == V351, V351 == V357, V357 == V363, V363 == V369, V369 == V375, V375 == V381, V381 == V387, V387 == V393, V393 == V406, V406 == V413, V413 == V420, V420 == V426, V426 == V432, V432 == V438, V438 == V444, V444 == V450, V450 == V456, V456 == V462, V462 == V469, V469 == V476, V476 == V483, V483 == V490, V490 == V496, V496 == V502, V502 == V508, V508 == V514, V514 == V520, V520 == V526, V526 == V532, V532 == V539, V539 == V546, V546 == V553, V553 == V559, V559 == V565, V565 == V571, V571 == V577, V577 == V583, V583 == V589, V589 == V595, V595 == V602, V602 == V609, V609 == V616, V616 == V623, V623 == V629, V629 == V635, V635 == V641, V641 == V647, V647 == V653, V653 == V659, V659 == V665, V665 == V672, V672 == V679, V679 == V686, V686 == V693, V693 == V699, V699 == V705, V705 == V711, V711 == V717, V717 == V723, V723 == V729, V729 == V735, V735 == V742, V3 == V10, V10 == V16, V16 == V23, V23 == V30, V30 == V36, V36 == V42, V42 == V48, V48 == V54, V54 == V60, V60 == V66, V66 == V72, V72 == V79, V79 == V86, V86 == V92, V92 == V99, V99 == V106, V106 == V112, V112 == V118, V118 == V124, V124 == V130, V130 == V136, V136 == V142, V142 == V148, V148 == V155, V155 == V168, V168 == V175, V175 == V182, V182 == V188, V188 == V194, V194 == V200, V200 == V206, V206 == V212, V212 == V218, V218 == V224, V224 == V231, V231 == V238, V238 == V244, V244 == V251, V251 == V258, V258 == V264, V264 == V270, V270 == V276, V276 == V282, V282 == V288, V288 == V294, V294 == V300, V300 == V307, V307 == V314, V314 == V325, V325 == V331, V331 == V338, V338 == V345, V345 == V352, V352 == V358, V358 == V364, V364 == V370, V370 == V376, V376 == V382, V382 == V388, V388 == V394, V394 == V400, V400 == V407, V407 == V414, V414 == V421, V421 == V427, V427 == V433, V433 == V439, V439 == V445, V445 == V451, V451 == V457, V457 == V463, V463 == V470, V470 == V477, V477 == V484, V484 == V491, V491 == V497, V497 == V503, V503 == V509, V509 == V515, V515 == V521, V521 == V527, V527 == V533, V533 == V540, V540 == V547, V547 == V554, V554 == V560, V560 == V566, V566 == V572, V572 == V578, V578 == V584, V584 == V590, V590 == V596, V596 == V603, V603 == V610, V610 == V617, V617 == V624, V624 == V630, V630 == V636, V636 == V642, V642 == V648, V648 == V654, V654 == V660, V660 == V666, V666 == V673, V673 == V680, V680 == V687, V687 == V694, V694 == V700, V700 == V706, V706 == V712, V712 == V718, V718 == V724, V724 == V730, V730 == V736, V736 == V743, V4 == V17, V17 == V24, V24 == V31, V31 == V37, V37 == V43, V43 == V49, V49 == V55, V55 == V61, V61 == V67, V67 == V73, V73 == V80, V80 == V93, V93 == V100, V100 == V107, V107 == V113, V113 == V119, V119 == V125, V125 == V131, V131 == V137, V137 == V143, V143 == V149, V149 == V156, V156 == V162, V162 == V169, V169 == V176, V176 == V183, V183 == V189, V189 == V195, V195 == V201, V201 == V207, V207 == V213, V213 == V219, V219 == V225, V225 == V232, V232 == V245, V245 == V252, V252 == V259, V259 == V265, V265 == V271, V271 == V277, V277 == V283, V283 == V289, V289 == V295, V295 == V301, V301 == V308, V308 == V320, V320 == V326, V326 == V332, V332 == V339, V339 == V346, V346 == V353, V353 == V359, V359 == V365, V365 == V371, V371 == V377, V377 == V383, V383 == V389, V389 == V395, V395 == V401, V401 == V408, V408 == V415, V415 == V422, V422 == V428, V428 == V434, V434 == V440, V440 == V446, V446 == V452, V452 == V458, V458 == V464, V464 == V471, V471 == V478, V478 == V485, V485 == V492, V492 == V498, V498 == V504, V504 == V510, V510 == V516, V516 == V522, V522 == V528, V528 == V534, V534 == V541, V541 == V548, V548 == V555, V555 == V561, V561 == V567, V567 == V573, V573 == V579, V579 == V585, V585 == V591, V591 == V597, V597 == V604, V604 == V611, V611 == V618, V618 == V625, V625 == V631, V631 == V637, V637 == V643, V643 == V649, V649 == V655, V655 == V661, V661 == V667, V667 == V674, V674 == V681, V681 == V688, V688 == V695, V695 == V701, V701 == V707, V707 == V713, V713 == V719, V719 == V725, V725 == V731, V731 == V737, V737 == V744, V5 == V11, V11 == V18, V18 == V25, V25 == V32, V32 == V38, V38 == V44, V44 == V50, V50 == V62, V62 == V68, V68 == V74, V74 == V81, V81 == V87, V87 == V94, V94 == V101, V101 == V108, V108 == V114, V114 == V120, V120 == V126, V126 == V138, V138 == V144, V144 == V150, V150 == V157, V157 == V163, V163 == V170, V170 == V177, V177 == V184, V184 == V190, V190 == V196, V196 == V202, V202 == V214, V214 == V220, V220 == V226, V226 == V233, V233 == V239, V239 == V246, V246 == V253, V253 == V260, V260 == V266, V266 == V272, V272 == V278, V278 == V290, V290 == V296, V296 == V302, V302 == V309, V309 == V315, V315 == V321, V321 == V327, V327 == V333, V333 == V340, V340 == V347, V347 == V354, V354 == V360, V360 == V366, V366 == V372, V372 == V378, V378 == V384, V384 == V396, V396 == V402, V402 == V409, V409 == V416, V416 == V423, V423 == V429, V429 == V435, V435 == V441, V441 == V447, V447 == V453, V453 == V465, V465 == V741, V741 == V472, V472 == V479, V479 == V486, V486 == V493, V493 == V499, V499 == V505, V505 == V511, V511 == V517, V517 == V523, V523 == V535, V535 == V542, V542 == V549, V549 == V556, V556 == V562, V562 == V568, V568 == V574, V574 == V586, V586 == V592, V592 == V598, V598 == V605, V605 == V612, V612 == V619, V619 == V626, V626 == V632, V632 == V638, V638 == V644, V644 == V656, V656 == V662, V662 == V668, V668 == V675, V675 == V682, V682 == V689, V689 == V696, V696 == V702, V702 == V708, V708 == V714, V714 == V726, V726 == V732, V732 == V738, V738 == V745, V6 == V12, V12 == V19, V19 == V26, V26 == V33, V33 == V39, V39 == V45, V45 == V51, V51 == V56, V56 == V75, V75 == V82, V82 == V88, V88 == V95, V95 == V102, V102 == V109, V109 == V115, V115 == V121, V121 == V127, V127 == V132, V132 == V151, V151 == V158, V158 == V164, V164 == V171, V171 == V178, V178 == V185, V185 == V191, V191 == V197, V197 == V203, V203 == V208, V208 == V227, V227 == V234, V234 == V240, V240 == V247, V247 == V254, V254 == V261, V261 == V267, V267 == V273, V273 == V279, V279 == V284, V284 == V303, V303 == V310, V310 == V316, V316 == V322, V322 == V328, V328 == V334, V334 == V341, V341 == V348, V348 == V355, V355 == V361, V361 == V367, V367 == V373, V373 == V390, V390 == V397, V397 == V403, V403 == V410, V410 == V417, V417 == V424, V424 == V430, V430 == V436, V436 == V442, V442 == V459, V459 == V466, V466 == V473, V473 == V480, V480 == V487, V487 == V494, V494 == V500, V500 == V506, V506 == V512, V512 == V529, V529 == V536, V536 == V543, V543 == V550, V550 == V557, V557 == V563, V563 == V569, V569 == V575, V575 == V580, V580 == V599, V599 == V606, V606 == V613, V613 == V620, V620 == V627, V627 == V633, V633 == V639, V639 == V645, V645 == V650, V650 == V669, V669 == V676, V676 == V683, V683 == V690, V690 == V697, V697 == V703, V703 == V709, V709 == V715, V715 == V720, V720 == V739, V739 == V746, V7 == V13, V13 == V20, V20 == V27, V27 == V57, V57 == V63, V63 == V69, V69 == V76, V76 == V83, V83 == V89, V89 == V96, V96 == V103, V103 == V133, V133 == V139, V139 == V145, V145 == V152, V152 == V159, V159 == V165, V165 == V172, V172 == V179, V179 == V209, V209 == V215, V215 == V221, V221 == V228, V228 == V235, V235 == V241, V241 == V248, V248 == V255, V255 == V285, V285 == V291, V291 == V297, V297 == V304, V304 == V311, V311 == V317, V317 == V323, V323 == V329, V329 == V335, V335 == V342, V342 == V349, V349 == V379, V379 == V385, V385 == V391, V391 == V398, V398 == V404, V404 == V411, V411 == V418, V418 == V448, V448 == V454, V454 == V460, V460 == V467, V467 == V474, V474 == V481, V481 == V488, V488 == V518, V518 == V524, V524 == V530, V530 == V537, V537 == V544, V544 == V551, V551 == V581, V581 == V587, V587 == V593, V593 == V600, V600 == V607, V607 == V614, V614 == V621, V621 == V651, V651 == V657, V657 == V663, V663 == V670, V670 == V677, V677 == V684, V684 == V691, V691 == V721, V721 == V727, V727 == V733, V733 == V740, V740 == V747; #4612 ), references = 1, size of lhs = 13:
% 71.67/71.83 old-{F}(V0), P_skc12-{F}(V0), street-{F}(V1), P_skc13-{F}(V1), event-{F}(V2), P_skc14-{F}(V2), chevy-{F}(V3), P_skc9-{F}(V3), hollywood-{F}(V4), P_skc15-{F}(V4), P_skc11-{F}(V4), event-{F}(V5), P_skc10-{F}(V5) | FALSE
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #6027: mergings( V1 == V7, V7 == V13, V13 == V18, V18 == V24, V24 == V30, V30 == V36, V36 == V42, V42 == V48, V48 == V54, V54 == V59, V59 == V64, V64 == V69, V69 == V75, V75 == V81, V81 == V86, V86 == V92, V92 == V98, V98 == V104, V104 == V110, V110 == V116, V116 == V122, V122 == V127, V127 == V132, V132 == V137, V137 == V143, V143 == V149, V149 == V154, V154 == V160, V160 == V166, V166 == V172, V172 == V178, V178 == V184, V184 == V190, V190 == V195, V195 == V200, V200 == V205, V205 == V211, V211 == V217, V217 == V222, V222 == V228, V228 == V234, V234 == V240, V240 == V246, V246 == V252, V252 == V258, V258 == V263, V263 == V268, V268 == V273, V273 == V279, V279 == V285, V285 == V290, V290 == V300, V300 == V305, V305 == V311, V311 == V317, V317 == V323, V323 == V329, V329 == V335, V335 == V341, V341 == V346, V346 == V351, V351 == V356, V356 == V362, V362 == V367, V367 == V373, V373 == V379, V379 == V385, V385 == V391, V391 == V397, V397 == V403, V403 == V408, V408 == V413, V413 == V418, V418 == V424, V424 == V430, V430 == V436, V436 == V442, V442 == V448, V448 == V454, V454 == V460, V460 == V466, V466 == V471, V471 == V476, V476 == V481, V481 == V487, V487 == V493, V493 == V499, V499 == V505, V505 == V511, V511 == V517, V517 == V523, V523 == V528, V528 == V533, V533 == V538, V538 == V544, V544 == V550, V550 == V556, V556 == V562, V562 == V568, V568 == V574, V574 == V580, V580 == V586, V586 == V591, V591 == V596, V596 == V601, V601 == V607, V607 == V613, V613 == V619, V619 == V625, V625 == V631, V631 == V637, V637 == V643, V643 == V649, V649 == V654, V654 == V659, V659 == V664, V664 == V670, V2 == V8, V8 == V14, V14 == V19, V19 == V25, V25 == V31, V31 == V37, V37 == V43, V43 == V49, V49 == V55, V55 == V60, V60 == V65, V65 == V70, V70 == V76, V76 == V82, V82 == V87, V87 == V93, V93 == V99, V99 == V105, V105 == V111, V111 == V117, V117 == V123, V123 == V128, V128 == V133, V133 == V138, V138 == V144, V144 == V150, V150 == V155, V155 == V161, V161 == V167, V167 == V173, V173 == V179, V179 == V185, V185 == V191, V191 == V196, V196 == V201, V201 == V206, V206 == V212, V212 == V218, V218 == V223, V223 == V229, V229 == V235, V235 == V241, V241 == V247, V247 == V253, V253 == V259, V259 == V264, V264 == V269, V269 == V274, V274 == V280, V280 == V286, V286 == V291, V291 == V295, V295 == V306, V306 == V312, V312 == V318, V318 == V324, V324 == V330, V330 == V336, V336 == V342, V342 == V347, V347 == V352, V352 == V357, V357 == V368, V368 == V374, V374 == V380, V380 == V386, V386 == V392, V392 == V398, V398 == V404, V404 == V409, V409 == V414, V414 == V419, V419 == V425, V425 == V431, V431 == V437, V437 == V443, V443 == V449, V449 == V455, V455 == V461, V461 == V467, V467 == V472, V472 == V477, V477 == V482, V482 == V488, V488 == V494, V494 == V500, V500 == V506, V506 == V512, V512 == V518, V518 == V524, V524 == V529, V529 == V534, V534 == V539, V539 == V545, V545 == V551, V551 == V557, V557 == V563, V563 == V569, V569 == V575, V575 == V581, V581 == V587, V587 == V592, V592 == V597, V597 == V602, V602 == V608, V608 == V614, V614 == V620, V620 == V626, V626 == V632, V632 == V638, V638 == V644, V644 == V650, V650 == V655, V655 == V660, V660 == V665, V665 == V671, V3 == V9, V9 == V15, V15 == V20, V20 == V26, V26 == V32, V32 == V38, V38 == V44, V44 == V50, V50 == V56, V56 == V61, V61 == V66, V66 == V71, V71 == V77, V77 == V83, V83 == V88, V88 == V94, V94 == V100, V100 == V106, V106 == V112, V112 == V118, V118 == V124, V124 == V129, V129 == V134, V134 == V139, V139 == V145, V145 == V156, V156 == V162, V162 == V168, V168 == V174, V174 == V180, V180 == V186, V186 == V192, V192 == V197, V197 == V202, V202 == V207, V207 == V213, V213 == V219, V219 == V224, V224 == V230, V230 == V236, V236 == V242, V242 == V248, V248 == V254, V254 == V260, V260 == V265, V265 == V270, V270 == V275, V275 == V281, V281 == V287, V287 == V296, V296 == V301, V301 == V307, V307 == V313, V313 == V319, V319 == V325, V325 == V331, V331 == V337, V337 == V343, V343 == V348, V348 == V353, V353 == V358, V358 == V363, V363 == V369, V369 == V375, V375 == V381, V381 == V387, V387 == V393, V393 == V399, V399 == V405, V405 == V410, V410 == V415, V415 == V420, V420 == V426, V426 == V432, V432 == V438, V438 == V444, V444 == V450, V450 == V456, V456 == V462, V462 == V468, V468 == V473, V473 == V478, V478 == V483, V483 == V489, V489 == V495, V495 == V501, V501 == V507, V507 == V513, V513 == V519, V519 == V525, V525 == V530, V530 == V535, V535 == V540, V540 == V546, V546 == V552, V552 == V558, V558 == V564, V564 == V570, V570 == V576, V576 == V582, V582 == V588, V588 == V593, V593 == V598, V598 == V603, V603 == V609, V609 == V615, V615 == V621, V621 == V627, V627 == V633, V633 == V639, V639 == V645, V645 == V651, V651 == V656, V656 == V661, V661 == V666, V666 == V672, V4 == V10, V10 == V21, V21 == V27, V27 == V33, V33 == V39, V39 == V45, V45 == V51, V51 == V57, V57 == V62, V62 == V67, V67 == V72, V72 == V78, V78 == V89, V89 == V95, V95 == V101, V101 == V107, V107 == V113, V113 == V119, V119 == V125, V125 == V130, V130 == V135, V135 == V140, V140 == V146, V146 == V151, V151 == V157, V157 == V163, V163 == V169, V169 == V175, V175 == V181, V181 == V187, V187 == V193, V193 == V198, V198 == V203, V203 == V208, V208 == V214, V214 == V225, V225 == V231, V231 == V237, V237 == V243, V243 == V249, V249 == V255, V255 == V261, V261 == V266, V266 == V271, V271 == V276, V276 == V282, V282 == V292, V292 == V297, V297 == V302, V302 == V308, V308 == V314, V314 == V320, V320 == V326, V326 == V332, V332 == V338, V338 == V344, V344 == V349, V349 == V354, V354 == V359, V359 == V364, V364 == V370, V370 == V376, V376 == V382, V382 == V388, V388 == V394, V394 == V400, V400 == V406, V406 == V411, V411 == V416, V416 == V421, V421 == V427, V427 == V433, V433 == V439, V439 == V445, V445 == V451, V451 == V457, V457 == V463, V463 == V469, V469 == V474, V474 == V479, V479 == V484, V484 == V490, V490 == V496, V496 == V502, V502 == V508, V508 == V514, V514 == V520, V520 == V526, V526 == V531, V531 == V536, V536 == V541, V541 == V547, V547 == V553, V553 == V559, V559 == V565, V565 == V571, V571 == V577, V577 == V583, V583 == V589, V589 == V594, V594 == V599, V599 == V604, V604 == V610, V610 == V616, V616 == V622, V622 == V628, V628 == V634, V634 == V640, V640 == V646, V646 == V652, V652 == V657, V657 == V662, V662 == V667, V667 == V673, V5 == V11, V11 == V16, V16 == V22, V22 == V28, V28 == V34, V34 == V40, V40 == V46, V46 == V52, V52 == V63, V63 == V68, V68 == V73, V73 == V79, V79 == V84, V84 == V90, V90 == V96, V96 == V102, V102 == V108, V108 == V114, V114 == V120, V120 == V131, V131 == V136, V136 == V141, V141 == V147, V147 == V152, V152 == V158, V158 == V164, V164 == V170, V170 == V176, V176 == V182, V182 == V188, V188 == V199, V199 == V204, V204 == V209, V209 == V215, V215 == V220, V220 == V226, V226 == V232, V232 == V238, V238 == V244, V244 == V250, V250 == V256, V256 == V267, V267 == V272, V272 == V277, V277 == V283, V283 == V288, V288 == V293, V293 == V298, V298 == V303, V303 == V309, V309 == V315, V315 == V321, V321 == V327, V327 == V333, V333 == V339, V339 == V345, V345 == V350, V350 == V360, V360 == V365, V365 == V371, V371 == V377, V377 == V383, V383 == V389, V389 == V395, V395 == V401, V401 == V407, V407 == V412, V412 == V422, V422 == V670, V670 == V428, V428 == V434, V434 == V440, V440 == V446, V446 == V452, V452 == V458, V458 == V464, V464 == V470, V470 == V475, V475 == V485, V485 == V491, V491 == V497, V497 == V503, V503 == V509, V509 == V515, V515 == V521, V521 == V532, V532 == V537, V537 == V542, V542 == V548, V548 == V554, V554 == V560, V560 == V566, V566 == V572, V572 == V578, V578 == V584, V584 == V595, V595 == V600, V600 == V605, V605 == V611, V611 == V617, V617 == V623, V623 == V629, V629 == V635, V635 == V641, V641 == V647, V647 == V658, V658 == V663, V663 == V668, V668 == V674, V6 == V12, V12 == V17, V17 == V23, V23 == V29, V29 == V35, V35 == V41, V41 == V47, V47 == V53, V53 == V58, V58 == V74, V74 == V80, V80 == V85, V85 == V91, V91 == V97, V97 == V103, V103 == V109, V109 == V115, V115 == V121, V121 == V126, V126 == V142, V142 == V148, V148 == V153, V153 == V159, V159 == V165, V165 == V171, V171 == V177, V177 == V183, V183 == V189, V189 == V194, V194 == V210, V210 == V216, V216 == V221, V221 == V227, V227 == V233, V233 == V239, V239 == V245, V245 == V251, V251 == V257, V257 == V262, V262 == V278, V278 == V284, V284 == V289, V289 == V294, V294 == V299, V299 == V304, V304 == V310, V310 == V316, V316 == V322, V322 == V328, V328 == V334, V334 == V340, V340 == V355, V355 == V361, V361 == V366, V366 == V372, V372 == V378, V378 == V384, V384 == V390, V390 == V396, V396 == V402, V402 == V417, V417 == V423, V423 == V429, V429 == V435, V435 == V441, V441 == V447, V447 == V453, V453 == V459, V459 == V465, V465 == V480, V480 == V486, V486 == V492, V492 == V498, V498 == V504, V504 == V510, V510 == V516, V516 == V522, V522 == V527, V527 == V543, V543 == V549, V549 == V555, V555 == V561, V561 == V567, V567 == V573, V573 == V579, V579 == V585, V585 == V590, V590 == V606, V606 == V612, V612 == V618, V618 == V624, V624 == V630, V630 == V636, V636 == V642, V642 == V648, V648 == V653, V653 == V669, V669 == V675; #5356 ), references = 1, size of lhs = 11:
% 71.67/71.83 old-{F}(V0), P_skc12-{F}(V0), street-{F}(V1), P_skc13-{F}(V1), event-{F}(V2), P_skc14-{F}(V2), hollywood-{F}(V3), P_skc15-{F}(V3), P_skc11-{F}(V3), event-{F}(V4), P_skc10-{F}(V4) | FALSE
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #6607: mergings( V1 == V6, V6 == V11, V11 == V16, V16 == V20, V20 == V25, V25 == V30, V30 == V35, V35 == V40, V40 == V45, V45 == V50, V50 == V54, V54 == V59, V59 == V64, V64 == V69, V69 == V74, V74 == V78, V78 == V83, V83 == V88, V88 == V93, V93 == V98, V98 == V103, V103 == V108, V108 == V112, V112 == V117, V117 == V122, V122 == V127, V127 == V132, V132 == V136, V136 == V141, V141 == V146, V146 == V151, V151 == V156, V156 == V161, V161 == V166, V166 == V170, V170 == V175, V175 == V180, V180 == V185, V185 == V190, V190 == V194, V194 == V199, V199 == V204, V204 == V209, V209 == V214, V214 == V219, V219 == V224, V224 == V228, V228 == V233, V233 == V238, V238 == V243, V243 == V248, V248 == V252, V252 == V260, V260 == V264, V264 == V269, V269 == V274, V274 == V279, V279 == V284, V284 == V289, V289 == V294, V294 == V299, V299 == V304, V304 == V308, V308 == V313, V313 == V317, V317 == V322, V322 == V327, V327 == V332, V332 == V337, V337 == V342, V342 == V347, V347 == V352, V352 == V357, V357 == V361, V361 == V366, V366 == V371, V371 == V376, V376 == V381, V381 == V386, V386 == V391, V391 == V396, V396 == V401, V401 == V406, V406 == V411, V411 == V415, V415 == V420, V420 == V425, V425 == V430, V430 == V435, V435 == V440, V440 == V445, V445 == V450, V450 == V454, V454 == V459, V459 == V464, V464 == V469, V469 == V474, V474 == V479, V479 == V484, V484 == V489, V489 == V494, V494 == V499, V499 == V504, V504 == V508, V508 == V513, V513 == V518, V518 == V523, V523 == V528, V528 == V533, V533 == V538, V538 == V543, V543 == V548, V548 == V553, V553 == V558, V558 == V562, V562 == V567, V567 == V572, V572 == V577, V2 == V7, V7 == V12, V12 == V17, V17 == V21, V21 == V26, V26 == V31, V31 == V36, V36 == V41, V41 == V46, V46 == V51, V51 == V55, V55 == V60, V60 == V65, V65 == V70, V70 == V75, V75 == V79, V79 == V84, V84 == V89, V89 == V94, V94 == V99, V99 == V104, V104 == V109, V109 == V113, V113 == V118, V118 == V123, V123 == V128, V128 == V133, V133 == V137, V137 == V142, V142 == V147, V147 == V152, V152 == V157, V157 == V162, V162 == V167, V167 == V171, V171 == V176, V176 == V181, V181 == V186, V186 == V191, V191 == V195, V195 == V200, V200 == V205, V205 == V210, V210 == V215, V215 == V220, V220 == V225, V225 == V229, V229 == V234, V234 == V239, V239 == V244, V244 == V249, V249 == V253, V253 == V256, V256 == V265, V265 == V270, V270 == V275, V275 == V280, V280 == V285, V285 == V290, V290 == V295, V295 == V300, V300 == V305, V305 == V309, V309 == V318, V318 == V323, V323 == V328, V328 == V333, V333 == V338, V338 == V343, V343 == V348, V348 == V353, V353 == V358, V358 == V362, V362 == V367, V367 == V372, V372 == V377, V377 == V382, V382 == V387, V387 == V392, V392 == V397, V397 == V402, V402 == V407, V407 == V412, V412 == V416, V416 == V421, V421 == V426, V426 == V431, V431 == V436, V436 == V441, V441 == V446, V446 == V451, V451 == V455, V455 == V460, V460 == V465, V465 == V470, V470 == V475, V475 == V480, V480 == V485, V485 == V490, V490 == V495, V495 == V500, V500 == V505, V505 == V509, V509 == V514, V514 == V519, V519 == V524, V524 == V529, V529 == V534, V534 == V539, V539 == V544, V544 == V549, V549 == V554, V554 == V559, V559 == V563, V563 == V568, V568 == V573, V573 == V578, V3 == V8, V8 == V13, V13 == V18, V18 == V22, V22 == V27, V27 == V32, V32 == V37, V37 == V42, V42 == V47, V47 == V52, V52 == V56, V56 == V61, V61 == V66, V66 == V71, V71 == V76, V76 == V80, V80 == V85, V85 == V90, V90 == V95, V95 == V100, V100 == V105, V105 == V110, V110 == V114, V114 == V119, V119 == V124, V124 == V129, V129 == V138, V138 == V143, V143 == V148, V148 == V153, V153 == V158, V158 == V163, V163 == V168, V168 == V172, V172 == V177, V177 == V182, V182 == V187, V187 == V192, V192 == V196, V196 == V201, V201 == V206, V206 == V211, V211 == V216, V216 == V221, V221 == V226, V226 == V230, V230 == V235, V235 == V240, V240 == V245, V245 == V250, V250 == V257, V257 == V261, V261 == V266, V266 == V271, V271 == V276, V276 == V281, V281 == V286, V286 == V291, V291 == V296, V296 == V301, V301 == V306, V306 == V310, V310 == V314, V314 == V319, V319 == V324, V324 == V329, V329 == V334, V334 == V339, V339 == V344, V344 == V349, V349 == V354, V354 == V359, V359 == V363, V363 == V368, V368 == V373, V373 == V378, V378 == V383, V383 == V388, V388 == V393, V393 == V398, V398 == V403, V403 == V408, V408 == V413, V413 == V417, V417 == V422, V422 == V427, V427 == V432, V432 == V437, V437 == V442, V442 == V447, V447 == V452, V452 == V456, V456 == V461, V461 == V466, V466 == V471, V471 == V476, V476 == V481, V481 == V486, V486 == V491, V491 == V496, V496 == V501, V501 == V506, V506 == V510, V510 == V515, V515 == V520, V520 == V525, V525 == V530, V530 == V535, V535 == V540, V540 == V545, V545 == V550, V550 == V555, V555 == V560, V560 == V564, V564 == V569, V569 == V574, V574 == V579, V4 == V9, V9 == V14, V14 == V23, V23 == V28, V28 == V33, V33 == V38, V38 == V43, V43 == V48, V48 == V53, V53 == V57, V57 == V62, V62 == V67, V67 == V72, V72 == V81, V81 == V86, V86 == V91, V91 == V96, V96 == V101, V101 == V106, V106 == V111, V111 == V115, V115 == V120, V120 == V125, V125 == V130, V130 == V134, V134 == V139, V139 == V144, V144 == V149, V149 == V154, V154 == V159, V159 == V164, V164 == V169, V169 == V173, V173 == V178, V178 == V183, V183 == V188, V188 == V197, V197 == V202, V202 == V207, V207 == V212, V212 == V217, V217 == V222, V222 == V227, V227 == V231, V231 == V236, V236 == V241, V241 == V246, V246 == V254, V254 == V258, V258 == V262, V262 == V267, V267 == V272, V272 == V277, V277 == V282, V282 == V287, V287 == V292, V292 == V297, V297 == V302, V302 == V307, V307 == V311, V311 == V315, V315 == V320, V320 == V325, V325 == V330, V330 == V335, V335 == V340, V340 == V345, V345 == V350, V350 == V355, V355 == V360, V360 == V364, V364 == V369, V369 == V374, V374 == V379, V379 == V384, V384 == V389, V389 == V394, V394 == V399, V399 == V404, V404 == V409, V409 == V414, V414 == V418, V418 == V423, V423 == V428, V428 == V433, V433 == V438, V438 == V443, V443 == V448, V448 == V453, V453 == V457, V457 == V462, V462 == V467, V467 == V472, V472 == V477, V477 == V482, V482 == V487, V487 == V492, V492 == V497, V497 == V502, V502 == V507, V507 == V511, V511 == V516, V516 == V521, V521 == V526, V526 == V531, V531 == V536, V536 == V541, V541 == V546, V546 == V551, V551 == V556, V556 == V561, V561 == V565, V565 == V570, V570 == V575, V575 == V580, V5 == V10, V10 == V15, V15 == V19, V19 == V24, V24 == V29, V29 == V34, V34 == V39, V39 == V44, V44 == V49, V49 == V58, V58 == V63, V63 == V68, V68 == V73, V73 == V77, V77 == V82, V82 == V87, V87 == V92, V92 == V97, V97 == V102, V102 == V107, V107 == V116, V116 == V121, V121 == V126, V126 == V131, V131 == V135, V135 == V140, V140 == V145, V145 == V150, V150 == V155, V155 == V160, V160 == V165, V165 == V174, V174 == V179, V179 == V184, V184 == V189, V189 == V193, V193 == V198, V198 == V203, V203 == V208, V208 == V213, V213 == V218, V218 == V223, V223 == V232, V232 == V237, V237 == V242, V242 == V247, V247 == V251, V251 == V255, V255 == V259, V259 == V263, V263 == V268, V268 == V273, V273 == V278, V278 == V283, V283 == V288, V288 == V293, V293 == V298, V298 == V303, V303 == V312, V312 == V316, V316 == V321, V321 == V326, V326 == V331, V331 == V336, V336 == V341, V341 == V346, V346 == V351, V351 == V356, V356 == V365, V365 == V577, V577 == V370, V370 == V375, V375 == V380, V380 == V385, V385 == V390, V390 == V395, V395 == V400, V400 == V405, V405 == V410, V410 == V419, V419 == V424, V424 == V429, V429 == V434, V434 == V439, V439 == V444, V444 == V449, V449 == V458, V458 == V463, V463 == V468, V468 == V473, V473 == V478, V478 == V483, V483 == V488, V488 == V493, V493 == V498, V498 == V503, V503 == V512, V512 == V517, V517 == V522, V522 == V527, V527 == V532, V532 == V537, V537 == V542, V542 == V547, V547 == V552, V552 == V557, V557 == V566, V566 == V571, V571 == V576, V576 == V581; #6029 ), references = 1, size of lhs = 9:
% 71.67/71.83 old-{F}(V0), P_skc12-{F}(V0), street-{F}(V1), P_skc13-{F}(V1), event-{F}(V2), P_skc14-{F}(V2), hollywood-{F}(V3), P_skc15-{F}(V3), P_skc11-{F}(V3) | FALSE
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #6698: mergings( V0 == V8, V8 == V15, V15 == V22, V22 == V29, V29 == V36, V36 == V43, V43 == V50, V50 == V57, V57 == V64, V64 == V71, V71 == V79, V1 == V9, V9 == V16, V16 == V23, V23 == V30, V30 == V37, V37 == V44, V44 == V51, V51 == V58, V58 == V65, V65 == V72, V72 == V80, V2 == V10, V10 == V17, V17 == V24, V24 == V31, V31 == V38, V38 == V45, V45 == V52, V52 == V59, V59 == V66, V66 == V73, V73 == V81, V3 == V11, V11 == V18, V18 == V25, V25 == V32, V32 == V39, V39 == V46, V46 == V53, V53 == V60, V60 == V67, V67 == V74, V74 == V82, V4 == V12, V12 == V19, V19 == V26, V26 == V33, V33 == V40, V40 == V47, V47 == V61, V61 == V68, V68 == V75, V75 == V83, V5 == V13, V13 == V20, V20 == V27, V27 == V34, V34 == V41, V41 == V48, V48 == V54, V54 == V76, V76 == V84, V6 == V14, V14 == V21, V21 == V55, V55 == V62, V62 == V69, V69 == V77, V77 == V85, V7 == V28, V28 == V35, V35 == V42, V42 == V49, V49 == V56, V56 == V63, V63 == V70, V70 == V78, V78 == V86; #6618 ), references = 1, size of lhs = 12:
% 71.67/71.83 chevy-{F}(V0), P_skc9-{F}(V0), lonely-{F}(V1), P_skc8-{F}(V1), hollywood-{F}(V2), P_skc11-{F}(V2), event-{F}(V3), P_skc10-{F}(V3), P_skc15-{F}(V4), P_skc14-{F}(V5), P_skc13-{F}(V6), P_skc12-{F}(V7) | chevy-{T}(V7)
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #6789: mergings( V0 == V8, V8 == V15, V15 == V22, V22 == V29, V29 == V36, V36 == V43, V43 == V50, V50 == V57, V57 == V64, V64 == V71, V71 == V79, V1 == V9, V9 == V16, V16 == V23, V23 == V30, V30 == V37, V37 == V44, V44 == V51, V51 == V58, V58 == V65, V65 == V72, V72 == V80, V2 == V10, V10 == V17, V17 == V24, V24 == V31, V31 == V38, V38 == V45, V45 == V52, V52 == V59, V59 == V66, V66 == V73, V73 == V81, V3 == V11, V11 == V18, V18 == V25, V25 == V32, V32 == V39, V39 == V46, V46 == V53, V53 == V60, V60 == V67, V67 == V74, V74 == V82, V4 == V12, V12 == V19, V19 == V26, V26 == V33, V33 == V40, V40 == V47, V47 == V61, V61 == V68, V68 == V75, V75 == V83, V5 == V13, V13 == V20, V20 == V27, V27 == V34, V34 == V41, V41 == V48, V48 == V54, V54 == V76, V76 == V84, V6 == V14, V14 == V21, V21 == V55, V55 == V62, V62 == V69, V69 == V77, V77 == V85, V7 == V28, V28 == V35, V35 == V42, V42 == V49, V49 == V56, V56 == V63, V63 == V70, V70 == V78, V78 == V86; #6709 ), references = 1, size of lhs = 12:
% 71.67/71.83 chevy-{F}(V0), P_skc9-{F}(V0), lonely-{F}(V1), P_skc8-{F}(V1), hollywood-{F}(V2), P_skc11-{F}(V2), event-{F}(V3), P_skc10-{F}(V3), P_skc15-{F}(V4), P_skc14-{F}(V5), P_skc13-{F}(V6), P_skc12-{F}(V7) | city-{T}(V4)
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #6880: mergings( V0 == V8, V8 == V15, V15 == V22, V22 == V29, V29 == V36, V36 == V43, V43 == V50, V50 == V57, V57 == V64, V64 == V71, V71 == V79, V1 == V9, V9 == V16, V16 == V23, V23 == V30, V30 == V37, V37 == V44, V44 == V51, V51 == V58, V58 == V65, V65 == V72, V72 == V80, V2 == V10, V10 == V17, V17 == V24, V24 == V31, V31 == V38, V38 == V45, V45 == V52, V52 == V59, V59 == V66, V66 == V73, V73 == V81, V3 == V11, V11 == V18, V18 == V25, V25 == V32, V32 == V39, V39 == V46, V46 == V53, V53 == V60, V60 == V67, V67 == V74, V74 == V82, V4 == V12, V12 == V19, V19 == V26, V26 == V33, V33 == V40, V40 == V47, V47 == V61, V61 == V68, V68 == V75, V75 == V83, V5 == V13, V13 == V20, V20 == V27, V27 == V34, V34 == V41, V41 == V48, V48 == V54, V54 == V76, V76 == V84, V6 == V14, V14 == V21, V21 == V55, V55 == V62, V62 == V69, V69 == V77, V77 == V85, V7 == V28, V28 == V35, V35 == V42, V42 == V49, V49 == V56, V56 == V63, V63 == V70, V70 == V78, V78 == V86; #6800 ), references = 1, size of lhs = 12:
% 71.67/71.83 chevy-{F}(V0), P_skc9-{F}(V0), lonely-{F}(V1), P_skc8-{F}(V1), hollywood-{F}(V2), P_skc11-{F}(V2), event-{F}(V3), P_skc10-{F}(V3), P_skc15-{F}(V4), P_skc14-{F}(V5), P_skc13-{F}(V6), P_skc12-{F}(V7) | way-{T}(V6)
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #6971: mergings( V0 == V8, V8 == V15, V15 == V22, V22 == V29, V29 == V36, V36 == V43, V43 == V50, V50 == V57, V57 == V64, V64 == V71, V71 == V79, V1 == V9, V9 == V16, V16 == V23, V23 == V30, V30 == V37, V37 == V44, V44 == V51, V51 == V58, V58 == V65, V65 == V72, V72 == V80, V2 == V10, V10 == V17, V17 == V24, V24 == V31, V31 == V38, V38 == V45, V45 == V52, V52 == V59, V59 == V66, V66 == V73, V73 == V81, V3 == V11, V11 == V18, V18 == V25, V25 == V32, V32 == V39, V39 == V46, V46 == V53, V53 == V60, V60 == V67, V67 == V74, V74 == V82, V4 == V12, V12 == V19, V19 == V26, V26 == V33, V33 == V40, V40 == V47, V47 == V61, V61 == V68, V68 == V75, V75 == V83, V5 == V13, V13 == V20, V20 == V27, V27 == V34, V34 == V41, V41 == V48, V48 == V54, V54 == V76, V76 == V84, V6 == V14, V14 == V21, V21 == V55, V55 == V62, V62 == V69, V69 == V77, V77 == V85, V7 == V28, V28 == V35, V35 == V42, V42 == V49, V49 == V56, V56 == V63, V63 == V70, V70 == V78, V78 == V86; #6891 ), references = 1, size of lhs = 12:
% 71.67/71.83 chevy-{F}(V0), P_skc9-{F}(V0), lonely-{F}(V1), P_skc8-{F}(V1), hollywood-{F}(V2), P_skc11-{F}(V2), event-{F}(V3), P_skc10-{F}(V3), P_skc15-{F}(V4), P_skc14-{F}(V5), P_skc13-{F}(V6), P_skc12-{F}(V7) | down-{T}(V5,V6)
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #7070: mergings( V0 == V8, V8 == V17, V17 == V24, V24 == V31, V31 == V38, V38 == V45, V45 == V52, V52 == V59, V59 == V66, V66 == V73, V73 == V80, V80 == V88, V1 == V18, V18 == V25, V25 == V32, V32 == V39, V39 == V46, V46 == V53, V53 == V60, V60 == V67, V67 == V74, V74 == V81, V81 == V89, V2 == V10, V10 == V19, V19 == V26, V26 == V33, V33 == V40, V40 == V47, V47 == V54, V54 == V61, V61 == V68, V68 == V75, V75 == V82, V82 == V90, V3 == V11, V11 == V20, V20 == V27, V27 == V34, V34 == V41, V41 == V48, V48 == V55, V55 == V62, V62 == V69, V69 == V76, V76 == V83, V83 == V91, V4 == V12, V12 == V21, V21 == V28, V28 == V35, V35 == V42, V42 == V49, V49 == V56, V56 == V70, V70 == V77, V77 == V84, V84 == V92, V5 == V13, V13 == V22, V22 == V29, V29 == V36, V36 == V43, V43 == V50, V50 == V57, V57 == V63, V63 == V85, V85 == V93, V6 == V14, V14 == V23, V23 == V30, V30 == V64, V64 == V71, V71 == V78, V78 == V86, V86 == V94, V7 == V15, V15 == V37, V37 == V44, V44 == V51, V51 == V58, V58 == V65, V65 == V72, V72 == V79, V79 == V87, V87 == V95; #6983 ), references = 1, size of lhs = 28:
% 71.67/71.83 chevy-{F}(V0), car-{F}(V0), white-{F}(V0), dirty-{F}(V0), old-{F}(V0), P_skc12-{F}(V0), city-{F}(V1), hollywood-{F}(V1), P_skc15-{F}(V1), event-{F}(V2), P_skc14-{F}(V2), street-{F}(V3), way-{F}(V3), lonely-{F}(V3), down-{F}(V2,V3), lonely-{F}(V4), way-{F}(V4), street-{F}(V4), down-{F}(V2,V4), chevy-{F}(V5), P_skc9-{F}(V5), lonely-{F}(V6), P_skc8-{F}(V6), hollywood-{F}(V7), P_skc11-{F}(V7), event-{F}(V8), P_skc10-{F}(V8), P_skc13-{F}(V9) | ssSkC0-{T}()
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #7573: mergings( V1 == V11, V11 == V17, V17 == V23, V23 == V29, V29 == V32, V32 == V38, V38 == V45, V45 == V52, V52 == V58, V58 == V64, V64 == V70, V70 == V76, V76 == V82, V82 == V88, V88 == V94, V94 == V101, V101 == V114, V114 == V121, V121 == V128, V128 == V134, V134 == V140, V140 == V146, V146 == V152, V152 == V158, V158 == V164, V164 == V170, V170 == V177, V177 == V184, V184 == V190, V190 == V197, V197 == V204, V204 == V210, V210 == V216, V216 == V222, V222 == V228, V228 == V234, V234 == V240, V240 == V246, V246 == V253, V253 == V260, V260 == V266, V266 == V273, V273 == V280, V280 == V286, V286 == V292, V292 == V298, V298 == V304, V304 == V310, V310 == V316, V316 == V322, V322 == V329, V329 == V336, V336 == V342, V342 == V349, V349 == V356, V356 == V363, V363 == V369, V369 == V375, V375 == V381, V381 == V387, V387 == V393, V393 == V399, V399 == V405, V405 == V412, V412 == V419, V419 == V426, V426 == V433, V433 == V439, V439 == V445, V445 == V451, V451 == V457, V457 == V463, V463 == V469, V469 == V475, V475 == V482, V2 == V12, V12 == V18, V18 == V24, V24 == V30, V30 == V33, V33 == V39, V39 == V46, V46 == V53, V53 == V59, V59 == V65, V65 == V71, V71 == V77, V77 == V83, V83 == V89, V89 == V95, V95 == V102, V102 == V108, V108 == V115, V115 == V122, V122 == V129, V129 == V135, V135 == V141, V141 == V147, V147 == V153, V153 == V159, V159 == V165, V165 == V171, V171 == V178, V178 == V185, V185 == V191, V191 == V198, V198 == V205, V205 == V211, V211 == V217, V217 == V223, V223 == V229, V229 == V235, V235 == V241, V241 == V247, V247 == V254, V254 == V267, V267 == V274, V274 == V281, V281 == V287, V287 == V293, V293 == V299, V299 == V305, V305 == V311, V311 == V317, V317 == V323, V323 == V330, V330 == V343, V343 == V350, V350 == V357, V357 == V364, V364 == V370, V370 == V376, V376 == V382, V382 == V388, V388 == V394, V394 == V400, V400 == V406, V406 == V413, V413 == V420, V420 == V427, V427 == V434, V434 == V440, V440 == V446, V446 == V452, V452 == V458, V458 == V464, V464 == V470, V470 == V476, V476 == V483, V3 == V13, V13 == V19, V19 == V31, V31 == V34, V34 == V40, V40 == V47, V47 == V54, V54 == V60, V60 == V66, V66 == V72, V72 == V78, V78 == V84, V84 == V90, V90 == V96, V96 == V103, V103 == V109, V109 == V116, V116 == V123, V123 == V130, V130 == V136, V136 == V142, V142 == V148, V148 == V154, V154 == V160, V160 == V166, V166 == V172, V172 == V179, V179 == V192, V192 == V199, V199 == V206, V206 == V212, V212 == V218, V218 == V224, V224 == V230, V230 == V236, V236 == V242, V242 == V248, V248 == V255, V255 == V261, V261 == V268, V268 == V275, V275 == V282, V282 == V288, V288 == V294, V294 == V300, V300 == V306, V306 == V312, V312 == V318, V318 == V324, V324 == V331, V331 == V337, V337 == V344, V344 == V351, V351 == V358, V358 == V365, V365 == V371, V371 == V377, V377 == V383, V383 == V389, V389 == V395, V395 == V401, V401 == V407, V407 == V414, V414 == V421, V421 == V428, V428 == V435, V435 == V441, V441 == V447, V447 == V453, V453 == V459, V459 == V465, V465 == V471, V471 == V477, V477 == V484, V4 == V25, V25 == V41, V41 == V48, V48 == V55, V55 == V61, V61 == V67, V67 == V73, V73 == V79, V79 == V85, V85 == V91, V91 == V97, V97 == V104, V104 == V110, V110 == V117, V117 == V124, V124 == V131, V131 == V137, V137 == V143, V143 == V149, V149 == V155, V155 == V161, V161 == V167, V167 == V173, V173 == V180, V180 == V186, V186 == V193, V193 == V200, V200 == V207, V207 == V213, V213 == V219, V219 == V225, V225 == V231, V231 == V237, V237 == V243, V243 == V249, V249 == V256, V256 == V262, V262 == V269, V269 == V276, V276 == V283, V283 == V289, V289 == V295, V295 == V301, V301 == V307, V307 == V313, V313 == V319, V319 == V325, V325 == V332, V332 == V338, V338 == V345, V345 == V352, V352 == V359, V359 == V366, V366 == V372, V372 == V378, V378 == V384, V384 == V390, V390 == V396, V396 == V402, V402 == V408, V408 == V415, V415 == V422, V422 == V429, V429 == V436, V436 == V442, V442 == V448, V448 == V454, V454 == V460, V460 == V466, V466 == V472, V472 == V478, V478 == V485, V5 == V9, V9 == V15, V15 == V21, V21 == V27, V27 == V35, V35 == V42, V42 == V49, V49 == V56, V56 == V62, V62 == V68, V68 == V74, V74 == V86, V86 == V92, V92 == V98, V98 == V105, V105 == V111, V111 == V118, V118 == V125, V125 == V132, V132 == V138, V138 == V144, V144 == V150, V150 == V162, V162 == V168, V168 == V174, V174 == V181, V181 == V187, V187 == V194, V194 == V201, V201 == V208, V208 == V214, V214 == V220, V220 == V226, V226 == V238, V238 == V244, V244 == V250, V250 == V257, V257 == V263, V263 == V270, V270 == V277, V277 == V284, V284 == V290, V290 == V296, V296 == V302, V302 == V314, V314 == V320, V320 == V326, V326 == V333, V333 == V339, V339 == V346, V346 == V353, V353 == V360, V360 == V367, V367 == V373, V373 == V379, V379 == V385, V385 == V397, V397 == V403, V403 == V409, V409 == V416, V416 == V423, V423 == V430, V430 == V437, V437 == V443, V443 == V449, V449 == V455, V455 == V467, V467 == V473, V473 == V479, V479 == V486, V6 == V10, V10 == V16, V16 == V22, V22 == V28, V28 == V36, V36 == V43, V43 == V50, V50 == V57, V57 == V63, V63 == V69, V69 == V75, V75 == V80, V80 == V99, V99 == V106, V106 == V112, V112 == V119, V119 == V126, V126 == V133, V133 == V139, V139 == V145, V145 == V151, V151 == V156, V156 == V175, V175 == V182, V182 == V188, V188 == V195, V195 == V202, V202 == V209, V209 == V215, V215 == V221, V221 == V227, V227 == V232, V232 == V251, V251 == V258, V258 == V264, V264 == V271, V271 == V278, V278 == V285, V285 == V291, V291 == V297, V297 == V303, V303 == V308, V308 == V327, V327 == V334, V334 == V340, V340 == V347, V347 == V354, V354 == V361, V361 == V368, V368 == V374, V374 == V380, V380 == V386, V386 == V391, V391 == V410, V410 == V417, V417 == V424, V424 == V431, V431 == V438, V438 == V444, V444 == V450, V450 == V456, V456 == V461, V461 == V480, V480 == V487, V7 == V8, V8 == V14, V14 == V20, V20 == V26, V26 == V37, V37 == V44, V44 == V51, V51 == V81, V81 == V87, V87 == V93, V93 == V100, V100 == V107, V107 == V113, V113 == V120, V120 == V127, V127 == V157, V157 == V163, V163 == V169, V169 == V176, V176 == V183, V183 == V189, V189 == V196, V196 == V203, V203 == V233, V233 == V239, V239 == V245, V245 == V252, V252 == V259, V259 == V265, V265 == V272, V272 == V279, V279 == V309, V309 == V315, V315 == V321, V321 == V328, V328 == V335, V335 == V341, V341 == V348, V348 == V355, V355 == V362, V362 == V392, V392 == V398, V398 == V404, V404 == V411, V411 == V418, V418 == V425, V425 == V432, V432 == V462, V462 == V468, V468 == V474, V474 == V481, V481 == V488; #7091 ), references = 1, size of lhs = 14:
% 71.67/71.83 street-{F}(V0), P_skc13-{F}(V0), old-{F}(V1), P_skc12-{F}(V1), hollywood-{F}(V2), P_skc15-{F}(V2), event-{F}(V3), P_skc14-{F}(V3), chevy-{F}(V4), P_skc9-{F}(V4), hollywood-{F}(V5), P_skc11-{F}(V5), event-{F}(V6), P_skc10-{F}(V6) | FALSE
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #8011: mergings( V1 == V7, V7 == V15, V15 == V20, V20 == V25, V25 == V30, V30 == V33, V33 == V38, V38 == V44, V44 == V50, V50 == V56, V56 == V62, V62 == V68, V68 == V74, V74 == V79, V79 == V84, V84 == V89, V89 == V95, V95 == V106, V106 == V112, V112 == V118, V118 == V124, V124 == V130, V130 == V136, V136 == V142, V142 == V147, V147 == V152, V152 == V157, V157 == V163, V163 == V169, V169 == V174, V174 == V180, V180 == V186, V186 == V192, V192 == V198, V198 == V204, V204 == V210, V210 == V215, V215 == V220, V220 == V225, V225 == V231, V231 == V237, V237 == V242, V242 == V248, V248 == V254, V254 == V260, V260 == V266, V266 == V272, V272 == V278, V278 == V283, V283 == V288, V288 == V293, V293 == V299, V299 == V305, V305 == V310, V310 == V316, V316 == V322, V322 == V328, V328 == V334, V334 == V340, V340 == V346, V346 == V352, V352 == V357, V357 == V362, V362 == V367, V367 == V373, V373 == V379, V379 == V385, V385 == V391, V391 == V397, V397 == V403, V403 == V409, V409 == V415, V415 == V420, V420 == V425, V425 == V430, V430 == V436, V2 == V8, V8 == V16, V16 == V21, V21 == V26, V26 == V31, V31 == V34, V34 == V39, V39 == V45, V45 == V51, V51 == V57, V57 == V63, V63 == V69, V69 == V75, V75 == V80, V80 == V85, V85 == V90, V90 == V96, V96 == V101, V101 == V107, V107 == V113, V113 == V119, V119 == V125, V125 == V131, V131 == V137, V137 == V143, V143 == V148, V148 == V153, V153 == V158, V158 == V164, V164 == V170, V170 == V175, V175 == V181, V181 == V187, V187 == V193, V193 == V199, V199 == V205, V205 == V211, V211 == V216, V216 == V221, V221 == V226, V226 == V232, V232 == V243, V243 == V249, V249 == V255, V255 == V261, V261 == V267, V267 == V273, V273 == V279, V279 == V284, V284 == V289, V289 == V294, V294 == V300, V300 == V311, V311 == V317, V317 == V323, V323 == V329, V329 == V335, V335 == V341, V341 == V347, V347 == V353, V353 == V358, V358 == V363, V363 == V368, V368 == V374, V374 == V380, V380 == V386, V386 == V392, V392 == V398, V398 == V404, V404 == V410, V410 == V416, V416 == V421, V421 == V426, V426 == V431, V431 == V437, V3 == V9, V9 == V17, V17 == V22, V22 == V32, V32 == V35, V35 == V40, V40 == V46, V46 == V52, V52 == V58, V58 == V64, V64 == V70, V70 == V76, V76 == V81, V81 == V86, V86 == V91, V91 == V97, V97 == V102, V102 == V108, V108 == V114, V114 == V120, V120 == V126, V126 == V132, V132 == V138, V138 == V144, V144 == V149, V149 == V154, V154 == V159, V159 == V165, V165 == V176, V176 == V182, V182 == V188, V188 == V194, V194 == V200, V200 == V206, V206 == V212, V212 == V217, V217 == V222, V222 == V227, V227 == V233, V233 == V238, V238 == V244, V244 == V250, V250 == V256, V256 == V262, V262 == V268, V268 == V274, V274 == V280, V280 == V285, V285 == V290, V290 == V295, V295 == V301, V301 == V306, V306 == V312, V312 == V318, V318 == V324, V324 == V330, V330 == V336, V336 == V342, V342 == V348, V348 == V354, V354 == V359, V359 == V364, V364 == V369, V369 == V375, V375 == V381, V381 == V387, V387 == V393, V393 == V399, V399 == V405, V405 == V411, V411 == V417, V417 == V422, V422 == V427, V427 == V432, V432 == V438, V4 == V10, V10 == V27, V27 == V41, V41 == V47, V47 == V53, V53 == V59, V59 == V65, V65 == V71, V71 == V77, V77 == V82, V82 == V87, V87 == V92, V92 == V98, V98 == V103, V103 == V109, V109 == V115, V115 == V121, V121 == V127, V127 == V133, V133 == V139, V139 == V145, V145 == V150, V150 == V155, V155 == V160, V160 == V166, V166 == V171, V171 == V177, V177 == V183, V183 == V189, V189 == V195, V195 == V201, V201 == V207, V207 == V213, V213 == V218, V218 == V223, V223 == V228, V228 == V234, V234 == V239, V239 == V245, V245 == V251, V251 == V257, V257 == V263, V263 == V269, V269 == V275, V275 == V281, V281 == V286, V286 == V291, V291 == V296, V296 == V302, V302 == V307, V307 == V313, V313 == V319, V319 == V325, V325 == V331, V331 == V337, V337 == V343, V343 == V349, V349 == V355, V355 == V360, V360 == V365, V365 == V370, V370 == V376, V376 == V382, V382 == V388, V388 == V394, V394 == V400, V400 == V406, V406 == V412, V412 == V418, V418 == V423, V423 == V428, V428 == V433, V433 == V439, V5 == V11, V11 == V13, V13 == V18, V18 == V23, V23 == V28, V28 == V36, V36 == V42, V42 == V48, V48 == V54, V54 == V60, V60 == V66, V66 == V72, V72 == V83, V83 == V88, V88 == V93, V93 == V99, V99 == V104, V104 == V110, V110 == V116, V116 == V122, V122 == V128, V128 == V134, V134 == V140, V140 == V151, V151 == V156, V156 == V161, V161 == V167, V167 == V172, V172 == V178, V178 == V184, V184 == V190, V190 == V196, V196 == V202, V202 == V208, V208 == V219, V219 == V224, V224 == V229, V229 == V235, V235 == V240, V240 == V246, V246 == V252, V252 == V258, V258 == V264, V264 == V270, V270 == V276, V276 == V287, V287 == V292, V292 == V297, V297 == V303, V303 == V308, V308 == V314, V314 == V320, V320 == V326, V326 == V332, V332 == V338, V338 == V344, V344 == V350, V350 == V361, V361 == V366, V366 == V371, V371 == V377, V377 == V383, V383 == V389, V389 == V395, V395 == V401, V401 == V407, V407 == V413, V413 == V424, V424 == V429, V429 == V434, V434 == V440, V6 == V12, V12 == V14, V14 == V19, V19 == V24, V24 == V29, V29 == V37, V37 == V43, V43 == V49, V49 == V55, V55 == V61, V61 == V67, V67 == V73, V73 == V78, V78 == V94, V94 == V100, V100 == V105, V105 == V111, V111 == V117, V117 == V123, V123 == V129, V129 == V135, V135 == V141, V141 == V146, V146 == V162, V162 == V168, V168 == V173, V173 == V179, V179 == V185, V185 == V191, V191 == V197, V197 == V203, V203 == V209, V209 == V214, V214 == V230, V230 == V236, V236 == V241, V241 == V247, V247 == V253, V253 == V259, V259 == V265, V265 == V271, V271 == V277, V277 == V282, V282 == V298, V298 == V304, V304 == V309, V309 == V315, V315 == V321, V321 == V327, V327 == V333, V333 == V339, V339 == V345, V345 == V351, V351 == V356, V356 == V372, V372 == V378, V378 == V384, V384 == V390, V390 == V396, V396 == V402, V402 == V408, V408 == V414, V414 == V419, V419 == V435, V435 == V441; #7575 ), references = 2, size of lhs = 12:
% 71.67/71.83 street-{F}(V0), P_skc13-{F}(V0), old-{F}(V1), P_skc12-{F}(V1), hollywood-{F}(V2), P_skc15-{F}(V2), event-{F}(V3), P_skc14-{F}(V3), hollywood-{F}(V4), P_skc11-{F}(V4), event-{F}(V5), P_skc10-{F}(V5) | FALSE
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #8019: mergings( V1 == V8, V2 == V9, V3 == V6, V4 == V7, V5 == V10; #8013 ), references = 1, size of lhs = 10:
% 71.67/71.83 street-{F}(V0), P_skc13-{F}(V0), old-{F}(V1), P_skc12-{F}(V1), hollywood-{F}(V2), P_skc15-{F}(V2), event-{F}(V3), P_skc14-{F}(V3), hollywood-{F}(V4), P_skc11-{F}(V4) | FALSE
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #8030: mergings( V1 == V5, V5 == V11, V2 == V6, V6 == V12, V3 == V7, V7 == V9, V4 == V8, V8 == V10; #8021 ), references = 1, size of lhs = 8:
% 71.67/71.83 street-{F}(V0), P_skc13-{F}(V0), old-{F}(V1), P_skc12-{F}(V1), hollywood-{F}(V2), P_skc15-{F}(V2), event-{F}(V3), P_skc14-{F}(V3) | FALSE
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #8042: mergings( V1 == V4, V4 == V7, V7 == V11, V2 == V5, V5 == V8, V8 == V12, V3 == V6, V6 == V9, V9 == V10; #8032 ), references = 1, size of lhs = 6:
% 71.67/71.83 street-{F}(V0), P_skc13-{F}(V0), hollywood-{F}(V1), P_skc15-{F}(V1), event-{F}(V2), P_skc14-{F}(V2) | FALSE
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #8053: mergings( V1 == V3, V3 == V5, V5 == V7, V7 == V9, V2 == V4, V4 == V6, V6 == V8, V8 == V10; #8044 ), references = 1, size of lhs = 4:
% 71.67/71.83 hollywood-{F}(V0), P_skc15-{F}(V0), event-{F}(V1), P_skc14-{F}(V1) | FALSE
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #8061: mergings( V1 == V2, V2 == V3, V3 == V4, V4 == V5, V5 == V6; #8055 ), references = 1, size of lhs = 2:
% 71.67/71.83 hollywood-{F}(V0), P_skc15-{F}(V0) | FALSE
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 #8064: exists( #30, #8062 ), references = 1, size of lhs = 0:
% 71.67/71.83 FALSE | FALSE
% 71.67/71.83 (used 0 times, uses = {})
% 71.67/71.83
% 71.67/71.83 number of learnt formulas = 43
% 71.67/71.83
% 71.67/71.83
% 71.67/71.83 % SZS output end Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 71.67/71.83
% 71.67/71.83 randbase = 1
%------------------------------------------------------------------------------