% Running in auto input_syntax mode. Trying TPTP
% Refutation found. Thanks to Tanya!
% SZS status Theorem for tptp_IMPLIES
% SZS output start Proof for tptp_IMPLIES
267. ? [X0] : x2_s_a12(X0) [input]
323. ! [X1] : (x2_s_a12(X1) => ((? [X4] : code_ok(X4) & ~? [X3] : manual(X3)) | (~? [X2] : code_ok(X2) & ? [X0] : manual(X0)))) [input]
407. ! [X1] : (l_s_b10(X1) => ? [X0] : manual(X0)) [input]
458. ! [X1] : ((manual(X1) | l_s_b10(X1) | fin(X1) | x2_s_b3(X1)) => ? [X0] : x2_e_b2(X0)) [input]
522. ! [X1] : ((x2_e_b2(X1) | x2_s_b2(X1)) => ? [X0] : (release(X0) | l_s_b11(X0))) [input]
564. ? [X0] : l_s_b10(X0) [input]
570. ! [X1] : ((release(X1) | l_s_b11(X1)) => ? [X0] : (code_ok(X0) | l_s_b12(X0))) [input]
582. ! [X1] : (l_s_b12(X1) => ? [X0] : code_ok(X0)) [input]
705. ! [X0] : (x2_s_a12(X0) => ((? [X1] : code_ok(X1) & ~? [X2] : manual(X2)) | (~? [X3] : code_ok(X3) & ? [X4] : manual(X4)))) [rectify 323]
728. ! [X0] : (l_s_b10(X0) => ? [X1] : manual(X1)) [rectify 407]
748. ! [X0] : ((manual(X0) | l_s_b10(X0) | fin(X0) | x2_s_b3(X0)) => ? [X1] : x2_e_b2(X1)) [rectify 458]
769. ! [X0] : ((x2_e_b2(X0) | x2_s_b2(X0)) => ? [X1] : (release(X1) | l_s_b11(X1))) [rectify 522]
782. ! [X0] : ((release(X0) | l_s_b11(X0)) => ? [X1] : (code_ok(X1) | l_s_b12(X1))) [rectify 570]
788. ! [X0] : (l_s_b12(X0) => ? [X1] : code_ok(X1)) [rectify 582]
1463. ! [X0] : (((? [X1] : code_ok(X1) & ! [X2] : ~manual(X2)) | (! [X3] : ~code_ok(X3) & ? [X4] : manual(X4))) | ~x2_s_a12(X0)) [ennf transformation 705]
1464. ! [X0] : ((? [X1] : code_ok(X1) & ! [X2] : ~manual(X2)) | (! [X3] : ~code_ok(X3) & ? [X4] : manual(X4)) | ~x2_s_a12(X0)) [flattening 1463]
1545. ! [X0] : (? [X1] : manual(X1) | ~l_s_b10(X0)) [ennf transformation 728]
1597. ! [X0] : (? [X1] : x2_e_b2(X1) | (~manual(X0) & ~l_s_b10(X0) & ~fin(X0) & ~x2_s_b3(X0))) [ennf transformation 748]
1655. ! [X0] : (? [X1] : (release(X1) | l_s_b11(X1)) | (~x2_e_b2(X0) & ~x2_s_b2(X0))) [ennf transformation 769]
1697. ! [X0] : (? [X1] : (code_ok(X1) | l_s_b12(X1)) | (~release(X0) & ~l_s_b11(X0))) [ennf transformation 782]
1709. ! [X0] : (? [X1] : code_ok(X1) | ~l_s_b12(X0)) [ennf transformation 788]
2011. ? [X0] : x2_s_a12(X0) => x2_s_a12(sK153) [choice axiom]
2012. x2_s_a12(sK153) [skolemisation 267,2011]
2074. ? [X1] : code_ok(X1) => code_ok(sK184) [choice axiom]
2075. ? [X4] : manual(X4) => manual(sK185) [choice axiom]
2076. ! [X0] : ((code_ok(sK184) & ! [X2] : ~manual(X2)) | (! [X3] : ~code_ok(X3) & manual(sK185)) | ~x2_s_a12(X0)) [skolemisation 1464,2075,2074]
2153. ? [X1] : manual(X1) => manual(sK227) [choice axiom]
2154. ! [X0] : (manual(sK227) | ~l_s_b10(X0)) [skolemisation 1545,2153]
2222. ? [X1] : x2_e_b2(X1) => x2_e_b2(sK263) [choice axiom]
2223. ! [X0] : (x2_e_b2(sK263) | (~manual(X0) & ~l_s_b10(X0) & ~fin(X0) & ~x2_s_b3(X0))) [skolemisation 1597,2222]
2294. ? [X1] : (release(X1) | l_s_b11(X1)) => (release(sK300) | l_s_b11(sK300)) [choice axiom]
2295. ! [X0] : ((release(sK300) | l_s_b11(sK300)) | (~x2_e_b2(X0) & ~x2_s_b2(X0))) [skolemisation 1655,2294]
2348. ? [X0] : l_s_b10(X0) => l_s_b10(sK329) [choice axiom]
2349. l_s_b10(sK329) [skolemisation 564,2348]
2352. ? [X1] : (code_ok(X1) | l_s_b12(X1)) => (code_ok(sK331) | l_s_b12(sK331)) [choice axiom]
2353. ! [X0] : ((code_ok(sK331) | l_s_b12(sK331)) | (~release(X0) & ~l_s_b11(X0))) [skolemisation 1697,2352]
2368. ? [X1] : code_ok(X1) => code_ok(sK340) [choice axiom]
2369. ! [X0] : (code_ok(sK340) | ~l_s_b12(X0)) [skolemisation 1709,2368]
2894. x2_s_a12(sK153) [cnf transformation 2012]
2996. ~manual(X2) | ~code_ok(X3) | ~x2_s_a12(X0) [cnf transformation 2076]
3153. manual(sK227) | ~l_s_b10(X0) [cnf transformation 2154]
3264. x2_e_b2(sK263) | ~l_s_b10(X0) [cnf transformation 2223]
3367. release(sK300) | l_s_b11(sK300) | ~x2_e_b2(X0) [cnf transformation 2295]
3449. l_s_b10(sK329) [cnf transformation 2349]
3459. code_ok(sK331) | l_s_b12(sK331) | ~l_s_b11(X0) [cnf transformation 2353]
3460. code_ok(sK331) | l_s_b12(sK331) | ~release(X0) [cnf transformation 2353]
3476. code_ok(sK340) | ~l_s_b12(X0) [cnf transformation 2369]
3525. 1 <=> ! [X0] : ~code_ok(X0) [avatar definition]
3526. ~code_ok(X0) <- (1) [avatar component clause 3525]
3533. 3 <=> ! [X0] : ~manual(X0) [avatar definition]
3534. ~manual(X0) <- (3) [avatar component clause 3533]
3606. 21 <=> ! [X0] : ~release(X0) [avatar definition]
3607. ~release(X0) <- (21) [avatar component clause 3606]
4725. 271 <=> ! [X3] : ~x2_s_a12(X3) [avatar definition]
4726. ~x2_s_a12(X3) <- (271) [avatar component clause 4725]
4896. 271 | 1 | 3 [avatar split clause 2996,3533,3525,4725]
5064. 337 <=> ! [X0] : ~l_s_b10(X0) [avatar definition]
5065. ~l_s_b10(X0) <- (337) [avatar component clause 5064]
5235. 377 <=> manual(sK227) [avatar definition]
5237. manual(sK227) <- (377) [avatar component clause 5235]
5238. 337 | 377 [avatar split clause 3153,5235,5064]
5491. 432 <=> x2_e_b2(sK263) [avatar definition]
5493. x2_e_b2(sK263) <- (432) [avatar component clause 5491]
5495. 337 | 432 [avatar split clause 3264,5491,5064]
5729. 483 <=> ! [X0] : ~x2_e_b2(X0) [avatar definition]
5730. ~x2_e_b2(X0) <- (483) [avatar component clause 5729]
5732. 484 <=> l_s_b11(sK300) [avatar definition]
5734. l_s_b11(sK300) <- (484) [avatar component clause 5732]
5736. 485 <=> release(sK300) [avatar definition]
5738. release(sK300) <- (485) [avatar component clause 5736]
5739. 483 | 484 | 485 [avatar split clause 3367,5736,5732,5729]
5913. 522 <=> l_s_b12(sK331) [avatar definition]
5915. l_s_b12(sK331) <- (522) [avatar component clause 5913]
5917. 523 <=> code_ok(sK331) [avatar definition]
5919. code_ok(sK331) <- (523) [avatar component clause 5917]
5920. 21 | 522 | 523 [avatar split clause 3460,5917,5913,3606]
5922. 524 <=> ! [X0] : ~l_s_b11(X0) [avatar definition]
5923. ~l_s_b11(X0) <- (524) [avatar component clause 5922]
5924. 524 | 522 | 523 [avatar split clause 3459,5917,5913,5922]
5977. 536 <=> ! [X0] : ~l_s_b12(X0) [avatar definition]
5978. ~l_s_b12(X0) <- (536) [avatar component clause 5977]
5980. 537 <=> code_ok(sK340) [avatar definition]
5982. code_ok(sK340) <- (537) [avatar component clause 5980]
5983. 536 | 537 [avatar split clause 3476,5980,5977]
6180. $false <- (432, 483) [subsumption resolution 5493,5730]
6181. ~432 | ~483 [avatar contradiction clause 6180]
6184. $false <- (484, 524) [subsumption resolution 5734,5923]
6185. ~484 | ~524 [avatar contradiction clause 6184]
6188. $false <- (21, 485) [subsumption resolution 5738,3607]
6189. ~21 | ~485 [avatar contradiction clause 6188]
6192. $false <- (522, 536) [subsumption resolution 5915,5978]
6193. ~522 | ~536 [avatar contradiction clause 6192]
6194. $false <- (1, 537) [subsumption resolution 5982,3526]
6195. ~1 | ~537 [avatar contradiction clause 6194]
6196. $false <- (1, 523) [subsumption resolution 5919,3526]
6197. ~1 | ~523 [avatar contradiction clause 6196]
6360. $false <- (271) [resolution 4726,2894]
6361. ~271 [avatar contradiction clause 6360]
6372. $false <- (337) [resolution 5065,3449]
6373. ~337 [avatar contradiction clause 6372]
6374. $false <- (3, 377) [subsumption resolution 5237,3534]
6375. ~3 | ~377 [avatar contradiction clause 6374]
6376. $false [avatar sat refutation 4896,5238,5495,5739,5920,5924,5983,6181,6185,6189,6193,6195,6197,6361,6373,6375]
% SZS output end Proof for tptp_IMPLIES
% ------------------------------
% 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]: 4172
% Time elapsed: 0.023 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.)
