% 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
46. ! [X1] : (x2_s_a17(X1) => ((? [X4] : (a4_e_a6(X4) | a4_s_a6(X4)) & ~? [X3] : (x2_e_a22(X3) | x2_s_a18(X3))) | (~? [X2] : (a4_e_a6(X2) | a4_s_a6(X2)) & ? [X0] : (x2_e_a22(X0) | x2_s_a18(X0))))) [input]
246. ? [X0] : x2_s_a18(X0) [input]
268. ? [X0] : a4_s_a6(X0) [input]
314. ? [X0] : x2_s_a17(X0) [input]
654. ! [X0] : (x2_s_a17(X0) => ((? [X1] : (a4_e_a6(X1) | a4_s_a6(X1)) & ~? [X2] : (x2_e_a22(X2) | x2_s_a18(X2))) | (~? [X3] : (a4_e_a6(X3) | a4_s_a6(X3)) & ? [X4] : (x2_e_a22(X4) | x2_s_a18(X4))))) [rectify 46]
1235. ! [X0] : (((? [X1] : (a4_e_a6(X1) | a4_s_a6(X1)) & ! [X2] : (~x2_e_a22(X2) & ~x2_s_a18(X2))) | (! [X3] : (~a4_e_a6(X3) & ~a4_s_a6(X3)) & ? [X4] : (x2_e_a22(X4) | x2_s_a18(X4)))) | ~x2_s_a17(X0)) [ennf transformation 654]
1236. ! [X0] : ((? [X1] : (a4_e_a6(X1) | a4_s_a6(X1)) & ! [X2] : (~x2_e_a22(X2) & ~x2_s_a18(X2))) | (! [X3] : (~a4_e_a6(X3) & ~a4_s_a6(X3)) & ? [X4] : (x2_e_a22(X4) | x2_s_a18(X4))) | ~x2_s_a17(X0)) [flattening 1235]
1798. (! [X3] : (~a4_e_a6(X3) & ~a4_s_a6(X3)) & ? [X4] : (x2_e_a22(X4) | x2_s_a18(X4))) | ~sP0 [predicate definition introduction]
1799. ! [X0] : ((? [X1] : (a4_e_a6(X1) | a4_s_a6(X1)) & ! [X2] : (~x2_e_a22(X2) & ~x2_s_a18(X2))) | sP0 | ~x2_s_a17(X0)) [definition folding 1236,1798]
1851. (! [X3] : (~a4_e_a6(X3) & ~a4_s_a6(X3)) & ? [X4] : (x2_e_a22(X4) | x2_s_a18(X4))) | ~sP0 [nnf transformation 1798]
1852. (! [X0] : (~a4_e_a6(X0) & ~a4_s_a6(X0)) & ? [X1] : (x2_e_a22(X1) | x2_s_a18(X1))) | ~sP0 [rectify 1851]
1853. ? [X1] : (x2_e_a22(X1) | x2_s_a18(X1)) => (x2_e_a22(sK31) | x2_s_a18(sK31)) [choice axiom]
1854. (! [X0] : (~a4_e_a6(X0) & ~a4_s_a6(X0)) & (x2_e_a22(sK31) | x2_s_a18(sK31))) | ~sP0 [skolemisation 1852,1853]
1855. ? [X1] : (a4_e_a6(X1) | a4_s_a6(X1)) => (a4_e_a6(sK32) | a4_s_a6(sK32)) [choice axiom]
1856. ! [X0] : (((a4_e_a6(sK32) | a4_s_a6(sK32)) & ! [X2] : (~x2_e_a22(X2) & ~x2_s_a18(X2))) | sP0 | ~x2_s_a17(X0)) [skolemisation 1799,1855]
2032. ? [X0] : x2_s_a18(X0) => x2_s_a18(sK129) [choice axiom]
2033. x2_s_a18(sK129) [skolemisation 246,2032]
2055. ? [X0] : a4_s_a6(X0) => a4_s_a6(sK143) [choice axiom]
2056. a4_s_a6(sK143) [skolemisation 268,2055]
2116. ? [X0] : x2_s_a17(X0) => x2_s_a17(sK174) [choice axiom]
2117. x2_s_a17(sK174) [skolemisation 314,2116]
2553. ~a4_s_a6(X0) | ~sP0 [cnf transformation 1854]
2555. ~x2_s_a18(X2) | sP0 | ~x2_s_a17(X0) [cnf transformation 1856]
2920. x2_s_a18(sK129) [cnf transformation 2033]
2962. a4_s_a6(sK143) [cnf transformation 2056]
3056. x2_s_a17(sK174) [cnf transformation 2117]
3887. 52 <=> ! [X0] : ~x2_s_a18(X0) [avatar definition]
3888. ~x2_s_a18(X0) <- (52) [avatar component clause 3887]
3917. 59 <=> sP0 [avatar definition]
3925. 61 <=> ! [X0] : ~a4_s_a6(X0) [avatar definition]
3926. ~a4_s_a6(X0) <- (61) [avatar component clause 3925]
3927. ~59 | 61 [avatar split clause 2553,3925,3917]
3938. 64 <=> ! [X0] : ~x2_s_a17(X0) [avatar definition]
3939. ~x2_s_a17(X0) <- (64) [avatar component clause 3938]
3953. 64 | 59 | 52 [avatar split clause 2555,3887,3917,3938]
6500. $false <- (52) [resolution 3888,2920]
6501. ~52 [avatar contradiction clause 6500]
6542. $false <- (61) [resolution 3926,2962]
6543. ~61 [avatar contradiction clause 6542]
6562. $false <- (64) [resolution 3939,3056]
6563. ~64 [avatar contradiction clause 6562]
6564. $false [avatar sat refutation 3927,3953,6501,6543,6563]
% 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]: 4385
% Time elapsed: 0.031 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.)
