%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : COL106-2 : TPTP v8.1.0. Released v3.2.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n020.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 : Fri Jul 15 00:42:40 EDT 2022 % Result : Unsatisfiable 0.46s 0.66s % Output : Refutation 0.46s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : COL106-2 : TPTP v8.1.0. Released v3.2.0. % 0.07/0.12 % Command : run_spass %d %s % 0.12/0.33 % Computer : n020.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Tue May 31 06:05:08 EDT 2022 % 0.12/0.33 % CPUTime : % 0.46/0.66 % 0.46/0.66 SPASS V 3.9 % 0.46/0.66 SPASS beiseite: Proof found. % 0.46/0.66 % SZS status Theorem % 0.46/0.66 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.46/0.66 SPASS derived 614 clauses, backtracked 83 clauses, performed 6 splits and kept 347 clauses. % 0.46/0.66 SPASS allocated 64432 KBytes. % 0.46/0.66 SPASS spent 0:00:00.32 on the problem. % 0.46/0.66 0:00:00.03 for the input. % 0.46/0.66 0:00:00.00 for the FLOTTER CNF translation. % 0.46/0.66 0:00:00.02 for inferences. % 0.46/0.66 0:00:00.01 for the backtracking. % 0.46/0.66 0:00:00.23 for the reduction. % 0.46/0.66 % 0.46/0.66 % 0.46/0.66 Here is a proof with depth 7, length 71 : % 0.46/0.66 % SZS output start Refutation % 0.46/0.66 1[0:Inp] || c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(u,v),w,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))*+ -> equal(w,c_Comb_Ocomb_Oop_A_D_D(u,v)) equal(u,c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,w)) equal(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(u,v,w)),v_sko__uTG(u,v,w)),u)** equal(c_Comb_Ocomb_Oop_A_D_D(v_sko__uTI(u,v,w),v_sko__uTH(u,v,w)),w). % 0.46/0.66 2[0:Inp] || c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(u,v),w,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))+ -> equal(w,c_Comb_Ocomb_Oop_A_D_D(u,v)) equal(u,c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,w)) equal(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(u,v,w)),v_sko__uTG(u,v,w)),u)** c_in(c_Pair(u,v_sko__uTI(u,v,w),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))*. % 0.46/0.66 3[0:Inp] || equal(c_Comb_Ocomb_Oop_A_D_D(u,v),c_Comb_Ocomb_OK)** -> . % 0.46/0.66 4[0:Inp] || equal(c_Comb_Ocomb_Oop_A_D_D(u,v),c_Comb_Ocomb_Oop_A_D_D(w,x))* -> equal(u,w). % 0.46/0.66 5[0:Inp] || equal(c_Comb_Ocomb_Oop_A_D_D(u,v),c_Comb_Ocomb_Oop_A_D_D(w,x))* -> equal(v,x). % 0.46/0.66 6[0:Inp] || c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,u),v,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))* -> equal(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_sko__uTE(u,v)),v). % 0.46/0.66 7[0:Inp] || c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,u),v,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))*+ -> c_in(c_Pair(u,v_sko__uTE(u,v),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))*. % 0.46/0.66 8[0:Inp] || -> c_in(c_Pair(u,u,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))*. % 0.46/0.66 9[0:Inp] || -> c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,u),v),u,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))*. % 0.46/0.66 10[0:Inp] || c_in(c_Pair(u,v,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) c_in(c_Pair(w,x,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) -> c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(u,w),c_Comb_Ocomb_Oop_A_D_D(v,x),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))*. % 0.46/0.66 11[0:Inp] || -> c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya),v_xb,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))*. % 0.46/0.66 12[0:Inp] || c_in(c_Pair(v_x,u,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) c_in(c_Pair(v_xb,u,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))* -> . % 0.46/0.66 18[0:Res:8.0,12.1] || c_in(c_Pair(v_xb,v_x,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))* -> . % 0.46/0.66 73[0:Res:10.2,6.0] || c_in(c_Pair(c_Comb_Ocomb_OK,u,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))*+ c_in(c_Pair(v,w,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))* -> equal(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_sko__uTE(v,c_Comb_Ocomb_Oop_A_D_D(u,w))),c_Comb_Ocomb_Oop_A_D_D(u,w))**. % 0.46/0.66 74[0:Res:8.0,73.0] || c_in(c_Pair(u,v,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))* -> equal(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_sko__uTE(u,c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v))),c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v)). % 0.46/0.66 76[0:Res:9.0,74.0] || -> equal(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_sko__uTE(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,u),v),c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,u))),c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,u))**. % 0.46/0.66 77[0:Res:11.0,74.0] || -> equal(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_sko__uTE(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya),c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xb))),c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xb))**. % 0.46/0.66 87[0:SpL:77.0,5.0] || equal(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xb),c_Comb_Ocomb_Oop_A_D_D(u,v))*+ -> equal(v_sko__uTE(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya),c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xb)),v)*. % 0.46/0.66 95[0:Res:11.0,1.0] || -> equal(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya),v_xb) equal(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xb),c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x)) equal(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)),v_sko__uTG(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)),c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x))** equal(c_Comb_Ocomb_Oop_A_D_D(v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb),v_sko__uTH(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)),v_xb). % 0.46/0.66 109[0:SpL:76.0,5.0] || equal(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,u),c_Comb_Ocomb_Oop_A_D_D(v,w))*+ -> equal(v_sko__uTE(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,u),x),c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,u)),w)*. % 0.46/0.66 117[0:EqR:87.0] || -> equal(v_sko__uTE(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya),c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xb)),v_xb)**. % 0.46/0.66 131[0:EqR:109.0] || -> equal(v_sko__uTE(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,u),v),c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,u)),u)**. % 0.46/0.66 147[0:Res:11.0,2.0] || -> equal(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya),v_xb) equal(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xb),c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x)) equal(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)),v_sko__uTG(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)),c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x)) c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))*. % 0.46/0.66 167[1:Spt:95.0] || -> equal(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya),v_xb)**. % 0.46/0.66 173[1:SpR:167.0,9.0] || -> c_in(c_Pair(v_xb,v_x,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))*. % 0.46/0.66 184[1:MRR:173.0,18.0] || -> . % 0.46/0.66 187[1:Spt:184.0,95.0,167.0] || equal(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya),v_xb)** -> . % 0.46/0.66 188[1:Spt:184.0,95.1,95.2,95.3] || -> equal(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xb),c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x)) equal(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)),v_sko__uTG(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)),c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x))** equal(c_Comb_Ocomb_Oop_A_D_D(v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb),v_sko__uTH(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)),v_xb). % 0.46/0.66 189[1:MRR:147.0,187.0] || -> equal(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xb),c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x)) equal(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)),v_sko__uTG(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)),c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x)) c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))*. % 0.46/0.66 190[2:Spt:188.0] || -> equal(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xb),c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x))**. % 0.46/0.66 191[2:Rew:190.0,117.0] || -> equal(v_sko__uTE(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya),c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x)),v_xb)**. % 0.46/0.66 192[2:Rew:131.0,191.0] || -> equal(v_xb,v_x)**. % 0.46/0.66 195[2:Rew:192.0,12.1] || c_in(c_Pair(v_x,u,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))* c_in(c_Pair(v_x,u,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))* -> . % 0.46/0.66 202[2:Obv:195.0] || c_in(c_Pair(v_x,u,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))* -> . % 0.46/0.66 203[2:UnC:202.0,8.0] || -> . % 0.46/0.66 206[2:Spt:203.0,188.0,190.0] || equal(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xb),c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x))** -> . % 0.46/0.66 207[2:Spt:203.0,188.1,188.2] || -> equal(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)),v_sko__uTG(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)),c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x))** equal(c_Comb_Ocomb_Oop_A_D_D(v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb),v_sko__uTH(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)),v_xb). % 0.46/0.66 208[2:MRR:189.0,206.0] || -> equal(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)),v_sko__uTG(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)),c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x)) c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))*. % 0.46/0.66 219[2:SpL:207.0,5.0] || equal(c_Comb_Ocomb_Oop_A_D_D(u,v),c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x))*+ -> equal(c_Comb_Ocomb_Oop_A_D_D(v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb),v_sko__uTH(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)),v_xb)** equal(v,v_sko__uTG(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb))*. % 0.46/0.66 230[3:Spt:219.0,219.2] || equal(c_Comb_Ocomb_Oop_A_D_D(u,v),c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x))*+ -> equal(v,v_sko__uTG(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb))*. % 0.46/0.66 231[3:EqR:230.0] || -> equal(v_sko__uTG(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb),v_x)**. % 0.46/0.66 233[3:Rew:231.0,207.0] || -> equal(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)),v_x),c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x)) equal(c_Comb_Ocomb_Oop_A_D_D(v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb),v_sko__uTH(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)),v_xb)**. % 0.46/0.66 235[3:Rew:231.0,208.0] || -> equal(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)),v_x),c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x)) c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))*. % 0.46/0.66 245[3:Res:235.1,7.0] || -> equal(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)),v_x),c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x)) c_in(c_Pair(v_x,v_sko__uTE(v_x,v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))*. % 0.46/0.66 246[3:Res:235.1,6.0] || -> equal(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)),v_x),c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x))** equal(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_sko__uTE(v_x,v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb))),v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)). % 0.46/0.66 251[4:Spt:233.0] || -> equal(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)),v_x),c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x))**. % 0.46/0.66 257[4:SpL:251.0,4.0] || equal(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),c_Comb_Ocomb_Oop_A_D_D(u,v))*+ -> equal(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)),u)*. % 0.46/0.66 265[4:EqR:257.0] || -> equal(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)),c_Comb_Ocomb_OK)**. % 0.46/0.66 267[4:MRR:265.0,3.0] || -> . % 0.46/0.66 268[4:Spt:267.0,233.0,251.0] || equal(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)),v_x),c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x))** -> . % 0.46/0.66 269[4:Spt:267.0,233.1] || -> equal(c_Comb_Ocomb_Oop_A_D_D(v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb),v_sko__uTH(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)),v_xb)**. % 0.46/0.66 270[4:MRR:245.0,268.0] || -> c_in(c_Pair(v_x,v_sko__uTE(v_x,v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))*. % 0.46/0.66 271[4:MRR:246.0,268.0] || -> equal(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_sko__uTE(v_x,v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb))),v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb))**. % 0.46/0.66 296[4:SpR:271.0,9.0] || -> c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb),u),v_sko__uTE(v_x,v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))*. % 0.46/0.66 433[4:SpR:269.0,296.0] || -> c_in(c_Pair(v_xb,v_sko__uTE(v_x,v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))*. % 0.46/0.66 438[4:Res:433.0,12.1] || c_in(c_Pair(v_x,v_sko__uTE(v_x,v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))* -> . % 0.46/0.66 440[4:MRR:438.0,270.0] || -> . % 0.46/0.66 442[3:Spt:440.0,219.1] || -> equal(c_Comb_Ocomb_Oop_A_D_D(v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb),v_sko__uTH(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)),v_xb)**. % 0.46/0.66 464[2:Res:208.1,7.0] || -> equal(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)),v_sko__uTG(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)),c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x)) c_in(c_Pair(v_x,v_sko__uTE(v_x,v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))*. % 0.46/0.66 465[2:Res:208.1,6.0] || -> equal(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)),v_sko__uTG(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)),c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x))** equal(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_sko__uTE(v_x,v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb))),v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)). % 0.46/0.66 473[4:Spt:465.0] || -> equal(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)),v_sko__uTG(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)),c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x))**. % 0.46/0.66 481[4:SpL:473.0,4.0] || equal(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),c_Comb_Ocomb_Oop_A_D_D(u,v))*+ -> equal(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)),u)*. % 0.46/0.66 538[4:EqR:481.0] || -> equal(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)),c_Comb_Ocomb_OK)**. % 0.46/0.66 543[4:MRR:538.0,3.0] || -> . % 0.46/0.66 544[4:Spt:543.0,465.0,473.0] || equal(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)),v_sko__uTG(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)),c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x))** -> . % 0.46/0.67 545[4:Spt:543.0,465.1] || -> equal(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_sko__uTE(v_x,v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb))),v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb))**. % 0.46/0.67 546[4:MRR:464.0,544.0] || -> c_in(c_Pair(v_x,v_sko__uTE(v_x,v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))*. % 0.46/0.67 556[4:SpR:545.0,9.0] || -> c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb),u),v_sko__uTE(v_x,v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))*. % 0.46/0.67 826[4:SpR:442.0,556.0] || -> c_in(c_Pair(v_xb,v_sko__uTE(v_x,v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))*. % 0.46/0.67 833[4:Res:826.0,12.1] || c_in(c_Pair(v_x,v_sko__uTE(v_x,v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))* -> . % 0.46/0.67 835[4:MRR:833.0,546.0] || -> . % 0.46/0.67 % SZS output end Refutation % 0.46/0.67 Formulae used in the proof : cls_Comb_OAp__parcontractE_0 cls_Comb_OAp__parcontractE_2 cls_Comb_Ocomb_Odistinct__3__iff1_0 cls_Comb_Ocomb_Oinject__iff1_0 cls_Comb_Ocomb_Oinject__iff1_1 cls_Comb_OK1__parcontractD__dest_0 cls_Comb_OK1__parcontractD__dest_1 cls_Comb_Oparcontract_Ointros__1_0 cls_Comb_Oparcontract_Ointros__2_0 cls_Comb_Oparcontract_Ointros__4_0 cls_conjecture_0 cls_conjecture_1 % 0.46/0.67 %------------------------------------------------------------------------------