Anne is blue. Anne is green. Anne is kind. Anne is not quiet. Anne is not rough. Anne is round. Anne is smart. Charlie is blue. Charlie is not green. Charlie is kind. Charlie is quiet. Charlie is rough. Charlie is round. Charlie is smart. All green things are round. If Charlie is green and Charlie is not quiet then Charlie is kind. If something is green and not round then it is blue.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is not quiet.
("Anne" "is" "quiet" "-")
Anne is not rough.
("Anne" "is" "rough" "-")
Anne is round.
("Anne" "is" "round" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is not green.
("Charlie" "is" "green" "-")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
All green things are round.
((("something" "is" "green" "+")) -> ("something" "is" "round" "+"))
If Charlie is green and Charlie is not quiet then Charlie is kind.
((("Charlie" "is" "green" "+") ("Charlie" "is" "quiet" "~")) -> ("Charlie" "is" "kind" "+"))
If something is green and not round then it is blue.
((("something" "is" "green" "+") ("something" "is" "round" "~")) -> ("something" "is" "blue" "+"))
Anne is not quiet.
True
1
proof
[(triple4)]
("Anne" "is" "quiet" "-")
triple4
Charlie is not blue.
False
1
inv-proof
[(triple8)]
("Charlie" "is" "blue" "-")
triple8
@0: Anne is blue.[(triple1)] Anne is green.[(triple2)] Anne is kind.[(triple3)] Anne is not quiet.[(triple4)] Anne is not rough.[(triple5)] Anne is round.[(triple6 OR ((triple2) -> rule1))] Anne is smart.[(triple7)] Charlie is blue.[(triple8)] Charlie is kind.[(triple10)] Charlie is not green.[(triple9)] Charlie is quiet.[(triple11)] Charlie is rough.[(triple12)] Charlie is round.[(triple13)] Charlie is smart.[(triple14)]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple2
Anne is kind.
("Anne" "is" "kind" "+")
triple3
Anne is not quiet.
("Anne" "is" "quiet" "-")
triple4
Anne is not rough.
("Anne" "is" "rough" "-")
triple5
Anne is round.
("Anne" "is" "round" "+")
triple6
((triple2) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
triple7
Charlie is blue.
("Charlie" "is" "blue" "+")
triple8
Charlie is kind.
("Charlie" "is" "kind" "+")
triple10
Charlie is not green.
("Charlie" "is" "green" "-")
triple9
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple11
Charlie is rough.
("Charlie" "is" "rough" "+")
triple12
Charlie is round.
("Charlie" "is" "round" "+")
triple13
Charlie is smart.
("Charlie" "is" "smart" "+")
triple14