Anne is rough. Anne is smart. Erin is big. If someone is white then they are not big. All white, quiet people are blue. If someone is smart and white then they are not blue. If Anne is smart then Anne is nice. If Erin is not rough then Erin is blue. If Erin is smart then Erin is not white. If someone is blue and nice then they are smart. Nice people are white.
Anne is rough.
("Anne" "is" "rough" "+")
Anne is smart.
("Anne" "is" "smart" "+")
Erin is big.
("Erin" "is" "big" "+")
If someone is white then they are not big.
((("someone" "is" "white" "+")) -> ("someone" "is" "big" "-"))
All white, quiet people are blue.
((("someone" "is" "white" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "blue" "+"))
If someone is smart and white then they are not blue.
((("someone" "is" "smart" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "blue" "-"))
If Anne is smart then Anne is nice.
((("Anne" "is" "smart" "+")) -> ("Anne" "is" "nice" "+"))
If Erin is not rough then Erin is blue.
((("Erin" "is" "rough" "~")) -> ("Erin" "is" "blue" "+"))
If Erin is smart then Erin is not white.
((("Erin" "is" "smart" "+")) -> ("Erin" "is" "white" "-"))
If someone is blue and nice then they are smart.
((("someone" "is" "blue" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "smart" "+"))
Nice people are white.
((("someone" "is" "nice" "+")) -> ("someone" "is" "white" "+"))
Anne is rough.
True
1
proof
[(triple1)]
("Anne" "is" "rough" "+")
triple1
Anne is not smart.
False
1
inv-proof
[(triple2)]
("Anne" "is" "smart" "-")
triple2
Anne is nice.
True
2
proof
[(((triple2) -> rule4))]
("Anne" "is" "nice" "+")
((triple2) -> (rule4 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is not nice.
False
2
inv-proof
[(((triple2) -> rule4))]
("Anne" "is" "nice" "-")
((triple2) -> (rule4 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is white.
True
3
proof
[(((((triple2) -> rule4)) -> rule8))]
("Anne" "is" "white" "+")
((((triple2) -> (rule4 % int2))) -> (rule8 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is not white.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule8))]
("Anne" "is" "white" "-")
((((triple2) -> (rule4 % int2))) -> (rule8 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is not blue.
True
5
proof
[(((triple2 ((((triple2) -> rule4)) -> rule8)) -> rule3))]
("Anne" "is" "blue" "-")
((triple2 ((((triple2) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
Anne is not blue.
("Anne" "is" "blue" "-")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is big.
False
4
inv-proof
[(((((((triple2) -> rule4)) -> rule8)) -> rule1))]
("Anne" "is" "big" "+")
((((((triple2) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
Anne is not big.
("Anne" "is" "big" "-")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Erin is not blue.
Unknown
inv-rconc
[@1: Erin is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "blue" "-")
Erin is white.
Unknown
rconc
[@1: Erin is white.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Erin" "is" "white" "+")
Erin is not smart.
Unknown
inv-rconc
[@1: Erin is smart.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Erin" "is" "smart" "-")
Erin is nice.
Unknown
random
[@0: Erin is nice.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "nice" "+")
Erin is not rough.
Unknown
inv-random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "-")
Anne is quiet.
Unknown
random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "+")
@0: Anne is rough.[(triple1)] Anne is smart.[(triple2)] Erin is big.[(triple3)] @1: Anne is nice.[(((triple2) -> rule4))] @2: Anne is white.[(((((triple2) -> rule4)) -> rule8))] @3: Anne is not big.[(((((((triple2) -> rule4)) -> rule8)) -> rule1))] Anne is not blue.[(((triple2 ((((triple2) -> rule4)) -> rule8)) -> rule3))]
Anne is rough.
("Anne" "is" "rough" "+")
triple1
Anne is smart.
("Anne" "is" "smart" "+")
triple2
Erin is big.
("Erin" "is" "big" "+")
triple3
Anne is nice.
("Anne" "is" "nice" "+")
((triple2) -> (rule4 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
((((triple2) -> (rule4 % int2))) -> (rule8 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is not big.
("Anne" "is" "big" "-")
((((((triple2) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
Anne is not big.
("Anne" "is" "big" "-")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3
Anne is not blue.
("Anne" "is" "blue" "-")
((triple2 ((((triple2) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
Anne is not blue.
("Anne" "is" "blue" "-")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
int3