%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : KRS260+1 : TPTP v8.1.0. Bugfixed v5.4.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n019.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 03:31:00 EDT 2022 % Result : Theorem 7.32s 7.51s % Output : Refutation 7.46s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.12 % Problem : KRS260+1 : TPTP v8.1.0. Bugfixed v5.4.0. % 0.12/0.13 % Command : run_spass %d %s % 0.12/0.34 % Computer : n019.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 : Tue Jun 7 14:42:10 EDT 2022 % 0.12/0.34 % CPUTime : % 7.32/7.51 % 7.32/7.51 SPASS V 3.9 % 7.32/7.51 SPASS beiseite: Proof found. % 7.32/7.51 % SZS status Theorem % 7.32/7.51 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 7.32/7.51 SPASS derived 24739 clauses, backtracked 881 clauses, performed 111 splits and kept 12631 clauses. % 7.32/7.51 SPASS allocated 98639 KBytes. % 7.32/7.51 SPASS spent 0:00:07.15 on the problem. % 7.32/7.51 0:00:00.04 for the input. % 7.32/7.51 0:00:00.20 for the FLOTTER CNF translation. % 7.32/7.51 0:00:00.14 for inferences. % 7.32/7.51 0:00:00.46 for the backtracking. % 7.32/7.51 0:00:06.01 for the reduction. % 7.32/7.51 % 7.32/7.51 % 7.32/7.51 Here is a proof with depth 8, length 384 : % 7.32/7.51 % SZS output start Refutation % 7.32/7.51 1[0:Inp] || -> model(u,skc57)*. % 7.32/7.51 2[0:Inp] || -> model(skc59,skc58)*. % 7.32/7.51 3[0:Inp] || -> model(skc64,skc62)*. % 7.32/7.51 4[0:Inp] || -> model(skc64,skc63)*. % 7.32/7.51 5[0:Inp] || -> model(skc69,skc68)*. % 7.32/7.51 6[0:Inp] || -> model(skc70,skc67)*. % 7.32/7.51 7[0:Inp] || -> model(skc73,skc74)*. % 7.32/7.51 8[0:Inp] || -> model(skc75,skc72)*. % 7.32/7.51 9[0:Inp] || mighta(wec,thm)* -> . % 7.32/7.51 10[0:Inp] || model(skc60,skc58)* -> . % 7.32/7.51 11[0:Inp] || model(u,skc61)* -> . % 7.32/7.51 13[0:Inp] || model(skc71,skc67)* -> . % 7.32/7.51 14[0:Inp] || model(skc73,skc72)* -> . % 7.32/7.51 16[0:Inp] || -> SkP0(u,v) model(v,not__dfg(u))*. % 7.32/7.51 18[0:Inp] || -> model(u,v) model(u,not__dfg(v))*. % 7.32/7.51 19[0:Inp] || model(u,skc68) -> model(u,skc67)*. % 7.32/7.51 20[0:Inp] || model(u,v)*+ -> status__dfg(v,w,unp)*. % 7.32/7.51 23[0:Inp] || model(u,v)*+ -> status__dfg(w,v,sap)*. % 7.32/7.51 24[0:Inp] || status__dfg(u,v,tac)*+ -> model(w,v)*. % 7.32/7.51 25[0:Inp] || status__dfg(u,v,tau)*+ -> model(w,u)*. % 7.32/7.51 26[0:Inp] || status__dfg(u,v,tau)*+ -> model(w,v)*. % 7.32/7.51 27[0:Inp] || status__dfg(u,v,wtc)*+ -> model(w,v)*. % 7.32/7.51 28[0:Inp] || -> model(skf81(u),u)* status__dfg(u,v,cax)*. % 7.32/7.51 29[0:Inp] || status__dfg(u,v,tca)*+ -> model(w,v)*. % 7.32/7.51 30[0:Inp] || status__dfg(u,v,uns)*+ -> model(w,u)*. % 7.32/7.51 32[0:Inp] || -> model(skf61(u,v),v)* status__dfg(v,u,thm). % 7.32/7.51 33[0:Inp] || status__dfg(u,v,eqv)*+ -> model(skf63(u),u)*. % 7.32/7.51 37[0:Inp] || status__dfg(u,v,wtc)*+ -> model(skf75(u),u)*. % 7.32/7.51 39[0:Inp] || model(u,v)* status__dfg(v,w,cax)*+ -> . % 7.32/7.51 41[0:Inp] || status__dfg(u,v,sca)*+ -> model(skf83(v),v)*. % 7.32/7.51 44[0:Inp] || status__dfg(u,v,wca)*+ -> model(skf87(v),v)*. % 7.32/7.51 46[0:Inp] || SkP0(u,v) model(v,not__dfg(u))* -> . % 7.32/7.51 47[0:Inp] || model(u,v) model(u,not__dfg(v))* -> . % 7.32/7.51 50[0:Inp] || model(skf61(u,v),u)*+ -> status__dfg(w,u,thm)*. % 7.32/7.51 56[0:Inp] || model(skf88(u),u)*+ status__dfg(v,u,wca)* -> . % 7.32/7.51 67[0:Inp] || -> nevera(u,v)* status__dfg(skf101(v,w),skf100(v,w),v)*. % 7.32/7.51 69[0:Inp] || model(u,v)*+ model(w,x)* -> status__dfg(x,v,esa)*. % 7.32/7.51 70[0:Inp] || model(u,v)*+ model(u,w)* -> status__dfg(w,v,sat)*. % 7.32/7.51 71[0:Inp] || model(u,v)* status__dfg(v,w,thm)*+ -> model(u,w)*. % 7.32/7.51 73[0:Inp] || model(u,v)* status__dfg(w,v,eqv)*+ -> model(u,w)*. % 7.32/7.51 76[0:Inp] || model(u,v)* status__dfg(w,v,eth)*+ -> model(u,w)*. % 7.32/7.51 78[0:Inp] || model(u,v)*+ -> model(skf82(w),w)* status__dfg(w,v,sca)*. % 7.32/7.51 82[0:Inp] || status__dfg(u,v,w)*+ -> nota(w,x)* status__dfg(u,v,x)*. % 7.32/7.51 85[0:Inp] || model(u,v)* status__dfg(w,v,unp)*+ -> model(skf53(w),w)*. % 7.32/7.51 86[0:Inp] || model(u,v)* status__dfg(v,w,sap)*+ -> model(skf55(w),w)*. % 7.32/7.51 87[0:Inp] || model(u,v)* status__dfg(v,w,esa)*+ -> model(skf58(w),w)*. % 7.32/7.51 88[0:Inp] || model(u,v)* status__dfg(w,v,esa)*+ -> model(skf59(w),w)*. % 7.32/7.51 89[0:Inp] || model(u,v)* model(skf64(w),w)*+ -> status__dfg(v,w,tac)*. % 7.32/7.51 92[0:Inp] || status__dfg(u,v,w)*+ status__dfg(u,v,x)* -> mighta(x,w)*. % 7.32/7.51 96[0:Inp] || nevera(u,v)* status__dfg(w,x,v)*+ status__dfg(w,x,u)* -> . % 7.32/7.51 98[0:Inp] || model(u,v)*+ -> model(w,v)* model(skf86(x),x)* status__dfg(x,v,wca)*. % 7.32/7.51 101[0:Inp] || model(u,v)* model(skf74(w),w)*+ -> model(x,v)* status__dfg(v,w,wtc)*. % 7.32/7.51 109[0:Inp] || model(u,v)* model(w,x)* model(skf66(x,y),x)*+ -> model(w,v)* status__dfg(v,x,wec)*. % 7.32/7.51 112[0:Res:92.2,9.0] || status__dfg(u,v,thm) status__dfg(u,v,wec)* -> . % 7.32/7.51 113[0:Res:19.1,13.0] || model(skc71,skc68)* -> . % 7.32/7.51 115[0:Res:8.0,23.0] || -> status__dfg(u,skc72,sap)*. % 7.32/7.51 122[0:Res:1.0,23.0] || -> status__dfg(u,skc57,sap)*. % 7.32/7.51 129[0:Res:8.0,20.0] || -> status__dfg(skc72,u,unp)*. % 7.32/7.51 136[0:Res:1.0,20.0] || -> status__dfg(skc57,u,unp)*. % 7.32/7.51 138[0:Res:18.1,20.0] || -> model(u,v)* status__dfg(not__dfg(v),w,unp)*. % 7.32/7.51 157[0:Res:28.0,46.1] || SkP0(u,skf81(not__dfg(u)))*+ -> status__dfg(not__dfg(u),v,cax)*. % 7.32/7.51 169[0:Res:28.1,39.1] || model(u,v)*+ -> model(skf81(v),v)*. % 7.32/7.51 182[0:Res:16.1,169.0] || -> SkP0(u,v)* model(skf81(not__dfg(u)),not__dfg(u))*. % 7.32/7.51 208[0:Res:19.1,56.0] || model(skf88(skc67),skc68) status__dfg(u,skc67,wca)* -> . % 7.32/7.51 287[0:Res:182.1,47.1] || model(skf81(not__dfg(u)),u)*+ -> SkP0(u,v)*. % 7.32/7.51 310[0:Res:1.0,287.0] || -> SkP0(skc57,u)*. % 7.32/7.51 334[0:Res:1.0,50.0] || -> status__dfg(u,skc57,thm)*. % 7.32/7.51 335[0:Res:19.1,50.0] || model(skf61(skc67,u),skc68)*+ -> status__dfg(v,skc67,thm)*. % 7.32/7.51 344[0:Res:138.0,335.0] || -> status__dfg(not__dfg(skc68),u,unp)* status__dfg(v,skc67,thm)*. % 7.32/7.51 346[0:Res:32.0,335.0] || -> status__dfg(skc68,skc67,thm)* status__dfg(u,skc67,thm)*. % 7.32/7.51 347[0:Con:346.1] || -> status__dfg(skc68,skc67,thm)*. % 7.32/7.51 348[1:Spt:344.1] || -> status__dfg(u,skc67,thm)*. % 7.32/7.51 495[0:Res:67.1,37.0] || -> nevera(u,wtc)* model(skf75(skf101(wtc,v)),skf101(wtc,v))*. % 7.32/7.51 496[0:Res:67.1,27.0] || -> nevera(u,wtc)* model(v,skf100(wtc,w))*. % 7.32/7.51 501[0:Res:67.1,44.0] || -> nevera(u,wca)* model(skf87(skf100(wca,v)),skf100(wca,v))*. % 7.32/7.51 502[0:Res:67.1,41.0] || -> nevera(u,sca)* model(skf83(skf100(sca,v)),skf100(sca,v))*. % 7.32/7.51 647[0:Res:8.0,78.0] || -> model(skf82(u),u)* status__dfg(u,skc72,sca)*. % 7.32/7.51 649[0:Res:7.0,78.0] || -> model(skf82(u),u)* status__dfg(u,skc74,sca)*. % 7.32/7.51 650[0:Res:6.0,78.0] || -> model(skf82(u),u)* status__dfg(u,skc67,sca)*. % 7.32/7.51 652[0:Res:5.0,78.0] || -> model(skf82(u),u)* status__dfg(u,skc68,sca)*. % 7.32/7.51 654[0:Res:4.0,78.0] || -> model(skf82(u),u)* status__dfg(u,skc63,sca)*. % 7.32/7.51 655[0:Res:3.0,78.0] || -> model(skf82(u),u)* status__dfg(u,skc62,sca)*. % 7.32/7.51 656[0:Res:2.0,78.0] || -> model(skf82(u),u)* status__dfg(u,skc58,sca)*. % 7.32/7.51 657[0:Res:1.0,78.0] || -> model(skf82(u),u)* status__dfg(u,skc57,sca)*. % 7.32/7.51 760[0:Res:1.0,70.0] || model(u,v)*+ -> status__dfg(v,skc57,sat)*. % 7.32/7.51 975[0:Res:647.1,41.0] || -> model(skf82(u),u)* model(skf83(skc72),skc72). % 7.32/7.51 994[0:Res:649.1,41.0] || -> model(skf82(u),u)* model(skf83(skc74),skc74). % 7.32/7.51 1016[0:Res:650.1,41.0] || -> model(skf82(u),u)* model(skf83(skc67),skc67). % 7.32/7.51 1035[0:Res:652.1,41.0] || -> model(skf82(u),u)* model(skf83(skc68),skc68). % 7.32/7.51 1045[1:Res:348.0,71.1] || model(u,v)*+ -> model(u,skc67)*. % 7.32/7.51 1065[1:Res:18.1,1045.0] || -> model(u,v)* model(u,skc67)*. % 7.32/7.51 1111[1:Con:1065.0] || -> model(u,skc67)*. % 7.32/7.51 1112[1:UnC:1111.0,13.0] || -> . % 7.32/7.51 1113[1:Spt:1112.0,344.0] || -> status__dfg(not__dfg(skc68),u,unp)*. % 7.32/7.51 1131[2:Spt:1035.0] || -> model(skf82(u),u)*. % 7.32/7.51 1132[2:UnC:1131.0,11.0] || -> . % 7.32/7.51 1133[2:Spt:1132.0,1035.1] || -> model(skf83(skc68),skc68)*. % 7.32/7.51 1140[0:Res:8.0,69.0] || model(u,v)*+ -> status__dfg(v,skc72,esa)*. % 7.32/7.51 1151[0:Res:1.0,69.0] || model(u,v)*+ -> status__dfg(v,skc57,esa)*. % 7.32/7.51 1200[3:Spt:1016.0] || -> model(skf82(u),u)*. % 7.32/7.51 1201[3:UnC:1200.0,11.0] || -> . % 7.32/7.51 1202[3:Spt:1201.0,1016.1] || -> model(skf83(skc67),skc67)*. % 7.32/7.51 1210[4:Spt:994.0] || -> model(skf82(u),u)*. % 7.32/7.51 1211[4:UnC:1210.0,11.0] || -> . % 7.32/7.51 1212[4:Spt:1211.0,994.1] || -> model(skf83(skc74),skc74)*. % 7.32/7.51 1220[5:Spt:975.0] || -> model(skf82(u),u)*. % 7.32/7.51 1221[5:UnC:1220.0,11.0] || -> . % 7.32/7.51 1222[5:Spt:1221.0,975.1] || -> model(skf83(skc72),skc72)*. % 7.32/7.51 1239[0:Res:654.1,41.0] || -> model(skf82(u),u)* model(skf83(skc63),skc63). % 7.32/7.51 1287[6:Spt:1239.0] || -> model(skf82(u),u)*. % 7.32/7.51 1288[6:UnC:1287.0,11.0] || -> . % 7.32/7.51 1289[6:Spt:1288.0,1239.1] || -> model(skf83(skc63),skc63)*. % 7.32/7.51 1306[0:Res:655.1,41.0] || -> model(skf82(u),u)* model(skf83(skc62),skc62). % 7.32/7.51 1308[7:Spt:1306.0] || -> model(skf82(u),u)*. % 7.32/7.51 1309[7:UnC:1308.0,11.0] || -> . % 7.32/7.51 1310[7:Spt:1309.0,1306.1] || -> model(skf83(skc62),skc62)*. % 7.32/7.51 1327[0:Res:656.1,41.0] || -> model(skf82(u),u)* model(skf83(skc58),skc58). % 7.32/7.51 1375[8:Spt:1327.0] || -> model(skf82(u),u)*. % 7.32/7.51 1376[8:UnC:1375.0,11.0] || -> . % 7.32/7.51 1377[8:Spt:1376.0,1327.1] || -> model(skf83(skc58),skc58)*. % 7.32/7.51 1416[0:Res:8.0,760.0] || -> status__dfg(skc72,skc57,sat)*. % 7.32/7.51 1565[0:Res:129.0,82.0] || -> nota(unp,u) status__dfg(skc72,v,u)*. % 7.32/7.51 1572[0:Res:136.0,82.0] || -> nota(unp,u) status__dfg(skc57,v,u)*. % 7.32/7.51 1587[0:Res:115.0,82.0] || -> nota(sap,u) status__dfg(v,skc72,u)*. % 7.32/7.51 1594[0:Res:122.0,82.0] || -> nota(sap,u) status__dfg(v,skc57,u)*. % 7.32/7.51 1642[0:Res:347.0,82.0] || -> nota(thm,u) status__dfg(skc68,skc67,u)*. % 7.32/7.51 1643[0:Res:1416.0,82.0] || -> nota(sat,u) status__dfg(skc72,skc57,u)*. % 7.32/7.51 1657[0:Res:1642.1,30.0] || -> nota(thm,uns)* model(u,skc68)*. % 7.32/7.51 1658[0:Res:1642.1,29.0] || -> nota(thm,tca)* model(u,skc67)*. % 7.32/7.51 1660[0:Res:1642.1,27.0] || -> nota(thm,wtc)* model(u,skc67)*. % 7.32/7.51 1661[0:Res:1642.1,25.0] || -> nota(thm,tau)* model(u,skc68)*. % 7.32/7.51 1664[0:Res:1642.1,24.0] || -> nota(thm,tac)* model(u,skc67)*. % 7.32/7.51 1706[9:Spt:1657.1] || -> model(u,skc68)*. % 7.32/7.51 1707[9:UnC:1706.0,113.0] || -> . % 7.32/7.51 1708[9:Spt:1707.0,1657.0] || -> nota(thm,uns)*. % 7.32/7.51 1731[10:Spt:1658.1] || -> model(u,skc67)*. % 7.32/7.51 1732[10:UnC:1731.0,13.0] || -> . % 7.32/7.51 1733[10:Spt:1732.0,1658.0] || -> nota(thm,tca)*. % 7.32/7.51 1734[11:Spt:1660.1] || -> model(u,skc67)*. % 7.32/7.51 1735[11:UnC:1734.0,13.0] || -> . % 7.32/7.51 1736[11:Spt:1735.0,1660.0] || -> nota(thm,wtc)*. % 7.32/7.51 1737[12:Spt:1661.1] || -> model(u,skc68)*. % 7.32/7.51 1738[12:UnC:1737.0,113.0] || -> . % 7.32/7.51 1739[12:Spt:1738.0,1661.0] || -> nota(thm,tau)*. % 7.32/7.51 1740[13:Spt:1664.1] || -> model(u,skc67)*. % 7.32/7.51 1741[13:UnC:1740.0,13.0] || -> . % 7.32/7.51 1742[13:Spt:1741.0,1664.0] || -> nota(thm,tac)*. % 7.32/7.51 1743[0:Res:1.0,89.1] || model(u,v)*+ -> status__dfg(v,skc57,tac)*. % 7.32/7.51 1884[0:Res:1643.1,30.0] || -> nota(sat,uns)* model(u,skc72)*. % 7.32/7.51 1888[0:Res:1643.1,25.0] || -> nota(sat,tau)* model(u,skc72)*. % 7.32/7.51 1914[0:Res:1643.1,76.1] || model(u,skc57)* -> nota(sat,eth)* model(u,skc72). % 7.32/7.51 1915[0:Res:1643.1,73.1] || model(u,skc57)* -> nota(sat,eqv)* model(u,skc72). % 7.32/7.51 1934[0:MRR:1914.0,1.0] || -> nota(sat,eth)* model(u,skc72)*. % 7.32/7.51 1935[0:MRR:1915.0,1.0] || -> nota(sat,eqv)* model(u,skc72)*. % 7.32/7.51 1945[14:Spt:1884.1] || -> model(u,skc72)*. % 7.32/7.51 1946[14:UnC:1945.0,14.0] || -> . % 7.32/7.51 1947[14:Spt:1946.0,1884.0] || -> nota(sat,uns)*. % 7.32/7.51 1948[15:Spt:1888.1] || -> model(u,skc72)*. % 7.32/7.51 1949[15:UnC:1948.0,14.0] || -> . % 7.32/7.51 1950[15:Spt:1949.0,1888.0] || -> nota(sat,tau)*. % 7.32/7.51 1984[16:Spt:1934.1] || -> model(u,skc72)*. % 7.32/7.51 1985[16:UnC:1984.0,14.0] || -> . % 7.32/7.51 1986[16:Spt:1985.0,1934.0] || -> nota(sat,eth)*. % 7.32/7.51 1987[17:Spt:1935.1] || -> model(u,skc72)*. % 7.32/7.51 1988[17:UnC:1987.0,14.0] || -> . % 7.32/7.51 1989[17:Spt:1988.0,1935.0] || -> nota(sat,eqv)*. % 7.32/7.51 2765[0:Res:1565.1,30.0] || -> nota(unp,uns)* model(u,skc72)*. % 7.32/7.51 2768[0:Res:1565.1,27.0] || -> nota(unp,wtc)* model(u,v)*. % 7.32/7.51 2770[0:Res:1565.1,26.0] || -> nota(unp,tau)* model(u,v)*. % 7.32/7.51 2772[0:Res:1565.1,24.0] || -> nota(unp,tac)* model(u,v)*. % 7.32/7.51 2906[0:Res:647.1,96.1] || nevera(u,sca) status__dfg(v,skc72,u)* -> model(skf82(v),v)*. % 7.32/7.51 2913[0:Res:657.1,96.1] || nevera(u,sca) status__dfg(v,skc57,u)* -> model(skf82(v),v)*. % 7.32/7.51 2939[18:Spt:2765.1] || -> model(u,skc72)*. % 7.32/7.51 2940[18:UnC:2939.0,14.0] || -> . % 7.32/7.51 2941[18:Spt:2940.0,2765.0] || -> nota(unp,uns)*. % 7.32/7.51 3055[19:Spt:2768.1] || -> model(u,v)*. % 7.32/7.51 3056[19:UnC:3055.0,11.0] || -> . % 7.32/7.51 3057[19:Spt:3056.0,2768.0] || -> nota(unp,wtc)*. % 7.32/7.51 3058[20:Spt:2770.1] || -> model(u,v)*. % 7.32/7.51 3059[20:UnC:3058.0,11.0] || -> . % 7.32/7.51 3060[20:Spt:3059.0,2770.0] || -> nota(unp,tau)*. % 7.32/7.51 3061[21:Spt:2772.1] || -> model(u,v)*. % 7.32/7.51 3062[21:UnC:3061.0,11.0] || -> . % 7.32/7.51 3063[21:Spt:3062.0,2772.0] || -> nota(unp,tac)*. % 7.32/7.51 3096[0:Res:8.0,98.0] || -> model(u,skc72)* model(skf86(v),v)* status__dfg(v,skc72,wca)*. % 7.32/7.51 3100[0:Res:6.0,98.0] || -> model(u,skc67)* model(skf86(v),v)* status__dfg(v,skc67,wca)*. % 7.32/7.51 3103[0:Res:5.0,98.0] || -> model(u,skc68)* model(skf86(v),v)* status__dfg(v,skc68,wca)*. % 7.32/7.51 3111[0:Res:2.0,98.0] || -> model(u,skc58)* model(skf86(v),v)* status__dfg(v,skc58,wca)*. % 7.32/7.51 3615[0:Res:1572.1,71.1] || model(u,skc57)* -> nota(unp,thm)* model(u,v)*. % 7.32/7.51 3616[0:Res:1572.1,87.1] || model(u,skc57)* -> nota(unp,esa) model(skf58(v),v)*. % 7.32/7.51 3617[0:Res:1572.1,86.1] || model(u,skc57)* -> nota(unp,sap) model(skf55(v),v)*. % 7.32/7.51 3639[0:MRR:3615.0,1.0] || -> nota(unp,thm)* model(u,v)*. % 7.32/7.51 3640[0:MRR:3616.0,1.0] || -> nota(unp,esa) model(skf58(u),u)*. % 7.32/7.51 3641[0:MRR:3617.0,1.0] || -> nota(unp,sap) model(skf55(u),u)*. % 7.32/7.51 3642[0:Res:1.0,101.1] || model(u,v)*+ -> model(w,v)* status__dfg(v,skc57,wtc)*. % 7.32/7.51 3664[22:Spt:3639.1] || -> model(u,v)*. % 7.32/7.51 3665[22:UnC:3664.0,11.0] || -> . % 7.32/7.51 3666[22:Spt:3665.0,3639.0] || -> nota(unp,thm)*. % 7.32/7.51 3667[23:Spt:3640.1] || -> model(skf58(u),u)*. % 7.32/7.51 3668[23:UnC:3667.0,11.0] || -> . % 7.32/7.51 3669[23:Spt:3668.0,3640.0] || -> nota(unp,esa)*. % 7.32/7.51 3670[24:Spt:3641.1] || -> model(skf55(u),u)*. % 7.32/7.51 3671[24:UnC:3670.0,11.0] || -> . % 7.32/7.51 3672[24:Spt:3671.0,3641.0] || -> nota(unp,sap)*. % 7.32/7.51 3674[0:Res:1587.1,30.0] || -> nota(sap,uns)* model(u,v)*. % 7.32/7.51 3678[0:Res:1587.1,25.0] || -> nota(sap,tau)* model(u,v)*. % 7.32/7.51 3681[0:Res:1587.1,24.0] || -> nota(sap,tac)* model(u,skc72)*. % 7.32/7.51 3694[0:Res:1587.1,33.0] || -> nota(sap,eqv) model(skf63(u),u)*. % 7.32/7.51 3910[25:Spt:3681.1] || -> model(u,skc72)*. % 7.32/7.51 3911[25:UnC:3910.0,14.0] || -> . % 7.32/7.51 3912[25:Spt:3911.0,3681.0] || -> nota(sap,tac)*. % 7.32/7.51 3913[26:Spt:3674.1] || -> model(u,v)*. % 7.32/7.51 3914[26:UnC:3913.0,11.0] || -> . % 7.32/7.51 3915[26:Spt:3914.0,3674.0] || -> nota(sap,uns)*. % 7.32/7.51 3916[27:Spt:3678.1] || -> model(u,v)*. % 7.32/7.51 3917[27:UnC:3916.0,11.0] || -> . % 7.32/7.51 3918[27:Spt:3917.0,3678.0] || -> nota(sap,tau)*. % 7.32/7.51 3992[28:Spt:3694.1] || -> model(skf63(u),u)*. % 7.32/7.51 3993[28:UnC:3992.0,11.0] || -> . % 7.32/7.51 3994[28:Spt:3993.0,3694.0] || -> nota(sap,eqv)*. % 7.32/7.51 4630[0:Res:1594.1,88.1] || model(u,skc57)* -> nota(sap,esa) model(skf59(v),v)*. % 7.32/7.51 4631[0:Res:1594.1,85.1] || model(u,skc57)* -> nota(sap,unp) model(skf53(v),v)*. % 7.32/7.51 4665[0:MRR:4630.0,1.0] || -> nota(sap,esa) model(skf59(u),u)*. % 7.32/7.51 4666[0:MRR:4631.0,1.0] || -> nota(sap,unp) model(skf53(u),u)*. % 7.32/7.51 4701[29:Spt:4665.1] || -> model(skf59(u),u)*. % 7.32/7.51 4702[29:UnC:4701.0,11.0] || -> . % 7.32/7.51 4703[29:Spt:4702.0,4665.0] || -> nota(sap,esa)*. % 7.32/7.51 4704[30:Spt:4666.1] || -> model(skf53(u),u)*. % 7.32/7.51 4705[30:UnC:4704.0,11.0] || -> . % 7.32/7.51 4706[30:Spt:4705.0,4666.0] || -> nota(sap,unp)*. % 7.32/7.51 4777[0:Res:1.0,109.2] || model(u,v)* model(w,skc57)* -> model(w,v)* status__dfg(v,skc57,wec)*. % 7.32/7.51 4800[0:MRR:4777.1,1.0] || model(u,v)*+ -> model(w,v)* status__dfg(v,skc57,wec)*. % 7.32/7.51 5298[0:Res:8.0,1140.0] || -> status__dfg(skc72,skc72,esa)*. % 7.32/7.51 5311[0:Res:1.0,1140.0] || -> status__dfg(skc57,skc72,esa)*. % 7.32/7.51 5373[0:Res:5298.0,82.0] || -> nota(esa,u) status__dfg(skc72,skc72,u)*. % 7.32/7.51 5494[0:Res:5311.0,82.0] || -> nota(esa,u) status__dfg(skc57,skc72,u)*. % 7.32/7.51 6014[0:Res:8.0,1151.0] || -> status__dfg(skc72,skc57,esa)*. % 7.32/7.51 6019[0:Res:6.0,1151.0] || -> status__dfg(skc67,skc57,esa)*. % 7.32/7.51 6190[0:Res:8.0,1743.0] || -> status__dfg(skc72,skc57,tac)*. % 7.32/7.51 6852[0:Res:6190.0,82.0] || -> nota(tac,u) status__dfg(skc72,skc57,u)*. % 7.32/7.51 8084[0:Res:5373.1,30.0] || -> nota(esa,uns)* model(u,skc72)*. % 7.32/7.51 8087[0:Res:5373.1,27.0] || -> nota(esa,wtc)* model(u,skc72)*. % 7.32/7.51 8088[0:Res:5373.1,25.0] || -> nota(esa,tau)* model(u,skc72)*. % 7.32/7.51 8091[0:Res:5373.1,24.0] || -> nota(esa,tac)* model(u,skc72)*. % 7.32/7.51 8182[31:Spt:8084.1] || -> model(u,skc72)*. % 7.32/7.51 8183[31:UnC:8182.0,14.0] || -> . % 7.32/7.51 8184[31:Spt:8183.0,8084.0] || -> nota(esa,uns)*. % 7.32/7.51 8185[32:Spt:8087.1] || -> model(u,skc72)*. % 7.32/7.51 8186[32:UnC:8185.0,14.0] || -> . % 7.32/7.51 8187[32:Spt:8186.0,8087.0] || -> nota(esa,wtc)*. % 7.32/7.51 8188[33:Spt:8088.1] || -> model(u,skc72)*. % 7.32/7.51 8189[33:UnC:8188.0,14.0] || -> . % 7.32/7.51 8190[33:Spt:8189.0,8088.0] || -> nota(esa,tau)*. % 7.32/7.51 8235[34:Spt:8091.1] || -> model(u,skc72)*. % 7.32/7.51 8236[34:UnC:8235.0,14.0] || -> . % 7.32/7.51 8237[34:Spt:8236.0,8091.0] || -> nota(esa,tac)*. % 7.32/7.51 8808[0:Res:5494.1,71.1] || model(u,skc57)* -> nota(esa,thm)* model(u,skc72). % 7.32/7.51 8824[0:MRR:8808.0,1.0] || -> nota(esa,thm)* model(u,skc72)*. % 7.32/7.51 8825[35:Spt:8824.1] || -> model(u,skc72)*. % 7.32/7.51 8826[35:UnC:8825.0,14.0] || -> . % 7.32/7.51 8827[35:Spt:8826.0,8824.0] || -> nota(esa,thm)*. % 7.32/7.51 12567[0:Res:6852.1,30.0] || -> nota(tac,uns)* model(u,skc72)*. % 7.32/7.51 12571[0:Res:6852.1,25.0] || -> nota(tac,tau)* model(u,skc72)*. % 7.32/7.51 12597[0:Res:6852.1,76.1] || model(u,skc57)* -> nota(tac,eth)* model(u,skc72). % 7.32/7.51 12598[0:Res:6852.1,73.1] || model(u,skc57)* -> nota(tac,eqv)* model(u,skc72). % 7.32/7.51 12624[0:MRR:12597.0,1.0] || -> nota(tac,eth)* model(u,skc72)*. % 7.32/7.51 12625[0:MRR:12598.0,1.0] || -> nota(tac,eqv)* model(u,skc72)*. % 7.32/7.51 12648[36:Spt:12567.1] || -> model(u,skc72)*. % 7.32/7.51 12649[36:UnC:12648.0,14.0] || -> . % 7.32/7.51 12650[36:Spt:12649.0,12567.0] || -> nota(tac,uns)*. % 7.32/7.51 12673[37:Spt:12571.1] || -> model(u,skc72)*. % 7.32/7.51 12674[37:UnC:12673.0,14.0] || -> . % 7.32/7.51 12675[37:Spt:12674.0,12571.0] || -> nota(tac,tau)*. % 7.32/7.51 12676[38:Spt:12624.1] || -> model(u,skc72)*. % 7.32/7.51 12677[38:UnC:12676.0,14.0] || -> . % 7.32/7.51 12678[38:Spt:12677.0,12624.0] || -> nota(tac,eth)*. % 7.32/7.51 12679[39:Spt:12625.1] || -> model(u,skc72)*. % 7.32/7.51 12680[39:UnC:12679.0,14.0] || -> . % 7.32/7.51 12681[39:Spt:12680.0,12625.0] || -> nota(tac,eqv)*. % 7.32/7.51 13109[40:Spt:495.0] || -> nevera(u,wtc)*. % 7.32/7.51 13387[41:Spt:501.0] || -> nevera(u,wca)*. % 7.32/7.51 13393[42:Spt:502.0] || -> nevera(u,sca)*. % 7.32/7.51 13401[42:MRR:2913.0,13393.0] || status__dfg(u,skc57,v)* -> model(skf82(u),u)*. % 7.46/7.63 13419[42:MRR:657.1,13401.0] || -> model(skf82(u),u)*. % 7.46/7.63 13420[42:UnC:13419.0,11.0] || -> . % 7.46/7.63 13421[42:Spt:13420.0,502.1] || -> model(skf83(skf100(sca,u)),skf100(sca,u))*. % 7.46/7.63 14344[0:Res:310.0,157.0] || -> status__dfg(not__dfg(skc57),u,cax)*. % 7.46/7.63 14345[0:Res:14344.0,39.1] || model(u,not__dfg(skc57))* -> . % 7.46/7.63 14963[43:Spt:3096.0] || -> model(u,skc72)*. % 7.46/7.63 14964[43:UnC:14963.0,14.0] || -> . % 7.46/7.63 14965[43:Spt:14964.0,3096.1,3096.2] || -> model(skf86(u),u)* status__dfg(u,skc72,wca)*. % 7.46/7.63 15018[43:Res:14965.1,96.1] || nevera(u,wca) status__dfg(v,skc72,u)* -> model(skf86(v),v)*. % 7.46/7.63 15019[43:MRR:15018.0,13387.0] || status__dfg(u,skc72,v)* -> model(skf86(u),u)*. % 7.46/7.63 15020[43:MRR:14965.1,15019.0] || -> model(skf86(u),u)*. % 7.46/7.63 15023[43:UnC:15020.0,14345.0] || -> . % 7.46/7.63 15025[41:Spt:15023.0,501.1] || -> model(skf87(skf100(wca,u)),skf100(wca,u))*. % 7.46/7.63 15287[42:Spt:502.0] || -> nevera(u,sca)*. % 7.46/7.63 15295[42:MRR:2906.0,15287.0] || status__dfg(u,skc72,v)* -> model(skf82(u),u)*. % 7.46/7.63 15329[42:MRR:647.1,15295.0] || -> model(skf82(u),u)*. % 7.46/7.63 15330[42:UnC:15329.0,14345.0] || -> . % 7.46/7.63 15331[42:Spt:15330.0,502.1] || -> model(skf83(skf100(sca,u)),skf100(sca,u))*. % 7.46/7.63 16130[43:Spt:3100.0] || -> model(u,skc67)*. % 7.46/7.63 16131[43:UnC:16130.0,13.0] || -> . % 7.46/7.63 16132[43:Spt:16131.0,3100.1,3100.2] || -> model(skf86(u),u)* status__dfg(u,skc67,wca)*. % 7.46/7.63 16158[43:Res:16132.0,14345.0] || -> status__dfg(not__dfg(skc57),skc67,wca)*. % 7.46/7.63 16190[43:Res:16158.0,208.1] || model(skf88(skc67),skc68)* -> . % 7.46/7.63 16224[44:Spt:3103.0] || -> model(u,skc68)*. % 7.46/7.63 16225[44:UnC:16224.0,16190.0] || -> . % 7.46/7.63 16226[44:Spt:16225.0,3103.1,3103.2] || -> model(skf86(u),u)* status__dfg(u,skc68,wca)*. % 7.46/7.63 16516[45:Spt:3111.0] || -> model(u,skc58)*. % 7.46/7.63 16517[45:UnC:16516.0,10.0] || -> . % 7.46/7.63 16518[45:Spt:16517.0,3111.1,3111.2] || -> model(skf86(u),u)* status__dfg(u,skc58,wca)*. % 7.46/7.63 16644[46:Spt:3096.0] || -> model(u,skc72)*. % 7.46/7.63 16645[46:UnC:16644.0,14.0] || -> . % 7.46/7.63 16646[46:Spt:16645.0,3096.1,3096.2] || -> model(skf86(u),u)* status__dfg(u,skc72,wca)*. % 7.46/7.63 16954[0:Res:8.0,3642.0] || -> model(u,skc72)* status__dfg(skc72,skc57,wtc)*. % 7.46/7.63 16960[0:Res:6.0,3642.0] || -> model(u,skc67)* status__dfg(skc67,skc57,wtc)*. % 7.46/7.63 16966[0:Res:5.0,3642.0] || -> model(u,skc68)* status__dfg(skc68,skc57,wtc)*. % 7.46/7.63 16973[0:Res:2.0,3642.0] || -> model(u,skc58)* status__dfg(skc58,skc57,wtc)*. % 7.46/7.63 17160[0:Res:8.0,4800.0] || -> model(u,skc72)* status__dfg(skc72,skc57,wec)*. % 7.46/7.63 19101[47:Spt:16954.0] || -> model(u,skc72)*. % 7.46/7.63 19102[47:UnC:19101.0,14.0] || -> . % 7.46/7.63 19103[47:Spt:19102.0,16954.1] || -> status__dfg(skc72,skc57,wtc)*. % 7.46/7.63 19110[47:Res:19103.0,96.1] || nevera(u,wtc) status__dfg(skc72,skc57,u)* -> . % 7.46/7.63 19111[47:MRR:19110.0,13109.0] || status__dfg(skc72,skc57,u)* -> . % 7.46/7.63 19112[47:UnC:19111.0,6014.0] || -> . % 7.46/7.63 19113[40:Spt:19112.0,495.1] || -> model(skf75(skf101(wtc,u)),skf101(wtc,u))*. % 7.46/7.63 19572[41:Spt:496.0] || -> nevera(u,wtc)*. % 7.46/7.63 19654[42:Spt:502.0] || -> nevera(u,sca)*. % 7.46/7.63 19670[42:MRR:2913.0,19654.0] || status__dfg(u,skc57,v)* -> model(skf82(u),u)*. % 7.46/7.63 19697[42:MRR:657.1,19670.0] || -> model(skf82(u),u)*. % 7.46/7.63 19698[42:UnC:19697.0,14345.0] || -> . % 7.46/7.63 19699[42:Spt:19698.0,502.1] || -> model(skf83(skf100(sca,u)),skf100(sca,u))*. % 7.46/7.63 20363[43:Spt:16960.0] || -> model(u,skc67)*. % 7.46/7.63 20364[43:UnC:20363.0,13.0] || -> . % 7.46/7.63 20365[43:Spt:20364.0,16960.1] || -> status__dfg(skc67,skc57,wtc)*. % 7.46/7.63 20373[43:Res:20365.0,96.1] || nevera(u,wtc) status__dfg(skc67,skc57,u)* -> . % 7.46/7.63 20374[43:MRR:20373.0,19572.0] || status__dfg(skc67,skc57,u)* -> . % 7.46/7.63 20375[43:UnC:20374.0,6019.0] || -> . % 7.46/7.63 20376[41:Spt:20375.0,496.1] || -> model(u,skf100(wtc,v))*. % 7.46/7.63 20748[42:Spt:501.0] || -> nevera(u,wca)*. % 7.46/7.63 20808[43:Spt:502.0] || -> nevera(u,sca)*. % 7.46/7.63 20824[43:MRR:2906.0,20808.0] || status__dfg(u,skc72,v)* -> model(skf82(u),u)*. % 7.46/7.63 20851[43:MRR:647.1,20824.0] || -> model(skf82(u),u)*. % 7.46/7.63 20852[43:UnC:20851.0,14345.0] || -> . % 7.46/7.63 20853[43:Spt:20852.0,502.1] || -> model(skf83(skf100(sca,u)),skf100(sca,u))*. % 7.46/7.63 21610[44:Spt:3096.0] || -> model(u,skc72)*. % 7.46/7.63 21611[44:UnC:21610.0,14.0] || -> . % 7.46/7.63 21612[44:Spt:21611.0,3096.1,3096.2] || -> model(skf86(u),u)* status__dfg(u,skc72,wca)*. % 7.46/7.63 21669[44:Res:21612.1,96.1] || nevera(u,wca) status__dfg(v,skc72,u)* -> model(skf86(v),v)*. % 7.46/7.63 21670[44:MRR:21669.0,20748.0] || status__dfg(u,skc72,v)* -> model(skf86(u),u)*. % 7.46/7.63 21671[44:MRR:21612.1,21670.0] || -> model(skf86(u),u)*. % 7.46/7.63 21674[44:UnC:21671.0,14345.0] || -> . % 7.46/7.63 21677[42:Spt:21674.0,501.1] || -> model(skf87(skf100(wca,u)),skf100(wca,u))*. % 7.46/7.63 21751[43:Spt:502.0] || -> nevera(u,sca)*. % 7.46/7.63 21767[43:MRR:2913.0,21751.0] || status__dfg(u,skc57,v)* -> model(skf82(u),u)*. % 7.46/7.63 21794[43:MRR:657.1,21767.0] || -> model(skf82(u),u)*. % 7.46/7.63 21795[43:UnC:21794.0,14345.0] || -> . % 7.46/7.63 21796[43:Spt:21795.0,502.1] || -> model(skf83(skf100(sca,u)),skf100(sca,u))*. % 7.46/7.63 22575[44:Spt:3111.0] || -> model(u,skc58)*. % 7.46/7.63 22576[44:UnC:22575.0,10.0] || -> . % 7.46/7.63 22577[44:Spt:22576.0,3111.1,3111.2] || -> model(skf86(u),u)* status__dfg(u,skc58,wca)*. % 7.46/7.63 22864[45:Spt:3103.0] || -> model(u,skc68)*. % 7.46/7.63 22865[45:UnC:22864.0,113.0] || -> . % 7.46/7.63 22866[45:Spt:22865.0,3103.1,3103.2] || -> model(skf86(u),u)* status__dfg(u,skc68,wca)*. % 7.46/7.63 22986[46:Spt:3100.0] || -> model(u,skc67)*. % 7.46/7.63 22987[46:UnC:22986.0,13.0] || -> . % 7.46/7.63 22988[46:Spt:22987.0,3100.1,3100.2] || -> model(skf86(u),u)* status__dfg(u,skc67,wca)*. % 7.46/7.63 23018[46:Res:22988.0,14345.0] || -> status__dfg(not__dfg(skc57),skc67,wca)*. % 7.46/7.63 23050[46:Res:23018.0,208.1] || model(skf88(skc67),skc68)* -> . % 7.46/7.63 23183[47:Spt:3096.0] || -> model(u,skc72)*. % 7.46/7.63 23184[47:UnC:23183.0,14.0] || -> . % 7.46/7.63 23185[47:Spt:23184.0,3096.1,3096.2] || -> model(skf86(u),u)* status__dfg(u,skc72,wca)*. % 7.46/7.63 25164[48:Spt:16966.0] || -> model(u,skc68)*. % 7.46/7.63 25165[48:UnC:25164.0,23050.0] || -> . % 7.46/7.63 25166[48:Spt:25165.0,16966.1] || -> status__dfg(skc68,skc57,wtc)*. % 7.46/7.63 25275[49:Spt:16973.0] || -> model(u,skc58)*. % 7.46/7.63 25276[49:UnC:25275.0,10.0] || -> . % 7.46/7.63 25277[49:Spt:25276.0,16973.1] || -> status__dfg(skc58,skc57,wtc)*. % 7.46/7.63 25311[50:Spt:17160.0] || -> model(u,skc72)*. % 7.46/7.63 25312[50:UnC:25311.0,14.0] || -> . % 7.46/7.63 25313[50:Spt:25312.0,17160.1] || -> status__dfg(skc72,skc57,wec)*. % 7.46/7.63 25314[50:Res:25313.0,112.1] || status__dfg(skc72,skc57,thm)* -> . % 7.46/7.63 25325[50:MRR:25314.0,334.0] || -> . % 7.46/7.63 % SZS output end Refutation % 7.46/7.63 Formulae used in the proof : tautology satisfiable__dfg sat_non_taut_pair mixed_pair non_thm_spt mighta_wec_thm contradiction completeness not__dfg unp sap tac tau wtc cax tca uns thm eqv sca wca nevera esa sat eth nota mighta wec % 7.46/7.63 %------------------------------------------------------------------------------