% 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
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]
873. ! [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]
874. ! [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 873]
1437. (! [X3] : (~a4_e_a6(X3) & ~a4_s_a6(X3)) & ? [X4] : (x2_e_a22(X4) | x2_s_a18(X4))) | ~sP0 [predicate definition introduction]
1438. ! [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 874,1437]
1490. (! [X3] : (~a4_e_a6(X3) & ~a4_s_a6(X3)) & ? [X4] : (x2_e_a22(X4) | x2_s_a18(X4))) | ~sP0 [nnf transformation 1437]
1491. (! [X0] : (~a4_e_a6(X0) & ~a4_s_a6(X0)) & ? [X1] : (x2_e_a22(X1) | x2_s_a18(X1))) | ~sP0 [rectify 1490]
1492. ? [X1] : (x2_e_a22(X1) | x2_s_a18(X1)) => (x2_e_a22(sK31) | x2_s_a18(sK31)) [choice axiom]
1493. (! [X0] : (~a4_e_a6(X0) & ~a4_s_a6(X0)) & (x2_e_a22(sK31) | x2_s_a18(sK31))) | ~sP0 [skolemisation 1491,1492]
1494. ? [X1] : (a4_e_a6(X1) | a4_s_a6(X1)) => (a4_e_a6(sK32) | a4_s_a6(sK32)) [choice axiom]
1495. ! [X0] : (((a4_e_a6(sK32) | a4_s_a6(sK32)) & ! [X2] : (~x2_e_a22(X2) & ~x2_s_a18(X2))) | sP0 | ~x2_s_a17(X0)) [skolemisation 1438,1494]
1671. ? [X0] : x2_s_a18(X0) => x2_s_a18(sK129) [choice axiom]
1672. x2_s_a18(sK129) [skolemisation 246,1671]
1694. ? [X0] : a4_s_a6(X0) => a4_s_a6(sK143) [choice axiom]
1695. a4_s_a6(sK143) [skolemisation 268,1694]
1755. ? [X0] : x2_s_a17(X0) => x2_s_a17(sK174) [choice axiom]
1756. x2_s_a17(sK174) [skolemisation 314,1755]
2196. ~a4_s_a6(X0) | ~sP0 [cnf transformation 1493]
2198. ~x2_s_a18(X2) | sP0 | ~x2_s_a17(X0) [cnf transformation 1495]
2563. x2_s_a18(sK129) [cnf transformation 1672]
2605. a4_s_a6(sK143) [cnf transformation 1695]
2699. x2_s_a17(sK174) [cnf transformation 1756]
103167. 52 <=> ! [X0] : ~x2_s_a18(X0) [avatar definition]
103168. ~x2_s_a18(X0) <- (52) [avatar component clause 103167]
103197. 59 <=> sP0 [avatar definition]
103205. 61 <=> ! [X0] : ~a4_s_a6(X0) [avatar definition]
103206. ~a4_s_a6(X0) <- (61) [avatar component clause 103205]
103207. ~59 | 61 [avatar split clause 2196,103205,103197]
103218. 64 <=> ! [X0] : ~x2_s_a17(X0) [avatar definition]
103219. ~x2_s_a17(X0) <- (64) [avatar component clause 103218]
103233. 64 | 59 | 52 [avatar split clause 2198,103167,103197,103218]
207961. $false <- (52) [resolution 103168,2563]
207962. ~52 [avatar contradiction clause 207961]
207987. $false <- (61) [resolution 103206,2605]
207988. ~61 [avatar contradiction clause 207987]
208007. $false <- (64) [resolution 103219,2699]
208008. ~64 [avatar contradiction clause 208007]
208009. $false [avatar sat refutation 103207,103233,207962,207988,208008]
% 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]: 77916
% Time elapsed: 0.417 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.)
