Anne is green. Anne is nice. Anne is quiet. Dave is big. Dave is green. Dave is kind. Dave is nice. Dave is quiet. Dave is round. Dave is white. If Anne is quiet then Anne is big. Kind, quiet things are nice. All round, quiet things are white. If something is round and big then it is nice. If Dave is green then Dave is white. Quiet things are nice.
Anne is green.
("Anne" "is" "green" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is white.
("Dave" "is" "white" "+")
If Anne is quiet then Anne is big.
((("Anne" "is" "quiet" "+")) -> ("Anne" "is" "big" "+"))
Kind, quiet things are nice.
((("something" "is" "kind" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "nice" "+"))
All round, quiet things are white.
((("something" "is" "round" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "white" "+"))
If something is round and big then it is nice.
((("something" "is" "round" "+") ("something" "is" "big" "+")) -> ("something" "is" "nice" "+"))
If Dave is green then Dave is white.
((("Dave" "is" "green" "+")) -> ("Dave" "is" "white" "+"))
Quiet things are nice.
((("something" "is" "quiet" "+")) -> ("something" "is" "nice" "+"))
Anne is green.
True
1
proof
[(triple1)]
("Anne" "is" "green" "+")
triple1
Anne is not quiet.
False
1
inv-proof
[(triple3)]
("Anne" "is" "quiet" "-")
triple3
Anne is big.
True
2
proof
[(((triple3) -> rule1))]
("Anne" "is" "big" "+")
((triple3) -> (rule1 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is not big.
False
2
inv-proof
[(((triple3) -> rule1))]
("Anne" "is" "big" "-")
((triple3) -> (rule1 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is not white.
Unknown
inv-rconc
[@1: Anne is white.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "white" "-")
Anne is kind.
Unknown
random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "+")
@0: Anne is green.[(triple1)] Anne is nice.[(triple2 OR ((triple3) -> rule6))] Anne is quiet.[(triple3)] Dave is big.[(triple4)] Dave is green.[(triple5)] Dave is kind.[(triple6)] Dave is nice.[(triple7 OR ((triple8) -> rule6) OR ((triple6 triple8) -> rule2) OR ((triple9 triple4) -> rule4))] Dave is quiet.[(triple8)] Dave is round.[(triple9)] Dave is white.[(triple10 OR ((triple5) -> rule5) OR ((triple9 triple8) -> rule3))] @1: Anne is big.[(((triple3) -> rule1))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Anne is nice.
("Anne" "is" "nice" "+")
triple2
((triple3) -> (rule6 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple3
Dave is big.
("Dave" "is" "big" "+")
triple4
Dave is green.
("Dave" "is" "green" "+")
triple5
Dave is kind.
("Dave" "is" "kind" "+")
triple6
Dave is nice.
("Dave" "is" "nice" "+")
triple7
((triple8) -> (rule6 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((triple6 triple8) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((triple9 triple4) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
triple8
Dave is round.
("Dave" "is" "round" "+")
triple9
Dave is white.
("Dave" "is" "white" "+")
triple10
((triple5) -> (rule5 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
((triple9 triple8) -> (rule3 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
((triple3) -> (rule1 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1