Charlie is big. Charlie is blue. Charlie is green. Charlie is nice. Charlie is rough. Charlie is white. Charlie is young. Nice, rough things are green. All nice things are young. If something is green then it is rough.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Nice, rough things are green.
((("something" "is" "nice" "+") ("something" "is" "rough" "+")) -> ("something" "is" "green" "+"))
All nice things are young.
((("something" "is" "nice" "+")) -> ("something" "is" "young" "+"))
If something is green then it is rough.
((("something" "is" "green" "+")) -> ("something" "is" "rough" "+"))
Charlie is green.
True
1
proof
[(triple3 OR ((triple4 triple5) -> rule1))]
("Charlie" "is" "green" "+")
triple3
((triple4 triple5) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is not white.
False
1
inv-proof
[(triple6)]
("Charlie" "is" "white" "-")
triple6
@0: Charlie is big.[(triple1)] Charlie is blue.[(triple2)] Charlie is green.[(triple3 OR ((triple4 triple5) -> rule1))] Charlie is nice.[(triple4)] Charlie is rough.[(triple5 OR ((triple3) -> rule3))] Charlie is white.[(triple6)] Charlie is young.[(triple7 OR ((triple4) -> rule2))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple2
Charlie is green.
("Charlie" "is" "green" "+")
triple3
((triple4 triple5) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple4
Charlie is rough.
("Charlie" "is" "rough" "+")
triple5
((triple3) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
triple6
Charlie is young.
("Charlie" "is" "young" "+")
triple7
((triple4) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1