Anne is kind. Anne is nice. Anne is quiet. Anne is red. Anne is rough. Anne is not smart. Anne is not young. Gary is kind. Gary is nice. Gary is quiet. Gary is red. Gary is rough. Gary is smart. Gary is young. Young things are smart. If Gary is not young then Gary is quiet. If something is young and not rough then it is red. If something is nice and not quiet then it is not kind. Smart, young things are nice. If something is kind and not red then it is nice.
Anne is kind.
("Anne" "is" "kind" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is not smart.
("Anne" "is" "smart" "-")
Anne is not young.
("Anne" "is" "young" "-")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is young.
("Gary" "is" "young" "+")
Young things are smart.
((("something" "is" "young" "+")) -> ("something" "is" "smart" "+"))
If Gary is not young then Gary is quiet.
((("Gary" "is" "young" "~")) -> ("Gary" "is" "quiet" "+"))
If something is young and not rough then it is red.
((("something" "is" "young" "+") ("something" "is" "rough" "~")) -> ("something" "is" "red" "+"))
If something is nice and not quiet then it is not kind.
((("something" "is" "nice" "+") ("something" "is" "quiet" "~")) -> ("something" "is" "kind" "-"))
Smart, young things are nice.
((("something" "is" "smart" "+") ("something" "is" "young" "+")) -> ("something" "is" "nice" "+"))
If something is kind and not red then it is nice.
((("something" "is" "kind" "+") ("something" "is" "red" "~")) -> ("something" "is" "nice" "+"))
Anne is kind.
True
1
proof
[(triple1)]
("Anne" "is" "kind" "+")
triple1
Gary is not rough.
False
1
inv-proof
[(triple12)]
("Gary" "is" "rough" "-")
triple12
@0: Anne is kind.[(triple1)] Anne is nice.[(triple2)] Anne is not smart.[(triple6)] Anne is not young.[(triple7)] Anne is quiet.[(triple3)] Anne is red.[(triple4)] Anne is rough.[(triple5)] Gary is kind.[(triple8)] Gary is nice.[(triple9 OR ((triple13 triple14) -> rule5) OR ((((triple14) -> rule1) triple14) -> rule5))] Gary is quiet.[(triple10)] Gary is red.[(triple11)] Gary is rough.[(triple12)] Gary is smart.[(triple13 OR ((triple14) -> rule1))] Gary is young.[(triple14)]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Anne is nice.
("Anne" "is" "nice" "+")
triple2
Anne is not smart.
("Anne" "is" "smart" "-")
triple6
Anne is not young.
("Anne" "is" "young" "-")
triple7
Anne is quiet.
("Anne" "is" "quiet" "+")
triple3
Anne is red.
("Anne" "is" "red" "+")
triple4
Anne is rough.
("Anne" "is" "rough" "+")
triple5
Gary is kind.
("Gary" "is" "kind" "+")
triple8
Gary is nice.
("Gary" "is" "nice" "+")
triple9
((triple13 triple14) -> (rule5 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
((((triple14) -> (rule1 % int2)) triple14) -> (rule5 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
triple10
Gary is red.
("Gary" "is" "red" "+")
triple11
Gary is rough.
("Gary" "is" "rough" "+")
triple12
Gary is smart.
("Gary" "is" "smart" "+")
triple13
((triple14) -> (rule1 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
triple14