%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWC027-1 : TPTP v8.1.0. Released v2.4.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n006.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 : Tue Jul 19 22:01:11 EDT 2022 % Result : Unsatisfiable 1.10s 1.32s % Output : Refutation 1.10s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.11 % Problem : SWC027-1 : TPTP v8.1.0. Released v2.4.0. % 0.06/0.12 % Command : run_spass %d %s % 0.11/0.33 % Computer : n006.cluster.edu % 0.11/0.33 % Model : x86_64 x86_64 % 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.33 % Memory : 8042.1875MB % 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.33 % CPULimit : 300 % 0.11/0.33 % WCLimit : 600 % 0.11/0.33 % DateTime : Sun Jun 12 06:12:12 EDT 2022 % 0.11/0.33 % CPUTime : % 1.10/1.32 % 1.10/1.32 SPASS V 3.9 % 1.10/1.32 SPASS beiseite: Proof found. % 1.10/1.32 % SZS status Theorem % 1.10/1.32 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 1.10/1.32 SPASS derived 1493 clauses, backtracked 1213 clauses, performed 23 splits and kept 2550 clauses. % 1.10/1.32 SPASS allocated 77479 KBytes. % 1.10/1.32 SPASS spent 0:00:00.97 on the problem. % 1.10/1.32 0:00:00.04 for the input. % 1.10/1.32 0:00:00.00 for the FLOTTER CNF translation. % 1.10/1.32 0:00:00.00 for inferences. % 1.10/1.32 0:00:00.02 for the backtracking. % 1.10/1.32 0:00:00.68 for the reduction. % 1.10/1.32 % 1.10/1.32 % 1.10/1.32 Here is a proof with depth 2, length 56 : % 1.10/1.32 % SZS output start Refutation % 1.10/1.32 1[0:Inp] || -> ssList(sk1)*. % 1.10/1.32 5[0:Inp] || -> equal(sk4,sk2)**. % 1.10/1.32 6[0:Inp] || -> equal(sk3,sk1)**. % 1.10/1.32 7[0:Inp] || -> ssItem(sk5)* equal(nil,sk4). % 1.10/1.32 8[0:Inp] || -> ssItem(sk5)* equal(nil,sk3). % 1.10/1.32 9[0:Inp] || -> equal(cons(sk5,nil),sk3)** equal(nil,sk4). % 1.10/1.32 10[0:Inp] || -> memberP(sk4,sk5)* equal(nil,sk4). % 1.10/1.32 12[0:Inp] || -> equal(cons(sk5,nil),sk3)** equal(nil,sk3). % 1.10/1.32 13[0:Inp] || -> memberP(sk4,sk5)* equal(nil,sk3). % 1.10/1.32 15[0:Inp] || -> equal(nil,sk1) equal(nil,sk2)**. % 1.10/1.32 18[0:Inp] || equal(nil,sk2)** equal(nil,sk1) -> . % 1.10/1.32 89[0:Inp] ssItem(u) || memberP(nil,u)* -> . % 1.10/1.32 90[0:Inp] ssList(u) || -> ssItem(v)* duplicatefreeP(u)*. % 1.10/1.32 117[0:Inp] ssList(u) ssItem(v) || equal(cons(v,u),u)** -> . % 1.10/1.32 206[0:Rew:6.0,8.1] || -> ssItem(sk5)* equal(nil,sk1). % 1.10/1.32 207[0:Rew:206.1,7.1,5.0,7.1] || -> ssItem(sk5)* equal(sk2,sk1). % 1.10/1.32 208[0:Rew:6.0,13.1,5.0,13.0] || -> equal(nil,sk1) memberP(sk2,sk5)*. % 1.10/1.32 209[0:Rew:208.1,10.1,5.0,10.1,5.0,10.0] || -> equal(sk2,sk1) memberP(sk2,sk5)*. % 1.10/1.32 210[0:Rew:6.0,12.1,6.0,12.0] || -> equal(nil,sk1) equal(cons(sk5,nil),sk1)**. % 1.10/1.32 211[0:Rew:210.1,9.1,5.0,9.1,6.0,9.0] || -> equal(sk2,sk1) equal(cons(sk5,nil),sk1)**. % 1.10/1.32 523[0:Res:1.0,117.1] ssItem(u) || equal(cons(u,sk1),sk1)** -> . % 1.10/1.32 574[1:Spt:90.1] || -> ssItem(u)*. % 1.10/1.32 579[1:MRR:89.0,574.0] || memberP(nil,u)* -> . % 1.10/1.32 588[1:MRR:523.0,574.0] || equal(cons(u,sk1),sk1)** -> . % 1.10/1.32 780[2:Spt:15.0] || -> equal(nil,sk1)**. % 1.10/1.32 785[2:Rew:780.0,18.1] || equal(nil,sk2)** equal(sk1,sk1) -> . % 1.10/1.32 809[2:Rew:780.0,211.1] || -> equal(sk2,sk1) equal(cons(sk5,sk1),sk1)**. % 1.10/1.32 920[2:Obv:785.1] || equal(nil,sk2)** -> . % 1.10/1.32 921[2:Rew:780.0,920.0] || equal(sk2,sk1)** -> . % 1.10/1.32 928[2:MRR:809.0,809.1,921.0,588.0] || -> . % 1.10/1.32 991[2:Spt:928.0,15.0,780.0] || equal(nil,sk1)** -> . % 1.10/1.32 992[2:Spt:928.0,15.1] || -> equal(nil,sk2)**. % 1.10/1.32 1024[2:Rew:992.0,579.0] || memberP(sk2,u)* -> . % 1.10/1.32 1029[2:Rew:992.0,991.0] || equal(sk2,sk1)** -> . % 1.10/1.32 1056[2:MRR:209.0,209.1,1029.0,1024.0] || -> . % 1.10/1.32 1177[1:Spt:1056.0,90.0,90.2] ssList(u) || -> duplicatefreeP(u)*. % 1.10/1.32 1194[2:Spt:15.0] || -> equal(nil,sk1)**. % 1.10/1.32 1218[2:Rew:1194.0,18.1] || equal(nil,sk2)** equal(sk1,sk1) -> . % 1.10/1.32 1260[2:Rew:1194.0,211.1] || -> equal(sk2,sk1) equal(cons(sk5,sk1),sk1)**. % 1.10/1.32 1334[2:Obv:1218.1] || equal(nil,sk2)** -> . % 1.10/1.32 1335[2:Rew:1194.0,1334.0] || equal(sk2,sk1)** -> . % 1.10/1.32 1336[2:MRR:207.1,1335.0] || -> ssItem(sk5)*. % 1.10/1.32 1368[2:MRR:1260.0,1335.0] || -> equal(cons(sk5,sk1),sk1)**. % 1.10/1.32 1698[2:SpL:1368.0,523.1] ssItem(sk5) || equal(sk1,sk1)* -> . % 1.10/1.32 1699[2:Obv:1698.1] ssItem(sk5) || -> . % 1.10/1.32 1700[2:SSi:1699.0,1336.0] || -> . % 1.10/1.32 1701[2:Spt:1700.0,15.0,1194.0] || equal(nil,sk1)** -> . % 1.10/1.32 1702[2:Spt:1700.0,15.1] || -> equal(nil,sk2)**. % 1.10/1.32 1719[2:Rew:1702.0,1701.0] || equal(sk2,sk1)** -> . % 1.10/1.32 1720[2:Rew:1702.0,206.1] || -> ssItem(sk5)* equal(sk2,sk1). % 1.10/1.32 1721[2:MRR:1720.1,1719.0] || -> ssItem(sk5)*. % 1.10/1.32 1728[2:Rew:1702.0,208.0] || -> equal(sk2,sk1) memberP(sk2,sk5)*. % 1.10/1.32 1729[2:MRR:1728.0,1719.0] || -> memberP(sk2,sk5)*. % 1.10/1.32 1754[2:Rew:1702.0,89.1] ssItem(u) || memberP(sk2,u)* -> . % 1.10/1.32 2092[2:Res:1729.0,1754.1] ssItem(sk5) || -> . % 1.10/1.32 2093[2:SSi:2092.0,1721.0] || -> . % 1.10/1.32 % SZS output end Refutation % 1.10/1.32 Formulae used in the proof : co1_1 co1_5 co1_6 co1_7 co1_8 co1_9 co1_10 co1_12 co1_13 co1_15 co1_18 clause71 clause72 clause99 % 1.10/1.32 %------------------------------------------------------------------------------