%------------------------------------------------------------------------------
% File : Geo-III---2018C
% Problem : LCL642+1.005 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : geo -tptp_input -nonempty -inputfile %s
% Computer : n027.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Sep 7 12:06:32 PM UTC 2026
% Result : Theorem 12.37s 12.68s
% Output : Refutation 12.37s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL642+1.005 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : geo -tptp_input -nonempty -inputfile %s
% 0.09/0.36 % Computer : n027.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sat Sep 5 04:54:28 UTC 2026
% 0.14/0.36 % CPUTime :
% 12.37/12.68 GeoParameters:
% 12.37/12.68
% 12.37/12.68 tptp_input = 1
% 12.37/12.68 tptp_output = 0
% 12.37/12.68 nonempty = 1
% 12.37/12.68 inputfile = /export/starexec/sandbox2/benchmark/theBenchmark.p
% 12.37/12.68 includepath = /export/starexec/sandbox2/solver/bin/../../benchmark/
% 12.37/12.68
% 12.37/12.68
% 12.37/12.68 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 12.37/12.68 % SZS output start Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 12.37/12.68
% 12.37/12.68 RuleSystem INPUT:
% 12.37/12.68
% 12.37/12.68 Initial Rules:
% 12.37/12.68 #0: input, references = 4, size of lhs = 0:
% 12.37/12.68 FALSE | EXISTS V0: pppp49-{T}(V0)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #1: input, references = 4, size of lhs = 1:
% 12.37/12.68 pppp49-{F}(V0) | pppp48-{T}(V0)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #2: input, references = 8, size of lhs = 2:
% 12.37/12.68 pppp48-{F}(V0), r1-{F}(V0,V1) | p2-{T}(V1), pppp50-{T}(V1)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #3: input, references = 8, size of lhs = 1:
% 12.37/12.68 pppp50-{F}(V0) | EXISTS V1: pppp47-{T}(V1,V0)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #4: input, references = 4, size of lhs = 2:
% 12.37/12.68 pppp48-{F}(V0), r1-{F}(V0,V1) | p1-{T}(V0), pppp51-{T}(V0)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #5: input, references = 3, size of lhs = 1:
% 12.37/12.68 pppp51-{F}(V0) | EXISTS V1: pppp46-{T}(V0,V1)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #6: input, references = 3, size of lhs = 2:
% 12.37/12.68 pppp48-{F}(V0), r1-{F}(V0,V1) | p2-{T}(V0), p1-{T}(V0), pppp52-{T}(V0)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #7: input, references = 3, size of lhs = 1:
% 12.37/12.68 pppp52-{F}(V0) | EXISTS V1: pppp42-{T}(V0,V1)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #8: input, references = 3, size of lhs = 2:
% 12.37/12.68 pppp48-{F}(V0), r1-{F}(V0,V1) | p3-{T}(V0), p2-{T}(V0), p1-{T}(V0), pppp53-{T}(V0)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #9: input, references = 3, size of lhs = 1:
% 12.37/12.68 pppp53-{F}(V0) | EXISTS V1: pppp38-{T}(V0,V1)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #10: input, references = 3, size of lhs = 2:
% 12.37/12.68 pppp48-{F}(V0), r1-{F}(V0,V1) | p4-{T}(V0), p3-{T}(V0), p2-{T}(V0), p1-{T}(V0), pppp54-{T}(V0)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #11: input, references = 3, size of lhs = 1:
% 12.37/12.68 pppp54-{F}(V0) | EXISTS V1: pppp34-{T}(V0,V1)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #12: input, references = 3, size of lhs = 1:
% 12.37/12.68 pppp48-{F}(V0) | p2-{T}(V0), pppp55-{T}(V0), pppp56-{T}(V0)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #13: input, references = 3, size of lhs = 1:
% 12.37/12.68 pppp55-{F}(V0) | EXISTS V1: pppp13-{T}(V0,V1)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #14: input, references = 3, size of lhs = 1:
% 12.37/12.68 pppp56-{F}(V0) | EXISTS V1: pppp29-{T}(V0,V1)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #15: input, references = 4, size of lhs = 3:
% 12.37/12.68 pppp48-{F}(V0), r1-{F}(V0,V1), r1-{F}(V1,V2) | p2-{T}(V2), pppp57-{T}(V2), pppp58-{T}(V0), pppp59-{T}(V0)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #16: input, references = 5, size of lhs = 1:
% 12.37/12.68 pppp57-{F}(V0) | EXISTS V1: pppp10-{T}(V0,V1)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #17: input, references = 4, size of lhs = 1:
% 12.37/12.68 pppp58-{F}(V0) | EXISTS V1: pppp11-{T}(V0,V1)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #18: input, references = 4, size of lhs = 1:
% 12.37/12.68 pppp59-{F}(V0) | EXISTS V1: pppp29-{T}(V0,V1)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #19: input, references = 5, size of lhs = 2:
% 12.37/12.68 pppp48-{F}(V0), r1-{F}(V0,V1) | p1-{T}(V1), pppp60-{T}(V1)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #20: input, references = 3, size of lhs = 1:
% 12.37/12.68 pppp60-{F}(V0) | EXISTS V1: pppp8-{T}(V1,V0)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #21: input, references = 3, size of lhs = 1:
% 12.37/12.68 pppp48-{F}(V0) | EXISTS V1: pppp6-{T}(V0,V1)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #22: input, references = 7, size of lhs = 2:
% 12.37/12.68 pppp48-{F}(V0), r1-{F}(V0,V1) | p2-{T}(V1), pppp61-{T}(V1)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #23: input, references = 6, size of lhs = 1:
% 12.37/12.68 pppp61-{F}(V0) | EXISTS V1: pppp5-{T}(V1,V0)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #24: input, references = 4, size of lhs = 1:
% 12.37/12.68 pppp48-{F}(V0) | EXISTS V1: pppp3-{T}(V0,V1)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #25: input, references = 4, size of lhs = 2:
% 12.37/12.68 pppp48-{F}(V0), r1-{F}(V0,V1) | p3-{T}(V1), pppp62-{T}(V1)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #26: input, references = 3, size of lhs = 1:
% 12.37/12.68 pppp62-{F}(V0) | EXISTS V1: pppp2-{T}(V1,V0)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #27: input, references = 3, size of lhs = 1:
% 12.37/12.68 pppp48-{F}(V0) | EXISTS V1: pppp0-{T}(V0,V1)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #28: input, references = 7, size of lhs = 4:
% 12.37/12.68 pppp47-{F}(V0,V1), r1-{F}(V0,V2), r1-{F}(V2,V3), p2-{F}(V2) | p2-{T}(V3)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #29: input, references = 4, size of lhs = 2:
% 12.37/12.68 pppp47-{F}(V0,V1), p2-{F}(V0) | FALSE
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #30: input, references = 9, size of lhs = 1:
% 12.37/12.68 pppp47-{F}(V0,V1) | r1-{T}(V1,V0)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #31: input, references = 3, size of lhs = 1:
% 12.37/12.68 pppp46-{F}(V0,V1) | pppp45-{T}(V0,V1)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #32: input, references = 5, size of lhs = 4:
% 12.37/12.68 pppp45-{F}(V0,V1), r1-{F}(V1,V2), r1-{F}(V2,V3), r1-{F}(V3,V4) | p1-{T}(V3), pppp63-{T}(V2)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #33: input, references = 3, size of lhs = 1:
% 12.37/12.68 pppp63-{F}(V0) | EXISTS V1: pppp44-{T}(V0,V1)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #34: input, references = 13, size of lhs = 5:
% 12.37/12.68 pppp45-{F}(V0,V1), r1-{F}(V1,V2), r1-{F}(V2,V3), r1-{F}(V3,V4), p1-{F}(V2) | p1-{T}(V3)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #35: input, references = 3, size of lhs = 1:
% 12.37/12.68 pppp45-{F}(V0,V1) | EXISTS V2: pppp43-{T}(V1,V2)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #36: input, references = 3, size of lhs = 2:
% 12.37/12.68 pppp45-{F}(V0,V1), p1-{F}(V1) | FALSE
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #37: input, references = 3, size of lhs = 1:
% 12.37/12.68 pppp45-{F}(V0,V1) | r1-{T}(V0,V1)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #38: input, references = 3, size of lhs = 1:
% 12.37/12.68 pppp44-{F}(V0,V1) | r1-{T}(V0,V1)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #39: input, references = 3, size of lhs = 1:
% 12.37/12.68 pppp43-{F}(V0,V1) | r1-{T}(V0,V1)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #40: input, references = 3, size of lhs = 1:
% 12.37/12.68 pppp42-{F}(V0,V1) | pppp41-{T}(V0,V1)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #41: input, references = 4, size of lhs = 4:
% 12.37/12.68 pppp41-{F}(V0,V1), r1-{F}(V1,V2), r1-{F}(V2,V3), r1-{F}(V3,V4) | p2-{T}(V3), p1-{T}(V3), pppp64-{T}(V2)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #42: input, references = 3, size of lhs = 1:
% 12.37/12.68 pppp64-{F}(V0) | EXISTS V1: pppp40-{T}(V0,V1)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #43: input, references = 3, size of lhs = 5:
% 12.37/12.68 pppp41-{F}(V0,V1), r1-{F}(V1,V2), r1-{F}(V2,V3), r1-{F}(V3,V4), p1-{F}(V2) | p2-{T}(V3), p1-{T}(V3)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #44: input, references = 4, size of lhs = 5:
% 12.37/12.68 pppp41-{F}(V0,V1), r1-{F}(V1,V2), r1-{F}(V2,V3), r1-{F}(V3,V4), p2-{F}(V2) | p2-{T}(V3), p1-{T}(V3)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #45: input, references = 3, size of lhs = 1:
% 12.37/12.68 pppp41-{F}(V0,V1) | EXISTS V2: pppp39-{T}(V1,V2)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #46: input, references = 3, size of lhs = 2:
% 12.37/12.68 pppp41-{F}(V0,V1), p1-{F}(V1) | FALSE
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #47: input, references = 3, size of lhs = 2:
% 12.37/12.68 pppp41-{F}(V0,V1), p2-{F}(V1) | FALSE
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #48: input, references = 3, size of lhs = 1:
% 12.37/12.68 pppp41-{F}(V0,V1) | r1-{T}(V0,V1)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #49: input, references = 3, size of lhs = 1:
% 12.37/12.68 pppp40-{F}(V0,V1) | r1-{T}(V0,V1)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #50: input, references = 3, size of lhs = 1:
% 12.37/12.68 pppp39-{F}(V0,V1) | r1-{T}(V0,V1)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #51: input, references = 3, size of lhs = 1:
% 12.37/12.68 pppp38-{F}(V0,V1) | pppp37-{T}(V0,V1)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #52: input, references = 3, size of lhs = 4:
% 12.37/12.68 pppp37-{F}(V0,V1), r1-{F}(V1,V2), r1-{F}(V2,V3), r1-{F}(V3,V4) | p3-{T}(V3), p2-{T}(V3), p1-{T}(V3), pppp65-{T}(V2)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #53: input, references = 3, size of lhs = 1:
% 12.37/12.68 pppp65-{F}(V0) | EXISTS V1: pppp36-{T}(V0,V1)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #54: input, references = 3, size of lhs = 5:
% 12.37/12.68 pppp37-{F}(V0,V1), r1-{F}(V1,V2), r1-{F}(V2,V3), r1-{F}(V3,V4), p1-{F}(V2) | p3-{T}(V3), p2-{T}(V3), p1-{T}(V3)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #55: input, references = 3, size of lhs = 5:
% 12.37/12.68 pppp37-{F}(V0,V1), r1-{F}(V1,V2), r1-{F}(V2,V3), r1-{F}(V3,V4), p2-{F}(V2) | p3-{T}(V3), p2-{T}(V3), p1-{T}(V3)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #56: input, references = 3, size of lhs = 5:
% 12.37/12.68 pppp37-{F}(V0,V1), r1-{F}(V1,V2), r1-{F}(V2,V3), r1-{F}(V3,V4), p3-{F}(V2) | p3-{T}(V3), p2-{T}(V3), p1-{T}(V3)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #57: input, references = 4, size of lhs = 1:
% 12.37/12.68 pppp37-{F}(V0,V1) | EXISTS V2: pppp35-{T}(V1,V2)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #58: input, references = 5, size of lhs = 2:
% 12.37/12.68 pppp37-{F}(V0,V1), p1-{F}(V1) | FALSE
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #59: input, references = 3, size of lhs = 2:
% 12.37/12.68 pppp37-{F}(V0,V1), p2-{F}(V1) | FALSE
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #60: input, references = 3, size of lhs = 2:
% 12.37/12.68 pppp37-{F}(V0,V1), p3-{F}(V1) | FALSE
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #61: input, references = 3, size of lhs = 1:
% 12.37/12.68 pppp37-{F}(V0,V1) | r1-{T}(V0,V1)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #62: input, references = 3, size of lhs = 1:
% 12.37/12.68 pppp36-{F}(V0,V1) | r1-{T}(V0,V1)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #63: input, references = 4, size of lhs = 1:
% 12.37/12.68 pppp35-{F}(V0,V1) | r1-{T}(V0,V1)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #64: input, references = 3, size of lhs = 1:
% 12.37/12.68 pppp34-{F}(V0,V1) | pppp33-{T}(V0,V1)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #65: input, references = 3, size of lhs = 4:
% 12.37/12.68 pppp33-{F}(V0,V1), r1-{F}(V1,V2), r1-{F}(V2,V3), r1-{F}(V3,V4) | p4-{T}(V3), p3-{T}(V3), p2-{T}(V3), p1-{T}(V3), pppp32-{T}(V2)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #66: input, references = 3, size of lhs = 1:
% 12.37/12.68 pppp33-{F}(V0,V1) | EXISTS V2: pppp30-{T}(V1,V2)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #67: input, references = 3, size of lhs = 2:
% 12.37/12.68 pppp33-{F}(V0,V1), p1-{F}(V1) | FALSE
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #68: input, references = 3, size of lhs = 2:
% 12.37/12.68 pppp33-{F}(V0,V1), p2-{F}(V1) | FALSE
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #69: input, references = 3, size of lhs = 2:
% 12.37/12.68 pppp33-{F}(V0,V1), p3-{F}(V1) | FALSE
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #70: input, references = 3, size of lhs = 2:
% 12.37/12.68 pppp33-{F}(V0,V1), p4-{F}(V1) | FALSE
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #71: input, references = 3, size of lhs = 1:
% 12.37/12.68 pppp33-{F}(V0,V1) | r1-{T}(V0,V1)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #72: input, references = 3, size of lhs = 1:
% 12.37/12.68 pppp32-{F}(V0) | EXISTS V1: pppp31-{T}(V0,V1)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #73: input, references = 3, size of lhs = 2:
% 12.37/12.68 pppp32-{F}(V0), p1-{F}(V0) | FALSE
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #74: input, references = 3, size of lhs = 2:
% 12.37/12.68 pppp32-{F}(V0), p2-{F}(V0) | FALSE
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #75: input, references = 3, size of lhs = 2:
% 12.37/12.68 pppp32-{F}(V0), p3-{F}(V0) | FALSE
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #76: input, references = 3, size of lhs = 2:
% 12.37/12.68 pppp32-{F}(V0), p4-{F}(V0) | FALSE
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #77: input, references = 3, size of lhs = 1:
% 12.37/12.68 pppp31-{F}(V0,V1) | r1-{T}(V0,V1)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #78: input, references = 3, size of lhs = 1:
% 12.37/12.68 pppp30-{F}(V0,V1) | r1-{T}(V0,V1)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #79: input, references = 4, size of lhs = 1:
% 12.37/12.68 pppp29-{F}(V0,V1) | pppp28-{T}(V0,V1)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #80: input, references = 15, size of lhs = 6:
% 12.37/12.68 pppp28-{F}(V0,V1), r1-{F}(V1,V2), r1-{F}(V2,V3), r1-{F}(V2,V4), r1-{F}(V4,V5), p2-{F}(V4) | pppp27-{T}(V2), p2-{T}(V3), pppp66-{T}(V3), p2-{T}(V5)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #81: input, references = 5, size of lhs = 1:
% 12.37/12.68 pppp66-{F}(V0) | EXISTS V1: pppp26-{T}(V1,V0)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #82: input, references = 5, size of lhs = 4:
% 12.37/12.68 pppp28-{F}(V0,V1), r1-{F}(V1,V2), r1-{F}(V2,V3), p2-{F}(V2) | pppp27-{T}(V2), p2-{T}(V3), pppp67-{T}(V3)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #83: input, references = 5, size of lhs = 1:
% 12.37/12.68 pppp67-{F}(V0) | EXISTS V1: pppp26-{T}(V1,V0)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #84: input, references = 5, size of lhs = 5:
% 12.37/12.68 pppp28-{F}(V0,V1), r1-{F}(V1,V2), r1-{F}(V2,V3), r1-{F}(V3,V4), p2-{F}(V3) | pppp27-{T}(V2), pppp68-{T}(V2), p2-{T}(V4)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #85: input, references = 3, size of lhs = 1:
% 12.37/12.68 pppp68-{F}(V0) | EXISTS V1: pppp24-{T}(V0,V1)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #86: input, references = 4, size of lhs = 3:
% 12.37/12.68 pppp28-{F}(V0,V1), r1-{F}(V1,V2), p2-{F}(V2) | pppp27-{T}(V2), pppp69-{T}(V2)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #87: input, references = 3, size of lhs = 1:
% 12.37/12.68 pppp69-{F}(V0) | EXISTS V1: pppp24-{T}(V0,V1)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #88: input, references = 8, size of lhs = 5:
% 12.37/12.68 pppp28-{F}(V0,V1), r1-{F}(V1,V2), r1-{F}(V1,V3), r1-{F}(V3,V4), p2-{F}(V3) | p2-{T}(V2), pppp70-{T}(V2), p2-{T}(V4)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #89: input, references = 5, size of lhs = 1:
% 12.37/12.68 pppp70-{F}(V0) | EXISTS V1: pppp17-{T}(V0,V1)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #90: input, references = 7, size of lhs = 3:
% 12.37/12.68 pppp28-{F}(V0,V1), r1-{F}(V1,V2), p2-{F}(V1) | p2-{T}(V2), pppp71-{T}(V2)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #91: input, references = 8, size of lhs = 1:
% 12.37/12.68 pppp71-{F}(V0) | EXISTS V1: pppp17-{T}(V0,V1)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #92: input, references = 5, size of lhs = 4:
% 12.37/12.68 pppp28-{F}(V0,V1), r1-{F}(V1,V2), r1-{F}(V2,V3), p2-{F}(V2) | pppp72-{T}(V1), p2-{T}(V3)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #93: input, references = 3, size of lhs = 1:
% 12.37/12.68 pppp72-{F}(V0) | EXISTS V1: pppp15-{T}(V1,V0)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #94: input, references = 4, size of lhs = 2:
% 12.37/12.68 pppp28-{F}(V0,V1), p2-{F}(V1) | EXISTS V2: pppp15-{T}(V2,V1)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #95: input, references = 4, size of lhs = 1:
% 12.37/12.68 pppp28-{F}(V0,V1) | r1-{T}(V0,V1)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #96: input, references = 5, size of lhs = 2:
% 12.37/12.68 pppp27-{F}(V0), r1-{F}(V0,V1) | p2-{T}(V1), pppp73-{T}(V1)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #97: input, references = 5, size of lhs = 1:
% 12.37/12.68 pppp73-{F}(V0) | EXISTS V1: pppp22-{T}(V1,V0)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #98: input, references = 3, size of lhs = 4:
% 12.37/12.68 pppp27-{F}(V0), r1-{F}(V0,V1), r1-{F}(V1,V2), r1-{F}(V2,V3) | p2-{T}(V3), pppp74-{T}(V3), pppp75-{T}(V1)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #99: input, references = 3, size of lhs = 1:
% 12.37/12.68 pppp74-{F}(V0) | EXISTS V1: pppp19-{T}(V1,V0)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #100: input, references = 3, size of lhs = 1:
% 12.37/12.68 pppp75-{F}(V0) | EXISTS V1: pppp20-{T}(V1,V0)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #101: input, references = 5, size of lhs = 1:
% 12.37/12.68 pppp26-{F}(V0,V1) | p2-{T}(V0)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #102: input, references = 4, size of lhs = 1:
% 12.37/12.68 pppp26-{F}(V0,V1) | EXISTS V2: pppp25-{T}(V0,V2)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #103: input, references = 7, size of lhs = 1:
% 12.37/12.68 pppp26-{F}(V0,V1) | r1-{T}(V1,V0)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #104: input, references = 4, size of lhs = 2:
% 12.37/12.68 pppp25-{F}(V0,V1), p2-{F}(V1) | FALSE
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #105: input, references = 4, size of lhs = 1:
% 12.37/12.68 pppp25-{F}(V0,V1) | r1-{T}(V0,V1)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #106: input, references = 3, size of lhs = 1:
% 12.37/12.68 pppp24-{F}(V0,V1) | EXISTS V2: pppp23-{T}(V2,V1)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #107: input, references = 3, size of lhs = 1:
% 12.37/12.68 pppp24-{F}(V0,V1) | r1-{T}(V0,V1)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #108: input, references = 3, size of lhs = 4:
% 12.37/12.68 pppp23-{F}(V0,V1), r1-{F}(V0,V2), r1-{F}(V2,V3), p2-{F}(V2) | p2-{T}(V3)
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.68
% 12.37/12.68 #109: input, references = 3, size of lhs = 2:
% 12.37/12.68 pppp23-{F}(V0,V1), p2-{F}(V0) | FALSE
% 12.37/12.68 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #110: input, references = 3, size of lhs = 1:
% 12.37/12.69 pppp23-{F}(V0,V1) | r1-{T}(V1,V0)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #111: input, references = 4, size of lhs = 1:
% 12.37/12.69 pppp22-{F}(V0,V1) | p2-{T}(V0)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #112: input, references = 4, size of lhs = 1:
% 12.37/12.69 pppp22-{F}(V0,V1) | EXISTS V2: pppp21-{T}(V0,V2)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #113: input, references = 5, size of lhs = 1:
% 12.37/12.69 pppp22-{F}(V0,V1) | r1-{T}(V1,V0)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #114: input, references = 4, size of lhs = 2:
% 12.37/12.69 pppp21-{F}(V0,V1), p2-{F}(V1) | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #115: input, references = 4, size of lhs = 1:
% 12.37/12.69 pppp21-{F}(V0,V1) | r1-{T}(V0,V1)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #116: input, references = 3, size of lhs = 4:
% 12.37/12.69 pppp20-{F}(V0,V1), r1-{F}(V0,V2), r1-{F}(V2,V3), p2-{F}(V2) | p2-{T}(V3)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #117: input, references = 3, size of lhs = 2:
% 12.37/12.69 pppp20-{F}(V0,V1), p2-{F}(V0) | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #118: input, references = 3, size of lhs = 1:
% 12.37/12.69 pppp20-{F}(V0,V1) | r1-{T}(V1,V0)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #119: input, references = 3, size of lhs = 1:
% 12.37/12.69 pppp19-{F}(V0,V1) | p2-{T}(V0)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #120: input, references = 3, size of lhs = 1:
% 12.37/12.69 pppp19-{F}(V0,V1) | EXISTS V2: pppp18-{T}(V0,V2)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #121: input, references = 3, size of lhs = 1:
% 12.37/12.69 pppp19-{F}(V0,V1) | r1-{T}(V1,V0)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #122: input, references = 3, size of lhs = 2:
% 12.37/12.69 pppp18-{F}(V0,V1), p2-{F}(V1) | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #123: input, references = 3, size of lhs = 1:
% 12.37/12.69 pppp18-{F}(V0,V1) | r1-{T}(V0,V1)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #124: input, references = 9, size of lhs = 1:
% 12.37/12.69 pppp17-{F}(V0,V1) | p2-{T}(V1)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #125: input, references = 7, size of lhs = 1:
% 12.37/12.69 pppp17-{F}(V0,V1) | EXISTS V2: pppp16-{T}(V2,V1)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #126: input, references = 10, size of lhs = 1:
% 12.37/12.69 pppp17-{F}(V0,V1) | r1-{T}(V0,V1)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #127: input, references = 6, size of lhs = 2:
% 12.37/12.69 pppp16-{F}(V0,V1), p2-{F}(V0) | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #128: input, references = 7, size of lhs = 1:
% 12.37/12.69 pppp16-{F}(V0,V1) | r1-{T}(V1,V0)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #129: input, references = 5, size of lhs = 1:
% 12.37/12.69 pppp15-{F}(V0,V1) | EXISTS V2: pppp14-{T}(V0,V2)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #130: input, references = 4, size of lhs = 1:
% 12.37/12.69 pppp15-{F}(V0,V1) | r1-{T}(V1,V0)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #131: input, references = 6, size of lhs = 4:
% 12.37/12.69 pppp14-{F}(V0,V1), r1-{F}(V1,V2), r1-{F}(V2,V3), p2-{F}(V2) | p2-{T}(V3)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #132: input, references = 4, size of lhs = 2:
% 12.37/12.69 pppp14-{F}(V0,V1), p2-{F}(V1) | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #133: input, references = 5, size of lhs = 1:
% 12.37/12.69 pppp14-{F}(V0,V1) | r1-{T}(V0,V1)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #134: input, references = 3, size of lhs = 1:
% 12.37/12.69 pppp13-{F}(V0,V1) | p2-{T}(V1)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #135: input, references = 4, size of lhs = 1:
% 12.37/12.69 pppp13-{F}(V0,V1) | EXISTS V2: pppp12-{T}(V2,V1)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #136: input, references = 3, size of lhs = 1:
% 12.37/12.69 pppp13-{F}(V0,V1) | r1-{T}(V0,V1)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #137: input, references = 4, size of lhs = 2:
% 12.37/12.69 pppp12-{F}(V0,V1), p2-{F}(V0) | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #138: input, references = 4, size of lhs = 1:
% 12.37/12.69 pppp12-{F}(V0,V1) | r1-{T}(V1,V0)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #139: input, references = 4, size of lhs = 4:
% 12.37/12.69 pppp11-{F}(V0,V1), r1-{F}(V1,V2), r1-{F}(V2,V3), p2-{F}(V2) | p2-{T}(V3)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #140: input, references = 3, size of lhs = 2:
% 12.37/12.69 pppp11-{F}(V0,V1), p2-{F}(V1) | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #141: input, references = 4, size of lhs = 1:
% 12.37/12.69 pppp11-{F}(V0,V1) | r1-{T}(V0,V1)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #142: input, references = 4, size of lhs = 1:
% 12.37/12.69 pppp10-{F}(V0,V1) | p2-{T}(V1)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #143: input, references = 4, size of lhs = 1:
% 12.37/12.69 pppp10-{F}(V0,V1) | EXISTS V2: pppp9-{T}(V2,V1)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #144: input, references = 5, size of lhs = 1:
% 12.37/12.69 pppp10-{F}(V0,V1) | r1-{T}(V0,V1)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #145: input, references = 4, size of lhs = 2:
% 12.37/12.69 pppp9-{F}(V0,V1), p2-{F}(V0) | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #146: input, references = 5, size of lhs = 1:
% 12.37/12.69 pppp9-{F}(V0,V1) | r1-{T}(V1,V0)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #147: input, references = 3, size of lhs = 1:
% 12.37/12.69 pppp8-{F}(V0,V1) | p1-{T}(V0)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #148: input, references = 3, size of lhs = 1:
% 12.37/12.69 pppp8-{F}(V0,V1) | EXISTS V2: pppp7-{T}(V0,V2)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #149: input, references = 3, size of lhs = 1:
% 12.37/12.69 pppp8-{F}(V0,V1) | r1-{T}(V1,V0)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #150: input, references = 11, size of lhs = 2:
% 12.37/12.69 pppp7-{F}(V0,V1), p1-{F}(V1) | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #151: input, references = 3, size of lhs = 1:
% 12.37/12.69 pppp7-{F}(V0,V1) | r1-{T}(V0,V1)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #152: input, references = 3, size of lhs = 2:
% 12.37/12.69 pppp6-{F}(V0,V1), p1-{F}(V1) | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #153: input, references = 3, size of lhs = 1:
% 12.37/12.69 pppp6-{F}(V0,V1) | r1-{T}(V0,V1)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #154: input, references = 6, size of lhs = 1:
% 12.37/12.69 pppp5-{F}(V0,V1) | p2-{T}(V0)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #155: input, references = 6, size of lhs = 1:
% 12.37/12.69 pppp5-{F}(V0,V1) | EXISTS V2: pppp4-{T}(V0,V2)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #156: input, references = 6, size of lhs = 1:
% 12.37/12.69 pppp5-{F}(V0,V1) | r1-{T}(V1,V0)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #157: input, references = 6, size of lhs = 2:
% 12.37/12.69 pppp4-{F}(V0,V1), p2-{F}(V1) | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #158: input, references = 6, size of lhs = 1:
% 12.37/12.69 pppp4-{F}(V0,V1) | r1-{T}(V0,V1)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #159: input, references = 3, size of lhs = 2:
% 12.37/12.69 pppp3-{F}(V0,V1), p2-{F}(V1) | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #160: input, references = 4, size of lhs = 1:
% 12.37/12.69 pppp3-{F}(V0,V1) | r1-{T}(V0,V1)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #161: input, references = 3, size of lhs = 1:
% 12.37/12.69 pppp2-{F}(V0,V1) | p3-{T}(V0)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #162: input, references = 4, size of lhs = 1:
% 12.37/12.69 pppp2-{F}(V0,V1) | EXISTS V2: pppp1-{T}(V0,V2)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #163: input, references = 3, size of lhs = 1:
% 12.37/12.69 pppp2-{F}(V0,V1) | r1-{T}(V1,V0)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #164: input, references = 3, size of lhs = 2:
% 12.37/12.69 pppp1-{F}(V0,V1), p3-{F}(V1) | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #165: input, references = 4, size of lhs = 1:
% 12.37/12.69 pppp1-{F}(V0,V1) | r1-{T}(V0,V1)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #166: input, references = 3, size of lhs = 2:
% 12.37/12.69 pppp0-{F}(V0,V1), p3-{F}(V1) | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #167: input, references = 3, size of lhs = 1:
% 12.37/12.69 pppp0-{F}(V0,V1) | r1-{T}(V0,V1)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 number of initial rules = 168
% 12.37/12.69
% 12.37/12.69 Simplifiers:
% 12.37/12.69 #168: unsound, references = 3, size of lhs = 3:
% 12.37/12.69 pppp0-{F}(V0,V1), pppp0-{F}(V0,V3), V1 == V3 | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #169: unsound, references = 3, size of lhs = 3:
% 12.37/12.69 pppp0-{F}(V0,V1), pppp0-{F}(V2,V3), V0 == V2 | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #170: unsound, references = 3, size of lhs = 3:
% 12.37/12.69 pppp1-{F}(V0,V1), pppp1-{F}(V0,V3), V1 == V3 | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #171: unsound, references = 3, size of lhs = 3:
% 12.37/12.69 pppp2-{F}(V0,V1), pppp2-{F}(V2,V1), V0 == V2 | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #172: unsound, references = 3, size of lhs = 3:
% 12.37/12.69 pppp3-{F}(V0,V1), pppp3-{F}(V0,V3), V1 == V3 | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #173: unsound, references = 3, size of lhs = 3:
% 12.37/12.69 pppp3-{F}(V0,V1), pppp3-{F}(V2,V3), V0 == V2 | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #174: unsound, references = 3, size of lhs = 3:
% 12.37/12.69 pppp4-{F}(V0,V1), pppp4-{F}(V0,V3), V1 == V3 | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #175: unsound, references = 3, size of lhs = 3:
% 12.37/12.69 pppp5-{F}(V0,V1), pppp5-{F}(V2,V1), V0 == V2 | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #176: unsound, references = 3, size of lhs = 3:
% 12.37/12.69 pppp6-{F}(V0,V1), pppp6-{F}(V0,V3), V1 == V3 | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #177: unsound, references = 3, size of lhs = 3:
% 12.37/12.69 pppp6-{F}(V0,V1), pppp6-{F}(V2,V3), V0 == V2 | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #178: unsound, references = 3, size of lhs = 3:
% 12.37/12.69 pppp7-{F}(V0,V1), pppp7-{F}(V0,V3), V1 == V3 | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #179: unsound, references = 3, size of lhs = 3:
% 12.37/12.69 pppp8-{F}(V0,V1), pppp8-{F}(V2,V1), V0 == V2 | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #180: unsound, references = 3, size of lhs = 3:
% 12.37/12.69 pppp9-{F}(V0,V1), pppp9-{F}(V2,V1), V0 == V2 | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #181: unsound, references = 3, size of lhs = 3:
% 12.37/12.69 pppp10-{F}(V0,V1), pppp10-{F}(V0,V3), V1 == V3 | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #182: unsound, references = 3, size of lhs = 3:
% 12.37/12.69 pppp11-{F}(V0,V1), pppp11-{F}(V0,V3), V1 == V3 | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #183: unsound, references = 3, size of lhs = 3:
% 12.37/12.69 pppp11-{F}(V0,V1), pppp11-{F}(V2,V3), V0 == V2 | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #184: unsound, references = 3, size of lhs = 3:
% 12.37/12.69 pppp12-{F}(V0,V1), pppp12-{F}(V2,V1), V0 == V2 | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #185: unsound, references = 3, size of lhs = 3:
% 12.37/12.69 pppp13-{F}(V0,V1), pppp13-{F}(V0,V3), V1 == V3 | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #186: unsound, references = 3, size of lhs = 3:
% 12.37/12.69 pppp13-{F}(V0,V1), pppp13-{F}(V2,V3), V0 == V2 | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #187: unsound, references = 3, size of lhs = 3:
% 12.37/12.69 pppp14-{F}(V0,V1), pppp14-{F}(V0,V3), V1 == V3 | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #188: unsound, references = 3, size of lhs = 3:
% 12.37/12.69 pppp15-{F}(V0,V1), pppp15-{F}(V2,V1), V0 == V2 | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #189: unsound, references = 3, size of lhs = 3:
% 12.37/12.69 pppp16-{F}(V0,V1), pppp16-{F}(V2,V1), V0 == V2 | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #190: unsound, references = 3, size of lhs = 3:
% 12.37/12.69 pppp17-{F}(V0,V1), pppp17-{F}(V0,V3), V1 == V3 | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #191: unsound, references = 3, size of lhs = 3:
% 12.37/12.69 pppp18-{F}(V0,V1), pppp18-{F}(V0,V3), V1 == V3 | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #192: unsound, references = 3, size of lhs = 3:
% 12.37/12.69 pppp19-{F}(V0,V1), pppp19-{F}(V2,V1), V0 == V2 | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #193: unsound, references = 3, size of lhs = 3:
% 12.37/12.69 pppp20-{F}(V0,V1), pppp20-{F}(V2,V1), V0 == V2 | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #194: unsound, references = 3, size of lhs = 3:
% 12.37/12.69 pppp21-{F}(V0,V1), pppp21-{F}(V0,V3), V1 == V3 | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #195: unsound, references = 3, size of lhs = 3:
% 12.37/12.69 pppp22-{F}(V0,V1), pppp22-{F}(V2,V1), V0 == V2 | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #196: unsound, references = 3, size of lhs = 3:
% 12.37/12.69 pppp23-{F}(V0,V1), pppp23-{F}(V2,V1), V0 == V2 | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #197: unsound, references = 3, size of lhs = 3:
% 12.37/12.69 pppp24-{F}(V0,V1), pppp24-{F}(V0,V3), V1 == V3 | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #198: unsound, references = 3, size of lhs = 3:
% 12.37/12.69 pppp25-{F}(V0,V1), pppp25-{F}(V0,V3), V1 == V3 | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #199: unsound, references = 3, size of lhs = 3:
% 12.37/12.69 pppp26-{F}(V0,V1), pppp26-{F}(V2,V1), V0 == V2 | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #200: unsound, references = 3, size of lhs = 3:
% 12.37/12.69 pppp28-{F}(V0,V1), pppp28-{F}(V0,V3), V1 == V3 | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #201: unsound, references = 3, size of lhs = 3:
% 12.37/12.69 pppp28-{F}(V0,V1), pppp28-{F}(V2,V3), V0 == V2 | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #202: unsound, references = 3, size of lhs = 3:
% 12.37/12.69 pppp29-{F}(V0,V1), pppp29-{F}(V0,V3), V1 == V3 | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #203: unsound, references = 3, size of lhs = 3:
% 12.37/12.69 pppp29-{F}(V0,V1), pppp29-{F}(V2,V3), V0 == V2 | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #204: unsound, references = 3, size of lhs = 3:
% 12.37/12.69 pppp30-{F}(V0,V1), pppp30-{F}(V0,V3), V1 == V3 | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #205: unsound, references = 3, size of lhs = 3:
% 12.37/12.69 pppp31-{F}(V0,V1), pppp31-{F}(V0,V3), V1 == V3 | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #206: unsound, references = 3, size of lhs = 3:
% 12.37/12.69 pppp33-{F}(V0,V1), pppp33-{F}(V0,V3), V1 == V3 | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #207: unsound, references = 3, size of lhs = 3:
% 12.37/12.69 pppp33-{F}(V0,V1), pppp33-{F}(V2,V3), V0 == V2 | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #208: unsound, references = 3, size of lhs = 3:
% 12.37/12.69 pppp34-{F}(V0,V1), pppp34-{F}(V0,V3), V1 == V3 | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #209: unsound, references = 3, size of lhs = 3:
% 12.37/12.69 pppp34-{F}(V0,V1), pppp34-{F}(V2,V3), V0 == V2 | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #210: unsound, references = 3, size of lhs = 3:
% 12.37/12.69 pppp35-{F}(V0,V1), pppp35-{F}(V0,V3), V1 == V3 | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #211: unsound, references = 3, size of lhs = 3:
% 12.37/12.69 pppp36-{F}(V0,V1), pppp36-{F}(V0,V3), V1 == V3 | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #212: unsound, references = 3, size of lhs = 3:
% 12.37/12.69 pppp37-{F}(V0,V1), pppp37-{F}(V0,V3), V1 == V3 | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #213: unsound, references = 3, size of lhs = 3:
% 12.37/12.69 pppp37-{F}(V0,V1), pppp37-{F}(V2,V3), V0 == V2 | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #214: unsound, references = 3, size of lhs = 3:
% 12.37/12.69 pppp38-{F}(V0,V1), pppp38-{F}(V0,V3), V1 == V3 | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #215: unsound, references = 3, size of lhs = 3:
% 12.37/12.69 pppp38-{F}(V0,V1), pppp38-{F}(V2,V3), V0 == V2 | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #216: unsound, references = 3, size of lhs = 3:
% 12.37/12.69 pppp39-{F}(V0,V1), pppp39-{F}(V0,V3), V1 == V3 | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #217: unsound, references = 3, size of lhs = 3:
% 12.37/12.69 pppp40-{F}(V0,V1), pppp40-{F}(V0,V3), V1 == V3 | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #218: unsound, references = 3, size of lhs = 3:
% 12.37/12.69 pppp41-{F}(V0,V1), pppp41-{F}(V0,V3), V1 == V3 | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #219: unsound, references = 3, size of lhs = 3:
% 12.37/12.69 pppp41-{F}(V0,V1), pppp41-{F}(V2,V3), V0 == V2 | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #220: unsound, references = 3, size of lhs = 3:
% 12.37/12.69 pppp42-{F}(V0,V1), pppp42-{F}(V0,V3), V1 == V3 | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #221: unsound, references = 3, size of lhs = 3:
% 12.37/12.69 pppp42-{F}(V0,V1), pppp42-{F}(V2,V3), V0 == V2 | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #222: unsound, references = 3, size of lhs = 3:
% 12.37/12.69 pppp43-{F}(V0,V1), pppp43-{F}(V0,V3), V1 == V3 | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #223: unsound, references = 3, size of lhs = 3:
% 12.37/12.69 pppp44-{F}(V0,V1), pppp44-{F}(V0,V3), V1 == V3 | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #224: unsound, references = 3, size of lhs = 3:
% 12.37/12.69 pppp45-{F}(V0,V1), pppp45-{F}(V0,V3), V1 == V3 | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #225: unsound, references = 3, size of lhs = 3:
% 12.37/12.69 pppp45-{F}(V0,V1), pppp45-{F}(V2,V3), V0 == V2 | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #226: unsound, references = 3, size of lhs = 3:
% 12.37/12.69 pppp46-{F}(V0,V1), pppp46-{F}(V0,V3), V1 == V3 | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #227: unsound, references = 3, size of lhs = 3:
% 12.37/12.69 pppp46-{F}(V0,V1), pppp46-{F}(V2,V3), V0 == V2 | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #228: unsound, references = 3, size of lhs = 3:
% 12.37/12.69 pppp47-{F}(V0,V1), pppp47-{F}(V2,V1), V0 == V2 | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #229: unsound, references = 3, size of lhs = 3:
% 12.37/12.69 pppp48-{F}(V0), pppp48-{F}(V1), V0 == V1 | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #230: unsound, references = 3, size of lhs = 3:
% 12.37/12.69 pppp49-{F}(V0), pppp49-{F}(V1), V0 == V1 | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #231: unsound, references = 3, size of lhs = 3:
% 12.37/12.69 pppp51-{F}(V0), pppp51-{F}(V1), V0 == V1 | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #232: unsound, references = 3, size of lhs = 3:
% 12.37/12.69 pppp52-{F}(V0), pppp52-{F}(V1), V0 == V1 | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #233: unsound, references = 3, size of lhs = 3:
% 12.37/12.69 pppp53-{F}(V0), pppp53-{F}(V1), V0 == V1 | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #234: unsound, references = 3, size of lhs = 3:
% 12.37/12.69 pppp54-{F}(V0), pppp54-{F}(V1), V0 == V1 | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #235: unsound, references = 3, size of lhs = 3:
% 12.37/12.69 pppp55-{F}(V0), pppp55-{F}(V1), V0 == V1 | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #236: unsound, references = 3, size of lhs = 3:
% 12.37/12.69 pppp56-{F}(V0), pppp56-{F}(V1), V0 == V1 | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #237: unsound, references = 3, size of lhs = 3:
% 12.37/12.69 pppp58-{F}(V0), pppp58-{F}(V1), V0 == V1 | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #238: unsound, references = 3, size of lhs = 3:
% 12.37/12.69 pppp59-{F}(V0), pppp59-{F}(V1), V0 == V1 | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 number of simplifiers = 71
% 12.37/12.69
% 12.37/12.69 Learnt:
% 12.37/12.69 #241: disj( #4, input ), references = 1, size of lhs = 3:
% 12.37/12.69 pppp48-{F}(V0), r1-{F}(V0,V1), pppp6-{F}(V2,V0) | pppp51-{T}(V0)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #244: disj( #2, input ), references = 2, size of lhs = 3:
% 12.37/12.69 pppp48-{F}(V0), r1-{F}(V0,V1), pppp3-{F}(V2,V1) | pppp50-{T}(V1)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #247: disj( #19, input ), references = 1, size of lhs = 3:
% 12.37/12.69 pppp48-{F}(V0), r1-{F}(V0,V1), pppp6-{F}(V2,V1) | pppp60-{T}(V1)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #250: disj( #22, input ), references = 1, size of lhs = 3:
% 12.37/12.69 pppp48-{F}(V0), r1-{F}(V0,V1), pppp3-{F}(V2,V1) | pppp61-{T}(V1)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #257: exists( #135, #255 ), references = 1, size of lhs = 4:
% 12.37/12.69 p2-{F}(V0), pppp13-{F}(V1,V0), r1-{F}(V2,V0), pppp47-{F}(V2,V3) | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #281: mergings( V5 == V0, V3 == V1; #276 ), references = 1, size of lhs = 5:
% 12.37/12.69 p2-{F}(V0), r1-{F}(V0,V1), r1-{F}(V1,V0), r1-{F}(V1,V2), pppp41-{F}(V3,V1) | p1-{T}(V1)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #282: disj( #44, input ), references = 1, size of lhs = 6:
% 12.37/12.69 p2-{F}(V0), r1-{F}(V0,V1), r1-{F}(V1,V2), pppp12-{F}(V1,V3), r1-{F}(V4,V0), pppp41-{F}(V5,V4) | p1-{T}(V1)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #283: disj( #44, input ), references = 1, size of lhs = 6:
% 12.37/12.69 p2-{F}(V0), r1-{F}(V0,V1), r1-{F}(V1,V2), pppp3-{F}(V3,V1), r1-{F}(V4,V0), pppp41-{F}(V5,V4) | p1-{T}(V1)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #293: disj( #2, input ), references = 1, size of lhs = 3:
% 12.37/12.69 pppp48-{F}(V0), r1-{F}(V0,V1), pppp47-{F}(V1,V2) | pppp50-{T}(V1)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #294: disj( #2, input ), references = 1, size of lhs = 3:
% 12.37/12.69 pppp48-{F}(V0), r1-{F}(V0,V1), pppp41-{F}(V2,V1) | pppp50-{T}(V1)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #297: disj( #19, input ), references = 1, size of lhs = 3:
% 12.37/12.69 pppp48-{F}(V0), r1-{F}(V0,V1), pppp45-{F}(V2,V1) | pppp60-{T}(V1)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #309: exists( #3, #305 ), references = 1, size of lhs = 6:
% 12.37/12.69 pppp50-{F}(V0), p1-{F}(V1), r1-{F}(V1,V0), pppp7-{F}(V2,V0), r1-{F}(V3,V1), pppp45-{F}(V4,V3) | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #310: exists( #3, #306 ), references = 1, size of lhs = 6:
% 12.37/12.69 pppp50-{F}(V0), p1-{F}(V1), r1-{F}(V1,V0), pppp37-{F}(V2,V0), r1-{F}(V3,V1), pppp45-{F}(V4,V3) | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #319: exists( #162, #317 ), references = 1, size of lhs = 6:
% 12.37/12.69 p1-{F}(V0), r1-{F}(V0,V1), pppp2-{F}(V1,V2), pppp7-{F}(V3,V1), r1-{F}(V4,V0), pppp45-{F}(V5,V4) | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #331: mergings( V0 == V5, V1 == V3, V5 == V6; #324 ), references = 1, size of lhs = 4:
% 12.37/12.69 pppp41-{F}(V0,V1), r1-{F}(V1,V2), r1-{F}(V2,V1), r1-{F}(V1,V3) | pppp64-{T}(V2)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #349: mergings( V0 == V4; #346 ), references = 1, size of lhs = 5:
% 12.37/12.69 p1-{F}(V0), r1-{F}(V0,V1), pppp37-{F}(V2,V1), r1-{F}(V3,V0), pppp45-{F}(V4,V3) | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #354: disj( #22, input ), references = 1, size of lhs = 3:
% 12.37/12.69 pppp48-{F}(V0), r1-{F}(V0,V1), pppp47-{F}(V1,V2) | pppp61-{T}(V1)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #355: disj( #22, input ), references = 1, size of lhs = 3:
% 12.37/12.69 pppp48-{F}(V0), r1-{F}(V0,V1), pppp12-{F}(V1,V2) | pppp61-{T}(V1)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #376: exists( #155, #374 ), references = 2, size of lhs = 4:
% 12.37/12.69 p2-{F}(V0), pppp5-{F}(V0,V1), r1-{F}(V2,V0), pppp47-{F}(V2,V3) | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #381: exists( #23, #379 ), references = 1, size of lhs = 2:
% 12.37/12.69 pppp61-{F}(V0), pppp47-{F}(V0,V1) | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #385: exists( #3, #383 ), references = 1, size of lhs = 2:
% 12.37/12.69 pppp50-{F}(V0), pppp48-{F}(V0) | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #389: mergings( V0 == V1; #387 ), references = 1, size of lhs = 2:
% 12.37/12.69 pppp48-{F}(V0), r1-{F}(V0,V0) | p2-{T}(V0)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #397: mergings( V0 == V5, V1 == V3; #393 ), references = 1, size of lhs = 4:
% 12.37/12.69 pppp45-{F}(V0,V1), r1-{F}(V1,V2), r1-{F}(V2,V1), r1-{F}(V1,V3) | pppp63-{T}(V2)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #398: disj( #32, input ), references = 1, size of lhs = 5:
% 12.37/12.69 pppp45-{F}(V0,V1), r1-{F}(V1,V2), r1-{F}(V2,V3), r1-{F}(V3,V4), pppp6-{F}(V5,V3) | pppp63-{T}(V2)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #410: disj( #92, input ), references = 1, size of lhs = 5:
% 12.37/12.69 p2-{F}(V0), r1-{F}(V0,V1), pppp3-{F}(V2,V1), r1-{F}(V3,V0), pppp28-{F}(V4,V3) | pppp72-{T}(V3)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #411: disj( #92, input ), references = 1, size of lhs = 5:
% 12.37/12.69 p2-{F}(V0), r1-{F}(V0,V1), pppp12-{F}(V1,V2), r1-{F}(V3,V0), pppp28-{F}(V4,V3) | pppp72-{T}(V3)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #412: disj( #92, input ), references = 1, size of lhs = 5:
% 12.37/12.69 p2-{F}(V0), r1-{F}(V0,V1), pppp4-{F}(V2,V1), r1-{F}(V3,V0), pppp28-{F}(V4,V3) | pppp72-{T}(V3)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #428: mergings( V6 == V5, V4 == V2; #417 ), references = 1, size of lhs = 6:
% 12.37/12.69 p2-{F}(V0), r1-{F}(V0,V1), pppp3-{F}(V2,V1), r1-{F}(V3,V0), r1-{F}(V3,V1), pppp28-{F}(V4,V3) | pppp70-{T}(V1)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #429: disj( #88, input, input ), references = 1, size of lhs = 7:
% 12.37/12.69 p2-{F}(V0), r1-{F}(V0,V1), pppp12-{F}(V1,V2), r1-{F}(V3,V0), pppp28-{F}(V4,V3), r1-{F}(V3,V5), pppp3-{F}(V6,V5) | pppp70-{T}(V5)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #430: disj( #88, input, input ), references = 1, size of lhs = 7:
% 12.37/12.69 p2-{F}(V0), r1-{F}(V0,V1), pppp3-{F}(V2,V1), r1-{F}(V3,V0), pppp28-{F}(V4,V3), r1-{F}(V3,V5), pppp12-{F}(V5,V6) | pppp70-{T}(V5)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #443: disj( #96, input ), references = 9, size of lhs = 3:
% 12.37/12.69 pppp27-{F}(V0), r1-{F}(V0,V1), pppp47-{F}(V1,V2) | pppp73-{T}(V1)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #461: exists( #97, #458 ), references = 14, size of lhs = 6:
% 12.37/12.69 pppp73-{F}(V0), p1-{F}(V1), r1-{F}(V1,V0), pppp7-{F}(V2,V0), r1-{F}(V3,V1), pppp45-{F}(V4,V3) | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #466: disj( #84, #442+#460, input ), references = 1, size of lhs = 13:
% 12.37/12.69 p2-{F}(V0), r1-{F}(V0,V1), p1-{F}(V2), r1-{F}(V2,V3), pppp47-{F}(V3,V4), pppp7-{F}(V5,V3), pppp3-{F}(V6,V1), r1-{F}(V7,V0), r1-{F}(V7,V3), r1-{F}(V8,V7), pppp28-{F}(V9,V8), r1-{F}(V10,V2), pppp45-{F}(V11,V10) | pppp68-{T}(V7)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #467: disj( #84, #442+#460, input ), references = 1, size of lhs = 13:
% 12.37/12.69 p2-{F}(V0), r1-{F}(V0,V1), p1-{F}(V2), r1-{F}(V2,V3), pppp47-{F}(V3,V4), pppp7-{F}(V5,V3), pppp12-{F}(V1,V6), r1-{F}(V7,V0), r1-{F}(V7,V3), r1-{F}(V8,V7), pppp28-{F}(V9,V8), r1-{F}(V10,V2), pppp45-{F}(V11,V10) | pppp68-{T}(V7)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #468: disj( #84, #442+#460, input ), references = 1, size of lhs = 13:
% 12.37/12.69 p2-{F}(V0), r1-{F}(V0,V1), p1-{F}(V2), r1-{F}(V2,V3), pppp47-{F}(V3,V4), pppp7-{F}(V5,V3), pppp4-{F}(V6,V1), r1-{F}(V7,V0), r1-{F}(V7,V3), r1-{F}(V8,V7), pppp28-{F}(V9,V8), r1-{F}(V10,V2), pppp45-{F}(V11,V10) | pppp68-{T}(V7)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #475: disj( #80, #443+#461, input ), references = 1, size of lhs = 14:
% 12.37/12.69 p2-{F}(V0), r1-{F}(V0,V1), p1-{F}(V2), r1-{F}(V2,V3), pppp47-{F}(V3,V4), pppp7-{F}(V5,V3), r1-{F}(V6,V0), r1-{F}(V6,V3), r1-{F}(V6,V7), pppp47-{F}(V7,V8), r1-{F}(V9,V6), pppp28-{F}(V10,V9), r1-{F}(V11,V2), pppp45-{F}(V12,V11) | pppp66-{T}(V7), p2-{T}(V1)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #489: mergings( V13 == V12, V5 == V3; #478 ), references = 1, size of lhs = 14:
% 12.37/12.69 p2-{F}(V0), r1-{F}(V0,V1), p1-{F}(V2), r1-{F}(V2,V3), pppp47-{F}(V3,V4), pppp7-{F}(V5,V3), pppp3-{F}(V6,V1), r1-{F}(V7,V0), r1-{F}(V7,V3), r1-{F}(V7,V1), r1-{F}(V8,V7), pppp28-{F}(V9,V8), r1-{F}(V10,V2), pppp45-{F}(V11,V10) | pppp66-{T}(V1)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #490: disj( #80, #443+#461, input, input ), references = 1, size of lhs = 15:
% 12.37/12.69 p2-{F}(V0), r1-{F}(V0,V1), p1-{F}(V2), r1-{F}(V2,V3), pppp47-{F}(V3,V4), pppp7-{F}(V5,V3), pppp12-{F}(V1,V6), r1-{F}(V7,V0), r1-{F}(V7,V3), r1-{F}(V7,V8), pppp3-{F}(V9,V8), r1-{F}(V10,V7), pppp28-{F}(V11,V10), r1-{F}(V12,V2), pppp45-{F}(V13,V12) | pppp66-{T}(V8)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #491: disj( #80, #443+#461, input, input ), references = 1, size of lhs = 15:
% 12.37/12.69 p2-{F}(V0), r1-{F}(V0,V1), p1-{F}(V2), r1-{F}(V2,V3), pppp47-{F}(V3,V4), pppp7-{F}(V5,V3), pppp3-{F}(V6,V1), r1-{F}(V7,V0), r1-{F}(V7,V3), r1-{F}(V7,V8), pppp12-{F}(V8,V9), r1-{F}(V10,V7), pppp28-{F}(V11,V10), r1-{F}(V12,V2), pppp45-{F}(V13,V12) | pppp66-{T}(V8)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #497: disj( #82, #443+#461, input ), references = 2, size of lhs = 12:
% 12.37/12.69 p2-{F}(V0), r1-{F}(V0,V1), r1-{F}(V0,V2), pppp47-{F}(V2,V3), p1-{F}(V4), r1-{F}(V4,V2), pppp7-{F}(V5,V2), pppp47-{F}(V1,V6), r1-{F}(V7,V0), pppp28-{F}(V8,V7), r1-{F}(V9,V4), pppp45-{F}(V10,V9) | pppp67-{T}(V1)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #500: disj( #86, #443+#461 ), references = 1, size of lhs = 10:
% 12.37/12.69 p2-{F}(V0), r1-{F}(V0,V1), pppp47-{F}(V1,V2), p1-{F}(V3), r1-{F}(V3,V1), pppp7-{F}(V4,V1), r1-{F}(V5,V0), pppp28-{F}(V6,V5), r1-{F}(V7,V3), pppp45-{F}(V8,V7) | pppp69-{T}(V0)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #503: disj( #80, #443+#461, input ), references = 1, size of lhs = 14:
% 12.37/12.69 p2-{F}(V0), r1-{F}(V0,V1), p1-{F}(V2), r1-{F}(V2,V3), pppp47-{F}(V3,V4), pppp7-{F}(V5,V3), r1-{F}(V6,V0), r1-{F}(V6,V3), r1-{F}(V6,V7), pppp47-{F}(V7,V8), r1-{F}(V9,V6), pppp28-{F}(V10,V9), r1-{F}(V11,V2), pppp45-{F}(V12,V11) | pppp66-{T}(V7), p2-{T}(V1)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #518: exists( #83, #516 ), references = 2, size of lhs = 6:
% 12.37/12.69 pppp67-{F}(V0), p1-{F}(V1), r1-{F}(V1,V0), pppp7-{F}(V2,V0), r1-{F}(V3,V1), pppp45-{F}(V4,V3) | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #522: disj( #90, input ), references = 2, size of lhs = 4:
% 12.37/12.69 p2-{F}(V0), pppp28-{F}(V1,V0), r1-{F}(V0,V2), pppp47-{F}(V2,V3) | pppp71-{T}(V2)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #532: exists( #91, #530 ), references = 1, size of lhs = 6:
% 12.37/12.69 pppp71-{F}(V0), p1-{F}(V1), r1-{F}(V1,V0), pppp7-{F}(V2,V0), r1-{F}(V3,V1), pppp45-{F}(V4,V3) | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #564: mergings( V0 == V8, V1 == V7; #560 ), references = 1, size of lhs = 8:
% 12.37/12.69 pppp50-{F}(V0), pppp7-{F}(V1,V0), r1-{F}(V2,V0), r1-{F}(V2,V3), r1-{F}(V4,V2), r1-{F}(V5,V4), r1-{F}(V5,V2), pppp45-{F}(V6,V5) | pppp63-{T}(V4)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #567: mergings( V0 == V9, V1 == V8; #561 ), references = 1, size of lhs = 8:
% 12.37/12.69 pppp7-{F}(V0,V1), pppp2-{F}(V1,V2), r1-{F}(V3,V1), r1-{F}(V3,V4), r1-{F}(V5,V3), r1-{F}(V6,V5), r1-{F}(V6,V3), pppp45-{F}(V7,V6) | pppp63-{T}(V5)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #576: disj( #88, input, input ), references = 1, size of lhs = 7:
% 12.37/12.69 p2-{F}(V0), r1-{F}(V0,V1), pppp47-{F}(V1,V2), r1-{F}(V3,V0), pppp28-{F}(V4,V3), r1-{F}(V3,V5), pppp47-{F}(V5,V6) | pppp70-{T}(V5)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #577: disj( #88, input, input ), references = 1, size of lhs = 7:
% 12.37/12.69 p2-{F}(V0), r1-{F}(V0,V1), pppp14-{F}(V2,V1), r1-{F}(V3,V0), pppp28-{F}(V4,V3), r1-{F}(V3,V5), pppp47-{F}(V5,V6) | pppp70-{T}(V5)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #578: disj( #88, input, input ), references = 1, size of lhs = 7:
% 12.37/12.69 p2-{F}(V0), r1-{F}(V0,V1), pppp47-{F}(V1,V2), r1-{F}(V3,V0), pppp28-{F}(V4,V3), r1-{F}(V3,V5), pppp14-{F}(V6,V5) | pppp70-{T}(V5)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #593: disj( #92, input ), references = 1, size of lhs = 5:
% 12.37/12.69 p2-{F}(V0), r1-{F}(V0,V1), pppp47-{F}(V1,V2), r1-{F}(V3,V0), pppp28-{F}(V4,V3) | pppp72-{T}(V3)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #594: disj( #92, input ), references = 1, size of lhs = 5:
% 12.37/12.69 p2-{F}(V0), r1-{F}(V0,V1), pppp14-{F}(V2,V1), r1-{F}(V3,V0), pppp28-{F}(V4,V3) | pppp72-{T}(V3)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #612: exists( #125, #609 ), references = 2, size of lhs = 4:
% 12.37/12.69 p2-{F}(V0), pppp17-{F}(V1,V0), r1-{F}(V2,V0), pppp47-{F}(V2,V3) | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #616: exists( #91, #614 ), references = 1, size of lhs = 2:
% 12.37/12.69 pppp71-{F}(V0), pppp47-{F}(V0,V1) | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #620: exists( #3, #618 ), references = 1, size of lhs = 3:
% 12.37/12.69 pppp50-{F}(V0), p2-{F}(V0), pppp28-{F}(V1,V0) | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #622: disj( #22, exists( #3, #618 ) ), references = 1, size of lhs = 4:
% 12.37/12.69 pppp48-{F}(V0), r1-{F}(V0,V1), pppp50-{F}(V1), pppp28-{F}(V2,V1) | pppp61-{T}(V1)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #640: mergings( V6 == V0, V4 == V1; #637 ), references = 1, size of lhs = 7:
% 12.37/12.69 p2-{F}(V0), r1-{F}(V0,V1), pppp50-{F}(V1), r1-{F}(V1,V0), pppp28-{F}(V2,V1), r1-{F}(V1,V3), pppp47-{F}(V3,V4) | pppp70-{T}(V3)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #651: exists( #89, #649 ), references = 1, size of lhs = 2:
% 12.37/12.69 pppp70-{F}(V0), pppp47-{F}(V0,V1) | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #665: disj( #88, input, exists( #89, #649 ) ), references = 1, size of lhs = 7:
% 12.37/12.69 p2-{F}(V0), r1-{F}(V0,V1), r1-{F}(V2,V0), pppp28-{F}(V3,V2), r1-{F}(V2,V4), pppp47-{F}(V4,V5), pppp47-{F}(V4,V6) | p2-{T}(V1)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #669: exists( #155, #667 ), references = 1, size of lhs = 7:
% 12.37/12.69 p2-{F}(V0), pppp5-{F}(V0,V1), r1-{F}(V2,V0), pppp28-{F}(V3,V2), r1-{F}(V2,V4), pppp47-{F}(V4,V5), pppp47-{F}(V4,V6) | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #673: exists( #23, #671 ), references = 1, size of lhs = 5:
% 12.37/12.69 pppp61-{F}(V0), pppp28-{F}(V1,V0), r1-{F}(V0,V2), pppp47-{F}(V2,V3), pppp47-{F}(V2,V4) | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #676: exists( #3, #674 ), references = 1, size of lhs = 3:
% 12.37/12.69 pppp50-{F}(V0), pppp61-{F}(V0), pppp28-{F}(V1,V0) | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #681: mergings( V3 == V4, V0 == V2; #678 ), references = 1, size of lhs = 3:
% 12.37/12.69 pppp48-{F}(V0), r1-{F}(V0,V1), pppp28-{F}(V2,V1) | p2-{T}(V1)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #704: disj( #88, input, input ), references = 1, size of lhs = 7:
% 12.37/12.69 p2-{F}(V0), r1-{F}(V0,V1), pppp14-{F}(V2,V1), r1-{F}(V3,V0), pppp28-{F}(V4,V3), r1-{F}(V3,V5), pppp14-{F}(V6,V5) | pppp70-{T}(V5)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #728: disj( #80, input, input ), references = 1, size of lhs = 8:
% 12.37/12.69 p2-{F}(V0), r1-{F}(V0,V1), pppp14-{F}(V2,V1), r1-{F}(V3,V0), r1-{F}(V3,V4), pppp14-{F}(V5,V4), r1-{F}(V6,V3), pppp28-{F}(V7,V6) | pppp27-{T}(V3), pppp66-{T}(V4)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #740: disj( #90, input ), references = 1, size of lhs = 4:
% 12.37/12.69 p2-{F}(V0), pppp28-{F}(V1,V0), r1-{F}(V0,V2), pppp14-{F}(V3,V2) | pppp71-{T}(V2)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #754: disj( #96, input ), references = 10, size of lhs = 3:
% 12.37/12.69 pppp27-{F}(V0), r1-{F}(V0,V1), pppp14-{F}(V2,V1) | pppp73-{T}(V1)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #795: exists( #125, #792 ), references = 2, size of lhs = 4:
% 12.37/12.69 p2-{F}(V0), pppp17-{F}(V1,V0), r1-{F}(V2,V0), pppp14-{F}(V3,V2) | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #799: exists( #89, #797 ), references = 1, size of lhs = 2:
% 12.37/12.69 pppp70-{F}(V0), pppp14-{F}(V1,V0) | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #803: exists( #129, #801 ), references = 1, size of lhs = 4:
% 12.37/12.69 p2-{F}(V0), r1-{F}(V0,V0), pppp15-{F}(V0,V1), pppp28-{F}(V2,V0) | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #812: exists( #91, #809 ), references = 1, size of lhs = 2:
% 12.37/12.69 pppp71-{F}(V0), pppp14-{F}(V1,V0) | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #824: mergings( V0 == V21, V1 == V20, V11 == V23, V10 == V22, V23 == V25, V22 == V24; #817 ), references = 1, size of lhs = 26:
% 12.37/12.69 p2-{F}(V0), r1-{F}(V0,V1), p1-{F}(V2), r1-{F}(V2,V3), pppp14-{F}(V4,V3), pppp7-{F}(V5,V3), r1-{F}(V1,V6), r1-{F}(V1,V7), pppp47-{F}(V7,V8), p1-{F}(V9), r1-{F}(V9,V7), pppp7-{F}(V10,V7), pppp47-{F}(V6,V11), p1-{F}(V12), r1-{F}(V12,V6), pppp7-{F}(V13,V6), r1-{F}(V14,V0), r1-{F}(V14,V3), r1-{F}(V14,V15), r1-{F}(V16,V14), r1-{F}(V16,V1), pppp28-{F}(V17,V16), r1-{F}(V18,V2), r1-{F}(V18,V9), r1-{F}(V18,V12), pppp45-{F}(V19,V18) | p2-{T}(V15), pppp66-{T}(V15)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #832: exists( #81, #830 ), references = 1, size of lhs = 6:
% 12.37/12.69 pppp66-{F}(V0), p1-{F}(V1), r1-{F}(V1,V0), pppp7-{F}(V2,V0), r1-{F}(V3,V1), pppp45-{F}(V4,V3) | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #842: mergings( V17 == V21, V16 == V20, V19 == V23, V18 == V22, V23 == V25, V22 == V24, V25 == V29, V24 == V28; #833 ), references = 1, size of lhs = 30:
% 12.37/12.69 p2-{F}(V0), r1-{F}(V0,V1), p1-{F}(V2), r1-{F}(V2,V3), pppp14-{F}(V4,V3), pppp7-{F}(V5,V3), r1-{F}(V1,V6), r1-{F}(V1,V7), pppp47-{F}(V7,V8), p1-{F}(V9), r1-{F}(V9,V7), pppp7-{F}(V10,V7), pppp47-{F}(V6,V11), p1-{F}(V12), r1-{F}(V12,V6), pppp7-{F}(V13,V6), p1-{F}(V14), r1-{F}(V14,V15), pppp7-{F}(V16,V15), r1-{F}(V17,V0), r1-{F}(V17,V3), r1-{F}(V17,V15), r1-{F}(V18,V17), r1-{F}(V18,V1), pppp28-{F}(V19,V18), r1-{F}(V20,V2), r1-{F}(V20,V9), r1-{F}(V20,V12), r1-{F}(V20,V14), pppp45-{F}(V21,V20) | p2-{T}(V15)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #849: disj( #80, input, exists( #81, #830 ) ), references = 1, size of lhs = 12:
% 12.37/12.69 p2-{F}(V0), r1-{F}(V0,V1), p1-{F}(V2), r1-{F}(V2,V3), pppp14-{F}(V4,V3), pppp7-{F}(V5,V3), r1-{F}(V6,V3), r1-{F}(V6,V0), r1-{F}(V7,V6), pppp28-{F}(V8,V7), r1-{F}(V9,V2), pppp45-{F}(V10,V9) | pppp27-{T}(V6), p2-{T}(V1)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #850: disj( #80, input, exists( #81, #830 ) ), references = 2, size of lhs = 12:
% 12.37/12.69 p2-{F}(V0), r1-{F}(V0,V1), p1-{F}(V2), r1-{F}(V2,V3), pppp47-{F}(V3,V4), pppp7-{F}(V5,V3), r1-{F}(V6,V3), r1-{F}(V6,V0), r1-{F}(V7,V6), pppp28-{F}(V8,V7), r1-{F}(V9,V2), pppp45-{F}(V10,V9) | pppp27-{T}(V6), p2-{T}(V1)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #854: disj( #847, input ), references = 1, size of lhs = 13:
% 12.37/12.69 p2-{F}(V0), r1-{F}(V0,V1), p1-{F}(V2), r1-{F}(V2,V3), pppp14-{F}(V4,V3), pppp7-{F}(V5,V3), pppp3-{F}(V6,V1), r1-{F}(V7,V3), r1-{F}(V7,V0), r1-{F}(V8,V7), pppp28-{F}(V9,V8), r1-{F}(V10,V2), pppp45-{F}(V11,V10) | pppp27-{T}(V7)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #855: disj( #847, input ), references = 1, size of lhs = 13:
% 12.37/12.69 p2-{F}(V0), r1-{F}(V0,V1), p1-{F}(V2), r1-{F}(V2,V3), pppp14-{F}(V4,V3), pppp7-{F}(V5,V3), pppp12-{F}(V1,V6), r1-{F}(V7,V3), r1-{F}(V7,V0), r1-{F}(V8,V7), pppp28-{F}(V9,V8), r1-{F}(V10,V2), pppp45-{F}(V11,V10) | pppp27-{T}(V7)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #856: disj( #847, input ), references = 1, size of lhs = 13:
% 12.37/12.69 p2-{F}(V0), r1-{F}(V0,V1), p1-{F}(V2), r1-{F}(V2,V3), pppp14-{F}(V4,V3), pppp7-{F}(V5,V3), pppp4-{F}(V6,V1), r1-{F}(V7,V3), r1-{F}(V7,V0), r1-{F}(V8,V7), pppp28-{F}(V9,V8), r1-{F}(V10,V2), pppp45-{F}(V11,V10) | pppp27-{T}(V7)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #863: disj( #84, #754+#461, input ), references = 1, size of lhs = 13:
% 12.37/12.69 p2-{F}(V0), r1-{F}(V0,V1), p1-{F}(V2), r1-{F}(V2,V3), pppp14-{F}(V4,V3), pppp7-{F}(V5,V3), pppp14-{F}(V6,V1), r1-{F}(V7,V0), r1-{F}(V7,V3), r1-{F}(V8,V7), pppp28-{F}(V9,V8), r1-{F}(V10,V2), pppp45-{F}(V11,V10) | pppp68-{T}(V7)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #864: disj( #84, #754+#461, input ), references = 1, size of lhs = 13:
% 12.37/12.69 p2-{F}(V0), r1-{F}(V0,V1), p1-{F}(V2), r1-{F}(V2,V3), pppp14-{F}(V4,V3), pppp7-{F}(V5,V3), pppp47-{F}(V1,V6), r1-{F}(V7,V0), r1-{F}(V7,V3), r1-{F}(V8,V7), pppp28-{F}(V9,V8), r1-{F}(V10,V2), pppp45-{F}(V11,V10) | pppp68-{T}(V7)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #869: disj( #80, input, input ), references = 1, size of lhs = 8:
% 12.37/12.69 p2-{F}(V0), r1-{F}(V0,V1), pppp14-{F}(V2,V1), r1-{F}(V3,V0), r1-{F}(V3,V4), pppp14-{F}(V5,V4), r1-{F}(V6,V3), pppp28-{F}(V7,V6) | pppp27-{T}(V3), pppp66-{T}(V4)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #870: disj( #80, input, input ), references = 1, size of lhs = 8:
% 12.37/12.69 p2-{F}(V0), r1-{F}(V0,V1), pppp47-{F}(V1,V2), r1-{F}(V3,V0), r1-{F}(V3,V4), pppp14-{F}(V5,V4), r1-{F}(V6,V3), pppp28-{F}(V7,V6) | pppp27-{T}(V3), pppp66-{T}(V4)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #871: disj( #80, input, input ), references = 1, size of lhs = 8:
% 12.37/12.69 p2-{F}(V0), r1-{F}(V0,V1), pppp14-{F}(V2,V1), r1-{F}(V3,V0), r1-{F}(V3,V4), pppp47-{F}(V4,V5), r1-{F}(V6,V3), pppp28-{F}(V7,V6) | pppp27-{T}(V3), pppp66-{T}(V4)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #874: disj( #865, #754+#461 ), references = 1, size of lhs = 15:
% 12.37/12.69 p2-{F}(V0), r1-{F}(V0,V1), pppp14-{F}(V2,V1), p1-{F}(V3), r1-{F}(V3,V4), pppp14-{F}(V5,V4), pppp7-{F}(V6,V4), r1-{F}(V7,V0), r1-{F}(V7,V4), r1-{F}(V7,V8), pppp14-{F}(V9,V8), r1-{F}(V10,V7), pppp28-{F}(V11,V10), r1-{F}(V12,V3), pppp45-{F}(V13,V12) | pppp66-{T}(V8)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #902: disj( #80, input, input ), references = 1, size of lhs = 8:
% 12.37/12.69 p2-{F}(V0), r1-{F}(V0,V1), pppp47-{F}(V1,V2), r1-{F}(V3,V0), r1-{F}(V3,V4), pppp14-{F}(V5,V4), r1-{F}(V6,V3), pppp28-{F}(V7,V6) | pppp27-{T}(V3), pppp66-{T}(V4)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #903: disj( #80, input, input ), references = 1, size of lhs = 8:
% 12.37/12.69 p2-{F}(V0), r1-{F}(V0,V1), pppp47-{F}(V1,V2), r1-{F}(V3,V0), r1-{F}(V3,V4), pppp47-{F}(V4,V5), r1-{F}(V6,V3), pppp28-{F}(V7,V6) | pppp27-{T}(V3), pppp66-{T}(V4)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #906: disj( #900, #754+#461 ), references = 1, size of lhs = 15:
% 12.37/12.69 p2-{F}(V0), r1-{F}(V0,V1), pppp47-{F}(V1,V2), p1-{F}(V3), r1-{F}(V3,V4), pppp14-{F}(V5,V4), pppp7-{F}(V6,V4), r1-{F}(V7,V0), r1-{F}(V7,V4), r1-{F}(V7,V8), pppp14-{F}(V9,V8), r1-{F}(V10,V7), pppp28-{F}(V11,V10), r1-{F}(V12,V3), pppp45-{F}(V13,V12) | pppp66-{T}(V8)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #912: disj( #80, #754+#461, input ), references = 1, size of lhs = 14:
% 12.37/12.69 p2-{F}(V0), r1-{F}(V0,V1), p1-{F}(V2), r1-{F}(V2,V3), pppp14-{F}(V4,V3), pppp7-{F}(V5,V3), r1-{F}(V6,V0), r1-{F}(V6,V3), r1-{F}(V6,V7), pppp14-{F}(V8,V7), r1-{F}(V9,V6), pppp28-{F}(V10,V9), r1-{F}(V11,V2), pppp45-{F}(V12,V11) | pppp66-{T}(V7), p2-{T}(V1)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #913: disj( #80, #754+#461, input ), references = 1, size of lhs = 14:
% 12.37/12.69 p2-{F}(V0), r1-{F}(V0,V1), p1-{F}(V2), r1-{F}(V2,V3), pppp14-{F}(V4,V3), pppp7-{F}(V5,V3), r1-{F}(V6,V0), r1-{F}(V6,V3), r1-{F}(V6,V7), pppp47-{F}(V7,V8), r1-{F}(V9,V6), pppp28-{F}(V10,V9), r1-{F}(V11,V2), pppp45-{F}(V12,V11) | pppp66-{T}(V7), p2-{T}(V1)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #917: mergings( V12 == V16, V11 == V15; #914 ), references = 1, size of lhs = 18:
% 12.37/12.69 p2-{F}(V0), r1-{F}(V0,V1), p1-{F}(V2), r1-{F}(V2,V3), pppp14-{F}(V4,V3), pppp7-{F}(V5,V3), p1-{F}(V6), r1-{F}(V6,V7), pppp14-{F}(V8,V7), pppp7-{F}(V9,V7), r1-{F}(V10,V0), r1-{F}(V10,V3), r1-{F}(V10,V7), r1-{F}(V11,V10), pppp28-{F}(V12,V11), r1-{F}(V13,V2), r1-{F}(V13,V6), pppp45-{F}(V14,V13) | p2-{T}(V1)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #923: mergings( V15 == V17, V14 == V16; #920 ), references = 1, size of lhs = 18:
% 12.37/12.69 p2-{F}(V0), pppp17-{F}(V1,V0), p1-{F}(V2), r1-{F}(V2,V3), pppp14-{F}(V4,V3), pppp7-{F}(V5,V3), p1-{F}(V6), r1-{F}(V6,V7), pppp14-{F}(V8,V7), pppp7-{F}(V9,V7), r1-{F}(V10,V0), r1-{F}(V10,V3), r1-{F}(V10,V7), r1-{F}(V11,V10), pppp28-{F}(V12,V11), r1-{F}(V13,V2), r1-{F}(V13,V6), pppp45-{F}(V14,V13) | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #929: mergings( V13 == V15, V12 == V14; #926 ), references = 1, size of lhs = 16:
% 12.37/12.69 pppp71-{F}(V0), p1-{F}(V1), r1-{F}(V1,V2), r1-{F}(V0,V2), pppp14-{F}(V3,V2), pppp7-{F}(V4,V2), p1-{F}(V5), r1-{F}(V5,V6), r1-{F}(V0,V6), pppp14-{F}(V7,V6), pppp7-{F}(V8,V6), r1-{F}(V9,V0), pppp28-{F}(V10,V9), r1-{F}(V11,V1), r1-{F}(V11,V5), pppp45-{F}(V12,V11) | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #935: mergings( V0 == V12, V1 == V11, V14 == V16, V13 == V15; #930 ), references = 1, size of lhs = 16:
% 12.37/12.69 p2-{F}(V0), p1-{F}(V1), r1-{F}(V1,V2), pppp14-{F}(V3,V2), pppp7-{F}(V4,V2), p1-{F}(V5), r1-{F}(V5,V6), pppp14-{F}(V7,V6), pppp7-{F}(V8,V6), r1-{F}(V0,V9), r1-{F}(V9,V2), r1-{F}(V9,V6), pppp28-{F}(V10,V0), r1-{F}(V11,V1), r1-{F}(V11,V5), pppp45-{F}(V12,V11) | p2-{T}(V9)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #956: exists( #112, #952 ), references = 2, size of lhs = 4:
% 12.37/12.69 p2-{F}(V0), pppp22-{F}(V0,V1), r1-{F}(V2,V0), pppp14-{F}(V3,V2) | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #963: exists( #97, #960 ), references = 4, size of lhs = 2:
% 12.37/12.69 pppp73-{F}(V0), pppp14-{F}(V1,V0) | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #966: disj( #82, #754+#962, input ), references = 1, size of lhs = 8:
% 12.37/12.69 p2-{F}(V0), r1-{F}(V0,V1), r1-{F}(V0,V2), pppp14-{F}(V3,V2), pppp14-{F}(V4,V2), pppp14-{F}(V5,V1), r1-{F}(V6,V0), pppp28-{F}(V7,V6) | pppp67-{T}(V1)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #989: exists( #102, #985 ), references = 3, size of lhs = 4:
% 12.37/12.69 p2-{F}(V0), pppp26-{F}(V0,V1), r1-{F}(V2,V0), pppp14-{F}(V3,V2) | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #994: exists( #83, #992 ), references = 1, size of lhs = 2:
% 12.37/12.69 pppp67-{F}(V0), pppp14-{F}(V1,V0) | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #999: mergings( V0 == V10, V1 == V9; #996 ), references = 1, size of lhs = 9:
% 12.37/12.69 p2-{F}(V0), r1-{F}(V0,V1), r1-{F}(V1,V2), r1-{F}(V1,V3), pppp14-{F}(V4,V3), pppp14-{F}(V5,V3), pppp14-{F}(V6,V2), pppp14-{F}(V7,V2), pppp28-{F}(V8,V0) | pppp71-{T}(V1)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #1007: disj( #850, input ), references = 1, size of lhs = 13:
% 12.37/12.69 p2-{F}(V0), r1-{F}(V0,V1), p1-{F}(V2), r1-{F}(V2,V3), pppp47-{F}(V3,V4), pppp7-{F}(V5,V3), pppp3-{F}(V6,V1), r1-{F}(V7,V3), r1-{F}(V7,V0), r1-{F}(V8,V7), pppp28-{F}(V9,V8), r1-{F}(V10,V2), pppp45-{F}(V11,V10) | pppp27-{T}(V7)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #1008: disj( #850, input ), references = 1, size of lhs = 13:
% 12.37/12.69 p2-{F}(V0), r1-{F}(V0,V1), p1-{F}(V2), r1-{F}(V2,V3), pppp47-{F}(V3,V4), pppp7-{F}(V5,V3), pppp12-{F}(V1,V6), r1-{F}(V7,V3), r1-{F}(V7,V0), r1-{F}(V8,V7), pppp28-{F}(V9,V8), r1-{F}(V10,V2), pppp45-{F}(V11,V10) | pppp27-{T}(V7)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #1009: disj( #850, input ), references = 1, size of lhs = 13:
% 12.37/12.69 p2-{F}(V0), r1-{F}(V0,V1), p1-{F}(V2), r1-{F}(V2,V3), pppp47-{F}(V3,V4), pppp7-{F}(V5,V3), pppp4-{F}(V6,V1), r1-{F}(V7,V3), r1-{F}(V7,V0), r1-{F}(V8,V7), pppp28-{F}(V9,V8), r1-{F}(V10,V2), pppp45-{F}(V11,V10) | pppp27-{T}(V7)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #1017: disj( #80, input, input ), references = 1, size of lhs = 8:
% 12.37/12.69 p2-{F}(V0), r1-{F}(V0,V1), pppp47-{F}(V1,V2), r1-{F}(V3,V0), r1-{F}(V3,V4), pppp47-{F}(V4,V5), r1-{F}(V6,V3), pppp28-{F}(V7,V6) | pppp27-{T}(V3), pppp66-{T}(V4)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #1022: disj( #1016, #754+#963 ), references = 1, size of lhs = 11:
% 12.37/12.69 p2-{F}(V0), r1-{F}(V0,V1), pppp47-{F}(V1,V2), r1-{F}(V3,V0), r1-{F}(V3,V4), pppp47-{F}(V4,V5), r1-{F}(V3,V6), pppp14-{F}(V7,V6), pppp14-{F}(V8,V6), r1-{F}(V9,V3), pppp28-{F}(V10,V9) | pppp66-{T}(V4)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #1023: disj( #1016, #443+#461 ), references = 1, size of lhs = 15:
% 12.37/12.69 p2-{F}(V0), r1-{F}(V0,V1), pppp47-{F}(V1,V2), p1-{F}(V3), r1-{F}(V3,V4), pppp47-{F}(V4,V5), pppp7-{F}(V6,V4), r1-{F}(V7,V0), r1-{F}(V7,V4), r1-{F}(V7,V8), pppp47-{F}(V8,V9), r1-{F}(V10,V7), pppp28-{F}(V11,V10), r1-{F}(V12,V3), pppp45-{F}(V13,V12) | pppp66-{T}(V8)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #1039: disj( #80, input, input ), references = 1, size of lhs = 8:
% 12.37/12.69 p2-{F}(V0), r1-{F}(V0,V1), pppp16-{F}(V1,V2), r1-{F}(V3,V0), r1-{F}(V3,V4), pppp16-{F}(V4,V5), r1-{F}(V6,V3), pppp28-{F}(V7,V6) | pppp27-{T}(V3), pppp66-{T}(V4)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #1040: disj( #80, input, input ), references = 1, size of lhs = 8:
% 12.37/12.69 p2-{F}(V0), r1-{F}(V0,V1), pppp14-{F}(V2,V1), r1-{F}(V3,V0), r1-{F}(V3,V4), pppp16-{F}(V4,V5), r1-{F}(V6,V3), pppp28-{F}(V7,V6) | pppp27-{T}(V3), pppp66-{T}(V4)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #1041: disj( #80, input, input ), references = 1, size of lhs = 8:
% 12.37/12.69 p2-{F}(V0), r1-{F}(V0,V1), pppp16-{F}(V1,V2), r1-{F}(V3,V0), r1-{F}(V3,V4), pppp14-{F}(V5,V4), r1-{F}(V6,V3), pppp28-{F}(V7,V6) | pppp27-{T}(V3), pppp66-{T}(V4)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #1046: disj( #1035, #754+#963 ), references = 1, size of lhs = 11:
% 12.37/12.69 p2-{F}(V0), r1-{F}(V0,V1), pppp16-{F}(V1,V2), r1-{F}(V3,V0), r1-{F}(V3,V4), pppp16-{F}(V4,V5), r1-{F}(V3,V6), pppp14-{F}(V7,V6), pppp14-{F}(V8,V6), r1-{F}(V9,V3), pppp28-{F}(V10,V9) | pppp66-{T}(V4)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #1047: disj( #1035, #443+#461 ), references = 1, size of lhs = 15:
% 12.37/12.69 p2-{F}(V0), r1-{F}(V0,V1), pppp16-{F}(V1,V2), p1-{F}(V3), r1-{F}(V3,V4), pppp47-{F}(V4,V5), pppp7-{F}(V6,V4), r1-{F}(V7,V0), r1-{F}(V7,V4), r1-{F}(V7,V8), pppp16-{F}(V8,V9), r1-{F}(V10,V7), pppp28-{F}(V11,V10), r1-{F}(V12,V3), pppp45-{F}(V13,V12) | pppp66-{T}(V8)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #1053: exists( #81, #1050 ), references = 1, size of lhs = 2:
% 12.37/12.69 pppp66-{F}(V0), pppp14-{F}(V1,V0) | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #1060: disj( #80, #754+#963, input ), references = 1, size of lhs = 10:
% 12.37/12.69 p2-{F}(V0), r1-{F}(V0,V1), pppp16-{F}(V1,V2), r1-{F}(V3,V0), r1-{F}(V3,V4), r1-{F}(V3,V5), pppp14-{F}(V6,V5), pppp14-{F}(V7,V5), r1-{F}(V8,V3), pppp28-{F}(V9,V8) | p2-{T}(V4), pppp66-{T}(V4)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #1061: disj( #80, #443+#461, input ), references = 1, size of lhs = 14:
% 12.37/12.69 p2-{F}(V0), r1-{F}(V0,V1), p1-{F}(V2), r1-{F}(V2,V3), pppp47-{F}(V3,V4), pppp7-{F}(V5,V3), pppp16-{F}(V1,V6), r1-{F}(V7,V0), r1-{F}(V7,V3), r1-{F}(V7,V8), r1-{F}(V9,V7), pppp28-{F}(V10,V9), r1-{F}(V11,V2), pppp45-{F}(V12,V11) | p2-{T}(V8), pppp66-{T}(V8)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #1063: disj( #1058, exists( #81, #1050 ) ), references = 1, size of lhs = 11:
% 12.37/12.69 p2-{F}(V0), r1-{F}(V0,V1), pppp16-{F}(V1,V2), r1-{F}(V3,V0), r1-{F}(V3,V4), r1-{F}(V3,V5), pppp14-{F}(V6,V5), pppp14-{F}(V7,V5), pppp14-{F}(V8,V4), r1-{F}(V9,V3), pppp28-{F}(V10,V9) | p2-{T}(V4)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #1067: exists( #125, #1065 ), references = 1, size of lhs = 11:
% 12.37/12.69 p2-{F}(V0), pppp17-{F}(V1,V0), r1-{F}(V2,V0), r1-{F}(V2,V3), r1-{F}(V2,V4), pppp14-{F}(V5,V4), pppp14-{F}(V6,V4), pppp14-{F}(V7,V3), pppp14-{F}(V8,V3), r1-{F}(V9,V2), pppp28-{F}(V10,V9) | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #1071: exists( #91, #1069 ), references = 1, size of lhs = 9:
% 12.37/12.69 pppp71-{F}(V0), r1-{F}(V0,V1), r1-{F}(V0,V2), pppp14-{F}(V3,V2), pppp14-{F}(V4,V2), pppp14-{F}(V5,V1), pppp14-{F}(V6,V1), r1-{F}(V7,V0), pppp28-{F}(V8,V7) | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #1079: mergings( V4 == V6, V3 == V5, V6 == V8, V5 == V7; #1074 ), references = 1, size of lhs = 4:
% 12.37/12.69 p2-{F}(V0), r1-{F}(V0,V1), pppp15-{F}(V1,V2), pppp28-{F}(V3,V0) | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #1085: mergings( V0 == V3, V3 == V4, V4 == V5; #1081 ), references = 1, size of lhs = 2:
% 12.37/12.69 p2-{F}(V0), pppp28-{F}(V1,V0) | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #1090: exists( #18, #1088 ), references = 1, size of lhs = 2:
% 12.37/12.69 pppp59-{F}(V0), pppp48-{F}(V0) | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #1104: disj( #22, input ), references = 1, size of lhs = 3:
% 12.37/12.69 pppp48-{F}(V0), r1-{F}(V0,V1), pppp11-{F}(V2,V1) | pppp61-{T}(V1)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #1106: disj( #2, input ), references = 1, size of lhs = 3:
% 12.37/12.69 pppp48-{F}(V0), r1-{F}(V0,V1), pppp11-{F}(V2,V1) | pppp50-{T}(V1)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #1121: exists( #155, #1118 ), references = 1, size of lhs = 4:
% 12.37/12.69 p2-{F}(V0), pppp5-{F}(V0,V1), r1-{F}(V2,V0), pppp11-{F}(V3,V2) | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #1125: exists( #23, #1123 ), references = 1, size of lhs = 2:
% 12.37/12.69 pppp61-{F}(V0), pppp11-{F}(V1,V0) | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #1129: exists( #17, #1127 ), references = 1, size of lhs = 2:
% 12.37/12.69 pppp58-{F}(V0), pppp48-{F}(V0) | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #1131: disj( #15, exists( #17, #1127 ), exists( #18, #1088 ) ), references = 4, size of lhs = 3:
% 12.37/12.69 pppp48-{F}(V0), r1-{F}(V0,V1), r1-{F}(V1,V2) | p2-{T}(V2), pppp57-{T}(V2)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #1133: disj( #25, input ), references = 1, size of lhs = 3:
% 12.37/12.69 pppp48-{F}(V0), r1-{F}(V0,V1), pppp0-{F}(V2,V1) | pppp62-{T}(V1)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #1150: disj( #1131, input ), references = 1, size of lhs = 4:
% 12.37/12.69 pppp48-{F}(V0), r1-{F}(V0,V1), r1-{F}(V1,V2), pppp4-{F}(V3,V2) | pppp57-{T}(V2)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #1151: disj( #1131, input ), references = 1, size of lhs = 4:
% 12.37/12.69 pppp48-{F}(V0), r1-{F}(V0,V1), r1-{F}(V1,V2), pppp9-{F}(V2,V3) | pppp57-{T}(V2)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #1171: exists( #16, #1169 ), references = 1, size of lhs = 6:
% 12.37/12.69 pppp57-{F}(V0), p1-{F}(V1), r1-{F}(V1,V0), pppp7-{F}(V2,V0), r1-{F}(V3,V1), pppp45-{F}(V4,V3) | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #1178: disj( #1131, exists( #16, #1169 ) ), references = 1, size of lhs = 8:
% 12.37/12.69 pppp48-{F}(V0), r1-{F}(V0,V1), r1-{F}(V1,V2), p1-{F}(V3), r1-{F}(V3,V2), pppp7-{F}(V4,V2), r1-{F}(V5,V3), pppp45-{F}(V6,V5) | p2-{T}(V2)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #1198: exists( #143, #1194 ), references = 2, size of lhs = 4:
% 12.37/12.69 p2-{F}(V0), pppp10-{F}(V1,V0), r1-{F}(V2,V0), pppp47-{F}(V2,V3) | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #1199: exists( #143, #1195 ), references = 1, size of lhs = 6:
% 12.37/12.69 p1-{F}(V0), r1-{F}(V0,V1), pppp10-{F}(V2,V1), pppp7-{F}(V3,V1), r1-{F}(V4,V0), pppp45-{F}(V5,V4) | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #1207: exists( #16, #1205 ), references = 1, size of lhs = 2:
% 12.37/12.69 pppp57-{F}(V0), pppp47-{F}(V0,V1) | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #1209: disj( #1131, exists( #16, #1205 ) ), references = 1, size of lhs = 4:
% 12.37/12.69 pppp48-{F}(V0), r1-{F}(V0,V1), r1-{F}(V1,V2), pppp47-{F}(V2,V3) | p2-{T}(V2)
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #1213: exists( #3, #1211 ), references = 1, size of lhs = 3:
% 12.37/12.69 pppp50-{F}(V0), pppp48-{F}(V1), r1-{F}(V1,V0) | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #1217: exists( #24, #1215 ), references = 1, size of lhs = 1:
% 12.37/12.69 pppp48-{F}(V0) | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 #1220: exists( #0, #1218 ), references = 1, size of lhs = 0:
% 12.37/12.69 FALSE | FALSE
% 12.37/12.69 (used 0 times, uses = {})
% 12.37/12.69
% 12.37/12.69 number of learnt formulas = 138
% 12.37/12.69
% 12.37/12.69
% 12.37/12.69 % SZS output end Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 12.37/12.69
% 12.37/12.69 randbase = 1
%------------------------------------------------------------------------------