%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SYO604+1 : TPTP v8.1.0. Released v7.0.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 : Thu Jul 21 19:55:02 EDT 2022 % Result : Theorem 0.44s 0.61s % Output : Refutation 0.44s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.11 % Problem : SYO604+1 : TPTP v8.1.0. Released v7.0.0. % 0.11/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 : Sat Jul 9 12:40:29 EDT 2022 % 0.12/0.33 % CPUTime : % 0.44/0.61 % 0.44/0.61 SPASS V 3.9 % 0.44/0.61 SPASS beiseite: Proof found. % 0.44/0.61 % SZS status Theorem % 0.44/0.61 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.44/0.61 SPASS derived 1269 clauses, backtracked 128 clauses, performed 6 splits and kept 813 clauses. % 0.44/0.61 SPASS allocated 98778 KBytes. % 0.44/0.61 SPASS spent 0:00:00.27 on the problem. % 0.44/0.61 0:00:00.04 for the input. % 0.44/0.61 0:00:00.06 for the FLOTTER CNF translation. % 0.44/0.61 0:00:00.02 for inferences. % 0.44/0.61 0:00:00.00 for the backtracking. % 0.44/0.61 0:00:00.12 for the reduction. % 0.44/0.61 % 0.44/0.61 % 0.44/0.61 Here is a proof with depth 9, length 140 : % 0.44/0.61 % SZS output start Refutation % 0.44/0.61 1[0:Inp] || SkP1(skc2,u)* -> . % 0.44/0.61 2[0:Inp] || SkP2(skc2,u)* -> . % 0.44/0.61 5[0:Inp] || g_false_only(u,skf11(u))* -> . % 0.44/0.61 6[0:Inp] SkP3(u) || -> SkP5(u)*. % 0.44/0.61 7[0:Inp] SkP3(u) || g_false_only(u,skc2)* -> . % 0.44/0.61 10[0:Inp] || SkP4(u,v)* -> g_true_only(v,u). % 0.44/0.61 12[0:Inp] || g_both(u,v) -> g_true(u,v)*. % 0.44/0.61 14[0:Inp] || g_false_only(u,v) -> g_false(u,v)*. % 0.44/0.61 15[0:Inp] || SkC0 -> g_false_only(u,skc4) SkP4(skc4,u)*. % 0.44/0.61 17[0:Inp] || g_true_only(u,v) g_false(u,v)* -> . % 0.44/0.61 18[0:Inp] || g_false_only(u,v) g_true(u,v)* -> . % 0.44/0.61 19[0:Inp] || g_false_only(u,skc2) g_false_only(skf11(u),u)* -> . % 0.44/0.61 20[0:Inp] || SkC0 -> g_true_only(u,skf12(u))* SkP4(skc4,u). % 0.44/0.61 21[0:Inp] || SkC0 -> SkP4(skc4,u) g_true_only(skf12(u),u)*. % 0.44/0.61 22[0:Inp] SkP5(u) || -> SkP3(u) g_true_only(u,skf21(u))*. % 0.44/0.61 23[0:Inp] SkP5(u) || -> SkP3(u) g_true_only(skf21(u),u)*. % 0.44/0.61 24[0:Inp] || -> g_false_only(u,v)* g_both(u,v) g_true_only(u,v). % 0.44/0.61 27[0:Inp] SkP3(u) || g_true_only(u,v) -> SkP1(v,u)*. % 0.44/0.61 28[0:Inp] || SkP4(u,v)*+ -> g_false_only(w,v)* g_false_only(v,w)*. % 0.44/0.61 31[0:Inp] SkP3(u) || g_true_only(u,v)*+ g_true_only(v,u)* -> . % 0.44/0.61 35[0:Inp] || g_both(u,v) -> SkP5(u) g_false_only(v,u)* g_false_only(u,v)*. % 0.44/0.61 37[0:Inp] SkP5(u) || g_both(u,v)*+ -> SkP0(v) g_true_only(u,skf17(u))*. % 0.44/0.61 38[0:Inp] SkP5(u) || g_both(u,v)*+ -> SkP0(v) g_true_only(skf17(u),u)*. % 0.44/0.61 41[0:Inp] || g_true_only(u,v)+ g_true_only(w,u)* g_true_only(u,w)* -> SkP1(v,u)*. % 0.44/0.61 42[0:Inp] || g_both(u,v)+ g_true_only(w,u)* g_true_only(u,w)* -> SkP2(v,u)*. % 0.44/0.61 43[0:Inp] SkP0(u) || -> SkC0 SkP2(u,skf14(u))* SkP1(u,skf13(u)) g_false_only(skf16(u),u). % 0.44/0.61 44[0:Inp] SkP0(u) || -> SkC0 SkP3(skf16(v)) SkP2(u,skf14(u))* SkP1(u,skf13(u)) g_false_only(w,skf16(v))* g_false_only(skf16(v),w)*. % 0.44/0.61 55[1:Spt:43.1] || -> SkC0*. % 0.44/0.61 56[1:MRR:15.0,55.0] || -> g_false_only(u,skc4) SkP4(skc4,u)*. % 0.44/0.61 57[1:MRR:21.0,55.0] || -> SkP4(skc4,u) g_true_only(skf12(u),u)*. % 0.44/0.61 58[1:MRR:20.0,55.0] || -> g_true_only(u,skf12(u))* SkP4(skc4,u). % 0.44/0.61 61[0:Res:14.1,17.1] || g_false_only(u,v)* g_true_only(u,v) -> . % 0.44/0.61 65[0:Res:12.1,18.1] || g_both(u,v) g_false_only(u,v)* -> . % 0.44/0.61 67[0:MRR:35.3,65.1] || g_both(u,v) -> SkP5(u) g_false_only(v,u)*. % 0.44/0.61 80[0:Res:67.2,5.0] || g_both(skf11(u),u)* -> SkP5(skf11(u)). % 0.44/0.61 87[0:Res:67.2,19.1] || g_both(u,skf11(u))* g_false_only(u,skc2) -> SkP5(u). % 0.44/0.61 88[0:Res:24.0,5.0] || -> g_both(u,skf11(u))* g_true_only(u,skf11(u)). % 0.44/0.61 91[0:Res:24.0,7.1] SkP3(u) || -> g_both(u,skc2)* g_true_only(u,skc2). % 0.44/0.61 95[0:Res:24.0,19.1] || g_false_only(u,skc2) -> g_both(skf11(u),u)* g_true_only(skf11(u),u). % 0.44/0.61 102[0:Res:27.2,1.0] SkP3(u) || g_true_only(u,skc2)* -> . % 0.44/0.61 104[0:MRR:91.2,102.1] SkP3(u) || -> g_both(u,skc2)*. % 0.44/0.61 137[1:Res:56.1,28.0] || -> g_false_only(u,skc4)* g_false_only(v,u)* g_false_only(u,v)*. % 0.44/0.61 138[1:Fac:137.0,137.1] || -> g_false_only(skc4,skc4)* g_false_only(skc4,skc4)*. % 0.44/0.61 139[1:Fac:137.0,137.2] || -> g_false_only(skc4,u)* g_false_only(u,skc4)*. % 0.44/0.61 155[1:Obv:138.0] || -> g_false_only(skc4,skc4)*. % 0.44/0.61 161[1:Res:155.0,61.0] || g_true_only(skc4,skc4)* -> . % 0.44/0.61 172[1:Res:139.0,61.0] || g_true_only(skc4,u) -> g_false_only(u,skc4)*. % 0.44/0.61 244[0:Res:104.1,38.1] SkP3(u) SkP5(u) || -> SkP0(skc2) g_true_only(skf17(u),u)*. % 0.44/0.61 247[0:SSi:244.1,6.1] SkP3(u) || -> SkP0(skc2) g_true_only(skf17(u),u)*. % 0.44/0.61 269[1:Res:172.1,61.0] || g_true_only(skc4,u)*+ g_true_only(u,skc4)* -> . % 0.44/0.61 276[0:Res:104.1,37.1] SkP3(u) SkP5(u) || -> SkP0(skc2) g_true_only(u,skf17(u))*. % 0.44/0.61 279[0:SSi:276.1,6.1] SkP3(u) || -> SkP0(skc2) g_true_only(u,skf17(u))*. % 0.44/0.61 332[1:Res:58.0,269.0] || g_true_only(skf12(skc4),skc4)* -> SkP4(skc4,skc4). % 0.44/0.61 335[1:MRR:332.0,57.1] || -> SkP4(skc4,skc4)*. % 0.44/0.61 337[1:Res:335.0,10.0] || -> g_true_only(skc4,skc4)*. % 0.44/0.61 338[1:MRR:337.0,161.0] || -> . % 0.44/0.61 339[1:Spt:338.0,43.1,55.0] || SkC0* -> . % 0.44/0.61 340[1:Spt:338.0,43.0,43.2,43.3,43.4] SkP0(u) || -> SkP2(u,skf14(u))* SkP1(u,skf13(u)) g_false_only(skf16(u),u). % 0.44/0.61 341[1:MRR:44.1,339.0] SkP0(u) || -> SkP3(skf16(v)) SkP2(u,skf14(u))* SkP1(u,skf13(u)) g_false_only(w,skf16(v))* g_false_only(skf16(v),w)*. % 0.44/0.61 342[1:Res:340.1,2.0] SkP0(skc2) || -> SkP1(skc2,skf13(skc2))* g_false_only(skf16(skc2),skc2). % 0.44/0.61 346[1:MRR:342.1,1.0] SkP0(skc2) || -> g_false_only(skf16(skc2),skc2)*. % 0.44/0.61 368[2:Spt:247.0,247.2] SkP3(u) || -> g_true_only(skf17(u),u)*. % 0.44/0.61 370[3:Spt:279.0,279.2] SkP3(u) || -> g_true_only(u,skf17(u))*. % 0.44/0.61 379[3:Res:370.1,31.1] SkP3(u) SkP3(u) || g_true_only(skf17(u),u)* -> . % 0.44/0.61 381[3:Obv:379.0] SkP3(u) || g_true_only(skf17(u),u)* -> . % 0.44/0.61 382[3:MRR:381.1,368.1] SkP3(u) || -> . % 0.44/0.61 383[3:MRR:22.1,382.0] SkP5(u) || -> g_true_only(u,skf21(u))*. % 0.44/0.61 384[3:MRR:23.1,382.0] SkP5(u) || -> g_true_only(skf21(u),u)*. % 0.44/0.61 387[3:MRR:341.1,382.0] SkP0(u) || -> SkP2(u,skf14(u))* SkP1(u,skf13(u)) g_false_only(v,skf16(w))* g_false_only(skf16(w),v)*. % 0.44/0.61 390[0:Res:88.0,87.0] || g_false_only(u,skc2) -> g_true_only(u,skf11(u))* SkP5(u). % 0.44/0.61 407[3:Res:384.1,41.0] SkP5(u) || g_true_only(v,skf21(u))*+ g_true_only(skf21(u),v)* -> SkP1(u,skf21(u))*. % 0.44/0.61 411[0:Res:95.1,42.0] || g_false_only(u,skc2) g_true_only(v,skf11(u))*+ g_true_only(skf11(u),v)* -> g_true_only(skf11(u),u) SkP2(u,skf11(u))*. % 0.44/0.61 412[0:Res:95.1,37.1] SkP5(skf11(u)) || g_false_only(u,skc2) -> g_true_only(skf11(u),u) SkP0(u) g_true_only(skf11(u),skf17(skf11(u)))*. % 0.44/0.61 413[0:Res:95.1,38.1] SkP5(skf11(u)) || g_false_only(u,skc2) -> g_true_only(skf11(u),u) SkP0(u) g_true_only(skf17(skf11(u)),skf11(u))*. % 0.44/0.61 418[0:Res:95.1,80.0] || g_false_only(u,skc2) -> g_true_only(skf11(u),u)* SkP5(skf11(u)). % 0.44/0.61 420[0:MRR:413.0,418.2] || g_false_only(u,skc2) -> g_true_only(skf11(u),u) SkP0(u) g_true_only(skf17(skf11(u)),skf11(u))*. % 0.44/0.61 421[0:MRR:412.0,418.2] || g_false_only(u,skc2) -> g_true_only(skf11(u),u) SkP0(u) g_true_only(skf11(u),skf17(skf11(u)))*. % 0.44/0.61 427[4:Spt:387.0,387.1,387.2] SkP0(u) || -> SkP2(u,skf14(u))* SkP1(u,skf13(u)). % 0.44/0.61 428[4:Res:427.1,2.0] SkP0(skc2) || -> SkP1(skc2,skf13(skc2))*. % 0.44/0.61 432[4:MRR:428.1,1.0] SkP0(skc2) || -> . % 0.44/0.61 546[3:Res:383.1,407.1] SkP5(u) SkP5(u) || g_true_only(skf21(u),u) -> SkP1(u,skf21(u))*. % 0.44/0.61 547[3:Obv:546.0] SkP5(u) || g_true_only(skf21(u),u) -> SkP1(u,skf21(u))*. % 0.44/0.61 548[3:MRR:547.1,384.1] SkP5(u) || -> SkP1(u,skf21(u))*. % 0.44/0.61 549[3:Res:548.1,1.0] SkP5(skc2) || -> . % 0.44/0.61 1075[0:Res:420.3,411.1] || g_false_only(u,skc2) g_false_only(u,skc2) g_true_only(skf11(u),skf17(skf11(u)))* -> g_true_only(skf11(u),u) SkP0(u) g_true_only(skf11(u),u) SkP2(u,skf11(u)). % 0.44/0.61 1079[0:Obv:1075.3] || g_false_only(u,skc2) g_true_only(skf11(u),skf17(skf11(u)))* -> SkP0(u) g_true_only(skf11(u),u) SkP2(u,skf11(u)). % 0.44/0.61 1080[0:MRR:1079.1,421.3] || g_false_only(u,skc2) -> SkP0(u) g_true_only(skf11(u),u) SkP2(u,skf11(u))*. % 0.44/0.61 1085[0:Res:1080.3,2.0] || g_false_only(skc2,skc2) -> SkP0(skc2) g_true_only(skf11(skc2),skc2)*. % 0.44/0.61 1089[4:MRR:1085.1,432.0] || g_false_only(skc2,skc2) -> g_true_only(skf11(skc2),skc2)*. % 0.44/0.61 1095[4:Res:1089.1,41.0] || g_false_only(skc2,skc2) g_true_only(u,skf11(skc2))* g_true_only(skf11(skc2),u)* -> SkP1(skc2,skf11(skc2))*. % 0.44/0.61 1096[4:MRR:1095.3,1.0] || g_false_only(skc2,skc2) g_true_only(u,skf11(skc2))*+ g_true_only(skf11(skc2),u)* -> . % 0.44/0.61 1116[4:Res:390.1,1096.1] || g_false_only(skc2,skc2) g_false_only(skc2,skc2) g_true_only(skf11(skc2),skc2)* -> SkP5(skc2). % 0.44/0.61 1119[4:Obv:1116.0] || g_false_only(skc2,skc2) g_true_only(skf11(skc2),skc2)* -> SkP5(skc2). % 0.44/0.61 1120[4:MRR:1119.1,1119.2,1089.1,549.0] || g_false_only(skc2,skc2)* -> . % 0.44/0.61 1123[4:Res:24.0,1120.0] || -> g_both(skc2,skc2)* g_true_only(skc2,skc2). % 0.44/0.61 1124[4:Res:67.2,1120.0] || g_both(skc2,skc2)* -> SkP5(skc2). % 0.44/0.61 1126[4:MRR:1124.1,549.0] || g_both(skc2,skc2)* -> . % 0.44/0.61 1127[4:MRR:1123.0,1126.0] || -> g_true_only(skc2,skc2)*. % 0.44/0.61 1145[4:Res:1127.0,41.0] || g_true_only(u,skc2)* g_true_only(skc2,u)* -> SkP1(skc2,skc2)*. % 0.44/0.61 1146[4:MRR:1145.2,1.0] || g_true_only(u,skc2)*+ g_true_only(skc2,u)* -> . % 0.44/0.61 1189[4:Res:1127.0,1146.0] || g_true_only(skc2,skc2)* -> . % 0.44/0.61 1190[4:MRR:1189.0,1127.0] || -> . % 0.44/0.61 1192[4:Spt:1190.0,387.3,387.4] || -> g_false_only(u,skf16(v))* g_false_only(skf16(v),u)*. % 0.44/0.61 1197[4:Res:1192.0,19.1] || g_false_only(skf16(u),skc2) -> g_false_only(skf16(u),skf11(skf16(u)))*. % 0.44/0.62 1202[4:MRR:1197.1,5.0] || g_false_only(skf16(u),skc2)* -> . % 0.44/0.62 1203[4:MRR:346.1,1202.0] SkP0(skc2) || -> . % 0.44/0.62 1204[4:MRR:1085.1,1203.0] || g_false_only(skc2,skc2) -> g_true_only(skf11(skc2),skc2)*. % 0.44/0.62 1228[4:Res:1204.1,41.0] || g_false_only(skc2,skc2) g_true_only(u,skf11(skc2))* g_true_only(skf11(skc2),u)* -> SkP1(skc2,skf11(skc2))*. % 0.44/0.62 1229[4:MRR:1228.3,1.0] || g_false_only(skc2,skc2) g_true_only(u,skf11(skc2))*+ g_true_only(skf11(skc2),u)* -> . % 0.44/0.62 1324[4:Res:390.1,1229.1] || g_false_only(skc2,skc2) g_false_only(skc2,skc2) g_true_only(skf11(skc2),skc2)* -> SkP5(skc2). % 0.44/0.62 1327[4:Obv:1324.0] || g_false_only(skc2,skc2) g_true_only(skf11(skc2),skc2)* -> SkP5(skc2). % 0.44/0.62 1328[4:MRR:1327.1,1327.2,1204.1,549.0] || g_false_only(skc2,skc2)* -> . % 0.44/0.62 1331[4:Res:24.0,1328.0] || -> g_both(skc2,skc2)* g_true_only(skc2,skc2). % 0.44/0.62 1332[4:Res:67.2,1328.0] || g_both(skc2,skc2)* -> SkP5(skc2). % 0.44/0.62 1334[4:MRR:1332.1,549.0] || g_both(skc2,skc2)* -> . % 0.44/0.62 1335[4:MRR:1331.0,1334.0] || -> g_true_only(skc2,skc2)*. % 0.44/0.62 1359[4:Res:1335.0,41.0] || g_true_only(u,skc2)* g_true_only(skc2,u)* -> SkP1(skc2,skc2)*. % 0.44/0.62 1360[4:MRR:1359.2,1.0] || g_true_only(u,skc2)*+ g_true_only(skc2,u)* -> . % 0.44/0.62 1404[4:Res:1335.0,1360.0] || g_true_only(skc2,skc2)* -> . % 0.44/0.62 1405[4:MRR:1404.0,1335.0] || -> . % 0.44/0.62 1407[3:Spt:1405.0,279.1] || -> SkP0(skc2)*. % 0.44/0.62 1408[3:MRR:346.0,1407.0] || -> g_false_only(skf16(skc2),skc2)*. % 0.44/0.62 1589[4:Spt:341.0,341.2,341.3] SkP0(u) || -> SkP2(u,skf14(u))* SkP1(u,skf13(u)). % 0.44/0.62 1590[4:Res:1589.1,2.0] SkP0(skc2) || -> SkP1(skc2,skf13(skc2))*. % 0.44/0.62 1594[4:SSi:1590.0,1407.0] || -> SkP1(skc2,skf13(skc2))*. % 0.44/0.62 1595[4:MRR:1594.0,1.0] || -> . % 0.44/0.62 1596[4:Spt:1595.0,341.1,341.4,341.5] || -> SkP3(skf16(u)) g_false_only(v,skf16(u))* g_false_only(skf16(u),v)*. % 0.44/0.62 1601[4:Res:1596.1,19.1] || g_false_only(skf16(u),skc2) -> SkP3(skf16(u)) g_false_only(skf16(u),skf11(skf16(u)))*. % 0.44/0.62 1607[4:MRR:1601.1,1601.2,7.0,5.0] || g_false_only(skf16(u),skc2)* -> . % 0.44/0.62 1608[4:UnC:1607.0,1408.0] || -> . % 0.44/0.62 1610[2:Spt:1608.0,247.1] || -> SkP0(skc2)*. % 0.44/0.62 1611[2:MRR:346.0,1610.0] || -> g_false_only(skf16(skc2),skc2)*. % 0.44/0.62 1616[3:Spt:341.0,341.2,341.3] SkP0(u) || -> SkP2(u,skf14(u))* SkP1(u,skf13(u)). % 0.44/0.62 1617[3:Res:1616.1,2.0] SkP0(skc2) || -> SkP1(skc2,skf13(skc2))*. % 0.44/0.62 1621[3:SSi:1617.0,1610.0] || -> SkP1(skc2,skf13(skc2))*. % 0.44/0.62 1622[3:MRR:1621.0,1.0] || -> . % 0.44/0.62 1623[3:Spt:1622.0,341.1,341.4,341.5] || -> SkP3(skf16(u)) g_false_only(v,skf16(u))* g_false_only(skf16(u),v)*. % 0.44/0.62 1628[3:Res:1623.1,19.1] || g_false_only(skf16(u),skc2) -> SkP3(skf16(u)) g_false_only(skf16(u),skf11(skf16(u)))*. % 0.44/0.62 1634[3:MRR:1628.1,1628.2,7.0,5.0] || g_false_only(skf16(u),skc2)* -> . % 0.44/0.62 1635[3:UnC:1634.0,1611.0] || -> . % 0.44/0.62 % SZS output end Refutation % 0.44/0.62 Formulae used in the proof : nc3 both_g false_only_g true_only_g exhaustion_g % 0.44/0.62 %------------------------------------------------------------------------------