Anne is kind. Anne is red. Anne is young. Bob is quiet. Bob is red. Bob is round. Bob is young. Charlie is quiet. Charlie is white. Charlie is young. Dave is big. Dave is kind. Dave is quiet. Dave is red. Dave is round. Dave is white. If Anne is quiet then Anne is round. If someone is kind and red then they are young.
Anne is kind.
("Anne" "is" "kind" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is young.
("Anne" "is" "young" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is young.
("Bob" "is" "young" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is white.
("Dave" "is" "white" "+")
If Anne is quiet then Anne is round.
((("Anne" "is" "quiet" "+")) -> ("Anne" "is" "round" "+"))
If someone is kind and red then they are young.
((("someone" "is" "kind" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "young" "+"))
Anne is kind.
True
1
proof
[(triple1)]
("Anne" "is" "kind" "+")
triple1
Dave is not red.
False
1
inv-proof
[(triple14)]
("Dave" "is" "red" "-")
triple14
Dave is young.
True
3
proof
[(((triple12 triple14) -> rule2))]
("Dave" "is" "young" "+")
((triple12 triple14) -> (rule2 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is not young.
False
3
inv-proof
[(((triple12 triple14) -> rule2))]
("Dave" "is" "young" "-")
((triple12 triple14) -> (rule2 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Anne is not round.
Unknown
inv-rconc
[@1: Anne is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "round" "-")
Charlie is red.
Unknown
random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "+")
Anne is not quiet.
Unknown
inv-random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "-")
Charlie is kind.
Unknown
random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "+")
@0: Anne is kind.[(triple1)] Anne is red.[(triple2)] Anne is young.[(triple3 OR ((triple1 triple2) -> rule2))] Bob is quiet.[(triple4)] Bob is red.[(triple5)] Bob is round.[(triple6)] Bob is young.[(triple7)] Charlie is quiet.[(triple8)] Charlie is white.[(triple9)] Charlie is young.[(triple10)] Dave is big.[(triple11)] Dave is kind.[(triple12)] Dave is quiet.[(triple13)] Dave is red.[(triple14)] Dave is round.[(triple15)] Dave is white.[(triple16)] @1: Dave is young.[(((triple12 triple14) -> rule2))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Anne is red.
("Anne" "is" "red" "+")
triple2
Anne is young.
("Anne" "is" "young" "+")
triple3
((triple1 triple2) -> (rule2 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple4
Bob is red.
("Bob" "is" "red" "+")
triple5
Bob is round.
("Bob" "is" "round" "+")
triple6
Bob is young.
("Bob" "is" "young" "+")
triple7
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple8
Charlie is white.
("Charlie" "is" "white" "+")
triple9
Charlie is young.
("Charlie" "is" "young" "+")
triple10
Dave is big.
("Dave" "is" "big" "+")
triple11
Dave is kind.
("Dave" "is" "kind" "+")
triple12
Dave is quiet.
("Dave" "is" "quiet" "+")
triple13
Dave is red.
("Dave" "is" "red" "+")
triple14
Dave is round.
("Dave" "is" "round" "+")
triple15
Dave is white.
("Dave" "is" "white" "+")
triple16
Dave is young.
("Dave" "is" "young" "+")
((triple12 triple14) -> (rule2 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1