%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : COL106-1 : 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 : n003.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 6.34s 1.42s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : COL106-1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/0.43 % Computer : n003.cluster.edu
% 0.18/0.43 % Model : x86_64 x86_64
% 0.18/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.43 % Memory : 8046.5625MB
% 0.18/0.43 % OS : Linux 6.8.0-71-generic
% 0.18/0.43 % CPULimit : 300
% 0.18/0.43 % WCLimit : 300
% 0.18/0.43 % DateTime : Mon Sep 21 14:13:01 UTC 2026
% 0.18/0.43 % CPUTime :
% 0.18/0.49 % Drodi V4.1.1
% 6.34/1.42 % Refutation found
% 6.34/1.42 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 6.34/1.42 % SZS output start CNFRefutation for theBenchmark
% 6.34/1.42 fof(f1,axiom,(
% 6.34/1.42 (![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)) ) ))),
% 6.34/1.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.34/1.42 fof(f3,axiom,(
% 6.34/1.42 (![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)) ) ))),
% 6.34/1.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.34/1.42 fof(f9,axiom,(
% 6.34/1.42 (![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)) ) ))),
% 6.34/1.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.34/1.42 fof(f10,axiom,(
% 6.34/1.42 (![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)) ) ))),
% 6.34/1.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.34/1.42 fof(f18,axiom,(
% 6.34/1.42 (![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)) ))),
% 6.34/1.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.34/1.42 fof(f19,axiom,(
% 6.34/1.42 (![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)) ))),
% 6.34/1.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.34/1.42 fof(f37,axiom,(
% 6.34/1.42 (![V_comb1_H,V_comb2_H]: (c_Comb_Ocomb_OK != c_Comb_Ocomb_Oop_A_D_D(V_comb1_H,V_comb2_H) ))),
% 6.34/1.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.34/1.42 fof(f41,axiom,(
% 6.34/1.42 (![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 ) ))),
% 6.34/1.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.34/1.42 fof(f42,axiom,(
% 6.34/1.42 (![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 ) ))),
% 6.34/1.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.34/1.42 fof(f1404,negated_conjecture,(
% 6.34/1.42 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)) ),
% 6.34/1.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.34/1.42 fof(f1405,negated_conjecture,(
% 6.34/1.42 (![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)) ) ))),
% 6.34/1.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.34/1.42 fof(f1406,plain,(
% 6.34/1.42 ![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)))),
% 6.34/1.42 inference(cnf_transformation,[status(thm)],[f1])).
% 6.34/1.42 fof(f1408,plain,(
% 6.34/1.42 ![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)))),
% 6.34/1.42 inference(cnf_transformation,[status(thm)],[f3])).
% 6.34/1.42 fof(f1416,plain,(
% 6.34/1.42 ![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)))),
% 6.34/1.42 inference(cnf_transformation,[status(thm)],[f9])).
% 6.34/1.42 fof(f1417,plain,(
% 6.34/1.42 ![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)))),
% 6.34/1.42 inference(cnf_transformation,[status(thm)],[f10])).
% 6.34/1.42 fof(f1425,plain,(
% 6.34/1.42 ![X0]: (c_in(c_Pair(X0,X0,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)))),
% 6.34/1.42 inference(cnf_transformation,[status(thm)],[f18])).
% 6.34/1.42 fof(f1426,plain,(
% 6.34/1.42 ![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)))),
% 6.34/1.42 inference(cnf_transformation,[status(thm)],[f19])).
% 6.34/1.42 fof(f1444,plain,(
% 6.34/1.42 ![X0,X1]: (~c_Comb_Ocomb_OK=c_Comb_Ocomb_Oop_A_D_D(X0,X1))),
% 6.34/1.42 inference(cnf_transformation,[status(thm)],[f37])).
% 6.34/1.42 fof(f1448,plain,(
% 6.34/1.42 ![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)),
% 6.34/1.42 inference(miniscoping,[status(thm)],[f41])).
% 6.34/1.42 fof(f1449,plain,(
% 6.34/1.42 ![X0,X1,X2,X3]: (~c_Comb_Ocomb_Oop_A_D_D(X0,X1)=c_Comb_Ocomb_Oop_A_D_D(X2,X3)|X0=X2)),
% 6.34/1.42 inference(cnf_transformation,[status(thm)],[f1448])).
% 6.34/1.42 fof(f1450,plain,(
% 6.34/1.42 ![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)),
% 6.34/1.42 inference(miniscoping,[status(thm)],[f42])).
% 6.34/1.42 fof(f1451,plain,(
% 6.34/1.42 ![X0,X1,X2,X3]: (~c_Comb_Ocomb_Oop_A_D_D(X0,X1)=c_Comb_Ocomb_Oop_A_D_D(X2,X3)|X1=X3)),
% 6.34/1.42 inference(cnf_transformation,[status(thm)],[f1450])).
% 6.34/1.42 fof(f2933,plain,(
% 6.34/1.42 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))),
% 6.34/1.42 inference(cnf_transformation,[status(thm)],[f1404])).
% 6.34/1.42 fof(f2934,plain,(
% 6.34/1.42 ![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)))),
% 6.34/1.42 inference(cnf_transformation,[status(thm)],[f1405])).
% 6.34/1.42 fof(f2938,plain,(
% 6.34/1.42 ~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))),
% 6.34/1.42 inference(resolution,[status(thm)],[f1425,f2934])).
% 6.34/1.42 fof(f2941,plain,(
% 6.34/1.42 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))),
% 6.34/1.42 inference(resolution,[status(thm)],[f1406,f2933])).
% 6.34/1.42 fof(f2945,plain,(
% 6.34/1.42 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))),
% 6.34/1.42 inference(resolution,[status(thm)],[f2941,f1449])).
% 6.34/1.42 fof(f2954,plain,(
% 6.34/1.42 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))),
% 6.34/1.42 inference(forward_subsumption_resolution,[status(thm)],[f2945,f1444])).
% 6.34/1.42 fof(f2978,plain,(
% 6.34/1.42 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))),
% 6.34/1.42 inference(resolution,[status(thm)],[f1408,f2933])).
% 6.34/1.42 fof(f2982,plain,(
% 6.34/1.42 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)))),
% 6.34/1.42 inference(resolution,[status(thm)],[f2978,f1416])).
% 6.34/1.42 fof(f3182,plain,(
% 6.34/1.42 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))|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))),
% 6.34/1.42 inference(resolution,[status(thm)],[f1417,f2978])).
% 6.34/1.42 fof(f3248,plain,(
% 6.34/1.42 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))),
% 6.34/1.42 inference(resolution,[status(thm)],[f2982,f1449])).
% 6.34/1.42 fof(f3273,plain,(
% 6.34/1.42 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)))),
% 6.34/1.42 inference(forward_subsumption_resolution,[status(thm)],[f3248,f1444])).
% 6.34/1.42 fof(f3296,plain,(
% 6.34/1.42 ![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))),
% 6.34/1.42 inference(paramodulation,[status(thm)],[f3273,f1426])).
% 6.34/1.42 fof(f3970,plain,(
% 6.34/1.42 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)),
% 6.34/1.42 inference(paramodulation,[status(thm)],[f2954,f3296])).
% 6.34/1.42 fof(f3971,plain,(
% 6.34/1.42 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)),
% 6.34/1.42 inference(duplicate_literals_removal,[status(thm)],[f3970])).
% 6.34/1.42 fof(f3973,plain,(
% 6.34/1.42 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))),
% 6.34/1.42 inference(resolution,[status(thm)],[f3971,f2934])).
% 6.34/1.42 fof(f4811,plain,(
% 6.34/1.42 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))),
% 6.34/1.43 inference(forward_subsumption_resolution,[status(thm)],[f3182,f3973])).
% 6.34/1.43 fof(f4813,plain,(
% 6.34/1.43 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))),
% 6.34/1.43 inference(resolution,[status(thm)],[f4811,f1449])).
% 6.34/1.43 fof(f4851,plain,(
% 6.34/1.43 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)),
% 6.34/1.43 inference(forward_subsumption_resolution,[status(thm)],[f4813,f1444])).
% 6.34/1.43 fof(f4914,plain,(
% 6.34/1.43 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)),
% 6.34/1.43 inference(paramodulation,[status(thm)],[f4851,f1426])).
% 6.34/1.43 fof(f4943,plain,(
% 6.34/1.43 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))),
% 6.34/1.43 inference(resolution,[status(thm)],[f4914,f2934])).
% 6.34/1.43 fof(f4948,plain,(
% 6.34/1.43 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)),
% 6.34/1.43 inference(forward_subsumption_resolution,[status(thm)],[f4943,f1425])).
% 6.34/1.43 fof(f5705,plain,(
% 6.34/1.43 v_x=v_xb),
% 6.34/1.43 inference(resolution,[status(thm)],[f4948,f1451])).
% 6.34/1.43 fof(f5857,plain,(
% 6.34/1.43 ~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))),
% 6.34/1.43 inference(backward_demodulation,[status(thm)],[f5705,f2938])).
% 6.34/1.43 fof(f5862,plain,(
% 6.34/1.43 $false),
% 6.34/1.43 inference(forward_subsumption_resolution,[status(thm)],[f5857,f1425])).
% 6.34/1.43 % SZS output end CNFRefutation for theBenchmark.p
% 5.27/1.47 % Elapsed time: 1.034895 seconds
% 5.27/1.47 % CPU time: 7.283495 seconds
% 5.27/1.47 % Total memory used: 242.260 MB
% 5.27/1.47 % Net memory used: 237.357 MB
%------------------------------------------------------------------------------