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