%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : SYN373+1 : TPTP v9.0.0. Released v2.0.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n005.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.03/0.12 % Problem : SYN373+1 : TPTP v9.0.0. Released v2.0.0.
% 0.03/0.12 % Command : run_E %s %d THM
% 0.12/0.33 % Computer : n005.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Fri Jun 20 12:33:05 EDT 2025
% 0.12/0.33 % CPUTime :
% 0.19/0.37 % SZS status Theorem
% 0.19/0.37 % SZS output start Proof
% 0.19/0.37 tff(big_q_type, type, (
% 0.19/0.37 big_q: $i > $o)).
% 0.19/0.37 tff(big_p_type, type, (
% 0.19/0.37 big_p: $i > $o)).
% 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_X_0_type, type, (
% 0.19/0.37 tptp_fun_X_0: $i)).
% 0.19/0.37 tff(tptp_fun_X_1_type, type, (
% 0.19/0.37 tptp_fun_X_1: $i)).
% 0.19/0.37 tff(1,assumption,(![X: $i] : (~(big_q(X) | (~big_p(X))))), introduced(assumption)).
% 0.19/0.37 tff(2,assumption,(big_q(X!0) | (~big_p(X!0))), introduced(assumption)).
% 0.19/0.37 tff(3,plain,
% 0.19/0.37 ((~![X: $i] : (~(big_q(X) | (~big_p(X))))) | (~(big_q(X!0) | (~big_p(X!0))))),
% 0.19/0.37 inference(quant_inst,[status(thm)],[])).
% 0.19/0.37 tff(4,plain,
% 0.19/0.37 ($false),
% 0.19/0.37 inference(unit_resolution,[status(thm)],[3, 1, 2])).
% 0.19/0.37 tff(5,plain,((~(big_q(X!0) | (~big_p(X!0)))) | (~![X: $i] : (~(big_q(X) | (~big_p(X)))))), inference(lemma,lemma(discharge,[]))).
% 0.19/0.37 tff(6,plain,
% 0.19/0.37 (~(big_q(X!0) | (~big_p(X!0)))),
% 0.19/0.37 inference(unit_resolution,[status(thm)],[5, 1])).
% 0.19/0.37 tff(7,plain,
% 0.19/0.37 ((big_q(X!0) | (~big_p(X!0))) | (~big_q(X!0))),
% 0.19/0.37 inference(tautology,[status(thm)],[])).
% 0.19/0.37 tff(8,plain,
% 0.19/0.37 (~big_q(X!0)),
% 0.19/0.37 inference(unit_resolution,[status(thm)],[7, 6])).
% 0.19/0.37 tff(9,assumption,(big_q(X!1) | (~big_p(X!1))), introduced(assumption)).
% 0.19/0.37 tff(10,plain,
% 0.19/0.37 ((~![X: $i] : (~(big_q(X) | (~big_p(X))))) | (~(big_q(X!1) | (~big_p(X!1))))),
% 0.19/0.37 inference(quant_inst,[status(thm)],[])).
% 0.19/0.37 tff(11,plain,
% 0.19/0.37 ($false),
% 0.19/0.37 inference(unit_resolution,[status(thm)],[10, 1, 9])).
% 0.19/0.37 tff(12,plain,((~(big_q(X!1) | (~big_p(X!1)))) | (~![X: $i] : (~(big_q(X) | (~big_p(X)))))), inference(lemma,lemma(discharge,[]))).
% 0.19/0.37 tff(13,plain,
% 0.19/0.37 (~(big_q(X!1) | (~big_p(X!1)))),
% 0.19/0.37 inference(unit_resolution,[status(thm)],[12, 1])).
% 0.19/0.37 tff(14,plain,
% 0.19/0.37 ((big_q(X!1) | (~big_p(X!1))) | big_p(X!1)),
% 0.19/0.37 inference(tautology,[status(thm)],[])).
% 0.19/0.37 tff(15,plain,
% 0.19/0.37 (big_p(X!1)),
% 0.19/0.37 inference(unit_resolution,[status(thm)],[14, 13])).
% 0.19/0.37 tff(16,plain,
% 0.19/0.37 ((big_q(X!0) | (~big_p(X!0))) | big_p(X!0)),
% 0.19/0.37 inference(tautology,[status(thm)],[])).
% 0.19/0.37 tff(17,plain,
% 0.19/0.37 (big_p(X!0)),
% 0.19/0.37 inference(unit_resolution,[status(thm)],[16, 6])).
% 0.19/0.37 tff(18,plain,
% 0.19/0.37 ((((big_q(X!0) | (~big_p(X!0))) | ((~big_p(X!1)) | big_q(X!2))) & (![X: $i] : (~(big_q(X) | (~big_p(X)))) | (![X: $i] : big_p(X) & ![X: $i] : (~big_q(X))))) <=> (((~big_p(X!0)) | big_q(X!0) | (~big_p(X!1)) | big_q(X!2)) & (![X: $i] : (~(big_q(X) | (~big_p(X)))) | (![X: $i] : big_p(X) & ![X: $i] : (~big_q(X)))))),
% 0.19/0.37 inference(rewrite,[status(thm)],[])).
% 0.19/0.37 tff(19,plain,
% 0.19/0.37 ((~(?[X: $i] : (big_q(X) | (~big_p(X))) <=> ((~![X: $i] : big_p(X)) | ?[X: $i] : big_q(X)))) <=> (~(?[X: $i] : (big_q(X) | (~big_p(X))) <=> ((~![X: $i] : big_p(X)) | ?[X: $i] : big_q(X))))),
% 0.19/0.37 inference(rewrite,[status(thm)],[])).
% 0.19/0.37 tff(20,plain,
% 0.19/0.37 ((?[X: $i] : (big_q(X) | (~big_p(X))) <=> ((~![X: $i] : big_p(X)) | ?[X: $i] : big_q(X))) <=> (?[X: $i] : (big_q(X) | (~big_p(X))) <=> ((~![X: $i] : big_p(X)) | ?[X: $i] : big_q(X)))),
% 0.19/0.37 inference(rewrite,[status(thm)],[])).
% 0.19/0.37 tff(21,plain,
% 0.19/0.37 ((~(?[X: $i] : (big_q(X) | (~big_p(X))) <=> ((~![X: $i] : big_p(X)) | ?[X: $i] : big_q(X)))) <=> (~(?[X: $i] : (big_q(X) | (~big_p(X))) <=> ((~![X: $i] : big_p(X)) | ?[X: $i] : big_q(X))))),
% 0.19/0.37 inference(monotonicity,[status(thm)],[20])).
% 0.19/0.37 tff(22,plain,
% 0.19/0.37 ((~(?[X: $i] : (big_q(X) | (~big_p(X))) <=> ((~![X: $i] : big_p(X)) | ?[X: $i] : big_q(X)))) <=> (~(?[X: $i] : (big_q(X) | (~big_p(X))) <=> ((~![X: $i] : big_p(X)) | ?[X: $i] : big_q(X))))),
% 0.19/0.37 inference(transitivity,[status(thm)],[21, 19])).
% 0.19/0.37 tff(23,plain,
% 0.19/0.37 ((?[X: $i] : (big_p(X) => big_q(X)) <=> (![X: $i] : big_p(X) => ?[X: $i] : big_q(X))) <=> (?[X: $i] : (big_q(X) | (~big_p(X))) <=> ((~![X: $i] : big_p(X)) | ?[X: $i] : big_q(X)))),
% 0.19/0.37 inference(rewrite,[status(thm)],[])).
% 0.19/0.37 tff(24,plain,
% 0.19/0.37 ((~(?[X: $i] : (big_p(X) => big_q(X)) <=> (![X: $i] : big_p(X) => ?[X: $i] : big_q(X)))) <=> (~(?[X: $i] : (big_q(X) | (~big_p(X))) <=> ((~![X: $i] : big_p(X)) | ?[X: $i] : big_q(X))))),
% 0.19/0.37 inference(monotonicity,[status(thm)],[23])).
% 0.19/0.37 tff(25,plain,
% 0.19/0.37 ((~(?[X: $i] : (big_p(X) => big_q(X)) <=> (![X: $i] : big_p(X) => ?[X: $i] : big_q(X)))) <=> (~(?[X: $i] : (big_q(X) | (~big_p(X))) <=> ((~![X: $i] : big_p(X)) | ?[X: $i] : big_q(X))))),
% 0.19/0.37 inference(transitivity,[status(thm)],[24, 19])).
% 0.19/0.37 tff(26,axiom,(~(?[X: $i] : (big_p(X) => big_q(X)) <=> (![X: $i] : big_p(X) => ?[X: $i] : big_q(X)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','x2124')).
% 0.19/0.37 tff(27,plain,
% 0.19/0.37 (~(?[X: $i] : (big_q(X) | (~big_p(X))) <=> ((~![X: $i] : big_p(X)) | ?[X: $i] : big_q(X)))),
% 0.19/0.37 inference(modus_ponens,[status(thm)],[26, 25])).
% 0.19/0.37 tff(28,plain,
% 0.19/0.37 (~(?[X: $i] : (big_q(X) | (~big_p(X))) <=> ((~![X: $i] : big_p(X)) | ?[X: $i] : big_q(X)))),
% 0.19/0.37 inference(modus_ponens,[status(thm)],[27, 22])).
% 0.19/0.37 tff(29,plain,
% 0.19/0.37 (~(?[X: $i] : (big_q(X) | (~big_p(X))) <=> ((~![X: $i] : big_p(X)) | ?[X: $i] : big_q(X)))),
% 0.19/0.37 inference(modus_ponens,[status(thm)],[28, 19])).
% 0.19/0.37 tff(30,plain,
% 0.19/0.37 (~(?[X: $i] : (big_q(X) | (~big_p(X))) <=> ((~![X: $i] : big_p(X)) | ?[X: $i] : big_q(X)))),
% 0.19/0.37 inference(modus_ponens,[status(thm)],[29, 22])).
% 0.19/0.37 unexpected number of arguments: (let ((a!1 (exists ((X $i)) (or (big_q X) (not (big_p X)))))
% 0.19/0.37 (a!3 (proof-bind (lambda ((X $i))
% 0.19/0.37 (let ((a!1 (not (or (big_q X) (not (big_p X))))))
% 0.19/0.37 (refl (~ a!1 a!1))))))
% 0.19/0.37 (a!4 (forall ((X $i)) (not (or (big_q X) (not (big_p X))))))
% 0.19/0.37 (a!5 (forall ((X $i)) (big_p X)))
% 0.19/0.37 (a!7 (exists ((X $i)) (big_q X)))
% 0.19/0.37 (a!10 (lambda ((X $i)) (refl (~ (big_p X) (big_p X)))))
% 0.19/0.37 (a!12 (lambda ((X $i)) (refl (~ (not (big_q X)) (not (big_q X))))))
% 0.19/0.37 (a!13 (forall ((X $i)) (not (big_q X))))
% 0.19/0.37 (a!17 (or (or (big_q X!0) (not (big_p X!0)))
% 0.19/0.37 (or (not (big_p X!1)) (big_q X!2)))))
% 0.19/0.37 (let ((a!2 (~ a!1 (or (big_q X!0) (not (big_p X!0)))))
% 0.19/0.37 (a!6 (sk (~ (not a!5) (not (big_p X!1)))))
% 0.19/0.37 (a!8 (~ (or (not a!5) a!7) (or (not (big_p X!1)) (big_q X!2))))
% 0.19/0.37 (a!11 (nnf-neg (nnf-pos (proof-bind a!10) (~ a!5 a!5))
% 0.19/0.37 (~ (not (not a!5)) a!5)))
% 0.19/0.37 (a!14 (~ (not (or (not a!5) a!7)) (and a!5 a!13)))
% 0.19/0.37 (a!16 (not (= a!1 (or (not a!5) a!7)))))
% 0.19/0.37 (let ((a!9 (monotonicity a!6 (sk (~ a!7 (big_q X!2))) a!8))
% 0.19/0.37 (a!15 (nnf-neg a!11 (nnf-neg (proof-bind a!12) (~ (not a!7) a!13)) a!14))
% 0.19/0.37 (a!18 (~ a!16 (and a!17 (or a!4 (and a!5 a!13))))))
% 0.19/0.37 (nnf-neg (sk a!2) (nnf-neg a!3 (~ (not a!1) a!4)) a!9 a!15 a!18))))
% 0.19/0.37 Proof display could not be completed: unexpected number of arguments
% 0.19/0.37 % E exiting
%------------------------------------------------------------------------------