%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SCT007-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n006.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:49 PM UTC 2026
% Result : Unsatisfiable 27.22s 3.93s
% Output : Proof 27.22s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 16
% Syntax : Number of formulae : 79 ( 47 unt; 0 def)
% Number of atoms : 115 ( 35 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 122 ( 86 ~; 36 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 20 ( 20 usr; 5 con; 0-4 aty)
% Number of variables : 164 ( 24 sgn 72 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f568,axiom,
( ~ hBOOL(c_Order__Relation_Olinear__order__on(V_A,V_r,T_a))
| hBOOL(hAPP(c_Order__Relation_Ostrict__linear__order__on(V_A,T_a),c_HOL_Ominus__class_Ominus(V_r,c_Relation_OId(T_a),tc_fun(tc_prod(T_a,T_a),tc_bool)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_strict__linear__order__on__diff__Id_0) ).
fof(f568_nnf,plain,
! [V_A,T_a,V_r] :
( ~ hBOOL(c_Order__Relation_Olinear__order__on(V_A,V_r,T_a))
| hBOOL(hAPP(c_Order__Relation_Ostrict__linear__order__on(V_A,T_a),c_HOL_Ominus__class_Ominus(V_r,c_Relation_OId(T_a),tc_fun(tc_prod(T_a,T_a),tc_bool)))) ),
inference(nnf_transformation,[status(thm)],[f568]) ).
fof(f568_sk,plain,
! [V_A,T_a,V_r] :
( ~ hBOOL(c_Order__Relation_Olinear__order__on(V_A,V_r,T_a))
| hBOOL(hAPP(c_Order__Relation_Ostrict__linear__order__on(V_A,T_a),c_HOL_Ominus__class_Ominus(V_r,c_Relation_OId(T_a),tc_fun(tc_prod(T_a,T_a),tc_bool)))) ),
inference(skolemisation,[status(esa)],[f568_nnf]) ).
cnf(c568,plain,
( ~ hBOOL(c_Order__Relation_Olinear__order__on(X0,X2,X1))
| hBOOL(hAPP(c_Order__Relation_Ostrict__linear__order__on(X0,X1),c_HOL_Ominus__class_Ominus(X2,c_Relation_OId(X1),tc_fun(tc_prod(X1,X1),tc_bool)))) ),
inference(cnf_transformation,[status(esa)],[f568_sk]) ).
cnf(t134,plain,
ifeq(hBOOL(c_Order__Relation_Olinear__order__on(X1,X2,X3)),true,hBOOL(hAPP(c_Order__Relation_Ostrict__linear__order__on(X1,X3),c_HOL_Ominus__class_Ominus(X2,c_Relation_OId(X3),tc_fun(tc_prod(X3,X3),tc_bool)))),true) = true,
inference(equality_encoding,[status(esa)],[c568]) ).
cnf(t336,plain,
ifeq(hBOOL(c_Order__Relation_Olinear__order__on(X1,X2,X3)),true,hBOOL(hAPP(c_Order__Relation_Ostrict__linear__order__on(X1,X3),c_HOL_Ominus__class_Ominus(X2,c_Relation_OId(X3),tc_fun(tc_prod(X3,X3),tc_bool)))),true) = true,
inference(orient,[status(thm)],[t134]) ).
cnf(f540,axiom,
( ~ hBOOL(c_Order__Relation_Olinear__order__on(V_A,V_r,T_a))
| hBOOL(c_Order__Relation_Olinear__order__on(V_A,c_Relation_Oconverse(V_r,T_a,T_a),T_a)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_linear__order__on__converse_1) ).
fof(f540_nnf,plain,
! [V_A,V_r,T_a] :
( ~ hBOOL(c_Order__Relation_Olinear__order__on(V_A,V_r,T_a))
| hBOOL(c_Order__Relation_Olinear__order__on(V_A,c_Relation_Oconverse(V_r,T_a,T_a),T_a)) ),
inference(nnf_transformation,[status(thm)],[f540]) ).
fof(f540_sk,plain,
! [V_A,V_r,T_a] :
( ~ hBOOL(c_Order__Relation_Olinear__order__on(V_A,V_r,T_a))
| hBOOL(c_Order__Relation_Olinear__order__on(V_A,c_Relation_Oconverse(V_r,T_a,T_a),T_a)) ),
inference(skolemisation,[status(esa)],[f540_nnf]) ).
cnf(c540,plain,
( ~ hBOOL(c_Order__Relation_Olinear__order__on(X0,X1,X2))
| hBOOL(c_Order__Relation_Olinear__order__on(X0,c_Relation_Oconverse(X1,X2,X2),X2)) ),
inference(cnf_transformation,[status(esa)],[f540_sk]) ).
cnf(t85,plain,
ifeq(hBOOL(c_Order__Relation_Olinear__order__on(X1,X2,X3)),true,hBOOL(c_Order__Relation_Olinear__order__on(X1,c_Relation_Oconverse(X2,X3,X3),X3)),true) = true,
inference(equality_encoding,[status(esa)],[c540]) ).
cnf(t337,plain,
ifeq(hBOOL(c_Order__Relation_Olinear__order__on(X1,X2,X3)),true,hBOOL(c_Order__Relation_Olinear__order__on(X1,c_Relation_Oconverse(X2,X3,X3),X3)),true) = true,
inference(orient,[status(thm)],[t85]) ).
cnf(f569,negated_conjecture,
hBOOL(c_Order__Relation_Olinear__order__on(c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_bool)),v_r,tc_Arrow__Order__Mirabelle_Oalt)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f569_nnf,plain,
hBOOL(c_Order__Relation_Olinear__order__on(c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_bool)),v_r,tc_Arrow__Order__Mirabelle_Oalt)),
inference(nnf_transformation,[status(thm)],[f569]) ).
cnf(c569,plain,
hBOOL(c_Order__Relation_Olinear__order__on(c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_bool)),v_r,tc_Arrow__Order__Mirabelle_Oalt)),
inference(cnf_transformation,[status(esa)],[f569_nnf]) ).
cnf(t13,plain,
hBOOL(c_Order__Relation_Olinear__order__on(c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_bool)),v_r,tc_Arrow__Order__Mirabelle_Oalt)) = true,
inference(equality_encoding,[status(esa)],[c569]) ).
cnf(t572,plain,
hBOOL(c_Order__Relation_Olinear__order__on(c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_bool)),v_r,tc_Arrow__Order__Mirabelle_Oalt)) = true,
inference(orient,[status(thm)],[t13]) ).
cnf(t575,plain,
true = ifeq(true,true,hBOOL(c_Order__Relation_Olinear__order__on(c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_bool)),c_Relation_Oconverse(v_r,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_Arrow__Order__Mirabelle_Oalt)),true),
inference(cp,[status(thm)],[t337,t572]) ).
cnf(t0,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t183,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t0]) ).
cnf(t2504,plain,
true = hBOOL(c_Order__Relation_Olinear__order__on(c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_bool)),c_Relation_Oconverse(v_r,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_Arrow__Order__Mirabelle_Oalt)),
inference(step,[status(thm)],[t575,t183]) ).
cnf(t2457,plain,
hBOOL(c_Order__Relation_Olinear__order__on(c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_bool)),c_Relation_Oconverse(v_r,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_Arrow__Order__Mirabelle_Oalt)) = true,
inference(orient,[status(thm)],[t2504]) ).
cnf(t2461,plain,
true = ifeq(true,true,hBOOL(hAPP(c_Order__Relation_Ostrict__linear__order__on(c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_bool)),tc_Arrow__Order__Mirabelle_Oalt),c_HOL_Ominus__class_Ominus(c_Relation_Oconverse(v_r,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Relation_OId(tc_Arrow__Order__Mirabelle_Oalt),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))),true),
inference(cp,[status(thm)],[t336,t2457]) ).
cnf(t2505,plain,
true = hBOOL(hAPP(c_Order__Relation_Ostrict__linear__order__on(c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_bool)),tc_Arrow__Order__Mirabelle_Oalt),c_HOL_Ominus__class_Ominus(c_Relation_Oconverse(v_r,tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),c_Relation_OId(tc_Arrow__Order__Mirabelle_Oalt),tc_fun(tc_prod(tc_Arrow__Order__Mirabelle_Oalt,tc_Arrow__Order__Mirabelle_Oalt),tc_bool)))),
inference(step,[status(thm)],[t2461,t183]) ).
cnf(f571,negated_conjecture,
~ hBOOL(hAPP(c_Order__Relation_Ostrict__linear__order__on(c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_bool)),tc_Arrow__Order__Mirabelle_Oalt),V_x)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_2) ).
fof(f571_nnf,plain,
! [V_x] : ~ hBOOL(hAPP(c_Order__Relation_Ostrict__linear__order__on(c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_bool)),tc_Arrow__Order__Mirabelle_Oalt),V_x)),
inference(nnf_transformation,[status(thm)],[f571]) ).
fof(f571_sk,plain,
! [V_x] : ~ hBOOL(hAPP(c_Order__Relation_Ostrict__linear__order__on(c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_bool)),tc_Arrow__Order__Mirabelle_Oalt),V_x)),
inference(skolemisation,[status(esa)],[f571_nnf]) ).
cnf(c571,plain,
~ hBOOL(hAPP(c_Order__Relation_Ostrict__linear__order__on(c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_bool)),tc_Arrow__Order__Mirabelle_Oalt),X0)),
inference(cnf_transformation,[status(esa)],[f571_sk]) ).
cnf(t29,plain,
hBOOL(hAPP(c_Order__Relation_Ostrict__linear__order__on(c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_bool)),tc_Arrow__Order__Mirabelle_Oalt),X1)) = false,
inference(equality_encoding,[status(esa)],[c571]) ).
cnf(t1042,plain,
hBOOL(hAPP(c_Order__Relation_Ostrict__linear__order__on(c_Orderings_Otop__class_Otop(tc_fun(tc_Arrow__Order__Mirabelle_Oalt,tc_bool)),tc_Arrow__Order__Mirabelle_Oalt),X1)) = false,
inference(orient,[status(thm)],[t29]) ).
cnf(t2506,plain,
true = false,
inference(step,[status(thm)],[t2505,t1042]) ).
cnf(t2462,plain,
false = true,
inference(orient,[status(thm)],[t2506]) ).
cnf(f5,axiom,
( ~ hBOOL(c_in(V_c,c_HOL_Ouminus__class_Ouminus(V_A,tc_fun(T_a,tc_bool)),T_a))
| ~ hBOOL(c_in(V_c,V_A,T_a)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_ComplD_0) ).
fof(f5_nnf,plain,
! [V_c,V_A,T_a] :
( ~ hBOOL(c_in(V_c,c_HOL_Ouminus__class_Ouminus(V_A,tc_fun(T_a,tc_bool)),T_a))
| ~ hBOOL(c_in(V_c,V_A,T_a)) ),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [V_c,V_A,T_a] :
( ~ hBOOL(c_in(V_c,c_HOL_Ouminus__class_Ouminus(V_A,tc_fun(T_a,tc_bool)),T_a))
| ~ hBOOL(c_in(V_c,V_A,T_a)) ),
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c5,plain,
( ~ hBOOL(c_in(X0,c_HOL_Ouminus__class_Ouminus(X1,tc_fun(X2,tc_bool)),X2))
| ~ hBOOL(c_in(X0,X1,X2)) ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(f157,axiom,
( ~ hBOOL(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/sandbox/benchmark/theBenchmark.p',cls_bex__empty_0) ).
fof(f157_nnf,plain,
! [V_P,V_x,T_a] :
( ~ hBOOL(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)],[f157]) ).
fof(f157_sk,plain,
! [V_P,V_x,T_a] :
( ~ hBOOL(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)],[f157_nnf]) ).
cnf(c157,plain,
( ~ hBOOL(c_in(X1,c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)),X2))
| ~ hBOOL(hAPP(X0,X1)) ),
inference(cnf_transformation,[status(esa)],[f157_sk]) ).
cnf(f209,axiom,
~ hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),V_x)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_bot1E_0) ).
fof(f209_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)],[f209]) ).
fof(f209_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)],[f209_nnf]) ).
cnf(c209,plain,
~ hBOOL(hAPP(c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),X1)),
inference(cnf_transformation,[status(esa)],[f209_sk]) ).
cnf(f210,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))
| ~ hBOOL(c_in(V_x,V_A,T_a))
| ~ hBOOL(c_in(V_x,V_B,T_a)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_disjoint__iff__not__equal_0) ).
fof(f210_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))
| ~ hBOOL(c_in(V_x,V_A,T_a))
| ~ hBOOL(c_in(V_x,V_B,T_a)) ),
inference(nnf_transformation,[status(thm)],[f210]) ).
fof(f210_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))
| ~ hBOOL(c_in(V_x,V_A,T_a))
| ~ hBOOL(c_in(V_x,V_B,T_a)) ),
inference(skolemisation,[status(esa)],[f210_nnf]) ).
cnf(c210,plain,
( c_Lattices_Olower__semilattice__class_Oinf(X3,X1,tc_fun(X2,tc_bool)) != c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool))
| ~ hBOOL(c_in(X0,X3,X2))
| ~ hBOOL(c_in(X0,X1,X2)) ),
inference(cnf_transformation,[status(esa)],[f210_sk]) ).
cnf(f221,axiom,
( ~ hBOOL(hAPP(V_P,V_x))
| c_Collect(V_P,T_a) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Collect__empty__eq_0) ).
fof(f221_nnf,plain,
! [V_P,T_a,V_x] :
( ~ hBOOL(hAPP(V_P,V_x))
| c_Collect(V_P,T_a) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) ),
inference(nnf_transformation,[status(thm)],[f221]) ).
fof(f221_sk,plain,
! [V_P,T_a,V_x] :
( ~ hBOOL(hAPP(V_P,V_x))
| c_Collect(V_P,T_a) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) ),
inference(skolemisation,[status(esa)],[f221_nnf]) ).
cnf(c221,plain,
( ~ hBOOL(hAPP(X0,X2))
| c_Collect(X0,X1) != c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)) ),
inference(cnf_transformation,[status(esa)],[f221_sk]) ).
cnf(f253,axiom,
~ hBOOL(c_in(V_a,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_emptyE_0) ).
fof(f253_nnf,plain,
! [V_a,T_a] : ~ hBOOL(c_in(V_a,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)),
inference(nnf_transformation,[status(thm)],[f253]) ).
fof(f253_sk,plain,
! [V_a,T_a] : ~ hBOOL(c_in(V_a,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)),
inference(skolemisation,[status(esa)],[f253_nnf]) ).
cnf(c253,plain,
~ hBOOL(c_in(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1)),
inference(cnf_transformation,[status(esa)],[f253_sk]) ).
cnf(f254,axiom,
~ hBOOL(c_in(V_c,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_empty__iff_0) ).
fof(f254_nnf,plain,
! [V_c,T_a] : ~ hBOOL(c_in(V_c,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)),
inference(nnf_transformation,[status(thm)],[f254]) ).
fof(f254_sk,plain,
! [V_c,T_a] : ~ hBOOL(c_in(V_c,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)),
inference(skolemisation,[status(esa)],[f254_nnf]) ).
cnf(c254,plain,
~ hBOOL(c_in(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1)),
inference(cnf_transformation,[status(esa)],[f254_sk]) ).
cnf(f256,axiom,
~ hBOOL(c_in(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_ex__in__conv_0) ).
fof(f256_nnf,plain,
! [V_x,T_a] : ~ hBOOL(c_in(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)),
inference(nnf_transformation,[status(thm)],[f256]) ).
fof(f256_sk,plain,
! [V_x,T_a] : ~ hBOOL(c_in(V_x,c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),T_a)),
inference(skolemisation,[status(esa)],[f256_nnf]) ).
cnf(c256,plain,
~ hBOOL(c_in(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1)),
inference(cnf_transformation,[status(esa)],[f256_sk]) ).
cnf(f380,axiom,
( ~ hBOOL(hAPP(V_P,V_x))
| c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) != c_Collect(V_P,T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_empty__Collect__eq_0) ).
fof(f380_nnf,plain,
! [T_a,V_P,V_x] :
( ~ hBOOL(hAPP(V_P,V_x))
| c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) != c_Collect(V_P,T_a) ),
inference(nnf_transformation,[status(thm)],[f380]) ).
fof(f380_sk,plain,
! [T_a,V_P,V_x] :
( ~ hBOOL(hAPP(V_P,V_x))
| c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)) != c_Collect(V_P,T_a) ),
inference(skolemisation,[status(esa)],[f380_nnf]) ).
cnf(c380,plain,
( ~ hBOOL(hAPP(X1,X2))
| c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)) != c_Collect(X1,X0) ),
inference(cnf_transformation,[status(esa)],[f380_sk]) ).
cnf(f477,axiom,
c_Orderings_Otop__class_Otop(tc_fun(T_a,tc_bool)) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_UNIV__not__empty_0) ).
fof(f477_nnf,plain,
! [T_a] : c_Orderings_Otop__class_Otop(tc_fun(T_a,tc_bool)) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),
inference(nnf_transformation,[status(thm)],[f477]) ).
fof(f477_sk,plain,
! [T_a] : c_Orderings_Otop__class_Otop(tc_fun(T_a,tc_bool)) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_bool)),
inference(skolemisation,[status(esa)],[f477_nnf]) ).
cnf(c477,plain,
c_Orderings_Otop__class_Otop(tc_fun(X0,tc_bool)) != c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)),
inference(cnf_transformation,[status(esa)],[f477_sk]) ).
cnf(f496,axiom,
( ~ hBOOL(c_in(V_c,c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),T_a))
| ~ hBOOL(c_in(V_c,V_B,T_a)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_DiffE_1) ).
fof(f496_nnf,plain,
! [V_c,V_B,T_a,V_A] :
( ~ hBOOL(c_in(V_c,c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),T_a))
| ~ hBOOL(c_in(V_c,V_B,T_a)) ),
inference(nnf_transformation,[status(thm)],[f496]) ).
fof(f496_sk,plain,
! [V_c,V_B,T_a,V_A] :
( ~ hBOOL(c_in(V_c,c_HOL_Ominus__class_Ominus(V_A,V_B,tc_fun(T_a,tc_bool)),T_a))
| ~ hBOOL(c_in(V_c,V_B,T_a)) ),
inference(skolemisation,[status(esa)],[f496_nnf]) ).
cnf(c496,plain,
( ~ hBOOL(c_in(X0,c_HOL_Ominus__class_Ominus(X3,X1,tc_fun(X2,tc_bool)),X2))
| ~ hBOOL(c_in(X0,X1,X2)) ),
inference(cnf_transformation,[status(esa)],[f496_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c5,c157,c209,c210,c221,c253,c254,c256,c380,c477,c496,c571]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t2462]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SCT007-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.08/0.36 % Computer : n006.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Thu Sep 24 08:31:41 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 27.22/3.93 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 27.22/3.93 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------