Charlie is big. Charlie is blue. Charlie is quiet. Charlie is not red. Charlie is rough. Charlie is smart. Charlie is white. Harry is big. Harry is blue. Harry is quiet. Harry is not red. Harry is rough. Harry is smart. Harry is white. If Harry is not quiet then Harry is blue. If someone is rough and red then they are not big.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is not red.
("Charlie" "is" "red" "-")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is not red.
("Harry" "is" "red" "-")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is white.
("Harry" "is" "white" "+")
If Harry is not quiet then Harry is blue.
((("Harry" "is" "quiet" "~")) -> ("Harry" "is" "blue" "+"))
If someone is rough and red then they are not big.
((("someone" "is" "rough" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "big" "-"))
Harry is big.
True
1
proof
[(triple8)]
("Harry" "is" "big" "+")
triple8
Harry is not rough.
False
1
inv-proof
[(triple12)]
("Harry" "is" "rough" "-")
triple12
@0: Charlie is big.[(triple1)] Charlie is blue.[(triple2)] Charlie is not red.[(triple4)] Charlie is quiet.[(triple3)] Charlie is rough.[(triple5)] Charlie is smart.[(triple6)] Charlie is white.[(triple7)] Harry is big.[(triple8)] Harry is blue.[(triple9)] Harry is not red.[(triple11)] Harry is quiet.[(triple10)] Harry is rough.[(triple12)] Harry is smart.[(triple13)] Harry is white.[(triple14)]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple2
Charlie is not red.
("Charlie" "is" "red" "-")
triple4
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple3
Charlie is rough.
("Charlie" "is" "rough" "+")
triple5
Charlie is smart.
("Charlie" "is" "smart" "+")
triple6
Charlie is white.
("Charlie" "is" "white" "+")
triple7
Harry is big.
("Harry" "is" "big" "+")
triple8
Harry is blue.
("Harry" "is" "blue" "+")
triple9
Harry is not red.
("Harry" "is" "red" "-")
triple11
Harry is quiet.
("Harry" "is" "quiet" "+")
triple10
Harry is rough.
("Harry" "is" "rough" "+")
triple12
Harry is smart.
("Harry" "is" "smart" "+")
triple13
Harry is white.
("Harry" "is" "white" "+")
triple14