Anne is big. Anne is blue. Anne is not green. Anne is kind. Anne is quiet. Anne is not smart. Anne is young. If Anne is kind and Anne is not green then Anne is big. If something is big and not blue then it is quiet. If Anne is not big then Anne is smart.
Anne is big.
("Anne" "is" "big" "+")
Anne is blue.
("Anne" "is" "blue" "+")
Anne is not green.
("Anne" "is" "green" "-")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is not smart.
("Anne" "is" "smart" "-")
Anne is young.
("Anne" "is" "young" "+")
If Anne is kind and Anne is not green then Anne is big.
((("Anne" "is" "kind" "+") ("Anne" "is" "green" "~")) -> ("Anne" "is" "big" "+"))
If something is big and not blue then it is quiet.
((("something" "is" "big" "+") ("something" "is" "blue" "~")) -> ("something" "is" "quiet" "+"))
If Anne is not big then Anne is smart.
((("Anne" "is" "big" "~")) -> ("Anne" "is" "smart" "+"))
Anne is kind.
True
1
proof
[(triple4)]
("Anne" "is" "kind" "+")
triple4
Anne is green.
False
1
inv-proof
[(triple3)]
("Anne" "is" "green" "+")
triple3
@0: Anne is big.[(triple1 OR ((triple4 triple3) -> rule1))] Anne is blue.[(triple2)] Anne is kind.[(triple4)] Anne is not green.[(triple3)] Anne is not smart.[(triple6)] Anne is quiet.[(triple5)] Anne is young.[(triple7)]
Anne is big.
("Anne" "is" "big" "+")
triple1
((triple4 triple3) -> (rule1 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
triple2
Anne is kind.
("Anne" "is" "kind" "+")
triple4
Anne is not green.
("Anne" "is" "green" "-")
triple3
Anne is not smart.
("Anne" "is" "smart" "-")
triple6
Anne is quiet.
("Anne" "is" "quiet" "+")
triple5
Anne is young.
("Anne" "is" "young" "+")
triple7