Dave is blue. Dave is not cold. Dave is not furry. Dave is nice. Dave is not white. Harry is not cold. Harry is furry. Harry is not nice. Harry is quiet. Harry is white. If someone is nice and quiet then they are white. If Dave is round and Dave is not white then Dave is furry. All cold, nice people are round. If someone is white and furry then they are not round. If someone is white and round then they are not cold. Round people are not cold. If someone is nice and not cold then they are blue. If someone is furry and not quiet then they are blue.
Dave is blue.
("Dave" "is" "blue" "+")
Dave is not cold.
("Dave" "is" "cold" "-")
Dave is not furry.
("Dave" "is" "furry" "-")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is not white.
("Dave" "is" "white" "-")
Harry is not cold.
("Harry" "is" "cold" "-")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is not nice.
("Harry" "is" "nice" "-")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is white.
("Harry" "is" "white" "+")
If someone is nice and quiet then they are white.
((("someone" "is" "nice" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "white" "+"))
If Dave is round and Dave is not white then Dave is furry.
((("Dave" "is" "round" "+") ("Dave" "is" "white" "~")) -> ("Dave" "is" "furry" "+"))
All cold, nice people are round.
((("someone" "is" "cold" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "round" "+"))
If someone is white and furry then they are not round.
((("someone" "is" "white" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "round" "-"))
If someone is white and round then they are not cold.
((("someone" "is" "white" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "cold" "-"))
Round people are not cold.
((("someone" "is" "round" "+")) -> ("someone" "is" "cold" "-"))
If someone is nice and not cold then they are blue.
((("someone" "is" "nice" "+") ("someone" "is" "cold" "~")) -> ("someone" "is" "blue" "+"))
If someone is furry and not quiet then they are blue.
((("someone" "is" "furry" "+") ("someone" "is" "quiet" "~")) -> ("someone" "is" "blue" "+"))
Harry is not nice.
True
1
proof
[(triple8)]
("Harry" "is" "nice" "-")
triple8
Dave is not nice.
False
1
inv-proof
[(triple4)]
("Dave" "is" "nice" "-")
triple4
Dave is not round.
Unknown
inv-rconc
[@1: Dave is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "round" "-")
Dave is quiet.
Unknown
random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "+")
@0: Dave is blue.[(triple1 OR ((triple4 triple2) -> rule7))] Dave is nice.[(triple4)] Dave is not cold.[(triple2)] Dave is not furry.[(triple3)] Dave is not white.[(triple5)] Harry is furry.[(triple7)] Harry is not cold.[(triple6)] Harry is not nice.[(triple8)] Harry is quiet.[(triple9)] Harry is white.[(triple10)] @1: Harry is not round.[(((triple10 triple7) -> rule4))]
Dave is blue.
("Dave" "is" "blue" "+")
triple1
((triple4 triple2) -> (rule7 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
triple4
Dave is not cold.
("Dave" "is" "cold" "-")
triple2
Dave is not furry.
("Dave" "is" "furry" "-")
triple3
Dave is not white.
("Dave" "is" "white" "-")
triple5
Harry is furry.
("Harry" "is" "furry" "+")
triple7
Harry is not cold.
("Harry" "is" "cold" "-")
triple6
Harry is not nice.
("Harry" "is" "nice" "-")
triple8
Harry is quiet.
("Harry" "is" "quiet" "+")
triple9
Harry is white.
("Harry" "is" "white" "+")
triple10
Harry is not round.
("Harry" "is" "round" "-")
((triple10 triple7) -> (rule4 % int1))
Harry is not round.
("Harry" "is" "round" "-")
int1