%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SET853-1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n004.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 : Thu Sep 24 02:10:49 PM UTC 2026
% Result : Unsatisfiable 0.10s 0.56s
% Output : CNFRefutation 0.81s
% Verified :
% SZS Type : Refutation
% Derivation depth : 6
% Number of leaves : 22
% Syntax : Number of formulae : 66 ( 18 unt; 9 def)
% Number of atoms : 175 ( 15 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 194 ( 85 ~; 100 |; 0 &)
% ( 9 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 13 ( 11 usr; 10 prp; 0-3 aty)
% Number of functors : 8 ( 8 usr; 4 con; 0-3 aty)
% Number of variables : 60 ( 60 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f309,axiom,
! [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)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f310,axiom,
! [V_A,T_a] : c_lessequals(V_A,V_A,tc_set(T_a)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1359,axiom,
! [V_m,V_S,T_a,V_n] :
( c_lessequals(c_Zorn_Osucc(V_S,V_m,T_a),V_n,tc_set(tc_set(T_a)))
| c_lessequals(V_n,V_m,tc_set(tc_set(T_a)))
| c_in(c_Zorn_OTFin__linear__lemma1__1(V_S,V_m,T_a),c_Zorn_OTFin(V_S,T_a),tc_set(tc_set(T_a)))
| ~ c_in(V_n,c_Zorn_OTFin(V_S,T_a),tc_set(tc_set(T_a)))
| ~ c_in(V_m,c_Zorn_OTFin(V_S,T_a),tc_set(tc_set(T_a))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1360,axiom,
! [V_m,V_S,T_a,V_n] :
( c_lessequals(c_Zorn_Osucc(V_S,V_m,T_a),V_n,tc_set(tc_set(T_a)))
| c_lessequals(c_Zorn_OTFin__linear__lemma1__1(V_S,V_m,T_a),V_m,tc_set(tc_set(T_a)))
| c_lessequals(V_n,V_m,tc_set(tc_set(T_a)))
| ~ c_in(V_n,c_Zorn_OTFin(V_S,T_a),tc_set(tc_set(T_a)))
| ~ c_in(V_m,c_Zorn_OTFin(V_S,T_a),tc_set(tc_set(T_a))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1361,axiom,
! [V_m,V_S,T_a,V_n] :
( c_lessequals(c_Zorn_Osucc(V_S,V_m,T_a),V_n,tc_set(tc_set(T_a)))
| c_lessequals(V_n,V_m,tc_set(tc_set(T_a)))
| c_Zorn_OTFin__linear__lemma1__1(V_S,V_m,T_a) != V_m
| ~ c_in(V_n,c_Zorn_OTFin(V_S,T_a),tc_set(tc_set(T_a)))
| ~ c_in(V_m,c_Zorn_OTFin(V_S,T_a),tc_set(tc_set(T_a))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1362,axiom,
! [V_m,V_S,T_a,V_n] :
( c_lessequals(c_Zorn_Osucc(V_S,V_m,T_a),V_n,tc_set(tc_set(T_a)))
| c_lessequals(V_n,V_m,tc_set(tc_set(T_a)))
| ~ c_lessequals(c_Zorn_Osucc(V_S,c_Zorn_OTFin__linear__lemma1__1(V_S,V_m,T_a),T_a),V_m,tc_set(tc_set(T_a)))
| ~ c_in(V_n,c_Zorn_OTFin(V_S,T_a),tc_set(tc_set(T_a)))
| ~ c_in(V_m,c_Zorn_OTFin(V_S,T_a),tc_set(tc_set(T_a))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1366,axiom,
! [V_x,V_y,T_a,V_S] :
( c_lessequals(V_x,c_Zorn_Osucc(V_S,V_y,T_a),tc_set(tc_set(T_a)))
| ~ c_lessequals(V_x,V_y,tc_set(tc_set(T_a))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1367,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') ).
fof(f1368,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') ).
fof(f1369,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') ).
fof(f1370,negated_conjecture,
v_xa != c_Zorn_Osucc(v_S,v_x,t_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1371,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') ).
fof(f1372,negated_conjecture,
! [V_U] :
( ~ c_in(V_U,c_Zorn_OTFin(v_S,t_a),tc_set(tc_set(t_a)))
| ~ c_lessequals(V_U,v_x,tc_set(tc_set(t_a)))
| V_U = v_x
| c_lessequals(c_Zorn_Osucc(v_S,V_U,t_a),v_x,tc_set(tc_set(t_a))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1789,plain,
! [V_B,V_A] :
( V_A = V_B
| ! [T_a] :
( ~ c_lessequals(V_A,V_B,tc_set(T_a))
| ~ c_lessequals(V_B,V_A,tc_set(T_a)) ) ),
inference(miniscoping,[status(thm)],[f309]) ).
fof(f1790,plain,
! [X0,X1,X2] :
( X1 = X0
| ~ c_lessequals(X1,X0,tc_set(X2))
| ~ c_lessequals(X0,X1,tc_set(X2)) ),
inference(cnf_transformation,[status(thm)],[f1789]) ).
fof(f1791,plain,
! [X0,X1] : c_lessequals(X0,X0,tc_set(X1)),
inference(cnf_transformation,[status(thm)],[f310]) ).
fof(f2849,plain,
! [X0,X1,X2,X3] :
( c_lessequals(c_Zorn_Osucc(X1,X0,X2),X3,tc_set(tc_set(X2)))
| c_lessequals(X3,X0,tc_set(tc_set(X2)))
| c_in(c_Zorn_OTFin__linear__lemma1__1(X1,X0,X2),c_Zorn_OTFin(X1,X2),tc_set(tc_set(X2)))
| ~ c_in(X3,c_Zorn_OTFin(X1,X2),tc_set(tc_set(X2)))
| ~ c_in(X0,c_Zorn_OTFin(X1,X2),tc_set(tc_set(X2))) ),
inference(cnf_transformation,[status(thm)],[f1359]) ).
fof(f2850,plain,
! [X0,X1,X2,X3] :
( c_lessequals(c_Zorn_Osucc(X1,X0,X2),X3,tc_set(tc_set(X2)))
| c_lessequals(c_Zorn_OTFin__linear__lemma1__1(X1,X0,X2),X0,tc_set(tc_set(X2)))
| c_lessequals(X3,X0,tc_set(tc_set(X2)))
| ~ c_in(X3,c_Zorn_OTFin(X1,X2),tc_set(tc_set(X2)))
| ~ c_in(X0,c_Zorn_OTFin(X1,X2),tc_set(tc_set(X2))) ),
inference(cnf_transformation,[status(thm)],[f1360]) ).
fof(f2851,plain,
! [X0,X1,X2,X3] :
( c_lessequals(c_Zorn_Osucc(X1,X0,X2),X3,tc_set(tc_set(X2)))
| c_lessequals(X3,X0,tc_set(tc_set(X2)))
| c_Zorn_OTFin__linear__lemma1__1(X1,X0,X2) != X0
| ~ c_in(X3,c_Zorn_OTFin(X1,X2),tc_set(tc_set(X2)))
| ~ c_in(X0,c_Zorn_OTFin(X1,X2),tc_set(tc_set(X2))) ),
inference(cnf_transformation,[status(thm)],[f1361]) ).
fof(f2852,plain,
! [X0,X1,X2,X3] :
( c_lessequals(c_Zorn_Osucc(X1,X0,X2),X3,tc_set(tc_set(X2)))
| c_lessequals(X3,X0,tc_set(tc_set(X2)))
| ~ c_lessequals(c_Zorn_Osucc(X1,c_Zorn_OTFin__linear__lemma1__1(X1,X0,X2),X2),X0,tc_set(tc_set(X2)))
| ~ c_in(X3,c_Zorn_OTFin(X1,X2),tc_set(tc_set(X2)))
| ~ c_in(X0,c_Zorn_OTFin(X1,X2),tc_set(tc_set(X2))) ),
inference(cnf_transformation,[status(thm)],[f1362]) ).
fof(f2859,plain,
! [V_x,V_y,T_a] :
( ! [V_S] : c_lessequals(V_x,c_Zorn_Osucc(V_S,V_y,T_a),tc_set(tc_set(T_a)))
| ~ c_lessequals(V_x,V_y,tc_set(tc_set(T_a))) ),
inference(miniscoping,[status(thm)],[f1366]) ).
fof(f2860,plain,
! [X0,X1,X2,X3] :
( c_lessequals(X0,c_Zorn_Osucc(X3,X1,X2),tc_set(tc_set(X2)))
| ~ c_lessequals(X0,X1,tc_set(tc_set(X2))) ),
inference(cnf_transformation,[status(thm)],[f2859]) ).
fof(f2861,plain,
c_in(v_x,c_Zorn_OTFin(v_S,t_a),tc_set(tc_set(t_a))),
inference(cnf_transformation,[status(thm)],[f1367]) ).
fof(f2862,plain,
c_in(v_xa,c_Zorn_OTFin(v_S,t_a),tc_set(tc_set(t_a))),
inference(cnf_transformation,[status(thm)],[f1368]) ).
fof(f2863,plain,
c_lessequals(v_xa,c_Zorn_Osucc(v_S,v_x,t_a),tc_set(tc_set(t_a))),
inference(cnf_transformation,[status(thm)],[f1369]) ).
fof(f2864,plain,
v_xa != c_Zorn_Osucc(v_S,v_x,t_a),
inference(cnf_transformation,[status(thm)],[f1370]) ).
fof(f2865,plain,
~ 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))),
inference(cnf_transformation,[status(thm)],[f1371]) ).
fof(f2866,plain,
! [X0] :
( ~ c_in(X0,c_Zorn_OTFin(v_S,t_a),tc_set(tc_set(t_a)))
| ~ c_lessequals(X0,v_x,tc_set(tc_set(t_a)))
| X0 = v_x
| c_lessequals(c_Zorn_Osucc(v_S,X0,t_a),v_x,tc_set(tc_set(t_a))) ),
inference(cnf_transformation,[status(thm)],[f1372]) ).
fof(f2867,plain,
! [X0] :
( ~ c_lessequals(v_xa,c_Zorn_Osucc(v_S,v_x,t_a),tc_set(X0))
| ~ c_lessequals(c_Zorn_Osucc(v_S,v_x,t_a),v_xa,tc_set(X0)) ),
inference(resolution,[status(thm)],[f1790,f2864]) ).
fof(f2869,plain,
~ c_lessequals(c_Zorn_Osucc(v_S,v_xa,t_a),v_x,tc_set(tc_set(t_a))),
inference(resolution,[status(thm)],[f2865,f2860]) ).
fof(f3044,plain,
( ~ c_lessequals(v_xa,c_Zorn_Osucc(v_S,v_x,t_a),tc_set(tc_set(t_a)))
| c_lessequals(v_xa,v_x,tc_set(tc_set(t_a)))
| c_Zorn_OTFin__linear__lemma1__1(v_S,v_x,t_a) != v_x
| ~ c_in(v_xa,c_Zorn_OTFin(v_S,t_a),tc_set(tc_set(t_a)))
| ~ c_in(v_x,c_Zorn_OTFin(v_S,t_a),tc_set(tc_set(t_a))) ),
inference(resolution,[status(thm)],[f2851,f2867]) ).
fof(f3046,definition,
( sQ31_spl
<=> c_in(v_x,c_Zorn_OTFin(v_S,t_a),tc_set(tc_set(t_a))) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f3048,plain,
( sQ31_spl
| ~ c_in(v_x,c_Zorn_OTFin(v_S,t_a),tc_set(tc_set(t_a))) ),
inference(component_clause,[status(thm)],[f3046]) ).
fof(f3049,definition,
( sQ32_spl
<=> c_in(v_xa,c_Zorn_OTFin(v_S,t_a),tc_set(tc_set(t_a))) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f3051,plain,
( sQ32_spl
| ~ c_in(v_xa,c_Zorn_OTFin(v_S,t_a),tc_set(tc_set(t_a))) ),
inference(component_clause,[status(thm)],[f3049]) ).
fof(f3052,definition,
( sQ33_spl
<=> c_Zorn_OTFin__linear__lemma1__1(v_S,v_x,t_a) = v_x ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f3055,definition,
( sQ34_spl
<=> c_lessequals(v_xa,v_x,tc_set(tc_set(t_a))) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f3058,definition,
( sQ35_spl
<=> c_lessequals(v_xa,c_Zorn_Osucc(v_S,v_x,t_a),tc_set(tc_set(t_a))) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f3060,plain,
( sQ35_spl
| ~ c_lessequals(v_xa,c_Zorn_Osucc(v_S,v_x,t_a),tc_set(tc_set(t_a))) ),
inference(component_clause,[status(thm)],[f3058]) ).
fof(f3061,plain,
( ~ sQ35_spl
| sQ34_spl
| ~ sQ33_spl
| ~ sQ32_spl
| ~ sQ31_spl ),
inference(split_clause,[status(thm)],[f3044,f3046,f3049,f3052,f3055,f3058]) ).
fof(f3072,plain,
( sQ32_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3051,f2862]) ).
fof(f3073,plain,
sQ32_spl,
inference(contradiction_clause,[status(thm)],[f3072]) ).
fof(f3074,plain,
( sQ35_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3060,f2863]) ).
fof(f3075,plain,
sQ35_spl,
inference(contradiction_clause,[status(thm)],[f3074]) ).
fof(f3076,plain,
( ~ c_lessequals(v_xa,c_Zorn_Osucc(v_S,v_x,t_a),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(v_xa,v_x,tc_set(tc_set(t_a)))
| ~ c_in(v_xa,c_Zorn_OTFin(v_S,t_a),tc_set(tc_set(t_a)))
| ~ c_in(v_x,c_Zorn_OTFin(v_S,t_a),tc_set(tc_set(t_a))) ),
inference(resolution,[status(thm)],[f2850,f2867]) ).
fof(f3078,definition,
( sQ39_spl
<=> c_lessequals(c_Zorn_OTFin__linear__lemma1__1(v_S,v_x,t_a),v_x,tc_set(tc_set(t_a))) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f3081,plain,
( ~ sQ35_spl
| sQ39_spl
| sQ34_spl
| ~ sQ32_spl
| ~ sQ31_spl ),
inference(split_clause,[status(thm)],[f3076,f3046,f3049,f3055,f3078,f3058]) ).
fof(f3086,plain,
( ~ c_lessequals(v_xa,c_Zorn_Osucc(v_S,v_x,t_a),tc_set(tc_set(t_a)))
| c_lessequals(v_xa,v_x,tc_set(tc_set(t_a)))
| 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_in(v_xa,c_Zorn_OTFin(v_S,t_a),tc_set(tc_set(t_a)))
| ~ c_in(v_x,c_Zorn_OTFin(v_S,t_a),tc_set(tc_set(t_a))) ),
inference(resolution,[status(thm)],[f2849,f2867]) ).
fof(f3088,definition,
( sQ41_spl
<=> 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))) ),
introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition]) ).
fof(f3091,plain,
( ~ sQ35_spl
| sQ34_spl
| sQ41_spl
| ~ sQ32_spl
| ~ sQ31_spl ),
inference(split_clause,[status(thm)],[f3086,f3046,f3049,f3088,f3055,f3058]) ).
fof(f3096,plain,
( ~ c_lessequals(v_xa,c_Zorn_Osucc(v_S,v_x,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,c_Zorn_OTFin__linear__lemma1__1(v_S,v_x,t_a),t_a),v_x,tc_set(tc_set(t_a)))
| ~ c_in(v_xa,c_Zorn_OTFin(v_S,t_a),tc_set(tc_set(t_a)))
| ~ c_in(v_x,c_Zorn_OTFin(v_S,t_a),tc_set(tc_set(t_a))) ),
inference(resolution,[status(thm)],[f2852,f2867]) ).
fof(f3098,definition,
( sQ43_spl
<=> 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))) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f3100,plain,
( sQ43_spl
| ~ 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(component_clause,[status(thm)],[f3098]) ).
fof(f3101,plain,
( ~ sQ35_spl
| sQ34_spl
| ~ sQ43_spl
| ~ sQ32_spl
| ~ sQ31_spl ),
inference(split_clause,[status(thm)],[f3096,f3046,f3049,f3098,f3055,f3058]) ).
fof(f3106,plain,
( ~ c_in(v_xa,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 = v_x ),
inference(resolution,[status(thm)],[f2869,f2866]) ).
fof(f3111,definition,
( sQ45_spl
<=> v_xa = v_x ),
introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition]) ).
fof(f3112,plain,
( ~ sQ45_spl
| v_xa = v_x ),
inference(component_clause,[status(thm)],[f3111]) ).
fof(f3114,plain,
( ~ sQ32_spl
| ~ sQ34_spl
| sQ45_spl ),
inference(split_clause,[status(thm)],[f3106,f3111,f3055,f3049]) ).
fof(f3122,plain,
( sQ31_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3048,f2861]) ).
fof(f3123,plain,
sQ31_spl,
inference(contradiction_clause,[status(thm)],[f3122]) ).
fof(f3244,plain,
( ~ sQ45_spl
| ~ c_lessequals(c_Zorn_Osucc(v_S,v_xa,t_a),c_Zorn_Osucc(v_S,v_xa,t_a),tc_set(tc_set(t_a))) ),
inference(backward_demodulation,[status(thm)],[f3112,f2865]) ).
fof(f3251,plain,
( ~ sQ45_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3244,f1791]) ).
fof(f3252,plain,
~ sQ45_spl,
inference(contradiction_clause,[status(thm)],[f3251]) ).
fof(f4113,plain,
( sQ43_spl
| ~ 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(c_Zorn_OTFin__linear__lemma1__1(v_S,v_x,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)],[f3100,f2866]) ).
fof(f4118,plain,
( sQ43_spl
| ~ sQ41_spl
| ~ sQ39_spl
| sQ33_spl ),
inference(split_clause,[status(thm)],[f4113,f3052,f3078,f3088,f3098]) ).
fof(f4138,plain,
$false,
inference(sat_refutation,[status(thm)],[f3061,f3073,f3075,f3081,f3091,f3101,f3114,f3123,f3252,f4118]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET853-1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.35 % Computer : n004.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 05:41:20 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.40 % Drodi V4.1.1
% 0.10/0.56 % Refutation found
% 0.10/0.56 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.10/0.56 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.81/0.57 % Elapsed time: 0.207615 seconds
% 0.81/0.57 % CPU time: 1.169667 seconds
% 0.81/0.57 % Total memory used: 171.519 MB
% 0.81/0.57 % Net memory used: 170.752 MB
%------------------------------------------------------------------------------