Anne is blue. Anne is cold. Anne is furry. Anne is nice. Anne is red. Anne is smart. Dave is cold. Dave is red. Dave is smart. Dave is young. If something is blue and not smart then it is cold. Red, nice things are furry. If something is furry then it is red. All furry, nice things are red. If Dave is red and Dave is nice then Dave is not furry. All blue things are young.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is young.
("Dave" "is" "young" "+")
If something is blue and not smart then it is cold.
((("something" "is" "blue" "+") ("something" "is" "smart" "~")) -> ("something" "is" "cold" "+"))
Red, nice things are furry.
((("something" "is" "red" "+") ("something" "is" "nice" "+")) -> ("something" "is" "furry" "+"))
If something is furry then it is red.
((("something" "is" "furry" "+")) -> ("something" "is" "red" "+"))
All furry, nice things are red.
((("something" "is" "furry" "+") ("something" "is" "nice" "+")) -> ("something" "is" "red" "+"))
If Dave is red and Dave is nice then Dave is not furry.
((("Dave" "is" "red" "+") ("Dave" "is" "nice" "+")) -> ("Dave" "is" "furry" "-"))
All blue things are young.
((("something" "is" "blue" "+")) -> ("something" "is" "young" "+"))
Anne is blue.
True
1
proof
[(triple1)]
("Anne" "is" "blue" "+")
triple1
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 nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
@0: Anne is blue.[(triple1)] Anne is cold.[(triple2)] Anne is furry.[(triple3 OR ((triple5 triple4) -> rule2))] Anne is nice.[(triple4)] Anne is red.[(triple5 OR ((triple3) -> rule3) OR ((triple3 triple4) -> rule4))] Anne is smart.[(triple6)] Dave is cold.[(triple7)] Dave is red.[(triple8)] Dave is smart.[(triple9)] Dave is young.[(triple10)] @1: Anne is young.[(((triple1) -> rule6))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is cold.
("Anne" "is" "cold" "+")
triple2
Anne is furry.
("Anne" "is" "furry" "+")
triple3
((triple5 triple4) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
triple4
Anne is red.
("Anne" "is" "red" "+")
triple5
((triple3) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((triple3 triple4) -> (rule4 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
triple6
Dave is cold.
("Dave" "is" "cold" "+")
triple7
Dave is red.
("Dave" "is" "red" "+")
triple8
Dave is smart.
("Dave" "is" "smart" "+")
triple9
Dave is young.
("Dave" "is" "young" "+")
triple10
Anne is young.
("Anne" "is" "young" "+")
((triple1) -> (rule6 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1