%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : GRA006+1 : TPTP v8.1.0. Bugfixed v3.2.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n018.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 : Sat Jul 16 07:22:09 EDT 2022 % Result : Theorem 0.49s 0.66s % Output : Refutation 0.49s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : GRA006+1 : TPTP v8.1.0. Bugfixed v3.2.0. % 0.03/0.12 % Command : run_spass %d %s % 0.14/0.33 % Computer : n018.cluster.edu % 0.14/0.33 % Model : x86_64 x86_64 % 0.14/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.33 % Memory : 8042.1875MB % 0.14/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.33 % CPULimit : 300 % 0.14/0.33 % WCLimit : 600 % 0.14/0.33 % DateTime : Tue May 31 02:12:57 EDT 2022 % 0.14/0.34 % CPUTime : % 0.49/0.66 % 0.49/0.66 SPASS V 3.9 % 0.49/0.66 SPASS beiseite: Proof found. % 0.49/0.66 % SZS status Theorem % 0.49/0.66 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.49/0.66 SPASS derived 990 clauses, backtracked 155 clauses, performed 13 splits and kept 654 clauses. % 0.49/0.66 SPASS allocated 98734 KBytes. % 0.49/0.66 SPASS spent 0:00:00.31 on the problem. % 0.49/0.66 0:00:00.03 for the input. % 0.49/0.66 0:00:00.07 for the FLOTTER CNF translation. % 0.49/0.66 0:00:00.02 for inferences. % 0.49/0.66 0:00:00.00 for the backtracking. % 0.49/0.66 0:00:00.15 for the reduction. % 0.49/0.66 % 0.49/0.66 % 0.49/0.66 Here is a proof with depth 5, length 86 : % 0.49/0.66 % SZS output start Refutation % 0.49/0.66 1[0:Inp] || -> complete*. % 0.49/0.66 2[0:Inp] || -> edge(skc11)*. % 0.49/0.66 4[0:Inp] || -> precedes(skc9,skc8,skc7)*. % 0.49/0.66 5[0:Inp] || -> shortest_path(skc12,skc13,skc7)*. % 0.49/0.66 6[0:Inp] || -> edge(skf12(u,v))*. % 0.49/0.66 8[0:Inp] edge(u) || -> vertex(head_of(u))*. % 0.49/0.66 9[0:Inp] edge(u) || -> vertex(tail_of(u))*. % 0.49/0.66 24[0:Inp] || SkP0(u,v,w)* -> equal(w,head_of(v)). % 0.49/0.66 25[0:Inp] || SkP0(u,v,w)* -> equal(u,tail_of(v)). % 0.49/0.66 28[0:Inp] || shortest_path(u,v,w)* -> path(u,v,w). % 0.49/0.66 32[0:Inp] || on_path(u,v)* path(w,x,v)*+ -> edge(u). % 0.49/0.66 38[0:Inp] || precedes(u,v,w)*+ path(x,y,w)* -> on_path(u,w). % 0.49/0.66 39[0:Inp] || precedes(u,v,w)*+ path(x,y,w)* -> on_path(v,w). % 0.49/0.66 49[0:Inp] edge(u) edge(v) || equal(head_of(u),tail_of(v)) -> sequential(u,v)* equal(u,v). % 0.49/0.66 54[0:Inp] edge(u) || equal(head_of(u),tail_of(skc9))**+ equal(tail_of(u),head_of(skc8))* -> equal(head_of(skc11),head_of(skc8))**. % 0.49/0.66 55[0:Inp] edge(u) || equal(head_of(u),tail_of(skc9))**+ equal(tail_of(u),head_of(skc8))* -> equal(tail_of(skc11),tail_of(skc9)). % 0.49/0.66 62[0:Inp] || equal(head_of(u),head_of(v))*+ equal(tail_of(u),tail_of(w))* shortest_path(x,y,z)* precedes(w,v,z)* -> . % 0.49/0.66 65[0:Inp] vertex(u) vertex(v) || complete -> equal(tail_of(skf12(u,v)),u) equal(u,v) SkP0(v,skf12(u,v),u)*. % 0.49/0.66 66[0:Inp] vertex(u) vertex(v) || complete -> equal(head_of(skf12(u,v)),v) equal(u,v) SkP0(v,skf12(u,v),u)*. % 0.49/0.66 68[0:Inp] || sequential(u,v)* precedes(v,w,x)* path(y,z,x)* on_path(u,x) on_path(w,x) -> precedes(u,w,x)*. % 0.49/0.66 73[0:MRR:65.2,1.0] vertex(u) vertex(v) || -> equal(v,u) equal(tail_of(skf12(v,u)),v) SkP0(u,skf12(v,u),v)*. % 0.49/0.66 74[0:MRR:66.2,1.0] vertex(u) vertex(v) || -> equal(v,u) equal(head_of(skf12(v,u)),u) SkP0(u,skf12(v,u),v)*. % 0.49/0.66 76[0:MRR:68.4,39.2] || on_path(u,v) sequential(u,w)* path(x,y,v)*+ precedes(w,z,v)* -> precedes(u,z,v)*. % 0.49/0.66 100[0:Res:2.0,9.0] || -> vertex(tail_of(skc11))*. % 0.49/0.66 101[0:Res:5.0,28.0] || -> path(skc12,skc13,skc7)*. % 0.49/0.66 105[0:Res:5.0,62.3] || equal(head_of(u),head_of(v))*+ equal(tail_of(u),tail_of(w))* precedes(w,v,skc7)* -> . % 0.49/0.66 108[0:Res:4.0,38.1] || path(u,v,skc7)* -> on_path(skc9,skc7). % 0.49/0.66 109[0:Res:4.0,39.1] || path(u,v,skc7)* -> on_path(skc8,skc7). % 0.49/0.66 112[0:Res:4.0,76.1] || on_path(u,skc7) sequential(u,skc9) path(v,w,skc7)*+ -> precedes(u,skc8,skc7)*. % 0.49/0.66 149[0:Res:4.0,105.2] || equal(head_of(u),head_of(skc8))* equal(tail_of(u),tail_of(skc9)) -> . % 0.49/0.66 159[1:Spt:55.3] || -> equal(tail_of(skc11),tail_of(skc9))**. % 0.49/0.66 162[1:Rew:159.0,100.0] || -> vertex(tail_of(skc9))*. % 0.49/0.66 168[2:Spt:54.0,54.1,54.2] edge(u) || equal(head_of(u),tail_of(skc9))**+ equal(tail_of(u),head_of(skc8))* -> . % 0.49/0.66 193[0:Res:101.0,109.0] || -> on_path(skc8,skc7)*. % 0.49/0.66 194[0:Res:101.0,108.0] || -> on_path(skc9,skc7)*. % 0.49/0.66 202[0:Res:101.0,32.1] || on_path(u,skc7)* -> edge(u). % 0.49/0.66 203[0:Res:193.0,202.0] || -> edge(skc8)*. % 0.49/0.66 204[0:Res:194.0,202.0] || -> edge(skc9)*. % 0.49/0.66 207[0:EqR:149.0] || equal(tail_of(skc9),tail_of(skc8))** -> . % 0.49/0.66 276[0:Res:101.0,112.2] || on_path(u,skc7) sequential(u,skc9) -> precedes(u,skc8,skc7)*. % 0.49/0.66 289[0:EqR:105.0] || equal(tail_of(u),tail_of(v)) precedes(v,u,skc7)* -> . % 0.49/0.66 304[0:Res:276.2,289.1] || on_path(u,skc7)* sequential(u,skc9) equal(tail_of(skc8),tail_of(u)) -> . % 0.49/0.66 305[0:Res:193.0,304.0] || sequential(skc8,skc9)* equal(tail_of(skc8),tail_of(skc8)) -> . % 0.49/0.66 308[0:Obv:305.1] || sequential(skc8,skc9)* -> . % 0.49/0.66 345[0:Res:74.4,24.0] vertex(u) vertex(v) || -> equal(v,u) equal(head_of(skf12(v,u)),u)** equal(head_of(skf12(v,u)),v)**. % 0.49/0.66 346[0:Res:74.4,25.0] vertex(u) vertex(v) || -> equal(v,u) equal(head_of(skf12(v,u)),u)** equal(tail_of(skf12(v,u)),u). % 0.49/0.66 356[0:Res:73.4,24.0] vertex(u) vertex(v) || -> equal(v,u) equal(tail_of(skf12(v,u)),v) equal(head_of(skf12(v,u)),v)**. % 0.49/0.66 391[0:SpL:345.3,149.0] vertex(u) vertex(v) || equal(u,head_of(skc8)) equal(tail_of(skf12(v,u)),tail_of(skc9)) -> equal(v,u) equal(head_of(skf12(v,u)),v)**. % 0.49/0.66 395[2:SpL:345.4,168.1] vertex(u) vertex(v) edge(skf12(v,u)) || equal(v,tail_of(skc9)) equal(tail_of(skf12(v,u)),head_of(skc8)) -> equal(v,u) equal(head_of(skf12(v,u)),u)**. % 0.49/0.66 397[0:SpL:345.4,149.0] vertex(u) vertex(v) || equal(v,head_of(skc8)) equal(tail_of(skf12(v,u)),tail_of(skc9)) -> equal(v,u) equal(head_of(skf12(v,u)),u)**. % 0.49/0.66 406[0:Rew:346.4,397.3] vertex(u) vertex(v) || equal(v,head_of(skc8)) equal(u,tail_of(skc9)) -> equal(v,u) equal(head_of(skf12(v,u)),u)**. % 0.49/0.66 407[0:Rew:356.3,391.3] vertex(u) vertex(v) || equal(u,head_of(skc8)) equal(v,tail_of(skc9)) -> equal(v,u) equal(head_of(skf12(v,u)),v)**. % 0.49/0.66 410[2:Rew:346.4,395.4] vertex(u) vertex(v) edge(skf12(v,u)) || equal(v,tail_of(skc9)) equal(u,head_of(skc8)) -> equal(v,u) equal(head_of(skf12(v,u)),u)**. % 0.49/0.66 411[2:Rew:407.5,410.6] vertex(u) vertex(v) edge(skf12(v,u)) || equal(v,tail_of(skc9))* equal(u,head_of(skc8))* -> equal(v,u)* equal(v,u)*. % 0.49/0.66 412[2:Obv:411.5] vertex(u) vertex(v) edge(skf12(v,u)) || equal(v,tail_of(skc9))* equal(u,head_of(skc8))* -> equal(v,u)*. % 0.49/0.66 413[2:SSi:412.2,6.0] vertex(u) vertex(v) || equal(v,tail_of(skc9))*+ equal(u,head_of(skc8))* -> equal(v,u)*. % 0.49/0.66 648[2:EqR:413.2] vertex(u) vertex(tail_of(skc9)) || equal(u,head_of(skc8))* -> equal(tail_of(skc9),u). % 0.49/0.66 649[2:SSi:648.1,162.0] vertex(u) || equal(u,head_of(skc8))* -> equal(tail_of(skc9),u). % 0.49/0.66 650[2:EqR:649.1] vertex(head_of(skc8)) || -> equal(head_of(skc8),tail_of(skc9))**. % 0.49/0.66 651[2:SSi:650.0,8.0,203.1] || -> equal(head_of(skc8),tail_of(skc9))**. % 0.49/0.66 664[0:Res:49.3,308.0] edge(skc8) edge(skc9) || equal(head_of(skc8),tail_of(skc9))** -> equal(skc9,skc8). % 0.49/0.66 665[2:Rew:651.0,664.2] edge(skc8) edge(skc9) || equal(tail_of(skc9),tail_of(skc9))* -> equal(skc9,skc8). % 0.49/0.66 666[2:Obv:665.2] edge(skc8) edge(skc9) || -> equal(skc9,skc8)**. % 0.49/0.66 667[2:SSi:666.1,666.0,204.0,203.0] || -> equal(skc9,skc8)**. % 0.49/0.66 674[2:Rew:667.0,207.0] || equal(tail_of(skc8),tail_of(skc8))* -> . % 0.49/0.66 734[2:Obv:674.0] || -> . % 0.49/0.66 747[2:Spt:734.0,54.3] || -> equal(head_of(skc11),head_of(skc8))**. % 0.49/0.66 993[2:SpL:747.0,149.0] || equal(head_of(skc8),head_of(skc8))* equal(tail_of(skc11),tail_of(skc9)) -> . % 0.49/0.66 999[2:Obv:993.0] || equal(tail_of(skc11),tail_of(skc9))** -> . % 0.49/0.66 1000[2:Rew:159.0,999.0] || equal(tail_of(skc9),tail_of(skc9))* -> . % 0.49/0.66 1001[2:Obv:1000.0] || -> . % 0.49/0.66 1006[1:Spt:1001.0,55.3,159.0] || equal(tail_of(skc11),tail_of(skc9))** -> . % 0.49/0.66 1007[1:Spt:1001.0,55.0,55.1,55.2] edge(u) || equal(head_of(u),tail_of(skc9))**+ equal(tail_of(u),head_of(skc8))* -> . % 0.49/0.66 1008[0:SSi:664.1,664.0,204.0,203.0] || equal(head_of(skc8),tail_of(skc9))** -> equal(skc9,skc8). % 0.49/0.66 1012[1:SpL:345.3,1007.1] vertex(u) vertex(v) edge(skf12(v,u)) || equal(u,tail_of(skc9)) equal(tail_of(skf12(v,u)),head_of(skc8)) -> equal(v,u) equal(head_of(skf12(v,u)),v)**. % 0.49/0.66 1017[1:Rew:406.5,1012.6,356.3,1012.4] vertex(u) vertex(v) edge(skf12(v,u)) || equal(u,tail_of(skc9))* equal(v,head_of(skc8))* -> equal(v,u)* equal(u,v)*. % 0.49/0.66 1018[1:Obv:1017.5] vertex(u) vertex(v) edge(skf12(v,u)) || equal(u,tail_of(skc9))* equal(v,head_of(skc8))* -> equal(u,v)*. % 0.49/0.66 1019[1:SSi:1018.2,6.0] vertex(u) vertex(v) || equal(u,tail_of(skc9))*+ equal(v,head_of(skc8))* -> equal(u,v)*. % 0.49/0.66 1282[1:EqR:1019.2] vertex(tail_of(skc9)) vertex(u) || equal(u,head_of(skc8))* -> equal(tail_of(skc9),u). % 0.49/0.66 1283[1:SSi:1282.0,9.0,204.1] vertex(u) || equal(u,head_of(skc8))* -> equal(tail_of(skc9),u). % 0.49/0.66 1284[1:EqR:1283.1] vertex(head_of(skc8)) || -> equal(head_of(skc8),tail_of(skc9))**. % 0.49/0.66 1285[1:SSi:1284.0,8.0,203.1] || -> equal(head_of(skc8),tail_of(skc9))**. % 0.49/0.66 1297[1:Rew:1285.0,1008.0] || equal(tail_of(skc9),tail_of(skc9))* -> equal(skc9,skc8). % 0.49/0.66 1298[1:Obv:1297.0] || -> equal(skc9,skc8)**. % 0.49/0.66 1301[1:Rew:1298.0,207.0] || equal(tail_of(skc8),tail_of(skc8))* -> . % 0.49/0.66 1341[1:Obv:1301.0] || -> . % 0.49/0.66 % SZS output end Refutation % 0.49/0.66 Formulae used in the proof : edge_some_way shortest_path_defn path_properties complete_properties edge_ends_are_vertices on_path_properties precedes_properties sequential_defn shortest_path_properties precedes_defn % 0.49/0.66 %------------------------------------------------------------------------------