Anne is kind. Charlie is kind. Erin is red. Fiona is white. If something is blue then it is kind. All white, kind things are blue. All red, kind things are blue. All white things are not red. If something is kind and not blue then it is quiet. If something is white and not quiet then it is nice. If something is nice and not red then it is green. If something is white and not blue then it is green.
Anne is kind.
("Anne" "is" "kind" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Erin is red.
("Erin" "is" "red" "+")
Fiona is white.
("Fiona" "is" "white" "+")
If something is blue then it is kind.
((("something" "is" "blue" "+")) -> ("something" "is" "kind" "+"))
All white, kind things are blue.
((("something" "is" "white" "+") ("something" "is" "kind" "+")) -> ("something" "is" "blue" "+"))
All red, kind things are blue.
((("something" "is" "red" "+") ("something" "is" "kind" "+")) -> ("something" "is" "blue" "+"))
All white things are not red.
((("something" "is" "white" "+")) -> ("something" "is" "red" "-"))
If something is kind and not blue then it is quiet.
((("something" "is" "kind" "+") ("something" "is" "blue" "~")) -> ("something" "is" "quiet" "+"))
If something is white and not quiet then it is nice.
((("something" "is" "white" "+") ("something" "is" "quiet" "~")) -> ("something" "is" "nice" "+"))
If something is nice and not red then it is green.
((("something" "is" "nice" "+") ("something" "is" "red" "~")) -> ("something" "is" "green" "+"))
If something is white and not blue then it is green.
((("something" "is" "white" "+") ("something" "is" "blue" "~")) -> ("something" "is" "green" "+"))
Erin is red.
True
1
proof
[(triple3)]
("Erin" "is" "red" "+")
triple3
Erin is not red.
False
1
inv-proof
[(triple3)]
("Erin" "is" "red" "-")
triple3
Fiona is not red.
True
2
proof
[(((triple4) -> rule4))]
("Fiona" "is" "red" "-")
((triple4) -> (rule4 % int1))
Fiona is not red.
("Fiona" "is" "red" "-")
int1
Fiona is red.
False
2
inv-proof
[(((triple4) -> rule4))]
("Fiona" "is" "red" "+")
((triple4) -> (rule4 % int1))
Fiona is not red.
("Fiona" "is" "red" "-")
int1
Erin is not quiet.
Unknown
inv-rconc
[@1: Erin is quiet.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Erin" "is" "quiet" "-")
Anne is green.
Unknown
rconc
[@1: Anne is green.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Anne" "is" "green" "+")
Charlie is not red.
Unknown
inv-random
[@0: Charlie is red.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "red" "-")
Anne is white.
Unknown
random
[@0: Anne is white.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "white" "+")
@0: Anne is kind.[(triple1)] Charlie is kind.[(triple2)] Erin is red.[(triple3)] Fiona is white.[(triple4)] @1: Fiona is not red.[(((triple4) -> rule4))]
Anne is kind.
("Anne" "is" "kind" "+")
triple1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple2
Erin is red.
("Erin" "is" "red" "+")
triple3
Fiona is white.
("Fiona" "is" "white" "+")
triple4
Fiona is not red.
("Fiona" "is" "red" "-")
((triple4) -> (rule4 % int1))
Fiona is not red.
("Fiona" "is" "red" "-")
int1