%------------------------------------------------------------------------------
% File : Geo-III---2018C
% Problem : PUZ032-1 : TPTP v8.1.0. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : geo -tptp_input -nonempty -inputfile %s
% Computer : n012.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:14:20 EDT 2022
% Result : Unsatisfiable 1.75s 1.96s
% Output : Refutation 1.75s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : PUZ032-1 : TPTP v8.1.0. Released v1.0.0.
% 0.06/0.13 % Command : geo -tptp_input -nonempty -inputfile %s
% 0.12/0.33 % Computer : n012.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Fri Jul 22 06:59:44 EDT 2022
% 0.12/0.34 % CPUTime :
% 1.75/1.96 GeoParameters:
% 1.75/1.96
% 1.75/1.96 tptp_input = 1
% 1.75/1.96 tptp_output = 0
% 1.75/1.96 nonempty = 1
% 1.75/1.96 inputfile = /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.75/1.96 includepath = /export/starexec/sandbox2/solver/bin/../../benchmark/
% 1.75/1.96
% 1.75/1.96
% 1.75/1.96 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.75/1.96 % SZS output start Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.75/1.96
% 1.75/1.96 RuleSystem INPUT:
% 1.75/1.96
% 1.75/1.96 Initial Rules:
% 1.75/1.96 #0: input, references = 26, size of lhs = 2:
% 1.75/1.96 P_truthteller-{F}(V0,V1), P_liar-{F}(V0,V2) | a_truth-{T}(V1), a_truth-{T}(V2)
% 1.75/1.96 (used 0 times, uses = {})
% 1.75/1.96
% 1.75/1.96 #1: input, references = 13, size of lhs = 4:
% 1.75/1.96 P_truthteller-{F}(V0,V1), P_liar-{F}(V0,V2), a_truth-{F}(V1), a_truth-{F}(V2) | FALSE
% 1.75/1.96 (used 0 times, uses = {})
% 1.75/1.96
% 1.75/1.96 #2: input, references = 37, size of lhs = 4:
% 1.75/1.96 P_truthteller-{F}(V1,V2), P_says-{F}(V1,V0,V3), a_truth-{F}(V2), a_truth-{F}(V3) | a_truth-{T}(V0)
% 1.75/1.96 (used 0 times, uses = {})
% 1.75/1.96
% 1.75/1.96 #3: input, references = 22, size of lhs = 5:
% 1.75/1.96 P_liar-{F}(V0,V1), a_truth-{F}(V1), P_says-{F}(V0,V2,V3), a_truth-{F}(V3), a_truth-{F}(V2) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #4: input, references = 5, size of lhs = 4:
% 1.75/1.97 a_truth-{F}(V0), P_says-{F}(V1,V0,V2), P_truthteller-{F}(V1,V3), a_truth-{F}(V2) | a_truth-{T}(V3)
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #5: input, references = 3, size of lhs = 3:
% 1.75/1.97 P_liar-{F}(V0,V1), P_says-{F}(V0,V2,V3), a_truth-{F}(V3) | a_truth-{T}(V1), a_truth-{T}(V2)
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #6: input, references = 19, size of lhs = 3:
% 1.75/1.97 P_a-{F}(V0), P_mumble-{F}(V1), P_says-{F}(V0,V1,V2) | a_truth-{T}(V2)
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #7: input, references = 13, size of lhs = 7:
% 1.75/1.97 P_a-{F}(V0), P_mumble-{F}(V1), P_says-{F}(V0,V1,V2), P_b-{F}(V3), P_liar-{F}(V0,V4), P_says-{F}(V0,V4,V5), P_says-{F}(V3,V5,V6) | a_truth-{T}(V6)
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #8: input, references = 7, size of lhs = 10:
% 1.75/1.97 P_a-{F}(V0), P_mumble-{F}(V1), P_says-{F}(V0,V1,V2), P_b-{F}(V3), P_liar-{F}(V0,V4), P_says-{F}(V0,V4,V5), P_says-{F}(V3,V5,V6), P_c-{F}(V7), P_liar-{F}(V3,V8), P_says-{F}(V7,V8,V9) | a_truth-{T}(V9)
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #9: input, references = 5, size of lhs = 12:
% 1.75/1.97 P_a-{F}(V0), P_mumble-{F}(V1), P_says-{F}(V0,V1,V2), P_b-{F}(V3), P_liar-{F}(V0,V4), P_says-{F}(V0,V4,V5), P_says-{F}(V3,V5,V6), P_c-{F}(V7), P_liar-{F}(V3,V8), P_says-{F}(V7,V8,V9), P_truthteller-{F}(V7,V10), a_truth-{F}(V10) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #10: input, references = 12, size of lhs = 1:
% 1.75/1.97 #-{F} V0 | EXISTS V1: P_truthteller-{T}(V0,V1)
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #11: input, references = 19, size of lhs = 1:
% 1.75/1.97 #-{F} V0 | EXISTS V1: P_liar-{T}(V0,V1)
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #12: input, references = 42, size of lhs = 2:
% 1.75/1.97 #-{F} V0, #-{F} V1 | EXISTS V2: P_says-{T}(V0,V1,V2)
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #13: input, references = 4, size of lhs = 0:
% 1.75/1.97 FALSE | EXISTS V0: P_a-{T}(V0)
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #14: input, references = 4, size of lhs = 0:
% 1.75/1.97 FALSE | EXISTS V0: P_mumble-{T}(V0)
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #15: input, references = 4, size of lhs = 0:
% 1.75/1.97 FALSE | EXISTS V0: P_b-{T}(V0)
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #16: input, references = 5, size of lhs = 0:
% 1.75/1.97 FALSE | EXISTS V0: P_c-{T}(V0)
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 number of initial rules = 17
% 1.75/1.97
% 1.75/1.97 Simplifiers:
% 1.75/1.97 #17: unsound, references = 3, size of lhs = 3:
% 1.75/1.97 P_truthteller-{F}(V0,V1), P_truthteller-{F}(V0,V3), V1 == V3 | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #18: unsound, references = 3, size of lhs = 3:
% 1.75/1.97 P_liar-{F}(V0,V1), P_liar-{F}(V0,V3), V1 == V3 | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #19: unsound, references = 3, size of lhs = 3:
% 1.75/1.97 P_says-{F}(V0,V1,V2), P_says-{F}(V0,V1,V5), V2 == V5 | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #20: unsound, references = 3, size of lhs = 3:
% 1.75/1.97 P_a-{F}(V0), P_a-{F}(V1), V0 == V1 | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #21: unsound, references = 3, size of lhs = 3:
% 1.75/1.97 P_mumble-{F}(V0), P_mumble-{F}(V1), V0 == V1 | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #22: unsound, references = 3, size of lhs = 3:
% 1.75/1.97 P_b-{F}(V0), P_b-{F}(V1), V0 == V1 | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #23: unsound, references = 3, size of lhs = 3:
% 1.75/1.97 P_c-{F}(V0), P_c-{F}(V1), V0 == V1 | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 number of simplifiers = 7
% 1.75/1.97
% 1.75/1.97 Learnt:
% 1.75/1.97 #26: disj( #0, input ), references = 1, size of lhs = 4:
% 1.75/1.97 P_truthteller-{F}(V0,V1), P_liar-{F}(V0,V2), P_truthteller-{F}(V3,V1), P_liar-{F}(V3,V1) | a_truth-{T}(V2)
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #27: disj( #0, input ), references = 1, size of lhs = 4:
% 1.75/1.97 P_truthteller-{F}(V0,V1), P_liar-{F}(V0,V2), P_liar-{F}(V3,V1), P_says-{F}(V3,V1,V1) | a_truth-{T}(V2)
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #40: exists( #12, #36 ), references = 3, size of lhs = 13:
% 1.75/1.97 P_a-{F}(V0), P_mumble-{F}(V1), P_says-{F}(V0,V1,V2), P_b-{F}(V3), P_liar-{F}(V0,V4), P_says-{F}(V0,V4,V5), P_c-{F}(V6), P_liar-{F}(V3,V7), P_says-{F}(V6,V7,V8), a_truth-{F}(V9), P_liar-{F}(V10,V9), a_truth-{F}(V11), P_says-{F}(V10,V11,V8) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #43: mergings( V1 == V6; #41 ), references = 4, size of lhs = 8:
% 1.75/1.97 P_a-{F}(V0), P_c-{F}(V0), P_mumble-{F}(V1), P_says-{F}(V0,V1,V2), P_b-{F}(V3), P_liar-{F}(V3,V4), a_truth-{F}(V4), P_liar-{F}(V0,V4) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #47: disj( #0, mergings( V1 == V6; #41 ) ), references = 6, size of lhs = 9:
% 1.75/1.97 P_a-{F}(V0), P_c-{F}(V0), P_mumble-{F}(V1), P_says-{F}(V0,V1,V2), P_b-{F}(V3), P_liar-{F}(V3,V4), P_liar-{F}(V0,V4), P_truthteller-{F}(V5,V4), P_liar-{F}(V5,V6) | a_truth-{T}(V6)
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #52: exists( #12, #50 ), references = 1, size of lhs = 11:
% 1.75/1.97 P_a-{F}(V0), P_c-{F}(V0), P_mumble-{F}(V1), P_b-{F}(V2), P_liar-{F}(V2,V3), P_liar-{F}(V0,V3), P_truthteller-{F}(V4,V3), P_liar-{F}(V4,V5), P_truthteller-{F}(V0,V5), P_liar-{F}(V6,V5), P_says-{F}(V6,V1,V5) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #59: exists( #12, #57 ), references = 1, size of lhs = 11:
% 1.75/1.97 P_a-{F}(V0), P_c-{F}(V0), P_mumble-{F}(V1), P_b-{F}(V2), P_liar-{F}(V2,V3), P_liar-{F}(V0,V3), P_truthteller-{F}(V4,V3), P_liar-{F}(V4,V5), P_truthteller-{F}(V0,V5), P_liar-{F}(V6,V5), P_says-{F}(V6,V1,V1) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #65: disj( #0, input ), references = 1, size of lhs = 6:
% 1.75/1.97 a_truth-{F}(V0), P_liar-{F}(V1,V0), a_truth-{F}(V2), P_says-{F}(V1,V2,V3), P_truthteller-{F}(V4,V3), P_liar-{F}(V4,V5) | a_truth-{T}(V5)
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #66: disj( #0, input ), references = 2, size of lhs = 5:
% 1.75/1.97 a_truth-{F}(V0), P_liar-{F}(V1,V0), P_truthteller-{F}(V1,V2), P_truthteller-{F}(V3,V2), P_liar-{F}(V3,V4) | a_truth-{T}(V4)
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #74: exists( #12, #9 ), references = 2, size of lhs = 11:
% 1.75/1.97 P_a-{F}(V0), P_mumble-{F}(V1), P_says-{F}(V0,V1,V2), P_b-{F}(V3), P_liar-{F}(V0,V4), P_says-{F}(V0,V4,V5), P_c-{F}(V6), P_liar-{F}(V3,V7), P_says-{F}(V6,V7,V8), P_truthteller-{F}(V6,V9), a_truth-{F}(V9) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #76: exists( #12, #73 ), references = 2, size of lhs = 9:
% 1.75/1.97 P_a-{F}(V0), P_c-{F}(V0), P_mumble-{F}(V1), P_says-{F}(V0,V1,V2), P_b-{F}(V3), P_liar-{F}(V0,V4), P_liar-{F}(V3,V4), P_truthteller-{F}(V0,V5), a_truth-{F}(V5) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #82: mergings( V4 == V8, V3 == V7; #79 ), references = 1, size of lhs = 9:
% 1.75/1.97 P_a-{F}(V0), P_c-{F}(V0), P_truthteller-{F}(V0,V1), P_liar-{F}(V2,V1), P_truthteller-{F}(V2,V3), P_liar-{F}(V0,V3), P_mumble-{F}(V4), P_b-{F}(V5), P_liar-{F}(V5,V3) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #91: disj( #0, input ), references = 15, size of lhs = 5:
% 1.75/1.97 a_truth-{F}(V0), P_truthteller-{F}(V1,V0), P_liar-{F}(V1,V2), P_truthteller-{F}(V3,V2), P_liar-{F}(V3,V4) | a_truth-{T}(V4)
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #92: disj( #0, input ), references = 1, size of lhs = 6:
% 1.75/1.97 a_truth-{F}(V0), a_truth-{F}(V1), P_says-{F}(V2,V1,V0), P_liar-{F}(V2,V3), P_truthteller-{F}(V4,V3), P_liar-{F}(V4,V5) | a_truth-{T}(V5)
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #99: disj( #0, exists( #12, #73 ) ), references = 1, size of lhs = 10:
% 1.75/1.97 P_a-{F}(V0), P_c-{F}(V0), P_mumble-{F}(V1), P_says-{F}(V0,V1,V2), P_b-{F}(V3), P_liar-{F}(V0,V4), P_liar-{F}(V3,V4), P_truthteller-{F}(V0,V5), P_liar-{F}(V6,V5), P_truthteller-{F}(V6,V7) | a_truth-{T}(V7)
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #108: mergings( V4 == V11, V3 == V12; #104 ), references = 1, size of lhs = 13:
% 1.75/1.97 P_a-{F}(V0), P_c-{F}(V0), P_truthteller-{F}(V0,V1), P_liar-{F}(V2,V1), P_truthteller-{F}(V2,V3), P_truthteller-{F}(V4,V3), P_liar-{F}(V4,V5), P_truthteller-{F}(V6,V5), P_liar-{F}(V6,V7), P_liar-{F}(V0,V7), P_mumble-{F}(V8), P_b-{F}(V9), P_liar-{F}(V9,V7) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #111: mergings( V2 == V6; #109 ), references = 1, size of lhs = 9:
% 1.75/1.97 P_a-{F}(V0), P_c-{F}(V0), P_b-{F}(V0), P_truthteller-{F}(V0,V1), P_liar-{F}(V2,V1), P_truthteller-{F}(V2,V3), P_truthteller-{F}(V4,V3), P_liar-{F}(V4,V1), P_mumble-{F}(V5) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #119: disj( #0, input ), references = 3, size of lhs = 5:
% 1.75/1.97 a_truth-{F}(V0), P_liar-{F}(V1,V0), P_says-{F}(V1,V2,V2), P_truthteller-{F}(V3,V2), P_liar-{F}(V3,V4) | a_truth-{T}(V4)
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #129: exists( #12, #123 ), references = 1, size of lhs = 14:
% 1.75/1.97 P_a-{F}(V0), P_c-{F}(V0), P_mumble-{F}(V1), P_b-{F}(V2), P_liar-{F}(V2,V3), P_liar-{F}(V0,V3), P_truthteller-{F}(V4,V3), P_liar-{F}(V4,V5), P_liar-{F}(V6,V5), P_liar-{F}(V7,V5), P_truthteller-{F}(V7,V8), P_liar-{F}(V9,V8), P_truthteller-{F}(V9,V10), P_says-{F}(V6,V10,V10) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #132: mergings( V4 == V9, V3 == V8; #127 ), references = 1, size of lhs = 12:
% 1.75/1.97 P_a-{F}(V0), P_c-{F}(V0), P_mumble-{F}(V1), P_b-{F}(V2), P_liar-{F}(V2,V3), P_liar-{F}(V0,V3), P_truthteller-{F}(V4,V3), P_liar-{F}(V4,V5), P_liar-{F}(V6,V5), P_liar-{F}(V7,V3), P_truthteller-{F}(V7,V8), P_says-{F}(V6,V8,V8) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #133: exists( #12, #125 ), references = 1, size of lhs = 14:
% 1.75/1.97 P_a-{F}(V0), P_c-{F}(V0), P_mumble-{F}(V1), P_b-{F}(V2), P_liar-{F}(V2,V3), P_liar-{F}(V0,V3), P_truthteller-{F}(V4,V3), P_liar-{F}(V4,V5), P_liar-{F}(V6,V5), P_liar-{F}(V7,V5), P_says-{F}(V6,V8,V8), P_truthteller-{F}(V9,V8), P_liar-{F}(V9,V10), P_says-{F}(V7,V10,V10) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #144: disj( #0, exists( #12, #73 ) ), references = 1, size of lhs = 10:
% 1.75/1.97 P_a-{F}(V0), P_c-{F}(V0), P_mumble-{F}(V1), P_says-{F}(V0,V1,V2), P_b-{F}(V3), P_liar-{F}(V0,V4), P_liar-{F}(V3,V4), P_truthteller-{F}(V0,V5), P_truthteller-{F}(V6,V5), P_liar-{F}(V6,V7) | a_truth-{T}(V7)
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #153: mergings( V4 == V7, V3 == V8; #150 ), references = 1, size of lhs = 9:
% 1.75/1.97 P_a-{F}(V0), P_c-{F}(V0), P_truthteller-{F}(V0,V1), P_truthteller-{F}(V2,V1), P_liar-{F}(V2,V3), P_liar-{F}(V0,V3), P_mumble-{F}(V4), P_b-{F}(V5), P_liar-{F}(V5,V3) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #155: exists( #11, #150 ), references = 1, size of lhs = 5:
% 1.75/1.97 P_a-{F}(V0), P_c-{F}(V0), P_b-{F}(V0), P_truthteller-{F}(V0,V1), P_mumble-{F}(V2) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #157: exists( #10, #154 ), references = 1, size of lhs = 4:
% 1.75/1.97 P_a-{F}(V0), P_c-{F}(V0), P_b-{F}(V0), P_mumble-{F}(V1) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #164: disj( #0, #91+#1 ), references = 1, size of lhs = 8:
% 1.75/1.97 P_truthteller-{F}(V0,V1), P_liar-{F}(V0,V2), P_truthteller-{F}(V3,V1), P_liar-{F}(V3,V4), P_truthteller-{F}(V5,V4), P_liar-{F}(V5,V6), P_truthteller-{F}(V7,V6), P_liar-{F}(V7,V1) | a_truth-{T}(V2)
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #173: disj( #0, #2+#1 ), references = 1, size of lhs = 6:
% 1.75/1.97 P_truthteller-{F}(V0,V1), P_liar-{F}(V0,V2), P_truthteller-{F}(V3,V2), P_truthteller-{F}(V4,V2), P_liar-{F}(V4,V5), P_says-{F}(V3,V5,V2) | a_truth-{T}(V1)
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #174: disj( #0, #2+#3 ), references = 1, size of lhs = 6:
% 1.75/1.97 P_truthteller-{F}(V0,V1), P_liar-{F}(V0,V2), P_truthteller-{F}(V3,V2), P_says-{F}(V3,V4,V2), P_liar-{F}(V5,V4), P_says-{F}(V5,V4,V2) | a_truth-{T}(V1)
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #188: disj( #0, #2+#1 ), references = 4, size of lhs = 7:
% 1.75/1.97 a_truth-{F}(V0), P_truthteller-{F}(V1,V2), P_liar-{F}(V1,V3), P_truthteller-{F}(V4,V3), P_truthteller-{F}(V5,V3), P_liar-{F}(V5,V6), P_says-{F}(V4,V6,V0) | a_truth-{T}(V2)
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #189: disj( #0, #2+#3 ), references = 1, size of lhs = 8:
% 1.75/1.97 a_truth-{F}(V0), a_truth-{F}(V1), P_truthteller-{F}(V2,V3), P_liar-{F}(V2,V4), P_truthteller-{F}(V5,V4), P_says-{F}(V5,V6,V0), P_liar-{F}(V7,V6), P_says-{F}(V7,V6,V1) | a_truth-{T}(V3)
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #194: exists( #12, #192 ), references = 1, size of lhs = 12:
% 1.75/1.97 P_a-{F}(V0), P_mumble-{F}(V1), P_liar-{F}(V0,V1), P_truthteller-{F}(V0,V2), P_liar-{F}(V3,V2), P_truthteller-{F}(V3,V4), P_truthteller-{F}(V5,V2), P_liar-{F}(V5,V1), P_truthteller-{F}(V6,V4), P_liar-{F}(V6,V7), P_truthteller-{F}(V8,V7), P_liar-{F}(V8,V1) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #200: exists( #12, #40 ), references = 1, size of lhs = 11:
% 1.75/1.97 P_a-{F}(V0), P_mumble-{F}(V1), P_says-{F}(V0,V1,V2), P_b-{F}(V3), P_liar-{F}(V0,V4), P_says-{F}(V0,V4,V5), P_c-{F}(V6), P_liar-{F}(V3,V7), a_truth-{F}(V7), a_truth-{F}(V8), P_liar-{F}(V6,V8) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #202: exists( #12, #199 ), references = 4, size of lhs = 10:
% 1.75/1.97 P_a-{F}(V0), P_mumble-{F}(V1), P_says-{F}(V0,V1,V2), P_b-{F}(V3), P_liar-{F}(V0,V4), P_c-{F}(V5), P_liar-{F}(V3,V6), a_truth-{F}(V6), a_truth-{F}(V7), P_liar-{F}(V5,V7) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #205: disj( #0, #91+#201 ), references = 2, size of lhs = 14:
% 1.75/1.97 P_a-{F}(V0), P_mumble-{F}(V1), P_says-{F}(V0,V1,V2), P_b-{F}(V3), P_liar-{F}(V3,V4), P_liar-{F}(V5,V4), P_truthteller-{F}(V5,V6), P_liar-{F}(V7,V6), P_truthteller-{F}(V7,V8), P_truthteller-{F}(V9,V8), P_liar-{F}(V9,V10), P_liar-{F}(V0,V11), P_c-{F}(V12), P_liar-{F}(V12,V4) | a_truth-{T}(V10)
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #219: exists( #12, #217 ), references = 1, size of lhs = 16:
% 1.75/1.97 P_a-{F}(V0), P_mumble-{F}(V1), P_b-{F}(V2), P_liar-{F}(V2,V3), P_liar-{F}(V4,V3), P_truthteller-{F}(V4,V5), P_liar-{F}(V6,V5), P_truthteller-{F}(V6,V7), P_truthteller-{F}(V8,V7), P_liar-{F}(V8,V9), P_truthteller-{F}(V0,V9), P_liar-{F}(V0,V10), P_c-{F}(V11), P_liar-{F}(V11,V3), P_liar-{F}(V12,V9), P_says-{F}(V12,V1,V9) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #253: mergings( V5 == V10; #249 ), references = 1, size of lhs = 13:
% 1.75/1.97 P_a-{F}(V0), P_mumble-{F}(V1), P_liar-{F}(V2,V1), P_truthteller-{F}(V2,V3), P_truthteller-{F}(V0,V3), P_liar-{F}(V4,V3), P_truthteller-{F}(V4,V5), P_truthteller-{F}(V6,V5), P_liar-{F}(V6,V7), P_truthteller-{F}(V8,V7), P_liar-{F}(V8,V1), P_truthteller-{F}(V9,V3), P_liar-{F}(V9,V1) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #255: mergings( V5 == V10; #250 ), references = 1, size of lhs = 13:
% 1.75/1.97 P_a-{F}(V0), P_mumble-{F}(V1), P_liar-{F}(V2,V1), P_truthteller-{F}(V2,V3), P_truthteller-{F}(V0,V3), P_liar-{F}(V4,V3), P_truthteller-{F}(V4,V5), P_truthteller-{F}(V6,V5), P_liar-{F}(V6,V7), P_truthteller-{F}(V8,V7), P_liar-{F}(V8,V1), P_liar-{F}(V9,V3), P_says-{F}(V9,V5,V3) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #256: exists( #12, #248 ), references = 1, size of lhs = 20:
% 1.75/1.97 P_a-{F}(V0), P_mumble-{F}(V1), P_b-{F}(V2), P_liar-{F}(V2,V3), P_liar-{F}(V4,V3), P_truthteller-{F}(V4,V5), P_truthteller-{F}(V6,V5), P_liar-{F}(V6,V7), P_liar-{F}(V8,V7), P_truthteller-{F}(V8,V9), P_liar-{F}(V10,V9), P_truthteller-{F}(V10,V11), P_truthteller-{F}(V12,V11), P_liar-{F}(V12,V13), P_truthteller-{F}(V0,V13), P_truthteller-{F}(V14,V13), P_liar-{F}(V14,V1), P_liar-{F}(V0,V15), P_c-{F}(V16), P_liar-{F}(V16,V7) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #268: disj( #0, #91+#3 ), references = 1, size of lhs = 8:
% 1.75/1.97 P_truthteller-{F}(V0,V1), P_liar-{F}(V0,V2), P_truthteller-{F}(V3,V1), P_liar-{F}(V3,V4), P_truthteller-{F}(V5,V4), P_liar-{F}(V5,V6), P_liar-{F}(V7,V6), P_says-{F}(V7,V1,V6) | a_truth-{T}(V2)
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #274: disj( #0, #91+#91+#202 ), references = 1, size of lhs = 18:
% 1.75/1.97 P_a-{F}(V0), P_mumble-{F}(V1), P_says-{F}(V0,V1,V2), P_b-{F}(V3), P_liar-{F}(V3,V4), P_liar-{F}(V5,V4), P_truthteller-{F}(V5,V6), P_liar-{F}(V7,V6), P_truthteller-{F}(V7,V8), P_truthteller-{F}(V9,V8), P_liar-{F}(V9,V10), P_truthteller-{F}(V11,V8), P_liar-{F}(V11,V12), P_truthteller-{F}(V13,V12), P_liar-{F}(V13,V14), P_liar-{F}(V0,V15), P_c-{F}(V16), P_liar-{F}(V16,V14) | a_truth-{T}(V10)
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #279: exists( #12, #277 ), references = 1, size of lhs = 20:
% 1.75/1.97 P_a-{F}(V0), P_mumble-{F}(V1), P_b-{F}(V2), P_liar-{F}(V2,V3), P_liar-{F}(V4,V3), P_truthteller-{F}(V4,V5), P_liar-{F}(V6,V5), P_truthteller-{F}(V6,V7), P_truthteller-{F}(V8,V7), P_liar-{F}(V8,V9), P_truthteller-{F}(V0,V9), P_truthteller-{F}(V10,V7), P_liar-{F}(V10,V11), P_truthteller-{F}(V12,V11), P_liar-{F}(V12,V13), P_liar-{F}(V0,V14), P_c-{F}(V15), P_liar-{F}(V15,V13), P_liar-{F}(V16,V9), P_says-{F}(V16,V1,V9) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #281: exists( #11, #278 ), references = 1, size of lhs = 18:
% 1.75/1.97 P_a-{F}(V0), P_mumble-{F}(V1), P_b-{F}(V2), P_liar-{F}(V2,V3), P_liar-{F}(V4,V3), P_truthteller-{F}(V4,V5), P_liar-{F}(V6,V5), P_truthteller-{F}(V6,V7), P_truthteller-{F}(V8,V7), P_liar-{F}(V8,V9), P_truthteller-{F}(V0,V9), P_truthteller-{F}(V10,V7), P_liar-{F}(V10,V11), P_liar-{F}(V0,V12), P_c-{F}(V13), P_truthteller-{F}(V13,V11), P_liar-{F}(V14,V9), P_says-{F}(V14,V1,V9) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #284: disj( #0, input ), references = 2, size of lhs = 5:
% 1.75/1.97 a_truth-{F}(V0), P_liar-{F}(V1,V0), P_truthteller-{F}(V1,V2), P_liar-{F}(V3,V2), P_truthteller-{F}(V3,V4) | a_truth-{T}(V4)
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #291: disj( #0, input ), references = 1, size of lhs = 6:
% 1.75/1.97 a_truth-{F}(V0), P_liar-{F}(V1,V0), a_truth-{F}(V2), P_says-{F}(V1,V3,V2), P_truthteller-{F}(V4,V3), P_liar-{F}(V4,V5) | a_truth-{T}(V5)
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #294: exists( #11, #292 ), references = 2, size of lhs = 13:
% 1.75/1.97 a_truth-{F}(V0), P_liar-{F}(V1,V0), a_truth-{F}(V2), P_a-{F}(V3), P_mumble-{F}(V4), P_says-{F}(V3,V4,V5), P_b-{F}(V6), P_liar-{F}(V3,V7), P_c-{F}(V8), P_liar-{F}(V6,V9), a_truth-{F}(V9), P_truthteller-{F}(V8,V10), P_says-{F}(V1,V10,V2) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #304: disj( #0, #2+#3 ), references = 3, size of lhs = 7:
% 1.75/1.97 a_truth-{F}(V0), P_truthteller-{F}(V1,V2), P_liar-{F}(V1,V3), P_truthteller-{F}(V4,V3), P_says-{F}(V4,V5,V0), P_liar-{F}(V6,V3), P_says-{F}(V6,V5,V3) | a_truth-{T}(V2)
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #310: mergings( V4 == V12; #308 ), references = 1, size of lhs = 16:
% 1.75/1.97 P_a-{F}(V0), P_mumble-{F}(V1), P_b-{F}(V2), P_liar-{F}(V2,V3), P_liar-{F}(V0,V3), P_liar-{F}(V4,V3), P_truthteller-{F}(V4,V5), P_liar-{F}(V6,V5), P_truthteller-{F}(V6,V7), P_truthteller-{F}(V8,V7), P_liar-{F}(V8,V9), P_truthteller-{F}(V0,V9), P_liar-{F}(V10,V9), P_says-{F}(V10,V1,V9), P_c-{F}(V11), P_truthteller-{F}(V11,V1) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #326: exists( #12, #74 ), references = 2, size of lhs = 10:
% 1.75/1.97 P_a-{F}(V0), P_mumble-{F}(V1), P_says-{F}(V0,V1,V2), P_b-{F}(V3), P_liar-{F}(V0,V4), P_says-{F}(V0,V4,V5), P_c-{F}(V6), P_liar-{F}(V3,V7), P_truthteller-{F}(V6,V8), a_truth-{F}(V8) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #327: exists( #12, #9 ), references = 1, size of lhs = 11:
% 1.75/1.97 P_a-{F}(V0), P_mumble-{F}(V1), P_says-{F}(V0,V1,V2), P_b-{F}(V3), P_liar-{F}(V0,V4), P_says-{F}(V0,V4,V5), P_says-{F}(V3,V5,V6), P_c-{F}(V7), P_liar-{F}(V3,V8), P_truthteller-{F}(V7,V9), a_truth-{F}(V9) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #329: exists( #12, #324 ), references = 6, size of lhs = 9:
% 1.75/1.97 P_a-{F}(V0), P_mumble-{F}(V1), P_says-{F}(V0,V1,V2), P_b-{F}(V3), P_liar-{F}(V0,V4), P_c-{F}(V5), P_liar-{F}(V3,V6), P_truthteller-{F}(V5,V7), a_truth-{F}(V7) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #334: exists( #12, #332 ), references = 1, size of lhs = 12:
% 1.75/1.97 P_a-{F}(V0), P_mumble-{F}(V1), P_b-{F}(V2), P_liar-{F}(V0,V3), P_c-{F}(V4), P_liar-{F}(V2,V5), P_truthteller-{F}(V4,V6), P_truthteller-{F}(V7,V6), P_liar-{F}(V7,V8), P_truthteller-{F}(V0,V8), P_liar-{F}(V9,V8), P_says-{F}(V9,V1,V8) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #342: disj( #0, input ), references = 1, size of lhs = 6:
% 1.75/1.97 a_truth-{F}(V0), P_liar-{F}(V1,V0), a_truth-{F}(V2), P_says-{F}(V1,V3,V2), P_liar-{F}(V4,V3), P_truthteller-{F}(V4,V5) | a_truth-{T}(V5)
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #343: disj( #0, exists( #12, #199 ) ), references = 2, size of lhs = 11:
% 1.75/1.97 P_a-{F}(V0), P_mumble-{F}(V1), P_says-{F}(V0,V1,V2), P_b-{F}(V3), P_liar-{F}(V0,V4), P_c-{F}(V5), P_liar-{F}(V3,V6), a_truth-{F}(V6), P_liar-{F}(V5,V7), P_liar-{F}(V8,V7), P_truthteller-{F}(V8,V9) | a_truth-{T}(V9)
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #354: mergings( V2 == V9, V6 == V13, V3 == V10, V4 == V11, V5 == V12, V7 == V15, V0 == V14; #346 ), references = 3, size of lhs = 9:
% 1.75/1.97 a_truth-{F}(V0), P_a-{F}(V1), P_mumble-{F}(V2), P_says-{F}(V1,V2,V3), P_b-{F}(V4), P_liar-{F}(V4,V0), P_liar-{F}(V1,V5), P_c-{F}(V6), P_truthteller-{F}(V6,V7) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #371: exists( #12, #369 ), references = 1, size of lhs = 16:
% 1.75/1.97 P_a-{F}(V0), P_mumble-{F}(V1), P_b-{F}(V2), P_liar-{F}(V2,V3), P_liar-{F}(V4,V3), P_truthteller-{F}(V4,V5), P_liar-{F}(V6,V5), P_truthteller-{F}(V6,V7), P_truthteller-{F}(V8,V7), P_liar-{F}(V8,V9), P_truthteller-{F}(V0,V9), P_liar-{F}(V10,V9), P_says-{F}(V10,V1,V9), P_liar-{F}(V0,V11), P_c-{F}(V12), P_truthteller-{F}(V12,V13) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #373: exists( #10, #370 ), references = 1, size of lhs = 15:
% 1.75/1.97 P_a-{F}(V0), P_mumble-{F}(V1), P_b-{F}(V2), P_liar-{F}(V2,V3), P_liar-{F}(V4,V3), P_truthteller-{F}(V4,V5), P_liar-{F}(V6,V5), P_truthteller-{F}(V6,V7), P_truthteller-{F}(V8,V7), P_liar-{F}(V8,V9), P_truthteller-{F}(V0,V9), P_liar-{F}(V10,V9), P_says-{F}(V10,V1,V9), P_liar-{F}(V0,V11), P_c-{F}(V12) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #380: exists( #10, #354 ), references = 5, size of lhs = 8:
% 1.75/1.97 a_truth-{F}(V0), P_a-{F}(V1), P_mumble-{F}(V2), P_says-{F}(V1,V2,V3), P_b-{F}(V4), P_liar-{F}(V4,V0), P_liar-{F}(V1,V5), P_c-{F}(V6) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #395: disj( #0, #2+#3 ), references = 3, size of lhs = 7:
% 1.75/1.97 a_truth-{F}(V0), P_truthteller-{F}(V1,V2), P_liar-{F}(V1,V3), P_truthteller-{F}(V4,V3), P_liar-{F}(V5,V3), P_says-{F}(V5,V6,V6), P_says-{F}(V4,V6,V0) | a_truth-{T}(V2)
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #400: exists( #12, #398 ), references = 1, size of lhs = 15:
% 1.75/1.97 P_a-{F}(V0), P_mumble-{F}(V1), P_b-{F}(V2), P_liar-{F}(V2,V3), P_liar-{F}(V4,V3), P_truthteller-{F}(V4,V5), P_liar-{F}(V6,V5), P_truthteller-{F}(V6,V7), P_truthteller-{F}(V8,V7), P_liar-{F}(V8,V9), P_truthteller-{F}(V0,V9), P_liar-{F}(V10,V9), P_says-{F}(V10,V1,V1), P_liar-{F}(V0,V11), P_c-{F}(V12) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #433: exists( #12, #427 ), references = 1, size of lhs = 15:
% 1.75/1.97 P_a-{F}(V0), P_mumble-{F}(V1), P_says-{F}(V0,V1,V2), P_b-{F}(V3), P_liar-{F}(V0,V4), P_says-{F}(V0,V4,V5), P_c-{F}(V6), P_liar-{F}(V3,V7), P_says-{F}(V6,V7,V8), a_truth-{F}(V9), P_truthteller-{F}(V10,V9), a_truth-{F}(V11), P_truthteller-{F}(V12,V11), P_liar-{F}(V12,V13), P_says-{F}(V10,V13,V8) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #434: exists( #12, #428 ), references = 2, size of lhs = 16:
% 1.75/1.97 P_a-{F}(V0), P_mumble-{F}(V1), P_says-{F}(V0,V1,V2), P_b-{F}(V3), P_liar-{F}(V0,V4), P_says-{F}(V0,V4,V5), P_c-{F}(V6), P_liar-{F}(V3,V7), P_says-{F}(V6,V7,V8), a_truth-{F}(V9), P_truthteller-{F}(V10,V9), a_truth-{F}(V11), a_truth-{F}(V12), P_says-{F}(V13,V12,V11), P_liar-{F}(V13,V14), P_says-{F}(V10,V14,V8) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #442: mergings( V3 == V12, V6 == V17, V4 == V13, V5 == V14, V0 == V15, V8 == V16, V7 == V18; #432 ), references = 1, size of lhs = 12:
% 1.75/1.97 a_truth-{F}(V0), P_truthteller-{F}(V1,V0), P_a-{F}(V2), P_mumble-{F}(V3), P_says-{F}(V2,V3,V4), P_b-{F}(V5), P_liar-{F}(V5,V6), P_says-{F}(V1,V6,V7), P_liar-{F}(V2,V8), P_says-{F}(V2,V8,V9), P_c-{F}(V10), P_says-{F}(V10,V6,V7) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #462: exists( #12, #456 ), references = 1, size of lhs = 11:
% 1.75/1.97 P_a-{F}(V0), P_mumble-{F}(V1), P_says-{F}(V0,V1,V2), P_b-{F}(V3), P_liar-{F}(V0,V4), P_says-{F}(V0,V4,V5), a_truth-{F}(V6), P_truthteller-{F}(V3,V6), a_truth-{F}(V7), P_liar-{F}(V8,V7), P_says-{F}(V8,V5,V5) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #463: exists( #12, #457 ), references = 1, size of lhs = 14:
% 1.75/1.97 P_a-{F}(V0), P_mumble-{F}(V1), P_says-{F}(V0,V1,V2), P_b-{F}(V3), P_liar-{F}(V0,V4), P_says-{F}(V0,V4,V5), a_truth-{F}(V6), P_liar-{F}(V7,V6), P_truthteller-{F}(V7,V8), P_truthteller-{F}(V9,V8), P_liar-{F}(V9,V10), P_truthteller-{F}(V3,V10), P_liar-{F}(V11,V10), P_says-{F}(V11,V5,V5) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #469: mergings( V3 == V7, V6 == V11, V4 == V8, V5 == V9, V0 == V10; #461 ), references = 1, size of lhs = 14:
% 1.75/1.97 P_a-{F}(V0), P_mumble-{F}(V1), P_says-{F}(V0,V1,V2), P_b-{F}(V3), P_liar-{F}(V0,V4), P_says-{F}(V0,V4,V5), P_c-{F}(V6), P_liar-{F}(V3,V7), P_truthteller-{F}(V6,V8), P_truthteller-{F}(V9,V8), P_liar-{F}(V9,V10), P_truthteller-{F}(V3,V10), P_liar-{F}(V11,V10), P_says-{F}(V11,V5,V5) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #484: exists( #12, #480 ), references = 2, size of lhs = 12:
% 1.75/1.97 P_a-{F}(V0), P_mumble-{F}(V1), P_says-{F}(V0,V1,V2), P_b-{F}(V3), P_liar-{F}(V0,V4), P_says-{F}(V0,V4,V5), a_truth-{F}(V6), P_truthteller-{F}(V3,V6), a_truth-{F}(V7), P_liar-{F}(V8,V7), P_says-{F}(V8,V5,V9), a_truth-{F}(V9) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #491: mergings( V3 == V8, V6 == V12, V1 == V13, V4 == V9, V5 == V10, V0 == V11; #483 ), references = 1, size of lhs = 14:
% 1.75/1.97 a_truth-{F}(V0), P_a-{F}(V1), P_mumble-{F}(V2), P_says-{F}(V1,V2,V3), P_b-{F}(V4), P_truthteller-{F}(V4,V0), P_liar-{F}(V1,V5), P_says-{F}(V1,V5,V6), P_c-{F}(V7), P_liar-{F}(V4,V8), P_says-{F}(V7,V8,V9), a_truth-{F}(V10), P_liar-{F}(V11,V10), P_says-{F}(V11,V6,V9) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #516: exists( #12, #510 ), references = 1, size of lhs = 14:
% 1.75/1.97 P_a-{F}(V0), P_mumble-{F}(V1), P_says-{F}(V0,V1,V2), P_b-{F}(V3), P_liar-{F}(V0,V4), P_says-{F}(V0,V4,V5), a_truth-{F}(V6), P_truthteller-{F}(V3,V6), a_truth-{F}(V7), P_truthteller-{F}(V8,V7), a_truth-{F}(V9), P_truthteller-{F}(V10,V9), P_liar-{F}(V10,V11), P_says-{F}(V8,V11,V5) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #517: exists( #12, #511 ), references = 1, size of lhs = 15:
% 1.75/1.97 P_a-{F}(V0), P_mumble-{F}(V1), P_says-{F}(V0,V1,V2), P_b-{F}(V3), P_liar-{F}(V0,V4), P_says-{F}(V0,V4,V5), a_truth-{F}(V6), P_truthteller-{F}(V3,V6), a_truth-{F}(V7), P_truthteller-{F}(V8,V7), a_truth-{F}(V9), a_truth-{F}(V10), P_says-{F}(V11,V10,V9), P_liar-{F}(V11,V12), P_says-{F}(V8,V12,V5) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #524: mergings( V3 == V10, V6 == V14, V4 == V11, V5 == V12, V0 == V13, V7 == V15; #515 ), references = 1, size of lhs = 12:
% 1.75/1.97 a_truth-{F}(V0), P_truthteller-{F}(V1,V0), P_a-{F}(V2), P_mumble-{F}(V3), P_says-{F}(V2,V3,V4), P_b-{F}(V5), P_liar-{F}(V2,V6), P_says-{F}(V2,V6,V7), a_truth-{F}(V8), P_truthteller-{F}(V5,V8), P_liar-{F}(V5,V9), P_says-{F}(V1,V9,V7) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #528: exists( #12, #513 ), references = 5, size of lhs = 12:
% 1.75/1.97 P_a-{F}(V0), P_mumble-{F}(V1), P_says-{F}(V0,V1,V2), P_b-{F}(V3), P_liar-{F}(V0,V4), a_truth-{F}(V5), P_truthteller-{F}(V3,V5), a_truth-{F}(V6), P_truthteller-{F}(V0,V6), a_truth-{F}(V7), P_truthteller-{F}(V8,V7), P_liar-{F}(V8,V4) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #529: exists( #12, #514 ), references = 4, size of lhs = 13:
% 1.75/1.97 P_a-{F}(V0), P_mumble-{F}(V1), P_says-{F}(V0,V1,V2), P_b-{F}(V3), P_liar-{F}(V0,V4), a_truth-{F}(V5), P_truthteller-{F}(V3,V5), a_truth-{F}(V6), P_truthteller-{F}(V0,V6), a_truth-{F}(V7), a_truth-{F}(V8), P_says-{F}(V9,V8,V7), P_liar-{F}(V9,V4) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #534: mergings( V3 == V8, V4 == V9, V5 == V10, V6 == V11; #527 ), references = 2, size of lhs = 10:
% 1.75/1.97 a_truth-{F}(V0), P_a-{F}(V1), P_truthteller-{F}(V1,V0), P_mumble-{F}(V2), P_says-{F}(V1,V2,V3), P_b-{F}(V4), P_liar-{F}(V1,V5), P_liar-{F}(V4,V5), a_truth-{F}(V6), P_truthteller-{F}(V4,V6) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #561: disj( #0, mergings( V3 == V8, V4 == V9, V5 == V10, V6 == V11; #527 ) ), references = 1, size of lhs = 10:
% 1.75/1.97 P_a-{F}(V0), P_truthteller-{F}(V0,V1), P_liar-{F}(V2,V1), P_truthteller-{F}(V2,V3), P_mumble-{F}(V4), P_says-{F}(V0,V4,V5), P_b-{F}(V6), P_truthteller-{F}(V6,V1), P_liar-{F}(V0,V7), P_liar-{F}(V6,V7) | a_truth-{T}(V3)
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #562: disj( #0, exists( #12, #513 ) ), references = 1, size of lhs = 11:
% 1.75/1.97 P_a-{F}(V0), P_mumble-{F}(V1), P_says-{F}(V0,V1,V2), P_b-{F}(V3), P_liar-{F}(V0,V4), P_truthteller-{F}(V3,V5), P_truthteller-{F}(V0,V5), P_liar-{F}(V6,V5), P_truthteller-{F}(V6,V7), P_truthteller-{F}(V8,V5), P_liar-{F}(V8,V4) | a_truth-{T}(V7)
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #563: disj( #0, input ), references = 1, size of lhs = 4:
% 1.75/1.97 P_truthteller-{F}(V0,V1), P_liar-{F}(V0,V2), P_liar-{F}(V3,V2), P_says-{F}(V3,V2,V2) | a_truth-{T}(V1)
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #575: mergings( V7 == V13, V6 == V12, V13 == V11; #570 ), references = 1, size of lhs = 14:
% 1.75/1.97 P_a-{F}(V0), P_truthteller-{F}(V0,V1), P_liar-{F}(V2,V1), P_truthteller-{F}(V2,V3), P_truthteller-{F}(V4,V3), P_liar-{F}(V4,V5), P_truthteller-{F}(V6,V5), P_liar-{F}(V6,V7), P_liar-{F}(V0,V7), P_mumble-{F}(V8), P_b-{F}(V9), P_truthteller-{F}(V9,V1), P_liar-{F}(V9,V7), P_c-{F}(V10) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #578: mergings( V6 == V2; #576 ), references = 1, size of lhs = 9:
% 1.75/1.97 P_a-{F}(V0), P_b-{F}(V0), P_truthteller-{F}(V0,V1), P_liar-{F}(V2,V1), P_truthteller-{F}(V2,V3), P_truthteller-{F}(V4,V3), P_liar-{F}(V4,V1), P_mumble-{F}(V5), P_c-{F}(V6) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #580: exists( #12, #380 ), references = 2, size of lhs = 7:
% 1.75/1.97 a_truth-{F}(V0), P_a-{F}(V1), P_mumble-{F}(V2), P_b-{F}(V3), P_liar-{F}(V3,V0), P_liar-{F}(V1,V4), P_c-{F}(V5) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #603: disj( #0, #119+#1 ), references = 1, size of lhs = 8:
% 1.75/1.97 P_truthteller-{F}(V0,V1), P_liar-{F}(V0,V2), P_liar-{F}(V3,V2), P_liar-{F}(V4,V2), P_truthteller-{F}(V4,V5), P_liar-{F}(V6,V5), P_truthteller-{F}(V6,V7), P_says-{F}(V3,V7,V7) | a_truth-{T}(V1)
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #604: disj( #0, #284+#3 ), references = 1, size of lhs = 8:
% 1.75/1.97 P_truthteller-{F}(V0,V1), P_liar-{F}(V0,V2), P_liar-{F}(V3,V2), P_truthteller-{F}(V3,V4), P_liar-{F}(V5,V4), P_truthteller-{F}(V5,V6), P_liar-{F}(V7,V2), P_says-{F}(V7,V6,V6) | a_truth-{T}(V1)
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #605: disj( #0, #119+#580 ), references = 2, size of lhs = 12:
% 1.75/1.97 P_a-{F}(V0), P_mumble-{F}(V1), P_b-{F}(V2), P_liar-{F}(V2,V3), P_liar-{F}(V4,V3), P_truthteller-{F}(V4,V5), P_says-{F}(V6,V5,V5), P_liar-{F}(V6,V7), P_liar-{F}(V8,V7), P_truthteller-{F}(V8,V9), P_liar-{F}(V0,V10), P_c-{F}(V11) | a_truth-{T}(V9)
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #615: disj( #0, exists( #12, #380 ) ), references = 1, size of lhs = 8:
% 1.75/1.97 P_a-{F}(V0), P_mumble-{F}(V1), P_b-{F}(V2), P_liar-{F}(V2,V3), P_truthteller-{F}(V4,V3), P_liar-{F}(V4,V5), P_liar-{F}(V0,V6), P_c-{F}(V7) | a_truth-{T}(V5)
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #616: disj( #0, input ), references = 1, size of lhs = 5:
% 1.75/1.97 a_truth-{F}(V0), P_truthteller-{F}(V1,V2), P_liar-{F}(V1,V3), P_liar-{F}(V4,V2), P_says-{F}(V4,V2,V0) | a_truth-{T}(V3)
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #619: exists( #12, #534 ), references = 2, size of lhs = 9:
% 1.75/1.97 a_truth-{F}(V0), P_a-{F}(V1), P_truthteller-{F}(V1,V0), P_mumble-{F}(V2), P_b-{F}(V3), P_liar-{F}(V1,V4), P_liar-{F}(V3,V4), a_truth-{F}(V5), P_truthteller-{F}(V3,V5) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #620: exists( #12, #528 ), references = 6, size of lhs = 11:
% 1.75/1.97 P_a-{F}(V0), P_mumble-{F}(V1), P_b-{F}(V2), P_liar-{F}(V0,V3), a_truth-{F}(V4), P_truthteller-{F}(V2,V4), a_truth-{F}(V5), P_truthteller-{F}(V0,V5), a_truth-{F}(V6), P_truthteller-{F}(V7,V6), P_liar-{F}(V7,V3) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #628: disj( #0, exists( #12, #380 ) ), references = 11, size of lhs = 8:
% 1.75/1.97 P_a-{F}(V0), P_mumble-{F}(V1), P_b-{F}(V2), P_liar-{F}(V2,V3), P_liar-{F}(V4,V3), P_truthteller-{F}(V4,V5), P_liar-{F}(V0,V6), P_c-{F}(V7) | a_truth-{T}(V5)
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #634: mergings( V2 == V5; #631 ), references = 1, size of lhs = 5:
% 1.75/1.97 P_c-{F}(V0), P_a-{F}(V1), P_b-{F}(V1), P_mumble-{F}(V2), P_truthteller-{F}(V1,V3) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #638: mergings( V2 == V4; #635 ), references = 1, size of lhs = 4:
% 1.75/1.97 P_c-{F}(V0), P_a-{F}(V1), P_b-{F}(V1), P_mumble-{F}(V2) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #642: mergings( V1 == V3; #639 ), references = 1, size of lhs = 3:
% 1.75/1.97 P_a-{F}(V0), P_b-{F}(V0), P_mumble-{F}(V1) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #658: mergings( V4 == V9, V2 == V7, V5 == V14, V7 == V16, V14 == V19, V3 == V8, V8 == V17, V0 == V18, V6 == V15; #648 ), references = 1, size of lhs = 13:
% 1.75/1.97 P_c-{F}(V0), P_a-{F}(V1), P_truthteller-{F}(V1,V2), P_truthteller-{F}(V3,V2), P_liar-{F}(V3,V4), P_liar-{F}(V5,V4), P_mumble-{F}(V6), P_b-{F}(V7), P_truthteller-{F}(V7,V8), P_says-{F}(V5,V8,V8), P_liar-{F}(V1,V9), P_truthteller-{F}(V10,V2), P_liar-{F}(V10,V9) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #677: mergings( V2 == V7, V5 == V10, V3 == V8, V0 == V9; #671 ), references = 1, size of lhs = 9:
% 1.75/1.97 P_c-{F}(V0), P_a-{F}(V1), P_truthteller-{F}(V1,V2), P_mumble-{F}(V3), P_b-{F}(V4), P_truthteller-{F}(V4,V2), P_liar-{F}(V1,V5), P_truthteller-{F}(V6,V2), P_liar-{F}(V6,V5) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #687: exists( #11, #329 ), references = 4, size of lhs = 8:
% 1.75/1.97 P_a-{F}(V0), P_mumble-{F}(V1), P_says-{F}(V0,V1,V2), P_b-{F}(V3), P_liar-{F}(V0,V4), P_c-{F}(V5), P_truthteller-{F}(V5,V6), a_truth-{F}(V6) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #688: exists( #11, #326 ), references = 3, size of lhs = 9:
% 1.75/1.97 P_a-{F}(V0), P_mumble-{F}(V1), P_says-{F}(V0,V1,V2), P_b-{F}(V3), P_liar-{F}(V0,V4), P_says-{F}(V0,V4,V5), P_c-{F}(V6), P_truthteller-{F}(V6,V7), a_truth-{F}(V7) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #704: mergings( V2 == V7, V5 == V10, V3 == V8, V6 == V11; #698 ), references = 1, size of lhs = 8:
% 1.75/1.97 P_a-{F}(V0), P_mumble-{F}(V1), P_says-{F}(V0,V1,V2), P_b-{F}(V3), P_truthteller-{F}(V3,V4), P_liar-{F}(V0,V5), P_c-{F}(V6), P_truthteller-{F}(V6,V4) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #710: mergings( V2 == V7, V5 == V11, V3 == V8, V0 == V10, V6 == V12; #697 ), references = 1, size of lhs = 8:
% 1.75/1.97 P_a-{F}(V0), P_mumble-{F}(V1), P_says-{F}(V0,V1,V2), P_b-{F}(V3), P_truthteller-{F}(V3,V4), P_liar-{F}(V0,V5), P_c-{F}(V6), P_truthteller-{F}(V6,V4) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #716: mergings( V2 == V7, V5 == V11, V3 == V8, V0 == V10, V6 == V13; #699 ), references = 1, size of lhs = 9:
% 1.75/1.97 P_a-{F}(V0), P_mumble-{F}(V1), P_says-{F}(V0,V1,V2), P_b-{F}(V3), P_truthteller-{F}(V3,V4), P_liar-{F}(V0,V5), P_says-{F}(V0,V5,V6), P_c-{F}(V7), P_truthteller-{F}(V7,V4) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #724: mergings( V3 == V0, V5 == V9, V4 == V1, V6 == V10; #717 ), references = 1, size of lhs = 7:
% 1.75/1.97 P_a-{F}(V0), P_mumble-{F}(V1), P_b-{F}(V2), P_truthteller-{F}(V2,V3), P_liar-{F}(V0,V4), P_c-{F}(V5), P_truthteller-{F}(V5,V3) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #732: mergings( V2 == V6, V4 == V8, V3 == V7, V5 == V0; #725 ), references = 1, size of lhs = 5:
% 1.75/1.97 P_a-{F}(V0), P_mumble-{F}(V1), P_b-{F}(V2), P_c-{F}(V2), P_liar-{F}(V0,V3) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #737: mergings( V2 == V4, V3 == V5; #733 ), references = 1, size of lhs = 4:
% 1.75/1.97 P_a-{F}(V0), P_mumble-{F}(V1), P_b-{F}(V2), P_c-{F}(V2) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #753: exists( #12, #749 ), references = 1, size of lhs = 12:
% 1.75/1.97 P_a-{F}(V0), P_mumble-{F}(V1), P_says-{F}(V0,V1,V2), P_b-{F}(V3), P_liar-{F}(V0,V4), P_says-{F}(V0,V4,V5), a_truth-{F}(V6), P_truthteller-{F}(V3,V6), a_truth-{F}(V7), P_liar-{F}(V8,V7), a_truth-{F}(V9), P_says-{F}(V8,V9,V5) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #760: mergings( V3 == V8, V6 == V12, V1 == V13, V4 == V9, V5 == V10, V0 == V11; #752 ), references = 1, size of lhs = 17:
% 1.75/1.97 a_truth-{F}(V0), P_a-{F}(V1), P_mumble-{F}(V2), P_says-{F}(V1,V2,V3), P_b-{F}(V4), P_truthteller-{F}(V4,V0), P_liar-{F}(V1,V5), P_says-{F}(V1,V5,V6), P_c-{F}(V7), P_liar-{F}(V4,V8), P_says-{F}(V7,V8,V9), a_truth-{F}(V10), P_truthteller-{F}(V11,V10), a_truth-{F}(V12), P_says-{F}(V13,V12,V6), P_liar-{F}(V13,V14), P_says-{F}(V11,V14,V9) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #764: mergings( V1 == V7; #761 ), references = 2, size of lhs = 8:
% 1.75/1.97 P_a-{F}(V0), P_mumble-{F}(V1), P_says-{F}(V0,V1,V2), P_b-{F}(V3), a_truth-{F}(V4), P_truthteller-{F}(V3,V4), a_truth-{F}(V5), P_liar-{F}(V0,V5) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #774: mergings( V2 == V7, V5 == V11, V3 == V8, V0 == V10; #769 ), references = 1, size of lhs = 8:
% 1.75/1.97 P_c-{F}(V0), P_a-{F}(V1), P_mumble-{F}(V2), P_says-{F}(V1,V2,V3), P_b-{F}(V4), P_truthteller-{F}(V4,V5), a_truth-{F}(V6), P_liar-{F}(V1,V6) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #779: mergings( V2 == V6, V4 == V9, V3 == V7; #775 ), references = 2, size of lhs = 7:
% 1.75/1.97 P_c-{F}(V0), P_a-{F}(V1), P_mumble-{F}(V2), P_says-{F}(V1,V2,V3), P_b-{F}(V4), a_truth-{F}(V5), P_liar-{F}(V1,V5) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #787: disj( #0, mergings( V2 == V6, V4 == V9, V3 == V7; #775 ) ), references = 14, size of lhs = 8:
% 1.75/1.97 P_c-{F}(V0), P_a-{F}(V1), P_mumble-{F}(V2), P_says-{F}(V1,V2,V3), P_b-{F}(V4), P_liar-{F}(V1,V5), P_liar-{F}(V6,V5), P_truthteller-{F}(V6,V7) | a_truth-{T}(V7)
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #794: mergings( V5 == V10, V4 == V9, V3 == V11; #790 ), references = 1, size of lhs = 10:
% 1.75/1.97 P_a-{F}(V0), P_mumble-{F}(V1), P_b-{F}(V2), P_liar-{F}(V0,V3), P_liar-{F}(V4,V3), P_truthteller-{F}(V4,V5), P_truthteller-{F}(V6,V5), P_c-{F}(V7), P_truthteller-{F}(V7,V8), P_says-{F}(V6,V8,V5) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #806: mergings( V5 == V9, V4 == V8, V3 == V10; #801 ), references = 1, size of lhs = 8:
% 1.75/1.97 P_a-{F}(V0), P_mumble-{F}(V1), P_b-{F}(V2), P_liar-{F}(V0,V3), P_liar-{F}(V4,V3), P_truthteller-{F}(V4,V5), P_c-{F}(V6), P_truthteller-{F}(V6,V5) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #810: mergings( V5 == V1, V4 == V8, V3 == V9; #802 ), references = 1, size of lhs = 8:
% 1.75/1.97 P_a-{F}(V0), P_mumble-{F}(V1), P_liar-{F}(V0,V1), P_liar-{F}(V2,V1), P_truthteller-{F}(V2,V3), P_b-{F}(V4), P_c-{F}(V5), P_truthteller-{F}(V5,V3) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #814: mergings( V3 == V6, V2 == V7; #811 ), references = 1, size of lhs = 6:
% 1.75/1.97 P_a-{F}(V0), P_truthteller-{F}(V0,V1), P_mumble-{F}(V2), P_b-{F}(V3), P_c-{F}(V4), P_truthteller-{F}(V4,V1) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #818: mergings( V3 == V5, V2 == V0; #815 ), references = 1, size of lhs = 4:
% 1.75/1.97 P_a-{F}(V0), P_c-{F}(V0), P_mumble-{F}(V1), P_b-{F}(V2) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #828: exists( #12, #822 ), references = 1, size of lhs = 11:
% 1.75/1.97 P_c-{F}(V0), P_a-{F}(V1), P_mumble-{F}(V2), P_b-{F}(V3), P_liar-{F}(V1,V4), P_liar-{F}(V5,V4), P_truthteller-{F}(V5,V6), P_truthteller-{F}(V7,V6), P_truthteller-{F}(V8,V6), P_liar-{F}(V8,V9), P_says-{F}(V7,V9,V6) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #832: mergings( V5 == V11, V4 == V10, V3 == V9; #827 ), references = 1, size of lhs = 9:
% 1.75/1.97 P_c-{F}(V0), P_a-{F}(V1), P_mumble-{F}(V2), P_b-{F}(V3), P_liar-{F}(V1,V4), P_liar-{F}(V5,V4), P_truthteller-{F}(V5,V6), P_truthteller-{F}(V7,V6), P_says-{F}(V7,V4,V6) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #847: mergings( V5 == V9, V4 == V8; #844 ), references = 1, size of lhs = 9:
% 1.75/1.97 P_c-{F}(V0), P_a-{F}(V1), P_truthteller-{F}(V1,V2), P_truthteller-{F}(V3,V2), P_liar-{F}(V3,V4), P_liar-{F}(V1,V4), P_mumble-{F}(V5), P_b-{F}(V6), P_truthteller-{F}(V6,V5) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #850: mergings( V5 == V9, V4 == V8; #843 ), references = 1, size of lhs = 11:
% 1.75/1.97 P_c-{F}(V0), P_a-{F}(V1), P_truthteller-{F}(V1,V2), P_truthteller-{F}(V3,V2), P_liar-{F}(V3,V4), P_liar-{F}(V1,V4), P_mumble-{F}(V5), P_b-{F}(V6), P_truthteller-{F}(V6,V5), P_truthteller-{F}(V7,V2), P_liar-{F}(V7,V4) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #855: mergings( V0 == V8, V5 == V11, V1 == V9, V4 == V10; #842 ), references = 1, size of lhs = 11:
% 1.75/1.97 P_c-{F}(V0), P_a-{F}(V1), P_truthteller-{F}(V1,V2), P_truthteller-{F}(V3,V2), P_liar-{F}(V3,V4), P_liar-{F}(V1,V4), P_mumble-{F}(V5), P_b-{F}(V6), P_truthteller-{F}(V6,V5), P_truthteller-{F}(V7,V2), P_liar-{F}(V7,V4) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #883: mergings( V5 == V10, V4 == V9; #879 ), references = 1, size of lhs = 13:
% 1.75/1.97 P_c-{F}(V0), P_a-{F}(V1), P_truthteller-{F}(V1,V2), P_truthteller-{F}(V3,V2), P_liar-{F}(V3,V4), P_liar-{F}(V1,V4), P_truthteller-{F}(V5,V2), P_mumble-{F}(V6), P_b-{F}(V7), P_truthteller-{F}(V7,V8), P_says-{F}(V5,V8,V2), P_truthteller-{F}(V9,V2), P_liar-{F}(V9,V4) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #888: mergings( V0 == V9, V5 == V12, V1 == V10, V4 == V11; #878 ), references = 1, size of lhs = 13:
% 1.75/1.97 P_c-{F}(V0), P_a-{F}(V1), P_truthteller-{F}(V1,V2), P_truthteller-{F}(V3,V2), P_liar-{F}(V3,V4), P_liar-{F}(V1,V4), P_truthteller-{F}(V5,V2), P_mumble-{F}(V6), P_b-{F}(V7), P_truthteller-{F}(V7,V8), P_says-{F}(V5,V8,V2), P_truthteller-{F}(V9,V2), P_liar-{F}(V9,V4) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #891: mergings( V5 == V10, V4 == V9; #880 ), references = 1, size of lhs = 13:
% 1.75/1.97 P_c-{F}(V0), P_a-{F}(V1), P_truthteller-{F}(V1,V2), P_truthteller-{F}(V3,V2), P_liar-{F}(V3,V4), P_liar-{F}(V1,V4), P_truthteller-{F}(V5,V2), P_mumble-{F}(V6), P_b-{F}(V7), P_truthteller-{F}(V7,V8), P_says-{F}(V5,V8,V2), P_says-{F}(V9,V8,V2), P_liar-{F}(V9,V4) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #909: mergings( V2 == V7, V5 == V10, V3 == V8, V0 == V9; #902 ), references = 1, size of lhs = 11:
% 1.75/1.97 P_c-{F}(V0), P_a-{F}(V1), P_mumble-{F}(V2), P_b-{F}(V3), P_truthteller-{F}(V3,V4), P_liar-{F}(V1,V5), a_truth-{F}(V6), P_truthteller-{F}(V1,V6), a_truth-{F}(V7), P_truthteller-{F}(V8,V7), P_liar-{F}(V8,V5) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #914: mergings( V2 == V7, V5 == V11, V3 == V8, V0 == V10; #903 ), references = 1, size of lhs = 12:
% 1.75/1.97 P_c-{F}(V0), P_a-{F}(V1), P_mumble-{F}(V2), P_says-{F}(V1,V2,V3), P_b-{F}(V4), P_truthteller-{F}(V4,V5), P_liar-{F}(V1,V6), a_truth-{F}(V7), P_truthteller-{F}(V1,V7), a_truth-{F}(V8), P_truthteller-{F}(V9,V8), P_liar-{F}(V9,V6) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #919: mergings( V2 == V7, V5 == V11, V3 == V8, V0 == V10; #904 ), references = 1, size of lhs = 13:
% 1.75/1.97 P_c-{F}(V0), P_a-{F}(V1), P_mumble-{F}(V2), P_says-{F}(V1,V2,V3), P_b-{F}(V4), P_truthteller-{F}(V4,V5), P_liar-{F}(V1,V6), a_truth-{F}(V7), P_truthteller-{F}(V1,V7), a_truth-{F}(V8), a_truth-{F}(V9), P_says-{F}(V10,V9,V8), P_liar-{F}(V10,V6) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #935: mergings( V5 == V15, V8 == V0, V12 == V15, V9 == V1, V4 == V10, V10 == V14, V3 == V13; #927 ), references = 1, size of lhs = 9:
% 1.75/1.97 P_c-{F}(V0), P_a-{F}(V1), P_truthteller-{F}(V1,V2), P_truthteller-{F}(V3,V2), P_liar-{F}(V3,V4), P_liar-{F}(V1,V4), P_mumble-{F}(V5), P_b-{F}(V6), P_truthteller-{F}(V6,V7) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #943: mergings( V5 == V15, V8 == V0, V12 == V15, V9 == V1, V4 == V10, V10 == V14, V3 == V13; #926 ), references = 1, size of lhs = 11:
% 1.75/1.97 P_c-{F}(V0), P_a-{F}(V1), P_truthteller-{F}(V1,V2), P_truthteller-{F}(V3,V2), P_liar-{F}(V3,V4), P_liar-{F}(V1,V4), P_mumble-{F}(V5), P_b-{F}(V6), P_truthteller-{F}(V6,V7), P_truthteller-{F}(V8,V2), P_liar-{F}(V8,V4) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #953: mergings( V0 == V8, V5 == V12, V8 == V14, V12 == V17, V1 == V9, V9 == V15, V4 == V10, V10 == V16, V3 == V13; #925 ), references = 1, size of lhs = 11:
% 1.75/1.97 P_c-{F}(V0), P_a-{F}(V1), P_truthteller-{F}(V1,V2), P_truthteller-{F}(V3,V2), P_liar-{F}(V3,V4), P_liar-{F}(V1,V4), P_mumble-{F}(V5), P_b-{F}(V6), P_truthteller-{F}(V6,V7), P_truthteller-{F}(V8,V2), P_liar-{F}(V8,V4) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #963: mergings( V9 == V13, V4 == V8, V6 == V13, V5 == V12, V3 == V0, V2 == V7; #954 ), references = 1, size of lhs = 8:
% 1.75/1.97 P_c-{F}(V0), P_a-{F}(V1), P_truthteller-{F}(V1,V2), P_truthteller-{F}(V3,V2), P_liar-{F}(V3,V4), P_liar-{F}(V1,V4), P_mumble-{F}(V5), P_b-{F}(V6) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #970: mergings( V9 == V13, V4 == V8, V6 == V13, V5 == V12, V3 == V0, V2 == V7; #955 ), references = 1, size of lhs = 10:
% 1.75/1.97 P_c-{F}(V0), P_a-{F}(V1), P_truthteller-{F}(V1,V2), P_truthteller-{F}(V3,V2), P_liar-{F}(V3,V4), P_liar-{F}(V1,V4), P_mumble-{F}(V5), P_b-{F}(V6), P_truthteller-{F}(V7,V2), P_liar-{F}(V7,V4) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #979: mergings( V3 == V9, V6 == V11, V9 == V13, V11 == V15, V4 == V10, V10 == V14, V5 == V0, V2 == V12; #956 ), references = 1, size of lhs = 10:
% 1.75/1.97 P_c-{F}(V0), P_a-{F}(V1), P_truthteller-{F}(V1,V2), P_truthteller-{F}(V3,V2), P_liar-{F}(V3,V4), P_liar-{F}(V1,V4), P_mumble-{F}(V5), P_b-{F}(V6), P_truthteller-{F}(V7,V2), P_liar-{F}(V7,V4) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #986: mergings( V4 == V7, V3 == V8, V2 == V5; #980 ), references = 1, size of lhs = 5:
% 1.75/1.97 P_c-{F}(V0), P_a-{F}(V1), P_truthteller-{F}(V1,V2), P_mumble-{F}(V3), P_b-{F}(V4) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #993: mergings( V4 == V6, V3 == V7, V2 == V5; #987 ), references = 1, size of lhs = 4:
% 1.75/1.97 P_c-{F}(V0), P_a-{F}(V1), P_mumble-{F}(V2), P_b-{F}(V3) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #999: mergings( V2 == V4, V1 == V5; #994 ), references = 1, size of lhs = 3:
% 1.75/1.97 P_a-{F}(V0), P_mumble-{F}(V1), P_b-{F}(V2) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #1004: mergings( V1 == V3; #1000 ), references = 1, size of lhs = 2:
% 1.75/1.97 P_a-{F}(V0), P_mumble-{F}(V1) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #1008: exists( #14, #1000 ), references = 1, size of lhs = 1:
% 1.75/1.97 P_a-{F}(V0) | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 #1012: exists( #13, #1005 ), references = 1, size of lhs = 0:
% 1.75/1.97 FALSE | FALSE
% 1.75/1.97 (used 0 times, uses = {})
% 1.75/1.97
% 1.75/1.97 number of learnt formulas = 134
% 1.75/1.97
% 1.75/1.97
% 1.75/1.97 % SZS output end Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.75/1.97
% 1.75/1.97 randbase = 1
%------------------------------------------------------------------------------