Anne is rough. Anne is round. Erin is big. Smart things are white. White things are kind. If Anne is round then Anne is smart. All white things are not big. Kind, rough things are smart. If Anne is not rough and Anne is not white then Anne is not young.
Anne is rough.
("Anne" "is" "rough" "+")
Anne is round.
("Anne" "is" "round" "+")
Erin is big.
("Erin" "is" "big" "+")
Smart things are white.
((("something" "is" "smart" "+")) -> ("something" "is" "white" "+"))
White things are kind.
((("something" "is" "white" "+")) -> ("something" "is" "kind" "+"))
If Anne is round then Anne is smart.
((("Anne" "is" "round" "+")) -> ("Anne" "is" "smart" "+"))
All white things are not big.
((("something" "is" "white" "+")) -> ("something" "is" "big" "-"))
Kind, rough things are smart.
((("something" "is" "kind" "+") ("something" "is" "rough" "+")) -> ("something" "is" "smart" "+"))
If Anne is not rough and Anne is not white then Anne is not young.
((("Anne" "is" "rough" "~") ("Anne" "is" "white" "~")) -> ("Anne" "is" "young" "-"))
Anne is rough.
True
1
proof
[(triple1)]
("Anne" "is" "rough" "+")
triple1
Erin is not big.
False
1
inv-proof
[(triple3)]
("Erin" "is" "big" "-")
triple3
Anne is smart.
True
2
proof
[(((triple2) -> rule3))]
("Anne" "is" "smart" "+")
((triple2) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is not smart.
False
2
inv-proof
[(((triple2) -> rule3))]
("Anne" "is" "smart" "-")
((triple2) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is white.
True
3
proof
[(((((triple2) -> rule3)) -> rule1))]
("Anne" "is" "white" "+")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is not white.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule1))]
("Anne" "is" "white" "-")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is kind.
True
4
proof
[(((((((triple2) -> rule3)) -> rule1)) -> rule2))]
("Anne" "is" "kind" "+")
((((((triple2) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is big.
False
4
inv-proof
[(((((((triple2) -> rule3)) -> rule1)) -> rule4))]
("Anne" "is" "big" "+")
((((((triple2) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Anne is not big.
("Anne" "is" "big" "-")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Erin is not smart.
Unknown
inv-rconc
[@1: Erin is smart.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Erin" "is" "smart" "-")
Erin is kind.
Unknown
rconc
[@3: Erin is kind.[CWA. Example of deepest failure = (rule2 <- rule1 <- rule5 <- FAIL)]]
("Erin" "is" "kind" "+")
Erin is not white.
Unknown
inv-rconc
[@2: Erin is white.[CWA. Example of deepest failure = (rule1 <- rule5 <- FAIL)]]
("Erin" "is" "white" "-")
Erin is rough.
Unknown
random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "+")
Erin is not round.
Unknown
inv-random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "-")
Erin is young.
Unknown
random
[@0: Erin is young.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "young" "+")
@0: Anne is rough.[(triple1)] Anne is round.[(triple2)] Erin is big.[(triple3)] @1: Anne is smart.[(((triple2) -> rule3))] @2: Anne is white.[(((((triple2) -> rule3)) -> rule1))] @3: Anne is kind.[(((((((triple2) -> rule3)) -> rule1)) -> rule2))] Anne is not big.[(((((((triple2) -> rule3)) -> rule1)) -> rule4))]
Anne is rough.
("Anne" "is" "rough" "+")
triple1
Anne is round.
("Anne" "is" "round" "+")
triple2
Erin is big.
("Erin" "is" "big" "+")
triple3
Anne is smart.
("Anne" "is" "smart" "+")
((triple2) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is kind.
("Anne" "is" "kind" "+")
((((((triple2) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is not big.
("Anne" "is" "big" "-")
((((((triple2) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Anne is not big.
("Anne" "is" "big" "-")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3