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