%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : SYN709-1 : TPTP v9.0.0. Released v2.5.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n012.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:53 AM UTC 2025
% Result : Unsatisfiable 0.12s 0.39s
% Output : Proof 0.19s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : SYN709-1 : TPTP v9.0.0. Released v2.5.0.
% 0.12/0.12 % Command : run_E %s %d THM
% 0.12/0.33 % Computer : n012.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Fri Jun 20 12:39:55 EDT 2025
% 0.12/0.33 % CPUTime :
% 0.12/0.39 % SZS status Unsatisfiable
% 0.12/0.39 % SZS output start Proof
% 0.12/0.39 tff(p30_type, type, (
% 0.12/0.39 p30: ( $i * $i ) > $o)).
% 0.12/0.39 tff(f31_type, type, (
% 0.12/0.39 f31: ( $i * $i ) > $i)).
% 0.12/0.39 tff(f34_type, type, (
% 0.12/0.39 f34: ( $i * $i ) > $i)).
% 0.12/0.39 tff(c56_type, type, (
% 0.12/0.39 c56: $i)).
% 0.12/0.39 tff(c65_type, type, (
% 0.12/0.39 c65: $i)).
% 0.12/0.39 tff(f33_type, type, (
% 0.12/0.39 f33: ( $i * $i ) > $i)).
% 0.12/0.39 tff(c63_type, type, (
% 0.12/0.39 c63: $i)).
% 0.12/0.39 tff(c62_type, type, (
% 0.12/0.39 c62: $i)).
% 0.12/0.39 tff(f25_type, type, (
% 0.12/0.39 f25: ( $i * $i ) > $i)).
% 0.12/0.39 tff(c66_type, type, (
% 0.12/0.39 c66: $i)).
% 0.12/0.39 tff(f28_type, type, (
% 0.12/0.39 f28: ( $i * $i ) > $i)).
% 0.12/0.39 tff(c64_type, type, (
% 0.12/0.39 c64: $i)).
% 0.12/0.39 tff(p29_type, type, (
% 0.12/0.39 p29: ( $i * $i ) > $o)).
% 0.12/0.39 tff(p19_type, type, (
% 0.12/0.39 p19: ( $i * $i ) > $o)).
% 0.12/0.39 tff(p47_type, type, (
% 0.12/0.39 p47: ( $i * $i ) > $o)).
% 0.12/0.39 tff(c60_type, type, (
% 0.12/0.39 c60: $i)).
% 0.12/0.39 tff(p46_type, type, (
% 0.12/0.39 p46: ( $i * $i ) > $o)).
% 0.12/0.39 tff(f20_type, type, (
% 0.12/0.39 f20: ( $i * $i ) > $i)).
% 0.12/0.39 tff(c59_type, type, (
% 0.12/0.39 c59: $i)).
% 0.12/0.39 tff(f23_type, type, (
% 0.12/0.39 f23: ( $i * $i ) > $i)).
% 0.12/0.39 tff(c58_type, type, (
% 0.12/0.39 c58: $i)).
% 0.12/0.39 tff(p24_type, type, (
% 0.12/0.39 p24: ( $i * $i ) > $o)).
% 0.12/0.39 tff(p26_type, type, (
% 0.12/0.39 p26: ( $i * $i ) > $o)).
% 0.12/0.39 tff(p27_type, type, (
% 0.12/0.39 p27: ( $i * $i ) > $o)).
% 0.12/0.39 tff(1,assumption,(~p29(f33(c62, c63), f33(c62, c63))), introduced(assumption)).
% 0.12/0.39 tff(2,plain,
% 0.12/0.39 (^[X72: $i] : refl(p29(X72, X72) <=> p29(X72, X72))),
% 0.12/0.39 inference(bind,[status(th)],[])).
% 0.12/0.39 tff(3,plain,
% 0.12/0.39 (![X72: $i] : p29(X72, X72) <=> ![X72: $i] : p29(X72, X72)),
% 0.12/0.39 inference(quant_intro,[status(thm)],[2])).
% 0.12/0.39 tff(4,plain,
% 0.12/0.39 (![X72: $i] : p29(X72, X72) <=> ![X72: $i] : p29(X72, X72)),
% 0.12/0.39 inference(rewrite,[status(thm)],[])).
% 0.12/0.39 tff(5,axiom,(![X72: $i] : p29(X72, X72)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','p29_14')).
% 0.12/0.39 tff(6,plain,
% 0.12/0.39 (![X72: $i] : p29(X72, X72)),
% 0.12/0.39 inference(modus_ponens,[status(thm)],[5, 4])).
% 0.12/0.39 tff(7,plain,(
% 0.12/0.39 ![X72: $i] : p29(X72, X72)),
% 0.12/0.39 inference(skolemize,[status(sab)],[6])).
% 0.12/0.39 tff(8,plain,
% 0.12/0.39 (![X72: $i] : p29(X72, X72)),
% 0.12/0.39 inference(modus_ponens,[status(thm)],[7, 3])).
% 0.12/0.39 tff(9,plain,
% 0.12/0.39 ((~![X72: $i] : p29(X72, X72)) | p29(f33(c62, c63), f33(c62, c63))),
% 0.12/0.39 inference(quant_inst,[status(thm)],[])).
% 0.12/0.39 tff(10,plain,
% 0.12/0.39 ($false),
% 0.12/0.39 inference(unit_resolution,[status(thm)],[9, 8, 1])).
% 0.12/0.39 tff(11,plain,(p29(f33(c62, c63), f33(c62, c63))), inference(lemma,lemma(discharge,[]))).
% 0.12/0.39 tff(12,plain,
% 0.12/0.39 (^[X34: $i, X33: $i] : refl(p19(f25(f28(c64, X33), f34(c66, X34)), f34(X33, X34)) <=> p19(f25(f28(c64, X33), f34(c66, X34)), f34(X33, X34)))),
% 0.12/0.39 inference(bind,[status(th)],[])).
% 0.12/0.39 tff(13,plain,
% 0.12/0.39 (![X34: $i, X33: $i] : p19(f25(f28(c64, X33), f34(c66, X34)), f34(X33, X34)) <=> ![X34: $i, X33: $i] : p19(f25(f28(c64, X33), f34(c66, X34)), f34(X33, X34))),
% 0.12/0.39 inference(quant_intro,[status(thm)],[12])).
% 0.12/0.39 tff(14,plain,
% 0.12/0.39 (![X34: $i, X33: $i] : p19(f25(f28(c64, X33), f34(c66, X34)), f34(X33, X34)) <=> ![X34: $i, X33: $i] : p19(f25(f28(c64, X33), f34(c66, X34)), f34(X33, X34))),
% 0.12/0.39 inference(rewrite,[status(thm)],[])).
% 0.12/0.39 tff(15,axiom,(![X34: $i, X33: $i] : p19(f25(f28(c64, X33), f34(c66, X34)), f34(X33, X34))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','p19_59')).
% 0.12/0.39 tff(16,plain,
% 0.12/0.39 (![X34: $i, X33: $i] : p19(f25(f28(c64, X33), f34(c66, X34)), f34(X33, X34))),
% 0.12/0.39 inference(modus_ponens,[status(thm)],[15, 14])).
% 0.12/0.39 tff(17,plain,(
% 0.12/0.39 ![X34: $i, X33: $i] : p19(f25(f28(c64, X33), f34(c66, X34)), f34(X33, X34))),
% 0.12/0.39 inference(skolemize,[status(sab)],[16])).
% 0.12/0.39 tff(18,plain,
% 0.12/0.39 (![X34: $i, X33: $i] : p19(f25(f28(c64, X33), f34(c66, X34)), f34(X33, X34))),
% 0.12/0.39 inference(modus_ponens,[status(thm)],[17, 13])).
% 0.12/0.39 tff(19,plain,
% 0.12/0.39 ((~![X34: $i, X33: $i] : p19(f25(f28(c64, X33), f34(c66, X34)), f34(X33, X34))) | p19(f25(f28(c64, c65), f34(c66, c56)), f34(c65, c56))),
% 0.12/0.39 inference(quant_inst,[status(thm)],[])).
% 0.12/0.39 tff(20,plain,
% 0.12/0.39 (p19(f25(f28(c64, c65), f34(c66, c56)), f34(c65, c56))),
% 0.12/0.39 inference(unit_resolution,[status(thm)],[19, 18])).
% 0.12/0.39 tff(21,plain,
% 0.12/0.39 (^[X89: $i, X90: $i, X91: $i, X92: $i] : refl(((~p29(X89, X91)) | (~p19(X90, X92)) | p30(f31(X89, X90), f31(X91, X92))) <=> ((~p29(X89, X91)) | (~p19(X90, X92)) | p30(f31(X89, X90), f31(X91, X92))))),
% 0.12/0.39 inference(bind,[status(th)],[])).
% 0.12/0.39 tff(22,plain,
% 0.12/0.39 (![X89: $i, X90: $i, X91: $i, X92: $i] : ((~p29(X89, X91)) | (~p19(X90, X92)) | p30(f31(X89, X90), f31(X91, X92))) <=> ![X89: $i, X90: $i, X91: $i, X92: $i] : ((~p29(X89, X91)) | (~p19(X90, X92)) | p30(f31(X89, X90), f31(X91, X92)))),
% 0.12/0.39 inference(quant_intro,[status(thm)],[21])).
% 0.12/0.39 tff(23,plain,
% 0.12/0.39 (![X89: $i, X90: $i, X91: $i, X92: $i] : ((~p29(X89, X91)) | (~p19(X90, X92)) | p30(f31(X89, X90), f31(X91, X92))) <=> ![X89: $i, X90: $i, X91: $i, X92: $i] : ((~p29(X89, X91)) | (~p19(X90, X92)) | p30(f31(X89, X90), f31(X91, X92)))),
% 0.12/0.39 inference(rewrite,[status(thm)],[])).
% 0.12/0.39 tff(24,plain,
% 0.12/0.39 (^[X89: $i, X90: $i, X91: $i, X92: $i] : trans(monotonicity(rewrite((p30(f31(X89, X90), f31(X91, X92)) | (~p19(X90, X92))) <=> ((~p19(X90, X92)) | p30(f31(X89, X90), f31(X91, X92)))), (((p30(f31(X89, X90), f31(X91, X92)) | (~p19(X90, X92))) | (~p29(X89, X91))) <=> (((~p19(X90, X92)) | p30(f31(X89, X90), f31(X91, X92))) | (~p29(X89, X91))))), rewrite((((~p19(X90, X92)) | p30(f31(X89, X90), f31(X91, X92))) | (~p29(X89, X91))) <=> ((~p29(X89, X91)) | (~p19(X90, X92)) | p30(f31(X89, X90), f31(X91, X92)))), (((p30(f31(X89, X90), f31(X91, X92)) | (~p19(X90, X92))) | (~p29(X89, X91))) <=> ((~p29(X89, X91)) | (~p19(X90, X92)) | p30(f31(X89, X90), f31(X91, X92)))))),
% 0.12/0.39 inference(bind,[status(th)],[])).
% 0.12/0.39 tff(25,plain,
% 0.12/0.39 (![X89: $i, X90: $i, X91: $i, X92: $i] : ((p30(f31(X89, X90), f31(X91, X92)) | (~p19(X90, X92))) | (~p29(X89, X91))) <=> ![X89: $i, X90: $i, X91: $i, X92: $i] : ((~p29(X89, X91)) | (~p19(X90, X92)) | p30(f31(X89, X90), f31(X91, X92)))),
% 0.12/0.39 inference(quant_intro,[status(thm)],[24])).
% 0.12/0.39 tff(26,axiom,(![X89: $i, X90: $i, X91: $i, X92: $i] : ((p30(f31(X89, X90), f31(X91, X92)) | (~p19(X90, X92))) | (~p29(X89, X91)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','p30_72')).
% 0.12/0.39 tff(27,plain,
% 0.12/0.39 (![X89: $i, X90: $i, X91: $i, X92: $i] : ((~p29(X89, X91)) | (~p19(X90, X92)) | p30(f31(X89, X90), f31(X91, X92)))),
% 0.12/0.39 inference(modus_ponens,[status(thm)],[26, 25])).
% 0.12/0.39 tff(28,plain,
% 0.12/0.39 (![X89: $i, X90: $i, X91: $i, X92: $i] : ((~p29(X89, X91)) | (~p19(X90, X92)) | p30(f31(X89, X90), f31(X91, X92)))),
% 0.12/0.39 inference(modus_ponens,[status(thm)],[27, 23])).
% 0.12/0.39 tff(29,plain,(
% 0.12/0.39 ![X89: $i, X90: $i, X91: $i, X92: $i] : ((~p29(X89, X91)) | (~p19(X90, X92)) | p30(f31(X89, X90), f31(X91, X92)))),
% 0.12/0.39 inference(skolemize,[status(sab)],[28])).
% 0.12/0.39 tff(30,plain,
% 0.12/0.39 (![X89: $i, X90: $i, X91: $i, X92: $i] : ((~p29(X89, X91)) | (~p19(X90, X92)) | p30(f31(X89, X90), f31(X91, X92)))),
% 0.12/0.39 inference(modus_ponens,[status(thm)],[29, 22])).
% 0.12/0.39 tff(31,plain,
% 0.12/0.39 (((~![X89: $i, X90: $i, X91: $i, X92: $i] : ((~p29(X89, X91)) | (~p19(X90, X92)) | p30(f31(X89, X90), f31(X91, X92)))) | ((~p29(f33(c62, c63), f33(c62, c63))) | (~p19(f25(f28(c64, c65), f34(c66, c56)), f34(c65, c56))) | p30(f31(f33(c62, c63), f25(f28(c64, c65), f34(c66, c56))), f31(f33(c62, c63), f34(c65, c56))))) <=> ((~![X89: $i, X90: $i, X91: $i, X92: $i] : ((~p29(X89, X91)) | (~p19(X90, X92)) | p30(f31(X89, X90), f31(X91, X92)))) | (~p29(f33(c62, c63), f33(c62, c63))) | (~p19(f25(f28(c64, c65), f34(c66, c56)), f34(c65, c56))) | p30(f31(f33(c62, c63), f25(f28(c64, c65), f34(c66, c56))), f31(f33(c62, c63), f34(c65, c56))))),
% 0.12/0.39 inference(rewrite,[status(thm)],[])).
% 0.12/0.39 tff(32,plain,
% 0.12/0.39 ((~![X89: $i, X90: $i, X91: $i, X92: $i] : ((~p29(X89, X91)) | (~p19(X90, X92)) | p30(f31(X89, X90), f31(X91, X92)))) | ((~p29(f33(c62, c63), f33(c62, c63))) | (~p19(f25(f28(c64, c65), f34(c66, c56)), f34(c65, c56))) | p30(f31(f33(c62, c63), f25(f28(c64, c65), f34(c66, c56))), f31(f33(c62, c63), f34(c65, c56))))),
% 0.12/0.39 inference(quant_inst,[status(thm)],[])).
% 0.12/0.39 tff(33,plain,
% 0.12/0.39 ((~![X89: $i, X90: $i, X91: $i, X92: $i] : ((~p29(X89, X91)) | (~p19(X90, X92)) | p30(f31(X89, X90), f31(X91, X92)))) | (~p29(f33(c62, c63), f33(c62, c63))) | (~p19(f25(f28(c64, c65), f34(c66, c56)), f34(c65, c56))) | p30(f31(f33(c62, c63), f25(f28(c64, c65), f34(c66, c56))), f31(f33(c62, c63), f34(c65, c56)))),
% 0.12/0.39 inference(modus_ponens,[status(thm)],[32, 31])).
% 0.12/0.39 tff(34,plain,
% 0.12/0.39 ((~p29(f33(c62, c63), f33(c62, c63))) | p30(f31(f33(c62, c63), f25(f28(c64, c65), f34(c66, c56))), f31(f33(c62, c63), f34(c65, c56)))),
% 0.12/0.40 inference(unit_resolution,[status(thm)],[33, 30, 20])).
% 0.12/0.40 tff(35,plain,
% 0.12/0.40 (p30(f31(f33(c62, c63), f25(f28(c64, c65), f34(c66, c56))), f31(f33(c62, c63), f34(c65, c56)))),
% 0.12/0.40 inference(unit_resolution,[status(thm)],[34, 11])).
% 0.12/0.40 tff(36,assumption,(~p47(f31(f33(c62, c63), f34(c66, c56)), c60)), introduced(assumption)).
% 0.12/0.40 tff(37,plain,
% 0.12/0.40 (^[X148: $i, X149: $i] : refl(((~p46(f23(c58, X148), f20(c59, X149))) | p47(f31(f33(c62, c63), f34(c66, X148)), X149)) <=> ((~p46(f23(c58, X148), f20(c59, X149))) | p47(f31(f33(c62, c63), f34(c66, X148)), X149)))),
% 0.12/0.40 inference(bind,[status(th)],[])).
% 0.12/0.40 tff(38,plain,
% 0.12/0.40 (![X148: $i, X149: $i] : ((~p46(f23(c58, X148), f20(c59, X149))) | p47(f31(f33(c62, c63), f34(c66, X148)), X149)) <=> ![X148: $i, X149: $i] : ((~p46(f23(c58, X148), f20(c59, X149))) | p47(f31(f33(c62, c63), f34(c66, X148)), X149))),
% 0.12/0.40 inference(quant_intro,[status(thm)],[37])).
% 0.12/0.40 tff(39,plain,
% 0.12/0.40 (![X148: $i, X149: $i] : ((~p46(f23(c58, X148), f20(c59, X149))) | p47(f31(f33(c62, c63), f34(c66, X148)), X149)) <=> ![X148: $i, X149: $i] : ((~p46(f23(c58, X148), f20(c59, X149))) | p47(f31(f33(c62, c63), f34(c66, X148)), X149))),
% 0.12/0.40 inference(rewrite,[status(thm)],[])).
% 0.12/0.40 tff(40,plain,
% 0.12/0.40 (^[X148: $i, X149: $i] : rewrite((p47(f31(f33(c62, c63), f34(c66, X148)), X149) | (~p46(f23(c58, X148), f20(c59, X149)))) <=> ((~p46(f23(c58, X148), f20(c59, X149))) | p47(f31(f33(c62, c63), f34(c66, X148)), X149)))),
% 0.12/0.40 inference(bind,[status(th)],[])).
% 0.12/0.40 tff(41,plain,
% 0.12/0.40 (![X148: $i, X149: $i] : (p47(f31(f33(c62, c63), f34(c66, X148)), X149) | (~p46(f23(c58, X148), f20(c59, X149)))) <=> ![X148: $i, X149: $i] : ((~p46(f23(c58, X148), f20(c59, X149))) | p47(f31(f33(c62, c63), f34(c66, X148)), X149))),
% 0.12/0.40 inference(quant_intro,[status(thm)],[40])).
% 0.12/0.40 tff(42,axiom,(![X148: $i, X149: $i] : (p47(f31(f33(c62, c63), f34(c66, X148)), X149) | (~p46(f23(c58, X148), f20(c59, X149))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','p47_81')).
% 0.12/0.40 tff(43,plain,
% 0.12/0.40 (![X148: $i, X149: $i] : ((~p46(f23(c58, X148), f20(c59, X149))) | p47(f31(f33(c62, c63), f34(c66, X148)), X149))),
% 0.12/0.40 inference(modus_ponens,[status(thm)],[42, 41])).
% 0.12/0.40 tff(44,plain,
% 0.12/0.40 (![X148: $i, X149: $i] : ((~p46(f23(c58, X148), f20(c59, X149))) | p47(f31(f33(c62, c63), f34(c66, X148)), X149))),
% 0.12/0.40 inference(modus_ponens,[status(thm)],[43, 39])).
% 0.12/0.40 tff(45,plain,(
% 0.12/0.40 ![X148: $i, X149: $i] : ((~p46(f23(c58, X148), f20(c59, X149))) | p47(f31(f33(c62, c63), f34(c66, X148)), X149))),
% 0.12/0.40 inference(skolemize,[status(sab)],[44])).
% 0.12/0.40 tff(46,plain,
% 0.12/0.40 (![X148: $i, X149: $i] : ((~p46(f23(c58, X148), f20(c59, X149))) | p47(f31(f33(c62, c63), f34(c66, X148)), X149))),
% 0.12/0.40 inference(modus_ponens,[status(thm)],[45, 38])).
% 0.12/0.40 tff(47,plain,
% 0.12/0.40 (p46(f23(c58, c56), f20(c59, c60)) <=> p46(f23(c58, c56), f20(c59, c60))),
% 0.12/0.40 inference(rewrite,[status(thm)],[])).
% 0.12/0.40 tff(48,axiom,(p46(f23(c58, c56), f20(c59, c60))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','p46_29')).
% 0.12/0.40 tff(49,plain,
% 0.12/0.40 (p46(f23(c58, c56), f20(c59, c60))),
% 0.12/0.40 inference(modus_ponens,[status(thm)],[48, 47])).
% 0.12/0.40 tff(50,plain,
% 0.12/0.40 (((~![X148: $i, X149: $i] : ((~p46(f23(c58, X148), f20(c59, X149))) | p47(f31(f33(c62, c63), f34(c66, X148)), X149))) | ((~p46(f23(c58, c56), f20(c59, c60))) | p47(f31(f33(c62, c63), f34(c66, c56)), c60))) <=> ((~![X148: $i, X149: $i] : ((~p46(f23(c58, X148), f20(c59, X149))) | p47(f31(f33(c62, c63), f34(c66, X148)), X149))) | (~p46(f23(c58, c56), f20(c59, c60))) | p47(f31(f33(c62, c63), f34(c66, c56)), c60))),
% 0.12/0.40 inference(rewrite,[status(thm)],[])).
% 0.12/0.40 tff(51,plain,
% 0.12/0.40 ((~![X148: $i, X149: $i] : ((~p46(f23(c58, X148), f20(c59, X149))) | p47(f31(f33(c62, c63), f34(c66, X148)), X149))) | ((~p46(f23(c58, c56), f20(c59, c60))) | p47(f31(f33(c62, c63), f34(c66, c56)), c60))),
% 0.12/0.40 inference(quant_inst,[status(thm)],[])).
% 0.12/0.40 tff(52,plain,
% 0.12/0.40 ((~![X148: $i, X149: $i] : ((~p46(f23(c58, X148), f20(c59, X149))) | p47(f31(f33(c62, c63), f34(c66, X148)), X149))) | (~p46(f23(c58, c56), f20(c59, c60))) | p47(f31(f33(c62, c63), f34(c66, c56)), c60)),
% 0.12/0.40 inference(modus_ponens,[status(thm)],[51, 50])).
% 0.12/0.40 tff(53,plain,
% 0.12/0.40 ($false),
% 0.12/0.40 inference(unit_resolution,[status(thm)],[52, 49, 46, 36])).
% 0.12/0.40 tff(54,plain,(p47(f31(f33(c62, c63), f34(c66, c56)), c60)), inference(lemma,lemma(discharge,[]))).
% 0.12/0.40 tff(55,plain,
% 0.12/0.40 (^[X146: $i, X147: $i] : refl(((~p47(f31(f33(c62, c63), X146), X147)) | p47(f31(f33(c62, c63), f25(f28(c64, c65), X146)), f25(f28(c64, c65), X147))) <=> ((~p47(f31(f33(c62, c63), X146), X147)) | p47(f31(f33(c62, c63), f25(f28(c64, c65), X146)), f25(f28(c64, c65), X147))))),
% 0.12/0.40 inference(bind,[status(th)],[])).
% 0.12/0.40 tff(56,plain,
% 0.12/0.40 (![X146: $i, X147: $i] : ((~p47(f31(f33(c62, c63), X146), X147)) | p47(f31(f33(c62, c63), f25(f28(c64, c65), X146)), f25(f28(c64, c65), X147))) <=> ![X146: $i, X147: $i] : ((~p47(f31(f33(c62, c63), X146), X147)) | p47(f31(f33(c62, c63), f25(f28(c64, c65), X146)), f25(f28(c64, c65), X147)))),
% 0.12/0.40 inference(quant_intro,[status(thm)],[55])).
% 0.12/0.40 tff(57,plain,
% 0.12/0.40 (![X146: $i, X147: $i] : ((~p47(f31(f33(c62, c63), X146), X147)) | p47(f31(f33(c62, c63), f25(f28(c64, c65), X146)), f25(f28(c64, c65), X147))) <=> ![X146: $i, X147: $i] : ((~p47(f31(f33(c62, c63), X146), X147)) | p47(f31(f33(c62, c63), f25(f28(c64, c65), X146)), f25(f28(c64, c65), X147)))),
% 0.12/0.40 inference(rewrite,[status(thm)],[])).
% 0.12/0.40 tff(58,plain,
% 0.12/0.40 (^[X146: $i, X147: $i] : rewrite((p47(f31(f33(c62, c63), f25(f28(c64, c65), X146)), f25(f28(c64, c65), X147)) | (~p47(f31(f33(c62, c63), X146), X147))) <=> ((~p47(f31(f33(c62, c63), X146), X147)) | p47(f31(f33(c62, c63), f25(f28(c64, c65), X146)), f25(f28(c64, c65), X147))))),
% 0.12/0.40 inference(bind,[status(th)],[])).
% 0.12/0.40 tff(59,plain,
% 0.12/0.40 (![X146: $i, X147: $i] : (p47(f31(f33(c62, c63), f25(f28(c64, c65), X146)), f25(f28(c64, c65), X147)) | (~p47(f31(f33(c62, c63), X146), X147))) <=> ![X146: $i, X147: $i] : ((~p47(f31(f33(c62, c63), X146), X147)) | p47(f31(f33(c62, c63), f25(f28(c64, c65), X146)), f25(f28(c64, c65), X147)))),
% 0.12/0.40 inference(quant_intro,[status(thm)],[58])).
% 0.12/0.40 tff(60,axiom,(![X146: $i, X147: $i] : (p47(f31(f33(c62, c63), f25(f28(c64, c65), X146)), f25(f28(c64, c65), X147)) | (~p47(f31(f33(c62, c63), X146), X147)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','p47_83')).
% 0.12/0.40 tff(61,plain,
% 0.12/0.40 (![X146: $i, X147: $i] : ((~p47(f31(f33(c62, c63), X146), X147)) | p47(f31(f33(c62, c63), f25(f28(c64, c65), X146)), f25(f28(c64, c65), X147)))),
% 0.12/0.40 inference(modus_ponens,[status(thm)],[60, 59])).
% 0.12/0.40 tff(62,plain,
% 0.12/0.40 (![X146: $i, X147: $i] : ((~p47(f31(f33(c62, c63), X146), X147)) | p47(f31(f33(c62, c63), f25(f28(c64, c65), X146)), f25(f28(c64, c65), X147)))),
% 0.12/0.40 inference(modus_ponens,[status(thm)],[61, 57])).
% 0.12/0.40 tff(63,plain,(
% 0.12/0.40 ![X146: $i, X147: $i] : ((~p47(f31(f33(c62, c63), X146), X147)) | p47(f31(f33(c62, c63), f25(f28(c64, c65), X146)), f25(f28(c64, c65), X147)))),
% 0.12/0.40 inference(skolemize,[status(sab)],[62])).
% 0.12/0.40 tff(64,plain,
% 0.12/0.40 (![X146: $i, X147: $i] : ((~p47(f31(f33(c62, c63), X146), X147)) | p47(f31(f33(c62, c63), f25(f28(c64, c65), X146)), f25(f28(c64, c65), X147)))),
% 0.12/0.40 inference(modus_ponens,[status(thm)],[63, 56])).
% 0.12/0.40 tff(65,plain,
% 0.12/0.40 (((~![X146: $i, X147: $i] : ((~p47(f31(f33(c62, c63), X146), X147)) | p47(f31(f33(c62, c63), f25(f28(c64, c65), X146)), f25(f28(c64, c65), X147)))) | ((~p47(f31(f33(c62, c63), f34(c66, c56)), c60)) | p47(f31(f33(c62, c63), f25(f28(c64, c65), f34(c66, c56))), f25(f28(c64, c65), c60)))) <=> ((~![X146: $i, X147: $i] : ((~p47(f31(f33(c62, c63), X146), X147)) | p47(f31(f33(c62, c63), f25(f28(c64, c65), X146)), f25(f28(c64, c65), X147)))) | (~p47(f31(f33(c62, c63), f34(c66, c56)), c60)) | p47(f31(f33(c62, c63), f25(f28(c64, c65), f34(c66, c56))), f25(f28(c64, c65), c60)))),
% 0.12/0.40 inference(rewrite,[status(thm)],[])).
% 0.12/0.40 tff(66,plain,
% 0.12/0.40 ((~![X146: $i, X147: $i] : ((~p47(f31(f33(c62, c63), X146), X147)) | p47(f31(f33(c62, c63), f25(f28(c64, c65), X146)), f25(f28(c64, c65), X147)))) | ((~p47(f31(f33(c62, c63), f34(c66, c56)), c60)) | p47(f31(f33(c62, c63), f25(f28(c64, c65), f34(c66, c56))), f25(f28(c64, c65), c60)))),
% 0.12/0.40 inference(quant_inst,[status(thm)],[])).
% 0.12/0.40 tff(67,plain,
% 0.12/0.40 ((~![X146: $i, X147: $i] : ((~p47(f31(f33(c62, c63), X146), X147)) | p47(f31(f33(c62, c63), f25(f28(c64, c65), X146)), f25(f28(c64, c65), X147)))) | (~p47(f31(f33(c62, c63), f34(c66, c56)), c60)) | p47(f31(f33(c62, c63), f25(f28(c64, c65), f34(c66, c56))), f25(f28(c64, c65), c60))),
% 0.12/0.40 inference(modus_ponens,[status(thm)],[66, 65])).
% 0.12/0.40 tff(68,plain,
% 0.12/0.40 ((~p47(f31(f33(c62, c63), f34(c66, c56)), c60)) | p47(f31(f33(c62, c63), f25(f28(c64, c65), f34(c66, c56))), f25(f28(c64, c65), c60))),
% 0.12/0.40 inference(unit_resolution,[status(thm)],[67, 64])).
% 0.12/0.40 tff(69,plain,
% 0.12/0.40 (p47(f31(f33(c62, c63), f25(f28(c64, c65), f34(c66, c56))), f25(f28(c64, c65), c60))),
% 0.12/0.40 inference(unit_resolution,[status(thm)],[68, 54])).
% 0.12/0.40 tff(70,assumption,(~p26(c64, c64)), introduced(assumption)).
% 0.12/0.40 tff(71,plain,
% 0.12/0.40 (^[X66: $i] : refl(p26(X66, X66) <=> p26(X66, X66))),
% 0.12/0.40 inference(bind,[status(th)],[])).
% 0.12/0.40 tff(72,plain,
% 0.12/0.40 (![X66: $i] : p26(X66, X66) <=> ![X66: $i] : p26(X66, X66)),
% 0.12/0.40 inference(quant_intro,[status(thm)],[71])).
% 0.12/0.40 tff(73,plain,
% 0.12/0.40 (![X66: $i] : p26(X66, X66) <=> ![X66: $i] : p26(X66, X66)),
% 0.12/0.40 inference(rewrite,[status(thm)],[])).
% 0.12/0.40 tff(74,axiom,(![X66: $i] : p26(X66, X66)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','p26_16')).
% 0.12/0.40 tff(75,plain,
% 0.12/0.40 (![X66: $i] : p26(X66, X66)),
% 0.12/0.40 inference(modus_ponens,[status(thm)],[74, 73])).
% 0.12/0.40 tff(76,plain,(
% 0.12/0.40 ![X66: $i] : p26(X66, X66)),
% 0.12/0.40 inference(skolemize,[status(sab)],[75])).
% 0.12/0.40 tff(77,plain,
% 0.12/0.40 (![X66: $i] : p26(X66, X66)),
% 0.12/0.40 inference(modus_ponens,[status(thm)],[76, 72])).
% 0.12/0.40 tff(78,plain,
% 0.12/0.40 ((~![X66: $i] : p26(X66, X66)) | p26(c64, c64)),
% 0.12/0.40 inference(quant_inst,[status(thm)],[])).
% 0.12/0.40 tff(79,plain,
% 0.12/0.40 ($false),
% 0.12/0.40 inference(unit_resolution,[status(thm)],[78, 77, 70])).
% 0.12/0.40 tff(80,plain,(p26(c64, c64)), inference(lemma,lemma(discharge,[]))).
% 0.12/0.40 tff(81,assumption,(~p27(c65, c65)), introduced(assumption)).
% 0.12/0.40 tff(82,plain,
% 0.12/0.40 (^[X69: $i] : refl(p27(X69, X69) <=> p27(X69, X69))),
% 0.12/0.40 inference(bind,[status(th)],[])).
% 0.12/0.40 tff(83,plain,
% 0.12/0.40 (![X69: $i] : p27(X69, X69) <=> ![X69: $i] : p27(X69, X69)),
% 0.12/0.40 inference(quant_intro,[status(thm)],[82])).
% 0.12/0.40 tff(84,plain,
% 0.12/0.40 (![X69: $i] : p27(X69, X69) <=> ![X69: $i] : p27(X69, X69)),
% 0.12/0.40 inference(rewrite,[status(thm)],[])).
% 0.12/0.40 tff(85,axiom,(![X69: $i] : p27(X69, X69)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','p27_15')).
% 0.12/0.40 tff(86,plain,
% 0.12/0.40 (![X69: $i] : p27(X69, X69)),
% 0.12/0.40 inference(modus_ponens,[status(thm)],[85, 84])).
% 0.12/0.40 tff(87,plain,(
% 0.12/0.40 ![X69: $i] : p27(X69, X69)),
% 0.12/0.40 inference(skolemize,[status(sab)],[86])).
% 0.12/0.40 tff(88,plain,
% 0.12/0.40 (![X69: $i] : p27(X69, X69)),
% 0.12/0.40 inference(modus_ponens,[status(thm)],[87, 83])).
% 0.12/0.40 tff(89,plain,
% 0.12/0.40 ((~![X69: $i] : p27(X69, X69)) | p27(c65, c65)),
% 0.12/0.40 inference(quant_inst,[status(thm)],[])).
% 0.12/0.40 tff(90,plain,
% 0.12/0.40 ($false),
% 0.12/0.40 inference(unit_resolution,[status(thm)],[89, 88, 81])).
% 0.12/0.40 tff(91,plain,(p27(c65, c65)), inference(lemma,lemma(discharge,[]))).
% 0.12/0.40 tff(92,plain,
% 0.12/0.40 (^[X62: $i, X64: $i, X65: $i, X63: $i] : refl(((~p27(X63, X65)) | (~p26(X62, X64)) | p24(f28(X62, X63), f28(X64, X65))) <=> ((~p27(X63, X65)) | (~p26(X62, X64)) | p24(f28(X62, X63), f28(X64, X65))))),
% 0.12/0.40 inference(bind,[status(th)],[])).
% 0.12/0.40 tff(93,plain,
% 0.12/0.40 (![X62: $i, X64: $i, X65: $i, X63: $i] : ((~p27(X63, X65)) | (~p26(X62, X64)) | p24(f28(X62, X63), f28(X64, X65))) <=> ![X62: $i, X64: $i, X65: $i, X63: $i] : ((~p27(X63, X65)) | (~p26(X62, X64)) | p24(f28(X62, X63), f28(X64, X65)))),
% 0.12/0.40 inference(quant_intro,[status(thm)],[92])).
% 0.12/0.40 tff(94,plain,
% 0.12/0.40 (![X62: $i, X64: $i, X65: $i, X63: $i] : ((~p27(X63, X65)) | (~p26(X62, X64)) | p24(f28(X62, X63), f28(X64, X65))) <=> ![X62: $i, X64: $i, X65: $i, X63: $i] : ((~p27(X63, X65)) | (~p26(X62, X64)) | p24(f28(X62, X63), f28(X64, X65)))),
% 0.12/0.40 inference(rewrite,[status(thm)],[])).
% 0.12/0.40 tff(95,plain,
% 0.12/0.40 (^[X62: $i, X64: $i, X65: $i, X63: $i] : trans(monotonicity(rewrite((p24(f28(X62, X63), f28(X64, X65)) | (~p26(X62, X64))) <=> ((~p26(X62, X64)) | p24(f28(X62, X63), f28(X64, X65)))), (((p24(f28(X62, X63), f28(X64, X65)) | (~p26(X62, X64))) | (~p27(X63, X65))) <=> (((~p26(X62, X64)) | p24(f28(X62, X63), f28(X64, X65))) | (~p27(X63, X65))))), rewrite((((~p26(X62, X64)) | p24(f28(X62, X63), f28(X64, X65))) | (~p27(X63, X65))) <=> ((~p27(X63, X65)) | (~p26(X62, X64)) | p24(f28(X62, X63), f28(X64, X65)))), (((p24(f28(X62, X63), f28(X64, X65)) | (~p26(X62, X64))) | (~p27(X63, X65))) <=> ((~p27(X63, X65)) | (~p26(X62, X64)) | p24(f28(X62, X63), f28(X64, X65)))))),
% 0.12/0.41 inference(bind,[status(th)],[])).
% 0.12/0.41 tff(96,plain,
% 0.12/0.41 (![X62: $i, X64: $i, X65: $i, X63: $i] : ((p24(f28(X62, X63), f28(X64, X65)) | (~p26(X62, X64))) | (~p27(X63, X65))) <=> ![X62: $i, X64: $i, X65: $i, X63: $i] : ((~p27(X63, X65)) | (~p26(X62, X64)) | p24(f28(X62, X63), f28(X64, X65)))),
% 0.12/0.41 inference(quant_intro,[status(thm)],[95])).
% 0.12/0.41 tff(97,axiom,(![X62: $i, X64: $i, X65: $i, X63: $i] : ((p24(f28(X62, X63), f28(X64, X65)) | (~p26(X62, X64))) | (~p27(X63, X65)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','p24_75')).
% 0.12/0.41 tff(98,plain,
% 0.12/0.41 (![X62: $i, X64: $i, X65: $i, X63: $i] : ((~p27(X63, X65)) | (~p26(X62, X64)) | p24(f28(X62, X63), f28(X64, X65)))),
% 0.12/0.41 inference(modus_ponens,[status(thm)],[97, 96])).
% 0.12/0.41 tff(99,plain,
% 0.12/0.41 (![X62: $i, X64: $i, X65: $i, X63: $i] : ((~p27(X63, X65)) | (~p26(X62, X64)) | p24(f28(X62, X63), f28(X64, X65)))),
% 0.12/0.41 inference(modus_ponens,[status(thm)],[98, 94])).
% 0.12/0.41 tff(100,plain,(
% 0.12/0.41 ![X62: $i, X64: $i, X65: $i, X63: $i] : ((~p27(X63, X65)) | (~p26(X62, X64)) | p24(f28(X62, X63), f28(X64, X65)))),
% 0.12/0.41 inference(skolemize,[status(sab)],[99])).
% 0.12/0.41 tff(101,plain,
% 0.12/0.41 (![X62: $i, X64: $i, X65: $i, X63: $i] : ((~p27(X63, X65)) | (~p26(X62, X64)) | p24(f28(X62, X63), f28(X64, X65)))),
% 0.12/0.41 inference(modus_ponens,[status(thm)],[100, 93])).
% 0.12/0.41 tff(102,plain,
% 0.12/0.41 (((~![X62: $i, X64: $i, X65: $i, X63: $i] : ((~p27(X63, X65)) | (~p26(X62, X64)) | p24(f28(X62, X63), f28(X64, X65)))) | ((~p27(c65, c65)) | (~p26(c64, c64)) | p24(f28(c64, c65), f28(c64, c65)))) <=> ((~![X62: $i, X64: $i, X65: $i, X63: $i] : ((~p27(X63, X65)) | (~p26(X62, X64)) | p24(f28(X62, X63), f28(X64, X65)))) | (~p27(c65, c65)) | (~p26(c64, c64)) | p24(f28(c64, c65), f28(c64, c65)))),
% 0.12/0.41 inference(rewrite,[status(thm)],[])).
% 0.12/0.41 tff(103,plain,
% 0.12/0.41 ((~![X62: $i, X64: $i, X65: $i, X63: $i] : ((~p27(X63, X65)) | (~p26(X62, X64)) | p24(f28(X62, X63), f28(X64, X65)))) | ((~p27(c65, c65)) | (~p26(c64, c64)) | p24(f28(c64, c65), f28(c64, c65)))),
% 0.12/0.41 inference(quant_inst,[status(thm)],[])).
% 0.12/0.41 tff(104,plain,
% 0.12/0.41 ((~![X62: $i, X64: $i, X65: $i, X63: $i] : ((~p27(X63, X65)) | (~p26(X62, X64)) | p24(f28(X62, X63), f28(X64, X65)))) | (~p27(c65, c65)) | (~p26(c64, c64)) | p24(f28(c64, c65), f28(c64, c65))),
% 0.12/0.41 inference(modus_ponens,[status(thm)],[103, 102])).
% 0.12/0.41 tff(105,plain,
% 0.12/0.41 ((~p27(c65, c65)) | (~p26(c64, c64)) | p24(f28(c64, c65), f28(c64, c65))),
% 0.12/0.41 inference(unit_resolution,[status(thm)],[104, 101])).
% 0.12/0.41 tff(106,plain,
% 0.12/0.41 ((~p26(c64, c64)) | p24(f28(c64, c65), f28(c64, c65))),
% 0.12/0.41 inference(unit_resolution,[status(thm)],[105, 91])).
% 0.12/0.41 tff(107,plain,
% 0.12/0.41 (p24(f28(c64, c65), f28(c64, c65))),
% 0.12/0.41 inference(unit_resolution,[status(thm)],[106, 80])).
% 0.12/0.41 tff(108,assumption,(~p19(c60, c60)), introduced(assumption)).
% 0.12/0.41 tff(109,plain,
% 0.12/0.41 (^[X26: $i] : refl(p19(X26, X26) <=> p19(X26, X26))),
% 0.12/0.41 inference(bind,[status(th)],[])).
% 0.12/0.41 tff(110,plain,
% 0.12/0.41 (![X26: $i] : p19(X26, X26) <=> ![X26: $i] : p19(X26, X26)),
% 0.12/0.41 inference(quant_intro,[status(thm)],[109])).
% 0.12/0.41 tff(111,plain,
% 0.12/0.41 (![X26: $i] : p19(X26, X26) <=> ![X26: $i] : p19(X26, X26)),
% 0.12/0.41 inference(rewrite,[status(thm)],[])).
% 0.12/0.41 tff(112,axiom,(![X26: $i] : p19(X26, X26)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','p19_21')).
% 0.12/0.41 tff(113,plain,
% 0.12/0.41 (![X26: $i] : p19(X26, X26)),
% 0.12/0.41 inference(modus_ponens,[status(thm)],[112, 111])).
% 0.12/0.41 tff(114,plain,(
% 0.12/0.41 ![X26: $i] : p19(X26, X26)),
% 0.12/0.41 inference(skolemize,[status(sab)],[113])).
% 0.12/0.41 tff(115,plain,
% 0.12/0.41 (![X26: $i] : p19(X26, X26)),
% 0.12/0.41 inference(modus_ponens,[status(thm)],[114, 110])).
% 0.12/0.41 tff(116,plain,
% 0.12/0.41 ((~![X26: $i] : p19(X26, X26)) | p19(c60, c60)),
% 0.12/0.41 inference(quant_inst,[status(thm)],[])).
% 0.12/0.41 tff(117,plain,
% 0.12/0.41 ($false),
% 0.12/0.41 inference(unit_resolution,[status(thm)],[116, 115, 108])).
% 0.12/0.41 tff(118,plain,(p19(c60, c60)), inference(lemma,lemma(discharge,[]))).
% 0.12/0.41 tff(119,plain,
% 0.12/0.41 (^[X31: $i, X32: $i, X30: $i, X29: $i] : refl(((~p24(X29, X31)) | (~p19(X30, X32)) | p19(f25(X29, X30), f25(X31, X32))) <=> ((~p24(X29, X31)) | (~p19(X30, X32)) | p19(f25(X29, X30), f25(X31, X32))))),
% 0.12/0.41 inference(bind,[status(th)],[])).
% 0.12/0.41 tff(120,plain,
% 0.12/0.41 (![X31: $i, X32: $i, X30: $i, X29: $i] : ((~p24(X29, X31)) | (~p19(X30, X32)) | p19(f25(X29, X30), f25(X31, X32))) <=> ![X31: $i, X32: $i, X30: $i, X29: $i] : ((~p24(X29, X31)) | (~p19(X30, X32)) | p19(f25(X29, X30), f25(X31, X32)))),
% 0.12/0.41 inference(quant_intro,[status(thm)],[119])).
% 0.12/0.41 tff(121,plain,
% 0.12/0.41 (![X31: $i, X32: $i, X30: $i, X29: $i] : ((~p24(X29, X31)) | (~p19(X30, X32)) | p19(f25(X29, X30), f25(X31, X32))) <=> ![X31: $i, X32: $i, X30: $i, X29: $i] : ((~p24(X29, X31)) | (~p19(X30, X32)) | p19(f25(X29, X30), f25(X31, X32)))),
% 0.12/0.41 inference(rewrite,[status(thm)],[])).
% 0.12/0.41 tff(122,plain,
% 0.12/0.41 (^[X31: $i, X32: $i, X30: $i, X29: $i] : trans(monotonicity(rewrite((p19(f25(X29, X30), f25(X31, X32)) | (~p19(X30, X32))) <=> ((~p19(X30, X32)) | p19(f25(X29, X30), f25(X31, X32)))), (((p19(f25(X29, X30), f25(X31, X32)) | (~p19(X30, X32))) | (~p24(X29, X31))) <=> (((~p19(X30, X32)) | p19(f25(X29, X30), f25(X31, X32))) | (~p24(X29, X31))))), rewrite((((~p19(X30, X32)) | p19(f25(X29, X30), f25(X31, X32))) | (~p24(X29, X31))) <=> ((~p24(X29, X31)) | (~p19(X30, X32)) | p19(f25(X29, X30), f25(X31, X32)))), (((p19(f25(X29, X30), f25(X31, X32)) | (~p19(X30, X32))) | (~p24(X29, X31))) <=> ((~p24(X29, X31)) | (~p19(X30, X32)) | p19(f25(X29, X30), f25(X31, X32)))))),
% 0.12/0.41 inference(bind,[status(th)],[])).
% 0.12/0.41 tff(123,plain,
% 0.12/0.41 (![X31: $i, X32: $i, X30: $i, X29: $i] : ((p19(f25(X29, X30), f25(X31, X32)) | (~p19(X30, X32))) | (~p24(X29, X31))) <=> ![X31: $i, X32: $i, X30: $i, X29: $i] : ((~p24(X29, X31)) | (~p19(X30, X32)) | p19(f25(X29, X30), f25(X31, X32)))),
% 0.12/0.41 inference(quant_intro,[status(thm)],[122])).
% 0.12/0.41 tff(124,axiom,(![X31: $i, X32: $i, X30: $i, X29: $i] : ((p19(f25(X29, X30), f25(X31, X32)) | (~p19(X30, X32))) | (~p24(X29, X31)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','p19_79')).
% 0.12/0.41 tff(125,plain,
% 0.12/0.41 (![X31: $i, X32: $i, X30: $i, X29: $i] : ((~p24(X29, X31)) | (~p19(X30, X32)) | p19(f25(X29, X30), f25(X31, X32)))),
% 0.12/0.41 inference(modus_ponens,[status(thm)],[124, 123])).
% 0.12/0.41 tff(126,plain,
% 0.12/0.41 (![X31: $i, X32: $i, X30: $i, X29: $i] : ((~p24(X29, X31)) | (~p19(X30, X32)) | p19(f25(X29, X30), f25(X31, X32)))),
% 0.12/0.41 inference(modus_ponens,[status(thm)],[125, 121])).
% 0.12/0.41 tff(127,plain,(
% 0.12/0.41 ![X31: $i, X32: $i, X30: $i, X29: $i] : ((~p24(X29, X31)) | (~p19(X30, X32)) | p19(f25(X29, X30), f25(X31, X32)))),
% 0.12/0.41 inference(skolemize,[status(sab)],[126])).
% 0.12/0.41 tff(128,plain,
% 0.12/0.41 (![X31: $i, X32: $i, X30: $i, X29: $i] : ((~p24(X29, X31)) | (~p19(X30, X32)) | p19(f25(X29, X30), f25(X31, X32)))),
% 0.12/0.41 inference(modus_ponens,[status(thm)],[127, 120])).
% 0.12/0.41 tff(129,plain,
% 0.12/0.41 (((~![X31: $i, X32: $i, X30: $i, X29: $i] : ((~p24(X29, X31)) | (~p19(X30, X32)) | p19(f25(X29, X30), f25(X31, X32)))) | ((~p24(f28(c64, c65), f28(c64, c65))) | (~p19(c60, c60)) | p19(f25(f28(c64, c65), c60), f25(f28(c64, c65), c60)))) <=> ((~![X31: $i, X32: $i, X30: $i, X29: $i] : ((~p24(X29, X31)) | (~p19(X30, X32)) | p19(f25(X29, X30), f25(X31, X32)))) | (~p24(f28(c64, c65), f28(c64, c65))) | (~p19(c60, c60)) | p19(f25(f28(c64, c65), c60), f25(f28(c64, c65), c60)))),
% 0.12/0.41 inference(rewrite,[status(thm)],[])).
% 0.12/0.41 tff(130,plain,
% 0.12/0.41 ((~![X31: $i, X32: $i, X30: $i, X29: $i] : ((~p24(X29, X31)) | (~p19(X30, X32)) | p19(f25(X29, X30), f25(X31, X32)))) | ((~p24(f28(c64, c65), f28(c64, c65))) | (~p19(c60, c60)) | p19(f25(f28(c64, c65), c60), f25(f28(c64, c65), c60)))),
% 0.12/0.41 inference(quant_inst,[status(thm)],[])).
% 0.12/0.41 tff(131,plain,
% 0.12/0.41 ((~![X31: $i, X32: $i, X30: $i, X29: $i] : ((~p24(X29, X31)) | (~p19(X30, X32)) | p19(f25(X29, X30), f25(X31, X32)))) | (~p24(f28(c64, c65), f28(c64, c65))) | (~p19(c60, c60)) | p19(f25(f28(c64, c65), c60), f25(f28(c64, c65), c60))),
% 0.12/0.41 inference(modus_ponens,[status(thm)],[130, 129])).
% 0.12/0.41 tff(132,plain,
% 0.12/0.41 ((~p24(f28(c64, c65), f28(c64, c65))) | (~p19(c60, c60)) | p19(f25(f28(c64, c65), c60), f25(f28(c64, c65), c60))),
% 0.19/0.41 inference(unit_resolution,[status(thm)],[131, 128])).
% 0.19/0.41 tff(133,plain,
% 0.19/0.41 ((~p24(f28(c64, c65), f28(c64, c65))) | p19(f25(f28(c64, c65), c60), f25(f28(c64, c65), c60))),
% 0.19/0.41 inference(unit_resolution,[status(thm)],[132, 118])).
% 0.19/0.41 tff(134,plain,
% 0.19/0.41 (p19(f25(f28(c64, c65), c60), f25(f28(c64, c65), c60))),
% 0.19/0.41 inference(unit_resolution,[status(thm)],[133, 107])).
% 0.19/0.41 tff(135,plain,
% 0.19/0.41 ((~p47(f31(f33(c62, c63), f34(c65, c56)), f25(f28(c64, c65), c60))) <=> (~p47(f31(f33(c62, c63), f34(c65, c56)), f25(f28(c64, c65), c60)))),
% 0.19/0.41 inference(rewrite,[status(thm)],[])).
% 0.19/0.41 tff(136,axiom,(~p47(f31(f33(c62, c63), f34(c65, c56)), f25(f28(c64, c65), c60))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','not_p47_64')).
% 0.19/0.41 tff(137,plain,
% 0.19/0.41 (~p47(f31(f33(c62, c63), f34(c65, c56)), f25(f28(c64, c65), c60))),
% 0.19/0.41 inference(modus_ponens,[status(thm)],[136, 135])).
% 0.19/0.41 tff(138,plain,
% 0.19/0.41 (^[X144: $i, X142: $i, X143: $i, X145: $i] : refl(((~p30(X145, X142)) | (~p19(X144, X143)) | (~p47(X145, X144)) | p47(X142, X143)) <=> ((~p30(X145, X142)) | (~p19(X144, X143)) | (~p47(X145, X144)) | p47(X142, X143)))),
% 0.19/0.41 inference(bind,[status(th)],[])).
% 0.19/0.41 tff(139,plain,
% 0.19/0.41 (![X144: $i, X142: $i, X143: $i, X145: $i] : ((~p30(X145, X142)) | (~p19(X144, X143)) | (~p47(X145, X144)) | p47(X142, X143)) <=> ![X144: $i, X142: $i, X143: $i, X145: $i] : ((~p30(X145, X142)) | (~p19(X144, X143)) | (~p47(X145, X144)) | p47(X142, X143))),
% 0.19/0.41 inference(quant_intro,[status(thm)],[138])).
% 0.19/0.41 tff(140,plain,
% 0.19/0.41 (![X144: $i, X142: $i, X143: $i, X145: $i] : ((~p30(X145, X142)) | (~p19(X144, X143)) | (~p47(X145, X144)) | p47(X142, X143)) <=> ![X144: $i, X142: $i, X143: $i, X145: $i] : ((~p30(X145, X142)) | (~p19(X144, X143)) | (~p47(X145, X144)) | p47(X142, X143))),
% 0.19/0.41 inference(rewrite,[status(thm)],[])).
% 0.19/0.41 tff(141,plain,
% 0.19/0.41 (^[X144: $i, X142: $i, X143: $i, X145: $i] : trans(monotonicity(trans(monotonicity(rewrite((p47(X142, X143) | (~p30(X145, X142))) <=> ((~p30(X145, X142)) | p47(X142, X143))), (((p47(X142, X143) | (~p30(X145, X142))) | (~p47(X145, X144))) <=> (((~p30(X145, X142)) | p47(X142, X143)) | (~p47(X145, X144))))), rewrite((((~p30(X145, X142)) | p47(X142, X143)) | (~p47(X145, X144))) <=> ((~p30(X145, X142)) | (~p47(X145, X144)) | p47(X142, X143))), (((p47(X142, X143) | (~p30(X145, X142))) | (~p47(X145, X144))) <=> ((~p30(X145, X142)) | (~p47(X145, X144)) | p47(X142, X143)))), ((((p47(X142, X143) | (~p30(X145, X142))) | (~p47(X145, X144))) | (~p19(X144, X143))) <=> (((~p30(X145, X142)) | (~p47(X145, X144)) | p47(X142, X143)) | (~p19(X144, X143))))), rewrite((((~p30(X145, X142)) | (~p47(X145, X144)) | p47(X142, X143)) | (~p19(X144, X143))) <=> ((~p30(X145, X142)) | (~p19(X144, X143)) | (~p47(X145, X144)) | p47(X142, X143))), ((((p47(X142, X143) | (~p30(X145, X142))) | (~p47(X145, X144))) | (~p19(X144, X143))) <=> ((~p30(X145, X142)) | (~p19(X144, X143)) | (~p47(X145, X144)) | p47(X142, X143))))),
% 0.19/0.41 inference(bind,[status(th)],[])).
% 0.19/0.41 tff(142,plain,
% 0.19/0.41 (![X144: $i, X142: $i, X143: $i, X145: $i] : (((p47(X142, X143) | (~p30(X145, X142))) | (~p47(X145, X144))) | (~p19(X144, X143))) <=> ![X144: $i, X142: $i, X143: $i, X145: $i] : ((~p30(X145, X142)) | (~p19(X144, X143)) | (~p47(X145, X144)) | p47(X142, X143))),
% 0.19/0.41 inference(quant_intro,[status(thm)],[141])).
% 0.19/0.41 tff(143,axiom,(![X144: $i, X142: $i, X143: $i, X145: $i] : (((p47(X142, X143) | (~p30(X145, X142))) | (~p47(X145, X144))) | (~p19(X144, X143)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','p47_60')).
% 0.19/0.41 tff(144,plain,
% 0.19/0.41 (![X144: $i, X142: $i, X143: $i, X145: $i] : ((~p30(X145, X142)) | (~p19(X144, X143)) | (~p47(X145, X144)) | p47(X142, X143))),
% 0.19/0.41 inference(modus_ponens,[status(thm)],[143, 142])).
% 0.19/0.41 tff(145,plain,
% 0.19/0.41 (![X144: $i, X142: $i, X143: $i, X145: $i] : ((~p30(X145, X142)) | (~p19(X144, X143)) | (~p47(X145, X144)) | p47(X142, X143))),
% 0.19/0.41 inference(modus_ponens,[status(thm)],[144, 140])).
% 0.19/0.41 tff(146,plain,(
% 0.19/0.41 ![X144: $i, X142: $i, X143: $i, X145: $i] : ((~p30(X145, X142)) | (~p19(X144, X143)) | (~p47(X145, X144)) | p47(X142, X143))),
% 0.19/0.42 inference(skolemize,[status(sab)],[145])).
% 0.19/0.42 tff(147,plain,
% 0.19/0.42 (![X144: $i, X142: $i, X143: $i, X145: $i] : ((~p30(X145, X142)) | (~p19(X144, X143)) | (~p47(X145, X144)) | p47(X142, X143))),
% 0.19/0.42 inference(modus_ponens,[status(thm)],[146, 139])).
% 0.19/0.42 tff(148,plain,
% 0.19/0.42 (((~![X144: $i, X142: $i, X143: $i, X145: $i] : ((~p30(X145, X142)) | (~p19(X144, X143)) | (~p47(X145, X144)) | p47(X142, X143))) | (p47(f31(f33(c62, c63), f34(c65, c56)), f25(f28(c64, c65), c60)) | (~p30(f31(f33(c62, c63), f25(f28(c64, c65), f34(c66, c56))), f31(f33(c62, c63), f34(c65, c56)))) | (~p19(f25(f28(c64, c65), c60), f25(f28(c64, c65), c60))) | (~p47(f31(f33(c62, c63), f25(f28(c64, c65), f34(c66, c56))), f25(f28(c64, c65), c60))))) <=> ((~![X144: $i, X142: $i, X143: $i, X145: $i] : ((~p30(X145, X142)) | (~p19(X144, X143)) | (~p47(X145, X144)) | p47(X142, X143))) | p47(f31(f33(c62, c63), f34(c65, c56)), f25(f28(c64, c65), c60)) | (~p30(f31(f33(c62, c63), f25(f28(c64, c65), f34(c66, c56))), f31(f33(c62, c63), f34(c65, c56)))) | (~p19(f25(f28(c64, c65), c60), f25(f28(c64, c65), c60))) | (~p47(f31(f33(c62, c63), f25(f28(c64, c65), f34(c66, c56))), f25(f28(c64, c65), c60))))),
% 0.19/0.42 inference(rewrite,[status(thm)],[])).
% 0.19/0.42 tff(149,plain,
% 0.19/0.42 (((~p30(f31(f33(c62, c63), f25(f28(c64, c65), f34(c66, c56))), f31(f33(c62, c63), f34(c65, c56)))) | (~p19(f25(f28(c64, c65), c60), f25(f28(c64, c65), c60))) | (~p47(f31(f33(c62, c63), f25(f28(c64, c65), f34(c66, c56))), f25(f28(c64, c65), c60))) | p47(f31(f33(c62, c63), f34(c65, c56)), f25(f28(c64, c65), c60))) <=> (p47(f31(f33(c62, c63), f34(c65, c56)), f25(f28(c64, c65), c60)) | (~p30(f31(f33(c62, c63), f25(f28(c64, c65), f34(c66, c56))), f31(f33(c62, c63), f34(c65, c56)))) | (~p19(f25(f28(c64, c65), c60), f25(f28(c64, c65), c60))) | (~p47(f31(f33(c62, c63), f25(f28(c64, c65), f34(c66, c56))), f25(f28(c64, c65), c60))))),
% 0.19/0.42 inference(rewrite,[status(thm)],[])).
% 0.19/0.42 tff(150,plain,
% 0.19/0.42 (((~![X144: $i, X142: $i, X143: $i, X145: $i] : ((~p30(X145, X142)) | (~p19(X144, X143)) | (~p47(X145, X144)) | p47(X142, X143))) | ((~p30(f31(f33(c62, c63), f25(f28(c64, c65), f34(c66, c56))), f31(f33(c62, c63), f34(c65, c56)))) | (~p19(f25(f28(c64, c65), c60), f25(f28(c64, c65), c60))) | (~p47(f31(f33(c62, c63), f25(f28(c64, c65), f34(c66, c56))), f25(f28(c64, c65), c60))) | p47(f31(f33(c62, c63), f34(c65, c56)), f25(f28(c64, c65), c60)))) <=> ((~![X144: $i, X142: $i, X143: $i, X145: $i] : ((~p30(X145, X142)) | (~p19(X144, X143)) | (~p47(X145, X144)) | p47(X142, X143))) | (p47(f31(f33(c62, c63), f34(c65, c56)), f25(f28(c64, c65), c60)) | (~p30(f31(f33(c62, c63), f25(f28(c64, c65), f34(c66, c56))), f31(f33(c62, c63), f34(c65, c56)))) | (~p19(f25(f28(c64, c65), c60), f25(f28(c64, c65), c60))) | (~p47(f31(f33(c62, c63), f25(f28(c64, c65), f34(c66, c56))), f25(f28(c64, c65), c60)))))),
% 0.19/0.42 inference(monotonicity,[status(thm)],[149])).
% 0.19/0.42 tff(151,plain,
% 0.19/0.42 (((~![X144: $i, X142: $i, X143: $i, X145: $i] : ((~p30(X145, X142)) | (~p19(X144, X143)) | (~p47(X145, X144)) | p47(X142, X143))) | ((~p30(f31(f33(c62, c63), f25(f28(c64, c65), f34(c66, c56))), f31(f33(c62, c63), f34(c65, c56)))) | (~p19(f25(f28(c64, c65), c60), f25(f28(c64, c65), c60))) | (~p47(f31(f33(c62, c63), f25(f28(c64, c65), f34(c66, c56))), f25(f28(c64, c65), c60))) | p47(f31(f33(c62, c63), f34(c65, c56)), f25(f28(c64, c65), c60)))) <=> ((~![X144: $i, X142: $i, X143: $i, X145: $i] : ((~p30(X145, X142)) | (~p19(X144, X143)) | (~p47(X145, X144)) | p47(X142, X143))) | p47(f31(f33(c62, c63), f34(c65, c56)), f25(f28(c64, c65), c60)) | (~p30(f31(f33(c62, c63), f25(f28(c64, c65), f34(c66, c56))), f31(f33(c62, c63), f34(c65, c56)))) | (~p19(f25(f28(c64, c65), c60), f25(f28(c64, c65), c60))) | (~p47(f31(f33(c62, c63), f25(f28(c64, c65), f34(c66, c56))), f25(f28(c64, c65), c60))))),
% 0.19/0.42 inference(transitivity,[status(thm)],[150, 148])).
% 0.19/0.42 tff(152,plain,
% 0.19/0.42 ((~![X144: $i, X142: $i, X143: $i, X145: $i] : ((~p30(X145, X142)) | (~p19(X144, X143)) | (~p47(X145, X144)) | p47(X142, X143))) | ((~p30(f31(f33(c62, c63), f25(f28(c64, c65), f34(c66, c56))), f31(f33(c62, c63), f34(c65, c56)))) | (~p19(f25(f28(c64, c65), c60), f25(f28(c64, c65), c60))) | (~p47(f31(f33(c62, c63), f25(f28(c64, c65), f34(c66, c56))), f25(f28(c64, c65), c60))) | p47(f31(f33(c62, c63), f34(c65, c56)), f25(f28(c64, c65), c60)))),
% 0.19/0.42 inference(quant_inst,[status(thm)],[])).
% 0.19/0.42 tff(153,plain,
% 0.19/0.42 ((~![X144: $i, X142: $i, X143: $i, X145: $i] : ((~p30(X145, X142)) | (~p19(X144, X143)) | (~p47(X145, X144)) | p47(X142, X143))) | p47(f31(f33(c62, c63), f34(c65, c56)), f25(f28(c64, c65), c60)) | (~p30(f31(f33(c62, c63), f25(f28(c64, c65), f34(c66, c56))), f31(f33(c62, c63), f34(c65, c56)))) | (~p19(f25(f28(c64, c65), c60), f25(f28(c64, c65), c60))) | (~p47(f31(f33(c62, c63), f25(f28(c64, c65), f34(c66, c56))), f25(f28(c64, c65), c60)))),
% 0.19/0.42 inference(modus_ponens,[status(thm)],[152, 151])).
% 0.19/0.42 tff(154,plain,
% 0.19/0.42 ($false),
% 0.19/0.42 inference(unit_resolution,[status(thm)],[153, 147, 137, 134, 69, 35])).
% 0.19/0.42 % SZS output end Proof
% 0.19/0.42 % E exiting
%------------------------------------------------------------------------------