%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : SYN719-1 : TPTP v9.0.0. Released v2.5.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n003.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:54 AM UTC 2025
% Result : Unsatisfiable 0.38s 0.57s
% Output : Proof 0.38s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SYN719-1 : TPTP v9.0.0. Released v2.5.0.
% 0.07/0.12 % Command : run_E %s %d THM
% 0.12/0.34 % Computer : n003.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Fri Jun 20 12:40:54 EDT 2025
% 0.12/0.34 % CPUTime :
% 0.38/0.57 % SZS status Unsatisfiable
% 0.38/0.57 % SZS output start Proof
% 0.38/0.57 tff(p70_type, type, (
% 0.38/0.57 p70: ( $i * $i ) > $o)).
% 0.38/0.57 tff(f38_type, type, (
% 0.38/0.57 f38: ( $i * $i ) > $i)).
% 0.38/0.57 tff(f40_type, type, (
% 0.38/0.57 f40: ( $i * $i ) > $i)).
% 0.38/0.57 tff(c81_type, type, (
% 0.38/0.57 c81: $i)).
% 0.38/0.57 tff(f42_type, type, (
% 0.38/0.57 f42: ( $i * $i ) > $i)).
% 0.38/0.57 tff(c85_type, type, (
% 0.38/0.57 c85: $i)).
% 0.38/0.57 tff(f44_type, type, (
% 0.38/0.57 f44: ( $i * $i ) > $i)).
% 0.38/0.57 tff(f46_type, type, (
% 0.38/0.57 f46: ( $i * $i ) > $i)).
% 0.38/0.57 tff(c79_type, type, (
% 0.38/0.57 c79: $i)).
% 0.38/0.57 tff(c87_type, type, (
% 0.38/0.57 c87: $i)).
% 0.38/0.57 tff(f30_type, type, (
% 0.38/0.57 f30: ( $i * $i ) > $i)).
% 0.38/0.57 tff(f32_type, type, (
% 0.38/0.57 f32: ( $i * $i ) > $i)).
% 0.38/0.57 tff(f8_type, type, (
% 0.38/0.57 f8: ( $i * $i ) > $i)).
% 0.38/0.57 tff(c76_type, type, (
% 0.38/0.57 c76: $i)).
% 0.38/0.57 tff(c75_type, type, (
% 0.38/0.57 c75: $i)).
% 0.38/0.57 tff(c89_type, type, (
% 0.38/0.57 c89: $i)).
% 0.38/0.57 tff(c88_type, type, (
% 0.38/0.57 c88: $i)).
% 0.38/0.57 tff(p69_type, type, (
% 0.38/0.57 p69: ( $i * $i ) > $o)).
% 0.38/0.57 tff(f36_type, type, (
% 0.38/0.57 f36: ( $i * $i ) > $i)).
% 0.38/0.57 tff(c86_type, type, (
% 0.38/0.57 c86: $i)).
% 0.38/0.57 tff(p14_type, type, (
% 0.38/0.57 p14: ( $i * $i ) > $o)).
% 0.38/0.57 tff(f23_type, type, (
% 0.38/0.57 f23: ( $i * $i ) > $i)).
% 0.38/0.57 tff(f26_type, type, (
% 0.38/0.57 f26: ( $i * $i ) > $i)).
% 0.38/0.57 tff(c84_type, type, (
% 0.38/0.57 c84: $i)).
% 0.38/0.57 tff(p68_type, type, (
% 0.38/0.57 p68: ( $i * $i ) > $o)).
% 0.38/0.57 tff(f19_type, type, (
% 0.38/0.57 f19: ( $i * $i ) > $i)).
% 0.38/0.57 tff(f21_type, type, (
% 0.38/0.57 f21: ( $i * $i ) > $i)).
% 0.38/0.57 tff(c77_type, type, (
% 0.38/0.57 c77: $i)).
% 0.38/0.57 tff(c83_type, type, (
% 0.38/0.57 c83: $i)).
% 0.38/0.57 tff(p67_type, type, (
% 0.38/0.57 p67: ( $i * $i ) > $o)).
% 0.38/0.57 tff(c82_type, type, (
% 0.38/0.57 c82: $i)).
% 0.38/0.57 tff(f16_type, type, (
% 0.38/0.57 f16: ( $i * $i ) > $i)).
% 0.38/0.57 tff(c80_type, type, (
% 0.38/0.57 c80: $i)).
% 0.38/0.57 tff(p66_type, type, (
% 0.38/0.57 p66: ( $i * $i ) > $o)).
% 0.38/0.57 tff(f12_type, type, (
% 0.38/0.57 f12: ( $i * $i ) > $i)).
% 0.38/0.57 tff(c78_type, type, (
% 0.38/0.57 c78: $i)).
% 0.38/0.57 tff(1,assumption,(~p14(f23(f26(c84, c85), c81), f23(f26(c84, c85), c81))), introduced(assumption)).
% 0.38/0.57 tff(2,plain,
% 0.38/0.57 (^[X13: $i] : refl(p14(X13, X13) <=> p14(X13, X13))),
% 0.38/0.57 inference(bind,[status(th)],[])).
% 0.38/0.57 tff(3,plain,
% 0.38/0.57 (![X13: $i] : p14(X13, X13) <=> ![X13: $i] : p14(X13, X13)),
% 0.38/0.57 inference(quant_intro,[status(thm)],[2])).
% 0.38/0.57 tff(4,plain,
% 0.38/0.57 (![X13: $i] : p14(X13, X13) <=> ![X13: $i] : p14(X13, X13)),
% 0.38/0.57 inference(rewrite,[status(thm)],[])).
% 0.38/0.57 tff(5,axiom,(![X13: $i] : p14(X13, X13)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','p14_38')).
% 0.38/0.57 tff(6,plain,
% 0.38/0.57 (![X13: $i] : p14(X13, X13)),
% 0.38/0.57 inference(modus_ponens,[status(thm)],[5, 4])).
% 0.38/0.57 tff(7,plain,(
% 0.38/0.57 ![X13: $i] : p14(X13, X13)),
% 0.38/0.57 inference(skolemize,[status(sab)],[6])).
% 0.38/0.57 tff(8,plain,
% 0.38/0.57 (![X13: $i] : p14(X13, X13)),
% 0.38/0.57 inference(modus_ponens,[status(thm)],[7, 3])).
% 0.38/0.57 tff(9,plain,
% 0.38/0.57 ((~![X13: $i] : p14(X13, X13)) | p14(f23(f26(c84, c85), c81), f23(f26(c84, c85), c81))),
% 0.38/0.57 inference(quant_inst,[status(thm)],[])).
% 0.38/0.57 tff(10,plain,
% 0.38/0.57 ($false),
% 0.38/0.57 inference(unit_resolution,[status(thm)],[9, 8, 1])).
% 0.38/0.57 tff(11,plain,(p14(f23(f26(c84, c85), c81), f23(f26(c84, c85), c81))), inference(lemma,lemma(discharge,[]))).
% 0.38/0.57 tff(12,plain,
% 0.38/0.57 (^[X20: $i] : refl(p14(f23(f26(c84, c85), X20), X20) <=> p14(f23(f26(c84, c85), X20), X20))),
% 0.38/0.57 inference(bind,[status(th)],[])).
% 0.38/0.57 tff(13,plain,
% 0.38/0.57 (![X20: $i] : p14(f23(f26(c84, c85), X20), X20) <=> ![X20: $i] : p14(f23(f26(c84, c85), X20), X20)),
% 0.38/0.57 inference(quant_intro,[status(thm)],[12])).
% 0.38/0.57 tff(14,plain,
% 0.38/0.57 (![X20: $i] : p14(f23(f26(c84, c85), X20), X20) <=> ![X20: $i] : p14(f23(f26(c84, c85), X20), X20)),
% 0.38/0.57 inference(rewrite,[status(thm)],[])).
% 0.38/0.57 tff(15,axiom,(![X20: $i] : p14(f23(f26(c84, c85), X20), X20)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','p14_45')).
% 0.38/0.57 tff(16,plain,
% 0.38/0.57 (![X20: $i] : p14(f23(f26(c84, c85), X20), X20)),
% 0.38/0.57 inference(modus_ponens,[status(thm)],[15, 14])).
% 0.38/0.57 tff(17,plain,(
% 0.38/0.57 ![X20: $i] : p14(f23(f26(c84, c85), X20), X20)),
% 0.38/0.57 inference(skolemize,[status(sab)],[16])).
% 0.38/0.57 tff(18,plain,
% 0.38/0.57 (![X20: $i] : p14(f23(f26(c84, c85), X20), X20)),
% 0.38/0.57 inference(modus_ponens,[status(thm)],[17, 13])).
% 0.38/0.57 tff(19,plain,
% 0.38/0.57 ((~![X20: $i] : p14(f23(f26(c84, c85), X20), X20)) | p14(f23(f26(c84, c85), c81), c81)),
% 0.38/0.57 inference(quant_inst,[status(thm)],[])).
% 0.38/0.57 tff(20,plain,
% 0.38/0.57 (p14(f23(f26(c84, c85), c81), c81)),
% 0.38/0.57 inference(unit_resolution,[status(thm)],[19, 18])).
% 0.38/0.57 tff(21,plain,
% 0.38/0.57 (^[X14: $i, X13: $i, X15: $i] : refl(((~p14(X13, X15)) | (~p14(X13, X14)) | p14(X14, X15)) <=> ((~p14(X13, X15)) | (~p14(X13, X14)) | p14(X14, X15)))),
% 0.38/0.57 inference(bind,[status(th)],[])).
% 0.38/0.57 tff(22,plain,
% 0.38/0.57 (![X14: $i, X13: $i, X15: $i] : ((~p14(X13, X15)) | (~p14(X13, X14)) | p14(X14, X15)) <=> ![X14: $i, X13: $i, X15: $i] : ((~p14(X13, X15)) | (~p14(X13, X14)) | p14(X14, X15))),
% 0.38/0.57 inference(quant_intro,[status(thm)],[21])).
% 0.38/0.57 tff(23,plain,
% 0.38/0.57 (![X14: $i, X13: $i, X15: $i] : ((~p14(X13, X15)) | (~p14(X13, X14)) | p14(X14, X15)) <=> ![X14: $i, X13: $i, X15: $i] : ((~p14(X13, X15)) | (~p14(X13, X14)) | p14(X14, X15))),
% 0.38/0.57 inference(rewrite,[status(thm)],[])).
% 0.38/0.57 tff(24,plain,
% 0.38/0.57 (^[X14: $i, X13: $i, X15: $i] : trans(monotonicity(rewrite((p14(X14, X15) | (~p14(X13, X14))) <=> ((~p14(X13, X14)) | p14(X14, X15))), (((p14(X14, X15) | (~p14(X13, X14))) | (~p14(X13, X15))) <=> (((~p14(X13, X14)) | p14(X14, X15)) | (~p14(X13, X15))))), rewrite((((~p14(X13, X14)) | p14(X14, X15)) | (~p14(X13, X15))) <=> ((~p14(X13, X15)) | (~p14(X13, X14)) | p14(X14, X15))), (((p14(X14, X15) | (~p14(X13, X14))) | (~p14(X13, X15))) <=> ((~p14(X13, X15)) | (~p14(X13, X14)) | p14(X14, X15))))),
% 0.38/0.57 inference(bind,[status(th)],[])).
% 0.38/0.57 tff(25,plain,
% 0.38/0.57 (![X14: $i, X13: $i, X15: $i] : ((p14(X14, X15) | (~p14(X13, X14))) | (~p14(X13, X15))) <=> ![X14: $i, X13: $i, X15: $i] : ((~p14(X13, X15)) | (~p14(X13, X14)) | p14(X14, X15))),
% 0.38/0.57 inference(quant_intro,[status(thm)],[24])).
% 0.38/0.57 tff(26,axiom,(![X14: $i, X13: $i, X15: $i] : ((p14(X14, X15) | (~p14(X13, X14))) | (~p14(X13, X15)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','p14_90')).
% 0.38/0.57 tff(27,plain,
% 0.38/0.57 (![X14: $i, X13: $i, X15: $i] : ((~p14(X13, X15)) | (~p14(X13, X14)) | p14(X14, X15))),
% 0.38/0.57 inference(modus_ponens,[status(thm)],[26, 25])).
% 0.38/0.57 tff(28,plain,
% 0.38/0.57 (![X14: $i, X13: $i, X15: $i] : ((~p14(X13, X15)) | (~p14(X13, X14)) | p14(X14, X15))),
% 0.38/0.57 inference(modus_ponens,[status(thm)],[27, 23])).
% 0.38/0.57 tff(29,plain,(
% 0.38/0.57 ![X14: $i, X13: $i, X15: $i] : ((~p14(X13, X15)) | (~p14(X13, X14)) | p14(X14, X15))),
% 0.38/0.57 inference(skolemize,[status(sab)],[28])).
% 0.38/0.57 tff(30,plain,
% 0.38/0.57 (![X14: $i, X13: $i, X15: $i] : ((~p14(X13, X15)) | (~p14(X13, X14)) | p14(X14, X15))),
% 0.38/0.57 inference(modus_ponens,[status(thm)],[29, 22])).
% 0.38/0.57 tff(31,plain,
% 0.38/0.57 (((~![X14: $i, X13: $i, X15: $i] : ((~p14(X13, X15)) | (~p14(X13, X14)) | p14(X14, X15))) | ((~p14(f23(f26(c84, c85), c81), f23(f26(c84, c85), c81))) | (~p14(f23(f26(c84, c85), c81), c81)) | p14(c81, f23(f26(c84, c85), c81)))) <=> ((~![X14: $i, X13: $i, X15: $i] : ((~p14(X13, X15)) | (~p14(X13, X14)) | p14(X14, X15))) | (~p14(f23(f26(c84, c85), c81), f23(f26(c84, c85), c81))) | (~p14(f23(f26(c84, c85), c81), c81)) | p14(c81, f23(f26(c84, c85), c81)))),
% 0.38/0.57 inference(rewrite,[status(thm)],[])).
% 0.38/0.57 tff(32,plain,
% 0.38/0.57 ((~![X14: $i, X13: $i, X15: $i] : ((~p14(X13, X15)) | (~p14(X13, X14)) | p14(X14, X15))) | ((~p14(f23(f26(c84, c85), c81), f23(f26(c84, c85), c81))) | (~p14(f23(f26(c84, c85), c81), c81)) | p14(c81, f23(f26(c84, c85), c81)))),
% 0.38/0.57 inference(quant_inst,[status(thm)],[])).
% 0.38/0.57 tff(33,plain,
% 0.38/0.57 ((~![X14: $i, X13: $i, X15: $i] : ((~p14(X13, X15)) | (~p14(X13, X14)) | p14(X14, X15))) | (~p14(f23(f26(c84, c85), c81), f23(f26(c84, c85), c81))) | (~p14(f23(f26(c84, c85), c81), c81)) | p14(c81, f23(f26(c84, c85), c81))),
% 0.38/0.57 inference(modus_ponens,[status(thm)],[32, 31])).
% 0.38/0.57 tff(34,plain,
% 0.38/0.57 (p14(c81, f23(f26(c84, c85), c81))),
% 0.38/0.57 inference(unit_resolution,[status(thm)],[33, 30, 20, 11])).
% 0.38/0.57 tff(35,plain,
% 0.38/0.57 (^[X222: $i, X224: $i, X221: $i, X223: $i] : refl(((~p69(f36(c86, f38(X223, f40(f42(f44(f46(c87, X221), X222), X223), X224))), f30(c88, f32(c89, f8(c75, c76))))) | (~p14(X222, f23(f26(c84, X223), X224))) | (~p66(f12(c78, c77), X221)) | (~p67(f16(c80, X224), c82)) | p68(f19(f21(c83, c77), X221), X222)) <=> ((~p69(f36(c86, f38(X223, f40(f42(f44(f46(c87, X221), X222), X223), X224))), f30(c88, f32(c89, f8(c75, c76))))) | (~p14(X222, f23(f26(c84, X223), X224))) | (~p66(f12(c78, c77), X221)) | (~p67(f16(c80, X224), c82)) | p68(f19(f21(c83, c77), X221), X222)))),
% 0.38/0.57 inference(bind,[status(th)],[])).
% 0.38/0.57 tff(36,plain,
% 0.38/0.57 (![X222: $i, X224: $i, X221: $i, X223: $i] : ((~p69(f36(c86, f38(X223, f40(f42(f44(f46(c87, X221), X222), X223), X224))), f30(c88, f32(c89, f8(c75, c76))))) | (~p14(X222, f23(f26(c84, X223), X224))) | (~p66(f12(c78, c77), X221)) | (~p67(f16(c80, X224), c82)) | p68(f19(f21(c83, c77), X221), X222)) <=> ![X222: $i, X224: $i, X221: $i, X223: $i] : ((~p69(f36(c86, f38(X223, f40(f42(f44(f46(c87, X221), X222), X223), X224))), f30(c88, f32(c89, f8(c75, c76))))) | (~p14(X222, f23(f26(c84, X223), X224))) | (~p66(f12(c78, c77), X221)) | (~p67(f16(c80, X224), c82)) | p68(f19(f21(c83, c77), X221), X222))),
% 0.38/0.57 inference(quant_intro,[status(thm)],[35])).
% 0.38/0.57 tff(37,plain,
% 0.38/0.57 (![X222: $i, X224: $i, X221: $i, X223: $i] : ((~p69(f36(c86, f38(X223, f40(f42(f44(f46(c87, X221), X222), X223), X224))), f30(c88, f32(c89, f8(c75, c76))))) | (~p14(X222, f23(f26(c84, X223), X224))) | (~p66(f12(c78, c77), X221)) | (~p67(f16(c80, X224), c82)) | p68(f19(f21(c83, c77), X221), X222)) <=> ![X222: $i, X224: $i, X221: $i, X223: $i] : ((~p69(f36(c86, f38(X223, f40(f42(f44(f46(c87, X221), X222), X223), X224))), f30(c88, f32(c89, f8(c75, c76))))) | (~p14(X222, f23(f26(c84, X223), X224))) | (~p66(f12(c78, c77), X221)) | (~p67(f16(c80, X224), c82)) | p68(f19(f21(c83, c77), X221), X222))),
% 0.38/0.57 inference(rewrite,[status(thm)],[])).
% 0.38/0.57 tff(38,plain,
% 0.38/0.57 (^[X222: $i, X224: $i, X221: $i, X223: $i] : trans(monotonicity(trans(monotonicity(trans(monotonicity(rewrite((p68(f19(f21(c83, c77), X221), X222) | (~p67(f16(c80, X224), c82))) <=> ((~p67(f16(c80, X224), c82)) | p68(f19(f21(c83, c77), X221), X222))), (((p68(f19(f21(c83, c77), X221), X222) | (~p67(f16(c80, X224), c82))) | (~p66(f12(c78, c77), X221))) <=> (((~p67(f16(c80, X224), c82)) | p68(f19(f21(c83, c77), X221), X222)) | (~p66(f12(c78, c77), X221))))), rewrite((((~p67(f16(c80, X224), c82)) | p68(f19(f21(c83, c77), X221), X222)) | (~p66(f12(c78, c77), X221))) <=> ((~p66(f12(c78, c77), X221)) | (~p67(f16(c80, X224), c82)) | p68(f19(f21(c83, c77), X221), X222))), (((p68(f19(f21(c83, c77), X221), X222) | (~p67(f16(c80, X224), c82))) | (~p66(f12(c78, c77), X221))) <=> ((~p66(f12(c78, c77), X221)) | (~p67(f16(c80, X224), c82)) | p68(f19(f21(c83, c77), X221), X222)))), ((((p68(f19(f21(c83, c77), X221), X222) | (~p67(f16(c80, X224), c82))) | (~p66(f12(c78, c77), X221))) | (~p14(X222, f23(f26(c84, X223), X224)))) <=> (((~p66(f12(c78, c77), X221)) | (~p67(f16(c80, X224), c82)) | p68(f19(f21(c83, c77), X221), X222)) | (~p14(X222, f23(f26(c84, X223), X224)))))), rewrite((((~p66(f12(c78, c77), X221)) | (~p67(f16(c80, X224), c82)) | p68(f19(f21(c83, c77), X221), X222)) | (~p14(X222, f23(f26(c84, X223), X224)))) <=> ((~p14(X222, f23(f26(c84, X223), X224))) | (~p66(f12(c78, c77), X221)) | (~p67(f16(c80, X224), c82)) | p68(f19(f21(c83, c77), X221), X222))), ((((p68(f19(f21(c83, c77), X221), X222) | (~p67(f16(c80, X224), c82))) | (~p66(f12(c78, c77), X221))) | (~p14(X222, f23(f26(c84, X223), X224)))) <=> ((~p14(X222, f23(f26(c84, X223), X224))) | (~p66(f12(c78, c77), X221)) | (~p67(f16(c80, X224), c82)) | p68(f19(f21(c83, c77), X221), X222)))), (((((p68(f19(f21(c83, c77), X221), X222) | (~p67(f16(c80, X224), c82))) | (~p66(f12(c78, c77), X221))) | (~p14(X222, f23(f26(c84, X223), X224)))) | (~p69(f36(c86, f38(X223, f40(f42(f44(f46(c87, X221), X222), X223), X224))), f30(c88, f32(c89, f8(c75, c76)))))) <=> (((~p14(X222, f23(f26(c84, X223), X224))) | (~p66(f12(c78, c77), X221)) | (~p67(f16(c80, X224), c82)) | p68(f19(f21(c83, c77), X221), X222)) | (~p69(f36(c86, f38(X223, f40(f42(f44(f46(c87, X221), X222), X223), X224))), f30(c88, f32(c89, f8(c75, c76)))))))), rewrite((((~p14(X222, f23(f26(c84, X223), X224))) | (~p66(f12(c78, c77), X221)) | (~p67(f16(c80, X224), c82)) | p68(f19(f21(c83, c77), X221), X222)) | (~p69(f36(c86, f38(X223, f40(f42(f44(f46(c87, X221), X222), X223), X224))), f30(c88, f32(c89, f8(c75, c76)))))) <=> ((~p69(f36(c86, f38(X223, f40(f42(f44(f46(c87, X221), X222), X223), X224))), f30(c88, f32(c89, f8(c75, c76))))) | (~p14(X222, f23(f26(c84, X223), X224))) | (~p66(f12(c78, c77), X221)) | (~p67(f16(c80, X224), c82)) | p68(f19(f21(c83, c77), X221), X222))), (((((p68(f19(f21(c83, c77), X221), X222) | (~p67(f16(c80, X224), c82))) | (~p66(f12(c78, c77), X221))) | (~p14(X222, f23(f26(c84, X223), X224)))) | (~p69(f36(c86, f38(X223, f40(f42(f44(f46(c87, X221), X222), X223), X224))), f30(c88, f32(c89, f8(c75, c76)))))) <=> ((~p69(f36(c86, f38(X223, f40(f42(f44(f46(c87, X221), X222), X223), X224))), f30(c88, f32(c89, f8(c75, c76))))) | (~p14(X222, f23(f26(c84, X223), X224))) | (~p66(f12(c78, c77), X221)) | (~p67(f16(c80, X224), c82)) | p68(f19(f21(c83, c77), X221), X222))))),
% 0.38/0.57 inference(bind,[status(th)],[])).
% 0.38/0.57 tff(39,plain,
% 0.38/0.57 (![X222: $i, X224: $i, X221: $i, X223: $i] : ((((p68(f19(f21(c83, c77), X221), X222) | (~p67(f16(c80, X224), c82))) | (~p66(f12(c78, c77), X221))) | (~p14(X222, f23(f26(c84, X223), X224)))) | (~p69(f36(c86, f38(X223, f40(f42(f44(f46(c87, X221), X222), X223), X224))), f30(c88, f32(c89, f8(c75, c76)))))) <=> ![X222: $i, X224: $i, X221: $i, X223: $i] : ((~p69(f36(c86, f38(X223, f40(f42(f44(f46(c87, X221), X222), X223), X224))), f30(c88, f32(c89, f8(c75, c76))))) | (~p14(X222, f23(f26(c84, X223), X224))) | (~p66(f12(c78, c77), X221)) | (~p67(f16(c80, X224), c82)) | p68(f19(f21(c83, c77), X221), X222))),
% 0.38/0.57 inference(quant_intro,[status(thm)],[38])).
% 0.38/0.57 tff(40,axiom,(![X222: $i, X224: $i, X221: $i, X223: $i] : ((((p68(f19(f21(c83, c77), X221), X222) | (~p67(f16(c80, X224), c82))) | (~p66(f12(c78, c77), X221))) | (~p14(X222, f23(f26(c84, X223), X224)))) | (~p69(f36(c86, f38(X223, f40(f42(f44(f46(c87, X221), X222), X223), X224))), f30(c88, f32(c89, f8(c75, c76))))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','p68_126')).
% 0.38/0.57 tff(41,plain,
% 0.38/0.57 (![X222: $i, X224: $i, X221: $i, X223: $i] : ((~p69(f36(c86, f38(X223, f40(f42(f44(f46(c87, X221), X222), X223), X224))), f30(c88, f32(c89, f8(c75, c76))))) | (~p14(X222, f23(f26(c84, X223), X224))) | (~p66(f12(c78, c77), X221)) | (~p67(f16(c80, X224), c82)) | p68(f19(f21(c83, c77), X221), X222))),
% 0.38/0.57 inference(modus_ponens,[status(thm)],[40, 39])).
% 0.38/0.57 tff(42,plain,
% 0.38/0.57 (![X222: $i, X224: $i, X221: $i, X223: $i] : ((~p69(f36(c86, f38(X223, f40(f42(f44(f46(c87, X221), X222), X223), X224))), f30(c88, f32(c89, f8(c75, c76))))) | (~p14(X222, f23(f26(c84, X223), X224))) | (~p66(f12(c78, c77), X221)) | (~p67(f16(c80, X224), c82)) | p68(f19(f21(c83, c77), X221), X222))),
% 0.38/0.57 inference(modus_ponens,[status(thm)],[41, 37])).
% 0.38/0.57 tff(43,plain,(
% 0.38/0.57 ![X222: $i, X224: $i, X221: $i, X223: $i] : ((~p69(f36(c86, f38(X223, f40(f42(f44(f46(c87, X221), X222), X223), X224))), f30(c88, f32(c89, f8(c75, c76))))) | (~p14(X222, f23(f26(c84, X223), X224))) | (~p66(f12(c78, c77), X221)) | (~p67(f16(c80, X224), c82)) | p68(f19(f21(c83, c77), X221), X222))),
% 0.38/0.57 inference(skolemize,[status(sab)],[42])).
% 0.38/0.57 tff(44,plain,
% 0.38/0.57 (![X222: $i, X224: $i, X221: $i, X223: $i] : ((~p69(f36(c86, f38(X223, f40(f42(f44(f46(c87, X221), X222), X223), X224))), f30(c88, f32(c89, f8(c75, c76))))) | (~p14(X222, f23(f26(c84, X223), X224))) | (~p66(f12(c78, c77), X221)) | (~p67(f16(c80, X224), c82)) | p68(f19(f21(c83, c77), X221), X222))),
% 0.38/0.57 inference(modus_ponens,[status(thm)],[43, 36])).
% 0.38/0.57 tff(45,plain,
% 0.38/0.57 ((~p68(f19(f21(c83, c77), c79), c81)) <=> (~p68(f19(f21(c83, c77), c79), c81))),
% 0.38/0.57 inference(rewrite,[status(thm)],[])).
% 0.38/0.57 tff(46,axiom,(~p68(f19(f21(c83, c77), c79), c81)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','not_p68_46')).
% 0.38/0.57 tff(47,plain,
% 0.38/0.57 (~p68(f19(f21(c83, c77), c79), c81)),
% 0.38/0.57 inference(modus_ponens,[status(thm)],[46, 45])).
% 0.38/0.57 tff(48,plain,
% 0.38/0.57 (p67(f16(c80, c81), c82) <=> p67(f16(c80, c81), c82)),
% 0.38/0.57 inference(rewrite,[status(thm)],[])).
% 0.38/0.57 tff(49,axiom,(p67(f16(c80, c81), c82)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','p67_42')).
% 0.38/0.57 tff(50,plain,
% 0.38/0.57 (p67(f16(c80, c81), c82)),
% 0.38/0.57 inference(modus_ponens,[status(thm)],[49, 48])).
% 0.38/0.57 tff(51,plain,
% 0.38/0.57 (p66(f12(c78, c77), c79) <=> p66(f12(c78, c77), c79)),
% 0.38/0.57 inference(rewrite,[status(thm)],[])).
% 0.38/0.57 tff(52,axiom,(p66(f12(c78, c77), c79)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','p66_41')).
% 0.38/0.57 tff(53,plain,
% 0.38/0.58 (p66(f12(c78, c77), c79)),
% 0.38/0.58 inference(modus_ponens,[status(thm)],[52, 51])).
% 0.38/0.58 tff(54,plain,
% 0.38/0.58 (((~![X222: $i, X224: $i, X221: $i, X223: $i] : ((~p69(f36(c86, f38(X223, f40(f42(f44(f46(c87, X221), X222), X223), X224))), f30(c88, f32(c89, f8(c75, c76))))) | (~p14(X222, f23(f26(c84, X223), X224))) | (~p66(f12(c78, c77), X221)) | (~p67(f16(c80, X224), c82)) | p68(f19(f21(c83, c77), X221), X222))) | (p68(f19(f21(c83, c77), c79), c81) | (~p67(f16(c80, c81), c82)) | (~p66(f12(c78, c77), c79)) | (~p14(c81, f23(f26(c84, c85), c81))) | (~p69(f36(c86, f38(c85, f40(f42(f44(f46(c87, c79), c81), c85), c81))), f30(c88, f32(c89, f8(c75, c76))))))) <=> ((~![X222: $i, X224: $i, X221: $i, X223: $i] : ((~p69(f36(c86, f38(X223, f40(f42(f44(f46(c87, X221), X222), X223), X224))), f30(c88, f32(c89, f8(c75, c76))))) | (~p14(X222, f23(f26(c84, X223), X224))) | (~p66(f12(c78, c77), X221)) | (~p67(f16(c80, X224), c82)) | p68(f19(f21(c83, c77), X221), X222))) | p68(f19(f21(c83, c77), c79), c81) | (~p67(f16(c80, c81), c82)) | (~p66(f12(c78, c77), c79)) | (~p14(c81, f23(f26(c84, c85), c81))) | (~p69(f36(c86, f38(c85, f40(f42(f44(f46(c87, c79), c81), c85), c81))), f30(c88, f32(c89, f8(c75, c76))))))),
% 0.38/0.58 inference(rewrite,[status(thm)],[])).
% 0.38/0.58 tff(55,plain,
% 0.38/0.58 (((~p69(f36(c86, f38(c85, f40(f42(f44(f46(c87, c79), c81), c85), c81))), f30(c88, f32(c89, f8(c75, c76))))) | (~p14(c81, f23(f26(c84, c85), c81))) | (~p66(f12(c78, c77), c79)) | (~p67(f16(c80, c81), c82)) | p68(f19(f21(c83, c77), c79), c81)) <=> (p68(f19(f21(c83, c77), c79), c81) | (~p67(f16(c80, c81), c82)) | (~p66(f12(c78, c77), c79)) | (~p14(c81, f23(f26(c84, c85), c81))) | (~p69(f36(c86, f38(c85, f40(f42(f44(f46(c87, c79), c81), c85), c81))), f30(c88, f32(c89, f8(c75, c76))))))),
% 0.38/0.58 inference(rewrite,[status(thm)],[])).
% 0.38/0.58 tff(56,plain,
% 0.38/0.58 (((~![X222: $i, X224: $i, X221: $i, X223: $i] : ((~p69(f36(c86, f38(X223, f40(f42(f44(f46(c87, X221), X222), X223), X224))), f30(c88, f32(c89, f8(c75, c76))))) | (~p14(X222, f23(f26(c84, X223), X224))) | (~p66(f12(c78, c77), X221)) | (~p67(f16(c80, X224), c82)) | p68(f19(f21(c83, c77), X221), X222))) | ((~p69(f36(c86, f38(c85, f40(f42(f44(f46(c87, c79), c81), c85), c81))), f30(c88, f32(c89, f8(c75, c76))))) | (~p14(c81, f23(f26(c84, c85), c81))) | (~p66(f12(c78, c77), c79)) | (~p67(f16(c80, c81), c82)) | p68(f19(f21(c83, c77), c79), c81))) <=> ((~![X222: $i, X224: $i, X221: $i, X223: $i] : ((~p69(f36(c86, f38(X223, f40(f42(f44(f46(c87, X221), X222), X223), X224))), f30(c88, f32(c89, f8(c75, c76))))) | (~p14(X222, f23(f26(c84, X223), X224))) | (~p66(f12(c78, c77), X221)) | (~p67(f16(c80, X224), c82)) | p68(f19(f21(c83, c77), X221), X222))) | (p68(f19(f21(c83, c77), c79), c81) | (~p67(f16(c80, c81), c82)) | (~p66(f12(c78, c77), c79)) | (~p14(c81, f23(f26(c84, c85), c81))) | (~p69(f36(c86, f38(c85, f40(f42(f44(f46(c87, c79), c81), c85), c81))), f30(c88, f32(c89, f8(c75, c76)))))))),
% 0.38/0.58 inference(monotonicity,[status(thm)],[55])).
% 0.38/0.58 tff(57,plain,
% 0.38/0.58 (((~![X222: $i, X224: $i, X221: $i, X223: $i] : ((~p69(f36(c86, f38(X223, f40(f42(f44(f46(c87, X221), X222), X223), X224))), f30(c88, f32(c89, f8(c75, c76))))) | (~p14(X222, f23(f26(c84, X223), X224))) | (~p66(f12(c78, c77), X221)) | (~p67(f16(c80, X224), c82)) | p68(f19(f21(c83, c77), X221), X222))) | ((~p69(f36(c86, f38(c85, f40(f42(f44(f46(c87, c79), c81), c85), c81))), f30(c88, f32(c89, f8(c75, c76))))) | (~p14(c81, f23(f26(c84, c85), c81))) | (~p66(f12(c78, c77), c79)) | (~p67(f16(c80, c81), c82)) | p68(f19(f21(c83, c77), c79), c81))) <=> ((~![X222: $i, X224: $i, X221: $i, X223: $i] : ((~p69(f36(c86, f38(X223, f40(f42(f44(f46(c87, X221), X222), X223), X224))), f30(c88, f32(c89, f8(c75, c76))))) | (~p14(X222, f23(f26(c84, X223), X224))) | (~p66(f12(c78, c77), X221)) | (~p67(f16(c80, X224), c82)) | p68(f19(f21(c83, c77), X221), X222))) | p68(f19(f21(c83, c77), c79), c81) | (~p67(f16(c80, c81), c82)) | (~p66(f12(c78, c77), c79)) | (~p14(c81, f23(f26(c84, c85), c81))) | (~p69(f36(c86, f38(c85, f40(f42(f44(f46(c87, c79), c81), c85), c81))), f30(c88, f32(c89, f8(c75, c76))))))),
% 0.38/0.58 inference(transitivity,[status(thm)],[56, 54])).
% 0.38/0.58 tff(58,plain,
% 0.38/0.58 ((~![X222: $i, X224: $i, X221: $i, X223: $i] : ((~p69(f36(c86, f38(X223, f40(f42(f44(f46(c87, X221), X222), X223), X224))), f30(c88, f32(c89, f8(c75, c76))))) | (~p14(X222, f23(f26(c84, X223), X224))) | (~p66(f12(c78, c77), X221)) | (~p67(f16(c80, X224), c82)) | p68(f19(f21(c83, c77), X221), X222))) | ((~p69(f36(c86, f38(c85, f40(f42(f44(f46(c87, c79), c81), c85), c81))), f30(c88, f32(c89, f8(c75, c76))))) | (~p14(c81, f23(f26(c84, c85), c81))) | (~p66(f12(c78, c77), c79)) | (~p67(f16(c80, c81), c82)) | p68(f19(f21(c83, c77), c79), c81))),
% 0.38/0.58 inference(quant_inst,[status(thm)],[])).
% 0.38/0.58 tff(59,plain,
% 0.38/0.58 ((~![X222: $i, X224: $i, X221: $i, X223: $i] : ((~p69(f36(c86, f38(X223, f40(f42(f44(f46(c87, X221), X222), X223), X224))), f30(c88, f32(c89, f8(c75, c76))))) | (~p14(X222, f23(f26(c84, X223), X224))) | (~p66(f12(c78, c77), X221)) | (~p67(f16(c80, X224), c82)) | p68(f19(f21(c83, c77), X221), X222))) | p68(f19(f21(c83, c77), c79), c81) | (~p67(f16(c80, c81), c82)) | (~p66(f12(c78, c77), c79)) | (~p14(c81, f23(f26(c84, c85), c81))) | (~p69(f36(c86, f38(c85, f40(f42(f44(f46(c87, c79), c81), c85), c81))), f30(c88, f32(c89, f8(c75, c76)))))),
% 0.38/0.58 inference(modus_ponens,[status(thm)],[58, 57])).
% 0.38/0.58 tff(60,plain,
% 0.38/0.58 (~p69(f36(c86, f38(c85, f40(f42(f44(f46(c87, c79), c81), c85), c81))), f30(c88, f32(c89, f8(c75, c76))))),
% 0.38/0.58 inference(unit_resolution,[status(thm)],[59, 53, 50, 47, 44, 34])).
% 0.38/0.58 tff(61,plain,
% 0.38/0.58 (^[X230: $i, X229: $i] : refl((p69(f36(c86, X229), X230) | (~p70(X230, X229))) <=> (p69(f36(c86, X229), X230) | (~p70(X230, X229))))),
% 0.38/0.58 inference(bind,[status(th)],[])).
% 0.38/0.58 tff(62,plain,
% 0.38/0.58 (![X230: $i, X229: $i] : (p69(f36(c86, X229), X230) | (~p70(X230, X229))) <=> ![X230: $i, X229: $i] : (p69(f36(c86, X229), X230) | (~p70(X230, X229)))),
% 0.38/0.58 inference(quant_intro,[status(thm)],[61])).
% 0.38/0.58 tff(63,plain,
% 0.38/0.58 (![X230: $i, X229: $i] : (p69(f36(c86, X229), X230) | (~p70(X230, X229))) <=> ![X230: $i, X229: $i] : (p69(f36(c86, X229), X230) | (~p70(X230, X229)))),
% 0.38/0.58 inference(rewrite,[status(thm)],[])).
% 0.38/0.58 tff(64,axiom,(![X230: $i, X229: $i] : (p69(f36(c86, X229), X230) | (~p70(X230, X229)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','p69_52')).
% 0.38/0.58 tff(65,plain,
% 0.38/0.58 (![X230: $i, X229: $i] : (p69(f36(c86, X229), X230) | (~p70(X230, X229)))),
% 0.38/0.58 inference(modus_ponens,[status(thm)],[64, 63])).
% 0.38/0.58 tff(66,plain,(
% 0.38/0.58 ![X230: $i, X229: $i] : (p69(f36(c86, X229), X230) | (~p70(X230, X229)))),
% 0.38/0.58 inference(skolemize,[status(sab)],[65])).
% 0.38/0.58 tff(67,plain,
% 0.38/0.58 (![X230: $i, X229: $i] : (p69(f36(c86, X229), X230) | (~p70(X230, X229)))),
% 0.38/0.58 inference(modus_ponens,[status(thm)],[66, 62])).
% 0.38/0.58 tff(68,plain,
% 0.38/0.58 (((~![X230: $i, X229: $i] : (p69(f36(c86, X229), X230) | (~p70(X230, X229)))) | (p69(f36(c86, f38(c85, f40(f42(f44(f46(c87, c79), c81), c85), c81))), f30(c88, f32(c89, f8(c75, c76)))) | (~p70(f30(c88, f32(c89, f8(c75, c76))), f38(c85, f40(f42(f44(f46(c87, c79), c81), c85), c81)))))) <=> ((~![X230: $i, X229: $i] : (p69(f36(c86, X229), X230) | (~p70(X230, X229)))) | p69(f36(c86, f38(c85, f40(f42(f44(f46(c87, c79), c81), c85), c81))), f30(c88, f32(c89, f8(c75, c76)))) | (~p70(f30(c88, f32(c89, f8(c75, c76))), f38(c85, f40(f42(f44(f46(c87, c79), c81), c85), c81)))))),
% 0.38/0.58 inference(rewrite,[status(thm)],[])).
% 0.38/0.58 tff(69,plain,
% 0.38/0.58 ((~![X230: $i, X229: $i] : (p69(f36(c86, X229), X230) | (~p70(X230, X229)))) | (p69(f36(c86, f38(c85, f40(f42(f44(f46(c87, c79), c81), c85), c81))), f30(c88, f32(c89, f8(c75, c76)))) | (~p70(f30(c88, f32(c89, f8(c75, c76))), f38(c85, f40(f42(f44(f46(c87, c79), c81), c85), c81)))))),
% 0.38/0.58 inference(quant_inst,[status(thm)],[])).
% 0.38/0.58 tff(70,plain,
% 0.38/0.58 ((~![X230: $i, X229: $i] : (p69(f36(c86, X229), X230) | (~p70(X230, X229)))) | p69(f36(c86, f38(c85, f40(f42(f44(f46(c87, c79), c81), c85), c81))), f30(c88, f32(c89, f8(c75, c76)))) | (~p70(f30(c88, f32(c89, f8(c75, c76))), f38(c85, f40(f42(f44(f46(c87, c79), c81), c85), c81))))),
% 0.38/0.58 inference(modus_ponens,[status(thm)],[69, 68])).
% 0.38/0.58 tff(71,plain,
% 0.38/0.58 (~p70(f30(c88, f32(c89, f8(c75, c76))), f38(c85, f40(f42(f44(f46(c87, c79), c81), c85), c81)))),
% 0.38/0.58 inference(unit_resolution,[status(thm)],[70, 67, 60])).
% 0.38/0.58 tff(72,plain,
% 0.38/0.58 (^[X242: $i, X243: $i] : refl(p70(f30(c88, X242), f38(c85, X243)) <=> p70(f30(c88, X242), f38(c85, X243)))),
% 0.38/0.58 inference(bind,[status(th)],[])).
% 0.38/0.58 tff(73,plain,
% 0.38/0.58 (![X242: $i, X243: $i] : p70(f30(c88, X242), f38(c85, X243)) <=> ![X242: $i, X243: $i] : p70(f30(c88, X242), f38(c85, X243))),
% 0.38/0.58 inference(quant_intro,[status(thm)],[72])).
% 0.38/0.58 tff(74,plain,
% 0.38/0.58 (![X242: $i, X243: $i] : p70(f30(c88, X242), f38(c85, X243)) <=> ![X242: $i, X243: $i] : p70(f30(c88, X242), f38(c85, X243))),
% 0.38/0.58 inference(rewrite,[status(thm)],[])).
% 0.38/0.58 tff(75,axiom,(![X242: $i, X243: $i] : p70(f30(c88, X242), f38(c85, X243))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','p70_43')).
% 0.38/0.58 tff(76,plain,
% 0.38/0.58 (![X242: $i, X243: $i] : p70(f30(c88, X242), f38(c85, X243))),
% 0.38/0.58 inference(modus_ponens,[status(thm)],[75, 74])).
% 0.38/0.58 tff(77,plain,(
% 0.38/0.58 ![X242: $i, X243: $i] : p70(f30(c88, X242), f38(c85, X243))),
% 0.38/0.58 inference(skolemize,[status(sab)],[76])).
% 0.38/0.58 tff(78,plain,
% 0.38/0.58 (![X242: $i, X243: $i] : p70(f30(c88, X242), f38(c85, X243))),
% 0.38/0.58 inference(modus_ponens,[status(thm)],[77, 73])).
% 0.38/0.58 tff(79,plain,
% 0.38/0.58 ((~![X242: $i, X243: $i] : p70(f30(c88, X242), f38(c85, X243))) | p70(f30(c88, f32(c89, f8(c75, c76))), f38(c85, f40(f42(f44(f46(c87, c79), c81), c85), c81)))),
% 0.38/0.58 inference(quant_inst,[status(thm)],[])).
% 0.38/0.58 tff(80,plain,
% 0.38/0.58 ($false),
% 0.38/0.58 inference(unit_resolution,[status(thm)],[79, 78, 71])).
% 0.38/0.58 % SZS output end Proof
% 0.38/0.59 % E exiting
%------------------------------------------------------------------------------