% Running in auto input_syntax mode. Trying TPTP
% Refutation found. Thanks to Tanya!
% SZS status Theorem for tptp_thesis
% SZS output start Proof for tptp_thesis
176. ! [X1] : (x3_s_0(X1) => ((? [X9] : a_preaccepted(X9) & ~? [X8] : w_beoordelen_fraude(X8) & ~? [X7] : w_afhandelen_leads(X7)) | (~? [X6] : a_preaccepted(X6) & ? [X5] : w_beoordelen_fraude(X5) & ~? [X4] : w_afhandelen_leads(X4)) | (~? [X3] : a_preaccepted(X3) & ~? [X2] : w_beoordelen_fraude(X2) & ? [X0] : w_afhandelen_leads(X0)))) [input]
208. ? [X0] : x3_s_0(X0) [input]
277. ! [X10] : ~(a_preaccepted(X10) & w_afhandelen_leads(X10)) [input]
278. ~! [X10] : ~(a_preaccepted(X10) & w_afhandelen_leads(X10)) [negated conjecture 277]
331. ! [X0] : (x3_s_0(X0) => ((? [X1] : a_preaccepted(X1) & ~? [X2] : w_beoordelen_fraude(X2) & ~? [X3] : w_afhandelen_leads(X3)) | (~? [X4] : a_preaccepted(X4) & ? [X5] : w_beoordelen_fraude(X5) & ~? [X6] : w_afhandelen_leads(X6)) | (~? [X7] : a_preaccepted(X7) & ~? [X8] : w_beoordelen_fraude(X8) & ? [X9] : w_afhandelen_leads(X9)))) [rectify 176]
359. ~! [X0] : ~(a_preaccepted(X0) & w_afhandelen_leads(X0)) [rectify 278]
525. ! [X0] : (((? [X1] : a_preaccepted(X1) & ! [X2] : ~w_beoordelen_fraude(X2) & ! [X3] : ~w_afhandelen_leads(X3)) | (! [X4] : ~a_preaccepted(X4) & ? [X5] : w_beoordelen_fraude(X5) & ! [X6] : ~w_afhandelen_leads(X6)) | (! [X7] : ~a_preaccepted(X7) & ! [X8] : ~w_beoordelen_fraude(X8) & ? [X9] : w_afhandelen_leads(X9))) | ~x3_s_0(X0)) [ennf transformation 331]
526. ! [X0] : ((? [X1] : a_preaccepted(X1) & ! [X2] : ~w_beoordelen_fraude(X2) & ! [X3] : ~w_afhandelen_leads(X3)) | (! [X4] : ~a_preaccepted(X4) & ? [X5] : w_beoordelen_fraude(X5) & ! [X6] : ~w_afhandelen_leads(X6)) | (! [X7] : ~a_preaccepted(X7) & ! [X8] : ~w_beoordelen_fraude(X8) & ? [X9] : w_afhandelen_leads(X9)) | ~x3_s_0(X0)) [flattening 525]
624. ? [X0] : (a_preaccepted(X0) & w_afhandelen_leads(X0)) [ennf transformation 359]
628. (! [X7] : ~a_preaccepted(X7) & ! [X8] : ~w_beoordelen_fraude(X8) & ? [X9] : w_afhandelen_leads(X9)) | ~sP2 [predicate definition introduction]
629. (! [X4] : ~a_preaccepted(X4) & ? [X5] : w_beoordelen_fraude(X5) & ! [X6] : ~w_afhandelen_leads(X6)) | ~sP3 [predicate definition introduction]
630. ! [X0] : ((? [X1] : a_preaccepted(X1) & ! [X2] : ~w_beoordelen_fraude(X2) & ! [X3] : ~w_afhandelen_leads(X3)) | sP3 | sP2 | ~x3_s_0(X0)) [definition folding 526,629,628]
813. (! [X4] : ~a_preaccepted(X4) & ? [X5] : w_beoordelen_fraude(X5) & ! [X6] : ~w_afhandelen_leads(X6)) | ~sP3 [nnf transformation 629]
814. (! [X0] : ~a_preaccepted(X0) & ? [X1] : w_beoordelen_fraude(X1) & ! [X2] : ~w_afhandelen_leads(X2)) | ~sP3 [rectify 813]
815. ? [X1] : w_beoordelen_fraude(X1) => w_beoordelen_fraude(sK102) [choice axiom]
816. (! [X0] : ~a_preaccepted(X0) & w_beoordelen_fraude(sK102) & ! [X2] : ~w_afhandelen_leads(X2)) | ~sP3 [skolemisation 814,815]
817. (! [X7] : ~a_preaccepted(X7) & ! [X8] : ~w_beoordelen_fraude(X8) & ? [X9] : w_afhandelen_leads(X9)) | ~sP2 [nnf transformation 628]
818. (! [X0] : ~a_preaccepted(X0) & ! [X1] : ~w_beoordelen_fraude(X1) & ? [X2] : w_afhandelen_leads(X2)) | ~sP2 [rectify 817]
819. ? [X2] : w_afhandelen_leads(X2) => w_afhandelen_leads(sK103) [choice axiom]
820. (! [X0] : ~a_preaccepted(X0) & ! [X1] : ~w_beoordelen_fraude(X1) & w_afhandelen_leads(sK103)) | ~sP2 [skolemisation 818,819]
821. ? [X1] : a_preaccepted(X1) => a_preaccepted(sK104) [choice axiom]
822. ! [X0] : ((a_preaccepted(sK104) & ! [X2] : ~w_beoordelen_fraude(X2) & ! [X3] : ~w_afhandelen_leads(X3)) | sP3 | sP2 | ~x3_s_0(X0)) [skolemisation 630,821]
851. ? [X0] : x3_s_0(X0) => x3_s_0(sK120) [choice axiom]
852. x3_s_0(sK120) [skolemisation 208,851]
922. ? [X0] : (a_preaccepted(X0) & w_afhandelen_leads(X0)) => (a_preaccepted(sK157) & w_afhandelen_leads(sK157)) [choice axiom]
923. a_preaccepted(sK157) & w_afhandelen_leads(sK157) [skolemisation 624,922]
1254. ~w_afhandelen_leads(X2) | ~sP3 [cnf transformation 816]
1259. ~a_preaccepted(X0) | ~sP2 [cnf transformation 820]
1260. ~w_afhandelen_leads(X3) | sP3 | sP2 | ~x3_s_0(X0) [cnf transformation 822]
1311. x3_s_0(sK120) [cnf transformation 852]
1445. w_afhandelen_leads(sK157) [cnf transformation 923]
1446. a_preaccepted(sK157) [cnf transformation 923]
1594. 37 <=> ! [X0] : ~x3_s_0(X0) [avatar definition]
1595. ~x3_s_0(X0) <- (37) [avatar component clause 1594]
2064. 145 <=> ! [X0] : ~a_preaccepted(X0) [avatar definition]
2065. ~a_preaccepted(X0) <- (145) [avatar component clause 2064]
2076. 148 <=> ! [X0] : ~w_afhandelen_leads(X0) [avatar definition]
2077. ~w_afhandelen_leads(X0) <- (148) [avatar component clause 2076]
2257. 186 <=> sP3 [avatar definition]
2266. ~186 | 148 [avatar split clause 1254,2076,2257]
2268. 188 <=> sP2 [avatar definition]
2271. ~188 | 145 [avatar split clause 1259,2064,2268]
2284. 37 | 188 | 186 | 148 [avatar split clause 1260,2076,2257,2268,1594]
2729. $false <- (37) [resolution 1595,1311]
2730. ~37 [avatar contradiction clause 2729]
2787. $false <- (145) [resolution 2065,1446]
2788. ~145 [avatar contradiction clause 2787]
2789. $false <- (148) [resolution 2077,1445]
2790. ~148 [avatar contradiction clause 2789]
2791. $false [avatar sat refutation 2266,2271,2284,2730,2788,2790]
% SZS output end Proof for tptp_thesis
% ------------------------------
% 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: Refutation

% Memory used [KB]: 1467
% Time elapsed: 0.013 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.)
