Anne is nice. Anne is quiet. Anne is red. Anne is rough. Anne is not smart. Dave is big. Dave is nice. Dave is not quiet. Dave is red. Dave is smart. If Dave is quiet and Dave is red then Dave is big. Quiet, smart people are red. Round, quiet people are not red. If Dave is round and Dave is nice then Dave is smart. Big people are round. Round people are smart.
Anne is nice.
("Anne" "is" "nice" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is not smart.
("Anne" "is" "smart" "-")
Dave is big.
("Dave" "is" "big" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is not quiet.
("Dave" "is" "quiet" "-")
Dave is red.
("Dave" "is" "red" "+")
Dave is smart.
("Dave" "is" "smart" "+")
If Dave is quiet and Dave is red then Dave is big.
((("Dave" "is" "quiet" "+") ("Dave" "is" "red" "+")) -> ("Dave" "is" "big" "+"))
Quiet, smart people are red.
((("someone" "is" "quiet" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "red" "+"))
Round, quiet people are not red.
((("someone" "is" "round" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "red" "-"))
If Dave is round and Dave is nice then Dave is smart.
((("Dave" "is" "round" "+") ("Dave" "is" "nice" "+")) -> ("Dave" "is" "smart" "+"))
Big people are round.
((("someone" "is" "big" "+")) -> ("someone" "is" "round" "+"))
Round people are smart.
((("someone" "is" "round" "+")) -> ("someone" "is" "smart" "+"))
Dave is not quiet.
True
1
proof
[(triple8)]
("Dave" "is" "quiet" "-")
triple8
Dave is not nice.
False
1
inv-proof
[(triple7)]
("Dave" "is" "nice" "-")
triple7
Dave is round.
True
2
proof
[(((triple6) -> rule5))]
("Dave" "is" "round" "+")
((triple6) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is not round.
False
2
inv-proof
[(((triple6) -> rule5))]
("Dave" "is" "round" "-")
((triple6) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Anne is not round.
Unknown
inv-rconc
[@1: Anne is round.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Anne" "is" "round" "-")
Anne is big.
Unknown
random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "+")
@0: Anne is nice.[(triple1)] Anne is not smart.[(triple5)] Anne is quiet.[(triple2)] Anne is red.[(triple3)] Anne is rough.[(triple4)] Dave is big.[(triple6)] Dave is nice.[(triple7)] Dave is not quiet.[(triple8)] Dave is red.[(triple9)] Dave is smart.[(triple10 OR ((((triple6) -> rule5)) -> rule6) OR ((((triple6) -> rule5) triple7) -> rule4))] @1: Dave is round.[(((triple6) -> rule5))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Anne is not smart.
("Anne" "is" "smart" "-")
triple5
Anne is quiet.
("Anne" "is" "quiet" "+")
triple2
Anne is red.
("Anne" "is" "red" "+")
triple3
Anne is rough.
("Anne" "is" "rough" "+")
triple4
Dave is big.
("Dave" "is" "big" "+")
triple6
Dave is nice.
("Dave" "is" "nice" "+")
triple7
Dave is not quiet.
("Dave" "is" "quiet" "-")
triple8
Dave is red.
("Dave" "is" "red" "+")
triple9
Dave is smart.
("Dave" "is" "smart" "+")
triple10
((((triple6) -> (rule5 % int2))) -> (rule6 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
((((triple6) -> (rule5 % int2)) triple7) -> (rule4 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
((triple6) -> (rule5 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1