Charlie is nice. Fiona is nice. Harry is green. If something is kind then it is red. If Harry is rough and Harry is red then Harry is blue. If Fiona is green and Fiona is blue then Fiona is nice. If Fiona is green then Fiona is rough. If something is quiet and green then it is nice. If something is blue then it is nice.
Charlie is nice.
("Charlie" "is" "nice" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Harry is green.
("Harry" "is" "green" "+")
If something is kind then it is red.
((("something" "is" "kind" "+")) -> ("something" "is" "red" "+"))
If Harry is rough and Harry is red then Harry is blue.
((("Harry" "is" "rough" "+") ("Harry" "is" "red" "+")) -> ("Harry" "is" "blue" "+"))
If Fiona is green and Fiona is blue then Fiona is nice.
((("Fiona" "is" "green" "+") ("Fiona" "is" "blue" "+")) -> ("Fiona" "is" "nice" "+"))
If Fiona is green then Fiona is rough.
((("Fiona" "is" "green" "+")) -> ("Fiona" "is" "rough" "+"))
If something is quiet and green then it is nice.
((("something" "is" "quiet" "+") ("something" "is" "green" "+")) -> ("something" "is" "nice" "+"))
If something is blue then it is nice.
((("something" "is" "blue" "+")) -> ("something" "is" "nice" "+"))
Charlie is nice.
True
1
proof
[(triple1)]
("Charlie" "is" "nice" "+")
triple1
Harry is not green.
False
1
inv-proof
[(triple3)]
("Harry" "is" "green" "-")
triple3
Harry is not nice.
Unknown
inv-rconc
[@2: Harry is nice.[CWA. Example of deepest failure = (rule6 <- rule2 <- FAIL)]]
("Harry" "is" "nice" "-")
Charlie is green.
Unknown
random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "+")
@0: Charlie is nice.[(triple1)] Fiona is nice.[(triple2)] Harry is green.[(triple3)]
Charlie is nice.
("Charlie" "is" "nice" "+")
triple1
Fiona is nice.
("Fiona" "is" "nice" "+")
triple2
Harry is green.
("Harry" "is" "green" "+")
triple3