Anne is white. All quiet people are young. Quiet people are not young. If someone is big then they are kind. If someone is white and not smart then they are kind. If Anne is smart and Anne is quiet then Anne is not big. All white people are big. If Anne is smart and Anne is white then Anne is not quiet. All white, kind people are green.
Anne is white.
("Anne" "is" "white" "+")
All quiet people are young.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "young" "+"))
Quiet people are not young.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "young" "-"))
If someone is big then they are kind.
((("someone" "is" "big" "+")) -> ("someone" "is" "kind" "+"))
If someone is white and not smart then they are kind.
((("someone" "is" "white" "+") ("someone" "is" "smart" "~")) -> ("someone" "is" "kind" "+"))
If Anne is smart and Anne is quiet then Anne is not big.
((("Anne" "is" "smart" "+") ("Anne" "is" "quiet" "+")) -> ("Anne" "is" "big" "-"))
All white people are big.
((("someone" "is" "white" "+")) -> ("someone" "is" "big" "+"))
If Anne is smart and Anne is white then Anne is not quiet.
((("Anne" "is" "smart" "+") ("Anne" "is" "white" "+")) -> ("Anne" "is" "quiet" "-"))
All white, kind people are green.
((("someone" "is" "white" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "green" "+"))
Anne is white.
True
1
proof
[(triple1)]
("Anne" "is" "white" "+")
triple1
Anne is not white.
False
1
inv-proof
[(triple1)]
("Anne" "is" "white" "-")
triple1
Anne is big.
True
2
proof
[(((triple1) -> rule6))]
("Anne" "is" "big" "+")
((triple1) -> (rule6 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is not big.
False
2
inv-proof
[(((triple1) -> rule6))]
("Anne" "is" "big" "-")
((triple1) -> (rule6 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is kind.
True
3
proof
[(((((triple1) -> rule6)) -> rule3))]
("Anne" "is" "kind" "+")
((((triple1) -> (rule6 % int2))) -> (rule3 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is not kind.
False
3
inv-proof
[(((((triple1) -> rule6)) -> rule3))]
("Anne" "is" "kind" "-")
((((triple1) -> (rule6 % int2))) -> (rule3 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is green.
True
5
proof
[(((triple1 ((((triple1) -> rule6)) -> rule3)) -> rule8))]
("Anne" "is" "green" "+")
((triple1 ((((triple1) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Anne is not green.
False
5
inv-proof
[(((triple1 ((((triple1) -> rule6)) -> rule3)) -> rule8))]
("Anne" "is" "green" "-")
((triple1 ((((triple1) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3
Anne is not young.
Unknown
inv-rconc
[@1: Anne is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "young" "-")
Anne is quiet.
Unknown
random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "+")
@0: Anne is white.[(triple1)] @1: Anne is big.[(((triple1) -> rule6))] @2: Anne is kind.[(((((triple1) -> rule6)) -> rule3))] @3: Anne is green.[(((triple1 ((((triple1) -> rule6)) -> rule3)) -> rule8))]
Anne is white.
("Anne" "is" "white" "+")
triple1
Anne is big.
("Anne" "is" "big" "+")
((triple1) -> (rule6 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
((((triple1) -> (rule6 % int2))) -> (rule3 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is green.
("Anne" "is" "green" "+")
((triple1 ((((triple1) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is big.
("Anne" "is" "big" "+")
int3