%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SYN015-2 : TPTP v8.1.0. Released v1.0.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n009.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:20 EDT 2022 % Result : Unsatisfiable 0.20s 0.57s % Output : Refutation 0.20s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SYN015-2 : TPTP v8.1.0. Released v1.0.0. % 0.07/0.13 % Command : run_spass %d %s % 0.12/0.34 % Computer : n009.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 Jul 12 04:45:22 EDT 2022 % 0.12/0.34 % CPUTime : % 0.20/0.57 % 0.20/0.57 SPASS V 3.9 % 0.20/0.57 SPASS beiseite: Proof found. % 0.20/0.57 % SZS status Theorem % 0.20/0.57 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.20/0.57 SPASS derived 2623 clauses, backtracked 176 clauses, performed 22 splits and kept 841 clauses. % 0.20/0.57 SPASS allocated 64754 KBytes. % 0.20/0.57 SPASS spent 0:00:00.22 on the problem. % 0.20/0.57 0:00:00.04 for the input. % 0.20/0.57 0:00:00.00 for the FLOTTER CNF translation. % 0.20/0.57 0:00:00.03 for inferences. % 0.20/0.57 0:00:00.00 for the backtracking. % 0.20/0.57 0:00:00.12 for the reduction. % 0.20/0.57 % 0.20/0.57 % 0.20/0.57 Here is a proof with depth 14, length 187 : % 0.20/0.57 % SZS output start Refutation % 0.20/0.57 1[0:Inp] || -> equalish(u,u)*. % 0.20/0.57 2[0:Inp] || equalish(u,v)* -> equalish(v,u). % 0.20/0.57 3[0:Inp] || equalish(u,v)* equalish(v,w)* -> equalish(u,w)*. % 0.20/0.57 4[0:Inp] || element(u,v)* equalish(v,w)*+ -> element(u,w)*. % 0.20/0.57 5[0:Inp] || equalish(u,v)*+ element(u,w)* -> element(v,w)*. % 0.20/0.57 6[0:Inp] || element(u,a)* -> equalish(u,a) equalish(u,k). % 0.20/0.57 8[0:Inp] || element(u,m)* equalish(f(u),m) -> equalish(u,m). % 0.20/0.57 9[0:Inp] || element(u,m)* equalish(f(u),u) -> equalish(u,m). % 0.20/0.57 10[0:Inp] || element(u,m) -> equalish(u,m) element(u,f(u))*. % 0.20/0.57 11[0:Inp] || element(u,m) -> equalish(u,m) element(f(u),u)*. % 0.20/0.57 12[0:Inp] || element(u,v)* element(v,u)* -> equalish(u,v) equalish(u,m) element(v,m)* equalish(v,m). % 0.20/0.57 13[0:Inp] || equalish(g(u),n) -> equalish(u,n) element(u,n)*. % 0.20/0.57 14[0:Inp] || equalish(g(u),u) -> equalish(u,n) element(u,n)*. % 0.20/0.57 15[0:Inp] || -> equalish(u,n) element(u,n) element(u,g(u))*. % 0.20/0.57 16[0:Inp] || -> equalish(u,n) element(u,n) element(g(u),u)*. % 0.20/0.57 17[0:Inp] || element(u,v)*+ element(v,u)* element(u,n)* -> equalish(v,u) equalish(u,n) equalish(v,n). % 0.20/0.57 19[0:Inp] || equalish(u,n) -> equalish(u,k) element(u,k)*. % 0.20/0.57 20[0:Inp] || element(u,k)* -> equalish(u,k) equalish(u,m) equalish(u,n). % 0.20/0.57 21[0:Inp] || equalish(n,a)*r -> . % 0.20/0.57 22[0:Inp] || equalish(m,n)*l -> . % 0.20/0.57 23[0:Inp] || equalish(n,k)*r -> . % 0.20/0.57 25[0:Inp] || equalish(k,a)*r -> . % 0.20/0.57 26[0:Inp] || -> equalish(m,k)*r. % 0.20/0.57 27[0:MRR:12.3,4.0] || element(u,v)*+ element(v,u)* -> equalish(v,u) equalish(u,m) element(u,m)*. % 0.20/0.57 28[0:NCh:3.2,3.1,23.0,26.0] || equalish(n,m)*r -> . % 0.20/0.57 32[0:Res:26.0,4.1] || element(u,m) -> element(u,k)*. % 0.20/0.57 37[0:Res:26.0,2.0] || -> equalish(k,m)*l. % 0.20/0.57 39[0:NCh:3.2,3.1,2.0,26.0] || equalish(u,m)*+ -> equalish(k,u)*. % 0.20/0.57 41[0:Res:37.0,5.0] || element(k,u)* -> element(m,u). % 0.20/0.57 44[0:Res:37.0,4.1] || element(u,k)* -> element(u,m). % 0.20/0.57 46[0:NCh:3.2,3.0,37.0,2.0] || equalish(m,u)*+ -> equalish(u,k)*. % 0.20/0.57 57[0:Res:19.2,44.0] || equalish(u,n) -> equalish(u,k) element(u,m)*. % 0.20/0.57 81[0:Res:16.2,6.0] || -> equalish(a,n) element(a,n)* equalish(g(a),a) equalish(g(a),k). % 0.20/0.57 85[0:MRR:81.2,14.0] || -> equalish(a,n) element(a,n)* equalish(g(a),k). % 0.20/0.57 93[0:Res:13.2,41.0] || equalish(g(k),n) -> equalish(k,n) element(m,n)*. % 0.20/0.57 94[1:Spt:93.1] || -> equalish(k,n)*l. % 0.20/0.57 98[1:OCh:3.1,3.0,94.0,26.0] || -> equalish(m,n)*l. % 0.20/0.57 106[1:MRR:98.0,22.0] || -> . % 0.20/0.57 107[1:Spt:106.0,93.1,94.0] || equalish(k,n)*l -> . % 0.20/0.57 108[1:Spt:106.0,93.0,93.2] || equalish(g(k),n) -> element(m,n)*. % 0.20/0.57 115[0:Res:57.2,8.0] || equalish(u,n) equalish(f(u),m)*l -> equalish(u,k) equalish(u,m). % 0.20/0.57 123[0:Res:57.2,9.0] || equalish(u,n) equalish(f(u),u)*l -> equalish(u,k) equalish(u,m). % 0.20/0.57 134[0:Res:15.2,27.0] || element(g(u),u)* -> equalish(u,n) element(u,n) equalish(g(u),u) equalish(u,m) element(u,m). % 0.20/0.57 143[0:Res:11.2,27.0] || element(u,m) element(u,f(u))* -> equalish(u,m) equalish(u,f(u)) equalish(f(u),m) element(f(u),m)*. % 0.20/0.57 148[0:Res:85.1,27.0] || element(n,a) -> equalish(a,n) equalish(g(a),k) equalish(n,a) equalish(a,m) element(a,m)*. % 0.20/0.57 150[0:MRR:134.0,134.3,16.2,14.0] || -> equalish(u,n) element(u,n) equalish(u,m) element(u,m)*. % 0.20/0.57 152[0:MRR:143.1,143.3,143.4,10.2,5.0,8.1] || element(u,m) -> equalish(u,m) element(f(u),m)*. % 0.20/0.57 153[0:MRR:148.1,148.3,2.0,21.0] || element(n,a) -> equalish(g(a),k) equalish(a,m) element(a,m)*. % 0.20/0.57 175[0:Res:32.1,20.0] || element(u,m)* -> equalish(u,k) equalish(u,m) equalish(u,n). % 0.20/0.57 179[2:Spt:153.1] || -> equalish(g(a),k)*l. % 0.20/0.57 180[2:Res:179.0,2.0] || -> equalish(k,g(a))*r. % 0.20/0.57 181[2:Res:179.0,5.0] || element(g(a),u)* -> element(k,u). % 0.20/0.57 182[2:Res:179.0,4.1] || element(u,g(a))* -> element(u,k). % 0.20/0.57 183[2:NCh:3.2,3.0,179.0,2.0] || equalish(k,u)*+ -> equalish(u,g(a))*. % 0.20/0.57 191[2:Res:15.2,181.0] || -> equalish(g(a),n) element(g(a),n) element(k,g(g(a)))*. % 0.20/0.57 205[2:Res:15.2,182.0] || -> equalish(a,n) element(a,n) element(a,k)*. % 0.20/0.57 215[0:Res:10.2,17.0] || element(u,m) element(f(u),u)* element(u,n) -> equalish(u,m) equalish(f(u),u) equalish(u,n) equalish(f(u),n). % 0.20/0.57 218[0:Res:32.1,17.0] || element(u,m)* element(k,u)* element(u,n) -> equalish(k,u) equalish(u,n) equalish(k,n). % 0.20/0.57 227[0:Res:152.2,17.0] || element(u,m) element(m,f(u)) element(f(u),n)* -> equalish(u,m) equalish(m,f(u)) equalish(f(u),n) equalish(m,n). % 0.20/0.57 231[1:MRR:218.5,107.0] || element(u,m)*+ element(k,u)* element(u,n) -> equalish(k,u) equalish(u,n). % 0.20/0.57 234[0:MRR:215.1,215.4,11.2,9.1] || element(u,m)* element(u,n) -> equalish(u,m) equalish(u,n) equalish(f(u),n). % 0.20/0.57 235[0:MRR:227.6,22.0] || element(u,m) element(m,f(u)) element(f(u),n)* -> equalish(u,m) equalish(m,f(u)) equalish(f(u),n). % 0.20/0.57 350[0:Res:152.2,234.0] || element(u,m) element(f(u),n)* -> equalish(u,m) equalish(f(u),m) equalish(f(u),n) equalish(f(f(u)),n). % 0.20/0.57 353[0:MRR:350.3,8.1] || element(u,m) element(f(u),n)* -> equalish(u,m) equalish(f(u),n) equalish(f(f(u)),n). % 0.20/0.57 354[3:Spt:205.0] || -> equalish(a,n)*l. % 0.20/0.57 356[3:Res:354.0,2.0] || -> equalish(n,a)*r. % 0.20/0.57 366[3:MRR:356.0,21.0] || -> . % 0.20/0.57 367[3:Spt:366.0,205.0,354.0] || equalish(a,n)*l -> . % 0.20/0.57 368[3:Spt:366.0,205.1,205.2] || -> element(a,n) element(a,k)*. % 0.20/0.57 590[0:Res:150.3,175.0] || -> equalish(u,n) element(u,n)* equalish(u,m) equalish(u,k) equalish(u,m) equalish(u,n). % 0.20/0.57 606[0:Obv:590.2] || -> element(u,n)* equalish(u,k) equalish(u,m) equalish(u,n). % 0.20/0.57 647[1:Res:152.2,231.0] || element(u,m) element(k,f(u)) element(f(u),n)* -> equalish(u,m) equalish(k,f(u)) equalish(f(u),n). % 0.20/0.57 666[4:Spt:191.0] || -> equalish(g(a),n)*l. % 0.20/0.57 671[4:OCh:3.1,3.0,666.0,180.0] || -> equalish(k,n)*l. % 0.20/0.57 686[4:MRR:671.0,107.0] || -> . % 0.20/0.57 687[4:Spt:686.0,191.0,666.0] || equalish(g(a),n)*l -> . % 0.20/0.57 688[4:Spt:686.0,191.1,191.2] || -> element(g(a),n) element(k,g(g(a)))*. % 0.20/0.57 823[2:Res:37.0,183.0] || -> equalish(m,g(a))*r. % 0.20/0.57 825[2:NCh:3.2,3.0,183.0,37.0] || equalish(m,u)*+ -> equalish(u,g(a))*. % 0.20/0.57 828[2:Res:823.0,2.0] || -> equalish(g(a),m)*l. % 0.20/0.57 948[0:Res:11.2,353.1] || element(n,m) element(n,m) -> equalish(n,m) equalish(n,m) equalish(f(n),n) equalish(f(f(n)),n)*l. % 0.20/0.57 949[0:Obv:948.2] || element(n,m) -> equalish(n,m) equalish(f(n),n) equalish(f(f(n)),n)*l. % 0.20/0.57 950[0:MRR:949.1,28.0] || element(n,m) -> equalish(f(n),n) equalish(f(f(n)),n)*l. % 0.20/0.57 957[0:Res:950.2,4.1] || element(n,m) element(u,f(f(n)))* -> equalish(f(n),n) element(u,n). % 0.20/0.57 976[5:Spt:957.1,957.3] || element(u,f(f(n)))* -> element(u,n). % 0.20/0.57 977[5:Res:10.2,976.0] || element(f(n),m)* -> equalish(f(n),m) element(f(n),n). % 0.20/0.57 985[5:Res:57.2,977.0] || equalish(f(n),n) -> equalish(f(n),k) equalish(f(n),m) element(f(n),n)*. % 0.20/0.57 987[5:MRR:985.0,606.3] || -> equalish(f(n),k) equalish(f(n),m) element(f(n),n)*. % 0.20/0.57 997[0:Res:11.2,235.2] || element(n,m) element(n,m) element(m,f(n))* -> equalish(n,m) equalish(n,m) equalish(m,f(n)) equalish(f(n),n). % 0.20/0.57 998[0:Obv:997.3] || element(n,m) element(m,f(n))* -> equalish(n,m) equalish(m,f(n)) equalish(f(n),n). % 0.20/0.57 999[0:MRR:998.2,28.0] || element(n,m) element(m,f(n))* -> equalish(m,f(n)) equalish(f(n),n). % 0.20/0.57 1012[6:Spt:987.1] || -> equalish(f(n),m)*l. % 0.20/0.57 1013[6:Res:1012.0,2.0] || -> equalish(m,f(n))*r. % 0.20/0.57 1137[6:Res:1013.0,825.0] || -> equalish(f(n),g(a))*l. % 0.20/0.57 1576[1:Res:11.2,647.2] || element(n,m) element(n,m) element(k,f(n))* -> equalish(n,m) equalish(n,m) equalish(k,f(n)) equalish(f(n),n). % 0.20/0.57 1580[1:Obv:1576.3] || element(n,m) element(k,f(n))* -> equalish(n,m) equalish(k,f(n)) equalish(f(n),n). % 0.20/0.57 2500[6:NCh:3.2,3.0,115.1,1137.0] || equalish(n,n) equalish(g(a),m)*l -> equalish(n,k) equalish(n,m). % 0.20/0.57 2504[6:MRR:2500.0,2500.1,2500.2,2500.3,1.0,828.0,23.0,28.0] || -> . % 0.20/0.57 2505[6:Spt:2504.0,987.1,1012.0] || equalish(f(n),m)*l -> . % 0.20/0.57 2506[6:Spt:2504.0,987.0,987.2] || -> equalish(f(n),k) element(f(n),n)*. % 0.20/0.57 2509[1:MRR:1580.2,28.0] || element(n,m) element(k,f(n))* -> equalish(k,f(n)) equalish(f(n),n). % 0.20/0.57 2510[7:Spt:2506.0] || -> equalish(f(n),k)*l. % 0.20/0.57 2532[7:NCh:3.2,3.0,2510.0,115.1] || equalish(n,n) equalish(k,m)*l -> equalish(n,k) equalish(n,m). % 0.20/0.57 2537[7:MRR:2532.0,2532.1,2532.2,2532.3,1.0,37.0,23.0,28.0] || -> . % 0.20/0.57 2538[7:Spt:2537.0,2506.0,2510.0] || equalish(f(n),k)*l -> . % 0.20/0.58 2539[7:Spt:2537.0,2506.1] || -> element(f(n),n)*. % 0.20/0.58 2541[7:Res:2539.0,27.0] || element(n,f(n)) -> equalish(n,f(n)) equalish(f(n),m) element(f(n),m)*. % 0.20/0.58 2545[7:MRR:2541.2,2505.0] || element(n,f(n)) -> equalish(n,f(n)) element(f(n),m)*. % 0.20/0.58 2549[7:Res:2545.2,175.0] || element(n,f(n))* -> equalish(n,f(n)) equalish(f(n),k) equalish(f(n),m) equalish(f(n),n). % 0.20/0.58 2556[7:MRR:2549.1,2549.2,2549.3,2.0,2538.0,2505.0] || element(n,f(n))* -> equalish(f(n),n). % 0.20/0.58 2558[7:Res:10.2,2556.0] || element(n,m)* -> equalish(n,m) equalish(f(n),n). % 0.20/0.58 2559[7:MRR:2558.1,28.0] || element(n,m)* -> equalish(f(n),n). % 0.20/0.58 2562[7:Res:57.2,2559.0] || equalish(n,n) -> equalish(n,k) equalish(f(n),n)*l. % 0.20/0.58 2563[7:MRR:2562.0,2562.1,1.0,23.0] || -> equalish(f(n),n)*l. % 0.20/0.58 2586[7:NCh:3.2,3.0,2563.0,123.1] || equalish(n,n) equalish(n,n) -> equalish(n,k)*r equalish(n,m). % 0.20/0.58 2588[7:Obv:2586.0] || equalish(n,n) -> equalish(n,k)*r equalish(n,m). % 0.20/0.58 2589[7:MRR:2588.0,2588.1,2588.2,1.0,23.0,28.0] || -> . % 0.20/0.58 2590[5:Spt:2589.0,957.0,957.2] || element(n,m)* -> equalish(f(n),n). % 0.20/0.58 2593[5:Res:57.2,2590.0] || equalish(n,n) -> equalish(n,k) equalish(f(n),n)*l. % 0.20/0.58 2594[5:MRR:2593.0,2593.1,1.0,23.0] || -> equalish(f(n),n)*l. % 0.20/0.58 2615[5:NCh:3.2,3.0,2594.0,123.1] || equalish(n,n) equalish(n,n) -> equalish(n,k)*r equalish(n,m). % 0.20/0.58 2617[5:Obv:2615.0] || equalish(n,n) -> equalish(n,k)*r equalish(n,m). % 0.20/0.58 2618[5:MRR:2617.0,2617.1,2617.2,1.0,23.0,28.0] || -> . % 0.20/0.58 2619[2:Spt:2618.0,153.1,179.0] || equalish(g(a),k)*l -> . % 0.20/0.58 2620[2:Spt:2618.0,153.0,153.2,153.3] || element(n,a) -> equalish(a,m) element(a,m)*. % 0.20/0.58 2621[2:MRR:85.2,2619.0] || -> equalish(a,n) element(a,n)*. % 0.20/0.58 2622[3:Spt:2620.1] || -> equalish(a,m)*l. % 0.20/0.58 2632[3:NCh:3.2,3.0,2622.0,39.0] || equalish(m,m) -> equalish(k,a)*r. % 0.20/0.58 2638[3:MRR:2632.0,2632.1,1.0,25.0] || -> . % 0.20/0.58 2639[3:Spt:2638.0,2620.1,2622.0] || equalish(a,m)*l -> . % 0.20/0.58 2640[3:Spt:2638.0,2620.0,2620.2] || element(n,a) -> element(a,m)*. % 0.20/0.58 2661[4:Spt:2621.0] || -> equalish(a,n)*l. % 0.20/0.58 2663[4:Res:2661.0,2.0] || -> equalish(n,a)*r. % 0.20/0.58 2674[4:MRR:2663.0,21.0] || -> . % 0.20/0.58 2675[4:Spt:2674.0,2621.0,2661.0] || equalish(a,n)*l -> . % 0.20/0.58 2676[4:Spt:2674.0,2621.1] || -> element(a,n)*. % 0.20/0.58 2695[5:Spt:957.1,957.3] || element(u,f(f(n)))* -> element(u,n). % 0.20/0.58 2696[5:Res:10.2,2695.0] || element(f(n),m)* -> equalish(f(n),m) element(f(n),n). % 0.20/0.58 2702[5:Res:57.2,2696.0] || equalish(f(n),n) -> equalish(f(n),k) equalish(f(n),m) element(f(n),n)*. % 0.20/0.58 2704[5:MRR:2702.0,606.3] || -> equalish(f(n),k) equalish(f(n),m) element(f(n),n)*. % 0.20/0.58 2721[6:Spt:2704.1] || -> equalish(f(n),m)*l. % 0.20/0.58 2738[6:NCh:3.2,3.0,2721.0,115.1] || equalish(n,n) equalish(m,m) -> equalish(n,k)*r equalish(n,m). % 0.20/0.58 2742[6:MRR:2738.0,2738.1,2738.2,2738.3,1.0,1.0,23.0,28.0] || -> . % 0.20/0.58 2743[6:Spt:2742.0,2704.1,2721.0] || equalish(f(n),m)*l -> . % 0.20/0.58 2744[6:Spt:2742.0,2704.0,2704.2] || -> equalish(f(n),k) element(f(n),n)*. % 0.20/0.58 2747[7:Spt:2744.0] || -> equalish(f(n),k)*l. % 0.20/0.58 2761[7:NCh:3.2,3.0,2747.0,115.1] || equalish(n,n) equalish(k,m)*l -> equalish(n,k) equalish(n,m). % 0.20/0.58 2766[7:MRR:2761.0,2761.1,2761.2,2761.3,1.0,37.0,23.0,28.0] || -> . % 0.20/0.58 2767[7:Spt:2766.0,2744.0,2747.0] || equalish(f(n),k)*l -> . % 0.20/0.58 2768[7:Spt:2766.0,2744.1] || -> element(f(n),n)*. % 0.20/0.58 2770[7:Res:2768.0,27.0] || element(n,f(n)) -> equalish(n,f(n)) equalish(f(n),m) element(f(n),m)*. % 0.20/0.58 2774[7:MRR:2770.2,2743.0] || element(n,f(n)) -> equalish(n,f(n)) element(f(n),m)*. % 0.20/0.58 2775[8:Spt:950.2] || -> equalish(f(f(n)),n)*l. % 0.20/0.58 2790[8:NCh:3.2,3.0,2775.0,123.1] || equalish(f(n),n)*l equalish(n,f(n)) -> equalish(f(n),k) equalish(f(n),m). % 0.20/0.58 2793[8:MRR:2790.0,2790.2,2790.3,2.1,2767.0,2743.0] || equalish(n,f(n))*r -> . % 0.20/0.58 2794[8:MRR:2774.1,2793.0] || element(n,f(n)) -> element(f(n),m)*. % 0.20/0.58 2797[8:Res:2794.1,175.0] || element(n,f(n))* -> equalish(f(n),k) equalish(f(n),m) equalish(f(n),n). % 0.20/0.58 2805[8:MRR:2797.1,2797.2,2767.0,2743.0] || element(n,f(n))* -> equalish(f(n),n). % 0.20/0.58 2835[9:Spt:999.2] || -> equalish(m,f(n))*r. % 0.20/0.58 2845[9:NCh:3.2,3.1,2835.0,46.0] || equalish(m,m) -> equalish(f(n),k)*l. % 0.20/0.58 2850[9:MRR:2845.0,2845.1,1.0,2767.0] || -> . % 0.20/0.58 2851[9:Spt:2850.0,999.2,2835.0] || equalish(m,f(n))*r -> . % 0.20/0.58 2852[9:Spt:2850.0,999.0,999.1,999.3] || element(n,m) element(m,f(n))* -> equalish(f(n),n). % 0.20/0.58 2921[10:Spt:2509.3] || -> equalish(f(n),n)*l. % 0.20/0.58 2962[10:NCh:3.2,3.0,2921.0,123.1] || equalish(n,n) equalish(n,n) -> equalish(n,k)*r equalish(n,m). % 0.20/0.58 2965[10:Obv:2962.0] || equalish(n,n) -> equalish(n,k)*r equalish(n,m). % 0.20/0.58 2966[10:MRR:2965.0,2965.1,2965.2,1.0,23.0,28.0] || -> . % 0.20/0.58 2967[10:Spt:2966.0,2509.3,2921.0] || equalish(f(n),n)*l -> . % 0.20/0.58 2968[10:Spt:2966.0,2509.0,2509.1,2509.2] || element(n,m) element(k,f(n))* -> equalish(k,f(n)). % 0.20/0.58 2969[10:MRR:2805.1,2967.0] || element(n,f(n))* -> . % 0.20/0.58 2979[10:Res:10.2,2969.0] || element(n,m)* -> equalish(n,m). % 0.20/0.58 2980[10:MRR:2979.1,28.0] || element(n,m)* -> . % 0.20/0.58 2985[10:Res:57.2,2980.0] || equalish(n,n) -> equalish(n,k)*r. % 0.20/0.58 2986[10:MRR:2985.0,2985.1,1.0,23.0] || -> . % 0.20/0.58 2987[8:Spt:2986.0,950.2,2775.0] || equalish(f(f(n)),n)*l -> . % 0.20/0.58 2988[8:Spt:2986.0,950.0,950.1] || element(n,m)* -> equalish(f(n),n). % 0.20/0.58 2995[8:Res:57.2,2988.0] || equalish(n,n) -> equalish(n,k) equalish(f(n),n)*l. % 0.20/0.58 2996[8:MRR:2995.0,2995.1,1.0,23.0] || -> equalish(f(n),n)*l. % 0.20/0.58 3013[8:NCh:3.2,3.0,2996.0,123.1] || equalish(n,n) equalish(n,n) -> equalish(n,k)*r equalish(n,m). % 0.20/0.58 3015[8:Obv:3013.0] || equalish(n,n) -> equalish(n,k)*r equalish(n,m). % 0.20/0.58 3016[8:MRR:3015.0,3015.1,3015.2,1.0,23.0,28.0] || -> . % 0.20/0.58 3017[5:Spt:3016.0,957.0,957.2] || element(n,m)* -> equalish(f(n),n). % 0.20/0.58 3020[5:Res:57.2,3017.0] || equalish(n,n) -> equalish(n,k) equalish(f(n),n)*l. % 0.20/0.58 3021[5:MRR:3020.0,3020.1,1.0,23.0] || -> equalish(f(n),n)*l. % 0.20/0.58 3055[5:NCh:3.2,3.0,3021.0,123.1] || equalish(n,n) equalish(n,n) -> equalish(n,k)*r equalish(n,m). % 0.20/0.58 3057[5:Obv:3055.0] || equalish(n,n) -> equalish(n,k)*r equalish(n,m). % 0.20/0.58 3058[5:MRR:3057.0,3057.1,3057.2,1.0,23.0,28.0] || -> . % 0.20/0.58 % SZS output end Refutation % 0.20/0.58 Formulae used in the proof : reflexivityish symmetryish transitivityish element_substitutionish1 element_substitutionish2 c_3 c_5 c_6 c_7 c_8 c_9 c_10 c_11 c_12 c_13 c_14 c_16 c_17 c_18 c_19 c_20 c_22 c_23 % 0.20/0.58 %------------------------------------------------------------------------------