% Running in auto input_syntax mode. Trying TPTP
% Refutation found. Thanks to Tanya!
% SZS status Unsatisfiable for tptp_25
% SZS output start Proof for tptp_25
10. ! [X1] : (x2_s_b2(X1) => ((? [X4] : (manual(X4) | l_s_b10(X4)) & ~? [X3] : (fin(X3) | x2_s_b3(X3))) | (~? [X2] : (manual(X2) | l_s_b10(X2)) & ? [X0] : (fin(X0) | x2_s_b3(X0))))) [input]
86. ! [X1] : (l_s_b9(X1) => ? [X0] : fin(X0)) [input]
128. ? [X0] : l_s_b6(X0) [input]
132. ! [X1] : ((x3_e_b4(X1) | x3_s_b4(X1) | tau_b2(X1)) => ? [X0] : x2_e_b3(X0)) [input]
210. ? [X0] : l_s_b10(X0) [input]
217. ? [X0] : x2_s_b2(X0) [input]
233. ! [X1] : ((x2_e_b3(X1) | x2_s_b3(X1)) => ? [X0] : (fin(X0) | l_s_b9(X0))) [input]
246. ! [X1] : ((change_end(X1) | l_s_b8(X1) | change_diagn(X1) | l_s_b7(X1) | x2_e_b6(X1) | x2_s_b5(X1)) => ? [X0] : x3_e_b4(X0)) [input]
248. ! [X1] : ((reopen(X1) | l_s_b6(X1) | tau_b8(X1)) => ? [X0] : x2_e_b6(X0)) [input]
254. ! [X0] : (x2_s_b2(X0) => ((? [X1] : (manual(X1) | l_s_b10(X1)) & ~? [X2] : (fin(X2) | x2_s_b3(X2))) | (~? [X3] : (manual(X3) | l_s_b10(X3)) & ? [X4] : (fin(X4) | x2_s_b3(X4))))) [rectify 10]
282. ! [X0] : (l_s_b9(X0) => ? [X1] : fin(X1)) [rectify 86]
297. ! [X0] : ((x3_e_b4(X0) | x3_s_b4(X0) | tau_b2(X0)) => ? [X1] : x2_e_b3(X1)) [rectify 132]
329. ! [X0] : ((x2_e_b3(X0) | x2_s_b3(X0)) => ? [X1] : (fin(X1) | l_s_b9(X1))) [rectify 233]
334. ! [X0] : ((change_end(X0) | l_s_b8(X0) | change_diagn(X0) | l_s_b7(X0) | x2_e_b6(X0) | x2_s_b5(X0)) => ? [X1] : x3_e_b4(X1)) [rectify 246]
336. ! [X0] : ((reopen(X0) | l_s_b6(X0) | tau_b8(X0)) => ? [X1] : x2_e_b6(X1)) [rectify 248]
347. ! [X0] : (((? [X1] : (manual(X1) | l_s_b10(X1)) & ! [X2] : (~fin(X2) & ~x2_s_b3(X2))) | (! [X3] : (~manual(X3) & ~l_s_b10(X3)) & ? [X4] : (fin(X4) | x2_s_b3(X4)))) | ~x2_s_b2(X0)) [ennf transformation 254]
348. ! [X0] : ((? [X1] : (manual(X1) | l_s_b10(X1)) & ! [X2] : (~fin(X2) & ~x2_s_b3(X2))) | (! [X3] : (~manual(X3) & ~l_s_b10(X3)) & ? [X4] : (fin(X4) | x2_s_b3(X4))) | ~x2_s_b2(X0)) [flattening 347]
420. ! [X0] : (? [X1] : fin(X1) | ~l_s_b9(X0)) [ennf transformation 282]
460. ! [X0] : (? [X1] : x2_e_b3(X1) | (~x3_e_b4(X0) & ~x3_s_b4(X0) & ~tau_b2(X0))) [ennf transformation 297]
556. ! [X0] : (? [X1] : (fin(X1) | l_s_b9(X1)) | (~x2_e_b3(X0) & ~x2_s_b3(X0))) [ennf transformation 329]
571. ! [X0] : (? [X1] : x3_e_b4(X1) | (~change_end(X0) & ~l_s_b8(X0) & ~change_diagn(X0) & ~l_s_b7(X0) & ~x2_e_b6(X0) & ~x2_s_b5(X0))) [ennf transformation 334]
574. ! [X0] : (? [X1] : x2_e_b6(X1) | (~reopen(X0) & ~l_s_b6(X0) & ~tau_b8(X0))) [ennf transformation 336]
578. (! [X3] : (~manual(X3) & ~l_s_b10(X3)) & ? [X4] : (fin(X4) | x2_s_b3(X4))) | ~sP0 [predicate definition introduction]
579. ! [X0] : ((? [X1] : (manual(X1) | l_s_b10(X1)) & ! [X2] : (~fin(X2) & ~x2_s_b3(X2))) | sP0 | ~x2_s_b2(X0)) [definition folding 348,578]
594. (! [X3] : (~manual(X3) & ~l_s_b10(X3)) & ? [X4] : (fin(X4) | x2_s_b3(X4))) | ~sP0 [nnf transformation 578]
595. (! [X0] : (~manual(X0) & ~l_s_b10(X0)) & ? [X1] : (fin(X1) | x2_s_b3(X1))) | ~sP0 [rectify 594]
596. ? [X1] : (fin(X1) | x2_s_b3(X1)) => (fin(sK9) | x2_s_b3(sK9)) [choice axiom]
597. (! [X0] : (~manual(X0) & ~l_s_b10(X0)) & (fin(sK9) | x2_s_b3(sK9))) | ~sP0 [skolemisation 595,596]
598. ? [X1] : (manual(X1) | l_s_b10(X1)) => (manual(sK10) | l_s_b10(sK10)) [choice axiom]
599. ! [X0] : (((manual(sK10) | l_s_b10(sK10)) & ! [X2] : (~fin(X2) & ~x2_s_b3(X2))) | sP0 | ~x2_s_b2(X0)) [skolemisation 579,598]
693. ? [X1] : fin(X1) => fin(sK59) [choice axiom]
694. ! [X0] : (fin(sK59) | ~l_s_b9(X0)) [skolemisation 420,693]
740. ? [X0] : l_s_b6(X0) => l_s_b6(sK84) [choice axiom]
741. l_s_b6(sK84) [skolemisation 128,740]
744. ? [X1] : x2_e_b3(X1) => x2_e_b3(sK86) [choice axiom]
745. ! [X0] : (x2_e_b3(sK86) | (~x3_e_b4(X0) & ~x3_s_b4(X0) & ~tau_b2(X0))) [skolemisation 460,744]
833. ? [X0] : l_s_b10(X0) => l_s_b10(sK133) [choice axiom]
834. l_s_b10(sK133) [skolemisation 210,833]
839. ? [X0] : x2_s_b2(X0) => x2_s_b2(sK136) [choice axiom]
840. x2_s_b2(sK136) [skolemisation 217,839]
857. ? [X1] : (fin(X1) | l_s_b9(X1)) => (fin(sK146) | l_s_b9(sK146)) [choice axiom]
858. ! [X0] : ((fin(sK146) | l_s_b9(sK146)) | (~x2_e_b3(X0) & ~x2_s_b3(X0))) [skolemisation 556,857]
869. ? [X1] : x3_e_b4(X1) => x3_e_b4(sK153) [choice axiom]
870. ! [X0] : (x3_e_b4(sK153) | (~change_end(X0) & ~l_s_b8(X0) & ~change_diagn(X0) & ~l_s_b7(X0) & ~x2_e_b6(X0) & ~x2_s_b5(X0))) [skolemisation 571,869]
874. ? [X1] : x2_e_b6(X1) => x2_e_b6(sK156) [choice axiom]
875. ! [X0] : (x2_e_b6(sK156) | (~reopen(X0) & ~l_s_b6(X0) & ~tau_b8(X0))) [skolemisation 574,874]
893. ~l_s_b10(X0) | ~sP0 [cnf transformation 597]
896. ~fin(X2) | sP0 | ~x2_s_b2(X0) [cnf transformation 599]
1042. fin(sK59) | ~l_s_b9(X0) [cnf transformation 694]
1115. l_s_b6(sK84) [cnf transformation 741]
1125. x2_e_b3(sK86) | ~x3_e_b4(X0) [cnf transformation 745]
1263. l_s_b10(sK133) [cnf transformation 834]
1275. x2_s_b2(sK136) [cnf transformation 840]
1301. fin(sK146) | l_s_b9(sK146) | ~x2_e_b3(X0) [cnf transformation 858]
1322. x3_e_b4(sK153) | ~x2_e_b6(X0) [cnf transformation 870]
1332. x2_e_b6(sK156) | ~l_s_b6(X0) [cnf transformation 875]
1371. 9 <=> ! [X3] : ~l_s_b6(X3) [avatar definition]
1372. ~l_s_b6(X3) <- (9) [avatar component clause 1371]
1386. 12 <=> sP0 [avatar definition]
1394. 14 <=> ! [X0] : ~l_s_b10(X0) [avatar definition]
1395. ~l_s_b10(X0) <- (14) [avatar component clause 1394]
1396. ~12 | 14 [avatar split clause 893,1394,1386]
1407. 17 <=> ! [X0] : ~x2_s_b2(X0) [avatar definition]
1408. ~x2_s_b2(X0) <- (17) [avatar component clause 1407]
1419. 20 <=> ! [X2] : ~fin(X2) [avatar definition]
1420. ~fin(X2) <- (20) [avatar component clause 1419]
1421. 17 | 12 | 20 [avatar split clause 896,1419,1386,1407]
1725. 92 <=> ! [X2] : ~x2_e_b6(X2) [avatar definition]
1726. ~x2_e_b6(X2) <- (92) [avatar component clause 1725]
1791. 106 <=> ! [X0] : ~l_s_b9(X0) [avatar definition]
1792. ~l_s_b9(X0) <- (106) [avatar component clause 1791]
1794. 107 <=> fin(sK59) [avatar definition]
1796. fin(sK59) <- (107) [avatar component clause 1794]
1797. 106 | 107 [avatar split clause 1042,1794,1791]
1821. 113 <=> ! [X3] : ~x3_e_b4(X3) [avatar definition]
1822. ~x3_e_b4(X3) <- (113) [avatar component clause 1821]
1975. 147 <=> x2_e_b3(sK86) [avatar definition]
1977. x2_e_b3(sK86) <- (147) [avatar component clause 1975]
1978. 113 | 147 [avatar split clause 1125,1975,1821]
2369. 232 <=> ! [X0] : ~x2_e_b3(X0) [avatar definition]
2370. ~x2_e_b3(X0) <- (232) [avatar component clause 2369]
2372. 233 <=> l_s_b9(sK146) [avatar definition]
2374. l_s_b9(sK146) <- (233) [avatar component clause 2372]
2376. 234 <=> fin(sK146) [avatar definition]
2378. fin(sK146) <- (234) [avatar component clause 2376]
2379. 232 | 233 | 234 [avatar split clause 1301,2376,2372,2369]
2412. 241 <=> x3_e_b4(sK153) [avatar definition]
2414. x3_e_b4(sK153) <- (241) [avatar component clause 2412]
2419. 92 | 241 [avatar split clause 1322,2412,1725]
2437. 245 <=> x2_e_b6(sK156) [avatar definition]
2439. x2_e_b6(sK156) <- (245) [avatar component clause 2437]
2441. 9 | 245 [avatar split clause 1332,2437,1371]
2474. $false <- (92, 245) [subsumption resolution 2439,1726]
2475. ~92 | ~245 [avatar contradiction clause 2474]
2478. $false <- (113, 241) [subsumption resolution 2414,1822]
2479. ~113 | ~241 [avatar contradiction clause 2478]
2480. $false <- (147, 232) [subsumption resolution 1977,2370]
2481. ~147 | ~232 [avatar contradiction clause 2480]
2482. $false <- (20, 234) [subsumption resolution 2378,1420]
2483. ~20 | ~234 [avatar contradiction clause 2482]
2496. $false <- (9) [resolution 1372,1115]
2497. ~9 [avatar contradiction clause 2496]
2498. $false <- (14) [resolution 1395,1263]
2499. ~14 [avatar contradiction clause 2498]
2502. $false <- (17) [resolution 1408,1275]
2503. ~17 [avatar contradiction clause 2502]
2504. $false <- (106, 233) [subsumption resolution 2374,1792]
2505. ~106 | ~233 [avatar contradiction clause 2504]
2506. $false <- (20, 107) [subsumption resolution 1796,1420]
2507. ~20 | ~107 [avatar contradiction clause 2506]
2508. $false [avatar sat refutation 1396,1421,1797,1978,2379,2419,2441,2475,2479,2481,2483,2497,2499,2503,2505,2507]
% SZS output end Proof for tptp_25
% ------------------------------
% 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]: 1315
% Time elapsed: 0.005 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.)
