%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : SEU394+1 : TPTP v5.0.0. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : Source/sine.py -e eprover -t %d %s
% Computer : art06.cs.miami.edu
% Model : i686 i686
% CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
% Memory : 2018MB
% OS : Linux 2.6.26.8-57.fc8
% CPULimit : 300s
% DateTime : Sun Dec 26 08:14:36 EST 2010
% Result : Theorem 0.42s
% Output : CNFRefutation 0.42s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 7
% Syntax : Number of formulae : 65 ( 15 unt; 0 def)
% Number of atoms : 275 ( 28 equ)
% Maximal formula atoms : 8 ( 4 avg)
% Number of connectives : 345 ( 135 ~; 131 |; 61 &)
% ( 2 <=>; 16 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 6 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 12 ( 10 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 3 con; 0-3 aty)
% Number of variables : 71 ( 1 sgn 49 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(1,axiom,
! [X1,X2] :
( set_difference(X1,singleton(X2)) = X1
<=> ~ in(X2,X1) ),
file('/tmp/tmpm2d8iW/sel_SEU394+1.p_1',t65_zfmisc_1) ).
fof(18,axiom,
( empty(empty_set)
& relation(empty_set)
& relation_empty_yielding(empty_set) ),
file('/tmp/tmpm2d8iW/sel_SEU394+1.p_1',fc12_relat_1) ).
fof(62,axiom,
! [X1] :
( ( ~ empty_carrier(X1)
& one_sorted_str(X1) )
=> ! [X2] :
( ( ~ empty(X2)
& filtered_subset(X2,boole_POSet(cast_as_carrier_subset(X1)))
& upper_relstr_subset(X2,boole_POSet(cast_as_carrier_subset(X1)))
& element(X2,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X1))))) )
=> set_difference(X2,singleton(empty_set)) = filter_of_net_str(X1,net_of_bool_filter(X1,cast_as_carrier_subset(X1),X2)) ) ),
file('/tmp/tmpm2d8iW/sel_SEU394+1.p_1',t14_yellow19) ).
fof(64,axiom,
! [X1,X2] :
~ ( in(X1,X2)
& empty(X2) ),
file('/tmp/tmpm2d8iW/sel_SEU394+1.p_1',t7_boole) ).
fof(66,axiom,
! [X1] :
( ( ~ empty_carrier(X1)
& one_sorted_str(X1) )
=> ~ empty(cast_as_carrier_subset(X1)) ),
file('/tmp/tmpm2d8iW/sel_SEU394+1.p_1',fc2_pre_topc) ).
fof(71,axiom,
! [X1] :
( ~ empty(X1)
=> ! [X2] :
( ( ~ empty(X2)
& filtered_subset(X2,boole_POSet(X1))
& upper_relstr_subset(X2,boole_POSet(X1))
& proper_element(X2,powerset(the_carrier(boole_POSet(X1))))
& element(X2,powerset(the_carrier(boole_POSet(X1)))) )
=> ! [X3] :
~ ( in(X3,X2)
& empty(X3) ) ) ),
file('/tmp/tmpm2d8iW/sel_SEU394+1.p_1',t2_yellow19) ).
fof(122,conjecture,
! [X1] :
( ( ~ empty_carrier(X1)
& one_sorted_str(X1) )
=> ! [X2] :
( ( ~ empty(X2)
& filtered_subset(X2,boole_POSet(cast_as_carrier_subset(X1)))
& upper_relstr_subset(X2,boole_POSet(cast_as_carrier_subset(X1)))
& proper_element(X2,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X1)))))
& element(X2,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X1))))) )
=> X2 = filter_of_net_str(X1,net_of_bool_filter(X1,cast_as_carrier_subset(X1),X2)) ) ),
file('/tmp/tmpm2d8iW/sel_SEU394+1.p_1',t15_yellow19) ).
fof(128,negated_conjecture,
~ ! [X1] :
( ( ~ empty_carrier(X1)
& one_sorted_str(X1) )
=> ! [X2] :
( ( ~ empty(X2)
& filtered_subset(X2,boole_POSet(cast_as_carrier_subset(X1)))
& upper_relstr_subset(X2,boole_POSet(cast_as_carrier_subset(X1)))
& proper_element(X2,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X1)))))
& element(X2,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X1))))) )
=> X2 = filter_of_net_str(X1,net_of_bool_filter(X1,cast_as_carrier_subset(X1),X2)) ) ),
inference(assume_negation,[status(cth)],[122]) ).
fof(129,plain,
! [X1,X2] :
( set_difference(X1,singleton(X2)) = X1
<=> ~ in(X2,X1) ),
inference(fof_simplification,[status(thm)],[1,theory(equality)]) ).
fof(156,plain,
! [X1] :
( ( ~ empty_carrier(X1)
& one_sorted_str(X1) )
=> ! [X2] :
( ( ~ empty(X2)
& filtered_subset(X2,boole_POSet(cast_as_carrier_subset(X1)))
& upper_relstr_subset(X2,boole_POSet(cast_as_carrier_subset(X1)))
& element(X2,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X1))))) )
=> set_difference(X2,singleton(empty_set)) = filter_of_net_str(X1,net_of_bool_filter(X1,cast_as_carrier_subset(X1),X2)) ) ),
inference(fof_simplification,[status(thm)],[62,theory(equality)]) ).
fof(158,plain,
! [X1] :
( ( ~ empty_carrier(X1)
& one_sorted_str(X1) )
=> ~ empty(cast_as_carrier_subset(X1)) ),
inference(fof_simplification,[status(thm)],[66,theory(equality)]) ).
fof(162,plain,
! [X1] :
( ~ empty(X1)
=> ! [X2] :
( ( ~ empty(X2)
& filtered_subset(X2,boole_POSet(X1))
& upper_relstr_subset(X2,boole_POSet(X1))
& proper_element(X2,powerset(the_carrier(boole_POSet(X1))))
& element(X2,powerset(the_carrier(boole_POSet(X1)))) )
=> ! [X3] :
~ ( in(X3,X2)
& empty(X3) ) ) ),
inference(fof_simplification,[status(thm)],[71,theory(equality)]) ).
fof(193,negated_conjecture,
~ ! [X1] :
( ( ~ empty_carrier(X1)
& one_sorted_str(X1) )
=> ! [X2] :
( ( ~ empty(X2)
& filtered_subset(X2,boole_POSet(cast_as_carrier_subset(X1)))
& upper_relstr_subset(X2,boole_POSet(cast_as_carrier_subset(X1)))
& proper_element(X2,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X1)))))
& element(X2,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X1))))) )
=> X2 = filter_of_net_str(X1,net_of_bool_filter(X1,cast_as_carrier_subset(X1),X2)) ) ),
inference(fof_simplification,[status(thm)],[128,theory(equality)]) ).
fof(198,plain,
! [X1,X2] :
( ( set_difference(X1,singleton(X2)) != X1
| ~ in(X2,X1) )
& ( in(X2,X1)
| set_difference(X1,singleton(X2)) = X1 ) ),
inference(fof_nnf,[status(thm)],[129]) ).
fof(199,plain,
! [X3,X4] :
( ( set_difference(X3,singleton(X4)) != X3
| ~ in(X4,X3) )
& ( in(X4,X3)
| set_difference(X3,singleton(X4)) = X3 ) ),
inference(variable_rename,[status(thm)],[198]) ).
cnf(200,plain,
( set_difference(X1,singleton(X2)) = X1
| in(X2,X1) ),
inference(split_conjunct,[status(thm)],[199]) ).
cnf(285,plain,
empty(empty_set),
inference(split_conjunct,[status(thm)],[18]) ).
fof(509,plain,
! [X1] :
( empty_carrier(X1)
| ~ one_sorted_str(X1)
| ! [X2] :
( empty(X2)
| ~ filtered_subset(X2,boole_POSet(cast_as_carrier_subset(X1)))
| ~ upper_relstr_subset(X2,boole_POSet(cast_as_carrier_subset(X1)))
| ~ element(X2,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X1)))))
| set_difference(X2,singleton(empty_set)) = filter_of_net_str(X1,net_of_bool_filter(X1,cast_as_carrier_subset(X1),X2)) ) ),
inference(fof_nnf,[status(thm)],[156]) ).
fof(510,plain,
! [X3] :
( empty_carrier(X3)
| ~ one_sorted_str(X3)
| ! [X4] :
( empty(X4)
| ~ filtered_subset(X4,boole_POSet(cast_as_carrier_subset(X3)))
| ~ upper_relstr_subset(X4,boole_POSet(cast_as_carrier_subset(X3)))
| ~ element(X4,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X3)))))
| set_difference(X4,singleton(empty_set)) = filter_of_net_str(X3,net_of_bool_filter(X3,cast_as_carrier_subset(X3),X4)) ) ),
inference(variable_rename,[status(thm)],[509]) ).
fof(511,plain,
! [X3,X4] :
( empty(X4)
| ~ filtered_subset(X4,boole_POSet(cast_as_carrier_subset(X3)))
| ~ upper_relstr_subset(X4,boole_POSet(cast_as_carrier_subset(X3)))
| ~ element(X4,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X3)))))
| set_difference(X4,singleton(empty_set)) = filter_of_net_str(X3,net_of_bool_filter(X3,cast_as_carrier_subset(X3),X4))
| empty_carrier(X3)
| ~ one_sorted_str(X3) ),
inference(shift_quantors,[status(thm)],[510]) ).
cnf(512,plain,
( empty_carrier(X1)
| set_difference(X2,singleton(empty_set)) = filter_of_net_str(X1,net_of_bool_filter(X1,cast_as_carrier_subset(X1),X2))
| empty(X2)
| ~ one_sorted_str(X1)
| ~ element(X2,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X1)))))
| ~ upper_relstr_subset(X2,boole_POSet(cast_as_carrier_subset(X1)))
| ~ filtered_subset(X2,boole_POSet(cast_as_carrier_subset(X1))) ),
inference(split_conjunct,[status(thm)],[511]) ).
fof(514,plain,
! [X1,X2] :
( ~ in(X1,X2)
| ~ empty(X2) ),
inference(fof_nnf,[status(thm)],[64]) ).
fof(515,plain,
! [X3,X4] :
( ~ in(X3,X4)
| ~ empty(X4) ),
inference(variable_rename,[status(thm)],[514]) ).
cnf(516,plain,
( ~ empty(X1)
| ~ in(X2,X1) ),
inference(split_conjunct,[status(thm)],[515]) ).
fof(520,plain,
! [X1] :
( empty_carrier(X1)
| ~ one_sorted_str(X1)
| ~ empty(cast_as_carrier_subset(X1)) ),
inference(fof_nnf,[status(thm)],[158]) ).
fof(521,plain,
! [X2] :
( empty_carrier(X2)
| ~ one_sorted_str(X2)
| ~ empty(cast_as_carrier_subset(X2)) ),
inference(variable_rename,[status(thm)],[520]) ).
cnf(522,plain,
( empty_carrier(X1)
| ~ empty(cast_as_carrier_subset(X1))
| ~ one_sorted_str(X1) ),
inference(split_conjunct,[status(thm)],[521]) ).
fof(542,plain,
! [X1] :
( empty(X1)
| ! [X2] :
( empty(X2)
| ~ filtered_subset(X2,boole_POSet(X1))
| ~ upper_relstr_subset(X2,boole_POSet(X1))
| ~ proper_element(X2,powerset(the_carrier(boole_POSet(X1))))
| ~ element(X2,powerset(the_carrier(boole_POSet(X1))))
| ! [X3] :
( ~ in(X3,X2)
| ~ empty(X3) ) ) ),
inference(fof_nnf,[status(thm)],[162]) ).
fof(543,plain,
! [X4] :
( empty(X4)
| ! [X5] :
( empty(X5)
| ~ filtered_subset(X5,boole_POSet(X4))
| ~ upper_relstr_subset(X5,boole_POSet(X4))
| ~ proper_element(X5,powerset(the_carrier(boole_POSet(X4))))
| ~ element(X5,powerset(the_carrier(boole_POSet(X4))))
| ! [X6] :
( ~ in(X6,X5)
| ~ empty(X6) ) ) ),
inference(variable_rename,[status(thm)],[542]) ).
fof(544,plain,
! [X4,X5,X6] :
( ~ in(X6,X5)
| ~ empty(X6)
| empty(X5)
| ~ filtered_subset(X5,boole_POSet(X4))
| ~ upper_relstr_subset(X5,boole_POSet(X4))
| ~ proper_element(X5,powerset(the_carrier(boole_POSet(X4))))
| ~ element(X5,powerset(the_carrier(boole_POSet(X4))))
| empty(X4) ),
inference(shift_quantors,[status(thm)],[543]) ).
cnf(545,plain,
( empty(X1)
| empty(X2)
| ~ element(X2,powerset(the_carrier(boole_POSet(X1))))
| ~ proper_element(X2,powerset(the_carrier(boole_POSet(X1))))
| ~ upper_relstr_subset(X2,boole_POSet(X1))
| ~ filtered_subset(X2,boole_POSet(X1))
| ~ empty(X3)
| ~ in(X3,X2) ),
inference(split_conjunct,[status(thm)],[544]) ).
fof(834,negated_conjecture,
? [X1] :
( ~ empty_carrier(X1)
& one_sorted_str(X1)
& ? [X2] :
( ~ empty(X2)
& filtered_subset(X2,boole_POSet(cast_as_carrier_subset(X1)))
& upper_relstr_subset(X2,boole_POSet(cast_as_carrier_subset(X1)))
& proper_element(X2,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X1)))))
& element(X2,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X1)))))
& X2 != filter_of_net_str(X1,net_of_bool_filter(X1,cast_as_carrier_subset(X1),X2)) ) ),
inference(fof_nnf,[status(thm)],[193]) ).
fof(835,negated_conjecture,
? [X3] :
( ~ empty_carrier(X3)
& one_sorted_str(X3)
& ? [X4] :
( ~ empty(X4)
& filtered_subset(X4,boole_POSet(cast_as_carrier_subset(X3)))
& upper_relstr_subset(X4,boole_POSet(cast_as_carrier_subset(X3)))
& proper_element(X4,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X3)))))
& element(X4,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(X3)))))
& X4 != filter_of_net_str(X3,net_of_bool_filter(X3,cast_as_carrier_subset(X3),X4)) ) ),
inference(variable_rename,[status(thm)],[834]) ).
fof(836,negated_conjecture,
( ~ empty_carrier(esk39_0)
& one_sorted_str(esk39_0)
& ~ empty(esk40_0)
& filtered_subset(esk40_0,boole_POSet(cast_as_carrier_subset(esk39_0)))
& upper_relstr_subset(esk40_0,boole_POSet(cast_as_carrier_subset(esk39_0)))
& proper_element(esk40_0,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(esk39_0)))))
& element(esk40_0,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(esk39_0)))))
& esk40_0 != filter_of_net_str(esk39_0,net_of_bool_filter(esk39_0,cast_as_carrier_subset(esk39_0),esk40_0)) ),
inference(skolemize,[status(esa)],[835]) ).
cnf(837,negated_conjecture,
esk40_0 != filter_of_net_str(esk39_0,net_of_bool_filter(esk39_0,cast_as_carrier_subset(esk39_0),esk40_0)),
inference(split_conjunct,[status(thm)],[836]) ).
cnf(838,negated_conjecture,
element(esk40_0,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(esk39_0))))),
inference(split_conjunct,[status(thm)],[836]) ).
cnf(839,negated_conjecture,
proper_element(esk40_0,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(esk39_0))))),
inference(split_conjunct,[status(thm)],[836]) ).
cnf(840,negated_conjecture,
upper_relstr_subset(esk40_0,boole_POSet(cast_as_carrier_subset(esk39_0))),
inference(split_conjunct,[status(thm)],[836]) ).
cnf(841,negated_conjecture,
filtered_subset(esk40_0,boole_POSet(cast_as_carrier_subset(esk39_0))),
inference(split_conjunct,[status(thm)],[836]) ).
cnf(842,negated_conjecture,
~ empty(esk40_0),
inference(split_conjunct,[status(thm)],[836]) ).
cnf(843,negated_conjecture,
one_sorted_str(esk39_0),
inference(split_conjunct,[status(thm)],[836]) ).
cnf(844,negated_conjecture,
~ empty_carrier(esk39_0),
inference(split_conjunct,[status(thm)],[836]) ).
cnf(1282,plain,
( empty(X1)
| ~ proper_element(X2,powerset(the_carrier(boole_POSet(X1))))
| ~ upper_relstr_subset(X2,boole_POSet(X1))
| ~ filtered_subset(X2,boole_POSet(X1))
| ~ empty(X3)
| ~ element(X2,powerset(the_carrier(boole_POSet(X1))))
| ~ in(X3,X2) ),
inference(csr,[status(thm)],[545,516]) ).
cnf(1283,negated_conjecture,
( empty(cast_as_carrier_subset(esk39_0))
| ~ upper_relstr_subset(esk40_0,boole_POSet(cast_as_carrier_subset(esk39_0)))
| ~ filtered_subset(esk40_0,boole_POSet(cast_as_carrier_subset(esk39_0)))
| ~ empty(X1)
| ~ element(esk40_0,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(esk39_0)))))
| ~ in(X1,esk40_0) ),
inference(spm,[status(thm)],[1282,839,theory(equality)]) ).
cnf(1285,negated_conjecture,
( empty(cast_as_carrier_subset(esk39_0))
| $false
| ~ filtered_subset(esk40_0,boole_POSet(cast_as_carrier_subset(esk39_0)))
| ~ empty(X1)
| ~ element(esk40_0,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(esk39_0)))))
| ~ in(X1,esk40_0) ),
inference(rw,[status(thm)],[1283,840,theory(equality)]) ).
cnf(1286,negated_conjecture,
( empty(cast_as_carrier_subset(esk39_0))
| $false
| $false
| ~ empty(X1)
| ~ element(esk40_0,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(esk39_0)))))
| ~ in(X1,esk40_0) ),
inference(rw,[status(thm)],[1285,841,theory(equality)]) ).
cnf(1287,negated_conjecture,
( empty(cast_as_carrier_subset(esk39_0))
| $false
| $false
| ~ empty(X1)
| $false
| ~ in(X1,esk40_0) ),
inference(rw,[status(thm)],[1286,838,theory(equality)]) ).
cnf(1288,negated_conjecture,
( empty(cast_as_carrier_subset(esk39_0))
| ~ empty(X1)
| ~ in(X1,esk40_0) ),
inference(cn,[status(thm)],[1287,theory(equality)]) ).
cnf(1384,negated_conjecture,
( empty(esk40_0)
| empty_carrier(esk39_0)
| set_difference(esk40_0,singleton(empty_set)) != esk40_0
| ~ upper_relstr_subset(esk40_0,boole_POSet(cast_as_carrier_subset(esk39_0)))
| ~ filtered_subset(esk40_0,boole_POSet(cast_as_carrier_subset(esk39_0)))
| ~ element(esk40_0,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(esk39_0)))))
| ~ one_sorted_str(esk39_0) ),
inference(spm,[status(thm)],[837,512,theory(equality)]) ).
cnf(1390,negated_conjecture,
( empty(esk40_0)
| empty_carrier(esk39_0)
| set_difference(esk40_0,singleton(empty_set)) != esk40_0
| $false
| ~ filtered_subset(esk40_0,boole_POSet(cast_as_carrier_subset(esk39_0)))
| ~ element(esk40_0,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(esk39_0)))))
| ~ one_sorted_str(esk39_0) ),
inference(rw,[status(thm)],[1384,840,theory(equality)]) ).
cnf(1391,negated_conjecture,
( empty(esk40_0)
| empty_carrier(esk39_0)
| set_difference(esk40_0,singleton(empty_set)) != esk40_0
| $false
| $false
| ~ element(esk40_0,powerset(the_carrier(boole_POSet(cast_as_carrier_subset(esk39_0)))))
| ~ one_sorted_str(esk39_0) ),
inference(rw,[status(thm)],[1390,841,theory(equality)]) ).
cnf(1392,negated_conjecture,
( empty(esk40_0)
| empty_carrier(esk39_0)
| set_difference(esk40_0,singleton(empty_set)) != esk40_0
| $false
| $false
| $false
| ~ one_sorted_str(esk39_0) ),
inference(rw,[status(thm)],[1391,838,theory(equality)]) ).
cnf(1393,negated_conjecture,
( empty(esk40_0)
| empty_carrier(esk39_0)
| set_difference(esk40_0,singleton(empty_set)) != esk40_0
| $false
| $false
| $false
| $false ),
inference(rw,[status(thm)],[1392,843,theory(equality)]) ).
cnf(1394,negated_conjecture,
( empty(esk40_0)
| empty_carrier(esk39_0)
| set_difference(esk40_0,singleton(empty_set)) != esk40_0 ),
inference(cn,[status(thm)],[1393,theory(equality)]) ).
cnf(1395,negated_conjecture,
( empty_carrier(esk39_0)
| set_difference(esk40_0,singleton(empty_set)) != esk40_0 ),
inference(sr,[status(thm)],[1394,842,theory(equality)]) ).
cnf(1396,negated_conjecture,
set_difference(esk40_0,singleton(empty_set)) != esk40_0,
inference(sr,[status(thm)],[1395,844,theory(equality)]) ).
cnf(1665,negated_conjecture,
in(empty_set,esk40_0),
inference(spm,[status(thm)],[1396,200,theory(equality)]) ).
cnf(1669,negated_conjecture,
( empty(cast_as_carrier_subset(esk39_0))
| ~ empty(empty_set) ),
inference(spm,[status(thm)],[1288,1665,theory(equality)]) ).
cnf(1671,negated_conjecture,
( empty(cast_as_carrier_subset(esk39_0))
| $false ),
inference(rw,[status(thm)],[1669,285,theory(equality)]) ).
cnf(1672,negated_conjecture,
empty(cast_as_carrier_subset(esk39_0)),
inference(cn,[status(thm)],[1671,theory(equality)]) ).
cnf(1675,negated_conjecture,
( empty_carrier(esk39_0)
| ~ one_sorted_str(esk39_0) ),
inference(spm,[status(thm)],[522,1672,theory(equality)]) ).
cnf(1684,negated_conjecture,
( empty_carrier(esk39_0)
| $false ),
inference(rw,[status(thm)],[1675,843,theory(equality)]) ).
cnf(1685,negated_conjecture,
empty_carrier(esk39_0),
inference(cn,[status(thm)],[1684,theory(equality)]) ).
cnf(1686,negated_conjecture,
$false,
inference(sr,[status(thm)],[1685,844,theory(equality)]) ).
cnf(1687,negated_conjecture,
$false,
1686,
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% % SZS status Started for /home/graph/tptp/TPTP/Problems/SEU/SEU394+1.p
% --creating new selector for []
% -running prover on /tmp/tmpm2d8iW/sel_SEU394+1.p_1 with time limit 29
% -prover status Theorem
% Problem SEU394+1.p solved in phase 0.
% % SZS status Theorem for /home/graph/tptp/TPTP/Problems/SEU/SEU394+1.p
% % SZS status Ended for /home/graph/tptp/TPTP/Problems/SEU/SEU394+1.p
% Solved 1 out of 1.
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% See solution above
% # SZS output end CNFRefutation
%
%------------------------------------------------------------------------------