Anne is furry. Charlie is young. Dave is blue. Harry is young. Rough, blue people are young. All furry people are rough. If someone is rough then they are smart.
Anne is furry.
("Anne" "is" "furry" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Harry is young.
("Harry" "is" "young" "+")
Rough, blue people are young.
((("someone" "is" "rough" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "young" "+"))
All furry people are rough.
((("someone" "is" "furry" "+")) -> ("someone" "is" "rough" "+"))
If someone is rough then they are smart.
((("someone" "is" "rough" "+")) -> ("someone" "is" "smart" "+"))
Anne is furry.
True
1
proof
[(triple1)]
("Anne" "is" "furry" "+")
triple1
Dave is not blue.
False
1
inv-proof
[(triple3)]
("Dave" "is" "blue" "-")
triple3
Anne is rough.
True
2
proof
[(((triple1) -> rule2))]
("Anne" "is" "rough" "+")
((triple1) -> (rule2 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is not rough.
False
2
inv-proof
[(((triple1) -> rule2))]
("Anne" "is" "rough" "-")
((triple1) -> (rule2 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is smart.
True
3
proof
[(((((triple1) -> rule2)) -> rule3))]
("Anne" "is" "smart" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is not smart.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule3))]
("Anne" "is" "smart" "-")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Dave is not rough.
Unknown
inv-rconc
[@1: Dave is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "rough" "-")
Dave is smart.
Unknown
rconc
[@2: Dave is smart.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("Dave" "is" "smart" "+")
Harry is not rough.
Unknown
inv-rconc
[@1: Harry is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "rough" "-")
Harry is furry.
Unknown
random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "+")
Harry is not quiet.
Unknown
inv-random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "-")
Charlie is red.
Unknown
random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "+")
@0: Anne is furry.[(triple1)] Charlie is young.[(triple2)] Dave is blue.[(triple3)] Harry is young.[(triple4)] @1: Anne is rough.[(((triple1) -> rule2))] @2: Anne is smart.[(((((triple1) -> rule2)) -> rule3))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Charlie is young.
("Charlie" "is" "young" "+")
triple2
Dave is blue.
("Dave" "is" "blue" "+")
triple3
Harry is young.
("Harry" "is" "young" "+")
triple4
Anne is rough.
("Anne" "is" "rough" "+")
((triple1) -> (rule2 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
((((triple1) -> (rule2 % int2))) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2