Anne is big. Anne is blue. Anne is kind. Anne is nice. Anne is quiet. Anne is rough. Anne is not smart. Erin is big. Erin is blue. Erin is not kind. Erin is quiet. Erin is not smart. Smart, quiet people are kind. If someone is quiet and not big then they are rough. If someone is smart then they are blue. If someone is quiet and smart then they are not blue. If someone is nice and smart then they are not blue. Rough people are nice.
Anne is big.
("Anne" "is" "big" "+")
Anne is blue.
("Anne" "is" "blue" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is not smart.
("Anne" "is" "smart" "-")
Erin is big.
("Erin" "is" "big" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is not kind.
("Erin" "is" "kind" "-")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is not smart.
("Erin" "is" "smart" "-")
Smart, quiet people are kind.
((("someone" "is" "smart" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "kind" "+"))
If someone is quiet and not big then they are rough.
((("someone" "is" "quiet" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "rough" "+"))
If someone is smart then they are blue.
((("someone" "is" "smart" "+")) -> ("someone" "is" "blue" "+"))
If someone is quiet and smart then they are not blue.
((("someone" "is" "quiet" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "blue" "-"))
If someone is nice and smart then they are not blue.
((("someone" "is" "nice" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "blue" "-"))
Rough people are nice.
((("someone" "is" "rough" "+")) -> ("someone" "is" "nice" "+"))
Anne is quiet.
True
1
proof
[(triple5)]
("Anne" "is" "quiet" "+")
triple5
Erin is not big.
False
1
inv-proof
[(triple8)]
("Erin" "is" "big" "-")
triple8
@0: Anne is big.[(triple1)] Anne is blue.[(triple2)] Anne is kind.[(triple3)] Anne is nice.[(triple4 OR ((triple6) -> rule6))] Anne is not smart.[(triple7)] Anne is quiet.[(triple5)] Anne is rough.[(triple6)] Erin is big.[(triple8)] Erin is blue.[(triple9)] Erin is not kind.[(triple10)] Erin is not smart.[(triple12)] Erin is quiet.[(triple11)]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is blue.
("Anne" "is" "blue" "+")
triple2
Anne is kind.
("Anne" "is" "kind" "+")
triple3
Anne is nice.
("Anne" "is" "nice" "+")
triple4
((triple6) -> (rule6 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is not smart.
("Anne" "is" "smart" "-")
triple7
Anne is quiet.
("Anne" "is" "quiet" "+")
triple5
Anne is rough.
("Anne" "is" "rough" "+")
triple6
Erin is big.
("Erin" "is" "big" "+")
triple8
Erin is blue.
("Erin" "is" "blue" "+")
triple9
Erin is not kind.
("Erin" "is" "kind" "-")
triple10
Erin is not smart.
("Erin" "is" "smart" "-")
triple12
Erin is quiet.
("Erin" "is" "quiet" "+")
triple11