Anne is quiet. Anne is smart. Anne is young. Kind people are furry. If someone is round and quiet then they are kind. Smart people are round.
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Anne is young.
("Anne" "is" "young" "+")
Kind people are furry.
((("someone" "is" "kind" "+")) -> ("someone" "is" "furry" "+"))
If someone is round and quiet then they are kind.
((("someone" "is" "round" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "kind" "+"))
Smart people are round.
((("someone" "is" "smart" "+")) -> ("someone" "is" "round" "+"))
Anne is quiet.
True
1
proof
[(triple1)]
("Anne" "is" "quiet" "+")
triple1
Anne is not smart.
False
1
inv-proof
[(triple2)]
("Anne" "is" "smart" "-")
triple2
Anne is round.
True
2
proof
[(((triple2) -> rule3))]
("Anne" "is" "round" "+")
((triple2) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is not round.
False
2
inv-proof
[(((triple2) -> rule3))]
("Anne" "is" "round" "-")
((triple2) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is kind.
True
4
proof
[(((((triple2) -> rule3) triple1) -> rule2))]
("Anne" "is" "kind" "+")
((((triple2) -> (rule3 % int2)) triple1) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is not kind.
False
4
inv-proof
[(((((triple2) -> rule3) triple1) -> rule2))]
("Anne" "is" "kind" "-")
((((triple2) -> (rule3 % int2)) triple1) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is furry.
True
5
proof
[(((((((triple2) -> rule3) triple1) -> rule2)) -> rule1))]
("Anne" "is" "furry" "+")
((((((triple2) -> (rule3 % int3)) triple1) -> (rule2 % int2))) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Anne is not furry.
False
5
inv-proof
[(((((((triple2) -> rule3) triple1) -> rule2)) -> rule1))]
("Anne" "is" "furry" "-")
((((((triple2) -> (rule3 % int3)) triple1) -> (rule2 % int2))) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
@0: Anne is quiet.[(triple1)] Anne is smart.[(triple2)] Anne is young.[(triple3)] @1: Anne is round.[(((triple2) -> rule3))] @2: Anne is kind.[(((((triple2) -> rule3) triple1) -> rule2))] @3: Anne is furry.[(((((((triple2) -> rule3) triple1) -> rule2)) -> rule1))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Anne is smart.
("Anne" "is" "smart" "+")
triple2
Anne is young.
("Anne" "is" "young" "+")
triple3
Anne is round.
("Anne" "is" "round" "+")
((triple2) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
((((triple2) -> (rule3 % int2)) triple1) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
((((((triple2) -> (rule3 % int3)) triple1) -> (rule2 % int2))) -> (rule1 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3