Anne is not big. Anne is blue. Anne is not cold. Anne is green. Anne is not kind. Anne is not nice. Anne is young. Erin is big. Erin is blue. Erin is cold. Erin is green. Erin is kind. Erin is not nice. Erin is young. If Erin is not young then Erin is not nice. All kind, nice things are not cold. If something is kind and not nice then it is big. If Anne is blue then Anne is green. All green, big things are blue. If something is cold and not big then it is green.
Anne is not big.
("Anne" "is" "big" "-")
Anne is blue.
("Anne" "is" "blue" "+")
Anne is not cold.
("Anne" "is" "cold" "-")
Anne is green.
("Anne" "is" "green" "+")
Anne is not kind.
("Anne" "is" "kind" "-")
Anne is not nice.
("Anne" "is" "nice" "-")
Anne is young.
("Anne" "is" "young" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is not nice.
("Erin" "is" "nice" "-")
Erin is young.
("Erin" "is" "young" "+")
If Erin is not young then Erin is not nice.
((("Erin" "is" "young" "~")) -> ("Erin" "is" "nice" "-"))
All kind, nice things are not cold.
((("something" "is" "kind" "+") ("something" "is" "nice" "+")) -> ("something" "is" "cold" "-"))
If something is kind and not nice then it is big.
((("something" "is" "kind" "+") ("something" "is" "nice" "~")) -> ("something" "is" "big" "+"))
If Anne is blue then Anne is green.
((("Anne" "is" "blue" "+")) -> ("Anne" "is" "green" "+"))
All green, big things are blue.
((("something" "is" "green" "+") ("something" "is" "big" "+")) -> ("something" "is" "blue" "+"))
If something is cold and not big then it is green.
((("something" "is" "cold" "+") ("something" "is" "big" "~")) -> ("something" "is" "green" "+"))
Anne is blue.
True
1
proof
[(triple2)]
("Anne" "is" "blue" "+")
triple2
Erin is not young.
False
1
inv-proof
[(triple14)]
("Erin" "is" "young" "-")
triple14
@0: Anne is blue.[(triple2)] Anne is green.[(triple4 OR ((triple2) -> rule4))] Anne is not big.[(triple1)] Anne is not cold.[(triple3)] Anne is not kind.[(triple5)] Anne is not nice.[(triple6)] Anne is young.[(triple7)] Erin is big.[(triple8 OR ((triple12 triple13) -> rule3))] Erin is blue.[(triple9 OR ((triple11 triple8) -> rule5) OR ((triple11 ((triple12 triple13) -> rule3)) -> rule5))] Erin is cold.[(triple10)] Erin is green.[(triple11)] Erin is kind.[(triple12)] Erin is not nice.[(triple13)] Erin is young.[(triple14)]
Anne is blue.
("Anne" "is" "blue" "+")
triple2
Anne is green.
("Anne" "is" "green" "+")
triple4
((triple2) -> (rule4 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is not big.
("Anne" "is" "big" "-")
triple1
Anne is not cold.
("Anne" "is" "cold" "-")
triple3
Anne is not kind.
("Anne" "is" "kind" "-")
triple5
Anne is not nice.
("Anne" "is" "nice" "-")
triple6
Anne is young.
("Anne" "is" "young" "+")
triple7
Erin is big.
("Erin" "is" "big" "+")
triple8
((triple12 triple13) -> (rule3 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
triple9
((triple11 triple8) -> (rule5 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
((triple11 ((triple12 triple13) -> (rule3 % int2))) -> (rule5 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is cold.
("Erin" "is" "cold" "+")
triple10
Erin is green.
("Erin" "is" "green" "+")
triple11
Erin is kind.
("Erin" "is" "kind" "+")
triple12
Erin is not nice.
("Erin" "is" "nice" "-")
triple13
Erin is young.
("Erin" "is" "young" "+")
triple14