Erin is big. Erin is blue. Erin is cold. Erin is quiet. Erin is rough. Erin is round. Erin is young. If something is round then it is rough. If something is quiet and young then it is big. Round things are young. If Erin is blue and Erin is big then Erin is rough. If Erin is quiet and Erin is rough then Erin is round. All young, blue things are rough.
Erin is big.
("Erin" "is" "big" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is young.
("Erin" "is" "young" "+")
If something is round then it is rough.
((("something" "is" "round" "+")) -> ("something" "is" "rough" "+"))
If something is quiet and young then it is big.
((("something" "is" "quiet" "+") ("something" "is" "young" "+")) -> ("something" "is" "big" "+"))
Round things are young.
((("something" "is" "round" "+")) -> ("something" "is" "young" "+"))
If Erin is blue and Erin is big then Erin is rough.
((("Erin" "is" "blue" "+") ("Erin" "is" "big" "+")) -> ("Erin" "is" "rough" "+"))
If Erin is quiet and Erin is rough then Erin is round.
((("Erin" "is" "quiet" "+") ("Erin" "is" "rough" "+")) -> ("Erin" "is" "round" "+"))
All young, blue things are rough.
((("something" "is" "young" "+") ("something" "is" "blue" "+")) -> ("something" "is" "rough" "+"))
Erin is big.
True
1
proof
[(triple1 OR ((triple4 triple7) -> rule2) OR ((triple4 ((triple6) -> rule3)) -> rule2) OR ((triple4 ((((triple4 triple5) -> rule5)) -> rule3)) -> rule2))]
("Erin" "is" "big" "+")
triple1
((triple4 triple7) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((triple4 ((triple6) -> (rule3 % int2))) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
((triple4 ((((triple4 triple5) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is not rough.
False
1
inv-proof
[(triple5 OR ((triple6) -> rule1) OR ((triple2 triple1) -> rule4) OR ((triple7 triple2) -> rule6) OR ((triple2 ((triple4 triple7) -> rule2)) -> rule4) OR ((((triple6) -> rule3) triple2) -> rule6) OR ((triple2 ((triple4 ((triple6) -> rule3)) -> rule2)) -> rule4))]
("Erin" "is" "rough" "-")
triple5
((triple6) -> (rule1 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
((triple2 triple1) -> (rule4 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
((triple7 triple2) -> (rule6 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
((triple2 ((triple4 triple7) -> (rule2 % int2))) -> (rule4 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
((((triple6) -> (rule3 % int2)) triple2) -> (rule6 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
((triple2 ((triple4 ((triple6) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
@0: Erin is big.[(triple1 OR ((triple4 triple7) -> rule2) OR ((triple4 ((triple6) -> rule3)) -> rule2) OR ((triple4 ((((triple4 triple5) -> rule5)) -> rule3)) -> rule2))] Erin is blue.[(triple2)] Erin is cold.[(triple3)] Erin is quiet.[(triple4)] Erin is rough.[(triple5 OR ((triple6) -> rule1) OR ((triple2 triple1) -> rule4) OR ((triple7 triple2) -> rule6) OR ((triple2 ((triple4 triple7) -> rule2)) -> rule4) OR ((((triple6) -> rule3) triple2) -> rule6) OR ((triple2 ((triple4 ((triple6) -> rule3)) -> rule2)) -> rule4))] Erin is round.[(triple6 OR ((triple4 triple5) -> rule5) OR ((triple4 ((triple2 triple1) -> rule4)) -> rule5) OR ((triple4 ((triple7 triple2) -> rule6)) -> rule5) OR ((triple4 ((triple2 ((triple4 triple7) -> rule2)) -> rule4)) -> rule5))] Erin is young.[(triple7 OR ((triple6) -> rule3) OR ((((triple4 triple5) -> rule5)) -> rule3) OR ((((triple4 ((triple2 triple1) -> rule4)) -> rule5)) -> rule3))]
Erin is big.
("Erin" "is" "big" "+")
triple1
((triple4 triple7) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((triple4 ((triple6) -> (rule3 % int2))) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
((triple4 ((((triple4 triple5) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is blue.
("Erin" "is" "blue" "+")
triple2
Erin is cold.
("Erin" "is" "cold" "+")
triple3
Erin is quiet.
("Erin" "is" "quiet" "+")
triple4
Erin is rough.
("Erin" "is" "rough" "+")
triple5
((triple6) -> (rule1 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
((triple2 triple1) -> (rule4 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
((triple7 triple2) -> (rule6 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
((triple2 ((triple4 triple7) -> (rule2 % int2))) -> (rule4 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
((((triple6) -> (rule3 % int2)) triple2) -> (rule6 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
((triple2 ((triple4 ((triple6) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is round.
("Erin" "is" "round" "+")
triple6
((triple4 triple5) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
((triple4 ((triple2 triple1) -> (rule4 % int2))) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
((triple4 ((triple7 triple2) -> (rule6 % int2))) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
((triple4 ((triple2 ((triple4 triple7) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is young.
("Erin" "is" "young" "+")
triple7
((triple6) -> (rule3 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
((((triple4 triple5) -> (rule5 % int2))) -> (rule3 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
((((triple4 ((triple2 triple1) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3