Erin is blue. Erin is furry. Erin is not green. Erin is rough. Erin is round. Erin is white. Erin is not young. If Erin is green and Erin is furry then Erin is not young. If someone is white and round then they are furry. All round, white people are furry. If someone is rough then they are furry. Blue, young people are rough. All furry people are white.
Erin is blue.
("Erin" "is" "blue" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is not green.
("Erin" "is" "green" "-")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is white.
("Erin" "is" "white" "+")
Erin is not young.
("Erin" "is" "young" "-")
If Erin is green and Erin is furry then Erin is not young.
((("Erin" "is" "green" "+") ("Erin" "is" "furry" "+")) -> ("Erin" "is" "young" "-"))
If someone is white and round then they are furry.
((("someone" "is" "white" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "furry" "+"))
All round, white people are furry.
((("someone" "is" "round" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "furry" "+"))
If someone is rough then they are furry.
((("someone" "is" "rough" "+")) -> ("someone" "is" "furry" "+"))
Blue, young people are rough.
((("someone" "is" "blue" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "rough" "+"))
All furry people are white.
((("someone" "is" "furry" "+")) -> ("someone" "is" "white" "+"))
Erin is furry.
True
1
proof
[(triple2 OR ((triple4) -> rule4) OR ((triple5 triple6) -> rule3) OR ((triple6 triple5) -> rule2))]
("Erin" "is" "furry" "+")
triple2
((triple4) -> (rule4 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
((triple5 triple6) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
((triple6 triple5) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is not blue.
False
1
inv-proof
[(triple1)]
("Erin" "is" "blue" "-")
triple1
@0: Erin is blue.[(triple1)] Erin is furry.[(triple2 OR ((triple4) -> rule4) OR ((triple5 triple6) -> rule3) OR ((triple6 triple5) -> rule2))] Erin is not green.[(triple3)] Erin is not young.[(triple7)] Erin is rough.[(triple4)] Erin is round.[(triple5)] Erin is white.[(triple6 OR ((triple2) -> rule6) OR ((((triple4) -> rule4)) -> rule6))]
Erin is blue.
("Erin" "is" "blue" "+")
triple1
Erin is furry.
("Erin" "is" "furry" "+")
triple2
((triple4) -> (rule4 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
((triple5 triple6) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
((triple6 triple5) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is not green.
("Erin" "is" "green" "-")
triple3
Erin is not young.
("Erin" "is" "young" "-")
triple7
Erin is rough.
("Erin" "is" "rough" "+")
triple4
Erin is round.
("Erin" "is" "round" "+")
triple5
Erin is white.
("Erin" "is" "white" "+")
triple6
((triple2) -> (rule6 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
((((triple4) -> (rule4 % int2))) -> (rule6 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2