% Running in auto input_syntax mode. Trying TPTP
% SZS status Satisfiable for tptp_25
% # SZS output start Saturation.
cnf(u1445,axiom,
    x2_s_16(sK7)).

cnf(u1448,axiom,
    ~x2_e_16(sK7)).

cnf(u1453,axiom,
    ~x2_s_15(sK8)).

cnf(u1458,axiom,
    x2_e_15(sK8)).

cnf(u1466,axiom,
    l_s_0(sK9)).

cnf(u1477,axiom,
    ~a_accepted(X3)).

cnf(u1480,axiom,
    ~a_accepted(sK10)).

cnf(u1486,axiom,
    tau_3(sK11)).

cnf(u1499,axiom,
    a2_e_1(sK12)).

cnf(u1514,axiom,
    a_approved(sK16)).

cnf(u1518,axiom,
    ~tau_9(sK17)).

cnf(u1523,axiom,
    ~tau_9(X2)).

cnf(u1532,axiom,
    x2_e_6(sK18)).

cnf(u1540,axiom,
    ~tau_7(X0)).

cnf(u1544,axiom,
    ~tau_5(X0)).

cnf(u1552,axiom,
    ~a_finalized(X0)).

cnf(u1556,axiom,
    x2_e_5(sK20)).

cnf(u1568,axiom,
    o_sent(sK21)).

cnf(u1583,axiom,
    ~tau_19(X1)).

cnf(u1600,axiom,
    ~a_activated(X3)).

cnf(u1603,axiom,
    ~a_activated(sK25)).

cnf(u1609,axiom,
    tau_10(sK26)).

cnf(u1621,axiom,
    ~o_accepted(X3)).

cnf(u1624,axiom,
    ~o_accepted(sK27)).

cnf(u1630,axiom,
    tau_11(sK28)).

cnf(u1647,axiom,
    a2_e_3(sK29)).

cnf(u1651,axiom,
    ~x2_s_14(sK30)).

cnf(u1656,axiom,
    x2_e_14(sK30)).

cnf(u1661,axiom,
    x2_s_13(sK31)).

cnf(u1669,axiom,
    ~x2_s_12(sK32)).

cnf(u1674,axiom,
    x2_e_12(sK32)).

cnf(u1682,axiom,
    a4_e_2(sK34)).

cnf(u1687,axiom,
    ~w_nabellen_incomplete_dossiers(X0)).

cnf(u1691,axiom,
    x2_e_11(sK35)).

cnf(u1701,axiom,
    x2_s_3(sK37)).

cnf(u1713,axiom,
    x2_e_4(sK38)).

cnf(u1721,axiom,
    ~tau_4(X0)).

cnf(u1729,axiom,
    w_valideren_aanvraag(sK39)).

cnf(u1737,axiom,
    x2_e_15(sK40)).

cnf(u1741,axiom,
    ~tau_12(X0)).

cnf(u1745,axiom,
    ~x2_s_10(sK41)).

cnf(u1750,axiom,
    x2_e_10(sK41)).

cnf(u1758,axiom,
    a2_e_0(sK42)).

cnf(u1777,axiom,
    a2_e_0(sK43)).

cnf(u1790,axiom,
    ~tau_0(X2)).

cnf(u1800,axiom,
    x2_e_16(sK45)).

cnf(u1805,axiom,
    ~tau_13(X0)).

cnf(u1813,axiom,
    a4_e_2(sK46)).

cnf(u1818,axiom,
    ~tau_15(X0)).

cnf(u1834,axiom,
    x2_s_6(sK49)).

cnf(u1843,axiom,
    x2_e_12(sK50)).

cnf(u1849,axiom,
    x2_e_1(sK51)).

cnf(u1859,axiom,
    ~tau_14(X1)).

cnf(u1871,axiom,
    ~a2_s_1(sK55)).

cnf(u1876,axiom,
    a2_e_1(sK55)).

cnf(u1885,axiom,
    x3_s_0(sK56)).

cnf(u1888,axiom,
    ~x2_e_1(sK56)).

cnf(u1897,axiom,
    a_registered(sK57)).

cnf(u1909,axiom,
    x2_e_13(sK61)).

cnf(u1914,axiom,
    ~tau_2(X0)).

cnf(u1925,axiom,
    ~l_s_5(sK65)).

cnf(u1930,axiom,
    w_valideren_aanvraag(sK65)).

cnf(u1935,axiom,
    ~tau_13(sK66)).

cnf(u1957,axiom,
    a2_e_3(sK69)).

cnf(u1963,axiom,
    x2_s_3(sK70)).

cnf(u1972,axiom,
    x2_s_2(sK71)).

cnf(u1985,axiom,
    ~tau_17(X0)).

cnf(u1997,axiom,
    x2_e_17(sK74)).

cnf(u2005,axiom,
    ~tau_16(X0)).

cnf(u2013,axiom,
    l_s_3(sK77)).

cnf(u2016,axiom,
    ~x2_e_17(sK77)).

cnf(u2028,axiom,
    ~x2_s_11(sK78)).

cnf(u2033,axiom,
    x2_e_11(sK78)).

cnf(u2045,axiom,
    x2_e_2(sK80)).

cnf(u2053,axiom,
    ~tau_1(X0)).

cnf(u2057,axiom,
    ~a_preaccepted(X0)).

cnf(u2061,axiom,
    x3_e_0(sK81)).

cnf(u2069,axiom,
    ~w_afhandelen_leads(X0)).

cnf(u2077,axiom,
    a2_e_3(sK82)).

cnf(u2090,axiom,
    x2_e_17(sK83)).

cnf(u2102,axiom,
    x2_e_7(sK84)).

cnf(u2107,axiom,
    ~a_cancelled(X0)).

cnf(u2112,axiom,
    x2_s_6(sK85)).

cnf(u2115,axiom,
    ~x2_e_6(sK85)).

cnf(u2142,axiom,
    ~a_declined(X0)).

cnf(u2146,axiom,
    x3_e_9(sK89)).

cnf(u2150,axiom,
    ~o_declined(X0)).

cnf(u2163,axiom,
    a_partlysubmitted(sK90)).

cnf(u2168,axiom,
    ~sP1).

cnf(u2180,axiom,
    ~sP0).

cnf(u2194,axiom,
    x2_s_10(sK93)).

cnf(u2197,axiom,
    ~x2_e_11(sK93)).

cnf(u2205,axiom,
    ~l_s_6(sK94)).

cnf(u2210,axiom,
    w_wijzigen_contractgegevens(sK94)).

cnf(u2215,axiom,
    ~tau_16(sK95)).

cnf(u2224,axiom,
    l_s_2(sK99)).

cnf(u2227,axiom,
    ~o_selected(sK99)).

cnf(u2242,axiom,
    x2_s_5(sK101)).

cnf(u2250,axiom,
    sP3).

cnf(u2256,axiom,
    w_beoordelen_fraude(sK102)).

cnf(u2262,axiom,
    ~sP2).

cnf(u2283,axiom,
    a4_e_2(sK105)).

cnf(u2288,axiom,
    ~o_cancelled(X0)).

cnf(u2292,axiom,
    x3_e_8(sK106)).

cnf(u2296,axiom,
    ~w_nabellen_offertes(X0)).

cnf(u2316,axiom,
    x3_s_0(sK109)).

cnf(u2325,axiom,
    x3_s_9(sK110)).

cnf(u2328,axiom,
    ~x3_e_9(sK110)).

cnf(u2333,axiom,
    ~tau_18(X0)).

cnf(u2349,axiom,
    a4_e_2(sK113)).

cnf(u2354,axiom,
    ~x3_s_8(sK114)).

cnf(u2359,axiom,
    x3_e_8(sK114)).

cnf(u2367,axiom,
    x2_s_5(sK115)).

cnf(u2376,axiom,
    x2_s_4(sK116)).

cnf(u2388,axiom,
    x2_s_17(sK118)).

cnf(u2401,axiom,
    x2_e_14(sK122)).

cnf(u2407,axiom,
    l_s_1(sK124)).

cnf(u2416,axiom,
    ~tau_1(sK125)).

cnf(u2428,axiom,
    o_sent_back(sK126)).

cnf(u2437,axiom,
    ~tau_8(X2)).

cnf(u2452,axiom,
    w_completeren_aanvraag(sK130)).

cnf(u2464,axiom,
    x2_e_1(sK133)).

cnf(u2499,axiom,
    a2_e_1(sK140)).

cnf(u2508,axiom,
    a2_e_0(sK141)).

cnf(u2514,axiom,
    x2_e_3(sK142)).

cnf(u2528,axiom,
    a4_s_2(sK144)).

cnf(u2546,axiom,
    tau_6(sK146)).

cnf(u2553,axiom,
    ~sP5).

cnf(u2565,axiom,
    ~sP4).

cnf(u2583,axiom,
    x3_e_9(sK149)).

cnf(u2588,axiom,
    o_selected(sK150)).

cnf(u2593,axiom,
    w_wijzigen_contractgegevens(sK151)).

cnf(u2598,axiom,
    x2_s_7(sK152)).

cnf(u2615,axiom,
    ~o_created(sK154)).

cnf(u2620,axiom,
    o_sent(sK154)).

cnf(u2625,axiom,
    ~a_cancelled(sK155)).

cnf(u2634,axiom,
    x2_e_10(sK156)).

cnf(u3117,axiom,
    ~x2_s_17(sK151)).

cnf(u3062,axiom,
    ~l_s_0(sK133)).

cnf(u1025,axiom,
    ~x2_e_11(X0) | ~w_nabellen_incomplete_dossiers(X0)).

cnf(u2975,axiom,
    ~x2_s_7(sK154)).

cnf(u1194,axiom,
    ~tau_13(X0) | ~w_valideren_aanvraag(X0)).

cnf(u2910,axiom,
    ~x2_s_3(sK136)).

cnf(u1088,axiom,
    ~a2_s_0(X0) | ~x2_e_1(X0)).

cnf(u1015,axiom,
    ~x2_e_7(X0) | ~x2_s_7(X0)).

cnf(u3114,axiom,
    ~a_approved(sK50)).

cnf(u3069,axiom,
    ~x2_e_5(sK86)).

cnf(u1225,axiom,
    ~x2_s_12(X0) | ~a4_s_2(X0)).

cnf(u1281,axiom,
    x2_s_15(sK112)).

cnf(u2970,axiom,
    ~x2_e_2(sK59)).

cnf(u2806,axiom,
    ~x2_e_15(sK82)).

cnf(u2892,axiom,
    ~x2_s_5(sK12)).

cnf(u1356,axiom,
    ~x2_e_3(X0) | ~tau_3(X0)).

cnf(u1311,axiom,
    ~x2_e_1(X0) | ~l_s_0(X0)).

cnf(u1202,axiom,
    ~tau_4(X0) | ~x2_s_4(X0)).

cnf(u2812,axiom,
    ~x2_e_16(sK82)).

cnf(u2818,axiom,
    ~x2_s_3(sK140)).

cnf(u2917,axiom,
    ~x2_s_7(sK49)).

cnf(u2868,axiom,
    ~x2_e_4(sK96)).

cnf(u1304,axiom,
    ~a_submitted(X0) | ~a_partlysubmitted(X0)).

cnf(u1037,axiom,
    ~x2_s_10(X0) | ~o_declined(X0)).

cnf(u1096,axiom,
    ~x2_s_6(X0) | ~x2_s_7(X0)).

cnf(u2977,axiom,
    ~x2_s_14(sK122)).

cnf(u1023,axiom,
    ~o_accepted(X0) | ~tau_11(X0)).

cnf(u2928,axiom,
    ~x2_e_12(sK34)).

cnf(u2891,axiom,
    ~x2_e_4(sK140)).

cnf(u1289,axiom,
    a2_s_3(sK117)).

cnf(u1051,axiom,
    x2_s_10(sK54)).

cnf(u1233,axiom,
    x2_s_3(sK98)).

cnf(u1355,axiom,
    ~a_submitted(X0) | ~x2_e_1(X0)).

cnf(u1364,axiom,
    o_created(sK139)).

cnf(u1349,axiom,
    ~tau_14(X0) | ~l_s_5(X0)).

cnf(u1018,axiom,
    ~w_nabellen_incomplete_dossiers(X0) | ~x2_s_11(X0)).

cnf(u989,axiom,
    ~a_approved(X0) | ~x2_s_12(X0)).

cnf(u940,axiom,
    ~x2_e_3(X0) | ~a2_e_1(X0)).

cnf(u2943,axiom,
    ~x2_s_14(sK113)).

cnf(u1034,axiom,
    ~x2_s_1(X0) | ~tau_0(X0)).

cnf(u1363,axiom,
    ~x3_e_8(X0) | ~x2_e_17(X0)).

cnf(u2878,axiom,
    ~x2_s_16(sK129)).

cnf(u3105,axiom,
    ~a4_s_2(sK22)).

cnf(u1056,axiom,
    ~x2_e_10(X0) | ~x2_s_10(X0)).

cnf(u2948,axiom,
    ~a2_s_3(sK34)).

cnf(u3032,axiom,
    ~x2_s_10(sK126)).

cnf(u1302,axiom,
    ~tau_18(X0) | ~x2_s_6(X0)).

cnf(u1245,axiom,
    ~w_wijzigen_contractgegevens(X0) | ~x2_e_17(X0)).

cnf(u1193,axiom,
    ~tau_13(X0) | ~l_s_5(X0)).

cnf(u939,axiom,
    ~a2_e_1(X0) | ~x2_s_3(X0)).

cnf(u2938,axiom,
    ~x2_e_13(sK105)).

cnf(u2909,axiom,
    ~x2_e_2(sK136)).

cnf(u2860,axiom,
    ~x2_e_6(sK49)).

cnf(u3008,axiom,
    ~a4_s_2(sK78)).

cnf(u1042,axiom,
    ~w_valideren_aanvraag(X0) | ~x2_s_16(X0)).

cnf(u3033,axiom,
    ~x3_s_9(sK54)).

cnf(u1116,axiom,
    ~x2_s_1(X0) | ~x3_e_0(X0)).

cnf(u2947,axiom,
    ~x2_e_14(sK113)).

cnf(u1064,axiom,
    ~a2_e_1(X0) | ~x2_s_5(X0)).

cnf(u2817,axiom,
    ~x2_s_3(sK55)).

cnf(u1310,axiom,
    ~x3_s_0(X0) | ~l_s_0(X0)).

cnf(u2859,axiom,
    ~x2_e_6(sK121)).

cnf(u3023,axiom,
    ~a2_s_3(sK144)).

cnf(u1332,axiom,
    ~l_s_3(X0) | ~x2_e_5(X0)).

cnf(u1242,axiom,
    ~tau_19(X0) | ~l_s_0(X0)).

cnf(u1267,axiom,
    ~x2_s_10(X0) | ~x3_s_9(X0)).

cnf(u2999,axiom,
    ~tau_11(sK30)).

cnf(u2958,axiom,
    ~x3_e_0(sK123)).

cnf(u1103,axiom,
    ~o_selected(X0) | ~tau_5(X0)).

cnf(u3080,axiom,
    ~l_s_0(sK63)).

cnf(u2870,axiom,
    ~x2_e_4(sK150)).

cnf(u2813,axiom,
    ~x2_s_3(sK142)).

cnf(u3068,axiom,
    ~x2_s_5(sK77)).

cnf(u1359,axiom,
    ~w_completeren_aanvraag(X0) | ~l_s_1(X0)).

cnf(u1331,axiom,
    ~l_s_3(X0) | ~x2_s_5(X0)).

cnf(u3018,axiom,
    ~a4_s_2(sK61)).

cnf(u1076,axiom,
    a_submitted(sK63)).

cnf(u2994,axiom,
    ~a2_s_1(sK74)).

cnf(u2965,axiom,
    ~a_partlysubmitted(sK76)).

cnf(u2916,axiom,
    ~x2_s_7(sK121)).

cnf(u3000,axiom,
    ~tau_11(sK122)).

cnf(u1272,axiom,
    ~a2_s_0(X0) | ~tau_0(X0)).

cnf(u1033,axiom,
    ~o_selected(X0) | ~x2_e_4(X0)).

cnf(u1062,axiom,
    ~a2_e_1(X0) | ~x2_s_4(X0)).

cnf(u3025,axiom,
    ~a2_e_3(sK144)).

cnf(u3067,axiom,
    ~x2_s_5(sK86)).

cnf(u3001,axiom,
    ~l_s_4(sK106)).

cnf(u2915,axiom,
    ~x2_e_1(sK141)).

cnf(u1084,axiom,
    ~a2_s_0(X0) | ~a2_e_1(X0)).

cnf(u1063,axiom,
    ~a2_e_1(X0) | ~x2_e_4(X0)).

cnf(u1412,axiom,
    ~a_accepted(X0) | ~tau_3(X0)).

cnf(u1290,axiom,
    ~a_registered(X0) | ~x2_s_15(X0)).

cnf(u2991,axiom,
    ~x2_s_4(sK36)).

cnf(u2950,axiom,
    ~a2_s_3(sK105)).

cnf(u1107,axiom,
    ~a4_e_2(X0) | ~x2_e_13(X0)).

cnf(u1312,axiom,
    ~w_nabellen_incomplete_dossiers(X0) | ~a4_s_2(X0)).

cnf(u2926,axiom,
    ~x2_s_12(sK105)).

cnf(u2839,axiom,
    ~x2_e_11(sK156)).

cnf(u1071,axiom,
    ~o_cancelled(X0) | ~l_s_4(X0)).

cnf(u1411,axiom,
    ~w_wijzigen_contractgegevens(X0) | ~x2_s_17(X0)).

cnf(u1104,axiom,
    ~a4_e_2(X0) | ~x2_s_12(X0)).

cnf(u990,axiom,
    ~x2_s_10(X0) | ~x2_s_11(X0)).

cnf(u1298,axiom,
    ~tau_8(X0) | ~x2_e_10(X0)).

cnf(u1241,axiom,
    ~tau_16(X0) | ~x2_e_17(X0)).

cnf(u1297,axiom,
    x2_s_16(sK119)).

cnf(u2986,axiom,
    ~x2_e_7(sK21)).

cnf(u2957,axiom,
    ~x3_s_0(sK123)).

cnf(u2908,axiom,
    ~x2_s_2(sK136)).

cnf(u1270,axiom,
    ~x2_e_13(X0) | ~tau_10(X0)).

cnf(u3079,axiom,
    ~x2_s_14(sK28)).

cnf(u1327,axiom,
    ~w_valideren_aanvraag(X0) | ~x2_e_16(X0)).

cnf(u2933,axiom,
    ~x2_s_13(sK46)).

cnf(u2834,axiom,
    ~x2_s_11(sK156)).

cnf(u1271,axiom,
    ~a_activated(X0) | ~tau_10(X0)).

cnf(u1164,axiom,
    ~tau_16(X0) | ~w_wijzigen_contractgegevens(X0)).

cnf(u1358,axiom,
    ~x2_e_11(X0) | ~x2_s_11(X0)).

cnf(u1357,axiom,
    ~tau_8(X0) | ~x2_s_10(X0)).

cnf(u998,axiom,
    ~a_preaccepted(X0) | ~w_afhandelen_leads(X0)).

cnf(u2993,axiom,
    ~x2_s_5(sK36)).

cnf(u2816,axiom,
    ~x2_s_3(sK12)).

cnf(u1305,axiom,
    x3_s_0(sK120)).

cnf(u1067,axiom,
    x2_s_7(sK60)).

cnf(u2841,axiom,
    ~x2_s_2(sK42)).

cnf(u1380,axiom,
    ~x2_s_1(X0) | ~x2_e_1(X0)).

cnf(u1335,axiom,
    ~x2_e_13(X0) | ~a_activated(X0)).

cnf(u1279,axiom,
    ~x2_e_6(X0) | ~x2_e_7(X0)).

cnf(u1061,axiom,
    l_s_1(sK59)).

cnf(u1005,axiom,
    ~a2_e_0(X0) | ~a2_e_1(X0)).

cnf(u2831,axiom,
    ~x2_s_11(sK54)).

cnf(u2918,axiom,
    ~x2_s_7(sK85)).

cnf(u1075,axiom,
    ~l_s_3(X0) | ~x2_e_17(X0)).

cnf(u1379,axiom,
    ~x3_e_0(X0) | ~w_afhandelen_leads(X0)).

cnf(u1124,axiom,
    ~w_completeren_aanvraag(X0) | ~x2_e_2(X0)).

cnf(u3013,axiom,
    ~a4_s_2(sK75)).

cnf(u1072,axiom,
    ~o_cancelled(X0) | ~x3_e_9(X0)).

cnf(u3121,axiom,
    ~x2_s_6(sK83)).

cnf(u3048,axiom,
    ~x2_s_15(sK57)).

cnf(u1261,axiom,
    ~x2_e_3(X0) | ~a_accepted(X0)).

cnf(u2826,axiom,
    ~x2_s_15(sK40)).

cnf(u2925,axiom,
    ~x2_s_12(sK46)).

cnf(u2811,axiom,
    ~x2_e_16(sK69)).

cnf(u1110,axiom,
    ~a4_e_2(X0) | ~a2_s_3(X0)).

cnf(u3024,axiom,
    ~a2_e_3(sK13)).

cnf(u1340,axiom,
    ~l_s_1(X0) | ~x2_s_2(X0)).

cnf(u1111,axiom,
    ~a4_e_2(X0) | ~a2_e_3(X0)).

cnf(u3049,axiom,
    ~a2_s_3(sK112)).

cnf(u3077,axiom,
    ~x2_s_2(sK124)).

cnf(u2963,axiom,
    ~x2_e_1(sK81)).

cnf(u1415,axiom,
    ~x3_s_8(X0) | ~x2_e_6(X0)).

cnf(u1080,axiom,
    ~tau_4(X0) | ~o_selected(X0)).

cnf(u1408,axiom,
    ~x2_e_12(X0) | ~a_approved(X0)).

cnf(u3063,axiom,
    ~x2_e_16(sK129)).

cnf(u1326,axiom,
    ~l_s_5(X0) | ~x2_e_16(X0)).

cnf(u2833,axiom,
    ~x2_s_11(sK41)).

cnf(u1269,axiom,
    ~x2_e_2(X0) | ~x2_s_2(X0)).

cnf(u3091,axiom,
    ~x2_e_17(sK114)).

cnf(u1089,axiom,
    ~a2_e_0(X0) | ~x2_e_1(X0)).

cnf(u1339,axiom,
    ~tau_4(X0) | ~x2_e_4(X0)).

cnf(u1258,axiom,
    ~tau_19(X0) | ~x2_e_1(X0)).

cnf(u1360,axiom,
    ~x3_s_8(X0) | ~x2_s_17(X0)).

cnf(u2974,axiom,
    ~x2_s_7(sK21)).

cnf(u2887,axiom,
    ~x2_s_4(sK55)).

cnf(u1119,axiom,
    ~a_approved(X0) | ~tau_9(X0)).

cnf(u1152,axiom,
    x2_s_4(sK79)).

cnf(u1041,axiom,
    ~l_s_5(X0) | ~x2_s_16(X0)).

cnf(u1333,axiom,
    ~x2_e_17(X0) | ~x2_s_5(X0)).

cnf(u3074,axiom,
    ~x2_e_5(sK83)).

cnf(u1345,axiom,
    ~tau_11(X0) | ~x2_s_14(X0)).

cnf(u3034,axiom,
    ~x3_s_9(sK93)).

cnf(u2956,axiom,
    ~x3_s_0(sK81)).

cnf(u1266,axiom,
    ~o_sent_back(X0) | ~x2_s_10(X0)).

cnf(u2981,axiom,
    ~x3_e_9(sK54)).

cnf(u2932,axiom,
    ~x2_s_13(sK34)).

cnf(u2802,axiom,
    ~x2_s_15(sK69)).

cnf(u2888,axiom,
    ~x2_s_4(sK140)).

cnf(u3072,axiom,
    ~x2_s_5(sK83)).

cnf(u1160,axiom,
    ~o_sent_back(X0) | ~x2_e_10(X0)).

cnf(u1078,axiom,
    ~x3_s_8(X0) | ~x3_e_9(X0)).

cnf(u2992,axiom,
    ~x2_e_4(sK36)).

cnf(u2955,axiom,
    ~a2_e_3(sK113)).

cnf(u1115,axiom,
    ~x2_s_1(X0) | ~x3_s_0(X0)).

cnf(u1419,axiom,
    ~w_valideren_aanvraag(X0) | ~l_s_5(X0)).

cnf(u1079,axiom,
    ~l_s_2(X0) | ~tau_4(X0)).

cnf(u2889,axiom,
    ~x2_e_4(sK12)).

cnf(u2840,axiom,
    ~w_beoordelen_fraude(sK81)).

cnf(u2931,axiom,
    ~x2_e_12(sK113)).

cnf(u3086,axiom,
    ~x2_s_17(sK48)).

cnf(u1413,axiom,
    ~a_declined(X0) | ~x3_s_9(X0)).

cnf(u1278,axiom,
    ~x2_e_6(X0) | ~x2_s_7(X0)).

cnf(u1220,axiom,
    l_s_2(sK96)).

cnf(u1109,axiom,
    ~a4_e_2(X0) | ~x2_e_14(X0)).

cnf(u3007,axiom,
    ~a4_s_2(sK35)).

cnf(u1004,axiom,
    ~a2_e_0(X0) | ~x2_s_3(X0)).

cnf(u1306,axiom,
    x2_s_6(sK121)).

cnf(u2966,axiom,
    ~a_partlysubmitted(sK9)).

cnf(u3108,axiom,
    ~x2_s_11(sK105)).

cnf(u1098,axiom,
    ~x2_e_6(X0) | ~tau_7(X0)).

cnf(u1123,axiom,
    ~l_s_1(X0) | ~x2_e_2(X0)).

cnf(u2942,axiom,
    ~x2_s_14(sK105)).

cnf(u1087,axiom,
    ~a_preaccepted(X0) | ~x3_s_0(X0)).

cnf(u2855,axiom,
    ~x2_s_17(sK83)).

cnf(u1328,axiom,
    l_s_5(sK129)).

cnf(u1120,axiom,
    ~l_s_0(X0) | ~a_partlysubmitted(X0)).

cnf(u3012,axiom,
    ~a2_e_0(sK123)).

cnf(u919,axiom,
    ~x3_e_9(X0) | ~o_declined(X0)).

cnf(u1313,axiom,
    ~w_nabellen_incomplete_dossiers(X0) | ~a4_e_2(X0)).

cnf(u3002,axiom,
    ~l_s_4(sK114)).

cnf(u1257,axiom,
    ~tau_19(X0) | ~x3_s_0(X0)).

cnf(u1003,axiom,
    ~a2_e_0(X0) | ~x2_e_2(X0)).

cnf(u2973,axiom,
    ~x2_s_7(sK139)).

cnf(u2924,axiom,
    ~x2_s_12(sK34)).

cnf(u1314,axiom,
    x2_s_1(sK123)).

cnf(u3095,axiom,
    ~x2_s_13(sK61)).

cnf(u1388,axiom,
    ~l_s_4(X0) | ~x3_e_9(X0)).

cnf(u1106,axiom,
    ~a4_e_2(X0) | ~x2_s_13(X0)).

cnf(u2850,axiom,
    ~a2_e_1(sK42)).

cnf(u1159,axiom,
    ~o_accepted(X0) | ~x2_s_14(X0)).

cnf(u1336,axiom,
    x2_s_2(sK131)).

cnf(u1180,axiom,
    ~x3_e_8(X0) | ~o_cancelled(X0)).

cnf(u2807,axiom,
    ~x2_s_16(sK29)).

cnf(u3011,axiom,
    ~x2_s_1(sK136)).

cnf(u1128,axiom,
    ~tau_16(X0) | ~x2_s_17(X0)).

cnf(u927,axiom,
    ~a2_e_3(X0) | ~x2_s_15(X0)).

cnf(u2881,axiom,
    ~x2_s_4(sK38)).

cnf(u2832,axiom,
    ~x2_s_11(sK93)).

cnf(u1083,axiom,
    ~a2_s_0(X0) | ~x2_s_3(X0)).

cnf(u3078,axiom,
    ~x2_s_2(sK130)).

cnf(u1387,axiom,
    ~l_s_4(X0) | ~x3_s_9(X0)).

cnf(u2857,axiom,
    ~x2_s_4(sK99)).

cnf(u1396,axiom,
    ~l_s_2(X0) | ~o_selected(X0)).

cnf(u3022,axiom,
    ~a2_s_3(sK13)).

cnf(u1167,axiom,
    ~tau_13(X0) | ~x2_e_16(X0)).

cnf(u3100,axiom,
    ~x3_s_9(sK15)).

cnf(u1077,axiom,
    ~x3_s_8(X0) | ~l_s_4(X0)).

cnf(u1021,axiom,
    ~l_s_2(X0) | ~x2_s_4(X0)).

cnf(u1118,axiom,
    ~x3_e_0(X0) | ~x2_e_1(X0)).

cnf(u2847,axiom,
    ~x2_s_3(sK42)).

cnf(u2934,axiom,
    ~x2_s_13(sK105)).

cnf(u1066,axiom,
    ~w_beoordelen_fraude(X0) | ~x3_s_0(X0)).

cnf(u1423,axiom,
    ~tau_9(X0) | ~x2_s_12(X0)).

cnf(u3087,axiom,
    ~x2_s_17(sK106)).

cnf(u1395,axiom,
    ~a4_e_2(X0) | ~x2_s_11(X0)).

cnf(u1140,axiom,
    ~tau_1(X0) | ~x2_s_2(X0)).

cnf(u3058,axiom,
    ~l_s_0(sK120)).

cnf(u3029,axiom,
    ~x2_e_17(sK151)).

cnf(u2809,axiom,
    ~x2_s_16(sK82)).

cnf(u1416,axiom,
    ~x2_e_17(X0) | ~x2_s_6(X0)).

cnf(u3064,axiom,
    ~x2_e_16(sK39)).

cnf(u929,axiom,
    ~a2_e_3(X0) | ~x2_s_16(X0)).

cnf(u1334,axiom,
    ~x2_e_17(X0) | ~x2_e_5(X0)).

cnf(u2842,axiom,
    ~x2_s_2(sK43)).

cnf(u2941,axiom,
    ~x2_s_14(sK46)).

cnf(u1097,axiom,
    ~x2_s_6(X0) | ~x2_e_7(X0)).

cnf(u1126,axiom,
    ~tau_15(X0) | ~x3_s_9(X0)).

cnf(u1074,axiom,
    ~l_s_3(X0) | ~x2_s_6(X0)).

cnf(u1163,axiom,
    ~tau_16(X0) | ~l_s_6(X0)).

cnf(u1127,axiom,
    ~tau_15(X0) | ~x3_e_9(X0)).

cnf(u3065,axiom,
    ~x2_e_16(sK65)).

cnf(u3093,axiom,
    ~x2_s_12(sK50)).

cnf(u1341,axiom,
    ~w_completeren_aanvraag(X0) | ~x2_s_2(X0)).

cnf(u2951,axiom,
    ~a2_s_3(sK113)).

cnf(u2808,axiom,
    ~x2_s_16(sK69)).

cnf(u1424,axiom,
    ~w_completeren_aanvraag(X0) | ~tau_2(X0)).

cnf(u2849,axiom,
    ~x2_s_3(sK141)).

cnf(u1342,axiom,
    ~a_finalized(X0) | ~tau_6(X0)).

cnf(u3107,axiom,
    ~x2_s_11(sK46)).

cnf(u1354,axiom,
    ~a_submitted(X0) | ~l_s_0(X0)).

cnf(u1105,axiom,
    ~a4_e_2(X0) | ~x2_e_12(X0)).

cnf(u3014,axiom,
    ~a4_s_2(sK32)).

cnf(u3083,axiom,
    ~x2_s_11(sK35)).

cnf(u1135,axiom,
    ~a_preaccepted(X0) | ~x3_e_0(X0)).

cnf(u1168,axiom,
    ~x3_e_8(X0) | ~x3_s_8(X0)).

cnf(u3090,axiom,
    ~x2_e_17(sK106)).

cnf(u1414,axiom,
    ~x3_s_8(X0) | ~x2_s_6(X0)).

cnf(u1362,axiom,
    ~x3_s_8(X0) | ~x2_e_17(X0)).

cnf(u1361,axiom,
    ~x3_e_8(X0) | ~x2_s_17(X0)).

cnf(u960,axiom,
    ~a_accepted(X0) | ~x2_s_3(X0)).

cnf(u3050,axiom,
    ~a2_s_3(sK8)).

cnf(u3021,axiom,
    ~a4_s_2(sK122)).

cnf(u2972,axiom,
    ~x2_e_2(sK130)).

cnf(u1422,axiom,
    ~a_cancelled(X0) | ~x2_s_7(X0)).

cnf(u1391,axiom,
    ~tau_2(X0) | ~l_s_1(X0)).

cnf(u1421,axiom,
    ~tau_13(X0) | ~x2_s_16(X0)).

cnf(u3088,axiom,
    ~x2_s_17(sK114)).

cnf(u1228,axiom,
    ~x2_e_13(X0) | ~a4_s_2(X0)).

cnf(u1117,axiom,
    ~x3_s_0(X0) | ~x2_e_1(X0)).

cnf(u2904,axiom,
    ~l_s_4(sK48)).

cnf(u1369,axiom,
    ~x2_e_12(X0) | ~x2_s_12(X0)).

cnf(u1176,axiom,
    ~a2_s_1(X0) | ~x2_s_5(X0)).

cnf(u1065,axiom,
    ~x2_e_17(X0) | ~a2_e_1(X0)).

cnf(u975,axiom,
    x2_s_14(sK33)).

cnf(u3057,axiom,
    ~x2_s_3(sK11)).

cnf(u2880,axiom,
    ~x2_s_16(sK65)).

cnf(u2971,axiom,
    ~x2_e_2(sK124)).

cnf(u2905,axiom,
    ~x3_e_9(sK48)).

cnf(u2856,axiom,
    ~x2_s_4(sK96)).

cnf(u2819,axiom,
    ~a2_e_1(sK142)).

cnf(u969,axiom,
    ~x2_e_15(X0) | ~x2_s_15(X0)).

cnf(u970,axiom,
    ~o_cancelled(X0) | ~w_nabellen_offertes(X0)).

cnf(u2895,axiom,
    ~a2_e_1(sK74)).

cnf(u1020,axiom,
    ~a_finalized(X0) | ~x2_s_5(X0)).

cnf(u983,axiom,
    a2_s_1(sK36)).

cnf(u2982,axiom,
    ~x3_e_9(sK93)).

cnf(u3124,axiom,
    ~l_s_5(sK39)).

cnf(u1114,axiom,
    ~x3_e_0(X0) | ~x3_s_0(X0)).

cnf(u1139,axiom,
    l_s_0(sK76)).

cnf(u2830,axiom,
    ~x2_s_12(sK16)).

cnf(u3081,axiom,
    ~x2_e_1(sK63)).

cnf(u1329,axiom,
    ~tau_6(X0) | ~x2_s_5(X0)).

cnf(u3028,axiom,
    ~x2_e_17(sK94)).

cnf(u1136,axiom,
    x2_s_12(sK75)).

cnf(u1273,axiom,
    ~a2_e_0(X0) | ~tau_0(X0)).

cnf(u935,axiom,
    ~tau_12(X0) | ~x2_s_15(X0)).

cnf(u1022,axiom,
    ~o_selected(X0) | ~x2_s_4(X0)).

cnf(u977,axiom,
    ~x2_e_14(X0) | ~o_accepted(X0)).

cnf(u928,axiom,
    ~a2_e_3(X0) | ~x2_e_15(X0)).

cnf(u1019,axiom,
    ~x2_e_17(X0) | ~x2_s_17(X0)).

cnf(u2890,axiom,
    ~x2_e_4(sK55)).

cnf(u2989,axiom,
    ~x3_s_8(sK106)).

cnf(u2940,axiom,
    ~x2_s_14(sK34)).

cnf(u1174,axiom,
    ~a2_s_1(X0) | ~x2_s_4(X0)).

cnf(u2810,axiom,
    ~x2_e_16(sK29)).

cnf(u1122,axiom,
    ~a_registered(X0) | ~x2_e_15(X0)).

cnf(u2866,axiom,
    ~x2_s_5(sK20)).

cnf(u1390,axiom,
    ~a_cancelled(X0) | ~o_sent(X0)).

cnf(u1175,axiom,
    ~a2_s_1(X0) | ~x2_e_4(X0)).

cnf(u3027,axiom,
    ~x2_e_17(sK97)).

cnf(u1085,axiom,
    ~tau_14(X0) | ~w_valideren_aanvraag(X0)).

cnf(u930,axiom,
    ~a2_e_3(X0) | ~x2_e_16(X0)).

cnf(u1144,axiom,
    ~x2_s_10(X0) | ~x3_e_9(X0)).

cnf(u1389,axiom,
    ~a_cancelled(X0) | ~o_created(X0)).

cnf(u1337,axiom,
    ~tau_15(X0) | ~l_s_4(X0)).

cnf(u2897,axiom,
    ~x3_s_0(sK102)).

cnf(u2848,axiom,
    ~x2_s_3(sK43)).

cnf(u936,axiom,
    ~x2_e_3(X0) | ~x2_s_3(X0)).

cnf(u2939,axiom,
    ~x2_e_13(sK113)).

cnf(u1284,axiom,
    ~x3_s_9(X0) | ~x3_e_9(X0)).

cnf(u3116,axiom,
    ~x2_s_17(sK94)).

cnf(u3038,axiom,
    ~tau_10(sK61)).

cnf(u1183,axiom,
    ~tau_10(X0) | ~x2_s_13(X0)).

cnf(u937,axiom,
    ~a2_s_1(X0) | ~x2_s_3(X0)).

cnf(u938,axiom,
    ~a2_s_1(X0) | ~x2_e_3(X0)).

cnf(u1082,axiom,
    ~a2_s_0(X0) | ~x2_e_2(X0)).

cnf(u1410,axiom,
    ~l_s_6(X0) | ~x2_s_17(X0)).

cnf(u3020,axiom,
    ~a4_s_2(sK30)).

cnf(u1028,axiom,
    x3_s_8(sK48)).

cnf(u1227,axiom,
    ~x2_s_13(X0) | ~a4_s_2(X0)).

cnf(u2946,axiom,
    ~x2_e_14(sK105)).

cnf(u3045,axiom,
    ~x3_e_9(sK14)).

cnf(u2952,axiom,
    ~a2_e_3(sK34)).

cnf(u2858,axiom,
    ~x2_s_4(sK150)).

cnf(u2801,axiom,
    ~x2_s_15(sK29)).

cnf(u1224,axiom,
    ~tau_17(X0) | ~w_wijzigen_contractgegevens(X0)).

cnf(u1142,axiom,
    ~w_nabellen_offertes(X0) | ~x3_e_9(X0)).

cnf(u1417,axiom,
    ~x2_e_17(X0) | ~x2_e_6(X0)).

cnf(u3056,axiom,
    ~a_partlysubmitted(sK63)).

cnf(u3019,axiom,
    ~a4_s_2(sK33)).

cnf(u1179,axiom,
    ~tau_1(X0) | ~w_completeren_aanvraag(X0)).

cnf(u1143,axiom,
    ~l_s_2(X0) | ~tau_5(X0)).

cnf(u2953,axiom,
    ~a2_e_3(sK46)).

cnf(u3109,axiom,
    ~x2_s_11(sK113)).

cnf(u2995,axiom,
    ~a2_s_1(sK83)).

cnf(u3123,axiom,
    ~x2_e_6(sK83)).

cnf(u3085,axiom,
    ~l_s_1(sK130)).

cnf(u2865,axiom,
    ~x2_s_16(sK45)).

cnf(u3071,axiom,
    ~x2_s_5(sK74)).

cnf(u1370,axiom,
    ~x2_e_13(X0) | ~x2_s_13(X0)).

cnf(u3030,axiom,
    ~tau_6(sK20)).

cnf(u1121,axiom,
    ~x2_e_1(X0) | ~a_partlysubmitted(X0)).

cnf(u1162,axiom,
    ~a_declined(X0) | ~o_declined(X0)).

cnf(u2919,axiom,
    ~x2_e_7(sK121)).

cnf(u1392,axiom,
    ~x2_s_7(X0) | ~tau_7(X0)).

cnf(u1184,axiom,
    ~a_cancelled(X0) | ~x2_e_7(X0)).

cnf(u1073,axiom,
    x2_s_17(sK62)).

cnf(u976,axiom,
    ~tau_0(X0) | ~x2_e_1(X0)).

cnf(u3106,axiom,
    ~x2_s_11(sK34)).

cnf(u3066,axiom,
    ~x2_s_5(sK146)).

cnf(u3037,axiom,
    ~x2_s_2(sK80)).

cnf(u2988,axiom,
    ~x2_e_10(sK126)).

cnf(u1222,axiom,
    ~a2_s_0(X0) | ~x2_s_1(X0)).

cnf(u3082,axiom,
    ~tau_3(sK142)).

cnf(u2914,axiom,
    ~x2_e_1(sK43)).

cnf(u2885,axiom,
    ~x2_s_10(sK156)).

cnf(u1223,axiom,
    ~x2_s_1(X0) | ~a2_e_0(X0)).

cnf(u1244,axiom,
    ~l_s_6(X0) | ~x2_e_17(X0)).

cnf(u1385,axiom,
    ~x3_s_9(X0) | ~o_declined(X0)).

cnf(u2987,axiom,
    ~x2_e_7(sK154)).

cnf(u1192,axiom,
    ~o_sent(X0) | ~o_created(X0)).

cnf(u1081,axiom,
    ~a2_s_0(X0) | ~x2_s_2(X0)).

cnf(u991,axiom,
    ~x2_e_10(X0) | ~x2_s_11(X0)).

cnf(u2945,axiom,
    ~x2_e_14(sK46)).

cnf(u2896,axiom,
    ~a2_e_1(sK83)).

cnf(u1147,axiom,
    ~o_sent(X0) | ~x2_e_7(X0)).

cnf(u2921,axiom,
    ~x2_e_7(sK85)).

cnf(u2835,axiom,
    ~x2_e_11(sK54)).

cnf(u3118,axiom,
    ~x2_s_6(sK48)).

cnf(u1231,axiom,
    ~a4_s_2(X0) | ~a2_s_3(X0)).

cnf(u985,axiom,
    ~w_beoordelen_fraude(X0) | ~w_afhandelen_leads(X0)).

cnf(u1141,axiom,
    ~w_nabellen_offertes(X0) | ~l_s_4(X0)).

cnf(u2911,axiom,
    ~a2_e_1(sK136)).

cnf(u1338,axiom,
    x2_s_13(sK132)).

cnf(u1182,axiom,
    l_s_3(sK86)).

cnf(u2998,axiom,
    ~x2_s_13(sK26)).

cnf(u1130,axiom,
    ~o_sent(X0) | ~x2_s_7(X0)).

cnf(u2846,axiom,
    ~x2_e_2(sK141)).

cnf(u3097,axiom,
    ~x2_e_1(sK123)).

cnf(u1024,axiom,
    ~x2_s_6(X0) | ~x2_e_6(X0)).

cnf(u3044,axiom,
    ~x2_e_7(sK18)).

cnf(u993,axiom,
    ~x2_e_10(X0) | ~x2_e_11(X0)).

cnf(u3073,axiom,
    ~x2_e_5(sK74)).

cnf(u3005,axiom,
    ~o_created(sK21)).

cnf(u1161,axiom,
    ~tau_18(X0) | ~l_s_3(X0)).

cnf(u1190,axiom,
    ~x3_e_8(X0) | ~l_s_4(X0)).

cnf(u1138,axiom,
    ~a_declined(X0) | ~x3_e_9(X0)).

cnf(u1292,axiom,
    ~x2_e_15(X0) | ~a2_s_3(X0)).

cnf(u2853,axiom,
    ~x2_s_7(sK84)).

cnf(u3110,axiom,
    ~o_selected(sK96)).

cnf(u3043,axiom,
    ~x2_s_7(sK18)).

cnf(u1191,axiom,
    ~x3_e_8(X0) | ~x3_e_9(X0)).

cnf(u3015,axiom,
    ~a4_s_2(sK50)).

cnf(u2913,axiom,
    ~x2_e_1(sK42)).

cnf(u946,axiom,
    ~x2_e_12(X0) | ~tau_9(X0)).

cnf(u1032,axiom,
    ~l_s_2(X0) | ~x2_e_4(X0)).

cnf(u959,axiom,
    ~x2_s_6(X0) | ~tau_7(X0)).

cnf(u918,axiom,
    x2_s_5(sK6)).

cnf(u1221,axiom,
    l_s_6(sK97)).

cnf(u2815,axiom,
    ~x2_e_3(sK36)).

cnf(u1418,axiom,
    ~tau_1(X0) | ~x2_e_2(X0)).

cnf(u1291,axiom,
    ~x2_s_15(X0) | ~a2_s_3(X0)).

cnf(u1300,axiom,
    ~a_declined(X0) | ~x2_e_11(X0)).

cnf(u3054,axiom,
    ~a2_s_3(sK45)).

cnf(u2967,axiom,
    ~a_partlysubmitted(sK51)).

cnf(u1199,axiom,
    ~x2_e_11(X0) | ~a4_s_2(X0)).

cnf(u954,axiom,
    x2_s_11(sK22)).

cnf(u1232,axiom,
    ~a4_s_2(X0) | ~a2_e_3(X0)).

cnf(u2879,axiom,
    ~x2_s_16(sK39)).

cnf(u2838,axiom,
    ~x2_e_11(sK41)).

cnf(u3036,axiom,
    ~x3_s_9(sK78)).

cnf(u1299,axiom,
    ~a_declined(X0) | ~x2_s_10(X0)).

cnf(u1243,axiom,
    ~tau_17(X0) | ~l_s_6(X0)).

cnf(u3061,axiom,
    ~l_s_0(sK51)).

cnf(u3119,axiom,
    ~x2_e_6(sK48)).

cnf(u2968,axiom,
    ~a_partlysubmitted(sK133)).

cnf(u2804,axiom,
    ~x2_e_15(sK29)).

cnf(u1129,axiom,
    ~o_created(X0) | ~x2_s_7(X0)).

cnf(u2944,axiom,
    ~x2_e_14(sK34)).

cnf(u3035,axiom,
    ~x3_s_9(sK35)).

cnf(u2969,axiom,
    ~x2_e_15(sK57)).

cnf(u1052,axiom,
    ~w_wijzigen_contractgegevens(X0) | ~l_s_6(X0)).

cnf(u1031,axiom,
    ~x2_e_5(X0) | ~a_finalized(X0)).

cnf(u2920,axiom,
    ~x2_e_7(sK49)).

cnf(u2883,axiom,
    ~l_s_6(sK151)).

cnf(u3101,axiom,
    ~x3_e_9(sK15)).

cnf(u1386,axiom,
    ~w_afhandelen_leads(X0) | ~x3_s_0(X0)).

cnf(u1230,axiom,
    ~x2_e_14(X0) | ~a4_s_2(X0)).

cnf(u1137,axiom,
    ~x2_e_14(X0) | ~x2_s_14(X0)).

cnf(u2959,axiom,
    ~x2_e_1(sK120)).

cnf(u1178,axiom,
    ~tau_1(X0) | ~l_s_1(X0)).

cnf(u3115,axiom,
    ~x2_s_17(sK97)).

cnf(u2935,axiom,
    ~x2_s_13(sK113)).

cnf(u2894,axiom,
    ~x2_s_5(sK140)).

cnf(u1039,axiom,
    ~tau_12(X0) | ~x2_e_15(X0)).

cnf(u1200,axiom,
    ~x2_e_11(X0) | ~a4_e_2(X0)).

cnf(u2814,axiom,
    ~x2_s_3(sK36)).

cnf(u3122,axiom,
    ~x2_e_6(sK74)).

cnf(u1394,axiom,
    ~x2_s_11(X0) | ~a4_s_2(X0)).

cnf(u992,axiom,
    ~x2_s_10(X0) | ~x2_e_11(X0)).

cnf(u1393,axiom,
    ~x2_e_7(X0) | ~tau_7(X0)).

cnf(u2954,axiom,
    ~a2_e_3(sK105)).

cnf(u3053,axiom,
    ~a2_s_3(sK7)).

cnf(u3004,axiom,
    ~x3_e_9(sK114)).

cnf(u2930,axiom,
    ~x2_e_12(sK105)).

cnf(u2901,axiom,
    ~x2_e_17(sK86)).

cnf(u2852,axiom,
    ~a2_e_1(sK141)).

cnf(u994,axiom,
    ~x3_e_0(X0) | ~w_beoordelen_fraude(X0)).

cnf(u3120,axiom,
    ~x2_s_6(sK74)).

cnf(u2961,axiom,
    ~x2_e_1(sK109)).

cnf(u2912,axiom,
    ~x2_e_1(sK136)).

cnf(u3003,axiom,
    ~x3_e_9(sK106)).

cnf(u3076,axiom,
    ~x2_s_2(sK59)).

cnf(u2937,axiom,
    ~x2_e_13(sK46)).

cnf(u2851,axiom,
    ~a2_e_1(sK43)).

cnf(u1348,axiom,
    a2_s_0(sK136)).

cnf(u1303,axiom,
    ~tau_18(X0) | ~x2_e_17(X0)).

cnf(u1247,axiom,
    ~x2_e_5(X0) | ~tau_6(X0)).

cnf(u1268,axiom,
    ~x2_e_11(X0) | ~x3_s_9(X0)).

cnf(u1029,axiom,
    ~x2_e_5(X0) | ~x2_s_5(X0)).

cnf(u1002,axiom,
    ~a2_e_0(X0) | ~x2_s_2(X0)).

cnf(u2927,axiom,
    ~x2_s_12(sK113)).

cnf(u2886,axiom,
    ~x2_s_4(sK12)).

cnf(u1146,axiom,
    ~o_created(X0) | ~x2_e_7(X0)).

cnf(u1043,axiom,
    ~x2_e_4(X0) | ~x2_s_4(X0)).

cnf(u2805,axiom,
    ~x2_e_15(sK69)).

cnf(u3113,axiom,
    ~a_approved(sK32)).

cnf(u3060,axiom,
    ~l_s_0(sK109)).

cnf(u3010,axiom,
    ~a4_e_2(sK78)).

cnf(u1040,axiom,
    ~x3_e_8(X0) | ~w_nabellen_offertes(X0)).

cnf(u2803,axiom,
    ~x2_s_15(sK82)).

cnf(u3016,axiom,
    ~a4_s_2(sK132)).

cnf(u1286,axiom,
    ~tau_8(X0) | ~o_sent_back(X0)).

cnf(u1229,axiom,
    ~x2_s_14(X0) | ~a4_s_2(X0)).

cnf(u3089,axiom,
    ~x2_e_17(sK48)).

cnf(u1177,axiom,
    ~x2_e_17(X0) | ~a2_s_1(X0)).

cnf(u2893,axiom,
    ~x2_s_5(sK55)).

cnf(u2844,axiom,
    ~x2_e_2(sK42)).

cnf(u1026,axiom,
    ~x2_e_16(X0) | ~x2_s_16(X0)).

cnf(u2869,axiom,
    ~x2_e_4(sK99)).

cnf(u3017,axiom,
    ~a4_s_2(sK31)).

cnf(u3059,axiom,
    ~l_s_0(sK56)).

cnf(u1048,axiom,
    ~a_preaccepted(X0) | ~w_beoordelen_fraude(X0)).

cnf(u2845,axiom,
    ~x2_e_2(sK43)).

cnf(u933,axiom,
    a4_s_2(sK13)).

cnf(u1294,axiom,
    ~x2_e_16(X0) | ~a2_s_3(X0)).

cnf(u1293,axiom,
    ~x2_s_16(X0) | ~a2_s_3(X0)).

cnf(u934,axiom,
    x3_s_9(sK14)).

cnf(u2929,axiom,
    ~x2_e_12(sK46)).

cnf(u2843,axiom,
    ~x2_s_2(sK141)).

cnf(u1185,axiom,
    ~x2_e_14(X0) | ~tau_11(X0)).

cnf(u1307,axiom,
    ~tau_3(X0) | ~x2_s_3(X0)).

cnf(u1226,axiom,
    ~x2_e_12(X0) | ~a4_s_2(X0)).

cnf(u2983,axiom,
    ~x3_e_9(sK35)).

cnf(u3070,axiom,
    ~x2_e_5(sK77)).

cnf(u1108,axiom,
    ~a4_e_2(X0) | ~x2_s_14(X0)).

cnf(u941,axiom,
    l_s_4(sK15)).

cnf(u1301,axiom,
    ~x3_s_8(X0) | ~o_cancelled(X0)).

cnf(u1038,axiom,
    ~x2_e_11(X0) | ~o_declined(X0)).

cnf(u2854,axiom,
    ~x2_s_17(sK74)).

cnf(u3052,axiom,
    ~a2_s_3(sK119)).

cnf(u1234,axiom,
    ~x3_s_8(X0) | ~w_nabellen_offertes(X0)).

cnf(u2949,axiom,
    ~a2_s_3(sK46)).

cnf(u2900,axiom,
    ~x2_s_6(sK77)).

cnf(u2984,axiom,
    ~x3_e_9(sK78)).

cnf(u1145,axiom,
    ~x2_e_11(X0) | ~x3_e_9(X0)).

cnf(u3009,axiom,
    ~a4_e_2(sK35)).

cnf(u3051,axiom,
    ~a2_s_3(sK40)).

cnf(u2985,axiom,
    ~x2_e_7(sK139)).

cnf(u2936,axiom,
    ~x2_e_13(sK34)).

cnf(u1047,axiom,
    ~a_activated(X0) | ~x2_s_13(X0)).

cnf(u1068,axiom,
    ~a_registered(X0) | ~tau_12(X0)).

cnf(u2899,axiom,
    ~x2_s_6(sK86)).

% # SZS output end Saturation.
% ------------------------------
% Version: Vampire 4.9 (commit 5ad494e78 on 2024-06-14 14:05:27 +0100)
% Linked with Z3 4.12.3.0 79bbbf76d0c123481c8ca05cd3a98939270074d3 z3-4.8.4-7980-g79bbbf76d
% Termination reason: Satisfiable

% Memory used [KB]: 1560
% Time elapsed: 0.010 s
% ------------------------------
% ------------------------------

perf_event_open failed (instruction limiting will be disabled): Permission denied
(If you are seeing 'Permission denied' ask your admin to run 'sudo sysctl -w kernel.perf_event_paranoid=-1' for you.)
