Anne is blue. Anne is not red. Dave is blue. Dave is red. Dave is smart. Harry is blue. Harry is furry. If someone is furry and not blue then they are red. If someone is smart and not blue then they are furry. If Dave is blue and Dave is smart then Dave is rough.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is not red.
("Anne" "is" "red" "-")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is furry.
("Harry" "is" "furry" "+")
If someone is furry and not blue then they are red.
((("someone" "is" "furry" "+") ("someone" "is" "blue" "~")) -> ("someone" "is" "red" "+"))
If someone is smart and not blue then they are furry.
((("someone" "is" "smart" "+") ("someone" "is" "blue" "~")) -> ("someone" "is" "furry" "+"))
If Dave is blue and Dave is smart then Dave is rough.
((("Dave" "is" "blue" "+") ("Dave" "is" "smart" "+")) -> ("Dave" "is" "rough" "+"))
Dave is smart.
True
1
proof
[(triple5)]
("Dave" "is" "smart" "+")
triple5
Dave is not red.
False
1
inv-proof
[(triple4)]
("Dave" "is" "red" "-")
triple4
Harry is not red.
Unknown
inv-rconc
[@1: Harry is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "red" "-")
Anne is rough.
Unknown
random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "+")
@0: Anne is blue.[(triple1)] Anne is not red.[(triple2)] Dave is blue.[(triple3)] Dave is red.[(triple4)] Dave is smart.[(triple5)] Harry is blue.[(triple6)] Harry is furry.[(triple7)] @1: Dave is rough.[(((triple3 triple5) -> rule3))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is not red.
("Anne" "is" "red" "-")
triple2
Dave is blue.
("Dave" "is" "blue" "+")
triple3
Dave is red.
("Dave" "is" "red" "+")
triple4
Dave is smart.
("Dave" "is" "smart" "+")
triple5
Harry is blue.
("Harry" "is" "blue" "+")
triple6
Harry is furry.
("Harry" "is" "furry" "+")
triple7
Dave is rough.
("Dave" "is" "rough" "+")
((triple3 triple5) -> (rule3 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1