Dave is not cold. Dave is green. Dave is kind. Dave is red. Dave is round. Gary is quiet. Gary is smart. If Dave is red and Dave is round then Dave is not smart.
Dave is not cold.
("Dave" "is" "cold" "-")
Dave is green.
("Dave" "is" "green" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is round.
("Dave" "is" "round" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is smart.
("Gary" "is" "smart" "+")
If Dave is red and Dave is round then Dave is not smart.
((("Dave" "is" "red" "+") ("Dave" "is" "round" "+")) -> ("Dave" "is" "smart" "-"))
Gary is quiet.
True
1
proof
[(triple6)]
("Gary" "is" "quiet" "+")
triple6
Dave is cold.
False
1
inv-proof
[(triple1)]
("Dave" "is" "cold" "+")
triple1
Dave is not smart.
True
3
proof
[(((triple4 triple5) -> rule1))]
("Dave" "is" "smart" "-")
((triple4 triple5) -> (rule1 % int1))
Dave is not smart.
("Dave" "is" "smart" "-")
int1
Dave is smart.
False
3
inv-proof
[(((triple4 triple5) -> rule1))]
("Dave" "is" "smart" "+")
((triple4 triple5) -> (rule1 % int1))
Dave is not smart.
("Dave" "is" "smart" "-")
int1
Dave is not quiet.
Unknown
inv-random
[@0: Dave is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "quiet" "-")
Gary is cold.
Unknown
random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "+")
Gary is not kind.
Unknown
inv-random
[@0: Gary is kind.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "kind" "-")
Gary is green.
Unknown
random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "+")
@0: Dave is green.[(triple2)] Dave is kind.[(triple3)] Dave is not cold.[(triple1)] Dave is red.[(triple4)] Dave is round.[(triple5)] Gary is quiet.[(triple6)] Gary is smart.[(triple7)] @1: Dave is not smart.[(((triple4 triple5) -> rule1))]
Dave is green.
("Dave" "is" "green" "+")
triple2
Dave is kind.
("Dave" "is" "kind" "+")
triple3
Dave is not cold.
("Dave" "is" "cold" "-")
triple1
Dave is red.
("Dave" "is" "red" "+")
triple4
Dave is round.
("Dave" "is" "round" "+")
triple5
Gary is quiet.
("Gary" "is" "quiet" "+")
triple6
Gary is smart.
("Gary" "is" "smart" "+")
triple7
Dave is not smart.
("Dave" "is" "smart" "-")
((triple4 triple5) -> (rule1 % int1))
Dave is not smart.
("Dave" "is" "smart" "-")
int1