Charlie is big. Charlie is furry. Charlie is green. Charlie is kind. Charlie is red. Charlie is round. Charlie is smart. If Charlie is big then Charlie is kind. If something is kind and smart then it is furry. Round, green things are red.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
If Charlie is big then Charlie is kind.
((("Charlie" "is" "big" "+")) -> ("Charlie" "is" "kind" "+"))
If something is kind and smart then it is furry.
((("something" "is" "kind" "+") ("something" "is" "smart" "+")) -> ("something" "is" "furry" "+"))
Round, green things are red.
((("something" "is" "round" "+") ("something" "is" "green" "+")) -> ("something" "is" "red" "+"))
Charlie is kind.
True
1
proof
[(triple4 OR ((triple1) -> rule1))]
("Charlie" "is" "kind" "+")
triple4
((triple1) -> (rule1 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is not smart.
False
1
inv-proof
[(triple7)]
("Charlie" "is" "smart" "-")
triple7
@0: Charlie is big.[(triple1)] Charlie is furry.[(triple2 OR ((triple4 triple7) -> rule2) OR ((((triple1) -> rule1) triple7) -> rule2))] Charlie is green.[(triple3)] Charlie is kind.[(triple4 OR ((triple1) -> rule1))] Charlie is red.[(triple5 OR ((triple6 triple3) -> rule3))] Charlie is round.[(triple6)] Charlie is smart.[(triple7)]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple2
((triple4 triple7) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
((((triple1) -> (rule1 % int2)) triple7) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
triple3
Charlie is kind.
("Charlie" "is" "kind" "+")
triple4
((triple1) -> (rule1 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
triple5
((triple6 triple3) -> (rule3 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
triple6
Charlie is smart.
("Charlie" "is" "smart" "+")
triple7