Anne is not big. Anne is green. Anne is quiet. Bob is green. Bob is not nice. Bob is quiet. Bob is smart. Erin is blue. Erin is nice. Erin is quiet. All green, quiet people are not nice. If someone is green then they are blue. If Anne is quiet then Anne is smart. If Anne is big then Anne is not quiet. All blue people are not red. Nice, green people are red.
Anne is not big.
("Anne" "is" "big" "-")
Anne is green.
("Anne" "is" "green" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is not nice.
("Bob" "is" "nice" "-")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
All green, quiet people are not nice.
((("someone" "is" "green" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "nice" "-"))
If someone is green then they are blue.
((("someone" "is" "green" "+")) -> ("someone" "is" "blue" "+"))
If Anne is quiet then Anne is smart.
((("Anne" "is" "quiet" "+")) -> ("Anne" "is" "smart" "+"))
If Anne is big then Anne is not quiet.
((("Anne" "is" "big" "+")) -> ("Anne" "is" "quiet" "-"))
All blue people are not red.
((("someone" "is" "blue" "+")) -> ("someone" "is" "red" "-"))
Nice, green people are red.
((("someone" "is" "nice" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "red" "+"))
Bob is smart.
True
1
proof
[(triple7)]
("Bob" "is" "smart" "+")
triple7
Bob is not quiet.
False
1
inv-proof
[(triple6)]
("Bob" "is" "quiet" "-")
triple6
Bob is blue.
True
2
proof
[(((triple4) -> rule2))]
("Bob" "is" "blue" "+")
((triple4) -> (rule2 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Erin is red.
False
2
inv-proof
[(((triple8) -> rule5))]
("Erin" "is" "red" "+")
((triple8) -> (rule5 % int1))
Erin is not red.
("Erin" "is" "red" "-")
int1
Bob is not red.
True
3
proof
[(((((triple4) -> rule2)) -> rule5))]
("Bob" "is" "red" "-")
((((triple4) -> (rule2 % int2))) -> (rule5 % int1))
Bob is not red.
("Bob" "is" "red" "-")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Anne is red.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule5))]
("Anne" "is" "red" "+")
((((triple2) -> (rule2 % int2))) -> (rule5 % int1))
Anne is not red.
("Anne" "is" "red" "-")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Erin is not smart.
Unknown
inv-random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "-")
Erin is green.
Unknown
random
[@0: Erin is green.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "green" "+")
Bob is not big.
Unknown
inv-random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "-")
Erin is big.
Unknown
random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "+")
@0: Anne is green.[(triple2)] Anne is not big.[(triple1)] Anne is quiet.[(triple3)] Bob is green.[(triple4)] Bob is not nice.[(triple5 OR ((triple4 triple6) -> rule1))] Bob is quiet.[(triple6)] Bob is smart.[(triple7)] Erin is blue.[(triple8)] Erin is nice.[(triple9)] Erin is quiet.[(triple10)] @1: Anne is blue.[(((triple2) -> rule2))] Anne is not nice.[(((triple2 triple3) -> rule1))] Anne is smart.[(((triple3) -> rule3))] Bob is blue.[(((triple4) -> rule2))] Erin is not red.[(((triple8) -> rule5))] @2: Anne is not red.[(((((triple2) -> rule2)) -> rule5))] Bob is not red.[(((((triple4) -> rule2)) -> rule5))]
Anne is green.
("Anne" "is" "green" "+")
triple2
Anne is not big.
("Anne" "is" "big" "-")
triple1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple3
Bob is green.
("Bob" "is" "green" "+")
triple4
Bob is not nice.
("Bob" "is" "nice" "-")
triple5
((triple4 triple6) -> (rule1 % int1))
Bob is not nice.
("Bob" "is" "nice" "-")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple6
Bob is smart.
("Bob" "is" "smart" "+")
triple7
Erin is blue.
("Erin" "is" "blue" "+")
triple8
Erin is nice.
("Erin" "is" "nice" "+")
triple9
Erin is quiet.
("Erin" "is" "quiet" "+")
triple10
Anne is blue.
("Anne" "is" "blue" "+")
((triple2) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is not nice.
("Anne" "is" "nice" "-")
((triple2 triple3) -> (rule1 % int1))
Anne is not nice.
("Anne" "is" "nice" "-")
int1
Anne is smart.
("Anne" "is" "smart" "+")
((triple3) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
((triple4) -> (rule2 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Erin is not red.
("Erin" "is" "red" "-")
((triple8) -> (rule5 % int1))
Erin is not red.
("Erin" "is" "red" "-")
int1
Anne is not red.
("Anne" "is" "red" "-")
((((triple2) -> (rule2 % int2))) -> (rule5 % int1))
Anne is not red.
("Anne" "is" "red" "-")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Bob is not red.
("Bob" "is" "red" "-")
((((triple4) -> (rule2 % int2))) -> (rule5 % int1))
Bob is not red.
("Bob" "is" "red" "-")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2