%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SET887+1 : 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 : n022.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 14:22:54 EDT 2024 % Result : Theorem 116.61s 117.36s % Output : CNFRefutation 116.68s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.11 % Problem : SET887+1 : TPTP v8.2.0. Released v3.2.0. % 0.06/0.11 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.11/0.32 % Computer : n022.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.11/0.32 % WCLimit : 300 % 0.11/0.32 % DateTime : Sun Jun 23 15:13:08 EDT 2024 % 0.11/0.32 % CPUTime : % 0.48/0.56 start to proof:theBenchmark % 116.61/117.34 %------------------------------------------- % 116.61/117.34 % File :CSE---1.7 % 116.61/117.34 % Problem :theBenchmark % 116.61/117.34 % Transform :cnf % 116.61/117.34 % Format :tptp:raw % 116.61/117.34 % Command :java -jar mcs_scs.jar %d %s % 116.61/117.34 % 116.61/117.34 % Result :Theorem 116.070000s % 116.61/117.34 % Output :CNFRefutation 116.070000s % 116.61/117.34 %------------------------------------------- % 116.61/117.36 %------------------------------------------------------------------------------ % 116.61/117.36 % File : SET887+1 : TPTP v8.2.0. Released v3.2.0. % 116.61/117.36 % Domain : Set theory % 116.61/117.36 % Problem : ~ ( subset(uno_pair(A,B),uno_pair(C,D)) & A != C & A != D ) % 116.61/117.36 % Version : [Urb06] axioms : Especial. % 116.61/117.36 % English : % 116.61/117.36 % 116.61/117.36 % Refs : [Byl90] Bylinski (1990), Some Basic Properties of Sets % 116.61/117.36 % : [Urb06] Urban (2006), Email to G. Sutcliffe % 116.61/117.36 % Source : [Urb06] % 116.61/117.36 % Names : zfmisc_1__t28_zfmisc_1 [Urb06] % 116.61/117.36 % 116.61/117.36 % Status : Theorem % 116.61/117.36 % Rating : 0.28 v8.1.0, 0.25 v7.5.0, 0.28 v7.4.0, 0.23 v7.3.0, 0.28 v7.2.0, 0.24 v7.1.0, 0.22 v7.0.0, 0.20 v6.4.0, 0.19 v6.3.0, 0.29 v6.2.0, 0.36 v6.1.0, 0.43 v6.0.0, 0.39 v5.5.0, 0.37 v5.4.0, 0.32 v5.3.0, 0.44 v5.2.0, 0.30 v5.1.0, 0.33 v5.0.0, 0.38 v4.1.0, 0.39 v4.0.0, 0.38 v3.7.0, 0.30 v3.5.0, 0.37 v3.4.0, 0.42 v3.3.0, 0.36 v3.2.0 % 116.61/117.36 % Syntax : Number of formulae : 12 ( 5 unt; 0 def) % 116.61/117.36 % Number of atoms : 26 ( 16 equ) % 116.61/117.36 % Maximal formula atoms : 5 ( 2 avg) % 116.61/117.36 % Number of connectives : 28 ( 14 ~; 1 |; 7 &) % 116.61/117.36 % ( 4 <=>; 2 =>; 0 <=; 0 <~>) % 116.61/117.36 % Maximal formula depth : 10 ( 5 avg) % 116.61/117.36 % Maximal term depth : 2 ( 1 avg) % 116.61/117.36 % Number of predicates : 4 ( 3 usr; 0 prp; 1-2 aty) % 116.61/117.36 % Number of functors : 3 ( 3 usr; 1 con; 0-2 aty) % 116.61/117.36 % Number of variables : 28 ( 26 !; 2 ?) % 116.61/117.36 % SPC : FOF_THM_RFO_SEQ % 116.61/117.36 % 116.61/117.36 % Comments : Translated by MPTP 0.2 from the original problem in the Mizar % 116.61/117.36 % library, www.mizar.org % 116.61/117.36 %------------------------------------------------------------------------------ % 116.61/117.36 fof(antisymmetry_r2_hidden,axiom, % 116.61/117.36 ! [A,B] : % 116.61/117.36 ( in(A,B) % 116.61/117.36 => ~ in(B,A) ) ). % 116.61/117.36 % 116.61/117.36 fof(commutativity_k2_tarski,axiom, % 116.61/117.36 ! [A,B] : unordered_pair(A,B) = unordered_pair(B,A) ). % 116.61/117.36 % 116.61/117.36 fof(d1_xboole_0,axiom, % 116.61/117.36 ! [A] : % 116.61/117.36 ( A = empty_set % 116.61/117.36 <=> ! [B] : ~ in(B,A) ) ). % 116.61/117.36 % 116.61/117.36 fof(d2_tarski,axiom, % 116.61/117.36 ! [A,B,C] : % 116.61/117.36 ( C = unordered_pair(A,B) % 116.61/117.36 <=> ! [D] : % 116.61/117.36 ( in(D,C) % 116.61/117.36 <=> ( D = A % 116.61/117.36 | D = B ) ) ) ). % 116.61/117.36 % 116.61/117.36 fof(fc1_xboole_0,axiom, % 116.61/117.36 empty(empty_set) ). % 116.61/117.36 % 116.61/117.36 fof(l46_zfmisc_1,axiom, % 116.61/117.36 ! [A,B,C] : % 116.61/117.36 ( subset(A,unordered_pair(B,C)) % 116.61/117.36 <=> ~ ( A != empty_set % 116.61/117.36 & A != singleton(B) % 116.61/117.36 & A != singleton(C) % 116.61/117.36 & A != unordered_pair(B,C) ) ) ). % 116.61/117.36 % 116.61/117.36 fof(rc1_xboole_0,axiom, % 116.61/117.36 ? [A] : empty(A) ). % 116.61/117.36 % 116.61/117.36 fof(rc2_xboole_0,axiom, % 116.61/117.36 ? [A] : ~ empty(A) ). % 116.61/117.36 % 116.61/117.36 fof(reflexivity_r1_tarski,axiom, % 116.61/117.36 ! [A,B] : subset(A,A) ). % 116.61/117.36 % 116.61/117.36 fof(t10_zfmisc_1,axiom, % 116.61/117.36 ! [A,B,C,D] : % 116.61/117.36 ~ ( unordered_pair(A,B) = unordered_pair(C,D) % 116.61/117.36 & A != C % 116.61/117.36 & A != D ) ). % 116.61/117.36 % 116.61/117.36 fof(t28_zfmisc_1,conjecture, % 116.61/117.36 ! [A,B,C,D] : % 116.61/117.36 ~ ( subset(unordered_pair(A,B),unordered_pair(C,D)) % 116.61/117.36 & A != C % 116.61/117.36 & A != D ) ). % 116.61/117.36 % 116.61/117.36 fof(t8_zfmisc_1,axiom, % 116.61/117.36 ! [A,B,C] : % 116.61/117.36 ( singleton(A) = unordered_pair(B,C) % 116.61/117.36 => A = B ) ). % 116.61/117.36 % 116.61/117.36 %------------------------------------------------------------------------------ % 116.61/117.36 %------------------------------------------- % 116.61/117.36 % Proof found % 116.61/117.36 % SZS status Theorem for theBenchmark % 116.61/117.36 % SZS output start Proof % 116.68/117.38 %ClaNum:39(EqnAxiom:15) % 116.68/117.38 %VarNum:120(SingletonVarNum:51) % 116.68/117.38 %MaxLitNum:5 % 116.68/117.38 %MaxfuncDepth:1 % 116.68/117.38 %SharedTerms:15 % 116.68/117.38 %goalClause: 20 21 22 % 116.68/117.38 %singleGoalClaCount:3 % 116.68/117.38 [16]P1(a1) % 116.68/117.38 [17]P1(a2) % 116.68/117.38 [21]~E(a9,a6) % 116.68/117.38 [22]~E(a10,a6) % 116.68/117.38 [23]~P1(a7) % 116.68/117.38 [20]P2(f5(a6,a8),f5(a9,a10)) % 116.68/117.38 [18]P2(x181,x181) % 116.68/117.38 [19]E(f5(x191,x192),f5(x192,x191)) % 116.68/117.38 [24]P3(f3(x241),x241)+E(x241,a1) % 116.68/117.38 [25]~P3(x252,x251)+~E(x251,a1) % 116.68/117.38 [30]~P3(x302,x301)+~P3(x301,x302) % 116.68/117.38 [26]E(x261,x262)+~E(f11(x261),f5(x262,x263)) % 116.68/117.38 [29]~E(x291,a1)+P2(x291,f5(x292,x293)) % 116.68/117.38 [31]~E(x311,f11(x313))+P2(x311,f5(x312,x313)) % 116.68/117.38 [32]~E(x321,f11(x322))+P2(x321,f5(x322,x323)) % 116.68/117.38 [35]P2(x351,f5(x352,x353))+~E(x351,f5(x352,x353)) % 116.68/117.38 [38]~E(f4(x382,x383,x381),x383)+~P3(f4(x382,x383,x381),x381)+E(x381,f5(x382,x383)) % 116.68/117.38 [39]~E(f4(x392,x393,x391),x392)+~P3(f4(x392,x393,x391),x391)+E(x391,f5(x392,x393)) % 116.68/117.38 [27]P3(x271,x272)+~E(x271,x273)+~E(x272,f5(x274,x273)) % 116.68/117.38 [28]P3(x281,x282)+~E(x281,x283)+~E(x282,f5(x283,x284)) % 116.68/117.38 [33]E(x331,x332)+E(x331,x333)+~E(f5(x331,x334),f5(x333,x332)) % 116.68/117.38 [37]E(f4(x372,x373,x371),x373)+E(f4(x372,x373,x371),x372)+P3(f4(x372,x373,x371),x371)+E(x371,f5(x372,x373)) % 116.68/117.38 [34]~P3(x341,x344)+E(x341,x342)+E(x341,x343)+~E(x344,f5(x343,x342)) % 116.68/117.38 [36]E(x361,f5(x363,x362))+~P2(x361,f5(x363,x362))+E(x361,a1)+E(x361,f11(x362))+E(x361,f11(x363)) % 116.68/117.38 %EqnAxiom % 116.68/117.38 [1]E(x11,x11) % 116.68/117.38 [2]E(x22,x21)+~E(x21,x22) % 116.68/117.38 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 116.68/117.38 [4]~E(x41,x42)+E(f5(x41,x43),f5(x42,x43)) % 116.68/117.38 [5]~E(x51,x52)+E(f5(x53,x51),f5(x53,x52)) % 116.68/117.38 [6]~E(x61,x62)+E(f4(x61,x63,x64),f4(x62,x63,x64)) % 116.68/117.38 [7]~E(x71,x72)+E(f4(x73,x71,x74),f4(x73,x72,x74)) % 116.68/117.38 [8]~E(x81,x82)+E(f4(x83,x84,x81),f4(x83,x84,x82)) % 116.68/117.38 [9]~E(x91,x92)+E(f11(x91),f11(x92)) % 116.68/117.38 [10]~E(x101,x102)+E(f3(x101),f3(x102)) % 116.68/117.38 [11]~P1(x111)+P1(x112)+~E(x111,x112) % 116.68/117.38 [12]P3(x122,x123)+~E(x121,x122)+~P3(x121,x123) % 116.68/117.38 [13]P3(x133,x132)+~E(x131,x132)+~P3(x133,x131) % 116.68/117.38 [14]P2(x142,x143)+~E(x141,x142)+~P2(x141,x143) % 116.68/117.38 [15]P2(x153,x152)+~E(x151,x152)+~P2(x153,x151) % 116.68/117.38 % 116.68/117.38 %------------------------------------------- % 116.68/117.40 cnf(40,plain, % 116.68/117.40 (~P3(x401,a1)), % 116.68/117.40 inference(equality_inference,[],[25])). % 116.68/117.40 cnf(41,plain, % 116.68/117.40 (P2(a1,f5(x411,x412))), % 116.68/117.40 inference(equality_inference,[],[29])). % 116.68/117.40 cnf(42,plain, % 116.68/117.40 (P2(f11(x421),f5(x422,x421))), % 116.68/117.40 inference(equality_inference,[],[31])). % 116.68/117.40 cnf(45,plain, % 116.68/117.40 (~P3(x451,f5(x452,x453))+E(x451,x453)+E(x451,x452)), % 116.68/117.40 inference(equality_inference,[],[34])). % 116.68/117.40 cnf(47,plain, % 116.68/117.40 (~P3(a9,f5(a6,a6))), % 116.68/117.40 inference(scs_inference,[],[21,45])). % 116.68/117.40 cnf(54,plain, % 116.68/117.40 (~P3(a10,f5(a6,a6))), % 116.68/117.40 inference(scs_inference,[],[22,45])). % 116.68/117.40 cnf(60,plain, % 116.68/117.40 (P2(x601,f5(x602,x603))+~E(f11(x603),x601)), % 116.68/117.40 inference(scs_inference,[],[42,14])). % 116.68/117.40 cnf(61,plain, % 116.68/117.40 (P2(x611,f5(x612,x613))+~E(f11(x612),x611)), % 116.68/117.40 inference(scs_inference,[],[42,19,14,15])). % 116.68/117.40 cnf(67,plain, % 116.68/117.40 (P2(x671,f5(x672,x673))+~E(a1,x671)), % 116.68/117.40 inference(scs_inference,[],[41,14])). % 116.68/117.40 cnf(69,plain, % 116.68/117.40 (E(f5(f5(x691,x692),x693),f5(f5(x692,x691),x693))), % 116.68/117.40 inference(scs_inference,[],[19,2,4])). % 116.68/117.40 cnf(70,plain, % 116.68/117.40 (~P3(x701,f3(x701))+E(x701,a1)), % 116.68/117.40 inference(scs_inference,[],[30,24])). % 116.68/117.40 cnf(71,plain, % 116.68/117.40 (~P3(f5(x711,x712),f3(f5(x712,x711)))+E(f5(x712,x711),a1)), % 116.68/117.40 inference(scs_inference,[],[19,70,12])). % 116.68/117.40 cnf(72,plain, % 116.68/117.40 (E(f11(f5(x721,f5(x722,x723))),f11(f5(x721,f5(x723,x722))))), % 116.68/117.40 inference(scs_inference,[],[19,9,5])). % 116.68/117.40 cnf(74,plain, % 116.68/117.40 (~E(f11(a6),f5(a10,x741))), % 116.68/117.40 inference(scs_inference,[],[22,26,2])). % 116.68/117.40 cnf(75,plain, % 116.68/117.40 (~E(f11(a6),f5(x751,a10))), % 116.68/117.40 inference(scs_inference,[],[74,19,3])). % 116.68/117.40 cnf(130,plain, % 116.68/117.40 (E(f5(x1301,x1302),a1)+~E(f3(f5(x1301,x1302)),f5(x1303,f5(x1301,x1302)))), % 116.68/117.40 inference(scs_inference,[],[19,71,27])). % 116.68/117.40 cnf(395,plain, % 116.68/117.40 (E(f5(x3951,f5(x3952,x3953)),f5(x3951,f5(x3953,x3952)))), % 116.68/117.40 inference(scs_inference,[],[19,2,5])). % 116.68/117.40 cnf(427,plain, % 116.68/117.40 (E(f4(x4271,f5(x4272,x4273),x4274),f4(x4271,f5(x4273,x4272),x4274))), % 116.68/117.40 inference(scs_inference,[],[19,2,7])). % 116.68/117.40 cnf(443,plain, % 116.68/117.40 (E(f4(x4431,x4432,f5(x4433,x4434)),f4(x4431,x4432,f5(x4434,x4433)))), % 116.68/117.40 inference(scs_inference,[],[19,2,8])). % 116.68/117.40 cnf(459,plain, % 116.68/117.40 (E(f11(f5(x4591,x4592)),f11(f5(x4592,x4591)))), % 116.68/117.40 inference(scs_inference,[],[19,2,9])). % 116.68/117.40 cnf(491,plain, % 116.68/117.40 (~E(f5(a6,x4911),f11(a10))), % 116.68/117.40 inference(scs_inference,[],[22,2,26])). % 116.68/117.40 cnf(492,plain, % 116.68/117.40 (~P3(f5(a6,x4921),f5(f11(a10),f11(a10)))), % 116.68/117.40 inference(scs_inference,[],[491,45])). % 116.68/117.40 cnf(509,plain, % 116.68/117.40 (~P3(x5091,f3(x5091))+E(a1,x5091)), % 116.68/117.40 inference(scs_inference,[],[2,70])). % 116.68/117.40 cnf(525,plain, % 116.68/117.40 (~P3(f5(x5251,x5252),f3(f5(x5252,x5251)))+E(a1,f5(x5252,x5251))), % 116.68/117.40 inference(scs_inference,[],[19,509,12])). % 116.68/117.40 cnf(541,plain, % 116.68/117.40 (E(a1,f5(x5411,x5412))+~E(f3(f5(x5411,x5412)),f5(x5413,f5(x5411,x5412)))), % 116.68/117.40 inference(scs_inference,[],[19,525,27])). % 116.68/117.40 cnf(572,plain, % 116.68/117.40 (~E(f5(a6,x5721),f11(a9))), % 116.68/117.40 inference(scs_inference,[],[21,2,26])). % 116.68/117.40 cnf(573,plain, % 116.68/117.40 (~P3(f5(a6,x5731),f5(f11(a9),f11(a9)))), % 116.68/117.40 inference(scs_inference,[],[572,45])). % 116.68/117.40 cnf(590,plain, % 116.68/117.40 (~E(f5(a6,x5901),f5(a10,a10))), % 116.68/117.40 inference(scs_inference,[],[22,2,33])). % 116.68/117.40 cnf(591,plain, % 116.68/117.40 (~E(a6,a10)), % 116.68/117.40 inference(scs_inference,[],[590,4])). % 116.68/117.40 cnf(592,plain, % 116.68/117.40 (~E(f5(a6,x5921),f5(a10,a10))), % 116.68/117.40 inference(rename_variables,[],[590])). % 116.68/117.40 cnf(593,plain, % 116.68/117.40 (~P3(f5(a6,x5931),f5(f5(a10,a10),f5(a10,a10)))), % 116.68/117.40 inference(scs_inference,[],[590,592,4,45])). % 116.68/117.40 cnf(603,plain, % 116.68/117.40 (~P3(a6,f5(a10,a10))), % 116.68/117.40 inference(scs_inference,[],[591,45])). % 116.68/117.40 cnf(605,plain, % 116.68/117.40 (E(f4(a10,a10,f5(a6,x6051)),a10)+P3(f4(a10,a10,f5(a6,x6051)),f5(a6,x6051))), % 116.68/117.40 inference(scs_inference,[],[590,591,45,37])). % 116.68/117.40 cnf(607,plain, % 116.68/117.40 (E(a10,f4(a10,a10,f5(a6,x6071)))+P3(f4(a10,a10,f5(a6,x6071)),f5(a6,x6071))), % 116.68/117.40 inference(scs_inference,[],[590,591,45,37,2])). % 116.68/117.40 cnf(609,plain, % 116.68/117.40 (~E(a6,f4(a10,a10,f5(a6,x6091)))+P3(f4(a10,a10,f5(a6,x6091)),f5(a6,x6091))), % 116.68/117.40 inference(scs_inference,[],[75,590,591,45,37,2,39,3])). % 116.68/117.40 cnf(705,plain, % 116.68/117.40 (~E(f5(a6,x7051),a1)+E(a10,f4(a10,a10,f5(a6,x7051)))), % 116.68/117.40 inference(scs_inference,[],[607,25])). % 116.68/117.40 cnf(909,plain, % 116.68/117.40 (~P3(f5(x9091,a6),f5(f5(a10,a10),f5(a10,a10)))), % 116.68/117.40 inference(scs_inference,[],[19,593,2,12])). % 116.68/117.40 cnf(925,plain, % 116.68/117.40 (E(f4(a6,x9251,f5(a10,a10)),x9251)+E(f4(a6,x9251,f5(a10,a10)),a6)+P3(f4(a6,x9251,f5(a10,a10)),f5(a10,a10))), % 116.68/117.40 inference(scs_inference,[],[590,2,37])). % 116.68/117.40 cnf(941,plain, % 116.68/117.40 (E(f4(a6,x9411,f5(a10,a10)),a10)+E(f4(a6,x9411,f5(a10,a10)),x9411)+E(f4(a6,x9411,f5(a10,a10)),a6)), % 116.68/117.40 inference(scs_inference,[],[925,45])). % 116.68/117.40 cnf(1004,plain, % 116.68/117.40 (~P3(f5(x10041,a6),f5(f11(a10),f11(a10)))), % 116.68/117.40 inference(scs_inference,[],[19,492,2,12])). % 116.68/117.40 cnf(1020,plain, % 116.68/117.40 (~E(f11(a6),f5(a9,x10201))), % 116.68/117.40 inference(scs_inference,[],[21,2,26])). % 116.68/117.40 cnf(1623,plain, % 116.68/117.40 (~P3(f5(x16231,a6),f5(f11(a9),f11(a9)))), % 116.68/117.40 inference(scs_inference,[],[19,573,2,12])). % 116.68/117.40 cnf(1639,plain, % 116.68/117.40 (~E(f5(a10,x16391),f11(a6))), % 116.68/117.40 inference(scs_inference,[],[75,19,2,3])). % 116.68/117.40 cnf(1640,plain, % 116.68/117.40 (~P3(f5(a10,x16401),f5(f11(a6),f11(a6)))), % 116.68/117.40 inference(scs_inference,[],[1639,45])). % 116.68/117.40 cnf(1784,plain, % 116.68/117.40 (E(a1,f5(a6,x17841))+~P2(f5(a6,x17841),f5(a10,a10))), % 116.68/117.40 inference(scs_inference,[],[590,491,2,36])). % 116.68/117.40 cnf(1796,plain, % 116.68/117.40 (~E(f11(a6),f5(x17961,a9))), % 116.68/117.40 inference(scs_inference,[],[1020,19,3])). % 116.68/117.40 cnf(2218,plain, % 116.68/117.40 (~E(f11(a9),f5(x22181,a6))), % 116.68/117.40 inference(scs_inference,[],[572,19,2,3])). % 116.68/117.40 cnf(2380,plain, % 116.68/117.40 (~E(f5(a6,x23801),f5(a9,a9))), % 116.68/117.40 inference(scs_inference,[],[21,2,33])). % 116.68/117.40 cnf(2381,plain, % 116.68/117.40 (~E(a6,a9)), % 116.68/117.40 inference(scs_inference,[],[2380,4])). % 116.68/117.40 cnf(2382,plain, % 116.68/117.40 (~E(f5(a6,x23821),f5(a9,a9))), % 116.68/117.40 inference(rename_variables,[],[2380])). % 116.68/117.40 cnf(2383,plain, % 116.68/117.40 (~P3(f5(a6,x23831),f5(f5(a9,a9),f5(a9,a9)))), % 116.68/117.40 inference(scs_inference,[],[2380,2382,4,45])). % 116.68/117.40 cnf(2391,plain, % 116.68/117.40 (~P3(a6,f5(a9,a9))), % 116.68/117.40 inference(scs_inference,[],[2381,45])). % 116.68/117.40 cnf(2393,plain, % 116.68/117.40 (E(f4(a9,a9,f5(a6,x23931)),a9)+P3(f4(a9,a9,f5(a6,x23931)),f5(a6,x23931))), % 116.68/117.40 inference(scs_inference,[],[2380,2381,45,37])). % 116.68/117.40 cnf(2395,plain, % 116.68/117.40 (E(a9,f4(a9,a9,f5(a6,x23951)))+P3(f4(a9,a9,f5(a6,x23951)),f5(a6,x23951))), % 116.68/117.40 inference(scs_inference,[],[2380,2381,45,37,2])). % 116.68/117.40 cnf(2396,plain, % 116.68/117.40 (~E(a6,f4(a9,a9,f5(a6,x23961)))+P3(f4(a9,a9,f5(a6,x23961)),f5(a6,x23961))), % 116.68/117.40 inference(scs_inference,[],[2380,2381,45,37,2,3])). % 116.68/117.40 cnf(2444,plain, % 116.68/117.40 (~E(f5(a6,x24441),a1)+E(a9,f4(a9,a9,f5(a6,x24441)))), % 116.68/117.40 inference(scs_inference,[],[2395,25])). % 116.68/117.40 cnf(2633,plain, % 116.68/117.40 (~P3(f5(x26331,a6),f5(f5(a9,a9),f5(a9,a9)))), % 116.68/117.40 inference(scs_inference,[],[19,2383,2,12])). % 116.68/117.40 cnf(2649,plain, % 116.68/117.40 (~E(f11(a10),f5(a6,x26491))), % 116.68/117.40 inference(scs_inference,[],[591,2,26])). % 116.68/117.40 cnf(2837,plain, % 116.68/117.40 (~P3(f5(x28371,a10),f5(f11(a6),f11(a6)))), % 116.68/117.40 inference(scs_inference,[],[19,1640,2,12])). % 116.68/117.40 cnf(2933,plain, % 116.68/117.40 (E(f5(x29331,x29332),f5(x29332,x29331))), % 116.68/117.40 inference(rename_variables,[],[19])). % 116.68/117.40 cnf(2936,plain, % 116.68/117.40 (~E(f5(x29361,a6),f5(a10,a10))), % 116.68/117.40 inference(scs_inference,[],[909,2218,19,2933,3,45,27])). % 116.68/117.40 cnf(2960,plain, % 116.68/117.40 (~E(f5(x29601,a6),a1)+E(f4(a10,a10,f5(x29601,a6)),a10)), % 116.68/117.40 inference(scs_inference,[],[2936,40,37,30,13])). % 116.68/117.40 cnf(3087,plain, % 116.68/117.40 (~E(f5(x30871,a6),f11(a10))), % 116.68/117.40 inference(scs_inference,[],[1004,19,28])). % 116.68/117.40 cnf(3441,plain, % 116.68/117.40 (~E(f5(x34411,a6),f11(a9))), % 116.68/117.40 inference(scs_inference,[],[1623,19,28])). % 116.68/117.40 cnf(3509,plain, % 116.68/117.40 (E(f11(a6),f5(x35091,a9))+E(f5(x35091,a9),a1)+E(f5(x35091,a9),f5(a6,a6))+~P2(f5(x35091,a9),f5(a6,a6))), % 116.68/117.40 inference(scs_inference,[],[1796,2,36])). % 116.68/117.40 cnf(3603,plain, % 116.68/117.40 (~P3(x36031,f5(a10,x36032))+~P3(f5(a10,x36032),f5(f11(a6),a1))), % 116.68/117.40 inference(scs_inference,[],[1639,25,45])). % 116.68/117.40 cnf(3619,plain, % 116.68/117.40 (~P3(f5(a10,x36191),f5(f11(a6),a1))+E(f5(a10,x36191),a1)), % 116.68/117.40 inference(scs_inference,[],[3603,24])). % 116.68/117.40 cnf(3635,plain, % 116.68/117.40 (~P3(f5(x36351,a10),f5(f11(a6),a1))+E(f5(a10,x36351),a1)), % 116.68/117.40 inference(scs_inference,[],[19,3619,12])). % 116.68/117.40 cnf(3651,plain, % 116.68/117.40 (~P3(f5(x36511,a10),f5(a1,f11(a6)))+E(f5(a10,x36511),a1)), % 116.68/117.40 inference(scs_inference,[],[19,3635,13])). % 116.68/117.41 cnf(3667,plain, % 116.68/117.41 (~E(f5(x36671,a10),a1)+E(f5(a10,x36671),a1)), % 116.68/117.41 inference(scs_inference,[],[19,3651,27])). % 116.68/117.41 cnf(3683,plain, % 116.68/117.41 (E(a1,f5(a10,x36831))+~E(f5(x36831,a10),a1)), % 116.68/117.41 inference(scs_inference,[],[3667,2])). % 116.68/117.41 cnf(3734,plain, % 116.68/117.41 (~E(x37341,a6)+~E(a10,x37341)), % 116.68/117.41 inference(scs_inference,[],[22,3])). % 116.68/117.41 cnf(3756,plain, % 116.68/117.41 (E(f5(a6,x37561),a1)+~P2(f5(a6,x37561),f5(a9,a9))), % 116.68/117.41 inference(scs_inference,[],[75,2649,2380,572,19,3,39,38,37,36])). % 116.68/117.41 cnf(3773,plain, % 116.68/117.41 (~E(x37731,a10)+~P2(f5(a6,a10),f5(a10,a10))), % 116.68/117.41 inference(scs_inference,[],[590,491,1639,19,40,3,36,3683,25,29,2,28])). % 116.68/117.41 cnf(3781,plain, % 116.68/117.41 (~P2(f5(a6,a10),f5(a10,a10))), % 116.68/117.41 inference(equality_inference,[],[3773])). % 116.68/117.41 cnf(3782,plain, % 116.68/117.41 (~E(x37821,a6)+~E(a9,x37821)), % 116.68/117.41 inference(scs_inference,[],[21,3])). % 116.68/117.41 cnf(3796,plain, % 116.68/117.41 (~E(x37961,a10)+~E(a6,x37961)), % 116.68/117.41 inference(scs_inference,[],[591,3])). % 116.68/117.41 cnf(3811,plain, % 116.68/117.41 (~E(x38111,a9)+~E(a6,x38111)), % 116.68/117.41 inference(scs_inference,[],[2381,3])). % 116.68/117.41 cnf(3825,plain, % 116.68/117.41 (E(f5(a10,x38251),a1)+E(f5(a10,x38251),f5(a6,a6))+~P2(f5(a10,x38251),f5(a6,a6))), % 116.68/117.41 inference(scs_inference,[],[74,1639,36])). % 116.68/117.41 cnf(3832,plain, % 116.68/117.41 (~P3(a10,f5(x38321,a6))+~E(x38321,a6)), % 116.68/117.41 inference(scs_inference,[],[19,22,3734,34])). % 116.68/117.41 cnf(3840,plain, % 116.68/117.41 (~E(f5(a9,a9),f5(x38401,a6))), % 116.68/117.41 inference(scs_inference,[],[2380,19,2,3])). % 116.68/117.41 cnf(3852,plain, % 116.68/117.41 (~E(f5(a10,a10),f5(a6,x38521))), % 116.68/117.41 inference(scs_inference,[],[590,2])). % 116.68/117.41 cnf(3863,plain, % 116.68/117.41 (~E(f5(x38631,a6),f5(a9,a9))), % 116.68/117.41 inference(scs_inference,[],[3840,2])). % 116.68/117.41 cnf(3866,plain, % 116.68/117.41 (~E(f4(a6,x38661,f5(a10,a10)),a6)+~P3(f4(a6,x38661,f5(a10,a10)),f5(a10,a10))), % 116.68/117.41 inference(scs_inference,[],[3840,3852,2,38,39])). % 116.68/117.41 cnf(3882,plain, % 116.68/117.41 (~E(f4(a6,x38821,f5(a10,a10)),x38821)+~P3(f4(a6,x38821,f5(a10,a10)),f5(a10,a10))), % 116.68/117.41 inference(scs_inference,[],[3852,38])). % 116.68/117.41 cnf(3929,plain, % 116.68/117.41 (~P3(a9,f5(x39291,a6))+~E(x39291,a6)), % 116.68/117.41 inference(scs_inference,[],[19,21,3782,34])). % 116.68/117.41 cnf(3946,plain, % 116.68/117.41 (~P3(a6,f5(x39461,a10))+~E(x39461,a10)), % 116.68/117.41 inference(scs_inference,[],[19,591,3796,34])). % 116.68/117.41 cnf(3963,plain, % 116.68/117.41 (~P3(a6,f5(x39631,a10))+~E(x39631,a9)), % 116.68/117.41 inference(scs_inference,[],[19,591,3811,34])). % 116.68/117.41 cnf(3964,plain, % 116.68/117.41 (~P3(a6,f5(a9,a10))), % 116.68/117.41 inference(equality_inference,[],[3963])). % 116.68/117.41 cnf(3965,plain, % 116.68/117.41 (~P3(a6,f5(a10,a9))), % 116.68/117.41 inference(scs_inference,[],[3964,19,13])). % 116.68/117.41 cnf(3972,plain, % 116.68/117.41 (E(f5(x39721,a6),a1)+~P2(f5(x39721,a6),f5(a9,a9))), % 116.68/117.41 inference(scs_inference,[],[3863,3441,36])). % 116.68/117.41 cnf(3977,plain, % 116.68/117.41 (P2(f5(x39771,a6),f5(x39772,x39773))+~P2(f5(x39771,a6),f5(a9,a9))), % 116.68/117.41 inference(scs_inference,[],[3863,3441,36,25,29])). % 116.68/117.41 cnf(4057,plain, % 116.68/117.41 (~P2(f5(x40571,a6),f5(a9,a9))+E(f5(a6,x40571),a1)), % 116.68/117.41 inference(scs_inference,[],[19,3756,14])). % 116.68/117.41 cnf(4109,plain, % 116.68/117.41 (~P2(f5(a6,x41091),f5(a9,a9))+E(f5(x41091,a6),a1)), % 116.68/117.41 inference(scs_inference,[],[19,3972,14])). % 116.68/117.41 cnf(4157,plain, % 116.68/117.41 (~E(f5(x41571,a6),a1)+E(f5(a6,x41571),a1)), % 116.68/117.41 inference(scs_inference,[],[4057,29])). % 116.68/117.41 cnf(4173,plain, % 116.68/117.41 (~E(f5(a10,a6),a1)), % 116.68/117.41 inference(scs_inference,[],[3781,4157,29])). % 116.68/117.41 cnf(4178,plain, % 116.68/117.41 (~E(f5(a6,a10),a1)), % 116.68/117.41 inference(scs_inference,[],[4173,3619,4109,3667])). % 116.68/117.41 cnf(4184,plain, % 116.68/117.41 (~P3(f5(a6,a10),f5(f11(a6),a1))), % 116.68/117.41 inference(scs_inference,[],[4173,3619,4109,3667,70,71,3635])). % 116.68/117.41 cnf(4188,plain, % 116.68/117.41 (~E(a1,f5(a10,a6))), % 116.68/117.41 inference(scs_inference,[],[4173,3619,4109,3667,70,71,3635,3651,2])). % 116.68/117.41 cnf(4190,plain, % 116.68/117.41 (E(f5(x41901,x41902),f5(x41902,x41901))), % 116.68/117.41 inference(rename_variables,[],[19])). % 116.68/117.41 cnf(4191,plain, % 116.68/117.41 (~E(a1,f5(a6,a10))), % 116.68/117.41 inference(scs_inference,[],[19,4190,4173,3619,4109,3667,70,71,3635,3651,2,13,3])). % 116.68/117.41 cnf(4227,plain, % 116.68/117.41 (E(f4(a10,a6,a1),a6)+E(f4(a10,a6,a1),a10)), % 116.68/117.41 inference(scs_inference,[],[4188,40,37])). % 116.68/117.41 cnf(4286,plain, % 116.68/117.41 (E(f4(a10,a6,a1),a6)+E(f5(x42861,f4(a10,a6,a1)),f5(x42861,a10))), % 116.68/117.41 inference(scs_inference,[],[4227,5])). % 116.68/117.41 cnf(5061,plain, % 116.68/117.41 (P3(f4(a10,a6,a1),f5(a6,x50611))+E(f5(x50612,f4(a10,a6,a1)),f5(x50612,a10))), % 116.68/117.41 inference(scs_inference,[],[19,4286,27])). % 116.68/117.41 cnf(5644,plain, % 116.68/117.41 (~E(f4(a6,x56441,f5(a10,a10)),a10)+~E(f4(a6,x56441,f5(a10,a10)),x56441)), % 116.68/117.41 inference(scs_inference,[],[19,3882,27])). % 116.68/117.41 cnf(5660,plain, % 116.68/117.41 (E(f4(a6,a10,f5(a10,a10)),a6)), % 116.68/117.41 inference(scs_inference,[],[5644,941])). % 116.68/117.41 cnf(5661,plain, % 116.68/117.41 (~P3(f4(a6,a10,f5(a10,a10)),f5(a10,a10))), % 116.68/117.41 inference(scs_inference,[],[5660,3866])). % 116.68/117.41 cnf(5665,plain, % 116.68/117.41 (~E(a9,f4(a6,a10,f5(a10,a10)))), % 116.68/117.41 inference(scs_inference,[],[21,18,5660,3866,14,3])). % 116.68/117.41 cnf(5670,plain, % 116.68/117.41 (~E(a10,f4(a6,a10,f5(a10,a10)))), % 116.68/117.41 inference(scs_inference,[],[22,5660,3])). % 116.68/117.41 cnf(5674,plain, % 116.68/117.41 (~E(x56741,f4(a6,a10,f5(a10,a10)))+~E(a9,x56741)), % 116.68/117.41 inference(scs_inference,[],[5665,3])). % 116.68/117.41 cnf(5684,plain, % 116.68/117.41 (~E(x56841,f4(a6,a10,f5(a10,a10)))+~E(a10,x56841)), % 116.68/117.41 inference(scs_inference,[],[5670,3])). % 116.68/117.41 cnf(5685,plain, % 116.68/117.41 (~E(x56851,a10)+~E(a10,f4(a6,x56851,f5(a10,a10)))), % 116.68/117.41 inference(scs_inference,[],[5670,3,7])). % 116.68/117.41 cnf(6066,plain, % 116.68/117.41 (~E(a1,a7)), % 116.68/117.41 inference(scs_inference,[],[16,23,4173,22,33,3825,11])). % 116.68/117.41 cnf(6069,plain, % 116.68/117.41 (~P3(a1,f5(a7,a7))), % 116.68/117.41 inference(scs_inference,[],[16,23,4173,22,33,3825,11,26,45])). % 116.68/117.41 cnf(6075,plain, % 116.68/117.41 (E(a1,f5(a6,a8))+E(f5(a6,a8),f5(a9,a10))), % 116.68/117.41 inference(scs_inference,[],[20,16,23,491,572,4173,22,33,3825,11,26,45,36,2])). % 116.68/117.41 cnf(6079,plain, % 116.68/117.41 (E(f5(a8,a6),a1)+E(f5(a6,a8),f5(a9,a10))), % 116.68/117.41 inference(scs_inference,[],[20,16,23,491,40,572,4173,19,22,33,3825,11,26,45,36,2,27,3])). % 116.68/117.41 cnf(6135,plain, % 116.68/117.41 (~P3(x61351,f5(a10,a9))+~E(x61351,a6)), % 116.68/117.41 inference(scs_inference,[],[3965,12])). % 116.68/117.41 cnf(6153,plain, % 116.68/117.41 (~P3(x61531,f5(a9,a10))+~E(x61531,a6)), % 116.68/117.41 inference(scs_inference,[],[3964,12])). % 116.68/117.41 cnf(6175,plain, % 116.68/117.41 (~P3(x61751,f5(a9,a9))+~E(x61751,a6)), % 116.68/117.41 inference(scs_inference,[],[2391,12])). % 116.68/117.41 cnf(6190,plain, % 116.68/117.41 (~P3(x61901,f5(a6,a6))+~E(x61901,a9)), % 116.68/117.41 inference(scs_inference,[],[47,12])). % 116.68/117.41 cnf(6200,plain, % 116.68/117.41 (E(a1,f5(a6,a8))), % 116.68/117.41 inference(scs_inference,[],[2381,591,6075,33])). % 116.68/117.41 cnf(6201,plain, % 116.68/117.41 (E(f5(a6,a8),a1)), % 116.68/117.41 inference(scs_inference,[],[6200,2])). % 116.68/117.41 cnf(6204,plain, % 116.68/117.41 (~P3(f5(a6,a8),f5(a7,a7))), % 116.68/117.41 inference(scs_inference,[],[18,6200,6069,2,15,12])). % 116.68/117.41 cnf(6206,plain, % 116.68/117.41 (E(f5(x62061,x62062),f5(x62062,x62061))), % 116.68/117.41 inference(rename_variables,[],[19])). % 116.68/117.41 cnf(6207,plain, % 116.68/117.41 (~P3(x62071,f5(a6,a8))), % 116.68/117.41 inference(scs_inference,[],[18,6200,6069,40,19,2,15,12,14,13])). % 116.68/117.41 cnf(6208,plain, % 116.68/117.41 (~E(a1,f5(x62081,a1))), % 116.68/117.41 inference(scs_inference,[],[18,6200,6069,40,19,2,15,12,14,13,27])). % 116.68/117.41 cnf(6209,plain, % 116.68/117.41 (~P3(x62091,a1)), % 116.68/117.41 inference(rename_variables,[],[40])). % 116.68/117.41 cnf(6211,plain, % 116.68/117.41 (E(a1,f5(a8,a6))), % 116.68/117.41 inference(scs_inference,[],[18,6200,6069,40,19,6206,2,15,12,14,13,27,3])). % 116.68/117.41 cnf(6213,plain, % 116.68/117.41 (~E(a1,f5(a1,x62131))), % 116.68/117.41 inference(scs_inference,[],[18,6200,6069,40,6209,19,6206,2,15,12,14,13,27,3,28])). % 116.68/117.41 cnf(6216,plain, % 116.68/117.41 (~E(f5(a1,a10),a1)), % 116.68/117.41 inference(scs_inference,[],[18,6200,6069,40,6209,19,6206,2,15,12,14,13,27,3,28,3683])). % 116.68/117.41 cnf(6218,plain, % 116.68/117.41 (~P3(f5(a1,a10),f5(a1,a1))), % 116.68/117.41 inference(scs_inference,[],[18,6200,6069,40,6209,19,6206,2,15,12,14,13,27,3,28,3683,45])). % 116.68/117.41 cnf(6223,plain, % 116.68/117.41 (E(f5(x62231,f4(a10,a6,a1)),f5(x62231,a10))), % 116.68/117.41 inference(scs_inference,[],[6207,5061])). % 116.68/117.41 cnf(6224,plain, % 116.68/117.41 (E(f5(a8,a6),a1)), % 116.68/117.41 inference(scs_inference,[],[591,2381,6079,33])). % 116.68/117.41 cnf(6229,plain, % 116.68/117.41 (~E(f5(a7,a7),f5(x62291,a1))), % 116.68/117.41 inference(scs_inference,[],[6204,6201,6218,42,19,15,12,27])). % 116.68/117.41 cnf(6239,plain, % 116.68/117.41 (~P3(x62391,f5(a6,a8))), % 116.68/117.41 inference(rename_variables,[],[6207])). % 116.68/117.41 cnf(6241,plain, % 116.68/117.41 (~E(f5(a6,a8),f5(a1,x62411))), % 116.68/117.41 inference(scs_inference,[],[6207,6239,6224,27,28])). % 116.68/117.41 cnf(6244,plain, % 116.68/117.41 (~P3(x62441,f5(a6,a6))+~E(x62441,a10)), % 116.68/117.41 inference(scs_inference,[],[6207,6239,6224,54,27,28,12])). % 116.68/117.41 cnf(6252,plain, % 116.68/117.41 (E(f4(a1,x62521,a1),a1)+E(f4(a1,x62521,a1),x62521)), % 116.68/117.41 inference(scs_inference,[],[6213,40,37])). % 116.68/117.41 cnf(6256,plain, % 116.68/117.41 (~P3(x62561,f5(a8,a6))), % 116.68/117.41 inference(scs_inference,[],[6224,40,13])). % 116.68/117.41 cnf(6261,plain, % 116.68/117.41 (~P3(x62611,f5(a8,a6))), % 116.68/117.41 inference(rename_variables,[],[6256])). % 116.68/117.41 cnf(6263,plain, % 116.68/117.41 (~E(f5(a8,a6),f5(a1,x62631))), % 116.68/117.41 inference(scs_inference,[],[6256,6261,6201,603,12,27,28])). % 116.68/117.41 cnf(6291,plain, % 116.68/117.41 (~P3(x62911,f4(a1,a1,a1))), % 116.68/117.41 inference(scs_inference,[],[6252,25])). % 116.68/117.41 cnf(6406,plain, % 116.68/117.41 (~E(f5(a8,a6),f5(x64061,f5(a8,a6)))), % 116.68/117.41 inference(scs_inference,[],[6224,6211,25,27])). % 116.68/117.41 cnf(6414,plain, % 116.68/117.41 (~E(f5(a8,a6),f5(f5(a8,a6),x64141))), % 116.68/117.41 inference(scs_inference,[],[6224,6211,25,28])). % 116.68/117.41 cnf(6416,plain, % 116.68/117.41 (~E(f5(a6,a8),f5(x64161,f5(x64162,x64163)))), % 116.68/117.41 inference(scs_inference,[],[6201,19,25,27])). % 116.68/117.41 cnf(6435,plain, % 116.68/117.41 (~P3(x64351,f5(a6,x64352))+~P3(f5(a6,x64352),f5(a1,f11(a9)))), % 116.68/117.41 inference(scs_inference,[],[572,19,25,34])). % 116.68/117.41 cnf(6445,plain, % 116.68/117.41 (~P3(x64451,a6)+~P3(a6,f5(a1,a9))), % 116.68/117.41 inference(scs_inference,[],[2381,19,25,34])). % 116.68/117.41 cnf(6446,plain, % 116.68/117.41 (E(a6,a1)+~P3(a6,f5(a1,a9))), % 116.68/117.41 inference(scs_inference,[],[6445,24])). % 116.68/117.41 cnf(6447,plain, % 116.68/117.41 (~P3(a6,f5(a9,a1))+E(a6,a1)), % 116.68/117.41 inference(scs_inference,[],[19,6446,13])). % 116.68/117.41 cnf(6448,plain, % 116.68/117.41 (~P3(a6,f5(a9,a1))), % 116.68/117.41 inference(scs_inference,[],[6241,6447,4])). % 116.68/117.41 cnf(6450,plain, % 116.68/117.41 (E(f5(x64501,x64502),f5(x64502,x64501))), % 116.68/117.41 inference(rename_variables,[],[19])). % 116.68/117.41 cnf(6452,plain, % 116.68/117.41 (~P3(a6,f5(a1,a1))), % 116.68/117.41 inference(scs_inference,[],[6448,19,6450,28,34])). % 116.68/117.41 cnf(6455,plain, % 116.68/117.41 (P3(f3(a6),a6)), % 116.68/117.41 inference(scs_inference,[],[6448,19,6450,28,34,24])). % 116.68/117.41 cnf(6457,plain, % 116.68/117.41 (~E(f11(a6),f5(a1,x64571))), % 116.68/117.41 inference(scs_inference,[],[6448,19,6450,28,34,24,26])). % 116.68/117.41 cnf(6459,plain, % 116.68/117.41 (~P3(a6,f3(a6))), % 116.68/117.41 inference(scs_inference,[],[6448,19,6450,28,34,24,26,30])). % 116.68/117.41 cnf(6462,plain, % 116.68/117.41 (~E(f5(a6,x64621),f5(a1,a1))), % 116.68/117.41 inference(scs_inference,[],[6448,19,6450,28,34,24,26,30,12,33])). % 116.68/117.41 cnf(6464,plain, % 116.68/117.41 (~P3(a6,f5(a1,a9))), % 116.68/117.41 inference(scs_inference,[],[6448,19,6450,28,34,24,26,30,12,33,6445])). % 116.68/117.41 cnf(6499,plain, % 116.68/117.41 (~P2(f5(a1,a9),f5(a6,a6))+E(f5(a1,a9),f5(a6,a6))+E(f5(a1,a9),a1)), % 116.68/117.41 inference(scs_inference,[],[6457,3509])). % 116.68/117.41 cnf(6501,plain, % 116.68/117.41 (~E(a6,f5(a8,a6))), % 116.68/117.41 inference(scs_inference,[],[6452,6455,6256,12,13])). % 116.68/117.41 cnf(6526,plain, % 116.68/117.41 (E(f5(a6,a10),f11(a1))+~P2(f5(a6,a10),f5(a1,a1))), % 116.68/117.41 inference(scs_inference,[],[6462,4178,36])). % 116.68/117.41 cnf(6532,plain, % 116.68/117.41 (~E(a6,f4(a1,a1,a1))), % 116.68/117.41 inference(scs_inference,[],[6464,6455,6291,12,13])). % 116.68/117.41 cnf(6552,plain, % 116.68/117.41 (~P3(x65521,f3(a6))+~E(x65521,a6)), % 116.68/117.41 inference(scs_inference,[],[6459,12])). % 116.68/117.41 cnf(6553,plain, % 116.68/117.41 (~E(a6,f5(a6,a8))), % 116.68/117.41 inference(scs_inference,[],[6459,6455,6207,12,13])). % 116.68/117.41 cnf(6683,plain, % 116.68/117.41 (~P2(f5(a6,a10),f5(a1,a1))+E(f11(a1),f5(a6,a10))), % 116.68/117.41 inference(scs_inference,[],[6526,2])). % 116.68/117.41 cnf(6712,plain, % 116.68/117.41 (~E(f5(a6,a1),a1)), % 116.68/117.41 inference(scs_inference,[],[6208,1784,29])). % 116.68/117.41 cnf(6899,plain, % 116.68/117.41 (E(f4(a9,a9,f5(a8,a6)),a9)), % 116.68/117.41 inference(scs_inference,[],[6224,3863,25,37])). % 116.68/117.41 cnf(6903,plain, % 116.68/117.41 (~E(a1,a6)), % 116.68/117.41 inference(scs_inference,[],[6455,25,2])). % 116.68/117.41 cnf(6904,plain, % 116.68/117.41 (~E(f11(a1),f5(a6,x69041))), % 116.68/117.41 inference(scs_inference,[],[6903,26])). % 116.68/117.41 cnf(6908,plain, % 116.68/117.41 (~E(f5(a1,x69081),f5(a6,a6))), % 116.68/117.41 inference(scs_inference,[],[6903,26,45,33])). % 116.68/117.41 cnf(6923,plain, % 116.68/117.41 (~P2(f5(a1,a9),f5(a6,a6))+E(f5(a1,a9),a1)), % 116.68/117.41 inference(scs_inference,[],[6908,6499])). % 116.68/117.41 cnf(6924,plain, % 116.68/117.41 (~P2(f5(a6,a10),f5(a1,a1))), % 116.68/117.41 inference(scs_inference,[],[6904,6683])). % 116.68/117.41 cnf(6926,plain, % 116.68/117.41 (~P2(f5(a1,a9),f5(a6,a6))), % 116.68/117.41 inference(scs_inference,[],[6213,6923,2])). % 116.68/117.41 cnf(6929,plain, % 116.68/117.41 (~E(f5(a1,a9),a1)), % 116.68/117.41 inference(scs_inference,[],[6924,6926,31,29])). % 116.68/117.41 cnf(7107,plain, % 116.68/117.41 (~P3(a6,f4(a6,a8,a6))+E(f4(a6,a8,a6),a6)+E(f4(a6,a8,a6),a8)), % 116.68/117.41 inference(scs_inference,[],[6553,30,37])). % 116.68/117.41 cnf(7108,plain, % 116.68/117.41 (E(f4(a6,a8,a6),a6)+~P3(a6,f4(a6,a8,a6))), % 116.68/117.41 inference(scs_inference,[],[6207,19,7107,28])). % 116.68/117.41 cnf(7110,plain, % 116.68/117.41 (~P3(a6,f4(a6,a8,a6))), % 116.68/117.41 inference(scs_inference,[],[6256,19,7108,28])). % 116.68/117.41 cnf(7111,plain, % 116.68/117.41 (~E(a6,x71111)+~E(f4(a6,a8,a6),f5(x71112,x71111))), % 116.68/117.41 inference(scs_inference,[],[7110,27])). % 116.68/117.41 cnf(7116,plain, % 116.68/117.41 (~E(a6,x71161)+~E(f4(a6,a8,a6),f5(x71161,x71162))), % 116.68/117.41 inference(scs_inference,[],[7110,28])). % 116.68/117.41 cnf(7118,plain, % 116.68/117.41 (~P3(x71181,f4(a6,a8,a6))+~E(x71181,a6)), % 116.68/117.41 inference(scs_inference,[],[7110,28,12])). % 116.68/117.41 cnf(7124,plain, % 116.68/117.41 (~P3(f4(a6,a8,a6),f5(f5(x71241,x71242),f5(x71241,x71242)))+~E(a6,x71242)), % 116.68/117.41 inference(scs_inference,[],[19,7111,34])). % 116.68/117.41 cnf(7125,plain, % 116.68/117.41 (~P3(f4(a6,a8,a6),f5(f5(x71251,a6),f5(x71251,a6)))), % 116.68/117.41 inference(equality_inference,[],[7124])). % 116.68/117.41 cnf(7127,plain, % 116.68/117.41 (~P3(f4(a6,a8,a6),f5(f5(x71271,x71272),f5(x71271,x71272)))+~E(a6,x71271)), % 116.68/117.41 inference(scs_inference,[],[19,7116,34])). % 116.68/117.41 cnf(7128,plain, % 116.68/117.41 (~P3(f4(a6,a8,a6),f5(f5(a6,x71281),f5(a6,x71281)))), % 116.68/117.41 inference(equality_inference,[],[7127])). % 116.68/117.41 cnf(7349,plain, % 116.68/117.41 (~P3(a6,f5(f4(a1,a1,a1),x73491))+~E(x73491,a10)), % 116.68/117.41 inference(scs_inference,[],[6532,19,3796,34])). % 116.68/117.41 cnf(7501,plain, % 116.68/117.41 (~P3(a6,f5(f4(a1,a1,a1),x75011))+~E(x75011,a9)), % 116.68/117.41 inference(scs_inference,[],[6532,19,3811,34])). % 116.68/117.41 cnf(7506,plain, % 116.68/117.41 (~P3(a10,f5(f4(a6,a10,f5(a10,a10)),a6))), % 116.68/117.41 inference(scs_inference,[],[69,6899,5660,3811,9,10,3832])). % 116.68/117.41 cnf(7516,plain, % 116.68/117.41 (E(a9,f4(a9,a9,f5(a6,a8)))), % 116.68/117.41 inference(scs_inference,[],[69,6899,5660,6201,3811,9,10,3832,3929,3963,7118,8,705,2444])). % 116.68/117.41 cnf(7518,plain, % 116.68/117.41 (E(f4(a10,a10,f5(a8,a6)),a10)), % 116.68/117.41 inference(scs_inference,[],[69,6899,5660,6224,6201,3811,9,10,3832,3929,3963,7118,8,705,2444,2960])). % 116.68/117.41 cnf(7520,plain, % 116.68/117.41 (E(f4(a10,a10,f5(a6,a8)),a10)), % 116.68/117.41 inference(scs_inference,[],[69,6899,5660,6207,6224,6201,3811,9,10,3832,3929,3963,7118,8,705,2444,2960,605])). % 116.68/117.41 cnf(7521,plain, % 116.68/117.41 (~P3(x75211,f5(a6,a8))), % 116.68/117.41 inference(rename_variables,[],[6207])). % 116.68/117.41 cnf(7524,plain, % 116.68/117.41 (~P3(x75241,f5(a6,a8))), % 116.68/117.41 inference(rename_variables,[],[6207])). % 116.68/117.41 cnf(7526,plain, % 116.68/117.41 (E(f4(a9,a9,f5(a6,a8)),a9)), % 116.68/117.41 inference(scs_inference,[],[69,6899,5660,6207,7521,7524,6224,6201,3811,9,10,3832,3929,3963,7118,8,705,2444,2960,605,609,2393])). % 116.68/117.41 cnf(7527,plain, % 116.68/117.41 (~P3(x75271,f5(a6,a8))), % 116.68/117.41 inference(rename_variables,[],[6207])). % 116.68/117.41 cnf(7536,plain, % 116.68/117.41 (P3(f3(f5(a6,a1)),f5(a6,a1))), % 116.68/117.41 inference(scs_inference,[],[69,6899,459,6712,5660,6207,7521,7524,7527,6224,6201,3811,9,10,3832,3929,3963,7118,8,705,2444,2960,605,609,2393,2396,35,60,5,24])). % 116.68/117.41 cnf(7541,plain, % 116.68/117.41 (E(f4(x75411,f5(x75412,f4(a10,a6,a1)),x75413),f4(x75411,f5(x75412,a10),x75413))), % 116.68/117.41 inference(scs_inference,[],[69,6223,6406,6899,459,6712,5660,6207,7521,7524,7527,6224,6201,3811,9,10,3832,3929,3963,7118,8,705,2444,2960,605,609,2393,2396,35,60,5,24,26,6,7])). % 116.68/117.41 cnf(7543,plain, % 116.68/117.41 (E(f5(x75431,a10),f5(x75431,f4(a10,a6,a1)))), % 116.68/117.41 inference(scs_inference,[],[69,6223,6406,6899,459,6712,5660,6207,7521,7524,7527,6224,6201,3811,9,10,3832,3929,3963,7118,8,705,2444,2960,605,609,2393,2396,35,60,5,24,26,6,7,4,2])). % 116.68/117.41 cnf(7547,plain, % 116.68/117.41 (P2(f4(a9,a9,f5(a8,a6)),a9)), % 116.68/117.41 inference(scs_inference,[],[69,5661,6223,6406,6899,443,459,6712,5660,6207,7521,7524,7527,18,6224,6201,3811,9,10,3832,3929,3963,7118,8,705,2444,2960,605,609,2393,2396,35,60,5,24,26,6,7,4,2,28,15])). % 116.68/117.41 cnf(7552,plain, % 116.68/117.41 (E(f5(x75521,f4(a10,a6,a1)),f5(x75521,a10))), % 116.68/117.41 inference(rename_variables,[],[6223])). % 116.68/117.41 cnf(7554,plain, % 116.68/117.41 (E(f5(f5(x75541,x75542),x75543),f5(f5(x75542,x75541),x75543))), % 116.68/117.41 inference(rename_variables,[],[69])). % 116.68/117.41 cnf(7558,plain, % 116.68/117.41 (E(f5(x75581,f4(a10,a6,a1)),f5(x75581,a10))), % 116.68/117.41 inference(rename_variables,[],[6223])). % 116.68/117.41 cnf(7561,plain, % 116.68/117.41 (E(f5(f5(x75611,x75612),f4(a10,a6,a1)),f5(f5(x75612,x75611),a10))), % 116.68/117.41 inference(scs_inference,[],[69,7554,5661,6223,7552,7558,6406,6899,7125,443,459,4184,492,6712,5660,6207,7521,7524,7527,18,6224,6201,3811,9,10,3832,3929,3963,7118,8,705,2444,2960,605,609,2393,2396,35,60,5,24,26,6,7,4,2,28,15,45,12,13,33,27,3])). % 116.68/117.41 cnf(7563,plain, % 116.68/117.41 (E(f5(f5(x75631,x75632),x75633),f5(f5(x75632,x75631),x75633))), % 116.68/117.41 inference(rename_variables,[],[69])). % 116.68/117.41 cnf(7572,plain, % 116.68/117.41 (~P3(f4(a6,a10,f5(a10,a10)),f5(a10,a9))), % 116.68/117.42 inference(scs_inference,[],[69,7554,7563,5661,6223,7552,7558,6406,6899,7125,443,459,4184,492,6712,5660,6207,7521,7524,7527,18,6224,6201,3811,9,10,3832,3929,3963,7118,8,705,2444,2960,605,609,2393,2396,35,60,5,24,26,6,7,4,2,28,15,45,12,13,33,27,3,34,3796,6552,3946,6135])). % 116.68/117.42 cnf(7573,plain, % 116.68/117.42 (~P3(f4(a6,a10,f5(a10,a10)),f5(a9,a10))), % 116.68/117.42 inference(scs_inference,[],[69,7554,7563,5661,6223,7552,7558,6406,6899,7125,443,459,4184,492,6712,5660,6207,7521,7524,7527,18,6224,6201,3811,9,10,3832,3929,3963,7118,8,705,2444,2960,605,609,2393,2396,35,60,5,24,26,6,7,4,2,28,15,45,12,13,33,27,3,34,3796,6552,3946,6135,6153])). % 116.68/117.42 cnf(7576,plain, % 116.68/117.42 (~P3(f4(a10,a10,f5(a8,a6)),f5(a6,a6))), % 116.68/117.42 inference(scs_inference,[],[69,7554,7563,5661,6223,7552,7558,6406,6899,7125,443,459,4184,492,6712,5660,6207,7521,7524,7527,18,6224,6201,3811,9,10,3832,3929,3963,7118,8,705,2444,2960,605,609,2393,2396,35,60,5,24,26,6,7,4,2,28,15,45,12,13,33,27,3,34,3796,6552,3946,6135,6153,6175,6190,6244])). % 116.68/117.42 cnf(7611,plain, % 116.68/117.42 (P2(f5(x76111,a10),f5(x76111,f4(a10,a6,a1)))), % 116.68/117.42 inference(scs_inference,[],[7520,7543,3946,35])). % 116.68/117.42 cnf(7613,plain, % 116.68/117.42 (E(f11(f4(a10,a10,f5(a8,a6))),f11(a10))), % 116.68/117.42 inference(scs_inference,[],[7518,7520,7543,3946,35,9])). % 116.68/117.42 cnf(7619,plain, % 116.68/117.42 (E(f4(x76191,x76192,f4(a10,a10,f5(a8,a6))),f4(x76191,x76192,a10))), % 116.68/117.42 inference(scs_inference,[],[7518,7520,7526,7543,72,3946,35,9,60,10,5,3963,8])). % 116.68/117.42 cnf(7620,plain, % 116.68/117.42 (P3(f3(f5(a6,a10)),f5(a6,a10))), % 116.68/117.42 inference(scs_inference,[],[7518,7520,7526,7543,72,4178,3946,35,9,60,10,5,3963,8,24])). % 116.68/117.42 cnf(7627,plain, % 116.68/117.42 (E(a10,f4(a10,a10,f5(a8,a6)))), % 116.68/117.42 inference(scs_inference,[],[6414,7518,7520,7526,7543,72,4178,3946,35,9,60,10,5,3963,8,24,26,6,7,4,2])). % 116.68/117.42 cnf(7629,plain, % 116.68/117.42 (E(f5(f5(x76291,x76292),x76293),f5(f5(x76292,x76291),x76293))), % 116.68/117.42 inference(rename_variables,[],[69])). % 116.68/117.42 cnf(7633,plain, % 116.68/117.42 (E(f4(x76331,x76332,f5(x76333,x76334)),f4(x76331,x76332,f5(x76334,x76333)))), % 116.68/117.42 inference(rename_variables,[],[443])). % 116.68/117.42 cnf(7640,plain, % 116.68/117.42 (E(f4(x76401,x76402,f5(x76403,x76404)),f4(x76401,x76402,f5(x76404,x76403)))), % 116.68/117.42 inference(rename_variables,[],[443])). % 116.68/117.42 cnf(7648,plain, % 116.68/117.42 (E(f5(f5(x76481,x76482),x76483),f5(f5(x76482,x76481),x76483))), % 116.68/117.42 inference(rename_variables,[],[69])). % 116.68/117.42 cnf(7654,plain, % 116.68/117.42 (~E(f5(a1,a6),a1)), % 116.68/117.42 inference(scs_inference,[],[69,7629,7648,7536,7572,7576,6414,7518,7516,7520,7526,7543,7547,72,2633,443,7633,7640,4178,19,3946,35,9,60,10,5,3963,8,24,26,6,7,4,2,28,14,15,45,33,12,13,27,3,34,5674,25])). % 116.68/117.42 cnf(7685,plain, % 116.68/117.42 (E(f5(f5(x76851,x76852),x76853),f5(f5(x76852,x76851),x76853))), % 116.68/117.42 inference(rename_variables,[],[69])). % 116.68/117.42 cnf(7700,plain, % 116.68/117.42 (~P2(f5(a1,a6),f5(a10,a10))), % 116.68/117.42 inference(scs_inference,[],[69,7685,7654,7573,6416,7128,7611,7627,395,427,7561,7619,7613,7506,7541,2837,443,2936,3087,35,9,24,10,60,5,8,26,6,7,30,4,2,28,15,45,33,13,12,27,3,36])). % 116.68/117.42 cnf(7753,plain, % 116.68/117.42 ($false), % 116.68/117.42 inference(scs_inference,[],[19,6501,4173,5660,6201,6263,6207,6229,6291,6200,7627,6211,6929,6216,6066,4191,6213,16,7613,7516,7520,7526,7700,7620,2,4,29,5,71,31,32,24,509,5685,5684,70,6190,6435,7501,525,3977,67,7349,541,130,3782,3734,61,3,11,27]), % 116.68/117.42 ['proof']). % 116.68/117.42 % SZS output end Proof % 116.68/117.42 % Total time :116.070000s %------------------------------------------------------------------------------