Erin is big. Erin is furry. Erin is red. Erin is rough. Erin is round. Erin is white. Erin is young. If something is red then it is round. Round, red things are big.
Erin is big.
("Erin" "is" "big" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is white.
("Erin" "is" "white" "+")
Erin is young.
("Erin" "is" "young" "+")
If something is red then it is round.
((("something" "is" "red" "+")) -> ("something" "is" "round" "+"))
Round, red things are big.
((("something" "is" "round" "+") ("something" "is" "red" "+")) -> ("something" "is" "big" "+"))
Erin is round.
True
1
proof
[(triple5 OR ((triple3) -> rule1))]
("Erin" "is" "round" "+")
triple5
((triple3) -> (rule1 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is not furry.
False
1
inv-proof
[(triple2)]
("Erin" "is" "furry" "-")
triple2
@0: Erin is big.[(triple1 OR ((triple5 triple3) -> rule2) OR ((((triple3) -> rule1) triple3) -> rule2))] Erin is furry.[(triple2)] Erin is red.[(triple3)] Erin is rough.[(triple4)] Erin is round.[(triple5 OR ((triple3) -> rule1))] Erin is white.[(triple6)] Erin is young.[(triple7)]
Erin is big.
("Erin" "is" "big" "+")
triple1
((triple5 triple3) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((((triple3) -> (rule1 % int2)) triple3) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
triple2
Erin is red.
("Erin" "is" "red" "+")
triple3
Erin is rough.
("Erin" "is" "rough" "+")
triple4
Erin is round.
("Erin" "is" "round" "+")
triple5
((triple3) -> (rule1 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
triple6
Erin is young.
("Erin" "is" "young" "+")
triple7