%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : LCL439-2 : TPTP v9.3.1. Released v3.2.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n011.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Sep 7 11:19:11 AM UTC 2026 % Result : Unsatisfiable 58.38s 58.52s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL439-2 : TPTP v9.3.1. Released v3.2.0. % 0.00/0.03 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.08/0.34 % Computer : n011.cluster.edu % 0.08/0.34 % Model : x86_64 x86_64 % 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.34 % Memory : 8046.5625MB % 0.08/0.34 % OS : Linux 6.8.0-71-generic % 0.08/0.34 % CPULimit : 300 % 0.08/0.34 % WCLimit : 300 % 0.08/0.34 % DateTime : Sun Sep 6 01:31:29 UTC 2026 % 0.08/0.35 % CPUTime : % 0.25/0.50 start to proof:theBenchmark % 58.38/58.51 %------------------------------------------- % 58.38/58.51 % File :CSE---1.7 % 58.38/58.51 % Problem :theBenchmark % 58.38/58.51 % Transform :cnf % 58.38/58.51 % Format :tptp:raw % 58.38/58.51 % Command :java -jar mcs_scs.jar %d %s % 58.38/58.51 % 58.38/58.51 % Result :Theorem 58.006497s % 58.38/58.51 % Output :CNFRefutation 58.006497s % 58.38/58.51 %------------------------------------------- % 58.38/58.52 %------------------------------------------------------------------------------ % 58.38/58.52 % File : LCL439-2 : TPTP v9.3.1. Released v3.2.0. % 58.38/58.52 % Domain : Logic Calculi (Propositional) % 58.38/58.52 % Problem : Problem about propositional logic % 58.38/58.52 % Version : [Pau06] axioms : Reduced > Especial. % 58.38/58.52 % English : % 58.38/58.52 % 58.38/58.52 % Refs : [Pau06] Paulson (2006), Email to G. Sutcliffe % 58.38/58.52 % Source : [Pau06] % 58.38/58.52 % Names : % 58.38/58.52 % 58.38/58.52 % Status : Unsatisfiable % 58.38/58.52 % Rating : 0.00 v5.4.0, 0.06 v5.3.0, 0.10 v5.2.0, 0.00 v3.2.0 % 58.38/58.52 % Syntax : Number of clauses : 7 ( 3 unt; 0 nHn; 4 RR) % 58.38/58.52 % Number of literals : 12 ( 0 equ; 6 neg) % 58.38/58.52 % Maximal clause size : 3 ( 1 avg) % 58.38/58.52 % Maximal term depth : 4 ( 1 avg) % 58.38/58.52 % Number of predicates : 1 ( 1 usr; 0 prp; 3-3 aty) % 58.38/58.52 % Number of functors : 9 ( 9 usr; 5 con; 0-3 aty) % 58.38/58.52 % Number of variables : 18 ( 3 sgn) % 58.38/58.52 % SPC : CNF_UNS_RFO_NEQ_HRN % 58.38/58.52 % 58.38/58.52 % Comments : The problems in the [Pau06] collection each have very many axioms, % 58.38/58.52 % of which only a small selection are required for the refutation. % 58.38/58.52 % The mission is to find those few axioms, after which a refutation % 58.38/58.52 % can be quite easily found. This version has only the necessary % 58.38/58.52 % axioms. % 58.38/58.52 %------------------------------------------------------------------------------ % 58.38/58.52 cnf(cls_PropLog_Odeduction_0,axiom, % 58.38/58.52 ( ~ c_in(V_q,c_PropLog_Othms(c_insert(V_p,V_H,tc_PropLog_Opl(T_a)),T_a),tc_PropLog_Opl(T_a)) % 58.38/58.52 | c_in(c_PropLog_Opl_Oop_A_N_62(V_p,V_q,T_a),c_PropLog_Othms(V_H,T_a),tc_PropLog_Opl(T_a)) ) ). % 58.38/58.52 % 58.38/58.52 cnf(cls_PropLog_Othms_OH_0,axiom, % 58.38/58.52 ( ~ c_in(V_p,V_H,tc_PropLog_Opl(T_a)) % 58.38/58.52 | c_in(V_p,c_PropLog_Othms(V_H,T_a),tc_PropLog_Opl(T_a)) ) ). % 58.38/58.52 % 58.38/58.52 cnf(cls_PropLog_Othms__notE_0,axiom, % 58.38/58.52 ( ~ c_in(V_p,c_PropLog_Othms(V_H,T_a),tc_PropLog_Opl(T_a)) % 58.38/58.52 | ~ c_in(c_PropLog_Opl_Oop_A_N_62(V_p,c_PropLog_Opl_Ofalse,T_a),c_PropLog_Othms(V_H,T_a),tc_PropLog_Opl(T_a)) % 58.38/58.52 | c_in(V_q,c_PropLog_Othms(V_H,T_a),tc_PropLog_Opl(T_a)) ) ). % 58.38/58.52 % 58.38/58.52 cnf(cls_PropLog_Oweaken__left__insert_0,axiom, % 58.38/58.52 ( ~ c_in(V_p,c_PropLog_Othms(V_G,T_a),tc_PropLog_Opl(T_a)) % 58.38/58.52 | c_in(V_p,c_PropLog_Othms(c_insert(V_a,V_G,tc_PropLog_Opl(T_a)),T_a),tc_PropLog_Opl(T_a)) ) ). % 58.38/58.52 % 58.38/58.52 cnf(cls_Set_OinsertCI_1,axiom, % 58.38/58.52 c_in(V_x,c_insert(V_x,V_B,T_a),T_a) ). % 58.38/58.52 % 58.38/58.52 cnf(cls_conjecture_0,negated_conjecture, % 58.38/58.52 c_in(c_PropLog_Opl_Oop_A_N_62(v_p,c_PropLog_Opl_Ofalse,t_a),c_PropLog_Othms(v_H,t_a),tc_PropLog_Opl(t_a)) ). % 58.38/58.52 % 58.38/58.52 cnf(cls_conjecture_1,negated_conjecture, % 58.38/58.52 ~ c_in(c_PropLog_Opl_Oop_A_N_62(v_p,v_q,t_a),c_PropLog_Othms(v_H,t_a),tc_PropLog_Opl(t_a)) ). % 58.38/58.52 % 58.38/58.52 %------------------------------------------------------------------------------ % 58.38/58.52 %------------------------------------------- % 58.38/58.52 % Proof found % 58.38/58.52 % SZS status Theorem for theBenchmark % 58.38/58.52 % SZS output start Proof % 58.38/58.52 %ClaNum:7(EqnAxiom:0) % 58.38/58.52 %VarNum:47(SingletonVarNum:18) % 58.38/58.52 %MaxLitNum:3 % 58.38/58.52 %MaxfuncDepth:3 % 58.38/58.52 %SharedTerms:11 % 58.38/58.52 %goalClause: 2 3 % 58.38/58.52 %singleGoalClaCount:2 % 58.38/58.52 [2]P1(f3(a5,a2,a6),f4(a7,a6),f8(a6)) % 58.38/58.52 [3]~P1(f3(a5,a9,a6),f4(a7,a6),f8(a6)) % 58.38/58.52 [1]P1(x11,f1(x11,x12,x13),x13) % 58.38/58.52 [4]~P1(x41,x42,f8(x43))+P1(x41,f4(x42,x43),f8(x43)) % 58.38/58.52 [5]~P1(x51,f4(x53,x54),f8(x54))+P1(x51,f4(f1(x52,x53,f8(x54)),x54),f8(x54)) % 58.38/58.52 [7]P1(f3(x71,x72,x73),f4(x74,x73),f8(x73))+~P1(x72,f4(f1(x71,x74,f8(x73)),x73),f8(x73)) % 58.38/58.52 [6]P1(x61,f4(x62,x63),f8(x63))+~P1(x64,f4(x62,x63),f8(x63))+~P1(f3(x64,a2,x63),f4(x62,x63),f8(x63)) % 58.38/58.52 %EqnAxiom % 58.38/58.52 % 58.38/58.52 %------------------------------------------- % 58.58/58.76 cnf(252068,plain, % 58.58/58.76 (P1(f3(a5,a2,a6),f4(f1(x2520681,a7,f8(a6)),a6),f8(a6))), % 58.58/58.76 inference(scs_inference,[],[2,5])). % 58.58/58.76 cnf(252070,plain, % 58.58/58.76 (~P1(a9,f4(f1(a5,a7,f8(a6)),a6),f8(a6))), % 58.58/58.76 inference(scs_inference,[],[2,3,5,7])). % 58.58/58.76 cnf(252072,plain, % 58.58/58.76 (P1(f3(a5,a2,a6),f4(f4(a7,a6),a6),f8(a6))), % 58.58/58.76 inference(scs_inference,[],[2,3,5,7,4])). % 58.58/58.76 cnf(252074,plain, % 58.58/58.76 (~P1(f3(f3(a5,a2,a6),a2,a6),f4(a7,a6),f8(a6))), % 58.58/58.76 inference(scs_inference,[],[2,3,5,7,4,6])). % 58.58/58.77 cnf(252083,plain, % 58.58/58.77 ($false), % 58.58/58.77 inference(scs_inference,[],[1,252074,252072,252068,252070,5,7,4,6]), % 58.58/58.77 ['proof']). % 58.68/58.85 % SZS output end Proof % 58.68/58.85 % Total time :58.006497s %------------------------------------------------------------------------------