Anne is blue. Anne is furry. Anne is green. Anne is kind. Anne is quiet. Anne is red. Anne is smart. Dave is furry. Dave is green. Dave is kind. Dave is red. Dave is smart. Gary is blue. Gary is red. Gary is smart. Red things are smart. If something is smart and kind then it is green. All red things are kind.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Red things are smart.
((("something" "is" "red" "+")) -> ("something" "is" "smart" "+"))
If something is smart and kind then it is green.
((("something" "is" "smart" "+") ("something" "is" "kind" "+")) -> ("something" "is" "green" "+"))
All red things are kind.
((("something" "is" "red" "+")) -> ("something" "is" "kind" "+"))
Gary is red.
True
1
proof
[(triple14)]
("Gary" "is" "red" "+")
triple14
Gary is not smart.
False
1
inv-proof
[(triple15 OR ((triple14) -> rule1))]
("Gary" "is" "smart" "-")
triple15
((triple14) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is kind.
True
2
proof
[(((triple14) -> rule3))]
("Gary" "is" "kind" "+")
((triple14) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is not kind.
False
2
inv-proof
[(((triple14) -> rule3))]
("Gary" "is" "kind" "-")
((triple14) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is green.
True
4
proof
[(((triple15 ((triple14) -> rule3)) -> rule2) OR ((((triple14) -> rule1) ((triple14) -> rule3)) -> rule2))]
("Gary" "is" "green" "+")
((triple15 ((triple14) -> (rule3 % int2))) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
((((triple14) -> (rule1 % int3)) ((triple14) -> (rule3 % int2))) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is not green.
False
4
inv-proof
[(((triple15 ((triple14) -> rule3)) -> rule2) OR ((((triple14) -> rule1) ((triple14) -> rule3)) -> rule2))]
("Gary" "is" "green" "-")
((triple15 ((triple14) -> (rule3 % int2))) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
((((triple14) -> (rule1 % int3)) ((triple14) -> (rule3 % int2))) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Dave is not blue.
Unknown
inv-random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "-")
Dave is quiet.
Unknown
random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "+")
Gary is not quiet.
Unknown
inv-random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "-")
Gary is furry.
Unknown
random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "+")
@0: Anne is blue.[(triple1)] Anne is furry.[(triple2)] Anne is green.[(triple3 OR ((triple7 triple4) -> rule2) OR ((triple7 ((triple6) -> rule3)) -> rule2) OR ((((triple6) -> rule1) triple4) -> rule2) OR ((((triple6) -> rule1) ((triple6) -> rule3)) -> rule2))] Anne is kind.[(triple4 OR ((triple6) -> rule3))] Anne is quiet.[(triple5)] Anne is red.[(triple6)] Anne is smart.[(triple7 OR ((triple6) -> rule1))] Dave is furry.[(triple8)] Dave is green.[(triple9 OR ((triple12 triple10) -> rule2) OR ((triple12 ((triple11) -> rule3)) -> rule2) OR ((((triple11) -> rule1) triple10) -> rule2) OR ((((triple11) -> rule1) ((triple11) -> rule3)) -> rule2))] Dave is kind.[(triple10 OR ((triple11) -> rule3))] Dave is red.[(triple11)] Dave is smart.[(triple12 OR ((triple11) -> rule1))] Gary is blue.[(triple13)] Gary is red.[(triple14)] Gary is smart.[(triple15 OR ((triple14) -> rule1))] @1: Gary is kind.[(((triple14) -> rule3))] @2: Gary is green.[(((triple15 ((triple14) -> rule3)) -> rule2) OR ((((triple14) -> rule1) ((triple14) -> rule3)) -> rule2))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is furry.
("Anne" "is" "furry" "+")
triple2
Anne is green.
("Anne" "is" "green" "+")
triple3
((triple7 triple4) -> (rule2 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
((triple7 ((triple6) -> (rule3 % int2))) -> (rule2 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
((((triple6) -> (rule1 % int2)) triple4) -> (rule2 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
((((triple6) -> (rule1 % int3)) ((triple6) -> (rule3 % int2))) -> (rule2 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is kind.
("Anne" "is" "kind" "+")
triple4
((triple6) -> (rule3 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple5
Anne is red.
("Anne" "is" "red" "+")
triple6
Anne is smart.
("Anne" "is" "smart" "+")
triple7
((triple6) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
triple8
Dave is green.
("Dave" "is" "green" "+")
triple9
((triple12 triple10) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
((triple12 ((triple11) -> (rule3 % int2))) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
((((triple11) -> (rule1 % int2)) triple10) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
((((triple11) -> (rule1 % int3)) ((triple11) -> (rule3 % int2))) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
triple10
((triple11) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
triple11
Dave is smart.
("Dave" "is" "smart" "+")
triple12
((triple11) -> (rule1 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Gary is blue.
("Gary" "is" "blue" "+")
triple13
Gary is red.
("Gary" "is" "red" "+")
triple14
Gary is smart.
("Gary" "is" "smart" "+")
triple15
((triple14) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
((triple14) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is green.
("Gary" "is" "green" "+")
((triple15 ((triple14) -> (rule3 % int2))) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
((((triple14) -> (rule1 % int3)) ((triple14) -> (rule3 % int2))) -> (rule2 % int1))
Gary is green.
("Gary" "is" "green" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3