%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SCT074-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n003.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 02:39:56 PM UTC 2026
% Result : Unsatisfiable 14.25s 2.24s
% Output : Proof 14.25s
% Verified :
% Comments :
%------------------------------------------------------------------------------
cnf(t37,axiom,
sF2 = c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_Lab____,tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),
introduced(definition) ).
cnf(t35,axiom,
sF0 = c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),
introduced(definition) ).
cnf(t46,plain,
c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt) = sF0,
inference(orient,[status(thm)],[t35]) ).
cnf(t214,plain,
sF2 = c_in(sF0,v_Lab____,tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),
inference(step,[status(thm)],[t37,t46]) ).
cnf(t36,axiom,
sF1 = tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),
introduced(definition) ).
cnf(t44,plain,
tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt) = sF1,
inference(orient,[status(thm)],[t36]) ).
cnf(t215,plain,
sF2 = c_in(sF0,v_Lab____,sF1),
inference(step,[status(thm)],[t214,t44]) ).
cnf(f688,negated_conjecture,
c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_Lab____,tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f688_nnf,plain,
c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_Lab____,tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),
inference(nnf_transformation,[status(thm)],[f688]) ).
cnf(c688,plain,
c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_Lab____,tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),
inference(cnf_transformation,[status(esa)],[f688_nnf]) ).
cnf(t13,plain,
c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_Lab____,tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) = true,
inference(equality_encoding,[status(esa)],[c688]) ).
cnf(t212,plain,
c_in(sF0,v_Lab____,tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) = true,
inference(step,[status(thm)],[t13,t46]) ).
cnf(t213,plain,
c_in(sF0,v_Lab____,sF1) = true,
inference(step,[status(thm)],[t212,t44]) ).
cnf(t53,plain,
c_in(sF0,v_Lab____,sF1) = true,
inference(orient,[status(thm)],[t213]) ).
cnf(t216,plain,
sF2 = true,
inference(step,[status(thm)],[t215,t53]) ).
cnf(t54,plain,
true = sF2,
inference(orient,[status(thm)],[t216]) ).
cnf(f587,axiom,
( ~ c_in(V_L,c_Arrow__Order__Mirabelle_OLin,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))
| ~ c_in(c_Pair(V_a,V_b,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),V_L,tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_Pair(V_b,V_a,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),V_L,tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Lin__irrefl_0) ).
fof(f587_nnf,plain,
! [V_b,V_a,V_L] :
( ~ c_in(V_L,c_Arrow__Order__Mirabelle_OLin,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))
| ~ c_in(c_Pair(V_a,V_b,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),V_L,tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_Pair(V_b,V_a,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),V_L,tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(nnf_transformation,[status(thm)],[f587]) ).
fof(f587_sk,plain,
! [V_b,V_a,V_L] :
( ~ c_in(V_L,c_Arrow__Order__Mirabelle_OLin,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))
| ~ c_in(c_Pair(V_a,V_b,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),V_L,tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_Pair(V_b,V_a,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),V_L,tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(skolemisation,[status(esa)],[f587_nnf]) ).
cnf(c587,plain,
( ~ c_in(X2,c_Arrow__Order__Mirabelle_OLin,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))
| ~ c_in(c_Pair(X1,X0,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X2,tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))
| ~ c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X2,tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) ),
inference(cnf_transformation,[status(esa)],[f587_sk]) ).
cnf(t30,plain,
or(not(c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X3,tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))),or(not(c_in(c_Pair(X2,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X3,tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))),not(c_in(X3,c_Arrow__Order__Mirabelle_OLin,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))))) = true,
inference(equality_encoding,[status(esa)],[c587]) ).
cnf(t286,plain,
or(not(c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X3,sF1)),or(not(c_in(c_Pair(X2,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X3,tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt))),not(c_in(X3,c_Arrow__Order__Mirabelle_OLin,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))))) = true,
inference(step,[status(thm)],[t30,t44]) ).
cnf(t287,plain,
or(not(c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X3,sF1)),or(not(c_in(c_Pair(X2,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X3,sF1)),not(c_in(X3,c_Arrow__Order__Mirabelle_OLin,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool))))) = true,
inference(step,[status(thm)],[t286,t44]) ).
cnf(t288,plain,
or(not(c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X3,sF1)),or(not(c_in(c_Pair(X2,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X3,sF1)),not(c_in(X3,c_Arrow__Order__Mirabelle_OLin,tc_fun(sF1,tc_bool))))) = true,
inference(step,[status(thm)],[t287,t44]) ).
cnf(t289,plain,
or(not(c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X3,sF1)),or(not(c_in(c_Pair(X2,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X3,sF1)),not(c_in(X3,c_Arrow__Order__Mirabelle_OLin,tc_fun(sF1,tc_bool))))) = sF2,
inference(step,[status(thm)],[t288,t54]) ).
cnf(t167,plain,
or(not(c_in(c_Pair(X1,X2,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X3,sF1)),or(not(c_in(c_Pair(X2,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),X3,sF1)),not(c_in(X3,c_Arrow__Order__Mirabelle_OLin,tc_fun(sF1,tc_bool))))) = sF2,
inference(orient,[status(thm)],[t289]) ).
cnf(f687,axiom,
c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_Lab____,tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_CHAINED_0_01) ).
fof(f687_nnf,plain,
c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_Lab____,tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),
inference(nnf_transformation,[status(thm)],[f687]) ).
cnf(c687,plain,
c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_Lab____,tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),
inference(cnf_transformation,[status(esa)],[f687_nnf]) ).
cnf(t12,plain,
c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_Lab____,tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)) = true,
inference(equality_encoding,[status(esa)],[c687]) ).
cnf(t211,plain,
c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_Lab____,sF1) = true,
inference(step,[status(thm)],[t12,t44]) ).
cnf(t52,plain,
c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_Lab____,sF1) = true,
inference(orient,[status(thm)],[t211]) ).
cnf(t225,plain,
c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_Lab____,sF1) = sF2,
inference(step,[status(thm)],[t52,t54]) ).
cnf(t64,plain,
c_in(c_Pair(v_a____,v_b____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_Lab____,sF1) = sF2,
inference(orient,[status(thm)],[t225]) ).
cnf(t171,plain,
sF2 = or(not(sF2),or(not(c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_Lab____,sF1)),not(c_in(v_Lab____,c_Arrow__Order__Mirabelle_OLin,tc_fun(sF1,tc_bool))))),
inference(cp,[status(thm)],[t167,t64]) ).
cnf(t1,plain,
not(true) = false,
introduced(definition) ).
cnf(t39,plain,
not(true) = false,
inference(orient,[status(thm)],[t1]) ).
cnf(t219,plain,
not(sF2) = false,
inference(step,[status(thm)],[t39,t54]) ).
cnf(t57,plain,
not(sF2) = false,
inference(rw,[status(thm)],[t219]) ).
cnf(t68,plain,
not(sF2) = false,
inference(orient,[status(thm)],[t57]) ).
cnf(t290,plain,
sF2 = or(false,or(not(c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_Lab____,sF1)),not(c_in(v_Lab____,c_Arrow__Order__Mirabelle_OLin,tc_fun(sF1,tc_bool))))),
inference(step,[status(thm)],[t171,t68]) ).
cnf(t4,plain,
or(false,X1) = X1,
introduced(definition) ).
cnf(t42,plain,
or(false,X1) = X1,
inference(orient,[status(thm)],[t4]) ).
cnf(t291,plain,
sF2 = or(not(c_in(c_Pair(v_b____,v_a____,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),v_Lab____,sF1)),not(c_in(v_Lab____,c_Arrow__Order__Mirabelle_OLin,tc_fun(sF1,tc_bool)))),
inference(step,[status(thm)],[t290,t42]) ).
cnf(t292,plain,
sF2 = or(not(c_in(sF0,v_Lab____,sF1)),not(c_in(v_Lab____,c_Arrow__Order__Mirabelle_OLin,tc_fun(sF1,tc_bool)))),
inference(step,[status(thm)],[t291,t46]) ).
cnf(t227,plain,
c_in(sF0,v_Lab____,sF1) = sF2,
inference(step,[status(thm)],[t53,t54]) ).
cnf(t66,plain,
c_in(sF0,v_Lab____,sF1) = sF2,
inference(orient,[status(thm)],[t227]) ).
cnf(t293,plain,
sF2 = or(not(sF2),not(c_in(v_Lab____,c_Arrow__Order__Mirabelle_OLin,tc_fun(sF1,tc_bool)))),
inference(step,[status(thm)],[t292,t66]) ).
cnf(t294,plain,
sF2 = or(false,not(c_in(v_Lab____,c_Arrow__Order__Mirabelle_OLin,tc_fun(sF1,tc_bool)))),
inference(step,[status(thm)],[t293,t68]) ).
cnf(t295,plain,
sF2 = not(c_in(v_Lab____,c_Arrow__Order__Mirabelle_OLin,tc_fun(sF1,tc_bool))),
inference(step,[status(thm)],[t294,t42]) ).
cnf(f686,axiom,
c_in(v_Lab____,c_Arrow__Order__Mirabelle_OLin,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_CHAINED_0) ).
fof(f686_nnf,plain,
c_in(v_Lab____,c_Arrow__Order__Mirabelle_OLin,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)),
inference(nnf_transformation,[status(thm)],[f686]) ).
cnf(c686,plain,
c_in(v_Lab____,c_Arrow__Order__Mirabelle_OLin,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)),
inference(cnf_transformation,[status(esa)],[f686_nnf]) ).
cnf(t11,plain,
c_in(v_Lab____,c_Arrow__Order__Mirabelle_OLin,tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)) = true,
inference(equality_encoding,[status(esa)],[c686]) ).
cnf(t210,plain,
c_in(v_Lab____,c_Arrow__Order__Mirabelle_OLin,tc_fun(sF1,tc_bool)) = true,
inference(step,[status(thm)],[t11,t44]) ).
cnf(t51,plain,
c_in(v_Lab____,c_Arrow__Order__Mirabelle_OLin,tc_fun(sF1,tc_bool)) = true,
inference(orient,[status(thm)],[t210]) ).
cnf(t223,plain,
c_in(v_Lab____,c_Arrow__Order__Mirabelle_OLin,tc_fun(sF1,tc_bool)) = sF2,
inference(step,[status(thm)],[t51,t54]) ).
cnf(t62,plain,
c_in(v_Lab____,c_Arrow__Order__Mirabelle_OLin,tc_fun(sF1,tc_bool)) = sF2,
inference(orient,[status(thm)],[t223]) ).
cnf(t296,plain,
sF2 = not(sF2),
inference(step,[status(thm)],[t295,t62]) ).
cnf(t297,plain,
sF2 = false,
inference(step,[status(thm)],[t296,t68]) ).
cnf(t173,plain,
false = sF2,
inference(orient,[status(thm)],[t297]) ).
cnf(f5,axiom,
c_Set_Oinsert(V_a,V_A,T_a) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_insert__not__empty_0) ).
fof(f5_nnf,plain,
! [V_a,V_A,T_a] : c_Set_Oinsert(V_a,V_A,T_a) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [V_a,V_A,T_a] : c_Set_Oinsert(V_a,V_A,T_a) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c5,plain,
c_Set_Oinsert(X0,X1,X2) != c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(f125,axiom,
~ hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),V_x)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_bot1E_0) ).
fof(f125_nnf,plain,
! [T_a,V_x] : ~ hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),V_x)),
inference(nnf_transformation,[status(thm)],[f125]) ).
fof(f125_sk,plain,
! [T_a,V_x] : ~ hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),V_x)),
inference(skolemisation,[status(esa)],[f125_nnf]) ).
cnf(c125,plain,
~ hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1)),
inference(cnf_transformation,[status(esa)],[f125_sk]) ).
cnf(f130,axiom,
( c_Lattices_Olower__semilattice__class_Oinf(V_A,V_B,tc_fun(T_a,tc_bool)) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))
| ~ c_in(V_x,V_A,T_a)
| ~ c_in(V_x,V_B,T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_disjoint__iff__not__equal_0) ).
fof(f130_nnf,plain,
! [V_x,V_B,T_a,V_A] :
( c_Lattices_Olower__semilattice__class_Oinf(V_A,V_B,tc_fun(T_a,tc_bool)) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))
| ~ c_in(V_x,V_A,T_a)
| ~ c_in(V_x,V_B,T_a) ),
inference(nnf_transformation,[status(thm)],[f130]) ).
fof(f130_sk,plain,
! [V_x,V_B,T_a,V_A] :
( c_Lattices_Olower__semilattice__class_Oinf(V_A,V_B,tc_fun(T_a,tc_bool)) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool))
| ~ c_in(V_x,V_A,T_a)
| ~ c_in(V_x,V_B,T_a) ),
inference(skolemisation,[status(esa)],[f130_nnf]) ).
cnf(c130,plain,
( c_Lattices_Olower__semilattice__class_Oinf(X3,X1,tc_fun(X2,tc_bool)) != c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool))
| ~ c_in(X0,X3,X2)
| ~ c_in(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f130_sk]) ).
cnf(f166,axiom,
c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) != c_Set_Oinsert(V_a,V_A,T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_empty__not__insert_0) ).
fof(f166_nnf,plain,
! [T_a,V_a,V_A] : c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) != c_Set_Oinsert(V_a,V_A,T_a),
inference(nnf_transformation,[status(thm)],[f166]) ).
fof(f166_sk,plain,
! [T_a,V_a,V_A] : c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) != c_Set_Oinsert(V_a,V_A,T_a),
inference(skolemisation,[status(esa)],[f166_nnf]) ).
cnf(c166,plain,
c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)) != c_Set_Oinsert(X1,X2,X0),
inference(cnf_transformation,[status(esa)],[f166_sk]) ).
cnf(f265,axiom,
~ c_in(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_ex__in__conv_0) ).
fof(f265_nnf,plain,
! [V_x,T_a] : ~ c_in(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),
inference(nnf_transformation,[status(thm)],[f265]) ).
fof(f265_sk,plain,
! [V_x,T_a] : ~ c_in(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),
inference(skolemisation,[status(esa)],[f265_nnf]) ).
cnf(c265,plain,
~ c_in(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1),
inference(cnf_transformation,[status(esa)],[f265_sk]) ).
cnf(f267,axiom,
~ c_in(V_c,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_empty__iff_0) ).
fof(f267_nnf,plain,
! [V_c,T_a] : ~ c_in(V_c,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),
inference(nnf_transformation,[status(thm)],[f267]) ).
fof(f267_sk,plain,
! [V_c,T_a] : ~ c_in(V_c,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),
inference(skolemisation,[status(esa)],[f267_nnf]) ).
cnf(c267,plain,
~ c_in(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1),
inference(cnf_transformation,[status(esa)],[f267_sk]) ).
cnf(f268,axiom,
~ c_in(V_a,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_emptyE_0) ).
fof(f268_nnf,plain,
! [V_a,T_a] : ~ c_in(V_a,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),
inference(nnf_transformation,[status(thm)],[f268]) ).
fof(f268_sk,plain,
! [V_a,T_a] : ~ c_in(V_a,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a),
inference(skolemisation,[status(esa)],[f268_nnf]) ).
cnf(c268,plain,
~ c_in(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1),
inference(cnf_transformation,[status(esa)],[f268_sk]) ).
cnf(f271,axiom,
( ~ c_in(V_c,c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),T_a)
| ~ c_in(V_c,V_B,T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_DiffE_1) ).
fof(f271_nnf,plain,
! [V_c,V_B,T_a,V_A] :
( ~ c_in(V_c,c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),T_a)
| ~ c_in(V_c,V_B,T_a) ),
inference(nnf_transformation,[status(thm)],[f271]) ).
fof(f271_sk,plain,
! [V_c,V_B,T_a,V_A] :
( ~ c_in(V_c,c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),T_a)
| ~ c_in(V_c,V_B,T_a) ),
inference(skolemisation,[status(esa)],[f271_nnf]) ).
cnf(c271,plain,
( ~ c_in(X0,c_HOL_Ominus__class_Ominus(X3,X1,tc_fun(X2,tc_bool)),X2)
| ~ c_in(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f271_sk]) ).
cnf(f278,axiom,
( ~ c_in(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)
| ~ hBOOL(hAPP(V_P,V_x)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_bex__empty_0) ).
fof(f278_nnf,plain,
! [V_P,V_x,T_a] :
( ~ c_in(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)
| ~ hBOOL(hAPP(V_P,V_x)) ),
inference(nnf_transformation,[status(thm)],[f278]) ).
fof(f278_sk,plain,
! [V_P,V_x,T_a] :
( ~ c_in(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)
| ~ hBOOL(hAPP(V_P,V_x)) ),
inference(skolemisation,[status(esa)],[f278_nnf]) ).
cnf(c278,plain,
( ~ c_in(X1,c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)),X2)
| ~ hBOOL(hAPP(X0,X1)) ),
inference(cnf_transformation,[status(esa)],[f278_sk]) ).
cnf(f351,axiom,
( ~ c_Wellfounded_Oacyclic(c_Set_Oinsert(c_Pair(V_y,V_x,T_a,T_a),V_r,tc_prod(T_a,T_a)),T_a)
| ~ 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)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_acyclic__insert_1) ).
fof(f351_nnf,plain,
! [V_x,V_y,T_a,V_r] :
( ~ c_Wellfounded_Oacyclic(c_Set_Oinsert(c_Pair(V_y,V_x,T_a,T_a),V_r,tc_prod(T_a,T_a)),T_a)
| ~ 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)) ),
inference(nnf_transformation,[status(thm)],[f351]) ).
fof(f351_sk,plain,
! [V_x,V_y,T_a,V_r] :
( ~ c_Wellfounded_Oacyclic(c_Set_Oinsert(c_Pair(V_y,V_x,T_a,T_a),V_r,tc_prod(T_a,T_a)),T_a)
| ~ 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)) ),
inference(skolemisation,[status(esa)],[f351_nnf]) ).
cnf(c351,plain,
( ~ c_Wellfounded_Oacyclic(c_Set_Oinsert(c_Pair(X1,X0,X2,X2),X3,tc_prod(X2,X2)),X2)
| ~ c_in(c_Pair(X0,X1,X2,X2),c_Transitive__Closure_Ortrancl(X3,X2),tc_prod(X2,X2)) ),
inference(cnf_transformation,[status(esa)],[f351_sk]) ).
cnf(f428,axiom,
( ~ c_Wellfounded_Owf(c_Set_Oinsert(c_Pair(V_y,V_x,T_a,T_a),V_r,tc_prod(T_a,T_a)),T_a)
| ~ 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)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_wf__insert_1) ).
fof(f428_nnf,plain,
! [V_x,V_y,T_a,V_r] :
( ~ c_Wellfounded_Owf(c_Set_Oinsert(c_Pair(V_y,V_x,T_a,T_a),V_r,tc_prod(T_a,T_a)),T_a)
| ~ 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)) ),
inference(nnf_transformation,[status(thm)],[f428]) ).
fof(f428_sk,plain,
! [V_x,V_y,T_a,V_r] :
( ~ c_Wellfounded_Owf(c_Set_Oinsert(c_Pair(V_y,V_x,T_a,T_a),V_r,tc_prod(T_a,T_a)),T_a)
| ~ 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)) ),
inference(skolemisation,[status(esa)],[f428_nnf]) ).
cnf(c428,plain,
( ~ c_Wellfounded_Owf(c_Set_Oinsert(c_Pair(X1,X0,X2,X2),X3,tc_prod(X2,X2)),X2)
| ~ c_in(c_Pair(X0,X1,X2,X2),c_Transitive__Closure_Ortrancl(X3,X2),tc_prod(X2,X2)) ),
inference(cnf_transformation,[status(esa)],[f428_sk]) ).
cnf(f453,axiom,
( ~ c_Wellfounded_Oacyclic(V_r,T_a)
| ~ c_in(c_Pair(V_x,V_x,T_a,T_a),c_Transitive__Closure_Otrancl(V_r,T_a),tc_prod(T_a,T_a)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_acyclic__def_0) ).
fof(f453_nnf,plain,
! [V_x,T_a,V_r] :
( ~ c_Wellfounded_Oacyclic(V_r,T_a)
| ~ c_in(c_Pair(V_x,V_x,T_a,T_a),c_Transitive__Closure_Otrancl(V_r,T_a),tc_prod(T_a,T_a)) ),
inference(nnf_transformation,[status(thm)],[f453]) ).
fof(f453_sk,plain,
! [V_x,T_a,V_r] :
( ~ c_Wellfounded_Oacyclic(V_r,T_a)
| ~ c_in(c_Pair(V_x,V_x,T_a,T_a),c_Transitive__Closure_Otrancl(V_r,T_a),tc_prod(T_a,T_a)) ),
inference(skolemisation,[status(esa)],[f453_nnf]) ).
cnf(c453,plain,
( ~ c_Wellfounded_Oacyclic(X2,X1)
| ~ c_in(c_Pair(X0,X0,X1,X1),c_Transitive__Closure_Otrancl(X2,X1),tc_prod(X1,X1)) ),
inference(cnf_transformation,[status(esa)],[f453_sk]) ).
cnf(f478,axiom,
( ~ c_in(c_Pair(V_x,V_x,T_a,T_a),c_Transitive__Closure_Otrancl(V_r,T_a),tc_prod(T_a,T_a))
| c_Lattices_Olower__semilattice__class_Oinf(c_Relation_Oconverse(V_r,T_a,T_a),c_Transitive__Closure_Ortrancl(V_r,T_a),tc_fun(tc_prod(T_a,T_a),tc_bool)) != c_Orderings_Obot__class_Obot(tc_fun(tc_prod(T_a,T_a),tc_bool)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_irrefl__tranclI_0) ).
fof(f478_nnf,plain,
! [V_r,T_a,V_x] :
( ~ c_in(c_Pair(V_x,V_x,T_a,T_a),c_Transitive__Closure_Otrancl(V_r,T_a),tc_prod(T_a,T_a))
| c_Lattices_Olower__semilattice__class_Oinf(c_Relation_Oconverse(V_r,T_a,T_a),c_Transitive__Closure_Ortrancl(V_r,T_a),tc_fun(tc_prod(T_a,T_a),tc_bool)) != c_Orderings_Obot__class_Obot(tc_fun(tc_prod(T_a,T_a),tc_bool)) ),
inference(nnf_transformation,[status(thm)],[f478]) ).
fof(f478_sk,plain,
! [V_r,T_a,V_x] :
( ~ c_in(c_Pair(V_x,V_x,T_a,T_a),c_Transitive__Closure_Otrancl(V_r,T_a),tc_prod(T_a,T_a))
| c_Lattices_Olower__semilattice__class_Oinf(c_Relation_Oconverse(V_r,T_a,T_a),c_Transitive__Closure_Ortrancl(V_r,T_a),tc_fun(tc_prod(T_a,T_a),tc_bool)) != c_Orderings_Obot__class_Obot(tc_fun(tc_prod(T_a,T_a),tc_bool)) ),
inference(skolemisation,[status(esa)],[f478_nnf]) ).
cnf(c478,plain,
( ~ c_in(c_Pair(X2,X2,X1,X1),c_Transitive__Closure_Otrancl(X0,X1),tc_prod(X1,X1))
| c_Lattices_Olower__semilattice__class_Oinf(c_Relation_Oconverse(X0,X1,X1),c_Transitive__Closure_Ortrancl(X0,X1),tc_fun(tc_prod(X1,X1),tc_bool)) != c_Orderings_Obot__class_Obot(tc_fun(tc_prod(X1,X1),tc_bool)) ),
inference(cnf_transformation,[status(esa)],[f478_sk]) ).
cnf(f592,axiom,
( ~ c_Wellfounded_Owf(V_R,T_a)
| ~ c_in(V_x,V_Q,T_a)
| ~ c_in(c_Pair(V_y,c_ATP__Linkup_Osko__Wellfounded__XwfE__min__1__1(V_Q,V_R,T_a),T_a,T_a),V_R,tc_prod(T_a,T_a))
| ~ c_in(V_y,V_Q,T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_wfE__min_1) ).
fof(f592_nnf,plain,
! [V_y,V_Q,T_a,V_R,V_x] :
( ~ c_Wellfounded_Owf(V_R,T_a)
| ~ c_in(V_x,V_Q,T_a)
| ~ c_in(c_Pair(V_y,c_ATP__Linkup_Osko__Wellfounded__XwfE__min__1__1(V_Q,V_R,T_a),T_a,T_a),V_R,tc_prod(T_a,T_a))
| ~ c_in(V_y,V_Q,T_a) ),
inference(nnf_transformation,[status(thm)],[f592]) ).
fof(f592_sk,plain,
! [V_y,V_Q,T_a,V_R,V_x] :
( ~ c_Wellfounded_Owf(V_R,T_a)
| ~ c_in(V_x,V_Q,T_a)
| ~ c_in(c_Pair(V_y,c_ATP__Linkup_Osko__Wellfounded__XwfE__min__1__1(V_Q,V_R,T_a),T_a,T_a),V_R,tc_prod(T_a,T_a))
| ~ c_in(V_y,V_Q,T_a) ),
inference(skolemisation,[status(esa)],[f592_nnf]) ).
cnf(c592,plain,
( ~ c_Wellfounded_Owf(X3,X2)
| ~ c_in(X4,X1,X2)
| ~ c_in(c_Pair(X0,c_ATP__Linkup_Osko__Wellfounded__XwfE__min__1__1(X1,X3,X2),X2,X2),X3,tc_prod(X2,X2))
| ~ c_in(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f592_sk]) ).
cnf(f604,axiom,
( ~ c_Wellfounded_Owf(V_r,T_a)
| ~ c_in(V_xa,V_Q,T_a)
| ~ c_in(c_Pair(V_y,c_ATP__Linkup_Osko__Wellfounded__Xwf__eq__minimal__1__1(V_Q,V_r,T_a),T_a,T_a),V_r,tc_prod(T_a,T_a))
| ~ c_in(V_y,V_Q,T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_wf__eq__minimal_1) ).
fof(f604_nnf,plain,
! [V_y,V_Q,T_a,V_r,V_xa] :
( ~ c_Wellfounded_Owf(V_r,T_a)
| ~ c_in(V_xa,V_Q,T_a)
| ~ c_in(c_Pair(V_y,c_ATP__Linkup_Osko__Wellfounded__Xwf__eq__minimal__1__1(V_Q,V_r,T_a),T_a,T_a),V_r,tc_prod(T_a,T_a))
| ~ c_in(V_y,V_Q,T_a) ),
inference(nnf_transformation,[status(thm)],[f604]) ).
fof(f604_sk,plain,
! [V_y,V_Q,T_a,V_r,V_xa] :
( ~ c_Wellfounded_Owf(V_r,T_a)
| ~ c_in(V_xa,V_Q,T_a)
| ~ c_in(c_Pair(V_y,c_ATP__Linkup_Osko__Wellfounded__Xwf__eq__minimal__1__1(V_Q,V_r,T_a),T_a,T_a),V_r,tc_prod(T_a,T_a))
| ~ c_in(V_y,V_Q,T_a) ),
inference(skolemisation,[status(esa)],[f604_nnf]) ).
cnf(c604,plain,
( ~ c_Wellfounded_Owf(X3,X2)
| ~ c_in(X4,X1,X2)
| ~ c_in(c_Pair(X0,c_ATP__Linkup_Osko__Wellfounded__Xwf__eq__minimal__1__1(X1,X3,X2),X2,X2),X3,tc_prod(X2,X2))
| ~ c_in(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f604_sk]) ).
cnf(f621,axiom,
( ~ c_Relation_Oirrefl(V_r,T_a)
| ~ c_in(c_Pair(V_x,V_x,T_a,T_a),V_r,tc_prod(T_a,T_a)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_irrefl__def_0) ).
fof(f621_nnf,plain,
! [V_x,T_a,V_r] :
( ~ c_Relation_Oirrefl(V_r,T_a)
| ~ c_in(c_Pair(V_x,V_x,T_a,T_a),V_r,tc_prod(T_a,T_a)) ),
inference(nnf_transformation,[status(thm)],[f621]) ).
fof(f621_sk,plain,
! [V_x,T_a,V_r] :
( ~ c_Relation_Oirrefl(V_r,T_a)
| ~ c_in(c_Pair(V_x,V_x,T_a,T_a),V_r,tc_prod(T_a,T_a)) ),
inference(skolemisation,[status(esa)],[f621_nnf]) ).
cnf(c621,plain,
( ~ c_Relation_Oirrefl(X2,X1)
| ~ c_in(c_Pair(X0,X0,X1,X1),X2,tc_prod(X1,X1)) ),
inference(cnf_transformation,[status(esa)],[f621_sk]) ).
cnf(f630,axiom,
( ~ c_Wellfounded_Owf(V_r,T_a)
| ~ c_in(c_Pair(V_a,V_x,T_a,T_a),V_r,tc_prod(T_a,T_a))
| ~ c_in(c_Pair(V_x,V_a,T_a,T_a),V_r,tc_prod(T_a,T_a)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_wf__asym_0) ).
fof(f630_nnf,plain,
! [V_x,V_a,T_a,V_r] :
( ~ c_Wellfounded_Owf(V_r,T_a)
| ~ c_in(c_Pair(V_a,V_x,T_a,T_a),V_r,tc_prod(T_a,T_a))
| ~ c_in(c_Pair(V_x,V_a,T_a,T_a),V_r,tc_prod(T_a,T_a)) ),
inference(nnf_transformation,[status(thm)],[f630]) ).
fof(f630_sk,plain,
! [V_x,V_a,T_a,V_r] :
( ~ c_Wellfounded_Owf(V_r,T_a)
| ~ c_in(c_Pair(V_a,V_x,T_a,T_a),V_r,tc_prod(T_a,T_a))
| ~ c_in(c_Pair(V_x,V_a,T_a,T_a),V_r,tc_prod(T_a,T_a)) ),
inference(skolemisation,[status(esa)],[f630_nnf]) ).
cnf(c630,plain,
( ~ c_Wellfounded_Owf(X3,X2)
| ~ c_in(c_Pair(X1,X0,X2,X2),X3,tc_prod(X2,X2))
| ~ c_in(c_Pair(X0,X1,X2,X2),X3,tc_prod(X2,X2)) ),
inference(cnf_transformation,[status(esa)],[f630_sk]) ).
cnf(f638,axiom,
( ~ c_Wellfounded_Owf(V_r,T_a)
| ~ c_in(c_Pair(V_a,V_a,T_a,T_a),V_r,tc_prod(T_a,T_a)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_wf__irrefl_0) ).
fof(f638_nnf,plain,
! [V_a,T_a,V_r] :
( ~ c_Wellfounded_Owf(V_r,T_a)
| ~ c_in(c_Pair(V_a,V_a,T_a,T_a),V_r,tc_prod(T_a,T_a)) ),
inference(nnf_transformation,[status(thm)],[f638]) ).
fof(f638_sk,plain,
! [V_a,T_a,V_r] :
( ~ c_Wellfounded_Owf(V_r,T_a)
| ~ c_in(c_Pair(V_a,V_a,T_a,T_a),V_r,tc_prod(T_a,T_a)) ),
inference(skolemisation,[status(esa)],[f638_nnf]) ).
cnf(c638,plain,
( ~ c_Wellfounded_Owf(X2,X1)
| ~ c_in(c_Pair(X0,X0,X1,X1),X2,tc_prod(X1,X1)) ),
inference(cnf_transformation,[status(esa)],[f638_sk]) ).
cnf(f650,axiom,
~ c_in(c_Pair(V_x,V_x,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Arrow__Order__Mirabelle_Omktop(V_L,V_x),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_in__mktop_1) ).
fof(f650_nnf,plain,
! [V_x,V_L] : ~ c_in(c_Pair(V_x,V_x,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Arrow__Order__Mirabelle_Omktop(V_L,V_x),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),
inference(nnf_transformation,[status(thm)],[f650]) ).
fof(f650_sk,plain,
! [V_x,V_L] : ~ c_in(c_Pair(V_x,V_x,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Arrow__Order__Mirabelle_Omktop(V_L,V_x),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),
inference(skolemisation,[status(esa)],[f650_nnf]) ).
cnf(c650,plain,
~ c_in(c_Pair(X0,X0,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Arrow__Order__Mirabelle_Omktop(X1,X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),
inference(cnf_transformation,[status(esa)],[f650_sk]) ).
cnf(f651,axiom,
~ c_in(c_Pair(V_x,V_y,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Arrow__Order__Mirabelle_Omktop(V_L,V_x),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_in__mktop_0) ).
fof(f651_nnf,plain,
! [V_x,V_y,V_L] : ~ c_in(c_Pair(V_x,V_y,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Arrow__Order__Mirabelle_Omktop(V_L,V_x),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),
inference(nnf_transformation,[status(thm)],[f651]) ).
fof(f651_sk,plain,
! [V_x,V_y,V_L] : ~ c_in(c_Pair(V_x,V_y,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Arrow__Order__Mirabelle_Omktop(V_L,V_x),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),
inference(skolemisation,[status(esa)],[f651_nnf]) ).
cnf(c651,plain,
~ c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Arrow__Order__Mirabelle_Omktop(X2,X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),
inference(cnf_transformation,[status(esa)],[f651_sk]) ).
cnf(f654,axiom,
~ c_in(c_Pair(V_x,V_x,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Arrow__Order__Mirabelle_Omkbot(V_L,V_x),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_in__mkbot_1) ).
fof(f654_nnf,plain,
! [V_x,V_L] : ~ c_in(c_Pair(V_x,V_x,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Arrow__Order__Mirabelle_Omkbot(V_L,V_x),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),
inference(nnf_transformation,[status(thm)],[f654]) ).
fof(f654_sk,plain,
! [V_x,V_L] : ~ c_in(c_Pair(V_x,V_x,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Arrow__Order__Mirabelle_Omkbot(V_L,V_x),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),
inference(skolemisation,[status(esa)],[f654_nnf]) ).
cnf(c654,plain,
~ c_in(c_Pair(X0,X0,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Arrow__Order__Mirabelle_Omkbot(X1,X0),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),
inference(cnf_transformation,[status(esa)],[f654_sk]) ).
cnf(f655,axiom,
~ c_in(c_Pair(V_xa,V_x,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Arrow__Order__Mirabelle_Omkbot(V_L,V_x),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_in__mkbot_0) ).
fof(f655_nnf,plain,
! [V_xa,V_x,V_L] : ~ c_in(c_Pair(V_xa,V_x,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Arrow__Order__Mirabelle_Omkbot(V_L,V_x),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),
inference(nnf_transformation,[status(thm)],[f655]) ).
fof(f655_sk,plain,
! [V_xa,V_x,V_L] : ~ c_in(c_Pair(V_xa,V_x,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Arrow__Order__Mirabelle_Omkbot(V_L,V_x),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),
inference(skolemisation,[status(esa)],[f655_nnf]) ).
cnf(c655,plain,
~ c_in(c_Pair(X0,X1,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Arrow__Order__Mirabelle_Omkbot(X2,X1),tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt)),
inference(cnf_transformation,[status(esa)],[f655_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c5,c125,c130,c166,c265,c267,c268,c271,c278,c351,c428,c453,c478,c587,c592,c604,c621,c630,c638,c650,c651,c654,c655]) ).
cnf(g0_0,plain,
sF2 != false,
inference(rw,[status(thm)],[goal_0,t54]) ).
cnf(g0_1,plain,
sF2 != sF2,
inference(rw,[status(thm)],[g0_0,t173]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SCT074-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.36 % Computer : n003.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Thu Sep 24 08:43:06 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 14.25/2.24 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 14.25/2.24 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------