Charlie is blue. Charlie is green. Charlie is kind. Charlie is nice. Charlie is red. Charlie is white. Charlie is young. If someone is kind then they are young. Young people are kind.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Charlie is young.
("Charlie" "is" "young" "+")
If someone is kind then they are young.
((("someone" "is" "kind" "+")) -> ("someone" "is" "young" "+"))
Young people are kind.
((("someone" "is" "young" "+")) -> ("someone" "is" "kind" "+"))
Charlie is nice.
True
1
proof
[(triple4)]
("Charlie" "is" "nice" "+")
triple4
Charlie is not young.
False
1
inv-proof
[(triple7 OR ((triple3) -> rule1))]
("Charlie" "is" "young" "-")
triple7
((triple3) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
@0: Charlie is blue.[(triple1)] Charlie is green.[(triple2)] Charlie is kind.[(triple3 OR ((triple7) -> rule2))] Charlie is nice.[(triple4)] Charlie is red.[(triple5)] Charlie is white.[(triple6)] Charlie is young.[(triple7 OR ((triple3) -> rule1))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Charlie is green.
("Charlie" "is" "green" "+")
triple2
Charlie is kind.
("Charlie" "is" "kind" "+")
triple3
((triple7) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple4
Charlie is red.
("Charlie" "is" "red" "+")
triple5
Charlie is white.
("Charlie" "is" "white" "+")
triple6
Charlie is young.
("Charlie" "is" "young" "+")
triple7
((triple3) -> (rule1 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1