%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : NUN065+1 : TPTP v8.1.0. Released v7.3.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n024.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 : Mon Jul 18 16:38:44 EDT 2022 % Result : Theorem 11.40s 11.56s % Output : Refutation 11.40s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.11 % Problem : NUN065+1 : TPTP v8.1.0. Released v7.3.0. % 0.11/0.12 % Command : run_spass %d %s % 0.11/0.33 % Computer : n024.cluster.edu % 0.11/0.33 % Model : x86_64 x86_64 % 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.33 % Memory : 8042.1875MB % 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.33 % CPULimit : 300 % 0.11/0.33 % WCLimit : 600 % 0.11/0.33 % DateTime : Thu Jun 2 11:06:36 EDT 2022 % 0.11/0.33 % CPUTime : % 11.40/11.56 % 11.40/11.56 SPASS V 3.9 % 11.40/11.56 SPASS beiseite: Proof found. % 11.40/11.56 % SZS status Theorem % 11.40/11.56 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 11.40/11.56 SPASS derived 14032 clauses, backtracked 0 clauses, performed 0 splits and kept 6657 clauses. % 11.40/11.56 SPASS allocated 107322 KBytes. % 11.40/11.56 SPASS spent 0:0:11.14 on the problem. % 11.40/11.56 0:00:00.04 for the input. % 11.40/11.56 0:00:00.04 for the FLOTTER CNF translation. % 11.40/11.56 0:00:00.14 for inferences. % 11.40/11.56 0:00:00.00 for the backtracking. % 11.40/11.56 0:0:10.82 for the reduction. % 11.40/11.56 % 11.40/11.56 % 11.40/11.56 Here is a proof with depth 6, length 50 : % 11.40/11.56 % SZS output start Refutation % 11.40/11.56 1[0:Inp] || -> r1(skf24(u))*. % 11.40/11.56 6[0:Inp] || -> id__dfg(u,skf22(u))*r. % 11.40/11.56 8[0:Inp] || -> id__dfg(u,skf43(u))*r. % 11.40/11.56 9[0:Inp] || -> r2(skf24(u),skf23(u))*. % 11.40/11.56 11[0:Inp] || -> r2(u,skf34(v,u))*. % 11.40/11.56 14[0:Inp] SkP9(u) || -> r1(skf22(u))*. % 11.40/11.56 15[0:Inp] || -> SkP9(u) id__dfg(u,skf23(u))*r. % 11.40/11.56 16[0:Inp] r1(u) || -> SkP0(skc2,u)*. % 11.40/11.56 17[0:Inp] || SkP0(u,v)* -> r1(v). % 11.40/11.56 22[0:Inp] || -> SkP8(u) id__dfg(u,skf41(u))*r. % 11.40/11.56 23[0:Inp] SkP8(u) || -> r1(skf43(u))*. % 11.40/11.56 24[0:Inp] || id__dfg(u,skc2) -> SkP0(skc2,u)*. % 11.40/11.56 25[0:Inp] || SkP0(u,v)* -> id__dfg(v,u). % 11.40/11.56 26[0:Inp] || id__dfg(u,v)* -> id__dfg(v,u). % 11.40/11.56 28[0:Inp] r1(u) || SkP4(u,v)* -> . % 11.40/11.56 40[0:Inp] || id__dfg(u,v) -> r1(u) SkP4(v,u)*. % 11.40/11.56 45[0:Inp] || r2(u,v) SkP5(w,x,v,u)* -> . % 11.40/11.56 47[0:Inp] || id__dfg(u,v)* id__dfg(v,w)* -> id__dfg(u,w)*. % 11.40/11.56 48[0:Inp] r1(u) || r2(v,w)* id__dfg(u,w)*+ -> . % 11.40/11.56 57[0:Inp] || r2(u,v)* r2(w,x)* id__dfg(x,v)*+ -> id__dfg(w,u)*. % 11.40/11.56 59[0:Inp] || id__dfg(u,v) id__dfg(w,x) -> r2(x,v) SkP5(v,x,u,w)*. % 11.40/11.56 66[0:Res:1.0,28.0] || SkP4(skf24(u),v)* -> . % 11.40/11.56 68[0:Res:9.0,45.0] || SkP5(u,v,skf23(w),skf24(w))* -> . % 11.40/11.56 71[0:Res:9.0,48.2] r1(u) || id__dfg(u,skf23(v))* -> . % 11.40/11.56 82[0:Res:6.0,48.1] r1(u) || r2(v,skf22(u))* -> . % 11.40/11.56 89[0:Res:6.0,59.1] || id__dfg(u,v) -> r2(v,skf22(w)) SkP5(skf22(w),v,w,u)*. % 11.40/11.56 113[0:Res:6.0,89.0] || -> r2(skf22(u),skf22(v)) SkP5(skf22(v),skf22(u),v,u)*. % 11.40/11.56 163[0:Res:24.1,17.0] || id__dfg(u,skc2) -> r1(u)*. % 11.40/11.56 182[0:Res:16.1,25.0] r1(u) || -> id__dfg(u,skc2)*. % 11.40/11.56 191[0:OCh:47.1,47.0,182.1,8.0] r1(skf43(u)) || -> id__dfg(u,skc2)*. % 11.40/11.56 202[0:SoR:191.0,23.1] SkP8(u) || -> id__dfg(u,skc2)*. % 11.40/11.56 261[0:Res:113.1,45.1] || r2(u,v) -> r2(skf22(u),skf22(v))*. % 11.40/11.56 262[0:Res:113.1,68.0] || -> r2(skf22(skf24(u)),skf22(skf23(u)))*. % 11.40/11.56 264[0:Res:262.0,82.1] r1(skf23(u)) || -> . % 11.40/11.56 267[0:SoR:264.0,163.1] || id__dfg(skf23(u),skc2)*l -> . % 11.40/11.56 271[0:Res:261.1,82.1] r1(u) || r2(v,u)* -> . % 11.40/11.56 278[0:Res:261.1,271.1] r1(skf22(u)) || r2(v,u)* -> . % 11.40/11.56 296[0:Res:40.2,66.0] || id__dfg(u,skf24(v))*+ -> r1(u)*. % 11.40/11.56 320[0:SoR:278.0,14.1] SkP9(u) || r2(v,u)* -> . % 11.40/11.56 337[0:Res:202.1,267.0] SkP8(skf23(u)) || -> . % 11.40/11.56 411[0:NCh:47.2,47.1,26.0,6.0] || id__dfg(u,v)*+ -> id__dfg(skf22(v),u)*. % 11.40/11.56 468[0:Res:15.1,57.2] || r2(u,skf23(v))* r2(w,v)* -> SkP9(v) id__dfg(w,u)*. % 11.40/11.56 498[0:MRR:468.2,320.0] || r2(u,skf23(v))*+ r2(w,v)* -> id__dfg(w,u)*. % 11.40/11.56 1724[0:Res:9.0,498.0] || r2(u,v)* -> id__dfg(u,skf24(v)). % 11.40/11.56 1974[0:Res:22.1,411.0] || -> SkP8(u) id__dfg(skf22(skf41(u)),u)*l. % 11.40/11.56 11615[0:Res:1974.1,71.1] r1(skf22(skf41(skf23(u)))) || -> SkP8(skf23(u))*. % 11.40/11.56 11687[0:MRR:11615.1,337.0] r1(skf22(skf41(skf23(u)))) || -> . % 11.40/11.56 11735[0:SoR:11687.0,296.1] || id__dfg(skf22(skf41(skf23(u))),skf24(v))* -> . % 11.40/11.56 14952[0:Res:11.0,1724.0] || -> id__dfg(u,skf24(skf34(v,u)))*r. % 11.40/11.56 14958[0:UnC:14952.0,11735.0] || -> . % 11.40/11.56 % SZS output end Refutation % 11.40/11.56 Formulae used in the proof : nononesexistid axiom_5 axiom_6 axiom_5a axiom_1a axiom_6a axiom_2a axiom_1 axiom_8 axiom_9 axiom_7 axiom_7a axiom_3a % 11.40/11.56 %------------------------------------------------------------------------------