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