Anne is smart. If someone is smart and not rough then they are blue. If Anne is not quiet and Anne is not rough then Anne is red. If Anne is blue then Anne is smart. Blue people are not red. If Anne is green and Anne is smart then Anne is white. All smart people are green. If someone is smart and not blue then they are not white. All rough people are white.
Anne is smart.
("Anne" "is" "smart" "+")
If someone is smart and not rough then they are blue.
((("someone" "is" "smart" "+") ("someone" "is" "rough" "~")) -> ("someone" "is" "blue" "+"))
If Anne is not quiet and Anne is not rough then Anne is red.
((("Anne" "is" "quiet" "~") ("Anne" "is" "rough" "~")) -> ("Anne" "is" "red" "+"))
If Anne is blue then Anne is smart.
((("Anne" "is" "blue" "+")) -> ("Anne" "is" "smart" "+"))
Blue people are not red.
((("someone" "is" "blue" "+")) -> ("someone" "is" "red" "-"))
If Anne is green and Anne is smart then Anne is white.
((("Anne" "is" "green" "+") ("Anne" "is" "smart" "+")) -> ("Anne" "is" "white" "+"))
All smart people are green.
((("someone" "is" "smart" "+")) -> ("someone" "is" "green" "+"))
If someone is smart and not blue then they are not white.
((("someone" "is" "smart" "+") ("someone" "is" "blue" "~")) -> ("someone" "is" "white" "-"))
All rough people are white.
((("someone" "is" "rough" "+")) -> ("someone" "is" "white" "+"))
Anne is smart.
True
1
proof
[(triple1)]
("Anne" "is" "smart" "+")
triple1
Anne is not smart.
False
1
inv-proof
[(triple1)]
("Anne" "is" "smart" "-")
triple1
Anne is green.
True
2
proof
[(((triple1) -> rule6))]
("Anne" "is" "green" "+")
((triple1) -> (rule6 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is not green.
False
2
inv-proof
[(((triple1) -> rule6))]
("Anne" "is" "green" "-")
((triple1) -> (rule6 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is white.
True
4
proof
[(((((triple1) -> rule6) triple1) -> rule5))]
("Anne" "is" "white" "+")
((((triple1) -> (rule6 % int2)) triple1) -> (rule5 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is not white.
False
4
inv-proof
[(((((triple1) -> rule6) triple1) -> rule5))]
("Anne" "is" "white" "-")
((((triple1) -> (rule6 % int2)) triple1) -> (rule5 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is not blue.
Unknown
inv-rconc
[@1: Anne is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "blue" "-")
Anne is red.
Unknown
rconc
[@1: Anne is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "red" "+")
Anne is not quiet.
Unknown
inv-random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "-")
Anne is rough.
Unknown
random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "+")
@0: Anne is smart.[(triple1)] @1: Anne is green.[(((triple1) -> rule6))] @2: Anne is white.[(((((triple1) -> rule6) triple1) -> rule5))]
Anne is smart.
("Anne" "is" "smart" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
((triple1) -> (rule6 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
((((triple1) -> (rule6 % int2)) triple1) -> (rule5 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2