%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : SYN374+1 : TPTP v9.0.0. Released v2.0.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n001.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sat Jun 21 05:38:55 AM UTC 2025
% Result : Theorem 0.19s 0.37s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : SYN374+1 : TPTP v9.0.0. Released v2.0.0.
% 0.00/0.11 % Command : run_E %s %d THM
% 0.11/0.33 % Computer : n001.cluster.edu
% 0.11/0.33 % Model : x86_64 x86_64
% 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.33 % Memory : 8042.1875MB
% 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.33 % CPULimit : 300
% 0.11/0.33 % WCLimit : 300
% 0.11/0.33 % DateTime : Fri Jun 20 12:37:20 EDT 2025
% 0.11/0.33 % CPUTime :
% 0.19/0.37 % SZS status Theorem
% 0.19/0.37 % SZS output start Proof
% 0.19/0.37 tff(big_p_type, type, (
% 0.19/0.37 big_p: $i > $o)).
% 0.19/0.37 tff(tptp_fun_Y_3_type, type, (
% 0.19/0.37 tptp_fun_Y_3: $i)).
% 0.19/0.37 tff(tptp_fun_X_0_type, type, (
% 0.19/0.37 tptp_fun_X_0: $i)).
% 0.19/0.37 tff(tptp_fun_X_2_type, type, (
% 0.19/0.37 tptp_fun_X_2: $i)).
% 0.19/0.37 tff(tptp_fun_Y_1_type, type, (
% 0.19/0.37 tptp_fun_Y_1: $i > $i)).
% 0.19/0.37 tff(elem_4_type, type, (
% 0.19/0.37 elem_4: $i)).
% 0.19/0.37 tff(1,assumption,(![X: $i] : (~big_p(X)) | ![Y: $i] : big_p(Y)), introduced(assumption)).
% 0.19/0.37 tff(2,assumption,(~(big_p(X!2) | ![Y: $i] : big_p(Y))), introduced(assumption)).
% 0.19/0.37 tff(3,plain,
% 0.19/0.37 (((~(big_p(X!2) | ![Y: $i] : big_p(Y))) | (~((~big_p(Y!3)) | ![X: $i] : (~big_p(X))))) | (big_p(X!2) | ![Y: $i] : big_p(Y))),
% 0.19/0.37 inference(tautology,[status(thm)],[])).
% 0.19/0.37 tff(4,plain,
% 0.19/0.37 ((~(big_p(X!2) | ![Y: $i] : big_p(Y))) | (~((~big_p(Y!3)) | ![X: $i] : (~big_p(X))))),
% 0.19/0.37 inference(unit_resolution,[status(thm)],[3, 2])).
% 0.19/0.37 tff(5,plain,
% 0.19/0.37 ((![X: $i] : (~(big_p(X) <=> big_p(tptp_fun_Y_1(X)))) | (~((~(big_p(X!2) | ![Y: $i] : big_p(Y))) | (~((~big_p(Y!3)) | ![X: $i] : (~big_p(X))))))) <=> (![X: $i] : (~(big_p(X) <=> big_p(tptp_fun_Y_1(X)))) | (~((~(big_p(X!2) | ![Y: $i] : big_p(Y))) | (~((~big_p(Y!3)) | ![X: $i] : (~big_p(X)))))))),
% 0.19/0.37 inference(rewrite,[status(thm)],[])).
% 0.19/0.37 tff(6,plain,
% 0.19/0.37 ((~((~(big_p(X!2) | ![Y: $i] : big_p(Y))) | (~(![X: $i] : (~big_p(X)) | (~big_p(Y!3)))))) <=> (~((~(big_p(X!2) | ![Y: $i] : big_p(Y))) | (~((~big_p(Y!3)) | ![X: $i] : (~big_p(X))))))),
% 0.19/0.37 inference(rewrite,[status(thm)],[])).
% 0.19/0.37 tff(7,plain,
% 0.19/0.37 ((![X: $i] : (~(big_p(X) <=> big_p(tptp_fun_Y_1(X)))) | (~((~(big_p(X!2) | ![Y: $i] : big_p(Y))) | (~(![X: $i] : (~big_p(X)) | (~big_p(Y!3))))))) <=> (![X: $i] : (~(big_p(X) <=> big_p(tptp_fun_Y_1(X)))) | (~((~(big_p(X!2) | ![Y: $i] : big_p(Y))) | (~((~big_p(Y!3)) | ![X: $i] : (~big_p(X)))))))),
% 0.19/0.37 inference(monotonicity,[status(thm)],[6])).
% 0.19/0.37 tff(8,plain,
% 0.19/0.37 ((![X: $i] : (~(big_p(X) <=> big_p(tptp_fun_Y_1(X)))) | (~((~(big_p(X!2) | ![Y: $i] : big_p(Y))) | (~(![X: $i] : (~big_p(X)) | (~big_p(Y!3))))))) <=> (![X: $i] : (~(big_p(X) <=> big_p(tptp_fun_Y_1(X)))) | (~((~(big_p(X!2) | ![Y: $i] : big_p(Y))) | (~((~big_p(Y!3)) | ![X: $i] : (~big_p(X)))))))),
% 0.19/0.37 inference(transitivity,[status(thm)],[7, 5])).
% 0.19/0.37 tff(9,plain,
% 0.19/0.37 ((![X: $i] : (~(big_p(X) <=> big_p(tptp_fun_Y_1(X)))) | (~((~(big_p(X!2) | ![Y: $i] : big_p(Y))) | (~(![X: $i] : (~big_p(X)) | (~big_p(Y!3))))))) <=> (![X: $i] : (~(big_p(X) <=> big_p(tptp_fun_Y_1(X)))) | (~((~(big_p(X!2) | ![Y: $i] : big_p(Y))) | (~(![X: $i] : (~big_p(X)) | (~big_p(Y!3)))))))),
% 0.19/0.37 inference(rewrite,[status(thm)],[])).
% 0.19/0.37 tff(10,plain,
% 0.19/0.37 ((![X: $i] : (~(big_p(X) <=> big_p(tptp_fun_Y_1(X)))) | (~((~(big_p(X!2) | ![Y: $i] : big_p(Y))) | (~(![X: $i] : (~big_p(X)) | (~big_p(Y!3))))))) <=> (![X: $i] : (~(big_p(X) <=> big_p(tptp_fun_Y_1(X)))) | (~((~(big_p(X!2) | ![Y: $i] : big_p(Y))) | (~(![X: $i] : (~big_p(X)) | (~big_p(Y!3)))))))),
% 0.19/0.37 inference(rewrite,[status(thm)],[])).
% 0.19/0.37 tff(11,plain,
% 0.19/0.37 (((big_p(X!2) | ![Y: $i] : big_p(Y)) & (![X: $i] : (~big_p(X)) | (~big_p(Y!3)))) <=> (~((~(big_p(X!2) | ![Y: $i] : big_p(Y))) | (~(![X: $i] : (~big_p(X)) | (~big_p(Y!3))))))),
% 0.19/0.37 inference(rewrite,[status(thm)],[])).
% 0.19/0.37 tff(12,plain,
% 0.19/0.37 ((![X: $i] : (~big_p(X)) | (~big_p(Y!3))) <=> (![X: $i] : (~big_p(X)) | (~big_p(Y!3)))),
% 0.19/0.37 inference(rewrite,[status(thm)],[])).
% 0.19/0.37 tff(13,plain,
% 0.19/0.37 (((big_p(X!2) | ![Y: $i] : big_p(Y)) & (![X: $i] : (~big_p(X)) | (~big_p(Y!3)))) <=> ((big_p(X!2) | ![Y: $i] : big_p(Y)) & (![X: $i] : (~big_p(X)) | (~big_p(Y!3))))),
% 0.19/0.37 inference(monotonicity,[status(thm)],[12])).
% 0.19/0.37 tff(14,plain,
% 0.19/0.37 (((big_p(X!2) | ![Y: $i] : big_p(Y)) & (![X: $i] : (~big_p(X)) | (~big_p(Y!3)))) <=> (~((~(big_p(X!2) | ![Y: $i] : big_p(Y))) | (~(![X: $i] : (~big_p(X)) | (~big_p(Y!3))))))),
% 0.19/0.37 inference(transitivity,[status(thm)],[13, 11])).
% 0.19/0.37 tff(15,plain,
% 0.19/0.37 ((![X: $i] : (~(big_p(X) <=> big_p(tptp_fun_Y_1(X)))) | ((big_p(X!2) | ![Y: $i] : big_p(Y)) & (![X: $i] : (~big_p(X)) | (~big_p(Y!3))))) <=> (![X: $i] : (~(big_p(X) <=> big_p(tptp_fun_Y_1(X)))) | (~((~(big_p(X!2) | ![Y: $i] : big_p(Y))) | (~(![X: $i] : (~big_p(X)) | (~big_p(Y!3)))))))),
% 0.19/0.37 inference(monotonicity,[status(thm)],[14])).
% 0.19/0.37 tff(16,plain,
% 0.19/0.37 ((![X: $i] : (~(big_p(X) <=> big_p(tptp_fun_Y_1(X)))) | ((big_p(X!2) | ![Y: $i] : big_p(Y)) & (![X: $i] : (~big_p(X)) | (~big_p(Y!3))))) <=> (![X: $i] : (~(big_p(X) <=> big_p(tptp_fun_Y_1(X)))) | (~((~(big_p(X!2) | ![Y: $i] : big_p(Y))) | (~(![X: $i] : (~big_p(X)) | (~big_p(Y!3)))))))),
% 0.19/0.37 inference(transitivity,[status(thm)],[15, 10])).
% 0.19/0.37 tff(17,plain,
% 0.19/0.37 (((![Y: $i] : (big_p(X!0) <=> big_p(Y)) | ((![X: $i] : (~big_p(X)) | ![Y: $i] : big_p(Y)) & (big_p(X!2) | (~big_p(Y!3))))) & (![X: $i] : (~(big_p(X) <=> big_p(tptp_fun_Y_1(X)))) | ((big_p(X!2) | ![Y: $i] : big_p(Y)) & (![X: $i] : (~big_p(X)) | (~big_p(Y!3)))))) <=> ((![Y: $i] : (big_p(X!0) <=> big_p(Y)) | ((![X: $i] : (~big_p(X)) | ![Y: $i] : big_p(Y)) & (big_p(X!2) | (~big_p(Y!3))))) & (![X: $i] : (~(big_p(X) <=> big_p(tptp_fun_Y_1(X)))) | ((big_p(X!2) | ![Y: $i] : big_p(Y)) & (![X: $i] : (~big_p(X)) | (~big_p(Y!3))))))),
% 0.19/0.37 inference(rewrite,[status(thm)],[])).
% 0.19/0.37 tff(18,plain,
% 0.19/0.37 ((~(?[X: $i] : ![Y: $i] : (big_p(X) <=> big_p(Y)) <=> (?[X: $i] : big_p(X) <=> ![Y: $i] : big_p(Y)))) <=> (~(?[X: $i] : ![Y: $i] : (big_p(X) <=> big_p(Y)) <=> (?[X: $i] : big_p(X) <=> ![Y: $i] : big_p(Y))))),
% 0.19/0.37 inference(rewrite,[status(thm)],[])).
% 0.19/0.37 tff(19,plain,
% 0.19/0.37 ((?[X: $i] : ![Y: $i] : (big_p(X) <=> big_p(Y)) <=> (?[X: $i] : big_p(X) <=> ![Y: $i] : big_p(Y))) <=> (?[X: $i] : ![Y: $i] : (big_p(X) <=> big_p(Y)) <=> (?[X: $i] : big_p(X) <=> ![Y: $i] : big_p(Y)))),
% 0.19/0.37 inference(rewrite,[status(thm)],[])).
% 0.19/0.37 tff(20,plain,
% 0.19/0.37 ((~(?[X: $i] : ![Y: $i] : (big_p(X) <=> big_p(Y)) <=> (?[X: $i] : big_p(X) <=> ![Y: $i] : big_p(Y)))) <=> (~(?[X: $i] : ![Y: $i] : (big_p(X) <=> big_p(Y)) <=> (?[X: $i] : big_p(X) <=> ![Y: $i] : big_p(Y))))),
% 0.19/0.37 inference(monotonicity,[status(thm)],[19])).
% 0.19/0.37 tff(21,plain,
% 0.19/0.37 ((~(?[X: $i] : ![Y: $i] : (big_p(X) <=> big_p(Y)) <=> (?[X: $i] : big_p(X) <=> ![Y: $i] : big_p(Y)))) <=> (~(?[X: $i] : ![Y: $i] : (big_p(X) <=> big_p(Y)) <=> (?[X: $i] : big_p(X) <=> ![Y: $i] : big_p(Y))))),
% 0.19/0.37 inference(transitivity,[status(thm)],[20, 18])).
% 0.19/0.37 tff(22,axiom,(~(?[X: $i] : ![Y: $i] : (big_p(X) <=> big_p(Y)) <=> (?[X: $i] : big_p(X) <=> ![Y: $i] : big_p(Y)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','x2125')).
% 0.19/0.37 tff(23,plain,
% 0.19/0.37 (~(?[X: $i] : ![Y: $i] : (big_p(X) <=> big_p(Y)) <=> (?[X: $i] : big_p(X) <=> ![Y: $i] : big_p(Y)))),
% 0.19/0.37 inference(modus_ponens,[status(thm)],[22, 21])).
% 0.19/0.37 tff(24,plain,
% 0.19/0.37 (~(?[X: $i] : ![Y: $i] : (big_p(X) <=> big_p(Y)) <=> (?[X: $i] : big_p(X) <=> ![Y: $i] : big_p(Y)))),
% 0.19/0.37 inference(modus_ponens,[status(thm)],[23, 21])).
% 0.19/0.37 tff(25,plain,
% 0.19/0.37 (~(?[X: $i] : ![Y: $i] : (big_p(X) <=> big_p(Y)) <=> (?[X: $i] : big_p(X) <=> ![Y: $i] : big_p(Y)))),
% 0.19/0.37 inference(modus_ponens,[status(thm)],[24, 18])).
% 0.19/0.37 tff(26,plain,
% 0.19/0.37 (~(?[X: $i] : ![Y: $i] : (big_p(X) <=> big_p(Y)) <=> (?[X: $i] : big_p(X) <=> ![Y: $i] : big_p(Y)))),
% 0.19/0.37 inference(modus_ponens,[status(thm)],[25, 21])).
% 0.19/0.37 unexpected number of arguments: (let ((a!1 (exists ((X $i)) (forall ((Y $i)) (= (big_p X) (big_p Y)))))
% 0.19/0.37 (a!2 (forall ((Y $i)) (= (big_p X!0) (big_p Y))))
% 0.19/0.37 (a!3 (lambda ((Y $i))
% 0.19/0.37 (refl (~ (= (big_p X!0) (big_p Y)) (= (big_p X!0) (big_p Y))))))
% 0.19/0.37 (a!4 (lambda ((X $i))
% 0.19/0.37 (let ((a!1 (forall ((Y $i)) (= (big_p X) (big_p Y))))
% 0.19/0.37 (a!2 (not (= (big_p X) (big_p (Y!1 X))))))
% 0.19/0.37 (sk (~ (not a!1) a!2)))))
% 0.19/0.37 (a!5 (forall ((X $i)) (not (= (big_p X) (big_p (Y!1 X))))))
% 0.19/0.37 (a!6 (exists ((X $i)) (big_p X)))
% 0.19/0.37 (a!7 (lambda ((X $i)) (refl (~ (not (big_p X)) (not (big_p X))))))
% 0.19/0.37 (a!8 (forall ((X $i)) (not (big_p X))))
% 0.19/0.37 (a!9 (lambda ((Y $i)) (refl (~ (big_p Y) (big_p Y)))))
% 0.19/0.37 (a!10 (forall ((Y $i)) (big_p Y))))
% 0.19/0.37 (let ((a!11 (sk (~ (not a!10) (not (big_p Y!3)))))
% 0.19/0.37 (a!12 (and (or a!8 a!10) (or (big_p X!2) (not (big_p Y!3)))))
% 0.19/0.37 (a!14 (and (or (big_p X!2) a!10) (or a!8 (not (big_p Y!3))))))
% 0.19/0.37 (let ((a!13 (nnf-pos (sk (~ a!6 (big_p X!2)))
% 0.19/0.37 (nnf-neg (proof-bind a!7) (~ (not a!6) a!8))
% 0.19/0.37 (nnf-pos (proof-bind a!9) (~ a!10 a!10))
% 0.19/0.37 a!11
% 0.19/0.37 (~ (= a!6 a!10) a!12)))
% 0.19/0.37 (a!15 (nnf-neg (sk (~ a!6 (big_p X!2)))
% 0.19/0.37 (nnf-neg (proof-bind a!7) (~ (not a!6) a!8))
% 0.19/0.37 (nnf-pos (proof-bind a!9) (~ a!10 a!10))
% 0.19/0.37 a!11
% 0.19/0.37 (~ (not (= a!6 a!10)) a!14)))
% 0.19/0.37 (a!16 (~ (not (= a!1 (= a!6 a!10))) (and (or a!2 a!12) (or a!5 a!14)))))
% 0.19/0.37 (nnf-neg (trans (sk (~ a!1 a!2))
% 0.19/0.37 (nnf-pos (proof-bind a!3) (~ a!2 a!2))
% 0.19/0.37 (~ a!1 a!2))
% 0.19/0.37 (nnf-neg (proof-bind a!4) (~ (not a!1) a!5))
% 0.19/0.37 a!13
% 0.19/0.37 a!15
% 0.19/0.37 a!16))))
% 0.19/0.37 Proof display could not be completed: unexpected number of arguments
% 0.19/0.38 % E exiting
%------------------------------------------------------------------------------