Charlie is cold. Charlie is furry. Charlie is green. Charlie is red. Charlie is smart. Charlie is not white. Charlie is young. If Charlie is not young then Charlie is red. If Charlie is green and Charlie is not white then Charlie is red.
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is not white.
("Charlie" "is" "white" "-")
Charlie is young.
("Charlie" "is" "young" "+")
If Charlie is not young then Charlie is red.
((("Charlie" "is" "young" "~")) -> ("Charlie" "is" "red" "+"))
If Charlie is green and Charlie is not white then Charlie is red.
((("Charlie" "is" "green" "+") ("Charlie" "is" "white" "~")) -> ("Charlie" "is" "red" "+"))
Charlie is young.
True
1
proof
[(triple7)]
("Charlie" "is" "young" "+")
triple7
Charlie is not smart.
False
1
inv-proof
[(triple5)]
("Charlie" "is" "smart" "-")
triple5
@0: Charlie is cold.[(triple1)] Charlie is furry.[(triple2)] Charlie is green.[(triple3)] Charlie is not white.[(triple6)] Charlie is red.[(triple4 OR ((triple3 triple6) -> rule2))] Charlie is smart.[(triple5)] Charlie is young.[(triple7)]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple2
Charlie is green.
("Charlie" "is" "green" "+")
triple3
Charlie is not white.
("Charlie" "is" "white" "-")
triple6
Charlie is red.
("Charlie" "is" "red" "+")
triple4
((triple3 triple6) -> (rule2 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
triple5
Charlie is young.
("Charlie" "is" "young" "+")
triple7