Anne is cold. Charlie is furry. If someone is furry then they are rough. If someone is red and cold then they are rough. If Anne is not furry then Anne is round. If someone is rough then they are cold. If someone is quiet and not red then they are not cold. If Anne is red and Anne is cold then Anne is quiet. If someone is rough and not round then they are big. All cold people are not big.
Anne is cold.
("Anne" "is" "cold" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
If someone is furry then they are rough.
((("someone" "is" "furry" "+")) -> ("someone" "is" "rough" "+"))
If someone is red and cold then they are rough.
((("someone" "is" "red" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "rough" "+"))
If Anne is not furry then Anne is round.
((("Anne" "is" "furry" "~")) -> ("Anne" "is" "round" "+"))
If someone is rough then they are cold.
((("someone" "is" "rough" "+")) -> ("someone" "is" "cold" "+"))
If someone is quiet and not red then they are not cold.
((("someone" "is" "quiet" "+") ("someone" "is" "red" "~")) -> ("someone" "is" "cold" "-"))
If Anne is red and Anne is cold then Anne is quiet.
((("Anne" "is" "red" "+") ("Anne" "is" "cold" "+")) -> ("Anne" "is" "quiet" "+"))
If someone is rough and not round then they are big.
((("someone" "is" "rough" "+") ("someone" "is" "round" "~")) -> ("someone" "is" "big" "+"))
All cold people are not big.
((("someone" "is" "cold" "+")) -> ("someone" "is" "big" "-"))
Anne is cold.
True
1
proof
[(triple1)]
("Anne" "is" "cold" "+")
triple1
Anne is not cold.
False
1
inv-proof
[(triple1)]
("Anne" "is" "cold" "-")
triple1
Anne is not big.
True
2
proof
[(((triple1) -> rule8))]
("Anne" "is" "big" "-")
((triple1) -> (rule8 % int1))
Anne is not big.
("Anne" "is" "big" "-")
int1
Anne is big.
False
2
inv-proof
[(((triple1) -> rule8))]
("Anne" "is" "big" "+")
((triple1) -> (rule8 % int1))
Anne is not big.
("Anne" "is" "big" "-")
int1
Charlie is cold.
True
3
proof
[(((((triple2) -> rule1)) -> rule4))]
("Charlie" "is" "cold" "+")
((((triple2) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is not cold.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule4))]
("Charlie" "is" "cold" "-")
((((triple2) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is not big.
True
4
proof
[(((((((triple2) -> rule1)) -> rule4)) -> rule8))]
("Charlie" "is" "big" "-")
((((((triple2) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Charlie is not big.
("Charlie" "is" "big" "-")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is big.
False
4
inv-proof
[(((((((triple2) -> rule1)) -> rule4)) -> rule8))]
("Charlie" "is" "big" "+")
((((((triple2) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Charlie is not big.
("Charlie" "is" "big" "-")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Anne is not round.
Unknown
inv-rconc
[@1: Anne is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "round" "-")
Anne is quiet.
Unknown
rconc
[@1: Anne is quiet.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Anne" "is" "quiet" "+")
Anne is not rough.
Unknown
inv-rconc
[@1: Anne is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "rough" "-")
Anne is red.
Unknown
random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "+")
Charlie is not quiet.
Unknown
inv-random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "-")
Charlie is red.
Unknown
random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "+")
Anne is not furry.
Unknown
inv-random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "-")
Charlie is round.
Unknown
random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "+")
@0: Anne is cold.[(triple1)] Charlie is furry.[(triple2)] @1: Anne is not big.[(((triple1) -> rule8))] Charlie is rough.[(((triple2) -> rule1))] @2: Charlie is cold.[(((((triple2) -> rule1)) -> rule4))] @3: Charlie is not big.[(((((((triple2) -> rule1)) -> rule4)) -> rule8))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple2
Anne is not big.
("Anne" "is" "big" "-")
((triple1) -> (rule8 % int1))
Anne is not big.
("Anne" "is" "big" "-")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple2) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
((((triple2) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is not big.
("Charlie" "is" "big" "-")
((((((triple2) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Charlie is not big.
("Charlie" "is" "big" "-")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3