%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : CSR064+3 : TPTP v8.1.0. Released v3.4.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n007.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:54 EDT 2022 % Result : Theorem 88.55s 88.75s % Output : Refutation 88.55s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : CSR064+3 : TPTP v8.1.0. Released v3.4.0. % 0.03/0.12 % Command : run_spass %d %s % 0.12/0.33 % Computer : n007.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 : Sat Jun 11 16:29:37 EDT 2022 % 0.12/0.33 % CPUTime : % 88.55/88.75 % 88.55/88.75 SPASS V 3.9 % 88.55/88.75 SPASS beiseite: Proof found. % 88.55/88.75 % SZS status Theorem % 88.55/88.75 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 88.55/88.75 SPASS derived 6296 clauses, backtracked 0 clauses, performed 0 splits and kept 13481 clauses. % 88.55/88.75 SPASS allocated 113490 KBytes. % 88.55/88.75 SPASS spent 0:1:25.69 on the problem. % 88.55/88.75 0:00:00.10 for the input. % 88.55/88.75 0:00:07.46 for the FLOTTER CNF translation. % 88.55/88.75 0:00:00.30 for inferences. % 88.55/88.75 0:00:00.00 for the backtracking. % 88.55/88.75 0:01:00.94 for the reduction. % 88.55/88.75 % 88.55/88.75 % 88.55/88.75 Here is a proof with depth 2, length 6 : % 88.55/88.75 % SZS output start Refutation % 88.55/88.75 2381[0:Inp] || -> individual(f_urlfn(f_urlfn(s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml)))*. % 88.55/88.75 2583[0:Inp] || -> genls(f_urlfn(f_urlfn(s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml)),c_tptpcol_15_74743)*l. % 88.55/88.75 3964[0:Inp] individual(u) collection(u) || -> . % 88.55/88.75 6552[0:Inp] || genls(u,v)* -> collection(u)*. % 88.55/88.75 8009[0:Res:2583.0,6552.0] || -> collection(f_urlfn(f_urlfn(s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml)))*. % 88.55/88.75 17084[0:EmS:3964.0,3964.1,2381.0,8009.0] || -> . % 88.55/88.75 % SZS output end Refutation % 88.55/88.75 Formulae used in the proof : ax2_2813 query164 ax2_3226 ax2_7990 % 88.55/88.75 %------------------------------------------------------------------------------