%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : SYN686-1 : TPTP v9.0.0. Released v2.5.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n006.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 0.18s 0.41s
% Output : Proof 0.18s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.11 % Problem : SYN686-1 : TPTP v9.0.0. Released v2.5.0.
% 0.06/0.11 % Command : run_E %s %d THM
% 0.12/0.32 % Computer : n006.cluster.edu
% 0.12/0.32 % Model : x86_64 x86_64
% 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.32 % Memory : 8042.1875MB
% 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.32 % CPULimit : 300
% 0.12/0.32 % WCLimit : 300
% 0.12/0.32 % DateTime : Fri Jun 20 12:39:20 EDT 2025
% 0.12/0.32 % CPUTime :
% 0.18/0.41 % SZS status Unsatisfiable
% 0.18/0.41 % SZS output start Proof
% 0.18/0.41 tff(p4_type, type, (
% 0.18/0.41 p4: ( $i * $i ) > $o)).
% 0.18/0.41 tff(c41_type, type, (
% 0.18/0.41 c41: $i)).
% 0.18/0.41 tff(p9_type, type, (
% 0.18/0.41 p9: ( $i * $i ) > $o)).
% 0.18/0.41 tff(f10_type, type, (
% 0.18/0.41 f10: ( $i * $i ) > $i)).
% 0.18/0.41 tff(c35_type, type, (
% 0.18/0.41 c35: $i)).
% 0.18/0.41 tff(f12_type, type, (
% 0.18/0.41 f12: ( $i * $i ) > $i)).
% 0.18/0.41 tff(f7_type, type, (
% 0.18/0.41 f7: ( $i * $i ) > $i)).
% 0.18/0.41 tff(c34_type, type, (
% 0.18/0.41 c34: $i)).
% 0.18/0.41 tff(c33_type, type, (
% 0.18/0.41 c33: $i)).
% 0.18/0.41 tff(c39_type, type, (
% 0.18/0.41 c39: $i)).
% 0.18/0.41 tff(c37_type, type, (
% 0.18/0.41 c37: $i)).
% 0.18/0.41 tff(c36_type, type, (
% 0.18/0.41 c36: $i)).
% 0.18/0.41 tff(p8_type, type, (
% 0.18/0.41 p8: ( $i * $i ) > $o)).
% 0.18/0.41 tff(p11_type, type, (
% 0.18/0.41 p11: ( $i * $i ) > $o)).
% 0.18/0.41 tff(p3_type, type, (
% 0.18/0.41 p3: ( $i * $i ) > $o)).
% 0.18/0.41 tff(f5_type, type, (
% 0.18/0.41 f5: ( $i * $i ) > $i)).
% 0.18/0.41 tff(c32_type, type, (
% 0.18/0.41 c32: $i)).
% 0.18/0.41 tff(p2_type, type, (
% 0.18/0.41 p2: ( $i * $i ) > $o)).
% 0.18/0.41 tff(p30_type, type, (
% 0.18/0.41 p30: ( $i * $i ) > $o)).
% 0.18/0.41 tff(1,assumption,(~p11(c39, c39)), introduced(assumption)).
% 0.18/0.41 tff(2,plain,
% 0.18/0.41 (^[X0: $i] : refl(p11(X0, X0) <=> p11(X0, X0))),
% 0.18/0.41 inference(bind,[status(th)],[])).
% 0.18/0.41 tff(3,plain,
% 0.18/0.41 (![X0: $i] : p11(X0, X0) <=> ![X0: $i] : p11(X0, X0)),
% 0.18/0.41 inference(quant_intro,[status(thm)],[2])).
% 0.18/0.41 tff(4,plain,
% 0.18/0.41 (![X0: $i] : p11(X0, X0) <=> ![X0: $i] : p11(X0, X0)),
% 0.18/0.41 inference(rewrite,[status(thm)],[])).
% 0.18/0.41 tff(5,axiom,(![X0: $i] : p11(X0, X0)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','p11_1')).
% 0.18/0.41 tff(6,plain,
% 0.18/0.41 (![X0: $i] : p11(X0, X0)),
% 0.18/0.41 inference(modus_ponens,[status(thm)],[5, 4])).
% 0.18/0.41 tff(7,plain,(
% 0.18/0.41 ![X0: $i] : p11(X0, X0)),
% 0.18/0.41 inference(skolemize,[status(sab)],[6])).
% 0.18/0.41 tff(8,plain,
% 0.18/0.41 (![X0: $i] : p11(X0, X0)),
% 0.18/0.41 inference(modus_ponens,[status(thm)],[7, 3])).
% 0.18/0.41 tff(9,plain,
% 0.18/0.41 ((~![X0: $i] : p11(X0, X0)) | p11(c39, c39)),
% 0.18/0.41 inference(quant_inst,[status(thm)],[])).
% 0.18/0.41 tff(10,plain,
% 0.18/0.41 ($false),
% 0.18/0.41 inference(unit_resolution,[status(thm)],[9, 8, 1])).
% 0.18/0.41 tff(11,plain,(p11(c39, c39)), inference(lemma,lemma(discharge,[]))).
% 0.18/0.41 tff(12,plain,
% 0.18/0.41 (^[X96: $i, X97: $i, X95: $i, X94: $i] : refl(((~p3(X95, X97)) | (~p11(X94, X96)) | p8(f12(X94, X95), f12(X96, X97))) <=> ((~p3(X95, X97)) | (~p11(X94, X96)) | p8(f12(X94, X95), f12(X96, X97))))),
% 0.18/0.41 inference(bind,[status(th)],[])).
% 0.18/0.41 tff(13,plain,
% 0.18/0.41 (![X96: $i, X97: $i, X95: $i, X94: $i] : ((~p3(X95, X97)) | (~p11(X94, X96)) | p8(f12(X94, X95), f12(X96, X97))) <=> ![X96: $i, X97: $i, X95: $i, X94: $i] : ((~p3(X95, X97)) | (~p11(X94, X96)) | p8(f12(X94, X95), f12(X96, X97)))),
% 0.18/0.41 inference(quant_intro,[status(thm)],[12])).
% 0.18/0.41 tff(14,plain,
% 0.18/0.41 (![X96: $i, X97: $i, X95: $i, X94: $i] : ((~p3(X95, X97)) | (~p11(X94, X96)) | p8(f12(X94, X95), f12(X96, X97))) <=> ![X96: $i, X97: $i, X95: $i, X94: $i] : ((~p3(X95, X97)) | (~p11(X94, X96)) | p8(f12(X94, X95), f12(X96, X97)))),
% 0.18/0.41 inference(rewrite,[status(thm)],[])).
% 0.18/0.41 tff(15,plain,
% 0.18/0.41 (^[X96: $i, X97: $i, X95: $i, X94: $i] : trans(monotonicity(rewrite((p8(f12(X94, X95), f12(X96, X97)) | (~p11(X94, X96))) <=> ((~p11(X94, X96)) | p8(f12(X94, X95), f12(X96, X97)))), (((p8(f12(X94, X95), f12(X96, X97)) | (~p11(X94, X96))) | (~p3(X95, X97))) <=> (((~p11(X94, X96)) | p8(f12(X94, X95), f12(X96, X97))) | (~p3(X95, X97))))), rewrite((((~p11(X94, X96)) | p8(f12(X94, X95), f12(X96, X97))) | (~p3(X95, X97))) <=> ((~p3(X95, X97)) | (~p11(X94, X96)) | p8(f12(X94, X95), f12(X96, X97)))), (((p8(f12(X94, X95), f12(X96, X97)) | (~p11(X94, X96))) | (~p3(X95, X97))) <=> ((~p3(X95, X97)) | (~p11(X94, X96)) | p8(f12(X94, X95), f12(X96, X97)))))),
% 0.18/0.41 inference(bind,[status(th)],[])).
% 0.18/0.41 tff(16,plain,
% 0.18/0.41 (![X96: $i, X97: $i, X95: $i, X94: $i] : ((p8(f12(X94, X95), f12(X96, X97)) | (~p11(X94, X96))) | (~p3(X95, X97))) <=> ![X96: $i, X97: $i, X95: $i, X94: $i] : ((~p3(X95, X97)) | (~p11(X94, X96)) | p8(f12(X94, X95), f12(X96, X97)))),
% 0.18/0.41 inference(quant_intro,[status(thm)],[15])).
% 0.18/0.41 tff(17,axiom,(![X96: $i, X97: $i, X95: $i, X94: $i] : ((p8(f12(X94, X95), f12(X96, X97)) | (~p11(X94, X96))) | (~p3(X95, X97)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','p8_51')).
% 0.18/0.41 tff(18,plain,
% 0.18/0.41 (![X96: $i, X97: $i, X95: $i, X94: $i] : ((~p3(X95, X97)) | (~p11(X94, X96)) | p8(f12(X94, X95), f12(X96, X97)))),
% 0.18/0.42 inference(modus_ponens,[status(thm)],[17, 16])).
% 0.18/0.42 tff(19,plain,
% 0.18/0.42 (![X96: $i, X97: $i, X95: $i, X94: $i] : ((~p3(X95, X97)) | (~p11(X94, X96)) | p8(f12(X94, X95), f12(X96, X97)))),
% 0.18/0.42 inference(modus_ponens,[status(thm)],[18, 14])).
% 0.18/0.42 tff(20,plain,(
% 0.18/0.42 ![X96: $i, X97: $i, X95: $i, X94: $i] : ((~p3(X95, X97)) | (~p11(X94, X96)) | p8(f12(X94, X95), f12(X96, X97)))),
% 0.18/0.42 inference(skolemize,[status(sab)],[19])).
% 0.18/0.42 tff(21,plain,
% 0.18/0.42 (![X96: $i, X97: $i, X95: $i, X94: $i] : ((~p3(X95, X97)) | (~p11(X94, X96)) | p8(f12(X94, X95), f12(X96, X97)))),
% 0.18/0.42 inference(modus_ponens,[status(thm)],[20, 13])).
% 0.18/0.42 tff(22,plain,
% 0.18/0.42 (p3(c36, f7(c33, c34)) <=> p3(c36, f7(c33, c34))),
% 0.18/0.42 inference(rewrite,[status(thm)],[])).
% 0.18/0.42 tff(23,axiom,(p3(c36, f7(c33, c34))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','p3_17')).
% 0.18/0.42 tff(24,plain,
% 0.18/0.42 (p3(c36, f7(c33, c34))),
% 0.18/0.42 inference(modus_ponens,[status(thm)],[23, 22])).
% 0.18/0.42 tff(25,plain,
% 0.18/0.42 (((~![X96: $i, X97: $i, X95: $i, X94: $i] : ((~p3(X95, X97)) | (~p11(X94, X96)) | p8(f12(X94, X95), f12(X96, X97)))) | ((~p3(c36, f7(c33, c34))) | p8(f12(c39, c36), f12(c39, f7(c33, c34))) | (~p11(c39, c39)))) <=> ((~![X96: $i, X97: $i, X95: $i, X94: $i] : ((~p3(X95, X97)) | (~p11(X94, X96)) | p8(f12(X94, X95), f12(X96, X97)))) | (~p3(c36, f7(c33, c34))) | p8(f12(c39, c36), f12(c39, f7(c33, c34))) | (~p11(c39, c39)))),
% 0.18/0.42 inference(rewrite,[status(thm)],[])).
% 0.18/0.42 tff(26,plain,
% 0.18/0.42 (((~p3(c36, f7(c33, c34))) | (~p11(c39, c39)) | p8(f12(c39, c36), f12(c39, f7(c33, c34)))) <=> ((~p3(c36, f7(c33, c34))) | p8(f12(c39, c36), f12(c39, f7(c33, c34))) | (~p11(c39, c39)))),
% 0.18/0.42 inference(rewrite,[status(thm)],[])).
% 0.18/0.42 tff(27,plain,
% 0.18/0.42 (((~![X96: $i, X97: $i, X95: $i, X94: $i] : ((~p3(X95, X97)) | (~p11(X94, X96)) | p8(f12(X94, X95), f12(X96, X97)))) | ((~p3(c36, f7(c33, c34))) | (~p11(c39, c39)) | p8(f12(c39, c36), f12(c39, f7(c33, c34))))) <=> ((~![X96: $i, X97: $i, X95: $i, X94: $i] : ((~p3(X95, X97)) | (~p11(X94, X96)) | p8(f12(X94, X95), f12(X96, X97)))) | ((~p3(c36, f7(c33, c34))) | p8(f12(c39, c36), f12(c39, f7(c33, c34))) | (~p11(c39, c39))))),
% 0.18/0.42 inference(monotonicity,[status(thm)],[26])).
% 0.18/0.42 tff(28,plain,
% 0.18/0.42 (((~![X96: $i, X97: $i, X95: $i, X94: $i] : ((~p3(X95, X97)) | (~p11(X94, X96)) | p8(f12(X94, X95), f12(X96, X97)))) | ((~p3(c36, f7(c33, c34))) | (~p11(c39, c39)) | p8(f12(c39, c36), f12(c39, f7(c33, c34))))) <=> ((~![X96: $i, X97: $i, X95: $i, X94: $i] : ((~p3(X95, X97)) | (~p11(X94, X96)) | p8(f12(X94, X95), f12(X96, X97)))) | (~p3(c36, f7(c33, c34))) | p8(f12(c39, c36), f12(c39, f7(c33, c34))) | (~p11(c39, c39)))),
% 0.18/0.42 inference(transitivity,[status(thm)],[27, 25])).
% 0.18/0.42 tff(29,plain,
% 0.18/0.42 ((~![X96: $i, X97: $i, X95: $i, X94: $i] : ((~p3(X95, X97)) | (~p11(X94, X96)) | p8(f12(X94, X95), f12(X96, X97)))) | ((~p3(c36, f7(c33, c34))) | (~p11(c39, c39)) | p8(f12(c39, c36), f12(c39, f7(c33, c34))))),
% 0.18/0.42 inference(quant_inst,[status(thm)],[])).
% 0.18/0.42 tff(30,plain,
% 0.18/0.42 ((~![X96: $i, X97: $i, X95: $i, X94: $i] : ((~p3(X95, X97)) | (~p11(X94, X96)) | p8(f12(X94, X95), f12(X96, X97)))) | (~p3(c36, f7(c33, c34))) | p8(f12(c39, c36), f12(c39, f7(c33, c34))) | (~p11(c39, c39))),
% 0.18/0.42 inference(modus_ponens,[status(thm)],[29, 28])).
% 0.18/0.42 tff(31,plain,
% 0.18/0.42 (p8(f12(c39, c36), f12(c39, f7(c33, c34))) | (~p11(c39, c39))),
% 0.18/0.42 inference(unit_resolution,[status(thm)],[30, 24, 21])).
% 0.18/0.42 tff(32,plain,
% 0.18/0.42 (p8(f12(c39, c36), f12(c39, f7(c33, c34)))),
% 0.18/0.42 inference(unit_resolution,[status(thm)],[31, 11])).
% 0.18/0.42 tff(33,assumption,(~p2(c32, c32)), introduced(assumption)).
% 0.18/0.42 tff(34,plain,
% 0.18/0.42 (^[X27: $i] : refl(p2(X27, X27) <=> p2(X27, X27))),
% 0.18/0.42 inference(bind,[status(th)],[])).
% 0.18/0.42 tff(35,plain,
% 0.18/0.42 (![X27: $i] : p2(X27, X27) <=> ![X27: $i] : p2(X27, X27)),
% 0.18/0.42 inference(quant_intro,[status(thm)],[34])).
% 0.18/0.42 tff(36,plain,
% 0.18/0.42 (![X27: $i] : p2(X27, X27) <=> ![X27: $i] : p2(X27, X27)),
% 0.18/0.42 inference(rewrite,[status(thm)],[])).
% 0.18/0.42 tff(37,axiom,(![X27: $i] : p2(X27, X27)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','p2_12')).
% 0.18/0.42 tff(38,plain,
% 0.18/0.42 (![X27: $i] : p2(X27, X27)),
% 0.18/0.42 inference(modus_ponens,[status(thm)],[37, 36])).
% 0.18/0.42 tff(39,plain,(
% 0.18/0.42 ![X27: $i] : p2(X27, X27)),
% 0.18/0.42 inference(skolemize,[status(sab)],[38])).
% 0.18/0.42 tff(40,plain,
% 0.18/0.42 (![X27: $i] : p2(X27, X27)),
% 0.18/0.42 inference(modus_ponens,[status(thm)],[39, 35])).
% 0.18/0.42 tff(41,plain,
% 0.18/0.42 ((~![X27: $i] : p2(X27, X27)) | p2(c32, c32)),
% 0.18/0.42 inference(quant_inst,[status(thm)],[])).
% 0.18/0.42 tff(42,plain,
% 0.18/0.42 ($false),
% 0.18/0.42 inference(unit_resolution,[status(thm)],[41, 40, 33])).
% 0.18/0.42 tff(43,plain,(p2(c32, c32)), inference(lemma,lemma(discharge,[]))).
% 0.18/0.42 tff(44,plain,
% 0.18/0.42 (^[X87: $i, X86: $i, X85: $i, X84: $i] : refl(((~p3(X85, X87)) | (~p2(X84, X86)) | p4(f5(X84, X85), f5(X86, X87))) <=> ((~p3(X85, X87)) | (~p2(X84, X86)) | p4(f5(X84, X85), f5(X86, X87))))),
% 0.18/0.42 inference(bind,[status(th)],[])).
% 0.18/0.42 tff(45,plain,
% 0.18/0.42 (![X87: $i, X86: $i, X85: $i, X84: $i] : ((~p3(X85, X87)) | (~p2(X84, X86)) | p4(f5(X84, X85), f5(X86, X87))) <=> ![X87: $i, X86: $i, X85: $i, X84: $i] : ((~p3(X85, X87)) | (~p2(X84, X86)) | p4(f5(X84, X85), f5(X86, X87)))),
% 0.18/0.42 inference(quant_intro,[status(thm)],[44])).
% 0.18/0.42 tff(46,plain,
% 0.18/0.42 (![X87: $i, X86: $i, X85: $i, X84: $i] : ((~p3(X85, X87)) | (~p2(X84, X86)) | p4(f5(X84, X85), f5(X86, X87))) <=> ![X87: $i, X86: $i, X85: $i, X84: $i] : ((~p3(X85, X87)) | (~p2(X84, X86)) | p4(f5(X84, X85), f5(X86, X87)))),
% 0.18/0.42 inference(rewrite,[status(thm)],[])).
% 0.18/0.42 tff(47,plain,
% 0.18/0.42 (^[X87: $i, X86: $i, X85: $i, X84: $i] : trans(monotonicity(rewrite((p4(f5(X84, X85), f5(X86, X87)) | (~p2(X84, X86))) <=> ((~p2(X84, X86)) | p4(f5(X84, X85), f5(X86, X87)))), (((p4(f5(X84, X85), f5(X86, X87)) | (~p2(X84, X86))) | (~p3(X85, X87))) <=> (((~p2(X84, X86)) | p4(f5(X84, X85), f5(X86, X87))) | (~p3(X85, X87))))), rewrite((((~p2(X84, X86)) | p4(f5(X84, X85), f5(X86, X87))) | (~p3(X85, X87))) <=> ((~p3(X85, X87)) | (~p2(X84, X86)) | p4(f5(X84, X85), f5(X86, X87)))), (((p4(f5(X84, X85), f5(X86, X87)) | (~p2(X84, X86))) | (~p3(X85, X87))) <=> ((~p3(X85, X87)) | (~p2(X84, X86)) | p4(f5(X84, X85), f5(X86, X87)))))),
% 0.18/0.42 inference(bind,[status(th)],[])).
% 0.18/0.42 tff(48,plain,
% 0.18/0.42 (![X87: $i, X86: $i, X85: $i, X84: $i] : ((p4(f5(X84, X85), f5(X86, X87)) | (~p2(X84, X86))) | (~p3(X85, X87))) <=> ![X87: $i, X86: $i, X85: $i, X84: $i] : ((~p3(X85, X87)) | (~p2(X84, X86)) | p4(f5(X84, X85), f5(X86, X87)))),
% 0.18/0.42 inference(quant_intro,[status(thm)],[47])).
% 0.18/0.42 tff(49,axiom,(![X87: $i, X86: $i, X85: $i, X84: $i] : ((p4(f5(X84, X85), f5(X86, X87)) | (~p2(X84, X86))) | (~p3(X85, X87)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','p4_50')).
% 0.18/0.42 tff(50,plain,
% 0.18/0.42 (![X87: $i, X86: $i, X85: $i, X84: $i] : ((~p3(X85, X87)) | (~p2(X84, X86)) | p4(f5(X84, X85), f5(X86, X87)))),
% 0.18/0.42 inference(modus_ponens,[status(thm)],[49, 48])).
% 0.18/0.42 tff(51,plain,
% 0.18/0.42 (![X87: $i, X86: $i, X85: $i, X84: $i] : ((~p3(X85, X87)) | (~p2(X84, X86)) | p4(f5(X84, X85), f5(X86, X87)))),
% 0.18/0.42 inference(modus_ponens,[status(thm)],[50, 46])).
% 0.18/0.42 tff(52,plain,(
% 0.18/0.42 ![X87: $i, X86: $i, X85: $i, X84: $i] : ((~p3(X85, X87)) | (~p2(X84, X86)) | p4(f5(X84, X85), f5(X86, X87)))),
% 0.18/0.42 inference(skolemize,[status(sab)],[51])).
% 0.18/0.42 tff(53,plain,
% 0.18/0.42 (![X87: $i, X86: $i, X85: $i, X84: $i] : ((~p3(X85, X87)) | (~p2(X84, X86)) | p4(f5(X84, X85), f5(X86, X87)))),
% 0.18/0.42 inference(modus_ponens,[status(thm)],[52, 45])).
% 0.18/0.42 tff(54,plain,
% 0.18/0.42 (((~![X87: $i, X86: $i, X85: $i, X84: $i] : ((~p3(X85, X87)) | (~p2(X84, X86)) | p4(f5(X84, X85), f5(X86, X87)))) | ((~p3(c36, f7(c33, c34))) | (~p2(c32, c32)) | p4(f5(c32, c36), f5(c32, f7(c33, c34))))) <=> ((~![X87: $i, X86: $i, X85: $i, X84: $i] : ((~p3(X85, X87)) | (~p2(X84, X86)) | p4(f5(X84, X85), f5(X86, X87)))) | (~p3(c36, f7(c33, c34))) | (~p2(c32, c32)) | p4(f5(c32, c36), f5(c32, f7(c33, c34))))),
% 0.18/0.42 inference(rewrite,[status(thm)],[])).
% 0.18/0.42 tff(55,plain,
% 0.18/0.42 ((~![X87: $i, X86: $i, X85: $i, X84: $i] : ((~p3(X85, X87)) | (~p2(X84, X86)) | p4(f5(X84, X85), f5(X86, X87)))) | ((~p3(c36, f7(c33, c34))) | (~p2(c32, c32)) | p4(f5(c32, c36), f5(c32, f7(c33, c34))))),
% 0.18/0.42 inference(quant_inst,[status(thm)],[])).
% 0.18/0.42 tff(56,plain,
% 0.18/0.42 ((~![X87: $i, X86: $i, X85: $i, X84: $i] : ((~p3(X85, X87)) | (~p2(X84, X86)) | p4(f5(X84, X85), f5(X86, X87)))) | (~p3(c36, f7(c33, c34))) | (~p2(c32, c32)) | p4(f5(c32, c36), f5(c32, f7(c33, c34)))),
% 0.18/0.42 inference(modus_ponens,[status(thm)],[55, 54])).
% 0.18/0.42 tff(57,plain,
% 0.18/0.42 ((~p2(c32, c32)) | p4(f5(c32, c36), f5(c32, f7(c33, c34)))),
% 0.18/0.42 inference(unit_resolution,[status(thm)],[56, 24, 53])).
% 0.18/0.42 tff(58,plain,
% 0.18/0.42 (p4(f5(c32, c36), f5(c32, f7(c33, c34)))),
% 0.18/0.42 inference(unit_resolution,[status(thm)],[57, 43])).
% 0.18/0.42 tff(59,plain,
% 0.18/0.42 (^[X81: $i, X82: $i, X83: $i] : refl(((~p4(X81, X83)) | (~p4(X81, X82)) | p4(X82, X83)) <=> ((~p4(X81, X83)) | (~p4(X81, X82)) | p4(X82, X83)))),
% 0.18/0.42 inference(bind,[status(th)],[])).
% 0.18/0.42 tff(60,plain,
% 0.18/0.42 (![X81: $i, X82: $i, X83: $i] : ((~p4(X81, X83)) | (~p4(X81, X82)) | p4(X82, X83)) <=> ![X81: $i, X82: $i, X83: $i] : ((~p4(X81, X83)) | (~p4(X81, X82)) | p4(X82, X83))),
% 0.18/0.42 inference(quant_intro,[status(thm)],[59])).
% 0.18/0.42 tff(61,plain,
% 0.18/0.42 (![X81: $i, X82: $i, X83: $i] : ((~p4(X81, X83)) | (~p4(X81, X82)) | p4(X82, X83)) <=> ![X81: $i, X82: $i, X83: $i] : ((~p4(X81, X83)) | (~p4(X81, X82)) | p4(X82, X83))),
% 0.18/0.42 inference(rewrite,[status(thm)],[])).
% 0.18/0.42 tff(62,plain,
% 0.18/0.42 (^[X81: $i, X82: $i, X83: $i] : trans(monotonicity(rewrite((p4(X82, X83) | (~p4(X81, X82))) <=> ((~p4(X81, X82)) | p4(X82, X83))), (((p4(X82, X83) | (~p4(X81, X82))) | (~p4(X81, X83))) <=> (((~p4(X81, X82)) | p4(X82, X83)) | (~p4(X81, X83))))), rewrite((((~p4(X81, X82)) | p4(X82, X83)) | (~p4(X81, X83))) <=> ((~p4(X81, X83)) | (~p4(X81, X82)) | p4(X82, X83))), (((p4(X82, X83) | (~p4(X81, X82))) | (~p4(X81, X83))) <=> ((~p4(X81, X83)) | (~p4(X81, X82)) | p4(X82, X83))))),
% 0.18/0.42 inference(bind,[status(th)],[])).
% 0.18/0.42 tff(63,plain,
% 0.18/0.42 (![X81: $i, X82: $i, X83: $i] : ((p4(X82, X83) | (~p4(X81, X82))) | (~p4(X81, X83))) <=> ![X81: $i, X82: $i, X83: $i] : ((~p4(X81, X83)) | (~p4(X81, X82)) | p4(X82, X83))),
% 0.18/0.42 inference(quant_intro,[status(thm)],[62])).
% 0.18/0.42 tff(64,axiom,(![X81: $i, X82: $i, X83: $i] : ((p4(X82, X83) | (~p4(X81, X82))) | (~p4(X81, X83)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','p4_27')).
% 0.18/0.42 tff(65,plain,
% 0.18/0.42 (![X81: $i, X82: $i, X83: $i] : ((~p4(X81, X83)) | (~p4(X81, X82)) | p4(X82, X83))),
% 0.18/0.42 inference(modus_ponens,[status(thm)],[64, 63])).
% 0.18/0.42 tff(66,plain,
% 0.18/0.42 (![X81: $i, X82: $i, X83: $i] : ((~p4(X81, X83)) | (~p4(X81, X82)) | p4(X82, X83))),
% 0.18/0.42 inference(modus_ponens,[status(thm)],[65, 61])).
% 0.18/0.42 tff(67,plain,(
% 0.18/0.42 ![X81: $i, X82: $i, X83: $i] : ((~p4(X81, X83)) | (~p4(X81, X82)) | p4(X82, X83))),
% 0.18/0.42 inference(skolemize,[status(sab)],[66])).
% 0.18/0.42 tff(68,plain,
% 0.18/0.42 (![X81: $i, X82: $i, X83: $i] : ((~p4(X81, X83)) | (~p4(X81, X82)) | p4(X82, X83))),
% 0.18/0.42 inference(modus_ponens,[status(thm)],[67, 60])).
% 0.18/0.42 tff(69,plain,
% 0.18/0.42 (p4(f5(c32, c36), c37) <=> p4(f5(c32, c36), c37)),
% 0.18/0.42 inference(rewrite,[status(thm)],[])).
% 0.18/0.42 tff(70,axiom,(p4(f5(c32, c36), c37)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','p4_19')).
% 0.18/0.42 tff(71,plain,
% 0.18/0.42 (p4(f5(c32, c36), c37)),
% 0.18/0.42 inference(modus_ponens,[status(thm)],[70, 69])).
% 0.18/0.42 tff(72,plain,
% 0.18/0.42 (((~![X81: $i, X82: $i, X83: $i] : ((~p4(X81, X83)) | (~p4(X81, X82)) | p4(X82, X83))) | ((~p4(f5(c32, c36), c37)) | (~p4(f5(c32, c36), f5(c32, f7(c33, c34)))) | p4(f5(c32, f7(c33, c34)), c37))) <=> ((~![X81: $i, X82: $i, X83: $i] : ((~p4(X81, X83)) | (~p4(X81, X82)) | p4(X82, X83))) | (~p4(f5(c32, c36), c37)) | (~p4(f5(c32, c36), f5(c32, f7(c33, c34)))) | p4(f5(c32, f7(c33, c34)), c37))),
% 0.18/0.42 inference(rewrite,[status(thm)],[])).
% 0.18/0.42 tff(73,plain,
% 0.18/0.42 ((~![X81: $i, X82: $i, X83: $i] : ((~p4(X81, X83)) | (~p4(X81, X82)) | p4(X82, X83))) | ((~p4(f5(c32, c36), c37)) | (~p4(f5(c32, c36), f5(c32, f7(c33, c34)))) | p4(f5(c32, f7(c33, c34)), c37))),
% 0.18/0.42 inference(quant_inst,[status(thm)],[])).
% 0.18/0.42 tff(74,plain,
% 0.18/0.42 ((~![X81: $i, X82: $i, X83: $i] : ((~p4(X81, X83)) | (~p4(X81, X82)) | p4(X82, X83))) | (~p4(f5(c32, c36), c37)) | (~p4(f5(c32, c36), f5(c32, f7(c33, c34)))) | p4(f5(c32, f7(c33, c34)), c37)),
% 0.18/0.42 inference(modus_ponens,[status(thm)],[73, 72])).
% 0.18/0.42 tff(75,plain,
% 0.18/0.42 (p4(f5(c32, f7(c33, c34)), c37)),
% 0.18/0.42 inference(unit_resolution,[status(thm)],[74, 71, 68, 58])).
% 0.18/0.42 tff(76,plain,
% 0.18/0.42 (p4(f5(c32, f7(c33, c34)), c35) <=> p4(f5(c32, f7(c33, c34)), c35)),
% 0.18/0.42 inference(rewrite,[status(thm)],[])).
% 0.18/0.42 tff(77,axiom,(p4(f5(c32, f7(c33, c34)), c35)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','p4_20')).
% 0.18/0.42 tff(78,plain,
% 0.18/0.42 (p4(f5(c32, f7(c33, c34)), c35)),
% 0.18/0.42 inference(modus_ponens,[status(thm)],[77, 76])).
% 0.18/0.42 tff(79,plain,
% 0.18/0.42 (((~![X81: $i, X82: $i, X83: $i] : ((~p4(X81, X83)) | (~p4(X81, X82)) | p4(X82, X83))) | ((~p4(f5(c32, f7(c33, c34)), c35)) | (~p4(f5(c32, f7(c33, c34)), c37)) | p4(c37, c35))) <=> ((~![X81: $i, X82: $i, X83: $i] : ((~p4(X81, X83)) | (~p4(X81, X82)) | p4(X82, X83))) | (~p4(f5(c32, f7(c33, c34)), c35)) | (~p4(f5(c32, f7(c33, c34)), c37)) | p4(c37, c35))),
% 0.18/0.42 inference(rewrite,[status(thm)],[])).
% 0.18/0.42 tff(80,plain,
% 0.18/0.42 ((~![X81: $i, X82: $i, X83: $i] : ((~p4(X81, X83)) | (~p4(X81, X82)) | p4(X82, X83))) | ((~p4(f5(c32, f7(c33, c34)), c35)) | (~p4(f5(c32, f7(c33, c34)), c37)) | p4(c37, c35))),
% 0.18/0.42 inference(quant_inst,[status(thm)],[])).
% 0.18/0.42 tff(81,plain,
% 0.18/0.42 ((~![X81: $i, X82: $i, X83: $i] : ((~p4(X81, X83)) | (~p4(X81, X82)) | p4(X82, X83))) | (~p4(f5(c32, f7(c33, c34)), c35)) | (~p4(f5(c32, f7(c33, c34)), c37)) | p4(c37, c35)),
% 0.18/0.42 inference(modus_ponens,[status(thm)],[80, 79])).
% 0.18/0.42 tff(82,plain,
% 0.18/0.42 (p4(c37, c35)),
% 0.18/0.42 inference(unit_resolution,[status(thm)],[81, 78, 68, 75])).
% 0.18/0.42 tff(83,plain,
% 0.18/0.42 (^[X105: $i, X107: $i, X106: $i, X108: $i] : refl(((~p8(X105, X107)) | (~p4(X106, X108)) | p9(f10(X105, X106), f10(X107, X108))) <=> ((~p8(X105, X107)) | (~p4(X106, X108)) | p9(f10(X105, X106), f10(X107, X108))))),
% 0.18/0.42 inference(bind,[status(th)],[])).
% 0.18/0.42 tff(84,plain,
% 0.18/0.42 (![X105: $i, X107: $i, X106: $i, X108: $i] : ((~p8(X105, X107)) | (~p4(X106, X108)) | p9(f10(X105, X106), f10(X107, X108))) <=> ![X105: $i, X107: $i, X106: $i, X108: $i] : ((~p8(X105, X107)) | (~p4(X106, X108)) | p9(f10(X105, X106), f10(X107, X108)))),
% 0.18/0.42 inference(quant_intro,[status(thm)],[83])).
% 0.18/0.42 tff(85,plain,
% 0.18/0.42 (![X105: $i, X107: $i, X106: $i, X108: $i] : ((~p8(X105, X107)) | (~p4(X106, X108)) | p9(f10(X105, X106), f10(X107, X108))) <=> ![X105: $i, X107: $i, X106: $i, X108: $i] : ((~p8(X105, X107)) | (~p4(X106, X108)) | p9(f10(X105, X106), f10(X107, X108)))),
% 0.18/0.42 inference(rewrite,[status(thm)],[])).
% 0.18/0.42 tff(86,plain,
% 0.18/0.42 (^[X105: $i, X107: $i, X106: $i, X108: $i] : trans(monotonicity(rewrite((p9(f10(X105, X106), f10(X107, X108)) | (~p4(X106, X108))) <=> ((~p4(X106, X108)) | p9(f10(X105, X106), f10(X107, X108)))), (((p9(f10(X105, X106), f10(X107, X108)) | (~p4(X106, X108))) | (~p8(X105, X107))) <=> (((~p4(X106, X108)) | p9(f10(X105, X106), f10(X107, X108))) | (~p8(X105, X107))))), rewrite((((~p4(X106, X108)) | p9(f10(X105, X106), f10(X107, X108))) | (~p8(X105, X107))) <=> ((~p8(X105, X107)) | (~p4(X106, X108)) | p9(f10(X105, X106), f10(X107, X108)))), (((p9(f10(X105, X106), f10(X107, X108)) | (~p4(X106, X108))) | (~p8(X105, X107))) <=> ((~p8(X105, X107)) | (~p4(X106, X108)) | p9(f10(X105, X106), f10(X107, X108)))))),
% 0.18/0.42 inference(bind,[status(th)],[])).
% 0.18/0.42 tff(87,plain,
% 0.18/0.42 (![X105: $i, X107: $i, X106: $i, X108: $i] : ((p9(f10(X105, X106), f10(X107, X108)) | (~p4(X106, X108))) | (~p8(X105, X107))) <=> ![X105: $i, X107: $i, X106: $i, X108: $i] : ((~p8(X105, X107)) | (~p4(X106, X108)) | p9(f10(X105, X106), f10(X107, X108)))),
% 0.18/0.42 inference(quant_intro,[status(thm)],[86])).
% 0.18/0.42 tff(88,axiom,(![X105: $i, X107: $i, X106: $i, X108: $i] : ((p9(f10(X105, X106), f10(X107, X108)) | (~p4(X106, X108))) | (~p8(X105, X107)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','p9_41')).
% 0.18/0.42 tff(89,plain,
% 0.18/0.42 (![X105: $i, X107: $i, X106: $i, X108: $i] : ((~p8(X105, X107)) | (~p4(X106, X108)) | p9(f10(X105, X106), f10(X107, X108)))),
% 0.18/0.42 inference(modus_ponens,[status(thm)],[88, 87])).
% 0.18/0.42 tff(90,plain,
% 0.18/0.42 (![X105: $i, X107: $i, X106: $i, X108: $i] : ((~p8(X105, X107)) | (~p4(X106, X108)) | p9(f10(X105, X106), f10(X107, X108)))),
% 0.18/0.42 inference(modus_ponens,[status(thm)],[89, 85])).
% 0.18/0.42 tff(91,plain,(
% 0.18/0.42 ![X105: $i, X107: $i, X106: $i, X108: $i] : ((~p8(X105, X107)) | (~p4(X106, X108)) | p9(f10(X105, X106), f10(X107, X108)))),
% 0.18/0.42 inference(skolemize,[status(sab)],[90])).
% 0.18/0.42 tff(92,plain,
% 0.18/0.42 (![X105: $i, X107: $i, X106: $i, X108: $i] : ((~p8(X105, X107)) | (~p4(X106, X108)) | p9(f10(X105, X106), f10(X107, X108)))),
% 0.18/0.43 inference(modus_ponens,[status(thm)],[91, 84])).
% 0.18/0.43 tff(93,plain,
% 0.18/0.43 (((~![X105: $i, X107: $i, X106: $i, X108: $i] : ((~p8(X105, X107)) | (~p4(X106, X108)) | p9(f10(X105, X106), f10(X107, X108)))) | ((~p8(f12(c39, c36), f12(c39, f7(c33, c34)))) | (~p4(c37, c35)) | p9(f10(f12(c39, c36), c37), f10(f12(c39, f7(c33, c34)), c35)))) <=> ((~![X105: $i, X107: $i, X106: $i, X108: $i] : ((~p8(X105, X107)) | (~p4(X106, X108)) | p9(f10(X105, X106), f10(X107, X108)))) | (~p8(f12(c39, c36), f12(c39, f7(c33, c34)))) | (~p4(c37, c35)) | p9(f10(f12(c39, c36), c37), f10(f12(c39, f7(c33, c34)), c35)))),
% 0.18/0.43 inference(rewrite,[status(thm)],[])).
% 0.18/0.43 tff(94,plain,
% 0.18/0.43 ((~![X105: $i, X107: $i, X106: $i, X108: $i] : ((~p8(X105, X107)) | (~p4(X106, X108)) | p9(f10(X105, X106), f10(X107, X108)))) | ((~p8(f12(c39, c36), f12(c39, f7(c33, c34)))) | (~p4(c37, c35)) | p9(f10(f12(c39, c36), c37), f10(f12(c39, f7(c33, c34)), c35)))),
% 0.18/0.43 inference(quant_inst,[status(thm)],[])).
% 0.18/0.43 tff(95,plain,
% 0.18/0.43 ((~![X105: $i, X107: $i, X106: $i, X108: $i] : ((~p8(X105, X107)) | (~p4(X106, X108)) | p9(f10(X105, X106), f10(X107, X108)))) | (~p8(f12(c39, c36), f12(c39, f7(c33, c34)))) | (~p4(c37, c35)) | p9(f10(f12(c39, c36), c37), f10(f12(c39, f7(c33, c34)), c35))),
% 0.18/0.43 inference(modus_ponens,[status(thm)],[94, 93])).
% 0.18/0.43 tff(96,plain,
% 0.18/0.43 ((~p8(f12(c39, c36), f12(c39, f7(c33, c34)))) | (~p4(c37, c35)) | p9(f10(f12(c39, c36), c37), f10(f12(c39, f7(c33, c34)), c35))),
% 0.18/0.43 inference(unit_resolution,[status(thm)],[95, 92])).
% 0.18/0.43 tff(97,plain,
% 0.18/0.43 (p9(f10(f12(c39, c36), c37), f10(f12(c39, f7(c33, c34)), c35))),
% 0.18/0.43 inference(unit_resolution,[status(thm)],[96, 82, 32])).
% 0.18/0.43 tff(98,plain,
% 0.18/0.43 (^[X68: $i, X70: $i, X69: $i, X71: $i] : refl(((~p30(X70, X71)) | (~p9(X70, X68)) | (~p4(X71, X69)) | p30(X68, X69)) <=> ((~p30(X70, X71)) | (~p9(X70, X68)) | (~p4(X71, X69)) | p30(X68, X69)))),
% 0.18/0.43 inference(bind,[status(th)],[])).
% 0.18/0.43 tff(99,plain,
% 0.18/0.43 (![X68: $i, X70: $i, X69: $i, X71: $i] : ((~p30(X70, X71)) | (~p9(X70, X68)) | (~p4(X71, X69)) | p30(X68, X69)) <=> ![X68: $i, X70: $i, X69: $i, X71: $i] : ((~p30(X70, X71)) | (~p9(X70, X68)) | (~p4(X71, X69)) | p30(X68, X69))),
% 0.18/0.43 inference(quant_intro,[status(thm)],[98])).
% 0.18/0.43 tff(100,plain,
% 0.18/0.43 (![X68: $i, X70: $i, X69: $i, X71: $i] : ((~p30(X70, X71)) | (~p9(X70, X68)) | (~p4(X71, X69)) | p30(X68, X69)) <=> ![X68: $i, X70: $i, X69: $i, X71: $i] : ((~p30(X70, X71)) | (~p9(X70, X68)) | (~p4(X71, X69)) | p30(X68, X69))),
% 0.18/0.43 inference(rewrite,[status(thm)],[])).
% 0.18/0.43 tff(101,plain,
% 0.18/0.43 (^[X68: $i, X70: $i, X69: $i, X71: $i] : trans(monotonicity(trans(monotonicity(rewrite((p30(X68, X69) | (~p4(X71, X69))) <=> ((~p4(X71, X69)) | p30(X68, X69))), (((p30(X68, X69) | (~p4(X71, X69))) | (~p9(X70, X68))) <=> (((~p4(X71, X69)) | p30(X68, X69)) | (~p9(X70, X68))))), rewrite((((~p4(X71, X69)) | p30(X68, X69)) | (~p9(X70, X68))) <=> ((~p9(X70, X68)) | (~p4(X71, X69)) | p30(X68, X69))), (((p30(X68, X69) | (~p4(X71, X69))) | (~p9(X70, X68))) <=> ((~p9(X70, X68)) | (~p4(X71, X69)) | p30(X68, X69)))), ((((p30(X68, X69) | (~p4(X71, X69))) | (~p9(X70, X68))) | (~p30(X70, X71))) <=> (((~p9(X70, X68)) | (~p4(X71, X69)) | p30(X68, X69)) | (~p30(X70, X71))))), rewrite((((~p9(X70, X68)) | (~p4(X71, X69)) | p30(X68, X69)) | (~p30(X70, X71))) <=> ((~p30(X70, X71)) | (~p9(X70, X68)) | (~p4(X71, X69)) | p30(X68, X69))), ((((p30(X68, X69) | (~p4(X71, X69))) | (~p9(X70, X68))) | (~p30(X70, X71))) <=> ((~p30(X70, X71)) | (~p9(X70, X68)) | (~p4(X71, X69)) | p30(X68, X69))))),
% 0.18/0.43 inference(bind,[status(th)],[])).
% 0.18/0.43 tff(102,plain,
% 0.18/0.43 (![X68: $i, X70: $i, X69: $i, X71: $i] : (((p30(X68, X69) | (~p4(X71, X69))) | (~p9(X70, X68))) | (~p30(X70, X71))) <=> ![X68: $i, X70: $i, X69: $i, X71: $i] : ((~p30(X70, X71)) | (~p9(X70, X68)) | (~p4(X71, X69)) | p30(X68, X69))),
% 0.18/0.43 inference(quant_intro,[status(thm)],[101])).
% 0.18/0.43 tff(103,axiom,(![X68: $i, X70: $i, X69: $i, X71: $i] : (((p30(X68, X69) | (~p4(X71, X69))) | (~p9(X70, X68))) | (~p30(X70, X71)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','p30_39')).
% 0.18/0.43 tff(104,plain,
% 0.18/0.43 (![X68: $i, X70: $i, X69: $i, X71: $i] : ((~p30(X70, X71)) | (~p9(X70, X68)) | (~p4(X71, X69)) | p30(X68, X69))),
% 0.18/0.43 inference(modus_ponens,[status(thm)],[103, 102])).
% 0.18/0.43 tff(105,plain,
% 0.18/0.43 (![X68: $i, X70: $i, X69: $i, X71: $i] : ((~p30(X70, X71)) | (~p9(X70, X68)) | (~p4(X71, X69)) | p30(X68, X69))),
% 0.18/0.43 inference(modus_ponens,[status(thm)],[104, 100])).
% 0.18/0.43 tff(106,plain,(
% 0.18/0.43 ![X68: $i, X70: $i, X69: $i, X71: $i] : ((~p30(X70, X71)) | (~p9(X70, X68)) | (~p4(X71, X69)) | p30(X68, X69))),
% 0.18/0.43 inference(skolemize,[status(sab)],[105])).
% 0.18/0.43 tff(107,plain,
% 0.18/0.43 (![X68: $i, X70: $i, X69: $i, X71: $i] : ((~p30(X70, X71)) | (~p9(X70, X68)) | (~p4(X71, X69)) | p30(X68, X69))),
% 0.18/0.43 inference(modus_ponens,[status(thm)],[106, 99])).
% 0.18/0.43 tff(108,plain,
% 0.18/0.43 ((~p30(f10(f12(c39, f7(c33, c34)), c35), c41)) <=> (~p30(f10(f12(c39, f7(c33, c34)), c35), c41))),
% 0.18/0.43 inference(rewrite,[status(thm)],[])).
% 0.18/0.43 tff(109,axiom,(~p30(f10(f12(c39, f7(c33, c34)), c35), c41)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','not_p30_22')).
% 0.18/0.43 tff(110,plain,
% 0.18/0.43 (~p30(f10(f12(c39, f7(c33, c34)), c35), c41)),
% 0.18/0.43 inference(modus_ponens,[status(thm)],[109, 108])).
% 0.18/0.43 tff(111,plain,
% 0.18/0.43 (p30(f10(f12(c39, c36), c37), c41) <=> p30(f10(f12(c39, c36), c37), c41)),
% 0.18/0.43 inference(rewrite,[status(thm)],[])).
% 0.18/0.43 tff(112,axiom,(p30(f10(f12(c39, c36), c37), c41)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','p30_21')).
% 0.18/0.43 tff(113,plain,
% 0.18/0.43 (p30(f10(f12(c39, c36), c37), c41)),
% 0.18/0.43 inference(modus_ponens,[status(thm)],[112, 111])).
% 0.18/0.43 tff(114,plain,
% 0.18/0.43 (((~![X68: $i, X70: $i, X69: $i, X71: $i] : ((~p30(X70, X71)) | (~p9(X70, X68)) | (~p4(X71, X69)) | p30(X68, X69))) | (p30(f10(f12(c39, f7(c33, c34)), c35), c41) | (~p9(f10(f12(c39, c36), c37), f10(f12(c39, f7(c33, c34)), c35))) | (~p30(f10(f12(c39, c36), c37), c41)) | (~p4(c41, c41)))) <=> ((~![X68: $i, X70: $i, X69: $i, X71: $i] : ((~p30(X70, X71)) | (~p9(X70, X68)) | (~p4(X71, X69)) | p30(X68, X69))) | p30(f10(f12(c39, f7(c33, c34)), c35), c41) | (~p9(f10(f12(c39, c36), c37), f10(f12(c39, f7(c33, c34)), c35))) | (~p30(f10(f12(c39, c36), c37), c41)) | (~p4(c41, c41)))),
% 0.18/0.43 inference(rewrite,[status(thm)],[])).
% 0.18/0.43 tff(115,plain,
% 0.18/0.43 (((~p30(f10(f12(c39, c36), c37), c41)) | (~p9(f10(f12(c39, c36), c37), f10(f12(c39, f7(c33, c34)), c35))) | (~p4(c41, c41)) | p30(f10(f12(c39, f7(c33, c34)), c35), c41)) <=> (p30(f10(f12(c39, f7(c33, c34)), c35), c41) | (~p9(f10(f12(c39, c36), c37), f10(f12(c39, f7(c33, c34)), c35))) | (~p30(f10(f12(c39, c36), c37), c41)) | (~p4(c41, c41)))),
% 0.18/0.43 inference(rewrite,[status(thm)],[])).
% 0.18/0.43 tff(116,plain,
% 0.18/0.43 (((~![X68: $i, X70: $i, X69: $i, X71: $i] : ((~p30(X70, X71)) | (~p9(X70, X68)) | (~p4(X71, X69)) | p30(X68, X69))) | ((~p30(f10(f12(c39, c36), c37), c41)) | (~p9(f10(f12(c39, c36), c37), f10(f12(c39, f7(c33, c34)), c35))) | (~p4(c41, c41)) | p30(f10(f12(c39, f7(c33, c34)), c35), c41))) <=> ((~![X68: $i, X70: $i, X69: $i, X71: $i] : ((~p30(X70, X71)) | (~p9(X70, X68)) | (~p4(X71, X69)) | p30(X68, X69))) | (p30(f10(f12(c39, f7(c33, c34)), c35), c41) | (~p9(f10(f12(c39, c36), c37), f10(f12(c39, f7(c33, c34)), c35))) | (~p30(f10(f12(c39, c36), c37), c41)) | (~p4(c41, c41))))),
% 0.18/0.43 inference(monotonicity,[status(thm)],[115])).
% 0.18/0.43 tff(117,plain,
% 0.18/0.43 (((~![X68: $i, X70: $i, X69: $i, X71: $i] : ((~p30(X70, X71)) | (~p9(X70, X68)) | (~p4(X71, X69)) | p30(X68, X69))) | ((~p30(f10(f12(c39, c36), c37), c41)) | (~p9(f10(f12(c39, c36), c37), f10(f12(c39, f7(c33, c34)), c35))) | (~p4(c41, c41)) | p30(f10(f12(c39, f7(c33, c34)), c35), c41))) <=> ((~![X68: $i, X70: $i, X69: $i, X71: $i] : ((~p30(X70, X71)) | (~p9(X70, X68)) | (~p4(X71, X69)) | p30(X68, X69))) | p30(f10(f12(c39, f7(c33, c34)), c35), c41) | (~p9(f10(f12(c39, c36), c37), f10(f12(c39, f7(c33, c34)), c35))) | (~p30(f10(f12(c39, c36), c37), c41)) | (~p4(c41, c41)))),
% 0.18/0.43 inference(transitivity,[status(thm)],[116, 114])).
% 0.18/0.43 tff(118,plain,
% 0.18/0.43 ((~![X68: $i, X70: $i, X69: $i, X71: $i] : ((~p30(X70, X71)) | (~p9(X70, X68)) | (~p4(X71, X69)) | p30(X68, X69))) | ((~p30(f10(f12(c39, c36), c37), c41)) | (~p9(f10(f12(c39, c36), c37), f10(f12(c39, f7(c33, c34)), c35))) | (~p4(c41, c41)) | p30(f10(f12(c39, f7(c33, c34)), c35), c41))),
% 0.18/0.44 inference(quant_inst,[status(thm)],[])).
% 0.18/0.44 tff(119,plain,
% 0.18/0.44 ((~![X68: $i, X70: $i, X69: $i, X71: $i] : ((~p30(X70, X71)) | (~p9(X70, X68)) | (~p4(X71, X69)) | p30(X68, X69))) | p30(f10(f12(c39, f7(c33, c34)), c35), c41) | (~p9(f10(f12(c39, c36), c37), f10(f12(c39, f7(c33, c34)), c35))) | (~p30(f10(f12(c39, c36), c37), c41)) | (~p4(c41, c41))),
% 0.18/0.44 inference(modus_ponens,[status(thm)],[118, 117])).
% 0.18/0.44 tff(120,plain,
% 0.18/0.44 (~p4(c41, c41)),
% 0.18/0.44 inference(unit_resolution,[status(thm)],[119, 113, 110, 107, 97])).
% 0.18/0.44 tff(121,plain,
% 0.18/0.44 (^[X81: $i] : refl(p4(X81, X81) <=> p4(X81, X81))),
% 0.18/0.44 inference(bind,[status(th)],[])).
% 0.18/0.44 tff(122,plain,
% 0.18/0.44 (![X81: $i] : p4(X81, X81) <=> ![X81: $i] : p4(X81, X81)),
% 0.18/0.44 inference(quant_intro,[status(thm)],[121])).
% 0.18/0.44 tff(123,plain,
% 0.18/0.44 (![X81: $i] : p4(X81, X81) <=> ![X81: $i] : p4(X81, X81)),
% 0.18/0.44 inference(rewrite,[status(thm)],[])).
% 0.18/0.44 tff(124,axiom,(![X81: $i] : p4(X81, X81)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','p4_5')).
% 0.18/0.44 tff(125,plain,
% 0.18/0.44 (![X81: $i] : p4(X81, X81)),
% 0.18/0.44 inference(modus_ponens,[status(thm)],[124, 123])).
% 0.18/0.44 tff(126,plain,(
% 0.18/0.44 ![X81: $i] : p4(X81, X81)),
% 0.18/0.44 inference(skolemize,[status(sab)],[125])).
% 0.18/0.44 tff(127,plain,
% 0.18/0.44 (![X81: $i] : p4(X81, X81)),
% 0.18/0.44 inference(modus_ponens,[status(thm)],[126, 122])).
% 0.18/0.44 tff(128,plain,
% 0.18/0.44 ((~![X81: $i] : p4(X81, X81)) | p4(c41, c41)),
% 0.18/0.44 inference(quant_inst,[status(thm)],[])).
% 0.18/0.44 tff(129,plain,
% 0.18/0.44 ($false),
% 0.18/0.44 inference(unit_resolution,[status(thm)],[128, 127, 120])).
% 0.18/0.44 % SZS output end Proof
% 0.18/0.44 % E exiting
%------------------------------------------------------------------------------