Erin is big. Erin is cold. Erin is green. Erin is kind. Erin is quiet. Erin is round. Erin is smart. If Erin is green and Erin is cold then Erin is kind. If something is smart and big then it is quiet. All smart things are kind.
Erin is big.
("Erin" "is" "big" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is smart.
("Erin" "is" "smart" "+")
If Erin is green and Erin is cold then Erin is kind.
((("Erin" "is" "green" "+") ("Erin" "is" "cold" "+")) -> ("Erin" "is" "kind" "+"))
If something is smart and big then it is quiet.
((("something" "is" "smart" "+") ("something" "is" "big" "+")) -> ("something" "is" "quiet" "+"))
All smart things are kind.
((("something" "is" "smart" "+")) -> ("something" "is" "kind" "+"))
Erin is big.
True
1
proof
[(triple1)]
("Erin" "is" "big" "+")
triple1
Erin is not cold.
False
1
inv-proof
[(triple2)]
("Erin" "is" "cold" "-")
triple2
@0: Erin is big.[(triple1)] Erin is cold.[(triple2)] Erin is green.[(triple3)] Erin is kind.[(triple4 OR ((triple7) -> rule3) OR ((triple3 triple2) -> rule1))] Erin is quiet.[(triple5 OR ((triple7 triple1) -> rule2))] Erin is round.[(triple6)] Erin is smart.[(triple7)]
Erin is big.
("Erin" "is" "big" "+")
triple1
Erin is cold.
("Erin" "is" "cold" "+")
triple2
Erin is green.
("Erin" "is" "green" "+")
triple3
Erin is kind.
("Erin" "is" "kind" "+")
triple4
((triple7) -> (rule3 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
((triple3 triple2) -> (rule1 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
triple5
((triple7 triple1) -> (rule2 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
triple6
Erin is smart.
("Erin" "is" "smart" "+")
triple7