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