Anne is big. Anne is cold. Anne is quiet. Anne is red. Anne is rough. Anne is smart. Anne is white. If someone is smart then they are quiet. If someone is cold and white then they are red.
Anne is big.
("Anne" "is" "big" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is white.
("Anne" "is" "white" "+")
If someone is smart then they are quiet.
((("someone" "is" "smart" "+")) -> ("someone" "is" "quiet" "+"))
If someone is cold and white then they are red.
((("someone" "is" "cold" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "red" "+"))
Anne is big.
True
1
proof
[(triple1)]
("Anne" "is" "big" "+")
triple1
Anne is not smart.
False
1
inv-proof
[(triple6)]
("Anne" "is" "smart" "-")
triple6
@0: Anne is big.[(triple1)] Anne is cold.[(triple2)] Anne is quiet.[(triple3 OR ((triple6) -> rule1))] Anne is red.[(triple4 OR ((triple2 triple7) -> rule2))] Anne is rough.[(triple5)] Anne is smart.[(triple6)] Anne is white.[(triple7)]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is cold.
("Anne" "is" "cold" "+")
triple2
Anne is quiet.
("Anne" "is" "quiet" "+")
triple3
((triple6) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
triple4
((triple2 triple7) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
triple5
Anne is smart.
("Anne" "is" "smart" "+")
triple6
Anne is white.
("Anne" "is" "white" "+")
triple7