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