%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : COL110-1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n005.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 : Fri Sep 25 01:02:05 PM UTC 2026
% Result : Unsatisfiable 123.55s 16.17s
% Output : Proof 0.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 60
% Syntax : Number of formulae : 281 ( 233 unt; 0 def)
% Number of atoms : 333 ( 170 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 306 ( 254 ~; 52 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-3 aty)
% Number of functors : 53 ( 53 usr; 25 con; 0-4 aty)
% Number of variables : 530 ( 134 sgn 246 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f1407,negated_conjecture,
( ~ c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(v_ya,v_w),V_U,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_yb,v_wa),V_U,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_4) ).
fof(f1407_nnf,plain,
! [V_U] :
( ~ c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(v_ya,v_w),V_U,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_yb,v_wa),V_U,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) ),
inference(nnf_transformation,[status(thm)],[f1407]) ).
fof(f1407_sk,plain,
! [V_U] :
( ~ c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(v_ya,v_w),V_U,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_yb,v_wa),V_U,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) ),
inference(skolemisation,[status(esa)],[f1407_nnf]) ).
cnf(c1407,plain,
( ~ c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(v_ya,v_w),X0,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_yb,v_wa),X0,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) ),
inference(cnf_transformation,[status(esa)],[f1407_sk]) ).
cnf(t121,plain,
or(not(c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(v_yb,v_wa),X1,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))),not(c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(v_ya,v_w),X1,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)))) = true,
inference(equality_encoding,[status(esa)],[c1407]) ).
cnf(t572,plain,
or(not(c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(v_yb,v_wa),X1,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))),not(c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(v_ya,v_w),X1,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)))) = true,
inference(orient,[status(thm)],[t121]) ).
cnf(f20,axiom,
( 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))
| ~ 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(V_z,V_w,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Comb_Oparcontract_Ointros__4_0) ).
fof(f20_nnf,plain,
! [V_z,V_w,V_x,V_y] :
( 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))
| ~ 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(V_z,V_w,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) ),
inference(nnf_transformation,[status(thm)],[f20]) ).
fof(f20_sk,plain,
! [V_z,V_w,V_x,V_y] :
( 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))
| ~ 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(V_z,V_w,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) ),
inference(skolemisation,[status(esa)],[f20_nnf]) ).
cnf(c20,plain,
( 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))
| ~ 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(X0,X1,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) ),
inference(cnf_transformation,[status(esa)],[f20_sk]) ).
cnf(t123,plain,
ifeq(c_in(c_Pair(X1,X2,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),true,ifeq(c_in(c_Pair(X3,X4,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),true,c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(X3,X1),c_Comb_Ocomb_Oop_A_D_D(X4,X2),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),true),true) = true,
inference(equality_encoding,[status(esa)],[c20]) ).
cnf(t626,plain,
ifeq(c_in(c_Pair(X1,X2,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),true,ifeq(c_in(c_Pair(X3,X4,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),true,c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(X3,X1),c_Comb_Ocomb_Oop_A_D_D(X4,X2),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),true),true) = true,
inference(orient,[status(thm)],[t123]) ).
cnf(f1408,negated_conjecture,
( ~ 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))
| c_in(c_Pair(v_ya,v_xb(V_U),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_5) ).
fof(f1408_nnf,plain,
! [V_U] :
( ~ 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))
| c_in(c_Pair(v_ya,v_xb(V_U),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) ),
inference(nnf_transformation,[status(thm)],[f1408]) ).
fof(f1408_sk,plain,
! [V_U] :
( ~ 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))
| c_in(c_Pair(v_ya,v_xb(V_U),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) ),
inference(skolemisation,[status(esa)],[f1408_nnf]) ).
cnf(c1408,plain,
( ~ c_in(c_Pair(v_x,X0,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| c_in(c_Pair(v_ya,v_xb(X0),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) ),
inference(cnf_transformation,[status(esa)],[f1408_sk]) ).
cnf(t118,plain,
ifeq(c_in(c_Pair(v_x,X1,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),true,c_in(c_Pair(v_ya,v_xb(X1),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),true) = true,
inference(equality_encoding,[status(esa)],[c1408]) ).
cnf(t453,plain,
ifeq(c_in(c_Pair(v_x,X1,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),true,c_in(c_Pair(v_ya,v_xb(X1),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),true) = true,
inference(orient,[status(thm)],[t118]) ).
cnf(f1405,negated_conjecture,
c_in(c_Pair(v_x,v_yb,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_2) ).
fof(f1405_nnf,plain,
c_in(c_Pair(v_x,v_yb,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),
inference(nnf_transformation,[status(thm)],[f1405]) ).
cnf(c1405,plain,
c_in(c_Pair(v_x,v_yb,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),
inference(cnf_transformation,[status(esa)],[f1405_nnf]) ).
cnf(t92,plain,
c_in(c_Pair(v_x,v_yb,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) = true,
inference(equality_encoding,[status(esa)],[c1405]) ).
cnf(t251,plain,
c_in(c_Pair(v_x,v_yb,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) = true,
inference(orient,[status(thm)],[t92]) ).
cnf(t455,plain,
true = ifeq(true,true,c_in(c_Pair(v_ya,v_xb(v_yb),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),true),
inference(cp,[status(thm)],[t453,t251]) ).
cnf(t36,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t155,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t36]) ).
cnf(t15680,plain,
true = c_in(c_Pair(v_ya,v_xb(v_yb),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),
inference(step,[status(thm)],[t455,t155]) ).
cnf(t462,plain,
c_in(c_Pair(v_ya,v_xb(v_yb),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) = true,
inference(orient,[status(thm)],[t15680]) ).
cnf(t648,plain,
true = ifeq(c_in(c_Pair(X1,X2,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),true,ifeq(true,true,c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(v_ya,X1),c_Comb_Ocomb_Oop_A_D_D(v_xb(v_yb),X2),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),true),true),
inference(cp,[status(thm)],[t626,t462]) ).
cnf(t16602,plain,
true = ifeq(c_in(c_Pair(X1,X2,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),true,c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(v_ya,X1),c_Comb_Ocomb_Oop_A_D_D(v_xb(v_yb),X2),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),true),
inference(step,[status(thm)],[t648,t155]) ).
cnf(t14676,plain,
ifeq(c_in(c_Pair(X1,X2,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),true,c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(v_ya,X1),c_Comb_Ocomb_Oop_A_D_D(v_xb(v_yb),X2),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),true) = true,
inference(orient,[status(thm)],[t16602]) ).
cnf(f1410,negated_conjecture,
( ~ c_in(c_Pair(v_z,V_U,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| c_in(c_Pair(v_w,v_xaa(V_U),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_7) ).
fof(f1410_nnf,plain,
! [V_U] :
( ~ c_in(c_Pair(v_z,V_U,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| c_in(c_Pair(v_w,v_xaa(V_U),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) ),
inference(nnf_transformation,[status(thm)],[f1410]) ).
fof(f1410_sk,plain,
! [V_U] :
( ~ c_in(c_Pair(v_z,V_U,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| c_in(c_Pair(v_w,v_xaa(V_U),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) ),
inference(skolemisation,[status(esa)],[f1410_nnf]) ).
cnf(c1410,plain,
( ~ c_in(c_Pair(v_z,X0,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| c_in(c_Pair(v_w,v_xaa(X0),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) ),
inference(cnf_transformation,[status(esa)],[f1410_sk]) ).
cnf(t120,plain,
ifeq(c_in(c_Pair(v_z,X1,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),true,c_in(c_Pair(v_w,v_xaa(X1),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),true) = true,
inference(equality_encoding,[status(esa)],[c1410]) ).
cnf(t531,plain,
ifeq(c_in(c_Pair(v_z,X1,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),true,c_in(c_Pair(v_w,v_xaa(X1),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),true) = true,
inference(orient,[status(thm)],[t120]) ).
cnf(f1406,negated_conjecture,
c_in(c_Pair(v_z,v_wa,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_3) ).
fof(f1406_nnf,plain,
c_in(c_Pair(v_z,v_wa,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),
inference(nnf_transformation,[status(thm)],[f1406]) ).
cnf(c1406,plain,
c_in(c_Pair(v_z,v_wa,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),
inference(cnf_transformation,[status(esa)],[f1406_nnf]) ).
cnf(t94,plain,
c_in(c_Pair(v_z,v_wa,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) = true,
inference(equality_encoding,[status(esa)],[c1406]) ).
cnf(t253,plain,
c_in(c_Pair(v_z,v_wa,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) = true,
inference(orient,[status(thm)],[t94]) ).
cnf(t533,plain,
true = ifeq(true,true,c_in(c_Pair(v_w,v_xaa(v_wa),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),true),
inference(cp,[status(thm)],[t531,t253]) ).
cnf(t15701,plain,
true = c_in(c_Pair(v_w,v_xaa(v_wa),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),
inference(step,[status(thm)],[t533,t155]) ).
cnf(t540,plain,
c_in(c_Pair(v_w,v_xaa(v_wa),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) = true,
inference(orient,[status(thm)],[t15701]) ).
cnf(t14683,plain,
true = ifeq(true,true,c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(v_ya,v_w),c_Comb_Ocomb_Oop_A_D_D(v_xb(v_yb),v_xaa(v_wa)),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),true),
inference(cp,[status(thm)],[t14676,t540]) ).
cnf(t16607,plain,
true = c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(v_ya,v_w),c_Comb_Ocomb_Oop_A_D_D(v_xb(v_yb),v_xaa(v_wa)),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),
inference(step,[status(thm)],[t14683,t155]) ).
cnf(t15251,plain,
c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(v_ya,v_w),c_Comb_Ocomb_Oop_A_D_D(v_xb(v_yb),v_xaa(v_wa)),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) = true,
inference(orient,[status(thm)],[t16607]) ).
cnf(t15256,plain,
true = or(not(c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(v_yb,v_wa),c_Comb_Ocomb_Oop_A_D_D(v_xb(v_yb),v_xaa(v_wa)),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))),not(true)),
inference(cp,[status(thm)],[t572,t15251]) ).
cnf(f1409,negated_conjecture,
( ~ 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))
| c_in(c_Pair(V_U,v_xb(V_U),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_6) ).
fof(f1409_nnf,plain,
! [V_U] :
( ~ 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))
| c_in(c_Pair(V_U,v_xb(V_U),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) ),
inference(nnf_transformation,[status(thm)],[f1409]) ).
fof(f1409_sk,plain,
! [V_U] :
( ~ 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))
| c_in(c_Pair(V_U,v_xb(V_U),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) ),
inference(skolemisation,[status(esa)],[f1409_nnf]) ).
cnf(c1409,plain,
( ~ c_in(c_Pair(v_x,X0,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| c_in(c_Pair(X0,v_xb(X0),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) ),
inference(cnf_transformation,[status(esa)],[f1409_sk]) ).
cnf(t117,plain,
ifeq(c_in(c_Pair(v_x,X1,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),true,c_in(c_Pair(X1,v_xb(X1),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),true) = true,
inference(equality_encoding,[status(esa)],[c1409]) ).
cnf(t412,plain,
ifeq(c_in(c_Pair(v_x,X1,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),true,c_in(c_Pair(X1,v_xb(X1),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),true) = true,
inference(orient,[status(thm)],[t117]) ).
cnf(t415,plain,
true = ifeq(true,true,c_in(c_Pair(v_yb,v_xb(v_yb),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),true),
inference(cp,[status(thm)],[t412,t251]) ).
cnf(t15671,plain,
true = c_in(c_Pair(v_yb,v_xb(v_yb),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),
inference(step,[status(thm)],[t415,t155]) ).
cnf(t427,plain,
c_in(c_Pair(v_yb,v_xb(v_yb),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) = true,
inference(orient,[status(thm)],[t15671]) ).
cnf(t642,plain,
true = ifeq(c_in(c_Pair(X1,X2,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),true,ifeq(true,true,c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(v_yb,X1),c_Comb_Ocomb_Oop_A_D_D(v_xb(v_yb),X2),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),true),true),
inference(cp,[status(thm)],[t626,t427]) ).
cnf(t16536,plain,
true = ifeq(c_in(c_Pair(X1,X2,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),true,c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(v_yb,X1),c_Comb_Ocomb_Oop_A_D_D(v_xb(v_yb),X2),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),true),
inference(step,[status(thm)],[t642,t155]) ).
cnf(t10600,plain,
ifeq(c_in(c_Pair(X1,X2,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),true,c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(v_yb,X1),c_Comb_Ocomb_Oop_A_D_D(v_xb(v_yb),X2),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),true) = true,
inference(orient,[status(thm)],[t16536]) ).
cnf(f1411,negated_conjecture,
( ~ c_in(c_Pair(v_z,V_U,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| c_in(c_Pair(V_U,v_xaa(V_U),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_8) ).
fof(f1411_nnf,plain,
! [V_U] :
( ~ c_in(c_Pair(v_z,V_U,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| c_in(c_Pair(V_U,v_xaa(V_U),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) ),
inference(nnf_transformation,[status(thm)],[f1411]) ).
fof(f1411_sk,plain,
! [V_U] :
( ~ c_in(c_Pair(v_z,V_U,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| c_in(c_Pair(V_U,v_xaa(V_U),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) ),
inference(skolemisation,[status(esa)],[f1411_nnf]) ).
cnf(c1411,plain,
( ~ c_in(c_Pair(v_z,X0,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb))
| c_in(c_Pair(X0,v_xaa(X0),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) ),
inference(cnf_transformation,[status(esa)],[f1411_sk]) ).
cnf(t119,plain,
ifeq(c_in(c_Pair(v_z,X1,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),true,c_in(c_Pair(X1,v_xaa(X1),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),true) = true,
inference(equality_encoding,[status(esa)],[c1411]) ).
cnf(t490,plain,
ifeq(c_in(c_Pair(v_z,X1,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),true,c_in(c_Pair(X1,v_xaa(X1),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),true) = true,
inference(orient,[status(thm)],[t119]) ).
cnf(t493,plain,
true = ifeq(true,true,c_in(c_Pair(v_wa,v_xaa(v_wa),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),true),
inference(cp,[status(thm)],[t490,t253]) ).
cnf(t15692,plain,
true = c_in(c_Pair(v_wa,v_xaa(v_wa),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),
inference(step,[status(thm)],[t493,t155]) ).
cnf(t505,plain,
c_in(c_Pair(v_wa,v_xaa(v_wa),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) = true,
inference(orient,[status(thm)],[t15692]) ).
cnf(t10607,plain,
true = ifeq(true,true,c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(v_yb,v_wa),c_Comb_Ocomb_Oop_A_D_D(v_xb(v_yb),v_xaa(v_wa)),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),true),
inference(cp,[status(thm)],[t10600,t505]) ).
cnf(t16570,plain,
true = c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(v_yb,v_wa),c_Comb_Ocomb_Oop_A_D_D(v_xb(v_yb),v_xaa(v_wa)),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),
inference(step,[status(thm)],[t10607,t155]) ).
cnf(t12976,plain,
c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(v_yb,v_wa),c_Comb_Ocomb_Oop_A_D_D(v_xb(v_yb),v_xaa(v_wa)),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Oparcontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)) = true,
inference(orient,[status(thm)],[t16570]) ).
cnf(t16608,plain,
true = or(not(true),not(true)),
inference(step,[status(thm)],[t15256,t12976]) ).
cnf(t16,plain,
not(true) = false,
introduced(definition) ).
cnf(t140,plain,
not(true) = false,
inference(orient,[status(thm)],[t16]) ).
cnf(t16609,plain,
true = or(false,not(true)),
inference(step,[status(thm)],[t16608,t140]) ).
cnf(t20,plain,
or(false,X1) = X1,
introduced(definition) ).
cnf(t144,plain,
or(false,X1) = X1,
inference(orient,[status(thm)],[t20]) ).
cnf(t16610,plain,
true = not(true),
inference(step,[status(thm)],[t16609,t144]) ).
cnf(t16611,plain,
true = false,
inference(step,[status(thm)],[t16610,t140]) ).
cnf(t15281,plain,
false = true,
inference(orient,[status(thm)],[t16611]) ).
cnf(f29,axiom,
~ c_in(c_Pair(c_Comb_OI,V_z,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Ocontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Comb_OI__contract__E_0) ).
fof(f29_nnf,plain,
! [V_z] : ~ c_in(c_Pair(c_Comb_OI,V_z,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Ocontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),
inference(nnf_transformation,[status(thm)],[f29]) ).
fof(f29_sk,plain,
! [V_z] : ~ c_in(c_Pair(c_Comb_OI,V_z,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Ocontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),
inference(skolemisation,[status(esa)],[f29_nnf]) ).
cnf(c29,plain,
~ c_in(c_Pair(c_Comb_OI,X0,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Ocontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),
inference(cnf_transformation,[status(esa)],[f29_sk]) ).
cnf(f32,axiom,
~ c_in(c_Pair(c_Comb_Ocomb_OK,V_r,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Ocontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Comb_OK__contractE_0) ).
fof(f32_nnf,plain,
! [V_r] : ~ c_in(c_Pair(c_Comb_Ocomb_OK,V_r,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Ocontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),
inference(nnf_transformation,[status(thm)],[f32]) ).
fof(f32_sk,plain,
! [V_r] : ~ c_in(c_Pair(c_Comb_Ocomb_OK,V_r,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Ocontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),
inference(skolemisation,[status(esa)],[f32_nnf]) ).
cnf(c32,plain,
~ c_in(c_Pair(c_Comb_Ocomb_OK,X0,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Ocontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),
inference(cnf_transformation,[status(esa)],[f32_sk]) ).
cnf(f33,axiom,
~ c_in(c_Pair(c_Comb_Ocomb_OS,V_r,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Ocontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Comb_OS__contractE_0) ).
fof(f33_nnf,plain,
! [V_r] : ~ c_in(c_Pair(c_Comb_Ocomb_OS,V_r,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Ocontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),
inference(nnf_transformation,[status(thm)],[f33]) ).
fof(f33_sk,plain,
! [V_r] : ~ c_in(c_Pair(c_Comb_Ocomb_OS,V_r,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Ocontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),
inference(skolemisation,[status(esa)],[f33_nnf]) ).
cnf(c33,plain,
~ c_in(c_Pair(c_Comb_Ocomb_OS,X0,tc_Comb_Ocomb,tc_Comb_Ocomb),c_Comb_Ocontract,tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),
inference(cnf_transformation,[status(esa)],[f33_sk]) ).
cnf(f34,axiom,
c_Comb_Ocomb_OK != c_Comb_Ocomb_OS,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Comb_Ocomb_Odistinct__1__iff1_0) ).
fof(f34_nnf,plain,
c_Comb_Ocomb_OK != c_Comb_Ocomb_OS,
inference(nnf_transformation,[status(thm)],[f34]) ).
fof(f34_sk,plain,
c_Comb_Ocomb_OK != c_Comb_Ocomb_OS,
inference(skolemisation,[status(esa)],[f34_nnf]) ).
cnf(c34,plain,
c_Comb_Ocomb_OK != c_Comb_Ocomb_OS,
inference(cnf_transformation,[status(esa)],[f34_sk]) ).
cnf(f35,axiom,
c_Comb_Ocomb_OS != c_Comb_Ocomb_OK,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Comb_Ocomb_Odistinct__2__iff1_0) ).
fof(f35_nnf,plain,
c_Comb_Ocomb_OS != c_Comb_Ocomb_OK,
inference(nnf_transformation,[status(thm)],[f35]) ).
fof(f35_sk,plain,
c_Comb_Ocomb_OS != c_Comb_Ocomb_OK,
inference(skolemisation,[status(esa)],[f35_nnf]) ).
cnf(c35,plain,
c_Comb_Ocomb_OS != c_Comb_Ocomb_OK,
inference(cnf_transformation,[status(esa)],[f35_sk]) ).
cnf(f36,axiom,
c_Comb_Ocomb_OK != c_Comb_Ocomb_Oop_A_D_D(V_comb1_H,V_comb2_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Comb_Ocomb_Odistinct__3__iff1_0) ).
fof(f36_nnf,plain,
! [V_comb1_H,V_comb2_H] : c_Comb_Ocomb_OK != c_Comb_Ocomb_Oop_A_D_D(V_comb1_H,V_comb2_H),
inference(nnf_transformation,[status(thm)],[f36]) ).
fof(f36_sk,plain,
! [V_comb1_H,V_comb2_H] : c_Comb_Ocomb_OK != c_Comb_Ocomb_Oop_A_D_D(V_comb1_H,V_comb2_H),
inference(skolemisation,[status(esa)],[f36_nnf]) ).
cnf(c36,plain,
c_Comb_Ocomb_OK != c_Comb_Ocomb_Oop_A_D_D(X0,X1),
inference(cnf_transformation,[status(esa)],[f36_sk]) ).
cnf(f37,axiom,
c_Comb_Ocomb_Oop_A_D_D(V_comb1_H,V_comb2_H) != c_Comb_Ocomb_OK,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Comb_Ocomb_Odistinct__4__iff1_0) ).
fof(f37_nnf,plain,
! [V_comb1_H,V_comb2_H] : c_Comb_Ocomb_Oop_A_D_D(V_comb1_H,V_comb2_H) != c_Comb_Ocomb_OK,
inference(nnf_transformation,[status(thm)],[f37]) ).
fof(f37_sk,plain,
! [V_comb1_H,V_comb2_H] : c_Comb_Ocomb_Oop_A_D_D(V_comb1_H,V_comb2_H) != c_Comb_Ocomb_OK,
inference(skolemisation,[status(esa)],[f37_nnf]) ).
cnf(c37,plain,
c_Comb_Ocomb_Oop_A_D_D(X0,X1) != c_Comb_Ocomb_OK,
inference(cnf_transformation,[status(esa)],[f37_sk]) ).
cnf(f38,axiom,
c_Comb_Ocomb_OS != c_Comb_Ocomb_Oop_A_D_D(V_comb1_H,V_comb2_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Comb_Ocomb_Odistinct__5__iff1_0) ).
fof(f38_nnf,plain,
! [V_comb1_H,V_comb2_H] : c_Comb_Ocomb_OS != c_Comb_Ocomb_Oop_A_D_D(V_comb1_H,V_comb2_H),
inference(nnf_transformation,[status(thm)],[f38]) ).
fof(f38_sk,plain,
! [V_comb1_H,V_comb2_H] : c_Comb_Ocomb_OS != c_Comb_Ocomb_Oop_A_D_D(V_comb1_H,V_comb2_H),
inference(skolemisation,[status(esa)],[f38_nnf]) ).
cnf(c38,plain,
c_Comb_Ocomb_OS != c_Comb_Ocomb_Oop_A_D_D(X0,X1),
inference(cnf_transformation,[status(esa)],[f38_sk]) ).
cnf(f39,axiom,
c_Comb_Ocomb_Oop_A_D_D(V_comb1_H,V_comb2_H) != c_Comb_Ocomb_OS,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Comb_Ocomb_Odistinct__6__iff1_0) ).
fof(f39_nnf,plain,
! [V_comb1_H,V_comb2_H] : c_Comb_Ocomb_Oop_A_D_D(V_comb1_H,V_comb2_H) != c_Comb_Ocomb_OS,
inference(nnf_transformation,[status(thm)],[f39]) ).
fof(f39_sk,plain,
! [V_comb1_H,V_comb2_H] : c_Comb_Ocomb_Oop_A_D_D(V_comb1_H,V_comb2_H) != c_Comb_Ocomb_OS,
inference(skolemisation,[status(esa)],[f39_nnf]) ).
cnf(c39,plain,
c_Comb_Ocomb_Oop_A_D_D(X0,X1) != c_Comb_Ocomb_OS,
inference(cnf_transformation,[status(esa)],[f39_sk]) ).
cnf(f50,axiom,
c_Datatype_Ooption_ONone != c_Datatype_Ooption_OSome(V_a_H,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Datatype_Ooption_Odistinct__1__iff1_0) ).
fof(f50_nnf,plain,
! [V_a_H,T_a] : c_Datatype_Ooption_ONone != c_Datatype_Ooption_OSome(V_a_H,T_a),
inference(nnf_transformation,[status(thm)],[f50]) ).
fof(f50_sk,plain,
! [V_a_H,T_a] : c_Datatype_Ooption_ONone != c_Datatype_Ooption_OSome(V_a_H,T_a),
inference(skolemisation,[status(esa)],[f50_nnf]) ).
cnf(c50,plain,
c_Datatype_Ooption_ONone != c_Datatype_Ooption_OSome(X0,X1),
inference(cnf_transformation,[status(esa)],[f50_sk]) ).
cnf(f51,axiom,
c_Datatype_Ooption_OSome(V_a_H,T_a) != c_Datatype_Ooption_ONone,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Datatype_Ooption_Odistinct__2__iff1_0) ).
fof(f51_nnf,plain,
! [V_a_H,T_a] : c_Datatype_Ooption_OSome(V_a_H,T_a) != c_Datatype_Ooption_ONone,
inference(nnf_transformation,[status(thm)],[f51]) ).
fof(f51_sk,plain,
! [V_a_H,T_a] : c_Datatype_Ooption_OSome(V_a_H,T_a) != c_Datatype_Ooption_ONone,
inference(skolemisation,[status(esa)],[f51_nnf]) ).
cnf(c51,plain,
c_Datatype_Ooption_OSome(X0,X1) != c_Datatype_Ooption_ONone,
inference(cnf_transformation,[status(esa)],[f51_sk]) ).
cnf(f54,axiom,
c_Datatype__Universe_OAtom(V_a,T_a,T_b) != c_Datatype__Universe_OScons(V_M,V_N,T_a,T_b),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Datatype__Universe_OAtom__not__Scons__iff1_0) ).
fof(f54_nnf,plain,
! [V_a,T_a,T_b,V_M,V_N] : c_Datatype__Universe_OAtom(V_a,T_a,T_b) != c_Datatype__Universe_OScons(V_M,V_N,T_a,T_b),
inference(nnf_transformation,[status(thm)],[f54]) ).
fof(f54_sk,plain,
! [V_a,T_a,T_b,V_M,V_N] : c_Datatype__Universe_OAtom(V_a,T_a,T_b) != c_Datatype__Universe_OScons(V_M,V_N,T_a,T_b),
inference(skolemisation,[status(esa)],[f54_nnf]) ).
cnf(c54,plain,
c_Datatype__Universe_OAtom(X0,X1,X2) != c_Datatype__Universe_OScons(X3,X4,X1,X2),
inference(cnf_transformation,[status(esa)],[f54_sk]) ).
cnf(f56,axiom,
c_Datatype__Universe_OIn0(V_M,T_a,T_b) != c_Datatype__Universe_OIn1(V_N,T_a,T_b),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Datatype__Universe_OIn0__not__In1__iff1_0) ).
fof(f56_nnf,plain,
! [V_M,T_a,T_b,V_N] : c_Datatype__Universe_OIn0(V_M,T_a,T_b) != c_Datatype__Universe_OIn1(V_N,T_a,T_b),
inference(nnf_transformation,[status(thm)],[f56]) ).
fof(f56_sk,plain,
! [V_M,T_a,T_b,V_N] : c_Datatype__Universe_OIn0(V_M,T_a,T_b) != c_Datatype__Universe_OIn1(V_N,T_a,T_b),
inference(skolemisation,[status(esa)],[f56_nnf]) ).
cnf(c56,plain,
c_Datatype__Universe_OIn0(X0,X1,X2) != c_Datatype__Universe_OIn1(X3,X1,X2),
inference(cnf_transformation,[status(esa)],[f56_sk]) ).
cnf(f58,axiom,
c_Datatype__Universe_OIn1(V_N,T_a,T_b) != c_Datatype__Universe_OIn0(V_M,T_a,T_b),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Datatype__Universe_OIn1__not__In0__iff1_0) ).
fof(f58_nnf,plain,
! [V_N,T_a,T_b,V_M] : c_Datatype__Universe_OIn1(V_N,T_a,T_b) != c_Datatype__Universe_OIn0(V_M,T_a,T_b),
inference(nnf_transformation,[status(thm)],[f58]) ).
fof(f58_sk,plain,
! [V_N,T_a,T_b,V_M] : c_Datatype__Universe_OIn1(V_N,T_a,T_b) != c_Datatype__Universe_OIn0(V_M,T_a,T_b),
inference(skolemisation,[status(esa)],[f58_nnf]) ).
cnf(c58,plain,
c_Datatype__Universe_OIn1(X0,X1,X2) != c_Datatype__Universe_OIn0(X3,X1,X2),
inference(cnf_transformation,[status(esa)],[f58_sk]) ).
cnf(f59,axiom,
c_Datatype__Universe_OLeaf(V_a,T_a,T_b) != c_Datatype__Universe_ONumb(V_k,T_a,T_b),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Datatype__Universe_OLeaf__not__Numb__iff1_0) ).
fof(f59_nnf,plain,
! [V_a,T_a,T_b,V_k] : c_Datatype__Universe_OLeaf(V_a,T_a,T_b) != c_Datatype__Universe_ONumb(V_k,T_a,T_b),
inference(nnf_transformation,[status(thm)],[f59]) ).
fof(f59_sk,plain,
! [V_a,T_a,T_b,V_k] : c_Datatype__Universe_OLeaf(V_a,T_a,T_b) != c_Datatype__Universe_ONumb(V_k,T_a,T_b),
inference(skolemisation,[status(esa)],[f59_nnf]) ).
cnf(c59,plain,
c_Datatype__Universe_OLeaf(X0,X1,X2) != c_Datatype__Universe_ONumb(X3,X1,X2),
inference(cnf_transformation,[status(esa)],[f59_sk]) ).
cnf(f60,axiom,
c_Datatype__Universe_OLeaf(V_a,T_a,T_b) != c_Datatype__Universe_OScons(V_M,V_N,T_a,T_b),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Datatype__Universe_OLeaf__not__Scons__iff1_0) ).
fof(f60_nnf,plain,
! [V_a,T_a,T_b,V_M,V_N] : c_Datatype__Universe_OLeaf(V_a,T_a,T_b) != c_Datatype__Universe_OScons(V_M,V_N,T_a,T_b),
inference(nnf_transformation,[status(thm)],[f60]) ).
fof(f60_sk,plain,
! [V_a,T_a,T_b,V_M,V_N] : c_Datatype__Universe_OLeaf(V_a,T_a,T_b) != c_Datatype__Universe_OScons(V_M,V_N,T_a,T_b),
inference(skolemisation,[status(esa)],[f60_nnf]) ).
cnf(c60,plain,
c_Datatype__Universe_OLeaf(X0,X1,X2) != c_Datatype__Universe_OScons(X3,X4,X1,X2),
inference(cnf_transformation,[status(esa)],[f60_sk]) ).
cnf(f61,axiom,
c_Datatype__Universe_ONumb(V_k,T_a,T_b) != c_Datatype__Universe_OLeaf(V_a,T_a,T_b),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Datatype__Universe_ONumb__not__Leaf__iff1_0) ).
fof(f61_nnf,plain,
! [V_k,T_a,T_b,V_a] : c_Datatype__Universe_ONumb(V_k,T_a,T_b) != c_Datatype__Universe_OLeaf(V_a,T_a,T_b),
inference(nnf_transformation,[status(thm)],[f61]) ).
fof(f61_sk,plain,
! [V_k,T_a,T_b,V_a] : c_Datatype__Universe_ONumb(V_k,T_a,T_b) != c_Datatype__Universe_OLeaf(V_a,T_a,T_b),
inference(skolemisation,[status(esa)],[f61_nnf]) ).
cnf(c61,plain,
c_Datatype__Universe_ONumb(X0,X1,X2) != c_Datatype__Universe_OLeaf(X3,X1,X2),
inference(cnf_transformation,[status(esa)],[f61_sk]) ).
cnf(f62,axiom,
c_Datatype__Universe_ONumb(V_k,T_a,T_b) != c_Datatype__Universe_OScons(V_M,V_N,T_a,T_b),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Datatype__Universe_ONumb__not__Scons__iff1_0) ).
fof(f62_nnf,plain,
! [V_k,T_a,T_b,V_M,V_N] : c_Datatype__Universe_ONumb(V_k,T_a,T_b) != c_Datatype__Universe_OScons(V_M,V_N,T_a,T_b),
inference(nnf_transformation,[status(thm)],[f62]) ).
fof(f62_sk,plain,
! [V_k,T_a,T_b,V_M,V_N] : c_Datatype__Universe_ONumb(V_k,T_a,T_b) != c_Datatype__Universe_OScons(V_M,V_N,T_a,T_b),
inference(skolemisation,[status(esa)],[f62_nnf]) ).
cnf(c62,plain,
c_Datatype__Universe_ONumb(X0,X1,X2) != c_Datatype__Universe_OScons(X3,X4,X1,X2),
inference(cnf_transformation,[status(esa)],[f62_sk]) ).
cnf(f65,axiom,
c_Datatype__Universe_OScons(V_M,V_N,T_a,T_b) != c_Datatype__Universe_OAtom(V_a,T_a,T_b),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Datatype__Universe_OScons__not__Atom__iff1_0) ).
fof(f65_nnf,plain,
! [V_M,V_N,T_a,T_b,V_a] : c_Datatype__Universe_OScons(V_M,V_N,T_a,T_b) != c_Datatype__Universe_OAtom(V_a,T_a,T_b),
inference(nnf_transformation,[status(thm)],[f65]) ).
fof(f65_sk,plain,
! [V_M,V_N,T_a,T_b,V_a] : c_Datatype__Universe_OScons(V_M,V_N,T_a,T_b) != c_Datatype__Universe_OAtom(V_a,T_a,T_b),
inference(skolemisation,[status(esa)],[f65_nnf]) ).
cnf(c65,plain,
c_Datatype__Universe_OScons(X0,X1,X2,X3) != c_Datatype__Universe_OAtom(X4,X2,X3),
inference(cnf_transformation,[status(esa)],[f65_sk]) ).
cnf(f66,axiom,
c_Datatype__Universe_OScons(V_M,V_N,T_a,T_b) != c_Datatype__Universe_OLeaf(V_a,T_a,T_b),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Datatype__Universe_OScons__not__Leaf__iff1_0) ).
fof(f66_nnf,plain,
! [V_M,V_N,T_a,T_b,V_a] : c_Datatype__Universe_OScons(V_M,V_N,T_a,T_b) != c_Datatype__Universe_OLeaf(V_a,T_a,T_b),
inference(nnf_transformation,[status(thm)],[f66]) ).
fof(f66_sk,plain,
! [V_M,V_N,T_a,T_b,V_a] : c_Datatype__Universe_OScons(V_M,V_N,T_a,T_b) != c_Datatype__Universe_OLeaf(V_a,T_a,T_b),
inference(skolemisation,[status(esa)],[f66_nnf]) ).
cnf(c66,plain,
c_Datatype__Universe_OScons(X0,X1,X2,X3) != c_Datatype__Universe_OLeaf(X4,X2,X3),
inference(cnf_transformation,[status(esa)],[f66_sk]) ).
cnf(f67,axiom,
c_Datatype__Universe_OScons(V_M,V_N,T_a,T_b) != c_Datatype__Universe_ONumb(V_k,T_a,T_b),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Datatype__Universe_OScons__not__Numb__iff1_0) ).
fof(f67_nnf,plain,
! [V_M,V_N,T_a,T_b,V_k] : c_Datatype__Universe_OScons(V_M,V_N,T_a,T_b) != c_Datatype__Universe_ONumb(V_k,T_a,T_b),
inference(nnf_transformation,[status(thm)],[f67]) ).
fof(f67_sk,plain,
! [V_M,V_N,T_a,T_b,V_k] : c_Datatype__Universe_OScons(V_M,V_N,T_a,T_b) != c_Datatype__Universe_ONumb(V_k,T_a,T_b),
inference(skolemisation,[status(esa)],[f67_nnf]) ).
cnf(c67,plain,
c_Datatype__Universe_OScons(X0,X1,X2,X3) != c_Datatype__Universe_ONumb(X4,X2,X3),
inference(cnf_transformation,[status(esa)],[f67_sk]) ).
cnf(f74,axiom,
c_Extraction_Osumbool_OLeft != c_Extraction_Osumbool_ORight,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Extraction_Osumbool_Odistinct__1__iff1_0) ).
fof(f74_nnf,plain,
c_Extraction_Osumbool_OLeft != c_Extraction_Osumbool_ORight,
inference(nnf_transformation,[status(thm)],[f74]) ).
fof(f74_sk,plain,
c_Extraction_Osumbool_OLeft != c_Extraction_Osumbool_ORight,
inference(skolemisation,[status(esa)],[f74_nnf]) ).
cnf(c74,plain,
c_Extraction_Osumbool_OLeft != c_Extraction_Osumbool_ORight,
inference(cnf_transformation,[status(esa)],[f74_sk]) ).
cnf(f75,axiom,
c_Extraction_Osumbool_ORight != c_Extraction_Osumbool_OLeft,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Extraction_Osumbool_Odistinct__2__iff1_0) ).
fof(f75_nnf,plain,
c_Extraction_Osumbool_ORight != c_Extraction_Osumbool_OLeft,
inference(nnf_transformation,[status(thm)],[f75]) ).
fof(f75_sk,plain,
c_Extraction_Osumbool_ORight != c_Extraction_Osumbool_OLeft,
inference(skolemisation,[status(esa)],[f75_nnf]) ).
cnf(c75,plain,
c_Extraction_Osumbool_ORight != c_Extraction_Osumbool_OLeft,
inference(cnf_transformation,[status(esa)],[f75_sk]) ).
cnf(f88,axiom,
~ c_in(c_UNIV,c_Finite__Set_OFinites,tc_set(tc_nat)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Infinite__Set_Onat__not__finite_0) ).
fof(f88_nnf,plain,
~ c_in(c_UNIV,c_Finite__Set_OFinites,tc_set(tc_nat)),
inference(nnf_transformation,[status(thm)],[f88]) ).
fof(f88_sk,plain,
~ c_in(c_UNIV,c_Finite__Set_OFinites,tc_set(tc_nat)),
inference(skolemisation,[status(esa)],[f88_nnf]) ).
cnf(c88,plain,
~ c_in(c_UNIV,c_Finite__Set_OFinites,tc_set(tc_nat)),
inference(cnf_transformation,[status(esa)],[f88_sk]) ).
cnf(f96,axiom,
~ c_in(c_Pair(V_xs,c_List_Olist_ONil,tc_List_Olist(T_a),tc_List_Olist(T_a)),c_List_Olex(V_r,T_a),tc_prod(tc_List_Olist(T_a),tc_List_Olist(T_a))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_List_ONil2__notin__lex__iff1_0) ).
fof(f96_nnf,plain,
! [V_xs,T_a,V_r] : ~ c_in(c_Pair(V_xs,c_List_Olist_ONil,tc_List_Olist(T_a),tc_List_Olist(T_a)),c_List_Olex(V_r,T_a),tc_prod(tc_List_Olist(T_a),tc_List_Olist(T_a))),
inference(nnf_transformation,[status(thm)],[f96]) ).
fof(f96_sk,plain,
! [V_xs,T_a,V_r] : ~ c_in(c_Pair(V_xs,c_List_Olist_ONil,tc_List_Olist(T_a),tc_List_Olist(T_a)),c_List_Olex(V_r,T_a),tc_prod(tc_List_Olist(T_a),tc_List_Olist(T_a))),
inference(skolemisation,[status(esa)],[f96_nnf]) ).
cnf(c96,plain,
~ c_in(c_Pair(X0,c_List_Olist_ONil,tc_List_Olist(X1),tc_List_Olist(X1)),c_List_Olex(X2,X1),tc_prod(tc_List_Olist(X1),tc_List_Olist(X1))),
inference(cnf_transformation,[status(esa)],[f96_sk]) ).
cnf(f102,axiom,
~ c_in(c_Pair(c_List_Olist_ONil,V_ys,tc_List_Olist(T_a),tc_List_Olist(T_a)),c_List_Olex(V_r,T_a),tc_prod(tc_List_Olist(T_a),tc_List_Olist(T_a))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_List_ONil__notin__lex__iff1_0) ).
fof(f102_nnf,plain,
! [V_ys,T_a,V_r] : ~ c_in(c_Pair(c_List_Olist_ONil,V_ys,tc_List_Olist(T_a),tc_List_Olist(T_a)),c_List_Olex(V_r,T_a),tc_prod(tc_List_Olist(T_a),tc_List_Olist(T_a))),
inference(nnf_transformation,[status(thm)],[f102]) ).
fof(f102_sk,plain,
! [V_ys,T_a,V_r] : ~ c_in(c_Pair(c_List_Olist_ONil,V_ys,tc_List_Olist(T_a),tc_List_Olist(T_a)),c_List_Olex(V_r,T_a),tc_prod(tc_List_Olist(T_a),tc_List_Olist(T_a))),
inference(skolemisation,[status(esa)],[f102_nnf]) ).
cnf(c102,plain,
~ c_in(c_Pair(c_List_Olist_ONil,X0,tc_List_Olist(X1),tc_List_Olist(X1)),c_List_Olex(X2,X1),tc_prod(tc_List_Olist(X1),tc_List_Olist(X1))),
inference(cnf_transformation,[status(esa)],[f102_sk]) ).
cnf(f120,axiom,
~ c_less(c_0,c_Nat_Osize(c_List_Olist_ONil,tc_List_Olist(T_a)),tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_List_Olength__greater__0__conv__iff1_0) ).
fof(f120_nnf,plain,
! [T_a] : ~ c_less(c_0,c_Nat_Osize(c_List_Olist_ONil,tc_List_Olist(T_a)),tc_nat),
inference(nnf_transformation,[status(thm)],[f120]) ).
fof(f120_sk,plain,
! [T_a] : ~ c_less(c_0,c_Nat_Osize(c_List_Olist_ONil,tc_List_Olist(T_a)),tc_nat),
inference(skolemisation,[status(esa)],[f120_nnf]) ).
cnf(c120,plain,
~ c_less(c_0,c_Nat_Osize(c_List_Olist_ONil,tc_List_Olist(X0)),tc_nat),
inference(cnf_transformation,[status(esa)],[f120_sk]) ).
cnf(f124,axiom,
c_List_Olist_ONil != c_List_Olist_OCons(V_a_H,V_list_H,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_List_Olist_Odistinct__1__iff1_0) ).
fof(f124_nnf,plain,
! [V_a_H,V_list_H,T_a] : c_List_Olist_ONil != c_List_Olist_OCons(V_a_H,V_list_H,T_a),
inference(nnf_transformation,[status(thm)],[f124]) ).
fof(f124_sk,plain,
! [V_a_H,V_list_H,T_a] : c_List_Olist_ONil != c_List_Olist_OCons(V_a_H,V_list_H,T_a),
inference(skolemisation,[status(esa)],[f124_nnf]) ).
cnf(c124,plain,
c_List_Olist_ONil != c_List_Olist_OCons(X0,X1,X2),
inference(cnf_transformation,[status(esa)],[f124_sk]) ).
cnf(f125,axiom,
c_List_Olist_OCons(V_a_H,V_list_H,T_a) != c_List_Olist_ONil,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_List_Olist_Odistinct__2__iff1_0) ).
fof(f125_nnf,plain,
! [V_a_H,V_list_H,T_a] : c_List_Olist_OCons(V_a_H,V_list_H,T_a) != c_List_Olist_ONil,
inference(nnf_transformation,[status(thm)],[f125]) ).
fof(f125_sk,plain,
! [V_a_H,V_list_H,T_a] : c_List_Olist_OCons(V_a_H,V_list_H,T_a) != c_List_Olist_ONil,
inference(skolemisation,[status(esa)],[f125_nnf]) ).
cnf(c125,plain,
c_List_Olist_OCons(X0,X1,X2) != c_List_Olist_ONil,
inference(cnf_transformation,[status(esa)],[f125_sk]) ).
cnf(f147,axiom,
c_Suc(V_m) != c_0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Nat_OSuc__not__Zero__iff1_0) ).
fof(f147_nnf,plain,
! [V_m] : c_Suc(V_m) != c_0,
inference(nnf_transformation,[status(thm)],[f147]) ).
fof(f147_sk,plain,
! [V_m] : c_Suc(V_m) != c_0,
inference(skolemisation,[status(esa)],[f147_nnf]) ).
cnf(c147,plain,
c_Suc(X0) != c_0,
inference(cnf_transformation,[status(esa)],[f147_sk]) ).
cnf(f148,axiom,
c_0 != c_Suc(V_m),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Nat_OZero__not__Suc__iff1_0) ).
fof(f148_nnf,plain,
! [V_m] : c_0 != c_Suc(V_m),
inference(nnf_transformation,[status(thm)],[f148]) ).
fof(f148_sk,plain,
! [V_m] : c_0 != c_Suc(V_m),
inference(skolemisation,[status(esa)],[f148_nnf]) ).
cnf(c148,plain,
c_0 != c_Suc(X0),
inference(cnf_transformation,[status(esa)],[f148_sk]) ).
cnf(f162,axiom,
~ c_less(c_0,c_0,tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Nat_Oneq0__conv__iff2_0) ).
fof(f162_nnf,plain,
~ c_less(c_0,c_0,tc_nat),
inference(nnf_transformation,[status(thm)],[f162]) ).
fof(f162_sk,plain,
~ c_less(c_0,c_0,tc_nat),
inference(skolemisation,[status(esa)],[f162_nnf]) ).
cnf(c162,plain,
~ c_less(c_0,c_0,tc_nat),
inference(cnf_transformation,[status(esa)],[f162_sk]) ).
cnf(f163,axiom,
~ c_less(c_plus(V_i,V_j,tc_nat),V_i,tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Nat_Onot__add__less1__iff1_0) ).
fof(f163_nnf,plain,
! [V_i,V_j] : ~ c_less(c_plus(V_i,V_j,tc_nat),V_i,tc_nat),
inference(nnf_transformation,[status(thm)],[f163]) ).
fof(f163_sk,plain,
! [V_i,V_j] : ~ c_less(c_plus(V_i,V_j,tc_nat),V_i,tc_nat),
inference(skolemisation,[status(esa)],[f163_nnf]) ).
cnf(c163,plain,
~ c_less(c_plus(X0,X1,tc_nat),X0,tc_nat),
inference(cnf_transformation,[status(esa)],[f163_sk]) ).
cnf(f164,axiom,
~ c_less(c_plus(V_j,V_i,tc_nat),V_i,tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Nat_Onot__add__less2__iff1_0) ).
fof(f164_nnf,plain,
! [V_j,V_i] : ~ c_less(c_plus(V_j,V_i,tc_nat),V_i,tc_nat),
inference(nnf_transformation,[status(thm)],[f164]) ).
fof(f164_sk,plain,
! [V_j,V_i] : ~ c_less(c_plus(V_j,V_i,tc_nat),V_i,tc_nat),
inference(skolemisation,[status(esa)],[f164_nnf]) ).
cnf(c164,plain,
~ c_less(c_plus(X0,X1,tc_nat),X1,tc_nat),
inference(cnf_transformation,[status(esa)],[f164_sk]) ).
cnf(f165,axiom,
~ c_less(V_n,c_0,tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Nat_Onot__less0__iff1_0) ).
fof(f165_nnf,plain,
! [V_n] : ~ c_less(V_n,c_0,tc_nat),
inference(nnf_transformation,[status(thm)],[f165]) ).
fof(f165_sk,plain,
! [V_n] : ~ c_less(V_n,c_0,tc_nat),
inference(skolemisation,[status(esa)],[f165_nnf]) ).
cnf(c165,plain,
~ c_less(X0,c_0,tc_nat),
inference(cnf_transformation,[status(esa)],[f165_sk]) ).
cnf(f166,axiom,
c_Numeral_Obit_OB0 != c_Numeral_Obit_OB1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Numeral_Obit_Odistinct__1__iff1_0) ).
fof(f166_nnf,plain,
c_Numeral_Obit_OB0 != c_Numeral_Obit_OB1,
inference(nnf_transformation,[status(thm)],[f166]) ).
fof(f166_sk,plain,
c_Numeral_Obit_OB0 != c_Numeral_Obit_OB1,
inference(skolemisation,[status(esa)],[f166_nnf]) ).
cnf(c166,plain,
c_Numeral_Obit_OB0 != c_Numeral_Obit_OB1,
inference(cnf_transformation,[status(esa)],[f166_sk]) ).
cnf(f167,axiom,
c_Numeral_Obit_OB1 != c_Numeral_Obit_OB0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Numeral_Obit_Odistinct__2__iff1_0) ).
fof(f167_nnf,plain,
c_Numeral_Obit_OB1 != c_Numeral_Obit_OB0,
inference(nnf_transformation,[status(thm)],[f167]) ).
fof(f167_sk,plain,
c_Numeral_Obit_OB1 != c_Numeral_Obit_OB0,
inference(skolemisation,[status(esa)],[f167_nnf]) ).
cnf(c167,plain,
c_Numeral_Obit_OB1 != c_Numeral_Obit_OB0,
inference(cnf_transformation,[status(esa)],[f167_sk]) ).
cnf(f168,axiom,
( ~ c_less(V_x,V_x,T_a)
| ~ class_Orderings_Oorder(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Orderings_Oorder__less__irrefl__iff1_0) ).
fof(f168_nnf,plain,
! [T_a,V_x] :
( ~ c_less(V_x,V_x,T_a)
| ~ class_Orderings_Oorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f168]) ).
fof(f168_sk,plain,
! [T_a,V_x] :
( ~ c_less(V_x,V_x,T_a)
| ~ class_Orderings_Oorder(T_a) ),
inference(skolemisation,[status(esa)],[f168_nnf]) ).
cnf(c168,plain,
( ~ c_less(X1,X1,X0)
| ~ class_Orderings_Oorder(X0) ),
inference(cnf_transformation,[status(esa)],[f168_sk]) ).
cnf(f197,axiom,
( ~ c_in(V_c,c_uminus(V_A,tc_set(T_a)),T_a)
| ~ c_in(V_c,V_A,T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Set_OComplD__dest_0) ).
fof(f197_nnf,plain,
! [V_c,V_A,T_a] :
( ~ c_in(V_c,c_uminus(V_A,tc_set(T_a)),T_a)
| ~ c_in(V_c,V_A,T_a) ),
inference(nnf_transformation,[status(thm)],[f197]) ).
fof(f197_sk,plain,
! [V_c,V_A,T_a] :
( ~ c_in(V_c,c_uminus(V_A,tc_set(T_a)),T_a)
| ~ c_in(V_c,V_A,T_a) ),
inference(skolemisation,[status(esa)],[f197_nnf]) ).
cnf(c197,plain,
( ~ c_in(X0,c_uminus(X1,tc_set(X2)),X2)
| ~ c_in(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f197_sk]) ).
cnf(f202,axiom,
( ~ c_in(V_c,c_minus(V_A,V_B,tc_set(T_a)),T_a)
| ~ c_in(V_c,V_B,T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Set_ODiffE_0) ).
fof(f202_nnf,plain,
! [V_c,V_B,T_a,V_A] :
( ~ c_in(V_c,c_minus(V_A,V_B,tc_set(T_a)),T_a)
| ~ c_in(V_c,V_B,T_a) ),
inference(nnf_transformation,[status(thm)],[f202]) ).
fof(f202_sk,plain,
! [V_c,V_B,T_a,V_A] :
( ~ c_in(V_c,c_minus(V_A,V_B,tc_set(T_a)),T_a)
| ~ c_in(V_c,V_B,T_a) ),
inference(skolemisation,[status(esa)],[f202_nnf]) ).
cnf(c202,plain,
( ~ c_in(X0,c_minus(X3,X1,tc_set(X2)),X2)
| ~ c_in(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f202_sk]) ).
cnf(f211,axiom,
c_UNIV != c_emptyset,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Set_OUNIV__not__empty__iff1_0) ).
fof(f211_nnf,plain,
c_UNIV != c_emptyset,
inference(nnf_transformation,[status(thm)],[f211]) ).
fof(f211_sk,plain,
c_UNIV != c_emptyset,
inference(skolemisation,[status(esa)],[f211_nnf]) ).
cnf(c211,plain,
c_UNIV != c_emptyset,
inference(cnf_transformation,[status(esa)],[f211_sk]) ).
cnf(f219,axiom,
~ c_in(V_a,c_emptyset,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Set_OemptyE_0) ).
fof(f219_nnf,plain,
! [V_a,T_a] : ~ c_in(V_a,c_emptyset,T_a),
inference(nnf_transformation,[status(thm)],[f219]) ).
fof(f219_sk,plain,
! [V_a,T_a] : ~ c_in(V_a,c_emptyset,T_a),
inference(skolemisation,[status(esa)],[f219_nnf]) ).
cnf(c219,plain,
~ c_in(X0,c_emptyset,X1),
inference(cnf_transformation,[status(esa)],[f219_sk]) ).
cnf(f223,axiom,
~ c_less(V_A,c_emptyset,tc_set(T_a)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Set_Onot__psubset__empty__iff1_0) ).
fof(f223_nnf,plain,
! [V_A,T_a] : ~ c_less(V_A,c_emptyset,tc_set(T_a)),
inference(nnf_transformation,[status(thm)],[f223]) ).
fof(f223_sk,plain,
! [V_A,T_a] : ~ c_less(V_A,c_emptyset,tc_set(T_a)),
inference(skolemisation,[status(esa)],[f223_nnf]) ).
cnf(c223,plain,
~ c_less(X0,c_emptyset,tc_set(X1)),
inference(cnf_transformation,[status(esa)],[f223_sk]) ).
cnf(f231,axiom,
c_Sum__Type_OInl(V_a,T_a,T_b) != c_Sum__Type_OInr(V_b,T_b,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Sum__Type_OInl__not__Inr__iff1_0) ).
fof(f231_nnf,plain,
! [V_a,T_a,T_b,V_b] : c_Sum__Type_OInl(V_a,T_a,T_b) != c_Sum__Type_OInr(V_b,T_b,T_a),
inference(nnf_transformation,[status(thm)],[f231]) ).
fof(f231_sk,plain,
! [V_a,T_a,T_b,V_b] : c_Sum__Type_OInl(V_a,T_a,T_b) != c_Sum__Type_OInr(V_b,T_b,T_a),
inference(skolemisation,[status(esa)],[f231_nnf]) ).
cnf(c231,plain,
c_Sum__Type_OInl(X0,X1,X2) != c_Sum__Type_OInr(X3,X2,X1),
inference(cnf_transformation,[status(esa)],[f231_sk]) ).
cnf(f233,axiom,
c_Sum__Type_OInr(V_b,T_b,T_a) != c_Sum__Type_OInl(V_a,T_a,T_b),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Sum__Type_OInr__not__Inl__iff1_0) ).
fof(f233_nnf,plain,
! [V_b,T_b,T_a,V_a] : c_Sum__Type_OInr(V_b,T_b,T_a) != c_Sum__Type_OInl(V_a,T_a,T_b),
inference(nnf_transformation,[status(thm)],[f233]) ).
fof(f233_sk,plain,
! [V_b,T_b,T_a,V_a] : c_Sum__Type_OInr(V_b,T_b,T_a) != c_Sum__Type_OInl(V_a,T_a,T_b),
inference(skolemisation,[status(esa)],[f233_nnf]) ).
cnf(c233,plain,
c_Sum__Type_OInr(X0,X1,X2) != c_Sum__Type_OInl(X3,X2,X1),
inference(cnf_transformation,[status(esa)],[f233_sk]) ).
cnf(f237,axiom,
( ~ c_in(c_Pair(V_x,V_y,T_a,T_a),c_Transitive__Closure_Ortrancl(V_r,T_a),tc_prod(T_a,T_a))
| ~ c_Wellfounded__Recursion_Oacyclic(c_insert(c_Pair(V_y,V_x,T_a,T_a),V_r,tc_prod(T_a,T_a)),T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Wellfounded__Recursion_Oacyclic__insert__iff1_1) ).
fof(f237_nnf,plain,
! [V_y,V_x,T_a,V_r] :
( ~ c_in(c_Pair(V_x,V_y,T_a,T_a),c_Transitive__Closure_Ortrancl(V_r,T_a),tc_prod(T_a,T_a))
| ~ c_Wellfounded__Recursion_Oacyclic(c_insert(c_Pair(V_y,V_x,T_a,T_a),V_r,tc_prod(T_a,T_a)),T_a) ),
inference(nnf_transformation,[status(thm)],[f237]) ).
fof(f237_sk,plain,
! [V_y,V_x,T_a,V_r] :
( ~ c_in(c_Pair(V_x,V_y,T_a,T_a),c_Transitive__Closure_Ortrancl(V_r,T_a),tc_prod(T_a,T_a))
| ~ c_Wellfounded__Recursion_Oacyclic(c_insert(c_Pair(V_y,V_x,T_a,T_a),V_r,tc_prod(T_a,T_a)),T_a) ),
inference(skolemisation,[status(esa)],[f237_nnf]) ).
cnf(c237,plain,
( ~ c_in(c_Pair(X1,X0,X2,X2),c_Transitive__Closure_Ortrancl(X3,X2),tc_prod(X2,X2))
| ~ c_Wellfounded__Recursion_Oacyclic(c_insert(c_Pair(X0,X1,X2,X2),X3,tc_prod(X2,X2)),X2) ),
inference(cnf_transformation,[status(esa)],[f237_sk]) ).
cnf(f240,axiom,
( ~ c_in(c_Pair(V_x,V_y,T_a,T_a),c_Transitive__Closure_Ortrancl(V_r,T_a),tc_prod(T_a,T_a))
| ~ c_Wellfounded__Recursion_Owf(c_insert(c_Pair(V_y,V_x,T_a,T_a),V_r,tc_prod(T_a,T_a)),T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Wellfounded__Recursion_Owf__insert__iff1_1) ).
fof(f240_nnf,plain,
! [V_y,V_x,T_a,V_r] :
( ~ c_in(c_Pair(V_x,V_y,T_a,T_a),c_Transitive__Closure_Ortrancl(V_r,T_a),tc_prod(T_a,T_a))
| ~ c_Wellfounded__Recursion_Owf(c_insert(c_Pair(V_y,V_x,T_a,T_a),V_r,tc_prod(T_a,T_a)),T_a) ),
inference(nnf_transformation,[status(thm)],[f240]) ).
fof(f240_sk,plain,
! [V_y,V_x,T_a,V_r] :
( ~ c_in(c_Pair(V_x,V_y,T_a,T_a),c_Transitive__Closure_Ortrancl(V_r,T_a),tc_prod(T_a,T_a))
| ~ c_Wellfounded__Recursion_Owf(c_insert(c_Pair(V_y,V_x,T_a,T_a),V_r,tc_prod(T_a,T_a)),T_a) ),
inference(skolemisation,[status(esa)],[f240_nnf]) ).
cnf(c240,plain,
( ~ c_in(c_Pair(X1,X0,X2,X2),c_Transitive__Closure_Ortrancl(X3,X2),tc_prod(X2,X2))
| ~ c_Wellfounded__Recursion_Owf(c_insert(c_Pair(X0,X1,X2,X2),X3,tc_prod(X2,X2)),X2) ),
inference(cnf_transformation,[status(esa)],[f240_sk]) ).
cnf(f309,axiom,
~ c_less(V_n,V_n,tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Nat_Oless__irrefl_0) ).
fof(f309_nnf,plain,
! [V_n] : ~ c_less(V_n,V_n,tc_nat),
inference(nnf_transformation,[status(thm)],[f309]) ).
fof(f309_sk,plain,
! [V_n] : ~ c_less(V_n,V_n,tc_nat),
inference(skolemisation,[status(esa)],[f309_nnf]) ).
cnf(c309,plain,
~ c_less(X0,X0,tc_nat),
inference(cnf_transformation,[status(esa)],[f309_sk]) ).
cnf(f345,axiom,
( ~ c_lessequals(V_B,V_A,tc_set(T_a))
| ~ c_less(V_A,V_B,tc_set(T_a)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Set_OpsubsetE_0) ).
fof(f345_nnf,plain,
! [V_A,V_B,T_a] :
( ~ c_lessequals(V_B,V_A,tc_set(T_a))
| ~ c_less(V_A,V_B,tc_set(T_a)) ),
inference(nnf_transformation,[status(thm)],[f345]) ).
fof(f345_sk,plain,
! [V_A,V_B,T_a] :
( ~ c_lessequals(V_B,V_A,tc_set(T_a))
| ~ c_less(V_A,V_B,tc_set(T_a)) ),
inference(skolemisation,[status(esa)],[f345_nnf]) ).
cnf(c345,plain,
( ~ c_lessequals(X1,X0,tc_set(X2))
| ~ c_less(X0,X1,tc_set(X2)) ),
inference(cnf_transformation,[status(esa)],[f345_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c29,c32,c33,c34,c35,c36,c37,c38,c39,c50,c51,c54,c56,c58,c59,c60,c61,c62,c65,c66,c67,c74,c75,c88,c96,c102,c120,c124,c125,c147,c148,c162,c163,c164,c165,c166,c167,c168,c197,c202,c211,c219,c223,c231,c233,c237,c240,c309,c345,c1407]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t15281]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : COL110-1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/0.34 % Computer : n005.cluster.edu
% 0.09/0.34 % Model : x86_64 x86_64
% 0.09/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.34 % Memory : 8046.5625MB
% 0.09/0.34 % OS : Linux 6.8.0-71-generic
% 0.09/0.34 % CPULimit : 300
% 0.09/0.34 % WCLimit : 300
% 0.09/0.34 % DateTime : Fri Sep 25 07:37:03 UTC 2026
% 0.09/0.34 % CPUTime :
% 0.09/0.34 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 123.55/16.17 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 123.55/16.17 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------