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