%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN415+1 : TPTP v8.2.0. Released v2.0.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n029.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 19:05:28 EDT 2024 % Result : Theorem 4.29s 4.39s % Output : CNFRefutation 4.40s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SYN415+1 : TPTP v8.2.0. Released v2.0.0. % 0.07/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n029.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 22:58:54 EDT 2024 % 0.12/0.34 % CPUTime : % 0.20/0.57 start to proof:theBenchmark % 4.29/4.38 %------------------------------------------- % 4.29/4.38 % File :CSE---1.7 % 4.29/4.38 % Problem :theBenchmark % 4.29/4.38 % Transform :cnf % 4.29/4.38 % Format :tptp:raw % 4.29/4.38 % Command :java -jar mcs_scs.jar %d %s % 4.29/4.38 % 4.29/4.38 % Result :Theorem 3.770000s % 4.29/4.38 % Output :CNFRefutation 3.770000s % 4.29/4.38 %------------------------------------------- % 4.29/4.39 %-------------------------------------------------------------------------- % 4.29/4.39 % File : SYN415+1 : TPTP v8.2.0. Released v2.0.0. % 4.29/4.39 % Domain : Syntactic % 4.29/4.39 % Problem : Kalish and Montague Problem 317 % 4.29/4.39 % Version : Especial. % 4.29/4.39 % English : % 4.29/4.39 % 4.29/4.39 % Refs : [KM64] Kalish & Montegue (1964), Logic: Techniques of Formal % 4.29/4.39 % : [Hah94] Haehnle (1994), Email to G. Sutcliffe % 4.29/4.39 % Source : [Hah94] % 4.29/4.39 % Names : kalish317 [Hah94] % 4.29/4.39 % 4.29/4.39 % Status : Theorem % 4.29/4.39 % Rating : 0.11 v8.1.0, 0.08 v7.5.0, 0.09 v7.4.0, 0.10 v7.2.0, 0.07 v7.1.0, 0.09 v7.0.0, 0.07 v6.4.0, 0.12 v6.3.0, 0.04 v6.2.0, 0.16 v6.1.0, 0.07 v6.0.0, 0.04 v5.5.0, 0.07 v5.4.0, 0.11 v5.3.0, 0.15 v5.2.0, 0.05 v5.0.0, 0.08 v4.1.0, 0.09 v4.0.0, 0.08 v3.7.0, 0.00 v3.2.0, 0.22 v3.1.0, 0.33 v2.6.0, 0.00 v2.5.0, 0.33 v2.4.0, 0.33 v2.2.1, 0.00 v2.1.0 % 4.29/4.39 % Syntax : Number of formulae : 1 ( 0 unt; 0 def) % 4.29/4.39 % Number of atoms : 7 ( 2 equ) % 4.29/4.39 % Maximal formula atoms : 7 ( 7 avg) % 4.29/4.39 % Number of connectives : 6 ( 0 ~; 0 |; 3 &) % 4.29/4.39 % ( 1 <=>; 2 =>; 0 <=; 0 <~>) % 4.29/4.39 % Maximal formula depth : 7 ( 7 avg) % 4.29/4.39 % Maximal term depth : 1 ( 1 avg) % 4.29/4.39 % Number of predicates : 2 ( 1 usr; 0 prp; 1-2 aty) % 4.29/4.39 % Number of functors : 0 ( 0 usr; 0 con; --- aty) % 4.29/4.39 % Number of variables : 5 ( 3 !; 2 ?) % 4.29/4.39 % SPC : FOF_THM_RFO_SEQ % 4.29/4.39 % 4.29/4.39 % Comments : % 4.29/4.39 %-------------------------------------------------------------------------- % 4.29/4.39 %----Problem axioms % 4.29/4.39 fof(kalish317,conjecture, % 4.29/4.39 ( ( ? [X] : f(X) % 4.29/4.39 & ! [Y,Z] : % 4.29/4.39 ( ( f(Y) % 4.29/4.39 & f(Z) ) % 4.29/4.39 => Y = Z ) ) % 4.29/4.39 <=> ? [U] : % 4.29/4.39 ( f(U) % 4.29/4.39 & ! [V] : % 4.29/4.39 ( f(V) % 4.29/4.39 => U = V ) ) ) ). % 4.29/4.39 % 4.29/4.39 %-------------------------------------------------------------------------- % 4.29/4.39 %------------------------------------------- % 4.29/4.39 % Proof found % 4.29/4.39 % SZS status Theorem for theBenchmark % 4.29/4.39 % SZS output start Proof % 4.29/4.39 %ClaNum:15(EqnAxiom:5) % 4.29/4.39 %VarNum:33(SingletonVarNum:18) % 4.29/4.39 %MaxLitNum:5 % 4.29/4.39 %MaxfuncDepth:1 % 4.29/4.39 %SharedTerms:9 % 4.29/4.39 %goalClause: 6 7 8 9 10 11 12 13 14 15 % 4.29/4.39 [6]P1(a1)+P1(a5) % 4.29/4.39 [7]~P1(x71)+E(a5,x71)+P1(a1) % 4.29/4.39 [8]~P1(x82)+~P1(x81)+E(x81,x82)+P1(a5) % 4.29/4.39 [9]~P1(x91)+~P1(x92)+~E(f2(x91),x91)+~E(a3,a4) % 4.29/4.39 [11]~P1(x111)+~P1(x112)+~E(f2(x111),x111)+P1(a4) % 4.29/4.39 [12]~P1(x121)+~P1(x122)+~E(f2(x121),x121)+P1(a3) % 4.29/4.39 [13]~P1(x131)+~P1(x132)+~E(a3,a4)+P1(f2(x131)) % 4.29/4.39 [14]~P1(x141)+~P1(x142)+P1(a4)+P1(f2(x141)) % 4.29/4.39 [15]~P1(x151)+~P1(x152)+P1(a3)+P1(f2(x151)) % 4.29/4.39 [10]~P1(x102)+~P1(x101)+~P1(x103)+E(x101,x102)+E(a5,x103) % 4.29/4.39 %EqnAxiom % 4.29/4.39 [1]E(x11,x11) % 4.29/4.39 [2]E(x22,x21)+~E(x21,x22) % 4.29/4.39 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 4.29/4.39 [4]~E(x41,x42)+E(f2(x41),f2(x42)) % 4.29/4.39 [5]~P1(x51)+P1(x52)+~E(x51,x52) % 4.29/4.39 % 4.29/4.39 %------------------------------------------- % 4.29/4.39 cnf(16,plain, % 4.29/4.39 (~E(a1,x161)+P1(x161)+P1(a5)), % 4.29/4.39 inference(scs_inference,[],[6,5])). % 4.29/4.39 cnf(20,plain, % 4.29/4.39 (~E(x201,x202)+E(x203,x201)+~E(x203,x202)), % 4.29/4.39 inference(scs_inference,[],[3,2])). % 4.29/4.39 cnf(21,plain, % 4.29/4.39 (~E(x211,x212)+~E(x213,x211)+E(x212,x213)), % 4.29/4.39 inference(scs_inference,[],[20,2])). % 4.29/4.39 cnf(24,plain, % 4.29/4.39 (~E(f2(a5),a5)+~E(a3,a4)+P1(a1)), % 4.29/4.39 inference(scs_inference,[],[6,9])). % 4.29/4.39 cnf(25,plain, % 4.29/4.39 (~E(a4,a3)+~E(f2(a5),a5)+P1(a1)), % 4.29/4.39 inference(scs_inference,[],[24,2])). % 4.29/4.40 cnf(26,plain, % 4.29/4.40 (~E(a5,f2(a5))+~E(a4,a3)+P1(a1)), % 4.29/4.40 inference(scs_inference,[],[25,2])). % 4.29/4.40 cnf(27,plain, % 4.29/4.40 (~P1(f2(a5))+~E(a4,a3)+P1(a1)), % 4.29/4.40 inference(scs_inference,[],[26,7])). % 4.29/4.40 cnf(28,plain, % 4.29/4.40 (~E(f2(a5),a5)+P1(a1)+P1(a4)), % 4.29/4.40 inference(scs_inference,[],[6,11])). % 4.29/4.40 cnf(35,plain, % 4.29/4.40 (P1(a1)+P1(a4)+P1(f2(a5))), % 4.29/4.40 inference(scs_inference,[],[6,14])). % 4.29/4.40 cnf(39,plain, % 4.29/4.40 (P1(a1)+P1(a3)+P1(f2(a5))), % 4.29/4.40 inference(scs_inference,[],[6,15])). % 4.29/4.40 cnf(40,plain, % 4.29/4.40 (E(a5,f2(a5))+P1(a3)+P1(a1)), % 4.29/4.40 inference(scs_inference,[],[39,7])). % 4.29/4.40 cnf(47,plain, % 4.29/4.40 (~E(f2(a5),a5)+P1(a1)+P1(a3)), % 4.29/4.40 inference(scs_inference,[],[6,12])). % 4.29/4.40 cnf(48,plain, % 4.29/4.40 (~E(a5,f2(a5))+P1(a1)+P1(a3)), % 4.29/4.40 inference(scs_inference,[],[47,2])). % 4.29/4.40 cnf(49,plain, % 4.29/4.40 (~P1(f2(a5))+P1(a3)+P1(a1)), % 4.29/4.40 inference(scs_inference,[],[48,7])). % 4.29/4.40 cnf(50,plain, % 4.29/4.40 (P1(a3)+P1(a1)+P1(a4)), % 4.29/4.40 inference(scs_inference,[],[49,35])). % 4.29/4.40 cnf(51,plain, % 4.29/4.40 (E(a5,a3)+P1(a4)+P1(a1)), % 4.29/4.40 inference(scs_inference,[],[50,7])). % 4.29/4.40 cnf(54,plain, % 4.29/4.40 (~E(a3,a4)+P1(a1)+P1(f2(a5))), % 4.29/4.40 inference(scs_inference,[],[6,13])). % 4.29/4.40 cnf(55,plain, % 4.29/4.40 (~E(a4,a3)+P1(f2(a5))+P1(a1)), % 4.29/4.40 inference(scs_inference,[],[54,2])). % 4.29/4.40 cnf(56,plain, % 4.29/4.40 (~E(a4,a3)+P1(a1)), % 4.29/4.40 inference(scs_inference,[],[55,27])). % 4.29/4.40 cnf(57,plain, % 4.29/4.40 (~E(a3,a4)+P1(a1)), % 4.29/4.40 inference(scs_inference,[],[56,2])). % 4.29/4.40 cnf(58,plain, % 4.29/4.40 (~E(x581,a4)+~E(a3,x581)+P1(a1)), % 4.29/4.40 inference(scs_inference,[],[57,3])). % 4.29/4.40 cnf(59,plain, % 4.29/4.40 (~E(x591,a3)+~E(x591,a4)+P1(a1)), % 4.29/4.40 inference(scs_inference,[],[58,2])). % 4.29/4.40 cnf(60,plain, % 4.29/4.40 (~E(a4,x601)+~E(x601,a3)+P1(a1)), % 4.29/4.40 inference(scs_inference,[],[59,2])). % 4.29/4.40 cnf(77,plain, % 4.29/4.40 (~E(a3,a4)+~E(a4,a3)+P1(f2(a1))), % 4.29/4.40 inference(scs_inference,[],[56,13])). % 4.29/4.40 cnf(78,plain, % 4.29/4.40 (~E(a4,a3)+P1(f2(a1))), % 4.29/4.40 inference(scs_inference,[],[77,2])). % 4.29/4.40 cnf(79,plain, % 4.29/4.40 (~E(x791,a3)+~E(a4,x791)+P1(f2(a1))), % 4.29/4.40 inference(scs_inference,[],[78,3])). % 4.29/4.40 cnf(97,plain, % 4.29/4.40 (E(x971,a5)+~P1(x971)+P1(a1)), % 4.29/4.40 inference(scs_inference,[],[2,7])). % 4.29/4.40 cnf(98,plain, % 4.29/4.40 (~E(f2(a5),a5)+E(a4,a5)+P1(a1)), % 4.29/4.40 inference(scs_inference,[],[97,28])). % 4.29/4.40 cnf(99,plain, % 4.29/4.40 (~P1(f2(a5))+E(a4,a5)+P1(a1)), % 4.29/4.40 inference(scs_inference,[],[98,97])). % 4.29/4.40 cnf(100,plain, % 4.29/4.40 (E(a4,a5)+P1(a1)+P1(a4)), % 4.29/4.40 inference(scs_inference,[],[99,35])). % 4.29/4.40 cnf(101,plain, % 4.29/4.40 (~E(a5,a3)+P1(a4)+P1(a1)), % 4.29/4.40 inference(scs_inference,[],[100,60])). % 4.29/4.40 cnf(102,plain, % 4.29/4.40 (P1(a4)+P1(a1)), % 4.29/4.40 inference(scs_inference,[],[101,51])). % 4.29/4.40 cnf(114,plain, % 4.29/4.40 (P1(a4)+P1(f2(a1))), % 4.29/4.40 inference(scs_inference,[],[102,14])). % 4.29/4.40 cnf(136,plain, % 4.29/4.40 (~E(x1361,x1362)+~E(x1361,x1363)+E(x1362,x1363)), % 4.29/4.40 inference(scs_inference,[],[2,3])). % 4.29/4.40 cnf(140,plain, % 4.29/4.40 (~E(x1401,x1402)+~P1(x1402)+P1(x1401)), % 4.29/4.40 inference(scs_inference,[],[2,5])). % 4.29/4.40 cnf(142,plain, % 4.29/4.40 (E(f2(a5),a5)+P1(a3)+P1(a1)), % 4.29/4.40 inference(scs_inference,[],[2,40])). % 4.29/4.40 cnf(143,plain, % 4.29/4.40 (P1(a1)+P1(a3)), % 4.29/4.40 inference(scs_inference,[],[142,47])). % 4.29/4.40 cnf(146,plain, % 4.29/4.40 (P1(a3)+P1(f2(a1))), % 4.29/4.40 inference(scs_inference,[],[143,15])). % 4.29/4.40 cnf(149,plain, % 4.29/4.40 (~E(f2(a1),a1)+P1(a3)), % 4.29/4.40 inference(scs_inference,[],[143,12])). % 4.29/4.40 cnf(239,plain, % 4.29/4.40 (~P1(f2(x2391))+P1(f2(x2392))+~E(x2392,x2391)), % 4.29/4.40 inference(scs_inference,[],[4,140])). % 4.29/4.40 cnf(293,plain, % 4.29/4.40 (~P1(a3)+~E(a5,a4)+P1(a1)), % 4.29/4.40 inference(scs_inference,[],[97,58])). % 4.29/4.40 cnf(294,plain, % 4.29/4.40 (~P1(a4)+~P1(a3)+P1(a1)), % 4.29/4.40 inference(scs_inference,[],[293,7])). % 4.29/4.40 cnf(295,plain, % 4.29/4.40 (~P1(a3)+P1(a1)), % 4.29/4.40 inference(scs_inference,[],[294,102])). % 4.29/4.40 cnf(296,plain, % 4.29/4.40 (P1(a1)), % 4.29/4.40 inference(scs_inference,[],[295,143])). % 4.29/4.40 cnf(297,plain, % 4.29/4.40 (~P1(x2971)+~E(a3,a4)+~E(f2(x2971),x2971)), % 4.29/4.40 inference(scs_inference,[],[296,9])). % 4.29/4.40 cnf(298,plain, % 4.29/4.40 (~P1(x2981)+~E(f2(x2981),x2981)+P1(a4)), % 4.29/4.40 inference(scs_inference,[],[296,11])). % 4.29/4.40 cnf(299,plain, % 4.29/4.40 (~P1(x2991)+~E(f2(x2991),x2991)+P1(a3)), % 4.29/4.40 inference(scs_inference,[],[296,12])). % 4.29/4.40 cnf(300,plain, % 4.29/4.40 (~P1(x3001)+~E(a3,a4)+P1(f2(x3001))), % 4.29/4.40 inference(scs_inference,[],[296,13])). % 4.29/4.40 cnf(301,plain, % 4.29/4.40 (~P1(x3011)+P1(a4)+P1(f2(x3011))), % 4.29/4.40 inference(scs_inference,[],[296,14])). % 4.29/4.40 cnf(302,plain, % 4.29/4.40 (~P1(x3021)+P1(a3)+P1(f2(x3021))), % 4.29/4.40 inference(scs_inference,[],[296,15])). % 4.29/4.40 cnf(303,plain, % 4.29/4.40 (P1(x3031)+~E(x3031,a1)), % 4.29/4.40 inference(scs_inference,[],[296,140])). % 4.29/4.40 cnf(307,plain, % 4.29/4.40 (P1(f2(a5))+~E(a1,a5)+P1(a3)), % 4.29/4.40 inference(scs_inference,[],[302,16])). % 4.29/4.40 cnf(390,plain, % 4.29/4.40 (~P1(a1)+~P1(f2(a1))+P1(a4)+P1(a5)), % 4.29/4.40 inference(scs_inference,[],[296,298,8])). % 4.29/4.40 cnf(391,plain, % 4.29/4.40 (~P1(f2(a1))+P1(a5)+P1(a4)), % 4.29/4.40 inference(scs_inference,[],[296,390])). % 4.29/4.40 cnf(394,plain, % 4.29/4.40 (~E(f2(a5),a5)+~P1(f2(a1))+P1(a4)), % 4.29/4.40 inference(scs_inference,[],[391,298])). % 4.29/4.40 cnf(395,plain, % 4.29/4.40 (~E(a5,f2(a5))+~P1(f2(a1))+P1(a4)), % 4.29/4.40 inference(scs_inference,[],[394,2])). % 4.29/4.40 cnf(396,plain, % 4.29/4.40 (~E(a5,f2(a5))+P1(a4)), % 4.29/4.40 inference(scs_inference,[],[395,114])). % 4.29/4.40 cnf(405,plain, % 4.29/4.40 (~P1(a5)+~P1(f2(a5))+P1(a4)), % 4.29/4.40 inference(scs_inference,[],[396,10])). % 4.29/4.40 cnf(416,plain, % 4.29/4.40 (P1(a5)+P1(a4)), % 4.29/4.40 inference(scs_inference,[],[391,114])). % 4.29/4.40 cnf(428,plain, % 4.29/4.40 (P1(f2(a5))+P1(a4)), % 4.29/4.40 inference(scs_inference,[],[416,301])). % 4.29/4.40 cnf(431,plain, % 4.29/4.40 (~E(f2(a4),a4)+~E(a3,a4)+P1(a5)), % 4.29/4.40 inference(scs_inference,[],[416,297])). % 4.29/4.40 cnf(432,plain, % 4.29/4.40 (~E(a4,a3)+~E(f2(a4),a4)+P1(a5)), % 4.29/4.40 inference(scs_inference,[],[431,2])). % 4.29/4.40 cnf(433,plain, % 4.29/4.40 (~P1(f2(a5))+P1(a4)), % 4.29/4.40 inference(scs_inference,[],[416,405])). % 4.29/4.40 cnf(445,plain, % 4.29/4.40 (P1(a4)), % 4.29/4.40 inference(scs_inference,[],[428,433])). % 4.29/4.40 cnf(446,plain, % 4.29/4.40 (P1(x4461)+~E(x4461,a4)), % 4.29/4.40 inference(scs_inference,[],[445,140])). % 4.29/4.40 cnf(455,plain, % 4.29/4.40 (~P1(a3)+~E(f2(a4),a4)+P1(a5)), % 4.29/4.40 inference(scs_inference,[],[445,432,8])). % 4.29/4.40 cnf(456,plain, % 4.29/4.40 (~P1(f2(a4))+~P1(a3)+P1(a5)), % 4.29/4.40 inference(scs_inference,[],[445,455,8])). % 4.29/4.40 cnf(457,plain, % 4.29/4.40 (~E(a3,a4)+~P1(a3)+P1(a5)), % 4.29/4.40 inference(scs_inference,[],[445,456,300])). % 4.29/4.40 cnf(458,plain, % 4.29/4.40 (~P1(a3)+P1(a5)), % 4.29/4.40 inference(scs_inference,[],[445,457,8])). % 4.29/4.40 cnf(476,plain, % 4.29/4.40 (~E(f2(a1),a1)+P1(a5)), % 4.29/4.40 inference(scs_inference,[],[458,149])). % 4.29/4.40 cnf(477,plain, % 4.29/4.40 (~E(a1,f2(a1))+P1(a5)), % 4.29/4.40 inference(scs_inference,[],[476,2])). % 4.29/4.40 cnf(478,plain, % 4.29/4.40 (~E(x4781,f2(a1))+~E(a1,x4781)+P1(a5)), % 4.29/4.40 inference(scs_inference,[],[477,3])). % 4.29/4.40 cnf(479,plain, % 4.29/4.40 (~P1(f2(a1))+P1(a5)), % 4.29/4.40 inference(scs_inference,[],[296,478,8])). % 4.29/4.40 cnf(480,plain, % 4.29/4.40 (P1(a5)+P1(a3)), % 4.29/4.40 inference(scs_inference,[],[479,146])). % 4.29/4.40 cnf(486,plain, % 4.29/4.40 (P1(f2(a5))+~E(a3,a4)+~P1(a3)), % 4.29/4.40 inference(scs_inference,[],[458,300])). % 4.29/4.40 cnf(487,plain, % 4.29/4.40 (~P1(a3)+P1(f2(a5))+E(a5,a1)), % 4.29/4.40 inference(scs_inference,[],[445,296,486,10])). % 4.29/4.40 cnf(488,plain, % 4.29/4.40 (~P1(f2(a1))+P1(f2(a5))+~P1(a3)), % 4.29/4.40 inference(scs_inference,[],[487,239])). % 4.29/4.40 cnf(499,plain, % 4.29/4.40 (P1(a5)), % 4.29/4.40 inference(scs_inference,[],[480,458])). % 4.29/4.40 cnf(508,plain, % 4.29/4.40 (~E(f2(x5081),x5081)+~E(a3,a4)+~E(x5081,a4)), % 4.29/4.40 inference(scs_inference,[],[446,297])). % 4.29/4.40 cnf(509,plain, % 4.29/4.40 (~E(x5091,f2(x5091))+~E(a3,a4)+~E(x5091,a4)), % 4.29/4.40 inference(scs_inference,[],[508,2])). % 4.29/4.40 cnf(510,plain, % 4.29/4.40 (~P1(f2(a5))+~E(a3,a4)+~E(a5,a4)), % 4.29/4.40 inference(scs_inference,[],[499,509,10])). % 4.29/4.40 cnf(511,plain, % 4.29/4.40 (~E(a4,a3)+~E(a5,a4)+~P1(f2(a5))), % 4.29/4.40 inference(scs_inference,[],[510,2])). % 4.29/4.40 cnf(512,plain, % 4.29/4.40 (~E(a4,a3)+~P1(f2(a5))), % 4.29/4.40 inference(scs_inference,[],[499,445,511,10])). % 4.29/4.40 cnf(513,plain, % 4.29/4.40 (~E(a3,a4)+~P1(f2(a5))), % 4.29/4.40 inference(scs_inference,[],[512,2])). % 4.29/4.40 cnf(514,plain, % 4.29/4.40 (~E(x5141,a4)+~E(a3,x5141)+~P1(f2(a5))), % 4.29/4.40 inference(scs_inference,[],[513,3])). % 4.29/4.40 cnf(515,plain, % 4.29/4.40 (~E(x5151,a3)+~E(x5151,a4)+~P1(f2(a5))), % 4.29/4.40 inference(scs_inference,[],[514,2])). % 4.29/4.40 cnf(516,plain, % 4.29/4.40 (~E(a5,a3)+~P1(f2(a5))), % 4.29/4.40 inference(scs_inference,[],[499,445,515,10])). % 4.29/4.40 cnf(526,plain, % 4.29/4.40 (~E(a5,a3)+~E(f2(a5),a4)), % 4.29/4.40 inference(scs_inference,[],[446,516])). % 4.29/4.40 cnf(527,plain, % 4.29/4.40 (~E(a3,a5)+~E(f2(a5),a4)), % 4.29/4.40 inference(scs_inference,[],[526,2])). % 4.29/4.40 cnf(528,plain, % 4.29/4.40 (~E(x5281,a5)+~E(a3,x5281)+~E(f2(a5),a4)), % 4.29/4.40 inference(scs_inference,[],[527,3])). % 4.29/4.40 cnf(529,plain, % 4.29/4.40 (~E(a4,f2(a5))+~E(a3,x5291)+~E(x5291,a5)), % 4.29/4.40 inference(scs_inference,[],[528,2])). % 4.29/4.40 cnf(530,plain, % 4.29/4.40 (~E(a5,x5301)+~E(a3,x5301)+~E(a4,f2(a5))), % 4.29/4.40 inference(scs_inference,[],[529,2])). % 4.29/4.40 cnf(531,plain, % 4.29/4.40 (~E(x5311,a3)+~E(a5,x5311)+~E(a4,f2(a5))), % 4.29/4.40 inference(scs_inference,[],[530,2])). % 4.29/4.40 cnf(532,plain, % 4.29/4.40 (E(a5,a4)+~E(a4,a3)+~E(a4,f2(a5))), % 4.29/4.40 inference(scs_inference,[],[445,499,531,10])). % 4.29/4.40 cnf(533,plain, % 4.29/4.40 (~E(a3,a4)+E(a5,a4)+~E(a4,f2(a5))), % 4.29/4.40 inference(scs_inference,[],[532,2])). % 4.29/4.40 cnf(534,plain, % 4.29/4.40 (~E(a3,a4)+~E(a4,f2(a5))), % 4.29/4.40 inference(scs_inference,[],[533,530])). % 4.29/4.40 cnf(535,plain, % 4.29/4.40 (~E(a4,a3)+~E(a4,f2(a5))), % 4.29/4.40 inference(scs_inference,[],[534,2])). % 4.29/4.40 cnf(536,plain, % 4.29/4.40 (~E(a4,x5361)+~E(a3,x5361)+~E(a4,f2(a5))), % 4.29/4.40 inference(scs_inference,[],[535,20])). % 4.29/4.40 cnf(537,plain, % 4.29/4.40 (~E(x5371,a3)+~E(a4,x5371)+~E(a4,f2(a5))), % 4.29/4.40 inference(scs_inference,[],[536,2])). % 4.29/4.40 cnf(538,plain, % 4.29/4.40 (~P1(a3)+~E(a4,a5)+~E(a4,f2(a5))), % 4.29/4.40 inference(scs_inference,[],[499,537,10])). % 4.29/4.40 cnf(539,plain, % 4.29/4.40 (~E(a5,a4)+~E(a4,f2(a5))+~P1(a3)), % 4.29/4.40 inference(scs_inference,[],[538,2])). % 4.29/4.40 cnf(540,plain, % 4.29/4.40 (~E(a4,f2(a5))+~P1(a3)), % 4.29/4.40 inference(scs_inference,[],[499,445,539,10])). % 4.29/4.40 cnf(541,plain, % 4.29/4.40 (~E(f2(a5),a4)+~P1(a3)), % 4.29/4.40 inference(scs_inference,[],[540,2])). % 4.29/4.40 cnf(545,plain, % 4.29/4.40 (~E(f2(x5451),x5451)+~E(x5451,a4)+P1(a3)), % 4.29/4.40 inference(scs_inference,[],[446,299])). % 4.29/4.40 cnf(546,plain, % 4.29/4.40 (~E(x5461,f2(x5461))+~E(x5461,a4)+P1(a3)), % 4.29/4.40 inference(scs_inference,[],[545,2])). % 4.29/4.40 cnf(547,plain, % 4.29/4.40 (~P1(f2(a5))+~E(a5,a4)+P1(a3)), % 4.29/4.40 inference(scs_inference,[],[499,546,10])). % 4.29/4.40 cnf(548,plain, % 4.40/4.40 (~P1(f2(a5))+P1(a3)), % 4.40/4.40 inference(scs_inference,[],[499,445,547,10])). % 4.40/4.40 cnf(549,plain, % 4.40/4.40 (~E(f2(a5),a1)+P1(a3)), % 4.40/4.41 inference(scs_inference,[],[548,303])). % 4.40/4.41 cnf(550,plain, % 4.40/4.41 (~E(a1,f2(a5))+P1(a3)), % 4.40/4.41 inference(scs_inference,[],[549,2])). % 4.40/4.41 cnf(551,plain, % 4.40/4.41 (~E(x5511,f2(a5))+~E(a1,x5511)+P1(a3)), % 4.40/4.41 inference(scs_inference,[],[550,3])). % 4.40/4.41 cnf(552,plain, % 4.40/4.41 (~E(a4,f2(a5))+E(a5,a4)+P1(a3)), % 4.40/4.41 inference(scs_inference,[],[445,296,551,10])). % 4.40/4.41 cnf(553,plain, % 4.40/4.41 (~E(f2(a5),a5)+~E(a4,f2(a5))+P1(a3)), % 4.40/4.41 inference(scs_inference,[],[552,545])). % 4.40/4.41 cnf(554,plain, % 4.40/4.41 (~E(a5,f2(a5))+~E(a4,f2(a5))+P1(a3)), % 4.40/4.41 inference(scs_inference,[],[553,2])). % 4.40/4.41 cnf(555,plain, % 4.40/4.41 (~E(f2(a5),a4)+~E(a5,f2(a5))+P1(a3)), % 4.40/4.41 inference(scs_inference,[],[554,2])). % 4.40/4.41 cnf(556,plain, % 4.40/4.41 (~E(a5,f2(a5))+~E(f2(a5),a4)), % 4.40/4.41 inference(scs_inference,[],[555,541])). % 4.40/4.41 cnf(557,plain, % 4.40/4.41 (~E(f2(a5),a5)+~E(f2(a5),a4)), % 4.40/4.41 inference(scs_inference,[],[556,2])). % 4.40/4.41 cnf(558,plain, % 4.40/4.41 (~E(f2(a5),x5581)+~E(a5,x5581)+~E(f2(a5),a4)), % 4.40/4.41 inference(scs_inference,[],[557,20])). % 4.40/4.41 cnf(559,plain, % 4.40/4.41 (~E(a4,f2(a5))+~E(a5,a4)), % 4.40/4.41 inference(scs_inference,[],[558,2])). % 4.40/4.41 cnf(560,plain, % 4.40/4.41 (~E(a4,f2(a5))), % 4.40/4.41 inference(scs_inference,[],[499,445,559,10])). % 4.40/4.41 cnf(567,plain, % 4.40/4.41 (~E(a5,f2(a5))), % 4.40/4.41 inference(scs_inference,[],[445,499,560,2,136,10])). % 4.40/4.41 cnf(570,plain, % 4.40/4.41 (~P1(f2(a5))), % 4.40/4.41 inference(scs_inference,[],[499,567,2,10])). % 4.40/4.41 cnf(579,plain, % 4.40/4.41 (~E(a1,a5)+P1(a3)), % 4.40/4.41 inference(scs_inference,[],[570,307])). % 4.40/4.41 cnf(581,plain, % 4.40/4.41 (E(a5,a1)+~P1(a3)), % 4.40/4.41 inference(scs_inference,[],[570,487])). % 4.40/4.41 cnf(582,plain, % 4.40/4.41 (~P1(f2(a1))+~P1(a3)), % 4.40/4.41 inference(scs_inference,[],[570,488])). % 4.40/4.41 cnf(598,plain, % 4.40/4.41 (~E(a5,a1)+P1(a3)), % 4.40/4.41 inference(scs_inference,[],[579,2])). % 4.40/4.41 cnf(602,plain, % 4.40/4.41 (P1(a3)), % 4.40/4.41 inference(scs_inference,[],[499,296,598,10])). % 4.40/4.41 cnf(605,plain, % 4.40/4.41 (E(a5,a1)), % 4.40/4.41 inference(scs_inference,[],[602,581])). % 4.40/4.41 cnf(606,plain, % 4.40/4.41 (~P1(f2(a1))), % 4.40/4.41 inference(scs_inference,[],[602,582])). % 4.40/4.41 cnf(618,plain, % 4.40/4.41 (~E(a4,x6181)+~E(x6181,a3)), % 4.40/4.41 inference(scs_inference,[],[606,79])). % 4.40/4.41 cnf(644,plain, % 4.40/4.41 (~E(a4,a5)), % 4.40/4.41 inference(scs_inference,[],[499,602,618,10])). % 4.40/4.41 cnf(648,plain, % 4.40/4.41 ($false), % 4.40/4.41 inference(scs_inference,[],[605,445,499,644,2,20,21,10]), % 4.40/4.41 ['proof']). % 4.40/4.41 % SZS output end Proof % 4.40/4.41 % Total time :3.770000s %------------------------------------------------------------------------------