Charlie is big. Charlie is not blue. Charlie is green. Charlie is kind. Charlie is quiet. Charlie is smart. Charlie is young. If Charlie is kind and Charlie is not young then Charlie is smart. If Charlie is blue then Charlie is smart. If someone is quiet and kind then they are green. If someone is blue and not quiet then they are green. Big people are green. If someone is kind and green then they are smart.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is not blue.
("Charlie" "is" "blue" "-")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is young.
("Charlie" "is" "young" "+")
If Charlie is kind and Charlie is not young then Charlie is smart.
((("Charlie" "is" "kind" "+") ("Charlie" "is" "young" "~")) -> ("Charlie" "is" "smart" "+"))
If Charlie is blue then Charlie is smart.
((("Charlie" "is" "blue" "+")) -> ("Charlie" "is" "smart" "+"))
If someone is quiet and kind then they are green.
((("someone" "is" "quiet" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "green" "+"))
If someone is blue and not quiet then they are green.
((("someone" "is" "blue" "+") ("someone" "is" "quiet" "~")) -> ("someone" "is" "green" "+"))
Big people are green.
((("someone" "is" "big" "+")) -> ("someone" "is" "green" "+"))
If someone is kind and green then they are smart.
((("someone" "is" "kind" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "smart" "+"))
Charlie is big.
True
1
proof
[(triple1)]
("Charlie" "is" "big" "+")
triple1
Charlie is not smart.
False
1
inv-proof
[(triple6 OR ((triple4 triple3) -> rule6) OR ((triple4 ((triple1) -> rule5)) -> rule6) OR ((triple4 ((triple5 triple4) -> rule3)) -> rule6))]
("Charlie" "is" "smart" "-")
triple6
((triple4 triple3) -> (rule6 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
((triple4 ((triple1) -> (rule5 % int2))) -> (rule6 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
((triple4 ((triple5 triple4) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
@0: Charlie is big.[(triple1)] Charlie is green.[(triple3 OR ((triple1) -> rule5) OR ((triple5 triple4) -> rule3))] Charlie is kind.[(triple4)] Charlie is not blue.[(triple2)] Charlie is quiet.[(triple5)] Charlie is smart.[(triple6 OR ((triple4 triple3) -> rule6) OR ((triple4 ((triple1) -> rule5)) -> rule6) OR ((triple4 ((triple5 triple4) -> rule3)) -> rule6))] Charlie is young.[(triple7)]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is green.
("Charlie" "is" "green" "+")
triple3
((triple1) -> (rule5 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
((triple5 triple4) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple4
Charlie is not blue.
("Charlie" "is" "blue" "-")
triple2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple5
Charlie is smart.
("Charlie" "is" "smart" "+")
triple6
((triple4 triple3) -> (rule6 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
((triple4 ((triple1) -> (rule5 % int2))) -> (rule6 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
((triple4 ((triple5 triple4) -> (rule3 % int2))) -> (rule6 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
triple7