%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : COL106-2 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n007.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 12:09:09 PM UTC 2026
% Result : Unsatisfiable 4.73s 1.05s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : COL106-2 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n007.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Mon Sep 21 14:09:20 UTC 2026
% 0.08/0.37 % CPUTime :
% 0.08/0.37 % Drodi V4.1.1
% 4.73/1.05 % Refutation found
% 4.73/1.05 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 4.73/1.05 % SZS output start CNFRefutation for theBenchmark
% 4.73/1.05 fof(f1,negated_conjecture,(
% 4.73/1.05 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)) ),
% 4.73/1.05 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.73/1.05 fof(f2,negated_conjecture,(
% 4.73/1.05 (![V_U]: (( ~ c_in(c_Pair(v_xb,V_U,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))| ~ c_in(c_Pair(v_x,V_U,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) ) ))),
% 4.73/1.05 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.73/1.05 fof(f3,axiom,(
% 4.73/1.05 (![V_p,V_q,V_r]: (( ~ c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(V_p,V_q),V_r,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))| V_r = c_Comb_Ocomb_Oop_A_D_D(V_p,V_q)| V_p = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,V_r)| V_p = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(V_p,V_q,V_r)),v_sko__uTG(V_p,V_q,V_r))| V_r = c_Comb_Ocomb_Oop_A_D_D(v_sko__uTI(V_p,V_q,V_r),v_sko__uTH(V_p,V_q,V_r)) ) ))),
% 4.73/1.05 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.73/1.05 fof(f4,axiom,(
% 4.73/1.05 (![V_p,V_q,V_r]: (( ~ c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(V_p,V_q),V_r,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))| c_in(c_Pair(V_p,v_sko__uTI(V_p,V_q,V_r),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))| V_r = c_Comb_Ocomb_Oop_A_D_D(V_p,V_q)| V_p = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,V_r)| V_p = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(V_p,V_q,V_r)),v_sko__uTG(V_p,V_q,V_r)) ) ))),
% 4.73/1.05 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.73/1.05 fof(f5,axiom,(
% 4.73/1.05 (![V_comb1_H,V_comb2_H]: (c_Comb_Ocomb_OK != c_Comb_Ocomb_Oop_A_D_D(V_comb1_H,V_comb2_H) ))),
% 4.73/1.05 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.73/1.05 fof(f6,axiom,(
% 4.73/1.05 (![V_comb1,V_comb2,V_comb1_H,V_comb2_H]: (( c_Comb_Ocomb_Oop_A_D_D(V_comb1,V_comb2) != c_Comb_Ocomb_Oop_A_D_D(V_comb1_H,V_comb2_H)| V_comb1 = V_comb1_H ) ))),
% 4.73/1.05 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.73/1.05 fof(f7,axiom,(
% 4.73/1.05 (![V_comb1,V_comb2,V_comb1_H,V_comb2_H]: (( c_Comb_Ocomb_Oop_A_D_D(V_comb1,V_comb2) != c_Comb_Ocomb_Oop_A_D_D(V_comb1_H,V_comb2_H)| V_comb2 = V_comb2_H ) ))),
% 4.73/1.05 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.73/1.05 fof(f8,axiom,(
% 4.73/1.05 (![V_x,V_z]: (( ~ c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,V_x),V_z,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))| V_z = c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_sko__uTE(V_x,V_z)) ) ))),
% 4.73/1.05 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.73/1.05 fof(f9,axiom,(
% 4.73/1.05 (![V_x,V_z]: (( ~ c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,V_x),V_z,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))| c_in(c_Pair(V_x,v_sko__uTE(V_x,V_z),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) ) ))),
% 4.73/1.05 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.73/1.05 fof(f10,axiom,(
% 4.73/1.05 (![V_x]: (c_in(c_Pair(V_x,V_x,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) ))),
% 4.73/1.05 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.73/1.05 fof(f11,axiom,(
% 4.73/1.05 (![V_x,V_y]: (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_y),V_x,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) ))),
% 4.73/1.05 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.73/1.05 fof(f12,axiom,(
% 4.73/1.05 (![V_z,V_w,V_x,V_y]: (( ~ c_in(c_Pair(V_z,V_w,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))| ~ c_in(c_Pair(V_x,V_y,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(V_x,V_z),c_Comb_Ocomb_Oop_A_D_D(V_y,V_w),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) ) ))),
% 4.73/1.05 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 4.73/1.05 fof(f13,plain,(
% 4.73/1.05 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))),
% 4.73/1.05 inference(cnf_transformation,[status(thm)],[f1])).
% 4.73/1.05 fof(f14,plain,(
% 4.73/1.05 ![X0]: (~c_in(c_Pair(v_xb,X0,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))|~c_in(c_Pair(v_x,X0,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)))),
% 4.73/1.05 inference(cnf_transformation,[status(thm)],[f2])).
% 4.73/1.05 fof(f15,plain,(
% 4.73/1.05 ![X0,X1,X2]: (~c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(X0,X1),X2,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))|X2=c_Comb_Ocomb_Oop_A_D_D(X0,X1)|X0=c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,X2)|X0=c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(X0,X1,X2)),v_sko__uTG(X0,X1,X2))|X2=c_Comb_Ocomb_Oop_A_D_D(v_sko__uTI(X0,X1,X2),v_sko__uTH(X0,X1,X2)))),
% 4.73/1.05 inference(cnf_transformation,[status(thm)],[f3])).
% 4.73/1.05 fof(f16,plain,(
% 4.73/1.05 ![X0,X1,X2]: (~c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(X0,X1),X2,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))|c_in(c_Pair(X0,v_sko__uTI(X0,X1,X2),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))|X2=c_Comb_Ocomb_Oop_A_D_D(X0,X1)|X0=c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,X2)|X0=c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OS,v_sko__uTF(X0,X1,X2)),v_sko__uTG(X0,X1,X2)))),
% 4.73/1.05 inference(cnf_transformation,[status(thm)],[f4])).
% 4.73/1.05 fof(f17,plain,(
% 4.73/1.05 ![X0,X1]: (~c_Comb_Ocomb_OK=c_Comb_Ocomb_Oop_A_D_D(X0,X1))),
% 4.73/1.05 inference(cnf_transformation,[status(thm)],[f5])).
% 4.73/1.05 fof(f18,plain,(
% 4.73/1.05 ![V_comb1,V_comb1_H]: ((![V_comb2,V_comb2_H]: ~c_Comb_Ocomb_Oop_A_D_D(V_comb1,V_comb2)=c_Comb_Ocomb_Oop_A_D_D(V_comb1_H,V_comb2_H))|V_comb1=V_comb1_H)),
% 4.73/1.05 inference(miniscoping,[status(thm)],[f6])).
% 4.73/1.05 fof(f19,plain,(
% 4.73/1.05 ![X0,X1,X2,X3]: (~c_Comb_Ocomb_Oop_A_D_D(X0,X1)=c_Comb_Ocomb_Oop_A_D_D(X2,X3)|X0=X2)),
% 4.73/1.05 inference(cnf_transformation,[status(thm)],[f18])).
% 4.73/1.05 fof(f20,plain,(
% 4.73/1.05 ![V_comb2,V_comb2_H]: ((![V_comb1,V_comb1_H]: ~c_Comb_Ocomb_Oop_A_D_D(V_comb1,V_comb2)=c_Comb_Ocomb_Oop_A_D_D(V_comb1_H,V_comb2_H))|V_comb2=V_comb2_H)),
% 4.73/1.05 inference(miniscoping,[status(thm)],[f7])).
% 4.73/1.05 fof(f21,plain,(
% 4.73/1.05 ![X0,X1,X2,X3]: (~c_Comb_Ocomb_Oop_A_D_D(X0,X1)=c_Comb_Ocomb_Oop_A_D_D(X2,X3)|X1=X3)),
% 4.73/1.05 inference(cnf_transformation,[status(thm)],[f20])).
% 4.73/1.05 fof(f22,plain,(
% 4.73/1.05 ![X0,X1]: (~c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,X0),X1,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))|X1=c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_sko__uTE(X0,X1)))),
% 4.73/1.05 inference(cnf_transformation,[status(thm)],[f8])).
% 4.73/1.05 fof(f23,plain,(
% 4.73/1.05 ![X0,X1]: (~c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,X0),X1,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))|c_in(c_Pair(X0,v_sko__uTE(X0,X1),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)))),
% 4.73/1.05 inference(cnf_transformation,[status(thm)],[f9])).
% 4.73/1.05 fof(f24,plain,(
% 4.73/1.05 ![X0]: (c_in(c_Pair(X0,X0,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)))),
% 4.73/1.05 inference(cnf_transformation,[status(thm)],[f10])).
% 4.73/1.05 fof(f25,plain,(
% 4.73/1.05 ![X0,X1]: (c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,X0),X1),X0,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)))),
% 4.73/1.05 inference(cnf_transformation,[status(thm)],[f11])).
% 4.73/1.05 fof(f26,plain,(
% 4.73/1.05 ![X0,X1,X2,X3]: (~c_in(c_Pair(X0,X1,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))|~c_in(c_Pair(X2,X3,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(X2,X0),c_Comb_Ocomb_Oop_A_D_D(X3,X1),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)))),
% 4.73/1.05 inference(cnf_transformation,[status(thm)],[f12])).
% 4.73/1.05 fof(f27,plain,(
% 4.73/1.05 ~c_in(c_Pair(v_x,v_xb,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))),
% 4.73/1.05 inference(resolution,[status(thm)],[f24,f14])).
% 4.73/1.05 fof(f30,plain,(
% 4.73/1.05 ![X0,X1,X2]: (c_Comb_Ocomb_Oop_A_D_D(X0,X1)=c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_sko__uTE(X2,c_Comb_Ocomb_Oop_A_D_D(X0,X1)))|~c_in(c_Pair(X2,X1,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))|~c_in(c_Pair(c_Comb_Ocomb_OK,X0,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)))),
% 4.73/1.05 inference(resolution,[status(thm)],[f22,f26])).
% 4.73/1.05 fof(f53,plain,(
% 4.73/1.05 ![X0,X1]: (c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,X0)=c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_sko__uTE(X1,c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,X0)))|~c_in(c_Pair(X1,X0,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)))),
% 4.73/1.05 inference(resolution,[status(thm)],[f30,f24])).
% 4.73/1.05 fof(f56,plain,(
% 4.73/1.05 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_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)))),
% 4.73/1.05 inference(resolution,[status(thm)],[f53,f13])).
% 4.73/1.05 fof(f57,plain,(
% 4.73/1.05 ![X0,X1]: (c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,X0)=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,X0),X1),c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,X0))))),
% 4.73/1.05 inference(resolution,[status(thm)],[f53,f25])).
% 4.73/1.05 fof(f60,plain,(
% 4.73/1.05 ![X0,X1]: (X0=v_sko__uTE(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,X0),X1),c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,X0)))),
% 4.73/1.05 inference(resolution,[status(thm)],[f57,f21])).
% 4.73/1.05 fof(f83,plain,(
% 4.73/1.05 v_xb=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))),
% 4.73/1.05 inference(resolution,[status(thm)],[f56,f21])).
% 4.73/1.05 fof(f113,plain,(
% 4.73/1.05 v_xb=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)=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)=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))|v_xb=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))),
% 4.73/1.05 inference(resolution,[status(thm)],[f15,f13])).
% 4.73/1.05 fof(f117,plain,(
% 4.73/1.05 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))|v_xb=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)=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)=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))),
% 4.73/1.05 inference(resolution,[status(thm)],[f16,f13])).
% 4.73/1.05 fof(f126,plain,(
% 4.73/1.05 v_xb=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)=c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xb)|v_xb=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))|c_Comb_Ocomb_OK=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))),
% 4.73/1.05 inference(resolution,[status(thm)],[f113,f19])).
% 4.73/1.05 fof(f138,plain,(
% 4.73/1.05 v_xb=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)=c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xb)|v_xb=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))),
% 4.73/1.05 inference(forward_subsumption_resolution,[status(thm)],[f126,f17])).
% 4.73/1.05 fof(f149,plain,(
% 4.73/1.05 v_xb=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)=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)=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_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))),
% 4.73/1.05 inference(resolution,[status(thm)],[f117,f23])).
% 4.73/1.05 fof(f150,plain,(
% 4.73/1.05 v_xb=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)=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)=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))|v_sko__uTI(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_sko__uTE(v_x,v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)))),
% 4.73/1.05 inference(resolution,[status(thm)],[f117,f22])).
% 4.73/1.05 fof(f362,plain,(
% 4.73/1.05 v_xb=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)=c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xb)|v_sko__uTI(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_sko__uTE(v_x,v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)))|c_Comb_Ocomb_OK=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))),
% 4.73/1.05 inference(resolution,[status(thm)],[f150,f19])).
% 4.73/1.05 fof(f375,plain,(
% 4.73/1.05 v_xb=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)=c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xb)|v_sko__uTI(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_sko__uTE(v_x,v_sko__uTI(c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x),v_ya,v_xb)))),
% 4.73/1.05 inference(forward_subsumption_resolution,[status(thm)],[f362,f17])).
% 4.73/1.05 fof(f391,plain,(
% 4.73/1.05 ![X0]: (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),X0),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))|v_xb=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)=c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xb))),
% 4.73/1.05 inference(paramodulation,[status(thm)],[f375,f25])).
% 4.73/1.05 fof(f725,plain,(
% 4.73/1.05 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))|v_xb=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)=c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xb)|v_xb=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)=c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xb)),
% 4.73/1.05 inference(paramodulation,[status(thm)],[f138,f391])).
% 4.73/1.05 fof(f730,plain,(
% 4.73/1.05 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))|v_xb=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)=c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xb)),
% 4.73/1.05 inference(duplicate_literals_removal,[status(thm)],[f725])).
% 4.73/1.05 fof(f731,plain,(
% 4.73/1.05 v_xb=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)=c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xb)|~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))),
% 4.73/1.05 inference(resolution,[status(thm)],[f730,f14])).
% 4.73/1.05 fof(f758,plain,(
% 4.73/1.05 v_xb=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)=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)=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))),
% 4.73/1.05 inference(backward_subsumption_resolution,[status(thm)],[f149,f731])).
% 4.73/1.05 fof(f760,plain,(
% 4.73/1.05 v_xb=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)=c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xb)|c_Comb_Ocomb_OK=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))),
% 4.73/1.05 inference(resolution,[status(thm)],[f758,f19])).
% 4.73/1.05 fof(f776,plain,(
% 4.73/1.05 v_xb=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)=c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xb)),
% 4.73/1.05 inference(forward_subsumption_resolution,[status(thm)],[f760,f17])).
% 4.73/1.05 fof(f799,plain,(
% 4.73/1.05 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))|c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x)=c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xb)),
% 4.73/1.05 inference(paramodulation,[status(thm)],[f776,f25])).
% 4.73/1.05 fof(f820,plain,(
% 4.73/1.05 c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x)=c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xb)|~c_in(c_Pair(v_x,v_x,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))),
% 4.73/1.05 inference(resolution,[status(thm)],[f799,f14])).
% 4.73/1.05 fof(f837,plain,(
% 4.73/1.05 c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_x)=c_Comb_Ocomb_Oop_A_D_D(c_Comb_Ocomb_OK,v_xb)),
% 4.73/1.05 inference(forward_subsumption_resolution,[status(thm)],[f820,f24])).
% 4.73/1.05 fof(f845,plain,(
% 4.73/1.05 v_xb=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))),
% 4.73/1.05 inference(backward_demodulation,[status(thm)],[f837,f83])).
% 4.73/1.05 fof(f876,plain,(
% 4.73/1.05 v_xb=v_x),
% 4.73/1.05 inference(forward_demodulation,[status(thm)],[f60,f845])).
% 4.73/1.05 fof(f919,plain,(
% 4.73/1.05 ~c_in(c_Pair(v_x,v_x,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))),
% 4.73/1.05 inference(backward_demodulation,[status(thm)],[f876,f27])).
% 4.73/1.05 fof(f941,plain,(
% 4.73/1.05 $false),
% 4.73/1.05 inference(forward_subsumption_resolution,[status(thm)],[f919,f24])).
% 4.73/1.05 % SZS output end CNFRefutation for theBenchmark.p
% 4.73/1.07 % Elapsed time: 0.691833 seconds
% 4.73/1.07 % CPU time: 5.159792 seconds
% 4.73/1.07 % Total memory used: 202.883 MB
% 4.73/1.07 % Net memory used: 198.312 MB
%------------------------------------------------------------------------------