Anne is big. Anne is blue. Anne is cold. Anne is green. Anne is red. Anne is smart. Anne is white. Dave is big. Dave is blue. Dave is cold. Dave is smart. Erin is big. Erin is blue. Erin is smart. Erin is white. If Anne is green and Anne is big then Anne is blue. All smart, cold people are green. All red people are smart. If Dave is smart then Dave is green. If someone is blue and red then they are smart. If someone is blue then they are green. If Erin is red and Erin is cold then Erin is white. All blue, smart people are green.
Anne is big.
("Anne" "is" "big" "+")
Anne is blue.
("Anne" "is" "blue" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is white.
("Anne" "is" "white" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Erin is white.
("Erin" "is" "white" "+")
If Anne is green and Anne is big then Anne is blue.
((("Anne" "is" "green" "+") ("Anne" "is" "big" "+")) -> ("Anne" "is" "blue" "+"))
All smart, cold people are green.
((("someone" "is" "smart" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "green" "+"))
All red people are smart.
((("someone" "is" "red" "+")) -> ("someone" "is" "smart" "+"))
If Dave is smart then Dave is green.
((("Dave" "is" "smart" "+")) -> ("Dave" "is" "green" "+"))
If someone is blue and red then they are smart.
((("someone" "is" "blue" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "smart" "+"))
If someone is blue then they are green.
((("someone" "is" "blue" "+")) -> ("someone" "is" "green" "+"))
If Erin is red and Erin is cold then Erin is white.
((("Erin" "is" "red" "+") ("Erin" "is" "cold" "+")) -> ("Erin" "is" "white" "+"))
All blue, smart people are green.
((("someone" "is" "blue" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "green" "+"))
Dave is blue.
True
1
proof
[(triple9)]
("Dave" "is" "blue" "+")
triple9
Erin is not blue.
False
1
inv-proof
[(triple13)]
("Erin" "is" "blue" "-")
triple13
Dave is not red.
Unknown
inv-random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "-")
Erin is red.
Unknown
random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "+")
@0: Anne is big.[(triple1)] Anne is blue.[(triple2 OR ((triple4 triple1) -> rule1) OR ((((triple6 triple3) -> rule2) triple1) -> rule1) OR ((((((triple5) -> rule3) triple3) -> rule2) triple1) -> rule1))] Anne is cold.[(triple3)] Anne is green.[(triple4 OR ((triple2) -> rule6) OR ((triple2 triple6) -> rule8) OR ((triple6 triple3) -> rule2) OR ((triple2 ((triple5) -> rule3)) -> rule8) OR ((triple2 ((triple2 triple5) -> rule5)) -> rule8) OR ((((triple5) -> rule3) triple3) -> rule2) OR ((((triple2 triple5) -> rule5) triple3) -> rule2))] Anne is red.[(triple5)] Anne is smart.[(triple6 OR ((triple5) -> rule3) OR ((triple2 triple5) -> rule5) OR ((((triple4 triple1) -> rule1) triple5) -> rule5))] Anne is white.[(triple7)] Dave is big.[(triple8)] Dave is blue.[(triple9)] Dave is cold.[(triple10)] Dave is smart.[(triple11)] Erin is big.[(triple12)] Erin is blue.[(triple13)] Erin is smart.[(triple14)] Erin is white.[(triple15)] @1: Dave is green.[(((triple11) -> rule4) OR ((triple9) -> rule6) OR ((triple11 triple10) -> rule2) OR ((triple9 triple11) -> rule8))] Erin is green.[(((triple13) -> rule6) OR ((triple13 triple14) -> rule8))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is blue.
("Anne" "is" "blue" "+")
triple2
((triple4 triple1) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
((((triple6 triple3) -> (rule2 % int2)) triple1) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
((((((triple5) -> (rule3 % int3)) triple3) -> (rule2 % int2)) triple1) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is cold.
("Anne" "is" "cold" "+")
triple3
Anne is green.
("Anne" "is" "green" "+")
triple4
((triple2) -> (rule6 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
((triple2 triple6) -> (rule8 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
((triple6 triple3) -> (rule2 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
((triple2 ((triple5) -> (rule3 % int2))) -> (rule8 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
((triple2 ((triple2 triple5) -> (rule5 % int2))) -> (rule8 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
((((triple5) -> (rule3 % int2)) triple3) -> (rule2 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
((((triple2 triple5) -> (rule5 % int2)) triple3) -> (rule2 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
triple5
Anne is smart.
("Anne" "is" "smart" "+")
triple6
((triple5) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
((triple2 triple5) -> (rule5 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
((((triple4 triple1) -> (rule1 % int2)) triple5) -> (rule5 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
triple7
Dave is big.
("Dave" "is" "big" "+")
triple8
Dave is blue.
("Dave" "is" "blue" "+")
triple9
Dave is cold.
("Dave" "is" "cold" "+")
triple10
Dave is smart.
("Dave" "is" "smart" "+")
triple11
Erin is big.
("Erin" "is" "big" "+")
triple12
Erin is blue.
("Erin" "is" "blue" "+")
triple13
Erin is smart.
("Erin" "is" "smart" "+")
triple14
Erin is white.
("Erin" "is" "white" "+")
triple15
Dave is green.
("Dave" "is" "green" "+")
((triple11) -> (rule4 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((triple9) -> (rule6 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((triple11 triple10) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((triple9 triple11) -> (rule8 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
((triple13) -> (rule6 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
((triple13 triple14) -> (rule8 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1