%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SET834-2 : 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 : n018.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:39 EDT 2024 % Result : Unsatisfiable 0.59s 0.96s % Output : CNFRefutation 0.59s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.13 % Problem : SET834-2 : TPTP v8.2.0. Released v3.2.0. % 0.07/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.13/0.34 % Computer : n018.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 : Sun Jun 23 13:02:09 EDT 2024 % 0.13/0.35 % CPUTime : % 0.43/0.62 start to proof:theBenchmark % 0.59/0.95 %------------------------------------------- % 0.59/0.95 % File :CSE---1.7 % 0.59/0.95 % Problem :theBenchmark % 0.59/0.95 % Transform :cnf % 0.59/0.95 % Format :tptp:raw % 0.59/0.95 % Command :java -jar mcs_scs.jar %d %s % 0.59/0.95 % 0.59/0.95 % Result :Theorem 0.280000s % 0.59/0.95 % Output :CNFRefutation 0.280000s % 0.59/0.95 %------------------------------------------- % 0.59/0.95 %------------------------------------------------------------------------------ % 0.59/0.95 % File : SET834-2 : TPTP v8.2.0. Released v3.2.0. % 0.59/0.95 % Domain : Set Theory % 0.59/0.95 % Problem : Problem about set theory % 0.59/0.95 % Version : [Pau06] axioms : Reduced > Especial. % 0.59/0.95 % English : % 0.59/0.95 % 0.59/0.95 % Refs : [Pau06] Paulson (2006), Email to G. Sutcliffe % 0.59/0.95 % Source : [Pau06] % 0.59/0.95 % Names : % 0.59/0.95 % 0.59/0.95 % Status : Unsatisfiable % 0.59/0.95 % Rating : 0.00 v7.1.0, 0.17 v7.0.0, 0.25 v6.3.0, 0.14 v6.2.0, 0.11 v6.1.0, 0.14 v5.5.0, 0.25 v5.4.0, 0.20 v5.2.0, 0.10 v5.1.0, 0.18 v5.0.0, 0.36 v4.1.0, 0.00 v4.0.1, 0.20 v4.0.0, 0.29 v3.7.0, 0.43 v3.4.0, 0.25 v3.3.0, 0.33 v3.2.0 % 0.59/0.95 % Syntax : Number of clauses : 10 ( 3 unt; 2 nHn; 7 RR) % 0.59/0.95 % Number of literals : 20 ( 0 equ; 10 neg) % 0.59/0.95 % Maximal clause size : 3 ( 2 avg) % 0.59/0.95 % Maximal term depth : 2 ( 1 avg) % 0.59/0.95 % Number of predicates : 2 ( 2 usr; 0 prp; 3-3 aty) % 0.59/0.95 % Number of functors : 8 ( 8 usr; 5 con; 0-3 aty) % 0.59/0.95 % Number of variables : 23 ( 2 sgn) % 0.59/0.95 % SPC : CNF_UNS_RFO_NEQ_NHN % 0.59/0.95 % 0.59/0.95 % Comments : The problems in the [Pau06] collection each have very many axioms, % 0.59/0.95 % of which only a small selection are required for the refutation. % 0.59/0.95 % The mission is to find those few axioms, after which a refutation % 0.59/0.95 % can be quite easily found. This version has only the necessary % 0.59/0.95 % axioms. % 0.59/0.95 %------------------------------------------------------------------------------ % 0.59/0.95 cnf(cls_Set_OUnCI_0,axiom, % 0.59/0.95 ( ~ c_in(V_c,V_B,T_a) % 0.59/0.95 | c_in(V_c,c_union(V_A,V_B,T_a),T_a) ) ). % 0.59/0.95 % 0.59/0.95 cnf(cls_Set_OUnCI_1,axiom, % 0.59/0.95 ( ~ c_in(V_c,V_A,T_a) % 0.59/0.95 | c_in(V_c,c_union(V_A,V_B,T_a),T_a) ) ). % 0.59/0.95 % 0.59/0.95 cnf(cls_Set_OUnE_0,axiom, % 0.59/0.96 ( ~ c_in(V_c,c_union(V_A,V_B,T_a),T_a) % 0.59/0.96 | c_in(V_c,V_B,T_a) % 0.59/0.96 | c_in(V_c,V_A,T_a) ) ). % 0.59/0.96 % 0.59/0.96 cnf(cls_Set_OsubsetD_0,axiom, % 0.59/0.96 ( ~ c_in(V_c,V_A,T_a) % 0.59/0.96 | ~ c_lessequals(V_A,V_B,tc_set(T_a)) % 0.59/0.96 | c_in(V_c,V_B,T_a) ) ). % 0.59/0.96 % 0.59/0.96 cnf(cls_Set_OsubsetI_0,axiom, % 0.59/0.96 ( c_in(c_Main_OsubsetI__1(V_A,V_B,T_a),V_A,T_a) % 0.59/0.96 | c_lessequals(V_A,V_B,tc_set(T_a)) ) ). % 0.59/0.96 % 0.59/0.96 cnf(cls_Set_OsubsetI_1,axiom, % 0.59/0.96 ( ~ c_in(c_Main_OsubsetI__1(V_A,V_B,T_a),V_B,T_a) % 0.59/0.96 | c_lessequals(V_A,V_B,tc_set(T_a)) ) ). % 0.59/0.96 % 0.59/0.96 cnf(cls_conjecture_2,negated_conjecture, % 0.59/0.96 c_in(v_x,v_X,t_a) ). % 0.59/0.96 % 0.59/0.96 cnf(cls_conjecture_3,negated_conjecture, % 0.59/0.96 ~ c_in(v_x,v_Z,t_a) ). % 0.59/0.96 % 0.59/0.96 cnf(cls_conjecture_4,negated_conjecture, % 0.59/0.96 ~ c_in(v_x,v_Y,t_a) ). % 0.59/0.96 % 0.59/0.96 cnf(cls_conjecture_5,negated_conjecture, % 0.59/0.96 ( c_lessequals(v_X,V_U,tc_set(t_a)) % 0.59/0.96 | ~ c_lessequals(v_Z,V_U,tc_set(t_a)) % 0.59/0.96 | ~ c_lessequals(v_Y,V_U,tc_set(t_a)) ) ). % 0.59/0.96 % 0.59/0.96 %------------------------------------------------------------------------------ % 0.59/0.96 %------------------------------------------- % 0.59/0.96 % Proof found % 0.59/0.96 % SZS status Theorem for theBenchmark % 0.59/0.96 % SZS output start Proof % 0.59/0.96 %ClaNum:10(EqnAxiom:0) % 0.59/0.96 %VarNum:55(SingletonVarNum:23) % 0.59/0.96 %MaxLitNum:3 % 0.59/0.96 %MaxfuncDepth:1 % 0.59/0.96 %SharedTerms:9 % 0.59/0.96 %goalClause: 1 2 3 5 % 0.59/0.96 %singleGoalClaCount:3 % 0.59/0.96 [1]P1(a1,a2,a3) % 0.59/0.96 [2]~P1(a1,a7,a3) % 0.59/0.96 [3]~P1(a1,a8,a3) % 0.59/0.96 [4]P1(f4(x41,x42,x43),x41,x43)+P2(x41,x42,f6(x43)) % 0.59/0.96 [9]~P1(f4(x91,x92,x93),x92,x93)+P2(x91,x92,f6(x93)) % 0.59/0.96 [7]~P1(x71,x73,x74)+P1(x71,f5(x72,x73,x74),x74) % 0.59/0.96 [8]~P1(x81,x82,x84)+P1(x81,f5(x82,x83,x84),x84) % 0.59/0.96 [5]~P2(a7,x51,f6(a3))+~P2(a8,x51,f6(a3))+P2(a2,x51,f6(a3)) % 0.59/0.96 [6]P1(x61,x62,x63)+~P1(x61,x64,x63)+~P2(x64,x62,f6(x63)) % 0.59/0.96 [10]P1(x101,x102,x103)+P1(x101,x104,x103)+~P1(x101,f5(x104,x102,x103),x103) % 0.59/0.96 %EqnAxiom % 0.59/0.96 % 0.59/0.96 %------------------------------------------- % 0.59/0.96 cnf(107,plain, % 0.59/0.96 (~P1(f4(x1071,f5(x1072,x1073,x1074),x1074),x1073,x1074)+P2(x1071,f5(x1072,x1073,x1074),f6(x1074))), % 0.59/0.96 inference(scs_inference,[],[7,9])). % 0.59/0.96 cnf(108,plain, % 0.59/0.96 (P2(x1081,f5(x1082,x1081,x1083),f6(x1083))), % 0.59/0.96 inference(scs_inference,[],[107,4])). % 0.59/0.96 cnf(109,plain, % 0.59/0.96 (P2(a2,f5(x1091,a8,a3),f6(a3))+~P2(a7,f5(x1091,a8,a3),f6(a3))), % 0.59/0.96 inference(scs_inference,[],[108,5])). % 0.59/0.96 cnf(112,plain, % 0.59/0.96 (P1(a1,f5(x1121,a8,a3),a3)+~P2(a7,f5(x1121,a8,a3),f6(a3))), % 0.59/0.96 inference(scs_inference,[],[1,108,5,6])). % 0.59/0.96 cnf(115,plain, % 0.59/0.96 (P1(f4(a7,f5(x1151,a8,a3),a3),a7,a3)+P1(a1,f5(x1151,a8,a3),a3)), % 0.59/0.96 inference(scs_inference,[],[112,4])). % 0.59/0.96 cnf(116,plain, % 0.59/0.96 (~P1(f4(a7,f5(x1161,a8,a3),a3),f5(x1161,a8,a3),a3)+P2(a2,f5(x1161,a8,a3),f6(a3))), % 0.59/0.96 inference(scs_inference,[],[109,9])). % 0.59/0.96 cnf(117,plain, % 0.59/0.96 (P1(f4(a7,f5(a7,a8,a3),a3),a7,a3)), % 0.59/0.96 inference(scs_inference,[],[3,2,115,10])). % 0.59/0.96 cnf(118,plain, % 0.59/0.96 (P2(a2,f5(a7,a8,a3),f6(a3))), % 0.59/0.96 inference(scs_inference,[],[117,116,8])). % 0.59/0.96 cnf(121,plain, % 0.59/0.96 ($false), % 0.59/0.96 inference(scs_inference,[],[2,3,1,118,6,10]), % 0.59/0.96 ['proof']). % 0.59/0.96 % SZS output end Proof % 0.59/0.96 % Total time :0.280000s %------------------------------------------------------------------------------