Bob is blue. Bob is cold. Bob is round. If someone is furry and not round then they are smart. If someone is round and cold then they are not smart. If Bob is blue and Bob is not round then Bob is not furry. If someone is round and not nice then they are cold. If Bob is round and Bob is blue then Bob is cold. All cold people are not furry.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is round.
("Bob" "is" "round" "+")
If someone is furry and not round then they are smart.
((("someone" "is" "furry" "+") ("someone" "is" "round" "~")) -> ("someone" "is" "smart" "+"))
If someone is round and cold then they are not smart.
((("someone" "is" "round" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "smart" "-"))
If Bob is blue and Bob is not round then Bob is not furry.
((("Bob" "is" "blue" "+") ("Bob" "is" "round" "~")) -> ("Bob" "is" "furry" "-"))
If someone is round and not nice then they are cold.
((("someone" "is" "round" "+") ("someone" "is" "nice" "~")) -> ("someone" "is" "cold" "+"))
If Bob is round and Bob is blue then Bob is cold.
((("Bob" "is" "round" "+") ("Bob" "is" "blue" "+")) -> ("Bob" "is" "cold" "+"))
All cold people are not furry.
((("someone" "is" "cold" "+")) -> ("someone" "is" "furry" "-"))
Bob is round.
True
1
proof
[(triple3)]
("Bob" "is" "round" "+")
triple3
Bob is not blue.
False
1
inv-proof
[(triple1)]
("Bob" "is" "blue" "-")
triple1
Bob is not nice.
Unknown
inv-random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "-")
Bob is kind.
Unknown
random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "+")
@0: Bob is blue.[(triple1)] Bob is cold.[(triple2 OR ((triple3 triple1) -> rule5))] Bob is round.[(triple3)] @1: Bob is not furry.[(((triple2) -> rule6) OR ((((triple3 triple1) -> rule5)) -> rule6))] Bob is not smart.[(((triple3 triple2) -> rule2) OR ((triple3 ((triple3 triple1) -> rule5)) -> rule2))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
((triple3 triple1) -> (rule5 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
triple3
Bob is not furry.
("Bob" "is" "furry" "-")
((triple2) -> (rule6 % int1))
Bob is not furry.
("Bob" "is" "furry" "-")
int1
((((triple3 triple1) -> (rule5 % int2))) -> (rule6 % int1))
Bob is not furry.
("Bob" "is" "furry" "-")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is not smart.
("Bob" "is" "smart" "-")
((triple3 triple2) -> (rule2 % int1))
Bob is not smart.
("Bob" "is" "smart" "-")
int1
((triple3 ((triple3 triple1) -> (rule5 % int2))) -> (rule2 % int1))
Bob is not smart.
("Bob" "is" "smart" "-")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2