%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : PRO018+4 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n023.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:55 EDT 2022 % Result : Theorem 1.47s 1.65s % Output : Refutation 1.47s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : PRO018+4 : TPTP v8.1.0. Released v4.0.0. % 0.11/0.13 % Command : run_spass %d %s % 0.12/0.34 % Computer : n023.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 600 % 0.12/0.34 % DateTime : Mon Jun 13 01:19:36 EDT 2022 % 0.12/0.35 % CPUTime : % 1.47/1.65 % 1.47/1.65 SPASS V 3.9 % 1.47/1.65 SPASS beiseite: Proof found. % 1.47/1.65 % SZS status Theorem % 1.47/1.65 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 1.47/1.65 SPASS derived 3634 clauses, backtracked 684 clauses, performed 13 splits and kept 2327 clauses. % 1.47/1.65 SPASS allocated 101755 KBytes. % 1.47/1.65 SPASS spent 0:00:01.28 on the problem. % 1.47/1.65 0:00:00.04 for the input. % 1.47/1.65 0:00:00.11 for the FLOTTER CNF translation. % 1.47/1.65 0:00:00.06 for inferences. % 1.47/1.65 0:00:00.01 for the backtracking. % 1.47/1.65 0:00:01.01 for the reduction. % 1.47/1.65 % 1.47/1.65 % 1.47/1.65 Here is a proof with depth 12, length 95 : % 1.47/1.65 % SZS output start Refutation % 1.47/1.65 1[0:Inp] || -> arboreal(skc3)*. % 1.47/1.65 3[0:Inp] || -> atomic(tptp4)*. % 1.47/1.65 6[0:Inp] || -> atomic(tptp3)*. % 1.47/1.65 7[0:Inp] || -> subactivity_occurrence(skc3,skc2)*. % 1.47/1.65 8[0:Inp] || -> occurrence_of(skc2,tptp0)*. % 1.47/1.65 11[0:Inp] || leaf_occ(skc3,skc2)* -> . % 1.47/1.65 13[0:Inp] || equal(tptp4,tptp3)** -> . % 1.47/1.65 16[0:Inp] || equal(tptp1,tptp3)** -> . % 1.47/1.65 17[0:Inp] || equal(tptp2,tptp3)** -> . % 1.47/1.65 23[0:Inp] || occurrence_of(u,v)* -> activity(v). % 1.47/1.65 24[0:Inp] || occurrence_of(u,v)* -> activity_occurrence(u). % 1.47/1.65 25[0:Inp] || subactivity_occurrence(u,v)* -> activity_occurrence(u). % 1.47/1.65 28[0:Inp] || precedes(u,v)* -> legal(v). % 1.47/1.65 30[0:Inp] activity_occurrence(u) || -> occurrence_of(u,skf23(u))*. % 1.47/1.65 38[0:Inp] || min_precedes(u,v,w)* -> precedes(u,v). % 1.47/1.65 45[0:Inp] atomic(u) || occurrence_of(v,u)* -> arboreal(v). % 1.47/1.65 51[0:Inp] || next_subocc(u,v,w)* -> min_precedes(u,v,w). % 1.47/1.65 56[0:Inp] || min_precedes(u,v,w) -> occurrence_of(skf21(v,u,w),w)*. % 1.47/1.65 58[0:Inp] || min_precedes(u,v,w)*+ -> subactivity_occurrence(v,skf21(v,x,y))*. % 1.47/1.65 61[0:Inp] || occurrence_of(u,v)*+ occurrence_of(u,w)* -> equal(w,v)*. % 1.47/1.65 64[0:Inp] || leaf_occ(u,v)* occurrence_of(v,w)* min_precedes(u,x,w)*+ -> . % 1.47/1.65 79[0:Inp] arboreal(u) || subactivity_occurrence(u,v) occurrence_of(v,tptp0) -> occurrence_of(skf36(w),tptp3)* leaf_occ(u,v)*. % 1.47/1.65 80[0:Inp] arboreal(u) || subactivity_occurrence(u,v) occurrence_of(v,tptp0) -> occurrence_of(skf34(w),tptp4)* leaf_occ(u,v)*. % 1.47/1.65 81[0:Inp] arboreal(u) || subactivity_occurrence(u,v)+ occurrence_of(v,tptp0) -> leaf_occ(u,v)* next_subocc(u,skf36(u),tptp0)*. % 1.47/1.65 83[0:Inp] arboreal(u) || subactivity_occurrence(u,v)+ occurrence_of(v,tptp0) -> leaf_occ(u,v)* min_precedes(skf36(u),skf34(u),tptp0)*. % 1.47/1.65 84[0:Inp] arboreal(u) || subactivity_occurrence(u,v) occurrence_of(v,tptp0) -> occurrence_of(skf32(w),tptp1) occurrence_of(skf32(w),tptp2)* leaf_occ(u,v)*. % 1.47/1.65 86[0:Inp] arboreal(u) || subactivity_occurrence(u,v) occurrence_of(v,tptp0) min_precedes(skf36(u),w,tptp0)*+ -> leaf_occ(u,v)* equal(w,skf32(u)) equal(w,skf34(u)). % 1.47/1.65 129[0:Res:7.0,86.1] arboreal(skc3) || min_precedes(skf36(skc3),u,tptp0)* occurrence_of(skc2,tptp0) -> equal(u,skf34(skc3)) equal(u,skf32(skc3)) leaf_occ(skc3,skc2). % 1.47/1.65 130[0:Res:7.0,84.1] arboreal(skc3) || occurrence_of(skc2,tptp0) -> occurrence_of(skf32(u),tptp1) occurrence_of(skf32(u),tptp2)* leaf_occ(skc3,skc2). % 1.47/1.65 131[0:Res:7.0,83.1] arboreal(skc3) || occurrence_of(skc2,tptp0) -> min_precedes(skf36(skc3),skf34(skc3),tptp0)* leaf_occ(skc3,skc2). % 1.47/1.65 133[0:Res:7.0,81.1] arboreal(skc3) || occurrence_of(skc2,tptp0) -> next_subocc(skc3,skf36(skc3),tptp0)* leaf_occ(skc3,skc2). % 1.47/1.65 134[0:Res:7.0,79.1] arboreal(skc3) || occurrence_of(skc2,tptp0) -> occurrence_of(skf36(u),tptp3)* leaf_occ(skc3,skc2). % 1.47/1.65 135[0:Res:7.0,80.1] arboreal(skc3) || occurrence_of(skc2,tptp0) -> occurrence_of(skf34(u),tptp4)* leaf_occ(skc3,skc2). % 1.47/1.65 136[0:Res:7.0,25.0] || -> activity_occurrence(skc3)*. % 1.47/1.65 159[0:MRR:134.0,134.1,134.3,1.0,8.0,11.0] || -> occurrence_of(skf36(u),tptp3)*. % 1.47/1.65 160[0:MRR:135.0,135.1,135.3,1.0,8.0,11.0] || -> occurrence_of(skf34(u),tptp4)*. % 1.47/1.65 161[0:MRR:133.0,133.1,133.3,1.0,8.0,11.0] || -> next_subocc(skc3,skf36(skc3),tptp0)*. % 1.47/1.65 162[0:MRR:131.0,131.1,131.3,1.0,8.0,11.0] || -> min_precedes(skf36(skc3),skf34(skc3),tptp0)*. % 1.47/1.65 164[0:MRR:130.0,130.1,130.4,1.0,8.0,11.0] || -> occurrence_of(skf32(u),tptp2)* occurrence_of(skf32(u),tptp1). % 1.47/1.65 166[0:MRR:129.0,129.2,129.5,1.0,8.0,11.0] || min_precedes(skf36(skc3),u,tptp0)* -> equal(u,skf32(skc3)) equal(u,skf34(skc3)). % 1.47/1.65 205[0:Res:160.0,23.0] || -> activity(tptp4)*. % 1.47/1.65 206[0:Res:159.0,23.0] || -> activity(tptp3)*. % 1.47/1.65 213[0:Res:160.0,24.0] || -> activity_occurrence(skf34(u))*. % 1.47/1.65 214[0:Res:159.0,24.0] || -> activity_occurrence(skf36(u))*. % 1.47/1.65 247[0:Res:160.0,45.1] atomic(tptp4) || -> arboreal(skf34(u))*. % 1.47/1.65 248[0:Res:159.0,45.1] atomic(tptp3) || -> arboreal(skf36(u))*. % 1.47/1.65 252[0:SSi:247.0,3.0,205.0] || -> arboreal(skf34(u))*. % 1.47/1.65 253[0:SSi:248.0,6.0,206.0] || -> arboreal(skf36(u))*. % 1.47/1.65 321[0:Res:161.0,51.0] || -> min_precedes(skc3,skf36(skc3),tptp0)*. % 1.47/1.65 324[0:Res:321.0,38.0] || -> precedes(skc3,skf36(skc3))*. % 1.47/1.65 327[0:Res:324.0,28.0] || -> legal(skf36(skc3))*. % 1.47/1.65 374[0:Res:160.0,61.0] || occurrence_of(skf34(u),v)* -> equal(v,tptp4). % 1.47/1.65 375[0:Res:159.0,61.0] || occurrence_of(skf36(u),v)* -> equal(v,tptp3). % 1.47/1.65 376[0:Res:30.1,61.0] activity_occurrence(u) || occurrence_of(u,v)* -> equal(v,skf23(u)). % 1.47/1.65 378[0:Res:164.0,61.0] || occurrence_of(skf32(u),v)*+ -> occurrence_of(skf32(u),tptp1)* equal(v,tptp2). % 1.47/1.65 382[0:MRR:376.0,24.1] || occurrence_of(u,v)* -> equal(v,skf23(u)). % 1.47/1.65 384[0:Res:30.1,374.0] activity_occurrence(skf34(u)) || -> equal(skf23(skf34(u)),tptp4)**. % 1.47/1.65 388[0:SSi:384.0,213.0,252.0] || -> equal(skf23(skf34(u)),tptp4)**. % 1.47/1.65 394[0:Res:30.1,375.0] activity_occurrence(skf36(u)) || -> equal(skf23(skf36(u)),tptp3)**. % 1.47/1.65 398[0:SSi:394.0,214.0,253.0] || -> equal(skf23(skf36(u)),tptp3)**. % 1.47/1.65 458[0:Res:321.0,58.0] || -> subactivity_occurrence(skf36(skc3),skf21(skf36(skc3),u,v))*. % 1.47/1.65 487[0:Res:164.0,382.0] || -> occurrence_of(skf32(u),tptp1)* equal(skf23(skf32(u)),tptp2). % 1.47/1.65 547[0:Res:162.0,64.2] || leaf_occ(skf36(skc3),u)* occurrence_of(u,tptp0) -> . % 1.47/1.65 576[0:Res:487.0,23.0] || -> equal(skf23(skf32(u)),tptp2)** activity(tptp1). % 1.47/1.65 578[1:Spt:576.0] || -> equal(skf23(skf32(u)),tptp2)**. % 1.47/1.65 877[0:Res:458.0,81.1] arboreal(skf36(skc3)) || occurrence_of(skf21(skf36(skc3),u,v),tptp0) -> leaf_occ(skf36(skc3),skf21(skf36(skc3),u,v))* next_subocc(skf36(skc3),skf36(skf36(skc3)),tptp0). % 1.47/1.65 879[0:SSi:877.0,327.0,214.0,1.0,136.0,253.0,1.0,136.0] || occurrence_of(skf21(skf36(skc3),u,v),tptp0) -> leaf_occ(skf36(skc3),skf21(skf36(skc3),u,v))* next_subocc(skf36(skc3),skf36(skf36(skc3)),tptp0). % 1.47/1.65 880[0:MRR:879.1,547.0] || occurrence_of(skf21(skf36(skc3),u,v),tptp0)*+ -> next_subocc(skf36(skc3),skf36(skf36(skc3)),tptp0)*. % 1.47/1.65 3148[0:Res:56.1,880.0] || min_precedes(u,skf36(skc3),tptp0)*+ -> next_subocc(skf36(skc3),skf36(skf36(skc3)),tptp0)*. % 1.47/1.65 3150[0:Res:321.0,3148.0] || -> next_subocc(skf36(skc3),skf36(skf36(skc3)),tptp0)*. % 1.47/1.65 3159[0:Res:3150.0,51.0] || -> min_precedes(skf36(skc3),skf36(skf36(skc3)),tptp0)*. % 1.47/1.65 3188[0:Res:3159.0,166.0] || -> equal(skf36(skf36(skc3)),skf32(skc3)) equal(skf36(skf36(skc3)),skf34(skc3))**. % 1.47/1.65 3372[2:Spt:3188.0] || -> equal(skf36(skf36(skc3)),skf32(skc3))**. % 1.47/1.65 3478[2:SpR:3372.0,398.0] || -> equal(skf23(skf32(skc3)),tptp3)**. % 1.47/1.65 3489[2:Rew:578.0,3478.0] || -> equal(tptp2,tptp3)**. % 1.47/1.65 3490[2:MRR:3489.0,17.0] || -> . % 1.47/1.65 3497[2:Spt:3490.0,3188.0,3372.0] || equal(skf36(skf36(skc3)),skf32(skc3))** -> . % 1.47/1.65 3498[2:Spt:3490.0,3188.1] || -> equal(skf36(skf36(skc3)),skf34(skc3))**. % 1.47/1.65 3586[2:SpR:3498.0,398.0] || -> equal(skf23(skf34(skc3)),tptp3)**. % 1.47/1.65 3598[2:Rew:388.0,3586.0] || -> equal(tptp4,tptp3)**. % 1.47/1.65 3599[2:MRR:3598.0,13.0] || -> . % 1.47/1.65 3606[1:Spt:3599.0,576.1] || -> activity(tptp1)*. % 1.47/1.65 4165[2:Spt:3188.0] || -> equal(skf36(skf36(skc3)),skf32(skc3))**. % 1.47/1.65 4268[2:SpR:4165.0,159.0] || -> occurrence_of(skf32(skc3),tptp3)*. % 1.47/1.65 4271[2:SpR:4165.0,398.0] || -> equal(skf23(skf32(skc3)),tptp3)**. % 1.47/1.65 4306[2:Res:4268.0,378.0] || -> occurrence_of(skf32(skc3),tptp1)* equal(tptp2,tptp3). % 1.47/1.65 4307[2:MRR:4306.1,17.0] || -> occurrence_of(skf32(skc3),tptp1)*. % 1.47/1.65 4311[2:Res:4307.0,382.0] || -> equal(skf23(skf32(skc3)),tptp1)**. % 1.47/1.65 4322[2:Rew:4271.0,4311.0] || -> equal(tptp1,tptp3)**. % 1.47/1.65 4323[2:MRR:4322.0,16.0] || -> . % 1.47/1.65 4325[2:Spt:4323.0,3188.0,4165.0] || equal(skf36(skf36(skc3)),skf32(skc3))** -> . % 1.47/1.65 4326[2:Spt:4323.0,3188.1] || -> equal(skf36(skf36(skc3)),skf34(skc3))**. % 1.47/1.65 4411[2:SpR:4326.0,398.0] || -> equal(skf23(skf34(skc3)),tptp3)**. % 1.47/1.65 4428[2:Rew:388.0,4411.0] || -> equal(tptp4,tptp3)**. % 1.47/1.65 4429[2:MRR:4428.0,13.0] || -> . % 1.47/1.65 % SZS output end Refutation % 1.47/1.65 Formulae used in the proof : goals sos_35 sos_38 sos_39 sos_42 sos_43 sos_03 sos_11 sos_21 sos_12 sos_24 sos_16 sos_26 sos_06 sos_08 sos_09 sos_32 % 1.47/1.65 %------------------------------------------------------------------------------