%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : CSR039+2 : TPTP v8.1.0. Released v3.4.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n021.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 : Fri Jul 15 23:24:30 EDT 2022 % Result : Theorem 76.13s 76.33s % Output : Refutation 76.13s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : CSR039+2 : TPTP v8.1.0. Released v3.4.0. % 0.03/0.12 % Command : run_spass %d %s % 0.12/0.33 % Computer : n021.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 : 600 % 0.12/0.33 % DateTime : Fri Jun 10 05:44:08 EDT 2022 % 0.12/0.33 % CPUTime : % 76.13/76.33 % 76.13/76.33 SPASS V 3.9 % 76.13/76.33 SPASS beiseite: Proof found. % 76.13/76.33 % SZS status Theorem % 76.13/76.33 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 76.13/76.33 SPASS derived 75963 clauses, backtracked 0 clauses, performed 0 splits and kept 61792 clauses. % 76.13/76.33 SPASS allocated 146563 KBytes. % 76.13/76.33 SPASS spent 0:1:15.93 on the problem. % 76.13/76.33 0:00:00.04 for the input. % 76.13/76.33 0:00:00.22 for the FLOTTER CNF translation. % 76.13/76.33 0:00:01.13 for inferences. % 76.13/76.33 0:00:00.00 for the backtracking. % 76.13/76.33 0:01:09.72 for the reduction. % 76.13/76.33 % 76.13/76.33 % 76.13/76.33 Here is a proof with depth 3, length 85 : % 76.13/76.33 % SZS output start Refutation % 76.13/76.33 28[0:Inp] || -> genls(c_tptpcol_7_93186,c_tptpcol_6_92162)*l. % 76.13/76.33 32[0:Inp] || -> genls(c_tptpcol_5_16388,c_tptpcol_4_16387)*l. % 76.13/76.33 41[0:Inp] || -> genls(c_tptpcol_3_81921,c_tptpcol_2_65537)*l. % 76.13/76.33 42[0:Inp] || -> genls(c_tptpcol_10_18567,c_tptpcol_9_18439)*l. % 76.13/76.33 58[0:Inp] || -> genls(c_tptpcol_12_93765,c_tptpcol_11_93764)*l. % 76.13/76.33 61[0:Inp] || -> genls(c_tptpcol_13_93766,c_tptpcol_12_93765)*r. % 76.13/76.33 73[0:Inp] || -> genls(c_tptpcol_12_18663,c_tptpcol_11_18631)*l. % 76.13/76.33 91[0:Inp] || -> genls(c_tptpcol_2_2,c_tptpcol_1_1)*l. % 76.13/76.33 95[0:Inp] || -> disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536)*. % 76.13/76.33 105[0:Inp] || -> genls(c_tptpcol_11_18631,c_tptpcol_10_18567)*r. % 76.13/76.33 108[0:Inp] || -> genls(c_tptpcol_15_93775,c_tptpcol_14_93774)*l. % 76.13/76.33 112[0:Inp] || -> genls(c_tptpcol_14_93774,c_tptpcol_13_93766)*r. % 76.13/76.33 119[0:Inp] || -> genls(c_tptpcol_13_18664,c_tptpcol_12_18663)*l. % 76.13/76.33 140[0:Inp] || -> genls(c_tptpcol_9_18439,c_tptpcol_8_18438)*l. % 76.13/76.33 157[0:Inp] || -> genls(c_tptpcol_4_16387,c_tptpcol_3_16386)*l. % 76.13/76.33 184[0:Inp] || -> genls(c_tptpcol_8_93698,c_tptpcol_7_93186)*r. % 76.13/76.33 185[0:Inp] || -> genls(c_tptpcol_2_65537,c_tptpcol_1_65536)*l. % 76.13/76.33 187[0:Inp] || -> genls(c_tptpcol_6_18436,c_tptpcol_5_16388)*r. % 76.13/76.33 188[0:Inp] || -> genls(c_tptpcol_8_18438,c_tptpcol_7_18437)*l. % 76.13/76.33 197[0:Inp] || -> genls(c_tptpcol_9_93699,c_tptpcol_8_93698)*r. % 76.13/76.33 198[0:Inp] || -> genls(c_tptpcol_11_93764,c_tptpcol_10_93700)*l. % 76.13/76.33 200[0:Inp] || -> genls(c_tptpcol_4_90113,c_tptpcol_3_81921)*r. % 76.13/76.33 202[0:Inp] || -> genls(c_tptpcol_10_93700,c_tptpcol_9_93699)*r. % 76.13/76.33 205[0:Inp] || -> genls(c_tptpcol_3_16386,c_tptpcol_2_2)*r. % 76.13/76.33 221[0:Inp] || -> genls(c_tptpcol_6_92162,c_tptpcol_5_90114)*l. % 76.13/76.33 248[0:Inp] || -> genls(c_tptpcol_5_90114,c_tptpcol_4_90113)*r. % 76.13/76.33 251[0:Inp] || -> genls(c_tptpcol_7_18437,c_tptpcol_6_18436)*r. % 76.13/76.33 267[0:Inp] || disjointwith(c_tptpcol_15_93775,c_tptpcol_13_18664)* -> . % 76.13/76.33 1053[0:Inp] || disjointwith(u,v)*+ -> disjointwith(v,u)*. % 76.13/76.33 1124[0:Inp] || genls(u,v)*+ disjointwith(w,v)* -> disjointwith(w,u)*. % 76.13/76.33 1125[0:Inp] || genls(u,v)*+ disjointwith(v,w)* -> disjointwith(u,w)*. % 76.13/76.33 2748[0:Res:95.0,1053.0] || -> disjointwith(c_tptpcol_1_65536,c_tptpcol_1_1)*. % 76.13/76.33 6661[0:Res:248.0,1125.0] || disjointwith(c_tptpcol_4_90113,u)* -> disjointwith(c_tptpcol_5_90114,u). % 76.13/76.33 6680[0:Res:221.0,1125.0] || disjointwith(c_tptpcol_5_90114,u) -> disjointwith(c_tptpcol_6_92162,u)*. % 76.13/76.33 6694[0:Res:202.0,1125.0] || disjointwith(c_tptpcol_9_93699,u)* -> disjointwith(c_tptpcol_10_93700,u). % 76.13/76.33 6695[0:Res:200.0,1125.0] || disjointwith(c_tptpcol_3_81921,u)* -> disjointwith(c_tptpcol_4_90113,u). % 76.13/76.33 6697[0:Res:198.0,1125.0] || disjointwith(c_tptpcol_10_93700,u) -> disjointwith(c_tptpcol_11_93764,u)*. % 76.13/76.33 6698[0:Res:197.0,1125.0] || disjointwith(c_tptpcol_8_93698,u)* -> disjointwith(c_tptpcol_9_93699,u). % 76.13/76.33 6704[0:Res:185.0,1125.0] || disjointwith(c_tptpcol_1_65536,u) -> disjointwith(c_tptpcol_2_65537,u)*. % 76.13/76.33 6706[0:Res:184.0,1125.0] || disjointwith(c_tptpcol_7_93186,u)* -> disjointwith(c_tptpcol_8_93698,u). % 76.13/76.33 6712[0:Res:28.0,1125.0] || disjointwith(c_tptpcol_6_92162,u) -> disjointwith(c_tptpcol_7_93186,u)*. % 76.13/76.33 6717[0:Res:41.0,1125.0] || disjointwith(c_tptpcol_2_65537,u) -> disjointwith(c_tptpcol_3_81921,u)*. % 76.13/76.33 6749[0:Res:112.0,1125.0] || disjointwith(c_tptpcol_13_93766,u)* -> disjointwith(c_tptpcol_14_93774,u). % 76.13/76.33 6753[0:Res:108.0,1125.0] || disjointwith(c_tptpcol_14_93774,u) -> disjointwith(c_tptpcol_15_93775,u)*. % 76.13/76.33 6776[0:Res:61.0,1125.0] || disjointwith(c_tptpcol_12_93765,u)* -> disjointwith(c_tptpcol_13_93766,u). % 76.13/76.33 6779[0:Res:58.0,1125.0] || disjointwith(c_tptpcol_11_93764,u) -> disjointwith(c_tptpcol_12_93765,u)*. % 76.13/76.33 6954[0:Res:251.0,1124.0] || disjointwith(u,c_tptpcol_6_18436)* -> disjointwith(u,c_tptpcol_7_18437). % 76.13/76.33 6986[0:Res:205.0,1124.0] || disjointwith(u,c_tptpcol_2_2)* -> disjointwith(u,c_tptpcol_3_16386). % 76.13/76.33 6997[0:Res:188.0,1124.0] || disjointwith(u,c_tptpcol_7_18437) -> disjointwith(u,c_tptpcol_8_18438)*. % 76.13/76.33 6998[0:Res:187.0,1124.0] || disjointwith(u,c_tptpcol_5_16388)* -> disjointwith(u,c_tptpcol_6_18436). % 76.13/76.33 7016[0:Res:157.0,1124.0] || disjointwith(u,c_tptpcol_3_16386) -> disjointwith(u,c_tptpcol_4_16387)*. % 76.13/76.33 7025[0:Res:140.0,1124.0] || disjointwith(u,c_tptpcol_8_18438) -> disjointwith(u,c_tptpcol_9_18439)*. % 76.13/76.33 7039[0:Res:119.0,1124.0] || disjointwith(u,c_tptpcol_12_18663) -> disjointwith(u,c_tptpcol_13_18664)*. % 76.13/76.33 7050[0:Res:105.0,1124.0] || disjointwith(u,c_tptpcol_10_18567)* -> disjointwith(u,c_tptpcol_11_18631). % 76.13/76.33 7057[0:Res:91.0,1124.0] || disjointwith(u,c_tptpcol_1_1) -> disjointwith(u,c_tptpcol_2_2)*. % 76.13/76.33 7065[0:Res:73.0,1124.0] || disjointwith(u,c_tptpcol_11_18631) -> disjointwith(u,c_tptpcol_12_18663)*. % 76.13/76.33 7080[0:Res:42.0,1124.0] || disjointwith(u,c_tptpcol_9_18439) -> disjointwith(u,c_tptpcol_10_18567)*. % 76.13/76.33 7085[0:Res:32.0,1124.0] || disjointwith(u,c_tptpcol_4_16387) -> disjointwith(u,c_tptpcol_5_16388)*. % 76.13/76.33 24190[0:Res:6753.1,267.0] || disjointwith(c_tptpcol_14_93774,c_tptpcol_13_18664)* -> . % 76.13/76.33 25138[0:Res:6712.1,6954.0] || disjointwith(c_tptpcol_6_92162,c_tptpcol_6_18436) -> disjointwith(c_tptpcol_7_93186,c_tptpcol_7_18437)*. % 76.13/76.33 27627[0:Res:6704.1,6986.0] || disjointwith(c_tptpcol_1_65536,c_tptpcol_2_2) -> disjointwith(c_tptpcol_2_65537,c_tptpcol_3_16386)*. % 76.13/76.33 28492[0:Res:6997.1,6706.0] || disjointwith(c_tptpcol_7_93186,c_tptpcol_7_18437)* -> disjointwith(c_tptpcol_8_93698,c_tptpcol_8_18438). % 76.13/76.33 28543[0:Res:6680.1,6998.0] || disjointwith(c_tptpcol_5_90114,c_tptpcol_5_16388) -> disjointwith(c_tptpcol_6_92162,c_tptpcol_6_18436)*. % 76.13/76.33 29943[0:Res:7016.1,6695.0] || disjointwith(c_tptpcol_3_81921,c_tptpcol_3_16386)* -> disjointwith(c_tptpcol_4_90113,c_tptpcol_4_16387). % 76.13/76.33 30632[0:Res:7025.1,6698.0] || disjointwith(c_tptpcol_8_93698,c_tptpcol_8_18438)* -> disjointwith(c_tptpcol_9_93699,c_tptpcol_9_18439). % 76.13/76.33 31753[0:Res:7039.1,6749.0] || disjointwith(c_tptpcol_13_93766,c_tptpcol_12_18663)* -> disjointwith(c_tptpcol_14_93774,c_tptpcol_13_18664). % 76.13/76.33 31761[0:MRR:31753.1,24190.0] || disjointwith(c_tptpcol_13_93766,c_tptpcol_12_18663)* -> . % 76.13/76.33 32558[0:Res:6697.1,7050.0] || disjointwith(c_tptpcol_10_93700,c_tptpcol_10_18567) -> disjointwith(c_tptpcol_11_93764,c_tptpcol_11_18631)*. % 76.13/76.33 33675[0:Res:7065.1,6776.0] || disjointwith(c_tptpcol_12_93765,c_tptpcol_11_18631)* -> disjointwith(c_tptpcol_13_93766,c_tptpcol_12_18663). % 76.13/76.33 33676[0:MRR:33675.1,31761.0] || disjointwith(c_tptpcol_12_93765,c_tptpcol_11_18631)* -> . % 76.13/76.33 34730[0:Res:7080.1,6694.0] || disjointwith(c_tptpcol_9_93699,c_tptpcol_9_18439)* -> disjointwith(c_tptpcol_10_93700,c_tptpcol_10_18567). % 76.13/76.33 35071[0:Res:7085.1,6661.0] || disjointwith(c_tptpcol_4_90113,c_tptpcol_4_16387)* -> disjointwith(c_tptpcol_5_90114,c_tptpcol_5_16388). % 76.13/76.33 76333[0:Res:6779.1,33676.0] || disjointwith(c_tptpcol_11_93764,c_tptpcol_11_18631)* -> . % 76.13/76.33 76334[0:MRR:32558.1,76333.0] || disjointwith(c_tptpcol_10_93700,c_tptpcol_10_18567)* -> . % 76.13/76.33 76335[0:MRR:34730.1,76334.0] || disjointwith(c_tptpcol_9_93699,c_tptpcol_9_18439)* -> . % 76.13/76.33 76336[0:MRR:30632.1,76335.0] || disjointwith(c_tptpcol_8_93698,c_tptpcol_8_18438)* -> . % 76.13/76.33 76337[0:MRR:28492.1,76336.0] || disjointwith(c_tptpcol_7_93186,c_tptpcol_7_18437)* -> . % 76.13/76.33 76338[0:MRR:25138.1,76337.0] || disjointwith(c_tptpcol_6_92162,c_tptpcol_6_18436)* -> . % 76.13/76.33 76339[0:MRR:28543.1,76338.0] || disjointwith(c_tptpcol_5_90114,c_tptpcol_5_16388)* -> . % 76.13/76.33 76340[0:MRR:35071.1,76339.0] || disjointwith(c_tptpcol_4_90113,c_tptpcol_4_16387)* -> . % 76.13/76.33 76341[0:MRR:29943.1,76340.0] || disjointwith(c_tptpcol_3_81921,c_tptpcol_3_16386)* -> . % 76.13/76.33 76908[0:Res:6717.1,76341.0] || disjointwith(c_tptpcol_2_65537,c_tptpcol_3_16386)* -> . % 76.13/76.33 76909[0:MRR:27627.1,76908.0] || disjointwith(c_tptpcol_1_65536,c_tptpcol_2_2)* -> . % 76.13/76.33 77816[0:Res:7057.1,76909.0] || disjointwith(c_tptpcol_1_65536,c_tptpcol_1_1)* -> . % 76.13/76.33 77818[0:MRR:77816.0,2748.0] || -> . % 76.13/76.33 % SZS output end Refutation % 76.13/76.33 Formulae used in the proof : ax1_14 ax1_23 ax1_41 ax1_43 ax1_72 ax1_78 ax1_109 ax1_145 ax1_152 ax1_175 ax1_182 ax1_191 ax1_208 ax1_255 ax1_285 ax1_345 ax1_348 ax1_351 ax1_353 ax1_370 ax1_372 ax1_376 ax1_379 ax1_385 ax1_417 ax1_476 ax1_483 query89 ax1_1120 ax1_1121 ax1_1122 % 78.08/78.28 %------------------------------------------------------------------------------