Charlie is blue. Charlie is furry. Charlie is kind. Charlie is nice. Charlie is quiet. Charlie is rough. Charlie is not white. Nice things are blue. If Charlie is furry then Charlie is not white.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is not white.
("Charlie" "is" "white" "-")
Nice things are blue.
((("something" "is" "nice" "+")) -> ("something" "is" "blue" "+"))
If Charlie is furry then Charlie is not white.
((("Charlie" "is" "furry" "+")) -> ("Charlie" "is" "white" "-"))
Charlie is rough.
True
1
proof
[(triple6)]
("Charlie" "is" "rough" "+")
triple6
Charlie is not nice.
False
1
inv-proof
[(triple4)]
("Charlie" "is" "nice" "-")
triple4
@0: Charlie is blue.[(triple1 OR ((triple4) -> rule1))] Charlie is furry.[(triple2)] Charlie is kind.[(triple3)] Charlie is nice.[(triple4)] Charlie is not white.[(triple7 OR ((triple2) -> rule2))] Charlie is quiet.[(triple5)] Charlie is rough.[(triple6)]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
((triple4) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple2
Charlie is kind.
("Charlie" "is" "kind" "+")
triple3
Charlie is nice.
("Charlie" "is" "nice" "+")
triple4
Charlie is not white.
("Charlie" "is" "white" "-")
triple7
((triple2) -> (rule2 % int1))
Charlie is not white.
("Charlie" "is" "white" "-")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple5
Charlie is rough.
("Charlie" "is" "rough" "+")
triple6