%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SET851-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 0.71s 0.91s
% Output : Refutation 0.71s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 10
% Syntax : Number of clauses : 23 ( 10 unt; 5 nHn; 13 RR)
% Number of literals : 48 ( 24 equ; 22 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 : 7 ( 7 usr; 4 con; 0-3 aty)
% Number of variables : 46 ( 7 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(cls_conjecture_3,negated_conjecture,
~ c_lessequals(c_Zorn_Osucc(v_S,v_m,t_a),c_Zorn_Osucc(v_S,v_x,t_a),tc_set(tc_set(t_a))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_3) ).
cnf(reflexivity,axiom,
X2 = X2,
theory(equality) ).
cnf(cls_Set_Osubset__refl_0,axiom,
c_lessequals(X4,X4,tc_set(X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Set_Osubset__refl_0) ).
cnf(c3,axiom,
( X45 != X47
| X48 != X50
| X46 != X49
| ~ c_lessequals(X45,X48,X46)
| c_lessequals(X47,X50,X49) ),
theory(equality) ).
cnf(c20,plain,
( X55 != X53
| X55 != X54
| tc_set(X51) != X52
| c_lessequals(X53,X54,X52) ),
inference(resolution,[status(thm)],[c3,cls_Set_Osubset__refl_0]) ).
cnf(c23,plain,
( X57 != X56
| X57 != X58
| c_lessequals(X56,X58,tc_set(X59)) ),
inference(resolution,[status(thm)],[c20,reflexivity]) ).
cnf(c29,plain,
( X63 != X65
| c_lessequals(X65,X63,tc_set(X64)) ),
inference(resolution,[status(thm)],[c23,reflexivity]) ).
cnf(c1,axiom,
( X81 != X83
| X84 != X86
| X82 != X85
| c_Zorn_Osucc(X81,X84,X82) = c_Zorn_Osucc(X83,X86,X85) ),
theory(equality) ).
cnf(c40,plain,
( X130 != X129
| X127 != X126
| c_Zorn_Osucc(X130,X127,X128) = c_Zorn_Osucc(X129,X126,X128) ),
inference(resolution,[status(thm)],[c1,reflexivity]) ).
cnf(cls_conjecture_2,negated_conjecture,
~ c_lessequals(c_Zorn_Osucc(v_S,v_x,t_a),v_m,tc_set(tc_set(t_a))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_2) ).
cnf(cls_Zorn_Osucc__trans_0,axiom,
( ~ c_lessequals(X14,X13,tc_set(tc_set(X12)))
| c_lessequals(X14,c_Zorn_Osucc(X11,X13,X12),tc_set(tc_set(X12))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Zorn_Osucc__trans_0) ).
cnf(cls_conjecture_4,negated_conjecture,
( c_lessequals(c_Zorn_Osucc(v_S,v_m,t_a),v_x,tc_set(tc_set(t_a)))
| c_lessequals(v_x,v_m,tc_set(tc_set(t_a))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_4) ).
cnf(c25,plain,
( c_lessequals(v_x,v_m,tc_set(tc_set(t_a)))
| c_lessequals(c_Zorn_Osucc(v_S,v_m,t_a),c_Zorn_Osucc(X212,v_x,t_a),tc_set(tc_set(t_a))) ),
inference(resolution,[status(thm)],[cls_conjecture_4,cls_Zorn_Osucc__trans_0]) ).
cnf(c72,plain,
c_lessequals(v_x,v_m,tc_set(tc_set(t_a))),
inference(resolution,[status(thm)],[c25,cls_conjecture_3]) ).
cnf(cls_conjecture_1,negated_conjecture,
c_in(v_x,c_Zorn_OTFin(v_S,t_a),tc_set(tc_set(t_a))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_1) ).
cnf(cls_conjecture_5,negated_conjecture,
( c_lessequals(c_Zorn_Osucc(v_S,X71,t_a),v_m,tc_set(tc_set(t_a)))
| X71 = v_m
| ~ c_lessequals(X71,v_m,tc_set(tc_set(t_a)))
| ~ c_in(X71,c_Zorn_OTFin(v_S,t_a),tc_set(tc_set(t_a))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_5) ).
cnf(c33,plain,
( c_lessequals(c_Zorn_Osucc(v_S,v_x,t_a),v_m,tc_set(tc_set(t_a)))
| v_x = v_m
| ~ c_lessequals(v_x,v_m,tc_set(tc_set(t_a))) ),
inference(resolution,[status(thm)],[cls_conjecture_5,cls_conjecture_1]) ).
cnf(c93,plain,
( c_lessequals(c_Zorn_Osucc(v_S,v_x,t_a),v_m,tc_set(tc_set(t_a)))
| v_x = v_m ),
inference(resolution,[status(thm)],[c33,c72]) ).
cnf(c95,plain,
v_x = v_m,
inference(resolution,[status(thm)],[c93,cls_conjecture_2]) ).
cnf(c120,plain,
( X469 != X468
| c_Zorn_Osucc(X469,v_x,X467) = c_Zorn_Osucc(X468,v_m,X467) ),
inference(resolution,[status(thm)],[c95,c40]) ).
cnf(c941,plain,
c_Zorn_Osucc(X470,v_x,X471) = c_Zorn_Osucc(X470,v_m,X471),
inference(resolution,[status(thm)],[c120,reflexivity]) ).
cnf(c986,plain,
c_lessequals(c_Zorn_Osucc(X484,v_m,X483),c_Zorn_Osucc(X484,v_x,X483),tc_set(X482)),
inference(resolution,[status(thm)],[c941,c29]) ).
cnf(c1098,plain,
$false,
inference(resolution,[status(thm)],[c986,cls_conjecture_3]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : SET851-2 : TPTP v8.1.2. Released v3.2.0.
% 0.07/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.35 % Computer : n028.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Wed May 8 19:08:38 EDT 2024
% 0.13/0.35 % CPUTime :
% 0.71/0.91 % Version: 1.5
% 0.71/0.91 % SZS status Unsatisfiable
% 0.71/0.91 % SZS output start CNFRefutation
% See solution above
% 0.71/0.91
% 0.71/0.91 % Initial clauses : 15
% 0.71/0.91 % Processed clauses : 145
% 0.71/0.91 % Factors computed : 16
% 0.71/0.91 % Resolvents computed: 1080
% 0.71/0.91 % Tautologies deleted: 2
% 0.71/0.91 % Forward subsumed : 129
% 0.71/0.91 % Backward subsumed : 10
% 0.71/0.91 % -------- CPU Time ---------
% 0.71/0.91 % User time : 0.536 s
% 0.71/0.91 % System time : 0.020 s
% 0.71/0.91 % Total time : 0.556 s
%------------------------------------------------------------------------------