Anne is blue. Anne is green. Bob is blue. Bob is red. Bob is round. Bob is smart. Erin is blue. Erin is red. Erin is smart. Erin is white. Fiona is blue. Fiona is green. Fiona is quiet. Fiona is round. Fiona is smart. Fiona is white. All round people are quiet. Quiet, smart people are red. If someone is blue then they are quiet. If Fiona is blue and Fiona is white then Fiona is green. If Bob is green then Bob is smart. If someone is round then they are white. If Bob is blue and Bob is smart then Bob is green. Blue people are smart.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is green.
("Anne" "is" "green" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is white.
("Erin" "is" "white" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Fiona is white.
("Fiona" "is" "white" "+")
All round people are quiet.
((("someone" "is" "round" "+")) -> ("someone" "is" "quiet" "+"))
Quiet, smart people are red.
((("someone" "is" "quiet" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "red" "+"))
If someone is blue then they are quiet.
((("someone" "is" "blue" "+")) -> ("someone" "is" "quiet" "+"))
If Fiona is blue and Fiona is white then Fiona is green.
((("Fiona" "is" "blue" "+") ("Fiona" "is" "white" "+")) -> ("Fiona" "is" "green" "+"))
If Bob is green then Bob is smart.
((("Bob" "is" "green" "+")) -> ("Bob" "is" "smart" "+"))
If someone is round then they are white.
((("someone" "is" "round" "+")) -> ("someone" "is" "white" "+"))
If Bob is blue and Bob is smart then Bob is green.
((("Bob" "is" "blue" "+") ("Bob" "is" "smart" "+")) -> ("Bob" "is" "green" "+"))
Blue people are smart.
((("someone" "is" "blue" "+")) -> ("someone" "is" "smart" "+"))
Erin is smart.
True
1
proof
[(triple9 OR ((triple7) -> rule8))]
("Erin" "is" "smart" "+")
triple9
((triple7) -> (rule8 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is not white.
False
1
inv-proof
[(triple10)]
("Erin" "is" "white" "-")
triple10
Erin is quiet.
True
2
proof
[(((triple7) -> rule3))]
("Erin" "is" "quiet" "+")
((triple7) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Anne is not smart.
False
2
inv-proof
[(((triple1) -> rule8))]
("Anne" "is" "smart" "-")
((triple1) -> (rule8 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is not white.
Unknown
inv-rconc
[@1: Anne is white.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Anne" "is" "white" "-")
Erin is round.
Unknown
random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "+")
Erin is not green.
Unknown
inv-random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "-")
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 green.[(triple2)] Bob is blue.[(triple3)] Bob is red.[(triple4 OR ((((triple3) -> rule3) triple6) -> rule2) OR ((((triple5) -> rule1) triple6) -> rule2) OR ((((triple3) -> rule3) ((triple3) -> rule8)) -> rule2) OR ((((triple5) -> rule1) ((triple3) -> rule8)) -> rule2))] Bob is round.[(triple5)] Bob is smart.[(triple6 OR ((triple3) -> rule8))] Erin is blue.[(triple7)] Erin is red.[(triple8 OR ((((triple7) -> rule3) triple9) -> rule2) OR ((((triple7) -> rule3) ((triple7) -> rule8)) -> rule2))] Erin is smart.[(triple9 OR ((triple7) -> rule8))] Erin is white.[(triple10)] Fiona is blue.[(triple11)] Fiona is green.[(triple12 OR ((triple11 triple16) -> rule4) OR ((triple11 ((triple14) -> rule6)) -> rule4))] Fiona is quiet.[(triple13 OR ((triple11) -> rule3) OR ((triple14) -> rule1))] Fiona is round.[(triple14)] Fiona is smart.[(triple15 OR ((triple11) -> rule8))] Fiona is white.[(triple16 OR ((triple14) -> rule6))] @1: Anne is quiet.[(((triple1) -> rule3))] Anne is smart.[(((triple1) -> rule8))] Bob is green.[(((triple3 triple6) -> rule7) OR ((triple3 ((triple3) -> rule8)) -> rule7))] Bob is quiet.[(((triple3) -> rule3) OR ((triple5) -> rule1))] Bob is white.[(((triple5) -> rule6))] Erin is quiet.[(((triple7) -> rule3))] Fiona is red.[(((triple13 triple15) -> rule2) OR ((triple13 ((triple11) -> rule8)) -> rule2) OR ((((triple11) -> rule3) triple15) -> rule2) OR ((((triple14) -> rule1) triple15) -> rule2) OR ((((triple11) -> rule3) ((triple11) -> rule8)) -> rule2) OR ((((triple14) -> rule1) ((triple11) -> rule8)) -> rule2))] @2: Anne is red.[(((((triple1) -> rule3) ((triple1) -> rule8)) -> rule2))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple2
Bob is blue.
("Bob" "is" "blue" "+")
triple3
Bob is red.
("Bob" "is" "red" "+")
triple4
((((triple3) -> (rule3 % int2)) triple6) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
((((triple5) -> (rule1 % int2)) triple6) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
((((triple3) -> (rule3 % int3)) ((triple3) -> (rule8 % int2))) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
((((triple5) -> (rule1 % int3)) ((triple3) -> (rule8 % int2))) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Bob is round.
("Bob" "is" "round" "+")
triple5
Bob is smart.
("Bob" "is" "smart" "+")
triple6
((triple3) -> (rule8 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
triple7
Erin is red.
("Erin" "is" "red" "+")
triple8
((((triple7) -> (rule3 % int2)) triple9) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
((((triple7) -> (rule3 % int3)) ((triple7) -> (rule8 % int2))) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
triple9
((triple7) -> (rule8 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
triple10
Fiona is blue.
("Fiona" "is" "blue" "+")
triple11
Fiona is green.
("Fiona" "is" "green" "+")
triple12
((triple11 triple16) -> (rule4 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
((triple11 ((triple14) -> (rule6 % int2))) -> (rule4 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple13
((triple11) -> (rule3 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
((triple14) -> (rule1 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
triple14
Fiona is smart.
("Fiona" "is" "smart" "+")
triple15
((triple11) -> (rule8 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
triple16
((triple14) -> (rule6 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple1) -> (rule3 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
((triple1) -> (rule8 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
((triple3 triple6) -> (rule7 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
((triple3 ((triple3) -> (rule8 % int2))) -> (rule7 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple3) -> (rule3 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((triple5) -> (rule1 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
((triple5) -> (rule6 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
((triple7) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
((triple13 triple15) -> (rule2 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
((triple13 ((triple11) -> (rule8 % int2))) -> (rule2 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
((((triple11) -> (rule3 % int2)) triple15) -> (rule2 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
((((triple14) -> (rule1 % int2)) triple15) -> (rule2 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
((((triple11) -> (rule3 % int3)) ((triple11) -> (rule8 % int2))) -> (rule2 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
((((triple14) -> (rule1 % int3)) ((triple11) -> (rule8 % int2))) -> (rule2 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int3
Anne is red.
("Anne" "is" "red" "+")
((((triple1) -> (rule3 % int3)) ((triple1) -> (rule8 % int2))) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3