Anne is green. Anne is kind. Anne is nice. Anne is not quiet. Anne is red. Anne is smart. Anne is not young. Quiet things are nice. If Anne is green then Anne is red. Green, smart things are red. Green, red things are not young. If something is green and not smart then it is young. If something is kind and not nice then it is green.
Anne is green.
("Anne" "is" "green" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is not quiet.
("Anne" "is" "quiet" "-")
Anne is red.
("Anne" "is" "red" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is not young.
("Anne" "is" "young" "-")
Quiet things are nice.
((("something" "is" "quiet" "+")) -> ("something" "is" "nice" "+"))
If Anne is green then Anne is red.
((("Anne" "is" "green" "+")) -> ("Anne" "is" "red" "+"))
Green, smart things are red.
((("something" "is" "green" "+") ("something" "is" "smart" "+")) -> ("something" "is" "red" "+"))
Green, red things are not young.
((("something" "is" "green" "+") ("something" "is" "red" "+")) -> ("something" "is" "young" "-"))
If something is green and not smart then it is young.
((("something" "is" "green" "+") ("something" "is" "smart" "~")) -> ("something" "is" "young" "+"))
If something is kind and not nice then it is green.
((("something" "is" "kind" "+") ("something" "is" "nice" "~")) -> ("something" "is" "green" "+"))
Anne is not young.
True
1
proof
[(triple7 OR ((triple1 triple5) -> rule4) OR ((triple1 ((triple1) -> rule2)) -> rule4) OR ((triple1 ((triple1 triple6) -> rule3)) -> rule4))]
("Anne" "is" "young" "-")
triple7
((triple1 triple5) -> (rule4 % int1))
Anne is not young.
("Anne" "is" "young" "-")
int1
((triple1 ((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Anne is not young.
("Anne" "is" "young" "-")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
((triple1 ((triple1 triple6) -> (rule3 % int2))) -> (rule4 % int1))
Anne is not young.
("Anne" "is" "young" "-")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is not nice.
False
1
inv-proof
[(triple3)]
("Anne" "is" "nice" "-")
triple3
@0: Anne is green.[(triple1)] Anne is kind.[(triple2)] Anne is nice.[(triple3)] Anne is not quiet.[(triple4)] Anne is not young.[(triple7 OR ((triple1 triple5) -> rule4) OR ((triple1 ((triple1) -> rule2)) -> rule4) OR ((triple1 ((triple1 triple6) -> rule3)) -> rule4))] Anne is red.[(triple5 OR ((triple1) -> rule2) OR ((triple1 triple6) -> rule3))] Anne is smart.[(triple6)]
Anne is green.
("Anne" "is" "green" "+")
triple1
Anne is kind.
("Anne" "is" "kind" "+")
triple2
Anne is nice.
("Anne" "is" "nice" "+")
triple3
Anne is not quiet.
("Anne" "is" "quiet" "-")
triple4
Anne is not young.
("Anne" "is" "young" "-")
triple7
((triple1 triple5) -> (rule4 % int1))
Anne is not young.
("Anne" "is" "young" "-")
int1
((triple1 ((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Anne is not young.
("Anne" "is" "young" "-")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
((triple1 ((triple1 triple6) -> (rule3 % int2))) -> (rule4 % int1))
Anne is not young.
("Anne" "is" "young" "-")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
triple5
((triple1) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((triple1 triple6) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
triple6