Bob is blue. Bob is cold. Bob is quiet. Bob is round. Charlie is blue. Charlie is cold. Charlie is furry. Charlie is quiet. Charlie is round. Charlie is young. White, blue people are quiet. All furry people are cold. If Charlie is round and Charlie is white then Charlie is blue. Quiet, blue people are furry. If someone is quiet then they are blue. Young people are cold. All furry, round people are quiet. If Charlie is young then Charlie is cold.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is round.
("Bob" "is" "round" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is young.
("Charlie" "is" "young" "+")
White, blue people are quiet.
((("someone" "is" "white" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "quiet" "+"))
All furry people are cold.
((("someone" "is" "furry" "+")) -> ("someone" "is" "cold" "+"))
If Charlie is round and Charlie is white then Charlie is blue.
((("Charlie" "is" "round" "+") ("Charlie" "is" "white" "+")) -> ("Charlie" "is" "blue" "+"))
Quiet, blue people are furry.
((("someone" "is" "quiet" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "furry" "+"))
If someone is quiet then they are blue.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "blue" "+"))
Young people are cold.
((("someone" "is" "young" "+")) -> ("someone" "is" "cold" "+"))
All furry, round people are quiet.
((("someone" "is" "furry" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "quiet" "+"))
If Charlie is young then Charlie is cold.
((("Charlie" "is" "young" "+")) -> ("Charlie" "is" "cold" "+"))
Charlie is cold.
True
1
proof
[(triple6 OR ((triple10) -> rule6) OR ((triple10) -> rule8) OR ((triple7) -> rule2) OR ((((triple8 triple5) -> rule4)) -> rule2) OR ((((triple8 ((triple8) -> rule5)) -> rule4)) -> rule2))]
("Charlie" "is" "cold" "+")
triple6
((triple10) -> (rule6 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
((triple10) -> (rule8 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
((triple7) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
((((triple8 triple5) -> (rule4 % int2))) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
((((triple8 ((triple8) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Bob is not quiet.
False
1
inv-proof
[(triple3)]
("Bob" "is" "quiet" "-")
triple3
Charlie is not white.
Unknown
inv-random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "-")
Bob is white.
Unknown
random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "+")
@0: Bob is blue.[(triple1 OR ((triple3) -> rule5))] Bob is cold.[(triple2 OR ((((triple3 triple1) -> rule4)) -> rule2) OR ((((triple3 ((triple3) -> rule5)) -> rule4)) -> rule2))] Bob is quiet.[(triple3)] Bob is round.[(triple4)] Charlie is blue.[(triple5 OR ((triple8) -> rule5) OR ((((triple7 triple9) -> rule7)) -> rule5))] Charlie is cold.[(triple6 OR ((triple10) -> rule6) OR ((triple10) -> rule8) OR ((triple7) -> rule2) OR ((((triple8 triple5) -> rule4)) -> rule2) OR ((((triple8 ((triple8) -> rule5)) -> rule4)) -> rule2))] Charlie is furry.[(triple7 OR ((triple8 triple5) -> rule4) OR ((triple8 ((triple8) -> rule5)) -> rule4))] Charlie is quiet.[(triple8 OR ((triple7 triple9) -> rule7))] Charlie is round.[(triple9)] Charlie is young.[(triple10)] @1: Bob is furry.[(((triple3 triple1) -> rule4) OR ((triple3 ((triple3) -> rule5)) -> rule4))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
((triple3) -> (rule5 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
((((triple3 triple1) -> (rule4 % int2))) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
((((triple3 ((triple3) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is blue.
("Bob" "is" "blue" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
triple3
Bob is round.
("Bob" "is" "round" "+")
triple4
Charlie is blue.
("Charlie" "is" "blue" "+")
triple5
((triple8) -> (rule5 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
((((triple7 triple9) -> (rule7 % int2))) -> (rule5 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
triple6
((triple10) -> (rule6 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
((triple10) -> (rule8 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
((triple7) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
((((triple8 triple5) -> (rule4 % int2))) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
((((triple8 ((triple8) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
int3
Charlie is furry.
("Charlie" "is" "furry" "+")
triple7
((triple8 triple5) -> (rule4 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
((triple8 ((triple8) -> (rule5 % int2))) -> (rule4 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple8
((triple7 triple9) -> (rule7 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
triple9
Charlie is young.
("Charlie" "is" "young" "+")
triple10
Bob is furry.
("Bob" "is" "furry" "+")
((triple3 triple1) -> (rule4 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((triple3 ((triple3) -> (rule5 % int2))) -> (rule4 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2