Anne is big. If Anne is young then Anne is kind. If something is furry then it is nice. Big things are furry. If something is nice then it is furry. Nice things are blue. If something is furry and not nice then it is not kind.
Anne is big.
("Anne" "is" "big" "+")
If Anne is young then Anne is kind.
((("Anne" "is" "young" "+")) -> ("Anne" "is" "kind" "+"))
If something is furry then it is nice.
((("something" "is" "furry" "+")) -> ("something" "is" "nice" "+"))
Big things are furry.
((("something" "is" "big" "+")) -> ("something" "is" "furry" "+"))
If something is nice then it is furry.
((("something" "is" "nice" "+")) -> ("something" "is" "furry" "+"))
Nice things are blue.
((("something" "is" "nice" "+")) -> ("something" "is" "blue" "+"))
If something is furry and not nice then it is not kind.
((("something" "is" "furry" "+") ("something" "is" "nice" "~")) -> ("something" "is" "kind" "-"))
Anne is big.
True
1
proof
[(triple1)]
("Anne" "is" "big" "+")
triple1
Anne is not big.
False
1
inv-proof
[(triple1)]
("Anne" "is" "big" "-")
triple1
Anne is furry.
True
2
proof
[(((triple1) -> rule3))]
("Anne" "is" "furry" "+")
((triple1) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is not furry.
False
2
inv-proof
[(((triple1) -> rule3))]
("Anne" "is" "furry" "-")
((triple1) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is nice.
True
3
proof
[(((((triple1) -> rule3)) -> rule2))]
("Anne" "is" "nice" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is not nice.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule2))]
("Anne" "is" "nice" "-")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is blue.
True
4
proof
[(((((((triple1) -> rule3)) -> rule2)) -> rule5))]
("Anne" "is" "blue" "+")
((((((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is not blue.
False
4
inv-proof
[(((((((triple1) -> rule3)) -> rule2)) -> rule5))]
("Anne" "is" "blue" "-")
((((((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is not kind.
Unknown
inv-rconc
[@1: Anne is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "kind" "-")
Anne is smart.
Unknown
random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "+")
@0: Anne is big.[(triple1)] @1: Anne is furry.[(((triple1) -> rule3))] @2: Anne is nice.[(((((triple1) -> rule3)) -> rule2))] @3: Anne is blue.[(((((((triple1) -> rule3)) -> rule2)) -> rule5))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is furry.
("Anne" "is" "furry" "+")
((triple1) -> (rule3 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
((((((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3