Charlie is blue. Charlie is furry. Charlie is green. Charlie is kind. Charlie is rough. Charlie is round. Charlie is smart. All green things are kind.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
All green things are kind.
((("something" "is" "green" "+")) -> ("something" "is" "kind" "+"))
Charlie is green.
True
1
proof
[(triple3)]
("Charlie" "is" "green" "+")
triple3
Charlie is not smart.
False
1
inv-proof
[(triple7)]
("Charlie" "is" "smart" "-")
triple7
@0: Charlie is blue.[(triple1)] Charlie is furry.[(triple2)] Charlie is green.[(triple3)] Charlie is kind.[(triple4 OR ((triple3) -> rule1))] Charlie is rough.[(triple5)] Charlie is round.[(triple6)] Charlie is smart.[(triple7)]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple2
Charlie is green.
("Charlie" "is" "green" "+")
triple3
Charlie is kind.
("Charlie" "is" "kind" "+")
triple4
((triple3) -> (rule1 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
triple5
Charlie is round.
("Charlie" "is" "round" "+")
triple6
Charlie is smart.
("Charlie" "is" "smart" "+")
triple7