Anne is blue. Anne is young. Dave is blue. If someone is white and not round then they are not young. If someone is white and young then they are furry. Blue people are white.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is young.
("Anne" "is" "young" "+")
Dave is blue.
("Dave" "is" "blue" "+")
If someone is white and not round then they are not young.
((("someone" "is" "white" "+") ("someone" "is" "round" "~")) -> ("someone" "is" "young" "-"))
If someone is white and young then they are furry.
((("someone" "is" "white" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "furry" "+"))
Blue people are white.
((("someone" "is" "blue" "+")) -> ("someone" "is" "white" "+"))
Dave is blue.
True
1
proof
[(triple3)]
("Dave" "is" "blue" "+")
triple3
Anne is not blue.
False
1
inv-proof
[(triple1)]
("Anne" "is" "blue" "-")
triple1
Dave is not furry.
Unknown
inv-rconc
[@1: Dave is furry.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "furry" "-")
Dave is red.
Unknown
random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "+")
@0: Anne is blue.[(triple1)] Anne is young.[(triple2)] Dave is blue.[(triple3)] @1: Anne is white.[(((triple1) -> rule3))] Dave is white.[(((triple3) -> rule3))] @2: Anne is furry.[(((((triple1) -> rule3) triple2) -> rule2))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is young.
("Anne" "is" "young" "+")
triple2
Dave is blue.
("Dave" "is" "blue" "+")
triple3
Anne is white.
("Anne" "is" "white" "+")
((triple1) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
((triple3) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
((((triple1) -> (rule3 % int2)) triple2) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2