Dave is red. Gary is kind. Gary is rough. If Gary is not kind and Gary is not rough then Gary is not round. Rough people are smart. If someone is red and not young then they are round.
Dave is red.
("Dave" "is" "red" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is rough.
("Gary" "is" "rough" "+")
If Gary is not kind and Gary is not rough then Gary is not round.
((("Gary" "is" "kind" "~") ("Gary" "is" "rough" "~")) -> ("Gary" "is" "round" "-"))
Rough people are smart.
((("someone" "is" "rough" "+")) -> ("someone" "is" "smart" "+"))
If someone is red and not young then they are round.
((("someone" "is" "red" "+") ("someone" "is" "young" "~")) -> ("someone" "is" "round" "+"))
Gary is rough.
True
1
proof
[(triple3)]
("Gary" "is" "rough" "+")
triple3
Gary is not kind.
False
1
inv-proof
[(triple2)]
("Gary" "is" "kind" "-")
triple2
Gary is smart.
True
2
proof
[(((triple3) -> rule2))]
("Gary" "is" "smart" "+")
((triple3) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is not smart.
False
2
inv-proof
[(((triple3) -> rule2))]
("Gary" "is" "smart" "-")
((triple3) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Dave is not smart.
Unknown
inv-rconc
[@1: Dave is smart.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "smart" "-")
Gary is round.
Unknown
rconc
[@1: Gary is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "round" "+")
Dave is not kind.
Unknown
inv-random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "-")
Gary is red.
Unknown
random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "+")
@0: Dave is red.[(triple1)] Gary is kind.[(triple2)] Gary is rough.[(triple3)] @1: Gary is smart.[(((triple3) -> rule2))]
Dave is red.
("Dave" "is" "red" "+")
triple1
Gary is kind.
("Gary" "is" "kind" "+")
triple2
Gary is rough.
("Gary" "is" "rough" "+")
triple3
Gary is smart.
("Gary" "is" "smart" "+")
((triple3) -> (rule2 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1