%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SEU172+1 : TPTP v8.2.0. Released v3.3.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/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 15:01:32 EDT 2024 % Result : Theorem 0.74s 0.80s % Output : CNFRefutation 0.74s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SEU172+1 : TPTP v8.2.0. Released v3.3.0. % 0.00/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n022.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 : Fri Jun 21 16:01:09 EDT 2024 % 0.12/0.33 % CPUTime : % 0.19/0.55 start to proof:theBenchmark % 0.69/0.80 %------------------------------------------- % 0.69/0.80 % File :CSE---1.7 % 0.69/0.80 % Problem :theBenchmark % 0.69/0.80 % Transform :cnf % 0.69/0.80 % Format :tptp:raw % 0.69/0.80 % Command :java -jar mcs_scs.jar %d %s % 0.69/0.80 % 0.69/0.80 % Result :Theorem 0.200000s % 0.69/0.80 % Output :CNFRefutation 0.200000s % 0.69/0.80 %------------------------------------------- % 0.74/0.80 %------------------------------------------------------------------------------ % 0.74/0.80 % File : SEU172+1 : TPTP v8.2.0. Released v3.3.0. % 0.74/0.80 % Domain : Set theory % 0.74/0.80 % Problem : MPTP bushy problem t54_subset_1 % 0.74/0.80 % Version : [Urb07] axioms : Especial. % 0.74/0.80 % English : % 0.74/0.80 % 0.74/0.80 % Refs : [Ban01] Bancerek et al. (2001), On the Characterizations of Co % 0.74/0.80 % : [Urb07] Urban (2006), Email to G. Sutcliffe % 0.74/0.80 % Source : [Urb07] % 0.74/0.80 % Names : bushy-t54_subset_1 [Urb07] % 0.74/0.80 % 0.74/0.80 % Status : Theorem % 0.74/0.80 % Rating : 0.08 v8.1.0, 0.11 v7.5.0, 0.12 v7.4.0, 0.03 v7.1.0, 0.04 v7.0.0, 0.00 v6.4.0, 0.04 v6.3.0, 0.12 v6.2.0, 0.20 v6.1.0, 0.23 v6.0.0, 0.22 v5.5.0, 0.19 v5.4.0, 0.21 v5.3.0, 0.22 v5.2.0, 0.00 v5.0.0, 0.12 v4.1.0, 0.13 v4.0.1, 0.17 v4.0.0, 0.21 v3.7.0, 0.15 v3.5.0, 0.16 v3.3.0 % 0.74/0.80 % Syntax : Number of formulae : 22 ( 11 unt; 0 def) % 0.74/0.80 % Number of atoms : 38 ( 7 equ) % 0.74/0.80 % Maximal formula atoms : 4 ( 1 avg) % 0.74/0.80 % Number of connectives : 26 ( 10 ~; 0 |; 7 &) % 0.74/0.80 % ( 2 <=>; 7 =>; 0 <=; 0 <~>) % 0.74/0.80 % Maximal formula depth : 9 ( 4 avg) % 0.74/0.80 % Maximal term depth : 3 ( 1 avg) % 0.74/0.80 % Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty) % 0.74/0.80 % Number of functors : 4 ( 4 usr; 1 con; 0-2 aty) % 0.74/0.80 % Number of variables : 31 ( 26 !; 5 ?) % 0.74/0.80 % SPC : FOF_THM_RFO_SEQ % 0.74/0.80 % 0.74/0.80 % Comments : Translated by MPTP 0.2 from the original problem in the Mizar % 0.74/0.80 % library, www.mizar.org % 0.74/0.80 %------------------------------------------------------------------------------ % 0.74/0.80 fof(dt_k1_xboole_0,axiom, % 0.74/0.80 $true ). % 0.74/0.80 % 0.74/0.80 fof(fc1_xboole_0,axiom, % 0.74/0.80 empty(empty_set) ). % 0.74/0.80 % 0.74/0.80 fof(t3_boole,axiom, % 0.74/0.80 ! [A] : set_difference(A,empty_set) = A ). % 0.74/0.80 % 0.74/0.80 fof(t4_boole,axiom, % 0.74/0.80 ! [A] : set_difference(empty_set,A) = empty_set ). % 0.74/0.80 % 0.74/0.80 fof(rc1_subset_1,axiom, % 0.74/0.80 ! [A] : % 0.74/0.80 ( ~ empty(A) % 0.74/0.80 => ? [B] : % 0.74/0.80 ( element(B,powerset(A)) % 0.74/0.80 & ~ empty(B) ) ) ). % 0.74/0.80 % 0.74/0.80 fof(rc2_subset_1,axiom, % 0.74/0.80 ! [A] : % 0.74/0.80 ? [B] : % 0.74/0.80 ( element(B,powerset(A)) % 0.74/0.80 & empty(B) ) ). % 0.74/0.80 % 0.74/0.80 fof(rc1_xboole_0,axiom, % 0.74/0.80 ? [A] : empty(A) ). % 0.74/0.80 % 0.74/0.80 fof(rc2_xboole_0,axiom, % 0.74/0.80 ? [A] : ~ empty(A) ). % 0.74/0.80 % 0.74/0.80 fof(t6_boole,axiom, % 0.74/0.80 ! [A] : % 0.74/0.80 ( empty(A) % 0.74/0.80 => A = empty_set ) ). % 0.74/0.80 % 0.74/0.80 fof(t8_boole,axiom, % 0.74/0.80 ! [A,B] : % 0.74/0.80 ~ ( empty(A) % 0.74/0.80 & A != B % 0.74/0.80 & empty(B) ) ). % 0.74/0.80 % 0.74/0.80 fof(involutiveness_k3_subset_1,axiom, % 0.74/0.80 ! [A,B] : % 0.74/0.80 ( element(B,powerset(A)) % 0.74/0.80 => subset_complement(A,subset_complement(A,B)) = B ) ). % 0.74/0.80 % 0.74/0.80 fof(antisymmetry_r2_hidden,axiom, % 0.74/0.80 ! [A,B] : % 0.74/0.80 ( in(A,B) % 0.74/0.80 => ~ in(B,A) ) ). % 0.74/0.80 % 0.74/0.80 fof(existence_m1_subset_1,axiom, % 0.74/0.80 ! [A] : % 0.74/0.80 ? [B] : element(B,A) ). % 0.74/0.80 % 0.74/0.80 fof(dt_k1_zfmisc_1,axiom, % 0.74/0.80 $true ). % 0.74/0.80 % 0.74/0.80 fof(dt_k3_subset_1,axiom, % 0.74/0.80 ! [A,B] : % 0.74/0.80 ( element(B,powerset(A)) % 0.74/0.80 => element(subset_complement(A,B),powerset(A)) ) ). % 0.74/0.80 % 0.74/0.80 fof(dt_k4_xboole_0,axiom, % 0.74/0.80 $true ). % 0.74/0.80 % 0.74/0.80 fof(dt_m1_subset_1,axiom, % 0.74/0.80 $true ). % 0.74/0.80 % 0.74/0.80 fof(fc1_subset_1,axiom, % 0.74/0.80 ! [A] : ~ empty(powerset(A)) ). % 0.74/0.80 % 0.74/0.80 fof(t7_boole,axiom, % 0.74/0.80 ! [A,B] : % 0.74/0.80 ~ ( in(A,B) % 0.74/0.80 & empty(B) ) ). % 0.74/0.80 % 0.74/0.80 fof(d5_subset_1,axiom, % 0.74/0.80 ! [A,B] : % 0.74/0.80 ( element(B,powerset(A)) % 0.74/0.80 => subset_complement(A,B) = set_difference(A,B) ) ). % 0.74/0.80 % 0.74/0.80 fof(t54_subset_1,conjecture, % 0.74/0.80 ! [A,B,C] : % 0.74/0.80 ( element(C,powerset(A)) % 0.74/0.80 => ~ ( in(B,subset_complement(A,C)) % 0.74/0.80 & in(B,C) ) ) ). % 0.74/0.80 % 0.74/0.80 fof(d4_xboole_0,axiom, % 0.74/0.80 ! [A,B,C] : % 0.74/0.80 ( C = set_difference(A,B) % 0.74/0.80 <=> ! [D] : % 0.74/0.80 ( in(D,C) % 0.74/0.80 <=> ( in(D,A) % 0.74/0.80 & ~ in(D,B) ) ) ) ). % 0.74/0.80 % 0.74/0.80 %------------------------------------------------------------------------------ % 0.74/0.80 %------------------------------------------- % 0.74/0.80 % Proof found % 0.74/0.80 % SZS status Theorem for theBenchmark % 0.74/0.81 % SZS output start Proof % 0.74/0.81 %ClaNum:46(EqnAxiom:19) % 0.74/0.81 %VarNum:104(SingletonVarNum:42) % 0.74/0.81 %MaxLitNum:4 % 0.74/0.81 %MaxfuncDepth:2 % 0.74/0.81 %SharedTerms:14 % 0.74/0.81 %goalClause: 23 26 29 % 0.74/0.81 %singleGoalClaCount:3 % 0.74/0.81 [20]P1(a1) % 0.74/0.81 [21]P1(a2) % 0.74/0.81 [23]P3(a5,a9) % 0.74/0.81 [30]~P1(a8) % 0.74/0.81 [26]P2(a9,f11(a6)) % 0.74/0.81 [29]P3(a5,f13(a6,a9)) % 0.74/0.81 [22]P1(f3(x221)) % 0.74/0.81 [24]E(f10(a1,x241),a1) % 0.74/0.81 [25]E(f10(x251,a1),x251) % 0.74/0.81 [27]P2(f7(x271),x271) % 0.74/0.81 [28]P2(f3(x281),f11(x281)) % 0.74/0.81 [31]~P1(f11(x311)) % 0.74/0.81 [32]~P1(x321)+E(x321,a1) % 0.74/0.81 [34]P1(x341)+~P1(f4(x341)) % 0.74/0.81 [36]P1(x361)+P2(f4(x361),f11(x361)) % 0.74/0.81 [35]~P1(x351)+~P3(x352,x351) % 0.74/0.81 [37]~P3(x372,x371)+~P3(x371,x372) % 0.74/0.81 [38]~P2(x382,f11(x381))+E(f13(x381,x382),f10(x381,x382)) % 0.74/0.81 [43]~P2(x432,f11(x431))+P2(f13(x431,x432),f11(x431)) % 0.74/0.81 [41]~P2(x412,f11(x411))+E(f13(x411,f13(x411,x412)),x412) % 0.74/0.81 [33]~P1(x332)+~P1(x331)+E(x331,x332) % 0.74/0.81 [44]P3(f12(x442,x443,x441),x441)+P3(f12(x442,x443,x441),x442)+E(x441,f10(x442,x443)) % 0.74/0.81 [45]P3(f12(x452,x453,x451),x451)+~P3(f12(x452,x453,x451),x453)+E(x451,f10(x452,x453)) % 0.74/0.81 [39]~P3(x391,x393)+P3(x391,x392)+~E(x393,f10(x392,x394)) % 0.74/0.81 [40]~P3(x404,x403)+~P3(x404,x401)+~E(x401,f10(x402,x403)) % 0.74/0.81 [46]P3(f12(x462,x463,x461),x463)+~P3(f12(x462,x463,x461),x461)+~P3(f12(x462,x463,x461),x462)+E(x461,f10(x462,x463)) % 0.74/0.81 [42]~P3(x421,x424)+P3(x421,x422)+P3(x421,x423)+~E(x422,f10(x424,x423)) % 0.74/0.81 %EqnAxiom % 0.74/0.81 [1]E(x11,x11) % 0.74/0.81 [2]E(x22,x21)+~E(x21,x22) % 0.74/0.81 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 0.74/0.81 [4]~E(x41,x42)+E(f3(x41),f3(x42)) % 0.74/0.81 [5]~E(x51,x52)+E(f10(x51,x53),f10(x52,x53)) % 0.74/0.81 [6]~E(x61,x62)+E(f10(x63,x61),f10(x63,x62)) % 0.74/0.81 [7]~E(x71,x72)+E(f12(x71,x73,x74),f12(x72,x73,x74)) % 0.74/0.81 [8]~E(x81,x82)+E(f12(x83,x81,x84),f12(x83,x82,x84)) % 0.74/0.81 [9]~E(x91,x92)+E(f12(x93,x94,x91),f12(x93,x94,x92)) % 0.74/0.81 [10]~E(x101,x102)+E(f11(x101),f11(x102)) % 0.74/0.81 [11]~E(x111,x112)+E(f7(x111),f7(x112)) % 0.74/0.81 [12]~E(x121,x122)+E(f13(x121,x123),f13(x122,x123)) % 0.74/0.81 [13]~E(x131,x132)+E(f13(x133,x131),f13(x133,x132)) % 0.74/0.81 [14]~E(x141,x142)+E(f4(x141),f4(x142)) % 0.74/0.81 [15]~P1(x151)+P1(x152)+~E(x151,x152) % 0.74/0.81 [16]P3(x162,x163)+~E(x161,x162)+~P3(x161,x163) % 0.74/0.81 [17]P3(x173,x172)+~E(x171,x172)+~P3(x173,x171) % 0.74/0.81 [18]P2(x182,x183)+~E(x181,x182)+~P2(x181,x183) % 0.74/0.81 [19]P2(x193,x192)+~E(x191,x192)+~P2(x193,x191) % 0.74/0.81 % 0.74/0.81 %------------------------------------------- % 0.74/0.81 cnf(47,plain, % 0.74/0.81 (~P3(x471,f10(x472,x473))+P3(x471,x472)), % 0.74/0.81 inference(equality_inference,[],[39])). % 0.74/0.81 cnf(48,plain, % 0.74/0.81 (~P3(x481,x482)+~P3(x481,f10(x483,x482))), % 0.74/0.81 inference(equality_inference,[],[40])). % 0.74/0.81 cnf(49,plain, % 0.74/0.81 (~P3(x491,x492)+P3(x491,f10(x492,x493))+P3(x491,x493)), % 0.74/0.81 inference(equality_inference,[],[42])). % 0.74/0.81 cnf(50,plain, % 0.74/0.81 (~P3(x501,a1)), % 0.74/0.81 inference(scs_inference,[],[20,35])). % 0.74/0.81 cnf(52,plain, % 0.74/0.81 (~P3(a9,a5)), % 0.74/0.81 inference(scs_inference,[],[23,20,35,37])). % 0.74/0.81 cnf(54,plain, % 0.74/0.81 (~P3(x541,f10(a1,x542))), % 0.74/0.81 inference(scs_inference,[],[23,20,35,37,47])). % 0.74/0.81 cnf(56,plain, % 0.74/0.81 (~P3(a5,f10(x561,a9))), % 0.74/0.81 inference(scs_inference,[],[23,20,35,37,47,48])). % 0.74/0.81 cnf(58,plain, % 0.74/0.81 (E(x581,f10(x581,a1))), % 0.74/0.81 inference(scs_inference,[],[23,20,25,35,37,47,48,2])). % 0.74/0.81 cnf(60,plain, % 0.74/0.81 (E(f10(x601,a1),x601)), % 0.74/0.81 inference(rename_variables,[],[25])). % 0.74/0.81 cnf(62,plain, % 0.74/0.81 (~P3(a5,f10(f10(x621,a9),a1))), % 0.74/0.81 inference(scs_inference,[],[23,20,25,60,35,37,47,48,2,39,40])). % 0.74/0.81 cnf(63,plain, % 0.74/0.81 (E(f10(x631,a1),x631)), % 0.74/0.81 inference(rename_variables,[],[25])). % 0.74/0.81 cnf(65,plain, % 0.74/0.81 (P3(a5,f10(a9,a1))), % 0.74/0.81 inference(scs_inference,[],[23,20,25,60,35,37,47,48,2,39,40,49])). % 0.74/0.81 cnf(67,plain, % 0.74/0.81 (~E(a9,a1)), % 0.74/0.81 inference(scs_inference,[],[23,20,25,60,35,37,47,48,2,39,40,49,17])). % 0.74/0.81 cnf(68,plain, % 0.74/0.81 (P2(f7(f10(x681,a1)),x681)), % 0.74/0.81 inference(scs_inference,[],[23,20,27,25,60,63,35,37,47,48,2,39,40,49,17,19])). % 0.74/0.81 cnf(72,plain, % 0.74/0.81 (~E(a9,f10(a1,a1))), % 0.74/0.81 inference(scs_inference,[],[23,20,27,25,60,63,35,37,47,48,2,39,40,49,17,19,33,3])). % 0.74/0.81 cnf(73,plain, % 0.74/0.81 (E(f10(x731,a1),x731)), % 0.74/0.81 inference(rename_variables,[],[25])). % 0.74/0.81 cnf(76,plain, % 0.74/0.81 (P3(x761,a9)+~E(a5,x761)), % 0.74/0.81 inference(scs_inference,[],[23,20,27,25,60,63,73,30,35,37,47,48,2,39,40,49,17,19,33,3,15,16])). % 0.74/0.81 cnf(77,plain, % 0.74/0.81 (P2(x771,f11(a6))+~E(a9,x771)), % 0.74/0.81 inference(scs_inference,[],[23,26,20,27,25,60,63,73,30,35,37,47,48,2,39,40,49,17,19,33,3,15,16,18])). % 0.74/0.81 cnf(82,plain, % 0.74/0.81 (P3(f10(a5,a1),a9)), % 0.74/0.81 inference(scs_inference,[],[58,76])). % 0.74/0.81 cnf(83,plain, % 0.74/0.81 (E(x831,f10(x831,a1))), % 0.74/0.81 inference(rename_variables,[],[58])). % 0.74/0.81 cnf(84,plain, % 0.74/0.81 (P2(f10(a9,a1),f11(a6))), % 0.74/0.81 inference(scs_inference,[],[58,83,76,77])). % 0.74/0.81 cnf(85,plain, % 0.74/0.81 (E(x851,f10(x851,a1))), % 0.74/0.81 inference(rename_variables,[],[58])). % 0.74/0.81 cnf(86,plain, % 0.74/0.81 (~P3(x861,f10(f10(a1,x862),x863))), % 0.74/0.81 inference(scs_inference,[],[54,58,83,76,77,47])). % 0.74/0.81 cnf(88,plain, % 0.74/0.81 (~P3(a5,f10(x881,f13(a6,a9)))), % 0.74/0.81 inference(scs_inference,[],[29,54,58,83,76,77,47,48])). % 0.74/0.81 cnf(90,plain, % 0.74/0.81 (~P3(x901,a2)), % 0.74/0.81 inference(scs_inference,[],[29,54,21,58,83,76,77,47,48,35])). % 0.74/0.81 cnf(92,plain, % 0.74/0.81 (~P3(f13(a6,a9),a5)), % 0.74/0.81 inference(scs_inference,[],[29,54,21,58,83,76,77,47,48,35,37])). % 0.74/0.81 cnf(94,plain, % 0.74/0.81 (E(a1,f10(a1,x941))), % 0.74/0.81 inference(scs_inference,[],[29,54,21,58,83,24,76,77,47,48,35,37,2])). % 0.74/0.81 cnf(96,plain, % 0.74/0.81 (E(x961,f10(x961,a1))), % 0.74/0.81 inference(rename_variables,[],[58])). % 0.74/0.81 cnf(97,plain, % 0.74/0.81 (~E(a9,f10(a1,x971))), % 0.74/0.81 inference(scs_inference,[],[29,54,67,20,21,58,83,85,24,76,77,47,48,35,37,2,15,3])). % 0.74/0.81 cnf(98,plain, % 0.74/0.81 (~E(f13(a6,a9),f10(a1,x981))), % 0.74/0.81 inference(scs_inference,[],[29,54,67,20,21,58,83,85,24,76,77,47,48,35,37,2,15,3,17])). % 0.74/0.81 cnf(99,plain, % 0.74/0.81 (~P3(x991,f10(a1,x992))), % 0.74/0.81 inference(rename_variables,[],[54])). % 0.74/0.81 cnf(102,plain, % 0.74/0.81 (P3(a5,f10(a9,f10(a1,x1021)))), % 0.74/0.81 inference(scs_inference,[],[23,29,54,99,67,20,21,58,83,85,24,76,77,47,48,35,37,2,15,3,17,33,49])). % 0.74/0.81 cnf(108,plain, % 0.74/0.81 (P2(a9,f10(f11(a6),a1))), % 0.74/0.81 inference(scs_inference,[],[23,29,26,54,99,50,67,20,21,58,83,85,96,72,24,76,77,47,48,35,37,2,15,3,17,33,49,44,19])). % 0.74/0.81 cnf(109,plain, % 0.74/0.81 (E(x1091,f10(x1091,a1))), % 0.74/0.81 inference(rename_variables,[],[58])). % 0.74/0.81 cnf(110,plain, % 0.74/0.81 (P2(f10(f3(x1101),a1),f11(x1101))), % 0.74/0.81 inference(scs_inference,[],[23,29,26,54,99,50,67,20,21,58,83,85,96,109,28,72,24,76,77,47,48,35,37,2,15,3,17,33,49,44,19,18])). % 0.74/0.81 cnf(111,plain, % 0.74/0.81 (E(x1111,f10(x1111,a1))), % 0.74/0.81 inference(rename_variables,[],[58])). % 0.74/0.81 cnf(112,plain, % 0.74/0.81 (P3(f10(a5,a1),f13(a6,a9))), % 0.74/0.81 inference(scs_inference,[],[23,29,26,54,99,50,67,20,21,58,83,85,96,109,111,28,72,24,76,77,47,48,35,37,2,15,3,17,33,49,44,19,18,16])). % 0.74/0.81 cnf(121,plain, % 0.74/0.81 (~P3(x1211,f3(x1212))), % 0.74/0.81 inference(scs_inference,[],[52,112,22,47,48,35])). % 0.74/0.81 cnf(125,plain, % 0.74/0.81 (P3(a5,f10(a9,a2))), % 0.74/0.81 inference(scs_inference,[],[23,52,112,90,22,47,48,35,37,49])). % 0.74/0.81 cnf(128,plain, % 0.74/0.81 (P3(f12(a1,x1281,f13(a6,a9)),f13(a6,a9))), % 0.74/0.81 inference(scs_inference,[],[23,52,112,98,90,50,22,47,48,35,37,49,44])). % 0.74/0.81 cnf(132,plain, % 0.74/0.81 (E(a1,f10(a1,x1321))), % 0.74/0.81 inference(rename_variables,[],[94])). % 0.74/0.81 cnf(133,plain, % 0.74/0.81 (~E(a9,f10(f10(a1,x1331),x1332))), % 0.74/0.81 inference(scs_inference,[],[23,86,52,112,98,90,50,22,94,47,48,35,37,49,44,3,17])). % 0.74/0.81 cnf(137,plain, % 0.74/0.81 (E(x1371,f10(x1371,a1))), % 0.74/0.81 inference(rename_variables,[],[58])). % 0.74/0.81 cnf(138,plain, % 0.74/0.81 (P2(f10(a9,a1),f10(f11(a6),a1))), % 0.74/0.81 inference(scs_inference,[],[23,86,110,52,112,98,90,108,50,20,22,94,132,58,137,47,48,35,37,49,44,3,17,15,19,18])). % 0.74/0.81 cnf(139,plain, % 0.74/0.81 (E(x1391,f10(x1391,a1))), % 0.74/0.81 inference(rename_variables,[],[58])). % 0.74/0.81 cnf(140,plain, % 0.74/0.81 (P3(f10(a5,a1),f10(a9,f10(a1,x1401)))), % 0.74/0.81 inference(scs_inference,[],[23,86,110,52,112,98,90,102,108,50,20,22,94,132,58,137,139,47,48,35,37,49,44,3,17,15,19,18,16])). % 0.74/0.81 cnf(146,plain, % 0.74/0.81 (~P3(x1461,f10(f3(x1462),x1463))), % 0.74/0.81 inference(scs_inference,[],[121,47])). % 0.74/0.81 cnf(148,plain, % 0.74/0.81 (~P3(f10(a5,a1),f10(x1481,a9))), % 0.74/0.81 inference(scs_inference,[],[121,82,47,48])). % 0.74/0.81 cnf(150,plain, % 0.74/0.81 (~P3(f10(a9,f10(a1,x1501)),f10(a5,a1))), % 0.74/0.81 inference(scs_inference,[],[121,82,140,47,48,37])). % 0.74/0.81 cnf(156,plain, % 0.74/0.81 (P3(a5,f10(a9,f3(x1561)))), % 0.74/0.81 inference(scs_inference,[],[23,121,82,140,133,54,47,48,37,44,49])). % 0.74/0.81 cnf(157,plain, % 0.74/0.81 (~P3(x1571,f3(x1572))), % 0.74/0.81 inference(rename_variables,[],[121])). % 0.74/0.81 cnf(161,plain, % 0.74/0.81 (P3(f10(a5,a1),f10(a9,a1))), % 0.74/0.81 inference(scs_inference,[],[23,121,157,82,140,133,65,54,58,47,48,37,44,49,17,16])). % 0.74/0.81 cnf(162,plain, % 0.74/0.81 (E(x1621,f10(x1621,a1))), % 0.74/0.81 inference(rename_variables,[],[58])). % 0.74/0.81 cnf(164,plain, % 0.74/0.81 (E(x1641,f10(x1641,a1))), % 0.74/0.81 inference(rename_variables,[],[58])). % 0.74/0.81 cnf(165,plain, % 0.74/0.81 (P2(f10(f7(x1651),a1),x1651)), % 0.74/0.81 inference(scs_inference,[],[23,121,157,82,140,133,65,54,27,28,58,162,164,47,48,37,44,49,17,16,19,18])). % 0.74/0.81 cnf(169,plain, % 0.74/0.81 (~P3(f10(a9,a1),f10(a5,a1))), % 0.74/0.81 inference(scs_inference,[],[161,148,47,37])). % 0.74/0.81 cnf(173,plain, % 0.74/0.81 (P3(f12(a1,x1731,a9),a9)), % 0.74/0.81 inference(scs_inference,[],[161,148,50,97,47,37,48,44])). % 0.74/0.81 cnf(176,plain, % 0.74/0.81 (P3(f10(a5,a1),f10(f10(a9,a1),f10(x1761,a9)))), % 0.74/0.81 inference(scs_inference,[],[161,148,50,97,47,37,48,44,49])). % 0.74/0.81 cnf(178,plain, % 0.74/0.81 (P3(f10(a5,a1),f10(a9,f3(x1781)))), % 0.74/0.81 inference(scs_inference,[],[161,148,156,50,97,58,47,37,48,44,49,16])). % 0.74/0.81 cnf(180,plain, % 0.74/0.81 (~E(a9,f10(f3(x1801),x1802))), % 0.74/0.81 inference(scs_inference,[],[23,146,161,148,156,50,97,58,47,37,48,44,49,16,17])). % 0.74/0.81 cnf(188,plain, % 0.74/0.81 (~P3(a5,f10(x1881,f10(a9,a2)))), % 0.74/0.81 inference(scs_inference,[],[169,125,47,48])). % 0.74/0.81 cnf(190,plain, % 0.74/0.81 (~P3(f10(f10(a9,a1),f10(x1901,a9)),f10(a5,a1))), % 0.74/0.81 inference(scs_inference,[],[169,176,125,47,48,37])). % 0.74/0.81 cnf(193,plain, % 0.74/0.81 (E(f10(x1931,a1),x1931)), % 0.74/0.81 inference(rename_variables,[],[25])). % 0.74/0.81 cnf(194,plain, % 0.74/0.81 (P3(f12(f3(x1941),x1942,a9),a9)), % 0.74/0.81 inference(scs_inference,[],[98,169,176,180,125,121,25,47,48,37,3,44])). % 0.74/0.81 cnf(198,plain, % 0.74/0.81 (P3(a5,f10(a9,f10(x1981,a9)))), % 0.74/0.81 inference(scs_inference,[],[23,98,169,176,180,56,125,121,25,47,48,37,3,44,49])). % 0.74/0.82 cnf(200,plain, % 0.74/0.82 (~E(a9,f10(x2001,f13(a6,a9)))), % 0.74/0.82 inference(scs_inference,[],[23,98,169,176,180,88,56,125,121,25,47,48,37,3,44,49,17])). % 0.74/0.82 cnf(201,plain, % 0.74/0.82 (P3(a5,f10(f10(a9,a1),f10(x2011,a9)))), % 0.74/0.82 inference(scs_inference,[],[23,98,169,176,180,88,56,125,121,25,193,47,48,37,3,44,49,17,16])). % 0.74/0.82 cnf(209,plain, % 0.74/0.82 (~P3(f10(a9,f3(x2091)),f10(a5,a1))), % 0.74/0.82 inference(scs_inference,[],[190,178,47,37])). % 0.74/0.82 cnf(211,plain, % 0.74/0.82 (~P3(a5,f10(x2111,f10(a9,a1)))), % 0.74/0.82 inference(scs_inference,[],[190,178,65,47,37,48])). % 0.74/0.82 cnf(217,plain, % 0.74/0.82 (P2(f10(f7(a1),a1),f10(a1,x2171))), % 0.74/0.82 inference(scs_inference,[],[165,190,178,200,146,65,94,47,37,48,44,19])). % 0.74/0.82 cnf(219,plain, % 0.74/0.82 (P3(f10(a5,a1),f10(f10(a9,f3(x2191)),f10(x2192,a9)))), % 0.74/0.82 inference(scs_inference,[],[165,190,178,200,146,65,148,94,47,37,48,44,19,49])). % 0.74/0.82 cnf(221,plain, % 0.74/0.82 (~E(a9,f10(x2211,f10(a9,a2)))), % 0.74/0.82 inference(scs_inference,[],[23,165,190,178,188,200,146,65,148,94,47,37,48,44,19,49,17])). % 0.74/0.82 cnf(222,plain, % 0.74/0.82 (P3(f10(a5,a1),f10(a9,f10(x2221,a9)))), % 0.74/0.82 inference(scs_inference,[],[23,165,190,178,188,200,198,146,65,148,94,58,47,37,48,44,19,49,17,16])). % 0.74/0.82 cnf(224,plain, % 0.74/0.82 (P2(f7(a1),f10(a1,x2241))), % 0.74/0.82 inference(scs_inference,[],[23,165,190,178,188,200,198,146,65,148,94,25,58,47,37,48,44,19,49,17,16,18])). % 0.74/0.82 cnf(226,plain, % 0.74/0.82 (~P3(f13(a6,a9),f10(a5,x2261))), % 0.74/0.82 inference(scs_inference,[],[92,47])). % 0.74/0.82 cnf(232,plain, % 0.74/0.82 (P3(f12(f10(f10(a1,x2321),x2322),f10(a9,a2),a9),a9)), % 0.74/0.82 inference(scs_inference,[],[92,219,221,86,128,47,48,37,44])). % 0.74/0.82 cnf(236,plain, % 0.74/0.82 (P2(f7(f10(a1,a1)),f10(a1,x2361))), % 0.74/0.82 inference(scs_inference,[],[92,68,219,221,86,94,128,47,48,37,44,19])). % 0.74/0.82 cnf(238,plain, % 0.74/0.82 (~E(a9,f10(x2381,f10(a9,a1)))), % 0.74/0.82 inference(scs_inference,[],[23,92,68,219,211,221,86,94,128,47,48,37,44,19,17])). % 0.74/0.82 cnf(239,plain, % 0.74/0.82 (P3(a5,f10(f10(a9,f3(x2391)),f10(x2392,a9)))), % 0.74/0.82 inference(scs_inference,[],[23,92,68,219,211,221,86,94,25,128,47,48,37,44,19,17,16])). % 0.74/0.82 cnf(243,plain, % 0.74/0.82 (~P3(f10(a9,f10(x2431,a9)),f10(a5,a1))), % 0.74/0.82 inference(scs_inference,[],[209,222,47,37])). % 0.74/0.82 cnf(245,plain, % 0.74/0.82 (~P3(f12(f3(x2451),x2452,a9),f10(x2453,a9))), % 0.74/0.82 inference(scs_inference,[],[209,222,194,47,37,48])). % 0.74/0.82 cnf(251,plain, % 0.74/0.82 (P3(f10(a5,a1),f10(f10(a9,f10(x2511,a9)),f10(x2512,a9)))), % 0.74/0.82 inference(scs_inference,[],[200,209,222,90,148,194,47,37,48,44,49])). % 0.74/0.82 cnf(254,plain, % 0.74/0.82 (P3(f10(a5,a1),f10(a9,a2))), % 0.74/0.82 inference(scs_inference,[],[23,200,209,222,62,125,90,148,58,194,47,37,48,44,49,17,16])). % 0.74/0.82 cnf(260,plain, % 0.74/0.82 (~P3(f10(a9,a2),f10(a5,a1))), % 0.74/0.82 inference(scs_inference,[],[254,243,47,48,37])). % 0.74/0.82 cnf(262,plain, % 0.74/0.82 (P3(f12(f10(f3(x2621),x2622),f10(a9,a1),a9),a9)), % 0.74/0.82 inference(scs_inference,[],[238,254,243,146,47,48,37,44])). % 0.74/0.82 cnf(266,plain, % 0.74/0.82 (P3(f12(f3(x2661),x2662,a9),f10(a9,f10(x2663,a9)))), % 0.74/0.82 inference(scs_inference,[],[238,254,243,245,146,194,47,48,37,44,49])). % 0.74/0.82 cnf(269,plain, % 0.74/0.82 (~E(f13(a6,a9),f10(x2691,f10(a9,a1)))), % 0.74/0.82 inference(scs_inference,[],[29,238,254,243,245,211,146,194,47,48,37,44,49,17])). % 0.74/0.82 cnf(270,plain, % 0.74/0.82 (P3(a5,f10(f10(a9,f10(x2701,a9)),f10(x2702,a9)))), % 0.74/0.82 inference(scs_inference,[],[29,238,254,251,243,245,211,146,25,194,47,48,37,44,49,17,16])). % 0.74/0.82 cnf(282,plain, % 0.74/0.82 (E(x2821,f10(x2821,a1))), % 0.74/0.82 inference(rename_variables,[],[58])). % 0.74/0.82 cnf(288,plain, % 0.74/0.82 (E(x2881,f10(x2881,a1))), % 0.74/0.82 inference(rename_variables,[],[58])). % 0.74/0.82 cnf(289,plain, % 0.74/0.82 (P3(f10(f10(a5,a1),a1),a9)), % 0.74/0.82 inference(scs_inference,[],[84,200,217,260,266,82,86,58,282,288,262,47,37,48,18,44,19,16])). % 0.74/0.82 cnf(294,plain, % 0.74/0.82 (~P3(f10(f10(a5,a1),a1),f10(x2941,a9))), % 0.74/0.82 inference(scs_inference,[],[150,289,47,48])). % 0.74/0.82 cnf(296,plain, % 0.74/0.82 (~P3(f10(f10(a9,a1),f10(x2961,a9)),a5)), % 0.74/0.82 inference(scs_inference,[],[150,201,289,47,48,37])). % 0.74/0.82 cnf(299,plain, % 0.74/0.82 (E(x2991,f10(x2991,a1))), % 0.74/0.82 inference(rename_variables,[],[58])). % 0.74/0.82 cnf(307,plain, % 0.74/0.82 (E(x3071,f10(x3071,a1))), % 0.74/0.82 inference(rename_variables,[],[58])). % 0.74/0.82 cnf(308,plain, % 0.74/0.82 (P3(f10(f10(a5,a1),a1),f10(a9,f10(a1,x3081)))), % 0.74/0.82 inference(scs_inference,[],[138,221,224,150,201,289,140,90,58,299,307,47,48,37,18,44,49,19,16])). % 0.74/0.82 cnf(310,plain, % 0.74/0.82 (~E(f13(a6,a9),f10(x3101,f10(a9,a2)))), % 0.74/0.82 inference(scs_inference,[],[29,138,221,224,150,201,289,140,188,90,58,299,307,47,48,37,18,44,49,19,16,17])). % 0.74/0.82 cnf(314,plain, % 0.74/0.82 (~P3(f10(f10(a5,a1),a1),f10(f10(x3141,a9),x3142))), % 0.74/0.82 inference(scs_inference,[],[294,47])). % 0.74/0.82 cnf(320,plain, % 0.74/0.82 (P3(f12(f3(x3201),f10(a9,a1),f13(a6,a9)),f13(a6,a9))), % 0.74/0.82 inference(scs_inference,[],[269,294,239,121,232,47,37,48,44])). % 0.74/0.82 cnf(324,plain, % 0.74/0.82 (P3(f10(f12(a1,x3241,a9),a1),a9)), % 0.74/0.82 inference(scs_inference,[],[269,294,239,121,58,232,173,47,37,48,44,16])). % 0.74/0.82 cnf(329,plain, % 0.74/0.82 (~P3(f10(f12(a1,x3291,a9),a1),f10(x3292,a9))), % 0.74/0.82 inference(scs_inference,[],[226,324,47,48])). % 0.74/0.82 cnf(337,plain, % 0.74/0.82 (P3(f10(f12(a1,x3371,a9),a1),f10(a9,f10(x3372,a9)))), % 0.74/0.82 inference(scs_inference,[],[269,226,270,324,146,47,48,37,44,49])). % 0.74/0.82 cnf(339,plain, % 0.74/0.82 (P3(f12(a1,x3391,a9),f10(a9,f10(x3392,a9)))), % 0.74/0.82 inference(scs_inference,[],[269,226,270,324,146,25,47,48,37,44,49,16])). % 0.74/0.82 cnf(357,plain, % 0.74/0.82 (E(x3571,f10(x3571,a1))), % 0.74/0.82 inference(rename_variables,[],[58])). % 0.74/0.82 cnf(359,plain, % 0.74/0.82 (P3(f10(f10(a5,a1),a1),f13(a6,a9))), % 0.74/0.82 inference(scs_inference,[],[310,236,314,308,329,337,112,86,58,357,320,47,37,48,44,19,17,16])). % 0.74/0.82 cnf(378,plain, % 0.74/0.82 ($false), % 0.74/0.82 inference(scs_inference,[],[26,29,269,296,56,54,359,339,294,25,47,48,37,44,49,16,17,38]), % 0.74/0.82 ['proof']). % 0.74/0.82 % SZS output end Proof % 0.74/0.82 % Total time :0.200000s %------------------------------------------------------------------------------