%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : SYN703-1 : TPTP v9.0.0. Released v2.5.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n013.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:52 AM UTC 2025
% Result : Unsatisfiable 0.20s 0.49s
% Output : Proof 0.20s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SYN703-1 : TPTP v9.0.0. Released v2.5.0.
% 0.03/0.12 % Command : run_E %s %d THM
% 0.12/0.34 % Computer : n013.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 12:40:53 EDT 2025
% 0.12/0.34 % CPUTime :
% 0.20/0.49 % SZS status Unsatisfiable
% 0.20/0.49 % SZS output start Proof
% 0.20/0.49 tff(p47_type, type, (
% 0.20/0.49 p47: ( $i * $i ) > $o)).
% 0.20/0.49 tff(c53_type, type, (
% 0.20/0.49 c53: $i)).
% 0.20/0.49 tff(f20_type, type, (
% 0.20/0.49 f20: ( $i * $i ) > $i)).
% 0.20/0.49 tff(c55_type, type, (
% 0.20/0.49 c55: $i)).
% 0.20/0.49 tff(f22_type, type, (
% 0.20/0.49 f22: ( $i * $i ) > $i)).
% 0.20/0.49 tff(c52_type, type, (
% 0.20/0.49 c52: $i)).
% 0.20/0.49 tff(f24_type, type, (
% 0.20/0.49 f24: ( $i * $i ) > $i)).
% 0.20/0.49 tff(c51_type, type, (
% 0.20/0.49 c51: $i)).
% 0.20/0.49 tff(f26_type, type, (
% 0.20/0.49 f26: ( $i * $i ) > $i)).
% 0.20/0.49 tff(c50_type, type, (
% 0.20/0.49 c50: $i)).
% 0.20/0.49 tff(c56_type, type, (
% 0.20/0.49 c56: $i)).
% 0.20/0.49 tff(f5_type, type, (
% 0.20/0.49 f5: ( $i * $i ) > $i)).
% 0.20/0.49 tff(f8_type, type, (
% 0.20/0.49 f8: ( $i * $i ) > $i)).
% 0.20/0.49 tff(f40_type, type, (
% 0.20/0.49 f40: ( $i * $i ) > $i)).
% 0.20/0.49 tff(f42_type, type, (
% 0.20/0.49 f42: ( $i * $i ) > $i)).
% 0.20/0.49 tff(f44_type, type, (
% 0.20/0.49 f44: ( $i * $i ) > $i)).
% 0.20/0.49 tff(f46_type, type, (
% 0.20/0.49 f46: ( $i * $i ) > $i)).
% 0.20/0.49 tff(c58_type, type, (
% 0.20/0.49 c58: $i)).
% 0.20/0.49 tff(f11_type, type, (
% 0.20/0.49 f11: ( $i * $i ) > $i)).
% 0.20/0.49 tff(f30_type, type, (
% 0.20/0.49 f30: ( $i * $i ) > $i)).
% 0.20/0.49 tff(f32_type, type, (
% 0.20/0.49 f32: ( $i * $i ) > $i)).
% 0.20/0.49 tff(f34_type, type, (
% 0.20/0.49 f34: ( $i * $i ) > $i)).
% 0.20/0.49 tff(f36_type, type, (
% 0.20/0.49 f36: ( $i * $i ) > $i)).
% 0.20/0.49 tff(c57_type, type, (
% 0.20/0.49 c57: $i)).
% 0.20/0.49 tff(f13_type, type, (
% 0.20/0.49 f13: ( $i * $i ) > $i)).
% 0.20/0.49 tff(c49_type, type, (
% 0.20/0.49 c49: $i)).
% 0.20/0.49 tff(c48_type, type, (
% 0.20/0.49 c48: $i)).
% 0.20/0.49 tff(p15_type, type, (
% 0.20/0.49 p15: ( $i * $i ) > $o)).
% 0.20/0.49 tff(p4_type, type, (
% 0.20/0.49 p4: ( $i * $i ) > $o)).
% 0.20/0.49 tff(f16_type, type, (
% 0.20/0.49 f16: ( $i * $i ) > $i)).
% 0.20/0.49 tff(f18_type, type, (
% 0.20/0.49 f18: ( $i * $i ) > $i)).
% 0.20/0.49 tff(c54_type, type, (
% 0.20/0.49 c54: $i)).
% 0.20/0.49 tff(p3_type, type, (
% 0.20/0.49 p3: ( $i * $i ) > $o)).
% 0.20/0.49 tff(p2_type, type, (
% 0.20/0.49 p2: ( $i * $i ) > $o)).
% 0.20/0.49 tff(1,assumption,(~p15(c53, c53)), introduced(assumption)).
% 0.20/0.49 tff(2,plain,
% 0.20/0.49 (^[X17: $i] : refl(p15(X17, X17) <=> p15(X17, X17))),
% 0.20/0.49 inference(bind,[status(th)],[])).
% 0.20/0.49 tff(3,plain,
% 0.20/0.49 (![X17: $i] : p15(X17, X17) <=> ![X17: $i] : p15(X17, X17)),
% 0.20/0.49 inference(quant_intro,[status(thm)],[2])).
% 0.20/0.49 tff(4,plain,
% 0.20/0.49 (![X17: $i] : p15(X17, X17) <=> ![X17: $i] : p15(X17, X17)),
% 0.20/0.49 inference(rewrite,[status(thm)],[])).
% 0.20/0.49 tff(5,axiom,(![X17: $i] : p15(X17, X17)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','p15_5')).
% 0.20/0.49 tff(6,plain,
% 0.20/0.49 (![X17: $i] : p15(X17, X17)),
% 0.20/0.49 inference(modus_ponens,[status(thm)],[5, 4])).
% 0.20/0.49 tff(7,plain,(
% 0.20/0.49 ![X17: $i] : p15(X17, X17)),
% 0.20/0.49 inference(skolemize,[status(sab)],[6])).
% 0.20/0.49 tff(8,plain,
% 0.20/0.49 (![X17: $i] : p15(X17, X17)),
% 0.20/0.49 inference(modus_ponens,[status(thm)],[7, 3])).
% 0.20/0.49 tff(9,plain,
% 0.20/0.49 ((~![X17: $i] : p15(X17, X17)) | p15(c53, c53)),
% 0.20/0.49 inference(quant_inst,[status(thm)],[])).
% 0.20/0.49 tff(10,plain,
% 0.20/0.49 ($false),
% 0.20/0.49 inference(unit_resolution,[status(thm)],[9, 8, 1])).
% 0.20/0.49 tff(11,plain,(p15(c53, c53)), inference(lemma,lemma(discharge,[]))).
% 0.20/0.49 tff(12,plain,
% 0.20/0.49 (^[X57: $i, X59: $i, X60: $i, X58: $i] : refl(p3(f16(f18(c54, f8(f11(f13(c49, X57), X58), X59)), X60), f8(f11(f13(c49, f20(f22(f24(f26(c56, X57), X58), X59), X60)), f30(f32(f34(f36(c57, X57), X58), X59), X60)), f40(f42(f44(f46(c58, X57), X58), X59), X60))) <=> p3(f16(f18(c54, f8(f11(f13(c49, X57), X58), X59)), X60), f8(f11(f13(c49, f20(f22(f24(f26(c56, X57), X58), X59), X60)), f30(f32(f34(f36(c57, X57), X58), X59), X60)), f40(f42(f44(f46(c58, X57), X58), X59), X60))))),
% 0.20/0.49 inference(bind,[status(th)],[])).
% 0.20/0.49 tff(13,plain,
% 0.20/0.49 (![X57: $i, X59: $i, X60: $i, X58: $i] : p3(f16(f18(c54, f8(f11(f13(c49, X57), X58), X59)), X60), f8(f11(f13(c49, f20(f22(f24(f26(c56, X57), X58), X59), X60)), f30(f32(f34(f36(c57, X57), X58), X59), X60)), f40(f42(f44(f46(c58, X57), X58), X59), X60))) <=> ![X57: $i, X59: $i, X60: $i, X58: $i] : p3(f16(f18(c54, f8(f11(f13(c49, X57), X58), X59)), X60), f8(f11(f13(c49, f20(f22(f24(f26(c56, X57), X58), X59), X60)), f30(f32(f34(f36(c57, X57), X58), X59), X60)), f40(f42(f44(f46(c58, X57), X58), X59), X60)))),
% 0.20/0.49 inference(quant_intro,[status(thm)],[12])).
% 0.20/0.49 tff(14,plain,
% 0.20/0.49 (![X57: $i, X59: $i, X60: $i, X58: $i] : p3(f16(f18(c54, f8(f11(f13(c49, X57), X58), X59)), X60), f8(f11(f13(c49, f20(f22(f24(f26(c56, X57), X58), X59), X60)), f30(f32(f34(f36(c57, X57), X58), X59), X60)), f40(f42(f44(f46(c58, X57), X58), X59), X60))) <=> ![X57: $i, X59: $i, X60: $i, X58: $i] : p3(f16(f18(c54, f8(f11(f13(c49, X57), X58), X59)), X60), f8(f11(f13(c49, f20(f22(f24(f26(c56, X57), X58), X59), X60)), f30(f32(f34(f36(c57, X57), X58), X59), X60)), f40(f42(f44(f46(c58, X57), X58), X59), X60)))),
% 0.20/0.49 inference(rewrite,[status(thm)],[])).
% 0.20/0.49 tff(15,axiom,(![X57: $i, X59: $i, X60: $i, X58: $i] : p3(f16(f18(c54, f8(f11(f13(c49, X57), X58), X59)), X60), f8(f11(f13(c49, f20(f22(f24(f26(c56, X57), X58), X59), X60)), f30(f32(f34(f36(c57, X57), X58), X59), X60)), f40(f42(f44(f46(c58, X57), X58), X59), X60)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','p3_80')).
% 0.20/0.49 tff(16,plain,
% 0.20/0.49 (![X57: $i, X59: $i, X60: $i, X58: $i] : p3(f16(f18(c54, f8(f11(f13(c49, X57), X58), X59)), X60), f8(f11(f13(c49, f20(f22(f24(f26(c56, X57), X58), X59), X60)), f30(f32(f34(f36(c57, X57), X58), X59), X60)), f40(f42(f44(f46(c58, X57), X58), X59), X60)))),
% 0.20/0.49 inference(modus_ponens,[status(thm)],[15, 14])).
% 0.20/0.49 tff(17,plain,(
% 0.20/0.49 ![X57: $i, X59: $i, X60: $i, X58: $i] : p3(f16(f18(c54, f8(f11(f13(c49, X57), X58), X59)), X60), f8(f11(f13(c49, f20(f22(f24(f26(c56, X57), X58), X59), X60)), f30(f32(f34(f36(c57, X57), X58), X59), X60)), f40(f42(f44(f46(c58, X57), X58), X59), X60)))),
% 0.20/0.49 inference(skolemize,[status(sab)],[16])).
% 0.20/0.49 tff(18,plain,
% 0.20/0.49 (![X57: $i, X59: $i, X60: $i, X58: $i] : p3(f16(f18(c54, f8(f11(f13(c49, X57), X58), X59)), X60), f8(f11(f13(c49, f20(f22(f24(f26(c56, X57), X58), X59), X60)), f30(f32(f34(f36(c57, X57), X58), X59), X60)), f40(f42(f44(f46(c58, X57), X58), X59), X60)))),
% 0.20/0.49 inference(modus_ponens,[status(thm)],[17, 13])).
% 0.20/0.49 tff(19,plain,
% 0.20/0.49 ((~![X57: $i, X59: $i, X60: $i, X58: $i] : p3(f16(f18(c54, f8(f11(f13(c49, X57), X58), X59)), X60), f8(f11(f13(c49, f20(f22(f24(f26(c56, X57), X58), X59), X60)), f30(f32(f34(f36(c57, X57), X58), X59), X60)), f40(f42(f44(f46(c58, X57), X58), X59), X60)))) | p3(f16(f18(c54, f8(f11(f13(c49, c50), c51), c52)), c55), f8(f11(f13(c49, f20(f22(f24(f26(c56, c50), c51), c52), c55)), f30(f32(f34(f36(c57, c50), c51), c52), c55)), f40(f42(f44(f46(c58, c50), c51), c52), c55)))),
% 0.20/0.49 inference(quant_inst,[status(thm)],[])).
% 0.20/0.49 tff(20,plain,
% 0.20/0.49 (p3(f16(f18(c54, f8(f11(f13(c49, c50), c51), c52)), c55), f8(f11(f13(c49, f20(f22(f24(f26(c56, c50), c51), c52), c55)), f30(f32(f34(f36(c57, c50), c51), c52), c55)), f40(f42(f44(f46(c58, c50), c51), c52), c55)))),
% 0.20/0.49 inference(unit_resolution,[status(thm)],[19, 18])).
% 0.20/0.49 tff(21,assumption,(~p2(c48, c48)), introduced(assumption)).
% 0.20/0.49 tff(22,plain,
% 0.20/0.49 (^[X30: $i] : refl(p2(X30, X30) <=> p2(X30, X30))),
% 0.20/0.49 inference(bind,[status(th)],[])).
% 0.20/0.49 tff(23,plain,
% 0.20/0.49 (![X30: $i] : p2(X30, X30) <=> ![X30: $i] : p2(X30, X30)),
% 0.20/0.49 inference(quant_intro,[status(thm)],[22])).
% 0.20/0.49 tff(24,plain,
% 0.20/0.49 (![X30: $i] : p2(X30, X30) <=> ![X30: $i] : p2(X30, X30)),
% 0.20/0.49 inference(rewrite,[status(thm)],[])).
% 0.20/0.49 tff(25,axiom,(![X30: $i] : p2(X30, X30)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','p2_8')).
% 0.20/0.49 tff(26,plain,
% 0.20/0.49 (![X30: $i] : p2(X30, X30)),
% 0.20/0.49 inference(modus_ponens,[status(thm)],[25, 24])).
% 0.20/0.49 tff(27,plain,(
% 0.20/0.49 ![X30: $i] : p2(X30, X30)),
% 0.20/0.49 inference(skolemize,[status(sab)],[26])).
% 0.20/0.49 tff(28,plain,
% 0.20/0.49 (![X30: $i] : p2(X30, X30)),
% 0.20/0.49 inference(modus_ponens,[status(thm)],[27, 23])).
% 0.20/0.49 tff(29,plain,
% 0.20/0.49 ((~![X30: $i] : p2(X30, X30)) | p2(c48, c48)),
% 0.20/0.49 inference(quant_inst,[status(thm)],[])).
% 0.20/0.49 tff(30,plain,
% 0.20/0.49 ($false),
% 0.20/0.49 inference(unit_resolution,[status(thm)],[29, 28, 21])).
% 0.20/0.49 tff(31,plain,(p2(c48, c48)), inference(lemma,lemma(discharge,[]))).
% 0.20/0.49 tff(32,plain,
% 0.20/0.49 (^[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))))),
% 0.20/0.49 inference(bind,[status(th)],[])).
% 0.20/0.49 tff(33,plain,
% 0.20/0.49 (![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)))),
% 0.20/0.49 inference(quant_intro,[status(thm)],[32])).
% 0.20/0.49 tff(34,plain,
% 0.20/0.49 (![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)))),
% 0.20/0.49 inference(rewrite,[status(thm)],[])).
% 0.20/0.49 tff(35,plain,
% 0.20/0.49 (^[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)))))),
% 0.20/0.49 inference(bind,[status(th)],[])).
% 0.20/0.49 tff(36,plain,
% 0.20/0.49 (![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)))),
% 0.20/0.49 inference(quant_intro,[status(thm)],[35])).
% 0.20/0.49 tff(37,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/sandbox2/benchmark/theBenchmark.p','p4_60')).
% 0.20/0.49 tff(38,plain,
% 0.20/0.49 (![X118: $i, X119: $i, X121: $i, X120: $i] : ((~p3(X119, X121)) | (~p2(X118, X120)) | p4(f5(X118, X119), f5(X120, X121)))),
% 0.20/0.49 inference(modus_ponens,[status(thm)],[37, 36])).
% 0.20/0.49 tff(39,plain,
% 0.20/0.49 (![X118: $i, X119: $i, X121: $i, X120: $i] : ((~p3(X119, X121)) | (~p2(X118, X120)) | p4(f5(X118, X119), f5(X120, X121)))),
% 0.20/0.49 inference(modus_ponens,[status(thm)],[38, 34])).
% 0.20/0.49 tff(40,plain,(
% 0.20/0.49 ![X118: $i, X119: $i, X121: $i, X120: $i] : ((~p3(X119, X121)) | (~p2(X118, X120)) | p4(f5(X118, X119), f5(X120, X121)))),
% 0.20/0.49 inference(skolemize,[status(sab)],[39])).
% 0.20/0.49 tff(41,plain,
% 0.20/0.49 (![X118: $i, X119: $i, X121: $i, X120: $i] : ((~p3(X119, X121)) | (~p2(X118, X120)) | p4(f5(X118, X119), f5(X120, X121)))),
% 0.20/0.49 inference(modus_ponens,[status(thm)],[40, 33])).
% 0.20/0.49 tff(42,plain,
% 0.20/0.49 (((~![X118: $i, X119: $i, X121: $i, X120: $i] : ((~p3(X119, X121)) | (~p2(X118, X120)) | p4(f5(X118, X119), f5(X120, X121)))) | ((~p2(c48, c48)) | (~p3(f16(f18(c54, f8(f11(f13(c49, c50), c51), c52)), c55), f8(f11(f13(c49, f20(f22(f24(f26(c56, c50), c51), c52), c55)), f30(f32(f34(f36(c57, c50), c51), c52), c55)), f40(f42(f44(f46(c58, c50), c51), c52), c55)))) | p4(f5(c48, f16(f18(c54, f8(f11(f13(c49, c50), c51), c52)), c55)), f5(c48, f8(f11(f13(c49, f20(f22(f24(f26(c56, c50), c51), c52), c55)), f30(f32(f34(f36(c57, c50), c51), c52), c55)), f40(f42(f44(f46(c58, c50), c51), c52), c55)))))) <=> ((~![X118: $i, X119: $i, X121: $i, X120: $i] : ((~p3(X119, X121)) | (~p2(X118, X120)) | p4(f5(X118, X119), f5(X120, X121)))) | (~p2(c48, c48)) | (~p3(f16(f18(c54, f8(f11(f13(c49, c50), c51), c52)), c55), f8(f11(f13(c49, f20(f22(f24(f26(c56, c50), c51), c52), c55)), f30(f32(f34(f36(c57, c50), c51), c52), c55)), f40(f42(f44(f46(c58, c50), c51), c52), c55)))) | p4(f5(c48, f16(f18(c54, f8(f11(f13(c49, c50), c51), c52)), c55)), f5(c48, f8(f11(f13(c49, f20(f22(f24(f26(c56, c50), c51), c52), c55)), f30(f32(f34(f36(c57, c50), c51), c52), c55)), f40(f42(f44(f46(c58, c50), c51), c52), c55)))))),
% 0.20/0.49 inference(rewrite,[status(thm)],[])).
% 0.20/0.49 tff(43,plain,
% 0.20/0.49 (((~p3(f16(f18(c54, f8(f11(f13(c49, c50), c51), c52)), c55), f8(f11(f13(c49, f20(f22(f24(f26(c56, c50), c51), c52), c55)), f30(f32(f34(f36(c57, c50), c51), c52), c55)), f40(f42(f44(f46(c58, c50), c51), c52), c55)))) | (~p2(c48, c48)) | p4(f5(c48, f16(f18(c54, f8(f11(f13(c49, c50), c51), c52)), c55)), f5(c48, f8(f11(f13(c49, f20(f22(f24(f26(c56, c50), c51), c52), c55)), f30(f32(f34(f36(c57, c50), c51), c52), c55)), f40(f42(f44(f46(c58, c50), c51), c52), c55))))) <=> ((~p2(c48, c48)) | (~p3(f16(f18(c54, f8(f11(f13(c49, c50), c51), c52)), c55), f8(f11(f13(c49, f20(f22(f24(f26(c56, c50), c51), c52), c55)), f30(f32(f34(f36(c57, c50), c51), c52), c55)), f40(f42(f44(f46(c58, c50), c51), c52), c55)))) | p4(f5(c48, f16(f18(c54, f8(f11(f13(c49, c50), c51), c52)), c55)), f5(c48, f8(f11(f13(c49, f20(f22(f24(f26(c56, c50), c51), c52), c55)), f30(f32(f34(f36(c57, c50), c51), c52), c55)), f40(f42(f44(f46(c58, c50), c51), c52), c55)))))),
% 0.20/0.49 inference(rewrite,[status(thm)],[])).
% 0.20/0.49 tff(44,plain,
% 0.20/0.49 (((~![X118: $i, X119: $i, X121: $i, X120: $i] : ((~p3(X119, X121)) | (~p2(X118, X120)) | p4(f5(X118, X119), f5(X120, X121)))) | ((~p3(f16(f18(c54, f8(f11(f13(c49, c50), c51), c52)), c55), f8(f11(f13(c49, f20(f22(f24(f26(c56, c50), c51), c52), c55)), f30(f32(f34(f36(c57, c50), c51), c52), c55)), f40(f42(f44(f46(c58, c50), c51), c52), c55)))) | (~p2(c48, c48)) | p4(f5(c48, f16(f18(c54, f8(f11(f13(c49, c50), c51), c52)), c55)), f5(c48, f8(f11(f13(c49, f20(f22(f24(f26(c56, c50), c51), c52), c55)), f30(f32(f34(f36(c57, c50), c51), c52), c55)), f40(f42(f44(f46(c58, c50), c51), c52), c55)))))) <=> ((~![X118: $i, X119: $i, X121: $i, X120: $i] : ((~p3(X119, X121)) | (~p2(X118, X120)) | p4(f5(X118, X119), f5(X120, X121)))) | ((~p2(c48, c48)) | (~p3(f16(f18(c54, f8(f11(f13(c49, c50), c51), c52)), c55), f8(f11(f13(c49, f20(f22(f24(f26(c56, c50), c51), c52), c55)), f30(f32(f34(f36(c57, c50), c51), c52), c55)), f40(f42(f44(f46(c58, c50), c51), c52), c55)))) | p4(f5(c48, f16(f18(c54, f8(f11(f13(c49, c50), c51), c52)), c55)), f5(c48, f8(f11(f13(c49, f20(f22(f24(f26(c56, c50), c51), c52), c55)), f30(f32(f34(f36(c57, c50), c51), c52), c55)), f40(f42(f44(f46(c58, c50), c51), c52), c55))))))),
% 0.20/0.49 inference(monotonicity,[status(thm)],[43])).
% 0.20/0.49 tff(45,plain,
% 0.20/0.49 (((~![X118: $i, X119: $i, X121: $i, X120: $i] : ((~p3(X119, X121)) | (~p2(X118, X120)) | p4(f5(X118, X119), f5(X120, X121)))) | ((~p3(f16(f18(c54, f8(f11(f13(c49, c50), c51), c52)), c55), f8(f11(f13(c49, f20(f22(f24(f26(c56, c50), c51), c52), c55)), f30(f32(f34(f36(c57, c50), c51), c52), c55)), f40(f42(f44(f46(c58, c50), c51), c52), c55)))) | (~p2(c48, c48)) | p4(f5(c48, f16(f18(c54, f8(f11(f13(c49, c50), c51), c52)), c55)), f5(c48, f8(f11(f13(c49, f20(f22(f24(f26(c56, c50), c51), c52), c55)), f30(f32(f34(f36(c57, c50), c51), c52), c55)), f40(f42(f44(f46(c58, c50), c51), c52), c55)))))) <=> ((~![X118: $i, X119: $i, X121: $i, X120: $i] : ((~p3(X119, X121)) | (~p2(X118, X120)) | p4(f5(X118, X119), f5(X120, X121)))) | (~p2(c48, c48)) | (~p3(f16(f18(c54, f8(f11(f13(c49, c50), c51), c52)), c55), f8(f11(f13(c49, f20(f22(f24(f26(c56, c50), c51), c52), c55)), f30(f32(f34(f36(c57, c50), c51), c52), c55)), f40(f42(f44(f46(c58, c50), c51), c52), c55)))) | p4(f5(c48, f16(f18(c54, f8(f11(f13(c49, c50), c51), c52)), c55)), f5(c48, f8(f11(f13(c49, f20(f22(f24(f26(c56, c50), c51), c52), c55)), f30(f32(f34(f36(c57, c50), c51), c52), c55)), f40(f42(f44(f46(c58, c50), c51), c52), c55)))))),
% 0.20/0.49 inference(transitivity,[status(thm)],[44, 42])).
% 0.20/0.49 tff(46,plain,
% 0.20/0.49 ((~![X118: $i, X119: $i, X121: $i, X120: $i] : ((~p3(X119, X121)) | (~p2(X118, X120)) | p4(f5(X118, X119), f5(X120, X121)))) | ((~p3(f16(f18(c54, f8(f11(f13(c49, c50), c51), c52)), c55), f8(f11(f13(c49, f20(f22(f24(f26(c56, c50), c51), c52), c55)), f30(f32(f34(f36(c57, c50), c51), c52), c55)), f40(f42(f44(f46(c58, c50), c51), c52), c55)))) | (~p2(c48, c48)) | p4(f5(c48, f16(f18(c54, f8(f11(f13(c49, c50), c51), c52)), c55)), f5(c48, f8(f11(f13(c49, f20(f22(f24(f26(c56, c50), c51), c52), c55)), f30(f32(f34(f36(c57, c50), c51), c52), c55)), f40(f42(f44(f46(c58, c50), c51), c52), c55)))))),
% 0.20/0.49 inference(quant_inst,[status(thm)],[])).
% 0.20/0.49 tff(47,plain,
% 0.20/0.49 ((~![X118: $i, X119: $i, X121: $i, X120: $i] : ((~p3(X119, X121)) | (~p2(X118, X120)) | p4(f5(X118, X119), f5(X120, X121)))) | (~p2(c48, c48)) | (~p3(f16(f18(c54, f8(f11(f13(c49, c50), c51), c52)), c55), f8(f11(f13(c49, f20(f22(f24(f26(c56, c50), c51), c52), c55)), f30(f32(f34(f36(c57, c50), c51), c52), c55)), f40(f42(f44(f46(c58, c50), c51), c52), c55)))) | p4(f5(c48, f16(f18(c54, f8(f11(f13(c49, c50), c51), c52)), c55)), f5(c48, f8(f11(f13(c49, f20(f22(f24(f26(c56, c50), c51), c52), c55)), f30(f32(f34(f36(c57, c50), c51), c52), c55)), f40(f42(f44(f46(c58, c50), c51), c52), c55))))),
% 0.20/0.50 inference(modus_ponens,[status(thm)],[46, 45])).
% 0.20/0.50 tff(48,plain,
% 0.20/0.50 (p4(f5(c48, f16(f18(c54, f8(f11(f13(c49, c50), c51), c52)), c55)), f5(c48, f8(f11(f13(c49, f20(f22(f24(f26(c56, c50), c51), c52), c55)), f30(f32(f34(f36(c57, c50), c51), c52), c55)), f40(f42(f44(f46(c58, c50), c51), c52), c55))))),
% 0.20/0.50 inference(unit_resolution,[status(thm)],[47, 41, 31, 20])).
% 0.20/0.50 tff(49,plain,
% 0.20/0.50 (p47(f5(c48, f16(f18(c54, f8(f11(f13(c49, c50), c51), c52)), c55)), c53) <=> p47(f5(c48, f16(f18(c54, f8(f11(f13(c49, c50), c51), c52)), c55)), c53)),
% 0.20/0.50 inference(rewrite,[status(thm)],[])).
% 0.20/0.50 tff(50,axiom,(p47(f5(c48, f16(f18(c54, f8(f11(f13(c49, c50), c51), c52)), c55)), c53)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','p47_77')).
% 0.20/0.50 tff(51,plain,
% 0.20/0.50 (p47(f5(c48, f16(f18(c54, f8(f11(f13(c49, c50), c51), c52)), c55)), c53)),
% 0.20/0.50 inference(modus_ponens,[status(thm)],[50, 49])).
% 0.20/0.50 tff(52,plain,
% 0.20/0.50 (^[X144: $i, X146: $i, X143: $i, X145: $i] : refl(((~p4(X146, X143)) | (~p15(X145, X144)) | (~p47(X146, X145)) | p47(X143, X144)) <=> ((~p4(X146, X143)) | (~p15(X145, X144)) | (~p47(X146, X145)) | p47(X143, X144)))),
% 0.20/0.50 inference(bind,[status(th)],[])).
% 0.20/0.50 tff(53,plain,
% 0.20/0.50 (![X144: $i, X146: $i, X143: $i, X145: $i] : ((~p4(X146, X143)) | (~p15(X145, X144)) | (~p47(X146, X145)) | p47(X143, X144)) <=> ![X144: $i, X146: $i, X143: $i, X145: $i] : ((~p4(X146, X143)) | (~p15(X145, X144)) | (~p47(X146, X145)) | p47(X143, X144))),
% 0.20/0.50 inference(quant_intro,[status(thm)],[52])).
% 0.20/0.50 tff(54,plain,
% 0.20/0.50 (![X144: $i, X146: $i, X143: $i, X145: $i] : ((~p4(X146, X143)) | (~p15(X145, X144)) | (~p47(X146, X145)) | p47(X143, X144)) <=> ![X144: $i, X146: $i, X143: $i, X145: $i] : ((~p4(X146, X143)) | (~p15(X145, X144)) | (~p47(X146, X145)) | p47(X143, X144))),
% 0.20/0.50 inference(rewrite,[status(thm)],[])).
% 0.20/0.50 tff(55,plain,
% 0.20/0.50 (^[X144: $i, X146: $i, X143: $i, X145: $i] : trans(monotonicity(trans(monotonicity(rewrite((p47(X143, X144) | (~p4(X146, X143))) <=> ((~p4(X146, X143)) | p47(X143, X144))), (((p47(X143, X144) | (~p4(X146, X143))) | (~p47(X146, X145))) <=> (((~p4(X146, X143)) | p47(X143, X144)) | (~p47(X146, X145))))), rewrite((((~p4(X146, X143)) | p47(X143, X144)) | (~p47(X146, X145))) <=> ((~p4(X146, X143)) | (~p47(X146, X145)) | p47(X143, X144))), (((p47(X143, X144) | (~p4(X146, X143))) | (~p47(X146, X145))) <=> ((~p4(X146, X143)) | (~p47(X146, X145)) | p47(X143, X144)))), ((((p47(X143, X144) | (~p4(X146, X143))) | (~p47(X146, X145))) | (~p15(X145, X144))) <=> (((~p4(X146, X143)) | (~p47(X146, X145)) | p47(X143, X144)) | (~p15(X145, X144))))), rewrite((((~p4(X146, X143)) | (~p47(X146, X145)) | p47(X143, X144)) | (~p15(X145, X144))) <=> ((~p4(X146, X143)) | (~p15(X145, X144)) | (~p47(X146, X145)) | p47(X143, X144))), ((((p47(X143, X144) | (~p4(X146, X143))) | (~p47(X146, X145))) | (~p15(X145, X144))) <=> ((~p4(X146, X143)) | (~p15(X145, X144)) | (~p47(X146, X145)) | p47(X143, X144))))),
% 0.20/0.50 inference(bind,[status(th)],[])).
% 0.20/0.50 tff(56,plain,
% 0.20/0.50 (![X144: $i, X146: $i, X143: $i, X145: $i] : (((p47(X143, X144) | (~p4(X146, X143))) | (~p47(X146, X145))) | (~p15(X145, X144))) <=> ![X144: $i, X146: $i, X143: $i, X145: $i] : ((~p4(X146, X143)) | (~p15(X145, X144)) | (~p47(X146, X145)) | p47(X143, X144))),
% 0.20/0.50 inference(quant_intro,[status(thm)],[55])).
% 0.20/0.50 tff(57,axiom,(![X144: $i, X146: $i, X143: $i, X145: $i] : (((p47(X143, X144) | (~p4(X146, X143))) | (~p47(X146, X145))) | (~p15(X145, X144)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','p47_53')).
% 0.20/0.50 tff(58,plain,
% 0.20/0.50 (![X144: $i, X146: $i, X143: $i, X145: $i] : ((~p4(X146, X143)) | (~p15(X145, X144)) | (~p47(X146, X145)) | p47(X143, X144))),
% 0.20/0.50 inference(modus_ponens,[status(thm)],[57, 56])).
% 0.20/0.50 tff(59,plain,
% 0.20/0.50 (![X144: $i, X146: $i, X143: $i, X145: $i] : ((~p4(X146, X143)) | (~p15(X145, X144)) | (~p47(X146, X145)) | p47(X143, X144))),
% 0.20/0.50 inference(modus_ponens,[status(thm)],[58, 54])).
% 0.20/0.50 tff(60,plain,(
% 0.20/0.50 ![X144: $i, X146: $i, X143: $i, X145: $i] : ((~p4(X146, X143)) | (~p15(X145, X144)) | (~p47(X146, X145)) | p47(X143, X144))),
% 0.20/0.50 inference(skolemize,[status(sab)],[59])).
% 0.20/0.50 tff(61,plain,
% 0.20/0.50 (![X144: $i, X146: $i, X143: $i, X145: $i] : ((~p4(X146, X143)) | (~p15(X145, X144)) | (~p47(X146, X145)) | p47(X143, X144))),
% 0.20/0.50 inference(modus_ponens,[status(thm)],[60, 53])).
% 0.20/0.50 tff(62,plain,
% 0.20/0.50 (((~![X144: $i, X146: $i, X143: $i, X145: $i] : ((~p4(X146, X143)) | (~p15(X145, X144)) | (~p47(X146, X145)) | p47(X143, X144))) | ((~p47(f5(c48, f16(f18(c54, f8(f11(f13(c49, c50), c51), c52)), c55)), c53)) | (~p4(f5(c48, f16(f18(c54, f8(f11(f13(c49, c50), c51), c52)), c55)), f5(c48, f8(f11(f13(c49, f20(f22(f24(f26(c56, c50), c51), c52), c55)), f30(f32(f34(f36(c57, c50), c51), c52), c55)), f40(f42(f44(f46(c58, c50), c51), c52), c55))))) | p47(f5(c48, f8(f11(f13(c49, f20(f22(f24(f26(c56, c50), c51), c52), c55)), f30(f32(f34(f36(c57, c50), c51), c52), c55)), f40(f42(f44(f46(c58, c50), c51), c52), c55))), c53) | (~p15(c53, c53)))) <=> ((~![X144: $i, X146: $i, X143: $i, X145: $i] : ((~p4(X146, X143)) | (~p15(X145, X144)) | (~p47(X146, X145)) | p47(X143, X144))) | (~p47(f5(c48, f16(f18(c54, f8(f11(f13(c49, c50), c51), c52)), c55)), c53)) | (~p4(f5(c48, f16(f18(c54, f8(f11(f13(c49, c50), c51), c52)), c55)), f5(c48, f8(f11(f13(c49, f20(f22(f24(f26(c56, c50), c51), c52), c55)), f30(f32(f34(f36(c57, c50), c51), c52), c55)), f40(f42(f44(f46(c58, c50), c51), c52), c55))))) | p47(f5(c48, f8(f11(f13(c49, f20(f22(f24(f26(c56, c50), c51), c52), c55)), f30(f32(f34(f36(c57, c50), c51), c52), c55)), f40(f42(f44(f46(c58, c50), c51), c52), c55))), c53) | (~p15(c53, c53)))),
% 0.20/0.50 inference(rewrite,[status(thm)],[])).
% 0.20/0.50 tff(63,plain,
% 0.20/0.50 (((~p4(f5(c48, f16(f18(c54, f8(f11(f13(c49, c50), c51), c52)), c55)), f5(c48, f8(f11(f13(c49, f20(f22(f24(f26(c56, c50), c51), c52), c55)), f30(f32(f34(f36(c57, c50), c51), c52), c55)), f40(f42(f44(f46(c58, c50), c51), c52), c55))))) | (~p15(c53, c53)) | (~p47(f5(c48, f16(f18(c54, f8(f11(f13(c49, c50), c51), c52)), c55)), c53)) | p47(f5(c48, f8(f11(f13(c49, f20(f22(f24(f26(c56, c50), c51), c52), c55)), f30(f32(f34(f36(c57, c50), c51), c52), c55)), f40(f42(f44(f46(c58, c50), c51), c52), c55))), c53)) <=> ((~p47(f5(c48, f16(f18(c54, f8(f11(f13(c49, c50), c51), c52)), c55)), c53)) | (~p4(f5(c48, f16(f18(c54, f8(f11(f13(c49, c50), c51), c52)), c55)), f5(c48, f8(f11(f13(c49, f20(f22(f24(f26(c56, c50), c51), c52), c55)), f30(f32(f34(f36(c57, c50), c51), c52), c55)), f40(f42(f44(f46(c58, c50), c51), c52), c55))))) | p47(f5(c48, f8(f11(f13(c49, f20(f22(f24(f26(c56, c50), c51), c52), c55)), f30(f32(f34(f36(c57, c50), c51), c52), c55)), f40(f42(f44(f46(c58, c50), c51), c52), c55))), c53) | (~p15(c53, c53)))),
% 0.20/0.50 inference(rewrite,[status(thm)],[])).
% 0.20/0.50 tff(64,plain,
% 0.20/0.50 (((~![X144: $i, X146: $i, X143: $i, X145: $i] : ((~p4(X146, X143)) | (~p15(X145, X144)) | (~p47(X146, X145)) | p47(X143, X144))) | ((~p4(f5(c48, f16(f18(c54, f8(f11(f13(c49, c50), c51), c52)), c55)), f5(c48, f8(f11(f13(c49, f20(f22(f24(f26(c56, c50), c51), c52), c55)), f30(f32(f34(f36(c57, c50), c51), c52), c55)), f40(f42(f44(f46(c58, c50), c51), c52), c55))))) | (~p15(c53, c53)) | (~p47(f5(c48, f16(f18(c54, f8(f11(f13(c49, c50), c51), c52)), c55)), c53)) | p47(f5(c48, f8(f11(f13(c49, f20(f22(f24(f26(c56, c50), c51), c52), c55)), f30(f32(f34(f36(c57, c50), c51), c52), c55)), f40(f42(f44(f46(c58, c50), c51), c52), c55))), c53))) <=> ((~![X144: $i, X146: $i, X143: $i, X145: $i] : ((~p4(X146, X143)) | (~p15(X145, X144)) | (~p47(X146, X145)) | p47(X143, X144))) | ((~p47(f5(c48, f16(f18(c54, f8(f11(f13(c49, c50), c51), c52)), c55)), c53)) | (~p4(f5(c48, f16(f18(c54, f8(f11(f13(c49, c50), c51), c52)), c55)), f5(c48, f8(f11(f13(c49, f20(f22(f24(f26(c56, c50), c51), c52), c55)), f30(f32(f34(f36(c57, c50), c51), c52), c55)), f40(f42(f44(f46(c58, c50), c51), c52), c55))))) | p47(f5(c48, f8(f11(f13(c49, f20(f22(f24(f26(c56, c50), c51), c52), c55)), f30(f32(f34(f36(c57, c50), c51), c52), c55)), f40(f42(f44(f46(c58, c50), c51), c52), c55))), c53) | (~p15(c53, c53))))),
% 0.20/0.50 inference(monotonicity,[status(thm)],[63])).
% 0.20/0.50 tff(65,plain,
% 0.20/0.50 (((~![X144: $i, X146: $i, X143: $i, X145: $i] : ((~p4(X146, X143)) | (~p15(X145, X144)) | (~p47(X146, X145)) | p47(X143, X144))) | ((~p4(f5(c48, f16(f18(c54, f8(f11(f13(c49, c50), c51), c52)), c55)), f5(c48, f8(f11(f13(c49, f20(f22(f24(f26(c56, c50), c51), c52), c55)), f30(f32(f34(f36(c57, c50), c51), c52), c55)), f40(f42(f44(f46(c58, c50), c51), c52), c55))))) | (~p15(c53, c53)) | (~p47(f5(c48, f16(f18(c54, f8(f11(f13(c49, c50), c51), c52)), c55)), c53)) | p47(f5(c48, f8(f11(f13(c49, f20(f22(f24(f26(c56, c50), c51), c52), c55)), f30(f32(f34(f36(c57, c50), c51), c52), c55)), f40(f42(f44(f46(c58, c50), c51), c52), c55))), c53))) <=> ((~![X144: $i, X146: $i, X143: $i, X145: $i] : ((~p4(X146, X143)) | (~p15(X145, X144)) | (~p47(X146, X145)) | p47(X143, X144))) | (~p47(f5(c48, f16(f18(c54, f8(f11(f13(c49, c50), c51), c52)), c55)), c53)) | (~p4(f5(c48, f16(f18(c54, f8(f11(f13(c49, c50), c51), c52)), c55)), f5(c48, f8(f11(f13(c49, f20(f22(f24(f26(c56, c50), c51), c52), c55)), f30(f32(f34(f36(c57, c50), c51), c52), c55)), f40(f42(f44(f46(c58, c50), c51), c52), c55))))) | p47(f5(c48, f8(f11(f13(c49, f20(f22(f24(f26(c56, c50), c51), c52), c55)), f30(f32(f34(f36(c57, c50), c51), c52), c55)), f40(f42(f44(f46(c58, c50), c51), c52), c55))), c53) | (~p15(c53, c53)))),
% 0.20/0.50 inference(transitivity,[status(thm)],[64, 62])).
% 0.20/0.50 tff(66,plain,
% 0.20/0.50 ((~![X144: $i, X146: $i, X143: $i, X145: $i] : ((~p4(X146, X143)) | (~p15(X145, X144)) | (~p47(X146, X145)) | p47(X143, X144))) | ((~p4(f5(c48, f16(f18(c54, f8(f11(f13(c49, c50), c51), c52)), c55)), f5(c48, f8(f11(f13(c49, f20(f22(f24(f26(c56, c50), c51), c52), c55)), f30(f32(f34(f36(c57, c50), c51), c52), c55)), f40(f42(f44(f46(c58, c50), c51), c52), c55))))) | (~p15(c53, c53)) | (~p47(f5(c48, f16(f18(c54, f8(f11(f13(c49, c50), c51), c52)), c55)), c53)) | p47(f5(c48, f8(f11(f13(c49, f20(f22(f24(f26(c56, c50), c51), c52), c55)), f30(f32(f34(f36(c57, c50), c51), c52), c55)), f40(f42(f44(f46(c58, c50), c51), c52), c55))), c53))),
% 0.20/0.50 inference(quant_inst,[status(thm)],[])).
% 0.20/0.50 tff(67,plain,
% 0.20/0.50 ((~![X144: $i, X146: $i, X143: $i, X145: $i] : ((~p4(X146, X143)) | (~p15(X145, X144)) | (~p47(X146, X145)) | p47(X143, X144))) | (~p47(f5(c48, f16(f18(c54, f8(f11(f13(c49, c50), c51), c52)), c55)), c53)) | (~p4(f5(c48, f16(f18(c54, f8(f11(f13(c49, c50), c51), c52)), c55)), f5(c48, f8(f11(f13(c49, f20(f22(f24(f26(c56, c50), c51), c52), c55)), f30(f32(f34(f36(c57, c50), c51), c52), c55)), f40(f42(f44(f46(c58, c50), c51), c52), c55))))) | p47(f5(c48, f8(f11(f13(c49, f20(f22(f24(f26(c56, c50), c51), c52), c55)), f30(f32(f34(f36(c57, c50), c51), c52), c55)), f40(f42(f44(f46(c58, c50), c51), c52), c55))), c53) | (~p15(c53, c53))),
% 0.20/0.50 inference(modus_ponens,[status(thm)],[66, 65])).
% 0.20/0.50 tff(68,plain,
% 0.20/0.50 (p47(f5(c48, f8(f11(f13(c49, f20(f22(f24(f26(c56, c50), c51), c52), c55)), f30(f32(f34(f36(c57, c50), c51), c52), c55)), f40(f42(f44(f46(c58, c50), c51), c52), c55))), c53)),
% 0.20/0.50 inference(unit_resolution,[status(thm)],[67, 61, 51, 48, 11])).
% 0.20/0.50 tff(69,plain,
% 0.20/0.50 (^[X142: $i, X140: $i, X141: $i, X139: $i] : refl(((~p47(f5(c48, f8(f11(f13(c49, X139), X141), X142)), X140)) | p47(X139, X140)) <=> ((~p47(f5(c48, f8(f11(f13(c49, X139), X141), X142)), X140)) | p47(X139, X140)))),
% 0.20/0.50 inference(bind,[status(th)],[])).
% 0.20/0.50 tff(70,plain,
% 0.20/0.50 (![X142: $i, X140: $i, X141: $i, X139: $i] : ((~p47(f5(c48, f8(f11(f13(c49, X139), X141), X142)), X140)) | p47(X139, X140)) <=> ![X142: $i, X140: $i, X141: $i, X139: $i] : ((~p47(f5(c48, f8(f11(f13(c49, X139), X141), X142)), X140)) | p47(X139, X140))),
% 0.20/0.50 inference(quant_intro,[status(thm)],[69])).
% 0.20/0.50 tff(71,plain,
% 0.20/0.50 (![X142: $i, X140: $i, X141: $i, X139: $i] : ((~p47(f5(c48, f8(f11(f13(c49, X139), X141), X142)), X140)) | p47(X139, X140)) <=> ![X142: $i, X140: $i, X141: $i, X139: $i] : ((~p47(f5(c48, f8(f11(f13(c49, X139), X141), X142)), X140)) | p47(X139, X140))),
% 0.20/0.50 inference(rewrite,[status(thm)],[])).
% 0.20/0.50 tff(72,plain,
% 0.20/0.50 (^[X142: $i, X140: $i, X141: $i, X139: $i] : rewrite((p47(X139, X140) | (~p47(f5(c48, f8(f11(f13(c49, X139), X141), X142)), X140))) <=> ((~p47(f5(c48, f8(f11(f13(c49, X139), X141), X142)), X140)) | p47(X139, X140)))),
% 0.20/0.50 inference(bind,[status(th)],[])).
% 0.20/0.50 tff(73,plain,
% 0.20/0.50 (![X142: $i, X140: $i, X141: $i, X139: $i] : (p47(X139, X140) | (~p47(f5(c48, f8(f11(f13(c49, X139), X141), X142)), X140))) <=> ![X142: $i, X140: $i, X141: $i, X139: $i] : ((~p47(f5(c48, f8(f11(f13(c49, X139), X141), X142)), X140)) | p47(X139, X140))),
% 0.20/0.50 inference(quant_intro,[status(thm)],[72])).
% 0.20/0.50 tff(74,axiom,(![X142: $i, X140: $i, X141: $i, X139: $i] : (p47(X139, X140) | (~p47(f5(c48, f8(f11(f13(c49, X139), X141), X142)), X140)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','p47_74')).
% 0.20/0.50 tff(75,plain,
% 0.20/0.50 (![X142: $i, X140: $i, X141: $i, X139: $i] : ((~p47(f5(c48, f8(f11(f13(c49, X139), X141), X142)), X140)) | p47(X139, X140))),
% 0.20/0.50 inference(modus_ponens,[status(thm)],[74, 73])).
% 0.20/0.50 tff(76,plain,
% 0.20/0.50 (![X142: $i, X140: $i, X141: $i, X139: $i] : ((~p47(f5(c48, f8(f11(f13(c49, X139), X141), X142)), X140)) | p47(X139, X140))),
% 0.20/0.50 inference(modus_ponens,[status(thm)],[75, 71])).
% 0.20/0.50 tff(77,plain,(
% 0.20/0.50 ![X142: $i, X140: $i, X141: $i, X139: $i] : ((~p47(f5(c48, f8(f11(f13(c49, X139), X141), X142)), X140)) | p47(X139, X140))),
% 0.20/0.50 inference(skolemize,[status(sab)],[76])).
% 0.20/0.50 tff(78,plain,
% 0.20/0.50 (![X142: $i, X140: $i, X141: $i, X139: $i] : ((~p47(f5(c48, f8(f11(f13(c49, X139), X141), X142)), X140)) | p47(X139, X140))),
% 0.20/0.50 inference(modus_ponens,[status(thm)],[77, 70])).
% 0.20/0.50 tff(79,plain,
% 0.20/0.50 (((~![X142: $i, X140: $i, X141: $i, X139: $i] : ((~p47(f5(c48, f8(f11(f13(c49, X139), X141), X142)), X140)) | p47(X139, X140))) | ((~p47(f5(c48, f8(f11(f13(c49, f20(f22(f24(f26(c56, c50), c51), c52), c55)), f30(f32(f34(f36(c57, c50), c51), c52), c55)), f40(f42(f44(f46(c58, c50), c51), c52), c55))), c53)) | p47(f20(f22(f24(f26(c56, c50), c51), c52), c55), c53))) <=> ((~![X142: $i, X140: $i, X141: $i, X139: $i] : ((~p47(f5(c48, f8(f11(f13(c49, X139), X141), X142)), X140)) | p47(X139, X140))) | (~p47(f5(c48, f8(f11(f13(c49, f20(f22(f24(f26(c56, c50), c51), c52), c55)), f30(f32(f34(f36(c57, c50), c51), c52), c55)), f40(f42(f44(f46(c58, c50), c51), c52), c55))), c53)) | p47(f20(f22(f24(f26(c56, c50), c51), c52), c55), c53))),
% 0.20/0.50 inference(rewrite,[status(thm)],[])).
% 0.20/0.50 tff(80,plain,
% 0.20/0.50 ((~![X142: $i, X140: $i, X141: $i, X139: $i] : ((~p47(f5(c48, f8(f11(f13(c49, X139), X141), X142)), X140)) | p47(X139, X140))) | ((~p47(f5(c48, f8(f11(f13(c49, f20(f22(f24(f26(c56, c50), c51), c52), c55)), f30(f32(f34(f36(c57, c50), c51), c52), c55)), f40(f42(f44(f46(c58, c50), c51), c52), c55))), c53)) | p47(f20(f22(f24(f26(c56, c50), c51), c52), c55), c53))),
% 0.20/0.50 inference(quant_inst,[status(thm)],[])).
% 0.20/0.50 tff(81,plain,
% 0.20/0.50 ((~![X142: $i, X140: $i, X141: $i, X139: $i] : ((~p47(f5(c48, f8(f11(f13(c49, X139), X141), X142)), X140)) | p47(X139, X140))) | (~p47(f5(c48, f8(f11(f13(c49, f20(f22(f24(f26(c56, c50), c51), c52), c55)), f30(f32(f34(f36(c57, c50), c51), c52), c55)), f40(f42(f44(f46(c58, c50), c51), c52), c55))), c53)) | p47(f20(f22(f24(f26(c56, c50), c51), c52), c55), c53)),
% 0.20/0.50 inference(modus_ponens,[status(thm)],[80, 79])).
% 0.20/0.50 tff(82,plain,
% 0.20/0.50 (p47(f20(f22(f24(f26(c56, c50), c51), c52), c55), c53)),
% 0.20/0.50 inference(unit_resolution,[status(thm)],[81, 78, 68])).
% 0.20/0.50 tff(83,plain,
% 0.20/0.50 (^[X142: $i, X140: $i, X141: $i, X139: $i] : refl((p47(f5(c48, f8(f11(f13(c49, X139), X141), X142)), X140) | (~p47(X139, X140))) <=> (p47(f5(c48, f8(f11(f13(c49, X139), X141), X142)), X140) | (~p47(X139, X140))))),
% 0.20/0.50 inference(bind,[status(th)],[])).
% 0.20/0.50 tff(84,plain,
% 0.20/0.50 (![X142: $i, X140: $i, X141: $i, X139: $i] : (p47(f5(c48, f8(f11(f13(c49, X139), X141), X142)), X140) | (~p47(X139, X140))) <=> ![X142: $i, X140: $i, X141: $i, X139: $i] : (p47(f5(c48, f8(f11(f13(c49, X139), X141), X142)), X140) | (~p47(X139, X140)))),
% 0.20/0.50 inference(quant_intro,[status(thm)],[83])).
% 0.20/0.50 tff(85,plain,
% 0.20/0.50 (![X142: $i, X140: $i, X141: $i, X139: $i] : (p47(f5(c48, f8(f11(f13(c49, X139), X141), X142)), X140) | (~p47(X139, X140))) <=> ![X142: $i, X140: $i, X141: $i, X139: $i] : (p47(f5(c48, f8(f11(f13(c49, X139), X141), X142)), X140) | (~p47(X139, X140)))),
% 0.20/0.50 inference(rewrite,[status(thm)],[])).
% 0.20/0.50 tff(86,axiom,(![X142: $i, X140: $i, X141: $i, X139: $i] : (p47(f5(c48, f8(f11(f13(c49, X139), X141), X142)), X140) | (~p47(X139, X140)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','p47_76')).
% 0.20/0.51 tff(87,plain,
% 0.20/0.51 (![X142: $i, X140: $i, X141: $i, X139: $i] : (p47(f5(c48, f8(f11(f13(c49, X139), X141), X142)), X140) | (~p47(X139, X140)))),
% 0.20/0.51 inference(modus_ponens,[status(thm)],[86, 85])).
% 0.20/0.51 tff(88,plain,(
% 0.20/0.51 ![X142: $i, X140: $i, X141: $i, X139: $i] : (p47(f5(c48, f8(f11(f13(c49, X139), X141), X142)), X140) | (~p47(X139, X140)))),
% 0.20/0.51 inference(skolemize,[status(sab)],[87])).
% 0.20/0.51 tff(89,plain,
% 0.20/0.51 (![X142: $i, X140: $i, X141: $i, X139: $i] : (p47(f5(c48, f8(f11(f13(c49, X139), X141), X142)), X140) | (~p47(X139, X140)))),
% 0.20/0.51 inference(modus_ponens,[status(thm)],[88, 84])).
% 0.20/0.51 tff(90,plain,
% 0.20/0.51 ((~p47(f5(c48, f8(f11(f13(c49, c50), c51), c52)), c53)) <=> (~p47(f5(c48, f8(f11(f13(c49, c50), c51), c52)), c53))),
% 0.20/0.51 inference(rewrite,[status(thm)],[])).
% 0.20/0.51 tff(91,axiom,(~p47(f5(c48, f8(f11(f13(c49, c50), c51), c52)), c53)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','not_p47_51')).
% 0.20/0.51 tff(92,plain,
% 0.20/0.51 (~p47(f5(c48, f8(f11(f13(c49, c50), c51), c52)), c53)),
% 0.20/0.51 inference(modus_ponens,[status(thm)],[91, 90])).
% 0.20/0.51 tff(93,plain,
% 0.20/0.51 (((~![X142: $i, X140: $i, X141: $i, X139: $i] : (p47(f5(c48, f8(f11(f13(c49, X139), X141), X142)), X140) | (~p47(X139, X140)))) | (p47(f5(c48, f8(f11(f13(c49, c50), c51), c52)), c53) | (~p47(c50, c53)))) <=> ((~![X142: $i, X140: $i, X141: $i, X139: $i] : (p47(f5(c48, f8(f11(f13(c49, X139), X141), X142)), X140) | (~p47(X139, X140)))) | p47(f5(c48, f8(f11(f13(c49, c50), c51), c52)), c53) | (~p47(c50, c53)))),
% 0.20/0.51 inference(rewrite,[status(thm)],[])).
% 0.20/0.51 tff(94,plain,
% 0.20/0.51 ((~![X142: $i, X140: $i, X141: $i, X139: $i] : (p47(f5(c48, f8(f11(f13(c49, X139), X141), X142)), X140) | (~p47(X139, X140)))) | (p47(f5(c48, f8(f11(f13(c49, c50), c51), c52)), c53) | (~p47(c50, c53)))),
% 0.20/0.51 inference(quant_inst,[status(thm)],[])).
% 0.20/0.51 tff(95,plain,
% 0.20/0.51 ((~![X142: $i, X140: $i, X141: $i, X139: $i] : (p47(f5(c48, f8(f11(f13(c49, X139), X141), X142)), X140) | (~p47(X139, X140)))) | p47(f5(c48, f8(f11(f13(c49, c50), c51), c52)), c53) | (~p47(c50, c53))),
% 0.20/0.51 inference(modus_ponens,[status(thm)],[94, 93])).
% 0.20/0.51 tff(96,plain,
% 0.20/0.51 (~p47(c50, c53)),
% 0.20/0.51 inference(unit_resolution,[status(thm)],[95, 92, 89])).
% 0.20/0.51 tff(97,plain,
% 0.20/0.51 (^[X57: $i, X59: $i, X60: $i, X61: $i, X58: $i] : refl(((~p47(f20(f22(f24(f26(c56, X57), X58), X59), X60), X61)) | p47(X57, X61)) <=> ((~p47(f20(f22(f24(f26(c56, X57), X58), X59), X60), X61)) | p47(X57, X61)))),
% 0.20/0.51 inference(bind,[status(th)],[])).
% 0.20/0.51 tff(98,plain,
% 0.20/0.51 (![X57: $i, X59: $i, X60: $i, X61: $i, X58: $i] : ((~p47(f20(f22(f24(f26(c56, X57), X58), X59), X60), X61)) | p47(X57, X61)) <=> ![X57: $i, X59: $i, X60: $i, X61: $i, X58: $i] : ((~p47(f20(f22(f24(f26(c56, X57), X58), X59), X60), X61)) | p47(X57, X61))),
% 0.20/0.51 inference(quant_intro,[status(thm)],[97])).
% 0.20/0.51 tff(99,plain,
% 0.20/0.51 (![X57: $i, X59: $i, X60: $i, X61: $i, X58: $i] : ((~p47(f20(f22(f24(f26(c56, X57), X58), X59), X60), X61)) | p47(X57, X61)) <=> ![X57: $i, X59: $i, X60: $i, X61: $i, X58: $i] : ((~p47(f20(f22(f24(f26(c56, X57), X58), X59), X60), X61)) | p47(X57, X61))),
% 0.20/0.51 inference(rewrite,[status(thm)],[])).
% 0.20/0.51 tff(100,plain,
% 0.20/0.51 (^[X57: $i, X59: $i, X60: $i, X61: $i, X58: $i] : rewrite((p47(X57, X61) | (~p47(f20(f22(f24(f26(c56, X57), X58), X59), X60), X61))) <=> ((~p47(f20(f22(f24(f26(c56, X57), X58), X59), X60), X61)) | p47(X57, X61)))),
% 0.20/0.51 inference(bind,[status(th)],[])).
% 0.20/0.51 tff(101,plain,
% 0.20/0.51 (![X57: $i, X59: $i, X60: $i, X61: $i, X58: $i] : (p47(X57, X61) | (~p47(f20(f22(f24(f26(c56, X57), X58), X59), X60), X61))) <=> ![X57: $i, X59: $i, X60: $i, X61: $i, X58: $i] : ((~p47(f20(f22(f24(f26(c56, X57), X58), X59), X60), X61)) | p47(X57, X61))),
% 0.20/0.51 inference(quant_intro,[status(thm)],[100])).
% 0.20/0.51 tff(102,axiom,(![X57: $i, X59: $i, X60: $i, X61: $i, X58: $i] : (p47(X57, X61) | (~p47(f20(f22(f24(f26(c56, X57), X58), X59), X60), X61)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','p47_75')).
% 0.20/0.51 tff(103,plain,
% 0.20/0.51 (![X57: $i, X59: $i, X60: $i, X61: $i, X58: $i] : ((~p47(f20(f22(f24(f26(c56, X57), X58), X59), X60), X61)) | p47(X57, X61))),
% 0.20/0.51 inference(modus_ponens,[status(thm)],[102, 101])).
% 0.20/0.51 tff(104,plain,
% 0.20/0.51 (![X57: $i, X59: $i, X60: $i, X61: $i, X58: $i] : ((~p47(f20(f22(f24(f26(c56, X57), X58), X59), X60), X61)) | p47(X57, X61))),
% 0.20/0.51 inference(modus_ponens,[status(thm)],[103, 99])).
% 0.20/0.51 tff(105,plain,(
% 0.20/0.51 ![X57: $i, X59: $i, X60: $i, X61: $i, X58: $i] : ((~p47(f20(f22(f24(f26(c56, X57), X58), X59), X60), X61)) | p47(X57, X61))),
% 0.20/0.51 inference(skolemize,[status(sab)],[104])).
% 0.20/0.51 tff(106,plain,
% 0.20/0.51 (![X57: $i, X59: $i, X60: $i, X61: $i, X58: $i] : ((~p47(f20(f22(f24(f26(c56, X57), X58), X59), X60), X61)) | p47(X57, X61))),
% 0.20/0.51 inference(modus_ponens,[status(thm)],[105, 98])).
% 0.20/0.51 tff(107,plain,
% 0.20/0.51 (((~![X57: $i, X59: $i, X60: $i, X61: $i, X58: $i] : ((~p47(f20(f22(f24(f26(c56, X57), X58), X59), X60), X61)) | p47(X57, X61))) | ((~p47(f20(f22(f24(f26(c56, c50), c51), c52), c55), c53)) | p47(c50, c53))) <=> ((~![X57: $i, X59: $i, X60: $i, X61: $i, X58: $i] : ((~p47(f20(f22(f24(f26(c56, X57), X58), X59), X60), X61)) | p47(X57, X61))) | (~p47(f20(f22(f24(f26(c56, c50), c51), c52), c55), c53)) | p47(c50, c53))),
% 0.20/0.51 inference(rewrite,[status(thm)],[])).
% 0.20/0.51 tff(108,plain,
% 0.20/0.51 ((~![X57: $i, X59: $i, X60: $i, X61: $i, X58: $i] : ((~p47(f20(f22(f24(f26(c56, X57), X58), X59), X60), X61)) | p47(X57, X61))) | ((~p47(f20(f22(f24(f26(c56, c50), c51), c52), c55), c53)) | p47(c50, c53))),
% 0.20/0.51 inference(quant_inst,[status(thm)],[])).
% 0.20/0.51 tff(109,plain,
% 0.20/0.51 ((~![X57: $i, X59: $i, X60: $i, X61: $i, X58: $i] : ((~p47(f20(f22(f24(f26(c56, X57), X58), X59), X60), X61)) | p47(X57, X61))) | (~p47(f20(f22(f24(f26(c56, c50), c51), c52), c55), c53)) | p47(c50, c53)),
% 0.20/0.51 inference(modus_ponens,[status(thm)],[108, 107])).
% 0.20/0.51 tff(110,plain,
% 0.20/0.51 ($false),
% 0.20/0.51 inference(unit_resolution,[status(thm)],[109, 106, 96, 82])).
% 0.20/0.51 % SZS output end Proof
% 0.20/0.51 % E exiting
%------------------------------------------------------------------------------