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