Charlie is big. Charlie is cold. Charlie is furry. Charlie is kind. Charlie is nice. Charlie is quiet. Charlie is red. If someone is nice then they are furry. Furry people are quiet.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is red.
("Charlie" "is" "red" "+")
If someone is nice then they are furry.
((("someone" "is" "nice" "+")) -> ("someone" "is" "furry" "+"))
Furry people are quiet.
((("someone" "is" "furry" "+")) -> ("someone" "is" "quiet" "+"))
Charlie is big.
True
1
proof
[(triple1)]
("Charlie" "is" "big" "+")
triple1
Charlie is not nice.
False
1
inv-proof
[(triple5)]
("Charlie" "is" "nice" "-")
triple5
@0: Charlie is big.[(triple1)] Charlie is cold.[(triple2)] Charlie is furry.[(triple3 OR ((triple5) -> rule1))] Charlie is kind.[(triple4)] Charlie is nice.[(triple5)] Charlie is quiet.[(triple6 OR ((triple3) -> rule2) OR ((((triple5) -> rule1)) -> rule2))] Charlie is red.[(triple7)]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
Charlie is furry.
("Charlie" "is" "furry" "+")
triple3
((triple5) -> (rule1 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple4
Charlie is nice.
("Charlie" "is" "nice" "+")
triple5
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple6
((triple3) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
((((triple5) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
triple7