Anne is blue. Charlie is white. Fiona is nice. Harry is kind. If Charlie is quiet then Charlie is white. All white people are green. If Fiona is quiet and Fiona is kind then Fiona is white.
Anne is blue.
("Anne" "is" "blue" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Harry is kind.
("Harry" "is" "kind" "+")
If Charlie is quiet then Charlie is white.
((("Charlie" "is" "quiet" "+")) -> ("Charlie" "is" "white" "+"))
All white people are green.
((("someone" "is" "white" "+")) -> ("someone" "is" "green" "+"))
If Fiona is quiet and Fiona is kind then Fiona is white.
((("Fiona" "is" "quiet" "+") ("Fiona" "is" "kind" "+")) -> ("Fiona" "is" "white" "+"))
Fiona is nice.
True
1
proof
[(triple3)]
("Fiona" "is" "nice" "+")
triple3
Charlie is not white.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "white" "-")
triple2
Charlie is green.
True
2
proof
[(((triple2) -> rule2))]
("Charlie" "is" "green" "+")
((triple2) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is not green.
False
2
inv-proof
[(((triple2) -> rule2))]
("Charlie" "is" "green" "-")
((triple2) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Anne is not green.
Unknown
inv-rconc
[@1: Anne is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "green" "-")
Fiona is white.
Unknown
rconc
[@1: Fiona is white.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "white" "+")
Fiona is not kind.
Unknown
inv-random
[@0: Fiona is kind.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "kind" "-")
Fiona is rough.
Unknown
random
[@0: Fiona is rough.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "rough" "+")
@0: Anne is blue.[(triple1)] Charlie is white.[(triple2)] Fiona is nice.[(triple3)] Harry is kind.[(triple4)] @1: Charlie is green.[(((triple2) -> rule2))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Charlie is white.
("Charlie" "is" "white" "+")
triple2
Fiona is nice.
("Fiona" "is" "nice" "+")
triple3
Harry is kind.
("Harry" "is" "kind" "+")
triple4
Charlie is green.
("Charlie" "is" "green" "+")
((triple2) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1