Charlie is blue. Charlie is cold. Charlie is green. Charlie is kind. Charlie is nice. Charlie is rough. Charlie is smart. Nice, rough people are green.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Nice, rough people are green.
((("someone" "is" "nice" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "green" "+"))
Charlie is green.
True
1
proof
[(triple3 OR ((triple5 triple6) -> rule1))]
("Charlie" "is" "green" "+")
triple3
((triple5 triple6) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is not blue.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "blue" "-")
triple1
@0: Charlie is blue.[(triple1)] Charlie is cold.[(triple2)] Charlie is green.[(triple3 OR ((triple5 triple6) -> rule1))] Charlie is kind.[(triple4)] Charlie is nice.[(triple5)] Charlie is rough.[(triple6)] Charlie is smart.[(triple7)]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
Charlie is green.
("Charlie" "is" "green" "+")
triple3
((triple5 triple6) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple4
Charlie is nice.
("Charlie" "is" "nice" "+")
triple5
Charlie is rough.
("Charlie" "is" "rough" "+")
triple6
Charlie is smart.
("Charlie" "is" "smart" "+")
triple7