Charlie is blue. Dave is not furry. All young, rough things are not quiet. If something is blue then it is furry. Blue, furry things are rough.
Charlie is blue.
("Charlie" "is" "blue" "+")
Dave is not furry.
("Dave" "is" "furry" "-")
All young, rough things are not quiet.
((("something" "is" "young" "+") ("something" "is" "rough" "+")) -> ("something" "is" "quiet" "-"))
If something is blue then it is furry.
((("something" "is" "blue" "+")) -> ("something" "is" "furry" "+"))
Blue, furry things are rough.
((("something" "is" "blue" "+") ("something" "is" "furry" "+")) -> ("something" "is" "rough" "+"))
Charlie is blue.
True
1
proof
[(triple1)]
("Charlie" "is" "blue" "+")
triple1
Charlie is not blue.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "blue" "-")
triple1
Charlie is furry.
True
2
proof
[(((triple1) -> rule2))]
("Charlie" "is" "furry" "+")
((triple1) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is not furry.
False
2
inv-proof
[(((triple1) -> rule2))]
("Charlie" "is" "furry" "-")
((triple1) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is rough.
True
4
proof
[(((triple1 ((triple1) -> rule2)) -> rule3))]
("Charlie" "is" "rough" "+")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Charlie is not rough.
False
4
inv-proof
[(((triple1 ((triple1) -> rule2)) -> rule3))]
("Charlie" "is" "rough" "-")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2
Dave is not rough.
Unknown
inv-rconc
[@1: Dave is rough.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "rough" "-")
Charlie is white.
Unknown
random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "+")
Charlie is not young.
Unknown
inv-random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "-")
Dave is smart.
Unknown
random
[@0: Dave is smart.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "smart" "+")
Charlie is not quiet.
Unknown
inv-random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "-")
Dave is young.
Unknown
random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "+")
@0: Charlie is blue.[(triple1)] Dave is not furry.[(triple2)] @1: Charlie is furry.[(((triple1) -> rule2))] @2: Charlie is rough.[(((triple1 ((triple1) -> rule2)) -> rule3))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Dave is not furry.
("Dave" "is" "furry" "-")
triple2
Charlie is furry.
("Charlie" "is" "furry" "+")
((triple1) -> (rule2 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
int2