%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : COL103-1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n017.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:04 PM UTC 2026
% Result : Unsatisfiable 24.41s 13.63s
% Output : Proof 24.41s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 52
% Syntax : Number of formulae : 215 ( 191 unt; 0 def)
% Number of atoms : 239 ( 126 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 250 ( 226 ~; 24 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-3 aty)
% Number of functors : 44 ( 44 usr; 20 con; 0-4 aty)
% Number of variables : 480 ( 138 sgn 234 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f1384,negated_conjecture,
~ c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(v_z,v_x),c_Comb_Ocomb_Oop_A_D_D(v_z,v_x),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Transitive__Closure_Ortrancl(c_Comb_Ocontract,tc_Comb_Ocomb),tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f1384_nnf,plain,
~ c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(v_z,v_x),c_Comb_Ocomb_Oop_A_D_D(v_z,v_x),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Transitive__Closure_Ortrancl(c_Comb_Ocontract,tc_Comb_Ocomb),tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),
inference(nnf_transformation,[status(thm)],[f1384]) ).
fof(f1384_sk,plain,
~ c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(v_z,v_x),c_Comb_Ocomb_Oop_A_D_D(v_z,v_x),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Transitive__Closure_Ortrancl(c_Comb_Ocontract,tc_Comb_Ocomb),tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),
inference(skolemisation,[status(esa)],[f1384_nnf]) ).
cnf(c1384,plain,
~ c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(v_z,v_x),c_Comb_Ocomb_Oop_A_D_D(v_z,v_x),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Transitive__Closure_Ortrancl(c_Comb_Ocontract,tc_Comb_Ocomb),tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),
inference(cnf_transformation,[status(esa)],[f1384_sk]) ).
cnf(t70,plain,
ifeq(c_in(c_Pair(c_Comb_Ocomb_Oop_A_D_D(v_z,v_x),c_Comb_Ocomb_Oop_A_D_D(v_z,v_x),tc_Comb_Ocomb,tc_Comb_Ocomb),c_Transitive__Closure_Ortrancl(c_Comb_Ocontract,tc_Comb_Ocomb),tc_prod(tc_Comb_Ocomb,tc_Comb_Ocomb)),true,false,true) = true,
inference(equality_encoding,[status(esa)],[c1384]) ).
cnf(f342,axiom,
c_in(c_Pair(V_a,V_a,T_a,T_a),c_Transitive__Closure_Ortrancl(V_r,T_a),tc_prod(T_a,T_a)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Transitive__Closure_Ortrancl_Ortrancl__refl_0) ).
fof(f342_nnf,plain,
! [V_a,T_a,V_r] : c_in(c_Pair(V_a,V_a,T_a,T_a),c_Transitive__Closure_Ortrancl(V_r,T_a),tc_prod(T_a,T_a)),
inference(nnf_transformation,[status(thm)],[f342]) ).
fof(f342_sk,plain,
! [V_a,T_a,V_r] : c_in(c_Pair(V_a,V_a,T_a,T_a),c_Transitive__Closure_Ortrancl(V_r,T_a),tc_prod(T_a,T_a)),
inference(skolemisation,[status(esa)],[f342_nnf]) ).
cnf(c342,plain,
c_in(c_Pair(X0,X0,X1,X1),c_Transitive__Closure_Ortrancl(X2,X1),tc_prod(X1,X1)),
inference(cnf_transformation,[status(esa)],[f342_sk]) ).
cnf(t33,plain,
c_in(c_Pair(X1,X1,X2,X2),c_Transitive__Closure_Ortrancl(X3,X2),tc_prod(X2,X2)) = true,
inference(equality_encoding,[status(esa)],[c342]) ).
cnf(t147,plain,
c_in(c_Pair(X1,X1,X2,X2),c_Transitive__Closure_Ortrancl(X3,X2),tc_prod(X2,X2)) = true,
inference(orient,[status(thm)],[t33]) ).
cnf(t778,plain,
ifeq(true,true,false,true) = true,
inference(step,[status(thm)],[t70,t147]) ).
cnf(t2,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t106,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t2]) ).
cnf(t779,plain,
false = true,
inference(step,[status(thm)],[t778,t106]) ).
cnf(t774,plain,
false = true,
inference(orient,[status(thm)],[t779]) ).
cnf(f8,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/sandbox/benchmark/theBenchmark.p',cls_Comb_OI__contract__E_0) ).
fof(f8_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)],[f8]) ).
fof(f8_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)],[f8_nnf]) ).
cnf(c8,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)],[f8_sk]) ).
cnf(f11,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/sandbox/benchmark/theBenchmark.p',cls_Comb_OK__contractE_0) ).
fof(f11_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)],[f11]) ).
fof(f11_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)],[f11_nnf]) ).
cnf(c11,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)],[f11_sk]) ).
cnf(f12,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/sandbox/benchmark/theBenchmark.p',cls_Comb_OS__contractE_0) ).
fof(f12_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)],[f12]) ).
fof(f12_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)],[f12_nnf]) ).
cnf(c12,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)],[f12_sk]) ).
cnf(f13,axiom,
c_Comb_Ocomb_OK != c_Comb_Ocomb_OS,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Comb_Ocomb_Odistinct__1__iff1_0) ).
fof(f13_nnf,plain,
c_Comb_Ocomb_OK != c_Comb_Ocomb_OS,
inference(nnf_transformation,[status(thm)],[f13]) ).
fof(f13_sk,plain,
c_Comb_Ocomb_OK != c_Comb_Ocomb_OS,
inference(skolemisation,[status(esa)],[f13_nnf]) ).
cnf(c13,plain,
c_Comb_Ocomb_OK != c_Comb_Ocomb_OS,
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(f14,axiom,
c_Comb_Ocomb_OS != c_Comb_Ocomb_OK,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Comb_Ocomb_Odistinct__2__iff1_0) ).
fof(f14_nnf,plain,
c_Comb_Ocomb_OS != c_Comb_Ocomb_OK,
inference(nnf_transformation,[status(thm)],[f14]) ).
fof(f14_sk,plain,
c_Comb_Ocomb_OS != c_Comb_Ocomb_OK,
inference(skolemisation,[status(esa)],[f14_nnf]) ).
cnf(c14,plain,
c_Comb_Ocomb_OS != c_Comb_Ocomb_OK,
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(f15,axiom,
c_Comb_Ocomb_OK != c_Comb_Ocomb_Oop_A_D_D(V_comb1_H,V_comb2_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Comb_Ocomb_Odistinct__3__iff1_0) ).
fof(f15_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)],[f15]) ).
fof(f15_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)],[f15_nnf]) ).
cnf(c15,plain,
c_Comb_Ocomb_OK != c_Comb_Ocomb_Oop_A_D_D(X0,X1),
inference(cnf_transformation,[status(esa)],[f15_sk]) ).
cnf(f16,axiom,
c_Comb_Ocomb_Oop_A_D_D(V_comb1_H,V_comb2_H) != c_Comb_Ocomb_OK,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Comb_Ocomb_Odistinct__4__iff1_0) ).
fof(f16_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)],[f16]) ).
fof(f16_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)],[f16_nnf]) ).
cnf(c16,plain,
c_Comb_Ocomb_Oop_A_D_D(X0,X1) != c_Comb_Ocomb_OK,
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(f17,axiom,
c_Comb_Ocomb_OS != c_Comb_Ocomb_Oop_A_D_D(V_comb1_H,V_comb2_H),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Comb_Ocomb_Odistinct__5__iff1_0) ).
fof(f17_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)],[f17]) ).
fof(f17_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)],[f17_nnf]) ).
cnf(c17,plain,
c_Comb_Ocomb_OS != c_Comb_Ocomb_Oop_A_D_D(X0,X1),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(f18,axiom,
c_Comb_Ocomb_Oop_A_D_D(V_comb1_H,V_comb2_H) != c_Comb_Ocomb_OS,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Comb_Ocomb_Odistinct__6__iff1_0) ).
fof(f18_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)],[f18]) ).
fof(f18_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)],[f18_nnf]) ).
cnf(c18,plain,
c_Comb_Ocomb_Oop_A_D_D(X0,X1) != c_Comb_Ocomb_OS,
inference(cnf_transformation,[status(esa)],[f18_sk]) ).
cnf(f29,axiom,
c_Datatype_Ooption_ONone != c_Datatype_Ooption_OSome(V_a_H,T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Datatype_Ooption_Odistinct__1__iff1_0) ).
fof(f29_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)],[f29]) ).
fof(f29_sk,plain,
! [V_a_H,T_a] : c_Datatype_Ooption_ONone != c_Datatype_Ooption_OSome(V_a_H,T_a),
inference(skolemisation,[status(esa)],[f29_nnf]) ).
cnf(c29,plain,
c_Datatype_Ooption_ONone != c_Datatype_Ooption_OSome(X0,X1),
inference(cnf_transformation,[status(esa)],[f29_sk]) ).
cnf(f30,axiom,
c_Datatype_Ooption_OSome(V_a_H,T_a) != c_Datatype_Ooption_ONone,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Datatype_Ooption_Odistinct__2__iff1_0) ).
fof(f30_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)],[f30]) ).
fof(f30_sk,plain,
! [V_a_H,T_a] : c_Datatype_Ooption_OSome(V_a_H,T_a) != c_Datatype_Ooption_ONone,
inference(skolemisation,[status(esa)],[f30_nnf]) ).
cnf(c30,plain,
c_Datatype_Ooption_OSome(X0,X1) != c_Datatype_Ooption_ONone,
inference(cnf_transformation,[status(esa)],[f30_sk]) ).
cnf(f33,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/sandbox/benchmark/theBenchmark.p',cls_Datatype__Universe_OAtom__not__Scons__iff1_0) ).
fof(f33_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)],[f33]) ).
fof(f33_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)],[f33_nnf]) ).
cnf(c33,plain,
c_Datatype__Universe_OAtom(X0,X1,X2) != c_Datatype__Universe_OScons(X3,X4,X1,X2),
inference(cnf_transformation,[status(esa)],[f33_sk]) ).
cnf(f35,axiom,
c_Datatype__Universe_OIn0(V_M,T_a,T_b) != c_Datatype__Universe_OIn1(V_N,T_a,T_b),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Datatype__Universe_OIn0__not__In1__iff1_0) ).
fof(f35_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)],[f35]) ).
fof(f35_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)],[f35_nnf]) ).
cnf(c35,plain,
c_Datatype__Universe_OIn0(X0,X1,X2) != c_Datatype__Universe_OIn1(X3,X1,X2),
inference(cnf_transformation,[status(esa)],[f35_sk]) ).
cnf(f37,axiom,
c_Datatype__Universe_OIn1(V_N,T_a,T_b) != c_Datatype__Universe_OIn0(V_M,T_a,T_b),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Datatype__Universe_OIn1__not__In0__iff1_0) ).
fof(f37_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)],[f37]) ).
fof(f37_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)],[f37_nnf]) ).
cnf(c37,plain,
c_Datatype__Universe_OIn1(X0,X1,X2) != c_Datatype__Universe_OIn0(X3,X1,X2),
inference(cnf_transformation,[status(esa)],[f37_sk]) ).
cnf(f38,axiom,
c_Datatype__Universe_OLeaf(V_a,T_a,T_b) != c_Datatype__Universe_ONumb(V_k,T_a,T_b),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Datatype__Universe_OLeaf__not__Numb__iff1_0) ).
fof(f38_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)],[f38]) ).
fof(f38_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)],[f38_nnf]) ).
cnf(c38,plain,
c_Datatype__Universe_OLeaf(X0,X1,X2) != c_Datatype__Universe_ONumb(X3,X1,X2),
inference(cnf_transformation,[status(esa)],[f38_sk]) ).
cnf(f39,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/sandbox/benchmark/theBenchmark.p',cls_Datatype__Universe_OLeaf__not__Scons__iff1_0) ).
fof(f39_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)],[f39]) ).
fof(f39_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)],[f39_nnf]) ).
cnf(c39,plain,
c_Datatype__Universe_OLeaf(X0,X1,X2) != c_Datatype__Universe_OScons(X3,X4,X1,X2),
inference(cnf_transformation,[status(esa)],[f39_sk]) ).
cnf(f40,axiom,
c_Datatype__Universe_ONumb(V_k,T_a,T_b) != c_Datatype__Universe_OLeaf(V_a,T_a,T_b),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Datatype__Universe_ONumb__not__Leaf__iff1_0) ).
fof(f40_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)],[f40]) ).
fof(f40_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)],[f40_nnf]) ).
cnf(c40,plain,
c_Datatype__Universe_ONumb(X0,X1,X2) != c_Datatype__Universe_OLeaf(X3,X1,X2),
inference(cnf_transformation,[status(esa)],[f40_sk]) ).
cnf(f41,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/sandbox/benchmark/theBenchmark.p',cls_Datatype__Universe_ONumb__not__Scons__iff1_0) ).
fof(f41_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)],[f41]) ).
fof(f41_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)],[f41_nnf]) ).
cnf(c41,plain,
c_Datatype__Universe_ONumb(X0,X1,X2) != c_Datatype__Universe_OScons(X3,X4,X1,X2),
inference(cnf_transformation,[status(esa)],[f41_sk]) ).
cnf(f44,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/sandbox/benchmark/theBenchmark.p',cls_Datatype__Universe_OScons__not__Atom__iff1_0) ).
fof(f44_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)],[f44]) ).
fof(f44_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)],[f44_nnf]) ).
cnf(c44,plain,
c_Datatype__Universe_OScons(X0,X1,X2,X3) != c_Datatype__Universe_OAtom(X4,X2,X3),
inference(cnf_transformation,[status(esa)],[f44_sk]) ).
cnf(f45,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/sandbox/benchmark/theBenchmark.p',cls_Datatype__Universe_OScons__not__Leaf__iff1_0) ).
fof(f45_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)],[f45]) ).
fof(f45_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)],[f45_nnf]) ).
cnf(c45,plain,
c_Datatype__Universe_OScons(X0,X1,X2,X3) != c_Datatype__Universe_OLeaf(X4,X2,X3),
inference(cnf_transformation,[status(esa)],[f45_sk]) ).
cnf(f46,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/sandbox/benchmark/theBenchmark.p',cls_Datatype__Universe_OScons__not__Numb__iff1_0) ).
fof(f46_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)],[f46]) ).
fof(f46_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)],[f46_nnf]) ).
cnf(c46,plain,
c_Datatype__Universe_OScons(X0,X1,X2,X3) != c_Datatype__Universe_ONumb(X4,X2,X3),
inference(cnf_transformation,[status(esa)],[f46_sk]) ).
cnf(f53,axiom,
c_Extraction_Osumbool_OLeft != c_Extraction_Osumbool_ORight,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Extraction_Osumbool_Odistinct__1__iff1_0) ).
fof(f53_nnf,plain,
c_Extraction_Osumbool_OLeft != c_Extraction_Osumbool_ORight,
inference(nnf_transformation,[status(thm)],[f53]) ).
fof(f53_sk,plain,
c_Extraction_Osumbool_OLeft != c_Extraction_Osumbool_ORight,
inference(skolemisation,[status(esa)],[f53_nnf]) ).
cnf(c53,plain,
c_Extraction_Osumbool_OLeft != c_Extraction_Osumbool_ORight,
inference(cnf_transformation,[status(esa)],[f53_sk]) ).
cnf(f54,axiom,
c_Extraction_Osumbool_ORight != c_Extraction_Osumbool_OLeft,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Extraction_Osumbool_Odistinct__2__iff1_0) ).
fof(f54_nnf,plain,
c_Extraction_Osumbool_ORight != c_Extraction_Osumbool_OLeft,
inference(nnf_transformation,[status(thm)],[f54]) ).
fof(f54_sk,plain,
c_Extraction_Osumbool_ORight != c_Extraction_Osumbool_OLeft,
inference(skolemisation,[status(esa)],[f54_nnf]) ).
cnf(c54,plain,
c_Extraction_Osumbool_ORight != c_Extraction_Osumbool_OLeft,
inference(cnf_transformation,[status(esa)],[f54_sk]) ).
cnf(f67,axiom,
~ c_in(c_UNIV,c_Finite__Set_OFinites,tc_set(tc_nat)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Infinite__Set_Onat__not__finite_0) ).
fof(f67_nnf,plain,
~ c_in(c_UNIV,c_Finite__Set_OFinites,tc_set(tc_nat)),
inference(nnf_transformation,[status(thm)],[f67]) ).
fof(f67_sk,plain,
~ c_in(c_UNIV,c_Finite__Set_OFinites,tc_set(tc_nat)),
inference(skolemisation,[status(esa)],[f67_nnf]) ).
cnf(c67,plain,
~ c_in(c_UNIV,c_Finite__Set_OFinites,tc_set(tc_nat)),
inference(cnf_transformation,[status(esa)],[f67_sk]) ).
cnf(f75,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/sandbox/benchmark/theBenchmark.p',cls_List_ONil2__notin__lex__iff1_0) ).
fof(f75_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)],[f75]) ).
fof(f75_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)],[f75_nnf]) ).
cnf(c75,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)],[f75_sk]) ).
cnf(f81,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/sandbox/benchmark/theBenchmark.p',cls_List_ONil__notin__lex__iff1_0) ).
fof(f81_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)],[f81]) ).
fof(f81_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)],[f81_nnf]) ).
cnf(c81,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)],[f81_sk]) ).
cnf(f99,axiom,
~ c_less(c_0,c_Nat_Osize(c_List_Olist_ONil,tc_List_Olist(T_a)),tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_List_Olength__greater__0__conv__iff1_0) ).
fof(f99_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)],[f99]) ).
fof(f99_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)],[f99_nnf]) ).
cnf(c99,plain,
~ c_less(c_0,c_Nat_Osize(c_List_Olist_ONil,tc_List_Olist(X0)),tc_nat),
inference(cnf_transformation,[status(esa)],[f99_sk]) ).
cnf(f103,axiom,
c_List_Olist_ONil != c_List_Olist_OCons(V_a_H,V_list_H,T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_List_Olist_Odistinct__1__iff1_0) ).
fof(f103_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)],[f103]) ).
fof(f103_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)],[f103_nnf]) ).
cnf(c103,plain,
c_List_Olist_ONil != c_List_Olist_OCons(X0,X1,X2),
inference(cnf_transformation,[status(esa)],[f103_sk]) ).
cnf(f104,axiom,
c_List_Olist_OCons(V_a_H,V_list_H,T_a) != c_List_Olist_ONil,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_List_Olist_Odistinct__2__iff1_0) ).
fof(f104_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)],[f104]) ).
fof(f104_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)],[f104_nnf]) ).
cnf(c104,plain,
c_List_Olist_OCons(X0,X1,X2) != c_List_Olist_ONil,
inference(cnf_transformation,[status(esa)],[f104_sk]) ).
cnf(f126,axiom,
c_Suc(V_m) != c_0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Nat_OSuc__not__Zero__iff1_0) ).
fof(f126_nnf,plain,
! [V_m] : c_Suc(V_m) != c_0,
inference(nnf_transformation,[status(thm)],[f126]) ).
fof(f126_sk,plain,
! [V_m] : c_Suc(V_m) != c_0,
inference(skolemisation,[status(esa)],[f126_nnf]) ).
cnf(c126,plain,
c_Suc(X0) != c_0,
inference(cnf_transformation,[status(esa)],[f126_sk]) ).
cnf(f127,axiom,
c_0 != c_Suc(V_m),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Nat_OZero__not__Suc__iff1_0) ).
fof(f127_nnf,plain,
! [V_m] : c_0 != c_Suc(V_m),
inference(nnf_transformation,[status(thm)],[f127]) ).
fof(f127_sk,plain,
! [V_m] : c_0 != c_Suc(V_m),
inference(skolemisation,[status(esa)],[f127_nnf]) ).
cnf(c127,plain,
c_0 != c_Suc(X0),
inference(cnf_transformation,[status(esa)],[f127_sk]) ).
cnf(f141,axiom,
~ c_less(c_0,c_0,tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Nat_Oneq0__conv__iff2_0) ).
fof(f141_nnf,plain,
~ c_less(c_0,c_0,tc_nat),
inference(nnf_transformation,[status(thm)],[f141]) ).
fof(f141_sk,plain,
~ c_less(c_0,c_0,tc_nat),
inference(skolemisation,[status(esa)],[f141_nnf]) ).
cnf(c141,plain,
~ c_less(c_0,c_0,tc_nat),
inference(cnf_transformation,[status(esa)],[f141_sk]) ).
cnf(f142,axiom,
~ c_less(c_plus(V_i,V_j,tc_nat),V_i,tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Nat_Onot__add__less1__iff1_0) ).
fof(f142_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)],[f142]) ).
fof(f142_sk,plain,
! [V_i,V_j] : ~ c_less(c_plus(V_i,V_j,tc_nat),V_i,tc_nat),
inference(skolemisation,[status(esa)],[f142_nnf]) ).
cnf(c142,plain,
~ c_less(c_plus(X0,X1,tc_nat),X0,tc_nat),
inference(cnf_transformation,[status(esa)],[f142_sk]) ).
cnf(f143,axiom,
~ c_less(c_plus(V_j,V_i,tc_nat),V_i,tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Nat_Onot__add__less2__iff1_0) ).
fof(f143_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)],[f143]) ).
fof(f143_sk,plain,
! [V_j,V_i] : ~ c_less(c_plus(V_j,V_i,tc_nat),V_i,tc_nat),
inference(skolemisation,[status(esa)],[f143_nnf]) ).
cnf(c143,plain,
~ c_less(c_plus(X0,X1,tc_nat),X1,tc_nat),
inference(cnf_transformation,[status(esa)],[f143_sk]) ).
cnf(f144,axiom,
~ c_less(V_n,c_0,tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Nat_Onot__less0__iff1_0) ).
fof(f144_nnf,plain,
! [V_n] : ~ c_less(V_n,c_0,tc_nat),
inference(nnf_transformation,[status(thm)],[f144]) ).
fof(f144_sk,plain,
! [V_n] : ~ c_less(V_n,c_0,tc_nat),
inference(skolemisation,[status(esa)],[f144_nnf]) ).
cnf(c144,plain,
~ c_less(X0,c_0,tc_nat),
inference(cnf_transformation,[status(esa)],[f144_sk]) ).
cnf(f145,axiom,
c_Numeral_Obit_OB0 != c_Numeral_Obit_OB1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Numeral_Obit_Odistinct__1__iff1_0) ).
fof(f145_nnf,plain,
c_Numeral_Obit_OB0 != c_Numeral_Obit_OB1,
inference(nnf_transformation,[status(thm)],[f145]) ).
fof(f145_sk,plain,
c_Numeral_Obit_OB0 != c_Numeral_Obit_OB1,
inference(skolemisation,[status(esa)],[f145_nnf]) ).
cnf(c145,plain,
c_Numeral_Obit_OB0 != c_Numeral_Obit_OB1,
inference(cnf_transformation,[status(esa)],[f145_sk]) ).
cnf(f146,axiom,
c_Numeral_Obit_OB1 != c_Numeral_Obit_OB0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Numeral_Obit_Odistinct__2__iff1_0) ).
fof(f146_nnf,plain,
c_Numeral_Obit_OB1 != c_Numeral_Obit_OB0,
inference(nnf_transformation,[status(thm)],[f146]) ).
fof(f146_sk,plain,
c_Numeral_Obit_OB1 != c_Numeral_Obit_OB0,
inference(skolemisation,[status(esa)],[f146_nnf]) ).
cnf(c146,plain,
c_Numeral_Obit_OB1 != c_Numeral_Obit_OB0,
inference(cnf_transformation,[status(esa)],[f146_sk]) ).
cnf(f147,axiom,
( ~ c_less(V_x,V_x,T_a)
| ~ class_Orderings_Oorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Orderings_Oorder__less__irrefl__iff1_0) ).
fof(f147_nnf,plain,
! [T_a,V_x] :
( ~ c_less(V_x,V_x,T_a)
| ~ class_Orderings_Oorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f147]) ).
fof(f147_sk,plain,
! [T_a,V_x] :
( ~ c_less(V_x,V_x,T_a)
| ~ class_Orderings_Oorder(T_a) ),
inference(skolemisation,[status(esa)],[f147_nnf]) ).
cnf(c147,plain,
( ~ c_less(X1,X1,X0)
| ~ class_Orderings_Oorder(X0) ),
inference(cnf_transformation,[status(esa)],[f147_sk]) ).
cnf(f176,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/sandbox/benchmark/theBenchmark.p',cls_Set_OComplD__dest_0) ).
fof(f176_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)],[f176]) ).
fof(f176_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)],[f176_nnf]) ).
cnf(c176,plain,
( ~ c_in(X0,c_uminus(X1,tc_set(X2)),X2)
| ~ c_in(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f176_sk]) ).
cnf(f181,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/sandbox/benchmark/theBenchmark.p',cls_Set_ODiffE_0) ).
fof(f181_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)],[f181]) ).
fof(f181_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)],[f181_nnf]) ).
cnf(c181,plain,
( ~ c_in(X0,c_minus(X3,X1,tc_set(X2)),X2)
| ~ c_in(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f181_sk]) ).
cnf(f190,axiom,
c_UNIV != c_emptyset,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Set_OUNIV__not__empty__iff1_0) ).
fof(f190_nnf,plain,
c_UNIV != c_emptyset,
inference(nnf_transformation,[status(thm)],[f190]) ).
fof(f190_sk,plain,
c_UNIV != c_emptyset,
inference(skolemisation,[status(esa)],[f190_nnf]) ).
cnf(c190,plain,
c_UNIV != c_emptyset,
inference(cnf_transformation,[status(esa)],[f190_sk]) ).
cnf(f198,axiom,
~ c_in(V_a,c_emptyset,T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Set_OemptyE_0) ).
fof(f198_nnf,plain,
! [V_a,T_a] : ~ c_in(V_a,c_emptyset,T_a),
inference(nnf_transformation,[status(thm)],[f198]) ).
fof(f198_sk,plain,
! [V_a,T_a] : ~ c_in(V_a,c_emptyset,T_a),
inference(skolemisation,[status(esa)],[f198_nnf]) ).
cnf(c198,plain,
~ c_in(X0,c_emptyset,X1),
inference(cnf_transformation,[status(esa)],[f198_sk]) ).
cnf(f202,axiom,
~ c_less(V_A,c_emptyset,tc_set(T_a)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Set_Onot__psubset__empty__iff1_0) ).
fof(f202_nnf,plain,
! [V_A,T_a] : ~ c_less(V_A,c_emptyset,tc_set(T_a)),
inference(nnf_transformation,[status(thm)],[f202]) ).
fof(f202_sk,plain,
! [V_A,T_a] : ~ c_less(V_A,c_emptyset,tc_set(T_a)),
inference(skolemisation,[status(esa)],[f202_nnf]) ).
cnf(c202,plain,
~ c_less(X0,c_emptyset,tc_set(X1)),
inference(cnf_transformation,[status(esa)],[f202_sk]) ).
cnf(f210,axiom,
c_Sum__Type_OInl(V_a,T_a,T_b) != c_Sum__Type_OInr(V_b,T_b,T_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Sum__Type_OInl__not__Inr__iff1_0) ).
fof(f210_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)],[f210]) ).
fof(f210_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)],[f210_nnf]) ).
cnf(c210,plain,
c_Sum__Type_OInl(X0,X1,X2) != c_Sum__Type_OInr(X3,X2,X1),
inference(cnf_transformation,[status(esa)],[f210_sk]) ).
cnf(f212,axiom,
c_Sum__Type_OInr(V_b,T_b,T_a) != c_Sum__Type_OInl(V_a,T_a,T_b),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Sum__Type_OInr__not__Inl__iff1_0) ).
fof(f212_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)],[f212]) ).
fof(f212_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)],[f212_nnf]) ).
cnf(c212,plain,
c_Sum__Type_OInr(X0,X1,X2) != c_Sum__Type_OInl(X3,X2,X1),
inference(cnf_transformation,[status(esa)],[f212_sk]) ).
cnf(f216,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/sandbox/benchmark/theBenchmark.p',cls_Wellfounded__Recursion_Oacyclic__insert__iff1_1) ).
fof(f216_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)],[f216]) ).
fof(f216_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)],[f216_nnf]) ).
cnf(c216,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)],[f216_sk]) ).
cnf(f219,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/sandbox/benchmark/theBenchmark.p',cls_Wellfounded__Recursion_Owf__insert__iff1_1) ).
fof(f219_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)],[f219]) ).
fof(f219_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)],[f219_nnf]) ).
cnf(c219,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)],[f219_sk]) ).
cnf(f288,axiom,
~ c_less(V_n,V_n,tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Nat_Oless__irrefl_0) ).
fof(f288_nnf,plain,
! [V_n] : ~ c_less(V_n,V_n,tc_nat),
inference(nnf_transformation,[status(thm)],[f288]) ).
fof(f288_sk,plain,
! [V_n] : ~ c_less(V_n,V_n,tc_nat),
inference(skolemisation,[status(esa)],[f288_nnf]) ).
cnf(c288,plain,
~ c_less(X0,X0,tc_nat),
inference(cnf_transformation,[status(esa)],[f288_sk]) ).
cnf(f324,axiom,
( ~ c_lessequals(V_B,V_A,tc_set(T_a))
| ~ c_less(V_A,V_B,tc_set(T_a)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Set_OpsubsetE_0) ).
fof(f324_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)],[f324]) ).
fof(f324_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)],[f324_nnf]) ).
cnf(c324,plain,
( ~ c_lessequals(X1,X0,tc_set(X2))
| ~ c_less(X0,X1,tc_set(X2)) ),
inference(cnf_transformation,[status(esa)],[f324_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c8,c11,c12,c13,c14,c15,c16,c17,c18,c29,c30,c33,c35,c37,c38,c39,c40,c41,c44,c45,c46,c53,c54,c67,c75,c81,c99,c103,c104,c126,c127,c141,c142,c143,c144,c145,c146,c147,c176,c181,c190,c198,c202,c210,c212,c216,c219,c288,c324,c1384]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t774]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : COL103-1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/10.38 % Computer : n017.cluster.edu
% 0.09/10.38 % Model : x86_64 x86_64
% 0.09/10.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/10.38 % Memory : 8046.5625MB
% 0.09/10.38 % OS : Linux 6.8.0-71-generic
% 0.09/10.38 % CPULimit : 300
% 0.09/10.38 % WCLimit : 300
% 0.09/10.38 % DateTime : Fri Sep 25 07:31:13 UTC 2026
% 0.09/10.38 % CPUTime :
% 0.09/10.38 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 24.41/13.63 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 24.41/13.63 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------