Dave is furry. Gary is furry. Gary is kind. All cold, quiet people are furry. Furry people are white. If someone is green then they are kind. If Dave is blue then Dave is kind. If someone is furry and white then they are blue. If someone is cold then they are furry.
Dave is furry.
("Dave" "is" "furry" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is kind.
("Gary" "is" "kind" "+")
All cold, quiet people are furry.
((("someone" "is" "cold" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "furry" "+"))
Furry people are white.
((("someone" "is" "furry" "+")) -> ("someone" "is" "white" "+"))
If someone is green then they are kind.
((("someone" "is" "green" "+")) -> ("someone" "is" "kind" "+"))
If Dave is blue then Dave is kind.
((("Dave" "is" "blue" "+")) -> ("Dave" "is" "kind" "+"))
If someone is furry and white then they are blue.
((("someone" "is" "furry" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "blue" "+"))
If someone is cold then they are furry.
((("someone" "is" "cold" "+")) -> ("someone" "is" "furry" "+"))
Gary is kind.
True
1
proof
[(triple3)]
("Gary" "is" "kind" "+")
triple3
Gary is not furry.
False
1
inv-proof
[(triple2)]
("Gary" "is" "furry" "-")
triple2
Gary is white.
True
2
proof
[(((triple2) -> rule2))]
("Gary" "is" "white" "+")
((triple2) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is not white.
False
2
inv-proof
[(((triple2) -> rule2))]
("Gary" "is" "white" "-")
((triple2) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Dave is blue.
True
4
proof
[(((triple1 ((triple1) -> rule2)) -> rule5))]
("Dave" "is" "blue" "+")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is not blue.
False
4
inv-proof
[(((triple1 ((triple1) -> rule2)) -> rule5))]
("Dave" "is" "blue" "-")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Gary is not green.
Unknown
inv-random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "-")
Dave is cold.
Unknown
random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "+")
Dave is not quiet.
Unknown
inv-random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "-")
Dave is green.
Unknown
random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "+")
Gary is not cold.
Unknown
inv-random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "-")
Gary is quiet.
Unknown
random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "+")
@0: Dave is furry.[(triple1)] Gary is furry.[(triple2)] Gary is kind.[(triple3)] @1: Dave is white.[(((triple1) -> rule2))] Gary is white.[(((triple2) -> rule2))] @2: Dave is blue.[(((triple1 ((triple1) -> rule2)) -> rule5))] Gary is blue.[(((triple2 ((triple2) -> rule2)) -> rule5))] @3: Dave is kind.[(((((triple1 ((triple1) -> rule2)) -> rule5)) -> rule4))]
Dave is furry.
("Dave" "is" "furry" "+")
triple1
Gary is furry.
("Gary" "is" "furry" "+")
triple2
Gary is kind.
("Gary" "is" "kind" "+")
triple3
Dave is white.
("Dave" "is" "white" "+")
((triple1) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
((triple2) -> (rule2 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
((triple2 ((triple2) -> (rule2 % int2))) -> (rule5 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
((((triple1 ((triple1) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is white.
("Dave" "is" "white" "+")
int3