Charlie is rough. If someone is round then they are kind. If Charlie is rough then Charlie is kind. Nice people are quiet. If someone is kind then they are furry. If someone is quiet and not nice then they are furry. If someone is quiet and not kind then they are not furry. Kind, furry people are not cold. Rough, nice people are cold.
Charlie is rough.
("Charlie" "is" "rough" "+")
If someone is round then they are kind.
((("someone" "is" "round" "+")) -> ("someone" "is" "kind" "+"))
If Charlie is rough then Charlie is kind.
((("Charlie" "is" "rough" "+")) -> ("Charlie" "is" "kind" "+"))
Nice people are quiet.
((("someone" "is" "nice" "+")) -> ("someone" "is" "quiet" "+"))
If someone is kind then they are furry.
((("someone" "is" "kind" "+")) -> ("someone" "is" "furry" "+"))
If someone is quiet and not nice then they are furry.
((("someone" "is" "quiet" "+") ("someone" "is" "nice" "~")) -> ("someone" "is" "furry" "+"))
If someone is quiet and not kind then they are not furry.
((("someone" "is" "quiet" "+") ("someone" "is" "kind" "~")) -> ("someone" "is" "furry" "-"))
Kind, furry people are not cold.
((("someone" "is" "kind" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "cold" "-"))
Rough, nice people are cold.
((("someone" "is" "rough" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "cold" "+"))
Charlie is rough.
True
1
proof
[(triple1)]
("Charlie" "is" "rough" "+")
triple1
Charlie is not rough.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "rough" "-")
triple1
Charlie is kind.
True
2
proof
[(((triple1) -> rule2))]
("Charlie" "is" "kind" "+")
((triple1) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is not kind.
False
2
inv-proof
[(((triple1) -> rule2))]
("Charlie" "is" "kind" "-")
((triple1) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is furry.
True
3
proof
[(((((triple1) -> rule2)) -> rule4))]
("Charlie" "is" "furry" "+")
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is not furry.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule4))]
("Charlie" "is" "furry" "-")
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is not cold.
True
6
proof
[(((((triple1) -> rule2) ((((triple1) -> rule2)) -> rule4)) -> rule7))]
("Charlie" "is" "cold" "-")
((((triple1) -> (rule2 % int3)) ((((triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Charlie is not cold.
("Charlie" "is" "cold" "-")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is cold.
False
6
inv-proof
[(((((triple1) -> rule2) ((((triple1) -> rule2)) -> rule4)) -> rule7))]
("Charlie" "is" "cold" "+")
((((triple1) -> (rule2 % int3)) ((((triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Charlie is not cold.
("Charlie" "is" "cold" "-")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3
Charlie is not quiet.
Unknown
inv-rconc
[@1: Charlie is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "quiet" "-")
Charlie is nice.
Unknown
random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "+")
@0: Charlie is rough.[(triple1)] @1: Charlie is kind.[(((triple1) -> rule2))] @2: Charlie is furry.[(((((triple1) -> rule2)) -> rule4))] @3: Charlie is not cold.[(((((triple1) -> rule2) ((((triple1) -> rule2)) -> rule4)) -> rule7))]
Charlie is rough.
("Charlie" "is" "rough" "+")
triple1
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple1) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is not cold.
("Charlie" "is" "cold" "-")
((((triple1) -> (rule2 % int3)) ((((triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Charlie is not cold.
("Charlie" "is" "cold" "-")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
int3