%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SEU394+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n006.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:57:19 PM UTC 2026
% Result : Theorem 19.60s 4.54s
% Output : CNFRefutation 19.60s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 9
% Syntax : Number of formulae : 67 ( 22 unt; 0 def)
% Number of atoms : 231 ( 44 equ)
% Maximal formula atoms : 8 ( 3 avg)
% Number of connectives : 291 ( 127 ~; 110 |; 44 &)
% ( 1 <=>; 9 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 5 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 11 ( 9 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 3 con; 0-3 aty)
% Number of variables : 73 ( 0 sgn 69 !; 4 ?; 29 :)
% Comments :
%------------------------------------------------------------------------------
fof(f59,axiom,
! [X0] :
( ( one_sorted_str(X0)
& ~ empty_carrier(X0) )
=> ~ empty(cast_as_carrier_subset(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc2_pre_topc) ).
fof(f68,axiom,
( relation(empty_set)
& empty(empty_set) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc4_relat_1) ).
fof(f113,axiom,
! [X0] :
( ( one_sorted_str(X0)
& ~ empty_carrier(X0) )
=> ! [X1] :
( ( element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0)))))
& upper_relstr_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
& filtered_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
& ~ empty(X1) )
=> set_difference(X1,singleton(empty_set)) = filter_of_net_str(X0,net_of_bool_filter(X0,cast_as_carrier_subset(X0),X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t14_yellow19) ).
fof(f114,conjecture,
! [X0] :
( ( one_sorted_str(X0)
& ~ empty_carrier(X0) )
=> ! [X1] :
( ( element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0)))))
& proper_element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0)))))
& upper_relstr_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
& filtered_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
& ~ empty(X1) )
=> X1 = filter_of_net_str(X0,net_of_bool_filter(X0,cast_as_carrier_subset(X0),X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t15_yellow19) ).
fof(f115,negated_conjecture,
~ ! [X0] :
( ( one_sorted_str(X0)
& ~ empty_carrier(X0) )
=> ! [X1] :
( ( element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0)))))
& proper_element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0)))))
& upper_relstr_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
& filtered_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
& ~ empty(X1) )
=> X1 = filter_of_net_str(X0,net_of_bool_filter(X0,cast_as_carrier_subset(X0),X1)) ) ),
inference(negated_conjecture,[status(cth)],[f114]) ).
fof(f119,axiom,
! [X0] :
( ~ empty(X0)
=> ! [X1] :
( ( element(X1,powerset(the_carrier(boole_POSet(X0))))
& proper_element(X1,powerset(the_carrier(boole_POSet(X0))))
& upper_relstr_subset(X1,boole_POSet(X0))
& filtered_subset(X1,boole_POSet(X0))
& ~ empty(X1) )
=> ! [X2] :
~ ( empty(X2)
& in(X2,X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2_yellow19) ).
fof(f125,axiom,
! [X0,X1] :
( set_difference(X0,singleton(X1)) = X0
<=> ~ in(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t65_zfmisc_1) ).
fof(f127,axiom,
! [X0,X1] :
~ ( empty(X1)
& in(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t7_boole) ).
fof(f226,plain,
! [X0] :
( ~ one_sorted_str(X0)
| empty_carrier(X0)
| ~ empty(cast_as_carrier_subset(X0)) ),
inference(ennf_transformation,[],[f59]) ).
fof(f227,plain,
! [X0] :
( ~ one_sorted_str(X0)
| empty_carrier(X0)
| ~ empty(cast_as_carrier_subset(X0)) ),
inference(flattening,[],[f226]) ).
fof(f280,plain,
! [X0] :
( ~ one_sorted_str(X0)
| empty_carrier(X0)
| ! [X1] :
( ~ element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0)))))
| ~ upper_relstr_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
| ~ filtered_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
| empty(X1)
| set_difference(X1,singleton(empty_set)) = filter_of_net_str(X0,net_of_bool_filter(X0,cast_as_carrier_subset(X0),X1)) ) ),
inference(ennf_transformation,[],[f113]) ).
fof(f281,plain,
! [X0] :
( ~ one_sorted_str(X0)
| empty_carrier(X0)
| ! [X1] :
( ~ element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0)))))
| ~ upper_relstr_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
| ~ filtered_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
| empty(X1)
| set_difference(X1,singleton(empty_set)) = filter_of_net_str(X0,net_of_bool_filter(X0,cast_as_carrier_subset(X0),X1)) ) ),
inference(flattening,[],[f280]) ).
fof(f282,plain,
? [X0] :
( one_sorted_str(X0)
& ~ empty_carrier(X0)
& ? [X1] :
( element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0)))))
& proper_element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0)))))
& upper_relstr_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
& filtered_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
& ~ empty(X1)
& filter_of_net_str(X0,net_of_bool_filter(X0,cast_as_carrier_subset(X0),X1)) != X1 ) ),
inference(ennf_transformation,[],[f115]) ).
fof(f283,plain,
? [X0] :
( one_sorted_str(X0)
& ~ empty_carrier(X0)
& ? [X1] :
( element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0)))))
& proper_element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0)))))
& upper_relstr_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
& filtered_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
& ~ empty(X1)
& filter_of_net_str(X0,net_of_bool_filter(X0,cast_as_carrier_subset(X0),X1)) != X1 ) ),
inference(flattening,[],[f282]) ).
fof(f288,plain,
! [X0] :
( empty(X0)
| ! [X1] :
( ~ element(X1,powerset(the_carrier(boole_POSet(X0))))
| ~ proper_element(X1,powerset(the_carrier(boole_POSet(X0))))
| ~ upper_relstr_subset(X1,boole_POSet(X0))
| ~ filtered_subset(X1,boole_POSet(X0))
| empty(X1)
| ! [X2] :
( ~ empty(X2)
| ~ in(X2,X1) ) ) ),
inference(ennf_transformation,[],[f119]) ).
fof(f289,plain,
! [X0] :
( empty(X0)
| ! [X1] :
( ~ element(X1,powerset(the_carrier(boole_POSet(X0))))
| ~ proper_element(X1,powerset(the_carrier(boole_POSet(X0))))
| ~ upper_relstr_subset(X1,boole_POSet(X0))
| ~ filtered_subset(X1,boole_POSet(X0))
| empty(X1)
| ! [X2] :
( ~ empty(X2)
| ~ in(X2,X1) ) ) ),
inference(flattening,[],[f288]) ).
fof(f295,plain,
! [X0,X1] :
( ~ empty(X1)
| ~ in(X0,X1) ),
inference(ennf_transformation,[],[f127]) ).
fof(f343,plain,
( one_sorted_str(sK39)
& ~ empty_carrier(sK39)
& element(sK40,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK39)))))
& proper_element(sK40,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK39)))))
& upper_relstr_subset(sK40,boole_POSet(cast_as_carrier_subset(sK39)))
& filtered_subset(sK40,boole_POSet(cast_as_carrier_subset(sK39)))
& ~ empty(sK40)
& sK40 != filter_of_net_str(sK39,net_of_bool_filter(sK39,cast_as_carrier_subset(sK39),sK40)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK39,sK40]),skolemize(X0,sK39),skolemize(X1,sK40)],[f283]) ).
fof(f346,plain,
! [X0,X1] :
( ( set_difference(X0,singleton(X1)) != X0
| ~ in(X1,X0) )
& ( in(X1,X0)
| set_difference(X0,singleton(X1)) = X0 ) ),
inference(nnf_transformation,[],[f125]) ).
fof(f457,plain,
! [X0] :
( ~ one_sorted_str(X0)
| empty_carrier(X0)
| ~ empty(cast_as_carrier_subset(X0)) ),
inference(cnf_transformation,[],[f227]) ).
fof(f485,plain,
empty(empty_set),
inference(cnf_transformation,[],[f68]) ).
fof(f680,plain,
! [X0,X1] :
( ~ one_sorted_str(X0)
| empty_carrier(X0)
| ~ element(X1,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0)))))
| ~ upper_relstr_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
| ~ filtered_subset(X1,boole_POSet(cast_as_carrier_subset(X0)))
| empty(X1)
| set_difference(X1,singleton(empty_set)) = filter_of_net_str(X0,net_of_bool_filter(X0,cast_as_carrier_subset(X0),X1)) ),
inference(cnf_transformation,[],[f281]) ).
fof(f681,plain,
one_sorted_str(sK39),
inference(cnf_transformation,[],[f343]) ).
fof(f682,plain,
~ empty_carrier(sK39),
inference(cnf_transformation,[],[f343]) ).
fof(f683,plain,
element(sK40,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK39))))),
inference(cnf_transformation,[],[f343]) ).
fof(f684,plain,
proper_element(sK40,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK39))))),
inference(cnf_transformation,[],[f343]) ).
fof(f685,plain,
upper_relstr_subset(sK40,boole_POSet(cast_as_carrier_subset(sK39))),
inference(cnf_transformation,[],[f343]) ).
fof(f686,plain,
filtered_subset(sK40,boole_POSet(cast_as_carrier_subset(sK39))),
inference(cnf_transformation,[],[f343]) ).
fof(f687,plain,
~ empty(sK40),
inference(cnf_transformation,[],[f343]) ).
fof(f688,plain,
sK40 != filter_of_net_str(sK39,net_of_bool_filter(sK39,cast_as_carrier_subset(sK39),sK40)),
inference(cnf_transformation,[],[f343]) ).
fof(f693,plain,
! [X2,X0,X1] :
( empty(X0)
| ~ element(X1,powerset(the_carrier(boole_POSet(X0))))
| ~ proper_element(X1,powerset(the_carrier(boole_POSet(X0))))
| ~ upper_relstr_subset(X1,boole_POSet(X0))
| ~ filtered_subset(X1,boole_POSet(X0))
| empty(X1)
| ~ empty(X2)
| ~ in(X2,X1) ),
inference(cnf_transformation,[],[f289]) ).
fof(f700,plain,
! [X0,X1] :
( in(X1,X0)
| set_difference(X0,singleton(X1)) = X0 ),
inference(cnf_transformation,[],[f346]) ).
fof(f702,plain,
! [X0,X1] :
( ~ empty(X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[],[f295]) ).
tcf(c_140,plain,
! [X0: $i] :
( empty_carrier(X0)
| ~ one_sorted_str(X0)
| ~ empty(cast_as_carrier_subset(X0)) ),
inference(cnf_transformation,[],[f457]) ).
tcf(c_167,plain,
empty(empty_set),
inference(cnf_transformation,[],[f485]) ).
tcf(c_363,plain,
! [X0: $i,X1: $i] :
( empty(X0)
| empty_carrier(X1)
| ( filter_of_net_str(X1,net_of_bool_filter(X1,cast_as_carrier_subset(X1),X0)) = set_difference(X0,singleton(empty_set)) )
| ~ one_sorted_str(X1)
| ~ upper_relstr_subset(X0,boole_POSet(cast_as_carrier_subset(X1)))
| ~ filtered_subset(X0,boole_POSet(cast_as_carrier_subset(X1)))
| ~ element(X0,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X1))))) ),
inference(cnf_transformation,[],[f680]) ).
tcf(c_364,negated_conjecture,
filter_of_net_str(sK39,net_of_bool_filter(sK39,cast_as_carrier_subset(sK39),sK40)) != sK40,
inference(cnf_transformation,[],[f688]) ).
tcf(c_365,negated_conjecture,
~ empty(sK40),
inference(cnf_transformation,[],[f687]) ).
tcf(c_366,negated_conjecture,
filtered_subset(sK40,boole_POSet(cast_as_carrier_subset(sK39))),
inference(cnf_transformation,[],[f686]) ).
tcf(c_367,negated_conjecture,
upper_relstr_subset(sK40,boole_POSet(cast_as_carrier_subset(sK39))),
inference(cnf_transformation,[],[f685]) ).
tcf(c_368,negated_conjecture,
proper_element(sK40,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK39))))),
inference(cnf_transformation,[],[f684]) ).
tcf(c_369,negated_conjecture,
element(sK40,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK39))))),
inference(cnf_transformation,[],[f683]) ).
tcf(c_370,negated_conjecture,
~ empty_carrier(sK39),
inference(cnf_transformation,[],[f682]) ).
tcf(c_371,negated_conjecture,
one_sorted_str(sK39),
inference(cnf_transformation,[],[f681]) ).
tcf(c_376,plain,
! [X0: $i,X1: $i,X2: $i] :
( empty(X1)
| empty(X0)
| ~ empty(X2)
| ~ in(X2,X0)
| ~ upper_relstr_subset(X0,boole_POSet(X1))
| ~ filtered_subset(X0,boole_POSet(X1))
| ~ proper_element(X0,powerset(the_carrier(boole_POSet(X1))))
| ~ element(X0,powerset(the_carrier(boole_POSet(X1)))) ),
inference(cnf_transformation,[],[f693]) ).
tcf(c_382,plain,
! [X0: $i,X1: $i] :
( in(X1,X0)
| ( set_difference(X0,singleton(X1)) = X0 ) ),
inference(cnf_transformation,[],[f700]) ).
tcf(c_385,plain,
! [X0: $i,X1: $i] :
( ~ empty(X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[],[f702]) ).
tcf(c_650,plain,
! [X0: $i,X1: $i] :
( ~ empty(X1)
| ~ in(X0,X1) ),
inference(prop_impl_just,[status(thm)],[c_385]) ).
tcf(c_1537,plain,
! [X0: $i,X1: $i,X2: $i] :
( empty(X1)
| ~ empty(X2)
| ~ in(X2,X0)
| ~ upper_relstr_subset(X0,boole_POSet(X1))
| ~ filtered_subset(X0,boole_POSet(X1))
| ~ proper_element(X0,powerset(the_carrier(boole_POSet(X1))))
| ~ element(X0,powerset(the_carrier(boole_POSet(X1)))) ),
inference(backward_subsumption_resolution,[status(thm)],[c_376,c_650]) ).
tcf(c_11737,plain,
! [X0: $i] : X0 = X0,
theory(equality) ).
tcf(c_11739,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = X0 )
| ( X2 != X1 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_15738,plain,
! [X0: $i] :
( ( filter_of_net_str(sK39,net_of_bool_filter(sK39,cast_as_carrier_subset(sK39),sK40)) = sK40 )
| ( sK40 != X0 )
| ( filter_of_net_str(sK39,net_of_bool_filter(sK39,cast_as_carrier_subset(sK39),sK40)) != X0 ) ),
inference(instantiation,[status(thm)],[c_11739]) ).
tcf(c_15752,plain,
( empty_carrier(sK39)
| ~ one_sorted_str(sK39)
| ~ empty(cast_as_carrier_subset(sK39)) ),
inference(instantiation,[status(thm)],[c_140]) ).
tcf(c_15761,plain,
! [X0: $i] :
( empty(sK40)
| empty_carrier(X0)
| ( filter_of_net_str(X0,net_of_bool_filter(X0,cast_as_carrier_subset(X0),sK40)) = set_difference(sK40,singleton(empty_set)) )
| ~ one_sorted_str(X0)
| ~ upper_relstr_subset(sK40,boole_POSet(cast_as_carrier_subset(X0)))
| ~ filtered_subset(sK40,boole_POSet(cast_as_carrier_subset(X0)))
| ~ element(sK40,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X0))))) ),
inference(instantiation,[status(thm)],[c_363]) ).
tcf(c_15863,plain,
! [X0: $i,X1: $i] :
( ( sK40 = X0 )
| ( sK40 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_11739]) ).
tcf(c_16095,plain,
( empty(sK40)
| empty_carrier(sK39)
| ( filter_of_net_str(sK39,net_of_bool_filter(sK39,cast_as_carrier_subset(sK39),sK40)) = set_difference(sK40,singleton(empty_set)) )
| ~ one_sorted_str(sK39)
| ~ upper_relstr_subset(sK40,boole_POSet(cast_as_carrier_subset(sK39)))
| ~ filtered_subset(sK40,boole_POSet(cast_as_carrier_subset(sK39)))
| ~ element(sK40,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK39))))) ),
inference(instantiation,[status(thm)],[c_15761]) ).
tcf(c_16443,plain,
! [X0: $i] :
( ( sK40 = X0 )
| ( sK40 != sK40 )
| ( X0 != sK40 ) ),
inference(instantiation,[status(thm)],[c_15863]) ).
tcf(c_17048,plain,
! [X0: $i] :
( ( sK40 = set_difference(sK40,singleton(X0)) )
| ( sK40 != sK40 )
| ( set_difference(sK40,singleton(X0)) != sK40 ) ),
inference(instantiation,[status(thm)],[c_16443]) ).
tcf(c_17886,plain,
sK40 = sK40,
inference(instantiation,[status(thm)],[c_11737]) ).
tcf(c_18090,plain,
( ( filter_of_net_str(sK39,net_of_bool_filter(sK39,cast_as_carrier_subset(sK39),sK40)) = sK40 )
| ( sK40 != set_difference(sK40,singleton(empty_set)) )
| ( filter_of_net_str(sK39,net_of_bool_filter(sK39,cast_as_carrier_subset(sK39),sK40)) != set_difference(sK40,singleton(empty_set)) ) ),
inference(instantiation,[status(thm)],[c_15738]) ).
tcf(c_22302,plain,
( ( sK40 = set_difference(sK40,singleton(empty_set)) )
| ( sK40 != sK40 )
| ( set_difference(sK40,singleton(empty_set)) != sK40 ) ),
inference(instantiation,[status(thm)],[c_17048]) ).
tcf(c_25208,plain,
! [X0: $i] :
( empty(cast_as_carrier_subset(sK39))
| ~ empty(X0)
| ~ in(X0,sK40)
| ~ upper_relstr_subset(sK40,boole_POSet(cast_as_carrier_subset(sK39)))
| ~ filtered_subset(sK40,boole_POSet(cast_as_carrier_subset(sK39)))
| ~ proper_element(sK40,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(sK39))))) ),
inference(superposition,[status(thm)],[c_369,c_1537]) ).
tcf(c_25562,plain,
! [X0: $i] :
( ~ in(X0,sK40)
| ~ empty(X0) ),
inference(global_subsumption_just,[status(thm)],[c_25208,c_371,c_370,c_367,c_366,c_368,c_15752,c_25208]) ).
tcf(c_25563,plain,
! [X0: $i] :
( ~ empty(X0)
| ~ in(X0,sK40) ),
inference(renaming,[status(thm)],[c_25562]) ).
tcf(c_25565,plain,
! [X0: $i] :
( ( set_difference(sK40,singleton(X0)) = sK40 )
| ~ empty(X0) ),
inference(superposition,[status(thm)],[c_382,c_25563]) ).
tcf(c_25661,plain,
set_difference(sK40,singleton(empty_set)) = sK40,
inference(superposition,[status(thm)],[c_167,c_25565]) ).
tcf(c_25664,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_25661,c_22302,c_18090,c_17886,c_16095,c_364,c_369,c_366,c_367,c_365,c_370,c_371]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SEU394+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.07 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.17/0.42 % Computer : n006.cluster.edu
% 0.17/0.42 % Model : x86_64 x86_64
% 0.17/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.42 % Memory : 8046.5625MB
% 0.17/0.42 % OS : Linux 6.8.0-71-generic
% 0.17/0.42 % CPULimit : 300
% 0.17/0.42 % WCLimit : 300
% 0.17/0.42 % DateTime : Thu Sep 24 13:57:56 UTC 2026
% 0.17/0.42 % CPUTime :
% 0.17/0.42 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.17/0.49 Running first-order theorem proving
% 0.17/0.49 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.25/0.50
% 0.25/0.50 % ======== iProver multi-core TPTP/SMT =========
% 0.25/0.50
% 0.25/0.51 % Detected problem language: tptp
% 0.25/0.52 % Proving...
% 19.60/4.54 % SZS status Started for theBenchmark.p
% 19.60/4.54 % SZS status Theorem for theBenchmark.p
% 19.60/4.54
% 19.60/4.54 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 19.60/4.54
% 19.60/4.54 % ------ iProver source info
% 19.60/4.54
% 19.60/4.54 % git: date: 2026-07-19 20:42:38 +0200
% 19.60/4.54 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 19.60/4.54 % git: non_committed_changes: false
% 19.60/4.54
% 19.60/4.54 % ------ Parsing...
% 19.60/4.54 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 19.60/4.54
% 19.60/4.54 % ------ Preprocessing... sup_sim: 0 sf_s rm: 22 0s sf_e pe_s pe:1:0s pe:2:0s pe:4:0s pe:8:0s pe_e %
% 19.60/4.54
% 19.60/4.54 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 19.60/4.54
% 19.60/4.54 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 19.60/4.54 % ------ Proving...
% 19.60/4.54 % ------ Problem Properties
% 19.60/4.54
% 19.60/4.54 %
% 19.60/4.54 % clauses 247
% 19.60/4.54 % conjectures 8
% 19.60/4.54 % EPR 62
% 19.60/4.54 % Horn 188
% 19.60/4.54 % unary 120
% 19.60/4.54 % binary 63
% 19.60/4.54 % lits 564
% 19.60/4.54 % lits eq 26
% 19.60/4.54 % fd_pure 0
% 19.60/4.54 % fd_pseudo 0
% 19.60/4.54 % fd_cond 1
% 19.60/4.54 % fd_pseudo_cond 9
% 19.60/4.54 % AC symbols 0
% 19.60/4.54
% 19.60/4.54 % ------ Input Options Time Limit: Unbounded
% 19.60/4.54
% 19.60/4.54
% 19.60/4.54 % ------
% 19.60/4.54 % Current options:
% 19.60/4.54 % ------
% 19.60/4.54
% 19.60/4.54
% 19.60/4.54 %
% 19.60/4.54
% 19.60/4.54 % ------ Proving...
% 19.60/4.54 %
% 19.60/4.54
% 19.60/4.54 % SZS status Theorem for theBenchmark.p
% 19.60/4.54
% 19.60/4.54 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 19.60/4.54
% 19.60/4.54
%------------------------------------------------------------------------------