Charlie is not big. Charlie is cold. Charlie is furry. Charlie is green. Charlie is kind. Charlie is white. Charlie is not young. If someone is big then they are white. If someone is kind then they are not big. If Charlie is kind then Charlie is furry. All white people are green. If someone is big and not white then they are not furry. If someone is green and not kind then they are furry.
Charlie is not big.
("Charlie" "is" "big" "-")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Charlie is not young.
("Charlie" "is" "young" "-")
If someone is big then they are white.
((("someone" "is" "big" "+")) -> ("someone" "is" "white" "+"))
If someone is kind then they are not big.
((("someone" "is" "kind" "+")) -> ("someone" "is" "big" "-"))
If Charlie is kind then Charlie is furry.
((("Charlie" "is" "kind" "+")) -> ("Charlie" "is" "furry" "+"))
All white people are green.
((("someone" "is" "white" "+")) -> ("someone" "is" "green" "+"))
If someone is big and not white then they are not furry.
((("someone" "is" "big" "+") ("someone" "is" "white" "~")) -> ("someone" "is" "furry" "-"))
If someone is green and not kind then they are furry.
((("someone" "is" "green" "+") ("someone" "is" "kind" "~")) -> ("someone" "is" "furry" "+"))
Charlie is cold.
True
1
proof
[(triple2)]
("Charlie" "is" "cold" "+")
triple2
Charlie is not kind.
False
1
inv-proof
[(triple5)]
("Charlie" "is" "kind" "-")
triple5
@0: Charlie is cold.[(triple2)] Charlie is furry.[(triple3 OR ((triple5) -> rule3))] Charlie is green.[(triple4 OR ((triple6) -> rule4))] Charlie is kind.[(triple5)] Charlie is not big.[(triple1 OR ((triple5) -> rule2))] Charlie is not young.[(triple7)] Charlie is white.[(triple6)]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
Charlie is furry.
("Charlie" "is" "furry" "+")
triple3
((triple5) -> (rule3 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
triple4
((triple6) -> (rule4 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple5
Charlie is not big.
("Charlie" "is" "big" "-")
triple1
((triple5) -> (rule2 % int1))
Charlie is not big.
("Charlie" "is" "big" "-")
int1
Charlie is not young.
("Charlie" "is" "young" "-")
triple7
Charlie is white.
("Charlie" "is" "white" "+")
triple6