%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : SYN067+1 : TPTP v9.0.0. Released v2.0.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n006.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sat Jun 21 05:38:07 AM UTC 2025
% Result : Theorem 0.62s 0.77s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.11 % Problem : SYN067+1 : TPTP v9.0.0. Released v2.0.0.
% 0.11/0.11 % Command : run_E %s %d THM
% 0.11/0.32 % Computer : n006.cluster.edu
% 0.11/0.32 % Model : x86_64 x86_64
% 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.32 % Memory : 8042.1875MB
% 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.32 % CPULimit : 300
% 0.11/0.32 % WCLimit : 300
% 0.11/0.32 % DateTime : Fri Jun 20 12:27:05 EDT 2025
% 0.11/0.32 % CPUTime :
% 0.62/0.77 % SZS status Theorem
% 0.62/0.77 % SZS output start Proof
% 0.62/0.77 tff(big_r_type, type, (
% 0.62/0.77 big_r: ( $i * $i ) > $o)).
% 0.62/0.77 tff(tptp_fun_X1_8_type, type, (
% 0.62/0.77 tptp_fun_X1_8: $i)).
% 0.62/0.77 tff(big_p_type, type, (
% 0.62/0.77 big_p: $i > $o)).
% 0.62/0.77 tff(tptp_fun_Z_1_type, type, (
% 0.62/0.77 tptp_fun_Z_1: $i > $i)).
% 0.62/0.77 tff(tptp_fun_W_0_type, type, (
% 0.62/0.77 tptp_fun_W_0: $i > $i)).
% 0.62/0.77 tff(tptp_fun_Y1_9_type, type, (
% 0.62/0.77 tptp_fun_Y1_9: $i)).
% 0.62/0.77 tff(a_type, type, (
% 0.62/0.77 a: $i)).
% 0.62/0.77 tff(tptp_fun_Z1_5_type, type, (
% 0.62/0.77 tptp_fun_Z1_5: $i > $i)).
% 0.62/0.77 tff(tptp_fun_W1_4_type, type, (
% 0.62/0.77 tptp_fun_W1_4: $i > $i)).
% 0.62/0.77 tff(tptp_fun_Z2_7_type, type, (
% 0.62/0.77 tptp_fun_Z2_7: $i > $i)).
% 0.62/0.77 tff(tptp_fun_W2_6_type, type, (
% 0.62/0.77 tptp_fun_W2_6: $i > $i)).
% 0.62/0.77 tff(tptp_fun_X_2_type, type, (
% 0.62/0.77 tptp_fun_X_2: $i)).
% 0.62/0.77 tff(tptp_fun_Y_3_type, type, (
% 0.62/0.77 tptp_fun_Y_3: $i)).
% 0.62/0.77 tff(1,assumption,(~((~big_p(tptp_fun_Z_1(X1!8))) | (~big_r(X1!8, tptp_fun_W_0(X1!8))) | (~big_r(tptp_fun_W_0(X1!8), tptp_fun_Z_1(X1!8))))), introduced(assumption)).
% 0.62/0.77 tff(2,plain,
% 0.62/0.77 (((~big_p(tptp_fun_Z_1(X1!8))) | (~big_r(X1!8, tptp_fun_W_0(X1!8))) | (~big_r(tptp_fun_W_0(X1!8), tptp_fun_Z_1(X1!8)))) | big_r(tptp_fun_W_0(X1!8), tptp_fun_Z_1(X1!8))),
% 0.62/0.77 inference(tautology,[status(thm)],[])).
% 0.62/0.77 tff(3,plain,
% 0.62/0.77 (big_r(tptp_fun_W_0(X1!8), tptp_fun_Z_1(X1!8))),
% 0.62/0.77 inference(unit_resolution,[status(thm)],[2, 1])).
% 0.62/0.77 tff(4,plain,
% 0.62/0.77 (((~big_p(tptp_fun_Z_1(X1!8))) | (~big_r(X1!8, tptp_fun_W_0(X1!8))) | (~big_r(tptp_fun_W_0(X1!8), tptp_fun_Z_1(X1!8)))) | big_r(X1!8, tptp_fun_W_0(X1!8))),
% 0.62/0.77 inference(tautology,[status(thm)],[])).
% 0.62/0.77 tff(5,plain,
% 0.62/0.77 (big_r(X1!8, tptp_fun_W_0(X1!8))),
% 0.62/0.77 inference(unit_resolution,[status(thm)],[4, 1])).
% 0.62/0.77 tff(6,plain,
% 0.62/0.77 (((~big_p(tptp_fun_Z_1(X1!8))) | (~big_r(X1!8, tptp_fun_W_0(X1!8))) | (~big_r(tptp_fun_W_0(X1!8), tptp_fun_Z_1(X1!8)))) | big_p(tptp_fun_Z_1(X1!8))),
% 0.62/0.77 inference(tautology,[status(thm)],[])).
% 0.62/0.77 tff(7,plain,
% 0.62/0.77 (big_p(tptp_fun_Z_1(X1!8))),
% 0.62/0.77 inference(unit_resolution,[status(thm)],[6, 1])).
% 0.62/0.77 tff(8,assumption,((~big_p(a)) | (~big_p(Y1!9)) | (~big_r(X1!8, Y1!9)) | (~![Z2: $i, W2: $i] : ((~big_p(Z2)) | (~big_r(X1!8, W2)) | (~big_r(W2, Z2))))), introduced(assumption)).
% 0.62/0.77 tff(9,assumption,(~big_p(a)), introduced(assumption)).
% 0.62/0.77 tff(10,plain,
% 0.62/0.77 (((~big_p(a)) | big_p(X1!8) | (~![Z1: $i, W1: $i] : ((~big_p(Z1)) | (~big_r(X1!8, W1)) | (~big_r(W1, Z1))))) | big_p(a)),
% 0.62/0.77 inference(tautology,[status(thm)],[])).
% 0.62/0.77 tff(11,plain,
% 0.62/0.77 ((~big_p(a)) | big_p(X1!8) | (~![Z1: $i, W1: $i] : ((~big_p(Z1)) | (~big_r(X1!8, W1)) | (~big_r(W1, Z1))))),
% 0.62/0.77 inference(unit_resolution,[status(thm)],[10, 9])).
% 0.62/0.77 tff(12,plain,
% 0.62/0.77 (((~big_p(a)) | (~((~big_p(X!2)) | (~((~big_p(Y!3)) | (~big_r(X!2, Y!3)))))) | (~![Z: $i, W: $i] : ((~big_p(Z)) | (~big_r(X!2, W)) | (~big_r(W, Z))))) | big_p(a)),
% 0.62/0.77 inference(tautology,[status(thm)],[])).
% 0.62/0.77 tff(13,plain,
% 0.62/0.77 ((~big_p(a)) | (~((~big_p(X!2)) | (~((~big_p(Y!3)) | (~big_r(X!2, Y!3)))))) | (~![Z: $i, W: $i] : ((~big_p(Z)) | (~big_r(X!2, W)) | (~big_r(W, Z))))),
% 0.62/0.77 inference(unit_resolution,[status(thm)],[12, 9])).
% 0.62/0.77 tff(14,plain,
% 0.62/0.77 (((~((~big_p(a)) | big_p(X1!8) | (~![Z1: $i, W1: $i] : ((~big_p(Z1)) | (~big_r(X1!8, W1)) | (~big_r(W1, Z1)))))) | (~((~big_p(a)) | (~((~big_p(X!2)) | (~((~big_p(Y!3)) | (~big_r(X!2, Y!3)))))) | (~![Z: $i, W: $i] : ((~big_p(Z)) | (~big_r(X!2, W)) | (~big_r(W, Z)))))) | (~((~big_p(a)) | (~big_p(Y1!9)) | (~big_r(X1!8, Y1!9)) | (~![Z2: $i, W2: $i] : ((~big_p(Z2)) | (~big_r(X1!8, W2)) | (~big_r(W2, Z2))))))) <=> ((~((~big_p(a)) | big_p(X1!8) | (~![Z1: $i, W1: $i] : ((~big_p(Z1)) | (~big_r(X1!8, W1)) | (~big_r(W1, Z1)))))) | (~((~big_p(a)) | (~((~big_p(X!2)) | (~((~big_p(Y!3)) | (~big_r(X!2, Y!3)))))) | (~![Z: $i, W: $i] : ((~big_p(Z)) | (~big_r(X!2, W)) | (~big_r(W, Z)))))) | (~((~big_p(a)) | (~big_p(Y1!9)) | (~big_r(X1!8, Y1!9)) | (~![Z2: $i, W2: $i] : ((~big_p(Z2)) | (~big_r(X1!8, W2)) | (~big_r(W2, Z2)))))))),
% 0.62/0.77 inference(rewrite,[status(thm)],[])).
% 0.62/0.77 tff(15,plain,
% 0.62/0.77 (((~((~big_p(a)) | big_p(X1!8) | (~![Z1: $i, W1: $i] : ((~big_p(Z1)) | (~big_r(X1!8, W1)) | (~big_r(W1, Z1)))))) | (~((~big_p(a)) | (~((~big_p(X!2)) | (~((~big_p(Y!3)) | (~big_r(X!2, Y!3)))))) | (~![Z: $i, W: $i] : ((~big_p(Z)) | (~big_r(X!2, W)) | (~big_r(W, Z)))))) | (~((~big_p(a)) | (~big_p(Y1!9)) | (~big_r(X1!8, Y1!9)) | (~![Z2: $i, W2: $i] : ((~big_p(Z2)) | (~big_r(X1!8, W2)) | (~big_r(W2, Z2))))))) <=> ((~((~big_p(a)) | big_p(X1!8) | (~![Z1: $i, W1: $i] : ((~big_p(Z1)) | (~big_r(X1!8, W1)) | (~big_r(W1, Z1)))))) | (~((~big_p(a)) | (~((~big_p(X!2)) | (~((~big_p(Y!3)) | (~big_r(X!2, Y!3)))))) | (~![Z: $i, W: $i] : ((~big_p(Z)) | (~big_r(X!2, W)) | (~big_r(W, Z)))))) | (~((~big_p(a)) | (~big_p(Y1!9)) | (~big_r(X1!8, Y1!9)) | (~![Z2: $i, W2: $i] : ((~big_p(Z2)) | (~big_r(X1!8, W2)) | (~big_r(W2, Z2)))))))),
% 0.62/0.77 inference(rewrite,[status(thm)],[])).
% 0.62/0.77 tff(16,plain,
% 0.62/0.77 ((big_p(a) & big_p(Y1!9) & big_r(X1!8, Y1!9) & ![Z2: $i, W2: $i] : ((~big_p(Z2)) | (~big_r(X1!8, W2)) | (~big_r(W2, Z2)))) <=> (~((~big_p(a)) | (~big_p(Y1!9)) | (~big_r(X1!8, Y1!9)) | (~![Z2: $i, W2: $i] : ((~big_p(Z2)) | (~big_r(X1!8, W2)) | (~big_r(W2, Z2))))))),
% 0.62/0.77 inference(rewrite,[status(thm)],[])).
% 0.62/0.77 tff(17,plain,
% 0.62/0.77 (^[Z2: $i, W2: $i] : trans(monotonicity(rewrite((big_p(Z2) & big_r(X1!8, W2) & big_r(W2, Z2)) <=> (~((~big_p(Z2)) | (~big_r(X1!8, W2)) | (~big_r(W2, Z2))))), ((~(big_p(Z2) & big_r(X1!8, W2) & big_r(W2, Z2))) <=> (~(~((~big_p(Z2)) | (~big_r(X1!8, W2)) | (~big_r(W2, Z2))))))), rewrite((~(~((~big_p(Z2)) | (~big_r(X1!8, W2)) | (~big_r(W2, Z2))))) <=> ((~big_p(Z2)) | (~big_r(X1!8, W2)) | (~big_r(W2, Z2)))), ((~(big_p(Z2) & big_r(X1!8, W2) & big_r(W2, Z2))) <=> ((~big_p(Z2)) | (~big_r(X1!8, W2)) | (~big_r(W2, Z2)))))),
% 0.62/0.77 inference(bind,[status(th)],[])).
% 0.62/0.77 tff(18,plain,
% 0.62/0.77 (![Z2: $i, W2: $i] : (~(big_p(Z2) & big_r(X1!8, W2) & big_r(W2, Z2))) <=> ![Z2: $i, W2: $i] : ((~big_p(Z2)) | (~big_r(X1!8, W2)) | (~big_r(W2, Z2)))),
% 0.62/0.77 inference(quant_intro,[status(thm)],[17])).
% 0.62/0.77 tff(19,plain,
% 0.62/0.77 ((big_p(a) & big_p(Y1!9) & big_r(X1!8, Y1!9) & ![Z2: $i, W2: $i] : (~(big_p(Z2) & big_r(X1!8, W2) & big_r(W2, Z2)))) <=> (big_p(a) & big_p(Y1!9) & big_r(X1!8, Y1!9) & ![Z2: $i, W2: $i] : ((~big_p(Z2)) | (~big_r(X1!8, W2)) | (~big_r(W2, Z2))))),
% 0.62/0.77 inference(monotonicity,[status(thm)],[18])).
% 0.62/0.77 tff(20,plain,
% 0.62/0.77 ((big_p(a) & big_p(Y1!9) & big_r(X1!8, Y1!9) & ![Z2: $i, W2: $i] : (~(big_p(Z2) & big_r(X1!8, W2) & big_r(W2, Z2)))) <=> (~((~big_p(a)) | (~big_p(Y1!9)) | (~big_r(X1!8, Y1!9)) | (~![Z2: $i, W2: $i] : ((~big_p(Z2)) | (~big_r(X1!8, W2)) | (~big_r(W2, Z2))))))),
% 0.62/0.77 inference(transitivity,[status(thm)],[19, 16])).
% 0.62/0.77 tff(21,plain,
% 0.62/0.77 ((big_p(a) & ((~big_p(X!2)) | (~((~big_p(Y!3)) | (~big_r(X!2, Y!3))))) & ![Z: $i, W: $i] : ((~big_p(Z)) | (~big_r(X!2, W)) | (~big_r(W, Z)))) <=> (~((~big_p(a)) | (~((~big_p(X!2)) | (~((~big_p(Y!3)) | (~big_r(X!2, Y!3)))))) | (~![Z: $i, W: $i] : ((~big_p(Z)) | (~big_r(X!2, W)) | (~big_r(W, Z))))))),
% 0.62/0.77 inference(rewrite,[status(thm)],[])).
% 0.62/0.77 tff(22,plain,
% 0.62/0.77 (^[Z: $i, W: $i] : trans(monotonicity(rewrite((big_p(Z) & big_r(X!2, W) & big_r(W, Z)) <=> (~((~big_p(Z)) | (~big_r(X!2, W)) | (~big_r(W, Z))))), ((~(big_p(Z) & big_r(X!2, W) & big_r(W, Z))) <=> (~(~((~big_p(Z)) | (~big_r(X!2, W)) | (~big_r(W, Z))))))), rewrite((~(~((~big_p(Z)) | (~big_r(X!2, W)) | (~big_r(W, Z))))) <=> ((~big_p(Z)) | (~big_r(X!2, W)) | (~big_r(W, Z)))), ((~(big_p(Z) & big_r(X!2, W) & big_r(W, Z))) <=> ((~big_p(Z)) | (~big_r(X!2, W)) | (~big_r(W, Z)))))),
% 0.62/0.77 inference(bind,[status(th)],[])).
% 0.62/0.77 tff(23,plain,
% 0.62/0.77 (![Z: $i, W: $i] : (~(big_p(Z) & big_r(X!2, W) & big_r(W, Z))) <=> ![Z: $i, W: $i] : ((~big_p(Z)) | (~big_r(X!2, W)) | (~big_r(W, Z)))),
% 0.62/0.77 inference(quant_intro,[status(thm)],[22])).
% 0.62/0.77 tff(24,plain,
% 0.62/0.77 (((~big_p(X!2)) | (big_p(Y!3) & big_r(X!2, Y!3))) <=> ((~big_p(X!2)) | (~((~big_p(Y!3)) | (~big_r(X!2, Y!3)))))),
% 0.62/0.77 inference(rewrite,[status(thm)],[])).
% 0.62/0.77 tff(25,plain,
% 0.62/0.77 ((big_p(a) & ((~big_p(X!2)) | (big_p(Y!3) & big_r(X!2, Y!3))) & ![Z: $i, W: $i] : (~(big_p(Z) & big_r(X!2, W) & big_r(W, Z)))) <=> (big_p(a) & ((~big_p(X!2)) | (~((~big_p(Y!3)) | (~big_r(X!2, Y!3))))) & ![Z: $i, W: $i] : ((~big_p(Z)) | (~big_r(X!2, W)) | (~big_r(W, Z))))),
% 0.62/0.77 inference(monotonicity,[status(thm)],[24, 23])).
% 0.62/0.77 tff(26,plain,
% 0.62/0.77 ((big_p(a) & ((~big_p(X!2)) | (big_p(Y!3) & big_r(X!2, Y!3))) & ![Z: $i, W: $i] : (~(big_p(Z) & big_r(X!2, W) & big_r(W, Z)))) <=> (~((~big_p(a)) | (~((~big_p(X!2)) | (~((~big_p(Y!3)) | (~big_r(X!2, Y!3)))))) | (~![Z: $i, W: $i] : ((~big_p(Z)) | (~big_r(X!2, W)) | (~big_r(W, Z))))))),
% 0.62/0.78 inference(transitivity,[status(thm)],[25, 21])).
% 0.62/0.78 tff(27,plain,
% 0.62/0.78 ((big_p(a) & (~big_p(X1!8)) & ![Z1: $i, W1: $i] : ((~big_p(Z1)) | (~big_r(X1!8, W1)) | (~big_r(W1, Z1)))) <=> (~((~big_p(a)) | big_p(X1!8) | (~![Z1: $i, W1: $i] : ((~big_p(Z1)) | (~big_r(X1!8, W1)) | (~big_r(W1, Z1))))))),
% 0.62/0.78 inference(rewrite,[status(thm)],[])).
% 0.62/0.78 tff(28,plain,
% 0.62/0.78 (^[Z1: $i, W1: $i] : trans(monotonicity(rewrite((big_p(Z1) & big_r(X1!8, W1) & big_r(W1, Z1)) <=> (~((~big_p(Z1)) | (~big_r(X1!8, W1)) | (~big_r(W1, Z1))))), ((~(big_p(Z1) & big_r(X1!8, W1) & big_r(W1, Z1))) <=> (~(~((~big_p(Z1)) | (~big_r(X1!8, W1)) | (~big_r(W1, Z1))))))), rewrite((~(~((~big_p(Z1)) | (~big_r(X1!8, W1)) | (~big_r(W1, Z1))))) <=> ((~big_p(Z1)) | (~big_r(X1!8, W1)) | (~big_r(W1, Z1)))), ((~(big_p(Z1) & big_r(X1!8, W1) & big_r(W1, Z1))) <=> ((~big_p(Z1)) | (~big_r(X1!8, W1)) | (~big_r(W1, Z1)))))),
% 0.62/0.78 inference(bind,[status(th)],[])).
% 0.62/0.78 tff(29,plain,
% 0.62/0.78 (![Z1: $i, W1: $i] : (~(big_p(Z1) & big_r(X1!8, W1) & big_r(W1, Z1))) <=> ![Z1: $i, W1: $i] : ((~big_p(Z1)) | (~big_r(X1!8, W1)) | (~big_r(W1, Z1)))),
% 0.62/0.78 inference(quant_intro,[status(thm)],[28])).
% 0.62/0.78 tff(30,plain,
% 0.62/0.78 ((big_p(a) & (~big_p(X1!8)) & ![Z1: $i, W1: $i] : (~(big_p(Z1) & big_r(X1!8, W1) & big_r(W1, Z1)))) <=> (big_p(a) & (~big_p(X1!8)) & ![Z1: $i, W1: $i] : ((~big_p(Z1)) | (~big_r(X1!8, W1)) | (~big_r(W1, Z1))))),
% 0.62/0.78 inference(monotonicity,[status(thm)],[29])).
% 0.62/0.78 tff(31,plain,
% 0.62/0.78 ((big_p(a) & (~big_p(X1!8)) & ![Z1: $i, W1: $i] : (~(big_p(Z1) & big_r(X1!8, W1) & big_r(W1, Z1)))) <=> (~((~big_p(a)) | big_p(X1!8) | (~![Z1: $i, W1: $i] : ((~big_p(Z1)) | (~big_r(X1!8, W1)) | (~big_r(W1, Z1))))))),
% 0.62/0.78 inference(transitivity,[status(thm)],[30, 27])).
% 0.62/0.78 tff(32,plain,
% 0.62/0.78 (((big_p(a) & (~big_p(X1!8)) & ![Z1: $i, W1: $i] : (~(big_p(Z1) & big_r(X1!8, W1) & big_r(W1, Z1)))) | (big_p(a) & ((~big_p(X!2)) | (big_p(Y!3) & big_r(X!2, Y!3))) & ![Z: $i, W: $i] : (~(big_p(Z) & big_r(X!2, W) & big_r(W, Z)))) | (big_p(a) & big_p(Y1!9) & big_r(X1!8, Y1!9) & ![Z2: $i, W2: $i] : (~(big_p(Z2) & big_r(X1!8, W2) & big_r(W2, Z2))))) <=> ((~((~big_p(a)) | big_p(X1!8) | (~![Z1: $i, W1: $i] : ((~big_p(Z1)) | (~big_r(X1!8, W1)) | (~big_r(W1, Z1)))))) | (~((~big_p(a)) | (~((~big_p(X!2)) | (~((~big_p(Y!3)) | (~big_r(X!2, Y!3)))))) | (~![Z: $i, W: $i] : ((~big_p(Z)) | (~big_r(X!2, W)) | (~big_r(W, Z)))))) | (~((~big_p(a)) | (~big_p(Y1!9)) | (~big_r(X1!8, Y1!9)) | (~![Z2: $i, W2: $i] : ((~big_p(Z2)) | (~big_r(X1!8, W2)) | (~big_r(W2, Z2)))))))),
% 0.62/0.78 inference(monotonicity,[status(thm)],[31, 26, 20])).
% 0.62/0.78 tff(33,plain,
% 0.62/0.78 (((big_p(a) & (~big_p(X1!8)) & ![Z1: $i, W1: $i] : (~(big_p(Z1) & big_r(X1!8, W1) & big_r(W1, Z1)))) | (big_p(a) & ((~big_p(X!2)) | (big_p(Y!3) & big_r(X!2, Y!3))) & ![Z: $i, W: $i] : (~(big_p(Z) & big_r(X!2, W) & big_r(W, Z)))) | (big_p(a) & big_p(Y1!9) & big_r(X1!8, Y1!9) & ![Z2: $i, W2: $i] : (~(big_p(Z2) & big_r(X1!8, W2) & big_r(W2, Z2))))) <=> ((~((~big_p(a)) | big_p(X1!8) | (~![Z1: $i, W1: $i] : ((~big_p(Z1)) | (~big_r(X1!8, W1)) | (~big_r(W1, Z1)))))) | (~((~big_p(a)) | (~((~big_p(X!2)) | (~((~big_p(Y!3)) | (~big_r(X!2, Y!3)))))) | (~![Z: $i, W: $i] : ((~big_p(Z)) | (~big_r(X!2, W)) | (~big_r(W, Z)))))) | (~((~big_p(a)) | (~big_p(Y1!9)) | (~big_r(X1!8, Y1!9)) | (~![Z2: $i, W2: $i] : ((~big_p(Z2)) | (~big_r(X1!8, W2)) | (~big_r(W2, Z2)))))))),
% 0.62/0.78 inference(transitivity,[status(thm)],[32, 15])).
% 0.62/0.78 tff(34,plain,
% 0.62/0.78 (((![X: $i] : (((~big_p(a)) | (big_p(X) & ![Y: $i] : (~(big_p(Y) & big_r(X, Y))))) | (big_p(tptp_fun_Z_1(X)) & big_r(X, tptp_fun_W_0(X)) & big_r(tptp_fun_W_0(X), tptp_fun_Z_1(X)))) | ![X1: $i] : (((~big_p(a)) | big_p(X1) | (big_p(tptp_fun_Z1_5(X1)) & big_r(X1, tptp_fun_W1_4(X1)) & big_r(tptp_fun_W1_4(X1), tptp_fun_Z1_5(X1)))) & ((~big_p(a)) | ![Y1: $i] : (~(big_p(Y1) & big_r(X1, Y1))) | (big_p(tptp_fun_Z2_7(X1)) & big_r(X1, tptp_fun_W2_6(X1)) & big_r(tptp_fun_W2_6(X1), tptp_fun_Z2_7(X1)))))) & (((big_p(a) & ((~big_p(X!2)) | (big_p(Y!3) & big_r(X!2, Y!3)))) & ![Z: $i, W: $i] : (~(big_p(Z) & big_r(X!2, W) & big_r(W, Z)))) | ((big_p(a) & (~big_p(X1!8)) & ![Z1: $i, W1: $i] : (~(big_p(Z1) & big_r(X1!8, W1) & big_r(W1, Z1)))) | (big_p(a) & (big_p(Y1!9) & big_r(X1!8, Y1!9)) & ![Z2: $i, W2: $i] : (~(big_p(Z2) & big_r(X1!8, W2) & big_r(W2, Z2))))))) <=> ((![X: $i] : ((~big_p(a)) | (big_p(X) & ![Y: $i] : (~(big_p(Y) & big_r(X, Y)))) | (big_p(tptp_fun_Z_1(X)) & big_r(X, tptp_fun_W_0(X)) & big_r(tptp_fun_W_0(X), tptp_fun_Z_1(X)))) | ![X1: $i] : (((~big_p(a)) | big_p(X1) | (big_p(tptp_fun_Z1_5(X1)) & big_r(X1, tptp_fun_W1_4(X1)) & big_r(tptp_fun_W1_4(X1), tptp_fun_Z1_5(X1)))) & ((~big_p(a)) | ![Y1: $i] : (~(big_p(Y1) & big_r(X1, Y1))) | (big_p(tptp_fun_Z2_7(X1)) & big_r(X1, tptp_fun_W2_6(X1)) & big_r(tptp_fun_W2_6(X1), tptp_fun_Z2_7(X1)))))) & ((big_p(a) & (~big_p(X1!8)) & ![Z1: $i, W1: $i] : (~(big_p(Z1) & big_r(X1!8, W1) & big_r(W1, Z1)))) | (big_p(a) & ((~big_p(X!2)) | (big_p(Y!3) & big_r(X!2, Y!3))) & ![Z: $i, W: $i] : (~(big_p(Z) & big_r(X!2, W) & big_r(W, Z)))) | (big_p(a) & big_p(Y1!9) & big_r(X1!8, Y1!9) & ![Z2: $i, W2: $i] : (~(big_p(Z2) & big_r(X1!8, W2) & big_r(W2, Z2))))))),
% 0.62/0.78 inference(rewrite,[status(thm)],[])).
% 0.62/0.78 tff(35,plain,
% 0.62/0.78 ((~(![X: $i] : ((~(big_p(a) & ((~big_p(X)) | ?[Y: $i] : (big_p(Y) & big_r(X, Y))))) | ?[Z: $i, W: $i] : (big_p(Z) & big_r(X, W) & big_r(W, Z))) <=> ![X1: $i] : (((~big_p(a)) | big_p(X1) | ?[Z1: $i, W1: $i] : (big_p(Z1) & big_r(X1, W1) & big_r(W1, Z1))) & ((~big_p(a)) | (~?[Y1: $i] : (big_p(Y1) & big_r(X1, Y1))) | ?[Z2: $i, W2: $i] : (big_p(Z2) & big_r(X1, W2) & big_r(W2, Z2)))))) <=> (~(![X: $i] : ((~(big_p(a) & ((~big_p(X)) | ?[Y: $i] : (big_p(Y) & big_r(X, Y))))) | ?[Z: $i, W: $i] : (big_p(Z) & big_r(X, W) & big_r(W, Z))) <=> ![X1: $i] : (((~big_p(a)) | big_p(X1) | ?[Z1: $i, W1: $i] : (big_p(Z1) & big_r(X1, W1) & big_r(W1, Z1))) & ((~big_p(a)) | (~?[Y1: $i] : (big_p(Y1) & big_r(X1, Y1))) | ?[Z2: $i, W2: $i] : (big_p(Z2) & big_r(X1, W2) & big_r(W2, Z2))))))),
% 0.62/0.78 inference(rewrite,[status(thm)],[])).
% 0.62/0.78 tff(36,plain,
% 0.62/0.78 ((![X: $i] : ((~(big_p(a) & ((~big_p(X)) | ?[Y: $i] : (big_p(Y) & big_r(X, Y))))) | ?[Z: $i, W: $i] : (big_p(Z) & big_r(X, W) & big_r(W, Z))) <=> ![X1: $i] : (((~big_p(a)) | big_p(X1) | ?[Z1: $i, W1: $i] : (big_p(Z1) & big_r(X1, W1) & big_r(W1, Z1))) & ((~big_p(a)) | (~?[Y1: $i] : (big_p(Y1) & big_r(X1, Y1))) | ?[Z2: $i, W2: $i] : (big_p(Z2) & big_r(X1, W2) & big_r(W2, Z2))))) <=> (![X: $i] : ((~(big_p(a) & ((~big_p(X)) | ?[Y: $i] : (big_p(Y) & big_r(X, Y))))) | ?[Z: $i, W: $i] : (big_p(Z) & big_r(X, W) & big_r(W, Z))) <=> ![X1: $i] : (((~big_p(a)) | big_p(X1) | ?[Z1: $i, W1: $i] : (big_p(Z1) & big_r(X1, W1) & big_r(W1, Z1))) & ((~big_p(a)) | (~?[Y1: $i] : (big_p(Y1) & big_r(X1, Y1))) | ?[Z2: $i, W2: $i] : (big_p(Z2) & big_r(X1, W2) & big_r(W2, Z2)))))),
% 0.62/0.78 inference(rewrite,[status(thm)],[])).
% 0.62/0.78 tff(37,plain,
% 0.62/0.78 ((~(![X: $i] : ((~(big_p(a) & ((~big_p(X)) | ?[Y: $i] : (big_p(Y) & big_r(X, Y))))) | ?[Z: $i, W: $i] : (big_p(Z) & big_r(X, W) & big_r(W, Z))) <=> ![X1: $i] : (((~big_p(a)) | big_p(X1) | ?[Z1: $i, W1: $i] : (big_p(Z1) & big_r(X1, W1) & big_r(W1, Z1))) & ((~big_p(a)) | (~?[Y1: $i] : (big_p(Y1) & big_r(X1, Y1))) | ?[Z2: $i, W2: $i] : (big_p(Z2) & big_r(X1, W2) & big_r(W2, Z2)))))) <=> (~(![X: $i] : ((~(big_p(a) & ((~big_p(X)) | ?[Y: $i] : (big_p(Y) & big_r(X, Y))))) | ?[Z: $i, W: $i] : (big_p(Z) & big_r(X, W) & big_r(W, Z))) <=> ![X1: $i] : (((~big_p(a)) | big_p(X1) | ?[Z1: $i, W1: $i] : (big_p(Z1) & big_r(X1, W1) & big_r(W1, Z1))) & ((~big_p(a)) | (~?[Y1: $i] : (big_p(Y1) & big_r(X1, Y1))) | ?[Z2: $i, W2: $i] : (big_p(Z2) & big_r(X1, W2) & big_r(W2, Z2))))))),
% 0.62/0.78 inference(monotonicity,[status(thm)],[36])).
% 0.62/0.78 tff(38,plain,
% 0.62/0.78 ((~(![X: $i] : ((~(big_p(a) & ((~big_p(X)) | ?[Y: $i] : (big_p(Y) & big_r(X, Y))))) | ?[Z: $i, W: $i] : (big_p(Z) & big_r(X, W) & big_r(W, Z))) <=> ![X1: $i] : (((~big_p(a)) | big_p(X1) | ?[Z1: $i, W1: $i] : (big_p(Z1) & big_r(X1, W1) & big_r(W1, Z1))) & ((~big_p(a)) | (~?[Y1: $i] : (big_p(Y1) & big_r(X1, Y1))) | ?[Z2: $i, W2: $i] : (big_p(Z2) & big_r(X1, W2) & big_r(W2, Z2)))))) <=> (~(![X: $i] : ((~(big_p(a) & ((~big_p(X)) | ?[Y: $i] : (big_p(Y) & big_r(X, Y))))) | ?[Z: $i, W: $i] : (big_p(Z) & big_r(X, W) & big_r(W, Z))) <=> ![X1: $i] : (((~big_p(a)) | big_p(X1) | ?[Z1: $i, W1: $i] : (big_p(Z1) & big_r(X1, W1) & big_r(W1, Z1))) & ((~big_p(a)) | (~?[Y1: $i] : (big_p(Y1) & big_r(X1, Y1))) | ?[Z2: $i, W2: $i] : (big_p(Z2) & big_r(X1, W2) & big_r(W2, Z2))))))),
% 0.62/0.78 inference(transitivity,[status(thm)],[37, 35])).
% 0.62/0.78 tff(39,plain,
% 0.62/0.78 ((![X: $i] : ((big_p(a) & (big_p(X) => ?[Y: $i] : (big_p(Y) & big_r(X, Y)))) => ?[Z: $i, W: $i] : ((big_p(Z) & big_r(X, W)) & big_r(W, Z))) <=> ![X1: $i] : ((((~big_p(a)) | big_p(X1)) | ?[Z1: $i, W1: $i] : ((big_p(Z1) & big_r(X1, W1)) & big_r(W1, Z1))) & (((~big_p(a)) | (~?[Y1: $i] : (big_p(Y1) & big_r(X1, Y1)))) | ?[Z2: $i, W2: $i] : ((big_p(Z2) & big_r(X1, W2)) & big_r(W2, Z2))))) <=> (![X: $i] : ((~(big_p(a) & ((~big_p(X)) | ?[Y: $i] : (big_p(Y) & big_r(X, Y))))) | ?[Z: $i, W: $i] : (big_p(Z) & big_r(X, W) & big_r(W, Z))) <=> ![X1: $i] : (((~big_p(a)) | big_p(X1) | ?[Z1: $i, W1: $i] : (big_p(Z1) & big_r(X1, W1) & big_r(W1, Z1))) & ((~big_p(a)) | (~?[Y1: $i] : (big_p(Y1) & big_r(X1, Y1))) | ?[Z2: $i, W2: $i] : (big_p(Z2) & big_r(X1, W2) & big_r(W2, Z2)))))),
% 0.62/0.78 inference(rewrite,[status(thm)],[])).
% 0.62/0.78 tff(40,plain,
% 0.62/0.78 ((~(![X: $i] : ((big_p(a) & (big_p(X) => ?[Y: $i] : (big_p(Y) & big_r(X, Y)))) => ?[Z: $i, W: $i] : ((big_p(Z) & big_r(X, W)) & big_r(W, Z))) <=> ![X1: $i] : ((((~big_p(a)) | big_p(X1)) | ?[Z1: $i, W1: $i] : ((big_p(Z1) & big_r(X1, W1)) & big_r(W1, Z1))) & (((~big_p(a)) | (~?[Y1: $i] : (big_p(Y1) & big_r(X1, Y1)))) | ?[Z2: $i, W2: $i] : ((big_p(Z2) & big_r(X1, W2)) & big_r(W2, Z2)))))) <=> (~(![X: $i] : ((~(big_p(a) & ((~big_p(X)) | ?[Y: $i] : (big_p(Y) & big_r(X, Y))))) | ?[Z: $i, W: $i] : (big_p(Z) & big_r(X, W) & big_r(W, Z))) <=> ![X1: $i] : (((~big_p(a)) | big_p(X1) | ?[Z1: $i, W1: $i] : (big_p(Z1) & big_r(X1, W1) & big_r(W1, Z1))) & ((~big_p(a)) | (~?[Y1: $i] : (big_p(Y1) & big_r(X1, Y1))) | ?[Z2: $i, W2: $i] : (big_p(Z2) & big_r(X1, W2) & big_r(W2, Z2))))))),
% 0.62/0.78 inference(monotonicity,[status(thm)],[39])).
% 0.62/0.78 tff(41,plain,
% 0.62/0.78 ((~(![X: $i] : ((big_p(a) & (big_p(X) => ?[Y: $i] : (big_p(Y) & big_r(X, Y)))) => ?[Z: $i, W: $i] : ((big_p(Z) & big_r(X, W)) & big_r(W, Z))) <=> ![X1: $i] : ((((~big_p(a)) | big_p(X1)) | ?[Z1: $i, W1: $i] : ((big_p(Z1) & big_r(X1, W1)) & big_r(W1, Z1))) & (((~big_p(a)) | (~?[Y1: $i] : (big_p(Y1) & big_r(X1, Y1)))) | ?[Z2: $i, W2: $i] : ((big_p(Z2) & big_r(X1, W2)) & big_r(W2, Z2)))))) <=> (~(![X: $i] : ((~(big_p(a) & ((~big_p(X)) | ?[Y: $i] : (big_p(Y) & big_r(X, Y))))) | ?[Z: $i, W: $i] : (big_p(Z) & big_r(X, W) & big_r(W, Z))) <=> ![X1: $i] : (((~big_p(a)) | big_p(X1) | ?[Z1: $i, W1: $i] : (big_p(Z1) & big_r(X1, W1) & big_r(W1, Z1))) & ((~big_p(a)) | (~?[Y1: $i] : (big_p(Y1) & big_r(X1, Y1))) | ?[Z2: $i, W2: $i] : (big_p(Z2) & big_r(X1, W2) & big_r(W2, Z2))))))),
% 0.62/0.78 inference(transitivity,[status(thm)],[40, 35])).
% 0.62/0.78 tff(42,axiom,(~(![X: $i] : ((big_p(a) & (big_p(X) => ?[Y: $i] : (big_p(Y) & big_r(X, Y)))) => ?[Z: $i, W: $i] : ((big_p(Z) & big_r(X, W)) & big_r(W, Z))) <=> ![X1: $i] : ((((~big_p(a)) | big_p(X1)) | ?[Z1: $i, W1: $i] : ((big_p(Z1) & big_r(X1, W1)) & big_r(W1, Z1))) & (((~big_p(a)) | (~?[Y1: $i] : (big_p(Y1) & big_r(X1, Y1)))) | ?[Z2: $i, W2: $i] : ((big_p(Z2) & big_r(X1, W2)) & big_r(W2, Z2)))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','pel38')).
% 0.62/0.78 tff(43,plain,
% 0.62/0.78 (~(![X: $i] : ((~(big_p(a) & ((~big_p(X)) | ?[Y: $i] : (big_p(Y) & big_r(X, Y))))) | ?[Z: $i, W: $i] : (big_p(Z) & big_r(X, W) & big_r(W, Z))) <=> ![X1: $i] : (((~big_p(a)) | big_p(X1) | ?[Z1: $i, W1: $i] : (big_p(Z1) & big_r(X1, W1) & big_r(W1, Z1))) & ((~big_p(a)) | (~?[Y1: $i] : (big_p(Y1) & big_r(X1, Y1))) | ?[Z2: $i, W2: $i] : (big_p(Z2) & big_r(X1, W2) & big_r(W2, Z2)))))),
% 0.62/0.78 inference(modus_ponens,[status(thm)],[42, 41])).
% 0.62/0.78 tff(44,plain,
% 0.62/0.78 (~(![X: $i] : ((~(big_p(a) & ((~big_p(X)) | ?[Y: $i] : (big_p(Y) & big_r(X, Y))))) | ?[Z: $i, W: $i] : (big_p(Z) & big_r(X, W) & big_r(W, Z))) <=> ![X1: $i] : (((~big_p(a)) | big_p(X1) | ?[Z1: $i, W1: $i] : (big_p(Z1) & big_r(X1, W1) & big_r(W1, Z1))) & ((~big_p(a)) | (~?[Y1: $i] : (big_p(Y1) & big_r(X1, Y1))) | ?[Z2: $i, W2: $i] : (big_p(Z2) & big_r(X1, W2) & big_r(W2, Z2)))))),
% 0.62/0.80 inference(modus_ponens,[status(thm)],[43, 38])).
% 0.62/0.80 tff(45,plain,
% 0.62/0.80 (~(![X: $i] : ((~(big_p(a) & ((~big_p(X)) | ?[Y: $i] : (big_p(Y) & big_r(X, Y))))) | ?[Z: $i, W: $i] : (big_p(Z) & big_r(X, W) & big_r(W, Z))) <=> ![X1: $i] : (((~big_p(a)) | big_p(X1) | ?[Z1: $i, W1: $i] : (big_p(Z1) & big_r(X1, W1) & big_r(W1, Z1))) & ((~big_p(a)) | (~?[Y1: $i] : (big_p(Y1) & big_r(X1, Y1))) | ?[Z2: $i, W2: $i] : (big_p(Z2) & big_r(X1, W2) & big_r(W2, Z2)))))),
% 0.62/0.80 inference(modus_ponens,[status(thm)],[44, 35])).
% 0.62/0.80 tff(46,plain,
% 0.62/0.80 (~(![X: $i] : ((~(big_p(a) & ((~big_p(X)) | ?[Y: $i] : (big_p(Y) & big_r(X, Y))))) | ?[Z: $i, W: $i] : (big_p(Z) & big_r(X, W) & big_r(W, Z))) <=> ![X1: $i] : (((~big_p(a)) | big_p(X1) | ?[Z1: $i, W1: $i] : (big_p(Z1) & big_r(X1, W1) & big_r(W1, Z1))) & ((~big_p(a)) | (~?[Y1: $i] : (big_p(Y1) & big_r(X1, Y1))) | ?[Z2: $i, W2: $i] : (big_p(Z2) & big_r(X1, W2) & big_r(W2, Z2)))))),
% 0.62/0.80 inference(modus_ponens,[status(thm)],[45, 38])).
% 0.62/0.80 unexpected number of arguments: (let ((a!1 (lambda ((X $i))
% 0.62/0.80 (let ((a!1 (refl (~ (not (big_p a)) (not (big_p a)))))
% 0.62/0.80 (a!2 (exists ((Y $i)) (and (big_p Y) (big_r X Y))))
% 0.62/0.80 (a!3 (forall ((Y $i)) (not (and (big_p Y) (big_r X Y)))))
% 0.62/0.80 (a!9 (exists ((Z $i) (W $i))
% 0.62/0.80 (and (big_p Z) (big_r X W) (big_r W Z))))
% 0.62/0.80 (a!10 (and (big_p (Z!1 X))
% 0.62/0.80 (big_r X (W!0 X))
% 0.62/0.80 (big_r (W!0 X) (Z!1 X)))))
% 0.62/0.80 (let ((a!4 (nnf-neg (proof-bind (lambda ((Y $i))
% 0.62/0.80 (let ((a!1 (~ (not (and (big_p Y)
% 0.62/0.80 (big_r X
% 0.62/0.80 Y)))
% 0.62/0.80 (not (and (big_p Y)
% 0.62/0.80 (big_r X
% 0.62/0.80 Y))))))
% 0.62/0.80 (refl a!1))))
% 0.62/0.80 (~ (not a!2) a!3)))
% 0.62/0.80 (a!5 (not (or (not (big_p X)) a!2)))
% 0.62/0.80 (a!7 (and (big_p a) (or (not (big_p X)) a!2)))
% 0.62/0.80 (a!11 (or (or (not (big_p a)) (and (big_p X) a!3)) a!10)))
% 0.62/0.80 (let ((a!6 (nnf-neg (refl (~ (big_p X) (big_p X)))
% 0.62/0.80 a!4
% 0.62/0.80 (~ a!5 (and (big_p X) a!3))))
% 0.62/0.80 (a!8 (~ (not a!7) (or (not (big_p a)) (and (big_p X) a!3)))))
% 0.62/0.80 (monotonicity (nnf-neg a!1 a!6 a!8)
% 0.62/0.80 (sk (~ a!9 a!10))
% 0.62/0.80 (~ (or (not a!7) a!9) a!11)))))))
% 0.62/0.80 (a!2 (forall ((X $i))
% 0.62/0.80 (let ((a!1 (exists ((Y $i)) (and (big_p Y) (big_r X Y))))
% 0.62/0.80 (a!3 (exists ((Z $i) (W $i))
% 0.62/0.80 (and (big_p Z) (big_r X W) (big_r W Z)))))
% 0.62/0.80 (let ((a!2 (and (big_p a) (or (not (big_p X)) a!1))))
% 0.62/0.80 (or (not a!2) a!3)))))
% 0.62/0.80 (a!3 (forall ((X $i))
% 0.62/0.80 (let ((a!1 (forall ((Y $i)) (not (and (big_p Y) (big_r X Y)))))
% 0.62/0.80 (a!2 (and (big_p (Z!1 X))
% 0.62/0.80 (big_r X (W!0 X))
% 0.62/0.80 (big_r (W!0 X) (Z!1 X)))))
% 0.62/0.80 (or (or (not (big_p a)) (and (big_p X) a!1)) a!2))))
% 0.62/0.80 (a!4 (exists ((Y $i)) (and (big_p Y) (big_r X!2 Y))))
% 0.62/0.80 (a!6 (exists ((Z $i) (W $i)) (and (big_p Z) (big_r X!2 W) (big_r W Z))))
% 0.62/0.80 (a!8 (refl (~ (not (big_p X!2)) (not (big_p X!2)))))
% 0.62/0.80 (a!10 (or (not (big_p X!2)) (and (big_p Y!3) (big_r X!2 Y!3))))
% 0.62/0.80 (a!14 (proof-bind (lambda ((Z $i) (W $i))
% 0.62/0.80 (let ((a!1 (not (and (big_p Z)
% 0.62/0.80 (big_r X!2 W)
% 0.62/0.80 (big_r W Z)))))
% 0.62/0.80 (refl (~ a!1 a!1))))))
% 0.62/0.80 (a!15 (forall ((Z $i) (W $i))
% 0.62/0.80 (not (and (big_p Z) (big_r X!2 W) (big_r W Z)))))
% 0.62/0.80 (a!19 (lambda ((X1 $i))
% 0.62/0.80 (let ((a!1 (refl (~ (not (big_p a)) (not (big_p a)))))
% 0.62/0.80 (a!2 (exists ((Z1 $i) (W1 $i))
% 0.62/0.80 (and (big_p Z1) (big_r X1 W1) (big_r W1 Z1))))
% 0.62/0.80 (a!3 (and (big_p (Z1!5 X1))
% 0.62/0.80 (big_r X1 (W1!4 X1))
% 0.62/0.80 (big_r (W1!4 X1) (Z1!5 X1))))
% 0.62/0.80 (a!6 (not (exists ((Y1 $i)) (and (big_p Y1) (big_r X1 Y1)))))
% 0.62/0.80 (a!7 (forall ((Y1 $i)) (not (and (big_p Y1) (big_r X1 Y1)))))
% 0.62/0.80 (a!9 (exists ((Z2 $i) (W2 $i))
% 0.62/0.80 (and (big_p Z2) (big_r X1 W2) (big_r W2 Z2))))
% 0.62/0.80 (a!10 (and (big_p (Z2!7 X1))
% 0.62/0.80 (big_r X1 (W2!6 X1))
% 0.62/0.80 (big_r (W2!6 X1) (Z2!7 X1)))))
% 0.62/0.80 (let ((a!4 (~ (or (not (big_p a)) (big_p X1) a!2)
% 0.62/0.80 (or (not (big_p a)) (big_p X1) a!3)))
% 0.62/0.80 (a!8 (nnf-neg (proof-bind (lambda ((Y1 $i))
% 0.62/0.80 (let ((a!1 (~ (not (and (big_p Y1)
% 0.62/0.80 (big_r X1
% 0.62/0.80 Y1)))
% 0.62/0.80 (not (and (big_p Y1)
% 0.62/0.80 (big_r X1
% 0.62/0.80 Y1))))))
% 0.62/0.80 (refl a!1))))
% 0.62/0.80 (~ a!6 a!7)))
% 0.62/0.80 (a!11 (~ (or (not (big_p a)) a!6 a!9)
% 0.62/0.80 (or (not (big_p a)) a!7 a!10)))
% 0.62/0.80 (a!12 (and (or (not (big_p a)) (big_p X1) a!2)
% 0.62/0.80 (or (not (big_p a)) a!6 a!9)))
% 0.62/0.80 (a!13 (and (or (not (big_p a)) (big_p X1) a!3)
% 0.62/0.80 (or (not (big_p a)) a!7 a!10))))
% 0.62/0.80 (let ((a!5 (monotonicity a!1
% 0.62/0.80 (refl (~ (big_p X1) (big_p X1)))
% 0.62/0.80 (sk (~ a!2 a!3))
% 0.62/0.80 a!4)))
% 0.62/0.80 (monotonicity a!5
% 0.62/0.80 (monotonicity a!1 a!8 (sk (~ a!9 a!10)) a!11)
% 0.62/0.80 (~ a!12 a!13)))))))
% 0.62/0.80 (a!20 (forall ((X1 $i))
% 0.62/0.80 (let ((a!1 (exists ((Z1 $i) (W1 $i))
% 0.62/0.80 (and (big_p Z1) (big_r X1 W1) (big_r W1 Z1))))
% 0.62/0.80 (a!2 (not (exists ((Y1 $i)) (and (big_p Y1) (big_r X1 Y1)))))
% 0.62/0.80 (a!3 (exists ((Z2 $i) (W2 $i))
% 0.62/0.80 (and (big_p Z2) (big_r X1 W2) (big_r W2 Z2)))))
% 0.62/0.80 (and (or (not (big_p a)) (big_p X1) a!1)
% 0.62/0.80 (or (not (big_p a)) a!2 a!3)))))
% 0.62/0.80 (a!21 (forall ((X1 $i))
% 0.62/0.80 (let ((a!1 (and (big_p (Z1!5 X1))
% 0.62/0.80 (big_r X1 (W1!4 X1))
% 0.62/0.80 (big_r (W1!4 X1) (Z1!5 X1))))
% 0.62/0.80 (a!2 (forall ((Y1 $i)) (not (and (big_p Y1) (big_r X1 Y1)))))
% 0.62/0.80 (a!3 (and (big_p (Z2!7 X1))
% 0.62/0.80 (big_r X1 (W2!6 X1))
% 0.62/0.80 (big_r (W2!6 X1) (Z2!7 X1)))))
% 0.62/0.80 (and (or (not (big_p a)) (big_p X1) a!1)
% 0.62/0.80 (or (not (big_p a)) a!2 a!3)))))
% 0.62/0.80 (a!22 (exists ((Z1 $i) (W1 $i))
% 0.62/0.80 (and (big_p Z1) (big_r X1!8 W1) (big_r W1 Z1))))
% 0.62/0.80 (a!23 (exists ((Y1 $i)) (and (big_p Y1) (big_r X1!8 Y1))))
% 0.62/0.80 (a!24 (exists ((Z2 $i) (W2 $i))
% 0.62/0.80 (and (big_p Z2) (big_r X1!8 W2) (big_r W2 Z2))))
% 0.62/0.80 (a!26 (refl (~ (not (big_p X1!8)) (not (big_p X1!8)))))
% 0.62/0.80 (a!27 (proof-bind (lambda ((Z1 $i) (W1 $i))
% 0.62/0.80 (let ((a!1 (not (and (big_p Z1)
% 0.62/0.80 (big_r X1!8 W1)
% 0.62/0.80 (big_r W1 Z1)))))
% 0.62/0.80 (refl (~ a!1 a!1))))))
% 0.62/0.80 (a!28 (forall ((Z1 $i) (W1 $i))
% 0.62/0.80 (not (and (big_p Z1) (big_r X1!8 W1) (big_r W1 Z1)))))
% 0.62/0.80 (a!34 (proof-bind (lambda ((Z2 $i) (W2 $i))
% 0.62/0.80 (let ((a!1 (not (and (big_p Z2)
% 0.62/0.80 (big_r X1!8 W2)
% 0.62/0.80 (big_r W2 Z2)))))
% 0.62/0.80 (refl (~ a!1 a!1))))))
% 0.62/0.80 (a!35 (forall ((Z2 $i) (W2 $i))
% 0.62/0.80 (not (and (big_p Z2) (big_r X1!8 W2) (big_r W2 Z2))))))
% 0.62/0.80 (let ((a!5 (and (big_p a) (or (not (big_p X!2)) a!4)))
% 0.62/0.80 (a!9 (sk (~ a!4 (and (big_p Y!3) (big_r X!2 Y!3)))))
% 0.62/0.80 (a!11 (~ (or (not (big_p X!2)) a!4) a!10))
% 0.62/0.80 (a!18 (~ (not a!2) (and (and (big_p a) a!10) a!15)))
% 0.62/0.80 (a!25 (and (or (not (big_p a)) (big_p X1!8) a!22)
% 0.62/0.80 (or (not (big_p a)) (not a!23) a!24)))
% 0.62/0.80 (a!29 (not (or (not (big_p a)) (big_p X1!8) a!22)))
% 0.62/0.80 (a!32 (sk (~ a!23 (and (big_p Y1!9) (big_r X1!8 Y1!9)))))
% 0.62/0.80 (a!36 (not (or (not (big_p a)) (not a!23) a!24)))
% 0.62/0.80 (a!37 (and (big_p a) (and (big_p Y1!9) (big_r X1!8 Y1!9)) a!35)))
% 0.62/0.80 (let ((a!7 (~ (not a!2) (not (or (not a!5) a!6))))
% 0.62/0.80 (a!12 (monotonicity (refl (~ (big_p a) (big_p a)))
% 0.62/0.80 (monotonicity a!8 a!9 a!11)
% 0.62/0.80 (~ a!5 (and (big_p a) a!10))))
% 0.62/0.80 (a!16 (~ (not (or (not a!5) a!6)) (and (and (big_p a) a!10) a!15)))
% 0.62/0.80 (a!30 (~ a!29 (and (big_p a) (not (big_p X1!8)) a!28)))
% 0.62/0.80 (a!33 (nnf-neg a!32
% 0.62/0.80 (~ (not (not a!23)) (and (big_p Y1!9) (big_r X1!8 Y1!9)))))
% 0.62/0.80 (a!39 (or (and (big_p a) (not (big_p X1!8)) a!28) a!37)))
% 0.62/0.80 (let ((a!13 (nnf-neg a!12 (~ (not (not a!5)) (and (big_p a) a!10))))
% 0.62/0.80 (a!31 (nnf-neg (refl (~ (big_p a) (big_p a)))
% 0.62/0.80 a!26
% 0.62/0.80 (nnf-neg a!27 (~ (not a!22) a!28))
% 0.62/0.80 a!30))
% 0.62/0.80 (a!38 (nnf-neg (refl (~ (big_p a) (big_p a)))
% 0.62/0.80 a!33
% 0.62/0.80 (nnf-neg a!34 (~ (not a!24) a!35))
% 0.62/0.80 (~ a!36 a!37)))
% 0.62/0.80 (a!41 (or (and (and (big_p a) a!10) a!15) a!39)))
% 0.62/0.80 (let ((a!17 (nnf-neg a!13 (nnf-neg a!14 (~ (not a!6) a!15)) a!16))
% 0.62/0.80 (a!40 (trans (sk (~ (not a!20) (not a!25)))
% 0.62/0.80 (nnf-neg a!31 a!38 (~ (not a!25) a!39))
% 0.62/0.80 (~ (not a!20) a!39))))
% 0.62/0.80 (nnf-neg (nnf-pos (proof-bind a!1) (~ a!2 a!3))
% 0.62/0.80 (trans (sk a!7) a!17 a!18)
% 0.62/0.80 (nnf-pos (proof-bind a!19) (~ a!20 a!21))
% 0.62/0.80 a!40
% 0.62/0.80 (~ (not (= a!2 a!20)) (and (or a!3 a!21) a!41))))))))
% 0.62/0.80 Proof display could not be completed: unexpected number of arguments
% 0.62/0.80 % E exiting
%------------------------------------------------------------------------------