%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SYN014-1 : TPTP v8.1.0. Released v1.0.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n005.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 12:17:19 EDT 2022 % Result : Unsatisfiable 0.19s 0.48s % Output : Refutation 0.19s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : SYN014-1 : TPTP v8.1.0. Released v1.0.0. % 0.06/0.13 % Command : run_spass %d %s % 0.12/0.34 % Computer : n005.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 : Mon Jul 11 15:29:37 EDT 2022 % 0.12/0.34 % CPUTime : % 0.19/0.48 % 0.19/0.48 SPASS V 3.9 % 0.19/0.48 SPASS beiseite: Proof found. % 0.19/0.48 % SZS status Theorem % 0.19/0.48 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.19/0.48 SPASS derived 489 clauses, backtracked 93 clauses, performed 6 splits and kept 248 clauses. % 0.19/0.48 SPASS allocated 63471 KBytes. % 0.19/0.48 SPASS spent 0:00:00.12 on the problem. % 0.19/0.48 0:00:00.04 for the input. % 0.19/0.48 0:00:00.00 for the FLOTTER CNF translation. % 0.19/0.48 0:00:00.01 for inferences. % 0.19/0.48 0:00:00.00 for the backtracking. % 0.19/0.48 0:00:00.05 for the reduction. % 0.19/0.48 % 0.19/0.48 % 0.19/0.48 Here is a proof with depth 6, length 86 : % 0.19/0.48 % SZS output start Refutation % 0.19/0.48 1[0:Inp] || equal(n,m)** -> . % 0.19/0.48 2[0:Inp] || -> equal(k,m) equal(k,n)**. % 0.19/0.48 3[0:Inp] || equal(u,k) -> element(u,j)* equal(u,j). % 0.19/0.48 4[0:Inp] || element(u,j)* -> equal(u,k) equal(u,j). % 0.19/0.48 5[0:Inp] || element(u,m)* equal(f(u),m) -> equal(u,m). % 0.19/0.48 6[0:Inp] || element(u,m)* equal(f(u),u) -> equal(u,m). % 0.19/0.48 7[0:Inp] || element(u,m) -> equal(u,m) element(u,f(u))*. % 0.19/0.48 8[0:Inp] || element(u,m) -> equal(u,m) element(f(u),u)*. % 0.19/0.48 9[0:Inp] || element(u,v)*+ element(v,u)* -> equal(u,v) equal(u,m) element(v,m)* equal(v,m). % 0.19/0.48 10[0:Inp] || equal(g(u),n) -> element(u,n)* equal(u,n). % 0.19/0.48 11[0:Inp] || equal(g(u),u) -> element(u,n)* equal(u,n). % 0.19/0.48 12[0:Inp] || -> element(u,n) equal(u,n) element(u,g(u))*. % 0.19/0.48 13[0:Inp] || -> element(u,n) equal(u,n) element(g(u),u)*. % 0.19/0.48 15[0:Inp] || equal(u,m) -> element(u,k)* equal(u,k). % 0.19/0.48 16[0:Inp] || equal(u,n) -> element(u,k)* equal(u,k). % 0.19/0.48 17[0:Inp] || element(u,k)* -> equal(u,n) equal(u,m) equal(u,k). % 0.19/0.48 18[1:Spt:2.0] || -> equal(k,m)**. % 0.19/0.48 19[1:Rew:18.0,17.3] || element(u,k)* -> equal(u,n) equal(u,m) equal(u,m). % 0.19/0.48 23[1:Rew:18.0,16.2] || equal(u,n) -> element(u,k)* equal(u,m). % 0.19/0.48 24[1:Rew:18.0,23.1] || equal(u,n) -> element(u,m)* equal(u,m). % 0.19/0.48 25[1:Obv:19.2] || element(u,k)* -> equal(u,n) equal(u,m). % 0.19/0.48 26[1:Rew:18.0,25.0] || element(u,m)* -> equal(u,n) equal(u,m). % 0.19/0.48 55[0:Res:7.2,9.0] || element(u,m) element(f(u),u)* -> equal(u,m) equal(f(u),u) equal(u,m) element(f(u),m)* equal(f(u),m). % 0.19/0.48 56[0:Res:13.2,9.0] || element(u,g(u))* -> element(u,n) equal(u,n) equal(g(u),u) equal(g(u),m) element(u,m) equal(u,m). % 0.19/0.48 67[0:Obv:55.2] || element(u,m) element(f(u),u)* -> equal(f(u),u) equal(u,m) element(f(u),m)* equal(f(u),m). % 0.19/0.48 68[0:MRR:67.1,67.2,67.5,8.2,6.1,5.1] || element(u,m) -> equal(u,m) element(f(u),m)*. % 0.19/0.48 71[1:Res:68.2,26.0] || element(u,m)* -> equal(u,m) equal(f(u),n) equal(f(u),m). % 0.19/0.48 73[1:MRR:71.3,5.1] || element(u,m)* -> equal(u,m) equal(f(u),n). % 0.19/0.48 77[1:Rew:73.2,6.1] || element(u,m)* equal(n,u) -> equal(u,m). % 0.19/0.48 80[1:MRR:77.0,24.1] || equal(n,u)* -> equal(u,m). % 0.19/0.48 87[1:EqR:80.0] || -> equal(n,m)**. % 0.19/0.48 88[1:MRR:87.0,1.0] || -> . % 0.19/0.48 89[1:Spt:88.0,2.0,18.0] || equal(k,m)** -> . % 0.19/0.48 90[1:Spt:88.0,2.1] || -> equal(k,n)**. % 0.19/0.48 93[1:Rew:90.0,15.2,90.0,15.1] || equal(u,m) -> element(u,n)* equal(u,n). % 0.19/0.48 94[1:Rew:90.0,4.1] || element(u,j)* -> equal(u,n) equal(u,j). % 0.19/0.48 95[1:Rew:90.0,3.0] || equal(u,n) -> element(u,j)* equal(u,j). % 0.19/0.48 96[1:Rew:90.0,17.3,90.0,17.0] || element(u,n)* -> equal(u,n) equal(u,m) equal(u,n). % 0.19/0.48 97[1:Obv:96.1] || element(u,n)* -> equal(u,m) equal(u,n). % 0.19/0.48 103[0:MRR:56.0,56.3,12.2,11.0] || -> element(u,n)* equal(u,n) equal(g(u),m) element(u,m) equal(u,m). % 0.19/0.48 104[1:MRR:103.0,97.0] || -> equal(u,n) equal(g(u),m) element(u,m)* equal(u,m). % 0.19/0.48 107[1:Res:13.2,94.0] || -> element(j,n)* equal(j,n) equal(g(j),n) equal(g(j),j). % 0.19/0.48 108[1:MRR:107.2,107.3,10.0,11.0] || -> element(j,n)* equal(j,n). % 0.19/0.48 112[2:Spt:108.1] || -> equal(j,n)**. % 0.19/0.48 114[2:Rew:112.0,94.0] || element(u,n)* -> equal(u,n) equal(u,j). % 0.19/0.48 117[2:Rew:112.0,114.2] || element(u,n)* -> equal(u,n) equal(u,n). % 0.19/0.48 118[2:Obv:117.1] || element(u,n)* -> equal(u,n). % 0.19/0.48 123[2:MRR:93.1,118.0] || equal(u,m) -> equal(u,n)*. % 0.19/0.48 132[2:SpL:123.1,1.0] || equal(u,m)* equal(u,m)* -> . % 0.19/0.48 135[2:Obv:132.0] || equal(u,m)* -> . % 0.19/0.48 136[2:AED:1.0,135.0] || -> . % 0.19/0.48 137[2:Spt:136.0,108.1,112.0] || equal(j,n)** -> . % 0.19/0.48 138[2:Spt:136.0,108.0] || -> element(j,n)*. % 0.19/0.48 139[2:Res:138.0,9.0] || element(n,j)* -> equal(j,n) equal(j,m) element(n,m) equal(n,m). % 0.19/0.48 140[2:MRR:139.4,1.0] || element(n,j)* -> equal(j,n) equal(j,m) element(n,m). % 0.19/0.48 141[2:MRR:140.1,137.0] || element(n,j)* -> equal(j,m) element(n,m). % 0.19/0.48 142[3:Spt:141.1] || -> equal(j,m)**. % 0.19/0.48 145[3:Rew:142.0,94.0] || element(u,m)* -> equal(u,n) equal(u,j). % 0.19/0.48 146[3:Rew:142.0,95.1] || equal(u,n) -> element(u,m)* equal(u,j). % 0.19/0.48 147[3:Rew:142.0,145.2] || element(u,m)* -> equal(u,n) equal(u,m). % 0.19/0.48 148[3:MRR:104.2,147.0] || -> equal(u,n) equal(g(u),m)** equal(u,m). % 0.19/0.48 149[3:Rew:142.0,146.2] || equal(u,n) -> element(u,m)* equal(u,m). % 0.19/0.48 160[3:SpR:148.1,12.2] || -> equal(u,n) equal(u,m) element(u,n)* equal(u,n) element(u,m). % 0.19/0.48 162[3:Obv:160.0] || -> equal(u,m) element(u,n)* equal(u,n) element(u,m). % 0.19/0.48 163[3:MRR:162.0,93.0] || -> element(u,n)* equal(u,n) element(u,m). % 0.19/0.48 165[3:Res:163.0,97.0] || -> equal(u,n) element(u,m)* equal(u,m) equal(u,n). % 0.19/0.48 166[3:Obv:165.0] || -> element(u,m)* equal(u,m) equal(u,n). % 0.19/0.48 167[3:MRR:166.0,147.0] || -> equal(u,m) equal(u,n)*. % 0.19/0.48 462[3:SpR:167.1,68.2] || element(u,m)* -> equal(f(u),m) equal(u,m) element(n,m)*. % 0.19/0.48 471[3:MRR:462.1,5.1] || element(u,m)*+ -> equal(u,m) element(n,m)*. % 0.19/0.48 479[4:Spt:471.0,471.1] || element(u,m)* -> equal(u,m). % 0.19/0.48 480[4:MRR:149.1,479.0] || equal(u,n)* -> equal(u,m). % 0.19/0.48 492[4:EqR:480.0] || -> equal(n,m)**. % 0.19/0.48 500[4:MRR:492.0,1.0] || -> . % 0.19/0.48 501[4:Spt:500.0,471.2] || -> element(n,m)*. % 0.19/0.48 507[4:SpR:167.1,501.0] || -> equal(u,m) element(u,m)*. % 0.19/0.48 520[4:MRR:5.0,507.1] || equal(f(u),m)** -> equal(u,m). % 0.19/0.48 521[4:MRR:6.0,507.1] || equal(f(u),u)** -> equal(u,m). % 0.19/0.48 661[4:SpL:167.1,521.0] || equal(n,u) -> equal(f(u),m)** equal(u,m). % 0.19/0.48 668[4:MRR:661.1,520.0] || equal(n,u)* -> equal(u,m). % 0.19/0.48 671[4:EqR:668.0] || -> equal(n,m)**. % 0.19/0.48 679[4:MRR:671.0,1.0] || -> . % 0.19/0.48 680[3:Spt:679.0,141.1,142.0] || equal(j,m)** -> . % 0.19/0.48 681[3:Spt:679.0,141.0,141.2] || element(n,j)* -> element(n,m). % 0.19/0.48 687[2:Res:138.0,97.0] || -> equal(j,m) equal(j,n)**. % 0.19/0.48 688[3:MRR:687.0,687.1,680.0,137.0] || -> . % 0.19/0.48 % SZS output end Refutation % 0.19/0.48 Formulae used in the proof : c_1 c_2 c_3 c_4 c_5 c_6 c_7 c_8 c_9 c_10 c_11 c_12 c_13 c_15 c_16 c_17 % 0.19/0.48 %------------------------------------------------------------------------------