Charlie is cold. Rough, white things are not big. Cold things are big. If something is white then it is red. If something is furry and big then it is not green. Red, rough things are not green. If Charlie is big then Charlie is not furry.
Charlie is cold.
("Charlie" "is" "cold" "+")
Rough, white things are not big.
((("something" "is" "rough" "+") ("something" "is" "white" "+")) -> ("something" "is" "big" "-"))
Cold things are big.
((("something" "is" "cold" "+")) -> ("something" "is" "big" "+"))
If something is white then it is red.
((("something" "is" "white" "+")) -> ("something" "is" "red" "+"))
If something is furry and big then it is not green.
((("something" "is" "furry" "+") ("something" "is" "big" "+")) -> ("something" "is" "green" "-"))
Red, rough things are not green.
((("something" "is" "red" "+") ("something" "is" "rough" "+")) -> ("something" "is" "green" "-"))
If Charlie is big then Charlie is not furry.
((("Charlie" "is" "big" "+")) -> ("Charlie" "is" "furry" "-"))
Charlie is cold.
True
1
proof
[(triple1)]
("Charlie" "is" "cold" "+")
triple1
Charlie is not cold.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "cold" "-")
triple1
Charlie is big.
True
2
proof
[(((triple1) -> rule2))]
("Charlie" "is" "big" "+")
((triple1) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is not big.
False
2
inv-proof
[(((triple1) -> rule2))]
("Charlie" "is" "big" "-")
((triple1) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is not furry.
True
3
proof
[(((((triple1) -> rule2)) -> rule6))]
("Charlie" "is" "furry" "-")
((((triple1) -> (rule2 % int2))) -> (rule6 % int1))
Charlie is not furry.
("Charlie" "is" "furry" "-")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is furry.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule6))]
("Charlie" "is" "furry" "+")
((((triple1) -> (rule2 % int2))) -> (rule6 % int1))
Charlie is not furry.
("Charlie" "is" "furry" "-")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is not red.
Unknown
inv-rconc
[@1: Charlie is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "red" "-")
Charlie is green.
Unknown
random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "+")
Charlie is not rough.
Unknown
inv-random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "-")
Charlie is white.
Unknown
random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "+")
@0: Charlie is cold.[(triple1)] @1: Charlie is big.[(((triple1) -> rule2))] @2: Charlie is not furry.[(((((triple1) -> rule2)) -> rule6))]
Charlie is cold.
("Charlie" "is" "cold" "+")
triple1
Charlie is big.
("Charlie" "is" "big" "+")
((triple1) -> (rule2 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is not furry.
("Charlie" "is" "furry" "-")
((((triple1) -> (rule2 % int2))) -> (rule6 % int1))
Charlie is not furry.
("Charlie" "is" "furry" "-")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2