Anne is blue. Anne is kind. Anne is not red. Anne is white. Anne is young. Erin is blue. Erin is cold. Erin is green. Erin is white. Gary is not cold. If something is red and not blue then it is kind. If something is white and young then it is kind. If something is kind then it is not red. If something is young and not cold then it is not red. If something is green and not blue then it is white. If something is red and not green then it is not white. If something is cold and not blue then it is white. Cold things are young.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is not red.
("Anne" "is" "red" "-")
Anne is white.
("Anne" "is" "white" "+")
Anne is young.
("Anne" "is" "young" "+")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is white.
("Erin" "is" "white" "+")
Gary is not cold.
("Gary" "is" "cold" "-")
If something is red and not blue then it is kind.
((("something" "is" "red" "+") ("something" "is" "blue" "~")) -> ("something" "is" "kind" "+"))
If something is white and young then it is kind.
((("something" "is" "white" "+") ("something" "is" "young" "+")) -> ("something" "is" "kind" "+"))
If something is kind then it is not red.
((("something" "is" "kind" "+")) -> ("something" "is" "red" "-"))
If something is young and not cold then it is not red.
((("something" "is" "young" "+") ("something" "is" "cold" "~")) -> ("something" "is" "red" "-"))
If something is green and not blue then it is white.
((("something" "is" "green" "+") ("something" "is" "blue" "~")) -> ("something" "is" "white" "+"))
If something is red and not green then it is not white.
((("something" "is" "red" "+") ("something" "is" "green" "~")) -> ("something" "is" "white" "-"))
If something is cold and not blue then it is white.
((("something" "is" "cold" "+") ("something" "is" "blue" "~")) -> ("something" "is" "white" "+"))
Cold things are young.
((("something" "is" "cold" "+")) -> ("something" "is" "young" "+"))
Anne is not red.
True
1
proof
[(triple3 OR ((triple2) -> rule3) OR ((((triple4 triple5) -> rule2)) -> rule3))]
("Anne" "is" "red" "-")
triple3
((triple2) -> (rule3 % int1))
Anne is not red.
("Anne" "is" "red" "-")
int1
((((triple4 triple5) -> (rule2 % int2))) -> (rule3 % int1))
Anne is not red.
("Anne" "is" "red" "-")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Erin is not green.
False
1
inv-proof
[(triple8)]
("Erin" "is" "green" "-")
triple8
Erin is young.
True
2
proof
[(((triple7) -> rule8))]
("Erin" "is" "young" "+")
((triple7) -> (rule8 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is not young.
False
2
inv-proof
[(((triple7) -> rule8))]
("Erin" "is" "young" "-")
((triple7) -> (rule8 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is kind.
True
4
proof
[(((triple9 ((triple7) -> rule8)) -> rule2))]
("Erin" "is" "kind" "+")
((triple9 ((triple7) -> (rule8 % int2))) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is not kind.
False
4
inv-proof
[(((triple9 ((triple7) -> rule8)) -> rule2))]
("Erin" "is" "kind" "-")
((triple9 ((triple7) -> (rule8 % int2))) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is not red.
True
5
proof
[(((((triple9 ((triple7) -> rule8)) -> rule2)) -> rule3))]
("Erin" "is" "red" "-")
((((triple9 ((triple7) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Erin is not red.
("Erin" "is" "red" "-")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is red.
False
5
inv-proof
[(((((triple9 ((triple7) -> rule8)) -> rule2)) -> rule3))]
("Erin" "is" "red" "+")
((((triple9 ((triple7) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Erin is not red.
("Erin" "is" "red" "-")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Gary is not young.
Unknown
inv-rconc
[@1: Gary is young.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Gary" "is" "young" "-")
Gary is white.
Unknown
rconc
[@1: Gary is white.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Gary" "is" "white" "+")
Gary is not kind.
Unknown
inv-rconc
[@2: Gary is kind.[CWA. Example of deepest failure = (rule2 <- rule5 <- FAIL)]]
("Gary" "is" "kind" "-")
Gary is red.
Unknown
random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "+")
Gary is not blue.
Unknown
inv-random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "-")
Gary is green.
Unknown
random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "+")
Anne is not cold.
Unknown
inv-random
[@0: Anne is cold.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "cold" "-")
Anne is green.
Unknown
random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "+")
@0: Anne is blue.[(triple1)] Anne is kind.[(triple2 OR ((triple4 triple5) -> rule2))] Anne is not red.[(triple3 OR ((triple2) -> rule3) OR ((((triple4 triple5) -> rule2)) -> rule3))] Anne is white.[(triple4)] Anne is young.[(triple5)] Erin is blue.[(triple6)] Erin is cold.[(triple7)] Erin is green.[(triple8)] Erin is white.[(triple9)] Gary is not cold.[(triple10)] @1: Erin is young.[(((triple7) -> rule8))] @2: Erin is kind.[(((triple9 ((triple7) -> rule8)) -> rule2))] @3: Erin is not red.[(((((triple9 ((triple7) -> rule8)) -> rule2)) -> rule3))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is kind.
("Anne" "is" "kind" "+")
triple2
((triple4 triple5) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is not red.
("Anne" "is" "red" "-")
triple3
((triple2) -> (rule3 % int1))
Anne is not red.
("Anne" "is" "red" "-")
int1
((((triple4 triple5) -> (rule2 % int2))) -> (rule3 % int1))
Anne is not red.
("Anne" "is" "red" "-")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
triple4
Anne is young.
("Anne" "is" "young" "+")
triple5
Erin is blue.
("Erin" "is" "blue" "+")
triple6
Erin is cold.
("Erin" "is" "cold" "+")
triple7
Erin is green.
("Erin" "is" "green" "+")
triple8
Erin is white.
("Erin" "is" "white" "+")
triple9
Gary is not cold.
("Gary" "is" "cold" "-")
triple10
Erin is young.
("Erin" "is" "young" "+")
((triple7) -> (rule8 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is kind.
("Erin" "is" "kind" "+")
((triple9 ((triple7) -> (rule8 % int2))) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is not red.
("Erin" "is" "red" "-")
((((triple9 ((triple7) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Erin is not red.
("Erin" "is" "red" "-")
int1
Erin is kind.
("Erin" "is" "kind" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3