%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : PRO009+1 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n005.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 17:53:46 EDT 2022 % Result : Theorem 227.49s 227.67s % Output : Refutation 229.06s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.13 % Problem : PRO009+1 : TPTP v8.1.0. Released v4.0.0. % 0.07/0.14 % Command : run_spass %d %s % 0.14/0.35 % Computer : n005.cluster.edu % 0.14/0.35 % Model : x86_64 x86_64 % 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.35 % Memory : 8042.1875MB % 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.35 % CPULimit : 300 % 0.14/0.35 % WCLimit : 600 % 0.14/0.35 % DateTime : Mon Jun 13 03:36:54 EDT 2022 % 0.14/0.36 % CPUTime : % 227.49/227.67 % 227.49/227.67 SPASS V 3.9 % 227.49/227.67 SPASS beiseite: Proof found. % 227.49/227.67 % SZS status Theorem % 227.49/227.67 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 227.49/227.67 SPASS derived 61496 clauses, backtracked 3109 clauses, performed 82 splits and kept 31001 clauses. % 227.49/227.67 SPASS allocated 175032 KBytes. % 227.49/227.67 SPASS spent 0:3:47.24 on the problem. % 227.49/227.67 0:00:00.03 for the input. % 227.49/227.67 0:00:00.10 for the FLOTTER CNF translation. % 227.49/227.67 0:00:02.35 for inferences. % 227.49/227.67 0:00:09.57 for the backtracking. % 227.49/227.67 0:3:32.30 for the reduction. % 227.49/227.67 % 227.49/227.67 % 227.49/227.67 Here is a proof with depth 7, length 128 : % 227.49/227.67 % SZS output start Refutation % 227.49/227.67 3[0:Inp] || -> atomic(tptp2)*. % 227.49/227.67 4[0:Inp] || -> atomic(tptp1)*. % 227.49/227.67 5[0:Inp] || -> atomic(tptp3)*. % 227.49/227.67 6[0:Inp] || -> occurrence_of(skc1,tptp0)*. % 227.49/227.67 10[0:Inp] || -> occurrence_of(skf35(u),tptp3)*. % 227.49/227.67 18[0:Inp] legal(u) || -> arboreal(u)*. % 227.49/227.67 19[0:Inp] || occurrence_of(u,v)* -> activity(v). % 227.49/227.67 20[0:Inp] || occurrence_of(u,v)* -> activity_occurrence(u). % 227.49/227.67 22[0:Inp] || precedes(u,v)* -> legal(v). % 227.49/227.67 23[0:Inp] || root(u,v)* -> legal(u). % 227.49/227.67 26[0:Inp] activity_occurrence(u) || -> occurrence_of(u,skf18(u))*. % 227.49/227.67 27[0:Inp] || precedes(u,v)* -> earlier(u,v). % 227.49/227.67 28[0:Inp] || root_occ(u,v)* -> subactivity_occurrence(u,v). % 227.49/227.67 29[0:Inp] || leaf_occ(u,v)* -> subactivity_occurrence(u,v). % 227.49/227.67 30[0:Inp] || earlier(u,v)*+ earlier(v,u)* -> . % 227.49/227.67 31[0:Inp] || min_precedes(u,v,w)* -> precedes(u,v). % 227.49/227.67 33[0:Inp] || -> occurrence_of(skf33(u),tptp1)* occurrence_of(skf33(u),tptp2). % 227.49/227.67 34[0:Inp] || occurrence_of(u,tptp0) -> root_occ(skf35(u),u)*. % 227.49/227.67 35[0:Inp] || occurrence_of(u,tptp0) -> leaf_occ(skf33(u),u)*. % 227.49/227.67 37[0:Inp] atomic(u) || occurrence_of(v,u)* -> arboreal(v). % 227.49/227.67 41[0:Inp] || root(u,v) min_precedes(w,u,v)* -> . % 227.49/227.67 43[0:Inp] || next_subocc(u,v,w)* -> min_precedes(u,v,w). % 227.49/227.67 45[0:Inp] || atocc(u,v) -> occurrence_of(u,skf26(u,v))*. % 227.49/227.67 46[0:Inp] || root_occ(u,v) -> occurrence_of(v,skf31(u,v))*. % 227.49/227.67 47[0:Inp] || root_occ(u,v)*+ -> root(u,skf31(u,w))*. % 227.49/227.67 51[0:Inp] || min_precedes(u,v,w)*+ -> atocc(v,skf19(w,v))*. % 227.49/227.67 57[0:Inp] || occurrence_of(u,tptp0) -> next_subocc(skf35(u),skf34(u),tptp0)*. % 227.49/227.67 58[0:Inp] || occurrence_of(u,tptp0) -> next_subocc(skf34(u),skf33(u),tptp0)*. % 227.49/227.67 59[0:Inp] || occurrence_of(u,v)*+ occurrence_of(u,w)* -> equal(w,v)*. % 227.49/227.67 60[0:Inp] || earlier(u,v)* earlier(v,w)* -> earlier(u,w)*. % 227.49/227.67 69[0:Inp] || subactivity_occurrence(u,v)* subactivity_occurrence(v,w)* -> subactivity_occurrence(u,w)*. % 227.49/227.67 86[0:Inp] || leaf_occ(u,skc1) root_occ(v,skc1) occurrence_of(v,tptp3) occurrence_of(u,tptp1) min_precedes(v,u,tptp0)* -> . % 227.49/227.67 87[0:Inp] || leaf_occ(u,skc1) root_occ(v,skc1) occurrence_of(v,tptp3) occurrence_of(u,tptp2) min_precedes(v,u,tptp0)* -> . % 227.49/227.67 88[0:Inp] arboreal(u) arboreal(v) || subactivity_occurrence(u,w)*+ occurrence_of(w,x)* subactivity_occurrence(v,w)* -> equal(v,u) min_precedes(u,v,x)* min_precedes(v,u,x)*. % 227.49/227.67 94[0:Res:6.0,59.0] || occurrence_of(skc1,u)* -> equal(tptp0,u). % 227.49/227.67 98[0:Res:6.0,20.0] || -> activity_occurrence(skc1)*. % 227.49/227.67 99[0:Res:6.0,57.0] || -> next_subocc(skf35(skc1),skf34(skc1),tptp0)*. % 227.49/227.67 100[0:Res:6.0,58.0] || -> next_subocc(skf34(skc1),skf33(skc1),tptp0)*. % 227.49/227.67 101[0:Res:6.0,34.0] || -> root_occ(skf35(skc1),skc1)*. % 227.49/227.67 102[0:Res:6.0,35.0] || -> leaf_occ(skf33(skc1),skc1)*. % 227.49/227.67 109[0:Res:6.0,88.3] arboreal(u) arboreal(v) || subactivity_occurrence(u,skc1)+ subactivity_occurrence(v,skc1) -> equal(v,u) min_precedes(u,v,tptp0)* min_precedes(v,u,tptp0)*. % 227.49/227.67 126[0:Res:101.0,87.2] || occurrence_of(u,tptp2) occurrence_of(skf35(skc1),tptp3) min_precedes(skf35(skc1),u,tptp0)* leaf_occ(u,skc1) -> . % 227.49/227.67 127[0:Res:102.0,87.4] || root_occ(u,skc1) occurrence_of(u,tptp3) occurrence_of(skf33(skc1),tptp2) min_precedes(u,skf33(skc1),tptp0)* -> . % 227.49/227.67 128[0:Res:101.0,86.2] || occurrence_of(u,tptp1) occurrence_of(skf35(skc1),tptp3) min_precedes(skf35(skc1),u,tptp0)* leaf_occ(u,skc1) -> . % 227.49/227.67 129[0:Res:102.0,86.4] || root_occ(u,skc1) occurrence_of(u,tptp3) occurrence_of(skf33(skc1),tptp1) min_precedes(u,skf33(skc1),tptp0)* -> . % 227.49/227.67 130[0:MRR:126.1,10.0] || leaf_occ(u,skc1) occurrence_of(u,tptp2) min_precedes(skf35(skc1),u,tptp0)* -> . % 227.49/227.67 131[0:MRR:128.1,10.0] || leaf_occ(u,skc1) occurrence_of(u,tptp1) min_precedes(skf35(skc1),u,tptp0)* -> . % 227.49/227.67 136[0:Res:10.0,19.0] || -> activity(tptp3)*. % 227.49/227.67 139[0:Res:10.0,20.0] || -> activity_occurrence(skf35(u))*. % 227.49/227.67 146[0:Res:33.0,20.0] || -> occurrence_of(skf33(u),tptp2)* activity_occurrence(skf33(u)). % 227.49/227.67 147[0:Res:33.0,19.0] || -> occurrence_of(skf33(u),tptp2)* activity(tptp1). % 227.49/227.67 148[0:MRR:146.0,20.0] || -> activity_occurrence(skf33(u))*. % 227.49/227.67 152[1:Spt:147.0] || -> occurrence_of(skf33(u),tptp2)*. % 227.49/227.67 153[1:MRR:127.2,152.0] || root_occ(u,skc1) occurrence_of(u,tptp3) min_precedes(u,skf33(skc1),tptp0)* -> . % 227.49/227.67 155[1:Res:152.0,19.0] || -> activity(tptp2)*. % 227.49/227.67 158[0:Res:10.0,37.1] atomic(tptp3) || -> arboreal(skf35(u))*. % 227.49/227.67 160[1:Res:152.0,37.1] atomic(tptp2) || -> arboreal(skf33(u))*. % 227.49/227.67 162[0:SSi:158.0,5.0,136.0] || -> arboreal(skf35(u))*. % 227.49/227.67 163[1:SSi:160.0,3.0,155.0] || -> arboreal(skf33(u))*. % 227.49/227.67 184[0:Res:46.1,94.0] || root_occ(u,skc1) -> equal(skf31(u,skc1),tptp0)**. % 227.49/227.67 217[0:Res:101.0,47.0] || -> root(skf35(skc1),skf31(skf35(skc1),u))*. % 227.49/227.67 219[0:SpR:184.1,217.0] || root_occ(skf35(skc1),skc1)* -> root(skf35(skc1),tptp0). % 227.49/227.67 221[0:Res:217.0,23.0] || -> legal(skf35(skc1))*. % 227.49/227.67 222[0:MRR:219.0,101.0] || -> root(skf35(skc1),tptp0)*. % 227.49/227.67 227[0:Res:100.0,43.0] || -> min_precedes(skf34(skc1),skf33(skc1),tptp0)*. % 227.49/227.67 228[0:Res:99.0,43.0] || -> min_precedes(skf35(skc1),skf34(skc1),tptp0)*. % 227.49/227.67 230[0:Res:227.0,31.0] || -> precedes(skf34(skc1),skf33(skc1))*. % 227.49/227.67 233[0:Res:230.0,22.0] || -> legal(skf33(skc1))*. % 227.49/227.67 236[0:Res:228.0,31.0] || -> precedes(skf35(skc1),skf34(skc1))*. % 227.49/227.67 257[0:Res:227.0,51.0] || -> atocc(skf33(skc1),skf19(tptp0,skf33(skc1)))*. % 227.49/227.67 329[0:Res:26.1,59.0] activity_occurrence(u) || occurrence_of(u,v)* -> equal(v,skf18(u)). % 227.49/227.67 335[0:MRR:329.0,20.1] || occurrence_of(u,v)* -> equal(v,skf18(u)). % 227.49/227.67 394[0:Res:230.0,27.0] || -> earlier(skf34(skc1),skf33(skc1))*l. % 227.49/227.67 397[0:Res:236.0,27.0] || -> earlier(skf35(skc1),skf34(skc1))*l. % 227.49/227.67 414[0:Res:45.1,335.0] || atocc(u,v) -> equal(skf26(u,v),skf18(u))**. % 227.49/227.67 421[0:Rew:414.1,45.1] || atocc(u,v)*+ -> occurrence_of(u,skf18(u))*. % 227.49/227.67 456[0:Res:257.0,421.0] || -> occurrence_of(skf33(skc1),skf18(skf33(skc1)))*. % 227.49/227.67 509[0:Res:102.0,29.0] || -> subactivity_occurrence(skf33(skc1),skc1)*l. % 227.49/227.67 523[0:Res:101.0,28.0] || -> subactivity_occurrence(skf35(skc1),skc1)*l. % 227.49/227.67 853[0:NCh:60.2,60.0,30.0,394.0] || equal(skf33(skc1),u) earlier(u,skf34(skc1))* -> . % 227.49/227.67 3318[0:Res:397.0,853.1] || equal(skf35(skc1),skf33(skc1))** -> . % 227.49/227.67 3630[0:Res:523.0,109.2] arboreal(skf35(skc1)) arboreal(u) || subactivity_occurrence(u,skc1) -> equal(u,skf35(skc1)) min_precedes(skf35(skc1),u,tptp0)* min_precedes(u,skf35(skc1),tptp0)*. % 227.49/227.67 3655[0:SSi:3630.0,221.0,139.0,98.0,162.0,98.0] arboreal(u) || subactivity_occurrence(u,skc1)+ -> equal(u,skf35(skc1)) min_precedes(skf35(skc1),u,tptp0)* min_precedes(u,skf35(skc1),tptp0)*. % 227.49/227.67 65982[0:Res:509.0,3655.1] arboreal(skf33(skc1)) || -> equal(skf35(skc1),skf33(skc1)) min_precedes(skf35(skc1),skf33(skc1),tptp0)* min_precedes(skf33(skc1),skf35(skc1),tptp0). % 227.49/227.67 66011[0:NCh:69.2,69.0,3655.1,509.0] arboreal(skf33(skc1)) || equal(skc1,skc1) -> equal(skf35(skc1),skf33(skc1)) min_precedes(skf35(skc1),skf33(skc1),tptp0)* min_precedes(skf33(skc1),skf35(skc1),tptp0). % 227.49/227.67 66078[1:SSi:65982.0,233.0,148.0,98.0,163.0,98.0] || -> equal(skf35(skc1),skf33(skc1)) min_precedes(skf35(skc1),skf33(skc1),tptp0)* min_precedes(skf33(skc1),skf35(skc1),tptp0). % 227.49/227.67 66079[1:MRR:66078.0,3318.0] || -> min_precedes(skf35(skc1),skf33(skc1),tptp0)* min_precedes(skf33(skc1),skf35(skc1),tptp0). % 227.49/227.67 66081[0:Obv:66011.1] arboreal(skf33(skc1)) || -> equal(skf35(skc1),skf33(skc1)) min_precedes(skf35(skc1),skf33(skc1),tptp0)* min_precedes(skf33(skc1),skf35(skc1),tptp0). % 227.49/227.67 66164[1:Res:66079.0,153.2] || root_occ(skf35(skc1),skc1) occurrence_of(skf35(skc1),tptp3) -> min_precedes(skf33(skc1),skf35(skc1),tptp0)*. % 227.49/227.67 66183[1:MRR:66164.0,66164.1,101.0,10.0] || -> min_precedes(skf33(skc1),skf35(skc1),tptp0)*. % 227.49/227.67 66217[1:Res:66183.0,41.1] || root(skf35(skc1),tptp0)* -> . % 227.49/227.67 66227[1:MRR:66217.0,222.0] || -> . % 227.49/227.67 66228[1:Spt:66227.0,147.1] || -> activity(tptp1)*. % 227.49/227.67 66324[0:SSi:66081.0,18.0,233.0,148.0,98.1] || -> equal(skf35(skc1),skf33(skc1)) min_precedes(skf35(skc1),skf33(skc1),tptp0)* min_precedes(skf33(skc1),skf35(skc1),tptp0). % 227.49/227.67 66325[0:MRR:66324.0,3318.0] || -> min_precedes(skf35(skc1),skf33(skc1),tptp0)* min_precedes(skf33(skc1),skf35(skc1),tptp0). % 229.06/229.20 66651[0:Res:33.0,335.0] || -> occurrence_of(skf33(u),tptp2)* equal(skf18(skf33(u)),tptp1). % 229.06/229.20 66657[0:Res:33.0,37.1] atomic(tptp1) || -> occurrence_of(skf33(u),tptp2)* arboreal(skf33(u)). % 229.06/229.20 66666[1:SSi:66657.0,4.0,66228.0] || -> occurrence_of(skf33(u),tptp2)* arboreal(skf33(u)). % 229.06/229.20 66735[1:Res:66666.0,37.1] atomic(tptp2) || -> arboreal(skf33(u))* arboreal(skf33(u))*. % 229.06/229.20 66744[1:Obv:66735.1] atomic(tptp2) || -> arboreal(skf33(u))*. % 229.06/229.20 66745[1:SSi:66744.0,3.0] || -> arboreal(skf33(u))*. % 229.06/229.20 67365[0:Res:66651.0,335.0] || -> equal(skf18(skf33(u)),tptp1)** equal(skf18(skf33(u)),tptp2). % 229.06/229.20 67369[0:Res:66651.0,19.0] || -> equal(skf18(skf33(u)),tptp1)** activity(tptp2). % 229.06/229.20 67382[2:Spt:67369.0] || -> equal(skf18(skf33(u)),tptp1)**. % 229.06/229.20 67385[2:Rew:67382.0,456.0] || -> occurrence_of(skf33(skc1),tptp1)*. % 229.06/229.20 67451[2:MRR:129.2,67385.0] || root_occ(u,skc1) occurrence_of(u,tptp3) min_precedes(u,skf33(skc1),tptp0)* -> . % 229.06/229.20 68755[0:Res:66325.0,31.0] || -> min_precedes(skf33(skc1),skf35(skc1),tptp0)* precedes(skf35(skc1),skf33(skc1)). % 229.06/229.20 68760[2:Res:66325.0,67451.2] || root_occ(skf35(skc1),skc1) occurrence_of(skf35(skc1),tptp3) -> min_precedes(skf33(skc1),skf35(skc1),tptp0)*. % 229.06/229.20 68765[0:Res:66325.0,131.2] || leaf_occ(skf33(skc1),skc1) occurrence_of(skf33(skc1),tptp1) -> min_precedes(skf33(skc1),skf35(skc1),tptp0)*. % 229.06/229.20 68766[0:Res:66325.0,130.2] || leaf_occ(skf33(skc1),skc1) occurrence_of(skf33(skc1),tptp2) -> min_precedes(skf33(skc1),skf35(skc1),tptp0)*. % 229.06/229.20 68779[2:MRR:68760.0,68760.1,101.0,10.0] || -> min_precedes(skf33(skc1),skf35(skc1),tptp0)*. % 229.06/229.20 68813[2:Res:68779.0,41.1] || root(skf35(skc1),tptp0)* -> . % 229.06/229.20 68821[2:MRR:68813.0,222.0] || -> . % 229.06/229.20 68823[2:Spt:68821.0,67369.1] || -> activity(tptp2)*. % 229.06/229.20 68824[0:MRR:68765.0,102.0] || occurrence_of(skf33(skc1),tptp1) -> min_precedes(skf33(skc1),skf35(skc1),tptp0)*. % 229.06/229.20 68825[0:MRR:68766.0,102.0] || occurrence_of(skf33(skc1),tptp2) -> min_precedes(skf33(skc1),skf35(skc1),tptp0)*. % 229.06/229.20 69412[0:SpR:67365.0,26.1] activity_occurrence(skf33(u)) || -> equal(skf18(skf33(u)),tptp2) occurrence_of(skf33(u),tptp1)*. % 229.06/229.20 69551[1:SSi:69412.0,148.0,66745.0] || -> equal(skf18(skf33(u)),tptp2) occurrence_of(skf33(u),tptp1)*. % 229.06/229.20 70093[3:Spt:68755.0] || -> min_precedes(skf33(skc1),skf35(skc1),tptp0)*. % 229.06/229.20 70127[3:Res:70093.0,41.1] || root(skf35(skc1),tptp0)* -> . % 229.06/229.20 70135[3:MRR:70127.0,222.0] || -> . % 229.06/229.20 70137[3:Spt:70135.0,68755.0,70093.0] || min_precedes(skf33(skc1),skf35(skc1),tptp0)* -> . % 229.06/229.20 70138[3:Spt:70135.0,68755.1] || -> precedes(skf35(skc1),skf33(skc1))*. % 229.06/229.20 70139[3:MRR:68824.1,70137.0] || occurrence_of(skf33(skc1),tptp1)* -> . % 229.06/229.20 70140[3:MRR:68825.1,70137.0] || occurrence_of(skf33(skc1),tptp2)* -> . % 229.06/229.20 70164[3:Res:69551.1,70139.0] || -> equal(skf18(skf33(skc1)),tptp2)**. % 229.06/229.20 70168[3:Rew:70164.0,456.0] || -> occurrence_of(skf33(skc1),tptp2)*. % 229.06/229.20 70203[3:MRR:70168.0,70140.0] || -> . % 229.06/229.20 % SZS output end Refutation % 229.06/229.20 Formulae used in the proof : sos_39 sos_40 sos_41 goals sos_35 sos_08 sos sos_10 sos_16 sos_01 sos_33 sos_34 sos_04 sos_15 sos_07 sos_14 sos_22 sos_23 sos_11 sos_02 sos_05 sos_31 sos_28 % 229.06/229.20 %------------------------------------------------------------------------------