%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : SEU281+1 : TPTP v9.0.0. Released v3.3.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n003.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sat Jun 21 05:27:28 AM UTC 2025
% Result : Theorem 0.20s 0.52s
% Output : Proof 0.39s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SEU281+1 : TPTP v9.0.0. Released v3.3.0.
% 0.07/0.12 % Command : run_E %s %d THM
% 0.13/0.34 % Computer : n003.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Fri Jun 20 06:35:09 EDT 2025
% 0.13/0.34 % CPUTime :
% 0.20/0.52 % SZS status Theorem
% 0.20/0.52 % SZS output start Proof
% 0.20/0.52 tff(tptp_fun_D_2_type, type, (
% 0.20/0.52 tptp_fun_D_2: $i > $i)).
% 0.20/0.52 tff(tptp_fun_C_8_type, type, (
% 0.20/0.52 tptp_fun_C_8: ( $i * $i ) > $i)).
% 0.20/0.52 tff(tptp_fun_A_1_type, type, (
% 0.20/0.52 tptp_fun_A_1: $i)).
% 0.20/0.52 tff(tptp_fun_B_0_type, type, (
% 0.20/0.52 tptp_fun_B_0: $i)).
% 0.20/0.52 tff(ordered_pair_type, type, (
% 0.20/0.52 ordered_pair: ( $i * $i ) > $i)).
% 0.20/0.52 tff(singleton_type, type, (
% 0.20/0.52 singleton: $i > $i)).
% 0.20/0.52 tff(tptp_fun_J_9_type, type, (
% 0.20/0.52 tptp_fun_J_9: ( $i * $i ) > $i)).
% 0.20/0.52 tff(in_type, type, (
% 0.20/0.52 in: ( $i * $i ) > $o)).
% 0.20/0.52 tff(cartesian_product2_type, type, (
% 0.20/0.52 cartesian_product2: ( $i * $i ) > $i)).
% 0.20/0.52 tff(tptp_fun_E_3_type, type, (
% 0.20/0.52 tptp_fun_E_3: $i > $i)).
% 0.20/0.52 tff(1,assumption,((~((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), tptp_fun_C_8(B!0, A!1))) | (~((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | (~in(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1), A!1)) | (~(ordered_pair(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1), singleton(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1))) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))))))) | (~((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), tptp_fun_C_8(B!0, A!1)) | ![J: $i] : ((~in(J, A!1)) | (~(ordered_pair(J, singleton(J)) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))))))), introduced(assumption)).
% 0.20/0.52 tff(2,plain,
% 0.20/0.52 (^[A: $i, B: $i, D: $i] : refl((~((~((~in(D, tptp_fun_C_8(B, A))) | (~((~in(D, cartesian_product2(A, B))) | (~(ordered_pair(tptp_fun_J_9(D, A), singleton(tptp_fun_J_9(D, A))) = D)) | (~in(tptp_fun_J_9(D, A), A)))))) | (~(in(D, tptp_fun_C_8(B, A)) | (~in(D, cartesian_product2(A, B))) | ![J: $i] : ((~(ordered_pair(J, singleton(J)) = D)) | (~in(J, A))))))) <=> (~((~((~in(D, tptp_fun_C_8(B, A))) | (~((~in(D, cartesian_product2(A, B))) | (~(ordered_pair(tptp_fun_J_9(D, A), singleton(tptp_fun_J_9(D, A))) = D)) | (~in(tptp_fun_J_9(D, A), A)))))) | (~(in(D, tptp_fun_C_8(B, A)) | (~in(D, cartesian_product2(A, B))) | ![J: $i] : ((~(ordered_pair(J, singleton(J)) = D)) | (~in(J, A))))))))),
% 0.20/0.52 inference(bind,[status(th)],[])).
% 0.20/0.52 tff(3,plain,
% 0.20/0.52 (![A: $i, B: $i, D: $i] : (~((~((~in(D, tptp_fun_C_8(B, A))) | (~((~in(D, cartesian_product2(A, B))) | (~(ordered_pair(tptp_fun_J_9(D, A), singleton(tptp_fun_J_9(D, A))) = D)) | (~in(tptp_fun_J_9(D, A), A)))))) | (~(in(D, tptp_fun_C_8(B, A)) | (~in(D, cartesian_product2(A, B))) | ![J: $i] : ((~(ordered_pair(J, singleton(J)) = D)) | (~in(J, A))))))) <=> ![A: $i, B: $i, D: $i] : (~((~((~in(D, tptp_fun_C_8(B, A))) | (~((~in(D, cartesian_product2(A, B))) | (~(ordered_pair(tptp_fun_J_9(D, A), singleton(tptp_fun_J_9(D, A))) = D)) | (~in(tptp_fun_J_9(D, A), A)))))) | (~(in(D, tptp_fun_C_8(B, A)) | (~in(D, cartesian_product2(A, B))) | ![J: $i] : ((~(ordered_pair(J, singleton(J)) = D)) | (~in(J, A)))))))),
% 0.20/0.52 inference(quant_intro,[status(thm)],[2])).
% 0.20/0.52 tff(4,plain,
% 0.20/0.52 (^[A: $i, B: $i, D: $i] : rewrite((~((~((~in(D, tptp_fun_C_8(B, A))) | (~((~in(D, cartesian_product2(A, B))) | (~(ordered_pair(tptp_fun_J_9(D, A), singleton(tptp_fun_J_9(D, A))) = D)) | (~in(tptp_fun_J_9(D, A), A)))))) | (~(in(D, tptp_fun_C_8(B, A)) | (~in(D, cartesian_product2(A, B))) | ![J: $i] : ((~(ordered_pair(J, singleton(J)) = D)) | (~in(J, A))))))) <=> (~((~((~in(D, tptp_fun_C_8(B, A))) | (~((~in(D, cartesian_product2(A, B))) | (~(ordered_pair(tptp_fun_J_9(D, A), singleton(tptp_fun_J_9(D, A))) = D)) | (~in(tptp_fun_J_9(D, A), A)))))) | (~(in(D, tptp_fun_C_8(B, A)) | (~in(D, cartesian_product2(A, B))) | ![J: $i] : ((~(ordered_pair(J, singleton(J)) = D)) | (~in(J, A))))))))),
% 0.20/0.52 inference(bind,[status(th)],[])).
% 0.20/0.52 tff(5,plain,
% 0.20/0.52 (![A: $i, B: $i, D: $i] : (~((~((~in(D, tptp_fun_C_8(B, A))) | (~((~in(D, cartesian_product2(A, B))) | (~(ordered_pair(tptp_fun_J_9(D, A), singleton(tptp_fun_J_9(D, A))) = D)) | (~in(tptp_fun_J_9(D, A), A)))))) | (~(in(D, tptp_fun_C_8(B, A)) | (~in(D, cartesian_product2(A, B))) | ![J: $i] : ((~(ordered_pair(J, singleton(J)) = D)) | (~in(J, A))))))) <=> ![A: $i, B: $i, D: $i] : (~((~((~in(D, tptp_fun_C_8(B, A))) | (~((~in(D, cartesian_product2(A, B))) | (~(ordered_pair(tptp_fun_J_9(D, A), singleton(tptp_fun_J_9(D, A))) = D)) | (~in(tptp_fun_J_9(D, A), A)))))) | (~(in(D, tptp_fun_C_8(B, A)) | (~in(D, cartesian_product2(A, B))) | ![J: $i] : ((~(ordered_pair(J, singleton(J)) = D)) | (~in(J, A)))))))),
% 0.20/0.53 inference(quant_intro,[status(thm)],[4])).
% 0.20/0.53 tff(6,plain,
% 0.20/0.53 (![A: $i, B: $i, D: $i] : (~((~((~in(D, tptp_fun_C_8(B, A))) | (~((~in(D, cartesian_product2(A, B))) | (~(ordered_pair(tptp_fun_J_9(D, A), singleton(tptp_fun_J_9(D, A))) = D)) | (~in(tptp_fun_J_9(D, A), A)))))) | (~(in(D, tptp_fun_C_8(B, A)) | (~in(D, cartesian_product2(A, B))) | ![J: $i] : ((~(ordered_pair(J, singleton(J)) = D)) | (~in(J, A))))))) <=> ![A: $i, B: $i, D: $i] : (~((~((~in(D, tptp_fun_C_8(B, A))) | (~((~in(D, cartesian_product2(A, B))) | (~(ordered_pair(tptp_fun_J_9(D, A), singleton(tptp_fun_J_9(D, A))) = D)) | (~in(tptp_fun_J_9(D, A), A)))))) | (~(in(D, tptp_fun_C_8(B, A)) | (~in(D, cartesian_product2(A, B))) | ![J: $i] : ((~(ordered_pair(J, singleton(J)) = D)) | (~in(J, A)))))))),
% 0.20/0.53 inference(transitivity,[status(thm)],[5, 3])).
% 0.20/0.53 tff(7,plain,
% 0.20/0.53 (^[A: $i, B: $i, D: $i] : trans(monotonicity(rewrite(((~in(D, tptp_fun_C_8(B, A))) | ((ordered_pair(tptp_fun_J_9(D, A), singleton(tptp_fun_J_9(D, A))) = D) & in(tptp_fun_J_9(D, A), A) & in(D, cartesian_product2(A, B)))) <=> ((~in(D, tptp_fun_C_8(B, A))) | (~((~in(D, cartesian_product2(A, B))) | (~(ordered_pair(tptp_fun_J_9(D, A), singleton(tptp_fun_J_9(D, A))) = D)) | (~in(tptp_fun_J_9(D, A), A)))))), trans(monotonicity(quant_intro(proof_bind(^[J: $i] : trans(monotonicity(rewrite(((ordered_pair(J, singleton(J)) = D) & in(J, A)) <=> (~((~(ordered_pair(J, singleton(J)) = D)) | (~in(J, A))))), ((~((ordered_pair(J, singleton(J)) = D) & in(J, A))) <=> (~(~((~(ordered_pair(J, singleton(J)) = D)) | (~in(J, A))))))), rewrite((~(~((~(ordered_pair(J, singleton(J)) = D)) | (~in(J, A))))) <=> ((~(ordered_pair(J, singleton(J)) = D)) | (~in(J, A)))), ((~((ordered_pair(J, singleton(J)) = D) & in(J, A))) <=> ((~(ordered_pair(J, singleton(J)) = D)) | (~in(J, A)))))), (![J: $i] : (~((ordered_pair(J, singleton(J)) = D) & in(J, A))) <=> ![J: $i] : ((~(ordered_pair(J, singleton(J)) = D)) | (~in(J, A))))), ((in(D, tptp_fun_C_8(B, A)) | ![J: $i] : (~((ordered_pair(J, singleton(J)) = D) & in(J, A))) | (~in(D, cartesian_product2(A, B)))) <=> (in(D, tptp_fun_C_8(B, A)) | ![J: $i] : ((~(ordered_pair(J, singleton(J)) = D)) | (~in(J, A))) | (~in(D, cartesian_product2(A, B)))))), rewrite((in(D, tptp_fun_C_8(B, A)) | ![J: $i] : ((~(ordered_pair(J, singleton(J)) = D)) | (~in(J, A))) | (~in(D, cartesian_product2(A, B)))) <=> (in(D, tptp_fun_C_8(B, A)) | (~in(D, cartesian_product2(A, B))) | ![J: $i] : ((~(ordered_pair(J, singleton(J)) = D)) | (~in(J, A))))), ((in(D, tptp_fun_C_8(B, A)) | ![J: $i] : (~((ordered_pair(J, singleton(J)) = D) & in(J, A))) | (~in(D, cartesian_product2(A, B)))) <=> (in(D, tptp_fun_C_8(B, A)) | (~in(D, cartesian_product2(A, B))) | ![J: $i] : ((~(ordered_pair(J, singleton(J)) = D)) | (~in(J, A)))))), ((((~in(D, tptp_fun_C_8(B, A))) | ((ordered_pair(tptp_fun_J_9(D, A), singleton(tptp_fun_J_9(D, A))) = D) & in(tptp_fun_J_9(D, A), A) & in(D, cartesian_product2(A, B)))) & (in(D, tptp_fun_C_8(B, A)) | ![J: $i] : (~((ordered_pair(J, singleton(J)) = D) & in(J, A))) | (~in(D, cartesian_product2(A, B))))) <=> (((~in(D, tptp_fun_C_8(B, A))) | (~((~in(D, cartesian_product2(A, B))) | (~(ordered_pair(tptp_fun_J_9(D, A), singleton(tptp_fun_J_9(D, A))) = D)) | (~in(tptp_fun_J_9(D, A), A))))) & (in(D, tptp_fun_C_8(B, A)) | (~in(D, cartesian_product2(A, B))) | ![J: $i] : ((~(ordered_pair(J, singleton(J)) = D)) | (~in(J, A))))))), rewrite((((~in(D, tptp_fun_C_8(B, A))) | (~((~in(D, cartesian_product2(A, B))) | (~(ordered_pair(tptp_fun_J_9(D, A), singleton(tptp_fun_J_9(D, A))) = D)) | (~in(tptp_fun_J_9(D, A), A))))) & (in(D, tptp_fun_C_8(B, A)) | (~in(D, cartesian_product2(A, B))) | ![J: $i] : ((~(ordered_pair(J, singleton(J)) = D)) | (~in(J, A))))) <=> (~((~((~in(D, tptp_fun_C_8(B, A))) | (~((~in(D, cartesian_product2(A, B))) | (~(ordered_pair(tptp_fun_J_9(D, A), singleton(tptp_fun_J_9(D, A))) = D)) | (~in(tptp_fun_J_9(D, A), A)))))) | (~(in(D, tptp_fun_C_8(B, A)) | (~in(D, cartesian_product2(A, B))) | ![J: $i] : ((~(ordered_pair(J, singleton(J)) = D)) | (~in(J, A)))))))), ((((~in(D, tptp_fun_C_8(B, A))) | ((ordered_pair(tptp_fun_J_9(D, A), singleton(tptp_fun_J_9(D, A))) = D) & in(tptp_fun_J_9(D, A), A) & in(D, cartesian_product2(A, B)))) & (in(D, tptp_fun_C_8(B, A)) | ![J: $i] : (~((ordered_pair(J, singleton(J)) = D) & in(J, A))) | (~in(D, cartesian_product2(A, B))))) <=> (~((~((~in(D, tptp_fun_C_8(B, A))) | (~((~in(D, cartesian_product2(A, B))) | (~(ordered_pair(tptp_fun_J_9(D, A), singleton(tptp_fun_J_9(D, A))) = D)) | (~in(tptp_fun_J_9(D, A), A)))))) | (~(in(D, tptp_fun_C_8(B, A)) | (~in(D, cartesian_product2(A, B))) | ![J: $i] : ((~(ordered_pair(J, singleton(J)) = D)) | (~in(J, A)))))))))),
% 0.20/0.53 inference(bind,[status(th)],[])).
% 0.20/0.53 tff(8,plain,
% 0.20/0.53 (![A: $i, B: $i, D: $i] : (((~in(D, tptp_fun_C_8(B, A))) | ((ordered_pair(tptp_fun_J_9(D, A), singleton(tptp_fun_J_9(D, A))) = D) & in(tptp_fun_J_9(D, A), A) & in(D, cartesian_product2(A, B)))) & (in(D, tptp_fun_C_8(B, A)) | ![J: $i] : (~((ordered_pair(J, singleton(J)) = D) & in(J, A))) | (~in(D, cartesian_product2(A, B))))) <=> ![A: $i, B: $i, D: $i] : (~((~((~in(D, tptp_fun_C_8(B, A))) | (~((~in(D, cartesian_product2(A, B))) | (~(ordered_pair(tptp_fun_J_9(D, A), singleton(tptp_fun_J_9(D, A))) = D)) | (~in(tptp_fun_J_9(D, A), A)))))) | (~(in(D, tptp_fun_C_8(B, A)) | (~in(D, cartesian_product2(A, B))) | ![J: $i] : ((~(ordered_pair(J, singleton(J)) = D)) | (~in(J, A)))))))),
% 0.20/0.53 inference(quant_intro,[status(thm)],[7])).
% 0.20/0.53 tff(9,plain,
% 0.20/0.53 (![A: $i, B: $i] : ![D: $i] : (((~in(D, tptp_fun_C_8(B, A))) | ((ordered_pair(tptp_fun_J_9(D, A), singleton(tptp_fun_J_9(D, A))) = D) & in(tptp_fun_J_9(D, A), A) & in(D, cartesian_product2(A, B)))) & (in(D, tptp_fun_C_8(B, A)) | ![J: $i] : (~((ordered_pair(J, singleton(J)) = D) & in(J, A))) | (~in(D, cartesian_product2(A, B))))) <=> ![A: $i, B: $i, D: $i] : (((~in(D, tptp_fun_C_8(B, A))) | ((ordered_pair(tptp_fun_J_9(D, A), singleton(tptp_fun_J_9(D, A))) = D) & in(tptp_fun_J_9(D, A), A) & in(D, cartesian_product2(A, B)))) & (in(D, tptp_fun_C_8(B, A)) | ![J: $i] : (~((ordered_pair(J, singleton(J)) = D) & in(J, A))) | (~in(D, cartesian_product2(A, B)))))),
% 0.20/0.53 inference(pull_quant,[status(thm)],[])).
% 0.20/0.53 tff(10,plain,
% 0.20/0.53 (^[A: $i, B: $i] : quant_intro(proof_bind(^[D: $i] : rewrite((((~in(D, tptp_fun_C_8(B, A))) | (((ordered_pair(tptp_fun_J_9(D, A), singleton(tptp_fun_J_9(D, A))) = D) & in(tptp_fun_J_9(D, A), A)) & in(D, cartesian_product2(A, B)))) & (in(D, tptp_fun_C_8(B, A)) | (![J: $i] : (~((ordered_pair(J, singleton(J)) = D) & in(J, A))) | (~in(D, cartesian_product2(A, B)))))) <=> (((~in(D, tptp_fun_C_8(B, A))) | ((ordered_pair(tptp_fun_J_9(D, A), singleton(tptp_fun_J_9(D, A))) = D) & in(tptp_fun_J_9(D, A), A) & in(D, cartesian_product2(A, B)))) & (in(D, tptp_fun_C_8(B, A)) | ![J: $i] : (~((ordered_pair(J, singleton(J)) = D) & in(J, A))) | (~in(D, cartesian_product2(A, B))))))), (![D: $i] : (((~in(D, tptp_fun_C_8(B, A))) | (((ordered_pair(tptp_fun_J_9(D, A), singleton(tptp_fun_J_9(D, A))) = D) & in(tptp_fun_J_9(D, A), A)) & in(D, cartesian_product2(A, B)))) & (in(D, tptp_fun_C_8(B, A)) | (![J: $i] : (~((ordered_pair(J, singleton(J)) = D) & in(J, A))) | (~in(D, cartesian_product2(A, B)))))) <=> ![D: $i] : (((~in(D, tptp_fun_C_8(B, A))) | ((ordered_pair(tptp_fun_J_9(D, A), singleton(tptp_fun_J_9(D, A))) = D) & in(tptp_fun_J_9(D, A), A) & in(D, cartesian_product2(A, B)))) & (in(D, tptp_fun_C_8(B, A)) | ![J: $i] : (~((ordered_pair(J, singleton(J)) = D) & in(J, A))) | (~in(D, cartesian_product2(A, B)))))))),
% 0.20/0.53 inference(bind,[status(th)],[])).
% 0.20/0.53 tff(11,plain,
% 0.20/0.53 (![A: $i, B: $i] : ![D: $i] : (((~in(D, tptp_fun_C_8(B, A))) | (((ordered_pair(tptp_fun_J_9(D, A), singleton(tptp_fun_J_9(D, A))) = D) & in(tptp_fun_J_9(D, A), A)) & in(D, cartesian_product2(A, B)))) & (in(D, tptp_fun_C_8(B, A)) | (![J: $i] : (~((ordered_pair(J, singleton(J)) = D) & in(J, A))) | (~in(D, cartesian_product2(A, B)))))) <=> ![A: $i, B: $i] : ![D: $i] : (((~in(D, tptp_fun_C_8(B, A))) | ((ordered_pair(tptp_fun_J_9(D, A), singleton(tptp_fun_J_9(D, A))) = D) & in(tptp_fun_J_9(D, A), A) & in(D, cartesian_product2(A, B)))) & (in(D, tptp_fun_C_8(B, A)) | ![J: $i] : (~((ordered_pair(J, singleton(J)) = D) & in(J, A))) | (~in(D, cartesian_product2(A, B)))))),
% 0.20/0.53 inference(quant_intro,[status(thm)],[10])).
% 0.20/0.53 tff(12,plain,
% 0.20/0.53 (![A: $i, B: $i] : ![D: $i] : (((~in(D, tptp_fun_C_8(B, A))) | (((ordered_pair(tptp_fun_J_9(D, A), singleton(tptp_fun_J_9(D, A))) = D) & in(tptp_fun_J_9(D, A), A)) & in(D, cartesian_product2(A, B)))) & (in(D, tptp_fun_C_8(B, A)) | (![J: $i] : (~((ordered_pair(J, singleton(J)) = D) & in(J, A))) | (~in(D, cartesian_product2(A, B)))))) <=> ![A: $i, B: $i, D: $i] : (((~in(D, tptp_fun_C_8(B, A))) | ((ordered_pair(tptp_fun_J_9(D, A), singleton(tptp_fun_J_9(D, A))) = D) & in(tptp_fun_J_9(D, A), A) & in(D, cartesian_product2(A, B)))) & (in(D, tptp_fun_C_8(B, A)) | ![J: $i] : (~((ordered_pair(J, singleton(J)) = D) & in(J, A))) | (~in(D, cartesian_product2(A, B)))))),
% 0.20/0.53 inference(transitivity,[status(thm)],[11, 9])).
% 0.20/0.53 tff(13,plain,
% 0.20/0.53 (![A: $i, B: $i] : ?[C: $i] : ![D: $i] : (in(D, C) <=> (?[J: $i] : ((ordered_pair(J, singleton(J)) = D) & in(J, A)) & in(D, cartesian_product2(A, B)))) <=> ![A: $i, B: $i] : ?[C: $i] : ![D: $i] : (in(D, C) <=> (?[J: $i] : ((ordered_pair(J, singleton(J)) = D) & in(J, A)) & in(D, cartesian_product2(A, B))))),
% 0.20/0.53 inference(rewrite,[status(thm)],[])).
% 0.20/0.53 tff(14,plain,
% 0.20/0.53 (^[A: $i, B: $i] : trans(monotonicity(trans(quant_intro(proof_bind(^[C: $i, D: $i, E: $i] : trans(monotonicity(trans(monotonicity(trans(monotonicity(rewrite(((C = D) & ?[F: $i, G: $i] : (((ordered_pair(F, G) = D) & in(F, A)) & (G = singleton(F)))) <=> ((C = D) & ?[F: $i] : ((ordered_pair(F, singleton(F)) = D) & in(F, A)))), ((((C = D) & ?[F: $i, G: $i] : (((ordered_pair(F, G) = D) & in(F, A)) & (G = singleton(F)))) & (C = E)) <=> (((C = D) & ?[F: $i] : ((ordered_pair(F, singleton(F)) = D) & in(F, A))) & (C = E)))), rewrite((((C = D) & ?[F: $i] : ((ordered_pair(F, singleton(F)) = D) & in(F, A))) & (C = E)) <=> ((C = D) & ?[F: $i] : ((ordered_pair(F, singleton(F)) = D) & in(F, A)) & (C = E))), ((((C = D) & ?[F: $i, G: $i] : (((ordered_pair(F, G) = D) & in(F, A)) & (G = singleton(F)))) & (C = E)) <=> ((C = D) & ?[F: $i] : ((ordered_pair(F, singleton(F)) = D) & in(F, A)) & (C = E)))), trans(quant_intro(proof_bind(^[H: $i, I: $i] : rewrite((((ordered_pair(H, I) = E) & in(H, A)) & (I = singleton(H))) <=> ((ordered_pair(H, I) = E) & in(H, A) & (I = singleton(H))))), (?[H: $i, I: $i] : (((ordered_pair(H, I) = E) & in(H, A)) & (I = singleton(H))) <=> ?[H: $i, I: $i] : ((ordered_pair(H, I) = E) & in(H, A) & (I = singleton(H))))), trans(der(?[H: $i, I: $i] : ((ordered_pair(H, I) = E) & in(H, A) & (I = singleton(H))) <=> ?[H: $i, I: $i] : ((ordered_pair(H, singleton(H)) = E) & in(H, A))), elim_unused(?[H: $i, I: $i] : ((ordered_pair(H, singleton(H)) = E) & in(H, A)) <=> ?[H: $i] : ((ordered_pair(H, singleton(H)) = E) & in(H, A))), (?[H: $i, I: $i] : ((ordered_pair(H, I) = E) & in(H, A) & (I = singleton(H))) <=> ?[H: $i] : ((ordered_pair(H, singleton(H)) = E) & in(H, A)))), (?[H: $i, I: $i] : (((ordered_pair(H, I) = E) & in(H, A)) & (I = singleton(H))) <=> ?[H: $i] : ((ordered_pair(H, singleton(H)) = E) & in(H, A)))), (((((C = D) & ?[F: $i, G: $i] : (((ordered_pair(F, G) = D) & in(F, A)) & (G = singleton(F)))) & (C = E)) & ?[H: $i, I: $i] : (((ordered_pair(H, I) = E) & in(H, A)) & (I = singleton(H)))) <=> (((C = D) & ?[F: $i] : ((ordered_pair(F, singleton(F)) = D) & in(F, A)) & (C = E)) & ?[H: $i] : ((ordered_pair(H, singleton(H)) = E) & in(H, A))))), rewrite((((C = D) & ?[F: $i] : ((ordered_pair(F, singleton(F)) = D) & in(F, A)) & (C = E)) & ?[H: $i] : ((ordered_pair(H, singleton(H)) = E) & in(H, A))) <=> ((C = D) & ?[F: $i] : ((ordered_pair(F, singleton(F)) = D) & in(F, A)) & (C = E) & ?[H: $i] : ((ordered_pair(H, singleton(H)) = E) & in(H, A)))), (((((C = D) & ?[F: $i, G: $i] : (((ordered_pair(F, G) = D) & in(F, A)) & (G = singleton(F)))) & (C = E)) & ?[H: $i, I: $i] : (((ordered_pair(H, I) = E) & in(H, A)) & (I = singleton(H)))) <=> ((C = D) & ?[F: $i] : ((ordered_pair(F, singleton(F)) = D) & in(F, A)) & (C = E) & ?[H: $i] : ((ordered_pair(H, singleton(H)) = E) & in(H, A))))), ((((((C = D) & ?[F: $i, G: $i] : (((ordered_pair(F, G) = D) & in(F, A)) & (G = singleton(F)))) & (C = E)) & ?[H: $i, I: $i] : (((ordered_pair(H, I) = E) & in(H, A)) & (I = singleton(H)))) => (D = E)) <=> (((C = D) & ?[F: $i] : ((ordered_pair(F, singleton(F)) = D) & in(F, A)) & (C = E) & ?[H: $i] : ((ordered_pair(H, singleton(H)) = E) & in(H, A))) => (D = E)))), rewrite((((C = D) & ?[F: $i] : ((ordered_pair(F, singleton(F)) = D) & in(F, A)) & (C = E) & ?[H: $i] : ((ordered_pair(H, singleton(H)) = E) & in(H, A))) => (D = E)) <=> ((~((C = D) & ?[F: $i] : ((ordered_pair(F, singleton(F)) = D) & in(F, A)) & (C = E) & ?[H: $i] : ((ordered_pair(H, singleton(H)) = E) & in(H, A)))) | (D = E))), ((((((C = D) & ?[F: $i, G: $i] : (((ordered_pair(F, G) = D) & in(F, A)) & (G = singleton(F)))) & (C = E)) & ?[H: $i, I: $i] : (((ordered_pair(H, I) = E) & in(H, A)) & (I = singleton(H)))) => (D = E)) <=> ((~((C = D) & ?[F: $i] : ((ordered_pair(F, singleton(F)) = D) & in(F, A)) & (C = E) & ?[H: $i] : ((ordered_pair(H, singleton(H)) = E) & in(H, A)))) | (D = E))))), (![C: $i, D: $i, E: $i] : (((((C = D) & ?[F: $i, G: $i] : (((ordered_pair(F, G) = D) & in(F, A)) & (G = singleton(F)))) & (C = E)) & ?[H: $i, I: $i] : (((ordered_pair(H, I) = E) & in(H, A)) & (I = singleton(H)))) => (D = E)) <=> ![C: $i, D: $i, E: $i] : ((~((C = D) & ?[F: $i] : ((ordered_pair(F, singleton(F)) = D) & in(F, A)) & (C = E) & ?[H: $i] : ((ordered_pair(H, singleton(H)) = E) & in(H, A)))) | (D = E)))), trans(trans(trans(der(![C: $i, D: $i, E: $i] : ((~((C = D) & ?[F: $i] : ((ordered_pair(F, singleton(F)) = D) & in(F, A)) & (C = E) & ?[H: $i] : ((ordered_pair(H, singleton(H)) = E) & in(H, A)))) | (D = E)) <=> ![C: $i, D: $i, E: $i] : ((D = E) | (~?[H: $i] : ((ordered_pair(H, singleton(H)) = E) & in(H, A))) | (~?[F: $i] : ((ordered_pair(F, singleton(F)) = D) & in(F, A))) | (~(D = E)))), der(![C: $i, D: $i, E: $i] : ((D = E) | (~?[H: $i] : ((ordered_pair(H, singleton(H)) = E) & in(H, A))) | (~?[F: $i] : ((ordered_pair(F, singleton(F)) = D) & in(F, A))) | (~(D = E))) <=> ![C: $i, D: $i, E: $i] : ((E = E) | (~?[H: $i] : ((ordered_pair(H, singleton(H)) = E) & in(H, A))) | (~?[F: $i] : ((ordered_pair(F, singleton(F)) = E) & in(F, A))))), (![C: $i, D: $i, E: $i] : ((~((C = D) & ?[F: $i] : ((ordered_pair(F, singleton(F)) = D) & in(F, A)) & (C = E) & ?[H: $i] : ((ordered_pair(H, singleton(H)) = E) & in(H, A)))) | (D = E)) <=> ![C: $i, D: $i, E: $i] : ((E = E) | (~?[H: $i] : ((ordered_pair(H, singleton(H)) = E) & in(H, A))) | (~?[F: $i] : ((ordered_pair(F, singleton(F)) = E) & in(F, A)))))), elim_unused(![C: $i, D: $i, E: $i] : ((E = E) | (~?[H: $i] : ((ordered_pair(H, singleton(H)) = E) & in(H, A))) | (~?[F: $i] : ((ordered_pair(F, singleton(F)) = E) & in(F, A)))) <=> ![E: $i] : ((E = E) | (~?[H: $i] : ((ordered_pair(H, singleton(H)) = E) & in(H, A))) | (~?[F: $i] : ((ordered_pair(F, singleton(F)) = E) & in(F, A))))), (![C: $i, D: $i, E: $i] : ((~((C = D) & ?[F: $i] : ((ordered_pair(F, singleton(F)) = D) & in(F, A)) & (C = E) & ?[H: $i] : ((ordered_pair(H, singleton(H)) = E) & in(H, A)))) | (D = E)) <=> ![E: $i] : ((E = E) | (~?[H: $i] : ((ordered_pair(H, singleton(H)) = E) & in(H, A))) | (~?[F: $i] : ((ordered_pair(F, singleton(F)) = E) & in(F, A)))))), trans(quant_intro(proof_bind(^[E: $i] : trans(monotonicity(rewrite((E = E) <=> $true), rewrite((~?[H: $i] : ((ordered_pair(H, singleton(H)) = E) & in(H, A))) <=> (~?[H: $i] : ((ordered_pair(H, singleton(H)) = E) & in(H, A)))), rewrite((~?[F: $i] : ((ordered_pair(F, singleton(F)) = E) & in(F, A))) <=> (~?[F: $i] : ((ordered_pair(F, singleton(F)) = E) & in(F, A)))), (((E = E) | (~?[H: $i] : ((ordered_pair(H, singleton(H)) = E) & in(H, A))) | (~?[F: $i] : ((ordered_pair(F, singleton(F)) = E) & in(F, A)))) <=> ($true | (~?[H: $i] : ((ordered_pair(H, singleton(H)) = E) & in(H, A))) | (~?[F: $i] : ((ordered_pair(F, singleton(F)) = E) & in(F, A)))))), rewrite(($true | (~?[H: $i] : ((ordered_pair(H, singleton(H)) = E) & in(H, A))) | (~?[F: $i] : ((ordered_pair(F, singleton(F)) = E) & in(F, A)))) <=> $true), (((E = E) | (~?[H: $i] : ((ordered_pair(H, singleton(H)) = E) & in(H, A))) | (~?[F: $i] : ((ordered_pair(F, singleton(F)) = E) & in(F, A)))) <=> $true))), (![E: $i] : ((E = E) | (~?[H: $i] : ((ordered_pair(H, singleton(H)) = E) & in(H, A))) | (~?[F: $i] : ((ordered_pair(F, singleton(F)) = E) & in(F, A)))) <=> ![E: $i] : $true)), elim_unused(![E: $i] : $true <=> $true), (![E: $i] : ((E = E) | (~?[H: $i] : ((ordered_pair(H, singleton(H)) = E) & in(H, A))) | (~?[F: $i] : ((ordered_pair(F, singleton(F)) = E) & in(F, A)))) <=> $true)), (![C: $i, D: $i, E: $i] : ((~((C = D) & ?[F: $i] : ((ordered_pair(F, singleton(F)) = D) & in(F, A)) & (C = E) & ?[H: $i] : ((ordered_pair(H, singleton(H)) = E) & in(H, A)))) | (D = E)) <=> $true)), (![C: $i, D: $i, E: $i] : (((((C = D) & ?[F: $i, G: $i] : (((ordered_pair(F, G) = D) & in(F, A)) & (G = singleton(F)))) & (C = E)) & ?[H: $i, I: $i] : (((ordered_pair(H, I) = E) & in(H, A)) & (I = singleton(H)))) => (D = E)) <=> $true)), quant_intro(proof_bind(^[C: $i] : quant_intro(proof_bind(^[D: $i] : rewrite((in(D, C) <=> ?[E: $i] : ((in(E, cartesian_product2(A, B)) & (E = D)) & ?[J: $i, K: $i] : (((ordered_pair(J, K) = D) & in(J, A)) & (K = singleton(J))))) <=> (in(D, C) <=> (?[J: $i] : ((ordered_pair(J, singleton(J)) = D) & in(J, A)) & in(D, cartesian_product2(A, B)))))), (![D: $i] : (in(D, C) <=> ?[E: $i] : ((in(E, cartesian_product2(A, B)) & (E = D)) & ?[J: $i, K: $i] : (((ordered_pair(J, K) = D) & in(J, A)) & (K = singleton(J))))) <=> ![D: $i] : (in(D, C) <=> (?[J: $i] : ((ordered_pair(J, singleton(J)) = D) & in(J, A)) & in(D, cartesian_product2(A, B))))))), (?[C: $i] : ![D: $i] : (in(D, C) <=> ?[E: $i] : ((in(E, cartesian_product2(A, B)) & (E = D)) & ?[J: $i, K: $i] : (((ordered_pair(J, K) = D) & in(J, A)) & (K = singleton(J))))) <=> ?[C: $i] : ![D: $i] : (in(D, C) <=> (?[J: $i] : ((ordered_pair(J, singleton(J)) = D) & in(J, A)) & in(D, cartesian_product2(A, B)))))), ((![C: $i, D: $i, E: $i] : (((((C = D) & ?[F: $i, G: $i] : (((ordered_pair(F, G) = D) & in(F, A)) & (G = singleton(F)))) & (C = E)) & ?[H: $i, I: $i] : (((ordered_pair(H, I) = E) & in(H, A)) & (I = singleton(H)))) => (D = E)) => ?[C: $i] : ![D: $i] : (in(D, C) <=> ?[E: $i] : ((in(E, cartesian_product2(A, B)) & (E = D)) & ?[J: $i, K: $i] : (((ordered_pair(J, K) = D) & in(J, A)) & (K = singleton(J)))))) <=> ($true => ?[C: $i] : ![D: $i] : (in(D, C) <=> (?[J: $i] : ((ordered_pair(J, singleton(J)) = D) & in(J, A)) & in(D, cartesian_product2(A, B))))))), rewrite(($true => ?[C: $i] : ![D: $i] : (in(D, C) <=> (?[J: $i] : ((ordered_pair(J, singleton(J)) = D) & in(J, A)) & in(D, cartesian_product2(A, B))))) <=> ?[C: $i] : ![D: $i] : (in(D, C) <=> (?[J: $i] : ((ordered_pair(J, singleton(J)) = D) & in(J, A)) & in(D, cartesian_product2(A, B))))), ((![C: $i, D: $i, E: $i] : (((((C = D) & ?[F: $i, G: $i] : (((ordered_pair(F, G) = D) & in(F, A)) & (G = singleton(F)))) & (C = E)) & ?[H: $i, I: $i] : (((ordered_pair(H, I) = E) & in(H, A)) & (I = singleton(H)))) => (D = E)) => ?[C: $i] : ![D: $i] : (in(D, C) <=> ?[E: $i] : ((in(E, cartesian_product2(A, B)) & (E = D)) & ?[J: $i, K: $i] : (((ordered_pair(J, K) = D) & in(J, A)) & (K = singleton(J)))))) <=> ?[C: $i] : ![D: $i] : (in(D, C) <=> (?[J: $i] : ((ordered_pair(J, singleton(J)) = D) & in(J, A)) & in(D, cartesian_product2(A, B))))))),
% 0.20/0.53 inference(bind,[status(th)],[])).
% 0.20/0.53 tff(15,plain,
% 0.20/0.53 (![A: $i, B: $i] : (![C: $i, D: $i, E: $i] : (((((C = D) & ?[F: $i, G: $i] : (((ordered_pair(F, G) = D) & in(F, A)) & (G = singleton(F)))) & (C = E)) & ?[H: $i, I: $i] : (((ordered_pair(H, I) = E) & in(H, A)) & (I = singleton(H)))) => (D = E)) => ?[C: $i] : ![D: $i] : (in(D, C) <=> ?[E: $i] : ((in(E, cartesian_product2(A, B)) & (E = D)) & ?[J: $i, K: $i] : (((ordered_pair(J, K) = D) & in(J, A)) & (K = singleton(J)))))) <=> ![A: $i, B: $i] : ?[C: $i] : ![D: $i] : (in(D, C) <=> (?[J: $i] : ((ordered_pair(J, singleton(J)) = D) & in(J, A)) & in(D, cartesian_product2(A, B))))),
% 0.20/0.53 inference(quant_intro,[status(thm)],[14])).
% 0.20/0.53 tff(16,axiom,(![A: $i, B: $i] : (![C: $i, D: $i, E: $i] : (((((C = D) & ?[F: $i, G: $i] : (((ordered_pair(F, G) = D) & in(F, A)) & (G = singleton(F)))) & (C = E)) & ?[H: $i, I: $i] : (((ordered_pair(H, I) = E) & in(H, A)) & (I = singleton(H)))) => (D = E)) => ?[C: $i] : ![D: $i] : (in(D, C) <=> ?[E: $i] : ((in(E, cartesian_product2(A, B)) & (E = D)) & ?[J: $i, K: $i] : (((ordered_pair(J, K) = D) & in(J, A)) & (K = singleton(J))))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','s1_tarski__e16_22__wellord2__2')).
% 0.20/0.53 tff(17,plain,
% 0.20/0.53 (![A: $i, B: $i] : ?[C: $i] : ![D: $i] : (in(D, C) <=> (?[J: $i] : ((ordered_pair(J, singleton(J)) = D) & in(J, A)) & in(D, cartesian_product2(A, B))))),
% 0.20/0.53 inference(modus_ponens,[status(thm)],[16, 15])).
% 0.20/0.53 tff(18,plain,
% 0.20/0.53 (![A: $i, B: $i] : ?[C: $i] : ![D: $i] : (in(D, C) <=> (?[J: $i] : ((ordered_pair(J, singleton(J)) = D) & in(J, A)) & in(D, cartesian_product2(A, B))))),
% 0.20/0.53 inference(modus_ponens,[status(thm)],[17, 13])).
% 0.20/0.53 tff(19,plain,(
% 0.20/0.53 ![A: $i, B: $i] : ![D: $i] : (((~in(D, tptp_fun_C_8(B, A))) | (((ordered_pair(tptp_fun_J_9(D, A), singleton(tptp_fun_J_9(D, A))) = D) & in(tptp_fun_J_9(D, A), A)) & in(D, cartesian_product2(A, B)))) & (in(D, tptp_fun_C_8(B, A)) | (![J: $i] : (~((ordered_pair(J, singleton(J)) = D) & in(J, A))) | (~in(D, cartesian_product2(A, B))))))),
% 0.20/0.53 inference(skolemize,[status(sab)],[18])).
% 0.20/0.53 tff(20,plain,
% 0.20/0.53 (![A: $i, B: $i, D: $i] : (((~in(D, tptp_fun_C_8(B, A))) | ((ordered_pair(tptp_fun_J_9(D, A), singleton(tptp_fun_J_9(D, A))) = D) & in(tptp_fun_J_9(D, A), A) & in(D, cartesian_product2(A, B)))) & (in(D, tptp_fun_C_8(B, A)) | ![J: $i] : (~((ordered_pair(J, singleton(J)) = D) & in(J, A))) | (~in(D, cartesian_product2(A, B)))))),
% 0.20/0.53 inference(modus_ponens,[status(thm)],[19, 12])).
% 0.20/0.53 tff(21,plain,
% 0.20/0.53 (![A: $i, B: $i, D: $i] : (~((~((~in(D, tptp_fun_C_8(B, A))) | (~((~in(D, cartesian_product2(A, B))) | (~(ordered_pair(tptp_fun_J_9(D, A), singleton(tptp_fun_J_9(D, A))) = D)) | (~in(tptp_fun_J_9(D, A), A)))))) | (~(in(D, tptp_fun_C_8(B, A)) | (~in(D, cartesian_product2(A, B))) | ![J: $i] : ((~(ordered_pair(J, singleton(J)) = D)) | (~in(J, A)))))))),
% 0.20/0.53 inference(modus_ponens,[status(thm)],[20, 8])).
% 0.20/0.53 tff(22,plain,
% 0.20/0.53 (![A: $i, B: $i, D: $i] : (~((~((~in(D, tptp_fun_C_8(B, A))) | (~((~in(D, cartesian_product2(A, B))) | (~(ordered_pair(tptp_fun_J_9(D, A), singleton(tptp_fun_J_9(D, A))) = D)) | (~in(tptp_fun_J_9(D, A), A)))))) | (~(in(D, tptp_fun_C_8(B, A)) | (~in(D, cartesian_product2(A, B))) | ![J: $i] : ((~(ordered_pair(J, singleton(J)) = D)) | (~in(J, A)))))))),
% 0.20/0.53 inference(modus_ponens,[status(thm)],[21, 6])).
% 0.20/0.53 tff(23,plain,
% 0.20/0.53 (((~![A: $i, B: $i, D: $i] : (~((~((~in(D, tptp_fun_C_8(B, A))) | (~((~in(D, cartesian_product2(A, B))) | (~(ordered_pair(tptp_fun_J_9(D, A), singleton(tptp_fun_J_9(D, A))) = D)) | (~in(tptp_fun_J_9(D, A), A)))))) | (~(in(D, tptp_fun_C_8(B, A)) | (~in(D, cartesian_product2(A, B))) | ![J: $i] : ((~(ordered_pair(J, singleton(J)) = D)) | (~in(J, A)))))))) | (~((~((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), tptp_fun_C_8(B!0, A!1))) | (~((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | (~in(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1), A!1)) | (~(ordered_pair(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1), singleton(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1))) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))))))) | (~((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), tptp_fun_C_8(B!0, A!1)) | ![J: $i] : ((~in(J, A!1)) | (~(ordered_pair(J, singleton(J)) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))))))))) <=> ((~![A: $i, B: $i, D: $i] : (~((~((~in(D, tptp_fun_C_8(B, A))) | (~((~in(D, cartesian_product2(A, B))) | (~(ordered_pair(tptp_fun_J_9(D, A), singleton(tptp_fun_J_9(D, A))) = D)) | (~in(tptp_fun_J_9(D, A), A)))))) | (~(in(D, tptp_fun_C_8(B, A)) | (~in(D, cartesian_product2(A, B))) | ![J: $i] : ((~(ordered_pair(J, singleton(J)) = D)) | (~in(J, A)))))))) | (~((~((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), tptp_fun_C_8(B!0, A!1))) | (~((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | (~in(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1), A!1)) | (~(ordered_pair(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1), singleton(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1))) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))))))) | (~((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), tptp_fun_C_8(B!0, A!1)) | ![J: $i] : ((~in(J, A!1)) | (~(ordered_pair(J, singleton(J)) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1))))))))))),
% 0.37/0.53 inference(rewrite,[status(thm)],[])).
% 0.37/0.53 tff(24,plain,
% 0.37/0.53 ((~((~((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), tptp_fun_C_8(B!0, A!1))) | (~((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | (~(ordered_pair(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1), singleton(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1))) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))) | (~in(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1), A!1)))))) | (~(in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), tptp_fun_C_8(B!0, A!1)) | (~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | ![J: $i] : ((~(ordered_pair(J, singleton(J)) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))) | (~in(J, A!1))))))) <=> (~((~((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), tptp_fun_C_8(B!0, A!1))) | (~((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | (~in(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1), A!1)) | (~(ordered_pair(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1), singleton(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1))) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))))))) | (~((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), tptp_fun_C_8(B!0, A!1)) | ![J: $i] : ((~in(J, A!1)) | (~(ordered_pair(J, singleton(J)) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))))))))),
% 0.37/0.53 inference(rewrite,[status(thm)],[])).
% 0.37/0.53 tff(25,plain,
% 0.37/0.53 (((~![A: $i, B: $i, D: $i] : (~((~((~in(D, tptp_fun_C_8(B, A))) | (~((~in(D, cartesian_product2(A, B))) | (~(ordered_pair(tptp_fun_J_9(D, A), singleton(tptp_fun_J_9(D, A))) = D)) | (~in(tptp_fun_J_9(D, A), A)))))) | (~(in(D, tptp_fun_C_8(B, A)) | (~in(D, cartesian_product2(A, B))) | ![J: $i] : ((~(ordered_pair(J, singleton(J)) = D)) | (~in(J, A)))))))) | (~((~((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), tptp_fun_C_8(B!0, A!1))) | (~((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | (~(ordered_pair(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1), singleton(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1))) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))) | (~in(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1), A!1)))))) | (~(in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), tptp_fun_C_8(B!0, A!1)) | (~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | ![J: $i] : ((~(ordered_pair(J, singleton(J)) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))) | (~in(J, A!1)))))))) <=> ((~![A: $i, B: $i, D: $i] : (~((~((~in(D, tptp_fun_C_8(B, A))) | (~((~in(D, cartesian_product2(A, B))) | (~(ordered_pair(tptp_fun_J_9(D, A), singleton(tptp_fun_J_9(D, A))) = D)) | (~in(tptp_fun_J_9(D, A), A)))))) | (~(in(D, tptp_fun_C_8(B, A)) | (~in(D, cartesian_product2(A, B))) | ![J: $i] : ((~(ordered_pair(J, singleton(J)) = D)) | (~in(J, A)))))))) | (~((~((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), tptp_fun_C_8(B!0, A!1))) | (~((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | (~in(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1), A!1)) | (~(ordered_pair(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1), singleton(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1))) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))))))) | (~((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), tptp_fun_C_8(B!0, A!1)) | ![J: $i] : ((~in(J, A!1)) | (~(ordered_pair(J, singleton(J)) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1))))))))))),
% 0.37/0.54 inference(monotonicity,[status(thm)],[24])).
% 0.37/0.54 tff(26,plain,
% 0.37/0.54 (((~![A: $i, B: $i, D: $i] : (~((~((~in(D, tptp_fun_C_8(B, A))) | (~((~in(D, cartesian_product2(A, B))) | (~(ordered_pair(tptp_fun_J_9(D, A), singleton(tptp_fun_J_9(D, A))) = D)) | (~in(tptp_fun_J_9(D, A), A)))))) | (~(in(D, tptp_fun_C_8(B, A)) | (~in(D, cartesian_product2(A, B))) | ![J: $i] : ((~(ordered_pair(J, singleton(J)) = D)) | (~in(J, A)))))))) | (~((~((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), tptp_fun_C_8(B!0, A!1))) | (~((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | (~(ordered_pair(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1), singleton(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1))) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))) | (~in(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1), A!1)))))) | (~(in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), tptp_fun_C_8(B!0, A!1)) | (~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | ![J: $i] : ((~(ordered_pair(J, singleton(J)) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))) | (~in(J, A!1)))))))) <=> ((~![A: $i, B: $i, D: $i] : (~((~((~in(D, tptp_fun_C_8(B, A))) | (~((~in(D, cartesian_product2(A, B))) | (~(ordered_pair(tptp_fun_J_9(D, A), singleton(tptp_fun_J_9(D, A))) = D)) | (~in(tptp_fun_J_9(D, A), A)))))) | (~(in(D, tptp_fun_C_8(B, A)) | (~in(D, cartesian_product2(A, B))) | ![J: $i] : ((~(ordered_pair(J, singleton(J)) = D)) | (~in(J, A)))))))) | (~((~((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), tptp_fun_C_8(B!0, A!1))) | (~((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | (~in(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1), A!1)) | (~(ordered_pair(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1), singleton(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1))) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))))))) | (~((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), tptp_fun_C_8(B!0, A!1)) | ![J: $i] : ((~in(J, A!1)) | (~(ordered_pair(J, singleton(J)) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1))))))))))),
% 0.37/0.54 inference(transitivity,[status(thm)],[25, 23])).
% 0.37/0.54 tff(27,plain,
% 0.37/0.54 ((~![A: $i, B: $i, D: $i] : (~((~((~in(D, tptp_fun_C_8(B, A))) | (~((~in(D, cartesian_product2(A, B))) | (~(ordered_pair(tptp_fun_J_9(D, A), singleton(tptp_fun_J_9(D, A))) = D)) | (~in(tptp_fun_J_9(D, A), A)))))) | (~(in(D, tptp_fun_C_8(B, A)) | (~in(D, cartesian_product2(A, B))) | ![J: $i] : ((~(ordered_pair(J, singleton(J)) = D)) | (~in(J, A)))))))) | (~((~((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), tptp_fun_C_8(B!0, A!1))) | (~((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | (~(ordered_pair(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1), singleton(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1))) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))) | (~in(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1), A!1)))))) | (~(in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), tptp_fun_C_8(B!0, A!1)) | (~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | ![J: $i] : ((~(ordered_pair(J, singleton(J)) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))) | (~in(J, A!1)))))))),
% 0.37/0.54 inference(quant_inst,[status(thm)],[])).
% 0.37/0.54 tff(28,plain,
% 0.37/0.54 ((~![A: $i, B: $i, D: $i] : (~((~((~in(D, tptp_fun_C_8(B, A))) | (~((~in(D, cartesian_product2(A, B))) | (~(ordered_pair(tptp_fun_J_9(D, A), singleton(tptp_fun_J_9(D, A))) = D)) | (~in(tptp_fun_J_9(D, A), A)))))) | (~(in(D, tptp_fun_C_8(B, A)) | (~in(D, cartesian_product2(A, B))) | ![J: $i] : ((~(ordered_pair(J, singleton(J)) = D)) | (~in(J, A)))))))) | (~((~((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), tptp_fun_C_8(B!0, A!1))) | (~((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | (~in(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1), A!1)) | (~(ordered_pair(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1), singleton(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1))) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))))))) | (~((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), tptp_fun_C_8(B!0, A!1)) | ![J: $i] : ((~in(J, A!1)) | (~(ordered_pair(J, singleton(J)) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))))))))),
% 0.37/0.54 inference(modus_ponens,[status(thm)],[27, 26])).
% 0.37/0.54 tff(29,plain,
% 0.37/0.54 ($false),
% 0.37/0.54 inference(unit_resolution,[status(thm)],[28, 22, 1])).
% 0.37/0.54 tff(30,plain,(~((~((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), tptp_fun_C_8(B!0, A!1))) | (~((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | (~in(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1), A!1)) | (~(ordered_pair(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1), singleton(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1))) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))))))) | (~((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), tptp_fun_C_8(B!0, A!1)) | ![J: $i] : ((~in(J, A!1)) | (~(ordered_pair(J, singleton(J)) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1))))))))), inference(lemma,lemma(discharge,[]))).
% 0.37/0.54 tff(31,plain,
% 0.37/0.54 (((~((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), tptp_fun_C_8(B!0, A!1))) | (~((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | (~in(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1), A!1)) | (~(ordered_pair(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1), singleton(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1))) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))))))) | (~((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), tptp_fun_C_8(B!0, A!1)) | ![J: $i] : ((~in(J, A!1)) | (~(ordered_pair(J, singleton(J)) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))))))) | ((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), tptp_fun_C_8(B!0, A!1))) | (~((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | (~in(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1), A!1)) | (~(ordered_pair(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1), singleton(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1))) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))))))),
% 0.37/0.54 inference(tautology,[status(thm)],[])).
% 0.37/0.54 tff(32,plain,
% 0.37/0.54 ((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), tptp_fun_C_8(B!0, A!1))) | (~((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | (~in(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1), A!1)) | (~(ordered_pair(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1), singleton(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1))) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1))))))),
% 0.37/0.54 inference(unit_resolution,[status(thm)],[31, 30])).
% 0.37/0.54 tff(33,plain,
% 0.37/0.54 (^[C: $i] : rewrite((~((~(in(tptp_fun_D_2(C), C) | (~((~in(tptp_fun_D_2(C), cartesian_product2(A!1, B!0))) | (~(ordered_pair(tptp_fun_E_3(C), singleton(tptp_fun_E_3(C))) = tptp_fun_D_2(C))) | (~in(tptp_fun_E_3(C), A!1)))))) | (~((~in(tptp_fun_D_2(C), C)) | (~in(tptp_fun_D_2(C), cartesian_product2(A!1, B!0))) | ![E: $i] : ((~(ordered_pair(E, singleton(E)) = tptp_fun_D_2(C))) | (~in(E, A!1))))))) <=> (~((~(in(tptp_fun_D_2(C), C) | (~((~in(tptp_fun_D_2(C), cartesian_product2(A!1, B!0))) | (~(ordered_pair(tptp_fun_E_3(C), singleton(tptp_fun_E_3(C))) = tptp_fun_D_2(C))) | (~in(tptp_fun_E_3(C), A!1)))))) | (~((~in(tptp_fun_D_2(C), C)) | (~in(tptp_fun_D_2(C), cartesian_product2(A!1, B!0))) | ![E: $i] : ((~(ordered_pair(E, singleton(E)) = tptp_fun_D_2(C))) | (~in(E, A!1))))))))),
% 0.37/0.54 inference(bind,[status(th)],[])).
% 0.37/0.54 tff(34,plain,
% 0.37/0.54 (![C: $i] : (~((~(in(tptp_fun_D_2(C), C) | (~((~in(tptp_fun_D_2(C), cartesian_product2(A!1, B!0))) | (~(ordered_pair(tptp_fun_E_3(C), singleton(tptp_fun_E_3(C))) = tptp_fun_D_2(C))) | (~in(tptp_fun_E_3(C), A!1)))))) | (~((~in(tptp_fun_D_2(C), C)) | (~in(tptp_fun_D_2(C), cartesian_product2(A!1, B!0))) | ![E: $i] : ((~(ordered_pair(E, singleton(E)) = tptp_fun_D_2(C))) | (~in(E, A!1))))))) <=> ![C: $i] : (~((~(in(tptp_fun_D_2(C), C) | (~((~in(tptp_fun_D_2(C), cartesian_product2(A!1, B!0))) | (~(ordered_pair(tptp_fun_E_3(C), singleton(tptp_fun_E_3(C))) = tptp_fun_D_2(C))) | (~in(tptp_fun_E_3(C), A!1)))))) | (~((~in(tptp_fun_D_2(C), C)) | (~in(tptp_fun_D_2(C), cartesian_product2(A!1, B!0))) | ![E: $i] : ((~(ordered_pair(E, singleton(E)) = tptp_fun_D_2(C))) | (~in(E, A!1)))))))),
% 0.37/0.54 inference(quant_intro,[status(thm)],[33])).
% 0.37/0.54 tff(35,plain,
% 0.37/0.54 (^[C: $i] : trans(monotonicity(trans(monotonicity(rewrite((in(tptp_fun_D_2(C), cartesian_product2(A!1, B!0)) & (ordered_pair(tptp_fun_E_3(C), singleton(tptp_fun_E_3(C))) = tptp_fun_D_2(C)) & in(tptp_fun_E_3(C), A!1)) <=> (~((~in(tptp_fun_D_2(C), cartesian_product2(A!1, B!0))) | (~(ordered_pair(tptp_fun_E_3(C), singleton(tptp_fun_E_3(C))) = tptp_fun_D_2(C))) | (~in(tptp_fun_E_3(C), A!1))))), ((in(tptp_fun_D_2(C), C) | (in(tptp_fun_D_2(C), cartesian_product2(A!1, B!0)) & (ordered_pair(tptp_fun_E_3(C), singleton(tptp_fun_E_3(C))) = tptp_fun_D_2(C)) & in(tptp_fun_E_3(C), A!1))) <=> (in(tptp_fun_D_2(C), C) | (~((~in(tptp_fun_D_2(C), cartesian_product2(A!1, B!0))) | (~(ordered_pair(tptp_fun_E_3(C), singleton(tptp_fun_E_3(C))) = tptp_fun_D_2(C))) | (~in(tptp_fun_E_3(C), A!1))))))), rewrite((in(tptp_fun_D_2(C), C) | (~((~in(tptp_fun_D_2(C), cartesian_product2(A!1, B!0))) | (~(ordered_pair(tptp_fun_E_3(C), singleton(tptp_fun_E_3(C))) = tptp_fun_D_2(C))) | (~in(tptp_fun_E_3(C), A!1))))) <=> (in(tptp_fun_D_2(C), C) | (~((~in(tptp_fun_D_2(C), cartesian_product2(A!1, B!0))) | (~(ordered_pair(tptp_fun_E_3(C), singleton(tptp_fun_E_3(C))) = tptp_fun_D_2(C))) | (~in(tptp_fun_E_3(C), A!1)))))), ((in(tptp_fun_D_2(C), C) | (in(tptp_fun_D_2(C), cartesian_product2(A!1, B!0)) & (ordered_pair(tptp_fun_E_3(C), singleton(tptp_fun_E_3(C))) = tptp_fun_D_2(C)) & in(tptp_fun_E_3(C), A!1))) <=> (in(tptp_fun_D_2(C), C) | (~((~in(tptp_fun_D_2(C), cartesian_product2(A!1, B!0))) | (~(ordered_pair(tptp_fun_E_3(C), singleton(tptp_fun_E_3(C))) = tptp_fun_D_2(C))) | (~in(tptp_fun_E_3(C), A!1))))))), trans(monotonicity(quant_intro(proof_bind(^[E: $i] : trans(monotonicity(rewrite(((ordered_pair(E, singleton(E)) = tptp_fun_D_2(C)) & in(E, A!1)) <=> (~((~(ordered_pair(E, singleton(E)) = tptp_fun_D_2(C))) | (~in(E, A!1))))), ((~((ordered_pair(E, singleton(E)) = tptp_fun_D_2(C)) & in(E, A!1))) <=> (~(~((~(ordered_pair(E, singleton(E)) = tptp_fun_D_2(C))) | (~in(E, A!1))))))), rewrite((~(~((~(ordered_pair(E, singleton(E)) = tptp_fun_D_2(C))) | (~in(E, A!1))))) <=> ((~(ordered_pair(E, singleton(E)) = tptp_fun_D_2(C))) | (~in(E, A!1)))), ((~((ordered_pair(E, singleton(E)) = tptp_fun_D_2(C)) & in(E, A!1))) <=> ((~(ordered_pair(E, singleton(E)) = tptp_fun_D_2(C))) | (~in(E, A!1)))))), (![E: $i] : (~((ordered_pair(E, singleton(E)) = tptp_fun_D_2(C)) & in(E, A!1))) <=> ![E: $i] : ((~(ordered_pair(E, singleton(E)) = tptp_fun_D_2(C))) | (~in(E, A!1))))), (((~in(tptp_fun_D_2(C), C)) | (~in(tptp_fun_D_2(C), cartesian_product2(A!1, B!0))) | ![E: $i] : (~((ordered_pair(E, singleton(E)) = tptp_fun_D_2(C)) & in(E, A!1)))) <=> ((~in(tptp_fun_D_2(C), C)) | (~in(tptp_fun_D_2(C), cartesian_product2(A!1, B!0))) | ![E: $i] : ((~(ordered_pair(E, singleton(E)) = tptp_fun_D_2(C))) | (~in(E, A!1)))))), rewrite(((~in(tptp_fun_D_2(C), C)) | (~in(tptp_fun_D_2(C), cartesian_product2(A!1, B!0))) | ![E: $i] : ((~(ordered_pair(E, singleton(E)) = tptp_fun_D_2(C))) | (~in(E, A!1)))) <=> ((~in(tptp_fun_D_2(C), C)) | (~in(tptp_fun_D_2(C), cartesian_product2(A!1, B!0))) | ![E: $i] : ((~(ordered_pair(E, singleton(E)) = tptp_fun_D_2(C))) | (~in(E, A!1))))), (((~in(tptp_fun_D_2(C), C)) | (~in(tptp_fun_D_2(C), cartesian_product2(A!1, B!0))) | ![E: $i] : (~((ordered_pair(E, singleton(E)) = tptp_fun_D_2(C)) & in(E, A!1)))) <=> ((~in(tptp_fun_D_2(C), C)) | (~in(tptp_fun_D_2(C), cartesian_product2(A!1, B!0))) | ![E: $i] : ((~(ordered_pair(E, singleton(E)) = tptp_fun_D_2(C))) | (~in(E, A!1)))))), (((in(tptp_fun_D_2(C), C) | (in(tptp_fun_D_2(C), cartesian_product2(A!1, B!0)) & (ordered_pair(tptp_fun_E_3(C), singleton(tptp_fun_E_3(C))) = tptp_fun_D_2(C)) & in(tptp_fun_E_3(C), A!1))) & ((~in(tptp_fun_D_2(C), C)) | (~in(tptp_fun_D_2(C), cartesian_product2(A!1, B!0))) | ![E: $i] : (~((ordered_pair(E, singleton(E)) = tptp_fun_D_2(C)) & in(E, A!1))))) <=> ((in(tptp_fun_D_2(C), C) | (~((~in(tptp_fun_D_2(C), cartesian_product2(A!1, B!0))) | (~(ordered_pair(tptp_fun_E_3(C), singleton(tptp_fun_E_3(C))) = tptp_fun_D_2(C))) | (~in(tptp_fun_E_3(C), A!1))))) & ((~in(tptp_fun_D_2(C), C)) | (~in(tptp_fun_D_2(C), cartesian_product2(A!1, B!0))) | ![E: $i] : ((~(ordered_pair(E, singleton(E)) = tptp_fun_D_2(C))) | (~in(E, A!1))))))), rewrite(((in(tptp_fun_D_2(C), C) | (~((~in(tptp_fun_D_2(C), cartesian_product2(A!1, B!0))) | (~(ordered_pair(tptp_fun_E_3(C), singleton(tptp_fun_E_3(C))) = tptp_fun_D_2(C))) | (~in(tptp_fun_E_3(C), A!1))))) & ((~in(tptp_fun_D_2(C), C)) | (~in(tptp_fun_D_2(C), cartesian_product2(A!1, B!0))) | ![E: $i] : ((~(ordered_pair(E, singleton(E)) = tptp_fun_D_2(C))) | (~in(E, A!1))))) <=> (~((~(in(tptp_fun_D_2(C), C) | (~((~in(tptp_fun_D_2(C), cartesian_product2(A!1, B!0))) | (~(ordered_pair(tptp_fun_E_3(C), singleton(tptp_fun_E_3(C))) = tptp_fun_D_2(C))) | (~in(tptp_fun_E_3(C), A!1)))))) | (~((~in(tptp_fun_D_2(C), C)) | (~in(tptp_fun_D_2(C), cartesian_product2(A!1, B!0))) | ![E: $i] : ((~(ordered_pair(E, singleton(E)) = tptp_fun_D_2(C))) | (~in(E, A!1)))))))), (((in(tptp_fun_D_2(C), C) | (in(tptp_fun_D_2(C), cartesian_product2(A!1, B!0)) & (ordered_pair(tptp_fun_E_3(C), singleton(tptp_fun_E_3(C))) = tptp_fun_D_2(C)) & in(tptp_fun_E_3(C), A!1))) & ((~in(tptp_fun_D_2(C), C)) | (~in(tptp_fun_D_2(C), cartesian_product2(A!1, B!0))) | ![E: $i] : (~((ordered_pair(E, singleton(E)) = tptp_fun_D_2(C)) & in(E, A!1))))) <=> (~((~(in(tptp_fun_D_2(C), C) | (~((~in(tptp_fun_D_2(C), cartesian_product2(A!1, B!0))) | (~(ordered_pair(tptp_fun_E_3(C), singleton(tptp_fun_E_3(C))) = tptp_fun_D_2(C))) | (~in(tptp_fun_E_3(C), A!1)))))) | (~((~in(tptp_fun_D_2(C), C)) | (~in(tptp_fun_D_2(C), cartesian_product2(A!1, B!0))) | ![E: $i] : ((~(ordered_pair(E, singleton(E)) = tptp_fun_D_2(C))) | (~in(E, A!1)))))))))),
% 0.37/0.54 inference(bind,[status(th)],[])).
% 0.37/0.54 tff(36,plain,
% 0.37/0.54 (![C: $i] : ((in(tptp_fun_D_2(C), C) | (in(tptp_fun_D_2(C), cartesian_product2(A!1, B!0)) & (ordered_pair(tptp_fun_E_3(C), singleton(tptp_fun_E_3(C))) = tptp_fun_D_2(C)) & in(tptp_fun_E_3(C), A!1))) & ((~in(tptp_fun_D_2(C), C)) | (~in(tptp_fun_D_2(C), cartesian_product2(A!1, B!0))) | ![E: $i] : (~((ordered_pair(E, singleton(E)) = tptp_fun_D_2(C)) & in(E, A!1))))) <=> ![C: $i] : (~((~(in(tptp_fun_D_2(C), C) | (~((~in(tptp_fun_D_2(C), cartesian_product2(A!1, B!0))) | (~(ordered_pair(tptp_fun_E_3(C), singleton(tptp_fun_E_3(C))) = tptp_fun_D_2(C))) | (~in(tptp_fun_E_3(C), A!1)))))) | (~((~in(tptp_fun_D_2(C), C)) | (~in(tptp_fun_D_2(C), cartesian_product2(A!1, B!0))) | ![E: $i] : ((~(ordered_pair(E, singleton(E)) = tptp_fun_D_2(C))) | (~in(E, A!1)))))))),
% 0.37/0.54 inference(quant_intro,[status(thm)],[35])).
% 0.37/0.54 tff(37,plain,
% 0.37/0.54 (^[C: $i] : rewrite(((in(tptp_fun_D_2(C), C) | (in(tptp_fun_D_2(C), cartesian_product2(A!1, B!0)) & ((ordered_pair(tptp_fun_E_3(C), singleton(tptp_fun_E_3(C))) = tptp_fun_D_2(C)) & in(tptp_fun_E_3(C), A!1)))) & ((~in(tptp_fun_D_2(C), C)) | ((~in(tptp_fun_D_2(C), cartesian_product2(A!1, B!0))) | ![E: $i] : (~((ordered_pair(E, singleton(E)) = tptp_fun_D_2(C)) & in(E, A!1)))))) <=> ((in(tptp_fun_D_2(C), C) | (in(tptp_fun_D_2(C), cartesian_product2(A!1, B!0)) & (ordered_pair(tptp_fun_E_3(C), singleton(tptp_fun_E_3(C))) = tptp_fun_D_2(C)) & in(tptp_fun_E_3(C), A!1))) & ((~in(tptp_fun_D_2(C), C)) | (~in(tptp_fun_D_2(C), cartesian_product2(A!1, B!0))) | ![E: $i] : (~((ordered_pair(E, singleton(E)) = tptp_fun_D_2(C)) & in(E, A!1))))))),
% 0.37/0.54 inference(bind,[status(th)],[])).
% 0.37/0.54 tff(38,plain,
% 0.37/0.54 (![C: $i] : ((in(tptp_fun_D_2(C), C) | (in(tptp_fun_D_2(C), cartesian_product2(A!1, B!0)) & ((ordered_pair(tptp_fun_E_3(C), singleton(tptp_fun_E_3(C))) = tptp_fun_D_2(C)) & in(tptp_fun_E_3(C), A!1)))) & ((~in(tptp_fun_D_2(C), C)) | ((~in(tptp_fun_D_2(C), cartesian_product2(A!1, B!0))) | ![E: $i] : (~((ordered_pair(E, singleton(E)) = tptp_fun_D_2(C)) & in(E, A!1)))))) <=> ![C: $i] : ((in(tptp_fun_D_2(C), C) | (in(tptp_fun_D_2(C), cartesian_product2(A!1, B!0)) & (ordered_pair(tptp_fun_E_3(C), singleton(tptp_fun_E_3(C))) = tptp_fun_D_2(C)) & in(tptp_fun_E_3(C), A!1))) & ((~in(tptp_fun_D_2(C), C)) | (~in(tptp_fun_D_2(C), cartesian_product2(A!1, B!0))) | ![E: $i] : (~((ordered_pair(E, singleton(E)) = tptp_fun_D_2(C)) & in(E, A!1)))))),
% 0.37/0.54 inference(quant_intro,[status(thm)],[37])).
% 0.37/0.54 tff(39,plain,
% 0.37/0.54 ((~![A: $i, B: $i] : ?[C: $i] : ![D: $i] : (in(D, C) <=> (in(D, cartesian_product2(A, B)) & ?[E: $i] : ((ordered_pair(E, singleton(E)) = D) & in(E, A))))) <=> (~![A: $i, B: $i] : ?[C: $i] : ![D: $i] : (in(D, C) <=> (in(D, cartesian_product2(A, B)) & ?[E: $i] : ((ordered_pair(E, singleton(E)) = D) & in(E, A)))))),
% 0.37/0.54 inference(rewrite,[status(thm)],[])).
% 0.37/0.54 tff(40,plain,
% 0.37/0.54 ((~![A: $i, B: $i] : ?[C: $i] : ![D: $i] : (in(D, C) <=> (in(D, cartesian_product2(A, B)) & ?[E: $i, F: $i] : (((ordered_pair(E, F) = D) & in(E, A)) & (F = singleton(E)))))) <=> (~![A: $i, B: $i] : ?[C: $i] : ![D: $i] : (in(D, C) <=> (in(D, cartesian_product2(A, B)) & ?[E: $i] : ((ordered_pair(E, singleton(E)) = D) & in(E, A)))))),
% 0.37/0.54 inference(rewrite,[status(thm)],[])).
% 0.37/0.54 tff(41,axiom,(~![A: $i, B: $i] : ?[C: $i] : ![D: $i] : (in(D, C) <=> (in(D, cartesian_product2(A, B)) & ?[E: $i, F: $i] : (((ordered_pair(E, F) = D) & in(E, A)) & (F = singleton(E)))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','s1_xboole_0__e16_22__wellord2__1')).
% 0.37/0.54 tff(42,plain,
% 0.37/0.54 (~![A: $i, B: $i] : ?[C: $i] : ![D: $i] : (in(D, C) <=> (in(D, cartesian_product2(A, B)) & ?[E: $i] : ((ordered_pair(E, singleton(E)) = D) & in(E, A))))),
% 0.37/0.54 inference(modus_ponens,[status(thm)],[41, 40])).
% 0.37/0.54 tff(43,plain,
% 0.37/0.54 (~![A: $i, B: $i] : ?[C: $i] : ![D: $i] : (in(D, C) <=> (in(D, cartesian_product2(A, B)) & ?[E: $i] : ((ordered_pair(E, singleton(E)) = D) & in(E, A))))),
% 0.37/0.54 inference(modus_ponens,[status(thm)],[42, 39])).
% 0.37/0.54 tff(44,plain,
% 0.37/0.54 (~![A: $i, B: $i] : ?[C: $i] : ![D: $i] : (in(D, C) <=> (in(D, cartesian_product2(A, B)) & ?[E: $i] : ((ordered_pair(E, singleton(E)) = D) & in(E, A))))),
% 0.37/0.54 inference(modus_ponens,[status(thm)],[43, 39])).
% 0.37/0.54 tff(45,plain,
% 0.37/0.54 (~![A: $i, B: $i] : ?[C: $i] : ![D: $i] : (in(D, C) <=> (in(D, cartesian_product2(A, B)) & ?[E: $i] : ((ordered_pair(E, singleton(E)) = D) & in(E, A))))),
% 0.37/0.54 inference(modus_ponens,[status(thm)],[44, 39])).
% 0.37/0.54 tff(46,plain,(
% 0.37/0.54 $oeq((~?[C: $i] : ![D: $i] : (in(D, C) <=> (in(D, cartesian_product2(A!1, B!0)) & ?[E: $i] : ((ordered_pair(E, singleton(E)) = D) & in(E, A!1))))), ![C: $i] : ((in(tptp_fun_D_2(C), C) | (in(tptp_fun_D_2(C), cartesian_product2(A!1, B!0)) & ((ordered_pair(tptp_fun_E_3(C), singleton(tptp_fun_E_3(C))) = tptp_fun_D_2(C)) & in(tptp_fun_E_3(C), A!1)))) & ((~in(tptp_fun_D_2(C), C)) | ((~in(tptp_fun_D_2(C), cartesian_product2(A!1, B!0))) | ![E: $i] : (~((ordered_pair(E, singleton(E)) = tptp_fun_D_2(C)) & in(E, A!1)))))))),
% 0.37/0.54 inference(transitivity,[status(sab)],[45])).
% 0.37/0.54 tff(47,plain,
% 0.37/0.54 (![C: $i] : ((in(tptp_fun_D_2(C), C) | (in(tptp_fun_D_2(C), cartesian_product2(A!1, B!0)) & (ordered_pair(tptp_fun_E_3(C), singleton(tptp_fun_E_3(C))) = tptp_fun_D_2(C)) & in(tptp_fun_E_3(C), A!1))) & ((~in(tptp_fun_D_2(C), C)) | (~in(tptp_fun_D_2(C), cartesian_product2(A!1, B!0))) | ![E: $i] : (~((ordered_pair(E, singleton(E)) = tptp_fun_D_2(C)) & in(E, A!1)))))),
% 0.37/0.54 inference(modus_ponens,[status(thm)],[46, 38])).
% 0.37/0.54 tff(48,plain,
% 0.37/0.54 (![C: $i] : (~((~(in(tptp_fun_D_2(C), C) | (~((~in(tptp_fun_D_2(C), cartesian_product2(A!1, B!0))) | (~(ordered_pair(tptp_fun_E_3(C), singleton(tptp_fun_E_3(C))) = tptp_fun_D_2(C))) | (~in(tptp_fun_E_3(C), A!1)))))) | (~((~in(tptp_fun_D_2(C), C)) | (~in(tptp_fun_D_2(C), cartesian_product2(A!1, B!0))) | ![E: $i] : ((~(ordered_pair(E, singleton(E)) = tptp_fun_D_2(C))) | (~in(E, A!1)))))))),
% 0.37/0.54 inference(modus_ponens,[status(thm)],[47, 36])).
% 0.37/0.54 tff(49,plain,
% 0.37/0.54 (![C: $i] : (~((~(in(tptp_fun_D_2(C), C) | (~((~in(tptp_fun_D_2(C), cartesian_product2(A!1, B!0))) | (~(ordered_pair(tptp_fun_E_3(C), singleton(tptp_fun_E_3(C))) = tptp_fun_D_2(C))) | (~in(tptp_fun_E_3(C), A!1)))))) | (~((~in(tptp_fun_D_2(C), C)) | (~in(tptp_fun_D_2(C), cartesian_product2(A!1, B!0))) | ![E: $i] : ((~(ordered_pair(E, singleton(E)) = tptp_fun_D_2(C))) | (~in(E, A!1)))))))),
% 0.37/0.54 inference(modus_ponens,[status(thm)],[48, 34])).
% 0.37/0.54 tff(50,plain,
% 0.37/0.54 (((~![C: $i] : (~((~(in(tptp_fun_D_2(C), C) | (~((~in(tptp_fun_D_2(C), cartesian_product2(A!1, B!0))) | (~(ordered_pair(tptp_fun_E_3(C), singleton(tptp_fun_E_3(C))) = tptp_fun_D_2(C))) | (~in(tptp_fun_E_3(C), A!1)))))) | (~((~in(tptp_fun_D_2(C), C)) | (~in(tptp_fun_D_2(C), cartesian_product2(A!1, B!0))) | ![E: $i] : ((~(ordered_pair(E, singleton(E)) = tptp_fun_D_2(C))) | (~in(E, A!1)))))))) | (~((~((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), tptp_fun_C_8(B!0, A!1))) | (~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | ![E: $i] : ((~in(E, A!1)) | (~(ordered_pair(E, singleton(E)) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1))))))) | (~(in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), tptp_fun_C_8(B!0, A!1)) | (~((~(ordered_pair(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)), singleton(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)))) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))) | (~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | (~in(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)), A!1))))))))) <=> ((~![C: $i] : (~((~(in(tptp_fun_D_2(C), C) | (~((~in(tptp_fun_D_2(C), cartesian_product2(A!1, B!0))) | (~(ordered_pair(tptp_fun_E_3(C), singleton(tptp_fun_E_3(C))) = tptp_fun_D_2(C))) | (~in(tptp_fun_E_3(C), A!1)))))) | (~((~in(tptp_fun_D_2(C), C)) | (~in(tptp_fun_D_2(C), cartesian_product2(A!1, B!0))) | ![E: $i] : ((~(ordered_pair(E, singleton(E)) = tptp_fun_D_2(C))) | (~in(E, A!1)))))))) | (~((~((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), tptp_fun_C_8(B!0, A!1))) | (~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | ![E: $i] : ((~in(E, A!1)) | (~(ordered_pair(E, singleton(E)) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1))))))) | (~(in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), tptp_fun_C_8(B!0, A!1)) | (~((~(ordered_pair(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)), singleton(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)))) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))) | (~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | (~in(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)), A!1)))))))))),
% 0.37/0.54 inference(rewrite,[status(thm)],[])).
% 0.37/0.54 tff(51,plain,
% 0.37/0.54 ((~((~(in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), tptp_fun_C_8(B!0, A!1)) | (~((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | (~(ordered_pair(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)), singleton(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)))) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))) | (~in(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)), A!1)))))) | (~((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), tptp_fun_C_8(B!0, A!1))) | (~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | ![E: $i] : ((~(ordered_pair(E, singleton(E)) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))) | (~in(E, A!1))))))) <=> (~((~((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), tptp_fun_C_8(B!0, A!1))) | (~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | ![E: $i] : ((~in(E, A!1)) | (~(ordered_pair(E, singleton(E)) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1))))))) | (~(in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), tptp_fun_C_8(B!0, A!1)) | (~((~(ordered_pair(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)), singleton(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)))) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))) | (~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | (~in(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)), A!1))))))))),
% 0.37/0.54 inference(rewrite,[status(thm)],[])).
% 0.37/0.54 tff(52,plain,
% 0.37/0.54 (((~![C: $i] : (~((~(in(tptp_fun_D_2(C), C) | (~((~in(tptp_fun_D_2(C), cartesian_product2(A!1, B!0))) | (~(ordered_pair(tptp_fun_E_3(C), singleton(tptp_fun_E_3(C))) = tptp_fun_D_2(C))) | (~in(tptp_fun_E_3(C), A!1)))))) | (~((~in(tptp_fun_D_2(C), C)) | (~in(tptp_fun_D_2(C), cartesian_product2(A!1, B!0))) | ![E: $i] : ((~(ordered_pair(E, singleton(E)) = tptp_fun_D_2(C))) | (~in(E, A!1)))))))) | (~((~(in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), tptp_fun_C_8(B!0, A!1)) | (~((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | (~(ordered_pair(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)), singleton(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)))) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))) | (~in(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)), A!1)))))) | (~((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), tptp_fun_C_8(B!0, A!1))) | (~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | ![E: $i] : ((~(ordered_pair(E, singleton(E)) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))) | (~in(E, A!1)))))))) <=> ((~![C: $i] : (~((~(in(tptp_fun_D_2(C), C) | (~((~in(tptp_fun_D_2(C), cartesian_product2(A!1, B!0))) | (~(ordered_pair(tptp_fun_E_3(C), singleton(tptp_fun_E_3(C))) = tptp_fun_D_2(C))) | (~in(tptp_fun_E_3(C), A!1)))))) | (~((~in(tptp_fun_D_2(C), C)) | (~in(tptp_fun_D_2(C), cartesian_product2(A!1, B!0))) | ![E: $i] : ((~(ordered_pair(E, singleton(E)) = tptp_fun_D_2(C))) | (~in(E, A!1)))))))) | (~((~((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), tptp_fun_C_8(B!0, A!1))) | (~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | ![E: $i] : ((~in(E, A!1)) | (~(ordered_pair(E, singleton(E)) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1))))))) | (~(in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), tptp_fun_C_8(B!0, A!1)) | (~((~(ordered_pair(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)), singleton(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)))) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))) | (~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | (~in(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)), A!1)))))))))),
% 0.37/0.54 inference(monotonicity,[status(thm)],[51])).
% 0.37/0.54 tff(53,plain,
% 0.37/0.54 (((~![C: $i] : (~((~(in(tptp_fun_D_2(C), C) | (~((~in(tptp_fun_D_2(C), cartesian_product2(A!1, B!0))) | (~(ordered_pair(tptp_fun_E_3(C), singleton(tptp_fun_E_3(C))) = tptp_fun_D_2(C))) | (~in(tptp_fun_E_3(C), A!1)))))) | (~((~in(tptp_fun_D_2(C), C)) | (~in(tptp_fun_D_2(C), cartesian_product2(A!1, B!0))) | ![E: $i] : ((~(ordered_pair(E, singleton(E)) = tptp_fun_D_2(C))) | (~in(E, A!1)))))))) | (~((~(in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), tptp_fun_C_8(B!0, A!1)) | (~((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | (~(ordered_pair(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)), singleton(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)))) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))) | (~in(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)), A!1)))))) | (~((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), tptp_fun_C_8(B!0, A!1))) | (~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | ![E: $i] : ((~(ordered_pair(E, singleton(E)) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))) | (~in(E, A!1)))))))) <=> ((~![C: $i] : (~((~(in(tptp_fun_D_2(C), C) | (~((~in(tptp_fun_D_2(C), cartesian_product2(A!1, B!0))) | (~(ordered_pair(tptp_fun_E_3(C), singleton(tptp_fun_E_3(C))) = tptp_fun_D_2(C))) | (~in(tptp_fun_E_3(C), A!1)))))) | (~((~in(tptp_fun_D_2(C), C)) | (~in(tptp_fun_D_2(C), cartesian_product2(A!1, B!0))) | ![E: $i] : ((~(ordered_pair(E, singleton(E)) = tptp_fun_D_2(C))) | (~in(E, A!1)))))))) | (~((~((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), tptp_fun_C_8(B!0, A!1))) | (~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | ![E: $i] : ((~in(E, A!1)) | (~(ordered_pair(E, singleton(E)) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1))))))) | (~(in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), tptp_fun_C_8(B!0, A!1)) | (~((~(ordered_pair(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)), singleton(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)))) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))) | (~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | (~in(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)), A!1)))))))))),
% 0.37/0.54 inference(transitivity,[status(thm)],[52, 50])).
% 0.37/0.54 tff(54,plain,
% 0.37/0.54 ((~![C: $i] : (~((~(in(tptp_fun_D_2(C), C) | (~((~in(tptp_fun_D_2(C), cartesian_product2(A!1, B!0))) | (~(ordered_pair(tptp_fun_E_3(C), singleton(tptp_fun_E_3(C))) = tptp_fun_D_2(C))) | (~in(tptp_fun_E_3(C), A!1)))))) | (~((~in(tptp_fun_D_2(C), C)) | (~in(tptp_fun_D_2(C), cartesian_product2(A!1, B!0))) | ![E: $i] : ((~(ordered_pair(E, singleton(E)) = tptp_fun_D_2(C))) | (~in(E, A!1)))))))) | (~((~(in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), tptp_fun_C_8(B!0, A!1)) | (~((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | (~(ordered_pair(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)), singleton(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)))) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))) | (~in(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)), A!1)))))) | (~((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), tptp_fun_C_8(B!0, A!1))) | (~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | ![E: $i] : ((~(ordered_pair(E, singleton(E)) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))) | (~in(E, A!1)))))))),
% 0.37/0.55 inference(quant_inst,[status(thm)],[])).
% 0.37/0.55 tff(55,plain,
% 0.37/0.55 ((~![C: $i] : (~((~(in(tptp_fun_D_2(C), C) | (~((~in(tptp_fun_D_2(C), cartesian_product2(A!1, B!0))) | (~(ordered_pair(tptp_fun_E_3(C), singleton(tptp_fun_E_3(C))) = tptp_fun_D_2(C))) | (~in(tptp_fun_E_3(C), A!1)))))) | (~((~in(tptp_fun_D_2(C), C)) | (~in(tptp_fun_D_2(C), cartesian_product2(A!1, B!0))) | ![E: $i] : ((~(ordered_pair(E, singleton(E)) = tptp_fun_D_2(C))) | (~in(E, A!1)))))))) | (~((~((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), tptp_fun_C_8(B!0, A!1))) | (~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | ![E: $i] : ((~in(E, A!1)) | (~(ordered_pair(E, singleton(E)) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1))))))) | (~(in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), tptp_fun_C_8(B!0, A!1)) | (~((~(ordered_pair(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)), singleton(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)))) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))) | (~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | (~in(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)), A!1))))))))),
% 0.37/0.55 inference(modus_ponens,[status(thm)],[54, 53])).
% 0.37/0.55 tff(56,plain,
% 0.37/0.55 (~((~((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), tptp_fun_C_8(B!0, A!1))) | (~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | ![E: $i] : ((~in(E, A!1)) | (~(ordered_pair(E, singleton(E)) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1))))))) | (~(in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), tptp_fun_C_8(B!0, A!1)) | (~((~(ordered_pair(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)), singleton(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)))) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))) | (~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | (~in(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)), A!1)))))))),
% 0.37/0.55 inference(unit_resolution,[status(thm)],[55, 49])).
% 0.37/0.55 tff(57,plain,
% 0.37/0.55 (((~((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), tptp_fun_C_8(B!0, A!1))) | (~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | ![E: $i] : ((~in(E, A!1)) | (~(ordered_pair(E, singleton(E)) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1))))))) | (~(in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), tptp_fun_C_8(B!0, A!1)) | (~((~(ordered_pair(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)), singleton(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)))) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))) | (~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | (~in(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)), A!1))))))) | (in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), tptp_fun_C_8(B!0, A!1)) | (~((~(ordered_pair(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)), singleton(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)))) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))) | (~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | (~in(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)), A!1)))))),
% 0.37/0.55 inference(tautology,[status(thm)],[])).
% 0.37/0.55 tff(58,plain,
% 0.37/0.55 (in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), tptp_fun_C_8(B!0, A!1)) | (~((~(ordered_pair(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)), singleton(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)))) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))) | (~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | (~in(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)), A!1))))),
% 0.37/0.55 inference(unit_resolution,[status(thm)],[57, 56])).
% 0.37/0.55 tff(59,plain,
% 0.37/0.55 (~((~((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), tptp_fun_C_8(B!0, A!1))) | (~((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | (~in(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1), A!1)) | (~(ordered_pair(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1), singleton(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1))) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))))))) | (~((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), tptp_fun_C_8(B!0, A!1)) | ![J: $i] : ((~in(J, A!1)) | (~(ordered_pair(J, singleton(J)) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1))))))))),
% 0.37/0.55 inference(unit_resolution,[status(thm)],[28, 22])).
% 0.37/0.55 tff(60,plain,
% 0.37/0.55 ((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), tptp_fun_C_8(B!0, A!1))) | (~((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | (~in(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1), A!1)) | (~(ordered_pair(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1), singleton(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1))) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1))))))),
% 0.37/0.55 inference(unit_resolution,[status(thm)],[31, 59])).
% 0.37/0.55 tff(61,plain,
% 0.37/0.55 (((~((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), tptp_fun_C_8(B!0, A!1))) | (~((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | (~in(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1), A!1)) | (~(ordered_pair(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1), singleton(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1))) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))))))) | (~((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), tptp_fun_C_8(B!0, A!1)) | ![J: $i] : ((~in(J, A!1)) | (~(ordered_pair(J, singleton(J)) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))))))) | ((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), tptp_fun_C_8(B!0, A!1)) | ![J: $i] : ((~in(J, A!1)) | (~(ordered_pair(J, singleton(J)) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1))))))),
% 0.37/0.55 inference(tautology,[status(thm)],[])).
% 0.37/0.55 tff(62,plain,
% 0.37/0.55 ((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), tptp_fun_C_8(B!0, A!1)) | ![J: $i] : ((~in(J, A!1)) | (~(ordered_pair(J, singleton(J)) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))))),
% 0.37/0.55 inference(unit_resolution,[status(thm)],[61, 59])).
% 0.37/0.55 tff(63,assumption,(~((~(ordered_pair(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)), singleton(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)))) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))) | (~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | (~in(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)), A!1)))), introduced(assumption)).
% 0.37/0.55 tff(64,plain,
% 0.37/0.55 (((~(ordered_pair(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)), singleton(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)))) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))) | (~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | (~in(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)), A!1))) | in(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)), A!1)),
% 0.37/0.55 inference(tautology,[status(thm)],[])).
% 0.37/0.55 tff(65,plain,
% 0.37/0.55 (in(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)), A!1)),
% 0.37/0.55 inference(unit_resolution,[status(thm)],[64, 63])).
% 0.37/0.55 tff(66,plain,
% 0.37/0.55 (((~(ordered_pair(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)), singleton(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)))) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))) | (~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | (~in(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)), A!1))) | (ordered_pair(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)), singleton(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)))) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))),
% 0.37/0.55 inference(tautology,[status(thm)],[])).
% 0.37/0.55 tff(67,plain,
% 0.37/0.55 (ordered_pair(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)), singleton(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)))) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1))),
% 0.37/0.55 inference(unit_resolution,[status(thm)],[66, 63])).
% 0.37/0.55 tff(68,assumption,(![J: $i] : ((~in(J, A!1)) | (~(ordered_pair(J, singleton(J)) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))))), introduced(assumption)).
% 0.37/0.55 tff(69,assumption,(in(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)), A!1)), introduced(assumption)).
% 0.37/0.55 tff(70,assumption,(ordered_pair(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)), singleton(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)))) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1))), introduced(assumption)).
% 0.37/0.55 tff(71,plain,
% 0.37/0.55 (((~![J: $i] : ((~in(J, A!1)) | (~(ordered_pair(J, singleton(J)) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))))) | ((~in(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)), A!1)) | (~(ordered_pair(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)), singleton(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)))) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))))) <=> ((~![J: $i] : ((~in(J, A!1)) | (~(ordered_pair(J, singleton(J)) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))))) | (~in(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)), A!1)) | (~(ordered_pair(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)), singleton(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)))) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))))),
% 0.37/0.55 inference(rewrite,[status(thm)],[])).
% 0.37/0.55 tff(72,plain,
% 0.37/0.55 ((~![J: $i] : ((~in(J, A!1)) | (~(ordered_pair(J, singleton(J)) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))))) | ((~in(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)), A!1)) | (~(ordered_pair(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)), singleton(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)))) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))))),
% 0.37/0.55 inference(quant_inst,[status(thm)],[])).
% 0.37/0.55 tff(73,plain,
% 0.37/0.55 ((~![J: $i] : ((~in(J, A!1)) | (~(ordered_pair(J, singleton(J)) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))))) | (~in(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)), A!1)) | (~(ordered_pair(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)), singleton(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)))) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1))))),
% 0.37/0.55 inference(modus_ponens,[status(thm)],[72, 71])).
% 0.37/0.55 tff(74,plain,
% 0.37/0.55 ($false),
% 0.37/0.55 inference(unit_resolution,[status(thm)],[73, 70, 69, 68])).
% 0.37/0.55 tff(75,plain,((~![J: $i] : ((~in(J, A!1)) | (~(ordered_pair(J, singleton(J)) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))))) | (~(ordered_pair(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)), singleton(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)))) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))) | (~in(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)), A!1))), inference(lemma,lemma(discharge,[]))).
% 0.37/0.55 tff(76,plain,
% 0.37/0.55 (~![J: $i] : ((~in(J, A!1)) | (~(ordered_pair(J, singleton(J)) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))))),
% 0.37/0.55 inference(unit_resolution,[status(thm)],[75, 67, 65])).
% 0.37/0.55 tff(77,plain,
% 0.37/0.55 (((~(ordered_pair(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)), singleton(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)))) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))) | (~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | (~in(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)), A!1))) | in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))),
% 0.37/0.55 inference(tautology,[status(thm)],[])).
% 0.37/0.55 tff(78,plain,
% 0.37/0.55 (in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))),
% 0.37/0.55 inference(unit_resolution,[status(thm)],[77, 63])).
% 0.37/0.55 tff(79,plain,
% 0.37/0.55 ((~((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), tptp_fun_C_8(B!0, A!1)) | ![J: $i] : ((~in(J, A!1)) | (~(ordered_pair(J, singleton(J)) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1))))))) | (~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), tptp_fun_C_8(B!0, A!1)) | ![J: $i] : ((~in(J, A!1)) | (~(ordered_pair(J, singleton(J)) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))))),
% 0.37/0.55 inference(tautology,[status(thm)],[])).
% 0.37/0.55 tff(80,plain,
% 0.37/0.55 ((~((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), tptp_fun_C_8(B!0, A!1)) | ![J: $i] : ((~in(J, A!1)) | (~(ordered_pair(J, singleton(J)) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1))))))) | in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), tptp_fun_C_8(B!0, A!1)) | ![J: $i] : ((~in(J, A!1)) | (~(ordered_pair(J, singleton(J)) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))))),
% 0.37/0.55 inference(unit_resolution,[status(thm)],[79, 78])).
% 0.37/0.55 tff(81,plain,
% 0.37/0.55 (in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), tptp_fun_C_8(B!0, A!1))),
% 0.37/0.55 inference(unit_resolution,[status(thm)],[80, 76, 62])).
% 0.37/0.55 tff(82,plain,
% 0.37/0.55 ((~((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), tptp_fun_C_8(B!0, A!1))) | (~((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | (~in(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1), A!1)) | (~(ordered_pair(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1), singleton(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1))) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))))))) | (~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), tptp_fun_C_8(B!0, A!1))) | (~((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | (~in(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1), A!1)) | (~(ordered_pair(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1), singleton(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1))) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1))))))),
% 0.39/0.55 inference(tautology,[status(thm)],[])).
% 0.39/0.55 tff(83,plain,
% 0.39/0.55 (~((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | (~in(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1), A!1)) | (~(ordered_pair(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1), singleton(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1))) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))))),
% 0.39/0.55 inference(unit_resolution,[status(thm)],[82, 81, 60])).
% 0.39/0.55 tff(84,plain,
% 0.39/0.55 (((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | (~in(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1), A!1)) | (~(ordered_pair(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1), singleton(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1))) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1))))) | (ordered_pair(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1), singleton(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1))) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))),
% 0.39/0.55 inference(tautology,[status(thm)],[])).
% 0.39/0.55 tff(85,plain,
% 0.39/0.55 (ordered_pair(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1), singleton(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1))) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1))),
% 0.39/0.55 inference(unit_resolution,[status(thm)],[84, 83])).
% 0.39/0.55 tff(86,plain,
% 0.39/0.55 (((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | (~in(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1), A!1)) | (~(ordered_pair(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1), singleton(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1))) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1))))) | in(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1), A!1)),
% 0.39/0.55 inference(tautology,[status(thm)],[])).
% 0.39/0.55 tff(87,plain,
% 0.39/0.55 (in(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1), A!1)),
% 0.39/0.55 inference(unit_resolution,[status(thm)],[86, 83])).
% 0.39/0.55 tff(88,plain,
% 0.39/0.55 (((~((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), tptp_fun_C_8(B!0, A!1))) | (~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | ![E: $i] : ((~in(E, A!1)) | (~(ordered_pair(E, singleton(E)) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1))))))) | (~(in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), tptp_fun_C_8(B!0, A!1)) | (~((~(ordered_pair(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)), singleton(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)))) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))) | (~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | (~in(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)), A!1))))))) | ((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), tptp_fun_C_8(B!0, A!1))) | (~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | ![E: $i] : ((~in(E, A!1)) | (~(ordered_pair(E, singleton(E)) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1))))))),
% 0.39/0.55 inference(tautology,[status(thm)],[])).
% 0.39/0.55 tff(89,plain,
% 0.39/0.55 ((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), tptp_fun_C_8(B!0, A!1))) | (~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | ![E: $i] : ((~in(E, A!1)) | (~(ordered_pair(E, singleton(E)) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))))),
% 0.39/0.55 inference(unit_resolution,[status(thm)],[88, 56])).
% 0.39/0.55 tff(90,plain,
% 0.39/0.55 ((~((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), tptp_fun_C_8(B!0, A!1))) | (~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | ![E: $i] : ((~in(E, A!1)) | (~(ordered_pair(E, singleton(E)) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1))))))) | (~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), tptp_fun_C_8(B!0, A!1))) | (~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | ![E: $i] : ((~in(E, A!1)) | (~(ordered_pair(E, singleton(E)) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))))),
% 0.39/0.55 inference(tautology,[status(thm)],[])).
% 0.39/0.55 tff(91,plain,
% 0.39/0.55 (![E: $i] : ((~in(E, A!1)) | (~(ordered_pair(E, singleton(E)) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))))),
% 0.39/0.55 inference(unit_resolution,[status(thm)],[90, 81, 78, 89])).
% 0.39/0.55 tff(92,plain,
% 0.39/0.55 (((~![E: $i] : ((~in(E, A!1)) | (~(ordered_pair(E, singleton(E)) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))))) | ((~in(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1), A!1)) | (~(ordered_pair(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1), singleton(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1))) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))))) <=> ((~![E: $i] : ((~in(E, A!1)) | (~(ordered_pair(E, singleton(E)) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))))) | (~in(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1), A!1)) | (~(ordered_pair(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1), singleton(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1))) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))))),
% 0.39/0.55 inference(rewrite,[status(thm)],[])).
% 0.39/0.55 tff(93,plain,
% 0.39/0.55 ((~![E: $i] : ((~in(E, A!1)) | (~(ordered_pair(E, singleton(E)) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))))) | ((~in(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1), A!1)) | (~(ordered_pair(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1), singleton(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1))) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))))),
% 0.39/0.55 inference(quant_inst,[status(thm)],[])).
% 0.39/0.55 tff(94,plain,
% 0.39/0.55 ((~![E: $i] : ((~in(E, A!1)) | (~(ordered_pair(E, singleton(E)) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))))) | (~in(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1), A!1)) | (~(ordered_pair(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1), singleton(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1))) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1))))),
% 0.39/0.55 inference(modus_ponens,[status(thm)],[93, 92])).
% 0.39/0.55 tff(95,plain,
% 0.39/0.55 ($false),
% 0.39/0.55 inference(unit_resolution,[status(thm)],[94, 91, 87, 85])).
% 0.39/0.55 tff(96,plain,((~(ordered_pair(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)), singleton(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)))) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))) | (~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | (~in(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)), A!1))), inference(lemma,lemma(discharge,[]))).
% 0.39/0.55 tff(97,plain,
% 0.39/0.55 ((~(in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), tptp_fun_C_8(B!0, A!1)) | (~((~(ordered_pair(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)), singleton(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)))) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))) | (~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | (~in(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)), A!1)))))) | in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), tptp_fun_C_8(B!0, A!1)) | (~((~(ordered_pair(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)), singleton(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)))) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))) | (~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | (~in(tptp_fun_E_3(tptp_fun_C_8(B!0, A!1)), A!1))))),
% 0.39/0.55 inference(tautology,[status(thm)],[])).
% 0.39/0.55 tff(98,plain,
% 0.39/0.55 (in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), tptp_fun_C_8(B!0, A!1))),
% 0.39/0.55 inference(unit_resolution,[status(thm)],[97, 96, 58])).
% 0.39/0.55 tff(99,plain,
% 0.39/0.55 ((~((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), tptp_fun_C_8(B!0, A!1))) | (~((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | (~in(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1), A!1)) | (~(ordered_pair(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1), singleton(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1))) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))))))) | (~((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | (~in(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1), A!1)) | (~(ordered_pair(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1), singleton(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1))) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1))))))),
% 0.39/0.56 inference(unit_resolution,[status(thm)],[82, 98])).
% 0.39/0.56 tff(100,plain,
% 0.39/0.56 (~((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | (~in(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1), A!1)) | (~(ordered_pair(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1), singleton(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1))) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))))),
% 0.39/0.56 inference(unit_resolution,[status(thm)],[99, 32])).
% 0.39/0.56 tff(101,plain,
% 0.39/0.56 (ordered_pair(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1), singleton(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1))) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1))),
% 0.39/0.56 inference(unit_resolution,[status(thm)],[84, 100])).
% 0.39/0.56 tff(102,plain,
% 0.39/0.56 (in(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1), A!1)),
% 0.39/0.56 inference(unit_resolution,[status(thm)],[86, 100])).
% 0.39/0.56 tff(103,plain,
% 0.39/0.56 (((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | (~in(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1), A!1)) | (~(ordered_pair(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1), singleton(tptp_fun_J_9(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), A!1))) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1))))) | in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))),
% 0.39/0.56 inference(tautology,[status(thm)],[])).
% 0.39/0.56 tff(104,plain,
% 0.39/0.56 (in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))),
% 0.39/0.56 inference(unit_resolution,[status(thm)],[103, 100])).
% 0.39/0.56 tff(105,plain,
% 0.39/0.56 ((~in(tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)), cartesian_product2(A!1, B!0))) | ![E: $i] : ((~in(E, A!1)) | (~(ordered_pair(E, singleton(E)) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))))),
% 0.39/0.56 inference(unit_resolution,[status(thm)],[90, 98, 89])).
% 0.39/0.56 tff(106,plain,
% 0.39/0.56 (![E: $i] : ((~in(E, A!1)) | (~(ordered_pair(E, singleton(E)) = tptp_fun_D_2(tptp_fun_C_8(B!0, A!1)))))),
% 0.39/0.56 inference(unit_resolution,[status(thm)],[105, 104])).
% 0.39/0.56 tff(107,plain,
% 0.39/0.56 ($false),
% 0.39/0.56 inference(unit_resolution,[status(thm)],[94, 106, 102, 101])).
% 0.39/0.56 % SZS output end Proof
% 0.39/0.56 % E exiting
%------------------------------------------------------------------------------