%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : SYN250-1 : TPTP v9.0.0. Released v1.1.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:35 AM UTC 2025
% Result : Unsatisfiable 0.19s 0.48s
% Output : Proof 0.19s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.11 % Problem : SYN250-1 : TPTP v9.0.0. Released v1.1.0.
% 0.10/0.11 % Command : run_E %s %d THM
% 0.11/0.32 % Computer : n005.cluster.edu
% 0.11/0.32 % Model : x86_64 x86_64
% 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.32 % Memory : 8042.1875MB
% 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.32 % CPULimit : 300
% 0.11/0.32 % WCLimit : 300
% 0.11/0.32 % DateTime : Fri Jun 20 12:29:50 EDT 2025
% 0.11/0.32 % CPUTime :
% 0.19/0.48 % SZS status Unsatisfiable
% 0.19/0.48 % SZS output start Proof
% 0.19/0.48 tff(m1_type, type, (
% 0.19/0.48 m1: ( $i * $i * $i ) > $o)).
% 0.19/0.48 tff(a_type, type, (
% 0.19/0.48 a: $i)).
% 0.19/0.48 tff(b_type, type, (
% 0.19/0.48 b: $i)).
% 0.19/0.48 tff(c_type, type, (
% 0.19/0.48 c: $i)).
% 0.19/0.48 tff(s0_type, type, (
% 0.19/0.48 s0: $i > $o)).
% 0.19/0.48 tff(p0_type, type, (
% 0.19/0.48 p0: ( $i * $i ) > $o)).
% 0.19/0.48 tff(m0_type, type, (
% 0.19/0.48 m0: ( $i * $i * $i ) > $o)).
% 0.19/0.48 tff(d_type, type, (
% 0.19/0.48 d: $i)).
% 0.19/0.48 tff(q0_type, type, (
% 0.19/0.48 q0: ( $i * $i ) > $o)).
% 0.19/0.48 tff(l0_type, type, (
% 0.19/0.48 l0: $i > $o)).
% 0.19/0.48 tff(e_type, type, (
% 0.19/0.48 e: $i)).
% 0.19/0.48 tff(r0_type, type, (
% 0.19/0.48 r0: $i > $o)).
% 0.19/0.48 tff(1,plain,
% 0.19/0.48 (^[I: $i, H: $i] : refl((m1(H, I, H) | (~p0(H, I)) | (~s0(H))) <=> (m1(H, I, H) | (~p0(H, I)) | (~s0(H))))),
% 0.19/0.48 inference(bind,[status(th)],[])).
% 0.19/0.48 tff(2,plain,
% 0.19/0.48 (![I: $i, H: $i] : (m1(H, I, H) | (~p0(H, I)) | (~s0(H))) <=> ![I: $i, H: $i] : (m1(H, I, H) | (~p0(H, I)) | (~s0(H)))),
% 0.19/0.48 inference(quant_intro,[status(thm)],[1])).
% 0.19/0.48 tff(3,plain,
% 0.19/0.48 (![I: $i, H: $i] : (m1(H, I, H) | (~p0(H, I)) | (~s0(H))) <=> ![I: $i, H: $i] : (m1(H, I, H) | (~p0(H, I)) | (~s0(H)))),
% 0.19/0.48 inference(rewrite,[status(thm)],[])).
% 0.19/0.48 tff(4,plain,
% 0.19/0.48 (^[I: $i, H: $i] : trans(monotonicity(rewrite((m1(H, I, H) | (~p0(H, I))) <=> (m1(H, I, H) | (~p0(H, I)))), (((m1(H, I, H) | (~p0(H, I))) | (~s0(H))) <=> ((m1(H, I, H) | (~p0(H, I))) | (~s0(H))))), rewrite(((m1(H, I, H) | (~p0(H, I))) | (~s0(H))) <=> (m1(H, I, H) | (~p0(H, I)) | (~s0(H)))), (((m1(H, I, H) | (~p0(H, I))) | (~s0(H))) <=> (m1(H, I, H) | (~p0(H, I)) | (~s0(H)))))),
% 0.19/0.48 inference(bind,[status(th)],[])).
% 0.19/0.48 tff(5,plain,
% 0.19/0.48 (![I: $i, H: $i] : ((m1(H, I, H) | (~p0(H, I))) | (~s0(H))) <=> ![I: $i, H: $i] : (m1(H, I, H) | (~p0(H, I)) | (~s0(H)))),
% 0.19/0.48 inference(quant_intro,[status(thm)],[4])).
% 0.19/0.48 tff(6,axiom,(![I: $i, H: $i] : ((m1(H, I, H) | (~p0(H, I))) | (~s0(H)))), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax','rule_029')).
% 0.19/0.48 tff(7,plain,
% 0.19/0.48 (![I: $i, H: $i] : (m1(H, I, H) | (~p0(H, I)) | (~s0(H)))),
% 0.19/0.48 inference(modus_ponens,[status(thm)],[6, 5])).
% 0.19/0.48 tff(8,plain,
% 0.19/0.48 (![I: $i, H: $i] : (m1(H, I, H) | (~p0(H, I)) | (~s0(H)))),
% 0.19/0.48 inference(modus_ponens,[status(thm)],[7, 3])).
% 0.19/0.48 tff(9,plain,(
% 0.19/0.48 ![I: $i, H: $i] : (m1(H, I, H) | (~p0(H, I)) | (~s0(H)))),
% 0.19/0.48 inference(skolemize,[status(sab)],[8])).
% 0.19/0.48 tff(10,plain,
% 0.19/0.48 (![I: $i, H: $i] : (m1(H, I, H) | (~p0(H, I)) | (~s0(H)))),
% 0.19/0.48 inference(modus_ponens,[status(thm)],[9, 2])).
% 0.19/0.48 tff(11,plain,
% 0.19/0.48 (p0(b, c) <=> p0(b, c)),
% 0.19/0.48 inference(rewrite,[status(thm)],[])).
% 0.19/0.48 tff(12,axiom,(p0(b, c)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax','axiom_22')).
% 0.19/0.48 tff(13,plain,
% 0.19/0.48 (p0(b, c)),
% 0.19/0.48 inference(modus_ponens,[status(thm)],[12, 11])).
% 0.19/0.48 tff(14,plain,
% 0.19/0.48 (s0(b) <=> s0(b)),
% 0.19/0.48 inference(rewrite,[status(thm)],[])).
% 0.19/0.48 tff(15,axiom,(s0(b)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax','axiom_5')).
% 0.19/0.48 tff(16,plain,
% 0.19/0.48 (s0(b)),
% 0.19/0.48 inference(modus_ponens,[status(thm)],[15, 14])).
% 0.19/0.48 tff(17,plain,
% 0.19/0.48 (((~![I: $i, H: $i] : (m1(H, I, H) | (~p0(H, I)) | (~s0(H)))) | ((~s0(b)) | (~p0(b, c)) | m1(b, c, b))) <=> ((~![I: $i, H: $i] : (m1(H, I, H) | (~p0(H, I)) | (~s0(H)))) | (~s0(b)) | (~p0(b, c)) | m1(b, c, b))),
% 0.19/0.48 inference(rewrite,[status(thm)],[])).
% 0.19/0.48 tff(18,plain,
% 0.19/0.48 ((m1(b, c, b) | (~p0(b, c)) | (~s0(b))) <=> ((~s0(b)) | (~p0(b, c)) | m1(b, c, b))),
% 0.19/0.48 inference(rewrite,[status(thm)],[])).
% 0.19/0.48 tff(19,plain,
% 0.19/0.48 (((~![I: $i, H: $i] : (m1(H, I, H) | (~p0(H, I)) | (~s0(H)))) | (m1(b, c, b) | (~p0(b, c)) | (~s0(b)))) <=> ((~![I: $i, H: $i] : (m1(H, I, H) | (~p0(H, I)) | (~s0(H)))) | ((~s0(b)) | (~p0(b, c)) | m1(b, c, b)))),
% 0.19/0.48 inference(monotonicity,[status(thm)],[18])).
% 0.19/0.48 tff(20,plain,
% 0.19/0.48 (((~![I: $i, H: $i] : (m1(H, I, H) | (~p0(H, I)) | (~s0(H)))) | (m1(b, c, b) | (~p0(b, c)) | (~s0(b)))) <=> ((~![I: $i, H: $i] : (m1(H, I, H) | (~p0(H, I)) | (~s0(H)))) | (~s0(b)) | (~p0(b, c)) | m1(b, c, b))),
% 0.19/0.48 inference(transitivity,[status(thm)],[19, 17])).
% 0.19/0.48 tff(21,plain,
% 0.19/0.48 ((~![I: $i, H: $i] : (m1(H, I, H) | (~p0(H, I)) | (~s0(H)))) | (m1(b, c, b) | (~p0(b, c)) | (~s0(b)))),
% 0.19/0.48 inference(quant_inst,[status(thm)],[])).
% 0.19/0.48 tff(22,plain,
% 0.19/0.48 ((~![I: $i, H: $i] : (m1(H, I, H) | (~p0(H, I)) | (~s0(H)))) | (~s0(b)) | (~p0(b, c)) | m1(b, c, b)),
% 0.19/0.49 inference(modus_ponens,[status(thm)],[21, 20])).
% 0.19/0.49 tff(23,plain,
% 0.19/0.49 (m1(b, c, b)),
% 0.19/0.49 inference(unit_resolution,[status(thm)],[22, 16, 13, 10])).
% 0.19/0.49 tff(24,assumption,(~m0(a, d, a)), introduced(assumption)).
% 0.19/0.49 tff(25,plain,
% 0.19/0.49 (^[X: $i] : refl(m0(a, X, a) <=> m0(a, X, a))),
% 0.19/0.49 inference(bind,[status(th)],[])).
% 0.19/0.49 tff(26,plain,
% 0.19/0.49 (![X: $i] : m0(a, X, a) <=> ![X: $i] : m0(a, X, a)),
% 0.19/0.49 inference(quant_intro,[status(thm)],[25])).
% 0.19/0.49 tff(27,plain,
% 0.19/0.49 (![X: $i] : m0(a, X, a) <=> ![X: $i] : m0(a, X, a)),
% 0.19/0.49 inference(rewrite,[status(thm)],[])).
% 0.19/0.49 tff(28,axiom,(![X: $i] : m0(a, X, a)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax','axiom_12')).
% 0.19/0.49 tff(29,plain,
% 0.19/0.49 (![X: $i] : m0(a, X, a)),
% 0.19/0.49 inference(modus_ponens,[status(thm)],[28, 27])).
% 0.19/0.49 tff(30,plain,(
% 0.19/0.49 ![X: $i] : m0(a, X, a)),
% 0.19/0.49 inference(skolemize,[status(sab)],[29])).
% 0.19/0.49 tff(31,plain,
% 0.19/0.49 (![X: $i] : m0(a, X, a)),
% 0.19/0.49 inference(modus_ponens,[status(thm)],[30, 26])).
% 0.19/0.49 tff(32,plain,
% 0.19/0.49 ((~![X: $i] : m0(a, X, a)) | m0(a, d, a)),
% 0.19/0.49 inference(quant_inst,[status(thm)],[])).
% 0.19/0.49 tff(33,plain,
% 0.19/0.49 ($false),
% 0.19/0.49 inference(unit_resolution,[status(thm)],[32, 31, 24])).
% 0.19/0.49 tff(34,plain,(m0(a, d, a)), inference(lemma,lemma(discharge,[]))).
% 0.19/0.49 tff(35,plain,
% 0.19/0.49 (^[H: $i, F: $i, G: $i] : refl(((~q0(F, G)) | (~m1(G, c, G)) | (~m0(a, H, a)) | m1(F, a, G)) <=> ((~q0(F, G)) | (~m1(G, c, G)) | (~m0(a, H, a)) | m1(F, a, G)))),
% 0.19/0.49 inference(bind,[status(th)],[])).
% 0.19/0.49 tff(36,plain,
% 0.19/0.49 (![H: $i, F: $i, G: $i] : ((~q0(F, G)) | (~m1(G, c, G)) | (~m0(a, H, a)) | m1(F, a, G)) <=> ![H: $i, F: $i, G: $i] : ((~q0(F, G)) | (~m1(G, c, G)) | (~m0(a, H, a)) | m1(F, a, G))),
% 0.19/0.49 inference(quant_intro,[status(thm)],[35])).
% 0.19/0.49 tff(37,plain,
% 0.19/0.49 (![H: $i, F: $i, G: $i] : ((~q0(F, G)) | (~m1(G, c, G)) | (~m0(a, H, a)) | m1(F, a, G)) <=> ![H: $i, F: $i, G: $i] : ((~q0(F, G)) | (~m1(G, c, G)) | (~m0(a, H, a)) | m1(F, a, G))),
% 0.19/0.49 inference(rewrite,[status(thm)],[])).
% 0.19/0.49 tff(38,plain,
% 0.19/0.49 (^[H: $i, F: $i, G: $i] : trans(monotonicity(trans(monotonicity(rewrite((m1(F, a, G) | (~m0(a, H, a))) <=> ((~m0(a, H, a)) | m1(F, a, G))), (((m1(F, a, G) | (~m0(a, H, a))) | (~q0(F, G))) <=> (((~m0(a, H, a)) | m1(F, a, G)) | (~q0(F, G))))), rewrite((((~m0(a, H, a)) | m1(F, a, G)) | (~q0(F, G))) <=> ((~q0(F, G)) | (~m0(a, H, a)) | m1(F, a, G))), (((m1(F, a, G) | (~m0(a, H, a))) | (~q0(F, G))) <=> ((~q0(F, G)) | (~m0(a, H, a)) | m1(F, a, G)))), ((((m1(F, a, G) | (~m0(a, H, a))) | (~q0(F, G))) | (~m1(G, c, G))) <=> (((~q0(F, G)) | (~m0(a, H, a)) | m1(F, a, G)) | (~m1(G, c, G))))), rewrite((((~q0(F, G)) | (~m0(a, H, a)) | m1(F, a, G)) | (~m1(G, c, G))) <=> ((~q0(F, G)) | (~m1(G, c, G)) | (~m0(a, H, a)) | m1(F, a, G))), ((((m1(F, a, G) | (~m0(a, H, a))) | (~q0(F, G))) | (~m1(G, c, G))) <=> ((~q0(F, G)) | (~m1(G, c, G)) | (~m0(a, H, a)) | m1(F, a, G))))),
% 0.19/0.49 inference(bind,[status(th)],[])).
% 0.19/0.49 tff(39,plain,
% 0.19/0.49 (![H: $i, F: $i, G: $i] : (((m1(F, a, G) | (~m0(a, H, a))) | (~q0(F, G))) | (~m1(G, c, G))) <=> ![H: $i, F: $i, G: $i] : ((~q0(F, G)) | (~m1(G, c, G)) | (~m0(a, H, a)) | m1(F, a, G))),
% 0.19/0.49 inference(quant_intro,[status(thm)],[38])).
% 0.19/0.49 tff(40,axiom,(![H: $i, F: $i, G: $i] : (((m1(F, a, G) | (~m0(a, H, a))) | (~q0(F, G))) | (~m1(G, c, G)))), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax','rule_024')).
% 0.19/0.49 tff(41,plain,
% 0.19/0.49 (![H: $i, F: $i, G: $i] : ((~q0(F, G)) | (~m1(G, c, G)) | (~m0(a, H, a)) | m1(F, a, G))),
% 0.19/0.49 inference(modus_ponens,[status(thm)],[40, 39])).
% 0.19/0.49 tff(42,plain,
% 0.19/0.49 (![H: $i, F: $i, G: $i] : ((~q0(F, G)) | (~m1(G, c, G)) | (~m0(a, H, a)) | m1(F, a, G))),
% 0.19/0.49 inference(modus_ponens,[status(thm)],[41, 37])).
% 0.19/0.49 tff(43,plain,(
% 0.19/0.49 ![H: $i, F: $i, G: $i] : ((~q0(F, G)) | (~m1(G, c, G)) | (~m0(a, H, a)) | m1(F, a, G))),
% 0.19/0.49 inference(skolemize,[status(sab)],[42])).
% 0.19/0.49 tff(44,plain,
% 0.19/0.49 (![H: $i, F: $i, G: $i] : ((~q0(F, G)) | (~m1(G, c, G)) | (~m0(a, H, a)) | m1(F, a, G))),
% 0.19/0.49 inference(modus_ponens,[status(thm)],[43, 36])).
% 0.19/0.49 tff(45,plain,
% 0.19/0.49 (q0(a, b) <=> q0(a, b)),
% 0.19/0.49 inference(rewrite,[status(thm)],[])).
% 0.19/0.49 tff(46,axiom,(q0(a, b)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax','axiom_36')).
% 0.19/0.49 tff(47,plain,
% 0.19/0.49 (q0(a, b)),
% 0.19/0.49 inference(modus_ponens,[status(thm)],[46, 45])).
% 0.19/0.49 tff(48,plain,
% 0.19/0.49 (((~![H: $i, F: $i, G: $i] : ((~q0(F, G)) | (~m1(G, c, G)) | (~m0(a, H, a)) | m1(F, a, G))) | ((~m0(a, d, a)) | (~q0(a, b)) | (~m1(b, c, b)) | m1(a, a, b))) <=> ((~![H: $i, F: $i, G: $i] : ((~q0(F, G)) | (~m1(G, c, G)) | (~m0(a, H, a)) | m1(F, a, G))) | (~m0(a, d, a)) | (~q0(a, b)) | (~m1(b, c, b)) | m1(a, a, b))),
% 0.19/0.49 inference(rewrite,[status(thm)],[])).
% 0.19/0.49 tff(49,plain,
% 0.19/0.49 (((~q0(a, b)) | (~m1(b, c, b)) | (~m0(a, d, a)) | m1(a, a, b)) <=> ((~m0(a, d, a)) | (~q0(a, b)) | (~m1(b, c, b)) | m1(a, a, b))),
% 0.19/0.49 inference(rewrite,[status(thm)],[])).
% 0.19/0.49 tff(50,plain,
% 0.19/0.49 (((~![H: $i, F: $i, G: $i] : ((~q0(F, G)) | (~m1(G, c, G)) | (~m0(a, H, a)) | m1(F, a, G))) | ((~q0(a, b)) | (~m1(b, c, b)) | (~m0(a, d, a)) | m1(a, a, b))) <=> ((~![H: $i, F: $i, G: $i] : ((~q0(F, G)) | (~m1(G, c, G)) | (~m0(a, H, a)) | m1(F, a, G))) | ((~m0(a, d, a)) | (~q0(a, b)) | (~m1(b, c, b)) | m1(a, a, b)))),
% 0.19/0.49 inference(monotonicity,[status(thm)],[49])).
% 0.19/0.49 tff(51,plain,
% 0.19/0.49 (((~![H: $i, F: $i, G: $i] : ((~q0(F, G)) | (~m1(G, c, G)) | (~m0(a, H, a)) | m1(F, a, G))) | ((~q0(a, b)) | (~m1(b, c, b)) | (~m0(a, d, a)) | m1(a, a, b))) <=> ((~![H: $i, F: $i, G: $i] : ((~q0(F, G)) | (~m1(G, c, G)) | (~m0(a, H, a)) | m1(F, a, G))) | (~m0(a, d, a)) | (~q0(a, b)) | (~m1(b, c, b)) | m1(a, a, b))),
% 0.19/0.49 inference(transitivity,[status(thm)],[50, 48])).
% 0.19/0.49 tff(52,plain,
% 0.19/0.49 ((~![H: $i, F: $i, G: $i] : ((~q0(F, G)) | (~m1(G, c, G)) | (~m0(a, H, a)) | m1(F, a, G))) | ((~q0(a, b)) | (~m1(b, c, b)) | (~m0(a, d, a)) | m1(a, a, b))),
% 0.19/0.49 inference(quant_inst,[status(thm)],[])).
% 0.19/0.49 tff(53,plain,
% 0.19/0.49 ((~![H: $i, F: $i, G: $i] : ((~q0(F, G)) | (~m1(G, c, G)) | (~m0(a, H, a)) | m1(F, a, G))) | (~m0(a, d, a)) | (~q0(a, b)) | (~m1(b, c, b)) | m1(a, a, b)),
% 0.19/0.49 inference(modus_ponens,[status(thm)],[52, 51])).
% 0.19/0.49 tff(54,plain,
% 0.19/0.49 (m1(a, a, b)),
% 0.19/0.49 inference(unit_resolution,[status(thm)],[53, 47, 44, 34, 23])).
% 0.19/0.49 tff(55,plain,
% 0.19/0.49 (l0(a) <=> l0(a)),
% 0.19/0.49 inference(rewrite,[status(thm)],[])).
% 0.19/0.49 tff(56,axiom,(l0(a)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax','axiom_20')).
% 0.19/0.49 tff(57,plain,
% 0.19/0.49 (l0(a)),
% 0.19/0.49 inference(modus_ponens,[status(thm)],[56, 55])).
% 0.19/0.49 tff(58,plain,
% 0.19/0.49 (s0(d) <=> s0(d)),
% 0.19/0.49 inference(rewrite,[status(thm)],[])).
% 0.19/0.49 tff(59,axiom,(s0(d)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax','axiom_1')).
% 0.19/0.49 tff(60,plain,
% 0.19/0.49 (s0(d)),
% 0.19/0.49 inference(modus_ponens,[status(thm)],[59, 58])).
% 0.19/0.49 tff(61,plain,
% 0.19/0.49 ((m1(a, a, a) | (~s0(d)) | (~l0(a))) <=> (m1(a, a, a) | (~s0(d)) | (~l0(a)))),
% 0.19/0.49 inference(rewrite,[status(thm)],[])).
% 0.19/0.49 tff(62,plain,
% 0.19/0.49 (((m1(a, a, a) | (~l0(a))) | (~s0(d))) <=> (m1(a, a, a) | (~s0(d)) | (~l0(a)))),
% 0.19/0.49 inference(rewrite,[status(thm)],[])).
% 0.19/0.49 tff(63,plain,
% 0.19/0.49 ((m1(a, a, a) | (~l0(a))) <=> (m1(a, a, a) | (~l0(a)))),
% 0.19/0.49 inference(rewrite,[status(thm)],[])).
% 0.19/0.49 tff(64,plain,
% 0.19/0.49 (((m1(a, a, a) | (~l0(a))) | (~s0(d))) <=> ((m1(a, a, a) | (~l0(a))) | (~s0(d)))),
% 0.19/0.49 inference(monotonicity,[status(thm)],[63])).
% 0.19/0.49 tff(65,plain,
% 0.19/0.49 (((m1(a, a, a) | (~l0(a))) | (~s0(d))) <=> (m1(a, a, a) | (~s0(d)) | (~l0(a)))),
% 0.19/0.49 inference(transitivity,[status(thm)],[64, 62])).
% 0.19/0.49 tff(66,axiom,((m1(a, a, a) | (~l0(a))) | (~s0(d))), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax','rule_023')).
% 0.19/0.49 tff(67,plain,
% 0.19/0.49 (m1(a, a, a) | (~s0(d)) | (~l0(a))),
% 0.19/0.49 inference(modus_ponens,[status(thm)],[66, 65])).
% 0.19/0.49 tff(68,plain,
% 0.19/0.49 (m1(a, a, a) | (~s0(d)) | (~l0(a))),
% 0.19/0.49 inference(modus_ponens,[status(thm)],[67, 61])).
% 0.19/0.49 tff(69,plain,
% 0.19/0.49 (m1(a, a, a) | (~s0(d)) | (~l0(a))),
% 0.19/0.49 inference(modus_ponens,[status(thm)],[68, 61])).
% 0.19/0.49 tff(70,plain,
% 0.19/0.49 (m1(a, a, a) | (~s0(d)) | (~l0(a))),
% 0.19/0.49 inference(modus_ponens,[status(thm)],[69, 61])).
% 0.19/0.49 tff(71,plain,
% 0.19/0.49 (m1(a, a, a) | (~s0(d)) | (~l0(a))),
% 0.19/0.49 inference(modus_ponens,[status(thm)],[70, 61])).
% 0.19/0.49 tff(72,plain,
% 0.19/0.49 (m1(a, a, a)),
% 0.19/0.49 inference(unit_resolution,[status(thm)],[71, 60, 57])).
% 0.19/0.49 tff(73,plain,
% 0.19/0.49 (^[I: $i, A: $i, J: $i, H: $i] : refl(((~m1(J, A, I)) | (~m1(J, I, H)) | m1(H, I, I)) <=> ((~m1(J, A, I)) | (~m1(J, I, H)) | m1(H, I, I)))),
% 0.19/0.49 inference(bind,[status(th)],[])).
% 0.19/0.49 tff(74,plain,
% 0.19/0.49 (![I: $i, A: $i, J: $i, H: $i] : ((~m1(J, A, I)) | (~m1(J, I, H)) | m1(H, I, I)) <=> ![I: $i, A: $i, J: $i, H: $i] : ((~m1(J, A, I)) | (~m1(J, I, H)) | m1(H, I, I))),
% 0.19/0.49 inference(quant_intro,[status(thm)],[73])).
% 0.19/0.49 tff(75,plain,
% 0.19/0.49 (![I: $i, A: $i, J: $i, H: $i] : ((~m1(J, A, I)) | (~m1(J, I, H)) | m1(H, I, I)) <=> ![I: $i, A: $i, J: $i, H: $i] : ((~m1(J, A, I)) | (~m1(J, I, H)) | m1(H, I, I))),
% 0.19/0.49 inference(rewrite,[status(thm)],[])).
% 0.19/0.49 tff(76,plain,
% 0.19/0.49 (^[I: $i, A: $i, J: $i, H: $i] : trans(monotonicity(rewrite((m1(H, I, I) | (~m1(J, I, H))) <=> ((~m1(J, I, H)) | m1(H, I, I))), (((m1(H, I, I) | (~m1(J, I, H))) | (~m1(J, A, I))) <=> (((~m1(J, I, H)) | m1(H, I, I)) | (~m1(J, A, I))))), rewrite((((~m1(J, I, H)) | m1(H, I, I)) | (~m1(J, A, I))) <=> ((~m1(J, A, I)) | (~m1(J, I, H)) | m1(H, I, I))), (((m1(H, I, I) | (~m1(J, I, H))) | (~m1(J, A, I))) <=> ((~m1(J, A, I)) | (~m1(J, I, H)) | m1(H, I, I))))),
% 0.19/0.49 inference(bind,[status(th)],[])).
% 0.19/0.49 tff(77,plain,
% 0.19/0.49 (![I: $i, A: $i, J: $i, H: $i] : ((m1(H, I, I) | (~m1(J, I, H))) | (~m1(J, A, I))) <=> ![I: $i, A: $i, J: $i, H: $i] : ((~m1(J, A, I)) | (~m1(J, I, H)) | m1(H, I, I))),
% 0.19/0.49 inference(quant_intro,[status(thm)],[76])).
% 0.19/0.49 tff(78,axiom,(![I: $i, A: $i, J: $i, H: $i] : ((m1(H, I, I) | (~m1(J, I, H))) | (~m1(J, A, I)))), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax','rule_016')).
% 0.19/0.49 tff(79,plain,
% 0.19/0.49 (![I: $i, A: $i, J: $i, H: $i] : ((~m1(J, A, I)) | (~m1(J, I, H)) | m1(H, I, I))),
% 0.19/0.49 inference(modus_ponens,[status(thm)],[78, 77])).
% 0.19/0.49 tff(80,plain,
% 0.19/0.49 (![I: $i, A: $i, J: $i, H: $i] : ((~m1(J, A, I)) | (~m1(J, I, H)) | m1(H, I, I))),
% 0.19/0.49 inference(modus_ponens,[status(thm)],[79, 75])).
% 0.19/0.49 tff(81,plain,(
% 0.19/0.49 ![I: $i, A: $i, J: $i, H: $i] : ((~m1(J, A, I)) | (~m1(J, I, H)) | m1(H, I, I))),
% 0.19/0.49 inference(skolemize,[status(sab)],[80])).
% 0.19/0.49 tff(82,plain,
% 0.19/0.49 (![I: $i, A: $i, J: $i, H: $i] : ((~m1(J, A, I)) | (~m1(J, I, H)) | m1(H, I, I))),
% 0.19/0.49 inference(modus_ponens,[status(thm)],[81, 74])).
% 0.19/0.49 tff(83,plain,
% 0.19/0.49 (((~![I: $i, A: $i, J: $i, H: $i] : ((~m1(J, A, I)) | (~m1(J, I, H)) | m1(H, I, I))) | ((~m1(a, a, a)) | (~m1(a, a, b)) | m1(b, a, a))) <=> ((~![I: $i, A: $i, J: $i, H: $i] : ((~m1(J, A, I)) | (~m1(J, I, H)) | m1(H, I, I))) | (~m1(a, a, a)) | (~m1(a, a, b)) | m1(b, a, a))),
% 0.19/0.49 inference(rewrite,[status(thm)],[])).
% 0.19/0.49 tff(84,plain,
% 0.19/0.49 ((~![I: $i, A: $i, J: $i, H: $i] : ((~m1(J, A, I)) | (~m1(J, I, H)) | m1(H, I, I))) | ((~m1(a, a, a)) | (~m1(a, a, b)) | m1(b, a, a))),
% 0.19/0.49 inference(quant_inst,[status(thm)],[])).
% 0.19/0.49 tff(85,plain,
% 0.19/0.49 ((~![I: $i, A: $i, J: $i, H: $i] : ((~m1(J, A, I)) | (~m1(J, I, H)) | m1(H, I, I))) | (~m1(a, a, a)) | (~m1(a, a, b)) | m1(b, a, a)),
% 0.19/0.49 inference(modus_ponens,[status(thm)],[84, 83])).
% 0.19/0.49 tff(86,plain,
% 0.19/0.49 (m1(b, a, a)),
% 0.19/0.49 inference(unit_resolution,[status(thm)],[85, 82, 72, 54])).
% 0.19/0.49 tff(87,plain,
% 0.19/0.49 ((~m1(e, a, a)) <=> (~m1(e, a, a))),
% 0.19/0.49 inference(rewrite,[status(thm)],[])).
% 0.19/0.49 tff(88,axiom,(~m1(e, a, a)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','prove_this')).
% 0.19/0.49 tff(89,plain,
% 0.19/0.49 (~m1(e, a, a)),
% 0.19/0.49 inference(modus_ponens,[status(thm)],[88, 87])).
% 0.19/0.49 tff(90,assumption,(~m1(e, c, e)), introduced(assumption)).
% 0.19/0.49 tff(91,plain,
% 0.19/0.49 (^[I: $i, J: $i] : refl((m1(I, J, I) | (~r0(I)) | (~l0(J))) <=> (m1(I, J, I) | (~r0(I)) | (~l0(J))))),
% 0.19/0.49 inference(bind,[status(th)],[])).
% 0.19/0.49 tff(92,plain,
% 0.19/0.49 (![I: $i, J: $i] : (m1(I, J, I) | (~r0(I)) | (~l0(J))) <=> ![I: $i, J: $i] : (m1(I, J, I) | (~r0(I)) | (~l0(J)))),
% 0.19/0.49 inference(quant_intro,[status(thm)],[91])).
% 0.19/0.49 tff(93,plain,
% 0.19/0.49 (![I: $i, J: $i] : (m1(I, J, I) | (~r0(I)) | (~l0(J))) <=> ![I: $i, J: $i] : (m1(I, J, I) | (~r0(I)) | (~l0(J)))),
% 0.19/0.49 inference(rewrite,[status(thm)],[])).
% 0.19/0.49 tff(94,plain,
% 0.19/0.49 (^[I: $i, J: $i] : trans(monotonicity(rewrite((m1(I, J, I) | (~r0(I))) <=> (m1(I, J, I) | (~r0(I)))), (((m1(I, J, I) | (~r0(I))) | (~l0(J))) <=> ((m1(I, J, I) | (~r0(I))) | (~l0(J))))), rewrite(((m1(I, J, I) | (~r0(I))) | (~l0(J))) <=> (m1(I, J, I) | (~r0(I)) | (~l0(J)))), (((m1(I, J, I) | (~r0(I))) | (~l0(J))) <=> (m1(I, J, I) | (~r0(I)) | (~l0(J)))))),
% 0.19/0.49 inference(bind,[status(th)],[])).
% 0.19/0.49 tff(95,plain,
% 0.19/0.49 (![I: $i, J: $i] : ((m1(I, J, I) | (~r0(I))) | (~l0(J))) <=> ![I: $i, J: $i] : (m1(I, J, I) | (~r0(I)) | (~l0(J)))),
% 0.19/0.49 inference(quant_intro,[status(thm)],[94])).
% 0.19/0.49 tff(96,axiom,(![I: $i, J: $i] : ((m1(I, J, I) | (~r0(I))) | (~l0(J)))), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax','rule_035')).
% 0.19/0.49 tff(97,plain,
% 0.19/0.49 (![I: $i, J: $i] : (m1(I, J, I) | (~r0(I)) | (~l0(J)))),
% 0.19/0.49 inference(modus_ponens,[status(thm)],[96, 95])).
% 0.19/0.49 tff(98,plain,
% 0.19/0.49 (![I: $i, J: $i] : (m1(I, J, I) | (~r0(I)) | (~l0(J)))),
% 0.19/0.49 inference(modus_ponens,[status(thm)],[97, 93])).
% 0.19/0.49 tff(99,plain,(
% 0.19/0.49 ![I: $i, J: $i] : (m1(I, J, I) | (~r0(I)) | (~l0(J)))),
% 0.19/0.49 inference(skolemize,[status(sab)],[98])).
% 0.19/0.49 tff(100,plain,
% 0.19/0.49 (![I: $i, J: $i] : (m1(I, J, I) | (~r0(I)) | (~l0(J)))),
% 0.19/0.49 inference(modus_ponens,[status(thm)],[99, 92])).
% 0.19/0.49 tff(101,plain,
% 0.19/0.49 (l0(c) <=> l0(c)),
% 0.19/0.49 inference(rewrite,[status(thm)],[])).
% 0.19/0.49 tff(102,axiom,(l0(c)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax','axiom_24')).
% 0.19/0.49 tff(103,plain,
% 0.19/0.49 (l0(c)),
% 0.19/0.49 inference(modus_ponens,[status(thm)],[102, 101])).
% 0.19/0.49 tff(104,plain,
% 0.19/0.49 (r0(e) <=> r0(e)),
% 0.19/0.49 inference(rewrite,[status(thm)],[])).
% 0.19/0.49 tff(105,axiom,(r0(e)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax','axiom_13')).
% 0.19/0.49 tff(106,plain,
% 0.19/0.49 (r0(e)),
% 0.19/0.49 inference(modus_ponens,[status(thm)],[105, 104])).
% 0.19/0.49 tff(107,plain,
% 0.19/0.49 (((~![I: $i, J: $i] : (m1(I, J, I) | (~r0(I)) | (~l0(J)))) | ((~r0(e)) | (~l0(c)) | m1(e, c, e))) <=> ((~![I: $i, J: $i] : (m1(I, J, I) | (~r0(I)) | (~l0(J)))) | (~r0(e)) | (~l0(c)) | m1(e, c, e))),
% 0.19/0.49 inference(rewrite,[status(thm)],[])).
% 0.19/0.49 tff(108,plain,
% 0.19/0.49 ((m1(e, c, e) | (~r0(e)) | (~l0(c))) <=> ((~r0(e)) | (~l0(c)) | m1(e, c, e))),
% 0.19/0.49 inference(rewrite,[status(thm)],[])).
% 0.19/0.49 tff(109,plain,
% 0.19/0.49 (((~![I: $i, J: $i] : (m1(I, J, I) | (~r0(I)) | (~l0(J)))) | (m1(e, c, e) | (~r0(e)) | (~l0(c)))) <=> ((~![I: $i, J: $i] : (m1(I, J, I) | (~r0(I)) | (~l0(J)))) | ((~r0(e)) | (~l0(c)) | m1(e, c, e)))),
% 0.19/0.49 inference(monotonicity,[status(thm)],[108])).
% 0.19/0.49 tff(110,plain,
% 0.19/0.49 (((~![I: $i, J: $i] : (m1(I, J, I) | (~r0(I)) | (~l0(J)))) | (m1(e, c, e) | (~r0(e)) | (~l0(c)))) <=> ((~![I: $i, J: $i] : (m1(I, J, I) | (~r0(I)) | (~l0(J)))) | (~r0(e)) | (~l0(c)) | m1(e, c, e))),
% 0.19/0.49 inference(transitivity,[status(thm)],[109, 107])).
% 0.19/0.49 tff(111,plain,
% 0.19/0.49 ((~![I: $i, J: $i] : (m1(I, J, I) | (~r0(I)) | (~l0(J)))) | (m1(e, c, e) | (~r0(e)) | (~l0(c)))),
% 0.19/0.49 inference(quant_inst,[status(thm)],[])).
% 0.19/0.49 tff(112,plain,
% 0.19/0.49 ((~![I: $i, J: $i] : (m1(I, J, I) | (~r0(I)) | (~l0(J)))) | (~r0(e)) | (~l0(c)) | m1(e, c, e)),
% 0.19/0.49 inference(modus_ponens,[status(thm)],[111, 110])).
% 0.19/0.49 tff(113,plain,
% 0.19/0.49 ($false),
% 0.19/0.49 inference(unit_resolution,[status(thm)],[112, 106, 103, 100, 90])).
% 0.19/0.49 tff(114,plain,(m1(e, c, e)), inference(lemma,lemma(discharge,[]))).
% 0.19/0.49 tff(115,plain,
% 0.19/0.49 (q0(b, e) <=> q0(b, e)),
% 0.19/0.49 inference(rewrite,[status(thm)],[])).
% 0.19/0.49 tff(116,axiom,(q0(b, e)), file('/export/starexec/sandbox/benchmark/Axioms/SYN001-0.ax','axiom_21')).
% 0.19/0.49 tff(117,plain,
% 0.19/0.49 (q0(b, e)),
% 0.19/0.49 inference(modus_ponens,[status(thm)],[116, 115])).
% 0.19/0.49 tff(118,plain,
% 0.19/0.49 (((~![H: $i, F: $i, G: $i] : ((~q0(F, G)) | (~m1(G, c, G)) | (~m0(a, H, a)) | m1(F, a, G))) | ((~q0(b, e)) | m1(b, a, e) | (~m0(a, d, a)) | (~m1(e, c, e)))) <=> ((~![H: $i, F: $i, G: $i] : ((~q0(F, G)) | (~m1(G, c, G)) | (~m0(a, H, a)) | m1(F, a, G))) | (~q0(b, e)) | m1(b, a, e) | (~m0(a, d, a)) | (~m1(e, c, e)))),
% 0.19/0.49 inference(rewrite,[status(thm)],[])).
% 0.19/0.49 tff(119,plain,
% 0.19/0.49 (((~q0(b, e)) | (~m1(e, c, e)) | (~m0(a, d, a)) | m1(b, a, e)) <=> ((~q0(b, e)) | m1(b, a, e) | (~m0(a, d, a)) | (~m1(e, c, e)))),
% 0.19/0.49 inference(rewrite,[status(thm)],[])).
% 0.19/0.49 tff(120,plain,
% 0.19/0.49 (((~![H: $i, F: $i, G: $i] : ((~q0(F, G)) | (~m1(G, c, G)) | (~m0(a, H, a)) | m1(F, a, G))) | ((~q0(b, e)) | (~m1(e, c, e)) | (~m0(a, d, a)) | m1(b, a, e))) <=> ((~![H: $i, F: $i, G: $i] : ((~q0(F, G)) | (~m1(G, c, G)) | (~m0(a, H, a)) | m1(F, a, G))) | ((~q0(b, e)) | m1(b, a, e) | (~m0(a, d, a)) | (~m1(e, c, e))))),
% 0.19/0.49 inference(monotonicity,[status(thm)],[119])).
% 0.19/0.50 tff(121,plain,
% 0.19/0.50 (((~![H: $i, F: $i, G: $i] : ((~q0(F, G)) | (~m1(G, c, G)) | (~m0(a, H, a)) | m1(F, a, G))) | ((~q0(b, e)) | (~m1(e, c, e)) | (~m0(a, d, a)) | m1(b, a, e))) <=> ((~![H: $i, F: $i, G: $i] : ((~q0(F, G)) | (~m1(G, c, G)) | (~m0(a, H, a)) | m1(F, a, G))) | (~q0(b, e)) | m1(b, a, e) | (~m0(a, d, a)) | (~m1(e, c, e)))),
% 0.19/0.50 inference(transitivity,[status(thm)],[120, 118])).
% 0.19/0.50 tff(122,plain,
% 0.19/0.50 ((~![H: $i, F: $i, G: $i] : ((~q0(F, G)) | (~m1(G, c, G)) | (~m0(a, H, a)) | m1(F, a, G))) | ((~q0(b, e)) | (~m1(e, c, e)) | (~m0(a, d, a)) | m1(b, a, e))),
% 0.19/0.50 inference(quant_inst,[status(thm)],[])).
% 0.19/0.50 tff(123,plain,
% 0.19/0.50 ((~![H: $i, F: $i, G: $i] : ((~q0(F, G)) | (~m1(G, c, G)) | (~m0(a, H, a)) | m1(F, a, G))) | (~q0(b, e)) | m1(b, a, e) | (~m0(a, d, a)) | (~m1(e, c, e))),
% 0.19/0.50 inference(modus_ponens,[status(thm)],[122, 121])).
% 0.19/0.50 tff(124,plain,
% 0.19/0.50 (m1(b, a, e) | (~m1(e, c, e))),
% 0.19/0.50 inference(unit_resolution,[status(thm)],[123, 117, 44, 34])).
% 0.19/0.50 tff(125,plain,
% 0.19/0.50 (m1(b, a, e)),
% 0.19/0.50 inference(unit_resolution,[status(thm)],[124, 114])).
% 0.19/0.50 tff(126,plain,
% 0.19/0.50 (((~![I: $i, A: $i, J: $i, H: $i] : ((~m1(J, A, I)) | (~m1(J, I, H)) | m1(H, I, I))) | ((~m1(b, a, a)) | (~m1(b, a, e)) | m1(e, a, a))) <=> ((~![I: $i, A: $i, J: $i, H: $i] : ((~m1(J, A, I)) | (~m1(J, I, H)) | m1(H, I, I))) | (~m1(b, a, a)) | (~m1(b, a, e)) | m1(e, a, a))),
% 0.19/0.50 inference(rewrite,[status(thm)],[])).
% 0.19/0.50 tff(127,plain,
% 0.19/0.50 ((~![I: $i, A: $i, J: $i, H: $i] : ((~m1(J, A, I)) | (~m1(J, I, H)) | m1(H, I, I))) | ((~m1(b, a, a)) | (~m1(b, a, e)) | m1(e, a, a))),
% 0.19/0.50 inference(quant_inst,[status(thm)],[])).
% 0.19/0.50 tff(128,plain,
% 0.19/0.50 ((~![I: $i, A: $i, J: $i, H: $i] : ((~m1(J, A, I)) | (~m1(J, I, H)) | m1(H, I, I))) | (~m1(b, a, a)) | (~m1(b, a, e)) | m1(e, a, a)),
% 0.19/0.50 inference(modus_ponens,[status(thm)],[127, 126])).
% 0.19/0.50 tff(129,plain,
% 0.19/0.50 ($false),
% 0.19/0.50 inference(unit_resolution,[status(thm)],[128, 82, 125, 89, 86])).
% 0.19/0.50 % SZS output end Proof
% 0.19/0.51 % E exiting
%------------------------------------------------------------------------------