%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : PRO018+3 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n006.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:54 EDT 2022 % Result : Theorem 9.29s 9.48s % Output : Refutation 9.29s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : PRO018+3 : TPTP v8.1.0. Released v4.0.0. % 0.03/0.13 % Command : run_spass %d %s % 0.13/0.34 % Computer : n006.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Mon Jun 13 03:16:42 EDT 2022 % 0.13/0.34 % CPUTime : % 9.29/9.48 % 9.29/9.48 SPASS V 3.9 % 9.29/9.48 SPASS beiseite: Proof found. % 9.29/9.48 % SZS status Theorem % 9.29/9.48 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 9.29/9.48 SPASS derived 11721 clauses, backtracked 989 clauses, performed 44 splits and kept 6566 clauses. % 9.29/9.48 SPASS allocated 109891 KBytes. % 9.29/9.48 SPASS spent 0:00:09.04 on the problem. % 9.29/9.48 0:00:00.04 for the input. % 9.29/9.48 0:00:00.18 for the FLOTTER CNF translation. % 9.29/9.48 0:00:00.23 for inferences. % 9.29/9.48 0:00:00.19 for the backtracking. % 9.29/9.48 0:00:08.23 for the reduction. % 9.29/9.48 % 9.29/9.48 % 9.29/9.48 Here is a proof with depth 9, length 92 : % 9.29/9.48 % SZS output start Refutation % 9.29/9.48 1[0:Inp] || -> arboreal(skc3)*. % 9.29/9.48 3[0:Inp] || -> atomic(tptp4)*. % 9.29/9.48 7[0:Inp] || -> subactivity_occurrence(skc3,skc2)*l. % 9.29/9.48 8[0:Inp] || -> occurrence_of(skc2,tptp0)*. % 9.29/9.48 11[0:Inp] || leaf_occ(skc3,skc2)* -> . % 9.29/9.48 13[0:Inp] || equal(tptp4,tptp3)** -> . % 9.29/9.48 16[0:Inp] || equal(tptp1,tptp3)** -> . % 9.29/9.48 17[0:Inp] || equal(tptp2,tptp3)** -> . % 9.29/9.48 23[0:Inp] || occurrence_of(u,v)* -> activity(v). % 9.29/9.48 24[0:Inp] || occurrence_of(u,v)* -> activity_occurrence(u). % 9.29/9.48 26[0:Inp] || precedes(u,v)* -> legal(v). % 9.29/9.48 31[0:Inp] activity_occurrence(u) || -> occurrence_of(u,skf23(u))*. % 9.29/9.48 36[0:Inp] || next_subocc(u,v,w)* -> arboreal(v). % 9.29/9.48 40[0:Inp] || min_precedes(u,v,w)* -> precedes(u,v). % 9.29/9.48 43[0:Inp] atomic(u) || occurrence_of(v,u)* -> arboreal(v). % 9.29/9.48 49[0:Inp] || next_subocc(u,v,w)* -> min_precedes(u,v,w). % 9.29/9.48 63[0:Inp] || occurrence_of(u,v)*+ occurrence_of(u,w)* -> equal(w,v)*. % 9.29/9.48 66[0:Inp] || min_precedes(u,v,w) -> occurrence_of(skf32(v,u,w),w)*. % 9.29/9.48 68[0:Inp] || min_precedes(u,v,w)*+ -> subactivity_occurrence(v,skf32(v,x,y))*r. % 9.29/9.48 78[0:Inp] || leaf_occ(u,v)* occurrence_of(v,w)* min_precedes(u,x,w)*+ -> . % 9.29/9.48 83[0:Inp] || min_precedes(skf44(u),v,tptp0)* -> equal(v,skf40(u)) equal(v,skf42(u)). % 9.29/9.48 96[0:Inp] arboreal(u) || subactivity_occurrence(u,v)+ occurrence_of(v,tptp0) -> leaf_occ(u,v)* occurrence_of(skf44(u),tptp3)*. % 9.29/9.48 97[0:Inp] arboreal(u) || subactivity_occurrence(u,v) occurrence_of(v,tptp0) -> occurrence_of(skf42(w),tptp4)* leaf_occ(u,v)*. % 9.29/9.48 99[0:Inp] arboreal(u) || subactivity_occurrence(u,v)+ occurrence_of(v,tptp0) -> leaf_occ(u,v)* next_subocc(u,skf44(u),tptp0)*. % 9.29/9.48 101[0:Inp] arboreal(u) || subactivity_occurrence(u,v)+ occurrence_of(v,tptp0) -> leaf_occ(u,v)* min_precedes(skf44(u),skf42(u),tptp0)*. % 9.29/9.48 104[0:Inp] arboreal(u) || subactivity_occurrence(u,v) occurrence_of(v,tptp0) -> occurrence_of(skf40(w),tptp1) occurrence_of(skf40(w),tptp2)* leaf_occ(u,v)*. % 9.29/9.48 167[0:Res:7.0,104.1] arboreal(skc3) || occurrence_of(skc2,tptp0) -> occurrence_of(skf40(u),tptp1) occurrence_of(skf40(u),tptp2)* leaf_occ(skc3,skc2). % 9.29/9.48 168[0:Res:7.0,101.1] arboreal(skc3) || occurrence_of(skc2,tptp0) -> min_precedes(skf44(skc3),skf42(skc3),tptp0)* leaf_occ(skc3,skc2). % 9.29/9.48 170[0:Res:7.0,99.1] arboreal(skc3) || occurrence_of(skc2,tptp0) -> next_subocc(skc3,skf44(skc3),tptp0)* leaf_occ(skc3,skc2). % 9.29/9.48 171[0:Res:7.0,97.1] arboreal(skc3) || occurrence_of(skc2,tptp0) -> occurrence_of(skf42(u),tptp4)* leaf_occ(skc3,skc2). % 9.29/9.48 172[0:Res:7.0,96.1] arboreal(skc3) || occurrence_of(skc2,tptp0) -> occurrence_of(skf44(skc3),tptp3)* leaf_occ(skc3,skc2). % 9.29/9.48 193[0:MRR:171.0,171.1,171.3,1.0,8.0,11.0] || -> occurrence_of(skf42(u),tptp4)*. % 9.29/9.48 194[0:MRR:172.0,172.1,172.3,1.0,8.0,11.0] || -> occurrence_of(skf44(skc3),tptp3)*. % 9.29/9.48 195[0:MRR:170.0,170.1,170.3,1.0,8.0,11.0] || -> next_subocc(skc3,skf44(skc3),tptp0)*. % 9.29/9.48 196[0:MRR:168.0,168.1,168.3,1.0,8.0,11.0] || -> min_precedes(skf44(skc3),skf42(skc3),tptp0)*. % 9.29/9.48 199[0:MRR:167.0,167.1,167.4,1.0,8.0,11.0] || -> occurrence_of(skf40(u),tptp2)* occurrence_of(skf40(u),tptp1). % 9.29/9.48 264[0:Res:193.0,23.0] || -> activity(tptp4)*. % 9.29/9.48 266[0:Res:194.0,24.0] || -> activity_occurrence(skf44(skc3))*. % 9.29/9.48 267[0:Res:193.0,24.0] || -> activity_occurrence(skf42(u))*. % 9.29/9.48 279[0:Res:195.0,36.0] || -> arboreal(skf44(skc3))*. % 9.29/9.48 307[0:Res:193.0,43.1] atomic(tptp4) || -> arboreal(skf42(u))*. % 9.29/9.48 311[0:SSi:307.0,3.0,264.0] || -> arboreal(skf42(u))*. % 9.29/9.48 377[0:Res:195.0,49.0] || -> min_precedes(skc3,skf44(skc3),tptp0)*. % 9.29/9.48 380[0:Res:377.0,40.0] || -> precedes(skc3,skf44(skc3))*. % 9.29/9.48 385[0:Res:380.0,26.0] || -> legal(skf44(skc3))*. % 9.29/9.48 499[0:Res:193.0,63.0] || occurrence_of(skf42(u),v)* -> equal(v,tptp4). % 9.29/9.48 500[0:Res:31.1,63.0] activity_occurrence(u) || occurrence_of(u,v)* -> equal(v,skf23(u)). % 9.29/9.48 502[0:Res:199.0,63.0] || occurrence_of(skf40(u),v)*+ -> occurrence_of(skf40(u),tptp1)* equal(v,tptp2). % 9.29/9.48 507[0:MRR:500.0,24.1] || occurrence_of(u,v)* -> equal(v,skf23(u)). % 9.29/9.48 519[0:Res:31.1,499.0] activity_occurrence(skf42(u)) || -> equal(skf23(skf42(u)),tptp4)**. % 9.29/9.48 523[0:SSi:519.0,267.0,311.0] || -> equal(skf23(skf42(u)),tptp4)**. % 9.29/9.48 603[0:Res:199.0,507.0] || -> occurrence_of(skf40(u),tptp1)* equal(skf23(skf40(u)),tptp2). % 9.29/9.48 696[0:Res:603.0,23.0] || -> equal(skf23(skf40(u)),tptp2)** activity(tptp1). % 9.29/9.48 698[1:Spt:696.0] || -> equal(skf23(skf40(u)),tptp2)**. % 9.29/9.48 717[0:Res:196.0,78.2] || leaf_occ(skf44(skc3),u)* occurrence_of(u,tptp0) -> . % 9.29/9.48 1001[0:Res:377.0,68.0] || -> subactivity_occurrence(skf44(skc3),skf32(skf44(skc3),u,v))*r. % 9.29/9.48 2268[0:Res:1001.0,99.1] arboreal(skf44(skc3)) || occurrence_of(skf32(skf44(skc3),u,v),tptp0) -> leaf_occ(skf44(skc3),skf32(skf44(skc3),u,v))* next_subocc(skf44(skc3),skf44(skf44(skc3)),tptp0). % 9.29/9.48 2269[0:Res:1001.0,96.1] arboreal(skf44(skc3)) || occurrence_of(skf32(skf44(skc3),u,v),tptp0) -> leaf_occ(skf44(skc3),skf32(skf44(skc3),u,v))* occurrence_of(skf44(skf44(skc3)),tptp3). % 9.29/9.48 2311[0:SSi:2269.0,266.0,279.0,385.0] || occurrence_of(skf32(skf44(skc3),u,v),tptp0) -> leaf_occ(skf44(skc3),skf32(skf44(skc3),u,v))* occurrence_of(skf44(skf44(skc3)),tptp3). % 9.29/9.48 2312[0:MRR:2311.1,717.0] || occurrence_of(skf32(skf44(skc3),u,v),tptp0)* -> occurrence_of(skf44(skf44(skc3)),tptp3). % 9.29/9.48 2313[0:SSi:2268.0,266.0,279.0,385.0] || occurrence_of(skf32(skf44(skc3),u,v),tptp0) -> leaf_occ(skf44(skc3),skf32(skf44(skc3),u,v))* next_subocc(skf44(skc3),skf44(skf44(skc3)),tptp0). % 9.29/9.48 2314[0:MRR:2313.1,717.0] || occurrence_of(skf32(skf44(skc3),u,v),tptp0)*+ -> next_subocc(skf44(skc3),skf44(skf44(skc3)),tptp0)*. % 9.29/9.48 2407[0:Res:66.1,2312.0] || min_precedes(u,skf44(skc3),tptp0)* -> occurrence_of(skf44(skf44(skc3)),tptp3). % 9.29/9.48 2409[0:Res:377.0,2407.0] || -> occurrence_of(skf44(skf44(skc3)),tptp3)*. % 9.29/9.48 2418[0:Res:2409.0,507.0] || -> equal(skf23(skf44(skf44(skc3))),tptp3)**. % 9.29/9.48 10605[0:Res:66.1,2314.0] || min_precedes(u,skf44(skc3),tptp0)*+ -> next_subocc(skf44(skc3),skf44(skf44(skc3)),tptp0)*. % 9.29/9.48 10609[0:Res:377.0,10605.0] || -> next_subocc(skf44(skc3),skf44(skf44(skc3)),tptp0)*. % 9.29/9.48 10617[0:Res:10609.0,49.0] || -> min_precedes(skf44(skc3),skf44(skf44(skc3)),tptp0)*. % 9.29/9.48 10624[0:Res:10617.0,83.0] || -> equal(skf44(skf44(skc3)),skf40(skc3)) equal(skf44(skf44(skc3)),skf42(skc3))**. % 9.29/9.48 10982[2:Spt:10624.0] || -> equal(skf44(skf44(skc3)),skf40(skc3))**. % 9.29/9.48 10986[2:Rew:10982.0,2418.0] || -> equal(skf23(skf40(skc3)),tptp3)**. % 9.29/9.48 11088[2:Rew:698.0,10986.0] || -> equal(tptp2,tptp3)**. % 9.29/9.48 11089[2:MRR:11088.0,17.0] || -> . % 9.29/9.48 11128[2:Spt:11089.0,10624.0,10982.0] || equal(skf44(skf44(skc3)),skf40(skc3))** -> . % 9.29/9.48 11129[2:Spt:11089.0,10624.1] || -> equal(skf44(skf44(skc3)),skf42(skc3))**. % 9.29/9.48 11140[2:Rew:11129.0,2418.0] || -> equal(skf23(skf42(skc3)),tptp3)**. % 9.29/9.48 11143[2:Rew:523.0,11140.0] || -> equal(tptp4,tptp3)**. % 9.29/9.48 11144[2:MRR:11143.0,13.0] || -> . % 9.29/9.48 11241[1:Spt:11144.0,696.1] || -> activity(tptp1)*. % 9.29/9.48 13730[2:Spt:10624.0] || -> equal(skf44(skf44(skc3)),skf40(skc3))**. % 9.29/9.48 13734[2:Rew:13730.0,2409.0] || -> occurrence_of(skf40(skc3),tptp3)*. % 9.29/9.48 13736[2:Rew:13730.0,2418.0] || -> equal(skf23(skf40(skc3)),tptp3)**. % 9.29/9.48 13937[2:Res:13734.0,502.0] || -> occurrence_of(skf40(skc3),tptp1)* equal(tptp2,tptp3). % 9.29/9.48 13938[2:MRR:13937.1,17.0] || -> occurrence_of(skf40(skc3),tptp1)*. % 9.29/9.48 13978[2:Res:13938.0,507.0] || -> equal(skf23(skf40(skc3)),tptp1)**. % 9.29/9.48 13986[2:Rew:13736.0,13978.0] || -> equal(tptp1,tptp3)**. % 9.29/9.48 13987[2:MRR:13986.0,16.0] || -> . % 9.29/9.48 13989[2:Spt:13987.0,10624.0,13730.0] || equal(skf44(skf44(skc3)),skf40(skc3))** -> . % 9.29/9.48 13990[2:Spt:13987.0,10624.1] || -> equal(skf44(skf44(skc3)),skf42(skc3))**. % 9.29/9.48 14001[2:Rew:13990.0,2418.0] || -> equal(skf23(skf42(skc3)),tptp3)**. % 9.29/9.48 14004[2:Rew:523.0,14001.0] || -> equal(tptp4,tptp3)**. % 9.29/9.48 14005[2:MRR:14004.0,13.0] || -> . % 9.29/9.48 % SZS output end Refutation % 9.29/9.48 Formulae used in the proof : goals sos_52 sos_56 sos_59 sos_60 sos sos_10 sos_01 sos_44 sos_15 sos_07 sos_22 sos_02 sos_25 sos_37 sos_49 sos_46 sos_51 % 9.29/9.48 %------------------------------------------------------------------------------