Charlie is red. Dave is blue. If someone is round and red then they are blue. If Dave is quiet and Dave is blue then Dave is furry. All furry people are nice. If Charlie is cold then Charlie is blue. Furry, quiet people are red. If Charlie is cold and Charlie is red then Charlie is quiet.
Charlie is red.
("Charlie" "is" "red" "+")
Dave is blue.
("Dave" "is" "blue" "+")
If someone is round and red then they are blue.
((("someone" "is" "round" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "blue" "+"))
If Dave is quiet and Dave is blue then Dave is furry.
((("Dave" "is" "quiet" "+") ("Dave" "is" "blue" "+")) -> ("Dave" "is" "furry" "+"))
All furry people are nice.
((("someone" "is" "furry" "+")) -> ("someone" "is" "nice" "+"))
If Charlie is cold then Charlie is blue.
((("Charlie" "is" "cold" "+")) -> ("Charlie" "is" "blue" "+"))
Furry, quiet people are red.
((("someone" "is" "furry" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "red" "+"))
If Charlie is cold and Charlie is red then Charlie is quiet.
((("Charlie" "is" "cold" "+") ("Charlie" "is" "red" "+")) -> ("Charlie" "is" "quiet" "+"))
Dave is blue.
True
1
proof
[(triple2)]
("Dave" "is" "blue" "+")
triple2
Dave is not blue.
False
1
inv-proof
[(triple2)]
("Dave" "is" "blue" "-")
triple2
Dave is not red.
Unknown
inv-rconc
[@1: Dave is red.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Dave" "is" "red" "-")
Dave is quiet.
Unknown
random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "+")
@0: Charlie is red.[(triple1)] Dave is blue.[(triple2)]
Charlie is red.
("Charlie" "is" "red" "+")
triple1
Dave is blue.
("Dave" "is" "blue" "+")
triple2