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