Anne is green. Charlie is quiet. Charlie is white. Fiona is green. Fiona is red. Gary is not quiet. Gary is young. All green things are blue. All green things are blue. All green, white things are not young. Red things are not white. If something is quiet and white then it is not red. If Anne is green and Anne is blue then Anne is red.
Anne is green.
("Anne" "is" "green" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is white.
("Charlie" "is" "white" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Gary is not quiet.
("Gary" "is" "quiet" "-")
Gary is young.
("Gary" "is" "young" "+")
All green things are blue.
((("something" "is" "green" "+")) -> ("something" "is" "blue" "+"))
All green things are blue.
((("something" "is" "green" "+")) -> ("something" "is" "blue" "+"))
All green, white things are not young.
((("something" "is" "green" "+") ("something" "is" "white" "+")) -> ("something" "is" "young" "-"))
Red things are not white.
((("something" "is" "red" "+")) -> ("something" "is" "white" "-"))
If something is quiet and white then it is not red.
((("something" "is" "quiet" "+") ("something" "is" "white" "+")) -> ("something" "is" "red" "-"))
If Anne is green and Anne is blue then Anne is red.
((("Anne" "is" "green" "+") ("Anne" "is" "blue" "+")) -> ("Anne" "is" "red" "+"))
Fiona is red.
True
1
proof
[(triple5)]
("Fiona" "is" "red" "+")
triple5
Fiona is not green.
False
1
inv-proof
[(triple4)]
("Fiona" "is" "green" "-")
triple4
Fiona is blue.
True
2
proof
[(((triple4) -> rule1) OR ((triple4) -> rule2))]
("Fiona" "is" "blue" "+")
((triple4) -> (rule1 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
((triple4) -> (rule2 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is not blue.
False
2
inv-proof
[(((triple4) -> rule1) OR ((triple4) -> rule2))]
("Fiona" "is" "blue" "-")
((triple4) -> (rule1 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
((triple4) -> (rule2 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Anne is red.
True
4
proof
[(((triple1 ((triple1) -> rule1)) -> rule6) OR ((triple1 ((triple1) -> rule2)) -> rule6))]
("Anne" "is" "red" "+")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
((triple1 ((triple1) -> (rule2 % int2))) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is not red.
False
4
inv-proof
[(((triple1 ((triple1) -> rule1)) -> rule6) OR ((triple1 ((triple1) -> rule2)) -> rule6))]
("Anne" "is" "red" "-")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
((triple1 ((triple1) -> (rule2 % int2))) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is not white.
True
5
proof
[(((((triple1 ((triple1) -> rule1)) -> rule6)) -> rule4) OR ((((triple1 ((triple1) -> rule2)) -> rule6)) -> rule4))]
("Anne" "is" "white" "-")
((((triple1 ((triple1) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Anne is not white.
("Anne" "is" "white" "-")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
((((triple1 ((triple1) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Anne is not white.
("Anne" "is" "white" "-")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Anne is white.
False
5
inv-proof
[(((((triple1 ((triple1) -> rule1)) -> rule6)) -> rule4) OR ((((triple1 ((triple1) -> rule2)) -> rule6)) -> rule4))]
("Anne" "is" "white" "+")
((((triple1 ((triple1) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Anne is not white.
("Anne" "is" "white" "-")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
((((triple1 ((triple1) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Anne is not white.
("Anne" "is" "white" "-")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Gary is not blue.
Unknown
inv-rconc
[@1: Gary is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "blue" "-")
Charlie is blue.
Unknown
rconc
[@1: Charlie is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "blue" "+")
Fiona is not quiet.
Unknown
inv-random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "-")
Gary is green.
Unknown
random
[@0: Gary is green.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "green" "+")
Anne is not big.
Unknown
inv-random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "-")
Gary is big.
Unknown
random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "+")
Anne is not quiet.
Unknown
inv-random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "-")
Charlie is big.
Unknown
random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "+")
@0: Anne is green.[(triple1)] Charlie is quiet.[(triple2)] Charlie is white.[(triple3)] Fiona is green.[(triple4)] Fiona is red.[(triple5)] Gary is not quiet.[(triple6)] Gary is young.[(triple7)] @1: Anne is blue.[(((triple1) -> rule1) OR ((triple1) -> rule2))] Charlie is not red.[(((triple2 triple3) -> rule5))] Fiona is blue.[(((triple4) -> rule1) OR ((triple4) -> rule2))] Fiona is not white.[(((triple5) -> rule4))] @2: Anne is red.[(((triple1 ((triple1) -> rule1)) -> rule6) OR ((triple1 ((triple1) -> rule2)) -> rule6))] @3: Anne is not white.[(((((triple1 ((triple1) -> rule1)) -> rule6)) -> rule4) OR ((((triple1 ((triple1) -> rule2)) -> rule6)) -> rule4))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple2
Charlie is white.
("Charlie" "is" "white" "+")
triple3
Fiona is green.
("Fiona" "is" "green" "+")
triple4
Fiona is red.
("Fiona" "is" "red" "+")
triple5
Gary is not quiet.
("Gary" "is" "quiet" "-")
triple6
Gary is young.
("Gary" "is" "young" "+")
triple7
Anne is blue.
("Anne" "is" "blue" "+")
((triple1) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
((triple1) -> (rule2 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Charlie is not red.
("Charlie" "is" "red" "-")
((triple2 triple3) -> (rule5 % int1))
Charlie is not red.
("Charlie" "is" "red" "-")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
((triple4) -> (rule1 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
((triple4) -> (rule2 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is not white.
("Fiona" "is" "white" "-")
((triple5) -> (rule4 % int1))
Fiona is not white.
("Fiona" "is" "white" "-")
int1
Anne is red.
("Anne" "is" "red" "+")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
((triple1 ((triple1) -> (rule2 % int2))) -> (rule6 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is not white.
("Anne" "is" "white" "-")
((((triple1 ((triple1) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Anne is not white.
("Anne" "is" "white" "-")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
((((triple1 ((triple1) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
Anne is not white.
("Anne" "is" "white" "-")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3