% Running in auto input_syntax mode. Trying TPTP
% SZS status CounterSatisfiable for tptp_thesis
% # SZS output start Saturation.
cnf(u1452,axiom,
    x2_s_16(sK7)).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u2175,axiom,
    ~sP1).

cnf(u2187,axiom,
    ~sP0).

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

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

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

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

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

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

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

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

cnf(u2257,axiom,
    sP3).

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

cnf(u2269,axiom,
    ~sP2).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u2560,axiom,
    ~sP5).

cnf(u2572,axiom,
    ~sP4).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u2644,negated_conjecture,
    ~a_submitted(sK157)).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

% # 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]: 1561
% 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.)
