Erin is blue. Erin is furry. Erin is green. Erin is kind. Erin is red. Erin is round. Erin is smart. If Erin is green then Erin is smart. If Erin is smart then Erin is blue. All red things are furry. Round things are blue. Red, kind things are round. All green, smart things are furry. If Erin is red and Erin is smart then Erin is blue. If Erin is kind and Erin is round then Erin is smart.
Erin is blue.
("Erin" "is" "blue" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is smart.
("Erin" "is" "smart" "+")
If Erin is green then Erin is smart.
((("Erin" "is" "green" "+")) -> ("Erin" "is" "smart" "+"))
If Erin is smart then Erin is blue.
((("Erin" "is" "smart" "+")) -> ("Erin" "is" "blue" "+"))
All red things are furry.
((("something" "is" "red" "+")) -> ("something" "is" "furry" "+"))
Round things are blue.
((("something" "is" "round" "+")) -> ("something" "is" "blue" "+"))
Red, kind things are round.
((("something" "is" "red" "+") ("something" "is" "kind" "+")) -> ("something" "is" "round" "+"))
All green, smart things are furry.
((("something" "is" "green" "+") ("something" "is" "smart" "+")) -> ("something" "is" "furry" "+"))
If Erin is red and Erin is smart then Erin is blue.
((("Erin" "is" "red" "+") ("Erin" "is" "smart" "+")) -> ("Erin" "is" "blue" "+"))
If Erin is kind and Erin is round then Erin is smart.
((("Erin" "is" "kind" "+") ("Erin" "is" "round" "+")) -> ("Erin" "is" "smart" "+"))
Erin is smart.
True
1
proof
[(triple7 OR ((triple3) -> rule1) OR ((triple4 triple6) -> rule8) OR ((triple4 ((triple5 triple4) -> rule5)) -> rule8))]
("Erin" "is" "smart" "+")
triple7
((triple3) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((triple4 triple6) -> (rule8 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((triple4 ((triple5 triple4) -> (rule5 % int2))) -> (rule8 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is not red.
False
1
inv-proof
[(triple5)]
("Erin" "is" "red" "-")
triple5
@0: Erin is blue.[(triple1 OR ((triple6) -> rule4) OR ((triple7) -> rule2) OR ((triple5 triple7) -> rule7) OR ((((triple3) -> rule1)) -> rule2) OR ((((triple4 triple6) -> rule8)) -> rule2) OR ((((triple5 triple4) -> rule5)) -> rule4) OR ((triple5 ((triple3) -> rule1)) -> rule7) OR ((triple5 ((triple4 triple6) -> rule8)) -> rule7) OR ((((triple4 ((triple5 triple4) -> rule5)) -> rule8)) -> rule2) OR ((triple5 ((triple4 ((triple5 triple4) -> rule5)) -> rule8)) -> rule7))] Erin is furry.[(triple2 OR ((triple5) -> rule3) OR ((triple3 triple7) -> rule6) OR ((triple3 ((triple3) -> rule1)) -> rule6) OR ((triple3 ((triple4 triple6) -> rule8)) -> rule6) OR ((triple3 ((triple4 ((triple5 triple4) -> rule5)) -> rule8)) -> rule6))] Erin is green.[(triple3)] Erin is kind.[(triple4)] Erin is red.[(triple5)] Erin is round.[(triple6 OR ((triple5 triple4) -> rule5))] Erin is smart.[(triple7 OR ((triple3) -> rule1) OR ((triple4 triple6) -> rule8) OR ((triple4 ((triple5 triple4) -> rule5)) -> rule8))]
Erin is blue.
("Erin" "is" "blue" "+")
triple1
((triple6) -> (rule4 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
((triple7) -> (rule2 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
((triple5 triple7) -> (rule7 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
((((triple4 triple6) -> (rule8 % int2))) -> (rule2 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
((((triple5 triple4) -> (rule5 % int2))) -> (rule4 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
((triple5 ((triple3) -> (rule1 % int2))) -> (rule7 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
((triple5 ((triple4 triple6) -> (rule8 % int2))) -> (rule7 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
((((triple4 ((triple5 triple4) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
((triple5 ((triple4 ((triple5 triple4) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is furry.
("Erin" "is" "furry" "+")
triple2
((triple5) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
((triple3 triple7) -> (rule6 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
((triple3 ((triple3) -> (rule1 % int2))) -> (rule6 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
((triple3 ((triple4 triple6) -> (rule8 % int2))) -> (rule6 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
((triple3 ((triple4 ((triple5 triple4) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is green.
("Erin" "is" "green" "+")
triple3
Erin is kind.
("Erin" "is" "kind" "+")
triple4
Erin is red.
("Erin" "is" "red" "+")
triple5
Erin is round.
("Erin" "is" "round" "+")
triple6
((triple5 triple4) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
triple7
((triple3) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((triple4 triple6) -> (rule8 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
((triple4 ((triple5 triple4) -> (rule5 % int2))) -> (rule8 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2