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