Anne is furry. If something is furry then it is young. All smart things are furry. Big things are round. White things are big. If Anne is furry then Anne is blue. If something is furry and blue then it is white.
Anne is furry.
("Anne" "is" "furry" "+")
If something is furry then it is young.
((("something" "is" "furry" "+")) -> ("something" "is" "young" "+"))
All smart things are furry.
((("something" "is" "smart" "+")) -> ("something" "is" "furry" "+"))
Big things are round.
((("something" "is" "big" "+")) -> ("something" "is" "round" "+"))
White things are big.
((("something" "is" "white" "+")) -> ("something" "is" "big" "+"))
If Anne is furry then Anne is blue.
((("Anne" "is" "furry" "+")) -> ("Anne" "is" "blue" "+"))
If something is furry and blue then it is white.
((("something" "is" "furry" "+") ("something" "is" "blue" "+")) -> ("something" "is" "white" "+"))
Anne is furry.
True
1
proof
[(triple1)]
("Anne" "is" "furry" "+")
triple1
Anne is not furry.
False
1
inv-proof
[(triple1)]
("Anne" "is" "furry" "-")
triple1
Anne is blue.
True
2
proof
[(((triple1) -> rule5))]
("Anne" "is" "blue" "+")
((triple1) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is not young.
False
2
inv-proof
[(((triple1) -> rule1))]
("Anne" "is" "young" "-")
((triple1) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is white.
True
4
proof
[(((triple1 ((triple1) -> rule5)) -> rule6))]
("Anne" "is" "white" "+")
((triple1 ((triple1) -> (rule5 % int2))) -> (rule6 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is not white.
False
4
inv-proof
[(((triple1 ((triple1) -> rule5)) -> rule6))]
("Anne" "is" "white" "-")
((triple1 ((triple1) -> (rule5 % int2))) -> (rule6 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is big.
True
5
proof
[(((((triple1 ((triple1) -> rule5)) -> rule6)) -> rule4))]
("Anne" "is" "big" "+")
((((triple1 ((triple1) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Anne is not big.
False
5
inv-proof
[(((((triple1 ((triple1) -> rule5)) -> rule6)) -> rule4))]
("Anne" "is" "big" "-")
((((triple1 ((triple1) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
@0: Anne is furry.[(triple1)] @1: Anne is blue.[(((triple1) -> rule5))] Anne is young.[(((triple1) -> rule1))] @2: Anne is white.[(((triple1 ((triple1) -> rule5)) -> rule6))] @3: Anne is big.[(((((triple1 ((triple1) -> rule5)) -> rule6)) -> rule4))] @4: Anne is round.[(((((((triple1 ((triple1) -> rule5)) -> rule6)) -> rule4)) -> rule3))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Anne is blue.
("Anne" "is" "blue" "+")
((triple1) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
((triple1) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
((triple1 ((triple1) -> (rule5 % int2))) -> (rule6 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
((((triple1 ((triple1) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Anne is round.
("Anne" "is" "round" "+")
((((((triple1 ((triple1) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Anne is blue.
("Anne" "is" "blue" "+")
int4