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