%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : KLE003+1 : TPTP v9.0.0. Released v4.0.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n002.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:12:49 AM UTC 2025
% Result : Theorem 0.14s 0.38s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : KLE003+1 : TPTP v9.0.0. Released v4.0.0.
% 0.07/0.13 % Command : run_E %s %d THM
% 0.14/0.35 % Computer : n002.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Thu Jun 19 18:51:31 EDT 2025
% 0.14/0.35 % CPUTime :
% 0.14/0.38 % SZS status Theorem
% 0.14/0.38 % SZS output start Proof
% 0.14/0.38 tff(one_type, type, (
% 0.14/0.38 one: $i)).
% 0.14/0.38 tff(addition_type, type, (
% 0.14/0.38 addition: ( $i * $i ) > $i)).
% 0.14/0.38 tff(tptp_fun_X0_0_type, type, (
% 0.14/0.38 tptp_fun_X0_0: $i)).
% 0.14/0.38 tff(1,assumption,(~(addition(X0!0, X0!0) = X0!0)), introduced(assumption)).
% 0.14/0.38 tff(2,plain,
% 0.14/0.38 (^[A: $i] : refl((addition(A, A) = A) <=> (addition(A, A) = A))),
% 0.14/0.38 inference(bind,[status(th)],[])).
% 0.14/0.38 tff(3,plain,
% 0.14/0.38 (![A: $i] : (addition(A, A) = A) <=> ![A: $i] : (addition(A, A) = A)),
% 0.14/0.38 inference(quant_intro,[status(thm)],[2])).
% 0.14/0.38 tff(4,plain,
% 0.14/0.38 (![A: $i] : (addition(A, A) = A) <=> ![A: $i] : (addition(A, A) = A)),
% 0.14/0.38 inference(rewrite,[status(thm)],[])).
% 0.14/0.38 tff(5,axiom,(![A: $i] : (addition(A, A) = A)), file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+0.ax','additive_idempotence')).
% 0.14/0.38 tff(6,plain,
% 0.14/0.38 (![A: $i] : (addition(A, A) = A)),
% 0.14/0.38 inference(modus_ponens,[status(thm)],[5, 4])).
% 0.14/0.38 tff(7,plain,(
% 0.14/0.38 ![A: $i] : (addition(A, A) = A)),
% 0.14/0.38 inference(skolemize,[status(sab)],[6])).
% 0.14/0.38 tff(8,plain,
% 0.14/0.38 (![A: $i] : (addition(A, A) = A)),
% 0.14/0.38 inference(modus_ponens,[status(thm)],[7, 3])).
% 0.14/0.38 tff(9,plain,
% 0.14/0.38 ((~![A: $i] : (addition(A, A) = A)) | (addition(X0!0, X0!0) = X0!0)),
% 0.14/0.38 inference(quant_inst,[status(thm)],[])).
% 0.14/0.38 tff(10,plain,
% 0.14/0.38 ($false),
% 0.14/0.38 inference(unit_resolution,[status(thm)],[9, 8, 1])).
% 0.14/0.38 tff(11,plain,(addition(X0!0, X0!0) = X0!0), inference(lemma,lemma(discharge,[]))).
% 0.14/0.38 tff(12,plain,
% 0.14/0.38 (((![X0: $i] : (addition(X0, X0) = X0) | (addition(one, one) = one)) & ((~(addition(X0!0, X0!0) = X0!0)) | (~(addition(one, one) = one)))) <=> (((addition(one, one) = one) | ![X0: $i] : (addition(X0, X0) = X0)) & ((~(addition(X0!0, X0!0) = X0!0)) | (~(addition(one, one) = one))))),
% 0.14/0.38 inference(rewrite,[status(thm)],[])).
% 0.14/0.38 tff(13,plain,
% 0.14/0.38 ((~(![X0: $i] : (addition(X0, X0) = X0) <=> (addition(one, one) = one))) <=> (~(![X0: $i] : (addition(X0, X0) = X0) <=> (addition(one, one) = one)))),
% 0.14/0.38 inference(rewrite,[status(thm)],[])).
% 0.14/0.38 tff(14,plain,
% 0.14/0.38 ((![X0: $i] : (addition(X0, X0) = X0) <=> (addition(one, one) = one)) <=> (![X0: $i] : (addition(X0, X0) = X0) <=> (addition(one, one) = one))),
% 0.14/0.38 inference(rewrite,[status(thm)],[])).
% 0.14/0.38 tff(15,plain,
% 0.14/0.38 ((~(![X0: $i] : (addition(X0, X0) = X0) <=> (addition(one, one) = one))) <=> (~(![X0: $i] : (addition(X0, X0) = X0) <=> (addition(one, one) = one)))),
% 0.14/0.38 inference(monotonicity,[status(thm)],[14])).
% 0.14/0.38 tff(16,plain,
% 0.14/0.38 ((~(![X0: $i] : (addition(X0, X0) = X0) <=> (addition(one, one) = one))) <=> (~(![X0: $i] : (addition(X0, X0) = X0) <=> (addition(one, one) = one)))),
% 0.14/0.38 inference(transitivity,[status(thm)],[15, 13])).
% 0.14/0.38 tff(17,axiom,(~(![X0: $i] : (addition(X0, X0) = X0) <=> (addition(one, one) = one))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','goals')).
% 0.14/0.38 tff(18,plain,
% 0.14/0.38 (~(![X0: $i] : (addition(X0, X0) = X0) <=> (addition(one, one) = one))),
% 0.14/0.38 inference(modus_ponens,[status(thm)],[17, 16])).
% 0.14/0.38 tff(19,plain,
% 0.14/0.38 (~(![X0: $i] : (addition(X0, X0) = X0) <=> (addition(one, one) = one))),
% 0.14/0.38 inference(modus_ponens,[status(thm)],[18, 16])).
% 0.14/0.38 tff(20,plain,
% 0.14/0.38 (~(![X0: $i] : (addition(X0, X0) = X0) <=> (addition(one, one) = one))),
% 0.14/0.39 inference(modus_ponens,[status(thm)],[19, 13])).
% 0.14/0.39 tff(21,plain,
% 0.14/0.39 (~(![X0: $i] : (addition(X0, X0) = X0) <=> (addition(one, one) = one))),
% 0.14/0.39 inference(modus_ponens,[status(thm)],[20, 16])).
% 0.14/0.39 unexpected number of arguments: (let ((a!1 (lambda ((X0 $i))
% 0.14/0.39 (refl (~ (= (addition X0 X0) X0) (= (addition X0 X0) X0)))))
% 0.14/0.39 (a!2 (forall ((X0 $i)) (= (addition X0 X0) X0)))
% 0.14/0.39 (a!4 (refl (~ (= (addition one one) one) (= (addition one one) one))))
% 0.14/0.39 (a!5 (~ (not (= (addition one one) one)) (not (= (addition one one) one))))
% 0.14/0.39 (a!7 (or (not (= (addition X0!0 X0!0) X0!0))
% 0.14/0.39 (not (= (addition one one) one)))))
% 0.14/0.39 (let ((a!3 (~ (not a!2) (not (= (addition X0!0 X0!0) X0!0))))
% 0.14/0.39 (a!6 (not (= a!2 (= (addition one one) one))))
% 0.14/0.39 (a!8 (and (or a!2 (= (addition one one) one)) a!7)))
% 0.14/0.39 (nnf-neg (nnf-pos (proof-bind a!1) (~ a!2 a!2))
% 0.14/0.39 (sk a!3)
% 0.14/0.39 a!4
% 0.14/0.39 (refl a!5)
% 0.14/0.39 (~ a!6 a!8))))
% 0.14/0.39 Proof display could not be completed: unexpected number of arguments
% 0.14/0.39 % E exiting
%------------------------------------------------------------------------------