Charlie is big. Charlie is cold. Charlie is furry. Charlie is quiet. Charlie is red. Charlie is smart. Charlie is white. Smart, big things are quiet. Smart things are furry.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Smart, big things are quiet.
((("something" "is" "smart" "+") ("something" "is" "big" "+")) -> ("something" "is" "quiet" "+"))
Smart things are furry.
((("something" "is" "smart" "+")) -> ("something" "is" "furry" "+"))
Charlie is cold.
True
1
proof
[(triple2)]
("Charlie" "is" "cold" "+")
triple2
Charlie is not cold.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "cold" "-")
triple2
@0: Charlie is big.[(triple1)] Charlie is cold.[(triple2)] Charlie is furry.[(triple3 OR ((triple6) -> rule2))] Charlie is quiet.[(triple4 OR ((triple6 triple1) -> rule1))] Charlie is red.[(triple5)] Charlie is smart.[(triple6)] Charlie is white.[(triple7)]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
Charlie is furry.
("Charlie" "is" "furry" "+")
triple3
((triple6) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple4
((triple6 triple1) -> (rule1 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
triple5
Charlie is smart.
("Charlie" "is" "smart" "+")
triple6
Charlie is white.
("Charlie" "is" "white" "+")
triple7