Anne is nice. Anne is round. Gary is quiet. White people are red. If someone is rough and not nice then they are not round. All nice people are round. If Gary is not nice then Gary is blue. Round, nice people are blue. All blue people are white. Rough people are white. Blue people are white.
Anne is nice.
("Anne" "is" "nice" "+")
Anne is round.
("Anne" "is" "round" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
White people are red.
((("someone" "is" "white" "+")) -> ("someone" "is" "red" "+"))
If someone is rough and not nice then they are not round.
((("someone" "is" "rough" "+") ("someone" "is" "nice" "~")) -> ("someone" "is" "round" "-"))
All nice people are round.
((("someone" "is" "nice" "+")) -> ("someone" "is" "round" "+"))
If Gary is not nice then Gary is blue.
((("Gary" "is" "nice" "~")) -> ("Gary" "is" "blue" "+"))
Round, nice people are blue.
((("someone" "is" "round" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "blue" "+"))
All blue people are white.
((("someone" "is" "blue" "+")) -> ("someone" "is" "white" "+"))
Rough people are white.
((("someone" "is" "rough" "+")) -> ("someone" "is" "white" "+"))
Blue people are white.
((("someone" "is" "blue" "+")) -> ("someone" "is" "white" "+"))
Anne is nice.
True
1
proof
[(triple1)]
("Anne" "is" "nice" "+")
triple1
Anne is not round.
False
1
inv-proof
[(triple2 OR ((triple1) -> rule3))]
("Anne" "is" "round" "-")
triple2
((triple1) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is blue.
True
3
proof
[(((triple2 triple1) -> rule5) OR ((((triple1) -> rule3) triple1) -> rule5))]
("Anne" "is" "blue" "+")
((triple2 triple1) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
((((triple1) -> (rule3 % int2)) triple1) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is not blue.
False
3
inv-proof
[(((triple2 triple1) -> rule5) OR ((((triple1) -> rule3) triple1) -> rule5))]
("Anne" "is" "blue" "-")
((triple2 triple1) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
((((triple1) -> (rule3 % int2)) triple1) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is white.
True
4
proof
[(((((triple2 triple1) -> rule5)) -> rule6) OR ((((triple2 triple1) -> rule5)) -> rule8) OR ((((((triple1) -> rule3) triple1) -> rule5)) -> rule6) OR ((((((triple1) -> rule3) triple1) -> rule5)) -> rule8))]
("Anne" "is" "white" "+")
((((triple2 triple1) -> (rule5 % int2))) -> (rule6 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
((((triple2 triple1) -> (rule5 % int2))) -> (rule8 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
((((((triple1) -> (rule3 % int3)) triple1) -> (rule5 % int2))) -> (rule6 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
((((((triple1) -> (rule3 % int3)) triple1) -> (rule5 % int2))) -> (rule8 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Anne is not white.
False
4
inv-proof
[(((((triple2 triple1) -> rule5)) -> rule6) OR ((((triple2 triple1) -> rule5)) -> rule8) OR ((((((triple1) -> rule3) triple1) -> rule5)) -> rule6) OR ((((((triple1) -> rule3) triple1) -> rule5)) -> rule8))]
("Anne" "is" "white" "-")
((((triple2 triple1) -> (rule5 % int2))) -> (rule6 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
((((triple2 triple1) -> (rule5 % int2))) -> (rule8 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
((((((triple1) -> (rule3 % int3)) triple1) -> (rule5 % int2))) -> (rule6 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
((((((triple1) -> (rule3 % int3)) triple1) -> (rule5 % int2))) -> (rule8 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Anne is red.
True
5
proof
[(((((((triple2 triple1) -> rule5)) -> rule6)) -> rule1) OR ((((((triple2 triple1) -> rule5)) -> rule8)) -> rule1) OR ((((((((triple1) -> rule3) triple1) -> rule5)) -> rule6)) -> rule1) OR ((((((((triple1) -> rule3) triple1) -> rule5)) -> rule8)) -> rule1))]
("Anne" "is" "red" "+")
((((((triple2 triple1) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
((((((triple2 triple1) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
((((((((triple1) -> (rule3 % int4)) triple1) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Anne is round.
("Anne" "is" "round" "+")
int4
((((((((triple1) -> (rule3 % int4)) triple1) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Anne is round.
("Anne" "is" "round" "+")
int4
Anne is not red.
False
5
inv-proof
[(((((((triple2 triple1) -> rule5)) -> rule6)) -> rule1) OR ((((((triple2 triple1) -> rule5)) -> rule8)) -> rule1) OR ((((((((triple1) -> rule3) triple1) -> rule5)) -> rule6)) -> rule1) OR ((((((((triple1) -> rule3) triple1) -> rule5)) -> rule8)) -> rule1))]
("Anne" "is" "red" "-")
((((((triple2 triple1) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
((((((triple2 triple1) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
((((((((triple1) -> (rule3 % int4)) triple1) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Anne is round.
("Anne" "is" "round" "+")
int4
((((((((triple1) -> (rule3 % int4)) triple1) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Anne is round.
("Anne" "is" "round" "+")
int4
Gary is not red.
Unknown
inv-rconc
[@3: Gary is red.[CWA. Example of deepest failure = (rule1 <- rule6 <- rule4 <- FAIL)]]
("Gary" "is" "red" "-")
Gary is blue.
Unknown
rconc
[@1: Gary is blue.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "blue" "+")
Gary is not round.
Unknown
inv-rconc
[@1: Gary is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "round" "-")
Gary is white.
Unknown
rconc
[@2: Gary is white.[CWA. Example of deepest failure = (rule6 <- rule4 <- FAIL)]]
("Gary" "is" "white" "+")
Gary is not nice.
Unknown
inv-random
[@0: Gary is nice.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "nice" "-")
Gary is rough.
Unknown
random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "+")
Anne is not rough.
Unknown
inv-random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "-")
Anne is quiet.
Unknown
random
[@0: Anne is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "quiet" "+")
@0: Anne is nice.[(triple1)] Anne is round.[(triple2 OR ((triple1) -> rule3))] Gary is quiet.[(triple3)] @1: Anne is blue.[(((triple2 triple1) -> rule5) OR ((((triple1) -> rule3) triple1) -> rule5))] @2: Anne is white.[(((((triple2 triple1) -> rule5)) -> rule6) OR ((((triple2 triple1) -> rule5)) -> rule8) OR ((((((triple1) -> rule3) triple1) -> rule5)) -> rule6) OR ((((((triple1) -> rule3) triple1) -> rule5)) -> rule8))] @3: Anne is red.[(((((((triple2 triple1) -> rule5)) -> rule6)) -> rule1) OR ((((((triple2 triple1) -> rule5)) -> rule8)) -> rule1) OR ((((((((triple1) -> rule3) triple1) -> rule5)) -> rule6)) -> rule1) OR ((((((((triple1) -> rule3) triple1) -> rule5)) -> rule8)) -> rule1))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Anne is round.
("Anne" "is" "round" "+")
triple2
((triple1) -> (rule3 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Gary is quiet.
("Gary" "is" "quiet" "+")
triple3
Anne is blue.
("Anne" "is" "blue" "+")
((triple2 triple1) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
((((triple1) -> (rule3 % int2)) triple1) -> (rule5 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is white.
("Anne" "is" "white" "+")
((((triple2 triple1) -> (rule5 % int2))) -> (rule6 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
((((triple2 triple1) -> (rule5 % int2))) -> (rule8 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
((((((triple1) -> (rule3 % int3)) triple1) -> (rule5 % int2))) -> (rule6 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
((((((triple1) -> (rule3 % int3)) triple1) -> (rule5 % int2))) -> (rule8 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Anne is red.
("Anne" "is" "red" "+")
((((((triple2 triple1) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
((((((triple2 triple1) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
((((((((triple1) -> (rule3 % int4)) triple1) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Anne is round.
("Anne" "is" "round" "+")
int4
((((((((triple1) -> (rule3 % int4)) triple1) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3
Anne is round.
("Anne" "is" "round" "+")
int4