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