%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SWV540-1.004 : TPTP v8.1.0. Released v4.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 : Wed Jul 20 21:44:04 EDT 2022 % Result : Unsatisfiable 0.83s 1.06s % Output : Refutation 0.90s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWV540-1.004 : TPTP v8.1.0. Released v4.0.0. % 0.11/0.12 % Command : run_spass %d %s % 0.13/0.33 % Computer : n005.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 600 % 0.13/0.33 % DateTime : Tue Jun 14 19:49:24 EDT 2022 % 0.13/0.33 % CPUTime : % 0.83/1.06 % 0.83/1.06 SPASS V 3.9 % 0.83/1.06 SPASS beiseite: Proof found. % 0.83/1.06 % SZS status Theorem % 0.83/1.06 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.83/1.06 SPASS derived 4592 clauses, backtracked 844 clauses, performed 10 splits and kept 1861 clauses. % 0.83/1.06 SPASS allocated 65914 KBytes. % 0.83/1.06 SPASS spent 0:00:00.72 on the problem. % 0.83/1.06 0:00:00.04 for the input. % 0.83/1.06 0:00:00.00 for the FLOTTER CNF translation. % 0.83/1.06 0:00:00.05 for inferences. % 0.83/1.06 0:00:00.01 for the backtracking. % 0.83/1.06 0:00:00.58 for the reduction. % 0.83/1.06 % 0.83/1.06 % 0.83/1.06 Here is a proof with depth 4, length 304 : % 0.83/1.06 % SZS output start Refutation % 0.83/1.06 1[0:Inp] || -> equal(select(store(u,v,w),v),w)**. % 0.83/1.06 2[0:Inp] || -> equal(u,v) equal(select(store(w,u,x),v),select(w,v))**. % 0.83/1.06 3[0:Inp] || -> equal(store(u,v,select(u,v)),u)**. % 0.83/1.06 4[0:Inp] || -> equal(store(store(u,v,w),v,x),store(u,v,x))**. % 0.83/1.06 5[0:Inp] || -> equal(u,v) equal(store(store(w,u,x),v,y),store(store(w,v,y),u,x))*. % 0.83/1.06 6[0:Inp] || -> equal(store(a1,i1,e_416),a_417)**. % 0.83/1.06 7[0:Inp] || -> equal(store(a_417,i1,e_416),a_418)**. % 0.83/1.06 8[0:Inp] || -> equal(store(a_418,i0,e_419),a_420)**. % 0.83/1.06 9[0:Inp] || -> equal(store(a_420,i3,e_421),a_422)**. % 0.83/1.06 10[0:Inp] || -> equal(store(a_422,i3,e_423),a_424)**. % 0.83/1.06 11[0:Inp] || -> equal(store(a_424,i2,e_425),a_426)**. % 0.83/1.06 12[0:Inp] || -> equal(store(a_426,i2,e_427),a_428)**. % 0.83/1.06 13[0:Inp] || -> equal(store(a_428,i0,e_429),a_430)**. % 0.83/1.06 14[0:Inp] || -> equal(store(a_418,i3,e_421),a_431)**. % 0.83/1.06 15[0:Inp] || -> equal(store(a_431,i0,e_419),a_432)**. % 0.83/1.06 16[0:Inp] || -> equal(store(a_432,i3,e_433),a_434)**. % 0.83/1.06 17[0:Inp] || -> equal(store(a_434,i2,e_435),a_436)**. % 0.83/1.06 18[0:Inp] || -> equal(store(a_436,i0,e_437),a_438)**. % 0.83/1.06 19[0:Inp] || -> equal(store(a_438,i2,e_439),a_440)**. % 0.83/1.06 20[0:Inp] || -> equal(select(a1,i1),e_416)**. % 0.83/1.06 21[0:Inp] || -> equal(select(a_418,i3),e_419)**. % 0.83/1.06 22[0:Inp] || -> equal(select(a_418,i0),e_421)**. % 0.83/1.06 23[0:Inp] || -> equal(select(a_422,i2),e_423)**. % 0.83/1.06 24[0:Inp] || -> equal(select(a_422,i3),e_425)**. % 0.83/1.06 25[0:Inp] || -> equal(select(a_426,i0),e_427)**. % 0.83/1.06 26[0:Inp] || -> equal(select(a_426,i2),e_429)**. % 0.83/1.06 27[0:Inp] || -> equal(select(a_432,i2),e_433)**. % 0.83/1.06 28[0:Inp] || -> equal(select(a_432,i3),e_435)**. % 0.83/1.06 29[0:Inp] || -> equal(select(a_436,i2),e_437)**. % 0.83/1.06 30[0:Inp] || -> equal(select(a_436,i0),e_439)**. % 0.83/1.06 31[0:Inp] || equal(a_440,a_430)** -> . % 0.83/1.06 62[0:SpR:30.0,3.0] || -> equal(store(a_436,i0,e_439),a_436)**. % 0.83/1.06 63[0:SpR:29.0,3.0] || -> equal(store(a_436,i2,e_437),a_436)**. % 0.83/1.06 64[0:SpR:28.0,3.0] || -> equal(store(a_432,i3,e_435),a_432)**. % 0.83/1.06 67[0:SpR:25.0,3.0] || -> equal(store(a_426,i0,e_427),a_426)**. % 0.83/1.06 68[0:SpR:24.0,3.0] || -> equal(store(a_422,i3,e_425),a_422)**. % 0.83/1.06 69[0:SpR:23.0,3.0] || -> equal(store(a_422,i2,e_423),a_422)**. % 0.83/1.06 70[0:SpR:22.0,3.0] || -> equal(store(a_418,i0,e_421),a_418)**. % 0.83/1.06 71[0:SpR:21.0,3.0] || -> equal(store(a_418,i3,e_419),a_418)**. % 0.83/1.06 72[0:SpR:20.0,3.0] || -> equal(store(a1,i1,e_416),a1)**. % 0.83/1.06 73[0:Rew:6.0,72.0] || -> equal(a1,a_417)**. % 0.83/1.06 75[0:Rew:73.0,6.0] || -> equal(store(a_417,i1,e_416),a_417)**. % 0.83/1.06 76[0:Rew:7.0,75.0] || -> equal(a_418,a_417)**. % 0.83/1.06 77[0:Rew:76.0,22.0] || -> equal(select(a_417,i0),e_421)**. % 0.83/1.06 78[0:Rew:76.0,21.0] || -> equal(select(a_417,i3),e_419)**. % 0.83/1.06 79[0:Rew:76.0,14.0] || -> equal(store(a_417,i3,e_421),a_431)**. % 0.83/1.06 80[0:Rew:76.0,8.0] || -> equal(store(a_417,i0,e_419),a_420)**. % 0.83/1.06 82[0:Rew:76.0,70.0] || -> equal(store(a_417,i0,e_421),a_417)**. % 0.83/1.06 83[0:Rew:76.0,71.0] || -> equal(store(a_417,i3,e_419),a_417)**. % 0.83/1.06 107[0:SpR:17.0,1.0] || -> equal(select(a_436,i2),e_435)**. % 0.83/1.06 108[0:SpR:12.0,1.0] || -> equal(select(a_428,i2),e_427)**. % 0.83/1.06 110[0:SpR:11.0,1.0] || -> equal(select(a_426,i2),e_425)**. % 0.83/1.06 111[0:SpR:63.0,1.0] || -> equal(select(a_436,i2),e_437)**. % 0.83/1.06 116[0:SpR:15.0,1.0] || -> equal(select(a_432,i0),e_419)**. % 0.83/1.06 117[0:SpR:80.0,1.0] || -> equal(select(a_420,i0),e_419)**. % 0.83/1.06 121[0:SpR:16.0,1.0] || -> equal(select(a_434,i3),e_433)**. % 0.83/1.06 123[0:SpR:9.0,1.0] || -> equal(select(a_422,i3),e_421)**. % 0.83/1.06 124[0:SpR:79.0,1.0] || -> equal(select(a_431,i3),e_421)**. % 0.83/1.06 126[0:SpR:68.0,1.0] || -> equal(select(a_422,i3),e_425)**. % 0.83/1.06 129[0:Rew:29.0,107.0] || -> equal(e_437,e_435)**. % 0.83/1.06 131[0:Rew:129.0,18.0] || -> equal(store(a_436,i0,e_435),a_438)**. % 0.83/1.06 133[0:Rew:26.0,110.0] || -> equal(e_429,e_425)**. % 0.83/1.06 134[0:Rew:133.0,26.0] || -> equal(select(a_426,i2),e_425)**. % 0.83/1.06 135[0:Rew:133.0,13.0] || -> equal(store(a_428,i0,e_425),a_430)**. % 0.83/1.06 137[0:Rew:129.0,111.0] || -> equal(select(a_436,i2),e_435)**. % 0.83/1.06 140[0:Rew:24.0,123.0] || -> equal(e_425,e_421)**. % 0.83/1.06 142[0:Rew:140.0,11.0] || -> equal(store(a_424,i2,e_421),a_426)**. % 0.83/1.06 146[0:Rew:140.0,126.0] || -> equal(select(a_422,i3),e_421)**. % 0.83/1.06 147[0:Rew:140.0,134.0] || -> equal(select(a_426,i2),e_421)**. % 0.83/1.06 148[0:Rew:140.0,135.0] || -> equal(store(a_428,i0,e_421),a_430)**. % 0.83/1.06 203[0:SpR:12.0,4.0] || -> equal(store(a_428,i2,u),store(a_426,i2,u))**. % 0.83/1.06 207[0:SpR:142.0,4.0] || -> equal(store(a_426,i2,u),store(a_424,i2,u))**. % 0.83/1.06 210[0:SpR:131.0,4.0] || -> equal(store(a_438,i0,u),store(a_436,i0,u))**. % 0.83/1.06 212[0:SpR:80.0,4.0] || -> equal(store(a_420,i0,u),store(a_417,i0,u))**. % 0.83/1.06 218[0:SpR:9.0,4.0] || -> equal(store(a_422,i3,u),store(a_420,i3,u))**. % 0.83/1.06 221[0:SpR:10.0,4.0] || -> equal(store(a_424,i3,u),store(a_422,i3,u))**. % 0.83/1.06 229[0:Rew:207.0,12.0] || -> equal(store(a_424,i2,e_427),a_428)**. % 0.83/1.06 230[0:Rew:207.0,203.0] || -> equal(store(a_428,i2,u),store(a_424,i2,u))**. % 0.83/1.06 236[0:Rew:218.0,10.0] || -> equal(store(a_420,i3,e_423),a_424)**. % 0.83/1.06 239[0:Rew:218.0,221.0] || -> equal(store(a_424,i3,u),store(a_420,i3,u))**. % 0.83/1.06 265[0:SpR:17.0,2.1] || -> equal(i2,u) equal(select(a_436,u),select(a_434,u))**. % 0.83/1.06 269[0:SpR:229.0,2.1] || -> equal(i2,u) equal(select(a_428,u),select(a_424,u))**. % 0.83/1.06 274[0:SpR:15.0,2.1] || -> equal(i0,u) equal(select(a_432,u),select(a_431,u))**. % 0.83/1.06 278[0:SpR:148.0,2.1] || -> equal(i0,u) equal(select(a_430,u),select(a_428,u))**. % 0.83/1.06 279[0:SpR:16.0,2.1] || -> equal(i3,u) equal(select(a_434,u),select(a_432,u))**. % 0.83/1.06 281[0:SpR:9.0,2.1] || -> equal(i3,u) equal(select(a_422,u),select(a_420,u))**. % 0.83/1.06 284[0:SpR:236.0,2.1] || -> equal(i3,u) equal(select(a_424,u),select(a_420,u))**. % 0.83/1.06 340[0:SpR:17.0,5.1] || -> equal(i2,u) equal(store(store(a_434,u,v),i2,e_435),store(a_436,u,v))**. % 0.83/1.06 344[0:SpR:229.0,5.1] || -> equal(i2,u) equal(store(store(a_424,u,v),i2,e_427),store(a_428,u,v))**. % 0.83/1.06 349[0:SpR:131.0,5.1] || -> equal(i0,u) equal(store(store(a_436,u,v),i0,e_435),store(a_438,u,v))**. % 0.83/1.06 350[0:SpR:15.0,5.1] || -> equal(i0,u) equal(store(store(a_431,u,v),i0,e_419),store(a_432,u,v))**. % 0.83/1.06 354[0:SpR:148.0,5.1] || -> equal(i0,u) equal(store(store(a_428,u,v),i0,e_421),store(a_430,u,v))**. % 0.83/1.06 360[0:SpR:9.0,5.1] || -> equal(i3,u) equal(store(store(a_420,u,v),i3,e_421),store(a_422,u,v))**. % 0.83/1.06 361[0:SpR:79.0,5.1] || -> equal(i3,u) equal(store(store(a_417,u,v),i3,e_421),store(a_431,u,v))**. % 0.83/1.06 363[0:SpR:236.0,5.1] || -> equal(i3,u) equal(store(store(a_420,u,v),i3,e_423),store(a_424,u,v))**. % 0.83/1.06 478[0:SpR:265.1,30.0] || -> equal(i2,i0) equal(select(a_434,i0),e_439)**. % 0.83/1.06 480[0:SpR:265.1,3.0] || -> equal(i2,u) equal(store(a_436,u,select(a_434,u)),a_436)**. % 0.83/1.06 482[1:Spt:478.0] || -> equal(i2,i0)**. % 0.83/1.06 483[1:Rew:482.0,27.0] || -> equal(select(a_432,i0),e_433)**. % 0.83/1.06 484[1:Rew:482.0,23.0] || -> equal(select(a_422,i0),e_423)**. % 0.83/1.06 485[1:Rew:482.0,19.0] || -> equal(store(a_438,i0,e_439),a_440)**. % 0.83/1.06 486[1:Rew:482.0,17.0] || -> equal(store(a_434,i0,e_435),a_436)**. % 0.83/1.06 488[1:Rew:482.0,69.0] || -> equal(store(a_422,i0,e_423),a_422)**. % 0.83/1.06 490[1:Rew:482.0,147.0] || -> equal(select(a_426,i0),e_421)**. % 0.83/1.06 492[1:Rew:482.0,137.0] || -> equal(select(a_436,i0),e_435)**. % 0.83/1.06 493[1:Rew:482.0,142.0] || -> equal(store(a_424,i0,e_421),a_426)**. % 0.83/1.06 494[1:Rew:482.0,229.0] || -> equal(store(a_424,i0,e_427),a_428)**. % 0.83/1.06 501[1:Rew:482.0,480.0] || -> equal(i0,u) equal(store(a_436,u,select(a_434,u)),a_436)**. % 0.83/1.06 506[1:Rew:482.0,344.0] || -> equal(i0,u) equal(store(store(a_424,u,v),i2,e_427),store(a_428,u,v))**. % 0.83/1.06 510[1:Rew:482.0,340.0] || -> equal(i0,u) equal(store(store(a_434,u,v),i2,e_435),store(a_436,u,v))**. % 0.83/1.06 512[1:Rew:482.0,269.0] || -> equal(i0,u) equal(select(a_428,u),select(a_424,u))**. % 0.83/1.06 515[1:Rew:116.0,483.0] || -> equal(e_433,e_419)**. % 0.83/1.06 516[1:Rew:515.0,16.0] || -> equal(store(a_432,i3,e_419),a_434)**. % 0.83/1.06 519[1:Rew:25.0,490.0] || -> equal(e_427,e_421)**. % 0.83/1.06 521[1:Rew:519.0,67.0] || -> equal(store(a_426,i0,e_421),a_426)**. % 0.83/1.06 524[1:Rew:30.0,492.0] || -> equal(e_439,e_435)**. % 0.83/1.06 526[1:Rew:524.0,62.0] || -> equal(store(a_436,i0,e_435),a_436)**. % 0.83/1.06 529[1:Rew:210.0,485.0] || -> equal(store(a_436,i0,e_439),a_440)**. % 0.83/1.06 530[1:Rew:524.0,529.0] || -> equal(store(a_436,i0,e_435),a_440)**. % 0.83/1.06 531[1:Rew:131.0,530.0] || -> equal(a_440,a_438)**. % 0.83/1.06 532[1:Rew:531.0,31.0] || equal(a_438,a_430)** -> . % 0.83/1.06 543[1:Rew:493.0,494.0,519.0,494.0] || -> equal(a_428,a_426)**. % 0.83/1.06 544[1:Rew:543.0,148.0] || -> equal(store(a_426,i0,e_421),a_430)**. % 0.83/1.06 550[1:Rew:131.0,526.0] || -> equal(a_438,a_436)**. % 0.83/1.06 558[1:Rew:550.0,532.0] || equal(a_436,a_430)** -> . % 0.83/1.06 559[1:Rew:521.0,544.0] || -> equal(a_430,a_426)**. % 0.83/1.06 561[1:Rew:559.0,558.0] || equal(a_436,a_426)** -> . % 0.83/1.06 568[1:Rew:543.0,512.1] || -> equal(i0,u) equal(select(a_426,u),select(a_424,u))**. % 0.83/1.06 575[1:Rew:482.0,506.1,519.0,506.1,543.0,506.1] || -> equal(i0,u) equal(store(store(a_424,u,v),i0,e_421),store(a_426,u,v))**. % 0.83/1.06 580[1:Rew:482.0,510.1] || -> equal(i0,u) equal(store(store(a_434,u,v),i0,e_435),store(a_436,u,v))**. % 0.83/1.06 658[0:SpR:274.1,28.0] || -> equal(i3,i0) equal(select(a_431,i3),e_435)**. % 0.83/1.06 660[0:SpR:274.1,3.0] || -> equal(i0,u) equal(store(a_432,u,select(a_431,u)),a_432)**. % 0.83/1.06 662[0:Rew:124.0,658.1] || -> equal(i3,i0) equal(e_435,e_421)**. % 0.83/1.06 663[2:Spt:662.0] || -> equal(i3,i0)**. % 0.83/1.06 664[2:Rew:663.0,28.0] || -> equal(select(a_432,i0),e_435)**. % 0.83/1.06 665[2:Rew:663.0,9.0] || -> equal(store(a_420,i0,e_421),a_422)**. % 0.83/1.06 666[2:Rew:663.0,78.0] || -> equal(select(a_417,i0),e_419)**. % 0.83/1.06 667[2:Rew:663.0,79.0] || -> equal(store(a_417,i0,e_421),a_431)**. % 0.83/1.06 668[2:Rew:663.0,64.0] || -> equal(store(a_432,i0,e_435),a_432)**. % 0.83/1.06 671[2:Rew:663.0,146.0] || -> equal(select(a_422,i0),e_421)**. % 0.83/1.06 672[2:Rew:663.0,83.0] || -> equal(store(a_417,i0,e_419),a_417)**. % 0.83/1.06 673[2:Rew:663.0,236.0] || -> equal(store(a_420,i0,e_423),a_424)**. % 0.83/1.06 679[2:Rew:663.0,516.0] || -> equal(store(a_432,i0,e_419),a_434)**. % 0.83/1.06 681[2:Rew:663.0,363.0] || -> equal(i0,u) equal(store(store(a_420,u,v),i3,e_423),store(a_424,u,v))**. % 0.83/1.06 694[2:Rew:116.0,664.0] || -> equal(e_435,e_419)**. % 0.83/1.06 698[2:Rew:694.0,486.0] || -> equal(store(a_434,i0,e_419),a_436)**. % 0.83/1.06 700[2:Rew:77.0,666.0] || -> equal(e_421,e_419)**. % 0.83/1.06 702[2:Rew:700.0,82.0] || -> equal(store(a_417,i0,e_419),a_417)**. % 0.83/1.06 707[2:Rew:700.0,493.0] || -> equal(store(a_424,i0,e_419),a_426)**. % 0.83/1.06 711[2:Rew:484.0,671.0] || -> equal(e_423,e_421)**. % 0.83/1.06 712[2:Rew:700.0,711.0] || -> equal(e_423,e_419)**. % 0.83/1.06 714[2:Rew:712.0,488.0] || -> equal(store(a_422,i0,e_419),a_422)**. % 0.83/1.06 717[2:Rew:212.0,665.0] || -> equal(store(a_417,i0,e_421),a_422)**. % 0.83/1.06 718[2:Rew:700.0,717.0] || -> equal(store(a_417,i0,e_419),a_422)**. % 0.83/1.06 719[2:Rew:80.0,718.0] || -> equal(a_422,a_420)**. % 0.83/1.06 721[2:Rew:700.0,667.0] || -> equal(store(a_417,i0,e_419),a_431)**. % 0.83/1.06 722[2:Rew:80.0,721.0] || -> equal(a_431,a_420)**. % 0.83/1.06 726[2:Rew:722.0,660.1] || -> equal(i0,u) equal(store(a_432,u,select(a_420,u)),a_432)**. % 0.83/1.06 727[2:Rew:722.0,350.1] || -> equal(i0,u) equal(store(store(a_420,u,v),i0,e_419),store(a_432,u,v))**. % 0.83/1.06 730[2:Rew:694.0,668.0] || -> equal(store(a_432,i0,e_419),a_432)**. % 0.83/1.06 731[2:Rew:80.0,672.0] || -> equal(a_420,a_417)**. % 0.83/1.06 738[2:Rew:731.0,719.0] || -> equal(a_422,a_417)**. % 0.83/1.06 740[2:Rew:731.0,673.0,712.0,673.0] || -> equal(store(a_417,i0,e_419),a_424)**. % 0.83/1.06 741[2:Rew:730.0,679.0] || -> equal(a_434,a_432)**. % 0.83/1.06 747[2:Rew:730.0,698.0,741.0,698.0] || -> equal(a_436,a_432)**. % 0.83/1.06 750[2:Rew:747.0,561.0] || equal(a_432,a_426)** -> . % 0.83/1.06 759[2:Rew:740.0,702.0] || -> equal(a_424,a_417)**. % 0.83/1.06 765[2:Rew:759.0,707.0] || -> equal(store(a_417,i0,e_419),a_426)**. % 0.83/1.06 766[2:Rew:765.0,714.0,738.0,714.0] || -> equal(a_426,a_417)**. % 0.83/1.06 770[2:Rew:766.0,750.0] || equal(a_432,a_417)** -> . % 0.83/1.06 796[2:Rew:731.0,726.1] || -> equal(i0,u) equal(store(a_432,u,select(a_417,u)),a_432)**. % 0.83/1.06 801[2:Rew:731.0,681.1,663.0,681.1,712.0,681.1,759.0,681.1] || -> equal(i0,u) equal(store(store(a_417,u,v),i0,e_419),store(a_417,u,v))**. % 0.83/1.06 809[2:Rew:801.1,727.1,731.0,727.1] || -> equal(i0,u) equal(store(a_432,u,v),store(a_417,u,v))**. % 0.83/1.06 811[2:Rew:809.1,796.1] || -> equal(i0,u) equal(store(a_417,u,select(a_417,u)),a_432)**. % 0.83/1.06 812[2:Rew:3.0,811.1] || -> equal(i0,u)* equal(a_432,a_417)**. % 0.83/1.06 813[2:MRR:812.1,770.0] || -> equal(i0,u)*. % 0.83/1.06 819[2:Rew:813.0,1.0] || -> equal(select(i0,u),v)*. % 0.83/1.06 869[2:AED:31.0,819.0] || -> . % 0.83/1.06 888[2:Spt:869.0,662.0,663.0] || equal(i3,i0)** -> . % 0.83/1.06 889[2:Spt:869.0,662.1] || -> equal(e_435,e_421)**. % 0.83/1.06 897[2:Rew:889.0,580.1] || -> equal(i0,u) equal(store(store(a_434,u,v),i0,e_421),store(a_436,u,v))**. % 0.83/1.06 1078[0:SpR:279.1,3.0] || -> equal(i3,u) equal(store(a_434,u,select(a_432,u)),a_434)**. % 0.83/1.06 1081[1:SpR:281.1,484.0] || -> equal(i3,i0) equal(select(a_420,i0),e_423)**. % 0.83/1.06 1082[0:SpR:281.1,3.0] || -> equal(i3,u) equal(store(a_422,u,select(a_420,u)),a_422)**. % 0.83/1.06 1084[1:Rew:117.0,1081.1] || -> equal(i3,i0) equal(e_423,e_419)**. % 0.83/1.06 1085[2:MRR:1084.0,888.0] || -> equal(e_423,e_419)**. % 0.83/1.06 1088[2:Rew:1085.0,236.0] || -> equal(store(a_420,i3,e_419),a_424)**. % 0.83/1.06 1089[2:Rew:1085.0,488.0] || -> equal(store(a_422,i0,e_419),a_422)**. % 0.83/1.06 1206[1:SpR:568.1,3.0] || -> equal(i0,u) equal(store(a_426,u,select(a_424,u)),a_426)**. % 0.83/1.06 1230[0:SpR:212.0,360.1] || -> equal(i3,i0) equal(store(store(a_417,i0,u),i3,e_421),store(a_422,i0,u))**. % 0.83/1.06 1234[0:Rew:361.1,1230.1] || -> equal(i3,i0) equal(store(a_431,i0,u),store(a_422,i0,u))**. % 0.83/1.06 1235[2:MRR:1234.0,888.0] || -> equal(store(a_431,i0,u),store(a_422,i0,u))**. % 0.83/1.06 1237[2:Rew:1235.0,15.0] || -> equal(store(a_422,i0,e_419),a_432)**. % 0.83/1.06 1239[2:Rew:1089.0,1237.0] || -> equal(a_432,a_422)**. % 0.83/1.06 1242[2:Rew:1239.0,516.0] || -> equal(store(a_422,i3,e_419),a_434)**. % 0.83/1.06 1255[2:Rew:1088.0,1242.0,218.0,1242.0] || -> equal(a_434,a_424)**. % 0.83/1.06 1260[2:Rew:1255.0,501.1] || -> equal(i0,u) equal(store(a_436,u,select(a_424,u)),a_436)**. % 0.83/1.06 1261[2:Rew:1255.0,897.1] || -> equal(i0,u) equal(store(store(a_424,u,v),i0,e_421),store(a_436,u,v))**. % 0.83/1.06 1278[2:Rew:575.1,1261.1] || -> equal(i0,u) equal(store(a_436,u,v),store(a_426,u,v))**. % 0.83/1.06 1279[2:Rew:1278.1,1260.1] || -> equal(i0,u) equal(store(a_426,u,select(a_424,u)),a_436)**. % 0.83/1.06 1280[2:Rew:1206.1,1279.1] || -> equal(i0,u)* equal(a_436,a_426)**. % 0.83/1.06 1281[2:MRR:1280.1,561.0] || -> equal(i0,u)*. % 0.83/1.06 1282[2:UnC:1281.0,888.0] || -> . % 0.83/1.06 1293[1:Spt:1282.0,478.0,482.0] || equal(i2,i0)** -> . % 0.83/1.06 1294[1:Spt:1282.0,478.1] || -> equal(select(a_434,i0),e_439)**. % 0.83/1.06 1358[2:Spt:662.0] || -> equal(i3,i0)**. % 0.83/1.06 1359[2:Rew:1358.0,78.0] || -> equal(select(a_417,i0),e_419)**. % 0.83/1.06 1362[2:Rew:1358.0,79.0] || -> equal(store(a_417,i0,e_421),a_431)**. % 0.83/1.06 1363[2:Rew:1358.0,83.0] || -> equal(store(a_417,i0,e_419),a_417)**. % 0.83/1.06 1364[2:Rew:1358.0,9.0] || -> equal(store(a_420,i0,e_421),a_422)**. % 0.83/1.06 1365[2:Rew:1358.0,239.0] || -> equal(store(a_424,i0,u),store(a_420,i0,u))**. % 0.83/1.06 1372[2:Rew:1358.0,28.0] || -> equal(select(a_432,i0),e_435)**. % 0.83/1.06 1374[2:Rew:1358.0,121.0] || -> equal(select(a_434,i0),e_433)**. % 0.83/1.06 1376[2:Rew:1358.0,236.0] || -> equal(store(a_420,i0,e_423),a_424)**. % 0.83/1.06 1381[2:Rew:1358.0,1078.0] || -> equal(i0,u) equal(store(a_434,u,select(a_432,u)),a_434)**. % 0.83/1.06 1394[2:Rew:1358.0,16.0] || -> equal(store(a_432,i0,e_433),a_434)**. % 0.83/1.06 1397[2:Rew:77.0,1359.0] || -> equal(e_421,e_419)**. % 0.83/1.06 1401[2:Rew:1397.0,82.0] || -> equal(store(a_417,i0,e_419),a_417)**. % 0.83/1.06 1405[2:Rew:1397.0,142.0] || -> equal(store(a_424,i2,e_419),a_426)**. % 0.83/1.06 1406[2:Rew:1397.0,148.0] || -> equal(store(a_428,i0,e_419),a_430)**. % 0.83/1.06 1411[2:Rew:116.0,1372.0] || -> equal(e_435,e_419)**. % 0.83/1.06 1415[2:Rew:1411.0,17.0] || -> equal(store(a_434,i2,e_419),a_436)**. % 0.83/1.06 1418[2:Rew:1411.0,349.1] || -> equal(i0,u) equal(store(store(a_436,u,v),i0,e_419),store(a_438,u,v))**. % 0.83/1.06 1419[2:Rew:1294.0,1374.0] || -> equal(e_439,e_433)**. % 0.83/1.06 1422[2:Rew:1419.0,30.0] || -> equal(select(a_436,i0),e_433)**. % 0.83/1.06 1423[2:Rew:1419.0,19.0] || -> equal(store(a_438,i2,e_433),a_440)**. % 0.83/1.06 1428[2:Rew:1397.0,1362.0] || -> equal(store(a_417,i0,e_419),a_431)**. % 0.83/1.06 1429[2:Rew:80.0,1428.0] || -> equal(a_431,a_420)**. % 0.83/1.06 1430[2:Rew:1429.0,15.0] || -> equal(store(a_420,i0,e_419),a_432)**. % 0.83/1.06 1438[2:Rew:80.0,1363.0] || -> equal(a_420,a_417)**. % 0.83/1.06 1440[2:Rew:1438.0,80.0] || -> equal(store(a_417,i0,e_419),a_417)**. % 0.83/1.06 1447[2:Rew:1438.0,1364.0,1397.0,1364.0] || -> equal(store(a_417,i0,e_419),a_422)**. % 0.83/1.06 1449[2:Rew:1438.0,1376.0] || -> equal(store(a_417,i0,e_423),a_424)**. % 0.83/1.06 1450[2:Rew:1447.0,1401.0] || -> equal(a_422,a_417)**. % 0.83/1.06 1451[2:Rew:1450.0,23.0] || -> equal(select(a_417,i2),e_423)**. % 0.83/1.06 1453[2:Rew:1450.0,69.0] || -> equal(store(a_417,i2,e_423),a_417)**. % 0.83/1.06 1455[2:Rew:1450.0,1447.0] || -> equal(store(a_417,i0,e_419),a_417)**. % 0.90/1.08 1456[2:Rew:1438.0,1430.0] || -> equal(store(a_417,i0,e_419),a_432)**. % 0.90/1.08 1457[2:Rew:1456.0,1440.0] || -> equal(a_432,a_417)**. % 0.90/1.08 1459[2:Rew:1457.0,27.0] || -> equal(select(a_417,i2),e_433)**. % 0.90/1.08 1463[2:Rew:1457.0,1394.0] || -> equal(store(a_417,i0,e_433),a_434)**. % 0.90/1.08 1465[2:Rew:1451.0,1459.0] || -> equal(e_433,e_423)**. % 0.90/1.08 1469[2:Rew:1465.0,1422.0] || -> equal(select(a_436,i0),e_423)**. % 0.90/1.08 1470[2:Rew:1465.0,1423.0] || -> equal(store(a_438,i2,e_423),a_440)**. % 0.90/1.08 1474[2:Rew:1449.0,1463.0,1465.0,1463.0] || -> equal(a_434,a_424)**. % 0.90/1.08 1479[2:Rew:1474.0,1415.0] || -> equal(store(a_424,i2,e_419),a_436)**. % 0.90/1.08 1482[2:Rew:1405.0,1479.0] || -> equal(a_436,a_426)**. % 0.90/1.08 1488[2:Rew:1482.0,1469.0] || -> equal(select(a_426,i0),e_423)**. % 0.90/1.08 1490[2:Rew:25.0,1488.0] || -> equal(e_427,e_423)**. % 0.90/1.08 1493[2:Rew:1490.0,229.0] || -> equal(store(a_424,i2,e_423),a_428)**. % 0.90/1.08 1498[2:Rew:1438.0,1365.0] || -> equal(store(a_424,i0,u),store(a_417,i0,u))**. % 0.90/1.08 1511[2:Rew:1457.0,1381.1,1474.0,1381.1] || -> equal(i0,u) equal(store(a_424,u,select(a_417,u)),a_424)**. % 0.90/1.08 1526[2:Rew:1482.0,1418.1] || -> equal(i0,u) equal(store(store(a_426,u,v),i0,e_419),store(a_438,u,v))**. % 0.90/1.08 1719[0:SpR:278.1,3.0] || -> equal(i0,u) equal(store(a_430,u,select(a_428,u)),a_430)**. % 0.90/1.08 2366[2:SpR:1451.0,1511.1] || -> equal(i2,i0) equal(store(a_424,i2,e_423),a_424)**. % 0.90/1.08 2368[2:Rew:1493.0,2366.1] || -> equal(i2,i0) equal(a_428,a_424)**. % 0.90/1.08 2369[2:MRR:2368.0,1293.0] || -> equal(a_428,a_424)**. % 0.90/1.08 2372[2:Rew:2369.0,1406.0] || -> equal(store(a_424,i0,e_419),a_430)**. % 0.90/1.08 2383[2:Rew:1455.0,2372.0,1498.0,2372.0] || -> equal(a_430,a_417)**. % 0.90/1.08 2384[2:Rew:2383.0,31.0] || equal(a_440,a_417)** -> . % 0.90/1.08 2496[2:SpR:207.0,1526.1] || -> equal(i2,i0) equal(store(store(a_424,i2,u),i0,e_419),store(a_438,i2,u))**. % 0.90/1.08 2501[2:Rew:1455.0,2496.1,1498.0,2496.1,5.1,2496.1] || -> equal(i2,i0) equal(store(a_438,i2,u),store(a_417,i2,u))**. % 0.90/1.08 2502[2:MRR:2501.0,1293.0] || -> equal(store(a_438,i2,u),store(a_417,i2,u))**. % 0.90/1.08 2504[2:Rew:2502.0,1470.0] || -> equal(store(a_417,i2,e_423),a_440)**. % 0.90/1.08 2506[2:Rew:1453.0,2504.0] || -> equal(a_440,a_417)**. % 0.90/1.08 2507[2:MRR:2506.0,2384.0] || -> . % 0.90/1.08 2508[2:Spt:2507.0,662.0,1358.0] || equal(i3,i0)** -> . % 0.90/1.08 2509[2:Spt:2507.0,662.1] || -> equal(e_435,e_421)**. % 0.90/1.08 2516[2:Rew:2509.0,17.0] || -> equal(store(a_434,i2,e_421),a_436)**. % 0.90/1.08 2523[2:MRR:1234.0,2508.0] || -> equal(store(a_431,i0,u),store(a_422,i0,u))**. % 0.90/1.08 2525[2:Rew:2523.0,15.0] || -> equal(store(a_422,i0,e_419),a_432)**. % 0.90/1.08 2527[2:Rew:2509.0,349.1] || -> equal(i0,u) equal(store(store(a_436,u,v),i0,e_421),store(a_438,u,v))**. % 0.90/1.08 3902[0:SpR:117.0,1082.1] || -> equal(i3,i0) equal(store(a_422,i0,e_419),a_422)**. % 0.90/1.08 4191[2:Rew:2525.0,3902.1] || -> equal(i3,i0) equal(a_432,a_422)**. % 0.90/1.08 4192[2:MRR:4191.0,2508.0] || -> equal(a_432,a_422)**. % 0.90/1.08 4193[2:Rew:4192.0,27.0] || -> equal(select(a_422,i2),e_433)**. % 0.90/1.08 4197[2:Rew:4192.0,16.0] || -> equal(store(a_422,i3,e_433),a_434)**. % 0.90/1.08 4202[2:Rew:23.0,4193.0] || -> equal(e_433,e_423)**. % 0.90/1.08 4205[2:Rew:218.0,4197.0] || -> equal(store(a_420,i3,e_433),a_434)**. % 0.90/1.08 4206[2:Rew:236.0,4205.0,4202.0,4205.0] || -> equal(a_434,a_424)**. % 0.90/1.08 4207[2:Rew:4206.0,1294.0] || -> equal(select(a_424,i0),e_439)**. % 0.90/1.08 4208[2:Rew:4206.0,2516.0] || -> equal(store(a_424,i2,e_421),a_436)**. % 0.90/1.08 4213[2:Rew:142.0,4208.0] || -> equal(a_436,a_426)**. % 0.90/1.08 4215[2:Rew:4213.0,30.0] || -> equal(select(a_426,i0),e_439)**. % 0.90/1.08 4219[2:Rew:25.0,4215.0] || -> equal(e_439,e_427)**. % 0.90/1.08 4221[2:Rew:4219.0,19.0] || -> equal(store(a_438,i2,e_427),a_440)**. % 0.90/1.08 4222[2:Rew:4219.0,4207.0] || -> equal(select(a_424,i0),e_427)**. % 0.90/1.08 4246[2:Rew:4213.0,2527.1] || -> equal(i0,u) equal(store(store(a_426,u,v),i0,e_421),store(a_438,u,v))**. % 0.90/1.08 5123[2:SpR:4222.0,284.1] || -> equal(i3,i0) equal(select(a_420,i0),e_427)**. % 0.90/1.08 5127[2:Rew:117.0,5123.1] || -> equal(i3,i0) equal(e_427,e_419)**. % 0.90/1.08 5128[2:MRR:5127.0,2508.0] || -> equal(e_427,e_419)**. % 0.90/1.08 5133[2:Rew:5128.0,108.0] || -> equal(select(a_428,i2),e_419)**. % 0.90/1.08 5136[2:Rew:5128.0,4221.0] || -> equal(store(a_438,i2,e_419),a_440)**. % 0.90/1.08 5687[2:SpR:207.0,4246.1] || -> equal(i2,i0) equal(store(store(a_424,i2,u),i0,e_421),store(a_438,i2,u))**. % 0.90/1.08 5694[2:Rew:5.1,5687.1] || -> equal(i2,i0) equal(store(store(a_424,i0,e_421),i2,u),store(a_438,i2,u))**. % 0.90/1.08 5695[2:MRR:5694.0,1293.0] || -> equal(store(store(a_424,i0,e_421),i2,u),store(a_438,i2,u))**. % 0.90/1.08 5732[0:SpR:230.0,354.1] || -> equal(i2,i0) equal(store(store(a_424,i2,u),i0,e_421),store(a_430,i2,u))**. % 0.90/1.08 5738[0:Rew:5.1,5732.1] || -> equal(i2,i0) equal(store(store(a_424,i0,e_421),i2,u),store(a_430,i2,u))**. % 0.90/1.08 5739[2:Rew:5695.0,5738.1] || -> equal(i2,i0) equal(store(a_438,i2,u),store(a_430,i2,u))**. % 0.90/1.08 5740[2:MRR:5739.0,1293.0] || -> equal(store(a_438,i2,u),store(a_430,i2,u))**. % 0.90/1.08 5755[2:Rew:5740.0,5136.0] || -> equal(store(a_430,i2,e_419),a_440)**. % 0.90/1.08 5801[2:SpR:5133.0,1719.1] || -> equal(i2,i0) equal(store(a_430,i2,e_419),a_430)**. % 0.90/1.08 5804[2:Rew:5755.0,5801.1] || -> equal(i2,i0) equal(a_440,a_430)**. % 0.90/1.08 5805[2:MRR:5804.0,5804.1,1293.0,31.0] || -> . % 0.90/1.08 % SZS output end Refutation % 0.90/1.08 Formulae used in the proof : a1 a2 a3 a4 a5 hyp0 hyp1 hyp2 hyp3 hyp4 hyp5 hyp6 hyp7 hyp8 hyp9 hyp10 hyp11 hyp12 hyp13 hyp14 hyp15 hyp16 hyp17 hyp18 hyp19 hyp20 hyp21 hyp22 hyp23 hyp24 goal % 0.90/1.08 %------------------------------------------------------------------------------