%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SEU305+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n011.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 : Fri Sep 25 02:56:34 PM UTC 2026
% Result : Theorem 51.09s 7.84s
% Output : CNFRefutation 51.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 6
% Syntax : Number of formulae : 74 ( 36 unt; 2 def)
% Number of atoms : 296 ( 64 equ)
% Maximal formula atoms : 8 ( 4 avg)
% Number of connectives : 288 ( 116 ~; 119 |; 37 &)
% ( 3 <=>; 13 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 5 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 10 ( 8 usr; 4 prp; 0-3 aty)
% Number of functors : 6 ( 6 usr; 3 con; 0-3 aty)
% Number of variables : 91 ( 0 sgn 85 !; 6 ?; 40 :)
% Comments :
%------------------------------------------------------------------------------
fof(f19,axiom,
! [X0,X1,X2] :
( ( element(X2,the_carrier(X0))
& element(X1,the_carrier(X0))
& join_semilatt_str(X0)
& join_commutative(X0)
& ~ empty_carrier(X0) )
=> join_commut(X0,X1,X2) = join_commut(X0,X2,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutativity_k3_lattices) ).
fof(f59,axiom,
! [X0] :
( ( join_semilatt_str(X0)
& ~ empty_carrier(X0) )
=> ! [X1] :
( element(X1,the_carrier(X0))
=> ! [X2] :
( element(X2,the_carrier(X0))
=> ( below(X0,X1,X2)
<=> join(X0,X1,X2) = X2 ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d3_lattices) ).
fof(f247,axiom,
! [X0,X1,X2] :
( ( element(X2,the_carrier(X0))
& element(X1,the_carrier(X0))
& join_semilatt_str(X0)
& join_commutative(X0)
& ~ empty_carrier(X0) )
=> join_commut(X0,X1,X2) = join(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k3_lattices) ).
fof(f352,conjecture,
! [X0] :
( ( join_semilatt_str(X0)
& join_commutative(X0)
& ~ empty_carrier(X0) )
=> ! [X1] :
( element(X1,the_carrier(X0))
=> ! [X2] :
( element(X2,the_carrier(X0))
=> ( ( below(X0,X2,X1)
& below(X0,X1,X2) )
=> X1 = X2 ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t26_lattices) ).
fof(f353,negated_conjecture,
~ ! [X0] :
( ( join_semilatt_str(X0)
& join_commutative(X0)
& ~ empty_carrier(X0) )
=> ! [X1] :
( element(X1,the_carrier(X0))
=> ! [X2] :
( element(X2,the_carrier(X0))
=> ( ( below(X0,X2,X1)
& below(X0,X1,X2) )
=> X1 = X2 ) ) ) ),
inference(negated_conjecture,[status(cth)],[f352]) ).
fof(f511,plain,
! [X0,X1,X2] :
( ~ element(X2,the_carrier(X0))
| ~ element(X1,the_carrier(X0))
| ~ join_semilatt_str(X0)
| ~ join_commutative(X0)
| empty_carrier(X0)
| join_commut(X0,X1,X2) = join_commut(X0,X2,X1) ),
inference(ennf_transformation,[],[f19]) ).
fof(f512,plain,
! [X0,X1,X2] :
( ~ element(X2,the_carrier(X0))
| ~ element(X1,the_carrier(X0))
| ~ join_semilatt_str(X0)
| ~ join_commutative(X0)
| empty_carrier(X0)
| join_commut(X0,X1,X2) = join_commut(X0,X2,X1) ),
inference(flattening,[],[f511]) ).
fof(f548,plain,
! [X0] :
( ~ join_semilatt_str(X0)
| empty_carrier(X0)
| ! [X1] :
( ~ element(X1,the_carrier(X0))
| ! [X2] :
( ~ element(X2,the_carrier(X0))
| ( below(X0,X1,X2)
<=> join(X0,X1,X2) = X2 ) ) ) ),
inference(ennf_transformation,[],[f59]) ).
fof(f549,plain,
! [X0] :
( ~ join_semilatt_str(X0)
| empty_carrier(X0)
| ! [X1] :
( ~ element(X1,the_carrier(X0))
| ! [X2] :
( ~ element(X2,the_carrier(X0))
| ( below(X0,X1,X2)
<=> join(X0,X1,X2) = X2 ) ) ) ),
inference(flattening,[],[f548]) ).
fof(f688,plain,
! [X0,X1,X2] :
( ~ element(X2,the_carrier(X0))
| ~ element(X1,the_carrier(X0))
| ~ join_semilatt_str(X0)
| ~ join_commutative(X0)
| empty_carrier(X0)
| join_commut(X0,X1,X2) = join(X0,X1,X2) ),
inference(ennf_transformation,[],[f247]) ).
fof(f689,plain,
! [X0,X1,X2] :
( ~ element(X2,the_carrier(X0))
| ~ element(X1,the_carrier(X0))
| ~ join_semilatt_str(X0)
| ~ join_commutative(X0)
| empty_carrier(X0)
| join_commut(X0,X1,X2) = join(X0,X1,X2) ),
inference(flattening,[],[f688]) ).
fof(f837,plain,
? [X0] :
( join_semilatt_str(X0)
& join_commutative(X0)
& ~ empty_carrier(X0)
& ? [X1] :
( element(X1,the_carrier(X0))
& ? [X2] :
( element(X2,the_carrier(X0))
& below(X0,X2,X1)
& below(X0,X1,X2)
& X1 != X2 ) ) ),
inference(ennf_transformation,[],[f353]) ).
fof(f838,plain,
? [X0] :
( join_semilatt_str(X0)
& join_commutative(X0)
& ~ empty_carrier(X0)
& ? [X1] :
( element(X1,the_carrier(X0))
& ? [X2] :
( element(X2,the_carrier(X0))
& below(X0,X2,X1)
& below(X0,X1,X2)
& X1 != X2 ) ) ),
inference(flattening,[],[f837]) ).
fof(f1103,plain,
! [X0] :
( ~ join_semilatt_str(X0)
| empty_carrier(X0)
| ! [X1] :
( ~ element(X1,the_carrier(X0))
| ! [X2] :
( ~ element(X2,the_carrier(X0))
| ( ( ~ below(X0,X1,X2)
| join(X0,X1,X2) = X2 )
& ( join(X0,X1,X2) != X2
| below(X0,X1,X2) ) ) ) ) ),
inference(nnf_transformation,[],[f549]) ).
fof(f1428,plain,
( join_semilatt_str(sK336)
& join_commutative(sK336)
& ~ empty_carrier(sK336)
& element(sK337,the_carrier(sK336))
& element(sK338,the_carrier(sK336))
& below(sK336,sK338,sK337)
& below(sK336,sK337,sK338)
& sK337 != sK338 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK336,sK337,sK338]),skolemize(X0,sK336),skolemize(X1,sK337),skolemize(X2,sK338)],[f838]) ).
fof(f1513,plain,
! [X2,X0,X1] :
( ~ element(X2,the_carrier(X0))
| ~ element(X1,the_carrier(X0))
| ~ join_semilatt_str(X0)
| ~ join_commutative(X0)
| empty_carrier(X0)
| join_commut(X0,X1,X2) = join_commut(X0,X2,X1) ),
inference(cnf_transformation,[],[f512]) ).
fof(f1676,plain,
! [X2,X0,X1] :
( ~ join_semilatt_str(X0)
| empty_carrier(X0)
| ~ element(X1,the_carrier(X0))
| ~ element(X2,the_carrier(X0))
| ~ below(X0,X1,X2)
| join(X0,X1,X2) = X2 ),
inference(cnf_transformation,[],[f1103]) ).
fof(f2071,plain,
! [X2,X0,X1] :
( ~ element(X2,the_carrier(X0))
| ~ element(X1,the_carrier(X0))
| ~ join_semilatt_str(X0)
| ~ join_commutative(X0)
| empty_carrier(X0)
| join_commut(X0,X1,X2) = join(X0,X1,X2) ),
inference(cnf_transformation,[],[f689]) ).
fof(f2491,plain,
join_semilatt_str(sK336),
inference(cnf_transformation,[],[f1428]) ).
fof(f2492,plain,
join_commutative(sK336),
inference(cnf_transformation,[],[f1428]) ).
fof(f2493,plain,
~ empty_carrier(sK336),
inference(cnf_transformation,[],[f1428]) ).
fof(f2494,plain,
element(sK337,the_carrier(sK336)),
inference(cnf_transformation,[],[f1428]) ).
fof(f2495,plain,
element(sK338,the_carrier(sK336)),
inference(cnf_transformation,[],[f1428]) ).
fof(f2496,plain,
below(sK336,sK338,sK337),
inference(cnf_transformation,[],[f1428]) ).
fof(f2497,plain,
below(sK336,sK337,sK338),
inference(cnf_transformation,[],[f1428]) ).
fof(f2498,plain,
sK337 != sK338,
inference(cnf_transformation,[],[f1428]) ).
tcf(c_78,plain,
! [X0: $i,X1: $i,X2: $i] :
( empty_carrier(X1)
| ( join_commut(X1,X0,X2) = join_commut(X1,X2,X0) )
| ~ join_semilatt_str(X1)
| ~ join_commutative(X1)
| ~ element(X2,the_carrier(X1))
| ~ element(X0,the_carrier(X1)) ),
inference(cnf_transformation,[],[f1513]) ).
tcf(c_241,plain,
! [X0: $i,X1: $i,X2: $i] :
( empty_carrier(X0)
| ( join(X0,X1,X2) = X2 )
| ~ join_semilatt_str(X0)
| ~ element(X2,the_carrier(X0))
| ~ element(X1,the_carrier(X0))
| ~ below(X0,X1,X2) ),
inference(cnf_transformation,[],[f1676]) ).
tcf(c_634,plain,
! [X0: $i,X1: $i,X2: $i] :
( empty_carrier(X1)
| ( join_commut(X1,X0,X2) = join(X1,X0,X2) )
| ~ join_semilatt_str(X1)
| ~ join_commutative(X1)
| ~ element(X2,the_carrier(X1))
| ~ element(X0,the_carrier(X1)) ),
inference(cnf_transformation,[],[f2071]) ).
tcf(c_1054,negated_conjecture,
sK337 != sK338,
inference(cnf_transformation,[],[f2498]) ).
tcf(c_1055,negated_conjecture,
below(sK336,sK337,sK338),
inference(cnf_transformation,[],[f2497]) ).
tcf(c_1056,negated_conjecture,
below(sK336,sK338,sK337),
inference(cnf_transformation,[],[f2496]) ).
tcf(c_1057,negated_conjecture,
element(sK338,the_carrier(sK336)),
inference(cnf_transformation,[],[f2495]) ).
tcf(c_1058,negated_conjecture,
element(sK337,the_carrier(sK336)),
inference(cnf_transformation,[],[f2494]) ).
tcf(c_1059,negated_conjecture,
~ empty_carrier(sK336),
inference(cnf_transformation,[],[f2493]) ).
tcf(c_1060,negated_conjecture,
join_commutative(sK336),
inference(cnf_transformation,[],[f2492]) ).
tcf(c_1061,negated_conjecture,
join_semilatt_str(sK336),
inference(cnf_transformation,[],[f2491]) ).
tcf(c_18912,plain,
! [X0: $i,X1: $i,X2: $i] :
( empty_carrier(X0)
| ( join_commut(X0,X1,X2) = join(X0,X1,X2) )
| ~ join_semilatt_str(X0)
| ~ element(X2,the_carrier(X0))
| ~ element(X1,the_carrier(X0))
| ( X0 != sK336 ) ),
inference(resolution_lifted,[status(thm)],[c_634,c_1060]) ).
tcf(c_18913,plain,
! [X0: $i,X1: $i] :
( empty_carrier(sK336)
| ( join_commut(sK336,X0,X1) = join(sK336,X0,X1) )
| ~ join_semilatt_str(sK336)
| ~ element(X1,the_carrier(sK336))
| ~ element(X0,the_carrier(sK336)) ),
inference(unflattening,[status(thm)],[c_18912]) ).
tcf(c_18915,plain,
! [X0: $i,X1: $i] :
( ~ element(X1,the_carrier(sK336))
| ~ element(X0,the_carrier(sK336))
| ( join_commut(sK336,X0,X1) = join(sK336,X0,X1) ) ),
inference(global_subsumption_just,[status(thm)],[c_18913,c_1061,c_1059,c_18913]) ).
tcf(c_18916,plain,
! [X0: $i,X1: $i] :
( ( join_commut(sK336,X0,X1) = join(sK336,X0,X1) )
| ~ element(X1,the_carrier(sK336))
| ~ element(X0,the_carrier(sK336)) ),
inference(renaming,[status(thm)],[c_18915]) ).
tcf(c_18942,plain,
! [X0: $i,X1: $i,X2: $i] :
( empty_carrier(X0)
| ( join_commut(X0,X1,X2) = join_commut(X0,X2,X1) )
| ~ join_semilatt_str(X0)
| ~ element(X2,the_carrier(X0))
| ~ element(X1,the_carrier(X0))
| ( X0 != sK336 ) ),
inference(resolution_lifted,[status(thm)],[c_78,c_1060]) ).
tcf(c_18943,plain,
! [X0: $i,X1: $i] :
( empty_carrier(sK336)
| ( join_commut(sK336,X0,X1) = join_commut(sK336,X1,X0) )
| ~ join_semilatt_str(sK336)
| ~ element(X1,the_carrier(sK336))
| ~ element(X0,the_carrier(sK336)) ),
inference(unflattening,[status(thm)],[c_18942]) ).
tcf(c_18945,plain,
! [X0: $i,X1: $i] :
( ~ element(X1,the_carrier(sK336))
| ~ element(X0,the_carrier(sK336))
| ( join_commut(sK336,X0,X1) = join_commut(sK336,X1,X0) ) ),
inference(global_subsumption_just,[status(thm)],[c_18943,c_1061,c_1059,c_18943]) ).
tcf(c_18946,plain,
! [X0: $i,X1: $i] :
( ( join_commut(sK336,X0,X1) = join_commut(sK336,X1,X0) )
| ~ element(X1,the_carrier(sK336))
| ~ element(X0,the_carrier(sK336)) ),
inference(renaming,[status(thm)],[c_18945]) ).
tcf(c_19111,plain,
! [X0: $i,X1: $i,X2: $i] :
( empty_carrier(X0)
| ( join(X0,X1,X2) = X2 )
| ~ join_semilatt_str(X0)
| ~ element(X2,the_carrier(X0))
| ~ element(X1,the_carrier(X0))
| ( X2 != sK338 )
| ( X1 != sK337 )
| ( X0 != sK336 ) ),
inference(resolution_lifted,[status(thm)],[c_241,c_1055]) ).
tcf(c_19112,plain,
( empty_carrier(sK336)
| ( join(sK336,sK337,sK338) = sK338 )
| ~ join_semilatt_str(sK336)
| ~ element(sK338,the_carrier(sK336))
| ~ element(sK337,the_carrier(sK336)) ),
inference(unflattening,[status(thm)],[c_19111]) ).
tcf(c_19113,plain,
join(sK336,sK337,sK338) = sK338,
inference(global_subsumption_just,[status(thm)],[c_19112,c_1061,c_1059,c_1058,c_1057,c_19112]) ).
tcf(c_19118,plain,
! [X0: $i,X1: $i,X2: $i] :
( empty_carrier(X0)
| ( join(X0,X1,X2) = X2 )
| ~ join_semilatt_str(X0)
| ~ element(X2,the_carrier(X0))
| ~ element(X1,the_carrier(X0))
| ( X2 != sK337 )
| ( X1 != sK338 )
| ( X0 != sK336 ) ),
inference(resolution_lifted,[status(thm)],[c_241,c_1056]) ).
tcf(c_19119,plain,
( empty_carrier(sK336)
| ( join(sK336,sK338,sK337) = sK337 )
| ~ join_semilatt_str(sK336)
| ~ element(sK338,the_carrier(sK336))
| ~ element(sK337,the_carrier(sK336)) ),
inference(unflattening,[status(thm)],[c_19118]) ).
tcf(c_19120,plain,
join(sK336,sK338,sK337) = sK337,
inference(global_subsumption_just,[status(thm)],[c_19119,c_1061,c_1059,c_1058,c_1057,c_19119]) ).
tcf(c_116901,definition,
iPr_def_27 = join(sK336,sK338,sK337),
introduced(definition,[new_symbols(definition,[iPr_def_27])],[]) ).
tcf(c_116902,definition,
iPr_def_28 = join(sK336,sK337,sK338),
introduced(definition,[new_symbols(definition,[iPr_def_28])],[]) ).
tcf(c_116911,plain,
iPr_def_27 = sK337,
inference(demodulation,[status(thm)],[c_19120,c_116901]) ).
tcf(c_116912,plain,
iPr_def_28 = sK338,
inference(demodulation,[status(thm)],[c_19113,c_116902]) ).
tcf(c_116913,plain,
! [X0: $i,X1: $i] :
( ( join_commut(sK336,X0,X1) = join_commut(sK336,X1,X0) )
| ~ element(X1,iPr_def_23)
| ~ element(X0,iPr_def_23) ),
inference(demodulation,[status(thm)],[c_18946]) ).
tcf(c_116915,plain,
! [X0: $i,X1: $i] :
( ( join_commut(sK336,X0,X1) = join(sK336,X0,X1) )
| ~ element(X1,iPr_def_23)
| ~ element(X0,iPr_def_23) ),
inference(demodulation,[status(thm)],[c_18916]) ).
tcf(c_116917,negated_conjecture,
element(sK337,iPr_def_23),
inference(demodulation,[status(thm)],[c_1058]) ).
tcf(c_116918,negated_conjecture,
element(sK338,iPr_def_23),
inference(demodulation,[status(thm)],[c_1057]) ).
tcf(c_116919,negated_conjecture,
sK337 != sK338,
inference(demodulation,[status(thm)],[c_1054]) ).
tcf(c_137523,plain,
element(iPr_def_27,iPr_def_23),
inference(light_normalisation,[status(thm)],[c_116917,c_116911]) ).
tcf(c_137524,plain,
element(iPr_def_28,iPr_def_23),
inference(light_normalisation,[status(thm)],[c_116918,c_116912]) ).
tcf(c_137525,plain,
iPr_def_27 != iPr_def_28,
inference(light_normalisation,[status(thm)],[c_116919,c_116911,c_116912]) ).
tcf(c_137543,plain,
! [X0: $i] :
( ( join_commut(sK336,X0,iPr_def_27) = join_commut(sK336,iPr_def_27,X0) )
| ~ element(X0,iPr_def_23) ),
inference(superposition,[status(thm)],[c_137523,c_116913]) ).
tcf(c_137568,plain,
join_commut(sK336,iPr_def_27,iPr_def_28) = join_commut(sK336,iPr_def_28,iPr_def_27),
inference(superposition,[status(thm)],[c_137524,c_137543]) ).
tcf(c_137609,plain,
! [X0: $i] :
( ( join_commut(sK336,iPr_def_27,X0) = join(sK336,iPr_def_27,X0) )
| ~ element(X0,iPr_def_23) ),
inference(superposition,[status(thm)],[c_137523,c_116915]) ).
tcf(c_137610,plain,
! [X0: $i] :
( ( join_commut(sK336,iPr_def_28,X0) = join(sK336,iPr_def_28,X0) )
| ~ element(X0,iPr_def_23) ),
inference(superposition,[status(thm)],[c_137524,c_116915]) ).
tcf(c_137638,plain,
join_commut(sK336,iPr_def_27,iPr_def_28) = join(sK336,iPr_def_27,iPr_def_28),
inference(superposition,[status(thm)],[c_137524,c_137609]) ).
tcf(c_137647,plain,
join_commut(sK336,iPr_def_28,iPr_def_27) = join(sK336,iPr_def_27,iPr_def_28),
inference(demodulation,[status(thm)],[c_137568,c_137638]) ).
tcf(c_137670,plain,
join_commut(sK336,iPr_def_28,iPr_def_27) = join(sK336,iPr_def_28,iPr_def_27),
inference(superposition,[status(thm)],[c_137523,c_137610]) ).
tcf(c_137673,plain,
join(sK336,iPr_def_27,iPr_def_28) = join(sK336,iPr_def_28,iPr_def_27),
inference(light_normalisation,[status(thm)],[c_137670,c_137647]) ).
tcf(c_137767,plain,
join(sK336,iPr_def_27,iPr_def_28) = iPr_def_27,
inference(light_normalisation,[status(thm)],[c_116901,c_116911,c_116912,c_137673]) ).
tcf(c_137779,plain,
iPr_def_27 = iPr_def_28,
inference(light_normalisation,[status(thm)],[c_116902,c_116911,c_116912,c_137767]) ).
tcf(c_137780,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_137779,c_137525]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU305+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.09/0.37 % Computer : n011.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Thu Sep 24 13:37:43 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.09/0.41 Running first-order theorem proving
% 0.09/0.41 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.42
% 0.09/0.42 % ======== iProver multi-core TPTP/SMT =========
% 0.09/0.42
% 0.09/0.42 % Detected problem language: tptp
% 0.09/0.43 % Proving...
% 51.09/7.84 % SZS status Started for theBenchmark.p
% 51.09/7.84 % SZS status Theorem for theBenchmark.p
% 51.09/7.84
% 51.09/7.84 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 51.09/7.84
% 51.09/7.84 % ------ iProver source info
% 51.09/7.84
% 51.09/7.84 % git: date: 2026-07-19 20:42:38 +0200
% 51.09/7.84 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 51.09/7.84 % git: non_committed_changes: false
% 51.09/7.84
% 51.09/7.84 % ------ Parsing...
% 51.09/7.84 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 51.09/7.84
% 51.09/7.84 % ------ Preprocessing... sup_sim: 95 sf_s rm: 21 0s sf_e pe_s pe:1:0s pe:2:0s pe:4:0s pe:8:0s pe_e sup_sim: 0 sf_s rm: 18 0s sf_e pe_s pe_e sup_sim: 0 sf_s rm: 18 0s sf_e pe_s pe_e %
% 51.09/7.84
% 51.09/7.84 % ------ Preprocessing... gs_s sp: 15 0s gs_e snvd_s sp: 0 0s snvd_e %
% 51.09/7.84
% 51.09/7.84 % ------ Preprocessing... sf_s rm: 3 0s sf_e sf_s rm: 0 0s sf_e
% 51.09/7.84 % ------ Proving...
% 51.09/7.84 % ------ Problem Properties
% 51.09/7.84
% 51.09/7.84 %
% 51.09/7.84 % clauses 1111
% 51.09/7.84 % conjectures 4
% 51.09/7.84 % EPR 183
% 51.09/7.84 % Horn 822
% 51.09/7.84 % unary 167
% 51.09/7.84 % binary 333
% 51.09/7.84 % lits 3267
% 51.09/7.84 % lits eq 484
% 51.09/7.84 % fd_pure 0
% 51.09/7.84 % fd_pseudo 0
% 51.09/7.84 % fd_cond 44
% 51.09/7.84 % fd_pseudo_cond 115
% 51.09/7.84 % AC symbols 0
% 51.09/7.84
% 51.09/7.84 % ------ Schedule dynamic 5 is on
% 51.09/7.84
% 51.09/7.84 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 51.09/7.84
% 51.09/7.84
% 51.09/7.84 % ------
% 51.09/7.84 % Current options:
% 51.09/7.84 % ------
% 51.09/7.84
% 51.09/7.84
% 51.09/7.84 %
% 51.09/7.84
% 51.09/7.84 % ------ Proving...
% 51.09/7.84 %
% 51.09/7.84
% 51.09/7.84 % SZS status Theorem for theBenchmark.p
% 51.09/7.84
% 51.09/7.84 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 51.09/7.85
% 51.09/7.85
%------------------------------------------------------------------------------