Anne is kind. Anne is nice. Anne is red. Anne is rough. Anne is round. Anne is white. Anne is young. All red, nice people are rough. If someone is round then they are kind. If someone is kind and red then they are young. If someone is nice then they are kind. All nice people are kind. All white people are rough.
Anne is kind.
("Anne" "is" "kind" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is white.
("Anne" "is" "white" "+")
Anne is young.
("Anne" "is" "young" "+")
All red, nice people are rough.
((("someone" "is" "red" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "rough" "+"))
If someone is round then they are kind.
((("someone" "is" "round" "+")) -> ("someone" "is" "kind" "+"))
If someone is kind and red then they are young.
((("someone" "is" "kind" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "young" "+"))
If someone is nice then they are kind.
((("someone" "is" "nice" "+")) -> ("someone" "is" "kind" "+"))
All nice people are kind.
((("someone" "is" "nice" "+")) -> ("someone" "is" "kind" "+"))
All white people are rough.
((("someone" "is" "white" "+")) -> ("someone" "is" "rough" "+"))
Anne is red.
True
1
proof
[(triple3)]
("Anne" "is" "red" "+")
triple3
Anne is not young.
False
1
inv-proof
[(triple7 OR ((triple1 triple3) -> rule3) OR ((((triple2) -> rule4) triple3) -> rule3) OR ((((triple2) -> rule5) triple3) -> rule3) OR ((((triple5) -> rule2) triple3) -> rule3))]
("Anne" "is" "young" "-")
triple7
((triple1 triple3) -> (rule3 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
((((triple2) -> (rule4 % int2)) triple3) -> (rule3 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
((((triple2) -> (rule5 % int2)) triple3) -> (rule3 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
((((triple5) -> (rule2 % int2)) triple3) -> (rule3 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
@0: Anne is kind.[(triple1 OR ((triple2) -> rule4) OR ((triple2) -> rule5) OR ((triple5) -> rule2))] Anne is nice.[(triple2)] Anne is red.[(triple3)] Anne is rough.[(triple4 OR ((triple6) -> rule6) OR ((triple3 triple2) -> rule1))] Anne is round.[(triple5)] Anne is white.[(triple6)] Anne is young.[(triple7 OR ((triple1 triple3) -> rule3) OR ((((triple2) -> rule4) triple3) -> rule3) OR ((((triple2) -> rule5) triple3) -> rule3) OR ((((triple5) -> rule2) triple3) -> rule3))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
((triple2) -> (rule4 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
((triple2) -> (rule5 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
((triple5) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
triple2
Anne is red.
("Anne" "is" "red" "+")
triple3
Anne is rough.
("Anne" "is" "rough" "+")
triple4
((triple6) -> (rule6 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
((triple3 triple2) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
triple5
Anne is white.
("Anne" "is" "white" "+")
triple6
Anne is young.
("Anne" "is" "young" "+")
triple7
((triple1 triple3) -> (rule3 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
((((triple2) -> (rule4 % int2)) triple3) -> (rule3 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
((((triple2) -> (rule5 % int2)) triple3) -> (rule3 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
((((triple5) -> (rule2 % int2)) triple3) -> (rule3 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2