Anne is rough. Harry is white. If Anne is white and Anne is not quiet then Anne is nice. All round things are white. All rough things are round.
Anne is rough.
("Anne" "is" "rough" "+")
Harry is white.
("Harry" "is" "white" "+")
If Anne is white and Anne is not quiet then Anne is nice.
((("Anne" "is" "white" "+") ("Anne" "is" "quiet" "~")) -> ("Anne" "is" "nice" "+"))
All round things are white.
((("something" "is" "round" "+")) -> ("something" "is" "white" "+"))
All rough things are round.
((("something" "is" "rough" "+")) -> ("something" "is" "round" "+"))
Harry is white.
True
1
proof
[(triple2)]
("Harry" "is" "white" "+")
triple2
Anne is not rough.
False
1
inv-proof
[(triple1)]
("Anne" "is" "rough" "-")
triple1
Anne is round.
True
2
proof
[(((triple1) -> rule3))]
("Anne" "is" "round" "+")
((triple1) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is not round.
False
2
inv-proof
[(((triple1) -> rule3))]
("Anne" "is" "round" "-")
((triple1) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is white.
True
3
proof
[(((((triple1) -> rule3)) -> rule2))]
("Anne" "is" "white" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is not white.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule2))]
("Anne" "is" "white" "-")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Harry is not round.
Unknown
inv-rconc
[@1: Harry is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "round" "-")
Anne is nice.
Unknown
rconc
[@1: Anne is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "nice" "+")
Anne is not quiet.
Unknown
inv-random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "-")
Harry is green.
Unknown
random
[@0: Harry is green.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "green" "+")
Harry is not nice.
Unknown
inv-random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "-")
Anne is big.
Unknown
random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "+")
@0: Anne is rough.[(triple1)] Harry is white.[(triple2)] @1: Anne is round.[(((triple1) -> rule3))] @2: Anne is white.[(((((triple1) -> rule3)) -> rule2))]
Anne is rough.
("Anne" "is" "rough" "+")
triple1
Harry is white.
("Harry" "is" "white" "+")
triple2
Anne is round.
("Anne" "is" "round" "+")
((triple1) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2