Anne is round. If Anne is furry then Anne is quiet. All round people are furry. If Anne is round then Anne is rough. All big, rough people are furry. If someone is quiet then they are rough. All young, big people are quiet. If Anne is rough then Anne is round. All big, quiet people are furry.
Anne is round.
("Anne" "is" "round" "+")
If Anne is furry then Anne is quiet.
((("Anne" "is" "furry" "+")) -> ("Anne" "is" "quiet" "+"))
All round people are furry.
((("someone" "is" "round" "+")) -> ("someone" "is" "furry" "+"))
If Anne is round then Anne is rough.
((("Anne" "is" "round" "+")) -> ("Anne" "is" "rough" "+"))
All big, rough people are furry.
((("someone" "is" "big" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "furry" "+"))
If someone is quiet then they are rough.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "rough" "+"))
All young, big people are quiet.
((("someone" "is" "young" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "quiet" "+"))
If Anne is rough then Anne is round.
((("Anne" "is" "rough" "+")) -> ("Anne" "is" "round" "+"))
All big, quiet people are furry.
((("someone" "is" "big" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "furry" "+"))
Anne is round.
True
1
proof
[(triple1)]
("Anne" "is" "round" "+")
triple1
Anne is not round.
False
1
inv-proof
[(triple1)]
("Anne" "is" "round" "-")
triple1
Anne is rough.
True
2
proof
[(((triple1) -> rule3) OR ((((((triple1) -> rule2)) -> rule1)) -> rule5))]
("Anne" "is" "rough" "+")
((triple1) -> (rule3 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
((((((triple1) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is not furry.
False
2
inv-proof
[(((triple1) -> rule2))]
("Anne" "is" "furry" "-")
((triple1) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is quiet.
True
3
proof
[(((((triple1) -> rule2)) -> rule1))]
("Anne" "is" "quiet" "+")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is not quiet.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule1))]
("Anne" "is" "quiet" "-")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2
Anne is not big.
Unknown
inv-random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "-")
Anne is kind.
Unknown
random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "+")
@0: Anne is round.[(triple1)] @1: Anne is furry.[(((triple1) -> rule2))] Anne is rough.[(((triple1) -> rule3) OR ((((((triple1) -> rule2)) -> rule1)) -> rule5))] @2: Anne is quiet.[(((((triple1) -> rule2)) -> rule1))]
Anne is round.
("Anne" "is" "round" "+")
triple1
Anne is furry.
("Anne" "is" "furry" "+")
((triple1) -> (rule2 % int1))
Anne is furry.
("Anne" "is" "furry" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
((triple1) -> (rule3 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
((((((triple1) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is furry.
("Anne" "is" "furry" "+")
int3
Anne is quiet.
("Anne" "is" "quiet" "+")
((((triple1) -> (rule2 % int2))) -> (rule1 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is furry.
("Anne" "is" "furry" "+")
int2