%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : RNG125+4 : TPTP v9.0.0. Released v4.0.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n009.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:24:16 AM UTC 2025
% Result : Theorem 0.20s 0.41s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : RNG125+4 : TPTP v9.0.0. Released v4.0.0.
% 0.07/0.13 % Command : run_E %s %d THM
% 0.12/0.34 % Computer : n009.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Fri Jun 20 03:26:18 EDT 2025
% 0.12/0.34 % CPUTime :
% 0.20/0.41 % SZS status Theorem
% 0.20/0.41 % SZS output start Proof
% 0.20/0.41 tff(xa_type, type, (
% 0.20/0.41 xa: $i)).
% 0.20/0.41 tff(sdtasdt0_type, type, (
% 0.20/0.41 sdtasdt0: ( $i * $i ) > $i)).
% 0.20/0.41 tff(xu_type, type, (
% 0.20/0.41 xu: $i)).
% 0.20/0.41 tff(aElement0_type, type, (
% 0.20/0.41 aElement0: $i > $o)).
% 0.20/0.41 tff(aDivisorOf0_type, type, (
% 0.20/0.41 aDivisorOf0: ( $i * $i ) > $o)).
% 0.20/0.41 tff(doDivides0_type, type, (
% 0.20/0.41 doDivides0: ( $i * $i ) > $o)).
% 0.20/0.41 tff(xb_type, type, (
% 0.20/0.41 xb: $i)).
% 0.20/0.41 tff(1,plain,
% 0.20/0.41 (doDivides0(xu, xa) <=> doDivides0(xu, xa)),
% 0.20/0.41 inference(rewrite,[status(thm)],[])).
% 0.20/0.41 tff(2,plain,
% 0.20/0.41 ((~(~(?[W0: $i] : (aElement0(W0) & (sdtasdt0(xu, W0) = xa)) & doDivides0(xu, xa)))) <=> (?[W0: $i] : (aElement0(W0) & (sdtasdt0(xu, W0) = xa)) & doDivides0(xu, xa))),
% 0.20/0.41 inference(rewrite,[status(thm)],[])).
% 0.20/0.41 tff(3,axiom,(~(~(?[W0: $i] : (aElement0(W0) & (sdtasdt0(xu, W0) = xa)) & doDivides0(xu, xa)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','m__2479')).
% 0.20/0.41 tff(4,plain,
% 0.20/0.41 (?[W0: $i] : (aElement0(W0) & (sdtasdt0(xu, W0) = xa)) & doDivides0(xu, xa)),
% 0.20/0.41 inference(modus_ponens,[status(thm)],[3, 2])).
% 0.20/0.41 tff(5,plain,
% 0.20/0.41 (doDivides0(xu, xa)),
% 0.20/0.41 inference(and_elim,[status(thm)],[4])).
% 0.20/0.41 tff(6,plain,
% 0.20/0.41 (doDivides0(xu, xa)),
% 0.20/0.41 inference(modus_ponens,[status(thm)],[5, 1])).
% 0.20/0.41 tff(7,plain,
% 0.20/0.41 ((doDivides0(xu, xa) | aDivisorOf0(xu, xa) | (~![W0: $i] : ((~aElement0(W0)) | (~(sdtasdt0(xu, W0) = xa))))) | (~doDivides0(xu, xa))),
% 0.20/0.41 inference(tautology,[status(thm)],[])).
% 0.20/0.41 tff(8,plain,
% 0.20/0.41 (doDivides0(xu, xa) | aDivisorOf0(xu, xa) | (~![W0: $i] : ((~aElement0(W0)) | (~(sdtasdt0(xu, W0) = xa))))),
% 0.20/0.41 inference(unit_resolution,[status(thm)],[7, 6])).
% 0.20/0.41 tff(9,plain,
% 0.20/0.41 (doDivides0(xu, xb) <=> doDivides0(xu, xb)),
% 0.20/0.41 inference(rewrite,[status(thm)],[])).
% 0.20/0.41 tff(10,plain,
% 0.20/0.41 ((~(~(?[W0: $i] : (aElement0(W0) & (sdtasdt0(xu, W0) = xb)) & doDivides0(xu, xb)))) <=> (?[W0: $i] : (aElement0(W0) & (sdtasdt0(xu, W0) = xb)) & doDivides0(xu, xb))),
% 0.20/0.41 inference(rewrite,[status(thm)],[])).
% 0.20/0.41 tff(11,axiom,(~(~(?[W0: $i] : (aElement0(W0) & (sdtasdt0(xu, W0) = xb)) & doDivides0(xu, xb)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','m__2612')).
% 0.20/0.41 tff(12,plain,
% 0.20/0.41 (?[W0: $i] : (aElement0(W0) & (sdtasdt0(xu, W0) = xb)) & doDivides0(xu, xb)),
% 0.20/0.41 inference(modus_ponens,[status(thm)],[11, 10])).
% 0.20/0.41 tff(13,plain,
% 0.20/0.41 (doDivides0(xu, xb)),
% 0.20/0.41 inference(and_elim,[status(thm)],[12])).
% 0.20/0.41 tff(14,plain,
% 0.20/0.41 (doDivides0(xu, xb)),
% 0.20/0.41 inference(modus_ponens,[status(thm)],[13, 9])).
% 0.20/0.41 tff(15,plain,
% 0.20/0.41 ((doDivides0(xu, xb) | aDivisorOf0(xu, xb) | (~![W0: $i] : ((~aElement0(W0)) | (~(sdtasdt0(xu, W0) = xb))))) | (~doDivides0(xu, xb))),
% 0.20/0.41 inference(tautology,[status(thm)],[])).
% 0.20/0.41 tff(16,plain,
% 0.20/0.41 (doDivides0(xu, xb) | aDivisorOf0(xu, xb) | (~![W0: $i] : ((~aElement0(W0)) | (~(sdtasdt0(xu, W0) = xb))))),
% 0.20/0.41 inference(unit_resolution,[status(thm)],[15, 14])).
% 0.20/0.41 tff(17,plain,
% 0.20/0.41 (((~(doDivides0(xu, xa) | aDivisorOf0(xu, xa) | (~![W0: $i] : ((~aElement0(W0)) | (~(sdtasdt0(xu, W0) = xa)))))) | (~(doDivides0(xu, xb) | aDivisorOf0(xu, xb) | (~![W0: $i] : ((~aElement0(W0)) | (~(sdtasdt0(xu, W0) = xb))))))) <=> ((~(doDivides0(xu, xa) | aDivisorOf0(xu, xa) | (~![W0: $i] : ((~aElement0(W0)) | (~(sdtasdt0(xu, W0) = xa)))))) | (~(doDivides0(xu, xb) | aDivisorOf0(xu, xb) | (~![W0: $i] : ((~aElement0(W0)) | (~(sdtasdt0(xu, W0) = xb)))))))),
% 0.20/0.41 inference(rewrite,[status(thm)],[])).
% 0.20/0.41 tff(18,plain,
% 0.20/0.41 ((((~doDivides0(xu, xa)) & ![W0: $i] : (~(aElement0(W0) & (sdtasdt0(xu, W0) = xa))) & (~aDivisorOf0(xu, xa))) | ((~doDivides0(xu, xb)) & (~aDivisorOf0(xu, xb)) & ![W0: $i] : (~(aElement0(W0) & (sdtasdt0(xu, W0) = xb))))) <=> ((~(doDivides0(xu, xa) | aDivisorOf0(xu, xa) | (~![W0: $i] : ((~aElement0(W0)) | (~(sdtasdt0(xu, W0) = xa)))))) | (~(doDivides0(xu, xb) | aDivisorOf0(xu, xb) | (~![W0: $i] : ((~aElement0(W0)) | (~(sdtasdt0(xu, W0) = xb)))))))),
% 0.20/0.41 inference(rewrite,[status(thm)],[])).
% 0.20/0.41 tff(19,plain,
% 0.20/0.41 (((~doDivides0(xu, xb)) & (~aDivisorOf0(xu, xb)) & ![W0: $i] : (~(aElement0(W0) & (sdtasdt0(xu, W0) = xb)))) <=> ((~doDivides0(xu, xb)) & (~aDivisorOf0(xu, xb)) & ![W0: $i] : (~(aElement0(W0) & (sdtasdt0(xu, W0) = xb))))),
% 0.20/0.41 inference(rewrite,[status(thm)],[])).
% 0.20/0.41 tff(20,plain,
% 0.20/0.41 (((~doDivides0(xu, xa)) & ![W0: $i] : (~(aElement0(W0) & (sdtasdt0(xu, W0) = xa))) & (~aDivisorOf0(xu, xa))) <=> ((~doDivides0(xu, xa)) & ![W0: $i] : (~(aElement0(W0) & (sdtasdt0(xu, W0) = xa))) & (~aDivisorOf0(xu, xa)))),
% 0.20/0.41 inference(rewrite,[status(thm)],[])).
% 0.20/0.41 tff(21,plain,
% 0.20/0.41 ((((~doDivides0(xu, xa)) & ![W0: $i] : (~(aElement0(W0) & (sdtasdt0(xu, W0) = xa))) & (~aDivisorOf0(xu, xa))) | ((~doDivides0(xu, xb)) & (~aDivisorOf0(xu, xb)) & ![W0: $i] : (~(aElement0(W0) & (sdtasdt0(xu, W0) = xb))))) <=> (((~doDivides0(xu, xa)) & ![W0: $i] : (~(aElement0(W0) & (sdtasdt0(xu, W0) = xa))) & (~aDivisorOf0(xu, xa))) | ((~doDivides0(xu, xb)) & (~aDivisorOf0(xu, xb)) & ![W0: $i] : (~(aElement0(W0) & (sdtasdt0(xu, W0) = xb)))))),
% 0.20/0.41 inference(monotonicity,[status(thm)],[20, 19])).
% 0.20/0.41 tff(22,plain,
% 0.20/0.41 (((doDivides0(xu, xa) | ?[W0: $i] : (aElement0(W0) & (sdtasdt0(xu, W0) = xa)) | aDivisorOf0(xu, xa)) & (doDivides0(xu, xb) | aDivisorOf0(xu, xb) | ?[W0: $i] : (aElement0(W0) & (sdtasdt0(xu, W0) = xb)))) <=> ((doDivides0(xu, xa) | ?[W0: $i] : (aElement0(W0) & (sdtasdt0(xu, W0) = xa)) | aDivisorOf0(xu, xa)) & (doDivides0(xu, xb) | aDivisorOf0(xu, xb) | ?[W0: $i] : (aElement0(W0) & (sdtasdt0(xu, W0) = xb))))),
% 0.20/0.41 inference(rewrite,[status(thm)],[])).
% 0.20/0.41 tff(23,plain,
% 0.20/0.41 ((~((doDivides0(xu, xa) | ?[W0: $i] : (aElement0(W0) & (sdtasdt0(xu, W0) = xa)) | aDivisorOf0(xu, xa)) & (doDivides0(xu, xb) | aDivisorOf0(xu, xb) | ?[W0: $i] : (aElement0(W0) & (sdtasdt0(xu, W0) = xb))))) <=> (~((doDivides0(xu, xa) | ?[W0: $i] : (aElement0(W0) & (sdtasdt0(xu, W0) = xa)) | aDivisorOf0(xu, xa)) & (doDivides0(xu, xb) | aDivisorOf0(xu, xb) | ?[W0: $i] : (aElement0(W0) & (sdtasdt0(xu, W0) = xb)))))),
% 0.20/0.41 inference(monotonicity,[status(thm)],[22])).
% 0.20/0.41 tff(24,plain,
% 0.20/0.41 ((~((doDivides0(xu, xa) | ?[W0: $i] : (aElement0(W0) & (sdtasdt0(xu, W0) = xa)) | aDivisorOf0(xu, xa)) & (doDivides0(xu, xb) | aDivisorOf0(xu, xb) | ?[W0: $i] : (aElement0(W0) & (sdtasdt0(xu, W0) = xb))))) <=> (~((doDivides0(xu, xa) | ?[W0: $i] : (aElement0(W0) & (sdtasdt0(xu, W0) = xa)) | aDivisorOf0(xu, xa)) & (doDivides0(xu, xb) | aDivisorOf0(xu, xb) | ?[W0: $i] : (aElement0(W0) & (sdtasdt0(xu, W0) = xb)))))),
% 0.20/0.41 inference(rewrite,[status(thm)],[])).
% 0.20/0.41 tff(25,plain,
% 0.20/0.41 ((~(((?[W0: $i] : (aElement0(W0) & (sdtasdt0(xu, W0) = xa)) | doDivides0(xu, xa)) | aDivisorOf0(xu, xa)) & ((?[W0: $i] : (aElement0(W0) & (sdtasdt0(xu, W0) = xb)) | doDivides0(xu, xb)) | aDivisorOf0(xu, xb)))) <=> (~((doDivides0(xu, xa) | ?[W0: $i] : (aElement0(W0) & (sdtasdt0(xu, W0) = xa)) | aDivisorOf0(xu, xa)) & (doDivides0(xu, xb) | aDivisorOf0(xu, xb) | ?[W0: $i] : (aElement0(W0) & (sdtasdt0(xu, W0) = xb)))))),
% 0.20/0.41 inference(rewrite,[status(thm)],[])).
% 0.20/0.41 tff(26,axiom,(~(((?[W0: $i] : (aElement0(W0) & (sdtasdt0(xu, W0) = xa)) | doDivides0(xu, xa)) | aDivisorOf0(xu, xa)) & ((?[W0: $i] : (aElement0(W0) & (sdtasdt0(xu, W0) = xb)) | doDivides0(xu, xb)) | aDivisorOf0(xu, xb)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','m__2383')).
% 0.20/0.41 tff(27,plain,
% 0.20/0.41 (~((doDivides0(xu, xa) | ?[W0: $i] : (aElement0(W0) & (sdtasdt0(xu, W0) = xa)) | aDivisorOf0(xu, xa)) & (doDivides0(xu, xb) | aDivisorOf0(xu, xb) | ?[W0: $i] : (aElement0(W0) & (sdtasdt0(xu, W0) = xb))))),
% 0.20/0.41 inference(modus_ponens,[status(thm)],[26, 25])).
% 0.20/0.41 tff(28,plain,
% 0.20/0.41 (~((doDivides0(xu, xa) | ?[W0: $i] : (aElement0(W0) & (sdtasdt0(xu, W0) = xa)) | aDivisorOf0(xu, xa)) & (doDivides0(xu, xb) | aDivisorOf0(xu, xb) | ?[W0: $i] : (aElement0(W0) & (sdtasdt0(xu, W0) = xb))))),
% 0.20/0.41 inference(modus_ponens,[status(thm)],[27, 23])).
% 0.20/0.41 tff(29,plain,
% 0.20/0.41 (~((doDivides0(xu, xa) | ?[W0: $i] : (aElement0(W0) & (sdtasdt0(xu, W0) = xa)) | aDivisorOf0(xu, xa)) & (doDivides0(xu, xb) | aDivisorOf0(xu, xb) | ?[W0: $i] : (aElement0(W0) & (sdtasdt0(xu, W0) = xb))))),
% 0.20/0.41 inference(modus_ponens,[status(thm)],[28, 24])).
% 0.20/0.41 tff(30,plain,
% 0.20/0.41 (~((doDivides0(xu, xa) | ?[W0: $i] : (aElement0(W0) & (sdtasdt0(xu, W0) = xa)) | aDivisorOf0(xu, xa)) & (doDivides0(xu, xb) | aDivisorOf0(xu, xb) | ?[W0: $i] : (aElement0(W0) & (sdtasdt0(xu, W0) = xb))))),
% 0.20/0.41 inference(modus_ponens,[status(thm)],[29, 23])).
% 0.20/0.42 unexpected number of arguments: (let ((a!1 (refl (~ (not (doDivides0 xu xa)) (not (doDivides0 xu xa)))))
% 0.20/0.42 (a!2 (proof-bind (lambda ((W0 $i))
% 0.20/0.42 (let ((a!1 (not (and (aElement0 W0)
% 0.20/0.42 (= (sdtasdt0 xu W0) xa)))))
% 0.20/0.42 (refl (~ a!1 a!1))))))
% 0.20/0.42 (a!3 (exists ((W0 $i)) (and (aElement0 W0) (= (sdtasdt0 xu W0) xa))))
% 0.20/0.42 (a!4 (forall ((W0 $i)) (not (and (aElement0 W0) (= (sdtasdt0 xu W0) xa)))))
% 0.20/0.42 (a!5 (refl (~ (not (aDivisorOf0 xu xa)) (not (aDivisorOf0 xu xa)))))
% 0.20/0.42 (a!9 (refl (~ (not (doDivides0 xu xb)) (not (doDivides0 xu xb)))))
% 0.20/0.42 (a!10 (refl (~ (not (aDivisorOf0 xu xb)) (not (aDivisorOf0 xu xb)))))
% 0.20/0.42 (a!11 (proof-bind (lambda ((W0 $i))
% 0.20/0.42 (let ((a!1 (not (and (aElement0 W0)
% 0.20/0.42 (= (sdtasdt0 xu W0) xb)))))
% 0.20/0.42 (refl (~ a!1 a!1))))))
% 0.20/0.42 (a!12 (exists ((W0 $i)) (and (aElement0 W0) (= (sdtasdt0 xu W0) xb))))
% 0.20/0.42 (a!13 (forall ((W0 $i))
% 0.20/0.42 (not (and (aElement0 W0) (= (sdtasdt0 xu W0) xb))))))
% 0.20/0.42 (let ((a!6 (and (not (doDivides0 xu xa)) a!4 (not (aDivisorOf0 xu xa))))
% 0.20/0.42 (a!14 (and (not (doDivides0 xu xb)) (not (aDivisorOf0 xu xb)) a!13))
% 0.20/0.42 (a!17 (not (and (or (doDivides0 xu xa) a!3 (aDivisorOf0 xu xa))
% 0.20/0.42 (or (doDivides0 xu xb) (aDivisorOf0 xu xb) a!12)))))
% 0.20/0.42 (let ((a!7 (~ (not (or (doDivides0 xu xa) a!3 (aDivisorOf0 xu xa))) a!6))
% 0.20/0.42 (a!15 (~ (not (or (doDivides0 xu xb) (aDivisorOf0 xu xb) a!12)) a!14)))
% 0.20/0.42 (let ((a!8 (nnf-neg a!1 (nnf-neg a!2 (~ (not a!3) a!4)) a!5 a!7))
% 0.20/0.42 (a!16 (nnf-neg a!9 a!10 (nnf-neg a!11 (~ (not a!12) a!13)) a!15)))
% 0.20/0.42 (nnf-neg a!8 a!16 (~ a!17 (or a!6 a!14)))))))
% 0.20/0.42 Proof display could not be completed: unexpected number of arguments
% 0.20/0.42 % E exiting
%------------------------------------------------------------------------------