Erin is big. Erin is blue. Erin is furry. Erin is green. Erin is nice. Erin is quiet. Erin is round. If Erin is quiet and Erin is green then Erin is round. If Erin is not quiet then Erin is not nice. If something is big then it is furry. If something is furry and not nice then it is big. If something is blue and not green then it is big. Furry, green things are round. If something is round and nice then it is blue. If Erin is round then Erin is blue.
Erin is big.
("Erin" "is" "big" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is round.
("Erin" "is" "round" "+")
If Erin is quiet and Erin is green then Erin is round.
((("Erin" "is" "quiet" "+") ("Erin" "is" "green" "+")) -> ("Erin" "is" "round" "+"))
If Erin is not quiet then Erin is not nice.
((("Erin" "is" "quiet" "~")) -> ("Erin" "is" "nice" "-"))
If something is big then it is furry.
((("something" "is" "big" "+")) -> ("something" "is" "furry" "+"))
If something is furry and not nice then it is big.
((("something" "is" "furry" "+") ("something" "is" "nice" "~")) -> ("something" "is" "big" "+"))
If something is blue and not green then it is big.
((("something" "is" "blue" "+") ("something" "is" "green" "~")) -> ("something" "is" "big" "+"))
Furry, green things are round.
((("something" "is" "furry" "+") ("something" "is" "green" "+")) -> ("something" "is" "round" "+"))
If something is round and nice then it is blue.
((("something" "is" "round" "+") ("something" "is" "nice" "+")) -> ("something" "is" "blue" "+"))
If Erin is round then Erin is blue.
((("Erin" "is" "round" "+")) -> ("Erin" "is" "blue" "+"))
Erin is big.
True
1
proof
[(triple1)]
("Erin" "is" "big" "+")
triple1
Erin is not round.
False
1
inv-proof
[(triple7 OR ((triple3 triple4) -> rule6) OR ((triple6 triple4) -> rule1) OR ((((triple1) -> rule3) triple4) -> rule6))]
("Erin" "is" "round" "-")
triple7
((triple3 triple4) -> (rule6 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
((triple6 triple4) -> (rule1 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
((((triple1) -> (rule3 % int2)) triple4) -> (rule6 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
@0: Erin is big.[(triple1)] Erin is blue.[(triple2 OR ((triple7) -> rule8) OR ((triple7 triple5) -> rule7) OR ((((triple3 triple4) -> rule6)) -> rule8) OR ((((triple6 triple4) -> rule1)) -> rule8) OR ((((triple3 triple4) -> rule6) triple5) -> rule7) OR ((((triple6 triple4) -> rule1) triple5) -> rule7) OR ((((((triple1) -> rule3) triple4) -> rule6)) -> rule8) OR ((((((triple1) -> rule3) triple4) -> rule6) triple5) -> rule7))] Erin is furry.[(triple3 OR ((triple1) -> rule3))] Erin is green.[(triple4)] Erin is nice.[(triple5)] Erin is quiet.[(triple6)] Erin is round.[(triple7 OR ((triple3 triple4) -> rule6) OR ((triple6 triple4) -> rule1) OR ((((triple1) -> rule3) triple4) -> rule6))]
Erin is big.
("Erin" "is" "big" "+")
triple1
Erin is blue.
("Erin" "is" "blue" "+")
triple2
((triple7) -> (rule8 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
((triple7 triple5) -> (rule7 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
((((triple3 triple4) -> (rule6 % int2))) -> (rule8 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
((((triple6 triple4) -> (rule1 % int2))) -> (rule8 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
((((triple3 triple4) -> (rule6 % int2)) triple5) -> (rule7 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
((((triple6 triple4) -> (rule1 % int2)) triple5) -> (rule7 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
((((((triple1) -> (rule3 % int3)) triple4) -> (rule6 % int2))) -> (rule8 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
((((((triple1) -> (rule3 % int3)) triple4) -> (rule6 % int2)) triple5) -> (rule7 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
int3
Erin is furry.
("Erin" "is" "furry" "+")
triple3
((triple1) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
triple4
Erin is nice.
("Erin" "is" "nice" "+")
triple5
Erin is quiet.
("Erin" "is" "quiet" "+")
triple6
Erin is round.
("Erin" "is" "round" "+")
triple7
((triple3 triple4) -> (rule6 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
((triple6 triple4) -> (rule1 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
((((triple1) -> (rule3 % int2)) triple4) -> (rule6 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2