%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : SYN617-1 : TPTP v9.0.0. Released v2.5.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n007.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.20s 0.43s
% Output : Proof 0.20s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.11 % Problem : SYN617-1 : TPTP v9.0.0. Released v2.5.0.
% 0.06/0.11 % Command : run_E %s %d THM
% 0.11/0.32 % Computer : n007.cluster.edu
% 0.11/0.32 % Model : x86_64 x86_64
% 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.32 % Memory : 8042.1875MB
% 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.32 % CPULimit : 300
% 0.11/0.32 % WCLimit : 300
% 0.11/0.32 % DateTime : Fri Jun 20 12:40:35 EDT 2025
% 0.11/0.32 % CPUTime :
% 0.20/0.43 % SZS status Unsatisfiable
% 0.20/0.43 % SZS output start Proof
% 0.20/0.43 tff(p13_type, type, (
% 0.20/0.43 p13: ( $i * $i ) > $o)).
% 0.20/0.43 tff(f15_type, type, (
% 0.20/0.43 f15: ( $i * $i ) > $i)).
% 0.20/0.43 tff(f14_type, type, (
% 0.20/0.43 f14: ( $i * $i ) > $i)).
% 0.20/0.43 tff(c24_type, type, (
% 0.20/0.43 c24: $i)).
% 0.20/0.43 tff(c23_type, type, (
% 0.20/0.43 c23: $i)).
% 0.20/0.43 tff(f4_type, type, (
% 0.20/0.43 f4: ( $i * $i ) > $i)).
% 0.20/0.43 tff(c21_type, type, (
% 0.20/0.43 c21: $i)).
% 0.20/0.43 tff(f5_type, type, (
% 0.20/0.43 f5: $i > $i)).
% 0.20/0.43 tff(f6_type, type, (
% 0.20/0.43 f6: $i > $i)).
% 0.20/0.43 tff(c20_type, type, (
% 0.20/0.43 c20: $i)).
% 0.20/0.43 tff(f3_type, type, (
% 0.20/0.43 f3: $i > $i)).
% 0.20/0.43 tff(c22_type, type, (
% 0.20/0.43 c22: $i)).
% 0.20/0.43 tff(f12_type, type, (
% 0.20/0.43 f12: $i > $i)).
% 0.20/0.43 tff(p2_type, type, (
% 0.20/0.43 p2: ( $i * $i ) > $o)).
% 0.20/0.43 tff(p19_type, type, (
% 0.20/0.43 p19: ( $i * $i ) > $o)).
% 0.20/0.43 tff(p11_type, type, (
% 0.20/0.43 p11: ( $i * $i ) > $o)).
% 0.20/0.43 tff(1,plain,
% 0.20/0.43 (^[X37: $i, X36: $i] : refl(((~p19(X37, X36)) | p2(f4(f4(f3(X36), f5(f6(c20))), X37), f3(f4(f4(X36, f5(f6(c20))), X37)))) <=> ((~p19(X37, X36)) | p2(f4(f4(f3(X36), f5(f6(c20))), X37), f3(f4(f4(X36, f5(f6(c20))), X37)))))),
% 0.20/0.43 inference(bind,[status(th)],[])).
% 0.20/0.43 tff(2,plain,
% 0.20/0.43 (![X37: $i, X36: $i] : ((~p19(X37, X36)) | p2(f4(f4(f3(X36), f5(f6(c20))), X37), f3(f4(f4(X36, f5(f6(c20))), X37)))) <=> ![X37: $i, X36: $i] : ((~p19(X37, X36)) | p2(f4(f4(f3(X36), f5(f6(c20))), X37), f3(f4(f4(X36, f5(f6(c20))), X37))))),
% 0.20/0.43 inference(quant_intro,[status(thm)],[1])).
% 0.20/0.43 tff(3,plain,
% 0.20/0.43 (![X37: $i, X36: $i] : ((~p19(X37, X36)) | p2(f4(f4(f3(X36), f5(f6(c20))), X37), f3(f4(f4(X36, f5(f6(c20))), X37)))) <=> ![X37: $i, X36: $i] : ((~p19(X37, X36)) | p2(f4(f4(f3(X36), f5(f6(c20))), X37), f3(f4(f4(X36, f5(f6(c20))), X37))))),
% 0.20/0.43 inference(rewrite,[status(thm)],[])).
% 0.20/0.43 tff(4,plain,
% 0.20/0.43 (^[X37: $i, X36: $i] : rewrite((p2(f4(f4(f3(X36), f5(f6(c20))), X37), f3(f4(f4(X36, f5(f6(c20))), X37))) | (~p19(X37, X36))) <=> ((~p19(X37, X36)) | p2(f4(f4(f3(X36), f5(f6(c20))), X37), f3(f4(f4(X36, f5(f6(c20))), X37)))))),
% 0.20/0.43 inference(bind,[status(th)],[])).
% 0.20/0.43 tff(5,plain,
% 0.20/0.43 (![X37: $i, X36: $i] : (p2(f4(f4(f3(X36), f5(f6(c20))), X37), f3(f4(f4(X36, f5(f6(c20))), X37))) | (~p19(X37, X36))) <=> ![X37: $i, X36: $i] : ((~p19(X37, X36)) | p2(f4(f4(f3(X36), f5(f6(c20))), X37), f3(f4(f4(X36, f5(f6(c20))), X37))))),
% 0.20/0.43 inference(quant_intro,[status(thm)],[4])).
% 0.20/0.43 tff(6,axiom,(![X37: $i, X36: $i] : (p2(f4(f4(f3(X36), f5(f6(c20))), X37), f3(f4(f4(X36, f5(f6(c20))), X37))) | (~p19(X37, X36)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','p2_31')).
% 0.20/0.43 tff(7,plain,
% 0.20/0.43 (![X37: $i, X36: $i] : ((~p19(X37, X36)) | p2(f4(f4(f3(X36), f5(f6(c20))), X37), f3(f4(f4(X36, f5(f6(c20))), X37))))),
% 0.20/0.43 inference(modus_ponens,[status(thm)],[6, 5])).
% 0.20/0.43 tff(8,plain,
% 0.20/0.43 (![X37: $i, X36: $i] : ((~p19(X37, X36)) | p2(f4(f4(f3(X36), f5(f6(c20))), X37), f3(f4(f4(X36, f5(f6(c20))), X37))))),
% 0.20/0.43 inference(modus_ponens,[status(thm)],[7, 3])).
% 0.20/0.43 tff(9,plain,(
% 0.20/0.43 ![X37: $i, X36: $i] : ((~p19(X37, X36)) | p2(f4(f4(f3(X36), f5(f6(c20))), X37), f3(f4(f4(X36, f5(f6(c20))), X37))))),
% 0.20/0.43 inference(skolemize,[status(sab)],[8])).
% 0.20/0.43 tff(10,plain,
% 0.20/0.43 (![X37: $i, X36: $i] : ((~p19(X37, X36)) | p2(f4(f4(f3(X36), f5(f6(c20))), X37), f3(f4(f4(X36, f5(f6(c20))), X37))))),
% 0.20/0.43 inference(modus_ponens,[status(thm)],[9, 2])).
% 0.20/0.43 tff(11,plain,
% 0.20/0.43 (p19(c21, c22) <=> p19(c21, c22)),
% 0.20/0.43 inference(rewrite,[status(thm)],[])).
% 0.20/0.43 tff(12,axiom,(p19(c21, c22)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','p19_6')).
% 0.20/0.43 tff(13,plain,
% 0.20/0.43 (p19(c21, c22)),
% 0.20/0.43 inference(modus_ponens,[status(thm)],[12, 11])).
% 0.20/0.43 tff(14,plain,
% 0.20/0.43 (((~![X37: $i, X36: $i] : ((~p19(X37, X36)) | p2(f4(f4(f3(X36), f5(f6(c20))), X37), f3(f4(f4(X36, f5(f6(c20))), X37))))) | ((~p19(c21, c22)) | p2(f4(f4(f3(c22), f5(f6(c20))), c21), f3(f4(f4(c22, f5(f6(c20))), c21))))) <=> ((~![X37: $i, X36: $i] : ((~p19(X37, X36)) | p2(f4(f4(f3(X36), f5(f6(c20))), X37), f3(f4(f4(X36, f5(f6(c20))), X37))))) | (~p19(c21, c22)) | p2(f4(f4(f3(c22), f5(f6(c20))), c21), f3(f4(f4(c22, f5(f6(c20))), c21))))),
% 0.20/0.43 inference(rewrite,[status(thm)],[])).
% 0.20/0.43 tff(15,plain,
% 0.20/0.43 ((~![X37: $i, X36: $i] : ((~p19(X37, X36)) | p2(f4(f4(f3(X36), f5(f6(c20))), X37), f3(f4(f4(X36, f5(f6(c20))), X37))))) | ((~p19(c21, c22)) | p2(f4(f4(f3(c22), f5(f6(c20))), c21), f3(f4(f4(c22, f5(f6(c20))), c21))))),
% 0.20/0.44 inference(quant_inst,[status(thm)],[])).
% 0.20/0.44 tff(16,plain,
% 0.20/0.44 ((~![X37: $i, X36: $i] : ((~p19(X37, X36)) | p2(f4(f4(f3(X36), f5(f6(c20))), X37), f3(f4(f4(X36, f5(f6(c20))), X37))))) | (~p19(c21, c22)) | p2(f4(f4(f3(c22), f5(f6(c20))), c21), f3(f4(f4(c22, f5(f6(c20))), c21)))),
% 0.20/0.44 inference(modus_ponens,[status(thm)],[15, 14])).
% 0.20/0.44 tff(17,plain,
% 0.20/0.44 (p2(f4(f4(f3(c22), f5(f6(c20))), c21), f3(f4(f4(c22, f5(f6(c20))), c21)))),
% 0.20/0.44 inference(unit_resolution,[status(thm)],[16, 13, 10])).
% 0.20/0.44 tff(18,assumption,(~p2(c20, c20)), introduced(assumption)).
% 0.20/0.44 tff(19,plain,
% 0.20/0.44 (^[X27: $i] : refl(p2(X27, X27) <=> p2(X27, X27))),
% 0.20/0.44 inference(bind,[status(th)],[])).
% 0.20/0.44 tff(20,plain,
% 0.20/0.44 (![X27: $i] : p2(X27, X27) <=> ![X27: $i] : p2(X27, X27)),
% 0.20/0.44 inference(quant_intro,[status(thm)],[19])).
% 0.20/0.44 tff(21,plain,
% 0.20/0.44 (![X27: $i] : p2(X27, X27) <=> ![X27: $i] : p2(X27, X27)),
% 0.20/0.44 inference(rewrite,[status(thm)],[])).
% 0.20/0.44 tff(22,axiom,(![X27: $i] : p2(X27, X27)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','p2_4')).
% 0.20/0.44 tff(23,plain,
% 0.20/0.44 (![X27: $i] : p2(X27, X27)),
% 0.20/0.44 inference(modus_ponens,[status(thm)],[22, 21])).
% 0.20/0.44 tff(24,plain,(
% 0.20/0.44 ![X27: $i] : p2(X27, X27)),
% 0.20/0.44 inference(skolemize,[status(sab)],[23])).
% 0.20/0.44 tff(25,plain,
% 0.20/0.44 (![X27: $i] : p2(X27, X27)),
% 0.20/0.44 inference(modus_ponens,[status(thm)],[24, 20])).
% 0.20/0.44 tff(26,plain,
% 0.20/0.44 ((~![X27: $i] : p2(X27, X27)) | p2(c20, c20)),
% 0.20/0.44 inference(quant_inst,[status(thm)],[])).
% 0.20/0.44 tff(27,plain,
% 0.20/0.44 ($false),
% 0.20/0.44 inference(unit_resolution,[status(thm)],[26, 25, 18])).
% 0.20/0.44 tff(28,plain,(p2(c20, c20)), inference(lemma,lemma(discharge,[]))).
% 0.20/0.44 tff(29,plain,
% 0.20/0.44 (^[X41: $i, X40: $i] : refl(((~p2(X40, X41)) | p2(f6(X40), f6(X41))) <=> ((~p2(X40, X41)) | p2(f6(X40), f6(X41))))),
% 0.20/0.44 inference(bind,[status(th)],[])).
% 0.20/0.44 tff(30,plain,
% 0.20/0.44 (![X41: $i, X40: $i] : ((~p2(X40, X41)) | p2(f6(X40), f6(X41))) <=> ![X41: $i, X40: $i] : ((~p2(X40, X41)) | p2(f6(X40), f6(X41)))),
% 0.20/0.44 inference(quant_intro,[status(thm)],[29])).
% 0.20/0.44 tff(31,plain,
% 0.20/0.44 (![X41: $i, X40: $i] : ((~p2(X40, X41)) | p2(f6(X40), f6(X41))) <=> ![X41: $i, X40: $i] : ((~p2(X40, X41)) | p2(f6(X40), f6(X41)))),
% 0.20/0.44 inference(rewrite,[status(thm)],[])).
% 0.20/0.44 tff(32,plain,
% 0.20/0.44 (^[X41: $i, X40: $i] : rewrite((p2(f6(X40), f6(X41)) | (~p2(X40, X41))) <=> ((~p2(X40, X41)) | p2(f6(X40), f6(X41))))),
% 0.20/0.44 inference(bind,[status(th)],[])).
% 0.20/0.44 tff(33,plain,
% 0.20/0.44 (![X41: $i, X40: $i] : (p2(f6(X40), f6(X41)) | (~p2(X40, X41))) <=> ![X41: $i, X40: $i] : ((~p2(X40, X41)) | p2(f6(X40), f6(X41)))),
% 0.20/0.44 inference(quant_intro,[status(thm)],[32])).
% 0.20/0.44 tff(34,axiom,(![X41: $i, X40: $i] : (p2(f6(X40), f6(X41)) | (~p2(X40, X41)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','p2_14')).
% 0.20/0.44 tff(35,plain,
% 0.20/0.44 (![X41: $i, X40: $i] : ((~p2(X40, X41)) | p2(f6(X40), f6(X41)))),
% 0.20/0.44 inference(modus_ponens,[status(thm)],[34, 33])).
% 0.20/0.44 tff(36,plain,
% 0.20/0.44 (![X41: $i, X40: $i] : ((~p2(X40, X41)) | p2(f6(X40), f6(X41)))),
% 0.20/0.44 inference(modus_ponens,[status(thm)],[35, 31])).
% 0.20/0.44 tff(37,plain,(
% 0.20/0.44 ![X41: $i, X40: $i] : ((~p2(X40, X41)) | p2(f6(X40), f6(X41)))),
% 0.20/0.44 inference(skolemize,[status(sab)],[36])).
% 0.20/0.44 tff(38,plain,
% 0.20/0.44 (![X41: $i, X40: $i] : ((~p2(X40, X41)) | p2(f6(X40), f6(X41)))),
% 0.20/0.44 inference(modus_ponens,[status(thm)],[37, 30])).
% 0.20/0.44 tff(39,plain,
% 0.20/0.44 (((~![X41: $i, X40: $i] : ((~p2(X40, X41)) | p2(f6(X40), f6(X41)))) | ((~p2(c20, c20)) | p2(f6(c20), f6(c20)))) <=> ((~![X41: $i, X40: $i] : ((~p2(X40, X41)) | p2(f6(X40), f6(X41)))) | (~p2(c20, c20)) | p2(f6(c20), f6(c20)))),
% 0.20/0.44 inference(rewrite,[status(thm)],[])).
% 0.20/0.44 tff(40,plain,
% 0.20/0.44 ((~![X41: $i, X40: $i] : ((~p2(X40, X41)) | p2(f6(X40), f6(X41)))) | ((~p2(c20, c20)) | p2(f6(c20), f6(c20)))),
% 0.20/0.44 inference(quant_inst,[status(thm)],[])).
% 0.20/0.44 tff(41,plain,
% 0.20/0.44 ((~![X41: $i, X40: $i] : ((~p2(X40, X41)) | p2(f6(X40), f6(X41)))) | (~p2(c20, c20)) | p2(f6(c20), f6(c20))),
% 0.20/0.44 inference(modus_ponens,[status(thm)],[40, 39])).
% 0.20/0.44 tff(42,plain,
% 0.20/0.44 ((~p2(c20, c20)) | p2(f6(c20), f6(c20))),
% 0.20/0.44 inference(unit_resolution,[status(thm)],[41, 38])).
% 0.20/0.44 tff(43,plain,
% 0.20/0.44 (p2(f6(c20), f6(c20))),
% 0.20/0.44 inference(unit_resolution,[status(thm)],[42, 28])).
% 0.20/0.44 tff(44,plain,
% 0.20/0.44 (^[X39: $i, X38: $i] : refl(((~p2(X38, X39)) | p2(f5(X38), f5(X39))) <=> ((~p2(X38, X39)) | p2(f5(X38), f5(X39))))),
% 0.20/0.44 inference(bind,[status(th)],[])).
% 0.20/0.44 tff(45,plain,
% 0.20/0.44 (![X39: $i, X38: $i] : ((~p2(X38, X39)) | p2(f5(X38), f5(X39))) <=> ![X39: $i, X38: $i] : ((~p2(X38, X39)) | p2(f5(X38), f5(X39)))),
% 0.20/0.44 inference(quant_intro,[status(thm)],[44])).
% 0.20/0.44 tff(46,plain,
% 0.20/0.44 (![X39: $i, X38: $i] : ((~p2(X38, X39)) | p2(f5(X38), f5(X39))) <=> ![X39: $i, X38: $i] : ((~p2(X38, X39)) | p2(f5(X38), f5(X39)))),
% 0.20/0.44 inference(rewrite,[status(thm)],[])).
% 0.20/0.44 tff(47,plain,
% 0.20/0.44 (^[X39: $i, X38: $i] : rewrite((p2(f5(X38), f5(X39)) | (~p2(X38, X39))) <=> ((~p2(X38, X39)) | p2(f5(X38), f5(X39))))),
% 0.20/0.44 inference(bind,[status(th)],[])).
% 0.20/0.44 tff(48,plain,
% 0.20/0.44 (![X39: $i, X38: $i] : (p2(f5(X38), f5(X39)) | (~p2(X38, X39))) <=> ![X39: $i, X38: $i] : ((~p2(X38, X39)) | p2(f5(X38), f5(X39)))),
% 0.20/0.44 inference(quant_intro,[status(thm)],[47])).
% 0.20/0.44 tff(49,axiom,(![X39: $i, X38: $i] : (p2(f5(X38), f5(X39)) | (~p2(X38, X39)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','p2_15')).
% 0.20/0.44 tff(50,plain,
% 0.20/0.44 (![X39: $i, X38: $i] : ((~p2(X38, X39)) | p2(f5(X38), f5(X39)))),
% 0.20/0.44 inference(modus_ponens,[status(thm)],[49, 48])).
% 0.20/0.44 tff(51,plain,
% 0.20/0.44 (![X39: $i, X38: $i] : ((~p2(X38, X39)) | p2(f5(X38), f5(X39)))),
% 0.20/0.44 inference(modus_ponens,[status(thm)],[50, 46])).
% 0.20/0.44 tff(52,plain,(
% 0.20/0.44 ![X39: $i, X38: $i] : ((~p2(X38, X39)) | p2(f5(X38), f5(X39)))),
% 0.20/0.44 inference(skolemize,[status(sab)],[51])).
% 0.20/0.44 tff(53,plain,
% 0.20/0.44 (![X39: $i, X38: $i] : ((~p2(X38, X39)) | p2(f5(X38), f5(X39)))),
% 0.20/0.44 inference(modus_ponens,[status(thm)],[52, 45])).
% 0.20/0.44 tff(54,plain,
% 0.20/0.44 (((~![X39: $i, X38: $i] : ((~p2(X38, X39)) | p2(f5(X38), f5(X39)))) | ((~p2(f6(c20), f6(c20))) | p2(f5(f6(c20)), f5(f6(c20))))) <=> ((~![X39: $i, X38: $i] : ((~p2(X38, X39)) | p2(f5(X38), f5(X39)))) | (~p2(f6(c20), f6(c20))) | p2(f5(f6(c20)), f5(f6(c20))))),
% 0.20/0.44 inference(rewrite,[status(thm)],[])).
% 0.20/0.44 tff(55,plain,
% 0.20/0.44 ((~![X39: $i, X38: $i] : ((~p2(X38, X39)) | p2(f5(X38), f5(X39)))) | ((~p2(f6(c20), f6(c20))) | p2(f5(f6(c20)), f5(f6(c20))))),
% 0.20/0.44 inference(quant_inst,[status(thm)],[])).
% 0.20/0.44 tff(56,plain,
% 0.20/0.44 ((~![X39: $i, X38: $i] : ((~p2(X38, X39)) | p2(f5(X38), f5(X39)))) | (~p2(f6(c20), f6(c20))) | p2(f5(f6(c20)), f5(f6(c20)))),
% 0.20/0.44 inference(modus_ponens,[status(thm)],[55, 54])).
% 0.20/0.44 tff(57,plain,
% 0.20/0.44 ((~p2(f6(c20), f6(c20))) | p2(f5(f6(c20)), f5(f6(c20)))),
% 0.20/0.44 inference(unit_resolution,[status(thm)],[56, 53])).
% 0.20/0.44 tff(58,plain,
% 0.20/0.44 (p2(f5(f6(c20)), f5(f6(c20)))),
% 0.20/0.44 inference(unit_resolution,[status(thm)],[57, 43])).
% 0.20/0.44 tff(59,assumption,(~p2(f3(c22), f3(c22))), introduced(assumption)).
% 0.20/0.44 tff(60,plain,
% 0.20/0.44 ((~![X27: $i] : p2(X27, X27)) | p2(f3(c22), f3(c22))),
% 0.20/0.44 inference(quant_inst,[status(thm)],[])).
% 0.20/0.44 tff(61,plain,
% 0.20/0.44 ($false),
% 0.20/0.44 inference(unit_resolution,[status(thm)],[60, 25, 59])).
% 0.20/0.44 tff(62,plain,(p2(f3(c22), f3(c22))), inference(lemma,lemma(discharge,[]))).
% 0.20/0.44 tff(63,plain,
% 0.20/0.44 (^[X32: $i, X35: $i, X34: $i, X33: $i] : refl(((~p2(X33, X35)) | (~p2(X32, X34)) | p2(f4(X32, X33), f4(X34, X35))) <=> ((~p2(X33, X35)) | (~p2(X32, X34)) | p2(f4(X32, X33), f4(X34, X35))))),
% 0.20/0.44 inference(bind,[status(th)],[])).
% 0.20/0.44 tff(64,plain,
% 0.20/0.44 (![X32: $i, X35: $i, X34: $i, X33: $i] : ((~p2(X33, X35)) | (~p2(X32, X34)) | p2(f4(X32, X33), f4(X34, X35))) <=> ![X32: $i, X35: $i, X34: $i, X33: $i] : ((~p2(X33, X35)) | (~p2(X32, X34)) | p2(f4(X32, X33), f4(X34, X35)))),
% 0.20/0.44 inference(quant_intro,[status(thm)],[63])).
% 0.20/0.44 tff(65,plain,
% 0.20/0.44 (![X32: $i, X35: $i, X34: $i, X33: $i] : ((~p2(X33, X35)) | (~p2(X32, X34)) | p2(f4(X32, X33), f4(X34, X35))) <=> ![X32: $i, X35: $i, X34: $i, X33: $i] : ((~p2(X33, X35)) | (~p2(X32, X34)) | p2(f4(X32, X33), f4(X34, X35)))),
% 0.20/0.44 inference(rewrite,[status(thm)],[])).
% 0.20/0.44 tff(66,plain,
% 0.20/0.44 (^[X32: $i, X35: $i, X34: $i, X33: $i] : trans(monotonicity(rewrite((p2(f4(X32, X33), f4(X34, X35)) | (~p2(X32, X34))) <=> ((~p2(X32, X34)) | p2(f4(X32, X33), f4(X34, X35)))), (((p2(f4(X32, X33), f4(X34, X35)) | (~p2(X32, X34))) | (~p2(X33, X35))) <=> (((~p2(X32, X34)) | p2(f4(X32, X33), f4(X34, X35))) | (~p2(X33, X35))))), rewrite((((~p2(X32, X34)) | p2(f4(X32, X33), f4(X34, X35))) | (~p2(X33, X35))) <=> ((~p2(X33, X35)) | (~p2(X32, X34)) | p2(f4(X32, X33), f4(X34, X35)))), (((p2(f4(X32, X33), f4(X34, X35)) | (~p2(X32, X34))) | (~p2(X33, X35))) <=> ((~p2(X33, X35)) | (~p2(X32, X34)) | p2(f4(X32, X33), f4(X34, X35)))))),
% 0.20/0.44 inference(bind,[status(th)],[])).
% 0.20/0.44 tff(67,plain,
% 0.20/0.44 (![X32: $i, X35: $i, X34: $i, X33: $i] : ((p2(f4(X32, X33), f4(X34, X35)) | (~p2(X32, X34))) | (~p2(X33, X35))) <=> ![X32: $i, X35: $i, X34: $i, X33: $i] : ((~p2(X33, X35)) | (~p2(X32, X34)) | p2(f4(X32, X33), f4(X34, X35)))),
% 0.20/0.44 inference(quant_intro,[status(thm)],[66])).
% 0.20/0.44 tff(68,axiom,(![X32: $i, X35: $i, X34: $i, X33: $i] : ((p2(f4(X32, X33), f4(X34, X35)) | (~p2(X32, X34))) | (~p2(X33, X35)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','p2_29')).
% 0.20/0.44 tff(69,plain,
% 0.20/0.44 (![X32: $i, X35: $i, X34: $i, X33: $i] : ((~p2(X33, X35)) | (~p2(X32, X34)) | p2(f4(X32, X33), f4(X34, X35)))),
% 0.20/0.44 inference(modus_ponens,[status(thm)],[68, 67])).
% 0.20/0.44 tff(70,plain,
% 0.20/0.44 (![X32: $i, X35: $i, X34: $i, X33: $i] : ((~p2(X33, X35)) | (~p2(X32, X34)) | p2(f4(X32, X33), f4(X34, X35)))),
% 0.20/0.44 inference(modus_ponens,[status(thm)],[69, 65])).
% 0.20/0.44 tff(71,plain,(
% 0.20/0.44 ![X32: $i, X35: $i, X34: $i, X33: $i] : ((~p2(X33, X35)) | (~p2(X32, X34)) | p2(f4(X32, X33), f4(X34, X35)))),
% 0.20/0.44 inference(skolemize,[status(sab)],[70])).
% 0.20/0.44 tff(72,plain,
% 0.20/0.44 (![X32: $i, X35: $i, X34: $i, X33: $i] : ((~p2(X33, X35)) | (~p2(X32, X34)) | p2(f4(X32, X33), f4(X34, X35)))),
% 0.20/0.44 inference(modus_ponens,[status(thm)],[71, 64])).
% 0.20/0.44 tff(73,plain,
% 0.20/0.44 (((~![X32: $i, X35: $i, X34: $i, X33: $i] : ((~p2(X33, X35)) | (~p2(X32, X34)) | p2(f4(X32, X33), f4(X34, X35)))) | ((~p2(f5(f6(c20)), f5(f6(c20)))) | (~p2(f3(c22), f3(c22))) | p2(f4(f3(c22), f5(f6(c20))), f4(f3(c22), f5(f6(c20)))))) <=> ((~![X32: $i, X35: $i, X34: $i, X33: $i] : ((~p2(X33, X35)) | (~p2(X32, X34)) | p2(f4(X32, X33), f4(X34, X35)))) | (~p2(f5(f6(c20)), f5(f6(c20)))) | (~p2(f3(c22), f3(c22))) | p2(f4(f3(c22), f5(f6(c20))), f4(f3(c22), f5(f6(c20)))))),
% 0.20/0.44 inference(rewrite,[status(thm)],[])).
% 0.20/0.44 tff(74,plain,
% 0.20/0.44 ((~![X32: $i, X35: $i, X34: $i, X33: $i] : ((~p2(X33, X35)) | (~p2(X32, X34)) | p2(f4(X32, X33), f4(X34, X35)))) | ((~p2(f5(f6(c20)), f5(f6(c20)))) | (~p2(f3(c22), f3(c22))) | p2(f4(f3(c22), f5(f6(c20))), f4(f3(c22), f5(f6(c20)))))),
% 0.20/0.44 inference(quant_inst,[status(thm)],[])).
% 0.20/0.44 tff(75,plain,
% 0.20/0.44 ((~![X32: $i, X35: $i, X34: $i, X33: $i] : ((~p2(X33, X35)) | (~p2(X32, X34)) | p2(f4(X32, X33), f4(X34, X35)))) | (~p2(f5(f6(c20)), f5(f6(c20)))) | (~p2(f3(c22), f3(c22))) | p2(f4(f3(c22), f5(f6(c20))), f4(f3(c22), f5(f6(c20))))),
% 0.20/0.44 inference(modus_ponens,[status(thm)],[74, 73])).
% 0.20/0.44 tff(76,plain,
% 0.20/0.44 ((~p2(f5(f6(c20)), f5(f6(c20)))) | (~p2(f3(c22), f3(c22))) | p2(f4(f3(c22), f5(f6(c20))), f4(f3(c22), f5(f6(c20))))),
% 0.20/0.44 inference(unit_resolution,[status(thm)],[75, 72])).
% 0.20/0.44 tff(77,plain,
% 0.20/0.44 (p2(f4(f3(c22), f5(f6(c20))), f4(f3(c22), f5(f6(c20))))),
% 0.20/0.44 inference(unit_resolution,[status(thm)],[76, 62, 58])).
% 0.20/0.44 tff(78,assumption,(~p2(c21, c21)), introduced(assumption)).
% 0.20/0.44 tff(79,plain,
% 0.20/0.44 ((~![X27: $i] : p2(X27, X27)) | p2(c21, c21)),
% 0.20/0.44 inference(quant_inst,[status(thm)],[])).
% 0.20/0.44 tff(80,plain,
% 0.20/0.44 ($false),
% 0.20/0.44 inference(unit_resolution,[status(thm)],[79, 25, 78])).
% 0.20/0.44 tff(81,plain,(p2(c21, c21)), inference(lemma,lemma(discharge,[]))).
% 0.20/0.44 tff(82,plain,
% 0.20/0.44 (((~![X32: $i, X35: $i, X34: $i, X33: $i] : ((~p2(X33, X35)) | (~p2(X32, X34)) | p2(f4(X32, X33), f4(X34, X35)))) | ((~p2(c21, c21)) | (~p2(f4(f3(c22), f5(f6(c20))), f4(f3(c22), f5(f6(c20))))) | p2(f4(f4(f3(c22), f5(f6(c20))), c21), f4(f4(f3(c22), f5(f6(c20))), c21)))) <=> ((~![X32: $i, X35: $i, X34: $i, X33: $i] : ((~p2(X33, X35)) | (~p2(X32, X34)) | p2(f4(X32, X33), f4(X34, X35)))) | (~p2(c21, c21)) | (~p2(f4(f3(c22), f5(f6(c20))), f4(f3(c22), f5(f6(c20))))) | p2(f4(f4(f3(c22), f5(f6(c20))), c21), f4(f4(f3(c22), f5(f6(c20))), c21)))),
% 0.20/0.44 inference(rewrite,[status(thm)],[])).
% 0.20/0.44 tff(83,plain,
% 0.20/0.44 ((~![X32: $i, X35: $i, X34: $i, X33: $i] : ((~p2(X33, X35)) | (~p2(X32, X34)) | p2(f4(X32, X33), f4(X34, X35)))) | ((~p2(c21, c21)) | (~p2(f4(f3(c22), f5(f6(c20))), f4(f3(c22), f5(f6(c20))))) | p2(f4(f4(f3(c22), f5(f6(c20))), c21), f4(f4(f3(c22), f5(f6(c20))), c21)))),
% 0.20/0.44 inference(quant_inst,[status(thm)],[])).
% 0.20/0.44 tff(84,plain,
% 0.20/0.44 ((~![X32: $i, X35: $i, X34: $i, X33: $i] : ((~p2(X33, X35)) | (~p2(X32, X34)) | p2(f4(X32, X33), f4(X34, X35)))) | (~p2(c21, c21)) | (~p2(f4(f3(c22), f5(f6(c20))), f4(f3(c22), f5(f6(c20))))) | p2(f4(f4(f3(c22), f5(f6(c20))), c21), f4(f4(f3(c22), f5(f6(c20))), c21))),
% 0.20/0.44 inference(modus_ponens,[status(thm)],[83, 82])).
% 0.20/0.44 tff(85,plain,
% 0.20/0.44 ((~p2(c21, c21)) | (~p2(f4(f3(c22), f5(f6(c20))), f4(f3(c22), f5(f6(c20))))) | p2(f4(f4(f3(c22), f5(f6(c20))), c21), f4(f4(f3(c22), f5(f6(c20))), c21))),
% 0.20/0.44 inference(unit_resolution,[status(thm)],[84, 72])).
% 0.20/0.44 tff(86,plain,
% 0.20/0.44 (p2(f4(f4(f3(c22), f5(f6(c20))), c21), f4(f4(f3(c22), f5(f6(c20))), c21))),
% 0.20/0.44 inference(unit_resolution,[status(thm)],[85, 81, 77])).
% 0.20/0.44 tff(87,plain,
% 0.20/0.44 (^[X27: $i, X29: $i, X28: $i] : refl((p2(X28, X29) | (~p2(X27, X29)) | (~p2(X27, X28))) <=> (p2(X28, X29) | (~p2(X27, X29)) | (~p2(X27, X28))))),
% 0.20/0.44 inference(bind,[status(th)],[])).
% 0.20/0.44 tff(88,plain,
% 0.20/0.44 (![X27: $i, X29: $i, X28: $i] : (p2(X28, X29) | (~p2(X27, X29)) | (~p2(X27, X28))) <=> ![X27: $i, X29: $i, X28: $i] : (p2(X28, X29) | (~p2(X27, X29)) | (~p2(X27, X28)))),
% 0.20/0.44 inference(quant_intro,[status(thm)],[87])).
% 0.20/0.44 tff(89,plain,
% 0.20/0.44 (![X27: $i, X29: $i, X28: $i] : (p2(X28, X29) | (~p2(X27, X29)) | (~p2(X27, X28))) <=> ![X27: $i, X29: $i, X28: $i] : (p2(X28, X29) | (~p2(X27, X29)) | (~p2(X27, X28)))),
% 0.20/0.44 inference(rewrite,[status(thm)],[])).
% 0.20/0.44 tff(90,plain,
% 0.20/0.44 (^[X27: $i, X29: $i, X28: $i] : trans(monotonicity(rewrite((p2(X28, X29) | (~p2(X27, X28))) <=> (p2(X28, X29) | (~p2(X27, X28)))), (((p2(X28, X29) | (~p2(X27, X28))) | (~p2(X27, X29))) <=> ((p2(X28, X29) | (~p2(X27, X28))) | (~p2(X27, X29))))), rewrite(((p2(X28, X29) | (~p2(X27, X28))) | (~p2(X27, X29))) <=> (p2(X28, X29) | (~p2(X27, X29)) | (~p2(X27, X28)))), (((p2(X28, X29) | (~p2(X27, X28))) | (~p2(X27, X29))) <=> (p2(X28, X29) | (~p2(X27, X29)) | (~p2(X27, X28)))))),
% 0.20/0.44 inference(bind,[status(th)],[])).
% 0.20/0.44 tff(91,plain,
% 0.20/0.44 (![X27: $i, X29: $i, X28: $i] : ((p2(X28, X29) | (~p2(X27, X28))) | (~p2(X27, X29))) <=> ![X27: $i, X29: $i, X28: $i] : (p2(X28, X29) | (~p2(X27, X29)) | (~p2(X27, X28)))),
% 0.20/0.44 inference(quant_intro,[status(thm)],[90])).
% 0.20/0.44 tff(92,axiom,(![X27: $i, X29: $i, X28: $i] : ((p2(X28, X29) | (~p2(X27, X28))) | (~p2(X27, X29)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','p2_23')).
% 0.20/0.44 tff(93,plain,
% 0.20/0.44 (![X27: $i, X29: $i, X28: $i] : (p2(X28, X29) | (~p2(X27, X29)) | (~p2(X27, X28)))),
% 0.20/0.44 inference(modus_ponens,[status(thm)],[92, 91])).
% 0.20/0.44 tff(94,plain,
% 0.20/0.44 (![X27: $i, X29: $i, X28: $i] : (p2(X28, X29) | (~p2(X27, X29)) | (~p2(X27, X28)))),
% 0.20/0.44 inference(modus_ponens,[status(thm)],[93, 89])).
% 0.20/0.44 tff(95,plain,(
% 0.20/0.44 ![X27: $i, X29: $i, X28: $i] : (p2(X28, X29) | (~p2(X27, X29)) | (~p2(X27, X28)))),
% 0.20/0.44 inference(skolemize,[status(sab)],[94])).
% 0.20/0.44 tff(96,plain,
% 0.20/0.44 (![X27: $i, X29: $i, X28: $i] : (p2(X28, X29) | (~p2(X27, X29)) | (~p2(X27, X28)))),
% 0.20/0.44 inference(modus_ponens,[status(thm)],[95, 88])).
% 0.20/0.44 tff(97,plain,
% 0.20/0.44 (((~![X27: $i, X29: $i, X28: $i] : (p2(X28, X29) | (~p2(X27, X29)) | (~p2(X27, X28)))) | ((~p2(f4(f4(f3(c22), f5(f6(c20))), c21), f4(f4(f3(c22), f5(f6(c20))), c21))) | p2(f3(f4(f4(c22, f5(f6(c20))), c21)), f4(f4(f3(c22), f5(f6(c20))), c21)) | (~p2(f4(f4(f3(c22), f5(f6(c20))), c21), f3(f4(f4(c22, f5(f6(c20))), c21)))))) <=> ((~![X27: $i, X29: $i, X28: $i] : (p2(X28, X29) | (~p2(X27, X29)) | (~p2(X27, X28)))) | (~p2(f4(f4(f3(c22), f5(f6(c20))), c21), f4(f4(f3(c22), f5(f6(c20))), c21))) | p2(f3(f4(f4(c22, f5(f6(c20))), c21)), f4(f4(f3(c22), f5(f6(c20))), c21)) | (~p2(f4(f4(f3(c22), f5(f6(c20))), c21), f3(f4(f4(c22, f5(f6(c20))), c21)))))),
% 0.20/0.44 inference(rewrite,[status(thm)],[])).
% 0.20/0.44 tff(98,plain,
% 0.20/0.44 ((p2(f3(f4(f4(c22, f5(f6(c20))), c21)), f4(f4(f3(c22), f5(f6(c20))), c21)) | (~p2(f4(f4(f3(c22), f5(f6(c20))), c21), f4(f4(f3(c22), f5(f6(c20))), c21))) | (~p2(f4(f4(f3(c22), f5(f6(c20))), c21), f3(f4(f4(c22, f5(f6(c20))), c21))))) <=> ((~p2(f4(f4(f3(c22), f5(f6(c20))), c21), f4(f4(f3(c22), f5(f6(c20))), c21))) | p2(f3(f4(f4(c22, f5(f6(c20))), c21)), f4(f4(f3(c22), f5(f6(c20))), c21)) | (~p2(f4(f4(f3(c22), f5(f6(c20))), c21), f3(f4(f4(c22, f5(f6(c20))), c21)))))),
% 0.20/0.44 inference(rewrite,[status(thm)],[])).
% 0.20/0.44 tff(99,plain,
% 0.20/0.44 (((~![X27: $i, X29: $i, X28: $i] : (p2(X28, X29) | (~p2(X27, X29)) | (~p2(X27, X28)))) | (p2(f3(f4(f4(c22, f5(f6(c20))), c21)), f4(f4(f3(c22), f5(f6(c20))), c21)) | (~p2(f4(f4(f3(c22), f5(f6(c20))), c21), f4(f4(f3(c22), f5(f6(c20))), c21))) | (~p2(f4(f4(f3(c22), f5(f6(c20))), c21), f3(f4(f4(c22, f5(f6(c20))), c21)))))) <=> ((~![X27: $i, X29: $i, X28: $i] : (p2(X28, X29) | (~p2(X27, X29)) | (~p2(X27, X28)))) | ((~p2(f4(f4(f3(c22), f5(f6(c20))), c21), f4(f4(f3(c22), f5(f6(c20))), c21))) | p2(f3(f4(f4(c22, f5(f6(c20))), c21)), f4(f4(f3(c22), f5(f6(c20))), c21)) | (~p2(f4(f4(f3(c22), f5(f6(c20))), c21), f3(f4(f4(c22, f5(f6(c20))), c21))))))),
% 0.20/0.44 inference(monotonicity,[status(thm)],[98])).
% 0.20/0.44 tff(100,plain,
% 0.20/0.44 (((~![X27: $i, X29: $i, X28: $i] : (p2(X28, X29) | (~p2(X27, X29)) | (~p2(X27, X28)))) | (p2(f3(f4(f4(c22, f5(f6(c20))), c21)), f4(f4(f3(c22), f5(f6(c20))), c21)) | (~p2(f4(f4(f3(c22), f5(f6(c20))), c21), f4(f4(f3(c22), f5(f6(c20))), c21))) | (~p2(f4(f4(f3(c22), f5(f6(c20))), c21), f3(f4(f4(c22, f5(f6(c20))), c21)))))) <=> ((~![X27: $i, X29: $i, X28: $i] : (p2(X28, X29) | (~p2(X27, X29)) | (~p2(X27, X28)))) | (~p2(f4(f4(f3(c22), f5(f6(c20))), c21), f4(f4(f3(c22), f5(f6(c20))), c21))) | p2(f3(f4(f4(c22, f5(f6(c20))), c21)), f4(f4(f3(c22), f5(f6(c20))), c21)) | (~p2(f4(f4(f3(c22), f5(f6(c20))), c21), f3(f4(f4(c22, f5(f6(c20))), c21)))))),
% 0.20/0.44 inference(transitivity,[status(thm)],[99, 97])).
% 0.20/0.44 tff(101,plain,
% 0.20/0.44 ((~![X27: $i, X29: $i, X28: $i] : (p2(X28, X29) | (~p2(X27, X29)) | (~p2(X27, X28)))) | (p2(f3(f4(f4(c22, f5(f6(c20))), c21)), f4(f4(f3(c22), f5(f6(c20))), c21)) | (~p2(f4(f4(f3(c22), f5(f6(c20))), c21), f4(f4(f3(c22), f5(f6(c20))), c21))) | (~p2(f4(f4(f3(c22), f5(f6(c20))), c21), f3(f4(f4(c22, f5(f6(c20))), c21)))))),
% 0.20/0.44 inference(quant_inst,[status(thm)],[])).
% 0.20/0.44 tff(102,plain,
% 0.20/0.44 ((~![X27: $i, X29: $i, X28: $i] : (p2(X28, X29) | (~p2(X27, X29)) | (~p2(X27, X28)))) | (~p2(f4(f4(f3(c22), f5(f6(c20))), c21), f4(f4(f3(c22), f5(f6(c20))), c21))) | p2(f3(f4(f4(c22, f5(f6(c20))), c21)), f4(f4(f3(c22), f5(f6(c20))), c21)) | (~p2(f4(f4(f3(c22), f5(f6(c20))), c21), f3(f4(f4(c22, f5(f6(c20))), c21))))),
% 0.20/0.44 inference(modus_ponens,[status(thm)],[101, 100])).
% 0.20/0.44 tff(103,plain,
% 0.20/0.44 (p2(f3(f4(f4(c22, f5(f6(c20))), c21)), f4(f4(f3(c22), f5(f6(c20))), c21))),
% 0.20/0.44 inference(unit_resolution,[status(thm)],[102, 96, 86, 17])).
% 0.20/0.44 tff(104,assumption,(~p11(f14(c23, c24), f14(c23, c24))), introduced(assumption)).
% 0.20/0.44 tff(105,plain,
% 0.20/0.44 (^[X0: $i] : refl(p11(X0, X0) <=> p11(X0, X0))),
% 0.20/0.44 inference(bind,[status(th)],[])).
% 0.20/0.44 tff(106,plain,
% 0.20/0.44 (![X0: $i] : p11(X0, X0) <=> ![X0: $i] : p11(X0, X0)),
% 0.20/0.44 inference(quant_intro,[status(thm)],[105])).
% 0.20/0.44 tff(107,plain,
% 0.20/0.44 (![X0: $i] : p11(X0, X0) <=> ![X0: $i] : p11(X0, X0)),
% 0.20/0.44 inference(rewrite,[status(thm)],[])).
% 0.20/0.44 tff(108,axiom,(![X0: $i] : p11(X0, X0)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','p11_1')).
% 0.20/0.44 tff(109,plain,
% 0.20/0.44 (![X0: $i] : p11(X0, X0)),
% 0.20/0.44 inference(modus_ponens,[status(thm)],[108, 107])).
% 0.20/0.44 tff(110,plain,(
% 0.20/0.44 ![X0: $i] : p11(X0, X0)),
% 0.20/0.44 inference(skolemize,[status(sab)],[109])).
% 0.20/0.44 tff(111,plain,
% 0.20/0.44 (![X0: $i] : p11(X0, X0)),
% 0.20/0.44 inference(modus_ponens,[status(thm)],[110, 106])).
% 0.20/0.44 tff(112,plain,
% 0.20/0.44 ((~![X0: $i] : p11(X0, X0)) | p11(f14(c23, c24), f14(c23, c24))),
% 0.20/0.44 inference(quant_inst,[status(thm)],[])).
% 0.20/0.44 tff(113,plain,
% 0.20/0.44 ($false),
% 0.20/0.44 inference(unit_resolution,[status(thm)],[112, 111, 104])).
% 0.20/0.44 tff(114,plain,(p11(f14(c23, c24), f14(c23, c24))), inference(lemma,lemma(discharge,[]))).
% 0.20/0.44 tff(115,plain,
% 0.20/0.44 (^[X14: $i, X17: $i, X16: $i, X15: $i] : refl(((~p11(X15, X17)) | (~p2(X14, X16)) | p13(f15(X14, X15), f15(X16, X17))) <=> ((~p11(X15, X17)) | (~p2(X14, X16)) | p13(f15(X14, X15), f15(X16, X17))))),
% 0.20/0.44 inference(bind,[status(th)],[])).
% 0.20/0.44 tff(116,plain,
% 0.20/0.44 (![X14: $i, X17: $i, X16: $i, X15: $i] : ((~p11(X15, X17)) | (~p2(X14, X16)) | p13(f15(X14, X15), f15(X16, X17))) <=> ![X14: $i, X17: $i, X16: $i, X15: $i] : ((~p11(X15, X17)) | (~p2(X14, X16)) | p13(f15(X14, X15), f15(X16, X17)))),
% 0.20/0.44 inference(quant_intro,[status(thm)],[115])).
% 0.20/0.44 tff(117,plain,
% 0.20/0.44 (![X14: $i, X17: $i, X16: $i, X15: $i] : ((~p11(X15, X17)) | (~p2(X14, X16)) | p13(f15(X14, X15), f15(X16, X17))) <=> ![X14: $i, X17: $i, X16: $i, X15: $i] : ((~p11(X15, X17)) | (~p2(X14, X16)) | p13(f15(X14, X15), f15(X16, X17)))),
% 0.20/0.44 inference(rewrite,[status(thm)],[])).
% 0.20/0.44 tff(118,plain,
% 0.20/0.44 (^[X14: $i, X17: $i, X16: $i, X15: $i] : trans(monotonicity(rewrite((p13(f15(X14, X15), f15(X16, X17)) | (~p11(X15, X17))) <=> ((~p11(X15, X17)) | p13(f15(X14, X15), f15(X16, X17)))), (((p13(f15(X14, X15), f15(X16, X17)) | (~p11(X15, X17))) | (~p2(X14, X16))) <=> (((~p11(X15, X17)) | p13(f15(X14, X15), f15(X16, X17))) | (~p2(X14, X16))))), rewrite((((~p11(X15, X17)) | p13(f15(X14, X15), f15(X16, X17))) | (~p2(X14, X16))) <=> ((~p11(X15, X17)) | (~p2(X14, X16)) | p13(f15(X14, X15), f15(X16, X17)))), (((p13(f15(X14, X15), f15(X16, X17)) | (~p11(X15, X17))) | (~p2(X14, X16))) <=> ((~p11(X15, X17)) | (~p2(X14, X16)) | p13(f15(X14, X15), f15(X16, X17)))))),
% 0.20/0.44 inference(bind,[status(th)],[])).
% 0.20/0.44 tff(119,plain,
% 0.20/0.44 (![X14: $i, X17: $i, X16: $i, X15: $i] : ((p13(f15(X14, X15), f15(X16, X17)) | (~p11(X15, X17))) | (~p2(X14, X16))) <=> ![X14: $i, X17: $i, X16: $i, X15: $i] : ((~p11(X15, X17)) | (~p2(X14, X16)) | p13(f15(X14, X15), f15(X16, X17)))),
% 0.20/0.44 inference(quant_intro,[status(thm)],[118])).
% 0.20/0.44 tff(120,axiom,(![X14: $i, X17: $i, X16: $i, X15: $i] : ((p13(f15(X14, X15), f15(X16, X17)) | (~p11(X15, X17))) | (~p2(X14, X16)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','p13_28')).
% 0.20/0.44 tff(121,plain,
% 0.20/0.44 (![X14: $i, X17: $i, X16: $i, X15: $i] : ((~p11(X15, X17)) | (~p2(X14, X16)) | p13(f15(X14, X15), f15(X16, X17)))),
% 0.20/0.44 inference(modus_ponens,[status(thm)],[120, 119])).
% 0.20/0.44 tff(122,plain,
% 0.20/0.44 (![X14: $i, X17: $i, X16: $i, X15: $i] : ((~p11(X15, X17)) | (~p2(X14, X16)) | p13(f15(X14, X15), f15(X16, X17)))),
% 0.20/0.44 inference(modus_ponens,[status(thm)],[121, 117])).
% 0.20/0.44 tff(123,plain,(
% 0.20/0.44 ![X14: $i, X17: $i, X16: $i, X15: $i] : ((~p11(X15, X17)) | (~p2(X14, X16)) | p13(f15(X14, X15), f15(X16, X17)))),
% 0.20/0.44 inference(skolemize,[status(sab)],[122])).
% 0.20/0.44 tff(124,plain,
% 0.20/0.44 (![X14: $i, X17: $i, X16: $i, X15: $i] : ((~p11(X15, X17)) | (~p2(X14, X16)) | p13(f15(X14, X15), f15(X16, X17)))),
% 0.20/0.44 inference(modus_ponens,[status(thm)],[123, 116])).
% 0.20/0.44 tff(125,plain,
% 0.20/0.44 (((~![X14: $i, X17: $i, X16: $i, X15: $i] : ((~p11(X15, X17)) | (~p2(X14, X16)) | p13(f15(X14, X15), f15(X16, X17)))) | ((~p11(f14(c23, c24), f14(c23, c24))) | (~p2(f3(f4(f4(c22, f5(f6(c20))), c21)), f4(f4(f3(c22), f5(f6(c20))), c21))) | p13(f15(f3(f4(f4(c22, f5(f6(c20))), c21)), f14(c23, c24)), f15(f4(f4(f3(c22), f5(f6(c20))), c21), f14(c23, c24))))) <=> ((~![X14: $i, X17: $i, X16: $i, X15: $i] : ((~p11(X15, X17)) | (~p2(X14, X16)) | p13(f15(X14, X15), f15(X16, X17)))) | (~p11(f14(c23, c24), f14(c23, c24))) | (~p2(f3(f4(f4(c22, f5(f6(c20))), c21)), f4(f4(f3(c22), f5(f6(c20))), c21))) | p13(f15(f3(f4(f4(c22, f5(f6(c20))), c21)), f14(c23, c24)), f15(f4(f4(f3(c22), f5(f6(c20))), c21), f14(c23, c24))))),
% 0.20/0.44 inference(rewrite,[status(thm)],[])).
% 0.20/0.44 tff(126,plain,
% 0.20/0.44 ((~![X14: $i, X17: $i, X16: $i, X15: $i] : ((~p11(X15, X17)) | (~p2(X14, X16)) | p13(f15(X14, X15), f15(X16, X17)))) | ((~p11(f14(c23, c24), f14(c23, c24))) | (~p2(f3(f4(f4(c22, f5(f6(c20))), c21)), f4(f4(f3(c22), f5(f6(c20))), c21))) | p13(f15(f3(f4(f4(c22, f5(f6(c20))), c21)), f14(c23, c24)), f15(f4(f4(f3(c22), f5(f6(c20))), c21), f14(c23, c24))))),
% 0.20/0.44 inference(quant_inst,[status(thm)],[])).
% 0.20/0.44 tff(127,plain,
% 0.20/0.44 ((~![X14: $i, X17: $i, X16: $i, X15: $i] : ((~p11(X15, X17)) | (~p2(X14, X16)) | p13(f15(X14, X15), f15(X16, X17)))) | (~p11(f14(c23, c24), f14(c23, c24))) | (~p2(f3(f4(f4(c22, f5(f6(c20))), c21)), f4(f4(f3(c22), f5(f6(c20))), c21))) | p13(f15(f3(f4(f4(c22, f5(f6(c20))), c21)), f14(c23, c24)), f15(f4(f4(f3(c22), f5(f6(c20))), c21), f14(c23, c24)))),
% 0.20/0.44 inference(modus_ponens,[status(thm)],[126, 125])).
% 0.20/0.45 tff(128,plain,
% 0.20/0.45 (p13(f15(f3(f4(f4(c22, f5(f6(c20))), c21)), f14(c23, c24)), f15(f4(f4(f3(c22), f5(f6(c20))), c21), f14(c23, c24)))),
% 0.20/0.45 inference(unit_resolution,[status(thm)],[127, 124, 114, 103])).
% 0.20/0.45 tff(129,plain,
% 0.20/0.45 (^[X18: $i, X19: $i] : refl(p13(f15(f3(X18), X19), f15(X18, f12(X19))) <=> p13(f15(f3(X18), X19), f15(X18, f12(X19))))),
% 0.20/0.45 inference(bind,[status(th)],[])).
% 0.20/0.45 tff(130,plain,
% 0.20/0.45 (![X18: $i, X19: $i] : p13(f15(f3(X18), X19), f15(X18, f12(X19))) <=> ![X18: $i, X19: $i] : p13(f15(f3(X18), X19), f15(X18, f12(X19)))),
% 0.20/0.45 inference(quant_intro,[status(thm)],[129])).
% 0.20/0.45 tff(131,plain,
% 0.20/0.45 (![X18: $i, X19: $i] : p13(f15(f3(X18), X19), f15(X18, f12(X19))) <=> ![X18: $i, X19: $i] : p13(f15(f3(X18), X19), f15(X18, f12(X19)))),
% 0.20/0.45 inference(rewrite,[status(thm)],[])).
% 0.20/0.45 tff(132,axiom,(![X18: $i, X19: $i] : p13(f15(f3(X18), X19), f15(X18, f12(X19)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','p13_19')).
% 0.20/0.45 tff(133,plain,
% 0.20/0.45 (![X18: $i, X19: $i] : p13(f15(f3(X18), X19), f15(X18, f12(X19)))),
% 0.20/0.45 inference(modus_ponens,[status(thm)],[132, 131])).
% 0.20/0.45 tff(134,plain,(
% 0.20/0.45 ![X18: $i, X19: $i] : p13(f15(f3(X18), X19), f15(X18, f12(X19)))),
% 0.20/0.45 inference(skolemize,[status(sab)],[133])).
% 0.20/0.45 tff(135,plain,
% 0.20/0.45 (![X18: $i, X19: $i] : p13(f15(f3(X18), X19), f15(X18, f12(X19)))),
% 0.20/0.45 inference(modus_ponens,[status(thm)],[134, 130])).
% 0.20/0.45 tff(136,plain,
% 0.20/0.45 ((~![X18: $i, X19: $i] : p13(f15(f3(X18), X19), f15(X18, f12(X19)))) | p13(f15(f3(f4(f4(c22, f5(f6(c20))), c21)), f14(c23, c24)), f15(f4(f4(c22, f5(f6(c20))), c21), f12(f14(c23, c24))))),
% 0.20/0.45 inference(quant_inst,[status(thm)],[])).
% 0.20/0.45 tff(137,plain,
% 0.20/0.45 (p13(f15(f3(f4(f4(c22, f5(f6(c20))), c21)), f14(c23, c24)), f15(f4(f4(c22, f5(f6(c20))), c21), f12(f14(c23, c24))))),
% 0.20/0.45 inference(unit_resolution,[status(thm)],[136, 135])).
% 0.20/0.45 tff(138,plain,
% 0.20/0.45 (^[X12: $i, X11: $i, X13: $i] : refl(((~p13(X11, X13)) | (~p13(X11, X12)) | p13(X12, X13)) <=> ((~p13(X11, X13)) | (~p13(X11, X12)) | p13(X12, X13)))),
% 0.20/0.45 inference(bind,[status(th)],[])).
% 0.20/0.45 tff(139,plain,
% 0.20/0.45 (![X12: $i, X11: $i, X13: $i] : ((~p13(X11, X13)) | (~p13(X11, X12)) | p13(X12, X13)) <=> ![X12: $i, X11: $i, X13: $i] : ((~p13(X11, X13)) | (~p13(X11, X12)) | p13(X12, X13))),
% 0.20/0.45 inference(quant_intro,[status(thm)],[138])).
% 0.20/0.45 tff(140,plain,
% 0.20/0.45 (![X12: $i, X11: $i, X13: $i] : ((~p13(X11, X13)) | (~p13(X11, X12)) | p13(X12, X13)) <=> ![X12: $i, X11: $i, X13: $i] : ((~p13(X11, X13)) | (~p13(X11, X12)) | p13(X12, X13))),
% 0.20/0.45 inference(rewrite,[status(thm)],[])).
% 0.20/0.45 tff(141,plain,
% 0.20/0.45 (^[X12: $i, X11: $i, X13: $i] : trans(monotonicity(rewrite((p13(X12, X13) | (~p13(X11, X12))) <=> ((~p13(X11, X12)) | p13(X12, X13))), (((p13(X12, X13) | (~p13(X11, X12))) | (~p13(X11, X13))) <=> (((~p13(X11, X12)) | p13(X12, X13)) | (~p13(X11, X13))))), rewrite((((~p13(X11, X12)) | p13(X12, X13)) | (~p13(X11, X13))) <=> ((~p13(X11, X13)) | (~p13(X11, X12)) | p13(X12, X13))), (((p13(X12, X13) | (~p13(X11, X12))) | (~p13(X11, X13))) <=> ((~p13(X11, X13)) | (~p13(X11, X12)) | p13(X12, X13))))),
% 0.20/0.45 inference(bind,[status(th)],[])).
% 0.20/0.45 tff(142,plain,
% 0.20/0.45 (![X12: $i, X11: $i, X13: $i] : ((p13(X12, X13) | (~p13(X11, X12))) | (~p13(X11, X13))) <=> ![X12: $i, X11: $i, X13: $i] : ((~p13(X11, X13)) | (~p13(X11, X12)) | p13(X12, X13))),
% 0.20/0.45 inference(quant_intro,[status(thm)],[141])).
% 0.20/0.45 tff(143,axiom,(![X12: $i, X11: $i, X13: $i] : ((p13(X12, X13) | (~p13(X11, X12))) | (~p13(X11, X13)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','p13_24')).
% 0.20/0.45 tff(144,plain,
% 0.20/0.45 (![X12: $i, X11: $i, X13: $i] : ((~p13(X11, X13)) | (~p13(X11, X12)) | p13(X12, X13))),
% 0.20/0.45 inference(modus_ponens,[status(thm)],[143, 142])).
% 0.20/0.45 tff(145,plain,
% 0.20/0.45 (![X12: $i, X11: $i, X13: $i] : ((~p13(X11, X13)) | (~p13(X11, X12)) | p13(X12, X13))),
% 0.20/0.45 inference(modus_ponens,[status(thm)],[144, 140])).
% 0.20/0.45 tff(146,plain,(
% 0.20/0.45 ![X12: $i, X11: $i, X13: $i] : ((~p13(X11, X13)) | (~p13(X11, X12)) | p13(X12, X13))),
% 0.20/0.45 inference(skolemize,[status(sab)],[145])).
% 0.20/0.45 tff(147,plain,
% 0.20/0.45 (![X12: $i, X11: $i, X13: $i] : ((~p13(X11, X13)) | (~p13(X11, X12)) | p13(X12, X13))),
% 0.20/0.45 inference(modus_ponens,[status(thm)],[146, 139])).
% 0.20/0.45 tff(148,plain,
% 0.20/0.45 (((~![X12: $i, X11: $i, X13: $i] : ((~p13(X11, X13)) | (~p13(X11, X12)) | p13(X12, X13))) | (p13(f15(f4(f4(c22, f5(f6(c20))), c21), f12(f14(c23, c24))), f15(f4(f4(f3(c22), f5(f6(c20))), c21), f14(c23, c24))) | (~p13(f15(f3(f4(f4(c22, f5(f6(c20))), c21)), f14(c23, c24)), f15(f4(f4(f3(c22), f5(f6(c20))), c21), f14(c23, c24)))) | (~p13(f15(f3(f4(f4(c22, f5(f6(c20))), c21)), f14(c23, c24)), f15(f4(f4(c22, f5(f6(c20))), c21), f12(f14(c23, c24))))))) <=> ((~![X12: $i, X11: $i, X13: $i] : ((~p13(X11, X13)) | (~p13(X11, X12)) | p13(X12, X13))) | p13(f15(f4(f4(c22, f5(f6(c20))), c21), f12(f14(c23, c24))), f15(f4(f4(f3(c22), f5(f6(c20))), c21), f14(c23, c24))) | (~p13(f15(f3(f4(f4(c22, f5(f6(c20))), c21)), f14(c23, c24)), f15(f4(f4(f3(c22), f5(f6(c20))), c21), f14(c23, c24)))) | (~p13(f15(f3(f4(f4(c22, f5(f6(c20))), c21)), f14(c23, c24)), f15(f4(f4(c22, f5(f6(c20))), c21), f12(f14(c23, c24))))))),
% 0.20/0.45 inference(rewrite,[status(thm)],[])).
% 0.20/0.45 tff(149,plain,
% 0.20/0.45 (((~p13(f15(f3(f4(f4(c22, f5(f6(c20))), c21)), f14(c23, c24)), f15(f4(f4(f3(c22), f5(f6(c20))), c21), f14(c23, c24)))) | (~p13(f15(f3(f4(f4(c22, f5(f6(c20))), c21)), f14(c23, c24)), f15(f4(f4(c22, f5(f6(c20))), c21), f12(f14(c23, c24))))) | p13(f15(f4(f4(c22, f5(f6(c20))), c21), f12(f14(c23, c24))), f15(f4(f4(f3(c22), f5(f6(c20))), c21), f14(c23, c24)))) <=> (p13(f15(f4(f4(c22, f5(f6(c20))), c21), f12(f14(c23, c24))), f15(f4(f4(f3(c22), f5(f6(c20))), c21), f14(c23, c24))) | (~p13(f15(f3(f4(f4(c22, f5(f6(c20))), c21)), f14(c23, c24)), f15(f4(f4(f3(c22), f5(f6(c20))), c21), f14(c23, c24)))) | (~p13(f15(f3(f4(f4(c22, f5(f6(c20))), c21)), f14(c23, c24)), f15(f4(f4(c22, f5(f6(c20))), c21), f12(f14(c23, c24))))))),
% 0.20/0.45 inference(rewrite,[status(thm)],[])).
% 0.20/0.45 tff(150,plain,
% 0.20/0.45 (((~![X12: $i, X11: $i, X13: $i] : ((~p13(X11, X13)) | (~p13(X11, X12)) | p13(X12, X13))) | ((~p13(f15(f3(f4(f4(c22, f5(f6(c20))), c21)), f14(c23, c24)), f15(f4(f4(f3(c22), f5(f6(c20))), c21), f14(c23, c24)))) | (~p13(f15(f3(f4(f4(c22, f5(f6(c20))), c21)), f14(c23, c24)), f15(f4(f4(c22, f5(f6(c20))), c21), f12(f14(c23, c24))))) | p13(f15(f4(f4(c22, f5(f6(c20))), c21), f12(f14(c23, c24))), f15(f4(f4(f3(c22), f5(f6(c20))), c21), f14(c23, c24))))) <=> ((~![X12: $i, X11: $i, X13: $i] : ((~p13(X11, X13)) | (~p13(X11, X12)) | p13(X12, X13))) | (p13(f15(f4(f4(c22, f5(f6(c20))), c21), f12(f14(c23, c24))), f15(f4(f4(f3(c22), f5(f6(c20))), c21), f14(c23, c24))) | (~p13(f15(f3(f4(f4(c22, f5(f6(c20))), c21)), f14(c23, c24)), f15(f4(f4(f3(c22), f5(f6(c20))), c21), f14(c23, c24)))) | (~p13(f15(f3(f4(f4(c22, f5(f6(c20))), c21)), f14(c23, c24)), f15(f4(f4(c22, f5(f6(c20))), c21), f12(f14(c23, c24)))))))),
% 0.20/0.45 inference(monotonicity,[status(thm)],[149])).
% 0.20/0.45 tff(151,plain,
% 0.20/0.45 (((~![X12: $i, X11: $i, X13: $i] : ((~p13(X11, X13)) | (~p13(X11, X12)) | p13(X12, X13))) | ((~p13(f15(f3(f4(f4(c22, f5(f6(c20))), c21)), f14(c23, c24)), f15(f4(f4(f3(c22), f5(f6(c20))), c21), f14(c23, c24)))) | (~p13(f15(f3(f4(f4(c22, f5(f6(c20))), c21)), f14(c23, c24)), f15(f4(f4(c22, f5(f6(c20))), c21), f12(f14(c23, c24))))) | p13(f15(f4(f4(c22, f5(f6(c20))), c21), f12(f14(c23, c24))), f15(f4(f4(f3(c22), f5(f6(c20))), c21), f14(c23, c24))))) <=> ((~![X12: $i, X11: $i, X13: $i] : ((~p13(X11, X13)) | (~p13(X11, X12)) | p13(X12, X13))) | p13(f15(f4(f4(c22, f5(f6(c20))), c21), f12(f14(c23, c24))), f15(f4(f4(f3(c22), f5(f6(c20))), c21), f14(c23, c24))) | (~p13(f15(f3(f4(f4(c22, f5(f6(c20))), c21)), f14(c23, c24)), f15(f4(f4(f3(c22), f5(f6(c20))), c21), f14(c23, c24)))) | (~p13(f15(f3(f4(f4(c22, f5(f6(c20))), c21)), f14(c23, c24)), f15(f4(f4(c22, f5(f6(c20))), c21), f12(f14(c23, c24))))))),
% 0.20/0.45 inference(transitivity,[status(thm)],[150, 148])).
% 0.20/0.45 tff(152,plain,
% 0.20/0.45 ((~![X12: $i, X11: $i, X13: $i] : ((~p13(X11, X13)) | (~p13(X11, X12)) | p13(X12, X13))) | ((~p13(f15(f3(f4(f4(c22, f5(f6(c20))), c21)), f14(c23, c24)), f15(f4(f4(f3(c22), f5(f6(c20))), c21), f14(c23, c24)))) | (~p13(f15(f3(f4(f4(c22, f5(f6(c20))), c21)), f14(c23, c24)), f15(f4(f4(c22, f5(f6(c20))), c21), f12(f14(c23, c24))))) | p13(f15(f4(f4(c22, f5(f6(c20))), c21), f12(f14(c23, c24))), f15(f4(f4(f3(c22), f5(f6(c20))), c21), f14(c23, c24))))),
% 0.20/0.45 inference(quant_inst,[status(thm)],[])).
% 0.20/0.45 tff(153,plain,
% 0.20/0.45 ((~![X12: $i, X11: $i, X13: $i] : ((~p13(X11, X13)) | (~p13(X11, X12)) | p13(X12, X13))) | p13(f15(f4(f4(c22, f5(f6(c20))), c21), f12(f14(c23, c24))), f15(f4(f4(f3(c22), f5(f6(c20))), c21), f14(c23, c24))) | (~p13(f15(f3(f4(f4(c22, f5(f6(c20))), c21)), f14(c23, c24)), f15(f4(f4(f3(c22), f5(f6(c20))), c21), f14(c23, c24)))) | (~p13(f15(f3(f4(f4(c22, f5(f6(c20))), c21)), f14(c23, c24)), f15(f4(f4(c22, f5(f6(c20))), c21), f12(f14(c23, c24)))))),
% 0.20/0.45 inference(modus_ponens,[status(thm)],[152, 151])).
% 0.20/0.45 tff(154,plain,
% 0.20/0.45 (p13(f15(f4(f4(c22, f5(f6(c20))), c21), f12(f14(c23, c24))), f15(f4(f4(f3(c22), f5(f6(c20))), c21), f14(c23, c24)))),
% 0.20/0.45 inference(unit_resolution,[status(thm)],[153, 147, 137, 128])).
% 0.20/0.45 tff(155,assumption,(~p2(f4(f4(c22, f5(f6(c20))), c21), f4(f4(c22, f5(f6(c20))), c21))), introduced(assumption)).
% 0.20/0.45 tff(156,plain,
% 0.20/0.45 ((~![X27: $i] : p2(X27, X27)) | p2(f4(f4(c22, f5(f6(c20))), c21), f4(f4(c22, f5(f6(c20))), c21))),
% 0.20/0.45 inference(quant_inst,[status(thm)],[])).
% 0.20/0.45 tff(157,plain,
% 0.20/0.45 ($false),
% 0.20/0.45 inference(unit_resolution,[status(thm)],[156, 25, 155])).
% 0.20/0.45 tff(158,plain,(p2(f4(f4(c22, f5(f6(c20))), c21), f4(f4(c22, f5(f6(c20))), c21))), inference(lemma,lemma(discharge,[]))).
% 0.20/0.45 tff(159,plain,
% 0.20/0.45 (^[X6: $i, X5: $i] : refl(p11(f12(f14(X5, X6)), X6) <=> p11(f12(f14(X5, X6)), X6))),
% 0.20/0.45 inference(bind,[status(th)],[])).
% 0.20/0.45 tff(160,plain,
% 0.20/0.45 (![X6: $i, X5: $i] : p11(f12(f14(X5, X6)), X6) <=> ![X6: $i, X5: $i] : p11(f12(f14(X5, X6)), X6)),
% 0.20/0.45 inference(quant_intro,[status(thm)],[159])).
% 0.20/0.45 tff(161,plain,
% 0.20/0.45 (![X6: $i, X5: $i] : p11(f12(f14(X5, X6)), X6) <=> ![X6: $i, X5: $i] : p11(f12(f14(X5, X6)), X6)),
% 0.20/0.45 inference(rewrite,[status(thm)],[])).
% 0.20/0.45 tff(162,axiom,(![X6: $i, X5: $i] : p11(f12(f14(X5, X6)), X6)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','p11_7')).
% 0.20/0.45 tff(163,plain,
% 0.20/0.45 (![X6: $i, X5: $i] : p11(f12(f14(X5, X6)), X6)),
% 0.20/0.45 inference(modus_ponens,[status(thm)],[162, 161])).
% 0.20/0.45 tff(164,plain,(
% 0.20/0.45 ![X6: $i, X5: $i] : p11(f12(f14(X5, X6)), X6)),
% 0.20/0.45 inference(skolemize,[status(sab)],[163])).
% 0.20/0.45 tff(165,plain,
% 0.20/0.45 (![X6: $i, X5: $i] : p11(f12(f14(X5, X6)), X6)),
% 0.20/0.45 inference(modus_ponens,[status(thm)],[164, 160])).
% 0.20/0.45 tff(166,plain,
% 0.20/0.45 ((~![X6: $i, X5: $i] : p11(f12(f14(X5, X6)), X6)) | p11(f12(f14(c23, c24)), c24)),
% 0.20/0.45 inference(quant_inst,[status(thm)],[])).
% 0.20/0.45 tff(167,plain,
% 0.20/0.45 (p11(f12(f14(c23, c24)), c24)),
% 0.20/0.45 inference(unit_resolution,[status(thm)],[166, 165])).
% 0.20/0.45 tff(168,plain,
% 0.20/0.45 (((~![X14: $i, X17: $i, X16: $i, X15: $i] : ((~p11(X15, X17)) | (~p2(X14, X16)) | p13(f15(X14, X15), f15(X16, X17)))) | ((~p11(f12(f14(c23, c24)), c24)) | (~p2(f4(f4(c22, f5(f6(c20))), c21), f4(f4(c22, f5(f6(c20))), c21))) | p13(f15(f4(f4(c22, f5(f6(c20))), c21), f12(f14(c23, c24))), f15(f4(f4(c22, f5(f6(c20))), c21), c24)))) <=> ((~![X14: $i, X17: $i, X16: $i, X15: $i] : ((~p11(X15, X17)) | (~p2(X14, X16)) | p13(f15(X14, X15), f15(X16, X17)))) | (~p11(f12(f14(c23, c24)), c24)) | (~p2(f4(f4(c22, f5(f6(c20))), c21), f4(f4(c22, f5(f6(c20))), c21))) | p13(f15(f4(f4(c22, f5(f6(c20))), c21), f12(f14(c23, c24))), f15(f4(f4(c22, f5(f6(c20))), c21), c24)))),
% 0.20/0.45 inference(rewrite,[status(thm)],[])).
% 0.20/0.45 tff(169,plain,
% 0.20/0.45 ((~![X14: $i, X17: $i, X16: $i, X15: $i] : ((~p11(X15, X17)) | (~p2(X14, X16)) | p13(f15(X14, X15), f15(X16, X17)))) | ((~p11(f12(f14(c23, c24)), c24)) | (~p2(f4(f4(c22, f5(f6(c20))), c21), f4(f4(c22, f5(f6(c20))), c21))) | p13(f15(f4(f4(c22, f5(f6(c20))), c21), f12(f14(c23, c24))), f15(f4(f4(c22, f5(f6(c20))), c21), c24)))),
% 0.20/0.45 inference(quant_inst,[status(thm)],[])).
% 0.20/0.45 tff(170,plain,
% 0.20/0.45 ((~![X14: $i, X17: $i, X16: $i, X15: $i] : ((~p11(X15, X17)) | (~p2(X14, X16)) | p13(f15(X14, X15), f15(X16, X17)))) | (~p11(f12(f14(c23, c24)), c24)) | (~p2(f4(f4(c22, f5(f6(c20))), c21), f4(f4(c22, f5(f6(c20))), c21))) | p13(f15(f4(f4(c22, f5(f6(c20))), c21), f12(f14(c23, c24))), f15(f4(f4(c22, f5(f6(c20))), c21), c24))),
% 0.20/0.45 inference(modus_ponens,[status(thm)],[169, 168])).
% 0.20/0.45 tff(171,plain,
% 0.20/0.45 (p13(f15(f4(f4(c22, f5(f6(c20))), c21), f12(f14(c23, c24))), f15(f4(f4(c22, f5(f6(c20))), c21), c24))),
% 0.20/0.45 inference(unit_resolution,[status(thm)],[170, 124, 167, 158])).
% 0.20/0.45 tff(172,plain,
% 0.20/0.45 ((~p13(f15(f4(f4(f3(c22), f5(f6(c20))), c21), f14(c23, c24)), f15(f4(f4(c22, f5(f6(c20))), c21), c24))) <=> (~p13(f15(f4(f4(f3(c22), f5(f6(c20))), c21), f14(c23, c24)), f15(f4(f4(c22, f5(f6(c20))), c21), c24)))),
% 0.20/0.45 inference(rewrite,[status(thm)],[])).
% 0.20/0.45 tff(173,axiom,(~p13(f15(f4(f4(f3(c22), f5(f6(c20))), c21), f14(c23, c24)), f15(f4(f4(c22, f5(f6(c20))), c21), c24))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','not_p13_32')).
% 0.20/0.45 tff(174,plain,
% 0.20/0.45 (~p13(f15(f4(f4(f3(c22), f5(f6(c20))), c21), f14(c23, c24)), f15(f4(f4(c22, f5(f6(c20))), c21), c24))),
% 0.20/0.45 inference(modus_ponens,[status(thm)],[173, 172])).
% 0.20/0.45 tff(175,plain,
% 0.20/0.45 (((~![X12: $i, X11: $i, X13: $i] : ((~p13(X11, X13)) | (~p13(X11, X12)) | p13(X12, X13))) | ((~p13(f15(f4(f4(c22, f5(f6(c20))), c21), f12(f14(c23, c24))), f15(f4(f4(c22, f5(f6(c20))), c21), c24))) | (~p13(f15(f4(f4(c22, f5(f6(c20))), c21), f12(f14(c23, c24))), f15(f4(f4(f3(c22), f5(f6(c20))), c21), f14(c23, c24)))) | p13(f15(f4(f4(f3(c22), f5(f6(c20))), c21), f14(c23, c24)), f15(f4(f4(c22, f5(f6(c20))), c21), c24)))) <=> ((~![X12: $i, X11: $i, X13: $i] : ((~p13(X11, X13)) | (~p13(X11, X12)) | p13(X12, X13))) | (~p13(f15(f4(f4(c22, f5(f6(c20))), c21), f12(f14(c23, c24))), f15(f4(f4(c22, f5(f6(c20))), c21), c24))) | (~p13(f15(f4(f4(c22, f5(f6(c20))), c21), f12(f14(c23, c24))), f15(f4(f4(f3(c22), f5(f6(c20))), c21), f14(c23, c24)))) | p13(f15(f4(f4(f3(c22), f5(f6(c20))), c21), f14(c23, c24)), f15(f4(f4(c22, f5(f6(c20))), c21), c24)))),
% 0.20/0.45 inference(rewrite,[status(thm)],[])).
% 0.20/0.45 tff(176,plain,
% 0.20/0.45 ((~![X12: $i, X11: $i, X13: $i] : ((~p13(X11, X13)) | (~p13(X11, X12)) | p13(X12, X13))) | ((~p13(f15(f4(f4(c22, f5(f6(c20))), c21), f12(f14(c23, c24))), f15(f4(f4(c22, f5(f6(c20))), c21), c24))) | (~p13(f15(f4(f4(c22, f5(f6(c20))), c21), f12(f14(c23, c24))), f15(f4(f4(f3(c22), f5(f6(c20))), c21), f14(c23, c24)))) | p13(f15(f4(f4(f3(c22), f5(f6(c20))), c21), f14(c23, c24)), f15(f4(f4(c22, f5(f6(c20))), c21), c24)))),
% 0.20/0.45 inference(quant_inst,[status(thm)],[])).
% 0.20/0.45 tff(177,plain,
% 0.20/0.45 ((~![X12: $i, X11: $i, X13: $i] : ((~p13(X11, X13)) | (~p13(X11, X12)) | p13(X12, X13))) | (~p13(f15(f4(f4(c22, f5(f6(c20))), c21), f12(f14(c23, c24))), f15(f4(f4(c22, f5(f6(c20))), c21), c24))) | (~p13(f15(f4(f4(c22, f5(f6(c20))), c21), f12(f14(c23, c24))), f15(f4(f4(f3(c22), f5(f6(c20))), c21), f14(c23, c24)))) | p13(f15(f4(f4(f3(c22), f5(f6(c20))), c21), f14(c23, c24)), f15(f4(f4(c22, f5(f6(c20))), c21), c24))),
% 0.20/0.45 inference(modus_ponens,[status(thm)],[176, 175])).
% 0.20/0.45 tff(178,plain,
% 0.20/0.45 ($false),
% 0.20/0.45 inference(unit_resolution,[status(thm)],[177, 147, 174, 171, 154])).
% 0.20/0.45 % SZS output end Proof
% 0.20/0.45 % E exiting
%------------------------------------------------------------------------------