Charlie is big. Charlie is blue. Charlie is kind. Charlie is nice. Charlie is red. Charlie is rough. Charlie is smart. Rough, kind things 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 smart.
("Charlie" "is" "smart" "+")
Rough, kind things are nice.
((("something" "is" "rough" "+") ("something" "is" "kind" "+")) -> ("something" "is" "nice" "+"))
Charlie is smart.
True
1
proof
[(triple7)]
("Charlie" "is" "smart" "+")
triple7
Charlie is not rough.
False
1
inv-proof
[(triple6)]
("Charlie" "is" "rough" "-")
triple6
@0: Charlie is big.[(triple1)] Charlie is blue.[(triple2)] Charlie is kind.[(triple3)] Charlie is nice.[(triple4 OR ((triple6 triple3) -> rule1))] Charlie is red.[(triple5)] Charlie is rough.[(triple6)] Charlie is smart.[(triple7)]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple2
Charlie is kind.
("Charlie" "is" "kind" "+")
triple3
Charlie is nice.
("Charlie" "is" "nice" "+")
triple4
((triple6 triple3) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
triple5
Charlie is rough.
("Charlie" "is" "rough" "+")
triple6
Charlie is smart.
("Charlie" "is" "smart" "+")
triple7