Anne is big. Anne is quiet. Anne is white. Erin is blue. Erin is kind. Erin is nice. Erin is quiet. If Anne is smart then Anne is white. If someone is blue and big then they are smart. If Erin is kind and Erin is blue then Erin is white. All blue people are quiet. White people are nice. If someone is white then they are smart. If someone is white then they are quiet. Nice people are white.
Anne is big.
("Anne" "is" "big" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is white.
("Anne" "is" "white" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
If Anne is smart then Anne is white.
((("Anne" "is" "smart" "+")) -> ("Anne" "is" "white" "+"))
If someone is blue and big then they are smart.
((("someone" "is" "blue" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "smart" "+"))
If Erin is kind and Erin is blue then Erin is white.
((("Erin" "is" "kind" "+") ("Erin" "is" "blue" "+")) -> ("Erin" "is" "white" "+"))
All blue people are quiet.
((("someone" "is" "blue" "+")) -> ("someone" "is" "quiet" "+"))
White people are nice.
((("someone" "is" "white" "+")) -> ("someone" "is" "nice" "+"))
If someone is white then they are smart.
((("someone" "is" "white" "+")) -> ("someone" "is" "smart" "+"))
If someone is white then they are quiet.
((("someone" "is" "white" "+")) -> ("someone" "is" "quiet" "+"))
Nice people are white.
((("someone" "is" "nice" "+")) -> ("someone" "is" "white" "+"))
Anne is white.
True
1
proof
[(triple3)]
("Anne" "is" "white" "+")
triple3
Erin is not quiet.
False
1
inv-proof
[(triple7 OR ((triple4) -> rule4) OR ((((triple6) -> rule8)) -> rule7) OR ((((triple5 triple4) -> rule3)) -> rule7))]
("Erin" "is" "quiet" "-")
triple7
((triple4) -> (rule4 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((((triple6) -> (rule8 % int2))) -> (rule7 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
((((triple5 triple4) -> (rule3 % int2))) -> (rule7 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Anne is not blue.
Unknown
inv-random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "-")
Anne is kind.
Unknown
random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "+")
@0: Anne is big.[(triple1)] Anne is quiet.[(triple2 OR ((triple3) -> rule7))] Anne is white.[(triple3)] Erin is blue.[(triple4)] Erin is kind.[(triple5)] Erin is nice.[(triple6 OR ((((triple5 triple4) -> rule3)) -> rule5))] Erin is quiet.[(triple7 OR ((triple4) -> rule4) OR ((((triple6) -> rule8)) -> rule7) OR ((((triple5 triple4) -> rule3)) -> rule7))] @1: Anne is nice.[(((triple3) -> rule5))] Anne is smart.[(((triple3) -> rule6))] Erin is white.[(((triple6) -> rule8) OR ((triple5 triple4) -> rule3))] @2: Erin is smart.[(((((triple6) -> rule8)) -> rule6) OR ((((triple5 triple4) -> rule3)) -> rule6))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple2
((triple3) -> (rule7 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
triple3
Erin is blue.
("Erin" "is" "blue" "+")
triple4
Erin is kind.
("Erin" "is" "kind" "+")
triple5
Erin is nice.
("Erin" "is" "nice" "+")
triple6
((((triple5 triple4) -> (rule3 % int2))) -> (rule5 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is quiet.
("Erin" "is" "quiet" "+")
triple7
((triple4) -> (rule4 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((((triple6) -> (rule8 % int2))) -> (rule7 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
((((triple5 triple4) -> (rule3 % int2))) -> (rule7 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
((triple3) -> (rule5 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
((triple3) -> (rule6 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
((triple6) -> (rule8 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((triple5 triple4) -> (rule3 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
((((triple6) -> (rule8 % int2))) -> (rule6 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
((((triple5 triple4) -> (rule3 % int2))) -> (rule6 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2