Anne is furry. Anne is red. Charlie is young. If someone is young then they are nice. If someone is red and furry then they are nice. If Anne is quiet and Anne is furry then Anne is not smart. If Anne is smart then Anne is furry. If someone is young and quiet then they are white. If someone is furry then they are young.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is red.
("Anne" "is" "red" "+")
Charlie is young.
("Charlie" "is" "young" "+")
If someone is young then they are nice.
((("someone" "is" "young" "+")) -> ("someone" "is" "nice" "+"))
If someone is red and furry then they are nice.
((("someone" "is" "red" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "nice" "+"))
If Anne is quiet and Anne is furry then Anne is not smart.
((("Anne" "is" "quiet" "+") ("Anne" "is" "furry" "+")) -> ("Anne" "is" "smart" "-"))
If Anne is smart then Anne is furry.
((("Anne" "is" "smart" "+")) -> ("Anne" "is" "furry" "+"))
If someone is young and quiet then they are white.
((("someone" "is" "young" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "white" "+"))
If someone is furry then they are young.
((("someone" "is" "furry" "+")) -> ("someone" "is" "young" "+"))
Anne is furry.
True
1
proof
[(triple1)]
("Anne" "is" "furry" "+")
triple1
Anne is not red.
False
1
inv-proof
[(triple2)]
("Anne" "is" "red" "-")
triple2
Charlie is nice.
True
2
proof
[(((triple3) -> rule1))]
("Charlie" "is" "nice" "+")
((triple3) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is not nice.
False
2
inv-proof
[(((triple3) -> rule1))]
("Charlie" "is" "nice" "-")
((triple3) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is not white.
Unknown
inv-rconc
[@1: Charlie is white.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "white" "-")
Anne is white.
Unknown
rconc
[@1: Anne is white.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Anne" "is" "white" "+")
Anne is not smart.
Unknown
inv-random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "-")
Anne is quiet.
Unknown
random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "+")
@0: Anne is furry.[(triple1)] Anne is red.[(triple2)] Charlie is young.[(triple3)] @1: Anne is nice.[(((triple2 triple1) -> rule2) OR ((((triple1) -> rule6)) -> rule1))] Anne is young.[(((triple1) -> rule6))] Charlie is nice.[(((triple3) -> rule1))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Anne is red.
("Anne" "is" "red" "+")
triple2
Charlie is young.
("Charlie" "is" "young" "+")
triple3
Anne is nice.
("Anne" "is" "nice" "+")
((triple2 triple1) -> (rule2 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
((((triple1) -> (rule6 % int2))) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
((triple1) -> (rule6 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple3) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1