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