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