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