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