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