Charlie is green. Charlie is kind. Charlie is smart. If someone is smart then they are big. Kind, rough people are young. If someone is kind and green then they are rough.
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
If someone is smart then they are big.
((("someone" "is" "smart" "+")) -> ("someone" "is" "big" "+"))
Kind, rough people are young.
((("someone" "is" "kind" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "young" "+"))
If someone is kind and green then they are rough.
((("someone" "is" "kind" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "rough" "+"))
Charlie is smart.
True
1
proof
[(triple3)]
("Charlie" "is" "smart" "+")
triple3
Charlie is not smart.
False
1
inv-proof
[(triple3)]
("Charlie" "is" "smart" "-")
triple3
Charlie is big.
True
2
proof
[(((triple3) -> rule1))]
("Charlie" "is" "big" "+")
((triple3) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is not big.
False
2
inv-proof
[(((triple3) -> rule1))]
("Charlie" "is" "big" "-")
((triple3) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is young.
True
5
proof
[(((triple2 ((triple2 triple1) -> rule3)) -> rule2))]
("Charlie" "is" "young" "+")
((triple2 ((triple2 triple1) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is not young.
False
5
inv-proof
[(((triple2 ((triple2 triple1) -> rule3)) -> rule2))]
("Charlie" "is" "young" "-")
((triple2 ((triple2 triple1) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
@0: Charlie is green.[(triple1)] Charlie is kind.[(triple2)] Charlie is smart.[(triple3)] @1: Charlie is big.[(((triple3) -> rule1))] Charlie is rough.[(((triple2 triple1) -> rule3))] @2: Charlie is young.[(((triple2 ((triple2 triple1) -> rule3)) -> rule2))]
Charlie is green.
("Charlie" "is" "green" "+")
triple1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple2
Charlie is smart.
("Charlie" "is" "smart" "+")
triple3
Charlie is big.
("Charlie" "is" "big" "+")
((triple3) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple2 triple1) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is young.
("Charlie" "is" "young" "+")
((triple2 ((triple2 triple1) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2