% COMMAND-LINE: --incremental
% EXPECT: invalid
% EXPECT: invalid
% EXPECT: invalid
% EXPECT: invalid
% EXPECT: invalid
% EXPECT: invalid
% EXPECT: invalid
% EXPECT: valid
% EXPECT: invalid
% EXPECT: invalid
% EXPECT: valid
% EXPECT: invalid
% EXPECT: invalid
% EXPECT: invalid
% EXPECT: invalid
% EXPECT: invalid
% EXPECT: invalid
% EXPECT: invalid
% EXPECT: invalid
% EXPECT: invalid
% EXPECT: invalid
% EXPECT: invalid
% EXPECT: invalid
% EXPECT: invalid
% EXPECT: invalid
% EXPECT: invalid
% EXPECT: invalid
% EXPECT: valid
% EXPECT: valid
% EXPECT: valid
A: TYPE;
P_1: BOOLEAN;
P_2: BOOLEAN;
P_3: BOOLEAN;
ASSERT (NOT P_1 OR P_2 OR P_2);
ASSERT (NOT P_1 OR P_2 OR P_3);
P_4: BOOLEAN;
P_5: BOOLEAN;
ASSERT (NOT P_1 OR NOT P_4 OR P_2);
ASSERT (NOT P_1 OR NOT P_5 OR P_2);
P_6: BOOLEAN;
P_7: BOOLEAN;
ASSERT (NOT P_2 OR P_6 OR P_1);
ASSERT (NOT P_2 OR P_7 OR P_1);
P_8: BOOLEAN;
P_9: BOOLEAN;
ASSERT (NOT P_2 OR NOT P_8 OR P_1);
ASSERT (NOT P_2 OR NOT P_9 OR P_1);
P_10: BOOLEAN;
ASSERT (P_2 OR P_1 OR P_4);
ASSERT (P_2 OR P_1 OR P_10);
ASSERT (NOT P_2 OR NOT P_1 OR P_4);
ASSERT (NOT P_2 OR NOT P_1 OR P_10);
P_11: BOOLEAN;
ASSERT (NOT P_6 OR P_2 OR P_1);
ASSERT (NOT P_11 OR P_2 OR P_1);
ASSERT (NOT P_6 OR NOT P_2 OR NOT P_1);
ASSERT (NOT P_11 OR NOT P_2 OR NOT P_1);
PUSH;
QUERY (NOT P_2 OR NOT P_3);
POP;
PUSH;
QUERY (P_1 OR NOT P_3);
POP;
PUSH;
QUERY (NOT P_2 OR P_1);
POP;
PUSH;
QUERY (P_5 OR NOT P_2);
POP;
PUSH;
QUERY (P_1 OR NOT P_2);
POP;
PUSH;
QUERY (P_5 OR P_1);
POP;
PUSH;
QUERY (NOT P_7 OR NOT P_1);
POP;
PUSH;
QUERY (P_2 OR NOT P_1);
POP;
PUSH;
QUERY P_2;
POP;
PUSH;
QUERY (P_9 OR NOT P_1);
POP;
PUSH;
QUERY (P_2 OR NOT P_1);
POP;
PUSH;
QUERY P_2;
POP;
PUSH;
QUERY (NOT P_1 OR NOT P_10);
POP;
PUSH;
QUERY (NOT P_2 OR NOT P_10);
POP;
PUSH;
QUERY (NOT P_1 OR NOT P_2);
POP;
PUSH;
QUERY (P_1 OR NOT P_10);
POP;
PUSH;
QUERY (P_2 OR NOT P_10);
POP;
PUSH;
QUERY (P_1 OR P_2);
POP;
PUSH;
QUERY (NOT P_2 OR NOT P_1);
POP;
PUSH;
QUERY (P_11 OR NOT P_1);
POP;
PUSH;
QUERY (NOT P_2 OR P_11);
POP;
PUSH;
QUERY (P_2 OR P_1);
POP;
PUSH;
QUERY (P_11 OR P_1);
POP;
PUSH;
QUERY (P_2 OR P_11);
POP;
P_12: BOOLEAN;
ASSERT (NOT P_12 OR P_2);
ASSERT (NOT P_12 OR P_3);
ASSERT (P_12 OR NOT P_1 OR P_2);
ASSERT (P_12 OR NOT P_1 OR P_2);
P_13: BOOLEAN;
ASSERT (NOT P_13 OR NOT P_4);
ASSERT (NOT P_13 OR NOT P_5);
ASSERT (P_13 OR NOT P_1 OR P_2);
ASSERT (P_13 OR NOT P_1 OR P_2);
ASSERT (NOT P_2 OR P_1);
ASSERT (NOT P_2 OR P_1);
ASSERT (NOT P_2 OR P_1);
ASSERT (NOT P_2 OR P_1);
P_14: BOOLEAN;
ASSERT (P_14 OR P_2 OR P_1);
ASSERT (P_14 OR P_2 OR P_1);
ASSERT (NOT P_14 OR P_4);
ASSERT (NOT P_14 OR P_10);
ASSERT (P_14 OR NOT P_2 OR NOT P_1);
ASSERT (P_14 OR NOT P_2 OR NOT P_1);
P_15: BOOLEAN;
ASSERT (P_15 OR P_2 OR P_1);
ASSERT (P_15 OR P_2 OR P_1);
ASSERT (NOT P_15 OR NOT P_6);
ASSERT (NOT P_15 OR NOT P_11);
ASSERT (P_15 OR NOT P_2 OR NOT P_1);
ASSERT (P_15 OR NOT P_2 OR NOT P_1);
PUSH;
QUERY NOT P_3;
POP;
PUSH;
QUERY P_12;
POP;
PUSH;
QUERY P_11;
POP;
PUSH;
QUERY P_15;
POP;
ASSERT NOT P_15;
ASSERT NOT P_15;
PUSH;
QUERY NOT P_10;
POP;
PUSH;
QUERY FALSE;
% EXIT: 20