Anne is blue. Anne is furry. Anne is not green. Anne is kind. Anne is red. Anne is rough. Anne is not white. Erin is blue. Erin is furry. Erin is green. Erin is not kind. Erin is red. Erin is rough. Erin is white. Green, blue things are rough. If something is red and not blue then it is rough. If something is blue then it is furry.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is not green.
("Anne" "is" "green" "-")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is not white.
("Anne" "is" "white" "-")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is not kind.
("Erin" "is" "kind" "-")
Erin is red.
("Erin" "is" "red" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is white.
("Erin" "is" "white" "+")
Green, blue things are rough.
((("something" "is" "green" "+") ("something" "is" "blue" "+")) -> ("something" "is" "rough" "+"))
If something is red and not blue then it is rough.
((("something" "is" "red" "+") ("something" "is" "blue" "~")) -> ("something" "is" "rough" "+"))
If something is blue then it is furry.
((("something" "is" "blue" "+")) -> ("something" "is" "furry" "+"))
Erin is green.
True
1
proof
[(triple10)]
("Erin" "is" "green" "+")
triple10
Erin is not white.
False
1
inv-proof
[(triple14)]
("Erin" "is" "white" "-")
triple14
@0: Anne is blue.[(triple1)] Anne is furry.[(triple2 OR ((triple1) -> rule3))] Anne is kind.[(triple4)] Anne is not green.[(triple3)] Anne is not white.[(triple7)] Anne is red.[(triple5)] Anne is rough.[(triple6)] Erin is blue.[(triple8)] Erin is furry.[(triple9 OR ((triple8) -> rule3))] Erin is green.[(triple10)] Erin is not kind.[(triple11)] Erin is red.[(triple12)] Erin is rough.[(triple13 OR ((triple10 triple8) -> rule1))] Erin is white.[(triple14)]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is furry.
("Anne" "is" "furry" "+")
triple2
((triple1) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
triple4
Anne is not green.
("Anne" "is" "green" "-")
triple3
Anne is not white.
("Anne" "is" "white" "-")
triple7
Anne is red.
("Anne" "is" "red" "+")
triple5
Anne is rough.
("Anne" "is" "rough" "+")
triple6
Erin is blue.
("Erin" "is" "blue" "+")
triple8
Erin is furry.
("Erin" "is" "furry" "+")
triple9
((triple8) -> (rule3 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
triple10
Erin is not kind.
("Erin" "is" "kind" "-")
triple11
Erin is red.
("Erin" "is" "red" "+")
triple12
Erin is rough.
("Erin" "is" "rough" "+")
triple13
((triple10 triple8) -> (rule1 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
triple14