Anne is nice. Charlie is big. Charlie is not nice. Charlie is not white. Dave is kind. Dave is white. Harry is big. Harry is green. Harry is kind. Harry is nice. All white things are nice. If Charlie is nice and Charlie is quiet then Charlie is green.
Anne is nice.
("Anne" "is" "nice" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is not nice.
("Charlie" "is" "nice" "-")
Charlie is not white.
("Charlie" "is" "white" "-")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is white.
("Dave" "is" "white" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is nice.
("Harry" "is" "nice" "+")
All white things are nice.
((("something" "is" "white" "+")) -> ("something" "is" "nice" "+"))
If Charlie is nice and Charlie is quiet then Charlie is green.
((("Charlie" "is" "nice" "+") ("Charlie" "is" "quiet" "+")) -> ("Charlie" "is" "green" "+"))
Dave is white.
True
1
proof
[(triple6)]
("Dave" "is" "white" "+")
triple6
Harry is not green.
False
1
inv-proof
[(triple8)]
("Harry" "is" "green" "-")
triple8
Charlie is not green.
Unknown
inv-rconc
[@1: Charlie is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "green" "-")
Charlie is quiet.
Unknown
random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "+")
@0: Anne is nice.[(triple1)] Charlie is big.[(triple2)] Charlie is not nice.[(triple3)] Charlie is not white.[(triple4)] Dave is kind.[(triple5)] Dave is white.[(triple6)] Harry is big.[(triple7)] Harry is green.[(triple8)] Harry is kind.[(triple9)] Harry is nice.[(triple10)] @1: Dave is nice.[(((triple6) -> rule1))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Charlie is big.
("Charlie" "is" "big" "+")
triple2
Charlie is not nice.
("Charlie" "is" "nice" "-")
triple3
Charlie is not white.
("Charlie" "is" "white" "-")
triple4
Dave is kind.
("Dave" "is" "kind" "+")
triple5
Dave is white.
("Dave" "is" "white" "+")
triple6
Harry is big.
("Harry" "is" "big" "+")
triple7
Harry is green.
("Harry" "is" "green" "+")
triple8
Harry is kind.
("Harry" "is" "kind" "+")
triple9
Harry is nice.
("Harry" "is" "nice" "+")
triple10
Dave is nice.
("Dave" "is" "nice" "+")
((triple6) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1