Anne is young. Dave is smart. If Anne is young then Anne is quiet. Round people are furry. If someone is quiet and not young then they are furry. Quiet people are round. If someone is quiet and young then they are rough. If someone is rough and not furry then they are white. Smart, round people are not white. If Anne is quiet and Anne is white then Anne is rough.
Anne is young.
("Anne" "is" "young" "+")
Dave is smart.
("Dave" "is" "smart" "+")
If Anne is young then Anne is quiet.
((("Anne" "is" "young" "+")) -> ("Anne" "is" "quiet" "+"))
Round people are furry.
((("someone" "is" "round" "+")) -> ("someone" "is" "furry" "+"))
If someone is quiet and not young then they are furry.
((("someone" "is" "quiet" "+") ("someone" "is" "young" "~")) -> ("someone" "is" "furry" "+"))
Quiet people are round.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "round" "+"))
If someone is quiet and young then they are rough.
((("someone" "is" "quiet" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "rough" "+"))
If someone is rough and not furry then they are white.
((("someone" "is" "rough" "+") ("someone" "is" "furry" "~")) -> ("someone" "is" "white" "+"))
Smart, round people are not white.
((("someone" "is" "smart" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "white" "-"))
If Anne is quiet and Anne is white then Anne is rough.
((("Anne" "is" "quiet" "+") ("Anne" "is" "white" "+")) -> ("Anne" "is" "rough" "+"))
Anne is young.
True
1
proof
[(triple1)]
("Anne" "is" "young" "+")
triple1
Anne is not young.
False
1
inv-proof
[(triple1)]
("Anne" "is" "young" "-")
triple1
Anne is quiet.
True
2
proof
[(((triple1) -> rule1))]
("Anne" "is" "quiet" "+")
((triple1) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is not quiet.
False
2
inv-proof
[(((triple1) -> rule1))]
("Anne" "is" "quiet" "-")
((triple1) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is rough.
True
4
proof
[(((((triple1) -> rule1) triple1) -> rule5))]
("Anne" "is" "rough" "+")
((((triple1) -> (rule1 % int2)) triple1) -> (rule5 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is not round.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule4))]
("Anne" "is" "round" "-")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is furry.
True
4
proof
[(((((((triple1) -> rule1)) -> rule4)) -> rule2))]
("Anne" "is" "furry" "+")
((((((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Anne is not furry.
False
4
inv-proof
[(((((((triple1) -> rule1)) -> rule4)) -> rule2))]
("Anne" "is" "furry" "-")
((((((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3
Dave is not white.
Unknown
inv-rconc
[@1: Dave is white.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Dave" "is" "white" "-")
Dave is furry.
Unknown
rconc
[@2: Dave is furry.[CWA. Example of deepest failure = (rule2 <- rule4 <- FAIL)]]
("Dave" "is" "furry" "+")
Dave is not round.
Unknown
inv-rconc
[@1: Dave is round.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "round" "-")
Dave is rough.
Unknown
rconc
[@1: Dave is rough.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Dave" "is" "rough" "+")
Dave is not young.
Unknown
inv-random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "-")
Anne is smart.
Unknown
random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "+")
@0: Anne is young.[(triple1)] Dave is smart.[(triple2)] @1: Anne is quiet.[(((triple1) -> rule1))] @2: Anne is rough.[(((((triple1) -> rule1) triple1) -> rule5))] Anne is round.[(((((triple1) -> rule1)) -> rule4))] @3: Anne is furry.[(((((((triple1) -> rule1)) -> rule4)) -> rule2))]
Anne is young.
("Anne" "is" "young" "+")
triple1
Dave is smart.
("Dave" "is" "smart" "+")
triple2
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple1) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
((((triple1) -> (rule1 % int2)) triple1) -> (rule5 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
((((triple1) -> (rule1 % int2))) -> (rule4 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
((((((triple1) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
int3