Anne is blue. Anne is green. Anne is nice. Anne is quiet. Anne is rough. Anne is white. Charlie is not blue. Charlie is white. Erin is white. Fiona is not blue. Fiona is green. Fiona is nice. If someone is rough and not nice then they are white. All nice people are white. Nice people are rough. If Charlie is quiet then Charlie is not cold. All white people are cold. If someone is white and quiet then they are green.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is white.
("Anne" "is" "white" "+")
Charlie is not blue.
("Charlie" "is" "blue" "-")
Charlie is white.
("Charlie" "is" "white" "+")
Erin is white.
("Erin" "is" "white" "+")
Fiona is not blue.
("Fiona" "is" "blue" "-")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
If someone is rough and not nice then they are white.
((("someone" "is" "rough" "+") ("someone" "is" "nice" "~")) -> ("someone" "is" "white" "+"))
All nice people are white.
((("someone" "is" "nice" "+")) -> ("someone" "is" "white" "+"))
Nice people are rough.
((("someone" "is" "nice" "+")) -> ("someone" "is" "rough" "+"))
If Charlie is quiet then Charlie is not cold.
((("Charlie" "is" "quiet" "+")) -> ("Charlie" "is" "cold" "-"))
All white people are cold.
((("someone" "is" "white" "+")) -> ("someone" "is" "cold" "+"))
If someone is white and quiet then they are green.
((("someone" "is" "white" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "green" "+"))
Charlie is not blue.
True
1
proof
[(triple7)]
("Charlie" "is" "blue" "-")
triple7
Erin is not white.
False
1
inv-proof
[(triple9)]
("Erin" "is" "white" "-")
triple9
Fiona is rough.
True
2
proof
[(((triple12) -> rule3))]
("Fiona" "is" "rough" "+")
((triple12) -> (rule3 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is not white.
False
2
inv-proof
[(((triple12) -> rule2))]
("Fiona" "is" "white" "-")
((triple12) -> (rule2 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is cold.
True
3
proof
[(((((triple12) -> rule2)) -> rule5))]
("Fiona" "is" "cold" "+")
((((triple12) -> (rule2 % int2))) -> (rule5 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is not cold.
False
3
inv-proof
[(((((triple12) -> rule2)) -> rule5))]
("Fiona" "is" "cold" "-")
((((triple12) -> (rule2 % int2))) -> (rule5 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Erin is not rough.
Unknown
inv-rconc
[@1: Erin is rough.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "rough" "-")
Erin is green.
Unknown
rconc
[@1: Erin is green.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Erin" "is" "green" "+")
Charlie is not green.
Unknown
inv-rconc
[@1: Charlie is green.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Charlie" "is" "green" "-")
Fiona is quiet.
Unknown
random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "+")
Erin is not nice.
Unknown
inv-random
[@0: Erin is nice.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "nice" "-")
Erin is blue.
Unknown
random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "+")
@0: Anne is blue.[(triple1)] Anne is green.[(triple2 OR ((triple6 triple4) -> rule6) OR ((((triple3) -> rule2) triple4) -> rule6))] Anne is nice.[(triple3)] Anne is quiet.[(triple4)] Anne is rough.[(triple5 OR ((triple3) -> rule3))] Anne is white.[(triple6 OR ((triple3) -> rule2))] Charlie is not blue.[(triple7)] Charlie is white.[(triple8)] Erin is white.[(triple9)] Fiona is green.[(triple11)] Fiona is nice.[(triple12)] Fiona is not blue.[(triple10)] @1: Anne is cold.[(((triple6) -> rule5) OR ((((triple3) -> rule2)) -> rule5))] Charlie is cold.[(((triple8) -> rule5))] Erin is cold.[(((triple9) -> rule5))] Fiona is rough.[(((triple12) -> rule3))] Fiona is white.[(((triple12) -> rule2))] @2: Fiona is cold.[(((((triple12) -> rule2)) -> rule5))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple2
((triple6 triple4) -> (rule6 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
((((triple3) -> (rule2 % int2)) triple4) -> (rule6 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
triple3
Anne is quiet.
("Anne" "is" "quiet" "+")
triple4
Anne is rough.
("Anne" "is" "rough" "+")
triple5
((triple3) -> (rule3 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
triple6
((triple3) -> (rule2 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Charlie is not blue.
("Charlie" "is" "blue" "-")
triple7
Charlie is white.
("Charlie" "is" "white" "+")
triple8
Erin is white.
("Erin" "is" "white" "+")
triple9
Fiona is green.
("Fiona" "is" "green" "+")
triple11
Fiona is nice.
("Fiona" "is" "nice" "+")
triple12
Fiona is not blue.
("Fiona" "is" "blue" "-")
triple10
Anne is cold.
("Anne" "is" "cold" "+")
((triple6) -> (rule5 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
((((triple3) -> (rule2 % int2))) -> (rule5 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple8) -> (rule5 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
((triple9) -> (rule5 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
((triple12) -> (rule3 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
((triple12) -> (rule2 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
((((triple12) -> (rule2 % int2))) -> (rule5 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2