Erin is big. Erin is furry. Erin is nice. Erin is red. Erin is round. Erin is white. Erin is young. Furry things are young. All round things are young. Furry things are young. Nice things are furry. All young, round things are nice. If something is furry then it is white.
Erin is big.
("Erin" "is" "big" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is white.
("Erin" "is" "white" "+")
Erin is young.
("Erin" "is" "young" "+")
Furry things are young.
((("something" "is" "furry" "+")) -> ("something" "is" "young" "+"))
All round things are young.
((("something" "is" "round" "+")) -> ("something" "is" "young" "+"))
Furry things are young.
((("something" "is" "furry" "+")) -> ("something" "is" "young" "+"))
Nice things are furry.
((("something" "is" "nice" "+")) -> ("something" "is" "furry" "+"))
All young, round things are nice.
((("something" "is" "young" "+") ("something" "is" "round" "+")) -> ("something" "is" "nice" "+"))
If something is furry then it is white.
((("something" "is" "furry" "+")) -> ("something" "is" "white" "+"))
Erin is young.
True
1
proof
[(triple7 OR ((triple2) -> rule1) OR ((triple2) -> rule3) OR ((triple5) -> rule2) OR ((((triple3) -> rule4)) -> rule1) OR ((((triple3) -> rule4)) -> rule3))]
("Erin" "is" "young" "+")
triple7
((triple2) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
((triple2) -> (rule3 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
((triple5) -> (rule2 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
((((triple3) -> (rule4 % int2))) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
((((triple3) -> (rule4 % int2))) -> (rule3 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is not big.
False
1
inv-proof
[(triple1)]
("Erin" "is" "big" "-")
triple1
@0: Erin is big.[(triple1)] Erin is furry.[(triple2 OR ((triple3) -> rule4) OR ((((triple7 triple5) -> rule5)) -> rule4) OR ((((((triple5) -> rule2) triple5) -> rule5)) -> rule4))] Erin is nice.[(triple3 OR ((triple7 triple5) -> rule5) OR ((((triple2) -> rule1) triple5) -> rule5) OR ((((triple2) -> rule3) triple5) -> rule5) OR ((((triple5) -> rule2) triple5) -> rule5))] Erin is red.[(triple4)] Erin is round.[(triple5)] Erin is white.[(triple6 OR ((triple2) -> rule6) OR ((((triple3) -> rule4)) -> rule6) OR ((((((triple7 triple5) -> rule5)) -> rule4)) -> rule6) OR ((((((((triple5) -> rule2) triple5) -> rule5)) -> rule4)) -> rule6))] Erin is young.[(triple7 OR ((triple2) -> rule1) OR ((triple2) -> rule3) OR ((triple5) -> rule2) OR ((((triple3) -> rule4)) -> rule1) OR ((((triple3) -> rule4)) -> rule3))]
Erin is big.
("Erin" "is" "big" "+")
triple1
Erin is furry.
("Erin" "is" "furry" "+")
triple2
((triple3) -> (rule4 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
((((triple7 triple5) -> (rule5 % int2))) -> (rule4 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
((((((triple5) -> (rule2 % int3)) triple5) -> (rule5 % int2))) -> (rule4 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is nice.
("Erin" "is" "nice" "+")
triple3
((triple7 triple5) -> (rule5 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
((((triple2) -> (rule1 % int2)) triple5) -> (rule5 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
((((triple2) -> (rule3 % int2)) triple5) -> (rule5 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
((((triple5) -> (rule2 % int2)) triple5) -> (rule5 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
triple4
Erin is round.
("Erin" "is" "round" "+")
triple5
Erin is white.
("Erin" "is" "white" "+")
triple6
((triple2) -> (rule6 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((((triple3) -> (rule4 % int2))) -> (rule6 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
((((((triple7 triple5) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
((((((((triple5) -> (rule2 % int4)) triple5) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Erin is young.
("Erin" "is" "young" "+")
int4
Erin is young.
("Erin" "is" "young" "+")
triple7
((triple2) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
((triple2) -> (rule3 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
((triple5) -> (rule2 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
((((triple3) -> (rule4 % int2))) -> (rule1 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
((((triple3) -> (rule4 % int2))) -> (rule3 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2