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