%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : SYN417+1 : TPTP v8.1.0. Released v2.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:21:13 EDT 2022 % Result : Theorem 0.19s 0.47s % Output : Refutation 0.19s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.14 % Problem : SYN417+1 : TPTP v8.1.0. Released v2.0.0. % 0.07/0.15 % Command : run_spass %d %s % 0.13/0.36 % Computer : n009.cluster.edu % 0.13/0.36 % Model : x86_64 x86_64 % 0.13/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.36 % Memory : 8042.1875MB % 0.13/0.36 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.36 % CPULimit : 300 % 0.13/0.36 % WCLimit : 600 % 0.13/0.36 % DateTime : Tue Jul 12 02:39:52 EDT 2022 % 0.13/0.36 % CPUTime : % 0.19/0.47 % 0.19/0.47 SPASS V 3.9 % 0.19/0.47 SPASS beiseite: Proof found. % 0.19/0.47 % SZS status Theorem % 0.19/0.47 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.19/0.47 SPASS derived 52 clauses, backtracked 18 clauses, performed 7 splits and kept 53 clauses. % 0.19/0.47 SPASS allocated 85169 KBytes. % 0.19/0.47 SPASS spent 0:00:00.10 on the problem. % 0.19/0.47 0:00:00.04 for the input. % 0.19/0.47 0:00:00.03 for the FLOTTER CNF translation. % 0.19/0.47 0:00:00.00 for inferences. % 0.19/0.47 0:00:00.00 for the backtracking. % 0.19/0.47 0:00:00.00 for the reduction. % 0.19/0.47 % 0.19/0.47 % 0.19/0.47 Here is a proof with depth 4, length 55 : % 0.19/0.47 % SZS output start Refutation % 0.19/0.47 1[0:Inp] || equal(skf5(u),u)** -> . % 0.19/0.47 2[0:Inp] || equal(skf4(u),u)** -> . % 0.19/0.47 3[0:Inp] || -> equal(f(g(skc2)),skc2)** equal(g(f(skc3)),skc3). % 0.19/0.47 4[0:Inp] || equal(f(g(u)),u)** -> equal(skc2,u) equal(g(f(skc3)),skc3). % 0.19/0.47 5[0:Inp] || equal(g(f(u)),u)**+ -> equal(skc3,u) equal(f(g(skc2)),skc2)**. % 0.19/0.47 6[0:Inp] || equal(g(f(u)),u)**+ equal(f(g(v)),v)** -> equal(skc3,u) equal(skc2,v). % 0.19/0.47 7[0:Inp] || equal(g(f(u)),u)+ equal(f(g(v)),v) -> equal(g(f(skf5(u))),skf5(u))** equal(f(g(skf4(v))),skf4(v))**. % 0.19/0.47 8[1:Spt:6.1,6.3] || equal(f(g(u)),u)** -> equal(skc2,u). % 0.19/0.47 9[2:Spt:5.2] || -> equal(f(g(skc2)),skc2)**. % 0.19/0.47 12[3:Spt:7.1,7.3] || equal(f(g(u)),u) -> equal(f(g(skf4(u))),skf4(u))**. % 0.19/0.47 14[3:SpL:12.1,8.0] || equal(f(g(u)),u)** equal(skf4(u),skf4(u)) -> equal(skf4(u),skc2). % 0.19/0.47 15[3:Obv:14.1] || equal(f(g(u)),u)** -> equal(skf4(u),skc2). % 0.19/0.47 17[3:SpL:9.0,15.0] || equal(skc2,skc2) -> equal(skf4(skc2),skc2)**. % 0.19/0.47 18[3:Obv:17.0] || -> equal(skf4(skc2),skc2)**. % 0.19/0.47 19[3:MRR:18.0,2.0] || -> . % 0.19/0.47 20[3:Spt:19.0,7.0,7.2] || equal(g(f(u)),u) -> equal(g(f(skf5(u))),skf5(u))**. % 0.19/0.47 22[3:SpL:20.1,8.0] || equal(g(f(u)),u) equal(f(skf5(u)),f(skf5(u)))* -> equal(f(skf5(u)),skc2). % 0.19/0.47 23[3:Obv:22.1] || equal(g(f(u)),u) -> equal(f(skf5(u)),skc2)**. % 0.19/0.47 24[3:Rew:23.1,20.1] || equal(g(f(u)),u)** -> equal(skf5(u),g(skc2)). % 0.19/0.47 26[3:SpL:9.0,24.0] || equal(g(skc2),g(skc2)) -> equal(skf5(g(skc2)),g(skc2))**. % 0.19/0.47 27[3:Obv:26.0] || -> equal(skf5(g(skc2)),g(skc2))**. % 0.19/0.47 28[3:MRR:27.0,1.0] || -> . % 0.19/0.47 29[2:Spt:28.0,5.2,9.0] || equal(f(g(skc2)),skc2)** -> . % 0.19/0.47 30[2:Spt:28.0,5.0,5.1] || equal(g(f(u)),u)** -> equal(skc3,u). % 0.19/0.47 31[2:MRR:3.0,29.0] || -> equal(g(f(skc3)),skc3)**. % 0.19/0.47 49[2:SpL:31.0,8.0] || equal(f(skc3),f(skc3))* -> equal(f(skc3),skc2). % 0.19/0.47 50[2:Obv:49.0] || -> equal(f(skc3),skc2)**. % 0.19/0.47 51[2:Rew:50.0,31.0] || -> equal(g(skc2),skc3)**. % 0.19/0.47 52[2:Rew:51.0,29.0] || equal(f(skc3),skc2)** -> . % 0.19/0.47 53[2:Rew:50.0,52.0] || equal(skc2,skc2)* -> . % 0.19/0.47 54[2:Obv:53.0] || -> . % 0.19/0.47 55[1:Spt:54.0,6.0,6.2] || equal(g(f(u)),u)** -> equal(skc3,u). % 0.19/0.47 56[2:Spt:4.2] || -> equal(g(f(skc3)),skc3)**. % 0.19/0.47 59[2:SpL:56.0,7.0] || equal(skc3,skc3) equal(f(g(u)),u) -> equal(g(f(skf5(skc3))),skf5(skc3)) equal(f(g(skf4(u))),skf4(u))**. % 0.19/0.47 60[2:Obv:59.0] || equal(f(g(u)),u) -> equal(g(f(skf5(skc3))),skf5(skc3)) equal(f(g(skf4(u))),skf4(u))**. % 0.19/0.47 63[2:SpL:60.2,55.0] || equal(f(g(u)),u)** equal(g(skf4(u)),g(skf4(u))) -> equal(g(f(skf5(skc3))),skf5(skc3))** equal(g(skf4(u)),skc3). % 0.19/0.47 64[2:Obv:63.1] || equal(f(g(u)),u)** -> equal(g(f(skf5(skc3))),skf5(skc3))** equal(g(skf4(u)),skc3). % 0.19/0.47 65[2:Rew:64.2,60.2] || equal(f(g(u)),u)**+ -> equal(g(f(skf5(skc3))),skf5(skc3))** equal(skf4(u),f(skc3)). % 0.19/0.47 71[3:Spt:65.0,65.2] || equal(f(g(u)),u)** -> equal(skf4(u),f(skc3)). % 0.19/0.47 74[3:SpL:56.0,71.0] || equal(f(skc3),f(skc3)) -> equal(skf4(f(skc3)),f(skc3))**. % 0.19/0.47 75[3:Obv:74.0] || -> equal(skf4(f(skc3)),f(skc3))**. % 0.19/0.47 76[3:MRR:75.0,2.0] || -> . % 0.19/0.47 77[3:Spt:76.0,65.1] || -> equal(g(f(skf5(skc3))),skf5(skc3))**. % 0.19/0.47 79[3:SpL:77.0,55.0] || equal(skf5(skc3),skf5(skc3))* -> equal(skf5(skc3),skc3). % 0.19/0.47 80[3:Obv:79.0] || -> equal(skf5(skc3),skc3)**. % 0.19/0.47 81[3:MRR:80.0,1.0] || -> . % 0.19/0.47 82[2:Spt:81.0,4.2,56.0] || equal(g(f(skc3)),skc3)** -> . % 0.19/0.47 83[2:Spt:81.0,4.0,4.1] || equal(f(g(u)),u)** -> equal(skc2,u). % 0.19/0.47 84[2:MRR:3.1,82.0] || -> equal(f(g(skc2)),skc2)**. % 0.19/0.47 94[2:SpL:84.0,55.0] || equal(g(skc2),g(skc2))* -> equal(g(skc2),skc3). % 0.19/0.47 96[2:Obv:94.0] || -> equal(g(skc2),skc3)**. % 0.19/0.47 97[2:Rew:96.0,84.0] || -> equal(f(skc3),skc2)**. % 0.19/0.47 98[2:Rew:97.0,82.0] || equal(g(skc2),skc3)** -> . % 0.19/0.47 99[2:Rew:96.0,98.0] || equal(skc3,skc3)* -> . % 0.19/0.47 100[2:Obv:99.0] || -> . % 0.19/0.47 % SZS output end Refutation % 0.19/0.47 Formulae used in the proof : cute % 0.19/0.47 %------------------------------------------------------------------------------