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