%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SET837-2 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n020.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:44:05 PM UTC 2026
% Result : Unsatisfiable 96.63s 67.60s
% Output : Proof 0.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 39
% Number of leaves : 13
% Syntax : Number of formulae : 154 ( 26 unt; 0 def)
% Number of atoms : 350 ( 70 equ)
% Maximal formula atoms : 4 ( 2 avg)
% Number of connectives : 307 ( 111 ~; 196 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-3 aty)
% Number of functors : 8 ( 8 usr; 5 con; 0-3 aty)
% Number of variables : 212 ( 17 sgn 52 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f8,axiom,
( c_in(V_c,V_A,T_a)
| c_in(V_c,V_B,T_a)
| ~ c_in(V_c,c_union(V_A,V_B,T_a),T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Set_OUnE_0) ).
fof(f8_nnf,plain,
! [V_c,V_A,V_B,T_a] :
( c_in(V_c,V_A,T_a)
| c_in(V_c,V_B,T_a)
| ~ c_in(V_c,c_union(V_A,V_B,T_a),T_a) ),
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
! [V_c,V_A,V_B,T_a] :
( c_in(V_c,V_A,T_a)
| c_in(V_c,V_B,T_a)
| ~ c_in(V_c,c_union(V_A,V_B,T_a),T_a) ),
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c8,plain,
( c_in(X0,X1,X3)
| c_in(X0,X2,X3)
| ~ c_in(X0,c_union(X1,X2,X3),X3) ),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(f10,axiom,
( c_lessequals(V_A,V_B,tc_set(T_a))
| c_in(c_Main_OsubsetI__1(V_A,V_B,T_a),V_A,T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Set_OsubsetI_0) ).
fof(f10_nnf,plain,
! [V_A,V_B,T_a] :
( c_lessequals(V_A,V_B,tc_set(T_a))
| c_in(c_Main_OsubsetI__1(V_A,V_B,T_a),V_A,T_a) ),
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
! [V_A,V_B,T_a] :
( c_lessequals(V_A,V_B,tc_set(T_a))
| c_in(c_Main_OsubsetI__1(V_A,V_B,T_a),V_A,T_a) ),
inference(skolemisation,[status(esa)],[f10_nnf]) ).
cnf(c10,plain,
( c_lessequals(X0,X1,tc_set(X2))
| c_in(c_Main_OsubsetI__1(X0,X1,X2),X0,X2) ),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(p18,plain,
( c_lessequals(c_union(X0,X1,X2),X3,tc_set(X2))
| c_in(c_Main_OsubsetI__1(c_union(X0,X1,X2),X3,X2),X0,X2)
| c_in(c_Main_OsubsetI__1(c_union(X0,X1,X2),X3,X2),X1,X2) ),
inference(resolution,[status(thm)],[c8,c10]) ).
cnf(f9,axiom,
( c_in(V_c,V_B,T_a)
| ~ c_lessequals(V_A,V_B,tc_set(T_a))
| ~ c_in(V_c,V_A,T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Set_OsubsetD_0) ).
fof(f9_nnf,plain,
! [V_c,V_A,T_a,V_B] :
( c_in(V_c,V_B,T_a)
| ~ c_lessequals(V_A,V_B,tc_set(T_a))
| ~ c_in(V_c,V_A,T_a) ),
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
! [V_c,V_A,T_a,V_B] :
( c_in(V_c,V_B,T_a)
| ~ c_lessequals(V_A,V_B,tc_set(T_a))
| ~ c_in(V_c,V_A,T_a) ),
inference(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c9,plain,
( c_in(X0,X3,X2)
| ~ c_lessequals(X1,X3,tc_set(X2))
| ~ c_in(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(p110,plain,
( c_in(c_Main_OsubsetI__1(c_union(X0,X1,X2),X3,X2),X4,X2)
| ~ c_lessequals(X1,X4,tc_set(X2))
| c_lessequals(c_union(X0,X1,X2),X3,tc_set(X2))
| c_in(c_Main_OsubsetI__1(c_union(X0,X1,X2),X3,X2),X0,X2) ),
inference(resolution,[status(thm)],[p18,c9]) ).
cnf(f1,negated_conjecture,
( c_lessequals(v_Z,v_X,tc_set(t_a))
| v_X = c_union(v_Y,v_Z,t_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_1) ).
fof(f1_nnf,plain,
( c_lessequals(v_Z,v_X,tc_set(t_a))
| v_X = c_union(v_Y,v_Z,t_a) ),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
( c_lessequals(v_Z,v_X,tc_set(t_a))
| v_X = c_union(v_Y,v_Z,t_a) ),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
( c_lessequals(v_Z,v_X,tc_set(t_a))
| v_X = c_union(v_Y,v_Z,t_a) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(f6,axiom,
( c_in(V_c,c_union(V_A,V_B,T_a),T_a)
| ~ c_in(V_c,V_B,T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Set_OUnCI_0) ).
fof(f6_nnf,plain,
! [V_c,V_B,T_a,V_A] :
( c_in(V_c,c_union(V_A,V_B,T_a),T_a)
| ~ c_in(V_c,V_B,T_a) ),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [V_c,V_B,T_a,V_A] :
( c_in(V_c,c_union(V_A,V_B,T_a),T_a)
| ~ c_in(V_c,V_B,T_a) ),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c6,plain,
( c_in(X0,c_union(X3,X1,X2),X2)
| ~ c_in(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(p13,plain,
( c_in(c_Main_OsubsetI__1(X0,X1,X2),c_union(X3,X0,X2),X2)
| c_lessequals(X0,X1,tc_set(X2)) ),
inference(resolution,[status(thm)],[c10,c6]) ).
cnf(p68,plain,
( c_in(c_Main_OsubsetI__1(v_Z,X0,t_a),v_X,t_a)
| c_lessequals(v_Z,X0,tc_set(t_a))
| c_lessequals(v_Z,v_X,tc_set(t_a)) ),
inference(superposition,[status(thm)],[c1,p13]) ).
cnf(p85,plain,
( c_in(c_Main_OsubsetI__1(v_Z,v_X,t_a),v_X,t_a)
| c_lessequals(v_Z,v_X,tc_set(t_a)) ),
inference(factoring,[status(thm)],[p68]) ).
cnf(f11,axiom,
( c_lessequals(V_A,V_B,tc_set(T_a))
| ~ c_in(c_Main_OsubsetI__1(V_A,V_B,T_a),V_B,T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Set_OsubsetI_1) ).
fof(f11_nnf,plain,
! [V_A,V_B,T_a] :
( c_lessequals(V_A,V_B,tc_set(T_a))
| ~ c_in(c_Main_OsubsetI__1(V_A,V_B,T_a),V_B,T_a) ),
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
! [V_A,V_B,T_a] :
( c_lessequals(V_A,V_B,tc_set(T_a))
| ~ c_in(c_Main_OsubsetI__1(V_A,V_B,T_a),V_B,T_a) ),
inference(skolemisation,[status(esa)],[f11_nnf]) ).
cnf(c11,plain,
( c_lessequals(X0,X1,tc_set(X2))
| ~ c_in(c_Main_OsubsetI__1(X0,X1,X2),X1,X2) ),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(p93,plain,
( c_lessequals(v_Z,v_X,tc_set(t_a))
| c_lessequals(v_Z,v_X,tc_set(t_a)) ),
inference(resolution,[status(thm)],[p85,c11]) ).
cnf(p94,plain,
c_lessequals(v_Z,v_X,tc_set(t_a)),
inference(factoring,[status(thm)],[p93]) ).
cnf(p381,plain,
( c_in(c_Main_OsubsetI__1(c_union(X0,v_Z,t_a),X1,t_a),v_X,t_a)
| c_lessequals(c_union(X0,v_Z,t_a),X1,tc_set(t_a))
| c_in(c_Main_OsubsetI__1(c_union(X0,v_Z,t_a),X1,t_a),X0,t_a) ),
inference(resolution,[status(thm)],[p110,p94]) ).
cnf(p1668,plain,
( c_lessequals(c_union(v_X,v_Z,t_a),X0,tc_set(t_a))
| c_in(c_Main_OsubsetI__1(c_union(v_X,v_Z,t_a),X0,t_a),v_X,t_a) ),
inference(factoring,[status(thm)],[p381]) ).
cnf(p1679,plain,
( c_lessequals(c_union(v_X,v_Z,t_a),v_X,tc_set(t_a))
| c_lessequals(c_union(v_X,v_Z,t_a),v_X,tc_set(t_a)) ),
inference(resolution,[status(thm)],[p1668,c11]) ).
cnf(p1680,plain,
c_lessequals(c_union(v_X,v_Z,t_a),v_X,tc_set(t_a)),
inference(factoring,[status(thm)],[p1679]) ).
cnf(f12,axiom,
( V_A = V_B
| ~ c_lessequals(V_A,V_B,tc_set(T_a))
| ~ c_lessequals(V_B,V_A,tc_set(T_a)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Set_Osubset__antisym_0) ).
fof(f12_nnf,plain,
! [V_B,V_A,T_a] :
( V_A = V_B
| ~ c_lessequals(V_A,V_B,tc_set(T_a))
| ~ c_lessequals(V_B,V_A,tc_set(T_a)) ),
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
! [V_B,V_A,T_a] :
( V_A = V_B
| ~ c_lessequals(V_A,V_B,tc_set(T_a))
| ~ c_lessequals(V_B,V_A,tc_set(T_a)) ),
inference(skolemisation,[status(esa)],[f12_nnf]) ).
cnf(c12,plain,
( X1 = X0
| ~ c_lessequals(X1,X0,tc_set(X2))
| ~ c_lessequals(X0,X1,tc_set(X2)) ),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(p1690,plain,
( v_X = c_union(v_X,v_Z,t_a)
| ~ c_lessequals(v_X,c_union(v_X,v_Z,t_a),tc_set(t_a)) ),
inference(resolution,[status(thm)],[p1680,c12]) ).
cnf(f7,axiom,
( c_in(V_c,c_union(V_A,V_B,T_a),T_a)
| ~ c_in(V_c,V_A,T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Set_OUnCI_1) ).
fof(f7_nnf,plain,
! [V_c,V_A,T_a,V_B] :
( c_in(V_c,c_union(V_A,V_B,T_a),T_a)
| ~ c_in(V_c,V_A,T_a) ),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [V_c,V_A,T_a,V_B] :
( c_in(V_c,c_union(V_A,V_B,T_a),T_a)
| ~ c_in(V_c,V_A,T_a) ),
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c7,plain,
( c_in(X0,c_union(X1,X3,X2),X2)
| ~ c_in(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(p14,plain,
( c_in(c_Main_OsubsetI__1(X0,X1,X2),c_union(X0,X3,X2),X2)
| c_lessequals(X0,X1,tc_set(X2)) ),
inference(resolution,[status(thm)],[c10,c7]) ).
cnf(p84,plain,
( c_lessequals(X0,c_union(X0,X1,X2),tc_set(X2))
| c_lessequals(X0,c_union(X0,X1,X2),tc_set(X2)) ),
inference(resolution,[status(thm)],[p14,c11]) ).
cnf(p219,plain,
c_lessequals(X0,c_union(X0,X1,X2),tc_set(X2)),
inference(factoring,[status(thm)],[p84]) ).
cnf(p1697,plain,
v_X = c_union(v_X,v_Z,t_a),
inference(resolution,[status(thm)],[p1690,p219]) ).
cnf(p1676,plain,
( c_in(c_Main_OsubsetI__1(c_union(v_X,v_Z,t_a),X0,t_a),c_union(X1,v_X,t_a),t_a)
| c_lessequals(c_union(v_X,v_Z,t_a),X0,tc_set(t_a)) ),
inference(resolution,[status(thm)],[p1668,c6]) ).
cnf(p2856,plain,
( c_lessequals(c_union(v_X,v_Z,t_a),c_union(X0,v_X,t_a),tc_set(t_a))
| c_lessequals(c_union(v_X,v_Z,t_a),c_union(X0,v_X,t_a),tc_set(t_a)) ),
inference(resolution,[status(thm)],[p1676,c11]) ).
cnf(p10414,plain,
c_lessequals(c_union(v_X,v_Z,t_a),c_union(X0,v_X,t_a),tc_set(t_a)),
inference(factoring,[status(thm)],[p2856]) ).
cnf(p10415,plain,
( c_union(X0,v_X,t_a) = c_union(v_X,v_Z,t_a)
| ~ c_lessequals(c_union(X0,v_X,t_a),c_union(v_X,v_Z,t_a),tc_set(t_a)) ),
inference(resolution,[status(thm)],[p10414,c12]) ).
cnf(p10457,plain,
( c_union(X0,v_X,t_a) = c_union(v_X,v_Z,t_a)
| ~ c_lessequals(c_union(X0,v_X,t_a),v_X,tc_set(t_a)) ),
inference(superposition,[status(thm)],[p1697,p10415]) ).
cnf(p111,plain,
( c_in(c_Main_OsubsetI__1(c_union(X0,X1,X2),X3,X2),X4,X2)
| ~ c_lessequals(X0,X4,tc_set(X2))
| c_lessequals(c_union(X0,X1,X2),X3,tc_set(X2))
| c_in(c_Main_OsubsetI__1(c_union(X0,X1,X2),X3,X2),X1,X2) ),
inference(resolution,[status(thm)],[p18,c9]) ).
cnf(p397,plain,
( ~ c_lessequals(X0,X1,tc_set(X2))
| c_lessequals(c_union(X0,X1,X2),X3,tc_set(X2))
| c_in(c_Main_OsubsetI__1(c_union(X0,X1,X2),X3,X2),X1,X2) ),
inference(factoring,[status(thm)],[p111]) ).
cnf(p5031,plain,
( c_lessequals(c_union(v_Z,v_X,t_a),X0,tc_set(t_a))
| c_in(c_Main_OsubsetI__1(c_union(v_Z,v_X,t_a),X0,t_a),v_X,t_a) ),
inference(resolution,[status(thm)],[p397,p94]) ).
cnf(p5098,plain,
( c_lessequals(c_union(v_Z,v_X,t_a),v_X,tc_set(t_a))
| c_lessequals(c_union(v_Z,v_X,t_a),v_X,tc_set(t_a)) ),
inference(resolution,[status(thm)],[p5031,c11]) ).
cnf(p5099,plain,
c_lessequals(c_union(v_Z,v_X,t_a),v_X,tc_set(t_a)),
inference(factoring,[status(thm)],[p5098]) ).
cnf(p10463,plain,
c_union(v_Z,v_X,t_a) = c_union(v_X,v_Z,t_a),
inference(resolution,[status(thm)],[p10457,p5099]) ).
cnf(p10631,plain,
c_union(v_X,v_Z,t_a) = v_X,
inference(superposition,[status(thm)],[p1697,p10463]) ).
cnf(p102,plain,
( c_in(c_Main_OsubsetI__1(c_union(X0,X1,X2),X3,X2),c_union(X4,X1,X2),X2)
| c_lessequals(c_union(X0,X1,X2),X3,tc_set(X2))
| c_in(c_Main_OsubsetI__1(c_union(X0,X1,X2),X3,X2),X0,X2) ),
inference(resolution,[status(thm)],[p18,c6]) ).
cnf(p264,plain,
( c_in(c_Main_OsubsetI__1(c_union(X0,X1,X2),X3,X2),X5,X2)
| ~ c_lessequals(X0,X5,tc_set(X2))
| c_in(c_Main_OsubsetI__1(c_union(X0,X1,X2),X3,X2),c_union(X4,X1,X2),X2)
| c_lessequals(c_union(X0,X1,X2),X3,tc_set(X2)) ),
inference(resolution,[status(thm)],[p102,c9]) ).
cnf(p1059,plain,
( ~ c_lessequals(X0,c_union(X4,X1,X2),tc_set(X2))
| c_in(c_Main_OsubsetI__1(c_union(X0,X1,X2),X3,X2),c_union(X4,X1,X2),X2)
| c_lessequals(c_union(X0,X1,X2),X3,tc_set(X2)) ),
inference(factoring,[status(thm)],[p264]) ).
cnf(p25,plain,
( c_lessequals(X0,X3,tc_set(X2))
| c_in(c_Main_OsubsetI__1(X0,X3,X2),X1,X2)
| ~ c_lessequals(X0,X1,tc_set(X2)) ),
inference(resolution,[status(thm)],[c9,c10]) ).
cnf(f0,negated_conjecture,
( c_lessequals(v_Y,v_X,tc_set(t_a))
| v_X = c_union(v_Y,v_Z,t_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f0_nnf,plain,
( c_lessequals(v_Y,v_X,tc_set(t_a))
| v_X = c_union(v_Y,v_Z,t_a) ),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
( c_lessequals(v_Y,v_X,tc_set(t_a))
| v_X = c_union(v_Y,v_Z,t_a) ),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
( c_lessequals(v_Y,v_X,tc_set(t_a))
| v_X = c_union(v_Y,v_Z,t_a) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p79,plain,
( c_in(c_Main_OsubsetI__1(v_Y,X0,t_a),v_X,t_a)
| c_lessequals(v_Y,X0,tc_set(t_a))
| c_lessequals(v_Y,v_X,tc_set(t_a)) ),
inference(superposition,[status(thm)],[c0,p14]) ).
cnf(p116,plain,
( c_in(c_Main_OsubsetI__1(v_Y,v_X,t_a),v_X,t_a)
| c_lessequals(v_Y,v_X,tc_set(t_a)) ),
inference(factoring,[status(thm)],[p79]) ).
cnf(p124,plain,
( c_lessequals(v_Y,v_X,tc_set(t_a))
| c_lessequals(v_Y,v_X,tc_set(t_a)) ),
inference(resolution,[status(thm)],[p116,c11]) ).
cnf(p125,plain,
c_lessequals(v_Y,v_X,tc_set(t_a)),
inference(factoring,[status(thm)],[p124]) ).
cnf(p131,plain,
( c_lessequals(v_Y,X0,tc_set(t_a))
| c_in(c_Main_OsubsetI__1(v_Y,X0,t_a),v_X,t_a) ),
inference(resolution,[status(thm)],[p25,p125]) ).
cnf(p142,plain,
( c_in(c_Main_OsubsetI__1(v_Y,X0,t_a),c_union(v_X,X1,t_a),t_a)
| c_lessequals(v_Y,X0,tc_set(t_a)) ),
inference(resolution,[status(thm)],[p131,c7]) ).
cnf(p163,plain,
( c_lessequals(v_Y,c_union(v_X,X0,t_a),tc_set(t_a))
| c_lessequals(v_Y,c_union(v_X,X0,t_a),tc_set(t_a)) ),
inference(resolution,[status(thm)],[p142,c11]) ).
cnf(p176,plain,
c_lessequals(v_Y,c_union(v_X,X0,t_a),tc_set(t_a)),
inference(factoring,[status(thm)],[p163]) ).
cnf(p29038,plain,
( c_in(c_Main_OsubsetI__1(c_union(v_Y,X0,t_a),X1,t_a),c_union(v_X,X0,t_a),t_a)
| c_lessequals(c_union(v_Y,X0,t_a),X1,tc_set(t_a)) ),
inference(resolution,[status(thm)],[p1059,p176]) ).
cnf(p29771,plain,
( c_in(c_Main_OsubsetI__1(c_union(v_Y,v_Z,t_a),X0,t_a),v_X,t_a)
| c_lessequals(c_union(v_Y,v_Z,t_a),X0,tc_set(t_a)) ),
inference(superposition,[status(thm)],[p10631,p29038]) ).
cnf(p29775,plain,
( c_lessequals(c_union(v_Y,v_Z,t_a),v_X,tc_set(t_a))
| c_lessequals(c_union(v_Y,v_Z,t_a),v_X,tc_set(t_a)) ),
inference(resolution,[status(thm)],[p29771,c11]) ).
cnf(p29776,plain,
c_lessequals(c_union(v_Y,v_Z,t_a),v_X,tc_set(t_a)),
inference(factoring,[status(thm)],[p29775]) ).
cnf(p72,plain,
( c_lessequals(X0,c_union(X1,X0,X2),tc_set(X2))
| c_lessequals(X0,c_union(X1,X0,X2),tc_set(X2)) ),
inference(resolution,[status(thm)],[p13,c11]) ).
cnf(p177,plain,
c_lessequals(X0,c_union(X1,X0,X2),tc_set(X2)),
inference(factoring,[status(thm)],[p72]) ).
cnf(f5,negated_conjecture,
( ~ c_lessequals(v_Y,V_U,tc_set(t_a))
| ~ c_lessequals(v_Z,V_U,tc_set(t_a))
| c_lessequals(v_X,V_U,tc_set(t_a))
| v_X = c_union(v_Y,v_Z,t_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_5) ).
fof(f5_nnf,plain,
! [V_U] :
( ~ c_lessequals(v_Y,V_U,tc_set(t_a))
| ~ c_lessequals(v_Z,V_U,tc_set(t_a))
| c_lessequals(v_X,V_U,tc_set(t_a))
| v_X = c_union(v_Y,v_Z,t_a) ),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [V_U] :
( ~ c_lessequals(v_Y,V_U,tc_set(t_a))
| ~ c_lessequals(v_Z,V_U,tc_set(t_a))
| c_lessequals(v_X,V_U,tc_set(t_a))
| v_X = c_union(v_Y,v_Z,t_a) ),
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c5,plain,
( ~ c_lessequals(v_Y,X0,tc_set(t_a))
| ~ c_lessequals(v_Z,X0,tc_set(t_a))
| c_lessequals(v_X,X0,tc_set(t_a))
| v_X = c_union(v_Y,v_Z,t_a) ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p583,plain,
( ~ c_lessequals(v_Y,c_union(X0,v_Z,t_a),tc_set(t_a))
| c_lessequals(v_X,c_union(X0,v_Z,t_a),tc_set(t_a))
| v_X = c_union(v_Y,v_Z,t_a) ),
inference(resolution,[status(thm)],[p177,c5]) ).
cnf(p723,plain,
( c_lessequals(v_X,c_union(v_Y,v_Z,t_a),tc_set(t_a))
| v_X = c_union(v_Y,v_Z,t_a) ),
inference(resolution,[status(thm)],[p219,p583]) ).
cnf(p724,plain,
( c_union(v_Y,v_Z,t_a) = v_X
| ~ c_lessequals(c_union(v_Y,v_Z,t_a),v_X,tc_set(t_a))
| v_X = c_union(v_Y,v_Z,t_a) ),
inference(resolution,[status(thm)],[p723,c12]) ).
cnf(p29784,plain,
( c_union(v_Y,v_Z,t_a) = v_X
| v_X = c_union(v_Y,v_Z,t_a) ),
inference(resolution,[status(thm)],[p29776,p724]) ).
cnf(p722,plain,
( c_union(X0,X1,X2) = X0
| ~ c_lessequals(c_union(X0,X1,X2),X0,tc_set(X2)) ),
inference(resolution,[status(thm)],[p219,c12]) ).
cnf(p380,plain,
( ~ c_lessequals(X1,X0,tc_set(X2))
| c_lessequals(c_union(X0,X1,X2),X3,tc_set(X2))
| c_in(c_Main_OsubsetI__1(c_union(X0,X1,X2),X3,X2),X0,X2) ),
inference(factoring,[status(thm)],[p110]) ).
cnf(p3641,plain,
( c_lessequals(c_union(v_X,v_Y,t_a),X0,tc_set(t_a))
| c_in(c_Main_OsubsetI__1(c_union(v_X,v_Y,t_a),X0,t_a),v_X,t_a) ),
inference(resolution,[status(thm)],[p380,p125]) ).
cnf(p3706,plain,
( c_lessequals(c_union(v_X,v_Y,t_a),v_X,tc_set(t_a))
| c_lessequals(c_union(v_X,v_Y,t_a),v_X,tc_set(t_a)) ),
inference(resolution,[status(thm)],[p3641,c11]) ).
cnf(p3707,plain,
c_lessequals(c_union(v_X,v_Y,t_a),v_X,tc_set(t_a)),
inference(factoring,[status(thm)],[p3706]) ).
cnf(p19582,plain,
c_union(v_X,v_Y,t_a) = v_X,
inference(resolution,[status(thm)],[p722,p3707]) ).
cnf(p130,plain,
( c_lessequals(v_Z,X0,tc_set(t_a))
| c_in(c_Main_OsubsetI__1(v_Z,X0,t_a),v_X,t_a) ),
inference(resolution,[status(thm)],[p25,p94]) ).
cnf(p139,plain,
( c_in(c_Main_OsubsetI__1(v_Z,X0,t_a),c_union(v_X,X1,t_a),t_a)
| c_lessequals(v_Z,X0,tc_set(t_a)) ),
inference(resolution,[status(thm)],[p130,c7]) ).
cnf(p151,plain,
( c_lessequals(v_Z,c_union(v_X,X0,t_a),tc_set(t_a))
| c_lessequals(v_Z,c_union(v_X,X0,t_a),tc_set(t_a)) ),
inference(resolution,[status(thm)],[p139,c11]) ).
cnf(p171,plain,
c_lessequals(v_Z,c_union(v_X,X0,t_a),tc_set(t_a)),
inference(factoring,[status(thm)],[p151]) ).
cnf(p29037,plain,
( c_in(c_Main_OsubsetI__1(c_union(v_Z,X0,t_a),X1,t_a),c_union(v_X,X0,t_a),t_a)
| c_lessequals(c_union(v_Z,X0,t_a),X1,tc_set(t_a)) ),
inference(resolution,[status(thm)],[p1059,p171]) ).
cnf(p29209,plain,
( c_in(c_Main_OsubsetI__1(c_union(v_Z,v_Y,t_a),X0,t_a),v_X,t_a)
| c_lessequals(c_union(v_Z,v_Y,t_a),X0,tc_set(t_a)) ),
inference(superposition,[status(thm)],[p19582,p29037]) ).
cnf(p29213,plain,
( c_lessequals(c_union(v_Z,v_Y,t_a),v_X,tc_set(t_a))
| c_lessequals(c_union(v_Z,v_Y,t_a),v_X,tc_set(t_a)) ),
inference(resolution,[status(thm)],[p29209,c11]) ).
cnf(p29214,plain,
c_lessequals(c_union(v_Z,v_Y,t_a),v_X,tc_set(t_a)),
inference(factoring,[status(thm)],[p29213]) ).
cnf(p721,plain,
( ~ c_lessequals(v_Y,c_union(v_Z,X0,t_a),tc_set(t_a))
| c_lessequals(v_X,c_union(v_Z,X0,t_a),tc_set(t_a))
| v_X = c_union(v_Y,v_Z,t_a) ),
inference(resolution,[status(thm)],[p219,c5]) ).
cnf(p732,plain,
( c_lessequals(v_X,c_union(v_Z,v_Y,t_a),tc_set(t_a))
| v_X = c_union(v_Y,v_Z,t_a) ),
inference(resolution,[status(thm)],[p721,p177]) ).
cnf(p738,plain,
( c_union(v_Z,v_Y,t_a) = v_X
| ~ c_lessequals(c_union(v_Z,v_Y,t_a),v_X,tc_set(t_a))
| v_X = c_union(v_Y,v_Z,t_a) ),
inference(resolution,[status(thm)],[p732,c12]) ).
cnf(p29218,plain,
( c_union(v_Z,v_Y,t_a) = v_X
| v_X = c_union(v_Y,v_Z,t_a) ),
inference(resolution,[status(thm)],[p29214,p738]) ).
cnf(p29215,plain,
( v_X = c_union(v_Z,v_Y,t_a)
| ~ c_lessequals(v_X,c_union(v_Z,v_Y,t_a),tc_set(t_a)) ),
inference(resolution,[status(thm)],[p29214,c12]) ).
cnf(p29472,plain,
( v_X = c_union(v_Y,v_Z,t_a)
| v_X = c_union(v_Z,v_Y,t_a) ),
inference(resolution,[status(thm)],[p29215,p732]) ).
cnf(p29479,plain,
( c_union(v_Y,v_Z,t_a) != c_union(v_Z,v_Y,t_a)
| v_X = c_union(v_Y,v_Z,t_a) ),
inference(equality_factoring,[status(thm)],[p29472]) ).
cnf(p29491,plain,
( c_union(v_Y,v_Z,t_a) != v_X
| v_X = c_union(v_Y,v_Z,t_a)
| v_X = c_union(v_Y,v_Z,t_a) ),
inference(superposition,[status(thm)],[p29218,p29479]) ).
cnf(p29548,plain,
( c_union(v_Y,v_Z,t_a) != v_X
| v_X = c_union(v_Y,v_Z,t_a) ),
inference(factoring,[status(thm)],[p29491]) ).
cnf(p30038,plain,
( v_X = c_union(v_Y,v_Z,t_a)
| v_X = c_union(v_Y,v_Z,t_a) ),
inference(resolution,[status(thm)],[p29784,p29548]) ).
cnf(p30046,plain,
v_X = c_union(v_Y,v_Z,t_a),
inference(factoring,[status(thm)],[p30038]) ).
cnf(f2,negated_conjecture,
( v_X != c_union(v_Y,v_Z,t_a)
| ~ c_lessequals(v_Y,v_X,tc_set(t_a))
| ~ c_lessequals(v_Z,v_X,tc_set(t_a))
| c_lessequals(v_Y,v_x,tc_set(t_a)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_2) ).
fof(f2_nnf,plain,
( v_X != c_union(v_Y,v_Z,t_a)
| ~ c_lessequals(v_Y,v_X,tc_set(t_a))
| ~ c_lessequals(v_Z,v_X,tc_set(t_a))
| c_lessequals(v_Y,v_x,tc_set(t_a)) ),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
( v_X != c_union(v_Y,v_Z,t_a)
| ~ c_lessequals(v_Y,v_X,tc_set(t_a))
| ~ c_lessequals(v_Z,v_X,tc_set(t_a))
| c_lessequals(v_Y,v_x,tc_set(t_a)) ),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
( v_X != c_union(v_Y,v_Z,t_a)
| ~ c_lessequals(v_Y,v_X,tc_set(t_a))
| ~ c_lessequals(v_Z,v_X,tc_set(t_a))
| c_lessequals(v_Y,v_x,tc_set(t_a)) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p95,plain,
( v_X != c_union(v_Y,v_Z,t_a)
| ~ c_lessequals(v_Y,v_X,tc_set(t_a))
| c_lessequals(v_Y,v_x,tc_set(t_a)) ),
inference(resolution,[status(thm)],[p94,c2]) ).
cnf(p127,plain,
( v_X != c_union(v_Y,v_Z,t_a)
| c_lessequals(v_Y,v_x,tc_set(t_a)) ),
inference(resolution,[status(thm)],[p125,p95]) ).
cnf(p30050,plain,
c_lessequals(v_Y,v_x,tc_set(t_a)),
inference(resolution,[status(thm)],[p30046,p127]) ).
cnf(p30323,plain,
( c_lessequals(c_union(v_x,v_Y,t_a),X0,tc_set(t_a))
| c_in(c_Main_OsubsetI__1(c_union(v_x,v_Y,t_a),X0,t_a),v_x,t_a) ),
inference(resolution,[status(thm)],[p30050,p380]) ).
cnf(p30842,plain,
( c_lessequals(c_union(v_x,v_Y,t_a),v_x,tc_set(t_a))
| c_lessequals(c_union(v_x,v_Y,t_a),v_x,tc_set(t_a)) ),
inference(resolution,[status(thm)],[p30323,c11]) ).
cnf(p30843,plain,
c_lessequals(c_union(v_x,v_Y,t_a),v_x,tc_set(t_a)),
inference(factoring,[status(thm)],[p30842]) ).
cnf(p30859,plain,
c_union(v_x,v_Y,t_a) = v_x,
inference(resolution,[status(thm)],[p30843,p722]) ).
cnf(f3,negated_conjecture,
( v_X != c_union(v_Y,v_Z,t_a)
| ~ c_lessequals(v_Y,v_X,tc_set(t_a))
| ~ c_lessequals(v_Z,v_X,tc_set(t_a))
| c_lessequals(v_Z,v_x,tc_set(t_a)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_3) ).
fof(f3_nnf,plain,
( v_X != c_union(v_Y,v_Z,t_a)
| ~ c_lessequals(v_Y,v_X,tc_set(t_a))
| ~ c_lessequals(v_Z,v_X,tc_set(t_a))
| c_lessequals(v_Z,v_x,tc_set(t_a)) ),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
( v_X != c_union(v_Y,v_Z,t_a)
| ~ c_lessequals(v_Y,v_X,tc_set(t_a))
| ~ c_lessequals(v_Z,v_X,tc_set(t_a))
| c_lessequals(v_Z,v_x,tc_set(t_a)) ),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
( v_X != c_union(v_Y,v_Z,t_a)
| ~ c_lessequals(v_Y,v_X,tc_set(t_a))
| ~ c_lessequals(v_Z,v_X,tc_set(t_a))
| c_lessequals(v_Z,v_x,tc_set(t_a)) ),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p96,plain,
( v_X != c_union(v_Y,v_Z,t_a)
| ~ c_lessequals(v_Y,v_X,tc_set(t_a))
| c_lessequals(v_Z,v_x,tc_set(t_a)) ),
inference(resolution,[status(thm)],[p94,c3]) ).
cnf(p128,plain,
( v_X != c_union(v_Y,v_Z,t_a)
| c_lessequals(v_Z,v_x,tc_set(t_a)) ),
inference(resolution,[status(thm)],[p125,p96]) ).
cnf(p30051,plain,
c_lessequals(v_Z,v_x,tc_set(t_a)),
inference(resolution,[status(thm)],[p30046,p128]) ).
cnf(p30345,plain,
( c_lessequals(c_union(v_x,v_Z,t_a),X0,tc_set(t_a))
| c_in(c_Main_OsubsetI__1(c_union(v_x,v_Z,t_a),X0,t_a),v_x,t_a) ),
inference(resolution,[status(thm)],[p30051,p380]) ).
cnf(p30989,plain,
( c_lessequals(c_union(v_x,v_Z,t_a),v_x,tc_set(t_a))
| c_lessequals(c_union(v_x,v_Z,t_a),v_x,tc_set(t_a)) ),
inference(resolution,[status(thm)],[p30345,c11]) ).
cnf(p30990,plain,
c_lessequals(c_union(v_x,v_Z,t_a),v_x,tc_set(t_a)),
inference(factoring,[status(thm)],[p30989]) ).
cnf(p31007,plain,
c_union(v_x,v_Z,t_a) = v_x,
inference(resolution,[status(thm)],[p30990,p722]) ).
cnf(p267,plain,
( c_lessequals(c_union(X0,X1,X2),c_union(X3,X1,X2),tc_set(X2))
| c_lessequals(c_union(X0,X1,X2),c_union(X3,X1,X2),tc_set(X2))
| c_in(c_Main_OsubsetI__1(c_union(X0,X1,X2),c_union(X3,X1,X2),X2),X0,X2) ),
inference(resolution,[status(thm)],[p102,c11]) ).
cnf(p1140,plain,
( c_lessequals(c_union(X0,X1,X2),c_union(X3,X1,X2),tc_set(X2))
| c_in(c_Main_OsubsetI__1(c_union(X0,X1,X2),c_union(X3,X1,X2),X2),X0,X2) ),
inference(factoring,[status(thm)],[p267]) ).
cnf(p31967,plain,
( c_lessequals(c_union(X0,v_Z,t_a),v_x,tc_set(t_a))
| c_in(c_Main_OsubsetI__1(c_union(X0,v_Z,t_a),v_x,t_a),X0,t_a) ),
inference(superposition,[status(thm)],[p31007,p1140]) ).
cnf(p31984,plain,
( c_lessequals(c_union(v_Y,v_Z,t_a),v_x,tc_set(t_a))
| c_in(c_Main_OsubsetI__1(v_X,v_x,t_a),v_Y,t_a) ),
inference(superposition,[status(thm)],[p30046,p31967]) ).
cnf(p32014,plain,
( c_lessequals(v_X,v_x,tc_set(t_a))
| c_in(c_Main_OsubsetI__1(v_X,v_x,t_a),v_Y,t_a) ),
inference(superposition,[status(thm)],[p30046,p31984]) ).
cnf(p32015,plain,
( c_in(c_Main_OsubsetI__1(v_X,v_x,t_a),c_union(X0,v_Y,t_a),t_a)
| c_lessequals(v_X,v_x,tc_set(t_a)) ),
inference(resolution,[status(thm)],[p32014,c6]) ).
cnf(p32021,plain,
( c_in(c_Main_OsubsetI__1(v_X,v_x,t_a),v_x,t_a)
| c_lessequals(v_X,v_x,tc_set(t_a)) ),
inference(superposition,[status(thm)],[p30859,p32015]) ).
cnf(p32025,plain,
( c_lessequals(v_X,v_x,tc_set(t_a))
| c_lessequals(v_X,v_x,tc_set(t_a)) ),
inference(resolution,[status(thm)],[p32021,c11]) ).
cnf(p32032,plain,
c_lessequals(v_X,v_x,tc_set(t_a)),
inference(factoring,[status(thm)],[p32025]) ).
cnf(f4,negated_conjecture,
( v_X != c_union(v_Y,v_Z,t_a)
| ~ c_lessequals(v_Y,v_X,tc_set(t_a))
| ~ c_lessequals(v_Z,v_X,tc_set(t_a))
| ~ c_lessequals(v_X,v_x,tc_set(t_a)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_4) ).
fof(f4_nnf,plain,
( v_X != c_union(v_Y,v_Z,t_a)
| ~ c_lessequals(v_Y,v_X,tc_set(t_a))
| ~ c_lessequals(v_Z,v_X,tc_set(t_a))
| ~ c_lessequals(v_X,v_x,tc_set(t_a)) ),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
( v_X != c_union(v_Y,v_Z,t_a)
| ~ c_lessequals(v_Y,v_X,tc_set(t_a))
| ~ c_lessequals(v_Z,v_X,tc_set(t_a))
| ~ c_lessequals(v_X,v_x,tc_set(t_a)) ),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c4,plain,
( v_X != c_union(v_Y,v_Z,t_a)
| ~ c_lessequals(v_Y,v_X,tc_set(t_a))
| ~ c_lessequals(v_Z,v_X,tc_set(t_a))
| ~ c_lessequals(v_X,v_x,tc_set(t_a)) ),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p32033,plain,
( v_X != c_union(v_Y,v_Z,t_a)
| ~ c_lessequals(v_Y,v_X,tc_set(t_a))
| ~ c_lessequals(v_Z,v_X,tc_set(t_a)) ),
inference(resolution,[status(thm)],[p32032,c4]) ).
cnf(p32788,plain,
( v_X != c_union(v_Y,v_Z,t_a)
| ~ c_lessequals(v_Y,v_X,tc_set(t_a)) ),
inference(resolution,[status(thm)],[p32033,p94]) ).
cnf(p32803,plain,
v_X != c_union(v_Y,v_Z,t_a),
inference(resolution,[status(thm)],[p32788,p125]) ).
cnf(p32804,plain,
$false,
inference(resolution,[status(thm)],[p32803,p30046]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET837-2 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.11/0.36 % Computer : n020.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Thu Sep 24 12:09:33 UTC 2026
% 0.11/0.36 % CPUTime :
% 0.11/0.36 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 96.63/67.60 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 96.63/67.60 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------