Erin is kind. Erin is nice. Erin is smart. Cold things are smart. If Erin is smart then Erin is blue. If something is blue then it is quiet. If something is cold and kind then it is quiet. All cold things are not blue. If something is quiet and not kind then it is big. All kind things are big. All smart things are nice.
Erin is kind.
("Erin" "is" "kind" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Cold things are smart.
((("something" "is" "cold" "+")) -> ("something" "is" "smart" "+"))
If Erin is smart then Erin is blue.
((("Erin" "is" "smart" "+")) -> ("Erin" "is" "blue" "+"))
If something is blue then it is quiet.
((("something" "is" "blue" "+")) -> ("something" "is" "quiet" "+"))
If something is cold and kind then it is quiet.
((("something" "is" "cold" "+") ("something" "is" "kind" "+")) -> ("something" "is" "quiet" "+"))
All cold things are not blue.
((("something" "is" "cold" "+")) -> ("something" "is" "blue" "-"))
If something is quiet and not kind then it is big.
((("something" "is" "quiet" "+") ("something" "is" "kind" "~")) -> ("something" "is" "big" "+"))
All kind things are big.
((("something" "is" "kind" "+")) -> ("something" "is" "big" "+"))
All smart things are nice.
((("something" "is" "smart" "+")) -> ("something" "is" "nice" "+"))
Erin is nice.
True
1
proof
[(triple2 OR ((triple3) -> rule8))]
("Erin" "is" "nice" "+")
triple2
((triple3) -> (rule8 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is not smart.
False
1
inv-proof
[(triple3)]
("Erin" "is" "smart" "-")
triple3
@0: Erin is kind.[(triple1)] Erin is nice.[(triple2 OR ((triple3) -> rule8))] Erin is smart.[(triple3)] @1: Erin is big.[(((triple1) -> rule7))] Erin is blue.[(((triple3) -> rule2))] @2: Erin is quiet.[(((((triple3) -> rule2)) -> rule3))]
Erin is kind.
("Erin" "is" "kind" "+")
triple1
Erin is nice.
("Erin" "is" "nice" "+")
triple2
((triple3) -> (rule8 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
triple3
Erin is big.
("Erin" "is" "big" "+")
((triple1) -> (rule7 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
((triple3) -> (rule2 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2