Charlie is blue. Charlie is cold. Charlie is furry. Charlie is kind. Charlie is red. Charlie is smart. Charlie is young. Kind people are young. All red, young people are kind.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Kind people are young.
((("someone" "is" "kind" "+")) -> ("someone" "is" "young" "+"))
All red, young people are kind.
((("someone" "is" "red" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "kind" "+"))
Charlie is red.
True
1
proof
[(triple5)]
("Charlie" "is" "red" "+")
triple5
Charlie is not smart.
False
1
inv-proof
[(triple6)]
("Charlie" "is" "smart" "-")
triple6
@0: Charlie is blue.[(triple1)] Charlie is cold.[(triple2)] Charlie is furry.[(triple3)] Charlie is kind.[(triple4 OR ((triple5 triple7) -> rule2))] Charlie is red.[(triple5)] Charlie is smart.[(triple6)] Charlie is young.[(triple7 OR ((triple4) -> rule1))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
Charlie is furry.
("Charlie" "is" "furry" "+")
triple3
Charlie is kind.
("Charlie" "is" "kind" "+")
triple4
((triple5 triple7) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
triple5
Charlie is smart.
("Charlie" "is" "smart" "+")
triple6
Charlie is young.
("Charlie" "is" "young" "+")
triple7
((triple4) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1