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