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