Anne is blue. Anne is furry. Anne is red. If Anne is young then Anne is nice. Furry, young people are rough. If someone is young then they are kind. All blue, rough people are red. If someone is young and furry then they are blue. If Anne is furry then Anne is young.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is furry.
("Anne" "is" "furry" "+")
Anne is red.
("Anne" "is" "red" "+")
If Anne is young then Anne is nice.
((("Anne" "is" "young" "+")) -> ("Anne" "is" "nice" "+"))
Furry, young people are rough.
((("someone" "is" "furry" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "rough" "+"))
If someone is young then they are kind.
((("someone" "is" "young" "+")) -> ("someone" "is" "kind" "+"))
All blue, rough people are red.
((("someone" "is" "blue" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "red" "+"))
If someone is young and furry then they are blue.
((("someone" "is" "young" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "blue" "+"))
If Anne is furry then Anne is young.
((("Anne" "is" "furry" "+")) -> ("Anne" "is" "young" "+"))
Anne is blue.
True
1
proof
[(triple1 OR ((((triple2) -> rule6) triple2) -> rule5))]
("Anne" "is" "blue" "+")
triple1
((((triple2) -> (rule6 % int2)) triple2) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is not blue.
False
1
inv-proof
[(triple1 OR ((((triple2) -> rule6) triple2) -> rule5))]
("Anne" "is" "blue" "-")
triple1
((((triple2) -> (rule6 % int2)) triple2) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is young.
True
2
proof
[(((triple2) -> rule6))]
("Anne" "is" "young" "+")
((triple2) -> (rule6 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is not young.
False
2
inv-proof
[(((triple2) -> rule6))]
("Anne" "is" "young" "-")
((triple2) -> (rule6 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is nice.
True
3
proof
[(((((triple2) -> rule6)) -> rule1))]
("Anne" "is" "nice" "+")
((((triple2) -> (rule6 % int2))) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is not kind.
False
3
inv-proof
[(((((triple2) -> rule6)) -> rule3))]
("Anne" "is" "kind" "-")
((((triple2) -> (rule6 % int2))) -> (rule3 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
@0: Anne is blue.[(triple1 OR ((((triple2) -> rule6) triple2) -> rule5))] Anne is furry.[(triple2)] Anne is red.[(triple3 OR ((triple1 ((triple2 ((triple2) -> rule6)) -> rule2)) -> rule4) OR ((((((triple2) -> rule6) triple2) -> rule5) ((triple2 ((triple2) -> rule6)) -> rule2)) -> rule4))] @1: Anne is young.[(((triple2) -> rule6))] @2: Anne is kind.[(((((triple2) -> rule6)) -> rule3))] Anne is nice.[(((((triple2) -> rule6)) -> rule1))] Anne is rough.[(((triple2 ((triple2) -> rule6)) -> rule2))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
((((triple2) -> (rule6 % int2)) triple2) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
triple2
Anne is red.
("Anne" "is" "red" "+")
triple3
((triple1 ((triple2 ((triple2) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
((((((triple2) -> (rule6 % int4)) triple2) -> (rule5 % int3)) ((triple2 ((triple2) -> (rule6 % int4))) -> (rule2 % int2))) -> (rule4 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Anne is young.
("Anne" "is" "young" "+")
int4
Anne is young.
("Anne" "is" "young" "+")
((triple2) -> (rule6 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
((((triple2) -> (rule6 % int2))) -> (rule3 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
((((triple2) -> (rule6 % int2))) -> (rule1 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
((triple2 ((triple2) -> (rule6 % int2))) -> (rule2 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2