Anne is big. Anne is kind. Anne is nice. Anne is red. Anne is round. Anne is white. Anne is young. If something is round and white then it is nice. If Anne is young then Anne is red.
Anne is big.
("Anne" "is" "big" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is white.
("Anne" "is" "white" "+")
Anne is young.
("Anne" "is" "young" "+")
If something is round and white then it is nice.
((("something" "is" "round" "+") ("something" "is" "white" "+")) -> ("something" "is" "nice" "+"))
If Anne is young then Anne is red.
((("Anne" "is" "young" "+")) -> ("Anne" "is" "red" "+"))
Anne is big.
True
1
proof
[(triple1)]
("Anne" "is" "big" "+")
triple1
Anne is not kind.
False
1
inv-proof
[(triple2)]
("Anne" "is" "kind" "-")
triple2
@0: Anne is big.[(triple1)] Anne is kind.[(triple2)] Anne is nice.[(triple3 OR ((triple5 triple6) -> rule1))] Anne is red.[(triple4 OR ((triple7) -> rule2))] Anne is round.[(triple5)] Anne is white.[(triple6)] Anne is young.[(triple7)]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is kind.
("Anne" "is" "kind" "+")
triple2
Anne is nice.
("Anne" "is" "nice" "+")
triple3
((triple5 triple6) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
triple4
((triple7) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
triple5
Anne is white.
("Anne" "is" "white" "+")
triple6
Anne is young.
("Anne" "is" "young" "+")
triple7