Anne is green. Fiona is kind. Gary is white. Harry is quiet. If someone is kind then they are green. All nice people are blue. If someone is green then they are white. Kind, blue people are green. If Anne is red and Anne is nice then Anne is blue. If someone is white then they are nice.
Anne is green.
("Anne" "is" "green" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Gary is white.
("Gary" "is" "white" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
If someone is kind then they are green.
((("someone" "is" "kind" "+")) -> ("someone" "is" "green" "+"))
All nice people are blue.
((("someone" "is" "nice" "+")) -> ("someone" "is" "blue" "+"))
If someone is green then they are white.
((("someone" "is" "green" "+")) -> ("someone" "is" "white" "+"))
Kind, blue people are green.
((("someone" "is" "kind" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "green" "+"))
If Anne is red and Anne is nice then Anne is blue.
((("Anne" "is" "red" "+") ("Anne" "is" "nice" "+")) -> ("Anne" "is" "blue" "+"))
If someone is white then they are nice.
((("someone" "is" "white" "+")) -> ("someone" "is" "nice" "+"))
Harry is quiet.
True
1
proof
[(triple4)]
("Harry" "is" "quiet" "+")
triple4
Gary is not white.
False
1
inv-proof
[(triple3)]
("Gary" "is" "white" "-")
triple3
Gary is nice.
True
2
proof
[(((triple3) -> rule6))]
("Gary" "is" "nice" "+")
((triple3) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Fiona is not green.
False
2
inv-proof
[(((triple2) -> rule1))]
("Fiona" "is" "green" "-")
((triple2) -> (rule1 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is white.
True
3
proof
[(((((triple2) -> rule1)) -> rule3))]
("Fiona" "is" "white" "+")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is not white.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule3))]
("Fiona" "is" "white" "-")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Anne is blue.
True
4
proof
[(((((((triple1) -> rule3)) -> rule6)) -> rule2))]
("Anne" "is" "blue" "+")
((((((triple1) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Anne is not blue.
False
4
inv-proof
[(((((((triple1) -> rule3)) -> rule6)) -> rule2))]
("Anne" "is" "blue" "-")
((((((triple1) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Gary is not green.
Unknown
inv-rconc
[@1: Gary is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "green" "-")
Harry is blue.
Unknown
rconc
[@4: Harry is blue.[CWA. Example of deepest failure = (rule2 <- rule6 <- rule3 <- rule1 <- FAIL)]]
("Harry" "is" "blue" "+")
Harry is not nice.
Unknown
inv-rconc
[@3: Harry is nice.[CWA. Example of deepest failure = (rule6 <- rule3 <- rule1 <- FAIL)]]
("Harry" "is" "nice" "-")
Harry is green.
Unknown
rconc
[@1: Harry is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "green" "+")
Fiona is not quiet.
Unknown
inv-random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "-")
Harry is red.
Unknown
random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "+")
Fiona is not red.
Unknown
inv-random
[@0: Fiona is red.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "red" "-")
Gary is quiet.
Unknown
random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "+")
@0: Anne is green.[(triple1)] Fiona is kind.[(triple2)] Gary is white.[(triple3)] Harry is quiet.[(triple4)] @1: Anne is white.[(((triple1) -> rule3))] Fiona is green.[(((triple2) -> rule1))] Gary is nice.[(((triple3) -> rule6))] @2: Anne is nice.[(((((triple1) -> rule3)) -> rule6))] Fiona is white.[(((((triple2) -> rule1)) -> rule3))] Gary is blue.[(((((triple3) -> rule6)) -> rule2))] @3: Anne is blue.[(((((((triple1) -> rule3)) -> rule6)) -> rule2))] Fiona is nice.[(((((((triple2) -> rule1)) -> rule3)) -> rule6))] @4: Fiona is blue.[(((((((((triple2) -> rule1)) -> rule3)) -> rule6)) -> rule2))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Fiona is kind.
("Fiona" "is" "kind" "+")
triple2
Gary is white.
("Gary" "is" "white" "+")
triple3
Harry is quiet.
("Harry" "is" "quiet" "+")
triple4
Anne is white.
("Anne" "is" "white" "+")
((triple1) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
((triple2) -> (rule1 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
((triple3) -> (rule6 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
((((triple1) -> (rule3 % int2))) -> (rule6 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Gary is blue.
("Gary" "is" "blue" "+")
((((triple3) -> (rule6 % int2))) -> (rule2 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
((((((triple1) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is nice.
("Anne" "is" "nice" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
int3
Fiona is nice.
("Fiona" "is" "nice" "+")
((((((triple2) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3
Fiona is blue.
("Fiona" "is" "blue" "+")
((((((((triple2) -> (rule1 % int4))) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
int3
Fiona is green.
("Fiona" "is" "green" "+")
int4