Gary is not green. Gary is not nice. Gary is not rough. Gary is not round. Harry is green. Harry is rough. Harry is round. If something is rough and round then it is kind. If something is round and not big then it is kind. If something is rough and not red then it is kind. If something is nice and red then it is round. If Harry is not big then Harry is round. If Gary is round then Gary is not rough.
Gary is not green.
("Gary" "is" "green" "-")
Gary is not nice.
("Gary" "is" "nice" "-")
Gary is not rough.
("Gary" "is" "rough" "-")
Gary is not round.
("Gary" "is" "round" "-")
Harry is green.
("Harry" "is" "green" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is round.
("Harry" "is" "round" "+")
If something is rough and round then it is kind.
((("something" "is" "rough" "+") ("something" "is" "round" "+")) -> ("something" "is" "kind" "+"))
If something is round and not big then it is kind.
((("something" "is" "round" "+") ("something" "is" "big" "~")) -> ("something" "is" "kind" "+"))
If something is rough and not red then it is kind.
((("something" "is" "rough" "+") ("something" "is" "red" "~")) -> ("something" "is" "kind" "+"))
If something is nice and red then it is round.
((("something" "is" "nice" "+") ("something" "is" "red" "+")) -> ("something" "is" "round" "+"))
If Harry is not big then Harry is round.
((("Harry" "is" "big" "~")) -> ("Harry" "is" "round" "+"))
If Gary is round then Gary is not rough.
((("Gary" "is" "round" "+")) -> ("Gary" "is" "rough" "-"))
Gary is not round.
True
1
proof
[(triple4)]
("Gary" "is" "round" "-")
triple4
Gary is nice.
False
1
inv-proof
[(triple2)]
("Gary" "is" "nice" "+")
triple2
Harry is kind.
True
3
proof
[(((triple6 triple7) -> rule1))]
("Harry" "is" "kind" "+")
((triple6 triple7) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is not kind.
False
3
inv-proof
[(((triple6 triple7) -> rule1))]
("Harry" "is" "kind" "-")
((triple6 triple7) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Gary is not kind.
Unknown
inv-rconc
[@1: Gary is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "kind" "-")
Harry is red.
Unknown
random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "+")
Harry is not big.
Unknown
inv-random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "-")
Gary is big.
Unknown
random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "+")
@0: Gary is not green.[(triple1)] Gary is not nice.[(triple2)] Gary is not rough.[(triple3)] Gary is not round.[(triple4)] Harry is green.[(triple5)] Harry is rough.[(triple6)] Harry is round.[(triple7)] @1: Harry is kind.[(((triple6 triple7) -> rule1))]
Gary is not green.
("Gary" "is" "green" "-")
triple1
Gary is not nice.
("Gary" "is" "nice" "-")
triple2
Gary is not rough.
("Gary" "is" "rough" "-")
triple3
Gary is not round.
("Gary" "is" "round" "-")
triple4
Harry is green.
("Harry" "is" "green" "+")
triple5
Harry is rough.
("Harry" "is" "rough" "+")
triple6
Harry is round.
("Harry" "is" "round" "+")
triple7
Harry is kind.
("Harry" "is" "kind" "+")
((triple6 triple7) -> (rule1 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1