%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWV926-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n019.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 : Sun Sep 27 09:09:21 AM UTC 2026
% Result : Unsatisfiable 15.85s 2.59s
% Output : CNFRefutation 15.85s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 13
% Syntax : Number of formulae : 47 ( 27 unt; 0 def)
% Number of atoms : 74 ( 11 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 60 ( 33 ~; 27 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-3 aty)
% Number of functors : 14 ( 14 usr; 10 con; 0-3 aty)
% Number of variables : 72 ( 14 sgn 27 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(clsarity_fun__Lattices_Oupper__semilattice,axiom,
! [VAR_0,VAR_1] :
( ~ class_Lattices_Olattice(VAR_1)
| class_Lattices_Oupper__semilattice(tc_fun(VAR_0,VAR_1)) ),
file('theBenchmark.p',clsarity_fun__Lattices_Oupper__semilattice) ).
cnf(c_3,plain,
( ~ class_Lattices_Olattice(B)
| class_Lattices_Oupper__semilattice(tc_fun(A,B)) ),
inference(clausify,[status(thm)],[clsarity_fun__Lattices_Oupper__semilattice]) ).
fof(cls_le__supI1_0,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ c_lessequals(VAR_1,VAR_2,VAR_0)
| c_lessequals(VAR_1,c_Lattices_Oupper__semilattice__class_Osup(VAR_2,VAR_3,VAR_0),VAR_0)
| ~ class_Lattices_Oupper__semilattice(VAR_0) ),
file('theBenchmark.p',cls_le__supI1_0) ).
cnf(c_20,plain,
( ~ c_lessequals(B,C,A)
| c_lessequals(B,c_Lattices_Oupper__semilattice__class_Osup(C,D,A),A)
| ~ class_Lattices_Oupper__semilattice(A) ),
inference(clausify,[status(thm)],[cls_le__supI1_0]) ).
fof(cls_subset__trans_0,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ c_lessequals(VAR_0,VAR_3,tc_fun(VAR_2,tc_bool))
| ~ c_lessequals(VAR_3,VAR_1,tc_fun(VAR_2,tc_bool))
| c_lessequals(VAR_0,VAR_1,tc_fun(VAR_2,tc_bool)) ),
file('theBenchmark.p',cls_subset__trans_0) ).
cnf(c_435,plain,
( ~ c_lessequals(A,D,tc_fun(C,tc_bool))
| ~ c_lessequals(D,B,tc_fun(C,tc_bool))
| c_lessequals(A,B,tc_fun(C,tc_bool)) ),
inference(clausify,[status(thm)],[cls_subset__trans_0]) ).
fof(cls_Un__subset__iff_1,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ c_lessequals(c_Lattices_Oupper__semilattice__class_Osup(VAR_3,VAR_0,tc_fun(VAR_2,tc_bool)),VAR_1,tc_fun(VAR_2,tc_bool))
| c_lessequals(VAR_0,VAR_1,tc_fun(VAR_2,tc_bool)) ),
file('theBenchmark.p',cls_Un__subset__iff_1) ).
cnf(c_440,plain,
( ~ c_lessequals(c_Lattices_Oupper__semilattice__class_Osup(D,A,tc_fun(C,tc_bool)),B,tc_fun(C,tc_bool))
| c_lessequals(A,B,tc_fun(C,tc_bool)) ),
inference(clausify,[status(thm)],[cls_Un__subset__iff_1]) ).
fof(cls_Un__absorb1_0,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ~ c_lessequals(VAR_0,VAR_1,tc_fun(VAR_2,tc_bool))
| c_Lattices_Oupper__semilattice__class_Osup(VAR_0,VAR_1,tc_fun(VAR_2,tc_bool)) = VAR_1 ),
file('theBenchmark.p',cls_Un__absorb1_0) ).
cnf(c_447,plain,
( ~ c_lessequals(A,B,tc_fun(C,tc_bool))
| c_Lattices_Oupper__semilattice__class_Osup(A,B,tc_fun(C,tc_bool)) = B ),
inference(clausify,[status(thm)],[cls_Un__absorb1_0]) ).
fof(cls_Un__assoc_0,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] : c_Lattices_Oupper__semilattice__class_Osup(c_Lattices_Oupper__semilattice__class_Osup(VAR_0,VAR_1,tc_fun(VAR_2,tc_bool)),VAR_3,tc_fun(VAR_2,tc_bool)) = c_Lattices_Oupper__semilattice__class_Osup(VAR_0,c_Lattices_Oupper__semilattice__class_Osup(VAR_1,VAR_3,tc_fun(VAR_2,tc_bool)),tc_fun(VAR_2,tc_bool)),
file('theBenchmark.p',cls_Un__assoc_0) ).
cnf(c_464,plain,
c_Lattices_Oupper__semilattice__class_Osup(c_Lattices_Oupper__semilattice__class_Osup(A,B,tc_fun(C,tc_bool)),D,tc_fun(C,tc_bool)) = c_Lattices_Oupper__semilattice__class_Osup(A,c_Lattices_Oupper__semilattice__class_Osup(B,D,tc_fun(C,tc_bool)),tc_fun(C,tc_bool)),
inference(clausify,[status(thm)],[cls_Un__assoc_0]) ).
fof(cls_Un__upper2_0,axiom,
! [VAR_0,VAR_1,VAR_2] : c_lessequals(VAR_0,c_Lattices_Oupper__semilattice__class_Osup(VAR_1,VAR_0,tc_fun(VAR_2,tc_bool)),tc_fun(VAR_2,tc_bool)),
file('theBenchmark.p',cls_Un__upper2_0) ).
cnf(c_468,plain,
c_lessequals(A,c_Lattices_Oupper__semilattice__class_Osup(B,A,tc_fun(C,tc_bool)),tc_fun(C,tc_bool)),
inference(clausify,[status(thm)],[cls_Un__upper2_0]) ).
fof(cls_Un__upper1_0,axiom,
! [VAR_0,VAR_1,VAR_2] : c_lessequals(VAR_0,c_Lattices_Oupper__semilattice__class_Osup(VAR_0,VAR_1,tc_fun(VAR_2,tc_bool)),tc_fun(VAR_2,tc_bool)),
file('theBenchmark.p',cls_Un__upper1_0) ).
cnf(c_469,plain,
c_lessequals(A,c_Lattices_Oupper__semilattice__class_Osup(A,B,tc_fun(C,tc_bool)),tc_fun(C,tc_bool)),
inference(clausify,[status(thm)],[cls_Un__upper1_0]) ).
fof(cls_conjecture_0,axiom,
c_lessequals(v_ad,v_ab,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),
file('theBenchmark.p',cls_conjecture_0) ).
cnf(c_477,plain,
c_lessequals(v_ad,v_ab,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),
inference(clausify,[status(thm)],[cls_conjecture_0]) ).
fof(cls_conjecture_3,axiom,
c_Lattices_Oupper__semilattice__class_Osup(c_Map_Odom(v_ba,tc_List_Olist(tc_String_Ochar),tc_Value_Oval),v_ac,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)) = v_ab,
file('theBenchmark.p',cls_conjecture_3) ).
cnf(c_481,plain,
c_Lattices_Oupper__semilattice__class_Osup(c_Map_Odom(v_ba,tc_List_Olist(tc_String_Ochar),tc_Value_Oval),v_ac,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)) = v_ab,
inference(clausify,[status(thm)],[cls_conjecture_3]) ).
fof(cls_conjecture_5,axiom,
c_Lattices_Oupper__semilattice__class_Osup(c_Map_Odom(v_b,tc_List_Olist(tc_String_Ochar),tc_Value_Oval),v_ae,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)) = v_ad,
file('theBenchmark.p',cls_conjecture_5) ).
cnf(c_484,plain,
c_Lattices_Oupper__semilattice__class_Osup(c_Map_Odom(v_b,tc_List_Olist(tc_String_Ochar),tc_Value_Oval),v_ae,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)) = v_ad,
inference(clausify,[status(thm)],[cls_conjecture_5]) ).
fof(cls_conjecture_7,axiom,
( ~ c_lessequals(c_Map_Odom(v_b,tc_List_Olist(tc_String_Ochar),tc_Value_Oval),c_Lattices_Oupper__semilattice__class_Osup(c_Map_Odom(v_ba,tc_List_Olist(tc_String_Ochar),tc_Value_Oval),c_Lattices_Oupper__semilattice__class_Osup(v_ac,v_x,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool))
| ~ c_lessequals(v_ae,c_Lattices_Oupper__semilattice__class_Osup(c_Map_Odom(v_ba,tc_List_Olist(tc_String_Ochar),tc_Value_Oval),c_Lattices_Oupper__semilattice__class_Osup(v_ac,v_x,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool))
| ~ c_lessequals(v_x,c_Lattices_Oupper__semilattice__class_Osup(c_Map_Odom(v_ba,tc_List_Olist(tc_String_Ochar),tc_Value_Oval),c_Lattices_Oupper__semilattice__class_Osup(v_ac,v_x,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)) ),
file('theBenchmark.p',cls_conjecture_7) ).
cnf(c_487,plain,
( ~ c_lessequals(c_Map_Odom(v_b,tc_List_Olist(tc_String_Ochar),tc_Value_Oval),c_Lattices_Oupper__semilattice__class_Osup(c_Map_Odom(v_ba,tc_List_Olist(tc_String_Ochar),tc_Value_Oval),c_Lattices_Oupper__semilattice__class_Osup(v_ac,v_x,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool))
| ~ c_lessequals(v_ae,c_Lattices_Oupper__semilattice__class_Osup(c_Map_Odom(v_ba,tc_List_Olist(tc_String_Ochar),tc_Value_Oval),c_Lattices_Oupper__semilattice__class_Osup(v_ac,v_x,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool))
| ~ c_lessequals(v_x,c_Lattices_Oupper__semilattice__class_Osup(c_Map_Odom(v_ba,tc_List_Olist(tc_String_Ochar),tc_Value_Oval),c_Lattices_Oupper__semilattice__class_Osup(v_ac,v_x,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)) ),
inference(clausify,[status(thm)],[cls_conjecture_7]) ).
fof(clsarity_bool__Lattices_Olattice,axiom,
class_Lattices_Olattice(tc_bool),
file('theBenchmark.p',clsarity_bool__Lattices_Olattice) ).
cnf(c_501,plain,
class_Lattices_Olattice(tc_bool),
inference(clausify,[status(thm)],[clsarity_bool__Lattices_Olattice]) ).
cnf(c_519,plain,
( ~ c_lessequals(B,C,tc_fun(E,A))
| c_lessequals(B,c_Lattices_Oupper__semilattice__class_Osup(C,D,tc_fun(E,A)),tc_fun(E,A))
| ~ class_Lattices_Olattice(A) ),
inference(resolve,[status(thm)],[c_3,c_20]) ).
cnf(c_918,plain,
c_lessequals(A,c_Lattices_Oupper__semilattice__class_Osup(B,c_Lattices_Oupper__semilattice__class_Osup(C,A,tc_fun(D,tc_bool)),tc_fun(D,tc_bool)),tc_fun(D,tc_bool)),
inference(resolve,[status(thm)],[c_468,c_440]) ).
cnf(c_921,plain,
( ~ c_lessequals(c_Map_Odom(v_b,tc_List_Olist(tc_String_Ochar),tc_Value_Oval),c_Lattices_Oupper__semilattice__class_Osup(c_Map_Odom(v_ba,tc_List_Olist(tc_String_Ochar),tc_Value_Oval),c_Lattices_Oupper__semilattice__class_Osup(v_ac,v_x,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool))
| ~ c_lessequals(v_ae,c_Lattices_Oupper__semilattice__class_Osup(c_Map_Odom(v_ba,tc_List_Olist(tc_String_Ochar),tc_Value_Oval),c_Lattices_Oupper__semilattice__class_Osup(v_ac,v_x,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)) ),
inference(resolve,[status(thm)],[c_918,c_487]) ).
cnf(c_942,plain,
c_Lattices_Oupper__semilattice__class_Osup(v_ad,v_ab,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)) = v_ab,
inference(resolve,[status(thm)],[c_477,c_447]) ).
cnf(c_952,plain,
( ~ c_lessequals(A,v_ad,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool))
| c_lessequals(A,v_ab,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)) ),
inference(resolve,[status(thm)],[c_477,c_435]) ).
cnf(c_6987,plain,
c_Lattices_Oupper__semilattice__class_Osup(v_ab,A,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)) = c_Lattices_Oupper__semilattice__class_Osup(c_Map_Odom(v_ba,tc_List_Olist(tc_String_Ochar),tc_Value_Oval),c_Lattices_Oupper__semilattice__class_Osup(v_ac,A,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),
inference(paramod,[status(thm)],[c_481,c_464]) ).
cnf(c_994,plain,
c_Lattices_Oupper__semilattice__class_Osup(c_Map_Odom(v_ba,tc_List_Olist(tc_String_Ochar),tc_Value_Oval),c_Lattices_Oupper__semilattice__class_Osup(v_ac,A,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)) = c_Lattices_Oupper__semilattice__class_Osup(v_ab,A,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),
inference(copy,[status(thm)],[c_6987]) ).
cnf(c_6988,plain,
( ~ c_lessequals(c_Map_Odom(v_b,tc_List_Olist(tc_String_Ochar),tc_Value_Oval),c_Lattices_Oupper__semilattice__class_Osup(c_Map_Odom(v_ba,tc_List_Olist(tc_String_Ochar),tc_Value_Oval),c_Lattices_Oupper__semilattice__class_Osup(v_ac,v_x,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool))
| ~ c_lessequals(v_ae,c_Lattices_Oupper__semilattice__class_Osup(v_ab,v_x,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)) ),
inference(paramod,[status(thm)],[c_994,c_921]) ).
cnf(c_999,plain,
( ~ c_lessequals(c_Map_Odom(v_b,tc_List_Olist(tc_String_Ochar),tc_Value_Oval),c_Lattices_Oupper__semilattice__class_Osup(v_ab,v_x,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool))
| ~ c_lessequals(v_ae,c_Lattices_Oupper__semilattice__class_Osup(v_ab,v_x,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)) ),
inference(paramod,[status(thm)],[c_994,c_6988]) ).
cnf(c_1037,plain,
c_lessequals(v_ae,v_ad,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),
inference(paramod,[status(thm)],[c_484,c_468]) ).
cnf(c_1038,plain,
c_lessequals(c_Map_Odom(v_b,tc_List_Olist(tc_String_Ochar),tc_Value_Oval),v_ad,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),
inference(paramod,[status(thm)],[c_484,c_469]) ).
cnf(c_6989,plain,
( c_lessequals(v_ae,c_Lattices_Oupper__semilattice__class_Osup(v_ad,A,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool))
| ~ class_Lattices_Olattice(tc_bool) ),
inference(resolve,[status(thm)],[c_1037,c_519]) ).
cnf(c_1407,plain,
c_lessequals(v_ae,c_Lattices_Oupper__semilattice__class_Osup(v_ad,A,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),
inference(resolve,[status(thm)],[c_501,c_6989]) ).
cnf(c_4732,plain,
c_lessequals(v_ae,v_ab,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),
inference(paramod,[status(thm)],[c_942,c_1407]) ).
cnf(c_6990,plain,
( c_lessequals(v_ae,c_Lattices_Oupper__semilattice__class_Osup(v_ab,A,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool))
| ~ class_Lattices_Olattice(tc_bool) ),
inference(resolve,[status(thm)],[c_4732,c_519]) ).
cnf(c_4742,plain,
c_lessequals(v_ae,c_Lattices_Oupper__semilattice__class_Osup(v_ab,A,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),
inference(resolve,[status(thm)],[c_501,c_6990]) ).
cnf(c_4757,plain,
~ c_lessequals(c_Map_Odom(v_b,tc_List_Olist(tc_String_Ochar),tc_Value_Oval),c_Lattices_Oupper__semilattice__class_Osup(v_ab,v_x,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),
inference(resolve,[status(thm)],[c_4742,c_999]) ).
cnf(c_6984,plain,
c_lessequals(c_Map_Odom(v_b,tc_List_Olist(tc_String_Ochar),tc_Value_Oval),v_ab,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),
inference(resolve,[status(thm)],[c_952,c_1038]) ).
cnf(c_6991,plain,
( c_lessequals(c_Map_Odom(v_b,tc_List_Olist(tc_String_Ochar),tc_Value_Oval),c_Lattices_Oupper__semilattice__class_Osup(v_ab,A,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool))
| ~ class_Lattices_Olattice(tc_bool) ),
inference(resolve,[status(thm)],[c_6984,c_519]) ).
cnf(c_6985,plain,
c_lessequals(c_Map_Odom(v_b,tc_List_Olist(tc_String_Ochar),tc_Value_Oval),c_Lattices_Oupper__semilattice__class_Osup(v_ab,A,tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),tc_fun(tc_List_Olist(tc_String_Ochar),tc_bool)),
inference(resolve,[status(thm)],[c_501,c_6991]) ).
cnf(c_6986,plain,
$false,
inference(resolve,[status(thm)],[c_6985,c_4757]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV926-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n019.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sat Sep 26 15:10:33 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.38 % Process 1624022 was started by sandbox2 on n019,
% 0.10/0.38 % Sat Sep 26 15:10:33 2026
% 0.10/0.38 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.10/0.41
% 0.10/0.41 % From the command line: assign(max_seconds, 300).
% 15.85/2.59
% 15.85/2.59 % given #500 (F,wt=3): 1625 -hBOOL(c_Orderings_Obot__class_Obot(tc_bool)). [para(1102(a,1),161(a,1))].
% 15.85/2.59
% 15.85/2.59 % SZS status Unsatisfiable for theBenchmark
% 15.85/2.59
% 15.85/2.59 % Proof 1 at 1.97 (+ 0.17) seconds.
% 15.85/2.59 % Length of proof is 29.
% 15.85/2.59 % Level of proof is 6.
% 15.85/2.59 % Maximum clause weight is 73.000.
% 15.85/2.59 % Given clauses 810.
% 15.85/2.59
% 15.85/2.59 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------