%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1.1
% Problem : LCL442-2 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox/solver/bin/SPASS-SCL-FOL -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n016.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 : Mon Sep 7 01:09:35 PM UTC 2026
% Result : Unsatisfiable 0.80s 1.09s
% Output : Proof 0.80s
% Verified :
% SZS Type : Refutation
% Derivation depth : 3
% Number of leaves : 12
% Syntax : Number of clauses : 19 ( 3 unt; 3 nHn; 11 RR)
% Number of literals : 39 ( 0 equ; 20 neg)
% Maximal clause size : 3 ( 2 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 3 ( 2 usr; 1 prp; 0-3 aty)
% Number of functors : 10 ( 10 usr; 5 con; 0-3 aty)
% Number of variables : 30 ( 8 sgn)
% Comments :
%------------------------------------------------------------------------------
% FILE RECORD
cnf(cls_PropLog_Oweaken__left__Un1_0,axiom,
( ~ c_in(X0,c_PropLog_Othms(X1,X2),tc_PropLog_Opl(X2))
| c_in(X0,c_PropLog_Othms(c_union(X1,X3,tc_PropLog_Opl(X2)),X2),tc_PropLog_Opl(X2)) ),
file('theBenchmark.p',cls_PropLog_Oweaken__left__Un1_0) ).
% FILE RECORD
cnf(cls_PropLog_Ofalse__imp_0,axiom,
( ~ c_in(c_PropLog_Opl_Oop_A_N_62(X0,c_PropLog_Opl_Ofalse,X1),c_PropLog_Othms(X2,X1),tc_PropLog_Opl(X1))
| c_in(c_PropLog_Opl_Oop_A_N_62(X0,X3,X1),c_PropLog_Othms(X2,X1),tc_PropLog_Opl(X1)) ),
file('theBenchmark.p',cls_PropLog_Ofalse__imp_0) ).
% FILE RECORD
cnf(cls_conjecture_1,negated_conjecture,
( c_in(c_PropLog_Opl_Oop_A_N_62(v_pl1,c_PropLog_Opl_Ofalse,t_a),c_PropLog_Othms(c_PropLog_Ohyps(v_pl1,v_tt,t_a),t_a),tc_PropLog_Opl(t_a))
| c_PropLog_Oeval(v_tt,v_pl1,t_a) ),
file('theBenchmark.p',cls_conjecture_1) ).
% FILE RECORD
cnf(cls_PropLog_Oweaken__left__Un2_0,axiom,
( ~ c_in(X0,c_PropLog_Othms(X1,X2),tc_PropLog_Opl(X2))
| c_in(X0,c_PropLog_Othms(c_union(X3,X1,tc_PropLog_Opl(X2)),X2),tc_PropLog_Opl(X2)) ),
file('theBenchmark.p',cls_PropLog_Oweaken__left__Un2_0) ).
% FILE RECORD
cnf(cls_PropLog_Oimp__false_0,axiom,
( ~ c_in(X0,c_PropLog_Othms(X1,X2),tc_PropLog_Opl(X2))
| ~ c_in(c_PropLog_Opl_Oop_A_N_62(X3,c_PropLog_Opl_Ofalse,X2),c_PropLog_Othms(X1,X2),tc_PropLog_Opl(X2))
| c_in(c_PropLog_Opl_Oop_A_N_62(c_PropLog_Opl_Oop_A_N_62(X0,X3,X2),c_PropLog_Opl_Ofalse,X2),c_PropLog_Othms(X1,X2),tc_PropLog_Opl(X2)) ),
file('theBenchmark.p',cls_PropLog_Oimp__false_0) ).
% CNF SPASS RESOLUTION.
cnf(c_17,plain,
( ~ c_in(X0,c_PropLog_Othms(X1,X2),tc_PropLog_Opl(X2))
| ~ c_in(c_PropLog_Opl_Oop_A_N_62(X3,c_PropLog_Opl_Ofalse,X2),c_PropLog_Othms(X1,X2),tc_PropLog_Opl(X2))
| c_in(c_PropLog_Opl_Oop_A_N_62(c_PropLog_Opl_Oop_A_N_62(X0,X3,X2),X4,X2),c_PropLog_Othms(X1,X2),tc_PropLog_Opl(X2)) ),
inference(resolution,[status(thm)],[cls_PropLog_Oimp__false_0,cls_PropLog_Ofalse__imp_0]) ).
% FILE RECORD
cnf(cls_conjecture_0,negated_conjecture,
( ~ c_PropLog_Oeval(v_tt,v_pl1,t_a)
| c_in(v_pl1,c_PropLog_Othms(c_PropLog_Ohyps(v_pl1,v_tt,t_a),t_a),tc_PropLog_Opl(t_a)) ),
file('theBenchmark.p',cls_conjecture_0) ).
% CNF SPASS RESOLUTION.
cnf(c_21,plain,
( ~ c_in(c_PropLog_Opl_Oop_A_N_62(X0,c_PropLog_Opl_Ofalse,t_a),c_PropLog_Othms(X1,t_a),tc_PropLog_Opl(t_a))
| ~ c_PropLog_Oeval(v_tt,v_pl1,t_a)
| c_in(c_PropLog_Opl_Oop_A_N_62(c_PropLog_Opl_Oop_A_N_62(v_pl1,X0,t_a),X2,t_a),c_PropLog_Othms(c_union(c_PropLog_Ohyps(v_pl1,v_tt,t_a),X1,tc_PropLog_Opl(t_a)),t_a),tc_PropLog_Opl(t_a)) ),
inference(resolution,[status(thm)],[cls_PropLog_Oweaken__left__Un2_0,c_17,cls_PropLog_Oweaken__left__Un1_0,cls_conjecture_0]) ).
% FILE RECORD
cnf(cls_conjecture_5,negated_conjecture,
( ~ c_PropLog_Oeval(v_tt,v_pl2,t_a)
| ~ c_in(c_PropLog_Opl_Oop_A_N_62(v_pl1,v_pl2,t_a),c_PropLog_Othms(c_union(c_PropLog_Ohyps(v_pl1,v_tt,t_a),c_PropLog_Ohyps(v_pl2,v_tt,t_a),tc_PropLog_Opl(t_a)),t_a),tc_PropLog_Opl(t_a)) ),
file('theBenchmark.p',cls_conjecture_5) ).
% FILE RECORD
cnf(cls_PropLog_Oweaken__right_0,axiom,
( ~ c_in(X0,c_PropLog_Othms(X1,X2),tc_PropLog_Opl(X2))
| c_in(c_PropLog_Opl_Oop_A_N_62(X3,X0,X2),c_PropLog_Othms(X1,X2),tc_PropLog_Opl(X2)) ),
file('theBenchmark.p',cls_PropLog_Oweaken__right_0) ).
% FILE RECORD
cnf(cls_conjecture_2,negated_conjecture,
( ~ c_PropLog_Oeval(v_tt,v_pl2,t_a)
| c_in(v_pl2,c_PropLog_Othms(c_PropLog_Ohyps(v_pl2,v_tt,t_a),t_a),tc_PropLog_Opl(t_a)) ),
file('theBenchmark.p',cls_conjecture_2) ).
% CNF SPASS RESOLUTION.
cnf(c_13,plain,
~ c_PropLog_Oeval(v_tt,v_pl2,t_a),
inference(resolution,[status(thm)],[cls_PropLog_Oweaken__left__Un2_0,cls_conjecture_5,cls_PropLog_Oweaken__right_0,cls_conjecture_2]) ).
% FILE RECORD
cnf(cls_conjecture_9,negated_conjecture,
( ~ c_in(c_PropLog_Opl_Oop_A_N_62(c_PropLog_Opl_Oop_A_N_62(v_pl1,v_pl2,t_a),c_PropLog_Opl_Ofalse,t_a),c_PropLog_Othms(c_union(c_PropLog_Ohyps(v_pl1,v_tt,t_a),c_PropLog_Ohyps(v_pl2,v_tt,t_a),tc_PropLog_Opl(t_a)),t_a),tc_PropLog_Opl(t_a))
| ~ c_PropLog_Oeval(v_tt,v_pl1,t_a)
| c_PropLog_Oeval(v_tt,v_pl2,t_a) ),
file('theBenchmark.p',cls_conjecture_9) ).
% CNF SPASS RESOLUTION.
cnf(c_16,plain,
( ~ c_in(c_PropLog_Opl_Oop_A_N_62(c_PropLog_Opl_Oop_A_N_62(v_pl1,v_pl2,t_a),c_PropLog_Opl_Ofalse,t_a),c_PropLog_Othms(c_union(c_PropLog_Ohyps(v_pl1,v_tt,t_a),c_PropLog_Ohyps(v_pl2,v_tt,t_a),tc_PropLog_Opl(t_a)),t_a),tc_PropLog_Opl(t_a))
| ~ c_PropLog_Oeval(v_tt,v_pl1,t_a) ),
inference(resolution,[status(thm)],[c_13,cls_conjecture_9]) ).
% FILE RECORD
cnf(cls_conjecture_3,negated_conjecture,
( c_in(c_PropLog_Opl_Oop_A_N_62(v_pl2,c_PropLog_Opl_Ofalse,t_a),c_PropLog_Othms(c_PropLog_Ohyps(v_pl2,v_tt,t_a),t_a),tc_PropLog_Opl(t_a))
| c_PropLog_Oeval(v_tt,v_pl2,t_a) ),
file('theBenchmark.p',cls_conjecture_3) ).
% CNF SPASS RESOLUTION.
cnf(c_14,plain,
( c_in(c_PropLog_Opl_Oop_A_N_62(v_pl2,X0,t_a),c_PropLog_Othms(c_PropLog_Ohyps(v_pl2,v_tt,t_a),t_a),tc_PropLog_Opl(t_a))
| c_PropLog_Oeval(v_tt,v_pl2,t_a) ),
inference(resolution,[status(thm)],[cls_PropLog_Ofalse__imp_0,cls_conjecture_3]) ).
% CNF SPASS RESOLUTION.
cnf(c_15,plain,
c_in(c_PropLog_Opl_Oop_A_N_62(v_pl2,X0,t_a),c_PropLog_Othms(c_PropLog_Ohyps(v_pl2,v_tt,t_a),t_a),tc_PropLog_Opl(t_a)),
inference(resolution,[status(thm)],[c_13,c_14]) ).
% FILE RECORD
cnf(cls_conjecture_4,negated_conjecture,
( ~ c_in(c_PropLog_Opl_Oop_A_N_62(v_pl1,v_pl2,t_a),c_PropLog_Othms(c_union(c_PropLog_Ohyps(v_pl1,v_tt,t_a),c_PropLog_Ohyps(v_pl2,v_tt,t_a),tc_PropLog_Opl(t_a)),t_a),tc_PropLog_Opl(t_a))
| c_PropLog_Oeval(v_tt,v_pl1,t_a) ),
file('theBenchmark.p',cls_conjecture_4) ).
% CNF SPASS RESOLUTION.
cnf(c_25,plain,
$false,
inference(byPropositionalAbstraction,[status(thm)],[cls_PropLog_Oweaken__left__Un1_0,cls_PropLog_Ofalse__imp_0,cls_conjecture_1,c_21,c_16,c_15,cls_conjecture_4]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL442-2 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.04 % Command : /export/starexec/sandbox/solver/bin/SPASS-SCL-FOL -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n016.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sat Sep 5 20:38:45 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running /export/starexec/sandbox/solver/bin/SPASS-SCL-FOL -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.14/0.36
% 0.14/0.36 % Input Clauses:
% 0.14/0.36 % 1:2:0:INP:: c_PropLog_Oeval(v_tt,v_pl1,t_a) -> c_in(v_pl1,c_PropLog_Othms(c_PropLog_Ohyps(v_pl1,v_tt,t_a),t_a),tc_PropLog_Opl(t_a))
% 0.14/0.36 % 2:2:0:INP:: -> c_in(c_PropLog_Opl_Oop_A_N_62(v_pl1,c_PropLog_Opl_Ofalse,t_a),c_PropLog_Othms(c_PropLog_Ohyps(v_pl1,v_tt,t_a),t_a),tc_PropLog_Opl(t_a)),c_PropLog_Oeval(v_tt,v_pl1,t_a)
% 0.14/0.36 % 3:2:0:INP:: c_PropLog_Oeval(v_tt,v_pl2,t_a) -> c_in(v_pl2,c_PropLog_Othms(c_PropLog_Ohyps(v_pl2,v_tt,t_a),t_a),tc_PropLog_Opl(t_a))
% 0.14/0.36 % 4:2:0:INP:: -> c_in(c_PropLog_Opl_Oop_A_N_62(v_pl2,c_PropLog_Opl_Ofalse,t_a),c_PropLog_Othms(c_PropLog_Ohyps(v_pl2,v_tt,t_a),t_a),tc_PropLog_Opl(t_a)),c_PropLog_Oeval(v_tt,v_pl2,t_a)
% 0.14/0.36 % 5:2:0:INP:: c_in(c_PropLog_Opl_Oop_A_N_62(v_pl1,v_pl2,t_a),c_PropLog_Othms(c_union(c_PropLog_Ohyps(v_pl1,v_tt,t_a),c_PropLog_Ohyps(v_pl2,v_tt,t_a),tc_PropLog_Opl(t_a)),t_a),tc_PropLog_Opl(t_a)) -> c_PropLog_Oeval(v_tt,v_pl1,t_a)
% 0.14/0.36 % 6:2:0:INP:: c_PropLog_Oeval(v_tt,v_pl2,t_a),c_in(c_PropLog_Opl_Oop_A_N_62(v_pl1,v_pl2,t_a),c_PropLog_Othms(c_union(c_PropLog_Ohyps(v_pl1,v_tt,t_a),c_PropLog_Ohyps(v_pl2,v_tt,t_a),tc_PropLog_Opl(t_a)),t_a),tc_PropLog_Opl(t_a)) ->
% 0.14/0.36 % 7:3:0:INP:: c_in(c_PropLog_Opl_Oop_A_N_62(c_PropLog_Opl_Oop_A_N_62(v_pl1,v_pl2,t_a),c_PropLog_Opl_Ofalse,t_a),c_PropLog_Othms(c_union(c_PropLog_Ohyps(v_pl1,v_tt,t_a),c_PropLog_Ohyps(v_pl2,v_tt,t_a),tc_PropLog_Opl(t_a)),t_a),tc_PropLog_Opl(t_a)),c_PropLog_Oeval(v_tt,v_pl1,t_a) -> c_PropLog_Oeval(v_tt,v_pl2,t_a)
% 0.14/0.36 % 8:2:4:INP:TopTopTopTop: c_in(c_PropLog_Opl_Oop_A_N_62(x0,c_PropLog_Opl_Ofalse,x1),c_PropLog_Othms(x2,x1),tc_PropLog_Opl(x1)) -> c_in(c_PropLog_Opl_Oop_A_N_62(x0,x3,x1),c_PropLog_Othms(x2,x1),tc_PropLog_Opl(x1))
% 0.14/0.36 % 9:3:4:INP:TopTopTopTop: c_in(x0,c_PropLog_Othms(x1,x2),tc_PropLog_Opl(x2)),c_in(c_PropLog_Opl_Oop_A_N_62(x3,c_PropLog_Opl_Ofalse,x2),c_PropLog_Othms(x1,x2),tc_PropLog_Opl(x2)) -> c_in(c_PropLog_Opl_Oop_A_N_62(c_PropLog_Opl_Oop_A_N_62(x0,x3,x2),c_PropLog_Opl_Ofalse,x2),c_PropLog_Othms(x1,x2),tc_PropLog_Opl(x2))
% 0.14/0.36 % 10:2:4:INP:TopTopTopTop: c_in(x0,c_PropLog_Othms(x1,x2),tc_PropLog_Opl(x2)) -> c_in(x0,c_PropLog_Othms(c_union(x1,x3,tc_PropLog_Opl(x2)),x2),tc_PropLog_Opl(x2))
% 0.14/0.36 % 11:2:4:INP:TopTopTopTop: c_in(x0,c_PropLog_Othms(x1,x2),tc_PropLog_Opl(x2)) -> c_in(x0,c_PropLog_Othms(c_union(x3,x1,tc_PropLog_Opl(x2)),x2),tc_PropLog_Opl(x2))
% 0.14/0.36 % 12:2:4:INP:TopTopTopTop: c_in(x0,c_PropLog_Othms(x1,x2),tc_PropLog_Opl(x2)) -> c_in(c_PropLog_Opl_Oop_A_N_62(x3,x0,x2),c_PropLog_Othms(x1,x2),tc_PropLog_Opl(x2))
% 0.14/0.36
% 0.14/0.36 % Predicates: c_in c_PropLog_Oeval
% 0.14/0.36 % Fol Constants: v_pl1 v_tt t_a c_PropLog_Opl_Ofalse v_pl2
% 0.14/0.36 % Fol Functions: c_PropLog_Ohyps c_PropLog_Othms tc_PropLog_Opl c_PropLog_Opl_Oop_A_N_62 c_union
% 0.14/0.36 % Problem Properties:
% 0.14/0.36 % This is a full first-order problem without equality. The Problem is non-linear.
% 0.14/0.36
% 0.14/0.36
% 0.14/0.36 % Reduced Input Axiom Clauses:
% 0.14/0.36 % 8:2:4:INP:TopTopTopTop: c_in(c_PropLog_Opl_Oop_A_N_62(x0,c_PropLog_Opl_Ofalse,x1),c_PropLog_Othms(x2,x1),tc_PropLog_Opl(x1)) -> c_in(c_PropLog_Opl_Oop_A_N_62(x0,x3,x1),c_PropLog_Othms(x2,x1),tc_PropLog_Opl(x1))
% 0.14/0.36 % 9:3:4:INP:TopTopTopTop: c_in(x0,c_PropLog_Othms(x1,x2),tc_PropLog_Opl(x2)),c_in(c_PropLog_Opl_Oop_A_N_62(x3,c_PropLog_Opl_Ofalse,x2),c_PropLog_Othms(x1,x2),tc_PropLog_Opl(x2)) -> c_in(c_PropLog_Opl_Oop_A_N_62(c_PropLog_Opl_Oop_A_N_62(x0,x3,x2),c_PropLog_Opl_Ofalse,x2),c_PropLog_Othms(x1,x2),tc_PropLog_Opl(x2))
% 0.14/0.36 % 10:2:4:INP:TopTopTopTop: c_in(x0,c_PropLog_Othms(x1,x2),tc_PropLog_Opl(x2)) -> c_in(x0,c_PropLog_Othms(c_union(x1,x3,tc_PropLog_Opl(x2)),x2),tc_PropLog_Opl(x2))
% 0.14/0.36 % 11:2:4:INP:TopTopTopTop: c_in(x0,c_PropLog_Othms(x1,x2),tc_PropLog_Opl(x2)) -> c_in(x0,c_PropLog_Othms(c_union(x3,x1,tc_PropLog_Opl(x2)),x2),tc_PropLog_Opl(x2))
% 0.14/0.36 % 12:2:4:INP:TopTopTopTop: c_in(x0,c_PropLog_Othms(x1,x2),tc_PropLog_Opl(x2)) -> c_in(c_PropLog_Opl_Oop_A_N_62(x3,x0,x2),c_PropLog_Othms(x1,x2),tc_PropLog_Opl(x2))
% 0.14/0.36
% 0.14/0.36 % Reduced Input Conjecture Clauses:
% 0.14/0.36 % 1:2:0:INP:: c_PropLog_Oeval(v_tt,v_pl1,t_a) -> c_in(v_pl1,c_PropLog_Othms(c_PropLog_Ohyps(v_pl1,v_tt,t_a),t_a),tc_PropLog_Opl(t_a))
% 0.14/0.36 % 2:2:0:INP:: -> c_in(c_PropLog_Opl_Oop_A_N_62(v_pl1,c_PropLog_Opl_Ofalse,t_a),c_PropLog_Othms(c_PropLog_Ohyps(v_pl1,v_tt,t_a),t_a),tc_PropLog_Opl(t_a)),c_PropLog_Oeval(v_tt,v_pl1,t_a)
% 0.80/1.09 % 3:2:0:INP:: c_PropLog_Oeval(v_tt,v_pl2,t_a) -> c_in(v_pl2,c_PropLog_Othms(c_PropLog_Ohyps(v_pl2,v_tt,t_a),t_a),tc_PropLog_Opl(t_a))
% 0.80/1.09 % 4:2:0:INP:: -> c_in(c_PropLog_Opl_Oop_A_N_62(v_pl2,c_PropLog_Opl_Ofalse,t_a),c_PropLog_Othms(c_PropLog_Ohyps(v_pl2,v_tt,t_a),t_a),tc_PropLog_Opl(t_a)),c_PropLog_Oeval(v_tt,v_pl2,t_a)
% 0.80/1.09 % 5:2:0:INP:: c_in(c_PropLog_Opl_Oop_A_N_62(v_pl1,v_pl2,t_a),c_PropLog_Othms(c_union(c_PropLog_Ohyps(v_pl1,v_tt,t_a),c_PropLog_Ohyps(v_pl2,v_tt,t_a),tc_PropLog_Opl(t_a)),t_a),tc_PropLog_Opl(t_a)) -> c_PropLog_Oeval(v_tt,v_pl1,t_a)
% 0.80/1.09 % 6:2:0:INP:: c_PropLog_Oeval(v_tt,v_pl2,t_a),c_in(c_PropLog_Opl_Oop_A_N_62(v_pl1,v_pl2,t_a),c_PropLog_Othms(c_union(c_PropLog_Ohyps(v_pl1,v_tt,t_a),c_PropLog_Ohyps(v_pl2,v_tt,t_a),tc_PropLog_Opl(t_a)),t_a),tc_PropLog_Opl(t_a)) ->
% 0.80/1.09 % 7:3:0:INP:: c_in(c_PropLog_Opl_Oop_A_N_62(c_PropLog_Opl_Oop_A_N_62(v_pl1,v_pl2,t_a),c_PropLog_Opl_Ofalse,t_a),c_PropLog_Othms(c_union(c_PropLog_Ohyps(v_pl1,v_tt,t_a),c_PropLog_Ohyps(v_pl2,v_tt,t_a),tc_PropLog_Opl(t_a)),t_a),tc_PropLog_Opl(t_a)),c_PropLog_Oeval(v_tt,v_pl1,t_a) -> c_PropLog_Oeval(v_tt,v_pl2,t_a)
% 0.80/1.09
% 0.80/1.09
% 0.80/1.09 % === Starting SPASS-SCL-FOL A Little Less Naive, considering 26 atoms initially. Used heuristic: lmodel_grow ===
% 0.80/1.09
% 0.80/1.09 %
% 0.80/1.09
% 0.80/1.09 % === SAT Conflict found: 25:0:0:[10.0,8.0,2.0,21.0,16.0,15.0,5.0]:: ->
% 0.80/1.09
% 0.80/1.09 % SZS status Unsatisfiable
% 0.80/1.09 % Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.80/1.09
% 0.80/1.09 % SPASS-SCL-FOL Statistics:
% 0.80/1.09 % Number of learned clauses: 10
% 0.80/1.09 % Number of propagations: 2169
% 0.80/1.09 % Number of decisions: 1144
% 0.80/1.09 % Number of resolutions: 19
% 0.80/1.09 % Number of condensations: 0
% 0.80/1.09 % Number of sub resolutions: 2
% 0.80/1.09
% 0.80/1.09 % Solver is done. Empty clause found
% 0.80/1.09
% 0.80/1.09 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 0.80/1.09 % SZS output start Proof for theBenchmark
% See solution above
% 0.80/1.09 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 0.80/1.09
% 0.80/1.09
% 0.80/1.09 % Needed: 0:00:00.72
% 0.80/1.09
% 0.80/1.09 % ###
% 0.80/1.09 % ### Pagesize: 8192
% 0.80/1.09 % ### Marksize: 0
% 0.80/1.09 % ### Memory demanded: 15314 KBytes
% 0.80/1.09 % ### Memory freed: 15314 KBytes
% 0.80/1.09 % ### Memory remaining: 0 Bytes
% 0.80/1.09 % ### Pages allocated: 1941 Pages
% 0.80/1.09 % ###
%------------------------------------------------------------------------------