Charlie is quiet. All big people are nice. Quiet people are rough. If Charlie is quiet and Charlie is rough then Charlie is nice. Quiet, furry people are rough. Rough, big people are quiet. All blue people are cold.
Charlie is quiet.
("Charlie" "is" "quiet" "+")
All big people are nice.
((("someone" "is" "big" "+")) -> ("someone" "is" "nice" "+"))
Quiet people are rough.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "rough" "+"))
If Charlie is quiet and Charlie is rough then Charlie is nice.
((("Charlie" "is" "quiet" "+") ("Charlie" "is" "rough" "+")) -> ("Charlie" "is" "nice" "+"))
Quiet, furry people are rough.
((("someone" "is" "quiet" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "rough" "+"))
Rough, big people are quiet.
((("someone" "is" "rough" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "quiet" "+"))
All blue people are cold.
((("someone" "is" "blue" "+")) -> ("someone" "is" "cold" "+"))
Charlie is quiet.
True
1
proof
[(triple1)]
("Charlie" "is" "quiet" "+")
triple1
Charlie is not quiet.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "quiet" "-")
triple1
Charlie is rough.
True
2
proof
[(((triple1) -> rule2))]
("Charlie" "is" "rough" "+")
((triple1) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is not rough.
False
2
inv-proof
[(((triple1) -> rule2))]
("Charlie" "is" "rough" "-")
((triple1) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is not cold.
Unknown
inv-rconc
[@1: Charlie is cold.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "cold" "-")
Charlie is furry.
Unknown
random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "+")
Charlie is not blue.
Unknown
inv-random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "-")
Charlie is big.
Unknown
random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "+")
@0: Charlie is quiet.[(triple1)] @1: Charlie is rough.[(((triple1) -> rule2))] @2: Charlie is nice.[(((triple1 ((triple1) -> rule2)) -> rule3))]
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple1
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple1) -> (rule2 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2