Anne is white. Fiona is quiet. If something is red and furry then it is quiet. If Anne is cold then Anne is furry. White things are cold. Cold, quiet things are big. If something is white and cold then it is quiet. If something is white then it is cold.
Anne is white.
("Anne" "is" "white" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
If something is red and furry then it is quiet.
((("something" "is" "red" "+") ("something" "is" "furry" "+")) -> ("something" "is" "quiet" "+"))
If Anne is cold then Anne is furry.
((("Anne" "is" "cold" "+")) -> ("Anne" "is" "furry" "+"))
White things are cold.
((("something" "is" "white" "+")) -> ("something" "is" "cold" "+"))
Cold, quiet things are big.
((("something" "is" "cold" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "big" "+"))
If something is white and cold then it is quiet.
((("something" "is" "white" "+") ("something" "is" "cold" "+")) -> ("something" "is" "quiet" "+"))
If something is white then it is cold.
((("something" "is" "white" "+")) -> ("something" "is" "cold" "+"))
Anne is white.
True
1
proof
[(triple1)]
("Anne" "is" "white" "+")
triple1
Anne is not white.
False
1
inv-proof
[(triple1)]
("Anne" "is" "white" "-")
triple1
Anne is cold.
True
2
proof
[(((triple1) -> rule3) OR ((triple1) -> rule6))]
("Anne" "is" "cold" "+")
((triple1) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
((triple1) -> (rule6 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is not cold.
False
2
inv-proof
[(((triple1) -> rule3) OR ((triple1) -> rule6))]
("Anne" "is" "cold" "-")
((triple1) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
((triple1) -> (rule6 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is furry.
True
3
proof
[(((((triple1) -> rule3)) -> rule2) OR ((((triple1) -> rule6)) -> rule2))]
("Anne" "is" "furry" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
((((triple1) -> (rule6 % int2))) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is not furry.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule2) OR ((((triple1) -> rule6)) -> rule2))]
("Anne" "is" "furry" "-")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
((((triple1) -> (rule6 % int2))) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is big.
True
7
proof
[(((((triple1) -> rule3) ((triple1 ((triple1) -> rule3)) -> rule5)) -> rule4) OR ((((triple1) -> rule3) ((triple1 ((triple1) -> rule6)) -> rule5)) -> rule4) OR ((((triple1) -> rule6) ((triple1 ((triple1) -> rule3)) -> rule5)) -> rule4) OR ((((triple1) -> rule6) ((triple1 ((triple1) -> rule6)) -> rule5)) -> rule4))]
("Anne" "is" "big" "+")
((((triple1) -> (rule3 % int3)) ((triple1 ((triple1) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
((((triple1) -> (rule3 % int3)) ((triple1 ((triple1) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
((((triple1) -> (rule6 % int3)) ((triple1 ((triple1) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
((((triple1) -> (rule6 % int3)) ((triple1 ((triple1) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is not big.
False
7
inv-proof
[(((((triple1) -> rule3) ((triple1 ((triple1) -> rule3)) -> rule5)) -> rule4) OR ((((triple1) -> rule3) ((triple1 ((triple1) -> rule6)) -> rule5)) -> rule4) OR ((((triple1) -> rule6) ((triple1 ((triple1) -> rule3)) -> rule5)) -> rule4) OR ((((triple1) -> rule6) ((triple1 ((triple1) -> rule6)) -> rule5)) -> rule4))]
("Anne" "is" "big" "-")
((((triple1) -> (rule3 % int3)) ((triple1 ((triple1) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
((((triple1) -> (rule3 % int3)) ((triple1 ((triple1) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
((((triple1) -> (rule6 % int3)) ((triple1 ((triple1) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
((((triple1) -> (rule6 % int3)) ((triple1 ((triple1) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Fiona is not cold.
Unknown
inv-rconc
[@1: Fiona is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "cold" "-")
Fiona is big.
Unknown
rconc
[@2: Fiona is big.[CWA. Example of deepest failure = (rule4 <- rule3 <- FAIL)]]
("Fiona" "is" "big" "+")
Fiona is not red.
Unknown
inv-random
[@0: Fiona is red.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "red" "-")
Anne is kind.
Unknown
random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "+")
Fiona is not furry.
Unknown
inv-random
[@0: Fiona is furry.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "furry" "-")
Anne is red.
Unknown
random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "+")
Fiona is not kind.
Unknown
inv-random
[@0: Fiona is kind.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "kind" "-")
Fiona is white.
Unknown
random
[@0: Fiona is white.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "white" "+")
@0: Anne is white.[(triple1)] Fiona is quiet.[(triple2)] @1: Anne is cold.[(((triple1) -> rule3) OR ((triple1) -> rule6))] @2: Anne is furry.[(((((triple1) -> rule3)) -> rule2) OR ((((triple1) -> rule6)) -> rule2))] Anne is quiet.[(((triple1 ((triple1) -> rule3)) -> rule5) OR ((triple1 ((triple1) -> rule6)) -> rule5))] @3: Anne is big.[(((((triple1) -> rule3) ((triple1 ((triple1) -> rule3)) -> rule5)) -> rule4) OR ((((triple1) -> rule3) ((triple1 ((triple1) -> rule6)) -> rule5)) -> rule4) OR ((((triple1) -> rule6) ((triple1 ((triple1) -> rule3)) -> rule5)) -> rule4) OR ((((triple1) -> rule6) ((triple1 ((triple1) -> rule6)) -> rule5)) -> rule4))]
Anne is white.
("Anne" "is" "white" "+")
triple1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple2
Anne is cold.
("Anne" "is" "cold" "+")
((triple1) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
((triple1) -> (rule6 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
((((triple1) -> (rule6 % int2))) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule5 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
((triple1 ((triple1) -> (rule6 % int2))) -> (rule5 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
((((triple1) -> (rule3 % int3)) ((triple1 ((triple1) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
((((triple1) -> (rule3 % int3)) ((triple1 ((triple1) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
((((triple1) -> (rule6 % int3)) ((triple1 ((triple1) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
((((triple1) -> (rule6 % int3)) ((triple1 ((triple1) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3