Anne is big. Anne is red. Anne is white. Charlie is green. Charlie is kind. Charlie is round. Charlie is white. If something is green and big then it is rough. If something is rough then it is green. If Charlie is white and Charlie is round then Charlie is red. If Charlie is green and Charlie is kind then Charlie is round. If something is green then it is round. If something is white then it is rough.
Anne is big.
("Anne" "is" "big" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is white.
("Anne" "is" "white" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is white.
("Charlie" "is" "white" "+")
If something is green and big then it is rough.
((("something" "is" "green" "+") ("something" "is" "big" "+")) -> ("something" "is" "rough" "+"))
If something is rough then it is green.
((("something" "is" "rough" "+")) -> ("something" "is" "green" "+"))
If Charlie is white and Charlie is round then Charlie is red.
((("Charlie" "is" "white" "+") ("Charlie" "is" "round" "+")) -> ("Charlie" "is" "red" "+"))
If Charlie is green and Charlie is kind then Charlie is round.
((("Charlie" "is" "green" "+") ("Charlie" "is" "kind" "+")) -> ("Charlie" "is" "round" "+"))
If something is green then it is round.
((("something" "is" "green" "+")) -> ("something" "is" "round" "+"))
If something is white then it is rough.
((("something" "is" "white" "+")) -> ("something" "is" "rough" "+"))
Charlie is white.
True
1
proof
[(triple7)]
("Charlie" "is" "white" "+")
triple7
Charlie is not round.
False
1
inv-proof
[(triple6 OR ((triple4) -> rule5) OR ((triple4 triple5) -> rule4) OR ((((((triple7) -> rule6)) -> rule2)) -> rule5) OR ((((((triple7) -> rule6)) -> rule2) triple5) -> rule4))]
("Charlie" "is" "round" "-")
triple6
((triple4) -> (rule5 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
((triple4 triple5) -> (rule4 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
((((((triple7) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
((((((triple7) -> (rule6 % int3))) -> (rule2 % int2)) triple5) -> (rule4 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is rough.
True
2
proof
[(((triple7) -> rule6))]
("Charlie" "is" "rough" "+")
((triple7) -> (rule6 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is not red.
False
3
inv-proof
[(((triple7 triple6) -> rule3) OR ((triple7 ((triple4) -> rule5)) -> rule3) OR ((triple7 ((triple4 triple5) -> rule4)) -> rule3) OR ((triple7 ((((((triple7) -> rule6)) -> rule2)) -> rule5)) -> rule3) OR ((triple7 ((((((triple7) -> rule6)) -> rule2) triple5) -> rule4)) -> rule3))]
("Charlie" "is" "red" "-")
((triple7 triple6) -> (rule3 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
((triple7 ((triple4) -> (rule5 % int2))) -> (rule3 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
((triple7 ((triple4 triple5) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
((triple7 ((((((triple7) -> (rule6 % int4))) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Charlie is rough.
("Charlie" "is" "rough" "+")
int4
((triple7 ((((((triple7) -> (rule6 % int4))) -> (rule2 % int3)) triple5) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Charlie is rough.
("Charlie" "is" "rough" "+")
int4
Anne is green.
True
3
proof
[(((((triple3) -> rule6)) -> rule2))]
("Anne" "is" "green" "+")
((((triple3) -> (rule6 % int2))) -> (rule2 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is not green.
False
3
inv-proof
[(((((triple3) -> rule6)) -> rule2))]
("Anne" "is" "green" "-")
((((triple3) -> (rule6 % int2))) -> (rule2 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is round.
True
4
proof
[(((((((triple3) -> rule6)) -> rule2)) -> rule5))]
("Anne" "is" "round" "+")
((((((triple3) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Anne is not round.
False
4
inv-proof
[(((((((triple3) -> rule6)) -> rule2)) -> rule5))]
("Anne" "is" "round" "-")
((((((triple3) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3
Anne is not kind.
Unknown
inv-random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "-")
Charlie is big.
Unknown
random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "+")
@0: Anne is big.[(triple1)] Anne is red.[(triple2)] Anne is white.[(triple3)] Charlie is green.[(triple4 OR ((((triple7) -> rule6)) -> rule2))] Charlie is kind.[(triple5)] Charlie is round.[(triple6 OR ((triple4) -> rule5) OR ((triple4 triple5) -> rule4) OR ((((((triple7) -> rule6)) -> rule2)) -> rule5) OR ((((((triple7) -> rule6)) -> rule2) triple5) -> rule4))] Charlie is white.[(triple7)] @1: Anne is rough.[(((triple3) -> rule6))] Charlie is red.[(((triple7 triple6) -> rule3) OR ((triple7 ((triple4) -> rule5)) -> rule3) OR ((triple7 ((triple4 triple5) -> rule4)) -> rule3) OR ((triple7 ((((((triple7) -> rule6)) -> rule2)) -> rule5)) -> rule3) OR ((triple7 ((((((triple7) -> rule6)) -> rule2) triple5) -> rule4)) -> rule3))] Charlie is rough.[(((triple7) -> rule6))] @2: Anne is green.[(((((triple3) -> rule6)) -> rule2))] @3: Anne is round.[(((((((triple3) -> rule6)) -> rule2)) -> rule5))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is red.
("Anne" "is" "red" "+")
triple2
Anne is white.
("Anne" "is" "white" "+")
triple3
Charlie is green.
("Charlie" "is" "green" "+")
triple4
((((triple7) -> (rule6 % int2))) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
triple5
Charlie is round.
("Charlie" "is" "round" "+")
triple6
((triple4) -> (rule5 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
((triple4 triple5) -> (rule4 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
((((((triple7) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
((((((triple7) -> (rule6 % int3))) -> (rule2 % int2)) triple5) -> (rule4 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is white.
("Charlie" "is" "white" "+")
triple7
Anne is rough.
("Anne" "is" "rough" "+")
((triple3) -> (rule6 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
((triple7 triple6) -> (rule3 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
((triple7 ((triple4) -> (rule5 % int2))) -> (rule3 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
((triple7 ((triple4 triple5) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
((triple7 ((((((triple7) -> (rule6 % int4))) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Charlie is rough.
("Charlie" "is" "rough" "+")
int4
((triple7 ((((((triple7) -> (rule6 % int4))) -> (rule2 % int3)) triple5) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is green.
("Charlie" "is" "green" "+")
int3
Charlie is rough.
("Charlie" "is" "rough" "+")
int4
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple7) -> (rule6 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
((((triple3) -> (rule6 % int2))) -> (rule2 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Anne is rough.
("Anne" "is" "rough" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
((((((triple3) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
int3