%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : LCL644+1.005 : TPTP v9.3.1. Released v4.0.0.
% Transfm : NO INFORMATION
% Format : NO INFORMATION
% Command : run_E %s %d THM
% Computer : n010.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Sep 7 03:00:21 PM UTC 2026
% Result : Theorem 0.13s 0.42s
% Output : Proof 0.22s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL644+1.005 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : run_E %s %d THM
% 0.08/0.35 % Computer : n010.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Sat Sep 5 07:08:40 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.13/0.42 % SZS status Theorem
% 0.13/0.42 % SZS output start Proof
% 0.13/0.42 tff(p2_type, type, (
% 0.13/0.42 p2: $i > $o)).
% 0.13/0.42 tff(tptp_fun_X_26_type, type, (
% 0.13/0.42 tptp_fun_X_26: $i > $i)).
% 0.13/0.42 tff(r1_type, type, (
% 0.13/0.42 r1: ( $i * $i ) > $o)).
% 0.13/0.42 tff(p1_type, type, (
% 0.13/0.42 p1: $i > $o)).
% 0.13/0.42 tff(tptp_fun_X_0_type, type, (
% 0.13/0.42 tptp_fun_X_0: $i)).
% 0.13/0.42 tff(tptp_fun_Y_32_type, type, (
% 0.13/0.42 tptp_fun_Y_32: $i)).
% 0.13/0.42 tff(tptp_fun_X_31_type, type, (
% 0.13/0.42 tptp_fun_X_31: $i)).
% 0.13/0.42 tff(tptp_fun_Y_30_type, type, (
% 0.13/0.42 tptp_fun_Y_30: $i)).
% 0.13/0.42 tff(tptp_fun_Y_28_type, type, (
% 0.13/0.42 tptp_fun_Y_28: $i)).
% 0.13/0.42 tff(tptp_fun_X_29_type, type, (
% 0.13/0.42 tptp_fun_X_29: $i)).
% 0.13/0.42 tff(tptp_fun_X_27_type, type, (
% 0.13/0.42 tptp_fun_X_27: $i > $i)).
% 0.13/0.42 tff(p3_type, type, (
% 0.13/0.42 p3: $i > $o)).
% 0.13/0.42 tff(tptp_fun_Y_25_type, type, (
% 0.13/0.42 tptp_fun_Y_25: $i)).
% 0.13/0.42 tff(tptp_fun_X_24_type, type, (
% 0.13/0.42 tptp_fun_X_24: $i)).
% 0.13/0.42 tff(tptp_fun_Y_23_type, type, (
% 0.13/0.42 tptp_fun_Y_23: $i)).
% 0.13/0.42 tff(tptp_fun_X_22_type, type, (
% 0.13/0.42 tptp_fun_X_22: $i)).
% 0.13/0.42 tff(tptp_fun_Y_21_type, type, (
% 0.13/0.42 tptp_fun_Y_21: $i)).
% 0.13/0.42 tff(tptp_fun_X_9_type, type, (
% 0.13/0.42 tptp_fun_X_9: $i > $i)).
% 0.13/0.42 tff(p5_type, type, (
% 0.13/0.42 p5: $i > $o)).
% 0.13/0.42 tff(tptp_fun_Y_20_type, type, (
% 0.13/0.42 tptp_fun_Y_20: $i)).
% 0.13/0.42 tff(p4_type, type, (
% 0.13/0.42 p4: $i > $o)).
% 0.13/0.42 tff(tptp_fun_X_8_type, type, (
% 0.13/0.42 tptp_fun_X_8: $i > $i)).
% 0.13/0.42 tff(tptp_fun_Y_19_type, type, (
% 0.13/0.42 tptp_fun_Y_19: $i)).
% 0.13/0.42 tff(tptp_fun_X_18_type, type, (
% 0.13/0.42 tptp_fun_X_18: $i)).
% 0.13/0.42 tff(tptp_fun_Y_17_type, type, (
% 0.13/0.42 tptp_fun_Y_17: $i)).
% 0.13/0.42 tff(tptp_fun_X_16_type, type, (
% 0.13/0.42 tptp_fun_X_16: $i)).
% 0.13/0.42 tff(tptp_fun_Y_15_type, type, (
% 0.13/0.42 tptp_fun_Y_15: $i)).
% 0.13/0.42 tff(tptp_fun_X_2_type, type, (
% 0.13/0.42 tptp_fun_X_2: $i > $i)).
% 0.13/0.42 tff(tptp_fun_Y_14_type, type, (
% 0.13/0.42 tptp_fun_Y_14: $i)).
% 0.13/0.42 tff(tptp_fun_X_13_type, type, (
% 0.13/0.42 tptp_fun_X_13: $i)).
% 0.13/0.42 tff(tptp_fun_Y_12_type, type, (
% 0.13/0.42 tptp_fun_Y_12: $i)).
% 0.13/0.42 tff(tptp_fun_Y_10_type, type, (
% 0.13/0.42 tptp_fun_Y_10: $i)).
% 0.13/0.42 tff(tptp_fun_X_11_type, type, (
% 0.13/0.42 tptp_fun_X_11: $i)).
% 0.13/0.42 tff(tptp_fun_Y_7_type, type, (
% 0.13/0.42 tptp_fun_Y_7: $i)).
% 0.13/0.42 tff(p6_type, type, (
% 0.13/0.42 p6: $i > $o)).
% 0.13/0.42 tff(tptp_fun_X_6_type, type, (
% 0.13/0.42 tptp_fun_X_6: $i)).
% 0.13/0.42 tff(tptp_fun_Y_5_type, type, (
% 0.13/0.42 tptp_fun_Y_5: $i)).
% 0.13/0.42 tff(tptp_fun_X_4_type, type, (
% 0.13/0.42 tptp_fun_X_4: $i)).
% 0.13/0.42 tff(tptp_fun_Y_3_type, type, (
% 0.13/0.42 tptp_fun_Y_3: $i)).
% 0.13/0.42 tff(tptp_fun_X_1_type, type, (
% 0.13/0.42 tptp_fun_X_1: $i > $i)).
% 0.13/0.42 tff(1,plain,
% 0.13/0.42 (((![Y: $i] : (p5(Y) | (~r1(X!0, Y)) | (~(p6(tptp_fun_X_1(Y)) | (~r1(Y, tptp_fun_X_1(Y))))) | (~p6(Y))) | ![Y: $i] : (p6(Y) | (~p5(Y)) | (~r1(X!0, Y)) | (~(p5(tptp_fun_X_2(Y)) | (~r1(Y, tptp_fun_X_2(Y)))))) | ((~p6(Y!3)) & r1(X!0, Y!3) & p5(Y!3) & ![X: $i] : (p5(X) | (~r1(Y!3, X))) & (~p5(X!4)) & r1(Y!3, X!4) & p6(X!4) & ![Y: $i] : (p6(Y) | (~r1(X!4, Y)))) | ((~p5(Y!5)) & r1(X!0, Y!5) & p6(Y!5) & ![X: $i] : (p6(X) | (~r1(Y!5, X))) & (~p6(X!6)) & r1(Y!5, X!6) & p5(X!6) & ![Y: $i] : (p5(Y) | (~r1(X!6, Y))))) & (![Y: $i] : (p3(Y) | (~r1(X!0, Y)) | (~p4(Y)) | (~((~r1(Y, tptp_fun_X_8(Y))) | p4(tptp_fun_X_8(Y))))) | ![Y: $i] : (p4(Y) | (~r1(X!0, Y)) | (~p3(Y)) | (~((~r1(Y, tptp_fun_X_9(Y))) | p3(tptp_fun_X_9(Y))))) | (r1(X!0, Y!10) & (~p4(Y!10)) & r1(Y!10, X!11) & p4(X!11) & ![Y: $i] : (p4(Y) | (~r1(X!11, Y))) & (~p3(X!11)) & p3(Y!10) & ![X: $i] : (p3(X) | (~r1(Y!10, X)))) | (r1(X!0, Y!12) & p4(Y!12) & ![X: $i] : (p4(X) | (~r1(Y!12, X))) & (~p3(Y!12)) & r1(Y!12, X!13) & (~p4(X!13)) & p3(X!13) & ![Y: $i] : (p3(Y) | (~r1(X!13, Y))))) & (![Y: $i] : (p4(Y) | (~p5(Y)) | (~r1(X!0, Y)) | (~(p5(tptp_fun_X_2(Y)) | (~r1(Y, tptp_fun_X_2(Y)))))) | ((~p5(Y!15)) & r1(X!0, Y!15) & p4(Y!15) & ![X: $i] : (p4(X) | (~r1(Y!15, X))) & r1(Y!15, X!16) & (~p4(X!16)) & p5(X!16) & ![Y: $i] : (p5(Y) | (~r1(X!16, Y)))) | (r1(X!0, Y!17) & (~p4(Y!17)) & p5(Y!17) & ![X: $i] : (p5(X) | (~r1(Y!17, X))) & (~p5(X!18)) & r1(Y!17, X!18) & p4(X!18) & ![Y: $i] : (p4(Y) | (~r1(X!18, Y)))) | ![Y: $i] : (p5(Y) | (~r1(X!0, Y)) | (~p4(Y)) | (~((~r1(Y, tptp_fun_X_8(Y))) | p4(tptp_fun_X_8(Y)))))) & $false & (![Y: $i] : (p2(Y) | (~r1(X!0, Y)) | (~p3(Y)) | (~((~r1(Y, tptp_fun_X_9(Y))) | p3(tptp_fun_X_9(Y))))) | (r1(X!0, Y!21) & (~p3(Y!21)) & p2(Y!21) & ![X: $i] : (p2(X) | (~r1(Y!21, X))) & r1(Y!21, X!22) & p3(X!22) & ![Y: $i] : (p3(Y) | (~r1(X!22, Y))) & (~p2(X!22))) | (r1(X!0, Y!23) & p3(Y!23) & ![X: $i] : (p3(X) | (~r1(Y!23, X))) & (~p2(Y!23)) & r1(Y!23, X!24) & (~p3(X!24)) & p2(X!24) & ![Y: $i] : (p2(Y) | (~r1(X!24, Y)))) | ![Y: $i] : (p3(Y) | (~r1(X!0, Y)) | (~p2(Y)) | (~((~r1(Y, tptp_fun_X_26(Y))) | p2(tptp_fun_X_26(Y)))))) & (![Y: $i] : (p2(Y) | (~r1(X!0, Y)) | (~p1(Y)) | (~((~r1(Y, tptp_fun_X_27(Y))) | p1(tptp_fun_X_27(Y))))) | (r1(X!0, Y!28) & r1(Y!28, X!29) & p2(X!29) & ![Y: $i] : (p2(Y) | (~r1(X!29, Y))) & (~p1(X!29)) & (~p2(Y!28)) & p1(Y!28) & ![X: $i] : (p1(X) | (~r1(Y!28, X)))) | (r1(X!0, Y!30) & (~p1(Y!30)) & p2(Y!30) & ![X: $i] : (p2(X) | (~r1(Y!30, X))) & r1(Y!30, X!31) & (~p2(X!31)) & p1(X!31) & ![Y: $i] : (p1(Y) | (~r1(X!31, Y)))) | ![Y: $i] : (p1(Y) | (~r1(X!0, Y)) | (~p2(Y)) | (~((~r1(Y, tptp_fun_X_26(Y))) | p2(tptp_fun_X_26(Y))))))) <=> $false),
% 0.13/0.43 inference(rewrite,[status(thm)],[])).
% 0.13/0.43 tff(2,plain,
% 0.13/0.43 ((![Y: $i] : (p2(Y) | (~r1(X!0, Y)) | (~p1(Y)) | (~((~r1(Y, tptp_fun_X_27(Y))) | p1(tptp_fun_X_27(Y))))) | ((r1(X!0, Y!28) & r1(Y!28, X!29) & p2(X!29) & ![Y: $i] : (p2(Y) | (~r1(X!29, Y))) & (~p1(X!29)) & (~p2(Y!28)) & p1(Y!28) & ![X: $i] : (p1(X) | (~r1(Y!28, X)))) | (r1(X!0, Y!30) & (~p1(Y!30)) & p2(Y!30) & ![X: $i] : (p2(X) | (~r1(Y!30, X))) & r1(Y!30, X!31) & (~p2(X!31)) & p1(X!31) & ![Y: $i] : (p1(Y) | (~r1(X!31, Y))))) | ![Y: $i] : (p1(Y) | (~r1(X!0, Y)) | (~p2(Y)) | (~((~r1(Y, tptp_fun_X_26(Y))) | p2(tptp_fun_X_26(Y)))))) <=> (![Y: $i] : (p2(Y) | (~r1(X!0, Y)) | (~p1(Y)) | (~((~r1(Y, tptp_fun_X_27(Y))) | p1(tptp_fun_X_27(Y))))) | (r1(X!0, Y!28) & r1(Y!28, X!29) & p2(X!29) & ![Y: $i] : (p2(Y) | (~r1(X!29, Y))) & (~p1(X!29)) & (~p2(Y!28)) & p1(Y!28) & ![X: $i] : (p1(X) | (~r1(Y!28, X)))) | (r1(X!0, Y!30) & (~p1(Y!30)) & p2(Y!30) & ![X: $i] : (p2(X) | (~r1(Y!30, X))) & r1(Y!30, X!31) & (~p2(X!31)) & p1(X!31) & ![Y: $i] : (p1(Y) | (~r1(X!31, Y)))) | ![Y: $i] : (p1(Y) | (~r1(X!0, Y)) | (~p2(Y)) | (~((~r1(Y, tptp_fun_X_26(Y))) | p2(tptp_fun_X_26(Y))))))),
% 0.13/0.43 inference(rewrite,[status(thm)],[])).
% 0.13/0.43 tff(3,plain,
% 0.13/0.43 (^[Y: $i] : trans(monotonicity(monotonicity(rewrite((~((~r1(Y, tptp_fun_X_26(Y))) | p2(tptp_fun_X_26(Y)))) <=> (~((~r1(Y, tptp_fun_X_26(Y))) | p2(tptp_fun_X_26(Y))))), (((~p2(Y)) | (~((~r1(Y, tptp_fun_X_26(Y))) | p2(tptp_fun_X_26(Y))))) <=> ((~p2(Y)) | (~((~r1(Y, tptp_fun_X_26(Y))) | p2(tptp_fun_X_26(Y))))))), (((~r1(X!0, Y)) | p1(Y) | ((~p2(Y)) | (~((~r1(Y, tptp_fun_X_26(Y))) | p2(tptp_fun_X_26(Y)))))) <=> ((~r1(X!0, Y)) | p1(Y) | ((~p2(Y)) | (~((~r1(Y, tptp_fun_X_26(Y))) | p2(tptp_fun_X_26(Y)))))))), rewrite(((~r1(X!0, Y)) | p1(Y) | ((~p2(Y)) | (~((~r1(Y, tptp_fun_X_26(Y))) | p2(tptp_fun_X_26(Y)))))) <=> (p1(Y) | (~r1(X!0, Y)) | (~p2(Y)) | (~((~r1(Y, tptp_fun_X_26(Y))) | p2(tptp_fun_X_26(Y)))))), (((~r1(X!0, Y)) | p1(Y) | ((~p2(Y)) | (~((~r1(Y, tptp_fun_X_26(Y))) | p2(tptp_fun_X_26(Y)))))) <=> (p1(Y) | (~r1(X!0, Y)) | (~p2(Y)) | (~((~r1(Y, tptp_fun_X_26(Y))) | p2(tptp_fun_X_26(Y)))))))),
% 0.13/0.43 inference(bind,[status(th)],[])).
% 0.13/0.43 tff(4,plain,
% 0.13/0.43 (![Y: $i] : ((~r1(X!0, Y)) | p1(Y) | ((~p2(Y)) | (~((~r1(Y, tptp_fun_X_26(Y))) | p2(tptp_fun_X_26(Y)))))) <=> ![Y: $i] : (p1(Y) | (~r1(X!0, Y)) | (~p2(Y)) | (~((~r1(Y, tptp_fun_X_26(Y))) | p2(tptp_fun_X_26(Y)))))),
% 0.13/0.43 inference(quant_intro,[status(thm)],[3])).
% 0.13/0.43 tff(5,plain,
% 0.13/0.43 (((r1(X!0, Y!28) & r1(Y!28, X!29) & p2(X!29) & ![Y: $i] : (p2(Y) | (~r1(X!29, Y))) & (~p1(X!29)) & (~p2(Y!28)) & p1(Y!28) & ![X: $i] : (p1(X) | (~r1(Y!28, X)))) | (r1(X!0, Y!30) & (~p1(Y!30)) & p2(Y!30) & ![X: $i] : (p2(X) | (~r1(Y!30, X))) & r1(Y!30, X!31) & (~p2(X!31)) & p1(X!31) & ![Y: $i] : (p1(Y) | (~r1(X!31, Y)))) | $false) <=> ((r1(X!0, Y!28) & r1(Y!28, X!29) & p2(X!29) & ![Y: $i] : (p2(Y) | (~r1(X!29, Y))) & (~p1(X!29)) & (~p2(Y!28)) & p1(Y!28) & ![X: $i] : (p1(X) | (~r1(Y!28, X)))) | (r1(X!0, Y!30) & (~p1(Y!30)) & p2(Y!30) & ![X: $i] : (p2(X) | (~r1(Y!30, X))) & r1(Y!30, X!31) & (~p2(X!31)) & p1(X!31) & ![Y: $i] : (p1(Y) | (~r1(X!31, Y)))))),
% 0.13/0.43 inference(rewrite,[status(thm)],[])).
% 0.13/0.43 tff(6,plain,
% 0.13/0.43 ((r1(X!0, Y!32) & (~p2(Y!32)) & (~p1(Y!32)) & (p2(Y!32) & ![X: $i] : (p2(X) | (~r1(Y!32, X)))) & (p1(Y!32) & ![X: $i] : (p1(X) | (~r1(Y!32, X))))) <=> $false),
% 0.13/0.43 inference(rewrite,[status(thm)],[])).
% 0.13/0.43 tff(7,plain,
% 0.13/0.43 ((p1(Y!32) & ![X: $i] : ((~r1(Y!32, X)) | p1(X))) <=> (p1(Y!32) & ![X: $i] : (p1(X) | (~r1(Y!32, X))))),
% 0.13/0.43 inference(rewrite,[status(thm)],[])).
% 0.13/0.43 tff(8,plain,
% 0.13/0.43 ((p2(Y!32) & ![X: $i] : ((~r1(Y!32, X)) | p2(X))) <=> (p2(Y!32) & ![X: $i] : (p2(X) | (~r1(Y!32, X))))),
% 0.13/0.43 inference(rewrite,[status(thm)],[])).
% 0.13/0.43 tff(9,plain,
% 0.13/0.43 ((r1(X!0, Y!32) & (~p2(Y!32)) & (~p1(Y!32)) & (p2(Y!32) & ![X: $i] : ((~r1(Y!32, X)) | p2(X))) & (p1(Y!32) & ![X: $i] : ((~r1(Y!32, X)) | p1(X)))) <=> (r1(X!0, Y!32) & (~p2(Y!32)) & (~p1(Y!32)) & (p2(Y!32) & ![X: $i] : (p2(X) | (~r1(Y!32, X)))) & (p1(Y!32) & ![X: $i] : (p1(X) | (~r1(Y!32, X)))))),
% 0.13/0.43 inference(monotonicity,[status(thm)],[8, 7])).
% 0.13/0.43 tff(10,plain,
% 0.13/0.43 ((r1(X!0, Y!32) & (~p2(Y!32)) & (~p1(Y!32)) & (p2(Y!32) & ![X: $i] : ((~r1(Y!32, X)) | p2(X))) & (p1(Y!32) & ![X: $i] : ((~r1(Y!32, X)) | p1(X)))) <=> $false),
% 0.13/0.43 inference(transitivity,[status(thm)],[9, 6])).
% 0.13/0.43 tff(11,plain,
% 0.13/0.43 ((r1(X!0, Y!30) & (~p1(Y!30)) & (p2(Y!30) & ![X: $i] : (p2(X) | (~r1(Y!30, X)))) & (r1(Y!30, X!31) & (~p2(X!31)) & p1(X!31) & ![Y: $i] : (p1(Y) | (~r1(X!31, Y))))) <=> (r1(X!0, Y!30) & (~p1(Y!30)) & p2(Y!30) & ![X: $i] : (p2(X) | (~r1(Y!30, X))) & r1(Y!30, X!31) & (~p2(X!31)) & p1(X!31) & ![Y: $i] : (p1(Y) | (~r1(X!31, Y))))),
% 0.13/0.43 inference(rewrite,[status(thm)],[])).
% 0.13/0.43 tff(12,plain,
% 0.13/0.43 ((r1(Y!30, X!31) & (~p2(X!31)) & (p1(X!31) & ![Y: $i] : (p1(Y) | (~r1(X!31, Y))))) <=> (r1(Y!30, X!31) & (~p2(X!31)) & p1(X!31) & ![Y: $i] : (p1(Y) | (~r1(X!31, Y))))),
% 0.13/0.43 inference(rewrite,[status(thm)],[])).
% 0.13/0.43 tff(13,plain,
% 0.13/0.43 ((p1(X!31) & ![Y: $i] : ((~r1(X!31, Y)) | p1(Y))) <=> (p1(X!31) & ![Y: $i] : (p1(Y) | (~r1(X!31, Y))))),
% 0.13/0.43 inference(rewrite,[status(thm)],[])).
% 0.13/0.43 tff(14,plain,
% 0.13/0.43 ((r1(Y!30, X!31) & (~p2(X!31)) & (p1(X!31) & ![Y: $i] : ((~r1(X!31, Y)) | p1(Y)))) <=> (r1(Y!30, X!31) & (~p2(X!31)) & (p1(X!31) & ![Y: $i] : (p1(Y) | (~r1(X!31, Y)))))),
% 0.13/0.43 inference(monotonicity,[status(thm)],[13])).
% 0.13/0.43 tff(15,plain,
% 0.13/0.43 ((r1(Y!30, X!31) & (~p2(X!31)) & (p1(X!31) & ![Y: $i] : ((~r1(X!31, Y)) | p1(Y)))) <=> (r1(Y!30, X!31) & (~p2(X!31)) & p1(X!31) & ![Y: $i] : (p1(Y) | (~r1(X!31, Y))))),
% 0.13/0.43 inference(transitivity,[status(thm)],[14, 12])).
% 0.13/0.43 tff(16,plain,
% 0.13/0.43 ((p2(Y!30) & ![X: $i] : ((~r1(Y!30, X)) | p2(X))) <=> (p2(Y!30) & ![X: $i] : (p2(X) | (~r1(Y!30, X))))),
% 0.13/0.43 inference(rewrite,[status(thm)],[])).
% 0.13/0.43 tff(17,plain,
% 0.13/0.43 ((r1(X!0, Y!30) & (~p1(Y!30)) & (p2(Y!30) & ![X: $i] : ((~r1(Y!30, X)) | p2(X))) & (r1(Y!30, X!31) & (~p2(X!31)) & (p1(X!31) & ![Y: $i] : ((~r1(X!31, Y)) | p1(Y))))) <=> (r1(X!0, Y!30) & (~p1(Y!30)) & (p2(Y!30) & ![X: $i] : (p2(X) | (~r1(Y!30, X)))) & (r1(Y!30, X!31) & (~p2(X!31)) & p1(X!31) & ![Y: $i] : (p1(Y) | (~r1(X!31, Y)))))),
% 0.13/0.43 inference(monotonicity,[status(thm)],[16, 15])).
% 0.13/0.43 tff(18,plain,
% 0.13/0.43 ((r1(X!0, Y!30) & (~p1(Y!30)) & (p2(Y!30) & ![X: $i] : ((~r1(Y!30, X)) | p2(X))) & (r1(Y!30, X!31) & (~p2(X!31)) & (p1(X!31) & ![Y: $i] : ((~r1(X!31, Y)) | p1(Y))))) <=> (r1(X!0, Y!30) & (~p1(Y!30)) & p2(Y!30) & ![X: $i] : (p2(X) | (~r1(Y!30, X))) & r1(Y!30, X!31) & (~p2(X!31)) & p1(X!31) & ![Y: $i] : (p1(Y) | (~r1(X!31, Y))))),
% 0.13/0.43 inference(transitivity,[status(thm)],[17, 11])).
% 0.13/0.43 tff(19,plain,
% 0.13/0.43 ((r1(X!0, Y!28) & (r1(Y!28, X!29) & p2(X!29) & ![Y: $i] : (p2(Y) | (~r1(X!29, Y))) & (~p1(X!29))) & (~p2(Y!28)) & (p1(Y!28) & ![X: $i] : (p1(X) | (~r1(Y!28, X))))) <=> (r1(X!0, Y!28) & r1(Y!28, X!29) & p2(X!29) & ![Y: $i] : (p2(Y) | (~r1(X!29, Y))) & (~p1(X!29)) & (~p2(Y!28)) & p1(Y!28) & ![X: $i] : (p1(X) | (~r1(Y!28, X))))),
% 0.13/0.43 inference(rewrite,[status(thm)],[])).
% 0.13/0.43 tff(20,plain,
% 0.13/0.43 ((p1(Y!28) & ![X: $i] : ((~r1(Y!28, X)) | p1(X))) <=> (p1(Y!28) & ![X: $i] : (p1(X) | (~r1(Y!28, X))))),
% 0.13/0.43 inference(rewrite,[status(thm)],[])).
% 0.13/0.43 tff(21,plain,
% 0.13/0.43 ((r1(Y!28, X!29) & (p2(X!29) & ![Y: $i] : (p2(Y) | (~r1(X!29, Y)))) & (~p1(X!29))) <=> (r1(Y!28, X!29) & p2(X!29) & ![Y: $i] : (p2(Y) | (~r1(X!29, Y))) & (~p1(X!29)))),
% 0.13/0.43 inference(rewrite,[status(thm)],[])).
% 0.13/0.43 tff(22,plain,
% 0.13/0.43 ((p2(X!29) & ![Y: $i] : ((~r1(X!29, Y)) | p2(Y))) <=> (p2(X!29) & ![Y: $i] : (p2(Y) | (~r1(X!29, Y))))),
% 0.13/0.43 inference(rewrite,[status(thm)],[])).
% 0.13/0.43 tff(23,plain,
% 0.13/0.43 ((r1(Y!28, X!29) & (p2(X!29) & ![Y: $i] : ((~r1(X!29, Y)) | p2(Y))) & (~p1(X!29))) <=> (r1(Y!28, X!29) & (p2(X!29) & ![Y: $i] : (p2(Y) | (~r1(X!29, Y)))) & (~p1(X!29)))),
% 0.13/0.43 inference(monotonicity,[status(thm)],[22])).
% 0.13/0.43 tff(24,plain,
% 0.13/0.43 ((r1(Y!28, X!29) & (p2(X!29) & ![Y: $i] : ((~r1(X!29, Y)) | p2(Y))) & (~p1(X!29))) <=> (r1(Y!28, X!29) & p2(X!29) & ![Y: $i] : (p2(Y) | (~r1(X!29, Y))) & (~p1(X!29)))),
% 0.13/0.43 inference(transitivity,[status(thm)],[23, 21])).
% 0.13/0.43 tff(25,plain,
% 0.13/0.43 ((r1(X!0, Y!28) & (r1(Y!28, X!29) & (p2(X!29) & ![Y: $i] : ((~r1(X!29, Y)) | p2(Y))) & (~p1(X!29))) & (~p2(Y!28)) & (p1(Y!28) & ![X: $i] : ((~r1(Y!28, X)) | p1(X)))) <=> (r1(X!0, Y!28) & (r1(Y!28, X!29) & p2(X!29) & ![Y: $i] : (p2(Y) | (~r1(X!29, Y))) & (~p1(X!29))) & (~p2(Y!28)) & (p1(Y!28) & ![X: $i] : (p1(X) | (~r1(Y!28, X)))))),
% 0.13/0.43 inference(monotonicity,[status(thm)],[24, 20])).
% 0.13/0.43 tff(26,plain,
% 0.13/0.43 ((r1(X!0, Y!28) & (r1(Y!28, X!29) & (p2(X!29) & ![Y: $i] : ((~r1(X!29, Y)) | p2(Y))) & (~p1(X!29))) & (~p2(Y!28)) & (p1(Y!28) & ![X: $i] : ((~r1(Y!28, X)) | p1(X)))) <=> (r1(X!0, Y!28) & r1(Y!28, X!29) & p2(X!29) & ![Y: $i] : (p2(Y) | (~r1(X!29, Y))) & (~p1(X!29)) & (~p2(Y!28)) & p1(Y!28) & ![X: $i] : (p1(X) | (~r1(Y!28, X))))),
% 0.13/0.43 inference(transitivity,[status(thm)],[25, 19])).
% 0.13/0.43 tff(27,plain,
% 0.13/0.43 (((r1(X!0, Y!28) & (r1(Y!28, X!29) & (p2(X!29) & ![Y: $i] : ((~r1(X!29, Y)) | p2(Y))) & (~p1(X!29))) & (~p2(Y!28)) & (p1(Y!28) & ![X: $i] : ((~r1(Y!28, X)) | p1(X)))) | (r1(X!0, Y!30) & (~p1(Y!30)) & (p2(Y!30) & ![X: $i] : ((~r1(Y!30, X)) | p2(X))) & (r1(Y!30, X!31) & (~p2(X!31)) & (p1(X!31) & ![Y: $i] : ((~r1(X!31, Y)) | p1(Y))))) | (r1(X!0, Y!32) & (~p2(Y!32)) & (~p1(Y!32)) & (p2(Y!32) & ![X: $i] : ((~r1(Y!32, X)) | p2(X))) & (p1(Y!32) & ![X: $i] : ((~r1(Y!32, X)) | p1(X))))) <=> ((r1(X!0, Y!28) & r1(Y!28, X!29) & p2(X!29) & ![Y: $i] : (p2(Y) | (~r1(X!29, Y))) & (~p1(X!29)) & (~p2(Y!28)) & p1(Y!28) & ![X: $i] : (p1(X) | (~r1(Y!28, X)))) | (r1(X!0, Y!30) & (~p1(Y!30)) & p2(Y!30) & ![X: $i] : (p2(X) | (~r1(Y!30, X))) & r1(Y!30, X!31) & (~p2(X!31)) & p1(X!31) & ![Y: $i] : (p1(Y) | (~r1(X!31, Y)))) | $false)),
% 0.13/0.43 inference(monotonicity,[status(thm)],[26, 18, 10])).
% 0.13/0.43 tff(28,plain,
% 0.13/0.43 (((r1(X!0, Y!28) & (r1(Y!28, X!29) & (p2(X!29) & ![Y: $i] : ((~r1(X!29, Y)) | p2(Y))) & (~p1(X!29))) & (~p2(Y!28)) & (p1(Y!28) & ![X: $i] : ((~r1(Y!28, X)) | p1(X)))) | (r1(X!0, Y!30) & (~p1(Y!30)) & (p2(Y!30) & ![X: $i] : ((~r1(Y!30, X)) | p2(X))) & (r1(Y!30, X!31) & (~p2(X!31)) & (p1(X!31) & ![Y: $i] : ((~r1(X!31, Y)) | p1(Y))))) | (r1(X!0, Y!32) & (~p2(Y!32)) & (~p1(Y!32)) & (p2(Y!32) & ![X: $i] : ((~r1(Y!32, X)) | p2(X))) & (p1(Y!32) & ![X: $i] : ((~r1(Y!32, X)) | p1(X))))) <=> ((r1(X!0, Y!28) & r1(Y!28, X!29) & p2(X!29) & ![Y: $i] : (p2(Y) | (~r1(X!29, Y))) & (~p1(X!29)) & (~p2(Y!28)) & p1(Y!28) & ![X: $i] : (p1(X) | (~r1(Y!28, X)))) | (r1(X!0, Y!30) & (~p1(Y!30)) & p2(Y!30) & ![X: $i] : (p2(X) | (~r1(Y!30, X))) & r1(Y!30, X!31) & (~p2(X!31)) & p1(X!31) & ![Y: $i] : (p1(Y) | (~r1(X!31, Y)))))),
% 0.13/0.43 inference(transitivity,[status(thm)],[27, 5])).
% 0.13/0.43 tff(29,plain,
% 0.13/0.43 (^[Y: $i] : trans(monotonicity(monotonicity(rewrite((~((~r1(Y, tptp_fun_X_27(Y))) | p1(tptp_fun_X_27(Y)))) <=> (~((~r1(Y, tptp_fun_X_27(Y))) | p1(tptp_fun_X_27(Y))))), (((~p1(Y)) | (~((~r1(Y, tptp_fun_X_27(Y))) | p1(tptp_fun_X_27(Y))))) <=> ((~p1(Y)) | (~((~r1(Y, tptp_fun_X_27(Y))) | p1(tptp_fun_X_27(Y))))))), (((~r1(X!0, Y)) | p2(Y) | ((~p1(Y)) | (~((~r1(Y, tptp_fun_X_27(Y))) | p1(tptp_fun_X_27(Y)))))) <=> ((~r1(X!0, Y)) | p2(Y) | ((~p1(Y)) | (~((~r1(Y, tptp_fun_X_27(Y))) | p1(tptp_fun_X_27(Y)))))))), rewrite(((~r1(X!0, Y)) | p2(Y) | ((~p1(Y)) | (~((~r1(Y, tptp_fun_X_27(Y))) | p1(tptp_fun_X_27(Y)))))) <=> (p2(Y) | (~r1(X!0, Y)) | (~p1(Y)) | (~((~r1(Y, tptp_fun_X_27(Y))) | p1(tptp_fun_X_27(Y)))))), (((~r1(X!0, Y)) | p2(Y) | ((~p1(Y)) | (~((~r1(Y, tptp_fun_X_27(Y))) | p1(tptp_fun_X_27(Y)))))) <=> (p2(Y) | (~r1(X!0, Y)) | (~p1(Y)) | (~((~r1(Y, tptp_fun_X_27(Y))) | p1(tptp_fun_X_27(Y)))))))),
% 0.13/0.43 inference(bind,[status(th)],[])).
% 0.13/0.43 tff(30,plain,
% 0.13/0.43 (![Y: $i] : ((~r1(X!0, Y)) | p2(Y) | ((~p1(Y)) | (~((~r1(Y, tptp_fun_X_27(Y))) | p1(tptp_fun_X_27(Y)))))) <=> ![Y: $i] : (p2(Y) | (~r1(X!0, Y)) | (~p1(Y)) | (~((~r1(Y, tptp_fun_X_27(Y))) | p1(tptp_fun_X_27(Y)))))),
% 0.13/0.44 inference(quant_intro,[status(thm)],[29])).
% 0.13/0.44 tff(31,plain,
% 0.13/0.44 ((![Y: $i] : ((~r1(X!0, Y)) | p2(Y) | ((~p1(Y)) | (~((~r1(Y, tptp_fun_X_27(Y))) | p1(tptp_fun_X_27(Y)))))) | ((r1(X!0, Y!28) & (r1(Y!28, X!29) & (p2(X!29) & ![Y: $i] : ((~r1(X!29, Y)) | p2(Y))) & (~p1(X!29))) & (~p2(Y!28)) & (p1(Y!28) & ![X: $i] : ((~r1(Y!28, X)) | p1(X)))) | (r1(X!0, Y!30) & (~p1(Y!30)) & (p2(Y!30) & ![X: $i] : ((~r1(Y!30, X)) | p2(X))) & (r1(Y!30, X!31) & (~p2(X!31)) & (p1(X!31) & ![Y: $i] : ((~r1(X!31, Y)) | p1(Y))))) | (r1(X!0, Y!32) & (~p2(Y!32)) & (~p1(Y!32)) & (p2(Y!32) & ![X: $i] : ((~r1(Y!32, X)) | p2(X))) & (p1(Y!32) & ![X: $i] : ((~r1(Y!32, X)) | p1(X))))) | ![Y: $i] : ((~r1(X!0, Y)) | p1(Y) | ((~p2(Y)) | (~((~r1(Y, tptp_fun_X_26(Y))) | p2(tptp_fun_X_26(Y))))))) <=> (![Y: $i] : (p2(Y) | (~r1(X!0, Y)) | (~p1(Y)) | (~((~r1(Y, tptp_fun_X_27(Y))) | p1(tptp_fun_X_27(Y))))) | ((r1(X!0, Y!28) & r1(Y!28, X!29) & p2(X!29) & ![Y: $i] : (p2(Y) | (~r1(X!29, Y))) & (~p1(X!29)) & (~p2(Y!28)) & p1(Y!28) & ![X: $i] : (p1(X) | (~r1(Y!28, X)))) | (r1(X!0, Y!30) & (~p1(Y!30)) & p2(Y!30) & ![X: $i] : (p2(X) | (~r1(Y!30, X))) & r1(Y!30, X!31) & (~p2(X!31)) & p1(X!31) & ![Y: $i] : (p1(Y) | (~r1(X!31, Y))))) | ![Y: $i] : (p1(Y) | (~r1(X!0, Y)) | (~p2(Y)) | (~((~r1(Y, tptp_fun_X_26(Y))) | p2(tptp_fun_X_26(Y))))))),
% 0.13/0.44 inference(monotonicity,[status(thm)],[30, 28, 4])).
% 0.13/0.44 tff(32,plain,
% 0.13/0.44 ((![Y: $i] : ((~r1(X!0, Y)) | p2(Y) | ((~p1(Y)) | (~((~r1(Y, tptp_fun_X_27(Y))) | p1(tptp_fun_X_27(Y)))))) | ((r1(X!0, Y!28) & (r1(Y!28, X!29) & (p2(X!29) & ![Y: $i] : ((~r1(X!29, Y)) | p2(Y))) & (~p1(X!29))) & (~p2(Y!28)) & (p1(Y!28) & ![X: $i] : ((~r1(Y!28, X)) | p1(X)))) | (r1(X!0, Y!30) & (~p1(Y!30)) & (p2(Y!30) & ![X: $i] : ((~r1(Y!30, X)) | p2(X))) & (r1(Y!30, X!31) & (~p2(X!31)) & (p1(X!31) & ![Y: $i] : ((~r1(X!31, Y)) | p1(Y))))) | (r1(X!0, Y!32) & (~p2(Y!32)) & (~p1(Y!32)) & (p2(Y!32) & ![X: $i] : ((~r1(Y!32, X)) | p2(X))) & (p1(Y!32) & ![X: $i] : ((~r1(Y!32, X)) | p1(X))))) | ![Y: $i] : ((~r1(X!0, Y)) | p1(Y) | ((~p2(Y)) | (~((~r1(Y, tptp_fun_X_26(Y))) | p2(tptp_fun_X_26(Y))))))) <=> (![Y: $i] : (p2(Y) | (~r1(X!0, Y)) | (~p1(Y)) | (~((~r1(Y, tptp_fun_X_27(Y))) | p1(tptp_fun_X_27(Y))))) | (r1(X!0, Y!28) & r1(Y!28, X!29) & p2(X!29) & ![Y: $i] : (p2(Y) | (~r1(X!29, Y))) & (~p1(X!29)) & (~p2(Y!28)) & p1(Y!28) & ![X: $i] : (p1(X) | (~r1(Y!28, X)))) | (r1(X!0, Y!30) & (~p1(Y!30)) & p2(Y!30) & ![X: $i] : (p2(X) | (~r1(Y!30, X))) & r1(Y!30, X!31) & (~p2(X!31)) & p1(X!31) & ![Y: $i] : (p1(Y) | (~r1(X!31, Y)))) | ![Y: $i] : (p1(Y) | (~r1(X!0, Y)) | (~p2(Y)) | (~((~r1(Y, tptp_fun_X_26(Y))) | p2(tptp_fun_X_26(Y))))))),
% 0.13/0.44 inference(transitivity,[status(thm)],[31, 2])).
% 0.13/0.44 tff(33,plain,
% 0.13/0.44 ((![Y: $i] : (p2(Y) | (~r1(X!0, Y)) | (~p3(Y)) | (~((~r1(Y, tptp_fun_X_9(Y))) | p3(tptp_fun_X_9(Y))))) | ((r1(X!0, Y!21) & (~p3(Y!21)) & p2(Y!21) & ![X: $i] : (p2(X) | (~r1(Y!21, X))) & r1(Y!21, X!22) & p3(X!22) & ![Y: $i] : (p3(Y) | (~r1(X!22, Y))) & (~p2(X!22))) | (r1(X!0, Y!23) & p3(Y!23) & ![X: $i] : (p3(X) | (~r1(Y!23, X))) & (~p2(Y!23)) & r1(Y!23, X!24) & (~p3(X!24)) & p2(X!24) & ![Y: $i] : (p2(Y) | (~r1(X!24, Y))))) | ![Y: $i] : (p3(Y) | (~r1(X!0, Y)) | (~p2(Y)) | (~((~r1(Y, tptp_fun_X_26(Y))) | p2(tptp_fun_X_26(Y)))))) <=> (![Y: $i] : (p2(Y) | (~r1(X!0, Y)) | (~p3(Y)) | (~((~r1(Y, tptp_fun_X_9(Y))) | p3(tptp_fun_X_9(Y))))) | (r1(X!0, Y!21) & (~p3(Y!21)) & p2(Y!21) & ![X: $i] : (p2(X) | (~r1(Y!21, X))) & r1(Y!21, X!22) & p3(X!22) & ![Y: $i] : (p3(Y) | (~r1(X!22, Y))) & (~p2(X!22))) | (r1(X!0, Y!23) & p3(Y!23) & ![X: $i] : (p3(X) | (~r1(Y!23, X))) & (~p2(Y!23)) & r1(Y!23, X!24) & (~p3(X!24)) & p2(X!24) & ![Y: $i] : (p2(Y) | (~r1(X!24, Y)))) | ![Y: $i] : (p3(Y) | (~r1(X!0, Y)) | (~p2(Y)) | (~((~r1(Y, tptp_fun_X_26(Y))) | p2(tptp_fun_X_26(Y))))))),
% 0.13/0.44 inference(rewrite,[status(thm)],[])).
% 0.13/0.44 tff(34,plain,
% 0.13/0.44 (^[Y: $i] : trans(monotonicity(monotonicity(rewrite((~((~r1(Y, tptp_fun_X_26(Y))) | p2(tptp_fun_X_26(Y)))) <=> (~((~r1(Y, tptp_fun_X_26(Y))) | p2(tptp_fun_X_26(Y))))), (((~p2(Y)) | (~((~r1(Y, tptp_fun_X_26(Y))) | p2(tptp_fun_X_26(Y))))) <=> ((~p2(Y)) | (~((~r1(Y, tptp_fun_X_26(Y))) | p2(tptp_fun_X_26(Y))))))), (((~r1(X!0, Y)) | p3(Y) | ((~p2(Y)) | (~((~r1(Y, tptp_fun_X_26(Y))) | p2(tptp_fun_X_26(Y)))))) <=> ((~r1(X!0, Y)) | p3(Y) | ((~p2(Y)) | (~((~r1(Y, tptp_fun_X_26(Y))) | p2(tptp_fun_X_26(Y)))))))), rewrite(((~r1(X!0, Y)) | p3(Y) | ((~p2(Y)) | (~((~r1(Y, tptp_fun_X_26(Y))) | p2(tptp_fun_X_26(Y)))))) <=> (p3(Y) | (~r1(X!0, Y)) | (~p2(Y)) | (~((~r1(Y, tptp_fun_X_26(Y))) | p2(tptp_fun_X_26(Y)))))), (((~r1(X!0, Y)) | p3(Y) | ((~p2(Y)) | (~((~r1(Y, tptp_fun_X_26(Y))) | p2(tptp_fun_X_26(Y)))))) <=> (p3(Y) | (~r1(X!0, Y)) | (~p2(Y)) | (~((~r1(Y, tptp_fun_X_26(Y))) | p2(tptp_fun_X_26(Y)))))))),
% 0.13/0.44 inference(bind,[status(th)],[])).
% 0.13/0.44 tff(35,plain,
% 0.13/0.44 (![Y: $i] : ((~r1(X!0, Y)) | p3(Y) | ((~p2(Y)) | (~((~r1(Y, tptp_fun_X_26(Y))) | p2(tptp_fun_X_26(Y)))))) <=> ![Y: $i] : (p3(Y) | (~r1(X!0, Y)) | (~p2(Y)) | (~((~r1(Y, tptp_fun_X_26(Y))) | p2(tptp_fun_X_26(Y)))))),
% 0.13/0.44 inference(quant_intro,[status(thm)],[34])).
% 0.13/0.44 tff(36,plain,
% 0.13/0.44 (((r1(X!0, Y!21) & (~p3(Y!21)) & p2(Y!21) & ![X: $i] : (p2(X) | (~r1(Y!21, X))) & r1(Y!21, X!22) & p3(X!22) & ![Y: $i] : (p3(Y) | (~r1(X!22, Y))) & (~p2(X!22))) | (r1(X!0, Y!23) & p3(Y!23) & ![X: $i] : (p3(X) | (~r1(Y!23, X))) & (~p2(Y!23)) & r1(Y!23, X!24) & (~p3(X!24)) & p2(X!24) & ![Y: $i] : (p2(Y) | (~r1(X!24, Y)))) | $false) <=> ((r1(X!0, Y!21) & (~p3(Y!21)) & p2(Y!21) & ![X: $i] : (p2(X) | (~r1(Y!21, X))) & r1(Y!21, X!22) & p3(X!22) & ![Y: $i] : (p3(Y) | (~r1(X!22, Y))) & (~p2(X!22))) | (r1(X!0, Y!23) & p3(Y!23) & ![X: $i] : (p3(X) | (~r1(Y!23, X))) & (~p2(Y!23)) & r1(Y!23, X!24) & (~p3(X!24)) & p2(X!24) & ![Y: $i] : (p2(Y) | (~r1(X!24, Y)))))),
% 0.13/0.44 inference(rewrite,[status(thm)],[])).
% 0.13/0.44 tff(37,plain,
% 0.13/0.44 ((r1(X!0, Y!25) & (~p3(Y!25)) & (p3(Y!25) & ![X: $i] : (p3(X) | (~r1(Y!25, X)))) & (~p2(Y!25)) & (p2(Y!25) & ![X: $i] : (p2(X) | (~r1(Y!25, X))))) <=> $false),
% 0.13/0.44 inference(rewrite,[status(thm)],[])).
% 0.13/0.44 tff(38,plain,
% 0.13/0.44 ((p2(Y!25) & ![X: $i] : ((~r1(Y!25, X)) | p2(X))) <=> (p2(Y!25) & ![X: $i] : (p2(X) | (~r1(Y!25, X))))),
% 0.13/0.44 inference(rewrite,[status(thm)],[])).
% 0.13/0.44 tff(39,plain,
% 0.13/0.44 ((p3(Y!25) & ![X: $i] : ((~r1(Y!25, X)) | p3(X))) <=> (p3(Y!25) & ![X: $i] : (p3(X) | (~r1(Y!25, X))))),
% 0.13/0.44 inference(rewrite,[status(thm)],[])).
% 0.13/0.44 tff(40,plain,
% 0.13/0.44 ((r1(X!0, Y!25) & (~p3(Y!25)) & (p3(Y!25) & ![X: $i] : ((~r1(Y!25, X)) | p3(X))) & (~p2(Y!25)) & (p2(Y!25) & ![X: $i] : ((~r1(Y!25, X)) | p2(X)))) <=> (r1(X!0, Y!25) & (~p3(Y!25)) & (p3(Y!25) & ![X: $i] : (p3(X) | (~r1(Y!25, X)))) & (~p2(Y!25)) & (p2(Y!25) & ![X: $i] : (p2(X) | (~r1(Y!25, X)))))),
% 0.13/0.44 inference(monotonicity,[status(thm)],[39, 38])).
% 0.13/0.44 tff(41,plain,
% 0.13/0.44 ((r1(X!0, Y!25) & (~p3(Y!25)) & (p3(Y!25) & ![X: $i] : ((~r1(Y!25, X)) | p3(X))) & (~p2(Y!25)) & (p2(Y!25) & ![X: $i] : ((~r1(Y!25, X)) | p2(X)))) <=> $false),
% 0.13/0.44 inference(transitivity,[status(thm)],[40, 37])).
% 0.13/0.44 tff(42,plain,
% 0.13/0.44 ((r1(X!0, Y!23) & (p3(Y!23) & ![X: $i] : (p3(X) | (~r1(Y!23, X)))) & (~p2(Y!23)) & (r1(Y!23, X!24) & (~p3(X!24)) & p2(X!24) & ![Y: $i] : (p2(Y) | (~r1(X!24, Y))))) <=> (r1(X!0, Y!23) & p3(Y!23) & ![X: $i] : (p3(X) | (~r1(Y!23, X))) & (~p2(Y!23)) & r1(Y!23, X!24) & (~p3(X!24)) & p2(X!24) & ![Y: $i] : (p2(Y) | (~r1(X!24, Y))))),
% 0.13/0.44 inference(rewrite,[status(thm)],[])).
% 0.13/0.44 tff(43,plain,
% 0.13/0.44 ((r1(Y!23, X!24) & (~p3(X!24)) & (p2(X!24) & ![Y: $i] : (p2(Y) | (~r1(X!24, Y))))) <=> (r1(Y!23, X!24) & (~p3(X!24)) & p2(X!24) & ![Y: $i] : (p2(Y) | (~r1(X!24, Y))))),
% 0.13/0.44 inference(rewrite,[status(thm)],[])).
% 0.13/0.44 tff(44,plain,
% 0.13/0.44 ((p2(X!24) & ![Y: $i] : ((~r1(X!24, Y)) | p2(Y))) <=> (p2(X!24) & ![Y: $i] : (p2(Y) | (~r1(X!24, Y))))),
% 0.13/0.44 inference(rewrite,[status(thm)],[])).
% 0.13/0.44 tff(45,plain,
% 0.13/0.44 ((r1(Y!23, X!24) & (~p3(X!24)) & (p2(X!24) & ![Y: $i] : ((~r1(X!24, Y)) | p2(Y)))) <=> (r1(Y!23, X!24) & (~p3(X!24)) & (p2(X!24) & ![Y: $i] : (p2(Y) | (~r1(X!24, Y)))))),
% 0.13/0.44 inference(monotonicity,[status(thm)],[44])).
% 0.13/0.44 tff(46,plain,
% 0.13/0.44 ((r1(Y!23, X!24) & (~p3(X!24)) & (p2(X!24) & ![Y: $i] : ((~r1(X!24, Y)) | p2(Y)))) <=> (r1(Y!23, X!24) & (~p3(X!24)) & p2(X!24) & ![Y: $i] : (p2(Y) | (~r1(X!24, Y))))),
% 0.13/0.44 inference(transitivity,[status(thm)],[45, 43])).
% 0.13/0.44 tff(47,plain,
% 0.13/0.44 ((p3(Y!23) & ![X: $i] : ((~r1(Y!23, X)) | p3(X))) <=> (p3(Y!23) & ![X: $i] : (p3(X) | (~r1(Y!23, X))))),
% 0.13/0.44 inference(rewrite,[status(thm)],[])).
% 0.13/0.44 tff(48,plain,
% 0.13/0.44 ((r1(X!0, Y!23) & (p3(Y!23) & ![X: $i] : ((~r1(Y!23, X)) | p3(X))) & (~p2(Y!23)) & (r1(Y!23, X!24) & (~p3(X!24)) & (p2(X!24) & ![Y: $i] : ((~r1(X!24, Y)) | p2(Y))))) <=> (r1(X!0, Y!23) & (p3(Y!23) & ![X: $i] : (p3(X) | (~r1(Y!23, X)))) & (~p2(Y!23)) & (r1(Y!23, X!24) & (~p3(X!24)) & p2(X!24) & ![Y: $i] : (p2(Y) | (~r1(X!24, Y)))))),
% 0.13/0.44 inference(monotonicity,[status(thm)],[47, 46])).
% 0.13/0.44 tff(49,plain,
% 0.13/0.44 ((r1(X!0, Y!23) & (p3(Y!23) & ![X: $i] : ((~r1(Y!23, X)) | p3(X))) & (~p2(Y!23)) & (r1(Y!23, X!24) & (~p3(X!24)) & (p2(X!24) & ![Y: $i] : ((~r1(X!24, Y)) | p2(Y))))) <=> (r1(X!0, Y!23) & p3(Y!23) & ![X: $i] : (p3(X) | (~r1(Y!23, X))) & (~p2(Y!23)) & r1(Y!23, X!24) & (~p3(X!24)) & p2(X!24) & ![Y: $i] : (p2(Y) | (~r1(X!24, Y))))),
% 0.13/0.44 inference(transitivity,[status(thm)],[48, 42])).
% 0.13/0.44 tff(50,plain,
% 0.13/0.44 ((r1(X!0, Y!21) & (~p3(Y!21)) & (p2(Y!21) & ![X: $i] : (p2(X) | (~r1(Y!21, X)))) & (r1(Y!21, X!22) & p3(X!22) & ![Y: $i] : (p3(Y) | (~r1(X!22, Y))) & (~p2(X!22)))) <=> (r1(X!0, Y!21) & (~p3(Y!21)) & p2(Y!21) & ![X: $i] : (p2(X) | (~r1(Y!21, X))) & r1(Y!21, X!22) & p3(X!22) & ![Y: $i] : (p3(Y) | (~r1(X!22, Y))) & (~p2(X!22)))),
% 0.13/0.44 inference(rewrite,[status(thm)],[])).
% 0.13/0.44 tff(51,plain,
% 0.13/0.44 ((r1(Y!21, X!22) & (p3(X!22) & ![Y: $i] : (p3(Y) | (~r1(X!22, Y)))) & (~p2(X!22))) <=> (r1(Y!21, X!22) & p3(X!22) & ![Y: $i] : (p3(Y) | (~r1(X!22, Y))) & (~p2(X!22)))),
% 0.13/0.44 inference(rewrite,[status(thm)],[])).
% 0.13/0.44 tff(52,plain,
% 0.13/0.44 ((p3(X!22) & ![Y: $i] : ((~r1(X!22, Y)) | p3(Y))) <=> (p3(X!22) & ![Y: $i] : (p3(Y) | (~r1(X!22, Y))))),
% 0.13/0.44 inference(rewrite,[status(thm)],[])).
% 0.13/0.44 tff(53,plain,
% 0.13/0.44 ((r1(Y!21, X!22) & (p3(X!22) & ![Y: $i] : ((~r1(X!22, Y)) | p3(Y))) & (~p2(X!22))) <=> (r1(Y!21, X!22) & (p3(X!22) & ![Y: $i] : (p3(Y) | (~r1(X!22, Y)))) & (~p2(X!22)))),
% 0.13/0.44 inference(monotonicity,[status(thm)],[52])).
% 0.13/0.44 tff(54,plain,
% 0.13/0.44 ((r1(Y!21, X!22) & (p3(X!22) & ![Y: $i] : ((~r1(X!22, Y)) | p3(Y))) & (~p2(X!22))) <=> (r1(Y!21, X!22) & p3(X!22) & ![Y: $i] : (p3(Y) | (~r1(X!22, Y))) & (~p2(X!22)))),
% 0.13/0.44 inference(transitivity,[status(thm)],[53, 51])).
% 0.13/0.44 tff(55,plain,
% 0.13/0.44 ((p2(Y!21) & ![X: $i] : ((~r1(Y!21, X)) | p2(X))) <=> (p2(Y!21) & ![X: $i] : (p2(X) | (~r1(Y!21, X))))),
% 0.13/0.44 inference(rewrite,[status(thm)],[])).
% 0.13/0.44 tff(56,plain,
% 0.13/0.44 ((r1(X!0, Y!21) & (~p3(Y!21)) & (p2(Y!21) & ![X: $i] : ((~r1(Y!21, X)) | p2(X))) & (r1(Y!21, X!22) & (p3(X!22) & ![Y: $i] : ((~r1(X!22, Y)) | p3(Y))) & (~p2(X!22)))) <=> (r1(X!0, Y!21) & (~p3(Y!21)) & (p2(Y!21) & ![X: $i] : (p2(X) | (~r1(Y!21, X)))) & (r1(Y!21, X!22) & p3(X!22) & ![Y: $i] : (p3(Y) | (~r1(X!22, Y))) & (~p2(X!22))))),
% 0.13/0.44 inference(monotonicity,[status(thm)],[55, 54])).
% 0.13/0.44 tff(57,plain,
% 0.13/0.44 ((r1(X!0, Y!21) & (~p3(Y!21)) & (p2(Y!21) & ![X: $i] : ((~r1(Y!21, X)) | p2(X))) & (r1(Y!21, X!22) & (p3(X!22) & ![Y: $i] : ((~r1(X!22, Y)) | p3(Y))) & (~p2(X!22)))) <=> (r1(X!0, Y!21) & (~p3(Y!21)) & p2(Y!21) & ![X: $i] : (p2(X) | (~r1(Y!21, X))) & r1(Y!21, X!22) & p3(X!22) & ![Y: $i] : (p3(Y) | (~r1(X!22, Y))) & (~p2(X!22)))),
% 0.13/0.44 inference(transitivity,[status(thm)],[56, 50])).
% 0.13/0.44 tff(58,plain,
% 0.13/0.44 (((r1(X!0, Y!21) & (~p3(Y!21)) & (p2(Y!21) & ![X: $i] : ((~r1(Y!21, X)) | p2(X))) & (r1(Y!21, X!22) & (p3(X!22) & ![Y: $i] : ((~r1(X!22, Y)) | p3(Y))) & (~p2(X!22)))) | (r1(X!0, Y!23) & (p3(Y!23) & ![X: $i] : ((~r1(Y!23, X)) | p3(X))) & (~p2(Y!23)) & (r1(Y!23, X!24) & (~p3(X!24)) & (p2(X!24) & ![Y: $i] : ((~r1(X!24, Y)) | p2(Y))))) | (r1(X!0, Y!25) & (~p3(Y!25)) & (p3(Y!25) & ![X: $i] : ((~r1(Y!25, X)) | p3(X))) & (~p2(Y!25)) & (p2(Y!25) & ![X: $i] : ((~r1(Y!25, X)) | p2(X))))) <=> ((r1(X!0, Y!21) & (~p3(Y!21)) & p2(Y!21) & ![X: $i] : (p2(X) | (~r1(Y!21, X))) & r1(Y!21, X!22) & p3(X!22) & ![Y: $i] : (p3(Y) | (~r1(X!22, Y))) & (~p2(X!22))) | (r1(X!0, Y!23) & p3(Y!23) & ![X: $i] : (p3(X) | (~r1(Y!23, X))) & (~p2(Y!23)) & r1(Y!23, X!24) & (~p3(X!24)) & p2(X!24) & ![Y: $i] : (p2(Y) | (~r1(X!24, Y)))) | $false)),
% 0.13/0.45 inference(monotonicity,[status(thm)],[57, 49, 41])).
% 0.13/0.45 tff(59,plain,
% 0.13/0.45 (((r1(X!0, Y!21) & (~p3(Y!21)) & (p2(Y!21) & ![X: $i] : ((~r1(Y!21, X)) | p2(X))) & (r1(Y!21, X!22) & (p3(X!22) & ![Y: $i] : ((~r1(X!22, Y)) | p3(Y))) & (~p2(X!22)))) | (r1(X!0, Y!23) & (p3(Y!23) & ![X: $i] : ((~r1(Y!23, X)) | p3(X))) & (~p2(Y!23)) & (r1(Y!23, X!24) & (~p3(X!24)) & (p2(X!24) & ![Y: $i] : ((~r1(X!24, Y)) | p2(Y))))) | (r1(X!0, Y!25) & (~p3(Y!25)) & (p3(Y!25) & ![X: $i] : ((~r1(Y!25, X)) | p3(X))) & (~p2(Y!25)) & (p2(Y!25) & ![X: $i] : ((~r1(Y!25, X)) | p2(X))))) <=> ((r1(X!0, Y!21) & (~p3(Y!21)) & p2(Y!21) & ![X: $i] : (p2(X) | (~r1(Y!21, X))) & r1(Y!21, X!22) & p3(X!22) & ![Y: $i] : (p3(Y) | (~r1(X!22, Y))) & (~p2(X!22))) | (r1(X!0, Y!23) & p3(Y!23) & ![X: $i] : (p3(X) | (~r1(Y!23, X))) & (~p2(Y!23)) & r1(Y!23, X!24) & (~p3(X!24)) & p2(X!24) & ![Y: $i] : (p2(Y) | (~r1(X!24, Y)))))),
% 0.13/0.45 inference(transitivity,[status(thm)],[58, 36])).
% 0.13/0.45 tff(60,plain,
% 0.13/0.45 (^[Y: $i] : trans(monotonicity(monotonicity(rewrite((~((~r1(Y, tptp_fun_X_9(Y))) | p3(tptp_fun_X_9(Y)))) <=> (~((~r1(Y, tptp_fun_X_9(Y))) | p3(tptp_fun_X_9(Y))))), (((~p3(Y)) | (~((~r1(Y, tptp_fun_X_9(Y))) | p3(tptp_fun_X_9(Y))))) <=> ((~p3(Y)) | (~((~r1(Y, tptp_fun_X_9(Y))) | p3(tptp_fun_X_9(Y))))))), (((~r1(X!0, Y)) | ((~p3(Y)) | (~((~r1(Y, tptp_fun_X_9(Y))) | p3(tptp_fun_X_9(Y))))) | p2(Y)) <=> ((~r1(X!0, Y)) | ((~p3(Y)) | (~((~r1(Y, tptp_fun_X_9(Y))) | p3(tptp_fun_X_9(Y))))) | p2(Y)))), rewrite(((~r1(X!0, Y)) | ((~p3(Y)) | (~((~r1(Y, tptp_fun_X_9(Y))) | p3(tptp_fun_X_9(Y))))) | p2(Y)) <=> (p2(Y) | (~r1(X!0, Y)) | (~p3(Y)) | (~((~r1(Y, tptp_fun_X_9(Y))) | p3(tptp_fun_X_9(Y)))))), (((~r1(X!0, Y)) | ((~p3(Y)) | (~((~r1(Y, tptp_fun_X_9(Y))) | p3(tptp_fun_X_9(Y))))) | p2(Y)) <=> (p2(Y) | (~r1(X!0, Y)) | (~p3(Y)) | (~((~r1(Y, tptp_fun_X_9(Y))) | p3(tptp_fun_X_9(Y)))))))),
% 0.13/0.45 inference(bind,[status(th)],[])).
% 0.13/0.45 tff(61,plain,
% 0.13/0.45 (![Y: $i] : ((~r1(X!0, Y)) | ((~p3(Y)) | (~((~r1(Y, tptp_fun_X_9(Y))) | p3(tptp_fun_X_9(Y))))) | p2(Y)) <=> ![Y: $i] : (p2(Y) | (~r1(X!0, Y)) | (~p3(Y)) | (~((~r1(Y, tptp_fun_X_9(Y))) | p3(tptp_fun_X_9(Y)))))),
% 0.13/0.45 inference(quant_intro,[status(thm)],[60])).
% 0.13/0.45 tff(62,plain,
% 0.13/0.45 ((![Y: $i] : ((~r1(X!0, Y)) | ((~p3(Y)) | (~((~r1(Y, tptp_fun_X_9(Y))) | p3(tptp_fun_X_9(Y))))) | p2(Y)) | ((r1(X!0, Y!21) & (~p3(Y!21)) & (p2(Y!21) & ![X: $i] : ((~r1(Y!21, X)) | p2(X))) & (r1(Y!21, X!22) & (p3(X!22) & ![Y: $i] : ((~r1(X!22, Y)) | p3(Y))) & (~p2(X!22)))) | (r1(X!0, Y!23) & (p3(Y!23) & ![X: $i] : ((~r1(Y!23, X)) | p3(X))) & (~p2(Y!23)) & (r1(Y!23, X!24) & (~p3(X!24)) & (p2(X!24) & ![Y: $i] : ((~r1(X!24, Y)) | p2(Y))))) | (r1(X!0, Y!25) & (~p3(Y!25)) & (p3(Y!25) & ![X: $i] : ((~r1(Y!25, X)) | p3(X))) & (~p2(Y!25)) & (p2(Y!25) & ![X: $i] : ((~r1(Y!25, X)) | p2(X))))) | ![Y: $i] : ((~r1(X!0, Y)) | p3(Y) | ((~p2(Y)) | (~((~r1(Y, tptp_fun_X_26(Y))) | p2(tptp_fun_X_26(Y))))))) <=> (![Y: $i] : (p2(Y) | (~r1(X!0, Y)) | (~p3(Y)) | (~((~r1(Y, tptp_fun_X_9(Y))) | p3(tptp_fun_X_9(Y))))) | ((r1(X!0, Y!21) & (~p3(Y!21)) & p2(Y!21) & ![X: $i] : (p2(X) | (~r1(Y!21, X))) & r1(Y!21, X!22) & p3(X!22) & ![Y: $i] : (p3(Y) | (~r1(X!22, Y))) & (~p2(X!22))) | (r1(X!0, Y!23) & p3(Y!23) & ![X: $i] : (p3(X) | (~r1(Y!23, X))) & (~p2(Y!23)) & r1(Y!23, X!24) & (~p3(X!24)) & p2(X!24) & ![Y: $i] : (p2(Y) | (~r1(X!24, Y))))) | ![Y: $i] : (p3(Y) | (~r1(X!0, Y)) | (~p2(Y)) | (~((~r1(Y, tptp_fun_X_26(Y))) | p2(tptp_fun_X_26(Y))))))),
% 0.13/0.45 inference(monotonicity,[status(thm)],[61, 59, 35])).
% 0.13/0.45 tff(63,plain,
% 0.13/0.45 ((![Y: $i] : ((~r1(X!0, Y)) | ((~p3(Y)) | (~((~r1(Y, tptp_fun_X_9(Y))) | p3(tptp_fun_X_9(Y))))) | p2(Y)) | ((r1(X!0, Y!21) & (~p3(Y!21)) & (p2(Y!21) & ![X: $i] : ((~r1(Y!21, X)) | p2(X))) & (r1(Y!21, X!22) & (p3(X!22) & ![Y: $i] : ((~r1(X!22, Y)) | p3(Y))) & (~p2(X!22)))) | (r1(X!0, Y!23) & (p3(Y!23) & ![X: $i] : ((~r1(Y!23, X)) | p3(X))) & (~p2(Y!23)) & (r1(Y!23, X!24) & (~p3(X!24)) & (p2(X!24) & ![Y: $i] : ((~r1(X!24, Y)) | p2(Y))))) | (r1(X!0, Y!25) & (~p3(Y!25)) & (p3(Y!25) & ![X: $i] : ((~r1(Y!25, X)) | p3(X))) & (~p2(Y!25)) & (p2(Y!25) & ![X: $i] : ((~r1(Y!25, X)) | p2(X))))) | ![Y: $i] : ((~r1(X!0, Y)) | p3(Y) | ((~p2(Y)) | (~((~r1(Y, tptp_fun_X_26(Y))) | p2(tptp_fun_X_26(Y))))))) <=> (![Y: $i] : (p2(Y) | (~r1(X!0, Y)) | (~p3(Y)) | (~((~r1(Y, tptp_fun_X_9(Y))) | p3(tptp_fun_X_9(Y))))) | (r1(X!0, Y!21) & (~p3(Y!21)) & p2(Y!21) & ![X: $i] : (p2(X) | (~r1(Y!21, X))) & r1(Y!21, X!22) & p3(X!22) & ![Y: $i] : (p3(Y) | (~r1(X!22, Y))) & (~p2(X!22))) | (r1(X!0, Y!23) & p3(Y!23) & ![X: $i] : (p3(X) | (~r1(Y!23, X))) & (~p2(Y!23)) & r1(Y!23, X!24) & (~p3(X!24)) & p2(X!24) & ![Y: $i] : (p2(Y) | (~r1(X!24, Y)))) | ![Y: $i] : (p3(Y) | (~r1(X!0, Y)) | (~p2(Y)) | (~((~r1(Y, tptp_fun_X_26(Y))) | p2(tptp_fun_X_26(Y))))))),
% 0.13/0.45 inference(transitivity,[status(thm)],[62, 33])).
% 0.13/0.45 tff(64,plain,
% 0.13/0.45 (((~p5(Y!20)) & r1(X!0, Y!20) & (![X: $i] : (p5(X) | (~r1(Y!20, X))) & p5(Y!20))) <=> $false),
% 0.13/0.45 inference(rewrite,[status(thm)],[])).
% 0.13/0.45 tff(65,plain,
% 0.13/0.45 ((![X: $i] : (p5(X) | (~r1(Y!20, X))) & p5(Y!20)) <=> (![X: $i] : (p5(X) | (~r1(Y!20, X))) & p5(Y!20))),
% 0.13/0.45 inference(rewrite,[status(thm)],[])).
% 0.13/0.45 tff(66,plain,
% 0.13/0.45 (((~p5(Y!20)) & r1(X!0, Y!20) & (![X: $i] : (p5(X) | (~r1(Y!20, X))) & p5(Y!20))) <=> ((~p5(Y!20)) & r1(X!0, Y!20) & (![X: $i] : (p5(X) | (~r1(Y!20, X))) & p5(Y!20)))),
% 0.13/0.45 inference(monotonicity,[status(thm)],[65])).
% 0.13/0.45 tff(67,plain,
% 0.13/0.45 (((~p5(Y!20)) & r1(X!0, Y!20) & (![X: $i] : (p5(X) | (~r1(Y!20, X))) & p5(Y!20))) <=> $false),
% 0.13/0.45 inference(transitivity,[status(thm)],[66, 64])).
% 0.13/0.45 tff(68,plain,
% 0.13/0.45 ((![Y: $i] : (p4(Y) | (~p5(Y)) | (~r1(X!0, Y)) | (~(p5(tptp_fun_X_2(Y)) | (~r1(Y, tptp_fun_X_2(Y)))))) | (((~p5(Y!15)) & r1(X!0, Y!15) & p4(Y!15) & ![X: $i] : (p4(X) | (~r1(Y!15, X))) & r1(Y!15, X!16) & (~p4(X!16)) & p5(X!16) & ![Y: $i] : (p5(Y) | (~r1(X!16, Y)))) | (r1(X!0, Y!17) & (~p4(Y!17)) & p5(Y!17) & ![X: $i] : (p5(X) | (~r1(Y!17, X))) & (~p5(X!18)) & r1(Y!17, X!18) & p4(X!18) & ![Y: $i] : (p4(Y) | (~r1(X!18, Y))))) | ![Y: $i] : (p5(Y) | (~r1(X!0, Y)) | (~p4(Y)) | (~((~r1(Y, tptp_fun_X_8(Y))) | p4(tptp_fun_X_8(Y)))))) <=> (![Y: $i] : (p4(Y) | (~p5(Y)) | (~r1(X!0, Y)) | (~(p5(tptp_fun_X_2(Y)) | (~r1(Y, tptp_fun_X_2(Y)))))) | ((~p5(Y!15)) & r1(X!0, Y!15) & p4(Y!15) & ![X: $i] : (p4(X) | (~r1(Y!15, X))) & r1(Y!15, X!16) & (~p4(X!16)) & p5(X!16) & ![Y: $i] : (p5(Y) | (~r1(X!16, Y)))) | (r1(X!0, Y!17) & (~p4(Y!17)) & p5(Y!17) & ![X: $i] : (p5(X) | (~r1(Y!17, X))) & (~p5(X!18)) & r1(Y!17, X!18) & p4(X!18) & ![Y: $i] : (p4(Y) | (~r1(X!18, Y)))) | ![Y: $i] : (p5(Y) | (~r1(X!0, Y)) | (~p4(Y)) | (~((~r1(Y, tptp_fun_X_8(Y))) | p4(tptp_fun_X_8(Y))))))),
% 0.13/0.45 inference(rewrite,[status(thm)],[])).
% 0.13/0.45 tff(69,plain,
% 0.13/0.45 (^[Y: $i] : trans(monotonicity(monotonicity(rewrite((~((~r1(Y, tptp_fun_X_8(Y))) | p4(tptp_fun_X_8(Y)))) <=> (~((~r1(Y, tptp_fun_X_8(Y))) | p4(tptp_fun_X_8(Y))))), (((~p4(Y)) | (~((~r1(Y, tptp_fun_X_8(Y))) | p4(tptp_fun_X_8(Y))))) <=> ((~p4(Y)) | (~((~r1(Y, tptp_fun_X_8(Y))) | p4(tptp_fun_X_8(Y))))))), ((p5(Y) | (~r1(X!0, Y)) | ((~p4(Y)) | (~((~r1(Y, tptp_fun_X_8(Y))) | p4(tptp_fun_X_8(Y)))))) <=> (p5(Y) | (~r1(X!0, Y)) | ((~p4(Y)) | (~((~r1(Y, tptp_fun_X_8(Y))) | p4(tptp_fun_X_8(Y)))))))), rewrite((p5(Y) | (~r1(X!0, Y)) | ((~p4(Y)) | (~((~r1(Y, tptp_fun_X_8(Y))) | p4(tptp_fun_X_8(Y)))))) <=> (p5(Y) | (~r1(X!0, Y)) | (~p4(Y)) | (~((~r1(Y, tptp_fun_X_8(Y))) | p4(tptp_fun_X_8(Y)))))), ((p5(Y) | (~r1(X!0, Y)) | ((~p4(Y)) | (~((~r1(Y, tptp_fun_X_8(Y))) | p4(tptp_fun_X_8(Y)))))) <=> (p5(Y) | (~r1(X!0, Y)) | (~p4(Y)) | (~((~r1(Y, tptp_fun_X_8(Y))) | p4(tptp_fun_X_8(Y)))))))),
% 0.13/0.45 inference(bind,[status(th)],[])).
% 0.13/0.45 tff(70,plain,
% 0.13/0.45 (![Y: $i] : (p5(Y) | (~r1(X!0, Y)) | ((~p4(Y)) | (~((~r1(Y, tptp_fun_X_8(Y))) | p4(tptp_fun_X_8(Y)))))) <=> ![Y: $i] : (p5(Y) | (~r1(X!0, Y)) | (~p4(Y)) | (~((~r1(Y, tptp_fun_X_8(Y))) | p4(tptp_fun_X_8(Y)))))),
% 0.13/0.45 inference(quant_intro,[status(thm)],[69])).
% 0.13/0.45 tff(71,plain,
% 0.13/0.45 ((((~p5(Y!15)) & r1(X!0, Y!15) & p4(Y!15) & ![X: $i] : (p4(X) | (~r1(Y!15, X))) & r1(Y!15, X!16) & (~p4(X!16)) & p5(X!16) & ![Y: $i] : (p5(Y) | (~r1(X!16, Y)))) | (r1(X!0, Y!17) & (~p4(Y!17)) & p5(Y!17) & ![X: $i] : (p5(X) | (~r1(Y!17, X))) & (~p5(X!18)) & r1(Y!17, X!18) & p4(X!18) & ![Y: $i] : (p4(Y) | (~r1(X!18, Y)))) | $false) <=> (((~p5(Y!15)) & r1(X!0, Y!15) & p4(Y!15) & ![X: $i] : (p4(X) | (~r1(Y!15, X))) & r1(Y!15, X!16) & (~p4(X!16)) & p5(X!16) & ![Y: $i] : (p5(Y) | (~r1(X!16, Y)))) | (r1(X!0, Y!17) & (~p4(Y!17)) & p5(Y!17) & ![X: $i] : (p5(X) | (~r1(Y!17, X))) & (~p5(X!18)) & r1(Y!17, X!18) & p4(X!18) & ![Y: $i] : (p4(Y) | (~r1(X!18, Y)))))),
% 0.13/0.45 inference(rewrite,[status(thm)],[])).
% 0.13/0.45 tff(72,plain,
% 0.13/0.45 (((~p5(Y!19)) & r1(X!0, Y!19) & (~p4(Y!19)) & (p4(Y!19) & ![X: $i] : (p4(X) | (~r1(Y!19, X)))) & (p5(Y!19) & ![X: $i] : (p5(X) | (~r1(Y!19, X))))) <=> $false),
% 0.13/0.45 inference(rewrite,[status(thm)],[])).
% 0.13/0.45 tff(73,plain,
% 0.13/0.45 ((p5(Y!19) & ![X: $i] : (p5(X) | (~r1(Y!19, X)))) <=> (p5(Y!19) & ![X: $i] : (p5(X) | (~r1(Y!19, X))))),
% 0.13/0.45 inference(rewrite,[status(thm)],[])).
% 0.13/0.45 tff(74,plain,
% 0.13/0.45 ((p4(Y!19) & ![X: $i] : ((~r1(Y!19, X)) | p4(X))) <=> (p4(Y!19) & ![X: $i] : (p4(X) | (~r1(Y!19, X))))),
% 0.13/0.45 inference(rewrite,[status(thm)],[])).
% 0.13/0.45 tff(75,plain,
% 0.13/0.45 (((~p5(Y!19)) & r1(X!0, Y!19) & (~p4(Y!19)) & (p4(Y!19) & ![X: $i] : ((~r1(Y!19, X)) | p4(X))) & (p5(Y!19) & ![X: $i] : (p5(X) | (~r1(Y!19, X))))) <=> ((~p5(Y!19)) & r1(X!0, Y!19) & (~p4(Y!19)) & (p4(Y!19) & ![X: $i] : (p4(X) | (~r1(Y!19, X)))) & (p5(Y!19) & ![X: $i] : (p5(X) | (~r1(Y!19, X)))))),
% 0.13/0.45 inference(monotonicity,[status(thm)],[74, 73])).
% 0.13/0.45 tff(76,plain,
% 0.13/0.45 (((~p5(Y!19)) & r1(X!0, Y!19) & (~p4(Y!19)) & (p4(Y!19) & ![X: $i] : ((~r1(Y!19, X)) | p4(X))) & (p5(Y!19) & ![X: $i] : (p5(X) | (~r1(Y!19, X))))) <=> $false),
% 0.13/0.45 inference(transitivity,[status(thm)],[75, 72])).
% 0.13/0.45 tff(77,plain,
% 0.13/0.45 ((r1(X!0, Y!17) & (~p4(Y!17)) & (p5(Y!17) & ![X: $i] : (p5(X) | (~r1(Y!17, X)))) & ((~p5(X!18)) & r1(Y!17, X!18) & p4(X!18) & ![Y: $i] : (p4(Y) | (~r1(X!18, Y))))) <=> (r1(X!0, Y!17) & (~p4(Y!17)) & p5(Y!17) & ![X: $i] : (p5(X) | (~r1(Y!17, X))) & (~p5(X!18)) & r1(Y!17, X!18) & p4(X!18) & ![Y: $i] : (p4(Y) | (~r1(X!18, Y))))),
% 0.13/0.45 inference(rewrite,[status(thm)],[])).
% 0.13/0.45 tff(78,plain,
% 0.13/0.45 (((~p5(X!18)) & r1(Y!17, X!18) & (p4(X!18) & ![Y: $i] : (p4(Y) | (~r1(X!18, Y))))) <=> ((~p5(X!18)) & r1(Y!17, X!18) & p4(X!18) & ![Y: $i] : (p4(Y) | (~r1(X!18, Y))))),
% 0.13/0.45 inference(rewrite,[status(thm)],[])).
% 0.13/0.45 tff(79,plain,
% 0.13/0.45 ((p4(X!18) & ![Y: $i] : ((~r1(X!18, Y)) | p4(Y))) <=> (p4(X!18) & ![Y: $i] : (p4(Y) | (~r1(X!18, Y))))),
% 0.13/0.45 inference(rewrite,[status(thm)],[])).
% 0.13/0.45 tff(80,plain,
% 0.13/0.45 (((~p5(X!18)) & r1(Y!17, X!18) & (p4(X!18) & ![Y: $i] : ((~r1(X!18, Y)) | p4(Y)))) <=> ((~p5(X!18)) & r1(Y!17, X!18) & (p4(X!18) & ![Y: $i] : (p4(Y) | (~r1(X!18, Y)))))),
% 0.13/0.45 inference(monotonicity,[status(thm)],[79])).
% 0.13/0.45 tff(81,plain,
% 0.13/0.45 (((~p5(X!18)) & r1(Y!17, X!18) & (p4(X!18) & ![Y: $i] : ((~r1(X!18, Y)) | p4(Y)))) <=> ((~p5(X!18)) & r1(Y!17, X!18) & p4(X!18) & ![Y: $i] : (p4(Y) | (~r1(X!18, Y))))),
% 0.13/0.45 inference(transitivity,[status(thm)],[80, 78])).
% 0.13/0.45 tff(82,plain,
% 0.13/0.45 ((p5(Y!17) & ![X: $i] : (p5(X) | (~r1(Y!17, X)))) <=> (p5(Y!17) & ![X: $i] : (p5(X) | (~r1(Y!17, X))))),
% 0.13/0.45 inference(rewrite,[status(thm)],[])).
% 0.13/0.45 tff(83,plain,
% 0.13/0.45 ((r1(X!0, Y!17) & (~p4(Y!17)) & (p5(Y!17) & ![X: $i] : (p5(X) | (~r1(Y!17, X)))) & ((~p5(X!18)) & r1(Y!17, X!18) & (p4(X!18) & ![Y: $i] : ((~r1(X!18, Y)) | p4(Y))))) <=> (r1(X!0, Y!17) & (~p4(Y!17)) & (p5(Y!17) & ![X: $i] : (p5(X) | (~r1(Y!17, X)))) & ((~p5(X!18)) & r1(Y!17, X!18) & p4(X!18) & ![Y: $i] : (p4(Y) | (~r1(X!18, Y)))))),
% 0.13/0.45 inference(monotonicity,[status(thm)],[82, 81])).
% 0.13/0.45 tff(84,plain,
% 0.13/0.45 ((r1(X!0, Y!17) & (~p4(Y!17)) & (p5(Y!17) & ![X: $i] : (p5(X) | (~r1(Y!17, X)))) & ((~p5(X!18)) & r1(Y!17, X!18) & (p4(X!18) & ![Y: $i] : ((~r1(X!18, Y)) | p4(Y))))) <=> (r1(X!0, Y!17) & (~p4(Y!17)) & p5(Y!17) & ![X: $i] : (p5(X) | (~r1(Y!17, X))) & (~p5(X!18)) & r1(Y!17, X!18) & p4(X!18) & ![Y: $i] : (p4(Y) | (~r1(X!18, Y))))),
% 0.13/0.45 inference(transitivity,[status(thm)],[83, 77])).
% 0.13/0.45 tff(85,plain,
% 0.13/0.45 (((~p5(Y!15)) & r1(X!0, Y!15) & (p4(Y!15) & ![X: $i] : (p4(X) | (~r1(Y!15, X)))) & (r1(Y!15, X!16) & (~p4(X!16)) & p5(X!16) & ![Y: $i] : (p5(Y) | (~r1(X!16, Y))))) <=> ((~p5(Y!15)) & r1(X!0, Y!15) & p4(Y!15) & ![X: $i] : (p4(X) | (~r1(Y!15, X))) & r1(Y!15, X!16) & (~p4(X!16)) & p5(X!16) & ![Y: $i] : (p5(Y) | (~r1(X!16, Y))))),
% 0.13/0.46 inference(rewrite,[status(thm)],[])).
% 0.13/0.46 tff(86,plain,
% 0.13/0.46 ((r1(Y!15, X!16) & (~p4(X!16)) & (p5(X!16) & ![Y: $i] : (p5(Y) | (~r1(X!16, Y))))) <=> (r1(Y!15, X!16) & (~p4(X!16)) & p5(X!16) & ![Y: $i] : (p5(Y) | (~r1(X!16, Y))))),
% 0.13/0.46 inference(rewrite,[status(thm)],[])).
% 0.13/0.46 tff(87,plain,
% 0.13/0.46 ((p5(X!16) & ![Y: $i] : (p5(Y) | (~r1(X!16, Y)))) <=> (p5(X!16) & ![Y: $i] : (p5(Y) | (~r1(X!16, Y))))),
% 0.13/0.46 inference(rewrite,[status(thm)],[])).
% 0.13/0.46 tff(88,plain,
% 0.13/0.46 ((r1(Y!15, X!16) & (~p4(X!16)) & (p5(X!16) & ![Y: $i] : (p5(Y) | (~r1(X!16, Y))))) <=> (r1(Y!15, X!16) & (~p4(X!16)) & (p5(X!16) & ![Y: $i] : (p5(Y) | (~r1(X!16, Y)))))),
% 0.13/0.46 inference(monotonicity,[status(thm)],[87])).
% 0.13/0.46 tff(89,plain,
% 0.13/0.46 ((r1(Y!15, X!16) & (~p4(X!16)) & (p5(X!16) & ![Y: $i] : (p5(Y) | (~r1(X!16, Y))))) <=> (r1(Y!15, X!16) & (~p4(X!16)) & p5(X!16) & ![Y: $i] : (p5(Y) | (~r1(X!16, Y))))),
% 0.13/0.46 inference(transitivity,[status(thm)],[88, 86])).
% 0.13/0.46 tff(90,plain,
% 0.13/0.46 ((p4(Y!15) & ![X: $i] : ((~r1(Y!15, X)) | p4(X))) <=> (p4(Y!15) & ![X: $i] : (p4(X) | (~r1(Y!15, X))))),
% 0.13/0.46 inference(rewrite,[status(thm)],[])).
% 0.13/0.46 tff(91,plain,
% 0.13/0.46 (((~p5(Y!15)) & r1(X!0, Y!15) & (p4(Y!15) & ![X: $i] : ((~r1(Y!15, X)) | p4(X))) & (r1(Y!15, X!16) & (~p4(X!16)) & (p5(X!16) & ![Y: $i] : (p5(Y) | (~r1(X!16, Y)))))) <=> ((~p5(Y!15)) & r1(X!0, Y!15) & (p4(Y!15) & ![X: $i] : (p4(X) | (~r1(Y!15, X)))) & (r1(Y!15, X!16) & (~p4(X!16)) & p5(X!16) & ![Y: $i] : (p5(Y) | (~r1(X!16, Y)))))),
% 0.13/0.46 inference(monotonicity,[status(thm)],[90, 89])).
% 0.13/0.46 tff(92,plain,
% 0.13/0.46 (((~p5(Y!15)) & r1(X!0, Y!15) & (p4(Y!15) & ![X: $i] : ((~r1(Y!15, X)) | p4(X))) & (r1(Y!15, X!16) & (~p4(X!16)) & (p5(X!16) & ![Y: $i] : (p5(Y) | (~r1(X!16, Y)))))) <=> ((~p5(Y!15)) & r1(X!0, Y!15) & p4(Y!15) & ![X: $i] : (p4(X) | (~r1(Y!15, X))) & r1(Y!15, X!16) & (~p4(X!16)) & p5(X!16) & ![Y: $i] : (p5(Y) | (~r1(X!16, Y))))),
% 0.13/0.46 inference(transitivity,[status(thm)],[91, 85])).
% 0.13/0.46 tff(93,plain,
% 0.13/0.46 ((((~p5(Y!15)) & r1(X!0, Y!15) & (p4(Y!15) & ![X: $i] : ((~r1(Y!15, X)) | p4(X))) & (r1(Y!15, X!16) & (~p4(X!16)) & (p5(X!16) & ![Y: $i] : (p5(Y) | (~r1(X!16, Y)))))) | (r1(X!0, Y!17) & (~p4(Y!17)) & (p5(Y!17) & ![X: $i] : (p5(X) | (~r1(Y!17, X)))) & ((~p5(X!18)) & r1(Y!17, X!18) & (p4(X!18) & ![Y: $i] : ((~r1(X!18, Y)) | p4(Y))))) | ((~p5(Y!19)) & r1(X!0, Y!19) & (~p4(Y!19)) & (p4(Y!19) & ![X: $i] : ((~r1(Y!19, X)) | p4(X))) & (p5(Y!19) & ![X: $i] : (p5(X) | (~r1(Y!19, X)))))) <=> (((~p5(Y!15)) & r1(X!0, Y!15) & p4(Y!15) & ![X: $i] : (p4(X) | (~r1(Y!15, X))) & r1(Y!15, X!16) & (~p4(X!16)) & p5(X!16) & ![Y: $i] : (p5(Y) | (~r1(X!16, Y)))) | (r1(X!0, Y!17) & (~p4(Y!17)) & p5(Y!17) & ![X: $i] : (p5(X) | (~r1(Y!17, X))) & (~p5(X!18)) & r1(Y!17, X!18) & p4(X!18) & ![Y: $i] : (p4(Y) | (~r1(X!18, Y)))) | $false)),
% 0.13/0.46 inference(monotonicity,[status(thm)],[92, 84, 76])).
% 0.13/0.46 tff(94,plain,
% 0.13/0.46 ((((~p5(Y!15)) & r1(X!0, Y!15) & (p4(Y!15) & ![X: $i] : ((~r1(Y!15, X)) | p4(X))) & (r1(Y!15, X!16) & (~p4(X!16)) & (p5(X!16) & ![Y: $i] : (p5(Y) | (~r1(X!16, Y)))))) | (r1(X!0, Y!17) & (~p4(Y!17)) & (p5(Y!17) & ![X: $i] : (p5(X) | (~r1(Y!17, X)))) & ((~p5(X!18)) & r1(Y!17, X!18) & (p4(X!18) & ![Y: $i] : ((~r1(X!18, Y)) | p4(Y))))) | ((~p5(Y!19)) & r1(X!0, Y!19) & (~p4(Y!19)) & (p4(Y!19) & ![X: $i] : ((~r1(Y!19, X)) | p4(X))) & (p5(Y!19) & ![X: $i] : (p5(X) | (~r1(Y!19, X)))))) <=> (((~p5(Y!15)) & r1(X!0, Y!15) & p4(Y!15) & ![X: $i] : (p4(X) | (~r1(Y!15, X))) & r1(Y!15, X!16) & (~p4(X!16)) & p5(X!16) & ![Y: $i] : (p5(Y) | (~r1(X!16, Y)))) | (r1(X!0, Y!17) & (~p4(Y!17)) & p5(Y!17) & ![X: $i] : (p5(X) | (~r1(Y!17, X))) & (~p5(X!18)) & r1(Y!17, X!18) & p4(X!18) & ![Y: $i] : (p4(Y) | (~r1(X!18, Y)))))),
% 0.13/0.46 inference(transitivity,[status(thm)],[93, 71])).
% 0.13/0.46 tff(95,plain,
% 0.13/0.46 (^[Y: $i] : rewrite(((~r1(X!0, Y)) | p4(Y) | ((~p5(Y)) | (~(p5(tptp_fun_X_2(Y)) | (~r1(Y, tptp_fun_X_2(Y))))))) <=> (p4(Y) | (~p5(Y)) | (~r1(X!0, Y)) | (~(p5(tptp_fun_X_2(Y)) | (~r1(Y, tptp_fun_X_2(Y)))))))),
% 0.13/0.46 inference(bind,[status(th)],[])).
% 0.13/0.46 tff(96,plain,
% 0.13/0.46 (![Y: $i] : ((~r1(X!0, Y)) | p4(Y) | ((~p5(Y)) | (~(p5(tptp_fun_X_2(Y)) | (~r1(Y, tptp_fun_X_2(Y))))))) <=> ![Y: $i] : (p4(Y) | (~p5(Y)) | (~r1(X!0, Y)) | (~(p5(tptp_fun_X_2(Y)) | (~r1(Y, tptp_fun_X_2(Y))))))),
% 0.22/0.46 inference(quant_intro,[status(thm)],[95])).
% 0.22/0.46 tff(97,plain,
% 0.22/0.46 ((![Y: $i] : ((~r1(X!0, Y)) | p4(Y) | ((~p5(Y)) | (~(p5(tptp_fun_X_2(Y)) | (~r1(Y, tptp_fun_X_2(Y))))))) | (((~p5(Y!15)) & r1(X!0, Y!15) & (p4(Y!15) & ![X: $i] : ((~r1(Y!15, X)) | p4(X))) & (r1(Y!15, X!16) & (~p4(X!16)) & (p5(X!16) & ![Y: $i] : (p5(Y) | (~r1(X!16, Y)))))) | (r1(X!0, Y!17) & (~p4(Y!17)) & (p5(Y!17) & ![X: $i] : (p5(X) | (~r1(Y!17, X)))) & ((~p5(X!18)) & r1(Y!17, X!18) & (p4(X!18) & ![Y: $i] : ((~r1(X!18, Y)) | p4(Y))))) | ((~p5(Y!19)) & r1(X!0, Y!19) & (~p4(Y!19)) & (p4(Y!19) & ![X: $i] : ((~r1(Y!19, X)) | p4(X))) & (p5(Y!19) & ![X: $i] : (p5(X) | (~r1(Y!19, X)))))) | ![Y: $i] : (p5(Y) | (~r1(X!0, Y)) | ((~p4(Y)) | (~((~r1(Y, tptp_fun_X_8(Y))) | p4(tptp_fun_X_8(Y))))))) <=> (![Y: $i] : (p4(Y) | (~p5(Y)) | (~r1(X!0, Y)) | (~(p5(tptp_fun_X_2(Y)) | (~r1(Y, tptp_fun_X_2(Y)))))) | (((~p5(Y!15)) & r1(X!0, Y!15) & p4(Y!15) & ![X: $i] : (p4(X) | (~r1(Y!15, X))) & r1(Y!15, X!16) & (~p4(X!16)) & p5(X!16) & ![Y: $i] : (p5(Y) | (~r1(X!16, Y)))) | (r1(X!0, Y!17) & (~p4(Y!17)) & p5(Y!17) & ![X: $i] : (p5(X) | (~r1(Y!17, X))) & (~p5(X!18)) & r1(Y!17, X!18) & p4(X!18) & ![Y: $i] : (p4(Y) | (~r1(X!18, Y))))) | ![Y: $i] : (p5(Y) | (~r1(X!0, Y)) | (~p4(Y)) | (~((~r1(Y, tptp_fun_X_8(Y))) | p4(tptp_fun_X_8(Y))))))),
% 0.22/0.46 inference(monotonicity,[status(thm)],[96, 94, 70])).
% 0.22/0.46 tff(98,plain,
% 0.22/0.46 ((![Y: $i] : ((~r1(X!0, Y)) | p4(Y) | ((~p5(Y)) | (~(p5(tptp_fun_X_2(Y)) | (~r1(Y, tptp_fun_X_2(Y))))))) | (((~p5(Y!15)) & r1(X!0, Y!15) & (p4(Y!15) & ![X: $i] : ((~r1(Y!15, X)) | p4(X))) & (r1(Y!15, X!16) & (~p4(X!16)) & (p5(X!16) & ![Y: $i] : (p5(Y) | (~r1(X!16, Y)))))) | (r1(X!0, Y!17) & (~p4(Y!17)) & (p5(Y!17) & ![X: $i] : (p5(X) | (~r1(Y!17, X)))) & ((~p5(X!18)) & r1(Y!17, X!18) & (p4(X!18) & ![Y: $i] : ((~r1(X!18, Y)) | p4(Y))))) | ((~p5(Y!19)) & r1(X!0, Y!19) & (~p4(Y!19)) & (p4(Y!19) & ![X: $i] : ((~r1(Y!19, X)) | p4(X))) & (p5(Y!19) & ![X: $i] : (p5(X) | (~r1(Y!19, X)))))) | ![Y: $i] : (p5(Y) | (~r1(X!0, Y)) | ((~p4(Y)) | (~((~r1(Y, tptp_fun_X_8(Y))) | p4(tptp_fun_X_8(Y))))))) <=> (![Y: $i] : (p4(Y) | (~p5(Y)) | (~r1(X!0, Y)) | (~(p5(tptp_fun_X_2(Y)) | (~r1(Y, tptp_fun_X_2(Y)))))) | ((~p5(Y!15)) & r1(X!0, Y!15) & p4(Y!15) & ![X: $i] : (p4(X) | (~r1(Y!15, X))) & r1(Y!15, X!16) & (~p4(X!16)) & p5(X!16) & ![Y: $i] : (p5(Y) | (~r1(X!16, Y)))) | (r1(X!0, Y!17) & (~p4(Y!17)) & p5(Y!17) & ![X: $i] : (p5(X) | (~r1(Y!17, X))) & (~p5(X!18)) & r1(Y!17, X!18) & p4(X!18) & ![Y: $i] : (p4(Y) | (~r1(X!18, Y)))) | ![Y: $i] : (p5(Y) | (~r1(X!0, Y)) | (~p4(Y)) | (~((~r1(Y, tptp_fun_X_8(Y))) | p4(tptp_fun_X_8(Y))))))),
% 0.22/0.46 inference(transitivity,[status(thm)],[97, 68])).
% 0.22/0.46 tff(99,plain,
% 0.22/0.46 ((![Y: $i] : (p3(Y) | (~r1(X!0, Y)) | (~p4(Y)) | (~((~r1(Y, tptp_fun_X_8(Y))) | p4(tptp_fun_X_8(Y))))) | ![Y: $i] : (p4(Y) | (~r1(X!0, Y)) | (~p3(Y)) | (~((~r1(Y, tptp_fun_X_9(Y))) | p3(tptp_fun_X_9(Y))))) | ((r1(X!0, Y!10) & (~p4(Y!10)) & r1(Y!10, X!11) & p4(X!11) & ![Y: $i] : (p4(Y) | (~r1(X!11, Y))) & (~p3(X!11)) & p3(Y!10) & ![X: $i] : (p3(X) | (~r1(Y!10, X)))) | (r1(X!0, Y!12) & p4(Y!12) & ![X: $i] : (p4(X) | (~r1(Y!12, X))) & (~p3(Y!12)) & r1(Y!12, X!13) & (~p4(X!13)) & p3(X!13) & ![Y: $i] : (p3(Y) | (~r1(X!13, Y)))))) <=> (![Y: $i] : (p3(Y) | (~r1(X!0, Y)) | (~p4(Y)) | (~((~r1(Y, tptp_fun_X_8(Y))) | p4(tptp_fun_X_8(Y))))) | ![Y: $i] : (p4(Y) | (~r1(X!0, Y)) | (~p3(Y)) | (~((~r1(Y, tptp_fun_X_9(Y))) | p3(tptp_fun_X_9(Y))))) | (r1(X!0, Y!10) & (~p4(Y!10)) & r1(Y!10, X!11) & p4(X!11) & ![Y: $i] : (p4(Y) | (~r1(X!11, Y))) & (~p3(X!11)) & p3(Y!10) & ![X: $i] : (p3(X) | (~r1(Y!10, X)))) | (r1(X!0, Y!12) & p4(Y!12) & ![X: $i] : (p4(X) | (~r1(Y!12, X))) & (~p3(Y!12)) & r1(Y!12, X!13) & (~p4(X!13)) & p3(X!13) & ![Y: $i] : (p3(Y) | (~r1(X!13, Y)))))),
% 0.22/0.46 inference(rewrite,[status(thm)],[])).
% 0.22/0.46 tff(100,plain,
% 0.22/0.46 (((r1(X!0, Y!10) & (~p4(Y!10)) & r1(Y!10, X!11) & p4(X!11) & ![Y: $i] : (p4(Y) | (~r1(X!11, Y))) & (~p3(X!11)) & p3(Y!10) & ![X: $i] : (p3(X) | (~r1(Y!10, X)))) | (r1(X!0, Y!12) & p4(Y!12) & ![X: $i] : (p4(X) | (~r1(Y!12, X))) & (~p3(Y!12)) & r1(Y!12, X!13) & (~p4(X!13)) & p3(X!13) & ![Y: $i] : (p3(Y) | (~r1(X!13, Y)))) | $false) <=> ((r1(X!0, Y!10) & (~p4(Y!10)) & r1(Y!10, X!11) & p4(X!11) & ![Y: $i] : (p4(Y) | (~r1(X!11, Y))) & (~p3(X!11)) & p3(Y!10) & ![X: $i] : (p3(X) | (~r1(Y!10, X)))) | (r1(X!0, Y!12) & p4(Y!12) & ![X: $i] : (p4(X) | (~r1(Y!12, X))) & (~p3(Y!12)) & r1(Y!12, X!13) & (~p4(X!13)) & p3(X!13) & ![Y: $i] : (p3(Y) | (~r1(X!13, Y)))))),
% 0.22/0.46 inference(rewrite,[status(thm)],[])).
% 0.22/0.46 tff(101,plain,
% 0.22/0.46 ((r1(X!0, Y!14) & (~p4(Y!14)) & (p4(Y!14) & ![X: $i] : (p4(X) | (~r1(Y!14, X)))) & (~p3(Y!14)) & (p3(Y!14) & ![X: $i] : (p3(X) | (~r1(Y!14, X))))) <=> $false),
% 0.22/0.46 inference(rewrite,[status(thm)],[])).
% 0.22/0.46 tff(102,plain,
% 0.22/0.46 ((p3(Y!14) & ![X: $i] : ((~r1(Y!14, X)) | p3(X))) <=> (p3(Y!14) & ![X: $i] : (p3(X) | (~r1(Y!14, X))))),
% 0.22/0.46 inference(rewrite,[status(thm)],[])).
% 0.22/0.46 tff(103,plain,
% 0.22/0.46 ((p4(Y!14) & ![X: $i] : ((~r1(Y!14, X)) | p4(X))) <=> (p4(Y!14) & ![X: $i] : (p4(X) | (~r1(Y!14, X))))),
% 0.22/0.46 inference(rewrite,[status(thm)],[])).
% 0.22/0.46 tff(104,plain,
% 0.22/0.46 ((r1(X!0, Y!14) & (~p4(Y!14)) & (p4(Y!14) & ![X: $i] : ((~r1(Y!14, X)) | p4(X))) & (~p3(Y!14)) & (p3(Y!14) & ![X: $i] : ((~r1(Y!14, X)) | p3(X)))) <=> (r1(X!0, Y!14) & (~p4(Y!14)) & (p4(Y!14) & ![X: $i] : (p4(X) | (~r1(Y!14, X)))) & (~p3(Y!14)) & (p3(Y!14) & ![X: $i] : (p3(X) | (~r1(Y!14, X)))))),
% 0.22/0.46 inference(monotonicity,[status(thm)],[103, 102])).
% 0.22/0.46 tff(105,plain,
% 0.22/0.46 ((r1(X!0, Y!14) & (~p4(Y!14)) & (p4(Y!14) & ![X: $i] : ((~r1(Y!14, X)) | p4(X))) & (~p3(Y!14)) & (p3(Y!14) & ![X: $i] : ((~r1(Y!14, X)) | p3(X)))) <=> $false),
% 0.22/0.46 inference(transitivity,[status(thm)],[104, 101])).
% 0.22/0.46 tff(106,plain,
% 0.22/0.46 ((r1(X!0, Y!12) & (p4(Y!12) & ![X: $i] : (p4(X) | (~r1(Y!12, X)))) & (~p3(Y!12)) & (r1(Y!12, X!13) & (~p4(X!13)) & p3(X!13) & ![Y: $i] : (p3(Y) | (~r1(X!13, Y))))) <=> (r1(X!0, Y!12) & p4(Y!12) & ![X: $i] : (p4(X) | (~r1(Y!12, X))) & (~p3(Y!12)) & r1(Y!12, X!13) & (~p4(X!13)) & p3(X!13) & ![Y: $i] : (p3(Y) | (~r1(X!13, Y))))),
% 0.22/0.46 inference(rewrite,[status(thm)],[])).
% 0.22/0.46 tff(107,plain,
% 0.22/0.46 ((r1(Y!12, X!13) & (~p4(X!13)) & (p3(X!13) & ![Y: $i] : (p3(Y) | (~r1(X!13, Y))))) <=> (r1(Y!12, X!13) & (~p4(X!13)) & p3(X!13) & ![Y: $i] : (p3(Y) | (~r1(X!13, Y))))),
% 0.22/0.46 inference(rewrite,[status(thm)],[])).
% 0.22/0.46 tff(108,plain,
% 0.22/0.46 ((p3(X!13) & ![Y: $i] : ((~r1(X!13, Y)) | p3(Y))) <=> (p3(X!13) & ![Y: $i] : (p3(Y) | (~r1(X!13, Y))))),
% 0.22/0.46 inference(rewrite,[status(thm)],[])).
% 0.22/0.46 tff(109,plain,
% 0.22/0.46 ((r1(Y!12, X!13) & (~p4(X!13)) & (p3(X!13) & ![Y: $i] : ((~r1(X!13, Y)) | p3(Y)))) <=> (r1(Y!12, X!13) & (~p4(X!13)) & (p3(X!13) & ![Y: $i] : (p3(Y) | (~r1(X!13, Y)))))),
% 0.22/0.46 inference(monotonicity,[status(thm)],[108])).
% 0.22/0.46 tff(110,plain,
% 0.22/0.46 ((r1(Y!12, X!13) & (~p4(X!13)) & (p3(X!13) & ![Y: $i] : ((~r1(X!13, Y)) | p3(Y)))) <=> (r1(Y!12, X!13) & (~p4(X!13)) & p3(X!13) & ![Y: $i] : (p3(Y) | (~r1(X!13, Y))))),
% 0.22/0.46 inference(transitivity,[status(thm)],[109, 107])).
% 0.22/0.46 tff(111,plain,
% 0.22/0.46 ((p4(Y!12) & ![X: $i] : ((~r1(Y!12, X)) | p4(X))) <=> (p4(Y!12) & ![X: $i] : (p4(X) | (~r1(Y!12, X))))),
% 0.22/0.46 inference(rewrite,[status(thm)],[])).
% 0.22/0.46 tff(112,plain,
% 0.22/0.46 ((r1(X!0, Y!12) & (p4(Y!12) & ![X: $i] : ((~r1(Y!12, X)) | p4(X))) & (~p3(Y!12)) & (r1(Y!12, X!13) & (~p4(X!13)) & (p3(X!13) & ![Y: $i] : ((~r1(X!13, Y)) | p3(Y))))) <=> (r1(X!0, Y!12) & (p4(Y!12) & ![X: $i] : (p4(X) | (~r1(Y!12, X)))) & (~p3(Y!12)) & (r1(Y!12, X!13) & (~p4(X!13)) & p3(X!13) & ![Y: $i] : (p3(Y) | (~r1(X!13, Y)))))),
% 0.22/0.46 inference(monotonicity,[status(thm)],[111, 110])).
% 0.22/0.46 tff(113,plain,
% 0.22/0.46 ((r1(X!0, Y!12) & (p4(Y!12) & ![X: $i] : ((~r1(Y!12, X)) | p4(X))) & (~p3(Y!12)) & (r1(Y!12, X!13) & (~p4(X!13)) & (p3(X!13) & ![Y: $i] : ((~r1(X!13, Y)) | p3(Y))))) <=> (r1(X!0, Y!12) & p4(Y!12) & ![X: $i] : (p4(X) | (~r1(Y!12, X))) & (~p3(Y!12)) & r1(Y!12, X!13) & (~p4(X!13)) & p3(X!13) & ![Y: $i] : (p3(Y) | (~r1(X!13, Y))))),
% 0.22/0.46 inference(transitivity,[status(thm)],[112, 106])).
% 0.22/0.46 tff(114,plain,
% 0.22/0.46 ((r1(X!0, Y!10) & (~p4(Y!10)) & (r1(Y!10, X!11) & p4(X!11) & ![Y: $i] : (p4(Y) | (~r1(X!11, Y))) & (~p3(X!11))) & (p3(Y!10) & ![X: $i] : (p3(X) | (~r1(Y!10, X))))) <=> (r1(X!0, Y!10) & (~p4(Y!10)) & r1(Y!10, X!11) & p4(X!11) & ![Y: $i] : (p4(Y) | (~r1(X!11, Y))) & (~p3(X!11)) & p3(Y!10) & ![X: $i] : (p3(X) | (~r1(Y!10, X))))),
% 0.22/0.47 inference(rewrite,[status(thm)],[])).
% 0.22/0.47 tff(115,plain,
% 0.22/0.47 ((p3(Y!10) & ![X: $i] : ((~r1(Y!10, X)) | p3(X))) <=> (p3(Y!10) & ![X: $i] : (p3(X) | (~r1(Y!10, X))))),
% 0.22/0.47 inference(rewrite,[status(thm)],[])).
% 0.22/0.47 tff(116,plain,
% 0.22/0.47 ((r1(Y!10, X!11) & (p4(X!11) & ![Y: $i] : (p4(Y) | (~r1(X!11, Y)))) & (~p3(X!11))) <=> (r1(Y!10, X!11) & p4(X!11) & ![Y: $i] : (p4(Y) | (~r1(X!11, Y))) & (~p3(X!11)))),
% 0.22/0.47 inference(rewrite,[status(thm)],[])).
% 0.22/0.47 tff(117,plain,
% 0.22/0.47 ((p4(X!11) & ![Y: $i] : ((~r1(X!11, Y)) | p4(Y))) <=> (p4(X!11) & ![Y: $i] : (p4(Y) | (~r1(X!11, Y))))),
% 0.22/0.47 inference(rewrite,[status(thm)],[])).
% 0.22/0.47 tff(118,plain,
% 0.22/0.47 ((r1(Y!10, X!11) & (p4(X!11) & ![Y: $i] : ((~r1(X!11, Y)) | p4(Y))) & (~p3(X!11))) <=> (r1(Y!10, X!11) & (p4(X!11) & ![Y: $i] : (p4(Y) | (~r1(X!11, Y)))) & (~p3(X!11)))),
% 0.22/0.47 inference(monotonicity,[status(thm)],[117])).
% 0.22/0.47 tff(119,plain,
% 0.22/0.47 ((r1(Y!10, X!11) & (p4(X!11) & ![Y: $i] : ((~r1(X!11, Y)) | p4(Y))) & (~p3(X!11))) <=> (r1(Y!10, X!11) & p4(X!11) & ![Y: $i] : (p4(Y) | (~r1(X!11, Y))) & (~p3(X!11)))),
% 0.22/0.47 inference(transitivity,[status(thm)],[118, 116])).
% 0.22/0.47 tff(120,plain,
% 0.22/0.47 ((r1(X!0, Y!10) & (~p4(Y!10)) & (r1(Y!10, X!11) & (p4(X!11) & ![Y: $i] : ((~r1(X!11, Y)) | p4(Y))) & (~p3(X!11))) & (p3(Y!10) & ![X: $i] : ((~r1(Y!10, X)) | p3(X)))) <=> (r1(X!0, Y!10) & (~p4(Y!10)) & (r1(Y!10, X!11) & p4(X!11) & ![Y: $i] : (p4(Y) | (~r1(X!11, Y))) & (~p3(X!11))) & (p3(Y!10) & ![X: $i] : (p3(X) | (~r1(Y!10, X)))))),
% 0.22/0.47 inference(monotonicity,[status(thm)],[119, 115])).
% 0.22/0.47 tff(121,plain,
% 0.22/0.47 ((r1(X!0, Y!10) & (~p4(Y!10)) & (r1(Y!10, X!11) & (p4(X!11) & ![Y: $i] : ((~r1(X!11, Y)) | p4(Y))) & (~p3(X!11))) & (p3(Y!10) & ![X: $i] : ((~r1(Y!10, X)) | p3(X)))) <=> (r1(X!0, Y!10) & (~p4(Y!10)) & r1(Y!10, X!11) & p4(X!11) & ![Y: $i] : (p4(Y) | (~r1(X!11, Y))) & (~p3(X!11)) & p3(Y!10) & ![X: $i] : (p3(X) | (~r1(Y!10, X))))),
% 0.22/0.47 inference(transitivity,[status(thm)],[120, 114])).
% 0.22/0.47 tff(122,plain,
% 0.22/0.47 (((r1(X!0, Y!10) & (~p4(Y!10)) & (r1(Y!10, X!11) & (p4(X!11) & ![Y: $i] : ((~r1(X!11, Y)) | p4(Y))) & (~p3(X!11))) & (p3(Y!10) & ![X: $i] : ((~r1(Y!10, X)) | p3(X)))) | (r1(X!0, Y!12) & (p4(Y!12) & ![X: $i] : ((~r1(Y!12, X)) | p4(X))) & (~p3(Y!12)) & (r1(Y!12, X!13) & (~p4(X!13)) & (p3(X!13) & ![Y: $i] : ((~r1(X!13, Y)) | p3(Y))))) | (r1(X!0, Y!14) & (~p4(Y!14)) & (p4(Y!14) & ![X: $i] : ((~r1(Y!14, X)) | p4(X))) & (~p3(Y!14)) & (p3(Y!14) & ![X: $i] : ((~r1(Y!14, X)) | p3(X))))) <=> ((r1(X!0, Y!10) & (~p4(Y!10)) & r1(Y!10, X!11) & p4(X!11) & ![Y: $i] : (p4(Y) | (~r1(X!11, Y))) & (~p3(X!11)) & p3(Y!10) & ![X: $i] : (p3(X) | (~r1(Y!10, X)))) | (r1(X!0, Y!12) & p4(Y!12) & ![X: $i] : (p4(X) | (~r1(Y!12, X))) & (~p3(Y!12)) & r1(Y!12, X!13) & (~p4(X!13)) & p3(X!13) & ![Y: $i] : (p3(Y) | (~r1(X!13, Y)))) | $false)),
% 0.22/0.47 inference(monotonicity,[status(thm)],[121, 113, 105])).
% 0.22/0.47 tff(123,plain,
% 0.22/0.47 (((r1(X!0, Y!10) & (~p4(Y!10)) & (r1(Y!10, X!11) & (p4(X!11) & ![Y: $i] : ((~r1(X!11, Y)) | p4(Y))) & (~p3(X!11))) & (p3(Y!10) & ![X: $i] : ((~r1(Y!10, X)) | p3(X)))) | (r1(X!0, Y!12) & (p4(Y!12) & ![X: $i] : ((~r1(Y!12, X)) | p4(X))) & (~p3(Y!12)) & (r1(Y!12, X!13) & (~p4(X!13)) & (p3(X!13) & ![Y: $i] : ((~r1(X!13, Y)) | p3(Y))))) | (r1(X!0, Y!14) & (~p4(Y!14)) & (p4(Y!14) & ![X: $i] : ((~r1(Y!14, X)) | p4(X))) & (~p3(Y!14)) & (p3(Y!14) & ![X: $i] : ((~r1(Y!14, X)) | p3(X))))) <=> ((r1(X!0, Y!10) & (~p4(Y!10)) & r1(Y!10, X!11) & p4(X!11) & ![Y: $i] : (p4(Y) | (~r1(X!11, Y))) & (~p3(X!11)) & p3(Y!10) & ![X: $i] : (p3(X) | (~r1(Y!10, X)))) | (r1(X!0, Y!12) & p4(Y!12) & ![X: $i] : (p4(X) | (~r1(Y!12, X))) & (~p3(Y!12)) & r1(Y!12, X!13) & (~p4(X!13)) & p3(X!13) & ![Y: $i] : (p3(Y) | (~r1(X!13, Y)))))),
% 0.22/0.47 inference(transitivity,[status(thm)],[122, 100])).
% 0.22/0.47 tff(124,plain,
% 0.22/0.47 (^[Y: $i] : trans(monotonicity(monotonicity(rewrite((~((~r1(Y, tptp_fun_X_9(Y))) | p3(tptp_fun_X_9(Y)))) <=> (~((~r1(Y, tptp_fun_X_9(Y))) | p3(tptp_fun_X_9(Y))))), (((~p3(Y)) | (~((~r1(Y, tptp_fun_X_9(Y))) | p3(tptp_fun_X_9(Y))))) <=> ((~p3(Y)) | (~((~r1(Y, tptp_fun_X_9(Y))) | p3(tptp_fun_X_9(Y))))))), (((~r1(X!0, Y)) | p4(Y) | ((~p3(Y)) | (~((~r1(Y, tptp_fun_X_9(Y))) | p3(tptp_fun_X_9(Y)))))) <=> ((~r1(X!0, Y)) | p4(Y) | ((~p3(Y)) | (~((~r1(Y, tptp_fun_X_9(Y))) | p3(tptp_fun_X_9(Y)))))))), rewrite(((~r1(X!0, Y)) | p4(Y) | ((~p3(Y)) | (~((~r1(Y, tptp_fun_X_9(Y))) | p3(tptp_fun_X_9(Y)))))) <=> (p4(Y) | (~r1(X!0, Y)) | (~p3(Y)) | (~((~r1(Y, tptp_fun_X_9(Y))) | p3(tptp_fun_X_9(Y)))))), (((~r1(X!0, Y)) | p4(Y) | ((~p3(Y)) | (~((~r1(Y, tptp_fun_X_9(Y))) | p3(tptp_fun_X_9(Y)))))) <=> (p4(Y) | (~r1(X!0, Y)) | (~p3(Y)) | (~((~r1(Y, tptp_fun_X_9(Y))) | p3(tptp_fun_X_9(Y)))))))),
% 0.22/0.47 inference(bind,[status(th)],[])).
% 0.22/0.47 tff(125,plain,
% 0.22/0.47 (![Y: $i] : ((~r1(X!0, Y)) | p4(Y) | ((~p3(Y)) | (~((~r1(Y, tptp_fun_X_9(Y))) | p3(tptp_fun_X_9(Y)))))) <=> ![Y: $i] : (p4(Y) | (~r1(X!0, Y)) | (~p3(Y)) | (~((~r1(Y, tptp_fun_X_9(Y))) | p3(tptp_fun_X_9(Y)))))),
% 0.22/0.47 inference(quant_intro,[status(thm)],[124])).
% 0.22/0.47 tff(126,plain,
% 0.22/0.47 (^[Y: $i] : trans(monotonicity(monotonicity(rewrite((~((~r1(Y, tptp_fun_X_8(Y))) | p4(tptp_fun_X_8(Y)))) <=> (~((~r1(Y, tptp_fun_X_8(Y))) | p4(tptp_fun_X_8(Y))))), (((~p4(Y)) | (~((~r1(Y, tptp_fun_X_8(Y))) | p4(tptp_fun_X_8(Y))))) <=> ((~p4(Y)) | (~((~r1(Y, tptp_fun_X_8(Y))) | p4(tptp_fun_X_8(Y))))))), (((~r1(X!0, Y)) | ((~p4(Y)) | (~((~r1(Y, tptp_fun_X_8(Y))) | p4(tptp_fun_X_8(Y))))) | p3(Y)) <=> ((~r1(X!0, Y)) | ((~p4(Y)) | (~((~r1(Y, tptp_fun_X_8(Y))) | p4(tptp_fun_X_8(Y))))) | p3(Y)))), rewrite(((~r1(X!0, Y)) | ((~p4(Y)) | (~((~r1(Y, tptp_fun_X_8(Y))) | p4(tptp_fun_X_8(Y))))) | p3(Y)) <=> (p3(Y) | (~r1(X!0, Y)) | (~p4(Y)) | (~((~r1(Y, tptp_fun_X_8(Y))) | p4(tptp_fun_X_8(Y)))))), (((~r1(X!0, Y)) | ((~p4(Y)) | (~((~r1(Y, tptp_fun_X_8(Y))) | p4(tptp_fun_X_8(Y))))) | p3(Y)) <=> (p3(Y) | (~r1(X!0, Y)) | (~p4(Y)) | (~((~r1(Y, tptp_fun_X_8(Y))) | p4(tptp_fun_X_8(Y)))))))),
% 0.22/0.47 inference(bind,[status(th)],[])).
% 0.22/0.47 tff(127,plain,
% 0.22/0.47 (![Y: $i] : ((~r1(X!0, Y)) | ((~p4(Y)) | (~((~r1(Y, tptp_fun_X_8(Y))) | p4(tptp_fun_X_8(Y))))) | p3(Y)) <=> ![Y: $i] : (p3(Y) | (~r1(X!0, Y)) | (~p4(Y)) | (~((~r1(Y, tptp_fun_X_8(Y))) | p4(tptp_fun_X_8(Y)))))),
% 0.22/0.47 inference(quant_intro,[status(thm)],[126])).
% 0.22/0.47 tff(128,plain,
% 0.22/0.47 ((![Y: $i] : ((~r1(X!0, Y)) | ((~p4(Y)) | (~((~r1(Y, tptp_fun_X_8(Y))) | p4(tptp_fun_X_8(Y))))) | p3(Y)) | ![Y: $i] : ((~r1(X!0, Y)) | p4(Y) | ((~p3(Y)) | (~((~r1(Y, tptp_fun_X_9(Y))) | p3(tptp_fun_X_9(Y)))))) | ((r1(X!0, Y!10) & (~p4(Y!10)) & (r1(Y!10, X!11) & (p4(X!11) & ![Y: $i] : ((~r1(X!11, Y)) | p4(Y))) & (~p3(X!11))) & (p3(Y!10) & ![X: $i] : ((~r1(Y!10, X)) | p3(X)))) | (r1(X!0, Y!12) & (p4(Y!12) & ![X: $i] : ((~r1(Y!12, X)) | p4(X))) & (~p3(Y!12)) & (r1(Y!12, X!13) & (~p4(X!13)) & (p3(X!13) & ![Y: $i] : ((~r1(X!13, Y)) | p3(Y))))) | (r1(X!0, Y!14) & (~p4(Y!14)) & (p4(Y!14) & ![X: $i] : ((~r1(Y!14, X)) | p4(X))) & (~p3(Y!14)) & (p3(Y!14) & ![X: $i] : ((~r1(Y!14, X)) | p3(X)))))) <=> (![Y: $i] : (p3(Y) | (~r1(X!0, Y)) | (~p4(Y)) | (~((~r1(Y, tptp_fun_X_8(Y))) | p4(tptp_fun_X_8(Y))))) | ![Y: $i] : (p4(Y) | (~r1(X!0, Y)) | (~p3(Y)) | (~((~r1(Y, tptp_fun_X_9(Y))) | p3(tptp_fun_X_9(Y))))) | ((r1(X!0, Y!10) & (~p4(Y!10)) & r1(Y!10, X!11) & p4(X!11) & ![Y: $i] : (p4(Y) | (~r1(X!11, Y))) & (~p3(X!11)) & p3(Y!10) & ![X: $i] : (p3(X) | (~r1(Y!10, X)))) | (r1(X!0, Y!12) & p4(Y!12) & ![X: $i] : (p4(X) | (~r1(Y!12, X))) & (~p3(Y!12)) & r1(Y!12, X!13) & (~p4(X!13)) & p3(X!13) & ![Y: $i] : (p3(Y) | (~r1(X!13, Y))))))),
% 0.22/0.47 inference(monotonicity,[status(thm)],[127, 125, 123])).
% 0.22/0.47 tff(129,plain,
% 0.22/0.47 ((![Y: $i] : ((~r1(X!0, Y)) | ((~p4(Y)) | (~((~r1(Y, tptp_fun_X_8(Y))) | p4(tptp_fun_X_8(Y))))) | p3(Y)) | ![Y: $i] : ((~r1(X!0, Y)) | p4(Y) | ((~p3(Y)) | (~((~r1(Y, tptp_fun_X_9(Y))) | p3(tptp_fun_X_9(Y)))))) | ((r1(X!0, Y!10) & (~p4(Y!10)) & (r1(Y!10, X!11) & (p4(X!11) & ![Y: $i] : ((~r1(X!11, Y)) | p4(Y))) & (~p3(X!11))) & (p3(Y!10) & ![X: $i] : ((~r1(Y!10, X)) | p3(X)))) | (r1(X!0, Y!12) & (p4(Y!12) & ![X: $i] : ((~r1(Y!12, X)) | p4(X))) & (~p3(Y!12)) & (r1(Y!12, X!13) & (~p4(X!13)) & (p3(X!13) & ![Y: $i] : ((~r1(X!13, Y)) | p3(Y))))) | (r1(X!0, Y!14) & (~p4(Y!14)) & (p4(Y!14) & ![X: $i] : ((~r1(Y!14, X)) | p4(X))) & (~p3(Y!14)) & (p3(Y!14) & ![X: $i] : ((~r1(Y!14, X)) | p3(X)))))) <=> (![Y: $i] : (p3(Y) | (~r1(X!0, Y)) | (~p4(Y)) | (~((~r1(Y, tptp_fun_X_8(Y))) | p4(tptp_fun_X_8(Y))))) | ![Y: $i] : (p4(Y) | (~r1(X!0, Y)) | (~p3(Y)) | (~((~r1(Y, tptp_fun_X_9(Y))) | p3(tptp_fun_X_9(Y))))) | (r1(X!0, Y!10) & (~p4(Y!10)) & r1(Y!10, X!11) & p4(X!11) & ![Y: $i] : (p4(Y) | (~r1(X!11, Y))) & (~p3(X!11)) & p3(Y!10) & ![X: $i] : (p3(X) | (~r1(Y!10, X)))) | (r1(X!0, Y!12) & p4(Y!12) & ![X: $i] : (p4(X) | (~r1(Y!12, X))) & (~p3(Y!12)) & r1(Y!12, X!13) & (~p4(X!13)) & p3(X!13) & ![Y: $i] : (p3(Y) | (~r1(X!13, Y)))))),
% 0.22/0.47 inference(transitivity,[status(thm)],[128, 99])).
% 0.22/0.47 tff(130,plain,
% 0.22/0.47 ((![Y: $i] : (p5(Y) | (~r1(X!0, Y)) | (~(p6(tptp_fun_X_1(Y)) | (~r1(Y, tptp_fun_X_1(Y))))) | (~p6(Y))) | ![Y: $i] : (p6(Y) | (~p5(Y)) | (~r1(X!0, Y)) | (~(p5(tptp_fun_X_2(Y)) | (~r1(Y, tptp_fun_X_2(Y)))))) | (((~p6(Y!3)) & r1(X!0, Y!3) & p5(Y!3) & ![X: $i] : (p5(X) | (~r1(Y!3, X))) & (~p5(X!4)) & r1(Y!3, X!4) & p6(X!4) & ![Y: $i] : (p6(Y) | (~r1(X!4, Y)))) | ((~p5(Y!5)) & r1(X!0, Y!5) & p6(Y!5) & ![X: $i] : (p6(X) | (~r1(Y!5, X))) & (~p6(X!6)) & r1(Y!5, X!6) & p5(X!6) & ![Y: $i] : (p5(Y) | (~r1(X!6, Y)))))) <=> (![Y: $i] : (p5(Y) | (~r1(X!0, Y)) | (~(p6(tptp_fun_X_1(Y)) | (~r1(Y, tptp_fun_X_1(Y))))) | (~p6(Y))) | ![Y: $i] : (p6(Y) | (~p5(Y)) | (~r1(X!0, Y)) | (~(p5(tptp_fun_X_2(Y)) | (~r1(Y, tptp_fun_X_2(Y)))))) | ((~p6(Y!3)) & r1(X!0, Y!3) & p5(Y!3) & ![X: $i] : (p5(X) | (~r1(Y!3, X))) & (~p5(X!4)) & r1(Y!3, X!4) & p6(X!4) & ![Y: $i] : (p6(Y) | (~r1(X!4, Y)))) | ((~p5(Y!5)) & r1(X!0, Y!5) & p6(Y!5) & ![X: $i] : (p6(X) | (~r1(Y!5, X))) & (~p6(X!6)) & r1(Y!5, X!6) & p5(X!6) & ![Y: $i] : (p5(Y) | (~r1(X!6, Y)))))),
% 0.22/0.47 inference(rewrite,[status(thm)],[])).
% 0.22/0.47 tff(131,plain,
% 0.22/0.47 ((((~p6(Y!3)) & r1(X!0, Y!3) & p5(Y!3) & ![X: $i] : (p5(X) | (~r1(Y!3, X))) & (~p5(X!4)) & r1(Y!3, X!4) & p6(X!4) & ![Y: $i] : (p6(Y) | (~r1(X!4, Y)))) | ((~p5(Y!5)) & r1(X!0, Y!5) & p6(Y!5) & ![X: $i] : (p6(X) | (~r1(Y!5, X))) & (~p6(X!6)) & r1(Y!5, X!6) & p5(X!6) & ![Y: $i] : (p5(Y) | (~r1(X!6, Y)))) | $false) <=> (((~p6(Y!3)) & r1(X!0, Y!3) & p5(Y!3) & ![X: $i] : (p5(X) | (~r1(Y!3, X))) & (~p5(X!4)) & r1(Y!3, X!4) & p6(X!4) & ![Y: $i] : (p6(Y) | (~r1(X!4, Y)))) | ((~p5(Y!5)) & r1(X!0, Y!5) & p6(Y!5) & ![X: $i] : (p6(X) | (~r1(Y!5, X))) & (~p6(X!6)) & r1(Y!5, X!6) & p5(X!6) & ![Y: $i] : (p5(Y) | (~r1(X!6, Y)))))),
% 0.22/0.47 inference(rewrite,[status(thm)],[])).
% 0.22/0.47 tff(132,plain,
% 0.22/0.47 (((~p6(Y!7)) & (~p5(Y!7)) & r1(X!0, Y!7) & (p6(Y!7) & ![X: $i] : (p6(X) | (~r1(Y!7, X)))) & (p5(Y!7) & ![X: $i] : (p5(X) | (~r1(Y!7, X))))) <=> $false),
% 0.22/0.47 inference(rewrite,[status(thm)],[])).
% 0.22/0.47 tff(133,plain,
% 0.22/0.47 ((p5(Y!7) & ![X: $i] : (p5(X) | (~r1(Y!7, X)))) <=> (p5(Y!7) & ![X: $i] : (p5(X) | (~r1(Y!7, X))))),
% 0.22/0.47 inference(rewrite,[status(thm)],[])).
% 0.22/0.47 tff(134,plain,
% 0.22/0.47 ((p6(Y!7) & ![X: $i] : (p6(X) | (~r1(Y!7, X)))) <=> (p6(Y!7) & ![X: $i] : (p6(X) | (~r1(Y!7, X))))),
% 0.22/0.47 inference(rewrite,[status(thm)],[])).
% 0.22/0.48 tff(135,plain,
% 0.22/0.48 (((~p6(Y!7)) & (~p5(Y!7)) & r1(X!0, Y!7) & (p6(Y!7) & ![X: $i] : (p6(X) | (~r1(Y!7, X)))) & (p5(Y!7) & ![X: $i] : (p5(X) | (~r1(Y!7, X))))) <=> ((~p6(Y!7)) & (~p5(Y!7)) & r1(X!0, Y!7) & (p6(Y!7) & ![X: $i] : (p6(X) | (~r1(Y!7, X)))) & (p5(Y!7) & ![X: $i] : (p5(X) | (~r1(Y!7, X)))))),
% 0.22/0.48 inference(monotonicity,[status(thm)],[134, 133])).
% 0.22/0.48 tff(136,plain,
% 0.22/0.48 (((~p6(Y!7)) & (~p5(Y!7)) & r1(X!0, Y!7) & (p6(Y!7) & ![X: $i] : (p6(X) | (~r1(Y!7, X)))) & (p5(Y!7) & ![X: $i] : (p5(X) | (~r1(Y!7, X))))) <=> $false),
% 0.22/0.48 inference(transitivity,[status(thm)],[135, 132])).
% 0.22/0.48 tff(137,plain,
% 0.22/0.48 (((~p5(Y!5)) & r1(X!0, Y!5) & (p6(Y!5) & ![X: $i] : (p6(X) | (~r1(Y!5, X)))) & ((~p6(X!6)) & r1(Y!5, X!6) & p5(X!6) & ![Y: $i] : (p5(Y) | (~r1(X!6, Y))))) <=> ((~p5(Y!5)) & r1(X!0, Y!5) & p6(Y!5) & ![X: $i] : (p6(X) | (~r1(Y!5, X))) & (~p6(X!6)) & r1(Y!5, X!6) & p5(X!6) & ![Y: $i] : (p5(Y) | (~r1(X!6, Y))))),
% 0.22/0.48 inference(rewrite,[status(thm)],[])).
% 0.22/0.48 tff(138,plain,
% 0.22/0.48 (((~p6(X!6)) & r1(Y!5, X!6) & (p5(X!6) & ![Y: $i] : (p5(Y) | (~r1(X!6, Y))))) <=> ((~p6(X!6)) & r1(Y!5, X!6) & p5(X!6) & ![Y: $i] : (p5(Y) | (~r1(X!6, Y))))),
% 0.22/0.48 inference(rewrite,[status(thm)],[])).
% 0.22/0.48 tff(139,plain,
% 0.22/0.48 ((p5(X!6) & ![Y: $i] : (p5(Y) | (~r1(X!6, Y)))) <=> (p5(X!6) & ![Y: $i] : (p5(Y) | (~r1(X!6, Y))))),
% 0.22/0.48 inference(rewrite,[status(thm)],[])).
% 0.22/0.48 tff(140,plain,
% 0.22/0.48 (((~p6(X!6)) & r1(Y!5, X!6) & (p5(X!6) & ![Y: $i] : (p5(Y) | (~r1(X!6, Y))))) <=> ((~p6(X!6)) & r1(Y!5, X!6) & (p5(X!6) & ![Y: $i] : (p5(Y) | (~r1(X!6, Y)))))),
% 0.22/0.48 inference(monotonicity,[status(thm)],[139])).
% 0.22/0.48 tff(141,plain,
% 0.22/0.48 (((~p6(X!6)) & r1(Y!5, X!6) & (p5(X!6) & ![Y: $i] : (p5(Y) | (~r1(X!6, Y))))) <=> ((~p6(X!6)) & r1(Y!5, X!6) & p5(X!6) & ![Y: $i] : (p5(Y) | (~r1(X!6, Y))))),
% 0.22/0.48 inference(transitivity,[status(thm)],[140, 138])).
% 0.22/0.48 tff(142,plain,
% 0.22/0.48 ((p6(Y!5) & ![X: $i] : (p6(X) | (~r1(Y!5, X)))) <=> (p6(Y!5) & ![X: $i] : (p6(X) | (~r1(Y!5, X))))),
% 0.22/0.48 inference(rewrite,[status(thm)],[])).
% 0.22/0.48 tff(143,plain,
% 0.22/0.48 (((~p5(Y!5)) & r1(X!0, Y!5) & (p6(Y!5) & ![X: $i] : (p6(X) | (~r1(Y!5, X)))) & ((~p6(X!6)) & r1(Y!5, X!6) & (p5(X!6) & ![Y: $i] : (p5(Y) | (~r1(X!6, Y)))))) <=> ((~p5(Y!5)) & r1(X!0, Y!5) & (p6(Y!5) & ![X: $i] : (p6(X) | (~r1(Y!5, X)))) & ((~p6(X!6)) & r1(Y!5, X!6) & p5(X!6) & ![Y: $i] : (p5(Y) | (~r1(X!6, Y)))))),
% 0.22/0.48 inference(monotonicity,[status(thm)],[142, 141])).
% 0.22/0.48 tff(144,plain,
% 0.22/0.48 (((~p5(Y!5)) & r1(X!0, Y!5) & (p6(Y!5) & ![X: $i] : (p6(X) | (~r1(Y!5, X)))) & ((~p6(X!6)) & r1(Y!5, X!6) & (p5(X!6) & ![Y: $i] : (p5(Y) | (~r1(X!6, Y)))))) <=> ((~p5(Y!5)) & r1(X!0, Y!5) & p6(Y!5) & ![X: $i] : (p6(X) | (~r1(Y!5, X))) & (~p6(X!6)) & r1(Y!5, X!6) & p5(X!6) & ![Y: $i] : (p5(Y) | (~r1(X!6, Y))))),
% 0.22/0.48 inference(transitivity,[status(thm)],[143, 137])).
% 0.22/0.48 tff(145,plain,
% 0.22/0.48 (((~p6(Y!3)) & r1(X!0, Y!3) & (p5(Y!3) & ![X: $i] : (p5(X) | (~r1(Y!3, X)))) & ((~p5(X!4)) & r1(Y!3, X!4) & p6(X!4) & ![Y: $i] : (p6(Y) | (~r1(X!4, Y))))) <=> ((~p6(Y!3)) & r1(X!0, Y!3) & p5(Y!3) & ![X: $i] : (p5(X) | (~r1(Y!3, X))) & (~p5(X!4)) & r1(Y!3, X!4) & p6(X!4) & ![Y: $i] : (p6(Y) | (~r1(X!4, Y))))),
% 0.22/0.48 inference(rewrite,[status(thm)],[])).
% 0.22/0.48 tff(146,plain,
% 0.22/0.48 (((~p5(X!4)) & r1(Y!3, X!4) & (p6(X!4) & ![Y: $i] : (p6(Y) | (~r1(X!4, Y))))) <=> ((~p5(X!4)) & r1(Y!3, X!4) & p6(X!4) & ![Y: $i] : (p6(Y) | (~r1(X!4, Y))))),
% 0.22/0.48 inference(rewrite,[status(thm)],[])).
% 0.22/0.48 tff(147,plain,
% 0.22/0.48 ((p6(X!4) & ![Y: $i] : (p6(Y) | (~r1(X!4, Y)))) <=> (p6(X!4) & ![Y: $i] : (p6(Y) | (~r1(X!4, Y))))),
% 0.22/0.48 inference(rewrite,[status(thm)],[])).
% 0.22/0.48 tff(148,plain,
% 0.22/0.48 (((~p5(X!4)) & r1(Y!3, X!4) & (p6(X!4) & ![Y: $i] : (p6(Y) | (~r1(X!4, Y))))) <=> ((~p5(X!4)) & r1(Y!3, X!4) & (p6(X!4) & ![Y: $i] : (p6(Y) | (~r1(X!4, Y)))))),
% 0.22/0.48 inference(monotonicity,[status(thm)],[147])).
% 0.22/0.48 tff(149,plain,
% 0.22/0.48 (((~p5(X!4)) & r1(Y!3, X!4) & (p6(X!4) & ![Y: $i] : (p6(Y) | (~r1(X!4, Y))))) <=> ((~p5(X!4)) & r1(Y!3, X!4) & p6(X!4) & ![Y: $i] : (p6(Y) | (~r1(X!4, Y))))),
% 0.22/0.48 inference(transitivity,[status(thm)],[148, 146])).
% 0.22/0.48 tff(150,plain,
% 0.22/0.48 ((p5(Y!3) & ![X: $i] : (p5(X) | (~r1(Y!3, X)))) <=> (p5(Y!3) & ![X: $i] : (p5(X) | (~r1(Y!3, X))))),
% 0.22/0.48 inference(rewrite,[status(thm)],[])).
% 0.22/0.48 tff(151,plain,
% 0.22/0.48 (((~p6(Y!3)) & r1(X!0, Y!3) & (p5(Y!3) & ![X: $i] : (p5(X) | (~r1(Y!3, X)))) & ((~p5(X!4)) & r1(Y!3, X!4) & (p6(X!4) & ![Y: $i] : (p6(Y) | (~r1(X!4, Y)))))) <=> ((~p6(Y!3)) & r1(X!0, Y!3) & (p5(Y!3) & ![X: $i] : (p5(X) | (~r1(Y!3, X)))) & ((~p5(X!4)) & r1(Y!3, X!4) & p6(X!4) & ![Y: $i] : (p6(Y) | (~r1(X!4, Y)))))),
% 0.22/0.48 inference(monotonicity,[status(thm)],[150, 149])).
% 0.22/0.48 tff(152,plain,
% 0.22/0.48 (((~p6(Y!3)) & r1(X!0, Y!3) & (p5(Y!3) & ![X: $i] : (p5(X) | (~r1(Y!3, X)))) & ((~p5(X!4)) & r1(Y!3, X!4) & (p6(X!4) & ![Y: $i] : (p6(Y) | (~r1(X!4, Y)))))) <=> ((~p6(Y!3)) & r1(X!0, Y!3) & p5(Y!3) & ![X: $i] : (p5(X) | (~r1(Y!3, X))) & (~p5(X!4)) & r1(Y!3, X!4) & p6(X!4) & ![Y: $i] : (p6(Y) | (~r1(X!4, Y))))),
% 0.22/0.48 inference(transitivity,[status(thm)],[151, 145])).
% 0.22/0.48 tff(153,plain,
% 0.22/0.48 ((((~p6(Y!3)) & r1(X!0, Y!3) & (p5(Y!3) & ![X: $i] : (p5(X) | (~r1(Y!3, X)))) & ((~p5(X!4)) & r1(Y!3, X!4) & (p6(X!4) & ![Y: $i] : (p6(Y) | (~r1(X!4, Y)))))) | ((~p5(Y!5)) & r1(X!0, Y!5) & (p6(Y!5) & ![X: $i] : (p6(X) | (~r1(Y!5, X)))) & ((~p6(X!6)) & r1(Y!5, X!6) & (p5(X!6) & ![Y: $i] : (p5(Y) | (~r1(X!6, Y)))))) | ((~p6(Y!7)) & (~p5(Y!7)) & r1(X!0, Y!7) & (p6(Y!7) & ![X: $i] : (p6(X) | (~r1(Y!7, X)))) & (p5(Y!7) & ![X: $i] : (p5(X) | (~r1(Y!7, X)))))) <=> (((~p6(Y!3)) & r1(X!0, Y!3) & p5(Y!3) & ![X: $i] : (p5(X) | (~r1(Y!3, X))) & (~p5(X!4)) & r1(Y!3, X!4) & p6(X!4) & ![Y: $i] : (p6(Y) | (~r1(X!4, Y)))) | ((~p5(Y!5)) & r1(X!0, Y!5) & p6(Y!5) & ![X: $i] : (p6(X) | (~r1(Y!5, X))) & (~p6(X!6)) & r1(Y!5, X!6) & p5(X!6) & ![Y: $i] : (p5(Y) | (~r1(X!6, Y)))) | $false)),
% 0.22/0.48 inference(monotonicity,[status(thm)],[152, 144, 136])).
% 0.22/0.48 tff(154,plain,
% 0.22/0.48 ((((~p6(Y!3)) & r1(X!0, Y!3) & (p5(Y!3) & ![X: $i] : (p5(X) | (~r1(Y!3, X)))) & ((~p5(X!4)) & r1(Y!3, X!4) & (p6(X!4) & ![Y: $i] : (p6(Y) | (~r1(X!4, Y)))))) | ((~p5(Y!5)) & r1(X!0, Y!5) & (p6(Y!5) & ![X: $i] : (p6(X) | (~r1(Y!5, X)))) & ((~p6(X!6)) & r1(Y!5, X!6) & (p5(X!6) & ![Y: $i] : (p5(Y) | (~r1(X!6, Y)))))) | ((~p6(Y!7)) & (~p5(Y!7)) & r1(X!0, Y!7) & (p6(Y!7) & ![X: $i] : (p6(X) | (~r1(Y!7, X)))) & (p5(Y!7) & ![X: $i] : (p5(X) | (~r1(Y!7, X)))))) <=> (((~p6(Y!3)) & r1(X!0, Y!3) & p5(Y!3) & ![X: $i] : (p5(X) | (~r1(Y!3, X))) & (~p5(X!4)) & r1(Y!3, X!4) & p6(X!4) & ![Y: $i] : (p6(Y) | (~r1(X!4, Y)))) | ((~p5(Y!5)) & r1(X!0, Y!5) & p6(Y!5) & ![X: $i] : (p6(X) | (~r1(Y!5, X))) & (~p6(X!6)) & r1(Y!5, X!6) & p5(X!6) & ![Y: $i] : (p5(Y) | (~r1(X!6, Y)))))),
% 0.22/0.48 inference(transitivity,[status(thm)],[153, 131])).
% 0.22/0.48 tff(155,plain,
% 0.22/0.48 (^[Y: $i] : rewrite((p6(Y) | (~r1(X!0, Y)) | ((~p5(Y)) | (~(p5(tptp_fun_X_2(Y)) | (~r1(Y, tptp_fun_X_2(Y))))))) <=> (p6(Y) | (~p5(Y)) | (~r1(X!0, Y)) | (~(p5(tptp_fun_X_2(Y)) | (~r1(Y, tptp_fun_X_2(Y)))))))),
% 0.22/0.48 inference(bind,[status(th)],[])).
% 0.22/0.48 tff(156,plain,
% 0.22/0.48 (![Y: $i] : (p6(Y) | (~r1(X!0, Y)) | ((~p5(Y)) | (~(p5(tptp_fun_X_2(Y)) | (~r1(Y, tptp_fun_X_2(Y))))))) <=> ![Y: $i] : (p6(Y) | (~p5(Y)) | (~r1(X!0, Y)) | (~(p5(tptp_fun_X_2(Y)) | (~r1(Y, tptp_fun_X_2(Y))))))),
% 0.22/0.48 inference(quant_intro,[status(thm)],[155])).
% 0.22/0.48 tff(157,plain,
% 0.22/0.48 (^[Y: $i] : rewrite((p5(Y) | (~r1(X!0, Y)) | ((~p6(Y)) | (~(p6(tptp_fun_X_1(Y)) | (~r1(Y, tptp_fun_X_1(Y))))))) <=> (p5(Y) | (~r1(X!0, Y)) | (~(p6(tptp_fun_X_1(Y)) | (~r1(Y, tptp_fun_X_1(Y))))) | (~p6(Y))))),
% 0.22/0.48 inference(bind,[status(th)],[])).
% 0.22/0.48 tff(158,plain,
% 0.22/0.48 (![Y: $i] : (p5(Y) | (~r1(X!0, Y)) | ((~p6(Y)) | (~(p6(tptp_fun_X_1(Y)) | (~r1(Y, tptp_fun_X_1(Y))))))) <=> ![Y: $i] : (p5(Y) | (~r1(X!0, Y)) | (~(p6(tptp_fun_X_1(Y)) | (~r1(Y, tptp_fun_X_1(Y))))) | (~p6(Y)))),
% 0.22/0.48 inference(quant_intro,[status(thm)],[157])).
% 0.22/0.48 tff(159,plain,
% 0.22/0.48 ((![Y: $i] : (p5(Y) | (~r1(X!0, Y)) | ((~p6(Y)) | (~(p6(tptp_fun_X_1(Y)) | (~r1(Y, tptp_fun_X_1(Y))))))) | ![Y: $i] : (p6(Y) | (~r1(X!0, Y)) | ((~p5(Y)) | (~(p5(tptp_fun_X_2(Y)) | (~r1(Y, tptp_fun_X_2(Y))))))) | (((~p6(Y!3)) & r1(X!0, Y!3) & (p5(Y!3) & ![X: $i] : (p5(X) | (~r1(Y!3, X)))) & ((~p5(X!4)) & r1(Y!3, X!4) & (p6(X!4) & ![Y: $i] : (p6(Y) | (~r1(X!4, Y)))))) | ((~p5(Y!5)) & r1(X!0, Y!5) & (p6(Y!5) & ![X: $i] : (p6(X) | (~r1(Y!5, X)))) & ((~p6(X!6)) & r1(Y!5, X!6) & (p5(X!6) & ![Y: $i] : (p5(Y) | (~r1(X!6, Y)))))) | ((~p6(Y!7)) & (~p5(Y!7)) & r1(X!0, Y!7) & (p6(Y!7) & ![X: $i] : (p6(X) | (~r1(Y!7, X)))) & (p5(Y!7) & ![X: $i] : (p5(X) | (~r1(Y!7, X))))))) <=> (![Y: $i] : (p5(Y) | (~r1(X!0, Y)) | (~(p6(tptp_fun_X_1(Y)) | (~r1(Y, tptp_fun_X_1(Y))))) | (~p6(Y))) | ![Y: $i] : (p6(Y) | (~p5(Y)) | (~r1(X!0, Y)) | (~(p5(tptp_fun_X_2(Y)) | (~r1(Y, tptp_fun_X_2(Y)))))) | (((~p6(Y!3)) & r1(X!0, Y!3) & p5(Y!3) & ![X: $i] : (p5(X) | (~r1(Y!3, X))) & (~p5(X!4)) & r1(Y!3, X!4) & p6(X!4) & ![Y: $i] : (p6(Y) | (~r1(X!4, Y)))) | ((~p5(Y!5)) & r1(X!0, Y!5) & p6(Y!5) & ![X: $i] : (p6(X) | (~r1(Y!5, X))) & (~p6(X!6)) & r1(Y!5, X!6) & p5(X!6) & ![Y: $i] : (p5(Y) | (~r1(X!6, Y))))))),
% 0.22/0.48 inference(monotonicity,[status(thm)],[158, 156, 154])).
% 0.22/0.48 tff(160,plain,
% 0.22/0.48 ((![Y: $i] : (p5(Y) | (~r1(X!0, Y)) | ((~p6(Y)) | (~(p6(tptp_fun_X_1(Y)) | (~r1(Y, tptp_fun_X_1(Y))))))) | ![Y: $i] : (p6(Y) | (~r1(X!0, Y)) | ((~p5(Y)) | (~(p5(tptp_fun_X_2(Y)) | (~r1(Y, tptp_fun_X_2(Y))))))) | (((~p6(Y!3)) & r1(X!0, Y!3) & (p5(Y!3) & ![X: $i] : (p5(X) | (~r1(Y!3, X)))) & ((~p5(X!4)) & r1(Y!3, X!4) & (p6(X!4) & ![Y: $i] : (p6(Y) | (~r1(X!4, Y)))))) | ((~p5(Y!5)) & r1(X!0, Y!5) & (p6(Y!5) & ![X: $i] : (p6(X) | (~r1(Y!5, X)))) & ((~p6(X!6)) & r1(Y!5, X!6) & (p5(X!6) & ![Y: $i] : (p5(Y) | (~r1(X!6, Y)))))) | ((~p6(Y!7)) & (~p5(Y!7)) & r1(X!0, Y!7) & (p6(Y!7) & ![X: $i] : (p6(X) | (~r1(Y!7, X)))) & (p5(Y!7) & ![X: $i] : (p5(X) | (~r1(Y!7, X))))))) <=> (![Y: $i] : (p5(Y) | (~r1(X!0, Y)) | (~(p6(tptp_fun_X_1(Y)) | (~r1(Y, tptp_fun_X_1(Y))))) | (~p6(Y))) | ![Y: $i] : (p6(Y) | (~p5(Y)) | (~r1(X!0, Y)) | (~(p5(tptp_fun_X_2(Y)) | (~r1(Y, tptp_fun_X_2(Y)))))) | ((~p6(Y!3)) & r1(X!0, Y!3) & p5(Y!3) & ![X: $i] : (p5(X) | (~r1(Y!3, X))) & (~p5(X!4)) & r1(Y!3, X!4) & p6(X!4) & ![Y: $i] : (p6(Y) | (~r1(X!4, Y)))) | ((~p5(Y!5)) & r1(X!0, Y!5) & p6(Y!5) & ![X: $i] : (p6(X) | (~r1(Y!5, X))) & (~p6(X!6)) & r1(Y!5, X!6) & p5(X!6) & ![Y: $i] : (p5(Y) | (~r1(X!6, Y)))))),
% 0.22/0.49 inference(transitivity,[status(thm)],[159, 130])).
% 0.22/0.49 tff(161,plain,
% 0.22/0.49 (((![Y: $i] : (p5(Y) | (~r1(X!0, Y)) | ((~p6(Y)) | (~(p6(tptp_fun_X_1(Y)) | (~r1(Y, tptp_fun_X_1(Y))))))) | ![Y: $i] : (p6(Y) | (~r1(X!0, Y)) | ((~p5(Y)) | (~(p5(tptp_fun_X_2(Y)) | (~r1(Y, tptp_fun_X_2(Y))))))) | (((~p6(Y!3)) & r1(X!0, Y!3) & (p5(Y!3) & ![X: $i] : (p5(X) | (~r1(Y!3, X)))) & ((~p5(X!4)) & r1(Y!3, X!4) & (p6(X!4) & ![Y: $i] : (p6(Y) | (~r1(X!4, Y)))))) | ((~p5(Y!5)) & r1(X!0, Y!5) & (p6(Y!5) & ![X: $i] : (p6(X) | (~r1(Y!5, X)))) & ((~p6(X!6)) & r1(Y!5, X!6) & (p5(X!6) & ![Y: $i] : (p5(Y) | (~r1(X!6, Y)))))) | ((~p6(Y!7)) & (~p5(Y!7)) & r1(X!0, Y!7) & (p6(Y!7) & ![X: $i] : (p6(X) | (~r1(Y!7, X)))) & (p5(Y!7) & ![X: $i] : (p5(X) | (~r1(Y!7, X))))))) & (![Y: $i] : ((~r1(X!0, Y)) | ((~p4(Y)) | (~((~r1(Y, tptp_fun_X_8(Y))) | p4(tptp_fun_X_8(Y))))) | p3(Y)) | ![Y: $i] : ((~r1(X!0, Y)) | p4(Y) | ((~p3(Y)) | (~((~r1(Y, tptp_fun_X_9(Y))) | p3(tptp_fun_X_9(Y)))))) | ((r1(X!0, Y!10) & (~p4(Y!10)) & (r1(Y!10, X!11) & (p4(X!11) & ![Y: $i] : ((~r1(X!11, Y)) | p4(Y))) & (~p3(X!11))) & (p3(Y!10) & ![X: $i] : ((~r1(Y!10, X)) | p3(X)))) | (r1(X!0, Y!12) & (p4(Y!12) & ![X: $i] : ((~r1(Y!12, X)) | p4(X))) & (~p3(Y!12)) & (r1(Y!12, X!13) & (~p4(X!13)) & (p3(X!13) & ![Y: $i] : ((~r1(X!13, Y)) | p3(Y))))) | (r1(X!0, Y!14) & (~p4(Y!14)) & (p4(Y!14) & ![X: $i] : ((~r1(Y!14, X)) | p4(X))) & (~p3(Y!14)) & (p3(Y!14) & ![X: $i] : ((~r1(Y!14, X)) | p3(X)))))) & (![Y: $i] : ((~r1(X!0, Y)) | p4(Y) | ((~p5(Y)) | (~(p5(tptp_fun_X_2(Y)) | (~r1(Y, tptp_fun_X_2(Y))))))) | (((~p5(Y!15)) & r1(X!0, Y!15) & (p4(Y!15) & ![X: $i] : ((~r1(Y!15, X)) | p4(X))) & (r1(Y!15, X!16) & (~p4(X!16)) & (p5(X!16) & ![Y: $i] : (p5(Y) | (~r1(X!16, Y)))))) | (r1(X!0, Y!17) & (~p4(Y!17)) & (p5(Y!17) & ![X: $i] : (p5(X) | (~r1(Y!17, X)))) & ((~p5(X!18)) & r1(Y!17, X!18) & (p4(X!18) & ![Y: $i] : ((~r1(X!18, Y)) | p4(Y))))) | ((~p5(Y!19)) & r1(X!0, Y!19) & (~p4(Y!19)) & (p4(Y!19) & ![X: $i] : ((~r1(Y!19, X)) | p4(X))) & (p5(Y!19) & ![X: $i] : (p5(X) | (~r1(Y!19, X)))))) | ![Y: $i] : (p5(Y) | (~r1(X!0, Y)) | ((~p4(Y)) | (~((~r1(Y, tptp_fun_X_8(Y))) | p4(tptp_fun_X_8(Y))))))) & ((~p5(Y!20)) & r1(X!0, Y!20) & (![X: $i] : (p5(X) | (~r1(Y!20, X))) & p5(Y!20))) & (![Y: $i] : ((~r1(X!0, Y)) | ((~p3(Y)) | (~((~r1(Y, tptp_fun_X_9(Y))) | p3(tptp_fun_X_9(Y))))) | p2(Y)) | ((r1(X!0, Y!21) & (~p3(Y!21)) & (p2(Y!21) & ![X: $i] : ((~r1(Y!21, X)) | p2(X))) & (r1(Y!21, X!22) & (p3(X!22) & ![Y: $i] : ((~r1(X!22, Y)) | p3(Y))) & (~p2(X!22)))) | (r1(X!0, Y!23) & (p3(Y!23) & ![X: $i] : ((~r1(Y!23, X)) | p3(X))) & (~p2(Y!23)) & (r1(Y!23, X!24) & (~p3(X!24)) & (p2(X!24) & ![Y: $i] : ((~r1(X!24, Y)) | p2(Y))))) | (r1(X!0, Y!25) & (~p3(Y!25)) & (p3(Y!25) & ![X: $i] : ((~r1(Y!25, X)) | p3(X))) & (~p2(Y!25)) & (p2(Y!25) & ![X: $i] : ((~r1(Y!25, X)) | p2(X))))) | ![Y: $i] : ((~r1(X!0, Y)) | p3(Y) | ((~p2(Y)) | (~((~r1(Y, tptp_fun_X_26(Y))) | p2(tptp_fun_X_26(Y))))))) & (![Y: $i] : ((~r1(X!0, Y)) | p2(Y) | ((~p1(Y)) | (~((~r1(Y, tptp_fun_X_27(Y))) | p1(tptp_fun_X_27(Y)))))) | ((r1(X!0, Y!28) & (r1(Y!28, X!29) & (p2(X!29) & ![Y: $i] : ((~r1(X!29, Y)) | p2(Y))) & (~p1(X!29))) & (~p2(Y!28)) & (p1(Y!28) & ![X: $i] : ((~r1(Y!28, X)) | p1(X)))) | (r1(X!0, Y!30) & (~p1(Y!30)) & (p2(Y!30) & ![X: $i] : ((~r1(Y!30, X)) | p2(X))) & (r1(Y!30, X!31) & (~p2(X!31)) & (p1(X!31) & ![Y: $i] : ((~r1(X!31, Y)) | p1(Y))))) | (r1(X!0, Y!32) & (~p2(Y!32)) & (~p1(Y!32)) & (p2(Y!32) & ![X: $i] : ((~r1(Y!32, X)) | p2(X))) & (p1(Y!32) & ![X: $i] : ((~r1(Y!32, X)) | p1(X))))) | ![Y: $i] : ((~r1(X!0, Y)) | p1(Y) | ((~p2(Y)) | (~((~r1(Y, tptp_fun_X_26(Y))) | p2(tptp_fun_X_26(Y)))))))) <=> ((![Y: $i] : (p5(Y) | (~r1(X!0, Y)) | (~(p6(tptp_fun_X_1(Y)) | (~r1(Y, tptp_fun_X_1(Y))))) | (~p6(Y))) | ![Y: $i] : (p6(Y) | (~p5(Y)) | (~r1(X!0, Y)) | (~(p5(tptp_fun_X_2(Y)) | (~r1(Y, tptp_fun_X_2(Y)))))) | ((~p6(Y!3)) & r1(X!0, Y!3) & p5(Y!3) & ![X: $i] : (p5(X) | (~r1(Y!3, X))) & (~p5(X!4)) & r1(Y!3, X!4) & p6(X!4) & ![Y: $i] : (p6(Y) | (~r1(X!4, Y)))) | ((~p5(Y!5)) & r1(X!0, Y!5) & p6(Y!5) & ![X: $i] : (p6(X) | (~r1(Y!5, X))) & (~p6(X!6)) & r1(Y!5, X!6) & p5(X!6) & ![Y: $i] : (p5(Y) | (~r1(X!6, Y))))) & (![Y: $i] : (p3(Y) | (~r1(X!0, Y)) | (~p4(Y)) | (~((~r1(Y, tptp_fun_X_8(Y))) | p4(tptp_fun_X_8(Y))))) | ![Y: $i] : (p4(Y) | (~r1(X!0, Y)) | (~p3(Y)) | (~((~r1(Y, tptp_fun_X_9(Y))) | p3(tptp_fun_X_9(Y))))) | (r1(X!0, Y!10) & (~p4(Y!10)) & r1(Y!10, X!11) & p4(X!11) & ![Y: $i] : (p4(Y) | (~r1(X!11, Y))) & (~p3(X!11)) & p3(Y!10) & ![X: $i] : (p3(X) | (~r1(Y!10, X)))) | (r1(X!0, Y!12) & p4(Y!12) & ![X: $i] : (p4(X) | (~r1(Y!12, X))) & (~p3(Y!12)) & r1(Y!12, X!13) & (~p4(X!13)) & p3(X!13) & ![Y: $i] : (p3(Y) | (~r1(X!13, Y))))) & (![Y: $i] : (p4(Y) | (~p5(Y)) | (~r1(X!0, Y)) | (~(p5(tptp_fun_X_2(Y)) | (~r1(Y, tptp_fun_X_2(Y)))))) | ((~p5(Y!15)) & r1(X!0, Y!15) & p4(Y!15) & ![X: $i] : (p4(X) | (~r1(Y!15, X))) & r1(Y!15, X!16) & (~p4(X!16)) & p5(X!16) & ![Y: $i] : (p5(Y) | (~r1(X!16, Y)))) | (r1(X!0, Y!17) & (~p4(Y!17)) & p5(Y!17) & ![X: $i] : (p5(X) | (~r1(Y!17, X))) & (~p5(X!18)) & r1(Y!17, X!18) & p4(X!18) & ![Y: $i] : (p4(Y) | (~r1(X!18, Y)))) | ![Y: $i] : (p5(Y) | (~r1(X!0, Y)) | (~p4(Y)) | (~((~r1(Y, tptp_fun_X_8(Y))) | p4(tptp_fun_X_8(Y)))))) & $false & (![Y: $i] : (p2(Y) | (~r1(X!0, Y)) | (~p3(Y)) | (~((~r1(Y, tptp_fun_X_9(Y))) | p3(tptp_fun_X_9(Y))))) | (r1(X!0, Y!21) & (~p3(Y!21)) & p2(Y!21) & ![X: $i] : (p2(X) | (~r1(Y!21, X))) & r1(Y!21, X!22) & p3(X!22) & ![Y: $i] : (p3(Y) | (~r1(X!22, Y))) & (~p2(X!22))) | (r1(X!0, Y!23) & p3(Y!23) & ![X: $i] : (p3(X) | (~r1(Y!23, X))) & (~p2(Y!23)) & r1(Y!23, X!24) & (~p3(X!24)) & p2(X!24) & ![Y: $i] : (p2(Y) | (~r1(X!24, Y)))) | ![Y: $i] : (p3(Y) | (~r1(X!0, Y)) | (~p2(Y)) | (~((~r1(Y, tptp_fun_X_26(Y))) | p2(tptp_fun_X_26(Y)))))) & (![Y: $i] : (p2(Y) | (~r1(X!0, Y)) | (~p1(Y)) | (~((~r1(Y, tptp_fun_X_27(Y))) | p1(tptp_fun_X_27(Y))))) | (r1(X!0, Y!28) & r1(Y!28, X!29) & p2(X!29) & ![Y: $i] : (p2(Y) | (~r1(X!29, Y))) & (~p1(X!29)) & (~p2(Y!28)) & p1(Y!28) & ![X: $i] : (p1(X) | (~r1(Y!28, X)))) | (r1(X!0, Y!30) & (~p1(Y!30)) & p2(Y!30) & ![X: $i] : (p2(X) | (~r1(Y!30, X))) & r1(Y!30, X!31) & (~p2(X!31)) & p1(X!31) & ![Y: $i] : (p1(Y) | (~r1(X!31, Y)))) | ![Y: $i] : (p1(Y) | (~r1(X!0, Y)) | (~p2(Y)) | (~((~r1(Y, tptp_fun_X_26(Y))) | p2(tptp_fun_X_26(Y)))))))),
% 0.22/0.49 inference(monotonicity,[status(thm)],[160, 129, 98, 67, 63, 32])).
% 0.22/0.49 tff(162,plain,
% 0.22/0.49 (((![Y: $i] : (p5(Y) | (~r1(X!0, Y)) | ((~p6(Y)) | (~(p6(tptp_fun_X_1(Y)) | (~r1(Y, tptp_fun_X_1(Y))))))) | ![Y: $i] : (p6(Y) | (~r1(X!0, Y)) | ((~p5(Y)) | (~(p5(tptp_fun_X_2(Y)) | (~r1(Y, tptp_fun_X_2(Y))))))) | (((~p6(Y!3)) & r1(X!0, Y!3) & (p5(Y!3) & ![X: $i] : (p5(X) | (~r1(Y!3, X)))) & ((~p5(X!4)) & r1(Y!3, X!4) & (p6(X!4) & ![Y: $i] : (p6(Y) | (~r1(X!4, Y)))))) | ((~p5(Y!5)) & r1(X!0, Y!5) & (p6(Y!5) & ![X: $i] : (p6(X) | (~r1(Y!5, X)))) & ((~p6(X!6)) & r1(Y!5, X!6) & (p5(X!6) & ![Y: $i] : (p5(Y) | (~r1(X!6, Y)))))) | ((~p6(Y!7)) & (~p5(Y!7)) & r1(X!0, Y!7) & (p6(Y!7) & ![X: $i] : (p6(X) | (~r1(Y!7, X)))) & (p5(Y!7) & ![X: $i] : (p5(X) | (~r1(Y!7, X))))))) & (![Y: $i] : ((~r1(X!0, Y)) | ((~p4(Y)) | (~((~r1(Y, tptp_fun_X_8(Y))) | p4(tptp_fun_X_8(Y))))) | p3(Y)) | ![Y: $i] : ((~r1(X!0, Y)) | p4(Y) | ((~p3(Y)) | (~((~r1(Y, tptp_fun_X_9(Y))) | p3(tptp_fun_X_9(Y)))))) | ((r1(X!0, Y!10) & (~p4(Y!10)) & (r1(Y!10, X!11) & (p4(X!11) & ![Y: $i] : ((~r1(X!11, Y)) | p4(Y))) & (~p3(X!11))) & (p3(Y!10) & ![X: $i] : ((~r1(Y!10, X)) | p3(X)))) | (r1(X!0, Y!12) & (p4(Y!12) & ![X: $i] : ((~r1(Y!12, X)) | p4(X))) & (~p3(Y!12)) & (r1(Y!12, X!13) & (~p4(X!13)) & (p3(X!13) & ![Y: $i] : ((~r1(X!13, Y)) | p3(Y))))) | (r1(X!0, Y!14) & (~p4(Y!14)) & (p4(Y!14) & ![X: $i] : ((~r1(Y!14, X)) | p4(X))) & (~p3(Y!14)) & (p3(Y!14) & ![X: $i] : ((~r1(Y!14, X)) | p3(X)))))) & (![Y: $i] : ((~r1(X!0, Y)) | p4(Y) | ((~p5(Y)) | (~(p5(tptp_fun_X_2(Y)) | (~r1(Y, tptp_fun_X_2(Y))))))) | (((~p5(Y!15)) & r1(X!0, Y!15) & (p4(Y!15) & ![X: $i] : ((~r1(Y!15, X)) | p4(X))) & (r1(Y!15, X!16) & (~p4(X!16)) & (p5(X!16) & ![Y: $i] : (p5(Y) | (~r1(X!16, Y)))))) | (r1(X!0, Y!17) & (~p4(Y!17)) & (p5(Y!17) & ![X: $i] : (p5(X) | (~r1(Y!17, X)))) & ((~p5(X!18)) & r1(Y!17, X!18) & (p4(X!18) & ![Y: $i] : ((~r1(X!18, Y)) | p4(Y))))) | ((~p5(Y!19)) & r1(X!0, Y!19) & (~p4(Y!19)) & (p4(Y!19) & ![X: $i] : ((~r1(Y!19, X)) | p4(X))) & (p5(Y!19) & ![X: $i] : (p5(X) | (~r1(Y!19, X)))))) | ![Y: $i] : (p5(Y) | (~r1(X!0, Y)) | ((~p4(Y)) | (~((~r1(Y, tptp_fun_X_8(Y))) | p4(tptp_fun_X_8(Y))))))) & ((~p5(Y!20)) & r1(X!0, Y!20) & (![X: $i] : (p5(X) | (~r1(Y!20, X))) & p5(Y!20))) & (![Y: $i] : ((~r1(X!0, Y)) | ((~p3(Y)) | (~((~r1(Y, tptp_fun_X_9(Y))) | p3(tptp_fun_X_9(Y))))) | p2(Y)) | ((r1(X!0, Y!21) & (~p3(Y!21)) & (p2(Y!21) & ![X: $i] : ((~r1(Y!21, X)) | p2(X))) & (r1(Y!21, X!22) & (p3(X!22) & ![Y: $i] : ((~r1(X!22, Y)) | p3(Y))) & (~p2(X!22)))) | (r1(X!0, Y!23) & (p3(Y!23) & ![X: $i] : ((~r1(Y!23, X)) | p3(X))) & (~p2(Y!23)) & (r1(Y!23, X!24) & (~p3(X!24)) & (p2(X!24) & ![Y: $i] : ((~r1(X!24, Y)) | p2(Y))))) | (r1(X!0, Y!25) & (~p3(Y!25)) & (p3(Y!25) & ![X: $i] : ((~r1(Y!25, X)) | p3(X))) & (~p2(Y!25)) & (p2(Y!25) & ![X: $i] : ((~r1(Y!25, X)) | p2(X))))) | ![Y: $i] : ((~r1(X!0, Y)) | p3(Y) | ((~p2(Y)) | (~((~r1(Y, tptp_fun_X_26(Y))) | p2(tptp_fun_X_26(Y))))))) & (![Y: $i] : ((~r1(X!0, Y)) | p2(Y) | ((~p1(Y)) | (~((~r1(Y, tptp_fun_X_27(Y))) | p1(tptp_fun_X_27(Y)))))) | ((r1(X!0, Y!28) & (r1(Y!28, X!29) & (p2(X!29) & ![Y: $i] : ((~r1(X!29, Y)) | p2(Y))) & (~p1(X!29))) & (~p2(Y!28)) & (p1(Y!28) & ![X: $i] : ((~r1(Y!28, X)) | p1(X)))) | (r1(X!0, Y!30) & (~p1(Y!30)) & (p2(Y!30) & ![X: $i] : ((~r1(Y!30, X)) | p2(X))) & (r1(Y!30, X!31) & (~p2(X!31)) & (p1(X!31) & ![Y: $i] : ((~r1(X!31, Y)) | p1(Y))))) | (r1(X!0, Y!32) & (~p2(Y!32)) & (~p1(Y!32)) & (p2(Y!32) & ![X: $i] : ((~r1(Y!32, X)) | p2(X))) & (p1(Y!32) & ![X: $i] : ((~r1(Y!32, X)) | p1(X))))) | ![Y: $i] : ((~r1(X!0, Y)) | p1(Y) | ((~p2(Y)) | (~((~r1(Y, tptp_fun_X_26(Y))) | p2(tptp_fun_X_26(Y)))))))) <=> $false),
% 0.22/0.49 inference(transitivity,[status(thm)],[161, 1])).
% 0.22/0.49 tff(163,plain,
% 0.22/0.49 (?[X: $i] : (~((~(![Y: $i] : (p5(Y) | (~r1(X, Y)) | (~(p6(Y) & ![X: $i] : (p6(X) | (~r1(Y, X)))))) | ![Y: $i] : (p6(Y) | (~r1(X, Y)) | (~(p5(Y) & ![X: $i] : (p5(X) | (~r1(Y, X)))))) | (~(![Y: $i] : (p6(Y) | (~r1(X, Y)) | (~(p5(Y) & ![X: $i] : (p5(X) | (~r1(Y, X))))) | ![X: $i] : (p5(X) | (~r1(Y, X)) | (~(p6(X) & ![Y: $i] : (p6(Y) | (~r1(X, Y))))))) & ![Y: $i] : (p5(Y) | (~r1(X, Y)) | (~(p6(Y) & ![X: $i] : (p6(X) | (~r1(Y, X))))) | ![X: $i] : (p6(X) | (~r1(Y, X)) | (~(p5(X) & ![Y: $i] : (p5(Y) | (~r1(X, Y))))))) & ![Y: $i] : (p6(Y) | p5(Y) | (~r1(X, Y)) | (~(p6(Y) & ![X: $i] : (p6(X) | (~r1(Y, X))))) | (~(p5(Y) & ![X: $i] : (p5(X) | (~r1(Y, X)))))))))) | (~(![Y: $i] : ((~r1(X, Y)) | (~(p4(Y) & ![X: $i] : ((~r1(Y, X)) | p4(X)))) | p3(Y)) | ![Y: $i] : ((~r1(X, Y)) | p4(Y) | (~(p3(Y) & ![X: $i] : ((~r1(Y, X)) | p3(X))))) | (~(![Y: $i] : ((~r1(X, Y)) | p4(Y) | ![X: $i] : ((~r1(Y, X)) | (~(p4(X) & ![Y: $i] : ((~r1(X, Y)) | p4(Y)))) | p3(X)) | (~(p3(Y) & ![X: $i] : ((~r1(Y, X)) | p3(X))))) & ![Y: $i] : ((~r1(X, Y)) | (~(p4(Y) & ![X: $i] : ((~r1(Y, X)) | p4(X)))) | p3(Y) | ![X: $i] : ((~r1(Y, X)) | p4(X) | (~(p3(X) & ![Y: $i] : ((~r1(X, Y)) | p3(Y)))))) & ![Y: $i] : ((~r1(X, Y)) | p4(Y) | (~(p4(Y) & ![X: $i] : ((~r1(Y, X)) | p4(X)))) | p3(Y) | (~(p3(Y) & ![X: $i] : ((~r1(Y, X)) | p3(X))))))))) | (~(![Y: $i] : ((~r1(X, Y)) | p4(Y) | (~(p5(Y) & ![X: $i] : (p5(X) | (~r1(Y, X)))))) | (~(![Y: $i] : (p5(Y) | (~r1(X, Y)) | (~(p4(Y) & ![X: $i] : ((~r1(Y, X)) | p4(X)))) | ![X: $i] : ((~r1(Y, X)) | p4(X) | (~(p5(X) & ![Y: $i] : (p5(Y) | (~r1(X, Y))))))) & ![Y: $i] : ((~r1(X, Y)) | p4(Y) | (~(p5(Y) & ![X: $i] : (p5(X) | (~r1(Y, X))))) | ![X: $i] : (p5(X) | (~r1(Y, X)) | (~(p4(X) & ![Y: $i] : ((~r1(X, Y)) | p4(Y)))))) & ![Y: $i] : (p5(Y) | (~r1(X, Y)) | p4(Y) | (~(p4(Y) & ![X: $i] : ((~r1(Y, X)) | p4(X)))) | (~(p5(Y) & ![X: $i] : (p5(X) | (~r1(Y, X)))))))) | ![Y: $i] : (p5(Y) | (~r1(X, Y)) | (~(p4(Y) & ![X: $i] : ((~r1(Y, X)) | p4(X))))))) | ![Y: $i] : (p5(Y) | (~r1(X, Y)) | (~(![X: $i] : (p5(X) | (~r1(Y, X))) & p5(Y)))) | (~(![Y: $i] : ((~r1(X, Y)) | (~(p3(Y) & ![X: $i] : ((~r1(Y, X)) | p3(X)))) | p2(Y)) | (~(![Y: $i] : ((~r1(X, Y)) | p3(Y) | (~(p2(Y) & ![X: $i] : ((~r1(Y, X)) | p2(X)))) | ![X: $i] : ((~r1(Y, X)) | (~(p3(X) & ![Y: $i] : ((~r1(X, Y)) | p3(Y)))) | p2(X))) & ![Y: $i] : ((~r1(X, Y)) | (~(p3(Y) & ![X: $i] : ((~r1(Y, X)) | p3(X)))) | p2(Y) | ![X: $i] : ((~r1(Y, X)) | p3(X) | (~(p2(X) & ![Y: $i] : ((~r1(X, Y)) | p2(Y)))))) & ![Y: $i] : ((~r1(X, Y)) | p3(Y) | (~(p3(Y) & ![X: $i] : ((~r1(Y, X)) | p3(X)))) | p2(Y) | (~(p2(Y) & ![X: $i] : ((~r1(Y, X)) | p2(X))))))) | ![Y: $i] : ((~r1(X, Y)) | p3(Y) | (~(p2(Y) & ![X: $i] : ((~r1(Y, X)) | p2(X))))))) | (~(![Y: $i] : ((~r1(X, Y)) | p2(Y) | (~(p1(Y) & ![X: $i] : ((~r1(Y, X)) | p1(X))))) | (~(![Y: $i] : ((~r1(X, Y)) | ![X: $i] : ((~r1(Y, X)) | (~(p2(X) & ![Y: $i] : ((~r1(X, Y)) | p2(Y)))) | p1(X)) | p2(Y) | (~(p1(Y) & ![X: $i] : ((~r1(Y, X)) | p1(X))))) & ![Y: $i] : ((~r1(X, Y)) | p1(Y) | (~(p2(Y) & ![X: $i] : ((~r1(Y, X)) | p2(X)))) | ![X: $i] : ((~r1(Y, X)) | p2(X) | (~(p1(X) & ![Y: $i] : ((~r1(X, Y)) | p1(Y)))))) & ![Y: $i] : ((~r1(X, Y)) | p2(Y) | p1(Y) | (~(p2(Y) & ![X: $i] : ((~r1(Y, X)) | p2(X)))) | (~(p1(Y) & ![X: $i] : ((~r1(Y, X)) | p1(X))))))) | ![Y: $i] : ((~r1(X, Y)) | p1(Y) | (~(p2(Y) & ![X: $i] : ((~r1(Y, X)) | p2(X))))))))) <=> ?[X: $i] : (~((~(![Y: $i] : (p5(Y) | (~r1(X, Y)) | (~(p6(Y) & ![X: $i] : (p6(X) | (~r1(Y, X)))))) | ![Y: $i] : (p6(Y) | (~r1(X, Y)) | (~(p5(Y) & ![X: $i] : (p5(X) | (~r1(Y, X)))))) | (~(![Y: $i] : (p6(Y) | (~r1(X, Y)) | (~(p5(Y) & ![X: $i] : (p5(X) | (~r1(Y, X))))) | ![X: $i] : (p5(X) | (~r1(Y, X)) | (~(p6(X) & ![Y: $i] : (p6(Y) | (~r1(X, Y))))))) & ![Y: $i] : (p5(Y) | (~r1(X, Y)) | (~(p6(Y) & ![X: $i] : (p6(X) | (~r1(Y, X))))) | ![X: $i] : (p6(X) | (~r1(Y, X)) | (~(p5(X) & ![Y: $i] : (p5(Y) | (~r1(X, Y))))))) & ![Y: $i] : (p6(Y) | p5(Y) | (~r1(X, Y)) | (~(p6(Y) & ![X: $i] : (p6(X) | (~r1(Y, X))))) | (~(p5(Y) & ![X: $i] : (p5(X) | (~r1(Y, X)))))))))) | (~(![Y: $i] : ((~r1(X, Y)) | (~(p4(Y) & ![X: $i] : ((~r1(Y, X)) | p4(X)))) | p3(Y)) | ![Y: $i] : ((~r1(X, Y)) | p4(Y) | (~(p3(Y) & ![X: $i] : ((~r1(Y, X)) | p3(X))))) | (~(![Y: $i] : ((~r1(X, Y)) | p4(Y) | ![X: $i] : ((~r1(Y, X)) | (~(p4(X) & ![Y: $i] : ((~r1(X, Y)) | p4(Y)))) | p3(X)) | (~(p3(Y) & ![X: $i] : ((~r1(Y, X)) | p3(X))))) & ![Y: $i] : ((~r1(X, Y)) | (~(p4(Y) & ![X: $i] : ((~r1(Y, X)) | p4(X)))) | p3(Y) | ![X: $i] : ((~r1(Y, X)) | p4(X) | (~(p3(X) & ![Y: $i] : ((~r1(X, Y)) | p3(Y)))))) & ![Y: $i] : ((~r1(X, Y)) | p4(Y) | (~(p4(Y) & ![X: $i] : ((~r1(Y, X)) | p4(X)))) | p3(Y) | (~(p3(Y) & ![X: $i] : ((~r1(Y, X)) | p3(X))))))))) | (~(![Y: $i] : ((~r1(X, Y)) | p4(Y) | (~(p5(Y) & ![X: $i] : (p5(X) | (~r1(Y, X)))))) | (~(![Y: $i] : (p5(Y) | (~r1(X, Y)) | (~(p4(Y) & ![X: $i] : ((~r1(Y, X)) | p4(X)))) | ![X: $i] : ((~r1(Y, X)) | p4(X) | (~(p5(X) & ![Y: $i] : (p5(Y) | (~r1(X, Y))))))) & ![Y: $i] : ((~r1(X, Y)) | p4(Y) | (~(p5(Y) & ![X: $i] : (p5(X) | (~r1(Y, X))))) | ![X: $i] : (p5(X) | (~r1(Y, X)) | (~(p4(X) & ![Y: $i] : ((~r1(X, Y)) | p4(Y)))))) & ![Y: $i] : (p5(Y) | (~r1(X, Y)) | p4(Y) | (~(p4(Y) & ![X: $i] : ((~r1(Y, X)) | p4(X)))) | (~(p5(Y) & ![X: $i] : (p5(X) | (~r1(Y, X)))))))) | ![Y: $i] : (p5(Y) | (~r1(X, Y)) | (~(p4(Y) & ![X: $i] : ((~r1(Y, X)) | p4(X))))))) | ![Y: $i] : (p5(Y) | (~r1(X, Y)) | (~(![X: $i] : (p5(X) | (~r1(Y, X))) & p5(Y)))) | (~(![Y: $i] : ((~r1(X, Y)) | (~(p3(Y) & ![X: $i] : ((~r1(Y, X)) | p3(X)))) | p2(Y)) | (~(![Y: $i] : ((~r1(X, Y)) | p3(Y) | (~(p2(Y) & ![X: $i] : ((~r1(Y, X)) | p2(X)))) | ![X: $i] : ((~r1(Y, X)) | (~(p3(X) & ![Y: $i] : ((~r1(X, Y)) | p3(Y)))) | p2(X))) & ![Y: $i] : ((~r1(X, Y)) | (~(p3(Y) & ![X: $i] : ((~r1(Y, X)) | p3(X)))) | p2(Y) | ![X: $i] : ((~r1(Y, X)) | p3(X) | (~(p2(X) & ![Y: $i] : ((~r1(X, Y)) | p2(Y)))))) & ![Y: $i] : ((~r1(X, Y)) | p3(Y) | (~(p3(Y) & ![X: $i] : ((~r1(Y, X)) | p3(X)))) | p2(Y) | (~(p2(Y) & ![X: $i] : ((~r1(Y, X)) | p2(X))))))) | ![Y: $i] : ((~r1(X, Y)) | p3(Y) | (~(p2(Y) & ![X: $i] : ((~r1(Y, X)) | p2(X))))))) | (~(![Y: $i] : ((~r1(X, Y)) | p2(Y) | (~(p1(Y) & ![X: $i] : ((~r1(Y, X)) | p1(X))))) | (~(![Y: $i] : ((~r1(X, Y)) | ![X: $i] : ((~r1(Y, X)) | (~(p2(X) & ![Y: $i] : ((~r1(X, Y)) | p2(Y)))) | p1(X)) | p2(Y) | (~(p1(Y) & ![X: $i] : ((~r1(Y, X)) | p1(X))))) & ![Y: $i] : ((~r1(X, Y)) | p1(Y) | (~(p2(Y) & ![X: $i] : ((~r1(Y, X)) | p2(X)))) | ![X: $i] : ((~r1(Y, X)) | p2(X) | (~(p1(X) & ![Y: $i] : ((~r1(X, Y)) | p1(Y)))))) & ![Y: $i] : ((~r1(X, Y)) | p2(Y) | p1(Y) | (~(p2(Y) & ![X: $i] : ((~r1(Y, X)) | p2(X)))) | (~(p1(Y) & ![X: $i] : ((~r1(Y, X)) | p1(X))))))) | ![Y: $i] : ((~r1(X, Y)) | p1(Y) | (~(p2(Y) & ![X: $i] : ((~r1(Y, X)) | p2(X)))))))))),
% 0.22/0.50 inference(rewrite,[status(thm)],[])).
% 0.22/0.50 tff(164,plain,
% 0.22/0.50 ((~(~?[X: $i] : (~((~(![Y: $i] : (p5(Y) | (~r1(X, Y)) | (~(p6(Y) & ![X: $i] : (p6(X) | (~r1(Y, X)))))) | ![Y: $i] : (p6(Y) | (~r1(X, Y)) | (~(p5(Y) & ![X: $i] : (p5(X) | (~r1(Y, X)))))) | (~(![Y: $i] : (p6(Y) | (~r1(X, Y)) | (~(p5(Y) & ![X: $i] : (p5(X) | (~r1(Y, X))))) | ![X: $i] : (p5(X) | (~r1(Y, X)) | (~(p6(X) & ![Y: $i] : (p6(Y) | (~r1(X, Y))))))) & ![Y: $i] : (p5(Y) | (~r1(X, Y)) | (~(p6(Y) & ![X: $i] : (p6(X) | (~r1(Y, X))))) | ![X: $i] : (p6(X) | (~r1(Y, X)) | (~(p5(X) & ![Y: $i] : (p5(Y) | (~r1(X, Y))))))) & ![Y: $i] : (p6(Y) | p5(Y) | (~r1(X, Y)) | (~(p6(Y) & ![X: $i] : (p6(X) | (~r1(Y, X))))) | (~(p5(Y) & ![X: $i] : (p5(X) | (~r1(Y, X)))))))))) | (~(![Y: $i] : ((~r1(X, Y)) | (~(p4(Y) & ![X: $i] : ((~r1(Y, X)) | p4(X)))) | p3(Y)) | ![Y: $i] : ((~r1(X, Y)) | p4(Y) | (~(p3(Y) & ![X: $i] : ((~r1(Y, X)) | p3(X))))) | (~(![Y: $i] : ((~r1(X, Y)) | p4(Y) | ![X: $i] : ((~r1(Y, X)) | (~(p4(X) & ![Y: $i] : ((~r1(X, Y)) | p4(Y)))) | p3(X)) | (~(p3(Y) & ![X: $i] : ((~r1(Y, X)) | p3(X))))) & ![Y: $i] : ((~r1(X, Y)) | (~(p4(Y) & ![X: $i] : ((~r1(Y, X)) | p4(X)))) | p3(Y) | ![X: $i] : ((~r1(Y, X)) | p4(X) | (~(p3(X) & ![Y: $i] : ((~r1(X, Y)) | p3(Y)))))) & ![Y: $i] : ((~r1(X, Y)) | p4(Y) | (~(p4(Y) & ![X: $i] : ((~r1(Y, X)) | p4(X)))) | p3(Y) | (~(p3(Y) & ![X: $i] : ((~r1(Y, X)) | p3(X))))))))) | (~(![Y: $i] : ((~r1(X, Y)) | p4(Y) | (~(p5(Y) & ![X: $i] : (p5(X) | (~r1(Y, X)))))) | (~(![Y: $i] : (p5(Y) | (~r1(X, Y)) | (~(p4(Y) & ![X: $i] : ((~r1(Y, X)) | p4(X)))) | ![X: $i] : ((~r1(Y, X)) | p4(X) | (~(p5(X) & ![Y: $i] : (p5(Y) | (~r1(X, Y))))))) & ![Y: $i] : ((~r1(X, Y)) | p4(Y) | (~(p5(Y) & ![X: $i] : (p5(X) | (~r1(Y, X))))) | ![X: $i] : (p5(X) | (~r1(Y, X)) | (~(p4(X) & ![Y: $i] : ((~r1(X, Y)) | p4(Y)))))) & ![Y: $i] : (p5(Y) | (~r1(X, Y)) | p4(Y) | (~(p4(Y) & ![X: $i] : ((~r1(Y, X)) | p4(X)))) | (~(p5(Y) & ![X: $i] : (p5(X) | (~r1(Y, X)))))))) | ![Y: $i] : (p5(Y) | (~r1(X, Y)) | (~(p4(Y) & ![X: $i] : ((~r1(Y, X)) | p4(X))))))) | ![Y: $i] : (p5(Y) | (~r1(X, Y)) | (~(![X: $i] : (p5(X) | (~r1(Y, X))) & p5(Y)))) | (~(![Y: $i] : ((~r1(X, Y)) | (~(p3(Y) & ![X: $i] : ((~r1(Y, X)) | p3(X)))) | p2(Y)) | (~(![Y: $i] : ((~r1(X, Y)) | p3(Y) | (~(p2(Y) & ![X: $i] : ((~r1(Y, X)) | p2(X)))) | ![X: $i] : ((~r1(Y, X)) | (~(p3(X) & ![Y: $i] : ((~r1(X, Y)) | p3(Y)))) | p2(X))) & ![Y: $i] : ((~r1(X, Y)) | (~(p3(Y) & ![X: $i] : ((~r1(Y, X)) | p3(X)))) | p2(Y) | ![X: $i] : ((~r1(Y, X)) | p3(X) | (~(p2(X) & ![Y: $i] : ((~r1(X, Y)) | p2(Y)))))) & ![Y: $i] : ((~r1(X, Y)) | p3(Y) | (~(p3(Y) & ![X: $i] : ((~r1(Y, X)) | p3(X)))) | p2(Y) | (~(p2(Y) & ![X: $i] : ((~r1(Y, X)) | p2(X))))))) | ![Y: $i] : ((~r1(X, Y)) | p3(Y) | (~(p2(Y) & ![X: $i] : ((~r1(Y, X)) | p2(X))))))) | (~(![Y: $i] : ((~r1(X, Y)) | p2(Y) | (~(p1(Y) & ![X: $i] : ((~r1(Y, X)) | p1(X))))) | (~(![Y: $i] : ((~r1(X, Y)) | ![X: $i] : ((~r1(Y, X)) | (~(p2(X) & ![Y: $i] : ((~r1(X, Y)) | p2(Y)))) | p1(X)) | p2(Y) | (~(p1(Y) & ![X: $i] : ((~r1(Y, X)) | p1(X))))) & ![Y: $i] : ((~r1(X, Y)) | p1(Y) | (~(p2(Y) & ![X: $i] : ((~r1(Y, X)) | p2(X)))) | ![X: $i] : ((~r1(Y, X)) | p2(X) | (~(p1(X) & ![Y: $i] : ((~r1(X, Y)) | p1(Y)))))) & ![Y: $i] : ((~r1(X, Y)) | p2(Y) | p1(Y) | (~(p2(Y) & ![X: $i] : ((~r1(Y, X)) | p2(X)))) | (~(p1(Y) & ![X: $i] : ((~r1(Y, X)) | p1(X))))))) | ![Y: $i] : ((~r1(X, Y)) | p1(Y) | (~(p2(Y) & ![X: $i] : ((~r1(Y, X)) | p2(X))))))))))) <=> ?[X: $i] : (~((~(![Y: $i] : (p5(Y) | (~r1(X, Y)) | (~(p6(Y) & ![X: $i] : (p6(X) | (~r1(Y, X)))))) | ![Y: $i] : (p6(Y) | (~r1(X, Y)) | (~(p5(Y) & ![X: $i] : (p5(X) | (~r1(Y, X)))))) | (~(![Y: $i] : (p6(Y) | (~r1(X, Y)) | (~(p5(Y) & ![X: $i] : (p5(X) | (~r1(Y, X))))) | ![X: $i] : (p5(X) | (~r1(Y, X)) | (~(p6(X) & ![Y: $i] : (p6(Y) | (~r1(X, Y))))))) & ![Y: $i] : (p5(Y) | (~r1(X, Y)) | (~(p6(Y) & ![X: $i] : (p6(X) | (~r1(Y, X))))) | ![X: $i] : (p6(X) | (~r1(Y, X)) | (~(p5(X) & ![Y: $i] : (p5(Y) | (~r1(X, Y))))))) & ![Y: $i] : (p6(Y) | p5(Y) | (~r1(X, Y)) | (~(p6(Y) & ![X: $i] : (p6(X) | (~r1(Y, X))))) | (~(p5(Y) & ![X: $i] : (p5(X) | (~r1(Y, X)))))))))) | (~(![Y: $i] : ((~r1(X, Y)) | (~(p4(Y) & ![X: $i] : ((~r1(Y, X)) | p4(X)))) | p3(Y)) | ![Y: $i] : ((~r1(X, Y)) | p4(Y) | (~(p3(Y) & ![X: $i] : ((~r1(Y, X)) | p3(X))))) | (~(![Y: $i] : ((~r1(X, Y)) | p4(Y) | ![X: $i] : ((~r1(Y, X)) | (~(p4(X) & ![Y: $i] : ((~r1(X, Y)) | p4(Y)))) | p3(X)) | (~(p3(Y) & ![X: $i] : ((~r1(Y, X)) | p3(X))))) & ![Y: $i] : ((~r1(X, Y)) | (~(p4(Y) & ![X: $i] : ((~r1(Y, X)) | p4(X)))) | p3(Y) | ![X: $i] : ((~r1(Y, X)) | p4(X) | (~(p3(X) & ![Y: $i] : ((~r1(X, Y)) | p3(Y)))))) & ![Y: $i] : ((~r1(X, Y)) | p4(Y) | (~(p4(Y) & ![X: $i] : ((~r1(Y, X)) | p4(X)))) | p3(Y) | (~(p3(Y) & ![X: $i] : ((~r1(Y, X)) | p3(X))))))))) | (~(![Y: $i] : ((~r1(X, Y)) | p4(Y) | (~(p5(Y) & ![X: $i] : (p5(X) | (~r1(Y, X)))))) | (~(![Y: $i] : (p5(Y) | (~r1(X, Y)) | (~(p4(Y) & ![X: $i] : ((~r1(Y, X)) | p4(X)))) | ![X: $i] : ((~r1(Y, X)) | p4(X) | (~(p5(X) & ![Y: $i] : (p5(Y) | (~r1(X, Y))))))) & ![Y: $i] : ((~r1(X, Y)) | p4(Y) | (~(p5(Y) & ![X: $i] : (p5(X) | (~r1(Y, X))))) | ![X: $i] : (p5(X) | (~r1(Y, X)) | (~(p4(X) & ![Y: $i] : ((~r1(X, Y)) | p4(Y)))))) & ![Y: $i] : (p5(Y) | (~r1(X, Y)) | p4(Y) | (~(p4(Y) & ![X: $i] : ((~r1(Y, X)) | p4(X)))) | (~(p5(Y) & ![X: $i] : (p5(X) | (~r1(Y, X)))))))) | ![Y: $i] : (p5(Y) | (~r1(X, Y)) | (~(p4(Y) & ![X: $i] : ((~r1(Y, X)) | p4(X))))))) | ![Y: $i] : (p5(Y) | (~r1(X, Y)) | (~(![X: $i] : (p5(X) | (~r1(Y, X))) & p5(Y)))) | (~(![Y: $i] : ((~r1(X, Y)) | (~(p3(Y) & ![X: $i] : ((~r1(Y, X)) | p3(X)))) | p2(Y)) | (~(![Y: $i] : ((~r1(X, Y)) | p3(Y) | (~(p2(Y) & ![X: $i] : ((~r1(Y, X)) | p2(X)))) | ![X: $i] : ((~r1(Y, X)) | (~(p3(X) & ![Y: $i] : ((~r1(X, Y)) | p3(Y)))) | p2(X))) & ![Y: $i] : ((~r1(X, Y)) | (~(p3(Y) & ![X: $i] : ((~r1(Y, X)) | p3(X)))) | p2(Y) | ![X: $i] : ((~r1(Y, X)) | p3(X) | (~(p2(X) & ![Y: $i] : ((~r1(X, Y)) | p2(Y)))))) & ![Y: $i] : ((~r1(X, Y)) | p3(Y) | (~(p3(Y) & ![X: $i] : ((~r1(Y, X)) | p3(X)))) | p2(Y) | (~(p2(Y) & ![X: $i] : ((~r1(Y, X)) | p2(X))))))) | ![Y: $i] : ((~r1(X, Y)) | p3(Y) | (~(p2(Y) & ![X: $i] : ((~r1(Y, X)) | p2(X))))))) | (~(![Y: $i] : ((~r1(X, Y)) | p2(Y) | (~(p1(Y) & ![X: $i] : ((~r1(Y, X)) | p1(X))))) | (~(![Y: $i] : ((~r1(X, Y)) | ![X: $i] : ((~r1(Y, X)) | (~(p2(X) & ![Y: $i] : ((~r1(X, Y)) | p2(Y)))) | p1(X)) | p2(Y) | (~(p1(Y) & ![X: $i] : ((~r1(Y, X)) | p1(X))))) & ![Y: $i] : ((~r1(X, Y)) | p1(Y) | (~(p2(Y) & ![X: $i] : ((~r1(Y, X)) | p2(X)))) | ![X: $i] : ((~r1(Y, X)) | p2(X) | (~(p1(X) & ![Y: $i] : ((~r1(X, Y)) | p1(Y)))))) & ![Y: $i] : ((~r1(X, Y)) | p2(Y) | p1(Y) | (~(p2(Y) & ![X: $i] : ((~r1(Y, X)) | p2(X)))) | (~(p1(Y) & ![X: $i] : ((~r1(Y, X)) | p1(X))))))) | ![Y: $i] : ((~r1(X, Y)) | p1(Y) | (~(p2(Y) & ![X: $i] : ((~r1(Y, X)) | p2(X)))))))))),
% 0.22/0.50 inference(rewrite,[status(thm)],[])).
% 0.22/0.50 tff(165,plain,
% 0.22/0.50 ((~?[X: $i] : (~(((((((~((![Y: $i] : (((~r1(X, Y)) | (~(p6(Y) & ![X: $i] : ((~r1(Y, X)) | p6(X))))) | p5(Y)) | ![Y: $i] : (((~r1(X, Y)) | p6(Y)) | (~((p5(Y) & ![X: $i] : ((~r1(Y, X)) | p5(X))) & p5(Y))))) | (~((![Y: $i] : ((((~r1(X, Y)) | ![X: $i] : (((~r1(Y, X)) | (~(p6(X) & ![Y: $i] : ((~r1(X, Y)) | p6(Y))))) | p5(X))) | p6(Y)) | (~((p5(Y) & ![X: $i] : ((~r1(Y, X)) | p5(X))) & p5(Y)))) & ![Y: $i] : ((((~r1(X, Y)) | (~(p6(Y) & ![X: $i] : ((~r1(Y, X)) | p6(X))))) | p5(Y)) | ![X: $i] : (((~r1(Y, X)) | p6(X)) | (~((p5(X) & ![Y: $i] : ((~r1(X, Y)) | p5(Y))) & p5(X)))))) & ![Y: $i] : (((((~r1(X, Y)) | (~(p6(Y) & ![X: $i] : ((~r1(Y, X)) | p6(X))))) | p5(Y)) | p6(Y)) | (~((p5(Y) & ![X: $i] : ((~r1(Y, X)) | p5(X))) & p5(Y)))))))) | (~((![Y: $i] : (((~r1(X, Y)) | (~(p5(Y) & ![X: $i] : ((~r1(Y, X)) | p5(X))))) | p4(Y)) | ![Y: $i] : (((~r1(X, Y)) | p5(Y)) | (~((p4(Y) & ![X: $i] : ((~r1(Y, X)) | p4(X))) & p4(Y))))) | (~((![Y: $i] : ((((~r1(X, Y)) | ![X: $i] : (((~r1(Y, X)) | (~(p5(X) & ![Y: $i] : ((~r1(X, Y)) | p5(Y))))) | p4(X))) | p5(Y)) | (~((p4(Y) & ![X: $i] : ((~r1(Y, X)) | p4(X))) & p4(Y)))) & ![Y: $i] : ((((~r1(X, Y)) | (~(p5(Y) & ![X: $i] : ((~r1(Y, X)) | p5(X))))) | p4(Y)) | ![X: $i] : (((~r1(Y, X)) | p5(X)) | (~((p4(X) & ![Y: $i] : ((~r1(X, Y)) | p4(Y))) & p4(X)))))) & ![Y: $i] : (((((~r1(X, Y)) | (~(p5(Y) & ![X: $i] : ((~r1(Y, X)) | p5(X))))) | p4(Y)) | p5(Y)) | (~((p4(Y) & ![X: $i] : ((~r1(Y, X)) | p4(X))) & p4(Y))))))))) | (~((![Y: $i] : (((~r1(X, Y)) | (~(p4(Y) & ![X: $i] : ((~r1(Y, X)) | p4(X))))) | p3(Y)) | ![Y: $i] : (((~r1(X, Y)) | p4(Y)) | (~((p3(Y) & ![X: $i] : ((~r1(Y, X)) | p3(X))) & p3(Y))))) | (~((![Y: $i] : ((((~r1(X, Y)) | ![X: $i] : (((~r1(Y, X)) | (~(p4(X) & ![Y: $i] : ((~r1(X, Y)) | p4(Y))))) | p3(X))) | p4(Y)) | (~((p3(Y) & ![X: $i] : ((~r1(Y, X)) | p3(X))) & p3(Y)))) & ![Y: $i] : ((((~r1(X, Y)) | (~(p4(Y) & ![X: $i] : ((~r1(Y, X)) | p4(X))))) | p3(Y)) | ![X: $i] : (((~r1(Y, X)) | p4(X)) | (~((p3(X) & ![Y: $i] : ((~r1(X, Y)) | p3(Y))) & p3(X)))))) & ![Y: $i] : (((((~r1(X, Y)) | (~(p4(Y) & ![X: $i] : ((~r1(Y, X)) | p4(X))))) | p3(Y)) | p4(Y)) | (~((p3(Y) & ![X: $i] : ((~r1(Y, X)) | p3(X))) & p3(Y))))))))) | (~((![Y: $i] : (((~r1(X, Y)) | (~(p3(Y) & ![X: $i] : ((~r1(Y, X)) | p3(X))))) | p2(Y)) | ![Y: $i] : (((~r1(X, Y)) | p3(Y)) | (~((p2(Y) & ![X: $i] : ((~r1(Y, X)) | p2(X))) & p2(Y))))) | (~((![Y: $i] : ((((~r1(X, Y)) | ![X: $i] : (((~r1(Y, X)) | (~(p3(X) & ![Y: $i] : ((~r1(X, Y)) | p3(Y))))) | p2(X))) | p3(Y)) | (~((p2(Y) & ![X: $i] : ((~r1(Y, X)) | p2(X))) & p2(Y)))) & ![Y: $i] : ((((~r1(X, Y)) | (~(p3(Y) & ![X: $i] : ((~r1(Y, X)) | p3(X))))) | p2(Y)) | ![X: $i] : (((~r1(Y, X)) | p3(X)) | (~((p2(X) & ![Y: $i] : ((~r1(X, Y)) | p2(Y))) & p2(X)))))) & ![Y: $i] : (((((~r1(X, Y)) | (~(p3(Y) & ![X: $i] : ((~r1(Y, X)) | p3(X))))) | p2(Y)) | p3(Y)) | (~((p2(Y) & ![X: $i] : ((~r1(Y, X)) | p2(X))) & p2(Y))))))))) | ![Y: $i] : (((~r1(X, Y)) | p5(Y)) | (~(![X: $i] : ((~r1(Y, X)) | p5(X)) & p5(Y))))) | ![Y: $i] : (((~r1(X, Y)) | p5(Y)) | (~(![X: $i] : ((~r1(Y, X)) | p5(X)) & p5(Y))))) | (~((![Y: $i] : (((~r1(X, Y)) | (~(p2(Y) & ![X: $i] : ((~r1(Y, X)) | p2(X))))) | p1(Y)) | ![Y: $i] : (((~r1(X, Y)) | p2(Y)) | (~((p1(Y) & ![X: $i] : ((~r1(Y, X)) | p1(X))) & p1(Y))))) | (~((![Y: $i] : ((((~r1(X, Y)) | ![X: $i] : (((~r1(Y, X)) | (~(p2(X) & ![Y: $i] : ((~r1(X, Y)) | p2(Y))))) | p1(X))) | p2(Y)) | (~((p1(Y) & ![X: $i] : ((~r1(Y, X)) | p1(X))) & p1(Y)))) & ![Y: $i] : ((((~r1(X, Y)) | (~(p2(Y) & ![X: $i] : ((~r1(Y, X)) | p2(X))))) | p1(Y)) | ![X: $i] : (((~r1(Y, X)) | p2(X)) | (~((p1(X) & ![Y: $i] : ((~r1(X, Y)) | p1(Y))) & p1(X)))))) & ![Y: $i] : (((((~r1(X, Y)) | (~(p2(Y) & ![X: $i] : ((~r1(Y, X)) | p2(X))))) | p1(Y)) | p2(Y)) | (~((p1(Y) & ![X: $i] : ((~r1(Y, X)) | p1(X))) & p1(Y))))))))))) <=> (~?[X: $i] : (~((~(![Y: $i] : (p5(Y) | (~r1(X, Y)) | (~(p6(Y) & ![X: $i] : (p6(X) | (~r1(Y, X)))))) | ![Y: $i] : (p6(Y) | (~r1(X, Y)) | (~(p5(Y) & ![X: $i] : (p5(X) | (~r1(Y, X)))))) | (~(![Y: $i] : (p6(Y) | (~r1(X, Y)) | (~(p5(Y) & ![X: $i] : (p5(X) | (~r1(Y, X))))) | ![X: $i] : (p5(X) | (~r1(Y, X)) | (~(p6(X) & ![Y: $i] : (p6(Y) | (~r1(X, Y))))))) & ![Y: $i] : (p5(Y) | (~r1(X, Y)) | (~(p6(Y) & ![X: $i] : (p6(X) | (~r1(Y, X))))) | ![X: $i] : (p6(X) | (~r1(Y, X)) | (~(p5(X) & ![Y: $i] : (p5(Y) | (~r1(X, Y))))))) & ![Y: $i] : (p6(Y) | p5(Y) | (~r1(X, Y)) | (~(p6(Y) & ![X: $i] : (p6(X) | (~r1(Y, X))))) | (~(p5(Y) & ![X: $i] : (p5(X) | (~r1(Y, X)))))))))) | (~(![Y: $i] : ((~r1(X, Y)) | (~(p4(Y) & ![X: $i] : ((~r1(Y, X)) | p4(X)))) | p3(Y)) | ![Y: $i] : ((~r1(X, Y)) | p4(Y) | (~(p3(Y) & ![X: $i] : ((~r1(Y, X)) | p3(X))))) | (~(![Y: $i] : ((~r1(X, Y)) | p4(Y) | ![X: $i] : ((~r1(Y, X)) | (~(p4(X) & ![Y: $i] : ((~r1(X, Y)) | p4(Y)))) | p3(X)) | (~(p3(Y) & ![X: $i] : ((~r1(Y, X)) | p3(X))))) & ![Y: $i] : ((~r1(X, Y)) | (~(p4(Y) & ![X: $i] : ((~r1(Y, X)) | p4(X)))) | p3(Y) | ![X: $i] : ((~r1(Y, X)) | p4(X) | (~(p3(X) & ![Y: $i] : ((~r1(X, Y)) | p3(Y)))))) & ![Y: $i] : ((~r1(X, Y)) | p4(Y) | (~(p4(Y) & ![X: $i] : ((~r1(Y, X)) | p4(X)))) | p3(Y) | (~(p3(Y) & ![X: $i] : ((~r1(Y, X)) | p3(X))))))))) | (~(![Y: $i] : ((~r1(X, Y)) | p4(Y) | (~(p5(Y) & ![X: $i] : (p5(X) | (~r1(Y, X)))))) | (~(![Y: $i] : (p5(Y) | (~r1(X, Y)) | (~(p4(Y) & ![X: $i] : ((~r1(Y, X)) | p4(X)))) | ![X: $i] : ((~r1(Y, X)) | p4(X) | (~(p5(X) & ![Y: $i] : (p5(Y) | (~r1(X, Y))))))) & ![Y: $i] : ((~r1(X, Y)) | p4(Y) | (~(p5(Y) & ![X: $i] : (p5(X) | (~r1(Y, X))))) | ![X: $i] : (p5(X) | (~r1(Y, X)) | (~(p4(X) & ![Y: $i] : ((~r1(X, Y)) | p4(Y)))))) & ![Y: $i] : (p5(Y) | (~r1(X, Y)) | p4(Y) | (~(p4(Y) & ![X: $i] : ((~r1(Y, X)) | p4(X)))) | (~(p5(Y) & ![X: $i] : (p5(X) | (~r1(Y, X)))))))) | ![Y: $i] : (p5(Y) | (~r1(X, Y)) | (~(p4(Y) & ![X: $i] : ((~r1(Y, X)) | p4(X))))))) | ![Y: $i] : (p5(Y) | (~r1(X, Y)) | (~(![X: $i] : (p5(X) | (~r1(Y, X))) & p5(Y)))) | (~(![Y: $i] : ((~r1(X, Y)) | (~(p3(Y) & ![X: $i] : ((~r1(Y, X)) | p3(X)))) | p2(Y)) | (~(![Y: $i] : ((~r1(X, Y)) | p3(Y) | (~(p2(Y) & ![X: $i] : ((~r1(Y, X)) | p2(X)))) | ![X: $i] : ((~r1(Y, X)) | (~(p3(X) & ![Y: $i] : ((~r1(X, Y)) | p3(Y)))) | p2(X))) & ![Y: $i] : ((~r1(X, Y)) | (~(p3(Y) & ![X: $i] : ((~r1(Y, X)) | p3(X)))) | p2(Y) | ![X: $i] : ((~r1(Y, X)) | p3(X) | (~(p2(X) & ![Y: $i] : ((~r1(X, Y)) | p2(Y)))))) & ![Y: $i] : ((~r1(X, Y)) | p3(Y) | (~(p3(Y) & ![X: $i] : ((~r1(Y, X)) | p3(X)))) | p2(Y) | (~(p2(Y) & ![X: $i] : ((~r1(Y, X)) | p2(X))))))) | ![Y: $i] : ((~r1(X, Y)) | p3(Y) | (~(p2(Y) & ![X: $i] : ((~r1(Y, X)) | p2(X))))))) | (~(![Y: $i] : ((~r1(X, Y)) | p2(Y) | (~(p1(Y) & ![X: $i] : ((~r1(Y, X)) | p1(X))))) | (~(![Y: $i] : ((~r1(X, Y)) | ![X: $i] : ((~r1(Y, X)) | (~(p2(X) & ![Y: $i] : ((~r1(X, Y)) | p2(Y)))) | p1(X)) | p2(Y) | (~(p1(Y) & ![X: $i] : ((~r1(Y, X)) | p1(X))))) & ![Y: $i] : ((~r1(X, Y)) | p1(Y) | (~(p2(Y) & ![X: $i] : ((~r1(Y, X)) | p2(X)))) | ![X: $i] : ((~r1(Y, X)) | p2(X) | (~(p1(X) & ![Y: $i] : ((~r1(X, Y)) | p1(Y)))))) & ![Y: $i] : ((~r1(X, Y)) | p2(Y) | p1(Y) | (~(p2(Y) & ![X: $i] : ((~r1(Y, X)) | p2(X)))) | (~(p1(Y) & ![X: $i] : ((~r1(Y, X)) | p1(X))))))) | ![Y: $i] : ((~r1(X, Y)) | p1(Y) | (~(p2(Y) & ![X: $i] : ((~r1(Y, X)) | p2(X))))))))))),
% 0.22/0.51 inference(rewrite,[status(thm)],[])).
% 0.22/0.51 tff(166,plain,
% 0.22/0.51 ((~(~?[X: $i] : (~(((((((~((![Y: $i] : (((~r1(X, Y)) | (~(p6(Y) & ![X: $i] : ((~r1(Y, X)) | p6(X))))) | p5(Y)) | ![Y: $i] : (((~r1(X, Y)) | p6(Y)) | (~((p5(Y) & ![X: $i] : ((~r1(Y, X)) | p5(X))) & p5(Y))))) | (~((![Y: $i] : ((((~r1(X, Y)) | ![X: $i] : (((~r1(Y, X)) | (~(p6(X) & ![Y: $i] : ((~r1(X, Y)) | p6(Y))))) | p5(X))) | p6(Y)) | (~((p5(Y) & ![X: $i] : ((~r1(Y, X)) | p5(X))) & p5(Y)))) & ![Y: $i] : ((((~r1(X, Y)) | (~(p6(Y) & ![X: $i] : ((~r1(Y, X)) | p6(X))))) | p5(Y)) | ![X: $i] : (((~r1(Y, X)) | p6(X)) | (~((p5(X) & ![Y: $i] : ((~r1(X, Y)) | p5(Y))) & p5(X)))))) & ![Y: $i] : (((((~r1(X, Y)) | (~(p6(Y) & ![X: $i] : ((~r1(Y, X)) | p6(X))))) | p5(Y)) | p6(Y)) | (~((p5(Y) & ![X: $i] : ((~r1(Y, X)) | p5(X))) & p5(Y)))))))) | (~((![Y: $i] : (((~r1(X, Y)) | (~(p5(Y) & ![X: $i] : ((~r1(Y, X)) | p5(X))))) | p4(Y)) | ![Y: $i] : (((~r1(X, Y)) | p5(Y)) | (~((p4(Y) & ![X: $i] : ((~r1(Y, X)) | p4(X))) & p4(Y))))) | (~((![Y: $i] : ((((~r1(X, Y)) | ![X: $i] : (((~r1(Y, X)) | (~(p5(X) & ![Y: $i] : ((~r1(X, Y)) | p5(Y))))) | p4(X))) | p5(Y)) | (~((p4(Y) & ![X: $i] : ((~r1(Y, X)) | p4(X))) & p4(Y)))) & ![Y: $i] : ((((~r1(X, Y)) | (~(p5(Y) & ![X: $i] : ((~r1(Y, X)) | p5(X))))) | p4(Y)) | ![X: $i] : (((~r1(Y, X)) | p5(X)) | (~((p4(X) & ![Y: $i] : ((~r1(X, Y)) | p4(Y))) & p4(X)))))) & ![Y: $i] : (((((~r1(X, Y)) | (~(p5(Y) & ![X: $i] : ((~r1(Y, X)) | p5(X))))) | p4(Y)) | p5(Y)) | (~((p4(Y) & ![X: $i] : ((~r1(Y, X)) | p4(X))) & p4(Y))))))))) | (~((![Y: $i] : (((~r1(X, Y)) | (~(p4(Y) & ![X: $i] : ((~r1(Y, X)) | p4(X))))) | p3(Y)) | ![Y: $i] : (((~r1(X, Y)) | p4(Y)) | (~((p3(Y) & ![X: $i] : ((~r1(Y, X)) | p3(X))) & p3(Y))))) | (~((![Y: $i] : ((((~r1(X, Y)) | ![X: $i] : (((~r1(Y, X)) | (~(p4(X) & ![Y: $i] : ((~r1(X, Y)) | p4(Y))))) | p3(X))) | p4(Y)) | (~((p3(Y) & ![X: $i] : ((~r1(Y, X)) | p3(X))) & p3(Y)))) & ![Y: $i] : ((((~r1(X, Y)) | (~(p4(Y) & ![X: $i] : ((~r1(Y, X)) | p4(X))))) | p3(Y)) | ![X: $i] : (((~r1(Y, X)) | p4(X)) | (~((p3(X) & ![Y: $i] : ((~r1(X, Y)) | p3(Y))) & p3(X)))))) & ![Y: $i] : (((((~r1(X, Y)) | (~(p4(Y) & ![X: $i] : ((~r1(Y, X)) | p4(X))))) | p3(Y)) | p4(Y)) | (~((p3(Y) & ![X: $i] : ((~r1(Y, X)) | p3(X))) & p3(Y))))))))) | (~((![Y: $i] : (((~r1(X, Y)) | (~(p3(Y) & ![X: $i] : ((~r1(Y, X)) | p3(X))))) | p2(Y)) | ![Y: $i] : (((~r1(X, Y)) | p3(Y)) | (~((p2(Y) & ![X: $i] : ((~r1(Y, X)) | p2(X))) & p2(Y))))) | (~((![Y: $i] : ((((~r1(X, Y)) | ![X: $i] : (((~r1(Y, X)) | (~(p3(X) & ![Y: $i] : ((~r1(X, Y)) | p3(Y))))) | p2(X))) | p3(Y)) | (~((p2(Y) & ![X: $i] : ((~r1(Y, X)) | p2(X))) & p2(Y)))) & ![Y: $i] : ((((~r1(X, Y)) | (~(p3(Y) & ![X: $i] : ((~r1(Y, X)) | p3(X))))) | p2(Y)) | ![X: $i] : (((~r1(Y, X)) | p3(X)) | (~((p2(X) & ![Y: $i] : ((~r1(X, Y)) | p2(Y))) & p2(X)))))) & ![Y: $i] : (((((~r1(X, Y)) | (~(p3(Y) & ![X: $i] : ((~r1(Y, X)) | p3(X))))) | p2(Y)) | p3(Y)) | (~((p2(Y) & ![X: $i] : ((~r1(Y, X)) | p2(X))) & p2(Y))))))))) | ![Y: $i] : (((~r1(X, Y)) | p5(Y)) | (~(![X: $i] : ((~r1(Y, X)) | p5(X)) & p5(Y))))) | ![Y: $i] : (((~r1(X, Y)) | p5(Y)) | (~(![X: $i] : ((~r1(Y, X)) | p5(X)) & p5(Y))))) | (~((![Y: $i] : (((~r1(X, Y)) | (~(p2(Y) & ![X: $i] : ((~r1(Y, X)) | p2(X))))) | p1(Y)) | ![Y: $i] : (((~r1(X, Y)) | p2(Y)) | (~((p1(Y) & ![X: $i] : ((~r1(Y, X)) | p1(X))) & p1(Y))))) | (~((![Y: $i] : ((((~r1(X, Y)) | ![X: $i] : (((~r1(Y, X)) | (~(p2(X) & ![Y: $i] : ((~r1(X, Y)) | p2(Y))))) | p1(X))) | p2(Y)) | (~((p1(Y) & ![X: $i] : ((~r1(Y, X)) | p1(X))) & p1(Y)))) & ![Y: $i] : ((((~r1(X, Y)) | (~(p2(Y) & ![X: $i] : ((~r1(Y, X)) | p2(X))))) | p1(Y)) | ![X: $i] : (((~r1(Y, X)) | p2(X)) | (~((p1(X) & ![Y: $i] : ((~r1(X, Y)) | p1(Y))) & p1(X)))))) & ![Y: $i] : (((((~r1(X, Y)) | (~(p2(Y) & ![X: $i] : ((~r1(Y, X)) | p2(X))))) | p1(Y)) | p2(Y)) | (~((p1(Y) & ![X: $i] : ((~r1(Y, X)) | p1(X))) & p1(Y)))))))))))) <=> (~(~?[X: $i] : (~((~(![Y: $i] : (p5(Y) | (~r1(X, Y)) | (~(p6(Y) & ![X: $i] : (p6(X) | (~r1(Y, X)))))) | ![Y: $i] : (p6(Y) | (~r1(X, Y)) | (~(p5(Y) & ![X: $i] : (p5(X) | (~r1(Y, X)))))) | (~(![Y: $i] : (p6(Y) | (~r1(X, Y)) | (~(p5(Y) & ![X: $i] : (p5(X) | (~r1(Y, X))))) | ![X: $i] : (p5(X) | (~r1(Y, X)) | (~(p6(X) & ![Y: $i] : (p6(Y) | (~r1(X, Y))))))) & ![Y: $i] : (p5(Y) | (~r1(X, Y)) | (~(p6(Y) & ![X: $i] : (p6(X) | (~r1(Y, X))))) | ![X: $i] : (p6(X) | (~r1(Y, X)) | (~(p5(X) & ![Y: $i] : (p5(Y) | (~r1(X, Y))))))) & ![Y: $i] : (p6(Y) | p5(Y) | (~r1(X, Y)) | (~(p6(Y) & ![X: $i] : (p6(X) | (~r1(Y, X))))) | (~(p5(Y) & ![X: $i] : (p5(X) | (~r1(Y, X)))))))))) | (~(![Y: $i] : ((~r1(X, Y)) | (~(p4(Y) & ![X: $i] : ((~r1(Y, X)) | p4(X)))) | p3(Y)) | ![Y: $i] : ((~r1(X, Y)) | p4(Y) | (~(p3(Y) & ![X: $i] : ((~r1(Y, X)) | p3(X))))) | (~(![Y: $i] : ((~r1(X, Y)) | p4(Y) | ![X: $i] : ((~r1(Y, X)) | (~(p4(X) & ![Y: $i] : ((~r1(X, Y)) | p4(Y)))) | p3(X)) | (~(p3(Y) & ![X: $i] : ((~r1(Y, X)) | p3(X))))) & ![Y: $i] : ((~r1(X, Y)) | (~(p4(Y) & ![X: $i] : ((~r1(Y, X)) | p4(X)))) | p3(Y) | ![X: $i] : ((~r1(Y, X)) | p4(X) | (~(p3(X) & ![Y: $i] : ((~r1(X, Y)) | p3(Y)))))) & ![Y: $i] : ((~r1(X, Y)) | p4(Y) | (~(p4(Y) & ![X: $i] : ((~r1(Y, X)) | p4(X)))) | p3(Y) | (~(p3(Y) & ![X: $i] : ((~r1(Y, X)) | p3(X))))))))) | (~(![Y: $i] : ((~r1(X, Y)) | p4(Y) | (~(p5(Y) & ![X: $i] : (p5(X) | (~r1(Y, X)))))) | (~(![Y: $i] : (p5(Y) | (~r1(X, Y)) | (~(p4(Y) & ![X: $i] : ((~r1(Y, X)) | p4(X)))) | ![X: $i] : ((~r1(Y, X)) | p4(X) | (~(p5(X) & ![Y: $i] : (p5(Y) | (~r1(X, Y))))))) & ![Y: $i] : ((~r1(X, Y)) | p4(Y) | (~(p5(Y) & ![X: $i] : (p5(X) | (~r1(Y, X))))) | ![X: $i] : (p5(X) | (~r1(Y, X)) | (~(p4(X) & ![Y: $i] : ((~r1(X, Y)) | p4(Y)))))) & ![Y: $i] : (p5(Y) | (~r1(X, Y)) | p4(Y) | (~(p4(Y) & ![X: $i] : ((~r1(Y, X)) | p4(X)))) | (~(p5(Y) & ![X: $i] : (p5(X) | (~r1(Y, X)))))))) | ![Y: $i] : (p5(Y) | (~r1(X, Y)) | (~(p4(Y) & ![X: $i] : ((~r1(Y, X)) | p4(X))))))) | ![Y: $i] : (p5(Y) | (~r1(X, Y)) | (~(![X: $i] : (p5(X) | (~r1(Y, X))) & p5(Y)))) | (~(![Y: $i] : ((~r1(X, Y)) | (~(p3(Y) & ![X: $i] : ((~r1(Y, X)) | p3(X)))) | p2(Y)) | (~(![Y: $i] : ((~r1(X, Y)) | p3(Y) | (~(p2(Y) & ![X: $i] : ((~r1(Y, X)) | p2(X)))) | ![X: $i] : ((~r1(Y, X)) | (~(p3(X) & ![Y: $i] : ((~r1(X, Y)) | p3(Y)))) | p2(X))) & ![Y: $i] : ((~r1(X, Y)) | (~(p3(Y) & ![X: $i] : ((~r1(Y, X)) | p3(X)))) | p2(Y) | ![X: $i] : ((~r1(Y, X)) | p3(X) | (~(p2(X) & ![Y: $i] : ((~r1(X, Y)) | p2(Y)))))) & ![Y: $i] : ((~r1(X, Y)) | p3(Y) | (~(p3(Y) & ![X: $i] : ((~r1(Y, X)) | p3(X)))) | p2(Y) | (~(p2(Y) & ![X: $i] : ((~r1(Y, X)) | p2(X))))))) | ![Y: $i] : ((~r1(X, Y)) | p3(Y) | (~(p2(Y) & ![X: $i] : ((~r1(Y, X)) | p2(X))))))) | (~(![Y: $i] : ((~r1(X, Y)) | p2(Y) | (~(p1(Y) & ![X: $i] : ((~r1(Y, X)) | p1(X))))) | (~(![Y: $i] : ((~r1(X, Y)) | ![X: $i] : ((~r1(Y, X)) | (~(p2(X) & ![Y: $i] : ((~r1(X, Y)) | p2(Y)))) | p1(X)) | p2(Y) | (~(p1(Y) & ![X: $i] : ((~r1(Y, X)) | p1(X))))) & ![Y: $i] : ((~r1(X, Y)) | p1(Y) | (~(p2(Y) & ![X: $i] : ((~r1(Y, X)) | p2(X)))) | ![X: $i] : ((~r1(Y, X)) | p2(X) | (~(p1(X) & ![Y: $i] : ((~r1(X, Y)) | p1(Y)))))) & ![Y: $i] : ((~r1(X, Y)) | p2(Y) | p1(Y) | (~(p2(Y) & ![X: $i] : ((~r1(Y, X)) | p2(X)))) | (~(p1(Y) & ![X: $i] : ((~r1(Y, X)) | p1(X))))))) | ![Y: $i] : ((~r1(X, Y)) | p1(Y) | (~(p2(Y) & ![X: $i] : ((~r1(Y, X)) | p2(X)))))))))))),
% 0.22/0.51 inference(monotonicity,[status(thm)],[165])).
% 0.22/0.51 tff(167,plain,
% 0.22/0.51 ((~(~?[X: $i] : (~(((((((~((![Y: $i] : (((~r1(X, Y)) | (~(p6(Y) & ![X: $i] : ((~r1(Y, X)) | p6(X))))) | p5(Y)) | ![Y: $i] : (((~r1(X, Y)) | p6(Y)) | (~((p5(Y) & ![X: $i] : ((~r1(Y, X)) | p5(X))) & p5(Y))))) | (~((![Y: $i] : ((((~r1(X, Y)) | ![X: $i] : (((~r1(Y, X)) | (~(p6(X) & ![Y: $i] : ((~r1(X, Y)) | p6(Y))))) | p5(X))) | p6(Y)) | (~((p5(Y) & ![X: $i] : ((~r1(Y, X)) | p5(X))) & p5(Y)))) & ![Y: $i] : ((((~r1(X, Y)) | (~(p6(Y) & ![X: $i] : ((~r1(Y, X)) | p6(X))))) | p5(Y)) | ![X: $i] : (((~r1(Y, X)) | p6(X)) | (~((p5(X) & ![Y: $i] : ((~r1(X, Y)) | p5(Y))) & p5(X)))))) & ![Y: $i] : (((((~r1(X, Y)) | (~(p6(Y) & ![X: $i] : ((~r1(Y, X)) | p6(X))))) | p5(Y)) | p6(Y)) | (~((p5(Y) & ![X: $i] : ((~r1(Y, X)) | p5(X))) & p5(Y)))))))) | (~((![Y: $i] : (((~r1(X, Y)) | (~(p5(Y) & ![X: $i] : ((~r1(Y, X)) | p5(X))))) | p4(Y)) | ![Y: $i] : (((~r1(X, Y)) | p5(Y)) | (~((p4(Y) & ![X: $i] : ((~r1(Y, X)) | p4(X))) & p4(Y))))) | (~((![Y: $i] : ((((~r1(X, Y)) | ![X: $i] : (((~r1(Y, X)) | (~(p5(X) & ![Y: $i] : ((~r1(X, Y)) | p5(Y))))) | p4(X))) | p5(Y)) | (~((p4(Y) & ![X: $i] : ((~r1(Y, X)) | p4(X))) & p4(Y)))) & ![Y: $i] : ((((~r1(X, Y)) | (~(p5(Y) & ![X: $i] : ((~r1(Y, X)) | p5(X))))) | p4(Y)) | ![X: $i] : (((~r1(Y, X)) | p5(X)) | (~((p4(X) & ![Y: $i] : ((~r1(X, Y)) | p4(Y))) & p4(X)))))) & ![Y: $i] : (((((~r1(X, Y)) | (~(p5(Y) & ![X: $i] : ((~r1(Y, X)) | p5(X))))) | p4(Y)) | p5(Y)) | (~((p4(Y) & ![X: $i] : ((~r1(Y, X)) | p4(X))) & p4(Y))))))))) | (~((![Y: $i] : (((~r1(X, Y)) | (~(p4(Y) & ![X: $i] : ((~r1(Y, X)) | p4(X))))) | p3(Y)) | ![Y: $i] : (((~r1(X, Y)) | p4(Y)) | (~((p3(Y) & ![X: $i] : ((~r1(Y, X)) | p3(X))) & p3(Y))))) | (~((![Y: $i] : ((((~r1(X, Y)) | ![X: $i] : (((~r1(Y, X)) | (~(p4(X) & ![Y: $i] : ((~r1(X, Y)) | p4(Y))))) | p3(X))) | p4(Y)) | (~((p3(Y) & ![X: $i] : ((~r1(Y, X)) | p3(X))) & p3(Y)))) & ![Y: $i] : ((((~r1(X, Y)) | (~(p4(Y) & ![X: $i] : ((~r1(Y, X)) | p4(X))))) | p3(Y)) | ![X: $i] : (((~r1(Y, X)) | p4(X)) | (~((p3(X) & ![Y: $i] : ((~r1(X, Y)) | p3(Y))) & p3(X)))))) & ![Y: $i] : (((((~r1(X, Y)) | (~(p4(Y) & ![X: $i] : ((~r1(Y, X)) | p4(X))))) | p3(Y)) | p4(Y)) | (~((p3(Y) & ![X: $i] : ((~r1(Y, X)) | p3(X))) & p3(Y))))))))) | (~((![Y: $i] : (((~r1(X, Y)) | (~(p3(Y) & ![X: $i] : ((~r1(Y, X)) | p3(X))))) | p2(Y)) | ![Y: $i] : (((~r1(X, Y)) | p3(Y)) | (~((p2(Y) & ![X: $i] : ((~r1(Y, X)) | p2(X))) & p2(Y))))) | (~((![Y: $i] : ((((~r1(X, Y)) | ![X: $i] : (((~r1(Y, X)) | (~(p3(X) & ![Y: $i] : ((~r1(X, Y)) | p3(Y))))) | p2(X))) | p3(Y)) | (~((p2(Y) & ![X: $i] : ((~r1(Y, X)) | p2(X))) & p2(Y)))) & ![Y: $i] : ((((~r1(X, Y)) | (~(p3(Y) & ![X: $i] : ((~r1(Y, X)) | p3(X))))) | p2(Y)) | ![X: $i] : (((~r1(Y, X)) | p3(X)) | (~((p2(X) & ![Y: $i] : ((~r1(X, Y)) | p2(Y))) & p2(X)))))) & ![Y: $i] : (((((~r1(X, Y)) | (~(p3(Y) & ![X: $i] : ((~r1(Y, X)) | p3(X))))) | p2(Y)) | p3(Y)) | (~((p2(Y) & ![X: $i] : ((~r1(Y, X)) | p2(X))) & p2(Y))))))))) | ![Y: $i] : (((~r1(X, Y)) | p5(Y)) | (~(![X: $i] : ((~r1(Y, X)) | p5(X)) & p5(Y))))) | ![Y: $i] : (((~r1(X, Y)) | p5(Y)) | (~(![X: $i] : ((~r1(Y, X)) | p5(X)) & p5(Y))))) | (~((![Y: $i] : (((~r1(X, Y)) | (~(p2(Y) & ![X: $i] : ((~r1(Y, X)) | p2(X))))) | p1(Y)) | ![Y: $i] : (((~r1(X, Y)) | p2(Y)) | (~((p1(Y) & ![X: $i] : ((~r1(Y, X)) | p1(X))) & p1(Y))))) | (~((![Y: $i] : ((((~r1(X, Y)) | ![X: $i] : (((~r1(Y, X)) | (~(p2(X) & ![Y: $i] : ((~r1(X, Y)) | p2(Y))))) | p1(X))) | p2(Y)) | (~((p1(Y) & ![X: $i] : ((~r1(Y, X)) | p1(X))) & p1(Y)))) & ![Y: $i] : ((((~r1(X, Y)) | (~(p2(Y) & ![X: $i] : ((~r1(Y, X)) | p2(X))))) | p1(Y)) | ![X: $i] : (((~r1(Y, X)) | p2(X)) | (~((p1(X) & ![Y: $i] : ((~r1(X, Y)) | p1(Y))) & p1(X)))))) & ![Y: $i] : (((((~r1(X, Y)) | (~(p2(Y) & ![X: $i] : ((~r1(Y, X)) | p2(X))))) | p1(Y)) | p2(Y)) | (~((p1(Y) & ![X: $i] : ((~r1(Y, X)) | p1(X))) & p1(Y)))))))))))) <=> ?[X: $i] : (~((~(![Y: $i] : (p5(Y) | (~r1(X, Y)) | (~(p6(Y) & ![X: $i] : (p6(X) | (~r1(Y, X)))))) | ![Y: $i] : (p6(Y) | (~r1(X, Y)) | (~(p5(Y) & ![X: $i] : (p5(X) | (~r1(Y, X)))))) | (~(![Y: $i] : (p6(Y) | (~r1(X, Y)) | (~(p5(Y) & ![X: $i] : (p5(X) | (~r1(Y, X))))) | ![X: $i] : (p5(X) | (~r1(Y, X)) | (~(p6(X) & ![Y: $i] : (p6(Y) | (~r1(X, Y))))))) & ![Y: $i] : (p5(Y) | (~r1(X, Y)) | (~(p6(Y) & ![X: $i] : (p6(X) | (~r1(Y, X))))) | ![X: $i] : (p6(X) | (~r1(Y, X)) | (~(p5(X) & ![Y: $i] : (p5(Y) | (~r1(X, Y))))))) & ![Y: $i] : (p6(Y) | p5(Y) | (~r1(X, Y)) | (~(p6(Y) & ![X: $i] : (p6(X) | (~r1(Y, X))))) | (~(p5(Y) & ![X: $i] : (p5(X) | (~r1(Y, X)))))))))) | (~(![Y: $i] : ((~r1(X, Y)) | (~(p4(Y) & ![X: $i] : ((~r1(Y, X)) | p4(X)))) | p3(Y)) | ![Y: $i] : ((~r1(X, Y)) | p4(Y) | (~(p3(Y) & ![X: $i] : ((~r1(Y, X)) | p3(X))))) | (~(![Y: $i] : ((~r1(X, Y)) | p4(Y) | ![X: $i] : ((~r1(Y, X)) | (~(p4(X) & ![Y: $i] : ((~r1(X, Y)) | p4(Y)))) | p3(X)) | (~(p3(Y) & ![X: $i] : ((~r1(Y, X)) | p3(X))))) & ![Y: $i] : ((~r1(X, Y)) | (~(p4(Y) & ![X: $i] : ((~r1(Y, X)) | p4(X)))) | p3(Y) | ![X: $i] : ((~r1(Y, X)) | p4(X) | (~(p3(X) & ![Y: $i] : ((~r1(X, Y)) | p3(Y)))))) & ![Y: $i] : ((~r1(X, Y)) | p4(Y) | (~(p4(Y) & ![X: $i] : ((~r1(Y, X)) | p4(X)))) | p3(Y) | (~(p3(Y) & ![X: $i] : ((~r1(Y, X)) | p3(X))))))))) | (~(![Y: $i] : ((~r1(X, Y)) | p4(Y) | (~(p5(Y) & ![X: $i] : (p5(X) | (~r1(Y, X)))))) | (~(![Y: $i] : (p5(Y) | (~r1(X, Y)) | (~(p4(Y) & ![X: $i] : ((~r1(Y, X)) | p4(X)))) | ![X: $i] : ((~r1(Y, X)) | p4(X) | (~(p5(X) & ![Y: $i] : (p5(Y) | (~r1(X, Y))))))) & ![Y: $i] : ((~r1(X, Y)) | p4(Y) | (~(p5(Y) & ![X: $i] : (p5(X) | (~r1(Y, X))))) | ![X: $i] : (p5(X) | (~r1(Y, X)) | (~(p4(X) & ![Y: $i] : ((~r1(X, Y)) | p4(Y)))))) & ![Y: $i] : (p5(Y) | (~r1(X, Y)) | p4(Y) | (~(p4(Y) & ![X: $i] : ((~r1(Y, X)) | p4(X)))) | (~(p5(Y) & ![X: $i] : (p5(X) | (~r1(Y, X)))))))) | ![Y: $i] : (p5(Y) | (~r1(X, Y)) | (~(p4(Y) & ![X: $i] : ((~r1(Y, X)) | p4(X))))))) | ![Y: $i] : (p5(Y) | (~r1(X, Y)) | (~(![X: $i] : (p5(X) | (~r1(Y, X))) & p5(Y)))) | (~(![Y: $i] : ((~r1(X, Y)) | (~(p3(Y) & ![X: $i] : ((~r1(Y, X)) | p3(X)))) | p2(Y)) | (~(![Y: $i] : ((~r1(X, Y)) | p3(Y) | (~(p2(Y) & ![X: $i] : ((~r1(Y, X)) | p2(X)))) | ![X: $i] : ((~r1(Y, X)) | (~(p3(X) & ![Y: $i] : ((~r1(X, Y)) | p3(Y)))) | p2(X))) & ![Y: $i] : ((~r1(X, Y)) | (~(p3(Y) & ![X: $i] : ((~r1(Y, X)) | p3(X)))) | p2(Y) | ![X: $i] : ((~r1(Y, X)) | p3(X) | (~(p2(X) & ![Y: $i] : ((~r1(X, Y)) | p2(Y)))))) & ![Y: $i] : ((~r1(X, Y)) | p3(Y) | (~(p3(Y) & ![X: $i] : ((~r1(Y, X)) | p3(X)))) | p2(Y) | (~(p2(Y) & ![X: $i] : ((~r1(Y, X)) | p2(X))))))) | ![Y: $i] : ((~r1(X, Y)) | p3(Y) | (~(p2(Y) & ![X: $i] : ((~r1(Y, X)) | p2(X))))))) | (~(![Y: $i] : ((~r1(X, Y)) | p2(Y) | (~(p1(Y) & ![X: $i] : ((~r1(Y, X)) | p1(X))))) | (~(![Y: $i] : ((~r1(X, Y)) | ![X: $i] : ((~r1(Y, X)) | (~(p2(X) & ![Y: $i] : ((~r1(X, Y)) | p2(Y)))) | p1(X)) | p2(Y) | (~(p1(Y) & ![X: $i] : ((~r1(Y, X)) | p1(X))))) & ![Y: $i] : ((~r1(X, Y)) | p1(Y) | (~(p2(Y) & ![X: $i] : ((~r1(Y, X)) | p2(X)))) | ![X: $i] : ((~r1(Y, X)) | p2(X) | (~(p1(X) & ![Y: $i] : ((~r1(X, Y)) | p1(Y)))))) & ![Y: $i] : ((~r1(X, Y)) | p2(Y) | p1(Y) | (~(p2(Y) & ![X: $i] : ((~r1(Y, X)) | p2(X)))) | (~(p1(Y) & ![X: $i] : ((~r1(Y, X)) | p1(X))))))) | ![Y: $i] : ((~r1(X, Y)) | p1(Y) | (~(p2(Y) & ![X: $i] : ((~r1(Y, X)) | p2(X)))))))))),
% 0.22/0.52 inference(transitivity,[status(thm)],[166, 164])).
% 0.22/0.52 tff(168,axiom,(~(~?[X: $i] : (~(((((((~((![Y: $i] : (((~r1(X, Y)) | (~(p6(Y) & ![X: $i] : ((~r1(Y, X)) | p6(X))))) | p5(Y)) | ![Y: $i] : (((~r1(X, Y)) | p6(Y)) | (~((p5(Y) & ![X: $i] : ((~r1(Y, X)) | p5(X))) & p5(Y))))) | (~((![Y: $i] : ((((~r1(X, Y)) | ![X: $i] : (((~r1(Y, X)) | (~(p6(X) & ![Y: $i] : ((~r1(X, Y)) | p6(Y))))) | p5(X))) | p6(Y)) | (~((p5(Y) & ![X: $i] : ((~r1(Y, X)) | p5(X))) & p5(Y)))) & ![Y: $i] : ((((~r1(X, Y)) | (~(p6(Y) & ![X: $i] : ((~r1(Y, X)) | p6(X))))) | p5(Y)) | ![X: $i] : (((~r1(Y, X)) | p6(X)) | (~((p5(X) & ![Y: $i] : ((~r1(X, Y)) | p5(Y))) & p5(X)))))) & ![Y: $i] : (((((~r1(X, Y)) | (~(p6(Y) & ![X: $i] : ((~r1(Y, X)) | p6(X))))) | p5(Y)) | p6(Y)) | (~((p5(Y) & ![X: $i] : ((~r1(Y, X)) | p5(X))) & p5(Y)))))))) | (~((![Y: $i] : (((~r1(X, Y)) | (~(p5(Y) & ![X: $i] : ((~r1(Y, X)) | p5(X))))) | p4(Y)) | ![Y: $i] : (((~r1(X, Y)) | p5(Y)) | (~((p4(Y) & ![X: $i] : ((~r1(Y, X)) | p4(X))) & p4(Y))))) | (~((![Y: $i] : ((((~r1(X, Y)) | ![X: $i] : (((~r1(Y, X)) | (~(p5(X) & ![Y: $i] : ((~r1(X, Y)) | p5(Y))))) | p4(X))) | p5(Y)) | (~((p4(Y) & ![X: $i] : ((~r1(Y, X)) | p4(X))) & p4(Y)))) & ![Y: $i] : ((((~r1(X, Y)) | (~(p5(Y) & ![X: $i] : ((~r1(Y, X)) | p5(X))))) | p4(Y)) | ![X: $i] : (((~r1(Y, X)) | p5(X)) | (~((p4(X) & ![Y: $i] : ((~r1(X, Y)) | p4(Y))) & p4(X)))))) & ![Y: $i] : (((((~r1(X, Y)) | (~(p5(Y) & ![X: $i] : ((~r1(Y, X)) | p5(X))))) | p4(Y)) | p5(Y)) | (~((p4(Y) & ![X: $i] : ((~r1(Y, X)) | p4(X))) & p4(Y))))))))) | (~((![Y: $i] : (((~r1(X, Y)) | (~(p4(Y) & ![X: $i] : ((~r1(Y, X)) | p4(X))))) | p3(Y)) | ![Y: $i] : (((~r1(X, Y)) | p4(Y)) | (~((p3(Y) & ![X: $i] : ((~r1(Y, X)) | p3(X))) & p3(Y))))) | (~((![Y: $i] : ((((~r1(X, Y)) | ![X: $i] : (((~r1(Y, X)) | (~(p4(X) & ![Y: $i] : ((~r1(X, Y)) | p4(Y))))) | p3(X))) | p4(Y)) | (~((p3(Y) & ![X: $i] : ((~r1(Y, X)) | p3(X))) & p3(Y)))) & ![Y: $i] : ((((~r1(X, Y)) | (~(p4(Y) & ![X: $i] : ((~r1(Y, X)) | p4(X))))) | p3(Y)) | ![X: $i] : (((~r1(Y, X)) | p4(X)) | (~((p3(X) & ![Y: $i] : ((~r1(X, Y)) | p3(Y))) & p3(X)))))) & ![Y: $i] : (((((~r1(X, Y)) | (~(p4(Y) & ![X: $i] : ((~r1(Y, X)) | p4(X))))) | p3(Y)) | p4(Y)) | (~((p3(Y) & ![X: $i] : ((~r1(Y, X)) | p3(X))) & p3(Y))))))))) | (~((![Y: $i] : (((~r1(X, Y)) | (~(p3(Y) & ![X: $i] : ((~r1(Y, X)) | p3(X))))) | p2(Y)) | ![Y: $i] : (((~r1(X, Y)) | p3(Y)) | (~((p2(Y) & ![X: $i] : ((~r1(Y, X)) | p2(X))) & p2(Y))))) | (~((![Y: $i] : ((((~r1(X, Y)) | ![X: $i] : (((~r1(Y, X)) | (~(p3(X) & ![Y: $i] : ((~r1(X, Y)) | p3(Y))))) | p2(X))) | p3(Y)) | (~((p2(Y) & ![X: $i] : ((~r1(Y, X)) | p2(X))) & p2(Y)))) & ![Y: $i] : ((((~r1(X, Y)) | (~(p3(Y) & ![X: $i] : ((~r1(Y, X)) | p3(X))))) | p2(Y)) | ![X: $i] : (((~r1(Y, X)) | p3(X)) | (~((p2(X) & ![Y: $i] : ((~r1(X, Y)) | p2(Y))) & p2(X)))))) & ![Y: $i] : (((((~r1(X, Y)) | (~(p3(Y) & ![X: $i] : ((~r1(Y, X)) | p3(X))))) | p2(Y)) | p3(Y)) | (~((p2(Y) & ![X: $i] : ((~r1(Y, X)) | p2(X))) & p2(Y))))))))) | ![Y: $i] : (((~r1(X, Y)) | p5(Y)) | (~(![X: $i] : ((~r1(Y, X)) | p5(X)) & p5(Y))))) | ![Y: $i] : (((~r1(X, Y)) | p5(Y)) | (~(![X: $i] : ((~r1(Y, X)) | p5(X)) & p5(Y))))) | (~((![Y: $i] : (((~r1(X, Y)) | (~(p2(Y) & ![X: $i] : ((~r1(Y, X)) | p2(X))))) | p1(Y)) | ![Y: $i] : (((~r1(X, Y)) | p2(Y)) | (~((p1(Y) & ![X: $i] : ((~r1(Y, X)) | p1(X))) & p1(Y))))) | (~((![Y: $i] : ((((~r1(X, Y)) | ![X: $i] : (((~r1(Y, X)) | (~(p2(X) & ![Y: $i] : ((~r1(X, Y)) | p2(Y))))) | p1(X))) | p2(Y)) | (~((p1(Y) & ![X: $i] : ((~r1(Y, X)) | p1(X))) & p1(Y)))) & ![Y: $i] : ((((~r1(X, Y)) | (~(p2(Y) & ![X: $i] : ((~r1(Y, X)) | p2(X))))) | p1(Y)) | ![X: $i] : (((~r1(Y, X)) | p2(X)) | (~((p1(X) & ![Y: $i] : ((~r1(X, Y)) | p1(Y))) & p1(X)))))) & ![Y: $i] : (((((~r1(X, Y)) | (~(p2(Y) & ![X: $i] : ((~r1(Y, X)) | p2(X))))) | p1(Y)) | p2(Y)) | (~((p1(Y) & ![X: $i] : ((~r1(Y, X)) | p1(X))) & p1(Y)))))))))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','main')).
% 0.22/0.52 tff(169,plain,
% 0.22/0.52 (?[X: $i] : (~((~(![Y: $i] : (p5(Y) | (~r1(X, Y)) | (~(p6(Y) & ![X: $i] : (p6(X) | (~r1(Y, X)))))) | ![Y: $i] : (p6(Y) | (~r1(X, Y)) | (~(p5(Y) & ![X: $i] : (p5(X) | (~r1(Y, X)))))) | (~(![Y: $i] : (p6(Y) | (~r1(X, Y)) | (~(p5(Y) & ![X: $i] : (p5(X) | (~r1(Y, X))))) | ![X: $i] : (p5(X) | (~r1(Y, X)) | (~(p6(X) & ![Y: $i] : (p6(Y) | (~r1(X, Y))))))) & ![Y: $i] : (p5(Y) | (~r1(X, Y)) | (~(p6(Y) & ![X: $i] : (p6(X) | (~r1(Y, X))))) | ![X: $i] : (p6(X) | (~r1(Y, X)) | (~(p5(X) & ![Y: $i] : (p5(Y) | (~r1(X, Y))))))) & ![Y: $i] : (p6(Y) | p5(Y) | (~r1(X, Y)) | (~(p6(Y) & ![X: $i] : (p6(X) | (~r1(Y, X))))) | (~(p5(Y) & ![X: $i] : (p5(X) | (~r1(Y, X)))))))))) | (~(![Y: $i] : ((~r1(X, Y)) | (~(p4(Y) & ![X: $i] : ((~r1(Y, X)) | p4(X)))) | p3(Y)) | ![Y: $i] : ((~r1(X, Y)) | p4(Y) | (~(p3(Y) & ![X: $i] : ((~r1(Y, X)) | p3(X))))) | (~(![Y: $i] : ((~r1(X, Y)) | p4(Y) | ![X: $i] : ((~r1(Y, X)) | (~(p4(X) & ![Y: $i] : ((~r1(X, Y)) | p4(Y)))) | p3(X)) | (~(p3(Y) & ![X: $i] : ((~r1(Y, X)) | p3(X))))) & ![Y: $i] : ((~r1(X, Y)) | (~(p4(Y) & ![X: $i] : ((~r1(Y, X)) | p4(X)))) | p3(Y) | ![X: $i] : ((~r1(Y, X)) | p4(X) | (~(p3(X) & ![Y: $i] : ((~r1(X, Y)) | p3(Y)))))) & ![Y: $i] : ((~r1(X, Y)) | p4(Y) | (~(p4(Y) & ![X: $i] : ((~r1(Y, X)) | p4(X)))) | p3(Y) | (~(p3(Y) & ![X: $i] : ((~r1(Y, X)) | p3(X))))))))) | (~(![Y: $i] : ((~r1(X, Y)) | p4(Y) | (~(p5(Y) & ![X: $i] : (p5(X) | (~r1(Y, X)))))) | (~(![Y: $i] : (p5(Y) | (~r1(X, Y)) | (~(p4(Y) & ![X: $i] : ((~r1(Y, X)) | p4(X)))) | ![X: $i] : ((~r1(Y, X)) | p4(X) | (~(p5(X) & ![Y: $i] : (p5(Y) | (~r1(X, Y))))))) & ![Y: $i] : ((~r1(X, Y)) | p4(Y) | (~(p5(Y) & ![X: $i] : (p5(X) | (~r1(Y, X))))) | ![X: $i] : (p5(X) | (~r1(Y, X)) | (~(p4(X) & ![Y: $i] : ((~r1(X, Y)) | p4(Y)))))) & ![Y: $i] : (p5(Y) | (~r1(X, Y)) | p4(Y) | (~(p4(Y) & ![X: $i] : ((~r1(Y, X)) | p4(X)))) | (~(p5(Y) & ![X: $i] : (p5(X) | (~r1(Y, X)))))))) | ![Y: $i] : (p5(Y) | (~r1(X, Y)) | (~(p4(Y) & ![X: $i] : ((~r1(Y, X)) | p4(X))))))) | ![Y: $i] : (p5(Y) | (~r1(X, Y)) | (~(![X: $i] : (p5(X) | (~r1(Y, X))) & p5(Y)))) | (~(![Y: $i] : ((~r1(X, Y)) | (~(p3(Y) & ![X: $i] : ((~r1(Y, X)) | p3(X)))) | p2(Y)) | (~(![Y: $i] : ((~r1(X, Y)) | p3(Y) | (~(p2(Y) & ![X: $i] : ((~r1(Y, X)) | p2(X)))) | ![X: $i] : ((~r1(Y, X)) | (~(p3(X) & ![Y: $i] : ((~r1(X, Y)) | p3(Y)))) | p2(X))) & ![Y: $i] : ((~r1(X, Y)) | (~(p3(Y) & ![X: $i] : ((~r1(Y, X)) | p3(X)))) | p2(Y) | ![X: $i] : ((~r1(Y, X)) | p3(X) | (~(p2(X) & ![Y: $i] : ((~r1(X, Y)) | p2(Y)))))) & ![Y: $i] : ((~r1(X, Y)) | p3(Y) | (~(p3(Y) & ![X: $i] : ((~r1(Y, X)) | p3(X)))) | p2(Y) | (~(p2(Y) & ![X: $i] : ((~r1(Y, X)) | p2(X))))))) | ![Y: $i] : ((~r1(X, Y)) | p3(Y) | (~(p2(Y) & ![X: $i] : ((~r1(Y, X)) | p2(X))))))) | (~(![Y: $i] : ((~r1(X, Y)) | p2(Y) | (~(p1(Y) & ![X: $i] : ((~r1(Y, X)) | p1(X))))) | (~(![Y: $i] : ((~r1(X, Y)) | ![X: $i] : ((~r1(Y, X)) | (~(p2(X) & ![Y: $i] : ((~r1(X, Y)) | p2(Y)))) | p1(X)) | p2(Y) | (~(p1(Y) & ![X: $i] : ((~r1(Y, X)) | p1(X))))) & ![Y: $i] : ((~r1(X, Y)) | p1(Y) | (~(p2(Y) & ![X: $i] : ((~r1(Y, X)) | p2(X)))) | ![X: $i] : ((~r1(Y, X)) | p2(X) | (~(p1(X) & ![Y: $i] : ((~r1(X, Y)) | p1(Y)))))) & ![Y: $i] : ((~r1(X, Y)) | p2(Y) | p1(Y) | (~(p2(Y) & ![X: $i] : ((~r1(Y, X)) | p2(X)))) | (~(p1(Y) & ![X: $i] : ((~r1(Y, X)) | p1(X))))))) | ![Y: $i] : ((~r1(X, Y)) | p1(Y) | (~(p2(Y) & ![X: $i] : ((~r1(Y, X)) | p2(X)))))))))),
% 0.22/0.52 inference(modus_ponens,[status(thm)],[168, 167])).
% 0.22/0.52 tff(170,plain,
% 0.22/0.52 (?[X: $i] : (~((~(![Y: $i] : (p5(Y) | (~r1(X, Y)) | (~(p6(Y) & ![X: $i] : (p6(X) | (~r1(Y, X)))))) | ![Y: $i] : (p6(Y) | (~r1(X, Y)) | (~(p5(Y) & ![X: $i] : (p5(X) | (~r1(Y, X)))))) | (~(![Y: $i] : (p6(Y) | (~r1(X, Y)) | (~(p5(Y) & ![X: $i] : (p5(X) | (~r1(Y, X))))) | ![X: $i] : (p5(X) | (~r1(Y, X)) | (~(p6(X) & ![Y: $i] : (p6(Y) | (~r1(X, Y))))))) & ![Y: $i] : (p5(Y) | (~r1(X, Y)) | (~(p6(Y) & ![X: $i] : (p6(X) | (~r1(Y, X))))) | ![X: $i] : (p6(X) | (~r1(Y, X)) | (~(p5(X) & ![Y: $i] : (p5(Y) | (~r1(X, Y))))))) & ![Y: $i] : (p6(Y) | p5(Y) | (~r1(X, Y)) | (~(p6(Y) & ![X: $i] : (p6(X) | (~r1(Y, X))))) | (~(p5(Y) & ![X: $i] : (p5(X) | (~r1(Y, X)))))))))) | (~(![Y: $i] : ((~r1(X, Y)) | (~(p4(Y) & ![X: $i] : ((~r1(Y, X)) | p4(X)))) | p3(Y)) | ![Y: $i] : ((~r1(X, Y)) | p4(Y) | (~(p3(Y) & ![X: $i] : ((~r1(Y, X)) | p3(X))))) | (~(![Y: $i] : ((~r1(X, Y)) | p4(Y) | ![X: $i] : ((~r1(Y, X)) | (~(p4(X) & ![Y: $i] : ((~r1(X, Y)) | p4(Y)))) | p3(X)) | (~(p3(Y) & ![X: $i] : ((~r1(Y, X)) | p3(X))))) & ![Y: $i] : ((~r1(X, Y)) | (~(p4(Y) & ![X: $i] : ((~r1(Y, X)) | p4(X)))) | p3(Y) | ![X: $i] : ((~r1(Y, X)) | p4(X) | (~(p3(X) & ![Y: $i] : ((~r1(X, Y)) | p3(Y)))))) & ![Y: $i] : ((~r1(X, Y)) | p4(Y) | (~(p4(Y) & ![X: $i] : ((~r1(Y, X)) | p4(X)))) | p3(Y) | (~(p3(Y) & ![X: $i] : ((~r1(Y, X)) | p3(X))))))))) | (~(![Y: $i] : ((~r1(X, Y)) | p4(Y) | (~(p5(Y) & ![X: $i] : (p5(X) | (~r1(Y, X)))))) | (~(![Y: $i] : (p5(Y) | (~r1(X, Y)) | (~(p4(Y) & ![X: $i] : ((~r1(Y, X)) | p4(X)))) | ![X: $i] : ((~r1(Y, X)) | p4(X) | (~(p5(X) & ![Y: $i] : (p5(Y) | (~r1(X, Y))))))) & ![Y: $i] : ((~r1(X, Y)) | p4(Y) | (~(p5(Y) & ![X: $i] : (p5(X) | (~r1(Y, X))))) | ![X: $i] : (p5(X) | (~r1(Y, X)) | (~(p4(X) & ![Y: $i] : ((~r1(X, Y)) | p4(Y)))))) & ![Y: $i] : (p5(Y) | (~r1(X, Y)) | p4(Y) | (~(p4(Y) & ![X: $i] : ((~r1(Y, X)) | p4(X)))) | (~(p5(Y) & ![X: $i] : (p5(X) | (~r1(Y, X)))))))) | ![Y: $i] : (p5(Y) | (~r1(X, Y)) | (~(p4(Y) & ![X: $i] : ((~r1(Y, X)) | p4(X))))))) | ![Y: $i] : (p5(Y) | (~r1(X, Y)) | (~(![X: $i] : (p5(X) | (~r1(Y, X))) & p5(Y)))) | (~(![Y: $i] : ((~r1(X, Y)) | (~(p3(Y) & ![X: $i] : ((~r1(Y, X)) | p3(X)))) | p2(Y)) | (~(![Y: $i] : ((~r1(X, Y)) | p3(Y) | (~(p2(Y) & ![X: $i] : ((~r1(Y, X)) | p2(X)))) | ![X: $i] : ((~r1(Y, X)) | (~(p3(X) & ![Y: $i] : ((~r1(X, Y)) | p3(Y)))) | p2(X))) & ![Y: $i] : ((~r1(X, Y)) | (~(p3(Y) & ![X: $i] : ((~r1(Y, X)) | p3(X)))) | p2(Y) | ![X: $i] : ((~r1(Y, X)) | p3(X) | (~(p2(X) & ![Y: $i] : ((~r1(X, Y)) | p2(Y)))))) & ![Y: $i] : ((~r1(X, Y)) | p3(Y) | (~(p3(Y) & ![X: $i] : ((~r1(Y, X)) | p3(X)))) | p2(Y) | (~(p2(Y) & ![X: $i] : ((~r1(Y, X)) | p2(X))))))) | ![Y: $i] : ((~r1(X, Y)) | p3(Y) | (~(p2(Y) & ![X: $i] : ((~r1(Y, X)) | p2(X))))))) | (~(![Y: $i] : ((~r1(X, Y)) | p2(Y) | (~(p1(Y) & ![X: $i] : ((~r1(Y, X)) | p1(X))))) | (~(![Y: $i] : ((~r1(X, Y)) | ![X: $i] : ((~r1(Y, X)) | (~(p2(X) & ![Y: $i] : ((~r1(X, Y)) | p2(Y)))) | p1(X)) | p2(Y) | (~(p1(Y) & ![X: $i] : ((~r1(Y, X)) | p1(X))))) & ![Y: $i] : ((~r1(X, Y)) | p1(Y) | (~(p2(Y) & ![X: $i] : ((~r1(Y, X)) | p2(X)))) | ![X: $i] : ((~r1(Y, X)) | p2(X) | (~(p1(X) & ![Y: $i] : ((~r1(X, Y)) | p1(Y)))))) & ![Y: $i] : ((~r1(X, Y)) | p2(Y) | p1(Y) | (~(p2(Y) & ![X: $i] : ((~r1(Y, X)) | p2(X)))) | (~(p1(Y) & ![X: $i] : ((~r1(Y, X)) | p1(X))))))) | ![Y: $i] : ((~r1(X, Y)) | p1(Y) | (~(p2(Y) & ![X: $i] : ((~r1(Y, X)) | p2(X)))))))))),
% 0.22/0.53 inference(modus_ponens,[status(thm)],[169, 163])).
% 0.22/0.53 tff(171,plain,
% 0.22/0.53 ($false),
% 0.22/0.53 inference(modus_ponens,[status(thm)],[170, 162])).
% 0.22/0.53 % SZS output end Proof
% 0.22/0.53 % E exiting
%------------------------------------------------------------------------------