%------------------------------------------------------------------------------ % File : CSE-F---1.0 % Problem : SYO607+1 : TPTP v7.5.0. Released v7.0.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n004.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 : 600s % DateTime : Tue Mar 29 01:05:41 EDT 2022 % Result : Theorem 52.00s 52.08s % Output : CNFRefutation 52.11s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.12 % Problem : SYO607+1 : TPTP v7.5.0. Released v7.0.0. % 0.08/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.13/0.33 % Computer : n004.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPUModel : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % RAMPerCPU : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 600 % 0.13/0.33 % DateTime : Mon Mar 14 06:23:10 EDT 2022 % 0.13/0.33 % CPUTime : % 0.18/0.45 openjdk version "1.8.0_171" % 0.18/0.45 OpenJDK Runtime Environment (build 1.8.0_171-b10) % 0.18/0.45 OpenJDK 64-Bit Server VM (build 25.171-b10, mixed mode) % 0.18/0.45 file=/export/starexec/sandbox2/benchmark/theBenchmark.p % 0.53/0.68 start to proof:theBenchmark % 52.00/52.08 % Version : CSE-F---1.0 % 52.00/52.08 % Problem : theBenchmark.p % 52.00/52.08 % Proof found % 52.00/52.08 % SZS status Theorem for theBenchmark.p % 52.00/52.08 % SZS output start Proof % 52.00/52.08 [1]~P1(x11,f1(x11)) % 52.00/52.08 [2]~P1(x21,x22)+P2(x21,x22) % 52.00/52.08 [3]~P3(x31,x32)+P2(x31,x32) % 52.00/52.08 [4]~P5(x41,x42)+P4(x41,x42) % 52.00/52.08 [5]~P3(x51,x52)+P4(x51,x52) % 52.00/52.08 [6]~P5(x61,x62)+~P5(a2,x61) % 52.00/52.08 [8]~P2(x81,x82)+~P5(x81,x82) % 52.00/52.08 [9]~P4(x91,x92)+~P1(x91,x92) % 52.00/52.08 [7]P1(x71,x72)+P3(x71,x72)+P5(x71,x72) % 52.00/52.08 [10]P2(x101,x102)+~P4(x101,x102)+P5(x101,x102) % 52.00/52.08 [11]P4(x111,x112)+~P2(x111,x112)+P1(x111,x112) % 52.00/52.08 [12]~P2(x121,x122)+~P4(x121,x122)+P3(x121,x122) % 52.00/52.08 [13]P1(x131,x132)+~P3(x134,x135)+P1(a2,x131)+~P3(a2,x131)+P5(x134,f4(x134))+P1(a3,x133)+P5(a2,a5) % 52.00/52.08 [14]P1(x141,x142)+~P3(x144,x145)+P1(a2,x141)+~P3(a2,x141)+P5(x144,f4(x144))+P1(a3,x143)+P5(a5,a7) % 52.00/52.08 [15]P1(x151,x152)+~P3(x154,x155)+~P3(x151,x156)+P1(a2,x151)+P5(x151,f6(x151))+P5(x154,f4(x154))+P1(a3,x153)+P5(a2,a5) % 52.00/52.08 [16]P1(x161,x162)+~P3(x164,x165)+~P3(x161,x166)+P1(a2,x161)+P5(x161,f6(x161))+P5(x164,f4(x164))+P1(a3,x163)+P5(a5,a7) % 52.00/52.10 cnf(17,plain, % 52.00/52.10 (~P1(x171,f1(x171))), % 52.00/52.10 inference(rename_variables,[],[1])). % 52.00/52.10 cnf(19,plain, % 52.00/52.10 (P1(f1(a2),x191)+~P3(x192,x193)+~P3(f1(a2),x194)+P5(f1(a2),f6(f1(a2)))+P5(a2,a5)+P5(x192,f4(x192))+P1(a3,x195)), % 52.00/52.10 inference(scs_inference,[],[1,17,15])). % 52.00/52.10 cnf(20,plain, % 52.00/52.10 (P1(x201,x202)+~P3(x203,x204)+P1(a2,x201)+~P3(a2,x201)+P5(x203,f4(x203))+P5(a2,a5)), % 52.00/52.10 inference(scs_inference,[],[1,13])). % 52.00/52.10 cnf(21,plain, % 52.00/52.10 (P1(x211,x212)+~P3(x213,x214)+P1(a2,x211)+~P3(a2,x211)+P5(x213,f4(x213))+P5(a5,a7)), % 52.00/52.10 inference(scs_inference,[],[1,14])). % 52.00/52.10 cnf(23,plain, % 52.00/52.10 (P1(x231,x232)+~P3(x233,x234)+~P3(x231,x235)+P1(a2,x231)+P5(x231,f6(x231))+P5(x233,f4(x233))+P5(a5,a7)), % 52.00/52.10 inference(scs_inference,[],[1,16])). % 52.00/52.10 cnf(25,plain, % 52.00/52.10 (P5(x251,f4(x251))+P1(f1(a2),x252)+~P3(x251,x253)+P5(a2,a5)+~P3(a2,f1(a2))), % 52.00/52.10 inference(scs_inference,[],[1,20])). % 52.00/52.10 cnf(26,plain, % 52.00/52.10 (P5(x261,f4(x261))+~P3(x261,x262)+P1(f1(a2),x263)+~P3(f1(a2),x264)+P5(f1(a2),f6(f1(a2)))+P5(a2,a5)), % 52.00/52.10 inference(scs_inference,[],[1,19])). % 52.00/52.10 cnf(28,plain, % 52.00/52.10 (P5(x281,f4(x281))+P1(f1(a2),x282)+~P3(x281,x283)+P5(a5,a7)+~P3(a2,f1(a2))), % 52.00/52.10 inference(scs_inference,[],[1,21])). % 52.00/52.10 cnf(29,plain, % 52.00/52.10 (P5(x291,f4(x291))+~P3(x291,x292)+~P3(a2,f1(a2))+P5(a2,a5)), % 52.00/52.10 inference(scs_inference,[],[1,25])). % 52.00/52.10 cnf(32,plain, % 52.00/52.10 (P5(x321,f4(x321))+~P3(x321,x322)+~P3(f1(a2),x323)+P5(f1(a2),f6(f1(a2)))+P5(a2,a5)), % 52.00/52.10 inference(scs_inference,[],[1,26])). % 52.00/52.10 cnf(33,plain, % 52.00/52.10 (P5(x331,f4(x331))+~P3(x331,x332)+~P3(a2,f1(a2))+P5(a5,a7)), % 52.00/52.10 inference(scs_inference,[],[1,28])). % 52.00/52.10 cnf(73,plain, % 52.00/52.10 (~P5(x731,x732)+~P3(x731,x732)), % 52.00/52.10 inference(scs_inference,[],[3,8])). % 52.00/52.10 cnf(135,plain, % 52.00/52.10 (~P1(x1351,x1352)+~P3(x1351,x1352)), % 52.00/52.10 inference(scs_inference,[],[5,9])). % 52.00/52.10 cnf(166,plain, % 52.00/52.10 (P3(x1661,f1(x1661))+~P5(a2,x1661)), % 52.00/52.10 inference(scs_inference,[],[1,6,7])). % 52.00/52.10 cnf(657,plain, % 52.00/52.10 (P2(x6571,x6572)+P3(x6571,x6572)+P5(x6571,x6572)), % 52.00/52.10 inference(scs_inference,[],[2,7])). % 52.00/52.10 cnf(688,plain, % 52.00/52.10 (P5(x6881,x6882)+P2(x6881,x6882)), % 52.00/52.10 inference(scs_inference,[],[657,3])). % 52.00/52.10 cnf(709,plain, % 52.00/52.10 (P5(x7091,f1(x7091))+P3(x7091,f1(x7091))), % 52.00/52.10 inference(scs_inference,[],[1,7])). % 52.00/52.10 cnf(711,plain, % 52.00/52.10 (P3(a2,f1(a2))+~P5(f1(a2),x7111)), % 52.00/52.10 inference(scs_inference,[],[1,7,6])). % 52.00/52.10 cnf(713,plain, % 52.00/52.10 (P3(a2,f1(a2))+P3(f1(a2),f1(f1(a2)))), % 52.00/52.10 inference(scs_inference,[],[1,7,6,166])). % 52.00/52.10 cnf(789,plain, % 52.00/52.10 (P4(x7891,f1(x7891))+P5(x7891,f1(x7891))), % 52.00/52.10 inference(scs_inference,[],[709,5])). % 52.00/52.10 cnf(851,plain, % 52.00/52.10 (P4(x8511,f1(x8511))), % 52.00/52.10 inference(scs_inference,[],[789,4])). % 52.00/52.10 cnf(852,plain, % 52.00/52.10 (P3(x8521,f1(x8521))+~P2(x8521,f1(x8521))), % 52.00/52.10 inference(scs_inference,[],[851,12])). % 52.00/52.10 cnf(856,plain, % 52.00/52.10 (~P1(x8561,f1(x8561))), % 52.00/52.10 inference(rename_variables,[],[1])). % 52.00/52.10 cnf(858,plain, % 52.00/52.10 (P5(a2,f1(a2))+P5(a2,f4(a2))+~P2(a2,f1(a2))+P1(f1(a2),x8581)+P5(a5,a7)), % 52.00/52.10 inference(scs_inference,[],[1,856,851,12,3,7,21])). % 52.00/52.10 cnf(861,plain, % 52.00/52.10 (P5(a2,f1(a2))+P5(a5,a7)+P5(a2,f4(a2))+~P2(a2,f1(a2))), % 52.00/52.10 inference(scs_inference,[],[1,858])). % 52.00/52.10 cnf(886,plain, % 52.00/52.10 (~P2(a2,f1(a2))+P5(a2,f4(a2))+P5(a2,a5)), % 52.00/52.10 inference(scs_inference,[],[852,29])). % 52.00/52.10 cnf(1624,plain, % 52.00/52.10 (~P3(a2,f1(a2))+P5(a2,f4(a2))+P5(a2,a5)), % 52.00/52.10 inference(scs_inference,[],[3,886])). % 52.00/52.10 cnf(1655,plain, % 52.00/52.10 (P5(a2,f1(a2))+P5(a2,f4(a2))+P5(a2,a5)), % 52.00/52.10 inference(scs_inference,[],[1624,709])). % 52.00/52.10 cnf(1686,plain, % 52.00/52.11 (P4(a2,f4(a2))+P5(a2,f1(a2))+P5(a2,a5)), % 52.00/52.11 inference(scs_inference,[],[1655,4])). % 52.00/52.11 cnf(1839,plain, % 52.00/52.11 (P4(x18391,x18392)+P2(x18391,x18392)), % 52.00/52.11 inference(scs_inference,[],[4,688])). % 52.00/52.11 cnf(1962,plain, % 52.00/52.11 (P4(a2,f4(a2))+~P2(a2,f1(a2))+P5(a2,a5)), % 52.00/52.11 inference(scs_inference,[],[4,886])). % 52.00/52.11 cnf(3650,plain, % 52.00/52.11 (P2(a2,x36501)+~P5(x36501,x36502)), % 52.00/52.11 inference(scs_inference,[],[6,688])). % 52.00/52.11 cnf(3681,plain, % 52.00/52.11 (P3(x36811,f1(x36811))+P2(a2,x36811)), % 52.00/52.11 inference(scs_inference,[],[3650,709])). % 52.00/52.11 cnf(4082,plain, % 52.00/52.11 (~P5(f4(a2),x40821)+~P2(a2,f1(a2))+P5(a2,a5)), % 52.00/52.11 inference(scs_inference,[],[6,886])). % 52.00/52.11 cnf(4329,plain, % 52.00/52.11 (~P5(a5,x43291)+~P2(a2,f1(a2))+P5(a2,f4(a2))), % 52.00/52.11 inference(scs_inference,[],[6,886])). % 52.00/52.11 cnf(4360,plain, % 52.00/52.11 (~P3(a2,f1(a2))+P5(a2,f4(a2))+~P5(a5,x43601)), % 52.00/52.11 inference(scs_inference,[],[4329,3])). % 52.00/52.11 cnf(4391,plain, % 52.00/52.11 (P5(a2,f1(a2))+P5(a2,f4(a2))+~P5(a5,x43911)), % 52.00/52.11 inference(scs_inference,[],[4360,709])). % 52.00/52.11 cnf(4422,plain, % 52.00/52.11 (P3(f1(a2),f1(f1(a2)))+P5(a2,f4(a2))+~P5(a5,x44221)), % 52.00/52.11 inference(scs_inference,[],[4391,166])). % 52.00/52.11 cnf(4453,plain, % 52.00/52.11 (P2(f1(a2),f1(f1(a2)))+P5(a2,f4(a2))+~P5(a5,x44531)), % 52.00/52.11 inference(scs_inference,[],[4422,3])). % 52.00/52.11 cnf(4484,plain, % 52.00/52.11 (~P2(a2,f4(a2))+P2(f1(a2),f1(f1(a2)))+~P5(a5,x44841)), % 52.00/52.11 inference(scs_inference,[],[4453,8])). % 52.00/52.11 cnf(4515,plain, % 52.00/52.11 (P3(f1(a2),f1(f1(a2)))+~P2(a2,f4(a2))+~P5(a5,x45151)), % 52.00/52.11 inference(scs_inference,[],[851,4484,12])). % 52.00/52.11 cnf(5191,plain, % 52.00/52.11 (~P5(a5,x51911)+P4(a2,f4(a2))+P5(a2,f1(a2))), % 52.00/52.11 inference(scs_inference,[],[6,1686])). % 52.00/52.11 cnf(5283,plain, % 52.00/52.11 (~P5(a5,x52831)+P4(a2,f4(a2))+~P2(a2,f1(a2))), % 52.00/52.11 inference(scs_inference,[],[6,1962])). % 52.00/52.11 cnf(5314,plain, % 52.00/52.11 (~P1(a2,f4(a2))+~P2(a2,f1(a2))+~P5(a5,x53141)), % 52.00/52.11 inference(scs_inference,[],[5283,9])). % 52.00/52.11 cnf(10051,plain, % 52.00/52.11 (~P2(a2,a5)+~P2(a2,f1(a2))+~P5(f4(a2),x100511)), % 52.00/52.11 inference(scs_inference,[],[8,4082])). % 52.00/52.11 cnf(11098,plain, % 52.00/52.11 (~P2(a2,f4(a2))+~P2(a2,f1(a2))+~P5(a5,x110981)), % 52.00/52.11 inference(scs_inference,[],[8,4329])). % 52.00/52.11 cnf(11129,plain, % 52.00/52.11 (~P3(a2,f4(a2))+~P2(a2,f1(a2))+~P5(a5,x111291)), % 52.00/52.11 inference(scs_inference,[],[11098,3])). % 52.00/52.11 cnf(11252,plain, % 52.00/52.11 (~P2(a2,f4(a2))+~P3(a2,f1(a2))+~P5(a5,x112521)), % 52.00/52.11 inference(scs_inference,[],[8,4360])). % 52.00/52.11 cnf(11283,plain, % 52.00/52.11 (~P3(a2,f1(a2))+~P3(a2,f4(a2))+~P5(a5,x112831)), % 52.00/52.11 inference(scs_inference,[],[11252,3])). % 52.00/52.11 cnf(15621,plain, % 52.00/52.11 (~P2(a2,f1(a2))+P5(a2,f4(a2))+P5(a5,a7)), % 52.00/52.11 inference(scs_inference,[],[8,861])). % 52.00/52.11 cnf(15652,plain, % 52.00/52.11 (~P3(a2,f1(a2))+P5(a2,f4(a2))+P5(a5,a7)), % 52.00/52.11 inference(scs_inference,[],[15621,3])). % 52.00/52.11 cnf(15683,plain, % 52.00/52.11 (P5(a2,f1(a2))+P5(a2,f4(a2))+P5(a5,a7)), % 52.00/52.11 inference(scs_inference,[],[15652,709])). % 52.00/52.11 cnf(16145,plain, % 52.00/52.11 (~P2(a5,a7)+~P2(a2,f1(a2))+P5(a2,f4(a2))), % 52.00/52.11 inference(scs_inference,[],[8,15621])). % 52.00/52.11 cnf(16176,plain, % 52.00/52.11 (~P3(a2,f1(a2))+P5(a2,f4(a2))+~P2(a5,a7)), % 52.00/52.11 inference(scs_inference,[],[16145,3])). % 52.00/52.11 cnf(16207,plain, % 52.00/52.11 (P5(a2,f1(a2))+P5(a2,f4(a2))+~P2(a5,a7)), % 52.00/52.11 inference(scs_inference,[],[16176,709])). % 52.00/52.11 cnf(16361,plain, % 52.00/52.11 (~P2(a2,f4(a2))+~P3(a2,f1(a2))+P5(a5,a7)), % 52.00/52.11 inference(scs_inference,[],[8,15652])). % 52.00/52.11 cnf(16392,plain, % 52.00/52.11 (~P3(a2,f1(a2))+~P1(a2,f4(a2))+P5(a5,a7)), % 52.00/52.11 inference(scs_inference,[],[16361,2])). % 52.00/52.11 cnf(16423,plain, % 52.00/52.11 (P5(a2,f1(a2))+~P1(a2,f4(a2))+P5(a5,a7)), % 52.00/52.11 inference(scs_inference,[],[16392,709])). % 52.00/52.11 cnf(16454,plain, % 52.00/52.11 (~P2(a2,f1(a2))+~P1(a2,f4(a2))+P5(a2,f1(a2))), % 52.00/52.11 inference(scs_inference,[],[16423,5314])). % 52.00/52.11 cnf(16546,plain, % 52.00/52.11 (~P2(a2,f4(a2))+P5(a2,f1(a2))+P5(a5,a7)), % 52.00/52.11 inference(scs_inference,[],[8,15683])). % 52.00/52.11 cnf(16577,plain, % 52.00/52.11 (~P3(a2,f4(a2))+P5(a2,f1(a2))+P5(a5,a7)), % 52.00/52.11 inference(scs_inference,[],[16546,3])). % 52.00/52.11 cnf(17347,plain, % 52.00/52.11 (~P2(a2,f4(a2))+P5(a2,f1(a2))+~P2(a5,a7)), % 52.00/52.11 inference(scs_inference,[],[8,16207])). % 52.00/52.11 cnf(17378,plain, % 52.00/52.11 (~P3(a2,f4(a2))+P5(a2,f1(a2))+~P2(a5,a7)), % 52.00/52.11 inference(scs_inference,[],[17347,3])). % 52.00/52.11 cnf(17624,plain, % 52.00/52.11 (~P2(a2,f1(a2))+~P1(a2,f4(a2))), % 52.00/52.11 inference(scs_inference,[],[8,16454])). % 52.00/52.11 cnf(17655,plain, % 52.00/52.11 (~P3(a2,f1(a2))+~P1(a2,f4(a2))), % 52.00/52.11 inference(scs_inference,[],[17624,3])). % 52.00/52.11 cnf(17686,plain, % 52.00/52.11 (P5(a2,f1(a2))+~P1(a2,f4(a2))), % 52.00/52.11 inference(scs_inference,[],[17655,709])). % 52.00/52.11 cnf(17717,plain, % 52.00/52.11 (P5(a2,f4(a2))+P3(a2,f4(a2))+P5(a2,f1(a2))), % 52.00/52.11 inference(scs_inference,[],[17686,7])). % 52.00/52.11 cnf(18057,plain, % 52.00/52.11 (~P2(a2,f1(a2))+~P3(a2,f4(a2))+P5(a5,a7)), % 52.00/52.11 inference(scs_inference,[],[8,16577])). % 52.00/52.11 cnf(18088,plain, % 52.00/52.11 (~P3(a2,f1(a2))+~P3(a2,f4(a2))+P5(a5,a7)), % 52.00/52.11 inference(scs_inference,[],[18057,3])). % 52.00/52.11 cnf(18119,plain, % 52.00/52.11 (P3(f1(a2),f1(f1(a2)))+~P3(a2,f4(a2))+P5(a5,a7)), % 52.00/52.11 inference(scs_inference,[],[18088,713])). % 52.00/52.11 cnf(18150,plain, % 52.00/52.11 (P2(f1(a2),f1(f1(a2)))+~P3(a2,f4(a2))+P5(a5,a7)), % 52.00/52.11 inference(scs_inference,[],[18119,3])). % 52.00/52.11 cnf(18642,plain, % 52.00/52.11 (~P2(a2,f1(a2))+~P2(a5,a7)+~P3(a2,f4(a2))), % 52.00/52.11 inference(scs_inference,[],[8,17378])). % 52.00/52.11 cnf(18673,plain, % 52.00/52.11 (~P3(a2,f1(a2))+~P2(a5,a7)+~P3(a2,f4(a2))), % 52.00/52.11 inference(scs_inference,[],[18642,3])). % 52.00/52.11 cnf(18827,plain, % 52.00/52.11 (~P2(a2,f4(a2))+P5(a2,f1(a2))+P3(a2,f4(a2))), % 52.00/52.11 inference(scs_inference,[],[8,17717])). % 52.00/52.11 cnf(18858,plain, % 52.00/52.11 (P4(a2,f4(a2))+P5(a2,f1(a2))+P3(a2,f4(a2))), % 52.00/52.11 inference(scs_inference,[],[18827,1839])). % 52.00/52.11 cnf(19755,plain, % 52.00/52.11 (~P2(a5,a7)+P2(f1(a2),f1(f1(a2)))+~P3(a2,f4(a2))), % 52.00/52.11 inference(scs_inference,[],[8,18150])). % 52.00/52.11 cnf(20341,plain, % 52.00/52.11 (~P2(a2,f1(a2))+P4(a2,f4(a2))+P3(a2,f4(a2))), % 52.00/52.11 inference(scs_inference,[],[8,18858])). % 52.00/52.11 cnf(20372,plain, % 52.00/52.11 (~P2(a2,f1(a2))+P4(a2,f4(a2))+P5(a5,a7)), % 52.00/52.11 inference(scs_inference,[],[20341,18057])). % 52.00/52.11 cnf(20403,plain, % 52.00/52.11 (~P3(a2,f1(a2))+P4(a2,f4(a2))+P5(a5,a7)), % 52.00/52.11 inference(scs_inference,[],[20372,3])). % 52.00/52.11 cnf(20434,plain, % 52.00/52.11 (P5(a2,f1(a2))+P4(a2,f4(a2))+P5(a5,a7)), % 52.00/52.11 inference(scs_inference,[],[20403,709])). % 52.00/52.11 cnf(20465,plain, % 52.00/52.11 (P4(a2,f4(a2))+P5(a2,f1(a2))), % 52.00/52.11 inference(scs_inference,[],[20434,5191])). % 52.00/52.11 cnf(20496,plain, % 52.00/52.11 (~P3(a2,f1(a2))+P4(a2,f4(a2))), % 52.00/52.11 inference(scs_inference,[],[20465,73])). % 52.00/52.11 cnf(20527,plain, % 52.00/52.11 (P4(a2,f4(a2))+P3(f1(a2),f1(f1(a2)))), % 52.00/52.11 inference(scs_inference,[],[20496,713])). % 52.00/52.11 cnf(20558,plain, % 52.00/52.11 (P3(a2,f4(a2))+~P2(a2,f4(a2))+P3(f1(a2),f1(f1(a2)))), % 52.00/52.11 inference(scs_inference,[],[20527,12])). % 52.00/52.11 cnf(20589,plain, % 52.00/52.11 (P3(f4(a2),f1(f4(a2)))+P3(f1(a2),f1(f1(a2)))+P3(a2,f4(a2))), % 52.00/52.11 inference(scs_inference,[],[20558,3681])). % 52.00/52.11 cnf(20620,plain, % 52.00/52.11 (P2(f1(a2),f1(f1(a2)))+P3(f4(a2),f1(f4(a2)))+P3(a2,f4(a2))), % 52.00/52.11 inference(scs_inference,[],[20589,3])). % 52.00/52.11 cnf(20651,plain, % 52.00/52.11 (P2(f4(a2),f1(f4(a2)))+P2(f1(a2),f1(f1(a2)))+P3(a2,f4(a2))), % 52.00/52.11 inference(scs_inference,[],[20620,3])). % 52.00/52.11 cnf(20682,plain, % 52.00/52.11 (P3(f1(a2),f1(f1(a2)))+P2(f4(a2),f1(f4(a2)))+P3(a2,f4(a2))), % 52.00/52.11 inference(scs_inference,[],[851,20651,12])). % 52.00/52.11 cnf(26143,plain, % 52.00/52.11 (P2(x261431,x261432)+P2(a2,x261431)), % 52.00/52.11 inference(scs_inference,[],[688,3650])). % 52.00/52.11 cnf(26174,plain, % 52.00/52.11 (~P2(a2,f1(a2))+P5(a2,f4(a2))+P2(a2,a5)), % 52.00/52.11 inference(scs_inference,[],[26143,16145])). % 52.00/52.11 cnf(26205,plain, % 52.00/52.11 (~P3(a2,f1(a2))+P5(a2,f4(a2))+P2(a2,a5)), % 52.00/52.11 inference(scs_inference,[],[26174,3])). % 52.00/52.11 cnf(27593,plain, % 52.00/52.11 (P2(a5,x275931)+~P2(a2,f4(a2))+P3(f1(a2),f1(f1(a2)))), % 52.00/52.11 inference(scs_inference,[],[688,4515])). % 52.00/52.11 cnf(27624,plain, % 52.00/52.11 (~P3(a2,f4(a2))+P3(f1(a2),f1(f1(a2)))+P2(a5,x276241)), % 52.00/52.11 inference(scs_inference,[],[27593,3])). % 52.00/52.11 cnf(27655,plain, % 52.00/52.11 (P3(f1(a2),f1(f1(a2)))+P2(f4(a2),f1(f4(a2)))+P2(a5,x276551)), % 52.00/52.11 inference(scs_inference,[],[27624,20682])). % 52.00/52.11 cnf(27686,plain, % 52.00/52.11 (P2(f1(a2),f1(f1(a2)))+P2(f4(a2),f1(f4(a2)))+P2(a5,x276861)), % 52.00/52.11 inference(scs_inference,[],[27655,3])). % 52.00/52.11 cnf(27717,plain, % 52.00/52.11 (~P3(a2,f4(a2))+P2(f1(a2),f1(f1(a2)))+P2(f4(a2),f1(f4(a2)))), % 52.00/52.11 inference(scs_inference,[],[27686,19755])). % 52.00/52.11 cnf(27748,plain, % 52.00/52.11 (P2(f1(a2),f1(f1(a2)))+P3(f4(a2),f1(f4(a2)))+P2(f4(a2),f1(f4(a2)))), % 52.00/52.11 inference(scs_inference,[],[27717,20620])). % 52.00/52.11 cnf(27779,plain, % 52.00/52.11 (P3(f1(a2),f1(f1(a2)))+P3(f4(a2),f1(f4(a2)))+P2(f4(a2),f1(f4(a2)))), % 52.00/52.11 inference(scs_inference,[],[851,27748,12])). % 52.00/52.11 cnf(27810,plain, % 52.00/52.11 (P2(f4(a2),f1(f4(a2)))+P3(f1(a2),f1(f1(a2)))), % 52.00/52.11 inference(scs_inference,[],[27779,3])). % 52.00/52.11 cnf(27841,plain, % 52.00/52.11 (P2(f1(a2),f1(f1(a2)))+P2(f4(a2),f1(f4(a2)))), % 52.00/52.11 inference(scs_inference,[],[27810,3])). % 52.00/52.11 cnf(27872,plain, % 52.00/52.11 (P3(f4(a2),f1(f4(a2)))+P2(f1(a2),f1(f1(a2)))), % 52.00/52.11 inference(scs_inference,[],[851,27841,12])). % 52.00/52.11 cnf(27903,plain, % 52.00/52.11 (P3(f1(a2),f1(f1(a2)))+P3(f4(a2),f1(f4(a2)))), % 52.00/52.11 inference(scs_inference,[],[851,27872,12])). % 52.00/52.11 cnf(29195,plain, % 52.00/52.11 (P2(f4(a2),x291951)+~P2(a2,f1(a2))+~P2(a2,a5)), % 52.00/52.11 inference(scs_inference,[],[688,10051])). % 52.00/52.11 cnf(29226,plain, % 52.00/52.11 (~P2(a2,a5)+~P3(a2,f1(a2))+P2(f4(a2),x292261)), % 52.00/52.11 inference(scs_inference,[],[29195,3])). % 52.00/52.11 cnf(29257,plain, % 52.00/52.11 (P5(a2,f4(a2))+~P3(a2,f1(a2))+P2(f4(a2),x292571)), % 52.00/52.11 inference(scs_inference,[],[29226,26205])). % 52.00/52.11 cnf(29288,plain, % 52.00/52.11 (~P3(a2,f1(a2))+~P5(f4(a2),x292881)+P2(f4(a2),x292882)), % 52.00/52.11 inference(scs_inference,[],[29257,6])). % 52.00/52.11 cnf(29319,plain, % 52.00/52.11 (~P3(a2,f1(a2))+P3(f4(a2),f1(f4(a2)))+P2(f4(a2),x293191)), % 52.00/52.11 inference(scs_inference,[],[29288,709])). % 52.00/52.11 cnf(29350,plain, % 52.00/52.11 (P3(f4(a2),f1(f4(a2)))+P2(f4(a2),x293501)+~P5(f1(a2),x293502)), % 52.00/52.11 inference(scs_inference,[],[29319,711])). % 52.00/52.11 cnf(29381,plain, % 52.00/52.11 (P2(f4(a2),f1(f4(a2)))+P2(f4(a2),x293811)+~P5(f1(a2),x293812)), % 52.00/52.11 inference(scs_inference,[],[29350,3])). % 52.00/52.11 cnf(29382,plain, % 52.00/52.11 (P2(f4(a2),f1(f4(a2)))+~P5(f1(a2),x293821)), % 52.00/52.11 inference(factoring_inference,[],[29381])). % 52.00/52.11 cnf(29413,plain, % 52.00/52.11 (P3(f4(a2),f1(f4(a2)))+~P5(f1(a2),x294131)), % 52.00/52.11 inference(scs_inference,[],[851,29382,12])). % 52.00/52.11 cnf(30058,plain, % 52.00/52.11 (P2(a5,x300581)+~P3(a2,f4(a2))+~P2(a2,f1(a2))), % 52.00/52.11 inference(scs_inference,[],[688,11129])). % 52.00/52.11 cnf(30089,plain, % 52.00/52.11 (~P3(a2,f4(a2))+~P2(a2,f1(a2))), % 52.00/52.11 inference(scs_inference,[],[30058,18642])). % 52.00/52.11 cnf(30120,plain, % 52.00/52.11 (~P2(a2,f1(a2))+P5(a2,f4(a2))+P1(a2,f4(a2))), % 52.00/52.11 inference(scs_inference,[],[30089,7])). % 52.00/52.11 cnf(30800,plain, % 52.00/52.11 (P5(a2,f1(a2))+P5(a2,f4(a2))+P1(a2,f4(a2))), % 52.00/52.11 inference(scs_inference,[],[688,30120])). % 52.00/52.11 cnf(30831,plain, % 52.00/52.11 (P5(a2,f4(a2))+P3(f1(a2),f1(f1(a2)))+P1(a2,f4(a2))), % 52.00/52.11 inference(scs_inference,[],[30800,166])). % 52.00/52.11 cnf(30862,plain, % 52.00/52.11 (~P2(a2,f4(a2))+P3(f1(a2),f1(f1(a2)))+P1(a2,f4(a2))), % 52.00/52.11 inference(scs_inference,[],[30831,8])). % 52.00/52.11 cnf(30893,plain, % 52.00/52.11 (~P3(a2,f4(a2))+P3(f1(a2),f1(f1(a2)))+P1(a2,f4(a2))), % 52.00/52.11 inference(scs_inference,[],[30862,3])). % 52.00/52.11 cnf(30924,plain, % 52.00/52.11 (~P3(a2,f4(a2))+P2(f1(a2),f1(f1(a2)))+P1(a2,f4(a2))), % 52.00/52.11 inference(scs_inference,[],[30893,3])). % 52.00/52.11 cnf(30955,plain, % 52.00/52.11 (P5(a2,f4(a2))+P1(a2,f4(a2))+P2(f1(a2),f1(f1(a2)))), % 52.00/52.11 inference(scs_inference,[],[30924,7])). % 52.00/52.11 cnf(30986,plain, % 52.00/52.11 (~P2(a2,f4(a2))+P2(f1(a2),f1(f1(a2)))+P1(a2,f4(a2))), % 52.00/52.11 inference(scs_inference,[],[30955,8])). % 52.00/52.11 cnf(31017,plain, % 52.00/52.11 (~P2(a2,f4(a2))+~P4(a2,f4(a2))+P2(f1(a2),f1(f1(a2)))), % 52.00/52.11 inference(scs_inference,[],[30986,9])). % 52.00/52.11 cnf(31048,plain, % 52.00/52.11 (P5(a2,f4(a2))+P2(f1(a2),f1(f1(a2)))+~P4(a2,f4(a2))), % 52.00/52.11 inference(scs_inference,[],[31017,688])). % 52.00/52.11 cnf(31079,plain, % 52.00/52.11 (~P3(a2,f4(a2))+P2(f1(a2),f1(f1(a2)))+~P4(a2,f4(a2))), % 52.00/52.11 inference(scs_inference,[],[31048,73])). % 52.00/52.11 cnf(31110,plain, % 52.00/52.11 (~P3(a2,f4(a2))+P2(f1(a2),f1(f1(a2)))), % 52.00/52.11 inference(scs_inference,[],[31079,5])). % 52.00/52.11 cnf(31141,plain, % 52.00/52.11 (P5(a2,f4(a2))+P5(a2,f1(a2))+P2(f1(a2),f1(f1(a2)))), % 52.00/52.11 inference(scs_inference,[],[31110,17717])). % 52.00/52.11 cnf(31172,plain, % 52.00/52.11 (P5(a2,f1(a2))+~P2(a2,f4(a2))+P2(f1(a2),f1(f1(a2)))), % 52.00/52.11 inference(scs_inference,[],[31141,8])). % 52.00/52.11 cnf(31203,plain, % 52.00/52.11 (~P2(a2,f4(a2))+~P5(f1(a2),x312031)+P2(f1(a2),f1(f1(a2)))), % 52.00/52.11 inference(scs_inference,[],[31172,6])). % 52.00/52.11 cnf(31234,plain, % 52.00/52.11 (P5(a2,f4(a2))+P2(f1(a2),f1(f1(a2)))+~P5(f1(a2),x312341)), % 52.00/52.11 inference(scs_inference,[],[31203,688])). % 52.00/52.11 cnf(31265,plain, % 52.00/52.11 (P5(a2,f4(a2))+P3(f1(a2),f1(f1(a2)))+~P5(f1(a2),x312651)), % 52.00/52.11 inference(scs_inference,[],[851,31234,12])). % 52.00/52.11 cnf(31296,plain, % 52.00/52.11 (~P2(a2,f4(a2))+P3(f1(a2),f1(f1(a2)))+~P5(f1(a2),x312961)), % 52.00/52.11 inference(scs_inference,[],[31265,8])). % 52.00/52.11 cnf(31327,plain, % 52.00/52.12 (~P2(a2,f4(a2))+~P5(f1(a2),f1(f1(a2)))+~P5(f1(a2),x313271)), % 52.00/52.12 inference(scs_inference,[],[31296,73])). % 52.00/52.12 cnf(31328,plain, % 52.00/52.12 (~P2(a2,f4(a2))+~P5(f1(a2),f1(f1(a2)))), % 52.00/52.12 inference(factoring_inference,[],[31327])). % 52.00/52.12 cnf(31451,plain, % 52.00/52.12 (P5(a2,f4(a2))+~P5(f1(a2),f1(f1(a2)))), % 52.00/52.12 inference(scs_inference,[],[688,31328])). % 52.00/52.12 cnf(31482,plain, % 52.00/52.12 (P5(a2,f4(a2))+P3(f1(a2),f1(f1(a2)))), % 52.00/52.12 inference(scs_inference,[],[31451,709])). % 52.00/52.12 cnf(32221,plain, % 52.00/52.12 (P2(a5,x322211)+~P3(a2,f4(a2))+~P3(a2,f1(a2))), % 52.00/52.12 inference(scs_inference,[],[688,11283])). % 52.00/52.12 cnf(32252,plain, % 52.00/52.12 (~P3(a2,f4(a2))+~P3(a2,f1(a2))), % 52.00/52.12 inference(scs_inference,[],[32221,18673])). % 52.00/52.12 cnf(32283,plain, % 52.00/52.12 (~P3(a2,f1(a2))+~P4(a2,f4(a2))+~P2(a2,f4(a2))), % 52.00/52.12 inference(scs_inference,[],[32252,12])). % 52.00/52.12 cnf(32468,plain, % 52.00/52.12 (P5(a2,f4(a2))+~P3(a2,f1(a2))+~P4(a2,f4(a2))), % 52.00/52.12 inference(scs_inference,[],[688,32283])). % 52.00/52.12 cnf(32499,plain, % 52.00/52.12 (~P3(a2,f1(a2))+~P5(f4(a2),x324991)+~P4(a2,f4(a2))), % 52.00/52.12 inference(scs_inference,[],[32468,6])). % 52.00/52.12 cnf(32530,plain, % 52.00/52.12 (~P2(a2,f1(a2))+~P4(a2,f4(a2))+~P5(f4(a2),x325301)), % 52.00/52.12 inference(scs_inference,[],[32499,852])). % 52.00/52.12 cnf(32561,plain, % 52.00/52.12 (~P2(a2,f1(a2))+P5(a2,f1(a2))+~P5(f4(a2),x325611)), % 52.00/52.12 inference(scs_inference,[],[32530,20465])). % 52.00/52.12 cnf(32592,plain, % 52.00/52.12 (P5(a2,f1(a2))+~P3(a2,f1(a2))+~P5(f4(a2),x325921)), % 52.00/52.12 inference(scs_inference,[],[32561,3])). % 52.00/52.12 cnf(32623,plain, % 52.00/52.12 (~P3(a2,f1(a2))+~P2(a2,f1(a2))+~P5(f4(a2),x326231)), % 52.00/52.12 inference(scs_inference,[],[32592,8])). % 52.00/52.12 cnf(32654,plain, % 52.00/52.12 (~P2(a2,f1(a2))+~P5(f4(a2),x326541)), % 52.00/52.12 inference(scs_inference,[],[32623,852])). % 52.00/52.12 cnf(32808,plain, % 52.00/52.12 (P5(a2,f1(a2))+~P5(f4(a2),x328081)), % 52.00/52.12 inference(scs_inference,[],[688,32654])). % 52.00/52.12 cnf(32839,plain, % 52.00/52.12 (~P3(a2,f1(a2))+~P5(f4(a2),x328391)), % 52.00/52.12 inference(scs_inference,[],[32808,73])). % 52.00/52.12 cnf(35991,plain, % 52.00/52.12 (P5(a5,a7)+~P3(a2,f1(a2))+~P3(f4(a2),x359911)), % 52.00/52.12 inference(scs_inference,[],[32839,33])). % 52.00/52.12 cnf(36176,plain, % 52.00/52.12 (~P3(a2,f1(a2))+P5(a2,a5)+~P3(f4(a2),x361761)), % 52.00/52.12 inference(scs_inference,[],[32839,29])). % 52.00/52.12 cnf(36721,plain, % 52.00/52.12 (P3(f1(a2),f1(f1(a2)))+P5(a5,a7)+~P3(f4(a2),x367211)), % 52.00/52.12 inference(scs_inference,[],[713,35991])). % 52.00/52.12 cnf(36752,plain, % 52.00/52.12 (P5(a5,a7)+P2(f1(a2),f1(f1(a2)))+~P3(f4(a2),x367521)), % 52.00/52.12 inference(scs_inference,[],[36721,3])). % 52.00/52.12 cnf(36783,plain, % 52.00/52.12 (P4(a5,a7)+P2(f1(a2),f1(f1(a2)))+~P3(f4(a2),x367831)), % 52.00/52.12 inference(scs_inference,[],[36752,4])). % 52.00/52.12 cnf(36814,plain, % 52.00/52.12 (P3(f1(a2),f1(f1(a2)))+P4(a5,a7)+~P3(f4(a2),x368141)), % 52.00/52.12 inference(scs_inference,[],[851,36783,12])). % 52.00/52.12 cnf(36845,plain, % 52.00/52.12 (P3(f1(a2),f1(f1(a2)))+P4(a5,a7)), % 52.00/52.12 inference(scs_inference,[],[36814,27903])). % 52.00/52.12 cnf(36999,plain, % 52.00/52.12 (P3(f1(a2),f1(f1(a2)))+P3(a5,a7)+~P2(a5,a7)), % 52.00/52.12 inference(scs_inference,[],[36845,12])). % 52.11/52.12 cnf(37030,plain, % 52.11/52.12 (~P2(a5,a7)+P2(f1(a2),f1(f1(a2)))+P3(a5,a7)), % 52.11/52.12 inference(scs_inference,[],[36999,3])). % 52.11/52.12 cnf(37061,plain, % 52.11/52.12 (P5(a5,a7)+P2(f1(a2),f1(f1(a2)))+P3(a5,a7)), % 52.11/52.12 inference(scs_inference,[],[37030,688])). % 52.11/52.12 cnf(37092,plain, % 52.11/52.12 (P2(f1(a2),f1(f1(a2)))+~P5(a2,a5)+P3(a5,a7)), % 52.11/52.12 inference(scs_inference,[],[37061,6])). % 52.11/52.12 cnf(37673,plain, % 52.11/52.12 (P3(f1(a2),f1(f1(a2)))+P5(a2,a5)+~P3(f4(a2),x376731)), % 52.11/52.12 inference(scs_inference,[],[713,36176])). % 52.11/52.12 cnf(37704,plain, % 52.11/52.12 (P5(a2,a5)+P2(f1(a2),f1(f1(a2)))+~P3(f4(a2),x377041)), % 52.11/52.12 inference(scs_inference,[],[37673,3])). % 52.11/52.12 cnf(37735,plain, % 52.11/52.12 (P2(f1(a2),f1(f1(a2)))+P3(a5,a7)+~P3(f4(a2),x377351)), % 52.11/52.12 inference(scs_inference,[],[37704,37092])). % 52.11/52.12 cnf(37766,plain, % 52.11/52.12 (P3(f1(a2),f1(f1(a2)))+P3(a5,a7)+~P3(f4(a2),x377661)), % 52.11/52.12 inference(scs_inference,[],[851,37735,12])). % 52.11/52.12 cnf(37797,plain, % 52.11/52.12 (P3(f1(a2),f1(f1(a2)))+P3(a5,a7)), % 52.11/52.12 inference(scs_inference,[],[37766,27903])). % 52.11/52.12 cnf(37828,plain, % 52.11/52.12 (P2(f1(a2),f1(f1(a2)))+P3(a5,a7)), % 52.11/52.12 inference(scs_inference,[],[37797,3])). % 52.11/52.12 cnf(37859,plain, % 52.11/52.12 (~P5(a5,a7)+P2(f1(a2),f1(f1(a2)))), % 52.11/52.12 inference(scs_inference,[],[37828,73])). % 52.11/52.12 cnf(38196,plain, % 52.11/52.12 (~P3(a2,f1(a2))+P2(f1(a2),f1(f1(a2)))+~P3(f4(a2),x381961)), % 52.11/52.12 inference(scs_inference,[],[37859,35991])). % 52.11/52.12 cnf(38227,plain, % 52.11/52.12 (P5(a2,f1(a2))+P2(f1(a2),f1(f1(a2)))+~P3(f4(a2),x382271)), % 52.11/52.12 inference(scs_inference,[],[38196,709])). % 52.11/52.12 cnf(38258,plain, % 52.11/52.12 (~P5(f1(a2),x382581)+P2(f1(a2),f1(f1(a2)))+~P3(f4(a2),x382582)), % 52.11/52.12 inference(scs_inference,[],[38227,6])). % 52.11/52.12 cnf(38289,plain, % 52.11/52.12 (P3(f1(a2),f1(f1(a2)))+~P5(f1(a2),x382891)+~P3(f4(a2),x382892)), % 52.11/52.12 inference(scs_inference,[],[851,38258,12])). % 52.11/52.12 cnf(38320,plain, % 52.11/52.12 (~P5(f1(a2),f1(f1(a2)))+~P5(f1(a2),x383201)+~P3(f4(a2),x383202)), % 52.11/52.12 inference(scs_inference,[],[38289,73])). % 52.11/52.12 cnf(38321,plain, % 52.11/52.12 (~P5(f1(a2),f1(f1(a2)))+~P3(f4(a2),x383211)), % 52.11/52.12 inference(factoring_inference,[],[38320])). % 52.11/52.12 cnf(38352,plain, % 52.11/52.12 (P2(f1(a2),f1(f1(a2)))+~P3(f4(a2),x383521)), % 52.11/52.12 inference(scs_inference,[],[38321,688])). % 52.11/52.12 cnf(38383,plain, % 52.11/52.12 (P3(f1(a2),f1(f1(a2)))+~P3(f4(a2),x383831)), % 52.11/52.12 inference(scs_inference,[],[851,38352,12])). % 52.11/52.12 cnf(38414,plain, % 52.11/52.12 (P3(f1(a2),f1(f1(a2)))+~P5(a2,f4(a2))), % 52.11/52.12 inference(scs_inference,[],[38383,166])). % 52.11/52.12 cnf(38445,plain, % 52.11/52.12 (~P5(a2,f4(a2))+~P5(f1(a2),f1(f1(a2)))), % 52.11/52.12 inference(scs_inference,[],[38414,73])). % 52.11/52.12 cnf(38476,plain, % 52.11/52.12 (~P5(f1(a2),f1(f1(a2)))+P3(f1(a2),f1(f1(a2)))), % 52.11/52.12 inference(scs_inference,[],[38445,31482])). % 52.11/52.12 cnf(38507,plain, % 52.11/52.12 (P3(f1(a2),f1(f1(a2)))+P2(f1(a2),f1(f1(a2)))), % 52.11/52.12 inference(scs_inference,[],[38476,688])). % 52.11/52.12 cnf(38538,plain, % 52.11/52.12 (~P5(f1(a2),f1(f1(a2)))+P2(f1(a2),f1(f1(a2)))), % 52.11/52.12 inference(scs_inference,[],[38507,73])). % 52.11/52.12 cnf(38569,plain, % 52.11/52.12 (P2(f1(a2),f1(f1(a2)))), % 52.11/52.12 inference(scs_inference,[],[38538,688])). % 52.11/52.12 cnf(38570,plain, % 52.11/52.12 (P3(f1(a2),f1(f1(a2)))), % 52.11/52.12 inference(scs_inference,[],[38569,852])). % 52.11/52.12 cnf(38577,plain, % 52.11/52.12 (P5(a2,a5)+P5(x385771,f4(x385771))+~P3(x385771,x385772)+P5(f1(a2),f6(f1(a2)))), % 52.11/52.12 inference(scs_inference,[],[38570,32])). % 52.11/52.12 cnf(39073,plain, % 52.11/52.12 (~P3(a2,f1(a2))+P5(a2,a5)+~P5(f1(a2),x390731)), % 52.11/52.12 inference(scs_inference,[],[29413,36176])). % 52.11/52.12 cnf(39119,plain, % 52.11/52.12 (P5(a2,a5)+P5(a2,f1(a2))+~P5(f1(a2),x391191)), % 52.11/52.12 inference(scs_inference,[],[39073,709])). % 52.11/52.12 cnf(39165,plain, % 52.11/52.12 (P5(a2,f1(a2))+P4(a2,a5)+~P5(f1(a2),x391651)), % 52.11/52.12 inference(scs_inference,[],[39119,4])). % 52.11/52.12 cnf(39211,plain, % 52.11/52.12 (P4(a2,a5)+~P5(f1(a2),x392111)+~P5(f1(a2),x392112)), % 52.11/52.12 inference(scs_inference,[],[39165,6])). % 52.11/52.12 cnf(39257,plain, % 52.11/52.12 (~P1(a2,a5)+~P5(f1(a2),x392571)+~P5(f1(a2),x392572)), % 52.11/52.12 inference(scs_inference,[],[39211,9])). % 52.11/52.12 cnf(39348,plain, % 52.11/52.12 (P3(f4(a2),f1(f4(a2)))+P5(a2,a5)+P5(f1(a2),f6(f1(a2)))), % 52.11/52.12 inference(scs_inference,[],[38570,29413,38577])). % 52.11/52.12 cnf(39394,plain, % 52.11/52.12 (~P3(a2,f1(a2))+P5(a2,a5)+P5(f1(a2),f6(f1(a2)))), % 52.11/52.12 inference(scs_inference,[],[39348,36176])). % 52.11/52.12 cnf(39440,plain, % 52.11/52.12 (P5(a2,a5)+P5(a2,f1(a2))+P5(f1(a2),f6(f1(a2)))), % 52.11/52.12 inference(scs_inference,[],[39394,709])). % 52.11/52.12 cnf(39486,plain, % 52.11/52.12 (P5(a2,f1(a2))+P4(a2,a5)+P5(f1(a2),f6(f1(a2)))), % 52.11/52.12 inference(scs_inference,[],[39440,4])). % 52.11/52.12 cnf(39532,plain, % 52.11/52.12 (P4(a2,a5)+~P2(a2,f1(a2))+P5(f1(a2),f6(f1(a2)))), % 52.11/52.12 inference(scs_inference,[],[39486,8])). % 52.11/52.12 cnf(39578,plain, % 52.11/52.12 (~P2(a2,f1(a2))+~P1(a2,a5)+P5(f1(a2),f6(f1(a2)))), % 52.11/52.12 inference(scs_inference,[],[39532,9])). % 52.11/52.12 cnf(39624,plain, % 52.11/52.12 (~P1(a2,a5)+~P3(a2,f1(a2))+P5(f1(a2),f6(f1(a2)))), % 52.11/52.12 inference(scs_inference,[],[39578,3])). % 52.11/52.12 cnf(39670,plain, % 52.11/52.12 (~P3(a2,f1(a2))+~P1(a2,a5)), % 52.11/52.12 inference(scs_inference,[],[39624,39257])). % 52.11/52.12 cnf(39716,plain, % 52.11/52.12 (~P1(a2,a5)+~P5(f1(a2),x397161)), % 52.11/52.12 inference(scs_inference,[],[39670,711])). % 52.11/52.12 cnf(41596,plain, % 52.11/52.12 (~P1(a2,a5)+P5(a2,a5)+P5(f1(a2),f6(f1(a2)))), % 52.11/52.12 inference(scs_inference,[],[38570,39716,38577])). % 52.11/52.12 cnf(41642,plain, % 52.11/52.12 (P3(a2,a5)+P5(a2,a5)+P5(f1(a2),f6(f1(a2)))), % 52.11/52.12 inference(scs_inference,[],[41596,7])). % 52.11/52.12 cnf(41688,plain, % 52.11/52.12 (P4(a2,a5)+P3(a2,a5)+P5(f1(a2),f6(f1(a2)))), % 52.11/52.12 inference(scs_inference,[],[41642,4])). % 52.11/52.12 cnf(41734,plain, % 52.11/52.12 (~P1(a2,a5)+P3(a2,a5)+P5(f1(a2),f6(f1(a2)))), % 52.11/52.12 inference(scs_inference,[],[41688,9])). % 52.11/52.12 cnf(41780,plain, % 52.11/52.12 (~P1(a2,a5)+P5(f1(a2),f6(f1(a2)))), % 52.11/52.12 inference(scs_inference,[],[41734,135])). % 52.11/52.12 cnf(42193,plain, % 52.11/52.12 (~P1(a2,a5)), % 52.11/52.12 inference(scs_inference,[],[39716,41780])). % 52.11/52.12 cnf(42200,plain, % 52.11/52.12 (P4(a2,a5)), % 52.11/52.12 inference(scs_inference,[],[42193,11,3650,3681,1839])). % 52.11/52.12 cnf(42204,plain, % 52.11/52.12 (P3(a2,a5)+~P2(a2,a5)), % 52.11/52.12 inference(scs_inference,[],[42200,12])). % 52.11/52.12 cnf(42212,plain, % 52.11/52.12 (P3(a2,a5)+P5(a2,a5)), % 52.11/52.12 inference(scs_inference,[],[42193,7])). % 52.11/52.12 cnf(42248,plain, % 52.11/52.12 (~P5(a5,x422481)+P3(a2,a5)), % 52.11/52.12 inference(scs_inference,[],[42204,3650])). % 52.11/52.12 cnf(42340,plain, % 52.11/52.12 (P5(a2,a5)+P5(a2,f4(a2))+~P5(a5,x423401)), % 52.11/52.12 inference(scs_inference,[],[42193,1,42248,20])). % 52.11/52.12 cnf(42432,plain, % 52.11/52.12 (P5(a2,f4(a2))+~P5(a5,x424321)+~P5(a5,x424322)), % 52.11/52.12 inference(scs_inference,[],[42340,6])). % 52.11/52.12 cnf(45048,plain, % 52.11/52.12 (~P2(a2,a5)+P5(a5,a7)+P5(a2,f4(a2))), % 52.11/52.12 inference(scs_inference,[],[42193,1,42204,21])). % 52.11/52.12 cnf(45094,plain, % 52.11/52.12 (P5(a5,a7)+P5(a2,f4(a2))+~P3(a2,a5)), % 52.11/52.12 inference(scs_inference,[],[45048,3])). % 52.11/52.12 cnf(45140,plain, % 52.11/52.12 (~P3(a2,a5)+P5(a2,f4(a2))), % 52.11/52.12 inference(scs_inference,[],[45094,42432])). % 52.11/52.12 cnf(45186,plain, % 52.11/52.12 (P5(a2,f4(a2))+P5(a2,a5)), % 52.11/52.12 inference(scs_inference,[],[45140,42212])). % 52.11/52.12 cnf(45232,plain, % 52.11/52.12 (P5(a2,a5)+~P5(f4(a2),x452321)), % 52.11/52.12 inference(scs_inference,[],[45186,6])). % 52.11/52.12 cnf(45966,plain, % 52.11/52.12 (~P2(a2,a5)+P5(a2,f4(a2))), % 52.11/52.12 inference(scs_inference,[],[42204,45140])). % 52.11/52.12 cnf(50112,plain, % 52.11/52.12 (~P3(f4(a2),x501121)+P5(a2,a5)+~P3(a2,a5)), % 52.11/52.12 inference(scs_inference,[],[1,42193,45232,20])). % 52.11/52.12 cnf(50113,plain, % 52.11/52.12 (P5(a2,a5)+~P2(a2,a5)+~P3(f4(a2),x501131)), % 52.11/52.12 inference(scs_inference,[],[50112,42204])). % 52.11/52.12 cnf(50114,plain, % 52.11/52.12 (P5(a2,a5)+~P3(f4(a2),x501141)), % 52.11/52.12 inference(scs_inference,[],[50113,688])). % 52.11/52.12 cnf(50115,plain, % 52.11/52.12 (~P5(a5,x501151)+~P3(f4(a2),x501152)), % 52.11/52.12 inference(scs_inference,[],[50114,6])). % 52.11/52.12 cnf(50116,plain, % 52.11/52.12 (~P5(a2,f4(a2))+~P5(a5,x501161)), % 52.11/52.12 inference(scs_inference,[],[50115,166])). % 52.11/52.12 cnf(50147,plain, % 52.11/52.12 (~P2(a2,a5)+~P5(a5,x501471)), % 52.11/52.12 inference(scs_inference,[],[45966,50116])). % 52.11/52.12 cnf(50148,plain, % 52.11/52.12 (~P3(a2,a5)+~P5(a5,x501481)), % 52.11/52.12 inference(scs_inference,[],[50147,3])). % 52.11/52.12 cnf(50150,plain, % 52.11/52.12 (P5(a2,a5)+~P5(a5,x501501)), % 52.11/52.12 inference(scs_inference,[],[50148,42212])). % 52.11/52.12 cnf(50153,plain, % 52.11/52.12 (~P5(a5,x501531)+~P5(a5,x501532)), % 52.11/52.12 inference(scs_inference,[],[50150,6])). % 52.11/52.12 cnf(50154,plain, % 52.11/52.12 (P3(a5,f1(a5))), % 52.11/52.12 inference(scs_inference,[],[50153,709])). % 52.11/52.12 cnf(50170,plain, % 52.11/52.12 (P5(a5,f4(a5))+P5(a5,a7)+~P3(a2,a5)), % 52.11/52.12 inference(scs_inference,[],[1,50154,42193,21])). % 52.11/52.12 cnf(50174,plain, % 52.11/52.12 (P5(a5,f6(a5))+P5(a5,a7)+P5(a5,f4(a5))), % 52.11/52.12 inference(scs_inference,[],[1,50154,42193,23])). % 52.11/52.12 cnf(50176,plain, % 52.11/52.12 (P5(a5,a7)+~P2(a2,a5)+P5(a5,f4(a5))), % 52.11/52.12 inference(scs_inference,[],[50170,42204])). % 52.11/52.12 cnf(50179,plain, % 52.11/52.12 (P5(a5,a7)+P5(a2,a5)+P5(a5,f4(a5))), % 52.11/52.12 inference(scs_inference,[],[50176,688])). % 52.11/52.12 cnf(50184,plain, % 52.11/52.12 (P5(a2,a5)+P5(a5,f4(a5))), % 52.11/52.12 inference(scs_inference,[],[50179,50153])). % 52.11/52.12 cnf(50186,plain, % 52.11/52.12 (~P2(a2,a5)+P5(a5,f4(a5))), % 52.11/52.12 inference(scs_inference,[],[50184,8])). % 52.11/52.12 cnf(50192,plain, % 52.11/52.12 (P2(a5,x501921)+P5(a5,f4(a5))), % 52.11/52.12 inference(scs_inference,[],[50186,26143])). % 52.11/52.12 cnf(50193,plain, % 52.11/52.12 (P2(a5,x501931)), % 52.11/52.12 inference(scs_inference,[],[50192,50153])). % 52.11/52.12 cnf(50202,plain, % 52.11/52.12 (~P5(a5,x502021)), % 52.11/52.12 inference(scs_inference,[],[50193,8])). % 52.11/52.12 cnf(50249,plain, % 52.11/52.12 (~P3(a2,a5)+P5(a5,f4(a5))), % 52.11/52.12 inference(scs_inference,[],[50202,50170])). % 52.11/52.12 cnf(50250,plain, % 52.11/52.12 (P5(a5,a7)+P5(a5,f6(a5))), % 52.11/52.12 inference(scs_inference,[],[50202,50174])). % 52.11/52.12 cnf(50262,plain, % 52.11/52.12 (~P5(a5,x502621)), % 52.11/52.12 inference(rename_variables,[],[50202])). % 52.11/52.12 cnf(50265,plain, % 52.11/52.12 ($false), % 52.11/52.12 inference(scs_inference,[],[50202,50262,50193,50249,50250,8]), % 52.11/52.12 ['proof']). % 52.11/52.12 % SZS output end Proof % 52.11/52.12 % Total time : 51.330000 s %------------------------------------------------------------------------------