% 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]
992. ~l_s_13(X0) | ~sP0 [cnf transformation 702]
994. ~x2_s_2(X2) | sP0 | ~x2_s_1(X0) [cnf transformation 704]
1187. l_s_13(sK58) [cnf transformation 802]
1374. x2_s_1(sK129) [cnf transformation 933]
1380. x2_s_2(sK133) [cnf transformation 941]
1454. 1 <=> sP0 [avatar definition]
1462. 3 <=> ! [X0] : ~l_s_13(X0) [avatar definition]
1463. ~l_s_13(X0) <- (3) [avatar component clause 1462]
1464. ~1 | 3 [avatar split clause 992,1462,1454]
1475. 6 <=> ! [X0] : ~x2_s_1(X0) [avatar definition]
1476. ~x2_s_1(X0) <- (6) [avatar component clause 1475]
1491. 10 <=> ! [X2] : ~x2_s_2(X2) [avatar definition]
1492. ~x2_s_2(X2) <- (10) [avatar component clause 1491]
1493. 6 | 1 | 10 [avatar split clause 994,1491,1454,1475]
2582. $false <- (3) [resolution 1463,1187]
2583. ~3 [avatar contradiction clause 2582]
2618. $false <- (6) [resolution 1476,1374]
2619. ~6 [avatar contradiction clause 2618]
2620. $false <- (10) [resolution 1492,1380]
2621. ~10 [avatar contradiction clause 2620]
2622. $false [avatar sat refutation 1464,1493,2583,2619,2621]
% 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]: 1372
% Time elapsed: 0.007 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.)
