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