%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : SYN644-1 : TPTP v9.0.0. Released v2.5.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n011.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:45 AM UTC 2025
% Result : Unsatisfiable 0.71s 0.90s
% Output : Proof 0.71s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : SYN644-1 : TPTP v9.0.0. Released v2.5.0.
% 0.04/0.13 % Command : run_E %s %d THM
% 0.12/0.34 % Computer : n011.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:39:41 EDT 2025
% 0.12/0.34 % CPUTime :
% 0.71/0.90 % SZS status Unsatisfiable
% 0.71/0.90 % SZS output start Proof
% 0.71/0.90 tff(p25_type, type, (
% 0.71/0.90 p25: ( $i * $i ) > $o)).
% 0.71/0.90 tff(f13_type, type, (
% 0.71/0.90 f13: $i > $i)).
% 0.71/0.90 tff(f14_type, type, (
% 0.71/0.90 f14: ( $i * $i ) > $i)).
% 0.71/0.90 tff(f21_type, type, (
% 0.71/0.90 f21: ( $i * $i * $i * $i * $i ) > $i)).
% 0.71/0.90 tff(c28_type, type, (
% 0.71/0.90 c28: $i)).
% 0.71/0.90 tff(c31_type, type, (
% 0.71/0.90 c31: $i)).
% 0.71/0.90 tff(c30_type, type, (
% 0.71/0.90 c30: $i)).
% 0.71/0.90 tff(c27_type, type, (
% 0.71/0.90 c27: $i)).
% 0.71/0.90 tff(c29_type, type, (
% 0.71/0.90 c29: $i)).
% 0.71/0.90 tff(f16_type, type, (
% 0.71/0.90 f16: ( $i * $i * $i ) > $i)).
% 0.71/0.90 tff(c32_type, type, (
% 0.71/0.90 c32: $i)).
% 0.71/0.90 tff(f10_type, type, (
% 0.71/0.90 f10: ( $i * $i ) > $i)).
% 0.71/0.90 tff(f11_type, type, (
% 0.71/0.90 f11: ( $i * $i ) > $i)).
% 0.71/0.90 tff(p23_type, type, (
% 0.71/0.90 p23: ( $i * $i ) > $o)).
% 0.71/0.90 tff(f8_type, type, (
% 0.71/0.90 f8: $i > $i)).
% 0.71/0.90 tff(p12_type, type, (
% 0.71/0.90 p12: ( $i * $i ) > $o)).
% 0.71/0.90 tff(p24_type, type, (
% 0.71/0.90 p24: $i > $o)).
% 0.71/0.90 tff(f17_type, type, (
% 0.71/0.90 f17: ( $i * $i ) > $i)).
% 0.71/0.90 tff(p22_type, type, (
% 0.71/0.90 p22: ( $i * $i ) > $o)).
% 0.71/0.90 tff(f3_type, type, (
% 0.71/0.90 f3: $i > $i)).
% 0.71/0.90 tff(f4_type, type, (
% 0.71/0.90 f4: $i > $i)).
% 0.71/0.90 tff(f5_type, type, (
% 0.71/0.90 f5: $i > $i)).
% 0.71/0.90 tff(c26_type, type, (
% 0.71/0.90 c26: $i)).
% 0.71/0.90 tff(p2_type, type, (
% 0.71/0.90 p2: ( $i * $i ) > $o)).
% 0.71/0.90 tff(1,plain,
% 0.71/0.90 (^[X6: $i, X4: $i, X3: $i, X7: $i, X5: $i] : refl(((~p22(f3(f4(f5(c26))), X5)) | (~p23(X3, f8(f10(X4, f11(X5, X6))))) | (~p24(f17(f10(X4, f11(X5, X6)), X3))) | p23(f21(X4, X5, X6, X7, X3), f8(f10(X4, f11(X5, X6)))) | p12(X3, f16(f10(X4, f11(X5, X6)), c32, X7))) <=> ((~p22(f3(f4(f5(c26))), X5)) | (~p23(X3, f8(f10(X4, f11(X5, X6))))) | (~p24(f17(f10(X4, f11(X5, X6)), X3))) | p23(f21(X4, X5, X6, X7, X3), f8(f10(X4, f11(X5, X6)))) | p12(X3, f16(f10(X4, f11(X5, X6)), c32, X7))))),
% 0.71/0.90 inference(bind,[status(th)],[])).
% 0.71/0.90 tff(2,plain,
% 0.71/0.90 (![X6: $i, X4: $i, X3: $i, X7: $i, X5: $i] : ((~p22(f3(f4(f5(c26))), X5)) | (~p23(X3, f8(f10(X4, f11(X5, X6))))) | (~p24(f17(f10(X4, f11(X5, X6)), X3))) | p23(f21(X4, X5, X6, X7, X3), f8(f10(X4, f11(X5, X6)))) | p12(X3, f16(f10(X4, f11(X5, X6)), c32, X7))) <=> ![X6: $i, X4: $i, X3: $i, X7: $i, X5: $i] : ((~p22(f3(f4(f5(c26))), X5)) | (~p23(X3, f8(f10(X4, f11(X5, X6))))) | (~p24(f17(f10(X4, f11(X5, X6)), X3))) | p23(f21(X4, X5, X6, X7, X3), f8(f10(X4, f11(X5, X6)))) | p12(X3, f16(f10(X4, f11(X5, X6)), c32, X7)))),
% 0.71/0.90 inference(quant_intro,[status(thm)],[1])).
% 0.71/0.90 tff(3,plain,
% 0.71/0.90 (![X6: $i, X4: $i, X3: $i, X7: $i, X5: $i] : ((~p22(f3(f4(f5(c26))), X5)) | (~p23(X3, f8(f10(X4, f11(X5, X6))))) | (~p24(f17(f10(X4, f11(X5, X6)), X3))) | p23(f21(X4, X5, X6, X7, X3), f8(f10(X4, f11(X5, X6)))) | p12(X3, f16(f10(X4, f11(X5, X6)), c32, X7))) <=> ![X6: $i, X4: $i, X3: $i, X7: $i, X5: $i] : ((~p22(f3(f4(f5(c26))), X5)) | (~p23(X3, f8(f10(X4, f11(X5, X6))))) | (~p24(f17(f10(X4, f11(X5, X6)), X3))) | p23(f21(X4, X5, X6, X7, X3), f8(f10(X4, f11(X5, X6)))) | p12(X3, f16(f10(X4, f11(X5, X6)), c32, X7)))),
% 0.71/0.90 inference(rewrite,[status(thm)],[])).
% 0.71/0.90 tff(4,plain,
% 0.71/0.90 (^[X6: $i, X4: $i, X3: $i, X7: $i, X5: $i] : trans(monotonicity(trans(monotonicity(rewrite(((p12(X3, f16(f10(X4, f11(X5, X6)), c32, X7)) | p23(f21(X4, X5, X6, X7, X3), f8(f10(X4, f11(X5, X6))))) | (~p22(f3(f4(f5(c26))), X5))) <=> ((~p22(f3(f4(f5(c26))), X5)) | p23(f21(X4, X5, X6, X7, X3), f8(f10(X4, f11(X5, X6)))) | p12(X3, f16(f10(X4, f11(X5, X6)), c32, X7)))), ((((p12(X3, f16(f10(X4, f11(X5, X6)), c32, X7)) | p23(f21(X4, X5, X6, X7, X3), f8(f10(X4, f11(X5, X6))))) | (~p22(f3(f4(f5(c26))), X5))) | (~p24(f17(f10(X4, f11(X5, X6)), X3)))) <=> (((~p22(f3(f4(f5(c26))), X5)) | p23(f21(X4, X5, X6, X7, X3), f8(f10(X4, f11(X5, X6)))) | p12(X3, f16(f10(X4, f11(X5, X6)), c32, X7))) | (~p24(f17(f10(X4, f11(X5, X6)), X3)))))), rewrite((((~p22(f3(f4(f5(c26))), X5)) | p23(f21(X4, X5, X6, X7, X3), f8(f10(X4, f11(X5, X6)))) | p12(X3, f16(f10(X4, f11(X5, X6)), c32, X7))) | (~p24(f17(f10(X4, f11(X5, X6)), X3)))) <=> ((~p22(f3(f4(f5(c26))), X5)) | (~p24(f17(f10(X4, f11(X5, X6)), X3))) | p23(f21(X4, X5, X6, X7, X3), f8(f10(X4, f11(X5, X6)))) | p12(X3, f16(f10(X4, f11(X5, X6)), c32, X7)))), ((((p12(X3, f16(f10(X4, f11(X5, X6)), c32, X7)) | p23(f21(X4, X5, X6, X7, X3), f8(f10(X4, f11(X5, X6))))) | (~p22(f3(f4(f5(c26))), X5))) | (~p24(f17(f10(X4, f11(X5, X6)), X3)))) <=> ((~p22(f3(f4(f5(c26))), X5)) | (~p24(f17(f10(X4, f11(X5, X6)), X3))) | p23(f21(X4, X5, X6, X7, X3), f8(f10(X4, f11(X5, X6)))) | p12(X3, f16(f10(X4, f11(X5, X6)), c32, X7))))), (((((p12(X3, f16(f10(X4, f11(X5, X6)), c32, X7)) | p23(f21(X4, X5, X6, X7, X3), f8(f10(X4, f11(X5, X6))))) | (~p22(f3(f4(f5(c26))), X5))) | (~p24(f17(f10(X4, f11(X5, X6)), X3)))) | (~p23(X3, f8(f10(X4, f11(X5, X6)))))) <=> (((~p22(f3(f4(f5(c26))), X5)) | (~p24(f17(f10(X4, f11(X5, X6)), X3))) | p23(f21(X4, X5, X6, X7, X3), f8(f10(X4, f11(X5, X6)))) | p12(X3, f16(f10(X4, f11(X5, X6)), c32, X7))) | (~p23(X3, f8(f10(X4, f11(X5, X6)))))))), rewrite((((~p22(f3(f4(f5(c26))), X5)) | (~p24(f17(f10(X4, f11(X5, X6)), X3))) | p23(f21(X4, X5, X6, X7, X3), f8(f10(X4, f11(X5, X6)))) | p12(X3, f16(f10(X4, f11(X5, X6)), c32, X7))) | (~p23(X3, f8(f10(X4, f11(X5, X6)))))) <=> ((~p22(f3(f4(f5(c26))), X5)) | (~p23(X3, f8(f10(X4, f11(X5, X6))))) | (~p24(f17(f10(X4, f11(X5, X6)), X3))) | p23(f21(X4, X5, X6, X7, X3), f8(f10(X4, f11(X5, X6)))) | p12(X3, f16(f10(X4, f11(X5, X6)), c32, X7)))), (((((p12(X3, f16(f10(X4, f11(X5, X6)), c32, X7)) | p23(f21(X4, X5, X6, X7, X3), f8(f10(X4, f11(X5, X6))))) | (~p22(f3(f4(f5(c26))), X5))) | (~p24(f17(f10(X4, f11(X5, X6)), X3)))) | (~p23(X3, f8(f10(X4, f11(X5, X6)))))) <=> ((~p22(f3(f4(f5(c26))), X5)) | (~p23(X3, f8(f10(X4, f11(X5, X6))))) | (~p24(f17(f10(X4, f11(X5, X6)), X3))) | p23(f21(X4, X5, X6, X7, X3), f8(f10(X4, f11(X5, X6)))) | p12(X3, f16(f10(X4, f11(X5, X6)), c32, X7)))))),
% 0.71/0.90 inference(bind,[status(th)],[])).
% 0.71/0.90 tff(5,plain,
% 0.71/0.90 (![X6: $i, X4: $i, X3: $i, X7: $i, X5: $i] : ((((p12(X3, f16(f10(X4, f11(X5, X6)), c32, X7)) | p23(f21(X4, X5, X6, X7, X3), f8(f10(X4, f11(X5, X6))))) | (~p22(f3(f4(f5(c26))), X5))) | (~p24(f17(f10(X4, f11(X5, X6)), X3)))) | (~p23(X3, f8(f10(X4, f11(X5, X6)))))) <=> ![X6: $i, X4: $i, X3: $i, X7: $i, X5: $i] : ((~p22(f3(f4(f5(c26))), X5)) | (~p23(X3, f8(f10(X4, f11(X5, X6))))) | (~p24(f17(f10(X4, f11(X5, X6)), X3))) | p23(f21(X4, X5, X6, X7, X3), f8(f10(X4, f11(X5, X6)))) | p12(X3, f16(f10(X4, f11(X5, X6)), c32, X7)))),
% 0.71/0.90 inference(quant_intro,[status(thm)],[4])).
% 0.71/0.90 tff(6,axiom,(![X6: $i, X4: $i, X3: $i, X7: $i, X5: $i] : ((((p12(X3, f16(f10(X4, f11(X5, X6)), c32, X7)) | p23(f21(X4, X5, X6, X7, X3), f8(f10(X4, f11(X5, X6))))) | (~p22(f3(f4(f5(c26))), X5))) | (~p24(f17(f10(X4, f11(X5, X6)), X3)))) | (~p23(X3, f8(f10(X4, f11(X5, X6))))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','p12_39')).
% 0.71/0.90 tff(7,plain,
% 0.71/0.90 (![X6: $i, X4: $i, X3: $i, X7: $i, X5: $i] : ((~p22(f3(f4(f5(c26))), X5)) | (~p23(X3, f8(f10(X4, f11(X5, X6))))) | (~p24(f17(f10(X4, f11(X5, X6)), X3))) | p23(f21(X4, X5, X6, X7, X3), f8(f10(X4, f11(X5, X6)))) | p12(X3, f16(f10(X4, f11(X5, X6)), c32, X7)))),
% 0.71/0.90 inference(modus_ponens,[status(thm)],[6, 5])).
% 0.71/0.90 tff(8,plain,
% 0.71/0.90 (![X6: $i, X4: $i, X3: $i, X7: $i, X5: $i] : ((~p22(f3(f4(f5(c26))), X5)) | (~p23(X3, f8(f10(X4, f11(X5, X6))))) | (~p24(f17(f10(X4, f11(X5, X6)), X3))) | p23(f21(X4, X5, X6, X7, X3), f8(f10(X4, f11(X5, X6)))) | p12(X3, f16(f10(X4, f11(X5, X6)), c32, X7)))),
% 0.71/0.90 inference(modus_ponens,[status(thm)],[7, 3])).
% 0.71/0.90 tff(9,plain,(
% 0.71/0.90 ![X6: $i, X4: $i, X3: $i, X7: $i, X5: $i] : ((~p22(f3(f4(f5(c26))), X5)) | (~p23(X3, f8(f10(X4, f11(X5, X6))))) | (~p24(f17(f10(X4, f11(X5, X6)), X3))) | p23(f21(X4, X5, X6, X7, X3), f8(f10(X4, f11(X5, X6)))) | p12(X3, f16(f10(X4, f11(X5, X6)), c32, X7)))),
% 0.71/0.90 inference(skolemize,[status(sab)],[8])).
% 0.71/0.90 tff(10,plain,
% 0.71/0.90 (![X6: $i, X4: $i, X3: $i, X7: $i, X5: $i] : ((~p22(f3(f4(f5(c26))), X5)) | (~p23(X3, f8(f10(X4, f11(X5, X6))))) | (~p24(f17(f10(X4, f11(X5, X6)), X3))) | p23(f21(X4, X5, X6, X7, X3), f8(f10(X4, f11(X5, X6)))) | p12(X3, f16(f10(X4, f11(X5, X6)), c32, X7)))),
% 0.71/0.90 inference(modus_ponens,[status(thm)],[9, 2])).
% 0.71/0.90 tff(11,plain,
% 0.71/0.90 ((~p12(c28, f16(f10(c29, f11(c27, c30)), c32, c31))) <=> (~p12(c28, f16(f10(c29, f11(c27, c30)), c32, c31)))),
% 0.71/0.90 inference(rewrite,[status(thm)],[])).
% 0.71/0.90 tff(12,axiom,(~p12(c28, f16(f10(c29, f11(c27, c30)), c32, c31))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','not_p12_23')).
% 0.71/0.90 tff(13,plain,
% 0.71/0.90 (~p12(c28, f16(f10(c29, f11(c27, c30)), c32, c31))),
% 0.71/0.90 inference(modus_ponens,[status(thm)],[12, 11])).
% 0.71/0.90 tff(14,plain,
% 0.71/0.90 (p23(c28, f8(f10(c29, f11(c27, c30)))) <=> p23(c28, f8(f10(c29, f11(c27, c30))))),
% 0.71/0.90 inference(rewrite,[status(thm)],[])).
% 0.71/0.90 tff(15,axiom,(p23(c28, f8(f10(c29, f11(c27, c30))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','p23_10')).
% 0.71/0.90 tff(16,plain,
% 0.71/0.90 (p23(c28, f8(f10(c29, f11(c27, c30))))),
% 0.71/0.90 inference(modus_ponens,[status(thm)],[15, 14])).
% 0.71/0.90 tff(17,plain,
% 0.71/0.90 (p24(f17(f10(c29, f11(c27, c30)), c28)) <=> p24(f17(f10(c29, f11(c27, c30)), c28))),
% 0.71/0.90 inference(rewrite,[status(thm)],[])).
% 0.71/0.90 tff(18,axiom,(p24(f17(f10(c29, f11(c27, c30)), c28))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','f17_is_p24_9')).
% 0.71/0.90 tff(19,plain,
% 0.71/0.90 (p24(f17(f10(c29, f11(c27, c30)), c28))),
% 0.71/0.90 inference(modus_ponens,[status(thm)],[18, 17])).
% 0.71/0.90 tff(20,plain,
% 0.71/0.90 (p22(f3(f4(f5(c26))), c27) <=> p22(f3(f4(f5(c26))), c27)),
% 0.71/0.90 inference(rewrite,[status(thm)],[])).
% 0.71/0.90 tff(21,axiom,(p22(f3(f4(f5(c26))), c27)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','p22_7')).
% 0.71/0.90 tff(22,plain,
% 0.71/0.90 (p22(f3(f4(f5(c26))), c27)),
% 0.71/0.90 inference(modus_ponens,[status(thm)],[21, 20])).
% 0.71/0.90 tff(23,plain,
% 0.71/0.90 (((~![X6: $i, X4: $i, X3: $i, X7: $i, X5: $i] : ((~p22(f3(f4(f5(c26))), X5)) | (~p23(X3, f8(f10(X4, f11(X5, X6))))) | (~p24(f17(f10(X4, f11(X5, X6)), X3))) | p23(f21(X4, X5, X6, X7, X3), f8(f10(X4, f11(X5, X6)))) | p12(X3, f16(f10(X4, f11(X5, X6)), c32, X7)))) | (p12(c28, f16(f10(c29, f11(c27, c30)), c32, c31)) | (~p22(f3(f4(f5(c26))), c27)) | (~p23(c28, f8(f10(c29, f11(c27, c30))))) | p23(f21(c29, c27, c30, c31, c28), f8(f10(c29, f11(c27, c30)))) | (~p24(f17(f10(c29, f11(c27, c30)), c28))))) <=> ((~![X6: $i, X4: $i, X3: $i, X7: $i, X5: $i] : ((~p22(f3(f4(f5(c26))), X5)) | (~p23(X3, f8(f10(X4, f11(X5, X6))))) | (~p24(f17(f10(X4, f11(X5, X6)), X3))) | p23(f21(X4, X5, X6, X7, X3), f8(f10(X4, f11(X5, X6)))) | p12(X3, f16(f10(X4, f11(X5, X6)), c32, X7)))) | p12(c28, f16(f10(c29, f11(c27, c30)), c32, c31)) | (~p22(f3(f4(f5(c26))), c27)) | (~p23(c28, f8(f10(c29, f11(c27, c30))))) | p23(f21(c29, c27, c30, c31, c28), f8(f10(c29, f11(c27, c30)))) | (~p24(f17(f10(c29, f11(c27, c30)), c28))))),
% 0.71/0.90 inference(rewrite,[status(thm)],[])).
% 0.71/0.90 tff(24,plain,
% 0.71/0.90 (((~p22(f3(f4(f5(c26))), c27)) | (~p23(c28, f8(f10(c29, f11(c27, c30))))) | (~p24(f17(f10(c29, f11(c27, c30)), c28))) | p23(f21(c29, c27, c30, c31, c28), f8(f10(c29, f11(c27, c30)))) | p12(c28, f16(f10(c29, f11(c27, c30)), c32, c31))) <=> (p12(c28, f16(f10(c29, f11(c27, c30)), c32, c31)) | (~p22(f3(f4(f5(c26))), c27)) | (~p23(c28, f8(f10(c29, f11(c27, c30))))) | p23(f21(c29, c27, c30, c31, c28), f8(f10(c29, f11(c27, c30)))) | (~p24(f17(f10(c29, f11(c27, c30)), c28))))),
% 0.71/0.90 inference(rewrite,[status(thm)],[])).
% 0.71/0.90 tff(25,plain,
% 0.71/0.90 (((~![X6: $i, X4: $i, X3: $i, X7: $i, X5: $i] : ((~p22(f3(f4(f5(c26))), X5)) | (~p23(X3, f8(f10(X4, f11(X5, X6))))) | (~p24(f17(f10(X4, f11(X5, X6)), X3))) | p23(f21(X4, X5, X6, X7, X3), f8(f10(X4, f11(X5, X6)))) | p12(X3, f16(f10(X4, f11(X5, X6)), c32, X7)))) | ((~p22(f3(f4(f5(c26))), c27)) | (~p23(c28, f8(f10(c29, f11(c27, c30))))) | (~p24(f17(f10(c29, f11(c27, c30)), c28))) | p23(f21(c29, c27, c30, c31, c28), f8(f10(c29, f11(c27, c30)))) | p12(c28, f16(f10(c29, f11(c27, c30)), c32, c31)))) <=> ((~![X6: $i, X4: $i, X3: $i, X7: $i, X5: $i] : ((~p22(f3(f4(f5(c26))), X5)) | (~p23(X3, f8(f10(X4, f11(X5, X6))))) | (~p24(f17(f10(X4, f11(X5, X6)), X3))) | p23(f21(X4, X5, X6, X7, X3), f8(f10(X4, f11(X5, X6)))) | p12(X3, f16(f10(X4, f11(X5, X6)), c32, X7)))) | (p12(c28, f16(f10(c29, f11(c27, c30)), c32, c31)) | (~p22(f3(f4(f5(c26))), c27)) | (~p23(c28, f8(f10(c29, f11(c27, c30))))) | p23(f21(c29, c27, c30, c31, c28), f8(f10(c29, f11(c27, c30)))) | (~p24(f17(f10(c29, f11(c27, c30)), c28)))))),
% 0.71/0.90 inference(monotonicity,[status(thm)],[24])).
% 0.71/0.90 tff(26,plain,
% 0.71/0.90 (((~![X6: $i, X4: $i, X3: $i, X7: $i, X5: $i] : ((~p22(f3(f4(f5(c26))), X5)) | (~p23(X3, f8(f10(X4, f11(X5, X6))))) | (~p24(f17(f10(X4, f11(X5, X6)), X3))) | p23(f21(X4, X5, X6, X7, X3), f8(f10(X4, f11(X5, X6)))) | p12(X3, f16(f10(X4, f11(X5, X6)), c32, X7)))) | ((~p22(f3(f4(f5(c26))), c27)) | (~p23(c28, f8(f10(c29, f11(c27, c30))))) | (~p24(f17(f10(c29, f11(c27, c30)), c28))) | p23(f21(c29, c27, c30, c31, c28), f8(f10(c29, f11(c27, c30)))) | p12(c28, f16(f10(c29, f11(c27, c30)), c32, c31)))) <=> ((~![X6: $i, X4: $i, X3: $i, X7: $i, X5: $i] : ((~p22(f3(f4(f5(c26))), X5)) | (~p23(X3, f8(f10(X4, f11(X5, X6))))) | (~p24(f17(f10(X4, f11(X5, X6)), X3))) | p23(f21(X4, X5, X6, X7, X3), f8(f10(X4, f11(X5, X6)))) | p12(X3, f16(f10(X4, f11(X5, X6)), c32, X7)))) | p12(c28, f16(f10(c29, f11(c27, c30)), c32, c31)) | (~p22(f3(f4(f5(c26))), c27)) | (~p23(c28, f8(f10(c29, f11(c27, c30))))) | p23(f21(c29, c27, c30, c31, c28), f8(f10(c29, f11(c27, c30)))) | (~p24(f17(f10(c29, f11(c27, c30)), c28))))),
% 0.71/0.90 inference(transitivity,[status(thm)],[25, 23])).
% 0.71/0.90 tff(27,plain,
% 0.71/0.90 ((~![X6: $i, X4: $i, X3: $i, X7: $i, X5: $i] : ((~p22(f3(f4(f5(c26))), X5)) | (~p23(X3, f8(f10(X4, f11(X5, X6))))) | (~p24(f17(f10(X4, f11(X5, X6)), X3))) | p23(f21(X4, X5, X6, X7, X3), f8(f10(X4, f11(X5, X6)))) | p12(X3, f16(f10(X4, f11(X5, X6)), c32, X7)))) | ((~p22(f3(f4(f5(c26))), c27)) | (~p23(c28, f8(f10(c29, f11(c27, c30))))) | (~p24(f17(f10(c29, f11(c27, c30)), c28))) | p23(f21(c29, c27, c30, c31, c28), f8(f10(c29, f11(c27, c30)))) | p12(c28, f16(f10(c29, f11(c27, c30)), c32, c31)))),
% 0.71/0.90 inference(quant_inst,[status(thm)],[])).
% 0.71/0.90 tff(28,plain,
% 0.71/0.90 ((~![X6: $i, X4: $i, X3: $i, X7: $i, X5: $i] : ((~p22(f3(f4(f5(c26))), X5)) | (~p23(X3, f8(f10(X4, f11(X5, X6))))) | (~p24(f17(f10(X4, f11(X5, X6)), X3))) | p23(f21(X4, X5, X6, X7, X3), f8(f10(X4, f11(X5, X6)))) | p12(X3, f16(f10(X4, f11(X5, X6)), c32, X7)))) | p12(c28, f16(f10(c29, f11(c27, c30)), c32, c31)) | (~p22(f3(f4(f5(c26))), c27)) | (~p23(c28, f8(f10(c29, f11(c27, c30))))) | p23(f21(c29, c27, c30, c31, c28), f8(f10(c29, f11(c27, c30)))) | (~p24(f17(f10(c29, f11(c27, c30)), c28)))),
% 0.71/0.90 inference(modus_ponens,[status(thm)],[27, 26])).
% 0.71/0.90 tff(29,plain,
% 0.71/0.90 (p23(f21(c29, c27, c30, c31, c28), f8(f10(c29, f11(c27, c30))))),
% 0.71/0.90 inference(unit_resolution,[status(thm)],[28, 22, 19, 16, 13, 10])).
% 0.71/0.90 tff(30,plain,
% 0.71/0.90 (^[X6: $i, X4: $i, X3: $i, X7: $i, X5: $i] : refl(((~p22(f3(f4(f5(c26))), X5)) | (~p23(X3, f8(f10(X4, f11(X5, X6))))) | p25(f13(f14(X7, f16(f10(X4, f11(X5, X6)), c32, X7))), f13(f14(X7, X3)))) <=> ((~p22(f3(f4(f5(c26))), X5)) | (~p23(X3, f8(f10(X4, f11(X5, X6))))) | p25(f13(f14(X7, f16(f10(X4, f11(X5, X6)), c32, X7))), f13(f14(X7, X3)))))),
% 0.71/0.90 inference(bind,[status(th)],[])).
% 0.71/0.90 tff(31,plain,
% 0.71/0.90 (![X6: $i, X4: $i, X3: $i, X7: $i, X5: $i] : ((~p22(f3(f4(f5(c26))), X5)) | (~p23(X3, f8(f10(X4, f11(X5, X6))))) | p25(f13(f14(X7, f16(f10(X4, f11(X5, X6)), c32, X7))), f13(f14(X7, X3)))) <=> ![X6: $i, X4: $i, X3: $i, X7: $i, X5: $i] : ((~p22(f3(f4(f5(c26))), X5)) | (~p23(X3, f8(f10(X4, f11(X5, X6))))) | p25(f13(f14(X7, f16(f10(X4, f11(X5, X6)), c32, X7))), f13(f14(X7, X3))))),
% 0.71/0.90 inference(quant_intro,[status(thm)],[30])).
% 0.71/0.90 tff(32,plain,
% 0.71/0.90 (![X6: $i, X4: $i, X3: $i, X7: $i, X5: $i] : ((~p22(f3(f4(f5(c26))), X5)) | (~p23(X3, f8(f10(X4, f11(X5, X6))))) | p25(f13(f14(X7, f16(f10(X4, f11(X5, X6)), c32, X7))), f13(f14(X7, X3)))) <=> ![X6: $i, X4: $i, X3: $i, X7: $i, X5: $i] : ((~p22(f3(f4(f5(c26))), X5)) | (~p23(X3, f8(f10(X4, f11(X5, X6))))) | p25(f13(f14(X7, f16(f10(X4, f11(X5, X6)), c32, X7))), f13(f14(X7, X3))))),
% 0.71/0.90 inference(rewrite,[status(thm)],[])).
% 0.71/0.90 tff(33,plain,
% 0.71/0.90 (^[X6: $i, X4: $i, X3: $i, X7: $i, X5: $i] : trans(monotonicity(rewrite((p25(f13(f14(X7, f16(f10(X4, f11(X5, X6)), c32, X7))), f13(f14(X7, X3))) | (~p22(f3(f4(f5(c26))), X5))) <=> ((~p22(f3(f4(f5(c26))), X5)) | p25(f13(f14(X7, f16(f10(X4, f11(X5, X6)), c32, X7))), f13(f14(X7, X3))))), (((p25(f13(f14(X7, f16(f10(X4, f11(X5, X6)), c32, X7))), f13(f14(X7, X3))) | (~p22(f3(f4(f5(c26))), X5))) | (~p23(X3, f8(f10(X4, f11(X5, X6)))))) <=> (((~p22(f3(f4(f5(c26))), X5)) | p25(f13(f14(X7, f16(f10(X4, f11(X5, X6)), c32, X7))), f13(f14(X7, X3)))) | (~p23(X3, f8(f10(X4, f11(X5, X6)))))))), rewrite((((~p22(f3(f4(f5(c26))), X5)) | p25(f13(f14(X7, f16(f10(X4, f11(X5, X6)), c32, X7))), f13(f14(X7, X3)))) | (~p23(X3, f8(f10(X4, f11(X5, X6)))))) <=> ((~p22(f3(f4(f5(c26))), X5)) | (~p23(X3, f8(f10(X4, f11(X5, X6))))) | p25(f13(f14(X7, f16(f10(X4, f11(X5, X6)), c32, X7))), f13(f14(X7, X3))))), (((p25(f13(f14(X7, f16(f10(X4, f11(X5, X6)), c32, X7))), f13(f14(X7, X3))) | (~p22(f3(f4(f5(c26))), X5))) | (~p23(X3, f8(f10(X4, f11(X5, X6)))))) <=> ((~p22(f3(f4(f5(c26))), X5)) | (~p23(X3, f8(f10(X4, f11(X5, X6))))) | p25(f13(f14(X7, f16(f10(X4, f11(X5, X6)), c32, X7))), f13(f14(X7, X3))))))),
% 0.71/0.90 inference(bind,[status(th)],[])).
% 0.71/0.90 tff(34,plain,
% 0.71/0.90 (![X6: $i, X4: $i, X3: $i, X7: $i, X5: $i] : ((p25(f13(f14(X7, f16(f10(X4, f11(X5, X6)), c32, X7))), f13(f14(X7, X3))) | (~p22(f3(f4(f5(c26))), X5))) | (~p23(X3, f8(f10(X4, f11(X5, X6)))))) <=> ![X6: $i, X4: $i, X3: $i, X7: $i, X5: $i] : ((~p22(f3(f4(f5(c26))), X5)) | (~p23(X3, f8(f10(X4, f11(X5, X6))))) | p25(f13(f14(X7, f16(f10(X4, f11(X5, X6)), c32, X7))), f13(f14(X7, X3))))),
% 0.71/0.90 inference(quant_intro,[status(thm)],[33])).
% 0.71/0.90 tff(35,axiom,(![X6: $i, X4: $i, X3: $i, X7: $i, X5: $i] : ((p25(f13(f14(X7, f16(f10(X4, f11(X5, X6)), c32, X7))), f13(f14(X7, X3))) | (~p22(f3(f4(f5(c26))), X5))) | (~p23(X3, f8(f10(X4, f11(X5, X6))))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','p25_37')).
% 0.71/0.90 tff(36,plain,
% 0.71/0.90 (![X6: $i, X4: $i, X3: $i, X7: $i, X5: $i] : ((~p22(f3(f4(f5(c26))), X5)) | (~p23(X3, f8(f10(X4, f11(X5, X6))))) | p25(f13(f14(X7, f16(f10(X4, f11(X5, X6)), c32, X7))), f13(f14(X7, X3))))),
% 0.71/0.90 inference(modus_ponens,[status(thm)],[35, 34])).
% 0.71/0.90 tff(37,plain,
% 0.71/0.90 (![X6: $i, X4: $i, X3: $i, X7: $i, X5: $i] : ((~p22(f3(f4(f5(c26))), X5)) | (~p23(X3, f8(f10(X4, f11(X5, X6))))) | p25(f13(f14(X7, f16(f10(X4, f11(X5, X6)), c32, X7))), f13(f14(X7, X3))))),
% 0.71/0.90 inference(modus_ponens,[status(thm)],[36, 32])).
% 0.71/0.90 tff(38,plain,(
% 0.71/0.90 ![X6: $i, X4: $i, X3: $i, X7: $i, X5: $i] : ((~p22(f3(f4(f5(c26))), X5)) | (~p23(X3, f8(f10(X4, f11(X5, X6))))) | p25(f13(f14(X7, f16(f10(X4, f11(X5, X6)), c32, X7))), f13(f14(X7, X3))))),
% 0.71/0.90 inference(skolemize,[status(sab)],[37])).
% 0.71/0.90 tff(39,plain,
% 0.71/0.90 (![X6: $i, X4: $i, X3: $i, X7: $i, X5: $i] : ((~p22(f3(f4(f5(c26))), X5)) | (~p23(X3, f8(f10(X4, f11(X5, X6))))) | p25(f13(f14(X7, f16(f10(X4, f11(X5, X6)), c32, X7))), f13(f14(X7, X3))))),
% 0.71/0.90 inference(modus_ponens,[status(thm)],[38, 31])).
% 0.71/0.90 tff(40,plain,
% 0.71/0.90 (((~![X6: $i, X4: $i, X3: $i, X7: $i, X5: $i] : ((~p22(f3(f4(f5(c26))), X5)) | (~p23(X3, f8(f10(X4, f11(X5, X6))))) | p25(f13(f14(X7, f16(f10(X4, f11(X5, X6)), c32, X7))), f13(f14(X7, X3))))) | ((~p22(f3(f4(f5(c26))), c27)) | (~p23(f21(c29, c27, c30, c31, c28), f8(f10(c29, f11(c27, c30))))) | p25(f13(f14(c31, f16(f10(c29, f11(c27, c30)), c32, c31))), f13(f14(c31, f21(c29, c27, c30, c31, c28)))))) <=> ((~![X6: $i, X4: $i, X3: $i, X7: $i, X5: $i] : ((~p22(f3(f4(f5(c26))), X5)) | (~p23(X3, f8(f10(X4, f11(X5, X6))))) | p25(f13(f14(X7, f16(f10(X4, f11(X5, X6)), c32, X7))), f13(f14(X7, X3))))) | (~p22(f3(f4(f5(c26))), c27)) | (~p23(f21(c29, c27, c30, c31, c28), f8(f10(c29, f11(c27, c30))))) | p25(f13(f14(c31, f16(f10(c29, f11(c27, c30)), c32, c31))), f13(f14(c31, f21(c29, c27, c30, c31, c28)))))),
% 0.71/0.90 inference(rewrite,[status(thm)],[])).
% 0.71/0.90 tff(41,plain,
% 0.71/0.90 ((~![X6: $i, X4: $i, X3: $i, X7: $i, X5: $i] : ((~p22(f3(f4(f5(c26))), X5)) | (~p23(X3, f8(f10(X4, f11(X5, X6))))) | p25(f13(f14(X7, f16(f10(X4, f11(X5, X6)), c32, X7))), f13(f14(X7, X3))))) | ((~p22(f3(f4(f5(c26))), c27)) | (~p23(f21(c29, c27, c30, c31, c28), f8(f10(c29, f11(c27, c30))))) | p25(f13(f14(c31, f16(f10(c29, f11(c27, c30)), c32, c31))), f13(f14(c31, f21(c29, c27, c30, c31, c28)))))),
% 0.71/0.90 inference(quant_inst,[status(thm)],[])).
% 0.71/0.90 tff(42,plain,
% 0.71/0.90 ((~![X6: $i, X4: $i, X3: $i, X7: $i, X5: $i] : ((~p22(f3(f4(f5(c26))), X5)) | (~p23(X3, f8(f10(X4, f11(X5, X6))))) | p25(f13(f14(X7, f16(f10(X4, f11(X5, X6)), c32, X7))), f13(f14(X7, X3))))) | (~p22(f3(f4(f5(c26))), c27)) | (~p23(f21(c29, c27, c30, c31, c28), f8(f10(c29, f11(c27, c30))))) | p25(f13(f14(c31, f16(f10(c29, f11(c27, c30)), c32, c31))), f13(f14(c31, f21(c29, c27, c30, c31, c28))))),
% 0.71/0.90 inference(modus_ponens,[status(thm)],[41, 40])).
% 0.71/0.90 tff(43,plain,
% 0.71/0.90 (p25(f13(f14(c31, f16(f10(c29, f11(c27, c30)), c32, c31))), f13(f14(c31, f21(c29, c27, c30, c31, c28))))),
% 0.71/0.90 inference(unit_resolution,[status(thm)],[42, 22, 39, 29])).
% 0.71/0.90 tff(44,assumption,(~p12(c28, c28)), introduced(assumption)).
% 0.71/0.90 tff(45,plain,
% 0.71/0.90 (^[X0: $i] : refl(p12(X0, X0) <=> p12(X0, X0))),
% 0.71/0.90 inference(bind,[status(th)],[])).
% 0.71/0.90 tff(46,plain,
% 0.71/0.90 (![X0: $i] : p12(X0, X0) <=> ![X0: $i] : p12(X0, X0)),
% 0.71/0.90 inference(quant_intro,[status(thm)],[45])).
% 0.71/0.90 tff(47,plain,
% 0.71/0.90 (![X0: $i] : p12(X0, X0) <=> ![X0: $i] : p12(X0, X0)),
% 0.71/0.90 inference(rewrite,[status(thm)],[])).
% 0.71/0.90 tff(48,axiom,(![X0: $i] : p12(X0, X0)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','p12_1')).
% 0.71/0.90 tff(49,plain,
% 0.71/0.90 (![X0: $i] : p12(X0, X0)),
% 0.71/0.90 inference(modus_ponens,[status(thm)],[48, 47])).
% 0.71/0.90 tff(50,plain,(
% 0.71/0.90 ![X0: $i] : p12(X0, X0)),
% 0.71/0.90 inference(skolemize,[status(sab)],[49])).
% 0.71/0.90 tff(51,plain,
% 0.71/0.90 (![X0: $i] : p12(X0, X0)),
% 0.71/0.90 inference(modus_ponens,[status(thm)],[50, 46])).
% 0.71/0.90 tff(52,plain,
% 0.71/0.90 ((~![X0: $i] : p12(X0, X0)) | p12(c28, c28)),
% 0.71/0.90 inference(quant_inst,[status(thm)],[])).
% 0.71/0.90 tff(53,plain,
% 0.71/0.90 ($false),
% 0.71/0.90 inference(unit_resolution,[status(thm)],[52, 51, 44])).
% 0.71/0.90 tff(54,plain,(p12(c28, c28)), inference(lemma,lemma(discharge,[]))).
% 0.71/0.90 tff(55,assumption,(~p2(c27, c27)), introduced(assumption)).
% 0.71/0.90 tff(56,plain,
% 0.71/0.90 (^[X43: $i] : refl(p2(X43, X43) <=> p2(X43, X43))),
% 0.71/0.90 inference(bind,[status(th)],[])).
% 0.71/0.90 tff(57,plain,
% 0.71/0.90 (![X43: $i] : p2(X43, X43) <=> ![X43: $i] : p2(X43, X43)),
% 0.71/0.90 inference(quant_intro,[status(thm)],[56])).
% 0.71/0.90 tff(58,plain,
% 0.71/0.90 (![X43: $i] : p2(X43, X43) <=> ![X43: $i] : p2(X43, X43)),
% 0.71/0.90 inference(rewrite,[status(thm)],[])).
% 0.71/0.90 tff(59,axiom,(![X43: $i] : p2(X43, X43)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','p2_5')).
% 0.71/0.90 tff(60,plain,
% 0.71/0.90 (![X43: $i] : p2(X43, X43)),
% 0.71/0.90 inference(modus_ponens,[status(thm)],[59, 58])).
% 0.71/0.90 tff(61,plain,(
% 0.71/0.90 ![X43: $i] : p2(X43, X43)),
% 0.71/0.90 inference(skolemize,[status(sab)],[60])).
% 0.71/0.90 tff(62,plain,
% 0.71/0.90 (![X43: $i] : p2(X43, X43)),
% 0.71/0.90 inference(modus_ponens,[status(thm)],[61, 57])).
% 0.71/0.90 tff(63,plain,
% 0.71/0.90 ((~![X43: $i] : p2(X43, X43)) | p2(c27, c27)),
% 0.71/0.90 inference(quant_inst,[status(thm)],[])).
% 0.71/0.90 tff(64,plain,
% 0.71/0.90 ($false),
% 0.71/0.90 inference(unit_resolution,[status(thm)],[63, 62, 55])).
% 0.71/0.90 tff(65,plain,(p2(c27, c27)), inference(lemma,lemma(discharge,[]))).
% 0.71/0.90 tff(66,assumption,(~p2(c29, c29)), introduced(assumption)).
% 0.71/0.90 tff(67,plain,
% 0.71/0.90 ((~![X43: $i] : p2(X43, X43)) | p2(c29, c29)),
% 0.71/0.90 inference(quant_inst,[status(thm)],[])).
% 0.71/0.90 tff(68,plain,
% 0.71/0.90 ($false),
% 0.71/0.90 inference(unit_resolution,[status(thm)],[67, 62, 66])).
% 0.71/0.90 tff(69,plain,(p2(c29, c29)), inference(lemma,lemma(discharge,[]))).
% 0.71/0.90 tff(70,assumption,(~p12(c31, c31)), introduced(assumption)).
% 0.71/0.90 tff(71,plain,
% 0.71/0.90 ((~![X0: $i] : p12(X0, X0)) | p12(c31, c31)),
% 0.71/0.90 inference(quant_inst,[status(thm)],[])).
% 0.71/0.90 tff(72,plain,
% 0.71/0.90 ($false),
% 0.71/0.90 inference(unit_resolution,[status(thm)],[71, 51, 70])).
% 0.71/0.90 tff(73,plain,(p12(c31, c31)), inference(lemma,lemma(discharge,[]))).
% 0.71/0.90 tff(74,assumption,(~p2(c30, c30)), introduced(assumption)).
% 0.71/0.90 tff(75,plain,
% 0.71/0.90 ((~![X43: $i] : p2(X43, X43)) | p2(c30, c30)),
% 0.71/0.91 inference(quant_inst,[status(thm)],[])).
% 0.71/0.91 tff(76,plain,
% 0.71/0.91 ($false),
% 0.71/0.91 inference(unit_resolution,[status(thm)],[75, 62, 74])).
% 0.71/0.91 tff(77,plain,(p2(c30, c30)), inference(lemma,lemma(discharge,[]))).
% 0.71/0.91 tff(78,plain,
% 0.71/0.91 (^[X39: $i, X31: $i, X38: $i, X37: $i, X32: $i, X30: $i, X35: $i, X34: $i, X36: $i, X33: $i] : refl(((~p2(X30, X35)) | (~p12(X34, X39)) | (~p12(X33, X38)) | (~p2(X32, X37)) | (~p2(X31, X36)) | p12(f21(X30, X31, X32, X33, X34), f21(X35, X36, X37, X38, X39))) <=> ((~p2(X30, X35)) | (~p12(X34, X39)) | (~p12(X33, X38)) | (~p2(X32, X37)) | (~p2(X31, X36)) | p12(f21(X30, X31, X32, X33, X34), f21(X35, X36, X37, X38, X39))))),
% 0.71/0.91 inference(bind,[status(th)],[])).
% 0.71/0.91 tff(79,plain,
% 0.71/0.91 (![X39: $i, X31: $i, X38: $i, X37: $i, X32: $i, X30: $i, X35: $i, X34: $i, X36: $i, X33: $i] : ((~p2(X30, X35)) | (~p12(X34, X39)) | (~p12(X33, X38)) | (~p2(X32, X37)) | (~p2(X31, X36)) | p12(f21(X30, X31, X32, X33, X34), f21(X35, X36, X37, X38, X39))) <=> ![X39: $i, X31: $i, X38: $i, X37: $i, X32: $i, X30: $i, X35: $i, X34: $i, X36: $i, X33: $i] : ((~p2(X30, X35)) | (~p12(X34, X39)) | (~p12(X33, X38)) | (~p2(X32, X37)) | (~p2(X31, X36)) | p12(f21(X30, X31, X32, X33, X34), f21(X35, X36, X37, X38, X39)))),
% 0.71/0.91 inference(quant_intro,[status(thm)],[78])).
% 0.71/0.91 tff(80,plain,
% 0.71/0.91 (![X39: $i, X31: $i, X38: $i, X37: $i, X32: $i, X30: $i, X35: $i, X34: $i, X36: $i, X33: $i] : ((~p2(X30, X35)) | (~p12(X34, X39)) | (~p12(X33, X38)) | (~p2(X32, X37)) | (~p2(X31, X36)) | p12(f21(X30, X31, X32, X33, X34), f21(X35, X36, X37, X38, X39))) <=> ![X39: $i, X31: $i, X38: $i, X37: $i, X32: $i, X30: $i, X35: $i, X34: $i, X36: $i, X33: $i] : ((~p2(X30, X35)) | (~p12(X34, X39)) | (~p12(X33, X38)) | (~p2(X32, X37)) | (~p2(X31, X36)) | p12(f21(X30, X31, X32, X33, X34), f21(X35, X36, X37, X38, X39)))),
% 0.71/0.91 inference(rewrite,[status(thm)],[])).
% 0.71/0.91 tff(81,plain,
% 0.71/0.91 (^[X39: $i, X31: $i, X38: $i, X37: $i, X32: $i, X30: $i, X35: $i, X34: $i, X36: $i, X33: $i] : trans(monotonicity(trans(monotonicity(trans(monotonicity(trans(monotonicity(rewrite((p12(f21(X30, X31, X32, X33, X34), f21(X35, X36, X37, X38, X39)) | (~p2(X31, X36))) <=> ((~p2(X31, X36)) | p12(f21(X30, X31, X32, X33, X34), f21(X35, X36, X37, X38, X39)))), (((p12(f21(X30, X31, X32, X33, X34), f21(X35, X36, X37, X38, X39)) | (~p2(X31, X36))) | (~p2(X32, X37))) <=> (((~p2(X31, X36)) | p12(f21(X30, X31, X32, X33, X34), f21(X35, X36, X37, X38, X39))) | (~p2(X32, X37))))), rewrite((((~p2(X31, X36)) | p12(f21(X30, X31, X32, X33, X34), f21(X35, X36, X37, X38, X39))) | (~p2(X32, X37))) <=> ((~p2(X32, X37)) | (~p2(X31, X36)) | p12(f21(X30, X31, X32, X33, X34), f21(X35, X36, X37, X38, X39)))), (((p12(f21(X30, X31, X32, X33, X34), f21(X35, X36, X37, X38, X39)) | (~p2(X31, X36))) | (~p2(X32, X37))) <=> ((~p2(X32, X37)) | (~p2(X31, X36)) | p12(f21(X30, X31, X32, X33, X34), f21(X35, X36, X37, X38, X39))))), ((((p12(f21(X30, X31, X32, X33, X34), f21(X35, X36, X37, X38, X39)) | (~p2(X31, X36))) | (~p2(X32, X37))) | (~p12(X33, X38))) <=> (((~p2(X32, X37)) | (~p2(X31, X36)) | p12(f21(X30, X31, X32, X33, X34), f21(X35, X36, X37, X38, X39))) | (~p12(X33, X38))))), rewrite((((~p2(X32, X37)) | (~p2(X31, X36)) | p12(f21(X30, X31, X32, X33, X34), f21(X35, X36, X37, X38, X39))) | (~p12(X33, X38))) <=> ((~p12(X33, X38)) | (~p2(X32, X37)) | (~p2(X31, X36)) | p12(f21(X30, X31, X32, X33, X34), f21(X35, X36, X37, X38, X39)))), ((((p12(f21(X30, X31, X32, X33, X34), f21(X35, X36, X37, X38, X39)) | (~p2(X31, X36))) | (~p2(X32, X37))) | (~p12(X33, X38))) <=> ((~p12(X33, X38)) | (~p2(X32, X37)) | (~p2(X31, X36)) | p12(f21(X30, X31, X32, X33, X34), f21(X35, X36, X37, X38, X39))))), (((((p12(f21(X30, X31, X32, X33, X34), f21(X35, X36, X37, X38, X39)) | (~p2(X31, X36))) | (~p2(X32, X37))) | (~p12(X33, X38))) | (~p12(X34, X39))) <=> (((~p12(X33, X38)) | (~p2(X32, X37)) | (~p2(X31, X36)) | p12(f21(X30, X31, X32, X33, X34), f21(X35, X36, X37, X38, X39))) | (~p12(X34, X39))))), rewrite((((~p12(X33, X38)) | (~p2(X32, X37)) | (~p2(X31, X36)) | p12(f21(X30, X31, X32, X33, X34), f21(X35, X36, X37, X38, X39))) | (~p12(X34, X39))) <=> ((~p12(X34, X39)) | (~p12(X33, X38)) | (~p2(X32, X37)) | (~p2(X31, X36)) | p12(f21(X30, X31, X32, X33, X34), f21(X35, X36, X37, X38, X39)))), (((((p12(f21(X30, X31, X32, X33, X34), f21(X35, X36, X37, X38, X39)) | (~p2(X31, X36))) | (~p2(X32, X37))) | (~p12(X33, X38))) | (~p12(X34, X39))) <=> ((~p12(X34, X39)) | (~p12(X33, X38)) | (~p2(X32, X37)) | (~p2(X31, X36)) | p12(f21(X30, X31, X32, X33, X34), f21(X35, X36, X37, X38, X39))))), ((((((p12(f21(X30, X31, X32, X33, X34), f21(X35, X36, X37, X38, X39)) | (~p2(X31, X36))) | (~p2(X32, X37))) | (~p12(X33, X38))) | (~p12(X34, X39))) | (~p2(X30, X35))) <=> (((~p12(X34, X39)) | (~p12(X33, X38)) | (~p2(X32, X37)) | (~p2(X31, X36)) | p12(f21(X30, X31, X32, X33, X34), f21(X35, X36, X37, X38, X39))) | (~p2(X30, X35))))), rewrite((((~p12(X34, X39)) | (~p12(X33, X38)) | (~p2(X32, X37)) | (~p2(X31, X36)) | p12(f21(X30, X31, X32, X33, X34), f21(X35, X36, X37, X38, X39))) | (~p2(X30, X35))) <=> ((~p2(X30, X35)) | (~p12(X34, X39)) | (~p12(X33, X38)) | (~p2(X32, X37)) | (~p2(X31, X36)) | p12(f21(X30, X31, X32, X33, X34), f21(X35, X36, X37, X38, X39)))), ((((((p12(f21(X30, X31, X32, X33, X34), f21(X35, X36, X37, X38, X39)) | (~p2(X31, X36))) | (~p2(X32, X37))) | (~p12(X33, X38))) | (~p12(X34, X39))) | (~p2(X30, X35))) <=> ((~p2(X30, X35)) | (~p12(X34, X39)) | (~p12(X33, X38)) | (~p2(X32, X37)) | (~p2(X31, X36)) | p12(f21(X30, X31, X32, X33, X34), f21(X35, X36, X37, X38, X39)))))),
% 0.71/0.91 inference(bind,[status(th)],[])).
% 0.71/0.91 tff(82,plain,
% 0.71/0.91 (![X39: $i, X31: $i, X38: $i, X37: $i, X32: $i, X30: $i, X35: $i, X34: $i, X36: $i, X33: $i] : (((((p12(f21(X30, X31, X32, X33, X34), f21(X35, X36, X37, X38, X39)) | (~p2(X31, X36))) | (~p2(X32, X37))) | (~p12(X33, X38))) | (~p12(X34, X39))) | (~p2(X30, X35))) <=> ![X39: $i, X31: $i, X38: $i, X37: $i, X32: $i, X30: $i, X35: $i, X34: $i, X36: $i, X33: $i] : ((~p2(X30, X35)) | (~p12(X34, X39)) | (~p12(X33, X38)) | (~p2(X32, X37)) | (~p2(X31, X36)) | p12(f21(X30, X31, X32, X33, X34), f21(X35, X36, X37, X38, X39)))),
% 0.71/0.91 inference(quant_intro,[status(thm)],[81])).
% 0.71/0.91 tff(83,axiom,(![X39: $i, X31: $i, X38: $i, X37: $i, X32: $i, X30: $i, X35: $i, X34: $i, X36: $i, X33: $i] : (((((p12(f21(X30, X31, X32, X33, X34), f21(X35, X36, X37, X38, X39)) | (~p2(X31, X36))) | (~p2(X32, X37))) | (~p12(X33, X38))) | (~p12(X34, X39))) | (~p2(X30, X35)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','p12_36')).
% 0.71/0.91 tff(84,plain,
% 0.71/0.91 (![X39: $i, X31: $i, X38: $i, X37: $i, X32: $i, X30: $i, X35: $i, X34: $i, X36: $i, X33: $i] : ((~p2(X30, X35)) | (~p12(X34, X39)) | (~p12(X33, X38)) | (~p2(X32, X37)) | (~p2(X31, X36)) | p12(f21(X30, X31, X32, X33, X34), f21(X35, X36, X37, X38, X39)))),
% 0.71/0.91 inference(modus_ponens,[status(thm)],[83, 82])).
% 0.71/0.91 tff(85,plain,
% 0.71/0.91 (![X39: $i, X31: $i, X38: $i, X37: $i, X32: $i, X30: $i, X35: $i, X34: $i, X36: $i, X33: $i] : ((~p2(X30, X35)) | (~p12(X34, X39)) | (~p12(X33, X38)) | (~p2(X32, X37)) | (~p2(X31, X36)) | p12(f21(X30, X31, X32, X33, X34), f21(X35, X36, X37, X38, X39)))),
% 0.71/0.91 inference(modus_ponens,[status(thm)],[84, 80])).
% 0.71/0.91 tff(86,plain,(
% 0.71/0.91 ![X39: $i, X31: $i, X38: $i, X37: $i, X32: $i, X30: $i, X35: $i, X34: $i, X36: $i, X33: $i] : ((~p2(X30, X35)) | (~p12(X34, X39)) | (~p12(X33, X38)) | (~p2(X32, X37)) | (~p2(X31, X36)) | p12(f21(X30, X31, X32, X33, X34), f21(X35, X36, X37, X38, X39)))),
% 0.71/0.91 inference(skolemize,[status(sab)],[85])).
% 0.71/0.91 tff(87,plain,
% 0.71/0.91 (![X39: $i, X31: $i, X38: $i, X37: $i, X32: $i, X30: $i, X35: $i, X34: $i, X36: $i, X33: $i] : ((~p2(X30, X35)) | (~p12(X34, X39)) | (~p12(X33, X38)) | (~p2(X32, X37)) | (~p2(X31, X36)) | p12(f21(X30, X31, X32, X33, X34), f21(X35, X36, X37, X38, X39)))),
% 0.71/0.91 inference(modus_ponens,[status(thm)],[86, 79])).
% 0.71/0.91 tff(88,plain,
% 0.71/0.91 (((~![X39: $i, X31: $i, X38: $i, X37: $i, X32: $i, X30: $i, X35: $i, X34: $i, X36: $i, X33: $i] : ((~p2(X30, X35)) | (~p12(X34, X39)) | (~p12(X33, X38)) | (~p2(X32, X37)) | (~p2(X31, X36)) | p12(f21(X30, X31, X32, X33, X34), f21(X35, X36, X37, X38, X39)))) | ((~p2(c30, c30)) | (~p2(c27, c27)) | (~p12(c28, c28)) | (~p12(c31, c31)) | (~p2(c29, c29)) | p12(f21(c29, c27, c30, c31, c28), f21(c29, c27, c30, c31, c28)))) <=> ((~![X39: $i, X31: $i, X38: $i, X37: $i, X32: $i, X30: $i, X35: $i, X34: $i, X36: $i, X33: $i] : ((~p2(X30, X35)) | (~p12(X34, X39)) | (~p12(X33, X38)) | (~p2(X32, X37)) | (~p2(X31, X36)) | p12(f21(X30, X31, X32, X33, X34), f21(X35, X36, X37, X38, X39)))) | (~p2(c30, c30)) | (~p2(c27, c27)) | (~p12(c28, c28)) | (~p12(c31, c31)) | (~p2(c29, c29)) | p12(f21(c29, c27, c30, c31, c28), f21(c29, c27, c30, c31, c28)))),
% 0.71/0.91 inference(rewrite,[status(thm)],[])).
% 0.71/0.91 tff(89,plain,
% 0.71/0.91 (((~p2(c29, c29)) | (~p12(c28, c28)) | (~p12(c31, c31)) | (~p2(c30, c30)) | (~p2(c27, c27)) | p12(f21(c29, c27, c30, c31, c28), f21(c29, c27, c30, c31, c28))) <=> ((~p2(c30, c30)) | (~p2(c27, c27)) | (~p12(c28, c28)) | (~p12(c31, c31)) | (~p2(c29, c29)) | p12(f21(c29, c27, c30, c31, c28), f21(c29, c27, c30, c31, c28)))),
% 0.71/0.91 inference(rewrite,[status(thm)],[])).
% 0.71/0.91 tff(90,plain,
% 0.71/0.91 (((~![X39: $i, X31: $i, X38: $i, X37: $i, X32: $i, X30: $i, X35: $i, X34: $i, X36: $i, X33: $i] : ((~p2(X30, X35)) | (~p12(X34, X39)) | (~p12(X33, X38)) | (~p2(X32, X37)) | (~p2(X31, X36)) | p12(f21(X30, X31, X32, X33, X34), f21(X35, X36, X37, X38, X39)))) | ((~p2(c29, c29)) | (~p12(c28, c28)) | (~p12(c31, c31)) | (~p2(c30, c30)) | (~p2(c27, c27)) | p12(f21(c29, c27, c30, c31, c28), f21(c29, c27, c30, c31, c28)))) <=> ((~![X39: $i, X31: $i, X38: $i, X37: $i, X32: $i, X30: $i, X35: $i, X34: $i, X36: $i, X33: $i] : ((~p2(X30, X35)) | (~p12(X34, X39)) | (~p12(X33, X38)) | (~p2(X32, X37)) | (~p2(X31, X36)) | p12(f21(X30, X31, X32, X33, X34), f21(X35, X36, X37, X38, X39)))) | ((~p2(c30, c30)) | (~p2(c27, c27)) | (~p12(c28, c28)) | (~p12(c31, c31)) | (~p2(c29, c29)) | p12(f21(c29, c27, c30, c31, c28), f21(c29, c27, c30, c31, c28))))),
% 0.71/0.91 inference(monotonicity,[status(thm)],[89])).
% 0.71/0.91 tff(91,plain,
% 0.71/0.91 (((~![X39: $i, X31: $i, X38: $i, X37: $i, X32: $i, X30: $i, X35: $i, X34: $i, X36: $i, X33: $i] : ((~p2(X30, X35)) | (~p12(X34, X39)) | (~p12(X33, X38)) | (~p2(X32, X37)) | (~p2(X31, X36)) | p12(f21(X30, X31, X32, X33, X34), f21(X35, X36, X37, X38, X39)))) | ((~p2(c29, c29)) | (~p12(c28, c28)) | (~p12(c31, c31)) | (~p2(c30, c30)) | (~p2(c27, c27)) | p12(f21(c29, c27, c30, c31, c28), f21(c29, c27, c30, c31, c28)))) <=> ((~![X39: $i, X31: $i, X38: $i, X37: $i, X32: $i, X30: $i, X35: $i, X34: $i, X36: $i, X33: $i] : ((~p2(X30, X35)) | (~p12(X34, X39)) | (~p12(X33, X38)) | (~p2(X32, X37)) | (~p2(X31, X36)) | p12(f21(X30, X31, X32, X33, X34), f21(X35, X36, X37, X38, X39)))) | (~p2(c30, c30)) | (~p2(c27, c27)) | (~p12(c28, c28)) | (~p12(c31, c31)) | (~p2(c29, c29)) | p12(f21(c29, c27, c30, c31, c28), f21(c29, c27, c30, c31, c28)))),
% 0.71/0.91 inference(transitivity,[status(thm)],[90, 88])).
% 0.71/0.91 tff(92,plain,
% 0.71/0.91 ((~![X39: $i, X31: $i, X38: $i, X37: $i, X32: $i, X30: $i, X35: $i, X34: $i, X36: $i, X33: $i] : ((~p2(X30, X35)) | (~p12(X34, X39)) | (~p12(X33, X38)) | (~p2(X32, X37)) | (~p2(X31, X36)) | p12(f21(X30, X31, X32, X33, X34), f21(X35, X36, X37, X38, X39)))) | ((~p2(c29, c29)) | (~p12(c28, c28)) | (~p12(c31, c31)) | (~p2(c30, c30)) | (~p2(c27, c27)) | p12(f21(c29, c27, c30, c31, c28), f21(c29, c27, c30, c31, c28)))),
% 0.71/0.91 inference(quant_inst,[status(thm)],[])).
% 0.71/0.91 tff(93,plain,
% 0.71/0.91 ((~![X39: $i, X31: $i, X38: $i, X37: $i, X32: $i, X30: $i, X35: $i, X34: $i, X36: $i, X33: $i] : ((~p2(X30, X35)) | (~p12(X34, X39)) | (~p12(X33, X38)) | (~p2(X32, X37)) | (~p2(X31, X36)) | p12(f21(X30, X31, X32, X33, X34), f21(X35, X36, X37, X38, X39)))) | (~p2(c30, c30)) | (~p2(c27, c27)) | (~p12(c28, c28)) | (~p12(c31, c31)) | (~p2(c29, c29)) | p12(f21(c29, c27, c30, c31, c28), f21(c29, c27, c30, c31, c28))),
% 0.71/0.91 inference(modus_ponens,[status(thm)],[92, 91])).
% 0.71/0.91 tff(94,plain,
% 0.71/0.91 ((~p2(c30, c30)) | (~p2(c27, c27)) | (~p12(c28, c28)) | (~p12(c31, c31)) | (~p2(c29, c29)) | p12(f21(c29, c27, c30, c31, c28), f21(c29, c27, c30, c31, c28))),
% 0.71/0.91 inference(unit_resolution,[status(thm)],[93, 87])).
% 0.71/0.91 tff(95,plain,
% 0.71/0.91 ((~p12(c28, c28)) | p12(f21(c29, c27, c30, c31, c28), f21(c29, c27, c30, c31, c28))),
% 0.71/0.91 inference(unit_resolution,[status(thm)],[94, 77, 73, 69, 65])).
% 0.71/0.91 tff(96,plain,
% 0.71/0.91 (p12(f21(c29, c27, c30, c31, c28), f21(c29, c27, c30, c31, c28))),
% 0.71/0.91 inference(unit_resolution,[status(thm)],[95, 54])).
% 0.71/0.91 tff(97,plain,
% 0.71/0.91 (^[X12: $i, X11: $i, X13: $i, X10: $i] : refl(((~p12(X11, X13)) | (~p12(X10, X12)) | p12(f14(X10, X11), f14(X12, X13))) <=> ((~p12(X11, X13)) | (~p12(X10, X12)) | p12(f14(X10, X11), f14(X12, X13))))),
% 0.71/0.91 inference(bind,[status(th)],[])).
% 0.71/0.91 tff(98,plain,
% 0.71/0.91 (![X12: $i, X11: $i, X13: $i, X10: $i] : ((~p12(X11, X13)) | (~p12(X10, X12)) | p12(f14(X10, X11), f14(X12, X13))) <=> ![X12: $i, X11: $i, X13: $i, X10: $i] : ((~p12(X11, X13)) | (~p12(X10, X12)) | p12(f14(X10, X11), f14(X12, X13)))),
% 0.71/0.91 inference(quant_intro,[status(thm)],[97])).
% 0.71/0.91 tff(99,plain,
% 0.71/0.91 (![X12: $i, X11: $i, X13: $i, X10: $i] : ((~p12(X11, X13)) | (~p12(X10, X12)) | p12(f14(X10, X11), f14(X12, X13))) <=> ![X12: $i, X11: $i, X13: $i, X10: $i] : ((~p12(X11, X13)) | (~p12(X10, X12)) | p12(f14(X10, X11), f14(X12, X13)))),
% 0.71/0.91 inference(rewrite,[status(thm)],[])).
% 0.71/0.91 tff(100,plain,
% 0.71/0.91 (^[X12: $i, X11: $i, X13: $i, X10: $i] : trans(monotonicity(rewrite((p12(f14(X10, X11), f14(X12, X13)) | (~p12(X10, X12))) <=> ((~p12(X10, X12)) | p12(f14(X10, X11), f14(X12, X13)))), (((p12(f14(X10, X11), f14(X12, X13)) | (~p12(X10, X12))) | (~p12(X11, X13))) <=> (((~p12(X10, X12)) | p12(f14(X10, X11), f14(X12, X13))) | (~p12(X11, X13))))), rewrite((((~p12(X10, X12)) | p12(f14(X10, X11), f14(X12, X13))) | (~p12(X11, X13))) <=> ((~p12(X11, X13)) | (~p12(X10, X12)) | p12(f14(X10, X11), f14(X12, X13)))), (((p12(f14(X10, X11), f14(X12, X13)) | (~p12(X10, X12))) | (~p12(X11, X13))) <=> ((~p12(X11, X13)) | (~p12(X10, X12)) | p12(f14(X10, X11), f14(X12, X13)))))),
% 0.71/0.91 inference(bind,[status(th)],[])).
% 0.71/0.91 tff(101,plain,
% 0.71/0.91 (![X12: $i, X11: $i, X13: $i, X10: $i] : ((p12(f14(X10, X11), f14(X12, X13)) | (~p12(X10, X12))) | (~p12(X11, X13))) <=> ![X12: $i, X11: $i, X13: $i, X10: $i] : ((~p12(X11, X13)) | (~p12(X10, X12)) | p12(f14(X10, X11), f14(X12, X13)))),
% 0.71/0.91 inference(quant_intro,[status(thm)],[100])).
% 0.71/0.91 tff(102,axiom,(![X12: $i, X11: $i, X13: $i, X10: $i] : ((p12(f14(X10, X11), f14(X12, X13)) | (~p12(X10, X12))) | (~p12(X11, X13)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','p12_28')).
% 0.71/0.91 tff(103,plain,
% 0.71/0.91 (![X12: $i, X11: $i, X13: $i, X10: $i] : ((~p12(X11, X13)) | (~p12(X10, X12)) | p12(f14(X10, X11), f14(X12, X13)))),
% 0.71/0.91 inference(modus_ponens,[status(thm)],[102, 101])).
% 0.71/0.91 tff(104,plain,
% 0.71/0.91 (![X12: $i, X11: $i, X13: $i, X10: $i] : ((~p12(X11, X13)) | (~p12(X10, X12)) | p12(f14(X10, X11), f14(X12, X13)))),
% 0.71/0.91 inference(modus_ponens,[status(thm)],[103, 99])).
% 0.71/0.91 tff(105,plain,(
% 0.71/0.91 ![X12: $i, X11: $i, X13: $i, X10: $i] : ((~p12(X11, X13)) | (~p12(X10, X12)) | p12(f14(X10, X11), f14(X12, X13)))),
% 0.71/0.91 inference(skolemize,[status(sab)],[104])).
% 0.71/0.91 tff(106,plain,
% 0.71/0.91 (![X12: $i, X11: $i, X13: $i, X10: $i] : ((~p12(X11, X13)) | (~p12(X10, X12)) | p12(f14(X10, X11), f14(X12, X13)))),
% 0.71/0.91 inference(modus_ponens,[status(thm)],[105, 98])).
% 0.71/0.91 tff(107,plain,
% 0.71/0.91 (((~![X12: $i, X11: $i, X13: $i, X10: $i] : ((~p12(X11, X13)) | (~p12(X10, X12)) | p12(f14(X10, X11), f14(X12, X13)))) | ((~p12(c31, c31)) | p12(f14(c31, f21(c29, c27, c30, c31, c28)), f14(c31, f21(c29, c27, c30, c31, c28))) | (~p12(f21(c29, c27, c30, c31, c28), f21(c29, c27, c30, c31, c28))))) <=> ((~![X12: $i, X11: $i, X13: $i, X10: $i] : ((~p12(X11, X13)) | (~p12(X10, X12)) | p12(f14(X10, X11), f14(X12, X13)))) | (~p12(c31, c31)) | p12(f14(c31, f21(c29, c27, c30, c31, c28)), f14(c31, f21(c29, c27, c30, c31, c28))) | (~p12(f21(c29, c27, c30, c31, c28), f21(c29, c27, c30, c31, c28))))),
% 0.71/0.91 inference(rewrite,[status(thm)],[])).
% 0.71/0.91 tff(108,plain,
% 0.71/0.91 (((~p12(f21(c29, c27, c30, c31, c28), f21(c29, c27, c30, c31, c28))) | (~p12(c31, c31)) | p12(f14(c31, f21(c29, c27, c30, c31, c28)), f14(c31, f21(c29, c27, c30, c31, c28)))) <=> ((~p12(c31, c31)) | p12(f14(c31, f21(c29, c27, c30, c31, c28)), f14(c31, f21(c29, c27, c30, c31, c28))) | (~p12(f21(c29, c27, c30, c31, c28), f21(c29, c27, c30, c31, c28))))),
% 0.71/0.91 inference(rewrite,[status(thm)],[])).
% 0.71/0.91 tff(109,plain,
% 0.71/0.91 (((~![X12: $i, X11: $i, X13: $i, X10: $i] : ((~p12(X11, X13)) | (~p12(X10, X12)) | p12(f14(X10, X11), f14(X12, X13)))) | ((~p12(f21(c29, c27, c30, c31, c28), f21(c29, c27, c30, c31, c28))) | (~p12(c31, c31)) | p12(f14(c31, f21(c29, c27, c30, c31, c28)), f14(c31, f21(c29, c27, c30, c31, c28))))) <=> ((~![X12: $i, X11: $i, X13: $i, X10: $i] : ((~p12(X11, X13)) | (~p12(X10, X12)) | p12(f14(X10, X11), f14(X12, X13)))) | ((~p12(c31, c31)) | p12(f14(c31, f21(c29, c27, c30, c31, c28)), f14(c31, f21(c29, c27, c30, c31, c28))) | (~p12(f21(c29, c27, c30, c31, c28), f21(c29, c27, c30, c31, c28)))))),
% 0.71/0.91 inference(monotonicity,[status(thm)],[108])).
% 0.71/0.91 tff(110,plain,
% 0.71/0.91 (((~![X12: $i, X11: $i, X13: $i, X10: $i] : ((~p12(X11, X13)) | (~p12(X10, X12)) | p12(f14(X10, X11), f14(X12, X13)))) | ((~p12(f21(c29, c27, c30, c31, c28), f21(c29, c27, c30, c31, c28))) | (~p12(c31, c31)) | p12(f14(c31, f21(c29, c27, c30, c31, c28)), f14(c31, f21(c29, c27, c30, c31, c28))))) <=> ((~![X12: $i, X11: $i, X13: $i, X10: $i] : ((~p12(X11, X13)) | (~p12(X10, X12)) | p12(f14(X10, X11), f14(X12, X13)))) | (~p12(c31, c31)) | p12(f14(c31, f21(c29, c27, c30, c31, c28)), f14(c31, f21(c29, c27, c30, c31, c28))) | (~p12(f21(c29, c27, c30, c31, c28), f21(c29, c27, c30, c31, c28))))),
% 0.71/0.91 inference(transitivity,[status(thm)],[109, 107])).
% 0.71/0.91 tff(111,plain,
% 0.71/0.91 ((~![X12: $i, X11: $i, X13: $i, X10: $i] : ((~p12(X11, X13)) | (~p12(X10, X12)) | p12(f14(X10, X11), f14(X12, X13)))) | ((~p12(f21(c29, c27, c30, c31, c28), f21(c29, c27, c30, c31, c28))) | (~p12(c31, c31)) | p12(f14(c31, f21(c29, c27, c30, c31, c28)), f14(c31, f21(c29, c27, c30, c31, c28))))),
% 0.71/0.91 inference(quant_inst,[status(thm)],[])).
% 0.71/0.91 tff(112,plain,
% 0.71/0.91 ((~![X12: $i, X11: $i, X13: $i, X10: $i] : ((~p12(X11, X13)) | (~p12(X10, X12)) | p12(f14(X10, X11), f14(X12, X13)))) | (~p12(c31, c31)) | p12(f14(c31, f21(c29, c27, c30, c31, c28)), f14(c31, f21(c29, c27, c30, c31, c28))) | (~p12(f21(c29, c27, c30, c31, c28), f21(c29, c27, c30, c31, c28)))),
% 0.71/0.91 inference(modus_ponens,[status(thm)],[111, 110])).
% 0.71/0.91 tff(113,plain,
% 0.71/0.91 ((~p12(c31, c31)) | p12(f14(c31, f21(c29, c27, c30, c31, c28)), f14(c31, f21(c29, c27, c30, c31, c28))) | (~p12(f21(c29, c27, c30, c31, c28), f21(c29, c27, c30, c31, c28)))),
% 0.71/0.91 inference(unit_resolution,[status(thm)],[112, 106])).
% 0.71/0.91 tff(114,plain,
% 0.71/0.91 (p12(f14(c31, f21(c29, c27, c30, c31, c28)), f14(c31, f21(c29, c27, c30, c31, c28))) | (~p12(f21(c29, c27, c30, c31, c28), f21(c29, c27, c30, c31, c28)))),
% 0.71/0.91 inference(unit_resolution,[status(thm)],[113, 73])).
% 0.71/0.91 tff(115,plain,
% 0.71/0.91 (p12(f14(c31, f21(c29, c27, c30, c31, c28)), f14(c31, f21(c29, c27, c30, c31, c28)))),
% 0.71/0.91 inference(unit_resolution,[status(thm)],[114, 96])).
% 0.71/0.91 tff(116,plain,
% 0.71/0.91 (^[X9: $i, X8: $i] : refl(((~p12(X8, X9)) | p12(f13(X8), f13(X9))) <=> ((~p12(X8, X9)) | p12(f13(X8), f13(X9))))),
% 0.71/0.91 inference(bind,[status(th)],[])).
% 0.71/0.91 tff(117,plain,
% 0.71/0.91 (![X9: $i, X8: $i] : ((~p12(X8, X9)) | p12(f13(X8), f13(X9))) <=> ![X9: $i, X8: $i] : ((~p12(X8, X9)) | p12(f13(X8), f13(X9)))),
% 0.71/0.91 inference(quant_intro,[status(thm)],[116])).
% 0.71/0.91 tff(118,plain,
% 0.71/0.91 (![X9: $i, X8: $i] : ((~p12(X8, X9)) | p12(f13(X8), f13(X9))) <=> ![X9: $i, X8: $i] : ((~p12(X8, X9)) | p12(f13(X8), f13(X9)))),
% 0.71/0.91 inference(rewrite,[status(thm)],[])).
% 0.71/0.91 tff(119,plain,
% 0.71/0.91 (^[X9: $i, X8: $i] : rewrite((p12(f13(X8), f13(X9)) | (~p12(X8, X9))) <=> ((~p12(X8, X9)) | p12(f13(X8), f13(X9))))),
% 0.71/0.91 inference(bind,[status(th)],[])).
% 0.71/0.91 tff(120,plain,
% 0.71/0.91 (![X9: $i, X8: $i] : (p12(f13(X8), f13(X9)) | (~p12(X8, X9))) <=> ![X9: $i, X8: $i] : ((~p12(X8, X9)) | p12(f13(X8), f13(X9)))),
% 0.71/0.91 inference(quant_intro,[status(thm)],[119])).
% 0.71/0.91 tff(121,axiom,(![X9: $i, X8: $i] : (p12(f13(X8), f13(X9)) | (~p12(X8, X9)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','p12_12')).
% 0.71/0.91 tff(122,plain,
% 0.71/0.91 (![X9: $i, X8: $i] : ((~p12(X8, X9)) | p12(f13(X8), f13(X9)))),
% 0.71/0.91 inference(modus_ponens,[status(thm)],[121, 120])).
% 0.71/0.91 tff(123,plain,
% 0.71/0.91 (![X9: $i, X8: $i] : ((~p12(X8, X9)) | p12(f13(X8), f13(X9)))),
% 0.71/0.91 inference(modus_ponens,[status(thm)],[122, 118])).
% 0.71/0.91 tff(124,plain,(
% 0.71/0.91 ![X9: $i, X8: $i] : ((~p12(X8, X9)) | p12(f13(X8), f13(X9)))),
% 0.71/0.91 inference(skolemize,[status(sab)],[123])).
% 0.71/0.91 tff(125,plain,
% 0.71/0.91 (![X9: $i, X8: $i] : ((~p12(X8, X9)) | p12(f13(X8), f13(X9)))),
% 0.71/0.91 inference(modus_ponens,[status(thm)],[124, 117])).
% 0.71/0.91 tff(126,plain,
% 0.71/0.91 (((~![X9: $i, X8: $i] : ((~p12(X8, X9)) | p12(f13(X8), f13(X9)))) | ((~p12(f14(c31, f21(c29, c27, c30, c31, c28)), f14(c31, f21(c29, c27, c30, c31, c28)))) | p12(f13(f14(c31, f21(c29, c27, c30, c31, c28))), f13(f14(c31, f21(c29, c27, c30, c31, c28)))))) <=> ((~![X9: $i, X8: $i] : ((~p12(X8, X9)) | p12(f13(X8), f13(X9)))) | (~p12(f14(c31, f21(c29, c27, c30, c31, c28)), f14(c31, f21(c29, c27, c30, c31, c28)))) | p12(f13(f14(c31, f21(c29, c27, c30, c31, c28))), f13(f14(c31, f21(c29, c27, c30, c31, c28)))))),
% 0.71/0.91 inference(rewrite,[status(thm)],[])).
% 0.71/0.91 tff(127,plain,
% 0.71/0.91 ((~![X9: $i, X8: $i] : ((~p12(X8, X9)) | p12(f13(X8), f13(X9)))) | ((~p12(f14(c31, f21(c29, c27, c30, c31, c28)), f14(c31, f21(c29, c27, c30, c31, c28)))) | p12(f13(f14(c31, f21(c29, c27, c30, c31, c28))), f13(f14(c31, f21(c29, c27, c30, c31, c28)))))),
% 0.71/0.91 inference(quant_inst,[status(thm)],[])).
% 0.71/0.91 tff(128,plain,
% 0.71/0.91 ((~![X9: $i, X8: $i] : ((~p12(X8, X9)) | p12(f13(X8), f13(X9)))) | (~p12(f14(c31, f21(c29, c27, c30, c31, c28)), f14(c31, f21(c29, c27, c30, c31, c28)))) | p12(f13(f14(c31, f21(c29, c27, c30, c31, c28))), f13(f14(c31, f21(c29, c27, c30, c31, c28))))),
% 0.71/0.91 inference(modus_ponens,[status(thm)],[127, 126])).
% 0.71/0.91 tff(129,plain,
% 0.71/0.91 ((~p12(f14(c31, f21(c29, c27, c30, c31, c28)), f14(c31, f21(c29, c27, c30, c31, c28)))) | p12(f13(f14(c31, f21(c29, c27, c30, c31, c28))), f13(f14(c31, f21(c29, c27, c30, c31, c28))))),
% 0.71/0.91 inference(unit_resolution,[status(thm)],[128, 125])).
% 0.71/0.91 tff(130,plain,
% 0.71/0.91 (p12(f13(f14(c31, f21(c29, c27, c30, c31, c28))), f13(f14(c31, f21(c29, c27, c30, c31, c28))))),
% 0.71/0.91 inference(unit_resolution,[status(thm)],[129, 115])).
% 0.71/0.91 tff(131,assumption,(~p12(f14(c31, c28), f14(c31, c28))), introduced(assumption)).
% 0.71/0.91 tff(132,plain,
% 0.71/0.91 ((~![X0: $i] : p12(X0, X0)) | p12(f14(c31, c28), f14(c31, c28))),
% 0.71/0.91 inference(quant_inst,[status(thm)],[])).
% 0.71/0.91 tff(133,plain,
% 0.71/0.91 ($false),
% 0.71/0.91 inference(unit_resolution,[status(thm)],[132, 51, 131])).
% 0.71/0.91 tff(134,plain,(p12(f14(c31, c28), f14(c31, c28))), inference(lemma,lemma(discharge,[]))).
% 0.71/0.91 tff(135,plain,
% 0.71/0.91 (((~![X9: $i, X8: $i] : ((~p12(X8, X9)) | p12(f13(X8), f13(X9)))) | ((~p12(f14(c31, c28), f14(c31, c28))) | p12(f13(f14(c31, c28)), f13(f14(c31, c28))))) <=> ((~![X9: $i, X8: $i] : ((~p12(X8, X9)) | p12(f13(X8), f13(X9)))) | (~p12(f14(c31, c28), f14(c31, c28))) | p12(f13(f14(c31, c28)), f13(f14(c31, c28))))),
% 0.71/0.91 inference(rewrite,[status(thm)],[])).
% 0.71/0.91 tff(136,plain,
% 0.71/0.91 ((~![X9: $i, X8: $i] : ((~p12(X8, X9)) | p12(f13(X8), f13(X9)))) | ((~p12(f14(c31, c28), f14(c31, c28))) | p12(f13(f14(c31, c28)), f13(f14(c31, c28))))),
% 0.71/0.91 inference(quant_inst,[status(thm)],[])).
% 0.71/0.91 tff(137,plain,
% 0.71/0.91 ((~![X9: $i, X8: $i] : ((~p12(X8, X9)) | p12(f13(X8), f13(X9)))) | (~p12(f14(c31, c28), f14(c31, c28))) | p12(f13(f14(c31, c28)), f13(f14(c31, c28)))),
% 0.71/0.91 inference(modus_ponens,[status(thm)],[136, 135])).
% 0.71/0.91 tff(138,plain,
% 0.71/0.91 ((~p12(f14(c31, c28), f14(c31, c28))) | p12(f13(f14(c31, c28)), f13(f14(c31, c28)))),
% 0.71/0.91 inference(unit_resolution,[status(thm)],[137, 125])).
% 0.71/0.91 tff(139,plain,
% 0.71/0.91 (p12(f13(f14(c31, c28)), f13(f14(c31, c28)))),
% 0.71/0.91 inference(unit_resolution,[status(thm)],[138, 134])).
% 0.71/0.91 tff(140,plain,
% 0.71/0.91 (p12(f13(f14(c31, c28)), f13(f14(c31, f16(f10(c29, f11(c27, c30)), c32, c31)))) <=> p12(f13(f14(c31, c28)), f13(f14(c31, f16(f10(c29, f11(c27, c30)), c32, c31))))),
% 0.71/0.91 inference(rewrite,[status(thm)],[])).
% 0.71/0.91 tff(141,axiom,(p12(f13(f14(c31, c28)), f13(f14(c31, f16(f10(c29, f11(c27, c30)), c32, c31))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','p12_33')).
% 0.71/0.91 tff(142,plain,
% 0.71/0.91 (p12(f13(f14(c31, c28)), f13(f14(c31, f16(f10(c29, f11(c27, c30)), c32, c31))))),
% 0.71/0.91 inference(modus_ponens,[status(thm)],[141, 140])).
% 0.71/0.91 tff(143,plain,
% 0.71/0.91 (^[X0: $i, X2: $i, X1: $i] : refl((p12(X1, X2) | (~p12(X0, X2)) | (~p12(X0, X1))) <=> (p12(X1, X2) | (~p12(X0, X2)) | (~p12(X0, X1))))),
% 0.71/0.91 inference(bind,[status(th)],[])).
% 0.71/0.91 tff(144,plain,
% 0.71/0.91 (![X0: $i, X2: $i, X1: $i] : (p12(X1, X2) | (~p12(X0, X2)) | (~p12(X0, X1))) <=> ![X0: $i, X2: $i, X1: $i] : (p12(X1, X2) | (~p12(X0, X2)) | (~p12(X0, X1)))),
% 0.71/0.91 inference(quant_intro,[status(thm)],[143])).
% 0.71/0.91 tff(145,plain,
% 0.71/0.91 (![X0: $i, X2: $i, X1: $i] : (p12(X1, X2) | (~p12(X0, X2)) | (~p12(X0, X1))) <=> ![X0: $i, X2: $i, X1: $i] : (p12(X1, X2) | (~p12(X0, X2)) | (~p12(X0, X1)))),
% 0.71/0.91 inference(rewrite,[status(thm)],[])).
% 0.71/0.91 tff(146,plain,
% 0.71/0.91 (^[X0: $i, X2: $i, X1: $i] : trans(monotonicity(rewrite((p12(X1, X2) | (~p12(X0, X1))) <=> (p12(X1, X2) | (~p12(X0, X1)))), (((p12(X1, X2) | (~p12(X0, X1))) | (~p12(X0, X2))) <=> ((p12(X1, X2) | (~p12(X0, X1))) | (~p12(X0, X2))))), rewrite(((p12(X1, X2) | (~p12(X0, X1))) | (~p12(X0, X2))) <=> (p12(X1, X2) | (~p12(X0, X2)) | (~p12(X0, X1)))), (((p12(X1, X2) | (~p12(X0, X1))) | (~p12(X0, X2))) <=> (p12(X1, X2) | (~p12(X0, X2)) | (~p12(X0, X1)))))),
% 0.71/0.91 inference(bind,[status(th)],[])).
% 0.71/0.91 tff(147,plain,
% 0.71/0.91 (![X0: $i, X2: $i, X1: $i] : ((p12(X1, X2) | (~p12(X0, X1))) | (~p12(X0, X2))) <=> ![X0: $i, X2: $i, X1: $i] : (p12(X1, X2) | (~p12(X0, X2)) | (~p12(X0, X1)))),
% 0.71/0.92 inference(quant_intro,[status(thm)],[146])).
% 0.71/0.92 tff(148,axiom,(![X0: $i, X2: $i, X1: $i] : ((p12(X1, X2) | (~p12(X0, X1))) | (~p12(X0, X2)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','p12_17')).
% 0.71/0.92 tff(149,plain,
% 0.71/0.92 (![X0: $i, X2: $i, X1: $i] : (p12(X1, X2) | (~p12(X0, X2)) | (~p12(X0, X1)))),
% 0.71/0.92 inference(modus_ponens,[status(thm)],[148, 147])).
% 0.71/0.92 tff(150,plain,
% 0.71/0.92 (![X0: $i, X2: $i, X1: $i] : (p12(X1, X2) | (~p12(X0, X2)) | (~p12(X0, X1)))),
% 0.71/0.92 inference(modus_ponens,[status(thm)],[149, 145])).
% 0.71/0.92 tff(151,plain,(
% 0.71/0.92 ![X0: $i, X2: $i, X1: $i] : (p12(X1, X2) | (~p12(X0, X2)) | (~p12(X0, X1)))),
% 0.71/0.92 inference(skolemize,[status(sab)],[150])).
% 0.71/0.92 tff(152,plain,
% 0.71/0.92 (![X0: $i, X2: $i, X1: $i] : (p12(X1, X2) | (~p12(X0, X2)) | (~p12(X0, X1)))),
% 0.71/0.92 inference(modus_ponens,[status(thm)],[151, 144])).
% 0.71/0.92 tff(153,plain,
% 0.71/0.92 (((~![X0: $i, X2: $i, X1: $i] : (p12(X1, X2) | (~p12(X0, X2)) | (~p12(X0, X1)))) | (p12(f13(f14(c31, f16(f10(c29, f11(c27, c30)), c32, c31))), f13(f14(c31, c28))) | (~p12(f13(f14(c31, c28)), f13(f14(c31, f16(f10(c29, f11(c27, c30)), c32, c31))))) | (~p12(f13(f14(c31, c28)), f13(f14(c31, c28)))))) <=> ((~![X0: $i, X2: $i, X1: $i] : (p12(X1, X2) | (~p12(X0, X2)) | (~p12(X0, X1)))) | p12(f13(f14(c31, f16(f10(c29, f11(c27, c30)), c32, c31))), f13(f14(c31, c28))) | (~p12(f13(f14(c31, c28)), f13(f14(c31, f16(f10(c29, f11(c27, c30)), c32, c31))))) | (~p12(f13(f14(c31, c28)), f13(f14(c31, c28)))))),
% 0.71/0.92 inference(rewrite,[status(thm)],[])).
% 0.71/0.92 tff(154,plain,
% 0.71/0.92 ((p12(f13(f14(c31, f16(f10(c29, f11(c27, c30)), c32, c31))), f13(f14(c31, c28))) | (~p12(f13(f14(c31, c28)), f13(f14(c31, c28)))) | (~p12(f13(f14(c31, c28)), f13(f14(c31, f16(f10(c29, f11(c27, c30)), c32, c31)))))) <=> (p12(f13(f14(c31, f16(f10(c29, f11(c27, c30)), c32, c31))), f13(f14(c31, c28))) | (~p12(f13(f14(c31, c28)), f13(f14(c31, f16(f10(c29, f11(c27, c30)), c32, c31))))) | (~p12(f13(f14(c31, c28)), f13(f14(c31, c28)))))),
% 0.71/0.92 inference(rewrite,[status(thm)],[])).
% 0.71/0.92 tff(155,plain,
% 0.71/0.92 (((~![X0: $i, X2: $i, X1: $i] : (p12(X1, X2) | (~p12(X0, X2)) | (~p12(X0, X1)))) | (p12(f13(f14(c31, f16(f10(c29, f11(c27, c30)), c32, c31))), f13(f14(c31, c28))) | (~p12(f13(f14(c31, c28)), f13(f14(c31, c28)))) | (~p12(f13(f14(c31, c28)), f13(f14(c31, f16(f10(c29, f11(c27, c30)), c32, c31))))))) <=> ((~![X0: $i, X2: $i, X1: $i] : (p12(X1, X2) | (~p12(X0, X2)) | (~p12(X0, X1)))) | (p12(f13(f14(c31, f16(f10(c29, f11(c27, c30)), c32, c31))), f13(f14(c31, c28))) | (~p12(f13(f14(c31, c28)), f13(f14(c31, f16(f10(c29, f11(c27, c30)), c32, c31))))) | (~p12(f13(f14(c31, c28)), f13(f14(c31, c28))))))),
% 0.71/0.92 inference(monotonicity,[status(thm)],[154])).
% 0.71/0.92 tff(156,plain,
% 0.71/0.92 (((~![X0: $i, X2: $i, X1: $i] : (p12(X1, X2) | (~p12(X0, X2)) | (~p12(X0, X1)))) | (p12(f13(f14(c31, f16(f10(c29, f11(c27, c30)), c32, c31))), f13(f14(c31, c28))) | (~p12(f13(f14(c31, c28)), f13(f14(c31, c28)))) | (~p12(f13(f14(c31, c28)), f13(f14(c31, f16(f10(c29, f11(c27, c30)), c32, c31))))))) <=> ((~![X0: $i, X2: $i, X1: $i] : (p12(X1, X2) | (~p12(X0, X2)) | (~p12(X0, X1)))) | p12(f13(f14(c31, f16(f10(c29, f11(c27, c30)), c32, c31))), f13(f14(c31, c28))) | (~p12(f13(f14(c31, c28)), f13(f14(c31, f16(f10(c29, f11(c27, c30)), c32, c31))))) | (~p12(f13(f14(c31, c28)), f13(f14(c31, c28)))))),
% 0.71/0.92 inference(transitivity,[status(thm)],[155, 153])).
% 0.71/0.92 tff(157,plain,
% 0.71/0.92 ((~![X0: $i, X2: $i, X1: $i] : (p12(X1, X2) | (~p12(X0, X2)) | (~p12(X0, X1)))) | (p12(f13(f14(c31, f16(f10(c29, f11(c27, c30)), c32, c31))), f13(f14(c31, c28))) | (~p12(f13(f14(c31, c28)), f13(f14(c31, c28)))) | (~p12(f13(f14(c31, c28)), f13(f14(c31, f16(f10(c29, f11(c27, c30)), c32, c31))))))),
% 0.71/0.92 inference(quant_inst,[status(thm)],[])).
% 0.71/0.92 tff(158,plain,
% 0.71/0.92 ((~![X0: $i, X2: $i, X1: $i] : (p12(X1, X2) | (~p12(X0, X2)) | (~p12(X0, X1)))) | p12(f13(f14(c31, f16(f10(c29, f11(c27, c30)), c32, c31))), f13(f14(c31, c28))) | (~p12(f13(f14(c31, c28)), f13(f14(c31, f16(f10(c29, f11(c27, c30)), c32, c31))))) | (~p12(f13(f14(c31, c28)), f13(f14(c31, c28))))),
% 0.71/0.92 inference(modus_ponens,[status(thm)],[157, 156])).
% 0.71/0.92 tff(159,plain,
% 0.71/0.92 (p12(f13(f14(c31, f16(f10(c29, f11(c27, c30)), c32, c31))), f13(f14(c31, c28)))),
% 0.71/0.92 inference(unit_resolution,[status(thm)],[158, 152, 142, 139])).
% 0.71/0.92 tff(160,plain,
% 0.71/0.92 (^[X6: $i, X4: $i, X3: $i, X7: $i, X5: $i] : refl(((~p22(f3(f4(f5(c26))), X5)) | (~p23(X3, f8(f10(X4, f11(X5, X6))))) | (~p24(f17(f10(X4, f11(X5, X6)), X3))) | p12(X3, f16(f10(X4, f11(X5, X6)), c32, X7)) | (~p25(f13(f14(X7, X3)), f13(f14(X7, f21(X4, X5, X6, X7, X3)))))) <=> ((~p22(f3(f4(f5(c26))), X5)) | (~p23(X3, f8(f10(X4, f11(X5, X6))))) | (~p24(f17(f10(X4, f11(X5, X6)), X3))) | p12(X3, f16(f10(X4, f11(X5, X6)), c32, X7)) | (~p25(f13(f14(X7, X3)), f13(f14(X7, f21(X4, X5, X6, X7, X3)))))))),
% 0.71/0.92 inference(bind,[status(th)],[])).
% 0.71/0.92 tff(161,plain,
% 0.71/0.92 (![X6: $i, X4: $i, X3: $i, X7: $i, X5: $i] : ((~p22(f3(f4(f5(c26))), X5)) | (~p23(X3, f8(f10(X4, f11(X5, X6))))) | (~p24(f17(f10(X4, f11(X5, X6)), X3))) | p12(X3, f16(f10(X4, f11(X5, X6)), c32, X7)) | (~p25(f13(f14(X7, X3)), f13(f14(X7, f21(X4, X5, X6, X7, X3)))))) <=> ![X6: $i, X4: $i, X3: $i, X7: $i, X5: $i] : ((~p22(f3(f4(f5(c26))), X5)) | (~p23(X3, f8(f10(X4, f11(X5, X6))))) | (~p24(f17(f10(X4, f11(X5, X6)), X3))) | p12(X3, f16(f10(X4, f11(X5, X6)), c32, X7)) | (~p25(f13(f14(X7, X3)), f13(f14(X7, f21(X4, X5, X6, X7, X3))))))),
% 0.71/0.92 inference(quant_intro,[status(thm)],[160])).
% 0.71/0.92 tff(162,plain,
% 0.71/0.92 (![X6: $i, X4: $i, X3: $i, X7: $i, X5: $i] : ((~p22(f3(f4(f5(c26))), X5)) | (~p23(X3, f8(f10(X4, f11(X5, X6))))) | (~p24(f17(f10(X4, f11(X5, X6)), X3))) | p12(X3, f16(f10(X4, f11(X5, X6)), c32, X7)) | (~p25(f13(f14(X7, X3)), f13(f14(X7, f21(X4, X5, X6, X7, X3)))))) <=> ![X6: $i, X4: $i, X3: $i, X7: $i, X5: $i] : ((~p22(f3(f4(f5(c26))), X5)) | (~p23(X3, f8(f10(X4, f11(X5, X6))))) | (~p24(f17(f10(X4, f11(X5, X6)), X3))) | p12(X3, f16(f10(X4, f11(X5, X6)), c32, X7)) | (~p25(f13(f14(X7, X3)), f13(f14(X7, f21(X4, X5, X6, X7, X3))))))),
% 0.71/0.92 inference(rewrite,[status(thm)],[])).
% 0.71/0.92 tff(163,plain,
% 0.71/0.92 (^[X6: $i, X4: $i, X3: $i, X7: $i, X5: $i] : trans(monotonicity(trans(monotonicity(trans(monotonicity(rewrite((p12(X3, f16(f10(X4, f11(X5, X6)), c32, X7)) | (~p22(f3(f4(f5(c26))), X5))) <=> ((~p22(f3(f4(f5(c26))), X5)) | p12(X3, f16(f10(X4, f11(X5, X6)), c32, X7)))), (((p12(X3, f16(f10(X4, f11(X5, X6)), c32, X7)) | (~p22(f3(f4(f5(c26))), X5))) | (~p24(f17(f10(X4, f11(X5, X6)), X3)))) <=> (((~p22(f3(f4(f5(c26))), X5)) | p12(X3, f16(f10(X4, f11(X5, X6)), c32, X7))) | (~p24(f17(f10(X4, f11(X5, X6)), X3)))))), rewrite((((~p22(f3(f4(f5(c26))), X5)) | p12(X3, f16(f10(X4, f11(X5, X6)), c32, X7))) | (~p24(f17(f10(X4, f11(X5, X6)), X3)))) <=> ((~p22(f3(f4(f5(c26))), X5)) | (~p24(f17(f10(X4, f11(X5, X6)), X3))) | p12(X3, f16(f10(X4, f11(X5, X6)), c32, X7)))), (((p12(X3, f16(f10(X4, f11(X5, X6)), c32, X7)) | (~p22(f3(f4(f5(c26))), X5))) | (~p24(f17(f10(X4, f11(X5, X6)), X3)))) <=> ((~p22(f3(f4(f5(c26))), X5)) | (~p24(f17(f10(X4, f11(X5, X6)), X3))) | p12(X3, f16(f10(X4, f11(X5, X6)), c32, X7))))), ((((p12(X3, f16(f10(X4, f11(X5, X6)), c32, X7)) | (~p22(f3(f4(f5(c26))), X5))) | (~p24(f17(f10(X4, f11(X5, X6)), X3)))) | (~p23(X3, f8(f10(X4, f11(X5, X6)))))) <=> (((~p22(f3(f4(f5(c26))), X5)) | (~p24(f17(f10(X4, f11(X5, X6)), X3))) | p12(X3, f16(f10(X4, f11(X5, X6)), c32, X7))) | (~p23(X3, f8(f10(X4, f11(X5, X6)))))))), rewrite((((~p22(f3(f4(f5(c26))), X5)) | (~p24(f17(f10(X4, f11(X5, X6)), X3))) | p12(X3, f16(f10(X4, f11(X5, X6)), c32, X7))) | (~p23(X3, f8(f10(X4, f11(X5, X6)))))) <=> ((~p22(f3(f4(f5(c26))), X5)) | (~p23(X3, f8(f10(X4, f11(X5, X6))))) | (~p24(f17(f10(X4, f11(X5, X6)), X3))) | p12(X3, f16(f10(X4, f11(X5, X6)), c32, X7)))), ((((p12(X3, f16(f10(X4, f11(X5, X6)), c32, X7)) | (~p22(f3(f4(f5(c26))), X5))) | (~p24(f17(f10(X4, f11(X5, X6)), X3)))) | (~p23(X3, f8(f10(X4, f11(X5, X6)))))) <=> ((~p22(f3(f4(f5(c26))), X5)) | (~p23(X3, f8(f10(X4, f11(X5, X6))))) | (~p24(f17(f10(X4, f11(X5, X6)), X3))) | p12(X3, f16(f10(X4, f11(X5, X6)), c32, X7))))), (((((p12(X3, f16(f10(X4, f11(X5, X6)), c32, X7)) | (~p22(f3(f4(f5(c26))), X5))) | (~p24(f17(f10(X4, f11(X5, X6)), X3)))) | (~p23(X3, f8(f10(X4, f11(X5, X6)))))) | (~p25(f13(f14(X7, X3)), f13(f14(X7, f21(X4, X5, X6, X7, X3)))))) <=> (((~p22(f3(f4(f5(c26))), X5)) | (~p23(X3, f8(f10(X4, f11(X5, X6))))) | (~p24(f17(f10(X4, f11(X5, X6)), X3))) | p12(X3, f16(f10(X4, f11(X5, X6)), c32, X7))) | (~p25(f13(f14(X7, X3)), f13(f14(X7, f21(X4, X5, X6, X7, X3)))))))), rewrite((((~p22(f3(f4(f5(c26))), X5)) | (~p23(X3, f8(f10(X4, f11(X5, X6))))) | (~p24(f17(f10(X4, f11(X5, X6)), X3))) | p12(X3, f16(f10(X4, f11(X5, X6)), c32, X7))) | (~p25(f13(f14(X7, X3)), f13(f14(X7, f21(X4, X5, X6, X7, X3)))))) <=> ((~p22(f3(f4(f5(c26))), X5)) | (~p23(X3, f8(f10(X4, f11(X5, X6))))) | (~p24(f17(f10(X4, f11(X5, X6)), X3))) | p12(X3, f16(f10(X4, f11(X5, X6)), c32, X7)) | (~p25(f13(f14(X7, X3)), f13(f14(X7, f21(X4, X5, X6, X7, X3))))))), (((((p12(X3, f16(f10(X4, f11(X5, X6)), c32, X7)) | (~p22(f3(f4(f5(c26))), X5))) | (~p24(f17(f10(X4, f11(X5, X6)), X3)))) | (~p23(X3, f8(f10(X4, f11(X5, X6)))))) | (~p25(f13(f14(X7, X3)), f13(f14(X7, f21(X4, X5, X6, X7, X3)))))) <=> ((~p22(f3(f4(f5(c26))), X5)) | (~p23(X3, f8(f10(X4, f11(X5, X6))))) | (~p24(f17(f10(X4, f11(X5, X6)), X3))) | p12(X3, f16(f10(X4, f11(X5, X6)), c32, X7)) | (~p25(f13(f14(X7, X3)), f13(f14(X7, f21(X4, X5, X6, X7, X3))))))))),
% 0.71/0.92 inference(bind,[status(th)],[])).
% 0.71/0.92 tff(164,plain,
% 0.71/0.92 (![X6: $i, X4: $i, X3: $i, X7: $i, X5: $i] : ((((p12(X3, f16(f10(X4, f11(X5, X6)), c32, X7)) | (~p22(f3(f4(f5(c26))), X5))) | (~p24(f17(f10(X4, f11(X5, X6)), X3)))) | (~p23(X3, f8(f10(X4, f11(X5, X6)))))) | (~p25(f13(f14(X7, X3)), f13(f14(X7, f21(X4, X5, X6, X7, X3)))))) <=> ![X6: $i, X4: $i, X3: $i, X7: $i, X5: $i] : ((~p22(f3(f4(f5(c26))), X5)) | (~p23(X3, f8(f10(X4, f11(X5, X6))))) | (~p24(f17(f10(X4, f11(X5, X6)), X3))) | p12(X3, f16(f10(X4, f11(X5, X6)), c32, X7)) | (~p25(f13(f14(X7, X3)), f13(f14(X7, f21(X4, X5, X6, X7, X3))))))),
% 0.71/0.92 inference(quant_intro,[status(thm)],[163])).
% 0.71/0.92 tff(165,axiom,(![X6: $i, X4: $i, X3: $i, X7: $i, X5: $i] : ((((p12(X3, f16(f10(X4, f11(X5, X6)), c32, X7)) | (~p22(f3(f4(f5(c26))), X5))) | (~p24(f17(f10(X4, f11(X5, X6)), X3)))) | (~p23(X3, f8(f10(X4, f11(X5, X6)))))) | (~p25(f13(f14(X7, X3)), f13(f14(X7, f21(X4, X5, X6, X7, X3))))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','p12_40')).
% 0.71/0.92 tff(166,plain,
% 0.71/0.92 (![X6: $i, X4: $i, X3: $i, X7: $i, X5: $i] : ((~p22(f3(f4(f5(c26))), X5)) | (~p23(X3, f8(f10(X4, f11(X5, X6))))) | (~p24(f17(f10(X4, f11(X5, X6)), X3))) | p12(X3, f16(f10(X4, f11(X5, X6)), c32, X7)) | (~p25(f13(f14(X7, X3)), f13(f14(X7, f21(X4, X5, X6, X7, X3))))))),
% 0.71/0.92 inference(modus_ponens,[status(thm)],[165, 164])).
% 0.71/0.92 tff(167,plain,
% 0.71/0.92 (![X6: $i, X4: $i, X3: $i, X7: $i, X5: $i] : ((~p22(f3(f4(f5(c26))), X5)) | (~p23(X3, f8(f10(X4, f11(X5, X6))))) | (~p24(f17(f10(X4, f11(X5, X6)), X3))) | p12(X3, f16(f10(X4, f11(X5, X6)), c32, X7)) | (~p25(f13(f14(X7, X3)), f13(f14(X7, f21(X4, X5, X6, X7, X3))))))),
% 0.71/0.92 inference(modus_ponens,[status(thm)],[166, 162])).
% 0.71/0.92 tff(168,plain,(
% 0.71/0.92 ![X6: $i, X4: $i, X3: $i, X7: $i, X5: $i] : ((~p22(f3(f4(f5(c26))), X5)) | (~p23(X3, f8(f10(X4, f11(X5, X6))))) | (~p24(f17(f10(X4, f11(X5, X6)), X3))) | p12(X3, f16(f10(X4, f11(X5, X6)), c32, X7)) | (~p25(f13(f14(X7, X3)), f13(f14(X7, f21(X4, X5, X6, X7, X3))))))),
% 0.71/0.92 inference(skolemize,[status(sab)],[167])).
% 0.71/0.92 tff(169,plain,
% 0.71/0.92 (![X6: $i, X4: $i, X3: $i, X7: $i, X5: $i] : ((~p22(f3(f4(f5(c26))), X5)) | (~p23(X3, f8(f10(X4, f11(X5, X6))))) | (~p24(f17(f10(X4, f11(X5, X6)), X3))) | p12(X3, f16(f10(X4, f11(X5, X6)), c32, X7)) | (~p25(f13(f14(X7, X3)), f13(f14(X7, f21(X4, X5, X6, X7, X3))))))),
% 0.71/0.92 inference(modus_ponens,[status(thm)],[168, 161])).
% 0.71/0.92 tff(170,plain,
% 0.71/0.92 (((~![X6: $i, X4: $i, X3: $i, X7: $i, X5: $i] : ((~p22(f3(f4(f5(c26))), X5)) | (~p23(X3, f8(f10(X4, f11(X5, X6))))) | (~p24(f17(f10(X4, f11(X5, X6)), X3))) | p12(X3, f16(f10(X4, f11(X5, X6)), c32, X7)) | (~p25(f13(f14(X7, X3)), f13(f14(X7, f21(X4, X5, X6, X7, X3))))))) | (p12(c28, f16(f10(c29, f11(c27, c30)), c32, c31)) | (~p22(f3(f4(f5(c26))), c27)) | (~p23(c28, f8(f10(c29, f11(c27, c30))))) | (~p25(f13(f14(c31, c28)), f13(f14(c31, f21(c29, c27, c30, c31, c28))))) | (~p24(f17(f10(c29, f11(c27, c30)), c28))))) <=> ((~![X6: $i, X4: $i, X3: $i, X7: $i, X5: $i] : ((~p22(f3(f4(f5(c26))), X5)) | (~p23(X3, f8(f10(X4, f11(X5, X6))))) | (~p24(f17(f10(X4, f11(X5, X6)), X3))) | p12(X3, f16(f10(X4, f11(X5, X6)), c32, X7)) | (~p25(f13(f14(X7, X3)), f13(f14(X7, f21(X4, X5, X6, X7, X3))))))) | p12(c28, f16(f10(c29, f11(c27, c30)), c32, c31)) | (~p22(f3(f4(f5(c26))), c27)) | (~p23(c28, f8(f10(c29, f11(c27, c30))))) | (~p25(f13(f14(c31, c28)), f13(f14(c31, f21(c29, c27, c30, c31, c28))))) | (~p24(f17(f10(c29, f11(c27, c30)), c28))))),
% 0.71/0.92 inference(rewrite,[status(thm)],[])).
% 0.71/0.92 tff(171,plain,
% 0.71/0.92 (((~p22(f3(f4(f5(c26))), c27)) | (~p23(c28, f8(f10(c29, f11(c27, c30))))) | (~p24(f17(f10(c29, f11(c27, c30)), c28))) | p12(c28, f16(f10(c29, f11(c27, c30)), c32, c31)) | (~p25(f13(f14(c31, c28)), f13(f14(c31, f21(c29, c27, c30, c31, c28)))))) <=> (p12(c28, f16(f10(c29, f11(c27, c30)), c32, c31)) | (~p22(f3(f4(f5(c26))), c27)) | (~p23(c28, f8(f10(c29, f11(c27, c30))))) | (~p25(f13(f14(c31, c28)), f13(f14(c31, f21(c29, c27, c30, c31, c28))))) | (~p24(f17(f10(c29, f11(c27, c30)), c28))))),
% 0.71/0.92 inference(rewrite,[status(thm)],[])).
% 0.71/0.92 tff(172,plain,
% 0.71/0.92 (((~![X6: $i, X4: $i, X3: $i, X7: $i, X5: $i] : ((~p22(f3(f4(f5(c26))), X5)) | (~p23(X3, f8(f10(X4, f11(X5, X6))))) | (~p24(f17(f10(X4, f11(X5, X6)), X3))) | p12(X3, f16(f10(X4, f11(X5, X6)), c32, X7)) | (~p25(f13(f14(X7, X3)), f13(f14(X7, f21(X4, X5, X6, X7, X3))))))) | ((~p22(f3(f4(f5(c26))), c27)) | (~p23(c28, f8(f10(c29, f11(c27, c30))))) | (~p24(f17(f10(c29, f11(c27, c30)), c28))) | p12(c28, f16(f10(c29, f11(c27, c30)), c32, c31)) | (~p25(f13(f14(c31, c28)), f13(f14(c31, f21(c29, c27, c30, c31, c28))))))) <=> ((~![X6: $i, X4: $i, X3: $i, X7: $i, X5: $i] : ((~p22(f3(f4(f5(c26))), X5)) | (~p23(X3, f8(f10(X4, f11(X5, X6))))) | (~p24(f17(f10(X4, f11(X5, X6)), X3))) | p12(X3, f16(f10(X4, f11(X5, X6)), c32, X7)) | (~p25(f13(f14(X7, X3)), f13(f14(X7, f21(X4, X5, X6, X7, X3))))))) | (p12(c28, f16(f10(c29, f11(c27, c30)), c32, c31)) | (~p22(f3(f4(f5(c26))), c27)) | (~p23(c28, f8(f10(c29, f11(c27, c30))))) | (~p25(f13(f14(c31, c28)), f13(f14(c31, f21(c29, c27, c30, c31, c28))))) | (~p24(f17(f10(c29, f11(c27, c30)), c28)))))),
% 0.71/0.92 inference(monotonicity,[status(thm)],[171])).
% 0.71/0.92 tff(173,plain,
% 0.71/0.92 (((~![X6: $i, X4: $i, X3: $i, X7: $i, X5: $i] : ((~p22(f3(f4(f5(c26))), X5)) | (~p23(X3, f8(f10(X4, f11(X5, X6))))) | (~p24(f17(f10(X4, f11(X5, X6)), X3))) | p12(X3, f16(f10(X4, f11(X5, X6)), c32, X7)) | (~p25(f13(f14(X7, X3)), f13(f14(X7, f21(X4, X5, X6, X7, X3))))))) | ((~p22(f3(f4(f5(c26))), c27)) | (~p23(c28, f8(f10(c29, f11(c27, c30))))) | (~p24(f17(f10(c29, f11(c27, c30)), c28))) | p12(c28, f16(f10(c29, f11(c27, c30)), c32, c31)) | (~p25(f13(f14(c31, c28)), f13(f14(c31, f21(c29, c27, c30, c31, c28))))))) <=> ((~![X6: $i, X4: $i, X3: $i, X7: $i, X5: $i] : ((~p22(f3(f4(f5(c26))), X5)) | (~p23(X3, f8(f10(X4, f11(X5, X6))))) | (~p24(f17(f10(X4, f11(X5, X6)), X3))) | p12(X3, f16(f10(X4, f11(X5, X6)), c32, X7)) | (~p25(f13(f14(X7, X3)), f13(f14(X7, f21(X4, X5, X6, X7, X3))))))) | p12(c28, f16(f10(c29, f11(c27, c30)), c32, c31)) | (~p22(f3(f4(f5(c26))), c27)) | (~p23(c28, f8(f10(c29, f11(c27, c30))))) | (~p25(f13(f14(c31, c28)), f13(f14(c31, f21(c29, c27, c30, c31, c28))))) | (~p24(f17(f10(c29, f11(c27, c30)), c28))))),
% 0.71/0.92 inference(transitivity,[status(thm)],[172, 170])).
% 0.71/0.92 tff(174,plain,
% 0.71/0.92 ((~![X6: $i, X4: $i, X3: $i, X7: $i, X5: $i] : ((~p22(f3(f4(f5(c26))), X5)) | (~p23(X3, f8(f10(X4, f11(X5, X6))))) | (~p24(f17(f10(X4, f11(X5, X6)), X3))) | p12(X3, f16(f10(X4, f11(X5, X6)), c32, X7)) | (~p25(f13(f14(X7, X3)), f13(f14(X7, f21(X4, X5, X6, X7, X3))))))) | ((~p22(f3(f4(f5(c26))), c27)) | (~p23(c28, f8(f10(c29, f11(c27, c30))))) | (~p24(f17(f10(c29, f11(c27, c30)), c28))) | p12(c28, f16(f10(c29, f11(c27, c30)), c32, c31)) | (~p25(f13(f14(c31, c28)), f13(f14(c31, f21(c29, c27, c30, c31, c28))))))),
% 0.71/0.92 inference(quant_inst,[status(thm)],[])).
% 0.71/0.92 tff(175,plain,
% 0.71/0.92 ((~![X6: $i, X4: $i, X3: $i, X7: $i, X5: $i] : ((~p22(f3(f4(f5(c26))), X5)) | (~p23(X3, f8(f10(X4, f11(X5, X6))))) | (~p24(f17(f10(X4, f11(X5, X6)), X3))) | p12(X3, f16(f10(X4, f11(X5, X6)), c32, X7)) | (~p25(f13(f14(X7, X3)), f13(f14(X7, f21(X4, X5, X6, X7, X3))))))) | p12(c28, f16(f10(c29, f11(c27, c30)), c32, c31)) | (~p22(f3(f4(f5(c26))), c27)) | (~p23(c28, f8(f10(c29, f11(c27, c30))))) | (~p25(f13(f14(c31, c28)), f13(f14(c31, f21(c29, c27, c30, c31, c28))))) | (~p24(f17(f10(c29, f11(c27, c30)), c28)))),
% 0.71/0.92 inference(modus_ponens,[status(thm)],[174, 173])).
% 0.71/0.92 tff(176,plain,
% 0.71/0.92 (~p25(f13(f14(c31, c28)), f13(f14(c31, f21(c29, c27, c30, c31, c28))))),
% 0.71/0.92 inference(unit_resolution,[status(thm)],[175, 22, 19, 16, 13, 169])).
% 0.71/0.92 tff(177,plain,
% 0.71/0.92 (^[X67: $i, X68: $i, X66: $i, X69: $i] : refl(((~p12(X68, X66)) | (~p25(X68, X69)) | (~p12(X69, X67)) | p25(X66, X67)) <=> ((~p12(X68, X66)) | (~p25(X68, X69)) | (~p12(X69, X67)) | p25(X66, X67)))),
% 0.71/0.92 inference(bind,[status(th)],[])).
% 0.71/0.92 tff(178,plain,
% 0.71/0.92 (![X67: $i, X68: $i, X66: $i, X69: $i] : ((~p12(X68, X66)) | (~p25(X68, X69)) | (~p12(X69, X67)) | p25(X66, X67)) <=> ![X67: $i, X68: $i, X66: $i, X69: $i] : ((~p12(X68, X66)) | (~p25(X68, X69)) | (~p12(X69, X67)) | p25(X66, X67))),
% 0.71/0.92 inference(quant_intro,[status(thm)],[177])).
% 0.71/0.92 tff(179,plain,
% 0.71/0.92 (![X67: $i, X68: $i, X66: $i, X69: $i] : ((~p12(X68, X66)) | (~p25(X68, X69)) | (~p12(X69, X67)) | p25(X66, X67)) <=> ![X67: $i, X68: $i, X66: $i, X69: $i] : ((~p12(X68, X66)) | (~p25(X68, X69)) | (~p12(X69, X67)) | p25(X66, X67))),
% 0.71/0.92 inference(rewrite,[status(thm)],[])).
% 0.71/0.92 tff(180,plain,
% 0.71/0.92 (^[X67: $i, X68: $i, X66: $i, X69: $i] : trans(monotonicity(trans(monotonicity(rewrite((p25(X66, X67) | (~p12(X69, X67))) <=> ((~p12(X69, X67)) | p25(X66, X67))), (((p25(X66, X67) | (~p12(X69, X67))) | (~p25(X68, X69))) <=> (((~p12(X69, X67)) | p25(X66, X67)) | (~p25(X68, X69))))), rewrite((((~p12(X69, X67)) | p25(X66, X67)) | (~p25(X68, X69))) <=> ((~p25(X68, X69)) | (~p12(X69, X67)) | p25(X66, X67))), (((p25(X66, X67) | (~p12(X69, X67))) | (~p25(X68, X69))) <=> ((~p25(X68, X69)) | (~p12(X69, X67)) | p25(X66, X67)))), ((((p25(X66, X67) | (~p12(X69, X67))) | (~p25(X68, X69))) | (~p12(X68, X66))) <=> (((~p25(X68, X69)) | (~p12(X69, X67)) | p25(X66, X67)) | (~p12(X68, X66))))), rewrite((((~p25(X68, X69)) | (~p12(X69, X67)) | p25(X66, X67)) | (~p12(X68, X66))) <=> ((~p12(X68, X66)) | (~p25(X68, X69)) | (~p12(X69, X67)) | p25(X66, X67))), ((((p25(X66, X67) | (~p12(X69, X67))) | (~p25(X68, X69))) | (~p12(X68, X66))) <=> ((~p12(X68, X66)) | (~p25(X68, X69)) | (~p12(X69, X67)) | p25(X66, X67))))),
% 0.71/0.92 inference(bind,[status(th)],[])).
% 0.71/0.92 tff(181,plain,
% 0.71/0.92 (![X67: $i, X68: $i, X66: $i, X69: $i] : (((p25(X66, X67) | (~p12(X69, X67))) | (~p25(X68, X69))) | (~p12(X68, X66))) <=> ![X67: $i, X68: $i, X66: $i, X69: $i] : ((~p12(X68, X66)) | (~p25(X68, X69)) | (~p12(X69, X67)) | p25(X66, X67))),
% 0.71/0.92 inference(quant_intro,[status(thm)],[180])).
% 0.71/0.92 tff(182,axiom,(![X67: $i, X68: $i, X66: $i, X69: $i] : (((p25(X66, X67) | (~p12(X69, X67))) | (~p25(X68, X69))) | (~p12(X68, X66)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','p25_25')).
% 0.71/0.92 tff(183,plain,
% 0.71/0.92 (![X67: $i, X68: $i, X66: $i, X69: $i] : ((~p12(X68, X66)) | (~p25(X68, X69)) | (~p12(X69, X67)) | p25(X66, X67))),
% 0.71/0.92 inference(modus_ponens,[status(thm)],[182, 181])).
% 0.71/0.92 tff(184,plain,
% 0.71/0.92 (![X67: $i, X68: $i, X66: $i, X69: $i] : ((~p12(X68, X66)) | (~p25(X68, X69)) | (~p12(X69, X67)) | p25(X66, X67))),
% 0.71/0.92 inference(modus_ponens,[status(thm)],[183, 179])).
% 0.71/0.92 tff(185,plain,(
% 0.71/0.92 ![X67: $i, X68: $i, X66: $i, X69: $i] : ((~p12(X68, X66)) | (~p25(X68, X69)) | (~p12(X69, X67)) | p25(X66, X67))),
% 0.71/0.92 inference(skolemize,[status(sab)],[184])).
% 0.71/0.92 tff(186,plain,
% 0.71/0.92 (![X67: $i, X68: $i, X66: $i, X69: $i] : ((~p12(X68, X66)) | (~p25(X68, X69)) | (~p12(X69, X67)) | p25(X66, X67))),
% 0.71/0.92 inference(modus_ponens,[status(thm)],[185, 178])).
% 0.71/0.92 tff(187,plain,
% 0.71/0.92 (((~![X67: $i, X68: $i, X66: $i, X69: $i] : ((~p12(X68, X66)) | (~p25(X68, X69)) | (~p12(X69, X67)) | p25(X66, X67))) | (p25(f13(f14(c31, c28)), f13(f14(c31, f21(c29, c27, c30, c31, c28)))) | (~p12(f13(f14(c31, f21(c29, c27, c30, c31, c28))), f13(f14(c31, f21(c29, c27, c30, c31, c28))))) | (~p12(f13(f14(c31, f16(f10(c29, f11(c27, c30)), c32, c31))), f13(f14(c31, c28)))) | (~p25(f13(f14(c31, f16(f10(c29, f11(c27, c30)), c32, c31))), f13(f14(c31, f21(c29, c27, c30, c31, c28))))))) <=> ((~![X67: $i, X68: $i, X66: $i, X69: $i] : ((~p12(X68, X66)) | (~p25(X68, X69)) | (~p12(X69, X67)) | p25(X66, X67))) | p25(f13(f14(c31, c28)), f13(f14(c31, f21(c29, c27, c30, c31, c28)))) | (~p12(f13(f14(c31, f21(c29, c27, c30, c31, c28))), f13(f14(c31, f21(c29, c27, c30, c31, c28))))) | (~p12(f13(f14(c31, f16(f10(c29, f11(c27, c30)), c32, c31))), f13(f14(c31, c28)))) | (~p25(f13(f14(c31, f16(f10(c29, f11(c27, c30)), c32, c31))), f13(f14(c31, f21(c29, c27, c30, c31, c28))))))),
% 0.71/0.92 inference(rewrite,[status(thm)],[])).
% 0.71/0.92 tff(188,plain,
% 0.71/0.92 (((~p12(f13(f14(c31, f16(f10(c29, f11(c27, c30)), c32, c31))), f13(f14(c31, c28)))) | (~p25(f13(f14(c31, f16(f10(c29, f11(c27, c30)), c32, c31))), f13(f14(c31, f21(c29, c27, c30, c31, c28))))) | (~p12(f13(f14(c31, f21(c29, c27, c30, c31, c28))), f13(f14(c31, f21(c29, c27, c30, c31, c28))))) | p25(f13(f14(c31, c28)), f13(f14(c31, f21(c29, c27, c30, c31, c28))))) <=> (p25(f13(f14(c31, c28)), f13(f14(c31, f21(c29, c27, c30, c31, c28)))) | (~p12(f13(f14(c31, f21(c29, c27, c30, c31, c28))), f13(f14(c31, f21(c29, c27, c30, c31, c28))))) | (~p12(f13(f14(c31, f16(f10(c29, f11(c27, c30)), c32, c31))), f13(f14(c31, c28)))) | (~p25(f13(f14(c31, f16(f10(c29, f11(c27, c30)), c32, c31))), f13(f14(c31, f21(c29, c27, c30, c31, c28))))))),
% 0.71/0.92 inference(rewrite,[status(thm)],[])).
% 0.71/0.92 tff(189,plain,
% 0.71/0.92 (((~![X67: $i, X68: $i, X66: $i, X69: $i] : ((~p12(X68, X66)) | (~p25(X68, X69)) | (~p12(X69, X67)) | p25(X66, X67))) | ((~p12(f13(f14(c31, f16(f10(c29, f11(c27, c30)), c32, c31))), f13(f14(c31, c28)))) | (~p25(f13(f14(c31, f16(f10(c29, f11(c27, c30)), c32, c31))), f13(f14(c31, f21(c29, c27, c30, c31, c28))))) | (~p12(f13(f14(c31, f21(c29, c27, c30, c31, c28))), f13(f14(c31, f21(c29, c27, c30, c31, c28))))) | p25(f13(f14(c31, c28)), f13(f14(c31, f21(c29, c27, c30, c31, c28)))))) <=> ((~![X67: $i, X68: $i, X66: $i, X69: $i] : ((~p12(X68, X66)) | (~p25(X68, X69)) | (~p12(X69, X67)) | p25(X66, X67))) | (p25(f13(f14(c31, c28)), f13(f14(c31, f21(c29, c27, c30, c31, c28)))) | (~p12(f13(f14(c31, f21(c29, c27, c30, c31, c28))), f13(f14(c31, f21(c29, c27, c30, c31, c28))))) | (~p12(f13(f14(c31, f16(f10(c29, f11(c27, c30)), c32, c31))), f13(f14(c31, c28)))) | (~p25(f13(f14(c31, f16(f10(c29, f11(c27, c30)), c32, c31))), f13(f14(c31, f21(c29, c27, c30, c31, c28)))))))),
% 0.71/0.92 inference(monotonicity,[status(thm)],[188])).
% 0.71/0.92 tff(190,plain,
% 0.71/0.92 (((~![X67: $i, X68: $i, X66: $i, X69: $i] : ((~p12(X68, X66)) | (~p25(X68, X69)) | (~p12(X69, X67)) | p25(X66, X67))) | ((~p12(f13(f14(c31, f16(f10(c29, f11(c27, c30)), c32, c31))), f13(f14(c31, c28)))) | (~p25(f13(f14(c31, f16(f10(c29, f11(c27, c30)), c32, c31))), f13(f14(c31, f21(c29, c27, c30, c31, c28))))) | (~p12(f13(f14(c31, f21(c29, c27, c30, c31, c28))), f13(f14(c31, f21(c29, c27, c30, c31, c28))))) | p25(f13(f14(c31, c28)), f13(f14(c31, f21(c29, c27, c30, c31, c28)))))) <=> ((~![X67: $i, X68: $i, X66: $i, X69: $i] : ((~p12(X68, X66)) | (~p25(X68, X69)) | (~p12(X69, X67)) | p25(X66, X67))) | p25(f13(f14(c31, c28)), f13(f14(c31, f21(c29, c27, c30, c31, c28)))) | (~p12(f13(f14(c31, f21(c29, c27, c30, c31, c28))), f13(f14(c31, f21(c29, c27, c30, c31, c28))))) | (~p12(f13(f14(c31, f16(f10(c29, f11(c27, c30)), c32, c31))), f13(f14(c31, c28)))) | (~p25(f13(f14(c31, f16(f10(c29, f11(c27, c30)), c32, c31))), f13(f14(c31, f21(c29, c27, c30, c31, c28))))))),
% 0.71/0.92 inference(transitivity,[status(thm)],[189, 187])).
% 0.71/0.92 tff(191,plain,
% 0.71/0.92 ((~![X67: $i, X68: $i, X66: $i, X69: $i] : ((~p12(X68, X66)) | (~p25(X68, X69)) | (~p12(X69, X67)) | p25(X66, X67))) | ((~p12(f13(f14(c31, f16(f10(c29, f11(c27, c30)), c32, c31))), f13(f14(c31, c28)))) | (~p25(f13(f14(c31, f16(f10(c29, f11(c27, c30)), c32, c31))), f13(f14(c31, f21(c29, c27, c30, c31, c28))))) | (~p12(f13(f14(c31, f21(c29, c27, c30, c31, c28))), f13(f14(c31, f21(c29, c27, c30, c31, c28))))) | p25(f13(f14(c31, c28)), f13(f14(c31, f21(c29, c27, c30, c31, c28)))))),
% 0.71/0.93 inference(quant_inst,[status(thm)],[])).
% 0.71/0.93 tff(192,plain,
% 0.71/0.93 ((~![X67: $i, X68: $i, X66: $i, X69: $i] : ((~p12(X68, X66)) | (~p25(X68, X69)) | (~p12(X69, X67)) | p25(X66, X67))) | p25(f13(f14(c31, c28)), f13(f14(c31, f21(c29, c27, c30, c31, c28)))) | (~p12(f13(f14(c31, f21(c29, c27, c30, c31, c28))), f13(f14(c31, f21(c29, c27, c30, c31, c28))))) | (~p12(f13(f14(c31, f16(f10(c29, f11(c27, c30)), c32, c31))), f13(f14(c31, c28)))) | (~p25(f13(f14(c31, f16(f10(c29, f11(c27, c30)), c32, c31))), f13(f14(c31, f21(c29, c27, c30, c31, c28)))))),
% 0.71/0.93 inference(modus_ponens,[status(thm)],[191, 190])).
% 0.71/0.93 tff(193,plain,
% 0.71/0.93 ($false),
% 0.71/0.93 inference(unit_resolution,[status(thm)],[192, 186, 176, 159, 130, 43])).
% 0.71/0.93 % SZS output end Proof
% 0.71/0.93 % E exiting
%------------------------------------------------------------------------------