%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SET901+1 : TPTP v8.2.0. Released v3.2.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n027.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 : Mon Jun 24 14:22:55 EDT 2024 % Result : Theorem 2.65s 2.70s % Output : CNFRefutation 2.68s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SET901+1 : TPTP v8.2.0. Released v3.2.0. % 0.07/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n027.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Sun Jun 23 14:43:54 EDT 2024 % 0.12/0.33 % CPUTime : % 0.19/0.57 start to proof:theBenchmark % 2.65/2.69 %------------------------------------------- % 2.65/2.69 % File :CSE---1.7 % 2.65/2.69 % Problem :theBenchmark % 2.65/2.69 % Transform :cnf % 2.65/2.69 % Format :tptp:raw % 2.65/2.69 % Command :java -jar mcs_scs.jar %d %s % 2.65/2.69 % 2.65/2.69 % Result :Theorem 2.090000s % 2.65/2.69 % Output :CNFRefutation 2.090000s % 2.65/2.69 %------------------------------------------- % 2.65/2.70 %------------------------------------------------------------------------------ % 2.65/2.70 % File : SET901+1 : TPTP v8.2.0. Released v3.2.0. % 2.65/2.70 % Domain : Set theory % 2.65/2.70 % Problem : Basic properties of sets, theorem 42 % 2.65/2.70 % Version : [Urb06] axioms : Especial. % 2.65/2.70 % English : subset(A,unordered_pair(B,C)) <=> ~ ( A != empty_set & % 2.65/2.70 % A != singleton(B) & A != singleton(C) & A != unordered_pair(B,C) ) % 2.65/2.70 % 2.65/2.70 % Refs : [Byl90] Bylinski (1990), Some Basic Properties of Sets % 2.65/2.70 % : [Urb06] Urban (2006), Email to G. Sutcliffe % 2.65/2.70 % Source : [Urb06] % 2.65/2.70 % Names : zfmisc_1__t42_zfmisc_1 [Urb06] % 2.65/2.70 % 2.65/2.70 % Status : Theorem % 2.65/2.70 % Rating : 0.11 v8.2.0, 0.08 v7.5.0, 0.09 v7.4.0, 0.10 v7.2.0, 0.07 v7.1.0, 0.09 v7.0.0, 0.07 v6.4.0, 0.12 v6.3.0, 0.08 v6.2.0, 0.12 v6.1.0, 0.13 v6.0.0, 0.09 v5.5.0, 0.07 v5.3.0, 0.15 v5.2.0, 0.00 v4.1.0, 0.04 v4.0.1, 0.09 v4.0.0, 0.08 v3.7.0, 0.00 v3.4.0, 0.05 v3.3.0, 0.07 v3.2.0 % 2.65/2.70 % Syntax : Number of formulae : 7 ( 5 unt; 0 def) % 2.65/2.70 % Number of atoms : 15 ( 9 equ) % 2.65/2.70 % Maximal formula atoms : 5 ( 2 avg) % 2.65/2.70 % Number of connectives : 19 ( 11 ~; 0 |; 6 &) % 2.65/2.70 % ( 2 <=>; 0 =>; 0 <=; 0 <~>) % 2.65/2.70 % Maximal formula depth : 10 ( 5 avg) % 2.65/2.70 % Maximal term depth : 2 ( 1 avg) % 2.65/2.70 % Number of predicates : 3 ( 2 usr; 0 prp; 1-2 aty) % 2.65/2.70 % Number of functors : 3 ( 3 usr; 1 con; 0-2 aty) % 2.65/2.70 % Number of variables : 12 ( 10 !; 2 ?) % 2.65/2.70 % SPC : FOF_THM_RFO_SEQ % 2.65/2.70 % 2.65/2.70 % Comments : Translated by MPTP 0.2 from the original problem in the Mizar % 2.65/2.70 % library, www.mizar.org % 2.65/2.70 %------------------------------------------------------------------------------ % 2.65/2.70 fof(commutativity_k2_tarski,axiom, % 2.65/2.70 ! [A,B] : unordered_pair(A,B) = unordered_pair(B,A) ). % 2.65/2.70 % 2.65/2.70 fof(reflexivity_r1_tarski,axiom, % 2.65/2.70 ! [A,B] : subset(A,A) ). % 2.65/2.70 % 2.65/2.70 fof(fc1_xboole_0,axiom, % 2.65/2.70 empty(empty_set) ). % 2.65/2.70 % 2.65/2.70 fof(rc1_xboole_0,axiom, % 2.65/2.70 ? [A] : empty(A) ). % 2.65/2.70 % 2.65/2.70 fof(rc2_xboole_0,axiom, % 2.65/2.70 ? [A] : ~ empty(A) ). % 2.65/2.70 % 2.65/2.70 fof(t42_zfmisc_1,conjecture, % 2.65/2.70 ! [A,B,C] : % 2.65/2.70 ( subset(A,unordered_pair(B,C)) % 2.65/2.70 <=> ~ ( A != empty_set % 2.65/2.70 & A != singleton(B) % 2.65/2.70 & A != singleton(C) % 2.65/2.70 & A != unordered_pair(B,C) ) ) ). % 2.65/2.70 % 2.65/2.70 fof(l46_zfmisc_1,axiom, % 2.65/2.70 ! [A,B,C] : % 2.65/2.70 ( subset(A,unordered_pair(B,C)) % 2.65/2.70 <=> ~ ( A != empty_set % 2.65/2.70 & A != singleton(B) % 2.65/2.70 & A != singleton(C) % 2.65/2.70 & A != unordered_pair(B,C) ) ) ). % 2.65/2.70 % 2.65/2.70 %------------------------------------------------------------------------------ % 2.65/2.70 %------------------------------------------- % 2.65/2.70 % Proof found % 2.65/2.70 % SZS status Theorem for theBenchmark % 2.65/2.70 % SZS output start Proof % 2.65/2.70 %ClaNum:24(EqnAxiom:9) % 2.65/2.70 %VarNum:37(SingletonVarNum:18) % 2.65/2.70 %MaxLitNum:5 % 2.65/2.70 %MaxfuncDepth:1 % 2.65/2.70 %SharedTerms:22 % 2.65/2.70 %goalClause: 18 19 20 21 23 % 2.65/2.70 [10]P1(a1) % 2.65/2.70 [11]P1(a2) % 2.65/2.70 [14]~P1(a4) % 2.65/2.70 [12]P2(x121,x121) % 2.65/2.70 [13]E(f3(x131,x132),f3(x132,x131)) % 2.65/2.70 [19]~E(a1,a6)+~P2(a6,f3(a7,a8)) % 2.65/2.70 [20]~P2(a6,f3(a7,a8))+~E(f5(a7),a6) % 2.65/2.70 [21]~P2(a6,f3(a7,a8))+~E(f5(a8),a6) % 2.65/2.70 [23]~E(f3(a7,a8),a6)+~P2(a6,f3(a7,a8)) % 2.65/2.70 [15]~E(x151,a1)+P2(x151,f3(x152,x153)) % 2.65/2.70 [16]~E(x161,f5(x163))+P2(x161,f3(x162,x163)) % 2.65/2.70 [17]~E(x171,f5(x172))+P2(x171,f3(x172,x173)) % 2.65/2.70 [22]P2(x221,f3(x222,x223))+~E(x221,f3(x222,x223)) % 2.65/2.70 [18]E(a1,a6)+P2(a6,f3(a7,a8))+E(f5(a7),a6)+E(f5(a8),a6)+E(f3(a7,a8),a6) % 2.65/2.70 [24]E(x241,f3(x243,x242))+~P2(x241,f3(x243,x242))+E(x241,a1)+E(x241,f5(x242))+E(x241,f5(x243)) % 2.65/2.70 %EqnAxiom % 2.65/2.70 [1]E(x11,x11) % 2.65/2.70 [2]E(x22,x21)+~E(x21,x22) % 2.65/2.70 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 2.65/2.70 [4]~E(x41,x42)+E(f3(x41,x43),f3(x42,x43)) % 2.65/2.70 [5]~E(x51,x52)+E(f3(x53,x51),f3(x53,x52)) % 2.65/2.70 [6]~E(x61,x62)+E(f5(x61),f5(x62)) % 2.65/2.70 [7]~P1(x71)+P1(x72)+~E(x71,x72) % 2.65/2.70 [8]P2(x82,x83)+~E(x81,x82)+~P2(x81,x83) % 2.65/2.70 [9]P2(x93,x92)+~E(x91,x92)+~P2(x93,x91) % 2.65/2.70 % 2.65/2.70 %------------------------------------------- % 2.65/2.70 cnf(25,plain, % 2.65/2.70 (P2(a1,f3(x251,x252))), % 2.65/2.70 inference(equality_inference,[],[15])). % 2.65/2.70 cnf(26,plain, % 2.65/2.70 (P2(f5(x261),f3(x262,x261))), % 2.65/2.70 inference(equality_inference,[],[16])). % 2.65/2.70 cnf(29,plain, % 2.65/2.70 (P2(f3(x291,x292),f3(x292,x291))), % 2.65/2.70 inference(scs_inference,[],[12,13,8])). % 2.65/2.70 cnf(34,plain, % 2.65/2.70 (~E(f5(a8),a6)), % 2.65/2.70 inference(scs_inference,[],[26,8,19,21])). % 2.65/2.70 cnf(37,plain, % 2.65/2.70 (E(a1,a6)+E(f3(a7,a8),a6)+P2(a6,f3(a7,a8))+E(f5(a7),a6)), % 2.65/2.70 inference(scs_inference,[],[34,18])). % 2.65/2.70 cnf(43,plain, % 2.65/2.70 (~E(a1,a6)), % 2.65/2.70 inference(scs_inference,[],[25,8,19])). % 2.65/2.70 cnf(46,plain, % 2.65/2.70 (E(f3(a7,a8),a6)+P2(a6,f3(a7,a8))+E(f5(a7),a6)), % 2.65/2.70 inference(scs_inference,[],[43,37])). % 2.65/2.70 cnf(49,plain, % 2.65/2.70 (~E(a6,f5(a7))+~P2(a6,f3(a7,a8))), % 2.65/2.70 inference(scs_inference,[],[20,2])). % 2.65/2.71 cnf(50,plain, % 2.65/2.71 (~E(x501,f5(a7))+~E(a6,x501)+~P2(a6,f3(a7,a8))), % 2.65/2.71 inference(scs_inference,[],[49,3])). % 2.65/2.71 cnf(51,plain, % 2.65/2.71 (~E(a6,f3(a7,a8))+~P2(a6,f3(a7,a8))), % 2.65/2.71 inference(scs_inference,[],[23,2])). % 2.65/2.71 cnf(52,plain, % 2.65/2.71 (~E(a6,f3(a8,a7))+~P2(a6,f3(a7,a8))), % 2.65/2.71 inference(scs_inference,[],[13,51,3])). % 2.65/2.71 cnf(53,plain, % 2.65/2.71 (~E(f3(a8,a7),a6)+~P2(a6,f3(a7,a8))), % 2.65/2.71 inference(scs_inference,[],[52,2])). % 2.65/2.71 cnf(59,plain, % 2.65/2.71 (P2(a6,f3(a8,a7))+E(f3(a7,a8),a6)+E(f5(a7),a6)), % 2.65/2.71 inference(scs_inference,[],[13,9,46])). % 2.65/2.71 cnf(78,plain, % 2.65/2.71 (~E(f5(a7),x781)+~E(a6,x781)+~P2(a6,f3(a7,a8))), % 2.65/2.71 inference(scs_inference,[],[50,2])). % 2.65/2.71 cnf(84,plain, % 2.65/2.71 (P2(a6,f3(a8,a7))+E(f5(a7),a6)), % 2.65/2.71 inference(scs_inference,[],[29,59,8])). % 2.65/2.71 cnf(96,plain, % 2.65/2.71 (E(a6,f5(a7))+P2(a6,f3(a8,a7))), % 2.65/2.71 inference(scs_inference,[],[2,84])). % 2.65/2.71 cnf(144,plain, % 2.65/2.71 (~E(x1441,a1)+E(a1,a6)+~E(a6,x1441)), % 2.65/2.71 inference(scs_inference,[],[43,2,3])). % 2.65/2.71 cnf(145,plain, % 2.65/2.71 (~E(a6,x1451)+~E(x1451,a1)), % 2.65/2.71 inference(scs_inference,[],[43,144])). % 2.65/2.71 cnf(146,plain, % 2.65/2.71 (~E(a1,x1461)+~E(a6,x1461)), % 2.65/2.71 inference(scs_inference,[],[145,2])). % 2.65/2.71 cnf(361,plain, % 2.65/2.71 (P2(a6,f3(a8,a7))+P2(a6,f3(x3611,a7))), % 2.65/2.71 inference(scs_inference,[],[16,96])). % 2.65/2.71 cnf(362,plain, % 2.65/2.71 (P2(a6,f3(a8,a7))), % 2.65/2.71 inference(factoring_inference,[],[361])). % 2.65/2.71 cnf(363,plain, % 2.65/2.71 (P2(a6,f3(a7,a8))), % 2.68/2.71 inference(scs_inference,[],[362,13,9])). % 2.68/2.71 cnf(369,plain, % 2.68/2.71 (~E(a6,f3(a8,a7))), % 2.68/2.71 inference(scs_inference,[],[362,13,9,20,23,49,51,52])). % 2.68/2.71 cnf(371,plain, % 2.68/2.71 (~E(x3711,f5(a7))+~E(a6,x3711)), % 2.68/2.71 inference(scs_inference,[],[362,13,9,20,23,49,51,52,53,50])). % 2.68/2.71 cnf(377,plain, % 2.68/2.71 (~E(f5(a7),x3771)+~E(a6,x3771)), % 2.68/2.71 inference(scs_inference,[],[363,78])). % 2.68/2.71 cnf(470,plain, % 2.68/2.71 (E(a6,a1)+E(a6,f5(a8))), % 2.68/2.71 inference(scs_inference,[],[369,362,371,24])). % 2.68/2.71 cnf(471,plain, % 2.68/2.71 (E(a6,f5(a8))), % 2.68/2.71 inference(scs_inference,[],[43,470,2])). % 2.68/2.71 cnf(482,plain, % 2.68/2.71 ($false), % 2.68/2.71 inference(scs_inference,[],[34,471,146,371,377,16,17,2]), % 2.68/2.71 ['proof']). % 2.68/2.71 % SZS output end Proof % 2.68/2.71 % Total time :2.090000s %------------------------------------------------------------------------------