%------------------------------------------------------------------------------
% File : Geo-III---2018C
% Problem : SYN704-1 : TPTP v8.1.0. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : geo -tptp_input -nonempty -inputfile %s
% Computer : n017.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:25:16 EDT 2022
% Result : Unsatisfiable 8.55s 8.72s
% Output : Refutation 8.55s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.11 % Problem : SYN704-1 : TPTP v8.1.0. Released v2.5.0.
% 0.03/0.12 % Command : geo -tptp_input -nonempty -inputfile %s
% 0.11/0.33 % Computer : n017.cluster.edu
% 0.11/0.33 % Model : x86_64 x86_64
% 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.33 % Memory : 8042.1875MB
% 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.33 % CPULimit : 300
% 0.11/0.33 % WCLimit : 300
% 0.11/0.33 % DateTime : Sat Jul 23 02:30:59 EDT 2022
% 0.11/0.33 % CPUTime :
% 8.55/8.72 GeoParameters:
% 8.55/8.72
% 8.55/8.72 tptp_input = 1
% 8.55/8.72 tptp_output = 0
% 8.55/8.72 nonempty = 1
% 8.55/8.72 inputfile = /export/starexec/sandbox2/benchmark/theBenchmark.p
% 8.55/8.72 includepath = /export/starexec/sandbox2/solver/bin/../../benchmark/
% 8.55/8.72
% 8.55/8.72
% 8.55/8.72 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 8.55/8.72 % SZS output start Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 8.55/8.72
% 8.55/8.72 RuleSystem INPUT:
% 8.55/8.72
% 8.55/8.72 Initial Rules:
% 8.55/8.72 #0: input, references = 3, size of lhs = 1:
% 8.55/8.72 #-{F} V0 | p11-{T}(V0,V0)
% 8.55/8.72 (used 0 times, uses = {})
% 8.55/8.72
% 8.55/8.72 #1: input, references = 3, size of lhs = 1:
% 8.55/8.72 #-{F} V0 | p9-{T}(V0,V0)
% 8.55/8.72 (used 0 times, uses = {})
% 8.55/8.72
% 8.55/8.72 #2: input, references = 4, size of lhs = 1:
% 8.55/8.72 #-{F} V0 | p7-{T}(V0,V0)
% 8.55/8.72 (used 0 times, uses = {})
% 8.55/8.72
% 8.55/8.72 #3: input, references = 3, size of lhs = 1:
% 8.55/8.72 #-{F} V0 | p6-{T}(V0,V0)
% 8.55/8.72 (used 0 times, uses = {})
% 8.55/8.72
% 8.55/8.72 #4: input, references = 3, size of lhs = 1:
% 8.55/8.72 #-{F} V0 | p45-{T}(V0,V0)
% 8.55/8.72 (used 0 times, uses = {})
% 8.55/8.72
% 8.55/8.72 #5: input, references = 3, size of lhs = 1:
% 8.55/8.72 #-{F} V0 | p43-{T}(V0,V0)
% 8.55/8.72 (used 0 times, uses = {})
% 8.55/8.72
% 8.55/8.72 #6: input, references = 3, size of lhs = 1:
% 8.55/8.72 #-{F} V0 | p41-{T}(V0,V0)
% 8.55/8.72 (used 0 times, uses = {})
% 8.55/8.72
% 8.55/8.72 #7: input, references = 3, size of lhs = 1:
% 8.55/8.72 #-{F} V0 | p4-{T}(V0,V0)
% 8.55/8.72 (used 0 times, uses = {})
% 8.55/8.72
% 8.55/8.72 #8: input, references = 3, size of lhs = 1:
% 8.55/8.72 #-{F} V0 | p39-{T}(V0,V0)
% 8.55/8.72 (used 0 times, uses = {})
% 8.55/8.72
% 8.55/8.72 #9: input, references = 3, size of lhs = 1:
% 8.55/8.72 #-{F} V0 | p37-{T}(V0,V0)
% 8.55/8.72 (used 0 times, uses = {})
% 8.55/8.72
% 8.55/8.72 #10: input, references = 3, size of lhs = 1:
% 8.55/8.72 #-{F} V0 | p35-{T}(V0,V0)
% 8.55/8.72 (used 0 times, uses = {})
% 8.55/8.72
% 8.55/8.72 #11: input, references = 3, size of lhs = 1:
% 8.55/8.72 #-{F} V0 | p33-{T}(V0,V0)
% 8.55/8.72 (used 0 times, uses = {})
% 8.55/8.72
% 8.55/8.72 #12: input, references = 3, size of lhs = 1:
% 8.55/8.72 #-{F} V0 | p31-{T}(V0,V0)
% 8.55/8.72 (used 0 times, uses = {})
% 8.55/8.72
% 8.55/8.72 #13: input, references = 3, size of lhs = 1:
% 8.55/8.72 #-{F} V0 | p3-{T}(V0,V0)
% 8.55/8.72 (used 0 times, uses = {})
% 8.55/8.72
% 8.55/8.72 #14: input, references = 3, size of lhs = 1:
% 8.55/8.72 #-{F} V0 | p29-{T}(V0,V0)
% 8.55/8.72 (used 0 times, uses = {})
% 8.55/8.72
% 8.55/8.72 #15: input, references = 3, size of lhs = 1:
% 8.55/8.72 #-{F} V0 | p27-{T}(V0,V0)
% 8.55/8.72 (used 0 times, uses = {})
% 8.55/8.72
% 8.55/8.72 #16: input, references = 3, size of lhs = 1:
% 8.55/8.72 #-{F} V0 | p25-{T}(V0,V0)
% 8.55/8.72 (used 0 times, uses = {})
% 8.55/8.72
% 8.55/8.72 #17: input, references = 3, size of lhs = 1:
% 8.55/8.72 #-{F} V0 | p23-{T}(V0,V0)
% 8.55/8.72 (used 0 times, uses = {})
% 8.55/8.72
% 8.55/8.72 #18: input, references = 3, size of lhs = 1:
% 8.55/8.72 #-{F} V0 | p21-{T}(V0,V0)
% 8.55/8.72 (used 0 times, uses = {})
% 8.55/8.72
% 8.55/8.72 #19: input, references = 4, size of lhs = 1:
% 8.55/8.72 #-{F} V0 | p2-{T}(V0,V0)
% 8.55/8.72 (used 0 times, uses = {})
% 8.55/8.72
% 8.55/8.72 #20: input, references = 3, size of lhs = 1:
% 8.55/8.72 #-{F} V0 | p19-{T}(V0,V0)
% 8.55/8.72 (used 0 times, uses = {})
% 8.55/8.72
% 8.55/8.72 #21: input, references = 3, size of lhs = 1:
% 8.55/8.72 #-{F} V0 | p17-{T}(V0,V0)
% 8.55/8.72 (used 0 times, uses = {})
% 8.55/8.72
% 8.55/8.72 #22: input, references = 3, size of lhs = 1:
% 8.55/8.72 #-{F} V0 | p15-{T}(V0,V0)
% 8.55/8.72 (used 0 times, uses = {})
% 8.55/8.72
% 8.55/8.72 #23: input, references = 3, size of lhs = 1:
% 8.55/8.72 #-{F} V0 | p14-{T}(V0,V0)
% 8.55/8.72 (used 0 times, uses = {})
% 8.55/8.72
% 8.55/8.72 #24: input, references = 3, size of lhs = 1:
% 8.55/8.72 #-{F} V0 | p12-{T}(V0,V0)
% 8.55/8.72 (used 0 times, uses = {})
% 8.55/8.72
% 8.55/8.72 #25: input, references = 4, size of lhs = 2:
% 8.55/8.72 P_c54-{F}(V0), P_c55-{F}(V1) | p7-{T}(V0,V1)
% 8.55/8.72 (used 0 times, uses = {})
% 8.55/8.72
% 8.55/8.72 #26: input, references = 3, size of lhs = 4:
% 8.55/8.72 P_c54-{F}(V0), P_c55-{F}(V1), p11-{F}(V4,V2), p11-{F}(V4,V3) | p11-{T}(V2,V3)
% 8.55/8.72 (used 0 times, uses = {})
% 8.55/8.72
% 8.55/8.72 #27: input, references = 3, size of lhs = 4:
% 8.55/8.72 P_c54-{F}(V0), P_c55-{F}(V1), p9-{F}(V4,V2), p9-{F}(V4,V3) | p9-{T}(V2,V3)
% 8.55/8.72 (used 0 times, uses = {})
% 8.55/8.72
% 8.55/8.72 #28: input, references = 4, size of lhs = 4:
% 8.55/8.72 P_c54-{F}(V0), P_c55-{F}(V1), p7-{F}(V4,V2), p7-{F}(V4,V3) | p7-{T}(V2,V3)
% 8.55/8.72 (used 0 times, uses = {})
% 8.55/8.72
% 8.55/8.72 #29: input, references = 3, size of lhs = 4:
% 8.55/8.72 P_c54-{F}(V0), P_c55-{F}(V1), p6-{F}(V4,V2), p6-{F}(V4,V3) | p6-{T}(V2,V3)
% 8.55/8.72 (used 0 times, uses = {})
% 8.55/8.72
% 8.55/8.72 #30: input, references = 3, size of lhs = 4:
% 8.55/8.72 P_c54-{F}(V0), P_c55-{F}(V1), p45-{F}(V4,V2), p45-{F}(V4,V3) | p45-{T}(V2,V3)
% 8.55/8.72 (used 0 times, uses = {})
% 8.55/8.72
% 8.55/8.72 #31: input, references = 3, size of lhs = 4:
% 8.55/8.72 P_c54-{F}(V0), P_c55-{F}(V1), p43-{F}(V4,V2), p43-{F}(V4,V3) | p43-{T}(V2,V3)
% 8.55/8.72 (used 0 times, uses = {})
% 8.55/8.72
% 8.55/8.72 #32: input, references = 3, size of lhs = 4:
% 8.55/8.72 P_c54-{F}(V0), P_c55-{F}(V1), p41-{F}(V4,V2), p41-{F}(V4,V3) | p41-{T}(V2,V3)
% 8.55/8.72 (used 0 times, uses = {})
% 8.55/8.72
% 8.55/8.72 #33: input, references = 4, size of lhs = 4:
% 8.55/8.72 P_c54-{F}(V0), P_c55-{F}(V1), p4-{F}(V4,V2), p4-{F}(V4,V3) | p4-{T}(V2,V3)
% 8.55/8.72 (used 0 times, uses = {})
% 8.55/8.72
% 8.55/8.72 #34: input, references = 3, size of lhs = 4:
% 8.55/8.72 P_c54-{F}(V0), P_c55-{F}(V1), p39-{F}(V4,V2), p39-{F}(V4,V3) | p39-{T}(V2,V3)
% 8.55/8.72 (used 0 times, uses = {})
% 8.55/8.72
% 8.55/8.72 #35: input, references = 3, size of lhs = 4:
% 8.55/8.72 P_c54-{F}(V0), P_c55-{F}(V1), p37-{F}(V4,V2), p37-{F}(V4,V3) | p37-{T}(V2,V3)
% 8.55/8.72 (used 0 times, uses = {})
% 8.55/8.72
% 8.55/8.72 #36: input, references = 3, size of lhs = 4:
% 8.55/8.72 P_c54-{F}(V0), P_c55-{F}(V1), p35-{F}(V4,V2), p35-{F}(V4,V3) | p35-{T}(V2,V3)
% 8.55/8.72 (used 0 times, uses = {})
% 8.55/8.72
% 8.55/8.72 #37: input, references = 3, size of lhs = 4:
% 8.55/8.72 P_c54-{F}(V0), P_c55-{F}(V1), p33-{F}(V4,V2), p33-{F}(V4,V3) | p33-{T}(V2,V3)
% 8.55/8.72 (used 0 times, uses = {})
% 8.55/8.72
% 8.55/8.72 #38: input, references = 3, size of lhs = 4:
% 8.55/8.72 P_c54-{F}(V0), P_c55-{F}(V1), p31-{F}(V4,V2), p31-{F}(V4,V3) | p31-{T}(V2,V3)
% 8.55/8.72 (used 0 times, uses = {})
% 8.55/8.72
% 8.55/8.72 #39: input, references = 3, size of lhs = 4:
% 8.55/8.72 P_c54-{F}(V0), P_c55-{F}(V1), p3-{F}(V4,V2), p3-{F}(V4,V3) | p3-{T}(V2,V3)
% 8.55/8.72 (used 0 times, uses = {})
% 8.55/8.72
% 8.55/8.72 #40: input, references = 3, size of lhs = 4:
% 8.55/8.72 P_c54-{F}(V0), P_c55-{F}(V1), p29-{F}(V4,V2), p29-{F}(V4,V3) | p29-{T}(V2,V3)
% 8.55/8.72 (used 0 times, uses = {})
% 8.55/8.72
% 8.55/8.72 #41: input, references = 3, size of lhs = 4:
% 8.55/8.72 P_c54-{F}(V0), P_c55-{F}(V1), p27-{F}(V4,V2), p27-{F}(V4,V3) | p27-{T}(V2,V3)
% 8.55/8.72 (used 0 times, uses = {})
% 8.55/8.72
% 8.55/8.72 #42: input, references = 3, size of lhs = 4:
% 8.55/8.72 P_c54-{F}(V0), P_c55-{F}(V1), p25-{F}(V4,V2), p25-{F}(V4,V3) | p25-{T}(V2,V3)
% 8.55/8.72 (used 0 times, uses = {})
% 8.55/8.72
% 8.55/8.72 #43: input, references = 3, size of lhs = 4:
% 8.55/8.72 P_c54-{F}(V0), P_c55-{F}(V1), p23-{F}(V4,V2), p23-{F}(V4,V3) | p23-{T}(V2,V3)
% 8.55/8.72 (used 0 times, uses = {})
% 8.55/8.72
% 8.55/8.72 #44: input, references = 3, size of lhs = 4:
% 8.55/8.72 P_c54-{F}(V0), P_c55-{F}(V1), p21-{F}(V4,V2), p21-{F}(V4,V3) | p21-{T}(V2,V3)
% 8.55/8.72 (used 0 times, uses = {})
% 8.55/8.72
% 8.55/8.72 #45: input, references = 3, size of lhs = 4:
% 8.55/8.72 P_c54-{F}(V0), P_c55-{F}(V1), p2-{F}(V4,V2), p2-{F}(V4,V3) | p2-{T}(V2,V3)
% 8.55/8.72 (used 0 times, uses = {})
% 8.55/8.72
% 8.55/8.72 #46: input, references = 3, size of lhs = 4:
% 8.55/8.72 P_c54-{F}(V0), P_c55-{F}(V1), p19-{F}(V4,V2), p19-{F}(V4,V3) | p19-{T}(V2,V3)
% 8.55/8.72 (used 0 times, uses = {})
% 8.55/8.72
% 8.55/8.72 #47: input, references = 3, size of lhs = 4:
% 8.55/8.72 P_c54-{F}(V0), P_c55-{F}(V1), p17-{F}(V4,V2), p17-{F}(V4,V3) | p17-{T}(V2,V3)
% 8.55/8.72 (used 0 times, uses = {})
% 8.55/8.72
% 8.55/8.72 #48: input, references = 3, size of lhs = 4:
% 8.55/8.72 P_c54-{F}(V0), P_c55-{F}(V1), p15-{F}(V4,V2), p15-{F}(V4,V3) | p15-{T}(V2,V3)
% 8.55/8.72 (used 0 times, uses = {})
% 8.55/8.72
% 8.55/8.72 #49: input, references = 3, size of lhs = 4:
% 8.55/8.72 P_c54-{F}(V0), P_c55-{F}(V1), p14-{F}(V4,V2), p14-{F}(V4,V3) | p14-{T}(V2,V3)
% 8.55/8.72 (used 0 times, uses = {})
% 8.55/8.72
% 8.55/8.72 #50: input, references = 3, size of lhs = 4:
% 8.55/8.72 P_c54-{F}(V0), P_c55-{F}(V1), p12-{F}(V4,V2), p12-{F}(V4,V3) | p12-{T}(V2,V3)
% 8.55/8.72 (used 0 times, uses = {})
% 8.55/8.72
% 8.55/8.72 #51: input, references = 7, size of lhs = 8:
% 8.55/8.72 P_c54-{F}(V0), P_c55-{F}(V1), P_c56-{F}(V2), P_f26-{F}(V2,V3,V7), P_f24-{F}(V7,V4,V8), P_f22-{F}(V8,V5,V9), P_f20-{F}(V9,V6,V10), p47-{F}(V10,V6) | FALSE
% 8.55/8.72 (used 0 times, uses = {})
% 8.55/8.72
% 8.55/8.72 #52: input, references = 6, size of lhs = 6:
% 8.55/8.72 P_c54-{F}(V0), P_c55-{F}(V1), P_c56-{F}(V2), p47-{F}(V3,V4), p7-{F}(V4,V5), p4-{F}(V3,V6) | p47-{T}(V6,V5)
% 8.55/8.72 (used 0 times, uses = {})
% 8.55/8.72
% 8.55/8.72 #53: input, references = 3, size of lhs = 7:
% 8.55/8.72 P_c54-{F}(V0), P_c55-{F}(V1), P_c56-{F}(V2), p15-{F}(V3,V4), P_f16-{F}(V6,V3,V7), P_f16-{F}(V5,V4,V8), p14-{F}(V6,V5) | p11-{T}(V7,V8)
% 8.55/8.72 (used 0 times, uses = {})
% 8.55/8.72
% 8.55/8.72 #54: input, references = 4, size of lhs = 7:
% 8.55/8.72 P_c54-{F}(V0), P_c55-{F}(V1), P_c56-{F}(V2), p3-{F}(V3,V4), P_f10-{F}(V6,V3,V7), P_f10-{F}(V5,V4,V8), p9-{F}(V6,V5) | p6-{T}(V7,V8)
% 8.55/8.72 (used 0 times, uses = {})
% 8.55/8.72
% 8.55/8.72 #55: input, references = 3, size of lhs = 7:
% 8.55/8.72 P_c54-{F}(V0), P_c55-{F}(V1), P_c56-{F}(V2), p4-{F}(V3,V4), P_f46-{F}(V6,V3,V7), P_f46-{F}(V5,V4,V8), p45-{F}(V6,V5) | p43-{T}(V7,V8)
% 8.55/8.72 (used 0 times, uses = {})
% 8.55/8.72
% 8.55/8.72 #56: input, references = 3, size of lhs = 7:
% 8.55/8.72 P_c54-{F}(V0), P_c55-{F}(V1), P_c56-{F}(V2), p15-{F}(V3,V4), P_f44-{F}(V6,V3,V7), P_f44-{F}(V5,V4,V8), p43-{F}(V6,V5) | p41-{T}(V7,V8)
% 8.55/8.72 (used 0 times, uses = {})
% 8.55/8.72
% 8.55/8.72 #57: input, references = 8, size of lhs = 7:
% 8.55/8.72 P_c54-{F}(V0), P_c55-{F}(V1), P_c56-{F}(V2), p3-{F}(V3,V4), P_f5-{F}(V6,V3,V7), P_f5-{F}(V5,V4,V8), p2-{F}(V6,V5) | p4-{T}(V7,V8)
% 8.55/8.72 (used 0 times, uses = {})
% 8.55/8.72
% 8.55/8.72 #58: input, references = 3, size of lhs = 7:
% 8.55/8.72 P_c54-{F}(V0), P_c55-{F}(V1), P_c56-{F}(V2), p7-{F}(V3,V4), P_f20-{F}(V6,V3,V7), P_f20-{F}(V5,V4,V8), p19-{F}(V6,V5) | p4-{T}(V7,V8)
% 8.55/8.72 (used 0 times, uses = {})
% 8.55/8.72
% 8.55/8.72 #59: input, references = 3, size of lhs = 7:
% 8.55/8.72 P_c54-{F}(V0), P_c55-{F}(V1), P_c56-{F}(V2), p12-{F}(V3,V4), P_f42-{F}(V6,V3,V7), P_f42-{F}(V5,V4,V8), p41-{F}(V6,V5) | p39-{T}(V7,V8)
% 8.55/8.72 (used 0 times, uses = {})
% 8.55/8.72
% 8.55/8.72 #60: input, references = 3, size of lhs = 7:
% 8.55/8.72 P_c54-{F}(V0), P_c55-{F}(V1), P_c56-{F}(V2), p7-{F}(V3,V4), P_f38-{F}(V6,V3,V7), P_f38-{F}(V5,V4,V8), p12-{F}(V6,V5) | p37-{T}(V7,V8)
% 8.55/8.72 (used 0 times, uses = {})
% 8.55/8.72
% 8.55/8.72 #61: input, references = 3, size of lhs = 7:
% 8.55/8.72 P_c54-{F}(V0), P_c55-{F}(V1), P_c56-{F}(V2), p4-{F}(V3,V4), P_f36-{F}(V6,V3,V7), P_f36-{F}(V5,V4,V8), p35-{F}(V6,V5) | p33-{T}(V7,V8)
% 8.55/8.72 (used 0 times, uses = {})
% 8.55/8.72
% 8.55/8.72 #62: input, references = 3, size of lhs = 7:
% 8.55/8.72 P_c54-{F}(V0), P_c55-{F}(V1), P_c56-{F}(V2), p15-{F}(V3,V4), P_f34-{F}(V6,V3,V7), P_f34-{F}(V5,V4,V8), p33-{F}(V6,V5) | p31-{T}(V7,V8)
% 8.55/8.72 (used 0 times, uses = {})
% 8.55/8.72
% 8.55/8.72 #63: input, references = 4, size of lhs = 7:
% 8.55/8.72 P_c54-{F}(V0), P_c55-{F}(V1), P_c56-{F}(V2), p7-{F}(V3,V4), P_f8-{F}(V6,V3,V7), P_f8-{F}(V5,V4,V8), p6-{F}(V6,V5) | p3-{T}(V7,V8)
% 8.55/8.72 (used 0 times, uses = {})
% 8.55/8.72
% 8.55/8.72 #64: input, references = 3, size of lhs = 7:
% 8.55/8.72 P_c54-{F}(V0), P_c55-{F}(V1), P_c56-{F}(V2), p12-{F}(V3,V4), P_f13-{F}(V6,V3,V7), P_f13-{F}(V5,V4,V8), p11-{F}(V6,V5) | p3-{T}(V7,V8)
% 8.55/8.72 (used 0 times, uses = {})
% 8.55/8.72
% 8.55/8.72 #65: input, references = 3, size of lhs = 7:
% 8.55/8.72 P_c54-{F}(V0), P_c55-{F}(V1), P_c56-{F}(V2), p12-{F}(V3,V4), P_f32-{F}(V6,V3,V7), P_f32-{F}(V5,V4,V8), p31-{F}(V6,V5) | p29-{T}(V7,V8)
% 8.55/8.72 (used 0 times, uses = {})
% 8.55/8.72
% 8.55/8.72 #66: input, references = 3, size of lhs = 7:
% 8.55/8.72 P_c54-{F}(V0), P_c55-{F}(V1), P_c56-{F}(V2), p7-{F}(V3,V4), P_f28-{F}(V6,V3,V7), P_f28-{F}(V5,V4,V8), p15-{F}(V6,V5) | p27-{T}(V7,V8)
% 8.55/8.72 (used 0 times, uses = {})
% 8.55/8.72
% 8.55/8.72 #67: input, references = 3, size of lhs = 7:
% 8.55/8.72 P_c54-{F}(V0), P_c55-{F}(V1), P_c56-{F}(V2), p4-{F}(V3,V4), P_f26-{F}(V6,V3,V7), P_f26-{F}(V5,V4,V8), p25-{F}(V6,V5) | p23-{T}(V7,V8)
% 8.55/8.72 (used 0 times, uses = {})
% 8.55/8.72
% 8.55/8.72 #68: input, references = 3, size of lhs = 7:
% 8.55/8.72 P_c54-{F}(V0), P_c55-{F}(V1), P_c56-{F}(V2), p15-{F}(V3,V4), P_f24-{F}(V6,V3,V7), P_f24-{F}(V5,V4,V8), p23-{F}(V6,V5) | p21-{T}(V7,V8)
% 8.55/8.72 (used 0 times, uses = {})
% 8.55/8.72
% 8.55/8.72 #69: input, references = 3, size of lhs = 7:
% 8.55/8.72 P_c54-{F}(V0), P_c55-{F}(V1), P_c56-{F}(V2), p12-{F}(V3,V4), P_f22-{F}(V6,V3,V7), P_f22-{F}(V5,V4,V8), p21-{F}(V6,V5) | p19-{T}(V7,V8)
% 8.55/8.72 (used 0 times, uses = {})
% 8.55/8.72
% 8.55/8.72 #70: input, references = 3, size of lhs = 7:
% 8.55/8.73 P_c54-{F}(V0), P_c55-{F}(V1), P_c56-{F}(V2), p7-{F}(V3,V4), P_f30-{F}(V6,V3,V7), P_f30-{F}(V5,V4,V8), p29-{F}(V6,V5) | p15-{T}(V7,V8)
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #71: input, references = 3, size of lhs = 7:
% 8.55/8.73 P_c54-{F}(V0), P_c55-{F}(V1), P_c56-{F}(V2), p4-{F}(V3,V4), P_f18-{F}(V6,V3,V7), P_f18-{F}(V5,V4,V8), p17-{F}(V6,V5) | p14-{T}(V7,V8)
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #72: input, references = 3, size of lhs = 7:
% 8.55/8.73 P_c54-{F}(V0), P_c55-{F}(V1), P_c56-{F}(V2), p7-{F}(V3,V4), P_f40-{F}(V6,V3,V7), P_f40-{F}(V5,V4,V8), p39-{F}(V6,V5) | p12-{T}(V7,V8)
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #73: input, references = 5, size of lhs = 10:
% 8.55/8.73 P_c54-{F}(V0), P_c55-{F}(V1), P_c56-{F}(V2), P_c48-{F}(V3), P_c50-{F}(V4), P_f18-{F}(V4,V5,V7), P_f16-{F}(V7,V9,V10), P_f13-{F}(V10,V8,V11), P_f5-{F}(V3,V11,V12), p47-{F}(V12,V6) | p47-{T}(V5,V6)
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #74: input, references = 3, size of lhs = 10:
% 8.55/8.73 P_c54-{F}(V0), P_c55-{F}(V1), P_c56-{F}(V2), P_c48-{F}(V3), P_c50-{F}(V4), P_f26-{F}(V2,V5,V7), P_f24-{F}(V7,V10,V11), P_f22-{F}(V11,V9,V12), P_f20-{F}(V12,V8,V13), p47-{F}(V13,V6) | p47-{T}(V5,V6)
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #75: input, references = 3, size of lhs = 10:
% 8.55/8.73 P_c54-{F}(V0), P_c55-{F}(V1), P_c56-{F}(V2), P_c48-{F}(V3), P_c50-{F}(V4), P_f18-{F}(V4,V5,V7), p47-{F}(V5,V6), P_f16-{F}(V7,V9,V10), P_f13-{F}(V10,V8,V11), P_f5-{F}(V3,V11,V12) | p47-{T}(V12,V6)
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #76: input, references = 7, size of lhs = 15:
% 8.55/8.73 P_c54-{F}(V0), P_c55-{F}(V1), P_c56-{F}(V2), P_c48-{F}(V3), P_c50-{F}(V4), P_c49-{F}(V5), P_c51-{F}(V6), P_f18-{F}(V4,V6,V7), P_c52-{F}(V8), P_f16-{F}(V7,V8,V9), P_c53-{F}(V10), P_f13-{F}(V9,V10,V11), P_f10-{F}(V5,V11,V12), P_f8-{F}(V12,V0,V13), P_f5-{F}(V3,V13,V14) | p47-{T}(V14,V1)
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #77: input, references = 3, size of lhs = 27:
% 8.55/8.73 P_c54-{F}(V0), P_c55-{F}(V1), P_c56-{F}(V2), P_c48-{F}(V3), P_c50-{F}(V4), P_c49-{F}(V5), P_c51-{F}(V6), P_f18-{F}(V4,V6,V7), P_c52-{F}(V8), P_f16-{F}(V7,V8,V9), P_c53-{F}(V10), P_f13-{F}(V9,V10,V11), P_f10-{F}(V5,V11,V12), P_f8-{F}(V12,V0,V13), P_f5-{F}(V3,V13,V14), P_c57-{F}(V15), P_f36-{F}(V15,V16,V21), P_f34-{F}(V21,V17,V22), P_f32-{F}(V22,V18,V23), P_f30-{F}(V23,V19,V24), P_f28-{F}(V24,V20,V25), P_f28-{F}(V17,V20,V26), P_f26-{F}(V2,V16,V27), P_f24-{F}(V27,V17,V28), P_f22-{F}(V28,V18,V29), P_f20-{F}(V29,V19,V30), p47-{F}(V30,V20) | p27-{T}(V25,V26)
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #78: input, references = 3, size of lhs = 28:
% 8.55/8.73 P_c54-{F}(V0), P_c55-{F}(V1), P_c56-{F}(V2), P_c48-{F}(V3), P_c50-{F}(V4), P_c49-{F}(V5), P_c51-{F}(V6), P_f18-{F}(V4,V6,V7), P_c52-{F}(V8), P_f16-{F}(V7,V8,V9), P_c53-{F}(V10), P_f13-{F}(V9,V10,V11), P_f10-{F}(V5,V11,V12), P_f8-{F}(V12,V0,V13), P_f5-{F}(V3,V13,V14), P_c57-{F}(V15), P_c58-{F}(V16), P_f46-{F}(V16,V17,V22), P_f44-{F}(V22,V18,V23), P_f42-{F}(V23,V19,V24), P_f40-{F}(V24,V20,V25), P_f38-{F}(V25,V21,V26), P_f38-{F}(V19,V21,V27), P_f26-{F}(V2,V17,V28), P_f24-{F}(V28,V18,V29), P_f22-{F}(V29,V19,V30), P_f20-{F}(V30,V20,V31), p47-{F}(V31,V21) | p37-{T}(V26,V27)
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #79: input, references = 8, size of lhs = 37:
% 8.55/8.73 P_c54-{F}(V0), P_c55-{F}(V1), P_c56-{F}(V2), P_c48-{F}(V3), P_c50-{F}(V4), P_c49-{F}(V5), P_c51-{F}(V6), P_f18-{F}(V4,V6,V7), P_c52-{F}(V8), P_f16-{F}(V7,V8,V9), P_c53-{F}(V10), P_f13-{F}(V9,V10,V11), P_f10-{F}(V5,V11,V12), P_f8-{F}(V12,V0,V13), P_f5-{F}(V3,V13,V14), P_c57-{F}(V15), P_c58-{F}(V16), P_f18-{F}(V4,V17,V21), P_f16-{F}(V21,V18,V22), P_f13-{F}(V22,V19,V23), P_f10-{F}(V5,V23,V24), P_f8-{F}(V24,V20,V25), P_f26-{F}(V2,V17,V26), P_f24-{F}(V26,V18,V27), P_f22-{F}(V27,V19,V28), P_f20-{F}(V28,V20,V29), P_f18-{F}(V4,V29,V30), P_f36-{F}(V15,V17,V31), P_f34-{F}(V31,V18,V32), P_f32-{F}(V32,V19,V33), P_f30-{F}(V33,V20,V34), P_f16-{F}(V30,V34,V35), P_f46-{F}(V16,V17,V36), P_f44-{F}(V36,V18,V37), P_f42-{F}(V37,V19,V38), P_f40-{F}(V38,V20,V39), P_f13-{F}(V35,V39,V40) | p3-{T}(V25,V40)
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #80: input, references = 4, size of lhs = 0:
% 8.55/8.73 FALSE | EXISTS V0: P_c54-{T}(V0)
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #81: input, references = 4, size of lhs = 0:
% 8.55/8.73 FALSE | EXISTS V0: P_c55-{T}(V0)
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #82: input, references = 4, size of lhs = 2:
% 8.55/8.73 #-{F} V0, #-{F} V1 | EXISTS V2: P_f20-{T}(V0,V1,V2)
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #83: input, references = 4, size of lhs = 2:
% 8.55/8.73 #-{F} V0, #-{F} V1 | EXISTS V2: P_f22-{T}(V0,V1,V2)
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #84: input, references = 4, size of lhs = 2:
% 8.55/8.73 #-{F} V0, #-{F} V1 | EXISTS V2: P_f24-{T}(V0,V1,V2)
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #85: input, references = 4, size of lhs = 2:
% 8.55/8.73 #-{F} V0, #-{F} V1 | EXISTS V2: P_f26-{T}(V0,V1,V2)
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #86: input, references = 4, size of lhs = 0:
% 8.55/8.73 FALSE | EXISTS V0: P_c56-{T}(V0)
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #87: input, references = 6, size of lhs = 2:
% 8.55/8.73 #-{F} V0, #-{F} V1 | EXISTS V2: P_f16-{T}(V0,V1,V2)
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #88: input, references = 5, size of lhs = 2:
% 8.55/8.73 #-{F} V0, #-{F} V1 | EXISTS V2: P_f10-{T}(V0,V1,V2)
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #89: input, references = 4, size of lhs = 2:
% 8.55/8.73 #-{F} V0, #-{F} V1 | EXISTS V2: P_f46-{T}(V0,V1,V2)
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #90: input, references = 4, size of lhs = 2:
% 8.55/8.73 #-{F} V0, #-{F} V1 | EXISTS V2: P_f44-{T}(V0,V1,V2)
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #91: input, references = 9, size of lhs = 2:
% 8.55/8.73 #-{F} V0, #-{F} V1 | EXISTS V2: P_f5-{T}(V0,V1,V2)
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #92: input, references = 4, size of lhs = 2:
% 8.55/8.73 #-{F} V0, #-{F} V1 | EXISTS V2: P_f42-{T}(V0,V1,V2)
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #93: input, references = 3, size of lhs = 2:
% 8.55/8.73 #-{F} V0, #-{F} V1 | EXISTS V2: P_f38-{T}(V0,V1,V2)
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #94: input, references = 4, size of lhs = 2:
% 8.55/8.73 #-{F} V0, #-{F} V1 | EXISTS V2: P_f36-{T}(V0,V1,V2)
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #95: input, references = 4, size of lhs = 2:
% 8.55/8.73 #-{F} V0, #-{F} V1 | EXISTS V2: P_f34-{T}(V0,V1,V2)
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #96: input, references = 6, size of lhs = 2:
% 8.55/8.73 #-{F} V0, #-{F} V1 | EXISTS V2: P_f8-{T}(V0,V1,V2)
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #97: input, references = 5, size of lhs = 2:
% 8.55/8.73 #-{F} V0, #-{F} V1 | EXISTS V2: P_f13-{T}(V0,V1,V2)
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #98: input, references = 4, size of lhs = 2:
% 8.55/8.73 #-{F} V0, #-{F} V1 | EXISTS V2: P_f32-{T}(V0,V1,V2)
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #99: input, references = 3, size of lhs = 2:
% 8.55/8.73 #-{F} V0, #-{F} V1 | EXISTS V2: P_f28-{T}(V0,V1,V2)
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #100: input, references = 4, size of lhs = 2:
% 8.55/8.73 #-{F} V0, #-{F} V1 | EXISTS V2: P_f30-{T}(V0,V1,V2)
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #101: input, references = 5, size of lhs = 2:
% 8.55/8.73 #-{F} V0, #-{F} V1 | EXISTS V2: P_f18-{T}(V0,V1,V2)
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #102: input, references = 4, size of lhs = 2:
% 8.55/8.73 #-{F} V0, #-{F} V1 | EXISTS V2: P_f40-{T}(V0,V1,V2)
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #103: input, references = 4, size of lhs = 0:
% 8.55/8.73 FALSE | EXISTS V0: P_c48-{T}(V0)
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #104: input, references = 4, size of lhs = 0:
% 8.55/8.73 FALSE | EXISTS V0: P_c50-{T}(V0)
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #105: input, references = 4, size of lhs = 0:
% 8.55/8.73 FALSE | EXISTS V0: P_c49-{T}(V0)
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #106: input, references = 4, size of lhs = 0:
% 8.55/8.73 FALSE | EXISTS V0: P_c51-{T}(V0)
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #107: input, references = 4, size of lhs = 0:
% 8.55/8.73 FALSE | EXISTS V0: P_c52-{T}(V0)
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #108: input, references = 4, size of lhs = 0:
% 8.55/8.73 FALSE | EXISTS V0: P_c53-{T}(V0)
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #109: input, references = 4, size of lhs = 0:
% 8.55/8.73 FALSE | EXISTS V0: P_c57-{T}(V0)
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #110: input, references = 4, size of lhs = 0:
% 8.55/8.73 FALSE | EXISTS V0: P_c58-{T}(V0)
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 number of initial rules = 111
% 8.55/8.73
% 8.55/8.73 Simplifiers:
% 8.55/8.73 #111: unsound, references = 3, size of lhs = 2:
% 8.55/8.73 p9-{F}(V0,V1), V1 == V0 | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #112: unsound, references = 3, size of lhs = 2:
% 8.55/8.73 p45-{F}(V0,V1), V1 == V0 | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #113: unsound, references = 3, size of lhs = 2:
% 8.55/8.73 p35-{F}(V0,V1), V1 == V0 | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #114: unsound, references = 3, size of lhs = 2:
% 8.55/8.73 p25-{F}(V0,V1), V1 == V0 | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #115: unsound, references = 3, size of lhs = 2:
% 8.55/8.73 p2-{F}(V0,V1), V1 == V0 | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #116: unsound, references = 3, size of lhs = 2:
% 8.55/8.73 p17-{F}(V0,V1), V1 == V0 | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #117: unsound, references = 3, size of lhs = 3:
% 8.55/8.73 P_c54-{F}(V0), P_c54-{F}(V1), V0 == V1 | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #118: unsound, references = 3, size of lhs = 3:
% 8.55/8.73 P_c55-{F}(V0), P_c55-{F}(V1), V0 == V1 | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #119: unsound, references = 3, size of lhs = 3:
% 8.55/8.73 P_f20-{F}(V0,V1,V2), P_f20-{F}(V0,V1,V5), V2 == V5 | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #120: unsound, references = 3, size of lhs = 3:
% 8.55/8.73 P_f22-{F}(V0,V1,V2), P_f22-{F}(V0,V1,V5), V2 == V5 | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #121: unsound, references = 3, size of lhs = 3:
% 8.55/8.73 P_f24-{F}(V0,V1,V2), P_f24-{F}(V0,V1,V5), V2 == V5 | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #122: unsound, references = 3, size of lhs = 3:
% 8.55/8.73 P_f26-{F}(V0,V1,V2), P_f26-{F}(V0,V1,V5), V2 == V5 | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #123: unsound, references = 3, size of lhs = 3:
% 8.55/8.73 P_c56-{F}(V0), P_c56-{F}(V1), V0 == V1 | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #124: unsound, references = 3, size of lhs = 3:
% 8.55/8.73 P_f16-{F}(V0,V1,V2), P_f16-{F}(V0,V1,V5), V2 == V5 | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #125: unsound, references = 3, size of lhs = 3:
% 8.55/8.73 P_f10-{F}(V0,V1,V2), P_f10-{F}(V0,V1,V5), V2 == V5 | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #126: unsound, references = 3, size of lhs = 3:
% 8.55/8.73 P_f46-{F}(V0,V1,V2), P_f46-{F}(V0,V1,V5), V2 == V5 | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #127: unsound, references = 3, size of lhs = 3:
% 8.55/8.73 P_f44-{F}(V0,V1,V2), P_f44-{F}(V0,V1,V5), V2 == V5 | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #128: unsound, references = 3, size of lhs = 3:
% 8.55/8.73 P_f5-{F}(V0,V1,V2), P_f5-{F}(V0,V1,V5), V2 == V5 | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #129: unsound, references = 3, size of lhs = 3:
% 8.55/8.73 P_f42-{F}(V0,V1,V2), P_f42-{F}(V0,V1,V5), V2 == V5 | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #130: unsound, references = 3, size of lhs = 3:
% 8.55/8.73 P_f38-{F}(V0,V1,V2), P_f38-{F}(V0,V1,V5), V2 == V5 | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #131: unsound, references = 3, size of lhs = 3:
% 8.55/8.73 P_f36-{F}(V0,V1,V2), P_f36-{F}(V0,V1,V5), V2 == V5 | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #132: unsound, references = 3, size of lhs = 3:
% 8.55/8.73 P_f34-{F}(V0,V1,V2), P_f34-{F}(V0,V1,V5), V2 == V5 | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #133: unsound, references = 3, size of lhs = 3:
% 8.55/8.73 P_f8-{F}(V0,V1,V2), P_f8-{F}(V0,V1,V5), V2 == V5 | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #134: unsound, references = 3, size of lhs = 3:
% 8.55/8.73 P_f13-{F}(V0,V1,V2), P_f13-{F}(V0,V1,V5), V2 == V5 | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #135: unsound, references = 3, size of lhs = 3:
% 8.55/8.73 P_f32-{F}(V0,V1,V2), P_f32-{F}(V0,V1,V5), V2 == V5 | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #136: unsound, references = 3, size of lhs = 3:
% 8.55/8.73 P_f28-{F}(V0,V1,V2), P_f28-{F}(V0,V1,V5), V2 == V5 | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #137: unsound, references = 3, size of lhs = 3:
% 8.55/8.73 P_f30-{F}(V0,V1,V2), P_f30-{F}(V0,V1,V5), V2 == V5 | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #138: unsound, references = 3, size of lhs = 3:
% 8.55/8.73 P_f18-{F}(V0,V1,V2), P_f18-{F}(V0,V1,V5), V2 == V5 | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #139: unsound, references = 3, size of lhs = 3:
% 8.55/8.73 P_f40-{F}(V0,V1,V2), P_f40-{F}(V0,V1,V5), V2 == V5 | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #140: unsound, references = 3, size of lhs = 3:
% 8.55/8.73 P_c48-{F}(V0), P_c48-{F}(V1), V0 == V1 | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #141: unsound, references = 3, size of lhs = 3:
% 8.55/8.73 P_c50-{F}(V0), P_c50-{F}(V1), V0 == V1 | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #142: unsound, references = 3, size of lhs = 3:
% 8.55/8.73 P_c49-{F}(V0), P_c49-{F}(V1), V0 == V1 | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #143: unsound, references = 3, size of lhs = 3:
% 8.55/8.73 P_c51-{F}(V0), P_c51-{F}(V1), V0 == V1 | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #144: unsound, references = 3, size of lhs = 3:
% 8.55/8.73 P_c52-{F}(V0), P_c52-{F}(V1), V0 == V1 | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #145: unsound, references = 3, size of lhs = 3:
% 8.55/8.73 P_c53-{F}(V0), P_c53-{F}(V1), V0 == V1 | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #146: unsound, references = 3, size of lhs = 3:
% 8.55/8.73 P_c57-{F}(V0), P_c57-{F}(V1), V0 == V1 | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #147: unsound, references = 3, size of lhs = 3:
% 8.55/8.73 P_c58-{F}(V0), P_c58-{F}(V1), V0 == V1 | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 number of simplifiers = 37
% 8.55/8.73
% 8.55/8.73 Learnt:
% 8.55/8.73 #189: mergings( V73 == V71, V0 == V78, V3 == V15, V15 == V29, V29 == V32, V32 == V35, V35 == V38, V38 == V40, V40 == V43, V4 == V16, V16 == V30, V30 == V33, V33 == V36, V36 == V39, V39 == V41, V41 == V44, V5 == V17, V17 == V31, V31 == V34, V34 == V37, V37 == V42, V42 == V45, V6 == V18, V7 == V19, V8 == V20, V9 == V21, V10 == V22, V11 == V23, V12 == V24, V13 == V25, V14 == V26; #157 ), references = 2, size of lhs = 50:
% 8.55/8.73 P_c48-{F}(V0), p2-{F}(V0,V0), P_c50-{F}(V1), P_c49-{F}(V2), P_c51-{F}(V3), P_f18-{F}(V1,V3,V4), P_c52-{F}(V5), P_f16-{F}(V4,V5,V6), P_c53-{F}(V7), P_f13-{F}(V6,V7,V8), P_f10-{F}(V2,V8,V9), P_c57-{F}(V10), P_c58-{F}(V11), P_c54-{F}(V12), P_f8-{F}(V9,V12,V13), P_c55-{F}(V14), P_c56-{F}(V15), p7-{F}(V14,V16), p9-{F}(V17,V17), P_f18-{F}(V1,V18,V19), P_f26-{F}(V15,V18,V20), P_f36-{F}(V10,V18,V21), P_f46-{F}(V11,V18,V22), P_f16-{F}(V19,V23,V24), P_f24-{F}(V20,V23,V25), P_f34-{F}(V21,V23,V26), P_f44-{F}(V22,V23,V27), P_f13-{F}(V24,V28,V29), P_f10-{F}(V2,V29,V30), P_f22-{F}(V25,V28,V31), P_f32-{F}(V26,V28,V32), P_f42-{F}(V27,V28,V33), P_f8-{F}(V30,V34,V35), P_f20-{F}(V31,V34,V36), P_f18-{F}(V1,V36,V37), P_f30-{F}(V32,V34,V38), P_f16-{F}(V37,V38,V39), P_f40-{F}(V33,V34,V40), P_f13-{F}(V39,V40,V41), P_f10-{F}(V17,V35,V42), P_f10-{F}(V17,V41,V43), P_f8-{F}(V43,V44,V13), p7-{F}(V45,V44), P_f8-{F}(V42,V45,V46), P_f5-{F}(V0,V46,V47), p4-{F}(V47,V48), P_f20-{F}(V49,V16,V48), P_f26-{F}(V15,V50,V51), P_f24-{F}(V51,V52,V53), P_f22-{F}(V53,V54,V49) | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #220: mergings( V71 == V69, V15 == V44, V1 == V26, V26 == V29, V29 == V32, V32 == V35, V35 == V37, V37 == V40, V3 == V13, V13 == V27, V27 == V30, V30 == V33, V33 == V36, V36 == V38, V38 == V41, V4 == V14, V14 == V28, V28 == V31, V31 == V34, V34 == V39, V39 == V42, V5 == V16, V6 == V17, V7 == V18, V8 == V19, V9 == V20, V10 == V21, V11 == V22, V12 == V23; #190 ), references = 2, size of lhs = 48:
% 8.55/8.73 P_c48-{F}(V0), p2-{F}(V0,V0), P_c50-{F}(V1), P_c49-{F}(V2), P_c51-{F}(V3), P_f18-{F}(V1,V3,V4), P_c52-{F}(V5), P_f16-{F}(V4,V5,V6), P_c53-{F}(V7), P_f13-{F}(V6,V7,V8), P_f10-{F}(V2,V8,V9), P_c57-{F}(V10), P_c58-{F}(V11), P_c54-{F}(V12), P_c55-{F}(V13), P_c56-{F}(V14), p7-{F}(V13,V15), p7-{F}(V16,V12), p9-{F}(V17,V17), P_f10-{F}(V17,V18,V9), P_f18-{F}(V1,V19,V20), P_f26-{F}(V14,V19,V21), P_f36-{F}(V10,V19,V22), P_f46-{F}(V11,V19,V23), P_f16-{F}(V20,V24,V25), P_f24-{F}(V21,V24,V26), P_f34-{F}(V22,V24,V27), P_f44-{F}(V23,V24,V28), P_f13-{F}(V25,V29,V30), P_f10-{F}(V2,V30,V31), P_f22-{F}(V26,V29,V32), P_f32-{F}(V27,V29,V33), P_f42-{F}(V28,V29,V34), P_f8-{F}(V31,V35,V36), P_f20-{F}(V32,V35,V37), P_f18-{F}(V1,V37,V38), P_f30-{F}(V33,V35,V39), P_f16-{F}(V38,V39,V40), P_f40-{F}(V34,V35,V41), P_f13-{F}(V40,V41,V18), P_f10-{F}(V17,V36,V42), P_f8-{F}(V42,V16,V43), P_f5-{F}(V0,V43,V44), p4-{F}(V44,V45), P_f20-{F}(V46,V15,V45), P_f26-{F}(V14,V47,V48), P_f24-{F}(V48,V49,V50), P_f22-{F}(V50,V51,V46) | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #249: mergings( V0 == V66, V14 == V41, V11 == V23, V23 == V26, V26 == V29, V29 == V32, V32 == V34, V34 == V37, V3 == V12, V12 == V24, V24 == V27, V27 == V30, V30 == V33, V33 == V35, V35 == V38, V4 == V13, V13 == V25, V25 == V28, V28 == V31, V31 == V36, V36 == V39, V5 == V15, V6 == V16, V7 == V17, V8 == V18, V9 == V19, V10 == V20; #221 ), references = 1, size of lhs = 46:
% 8.55/8.73 P_c48-{F}(V0), p2-{F}(V0,V0), P_c50-{F}(V1), P_c49-{F}(V2), p9-{F}(V2,V2), P_c51-{F}(V3), P_f18-{F}(V1,V3,V4), P_c52-{F}(V5), P_f16-{F}(V4,V5,V6), P_c53-{F}(V7), P_f13-{F}(V6,V7,V8), P_c57-{F}(V9), P_c58-{F}(V10), P_c54-{F}(V11), P_c55-{F}(V12), P_c56-{F}(V13), p7-{F}(V12,V14), p7-{F}(V15,V11), P_f18-{F}(V1,V16,V17), P_f26-{F}(V13,V16,V18), P_f36-{F}(V9,V16,V19), P_f46-{F}(V10,V16,V20), P_f16-{F}(V17,V21,V22), P_f24-{F}(V18,V21,V23), P_f34-{F}(V19,V21,V24), P_f44-{F}(V20,V21,V25), P_f13-{F}(V22,V26,V27), P_f10-{F}(V2,V27,V28), P_f22-{F}(V23,V26,V29), P_f32-{F}(V24,V26,V30), P_f42-{F}(V25,V26,V31), P_f8-{F}(V28,V32,V33), P_f20-{F}(V29,V32,V34), P_f18-{F}(V1,V34,V35), P_f30-{F}(V30,V32,V36), P_f16-{F}(V35,V36,V37), P_f40-{F}(V31,V32,V38), P_f13-{F}(V37,V38,V8), P_f10-{F}(V2,V33,V39), P_f8-{F}(V39,V15,V40), P_f5-{F}(V0,V40,V41), p4-{F}(V41,V42), P_f20-{F}(V43,V14,V42), P_f26-{F}(V13,V44,V45), P_f24-{F}(V45,V46,V47), P_f22-{F}(V47,V48,V43) | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #274: mergings( V61 == V0, V3 == V17, V17 == V31, V4 == V18, V18 == V32, V5 == V19, V19 == V33, V6 == V20, V7 == V21, V8 == V22, V9 == V23, V10 == V24, V11 == V25, V12 == V26, V13 == V27, V14 == V28, V15 == V29, V16 == V30; #254 ), references = 1, size of lhs = 68:
% 8.55/8.73 P_c48-{F}(V0), p2-{F}(V0,V0), P_c50-{F}(V1), P_c49-{F}(V2), P_c51-{F}(V3), P_f18-{F}(V1,V3,V4), P_c52-{F}(V5), P_f16-{F}(V4,V5,V6), P_c53-{F}(V7), P_f13-{F}(V6,V7,V8), P_f10-{F}(V2,V8,V9), P_c57-{F}(V10), P_c58-{F}(V11), P_c54-{F}(V12), P_f8-{F}(V9,V12,V13), P_c55-{F}(V14), P_c56-{F}(V15), p7-{F}(V14,V16), p7-{F}(V17,V12), p9-{F}(V18,V18), P_f10-{F}(V18,V19,V9), P_f8-{F}(V20,V17,V13), P_f10-{F}(V18,V21,V20), P_f18-{F}(V1,V22,V23), P_f26-{F}(V15,V22,V24), P_f36-{F}(V10,V22,V25), P_f46-{F}(V11,V22,V26), P_f16-{F}(V23,V27,V28), P_f24-{F}(V24,V27,V29), P_f34-{F}(V25,V27,V30), P_f44-{F}(V26,V27,V31), P_f13-{F}(V28,V32,V33), P_f10-{F}(V2,V33,V34), P_f22-{F}(V29,V32,V35), P_f32-{F}(V30,V32,V36), P_f42-{F}(V31,V32,V37), P_f8-{F}(V34,V38,V13), P_f20-{F}(V35,V38,V39), P_f18-{F}(V1,V39,V40), P_f30-{F}(V36,V38,V41), P_f16-{F}(V40,V41,V42), P_f40-{F}(V37,V38,V43), P_f13-{F}(V42,V43,V44), P_f5-{F}(V0,V44,V45), P_f20-{F}(V46,V16,V45), P_f18-{F}(V1,V47,V48), P_f26-{F}(V15,V47,V49), P_f36-{F}(V10,V47,V50), P_f46-{F}(V11,V47,V51), P_f16-{F}(V48,V52,V53), P_f24-{F}(V49,V52,V54), P_f34-{F}(V50,V52,V55), P_f44-{F}(V51,V52,V56), P_f13-{F}(V53,V57,V58), P_f10-{F}(V2,V58,V59), P_f22-{F}(V54,V57,V60), P_f32-{F}(V55,V57,V61), P_f42-{F}(V56,V57,V62), P_f8-{F}(V59,V63,V21), P_f20-{F}(V60,V63,V64), P_f18-{F}(V1,V64,V65), P_f30-{F}(V61,V63,V66), P_f16-{F}(V65,V66,V67), P_f40-{F}(V62,V63,V68), P_f13-{F}(V67,V68,V19), P_f26-{F}(V15,V69,V70), P_f24-{F}(V70,V71,V72), P_f22-{F}(V72,V73,V46) | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #294: mergings( V60 == V0, V3 == V17, V17 == V31, V4 == V18, V18 == V33, V5 == V19, V19 == V34, V6 == V20, V7 == V21, V8 == V22, V9 == V23, V10 == V24, V11 == V25, V12 == V26, V13 == V27, V14 == V28, V1 == V32, V15 == V29, V16 == V30; #255 ), references = 1, size of lhs = 69:
% 8.55/8.73 P_c48-{F}(V0), p2-{F}(V0,V0), P_c50-{F}(V1), P_c49-{F}(V2), P_c51-{F}(V3), P_f18-{F}(V1,V3,V4), P_c52-{F}(V5), P_f16-{F}(V4,V5,V6), P_c53-{F}(V7), P_f13-{F}(V6,V7,V8), P_f10-{F}(V2,V8,V9), P_c57-{F}(V10), P_c58-{F}(V11), P_c54-{F}(V12), P_f8-{F}(V9,V12,V13), P_c55-{F}(V14), P_c56-{F}(V15), p7-{F}(V14,V16), p9-{F}(V17,V17), P_f18-{F}(V1,V18,V19), P_f26-{F}(V15,V18,V20), P_f36-{F}(V10,V18,V21), P_f46-{F}(V11,V18,V22), P_f16-{F}(V19,V23,V24), P_f24-{F}(V20,V23,V25), P_f34-{F}(V21,V23,V26), P_f44-{F}(V22,V23,V27), P_f13-{F}(V24,V28,V29), P_f10-{F}(V2,V29,V30), P_f22-{F}(V25,V28,V31), P_f32-{F}(V26,V28,V32), P_f42-{F}(V27,V28,V33), P_f8-{F}(V30,V34,V13), P_f20-{F}(V31,V34,V35), P_f18-{F}(V1,V35,V36), P_f30-{F}(V32,V34,V37), P_f16-{F}(V36,V37,V38), P_f40-{F}(V33,V34,V39), P_f13-{F}(V38,V39,V40), P_f5-{F}(V0,V40,V41), P_f20-{F}(V42,V16,V41), P_f18-{F}(V1,V43,V44), P_f26-{F}(V15,V43,V45), P_f36-{F}(V10,V43,V46), P_f46-{F}(V11,V43,V47), P_f16-{F}(V44,V48,V49), P_f24-{F}(V45,V48,V50), P_f34-{F}(V46,V48,V51), P_f44-{F}(V47,V48,V52), P_f13-{F}(V49,V53,V54), P_f10-{F}(V2,V54,V55), P_f22-{F}(V50,V53,V56), P_f32-{F}(V51,V53,V57), P_f42-{F}(V52,V53,V58), P_f8-{F}(V55,V59,V60), P_f20-{F}(V56,V59,V61), P_f18-{F}(V1,V61,V62), P_f30-{F}(V57,V59,V63), P_f16-{F}(V62,V63,V64), P_f40-{F}(V58,V59,V65), P_f13-{F}(V64,V65,V66), P_f10-{F}(V17,V60,V67), P_f10-{F}(V17,V66,V68), P_f8-{F}(V67,V69,V13), p7-{F}(V69,V70), P_f8-{F}(V68,V70,V13), P_f26-{F}(V15,V71,V72), P_f24-{F}(V72,V73,V74), P_f22-{F}(V74,V75,V42) | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #323: mergings( V62 == V0, V3 == V15, V15 == V29, V29 == V32, V32 == V35, V4 == V16, V16 == V30, V30 == V33, V33 == V36, V5 == V17, V17 == V31, V31 == V34, V34 == V37, V6 == V18, V7 == V19, V8 == V20, V9 == V21, V10 == V22, V11 == V23, V12 == V24, V13 == V25, V14 == V26; #300 ), references = 1, size of lhs = 43:
% 8.55/8.73 P_c48-{F}(V0), p2-{F}(V0,V0), P_c50-{F}(V1), P_c49-{F}(V2), P_c51-{F}(V3), P_f18-{F}(V1,V3,V4), P_c52-{F}(V5), P_f16-{F}(V4,V5,V6), P_c53-{F}(V7), P_f13-{F}(V6,V7,V8), P_f10-{F}(V2,V8,V9), P_c57-{F}(V10), P_c58-{F}(V11), P_c54-{F}(V12), P_f8-{F}(V9,V12,V13), P_c55-{F}(V14), P_c56-{F}(V15), p7-{F}(V14,V16), P_f18-{F}(V1,V17,V18), P_f26-{F}(V15,V17,V19), P_f36-{F}(V10,V17,V20), P_f46-{F}(V11,V17,V21), P_f16-{F}(V18,V22,V23), P_f24-{F}(V19,V22,V24), P_f34-{F}(V20,V22,V25), P_f44-{F}(V21,V22,V26), P_f13-{F}(V23,V27,V28), P_f10-{F}(V2,V28,V29), P_f22-{F}(V24,V27,V30), P_f32-{F}(V25,V27,V31), P_f42-{F}(V26,V27,V32), P_f8-{F}(V29,V33,V13), P_f20-{F}(V30,V33,V34), P_f18-{F}(V1,V34,V35), P_f30-{F}(V31,V33,V36), P_f16-{F}(V35,V36,V37), P_f40-{F}(V32,V33,V38), P_f13-{F}(V37,V38,V39), P_f5-{F}(V0,V39,V40), P_f20-{F}(V41,V16,V40), P_f26-{F}(V15,V42,V43), P_f24-{F}(V43,V44,V45), P_f22-{F}(V45,V46,V41) | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #345: mergings( V36 == V15, V1 == V26, V26 == V29, V29 == V32, V3 == V13, V13 == V27, V27 == V30, V30 == V33, V4 == V14, V14 == V28, V28 == V31, V31 == V34, V5 == V16, V6 == V17, V7 == V18, V8 == V19, V9 == V20, V10 == V21, V11 == V22, V12 == V23; #324 ), references = 1, size of lhs = 41:
% 8.55/8.73 P_c48-{F}(V0), p2-{F}(V0,V0), P_c50-{F}(V1), P_c49-{F}(V2), P_c51-{F}(V3), P_f18-{F}(V1,V3,V4), P_c52-{F}(V5), P_f16-{F}(V4,V5,V6), P_c53-{F}(V7), P_f13-{F}(V6,V7,V8), P_f10-{F}(V2,V8,V9), P_c57-{F}(V10), P_c58-{F}(V11), P_c54-{F}(V12), P_c55-{F}(V13), P_c56-{F}(V14), p7-{F}(V13,V15), P_f10-{F}(V2,V16,V9), P_f18-{F}(V1,V17,V18), P_f26-{F}(V14,V17,V19), P_f36-{F}(V10,V17,V20), P_f46-{F}(V11,V17,V21), P_f16-{F}(V18,V22,V23), P_f24-{F}(V19,V22,V24), P_f34-{F}(V20,V22,V25), P_f44-{F}(V21,V22,V26), P_f13-{F}(V23,V27,V16), P_f22-{F}(V24,V27,V28), P_f32-{F}(V25,V27,V29), P_f42-{F}(V26,V27,V30), P_f20-{F}(V28,V12,V31), P_f18-{F}(V1,V31,V32), P_f30-{F}(V29,V12,V33), P_f16-{F}(V32,V33,V34), P_f40-{F}(V30,V12,V35), P_f13-{F}(V34,V35,V36), P_f5-{F}(V0,V36,V37), P_f20-{F}(V38,V15,V37), P_f26-{F}(V14,V39,V40), P_f24-{F}(V40,V41,V42), P_f22-{F}(V42,V43,V38) | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #381: mergings( V67 == V0, V3 == V15, V15 == V29, V29 == V32, V32 == V35, V35 == V40, V4 == V16, V16 == V30, V30 == V33, V33 == V36, V36 == V41, V5 == V17, V17 == V31, V31 == V34, V34 == V37, V37 == V42, V0 == V38, V6 == V18, V18 == V39, V7 == V19, V8 == V20, V9 == V21, V10 == V22, V11 == V23, V12 == V24, V13 == V25, V14 == V26; #353 ), references = 1, size of lhs = 47:
% 8.55/8.73 P_c49-{F}(V0), P_c51-{F}(V1), P_c52-{F}(V2), P_c53-{F}(V3), P_c57-{F}(V4), P_c58-{F}(V5), P_c48-{F}(V6), p2-{F}(V6,V6), P_c50-{F}(V7), P_f18-{F}(V7,V1,V8), P_f16-{F}(V8,V2,V9), P_f13-{F}(V9,V3,V10), P_f10-{F}(V0,V10,V11), P_c54-{F}(V12), P_f8-{F}(V11,V12,V13), P_c55-{F}(V14), P_c56-{F}(V15), p7-{F}(V14,V16), P_f18-{F}(V7,V17,V18), P_f26-{F}(V15,V17,V19), P_f36-{F}(V4,V17,V20), P_f46-{F}(V5,V17,V21), P_f16-{F}(V18,V22,V23), P_f24-{F}(V19,V22,V24), P_f34-{F}(V20,V22,V25), P_f44-{F}(V21,V22,V26), P_f13-{F}(V23,V27,V28), P_f10-{F}(V0,V28,V29), P_f22-{F}(V24,V27,V30), P_f32-{F}(V25,V27,V31), P_f42-{F}(V26,V27,V32), P_f8-{F}(V29,V33,V13), P_f20-{F}(V30,V33,V34), P_f18-{F}(V7,V34,V35), P_f30-{F}(V31,V33,V36), P_f16-{F}(V35,V36,V37), P_f40-{F}(V32,V33,V38), P_f13-{F}(V37,V38,V39), P_f5-{F}(V6,V39,V40), P_f5-{F}(V6,V41,V40), P_f26-{F}(V15,V42,V43), P_f24-{F}(V43,V44,V45), P_f22-{F}(V45,V46,V47), P_f20-{F}(V47,V16,V48), P_f18-{F}(V7,V48,V49), P_f16-{F}(V49,V50,V51), P_f13-{F}(V51,V52,V41) | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #408: mergings( V41 == V15, V1 == V26, V26 == V29, V29 == V32, V32 == V37, V3 == V13, V13 == V27, V27 == V30, V30 == V33, V33 == V38, V4 == V14, V14 == V28, V28 == V31, V31 == V34, V34 == V39, V15 == V35, V5 == V16, V16 == V36, V6 == V17, V7 == V18, V8 == V19, V9 == V20, V10 == V21, V11 == V22, V12 == V23; #382 ), references = 1, size of lhs = 45:
% 8.55/8.73 P_c49-{F}(V0), P_c51-{F}(V1), P_c52-{F}(V2), P_c53-{F}(V3), P_c57-{F}(V4), P_c58-{F}(V5), P_c48-{F}(V6), p2-{F}(V6,V6), P_c50-{F}(V7), P_f18-{F}(V7,V1,V8), P_f16-{F}(V8,V2,V9), P_f13-{F}(V9,V3,V10), P_f10-{F}(V0,V10,V11), P_c54-{F}(V12), P_c55-{F}(V13), P_c56-{F}(V14), p7-{F}(V13,V15), P_f10-{F}(V0,V16,V11), P_f18-{F}(V7,V17,V18), P_f26-{F}(V14,V17,V19), P_f36-{F}(V4,V17,V20), P_f46-{F}(V5,V17,V21), P_f16-{F}(V18,V22,V23), P_f24-{F}(V19,V22,V24), P_f34-{F}(V20,V22,V25), P_f44-{F}(V21,V22,V26), P_f13-{F}(V23,V27,V16), P_f22-{F}(V24,V27,V28), P_f32-{F}(V25,V27,V29), P_f42-{F}(V26,V27,V30), P_f20-{F}(V28,V12,V31), P_f18-{F}(V7,V31,V32), P_f30-{F}(V29,V12,V33), P_f16-{F}(V32,V33,V34), P_f40-{F}(V30,V12,V35), P_f13-{F}(V34,V35,V36), P_f5-{F}(V6,V36,V37), P_f5-{F}(V6,V38,V37), P_f26-{F}(V14,V39,V40), P_f24-{F}(V40,V41,V42), P_f22-{F}(V42,V43,V44), P_f20-{F}(V44,V15,V45), P_f18-{F}(V7,V45,V46), P_f16-{F}(V46,V47,V48), P_f13-{F}(V48,V49,V38) | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #434: mergings( V0 == V17, V14 == V28, V28 == V31, V31 == V34, V34 == V38, V3 == V15, V15 == V29, V29 == V32, V32 == V35, V35 == V39, V4 == V16, V16 == V30, V30 == V33, V33 == V36, V36 == V40, V5 == V18, V18 == V37, V6 == V19, V7 == V20, V8 == V21, V9 == V22, V10 == V23, V11 == V24, V12 == V25; #409 ), references = 1, size of lhs = 43:
% 8.55/8.73 P_c49-{F}(V0), P_c51-{F}(V1), P_c52-{F}(V2), P_c53-{F}(V3), P_c57-{F}(V4), P_c58-{F}(V5), P_c48-{F}(V6), p2-{F}(V6,V6), P_c50-{F}(V7), P_f18-{F}(V7,V1,V8), P_f16-{F}(V8,V2,V9), P_f13-{F}(V9,V3,V10), P_f10-{F}(V0,V10,V11), P_c54-{F}(V12), P_c55-{F}(V13), P_c56-{F}(V14), p7-{F}(V13,V15), P_f10-{F}(V0,V16,V11), P_f18-{F}(V7,V17,V18), P_f26-{F}(V14,V17,V19), P_f36-{F}(V4,V17,V20), P_f46-{F}(V5,V17,V21), P_f16-{F}(V18,V22,V23), P_f24-{F}(V19,V22,V24), P_f34-{F}(V20,V22,V25), P_f44-{F}(V21,V22,V26), P_f13-{F}(V23,V27,V16), P_f22-{F}(V24,V27,V28), P_f32-{F}(V25,V27,V29), P_f42-{F}(V26,V27,V30), P_f20-{F}(V28,V12,V31), P_f18-{F}(V7,V31,V32), P_f30-{F}(V29,V12,V33), P_f16-{F}(V32,V33,V34), P_f40-{F}(V30,V12,V35), P_f13-{F}(V34,V35,V36), P_f26-{F}(V14,V37,V38), P_f24-{F}(V38,V39,V40), P_f22-{F}(V40,V41,V42), P_f20-{F}(V42,V15,V43), P_f18-{F}(V7,V43,V44), P_f16-{F}(V44,V45,V46), P_f13-{F}(V46,V47,V36) | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #458: mergings( V32 == V14, V11 == V23, V23 == V26, V26 == V29, V29 == V34, V3 == V12, V12 == V24, V24 == V27, V27 == V30, V30 == V35, V4 == V13, V13 == V25, V25 == V28, V28 == V31, V31 == V36, V5 == V15, V15 == V33, V6 == V16, V7 == V17, V8 == V18, V9 == V19, V10 == V20; #435 ), references = 2, size of lhs = 41:
% 8.55/8.73 P_c49-{F}(V0), P_c51-{F}(V1), P_c52-{F}(V2), P_c53-{F}(V3), P_c57-{F}(V4), P_c58-{F}(V5), P_c48-{F}(V6), p2-{F}(V6,V6), P_c50-{F}(V7), P_f18-{F}(V7,V1,V8), P_f16-{F}(V8,V2,V9), P_f13-{F}(V9,V3,V10), P_c54-{F}(V11), P_c55-{F}(V12), P_c56-{F}(V13), p7-{F}(V12,V14), P_f18-{F}(V7,V15,V16), P_f26-{F}(V13,V15,V17), P_f36-{F}(V4,V15,V18), P_f46-{F}(V5,V15,V19), P_f16-{F}(V16,V20,V21), P_f24-{F}(V17,V20,V22), P_f34-{F}(V18,V20,V23), P_f44-{F}(V19,V20,V24), P_f13-{F}(V21,V25,V10), P_f22-{F}(V22,V25,V26), P_f32-{F}(V23,V25,V27), P_f42-{F}(V24,V25,V28), P_f20-{F}(V26,V11,V29), P_f18-{F}(V7,V29,V30), P_f30-{F}(V27,V11,V31), P_f16-{F}(V30,V31,V32), P_f40-{F}(V28,V11,V33), P_f13-{F}(V32,V33,V34), P_f26-{F}(V13,V35,V36), P_f24-{F}(V36,V37,V38), P_f22-{F}(V38,V39,V40), P_f20-{F}(V40,V14,V41), P_f18-{F}(V7,V41,V42), P_f16-{F}(V42,V43,V44), P_f13-{F}(V44,V45,V34) | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #461: exists( #97, #458 ), references = 1, size of lhs = 39:
% 8.55/8.73 P_c49-{F}(V0), P_c51-{F}(V1), P_c52-{F}(V2), P_c53-{F}(V3), P_c57-{F}(V4), P_c58-{F}(V5), P_c48-{F}(V6), p2-{F}(V6,V6), P_c50-{F}(V7), P_f18-{F}(V7,V1,V8), P_f16-{F}(V8,V2,V9), P_f13-{F}(V9,V3,V10), P_c54-{F}(V11), P_c55-{F}(V12), P_c56-{F}(V13), p7-{F}(V12,V14), P_f18-{F}(V7,V15,V16), P_f26-{F}(V13,V15,V17), P_f36-{F}(V4,V15,V18), P_f46-{F}(V5,V15,V19), P_f16-{F}(V16,V20,V21), P_f24-{F}(V17,V20,V22), P_f34-{F}(V18,V20,V23), P_f44-{F}(V19,V20,V24), P_f13-{F}(V21,V25,V10), P_f22-{F}(V22,V25,V26), P_f32-{F}(V23,V25,V27), P_f42-{F}(V24,V25,V28), P_f20-{F}(V26,V11,V29), P_f18-{F}(V7,V29,V30), P_f30-{F}(V27,V11,V31), P_f16-{F}(V30,V31,V32), P_f40-{F}(V28,V11,V33), P_f26-{F}(V13,V34,V35), P_f24-{F}(V35,V36,V37), P_f22-{F}(V37,V38,V39), P_f20-{F}(V39,V14,V40), P_f18-{F}(V7,V40,V41), P_f16-{F}(V41,V42,V32) | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #463: exists( #87, #459 ), references = 1, size of lhs = 39:
% 8.55/8.73 P_c49-{F}(V0), P_c51-{F}(V1), P_c52-{F}(V2), P_c53-{F}(V3), P_c57-{F}(V4), P_c58-{F}(V5), P_c48-{F}(V6), p2-{F}(V6,V6), P_c50-{F}(V7), P_f18-{F}(V7,V1,V8), P_f16-{F}(V8,V2,V9), P_f13-{F}(V9,V3,V10), P_c54-{F}(V11), P_c55-{F}(V12), P_c56-{F}(V13), p7-{F}(V12,V14), P_f18-{F}(V7,V15,V16), P_f26-{F}(V13,V15,V17), P_f36-{F}(V4,V15,V18), P_f46-{F}(V5,V15,V19), P_f16-{F}(V16,V20,V21), P_f24-{F}(V17,V20,V22), P_f34-{F}(V18,V20,V23), P_f44-{F}(V19,V20,V24), P_f13-{F}(V21,V25,V10), P_f22-{F}(V22,V25,V26), P_f32-{F}(V23,V25,V27), P_f42-{F}(V24,V25,V28), P_f20-{F}(V26,V11,V29), P_f18-{F}(V7,V29,V30), P_f30-{F}(V27,V11,V31), P_f16-{F}(V30,V31,V32), P_f40-{F}(V28,V11,V33), P_f26-{F}(V13,V34,V35), P_f24-{F}(V35,V36,V37), P_f22-{F}(V37,V38,V39), P_f20-{F}(V39,V14,V40), P_f18-{F}(V7,V40,V41), P_f16-{F}(V41,V42,V32) | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #465: exists( #102, #462 ), references = 2, size of lhs = 38:
% 8.55/8.73 P_c49-{F}(V0), P_c51-{F}(V1), P_c52-{F}(V2), P_c53-{F}(V3), P_c57-{F}(V4), P_c58-{F}(V5), P_c48-{F}(V6), p2-{F}(V6,V6), P_c50-{F}(V7), P_f18-{F}(V7,V1,V8), P_f16-{F}(V8,V2,V9), P_f13-{F}(V9,V3,V10), P_c54-{F}(V11), P_c55-{F}(V12), P_c56-{F}(V13), p7-{F}(V12,V14), P_f18-{F}(V7,V15,V16), P_f26-{F}(V13,V15,V17), P_f36-{F}(V4,V15,V18), P_f46-{F}(V5,V15,V19), P_f16-{F}(V16,V20,V21), P_f24-{F}(V17,V20,V22), P_f34-{F}(V18,V20,V23), P_f44-{F}(V19,V20,V24), P_f13-{F}(V21,V25,V10), P_f22-{F}(V22,V25,V26), P_f32-{F}(V23,V25,V27), P_f42-{F}(V24,V25,V28), P_f20-{F}(V26,V11,V29), P_f18-{F}(V7,V29,V30), P_f30-{F}(V27,V11,V31), P_f16-{F}(V30,V31,V32), P_f26-{F}(V13,V33,V34), P_f24-{F}(V34,V35,V36), P_f22-{F}(V36,V37,V38), P_f20-{F}(V38,V14,V39), P_f18-{F}(V7,V39,V40), P_f16-{F}(V40,V41,V32) | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #470: exists( #87, #465 ), references = 1, size of lhs = 36:
% 8.55/8.73 P_c49-{F}(V0), P_c51-{F}(V1), P_c52-{F}(V2), P_c53-{F}(V3), P_c57-{F}(V4), P_c58-{F}(V5), P_c48-{F}(V6), p2-{F}(V6,V6), P_c50-{F}(V7), P_f18-{F}(V7,V1,V8), P_f16-{F}(V8,V2,V9), P_f13-{F}(V9,V3,V10), P_c54-{F}(V11), P_c55-{F}(V12), P_c56-{F}(V13), p7-{F}(V12,V14), P_f18-{F}(V7,V15,V16), P_f26-{F}(V13,V15,V17), P_f36-{F}(V4,V15,V18), P_f46-{F}(V5,V15,V19), P_f16-{F}(V16,V20,V21), P_f24-{F}(V17,V20,V22), P_f34-{F}(V18,V20,V23), P_f44-{F}(V19,V20,V24), P_f13-{F}(V21,V25,V10), P_f22-{F}(V22,V25,V26), P_f32-{F}(V23,V25,V27), P_f42-{F}(V24,V25,V28), P_f20-{F}(V26,V11,V29), P_f18-{F}(V7,V29,V30), P_f30-{F}(V27,V11,V31), P_f18-{F}(V7,V32,V30), P_f20-{F}(V33,V14,V32), P_f26-{F}(V13,V34,V35), P_f24-{F}(V35,V36,V37), P_f22-{F}(V37,V38,V33) | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #472: exists( #101, #467 ), references = 2, size of lhs = 34:
% 8.55/8.73 P_c49-{F}(V0), P_c51-{F}(V1), P_c52-{F}(V2), P_c53-{F}(V3), P_c57-{F}(V4), P_c58-{F}(V5), P_c48-{F}(V6), p2-{F}(V6,V6), P_c50-{F}(V7), P_f18-{F}(V7,V1,V8), P_f16-{F}(V8,V2,V9), P_f13-{F}(V9,V3,V10), P_c54-{F}(V11), P_c55-{F}(V12), P_c56-{F}(V13), p7-{F}(V12,V14), P_f18-{F}(V7,V15,V16), P_f26-{F}(V13,V15,V17), P_f36-{F}(V4,V15,V18), P_f46-{F}(V5,V15,V19), P_f16-{F}(V16,V20,V21), P_f24-{F}(V17,V20,V22), P_f34-{F}(V18,V20,V23), P_f44-{F}(V19,V20,V24), P_f13-{F}(V21,V25,V10), P_f22-{F}(V22,V25,V26), P_f32-{F}(V23,V25,V27), P_f42-{F}(V24,V25,V28), P_f20-{F}(V26,V11,V29), P_f30-{F}(V27,V11,V30), P_f20-{F}(V31,V14,V29), P_f26-{F}(V13,V32,V33), P_f24-{F}(V33,V34,V35), P_f22-{F}(V35,V36,V31) | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #476: exists( #100, #472 ), references = 1, size of lhs = 33:
% 8.55/8.73 P_c49-{F}(V0), P_c51-{F}(V1), P_c52-{F}(V2), P_c53-{F}(V3), P_c57-{F}(V4), P_c58-{F}(V5), P_c48-{F}(V6), p2-{F}(V6,V6), P_c50-{F}(V7), P_f18-{F}(V7,V1,V8), P_f16-{F}(V8,V2,V9), P_f13-{F}(V9,V3,V10), P_c54-{F}(V11), P_c55-{F}(V12), P_c56-{F}(V13), p7-{F}(V12,V14), P_f18-{F}(V7,V15,V16), P_f26-{F}(V13,V15,V17), P_f36-{F}(V4,V15,V18), P_f46-{F}(V5,V15,V19), P_f16-{F}(V16,V20,V21), P_f24-{F}(V17,V20,V22), P_f34-{F}(V18,V20,V23), P_f44-{F}(V19,V20,V24), P_f13-{F}(V21,V25,V10), P_f22-{F}(V22,V25,V26), P_f32-{F}(V23,V25,V27), P_f42-{F}(V24,V25,V28), P_f20-{F}(V26,V11,V29), P_f20-{F}(V30,V14,V29), P_f26-{F}(V13,V31,V32), P_f24-{F}(V32,V33,V34), P_f22-{F}(V34,V35,V30) | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #478: exists( #98, #474 ), references = 1, size of lhs = 32:
% 8.55/8.73 P_c49-{F}(V0), P_c51-{F}(V1), P_c52-{F}(V2), P_c53-{F}(V3), P_c57-{F}(V4), P_c58-{F}(V5), P_c48-{F}(V6), p2-{F}(V6,V6), P_c50-{F}(V7), P_f18-{F}(V7,V1,V8), P_f16-{F}(V8,V2,V9), P_f13-{F}(V9,V3,V10), P_c54-{F}(V11), P_c55-{F}(V12), P_c56-{F}(V13), p7-{F}(V12,V14), P_f18-{F}(V7,V15,V16), P_f26-{F}(V13,V15,V17), P_f36-{F}(V4,V15,V18), P_f46-{F}(V5,V15,V19), P_f16-{F}(V16,V20,V21), P_f24-{F}(V17,V20,V22), P_f34-{F}(V18,V20,V23), P_f44-{F}(V19,V20,V24), P_f13-{F}(V21,V25,V10), P_f22-{F}(V22,V25,V26), P_f42-{F}(V24,V25,V27), P_f20-{F}(V26,V11,V28), P_f20-{F}(V29,V14,V28), P_f26-{F}(V13,V30,V31), P_f24-{F}(V31,V32,V33), P_f22-{F}(V33,V34,V29) | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #480: exists( #97, #477 ), references = 1, size of lhs = 30:
% 8.55/8.73 P_c49-{F}(V0), P_c51-{F}(V1), P_c52-{F}(V2), P_c53-{F}(V3), P_c57-{F}(V4), P_c58-{F}(V5), P_c48-{F}(V6), p2-{F}(V6,V6), P_c50-{F}(V7), P_f18-{F}(V7,V1,V8), P_f16-{F}(V8,V2,V9), P_c54-{F}(V10), P_c55-{F}(V11), P_c56-{F}(V12), p7-{F}(V11,V13), P_f18-{F}(V7,V14,V15), P_f26-{F}(V12,V14,V16), P_f36-{F}(V4,V14,V17), P_f46-{F}(V5,V14,V18), P_f16-{F}(V15,V19,V9), P_f24-{F}(V16,V19,V20), P_f34-{F}(V17,V19,V21), P_f44-{F}(V18,V19,V22), P_f22-{F}(V20,V3,V23), P_f42-{F}(V22,V3,V24), P_f20-{F}(V23,V10,V25), P_f20-{F}(V26,V13,V25), P_f26-{F}(V12,V27,V28), P_f24-{F}(V28,V29,V30), P_f22-{F}(V30,V31,V26) | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #482: exists( #95, #479 ), references = 1, size of lhs = 29:
% 8.55/8.73 P_c49-{F}(V0), P_c51-{F}(V1), P_c52-{F}(V2), P_c53-{F}(V3), P_c57-{F}(V4), P_c58-{F}(V5), P_c48-{F}(V6), p2-{F}(V6,V6), P_c50-{F}(V7), P_f18-{F}(V7,V1,V8), P_f16-{F}(V8,V2,V9), P_c54-{F}(V10), P_c55-{F}(V11), P_c56-{F}(V12), p7-{F}(V11,V13), P_f18-{F}(V7,V14,V15), P_f26-{F}(V12,V14,V16), P_f36-{F}(V4,V14,V17), P_f46-{F}(V5,V14,V18), P_f16-{F}(V15,V19,V9), P_f24-{F}(V16,V19,V20), P_f44-{F}(V18,V19,V21), P_f22-{F}(V20,V3,V22), P_f42-{F}(V21,V3,V23), P_f20-{F}(V22,V10,V24), P_f20-{F}(V25,V13,V24), P_f26-{F}(V12,V26,V27), P_f24-{F}(V27,V28,V29), P_f22-{F}(V29,V30,V25) | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #484: exists( #92, #481 ), references = 2, size of lhs = 28:
% 8.55/8.73 P_c49-{F}(V0), P_c51-{F}(V1), P_c52-{F}(V2), P_c53-{F}(V3), P_c57-{F}(V4), P_c58-{F}(V5), P_c48-{F}(V6), p2-{F}(V6,V6), P_c50-{F}(V7), P_f18-{F}(V7,V1,V8), P_f16-{F}(V8,V2,V9), P_c54-{F}(V10), P_c55-{F}(V11), P_c56-{F}(V12), p7-{F}(V11,V13), P_f18-{F}(V7,V14,V15), P_f26-{F}(V12,V14,V16), P_f36-{F}(V4,V14,V17), P_f46-{F}(V5,V14,V18), P_f16-{F}(V15,V19,V9), P_f24-{F}(V16,V19,V20), P_f44-{F}(V18,V19,V21), P_f22-{F}(V20,V3,V22), P_f20-{F}(V22,V10,V23), P_f20-{F}(V24,V13,V23), P_f26-{F}(V12,V25,V26), P_f24-{F}(V26,V27,V28), P_f22-{F}(V28,V29,V24) | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #495: mergings( V3 == V15, V15 == V19, V4 == V16, V16 == V20, V5 == V17, V17 == V21, V6 == V18; #487 ), references = 1, size of lhs = 21:
% 8.55/8.73 P_c49-{F}(V0), P_c51-{F}(V1), P_c52-{F}(V2), P_c53-{F}(V3), P_c48-{F}(V4), P_c50-{F}(V5), P_f18-{F}(V5,V1,V6), P_f16-{F}(V6,V2,V7), P_f13-{F}(V7,V3,V8), P_f10-{F}(V0,V8,V9), P_c54-{F}(V10), P_f8-{F}(V9,V10,V11), P_c55-{F}(V12), P_c56-{F}(V13), P_f26-{F}(V13,V14,V15), P_f24-{F}(V15,V16,V17), P_f22-{F}(V17,V18,V19), P_f20-{F}(V19,V12,V20), P_f18-{F}(V5,V20,V21), P_f16-{F}(V21,V22,V23), P_f13-{F}(V23,V24,V11) | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #497: exists( #90, #484 ), references = 1, size of lhs = 27:
% 8.55/8.73 P_c49-{F}(V0), P_c51-{F}(V1), P_c52-{F}(V2), P_c53-{F}(V3), P_c57-{F}(V4), P_c58-{F}(V5), P_c48-{F}(V6), p2-{F}(V6,V6), P_c50-{F}(V7), P_f18-{F}(V7,V1,V8), P_f16-{F}(V8,V2,V9), P_c54-{F}(V10), P_c55-{F}(V11), P_c56-{F}(V12), p7-{F}(V11,V13), P_f18-{F}(V7,V14,V15), P_f26-{F}(V12,V14,V16), P_f36-{F}(V4,V14,V17), P_f46-{F}(V5,V14,V18), P_f16-{F}(V15,V19,V9), P_f24-{F}(V16,V19,V20), P_f22-{F}(V20,V3,V21), P_f20-{F}(V21,V10,V22), P_f20-{F}(V23,V13,V22), P_f26-{F}(V12,V24,V25), P_f24-{F}(V25,V26,V27), P_f22-{F}(V27,V28,V23) | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #499: exists( #89, #496 ), references = 2, size of lhs = 26:
% 8.55/8.73 P_c49-{F}(V0), P_c51-{F}(V1), P_c52-{F}(V2), P_c53-{F}(V3), P_c57-{F}(V4), P_c58-{F}(V5), P_c48-{F}(V6), p2-{F}(V6,V6), P_c50-{F}(V7), P_f18-{F}(V7,V1,V8), P_f16-{F}(V8,V2,V9), P_c54-{F}(V10), P_c55-{F}(V11), P_c56-{F}(V12), p7-{F}(V11,V13), P_f18-{F}(V7,V14,V15), P_f26-{F}(V12,V14,V16), P_f36-{F}(V4,V14,V17), P_f16-{F}(V15,V18,V9), P_f24-{F}(V16,V18,V19), P_f22-{F}(V19,V3,V20), P_f20-{F}(V20,V10,V21), P_f20-{F}(V22,V13,V21), P_f26-{F}(V12,V23,V24), P_f24-{F}(V24,V25,V26), P_f22-{F}(V26,V27,V22) | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #501: exists( #87, #498 ), references = 2, size of lhs = 24:
% 8.55/8.73 P_c49-{F}(V0), P_c51-{F}(V1), P_c52-{F}(V2), P_c53-{F}(V3), P_c57-{F}(V4), P_c58-{F}(V5), P_c48-{F}(V6), p2-{F}(V6,V6), P_c50-{F}(V7), P_f18-{F}(V7,V1,V8), P_c54-{F}(V9), P_c55-{F}(V10), P_c56-{F}(V11), p7-{F}(V10,V12), P_f18-{F}(V7,V13,V8), P_f26-{F}(V11,V13,V14), P_f36-{F}(V4,V13,V15), P_f24-{F}(V14,V2,V16), P_f22-{F}(V16,V3,V17), P_f20-{F}(V17,V9,V18), P_f20-{F}(V19,V12,V18), P_f26-{F}(V11,V20,V21), P_f24-{F}(V21,V22,V23), P_f22-{F}(V23,V24,V19) | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #504: exists( #82, #501 ), references = 1, size of lhs = 22:
% 8.55/8.73 P_c49-{F}(V0), P_c51-{F}(V1), P_c52-{F}(V2), P_c53-{F}(V3), P_c57-{F}(V4), P_c58-{F}(V5), P_c48-{F}(V6), p2-{F}(V6,V6), P_c50-{F}(V7), P_f18-{F}(V7,V1,V8), P_c54-{F}(V9), P_c55-{F}(V10), p7-{F}(V10,V9), P_c56-{F}(V11), P_f18-{F}(V7,V12,V8), P_f26-{F}(V11,V12,V13), P_f36-{F}(V4,V12,V14), P_f24-{F}(V13,V2,V15), P_f22-{F}(V15,V3,V16), P_f26-{F}(V11,V17,V18), P_f24-{F}(V18,V19,V20), P_f22-{F}(V20,V21,V16) | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #505: exists( #82, #499 ), references = 1, size of lhs = 24:
% 8.55/8.73 P_c49-{F}(V0), P_c51-{F}(V1), P_c52-{F}(V2), P_c53-{F}(V3), P_c57-{F}(V4), P_c58-{F}(V5), P_c48-{F}(V6), p2-{F}(V6,V6), P_c50-{F}(V7), P_f18-{F}(V7,V1,V8), P_f16-{F}(V8,V2,V9), P_c54-{F}(V10), P_c55-{F}(V11), p7-{F}(V11,V10), P_c56-{F}(V12), P_f18-{F}(V7,V13,V14), P_f26-{F}(V12,V13,V15), P_f36-{F}(V4,V13,V16), P_f16-{F}(V14,V17,V9), P_f24-{F}(V15,V17,V18), P_f22-{F}(V18,V3,V19), P_f26-{F}(V12,V20,V21), P_f24-{F}(V21,V22,V23), P_f22-{F}(V23,V24,V19) | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #508: exists( #83, #502 ), references = 1, size of lhs = 20:
% 8.55/8.73 P_c49-{F}(V0), P_c51-{F}(V1), P_c52-{F}(V2), P_c53-{F}(V3), P_c57-{F}(V4), P_c58-{F}(V5), P_c48-{F}(V6), p2-{F}(V6,V6), P_c50-{F}(V7), P_f18-{F}(V7,V1,V8), P_c54-{F}(V9), P_c55-{F}(V10), p7-{F}(V10,V9), P_c56-{F}(V11), P_f18-{F}(V7,V12,V8), P_f26-{F}(V11,V12,V13), P_f36-{F}(V4,V12,V14), P_f24-{F}(V13,V2,V15), P_f26-{F}(V11,V16,V17), P_f24-{F}(V17,V18,V15) | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #510: exists( #84, #506 ), references = 1, size of lhs = 18:
% 8.55/8.73 P_c49-{F}(V0), P_c51-{F}(V1), P_c52-{F}(V2), P_c53-{F}(V3), P_c57-{F}(V4), P_c58-{F}(V5), P_c48-{F}(V6), p2-{F}(V6,V6), P_c50-{F}(V7), P_f18-{F}(V7,V1,V8), P_c54-{F}(V9), P_c55-{F}(V10), p7-{F}(V10,V9), P_c56-{F}(V11), P_f18-{F}(V7,V12,V8), P_f26-{F}(V11,V12,V13), P_f36-{F}(V4,V12,V14), P_f26-{F}(V11,V15,V13) | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #512: exists( #101, #509 ), references = 1, size of lhs = 16:
% 8.55/8.73 P_c49-{F}(V0), P_c51-{F}(V1), P_c52-{F}(V2), P_c53-{F}(V3), P_c57-{F}(V4), P_c58-{F}(V5), P_c48-{F}(V6), p2-{F}(V6,V6), P_c50-{F}(V7), P_c54-{F}(V8), P_c55-{F}(V9), p7-{F}(V9,V8), P_c56-{F}(V10), P_f26-{F}(V10,V1,V11), P_f36-{F}(V4,V1,V12), P_f26-{F}(V10,V13,V11) | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #514: exists( #94, #511 ), references = 1, size of lhs = 15:
% 8.55/8.73 P_c49-{F}(V0), P_c51-{F}(V1), P_c52-{F}(V2), P_c53-{F}(V3), P_c57-{F}(V4), P_c58-{F}(V5), P_c48-{F}(V6), p2-{F}(V6,V6), P_c50-{F}(V7), P_c54-{F}(V8), P_c55-{F}(V9), p7-{F}(V9,V8), P_c56-{F}(V10), P_f26-{F}(V10,V1,V11), P_f26-{F}(V10,V12,V11) | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #516: exists( #85, #513 ), references = 1, size of lhs = 13:
% 8.55/8.73 P_c49-{F}(V0), P_c51-{F}(V1), P_c52-{F}(V2), P_c53-{F}(V3), P_c57-{F}(V4), P_c58-{F}(V5), P_c48-{F}(V6), p2-{F}(V6,V6), P_c50-{F}(V7), P_c54-{F}(V8), P_c55-{F}(V9), p7-{F}(V9,V8), P_c56-{F}(V10) | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #518: exists( #110, #515 ), references = 1, size of lhs = 12:
% 8.55/8.73 P_c49-{F}(V0), P_c51-{F}(V1), P_c52-{F}(V2), P_c53-{F}(V3), P_c57-{F}(V4), P_c48-{F}(V5), p2-{F}(V5,V5), P_c50-{F}(V6), P_c54-{F}(V7), P_c55-{F}(V8), p7-{F}(V8,V7), P_c56-{F}(V9) | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #520: exists( #109, #517 ), references = 1, size of lhs = 11:
% 8.55/8.73 P_c49-{F}(V0), P_c51-{F}(V1), P_c52-{F}(V2), P_c53-{F}(V3), P_c48-{F}(V4), p2-{F}(V4,V4), P_c50-{F}(V5), P_c54-{F}(V6), P_c55-{F}(V7), p7-{F}(V7,V6), P_c56-{F}(V8) | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #522: exists( #108, #519 ), references = 1, size of lhs = 10:
% 8.55/8.73 P_c49-{F}(V0), P_c51-{F}(V1), P_c52-{F}(V2), P_c48-{F}(V3), p2-{F}(V3,V3), P_c50-{F}(V4), P_c54-{F}(V5), P_c55-{F}(V6), p7-{F}(V6,V5), P_c56-{F}(V7) | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #524: exists( #107, #521 ), references = 1, size of lhs = 9:
% 8.55/8.73 P_c49-{F}(V0), P_c51-{F}(V1), P_c48-{F}(V2), p2-{F}(V2,V2), P_c50-{F}(V3), P_c54-{F}(V4), P_c55-{F}(V5), p7-{F}(V5,V4), P_c56-{F}(V6) | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #526: exists( #106, #523 ), references = 1, size of lhs = 8:
% 8.55/8.73 P_c49-{F}(V0), P_c48-{F}(V1), p2-{F}(V1,V1), P_c50-{F}(V2), P_c54-{F}(V3), P_c55-{F}(V4), p7-{F}(V4,V3), P_c56-{F}(V5) | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #528: exists( #105, #525 ), references = 1, size of lhs = 7:
% 8.55/8.73 P_c48-{F}(V0), p2-{F}(V0,V0), P_c50-{F}(V1), P_c54-{F}(V2), P_c55-{F}(V3), p7-{F}(V3,V2), P_c56-{F}(V4) | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #530: exists( #104, #527 ), references = 2, size of lhs = 6:
% 8.55/8.73 P_c48-{F}(V0), p2-{F}(V0,V0), P_c54-{F}(V1), P_c55-{F}(V2), p7-{F}(V2,V1), P_c56-{F}(V3) | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #533: exists( #103, #531 ), references = 1, size of lhs = 4:
% 8.55/8.73 P_c54-{F}(V0), P_c55-{F}(V1), p7-{F}(V1,V0), P_c56-{F}(V2) | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #535: exists( #86, #532 ), references = 2, size of lhs = 3:
% 8.55/8.73 P_c54-{F}(V0), P_c55-{F}(V1), p7-{F}(V1,V0) | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #541: mergings( V1 == V2, V2 == V3; #538 ), references = 1, size of lhs = 2:
% 8.55/8.73 P_c54-{F}(V0), p7-{F}(V0,V0) | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 #544: exists( #80, #542 ), references = 1, size of lhs = 0:
% 8.55/8.73 FALSE | FALSE
% 8.55/8.73 (used 0 times, uses = {})
% 8.55/8.73
% 8.55/8.73 number of learnt formulas = 43
% 8.55/8.73
% 8.55/8.73
% 8.55/8.73 % SZS output end Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 8.55/8.73
% 8.55/8.73 randbase = 1
%------------------------------------------------------------------------------