%------------------------------------------------------------------------------ % File : Refute---2015 % Problem : CAT023+1 : TPTP v6.4.0. Released v3.4.0. % Transfm : none % Format : tptp:raw % Command : isabelle tptp_refute %d %s % Computer : n080.star.cs.uiowa.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 2.40GHz % Memory : 32218.75MB % OS : Linux 3.10.0-327.10.1.el7.x86_64 % CPULimit : 300s % DateTime : Tue Apr 12 12:00:12 EDT 2016 % Result : Timeout 300.42s % Output : None % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : CAT023+1 : TPTP v6.4.0. Released v3.4.0. % 0.00/0.04 % Command : isabelle tptp_refute %d %s % 0.03/0.23 % Computer : n080.star.cs.uiowa.edu % 0.03/0.23 % Model : x86_64 x86_64 % 0.03/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz % 0.03/0.23 % Memory : 32218.75MB % 0.03/0.23 % OS : Linux 3.10.0-327.10.1.el7.x86_64 % 0.03/0.23 % CPULimit : 300 % 0.03/0.23 % DateTime : Sat Apr 9 05:40:54 CDT 2016 % 0.03/0.23 % CPUTime : % 6.29/5.84 > val it = (): unit % 6.69/6.29 Trying to find a model that refutes: bnd_v2_cat_1 A & bnd_l1_cat_1 A --> % 6.69/6.29 (ALL B. % 6.69/6.29 bnd_v2_cat_1 B & bnd_l1_cat_1 B --> % 6.69/6.29 (ALL C. % 6.69/6.29 bnd_v2_cat_1 C & bnd_l1_cat_1 C --> % 6.69/6.29 (ALL D. % 6.69/6.29 bnd_m2_cat_1 D (bnd_k11_cat_2 A B) C --> % 6.69/6.29 bnd_r4_nattra_1 (bnd_u1_cat_1 A) % 6.69/6.29 (bnd_u2_cat_1 (bnd_k12_nattra_1 B C)) (bnd_u1_cat_1 A) % 6.69/6.29 (bnd_u2_cat_1 (bnd_k12_nattra_1 B C)) % 6.69/6.29 (bnd_k7_nattra_1 A (bnd_k12_nattra_1 B C) % 6.69/6.29 (bnd_k5_isocat_2 A B C D)) % 6.69/6.29 (bnd_k6_isocat_2 A B C D D % 6.69/6.29 (bnd_k7_nattra_1 (bnd_k11_cat_2 A B) C D))))) % 11.70/11.23 Unfolded term: [| ALL A. % 11.70/11.23 bnd_v2_cat_1 A & bnd_l1_cat_1 A --> % 11.70/11.23 (ALL B. % 11.70/11.23 bnd_v2_cat_1 B & bnd_l1_cat_1 B --> % 11.70/11.23 (ALL C. % 11.70/11.23 bnd_m1_subset_1 C (bnd_u1_cat_1 (bnd_k12_nattra_1 A B)) = % 11.70/11.23 bnd_m2_cat_1 C A B)); % 11.70/11.23 ALL A B. ~ ((bnd_v1_xboole_0 A & ~ A = B) & bnd_v1_xboole_0 B); % 11.70/11.23 ALL A B. ~ (bnd_r2_hidden A B & bnd_v1_xboole_0 B); % 11.70/11.23 ALL A. bnd_v1_xboole_0 A --> A = bnd_k1_xboole_0; % 11.70/11.23 ALL A B C. % 11.70/11.23 ~ ((bnd_r2_hidden A B & bnd_m1_subset_1 B (bnd_k1_zfmisc_1 C)) & % 11.70/11.23 bnd_v1_xboole_0 C); % 11.70/11.23 ALL A. % 11.70/11.23 bnd_v2_cat_1 A & bnd_l1_cat_1 A --> % 11.70/11.23 (ALL B. % 11.70/11.23 bnd_m1_subset_1 B (bnd_u1_cat_1 A) --> % 11.70/11.23 ~ bnd_k6_cat_1 A B B = bnd_k1_xboole_0); % 11.70/11.23 ALL A B C. % 11.70/11.23 bnd_r2_hidden A B & bnd_m1_subset_1 B (bnd_k1_zfmisc_1 C) --> % 11.70/11.23 bnd_m1_subset_1 A C; % 11.70/11.23 ALL A. % 11.70/11.23 bnd_v2_cat_1 A & bnd_l1_cat_1 A --> % 11.70/11.23 (ALL B. % 11.70/11.23 bnd_v2_cat_1 B & bnd_l1_cat_1 B --> % 11.70/11.23 (ALL C. % 11.70/11.23 bnd_v2_cat_1 C & bnd_l1_cat_1 C --> % 11.70/11.23 (ALL D. % 11.70/11.23 bnd_m2_cat_1 D (bnd_k11_cat_2 A B) C --> % 12.31/11.81 (ALL E. % 12.31/11.81 bnd_m1_subset_1 E (bnd_u1_cat_1 A) --> % 12.31/11.81 (ALL F. % 12.31/11.81 bnd_m1_subset_1 F (bnd_u2_cat_1 B) --> % 12.31/11.81 bnd_k8_funct_2 (bnd_u2_cat_1 B) (bnd_u2_cat_1 C) % 12.31/11.81 (bnd_k14_cat_2 A B C D E) F = % 12.31/11.81 bnd_k8_funct_2 (bnd_u2_cat_1 (bnd_k11_cat_2 A B)) % 12.31/11.81 (bnd_u2_cat_1 C) D % 12.31/11.81 (bnd_k13_cat_2 A B (bnd_k10_cat_1 A E) F)))))); % 12.31/11.81 ALL A. % 12.31/11.81 bnd_v2_cat_1 A & bnd_l1_cat_1 A --> % 12.31/11.81 (ALL B. % 12.31/11.81 bnd_v2_cat_1 B & bnd_l1_cat_1 B --> % 12.31/11.81 (ALL C. % 12.31/11.81 bnd_m1_subset_1 C (bnd_u1_cat_1 A) --> % 12.31/11.81 (ALL D. % 12.31/11.81 bnd_m1_subset_1 D (bnd_u1_cat_1 B) --> % 12.31/11.81 bnd_k10_cat_1 (bnd_k11_cat_2 A B) % 12.31/11.81 (bnd_k12_cat_2 A B C D) = % 12.31/11.81 bnd_k13_cat_2 A B (bnd_k10_cat_1 A C) % 12.31/11.81 (bnd_k10_cat_1 B D)))); % 12.31/11.81 ALL A B. bnd_m1_subset_1 A (bnd_k1_zfmisc_1 B) = bnd_r1_tarski A B; % 12.31/11.81 ALL A. % 12.31/11.81 ~ bnd_v1_xboole_0 A --> % 12.31/11.81 (ALL B. % 12.31/11.81 ~ bnd_v1_xboole_0 B --> % 12.31/11.81 (ALL C. % 12.31/11.81 ~ bnd_v1_xboole_0 C --> % 12.31/11.81 (ALL D. % 12.31/11.81 bnd_m1_subset_1 D A --> % 12.31/11.81 (ALL E. % 12.31/11.81 bnd_m1_subset_1 E B --> % 12.31/11.81 (ALL F. % 12.31/11.81 (bnd_v1_funct_1 F & % 12.31/11.81 bnd_v1_funct_2 F (bnd_k2_zfmisc_1 A B) C) & % 12.31/11.81 bnd_m2_relset_1 F (bnd_k2_zfmisc_1 A B) C --> % 12.31/11.81 bnd_k8_funct_2 (bnd_k2_zfmisc_1 A B) C F % 12.31/11.81 (bnd_k1_domain_1 A B D E) = % 12.31/11.81 bnd_k8_funct_2 B C % 12.31/11.81 (bnd_k1_cat_2 A B C (bnd_k1_fraenkel B C) % 12.31/11.81 (bnd_k2_cat_2 A B C F) D) % 12.31/11.81 E))))); % 12.31/11.81 ALL A. % 12.31/11.81 bnd_v2_cat_1 A & bnd_l1_cat_1 A --> % 12.31/11.81 (ALL B. % 12.31/11.81 bnd_v2_cat_1 B & bnd_l1_cat_1 B --> % 12.31/11.81 ((((bnd_u1_cat_1 (bnd_k11_cat_2 A B) = % 12.31/11.81 bnd_k2_zfmisc_1 (bnd_u1_cat_1 A) (bnd_u1_cat_1 B) & % 12.31/11.81 bnd_u2_cat_1 (bnd_k11_cat_2 A B) = % 12.31/11.81 bnd_k2_zfmisc_1 (bnd_u2_cat_1 A) (bnd_u2_cat_1 B)) & % 12.31/11.81 bnd_u3_cat_1 (bnd_k11_cat_2 A B) = % 12.31/11.81 bnd_k9_cat_2 (bnd_u2_cat_1 A) (bnd_u2_cat_1 B) (bnd_u1_cat_1 A) % 12.31/11.81 (bnd_u1_cat_1 B) (bnd_u3_cat_1 A) (bnd_u3_cat_1 B)) & % 12.31/11.81 bnd_u4_cat_1 (bnd_k11_cat_2 A B) = % 12.31/11.81 bnd_k9_cat_2 (bnd_u2_cat_1 A) (bnd_u2_cat_1 B) (bnd_u1_cat_1 A) % 12.31/11.81 (bnd_u1_cat_1 B) (bnd_u4_cat_1 A) (bnd_u4_cat_1 B)) & % 12.31/11.81 bnd_u5_cat_1 (bnd_k11_cat_2 A B) = % 12.31/11.81 bnd_k10_cat_2 (bnd_u2_cat_1 A) (bnd_u2_cat_1 B) (bnd_u5_cat_1 A) % 12.31/11.81 (bnd_u5_cat_1 B)) & % 12.31/11.81 bnd_u6_cat_1 (bnd_k11_cat_2 A B) = % 12.31/11.81 bnd_k9_cat_2 (bnd_u1_cat_1 A) (bnd_u1_cat_1 B) (bnd_u2_cat_1 A) % 12.31/11.81 (bnd_u2_cat_1 B) (bnd_u6_cat_1 A) (bnd_u6_cat_1 B)); % 12.31/11.81 ALL A B. bnd_m1_subset_1 A B --> bnd_v1_xboole_0 B | bnd_r2_hidden A B; % 12.31/11.81 ALL A. % 12.31/11.81 bnd_v2_cat_1 A & bnd_l1_cat_1 A --> % 12.31/11.81 (ALL B. % 12.31/11.81 bnd_v2_cat_1 B & bnd_l1_cat_1 B --> % 12.31/11.81 (ALL C. % 12.31/11.81 bnd_v2_cat_1 C & bnd_l1_cat_1 C --> % 12.31/11.81 (ALL D. % 12.31/11.81 bnd_m2_cat_1 D (bnd_k11_cat_2 A B) C --> % 12.31/11.81 (ALL E. % 12.31/11.81 bnd_m1_subset_1 E (bnd_u1_cat_1 A) --> % 12.31/11.81 bnd_k13_cat_1 A (bnd_k12_nattra_1 B C) % 12.31/11.81 (bnd_k5_isocat_2 A B C D) E = % 12.31/11.81 bnd_k14_cat_2 A B C D E)))); % 12.31/11.81 ALL A. % 12.31/11.81 bnd_v2_cat_1 A & bnd_l1_cat_1 A --> % 12.31/11.81 (ALL B. % 12.31/11.81 bnd_v2_cat_1 B & bnd_l1_cat_1 B --> % 12.31/11.81 (ALL C. % 12.31/11.81 bnd_m2_cat_1 C B A --> % 12.31/11.81 (ALL D. % 12.31/11.81 bnd_m1_subset_1 D (bnd_u1_cat_1 B) --> % 12.31/11.81 bnd_k5_nattra_1 B A C C (bnd_k4_nattra_1 B A C) D = % 12.31/11.81 bnd_k10_cat_1 A (bnd_k13_cat_1 B A C D)))); % 12.31/11.81 ALL A. % 12.31/11.81 bnd_v2_cat_1 A & bnd_l1_cat_1 A --> % 12.31/11.81 (ALL B. % 12.31/11.81 bnd_v2_cat_1 B & bnd_l1_cat_1 B --> % 12.31/11.81 (ALL C. % 12.31/11.81 bnd_m2_cat_1 C B A --> % 12.31/11.81 (ALL D. % 12.31/11.81 bnd_m2_cat_1 D B A --> % 12.31/11.81 bnd_r1_nattra_1 B A C D --> % 12.31/11.81 (ALL E. % 12.31/11.81 bnd_m1_nattra_1 E B A C D --> % 12.31/11.81 (ALL F. % 12.31/11.81 bnd_m1_nattra_1 F B A C D --> % 12.31/11.81 (ALL G. % 12.31/11.81 bnd_m1_subset_1 G (bnd_u1_cat_1 B) --> % 12.31/11.81 bnd_k5_nattra_1 B A C D E G = % 12.31/11.81 bnd_k5_nattra_1 B A C D F G) --> % 12.31/11.81 E = F))))); % 12.31/11.81 ALL A B. bnd_r2_hidden A B --> bnd_m1_subset_1 A B; % 12.31/11.81 ALL A B C. % 12.31/11.81 (bnd_v1_funct_1 C & bnd_v1_funct_2 C A B) & bnd_m2_relset_1 C A B --> % 12.31/11.81 (ALL D. % 12.31/11.81 (bnd_v1_funct_1 D & bnd_v1_funct_2 D A B) & % 12.31/11.81 bnd_m2_relset_1 D A B --> % 12.31/11.81 (ALL E. % 12.31/11.81 bnd_m1_subset_1 E A --> % 12.31/11.81 bnd_k1_funct_1 C E = bnd_k1_funct_1 D E) --> % 12.31/11.81 C = D); % 12.31/11.81 ALL A. % 12.31/11.81 bnd_v2_cat_1 A & bnd_l1_cat_1 A --> % 12.31/11.81 (ALL B. % 12.31/11.81 bnd_v2_cat_1 B & bnd_l1_cat_1 B --> % 12.31/11.81 (ALL C. % 12.31/11.81 bnd_m2_cat_1 C A B --> % 12.31/11.81 (ALL D. % 12.31/11.81 bnd_m1_subset_1 D (bnd_u1_cat_1 A) --> % 12.31/11.81 bnd_k8_funct_2 (bnd_u2_cat_1 A) (bnd_u2_cat_1 B) C % 12.31/11.81 (bnd_k10_cat_1 A D) = % 12.31/11.81 bnd_k10_cat_1 B (bnd_k13_cat_1 A B C D)))); % 12.31/11.81 ALL A B C D E F. % 12.31/11.81 ((((((((~ bnd_v1_xboole_0 A & ~ bnd_v1_xboole_0 B) & % 12.31/11.81 ~ bnd_v1_xboole_0 C) & % 12.31/11.81 ~ bnd_v1_xboole_0 D) & % 12.31/11.81 bnd_v1_funct_1 E) & % 12.31/11.81 bnd_v1_funct_2 E A B) & % 12.31/11.81 bnd_m1_relset_1 E A B) & % 12.31/11.81 bnd_v1_funct_1 F) & % 12.31/11.81 bnd_v1_funct_2 F C D) & % 12.31/11.81 bnd_m1_relset_1 F C D --> % 12.31/11.81 bnd_r4_nattra_1 A B C D E F --> bnd_r4_nattra_1 A B C D F E; % 12.31/11.81 ALL A B C D E F. % 12.31/11.81 ((((((((~ bnd_v1_xboole_0 A & ~ bnd_v1_xboole_0 B) & % 12.31/11.81 ~ bnd_v1_xboole_0 C) & % 12.31/11.81 ~ bnd_v1_xboole_0 D) & % 12.31/11.81 bnd_v1_funct_1 E) & % 12.31/11.81 bnd_v1_funct_2 E A B) & % 12.31/11.81 bnd_m1_relset_1 E A B) & % 12.31/11.81 bnd_v1_funct_1 F) & % 12.31/11.81 bnd_v1_funct_2 F C D) & % 12.31/11.81 bnd_m1_relset_1 F C D --> % 12.31/11.81 bnd_r4_nattra_1 A B C D E E; % 12.31/11.81 ALL A B C D. % 12.31/11.81 ((((bnd_v2_cat_1 A & bnd_l1_cat_1 A) & bnd_v2_cat_1 B) & % 12.31/11.81 bnd_l1_cat_1 B) & % 12.31/11.81 bnd_m2_cat_1 C A B) & % 12.31/11.81 bnd_m2_cat_1 D A B --> % 12.31/11.81 bnd_r2_nattra_1 A B C C; % 12.31/11.81 ALL A B. bnd_r1_tarski A A; % 12.31/11.81 ALL A B C D. % 12.31/11.81 ((((bnd_v2_cat_1 A & bnd_l1_cat_1 A) & bnd_v2_cat_1 B) & % 12.31/11.81 bnd_l1_cat_1 B) & % 12.31/11.81 bnd_m2_cat_1 C A B) & % 12.31/11.81 bnd_m2_cat_1 D A B --> % 12.31/11.81 bnd_r1_nattra_1 A B C C; % 12.31/11.81 ALL A B C D E F. % 12.31/11.81 ((((((((~ bnd_v1_xboole_0 A & ~ bnd_v1_xboole_0 B) & % 12.31/11.81 ~ bnd_v1_xboole_0 C) & % 12.31/11.81 ~ bnd_v1_xboole_0 D) & % 12.31/11.81 bnd_v1_funct_1 E) & % 12.31/11.81 bnd_v1_funct_2 E A B) & % 12.31/11.81 bnd_m1_relset_1 E A B) & % 12.31/11.81 bnd_v1_funct_1 F) & % 12.31/11.81 bnd_v1_funct_2 F C D) & % 12.31/11.81 bnd_m1_relset_1 F C D --> % 12.31/11.81 bnd_r4_nattra_1 A B C D E F = (E = F); % 12.31/11.81 ALL A B C. bnd_m2_relset_1 C A B = bnd_m1_relset_1 C A B; % 12.31/11.81 ALL A B C. % 12.31/11.81 ~ bnd_v1_xboole_0 B & bnd_m1_fraenkel C A B --> % 12.31/11.81 (ALL D. bnd_m2_fraenkel D A B C = bnd_m1_subset_1 D C); % 12.31/11.81 ALL A B C D E F. % 12.31/11.81 ((((((((~ bnd_v1_xboole_0 A & ~ bnd_v1_xboole_0 B) & % 12.31/11.81 ~ bnd_v1_xboole_0 C) & % 12.31/11.81 ~ bnd_v1_xboole_0 D) & % 12.31/11.81 bnd_v1_funct_1 E) & % 12.31/11.81 bnd_v1_funct_2 E A C) & % 12.31/11.81 bnd_m1_relset_1 E A C) & % 12.31/11.81 bnd_v1_funct_1 F) & % 12.31/11.81 bnd_v1_funct_2 F B D) & % 12.31/11.81 bnd_m1_relset_1 F B D --> % 12.31/11.81 bnd_k9_cat_2 A B C D E F = bnd_k15_funct_3 E F; % 12.31/11.81 ALL A B C D. % 12.31/11.81 (((~ bnd_v1_xboole_0 A & bnd_v1_funct_1 C) & bnd_v1_funct_2 C A B) & % 12.31/11.81 bnd_m1_relset_1 C A B) & % 12.31/11.81 bnd_m1_subset_1 D A --> % 12.31/11.81 bnd_k8_funct_2 A B C D = bnd_k1_funct_1 C D; % 12.31/11.81 ALL A B C. % 12.31/11.81 (((bnd_v2_cat_1 A & bnd_l1_cat_1 A) & bnd_v2_cat_1 B) & % 12.31/11.81 bnd_l1_cat_1 B) & % 12.31/11.81 bnd_m2_cat_1 C A B --> % 12.31/11.81 bnd_k7_nattra_1 A B C = bnd_k4_nattra_1 A B C; % 12.31/11.81 ALL A B. % 12.31/11.81 ((bnd_v2_cat_1 A & bnd_l1_cat_1 A) & bnd_v2_cat_1 B) & % 12.31/11.81 bnd_l1_cat_1 B --> % 12.31/11.81 bnd_k7_cat_2 A B = bnd_k5_cat_2 A B; % 12.31/11.81 ALL A B C D. % 12.31/11.81 ((((~ bnd_v1_xboole_0 A & ~ bnd_v1_xboole_0 B) & % 12.31/11.81 ~ bnd_v1_xboole_0 C) & % 12.31/11.81 bnd_v1_funct_1 D) & % 12.31/11.81 bnd_v1_funct_2 D (bnd_k2_zfmisc_1 A B) C) & % 12.31/11.81 bnd_m1_relset_1 D (bnd_k2_zfmisc_1 A B) C --> % 12.31/11.81 bnd_k2_cat_2 A B C D = bnd_k3_funct_5 D; % 12.31/11.81 ALL A B. % 12.31/11.81 ~ bnd_v1_xboole_0 B --> bnd_k1_fraenkel A B = bnd_k1_funct_2 A B; % 12.31/11.81 ALL A B C D. % 12.31/11.81 ((~ bnd_v1_xboole_0 A & ~ bnd_v1_xboole_0 B) & bnd_m1_subset_1 C A) & % 12.31/11.81 bnd_m1_subset_1 D B --> % 12.31/11.81 bnd_k1_domain_1 A B C D = bnd_k4_tarski C D; % 12.31/11.81 ALL A B C D E F. % 12.31/11.81 (((((~ bnd_v1_xboole_0 A & ~ bnd_v1_xboole_0 C) & % 12.31/11.81 bnd_m1_fraenkel D B C) & % 12.31/11.81 bnd_v1_funct_1 E) & % 12.31/11.81 bnd_v1_funct_2 E A D) & % 12.31/11.81 bnd_m1_relset_1 E A D) & % 12.31/11.81 bnd_m1_subset_1 F A --> % 12.31/11.81 bnd_k1_cat_2 A B C D E F = bnd_k1_funct_1 E F; % 12.31/11.81 ALL A B C D. % 12.31/11.81 ((((bnd_v2_cat_1 A & bnd_l1_cat_1 A) & bnd_v2_cat_1 B) & % 12.31/11.81 bnd_l1_cat_1 B) & % 12.31/11.81 bnd_m1_subset_1 C (bnd_u2_cat_1 A)) & % 12.31/11.81 bnd_m1_subset_1 D (bnd_u2_cat_1 B) --> % 12.31/11.81 bnd_k13_cat_2 A B C D = bnd_k4_tarski C D; % 12.31/11.81 ALL A B C D. % 12.31/11.81 ((((bnd_v2_cat_1 A & bnd_l1_cat_1 A) & bnd_v2_cat_1 B) & % 12.31/11.81 bnd_l1_cat_1 B) & % 12.31/11.81 bnd_m1_subset_1 C (bnd_u1_cat_1 A)) & % 12.31/11.81 bnd_m1_subset_1 D (bnd_u1_cat_1 B) --> % 12.31/11.81 bnd_k12_cat_2 A B C D = bnd_k4_tarski C D; % 12.31/11.81 ALL A B C D. % 12.31/11.81 ((((~ bnd_v1_xboole_0 A & ~ bnd_v1_xboole_0 B) & bnd_v1_funct_1 C) & % 12.31/11.81 bnd_m1_relset_1 C (bnd_k2_zfmisc_1 A A) A) & % 12.31/11.81 bnd_v1_funct_1 D) & % 12.31/11.81 bnd_m1_relset_1 D (bnd_k2_zfmisc_1 B B) B --> % 12.31/11.81 bnd_k10_cat_2 A B C D = bnd_k3_funct_4 C D; % 12.31/11.81 ALL A B. % 12.31/11.81 (bnd_v2_cat_1 A & bnd_l1_cat_1 A) & % 12.31/11.81 bnd_m1_subset_1 B (bnd_u1_cat_1 A) --> % 12.31/11.81 bnd_k10_cat_1 A B = bnd_k5_cat_1 A B; % 12.31/11.81 EX A. ~ bnd_v1_xboole_0 A; % 12.31/11.81 ALL A. EX B. bnd_m1_subset_1 B (bnd_k1_zfmisc_1 A) & bnd_v1_xboole_0 B; % 12.31/11.81 Ex bnd_v1_xboole_0; % 12.31/11.81 ALL A. % 12.31/11.81 ~ bnd_v1_xboole_0 A --> % 12.31/11.81 (EX B. bnd_m1_subset_1 B (bnd_k1_zfmisc_1 A) & ~ bnd_v1_xboole_0 B); % 12.31/11.81 ALL A B C D E F. % 12.31/11.81 (((((((((((~ bnd_v1_xboole_0 A & ~ bnd_v1_xboole_0 B) & % 12.31/11.81 bnd_v1_funct_1 C) & % 12.31/11.81 bnd_v1_funct_2 C B A) & % 12.31/11.81 bnd_m1_relset_1 C B A) & % 12.31/11.81 bnd_v1_funct_1 D) & % 12.31/11.81 bnd_v1_funct_2 D B A) & % 12.31/11.81 bnd_m1_relset_1 D B A) & % 12.31/11.81 bnd_v1_funct_1 E) & % 12.31/11.81 bnd_m1_relset_1 E (bnd_k2_zfmisc_1 B B) B) & % 12.31/11.81 bnd_v1_funct_1 F) & % 12.31/11.81 bnd_v1_funct_2 F A B) & % 12.31/11.81 bnd_m1_relset_1 F A B --> % 12.31/11.81 (ALL G H I J K L. % 12.31/11.81 bnd_g1_cat_1 A B C D E F = bnd_g1_cat_1 G H I J K L --> % 12.31/11.81 ((((A = G & B = H) & C = I) & D = J) & E = K) & F = L); % 12.31/11.81 ALL A B. % 12.31/11.81 ~ bnd_v1_xboole_0 A & ~ bnd_v1_xboole_0 B --> % 12.31/11.81 ~ bnd_v1_xboole_0 (bnd_k2_zfmisc_1 A B); % 12.31/11.81 ALL A B. ~ bnd_v1_xboole_0 (bnd_k2_tarski A B); % 12.31/11.81 ALL A. ~ bnd_v1_xboole_0 (bnd_k1_tarski A); % 12.31/11.81 bnd_v1_xboole_0 bnd_k1_xboole_0; % 12.31/11.81 ALL A. ~ bnd_v1_xboole_0 (bnd_k1_zfmisc_1 A); % 12.31/11.81 ALL A B. % 12.31/11.81 ((bnd_v2_cat_1 A & bnd_l1_cat_1 A) & bnd_v2_cat_1 B) & % 12.31/11.81 bnd_l1_cat_1 B --> % 12.31/11.81 (EX C. bnd_m4_nattra_1 C A B); % 12.31/11.81 ALL A B. EX C. bnd_m2_relset_1 C A B; % 12.31/11.81 ALL A B C D. % 12.31/11.81 ((((bnd_v2_cat_1 A & bnd_l1_cat_1 A) & bnd_v2_cat_1 B) & % 12.31/11.81 bnd_l1_cat_1 B) & % 12.31/11.81 bnd_m2_cat_1 C A B) & % 12.31/11.81 bnd_m2_cat_1 D A B --> % 12.31/11.81 (EX E. bnd_m2_nattra_1 E A B C D); % 12.31/11.81 ALL A B C. % 12.31/11.81 ~ bnd_v1_xboole_0 B & bnd_m1_fraenkel C A B --> % 12.31/11.81 (EX D. bnd_m2_fraenkel D A B C); % 12.31/11.81 ALL A B. % 12.31/11.81 ((bnd_v2_cat_1 A & bnd_l1_cat_1 A) & bnd_v2_cat_1 B) & % 12.31/11.81 bnd_l1_cat_1 B --> % 12.31/11.81 (EX C. bnd_m2_cat_1 C A B); % 12.31/11.81 ALL A. EX B. bnd_m1_subset_1 B A; ALL A B. EX C. bnd_m1_relset_1 C A B; % 12.31/11.81 ALL A B C D. % 12.31/11.81 ((((bnd_v2_cat_1 A & bnd_l1_cat_1 A) & bnd_v2_cat_1 B) & % 12.31/11.81 bnd_l1_cat_1 B) & % 12.31/11.81 bnd_m2_cat_1 C A B) & % 12.31/11.81 bnd_m2_cat_1 D A B --> % 12.31/11.81 (EX E. bnd_m1_nattra_1 E A B C D); % 12.31/11.81 ALL A B. EX C. bnd_m1_fraenkel C A B; % 12.31/11.81 ALL A B. % 12.31/11.81 ((bnd_v2_cat_1 A & bnd_l1_cat_1 A) & bnd_v2_cat_1 B) & % 12.31/11.81 bnd_l1_cat_1 B --> % 12.31/11.81 (EX C. bnd_m1_cat_2 C A B); % 12.31/11.81 ALL A B C. % 12.31/11.81 (bnd_l1_cat_1 A & bnd_m1_subset_1 B (bnd_u1_cat_1 A)) & % 12.31/11.81 bnd_m1_subset_1 C (bnd_u1_cat_1 A) --> % 12.31/11.81 (EX D. bnd_m1_cat_1 D A B C); % 12.31/11.81 Ex bnd_l1_cat_1; % 12.31/11.81 ALL A. % 12.31/11.81 bnd_l1_cat_1 A --> % 12.31/11.81 (bnd_v1_funct_1 (bnd_u6_cat_1 A) & % 12.31/11.81 bnd_v1_funct_2 (bnd_u6_cat_1 A) (bnd_u1_cat_1 A) (bnd_u2_cat_1 A)) & % 12.31/11.81 bnd_m2_relset_1 (bnd_u6_cat_1 A) (bnd_u1_cat_1 A) (bnd_u2_cat_1 A); % 12.31/11.81 ALL A. % 12.31/11.81 bnd_l1_cat_1 A --> % 12.31/11.81 bnd_v1_funct_1 (bnd_u5_cat_1 A) & % 12.31/11.81 bnd_m2_relset_1 (bnd_u5_cat_1 A) % 12.31/11.81 (bnd_k2_zfmisc_1 (bnd_u2_cat_1 A) (bnd_u2_cat_1 A)) (bnd_u2_cat_1 A); % 12.31/11.81 ALL A. % 12.31/11.81 bnd_l1_cat_1 A --> % 12.31/11.81 (bnd_v1_funct_1 (bnd_u4_cat_1 A) & % 12.31/11.81 bnd_v1_funct_2 (bnd_u4_cat_1 A) (bnd_u2_cat_1 A) (bnd_u1_cat_1 A)) & % 12.31/11.81 bnd_m2_relset_1 (bnd_u4_cat_1 A) (bnd_u2_cat_1 A) (bnd_u1_cat_1 A); % 12.31/11.81 ALL A. % 12.31/11.81 bnd_l1_cat_1 A --> % 12.31/11.81 (bnd_v1_funct_1 (bnd_u3_cat_1 A) & % 12.31/11.81 bnd_v1_funct_2 (bnd_u3_cat_1 A) (bnd_u2_cat_1 A) (bnd_u1_cat_1 A)) & % 12.31/11.81 bnd_m2_relset_1 (bnd_u3_cat_1 A) (bnd_u2_cat_1 A) (bnd_u1_cat_1 A); % 12.31/11.81 ALL A. bnd_l1_cat_1 A --> ~ bnd_v1_xboole_0 (bnd_u2_cat_1 A); % 12.31/11.81 ALL A. bnd_l1_cat_1 A --> ~ bnd_v1_xboole_0 (bnd_u1_cat_1 A); % 12.31/11.81 ALL A B. % 12.31/11.81 ((bnd_v2_cat_1 A & bnd_l1_cat_1 A) & bnd_v2_cat_1 B) & % 12.31/11.81 bnd_l1_cat_1 B --> % 12.31/11.81 (ALL C. bnd_m4_nattra_1 C A B --> ~ bnd_v1_xboole_0 C); % 12.31/11.81 ALL A B C. % 12.31/11.81 bnd_m2_relset_1 C A B --> % 12.31/11.81 bnd_m1_subset_1 C (bnd_k1_zfmisc_1 (bnd_k2_zfmisc_1 A B)); % 12.31/11.81 ALL A B C D. % 12.31/11.81 ((((bnd_v2_cat_1 A & bnd_l1_cat_1 A) & bnd_v2_cat_1 B) & % 12.31/11.81 bnd_l1_cat_1 B) & % 12.31/11.81 bnd_m2_cat_1 C A B) & % 12.31/11.81 bnd_m2_cat_1 D A B --> % 12.31/11.81 (ALL E. bnd_m2_nattra_1 E A B C D --> bnd_m1_nattra_1 E A B C D); % 12.31/11.81 ALL A B C. % 12.31/11.81 ~ bnd_v1_xboole_0 B & bnd_m1_fraenkel C A B --> % 12.31/11.81 (ALL D. % 12.31/11.81 bnd_m2_fraenkel D A B C --> % 12.31/11.81 (bnd_v1_funct_1 D & bnd_v1_funct_2 D A B) & % 12.31/11.81 bnd_m2_relset_1 D A B); % 12.31/11.81 ALL A B. % 12.31/11.81 ((bnd_v2_cat_1 A & bnd_l1_cat_1 A) & bnd_v2_cat_1 B) & % 12.31/11.81 bnd_l1_cat_1 B --> % 12.31/11.81 (ALL C. % 12.31/11.81 bnd_m2_cat_1 C A B --> % 12.31/11.81 (bnd_v1_funct_1 C & % 12.31/11.81 bnd_v1_funct_2 C (bnd_u2_cat_1 A) (bnd_u2_cat_1 B)) & % 12.31/11.81 bnd_m2_relset_1 C (bnd_u2_cat_1 A) (bnd_u2_cat_1 B)); % 12.31/11.81 True; True; % 12.31/11.81 ALL A B C D. % 12.31/11.82 ((((bnd_v2_cat_1 A & bnd_l1_cat_1 A) & bnd_v2_cat_1 B) & % 12.31/11.82 bnd_l1_cat_1 B) & % 12.31/11.82 bnd_m2_cat_1 C A B) & % 12.31/11.82 bnd_m2_cat_1 D A B --> % 12.31/11.82 (ALL E. % 12.31/11.82 bnd_m1_nattra_1 E A B C D --> % 12.31/11.82 (bnd_v1_funct_1 E & % 12.31/11.82 bnd_v1_funct_2 E (bnd_u1_cat_1 A) (bnd_u2_cat_1 B)) & % 12.31/11.82 bnd_m2_relset_1 E (bnd_u1_cat_1 A) (bnd_u2_cat_1 B)); % 12.31/11.82 ALL A B C. % 12.31/11.82 bnd_m1_fraenkel C A B --> ~ bnd_v1_xboole_0 C & bnd_v1_fraenkel C; % 12.31/11.82 ALL A B. % 12.31/11.82 ((bnd_v2_cat_1 A & bnd_l1_cat_1 A) & bnd_v2_cat_1 B) & % 12.31/11.82 bnd_l1_cat_1 B --> % 12.31/11.82 (ALL C. bnd_m1_cat_2 C A B --> ~ bnd_v1_xboole_0 C); % 12.31/11.82 ALL A B C. % 12.31/11.82 (bnd_l1_cat_1 A & bnd_m1_subset_1 B (bnd_u1_cat_1 A)) & % 12.31/11.82 bnd_m1_subset_1 C (bnd_u1_cat_1 A) --> % 12.31/11.82 (ALL D. bnd_m1_cat_1 D A B C --> bnd_m1_subset_1 D (bnd_u2_cat_1 A)); % 12.31/11.82 True; % 12.31/11.82 ALL A B C D E F. % 12.31/11.82 ((((((((~ bnd_v1_xboole_0 A & ~ bnd_v1_xboole_0 B) & % 12.31/11.82 ~ bnd_v1_xboole_0 C) & % 12.31/11.82 ~ bnd_v1_xboole_0 D) & % 12.31/11.82 bnd_v1_funct_1 E) & % 12.31/11.82 bnd_v1_funct_2 E A C) & % 12.31/11.82 bnd_m1_relset_1 E A C) & % 12.31/11.82 bnd_v1_funct_1 F) & % 12.31/11.82 bnd_v1_funct_2 F B D) & % 12.31/11.82 bnd_m1_relset_1 F B D --> % 12.31/11.82 (bnd_v1_funct_1 (bnd_k9_cat_2 A B C D E F) & % 12.31/11.82 bnd_v1_funct_2 (bnd_k9_cat_2 A B C D E F) (bnd_k2_zfmisc_1 A B) % 12.31/11.82 (bnd_k2_zfmisc_1 C D)) & % 12.31/11.82 bnd_m2_relset_1 (bnd_k9_cat_2 A B C D E F) (bnd_k2_zfmisc_1 A B) % 12.31/11.82 (bnd_k2_zfmisc_1 C D); % 12.31/11.82 ALL A B C D E F G. % 12.31/11.82 (((((((bnd_v2_cat_1 A & bnd_l1_cat_1 A) & bnd_v2_cat_1 B) & % 12.31/11.82 bnd_l1_cat_1 B) & % 12.31/11.82 bnd_m2_cat_1 C A B) & % 12.31/11.82 bnd_m2_cat_1 D A B) & % 12.31/11.82 bnd_m2_cat_1 E A B) & % 12.31/11.82 bnd_m2_nattra_1 F A B C D) & % 12.31/11.82 bnd_m2_nattra_1 G A B D E --> % 12.31/11.82 bnd_m2_nattra_1 (bnd_k8_nattra_1 A B C D E F G) A B C E; % 12.31/11.82 ALL A B C D. % 12.31/11.82 (((~ bnd_v1_xboole_0 A & bnd_v1_funct_1 C) & bnd_v1_funct_2 C A B) & % 12.31/11.82 bnd_m1_relset_1 C A B) & % 12.31/11.82 bnd_m1_subset_1 D A --> % 12.31/11.82 bnd_m1_subset_1 (bnd_k8_funct_2 A B C D) B; % 12.31/11.82 ALL A B C. % 12.31/11.82 (((bnd_v2_cat_1 A & bnd_l1_cat_1 A) & bnd_v2_cat_1 B) & % 12.31/11.82 bnd_l1_cat_1 B) & % 12.31/11.82 bnd_m2_cat_1 C A B --> % 12.31/11.82 bnd_m2_nattra_1 (bnd_k7_nattra_1 A B C) A B C C; % 12.31/11.82 ALL A B. % 12.31/11.82 ((bnd_v2_cat_1 A & bnd_l1_cat_1 A) & bnd_v2_cat_1 B) & % 12.31/11.82 bnd_l1_cat_1 B --> % 12.31/11.82 bnd_m1_cat_2 (bnd_k7_cat_2 A B) A B; % 12.31/11.82 ALL A B C D E F. % 12.31/11.82 (((((((bnd_v2_cat_1 A & bnd_l1_cat_1 A) & bnd_v2_cat_1 B) & % 12.31/11.82 bnd_l1_cat_1 B) & % 12.31/11.82 bnd_v2_cat_1 C) & % 12.31/11.82 bnd_l1_cat_1 C) & % 12.31/11.82 bnd_m2_cat_1 D (bnd_k11_cat_2 A B) C) & % 12.31/11.82 bnd_m2_cat_1 E (bnd_k11_cat_2 A B) C) & % 12.31/11.82 bnd_m2_nattra_1 F (bnd_k11_cat_2 A B) C D E --> % 12.31/11.82 bnd_m2_nattra_1 (bnd_k6_isocat_2 A B C D E F) A (bnd_k12_nattra_1 B C) % 12.31/11.82 (bnd_k5_isocat_2 A B C D) (bnd_k5_isocat_2 A B C E); % 12.31/11.82 ALL A B C. % 12.31/11.82 (bnd_l1_cat_1 A & bnd_m1_subset_1 B (bnd_u1_cat_1 A)) & % 12.31/11.82 bnd_m1_subset_1 C (bnd_u1_cat_1 A) --> % 12.31/11.82 bnd_m1_subset_1 (bnd_k6_cat_1 A B C) % 12.31/11.82 (bnd_k1_zfmisc_1 (bnd_u2_cat_1 A)); % 12.31/11.82 ALL A B C D E F. % 12.31/11.82 ((((((bnd_v2_cat_1 A & bnd_l1_cat_1 A) & bnd_v2_cat_1 B) & % 12.31/11.82 bnd_l1_cat_1 B) & % 12.31/11.82 bnd_m2_cat_1 C A B) & % 12.31/11.82 bnd_m2_cat_1 D A B) & % 12.31/11.82 bnd_m1_nattra_1 E A B C D) & % 12.31/11.82 bnd_m1_subset_1 F (bnd_u1_cat_1 A) --> % 12.31/11.82 bnd_m1_cat_1 (bnd_k5_nattra_1 A B C D E F) B (bnd_k13_cat_1 A B C F) % 12.31/11.82 (bnd_k13_cat_1 A B D F); % 12.31/11.82 ALL A B C D. % 12.31/11.82 (((((bnd_v2_cat_1 A & bnd_l1_cat_1 A) & bnd_v2_cat_1 B) & % 12.31/11.82 bnd_l1_cat_1 B) & % 12.31/11.82 bnd_v2_cat_1 C) & % 12.31/11.82 bnd_l1_cat_1 C) & % 12.31/11.82 bnd_m2_cat_1 D (bnd_k11_cat_2 A B) C --> % 12.31/11.82 bnd_m2_cat_1 (bnd_k5_isocat_2 A B C D) A (bnd_k12_nattra_1 B C); % 12.31/11.82 True; % 12.31/11.82 ALL A B. % 12.31/11.82 bnd_l1_cat_1 A & bnd_m1_subset_1 B (bnd_u1_cat_1 A) --> % 12.31/11.82 bnd_m1_subset_1 (bnd_k5_cat_1 A B) (bnd_u2_cat_1 A); % 12.31/11.82 True; % 12.31/11.82 ALL A B C. % 12.31/11.82 (((bnd_v2_cat_1 A & bnd_l1_cat_1 A) & bnd_v2_cat_1 B) & % 12.31/11.82 bnd_l1_cat_1 B) & % 12.31/11.82 bnd_m2_cat_1 C A B --> % 12.31/11.82 bnd_m1_nattra_1 (bnd_k4_nattra_1 A B C) A B C C; % 12.31/11.82 ALL A B C D E F. % 12.31/11.82 ((((((bnd_v2_cat_1 A & bnd_l1_cat_1 A) & bnd_v2_cat_1 B) & % 12.31/11.82 bnd_l1_cat_1 B) & % 12.31/11.82 bnd_m2_cat_1 C A B) & % 12.31/11.82 bnd_m1_subset_1 D (bnd_u1_cat_1 A)) & % 12.31/11.82 bnd_m1_subset_1 E (bnd_u1_cat_1 A)) & % 12.31/11.82 bnd_m1_cat_1 F A D E --> % 12.31/11.82 bnd_m1_cat_1 (bnd_k3_nattra_1 A B C D E F) B (bnd_k13_cat_1 A B C D) % 12.31/11.82 (bnd_k13_cat_1 A B C E); % 12.31/11.82 ALL A. % 12.31/11.82 bnd_v1_relat_1 A & bnd_v1_funct_1 A --> % 12.31/11.82 bnd_v1_relat_1 (bnd_k3_funct_5 A) & bnd_v1_funct_1 (bnd_k3_funct_5 A); % 12.31/11.82 ALL A B. % 12.31/11.82 ((bnd_v1_relat_1 A & bnd_v1_funct_1 A) & bnd_v1_relat_1 B) & % 12.31/11.82 bnd_v1_funct_1 B --> % 12.31/11.82 bnd_v1_relat_1 (bnd_k3_funct_4 A B) & % 12.31/11.82 bnd_v1_funct_1 (bnd_k3_funct_4 A B); % 12.31/11.82 ALL A B. % 12.31/11.82 bnd_l1_cat_1 A & bnd_m1_subset_1 B (bnd_u2_cat_1 A) --> % 12.31/11.82 bnd_m1_subset_1 (bnd_k3_cat_1 A B) (bnd_u1_cat_1 A); % 12.31/11.82 True; True; True; % 12.31/11.82 ALL A B C D. % 12.31/11.82 ((((~ bnd_v1_xboole_0 A & ~ bnd_v1_xboole_0 B) & % 12.31/11.82 ~ bnd_v1_xboole_0 C) & % 12.31/11.82 bnd_v1_funct_1 D) & % 12.31/11.82 bnd_v1_funct_2 D (bnd_k2_zfmisc_1 A B) C) & % 12.31/11.82 bnd_m1_relset_1 D (bnd_k2_zfmisc_1 A B) C --> % 12.31/11.82 (bnd_v1_funct_1 (bnd_k2_cat_2 A B C D) & % 12.31/11.82 bnd_v1_funct_2 (bnd_k2_cat_2 A B C D) A (bnd_k1_fraenkel B C)) & % 12.31/11.82 bnd_m2_relset_1 (bnd_k2_cat_2 A B C D) A (bnd_k1_fraenkel B C); % 12.31/11.82 ALL A B. % 12.31/11.82 bnd_l1_cat_1 A & bnd_m1_subset_1 B (bnd_u2_cat_1 A) --> % 12.31/11.82 bnd_m1_subset_1 (bnd_k2_cat_1 A B) (bnd_u1_cat_1 A); % 12.31/11.82 True; True; True; True; True; True; True; % 12.31/11.82 ALL A B. % 12.31/11.82 ~ bnd_v1_xboole_0 B --> bnd_m1_fraenkel (bnd_k1_fraenkel A B) A B; % 12.31/11.82 ALL A B C D. % 12.31/11.82 ((~ bnd_v1_xboole_0 A & ~ bnd_v1_xboole_0 B) & bnd_m1_subset_1 C A) & % 12.31/11.82 bnd_m1_subset_1 D B --> % 12.31/11.82 bnd_m1_subset_1 (bnd_k1_domain_1 A B C D) (bnd_k2_zfmisc_1 A B); % 12.31/11.82 ALL A B C D E F. % 12.31/11.82 (((((~ bnd_v1_xboole_0 A & ~ bnd_v1_xboole_0 C) & % 12.31/11.82 bnd_m1_fraenkel D B C) & % 12.31/11.82 bnd_v1_funct_1 E) & % 12.31/11.82 bnd_v1_funct_2 E A D) & % 12.31/11.82 bnd_m1_relset_1 E A D) & % 12.31/11.82 bnd_m1_subset_1 F A --> % 12.31/11.82 bnd_m2_fraenkel (bnd_k1_cat_2 A B C D E F) B C D; % 12.31/11.82 ALL A B. % 12.31/11.82 ((bnd_v1_relat_1 A & bnd_v1_funct_1 A) & bnd_v1_relat_1 B) & % 12.31/11.82 bnd_v1_funct_1 B --> % 12.31/11.82 bnd_v1_relat_1 (bnd_k15_funct_3 A B) & % 12.31/11.82 bnd_v1_funct_1 (bnd_k15_funct_3 A B); % 12.31/11.82 ALL A B C D E. % 12.31/11.82 ((((((bnd_v2_cat_1 A & bnd_l1_cat_1 A) & bnd_v2_cat_1 B) & % 12.31/11.82 bnd_l1_cat_1 B) & % 12.31/11.82 bnd_v2_cat_1 C) & % 12.31/11.82 bnd_l1_cat_1 C) & % 12.31/11.82 bnd_m2_cat_1 D (bnd_k11_cat_2 A B) C) & % 12.31/11.82 bnd_m1_subset_1 E (bnd_u1_cat_1 A) --> % 12.31/11.82 bnd_m2_cat_1 (bnd_k14_cat_2 A B C D E) B C; % 12.31/11.82 ALL A B C D. % 12.31/11.82 ((((bnd_v2_cat_1 A & bnd_l1_cat_1 A) & bnd_v2_cat_1 B) & % 12.31/11.82 bnd_l1_cat_1 B) & % 12.31/11.82 bnd_m1_subset_1 C (bnd_u2_cat_1 A)) & % 12.31/11.82 bnd_m1_subset_1 D (bnd_u2_cat_1 B) --> % 12.31/11.82 bnd_m1_subset_1 (bnd_k13_cat_2 A B C D) % 12.31/11.82 (bnd_u2_cat_1 (bnd_k11_cat_2 A B)); % 12.31/11.82 ALL A B C D. % 12.31/11.82 ((((bnd_v2_cat_1 A & bnd_l1_cat_1 A) & bnd_v2_cat_1 B) & % 12.31/11.82 bnd_l1_cat_1 B) & % 12.31/11.82 bnd_m2_cat_1 C A B) & % 12.31/11.82 bnd_m1_subset_1 D (bnd_u1_cat_1 A) --> % 12.31/11.82 bnd_m1_subset_1 (bnd_k13_cat_1 A B C D) (bnd_u1_cat_1 B); % 12.31/11.82 ALL A B. % 12.31/11.82 ((bnd_v2_cat_1 A & bnd_l1_cat_1 A) & bnd_v2_cat_1 B) & % 12.31/11.82 bnd_l1_cat_1 B --> % 12.31/11.82 (bnd_v1_cat_1 (bnd_k12_nattra_1 A B) & % 12.31/11.82 bnd_v2_cat_1 (bnd_k12_nattra_1 A B)) & % 12.31/11.82 bnd_l1_cat_1 (bnd_k12_nattra_1 A B); % 12.31/11.82 ALL A B C D. % 12.31/11.82 ((((bnd_v2_cat_1 A & bnd_l1_cat_1 A) & bnd_v2_cat_1 B) & % 12.31/11.82 bnd_l1_cat_1 B) & % 12.31/11.82 bnd_m1_subset_1 C (bnd_u1_cat_1 A)) & % 12.31/11.82 bnd_m1_subset_1 D (bnd_u1_cat_1 B) --> % 12.31/11.82 bnd_m1_subset_1 (bnd_k12_cat_2 A B C D) % 12.31/11.82 (bnd_u1_cat_1 (bnd_k11_cat_2 A B)); % 12.31/11.82 ALL A B. % 12.31/11.82 ((bnd_v2_cat_1 A & bnd_l1_cat_1 A) & bnd_v2_cat_1 B) & % 12.31/11.82 bnd_l1_cat_1 B --> % 12.31/11.82 bnd_m4_nattra_1 (bnd_k11_nattra_1 A B) A B; % 12.31/11.82 ALL A B. % 12.31/11.82 ((bnd_v2_cat_1 A & bnd_l1_cat_1 A) & bnd_v2_cat_1 B) & % 12.31/11.82 bnd_l1_cat_1 B --> % 12.31/11.82 bnd_v2_cat_1 (bnd_k11_cat_2 A B) & bnd_l1_cat_1 (bnd_k11_cat_2 A B); % 12.31/11.82 ALL A B C D. % 12.31/11.82 ((((~ bnd_v1_xboole_0 A & ~ bnd_v1_xboole_0 B) & bnd_v1_funct_1 C) & % 12.31/11.82 bnd_m1_relset_1 C (bnd_k2_zfmisc_1 A A) A) & % 12.31/11.82 bnd_v1_funct_1 D) & % 12.31/11.82 bnd_m1_relset_1 D (bnd_k2_zfmisc_1 B B) B --> % 12.31/11.82 bnd_v1_funct_1 (bnd_k10_cat_2 A B C D) & % 12.31/11.82 bnd_m2_relset_1 (bnd_k10_cat_2 A B C D) % 12.31/11.82 (bnd_k2_zfmisc_1 (bnd_k2_zfmisc_1 A B) (bnd_k2_zfmisc_1 A B)) % 12.31/11.82 (bnd_k2_zfmisc_1 A B); % 12.31/11.82 ALL A B. % 12.31/11.82 (bnd_v2_cat_1 A & bnd_l1_cat_1 A) & % 12.31/11.82 bnd_m1_subset_1 B (bnd_u1_cat_1 A) --> % 12.31/11.82 bnd_m1_cat_1 (bnd_k10_cat_1 A B) A B B; % 12.31/11.82 ALL A B C D E F. % 12.31/11.82 (((((((((((~ bnd_v1_xboole_0 A & ~ bnd_v1_xboole_0 B) & % 12.31/11.82 bnd_v1_funct_1 C) & % 12.31/11.82 bnd_v1_funct_2 C B A) & % 12.31/11.82 bnd_m1_relset_1 C B A) & % 12.31/11.82 bnd_v1_funct_1 D) & % 12.31/11.82 bnd_v1_funct_2 D B A) & % 12.31/11.82 bnd_m1_relset_1 D B A) & % 12.31/11.82 bnd_v1_funct_1 E) & % 12.31/11.82 bnd_m1_relset_1 E (bnd_k2_zfmisc_1 B B) B) & % 12.31/11.82 bnd_v1_funct_1 F) & % 12.31/11.82 bnd_v1_funct_2 F A B) & % 12.31/11.82 bnd_m1_relset_1 F A B --> % 12.31/11.82 bnd_v1_cat_1 (bnd_g1_cat_1 A B C D E F) & % 12.31/11.82 bnd_l1_cat_1 (bnd_g1_cat_1 A B C D E F); % 12.31/11.82 ALL A B. % 12.31/11.82 bnd_k4_tarski A B = % 12.31/11.82 bnd_k2_tarski (bnd_k2_tarski A B) (bnd_k1_tarski A); % 12.31/11.82 ALL A. % 12.31/11.82 bnd_v2_cat_1 A & bnd_l1_cat_1 A --> % 12.31/11.82 (ALL B. % 12.31/11.82 bnd_v2_cat_1 B & bnd_l1_cat_1 B --> % 12.31/11.82 (ALL C. % 12.31/11.82 bnd_m2_cat_1 C A B --> % 12.31/11.82 (ALL D. % 12.31/11.82 bnd_m2_cat_1 D A B --> % 12.31/11.82 bnd_r1_nattra_1 A B C D --> % 12.31/11.82 (ALL E. % 12.31/11.82 bnd_m1_nattra_1 E A B C D --> % 12.31/11.82 (ALL F. % 12.31/11.82 bnd_m1_subset_1 F (bnd_u1_cat_1 A) --> % 12.31/11.82 bnd_k5_nattra_1 A B C D E F = % 12.31/11.82 bnd_k8_funct_2 (bnd_u1_cat_1 A) (bnd_u2_cat_1 B) E % 12.31/11.82 F))))); % 12.31/11.82 ALL A. % 12.31/11.82 bnd_v2_cat_1 A & bnd_l1_cat_1 A --> % 12.31/11.82 (ALL B. % 12.31/11.82 bnd_v2_cat_1 B & bnd_l1_cat_1 B --> % 12.31/11.82 (ALL C. % 12.31/11.82 bnd_v2_cat_1 C & bnd_l1_cat_1 C --> % 12.31/11.82 (ALL D. % 12.31/11.82 bnd_m2_cat_1 D (bnd_k11_cat_2 A B) C --> % 12.31/11.82 (ALL E. % 12.31/11.82 bnd_m2_cat_1 E (bnd_k11_cat_2 A B) C --> % 12.31/11.82 bnd_r2_nattra_1 (bnd_k11_cat_2 A B) C D E --> % 12.31/11.82 (ALL F. % 12.31/11.82 bnd_m2_nattra_1 F (bnd_k11_cat_2 A B) C D E --> % 12.31/11.82 (ALL G. % 12.31/11.82 bnd_m2_nattra_1 G A (bnd_k12_nattra_1 B C) % 12.31/11.82 (bnd_k5_isocat_2 A B C D) % 12.31/11.82 (bnd_k5_isocat_2 A B C E) --> % 12.31/11.82 (G = bnd_k6_isocat_2 A B C D E F) = % 12.31/11.82 (ALL H. % 12.31/11.82 (bnd_v1_funct_1 H & % 12.31/11.82 bnd_v1_funct_2 H % 12.31/11.82 (bnd_k2_zfmisc_1 (bnd_u1_cat_1 A) % 12.31/11.82 (bnd_u1_cat_1 B)) % 12.31/11.82 (bnd_u2_cat_1 C)) & % 12.31/11.82 bnd_m2_relset_1 H % 12.31/11.82 (bnd_k2_zfmisc_1 (bnd_u1_cat_1 A) % 12.31/11.82 (bnd_u1_cat_1 B)) % 12.31/11.82 (bnd_u2_cat_1 C) --> % 12.31/11.82 bnd_r4_nattra_1 % 12.31/11.82 (bnd_u1_cat_1 (bnd_k11_cat_2 A B)) % 12.31/11.82 (bnd_u2_cat_1 C) % 12.31/11.82 (bnd_k2_zfmisc_1 (bnd_u1_cat_1 A) % 12.31/11.82 (bnd_u1_cat_1 B)) % 12.31/11.82 (bnd_u2_cat_1 C) F H --> % 12.31/11.82 (ALL I. % 12.31/11.82 bnd_m1_subset_1 I (bnd_u1_cat_1 A) --> % 12.31/11.82 bnd_k5_nattra_1 A (bnd_k12_nattra_1 B C) (bnd_k5_isocat_2 A B C D) % 12.31/11.82 (bnd_k5_isocat_2 A B C E) G I = % 12.31/11.82 bnd_k4_tarski % 12.31/11.82 (bnd_k12_cat_2 (bnd_k12_nattra_1 B C) (bnd_k12_nattra_1 B C) % 12.31/11.82 (bnd_k13_cat_1 A (bnd_k12_nattra_1 B C) (bnd_k5_isocat_2 A B C D) I) % 12.31/11.82 (bnd_k13_cat_1 A (bnd_k12_nattra_1 B C) (bnd_k5_isocat_2 A B C E) I)) % 12.31/11.82 (bnd_k1_cat_2 (bnd_u1_cat_1 A) (bnd_u1_cat_1 B) (bnd_u2_cat_1 C) % 12.31/11.82 (bnd_k1_fraenkel (bnd_u1_cat_1 B) (bnd_u2_cat_1 C)) % 12.31/11.82 (bnd_k2_cat_2 (bnd_u1_cat_1 A) (bnd_u1_cat_1 B) (bnd_u2_cat_1 C) H) % 12.31/11.82 I))))))))); % 12.31/11.82 ALL A. % 12.31/11.82 bnd_v2_cat_1 A & bnd_l1_cat_1 A --> % 12.31/11.82 (ALL B. % 12.31/11.82 bnd_v2_cat_1 B & bnd_l1_cat_1 B --> % 12.31/11.82 (ALL C. % 12.31/11.82 bnd_m2_cat_1 C A B --> % 12.31/11.82 (ALL D. % 12.31/11.82 bnd_m1_subset_1 D (bnd_u1_cat_1 A) --> % 12.31/11.82 (ALL E. % 12.31/11.82 bnd_m1_subset_1 E (bnd_u1_cat_1 A) --> % 12.31/11.82 ~ bnd_k6_cat_1 A D E = bnd_k1_xboole_0 --> % 12.31/11.82 (ALL F. % 12.31/11.82 bnd_m1_cat_1 F A D E --> % 12.31/11.82 bnd_k3_nattra_1 A B C D E F = % 12.31/11.82 bnd_k8_funct_2 (bnd_u2_cat_1 A) (bnd_u2_cat_1 B) C % 12.31/11.82 F))))); % 12.31/11.82 ALL A. % 12.31/11.82 bnd_v2_cat_1 A & bnd_l1_cat_1 A --> % 12.31/11.82 (ALL B. % 12.31/11.82 bnd_v2_cat_1 B & bnd_l1_cat_1 B --> % 12.31/11.82 (ALL C. % 12.31/11.82 (bnd_v1_cat_1 C & bnd_v2_cat_1 C) & bnd_l1_cat_1 C --> % 12.31/11.82 (C = bnd_k12_nattra_1 A B) = % 12.31/11.82 (((((bnd_u1_cat_1 C = bnd_k7_cat_2 A B & % 12.31/11.82 bnd_u2_cat_1 C = bnd_k11_nattra_1 A B) & % 12.31/11.82 (ALL D. % 12.31/11.82 bnd_m1_subset_1 D (bnd_u2_cat_1 C) --> % 12.31/11.82 bnd_k2_cat_1 C D = bnd_k1_mcart_1 (bnd_k1_mcart_1 D) & % 12.31/11.82 bnd_k3_cat_1 C D = % 12.31/11.82 bnd_k2_mcart_1 (bnd_k1_mcart_1 D))) & % 12.31/11.82 (ALL D. % 12.31/11.82 bnd_m1_subset_1 D (bnd_u2_cat_1 C) --> % 12.31/11.82 (ALL E. % 12.31/11.82 bnd_m1_subset_1 E (bnd_u2_cat_1 C) --> % 12.31/11.82 bnd_k2_cat_1 C E = bnd_k3_cat_1 C D --> % 12.31/11.82 bnd_r2_hidden (bnd_k13_cat_2 C C E D) % 12.31/11.82 (bnd_k1_relat_1 (bnd_u5_cat_1 C))))) & % 12.31/11.82 (ALL D. % 12.31/11.82 bnd_m1_subset_1 D (bnd_u2_cat_1 C) --> % 12.31/11.82 (ALL E. % 12.31/11.82 bnd_m1_subset_1 E (bnd_u2_cat_1 C) --> % 12.31/11.82 ~ (bnd_r2_hidden (bnd_k13_cat_2 C C E D) % 12.31/11.82 (bnd_k1_relat_1 (bnd_u5_cat_1 C)) & % 12.31/11.82 (ALL F. % 12.31/11.82 bnd_m2_cat_1 F A B --> % 12.31/11.82 (ALL G. % 12.31/11.82 bnd_m2_cat_1 G A B --> % 12.31/11.82 (ALL H. % 12.31/11.82 bnd_m2_cat_1 H A B --> % 12.31/11.82 (ALL I. % 12.31/11.82 bnd_m2_nattra_1 I A B F G --> % 12.31/11.82 (ALL J. % 12.31/11.82 bnd_m2_nattra_1 J A B G H --> % 12.31/11.82 ~ ((D = bnd_k4_tarski (bnd_k4_tarski F G) I & % 12.31/11.82 E = bnd_k4_tarski (bnd_k4_tarski G H) J) & % 12.31/11.82 bnd_k1_funct_1 (bnd_u5_cat_1 C) (bnd_k13_cat_2 C C E D) = % 12.31/11.82 bnd_k4_tarski (bnd_k4_tarski F H) % 12.31/11.82 (bnd_k8_nattra_1 A B F G H I J))))))))))) & % 12.31/11.82 (ALL D. % 12.31/11.82 bnd_m1_subset_1 D (bnd_u1_cat_1 C) --> % 12.31/11.82 (ALL E. % 12.31/11.82 bnd_m2_cat_1 E A B --> % 12.31/11.82 E = D --> % 12.31/11.82 bnd_k10_cat_1 C D = % 12.31/11.82 bnd_k4_tarski (bnd_k4_tarski E E) % 12.31/11.82 (bnd_k7_nattra_1 A B E)))))); % 12.31/11.82 ALL A B. bnd_k2_tarski A B = bnd_k2_tarski B A; % 12.31/11.82 ALL A B C. % 12.31/11.82 bnd_m1_subset_1 C (bnd_k1_zfmisc_1 (bnd_k2_zfmisc_1 A B)) --> % 12.31/11.82 bnd_v1_relat_1 C; % 12.31/11.82 ALL A B. bnd_r2_hidden A B --> ~ bnd_r2_hidden B A; % 12.31/11.82 ALL A. % 12.31/11.82 bnd_l1_cat_1 A --> % 12.31/11.82 bnd_v1_cat_1 A --> % 12.31/11.82 A = % 12.31/11.82 bnd_g1_cat_1 (bnd_u1_cat_1 A) (bnd_u2_cat_1 A) (bnd_u3_cat_1 A) % 12.31/11.82 (bnd_u4_cat_1 A) (bnd_u5_cat_1 A) (bnd_u6_cat_1 A) |] % 12.31/11.82 ==> bnd_v2_cat_1 A & bnd_l1_cat_1 A --> % 12.31/11.82 (ALL B. % 12.31/11.82 bnd_v2_cat_1 B & bnd_l1_cat_1 B --> % 12.31/11.82 (ALL C. % 12.31/11.82 bnd_v2_cat_1 C & bnd_l1_cat_1 C --> % 12.31/11.82 (ALL D. % 12.31/11.82 bnd_m2_cat_1 D (bnd_k11_cat_2 A B) C --> % 12.31/11.82 bnd_r4_nattra_1 (bnd_u1_cat_1 A) % 12.31/11.82 (bnd_u2_cat_1 (bnd_k12_nattra_1 B C)) (bnd_u1_cat_1 A) % 12.31/11.82 (bnd_u2_cat_1 (bnd_k12_nattra_1 B C)) % 12.31/11.82 (bnd_k7_nattra_1 A (bnd_k12_nattra_1 B C) % 12.31/11.82 (bnd_k5_isocat_2 A B C D)) % 12.31/11.82 (bnd_k6_isocat_2 A B C D D % 12.31/11.82 (bnd_k7_nattra_1 (bnd_k11_cat_2 A B) C D))))) % 12.31/11.82 Adding axioms... % 12.31/11.82 Typedef.type_definition_def % 42.64/42.13 ...done. % 42.64/42.17 Ground types: ?'b, TPTP_Interpret.ind % 42.64/42.17 Translating term (sizes: 1, 1) ... % 62.20/61.61 Invoking SAT solver... % 62.20/61.61 No model exists. % 62.20/61.61 Translating term (sizes: 2, 1) ... % 82.44/81.82 Invoking SAT solver... % 82.44/81.82 No model exists. % 82.44/81.82 Translating term (sizes: 1, 2) ... %------------------------------------------------------------------------------