Anne is nice. Anne is not quiet. Anne is white. Charlie is blue. Harry is big. Harry is green. Harry is not nice. Harry is quiet. Harry is round. Harry is not white. If Charlie is blue and Charlie is not green then Charlie is nice. If someone is blue and white then they are big. Nice people are not round.
Anne is nice.
("Anne" "is" "nice" "+")
Anne is not quiet.
("Anne" "is" "quiet" "-")
Anne is white.
("Anne" "is" "white" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is not nice.
("Harry" "is" "nice" "-")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is not white.
("Harry" "is" "white" "-")
If Charlie is blue and Charlie is not green then Charlie is nice.
((("Charlie" "is" "blue" "+") ("Charlie" "is" "green" "~")) -> ("Charlie" "is" "nice" "+"))
If someone is blue and white then they are big.
((("someone" "is" "blue" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "big" "+"))
Nice people are not round.
((("someone" "is" "nice" "+")) -> ("someone" "is" "round" "-"))
Anne is white.
True
1
proof
[(triple3)]
("Anne" "is" "white" "+")
triple3
Harry is nice.
False
1
inv-proof
[(triple7)]
("Harry" "is" "nice" "+")
triple7
Charlie is not nice.
Unknown
inv-rconc
[@1: Charlie is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "nice" "-")
Anne is green.
Unknown
random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "+")
@0: Anne is nice.[(triple1)] Anne is not quiet.[(triple2)] Anne is white.[(triple3)] Charlie is blue.[(triple4)] Harry is big.[(triple5)] Harry is green.[(triple6)] Harry is not nice.[(triple7)] Harry is not white.[(triple10)] Harry is quiet.[(triple8)] Harry is round.[(triple9)] @1: Anne is not round.[(((triple1) -> rule3))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Anne is not quiet.
("Anne" "is" "quiet" "-")
triple2
Anne is white.
("Anne" "is" "white" "+")
triple3
Charlie is blue.
("Charlie" "is" "blue" "+")
triple4
Harry is big.
("Harry" "is" "big" "+")
triple5
Harry is green.
("Harry" "is" "green" "+")
triple6
Harry is not nice.
("Harry" "is" "nice" "-")
triple7
Harry is not white.
("Harry" "is" "white" "-")
triple10
Harry is quiet.
("Harry" "is" "quiet" "+")
triple8
Harry is round.
("Harry" "is" "round" "+")
triple9
Anne is not round.
("Anne" "is" "round" "-")
((triple1) -> (rule3 % int1))
Anne is not round.
("Anne" "is" "round" "-")
int1