%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SET838-2 : TPTP v8.2.0. Released v3.2.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n020.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:40 EDT 2024 % Result : Unsatisfiable 117.09s 118.11s % Output : CNFRefutation 117.15s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SET838-2 : TPTP v8.2.0. Released v3.2.0. % 0.03/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n020.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 18:01:09 EDT 2024 % 0.12/0.33 % CPUTime : % 0.47/0.58 start to proof:theBenchmark % 117.09/118.10 %------------------------------------------- % 117.09/118.10 % File :CSE---1.7 % 117.09/118.10 % Problem :theBenchmark % 117.09/118.10 % Transform :cnf % 117.09/118.10 % Format :tptp:raw % 117.09/118.10 % Command :java -jar mcs_scs.jar %d %s % 117.09/118.10 % 117.09/118.10 % Result :Theorem 116.510000s % 117.09/118.10 % Output :CNFRefutation 116.510000s % 117.09/118.10 %------------------------------------------- % 117.09/118.11 %------------------------------------------------------------------------------ % 117.09/118.11 % File : SET838-2 : TPTP v8.2.0. Released v3.2.0. % 117.09/118.11 % Domain : Set Theory % 117.09/118.11 % Problem : Problem about set theory % 117.09/118.11 % Version : [Pau06] axioms : Reduced > Especial. % 117.09/118.11 % English : % 117.09/118.11 % 117.09/118.11 % Refs : [Pau06] Paulson (2006), Email to G. Sutcliffe % 117.09/118.11 % Source : [Pau06] % 117.09/118.11 % Names : % 117.09/118.11 % 117.09/118.11 % Status : Unsatisfiable % 117.09/118.11 % Rating : 0.00 v6.2.0, 0.10 v6.1.0, 0.09 v6.0.0, 0.00 v5.3.0, 0.10 v5.2.0, 0.00 v3.7.0, 0.14 v3.4.0, 0.17 v3.3.0, 0.22 v3.2.0 % 117.09/118.11 % Syntax : Number of clauses : 4 ( 1 unt; 0 nHn; 4 RR) % 117.09/118.11 % Number of literals : 7 ( 7 equ; 4 neg) % 117.09/118.11 % Maximal clause size : 2 ( 1 avg) % 117.09/118.11 % Maximal term depth : 4 ( 2 avg) % 117.09/118.11 % Number of predicates : 1 ( 0 usr; 0 prp; 2-2 aty) % 117.09/118.11 % Number of functors : 4 ( 4 usr; 1 con; 0-1 aty) % 117.09/118.11 % Number of variables : 3 ( 0 sgn) % 117.09/118.11 % SPC : CNF_UNS_RFO_PEQ_NUE % 117.09/118.11 % 117.09/118.11 % Comments : The problems in the [Pau06] collection each have very many axioms, % 117.09/118.11 % of which only a small selection are required for the refutation. % 117.09/118.11 % The mission is to find those few axioms, after which a refutation % 117.09/118.11 % can be quite easily found. This version has only the necessary % 117.09/118.11 % axioms. % 117.09/118.11 %------------------------------------------------------------------------------ % 117.09/118.11 cnf(cls_conjecture_0,negated_conjecture, % 117.09/118.11 v_f(v_g(v_x)) = v_x ). % 117.09/118.11 % 117.09/118.11 cnf(cls_conjecture_1,negated_conjecture, % 117.09/118.11 ( V_U = v_x % 117.09/118.11 | v_f(v_g(V_U)) != V_U ) ). % 117.09/118.11 % 117.09/118.11 cnf(cls_conjecture_2,negated_conjecture, % 117.09/118.11 ( v_g(v_f(v_xa(V_U))) = v_xa(V_U) % 117.09/118.11 | v_g(v_f(V_U)) != V_U ) ). % 117.09/118.11 % 117.09/118.11 cnf(cls_conjecture_3,negated_conjecture, % 117.09/118.11 ( v_xa(V_U) != V_U % 117.09/118.11 | v_g(v_f(V_U)) != V_U ) ). % 117.09/118.11 % 117.09/118.11 %------------------------------------------------------------------------------ % 117.09/118.11 %------------------------------------------- % 117.09/118.11 % Proof found % 117.09/118.11 % SZS status Theorem for theBenchmark % 117.09/118.11 % SZS output start Proof % 117.15/118.12 %ClaNum:10(EqnAxiom:6) % 117.15/118.12 %VarNum:11(SingletonVarNum:3) % 117.15/118.12 %MaxLitNum:2 % 117.15/118.12 %MaxfuncDepth:3 % 117.15/118.12 %SharedTerms:4 % 117.15/118.12 %goalClause: 7 8 9 10 % 117.15/118.12 %singleGoalClaCount:1 % 117.15/118.12 [7]E(f3(f2(a1)),a1) % 117.15/118.12 [8]E(x81,a1)+~E(f3(f2(x81)),x81) % 117.15/118.12 [9]~E(f4(x91),x91)+~E(f2(f3(x91)),x91) % 117.15/118.12 [10]~E(f2(f3(x101)),x101)+E(f2(f3(f4(x101))),f4(x101)) % 117.15/118.12 %EqnAxiom % 117.15/118.12 [1]E(x11,x11) % 117.15/118.12 [2]E(x22,x21)+~E(x21,x22) % 117.15/118.12 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 117.15/118.12 [4]~E(x41,x42)+E(f2(x41),f2(x42)) % 117.15/118.12 [5]~E(x51,x52)+E(f3(x51),f3(x52)) % 117.15/118.12 [6]~E(x61,x62)+E(f4(x61),f4(x62)) % 117.15/118.12 % 117.15/118.12 %------------------------------------------- % 117.15/118.13 cnf(11,plain, % 117.15/118.13 (E(a1,f3(f2(a1)))), % 117.15/118.13 inference(scs_inference,[],[7,2])). % 117.15/118.13 cnf(12,plain, % 117.15/118.13 (E(f2(f3(f2(a1))),f2(a1))), % 117.15/118.13 inference(scs_inference,[],[11,4,2])). % 117.15/118.13 cnf(15,plain, % 117.15/118.13 (E(f2(a1),f2(f3(f2(a1))))), % 117.15/118.13 inference(scs_inference,[],[12,9,2])). % 117.15/118.13 cnf(19,plain, % 117.15/118.13 (E(f2(f3(f4(f2(a1)))),f4(f2(a1)))), % 117.15/118.13 inference(scs_inference,[],[15,10,2])). % 117.15/118.13 cnf(29,plain, % 117.15/118.13 (E(f4(a1),f4(f3(f2(a1))))), % 117.15/118.13 inference(scs_inference,[],[7,2,6])). % 117.15/118.13 cnf(30,plain, % 117.15/118.13 (E(f4(f3(f2(a1))),f4(a1))), % 117.15/118.13 inference(scs_inference,[],[29,2])). % 117.15/118.13 cnf(31,plain, % 117.15/118.13 (~E(f2(a1),f4(f2(a1)))), % 117.15/118.13 inference(scs_inference,[],[12,2,9])). % 117.15/118.13 cnf(56,plain, % 117.15/118.13 (E(f4(f2(f4(a1))),f4(f2(f4(f3(f2(a1))))))), % 117.15/118.13 inference(scs_inference,[],[29,4,6])). % 117.15/118.13 cnf(57,plain, % 117.15/118.13 (E(f2(f3(f4(f3(f2(a1))))),f2(f3(f4(a1))))), % 117.15/118.13 inference(scs_inference,[],[30,4,5])). % 117.15/118.13 cnf(82,plain, % 117.15/118.13 (E(f3(f2(f3(f4(f2(a1))))),f3(f4(f2(a1))))), % 117.15/118.13 inference(scs_inference,[],[12,10,5])). % 117.15/118.13 cnf(1018,plain, % 117.15/118.13 (~E(f2(a1),f2(f3(f4(f2(a1)))))), % 117.15/118.13 inference(scs_inference,[],[31,12,3,10])). % 117.15/118.13 cnf(1710,plain, % 117.15/118.13 (~E(f2(f3(f4(f2(a1)))),f2(a1))), % 117.15/118.13 inference(scs_inference,[],[1018,2])). % 117.15/118.13 cnf(2836,plain, % 117.15/118.13 (E(f2(f3(f4(f4(f2(a1))))),f4(f4(f2(a1))))), % 117.15/118.13 inference(scs_inference,[],[19,10])). % 117.15/118.13 cnf(2916,plain, % 117.15/118.13 (E(f3(f4(f2(a1))),a1)), % 117.15/118.13 inference(scs_inference,[],[57,2836,1018,82,2,4,9,8])). % 117.15/118.13 cnf(2952,plain, % 117.15/118.13 ($false), % 117.15/118.13 inference(scs_inference,[],[56,2916,1710,2,4]), % 117.15/118.13 ['proof']). % 117.15/118.13 % SZS output end Proof % 117.15/118.13 % Total time :116.510000s %------------------------------------------------------------------------------