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