%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : ITP006+2 : TPTP v8.1.0. Bugfixed v7.5.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n021.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 : Sun Jul 17 00:37:31 EDT 2022 % Result : Theorem 12.73s 12.95s % Output : Refutation 13.31s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : ITP006+2 : TPTP v8.1.0. Bugfixed v7.5.0. % 0.14/0.13 % Command : run_spass %d %s % 0.14/0.34 % Computer : n021.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 600 % 0.14/0.34 % DateTime : Thu Jun 2 20:55:17 EDT 2022 % 0.14/0.34 % CPUTime : % 12.73/12.95 % 12.73/12.95 SPASS V 3.9 % 12.73/12.95 SPASS beiseite: Proof found. % 12.73/12.95 % SZS status Theorem % 12.73/12.95 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 12.73/12.95 SPASS derived 12782 clauses, backtracked 4947 clauses, performed 101 splits and kept 9959 clauses. % 12.73/12.95 SPASS allocated 115917 KBytes. % 12.73/12.95 SPASS spent 0:0:12.58 on the problem. % 12.73/12.95 0:00:00.04 for the input. % 12.73/12.95 0:00:00.45 for the FLOTTER CNF translation. % 12.73/12.95 0:00:00.25 for inferences. % 12.73/12.95 0:00:00.29 for the backtracking. % 12.73/12.95 0:0:11.36 for the reduction. % 12.73/12.95 % 12.73/12.95 % 12.73/12.95 Here is a proof with depth 6, length 101 : % 12.73/12.95 % SZS output start Refutation % 12.73/12.95 1[0:Inp] || -> ne(skc6)*. % 12.73/12.95 2[0:Inp] || -> ne(skc5)*. % 12.73/12.95 3[0:Inp] || -> p(c_2Ebool_2ET)*. % 12.73/12.95 6[0:Inp] || -> mem(c_2Ebool_2ET,bool)*. % 12.73/12.95 7[0:Inp] || -> mem(c_2Ebool_2EF,bool)*. % 12.73/12.95 8[0:Inp] || p(c_2Ebool_2EF)* -> . % 12.73/12.95 9[0:Inp] || -> mem(skc9,arr(skc5,bool))*. % 12.73/12.95 10[0:Inp] || -> mem(skc8,arr(skc5,bool))*. % 12.73/12.95 11[0:Inp] || -> mem(skc7,arr(skc6,skc5))*. % 12.73/12.95 28[0:Inp] || -> p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(skc6,skc5),skc7),skc8))*. % 12.73/12.95 33[0:Inp] || p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(skc6,skc5),skc7),skc9))* -> . % 12.73/12.95 55[0:Inp] ne(u) || -> mem(c_2Ebool_2E_21(u),arr(arr(u,bool),bool))*. % 12.73/12.95 65[0:Inp] || p(ap(skc9,u))* mem(u,skc5) -> p(ap(skc8,u)). % 12.73/12.95 69[0:Inp] || mem(u,v)* mem(w,arr(v,x))*+ -> mem(ap(w,u),x)*. % 12.73/12.95 70[0:Inp] || mem(u,bool)*+ mem(v,bool)* -> p(u) p(v) equal(v,u)*. % 12.73/12.95 77[0:Inp] p(u) p(v) || mem(u,bool)*+ mem(v,bool)* -> equal(v,u)*. % 12.73/12.95 86[0:Inp] ne(u) || mem(v,arr(u,bool))+ -> p(ap(c_2Ebool_2E_21(u),v))* mem(skf14(v,u),u)*. % 12.73/12.95 102[0:Inp] ne(u) || p(ap(c_2Ebool_2E_21(u),v))*+ mem(w,u)* mem(v,arr(u,bool)) -> p(ap(v,w))*. % 12.73/12.95 116[0:Inp] ne(u) ne(v) || mem(w,arr(v,u))+ mem(x,arr(u,bool)) -> p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(v,u),w),x))* mem(skf20(v,y,z),v)*. % 12.73/12.95 124[0:Inp] ne(u) ne(v) || mem(w,arr(v,u))+ mem(x,arr(u,bool)) -> p(ap(x,ap(w,skf20(v,w,x))))* p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(v,u),w),x))*. % 12.73/12.95 130[0:Inp] ne(u) ne(v) || p(ap(w,ap(x,y)))* p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(v,u),x),w))*+ mem(y,v)* mem(x,arr(v,u)) mem(w,arr(u,bool)) -> . % 12.73/12.95 184[0:Res:2.0,55.0] || -> mem(c_2Ebool_2E_21(skc5),arr(arr(skc5,bool),bool))*. % 12.73/12.95 242[0:Res:1.0,116.0] ne(u) || mem(v,arr(u,bool))+ mem(w,arr(skc6,u)) -> p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(skc6,u),w),v))* mem(skf20(skc6,x,y),skc6)*. % 12.73/12.95 301[1:Spt:242.0,242.1,242.2,242.3] ne(u) || mem(v,arr(u,bool)) mem(w,arr(skc6,u)) -> p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(skc6,u),w),v))*. % 12.73/12.95 321[1:Res:301.3,33.0] ne(skc5) || mem(skc9,arr(skc5,bool))* mem(skc7,arr(skc6,skc5)) -> . % 12.73/12.95 322[1:SSi:321.0,2.0] || mem(skc9,arr(skc5,bool))* mem(skc7,arr(skc6,skc5)) -> . % 12.73/12.95 323[1:MRR:322.0,322.1,9.0,11.0] || -> . % 12.73/12.95 324[1:Spt:323.0,242.4] || -> mem(skf20(skc6,u,v),skc6)*. % 12.73/12.95 376[0:Res:7.0,70.0] || mem(u,bool)* -> p(c_2Ebool_2EF) p(u) equal(u,c_2Ebool_2EF). % 12.73/12.95 378[0:MRR:376.1,8.0] || mem(u,bool)* -> p(u) equal(u,c_2Ebool_2EF). % 12.73/12.95 379[0:Res:11.0,69.1] || mem(u,skc6) -> mem(ap(skc7,u),skc5)*. % 12.73/12.95 380[0:Res:10.0,69.1] || mem(u,skc5) -> mem(ap(skc8,u),bool)*. % 12.73/12.95 381[0:Res:9.0,69.1] || mem(u,skc5) -> mem(ap(skc9,u),bool)*. % 12.73/12.95 385[0:Res:184.0,69.1] || mem(u,arr(skc5,bool)) -> mem(ap(c_2Ebool_2E_21(skc5),u),bool)*. % 12.73/12.95 401[0:Res:381.1,378.0] || mem(u,skc5) -> p(ap(skc9,u))* equal(ap(skc9,u),c_2Ebool_2EF). % 12.73/12.95 415[0:Res:385.1,378.0] || mem(u,arr(skc5,bool)) -> p(ap(c_2Ebool_2E_21(skc5),u))* equal(ap(c_2Ebool_2E_21(skc5),u),c_2Ebool_2EF). % 12.73/12.95 423[0:Res:401.1,65.0] || mem(u,skc5) mem(u,skc5) -> equal(ap(skc9,u),c_2Ebool_2EF) p(ap(skc8,u))*. % 12.73/12.95 424[0:Obv:423.0] || mem(u,skc5) -> equal(ap(skc9,u),c_2Ebool_2EF) p(ap(skc8,u))*. % 12.73/12.95 455[0:Res:6.0,77.2] p(c_2Ebool_2ET) p(u) || mem(u,bool)* -> equal(u,c_2Ebool_2ET). % 12.73/12.95 469[0:SSi:455.0,3.0] p(u) || mem(u,bool)* -> equal(u,c_2Ebool_2ET). % 12.73/12.95 470[0:Res:7.0,469.1] p(c_2Ebool_2EF) || -> equal(c_2Ebool_2EF,c_2Ebool_2ET)**. % 12.73/12.95 477[0:Res:380.1,469.1] p(ap(skc8,u)) || mem(u,skc5) -> equal(ap(skc8,u),c_2Ebool_2ET)**. % 12.73/12.95 478[0:Res:381.1,469.1] p(ap(skc9,u)) || mem(u,skc5) -> equal(ap(skc9,u),c_2Ebool_2ET)**. % 12.73/12.95 481[0:Res:385.1,469.1] p(ap(c_2Ebool_2E_21(skc5),u)) || mem(u,arr(skc5,bool))* -> equal(ap(c_2Ebool_2E_21(skc5),u),c_2Ebool_2ET). % 12.73/12.95 620[0:SoR:477.0,424.2] || mem(u,skc5) mem(u,skc5) -> equal(ap(skc8,u),c_2Ebool_2ET) equal(ap(skc9,u),c_2Ebool_2EF)**. % 12.73/12.95 627[0:Obv:620.0] || mem(u,skc5) -> equal(ap(skc8,u),c_2Ebool_2ET) equal(ap(skc9,u),c_2Ebool_2EF)**. % 12.73/12.95 747[0:Res:10.0,86.1] ne(skc5) || -> p(ap(c_2Ebool_2E_21(skc5),skc8))* mem(skf14(skc8,skc5),skc5). % 12.73/12.95 748[0:Res:9.0,86.1] ne(skc5) || -> p(ap(c_2Ebool_2E_21(skc5),skc9))* mem(skf14(skc9,skc5),skc5). % 12.73/12.95 762[0:SSi:747.0,2.0] || -> p(ap(c_2Ebool_2E_21(skc5),skc8))* mem(skf14(skc8,skc5),skc5). % 12.73/12.95 763[0:SSi:748.0,2.0] || -> p(ap(c_2Ebool_2E_21(skc5),skc9))* mem(skf14(skc9,skc5),skc5). % 12.73/12.95 980[0:SoR:481.0,415.1] || mem(u,arr(skc5,bool))* mem(u,arr(skc5,bool))* -> equal(ap(c_2Ebool_2E_21(skc5),u),c_2Ebool_2ET) equal(ap(c_2Ebool_2E_21(skc5),u),c_2Ebool_2EF). % 12.73/12.95 981[0:SoR:481.0,763.0] || mem(skc9,arr(skc5,bool)) -> equal(ap(c_2Ebool_2E_21(skc5),skc9),c_2Ebool_2ET) mem(skf14(skc9,skc5),skc5)*. % 12.73/12.95 982[0:SoR:481.0,762.0] || mem(skc8,arr(skc5,bool)) -> equal(ap(c_2Ebool_2E_21(skc5),skc8),c_2Ebool_2ET) mem(skf14(skc8,skc5),skc5)*. % 12.73/12.95 989[0:MRR:981.0,9.0] || -> equal(ap(c_2Ebool_2E_21(skc5),skc9),c_2Ebool_2ET) mem(skf14(skc9,skc5),skc5)*. % 12.73/12.95 991[0:MRR:982.0,10.0] || -> equal(ap(c_2Ebool_2E_21(skc5),skc8),c_2Ebool_2ET) mem(skf14(skc8,skc5),skc5)*. % 12.73/12.95 995[0:Obv:980.0] || mem(u,arr(skc5,bool))* -> equal(ap(c_2Ebool_2E_21(skc5),u),c_2Ebool_2ET) equal(ap(c_2Ebool_2E_21(skc5),u),c_2Ebool_2EF). % 12.73/12.95 1030[0:Res:10.0,995.0] || -> equal(ap(c_2Ebool_2E_21(skc5),skc8),c_2Ebool_2ET) equal(ap(c_2Ebool_2E_21(skc5),skc8),c_2Ebool_2EF)**. % 12.73/12.95 1178[0:Res:9.0,995.0] || -> equal(ap(c_2Ebool_2E_21(skc5),skc9),c_2Ebool_2ET) equal(ap(c_2Ebool_2E_21(skc5),skc9),c_2Ebool_2EF)**. % 12.73/12.95 1390[0:Res:380.1,70.0] || mem(u,skc5)+ mem(v,bool)* -> p(ap(skc8,u))* p(v) equal(v,ap(skc8,u))*. % 12.73/12.95 1817[2:Spt:989.0] || -> equal(ap(c_2Ebool_2E_21(skc5),skc9),c_2Ebool_2ET)**. % 12.73/12.95 1856[3:Spt:991.0] || -> equal(ap(c_2Ebool_2E_21(skc5),skc8),c_2Ebool_2ET)**. % 12.73/12.95 1881[2:SpL:1817.0,102.1] ne(skc5) || p(c_2Ebool_2ET) mem(u,skc5) mem(skc9,arr(skc5,bool))* -> p(ap(skc9,u))*. % 12.73/12.95 1882[3:SpL:1856.0,102.1] ne(skc5) || p(c_2Ebool_2ET) mem(u,skc5) mem(skc8,arr(skc5,bool))* -> p(ap(skc8,u))*. % 12.73/12.95 1888[3:SSi:1882.0,2.0] || p(c_2Ebool_2ET) mem(u,skc5) mem(skc8,arr(skc5,bool))* -> p(ap(skc8,u))*. % 12.73/12.95 1889[3:MRR:1888.0,1888.2,3.0,10.0] || mem(u,skc5) -> p(ap(skc8,u))*. % 12.73/12.95 1890[3:MRR:477.0,1889.1] || mem(u,skc5) -> equal(ap(skc8,u),c_2Ebool_2ET)**. % 12.73/12.95 1895[2:SSi:1881.0,2.0] || p(c_2Ebool_2ET) mem(u,skc5) mem(skc9,arr(skc5,bool))* -> p(ap(skc9,u))*. % 12.73/12.95 1896[2:MRR:1895.0,1895.2,3.0,9.0] || mem(u,skc5) -> p(ap(skc9,u))*. % 12.73/12.95 1897[2:MRR:478.0,1896.1] || mem(u,skc5) -> equal(ap(skc9,u),c_2Ebool_2ET)**. % 12.73/12.95 9078[0:Res:11.0,124.2] ne(skc5) ne(skc6) || mem(u,arr(skc5,bool)) -> p(ap(u,ap(skc7,skf20(skc6,skc7,u))))* p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(skc6,skc5),skc7),u)). % 12.73/12.95 9759[0:Res:28.0,130.3] ne(skc5) ne(skc6) || p(ap(skc8,ap(skc7,u)))* mem(u,skc6) mem(skc7,arr(skc6,skc5)) mem(skc8,arr(skc5,bool)) -> . % 12.73/12.95 9776[0:SSi:9759.1,9759.0,1.0,2.0] || p(ap(skc8,ap(skc7,u)))* mem(u,skc6) mem(skc7,arr(skc6,skc5)) mem(skc8,arr(skc5,bool)) -> . % 12.73/12.95 9794[0:MRR:9776.2,9776.3,11.0,10.0] || p(ap(skc8,ap(skc7,u)))* mem(u,skc6) -> . % 12.73/12.95 9800[0:SSi:9078.1,9078.0,1.0,2.0] || mem(u,arr(skc5,bool)) -> p(ap(u,ap(skc7,skf20(skc6,skc7,u))))* p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(skc6,skc5),skc7),u)). % 12.73/12.95 9871[3:SpL:1890.1,9794.0] || mem(ap(skc7,u),skc5)* p(c_2Ebool_2ET) mem(u,skc6) -> . % 12.73/12.95 9872[3:MRR:9871.0,9871.1,379.1,3.0] || mem(u,skc6)* -> . % 12.73/12.95 9873[3:UnC:9872.0,324.0] || -> . % 12.73/12.95 9874[3:Spt:9873.0,991.0,1856.0] || equal(ap(c_2Ebool_2E_21(skc5),skc8),c_2Ebool_2ET)** -> . % 12.73/12.95 9875[3:Spt:9873.0,991.1] || -> mem(skf14(skc8,skc5),skc5)*. % 12.73/12.95 9876[3:MRR:1030.0,9874.0] || -> equal(ap(c_2Ebool_2E_21(skc5),skc8),c_2Ebool_2EF)**. % 12.73/12.95 9877[3:Rew:9876.0,9874.0] || equal(c_2Ebool_2EF,c_2Ebool_2ET)** -> . % 12.73/12.95 9879[2:Rew:1897.1,627.2] || mem(u,skc5) -> equal(ap(skc8,u),c_2Ebool_2ET)** equal(c_2Ebool_2EF,c_2Ebool_2ET). % 12.73/12.95 9880[3:MRR:9879.2,9877.0] || mem(u,skc5) -> equal(ap(skc8,u),c_2Ebool_2ET)**. % 12.73/12.95 9945[3:SpL:9880.1,9794.0] || mem(ap(skc7,u),skc5)* p(c_2Ebool_2ET) mem(u,skc6) -> . % 12.73/12.95 9956[3:MRR:9945.0,9945.1,379.1,3.0] || mem(u,skc6)* -> . % 12.73/12.95 9957[3:UnC:9956.0,324.0] || -> . % 13.31/13.47 9963[2:Spt:9957.0,989.0,1817.0] || equal(ap(c_2Ebool_2E_21(skc5),skc9),c_2Ebool_2ET)** -> . % 13.31/13.47 9964[2:Spt:9957.0,989.1] || -> mem(skf14(skc9,skc5),skc5)*. % 13.31/13.47 9965[2:MRR:1178.0,9963.0] || -> equal(ap(c_2Ebool_2E_21(skc5),skc9),c_2Ebool_2EF)**. % 13.31/13.47 9966[2:Rew:9965.0,9963.0] || equal(c_2Ebool_2EF,c_2Ebool_2ET)** -> . % 13.31/13.47 9967[2:MRR:470.1,9966.0] p(c_2Ebool_2EF) || -> . % 13.31/13.47 12357[0:Res:379.1,1390.0] || mem(u,skc6) mem(v,bool)* -> p(ap(skc8,ap(skc7,u)))* p(v) equal(v,ap(skc8,ap(skc7,u)))*. % 13.31/13.47 12366[0:MRR:12357.2,9794.0] || mem(u,skc6)+ mem(v,bool)* -> p(v) equal(v,ap(skc8,ap(skc7,u)))*. % 13.31/13.47 12369[1:Res:324.0,12366.0] || mem(u,bool)*+ -> p(u) equal(u,ap(skc8,ap(skc7,skf20(skc6,v,w))))*. % 13.31/13.47 13190[1:Res:7.0,12369.0] || -> p(c_2Ebool_2EF) equal(ap(skc8,ap(skc7,skf20(skc6,u,v))),c_2Ebool_2EF)**. % 13.31/13.47 13204[2:MRR:13190.0,9967.0] || -> equal(ap(skc8,ap(skc7,skf20(skc6,u,v))),c_2Ebool_2EF)**. % 13.31/13.47 18241[0:SpR:627.2,9800.1] || mem(ap(skc7,skf20(skc6,skc7,skc9)),skc5) mem(skc9,arr(skc5,bool)) -> equal(ap(skc8,ap(skc7,skf20(skc6,skc7,skc9))),c_2Ebool_2ET)** p(c_2Ebool_2EF) p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(skc6,skc5),skc7),skc9)). % 13.31/13.47 18266[2:Rew:13204.0,18241.2] || mem(ap(skc7,skf20(skc6,skc7,skc9)),skc5) mem(skc9,arr(skc5,bool)) -> equal(c_2Ebool_2EF,c_2Ebool_2ET) p(c_2Ebool_2EF) p(ap(ap(c_2EquantHeuristics_2EGUESS__FORALL__POINT(skc6,skc5),skc7),skc9))*. % 13.31/13.47 18267[2:MRR:18266.1,18266.2,18266.3,18266.4,9.0,9966.0,9967.0,33.0] || mem(ap(skc7,skf20(skc6,skc7,skc9)),skc5)* -> . % 13.31/13.47 18280[2:Res:379.1,18267.0] || mem(skf20(skc6,skc7,skc9),skc6)* -> . % 13.31/13.47 18281[2:MRR:18280.0,324.0] || -> . % 13.31/13.47 % SZS output end Refutation % 13.31/13.47 Formulae used in the proof : conj_thm_2EquantHeuristics_2EGUESS__RULES__WEAKEN__FORALL__POINT ax_true_p mem_c_2Ebool_2ET mem_c_2Ebool_2EF ax_false_p mem_c_2Ebool_2E_21 ap_tp boolext ax_all_p conj_thm_2EquantHeuristics_2EGUESS__REWRITES % 13.31/13.47 %------------------------------------------------------------------------------