Dave is kind. Erin is kind. Harry is quiet. If Harry is big and Harry is kind then Harry is quiet. All rough things are quiet. Quiet things are green. If something is rough and green then it is kind. If Harry is blue then Harry is not green. If something is blue then it is rough.
Dave is kind.
("Dave" "is" "kind" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
If Harry is big and Harry is kind then Harry is quiet.
((("Harry" "is" "big" "+") ("Harry" "is" "kind" "+")) -> ("Harry" "is" "quiet" "+"))
All rough things are quiet.
((("something" "is" "rough" "+")) -> ("something" "is" "quiet" "+"))
Quiet things are green.
((("something" "is" "quiet" "+")) -> ("something" "is" "green" "+"))
If something is rough and green then it is kind.
((("something" "is" "rough" "+") ("something" "is" "green" "+")) -> ("something" "is" "kind" "+"))
If Harry is blue then Harry is not green.
((("Harry" "is" "blue" "+")) -> ("Harry" "is" "green" "-"))
If something is blue then it is rough.
((("something" "is" "blue" "+")) -> ("something" "is" "rough" "+"))
Dave is kind.
True
1
proof
[(triple1)]
("Dave" "is" "kind" "+")
triple1
Erin is not kind.
False
1
inv-proof
[(triple2)]
("Erin" "is" "kind" "-")
triple2
Dave is not green.
Unknown
inv-rconc
[@3: Dave is green.[CWA. Example of deepest failure = (rule3 <- rule2 <- rule6 <- FAIL)]]
("Dave" "is" "green" "-")
Dave is furry.
Unknown
random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "+")
@0: Dave is kind.[(triple1)] Erin is kind.[(triple2)] Harry is quiet.[(triple3)] @1: Harry is green.[(((triple3) -> rule3))]
Dave is kind.
("Dave" "is" "kind" "+")
triple1
Erin is kind.
("Erin" "is" "kind" "+")
triple2
Harry is quiet.
("Harry" "is" "quiet" "+")
triple3
Harry is green.
("Harry" "is" "green" "+")
((triple3) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1