Charlie is furry. If something is kind and not smart then it is not round. All kind, smart things are not round. If something is kind and not smart then it is not furry. All young things are furry. If Charlie is young and Charlie is rough then Charlie is not round. All furry, round things are kind. Cold things are not rough. If something is furry then it is cold.
Charlie is furry.
("Charlie" "is" "furry" "+")
If something is kind and not smart then it is not round.
((("something" "is" "kind" "+") ("something" "is" "smart" "~")) -> ("something" "is" "round" "-"))
All kind, smart things are not round.
((("something" "is" "kind" "+") ("something" "is" "smart" "+")) -> ("something" "is" "round" "-"))
If something is kind and not smart then it is not furry.
((("something" "is" "kind" "+") ("something" "is" "smart" "~")) -> ("something" "is" "furry" "-"))
All young things are furry.
((("something" "is" "young" "+")) -> ("something" "is" "furry" "+"))
If Charlie is young and Charlie is rough then Charlie is not round.
((("Charlie" "is" "young" "+") ("Charlie" "is" "rough" "+")) -> ("Charlie" "is" "round" "-"))
All furry, round things are kind.
((("something" "is" "furry" "+") ("something" "is" "round" "+")) -> ("something" "is" "kind" "+"))
Cold things are not rough.
((("something" "is" "cold" "+")) -> ("something" "is" "rough" "-"))
If something is furry then it is cold.
((("something" "is" "furry" "+")) -> ("something" "is" "cold" "+"))
Charlie is furry.
True
1
proof
[(triple1)]
("Charlie" "is" "furry" "+")
triple1
Charlie is not furry.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "furry" "-")
triple1
Charlie is cold.
True
2
proof
[(((triple1) -> rule8))]
("Charlie" "is" "cold" "+")
((triple1) -> (rule8 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is not cold.
False
2
inv-proof
[(((triple1) -> rule8))]
("Charlie" "is" "cold" "-")
((triple1) -> (rule8 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is not rough.
True
3
proof
[(((((triple1) -> rule8)) -> rule7))]
("Charlie" "is" "rough" "-")
((((triple1) -> (rule8 % int2))) -> (rule7 % int1))
Charlie is not rough.
("Charlie" "is" "rough" "-")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is rough.
False
3
inv-proof
[(((((triple1) -> rule8)) -> rule7))]
("Charlie" "is" "rough" "+")
((((triple1) -> (rule8 % int2))) -> (rule7 % int1))
Charlie is not rough.
("Charlie" "is" "rough" "-")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is not kind.
Unknown
inv-rconc
[@1: Charlie is kind.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "kind" "-")
Charlie is round.
Unknown
random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "+")
Charlie is not young.
Unknown
inv-random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "-")
Charlie is smart.
Unknown
random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "+")
@0: Charlie is furry.[(triple1)] @1: Charlie is cold.[(((triple1) -> rule8))] @2: Charlie is not rough.[(((((triple1) -> rule8)) -> rule7))]
Charlie is furry.
("Charlie" "is" "furry" "+")
triple1
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple1) -> (rule8 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is not rough.
("Charlie" "is" "rough" "-")
((((triple1) -> (rule8 % int2))) -> (rule7 % int1))
Charlie is not rough.
("Charlie" "is" "rough" "-")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2