%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SEU247+1 : TPTP v8.2.0. Released v3.3.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n028.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 15:02:02 EDT 2024 % Result : Theorem 0.55s 0.85s % Output : CNFRefutation 0.56s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.13/0.13 % Problem : SEU247+1 : TPTP v8.2.0. Released v3.3.0. % 0.13/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.13/0.34 % Computer : n028.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 21 14:45:39 EDT 2024 % 0.13/0.34 % CPUTime : % 0.51/0.58 start to proof:theBenchmark % 0.55/0.84 %------------------------------------------- % 0.55/0.84 % File :CSE---1.7 % 0.55/0.84 % Problem :theBenchmark % 0.55/0.84 % Transform :cnf % 0.55/0.84 % Format :tptp:raw % 0.55/0.84 % Command :java -jar mcs_scs.jar %d %s % 0.55/0.84 % 0.55/0.84 % Result :Theorem 0.220000s % 0.55/0.84 % Output :CNFRefutation 0.220000s % 0.55/0.84 %------------------------------------------- % 0.55/0.84 %------------------------------------------------------------------------------ % 0.55/0.84 % File : SEU247+1 : TPTP v8.2.0. Released v3.3.0. % 0.55/0.84 % Domain : Set theory % 0.55/0.84 % Problem : MPTP bushy problem t18_wellord1 % 0.55/0.84 % Version : [Urb07] axioms : Especial. % 0.55/0.84 % English : % 0.55/0.84 % 0.55/0.84 % Refs : [Ban01] Bancerek et al. (2001), On the Characterizations of Co % 0.55/0.84 % : [Urb07] Urban (2006), Email to G. Sutcliffe % 0.55/0.84 % Source : [Urb07] % 0.55/0.84 % Names : bushy-t18_wellord1 [Urb07] % 0.55/0.84 % 0.55/0.84 % Status : Theorem % 0.55/0.84 % Rating : 0.11 v8.1.0, 0.14 v7.5.0, 0.16 v7.4.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.17 v6.0.0, 0.09 v5.5.0, 0.11 v5.4.0, 0.14 v5.3.0, 0.15 v5.2.0, 0.05 v5.0.0, 0.04 v4.0.0, 0.08 v3.7.0, 0.10 v3.5.0, 0.11 v3.3.0 % 0.55/0.84 % Syntax : Number of formulae : 11 ( 4 unt; 0 def) % 0.55/0.84 % Number of atoms : 18 ( 6 equ) % 0.55/0.84 % Maximal formula atoms : 2 ( 1 avg) % 0.55/0.84 % Number of connectives : 7 ( 0 ~; 0 |; 0 &) % 0.55/0.84 % ( 0 <=>; 7 =>; 0 <=; 0 <~>) % 0.55/0.84 % Maximal formula depth : 5 ( 3 avg) % 0.55/0.84 % Maximal term depth : 3 ( 1 avg) % 0.55/0.84 % Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty) % 0.55/0.84 % Number of functors : 5 ( 5 usr; 0 con; 2-2 aty) % 0.55/0.84 % Number of variables : 19 ( 19 !; 0 ?) % 0.55/0.84 % SPC : FOF_THM_RFO_SEQ % 0.55/0.84 % 0.55/0.84 % Comments : Translated by MPTP 0.2 from the original problem in the Mizar % 0.55/0.84 % library, www.mizar.org % 0.55/0.84 %------------------------------------------------------------------------------ % 0.55/0.84 fof(commutativity_k3_xboole_0,axiom, % 0.55/0.84 ! [A,B] : set_intersection2(A,B) = set_intersection2(B,A) ). % 0.55/0.84 % 0.55/0.84 fof(d6_wellord1,axiom, % 0.55/0.84 ! [A] : % 0.55/0.84 ( relation(A) % 0.55/0.84 => ! [B] : relation_restriction(A,B) = set_intersection2(A,cartesian_product2(B,B)) ) ). % 0.55/0.84 % 0.55/0.84 fof(dt_k2_wellord1,axiom, % 0.55/0.84 ! [A,B] : % 0.55/0.84 ( relation(A) % 0.55/0.84 => relation(relation_restriction(A,B)) ) ). % 0.55/0.84 % 0.55/0.84 fof(dt_k2_zfmisc_1,axiom, % 0.55/0.84 $true ). % 0.55/0.84 % 0.55/0.84 fof(dt_k3_xboole_0,axiom, % 0.55/0.84 $true ). % 0.55/0.85 % 0.55/0.85 fof(dt_k7_relat_1,axiom, % 0.55/0.85 ! [A,B] : % 0.55/0.85 ( relation(A) % 0.55/0.85 => relation(relation_dom_restriction(A,B)) ) ). % 0.55/0.85 % 0.55/0.85 fof(dt_k8_relat_1,axiom, % 0.55/0.85 ! [A,B] : % 0.55/0.85 ( relation(B) % 0.55/0.85 => relation(relation_rng_restriction(A,B)) ) ). % 0.55/0.85 % 0.55/0.85 fof(idempotence_k3_xboole_0,axiom, % 0.55/0.85 ! [A,B] : set_intersection2(A,A) = A ). % 0.55/0.85 % 0.55/0.85 fof(t140_relat_1,axiom, % 0.55/0.85 ! [A,B,C] : % 0.55/0.85 ( relation(C) % 0.55/0.85 => relation_dom_restriction(relation_rng_restriction(A,C),B) = relation_rng_restriction(A,relation_dom_restriction(C,B)) ) ). % 0.55/0.85 % 0.55/0.85 fof(t17_wellord1,axiom, % 0.55/0.85 ! [A,B] : % 0.55/0.85 ( relation(B) % 0.55/0.85 => relation_restriction(B,A) = relation_dom_restriction(relation_rng_restriction(A,B),A) ) ). % 0.55/0.85 % 0.55/0.85 fof(t18_wellord1,conjecture, % 0.55/0.85 ! [A,B] : % 0.55/0.85 ( relation(B) % 0.55/0.85 => relation_restriction(B,A) = relation_rng_restriction(A,relation_dom_restriction(B,A)) ) ). % 0.55/0.85 % 0.55/0.85 %------------------------------------------------------------------------------ % 0.55/0.85 %------------------------------------------- % 0.55/0.85 % Proof found % 0.55/0.85 % SZS status Theorem for theBenchmark % 0.55/0.85 % SZS output start Proof % 0.55/0.85 %ClaNum:24(EqnAxiom:14) % 0.55/0.85 %VarNum:35(SingletonVarNum:16) % 0.55/0.85 %MaxLitNum:2 % 0.55/0.85 %MaxfuncDepth:2 % 0.55/0.85 %SharedTerms:7 % 0.55/0.85 %goalClause: 15 18 % 0.55/0.85 %singleGoalClaCount:2 % 0.55/0.85 [15]P1(a1) % 0.55/0.85 [18]~E(f6(a2,f5(a1,a2)),f7(a1,a2)) % 0.55/0.85 [16]E(f4(x161,x161),x161) % 0.55/0.85 [17]E(f4(x171,x172),f4(x172,x171)) % 0.55/0.85 [19]~P1(x191)+P1(f7(x191,x192)) % 0.55/0.85 [20]~P1(x201)+P1(f5(x201,x202)) % 0.55/0.85 [21]~P1(x212)+P1(f6(x211,x212)) % 0.55/0.85 [22]~P1(x221)+E(f4(x221,f3(x222,x222)),f7(x221,x222)) % 0.55/0.85 [23]~P1(x232)+E(f5(f6(x231,x232),x231),f7(x232,x231)) % 0.55/0.85 [24]~P1(x242)+E(f6(x241,f5(x242,x243)),f5(f6(x241,x242),x243)) % 0.55/0.85 %EqnAxiom % 0.55/0.85 [1]E(x11,x11) % 0.55/0.85 [2]E(x22,x21)+~E(x21,x22) % 0.55/0.85 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 0.55/0.85 [4]~E(x41,x42)+E(f4(x41,x43),f4(x42,x43)) % 0.55/0.85 [5]~E(x51,x52)+E(f4(x53,x51),f4(x53,x52)) % 0.55/0.85 [6]~E(x61,x62)+E(f5(x61,x63),f5(x62,x63)) % 0.55/0.85 [7]~E(x71,x72)+E(f5(x73,x71),f5(x73,x72)) % 0.55/0.85 [8]~E(x81,x82)+E(f6(x81,x83),f6(x82,x83)) % 0.55/0.85 [9]~E(x91,x92)+E(f6(x93,x91),f6(x93,x92)) % 0.55/0.85 [10]~E(x101,x102)+E(f7(x101,x103),f7(x102,x103)) % 0.56/0.85 [11]~E(x111,x112)+E(f7(x113,x111),f7(x113,x112)) % 0.56/0.85 [12]~E(x121,x122)+E(f3(x121,x123),f3(x122,x123)) % 0.56/0.85 [13]~E(x131,x132)+E(f3(x133,x131),f3(x133,x132)) % 0.56/0.85 [14]~P1(x141)+P1(x142)+~E(x141,x142) % 0.56/0.85 % 0.56/0.85 %------------------------------------------- % 0.56/0.85 cnf(96,plain, % 0.56/0.85 (E(f7(a1,x961),f5(f6(x961,a1),x961))), % 0.56/0.85 inference(scs_inference,[],[15,2,23])). % 0.56/0.85 cnf(97,plain, % 0.56/0.85 (E(f5(f6(x971,a1),x971),f7(a1,x971))), % 0.56/0.85 inference(scs_inference,[],[96,2])). % 0.56/0.85 cnf(98,plain, % 0.56/0.85 (E(f4(f7(a1,x981),f7(a1,x981)),f5(f6(x981,a1),x981))), % 0.56/0.85 inference(scs_inference,[],[16,96,2,3])). % 0.56/0.85 cnf(106,plain, % 0.56/0.85 ($false), % 0.56/0.85 inference(scs_inference,[],[18,15,97,98,2,3,24]), % 0.56/0.85 ['proof']). % 0.56/0.85 % SZS output end Proof % 0.56/0.85 % Total time :0.220000s %------------------------------------------------------------------------------