Anne is quiet. Charlie is not smart. If something is blue then it is cold. If Anne is quiet then Anne is kind. If something is kind and blue then it is big. If something is kind then it is not smart. If Anne is not smart then Anne is not rough. If Charlie is big and Charlie is not smart then Charlie is rough.
Anne is quiet.
("Anne" "is" "quiet" "+")
Charlie is not smart.
("Charlie" "is" "smart" "-")
If something is blue then it is cold.
((("something" "is" "blue" "+")) -> ("something" "is" "cold" "+"))
If Anne is quiet then Anne is kind.
((("Anne" "is" "quiet" "+")) -> ("Anne" "is" "kind" "+"))
If something is kind and blue then it is big.
((("something" "is" "kind" "+") ("something" "is" "blue" "+")) -> ("something" "is" "big" "+"))
If something is kind then it is not smart.
((("something" "is" "kind" "+")) -> ("something" "is" "smart" "-"))
If Anne is not smart then Anne is not rough.
((("Anne" "is" "smart" "~")) -> ("Anne" "is" "rough" "-"))
If Charlie is big and Charlie is not smart then Charlie is rough.
((("Charlie" "is" "big" "+") ("Charlie" "is" "smart" "~")) -> ("Charlie" "is" "rough" "+"))
Anne is quiet.
True
1
proof
[(triple1)]
("Anne" "is" "quiet" "+")
triple1
Anne is not quiet.
False
1
inv-proof
[(triple1)]
("Anne" "is" "quiet" "-")
triple1
Anne is kind.
True
2
proof
[(((triple1) -> rule2))]
("Anne" "is" "kind" "+")
((triple1) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is not kind.
False
2
inv-proof
[(((triple1) -> rule2))]
("Anne" "is" "kind" "-")
((triple1) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is not smart.
True
3
proof
[(((((triple1) -> rule2)) -> rule4))]
("Anne" "is" "smart" "-")
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Anne is not smart.
("Anne" "is" "smart" "-")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is smart.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule4))]
("Anne" "is" "smart" "+")
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Anne is not smart.
("Anne" "is" "smart" "-")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is not rough.
True
4
proof
[(((((((triple1) -> rule2)) -> rule4)) -> rule5))]
("Anne" "is" "rough" "-")
((((((triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Anne is not rough.
("Anne" "is" "rough" "-")
int1
Anne is not smart.
("Anne" "is" "smart" "-")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Anne is rough.
False
4
inv-proof
[(((((((triple1) -> rule2)) -> rule4)) -> rule5))]
("Anne" "is" "rough" "+")
((((((triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Anne is not rough.
("Anne" "is" "rough" "-")
int1
Anne is not smart.
("Anne" "is" "smart" "-")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3
Charlie is not big.
Unknown
inv-rconc
[@1: Charlie is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "big" "-")
Charlie is rough.
Unknown
rconc
[@1: Charlie is rough.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "rough" "+")
Anne is not cold.
Unknown
inv-rconc
[@1: Anne is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "cold" "-")
Charlie is cold.
Unknown
rconc
[@1: Charlie is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "cold" "+")
Anne is not blue.
Unknown
inv-random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "-")
Charlie is kind.
Unknown
random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "+")
Charlie is not blue.
Unknown
inv-random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "-")
Charlie is quiet.
Unknown
random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "+")
@0: Anne is quiet.[(triple1)] Charlie is not smart.[(triple2)] @1: Anne is kind.[(((triple1) -> rule2))] @2: Anne is not smart.[(((((triple1) -> rule2)) -> rule4))] @3: Anne is not rough.[(((((((triple1) -> rule2)) -> rule4)) -> rule5))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Charlie is not smart.
("Charlie" "is" "smart" "-")
triple2
Anne is kind.
("Anne" "is" "kind" "+")
((triple1) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is not smart.
("Anne" "is" "smart" "-")
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Anne is not smart.
("Anne" "is" "smart" "-")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is not rough.
("Anne" "is" "rough" "-")
((((((triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Anne is not rough.
("Anne" "is" "rough" "-")
int1
Anne is not smart.
("Anne" "is" "smart" "-")
int2
Anne is kind.
("Anne" "is" "kind" "+")
int3