%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SET853-2 : TPTP v8.1.2. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n028.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu May 9 17:40:14 EDT 2024
% Result : Unsatisfiable 28.54s 28.73s
% Output : Refutation 28.54s
% Verified :
% SZS Type : Refutation
% Derivation depth : 37
% Number of leaves : 17
% Syntax : Number of clauses : 67 ( 15 unt; 41 nHn; 46 RR)
% Number of literals : 169 ( 54 equ; 47 neg)
% Maximal clause size : 5 ( 2 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-3 aty)
% Number of functors : 8 ( 8 usr; 4 con; 0-3 aty)
% Number of variables : 95 ( 11 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(cls_conjecture_4,negated_conjecture,
~ c_lessequals(c_Zorn_Osucc(v_S,v_xa,t_a),c_Zorn_Osucc(v_S,v_x,t_a),tc_set(tc_set(t_a))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_4) ).
cnf(reflexivity,axiom,
X2 = X2,
theory(equality) ).
cnf(cls_Set_Osubset__refl_0,axiom,
c_lessequals(X3,X3,tc_set(X4)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Set_Osubset__refl_0) ).
cnf(c5,axiom,
( X67 != X69
| X70 != X71
| X66 != X68
| ~ c_lessequals(X67,X70,X66)
| c_lessequals(X69,X71,X68) ),
theory(equality) ).
cnf(c35,plain,
( X72 != X75
| X72 != X74
| tc_set(X76) != X73
| c_lessequals(X75,X74,X73) ),
inference(resolution,[status(thm)],[c5,cls_Set_Osubset__refl_0]) ).
cnf(c39,plain,
( X79 != X80
| X79 != X78
| c_lessequals(X80,X78,tc_set(X77)) ),
inference(resolution,[status(thm)],[c35,reflexivity]) ).
cnf(c41,plain,
( X85 != X86
| c_lessequals(X86,X85,tc_set(X84)) ),
inference(resolution,[status(thm)],[c39,reflexivity]) ).
cnf(symmetry,axiom,
( X6 != X5
| X5 = X6 ),
theory(equality) ).
cnf(c2,axiom,
( X119 != X121
| X122 != X123
| X118 != X120
| c_Zorn_Osucc(X119,X122,X118) = c_Zorn_Osucc(X121,X123,X120) ),
theory(equality) ).
cnf(c60,plain,
( X153 != X154
| X156 != X155
| c_Zorn_Osucc(X153,X156,X157) = c_Zorn_Osucc(X154,X155,X157) ),
inference(resolution,[status(thm)],[c2,reflexivity]) ).
cnf(cls_Zorn_Osucc__trans_0,axiom,
( ~ c_lessequals(X38,X39,tc_set(tc_set(X37)))
| c_lessequals(X38,c_Zorn_Osucc(X36,X39,X37),tc_set(tc_set(X37))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Zorn_Osucc__trans_0) ).
cnf(cls_conjecture_1,negated_conjecture,
c_in(v_xa,c_Zorn_OTFin(v_S,t_a),tc_set(tc_set(t_a))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_1) ).
cnf(cls_conjecture_5,negated_conjecture,
( c_lessequals(c_Zorn_Osucc(v_S,X40,t_a),v_x,tc_set(tc_set(t_a)))
| X40 = v_x
| ~ c_lessequals(X40,v_x,tc_set(tc_set(t_a)))
| ~ c_in(X40,c_Zorn_OTFin(v_S,t_a),tc_set(tc_set(t_a))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_5) ).
cnf(c20,plain,
( c_lessequals(c_Zorn_Osucc(v_S,v_xa,t_a),v_x,tc_set(tc_set(t_a)))
| v_xa = v_x
| ~ c_lessequals(v_xa,v_x,tc_set(tc_set(t_a))) ),
inference(resolution,[status(thm)],[cls_conjecture_5,cls_conjecture_1]) ).
cnf(cls_conjecture_3,negated_conjecture,
v_xa != c_Zorn_Osucc(v_S,v_x,t_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_3) ).
cnf(cls_conjecture_2,negated_conjecture,
c_lessequals(v_xa,c_Zorn_Osucc(v_S,v_x,t_a),tc_set(tc_set(t_a))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_2) ).
cnf(cls_Set_Osubset__antisym_0,axiom,
( ~ c_lessequals(X18,X17,tc_set(X19))
| ~ c_lessequals(X17,X18,tc_set(X19))
| X17 = X18 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Set_Osubset__antisym_0) ).
cnf(c11,plain,
( ~ c_lessequals(c_Zorn_Osucc(v_S,v_x,t_a),v_xa,tc_set(tc_set(t_a)))
| v_xa = c_Zorn_Osucc(v_S,v_x,t_a) ),
inference(resolution,[status(thm)],[cls_Set_Osubset__antisym_0,cls_conjecture_2]) ).
cnf(cls_conjecture_0,negated_conjecture,
c_in(v_x,c_Zorn_OTFin(v_S,t_a),tc_set(tc_set(t_a))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_0) ).
cnf(cls_Zorn_OTFin__linear__lemma1_3,axiom,
( ~ c_in(X117,c_Zorn_OTFin(X114,X116),tc_set(tc_set(X116)))
| ~ c_in(X115,c_Zorn_OTFin(X114,X116),tc_set(tc_set(X116)))
| ~ c_lessequals(c_Zorn_Osucc(X114,c_Zorn_OTFin__linear__lemma1__1(X114,X117,X116),X116),X117,tc_set(tc_set(X116)))
| c_lessequals(X115,X117,tc_set(tc_set(X116)))
| c_lessequals(c_Zorn_Osucc(X114,X117,X116),X115,tc_set(tc_set(X116))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Zorn_OTFin__linear__lemma1_3) ).
cnf(cls_Zorn_OTFin__linear__lemma1_2,axiom,
( ~ c_in(X104,c_Zorn_OTFin(X101,X103),tc_set(tc_set(X103)))
| ~ c_in(X102,c_Zorn_OTFin(X101,X103),tc_set(tc_set(X103)))
| c_Zorn_OTFin__linear__lemma1__1(X101,X104,X103) != X104
| c_lessequals(X102,X104,tc_set(tc_set(X103)))
| c_lessequals(c_Zorn_Osucc(X101,X104,X103),X102,tc_set(tc_set(X103))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Zorn_OTFin__linear__lemma1_2) ).
cnf(c52,plain,
( ~ c_in(X490,c_Zorn_OTFin(v_S,t_a),tc_set(tc_set(t_a)))
| c_Zorn_OTFin__linear__lemma1__1(v_S,X490,t_a) != X490
| c_lessequals(v_xa,X490,tc_set(tc_set(t_a)))
| c_lessequals(c_Zorn_Osucc(v_S,X490,t_a),v_xa,tc_set(tc_set(t_a))) ),
inference(resolution,[status(thm)],[cls_Zorn_OTFin__linear__lemma1_2,cls_conjecture_1]) ).
cnf(c157,plain,
( c_Zorn_OTFin__linear__lemma1__1(v_S,v_x,t_a) != v_x
| c_lessequals(v_xa,v_x,tc_set(tc_set(t_a)))
| c_lessequals(c_Zorn_Osucc(v_S,v_x,t_a),v_xa,tc_set(tc_set(t_a))) ),
inference(resolution,[status(thm)],[c52,cls_conjecture_0]) ).
cnf(cls_Zorn_OTFin__linear__lemma1_1,axiom,
( ~ c_in(X90,c_Zorn_OTFin(X87,X89),tc_set(tc_set(X89)))
| ~ c_in(X88,c_Zorn_OTFin(X87,X89),tc_set(tc_set(X89)))
| c_lessequals(X88,X90,tc_set(tc_set(X89)))
| c_lessequals(c_Zorn_OTFin__linear__lemma1__1(X87,X90,X89),X90,tc_set(tc_set(X89)))
| c_lessequals(c_Zorn_Osucc(X87,X90,X89),X88,tc_set(tc_set(X89))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Zorn_OTFin__linear__lemma1_1) ).
cnf(c45,plain,
( ~ c_in(X399,c_Zorn_OTFin(v_S,t_a),tc_set(tc_set(t_a)))
| c_lessequals(v_xa,X399,tc_set(tc_set(t_a)))
| c_lessequals(c_Zorn_OTFin__linear__lemma1__1(v_S,X399,t_a),X399,tc_set(tc_set(t_a)))
| c_lessequals(c_Zorn_Osucc(v_S,X399,t_a),v_xa,tc_set(tc_set(t_a))) ),
inference(resolution,[status(thm)],[cls_Zorn_OTFin__linear__lemma1_1,cls_conjecture_1]) ).
cnf(c138,plain,
( c_lessequals(v_xa,v_x,tc_set(tc_set(t_a)))
| c_lessequals(c_Zorn_OTFin__linear__lemma1__1(v_S,v_x,t_a),v_x,tc_set(tc_set(t_a)))
| c_lessequals(c_Zorn_Osucc(v_S,v_x,t_a),v_xa,tc_set(tc_set(t_a))) ),
inference(resolution,[status(thm)],[c45,cls_conjecture_0]) ).
cnf(c194,plain,
( c_lessequals(v_xa,v_x,tc_set(tc_set(t_a)))
| c_lessequals(c_Zorn_OTFin__linear__lemma1__1(v_S,v_x,t_a),v_x,tc_set(tc_set(t_a)))
| v_xa = c_Zorn_Osucc(v_S,v_x,t_a) ),
inference(resolution,[status(thm)],[c138,c11]) ).
cnf(c241,plain,
( c_lessequals(v_xa,v_x,tc_set(tc_set(t_a)))
| c_lessequals(c_Zorn_OTFin__linear__lemma1__1(v_S,v_x,t_a),v_x,tc_set(tc_set(t_a))) ),
inference(resolution,[status(thm)],[c194,cls_conjecture_3]) ).
cnf(c256,plain,
( c_lessequals(c_Zorn_OTFin__linear__lemma1__1(v_S,v_x,t_a),v_x,tc_set(tc_set(t_a)))
| c_lessequals(c_Zorn_Osucc(v_S,v_xa,t_a),v_x,tc_set(tc_set(t_a)))
| v_xa = v_x ),
inference(resolution,[status(thm)],[c241,c20]) ).
cnf(c322,plain,
( c_lessequals(c_Zorn_OTFin__linear__lemma1__1(v_S,v_x,t_a),v_x,tc_set(tc_set(t_a)))
| v_xa = v_x
| c_lessequals(c_Zorn_Osucc(v_S,v_xa,t_a),c_Zorn_Osucc(X897,v_x,t_a),tc_set(tc_set(t_a))) ),
inference(resolution,[status(thm)],[c256,cls_Zorn_Osucc__trans_0]) ).
cnf(c888,plain,
( c_lessequals(c_Zorn_OTFin__linear__lemma1__1(v_S,v_x,t_a),v_x,tc_set(tc_set(t_a)))
| v_xa = v_x ),
inference(resolution,[status(thm)],[c322,cls_conjecture_4]) ).
cnf(c910,plain,
( c_lessequals(c_Zorn_OTFin__linear__lemma1__1(v_S,v_x,t_a),v_x,tc_set(tc_set(t_a)))
| X1167 != X1168
| c_Zorn_Osucc(X1167,v_xa,X1166) = c_Zorn_Osucc(X1168,v_x,X1166) ),
inference(resolution,[status(thm)],[c888,c60]) ).
cnf(c3359,plain,
( c_lessequals(c_Zorn_OTFin__linear__lemma1__1(v_S,v_x,t_a),v_x,tc_set(tc_set(t_a)))
| c_Zorn_Osucc(X1170,v_xa,X1169) = c_Zorn_Osucc(X1170,v_x,X1169) ),
inference(resolution,[status(thm)],[c910,reflexivity]) ).
cnf(c3396,plain,
( c_lessequals(c_Zorn_OTFin__linear__lemma1__1(v_S,v_x,t_a),v_x,tc_set(tc_set(t_a)))
| c_Zorn_Osucc(X1172,v_x,X1171) = c_Zorn_Osucc(X1172,v_xa,X1171) ),
inference(resolution,[status(thm)],[c3359,symmetry]) ).
cnf(c3449,plain,
( c_lessequals(c_Zorn_OTFin__linear__lemma1__1(v_S,v_x,t_a),v_x,tc_set(tc_set(t_a)))
| c_lessequals(c_Zorn_Osucc(X1184,v_xa,X1186),c_Zorn_Osucc(X1184,v_x,X1186),tc_set(X1185)) ),
inference(resolution,[status(thm)],[c3396,c41]) ).
cnf(c3545,plain,
c_lessequals(c_Zorn_OTFin__linear__lemma1__1(v_S,v_x,t_a),v_x,tc_set(tc_set(t_a))),
inference(resolution,[status(thm)],[c3449,cls_conjecture_4]) ).
cnf(cls_Zorn_OTFin__linear__lemma1_0,axiom,
( ~ c_in(X65,c_Zorn_OTFin(X62,X64),tc_set(tc_set(X64)))
| ~ c_in(X63,c_Zorn_OTFin(X62,X64),tc_set(tc_set(X64)))
| c_in(c_Zorn_OTFin__linear__lemma1__1(X62,X65,X64),c_Zorn_OTFin(X62,X64),tc_set(tc_set(X64)))
| c_lessequals(X63,X65,tc_set(tc_set(X64)))
| c_lessequals(c_Zorn_Osucc(X62,X65,X64),X63,tc_set(tc_set(X64))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Zorn_OTFin__linear__lemma1_0) ).
cnf(c31,plain,
( ~ c_in(X295,c_Zorn_OTFin(v_S,t_a),tc_set(tc_set(t_a)))
| c_in(c_Zorn_OTFin__linear__lemma1__1(v_S,X295,t_a),c_Zorn_OTFin(v_S,t_a),tc_set(tc_set(t_a)))
| c_lessequals(v_xa,X295,tc_set(tc_set(t_a)))
| c_lessequals(c_Zorn_Osucc(v_S,X295,t_a),v_xa,tc_set(tc_set(t_a))) ),
inference(resolution,[status(thm)],[cls_Zorn_OTFin__linear__lemma1_0,cls_conjecture_1]) ).
cnf(c110,plain,
( c_in(c_Zorn_OTFin__linear__lemma1__1(v_S,v_x,t_a),c_Zorn_OTFin(v_S,t_a),tc_set(tc_set(t_a)))
| c_lessequals(v_xa,v_x,tc_set(tc_set(t_a)))
| c_lessequals(c_Zorn_Osucc(v_S,v_x,t_a),v_xa,tc_set(tc_set(t_a))) ),
inference(resolution,[status(thm)],[c31,cls_conjecture_0]) ).
cnf(c295,plain,
( c_in(c_Zorn_OTFin__linear__lemma1__1(v_S,v_x,t_a),c_Zorn_OTFin(v_S,t_a),tc_set(tc_set(t_a)))
| c_lessequals(v_xa,v_x,tc_set(tc_set(t_a)))
| v_xa = c_Zorn_Osucc(v_S,v_x,t_a) ),
inference(resolution,[status(thm)],[c110,c11]) ).
cnf(c489,plain,
( c_in(c_Zorn_OTFin__linear__lemma1__1(v_S,v_x,t_a),c_Zorn_OTFin(v_S,t_a),tc_set(tc_set(t_a)))
| c_lessequals(v_xa,v_x,tc_set(tc_set(t_a))) ),
inference(resolution,[status(thm)],[c295,cls_conjecture_3]) ).
cnf(c512,plain,
( c_lessequals(v_xa,v_x,tc_set(tc_set(t_a)))
| c_lessequals(c_Zorn_Osucc(v_S,c_Zorn_OTFin__linear__lemma1__1(v_S,v_x,t_a),t_a),v_x,tc_set(tc_set(t_a)))
| c_Zorn_OTFin__linear__lemma1__1(v_S,v_x,t_a) = v_x
| ~ c_lessequals(c_Zorn_OTFin__linear__lemma1__1(v_S,v_x,t_a),v_x,tc_set(tc_set(t_a))) ),
inference(resolution,[status(thm)],[c489,cls_conjecture_5]) ).
cnf(c4301,plain,
( c_lessequals(v_xa,v_x,tc_set(tc_set(t_a)))
| c_lessequals(c_Zorn_Osucc(v_S,c_Zorn_OTFin__linear__lemma1__1(v_S,v_x,t_a),t_a),v_x,tc_set(tc_set(t_a)))
| c_Zorn_OTFin__linear__lemma1__1(v_S,v_x,t_a) = v_x ),
inference(resolution,[status(thm)],[c512,c3545]) ).
cnf(c4805,plain,
( c_lessequals(v_xa,v_x,tc_set(tc_set(t_a)))
| c_lessequals(c_Zorn_Osucc(v_S,c_Zorn_OTFin__linear__lemma1__1(v_S,v_x,t_a),t_a),v_x,tc_set(tc_set(t_a)))
| c_lessequals(c_Zorn_Osucc(v_S,v_x,t_a),v_xa,tc_set(tc_set(t_a))) ),
inference(resolution,[status(thm)],[c4301,c157]) ).
cnf(c10496,plain,
( c_lessequals(v_xa,v_x,tc_set(tc_set(t_a)))
| c_lessequals(c_Zorn_Osucc(v_S,c_Zorn_OTFin__linear__lemma1__1(v_S,v_x,t_a),t_a),v_x,tc_set(tc_set(t_a)))
| v_xa = c_Zorn_Osucc(v_S,v_x,t_a) ),
inference(resolution,[status(thm)],[c4805,c11]) ).
cnf(c10532,plain,
( c_lessequals(v_xa,v_x,tc_set(tc_set(t_a)))
| c_lessequals(c_Zorn_Osucc(v_S,c_Zorn_OTFin__linear__lemma1__1(v_S,v_x,t_a),t_a),v_x,tc_set(tc_set(t_a))) ),
inference(resolution,[status(thm)],[c10496,cls_conjecture_3]) ).
cnf(c10558,plain,
( c_lessequals(c_Zorn_Osucc(v_S,c_Zorn_OTFin__linear__lemma1__1(v_S,v_x,t_a),t_a),v_x,tc_set(tc_set(t_a)))
| c_lessequals(c_Zorn_Osucc(v_S,v_xa,t_a),v_x,tc_set(tc_set(t_a)))
| v_xa = v_x ),
inference(resolution,[status(thm)],[c10532,c20]) ).
cnf(c10640,plain,
( c_lessequals(c_Zorn_Osucc(v_S,c_Zorn_OTFin__linear__lemma1__1(v_S,v_x,t_a),t_a),v_x,tc_set(tc_set(t_a)))
| v_xa = v_x
| c_lessequals(c_Zorn_Osucc(v_S,v_xa,t_a),c_Zorn_Osucc(X11529,v_x,t_a),tc_set(tc_set(t_a))) ),
inference(resolution,[status(thm)],[c10558,cls_Zorn_Osucc__trans_0]) ).
cnf(c11724,plain,
( c_lessequals(c_Zorn_Osucc(v_S,c_Zorn_OTFin__linear__lemma1__1(v_S,v_x,t_a),t_a),v_x,tc_set(tc_set(t_a)))
| v_xa = v_x ),
inference(resolution,[status(thm)],[c10640,cls_conjecture_4]) ).
cnf(c11747,plain,
( c_lessequals(c_Zorn_Osucc(v_S,c_Zorn_OTFin__linear__lemma1__1(v_S,v_x,t_a),t_a),v_x,tc_set(tc_set(t_a)))
| X11981 != X11982
| c_Zorn_Osucc(X11981,v_xa,X11980) = c_Zorn_Osucc(X11982,v_x,X11980) ),
inference(resolution,[status(thm)],[c11724,c60]) ).
cnf(c14217,plain,
( c_lessequals(c_Zorn_Osucc(v_S,c_Zorn_OTFin__linear__lemma1__1(v_S,v_x,t_a),t_a),v_x,tc_set(tc_set(t_a)))
| c_Zorn_Osucc(X11984,v_xa,X11983) = c_Zorn_Osucc(X11984,v_x,X11983) ),
inference(resolution,[status(thm)],[c11747,reflexivity]) ).
cnf(c14259,plain,
( c_lessequals(c_Zorn_Osucc(v_S,c_Zorn_OTFin__linear__lemma1__1(v_S,v_x,t_a),t_a),v_x,tc_set(tc_set(t_a)))
| c_Zorn_Osucc(X11986,v_x,X11985) = c_Zorn_Osucc(X11986,v_xa,X11985) ),
inference(resolution,[status(thm)],[c14217,symmetry]) ).
cnf(c14321,plain,
( c_lessequals(c_Zorn_Osucc(v_S,c_Zorn_OTFin__linear__lemma1__1(v_S,v_x,t_a),t_a),v_x,tc_set(tc_set(t_a)))
| c_lessequals(c_Zorn_Osucc(X11997,v_xa,X11996),c_Zorn_Osucc(X11997,v_x,X11996),tc_set(X11998)) ),
inference(resolution,[status(thm)],[c14259,c41]) ).
cnf(c14431,plain,
c_lessequals(c_Zorn_Osucc(v_S,c_Zorn_OTFin__linear__lemma1__1(v_S,v_x,t_a),t_a),v_x,tc_set(tc_set(t_a))),
inference(resolution,[status(thm)],[c14321,cls_conjecture_4]) ).
cnf(c14435,plain,
( ~ c_in(v_x,c_Zorn_OTFin(v_S,t_a),tc_set(tc_set(t_a)))
| ~ c_in(X20605,c_Zorn_OTFin(v_S,t_a),tc_set(tc_set(t_a)))
| c_lessequals(X20605,v_x,tc_set(tc_set(t_a)))
| c_lessequals(c_Zorn_Osucc(v_S,v_x,t_a),X20605,tc_set(tc_set(t_a))) ),
inference(resolution,[status(thm)],[c14431,cls_Zorn_OTFin__linear__lemma1_3]) ).
cnf(c17448,plain,
( ~ c_in(v_x,c_Zorn_OTFin(v_S,t_a),tc_set(tc_set(t_a)))
| c_lessequals(v_xa,v_x,tc_set(tc_set(t_a)))
| c_lessequals(c_Zorn_Osucc(v_S,v_x,t_a),v_xa,tc_set(tc_set(t_a))) ),
inference(resolution,[status(thm)],[c14435,cls_conjecture_1]) ).
cnf(c17451,plain,
( c_lessequals(v_xa,v_x,tc_set(tc_set(t_a)))
| c_lessequals(c_Zorn_Osucc(v_S,v_x,t_a),v_xa,tc_set(tc_set(t_a))) ),
inference(resolution,[status(thm)],[c17448,cls_conjecture_0]) ).
cnf(c17469,plain,
( c_lessequals(v_xa,v_x,tc_set(tc_set(t_a)))
| v_xa = c_Zorn_Osucc(v_S,v_x,t_a) ),
inference(resolution,[status(thm)],[c17451,c11]) ).
cnf(c17506,plain,
c_lessequals(v_xa,v_x,tc_set(tc_set(t_a))),
inference(resolution,[status(thm)],[c17469,cls_conjecture_3]) ).
cnf(c17536,plain,
( c_lessequals(c_Zorn_Osucc(v_S,v_xa,t_a),v_x,tc_set(tc_set(t_a)))
| v_xa = v_x ),
inference(resolution,[status(thm)],[c17506,c20]) ).
cnf(c17598,plain,
( v_xa = v_x
| c_lessequals(c_Zorn_Osucc(v_S,v_xa,t_a),c_Zorn_Osucc(X20648,v_x,t_a),tc_set(tc_set(t_a))) ),
inference(resolution,[status(thm)],[c17536,cls_Zorn_Osucc__trans_0]) ).
cnf(c18386,plain,
v_xa = v_x,
inference(resolution,[status(thm)],[c17598,cls_conjecture_4]) ).
cnf(c18407,plain,
( X20842 != X20843
| c_Zorn_Osucc(X20842,v_xa,X20841) = c_Zorn_Osucc(X20843,v_x,X20841) ),
inference(resolution,[status(thm)],[c18386,c60]) ).
cnf(c20133,plain,
c_Zorn_Osucc(X20845,v_xa,X20844) = c_Zorn_Osucc(X20845,v_x,X20844),
inference(resolution,[status(thm)],[c18407,reflexivity]) ).
cnf(c20167,plain,
c_Zorn_Osucc(X20847,v_x,X20846) = c_Zorn_Osucc(X20847,v_xa,X20846),
inference(resolution,[status(thm)],[c20133,symmetry]) ).
cnf(c20226,plain,
c_lessequals(c_Zorn_Osucc(X20858,v_xa,X20859),c_Zorn_Osucc(X20858,v_x,X20859),tc_set(X20857)),
inference(resolution,[status(thm)],[c20167,c41]) ).
cnf(c20323,plain,
$false,
inference(resolution,[status(thm)],[c20226,cls_conjecture_4]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : SET853-2 : TPTP v8.1.2. Released v3.2.0.
% 0.04/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.33 % Computer : n028.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Wed May 8 18:19:37 EDT 2024
% 0.12/0.33 % CPUTime :
% 28.54/28.73 % Version: 1.5
% 28.54/28.73 % SZS status Unsatisfiable
% 28.54/28.73 % SZS output start CNFRefutation
% See solution above
% 28.54/28.73
% 28.54/28.73 % Initial clauses : 22
% 28.54/28.73 % Processed clauses : 1144
% 28.54/28.73 % Factors computed : 34
% 28.54/28.73 % Resolvents computed: 20286
% 28.54/28.73 % Tautologies deleted: 2
% 28.54/28.73 % Forward subsumed : 6955
% 28.54/28.73 % Backward subsumed : 775
% 28.54/28.73 % -------- CPU Time ---------
% 28.54/28.73 % User time : 28.317 s
% 28.54/28.73 % System time : 0.082 s
% 28.54/28.73 % Total time : 28.399 s
%------------------------------------------------------------------------------