Anne is blue. Anne is furry. Anne is green. Anne is kind. Anne is rough. Anne is round. Anne is smart. Dave is rough. Gary is blue. Gary is kind. Gary is rough. Gary is smart. If something is smart then it is furry. All blue, smart things are green. All blue, kind things are rough.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is smart.
("Gary" "is" "smart" "+")
If something is smart then it is furry.
((("something" "is" "smart" "+")) -> ("something" "is" "furry" "+"))
All blue, smart things are green.
((("something" "is" "blue" "+") ("something" "is" "smart" "+")) -> ("something" "is" "green" "+"))
All blue, kind things are rough.
((("something" "is" "blue" "+") ("something" "is" "kind" "+")) -> ("something" "is" "rough" "+"))
Anne is round.
True
1
proof
[(triple6)]
("Anne" "is" "round" "+")
triple6
Dave is not rough.
False
1
inv-proof
[(triple8)]
("Dave" "is" "rough" "-")
triple8
Gary is green.
True
3
proof
[(((triple9 triple12) -> rule2))]
("Gary" "is" "green" "+")
((triple9 triple12) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is not furry.
False
2
inv-proof
[(((triple12) -> rule1))]
("Gary" "is" "furry" "-")
((triple12) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Dave is not green.
Unknown
inv-rconc
[@1: Dave is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "green" "-")
Dave is furry.
Unknown
rconc
[@1: Dave is furry.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "furry" "+")
Gary is not round.
Unknown
inv-random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
@0: Anne is blue.[(triple1)] Anne is furry.[(triple2 OR ((triple7) -> rule1))] Anne is green.[(triple3 OR ((triple1 triple7) -> rule2))] Anne is kind.[(triple4)] Anne is rough.[(triple5 OR ((triple1 triple4) -> rule3))] Anne is round.[(triple6)] Anne is smart.[(triple7)] Dave is rough.[(triple8)] Gary is blue.[(triple9)] Gary is kind.[(triple10)] Gary is rough.[(triple11 OR ((triple9 triple10) -> rule3))] Gary is smart.[(triple12)] @1: Gary is furry.[(((triple12) -> rule1))] Gary is green.[(((triple9 triple12) -> rule2))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is furry.
("Anne" "is" "furry" "+")
triple2
((triple7) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
triple3
((triple1 triple7) -> (rule2 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
triple4
Anne is rough.
("Anne" "is" "rough" "+")
triple5
((triple1 triple4) -> (rule3 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
triple6
Anne is smart.
("Anne" "is" "smart" "+")
triple7
Dave is rough.
("Dave" "is" "rough" "+")
triple8
Gary is blue.
("Gary" "is" "blue" "+")
triple9
Gary is kind.
("Gary" "is" "kind" "+")
triple10
Gary is rough.
("Gary" "is" "rough" "+")
triple11
((triple9 triple10) -> (rule3 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
triple12
Gary is furry.
("Gary" "is" "furry" "+")
((triple12) -> (rule1 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
((triple9 triple12) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1