%------------------------------------------------------------------------------ % File : Fiesta---2 % Problem : SEU323-10 : TPTP v8.1.0. Released v7.3.0. % Transfm : none % Format : dedam % Command : fiesta-wrapper %s % Computer : n032.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 : 600s % DateTime : Tue Jul 19 09:39:01 EDT 2022 % Result : Unsatisfiable 12.67s 13.05s % Output : CNFRefutation 12.67s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.05/0.09 % Problem : SEU323-10 : TPTP v8.1.0. Released v7.3.0. % 0.05/0.09 % Command : fiesta-wrapper %s % 0.08/0.28 % Computer : n032.cluster.edu % 0.08/0.28 % Model : x86_64 x86_64 % 0.08/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.28 % Memory : 8042.1875MB % 0.08/0.28 % OS : Linux 3.10.0-693.el7.x86_64 % 0.08/0.28 % CPULimit : 300 % 0.08/0.28 % WCLimit : 600 % 0.08/0.28 % DateTime : Sun Jun 19 18:48:03 EDT 2022 % 0.08/0.28 % CPUTime : % 12.67/13.05 Theorem Proved. % 12.67/13.05 % SZS status Unsatisfiable % 12.67/13.05 % SZS output start CNFRefutation % 12.67/13.05 [1=axiom,[], % 12.67/13.05 element(sK1_t51_tops_1_B,powerset(the_carrier(sK2_t51_tops_1_A))) = true]. % 12.67/13.05 [2=axiom,[], % 12.67/13.05 topological_space(sK2_t51_tops_1_A) = true]. % 12.67/13.05 [3=axiom,[], % 12.67/13.05 top_str(sK2_t51_tops_1_A) = true]. % 12.67/13.05 [4=axiom,[], % 12.67/13.05 ifeq2(element(X10,powerset(the_carrier(X11))),true,ifeq2(top_str(X11),true,subset_complement(the_carrier(X11),topstr_closure(X11,subset_complement(the_carrier(X11),X10))),interior(X11,X10)),interior(X11,X10)) = interior(X11,X10)]. % 12.67/13.05 [14=axiom,[], % 12.67/13.05 ifeq(element(X10,powerset(the_carrier(X11))),true,ifeq(topological_space(X11),true,ifeq(top_str(X11),true,closed_subset(topstr_closure(X11,X10),X11),true),true),true) = true]. % 12.67/13.05 [15=axiom,[], % 12.67/13.05 ifeq(element(X10,powerset(the_carrier(X11))),true,ifeq(top_str(X11),true,element(topstr_closure(X11,X10),powerset(the_carrier(X11))),true),true) = true]. % 12.67/13.05 [16=axiom,[], % 12.67/13.05 ifeq(element(X10,powerset(X11)),true,element(subset_complement(X11,X10),powerset(X11)),true) = true]. % 12.67/13.05 [22=axiom,[], % 12.67/13.05 ifeq(element(X10,powerset(the_carrier(X11))),true,ifeq(closed_subset(X10,X11),true,ifeq(topological_space(X11),true,ifeq(top_str(X11),true,open_subset(subset_complement(the_carrier(X11),X10),X11),true),true),true),true) = true]. % 12.67/13.05 [23=axiom,[], % 12.67/13.05 ifeq(X10,X10,X11,X12) = X11]. % 12.67/13.05 [24=axiom,[], % 12.67/13.05 ifeq2(X10,X10,X11,X12) = X11]. % 12.67/13.05 [25=axiom,[], % 12.67/13.05 thtop(X10,X10) = thmfalse]. % 12.67/13.05 [26=axiom,[], % 12.67/13.05 thtop(open_subset(interior(sK2_t51_tops_1_A,sK1_t51_tops_1_B),sK2_t51_tops_1_A),true) = thmtrue]. % 12.67/13.05 [56=param(16,1),[23], % 12.67/13.05 element(subset_complement(the_carrier(sK2_t51_tops_1_A),sK1_t51_tops_1_B),powerset(the_carrier(sK2_t51_tops_1_A))) = true]. % 12.67/13.05 [136=param(15,56),[3,23,23], % 12.67/13.05 element(topstr_closure(sK2_t51_tops_1_A,subset_complement(the_carrier(sK2_t51_tops_1_A),sK1_t51_tops_1_B)),powerset(the_carrier(sK2_t51_tops_1_A))) = true]. % 12.67/13.05 [256=param(14,56),[2,3,23,23,23], % 12.67/13.05 closed_subset(topstr_closure(sK2_t51_tops_1_A,subset_complement(the_carrier(sK2_t51_tops_1_A),sK1_t51_tops_1_B)),sK2_t51_tops_1_A) = true]. % 12.67/13.05 [1497=param(4,1),[3,24,24], % 12.67/13.05 subset_complement(the_carrier(sK2_t51_tops_1_A),topstr_closure(sK2_t51_tops_1_A,subset_complement(the_carrier(sK2_t51_tops_1_A),sK1_t51_tops_1_B))) = interior(sK2_t51_tops_1_A,sK1_t51_tops_1_B)]. % 12.67/13.05 [9190=param(22,2),[3,23,23], % 12.67/13.05 ifeq(element(X10,powerset(the_carrier(sK2_t51_tops_1_A))),true,ifeq(closed_subset(X10,sK2_t51_tops_1_A),true,open_subset(subset_complement(the_carrier(sK2_t51_tops_1_A),X10),sK2_t51_tops_1_A),true),true) = true]. % 12.67/13.05 [14333=param(9190,136),[256,1497,23,23], % 12.67/13.05 open_subset(interior(sK2_t51_tops_1_A,sK1_t51_tops_1_B),sK2_t51_tops_1_A) = true]. % 12.67/13.05 [14376=param(26,14333),[25], % 12.67/13.05 thmtrue = thmfalse]. % 12.67/13.05 % SZS output end CNFRefutation % 12.67/13.05 Space: 60294 KB %------------------------------------------------------------------------------