%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : SYN638-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:44 AM UTC 2025
% Result : Unsatisfiable 0.19s 0.38s
% Output : Proof 0.19s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : SYN638-1 : TPTP v9.0.0. Released v2.5.0.
% 0.11/0.12 % Command : run_E %s %d THM
% 0.11/0.33 % Computer : n009.cluster.edu
% 0.11/0.33 % Model : x86_64 x86_64
% 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.33 % Memory : 8042.1875MB
% 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.33 % CPULimit : 300
% 0.11/0.33 % WCLimit : 300
% 0.11/0.33 % DateTime : Fri Jun 20 12:39:18 EDT 2025
% 0.11/0.33 % CPUTime :
% 0.19/0.38 % SZS status Unsatisfiable
% 0.19/0.38 % SZS output start Proof
% 0.19/0.38 tff(p4_type, type, (
% 0.19/0.38 p4: ( $i * $i ) > $o)).
% 0.19/0.38 tff(f16_type, type, (
% 0.19/0.38 f16: $i > $i)).
% 0.19/0.38 tff(f17_type, type, (
% 0.19/0.38 f17: ( $i * $i ) > $i)).
% 0.19/0.38 tff(f5_type, type, (
% 0.19/0.38 f5: ( $i * $i * $i ) > $i)).
% 0.19/0.38 tff(c27_type, type, (
% 0.19/0.38 c27: $i)).
% 0.19/0.38 tff(c26_type, type, (
% 0.19/0.38 c26: $i)).
% 0.19/0.38 tff(c25_type, type, (
% 0.19/0.38 c25: $i)).
% 0.19/0.38 tff(c29_type, type, (
% 0.19/0.38 c29: $i)).
% 0.19/0.38 tff(f8_type, type, (
% 0.19/0.38 f8: ( $i * $i ) > $i)).
% 0.19/0.38 tff(f9_type, type, (
% 0.19/0.38 f9: ( $i * $i ) > $i)).
% 0.19/0.38 tff(c28_type, type, (
% 0.19/0.38 c28: $i)).
% 0.19/0.38 tff(f10_type, type, (
% 0.19/0.38 f10: $i > $i)).
% 0.19/0.38 tff(f11_type, type, (
% 0.19/0.38 f11: $i > $i)).
% 0.19/0.38 tff(p22_type, type, (
% 0.19/0.38 p22: ( $i * $i ) > $o)).
% 0.19/0.38 tff(1,assumption,(~p4(f17(c27, f5(c25, c26, c27)), f17(c27, f5(c25, c26, c27)))), introduced(assumption)).
% 0.19/0.38 tff(2,plain,
% 0.19/0.38 (^[X36: $i] : refl(p4(X36, X36) <=> p4(X36, X36))),
% 0.19/0.38 inference(bind,[status(th)],[])).
% 0.19/0.38 tff(3,plain,
% 0.19/0.38 (![X36: $i] : p4(X36, X36) <=> ![X36: $i] : p4(X36, X36)),
% 0.19/0.38 inference(quant_intro,[status(thm)],[2])).
% 0.19/0.38 tff(4,plain,
% 0.19/0.38 (![X36: $i] : p4(X36, X36) <=> ![X36: $i] : p4(X36, X36)),
% 0.19/0.38 inference(rewrite,[status(thm)],[])).
% 0.19/0.38 tff(5,axiom,(![X36: $i] : p4(X36, X36)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','p4_4')).
% 0.19/0.38 tff(6,plain,
% 0.19/0.38 (![X36: $i] : p4(X36, X36)),
% 0.19/0.38 inference(modus_ponens,[status(thm)],[5, 4])).
% 0.19/0.38 tff(7,plain,(
% 0.19/0.38 ![X36: $i] : p4(X36, X36)),
% 0.19/0.38 inference(skolemize,[status(sab)],[6])).
% 0.19/0.38 tff(8,plain,
% 0.19/0.38 (![X36: $i] : p4(X36, X36)),
% 0.19/0.38 inference(modus_ponens,[status(thm)],[7, 3])).
% 0.19/0.38 tff(9,plain,
% 0.19/0.38 ((~![X36: $i] : p4(X36, X36)) | p4(f17(c27, f5(c25, c26, c27)), f17(c27, f5(c25, c26, c27)))),
% 0.19/0.38 inference(quant_inst,[status(thm)],[])).
% 0.19/0.38 tff(10,plain,
% 0.19/0.38 ($false),
% 0.19/0.38 inference(unit_resolution,[status(thm)],[9, 8, 1])).
% 0.19/0.38 tff(11,plain,(p4(f17(c27, f5(c25, c26, c27)), f17(c27, f5(c25, c26, c27)))), inference(lemma,lemma(discharge,[]))).
% 0.19/0.38 tff(12,plain,
% 0.19/0.38 (^[X39: $i, X40: $i] : refl(((~p4(X39, X40)) | p4(f16(X39), f16(X40))) <=> ((~p4(X39, X40)) | p4(f16(X39), f16(X40))))),
% 0.19/0.38 inference(bind,[status(th)],[])).
% 0.19/0.38 tff(13,plain,
% 0.19/0.38 (![X39: $i, X40: $i] : ((~p4(X39, X40)) | p4(f16(X39), f16(X40))) <=> ![X39: $i, X40: $i] : ((~p4(X39, X40)) | p4(f16(X39), f16(X40)))),
% 0.19/0.38 inference(quant_intro,[status(thm)],[12])).
% 0.19/0.38 tff(14,plain,
% 0.19/0.38 (![X39: $i, X40: $i] : ((~p4(X39, X40)) | p4(f16(X39), f16(X40))) <=> ![X39: $i, X40: $i] : ((~p4(X39, X40)) | p4(f16(X39), f16(X40)))),
% 0.19/0.38 inference(rewrite,[status(thm)],[])).
% 0.19/0.38 tff(15,plain,
% 0.19/0.38 (^[X39: $i, X40: $i] : rewrite((p4(f16(X39), f16(X40)) | (~p4(X39, X40))) <=> ((~p4(X39, X40)) | p4(f16(X39), f16(X40))))),
% 0.19/0.38 inference(bind,[status(th)],[])).
% 0.19/0.38 tff(16,plain,
% 0.19/0.38 (![X39: $i, X40: $i] : (p4(f16(X39), f16(X40)) | (~p4(X39, X40))) <=> ![X39: $i, X40: $i] : ((~p4(X39, X40)) | p4(f16(X39), f16(X40)))),
% 0.19/0.38 inference(quant_intro,[status(thm)],[15])).
% 0.19/0.38 tff(17,axiom,(![X39: $i, X40: $i] : (p4(f16(X39), f16(X40)) | (~p4(X39, X40)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','p4_12')).
% 0.19/0.38 tff(18,plain,
% 0.19/0.38 (![X39: $i, X40: $i] : ((~p4(X39, X40)) | p4(f16(X39), f16(X40)))),
% 0.19/0.38 inference(modus_ponens,[status(thm)],[17, 16])).
% 0.19/0.38 tff(19,plain,
% 0.19/0.38 (![X39: $i, X40: $i] : ((~p4(X39, X40)) | p4(f16(X39), f16(X40)))),
% 0.19/0.38 inference(modus_ponens,[status(thm)],[18, 14])).
% 0.19/0.38 tff(20,plain,(
% 0.19/0.38 ![X39: $i, X40: $i] : ((~p4(X39, X40)) | p4(f16(X39), f16(X40)))),
% 0.19/0.38 inference(skolemize,[status(sab)],[19])).
% 0.19/0.38 tff(21,plain,
% 0.19/0.38 (![X39: $i, X40: $i] : ((~p4(X39, X40)) | p4(f16(X39), f16(X40)))),
% 0.19/0.38 inference(modus_ponens,[status(thm)],[20, 13])).
% 0.19/0.38 tff(22,plain,
% 0.19/0.38 (((~![X39: $i, X40: $i] : ((~p4(X39, X40)) | p4(f16(X39), f16(X40)))) | ((~p4(f17(c27, f5(c25, c26, c27)), f17(c27, f5(c25, c26, c27)))) | p4(f16(f17(c27, f5(c25, c26, c27))), f16(f17(c27, f5(c25, c26, c27)))))) <=> ((~![X39: $i, X40: $i] : ((~p4(X39, X40)) | p4(f16(X39), f16(X40)))) | (~p4(f17(c27, f5(c25, c26, c27)), f17(c27, f5(c25, c26, c27)))) | p4(f16(f17(c27, f5(c25, c26, c27))), f16(f17(c27, f5(c25, c26, c27)))))),
% 0.19/0.38 inference(rewrite,[status(thm)],[])).
% 0.19/0.38 tff(23,plain,
% 0.19/0.38 ((~![X39: $i, X40: $i] : ((~p4(X39, X40)) | p4(f16(X39), f16(X40)))) | ((~p4(f17(c27, f5(c25, c26, c27)), f17(c27, f5(c25, c26, c27)))) | p4(f16(f17(c27, f5(c25, c26, c27))), f16(f17(c27, f5(c25, c26, c27)))))),
% 0.19/0.38 inference(quant_inst,[status(thm)],[])).
% 0.19/0.38 tff(24,plain,
% 0.19/0.38 ((~![X39: $i, X40: $i] : ((~p4(X39, X40)) | p4(f16(X39), f16(X40)))) | (~p4(f17(c27, f5(c25, c26, c27)), f17(c27, f5(c25, c26, c27)))) | p4(f16(f17(c27, f5(c25, c26, c27))), f16(f17(c27, f5(c25, c26, c27))))),
% 0.19/0.38 inference(modus_ponens,[status(thm)],[23, 22])).
% 0.19/0.38 tff(25,plain,
% 0.19/0.38 ((~p4(f17(c27, f5(c25, c26, c27)), f17(c27, f5(c25, c26, c27)))) | p4(f16(f17(c27, f5(c25, c26, c27))), f16(f17(c27, f5(c25, c26, c27))))),
% 0.19/0.38 inference(unit_resolution,[status(thm)],[24, 21])).
% 0.19/0.38 tff(26,plain,
% 0.19/0.38 (p4(f16(f17(c27, f5(c25, c26, c27))), f16(f17(c27, f5(c25, c26, c27))))),
% 0.19/0.38 inference(unit_resolution,[status(thm)],[25, 11])).
% 0.19/0.38 tff(27,assumption,(~p4(c27, c27)), introduced(assumption)).
% 0.19/0.38 tff(28,plain,
% 0.19/0.38 ((~![X36: $i] : p4(X36, X36)) | p4(c27, c27)),
% 0.19/0.38 inference(quant_inst,[status(thm)],[])).
% 0.19/0.38 tff(29,plain,
% 0.19/0.38 ($false),
% 0.19/0.38 inference(unit_resolution,[status(thm)],[28, 8, 27])).
% 0.19/0.38 tff(30,plain,(p4(c27, c27)), inference(lemma,lemma(discharge,[]))).
% 0.19/0.38 tff(31,plain,
% 0.19/0.38 (^[X51: $i] : refl(p4(f5(f8(f11(c25), f9(f10(c25), c28)), X51, c27), f5(f8(f11(c25), f9(f10(c25), c28)), X51, c29)) <=> p4(f5(f8(f11(c25), f9(f10(c25), c28)), X51, c27), f5(f8(f11(c25), f9(f10(c25), c28)), X51, c29)))),
% 0.19/0.38 inference(bind,[status(th)],[])).
% 0.19/0.38 tff(32,plain,
% 0.19/0.38 (![X51: $i] : p4(f5(f8(f11(c25), f9(f10(c25), c28)), X51, c27), f5(f8(f11(c25), f9(f10(c25), c28)), X51, c29)) <=> ![X51: $i] : p4(f5(f8(f11(c25), f9(f10(c25), c28)), X51, c27), f5(f8(f11(c25), f9(f10(c25), c28)), X51, c29))),
% 0.19/0.38 inference(quant_intro,[status(thm)],[31])).
% 0.19/0.38 tff(33,plain,
% 0.19/0.38 (![X51: $i] : p4(f5(f8(f11(c25), f9(f10(c25), c28)), X51, c27), f5(f8(f11(c25), f9(f10(c25), c28)), X51, c29)) <=> ![X51: $i] : p4(f5(f8(f11(c25), f9(f10(c25), c28)), X51, c27), f5(f8(f11(c25), f9(f10(c25), c28)), X51, c29))),
% 0.19/0.38 inference(rewrite,[status(thm)],[])).
% 0.19/0.38 tff(34,axiom,(![X51: $i] : p4(f5(f8(f11(c25), f9(f10(c25), c28)), X51, c27), f5(f8(f11(c25), f9(f10(c25), c28)), X51, c29))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','p4_39')).
% 0.19/0.38 tff(35,plain,
% 0.19/0.38 (![X51: $i] : p4(f5(f8(f11(c25), f9(f10(c25), c28)), X51, c27), f5(f8(f11(c25), f9(f10(c25), c28)), X51, c29))),
% 0.19/0.38 inference(modus_ponens,[status(thm)],[34, 33])).
% 0.19/0.38 tff(36,plain,(
% 0.19/0.38 ![X51: $i] : p4(f5(f8(f11(c25), f9(f10(c25), c28)), X51, c27), f5(f8(f11(c25), f9(f10(c25), c28)), X51, c29))),
% 0.19/0.38 inference(skolemize,[status(sab)],[35])).
% 0.19/0.38 tff(37,plain,
% 0.19/0.38 (![X51: $i] : p4(f5(f8(f11(c25), f9(f10(c25), c28)), X51, c27), f5(f8(f11(c25), f9(f10(c25), c28)), X51, c29))),
% 0.19/0.38 inference(modus_ponens,[status(thm)],[36, 32])).
% 0.19/0.38 tff(38,plain,
% 0.19/0.38 ((~![X51: $i] : p4(f5(f8(f11(c25), f9(f10(c25), c28)), X51, c27), f5(f8(f11(c25), f9(f10(c25), c28)), X51, c29))) | p4(f5(f8(f11(c25), f9(f10(c25), c28)), c26, c27), f5(f8(f11(c25), f9(f10(c25), c28)), c26, c29))),
% 0.19/0.38 inference(quant_inst,[status(thm)],[])).
% 0.19/0.38 tff(39,plain,
% 0.19/0.38 (p4(f5(f8(f11(c25), f9(f10(c25), c28)), c26, c27), f5(f8(f11(c25), f9(f10(c25), c28)), c26, c29))),
% 0.19/0.38 inference(unit_resolution,[status(thm)],[38, 37])).
% 0.19/0.38 tff(40,plain,
% 0.19/0.38 (^[X43: $i, X42: $i, X44: $i, X41: $i] : refl(((~p4(X42, X44)) | (~p4(X41, X43)) | p4(f17(X41, X42), f17(X43, X44))) <=> ((~p4(X42, X44)) | (~p4(X41, X43)) | p4(f17(X41, X42), f17(X43, X44))))),
% 0.19/0.38 inference(bind,[status(th)],[])).
% 0.19/0.38 tff(41,plain,
% 0.19/0.38 (![X43: $i, X42: $i, X44: $i, X41: $i] : ((~p4(X42, X44)) | (~p4(X41, X43)) | p4(f17(X41, X42), f17(X43, X44))) <=> ![X43: $i, X42: $i, X44: $i, X41: $i] : ((~p4(X42, X44)) | (~p4(X41, X43)) | p4(f17(X41, X42), f17(X43, X44)))),
% 0.19/0.38 inference(quant_intro,[status(thm)],[40])).
% 0.19/0.38 tff(42,plain,
% 0.19/0.38 (![X43: $i, X42: $i, X44: $i, X41: $i] : ((~p4(X42, X44)) | (~p4(X41, X43)) | p4(f17(X41, X42), f17(X43, X44))) <=> ![X43: $i, X42: $i, X44: $i, X41: $i] : ((~p4(X42, X44)) | (~p4(X41, X43)) | p4(f17(X41, X42), f17(X43, X44)))),
% 0.19/0.38 inference(rewrite,[status(thm)],[])).
% 0.19/0.38 tff(43,plain,
% 0.19/0.38 (^[X43: $i, X42: $i, X44: $i, X41: $i] : trans(monotonicity(rewrite((p4(f17(X41, X42), f17(X43, X44)) | (~p4(X41, X43))) <=> ((~p4(X41, X43)) | p4(f17(X41, X42), f17(X43, X44)))), (((p4(f17(X41, X42), f17(X43, X44)) | (~p4(X41, X43))) | (~p4(X42, X44))) <=> (((~p4(X41, X43)) | p4(f17(X41, X42), f17(X43, X44))) | (~p4(X42, X44))))), rewrite((((~p4(X41, X43)) | p4(f17(X41, X42), f17(X43, X44))) | (~p4(X42, X44))) <=> ((~p4(X42, X44)) | (~p4(X41, X43)) | p4(f17(X41, X42), f17(X43, X44)))), (((p4(f17(X41, X42), f17(X43, X44)) | (~p4(X41, X43))) | (~p4(X42, X44))) <=> ((~p4(X42, X44)) | (~p4(X41, X43)) | p4(f17(X41, X42), f17(X43, X44)))))),
% 0.19/0.38 inference(bind,[status(th)],[])).
% 0.19/0.38 tff(44,plain,
% 0.19/0.38 (![X43: $i, X42: $i, X44: $i, X41: $i] : ((p4(f17(X41, X42), f17(X43, X44)) | (~p4(X41, X43))) | (~p4(X42, X44))) <=> ![X43: $i, X42: $i, X44: $i, X41: $i] : ((~p4(X42, X44)) | (~p4(X41, X43)) | p4(f17(X41, X42), f17(X43, X44)))),
% 0.19/0.38 inference(quant_intro,[status(thm)],[43])).
% 0.19/0.38 tff(45,axiom,(![X43: $i, X42: $i, X44: $i, X41: $i] : ((p4(f17(X41, X42), f17(X43, X44)) | (~p4(X41, X43))) | (~p4(X42, X44)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','p4_32')).
% 0.19/0.38 tff(46,plain,
% 0.19/0.38 (![X43: $i, X42: $i, X44: $i, X41: $i] : ((~p4(X42, X44)) | (~p4(X41, X43)) | p4(f17(X41, X42), f17(X43, X44)))),
% 0.19/0.38 inference(modus_ponens,[status(thm)],[45, 44])).
% 0.19/0.38 tff(47,plain,
% 0.19/0.38 (![X43: $i, X42: $i, X44: $i, X41: $i] : ((~p4(X42, X44)) | (~p4(X41, X43)) | p4(f17(X41, X42), f17(X43, X44)))),
% 0.19/0.38 inference(modus_ponens,[status(thm)],[46, 42])).
% 0.19/0.38 tff(48,plain,(
% 0.19/0.38 ![X43: $i, X42: $i, X44: $i, X41: $i] : ((~p4(X42, X44)) | (~p4(X41, X43)) | p4(f17(X41, X42), f17(X43, X44)))),
% 0.19/0.38 inference(skolemize,[status(sab)],[47])).
% 0.19/0.38 tff(49,plain,
% 0.19/0.38 (![X43: $i, X42: $i, X44: $i, X41: $i] : ((~p4(X42, X44)) | (~p4(X41, X43)) | p4(f17(X41, X42), f17(X43, X44)))),
% 0.19/0.38 inference(modus_ponens,[status(thm)],[48, 41])).
% 0.19/0.38 tff(50,plain,
% 0.19/0.38 (((~![X43: $i, X42: $i, X44: $i, X41: $i] : ((~p4(X42, X44)) | (~p4(X41, X43)) | p4(f17(X41, X42), f17(X43, X44)))) | (p4(f17(c27, f5(f8(f11(c25), f9(f10(c25), c28)), c26, c27)), f17(c27, f5(f8(f11(c25), f9(f10(c25), c28)), c26, c29))) | (~p4(c27, c27)) | (~p4(f5(f8(f11(c25), f9(f10(c25), c28)), c26, c27), f5(f8(f11(c25), f9(f10(c25), c28)), c26, c29))))) <=> ((~![X43: $i, X42: $i, X44: $i, X41: $i] : ((~p4(X42, X44)) | (~p4(X41, X43)) | p4(f17(X41, X42), f17(X43, X44)))) | p4(f17(c27, f5(f8(f11(c25), f9(f10(c25), c28)), c26, c27)), f17(c27, f5(f8(f11(c25), f9(f10(c25), c28)), c26, c29))) | (~p4(c27, c27)) | (~p4(f5(f8(f11(c25), f9(f10(c25), c28)), c26, c27), f5(f8(f11(c25), f9(f10(c25), c28)), c26, c29))))),
% 0.19/0.38 inference(rewrite,[status(thm)],[])).
% 0.19/0.38 tff(51,plain,
% 0.19/0.38 (((~p4(f5(f8(f11(c25), f9(f10(c25), c28)), c26, c27), f5(f8(f11(c25), f9(f10(c25), c28)), c26, c29))) | (~p4(c27, c27)) | p4(f17(c27, f5(f8(f11(c25), f9(f10(c25), c28)), c26, c27)), f17(c27, f5(f8(f11(c25), f9(f10(c25), c28)), c26, c29)))) <=> (p4(f17(c27, f5(f8(f11(c25), f9(f10(c25), c28)), c26, c27)), f17(c27, f5(f8(f11(c25), f9(f10(c25), c28)), c26, c29))) | (~p4(c27, c27)) | (~p4(f5(f8(f11(c25), f9(f10(c25), c28)), c26, c27), f5(f8(f11(c25), f9(f10(c25), c28)), c26, c29))))),
% 0.19/0.38 inference(rewrite,[status(thm)],[])).
% 0.19/0.38 tff(52,plain,
% 0.19/0.38 (((~![X43: $i, X42: $i, X44: $i, X41: $i] : ((~p4(X42, X44)) | (~p4(X41, X43)) | p4(f17(X41, X42), f17(X43, X44)))) | ((~p4(f5(f8(f11(c25), f9(f10(c25), c28)), c26, c27), f5(f8(f11(c25), f9(f10(c25), c28)), c26, c29))) | (~p4(c27, c27)) | p4(f17(c27, f5(f8(f11(c25), f9(f10(c25), c28)), c26, c27)), f17(c27, f5(f8(f11(c25), f9(f10(c25), c28)), c26, c29))))) <=> ((~![X43: $i, X42: $i, X44: $i, X41: $i] : ((~p4(X42, X44)) | (~p4(X41, X43)) | p4(f17(X41, X42), f17(X43, X44)))) | (p4(f17(c27, f5(f8(f11(c25), f9(f10(c25), c28)), c26, c27)), f17(c27, f5(f8(f11(c25), f9(f10(c25), c28)), c26, c29))) | (~p4(c27, c27)) | (~p4(f5(f8(f11(c25), f9(f10(c25), c28)), c26, c27), f5(f8(f11(c25), f9(f10(c25), c28)), c26, c29)))))),
% 0.19/0.38 inference(monotonicity,[status(thm)],[51])).
% 0.19/0.38 tff(53,plain,
% 0.19/0.38 (((~![X43: $i, X42: $i, X44: $i, X41: $i] : ((~p4(X42, X44)) | (~p4(X41, X43)) | p4(f17(X41, X42), f17(X43, X44)))) | ((~p4(f5(f8(f11(c25), f9(f10(c25), c28)), c26, c27), f5(f8(f11(c25), f9(f10(c25), c28)), c26, c29))) | (~p4(c27, c27)) | p4(f17(c27, f5(f8(f11(c25), f9(f10(c25), c28)), c26, c27)), f17(c27, f5(f8(f11(c25), f9(f10(c25), c28)), c26, c29))))) <=> ((~![X43: $i, X42: $i, X44: $i, X41: $i] : ((~p4(X42, X44)) | (~p4(X41, X43)) | p4(f17(X41, X42), f17(X43, X44)))) | p4(f17(c27, f5(f8(f11(c25), f9(f10(c25), c28)), c26, c27)), f17(c27, f5(f8(f11(c25), f9(f10(c25), c28)), c26, c29))) | (~p4(c27, c27)) | (~p4(f5(f8(f11(c25), f9(f10(c25), c28)), c26, c27), f5(f8(f11(c25), f9(f10(c25), c28)), c26, c29))))),
% 0.19/0.39 inference(transitivity,[status(thm)],[52, 50])).
% 0.19/0.39 tff(54,plain,
% 0.19/0.39 ((~![X43: $i, X42: $i, X44: $i, X41: $i] : ((~p4(X42, X44)) | (~p4(X41, X43)) | p4(f17(X41, X42), f17(X43, X44)))) | ((~p4(f5(f8(f11(c25), f9(f10(c25), c28)), c26, c27), f5(f8(f11(c25), f9(f10(c25), c28)), c26, c29))) | (~p4(c27, c27)) | p4(f17(c27, f5(f8(f11(c25), f9(f10(c25), c28)), c26, c27)), f17(c27, f5(f8(f11(c25), f9(f10(c25), c28)), c26, c29))))),
% 0.19/0.39 inference(quant_inst,[status(thm)],[])).
% 0.19/0.39 tff(55,plain,
% 0.19/0.39 ((~![X43: $i, X42: $i, X44: $i, X41: $i] : ((~p4(X42, X44)) | (~p4(X41, X43)) | p4(f17(X41, X42), f17(X43, X44)))) | p4(f17(c27, f5(f8(f11(c25), f9(f10(c25), c28)), c26, c27)), f17(c27, f5(f8(f11(c25), f9(f10(c25), c28)), c26, c29))) | (~p4(c27, c27)) | (~p4(f5(f8(f11(c25), f9(f10(c25), c28)), c26, c27), f5(f8(f11(c25), f9(f10(c25), c28)), c26, c29)))),
% 0.19/0.39 inference(modus_ponens,[status(thm)],[54, 53])).
% 0.19/0.39 tff(56,plain,
% 0.19/0.39 (p4(f17(c27, f5(f8(f11(c25), f9(f10(c25), c28)), c26, c27)), f17(c27, f5(f8(f11(c25), f9(f10(c25), c28)), c26, c29))) | (~p4(c27, c27)) | (~p4(f5(f8(f11(c25), f9(f10(c25), c28)), c26, c27), f5(f8(f11(c25), f9(f10(c25), c28)), c26, c29)))),
% 0.19/0.39 inference(unit_resolution,[status(thm)],[55, 49])).
% 0.19/0.39 tff(57,plain,
% 0.19/0.39 (p4(f17(c27, f5(f8(f11(c25), f9(f10(c25), c28)), c26, c27)), f17(c27, f5(f8(f11(c25), f9(f10(c25), c28)), c26, c29))) | (~p4(c27, c27))),
% 0.19/0.39 inference(unit_resolution,[status(thm)],[56, 39])).
% 0.19/0.39 tff(58,plain,
% 0.19/0.39 (p4(f17(c27, f5(f8(f11(c25), f9(f10(c25), c28)), c26, c27)), f17(c27, f5(f8(f11(c25), f9(f10(c25), c28)), c26, c29)))),
% 0.19/0.39 inference(unit_resolution,[status(thm)],[57, 30])).
% 0.19/0.39 tff(59,plain,
% 0.19/0.39 (((~![X39: $i, X40: $i] : ((~p4(X39, X40)) | p4(f16(X39), f16(X40)))) | ((~p4(f17(c27, f5(f8(f11(c25), f9(f10(c25), c28)), c26, c27)), f17(c27, f5(f8(f11(c25), f9(f10(c25), c28)), c26, c29)))) | p4(f16(f17(c27, f5(f8(f11(c25), f9(f10(c25), c28)), c26, c27))), f16(f17(c27, f5(f8(f11(c25), f9(f10(c25), c28)), c26, c29)))))) <=> ((~![X39: $i, X40: $i] : ((~p4(X39, X40)) | p4(f16(X39), f16(X40)))) | (~p4(f17(c27, f5(f8(f11(c25), f9(f10(c25), c28)), c26, c27)), f17(c27, f5(f8(f11(c25), f9(f10(c25), c28)), c26, c29)))) | p4(f16(f17(c27, f5(f8(f11(c25), f9(f10(c25), c28)), c26, c27))), f16(f17(c27, f5(f8(f11(c25), f9(f10(c25), c28)), c26, c29)))))),
% 0.19/0.39 inference(rewrite,[status(thm)],[])).
% 0.19/0.39 tff(60,plain,
% 0.19/0.39 ((~![X39: $i, X40: $i] : ((~p4(X39, X40)) | p4(f16(X39), f16(X40)))) | ((~p4(f17(c27, f5(f8(f11(c25), f9(f10(c25), c28)), c26, c27)), f17(c27, f5(f8(f11(c25), f9(f10(c25), c28)), c26, c29)))) | p4(f16(f17(c27, f5(f8(f11(c25), f9(f10(c25), c28)), c26, c27))), f16(f17(c27, f5(f8(f11(c25), f9(f10(c25), c28)), c26, c29)))))),
% 0.19/0.39 inference(quant_inst,[status(thm)],[])).
% 0.19/0.39 tff(61,plain,
% 0.19/0.39 ((~![X39: $i, X40: $i] : ((~p4(X39, X40)) | p4(f16(X39), f16(X40)))) | (~p4(f17(c27, f5(f8(f11(c25), f9(f10(c25), c28)), c26, c27)), f17(c27, f5(f8(f11(c25), f9(f10(c25), c28)), c26, c29)))) | p4(f16(f17(c27, f5(f8(f11(c25), f9(f10(c25), c28)), c26, c27))), f16(f17(c27, f5(f8(f11(c25), f9(f10(c25), c28)), c26, c29))))),
% 0.19/0.39 inference(modus_ponens,[status(thm)],[60, 59])).
% 0.19/0.39 tff(62,plain,
% 0.19/0.39 ((~p4(f17(c27, f5(f8(f11(c25), f9(f10(c25), c28)), c26, c27)), f17(c27, f5(f8(f11(c25), f9(f10(c25), c28)), c26, c29)))) | p4(f16(f17(c27, f5(f8(f11(c25), f9(f10(c25), c28)), c26, c27))), f16(f17(c27, f5(f8(f11(c25), f9(f10(c25), c28)), c26, c29))))),
% 0.19/0.39 inference(unit_resolution,[status(thm)],[61, 21])).
% 0.19/0.39 tff(63,plain,
% 0.19/0.39 (p4(f16(f17(c27, f5(f8(f11(c25), f9(f10(c25), c28)), c26, c27))), f16(f17(c27, f5(f8(f11(c25), f9(f10(c25), c28)), c26, c29))))),
% 0.19/0.39 inference(unit_resolution,[status(thm)],[62, 58])).
% 0.19/0.39 tff(64,plain,
% 0.19/0.39 ((~p22(f16(f17(c27, f5(f8(f11(c25), f9(f10(c25), c28)), c26, c29))), f16(f17(c27, f5(c25, c26, c27))))) <=> (~p22(f16(f17(c27, f5(f8(f11(c25), f9(f10(c25), c28)), c26, c29))), f16(f17(c27, f5(c25, c26, c27)))))),
% 0.19/0.39 inference(rewrite,[status(thm)],[])).
% 0.19/0.39 tff(65,axiom,(~p22(f16(f17(c27, f5(f8(f11(c25), f9(f10(c25), c28)), c26, c29))), f16(f17(c27, f5(c25, c26, c27))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','not_p22_41')).
% 0.19/0.39 tff(66,plain,
% 0.19/0.39 (~p22(f16(f17(c27, f5(f8(f11(c25), f9(f10(c25), c28)), c26, c29))), f16(f17(c27, f5(c25, c26, c27))))),
% 0.19/0.39 inference(modus_ponens,[status(thm)],[65, 64])).
% 0.19/0.39 tff(67,plain,
% 0.19/0.39 (p22(f16(f17(c27, f5(f8(f11(c25), f9(f10(c25), c28)), c26, c27))), f16(f17(c27, f5(c25, c26, c27)))) <=> p22(f16(f17(c27, f5(f8(f11(c25), f9(f10(c25), c28)), c26, c27))), f16(f17(c27, f5(c25, c26, c27))))),
% 0.19/0.39 inference(rewrite,[status(thm)],[])).
% 0.19/0.39 tff(68,axiom,(p22(f16(f17(c27, f5(f8(f11(c25), f9(f10(c25), c28)), c26, c27))), f16(f17(c27, f5(c25, c26, c27))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','p22_40')).
% 0.19/0.39 tff(69,plain,
% 0.19/0.39 (p22(f16(f17(c27, f5(f8(f11(c25), f9(f10(c25), c28)), c26, c27))), f16(f17(c27, f5(c25, c26, c27))))),
% 0.19/0.39 inference(modus_ponens,[status(thm)],[68, 67])).
% 0.19/0.39 tff(70,plain,
% 0.19/0.39 (^[X22: $i, X21: $i, X20: $i, X23: $i] : refl(((~p4(X23, X21)) | (~p22(X22, X23)) | (~p4(X22, X20)) | p22(X20, X21)) <=> ((~p4(X23, X21)) | (~p22(X22, X23)) | (~p4(X22, X20)) | p22(X20, X21)))),
% 0.19/0.39 inference(bind,[status(th)],[])).
% 0.19/0.39 tff(71,plain,
% 0.19/0.39 (![X22: $i, X21: $i, X20: $i, X23: $i] : ((~p4(X23, X21)) | (~p22(X22, X23)) | (~p4(X22, X20)) | p22(X20, X21)) <=> ![X22: $i, X21: $i, X20: $i, X23: $i] : ((~p4(X23, X21)) | (~p22(X22, X23)) | (~p4(X22, X20)) | p22(X20, X21))),
% 0.19/0.39 inference(quant_intro,[status(thm)],[70])).
% 0.19/0.39 tff(72,plain,
% 0.19/0.39 (![X22: $i, X21: $i, X20: $i, X23: $i] : ((~p4(X23, X21)) | (~p22(X22, X23)) | (~p4(X22, X20)) | p22(X20, X21)) <=> ![X22: $i, X21: $i, X20: $i, X23: $i] : ((~p4(X23, X21)) | (~p22(X22, X23)) | (~p4(X22, X20)) | p22(X20, X21))),
% 0.19/0.39 inference(rewrite,[status(thm)],[])).
% 0.19/0.39 tff(73,plain,
% 0.19/0.39 (^[X22: $i, X21: $i, X20: $i, X23: $i] : trans(monotonicity(trans(monotonicity(rewrite((p22(X20, X21) | (~p4(X22, X20))) <=> ((~p4(X22, X20)) | p22(X20, X21))), (((p22(X20, X21) | (~p4(X22, X20))) | (~p4(X23, X21))) <=> (((~p4(X22, X20)) | p22(X20, X21)) | (~p4(X23, X21))))), rewrite((((~p4(X22, X20)) | p22(X20, X21)) | (~p4(X23, X21))) <=> ((~p4(X23, X21)) | (~p4(X22, X20)) | p22(X20, X21))), (((p22(X20, X21) | (~p4(X22, X20))) | (~p4(X23, X21))) <=> ((~p4(X23, X21)) | (~p4(X22, X20)) | p22(X20, X21)))), ((((p22(X20, X21) | (~p4(X22, X20))) | (~p4(X23, X21))) | (~p22(X22, X23))) <=> (((~p4(X23, X21)) | (~p4(X22, X20)) | p22(X20, X21)) | (~p22(X22, X23))))), rewrite((((~p4(X23, X21)) | (~p4(X22, X20)) | p22(X20, X21)) | (~p22(X22, X23))) <=> ((~p4(X23, X21)) | (~p22(X22, X23)) | (~p4(X22, X20)) | p22(X20, X21))), ((((p22(X20, X21) | (~p4(X22, X20))) | (~p4(X23, X21))) | (~p22(X22, X23))) <=> ((~p4(X23, X21)) | (~p22(X22, X23)) | (~p4(X22, X20)) | p22(X20, X21))))),
% 0.19/0.39 inference(bind,[status(th)],[])).
% 0.19/0.39 tff(74,plain,
% 0.19/0.39 (![X22: $i, X21: $i, X20: $i, X23: $i] : (((p22(X20, X21) | (~p4(X22, X20))) | (~p4(X23, X21))) | (~p22(X22, X23))) <=> ![X22: $i, X21: $i, X20: $i, X23: $i] : ((~p4(X23, X21)) | (~p22(X22, X23)) | (~p4(X22, X20)) | p22(X20, X21))),
% 0.19/0.39 inference(quant_intro,[status(thm)],[73])).
% 0.19/0.39 tff(75,axiom,(![X22: $i, X21: $i, X20: $i, X23: $i] : (((p22(X20, X21) | (~p4(X22, X20))) | (~p4(X23, X21))) | (~p22(X22, X23)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','p22_28')).
% 0.19/0.39 tff(76,plain,
% 0.19/0.39 (![X22: $i, X21: $i, X20: $i, X23: $i] : ((~p4(X23, X21)) | (~p22(X22, X23)) | (~p4(X22, X20)) | p22(X20, X21))),
% 0.19/0.39 inference(modus_ponens,[status(thm)],[75, 74])).
% 0.19/0.39 tff(77,plain,
% 0.19/0.39 (![X22: $i, X21: $i, X20: $i, X23: $i] : ((~p4(X23, X21)) | (~p22(X22, X23)) | (~p4(X22, X20)) | p22(X20, X21))),
% 0.19/0.40 inference(modus_ponens,[status(thm)],[76, 72])).
% 0.19/0.40 tff(78,plain,(
% 0.19/0.40 ![X22: $i, X21: $i, X20: $i, X23: $i] : ((~p4(X23, X21)) | (~p22(X22, X23)) | (~p4(X22, X20)) | p22(X20, X21))),
% 0.19/0.40 inference(skolemize,[status(sab)],[77])).
% 0.19/0.40 tff(79,plain,
% 0.19/0.40 (![X22: $i, X21: $i, X20: $i, X23: $i] : ((~p4(X23, X21)) | (~p22(X22, X23)) | (~p4(X22, X20)) | p22(X20, X21))),
% 0.19/0.40 inference(modus_ponens,[status(thm)],[78, 71])).
% 0.19/0.40 tff(80,plain,
% 0.19/0.40 (((~![X22: $i, X21: $i, X20: $i, X23: $i] : ((~p4(X23, X21)) | (~p22(X22, X23)) | (~p4(X22, X20)) | p22(X20, X21))) | ((~p4(f16(f17(c27, f5(c25, c26, c27))), f16(f17(c27, f5(c25, c26, c27))))) | (~p22(f16(f17(c27, f5(f8(f11(c25), f9(f10(c25), c28)), c26, c27))), f16(f17(c27, f5(c25, c26, c27))))) | (~p4(f16(f17(c27, f5(f8(f11(c25), f9(f10(c25), c28)), c26, c27))), f16(f17(c27, f5(f8(f11(c25), f9(f10(c25), c28)), c26, c29))))) | p22(f16(f17(c27, f5(f8(f11(c25), f9(f10(c25), c28)), c26, c29))), f16(f17(c27, f5(c25, c26, c27)))))) <=> ((~![X22: $i, X21: $i, X20: $i, X23: $i] : ((~p4(X23, X21)) | (~p22(X22, X23)) | (~p4(X22, X20)) | p22(X20, X21))) | (~p4(f16(f17(c27, f5(c25, c26, c27))), f16(f17(c27, f5(c25, c26, c27))))) | (~p22(f16(f17(c27, f5(f8(f11(c25), f9(f10(c25), c28)), c26, c27))), f16(f17(c27, f5(c25, c26, c27))))) | (~p4(f16(f17(c27, f5(f8(f11(c25), f9(f10(c25), c28)), c26, c27))), f16(f17(c27, f5(f8(f11(c25), f9(f10(c25), c28)), c26, c29))))) | p22(f16(f17(c27, f5(f8(f11(c25), f9(f10(c25), c28)), c26, c29))), f16(f17(c27, f5(c25, c26, c27)))))),
% 0.19/0.40 inference(rewrite,[status(thm)],[])).
% 0.19/0.40 tff(81,plain,
% 0.19/0.40 ((~![X22: $i, X21: $i, X20: $i, X23: $i] : ((~p4(X23, X21)) | (~p22(X22, X23)) | (~p4(X22, X20)) | p22(X20, X21))) | ((~p4(f16(f17(c27, f5(c25, c26, c27))), f16(f17(c27, f5(c25, c26, c27))))) | (~p22(f16(f17(c27, f5(f8(f11(c25), f9(f10(c25), c28)), c26, c27))), f16(f17(c27, f5(c25, c26, c27))))) | (~p4(f16(f17(c27, f5(f8(f11(c25), f9(f10(c25), c28)), c26, c27))), f16(f17(c27, f5(f8(f11(c25), f9(f10(c25), c28)), c26, c29))))) | p22(f16(f17(c27, f5(f8(f11(c25), f9(f10(c25), c28)), c26, c29))), f16(f17(c27, f5(c25, c26, c27)))))),
% 0.19/0.40 inference(quant_inst,[status(thm)],[])).
% 0.19/0.40 tff(82,plain,
% 0.19/0.40 ((~![X22: $i, X21: $i, X20: $i, X23: $i] : ((~p4(X23, X21)) | (~p22(X22, X23)) | (~p4(X22, X20)) | p22(X20, X21))) | (~p4(f16(f17(c27, f5(c25, c26, c27))), f16(f17(c27, f5(c25, c26, c27))))) | (~p22(f16(f17(c27, f5(f8(f11(c25), f9(f10(c25), c28)), c26, c27))), f16(f17(c27, f5(c25, c26, c27))))) | (~p4(f16(f17(c27, f5(f8(f11(c25), f9(f10(c25), c28)), c26, c27))), f16(f17(c27, f5(f8(f11(c25), f9(f10(c25), c28)), c26, c29))))) | p22(f16(f17(c27, f5(f8(f11(c25), f9(f10(c25), c28)), c26, c29))), f16(f17(c27, f5(c25, c26, c27))))),
% 0.19/0.40 inference(modus_ponens,[status(thm)],[81, 80])).
% 0.19/0.40 tff(83,plain,
% 0.19/0.40 ($false),
% 0.19/0.40 inference(unit_resolution,[status(thm)],[82, 79, 69, 66, 63, 26])).
% 0.19/0.40 % SZS output end Proof
% 0.19/0.40 % E exiting
%------------------------------------------------------------------------------