Charlie is blue. Charlie is furry. Charlie is green. Charlie is quiet. Charlie is rough. Charlie is round. Charlie is smart. If Charlie is round and Charlie is not quiet then Charlie is furry.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
If Charlie is round and Charlie is not quiet then Charlie is furry.
((("Charlie" "is" "round" "+") ("Charlie" "is" "quiet" "~")) -> ("Charlie" "is" "furry" "+"))
Charlie is quiet.
True
1
proof
[(triple4)]
("Charlie" "is" "quiet" "+")
triple4
Charlie is not smart.
False
1
inv-proof
[(triple7)]
("Charlie" "is" "smart" "-")
triple7
@0: Charlie is blue.[(triple1)] Charlie is furry.[(triple2)] Charlie is green.[(triple3)] Charlie is quiet.[(triple4)] Charlie is rough.[(triple5)] Charlie is round.[(triple6)] Charlie is smart.[(triple7)]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple2
Charlie is green.
("Charlie" "is" "green" "+")
triple3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple4
Charlie is rough.
("Charlie" "is" "rough" "+")
triple5
Charlie is round.
("Charlie" "is" "round" "+")
triple6
Charlie is smart.
("Charlie" "is" "smart" "+")
triple7