% 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
1. ! [X0] : (x2_s_1(X0) => ((? [X4] : (set_status(X4) | l_s_13(X4)) & ~? [X3] : (code_ok(X3) | x2_s_2(X3))) | (~? [X2] : (set_status(X2) | l_s_13(X2)) & ? [X1] : (code_ok(X1) | x2_s_2(X1))))) [input]
103. ? [X1] : l_s_13(X1) [input]
207. ? [X1] : x2_s_1(X1) [input]
212. ? [X1] : x2_s_2(X1) [input]
254. ! [X0] : (x2_s_1(X0) => ((? [X1] : (set_status(X1) | l_s_13(X1)) & ~? [X2] : (code_ok(X2) | x2_s_2(X2))) | (~? [X3] : (set_status(X3) | l_s_13(X3)) & ? [X4] : (code_ok(X4) | x2_s_2(X4))))) [rectify 1]
335. ? [X0] : l_s_13(X0) [rectify 103]
414. ? [X0] : x2_s_1(X0) [rectify 207]
418. ? [X0] : x2_s_2(X0) [rectify 212]
449. ! [X0] : (((? [X1] : (set_status(X1) | l_s_13(X1)) & ! [X2] : (~code_ok(X2) & ~x2_s_2(X2))) | (! [X3] : (~set_status(X3) & ~l_s_13(X3)) & ? [X4] : (code_ok(X4) | x2_s_2(X4)))) | ~x2_s_1(X0)) [ennf transformation 254]
450. ! [X0] : ((? [X1] : (set_status(X1) | l_s_13(X1)) & ! [X2] : (~code_ok(X2) & ~x2_s_2(X2))) | (! [X3] : (~set_status(X3) & ~l_s_13(X3)) & ? [X4] : (code_ok(X4) | x2_s_2(X4))) | ~x2_s_1(X0)) [flattening 449]
690. (! [X3] : (~set_status(X3) & ~l_s_13(X3)) & ? [X4] : (code_ok(X4) | x2_s_2(X4))) | ~sP0 [predicate definition introduction]
691. ! [X0] : ((? [X1] : (set_status(X1) | l_s_13(X1)) & ! [X2] : (~code_ok(X2) & ~x2_s_2(X2))) | sP0 | ~x2_s_1(X0)) [definition folding 450,690]
699. (! [X3] : (~set_status(X3) & ~l_s_13(X3)) & ? [X4] : (code_ok(X4) | x2_s_2(X4))) | ~sP0 [nnf transformation 690]
700. (! [X0] : (~set_status(X0) & ~l_s_13(X0)) & ? [X1] : (code_ok(X1) | x2_s_2(X1))) | ~sP0 [rectify 699]
701. ? [X1] : (code_ok(X1) | x2_s_2(X1)) => (code_ok(sK5) | x2_s_2(sK5)) [choice axiom]
702. (! [X0] : (~set_status(X0) & ~l_s_13(X0)) & (code_ok(sK5) | x2_s_2(sK5))) | ~sP0 [skolemisation 700,701]
703. ? [X1] : (set_status(X1) | l_s_13(X1)) => (set_status(sK6) | l_s_13(sK6)) [choice axiom]
704. ! [X0] : (((set_status(sK6) | l_s_13(sK6)) & ! [X2] : (~code_ok(X2) & ~x2_s_2(X2))) | sP0 | ~x2_s_1(X0)) [skolemisation 691,703]
801. ? [X0] : l_s_13(X0) => l_s_13(sK58) [choice axiom]
802. l_s_13(sK58) [skolemisation 335,801]
932. ? [X0] : x2_s_1(X0) => x2_s_1(sK129) [choice axiom]
933. x2_s_1(sK129) [skolemisation 414,932]
940. ? [X0] : x2_s_2(X0) => x2_s_2(sK133) [choice axiom]
941. x2_s_2(sK133) [skolemisation 418,940]
994. ~l_s_13(X0) | ~sP0 [cnf transformation 702]
996. ~x2_s_2(X2) | sP0 | ~x2_s_1(X0) [cnf transformation 704]
1189. l_s_13(sK58) [cnf transformation 802]
1376. x2_s_1(sK129) [cnf transformation 933]
1382. x2_s_2(sK133) [cnf transformation 941]
1456. 1 <=> sP0 [avatar definition]
1464. 3 <=> ! [X0] : ~l_s_13(X0) [avatar definition]
1465. ~l_s_13(X0) <- (3) [avatar component clause 1464]
1466. ~1 | 3 [avatar split clause 994,1464,1456]
1477. 6 <=> ! [X0] : ~x2_s_1(X0) [avatar definition]
1478. ~x2_s_1(X0) <- (6) [avatar component clause 1477]
1493. 10 <=> ! [X2] : ~x2_s_2(X2) [avatar definition]
1494. ~x2_s_2(X2) <- (10) [avatar component clause 1493]
1495. 6 | 1 | 10 [avatar split clause 996,1493,1456,1477]
2582. $false <- (3) [resolution 1465,1189]
2583. ~3 [avatar contradiction clause 2582]
2606. $false <- (6) [resolution 1478,1376]
2607. ~6 [avatar contradiction clause 2606]
2608. $false <- (10) [resolution 1494,1382]
2609. ~10 [avatar contradiction clause 2608]
2610. $false [avatar sat refutation 1466,1495,2583,2607,2609]
% 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]: 1368
% Time elapsed: 0.008 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.)
