%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : NLP009+1 : TPTP v8.1.0. Released v2.4.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n028.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 : Mon Jul 18 05:25:34 EDT 2022 % Result : Theorem 0.19s 0.46s % Output : Refutation 0.19s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : NLP009+1 : TPTP v8.1.0. Released v2.4.0. % 0.07/0.13 % Command : run_spass %d %s % 0.13/0.33 % Computer : n028.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 : Fri Jul 1 00:48:30 EDT 2022 % 0.13/0.33 % CPUTime : % 0.19/0.46 % 0.19/0.46 SPASS V 3.9 % 0.19/0.46 SPASS beiseite: Proof found. % 0.19/0.46 % SZS status Theorem % 0.19/0.46 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.19/0.46 SPASS derived 38 clauses, backtracked 42 clauses, performed 3 splits and kept 111 clauses. % 0.19/0.46 SPASS allocated 104002 KBytes. % 0.19/0.46 SPASS spent 0:00:00.12 on the problem. % 0.19/0.46 0:00:00.04 for the input. % 0.19/0.46 0:00:00.04 for the FLOTTER CNF translation. % 0.19/0.46 0:00:00.00 for inferences. % 0.19/0.46 0:00:00.00 for the backtracking. % 0.19/0.46 0:00:00.01 for the reduction. % 0.19/0.46 % 0.19/0.46 % 0.19/0.46 Here is a proof with depth 4, length 121 : % 0.19/0.46 % SZS output start Refutation % 0.19/0.46 1[0:Inp] || -> hollywood(skc27)*. % 0.19/0.46 2[0:Inp] || -> event(skc26)*. % 0.19/0.46 3[0:Inp] || -> street(skc25)*. % 0.19/0.46 4[0:Inp] || -> old(skc24)*. % 0.19/0.46 5[0:Inp] || -> seat(skc23)*. % 0.19/0.46 6[0:Inp] || -> young(skc22)*. % 0.19/0.46 7[0:Inp] || -> fellow(skc21)*. % 0.19/0.46 8[0:Inp] || -> hollywood(skc20)*. % 0.19/0.46 9[0:Inp] || -> event(skc19)*. % 0.19/0.46 10[0:Inp] || -> chevy(skc18)*. % 0.19/0.46 11[0:Inp] || -> lonely(skc17)*. % 0.19/0.46 12[0:Inp] || -> seat(skc16)*. % 0.19/0.46 13[0:Inp] || -> young(skc15)*. % 0.19/0.46 14[0:Inp] || -> fellow(skc14)*. % 0.19/0.46 15[0:Inp] || -> SkC0 furniture(skc23)*. % 0.19/0.46 16[0:Inp] || -> SkC0 front(skc23)*. % 0.19/0.46 17[0:Inp] || -> SkC0 man(skc22)*. % 0.19/0.46 18[0:Inp] || -> SkC0 fellow(skc22)*. % 0.19/0.46 19[0:Inp] || -> SkC0 man(skc21)*. % 0.19/0.46 20[0:Inp] || -> SkC0 young(skc21)*. % 0.19/0.46 21[0:Inp] || -> SkC0 city(skc27)*. % 0.19/0.46 22[0:Inp] || -> SkC0 way(skc25)*. % 0.19/0.46 23[0:Inp] || -> SkC0 lonely(skc25)*. % 0.19/0.46 24[0:Inp] || -> SkC0 dirty(skc24)*. % 0.19/0.46 25[0:Inp] || -> SkC0 white(skc24)*. % 0.19/0.46 26[0:Inp] || -> SkC0 car(skc24)*. % 0.19/0.46 27[0:Inp] || -> SkC0 chevy(skc24)*. % 0.19/0.46 28[0:Inp] || SkC0 -> furniture(skc16)*. % 0.19/0.46 29[0:Inp] || SkC0 -> front(skc16)*. % 0.19/0.46 30[0:Inp] || SkC0 -> man(skc15)*. % 0.19/0.46 31[0:Inp] || SkC0 -> fellow(skc15)*. % 0.19/0.46 32[0:Inp] || SkC0 -> man(skc14)*. % 0.19/0.46 33[0:Inp] || SkC0 -> young(skc14)*. % 0.19/0.46 34[0:Inp] || SkC0 -> city(skc20)*. % 0.19/0.46 35[0:Inp] || SkC0 -> car(skc18)*. % 0.19/0.46 36[0:Inp] || SkC0 -> white(skc18)*. % 0.19/0.46 37[0:Inp] || SkC0 -> dirty(skc18)*. % 0.19/0.46 38[0:Inp] || SkC0 -> old(skc18)*. % 0.19/0.46 39[0:Inp] || SkC0 -> way(skc17)*. % 0.19/0.46 40[0:Inp] || SkC0 -> street(skc17)*. % 0.19/0.46 41[0:Inp] || -> SkC0 in(skc22,skc23)*. % 0.19/0.46 42[0:Inp] || -> SkC0 in(skc21,skc23)*. % 0.19/0.46 43[0:Inp] || -> SkC0 in(skc26,skc27)*. % 0.19/0.46 44[0:Inp] || -> SkC0 down(skc26,skc25)*. % 0.19/0.46 45[0:Inp] || -> SkC0 barrel(skc26,skc24)*. % 0.19/0.46 46[0:Inp] || SkC0 -> in(skc15,skc16)*. % 0.19/0.46 47[0:Inp] || SkC0 -> in(skc14,skc16)*. % 0.19/0.46 48[0:Inp] || SkC0 -> in(skc19,skc20)*. % 0.19/0.46 49[0:Inp] || SkC0 -> down(skc19,skc17)*. % 0.19/0.46 50[0:Inp] || SkC0 -> barrel(skc19,skc18)*. % 0.19/0.46 51[0:Inp] || equal(skc22,skc21) -> SkC0*. % 0.19/0.46 52[0:Inp] || SkC0* equal(skc15,skc14) -> . % 0.19/0.46 53[0:Inp] seat(u) furniture(u) front(u) young(v) man(v) fellow(v) fellow(w) man(w) young(w) hollywood(x) city(x) event(y) chevy(z) car(z) white(z) dirty(z) old(z) lonely(x1) way(x1) street(x1) || barrel(y,z)* in(v,u)* in(w,u)* in(y,x)* down(y,x1)* -> equal(v,w)* SkC0. % 0.19/0.46 54[0:Inp] seat(u) furniture(u) front(u) young(v) man(v) fellow(v) fellow(w) man(w) young(w) hollywood(x) city(x) event(y) street(z) way(z) lonely(z) old(x1) dirty(x1) white(x1) car(x1) chevy(x1) || barrel(y,x1)* in(v,u)* in(w,u)* in(y,x)* down(y,z)* SkC0 -> equal(v,w)*. % 0.19/0.46 55[0:MRR:54.25,53.26] chevy(u) car(u) white(u) dirty(u) old(u) lonely(v) way(v) street(v) event(w) city(x) hollywood(x) young(y) man(y) fellow(y) fellow(z) man(z) young(z) front(x1) furniture(x1) seat(x1) || down(w,v)*+ in(w,x)* in(y,x1)* in(z,x1)* barrel(w,u)* -> equal(z,y)*. % 0.19/0.46 96[1:Spt:27.0] || -> SkC0*. % 0.19/0.46 97[1:MRR:40.0,96.0] || -> street(skc17)*. % 0.19/0.46 98[1:MRR:39.0,96.0] || -> way(skc17)*. % 0.19/0.46 99[1:MRR:38.0,96.0] || -> old(skc18)*. % 0.19/0.46 100[1:MRR:37.0,96.0] || -> dirty(skc18)*. % 0.19/0.46 101[1:MRR:36.0,96.0] || -> white(skc18)*. % 0.19/0.46 102[1:MRR:35.0,96.0] || -> car(skc18)*. % 0.19/0.46 103[1:MRR:34.0,96.0] || -> city(skc20)*. % 0.19/0.46 104[1:MRR:33.0,96.0] || -> young(skc14)*. % 0.19/0.46 105[1:MRR:32.0,96.0] || -> man(skc14)*. % 0.19/0.46 106[1:MRR:31.0,96.0] || -> fellow(skc15)*. % 0.19/0.46 107[1:MRR:30.0,96.0] || -> man(skc15)*. % 0.19/0.46 108[1:MRR:29.0,96.0] || -> front(skc16)*. % 0.19/0.46 109[1:MRR:28.0,96.0] || -> furniture(skc16)*. % 0.19/0.46 110[1:MRR:50.0,96.0] || -> barrel(skc19,skc18)*. % 0.19/0.46 111[1:MRR:49.0,96.0] || -> down(skc19,skc17)*. % 0.19/0.46 112[1:MRR:48.0,96.0] || -> in(skc19,skc20)*. % 0.19/0.46 113[1:MRR:47.0,96.0] || -> in(skc14,skc16)*. % 0.19/0.46 114[1:MRR:46.0,96.0] || -> in(skc15,skc16)*. % 0.19/0.46 115[1:MRR:52.0,96.0] || equal(skc15,skc14)**+ -> . % 0.19/0.46 116[2:Spt:55.11,55.12,55.13,55.14,55.15,55.16,55.17,55.18,55.19,55.22,55.23,55.25] young(u) man(u) fellow(u) fellow(v) man(v) young(v) front(w) furniture(w) seat(w) || in(u,w)*+ in(v,w)* -> equal(v,u)*. % 0.19/0.46 118[2:Res:113.0,116.9] young(skc14) man(skc14) fellow(skc14) fellow(u) man(u) young(u) front(skc16) furniture(skc16) seat(skc16) || in(u,skc16)* -> equal(u,skc14). % 0.19/0.46 119[2:SSi:118.8,118.7,118.6,118.2,118.1,118.0,12.0,108.0,109.0,12.0,108.0,109.0,12.0,108.0,109.0,14.0,104.0,105.0,14.0,104.0,105.0,14.0,104.0,105.0] fellow(u) man(u) young(u) || in(u,skc16)*+ -> equal(u,skc14). % 0.19/0.46 123[2:Res:114.0,119.3] fellow(skc15) man(skc15) young(skc15) || -> equal(skc15,skc14)**. % 0.19/0.46 124[2:SSi:123.2,123.1,123.0,13.0,106.0,107.0,13.0,106.0,107.0,13.0,106.0,107.0] || -> equal(skc15,skc14)**. % 0.19/0.46 125[2:MRR:124.0,115.0] || -> . % 0.19/0.46 126[2:Spt:125.0,55.0,55.1,55.2,55.3,55.4,55.5,55.6,55.7,55.8,55.9,55.10,55.20,55.21,55.24] chevy(u) car(u) white(u) dirty(u) old(u) lonely(v) way(v) street(v) event(w) city(x) hollywood(x) || down(w,v)*+ in(w,x)* barrel(w,u)* -> . % 0.19/0.46 127[2:Res:111.0,126.11] chevy(u) car(u) white(u) dirty(u) old(u) lonely(skc17) way(skc17) street(skc17) event(skc19) city(v) hollywood(v) || in(skc19,v)* barrel(skc19,u)* -> . % 0.19/0.46 128[2:SSi:127.8,127.7,127.6,127.5,9.0,11.0,97.0,98.0,11.0,97.0,98.0,11.0,97.0,98.0] chevy(u) car(u) white(u) dirty(u) old(u) city(v) hollywood(v) || in(skc19,v)*+ barrel(skc19,u)* -> . % 0.19/0.46 129[2:Res:112.0,128.7] chevy(u) car(u) white(u) dirty(u) old(u) city(skc20) hollywood(skc20) || barrel(skc19,u)* -> . % 0.19/0.46 130[2:SSi:129.6,129.5,8.0,103.0,8.0,103.0] chevy(u) car(u) white(u) dirty(u) old(u) || barrel(skc19,u)*+ -> . % 0.19/0.46 131[2:Res:110.0,130.5] chevy(skc18) car(skc18) white(skc18) dirty(skc18) old(skc18) || -> . % 0.19/0.46 132[2:SSi:131.4,131.3,131.2,131.1,131.0,10.0,99.0,100.0,101.0,102.0,10.0,99.0,100.0,101.0,102.0,10.0,99.0,100.0,101.0,102.0,10.0,99.0,100.0,101.0,102.0,10.0,99.0,100.0,101.0,102.0] || -> . % 0.19/0.46 133[1:Spt:132.0,27.0,96.0] || SkC0*+ -> . % 0.19/0.46 134[1:Spt:132.0,27.1] || -> chevy(skc24)*. % 0.19/0.46 135[1:MRR:26.0,133.0] || -> car(skc24)*. % 0.19/0.46 136[1:MRR:25.0,133.0] || -> white(skc24)*. % 0.19/0.46 137[1:MRR:24.0,133.0] || -> dirty(skc24)*. % 0.19/0.46 138[1:MRR:23.0,133.0] || -> lonely(skc25)*. % 0.19/0.46 139[1:MRR:22.0,133.0] || -> way(skc25)*. % 0.19/0.46 140[1:MRR:21.0,133.0] || -> city(skc27)*. % 0.19/0.46 141[1:MRR:20.0,133.0] || -> young(skc21)*. % 0.19/0.46 142[1:MRR:19.0,133.0] || -> man(skc21)*. % 0.19/0.46 143[1:MRR:18.0,133.0] || -> fellow(skc22)*. % 0.19/0.46 144[1:MRR:17.0,133.0] || -> man(skc22)*. % 0.19/0.46 145[1:MRR:16.0,133.0] || -> front(skc23)*. % 0.19/0.46 146[1:MRR:15.0,133.0] || -> furniture(skc23)*. % 0.19/0.46 147[1:MRR:45.0,133.0] || -> barrel(skc26,skc24)*. % 0.19/0.46 148[1:MRR:44.0,133.0] || -> down(skc26,skc25)*. % 0.19/0.46 149[1:MRR:43.0,133.0] || -> in(skc26,skc27)*. % 0.19/0.46 150[1:MRR:42.0,133.0] || -> in(skc21,skc23)*. % 0.19/0.46 151[1:MRR:41.0,133.0] || -> in(skc22,skc23)*. % 0.19/0.46 152[1:MRR:51.1,133.0] || equal(skc22,skc21)**+ -> . % 0.19/0.46 153[2:Spt:55.11,55.12,55.13,55.14,55.15,55.16,55.17,55.18,55.19,55.22,55.23,55.25] young(u) man(u) fellow(u) fellow(v) man(v) young(v) front(w) furniture(w) seat(w) || in(u,w)*+ in(v,w)* -> equal(v,u)*. % 0.19/0.46 155[2:Res:150.0,153.9] young(skc21) man(skc21) fellow(skc21) fellow(u) man(u) young(u) front(skc23) furniture(skc23) seat(skc23) || in(u,skc23)* -> equal(u,skc21). % 0.19/0.46 156[2:SSi:155.8,155.7,155.6,155.2,155.1,155.0,5.0,145.0,146.0,5.0,145.0,146.0,5.0,145.0,146.0,7.0,141.0,142.0,7.0,141.0,142.0,7.0,141.0,142.0] fellow(u) man(u) young(u) || in(u,skc23)*+ -> equal(u,skc21). % 0.19/0.46 160[2:Res:151.0,156.3] fellow(skc22) man(skc22) young(skc22) || -> equal(skc22,skc21)**. % 0.19/0.46 161[2:SSi:160.2,160.1,160.0,6.0,143.0,144.0,6.0,143.0,144.0,6.0,143.0,144.0] || -> equal(skc22,skc21)**. % 0.19/0.46 162[2:MRR:161.0,152.0] || -> . % 0.19/0.46 163[2:Spt:162.0,55.0,55.1,55.2,55.3,55.4,55.5,55.6,55.7,55.8,55.9,55.10,55.20,55.21,55.24] chevy(u) car(u) white(u) dirty(u) old(u) lonely(v) way(v) street(v) event(w) city(x) hollywood(x) || down(w,v)*+ in(w,x)* barrel(w,u)* -> . % 0.19/0.46 164[2:Res:148.0,163.11] chevy(u) car(u) white(u) dirty(u) old(u) lonely(skc25) way(skc25) street(skc25) event(skc26) city(v) hollywood(v) || in(skc26,v)* barrel(skc26,u)* -> . % 0.19/0.46 165[2:SSi:164.8,164.7,164.6,164.5,2.0,3.0,138.0,139.0,3.0,138.0,139.0,3.0,138.0,139.0] chevy(u) car(u) white(u) dirty(u) old(u) city(v) hollywood(v) || in(skc26,v)*+ barrel(skc26,u)* -> . % 0.19/0.47 166[2:Res:149.0,165.7] chevy(u) car(u) white(u) dirty(u) old(u) city(skc27) hollywood(skc27) || barrel(skc26,u)* -> . % 0.19/0.47 167[2:SSi:166.6,166.5,1.0,140.0,1.0,140.0] chevy(u) car(u) white(u) dirty(u) old(u) || barrel(skc26,u)*+ -> . % 0.19/0.47 168[2:Res:147.0,167.5] chevy(skc24) car(skc24) white(skc24) dirty(skc24) old(skc24) || -> . % 0.19/0.47 169[2:SSi:168.4,168.3,168.2,168.1,168.0,4.0,134.0,135.0,136.0,137.0,4.0,134.0,135.0,136.0,137.0,4.0,134.0,135.0,136.0,137.0,4.0,134.0,135.0,136.0,137.0,4.0,134.0,135.0,136.0,137.0] || -> . % 0.19/0.47 % SZS output end Refutation % 0.19/0.47 Formulae used in the proof : co1 % 0.19/0.47 %------------------------------------------------------------------------------