Anne is red. Dave is kind. Dave is round. If something is quiet then it is nice. All round things are nice. If Anne is nice then Anne is round.
Anne is red.
("Anne" "is" "red" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is round.
("Dave" "is" "round" "+")
If something is quiet then it is nice.
((("something" "is" "quiet" "+")) -> ("something" "is" "nice" "+"))
All round things are nice.
((("something" "is" "round" "+")) -> ("something" "is" "nice" "+"))
If Anne is nice then Anne is round.
((("Anne" "is" "nice" "+")) -> ("Anne" "is" "round" "+"))
Dave is round.
True
1
proof
[(triple3)]
("Dave" "is" "round" "+")
triple3
Dave is not kind.
False
1
inv-proof
[(triple2)]
("Dave" "is" "kind" "-")
triple2
Dave is nice.
True
2
proof
[(((triple3) -> rule2))]
("Dave" "is" "nice" "+")
((triple3) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is not nice.
False
2
inv-proof
[(((triple3) -> rule2))]
("Dave" "is" "nice" "-")
((triple3) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Anne is not nice.
Unknown
inv-rconc
[@3: Anne is nice.[CWA. Example of deepest failure = (rule2 <- rule3 <- rule1 <- FAIL)]]
("Anne" "is" "nice" "-")
Anne is round.
Unknown
rconc
[@2: Anne is round.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("Anne" "is" "round" "+")
Dave is not quiet.
Unknown
inv-random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "-")
Anne is kind.
Unknown
random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "+")
@0: Anne is red.[(triple1)] Dave is kind.[(triple2)] Dave is round.[(triple3)] @1: Dave is nice.[(((triple3) -> rule2))]
Anne is red.
("Anne" "is" "red" "+")
triple1
Dave is kind.
("Dave" "is" "kind" "+")
triple2
Dave is round.
("Dave" "is" "round" "+")
triple3
Dave is nice.
("Dave" "is" "nice" "+")
((triple3) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1