Anne is quiet. If Anne is quiet and Anne is kind then Anne is young. If Anne is quiet then Anne is furry. All furry, quiet things are red. Quiet things are rough. Furry things are young. If something is red then it is kind.
Anne is quiet.
("Anne" "is" "quiet" "+")
If Anne is quiet and Anne is kind then Anne is young.
((("Anne" "is" "quiet" "+") ("Anne" "is" "kind" "+")) -> ("Anne" "is" "young" "+"))
If Anne is quiet then Anne is furry.
((("Anne" "is" "quiet" "+")) -> ("Anne" "is" "furry" "+"))
All furry, quiet things are red.
((("something" "is" "furry" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "red" "+"))
Quiet things are rough.
((("something" "is" "quiet" "+")) -> ("something" "is" "rough" "+"))
Furry things are young.
((("something" "is" "furry" "+")) -> ("something" "is" "young" "+"))
If something is red then it is kind.
((("something" "is" "red" "+")) -> ("something" "is" "kind" "+"))
Anne is quiet.
True
1
proof
[(triple1)]
("Anne" "is" "quiet" "+")
triple1
Anne is not quiet.
False
1
inv-proof
[(triple1)]
("Anne" "is" "quiet" "-")
triple1
Anne is furry.
True
2
proof
[(((triple1) -> rule2))]
("Anne" "is" "furry" "+")
((triple1) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is not furry.
False
2
inv-proof
[(((triple1) -> rule2))]
("Anne" "is" "furry" "-")
((triple1) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is red.
True
4
proof
[(((((triple1) -> rule2) triple1) -> rule3))]
("Anne" "is" "red" "+")
((((triple1) -> (rule2 % int2)) triple1) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is not young.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule5) OR ((triple1 ((((((triple1) -> rule2) triple1) -> rule3)) -> rule6)) -> rule1))]
("Anne" "is" "young" "-")
((((triple1) -> (rule2 % int2))) -> (rule5 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
((triple1 ((((((triple1) -> (rule2 % int4)) triple1) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is furry.
("Anne" "is" "furry" "+")
int4
@0: Anne is quiet.[(triple1)] @1: Anne is furry.[(((triple1) -> rule2))] Anne is rough.[(((triple1) -> rule4))] @2: Anne is red.[(((((triple1) -> rule2) triple1) -> rule3))] Anne is young.[(((((triple1) -> rule2)) -> rule5) OR ((triple1 ((((((triple1) -> rule2) triple1) -> rule3)) -> rule6)) -> rule1))] @3: Anne is kind.[(((((((triple1) -> rule2) triple1) -> rule3)) -> rule6))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Anne is furry.
("Anne" "is" "furry" "+")
((triple1) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
((triple1) -> (rule4 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
((((triple1) -> (rule2 % int2)) triple1) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
((((triple1) -> (rule2 % int2))) -> (rule5 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
((triple1 ((((((triple1) -> (rule2 % int4)) triple1) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is furry.
("Anne" "is" "furry" "+")
int4
Anne is kind.
("Anne" "is" "kind" "+")
((((((triple1) -> (rule2 % int3)) triple1) -> (rule3 % int2))) -> (rule6 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3