%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : LAT273-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 : n001.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 10:18:31 EDT 2024 % Result : Unsatisfiable 58.52s 60.15s % Output : CNFRefutation 58.73s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.09/0.11 % Problem : LAT273-2 : TPTP v8.2.0. Released v3.2.0. % 0.09/0.11 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.11/0.32 % Computer : n001.cluster.edu % 0.11/0.32 % Model : x86_64 x86_64 % 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.32 % Memory : 8042.1875MB % 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.32 % CPULimit : 300 % 0.16/0.32 % WCLimit : 300 % 0.16/0.32 % DateTime : Fri Jun 21 22:26:23 EDT 2024 % 0.16/0.32 % CPUTime : % 0.17/0.56 start to proof:theBenchmark % 58.52/60.14 %------------------------------------------- % 58.52/60.14 % File :CSE---1.7 % 58.52/60.14 % Problem :theBenchmark % 58.52/60.14 % Transform :cnf % 58.52/60.14 % Format :tptp:raw % 58.52/60.14 % Command :java -jar mcs_scs.jar %d %s % 58.52/60.14 % 58.52/60.14 % Result :Theorem 58.000000s % 58.52/60.14 % Output :CNFRefutation 58.000000s % 58.52/60.14 %------------------------------------------- % 58.52/60.15 %------------------------------------------------------------------------------ % 58.52/60.15 % File : LAT273-2 : TPTP v8.2.0. Released v3.2.0. % 58.52/60.15 % Domain : Analysis % 58.52/60.15 % Problem : Problem about Tarski's fixed point theorem % 58.52/60.15 % Version : [Pau06] axioms : Reduced > Especial. % 58.52/60.15 % English : % 58.52/60.15 % 58.52/60.15 % Refs : [Pau06] Paulson (2006), Email to G. Sutcliffe % 58.52/60.15 % Source : [Pau06] % 58.52/60.15 % Names : % 58.52/60.15 % 58.52/60.15 % Status : Unsatisfiable % 58.52/60.15 % Rating : 0.00 v4.0.0, 0.29 v3.4.0, 0.25 v3.3.0, 0.33 v3.2.0 % 58.52/60.15 % Syntax : Number of clauses : 7 ( 4 unt; 1 nHn; 7 RR) % 58.52/60.15 % Number of literals : 15 ( 0 equ; 8 neg) % 58.52/60.15 % Maximal clause size : 4 ( 2 avg) % 58.52/60.15 % Maximal term depth : 3 ( 1 avg) % 58.52/60.15 % Number of predicates : 3 ( 3 usr; 0 prp; 3-4 aty) % 58.52/60.15 % Number of functors : 13 ( 13 usr; 8 con; 0-4 aty) % 58.52/60.15 % Number of variables : 12 ( 1 sgn) % 58.52/60.15 % SPC : CNF_UNS_RFO_NEQ_NHN % 58.52/60.15 % 58.52/60.15 % Comments : The problems in the [Pau06] collection each have very many axioms, % 58.52/60.15 % of which only a small selection are required for the refutation. % 58.52/60.15 % The mission is to find those few axioms, after which a refutation % 58.52/60.15 % can be quite easily found. This version has only the necessary % 58.52/60.15 % axioms. % 58.52/60.15 %------------------------------------------------------------------------------ % 58.52/60.15 cnf(cls_Tarski_O_91_124_AS1_A_60_61_Ainterval_Ar_Aa1_Ab1_59_Ax1_A_58_AS1_A_124_93_A_61_61_62_A_Ix1_M_Ab1_J_A_58_Ar_A_61_61_ATrue_0,axiom, % 58.52/60.15 ( ~ c_in(V_x,V_S,T_a) % 58.52/60.15 | ~ c_lessequals(V_S,c_Tarski_Ointerval(V_r,V_a,V_b,T_a),tc_set(T_a)) % 58.52/60.15 | c_in(c_Pair(V_x,V_b,T_a,T_a),V_r,tc_prod(T_a,T_a)) ) ). % 58.52/60.15 % 58.52/60.15 cnf(cls_Tarski_O_91_124_AisLub_AS1_Acl_AL1_59_Az1_A_58_AA_59_AALL_Ay_58S1_O_A_Iy_M_Az1_J_A_58_Ar_A_124_93_A_61_61_62_A_IL1_M_Az1_J_A_58_Ar_A_61_61_ATrue_0,axiom, % 58.52/60.15 ( ~ c_Tarski_OisLub(V_S,v_cl,V_L,t_a) % 58.52/60.15 | ~ c_in(V_z,v_A,t_a) % 58.52/60.15 | c_in(c_Pair(V_L,V_z,t_a,t_a),v_r,tc_prod(t_a,t_a)) % 58.52/60.15 | c_in(v_sko__4mi(V_S,v_r,V_z),V_S,t_a) ) ). % 58.52/60.15 % 58.52/60.15 cnf(cls_Tarski_O_91_124_AisLub_AS1_Acl_AL1_59_Az1_A_58_AA_59_AALL_Ay_58S1_O_A_Iy_M_Az1_J_A_58_Ar_A_124_93_A_61_61_62_A_IL1_M_Az1_J_A_58_Ar_A_61_61_ATrue_1,axiom, % 58.52/60.15 ( ~ c_Tarski_OisLub(V_S,v_cl,V_L,t_a) % 58.52/60.15 | ~ c_in(V_z,v_A,t_a) % 58.52/60.15 | ~ c_in(c_Pair(v_sko__4mi(V_S,v_r,V_z),V_z,t_a,t_a),v_r,tc_prod(t_a,t_a)) % 58.52/60.15 | c_in(c_Pair(V_L,V_z,t_a,t_a),v_r,tc_prod(t_a,t_a)) ) ). % 58.52/60.15 % 58.52/60.15 cnf(cls_conjecture_1,negated_conjecture, % 58.52/60.15 c_in(v_b,v_A,t_a) ). % 58.52/60.15 % 58.52/60.15 cnf(cls_conjecture_2,negated_conjecture, % 58.52/60.15 c_lessequals(v_S,c_Tarski_Ointerval(v_r,v_a,v_b,t_a),tc_set(t_a)) ). % 58.52/60.15 % 58.52/60.15 cnf(cls_conjecture_4,negated_conjecture, % 58.52/60.15 c_Tarski_OisLub(v_S,v_cl,v_L,t_a) ). % 58.52/60.15 % 58.52/60.15 cnf(cls_conjecture_6,negated_conjecture, % 58.52/60.15 ~ c_in(c_Pair(v_L,v_b,t_a,t_a),v_r,tc_prod(t_a,t_a)) ). % 58.52/60.15 % 58.52/60.15 %------------------------------------------------------------------------------ % 58.52/60.15 %------------------------------------------- % 58.52/60.15 % Proof found % 58.52/60.15 % SZS status Theorem for theBenchmark % 58.52/60.15 % SZS output start Proof % 58.52/60.16 %ClaNum:7(EqnAxiom:0) % 58.52/60.16 %VarNum:32(SingletonVarNum:12) % 58.52/60.16 %MaxLitNum:4 % 58.52/60.16 %MaxfuncDepth:2 % 58.52/60.16 %SharedTerms:16 % 58.52/60.16 %goalClause: 1 2 3 4 % 58.52/60.16 %singleGoalClaCount:4 % 58.52/60.16 [1]P1(a1,a2,a3) % 58.52/60.16 [2]P2(a8,a11,a9,a3) % 58.52/60.16 [3]P3(a8,f4(a12,a10,a1,a3),f6(a3)) % 58.52/60.16 [4]~P1(f5(a9,a1,a3,a3),a12,f7(a3,a3)) % 58.52/60.16 [6]~P1(x61,x65,x63)+P1(f5(x61,x62,x63,x63),x64,f7(x63,x63))+~P3(x65,f4(x64,x66,x62,x63),f6(x63)) % 58.52/60.16 [5]~P2(x51,a11,x53,a3)+~P1(x52,a2,a3)+P1(f13(x51,a12,x52),x51,a3)+P1(f5(x53,x52,a3,a3),a12,f7(a3,a3)) % 58.52/60.16 [7]~P2(x73,a11,x71,a3)+~P1(x72,a2,a3)+P1(f5(x71,x72,a3,a3),a12,f7(a3,a3))+~P1(f5(f13(x73,a12,x72),x72,a3,a3),a12,f7(a3,a3)) % 58.52/60.16 %EqnAxiom % 58.52/60.16 % 58.52/60.16 %------------------------------------------- % 58.59/60.26 cnf(10,plain, % 58.59/60.26 (P1(f13(a8,a12,a1),a8,a3)), % 58.59/60.26 inference(scs_inference,[],[1,2,3,4,6,5])). % 58.59/60.26 cnf(136704,plain, % 58.68/60.26 ($false), % 58.68/60.26 inference(scs_inference,[],[1,10,2,3,4,6,7]), % 58.68/60.26 ['proof']). % 58.73/60.34 % SZS output end Proof % 58.73/60.34 % Total time :58.000000s %------------------------------------------------------------------------------