%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : SYN924+1 : TPTP v9.0.0. Released v3.1.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n003.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:41:00 AM UTC 2025
% Result : Theorem 0.12s 0.37s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SYN924+1 : TPTP v9.0.0. Released v3.1.0.
% 0.07/0.12 % Command : run_E %s %d THM
% 0.12/0.33 % Computer : n003.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 13:01:09 EDT 2025
% 0.12/0.33 % CPUTime :
% 0.12/0.37 % SZS status Theorem
% 0.12/0.37 % SZS output start Proof
% 0.12/0.37 tff(q_type, type, (
% 0.12/0.37 q: $i > $o)).
% 0.12/0.37 tff(p_type, type, (
% 0.12/0.37 p: $i > $o)).
% 0.12/0.37 tff(tptp_fun_X_2_type, type, (
% 0.12/0.37 tptp_fun_X_2: $i)).
% 0.12/0.37 tff(tptp_fun_X_0_type, type, (
% 0.12/0.37 tptp_fun_X_0: $i)).
% 0.12/0.37 tff(tptp_fun_X_1_type, type, (
% 0.12/0.37 tptp_fun_X_1: $i)).
% 0.12/0.37 tff(1,assumption,(![X: $i] : (~(p(X) | q(X)))), introduced(assumption)).
% 0.12/0.37 tff(2,assumption,(p(X!0) | q(X!0)), introduced(assumption)).
% 0.12/0.37 tff(3,plain,
% 0.12/0.37 ((~![X: $i] : (~(p(X) | q(X)))) | (~(p(X!0) | q(X!0)))),
% 0.12/0.37 inference(quant_inst,[status(thm)],[])).
% 0.12/0.37 tff(4,plain,
% 0.12/0.37 ($false),
% 0.12/0.37 inference(unit_resolution,[status(thm)],[3, 1, 2])).
% 0.12/0.37 tff(5,plain,((~(p(X!0) | q(X!0))) | (~![X: $i] : (~(p(X) | q(X))))), inference(lemma,lemma(discharge,[]))).
% 0.12/0.37 tff(6,plain,
% 0.12/0.37 (~(p(X!0) | q(X!0))),
% 0.12/0.37 inference(unit_resolution,[status(thm)],[5, 1])).
% 0.12/0.37 tff(7,plain,
% 0.12/0.37 ((p(X!0) | q(X!0)) | (~q(X!0))),
% 0.12/0.37 inference(tautology,[status(thm)],[])).
% 0.12/0.37 tff(8,plain,
% 0.12/0.37 (~q(X!0)),
% 0.12/0.37 inference(unit_resolution,[status(thm)],[7, 6])).
% 0.12/0.37 tff(9,plain,
% 0.12/0.37 ((p(X!0) | q(X!0)) | (~p(X!0))),
% 0.12/0.37 inference(tautology,[status(thm)],[])).
% 0.12/0.37 tff(10,plain,
% 0.12/0.37 (~p(X!0)),
% 0.12/0.37 inference(unit_resolution,[status(thm)],[9, 6])).
% 0.12/0.37 tff(11,assumption,(p(X!1) | q(X!1)), introduced(assumption)).
% 0.12/0.37 tff(12,plain,
% 0.12/0.37 ((~![X: $i] : (~(p(X) | q(X)))) | (~(p(X!1) | q(X!1)))),
% 0.12/0.37 inference(quant_inst,[status(thm)],[])).
% 0.12/0.37 tff(13,plain,
% 0.12/0.37 ($false),
% 0.12/0.37 inference(unit_resolution,[status(thm)],[12, 1, 11])).
% 0.12/0.37 tff(14,plain,((~(p(X!1) | q(X!1))) | (~![X: $i] : (~(p(X) | q(X))))), inference(lemma,lemma(discharge,[]))).
% 0.12/0.37 tff(15,plain,
% 0.12/0.37 (~(p(X!1) | q(X!1))),
% 0.12/0.37 inference(unit_resolution,[status(thm)],[14, 1])).
% 0.12/0.37 tff(16,plain,
% 0.12/0.37 ((p(X!1) | q(X!1)) | (~p(X!1))),
% 0.12/0.37 inference(tautology,[status(thm)],[])).
% 0.12/0.37 tff(17,plain,
% 0.12/0.37 (~p(X!1)),
% 0.12/0.37 inference(unit_resolution,[status(thm)],[16, 15])).
% 0.12/0.37 tff(18,plain,
% 0.12/0.37 ((((p(X!0) | q(X!0)) | (p(X!1) | q(X!2))) & (![X: $i] : (~(p(X) | q(X))) | (![X: $i] : (~p(X)) & ![X: $i] : (~q(X))))) <=> ((p(X!0) | q(X!0) | p(X!1) | q(X!2)) & (![X: $i] : (~(p(X) | q(X))) | (![X: $i] : (~p(X)) & ![X: $i] : (~q(X)))))),
% 0.12/0.37 inference(rewrite,[status(thm)],[])).
% 0.12/0.37 tff(19,plain,
% 0.12/0.37 ((~(?[X: $i] : (p(X) | q(X)) <=> (?[X: $i] : p(X) | ?[X: $i] : q(X)))) <=> (~(?[X: $i] : (p(X) | q(X)) <=> (?[X: $i] : p(X) | ?[X: $i] : q(X))))),
% 0.12/0.37 inference(rewrite,[status(thm)],[])).
% 0.12/0.37 tff(20,plain,
% 0.12/0.37 ((?[X: $i] : (p(X) | q(X)) <=> (?[X: $i] : p(X) | ?[X: $i] : q(X))) <=> (?[X: $i] : (p(X) | q(X)) <=> (?[X: $i] : p(X) | ?[X: $i] : q(X)))),
% 0.12/0.37 inference(rewrite,[status(thm)],[])).
% 0.12/0.37 tff(21,plain,
% 0.12/0.37 ((~(?[X: $i] : (p(X) | q(X)) <=> (?[X: $i] : p(X) | ?[X: $i] : q(X)))) <=> (~(?[X: $i] : (p(X) | q(X)) <=> (?[X: $i] : p(X) | ?[X: $i] : q(X))))),
% 0.12/0.37 inference(monotonicity,[status(thm)],[20])).
% 0.12/0.37 tff(22,plain,
% 0.12/0.37 ((~(?[X: $i] : (p(X) | q(X)) <=> (?[X: $i] : p(X) | ?[X: $i] : q(X)))) <=> (~(?[X: $i] : (p(X) | q(X)) <=> (?[X: $i] : p(X) | ?[X: $i] : q(X))))),
% 0.12/0.37 inference(transitivity,[status(thm)],[21, 19])).
% 0.12/0.37 tff(23,axiom,(~(?[X: $i] : (p(X) | q(X)) <=> (?[X: $i] : p(X) | ?[X: $i] : q(X)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','prove_this')).
% 0.12/0.37 tff(24,plain,
% 0.12/0.37 (~(?[X: $i] : (p(X) | q(X)) <=> (?[X: $i] : p(X) | ?[X: $i] : q(X)))),
% 0.12/0.37 inference(modus_ponens,[status(thm)],[23, 22])).
% 0.12/0.37 tff(25,plain,
% 0.12/0.37 (~(?[X: $i] : (p(X) | q(X)) <=> (?[X: $i] : p(X) | ?[X: $i] : q(X)))),
% 0.12/0.37 inference(modus_ponens,[status(thm)],[24, 22])).
% 0.12/0.37 tff(26,plain,
% 0.12/0.37 (~(?[X: $i] : (p(X) | q(X)) <=> (?[X: $i] : p(X) | ?[X: $i] : q(X)))),
% 0.12/0.37 inference(modus_ponens,[status(thm)],[25, 19])).
% 0.12/0.37 tff(27,plain,
% 0.12/0.37 (~(?[X: $i] : (p(X) | q(X)) <=> (?[X: $i] : p(X) | ?[X: $i] : q(X)))),
% 0.12/0.37 inference(modus_ponens,[status(thm)],[26, 22])).
% 0.12/0.37 unexpected number of arguments: (let ((a!1 (exists ((X $i)) (or (p X) (q X))))
% 0.12/0.37 (a!3 (forall ((X $i)) (not (or (p X) (q X)))))
% 0.12/0.37 (a!5 (exists ((X $i)) (p X)))
% 0.12/0.37 (a!6 (exists ((X $i)) (q X)))
% 0.12/0.37 (a!8 (lambda ((X $i)) (refl (~ (not (p X)) (not (p X))))))
% 0.12/0.37 (a!9 (forall ((X $i)) (not (p X))))
% 0.12/0.37 (a!10 (lambda ((X $i)) (refl (~ (not (q X)) (not (q X))))))
% 0.12/0.37 (a!11 (forall ((X $i)) (not (q X)))))
% 0.12/0.37 (let ((a!2 (sk (~ a!1 (or (p X!0) (q X!0)))))
% 0.12/0.37 (a!4 (nnf-neg (proof-bind (lambda ((X $i))
% 0.12/0.37 (let ((a!1 (~ (not (or (p X) (q X)))
% 0.12/0.37 (not (or (p X) (q X))))))
% 0.12/0.37 (refl a!1))))
% 0.12/0.37 (~ (not a!1) a!3)))
% 0.12/0.37 (a!7 (monotonicity (sk (~ a!5 (p X!1)))
% 0.12/0.37 (sk (~ a!6 (q X!2)))
% 0.12/0.37 (~ (or a!5 a!6) (or (p X!1) (q X!2)))))
% 0.12/0.37 (a!12 (nnf-neg (nnf-neg (proof-bind a!8) (~ (not a!5) a!9))
% 0.12/0.37 (nnf-neg (proof-bind a!10) (~ (not a!6) a!11))
% 0.12/0.37 (~ (not (or a!5 a!6)) (and a!9 a!11))))
% 0.12/0.37 (a!13 (and (or (or (p X!0) (q X!0)) (or (p X!1) (q X!2)))
% 0.12/0.37 (or a!3 (and a!9 a!11)))))
% 0.12/0.37 (let ((a!14 (~ (not (= a!1 (or a!5 a!6))) a!13)))
% 0.12/0.37 (nnf-neg a!2 a!4 a!7 a!12 a!14))))
% 0.12/0.37 Proof display could not be completed: unexpected number of arguments
% 0.12/0.37 % E exiting
%------------------------------------------------------------------------------