Erin is not big. Erin is blue. Erin is cold. Erin is furry. Erin is nice. Erin is red. Erin is round. If something is nice and not big then it is round. If something is big and cold then it is nice.
Erin is not big.
("Erin" "is" "big" "-")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is round.
("Erin" "is" "round" "+")
If something is nice and not big then it is round.
((("something" "is" "nice" "+") ("something" "is" "big" "~")) -> ("something" "is" "round" "+"))
If something is big and cold then it is nice.
((("something" "is" "big" "+") ("something" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
Erin is cold.
True
1
proof
[(triple3)]
("Erin" "is" "cold" "+")
triple3
Erin is not round.
False
1
inv-proof
[(triple7 OR ((triple5 triple1) -> rule1))]
("Erin" "is" "round" "-")
triple7
((triple5 triple1) -> (rule1 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
@0: Erin is blue.[(triple2)] Erin is cold.[(triple3)] Erin is furry.[(triple4)] Erin is nice.[(triple5)] Erin is not big.[(triple1)] Erin is red.[(triple6)] Erin is round.[(triple7 OR ((triple5 triple1) -> rule1))]
Erin is blue.
("Erin" "is" "blue" "+")
triple2
Erin is cold.
("Erin" "is" "cold" "+")
triple3
Erin is furry.
("Erin" "is" "furry" "+")
triple4
Erin is nice.
("Erin" "is" "nice" "+")
triple5
Erin is not big.
("Erin" "is" "big" "-")
triple1
Erin is red.
("Erin" "is" "red" "+")
triple6
Erin is round.
("Erin" "is" "round" "+")
triple7
((triple5 triple1) -> (rule1 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1