Anne is round. Anne is white. Harry is green. If Harry is round and Harry is red then Harry is quiet. Quiet things are rough. If something is red then it is rough. All nice, rough things are red. All round things are nice. All white things are green.
Anne is round.
("Anne" "is" "round" "+")
Anne is white.
("Anne" "is" "white" "+")
Harry is green.
("Harry" "is" "green" "+")
If Harry is round and Harry is red then Harry is quiet.
((("Harry" "is" "round" "+") ("Harry" "is" "red" "+")) -> ("Harry" "is" "quiet" "+"))
Quiet things are rough.
((("something" "is" "quiet" "+")) -> ("something" "is" "rough" "+"))
If something is red then it is rough.
((("something" "is" "red" "+")) -> ("something" "is" "rough" "+"))
All nice, rough things are red.
((("something" "is" "nice" "+") ("something" "is" "rough" "+")) -> ("something" "is" "red" "+"))
All round things are nice.
((("something" "is" "round" "+")) -> ("something" "is" "nice" "+"))
All white things are green.
((("something" "is" "white" "+")) -> ("something" "is" "green" "+"))
Anne is round.
True
1
proof
[(triple1)]
("Anne" "is" "round" "+")
triple1
Harry is not green.
False
1
inv-proof
[(triple3)]
("Harry" "is" "green" "-")
triple3
Harry is not quiet.
Unknown
inv-rconc
[@1: Harry is quiet.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "quiet" "-")
Anne is quiet.
Unknown
random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "+")
@0: Anne is round.[(triple1)] Anne is white.[(triple2)] Harry is green.[(triple3)] @1: Anne is green.[(((triple2) -> rule6))] Anne is nice.[(((triple1) -> rule5))]
Anne is round.
("Anne" "is" "round" "+")
triple1
Anne is white.
("Anne" "is" "white" "+")
triple2
Harry is green.
("Harry" "is" "green" "+")
triple3
Anne is green.
("Anne" "is" "green" "+")
((triple2) -> (rule6 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
((triple1) -> (rule5 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1