%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : SYN691-1 : TPTP v9.0.0. Released v2.5.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n011.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:39:50 AM UTC 2025
% Result : Unsatisfiable 1.96s 2.18s
% Output : Proof 1.96s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.13 % Problem : SYN691-1 : TPTP v9.0.0. Released v2.5.0.
% 0.12/0.13 % Command : run_E %s %d THM
% 0.13/0.34 % Computer : n011.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Fri Jun 20 12:39:56 EDT 2025
% 0.13/0.34 % CPUTime :
% 1.96/2.18 % SZS status Unsatisfiable
% 1.96/2.18 % SZS output start Proof
% 1.96/2.18 tff(p39_type, type, (
% 1.96/2.18 p39: ( $i * $i ) > $o)).
% 1.96/2.18 tff(c46_type, type, (
% 1.96/2.18 c46: $i)).
% 1.96/2.18 tff(f5_type, type, (
% 1.96/2.18 f5: ( $i * $i ) > $i)).
% 1.96/2.18 tff(f10_type, type, (
% 1.96/2.18 f10: ( $i * $i ) > $i)).
% 1.96/2.18 tff(f34_type, type, (
% 1.96/2.18 f34: ( $i * $i ) > $i)).
% 1.96/2.18 tff(c45_type, type, (
% 1.96/2.18 c45: $i)).
% 1.96/2.18 tff(f36_type, type, (
% 1.96/2.18 f36: ( $i * $i ) > $i)).
% 1.96/2.18 tff(c44_type, type, (
% 1.96/2.18 c44: $i)).
% 1.96/2.18 tff(f38_type, type, (
% 1.96/2.18 f38: ( $i * $i ) > $i)).
% 1.96/2.18 tff(c43_type, type, (
% 1.96/2.18 c43: $i)).
% 1.96/2.18 tff(c49_type, type, (
% 1.96/2.18 c49: $i)).
% 1.96/2.18 tff(f13_type, type, (
% 1.96/2.18 f13: ( $i * $i ) > $i)).
% 1.96/2.18 tff(f26_type, type, (
% 1.96/2.18 f26: ( $i * $i ) > $i)).
% 1.96/2.18 tff(f28_type, type, (
% 1.96/2.18 f28: ( $i * $i ) > $i)).
% 1.96/2.18 tff(f30_type, type, (
% 1.96/2.18 f30: ( $i * $i ) > $i)).
% 1.96/2.18 tff(c48_type, type, (
% 1.96/2.18 c48: $i)).
% 1.96/2.18 tff(f15_type, type, (
% 1.96/2.18 f15: ( $i * $i ) > $i)).
% 1.96/2.18 tff(f17_type, type, (
% 1.96/2.18 f17: ( $i * $i ) > $i)).
% 1.96/2.18 tff(f19_type, type, (
% 1.96/2.18 f19: ( $i * $i ) > $i)).
% 1.96/2.18 tff(f21_type, type, (
% 1.96/2.18 f21: ( $i * $i ) > $i)).
% 1.96/2.18 tff(c47_type, type, (
% 1.96/2.18 c47: $i)).
% 1.96/2.18 tff(c42_type, type, (
% 1.96/2.18 c42: $i)).
% 1.96/2.18 tff(c40_type, type, (
% 1.96/2.18 c40: $i)).
% 1.96/2.18 tff(p22_type, type, (
% 1.96/2.18 p22: ( $i * $i ) > $o)).
% 1.96/2.18 tff(p4_type, type, (
% 1.96/2.18 p4: ( $i * $i ) > $o)).
% 1.96/2.18 tff(f7_type, type, (
% 1.96/2.18 f7: ( $i * $i ) > $i)).
% 1.96/2.18 tff(c41_type, type, (
% 1.96/2.18 c41: $i)).
% 1.96/2.18 tff(p3_type, type, (
% 1.96/2.18 p3: ( $i * $i ) > $o)).
% 1.96/2.18 tff(p2_type, type, (
% 1.96/2.18 p2: ( $i * $i ) > $o)).
% 1.96/2.18 tff(1,assumption,(p39(f5(c40, f10(f13(f15(c42, f17(f19(f21(c47, c43), c44), c45)), f26(f28(f30(c48, c43), c44), c45)), f34(f36(f38(c49, c43), c44), c45))), c46)), introduced(assumption)).
% 1.96/2.18 tff(2,assumption,(p39(f17(f19(f21(c47, c43), c44), c45), c46)), introduced(assumption)).
% 1.96/2.18 tff(3,plain,
% 1.96/2.18 (^[X105: $i, X104: $i, X103: $i, X106: $i] : refl((p39(f5(c40, f10(f13(f15(c42, X103), X105), X106)), X104) | (~p39(X103, X104))) <=> (p39(f5(c40, f10(f13(f15(c42, X103), X105), X106)), X104) | (~p39(X103, X104))))),
% 1.96/2.18 inference(bind,[status(th)],[])).
% 1.96/2.18 tff(4,plain,
% 1.96/2.18 (![X105: $i, X104: $i, X103: $i, X106: $i] : (p39(f5(c40, f10(f13(f15(c42, X103), X105), X106)), X104) | (~p39(X103, X104))) <=> ![X105: $i, X104: $i, X103: $i, X106: $i] : (p39(f5(c40, f10(f13(f15(c42, X103), X105), X106)), X104) | (~p39(X103, X104)))),
% 1.96/2.19 inference(quant_intro,[status(thm)],[3])).
% 1.96/2.19 tff(5,plain,
% 1.96/2.19 (![X105: $i, X104: $i, X103: $i, X106: $i] : (p39(f5(c40, f10(f13(f15(c42, X103), X105), X106)), X104) | (~p39(X103, X104))) <=> ![X105: $i, X104: $i, X103: $i, X106: $i] : (p39(f5(c40, f10(f13(f15(c42, X103), X105), X106)), X104) | (~p39(X103, X104)))),
% 1.96/2.19 inference(rewrite,[status(thm)],[])).
% 1.96/2.19 tff(6,axiom,(![X105: $i, X104: $i, X103: $i, X106: $i] : (p39(f5(c40, f10(f13(f15(c42, X103), X105), X106)), X104) | (~p39(X103, X104)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','p39_64')).
% 1.96/2.19 tff(7,plain,
% 1.96/2.19 (![X105: $i, X104: $i, X103: $i, X106: $i] : (p39(f5(c40, f10(f13(f15(c42, X103), X105), X106)), X104) | (~p39(X103, X104)))),
% 1.96/2.19 inference(modus_ponens,[status(thm)],[6, 5])).
% 1.96/2.19 tff(8,plain,(
% 1.96/2.19 ![X105: $i, X104: $i, X103: $i, X106: $i] : (p39(f5(c40, f10(f13(f15(c42, X103), X105), X106)), X104) | (~p39(X103, X104)))),
% 1.96/2.19 inference(skolemize,[status(sab)],[7])).
% 1.96/2.19 tff(9,plain,
% 1.96/2.19 (![X105: $i, X104: $i, X103: $i, X106: $i] : (p39(f5(c40, f10(f13(f15(c42, X103), X105), X106)), X104) | (~p39(X103, X104)))),
% 1.96/2.19 inference(modus_ponens,[status(thm)],[8, 4])).
% 1.96/2.19 tff(10,plain,
% 1.96/2.19 ((~p39(f5(c40, f10(f13(f15(c42, c43), c44), c45)), c46)) <=> (~p39(f5(c40, f10(f13(f15(c42, c43), c44), c45)), c46))),
% 1.96/2.19 inference(rewrite,[status(thm)],[])).
% 1.96/2.19 tff(11,axiom,(~p39(f5(c40, f10(f13(f15(c42, c43), c44), c45)), c46)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','not_p39_43')).
% 1.96/2.19 tff(12,plain,
% 1.96/2.19 (~p39(f5(c40, f10(f13(f15(c42, c43), c44), c45)), c46)),
% 1.96/2.19 inference(modus_ponens,[status(thm)],[11, 10])).
% 1.96/2.19 tff(13,plain,
% 1.96/2.19 (((~![X105: $i, X104: $i, X103: $i, X106: $i] : (p39(f5(c40, f10(f13(f15(c42, X103), X105), X106)), X104) | (~p39(X103, X104)))) | (p39(f5(c40, f10(f13(f15(c42, c43), c44), c45)), c46) | (~p39(c43, c46)))) <=> ((~![X105: $i, X104: $i, X103: $i, X106: $i] : (p39(f5(c40, f10(f13(f15(c42, X103), X105), X106)), X104) | (~p39(X103, X104)))) | p39(f5(c40, f10(f13(f15(c42, c43), c44), c45)), c46) | (~p39(c43, c46)))),
% 1.96/2.19 inference(rewrite,[status(thm)],[])).
% 1.96/2.19 tff(14,plain,
% 1.96/2.19 ((~![X105: $i, X104: $i, X103: $i, X106: $i] : (p39(f5(c40, f10(f13(f15(c42, X103), X105), X106)), X104) | (~p39(X103, X104)))) | (p39(f5(c40, f10(f13(f15(c42, c43), c44), c45)), c46) | (~p39(c43, c46)))),
% 1.96/2.19 inference(quant_inst,[status(thm)],[])).
% 1.96/2.19 tff(15,plain,
% 1.96/2.19 ((~![X105: $i, X104: $i, X103: $i, X106: $i] : (p39(f5(c40, f10(f13(f15(c42, X103), X105), X106)), X104) | (~p39(X103, X104)))) | p39(f5(c40, f10(f13(f15(c42, c43), c44), c45)), c46) | (~p39(c43, c46))),
% 1.96/2.19 inference(modus_ponens,[status(thm)],[14, 13])).
% 1.96/2.19 tff(16,plain,
% 1.96/2.19 (~p39(c43, c46)),
% 1.96/2.19 inference(unit_resolution,[status(thm)],[15, 12, 9])).
% 1.96/2.19 tff(17,plain,
% 1.96/2.19 (^[X47: $i, X49: $i, X50: $i, X48: $i] : refl(((~p39(f17(f19(f21(c47, X47), X48), X49), X50)) | p39(X47, X50)) <=> ((~p39(f17(f19(f21(c47, X47), X48), X49), X50)) | p39(X47, X50)))),
% 1.96/2.19 inference(bind,[status(th)],[])).
% 1.96/2.19 tff(18,plain,
% 1.96/2.19 (![X47: $i, X49: $i, X50: $i, X48: $i] : ((~p39(f17(f19(f21(c47, X47), X48), X49), X50)) | p39(X47, X50)) <=> ![X47: $i, X49: $i, X50: $i, X48: $i] : ((~p39(f17(f19(f21(c47, X47), X48), X49), X50)) | p39(X47, X50))),
% 1.96/2.19 inference(quant_intro,[status(thm)],[17])).
% 1.96/2.19 tff(19,plain,
% 1.96/2.19 (![X47: $i, X49: $i, X50: $i, X48: $i] : ((~p39(f17(f19(f21(c47, X47), X48), X49), X50)) | p39(X47, X50)) <=> ![X47: $i, X49: $i, X50: $i, X48: $i] : ((~p39(f17(f19(f21(c47, X47), X48), X49), X50)) | p39(X47, X50))),
% 1.96/2.19 inference(rewrite,[status(thm)],[])).
% 1.96/2.19 tff(20,plain,
% 1.96/2.19 (^[X47: $i, X49: $i, X50: $i, X48: $i] : rewrite((p39(X47, X50) | (~p39(f17(f19(f21(c47, X47), X48), X49), X50))) <=> ((~p39(f17(f19(f21(c47, X47), X48), X49), X50)) | p39(X47, X50)))),
% 1.96/2.19 inference(bind,[status(th)],[])).
% 1.96/2.19 tff(21,plain,
% 1.96/2.19 (![X47: $i, X49: $i, X50: $i, X48: $i] : (p39(X47, X50) | (~p39(f17(f19(f21(c47, X47), X48), X49), X50))) <=> ![X47: $i, X49: $i, X50: $i, X48: $i] : ((~p39(f17(f19(f21(c47, X47), X48), X49), X50)) | p39(X47, X50))),
% 1.96/2.19 inference(quant_intro,[status(thm)],[20])).
% 1.96/2.19 tff(22,axiom,(![X47: $i, X49: $i, X50: $i, X48: $i] : (p39(X47, X50) | (~p39(f17(f19(f21(c47, X47), X48), X49), X50)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','p39_44')).
% 1.96/2.19 tff(23,plain,
% 1.96/2.19 (![X47: $i, X49: $i, X50: $i, X48: $i] : ((~p39(f17(f19(f21(c47, X47), X48), X49), X50)) | p39(X47, X50))),
% 1.96/2.19 inference(modus_ponens,[status(thm)],[22, 21])).
% 1.96/2.19 tff(24,plain,
% 1.96/2.19 (![X47: $i, X49: $i, X50: $i, X48: $i] : ((~p39(f17(f19(f21(c47, X47), X48), X49), X50)) | p39(X47, X50))),
% 1.96/2.19 inference(modus_ponens,[status(thm)],[23, 19])).
% 1.96/2.19 tff(25,plain,(
% 1.96/2.19 ![X47: $i, X49: $i, X50: $i, X48: $i] : ((~p39(f17(f19(f21(c47, X47), X48), X49), X50)) | p39(X47, X50))),
% 1.96/2.19 inference(skolemize,[status(sab)],[24])).
% 1.96/2.19 tff(26,plain,
% 1.96/2.19 (![X47: $i, X49: $i, X50: $i, X48: $i] : ((~p39(f17(f19(f21(c47, X47), X48), X49), X50)) | p39(X47, X50))),
% 1.96/2.19 inference(modus_ponens,[status(thm)],[25, 18])).
% 1.96/2.19 tff(27,plain,
% 1.96/2.19 (((~![X47: $i, X49: $i, X50: $i, X48: $i] : ((~p39(f17(f19(f21(c47, X47), X48), X49), X50)) | p39(X47, X50))) | ((~p39(f17(f19(f21(c47, c43), c44), c45), c46)) | p39(c43, c46))) <=> ((~![X47: $i, X49: $i, X50: $i, X48: $i] : ((~p39(f17(f19(f21(c47, X47), X48), X49), X50)) | p39(X47, X50))) | (~p39(f17(f19(f21(c47, c43), c44), c45), c46)) | p39(c43, c46))),
% 1.96/2.19 inference(rewrite,[status(thm)],[])).
% 1.96/2.19 tff(28,plain,
% 1.96/2.19 ((~![X47: $i, X49: $i, X50: $i, X48: $i] : ((~p39(f17(f19(f21(c47, X47), X48), X49), X50)) | p39(X47, X50))) | ((~p39(f17(f19(f21(c47, c43), c44), c45), c46)) | p39(c43, c46))),
% 1.96/2.19 inference(quant_inst,[status(thm)],[])).
% 1.96/2.19 tff(29,plain,
% 1.96/2.19 ((~![X47: $i, X49: $i, X50: $i, X48: $i] : ((~p39(f17(f19(f21(c47, X47), X48), X49), X50)) | p39(X47, X50))) | (~p39(f17(f19(f21(c47, c43), c44), c45), c46)) | p39(c43, c46)),
% 1.96/2.19 inference(modus_ponens,[status(thm)],[28, 27])).
% 1.96/2.19 tff(30,plain,
% 1.96/2.19 ($false),
% 1.96/2.19 inference(unit_resolution,[status(thm)],[29, 26, 16, 2])).
% 1.96/2.19 tff(31,plain,(~p39(f17(f19(f21(c47, c43), c44), c45), c46)), inference(lemma,lemma(discharge,[]))).
% 1.96/2.19 tff(32,plain,
% 1.96/2.19 (^[X105: $i, X104: $i, X103: $i, X106: $i] : refl(((~p39(f5(c40, f10(f13(f15(c42, X103), X105), X106)), X104)) | p39(X103, X104)) <=> ((~p39(f5(c40, f10(f13(f15(c42, X103), X105), X106)), X104)) | p39(X103, X104)))),
% 1.96/2.19 inference(bind,[status(th)],[])).
% 1.96/2.19 tff(33,plain,
% 1.96/2.19 (![X105: $i, X104: $i, X103: $i, X106: $i] : ((~p39(f5(c40, f10(f13(f15(c42, X103), X105), X106)), X104)) | p39(X103, X104)) <=> ![X105: $i, X104: $i, X103: $i, X106: $i] : ((~p39(f5(c40, f10(f13(f15(c42, X103), X105), X106)), X104)) | p39(X103, X104))),
% 1.96/2.19 inference(quant_intro,[status(thm)],[32])).
% 1.96/2.19 tff(34,plain,
% 1.96/2.19 (![X105: $i, X104: $i, X103: $i, X106: $i] : ((~p39(f5(c40, f10(f13(f15(c42, X103), X105), X106)), X104)) | p39(X103, X104)) <=> ![X105: $i, X104: $i, X103: $i, X106: $i] : ((~p39(f5(c40, f10(f13(f15(c42, X103), X105), X106)), X104)) | p39(X103, X104))),
% 1.96/2.19 inference(rewrite,[status(thm)],[])).
% 1.96/2.19 tff(35,plain,
% 1.96/2.19 (^[X105: $i, X104: $i, X103: $i, X106: $i] : rewrite((p39(X103, X104) | (~p39(f5(c40, f10(f13(f15(c42, X103), X105), X106)), X104))) <=> ((~p39(f5(c40, f10(f13(f15(c42, X103), X105), X106)), X104)) | p39(X103, X104)))),
% 1.96/2.19 inference(bind,[status(th)],[])).
% 1.96/2.19 tff(36,plain,
% 1.96/2.19 (![X105: $i, X104: $i, X103: $i, X106: $i] : (p39(X103, X104) | (~p39(f5(c40, f10(f13(f15(c42, X103), X105), X106)), X104))) <=> ![X105: $i, X104: $i, X103: $i, X106: $i] : ((~p39(f5(c40, f10(f13(f15(c42, X103), X105), X106)), X104)) | p39(X103, X104))),
% 1.96/2.19 inference(quant_intro,[status(thm)],[35])).
% 1.96/2.19 tff(37,axiom,(![X105: $i, X104: $i, X103: $i, X106: $i] : (p39(X103, X104) | (~p39(f5(c40, f10(f13(f15(c42, X103), X105), X106)), X104)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','p39_63')).
% 1.96/2.19 tff(38,plain,
% 1.96/2.19 (![X105: $i, X104: $i, X103: $i, X106: $i] : ((~p39(f5(c40, f10(f13(f15(c42, X103), X105), X106)), X104)) | p39(X103, X104))),
% 1.96/2.19 inference(modus_ponens,[status(thm)],[37, 36])).
% 1.96/2.19 tff(39,plain,
% 1.96/2.19 (![X105: $i, X104: $i, X103: $i, X106: $i] : ((~p39(f5(c40, f10(f13(f15(c42, X103), X105), X106)), X104)) | p39(X103, X104))),
% 1.96/2.19 inference(modus_ponens,[status(thm)],[38, 34])).
% 1.96/2.19 tff(40,plain,(
% 1.96/2.19 ![X105: $i, X104: $i, X103: $i, X106: $i] : ((~p39(f5(c40, f10(f13(f15(c42, X103), X105), X106)), X104)) | p39(X103, X104))),
% 1.96/2.19 inference(skolemize,[status(sab)],[39])).
% 1.96/2.19 tff(41,plain,
% 1.96/2.19 (![X105: $i, X104: $i, X103: $i, X106: $i] : ((~p39(f5(c40, f10(f13(f15(c42, X103), X105), X106)), X104)) | p39(X103, X104))),
% 1.96/2.19 inference(modus_ponens,[status(thm)],[40, 33])).
% 1.96/2.19 tff(42,plain,
% 1.96/2.19 (((~![X105: $i, X104: $i, X103: $i, X106: $i] : ((~p39(f5(c40, f10(f13(f15(c42, X103), X105), X106)), X104)) | p39(X103, X104))) | ((~p39(f5(c40, f10(f13(f15(c42, f17(f19(f21(c47, c43), c44), c45)), f26(f28(f30(c48, c43), c44), c45)), f34(f36(f38(c49, c43), c44), c45))), c46)) | p39(f17(f19(f21(c47, c43), c44), c45), c46))) <=> ((~![X105: $i, X104: $i, X103: $i, X106: $i] : ((~p39(f5(c40, f10(f13(f15(c42, X103), X105), X106)), X104)) | p39(X103, X104))) | (~p39(f5(c40, f10(f13(f15(c42, f17(f19(f21(c47, c43), c44), c45)), f26(f28(f30(c48, c43), c44), c45)), f34(f36(f38(c49, c43), c44), c45))), c46)) | p39(f17(f19(f21(c47, c43), c44), c45), c46))),
% 1.96/2.19 inference(rewrite,[status(thm)],[])).
% 1.96/2.19 tff(43,plain,
% 1.96/2.19 ((~![X105: $i, X104: $i, X103: $i, X106: $i] : ((~p39(f5(c40, f10(f13(f15(c42, X103), X105), X106)), X104)) | p39(X103, X104))) | ((~p39(f5(c40, f10(f13(f15(c42, f17(f19(f21(c47, c43), c44), c45)), f26(f28(f30(c48, c43), c44), c45)), f34(f36(f38(c49, c43), c44), c45))), c46)) | p39(f17(f19(f21(c47, c43), c44), c45), c46))),
% 1.96/2.19 inference(quant_inst,[status(thm)],[])).
% 1.96/2.19 tff(44,plain,
% 1.96/2.19 ((~![X105: $i, X104: $i, X103: $i, X106: $i] : ((~p39(f5(c40, f10(f13(f15(c42, X103), X105), X106)), X104)) | p39(X103, X104))) | (~p39(f5(c40, f10(f13(f15(c42, f17(f19(f21(c47, c43), c44), c45)), f26(f28(f30(c48, c43), c44), c45)), f34(f36(f38(c49, c43), c44), c45))), c46)) | p39(f17(f19(f21(c47, c43), c44), c45), c46)),
% 1.96/2.19 inference(modus_ponens,[status(thm)],[43, 42])).
% 1.96/2.19 tff(45,plain,
% 1.96/2.19 ($false),
% 1.96/2.19 inference(unit_resolution,[status(thm)],[44, 41, 31, 1])).
% 1.96/2.19 tff(46,plain,(~p39(f5(c40, f10(f13(f15(c42, f17(f19(f21(c47, c43), c44), c45)), f26(f28(f30(c48, c43), c44), c45)), f34(f36(f38(c49, c43), c44), c45))), c46)), inference(lemma,lemma(discharge,[]))).
% 1.96/2.19 tff(47,assumption,(~p22(c46, c46)), introduced(assumption)).
% 1.96/2.19 tff(48,plain,
% 1.96/2.19 (^[X37: $i] : refl(p22(X37, X37) <=> p22(X37, X37))),
% 1.96/2.19 inference(bind,[status(th)],[])).
% 1.96/2.19 tff(49,plain,
% 1.96/2.19 (![X37: $i] : p22(X37, X37) <=> ![X37: $i] : p22(X37, X37)),
% 1.96/2.19 inference(quant_intro,[status(thm)],[48])).
% 1.96/2.19 tff(50,plain,
% 1.96/2.19 (![X37: $i] : p22(X37, X37) <=> ![X37: $i] : p22(X37, X37)),
% 1.96/2.19 inference(rewrite,[status(thm)],[])).
% 1.96/2.19 tff(51,axiom,(![X37: $i] : p22(X37, X37)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','p22_15')).
% 1.96/2.19 tff(52,plain,
% 1.96/2.19 (![X37: $i] : p22(X37, X37)),
% 1.96/2.19 inference(modus_ponens,[status(thm)],[51, 50])).
% 1.96/2.19 tff(53,plain,(
% 1.96/2.19 ![X37: $i] : p22(X37, X37)),
% 1.96/2.19 inference(skolemize,[status(sab)],[52])).
% 1.96/2.19 tff(54,plain,
% 1.96/2.19 (![X37: $i] : p22(X37, X37)),
% 1.96/2.19 inference(modus_ponens,[status(thm)],[53, 49])).
% 1.96/2.19 tff(55,plain,
% 1.96/2.19 ((~![X37: $i] : p22(X37, X37)) | p22(c46, c46)),
% 1.96/2.19 inference(quant_inst,[status(thm)],[])).
% 1.96/2.19 tff(56,plain,
% 1.96/2.19 ($false),
% 1.96/2.19 inference(unit_resolution,[status(thm)],[55, 54, 47])).
% 1.96/2.19 tff(57,plain,(p22(c46, c46)), inference(lemma,lemma(discharge,[]))).
% 1.96/2.19 tff(58,plain,
% 1.96/2.19 (^[X47: $i, X49: $i, X48: $i] : refl(p3(f7(c41, f10(f13(f15(c42, X47), X48), X49)), f10(f13(f15(c42, f17(f19(f21(c47, X47), X48), X49)), f26(f28(f30(c48, X47), X48), X49)), f34(f36(f38(c49, X47), X48), X49))) <=> p3(f7(c41, f10(f13(f15(c42, X47), X48), X49)), f10(f13(f15(c42, f17(f19(f21(c47, X47), X48), X49)), f26(f28(f30(c48, X47), X48), X49)), f34(f36(f38(c49, X47), X48), X49))))),
% 1.96/2.19 inference(bind,[status(th)],[])).
% 1.96/2.19 tff(59,plain,
% 1.96/2.19 (![X47: $i, X49: $i, X48: $i] : p3(f7(c41, f10(f13(f15(c42, X47), X48), X49)), f10(f13(f15(c42, f17(f19(f21(c47, X47), X48), X49)), f26(f28(f30(c48, X47), X48), X49)), f34(f36(f38(c49, X47), X48), X49))) <=> ![X47: $i, X49: $i, X48: $i] : p3(f7(c41, f10(f13(f15(c42, X47), X48), X49)), f10(f13(f15(c42, f17(f19(f21(c47, X47), X48), X49)), f26(f28(f30(c48, X47), X48), X49)), f34(f36(f38(c49, X47), X48), X49)))),
% 1.96/2.19 inference(quant_intro,[status(thm)],[58])).
% 1.96/2.19 tff(60,plain,
% 1.96/2.19 (![X47: $i, X49: $i, X48: $i] : p3(f7(c41, f10(f13(f15(c42, X47), X48), X49)), f10(f13(f15(c42, f17(f19(f21(c47, X47), X48), X49)), f26(f28(f30(c48, X47), X48), X49)), f34(f36(f38(c49, X47), X48), X49))) <=> ![X47: $i, X49: $i, X48: $i] : p3(f7(c41, f10(f13(f15(c42, X47), X48), X49)), f10(f13(f15(c42, f17(f19(f21(c47, X47), X48), X49)), f26(f28(f30(c48, X47), X48), X49)), f34(f36(f38(c49, X47), X48), X49)))),
% 1.96/2.19 inference(rewrite,[status(thm)],[])).
% 1.96/2.19 tff(61,axiom,(![X47: $i, X49: $i, X48: $i] : p3(f7(c41, f10(f13(f15(c42, X47), X48), X49)), f10(f13(f15(c42, f17(f19(f21(c47, X47), X48), X49)), f26(f28(f30(c48, X47), X48), X49)), f34(f36(f38(c49, X47), X48), X49)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','p3_67')).
% 1.96/2.19 tff(62,plain,
% 1.96/2.19 (![X47: $i, X49: $i, X48: $i] : p3(f7(c41, f10(f13(f15(c42, X47), X48), X49)), f10(f13(f15(c42, f17(f19(f21(c47, X47), X48), X49)), f26(f28(f30(c48, X47), X48), X49)), f34(f36(f38(c49, X47), X48), X49)))),
% 1.96/2.19 inference(modus_ponens,[status(thm)],[61, 60])).
% 1.96/2.19 tff(63,plain,(
% 1.96/2.19 ![X47: $i, X49: $i, X48: $i] : p3(f7(c41, f10(f13(f15(c42, X47), X48), X49)), f10(f13(f15(c42, f17(f19(f21(c47, X47), X48), X49)), f26(f28(f30(c48, X47), X48), X49)), f34(f36(f38(c49, X47), X48), X49)))),
% 1.96/2.19 inference(skolemize,[status(sab)],[62])).
% 1.96/2.19 tff(64,plain,
% 1.96/2.19 (![X47: $i, X49: $i, X48: $i] : p3(f7(c41, f10(f13(f15(c42, X47), X48), X49)), f10(f13(f15(c42, f17(f19(f21(c47, X47), X48), X49)), f26(f28(f30(c48, X47), X48), X49)), f34(f36(f38(c49, X47), X48), X49)))),
% 1.96/2.19 inference(modus_ponens,[status(thm)],[63, 59])).
% 1.96/2.19 tff(65,plain,
% 1.96/2.19 ((~![X47: $i, X49: $i, X48: $i] : p3(f7(c41, f10(f13(f15(c42, X47), X48), X49)), f10(f13(f15(c42, f17(f19(f21(c47, X47), X48), X49)), f26(f28(f30(c48, X47), X48), X49)), f34(f36(f38(c49, X47), X48), X49)))) | p3(f7(c41, f10(f13(f15(c42, c43), c44), c45)), f10(f13(f15(c42, f17(f19(f21(c47, c43), c44), c45)), f26(f28(f30(c48, c43), c44), c45)), f34(f36(f38(c49, c43), c44), c45)))),
% 1.96/2.19 inference(quant_inst,[status(thm)],[])).
% 1.96/2.19 tff(66,plain,
% 1.96/2.19 (p3(f7(c41, f10(f13(f15(c42, c43), c44), c45)), f10(f13(f15(c42, f17(f19(f21(c47, c43), c44), c45)), f26(f28(f30(c48, c43), c44), c45)), f34(f36(f38(c49, c43), c44), c45)))),
% 1.96/2.19 inference(unit_resolution,[status(thm)],[65, 64])).
% 1.96/2.19 tff(67,assumption,(~p2(c40, c40)), introduced(assumption)).
% 1.96/2.19 tff(68,plain,
% 1.96/2.19 (^[X31: $i] : refl(p2(X31, X31) <=> p2(X31, X31))),
% 1.96/2.19 inference(bind,[status(th)],[])).
% 1.96/2.19 tff(69,plain,
% 1.96/2.19 (![X31: $i] : p2(X31, X31) <=> ![X31: $i] : p2(X31, X31)),
% 1.96/2.19 inference(quant_intro,[status(thm)],[68])).
% 1.96/2.19 tff(70,plain,
% 1.96/2.19 (![X31: $i] : p2(X31, X31) <=> ![X31: $i] : p2(X31, X31)),
% 1.96/2.19 inference(rewrite,[status(thm)],[])).
% 1.96/2.19 tff(71,axiom,(![X31: $i] : p2(X31, X31)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','p2_17')).
% 1.96/2.19 tff(72,plain,
% 1.96/2.19 (![X31: $i] : p2(X31, X31)),
% 1.96/2.19 inference(modus_ponens,[status(thm)],[71, 70])).
% 1.96/2.19 tff(73,plain,(
% 1.96/2.19 ![X31: $i] : p2(X31, X31)),
% 1.96/2.19 inference(skolemize,[status(sab)],[72])).
% 1.96/2.19 tff(74,plain,
% 1.96/2.19 (![X31: $i] : p2(X31, X31)),
% 1.96/2.19 inference(modus_ponens,[status(thm)],[73, 69])).
% 1.96/2.19 tff(75,plain,
% 1.96/2.19 ((~![X31: $i] : p2(X31, X31)) | p2(c40, c40)),
% 1.96/2.19 inference(quant_inst,[status(thm)],[])).
% 1.96/2.19 tff(76,plain,
% 1.96/2.19 ($false),
% 1.96/2.19 inference(unit_resolution,[status(thm)],[75, 74, 67])).
% 1.96/2.19 tff(77,plain,(p2(c40, c40)), inference(lemma,lemma(discharge,[]))).
% 1.96/2.19 tff(78,plain,
% 1.96/2.19 (^[X118: $i, X119: $i, X121: $i, X120: $i] : refl(((~p3(X119, X121)) | (~p2(X118, X120)) | p4(f5(X118, X119), f5(X120, X121))) <=> ((~p3(X119, X121)) | (~p2(X118, X120)) | p4(f5(X118, X119), f5(X120, X121))))),
% 1.96/2.19 inference(bind,[status(th)],[])).
% 1.96/2.19 tff(79,plain,
% 1.96/2.19 (![X118: $i, X119: $i, X121: $i, X120: $i] : ((~p3(X119, X121)) | (~p2(X118, X120)) | p4(f5(X118, X119), f5(X120, X121))) <=> ![X118: $i, X119: $i, X121: $i, X120: $i] : ((~p3(X119, X121)) | (~p2(X118, X120)) | p4(f5(X118, X119), f5(X120, X121)))),
% 1.96/2.19 inference(quant_intro,[status(thm)],[78])).
% 1.96/2.19 tff(80,plain,
% 1.96/2.19 (![X118: $i, X119: $i, X121: $i, X120: $i] : ((~p3(X119, X121)) | (~p2(X118, X120)) | p4(f5(X118, X119), f5(X120, X121))) <=> ![X118: $i, X119: $i, X121: $i, X120: $i] : ((~p3(X119, X121)) | (~p2(X118, X120)) | p4(f5(X118, X119), f5(X120, X121)))),
% 1.96/2.19 inference(rewrite,[status(thm)],[])).
% 1.96/2.19 tff(81,plain,
% 1.96/2.19 (^[X118: $i, X119: $i, X121: $i, X120: $i] : trans(monotonicity(rewrite((p4(f5(X118, X119), f5(X120, X121)) | (~p2(X118, X120))) <=> ((~p2(X118, X120)) | p4(f5(X118, X119), f5(X120, X121)))), (((p4(f5(X118, X119), f5(X120, X121)) | (~p2(X118, X120))) | (~p3(X119, X121))) <=> (((~p2(X118, X120)) | p4(f5(X118, X119), f5(X120, X121))) | (~p3(X119, X121))))), rewrite((((~p2(X118, X120)) | p4(f5(X118, X119), f5(X120, X121))) | (~p3(X119, X121))) <=> ((~p3(X119, X121)) | (~p2(X118, X120)) | p4(f5(X118, X119), f5(X120, X121)))), (((p4(f5(X118, X119), f5(X120, X121)) | (~p2(X118, X120))) | (~p3(X119, X121))) <=> ((~p3(X119, X121)) | (~p2(X118, X120)) | p4(f5(X118, X119), f5(X120, X121)))))),
% 1.96/2.19 inference(bind,[status(th)],[])).
% 1.96/2.19 tff(82,plain,
% 1.96/2.19 (![X118: $i, X119: $i, X121: $i, X120: $i] : ((p4(f5(X118, X119), f5(X120, X121)) | (~p2(X118, X120))) | (~p3(X119, X121))) <=> ![X118: $i, X119: $i, X121: $i, X120: $i] : ((~p3(X119, X121)) | (~p2(X118, X120)) | p4(f5(X118, X119), f5(X120, X121)))),
% 1.96/2.19 inference(quant_intro,[status(thm)],[81])).
% 1.96/2.19 tff(83,axiom,(![X118: $i, X119: $i, X121: $i, X120: $i] : ((p4(f5(X118, X119), f5(X120, X121)) | (~p2(X118, X120))) | (~p3(X119, X121)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','p4_50')).
% 1.96/2.19 tff(84,plain,
% 1.96/2.19 (![X118: $i, X119: $i, X121: $i, X120: $i] : ((~p3(X119, X121)) | (~p2(X118, X120)) | p4(f5(X118, X119), f5(X120, X121)))),
% 1.96/2.19 inference(modus_ponens,[status(thm)],[83, 82])).
% 1.96/2.19 tff(85,plain,
% 1.96/2.19 (![X118: $i, X119: $i, X121: $i, X120: $i] : ((~p3(X119, X121)) | (~p2(X118, X120)) | p4(f5(X118, X119), f5(X120, X121)))),
% 1.96/2.19 inference(modus_ponens,[status(thm)],[84, 80])).
% 1.96/2.19 tff(86,plain,(
% 1.96/2.19 ![X118: $i, X119: $i, X121: $i, X120: $i] : ((~p3(X119, X121)) | (~p2(X118, X120)) | p4(f5(X118, X119), f5(X120, X121)))),
% 1.96/2.19 inference(skolemize,[status(sab)],[85])).
% 1.96/2.19 tff(87,plain,
% 1.96/2.19 (![X118: $i, X119: $i, X121: $i, X120: $i] : ((~p3(X119, X121)) | (~p2(X118, X120)) | p4(f5(X118, X119), f5(X120, X121)))),
% 1.96/2.19 inference(modus_ponens,[status(thm)],[86, 79])).
% 1.96/2.19 tff(88,plain,
% 1.96/2.19 (((~![X118: $i, X119: $i, X121: $i, X120: $i] : ((~p3(X119, X121)) | (~p2(X118, X120)) | p4(f5(X118, X119), f5(X120, X121)))) | ((~p2(c40, c40)) | (~p3(f7(c41, f10(f13(f15(c42, c43), c44), c45)), f10(f13(f15(c42, f17(f19(f21(c47, c43), c44), c45)), f26(f28(f30(c48, c43), c44), c45)), f34(f36(f38(c49, c43), c44), c45)))) | p4(f5(c40, f7(c41, f10(f13(f15(c42, c43), c44), c45))), f5(c40, f10(f13(f15(c42, f17(f19(f21(c47, c43), c44), c45)), f26(f28(f30(c48, c43), c44), c45)), f34(f36(f38(c49, c43), c44), c45)))))) <=> ((~![X118: $i, X119: $i, X121: $i, X120: $i] : ((~p3(X119, X121)) | (~p2(X118, X120)) | p4(f5(X118, X119), f5(X120, X121)))) | (~p2(c40, c40)) | (~p3(f7(c41, f10(f13(f15(c42, c43), c44), c45)), f10(f13(f15(c42, f17(f19(f21(c47, c43), c44), c45)), f26(f28(f30(c48, c43), c44), c45)), f34(f36(f38(c49, c43), c44), c45)))) | p4(f5(c40, f7(c41, f10(f13(f15(c42, c43), c44), c45))), f5(c40, f10(f13(f15(c42, f17(f19(f21(c47, c43), c44), c45)), f26(f28(f30(c48, c43), c44), c45)), f34(f36(f38(c49, c43), c44), c45)))))),
% 1.96/2.19 inference(rewrite,[status(thm)],[])).
% 1.96/2.19 tff(89,plain,
% 1.96/2.19 (((~p3(f7(c41, f10(f13(f15(c42, c43), c44), c45)), f10(f13(f15(c42, f17(f19(f21(c47, c43), c44), c45)), f26(f28(f30(c48, c43), c44), c45)), f34(f36(f38(c49, c43), c44), c45)))) | (~p2(c40, c40)) | p4(f5(c40, f7(c41, f10(f13(f15(c42, c43), c44), c45))), f5(c40, f10(f13(f15(c42, f17(f19(f21(c47, c43), c44), c45)), f26(f28(f30(c48, c43), c44), c45)), f34(f36(f38(c49, c43), c44), c45))))) <=> ((~p2(c40, c40)) | (~p3(f7(c41, f10(f13(f15(c42, c43), c44), c45)), f10(f13(f15(c42, f17(f19(f21(c47, c43), c44), c45)), f26(f28(f30(c48, c43), c44), c45)), f34(f36(f38(c49, c43), c44), c45)))) | p4(f5(c40, f7(c41, f10(f13(f15(c42, c43), c44), c45))), f5(c40, f10(f13(f15(c42, f17(f19(f21(c47, c43), c44), c45)), f26(f28(f30(c48, c43), c44), c45)), f34(f36(f38(c49, c43), c44), c45)))))),
% 1.96/2.19 inference(rewrite,[status(thm)],[])).
% 1.96/2.19 tff(90,plain,
% 1.96/2.19 (((~![X118: $i, X119: $i, X121: $i, X120: $i] : ((~p3(X119, X121)) | (~p2(X118, X120)) | p4(f5(X118, X119), f5(X120, X121)))) | ((~p3(f7(c41, f10(f13(f15(c42, c43), c44), c45)), f10(f13(f15(c42, f17(f19(f21(c47, c43), c44), c45)), f26(f28(f30(c48, c43), c44), c45)), f34(f36(f38(c49, c43), c44), c45)))) | (~p2(c40, c40)) | p4(f5(c40, f7(c41, f10(f13(f15(c42, c43), c44), c45))), f5(c40, f10(f13(f15(c42, f17(f19(f21(c47, c43), c44), c45)), f26(f28(f30(c48, c43), c44), c45)), f34(f36(f38(c49, c43), c44), c45)))))) <=> ((~![X118: $i, X119: $i, X121: $i, X120: $i] : ((~p3(X119, X121)) | (~p2(X118, X120)) | p4(f5(X118, X119), f5(X120, X121)))) | ((~p2(c40, c40)) | (~p3(f7(c41, f10(f13(f15(c42, c43), c44), c45)), f10(f13(f15(c42, f17(f19(f21(c47, c43), c44), c45)), f26(f28(f30(c48, c43), c44), c45)), f34(f36(f38(c49, c43), c44), c45)))) | p4(f5(c40, f7(c41, f10(f13(f15(c42, c43), c44), c45))), f5(c40, f10(f13(f15(c42, f17(f19(f21(c47, c43), c44), c45)), f26(f28(f30(c48, c43), c44), c45)), f34(f36(f38(c49, c43), c44), c45))))))),
% 1.96/2.19 inference(monotonicity,[status(thm)],[89])).
% 1.96/2.19 tff(91,plain,
% 1.96/2.19 (((~![X118: $i, X119: $i, X121: $i, X120: $i] : ((~p3(X119, X121)) | (~p2(X118, X120)) | p4(f5(X118, X119), f5(X120, X121)))) | ((~p3(f7(c41, f10(f13(f15(c42, c43), c44), c45)), f10(f13(f15(c42, f17(f19(f21(c47, c43), c44), c45)), f26(f28(f30(c48, c43), c44), c45)), f34(f36(f38(c49, c43), c44), c45)))) | (~p2(c40, c40)) | p4(f5(c40, f7(c41, f10(f13(f15(c42, c43), c44), c45))), f5(c40, f10(f13(f15(c42, f17(f19(f21(c47, c43), c44), c45)), f26(f28(f30(c48, c43), c44), c45)), f34(f36(f38(c49, c43), c44), c45)))))) <=> ((~![X118: $i, X119: $i, X121: $i, X120: $i] : ((~p3(X119, X121)) | (~p2(X118, X120)) | p4(f5(X118, X119), f5(X120, X121)))) | (~p2(c40, c40)) | (~p3(f7(c41, f10(f13(f15(c42, c43), c44), c45)), f10(f13(f15(c42, f17(f19(f21(c47, c43), c44), c45)), f26(f28(f30(c48, c43), c44), c45)), f34(f36(f38(c49, c43), c44), c45)))) | p4(f5(c40, f7(c41, f10(f13(f15(c42, c43), c44), c45))), f5(c40, f10(f13(f15(c42, f17(f19(f21(c47, c43), c44), c45)), f26(f28(f30(c48, c43), c44), c45)), f34(f36(f38(c49, c43), c44), c45)))))),
% 1.96/2.19 inference(transitivity,[status(thm)],[90, 88])).
% 1.96/2.19 tff(92,plain,
% 1.96/2.19 ((~![X118: $i, X119: $i, X121: $i, X120: $i] : ((~p3(X119, X121)) | (~p2(X118, X120)) | p4(f5(X118, X119), f5(X120, X121)))) | ((~p3(f7(c41, f10(f13(f15(c42, c43), c44), c45)), f10(f13(f15(c42, f17(f19(f21(c47, c43), c44), c45)), f26(f28(f30(c48, c43), c44), c45)), f34(f36(f38(c49, c43), c44), c45)))) | (~p2(c40, c40)) | p4(f5(c40, f7(c41, f10(f13(f15(c42, c43), c44), c45))), f5(c40, f10(f13(f15(c42, f17(f19(f21(c47, c43), c44), c45)), f26(f28(f30(c48, c43), c44), c45)), f34(f36(f38(c49, c43), c44), c45)))))),
% 1.96/2.19 inference(quant_inst,[status(thm)],[])).
% 1.96/2.19 tff(93,plain,
% 1.96/2.19 ((~![X118: $i, X119: $i, X121: $i, X120: $i] : ((~p3(X119, X121)) | (~p2(X118, X120)) | p4(f5(X118, X119), f5(X120, X121)))) | (~p2(c40, c40)) | (~p3(f7(c41, f10(f13(f15(c42, c43), c44), c45)), f10(f13(f15(c42, f17(f19(f21(c47, c43), c44), c45)), f26(f28(f30(c48, c43), c44), c45)), f34(f36(f38(c49, c43), c44), c45)))) | p4(f5(c40, f7(c41, f10(f13(f15(c42, c43), c44), c45))), f5(c40, f10(f13(f15(c42, f17(f19(f21(c47, c43), c44), c45)), f26(f28(f30(c48, c43), c44), c45)), f34(f36(f38(c49, c43), c44), c45))))),
% 1.96/2.19 inference(modus_ponens,[status(thm)],[92, 91])).
% 1.96/2.19 tff(94,plain,
% 1.96/2.19 (p4(f5(c40, f7(c41, f10(f13(f15(c42, c43), c44), c45))), f5(c40, f10(f13(f15(c42, f17(f19(f21(c47, c43), c44), c45)), f26(f28(f30(c48, c43), c44), c45)), f34(f36(f38(c49, c43), c44), c45))))),
% 1.96/2.19 inference(unit_resolution,[status(thm)],[93, 87, 77, 66])).
% 1.96/2.19 tff(95,plain,
% 1.96/2.19 (p39(f5(c40, f7(c41, f10(f13(f15(c42, c43), c44), c45))), c46) <=> p39(f5(c40, f7(c41, f10(f13(f15(c42, c43), c44), c45))), c46)),
% 1.96/2.19 inference(rewrite,[status(thm)],[])).
% 1.96/2.19 tff(96,axiom,(p39(f5(c40, f7(c41, f10(f13(f15(c42, c43), c44), c45))), c46)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','p39_46')).
% 1.96/2.19 tff(97,plain,
% 1.96/2.19 (p39(f5(c40, f7(c41, f10(f13(f15(c42, c43), c44), c45))), c46)),
% 1.96/2.19 inference(modus_ponens,[status(thm)],[96, 95])).
% 1.96/2.19 tff(98,plain,
% 1.96/2.19 (^[X110: $i, X107: $i, X109: $i, X108: $i] : refl(((~p22(X109, X108)) | (~p4(X110, X107)) | (~p39(X110, X109)) | p39(X107, X108)) <=> ((~p22(X109, X108)) | (~p4(X110, X107)) | (~p39(X110, X109)) | p39(X107, X108)))),
% 1.96/2.19 inference(bind,[status(th)],[])).
% 1.96/2.19 tff(99,plain,
% 1.96/2.19 (![X110: $i, X107: $i, X109: $i, X108: $i] : ((~p22(X109, X108)) | (~p4(X110, X107)) | (~p39(X110, X109)) | p39(X107, X108)) <=> ![X110: $i, X107: $i, X109: $i, X108: $i] : ((~p22(X109, X108)) | (~p4(X110, X107)) | (~p39(X110, X109)) | p39(X107, X108))),
% 1.96/2.19 inference(quant_intro,[status(thm)],[98])).
% 1.96/2.19 tff(100,plain,
% 1.96/2.19 (![X110: $i, X107: $i, X109: $i, X108: $i] : ((~p22(X109, X108)) | (~p4(X110, X107)) | (~p39(X110, X109)) | p39(X107, X108)) <=> ![X110: $i, X107: $i, X109: $i, X108: $i] : ((~p22(X109, X108)) | (~p4(X110, X107)) | (~p39(X110, X109)) | p39(X107, X108))),
% 1.96/2.19 inference(rewrite,[status(thm)],[])).
% 1.96/2.19 tff(101,plain,
% 1.96/2.19 (^[X110: $i, X107: $i, X109: $i, X108: $i] : trans(monotonicity(trans(monotonicity(rewrite((p39(X107, X108) | (~p39(X110, X109))) <=> ((~p39(X110, X109)) | p39(X107, X108))), (((p39(X107, X108) | (~p39(X110, X109))) | (~p4(X110, X107))) <=> (((~p39(X110, X109)) | p39(X107, X108)) | (~p4(X110, X107))))), rewrite((((~p39(X110, X109)) | p39(X107, X108)) | (~p4(X110, X107))) <=> ((~p4(X110, X107)) | (~p39(X110, X109)) | p39(X107, X108))), (((p39(X107, X108) | (~p39(X110, X109))) | (~p4(X110, X107))) <=> ((~p4(X110, X107)) | (~p39(X110, X109)) | p39(X107, X108)))), ((((p39(X107, X108) | (~p39(X110, X109))) | (~p4(X110, X107))) | (~p22(X109, X108))) <=> (((~p4(X110, X107)) | (~p39(X110, X109)) | p39(X107, X108)) | (~p22(X109, X108))))), rewrite((((~p4(X110, X107)) | (~p39(X110, X109)) | p39(X107, X108)) | (~p22(X109, X108))) <=> ((~p22(X109, X108)) | (~p4(X110, X107)) | (~p39(X110, X109)) | p39(X107, X108))), ((((p39(X107, X108) | (~p39(X110, X109))) | (~p4(X110, X107))) | (~p22(X109, X108))) <=> ((~p22(X109, X108)) | (~p4(X110, X107)) | (~p39(X110, X109)) | p39(X107, X108))))),
% 1.96/2.20 inference(bind,[status(th)],[])).
% 1.96/2.20 tff(102,plain,
% 1.96/2.20 (![X110: $i, X107: $i, X109: $i, X108: $i] : (((p39(X107, X108) | (~p39(X110, X109))) | (~p4(X110, X107))) | (~p22(X109, X108))) <=> ![X110: $i, X107: $i, X109: $i, X108: $i] : ((~p22(X109, X108)) | (~p4(X110, X107)) | (~p39(X110, X109)) | p39(X107, X108))),
% 1.96/2.20 inference(quant_intro,[status(thm)],[101])).
% 1.96/2.20 tff(103,axiom,(![X110: $i, X107: $i, X109: $i, X108: $i] : (((p39(X107, X108) | (~p39(X110, X109))) | (~p4(X110, X107))) | (~p22(X109, X108)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','p39_45')).
% 1.96/2.20 tff(104,plain,
% 1.96/2.20 (![X110: $i, X107: $i, X109: $i, X108: $i] : ((~p22(X109, X108)) | (~p4(X110, X107)) | (~p39(X110, X109)) | p39(X107, X108))),
% 1.96/2.20 inference(modus_ponens,[status(thm)],[103, 102])).
% 1.96/2.20 tff(105,plain,
% 1.96/2.20 (![X110: $i, X107: $i, X109: $i, X108: $i] : ((~p22(X109, X108)) | (~p4(X110, X107)) | (~p39(X110, X109)) | p39(X107, X108))),
% 1.96/2.20 inference(modus_ponens,[status(thm)],[104, 100])).
% 1.96/2.20 tff(106,plain,(
% 1.96/2.20 ![X110: $i, X107: $i, X109: $i, X108: $i] : ((~p22(X109, X108)) | (~p4(X110, X107)) | (~p39(X110, X109)) | p39(X107, X108))),
% 1.96/2.20 inference(skolemize,[status(sab)],[105])).
% 1.96/2.20 tff(107,plain,
% 1.96/2.20 (![X110: $i, X107: $i, X109: $i, X108: $i] : ((~p22(X109, X108)) | (~p4(X110, X107)) | (~p39(X110, X109)) | p39(X107, X108))),
% 1.96/2.20 inference(modus_ponens,[status(thm)],[106, 99])).
% 1.96/2.20 tff(108,plain,
% 1.96/2.20 (((~![X110: $i, X107: $i, X109: $i, X108: $i] : ((~p22(X109, X108)) | (~p4(X110, X107)) | (~p39(X110, X109)) | p39(X107, X108))) | ((~p39(f5(c40, f7(c41, f10(f13(f15(c42, c43), c44), c45))), c46)) | (~p4(f5(c40, f7(c41, f10(f13(f15(c42, c43), c44), c45))), f5(c40, f10(f13(f15(c42, f17(f19(f21(c47, c43), c44), c45)), f26(f28(f30(c48, c43), c44), c45)), f34(f36(f38(c49, c43), c44), c45))))) | (~p22(c46, c46)) | p39(f5(c40, f10(f13(f15(c42, f17(f19(f21(c47, c43), c44), c45)), f26(f28(f30(c48, c43), c44), c45)), f34(f36(f38(c49, c43), c44), c45))), c46))) <=> ((~![X110: $i, X107: $i, X109: $i, X108: $i] : ((~p22(X109, X108)) | (~p4(X110, X107)) | (~p39(X110, X109)) | p39(X107, X108))) | (~p39(f5(c40, f7(c41, f10(f13(f15(c42, c43), c44), c45))), c46)) | (~p4(f5(c40, f7(c41, f10(f13(f15(c42, c43), c44), c45))), f5(c40, f10(f13(f15(c42, f17(f19(f21(c47, c43), c44), c45)), f26(f28(f30(c48, c43), c44), c45)), f34(f36(f38(c49, c43), c44), c45))))) | (~p22(c46, c46)) | p39(f5(c40, f10(f13(f15(c42, f17(f19(f21(c47, c43), c44), c45)), f26(f28(f30(c48, c43), c44), c45)), f34(f36(f38(c49, c43), c44), c45))), c46))),
% 1.96/2.20 inference(rewrite,[status(thm)],[])).
% 1.96/2.20 tff(109,plain,
% 1.96/2.20 (((~p22(c46, c46)) | (~p4(f5(c40, f7(c41, f10(f13(f15(c42, c43), c44), c45))), f5(c40, f10(f13(f15(c42, f17(f19(f21(c47, c43), c44), c45)), f26(f28(f30(c48, c43), c44), c45)), f34(f36(f38(c49, c43), c44), c45))))) | (~p39(f5(c40, f7(c41, f10(f13(f15(c42, c43), c44), c45))), c46)) | p39(f5(c40, f10(f13(f15(c42, f17(f19(f21(c47, c43), c44), c45)), f26(f28(f30(c48, c43), c44), c45)), f34(f36(f38(c49, c43), c44), c45))), c46)) <=> ((~p39(f5(c40, f7(c41, f10(f13(f15(c42, c43), c44), c45))), c46)) | (~p4(f5(c40, f7(c41, f10(f13(f15(c42, c43), c44), c45))), f5(c40, f10(f13(f15(c42, f17(f19(f21(c47, c43), c44), c45)), f26(f28(f30(c48, c43), c44), c45)), f34(f36(f38(c49, c43), c44), c45))))) | (~p22(c46, c46)) | p39(f5(c40, f10(f13(f15(c42, f17(f19(f21(c47, c43), c44), c45)), f26(f28(f30(c48, c43), c44), c45)), f34(f36(f38(c49, c43), c44), c45))), c46))),
% 1.96/2.20 inference(rewrite,[status(thm)],[])).
% 1.96/2.20 tff(110,plain,
% 1.96/2.20 (((~![X110: $i, X107: $i, X109: $i, X108: $i] : ((~p22(X109, X108)) | (~p4(X110, X107)) | (~p39(X110, X109)) | p39(X107, X108))) | ((~p22(c46, c46)) | (~p4(f5(c40, f7(c41, f10(f13(f15(c42, c43), c44), c45))), f5(c40, f10(f13(f15(c42, f17(f19(f21(c47, c43), c44), c45)), f26(f28(f30(c48, c43), c44), c45)), f34(f36(f38(c49, c43), c44), c45))))) | (~p39(f5(c40, f7(c41, f10(f13(f15(c42, c43), c44), c45))), c46)) | p39(f5(c40, f10(f13(f15(c42, f17(f19(f21(c47, c43), c44), c45)), f26(f28(f30(c48, c43), c44), c45)), f34(f36(f38(c49, c43), c44), c45))), c46))) <=> ((~![X110: $i, X107: $i, X109: $i, X108: $i] : ((~p22(X109, X108)) | (~p4(X110, X107)) | (~p39(X110, X109)) | p39(X107, X108))) | ((~p39(f5(c40, f7(c41, f10(f13(f15(c42, c43), c44), c45))), c46)) | (~p4(f5(c40, f7(c41, f10(f13(f15(c42, c43), c44), c45))), f5(c40, f10(f13(f15(c42, f17(f19(f21(c47, c43), c44), c45)), f26(f28(f30(c48, c43), c44), c45)), f34(f36(f38(c49, c43), c44), c45))))) | (~p22(c46, c46)) | p39(f5(c40, f10(f13(f15(c42, f17(f19(f21(c47, c43), c44), c45)), f26(f28(f30(c48, c43), c44), c45)), f34(f36(f38(c49, c43), c44), c45))), c46)))),
% 1.96/2.20 inference(monotonicity,[status(thm)],[109])).
% 1.96/2.20 tff(111,plain,
% 1.96/2.20 (((~![X110: $i, X107: $i, X109: $i, X108: $i] : ((~p22(X109, X108)) | (~p4(X110, X107)) | (~p39(X110, X109)) | p39(X107, X108))) | ((~p22(c46, c46)) | (~p4(f5(c40, f7(c41, f10(f13(f15(c42, c43), c44), c45))), f5(c40, f10(f13(f15(c42, f17(f19(f21(c47, c43), c44), c45)), f26(f28(f30(c48, c43), c44), c45)), f34(f36(f38(c49, c43), c44), c45))))) | (~p39(f5(c40, f7(c41, f10(f13(f15(c42, c43), c44), c45))), c46)) | p39(f5(c40, f10(f13(f15(c42, f17(f19(f21(c47, c43), c44), c45)), f26(f28(f30(c48, c43), c44), c45)), f34(f36(f38(c49, c43), c44), c45))), c46))) <=> ((~![X110: $i, X107: $i, X109: $i, X108: $i] : ((~p22(X109, X108)) | (~p4(X110, X107)) | (~p39(X110, X109)) | p39(X107, X108))) | (~p39(f5(c40, f7(c41, f10(f13(f15(c42, c43), c44), c45))), c46)) | (~p4(f5(c40, f7(c41, f10(f13(f15(c42, c43), c44), c45))), f5(c40, f10(f13(f15(c42, f17(f19(f21(c47, c43), c44), c45)), f26(f28(f30(c48, c43), c44), c45)), f34(f36(f38(c49, c43), c44), c45))))) | (~p22(c46, c46)) | p39(f5(c40, f10(f13(f15(c42, f17(f19(f21(c47, c43), c44), c45)), f26(f28(f30(c48, c43), c44), c45)), f34(f36(f38(c49, c43), c44), c45))), c46))),
% 1.96/2.20 inference(transitivity,[status(thm)],[110, 108])).
% 1.96/2.20 tff(112,plain,
% 1.96/2.20 ((~![X110: $i, X107: $i, X109: $i, X108: $i] : ((~p22(X109, X108)) | (~p4(X110, X107)) | (~p39(X110, X109)) | p39(X107, X108))) | ((~p22(c46, c46)) | (~p4(f5(c40, f7(c41, f10(f13(f15(c42, c43), c44), c45))), f5(c40, f10(f13(f15(c42, f17(f19(f21(c47, c43), c44), c45)), f26(f28(f30(c48, c43), c44), c45)), f34(f36(f38(c49, c43), c44), c45))))) | (~p39(f5(c40, f7(c41, f10(f13(f15(c42, c43), c44), c45))), c46)) | p39(f5(c40, f10(f13(f15(c42, f17(f19(f21(c47, c43), c44), c45)), f26(f28(f30(c48, c43), c44), c45)), f34(f36(f38(c49, c43), c44), c45))), c46))),
% 1.96/2.20 inference(quant_inst,[status(thm)],[])).
% 1.96/2.20 tff(113,plain,
% 1.96/2.20 ((~![X110: $i, X107: $i, X109: $i, X108: $i] : ((~p22(X109, X108)) | (~p4(X110, X107)) | (~p39(X110, X109)) | p39(X107, X108))) | (~p39(f5(c40, f7(c41, f10(f13(f15(c42, c43), c44), c45))), c46)) | (~p4(f5(c40, f7(c41, f10(f13(f15(c42, c43), c44), c45))), f5(c40, f10(f13(f15(c42, f17(f19(f21(c47, c43), c44), c45)), f26(f28(f30(c48, c43), c44), c45)), f34(f36(f38(c49, c43), c44), c45))))) | (~p22(c46, c46)) | p39(f5(c40, f10(f13(f15(c42, f17(f19(f21(c47, c43), c44), c45)), f26(f28(f30(c48, c43), c44), c45)), f34(f36(f38(c49, c43), c44), c45))), c46)),
% 1.96/2.20 inference(modus_ponens,[status(thm)],[112, 111])).
% 1.96/2.20 tff(114,plain,
% 1.96/2.20 ($false),
% 1.96/2.20 inference(unit_resolution,[status(thm)],[113, 107, 97, 94, 57, 46])).
% 1.96/2.20 % SZS output end Proof
% 1.96/2.21 % E exiting
%------------------------------------------------------------------------------