Erin is big. Erin is cold. Erin is furry. Erin is nice. Erin is red. Erin is rough. Erin is round. Cold, nice people are big. If someone is nice and cold then they are red. Round people are cold. Furry people are big. If someone is furry then they are rough. If Erin is rough then Erin is round. If Erin is red then Erin is big. Furry, red people are big.
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 red.
("Erin" "is" "red" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is round.
("Erin" "is" "round" "+")
Cold, nice people are big.
((("someone" "is" "cold" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "big" "+"))
If someone is nice and cold then they are red.
((("someone" "is" "nice" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "red" "+"))
Round people are cold.
((("someone" "is" "round" "+")) -> ("someone" "is" "cold" "+"))
Furry people are big.
((("someone" "is" "furry" "+")) -> ("someone" "is" "big" "+"))
If someone is furry then they are rough.
((("someone" "is" "furry" "+")) -> ("someone" "is" "rough" "+"))
If Erin is rough then Erin is round.
((("Erin" "is" "rough" "+")) -> ("Erin" "is" "round" "+"))
If Erin is red then Erin is big.
((("Erin" "is" "red" "+")) -> ("Erin" "is" "big" "+"))
Furry, red people are big.
((("someone" "is" "furry" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "big" "+"))
Erin is furry.
True
1
proof
[(triple3)]
("Erin" "is" "furry" "+")
triple3
Erin is not rough.
False
1
inv-proof
[(triple6 OR ((triple3) -> rule5))]
("Erin" "is" "rough" "-")
triple6
((triple3) -> (rule5 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
@0: Erin is big.[(triple1 OR ((triple3) -> rule4) OR ((triple5) -> rule7) OR ((triple2 triple4) -> rule1) OR ((triple3 triple5) -> rule8) OR ((((triple4 triple2) -> rule2)) -> rule7) OR ((triple3 ((triple4 triple2) -> rule2)) -> rule8) OR ((((triple7) -> rule3) triple4) -> rule1) OR ((((triple4 ((triple7) -> rule3)) -> rule2)) -> rule7) OR ((triple3 ((triple4 ((triple7) -> rule3)) -> rule2)) -> rule8) OR ((((((triple6) -> rule6)) -> rule3) triple4) -> rule1) OR ((((triple4 ((((triple6) -> rule6)) -> rule3)) -> rule2)) -> rule7) OR ((triple3 ((triple4 ((((triple6) -> rule6)) -> rule3)) -> rule2)) -> rule8) OR ((((((((triple3) -> rule5)) -> rule6)) -> rule3) triple4) -> rule1) OR ((((triple4 ((((((triple3) -> rule5)) -> rule6)) -> rule3)) -> rule2)) -> rule7) OR ((triple3 ((triple4 ((((((triple3) -> rule5)) -> rule6)) -> rule3)) -> rule2)) -> rule8))] Erin is cold.[(triple2 OR ((triple7) -> rule3) OR ((((triple6) -> rule6)) -> rule3) OR ((((((triple3) -> rule5)) -> rule6)) -> rule3))] Erin is furry.[(triple3)] Erin is nice.[(triple4)] Erin is red.[(triple5 OR ((triple4 triple2) -> rule2) OR ((triple4 ((triple7) -> rule3)) -> rule2) OR ((triple4 ((((triple6) -> rule6)) -> rule3)) -> rule2) OR ((triple4 ((((((triple3) -> rule5)) -> rule6)) -> rule3)) -> rule2))] Erin is rough.[(triple6 OR ((triple3) -> rule5))] Erin is round.[(triple7 OR ((triple6) -> rule6) OR ((((triple3) -> rule5)) -> rule6))]
Erin is big.
("Erin" "is" "big" "+")
triple1
((triple3) -> (rule4 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((triple5) -> (rule7 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((triple2 triple4) -> (rule1 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((triple3 triple5) -> (rule8 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
((((triple4 triple2) -> (rule2 % int2))) -> (rule7 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
((triple3 ((triple4 triple2) -> (rule2 % int2))) -> (rule8 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
((((triple7) -> (rule3 % int2)) triple4) -> (rule1 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
((((triple4 ((triple7) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
((triple3 ((triple4 ((triple7) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
((((((triple6) -> (rule6 % int3))) -> (rule3 % int2)) triple4) -> (rule1 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
((((triple4 ((((triple6) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is round.
("Erin" "is" "round" "+")
int4
((triple3 ((triple4 ((((triple6) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is round.
("Erin" "is" "round" "+")
int4
((((((((triple3) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule3 % int2)) triple4) -> (rule1 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is rough.
("Erin" "is" "rough" "+")
int4
((((triple4 ((((((triple3) -> (rule5 % int5))) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is round.
("Erin" "is" "round" "+")
int4
Erin is rough.
("Erin" "is" "rough" "+")
int5
((triple3 ((triple4 ((((((triple3) -> (rule5 % int5))) -> (rule6 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
int3
Erin is round.
("Erin" "is" "round" "+")
int4
Erin is rough.
("Erin" "is" "rough" "+")
int5
Erin is cold.
("Erin" "is" "cold" "+")
triple2
((triple7) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
((((triple6) -> (rule6 % int2))) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
((((((triple3) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
int3
Erin is furry.
("Erin" "is" "furry" "+")
triple3
Erin is nice.
("Erin" "is" "nice" "+")
triple4
Erin is red.
("Erin" "is" "red" "+")
triple5
((triple4 triple2) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
((triple4 ((triple7) -> (rule3 % int2))) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
((triple4 ((((triple6) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
((triple4 ((((((triple3) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is rough.
("Erin" "is" "rough" "+")
int4
Erin is rough.
("Erin" "is" "rough" "+")
triple6
((triple3) -> (rule5 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
triple7
((triple6) -> (rule6 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
((((triple3) -> (rule5 % int2))) -> (rule6 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2