Anne is young. Charlie is nice. Gary is red. Young things are blue. If something is white and round then it is red. Young things are white. If something is round and blue then it is red. Red things are white. If something is blue then it is round.
Anne is young.
("Anne" "is" "young" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Gary is red.
("Gary" "is" "red" "+")
Young things are blue.
((("something" "is" "young" "+")) -> ("something" "is" "blue" "+"))
If something is white and round then it is red.
((("something" "is" "white" "+") ("something" "is" "round" "+")) -> ("something" "is" "red" "+"))
Young things are white.
((("something" "is" "young" "+")) -> ("something" "is" "white" "+"))
If something is round and blue then it is red.
((("something" "is" "round" "+") ("something" "is" "blue" "+")) -> ("something" "is" "red" "+"))
Red things are white.
((("something" "is" "red" "+")) -> ("something" "is" "white" "+"))
If something is blue then it is round.
((("something" "is" "blue" "+")) -> ("something" "is" "round" "+"))
Gary is red.
True
1
proof
[(triple3)]
("Gary" "is" "red" "+")
triple3
Anne is not young.
False
1
inv-proof
[(triple1)]
("Anne" "is" "young" "-")
triple1
Gary is white.
True
2
proof
[(((triple3) -> rule5))]
("Gary" "is" "white" "+")
((triple3) -> (rule5 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is not white.
False
2
inv-proof
[(((triple3) -> rule5))]
("Gary" "is" "white" "-")
((triple3) -> (rule5 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Anne is round.
True
3
proof
[(((((triple1) -> rule1)) -> rule6))]
("Anne" "is" "round" "+")
((((triple1) -> (rule1 % int2))) -> (rule6 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is not round.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule6))]
("Anne" "is" "round" "-")
((((triple1) -> (rule1 % int2))) -> (rule6 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is red.
True
6
proof
[(((((triple1) -> rule3) ((((triple1) -> rule1)) -> rule6)) -> rule2) OR ((((((triple1) -> rule1)) -> rule6) ((triple1) -> rule1)) -> rule4))]
("Anne" "is" "red" "+")
((((triple1) -> (rule3 % int4)) ((((triple1) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Anne is white.
("Anne" "is" "white" "+")
int4
((((((triple1) -> (rule1 % int3))) -> (rule6 % int2)) ((triple1) -> (rule1 % int3))) -> (rule4 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Anne is not red.
False
6
inv-proof
[(((((triple1) -> rule3) ((((triple1) -> rule1)) -> rule6)) -> rule2) OR ((((((triple1) -> rule1)) -> rule6) ((triple1) -> rule1)) -> rule4))]
("Anne" "is" "red" "-")
((((triple1) -> (rule3 % int4)) ((((triple1) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Anne is white.
("Anne" "is" "white" "+")
int4
((((((triple1) -> (rule1 % int3))) -> (rule6 % int2)) ((triple1) -> (rule1 % int3))) -> (rule4 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Charlie is not blue.
Unknown
inv-rconc
[@1: Charlie is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "blue" "-")
Charlie is round.
Unknown
rconc
[@2: Charlie is round.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("Charlie" "is" "round" "+")
Gary is not round.
Unknown
inv-rconc
[@2: Gary is round.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("Gary" "is" "round" "-")
Charlie is white.
Unknown
rconc
[@3: Charlie is white.[CWA. Example of deepest failure = (rule5 <- rule2 <- rule3 <- FAIL)]]
("Charlie" "is" "white" "+")
Anne is not nice.
Unknown
inv-random
[@0: Anne is nice.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "nice" "-")
Charlie is green.
Unknown
random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "+")
Gary is not nice.
Unknown
inv-random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "-")
Charlie is young.
Unknown
random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "+")
@0: Anne is young.[(triple1)] Charlie is nice.[(triple2)] Gary is red.[(triple3)] @1: Anne is blue.[(((triple1) -> rule1))] Anne is white.[(((triple1) -> rule3) OR ((((((((triple1) -> rule1)) -> rule6) ((triple1) -> rule1)) -> rule4)) -> rule5))] Gary is white.[(((triple3) -> rule5))] @2: Anne is round.[(((((triple1) -> rule1)) -> rule6))] @3: Anne is red.[(((((triple1) -> rule3) ((((triple1) -> rule1)) -> rule6)) -> rule2) OR ((((((triple1) -> rule1)) -> rule6) ((triple1) -> rule1)) -> rule4))]
Anne is young.
("Anne" "is" "young" "+")
triple1
Charlie is nice.
("Charlie" "is" "nice" "+")
triple2
Gary is red.
("Gary" "is" "red" "+")
triple3
Anne is blue.
("Anne" "is" "blue" "+")
((triple1) -> (rule1 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
((triple1) -> (rule3 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
((((((((triple1) -> (rule1 % int4))) -> (rule6 % int3)) ((triple1) -> (rule1 % int4))) -> (rule4 % int2))) -> (rule5 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Anne is blue.
("Anne" "is" "blue" "+")
int4
Gary is white.
("Gary" "is" "white" "+")
((triple3) -> (rule5 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
((((triple1) -> (rule1 % int2))) -> (rule6 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
((((triple1) -> (rule3 % int4)) ((((triple1) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Anne is white.
("Anne" "is" "white" "+")
int4
((((((triple1) -> (rule1 % int3))) -> (rule6 % int2)) ((triple1) -> (rule1 % int3))) -> (rule4 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3