Erin is big. Erin is not cold. Erin is furry. Erin is kind. Erin is red. Erin is round. Gary is big. Gary is not cold. Gary is furry. Gary is quiet. Gary is red. Gary is not round. Furry, kind people are not quiet. All furry, kind people are not quiet. All cold people are big. Cold people are not big. If someone is round and not cold then they are kind. Cold, big people are round. If Erin is furry and Erin is not red then Erin is round. Quiet people are furry.
Erin is big.
("Erin" "is" "big" "+")
Erin is not cold.
("Erin" "is" "cold" "-")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is round.
("Erin" "is" "round" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is not cold.
("Gary" "is" "cold" "-")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is not round.
("Gary" "is" "round" "-")
Furry, kind people are not quiet.
((("someone" "is" "furry" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "quiet" "-"))
All furry, kind people are not quiet.
((("someone" "is" "furry" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "quiet" "-"))
All cold people are big.
((("someone" "is" "cold" "+")) -> ("someone" "is" "big" "+"))
Cold people are not big.
((("someone" "is" "cold" "+")) -> ("someone" "is" "big" "-"))
If someone is round and not cold then they are kind.
((("someone" "is" "round" "+") ("someone" "is" "cold" "~")) -> ("someone" "is" "kind" "+"))
Cold, big people are round.
((("someone" "is" "cold" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "round" "+"))
If Erin is furry and Erin is not red then Erin is round.
((("Erin" "is" "furry" "+") ("Erin" "is" "red" "~")) -> ("Erin" "is" "round" "+"))
Quiet people are furry.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "furry" "+"))
Gary is quiet.
True
1
proof
[(triple10)]
("Gary" "is" "quiet" "+")
triple10
Gary is not quiet.
False
1
inv-proof
[(triple10)]
("Gary" "is" "quiet" "-")
triple10
@0: Erin is big.[(triple1)] Erin is furry.[(triple3)] Erin is kind.[(triple4 OR ((triple6 triple2) -> rule5))] Erin is not cold.[(triple2)] Erin is red.[(triple5)] Erin is round.[(triple6)] Gary is big.[(triple7)] Gary is furry.[(triple9 OR ((triple10) -> rule8))] Gary is not cold.[(triple8)] Gary is not round.[(triple12)] Gary is quiet.[(triple10)] Gary is red.[(triple11)] @1: Erin is not quiet.[(((triple3 triple4) -> rule1) OR ((triple3 triple4) -> rule2) OR ((triple3 ((triple6 triple2) -> rule5)) -> rule1) OR ((triple3 ((triple6 triple2) -> rule5)) -> rule2))]
Erin is big.
("Erin" "is" "big" "+")
triple1
Erin is furry.
("Erin" "is" "furry" "+")
triple3
Erin is kind.
("Erin" "is" "kind" "+")
triple4
((triple6 triple2) -> (rule5 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is not cold.
("Erin" "is" "cold" "-")
triple2
Erin is red.
("Erin" "is" "red" "+")
triple5
Erin is round.
("Erin" "is" "round" "+")
triple6
Gary is big.
("Gary" "is" "big" "+")
triple7
Gary is furry.
("Gary" "is" "furry" "+")
triple9
((triple10) -> (rule8 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is not cold.
("Gary" "is" "cold" "-")
triple8
Gary is not round.
("Gary" "is" "round" "-")
triple12
Gary is quiet.
("Gary" "is" "quiet" "+")
triple10
Gary is red.
("Gary" "is" "red" "+")
triple11
Erin is not quiet.
("Erin" "is" "quiet" "-")
((triple3 triple4) -> (rule1 % int1))
Erin is not quiet.
("Erin" "is" "quiet" "-")
int1
((triple3 triple4) -> (rule2 % int1))
Erin is not quiet.
("Erin" "is" "quiet" "-")
int1
((triple3 ((triple6 triple2) -> (rule5 % int2))) -> (rule1 % int1))
Erin is not quiet.
("Erin" "is" "quiet" "-")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
((triple3 ((triple6 triple2) -> (rule5 % int2))) -> (rule2 % int1))
Erin is not quiet.
("Erin" "is" "quiet" "-")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2