Erin is big. Erin is cold. Erin is furry. Erin is nice. Erin is not round. Erin is not smart. Erin is young. Gary is big. Gary is cold. Gary is furry. Gary is nice. Gary is round. Gary is smart. Gary is not young. All young people are big. Young people are big. All cold people are furry. If someone is round then they are furry. If Gary is big and Gary is not cold then Gary is not nice. Smart people are nice.
Erin is big.
("Erin" "is" "big" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is not round.
("Erin" "is" "round" "-")
Erin is not smart.
("Erin" "is" "smart" "-")
Erin is young.
("Erin" "is" "young" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is cold.
("Gary" "is" "cold" "+")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is not young.
("Gary" "is" "young" "-")
All young people are big.
((("someone" "is" "young" "+")) -> ("someone" "is" "big" "+"))
Young people are big.
((("someone" "is" "young" "+")) -> ("someone" "is" "big" "+"))
All cold people are furry.
((("someone" "is" "cold" "+")) -> ("someone" "is" "furry" "+"))
If someone is round then they are furry.
((("someone" "is" "round" "+")) -> ("someone" "is" "furry" "+"))
If Gary is big and Gary is not cold then Gary is not nice.
((("Gary" "is" "big" "+") ("Gary" "is" "cold" "~")) -> ("Gary" "is" "nice" "-"))
Smart people are nice.
((("someone" "is" "smart" "+")) -> ("someone" "is" "nice" "+"))
Erin is furry.
True
1
proof
[(triple3 OR ((triple2) -> rule3))]
("Erin" "is" "furry" "+")
triple3
((triple2) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Gary is not nice.
False
1
inv-proof
[(triple11 OR ((triple13) -> rule6))]
("Gary" "is" "nice" "-")
triple11
((triple13) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
@0: Erin is big.[(triple1 OR ((triple7) -> rule1) OR ((triple7) -> rule2))] Erin is cold.[(triple2)] Erin is furry.[(triple3 OR ((triple2) -> rule3))] Erin is nice.[(triple4)] Erin is not round.[(triple5)] Erin is not smart.[(triple6)] Erin is young.[(triple7)] Gary is big.[(triple8)] Gary is cold.[(triple9)] Gary is furry.[(triple10 OR ((triple12) -> rule4) OR ((triple9) -> rule3))] Gary is nice.[(triple11 OR ((triple13) -> rule6))] Gary is not young.[(triple14)] Gary is round.[(triple12)] Gary is smart.[(triple13)]
Erin is big.
("Erin" "is" "big" "+")
triple1
((triple7) -> (rule1 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((triple7) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
triple2
Erin is furry.
("Erin" "is" "furry" "+")
triple3
((triple2) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
triple4
Erin is not round.
("Erin" "is" "round" "-")
triple5
Erin is not smart.
("Erin" "is" "smart" "-")
triple6
Erin is young.
("Erin" "is" "young" "+")
triple7
Gary is big.
("Gary" "is" "big" "+")
triple8
Gary is cold.
("Gary" "is" "cold" "+")
triple9
Gary is furry.
("Gary" "is" "furry" "+")
triple10
((triple12) -> (rule4 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
((triple9) -> (rule3 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
triple11
((triple13) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is not young.
("Gary" "is" "young" "-")
triple14
Gary is round.
("Gary" "is" "round" "+")
triple12
Gary is smart.
("Gary" "is" "smart" "+")
triple13