Anne is kind. All green, kind things are rough. All red, green things are not kind. If something is rough and big then it is red. All kind things are red. If Anne is red then Anne is big. If Anne is big then Anne is not cold. If something is smart then it is not cold. Green things are cold.
Anne is kind.
("Anne" "is" "kind" "+")
All green, kind things are rough.
((("something" "is" "green" "+") ("something" "is" "kind" "+")) -> ("something" "is" "rough" "+"))
All red, green things are not kind.
((("something" "is" "red" "+") ("something" "is" "green" "+")) -> ("something" "is" "kind" "-"))
If something is rough and big then it is red.
((("something" "is" "rough" "+") ("something" "is" "big" "+")) -> ("something" "is" "red" "+"))
All kind things are red.
((("something" "is" "kind" "+")) -> ("something" "is" "red" "+"))
If Anne is red then Anne is big.
((("Anne" "is" "red" "+")) -> ("Anne" "is" "big" "+"))
If Anne is big then Anne is not cold.
((("Anne" "is" "big" "+")) -> ("Anne" "is" "cold" "-"))
If something is smart then it is not cold.
((("something" "is" "smart" "+")) -> ("something" "is" "cold" "-"))
Green things are cold.
((("something" "is" "green" "+")) -> ("something" "is" "cold" "+"))
Anne is kind.
True
1
proof
[(triple1)]
("Anne" "is" "kind" "+")
triple1
Anne is not kind.
False
1
inv-proof
[(triple1)]
("Anne" "is" "kind" "-")
triple1
Anne is red.
True
2
proof
[(((triple1) -> rule4))]
("Anne" "is" "red" "+")
((triple1) -> (rule4 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is not red.
False
2
inv-proof
[(((triple1) -> rule4))]
("Anne" "is" "red" "-")
((triple1) -> (rule4 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is big.
True
3
proof
[(((((triple1) -> rule4)) -> rule5))]
("Anne" "is" "big" "+")
((((triple1) -> (rule4 % int2))) -> (rule5 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is not big.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule5))]
("Anne" "is" "big" "-")
((((triple1) -> (rule4 % int2))) -> (rule5 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is not cold.
True
4
proof
[(((((((triple1) -> rule4)) -> rule5)) -> rule6))]
("Anne" "is" "cold" "-")
((((((triple1) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Anne is not cold.
("Anne" "is" "cold" "-")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is cold.
False
4
inv-proof
[(((((((triple1) -> rule4)) -> rule5)) -> rule6))]
("Anne" "is" "cold" "+")
((((((triple1) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Anne is not cold.
("Anne" "is" "cold" "-")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Anne is not rough.
Unknown
inv-rconc
[@1: Anne is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "rough" "-")
Anne is smart.
Unknown
random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "+")
@0: Anne is kind.[(triple1)] @1: Anne is red.[(((triple1) -> rule4))] @2: Anne is big.[(((((triple1) -> rule4)) -> rule5))] @3: Anne is not cold.[(((((((triple1) -> rule4)) -> rule5)) -> rule6))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Anne is red.
("Anne" "is" "red" "+")
((triple1) -> (rule4 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
((((triple1) -> (rule4 % int2))) -> (rule5 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is not cold.
("Anne" "is" "cold" "-")
((((((triple1) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Anne is not cold.
("Anne" "is" "cold" "-")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3