Anne is not big. Anne is blue. Anne is kind. Anne is quiet. Anne is rough. Anne is round. Anne is young. If someone is kind and not round then they are big. If someone is blue and big then they are kind. Round, young people are kind. If someone is rough then they are young. All rough people are blue. All big, kind people are not blue. If Anne is round then Anne is blue. If Anne is blue and Anne is not round then Anne is young.
Anne is not big.
("Anne" "is" "big" "-")
Anne is blue.
("Anne" "is" "blue" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is young.
("Anne" "is" "young" "+")
If someone is kind and not round then they are big.
((("someone" "is" "kind" "+") ("someone" "is" "round" "~")) -> ("someone" "is" "big" "+"))
If someone is blue and big then they are kind.
((("someone" "is" "blue" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "kind" "+"))
Round, young people are kind.
((("someone" "is" "round" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "kind" "+"))
If someone is rough then they are young.
((("someone" "is" "rough" "+")) -> ("someone" "is" "young" "+"))
All rough people are blue.
((("someone" "is" "rough" "+")) -> ("someone" "is" "blue" "+"))
All big, kind people are not blue.
((("someone" "is" "big" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "-"))
If Anne is round then Anne is blue.
((("Anne" "is" "round" "+")) -> ("Anne" "is" "blue" "+"))
If Anne is blue and Anne is not round then Anne is young.
((("Anne" "is" "blue" "+") ("Anne" "is" "round" "~")) -> ("Anne" "is" "young" "+"))
Anne is rough.
True
1
proof
[(triple5)]
("Anne" "is" "rough" "+")
triple5
Anne is not kind.
False
1
inv-proof
[(triple3 OR ((triple6 triple7) -> rule3) OR ((triple6 ((triple5) -> rule4)) -> rule3))]
("Anne" "is" "kind" "-")
triple3
((triple6 triple7) -> (rule3 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
((triple6 ((triple5) -> (rule4 % int2))) -> (rule3 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
@0: Anne is blue.[(triple2 OR ((triple5) -> rule5) OR ((triple6) -> rule7))] Anne is kind.[(triple3 OR ((triple6 triple7) -> rule3) OR ((triple6 ((triple5) -> rule4)) -> rule3))] Anne is not big.[(triple1)] Anne is quiet.[(triple4)] Anne is rough.[(triple5)] Anne is round.[(triple6)] Anne is young.[(triple7 OR ((triple5) -> rule4))]
Anne is blue.
("Anne" "is" "blue" "+")
triple2
((triple5) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
((triple6) -> (rule7 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
triple3
((triple6 triple7) -> (rule3 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
((triple6 ((triple5) -> (rule4 % int2))) -> (rule3 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is not big.
("Anne" "is" "big" "-")
triple1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple4
Anne is rough.
("Anne" "is" "rough" "+")
triple5
Anne is round.
("Anne" "is" "round" "+")
triple6
Anne is young.
("Anne" "is" "young" "+")
triple7
((triple5) -> (rule4 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1