Anne is blue. Charlie is white. Erin is kind. Gary is round. If Anne is round then Anne is cold. If Gary is rough and Gary is round then Gary is not white. If Erin is round then Erin is not kind. All kind things are blue. Cold, round things are rough. If something is cold then it is not rough. All blue, kind things are cold. If something is rough then it is white.
Anne is blue.
("Anne" "is" "blue" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Gary is round.
("Gary" "is" "round" "+")
If Anne is round then Anne is cold.
((("Anne" "is" "round" "+")) -> ("Anne" "is" "cold" "+"))
If Gary is rough and Gary is round then Gary is not white.
((("Gary" "is" "rough" "+") ("Gary" "is" "round" "+")) -> ("Gary" "is" "white" "-"))
If Erin is round then Erin is not kind.
((("Erin" "is" "round" "+")) -> ("Erin" "is" "kind" "-"))
All kind things are blue.
((("something" "is" "kind" "+")) -> ("something" "is" "blue" "+"))
Cold, round things are rough.
((("something" "is" "cold" "+") ("something" "is" "round" "+")) -> ("something" "is" "rough" "+"))
If something is cold then it is not rough.
((("something" "is" "cold" "+")) -> ("something" "is" "rough" "-"))
All blue, kind things are cold.
((("something" "is" "blue" "+") ("something" "is" "kind" "+")) -> ("something" "is" "cold" "+"))
If something is rough then it is white.
((("something" "is" "rough" "+")) -> ("something" "is" "white" "+"))
Charlie is white.
True
1
proof
[(triple2)]
("Charlie" "is" "white" "+")
triple2
Erin is not kind.
False
1
inv-proof
[(triple3)]
("Erin" "is" "kind" "-")
triple3
Erin is blue.
True
2
proof
[(((triple3) -> rule4))]
("Erin" "is" "blue" "+")
((triple3) -> (rule4 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is not blue.
False
2
inv-proof
[(((triple3) -> rule4))]
("Erin" "is" "blue" "-")
((triple3) -> (rule4 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is cold.
True
4
proof
[(((((triple3) -> rule4) triple3) -> rule7))]
("Erin" "is" "cold" "+")
((((triple3) -> (rule4 % int2)) triple3) -> (rule7 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is not cold.
False
4
inv-proof
[(((((triple3) -> rule4) triple3) -> rule7))]
("Erin" "is" "cold" "-")
((((triple3) -> (rule4 % int2)) triple3) -> (rule7 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is not rough.
True
5
proof
[(((((((triple3) -> rule4) triple3) -> rule7)) -> rule6))]
("Erin" "is" "rough" "-")
((((((triple3) -> (rule4 % int3)) triple3) -> (rule7 % int2))) -> (rule6 % int1))
Erin is not rough.
("Erin" "is" "rough" "-")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Erin is rough.
False
5
inv-proof
[(((((((triple3) -> rule4) triple3) -> rule7)) -> rule6))]
("Erin" "is" "rough" "+")
((((((triple3) -> (rule4 % int3)) triple3) -> (rule7 % int2))) -> (rule6 % int1))
Erin is not rough.
("Erin" "is" "rough" "-")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3
Gary is not blue.
Unknown
inv-rconc
[@1: Gary is blue.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "blue" "-")
Gary is rough.
Unknown
rconc
[@2: Gary is rough.[CWA. Example of deepest failure = (rule5 <- rule7 <- FAIL)]]
("Gary" "is" "rough" "+")
Gary is not cold.
Unknown
inv-rconc
[@1: Gary is cold.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Gary" "is" "cold" "-")
Charlie is blue.
Unknown
rconc
[@1: Charlie is blue.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Charlie" "is" "blue" "+")
Charlie is not young.
Unknown
inv-random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "-")
Charlie is kind.
Unknown
random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "+")
Anne is not round.
Unknown
inv-random
[@0: Anne is round.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "round" "-")
Gary is young.
Unknown
random
[@0: Gary is young.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "young" "+")
@0: Anne is blue.[(triple1)] Charlie is white.[(triple2)] Erin is kind.[(triple3)] Gary is round.[(triple4)] @1: Erin is blue.[(((triple3) -> rule4))] @2: Erin is cold.[(((((triple3) -> rule4) triple3) -> rule7))] @3: Erin is not rough.[(((((((triple3) -> rule4) triple3) -> rule7)) -> rule6))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Charlie is white.
("Charlie" "is" "white" "+")
triple2
Erin is kind.
("Erin" "is" "kind" "+")
triple3
Gary is round.
("Gary" "is" "round" "+")
triple4
Erin is blue.
("Erin" "is" "blue" "+")
((triple3) -> (rule4 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
((((triple3) -> (rule4 % int2)) triple3) -> (rule7 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is not rough.
("Erin" "is" "rough" "-")
((((((triple3) -> (rule4 % int3)) triple3) -> (rule7 % int2))) -> (rule6 % int1))
Erin is not rough.
("Erin" "is" "rough" "-")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is blue.
("Erin" "is" "blue" "+")
int3