% Running in auto input_syntax mode. Trying TPTP
% Refutation found. Thanks to Tanya!
% SZS status Theorem for tptp_EQUIVALENT
% SZS output start Proof for tptp_EQUIVALENT
364. ! [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]
440. ! [X1] : (l_s_b9(X1) => ? [X0] : fin(X0)) [input]
482. ? [X0] : l_s_b6(X0) [input]
486. ! [X1] : ((x3_e_b4(X1) | x3_s_b4(X1) | tau_b2(X1)) => ? [X0] : x2_e_b3(X0)) [input]
564. ? [X0] : l_s_b10(X0) [input]
571. ? [X0] : x2_s_b2(X0) [input]
587. ! [X1] : ((x2_e_b3(X1) | x2_s_b3(X1)) => ? [X0] : (fin(X0) | l_s_b9(X0))) [input]
600. ! [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]
602. ! [X1] : ((reopen(X1) | l_s_b6(X1) | tau_b8(X1)) => ? [X0] : x2_e_b6(X0)) [input]
715. ! [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 364]
743. ! [X0] : (l_s_b9(X0) => ? [X1] : fin(X1)) [rectify 440]
758. ! [X0] : ((x3_e_b4(X0) | x3_s_b4(X0) | tau_b2(X0)) => ? [X1] : x2_e_b3(X1)) [rectify 486]
790. ! [X0] : ((x2_e_b3(X0) | x2_s_b3(X0)) => ? [X1] : (fin(X1) | l_s_b9(X1))) [rectify 587]
795. ! [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 600]
797. ! [X0] : ((reopen(X0) | l_s_b6(X0) | tau_b8(X0)) => ? [X1] : x2_e_b6(X1)) [rectify 602]
1150. ! [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 715]
1151. ! [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 1150]
1223. ! [X0] : (? [X1] : fin(X1) | ~l_s_b9(X0)) [ennf transformation 743]
1263. ! [X0] : (? [X1] : x2_e_b3(X1) | (~x3_e_b4(X0) & ~x3_s_b4(X0) & ~tau_b2(X0))) [ennf transformation 758]
1359. ! [X0] : (? [X1] : (fin(X1) | l_s_b9(X1)) | (~x2_e_b3(X0) & ~x2_s_b3(X0))) [ennf transformation 790]
1374. ! [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 795]
1377. ! [X0] : (? [X1] : x2_e_b6(X1) | (~reopen(X0) & ~l_s_b6(X0) & ~tau_b8(X0))) [ennf transformation 797]
1385. (! [X3] : (~manual(X3) & ~l_s_b10(X3)) & ? [X4] : (fin(X4) | x2_s_b3(X4))) | ~sP2 [predicate definition introduction]
1386. ! [X0] : ((? [X1] : (manual(X1) | l_s_b10(X1)) & ! [X2] : (~fin(X2) & ~x2_s_b3(X2))) | sP2 | ~x2_s_b2(X0)) [definition folding 1151,1385]
1755. (! [X3] : (~manual(X3) & ~l_s_b10(X3)) & ? [X4] : (fin(X4) | x2_s_b3(X4))) | ~sP2 [nnf transformation 1385]
1756. (! [X0] : (~manual(X0) & ~l_s_b10(X0)) & ? [X1] : (fin(X1) | x2_s_b3(X1))) | ~sP2 [rectify 1755]
1757. ? [X1] : (fin(X1) | x2_s_b3(X1)) => (fin(sK205) | x2_s_b3(sK205)) [choice axiom]
1758. (! [X0] : (~manual(X0) & ~l_s_b10(X0)) & (fin(sK205) | x2_s_b3(sK205))) | ~sP2 [skolemisation 1756,1757]
1759. ? [X1] : (manual(X1) | l_s_b10(X1)) => (manual(sK206) | l_s_b10(sK206)) [choice axiom]
1760. ! [X0] : (((manual(sK206) | l_s_b10(sK206)) & ! [X2] : (~fin(X2) & ~x2_s_b3(X2))) | sP2 | ~x2_s_b2(X0)) [skolemisation 1386,1759]
1854. ? [X1] : fin(X1) => fin(sK255) [choice axiom]
1855. ! [X0] : (fin(sK255) | ~l_s_b9(X0)) [skolemisation 1223,1854]
1901. ? [X0] : l_s_b6(X0) => l_s_b6(sK280) [choice axiom]
1902. l_s_b6(sK280) [skolemisation 482,1901]
1905. ? [X1] : x2_e_b3(X1) => x2_e_b3(sK282) [choice axiom]
1906. ! [X0] : (x2_e_b3(sK282) | (~x3_e_b4(X0) & ~x3_s_b4(X0) & ~tau_b2(X0))) [skolemisation 1263,1905]
1994. ? [X0] : l_s_b10(X0) => l_s_b10(sK329) [choice axiom]
1995. l_s_b10(sK329) [skolemisation 564,1994]
2000. ? [X0] : x2_s_b2(X0) => x2_s_b2(sK332) [choice axiom]
2001. x2_s_b2(sK332) [skolemisation 571,2000]
2018. ? [X1] : (fin(X1) | l_s_b9(X1)) => (fin(sK342) | l_s_b9(sK342)) [choice axiom]
2019. ! [X0] : ((fin(sK342) | l_s_b9(sK342)) | (~x2_e_b3(X0) & ~x2_s_b3(X0))) [skolemisation 1359,2018]
2030. ? [X1] : x3_e_b4(X1) => x3_e_b4(sK349) [choice axiom]
2031. ! [X0] : (x3_e_b4(sK349) | (~change_end(X0) & ~l_s_b8(X0) & ~change_diagn(X0) & ~l_s_b7(X0) & ~x2_e_b6(X0) & ~x2_s_b5(X0))) [skolemisation 1374,2030]
2035. ? [X1] : x2_e_b6(X1) => x2_e_b6(sK352) [choice axiom]
2036. ! [X0] : (x2_e_b6(sK352) | (~reopen(X0) & ~l_s_b6(X0) & ~tau_b8(X0))) [skolemisation 1377,2035]
2729. ~l_s_b10(X0) | ~sP2 [cnf transformation 1758]
2732. ~fin(X2) | sP2 | ~x2_s_b2(X0) [cnf transformation 1760]
2878. fin(sK255) | ~l_s_b9(X0) [cnf transformation 1855]
2951. l_s_b6(sK280) [cnf transformation 1902]
2961. x2_e_b3(sK282) | ~x3_e_b4(X0) [cnf transformation 1906]
3099. l_s_b10(sK329) [cnf transformation 1995]
3111. x2_s_b2(sK332) [cnf transformation 2001]
3137. fin(sK342) | l_s_b9(sK342) | ~x2_e_b3(X0) [cnf transformation 2019]
3158. x3_e_b4(sK349) | ~x2_e_b6(X0) [cnf transformation 2031]
3168. x2_e_b6(sK352) | ~l_s_b6(X0) [cnf transformation 2036]
92390. 86 <=> ! [X3] : ~fin(X3) [avatar definition]
92391. ~fin(X3) <- (86) [avatar component clause 92390]
93549. 333 <=> ! [X3] : ~l_s_b6(X3) [avatar definition]
93550. ~l_s_b6(X3) <- (333) [avatar component clause 93549]
93564. 336 <=> sP2 [avatar definition]
93569. 337 <=> ! [X0] : ~l_s_b10(X0) [avatar definition]
93570. ~l_s_b10(X0) <- (337) [avatar component clause 93569]
93571. ~336 | 337 [avatar split clause 2729,93569,93564]
93582. 340 <=> ! [X0] : ~x2_s_b2(X0) [avatar definition]
93583. ~x2_s_b2(X0) <- (340) [avatar component clause 93582]
93593. 340 | 336 | 86 [avatar split clause 2732,92390,93564,93582]
93876. 407 <=> ! [X2] : ~x2_e_b6(X2) [avatar definition]
93877. ~x2_e_b6(X2) <- (407) [avatar component clause 93876]
93936. 419 <=> ! [X0] : ~l_s_b9(X0) [avatar definition]
93937. ~l_s_b9(X0) <- (419) [avatar component clause 93936]
93939. 420 <=> fin(sK255) [avatar definition]
93941. fin(sK255) <- (420) [avatar component clause 93939]
93942. 419 | 420 [avatar split clause 2878,93939,93936]
93963. 425 <=> ! [X3] : ~x3_e_b4(X3) [avatar definition]
93964. ~x3_e_b4(X3) <- (425) [avatar component clause 93963]
94111. 457 <=> x2_e_b3(sK282) [avatar definition]
94113. x2_e_b3(sK282) <- (457) [avatar component clause 94111]
94114. 425 | 457 [avatar split clause 2961,94111,93963]
94496. 539 <=> ! [X0] : ~x2_e_b3(X0) [avatar definition]
94497. ~x2_e_b3(X0) <- (539) [avatar component clause 94496]
94499. 540 <=> l_s_b9(sK342) [avatar definition]
94501. l_s_b9(sK342) <- (540) [avatar component clause 94499]
94503. 541 <=> fin(sK342) [avatar definition]
94505. fin(sK342) <- (541) [avatar component clause 94503]
94506. 539 | 540 | 541 [avatar split clause 3137,94503,94499,94496]
94539. 548 <=> x3_e_b4(sK349) [avatar definition]
94541. x3_e_b4(sK349) <- (548) [avatar component clause 94539]
94546. 407 | 548 [avatar split clause 3158,94539,93876]
94564. 552 <=> x2_e_b6(sK352) [avatar definition]
94566. x2_e_b6(sK352) <- (552) [avatar component clause 94564]
94568. 333 | 552 [avatar split clause 3168,94564,93549]
185936. $false <- (407, 552) [subsumption resolution 94566,93877]
185937. ~407 | ~552 [avatar contradiction clause 185936]
185938. $false <- (425, 548) [subsumption resolution 94541,93964]
185939. ~425 | ~548 [avatar contradiction clause 185938]
185940. $false <- (457, 539) [subsumption resolution 94113,94497]
185941. ~457 | ~539 [avatar contradiction clause 185940]
185944. $false <- (419, 540) [subsumption resolution 94501,93937]
185945. ~419 | ~540 [avatar contradiction clause 185944]
185948. $false <- (86, 420) [subsumption resolution 93941,92391]
185949. ~86 | ~420 [avatar contradiction clause 185948]
185950. $false <- (86, 541) [subsumption resolution 94505,92391]
185951. ~86 | ~541 [avatar contradiction clause 185950]
186108. $false <- (333) [resolution 93550,2951]
186109. ~333 [avatar contradiction clause 186108]
186110. $false <- (337) [resolution 93570,3099]
186111. ~337 [avatar contradiction clause 186110]
186116. $false <- (340) [resolution 93583,3111]
186117. ~340 [avatar contradiction clause 186116]
186118. $false [avatar sat refutation 93571,93593,93942,94114,94506,94546,94568,185937,185939,185941,185945,185949,185951,186109,186111,186117]
% SZS output end Proof for tptp_EQUIVALENT
% ------------------------------
% 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]: 63515
% Time elapsed: 0.357 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.)
