%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : SYN614-1 : TPTP v9.0.0. Released v2.5.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n009.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:41 AM UTC 2025
% Result : Unsatisfiable 0.18s 0.39s
% Output : Proof 0.19s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : SYN614-1 : TPTP v9.0.0. Released v2.5.0.
% 0.11/0.12 % Command : run_E %s %d THM
% 0.12/0.33 % Computer : n009.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:38:48 EDT 2025
% 0.12/0.33 % CPUTime :
% 0.18/0.39 % SZS status Unsatisfiable
% 0.18/0.39 % SZS output start Proof
% 0.18/0.39 tff(p7_type, type, (
% 0.18/0.39 p7: ( $i * $i ) > $o)).
% 0.18/0.39 tff(c25_type, type, (
% 0.18/0.39 c25: $i)).
% 0.18/0.39 tff(f8_type, type, (
% 0.18/0.39 f8: ( $i * $i ) > $i)).
% 0.18/0.39 tff(f9_type, type, (
% 0.18/0.39 f9: ( $i * $i ) > $i)).
% 0.18/0.39 tff(f10_type, type, (
% 0.18/0.39 f10: ( $i * $i ) > $i)).
% 0.18/0.39 tff(c27_type, type, (
% 0.18/0.39 c27: $i)).
% 0.18/0.39 tff(f11_type, type, (
% 0.18/0.39 f11: $i > $i)).
% 0.18/0.39 tff(f3_type, type, (
% 0.18/0.39 f3: $i > $i)).
% 0.18/0.39 tff(f4_type, type, (
% 0.18/0.39 f4: $i > $i)).
% 0.18/0.39 tff(f5_type, type, (
% 0.18/0.39 f5: $i > $i)).
% 0.18/0.39 tff(c22_type, type, (
% 0.18/0.39 c22: $i)).
% 0.18/0.39 tff(c24_type, type, (
% 0.18/0.39 c24: $i)).
% 0.18/0.39 tff(c26_type, type, (
% 0.18/0.39 c26: $i)).
% 0.18/0.39 tff(c23_type, type, (
% 0.18/0.39 c23: $i)).
% 0.18/0.39 tff(f12_type, type, (
% 0.18/0.39 f12: $i > $i)).
% 0.18/0.39 tff(f14_type, type, (
% 0.18/0.39 f14: ( $i * $i ) > $i)).
% 0.18/0.39 tff(f16_type, type, (
% 0.18/0.39 f16: ( $i * $i ) > $i)).
% 0.18/0.39 tff(f17_type, type, (
% 0.18/0.39 f17: ( $i * $i ) > $i)).
% 0.18/0.39 tff(c21_type, type, (
% 0.18/0.39 c21: $i)).
% 0.18/0.39 tff(c28_type, type, (
% 0.18/0.39 c28: $i)).
% 0.18/0.39 tff(p2_type, type, (
% 0.18/0.39 p2: ( $i * $i ) > $o)).
% 0.18/0.39 tff(p19_type, type, (
% 0.18/0.39 p19: ( $i * $i ) > $o)).
% 0.18/0.39 tff(f6_type, type, (
% 0.18/0.39 f6: ( $i * $i ) > $i)).
% 0.18/0.39 tff(f18_type, type, (
% 0.18/0.39 f18: ( $i * $i ) > $i)).
% 0.18/0.39 tff(p20_type, type, (
% 0.18/0.39 p20: ( $i * $i ) > $o)).
% 0.18/0.39 tff(1,assumption,(~p7(f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27)), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27)))), introduced(assumption)).
% 0.18/0.39 tff(2,plain,
% 0.18/0.39 (^[X43: $i] : refl(p7(X43, X43) <=> p7(X43, X43))),
% 0.18/0.39 inference(bind,[status(th)],[])).
% 0.18/0.39 tff(3,plain,
% 0.18/0.39 (![X43: $i] : p7(X43, X43) <=> ![X43: $i] : p7(X43, X43)),
% 0.18/0.39 inference(quant_intro,[status(thm)],[2])).
% 0.18/0.39 tff(4,plain,
% 0.18/0.39 (![X43: $i] : p7(X43, X43) <=> ![X43: $i] : p7(X43, X43)),
% 0.18/0.39 inference(rewrite,[status(thm)],[])).
% 0.18/0.39 tff(5,axiom,(![X43: $i] : p7(X43, X43)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','p7_2')).
% 0.18/0.39 tff(6,plain,
% 0.18/0.39 (![X43: $i] : p7(X43, X43)),
% 0.18/0.39 inference(modus_ponens,[status(thm)],[5, 4])).
% 0.18/0.39 tff(7,plain,(
% 0.18/0.39 ![X43: $i] : p7(X43, X43)),
% 0.18/0.39 inference(skolemize,[status(sab)],[6])).
% 0.18/0.39 tff(8,plain,
% 0.18/0.39 (![X43: $i] : p7(X43, X43)),
% 0.18/0.39 inference(modus_ponens,[status(thm)],[7, 3])).
% 0.18/0.39 tff(9,plain,
% 0.18/0.39 ((~![X43: $i] : p7(X43, X43)) | p7(f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27)), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27)))),
% 0.18/0.39 inference(quant_inst,[status(thm)],[])).
% 0.18/0.39 tff(10,plain,
% 0.18/0.39 ($false),
% 0.18/0.39 inference(unit_resolution,[status(thm)],[9, 8, 1])).
% 0.18/0.39 tff(11,plain,(p7(f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27)), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27)))), inference(lemma,lemma(discharge,[]))).
% 0.18/0.39 tff(12,assumption,(~p2(c22, c22)), introduced(assumption)).
% 0.18/0.39 tff(13,plain,
% 0.18/0.39 (^[X18: $i] : refl(p2(X18, X18) <=> p2(X18, X18))),
% 0.18/0.39 inference(bind,[status(th)],[])).
% 0.18/0.39 tff(14,plain,
% 0.18/0.39 (![X18: $i] : p2(X18, X18) <=> ![X18: $i] : p2(X18, X18)),
% 0.18/0.39 inference(quant_intro,[status(thm)],[13])).
% 0.18/0.39 tff(15,plain,
% 0.18/0.39 (![X18: $i] : p2(X18, X18) <=> ![X18: $i] : p2(X18, X18)),
% 0.18/0.39 inference(rewrite,[status(thm)],[])).
% 0.18/0.39 tff(16,axiom,(![X18: $i] : p2(X18, X18)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','p2_3')).
% 0.18/0.39 tff(17,plain,
% 0.18/0.39 (![X18: $i] : p2(X18, X18)),
% 0.18/0.39 inference(modus_ponens,[status(thm)],[16, 15])).
% 0.18/0.39 tff(18,plain,(
% 0.18/0.40 ![X18: $i] : p2(X18, X18)),
% 0.18/0.40 inference(skolemize,[status(sab)],[17])).
% 0.18/0.40 tff(19,plain,
% 0.18/0.40 (![X18: $i] : p2(X18, X18)),
% 0.18/0.40 inference(modus_ponens,[status(thm)],[18, 14])).
% 0.18/0.40 tff(20,plain,
% 0.18/0.40 ((~![X18: $i] : p2(X18, X18)) | p2(c22, c22)),
% 0.18/0.40 inference(quant_inst,[status(thm)],[])).
% 0.18/0.40 tff(21,plain,
% 0.18/0.40 ($false),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[20, 19, 12])).
% 0.18/0.40 tff(22,plain,(p2(c22, c22)), inference(lemma,lemma(discharge,[]))).
% 0.18/0.40 tff(23,plain,
% 0.18/0.40 (^[X34: $i, X33: $i] : refl(((~p2(X33, X34)) | p2(f5(X33), f5(X34))) <=> ((~p2(X33, X34)) | p2(f5(X33), f5(X34))))),
% 0.18/0.40 inference(bind,[status(th)],[])).
% 0.18/0.40 tff(24,plain,
% 0.18/0.40 (![X34: $i, X33: $i] : ((~p2(X33, X34)) | p2(f5(X33), f5(X34))) <=> ![X34: $i, X33: $i] : ((~p2(X33, X34)) | p2(f5(X33), f5(X34)))),
% 0.18/0.40 inference(quant_intro,[status(thm)],[23])).
% 0.18/0.40 tff(25,plain,
% 0.18/0.40 (![X34: $i, X33: $i] : ((~p2(X33, X34)) | p2(f5(X33), f5(X34))) <=> ![X34: $i, X33: $i] : ((~p2(X33, X34)) | p2(f5(X33), f5(X34)))),
% 0.18/0.40 inference(rewrite,[status(thm)],[])).
% 0.18/0.40 tff(26,plain,
% 0.18/0.40 (^[X34: $i, X33: $i] : rewrite((p2(f5(X33), f5(X34)) | (~p2(X33, X34))) <=> ((~p2(X33, X34)) | p2(f5(X33), f5(X34))))),
% 0.18/0.40 inference(bind,[status(th)],[])).
% 0.18/0.40 tff(27,plain,
% 0.18/0.40 (![X34: $i, X33: $i] : (p2(f5(X33), f5(X34)) | (~p2(X33, X34))) <=> ![X34: $i, X33: $i] : ((~p2(X33, X34)) | p2(f5(X33), f5(X34)))),
% 0.18/0.40 inference(quant_intro,[status(thm)],[26])).
% 0.18/0.40 tff(28,axiom,(![X34: $i, X33: $i] : (p2(f5(X33), f5(X34)) | (~p2(X33, X34)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','p2_11')).
% 0.18/0.40 tff(29,plain,
% 0.18/0.40 (![X34: $i, X33: $i] : ((~p2(X33, X34)) | p2(f5(X33), f5(X34)))),
% 0.18/0.40 inference(modus_ponens,[status(thm)],[28, 27])).
% 0.18/0.40 tff(30,plain,
% 0.18/0.40 (![X34: $i, X33: $i] : ((~p2(X33, X34)) | p2(f5(X33), f5(X34)))),
% 0.18/0.40 inference(modus_ponens,[status(thm)],[29, 25])).
% 0.18/0.40 tff(31,plain,(
% 0.18/0.40 ![X34: $i, X33: $i] : ((~p2(X33, X34)) | p2(f5(X33), f5(X34)))),
% 0.18/0.40 inference(skolemize,[status(sab)],[30])).
% 0.18/0.40 tff(32,plain,
% 0.18/0.40 (![X34: $i, X33: $i] : ((~p2(X33, X34)) | p2(f5(X33), f5(X34)))),
% 0.18/0.40 inference(modus_ponens,[status(thm)],[31, 24])).
% 0.18/0.40 tff(33,plain,
% 0.18/0.40 (((~![X34: $i, X33: $i] : ((~p2(X33, X34)) | p2(f5(X33), f5(X34)))) | ((~p2(c22, c22)) | p2(f5(c22), f5(c22)))) <=> ((~![X34: $i, X33: $i] : ((~p2(X33, X34)) | p2(f5(X33), f5(X34)))) | (~p2(c22, c22)) | p2(f5(c22), f5(c22)))),
% 0.18/0.40 inference(rewrite,[status(thm)],[])).
% 0.18/0.40 tff(34,plain,
% 0.18/0.40 ((~![X34: $i, X33: $i] : ((~p2(X33, X34)) | p2(f5(X33), f5(X34)))) | ((~p2(c22, c22)) | p2(f5(c22), f5(c22)))),
% 0.18/0.40 inference(quant_inst,[status(thm)],[])).
% 0.18/0.40 tff(35,plain,
% 0.18/0.40 ((~![X34: $i, X33: $i] : ((~p2(X33, X34)) | p2(f5(X33), f5(X34)))) | (~p2(c22, c22)) | p2(f5(c22), f5(c22))),
% 0.18/0.40 inference(modus_ponens,[status(thm)],[34, 33])).
% 0.18/0.40 tff(36,plain,
% 0.18/0.40 ((~p2(c22, c22)) | p2(f5(c22), f5(c22))),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[35, 32])).
% 0.18/0.40 tff(37,plain,
% 0.18/0.40 (p2(f5(c22), f5(c22))),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[36, 22])).
% 0.18/0.40 tff(38,plain,
% 0.18/0.40 (^[X31: $i, X32: $i] : refl(((~p2(X31, X32)) | p2(f4(X31), f4(X32))) <=> ((~p2(X31, X32)) | p2(f4(X31), f4(X32))))),
% 0.18/0.40 inference(bind,[status(th)],[])).
% 0.18/0.40 tff(39,plain,
% 0.18/0.40 (![X31: $i, X32: $i] : ((~p2(X31, X32)) | p2(f4(X31), f4(X32))) <=> ![X31: $i, X32: $i] : ((~p2(X31, X32)) | p2(f4(X31), f4(X32)))),
% 0.18/0.40 inference(quant_intro,[status(thm)],[38])).
% 0.18/0.40 tff(40,plain,
% 0.18/0.40 (![X31: $i, X32: $i] : ((~p2(X31, X32)) | p2(f4(X31), f4(X32))) <=> ![X31: $i, X32: $i] : ((~p2(X31, X32)) | p2(f4(X31), f4(X32)))),
% 0.18/0.40 inference(rewrite,[status(thm)],[])).
% 0.18/0.40 tff(41,plain,
% 0.18/0.40 (^[X31: $i, X32: $i] : rewrite((p2(f4(X31), f4(X32)) | (~p2(X31, X32))) <=> ((~p2(X31, X32)) | p2(f4(X31), f4(X32))))),
% 0.18/0.40 inference(bind,[status(th)],[])).
% 0.18/0.40 tff(42,plain,
% 0.18/0.40 (![X31: $i, X32: $i] : (p2(f4(X31), f4(X32)) | (~p2(X31, X32))) <=> ![X31: $i, X32: $i] : ((~p2(X31, X32)) | p2(f4(X31), f4(X32)))),
% 0.18/0.40 inference(quant_intro,[status(thm)],[41])).
% 0.18/0.40 tff(43,axiom,(![X31: $i, X32: $i] : (p2(f4(X31), f4(X32)) | (~p2(X31, X32)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','p2_10')).
% 0.18/0.40 tff(44,plain,
% 0.18/0.40 (![X31: $i, X32: $i] : ((~p2(X31, X32)) | p2(f4(X31), f4(X32)))),
% 0.18/0.40 inference(modus_ponens,[status(thm)],[43, 42])).
% 0.18/0.40 tff(45,plain,
% 0.18/0.40 (![X31: $i, X32: $i] : ((~p2(X31, X32)) | p2(f4(X31), f4(X32)))),
% 0.18/0.40 inference(modus_ponens,[status(thm)],[44, 40])).
% 0.18/0.40 tff(46,plain,(
% 0.18/0.40 ![X31: $i, X32: $i] : ((~p2(X31, X32)) | p2(f4(X31), f4(X32)))),
% 0.18/0.40 inference(skolemize,[status(sab)],[45])).
% 0.18/0.40 tff(47,plain,
% 0.18/0.40 (![X31: $i, X32: $i] : ((~p2(X31, X32)) | p2(f4(X31), f4(X32)))),
% 0.18/0.40 inference(modus_ponens,[status(thm)],[46, 39])).
% 0.18/0.40 tff(48,plain,
% 0.18/0.40 (((~![X31: $i, X32: $i] : ((~p2(X31, X32)) | p2(f4(X31), f4(X32)))) | ((~p2(f5(c22), f5(c22))) | p2(f4(f5(c22)), f4(f5(c22))))) <=> ((~![X31: $i, X32: $i] : ((~p2(X31, X32)) | p2(f4(X31), f4(X32)))) | (~p2(f5(c22), f5(c22))) | p2(f4(f5(c22)), f4(f5(c22))))),
% 0.18/0.40 inference(rewrite,[status(thm)],[])).
% 0.18/0.40 tff(49,plain,
% 0.18/0.40 ((~![X31: $i, X32: $i] : ((~p2(X31, X32)) | p2(f4(X31), f4(X32)))) | ((~p2(f5(c22), f5(c22))) | p2(f4(f5(c22)), f4(f5(c22))))),
% 0.18/0.40 inference(quant_inst,[status(thm)],[])).
% 0.18/0.40 tff(50,plain,
% 0.18/0.40 ((~![X31: $i, X32: $i] : ((~p2(X31, X32)) | p2(f4(X31), f4(X32)))) | (~p2(f5(c22), f5(c22))) | p2(f4(f5(c22)), f4(f5(c22)))),
% 0.18/0.40 inference(modus_ponens,[status(thm)],[49, 48])).
% 0.18/0.40 tff(51,plain,
% 0.18/0.40 ((~p2(f5(c22), f5(c22))) | p2(f4(f5(c22)), f4(f5(c22)))),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[50, 47])).
% 0.18/0.40 tff(52,plain,
% 0.18/0.40 (p2(f4(f5(c22)), f4(f5(c22)))),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[51, 37])).
% 0.18/0.40 tff(53,plain,
% 0.18/0.40 (^[X30: $i, X29: $i] : refl(((~p2(X29, X30)) | p2(f3(X29), f3(X30))) <=> ((~p2(X29, X30)) | p2(f3(X29), f3(X30))))),
% 0.18/0.40 inference(bind,[status(th)],[])).
% 0.18/0.40 tff(54,plain,
% 0.18/0.40 (![X30: $i, X29: $i] : ((~p2(X29, X30)) | p2(f3(X29), f3(X30))) <=> ![X30: $i, X29: $i] : ((~p2(X29, X30)) | p2(f3(X29), f3(X30)))),
% 0.18/0.40 inference(quant_intro,[status(thm)],[53])).
% 0.18/0.40 tff(55,plain,
% 0.18/0.40 (![X30: $i, X29: $i] : ((~p2(X29, X30)) | p2(f3(X29), f3(X30))) <=> ![X30: $i, X29: $i] : ((~p2(X29, X30)) | p2(f3(X29), f3(X30)))),
% 0.18/0.40 inference(rewrite,[status(thm)],[])).
% 0.18/0.40 tff(56,plain,
% 0.18/0.40 (^[X30: $i, X29: $i] : rewrite((p2(f3(X29), f3(X30)) | (~p2(X29, X30))) <=> ((~p2(X29, X30)) | p2(f3(X29), f3(X30))))),
% 0.18/0.40 inference(bind,[status(th)],[])).
% 0.18/0.40 tff(57,plain,
% 0.18/0.40 (![X30: $i, X29: $i] : (p2(f3(X29), f3(X30)) | (~p2(X29, X30))) <=> ![X30: $i, X29: $i] : ((~p2(X29, X30)) | p2(f3(X29), f3(X30)))),
% 0.18/0.40 inference(quant_intro,[status(thm)],[56])).
% 0.18/0.40 tff(58,axiom,(![X30: $i, X29: $i] : (p2(f3(X29), f3(X30)) | (~p2(X29, X30)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','p2_9')).
% 0.18/0.40 tff(59,plain,
% 0.18/0.40 (![X30: $i, X29: $i] : ((~p2(X29, X30)) | p2(f3(X29), f3(X30)))),
% 0.18/0.40 inference(modus_ponens,[status(thm)],[58, 57])).
% 0.18/0.40 tff(60,plain,
% 0.18/0.40 (![X30: $i, X29: $i] : ((~p2(X29, X30)) | p2(f3(X29), f3(X30)))),
% 0.18/0.40 inference(modus_ponens,[status(thm)],[59, 55])).
% 0.18/0.40 tff(61,plain,(
% 0.18/0.40 ![X30: $i, X29: $i] : ((~p2(X29, X30)) | p2(f3(X29), f3(X30)))),
% 0.18/0.40 inference(skolemize,[status(sab)],[60])).
% 0.18/0.40 tff(62,plain,
% 0.18/0.40 (![X30: $i, X29: $i] : ((~p2(X29, X30)) | p2(f3(X29), f3(X30)))),
% 0.18/0.40 inference(modus_ponens,[status(thm)],[61, 54])).
% 0.18/0.40 tff(63,plain,
% 0.18/0.40 (((~![X30: $i, X29: $i] : ((~p2(X29, X30)) | p2(f3(X29), f3(X30)))) | ((~p2(f4(f5(c22)), f4(f5(c22)))) | p2(f3(f4(f5(c22))), f3(f4(f5(c22)))))) <=> ((~![X30: $i, X29: $i] : ((~p2(X29, X30)) | p2(f3(X29), f3(X30)))) | (~p2(f4(f5(c22)), f4(f5(c22)))) | p2(f3(f4(f5(c22))), f3(f4(f5(c22)))))),
% 0.18/0.40 inference(rewrite,[status(thm)],[])).
% 0.18/0.40 tff(64,plain,
% 0.18/0.40 ((~![X30: $i, X29: $i] : ((~p2(X29, X30)) | p2(f3(X29), f3(X30)))) | ((~p2(f4(f5(c22)), f4(f5(c22)))) | p2(f3(f4(f5(c22))), f3(f4(f5(c22)))))),
% 0.18/0.40 inference(quant_inst,[status(thm)],[])).
% 0.18/0.40 tff(65,plain,
% 0.18/0.40 ((~![X30: $i, X29: $i] : ((~p2(X29, X30)) | p2(f3(X29), f3(X30)))) | (~p2(f4(f5(c22)), f4(f5(c22)))) | p2(f3(f4(f5(c22))), f3(f4(f5(c22))))),
% 0.18/0.40 inference(modus_ponens,[status(thm)],[64, 63])).
% 0.18/0.40 tff(66,plain,
% 0.18/0.40 ((~p2(f4(f5(c22)), f4(f5(c22)))) | p2(f3(f4(f5(c22))), f3(f4(f5(c22))))),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[65, 62])).
% 0.18/0.40 tff(67,plain,
% 0.18/0.40 (p2(f3(f4(f5(c22))), f3(f4(f5(c22))))),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[66, 52])).
% 0.18/0.40 tff(68,plain,
% 0.18/0.40 (^[X51: $i, X50: $i] : refl(((~p2(X50, X51)) | p7(f11(X50), f11(X51))) <=> ((~p2(X50, X51)) | p7(f11(X50), f11(X51))))),
% 0.18/0.40 inference(bind,[status(th)],[])).
% 0.18/0.40 tff(69,plain,
% 0.18/0.40 (![X51: $i, X50: $i] : ((~p2(X50, X51)) | p7(f11(X50), f11(X51))) <=> ![X51: $i, X50: $i] : ((~p2(X50, X51)) | p7(f11(X50), f11(X51)))),
% 0.18/0.40 inference(quant_intro,[status(thm)],[68])).
% 0.18/0.40 tff(70,plain,
% 0.18/0.40 (![X51: $i, X50: $i] : ((~p2(X50, X51)) | p7(f11(X50), f11(X51))) <=> ![X51: $i, X50: $i] : ((~p2(X50, X51)) | p7(f11(X50), f11(X51)))),
% 0.18/0.40 inference(rewrite,[status(thm)],[])).
% 0.18/0.40 tff(71,plain,
% 0.18/0.40 (^[X51: $i, X50: $i] : rewrite((p7(f11(X50), f11(X51)) | (~p2(X50, X51))) <=> ((~p2(X50, X51)) | p7(f11(X50), f11(X51))))),
% 0.18/0.40 inference(bind,[status(th)],[])).
% 0.18/0.40 tff(72,plain,
% 0.18/0.40 (![X51: $i, X50: $i] : (p7(f11(X50), f11(X51)) | (~p2(X50, X51))) <=> ![X51: $i, X50: $i] : ((~p2(X50, X51)) | p7(f11(X50), f11(X51)))),
% 0.18/0.40 inference(quant_intro,[status(thm)],[71])).
% 0.18/0.40 tff(73,axiom,(![X51: $i, X50: $i] : (p7(f11(X50), f11(X51)) | (~p2(X50, X51)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','p7_12')).
% 0.18/0.40 tff(74,plain,
% 0.18/0.40 (![X51: $i, X50: $i] : ((~p2(X50, X51)) | p7(f11(X50), f11(X51)))),
% 0.18/0.40 inference(modus_ponens,[status(thm)],[73, 72])).
% 0.18/0.40 tff(75,plain,
% 0.18/0.40 (![X51: $i, X50: $i] : ((~p2(X50, X51)) | p7(f11(X50), f11(X51)))),
% 0.18/0.40 inference(modus_ponens,[status(thm)],[74, 70])).
% 0.18/0.40 tff(76,plain,(
% 0.18/0.40 ![X51: $i, X50: $i] : ((~p2(X50, X51)) | p7(f11(X50), f11(X51)))),
% 0.18/0.40 inference(skolemize,[status(sab)],[75])).
% 0.18/0.40 tff(77,plain,
% 0.18/0.40 (![X51: $i, X50: $i] : ((~p2(X50, X51)) | p7(f11(X50), f11(X51)))),
% 0.18/0.40 inference(modus_ponens,[status(thm)],[76, 69])).
% 0.18/0.40 tff(78,plain,
% 0.18/0.40 (((~![X51: $i, X50: $i] : ((~p2(X50, X51)) | p7(f11(X50), f11(X51)))) | ((~p2(f3(f4(f5(c22))), f3(f4(f5(c22))))) | p7(f11(f3(f4(f5(c22)))), f11(f3(f4(f5(c22))))))) <=> ((~![X51: $i, X50: $i] : ((~p2(X50, X51)) | p7(f11(X50), f11(X51)))) | (~p2(f3(f4(f5(c22))), f3(f4(f5(c22))))) | p7(f11(f3(f4(f5(c22)))), f11(f3(f4(f5(c22))))))),
% 0.18/0.40 inference(rewrite,[status(thm)],[])).
% 0.18/0.40 tff(79,plain,
% 0.18/0.40 ((~![X51: $i, X50: $i] : ((~p2(X50, X51)) | p7(f11(X50), f11(X51)))) | ((~p2(f3(f4(f5(c22))), f3(f4(f5(c22))))) | p7(f11(f3(f4(f5(c22)))), f11(f3(f4(f5(c22))))))),
% 0.18/0.40 inference(quant_inst,[status(thm)],[])).
% 0.18/0.40 tff(80,plain,
% 0.18/0.40 ((~![X51: $i, X50: $i] : ((~p2(X50, X51)) | p7(f11(X50), f11(X51)))) | (~p2(f3(f4(f5(c22))), f3(f4(f5(c22))))) | p7(f11(f3(f4(f5(c22)))), f11(f3(f4(f5(c22)))))),
% 0.18/0.40 inference(modus_ponens,[status(thm)],[79, 78])).
% 0.18/0.40 tff(81,plain,
% 0.18/0.40 (p7(f11(f3(f4(f5(c22)))), f11(f3(f4(f5(c22)))))),
% 0.18/0.40 inference(unit_resolution,[status(thm)],[80, 77, 67])).
% 0.18/0.40 tff(82,plain,
% 0.18/0.40 (^[X47: $i, X49: $i, X46: $i, X48: $i] : refl(((~p7(X46, X48)) | (~p2(X47, X49)) | p7(f10(X46, X47), f10(X48, X49))) <=> ((~p7(X46, X48)) | (~p2(X47, X49)) | p7(f10(X46, X47), f10(X48, X49))))),
% 0.18/0.40 inference(bind,[status(th)],[])).
% 0.18/0.40 tff(83,plain,
% 0.18/0.40 (![X47: $i, X49: $i, X46: $i, X48: $i] : ((~p7(X46, X48)) | (~p2(X47, X49)) | p7(f10(X46, X47), f10(X48, X49))) <=> ![X47: $i, X49: $i, X46: $i, X48: $i] : ((~p7(X46, X48)) | (~p2(X47, X49)) | p7(f10(X46, X47), f10(X48, X49)))),
% 0.18/0.40 inference(quant_intro,[status(thm)],[82])).
% 0.18/0.40 tff(84,plain,
% 0.18/0.40 (![X47: $i, X49: $i, X46: $i, X48: $i] : ((~p7(X46, X48)) | (~p2(X47, X49)) | p7(f10(X46, X47), f10(X48, X49))) <=> ![X47: $i, X49: $i, X46: $i, X48: $i] : ((~p7(X46, X48)) | (~p2(X47, X49)) | p7(f10(X46, X47), f10(X48, X49)))),
% 0.18/0.40 inference(rewrite,[status(thm)],[])).
% 0.18/0.40 tff(85,plain,
% 0.18/0.40 (^[X47: $i, X49: $i, X46: $i, X48: $i] : trans(monotonicity(rewrite((p7(f10(X46, X47), f10(X48, X49)) | (~p2(X47, X49))) <=> ((~p2(X47, X49)) | p7(f10(X46, X47), f10(X48, X49)))), (((p7(f10(X46, X47), f10(X48, X49)) | (~p2(X47, X49))) | (~p7(X46, X48))) <=> (((~p2(X47, X49)) | p7(f10(X46, X47), f10(X48, X49))) | (~p7(X46, X48))))), rewrite((((~p2(X47, X49)) | p7(f10(X46, X47), f10(X48, X49))) | (~p7(X46, X48))) <=> ((~p7(X46, X48)) | (~p2(X47, X49)) | p7(f10(X46, X47), f10(X48, X49)))), (((p7(f10(X46, X47), f10(X48, X49)) | (~p2(X47, X49))) | (~p7(X46, X48))) <=> ((~p7(X46, X48)) | (~p2(X47, X49)) | p7(f10(X46, X47), f10(X48, X49)))))),
% 0.18/0.40 inference(bind,[status(th)],[])).
% 0.18/0.40 tff(86,plain,
% 0.18/0.40 (![X47: $i, X49: $i, X46: $i, X48: $i] : ((p7(f10(X46, X47), f10(X48, X49)) | (~p2(X47, X49))) | (~p7(X46, X48))) <=> ![X47: $i, X49: $i, X46: $i, X48: $i] : ((~p7(X46, X48)) | (~p2(X47, X49)) | p7(f10(X46, X47), f10(X48, X49)))),
% 0.18/0.40 inference(quant_intro,[status(thm)],[85])).
% 0.18/0.40 tff(87,axiom,(![X47: $i, X49: $i, X46: $i, X48: $i] : ((p7(f10(X46, X47), f10(X48, X49)) | (~p2(X47, X49))) | (~p7(X46, X48)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','p7_24')).
% 0.18/0.40 tff(88,plain,
% 0.18/0.40 (![X47: $i, X49: $i, X46: $i, X48: $i] : ((~p7(X46, X48)) | (~p2(X47, X49)) | p7(f10(X46, X47), f10(X48, X49)))),
% 0.18/0.40 inference(modus_ponens,[status(thm)],[87, 86])).
% 0.18/0.40 tff(89,plain,
% 0.18/0.40 (![X47: $i, X49: $i, X46: $i, X48: $i] : ((~p7(X46, X48)) | (~p2(X47, X49)) | p7(f10(X46, X47), f10(X48, X49)))),
% 0.18/0.40 inference(modus_ponens,[status(thm)],[88, 84])).
% 0.18/0.40 tff(90,plain,(
% 0.18/0.40 ![X47: $i, X49: $i, X46: $i, X48: $i] : ((~p7(X46, X48)) | (~p2(X47, X49)) | p7(f10(X46, X47), f10(X48, X49)))),
% 0.18/0.41 inference(skolemize,[status(sab)],[89])).
% 0.18/0.41 tff(91,plain,
% 0.18/0.41 (![X47: $i, X49: $i, X46: $i, X48: $i] : ((~p7(X46, X48)) | (~p2(X47, X49)) | p7(f10(X46, X47), f10(X48, X49)))),
% 0.18/0.41 inference(modus_ponens,[status(thm)],[90, 83])).
% 0.18/0.41 tff(92,plain,
% 0.18/0.41 (p2(c26, f14(f16(c28, f17(c21, c27)), c25)) <=> p2(c26, f14(f16(c28, f17(c21, c27)), c25))),
% 0.18/0.41 inference(rewrite,[status(thm)],[])).
% 0.18/0.41 tff(93,axiom,(p2(c26, f14(f16(c28, f17(c21, c27)), c25))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','p2_13')).
% 0.18/0.41 tff(94,plain,
% 0.18/0.41 (p2(c26, f14(f16(c28, f17(c21, c27)), c25))),
% 0.18/0.41 inference(modus_ponens,[status(thm)],[93, 92])).
% 0.18/0.41 tff(95,plain,
% 0.18/0.41 (((~![X47: $i, X49: $i, X46: $i, X48: $i] : ((~p7(X46, X48)) | (~p2(X47, X49)) | p7(f10(X46, X47), f10(X48, X49)))) | ((~p2(c26, f14(f16(c28, f17(c21, c27)), c25))) | (~p7(f11(f3(f4(f5(c22)))), f11(f3(f4(f5(c22)))))) | p7(f10(f11(f3(f4(f5(c22)))), c26), f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25))))) <=> ((~![X47: $i, X49: $i, X46: $i, X48: $i] : ((~p7(X46, X48)) | (~p2(X47, X49)) | p7(f10(X46, X47), f10(X48, X49)))) | (~p2(c26, f14(f16(c28, f17(c21, c27)), c25))) | (~p7(f11(f3(f4(f5(c22)))), f11(f3(f4(f5(c22)))))) | p7(f10(f11(f3(f4(f5(c22)))), c26), f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25))))),
% 0.18/0.41 inference(rewrite,[status(thm)],[])).
% 0.18/0.41 tff(96,plain,
% 0.18/0.41 (((~p7(f11(f3(f4(f5(c22)))), f11(f3(f4(f5(c22)))))) | (~p2(c26, f14(f16(c28, f17(c21, c27)), c25))) | p7(f10(f11(f3(f4(f5(c22)))), c26), f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25)))) <=> ((~p2(c26, f14(f16(c28, f17(c21, c27)), c25))) | (~p7(f11(f3(f4(f5(c22)))), f11(f3(f4(f5(c22)))))) | p7(f10(f11(f3(f4(f5(c22)))), c26), f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25))))),
% 0.18/0.41 inference(rewrite,[status(thm)],[])).
% 0.18/0.41 tff(97,plain,
% 0.18/0.41 (((~![X47: $i, X49: $i, X46: $i, X48: $i] : ((~p7(X46, X48)) | (~p2(X47, X49)) | p7(f10(X46, X47), f10(X48, X49)))) | ((~p7(f11(f3(f4(f5(c22)))), f11(f3(f4(f5(c22)))))) | (~p2(c26, f14(f16(c28, f17(c21, c27)), c25))) | p7(f10(f11(f3(f4(f5(c22)))), c26), f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25))))) <=> ((~![X47: $i, X49: $i, X46: $i, X48: $i] : ((~p7(X46, X48)) | (~p2(X47, X49)) | p7(f10(X46, X47), f10(X48, X49)))) | ((~p2(c26, f14(f16(c28, f17(c21, c27)), c25))) | (~p7(f11(f3(f4(f5(c22)))), f11(f3(f4(f5(c22)))))) | p7(f10(f11(f3(f4(f5(c22)))), c26), f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25)))))),
% 0.18/0.41 inference(monotonicity,[status(thm)],[96])).
% 0.18/0.41 tff(98,plain,
% 0.18/0.41 (((~![X47: $i, X49: $i, X46: $i, X48: $i] : ((~p7(X46, X48)) | (~p2(X47, X49)) | p7(f10(X46, X47), f10(X48, X49)))) | ((~p7(f11(f3(f4(f5(c22)))), f11(f3(f4(f5(c22)))))) | (~p2(c26, f14(f16(c28, f17(c21, c27)), c25))) | p7(f10(f11(f3(f4(f5(c22)))), c26), f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25))))) <=> ((~![X47: $i, X49: $i, X46: $i, X48: $i] : ((~p7(X46, X48)) | (~p2(X47, X49)) | p7(f10(X46, X47), f10(X48, X49)))) | (~p2(c26, f14(f16(c28, f17(c21, c27)), c25))) | (~p7(f11(f3(f4(f5(c22)))), f11(f3(f4(f5(c22)))))) | p7(f10(f11(f3(f4(f5(c22)))), c26), f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25))))),
% 0.18/0.41 inference(transitivity,[status(thm)],[97, 95])).
% 0.18/0.41 tff(99,plain,
% 0.18/0.41 ((~![X47: $i, X49: $i, X46: $i, X48: $i] : ((~p7(X46, X48)) | (~p2(X47, X49)) | p7(f10(X46, X47), f10(X48, X49)))) | ((~p7(f11(f3(f4(f5(c22)))), f11(f3(f4(f5(c22)))))) | (~p2(c26, f14(f16(c28, f17(c21, c27)), c25))) | p7(f10(f11(f3(f4(f5(c22)))), c26), f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25))))),
% 0.18/0.41 inference(quant_inst,[status(thm)],[])).
% 0.18/0.41 tff(100,plain,
% 0.18/0.41 ((~![X47: $i, X49: $i, X46: $i, X48: $i] : ((~p7(X46, X48)) | (~p2(X47, X49)) | p7(f10(X46, X47), f10(X48, X49)))) | (~p2(c26, f14(f16(c28, f17(c21, c27)), c25))) | (~p7(f11(f3(f4(f5(c22)))), f11(f3(f4(f5(c22)))))) | p7(f10(f11(f3(f4(f5(c22)))), c26), f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25)))),
% 0.18/0.41 inference(modus_ponens,[status(thm)],[99, 98])).
% 0.18/0.41 tff(101,plain,
% 0.18/0.41 ((~p7(f11(f3(f4(f5(c22)))), f11(f3(f4(f5(c22)))))) | p7(f10(f11(f3(f4(f5(c22)))), c26), f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25)))),
% 0.18/0.41 inference(unit_resolution,[status(thm)],[100, 94, 91])).
% 0.18/0.41 tff(102,plain,
% 0.18/0.41 (p7(f10(f11(f3(f4(f5(c22)))), c26), f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25)))),
% 0.18/0.41 inference(unit_resolution,[status(thm)],[101, 81])).
% 0.18/0.41 tff(103,plain,
% 0.18/0.41 (^[X57: $i, X56: $i, X55: $i, X54: $i] : refl(((~p7(X54, X56)) | (~p7(X55, X57)) | p7(f8(X54, X55), f8(X56, X57))) <=> ((~p7(X54, X56)) | (~p7(X55, X57)) | p7(f8(X54, X55), f8(X56, X57))))),
% 0.18/0.41 inference(bind,[status(th)],[])).
% 0.18/0.41 tff(104,plain,
% 0.18/0.41 (![X57: $i, X56: $i, X55: $i, X54: $i] : ((~p7(X54, X56)) | (~p7(X55, X57)) | p7(f8(X54, X55), f8(X56, X57))) <=> ![X57: $i, X56: $i, X55: $i, X54: $i] : ((~p7(X54, X56)) | (~p7(X55, X57)) | p7(f8(X54, X55), f8(X56, X57)))),
% 0.18/0.41 inference(quant_intro,[status(thm)],[103])).
% 0.18/0.41 tff(105,plain,
% 0.18/0.41 (![X57: $i, X56: $i, X55: $i, X54: $i] : ((~p7(X54, X56)) | (~p7(X55, X57)) | p7(f8(X54, X55), f8(X56, X57))) <=> ![X57: $i, X56: $i, X55: $i, X54: $i] : ((~p7(X54, X56)) | (~p7(X55, X57)) | p7(f8(X54, X55), f8(X56, X57)))),
% 0.18/0.41 inference(rewrite,[status(thm)],[])).
% 0.18/0.41 tff(106,plain,
% 0.18/0.41 (^[X57: $i, X56: $i, X55: $i, X54: $i] : trans(monotonicity(rewrite((p7(f8(X54, X55), f8(X56, X57)) | (~p7(X54, X56))) <=> ((~p7(X54, X56)) | p7(f8(X54, X55), f8(X56, X57)))), (((p7(f8(X54, X55), f8(X56, X57)) | (~p7(X54, X56))) | (~p7(X55, X57))) <=> (((~p7(X54, X56)) | p7(f8(X54, X55), f8(X56, X57))) | (~p7(X55, X57))))), rewrite((((~p7(X54, X56)) | p7(f8(X54, X55), f8(X56, X57))) | (~p7(X55, X57))) <=> ((~p7(X54, X56)) | (~p7(X55, X57)) | p7(f8(X54, X55), f8(X56, X57)))), (((p7(f8(X54, X55), f8(X56, X57)) | (~p7(X54, X56))) | (~p7(X55, X57))) <=> ((~p7(X54, X56)) | (~p7(X55, X57)) | p7(f8(X54, X55), f8(X56, X57)))))),
% 0.18/0.41 inference(bind,[status(th)],[])).
% 0.18/0.41 tff(107,plain,
% 0.18/0.41 (![X57: $i, X56: $i, X55: $i, X54: $i] : ((p7(f8(X54, X55), f8(X56, X57)) | (~p7(X54, X56))) | (~p7(X55, X57))) <=> ![X57: $i, X56: $i, X55: $i, X54: $i] : ((~p7(X54, X56)) | (~p7(X55, X57)) | p7(f8(X54, X55), f8(X56, X57)))),
% 0.18/0.41 inference(quant_intro,[status(thm)],[106])).
% 0.18/0.41 tff(108,axiom,(![X57: $i, X56: $i, X55: $i, X54: $i] : ((p7(f8(X54, X55), f8(X56, X57)) | (~p7(X54, X56))) | (~p7(X55, X57)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','p7_23')).
% 0.18/0.41 tff(109,plain,
% 0.18/0.41 (![X57: $i, X56: $i, X55: $i, X54: $i] : ((~p7(X54, X56)) | (~p7(X55, X57)) | p7(f8(X54, X55), f8(X56, X57)))),
% 0.18/0.41 inference(modus_ponens,[status(thm)],[108, 107])).
% 0.18/0.41 tff(110,plain,
% 0.18/0.41 (![X57: $i, X56: $i, X55: $i, X54: $i] : ((~p7(X54, X56)) | (~p7(X55, X57)) | p7(f8(X54, X55), f8(X56, X57)))),
% 0.18/0.41 inference(modus_ponens,[status(thm)],[109, 105])).
% 0.18/0.41 tff(111,plain,(
% 0.18/0.41 ![X57: $i, X56: $i, X55: $i, X54: $i] : ((~p7(X54, X56)) | (~p7(X55, X57)) | p7(f8(X54, X55), f8(X56, X57)))),
% 0.18/0.41 inference(skolemize,[status(sab)],[110])).
% 0.18/0.41 tff(112,plain,
% 0.18/0.41 (![X57: $i, X56: $i, X55: $i, X54: $i] : ((~p7(X54, X56)) | (~p7(X55, X57)) | p7(f8(X54, X55), f8(X56, X57)))),
% 0.18/0.41 inference(modus_ponens,[status(thm)],[111, 104])).
% 0.18/0.41 tff(113,plain,
% 0.18/0.41 (((~![X57: $i, X56: $i, X55: $i, X54: $i] : ((~p7(X54, X56)) | (~p7(X55, X57)) | p7(f8(X54, X55), f8(X56, X57)))) | ((~p7(f10(f11(f3(f4(f5(c22)))), c26), f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25)))) | (~p7(f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27)), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27)))) | p7(f8(f10(f11(f3(f4(f5(c22)))), c26), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27))), f8(f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25)), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27)))))) <=> ((~![X57: $i, X56: $i, X55: $i, X54: $i] : ((~p7(X54, X56)) | (~p7(X55, X57)) | p7(f8(X54, X55), f8(X56, X57)))) | (~p7(f10(f11(f3(f4(f5(c22)))), c26), f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25)))) | (~p7(f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27)), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27)))) | p7(f8(f10(f11(f3(f4(f5(c22)))), c26), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27))), f8(f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25)), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27)))))),
% 0.18/0.41 inference(rewrite,[status(thm)],[])).
% 0.18/0.41 tff(114,plain,
% 0.18/0.41 ((~![X57: $i, X56: $i, X55: $i, X54: $i] : ((~p7(X54, X56)) | (~p7(X55, X57)) | p7(f8(X54, X55), f8(X56, X57)))) | ((~p7(f10(f11(f3(f4(f5(c22)))), c26), f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25)))) | (~p7(f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27)), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27)))) | p7(f8(f10(f11(f3(f4(f5(c22)))), c26), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27))), f8(f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25)), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27)))))),
% 0.18/0.41 inference(quant_inst,[status(thm)],[])).
% 0.18/0.41 tff(115,plain,
% 0.18/0.41 ((~![X57: $i, X56: $i, X55: $i, X54: $i] : ((~p7(X54, X56)) | (~p7(X55, X57)) | p7(f8(X54, X55), f8(X56, X57)))) | (~p7(f10(f11(f3(f4(f5(c22)))), c26), f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25)))) | (~p7(f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27)), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27)))) | p7(f8(f10(f11(f3(f4(f5(c22)))), c26), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27))), f8(f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25)), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27))))),
% 0.18/0.41 inference(modus_ponens,[status(thm)],[114, 113])).
% 0.18/0.41 tff(116,plain,
% 0.18/0.41 ((~p7(f10(f11(f3(f4(f5(c22)))), c26), f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25)))) | (~p7(f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27)), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27)))) | p7(f8(f10(f11(f3(f4(f5(c22)))), c26), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27))), f8(f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25)), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27))))),
% 0.18/0.41 inference(unit_resolution,[status(thm)],[115, 112])).
% 0.18/0.41 tff(117,plain,
% 0.18/0.41 ((~p7(f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27)), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27)))) | p7(f8(f10(f11(f3(f4(f5(c22)))), c26), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27))), f8(f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25)), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27))))),
% 0.18/0.41 inference(unit_resolution,[status(thm)],[116, 102])).
% 0.18/0.41 tff(118,plain,
% 0.18/0.41 (p7(f8(f10(f11(f3(f4(f5(c22)))), c26), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27))), f8(f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25)), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27))))),
% 0.18/0.41 inference(unit_resolution,[status(thm)],[117, 11])).
% 0.18/0.41 tff(119,assumption,(~p7(f10(f12(f11(f3(f5(c22)))), c23), f10(f12(f11(f3(f5(c22)))), c23))), introduced(assumption)).
% 0.18/0.41 tff(120,plain,
% 0.18/0.41 ((~![X43: $i] : p7(X43, X43)) | p7(f10(f12(f11(f3(f5(c22)))), c23), f10(f12(f11(f3(f5(c22)))), c23))),
% 0.18/0.41 inference(quant_inst,[status(thm)],[])).
% 0.18/0.41 tff(121,plain,
% 0.18/0.41 ($false),
% 0.18/0.41 inference(unit_resolution,[status(thm)],[120, 8, 119])).
% 0.18/0.41 tff(122,plain,(p7(f10(f12(f11(f3(f5(c22)))), c23), f10(f12(f11(f3(f5(c22)))), c23))), inference(lemma,lemma(discharge,[]))).
% 0.18/0.41 tff(123,plain,
% 0.18/0.41 (((~![X57: $i, X56: $i, X55: $i, X54: $i] : ((~p7(X54, X56)) | (~p7(X55, X57)) | p7(f8(X54, X55), f8(X56, X57)))) | ((~p7(f10(f12(f11(f3(f5(c22)))), c23), f10(f12(f11(f3(f5(c22)))), c23))) | (~p7(f8(f10(f11(f3(f4(f5(c22)))), c26), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27))), f8(f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25)), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27))))) | p7(f8(f10(f12(f11(f3(f5(c22)))), c23), f8(f10(f11(f3(f4(f5(c22)))), c26), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27)))), f8(f10(f12(f11(f3(f5(c22)))), c23), f8(f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25)), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27))))))) <=> ((~![X57: $i, X56: $i, X55: $i, X54: $i] : ((~p7(X54, X56)) | (~p7(X55, X57)) | p7(f8(X54, X55), f8(X56, X57)))) | (~p7(f10(f12(f11(f3(f5(c22)))), c23), f10(f12(f11(f3(f5(c22)))), c23))) | (~p7(f8(f10(f11(f3(f4(f5(c22)))), c26), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27))), f8(f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25)), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27))))) | p7(f8(f10(f12(f11(f3(f5(c22)))), c23), f8(f10(f11(f3(f4(f5(c22)))), c26), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27)))), f8(f10(f12(f11(f3(f5(c22)))), c23), f8(f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25)), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27))))))),
% 0.19/0.42 inference(rewrite,[status(thm)],[])).
% 0.19/0.42 tff(124,plain,
% 0.19/0.42 ((~![X57: $i, X56: $i, X55: $i, X54: $i] : ((~p7(X54, X56)) | (~p7(X55, X57)) | p7(f8(X54, X55), f8(X56, X57)))) | ((~p7(f10(f12(f11(f3(f5(c22)))), c23), f10(f12(f11(f3(f5(c22)))), c23))) | (~p7(f8(f10(f11(f3(f4(f5(c22)))), c26), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27))), f8(f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25)), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27))))) | p7(f8(f10(f12(f11(f3(f5(c22)))), c23), f8(f10(f11(f3(f4(f5(c22)))), c26), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27)))), f8(f10(f12(f11(f3(f5(c22)))), c23), f8(f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25)), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27))))))),
% 0.19/0.42 inference(quant_inst,[status(thm)],[])).
% 0.19/0.42 tff(125,plain,
% 0.19/0.42 ((~![X57: $i, X56: $i, X55: $i, X54: $i] : ((~p7(X54, X56)) | (~p7(X55, X57)) | p7(f8(X54, X55), f8(X56, X57)))) | (~p7(f10(f12(f11(f3(f5(c22)))), c23), f10(f12(f11(f3(f5(c22)))), c23))) | (~p7(f8(f10(f11(f3(f4(f5(c22)))), c26), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27))), f8(f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25)), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27))))) | p7(f8(f10(f12(f11(f3(f5(c22)))), c23), f8(f10(f11(f3(f4(f5(c22)))), c26), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27)))), f8(f10(f12(f11(f3(f5(c22)))), c23), f8(f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25)), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27)))))),
% 0.19/0.42 inference(modus_ponens,[status(thm)],[124, 123])).
% 0.19/0.42 tff(126,plain,
% 0.19/0.42 ((~p7(f10(f12(f11(f3(f5(c22)))), c23), f10(f12(f11(f3(f5(c22)))), c23))) | (~p7(f8(f10(f11(f3(f4(f5(c22)))), c26), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27))), f8(f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25)), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27))))) | p7(f8(f10(f12(f11(f3(f5(c22)))), c23), f8(f10(f11(f3(f4(f5(c22)))), c26), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27)))), f8(f10(f12(f11(f3(f5(c22)))), c23), f8(f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25)), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27)))))),
% 0.19/0.42 inference(unit_resolution,[status(thm)],[125, 112])).
% 0.19/0.42 tff(127,plain,
% 0.19/0.42 (p7(f8(f10(f12(f11(f3(f5(c22)))), c23), f8(f10(f11(f3(f4(f5(c22)))), c26), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27)))), f8(f10(f12(f11(f3(f5(c22)))), c23), f8(f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25)), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27)))))),
% 0.19/0.42 inference(unit_resolution,[status(thm)],[126, 122, 118])).
% 0.19/0.42 tff(128,plain,
% 0.19/0.42 (^[X62: $i, X63: $i] : refl(((~p7(c25, f8(f10(f12(f11(f3(f5(c22)))), X62), f8(f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25)), f9(f11(X63), f10(f11(f3(f4(f5(c22)))), c27)))))) | (~p20(X63, f6(f3(f4(f5(c22))), c21))) | (~p19(X62, f3(f4(f5(c22))))) | (~p19(f6(f3(f4(f5(c22))), f18(c21, f3(f5(c22)))), X63))) <=> ((~p7(c25, f8(f10(f12(f11(f3(f5(c22)))), X62), f8(f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25)), f9(f11(X63), f10(f11(f3(f4(f5(c22)))), c27)))))) | (~p20(X63, f6(f3(f4(f5(c22))), c21))) | (~p19(X62, f3(f4(f5(c22))))) | (~p19(f6(f3(f4(f5(c22))), f18(c21, f3(f5(c22)))), X63))))),
% 0.19/0.42 inference(bind,[status(th)],[])).
% 0.19/0.42 tff(129,plain,
% 0.19/0.42 (![X62: $i, X63: $i] : ((~p7(c25, f8(f10(f12(f11(f3(f5(c22)))), X62), f8(f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25)), f9(f11(X63), f10(f11(f3(f4(f5(c22)))), c27)))))) | (~p20(X63, f6(f3(f4(f5(c22))), c21))) | (~p19(X62, f3(f4(f5(c22))))) | (~p19(f6(f3(f4(f5(c22))), f18(c21, f3(f5(c22)))), X63))) <=> ![X62: $i, X63: $i] : ((~p7(c25, f8(f10(f12(f11(f3(f5(c22)))), X62), f8(f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25)), f9(f11(X63), f10(f11(f3(f4(f5(c22)))), c27)))))) | (~p20(X63, f6(f3(f4(f5(c22))), c21))) | (~p19(X62, f3(f4(f5(c22))))) | (~p19(f6(f3(f4(f5(c22))), f18(c21, f3(f5(c22)))), X63)))),
% 0.19/0.42 inference(quant_intro,[status(thm)],[128])).
% 0.19/0.42 tff(130,plain,
% 0.19/0.42 (![X62: $i, X63: $i] : ((~p7(c25, f8(f10(f12(f11(f3(f5(c22)))), X62), f8(f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25)), f9(f11(X63), f10(f11(f3(f4(f5(c22)))), c27)))))) | (~p20(X63, f6(f3(f4(f5(c22))), c21))) | (~p19(X62, f3(f4(f5(c22))))) | (~p19(f6(f3(f4(f5(c22))), f18(c21, f3(f5(c22)))), X63))) <=> ![X62: $i, X63: $i] : ((~p7(c25, f8(f10(f12(f11(f3(f5(c22)))), X62), f8(f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25)), f9(f11(X63), f10(f11(f3(f4(f5(c22)))), c27)))))) | (~p20(X63, f6(f3(f4(f5(c22))), c21))) | (~p19(X62, f3(f4(f5(c22))))) | (~p19(f6(f3(f4(f5(c22))), f18(c21, f3(f5(c22)))), X63)))),
% 0.19/0.42 inference(rewrite,[status(thm)],[])).
% 0.19/0.42 tff(131,plain,
% 0.19/0.42 (^[X62: $i, X63: $i] : trans(monotonicity(rewrite((((~p19(X62, f3(f4(f5(c22))))) | (~p20(X63, f6(f3(f4(f5(c22))), c21)))) | (~p19(f6(f3(f4(f5(c22))), f18(c21, f3(f5(c22)))), X63))) <=> ((~p20(X63, f6(f3(f4(f5(c22))), c21))) | (~p19(X62, f3(f4(f5(c22))))) | (~p19(f6(f3(f4(f5(c22))), f18(c21, f3(f5(c22)))), X63)))), (((((~p19(X62, f3(f4(f5(c22))))) | (~p20(X63, f6(f3(f4(f5(c22))), c21)))) | (~p19(f6(f3(f4(f5(c22))), f18(c21, f3(f5(c22)))), X63))) | (~p7(c25, f8(f10(f12(f11(f3(f5(c22)))), X62), f8(f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25)), f9(f11(X63), f10(f11(f3(f4(f5(c22)))), c27))))))) <=> (((~p20(X63, f6(f3(f4(f5(c22))), c21))) | (~p19(X62, f3(f4(f5(c22))))) | (~p19(f6(f3(f4(f5(c22))), f18(c21, f3(f5(c22)))), X63))) | (~p7(c25, f8(f10(f12(f11(f3(f5(c22)))), X62), f8(f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25)), f9(f11(X63), f10(f11(f3(f4(f5(c22)))), c27))))))))), rewrite((((~p20(X63, f6(f3(f4(f5(c22))), c21))) | (~p19(X62, f3(f4(f5(c22))))) | (~p19(f6(f3(f4(f5(c22))), f18(c21, f3(f5(c22)))), X63))) | (~p7(c25, f8(f10(f12(f11(f3(f5(c22)))), X62), f8(f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25)), f9(f11(X63), f10(f11(f3(f4(f5(c22)))), c27))))))) <=> ((~p7(c25, f8(f10(f12(f11(f3(f5(c22)))), X62), f8(f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25)), f9(f11(X63), f10(f11(f3(f4(f5(c22)))), c27)))))) | (~p20(X63, f6(f3(f4(f5(c22))), c21))) | (~p19(X62, f3(f4(f5(c22))))) | (~p19(f6(f3(f4(f5(c22))), f18(c21, f3(f5(c22)))), X63)))), (((((~p19(X62, f3(f4(f5(c22))))) | (~p20(X63, f6(f3(f4(f5(c22))), c21)))) | (~p19(f6(f3(f4(f5(c22))), f18(c21, f3(f5(c22)))), X63))) | (~p7(c25, f8(f10(f12(f11(f3(f5(c22)))), X62), f8(f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25)), f9(f11(X63), f10(f11(f3(f4(f5(c22)))), c27))))))) <=> ((~p7(c25, f8(f10(f12(f11(f3(f5(c22)))), X62), f8(f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25)), f9(f11(X63), f10(f11(f3(f4(f5(c22)))), c27)))))) | (~p20(X63, f6(f3(f4(f5(c22))), c21))) | (~p19(X62, f3(f4(f5(c22))))) | (~p19(f6(f3(f4(f5(c22))), f18(c21, f3(f5(c22)))), X63)))))),
% 0.19/0.42 inference(bind,[status(th)],[])).
% 0.19/0.42 tff(132,plain,
% 0.19/0.42 (![X62: $i, X63: $i] : ((((~p19(X62, f3(f4(f5(c22))))) | (~p20(X63, f6(f3(f4(f5(c22))), c21)))) | (~p19(f6(f3(f4(f5(c22))), f18(c21, f3(f5(c22)))), X63))) | (~p7(c25, f8(f10(f12(f11(f3(f5(c22)))), X62), f8(f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25)), f9(f11(X63), f10(f11(f3(f4(f5(c22)))), c27))))))) <=> ![X62: $i, X63: $i] : ((~p7(c25, f8(f10(f12(f11(f3(f5(c22)))), X62), f8(f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25)), f9(f11(X63), f10(f11(f3(f4(f5(c22)))), c27)))))) | (~p20(X63, f6(f3(f4(f5(c22))), c21))) | (~p19(X62, f3(f4(f5(c22))))) | (~p19(f6(f3(f4(f5(c22))), f18(c21, f3(f5(c22)))), X63)))),
% 0.19/0.42 inference(quant_intro,[status(thm)],[131])).
% 0.19/0.42 tff(133,axiom,(![X62: $i, X63: $i] : ((((~p19(X62, f3(f4(f5(c22))))) | (~p20(X63, f6(f3(f4(f5(c22))), c21)))) | (~p19(f6(f3(f4(f5(c22))), f18(c21, f3(f5(c22)))), X63))) | (~p7(c25, f8(f10(f12(f11(f3(f5(c22)))), X62), f8(f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25)), f9(f11(X63), f10(f11(f3(f4(f5(c22)))), c27)))))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','not_p19_31')).
% 0.19/0.42 tff(134,plain,
% 0.19/0.42 (![X62: $i, X63: $i] : ((~p7(c25, f8(f10(f12(f11(f3(f5(c22)))), X62), f8(f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25)), f9(f11(X63), f10(f11(f3(f4(f5(c22)))), c27)))))) | (~p20(X63, f6(f3(f4(f5(c22))), c21))) | (~p19(X62, f3(f4(f5(c22))))) | (~p19(f6(f3(f4(f5(c22))), f18(c21, f3(f5(c22)))), X63)))),
% 0.19/0.43 inference(modus_ponens,[status(thm)],[133, 132])).
% 0.19/0.43 tff(135,plain,
% 0.19/0.43 (![X62: $i, X63: $i] : ((~p7(c25, f8(f10(f12(f11(f3(f5(c22)))), X62), f8(f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25)), f9(f11(X63), f10(f11(f3(f4(f5(c22)))), c27)))))) | (~p20(X63, f6(f3(f4(f5(c22))), c21))) | (~p19(X62, f3(f4(f5(c22))))) | (~p19(f6(f3(f4(f5(c22))), f18(c21, f3(f5(c22)))), X63)))),
% 0.19/0.43 inference(modus_ponens,[status(thm)],[134, 130])).
% 0.19/0.43 tff(136,plain,(
% 0.19/0.43 ![X62: $i, X63: $i] : ((~p7(c25, f8(f10(f12(f11(f3(f5(c22)))), X62), f8(f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25)), f9(f11(X63), f10(f11(f3(f4(f5(c22)))), c27)))))) | (~p20(X63, f6(f3(f4(f5(c22))), c21))) | (~p19(X62, f3(f4(f5(c22))))) | (~p19(f6(f3(f4(f5(c22))), f18(c21, f3(f5(c22)))), X63)))),
% 0.19/0.43 inference(skolemize,[status(sab)],[135])).
% 0.19/0.43 tff(137,plain,
% 0.19/0.43 (![X62: $i, X63: $i] : ((~p7(c25, f8(f10(f12(f11(f3(f5(c22)))), X62), f8(f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25)), f9(f11(X63), f10(f11(f3(f4(f5(c22)))), c27)))))) | (~p20(X63, f6(f3(f4(f5(c22))), c21))) | (~p19(X62, f3(f4(f5(c22))))) | (~p19(f6(f3(f4(f5(c22))), f18(c21, f3(f5(c22)))), X63)))),
% 0.19/0.43 inference(modus_ponens,[status(thm)],[136, 129])).
% 0.19/0.43 tff(138,plain,
% 0.19/0.43 (p19(f6(f3(f4(f5(c22))), f18(c21, f3(f5(c22)))), c24) <=> p19(f6(f3(f4(f5(c22))), f18(c21, f3(f5(c22)))), c24)),
% 0.19/0.43 inference(rewrite,[status(thm)],[])).
% 0.19/0.43 tff(139,axiom,(p19(f6(f3(f4(f5(c22))), f18(c21, f3(f5(c22)))), c24)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','p19_18')).
% 0.19/0.43 tff(140,plain,
% 0.19/0.43 (p19(f6(f3(f4(f5(c22))), f18(c21, f3(f5(c22)))), c24)),
% 0.19/0.43 inference(modus_ponens,[status(thm)],[139, 138])).
% 0.19/0.43 tff(141,plain,
% 0.19/0.43 (p20(c24, f6(f3(f4(f5(c22))), c21)) <=> p20(c24, f6(f3(f4(f5(c22))), c21))),
% 0.19/0.43 inference(rewrite,[status(thm)],[])).
% 0.19/0.43 tff(142,axiom,(p20(c24, f6(f3(f4(f5(c22))), c21))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','p20_7')).
% 0.19/0.43 tff(143,plain,
% 0.19/0.43 (p20(c24, f6(f3(f4(f5(c22))), c21))),
% 0.19/0.43 inference(modus_ponens,[status(thm)],[142, 141])).
% 0.19/0.43 tff(144,plain,
% 0.19/0.43 (p19(c23, f3(f4(f5(c22)))) <=> p19(c23, f3(f4(f5(c22))))),
% 0.19/0.43 inference(rewrite,[status(thm)],[])).
% 0.19/0.43 tff(145,axiom,(p19(c23, f3(f4(f5(c22))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','p19_6')).
% 0.19/0.43 tff(146,plain,
% 0.19/0.43 (p19(c23, f3(f4(f5(c22))))),
% 0.19/0.43 inference(modus_ponens,[status(thm)],[145, 144])).
% 0.19/0.43 tff(147,plain,
% 0.19/0.43 (((~![X62: $i, X63: $i] : ((~p7(c25, f8(f10(f12(f11(f3(f5(c22)))), X62), f8(f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25)), f9(f11(X63), f10(f11(f3(f4(f5(c22)))), c27)))))) | (~p20(X63, f6(f3(f4(f5(c22))), c21))) | (~p19(X62, f3(f4(f5(c22))))) | (~p19(f6(f3(f4(f5(c22))), f18(c21, f3(f5(c22)))), X63)))) | ((~p19(c23, f3(f4(f5(c22))))) | (~p7(c25, f8(f10(f12(f11(f3(f5(c22)))), c23), f8(f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25)), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27)))))) | (~p20(c24, f6(f3(f4(f5(c22))), c21))) | (~p19(f6(f3(f4(f5(c22))), f18(c21, f3(f5(c22)))), c24)))) <=> ((~![X62: $i, X63: $i] : ((~p7(c25, f8(f10(f12(f11(f3(f5(c22)))), X62), f8(f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25)), f9(f11(X63), f10(f11(f3(f4(f5(c22)))), c27)))))) | (~p20(X63, f6(f3(f4(f5(c22))), c21))) | (~p19(X62, f3(f4(f5(c22))))) | (~p19(f6(f3(f4(f5(c22))), f18(c21, f3(f5(c22)))), X63)))) | (~p19(c23, f3(f4(f5(c22))))) | (~p7(c25, f8(f10(f12(f11(f3(f5(c22)))), c23), f8(f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25)), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27)))))) | (~p20(c24, f6(f3(f4(f5(c22))), c21))) | (~p19(f6(f3(f4(f5(c22))), f18(c21, f3(f5(c22)))), c24)))),
% 0.19/0.43 inference(rewrite,[status(thm)],[])).
% 0.19/0.43 tff(148,plain,
% 0.19/0.43 (((~p7(c25, f8(f10(f12(f11(f3(f5(c22)))), c23), f8(f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25)), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27)))))) | (~p20(c24, f6(f3(f4(f5(c22))), c21))) | (~p19(c23, f3(f4(f5(c22))))) | (~p19(f6(f3(f4(f5(c22))), f18(c21, f3(f5(c22)))), c24))) <=> ((~p19(c23, f3(f4(f5(c22))))) | (~p7(c25, f8(f10(f12(f11(f3(f5(c22)))), c23), f8(f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25)), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27)))))) | (~p20(c24, f6(f3(f4(f5(c22))), c21))) | (~p19(f6(f3(f4(f5(c22))), f18(c21, f3(f5(c22)))), c24)))),
% 0.19/0.43 inference(rewrite,[status(thm)],[])).
% 0.19/0.43 tff(149,plain,
% 0.19/0.43 (((~![X62: $i, X63: $i] : ((~p7(c25, f8(f10(f12(f11(f3(f5(c22)))), X62), f8(f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25)), f9(f11(X63), f10(f11(f3(f4(f5(c22)))), c27)))))) | (~p20(X63, f6(f3(f4(f5(c22))), c21))) | (~p19(X62, f3(f4(f5(c22))))) | (~p19(f6(f3(f4(f5(c22))), f18(c21, f3(f5(c22)))), X63)))) | ((~p7(c25, f8(f10(f12(f11(f3(f5(c22)))), c23), f8(f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25)), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27)))))) | (~p20(c24, f6(f3(f4(f5(c22))), c21))) | (~p19(c23, f3(f4(f5(c22))))) | (~p19(f6(f3(f4(f5(c22))), f18(c21, f3(f5(c22)))), c24)))) <=> ((~![X62: $i, X63: $i] : ((~p7(c25, f8(f10(f12(f11(f3(f5(c22)))), X62), f8(f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25)), f9(f11(X63), f10(f11(f3(f4(f5(c22)))), c27)))))) | (~p20(X63, f6(f3(f4(f5(c22))), c21))) | (~p19(X62, f3(f4(f5(c22))))) | (~p19(f6(f3(f4(f5(c22))), f18(c21, f3(f5(c22)))), X63)))) | ((~p19(c23, f3(f4(f5(c22))))) | (~p7(c25, f8(f10(f12(f11(f3(f5(c22)))), c23), f8(f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25)), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27)))))) | (~p20(c24, f6(f3(f4(f5(c22))), c21))) | (~p19(f6(f3(f4(f5(c22))), f18(c21, f3(f5(c22)))), c24))))),
% 0.19/0.43 inference(monotonicity,[status(thm)],[148])).
% 0.19/0.43 tff(150,plain,
% 0.19/0.43 (((~![X62: $i, X63: $i] : ((~p7(c25, f8(f10(f12(f11(f3(f5(c22)))), X62), f8(f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25)), f9(f11(X63), f10(f11(f3(f4(f5(c22)))), c27)))))) | (~p20(X63, f6(f3(f4(f5(c22))), c21))) | (~p19(X62, f3(f4(f5(c22))))) | (~p19(f6(f3(f4(f5(c22))), f18(c21, f3(f5(c22)))), X63)))) | ((~p7(c25, f8(f10(f12(f11(f3(f5(c22)))), c23), f8(f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25)), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27)))))) | (~p20(c24, f6(f3(f4(f5(c22))), c21))) | (~p19(c23, f3(f4(f5(c22))))) | (~p19(f6(f3(f4(f5(c22))), f18(c21, f3(f5(c22)))), c24)))) <=> ((~![X62: $i, X63: $i] : ((~p7(c25, f8(f10(f12(f11(f3(f5(c22)))), X62), f8(f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25)), f9(f11(X63), f10(f11(f3(f4(f5(c22)))), c27)))))) | (~p20(X63, f6(f3(f4(f5(c22))), c21))) | (~p19(X62, f3(f4(f5(c22))))) | (~p19(f6(f3(f4(f5(c22))), f18(c21, f3(f5(c22)))), X63)))) | (~p19(c23, f3(f4(f5(c22))))) | (~p7(c25, f8(f10(f12(f11(f3(f5(c22)))), c23), f8(f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25)), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27)))))) | (~p20(c24, f6(f3(f4(f5(c22))), c21))) | (~p19(f6(f3(f4(f5(c22))), f18(c21, f3(f5(c22)))), c24)))),
% 0.19/0.43 inference(transitivity,[status(thm)],[149, 147])).
% 0.19/0.43 tff(151,plain,
% 0.19/0.43 ((~![X62: $i, X63: $i] : ((~p7(c25, f8(f10(f12(f11(f3(f5(c22)))), X62), f8(f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25)), f9(f11(X63), f10(f11(f3(f4(f5(c22)))), c27)))))) | (~p20(X63, f6(f3(f4(f5(c22))), c21))) | (~p19(X62, f3(f4(f5(c22))))) | (~p19(f6(f3(f4(f5(c22))), f18(c21, f3(f5(c22)))), X63)))) | ((~p7(c25, f8(f10(f12(f11(f3(f5(c22)))), c23), f8(f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25)), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27)))))) | (~p20(c24, f6(f3(f4(f5(c22))), c21))) | (~p19(c23, f3(f4(f5(c22))))) | (~p19(f6(f3(f4(f5(c22))), f18(c21, f3(f5(c22)))), c24)))),
% 0.19/0.43 inference(quant_inst,[status(thm)],[])).
% 0.19/0.43 tff(152,plain,
% 0.19/0.43 ((~![X62: $i, X63: $i] : ((~p7(c25, f8(f10(f12(f11(f3(f5(c22)))), X62), f8(f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25)), f9(f11(X63), f10(f11(f3(f4(f5(c22)))), c27)))))) | (~p20(X63, f6(f3(f4(f5(c22))), c21))) | (~p19(X62, f3(f4(f5(c22))))) | (~p19(f6(f3(f4(f5(c22))), f18(c21, f3(f5(c22)))), X63)))) | (~p19(c23, f3(f4(f5(c22))))) | (~p7(c25, f8(f10(f12(f11(f3(f5(c22)))), c23), f8(f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25)), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27)))))) | (~p20(c24, f6(f3(f4(f5(c22))), c21))) | (~p19(f6(f3(f4(f5(c22))), f18(c21, f3(f5(c22)))), c24))),
% 0.19/0.44 inference(modus_ponens,[status(thm)],[151, 150])).
% 0.19/0.44 tff(153,plain,
% 0.19/0.44 (~p7(c25, f8(f10(f12(f11(f3(f5(c22)))), c23), f8(f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25)), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27)))))),
% 0.19/0.44 inference(unit_resolution,[status(thm)],[152, 146, 143, 140, 137])).
% 0.19/0.44 tff(154,plain,
% 0.19/0.44 (^[X43: $i, X45: $i, X44: $i] : refl((p7(X44, X45) | (~p7(X43, X45)) | (~p7(X43, X44))) <=> (p7(X44, X45) | (~p7(X43, X45)) | (~p7(X43, X44))))),
% 0.19/0.44 inference(bind,[status(th)],[])).
% 0.19/0.44 tff(155,plain,
% 0.19/0.44 (![X43: $i, X45: $i, X44: $i] : (p7(X44, X45) | (~p7(X43, X45)) | (~p7(X43, X44))) <=> ![X43: $i, X45: $i, X44: $i] : (p7(X44, X45) | (~p7(X43, X45)) | (~p7(X43, X44)))),
% 0.19/0.44 inference(quant_intro,[status(thm)],[154])).
% 0.19/0.44 tff(156,plain,
% 0.19/0.44 (![X43: $i, X45: $i, X44: $i] : (p7(X44, X45) | (~p7(X43, X45)) | (~p7(X43, X44))) <=> ![X43: $i, X45: $i, X44: $i] : (p7(X44, X45) | (~p7(X43, X45)) | (~p7(X43, X44)))),
% 0.19/0.44 inference(rewrite,[status(thm)],[])).
% 0.19/0.44 tff(157,plain,
% 0.19/0.44 (^[X43: $i, X45: $i, X44: $i] : trans(monotonicity(rewrite((p7(X44, X45) | (~p7(X43, X44))) <=> (p7(X44, X45) | (~p7(X43, X44)))), (((p7(X44, X45) | (~p7(X43, X44))) | (~p7(X43, X45))) <=> ((p7(X44, X45) | (~p7(X43, X44))) | (~p7(X43, X45))))), rewrite(((p7(X44, X45) | (~p7(X43, X44))) | (~p7(X43, X45))) <=> (p7(X44, X45) | (~p7(X43, X45)) | (~p7(X43, X44)))), (((p7(X44, X45) | (~p7(X43, X44))) | (~p7(X43, X45))) <=> (p7(X44, X45) | (~p7(X43, X45)) | (~p7(X43, X44)))))),
% 0.19/0.44 inference(bind,[status(th)],[])).
% 0.19/0.44 tff(158,plain,
% 0.19/0.44 (![X43: $i, X45: $i, X44: $i] : ((p7(X44, X45) | (~p7(X43, X44))) | (~p7(X43, X45))) <=> ![X43: $i, X45: $i, X44: $i] : (p7(X44, X45) | (~p7(X43, X45)) | (~p7(X43, X44)))),
% 0.19/0.44 inference(quant_intro,[status(thm)],[157])).
% 0.19/0.44 tff(159,axiom,(![X43: $i, X45: $i, X44: $i] : ((p7(X44, X45) | (~p7(X43, X44))) | (~p7(X43, X45)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','p7_15')).
% 0.19/0.44 tff(160,plain,
% 0.19/0.44 (![X43: $i, X45: $i, X44: $i] : (p7(X44, X45) | (~p7(X43, X45)) | (~p7(X43, X44)))),
% 0.19/0.44 inference(modus_ponens,[status(thm)],[159, 158])).
% 0.19/0.44 tff(161,plain,
% 0.19/0.44 (![X43: $i, X45: $i, X44: $i] : (p7(X44, X45) | (~p7(X43, X45)) | (~p7(X43, X44)))),
% 0.19/0.44 inference(modus_ponens,[status(thm)],[160, 156])).
% 0.19/0.44 tff(162,plain,(
% 0.19/0.44 ![X43: $i, X45: $i, X44: $i] : (p7(X44, X45) | (~p7(X43, X45)) | (~p7(X43, X44)))),
% 0.19/0.44 inference(skolemize,[status(sab)],[161])).
% 0.19/0.44 tff(163,plain,
% 0.19/0.44 (![X43: $i, X45: $i, X44: $i] : (p7(X44, X45) | (~p7(X43, X45)) | (~p7(X43, X44)))),
% 0.19/0.44 inference(modus_ponens,[status(thm)],[162, 155])).
% 0.19/0.44 tff(164,plain,
% 0.19/0.44 (((~![X43: $i, X45: $i, X44: $i] : (p7(X44, X45) | (~p7(X43, X45)) | (~p7(X43, X44)))) | (p7(c25, f8(f10(f12(f11(f3(f5(c22)))), c23), f8(f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25)), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27))))) | (~p7(f8(f10(f12(f11(f3(f5(c22)))), c23), f8(f10(f11(f3(f4(f5(c22)))), c26), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27)))), f8(f10(f12(f11(f3(f5(c22)))), c23), f8(f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25)), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27)))))) | (~p7(f8(f10(f12(f11(f3(f5(c22)))), c23), f8(f10(f11(f3(f4(f5(c22)))), c26), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27)))), c25)))) <=> ((~![X43: $i, X45: $i, X44: $i] : (p7(X44, X45) | (~p7(X43, X45)) | (~p7(X43, X44)))) | p7(c25, f8(f10(f12(f11(f3(f5(c22)))), c23), f8(f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25)), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27))))) | (~p7(f8(f10(f12(f11(f3(f5(c22)))), c23), f8(f10(f11(f3(f4(f5(c22)))), c26), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27)))), f8(f10(f12(f11(f3(f5(c22)))), c23), f8(f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25)), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27)))))) | (~p7(f8(f10(f12(f11(f3(f5(c22)))), c23), f8(f10(f11(f3(f4(f5(c22)))), c26), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27)))), c25)))),
% 0.19/0.44 inference(rewrite,[status(thm)],[])).
% 0.19/0.44 tff(165,plain,
% 0.19/0.44 ((~![X43: $i, X45: $i, X44: $i] : (p7(X44, X45) | (~p7(X43, X45)) | (~p7(X43, X44)))) | (p7(c25, f8(f10(f12(f11(f3(f5(c22)))), c23), f8(f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25)), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27))))) | (~p7(f8(f10(f12(f11(f3(f5(c22)))), c23), f8(f10(f11(f3(f4(f5(c22)))), c26), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27)))), f8(f10(f12(f11(f3(f5(c22)))), c23), f8(f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25)), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27)))))) | (~p7(f8(f10(f12(f11(f3(f5(c22)))), c23), f8(f10(f11(f3(f4(f5(c22)))), c26), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27)))), c25)))),
% 0.19/0.44 inference(quant_inst,[status(thm)],[])).
% 0.19/0.44 tff(166,plain,
% 0.19/0.44 ((~![X43: $i, X45: $i, X44: $i] : (p7(X44, X45) | (~p7(X43, X45)) | (~p7(X43, X44)))) | p7(c25, f8(f10(f12(f11(f3(f5(c22)))), c23), f8(f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25)), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27))))) | (~p7(f8(f10(f12(f11(f3(f5(c22)))), c23), f8(f10(f11(f3(f4(f5(c22)))), c26), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27)))), f8(f10(f12(f11(f3(f5(c22)))), c23), f8(f10(f11(f3(f4(f5(c22)))), f14(f16(c28, f17(c21, c27)), c25)), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27)))))) | (~p7(f8(f10(f12(f11(f3(f5(c22)))), c23), f8(f10(f11(f3(f4(f5(c22)))), c26), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27)))), c25))),
% 0.19/0.44 inference(modus_ponens,[status(thm)],[165, 164])).
% 0.19/0.44 tff(167,plain,
% 0.19/0.44 (~p7(f8(f10(f12(f11(f3(f5(c22)))), c23), f8(f10(f11(f3(f4(f5(c22)))), c26), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27)))), c25)),
% 0.19/0.44 inference(unit_resolution,[status(thm)],[166, 163, 153, 127])).
% 0.19/0.44 tff(168,assumption,(~p7(c25, c25)), introduced(assumption)).
% 0.19/0.44 tff(169,plain,
% 0.19/0.44 ((~![X43: $i] : p7(X43, X43)) | p7(c25, c25)),
% 0.19/0.44 inference(quant_inst,[status(thm)],[])).
% 0.19/0.44 tff(170,plain,
% 0.19/0.44 ($false),
% 0.19/0.44 inference(unit_resolution,[status(thm)],[169, 8, 168])).
% 0.19/0.44 tff(171,plain,(p7(c25, c25)), inference(lemma,lemma(discharge,[]))).
% 0.19/0.44 tff(172,plain,
% 0.19/0.44 (p7(c25, f8(f10(f12(f11(f3(f5(c22)))), c23), f8(f10(f11(f3(f4(f5(c22)))), c26), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27))))) <=> p7(c25, f8(f10(f12(f11(f3(f5(c22)))), c23), f8(f10(f11(f3(f4(f5(c22)))), c26), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27)))))),
% 0.19/0.44 inference(rewrite,[status(thm)],[])).
% 0.19/0.44 tff(173,axiom,(p7(c25, f8(f10(f12(f11(f3(f5(c22)))), c23), f8(f10(f11(f3(f4(f5(c22)))), c26), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27)))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','p7_29')).
% 0.19/0.44 tff(174,plain,
% 0.19/0.44 (p7(c25, f8(f10(f12(f11(f3(f5(c22)))), c23), f8(f10(f11(f3(f4(f5(c22)))), c26), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27)))))),
% 0.19/0.44 inference(modus_ponens,[status(thm)],[173, 172])).
% 0.19/0.44 tff(175,plain,
% 0.19/0.44 (((~![X43: $i, X45: $i, X44: $i] : (p7(X44, X45) | (~p7(X43, X45)) | (~p7(X43, X44)))) | ((~p7(c25, c25)) | p7(f8(f10(f12(f11(f3(f5(c22)))), c23), f8(f10(f11(f3(f4(f5(c22)))), c26), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27)))), c25) | (~p7(c25, f8(f10(f12(f11(f3(f5(c22)))), c23), f8(f10(f11(f3(f4(f5(c22)))), c26), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27)))))))) <=> ((~![X43: $i, X45: $i, X44: $i] : (p7(X44, X45) | (~p7(X43, X45)) | (~p7(X43, X44)))) | (~p7(c25, c25)) | p7(f8(f10(f12(f11(f3(f5(c22)))), c23), f8(f10(f11(f3(f4(f5(c22)))), c26), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27)))), c25) | (~p7(c25, f8(f10(f12(f11(f3(f5(c22)))), c23), f8(f10(f11(f3(f4(f5(c22)))), c26), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27)))))))),
% 0.19/0.44 inference(rewrite,[status(thm)],[])).
% 0.19/0.44 tff(176,plain,
% 0.19/0.44 ((p7(f8(f10(f12(f11(f3(f5(c22)))), c23), f8(f10(f11(f3(f4(f5(c22)))), c26), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27)))), c25) | (~p7(c25, c25)) | (~p7(c25, f8(f10(f12(f11(f3(f5(c22)))), c23), f8(f10(f11(f3(f4(f5(c22)))), c26), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27))))))) <=> ((~p7(c25, c25)) | p7(f8(f10(f12(f11(f3(f5(c22)))), c23), f8(f10(f11(f3(f4(f5(c22)))), c26), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27)))), c25) | (~p7(c25, f8(f10(f12(f11(f3(f5(c22)))), c23), f8(f10(f11(f3(f4(f5(c22)))), c26), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27)))))))),
% 0.19/0.44 inference(rewrite,[status(thm)],[])).
% 0.19/0.45 tff(177,plain,
% 0.19/0.45 (((~![X43: $i, X45: $i, X44: $i] : (p7(X44, X45) | (~p7(X43, X45)) | (~p7(X43, X44)))) | (p7(f8(f10(f12(f11(f3(f5(c22)))), c23), f8(f10(f11(f3(f4(f5(c22)))), c26), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27)))), c25) | (~p7(c25, c25)) | (~p7(c25, f8(f10(f12(f11(f3(f5(c22)))), c23), f8(f10(f11(f3(f4(f5(c22)))), c26), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27)))))))) <=> ((~![X43: $i, X45: $i, X44: $i] : (p7(X44, X45) | (~p7(X43, X45)) | (~p7(X43, X44)))) | ((~p7(c25, c25)) | p7(f8(f10(f12(f11(f3(f5(c22)))), c23), f8(f10(f11(f3(f4(f5(c22)))), c26), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27)))), c25) | (~p7(c25, f8(f10(f12(f11(f3(f5(c22)))), c23), f8(f10(f11(f3(f4(f5(c22)))), c26), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27))))))))),
% 0.19/0.45 inference(monotonicity,[status(thm)],[176])).
% 0.19/0.45 tff(178,plain,
% 0.19/0.45 (((~![X43: $i, X45: $i, X44: $i] : (p7(X44, X45) | (~p7(X43, X45)) | (~p7(X43, X44)))) | (p7(f8(f10(f12(f11(f3(f5(c22)))), c23), f8(f10(f11(f3(f4(f5(c22)))), c26), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27)))), c25) | (~p7(c25, c25)) | (~p7(c25, f8(f10(f12(f11(f3(f5(c22)))), c23), f8(f10(f11(f3(f4(f5(c22)))), c26), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27)))))))) <=> ((~![X43: $i, X45: $i, X44: $i] : (p7(X44, X45) | (~p7(X43, X45)) | (~p7(X43, X44)))) | (~p7(c25, c25)) | p7(f8(f10(f12(f11(f3(f5(c22)))), c23), f8(f10(f11(f3(f4(f5(c22)))), c26), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27)))), c25) | (~p7(c25, f8(f10(f12(f11(f3(f5(c22)))), c23), f8(f10(f11(f3(f4(f5(c22)))), c26), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27)))))))),
% 0.19/0.45 inference(transitivity,[status(thm)],[177, 175])).
% 0.19/0.45 tff(179,plain,
% 0.19/0.45 ((~![X43: $i, X45: $i, X44: $i] : (p7(X44, X45) | (~p7(X43, X45)) | (~p7(X43, X44)))) | (p7(f8(f10(f12(f11(f3(f5(c22)))), c23), f8(f10(f11(f3(f4(f5(c22)))), c26), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27)))), c25) | (~p7(c25, c25)) | (~p7(c25, f8(f10(f12(f11(f3(f5(c22)))), c23), f8(f10(f11(f3(f4(f5(c22)))), c26), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27)))))))),
% 0.19/0.45 inference(quant_inst,[status(thm)],[])).
% 0.19/0.45 tff(180,plain,
% 0.19/0.45 ((~![X43: $i, X45: $i, X44: $i] : (p7(X44, X45) | (~p7(X43, X45)) | (~p7(X43, X44)))) | (~p7(c25, c25)) | p7(f8(f10(f12(f11(f3(f5(c22)))), c23), f8(f10(f11(f3(f4(f5(c22)))), c26), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27)))), c25) | (~p7(c25, f8(f10(f12(f11(f3(f5(c22)))), c23), f8(f10(f11(f3(f4(f5(c22)))), c26), f9(f11(c24), f10(f11(f3(f4(f5(c22)))), c27))))))),
% 0.19/0.45 inference(modus_ponens,[status(thm)],[179, 178])).
% 0.19/0.45 tff(181,plain,
% 0.19/0.45 ($false),
% 0.19/0.45 inference(unit_resolution,[status(thm)],[180, 163, 174, 171, 167])).
% 0.19/0.45 % SZS output end Proof
% 0.19/0.45 % E exiting
%------------------------------------------------------------------------------