%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : KRS203+1 : TPTP v8.1.0. Bugfixed v5.4.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n024.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:30:53 EDT 2022 % Result : Theorem 240.77s 241.02s % Output : Refutation 244.07s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : KRS203+1 : TPTP v8.1.0. Bugfixed v5.4.0. % 0.03/0.12 % Command : run_spass %d %s % 0.12/0.33 % Computer : n024.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Tue Jun 7 11:44:34 EDT 2022 % 0.12/0.33 % CPUTime : % 240.77/241.02 % 240.77/241.02 SPASS V 3.9 % 240.77/241.02 SPASS beiseite: Proof found. % 240.77/241.02 % SZS status Theorem % 240.77/241.02 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 240.77/241.02 SPASS derived 155052 clauses, backtracked 15176 clauses, performed 371 splits and kept 66853 clauses. % 240.77/241.02 SPASS allocated 174042 KBytes. % 240.77/241.02 SPASS spent 0:04:00.49 on the problem. % 240.77/241.02 0:00:00.04 for the input. % 240.77/241.02 0:00:00.20 for the FLOTTER CNF translation. % 240.77/241.02 0:00:01.18 for inferences. % 240.77/241.02 0:0:13.09 for the backtracking. % 240.77/241.02 0:3:42.20 for the reduction. % 240.77/241.02 % 240.77/241.02 % 240.77/241.02 Here is a proof with depth 12, length 655 : % 240.77/241.02 % SZS output start Refutation % 240.77/241.02 1[0:Inp] || -> model(u,skc57)*. % 240.77/241.02 2[0:Inp] || -> model(skc59,skc58)*. % 240.77/241.02 3[0:Inp] || -> model(skc64,skc62)*. % 240.77/241.02 4[0:Inp] || -> model(skc64,skc63)*. % 240.77/241.02 5[0:Inp] || -> model(skc69,skc68)*. % 240.77/241.02 6[0:Inp] || -> model(skc70,skc67)*. % 240.77/241.02 7[0:Inp] || -> model(skc73,skc74)*. % 240.77/241.02 8[0:Inp] || -> model(skc75,skc72)*. % 240.77/241.02 9[0:Inp] || nota(sat,thm)* -> . % 240.77/241.02 10[0:Inp] || model(skc60,skc58)* -> . % 240.77/241.02 11[0:Inp] || model(u,skc61)* -> . % 240.77/241.02 13[0:Inp] || model(skc71,skc67)* -> . % 240.77/241.02 14[0:Inp] || model(skc73,skc72)* -> . % 240.77/241.02 16[0:Inp] || -> SkP0(u,v) model(v,not__dfg(u))*. % 240.77/241.02 18[0:Inp] || -> model(u,v) model(u,not__dfg(v))*. % 240.77/241.02 19[0:Inp] || model(u,skc68) -> model(u,skc67)*. % 240.77/241.02 20[0:Inp] || model(u,v)*+ -> status__dfg(v,w,unp)*. % 240.77/241.02 21[0:Inp] || -> model(skf52(u),u)* status__dfg(v,u,unp)*. % 240.77/241.02 22[0:Inp] || -> model(skf54(u),u)* status__dfg(u,v,sap)*. % 240.77/241.02 23[0:Inp] || model(u,v)*+ -> status__dfg(w,v,sap)*. % 240.77/241.02 24[0:Inp] || status__dfg(u,v,tac)*+ -> model(w,v)*. % 240.77/241.02 25[0:Inp] || status__dfg(u,v,tau)*+ -> model(w,u)*. % 240.77/241.02 26[0:Inp] || status__dfg(u,v,tau)*+ -> model(w,v)*. % 240.77/241.02 27[0:Inp] || status__dfg(u,v,wtc)*+ -> model(w,v)*. % 240.77/241.02 28[0:Inp] || -> model(skf81(u),u)* status__dfg(u,v,cax)*. % 240.77/241.02 29[0:Inp] || status__dfg(u,v,tca)*+ -> model(w,v)*. % 240.77/241.02 30[0:Inp] || status__dfg(u,v,uns)*+ -> model(w,u)*. % 240.77/241.02 32[0:Inp] || -> model(skf61(u,v),v)* status__dfg(v,u,thm). % 240.77/241.02 33[0:Inp] || status__dfg(u,v,eqv)*+ -> model(skf63(u),u)*. % 240.77/241.02 37[0:Inp] || status__dfg(u,v,wtc)*+ -> model(skf75(u),u)*. % 240.77/241.02 39[0:Inp] || model(u,v)* status__dfg(v,w,cax)*+ -> . % 240.77/241.02 41[0:Inp] || status__dfg(u,v,sca)*+ -> model(skf83(v),v)*. % 240.77/241.02 44[0:Inp] || status__dfg(u,v,wca)*+ -> model(skf87(v),v)*. % 240.77/241.02 46[0:Inp] || SkP0(u,v) model(v,not__dfg(u))* -> . % 240.77/241.02 47[0:Inp] || model(u,v) model(u,not__dfg(v))* -> . % 240.77/241.02 50[0:Inp] || model(skf61(u,v),u)*+ -> status__dfg(w,u,thm)*. % 240.77/241.02 53[0:Inp] || model(skf76(u),u)*+ status__dfg(u,v,wtc)* -> . % 240.77/241.02 56[0:Inp] || model(skf88(u),u)*+ status__dfg(v,u,wca)* -> . % 240.77/241.02 57[0:Inp] || status__dfg(u,v,csa) -> model(skf89(v,u),u)*. % 240.77/241.02 61[0:Inp] || model(skf68(u,v),u)*+ status__dfg(u,w,wec)* -> . % 240.77/241.02 63[0:Inp] || status__dfg(u,v,csa)*+ -> model(skf89(v,w),not__dfg(v))*. % 240.77/241.02 65[0:Inp] || -> isa(u,v) status__dfg(skf97(v,u),skf96(v,u),u)*. % 240.77/241.02 67[0:Inp] || -> nevera(u,v)* status__dfg(skf101(v,w),skf100(v,w),v)*. % 240.77/241.02 69[0:Inp] || model(u,v)*+ model(w,x)* -> status__dfg(x,v,esa)*. % 240.77/241.02 70[0:Inp] || model(u,v)*+ model(u,w)* -> status__dfg(w,v,sat)*. % 240.77/241.02 71[0:Inp] || model(u,v)* status__dfg(v,w,thm)*+ -> model(u,w)*. % 240.77/241.02 73[0:Inp] || model(u,v)* status__dfg(w,v,eqv)*+ -> model(u,w)*. % 240.77/241.02 74[0:Inp] || model(u,v)* status__dfg(v,w,wec)*+ -> model(u,w)*. % 240.77/241.02 76[0:Inp] || model(u,v)* status__dfg(w,v,eth)*+ -> model(u,w)*. % 240.77/241.02 78[0:Inp] || model(u,v)*+ -> model(skf82(w),w)* status__dfg(w,v,sca)*. % 240.77/241.02 81[0:Inp] || status__dfg(skf97(u,v),skf96(u,v),u)*+ -> isa(w,u)*. % 240.77/241.02 82[0:Inp] || status__dfg(u,v,w)*+ -> nota(w,x)* status__dfg(u,v,x)*. % 240.77/241.02 85[0:Inp] || model(u,v)* status__dfg(w,v,unp)*+ -> model(skf53(w),w)*. % 240.77/241.02 86[0:Inp] || model(u,v)* status__dfg(v,w,sap)*+ -> model(skf55(w),w)*. % 240.77/241.02 87[0:Inp] || model(u,v)* status__dfg(v,w,esa)*+ -> model(skf58(w),w)*. % 240.77/241.02 88[0:Inp] || model(u,v)* status__dfg(w,v,esa)*+ -> model(skf59(w),w)*. % 240.77/241.02 89[0:Inp] || model(u,v)* model(skf64(w),w)*+ -> status__dfg(v,w,tac)*. % 240.77/241.02 91[0:Inp] || model(u,v)* model(u,not__dfg(w))*+ -> status__dfg(v,w,csa)*. % 240.77/241.02 92[0:Inp] || status__dfg(u,v,w)*+ status__dfg(u,v,x)* -> mighta(x,w)*. % 240.77/241.02 93[0:Inp] || isa(u,v)* status__dfg(w,x,u)*+ -> status__dfg(w,x,v)*. % 240.77/241.02 94[0:Inp] || nota(u,v)* status__dfg(skf99(v,w),skf98(v,w),v)*+ -> . % 240.77/241.02 95[0:Inp] || model(skf73(u),u)*+ model(skf72(v),v)* -> status__dfg(v,u,tau)*. % 240.77/241.02 96[0:Inp] || nevera(u,v)* status__dfg(w,x,v)*+ status__dfg(w,x,u)* -> . % 240.77/241.02 98[0:Inp] || model(u,v)*+ -> model(w,v)* model(skf86(x),x)* status__dfg(x,v,wca)*. % 240.77/241.02 100[0:Inp] || model(skf62(u,v),u)*+ model(skf62(u,v),v)* -> status__dfg(v,u,eqv). % 240.77/241.02 101[0:Inp] || model(u,v)* model(skf74(w),w)*+ -> model(x,v)* status__dfg(v,w,wtc)*. % 240.77/241.02 109[0:Inp] || model(u,v)* model(w,x)* model(skf66(x,y),x)*+ -> model(w,v)* status__dfg(v,x,wec)*. % 240.77/241.02 112[0:Res:82.2,9.0] || status__dfg(u,v,sat)* -> status__dfg(u,v,thm). % 240.77/241.02 113[0:Res:19.1,13.0] || model(skc71,skc68)* -> . % 240.77/241.02 115[0:Res:8.0,23.0] || -> status__dfg(u,skc72,sap)*. % 240.77/241.02 122[0:Res:1.0,23.0] || -> status__dfg(u,skc57,sap)*. % 240.77/241.02 129[0:Res:8.0,20.0] || -> status__dfg(skc72,u,unp)*. % 240.77/241.02 136[0:Res:1.0,20.0] || -> status__dfg(skc57,u,unp)*. % 240.77/241.02 138[0:Res:18.1,20.0] || -> model(u,v)* status__dfg(not__dfg(v),w,unp)*. % 240.77/241.02 157[0:Res:28.0,46.1] || SkP0(u,skf81(not__dfg(u)))*+ -> status__dfg(not__dfg(u),v,cax)*. % 240.77/241.02 164[0:Res:28.0,47.1] || model(skf81(not__dfg(u)),u)*+ -> status__dfg(not__dfg(u),v,cax)*. % 240.77/241.02 169[0:Res:28.1,39.1] || model(u,v)*+ -> model(skf81(v),v)*. % 240.77/241.02 181[0:Res:18.1,169.0] || -> model(u,v)* model(skf81(not__dfg(v)),not__dfg(v))*. % 240.77/241.02 182[0:Res:16.1,169.0] || -> SkP0(u,v)* model(skf81(not__dfg(u)),not__dfg(u))*. % 240.77/241.02 208[0:Res:19.1,56.0] || model(skf88(skc67),skc68) status__dfg(u,skc67,wca)* -> . % 240.77/241.02 241[0:Res:19.1,53.0] || model(skf76(skc67),skc68) status__dfg(skc67,u,wtc)* -> . % 240.77/241.02 267[0:Res:181.1,47.1] || model(skf81(not__dfg(u)),u)*+ -> model(v,u)*. % 240.77/241.02 287[0:Res:182.1,47.1] || model(skf81(not__dfg(u)),u)*+ -> SkP0(u,v)*. % 240.77/241.02 296[0:Res:19.1,267.0] || model(skf81(not__dfg(skc67)),skc68)*+ -> model(u,skc67)*. % 240.77/241.02 310[0:Res:1.0,287.0] || -> SkP0(skc57,u)*. % 240.77/241.02 335[0:Res:19.1,50.0] || model(skf61(skc67,u),skc68)*+ -> status__dfg(v,skc67,thm)*. % 240.77/241.02 344[0:Res:138.0,335.0] || -> status__dfg(not__dfg(skc68),u,unp)* status__dfg(v,skc67,thm)*. % 240.77/241.02 346[0:Res:32.0,335.0] || -> status__dfg(skc68,skc67,thm)* status__dfg(u,skc67,thm)*. % 240.77/241.02 347[0:Con:346.1] || -> status__dfg(skc68,skc67,thm)*. % 240.77/241.02 348[1:Spt:344.1] || -> status__dfg(u,skc67,thm)*. % 240.77/241.02 495[0:Res:67.1,37.0] || -> nevera(u,wtc)* model(skf75(skf101(wtc,v)),skf101(wtc,v))*. % 240.77/241.02 496[0:Res:67.1,27.0] || -> nevera(u,wtc)* model(v,skf100(wtc,w))*. % 240.77/241.02 498[0:Res:67.1,26.0] || -> nevera(u,tau)* model(v,skf100(tau,w))*. % 240.77/241.02 501[0:Res:67.1,44.0] || -> nevera(u,wca)* model(skf87(skf100(wca,v)),skf100(wca,v))*. % 240.77/241.02 502[0:Res:67.1,41.0] || -> nevera(u,sca)* model(skf83(skf100(sca,v)),skf100(sca,v))*. % 240.77/241.02 647[0:Res:8.0,78.0] || -> model(skf82(u),u)* status__dfg(u,skc72,sca)*. % 240.77/241.02 649[0:Res:7.0,78.0] || -> model(skf82(u),u)* status__dfg(u,skc74,sca)*. % 240.77/241.02 650[0:Res:6.0,78.0] || -> model(skf82(u),u)* status__dfg(u,skc67,sca)*. % 240.77/241.02 652[0:Res:5.0,78.0] || -> model(skf82(u),u)* status__dfg(u,skc68,sca)*. % 240.77/241.02 654[0:Res:4.0,78.0] || -> model(skf82(u),u)* status__dfg(u,skc63,sca)*. % 240.77/241.02 655[0:Res:3.0,78.0] || -> model(skf82(u),u)* status__dfg(u,skc62,sca)*. % 240.77/241.02 656[0:Res:2.0,78.0] || -> model(skf82(u),u)* status__dfg(u,skc58,sca)*. % 240.77/241.02 657[0:Res:1.0,78.0] || -> model(skf82(u),u)* status__dfg(u,skc57,sca)*. % 240.77/241.02 662[0:Res:18.1,78.0] || -> model(u,v)* model(skf82(w),w)* status__dfg(w,not__dfg(v),sca)*. % 240.77/241.02 760[0:Res:1.0,70.0] || model(u,v)*+ -> status__dfg(v,skc57,sat)*. % 240.77/241.02 765[0:Res:18.1,70.0] || model(u,v)*+ -> model(u,w)* status__dfg(v,not__dfg(w),sat)*. % 240.77/241.02 899[0:Res:67.1,74.1] || model(u,skf101(wec,v))+ -> nevera(w,wec)* model(u,skf100(wec,v))*. % 240.77/241.02 938[0:Res:67.1,73.1] || model(u,skf100(eqv,v))*+ -> nevera(w,eqv)* model(u,skf101(eqv,v)). % 240.77/241.02 985[0:Res:647.1,41.0] || -> model(skf82(u),u)* model(skf83(skc72),skc72). % 240.77/241.02 1001[1:Res:348.0,71.1] || model(u,v)*+ -> model(u,skc67)*. % 240.77/241.02 1019[1:Res:18.1,1001.0] || -> model(u,v)* model(u,skc67)*. % 240.77/241.02 1061[1:Con:1019.0] || -> model(u,skc67)*. % 240.77/241.02 1062[1:UnC:1061.0,13.0] || -> . % 240.77/241.02 1063[1:Spt:1062.0,344.0] || -> status__dfg(not__dfg(skc68),u,unp)*. % 240.77/241.02 1081[2:Spt:985.0] || -> model(skf82(u),u)*. % 240.77/241.02 1082[2:UnC:1081.0,11.0] || -> . % 240.77/241.02 1083[2:Spt:1082.0,985.1] || -> model(skf83(skc72),skc72)*. % 240.77/241.02 1090[0:Res:8.0,69.0] || model(u,v)*+ -> status__dfg(v,skc72,esa)*. % 240.77/241.02 1101[0:Res:1.0,69.0] || model(u,v)*+ -> status__dfg(v,skc57,esa)*. % 240.77/241.02 1157[0:Res:649.1,41.0] || -> model(skf82(u),u)* model(skf83(skc74),skc74). % 240.77/241.02 1159[3:Spt:1157.0] || -> model(skf82(u),u)*. % 240.77/241.02 1160[3:UnC:1159.0,11.0] || -> . % 240.77/241.02 1161[3:Spt:1160.0,1157.1] || -> model(skf83(skc74),skc74)*. % 240.77/241.02 1178[0:Res:650.1,41.0] || -> model(skf82(u),u)* model(skf83(skc67),skc67). % 240.77/241.02 1226[4:Spt:1178.0] || -> model(skf82(u),u)*. % 240.77/241.02 1227[4:UnC:1226.0,11.0] || -> . % 240.77/241.02 1228[4:Spt:1227.0,1178.1] || -> model(skf83(skc67),skc67)*. % 240.77/241.02 1245[0:Res:652.1,41.0] || -> model(skf82(u),u)* model(skf83(skc68),skc68). % 240.77/241.02 1247[5:Spt:1245.0] || -> model(skf82(u),u)*. % 240.77/241.02 1248[5:UnC:1247.0,11.0] || -> . % 240.77/241.02 1249[5:Spt:1248.0,1245.1] || -> model(skf83(skc68),skc68)*. % 240.77/241.02 1266[0:Res:654.1,41.0] || -> model(skf82(u),u)* model(skf83(skc63),skc63). % 240.77/241.02 1314[6:Spt:1266.0] || -> model(skf82(u),u)*. % 240.77/241.02 1315[6:UnC:1314.0,11.0] || -> . % 240.77/241.02 1316[6:Spt:1315.0,1266.1] || -> model(skf83(skc63),skc63)*. % 240.77/241.02 1333[0:Res:655.1,41.0] || -> model(skf82(u),u)* model(skf83(skc62),skc62). % 240.77/241.02 1335[7:Spt:1333.0] || -> model(skf82(u),u)*. % 240.77/241.02 1336[7:UnC:1335.0,11.0] || -> . % 240.77/241.02 1337[7:Spt:1336.0,1333.1] || -> model(skf83(skc62),skc62)*. % 240.77/241.02 1354[0:Res:656.1,41.0] || -> model(skf82(u),u)* model(skf83(skc58),skc58). % 240.77/241.02 1356[8:Spt:1354.0] || -> model(skf82(u),u)*. % 240.77/241.02 1357[8:UnC:1356.0,11.0] || -> . % 240.77/241.02 1358[8:Spt:1357.0,1354.1] || -> model(skf83(skc58),skc58)*. % 240.77/241.02 1389[0:Res:28.1,81.0] || -> model(skf81(skf97(cax,u)),skf97(cax,u))* isa(v,cax)*. % 240.77/241.02 1393[0:Res:22.1,81.0] || -> model(skf54(skf97(sap,u)),skf97(sap,u))* isa(v,sap)*. % 240.77/241.02 1400[0:Res:21.1,81.0] || -> model(skf52(skf96(unp,u)),skf96(unp,u))* isa(v,unp)*. % 240.77/241.02 1428[0:Res:8.0,760.0] || -> status__dfg(skc72,skc57,sat)*. % 240.77/241.02 1534[0:Res:129.0,82.0] || -> nota(unp,u) status__dfg(skc72,v,u)*. % 240.77/241.02 1541[0:Res:136.0,82.0] || -> nota(unp,u) status__dfg(skc57,v,u)*. % 240.77/241.02 1556[0:Res:115.0,82.0] || -> nota(sap,u) status__dfg(v,skc72,u)*. % 240.77/241.02 1563[0:Res:122.0,82.0] || -> nota(sap,u) status__dfg(v,skc57,u)*. % 240.77/241.02 1618[0:Res:347.0,82.0] || -> nota(thm,u) status__dfg(skc68,skc67,u)*. % 240.77/241.02 1619[0:Res:1428.0,82.0] || -> nota(sat,u) status__dfg(skc72,skc57,u)*. % 240.77/241.02 1676[0:Res:1618.1,30.0] || -> nota(thm,uns) model(u,skc68)*. % 240.77/241.02 1677[0:Res:1618.1,29.0] || -> nota(thm,tca) model(u,skc67)*. % 240.77/241.02 1679[0:Res:1618.1,27.0] || -> nota(thm,wtc) model(u,skc67)*. % 240.77/241.02 1680[0:Res:1618.1,25.0] || -> nota(thm,tau) model(u,skc68)*. % 240.77/241.02 1683[0:Res:1618.1,24.0] || -> nota(thm,tac) model(u,skc67)*. % 240.77/241.02 1724[9:Spt:1676.1] || -> model(u,skc68)*. % 240.77/241.02 1725[9:UnC:1724.0,113.0] || -> . % 240.77/241.02 1726[9:Spt:1725.0,1676.0] || -> nota(thm,uns)*. % 240.77/241.02 1727[10:Spt:1677.1] || -> model(u,skc67)*. % 240.77/241.02 1728[10:UnC:1727.0,13.0] || -> . % 240.77/241.02 1729[10:Spt:1728.0,1677.0] || -> nota(thm,tca)*. % 240.77/241.02 1730[0:Res:1.0,89.1] || model(u,v)*+ -> status__dfg(v,skc57,tac)*. % 240.77/241.02 1752[11:Spt:1679.1] || -> model(u,skc67)*. % 240.77/241.02 1753[11:UnC:1752.0,13.0] || -> . % 240.77/241.02 1754[11:Spt:1753.0,1679.0] || -> nota(thm,wtc)*. % 240.77/241.02 1755[12:Spt:1680.1] || -> model(u,skc68)*. % 240.77/241.02 1756[12:UnC:1755.0,113.0] || -> . % 240.77/241.02 1757[12:Spt:1756.0,1680.0] || -> nota(thm,tau)*. % 240.77/241.02 1758[13:Spt:1683.1] || -> model(u,skc67)*. % 240.77/241.02 1759[13:UnC:1758.0,13.0] || -> . % 240.77/241.02 1760[13:Spt:1759.0,1683.0] || -> nota(thm,tac)*. % 240.77/241.02 1772[0:Res:18.1,91.1] || model(u,v)*+ -> model(u,w)* status__dfg(v,w,csa)*. % 240.77/241.02 1773[0:Res:16.1,91.1] || model(u,v)*+ -> SkP0(w,u)* status__dfg(v,w,csa)*. % 240.77/241.02 1879[0:Res:67.1,87.1] || model(u,skf101(esa,v))*+ -> nevera(w,esa)* model(skf58(skf100(esa,v)),skf100(esa,v))*. % 240.77/241.02 1898[0:Res:1619.1,30.0] || -> nota(sat,uns) model(u,skc72)*. % 240.77/241.02 1902[0:Res:1619.1,25.0] || -> nota(sat,tau) model(u,skc72)*. % 240.77/241.02 1932[0:Res:1619.1,76.1] || model(u,skc57)* -> nota(sat,eth) model(u,skc72). % 240.77/241.02 1933[0:Res:1619.1,73.1] || model(u,skc57)* -> nota(sat,eqv) model(u,skc72). % 240.77/241.02 1948[0:MRR:1932.0,1.0] || -> nota(sat,eth) model(u,skc72)*. % 240.77/241.02 1949[0:MRR:1933.0,1.0] || -> nota(sat,eqv) model(u,skc72)*. % 240.77/241.02 1984[14:Spt:1898.1] || -> model(u,skc72)*. % 240.77/241.02 1985[14:UnC:1984.0,14.0] || -> . % 240.77/241.02 1986[14:Spt:1985.0,1898.0] || -> nota(sat,uns)*. % 240.77/241.02 1987[15:Spt:1902.1] || -> model(u,skc72)*. % 240.77/241.02 1988[15:UnC:1987.0,14.0] || -> . % 240.77/241.02 1989[15:Spt:1988.0,1902.0] || -> nota(sat,tau)*. % 240.77/241.02 1990[16:Spt:1948.1] || -> model(u,skc72)*. % 240.77/241.02 1991[16:UnC:1990.0,14.0] || -> . % 240.77/241.02 1992[16:Spt:1991.0,1948.0] || -> nota(sat,eth)*. % 240.77/241.02 2035[17:Spt:1949.1] || -> model(u,skc72)*. % 240.77/241.02 2036[17:UnC:2035.0,14.0] || -> . % 240.77/241.02 2037[17:Spt:2036.0,1949.0] || -> nota(sat,eqv)*. % 240.77/241.02 2120[0:Res:28.1,93.1] || isa(cax,u)+ -> model(skf81(v),v)* status__dfg(v,w,u)*. % 240.77/241.02 2131[0:Res:21.1,93.1] || isa(unp,u)+ -> model(skf52(v),v)* status__dfg(w,v,u)*. % 240.77/241.02 2220[0:Res:347.0,93.1] || isa(thm,u) -> status__dfg(skc68,skc67,u)*. % 240.77/241.02 2360[0:Res:65.1,92.0] || status__dfg(skf97(u,v),skf96(u,v),w)* -> isa(v,u) mighta(w,v). % 240.77/241.02 2365[0:Res:67.1,92.0] || status__dfg(skf101(u,v),skf100(u,v),w)*+ -> nevera(x,u)* mighta(w,u). % 240.77/241.02 2435[0:Res:1.0,95.0] || model(skf72(u),u)*+ -> status__dfg(u,skc57,tau)*. % 240.77/241.02 2712[0:Res:647.1,96.1] || nevera(u,sca) status__dfg(v,skc72,u)* -> model(skf82(v),v)*. % 240.77/241.02 2719[0:Res:657.1,96.1] || nevera(u,sca) status__dfg(v,skc57,u)* -> model(skf82(v),v)*. % 240.77/241.02 2916[0:Res:1534.1,30.0] || -> nota(unp,uns) model(u,skc72)*. % 240.77/241.02 2919[0:Res:1534.1,27.0] || -> nota(unp,wtc) model(u,v)*. % 240.77/241.02 2921[0:Res:1534.1,26.0] || -> nota(unp,tau) model(u,v)*. % 240.77/241.02 2923[0:Res:1534.1,24.0] || -> nota(unp,tac) model(u,v)*. % 240.77/241.02 3102[18:Spt:2916.1] || -> model(u,skc72)*. % 240.77/241.02 3103[18:UnC:3102.0,14.0] || -> . % 240.77/241.02 3104[18:Spt:3103.0,2916.0] || -> nota(unp,uns)*. % 240.77/241.02 3105[19:Spt:2919.1] || -> model(u,v)*. % 240.77/241.02 3106[19:UnC:3105.0,11.0] || -> . % 240.77/241.02 3107[19:Spt:3106.0,2919.0] || -> nota(unp,wtc)*. % 240.77/241.02 3108[20:Spt:2921.1] || -> model(u,v)*. % 240.77/241.02 3109[20:UnC:3108.0,11.0] || -> . % 240.77/241.02 3110[20:Spt:3109.0,2921.0] || -> nota(unp,tau)*. % 240.77/241.02 3111[21:Spt:2923.1] || -> model(u,v)*. % 240.77/241.02 3112[21:UnC:3111.0,11.0] || -> . % 240.77/241.02 3113[21:Spt:3112.0,2923.0] || -> nota(unp,tac)*. % 240.77/241.02 3114[0:Res:8.0,98.0] || -> model(u,skc72)* model(skf86(v),v)* status__dfg(v,skc72,wca)*. % 240.77/241.02 3118[0:Res:6.0,98.0] || -> model(u,skc67)* model(skf86(v),v)* status__dfg(v,skc67,wca)*. % 240.77/241.02 3121[0:Res:5.0,98.0] || -> model(u,skc68)* model(skf86(v),v)* status__dfg(v,skc68,wca)*. % 240.77/241.02 3130[0:Res:2.0,98.0] || -> model(u,skc58)* model(skf86(v),v)* status__dfg(v,skc58,wca)*. % 240.77/241.02 3209[0:Res:1.0,100.0] || model(skf62(skc57,u),u)* -> status__dfg(u,skc57,eqv). % 240.77/241.02 3308[0:Res:1.0,101.1] || model(u,v)*+ -> model(w,v)* status__dfg(v,skc57,wtc)*. % 240.77/241.02 3769[0:Res:1541.1,71.1] || model(u,skc57)* -> nota(unp,thm) model(u,v)*. % 240.77/241.02 3770[0:Res:1541.1,87.1] || model(u,skc57)* -> nota(unp,esa) model(skf58(v),v)*. % 240.77/241.02 3771[0:Res:1541.1,86.1] || model(u,skc57)* -> nota(unp,sap) model(skf55(v),v)*. % 240.77/241.02 3789[0:MRR:3769.0,1.0] || -> nota(unp,thm) model(u,v)*. % 240.77/241.02 3790[0:MRR:3770.0,1.0] || -> nota(unp,esa) model(skf58(u),u)*. % 240.77/241.02 3791[0:MRR:3771.0,1.0] || -> nota(unp,sap) model(skf55(u),u)*. % 240.77/241.02 3792[22:Spt:3789.1] || -> model(u,v)*. % 240.77/241.02 3793[22:UnC:3792.0,11.0] || -> . % 240.77/241.02 3794[22:Spt:3793.0,3789.0] || -> nota(unp,thm)*. % 240.77/241.02 3869[23:Spt:3790.1] || -> model(skf58(u),u)*. % 240.77/241.02 3870[23:UnC:3869.0,11.0] || -> . % 240.77/241.02 3871[23:Spt:3870.0,3790.0] || -> nota(unp,esa)*. % 240.77/241.02 3872[24:Spt:3791.1] || -> model(skf55(u),u)*. % 240.77/241.02 3873[24:UnC:3872.0,11.0] || -> . % 240.77/241.02 3874[24:Spt:3873.0,3791.0] || -> nota(unp,sap)*. % 240.77/241.02 3876[0:Res:1556.1,30.0] || -> nota(sap,uns) model(u,v)*. % 240.77/241.02 3880[0:Res:1556.1,25.0] || -> nota(sap,tau) model(u,v)*. % 240.77/241.02 3883[0:Res:1556.1,24.0] || -> nota(sap,tac) model(u,skc72)*. % 240.77/241.02 3895[0:Res:1556.1,33.0] || -> nota(sap,eqv) model(skf63(u),u)*. % 240.77/241.02 4069[25:Spt:3883.1] || -> model(u,skc72)*. % 240.77/241.02 4070[25:UnC:4069.0,14.0] || -> . % 240.77/241.02 4071[25:Spt:4070.0,3883.0] || -> nota(sap,tac)*. % 240.77/241.02 4072[26:Spt:3876.1] || -> model(u,v)*. % 240.77/241.02 4073[26:UnC:4072.0,11.0] || -> . % 240.77/241.02 4074[26:Spt:4073.0,3876.0] || -> nota(sap,uns)*. % 240.77/241.02 4075[27:Spt:3880.1] || -> model(u,v)*. % 240.77/241.02 4076[27:UnC:4075.0,11.0] || -> . % 240.77/241.02 4077[27:Spt:4076.0,3880.0] || -> nota(sap,tau)*. % 240.77/241.02 4078[28:Spt:3895.1] || -> model(skf63(u),u)*. % 240.77/241.02 4079[28:UnC:4078.0,11.0] || -> . % 240.77/241.02 4080[28:Spt:4079.0,3895.0] || -> nota(sap,eqv)*. % 240.77/241.02 4558[0:Res:1.0,109.2] || model(u,v)* model(w,skc57)* -> model(w,v)* status__dfg(v,skc57,wec)*. % 240.77/241.02 4581[0:MRR:4558.1,1.0] || model(u,v)*+ -> model(w,v)* status__dfg(v,skc57,wec)*. % 240.77/241.02 4770[0:Res:1563.1,88.1] || model(u,skc57)* -> nota(sap,esa) model(skf59(v),v)*. % 240.77/241.02 4771[0:Res:1563.1,85.1] || model(u,skc57)* -> nota(sap,unp) model(skf53(v),v)*. % 240.77/241.02 4801[0:MRR:4770.0,1.0] || -> nota(sap,esa) model(skf59(u),u)*. % 240.77/241.02 4802[0:MRR:4771.0,1.0] || -> nota(sap,unp) model(skf53(u),u)*. % 240.77/241.02 4803[29:Spt:4801.1] || -> model(skf59(u),u)*. % 240.77/241.02 4804[29:UnC:4803.0,11.0] || -> . % 240.77/241.02 4805[29:Spt:4804.0,4801.0] || -> nota(sap,esa)*. % 240.77/241.02 4880[30:Spt:4802.1] || -> model(skf53(u),u)*. % 240.77/241.02 4881[30:UnC:4880.0,11.0] || -> . % 240.77/241.02 4882[30:Spt:4881.0,4802.0] || -> nota(sap,unp)*. % 240.77/241.02 5144[0:Res:8.0,1090.0] || -> status__dfg(skc72,skc72,esa)*. % 240.77/241.02 5157[0:Res:1.0,1090.0] || -> status__dfg(skc57,skc72,esa)*. % 240.77/241.02 5219[0:Res:5144.0,82.0] || -> nota(esa,u) status__dfg(skc72,skc72,u)*. % 240.77/241.02 5340[0:Res:5157.0,82.0] || -> nota(esa,u) status__dfg(skc57,skc72,u)*. % 240.77/241.02 5860[0:Res:8.0,1101.0] || -> status__dfg(skc72,skc57,esa)*. % 240.77/241.02 5865[0:Res:6.0,1101.0] || -> status__dfg(skc67,skc57,esa)*. % 240.77/241.02 5868[0:Res:5.0,1101.0] || -> status__dfg(skc68,skc57,esa)*. % 240.77/241.02 5874[0:Res:1.0,1101.0] || -> status__dfg(skc57,skc57,esa)*. % 240.77/241.02 6036[0:Res:8.0,1730.0] || -> status__dfg(skc72,skc57,tac)*. % 240.77/241.02 6698[0:Res:6036.0,82.0] || -> nota(tac,u) status__dfg(skc72,skc57,u)*. % 240.77/241.02 8035[0:Res:5219.1,30.0] || -> nota(esa,uns) model(u,skc72)*. % 240.77/241.02 8038[0:Res:5219.1,27.0] || -> nota(esa,wtc) model(u,skc72)*. % 240.77/241.02 8039[0:Res:5219.1,25.0] || -> nota(esa,tau) model(u,skc72)*. % 240.77/241.02 8042[0:Res:5219.1,24.0] || -> nota(esa,tac) model(u,skc72)*. % 240.77/241.02 8133[0:Res:1.0,2435.0] || -> status__dfg(skc57,skc57,tau)*. % 240.77/241.02 8176[0:Res:8133.0,96.1] || nevera(u,tau) status__dfg(skc57,skc57,u)* -> . % 240.77/241.02 8177[31:Spt:8035.1] || -> model(u,skc72)*. % 240.77/241.02 8178[31:UnC:8177.0,14.0] || -> . % 240.77/241.02 8179[31:Spt:8178.0,8035.0] || -> nota(esa,uns)*. % 240.77/241.02 8180[32:Spt:8038.1] || -> model(u,skc72)*. % 240.77/241.02 8181[32:UnC:8180.0,14.0] || -> . % 240.77/241.02 8182[32:Spt:8181.0,8038.0] || -> nota(esa,wtc)*. % 240.77/241.02 8183[33:Spt:8039.1] || -> model(u,skc72)*. % 240.77/241.02 8184[33:UnC:8183.0,14.0] || -> . % 240.77/241.02 8185[33:Spt:8184.0,8039.0] || -> nota(esa,tau)*. % 240.77/241.02 8191[34:Spt:8042.1] || -> model(u,skc72)*. % 240.77/241.02 8192[34:UnC:8191.0,14.0] || -> . % 240.77/241.02 8193[34:Spt:8192.0,8042.0] || -> nota(esa,tac)*. % 240.77/241.02 8797[0:Res:5340.1,71.1] || model(u,skc57)* -> nota(esa,thm) model(u,skc72). % 240.77/241.02 8809[0:MRR:8797.0,1.0] || -> nota(esa,thm) model(u,skc72)*. % 240.77/241.02 8810[35:Spt:8809.1] || -> model(u,skc72)*. % 240.77/241.02 8811[35:UnC:8810.0,14.0] || -> . % 240.77/241.02 8812[35:Spt:8811.0,8809.0] || -> nota(esa,thm)*. % 240.77/241.02 10355[0:Res:1.0,3209.0] || -> status__dfg(skc57,skc57,eqv)*. % 240.77/241.02 10401[0:Res:10355.0,96.1] || nevera(u,eqv) status__dfg(skc57,skc57,u)* -> . % 240.77/241.02 12569[0:Res:6698.1,30.0] || -> nota(tac,uns) model(u,skc72)*. % 240.77/241.02 12573[0:Res:6698.1,25.0] || -> nota(tac,tau) model(u,skc72)*. % 240.77/241.02 12603[0:Res:6698.1,76.1] || model(u,skc57)* -> nota(tac,eth) model(u,skc72). % 240.77/241.02 12604[0:Res:6698.1,73.1] || model(u,skc57)* -> nota(tac,eqv) model(u,skc72). % 240.77/241.02 12625[0:MRR:12603.0,1.0] || -> nota(tac,eth) model(u,skc72)*. % 240.77/241.02 12626[0:MRR:12604.0,1.0] || -> nota(tac,eqv) model(u,skc72)*. % 240.77/241.02 12627[36:Spt:12569.1] || -> model(u,skc72)*. % 240.77/241.02 12628[36:UnC:12627.0,14.0] || -> . % 240.77/241.02 12629[36:Spt:12628.0,12569.0] || -> nota(tac,uns)*. % 240.77/241.02 12652[37:Spt:12573.1] || -> model(u,skc72)*. % 240.77/241.02 12653[37:UnC:12652.0,14.0] || -> . % 240.77/241.02 12654[37:Spt:12653.0,12573.0] || -> nota(tac,tau)*. % 240.77/241.02 12655[38:Spt:12625.1] || -> model(u,skc72)*. % 240.77/241.02 12656[38:UnC:12655.0,14.0] || -> . % 240.77/241.02 12657[38:Spt:12656.0,12625.0] || -> nota(tac,eth)*. % 240.77/241.02 12658[39:Spt:12626.1] || -> model(u,skc72)*. % 240.77/241.02 12659[39:UnC:12658.0,14.0] || -> . % 240.77/241.02 12660[39:Spt:12659.0,12626.0] || -> nota(tac,eqv)*. % 240.77/241.02 12860[40:Spt:495.0] || -> nevera(u,wtc)*. % 240.77/241.02 13091[41:Spt:501.0] || -> nevera(u,wca)*. % 240.77/241.02 13119[42:Spt:502.0] || -> nevera(u,sca)*. % 240.77/241.02 13127[42:MRR:2719.0,13119.0] || status__dfg(u,skc57,v)* -> model(skf82(u),u)*. % 240.77/241.02 13145[42:MRR:657.1,13127.0] || -> model(skf82(u),u)*. % 240.77/241.02 13146[42:UnC:13145.0,11.0] || -> . % 240.77/241.02 13147[42:Spt:13146.0,502.1] || -> model(skf83(skf100(sca,u)),skf100(sca,u))*. % 240.77/241.02 14070[0:Res:310.0,157.0] || -> status__dfg(not__dfg(skc57),u,cax)*. % 240.77/241.02 14071[0:Res:14070.0,39.1] || model(u,not__dfg(skc57))* -> . % 240.77/241.02 14101[0:Res:181.0,14071.0] || -> model(skf81(not__dfg(not__dfg(skc57))),not__dfg(not__dfg(skc57)))*. % 240.77/241.02 14687[43:Spt:3114.0] || -> model(u,skc72)*. % 240.77/241.02 14688[43:UnC:14687.0,14.0] || -> . % 240.77/241.02 14689[43:Spt:14688.0,3114.1,3114.2] || -> model(skf86(u),u)* status__dfg(u,skc72,wca)*. % 240.77/241.02 14742[43:Res:14689.1,96.1] || nevera(u,wca) status__dfg(v,skc72,u)* -> model(skf86(v),v)*. % 240.77/241.02 14743[43:MRR:14742.0,13091.0] || status__dfg(u,skc72,v)* -> model(skf86(u),u)*. % 240.77/241.02 14744[43:MRR:14689.1,14743.0] || -> model(skf86(u),u)*. % 240.77/241.02 14747[43:UnC:14744.0,14071.0] || -> . % 240.77/241.02 14749[41:Spt:14747.0,501.1] || -> model(skf87(skf100(wca,u)),skf100(wca,u))*. % 240.77/241.02 15012[42:Spt:502.0] || -> nevera(u,sca)*. % 240.77/241.02 15020[42:MRR:2712.0,15012.0] || status__dfg(u,skc72,v)* -> model(skf82(u),u)*. % 240.77/241.02 15054[42:MRR:647.1,15020.0] || -> model(skf82(u),u)*. % 240.77/241.02 15055[42:UnC:15054.0,14071.0] || -> . % 240.77/241.02 15056[42:Spt:15055.0,502.1] || -> model(skf83(skf100(sca,u)),skf100(sca,u))*. % 240.77/241.02 15858[43:Spt:3118.0] || -> model(u,skc67)*. % 240.77/241.02 15859[43:UnC:15858.0,13.0] || -> . % 240.77/241.02 15860[43:Spt:15859.0,3118.1,3118.2] || -> model(skf86(u),u)* status__dfg(u,skc67,wca)*. % 240.77/241.02 15886[43:Res:15860.0,14071.0] || -> status__dfg(not__dfg(skc57),skc67,wca)*. % 240.77/241.02 15918[43:Res:15886.0,208.1] || model(skf88(skc67),skc68)* -> . % 240.77/241.02 15952[44:Spt:3121.0] || -> model(u,skc68)*. % 240.77/241.02 15953[44:UnC:15952.0,15918.0] || -> . % 240.77/241.02 15954[44:Spt:15953.0,3121.1,3121.2] || -> model(skf86(u),u)* status__dfg(u,skc68,wca)*. % 240.77/241.02 16242[45:Spt:3130.0] || -> model(u,skc58)*. % 240.77/241.02 16243[45:UnC:16242.0,10.0] || -> . % 240.77/241.02 16244[45:Spt:16243.0,3130.1,3130.2] || -> model(skf86(u),u)* status__dfg(u,skc58,wca)*. % 240.77/241.02 16366[46:Spt:3114.0] || -> model(u,skc72)*. % 240.77/241.02 16367[46:UnC:16366.0,14.0] || -> . % 240.77/241.02 16368[46:Spt:16367.0,3114.1,3114.2] || -> model(skf86(u),u)* status__dfg(u,skc72,wca)*. % 240.77/241.02 16661[0:Res:8.0,3308.0] || -> model(u,skc72)* status__dfg(skc72,skc57,wtc)*. % 240.77/241.02 16667[0:Res:6.0,3308.0] || -> model(u,skc67)* status__dfg(skc67,skc57,wtc)*. % 240.77/241.02 16673[0:Res:5.0,3308.0] || -> model(u,skc68)* status__dfg(skc68,skc57,wtc)*. % 240.77/241.02 16679[0:Res:3.0,3308.0] || -> model(u,skc62)* status__dfg(skc62,skc57,wtc)*. % 240.77/241.02 16680[0:Res:2.0,3308.0] || -> model(u,skc58)* status__dfg(skc58,skc57,wtc)*. % 240.77/241.02 16864[0:Res:8.0,4581.0] || -> model(u,skc72)* status__dfg(skc72,skc57,wec)*. % 240.77/241.02 16870[0:Res:6.0,4581.0] || -> model(u,skc67)* status__dfg(skc67,skc57,wec)*. % 240.77/241.02 16876[0:Res:5.0,4581.0] || -> model(u,skc68)* status__dfg(skc68,skc57,wec)*. % 240.77/241.02 16882[0:Res:3.0,4581.0] || -> model(u,skc62)* status__dfg(skc62,skc57,wec)*. % 240.77/241.02 16883[0:Res:2.0,4581.0] || -> model(u,skc58)* status__dfg(skc58,skc57,wec)*. % 240.77/241.02 17613[0:Res:1.0,1772.0] || -> model(u,v)* status__dfg(skc57,v,csa)*. % 240.77/241.02 17803[0:Res:5.0,1773.0] || -> SkP0(u,skc69) status__dfg(skc68,u,csa)*. % 240.77/241.02 18735[47:Spt:16661.0] || -> model(u,skc72)*. % 240.77/241.02 18736[47:UnC:18735.0,14.0] || -> . % 240.77/241.02 18737[47:Spt:18736.0,16661.1] || -> status__dfg(skc72,skc57,wtc)*. % 240.77/241.02 18744[47:Res:18737.0,96.1] || nevera(u,wtc) status__dfg(skc72,skc57,u)* -> . % 240.77/241.02 18745[47:MRR:18744.0,12860.0] || status__dfg(skc72,skc57,u)* -> . % 240.77/241.02 18746[47:UnC:18745.0,5860.0] || -> . % 240.77/241.02 18747[40:Spt:18746.0,495.1] || -> model(skf75(skf101(wtc,u)),skf101(wtc,u))*. % 240.77/241.02 18772[40:Res:18747.0,20.0] || -> status__dfg(skf101(wtc,u),v,unp)*. % 240.77/241.02 18780[0:Res:4.0,4581.0] || -> model(u,skc63)* status__dfg(skc63,skc57,wec)*. % 240.77/241.02 18781[0:Res:4.0,3308.0] || -> model(u,skc63)* status__dfg(skc63,skc57,wtc)*. % 240.77/241.02 18806[0:Res:7.0,4581.0] || -> model(u,skc74)* status__dfg(skc74,skc57,wec)*. % 240.77/241.02 18807[0:Res:7.0,3308.0] || -> model(u,skc74)* status__dfg(skc74,skc57,wtc)*. % 240.77/241.02 19179[41:Spt:496.0] || -> nevera(u,wtc)*. % 240.77/241.02 19259[42:Spt:502.0] || -> nevera(u,sca)*. % 240.77/241.02 19275[42:MRR:2719.0,19259.0] || status__dfg(u,skc57,v)* -> model(skf82(u),u)*. % 240.77/241.02 19302[42:MRR:657.1,19275.0] || -> model(skf82(u),u)*. % 240.77/241.02 19303[42:UnC:19302.0,14071.0] || -> . % 240.77/241.02 19304[42:Spt:19303.0,502.1] || -> model(skf83(skf100(sca,u)),skf100(sca,u))*. % 240.77/241.02 20233[43:Spt:1400.1] || -> isa(u,unp)*. % 240.77/241.02 22833[0:Res:662.2,96.1] || nevera(u,sca) status__dfg(v,not__dfg(w),u)* -> model(x,w)* model(skf82(v),v)*. % 240.77/241.02 23239[0:Res:1.0,765.0] || -> model(u,v)* status__dfg(skc57,not__dfg(v),sat)*. % 240.77/241.02 25017[43:Res:20233.0,2120.0] || -> model(skf81(u),u)* status__dfg(u,v,unp)*. % 240.77/241.02 25018[43:MRR:25017.0,20.0] || -> status__dfg(u,v,unp)*. % 240.77/241.02 25089[43:Res:25018.0,94.1] || nota(u,unp)* -> . % 240.77/241.02 25091[43:UnC:25089.0,4882.0] || -> . % 240.77/241.02 25092[43:Spt:25091.0,1400.0] || -> model(skf52(skf96(unp,u)),skf96(unp,u))*. % 240.77/241.02 25468[0:Res:21.1,81.0] || -> model(skf52(skf96(unp,u)),skf96(unp,u))* isa(v,unp)*. % 240.77/241.02 26249[44:Spt:16667.0] || -> model(u,skc67)*. % 240.77/241.02 26250[44:UnC:26249.0,13.0] || -> . % 240.77/241.02 26251[44:Spt:26250.0,16667.1] || -> status__dfg(skc67,skc57,wtc)*. % 240.77/241.02 26259[44:Res:26251.0,96.1] || nevera(u,wtc) status__dfg(skc67,skc57,u)* -> . % 240.77/241.02 26260[44:MRR:26259.0,19179.0] || status__dfg(skc67,skc57,u)* -> . % 240.77/241.02 26261[44:UnC:26260.0,5865.0] || -> . % 240.77/241.02 26262[41:Spt:26261.0,496.1] || -> model(u,skf100(wtc,v))*. % 240.77/241.02 26292[41:Res:26262.0,23.0] || -> status__dfg(u,skf100(wtc,v),sap)*. % 240.77/241.02 26298[41:Res:26262.0,50.0] || -> status__dfg(u,skf100(wtc,v),thm)*. % 240.77/241.02 26935[42:Spt:16673.0] || -> model(u,skc68)*. % 240.77/241.02 26936[42:UnC:26935.0,113.0] || -> . % 240.77/241.02 26937[42:Spt:26936.0,16673.1] || -> status__dfg(skc68,skc57,wtc)*. % 240.77/241.02 26941[42:Res:26937.0,82.0] || -> nota(wtc,u) status__dfg(skc68,skc57,u)*. % 240.77/241.02 26944[42:Res:26937.0,96.1] || nevera(u,wtc) status__dfg(skc68,skc57,u)* -> . % 240.77/241.02 26976[43:Spt:16680.0] || -> model(u,skc58)*. % 240.77/241.02 26977[43:UnC:26976.0,10.0] || -> . % 240.77/241.02 26978[43:Spt:26977.0,16680.1] || -> status__dfg(skc58,skc57,wtc)*. % 240.77/241.02 26982[43:Res:26978.0,82.0] || -> nota(wtc,u) status__dfg(skc58,skc57,u)*. % 240.77/241.02 27029[44:Spt:16864.0] || -> model(u,skc72)*. % 240.77/241.02 27030[44:UnC:27029.0,14.0] || -> . % 240.77/241.02 27031[44:Spt:27030.0,16864.1] || -> status__dfg(skc72,skc57,wec)*. % 240.77/241.02 27038[44:Res:27031.0,82.0] || -> nota(wec,u) status__dfg(skc72,skc57,u)*. % 240.77/241.02 27041[44:Res:27031.0,96.1] || nevera(u,wec) status__dfg(skc72,skc57,u)* -> . % 240.77/241.02 27072[45:Spt:16870.0] || -> model(u,skc67)*. % 240.77/241.02 27073[45:UnC:27072.0,13.0] || -> . % 240.77/241.02 27074[45:Spt:27073.0,16870.1] || -> status__dfg(skc67,skc57,wec)*. % 240.77/241.02 27081[45:Res:27074.0,82.0] || -> nota(wec,u) status__dfg(skc67,skc57,u)*. % 240.77/241.02 27135[46:Spt:16876.0] || -> model(u,skc68)*. % 240.77/241.02 27136[46:UnC:27135.0,113.0] || -> . % 240.77/241.02 27137[46:Spt:27136.0,16876.1] || -> status__dfg(skc68,skc57,wec)*. % 240.77/241.02 27179[47:Spt:16883.0] || -> model(u,skc58)*. % 240.77/241.02 27180[47:UnC:27179.0,10.0] || -> . % 240.77/241.02 27181[47:Spt:27180.0,16883.1] || -> status__dfg(skc58,skc57,wec)*. % 240.77/241.02 27227[48:Spt:501.0] || -> nevera(u,wca)*. % 240.77/241.02 27280[49:Spt:25468.1] || -> isa(u,unp)*. % 240.77/241.02 27281[49:Res:27280.0,2120.0] || -> model(skf81(u),u)* status__dfg(u,v,unp)*. % 240.77/241.02 27282[49:MRR:27281.0,20.0] || -> status__dfg(u,v,unp)*. % 240.77/241.02 27291[49:Res:27282.0,94.1] || nota(u,unp)* -> . % 240.77/241.02 27293[49:UnC:27291.0,4882.0] || -> . % 240.77/241.02 27294[49:Spt:27293.0,25468.0] || -> model(skf52(skf96(unp,u)),skf96(unp,u))*. % 240.77/241.02 28234[50:Spt:16661.0] || -> model(u,skc72)*. % 240.77/241.02 28235[50:UnC:28234.0,14.0] || -> . % 240.77/241.02 28236[50:Spt:28235.0,16661.1] || -> status__dfg(skc72,skc57,wtc)*. % 240.77/241.02 28371[51:Spt:18780.0] || -> model(u,skc63)*. % 240.77/241.02 28418[51:Res:28371.0,164.0] || -> status__dfg(not__dfg(skc63),u,cax)*. % 240.77/241.02 28866[51:Res:28418.0,39.1] || model(u,not__dfg(skc63))* -> . % 240.77/241.02 29109[52:Spt:502.0] || -> nevera(u,sca)*. % 240.77/241.02 29126[52:MRR:22833.0,29109.0] || status__dfg(u,not__dfg(v),w)* -> model(x,v)* model(skf82(u),u)*. % 240.77/241.02 29174[52:MRR:662.2,29126.0] || -> model(u,v)* model(skf82(w),w)*. % 240.77/241.02 29175[52:Con:29174.0] || -> model(skf82(u),u)*. % 240.77/241.02 29176[52:UnC:29175.0,28866.0] || -> . % 240.77/241.02 29185[52:Spt:29176.0,502.1] || -> model(skf83(skf100(sca,u)),skf100(sca,u))*. % 240.77/241.02 29988[53:Spt:3114.0] || -> model(u,skc72)*. % 240.77/241.02 29989[53:UnC:29988.0,14.0] || -> . % 240.77/241.02 29990[53:Spt:29989.0,3114.1,3114.2] || -> model(skf86(u),u)* status__dfg(u,skc72,wca)*. % 240.77/241.02 30052[53:Res:29990.1,96.1] || nevera(u,wca) status__dfg(v,skc72,u)* -> model(skf86(v),v)*. % 240.77/241.02 30053[53:MRR:30052.0,27227.0] || status__dfg(u,skc72,v)* -> model(skf86(u),u)*. % 240.77/241.02 30054[53:MRR:29990.1,30053.0] || -> model(skf86(u),u)*. % 240.77/241.02 30057[53:UnC:30054.0,28866.0] || -> . % 240.77/241.02 30060[51:Spt:30057.0,18780.1] || -> status__dfg(skc63,skc57,wec)*. % 240.77/241.02 30281[52:Spt:18806.0] || -> model(u,skc74)*. % 240.77/241.02 30327[52:Res:30281.0,164.0] || -> status__dfg(not__dfg(skc74),u,cax)*. % 240.77/241.02 30375[53:Spt:502.0] || -> nevera(u,sca)*. % 240.77/241.02 30395[53:MRR:22833.0,30375.0] || status__dfg(u,not__dfg(v),w)* -> model(x,v)* model(skf82(u),u)*. % 240.77/241.02 30434[53:MRR:662.2,30395.0] || -> model(u,v)* model(skf82(w),w)*. % 240.77/241.02 30435[53:Con:30434.0] || -> model(skf82(u),u)*. % 240.77/241.02 30436[53:UnC:30435.0,14071.0] || -> . % 240.77/241.02 30437[53:Spt:30436.0,502.1] || -> model(skf83(skf100(sca,u)),skf100(sca,u))*. % 240.77/241.02 30824[52:Res:30327.0,39.1] || model(u,not__dfg(skc74))* -> . % 240.77/241.02 31515[54:Spt:3118.0] || -> model(u,skc67)*. % 240.77/241.02 31516[54:UnC:31515.0,13.0] || -> . % 240.77/241.02 31517[54:Spt:31516.0,3118.1,3118.2] || -> model(skf86(u),u)* status__dfg(u,skc67,wca)*. % 240.77/241.02 31580[54:Res:31517.1,96.1] || nevera(u,wca) status__dfg(v,skc67,u)* -> model(skf86(v),v)*. % 240.77/241.02 31581[54:MRR:31580.0,27227.0] || status__dfg(u,skc67,v)* -> model(skf86(u),u)*. % 240.77/241.02 31582[54:MRR:31517.1,31581.0] || -> model(skf86(u),u)*. % 240.77/241.02 31585[54:UnC:31582.0,30824.0] || -> . % 240.77/241.02 31588[52:Spt:31585.0,18806.1] || -> status__dfg(skc74,skc57,wec)*. % 240.77/241.02 31821[53:Spt:16679.0] || -> model(u,skc62)*. % 240.77/241.02 31868[53:Res:31821.0,164.0] || -> status__dfg(not__dfg(skc62),u,cax)*. % 240.77/241.02 32160[54:Spt:502.0] || -> nevera(u,sca)*. % 240.77/241.02 32177[54:MRR:22833.0,32160.0] || status__dfg(u,not__dfg(v),w)* -> model(x,v)* model(skf82(u),u)*. % 240.77/241.02 32211[54:MRR:662.2,32177.0] || -> model(u,v)* model(skf82(w),w)*. % 240.77/241.02 32212[54:Con:32211.0] || -> model(skf82(u),u)*. % 240.77/241.02 32213[54:UnC:32212.0,14071.0] || -> . % 240.77/241.02 32222[54:Spt:32213.0,502.1] || -> model(skf83(skf100(sca,u)),skf100(sca,u))*. % 240.77/241.02 32373[53:Res:31868.0,39.1] || model(u,not__dfg(skc62))* -> . % 240.77/241.02 33034[55:Spt:3121.0] || -> model(u,skc68)*. % 240.77/241.02 33035[55:UnC:33034.0,113.0] || -> . % 240.77/241.02 33036[55:Spt:33035.0,3121.1,3121.2] || -> model(skf86(u),u)* status__dfg(u,skc68,wca)*. % 240.77/241.02 33098[55:Res:33036.1,96.1] || nevera(u,wca) status__dfg(v,skc68,u)* -> model(skf86(v),v)*. % 240.77/241.02 33099[55:MRR:33098.0,27227.0] || status__dfg(u,skc68,v)* -> model(skf86(u),u)*. % 240.77/241.02 33100[55:MRR:33036.1,33099.0] || -> model(skf86(u),u)*. % 240.77/241.02 33103[55:UnC:33100.0,32373.0] || -> . % 240.77/241.02 33106[53:Spt:33103.0,16679.1] || -> status__dfg(skc62,skc57,wtc)*. % 240.77/241.02 33324[54:Spt:16667.0] || -> model(u,skc67)*. % 240.77/241.02 33325[54:UnC:33324.0,13.0] || -> . % 240.77/241.02 33326[54:Spt:33325.0,16667.1] || -> status__dfg(skc67,skc57,wtc)*. % 240.77/241.02 33383[55:Spt:18781.0] || -> model(u,skc63)*. % 240.77/241.02 33422[55:Res:33383.0,61.0] || status__dfg(skc63,u,wec)* -> . % 240.77/241.02 33437[55:UnC:33422.0,30060.0] || -> . % 240.77/241.02 33439[55:Spt:33437.0,18781.1] || -> status__dfg(skc63,skc57,wtc)*. % 240.77/241.02 33687[56:Spt:18807.0] || -> model(u,skc74)*. % 240.77/241.02 33725[56:Res:33687.0,61.0] || status__dfg(skc74,u,wec)* -> . % 240.77/241.02 33740[56:UnC:33725.0,31588.0] || -> . % 240.77/241.02 33742[56:Spt:33740.0,18807.1] || -> status__dfg(skc74,skc57,wtc)*. % 240.77/241.02 34002[57:Spt:16882.0] || -> model(u,skc62)*. % 240.77/241.02 34037[57:Res:34002.0,53.0] || status__dfg(skc62,u,wtc)* -> . % 240.77/241.02 34056[57:UnC:34037.0,33106.0] || -> . % 240.77/241.02 34058[57:Spt:34056.0,16882.1] || -> status__dfg(skc62,skc57,wec)*. % 240.77/241.02 34636[58:Spt:502.0] || -> nevera(u,sca)*. % 240.77/241.02 34656[58:MRR:22833.0,34636.0] || status__dfg(u,not__dfg(v),w)* -> model(x,v)* model(skf82(u),u)*. % 240.77/241.02 34695[58:MRR:662.2,34656.0] || -> model(u,v)* model(skf82(w),w)*. % 240.77/241.02 34696[58:Con:34695.0] || -> model(skf82(u),u)*. % 240.77/241.02 34697[58:UnC:34696.0,14071.0] || -> . % 240.77/241.02 34698[58:Spt:34697.0,502.1] || -> model(skf83(skf100(sca,u)),skf100(sca,u))*. % 240.77/241.02 35618[59:Spt:3130.0] || -> model(u,skc58)*. % 240.77/241.02 35619[59:UnC:35618.0,10.0] || -> . % 240.77/241.02 35620[59:Spt:35619.0,3130.1,3130.2] || -> model(skf86(u),u)* status__dfg(u,skc58,wca)*. % 240.77/241.02 35681[59:Res:35620.1,96.1] || nevera(u,wca) status__dfg(v,skc58,u)* -> model(skf86(v),v)*. % 240.77/241.02 35682[59:MRR:35681.0,27227.0] || status__dfg(u,skc58,v)* -> model(skf86(u),u)*. % 240.77/241.02 35683[59:MRR:35620.1,35682.0] || -> model(skf86(u),u)*. % 240.77/241.02 35686[59:UnC:35683.0,14071.0] || -> . % 240.77/241.02 35689[48:Spt:35686.0,501.1] || -> model(skf87(skf100(wca,u)),skf100(wca,u))*. % 240.77/241.02 35816[49:Spt:1393.1] || -> isa(u,sap)*. % 240.77/241.02 37182[0:Res:21.1,81.0] || -> model(skf52(skf96(unp,u)),skf96(unp,u))* isa(v,unp)*. % 240.77/241.02 43036[49:Res:35816.0,2131.0] || -> model(skf52(u),u)* status__dfg(v,u,sap)*. % 240.77/241.02 43038[49:MRR:43036.0,23.0] || -> status__dfg(u,v,sap)*. % 240.77/241.02 43050[49:Res:43038.0,94.1] || nota(u,sap)* -> . % 240.77/241.02 43052[49:UnC:43050.0,3874.0] || -> . % 240.77/241.02 43053[49:Spt:43052.0,1393.0] || -> model(skf54(skf97(sap,u)),skf97(sap,u))*. % 240.77/241.02 45550[50:Spt:37182.1] || -> isa(u,unp)*. % 240.77/241.02 45551[50:Res:45550.0,2120.0] || -> model(skf81(u),u)* status__dfg(u,v,unp)*. % 240.77/241.02 45553[50:MRR:45551.0,20.0] || -> status__dfg(u,v,unp)*. % 240.77/241.02 45564[50:Res:45553.0,94.1] || nota(u,unp)* -> . % 240.77/241.02 45566[50:UnC:45564.0,4882.0] || -> . % 240.77/241.02 45567[50:Spt:45566.0,37182.0] || -> model(skf52(skf96(unp,u)),skf96(unp,u))*. % 240.77/241.02 46541[51:Spt:16667.0] || -> model(u,skc67)*. % 240.77/241.02 46542[51:UnC:46541.0,13.0] || -> . % 240.77/241.02 46543[51:Spt:46542.0,16667.1] || -> status__dfg(skc67,skc57,wtc)*. % 240.77/241.02 46546[51:Res:46543.0,241.1] || model(skf76(skc67),skc68)* -> . % 240.77/241.02 46677[52:Spt:16661.0] || -> model(u,skc72)*. % 240.77/241.02 46678[52:UnC:46677.0,14.0] || -> . % 240.77/241.02 46679[52:Spt:46678.0,16661.1] || -> status__dfg(skc72,skc57,wtc)*. % 240.77/241.02 46687[52:Res:46679.0,96.1] || nevera(u,wtc) status__dfg(skc72,skc57,u)* -> . % 240.77/241.02 48207[53:Spt:1389.1] || -> isa(u,cax)*. % 244.07/244.35 48242[54:Spt:3130.0] || -> model(u,skc58)*. % 244.07/244.35 48243[54:UnC:48242.0,10.0] || -> . % 244.07/244.35 48244[54:Spt:48243.0,3130.1,3130.2] || -> model(skf86(u),u)* status__dfg(u,skc58,wca)*. % 244.07/244.35 48487[55:Spt:3121.0] || -> model(u,skc68)*. % 244.07/244.35 48488[55:UnC:48487.0,46546.0] || -> . % 244.07/244.35 48489[55:Spt:48488.0,3121.1,3121.2] || -> model(skf86(u),u)* status__dfg(u,skc68,wca)*. % 244.07/244.35 48523[55:Res:48489.0,14071.0] || -> status__dfg(not__dfg(skc57),skc68,wca)*. % 244.07/244.35 48555[55:Res:48523.0,44.0] || -> model(skf87(skc68),skc68)*. % 244.07/244.35 53351[42:Res:26941.1,73.1] || model(u,skc57)* -> nota(wtc,eqv) model(u,skc68). % 244.07/244.35 53379[42:MRR:53351.0,1.0] || -> nota(wtc,eqv) model(u,skc68)*. % 244.07/244.35 53603[43:Res:26982.1,25.0] || -> nota(wtc,tau) model(u,skc58)*. % 244.07/244.35 53694[44:Res:27038.1,73.1] || model(u,skc57)* -> nota(wec,eqv) model(u,skc72). % 244.07/244.35 53722[44:MRR:53694.0,1.0] || -> nota(wec,eqv) model(u,skc72)*. % 244.07/244.35 53941[45:Res:27081.1,25.0] || -> nota(wec,tau) model(u,skc67)*. % 244.07/244.35 61114[0:Res:17613.0,296.0] || -> status__dfg(skc57,skc68,csa)* model(u,skc67)*. % 244.07/244.35 70256[0:Res:14101.0,1090.0] || -> status__dfg(not__dfg(not__dfg(skc57)),skc72,esa)*. % 244.07/244.35 70633[0:Res:70256.0,96.1] || nevera(u,esa) status__dfg(not__dfg(not__dfg(skc57)),skc72,u)* -> . % 244.07/244.35 75925[0:Res:2220.1,30.0] || isa(thm,uns)*+ -> model(u,skc68)*. % 244.07/244.35 75975[0:Res:2220.1,39.1] || isa(thm,cax)*+ model(u,skc68)* -> . % 244.07/244.35 75999[53:MRR:75975.0,48207.0] || model(u,skc68)* -> . % 244.07/244.35 76000[55:UnC:75999.0,48555.0] || -> . % 244.07/244.35 76001[53:Spt:76000.0,1389.0] || -> model(skf81(skf97(cax,u)),skf97(cax,u))*. % 244.07/244.35 76106[54:Spt:3114.0] || -> model(u,skc72)*. % 244.07/244.35 76107[54:UnC:76106.0,14.0] || -> . % 244.07/244.35 76108[54:Spt:76107.0,3114.1,3114.2] || -> model(skf86(u),u)* status__dfg(u,skc72,wca)*. % 244.07/244.35 76202[55:Spt:3118.0] || -> model(u,skc67)*. % 244.07/244.35 76203[55:UnC:76202.0,13.0] || -> . % 244.07/244.35 76204[55:Spt:76203.0,3118.1,3118.2] || -> model(skf86(u),u)* status__dfg(u,skc67,wca)*. % 244.07/244.35 76241[55:Res:76204.0,14071.0] || -> status__dfg(not__dfg(skc57),skc67,wca)*. % 244.07/244.35 76293[56:Spt:3121.0] || -> model(u,skc68)*. % 244.07/244.35 76294[56:UnC:76293.0,46546.0] || -> . % 244.07/244.35 76295[56:Spt:76294.0,3121.1,3121.2] || -> model(skf86(u),u)* status__dfg(u,skc68,wca)*. % 244.07/244.35 76566[57:Spt:3130.0] || -> model(u,skc58)*. % 244.07/244.35 76567[57:UnC:76566.0,10.0] || -> . % 244.07/244.35 76568[57:Spt:76567.0,3130.1,3130.2] || -> model(skf86(u),u)* status__dfg(u,skc58,wca)*. % 244.07/244.35 76733[55:Res:76241.0,208.1] || model(skf88(skc67),skc68)* -> . % 244.07/244.35 78138[58:Spt:899.1] || -> nevera(u,wec)*. % 244.07/244.35 78142[58:MRR:27041.0,78138.0] || status__dfg(skc72,skc57,u)* -> . % 244.07/244.35 78146[58:UnC:78142.0,5860.0] || -> . % 244.07/244.35 78147[58:Spt:78146.0,899.0,899.2] || model(u,skf101(wec,v)) -> model(u,skf100(wec,v))*. % 244.07/244.35 78284[59:Spt:53722.1] || -> model(u,skc72)*. % 244.07/244.35 78285[59:UnC:78284.0,14.0] || -> . % 244.07/244.35 78286[59:Spt:78285.0,53722.0] || -> nota(wec,eqv)*. % 244.07/244.35 78287[60:Spt:53941.1] || -> model(u,skc67)*. % 244.07/244.35 78288[60:UnC:78287.0,13.0] || -> . % 244.07/244.35 78289[60:Spt:78288.0,53941.0] || -> nota(wec,tau)*. % 244.07/244.35 78291[61:Spt:53379.1] || -> model(u,skc68)*. % 244.07/244.35 78292[61:UnC:78291.0,76733.0] || -> . % 244.07/244.35 78293[61:Spt:78292.0,53379.0] || -> nota(wtc,eqv)*. % 244.07/244.35 78294[62:Spt:53603.1] || -> model(u,skc58)*. % 244.07/244.35 78295[62:UnC:78294.0,10.0] || -> . % 244.07/244.35 78296[62:Spt:78295.0,53603.0] || -> nota(wtc,tau)*. % 244.07/244.35 78330[63:Spt:938.1] || -> nevera(u,eqv)*. % 244.07/244.35 78333[63:MRR:10401.0,78330.0] || status__dfg(skc57,skc57,u)* -> . % 244.07/244.35 78339[63:UnC:78333.0,5874.0] || -> . % 244.07/244.35 78343[63:Spt:78339.0,938.0,938.2] || model(u,skf100(eqv,v))* -> model(u,skf101(eqv,v)). % 244.07/244.35 78945[0:Res:65.1,2360.0] || -> isa(u,v)* isa(u,v)* mighta(u,u)*. % 244.07/244.35 78961[0:Obv:78945.0] || -> isa(u,v)* mighta(u,u)*. % 244.07/244.35 79045[40:Res:18772.0,2365.0] || -> nevera(u,wtc)* mighta(unp,wtc)*. % 244.07/244.35 79067[41:Res:26292.0,2365.0] || -> nevera(u,wtc)* mighta(sap,wtc)*. % 244.07/244.35 79079[41:Res:26298.0,2365.0] || -> nevera(u,wtc)* mighta(thm,wtc)*. % 244.07/244.35 79255[64:Spt:498.0] || -> nevera(u,tau)*. % 244.07/244.35 79258[64:MRR:8176.0,79255.0] || status__dfg(skc57,skc57,u)* -> . % 244.07/244.35 79264[64:UnC:79258.0,5874.0] || -> . % 244.07/244.35 79268[64:Spt:79264.0,498.1] || -> model(u,skf100(tau,v))*. % 244.07/244.35 79275[64:Res:79268.0,23.0] || -> status__dfg(u,skf100(tau,v),sap)*. % 244.07/244.35 79286[64:Res:79268.0,1101.0] || -> status__dfg(skf100(tau,u),skc57,esa)*. % 244.07/244.35 79312[64:Res:79268.0,50.0] || -> status__dfg(u,skf100(tau,v),thm)*. % 244.07/244.35 79326[64:Res:79268.0,2435.0] || -> status__dfg(skf100(tau,u),skc57,tau)*. % 244.07/244.35 80026[65:Spt:79045.0] || -> nevera(u,wtc)*. % 244.07/244.35 80030[65:MRR:46687.0,80026.0] || status__dfg(skc72,skc57,u)* -> . % 244.07/244.35 80034[65:UnC:80030.0,5860.0] || -> . % 244.07/244.35 80035[65:Spt:80034.0,79045.1] || -> mighta(unp,wtc)*. % 244.07/244.35 83126[64:Res:79326.0,96.1] || nevera(u,tau) status__dfg(skf100(tau,v),skc57,u)* -> . % 244.07/244.35 83127[66:Spt:79067.0] || -> nevera(u,wtc)*. % 244.07/244.35 83131[66:MRR:26944.0,83127.0] || status__dfg(skc68,skc57,u)* -> . % 244.07/244.35 83135[66:UnC:83131.0,5868.0] || -> . % 244.07/244.35 83136[66:Spt:83135.0,79067.1] || -> mighta(sap,wtc)*. % 244.07/244.35 83678[67:Spt:79079.0] || -> nevera(u,wtc)*. % 244.07/244.35 83682[67:MRR:46687.0,83678.0] || status__dfg(skc72,skc57,u)* -> . % 244.07/244.35 83686[67:UnC:83682.0,5860.0] || -> . % 244.07/244.35 83687[67:Spt:83686.0,79079.1] || -> mighta(thm,wtc)*. % 244.07/244.35 87575[64:Res:79275.0,2365.0] || -> nevera(u,tau)* mighta(sap,tau)*. % 244.07/244.35 87577[68:Spt:87575.0] || -> nevera(u,tau)*. % 244.07/244.35 87584[68:MRR:83126.0,87577.0] || status__dfg(skf100(tau,u),skc57,v)* -> . % 244.07/244.35 87591[68:UnC:87584.0,79286.0] || -> . % 244.07/244.35 87592[68:Spt:87591.0,87575.1] || -> mighta(sap,tau)*. % 244.07/244.35 87988[64:Res:79312.0,2365.0] || -> nevera(u,tau)* mighta(thm,tau)*. % 244.07/244.35 88137[69:Spt:87988.0] || -> nevera(u,tau)*. % 244.07/244.35 88141[69:MRR:83126.0,88137.0] || status__dfg(skf100(tau,u),skc57,v)* -> . % 244.07/244.35 88148[69:UnC:88141.0,79286.0] || -> . % 244.07/244.35 88152[69:Spt:88148.0,87988.1] || -> mighta(thm,tau)*. % 244.07/244.35 89164[0:Res:78961.0,75925.0] || -> mighta(thm,thm)* model(u,skc68)*. % 244.07/244.35 89237[70:Spt:89164.1] || -> model(u,skc68)*. % 244.07/244.35 89238[70:UnC:89237.0,76733.0] || -> . % 244.07/244.35 89239[70:Spt:89238.0,89164.0] || -> mighta(thm,thm)*. % 244.07/244.35 90394[71:Spt:1879.1] || -> nevera(u,esa)*. % 244.07/244.35 90583[71:MRR:70633.0,90394.0] || status__dfg(not__dfg(not__dfg(skc57)),skc72,u)* -> . % 244.07/244.35 90817[71:UnC:90583.0,70256.0] || -> . % 244.07/244.35 90905[71:Spt:90817.0,1879.0,1879.2] || model(u,skf101(esa,v))*+ -> model(skf58(skf100(esa,v)),skf100(esa,v))*. % 244.07/244.35 91396[72:Spt:61114.1] || -> model(u,skc67)*. % 244.07/244.35 91397[72:UnC:91396.0,13.0] || -> . % 244.07/244.35 91398[72:Spt:91397.0,61114.0] || -> status__dfg(skc57,skc68,csa)*. % 244.07/244.35 91404[72:Res:91398.0,63.0] || -> model(skf89(skc68,u),not__dfg(skc68))*. % 244.07/244.35 91464[72:Res:91404.0,47.1] || model(skf89(skc68,u),skc68)* -> . % 244.07/244.35 94332[72:Res:57.1,91464.0] || status__dfg(skc68,skc68,csa)* -> . % 244.07/244.35 94334[72:Res:17803.1,94332.0] || -> SkP0(skc68,skc69)*. % 244.07/244.35 159816[72:Res:23239.0,91464.0] || -> status__dfg(skc57,not__dfg(skc68),sat)*. % 244.07/244.35 160111[72:Res:159816.0,112.0] || -> status__dfg(skc57,not__dfg(skc68),thm)*. % 244.07/244.35 160158[72:Res:160111.0,71.1] || model(u,skc57) -> model(u,not__dfg(skc68))*. % 244.07/244.35 160176[72:MRR:160158.0,1.0] || -> model(u,not__dfg(skc68))*. % 244.07/244.35 160259[72:Res:160176.0,46.1] || SkP0(skc68,u)* -> . % 244.07/244.35 160342[72:UnC:160259.0,94334.0] || -> . % 244.07/244.35 % SZS output end Refutation % 244.07/244.35 Formulae used in the proof : tautology satisfiable__dfg sat_non_taut_pair mixed_pair non_thm_spt nota_sat_thm contradiction completeness not__dfg unp sap tac tau wtc cax tca uns thm eqv sca wca csa wec isa nevera esa sat eth nota mighta % 244.07/244.35 %------------------------------------------------------------------------------