%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : LCL443-2 : TPTP v9.3.1. Released v3.2.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n003.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 60.05s 60.19s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL443-2 : TPTP v9.3.1. Released v3.2.0. % 0.00/0.03 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.09/0.36 % Computer : n003.cluster.edu % 0.09/0.36 % Model : x86_64 x86_64 % 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.36 % Memory : 8046.5625MB % 0.09/0.36 % OS : Linux 6.8.0-71-generic % 0.09/0.36 % CPULimit : 300 % 0.09/0.36 % WCLimit : 300 % 0.09/0.36 % DateTime : Sat Sep 5 17:45:21 UTC 2026 % 0.09/0.36 % CPUTime : % 0.25/0.53 start to proof:theBenchmark % 60.05/60.18 %------------------------------------------- % 60.05/60.18 % File :CSE---1.7 % 60.05/60.18 % Problem :theBenchmark % 60.05/60.18 % Transform :cnf % 60.05/60.18 % Format :tptp:raw % 60.05/60.18 % Command :java -jar mcs_scs.jar %d %s % 60.05/60.18 % 60.05/60.18 % Result :Theorem 59.665292s % 60.05/60.18 % Output :CNFRefutation 59.665292s % 60.05/60.18 %------------------------------------------- % 60.05/60.19 %------------------------------------------------------------------------------ % 60.05/60.19 % File : LCL443-2 : TPTP v9.3.1. Released v3.2.0. % 60.05/60.19 % Domain : Logic Calculi (Propositional) % 60.05/60.19 % Problem : Problem about propositional logic % 60.05/60.19 % Version : [Pau06] axioms : Reduced > Especial. % 60.05/60.19 % English : % 60.05/60.19 % 60.05/60.19 % Refs : [Pau06] Paulson (2006), Email to G. Sutcliffe % 60.05/60.19 % Source : [Pau06] % 60.05/60.19 % Names : % 60.05/60.19 % 60.05/60.19 % Status : Unsatisfiable % 60.05/60.19 % Rating : 0.00 v7.4.0, 0.17 v7.3.0, 0.00 v5.4.0, 0.06 v5.3.0, 0.15 v5.2.0, 0.00 v3.2.0 % 60.05/60.19 % Syntax : Number of clauses : 8 ( 4 unt; 0 nHn; 6 RR) % 60.05/60.19 % Number of literals : 13 ( 0 equ; 6 neg) % 60.05/60.19 % Maximal clause size : 3 ( 1 avg) % 60.05/60.19 % Maximal term depth : 4 ( 1 avg) % 60.05/60.19 % Number of predicates : 1 ( 1 usr; 0 prp; 3-3 aty) % 60.05/60.19 % Number of functors : 9 ( 9 usr; 5 con; 0-3 aty) % 60.05/60.19 % Number of variables : 18 ( 2 sgn) % 60.05/60.19 % SPC : CNF_UNS_RFO_NEQ_HRN % 60.05/60.19 % 60.05/60.19 % Comments : The problems in the [Pau06] collection each have very many axioms, % 60.05/60.19 % of which only a small selection are required for the refutation. % 60.05/60.19 % The mission is to find those few axioms, after which a refutation % 60.05/60.19 % can be quite easily found. This version has only the necessary % 60.05/60.19 % axioms. % 60.05/60.19 %------------------------------------------------------------------------------ % 60.05/60.19 cnf(cls_PropLog_Othms_OMP_0,axiom, % 60.05/60.19 ( ~ c_in(V_p,c_PropLog_Othms(V_H,T_a),tc_PropLog_Opl(T_a)) % 60.05/60.19 | ~ 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)) % 60.05/60.19 | c_in(V_q,c_PropLog_Othms(V_H,T_a),tc_PropLog_Opl(T_a)) ) ). % 60.05/60.19 % 60.05/60.19 cnf(cls_PropLog_Odeduction_0,axiom, % 60.05/60.19 ( ~ 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)) % 60.05/60.19 | 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)) ) ). % 60.05/60.19 % 60.05/60.19 cnf(cls_PropLog_Othms_OH_0,axiom, % 60.05/60.19 ( ~ c_in(V_p,V_H,tc_PropLog_Opl(T_a)) % 60.05/60.19 | c_in(V_p,c_PropLog_Othms(V_H,T_a),tc_PropLog_Opl(T_a)) ) ). % 60.05/60.19 % 60.05/60.19 cnf(cls_PropLog_Oweaken__left__insert_0,axiom, % 60.05/60.19 ( ~ c_in(V_p,c_PropLog_Othms(V_G,T_a),tc_PropLog_Opl(T_a)) % 60.05/60.19 | 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)) ) ). % 60.05/60.19 % 60.05/60.19 cnf(cls_Set_OinsertCI_1,axiom, % 60.05/60.19 c_in(V_x,c_insert(V_x,V_B,T_a),T_a) ). % 60.05/60.19 % 60.05/60.19 cnf(cls_conjecture_0,negated_conjecture, % 60.05/60.19 c_in(v_p,c_PropLog_Othms(v_H,t_a),tc_PropLog_Opl(t_a)) ). % 60.05/60.19 % 60.05/60.19 cnf(cls_conjecture_1,negated_conjecture, % 60.05/60.19 c_in(c_PropLog_Opl_Oop_A_N_62(v_q,c_PropLog_Opl_Ofalse,t_a),c_PropLog_Othms(v_H,t_a),tc_PropLog_Opl(t_a)) ). % 60.05/60.19 % 60.05/60.19 cnf(cls_conjecture_2,negated_conjecture, % 60.05/60.19 ~ c_in(c_PropLog_Opl_Oop_A_N_62(c_PropLog_Opl_Oop_A_N_62(v_p,v_q,t_a),c_PropLog_Opl_Ofalse,t_a),c_PropLog_Othms(v_H,t_a),tc_PropLog_Opl(t_a)) ). % 60.05/60.19 % 60.05/60.19 %------------------------------------------------------------------------------ % 60.05/60.19 %------------------------------------------- % 60.05/60.19 % Proof found % 60.05/60.19 % SZS status Theorem for theBenchmark % 60.05/60.19 % SZS output start Proof % 60.05/60.19 %ClaNum:8(EqnAxiom:0) % 60.05/60.19 %VarNum:48(SingletonVarNum:18) % 60.05/60.19 %MaxLitNum:3 % 60.05/60.19 %MaxfuncDepth:3 % 60.05/60.19 %SharedTerms:13 % 60.05/60.19 %goalClause: 1 3 4 % 60.05/60.19 %singleGoalClaCount:3 % 60.05/60.19 [1]P1(a1,f4(a2,a3),f8(a3)) % 60.05/60.19 [3]P1(f6(a9,a5,a3),f4(a2,a3),f8(a3)) % 60.05/60.19 [4]~P1(f6(f6(a1,a9,a3),a5,a3),f4(a2,a3),f8(a3)) % 60.05/60.19 [2]P1(x21,f7(x21,x22,x23),x23) % 60.05/60.19 [5]~P1(x51,x52,f8(x53))+P1(x51,f4(x52,x53),f8(x53)) % 60.05/60.19 [6]~P1(x61,f4(x63,x64),f8(x64))+P1(x61,f4(f7(x62,x63,f8(x64)),x64),f8(x64)) % 60.05/60.19 [8]P1(f6(x81,x82,x83),f4(x84,x83),f8(x83))+~P1(x82,f4(f7(x81,x84,f8(x83)),x83),f8(x83)) % 60.05/60.19 [7]~P1(f6(x74,x71,x73),f4(x72,x73),f8(x73))+P1(x71,f4(x72,x73),f8(x73))+~P1(x74,f4(x72,x73),f8(x73)) % 60.05/60.19 %EqnAxiom % 60.05/60.19 % 60.05/60.19 %------------------------------------------- % 60.05/60.19 cnf(11,plain, % 60.05/60.19 (P1(a5,f4(a2,a3),f8(a3))+~P1(a9,f4(a2,a3),f8(a3))), % 60.05/60.19 inference(scs_inference,[],[3,4,5,7])). % 60.05/60.19 cnf(75,plain, % 60.05/60.20 (P1(a1,f4(f7(x751,f4(a2,a3),f8(a3)),a3),f8(a3))), % 60.05/60.20 inference(scs_inference,[],[1,6,5])). % 60.05/60.20 cnf(113,plain, % 60.05/60.20 (P1(f6(x1131,x1131,x1132),f4(x1133,x1132),f8(x1132))), % 60.05/60.20 inference(scs_inference,[],[2,5,8])). % 60.05/60.20 cnf(367,plain, % 60.05/60.20 (P1(f6(a9,a5,a3),f4(f7(x3671,f4(a2,a3),f8(a3)),a3),f8(a3))), % 60.05/60.20 inference(scs_inference,[],[3,5,6])). % 60.05/60.20 cnf(879,plain, % 60.05/60.20 (P1(x8791,f4(f7(x8792,f7(x8791,x8793,f8(x8794)),f8(x8794)),x8794),f8(x8794))), % 60.05/60.20 inference(scs_inference,[],[2,5,6])). % 60.05/60.20 cnf(880,plain, % 60.05/60.20 (P1(f6(x8801,x8802,x8803),f4(f7(x8802,x8804,f8(x8803)),x8803),f8(x8803))), % 60.05/60.20 inference(scs_inference,[],[879,8])). % 60.05/60.20 cnf(884,plain, % 60.05/60.20 (P1(x8841,f4(f7(x8841,f4(a2,a3),f8(a3)),a3),f8(a3))), % 60.05/60.20 inference(scs_inference,[],[4,367,879,8,5,7])). % 60.05/60.20 cnf(886,plain, % 60.05/60.20 (P1(f6(x8861,f6(x8862,x8861,x8863),x8863),f4(x8864,x8863),f8(x8863))), % 60.05/60.20 inference(scs_inference,[],[880,8])). % 60.05/60.20 cnf(890,plain, % 60.05/60.20 (P1(x8901,f4(f7(f6(f6(a9,a5,a3),x8901,a3),f4(a2,a3),f8(a3)),a3),f8(a3))), % 60.05/60.20 inference(scs_inference,[],[4,367,880,884,8,5,7])). % 60.05/60.20 cnf(909,plain, % 60.05/60.20 (~P1(a5,f4(a2,a3),f8(a3))), % 60.05/60.20 inference(scs_inference,[],[4,886,890,8,5,7])). % 60.05/60.20 cnf(912,plain, % 60.05/60.20 (~P1(a9,f4(a2,a3),f8(a3))), % 60.05/60.20 inference(scs_inference,[],[4,886,890,8,5,7,11])). % 60.05/60.20 cnf(1738,plain, % 60.05/60.20 (P1(x17381,f4(f7(f6(f6(x17382,x17382,a3),x17381,a3),f4(a2,a3),f8(a3)),a3),f8(a3))), % 60.05/60.20 inference(scs_inference,[],[113,4,884,5,7])). % 60.05/60.20 cnf(1750,plain, % 60.05/60.20 (P1(x17501,f4(f7(x17501,x17502,f8(x17503)),x17503),f8(x17503))), % 60.05/60.20 inference(scs_inference,[],[113,4,880,1738,5,8,7])). % 60.05/60.20 cnf(1762,plain, % 60.05/60.20 (P1(x17621,f4(f7(f6(f6(x17622,x17622,x17623),x17621,x17623),x17624,f8(x17623)),x17623),f8(x17623))), % 60.05/60.20 inference(scs_inference,[],[113,4,1750,5,7])). % 60.05/60.20 cnf(1766,plain, % 60.05/60.20 (P1(f6(f6(f6(x17661,x17661,x17662),x17663,x17662),x17663,x17662),f4(x17664,x17662),f8(x17662))), % 60.05/60.20 inference(scs_inference,[],[113,4,1750,5,7,8])). % 60.05/60.20 cnf(1770,plain, % 60.05/60.20 (~P1(f6(f6(x17701,x17701,a3),f6(f6(a1,a9,a3),a5,a3),a3),f4(a2,a3),f8(a3))), % 60.05/60.20 inference(scs_inference,[],[4,1766,5,7])). % 60.05/60.20 cnf(2216,plain, % 60.05/60.20 (P1(x22161,f4(f7(x22162,f7(f6(x22162,x22161,x22163),x22164,f8(x22163)),f8(x22163)),x22163),f8(x22163))), % 60.16/60.20 inference(scs_inference,[],[1750,879,7])). % 60.16/60.20 cnf(2233,plain, % 60.16/60.20 (P1(x22331,f4(f7(f6(x22332,x22331,x22333),f7(x22332,x22334,f8(x22333)),f8(x22333)),x22333),f8(x22333))), % 60.16/60.20 inference(scs_inference,[],[879,1750,7])). % 60.16/60.20 cnf(2237,plain, % 60.16/60.20 (P1(f6(f6(x22371,x22372,x22373),x22372,x22373),f4(f7(x22371,x22374,f8(x22373)),x22373),f8(x22373))), % 60.16/60.20 inference(scs_inference,[],[879,1750,7,8])). % 60.16/60.20 cnf(2240,plain, % 60.16/60.20 (P1(f6(x22401,f6(f6(x22401,x22402,x22403),x22402,x22403),x22403),f4(x22404,x22403),f8(x22403))), % 60.16/60.20 inference(scs_inference,[],[2237,8])). % 60.16/60.20 cnf(2255,plain, % 60.16/60.20 (~P1(f6(f6(x22551,x22551,a3),a5,a3),f4(a2,a3),f8(a3))), % 60.16/60.20 inference(scs_inference,[],[909,1766,7])). % 60.16/60.20 cnf(2258,plain, % 60.16/60.20 (P1(f6(x22581,f6(a9,a5,a3),a3),f4(a2,a3),f8(a3))), % 60.16/60.20 inference(scs_inference,[],[3,6,8])). % 60.16/60.20 cnf(2265,plain, % 60.16/60.20 (P1(a5,f4(f7(a9,a2,f8(a3)),a3),f8(a3))), % 60.16/60.20 inference(scs_inference,[],[3,1750,6,7])). % 60.16/60.20 cnf(2338,plain, % 60.16/60.20 (P1(f6(f6(f6(a9,a5,a3),x23381,a3),x23381,a3),f4(a2,a3),f8(a3))), % 60.16/60.20 inference(scs_inference,[],[3,2240,7])). % 60.16/60.20 cnf(2362,plain, % 60.16/60.20 (P1(f6(x23621,f6(x23622,x23623,x23624),x23624),f4(f7(f6(x23621,x23623,x23624),x23625,f8(x23624)),x23624),f8(x23624))), % 60.16/60.20 inference(scs_inference,[],[2216,886,7,8])). % 60.16/60.20 cnf(2365,plain, % 60.16/60.20 (P1(f6(f6(x23651,x23652,x23653),f6(x23651,f6(x23654,x23652,x23653),x23653),x23653),f4(x23655,x23653),f8(x23653))), % 60.16/60.20 inference(scs_inference,[],[2362,8])). % 60.16/60.20 cnf(2387,plain, % 60.16/60.20 (P1(f6(f6(x23871,x23872,x23873),f6(x23874,x23872,x23873),x23873),f4(f7(x23871,x23875,f8(x23873)),x23873),f8(x23873))), % 60.16/60.20 inference(scs_inference,[],[2233,886,7,8])). % 60.16/60.20 cnf(2390,plain, % 60.16/60.20 (P1(f6(x23901,f6(f6(x23901,x23902,x23903),f6(x23904,x23902,x23903),x23903),x23903),f4(x23905,x23903),f8(x23903))), % 60.16/60.20 inference(scs_inference,[],[2387,8])). % 60.16/60.20 cnf(2413,plain, % 60.16/60.20 (P1(f6(f6(f6(x24131,f6(a9,a5,a3),a3),x24132,a3),f6(x24133,x24132,a3),a3),f4(a2,a3),f8(a3))), % 60.16/60.20 inference(scs_inference,[],[2258,2390,7])). % 60.16/60.20 cnf(2416,plain, % 60.16/60.20 (P1(f6(a9,a5,a3),f4(f7(x24161,a2,f8(a3)),a3),f8(a3))), % 60.16/60.20 inference(scs_inference,[],[2258,3,6,7])). % 60.16/60.20 cnf(2459,plain, % 60.16/60.20 (P1(f6(x24591,a5,a3),f4(f7(a9,a2,f8(a3)),a3),f8(a3))), % 60.16/60.20 inference(scs_inference,[],[2265,886,7])). % 60.16/60.20 cnf(2578,plain, % 60.16/60.20 (~P1(f6(f6(a9,a5,a3),f6(f6(a1,a9,a3),a5,a3),a3),f4(a2,a3),f8(a3))), % 60.16/60.20 inference(scs_inference,[],[4,2338,7])). % 60.16/60.20 cnf(2582,plain, % 60.16/60.20 (~P1(f6(f6(a9,a5,a3),a5,a3),f4(a2,a3),f8(a3))), % 60.16/60.20 inference(scs_inference,[],[2365,2578,7])). % 60.16/60.20 cnf(2609,plain, % 60.16/60.20 (P1(x26091,f4(f7(f6(f6(a9,a5,a3),x26091,a3),a2,f8(a3)),a3),f8(a3))), % 60.16/60.20 inference(scs_inference,[],[2416,1750,7])). % 60.16/60.20 cnf(2693,plain, % 60.16/60.20 (P1(f6(f6(f6(a9,a5,a3),a9,a3),a5,a3),f4(a2,a3),f8(a3))), % 60.16/60.20 inference(scs_inference,[],[2609,2416,7,8])). % 60.16/60.20 cnf(2696,plain, % 60.16/60.20 (~P1(f6(f6(a9,a5,a3),a9,a3),f4(a2,a3),f8(a3))), % 60.16/60.20 inference(scs_inference,[],[2693,909,7])). % 60.16/60.20 cnf(2754,plain, % 60.16/60.20 (P1(f6(x27541,a1,a3),f4(f7(x27542,f4(a2,a3),f8(a3)),a3),f8(a3))), % 60.16/60.20 inference(scs_inference,[],[75,8,6])). % 60.16/60.20 cnf(2757,plain, % 60.16/60.20 (P1(x27571,f4(f7(f6(f6(x27572,x27572,a3),f6(a1,x27571,a3),a3),f4(a2,a3),f8(a3)),a3),f8(a3))), % 60.16/60.20 inference(scs_inference,[],[75,1762,2754,8,7])). % 60.16/60.20 cnf(2764,plain, % 60.16/60.20 (P1(f6(x27641,x27642,a3),f4(f7(f6(a1,x27642,a3),f4(a2,a3),f8(a3)),a3),f8(a3))), % 60.16/60.20 inference(scs_inference,[],[75,2362,2757,8,7])). % 60.16/60.20 cnf(2851,plain, % 60.16/60.20 (~P1(f6(f6(x28511,x28511,a3),f6(f6(x28512,x28512,a3),a5,a3),a3),f4(a2,a3),f8(a3))), % 60.16/60.20 inference(scs_inference,[],[2255,1766,7])). % 60.16/60.20 cnf(3009,plain, % 60.16/60.20 (~P1(f6(f6(x30091,f6(a9,a5,a3),a3),f6(f6(x30092,x30092,a3),a5,a3),a3),f4(a2,a3),f8(a3))), % 60.16/60.20 inference(scs_inference,[],[2851,2413,7])). % 60.16/60.20 cnf(3072,plain, % 60.16/60.20 (P1(a1,f4(f7(x30721,a2,f8(a3)),a3),f8(a3))), % 60.16/60.20 inference(scs_inference,[],[1,6])). % 60.16/60.20 cnf(3074,plain, % 60.16/60.20 (~P1(f6(f6(a1,a9,a3),a5,a3),f4(f7(f6(x30741,x30741,a3),a2,f8(a3)),a3),f8(a3))), % 60.16/60.20 inference(scs_inference,[],[1,1770,6,8])). % 60.16/60.20 cnf(3078,plain, % 60.16/60.20 (~P1(f6(a1,a9,a3),f4(a2,a3),f8(a3))), % 60.16/60.20 inference(scs_inference,[],[1,3009,912,1770,6,8,5,7])). % 60.16/60.20 cnf(3087,plain, % 60.16/60.20 (~P1(f6(a1,f6(a1,a9,a3),a3),f4(a2,a3),f8(a3))), % 60.16/60.20 inference(scs_inference,[],[1,3078,2764,6,8,5,7])). % 60.16/60.20 cnf(3089,plain, % 60.16/60.20 (P1(f6(x30891,a1,a3),f4(f7(x30892,a2,f8(a3)),a3),f8(a3))), % 60.16/60.20 inference(scs_inference,[],[3072,8,6])). % 60.16/60.20 cnf(3092,plain, % 60.16/60.20 (~P1(f6(a1,a9,a3),f4(f7(a1,a2,f8(a3)),a3),f8(a3))), % 60.16/60.20 inference(scs_inference,[],[3087,3089,6,8])). % 60.16/60.20 cnf(3096,plain, % 60.16/60.20 (~P1(f6(a1,f6(a1,f6(a1,a9,a3),a3),a3),f4(a2,a3),f8(a3))), % 60.16/60.20 inference(scs_inference,[],[1,3087,3089,6,8,5,7])). % 60.16/60.20 cnf(3101,plain, % 60.16/60.20 (~P1(f6(a1,f6(a1,a9,a3),a3),f4(f7(a1,a2,f8(a3)),a3),f8(a3))), % 60.16/60.20 inference(scs_inference,[],[3096,2459,6,8])). % 60.16/60.20 cnf(3105,plain, % 60.16/60.20 (~P1(f6(a1,a5,a3),f4(a2,a3),f8(a3))), % 60.16/60.20 inference(scs_inference,[],[1,3096,2459,909,6,8,5,7])). % 60.16/60.20 cnf(3108,plain, % 60.16/60.20 (P1(a1,f4(f7(x31081,f7(x31082,a2,f8(a3)),f8(a3)),a3),f8(a3))), % 60.16/60.20 inference(scs_inference,[],[3072,6])). % 60.16/60.20 cnf(3114,plain, % 60.16/60.20 (~P1(f6(a1,f6(a1,a5,a3),a3),f4(a2,a3),f8(a3))), % 60.16/60.20 inference(scs_inference,[],[1,3105,3072,6,8,5,7])). % 60.16/60.20 cnf(3119,plain, % 60.16/60.20 (~P1(f6(a1,a5,a3),f4(f7(a1,a2,f8(a3)),a3),f8(a3))), % 60.16/60.20 inference(scs_inference,[],[3114,2265,6,8])). % 60.16/60.20 cnf(3136,plain, % 60.16/60.20 (P1(f6(a9,a5,a3),f4(f7(x31361,f7(x31362,a2,f8(a3)),f8(a3)),a3),f8(a3))), % 60.16/60.20 inference(scs_inference,[],[2416,6])). % 60.16/60.20 cnf(3142,plain, % 60.16/60.20 (~P1(f6(a1,f6(f6(x31421,x31421,a3),a5,a3),a3),f4(a2,a3),f8(a3))), % 60.16/60.20 inference(scs_inference,[],[1,3092,2255,2416,6,8,5,7])). % 60.16/60.20 cnf(3147,plain, % 60.16/60.20 (~P1(a5,f4(f7(a1,f7(a1,a2,f8(a3)),f8(a3)),a3),f8(a3))), % 60.16/60.20 inference(scs_inference,[],[3119,75,6,8])). % 60.16/60.20 cnf(3160,plain, % 60.16/60.20 (~P1(f6(a1,a5,a3),f4(f7(a1,f7(a1,a2,f8(a3)),f8(a3)),a3),f8(a3))), % 60.16/60.20 inference(scs_inference,[],[3142,3147,3108,367,6,8,5,7])). % 60.16/60.20 cnf(3174,plain, % 60.16/60.20 (~P1(f6(a1,a9,a3),f4(f7(a1,f7(a1,a2,f8(a3)),f8(a3)),a3),f8(a3))), % 60.16/60.20 inference(scs_inference,[],[3101,8])). % 60.16/60.20 cnf(3178,plain, % 60.16/60.20 (~P1(f6(a1,f6(f6(a9,a5,a3),a5,a3),a3),f4(a2,a3),f8(a3))), % 60.16/60.20 inference(scs_inference,[],[1,3160,3101,2582,8,5,7])). % 60.16/60.20 cnf(3185,plain, % 60.16/60.20 (~P1(f6(a1,f6(f6(a9,a5,a3),a9,a3),a3),f4(a2,a3),f8(a3))), % 60.16/60.20 inference(scs_inference,[],[1,3178,2696,8,5,7])). % 60.16/60.20 cnf(3188,plain, % 60.16/60.20 (~P1(f6(f6(a9,a5,a3),a9,a3),f4(f7(a1,a2,f8(a3)),a3),f8(a3))), % 60.16/60.20 inference(scs_inference,[],[3185,8])). % 60.16/60.21 cnf(3198,plain, % 60.16/60.21 (~P1(a9,f4(f7(f6(a9,a5,a3),f7(a1,a2,f8(a3)),f8(a3)),a3),f8(a3))), % 60.16/60.21 inference(scs_inference,[],[3188,8])). % 60.16/60.21 cnf(3207,plain, % 60.16/60.21 (~P1(f6(a1,f6(f6(a1,a9,a3),a5,a3),a3),f4(a2,a3),f8(a3))), % 60.16/60.21 inference(scs_inference,[],[1,3174,3074,4,8,5,7])). % 60.16/60.21 cnf(3210,plain, % 60.16/60.21 (~P1(f6(f6(a1,a9,a3),a5,a3),f4(f7(a1,a2,f8(a3)),a3),f8(a3))), % 60.16/60.21 inference(scs_inference,[],[3207,8])). % 60.16/60.21 cnf(3214,plain, % 60.16/60.21 (~P1(f6(a1,a9,a3),f4(f7(f6(a9,a5,a3),f7(a1,a2,f8(a3)),f8(a3)),a3),f8(a3))), % 60.16/60.21 inference(scs_inference,[],[3207,3198,3108,8,5,7])). % 60.16/60.21 cnf(3222,plain, % 60.16/60.21 ($false), % 60.16/60.21 inference(scs_inference,[],[3214,3210,3136,2233,8,5,7]), % 60.16/60.21 ['proof']). % 60.16/60.21 % SZS output end Proof % 60.16/60.21 % Total time :59.665292s %------------------------------------------------------------------------------