Bob is cold. Charlie is round. Dave is furry. Erin is nice. If someone is nice and not young then they are not kind. If Bob is not furry then Bob is not nice. Cold, nice people are smart. If Bob is round then Bob is kind. Furry, round people are cold. If Charlie is round and Charlie is not smart then Charlie is kind.
Bob is cold.
("Bob" "is" "cold" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Erin is nice.
("Erin" "is" "nice" "+")
If someone is nice and not young then they are not kind.
((("someone" "is" "nice" "+") ("someone" "is" "young" "~")) -> ("someone" "is" "kind" "-"))
If Bob is not furry then Bob is not nice.
((("Bob" "is" "furry" "~")) -> ("Bob" "is" "nice" "-"))
Cold, nice people are smart.
((("someone" "is" "cold" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "smart" "+"))
If Bob is round then Bob is kind.
((("Bob" "is" "round" "+")) -> ("Bob" "is" "kind" "+"))
Furry, round people are cold.
((("someone" "is" "furry" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "cold" "+"))
If Charlie is round and Charlie is not smart then Charlie is kind.
((("Charlie" "is" "round" "+") ("Charlie" "is" "smart" "~")) -> ("Charlie" "is" "kind" "+"))
Dave is furry.
True
1
proof
[(triple3)]
("Dave" "is" "furry" "+")
triple3
Dave is not furry.
False
1
inv-proof
[(triple3)]
("Dave" "is" "furry" "-")
triple3
Charlie is not smart.
Unknown
inv-rconc
[@1: Charlie is smart.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "smart" "-")
Charlie is nice.
Unknown
random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "+")
@0: Bob is cold.[(triple1)] Charlie is round.[(triple2)] Dave is furry.[(triple3)] Erin is nice.[(triple4)]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Charlie is round.
("Charlie" "is" "round" "+")
triple2
Dave is furry.
("Dave" "is" "furry" "+")
triple3
Erin is nice.
("Erin" "is" "nice" "+")
triple4