%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : LCL433-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 : n006.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:10 AM UTC 2026 % Result : Unsatisfiable 1.41s 1.66s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : LCL433-2 : TPTP v9.3.1. Released v3.2.0. % 0.00/0.02 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.06/0.34 % Computer : n006.cluster.edu % 0.06/0.34 % Model : x86_64 x86_64 % 0.06/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.06/0.34 % Memory : 8046.5625MB % 0.06/0.34 % OS : Linux 6.8.0-71-generic % 0.06/0.34 % CPULimit : 300 % 0.06/0.34 % WCLimit : 300 % 0.06/0.34 % DateTime : Sat Sep 5 09:10:16 UTC 2026 % 0.06/0.34 % CPUTime : % 0.13/0.44 start to proof:theBenchmark % 1.41/1.66 %------------------------------------------- % 1.41/1.66 % File :CSE---1.7 % 1.41/1.66 % Problem :theBenchmark % 1.41/1.66 % Transform :cnf % 1.41/1.66 % Format :tptp:raw % 1.41/1.66 % Command :java -jar mcs_scs.jar %d %s % 1.41/1.66 % 1.41/1.66 % Result :Theorem 1.209363s % 1.41/1.66 % Output :CNFRefutation 1.209363s % 1.41/1.66 %------------------------------------------- % 1.41/1.66 %------------------------------------------------------------------------------ % 1.41/1.66 % File : LCL433-2 : TPTP v9.3.1. Released v3.2.0. % 1.41/1.66 % Domain : Logic Calculi (Propositional) % 1.41/1.66 % Problem : Problem about propositional logic % 1.41/1.66 % Version : [Pau06] axioms : Reduced > Especial. % 1.41/1.66 % English : % 1.41/1.66 % 1.41/1.66 % Refs : [Pau06] Paulson (2006), Email to G. Sutcliffe % 1.41/1.66 % Source : [Pau06] % 1.41/1.66 % Names : % 1.41/1.66 % 1.41/1.66 % Status : Unsatisfiable % 1.41/1.66 % Rating : 0.00 v5.4.0, 0.06 v5.3.0, 0.10 v5.2.0, 0.00 v3.2.0 % 1.41/1.66 % Syntax : Number of clauses : 8 ( 3 unt; 0 nHn; 6 RR) % 1.41/1.66 % Number of literals : 14 ( 0 equ; 7 neg) % 1.41/1.66 % Maximal clause size : 3 ( 1 avg) % 1.41/1.66 % Maximal term depth : 4 ( 1 avg) % 1.41/1.66 % Number of predicates : 2 ( 2 usr; 0 prp; 3-3 aty) % 1.41/1.66 % Number of functors : 8 ( 8 usr; 4 con; 0-3 aty) % 1.41/1.66 % Number of variables : 19 ( 2 sgn) % 1.41/1.66 % SPC : CNF_UNS_RFO_NEQ_HRN % 1.41/1.66 % 1.41/1.66 % Comments : The problems in the [Pau06] collection each have very many axioms, % 1.41/1.66 % of which only a small selection are required for the refutation. % 1.41/1.66 % The mission is to find those few axioms, after which a refutation % 1.41/1.66 % can be quite easily found. This version has only the necessary % 1.41/1.66 % axioms. % 1.41/1.66 %------------------------------------------------------------------------------ % 1.41/1.66 cnf(cls_conjecture_2,negated_conjecture, % 1.41/1.66 c_PropLog_Osat(c_insert(v_x,v_F,tc_PropLog_Opl(t_a)),v_xa,t_a) ). % 1.41/1.66 % 1.41/1.66 cnf(cls_conjecture_3,negated_conjecture, % 1.41/1.66 ~ c_in(v_xa,c_PropLog_Othms(c_insert(v_x,v_F,tc_PropLog_Opl(t_a)),t_a),tc_PropLog_Opl(t_a)) ). % 1.41/1.66 % 1.41/1.66 cnf(cls_conjecture_4,negated_conjecture, % 1.41/1.66 ( c_in(V_U,c_PropLog_Othms(v_F,t_a),tc_PropLog_Opl(t_a)) % 1.41/1.66 | ~ c_PropLog_Osat(v_F,V_U,t_a) ) ). % 1.41/1.66 % 1.41/1.66 cnf(cls_PropLog_Osat__imp_0,axiom, % 1.41/1.66 ( ~ c_PropLog_Osat(c_insert(V_p,V_H,tc_PropLog_Opl(T_a)),V_q,T_a) % 1.41/1.66 | c_PropLog_Osat(V_H,c_PropLog_Opl_Oop_A_N_62(V_p,V_q,T_a),T_a) ) ). % 1.41/1.66 % 1.41/1.66 cnf(cls_PropLog_Othms_OH_0,axiom, % 1.41/1.66 ( ~ c_in(V_p,V_H,tc_PropLog_Opl(T_a)) % 1.41/1.66 | c_in(V_p,c_PropLog_Othms(V_H,T_a),tc_PropLog_Opl(T_a)) ) ). % 1.41/1.66 % 1.41/1.66 cnf(cls_PropLog_Othms_OMP_0,axiom, % 1.41/1.66 ( ~ c_in(V_p,c_PropLog_Othms(V_H,T_a),tc_PropLog_Opl(T_a)) % 1.41/1.66 | ~ 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)) % 1.41/1.66 | c_in(V_q,c_PropLog_Othms(V_H,T_a),tc_PropLog_Opl(T_a)) ) ). % 1.41/1.66 % 1.41/1.66 cnf(cls_PropLog_Oweaken__left__insert_0,axiom, % 1.41/1.66 ( ~ c_in(V_p,c_PropLog_Othms(V_G,T_a),tc_PropLog_Opl(T_a)) % 1.41/1.66 | 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)) ) ). % 1.41/1.66 % 1.41/1.66 cnf(cls_Set_OinsertCI_1,axiom, % 1.41/1.66 c_in(V_x,c_insert(V_x,V_B,T_a),T_a) ). % 1.41/1.66 % 1.41/1.66 %------------------------------------------------------------------------------ % 1.41/1.66 %------------------------------------------- % 1.41/1.66 % Proof found % 1.41/1.66 % SZS status Theorem for theBenchmark % 1.41/1.66 % SZS output start Proof % 1.41/1.66 %ClaNum:8(EqnAxiom:0) % 1.41/1.66 %VarNum:48(SingletonVarNum:19) % 1.41/1.66 %MaxLitNum:3 % 1.41/1.66 %MaxfuncDepth:3 % 1.41/1.66 %SharedTerms:10 % 1.41/1.66 %goalClause: 1 3 4 % 1.41/1.66 %singleGoalClaCount:2 % 1.41/1.66 [1]P1(f4(a1,a2,f7(a3)),a8,a3) % 1.41/1.66 [3]~P2(a8,f5(f4(a1,a2,f7(a3)),a3),f7(a3)) % 1.41/1.66 [2]P2(x21,f4(x21,x22,x23),x23) % 1.41/1.66 [4]~P1(a2,x41,a3)+P2(x41,f5(a2,a3),f7(a3)) % 1.41/1.66 [5]~P2(x51,x52,f7(x53))+P2(x51,f5(x52,x53),f7(x53)) % 1.41/1.66 [6]P1(x61,f6(x62,x63,x64),x64)+~P1(f4(x62,x61,f7(x64)),x63,x64) % 1.41/1.66 [7]~P2(x71,f5(x73,x74),f7(x74))+P2(x71,f5(f4(x72,x73,f7(x74)),x74),f7(x74)) % 1.41/1.66 [8]~P2(f6(x84,x81,x83),f5(x82,x83),f7(x83))+P2(x81,f5(x82,x83),f7(x83))+~P2(x84,f5(x82,x83),f7(x83)) % 1.41/1.66 %EqnAxiom % 1.41/1.66 % 1.41/1.66 %------------------------------------------- % 1.41/1.67 cnf(9,plain, % 1.41/1.67 (P1(a2,f6(a1,a8,a3),a3)), % 1.41/1.67 inference(scs_inference,[],[1,6])). % 1.41/1.67 cnf(13,plain, % 1.41/1.67 (~P2(a8,f5(a2,a3),f7(a3))), % 1.41/1.67 inference(scs_inference,[],[1,3,6,5,7])). % 1.41/1.67 cnf(689,plain, % 1.41/1.67 (P2(f6(a1,a8,a3),f5(f4(x6891,a2,f7(a3)),a3),f7(a3))), % 1.41/1.67 inference(scs_inference,[],[9,4,7])). % 1.41/1.67 cnf(694,plain, % 1.41/1.67 (~P2(a1,f5(f4(a1,a2,f7(a3)),a3),f7(a3))), % 1.41/1.67 inference(scs_inference,[],[3,13,689,5,4,8])). % 1.41/1.67 cnf(4119,plain, % 1.41/1.67 ($false), % 1.41/1.67 inference(scs_inference,[],[694,13,2,4,5]), % 1.41/1.67 ['proof']). % 1.41/1.67 % SZS output end Proof % 1.41/1.67 % Total time :1.209363s %------------------------------------------------------------------------------