Gary is green. Gary is quiet. Harry is red. If Harry is nice and Harry is round then Harry is kind. If something is nice then it is quiet. If something is red and nice then it is quiet. If something is quiet and not green then it is red. If Harry is not green then Harry is quiet. If Gary is green then Gary is kind. If Gary is round and Gary is green then Gary is white. All quiet things are not nice.
Gary is green.
("Gary" "is" "green" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Harry is red.
("Harry" "is" "red" "+")
If Harry is nice and Harry is round then Harry is kind.
((("Harry" "is" "nice" "+") ("Harry" "is" "round" "+")) -> ("Harry" "is" "kind" "+"))
If something is nice then it is quiet.
((("something" "is" "nice" "+")) -> ("something" "is" "quiet" "+"))
If something is red and nice then it is quiet.
((("something" "is" "red" "+") ("something" "is" "nice" "+")) -> ("something" "is" "quiet" "+"))
If something is quiet and not green then it is red.
((("something" "is" "quiet" "+") ("something" "is" "green" "~")) -> ("something" "is" "red" "+"))
If Harry is not green then Harry is quiet.
((("Harry" "is" "green" "~")) -> ("Harry" "is" "quiet" "+"))
If Gary is green then Gary is kind.
((("Gary" "is" "green" "+")) -> ("Gary" "is" "kind" "+"))
If Gary is round and Gary is green then Gary is white.
((("Gary" "is" "round" "+") ("Gary" "is" "green" "+")) -> ("Gary" "is" "white" "+"))
All quiet things are not nice.
((("something" "is" "quiet" "+")) -> ("something" "is" "nice" "-"))
Gary is quiet.
True
1
proof
[(triple2)]
("Gary" "is" "quiet" "+")
triple2
Harry is not red.
False
1
inv-proof
[(triple3)]
("Harry" "is" "red" "-")
triple3
Gary is not nice.
True
2
proof
[(((triple2) -> rule8))]
("Gary" "is" "nice" "-")
((triple2) -> (rule8 % int1))
Gary is not nice.
("Gary" "is" "nice" "-")
int1
Gary is nice.
False
2
inv-proof
[(((triple2) -> rule8))]
("Gary" "is" "nice" "+")
((triple2) -> (rule8 % int1))
Gary is not nice.
("Gary" "is" "nice" "-")
int1
Gary is not red.
Unknown
inv-rconc
[@1: Gary is red.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "red" "-")
Gary is white.
Unknown
rconc
[@1: Gary is white.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Gary" "is" "white" "+")
Harry is not nice.
Unknown
inv-random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "-")
Harry is white.
Unknown
random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "+")
@0: Gary is green.[(triple1)] Gary is quiet.[(triple2)] Harry is red.[(triple3)] @1: Gary is kind.[(((triple1) -> rule6))] Gary is not nice.[(((triple2) -> rule8))]
Gary is green.
("Gary" "is" "green" "+")
triple1
Gary is quiet.
("Gary" "is" "quiet" "+")
triple2
Harry is red.
("Harry" "is" "red" "+")
triple3
Gary is kind.
("Gary" "is" "kind" "+")
((triple1) -> (rule6 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is not nice.
("Gary" "is" "nice" "-")
((triple2) -> (rule8 % int1))
Gary is not nice.
("Gary" "is" "nice" "-")
int1