Anne is blue. Anne is cold. Anne is green. Anne is rough. Dave is not blue. Erin is cold. Erin is white. If Anne is green and Anne is blue then Anne is not white. If someone is blue and not white then they are kind.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is cold.
("Anne" "is" "cold" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Dave is not blue.
("Dave" "is" "blue" "-")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is white.
("Erin" "is" "white" "+")
If Anne is green and Anne is blue then Anne is not white.
((("Anne" "is" "green" "+") ("Anne" "is" "blue" "+")) -> ("Anne" "is" "white" "-"))
If someone is blue and not white then they are kind.
((("someone" "is" "blue" "+") ("someone" "is" "white" "~")) -> ("someone" "is" "kind" "+"))
Anne is blue.
True
1
proof
[(triple1)]
("Anne" "is" "blue" "+")
triple1
Anne is not green.
False
1
inv-proof
[(triple3)]
("Anne" "is" "green" "-")
triple3
Anne is not white.
True
3
proof
[(((triple3 triple1) -> rule1))]
("Anne" "is" "white" "-")
((triple3 triple1) -> (rule1 % int1))
Anne is not white.
("Anne" "is" "white" "-")
int1
Anne is white.
False
3
inv-proof
[(((triple3 triple1) -> rule1))]
("Anne" "is" "white" "+")
((triple3 triple1) -> (rule1 % int1))
Anne is not white.
("Anne" "is" "white" "-")
int1
Anne is kind.
True
5
proof
[(((triple1 ((triple3 triple1) -> rule1)) -> rule2))]
("Anne" "is" "kind" "+")
((triple1 ((triple3 triple1) -> (rule1 % int2))) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is not white.
("Anne" "is" "white" "-")
int2
Anne is not kind.
False
5
inv-proof
[(((triple1 ((triple3 triple1) -> rule1)) -> rule2))]
("Anne" "is" "kind" "-")
((triple1 ((triple3 triple1) -> (rule1 % int2))) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is not white.
("Anne" "is" "white" "-")
int2
Erin is not kind.
Unknown
inv-rconc
[@1: Erin is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "kind" "-")
Dave is kind.
Unknown
rconc
[@1: Dave is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "kind" "+")
Anne is not smart.
Unknown
inv-random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "-")
Erin is rough.
Unknown
random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "+")
Dave is not white.
Unknown
inv-random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "-")
Dave is cold.
Unknown
random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "+")
@0: Anne is blue.[(triple1)] Anne is cold.[(triple2)] Anne is green.[(triple3)] Anne is rough.[(triple4)] Dave is not blue.[(triple5)] Erin is cold.[(triple6)] Erin is white.[(triple7)] @1: Anne is not white.[(((triple3 triple1) -> rule1))] @2: Anne is kind.[(((triple1 ((triple3 triple1) -> rule1)) -> rule2))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is cold.
("Anne" "is" "cold" "+")
triple2
Anne is green.
("Anne" "is" "green" "+")
triple3
Anne is rough.
("Anne" "is" "rough" "+")
triple4
Dave is not blue.
("Dave" "is" "blue" "-")
triple5
Erin is cold.
("Erin" "is" "cold" "+")
triple6
Erin is white.
("Erin" "is" "white" "+")
triple7
Anne is not white.
("Anne" "is" "white" "-")
((triple3 triple1) -> (rule1 % int1))
Anne is not white.
("Anne" "is" "white" "-")
int1
Anne is kind.
("Anne" "is" "kind" "+")
((triple1 ((triple3 triple1) -> (rule1 % int2))) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is not white.
("Anne" "is" "white" "-")
int2