%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : TOP009-1 : TPTP v8.1.0. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n022.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 0s
% DateTime : Thu Jul 21 21:20:16 EDT 2022
% Result : Timeout 300.05s 300.47s
% Output : None
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : TOP009-1 : TPTP v8.1.0. Released v1.0.0.
% 0.11/0.12 % Command : bliksem %s
% 0.12/0.33 % Computer : n022.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % DateTime : Sun May 29 06:25:23 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.41/1.08 *** allocated 10000 integers for termspace/termends
% 0.41/1.08 *** allocated 10000 integers for clauses
% 0.41/1.08 *** allocated 10000 integers for justifications
% 0.41/1.08 Bliksem 1.12
% 0.41/1.08
% 0.41/1.08
% 0.41/1.08 Automatic Strategy Selection
% 0.41/1.08
% 0.41/1.08 Clauses:
% 0.41/1.08 [
% 0.41/1.08 [ ~( 'element_of_set'( X, 'union_of_members'( Y ) ) ), 'element_of_set'(
% 0.41/1.08 X, f1( Y, X ) ) ],
% 0.41/1.08 [ ~( 'element_of_set'( X, 'union_of_members'( Y ) ) ),
% 0.41/1.08 'element_of_collection'( f1( Y, X ), Y ) ],
% 0.41/1.08 [ 'element_of_set'( X, 'union_of_members'( Y ) ), ~( 'element_of_set'( X
% 0.41/1.08 , Z ) ), ~( 'element_of_collection'( Z, Y ) ) ],
% 0.41/1.08 [ ~( 'element_of_set'( X, 'intersection_of_members'( Y ) ) ), ~(
% 0.41/1.08 'element_of_collection'( Z, Y ) ), 'element_of_set'( X, Z ) ],
% 0.41/1.08 [ 'element_of_set'( X, 'intersection_of_members'( Y ) ),
% 0.41/1.08 'element_of_collection'( f2( Y, X ), Y ) ],
% 0.41/1.08 [ 'element_of_set'( X, 'intersection_of_members'( Y ) ), ~(
% 0.41/1.08 'element_of_set'( X, f2( Y, X ) ) ) ],
% 0.41/1.08 [ ~( 'topological_space'( X, Y ) ), 'equal_sets'( 'union_of_members'( Y
% 0.41/1.08 ), X ) ],
% 0.41/1.08 [ ~( 'topological_space'( X, Y ) ), 'element_of_collection'( 'empty_set'
% 0.41/1.08 , Y ) ],
% 0.41/1.08 [ ~( 'topological_space'( X, Y ) ), 'element_of_collection'( X, Y ) ]
% 0.41/1.08 ,
% 0.41/1.08 [ ~( 'topological_space'( X, Y ) ), ~( 'element_of_collection'( Z, Y ) )
% 0.41/1.08 , ~( 'element_of_collection'( T, Y ) ), 'element_of_collection'(
% 0.41/1.08 'intersection_of_sets'( Z, T ), Y ) ],
% 0.41/1.08 [ ~( 'topological_space'( X, Y ) ), ~( 'subset_collections'( Z, Y ) ),
% 0.41/1.08 'element_of_collection'( 'union_of_members'( Z ), Y ) ],
% 0.41/1.08 [ 'topological_space'( X, Y ), ~( 'equal_sets'( 'union_of_members'( Y )
% 0.41/1.08 , X ) ), ~( 'element_of_collection'( 'empty_set', Y ) ), ~(
% 0.41/1.08 'element_of_collection'( X, Y ) ), 'element_of_collection'( f3( X, Y ), Y
% 0.41/1.08 ), 'subset_collections'( f5( X, Y ), Y ) ],
% 0.41/1.08 [ 'topological_space'( X, Y ), ~( 'equal_sets'( 'union_of_members'( Y )
% 0.41/1.08 , X ) ), ~( 'element_of_collection'( 'empty_set', Y ) ), ~(
% 0.41/1.08 'element_of_collection'( X, Y ) ), 'element_of_collection'( f3( X, Y ), Y
% 0.41/1.08 ), ~( 'element_of_collection'( 'union_of_members'( f5( X, Y ) ), Y ) ) ]
% 0.41/1.08 ,
% 0.41/1.08 [ 'topological_space'( X, Y ), ~( 'equal_sets'( 'union_of_members'( Y )
% 0.41/1.08 , X ) ), ~( 'element_of_collection'( 'empty_set', Y ) ), ~(
% 0.41/1.08 'element_of_collection'( X, Y ) ), 'element_of_collection'( f4( X, Y ), Y
% 0.41/1.08 ), 'subset_collections'( f5( X, Y ), Y ) ],
% 0.41/1.08 [ 'topological_space'( X, Y ), ~( 'equal_sets'( 'union_of_members'( Y )
% 0.41/1.08 , X ) ), ~( 'element_of_collection'( 'empty_set', Y ) ), ~(
% 0.41/1.08 'element_of_collection'( X, Y ) ), 'element_of_collection'( f4( X, Y ), Y
% 0.41/1.08 ), ~( 'element_of_collection'( 'union_of_members'( f5( X, Y ) ), Y ) ) ]
% 0.41/1.08 ,
% 0.41/1.08 [ 'topological_space'( X, Y ), ~( 'equal_sets'( 'union_of_members'( Y )
% 0.41/1.08 , X ) ), ~( 'element_of_collection'( 'empty_set', Y ) ), ~(
% 0.41/1.08 'element_of_collection'( X, Y ) ), ~( 'element_of_collection'(
% 0.41/1.08 'intersection_of_sets'( f3( X, Y ), f4( X, Y ) ), Y ) ),
% 0.41/1.08 'subset_collections'( f5( X, Y ), Y ) ],
% 0.41/1.08 [ 'topological_space'( X, Y ), ~( 'equal_sets'( 'union_of_members'( Y )
% 0.41/1.08 , X ) ), ~( 'element_of_collection'( 'empty_set', Y ) ), ~(
% 0.41/1.08 'element_of_collection'( X, Y ) ), ~( 'element_of_collection'(
% 0.41/1.08 'intersection_of_sets'( f3( X, Y ), f4( X, Y ) ), Y ) ), ~(
% 0.41/1.08 'element_of_collection'( 'union_of_members'( f5( X, Y ) ), Y ) ) ],
% 0.41/1.08 [ ~( open( X, Y, Z ) ), 'topological_space'( Y, Z ) ],
% 0.41/1.08 [ ~( open( X, Y, Z ) ), 'element_of_collection'( X, Z ) ],
% 0.41/1.08 [ open( X, Y, Z ), ~( 'topological_space'( Y, Z ) ), ~(
% 0.41/1.08 'element_of_collection'( X, Z ) ) ],
% 0.41/1.08 [ ~( closed( X, Y, Z ) ), 'topological_space'( Y, Z ) ],
% 0.41/1.08 [ ~( closed( X, Y, Z ) ), open( 'relative_complement_sets'( X, Y ), Y, Z
% 0.41/1.08 ) ],
% 0.41/1.08 [ closed( X, Y, Z ), ~( 'topological_space'( Y, Z ) ), ~( open(
% 0.41/1.08 'relative_complement_sets'( X, Y ), Y, Z ) ) ],
% 0.41/1.08 [ ~( finer( X, Y, Z ) ), 'topological_space'( Z, X ) ],
% 0.41/1.08 [ ~( finer( X, Y, Z ) ), 'topological_space'( Z, Y ) ],
% 0.41/1.08 [ ~( finer( X, Y, Z ) ), 'subset_collections'( Y, X ) ],
% 0.41/1.08 [ finer( X, Y, Z ), ~( 'topological_space'( Z, X ) ), ~(
% 0.41/1.08 'topological_space'( Z, Y ) ), ~( 'subset_collections'( Y, X ) ) ],
% 0.41/1.08 [ ~( basis( X, Y ) ), 'equal_sets'( 'union_of_members'( Y ), X ) ],
% 0.41/1.08 [ ~( basis( X, Y ) ), ~( 'element_of_set'( Z, X ) ), ~(
% 0.41/1.08 'element_of_collection'( T, Y ) ), ~( 'element_of_collection'( U, Y ) ),
% 0.41/1.08 ~( 'element_of_set'( Z, 'intersection_of_sets'( T, U ) ) ),
% 0.41/1.08 'element_of_set'( Z, f6( X, Y, Z, T, U ) ) ],
% 0.41/1.08 [ ~( basis( X, Y ) ), ~( 'element_of_set'( Z, X ) ), ~(
% 0.41/1.08 'element_of_collection'( T, Y ) ), ~( 'element_of_collection'( U, Y ) ),
% 0.41/1.08 ~( 'element_of_set'( Z, 'intersection_of_sets'( T, U ) ) ),
% 0.41/1.08 'element_of_collection'( f6( X, Y, Z, T, U ), Y ) ],
% 0.41/1.08 [ ~( basis( X, Y ) ), ~( 'element_of_set'( Z, X ) ), ~(
% 0.41/1.08 'element_of_collection'( T, Y ) ), ~( 'element_of_collection'( U, Y ) ),
% 0.41/1.08 ~( 'element_of_set'( Z, 'intersection_of_sets'( T, U ) ) ), 'subset_sets'(
% 0.41/1.08 f6( X, Y, Z, T, U ), 'intersection_of_sets'( T, U ) ) ],
% 0.41/1.08 [ basis( X, Y ), ~( 'equal_sets'( 'union_of_members'( Y ), X ) ),
% 0.41/1.08 'element_of_set'( f7( X, Y ), X ) ],
% 0.41/1.08 [ basis( X, Y ), ~( 'equal_sets'( 'union_of_members'( Y ), X ) ),
% 0.41/1.08 'element_of_collection'( f8( X, Y ), Y ) ],
% 0.41/1.08 [ basis( X, Y ), ~( 'equal_sets'( 'union_of_members'( Y ), X ) ),
% 0.41/1.08 'element_of_collection'( f9( X, Y ), Y ) ],
% 0.41/1.08 [ basis( X, Y ), ~( 'equal_sets'( 'union_of_members'( Y ), X ) ),
% 0.41/1.08 'element_of_set'( f7( X, Y ), 'intersection_of_sets'( f8( X, Y ), f9( X,
% 0.41/1.08 Y ) ) ) ],
% 0.41/1.08 [ basis( X, Y ), ~( 'equal_sets'( 'union_of_members'( Y ), X ) ), ~(
% 0.41/1.08 'element_of_set'( f7( X, Y ), Z ) ), ~( 'element_of_collection'( Z, Y ) )
% 0.41/1.08 , ~( 'subset_sets'( Z, 'intersection_of_sets'( f8( X, Y ), f9( X, Y ) ) )
% 0.41/1.08 ) ],
% 0.41/1.08 [ ~( 'element_of_collection'( X, 'top_of_basis'( Y ) ) ), ~(
% 0.41/1.08 'element_of_set'( Z, X ) ), 'element_of_set'( Z, f10( Y, X, Z ) ) ],
% 0.41/1.08 [ ~( 'element_of_collection'( X, 'top_of_basis'( Y ) ) ), ~(
% 0.41/1.08 'element_of_set'( Z, X ) ), 'element_of_collection'( f10( Y, X, Z ), Y )
% 0.41/1.08 ],
% 0.41/1.08 [ ~( 'element_of_collection'( X, 'top_of_basis'( Y ) ) ), ~(
% 0.41/1.08 'element_of_set'( Z, X ) ), 'subset_sets'( f10( Y, X, Z ), X ) ],
% 0.41/1.08 [ 'element_of_collection'( X, 'top_of_basis'( Y ) ), 'element_of_set'(
% 0.41/1.08 f11( Y, X ), X ) ],
% 0.41/1.08 [ 'element_of_collection'( X, 'top_of_basis'( Y ) ), ~( 'element_of_set'(
% 0.41/1.08 f11( Y, X ), Z ) ), ~( 'element_of_collection'( Z, Y ) ), ~(
% 0.41/1.08 'subset_sets'( Z, X ) ) ],
% 0.41/1.08 [ ~( 'element_of_collection'( X, 'subspace_topology'( Y, Z, T ) ) ),
% 0.41/1.08 'topological_space'( Y, Z ) ],
% 0.41/1.08 [ ~( 'element_of_collection'( X, 'subspace_topology'( Y, Z, T ) ) ),
% 0.41/1.08 'subset_sets'( T, Y ) ],
% 0.41/1.08 [ ~( 'element_of_collection'( X, 'subspace_topology'( Y, Z, T ) ) ),
% 0.41/1.08 'element_of_collection'( f12( Y, Z, T, X ), Z ) ],
% 0.41/1.08 [ ~( 'element_of_collection'( X, 'subspace_topology'( Y, Z, T ) ) ),
% 0.41/1.08 'equal_sets'( X, 'intersection_of_sets'( T, f12( Y, Z, T, X ) ) ) ],
% 0.41/1.08 [ 'element_of_collection'( X, 'subspace_topology'( Y, Z, T ) ), ~(
% 0.41/1.08 'topological_space'( Y, Z ) ), ~( 'subset_sets'( T, Y ) ), ~(
% 0.41/1.08 'element_of_collection'( U, Z ) ), ~( 'equal_sets'( X,
% 0.41/1.08 'intersection_of_sets'( T, U ) ) ) ],
% 0.41/1.08 [ ~( 'element_of_set'( X, interior( Y, Z, T ) ) ), 'topological_space'(
% 0.41/1.08 Z, T ) ],
% 0.41/1.08 [ ~( 'element_of_set'( X, interior( Y, Z, T ) ) ), 'subset_sets'( Y, Z )
% 0.41/1.08 ],
% 0.41/1.08 [ ~( 'element_of_set'( X, interior( Y, Z, T ) ) ), 'element_of_set'( X,
% 0.41/1.08 f13( Y, Z, T, X ) ) ],
% 0.41/1.08 [ ~( 'element_of_set'( X, interior( Y, Z, T ) ) ), 'subset_sets'( f13( Y
% 0.41/1.08 , Z, T, X ), Y ) ],
% 0.41/1.08 [ ~( 'element_of_set'( X, interior( Y, Z, T ) ) ), open( f13( Y, Z, T, X
% 0.41/1.08 ), Z, T ) ],
% 0.41/1.08 [ 'element_of_set'( X, interior( Y, Z, T ) ), ~( 'topological_space'( Z
% 0.41/1.08 , T ) ), ~( 'subset_sets'( Y, Z ) ), ~( 'element_of_set'( X, U ) ), ~(
% 0.41/1.08 'subset_sets'( U, Y ) ), ~( open( U, Z, T ) ) ],
% 0.41/1.08 [ ~( 'element_of_set'( X, closure( Y, Z, T ) ) ), 'topological_space'( Z
% 0.41/1.08 , T ) ],
% 0.41/1.08 [ ~( 'element_of_set'( X, closure( Y, Z, T ) ) ), 'subset_sets'( Y, Z )
% 0.41/1.08 ],
% 0.41/1.08 [ ~( 'element_of_set'( X, closure( Y, Z, T ) ) ), ~( 'subset_sets'( Y, U
% 0.41/1.08 ) ), ~( closed( U, Z, T ) ), 'element_of_set'( X, U ) ],
% 0.41/1.08 [ 'element_of_set'( X, closure( Y, Z, T ) ), ~( 'topological_space'( Z,
% 0.41/1.08 T ) ), ~( 'subset_sets'( Y, Z ) ), 'subset_sets'( Y, f14( Y, Z, T, X ) )
% 0.41/1.08 ],
% 0.41/1.08 [ 'element_of_set'( X, closure( Y, Z, T ) ), ~( 'topological_space'( Z,
% 0.41/1.08 T ) ), ~( 'subset_sets'( Y, Z ) ), closed( f14( Y, Z, T, X ), Z, T ) ]
% 0.41/1.08 ,
% 0.41/1.08 [ 'element_of_set'( X, closure( Y, Z, T ) ), ~( 'topological_space'( Z,
% 0.41/1.08 T ) ), ~( 'subset_sets'( Y, Z ) ), ~( 'element_of_set'( X, f14( Y, Z, T,
% 0.41/1.08 X ) ) ) ],
% 0.41/1.08 [ ~( neighborhood( X, Y, Z, T ) ), 'topological_space'( Z, T ) ],
% 0.41/1.08 [ ~( neighborhood( X, Y, Z, T ) ), open( X, Z, T ) ],
% 0.41/1.08 [ ~( neighborhood( X, Y, Z, T ) ), 'element_of_set'( Y, X ) ],
% 0.41/1.08 [ neighborhood( X, Y, Z, T ), ~( 'topological_space'( Z, T ) ), ~( open(
% 0.41/1.08 X, Z, T ) ), ~( 'element_of_set'( Y, X ) ) ],
% 0.41/1.08 [ ~( 'limit_point'( X, Y, Z, T ) ), 'topological_space'( Z, T ) ],
% 0.41/1.08 [ ~( 'limit_point'( X, Y, Z, T ) ), 'subset_sets'( Y, Z ) ],
% 0.41/1.08 [ ~( 'limit_point'( X, Y, Z, T ) ), ~( neighborhood( U, X, Z, T ) ),
% 0.41/1.08 'element_of_set'( f15( X, Y, Z, T, U ), 'intersection_of_sets'( U, Y ) )
% 0.41/1.08 ],
% 0.41/1.08 [ ~( 'limit_point'( X, Y, Z, T ) ), ~( neighborhood( U, X, Z, T ) ), ~(
% 0.41/1.08 'eq_p'( f15( X, Y, Z, T, U ), X ) ) ],
% 0.41/1.08 [ 'limit_point'( X, Y, Z, T ), ~( 'topological_space'( Z, T ) ), ~(
% 0.41/1.08 'subset_sets'( Y, Z ) ), neighborhood( f16( X, Y, Z, T ), X, Z, T ) ]
% 0.41/1.08 ,
% 0.41/1.08 [ 'limit_point'( X, Y, Z, T ), ~( 'topological_space'( Z, T ) ), ~(
% 0.41/1.08 'subset_sets'( Y, Z ) ), ~( 'element_of_set'( U, 'intersection_of_sets'(
% 0.41/1.08 f16( X, Y, Z, T ), Y ) ) ), 'eq_p'( U, X ) ],
% 0.41/1.08 [ ~( 'element_of_set'( X, boundary( Y, Z, T ) ) ), 'topological_space'(
% 0.41/1.08 Z, T ) ],
% 0.41/1.08 [ ~( 'element_of_set'( X, boundary( Y, Z, T ) ) ), 'element_of_set'( X,
% 0.41/1.08 closure( Y, Z, T ) ) ],
% 0.41/1.08 [ ~( 'element_of_set'( X, boundary( Y, Z, T ) ) ), 'element_of_set'( X,
% 0.41/1.08 closure( 'relative_complement_sets'( Y, Z ), Z, T ) ) ],
% 0.41/1.08 [ 'element_of_set'( X, boundary( Y, Z, T ) ), ~( 'topological_space'( Z
% 0.41/1.08 , T ) ), ~( 'element_of_set'( X, closure( Y, Z, T ) ) ), ~(
% 0.41/1.08 'element_of_set'( X, closure( 'relative_complement_sets'( Y, Z ), Z, T )
% 0.41/1.08 ) ) ],
% 0.41/1.08 [ ~( hausdorff( X, Y ) ), 'topological_space'( X, Y ) ],
% 0.41/1.08 [ ~( hausdorff( X, Y ) ), ~( 'element_of_set'( Z, X ) ), ~(
% 0.41/1.08 'element_of_set'( T, X ) ), 'eq_p'( Z, T ), neighborhood( f17( X, Y, Z, T
% 0.41/1.08 ), Z, X, Y ) ],
% 0.41/1.08 [ ~( hausdorff( X, Y ) ), ~( 'element_of_set'( Z, X ) ), ~(
% 0.41/1.08 'element_of_set'( T, X ) ), 'eq_p'( Z, T ), neighborhood( f18( X, Y, Z, T
% 0.41/1.08 ), T, X, Y ) ],
% 0.41/1.08 [ ~( hausdorff( X, Y ) ), ~( 'element_of_set'( Z, X ) ), ~(
% 0.41/1.08 'element_of_set'( T, X ) ), 'eq_p'( Z, T ), 'disjoint_s'( f17( X, Y, Z, T
% 0.41/1.08 ), f18( X, Y, Z, T ) ) ],
% 0.41/1.08 [ hausdorff( X, Y ), ~( 'topological_space'( X, Y ) ), 'element_of_set'(
% 0.41/1.08 f19( X, Y ), X ) ],
% 0.41/1.08 [ hausdorff( X, Y ), ~( 'topological_space'( X, Y ) ), 'element_of_set'(
% 0.41/1.08 f20( X, Y ), X ) ],
% 0.41/1.08 [ hausdorff( X, Y ), ~( 'topological_space'( X, Y ) ), ~( 'eq_p'( f19( X
% 0.41/1.08 , Y ), f20( X, Y ) ) ) ],
% 0.41/1.08 [ hausdorff( X, Y ), ~( 'topological_space'( X, Y ) ), ~( neighborhood(
% 0.41/1.08 Z, f19( X, Y ), X, Y ) ), ~( neighborhood( T, f20( X, Y ), X, Y ) ), ~(
% 0.41/1.08 'disjoint_s'( Z, T ) ) ],
% 0.41/1.08 [ ~( separation( X, Y, Z, T ) ), 'topological_space'( Z, T ) ],
% 0.41/1.08 [ ~( separation( X, Y, Z, T ) ), ~( 'equal_sets'( X, 'empty_set' ) ) ]
% 0.41/1.08 ,
% 0.41/1.08 [ ~( separation( X, Y, Z, T ) ), ~( 'equal_sets'( Y, 'empty_set' ) ) ]
% 0.41/1.08 ,
% 0.41/1.08 [ ~( separation( X, Y, Z, T ) ), 'element_of_collection'( X, T ) ],
% 0.41/1.08 [ ~( separation( X, Y, Z, T ) ), 'element_of_collection'( Y, T ) ],
% 0.41/1.08 [ ~( separation( X, Y, Z, T ) ), 'equal_sets'( 'union_of_sets'( X, Y ),
% 0.41/1.08 Z ) ],
% 0.41/1.08 [ ~( separation( X, Y, Z, T ) ), 'disjoint_s'( X, Y ) ],
% 0.41/1.08 [ separation( X, Y, Z, T ), ~( 'topological_space'( Z, T ) ),
% 0.41/1.08 'equal_sets'( X, 'empty_set' ), 'equal_sets'( Y, 'empty_set' ), ~(
% 0.41/1.08 'element_of_collection'( X, T ) ), ~( 'element_of_collection'( Y, T ) ),
% 0.41/1.08 ~( 'equal_sets'( 'union_of_sets'( X, Y ), Z ) ), ~( 'disjoint_s'( X, Y )
% 0.41/1.08 ) ],
% 0.41/1.08 [ ~( 'connected_space'( X, Y ) ), 'topological_space'( X, Y ) ],
% 0.41/1.08 [ ~( 'connected_space'( X, Y ) ), ~( separation( Z, T, X, Y ) ) ],
% 0.41/1.08 [ 'connected_space'( X, Y ), ~( 'topological_space'( X, Y ) ),
% 0.41/1.08 separation( f21( X, Y ), f22( X, Y ), X, Y ) ],
% 0.41/1.08 [ ~( 'connected_set'( X, Y, Z ) ), 'topological_space'( Y, Z ) ],
% 0.41/1.08 [ ~( 'connected_set'( X, Y, Z ) ), 'subset_sets'( X, Y ) ],
% 0.41/1.08 [ ~( 'connected_set'( X, Y, Z ) ), 'connected_space'( X,
% 3.81/4.19 'subspace_topology'( Y, Z, X ) ) ],
% 3.81/4.19 [ 'connected_set'( X, Y, Z ), ~( 'topological_space'( Y, Z ) ), ~(
% 3.81/4.19 'subset_sets'( X, Y ) ), ~( 'connected_space'( X, 'subspace_topology'( Y
% 3.81/4.19 , Z, X ) ) ) ],
% 3.81/4.19 [ ~( 'open_covering'( X, Y, Z ) ), 'topological_space'( Y, Z ) ],
% 3.81/4.19 [ ~( 'open_covering'( X, Y, Z ) ), 'subset_collections'( X, Z ) ],
% 3.81/4.19 [ ~( 'open_covering'( X, Y, Z ) ), 'equal_sets'( 'union_of_members'( X )
% 3.81/4.19 , Y ) ],
% 3.81/4.19 [ 'open_covering'( X, Y, Z ), ~( 'topological_space'( Y, Z ) ), ~(
% 3.81/4.19 'subset_collections'( X, Z ) ), ~( 'equal_sets'( 'union_of_members'( X )
% 3.81/4.19 , Y ) ) ],
% 3.81/4.19 [ ~( 'compact_space'( X, Y ) ), 'topological_space'( X, Y ) ],
% 3.81/4.19 [ ~( 'compact_space'( X, Y ) ), ~( 'open_covering'( Z, X, Y ) ), finite(
% 3.81/4.19 f23( X, Y, Z ) ) ],
% 3.81/4.19 [ ~( 'compact_space'( X, Y ) ), ~( 'open_covering'( Z, X, Y ) ),
% 3.81/4.19 'subset_collections'( f23( X, Y, Z ), Z ) ],
% 3.81/4.19 [ ~( 'compact_space'( X, Y ) ), ~( 'open_covering'( Z, X, Y ) ),
% 3.81/4.19 'open_covering'( f23( X, Y, Z ), X, Y ) ],
% 3.81/4.19 [ 'compact_space'( X, Y ), ~( 'topological_space'( X, Y ) ),
% 3.81/4.19 'open_covering'( f24( X, Y ), X, Y ) ],
% 3.81/4.19 [ 'compact_space'( X, Y ), ~( 'topological_space'( X, Y ) ), ~( finite(
% 3.81/4.19 Z ) ), ~( 'subset_collections'( Z, f24( X, Y ) ) ), ~( 'open_covering'( Z
% 3.81/4.19 , X, Y ) ) ],
% 3.81/4.19 [ ~( 'compact_set'( X, Y, Z ) ), 'topological_space'( Y, Z ) ],
% 3.81/4.19 [ ~( 'compact_set'( X, Y, Z ) ), 'subset_sets'( X, Y ) ],
% 3.81/4.19 [ ~( 'compact_set'( X, Y, Z ) ), 'compact_space'( X, 'subspace_topology'(
% 3.81/4.19 Y, Z, X ) ) ],
% 3.81/4.19 [ 'compact_set'( X, Y, Z ), ~( 'topological_space'( Y, Z ) ), ~(
% 3.81/4.19 'subset_sets'( X, Y ) ), ~( 'compact_space'( X, 'subspace_topology'( Y, Z
% 3.81/4.19 , X ) ) ) ],
% 3.81/4.19 [ open( cy, cx, ct ) ],
% 3.81/4.19 [ open( a, cy, 'subspace_topology'( cx, ct, cy ) ) ],
% 3.81/4.19 [ ~( open( a, cx, ct ) ) ]
% 3.81/4.19 ] .
% 3.81/4.19
% 3.81/4.19
% 3.81/4.19 percentage equality = 0.000000, percentage horn = 0.794643
% 3.81/4.19 This a non-horn, non-equality problem
% 3.81/4.19
% 3.81/4.19
% 3.81/4.19 Options Used:
% 3.81/4.19
% 3.81/4.19 useres = 1
% 3.81/4.19 useparamod = 0
% 3.81/4.19 useeqrefl = 0
% 3.81/4.19 useeqfact = 0
% 3.81/4.19 usefactor = 1
% 3.81/4.19 usesimpsplitting = 0
% 3.81/4.19 usesimpdemod = 0
% 3.81/4.19 usesimpres = 3
% 3.81/4.19
% 3.81/4.19 resimpinuse = 1000
% 3.81/4.19 resimpclauses = 20000
% 3.81/4.19 substype = standard
% 3.81/4.19 backwardsubs = 1
% 3.81/4.19 selectoldest = 5
% 3.81/4.19
% 3.81/4.19 litorderings [0] = split
% 3.81/4.19 litorderings [1] = liftord
% 3.81/4.19
% 3.81/4.19 termordering = none
% 3.81/4.19
% 3.81/4.19 litapriori = 1
% 3.81/4.19 termapriori = 0
% 3.81/4.19 litaposteriori = 0
% 3.81/4.19 termaposteriori = 0
% 3.81/4.19 demodaposteriori = 0
% 3.81/4.19 ordereqreflfact = 0
% 3.81/4.19
% 3.81/4.19 litselect = none
% 3.81/4.19
% 3.81/4.19 maxweight = 15
% 3.81/4.19 maxdepth = 30000
% 3.81/4.19 maxlength = 115
% 3.81/4.19 maxnrvars = 195
% 3.81/4.19 excuselevel = 1
% 3.81/4.19 increasemaxweight = 1
% 3.81/4.19
% 3.81/4.19 maxselected = 10000000
% 3.81/4.19 maxnrclauses = 10000000
% 3.81/4.19
% 3.81/4.19 showgenerated = 0
% 3.81/4.19 showkept = 0
% 3.81/4.19 showselected = 0
% 3.81/4.19 showdeleted = 0
% 3.81/4.19 showresimp = 1
% 3.81/4.19 showstatus = 2000
% 3.81/4.19
% 3.81/4.19 prologoutput = 1
% 3.81/4.19 nrgoals = 5000000
% 3.81/4.19 totalproof = 1
% 3.81/4.19
% 3.81/4.19 Symbols occurring in the translation:
% 3.81/4.19
% 3.81/4.19 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 3.81/4.19 . [1, 2] (w:1, o:48, a:1, s:1, b:0),
% 3.81/4.19 ! [4, 1] (w:0, o:39, a:1, s:1, b:0),
% 3.81/4.19 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 3.81/4.19 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 3.81/4.19 'union_of_members' [41, 1] (w:1, o:45, a:1, s:1, b:0),
% 3.81/4.19 'element_of_set' [42, 2] (w:1, o:76, a:1, s:1, b:0),
% 3.81/4.19 f1 [43, 2] (w:1, o:80, a:1, s:1, b:0),
% 3.81/4.19 'element_of_collection' [44, 2] (w:1, o:77, a:1, s:1, b:0),
% 3.81/4.19 'intersection_of_members' [46, 1] (w:1, o:46, a:1, s:1, b:0),
% 3.81/4.19 f2 [48, 2] (w:1, o:83, a:1, s:1, b:0),
% 3.81/4.19 'topological_space' [51, 2] (w:1, o:87, a:1, s:1, b:0),
% 3.81/4.19 'equal_sets' [52, 2] (w:1, o:78, a:1, s:1, b:0),
% 3.81/4.19 'empty_set' [53, 0] (w:1, o:24, a:1, s:1, b:0),
% 3.81/4.19 'intersection_of_sets' [56, 2] (w:1, o:89, a:1, s:1, b:0),
% 3.81/4.19 'subset_collections' [57, 2] (w:1, o:85, a:1, s:1, b:0),
% 3.81/4.19 f3 [58, 2] (w:1, o:94, a:1, s:1, b:0),
% 3.81/4.19 f5 [59, 2] (w:1, o:96, a:1, s:1, b:0),
% 3.81/4.19 f4 [60, 2] (w:1, o:95, a:1, s:1, b:0),
% 3.81/4.19 open [61, 3] (w:1, o:102, a:1, s:1, b:0),
% 3.81/4.19 closed [62, 3] (w:1, o:104, a:1, s:1, b:0),
% 3.81/4.19 'relative_complement_sets' [63, 2] (w:1, o:84, a:1, s:1, b:0),
% 3.81/4.19 finer [65, 3] (w:1, o:105, a:1, s:1, b:0),
% 33.76/34.17 basis [66, 2] (w:1, o:97, a:1, s:1, b:0),
% 33.76/34.17 f6 [69, 5] (w:1, o:123, a:1, s:1, b:0),
% 33.76/34.17 'subset_sets' [70, 2] (w:1, o:86, a:1, s:1, b:0),
% 33.76/34.17 f7 [71, 2] (w:1, o:98, a:1, s:1, b:0),
% 33.76/34.17 f8 [72, 2] (w:1, o:99, a:1, s:1, b:0),
% 33.76/34.17 f9 [73, 2] (w:1, o:100, a:1, s:1, b:0),
% 33.76/34.17 'top_of_basis' [75, 1] (w:1, o:44, a:1, s:1, b:0),
% 33.76/34.17 f10 [76, 3] (w:1, o:106, a:1, s:1, b:0),
% 33.76/34.17 f11 [77, 2] (w:1, o:81, a:1, s:1, b:0),
% 33.76/34.17 'subspace_topology' [79, 3] (w:1, o:107, a:1, s:1, b:0),
% 33.76/34.17 f12 [80, 4] (w:1, o:114, a:1, s:1, b:0),
% 33.76/34.17 interior [82, 3] (w:1, o:108, a:1, s:1, b:0),
% 33.76/34.17 f13 [83, 4] (w:1, o:115, a:1, s:1, b:0),
% 33.76/34.17 closure [85, 3] (w:1, o:109, a:1, s:1, b:0),
% 33.76/34.17 f14 [87, 4] (w:1, o:116, a:1, s:1, b:0),
% 33.76/34.17 neighborhood [88, 4] (w:1, o:117, a:1, s:1, b:0),
% 33.76/34.17 'limit_point' [89, 4] (w:1, o:118, a:1, s:1, b:0),
% 33.76/34.17 f15 [90, 5] (w:1, o:124, a:1, s:1, b:0),
% 33.76/34.17 'eq_p' [91, 2] (w:1, o:79, a:1, s:1, b:0),
% 33.76/34.17 f16 [92, 4] (w:1, o:119, a:1, s:1, b:0),
% 33.76/34.17 boundary [94, 3] (w:1, o:103, a:1, s:1, b:0),
% 33.76/34.17 hausdorff [95, 2] (w:1, o:88, a:1, s:1, b:0),
% 33.76/34.17 f17 [98, 4] (w:1, o:120, a:1, s:1, b:0),
% 33.76/34.17 f18 [99, 4] (w:1, o:121, a:1, s:1, b:0),
% 33.76/34.17 'disjoint_s' [100, 2] (w:1, o:75, a:1, s:1, b:0),
% 33.76/34.17 f19 [101, 2] (w:1, o:82, a:1, s:1, b:0),
% 33.76/34.17 f20 [102, 2] (w:1, o:90, a:1, s:1, b:0),
% 33.76/34.17 separation [107, 4] (w:1, o:122, a:1, s:1, b:0),
% 33.76/34.17 'union_of_sets' [108, 2] (w:1, o:101, a:1, s:1, b:0),
% 33.76/34.17 'connected_space' [109, 2] (w:1, o:74, a:1, s:1, b:0),
% 33.76/34.17 f21 [110, 2] (w:1, o:91, a:1, s:1, b:0),
% 33.76/34.17 f22 [111, 2] (w:1, o:92, a:1, s:1, b:0),
% 33.76/34.17 'connected_set' [112, 3] (w:1, o:111, a:1, s:1, b:0),
% 33.76/34.17 'open_covering' [113, 3] (w:1, o:112, a:1, s:1, b:0),
% 33.76/34.17 'compact_space' [114, 2] (w:1, o:73, a:1, s:1, b:0),
% 33.76/34.17 f23 [116, 3] (w:1, o:113, a:1, s:1, b:0),
% 33.76/34.17 finite [117, 1] (w:1, o:47, a:1, s:1, b:0),
% 33.76/34.17 f24 [118, 2] (w:1, o:93, a:1, s:1, b:0),
% 33.76/34.17 'compact_set' [120, 3] (w:1, o:110, a:1, s:1, b:0),
% 33.76/34.17 cy [121, 0] (w:1, o:36, a:1, s:1, b:0),
% 33.76/34.17 cx [122, 0] (w:1, o:35, a:1, s:1, b:0),
% 33.76/34.17 ct [123, 0] (w:1, o:37, a:1, s:1, b:0),
% 33.76/34.17 a [124, 0] (w:1, o:38, a:1, s:1, b:0).
% 33.76/34.17
% 33.76/34.17
% 33.76/34.17 Starting Search:
% 33.76/34.17
% 33.76/34.17 Resimplifying inuse:
% 33.76/34.17 Done
% 33.76/34.17
% 33.76/34.17
% 33.76/34.17 Intermediate Status:
% 33.76/34.17 Generated: 2895
% 33.76/34.17 Kept: 2000
% 33.76/34.17 Inuse: 332
% 33.76/34.17 Deleted: 8
% 33.76/34.17 Deletedinuse: 3
% 33.76/34.17
% 33.76/34.17 Resimplifying inuse:
% 33.76/34.17 Done
% 33.76/34.17
% 33.76/34.17 Resimplifying inuse:
% 33.76/34.17 Done
% 33.76/34.17
% 33.76/34.17
% 33.76/34.17 Intermediate Status:
% 33.76/34.17 Generated: 9101
% 33.76/34.17 Kept: 4003
% 33.76/34.17 Inuse: 578
% 33.76/34.17 Deleted: 15
% 33.76/34.17 Deletedinuse: 3
% 33.76/34.17
% 33.76/34.17 Resimplifying inuse:
% 33.76/34.17 Done
% 33.76/34.17
% 33.76/34.17 Resimplifying inuse:
% 33.76/34.17 Done
% 33.76/34.17
% 33.76/34.17
% 33.76/34.17 Intermediate Status:
% 33.76/34.17 Generated: 19636
% 33.76/34.17 Kept: 6178
% 33.76/34.17 Inuse: 788
% 33.76/34.17 Deleted: 15
% 33.76/34.17 Deletedinuse: 3
% 33.76/34.17
% 33.76/34.17 Resimplifying inuse:
% 33.76/34.17 Done
% 33.76/34.17
% 33.76/34.17 Resimplifying inuse:
% 33.76/34.17 Done
% 33.76/34.17
% 33.76/34.17
% 33.76/34.17 Intermediate Status:
% 33.76/34.17 Generated: 22829
% 33.76/34.17 Kept: 8335
% 33.76/34.17 Inuse: 802
% 33.76/34.17 Deleted: 15
% 33.76/34.17 Deletedinuse: 3
% 33.76/34.17
% 33.76/34.17 Resimplifying inuse:
% 33.76/34.17 Done
% 33.76/34.17
% 33.76/34.17 Resimplifying inuse:
% 33.76/34.17 Done
% 33.76/34.17
% 33.76/34.17
% 33.76/34.17 Intermediate Status:
% 33.76/34.17 Generated: 25866
% 33.76/34.17 Kept: 10521
% 33.76/34.17 Inuse: 813
% 33.76/34.17 Deleted: 15
% 33.76/34.17 Deletedinuse: 3
% 33.76/34.17
% 33.76/34.17 Resimplifying inuse:
% 33.76/34.17 Done
% 33.76/34.17
% 33.76/34.17 Resimplifying inuse:
% 33.76/34.17 Done
% 33.76/34.17
% 33.76/34.17
% 33.76/34.17 Intermediate Status:
% 33.76/34.17 Generated: 30615
% 33.76/34.17 Kept: 12615
% 33.76/34.17 Inuse: 847
% 33.76/34.17 Deleted: 19
% 33.76/34.17 Deletedinuse: 4
% 33.76/34.17
% 33.76/34.17 Resimplifying inuse:
% 33.76/34.17 Done
% 33.76/34.17
% 33.76/34.17 Resimplifying inuse:
% 33.76/34.17 Done
% 33.76/34.17
% 33.76/34.17
% 33.76/34.17 Intermediate Status:
% 33.76/34.17 Generated: 34032
% 33.76/34.17 Kept: 15087
% 33.76/34.17 Inuse: 860
% 33.76/34.17 Deleted: 19
% 33.76/34.17 Deletedinuse: 4
% 33.76/34.17
% 33.76/34.17 Resimplifying inuse:
% 33.76/34.17 Done
% 33.76/34.17
% 33.76/34.17 Resimplifying inuse:
% 33.76/34.17 Done
% 33.76/34.17
% 33.76/34.17
% 33.76/34.17 Intermediate Status:
% 33.76/34.17 Generated: 38502
% 33.76/34.17 Kept: 17110
% 33.76/34.17 Inuse: 893
% 33.76/34.17 Deleted: 21
% 33.76/34.17 Deletedinuse: 4
% 33.76/34.17
% 33.76/34.17 Resimplifying inuse:
% 33.76/34.17 Done
% 33.76/34.17
% 33.76/34.17
% 33.76/34.17 Intermediate Status:
% 33.76/34.17 Generated: 41459
% 33.76/34.17 Kept: 19211
% 33.76/34.17 Inuse: 916
% 33.76/34.17 Deleted: 21
% 33.76/34.17 Deletedinuse: 4
% 33.76/34.17
% 33.76/34.17 Resimplifying inuse:
% 33.76/34.17 Done
% 33.76/34.17
% 33.76/34.17 Resimplifying inuse:
% 33.76/34.17 Done
% 33.76/34.17
% 33.76/34.17 Resimplifying clauses:
% 33.76/34.17 Done
% 33.76/34.17
% 33.76/34.17
% 33.76/34.17 Intermediate Status:
% 33.76/34.17 Generated: 44474
% 33.76/34.17 Kept: 21445
% 33.76/34.17 Inuse: 926
% 33.76/34.17 Deleted: 167
% 33.76/34.17 Deletedinuse: 4
% 33.76/34.17
% 33.76/34.17 Resimplifying inuse:
% 33.76/34.17 Done
% 33.76/34.17
% 33.76/34.17 Resimplifying inuse:
% 33.76/34.17 Done
% 33.76/34.17
% 33.76/34.17
% 33.76/34.17 Intermediate Status:
% 33.76/34.17 Generated: 48837
% 33.76/34.17 Kept: 23445
% 33.76/34.17 Inuse: 947
% 33.76/34.17 Deleted: 167
% 33.76/34.17 Deletedinuse: 4
% 33.76/34.17
% 33.76/34.17 Resimplifying inuse:
% 33.76/34.17 Done
% 33.76/34.17
% 33.76/34.17 Resimplifying inuse:
% 103.86/104.27 Done
% 103.86/104.27
% 103.86/104.27
% 103.86/104.27 Intermediate Status:
% 103.86/104.27 Generated: 52042
% 103.86/104.27 Kept: 25471
% 103.86/104.27 Inuse: 975
% 103.86/104.27 Deleted: 167
% 103.86/104.27 Deletedinuse: 4
% 103.86/104.27
% 103.86/104.27 Resimplifying inuse:
% 103.86/104.27 Done
% 103.86/104.27
% 103.86/104.27 Resimplifying inuse:
% 103.86/104.27 Done
% 103.86/104.27
% 103.86/104.27
% 103.86/104.27 Intermediate Status:
% 103.86/104.27 Generated: 55306
% 103.86/104.27 Kept: 27861
% 103.86/104.27 Inuse: 982
% 103.86/104.27 Deleted: 167
% 103.86/104.27 Deletedinuse: 4
% 103.86/104.27
% 103.86/104.27 Resimplifying inuse:
% 103.86/104.27 Done
% 103.86/104.27
% 103.86/104.27 Resimplifying inuse:
% 103.86/104.27 Done
% 103.86/104.27
% 103.86/104.27
% 103.86/104.27 Intermediate Status:
% 103.86/104.27 Generated: 61130
% 103.86/104.27 Kept: 30487
% 103.86/104.27 Inuse: 1011
% 103.86/104.27 Deleted: 167
% 103.86/104.27 Deletedinuse: 4
% 103.86/104.27
% 103.86/104.27 Resimplifying inuse:
% 103.86/104.27 Done
% 103.86/104.27
% 103.86/104.27 Resimplifying inuse:
% 103.86/104.27 Done
% 103.86/104.27
% 103.86/104.27
% 103.86/104.27 Intermediate Status:
% 103.86/104.27 Generated: 64334
% 103.86/104.27 Kept: 32631
% 103.86/104.27 Inuse: 1032
% 103.86/104.27 Deleted: 167
% 103.86/104.27 Deletedinuse: 4
% 103.86/104.27
% 103.86/104.27 Resimplifying inuse:
% 103.86/104.27 Done
% 103.86/104.27
% 103.86/104.27 Resimplifying inuse:
% 103.86/104.27 Done
% 103.86/104.27
% 103.86/104.27
% 103.86/104.27 Intermediate Status:
% 103.86/104.27 Generated: 67849
% 103.86/104.27 Kept: 34996
% 103.86/104.27 Inuse: 1047
% 103.86/104.27 Deleted: 167
% 103.86/104.27 Deletedinuse: 4
% 103.86/104.27
% 103.86/104.27 Resimplifying inuse:
% 103.86/104.27 Done
% 103.86/104.27
% 103.86/104.27 Resimplifying inuse:
% 103.86/104.27 Done
% 103.86/104.27
% 103.86/104.27
% 103.86/104.27 Intermediate Status:
% 103.86/104.27 Generated: 73304
% 103.86/104.27 Kept: 37627
% 103.86/104.27 Inuse: 1071
% 103.86/104.27 Deleted: 167
% 103.86/104.27 Deletedinuse: 4
% 103.86/104.27
% 103.86/104.27 Resimplifying inuse:
% 103.86/104.27 Done
% 103.86/104.27
% 103.86/104.27 Resimplifying inuse:
% 103.86/104.27 Done
% 103.86/104.27
% 103.86/104.27
% 103.86/104.27 Intermediate Status:
% 103.86/104.27 Generated: 76060
% 103.86/104.27 Kept: 39739
% 103.86/104.27 Inuse: 1087
% 103.86/104.27 Deleted: 167
% 103.86/104.27 Deletedinuse: 4
% 103.86/104.27
% 103.86/104.27 Resimplifying inuse:
% 103.86/104.27 Done
% 103.86/104.27
% 103.86/104.27 Resimplifying clauses:
% 103.86/104.27 Done
% 103.86/104.27
% 103.86/104.27 Resimplifying inuse:
% 103.86/104.27 Done
% 103.86/104.27
% 103.86/104.27
% 103.86/104.27 Intermediate Status:
% 103.86/104.27 Generated: 81680
% 103.86/104.27 Kept: 42272
% 103.86/104.27 Inuse: 1108
% 103.86/104.27 Deleted: 199
% 103.86/104.27 Deletedinuse: 4
% 103.86/104.27
% 103.86/104.27 Resimplifying inuse:
% 103.86/104.27 Done
% 103.86/104.27
% 103.86/104.27 Resimplifying inuse:
% 103.86/104.27 Done
% 103.86/104.27
% 103.86/104.27
% 103.86/104.27 Intermediate Status:
% 103.86/104.27 Generated: 86749
% 103.86/104.27 Kept: 44313
% 103.86/104.27 Inuse: 1121
% 103.86/104.27 Deleted: 199
% 103.86/104.27 Deletedinuse: 4
% 103.86/104.27
% 103.86/104.27 Resimplifying inuse:
% 103.86/104.27 Done
% 103.86/104.27
% 103.86/104.27 Resimplifying inuse:
% 103.86/104.27 Done
% 103.86/104.27
% 103.86/104.27
% 103.86/104.27 Intermediate Status:
% 103.86/104.27 Generated: 89407
% 103.86/104.27 Kept: 46318
% 103.86/104.27 Inuse: 1132
% 103.86/104.27 Deleted: 199
% 103.86/104.27 Deletedinuse: 4
% 103.86/104.27
% 103.86/104.27 Resimplifying inuse:
% 103.86/104.27 Done
% 103.86/104.27
% 103.86/104.27 Resimplifying inuse:
% 103.86/104.27 Done
% 103.86/104.27
% 103.86/104.27
% 103.86/104.27 Intermediate Status:
% 103.86/104.27 Generated: 94513
% 103.86/104.27 Kept: 48349
% 103.86/104.27 Inuse: 1161
% 103.86/104.27 Deleted: 199
% 103.86/104.27 Deletedinuse: 4
% 103.86/104.27
% 103.86/104.27 Resimplifying inuse:
% 103.86/104.27 Done
% 103.86/104.27
% 103.86/104.27 Resimplifying inuse:
% 103.86/104.27 Done
% 103.86/104.27
% 103.86/104.27
% 103.86/104.27 Intermediate Status:
% 103.86/104.27 Generated: 101901
% 103.86/104.27 Kept: 50493
% 103.86/104.27 Inuse: 1210
% 103.86/104.27 Deleted: 203
% 103.86/104.27 Deletedinuse: 6
% 103.86/104.27
% 103.86/104.27 Resimplifying inuse:
% 103.86/104.27 Done
% 103.86/104.27
% 103.86/104.27 Resimplifying inuse:
% 103.86/104.27 Done
% 103.86/104.27
% 103.86/104.27
% 103.86/104.27 Intermediate Status:
% 103.86/104.27 Generated: 110336
% 103.86/104.27 Kept: 52674
% 103.86/104.27 Inuse: 1242
% 103.86/104.27 Deleted: 219
% 103.86/104.27 Deletedinuse: 20
% 103.86/104.27
% 103.86/104.27 Resimplifying inuse:
% 103.86/104.27 Done
% 103.86/104.27
% 103.86/104.27 Resimplifying inuse:
% 103.86/104.27 Done
% 103.86/104.27
% 103.86/104.27
% 103.86/104.27 Intermediate Status:
% 103.86/104.27 Generated: 115957
% 103.86/104.27 Kept: 54725
% 103.86/104.27 Inuse: 1286
% 103.86/104.27 Deleted: 237
% 103.86/104.27 Deletedinuse: 38
% 103.86/104.27
% 103.86/104.27 Resimplifying inuse:
% 103.86/104.27 Done
% 103.86/104.27
% 103.86/104.27 Resimplifying inuse:
% 103.86/104.27 Done
% 103.86/104.27
% 103.86/104.27
% 103.86/104.27 Intermediate Status:
% 103.86/104.27 Generated: 120152
% 103.86/104.27 Kept: 56773
% 103.86/104.27 Inuse: 1329
% 103.86/104.27 Deleted: 237
% 103.86/104.27 Deletedinuse: 38
% 103.86/104.27
% 103.86/104.27 Resimplifying inuse:
% 103.86/104.27 Done
% 103.86/104.27
% 103.86/104.27 Resimplifying inuse:
% 103.86/104.27 Done
% 103.86/104.27
% 103.86/104.27
% 103.86/104.27 Intermediate Status:
% 103.86/104.27 Generated: 125544
% 103.86/104.27 Kept: 58815
% 103.86/104.27 Inuse: 1449
% 103.86/104.27 Deleted: 237
% 103.86/104.27 Deletedinuse: 38
% 103.86/104.27
% 103.86/104.27 Resimplifying inuse:
% 103.86/104.27 Done
% 103.86/104.27
% 103.86/104.27 Resimplifying inuse:
% 103.86/104.27 Done
% 103.86/104.27
% 103.86/104.27 Resimplifying clauses:
% 103.86/104.27 Done
% 103.86/104.27
% 103.86/104.27
% 103.86/104.27 Intermediate Status:
% 103.86/104.27 Generated: 132696
% 103.86/104.27 Kept: 60871
% 103.86/104.27 Inuse: 1548
% 103.86/104.27 Deleted: 591
% 103.86/104.27 Deletedinuse: 38
% 103.86/104.27
% 103.86/104.27 Resimplifying inuse:
% 103.86/104.27 Done
% 103.86/104.27
% 103.86/104.27 Resimplifying inuse:
% 103.86/104.27 Done
% 103.86/104.27
% 103.86/104.27
% 103.86/104.27 Intermediate Status:
% 103.86/104.27 Generated: 137280
% 103.86/104.27 Kept: 62926
% 103.86/104.27 Inuse: 1589
% 103.86/104.27 Deleted: 591
% 103.86/104.27 Deletedinuse: 38
% 103.86/104.27
% 103.86/104.27 Resimplifying inuse:
% 103.86/104.27 Done
% 103.86/104.27
% 103.86/104.27 Resimplifying inuse:
% 103.86/104.27 Done
% 103.86/104.27
% 103.86/104.27
% 103.86/104.27 Intermediate Status:
% 103.86/104.27 Generated: 141728
% 103.86/104.27 Kept: 64978
% 103.86/104.27 Inuse: 1631
% 103.86/104.27 Deleted: 591
% 103.86/104.27 Deletedinuse: 38
% 103.86/104.27
% 103.86/104.27 Resimplifying inuse:
% 103.86/104.27 Done
% 103.86/104.27
% 103.86/104.27 Resimplifying inuse:
% 103.86/104.27 Done
% 103.86/104.27
% 103.86/104.27
% 103.86/104.27 Intermediate Status:
% 103.86/104.27 Generated: 145949
% 103.86/104.27 Kept: 66994
% 103.86/104.27 Inuse: 1672
% 103.86/104.27 Deleted: 591
% 103.86/104.27 Deletedinuse: 38
% 103.86/104.27
% 103.86/104.27 Resimplifying inuse:
% 103.86/104.27 Done
% 103.86/104.27
% 103.86/104.27 Resimplifying inuse:
% 103.86/104.27 Done
% 103.86/104.27
% 103.86/104.27
% 103.86/104.27 Intermediate Status:
% 103.86/104.27 Generated: 150238
% 103.86/104.27 Kept: 69010
% 103.86/104.27 Inuse: 1713
% 103.86/104.27 Deleted: 591
% 103.86/104.27 Deletedinuse: 38
% 103.86/104.27
% 103.86/104.27 Resimplifying inuse:
% 103.86/104.27 Done
% 103.86/104.27
% 103.86/104.27 Resimplifying inuse:
% 103.86/104.27 Done
% 103.86/104.27
% 103.86/104.27
% 103.86/104.27 Intermediate Status:
% 103.86/104.27 Generated: 154323
% 103.86/104.27 Kept: 71056
% 103.86/104.27 Inuse: 1754
% 103.86/104.27 Deleted: 591
% 103.86/104.27 Deletedinuse: 38
% 103.86/104.27
% 103.86/104.27 Resimplifying inuse:
% 103.86/104.27 Done
% 103.86/104.27
% 103.86/104.27 Resimplifying inuse:
% 103.86/104.27 Done
% 103.86/104.27
% 103.86/104.27
% 103.86/104.27 Intermediate Status:
% 103.86/104.27 Generated: 158660
% 103.86/104.27 Kept: 73098
% 103.86/104.27 Inuse: 1797
% 103.86/104.27 Deleted: 591
% 103.86/104.27 Deletedinuse: 38
% 103.86/104.27
% 103.86/104.27 Resimplifying inuse:
% 103.86/104.27 Done
% 103.86/104.27
% 103.86/104.27 Resimplifying inuse:
% 103.86/104.27 Done
% 103.86/104.27
% 103.86/104.27
% 103.86/104.27 Intermediate Status:
% 103.86/104.27 Generated: 162797
% 103.86/104.27 Kept: 75148
% 103.86/104.27 Inuse: 1838
% 103.86/104.27 Deleted: 591
% 198.00/198.43 Deletedinuse: 38
% 198.00/198.43
% 198.00/198.43 Resimplifying inuse:
% 198.00/198.43 Done
% 198.00/198.43
% 198.00/198.43 Resimplifying inuse:
% 198.00/198.43 Done
% 198.00/198.43
% 198.00/198.43
% 198.00/198.43 Intermediate Status:
% 198.00/198.43 Generated: 167583
% 198.00/198.43 Kept: 77185
% 198.00/198.43 Inuse: 1881
% 198.00/198.43 Deleted: 591
% 198.00/198.43 Deletedinuse: 38
% 198.00/198.43
% 198.00/198.43 Resimplifying inuse:
% 198.00/198.43 Done
% 198.00/198.43
% 198.00/198.43 Resimplifying inuse:
% 198.00/198.43 Done
% 198.00/198.43
% 198.00/198.43
% 198.00/198.43 Intermediate Status:
% 198.00/198.43 Generated: 172062
% 198.00/198.43 Kept: 79231
% 198.00/198.43 Inuse: 1922
% 198.00/198.43 Deleted: 591
% 198.00/198.43 Deletedinuse: 38
% 198.00/198.43
% 198.00/198.43 Resimplifying inuse:
% 198.00/198.43 Done
% 198.00/198.43
% 198.00/198.43 Resimplifying inuse:
% 198.00/198.43 Done
% 198.00/198.43
% 198.00/198.43 Resimplifying clauses:
% 198.00/198.43 Done
% 198.00/198.43
% 198.00/198.43
% 198.00/198.43 Intermediate Status:
% 198.00/198.43 Generated: 176378
% 198.00/198.43 Kept: 81231
% 198.00/198.43 Inuse: 1964
% 198.00/198.43 Deleted: 591
% 198.00/198.43 Deletedinuse: 38
% 198.00/198.43
% 198.00/198.43 Resimplifying inuse:
% 198.00/198.43 Done
% 198.00/198.43
% 198.00/198.43 Resimplifying inuse:
% 198.00/198.43 Done
% 198.00/198.43
% 198.00/198.43
% 198.00/198.43 Intermediate Status:
% 198.00/198.43 Generated: 180499
% 198.00/198.43 Kept: 83277
% 198.00/198.43 Inuse: 2006
% 198.00/198.43 Deleted: 591
% 198.00/198.43 Deletedinuse: 38
% 198.00/198.43
% 198.00/198.43 Resimplifying inuse:
% 198.00/198.43 Done
% 198.00/198.43
% 198.00/198.43 Resimplifying inuse:
% 198.00/198.43 Done
% 198.00/198.43
% 198.00/198.43
% 198.00/198.43 Intermediate Status:
% 198.00/198.43 Generated: 184769
% 198.00/198.43 Kept: 85277
% 198.00/198.43 Inuse: 2048
% 198.00/198.43 Deleted: 591
% 198.00/198.43 Deletedinuse: 38
% 198.00/198.43
% 198.00/198.43 Resimplifying inuse:
% 198.00/198.43 Done
% 198.00/198.43
% 198.00/198.43 Resimplifying inuse:
% 198.00/198.43 Done
% 198.00/198.43
% 198.00/198.43
% 198.00/198.43 Intermediate Status:
% 198.00/198.43 Generated: 188792
% 198.00/198.43 Kept: 87323
% 198.00/198.43 Inuse: 2089
% 198.00/198.43 Deleted: 591
% 198.00/198.43 Deletedinuse: 38
% 198.00/198.43
% 198.00/198.43 Resimplifying inuse:
% 198.00/198.43 Done
% 198.00/198.43
% 198.00/198.43 Resimplifying inuse:
% 198.00/198.43 Done
% 198.00/198.43
% 198.00/198.43
% 198.00/198.43 Intermediate Status:
% 198.00/198.43 Generated: 193091
% 198.00/198.43 Kept: 89349
% 198.00/198.43 Inuse: 2133
% 198.00/198.43 Deleted: 591
% 198.00/198.43 Deletedinuse: 38
% 198.00/198.43
% 198.00/198.43 Resimplifying inuse:
% 198.00/198.43 Done
% 198.00/198.43
% 198.00/198.43 Resimplifying inuse:
% 198.00/198.43 Done
% 198.00/198.43
% 198.00/198.43
% 198.00/198.43 Intermediate Status:
% 198.00/198.43 Generated: 198252
% 198.00/198.43 Kept: 91395
% 198.00/198.43 Inuse: 2174
% 198.00/198.43 Deleted: 591
% 198.00/198.43 Deletedinuse: 38
% 198.00/198.43
% 198.00/198.43 Resimplifying inuse:
% 198.00/198.43 Done
% 198.00/198.43
% 198.00/198.43 Resimplifying inuse:
% 198.00/198.43 Done
% 198.00/198.43
% 198.00/198.43
% 198.00/198.43 Intermediate Status:
% 198.00/198.43 Generated: 205784
% 198.00/198.43 Kept: 93423
% 198.00/198.43 Inuse: 2218
% 198.00/198.43 Deleted: 591
% 198.00/198.43 Deletedinuse: 38
% 198.00/198.43
% 198.00/198.43 Resimplifying inuse:
% 198.00/198.43 Done
% 198.00/198.43
% 198.00/198.43 Resimplifying inuse:
% 198.00/198.43 Done
% 198.00/198.43
% 198.00/198.43
% 198.00/198.43 Intermediate Status:
% 198.00/198.43 Generated: 209887
% 198.00/198.43 Kept: 95469
% 198.00/198.43 Inuse: 2259
% 198.00/198.43 Deleted: 591
% 198.00/198.43 Deletedinuse: 38
% 198.00/198.43
% 198.00/198.43 Resimplifying inuse:
% 198.00/198.43 Done
% 198.00/198.43
% 198.00/198.43 Resimplifying inuse:
% 198.00/198.43 Done
% 198.00/198.43
% 198.00/198.43
% 198.00/198.43 Intermediate Status:
% 198.00/198.43 Generated: 214536
% 198.00/198.43 Kept: 97482
% 198.00/198.43 Inuse: 2304
% 198.00/198.43 Deleted: 614
% 198.00/198.43 Deletedinuse: 61
% 198.00/198.43
% 198.00/198.43 Resimplifying inuse:
% 198.00/198.43 Done
% 198.00/198.43
% 198.00/198.43 Resimplifying inuse:
% 198.00/198.43 Done
% 198.00/198.43
% 198.00/198.43
% 198.00/198.43 Intermediate Status:
% 198.00/198.43 Generated: 220201
% 198.00/198.43 Kept: 99514
% 198.00/198.43 Inuse: 2348
% 198.00/198.43 Deleted: 614
% 198.00/198.43 Deletedinuse: 61
% 198.00/198.43
% 198.00/198.43 Resimplifying inuse:
% 198.00/198.43 Done
% 198.00/198.43
% 198.00/198.43 Resimplifying clauses:
% 198.00/198.43 Done
% 198.00/198.43
% 198.00/198.43 Resimplifying inuse:
% 198.00/198.43 Done
% 198.00/198.43
% 198.00/198.43
% 198.00/198.43 Intermediate Status:
% 198.00/198.43 Generated: 228098
% 198.00/198.43 Kept: 101575
% 198.00/198.43 Inuse: 2393
% 198.00/198.43 Deleted: 819
% 198.00/198.43 Deletedinuse: 82
% 198.00/198.43
% 198.00/198.43 Resimplifying inuse:
% 198.00/198.43 Done
% 198.00/198.43
% 198.00/198.43 Resimplifying inuse:
% 198.00/198.43 Done
% 198.00/198.43
% 198.00/198.43
% 198.00/198.43 Intermediate Status:
% 198.00/198.43 Generated: 233391
% 198.00/198.43 Kept: 103629
% 198.00/198.43 Inuse: 2441
% 198.00/198.43 Deleted: 833
% 198.00/198.43 Deletedinuse: 96
% 198.00/198.43
% 198.00/198.43 Resimplifying inuse:
% 198.00/198.43 Done
% 198.00/198.43
% 198.00/198.43 Resimplifying inuse:
% 198.00/198.43 Done
% 198.00/198.43
% 198.00/198.43
% 198.00/198.43 Intermediate Status:
% 198.00/198.43 Generated: 237858
% 198.00/198.43 Kept: 105673
% 198.00/198.43 Inuse: 2484
% 198.00/198.43 Deleted: 833
% 198.00/198.43 Deletedinuse: 96
% 198.00/198.43
% 198.00/198.43 Resimplifying inuse:
% 198.00/198.43 Done
% 198.00/198.43
% 198.00/198.43 Resimplifying inuse:
% 198.00/198.43 Done
% 198.00/198.43
% 198.00/198.43
% 198.00/198.43 Intermediate Status:
% 198.00/198.43 Generated: 242087
% 198.00/198.43 Kept: 107719
% 198.00/198.43 Inuse: 2526
% 198.00/198.43 Deleted: 833
% 198.00/198.43 Deletedinuse: 96
% 198.00/198.43
% 198.00/198.43 Resimplifying inuse:
% 198.00/198.43 Done
% 198.00/198.43
% 198.00/198.43 Resimplifying inuse:
% 198.00/198.43 Done
% 198.00/198.43
% 198.00/198.43
% 198.00/198.43 Intermediate Status:
% 198.00/198.43 Generated: 248448
% 198.00/198.43 Kept: 109789
% 198.00/198.43 Inuse: 2570
% 198.00/198.43 Deleted: 833
% 198.00/198.43 Deletedinuse: 96
% 198.00/198.43
% 198.00/198.43 Resimplifying inuse:
% 198.00/198.43 Done
% 198.00/198.43
% 198.00/198.43
% 198.00/198.43 Intermediate Status:
% 198.00/198.43 Generated: 265865
% 198.00/198.43 Kept: 111835
% 198.00/198.43 Inuse: 2606
% 198.00/198.43 Deleted: 833
% 198.00/198.43 Deletedinuse: 96
% 198.00/198.43
% 198.00/198.43 Resimplifying inuse:
% 198.00/198.43 Done
% 198.00/198.43
% 198.00/198.43 Resimplifying inuse:
% 198.00/198.43 Done
% 198.00/198.43
% 198.00/198.43
% 198.00/198.43 Intermediate Status:
% 198.00/198.43 Generated: 273287
% 198.00/198.43 Kept: 114052
% 198.00/198.43 Inuse: 2620
% 198.00/198.43 Deleted: 833
% 198.00/198.43 Deletedinuse: 96
% 198.00/198.43
% 198.00/198.43 Resimplifying inuse:
% 198.00/198.43 Done
% 198.00/198.43
% 198.00/198.43 Resimplifying inuse:
% 198.00/198.43 Done
% 198.00/198.43
% 198.00/198.43
% 198.00/198.43 Intermediate Status:
% 198.00/198.43 Generated: 280928
% 198.00/198.43 Kept: 116327
% 198.00/198.43 Inuse: 2635
% 198.00/198.43 Deleted: 833
% 198.00/198.43 Deletedinuse: 96
% 198.00/198.43
% 198.00/198.43 Resimplifying inuse:
% 198.00/198.43 Done
% 198.00/198.43
% 198.00/198.43 Resimplifying inuse:
% 198.00/198.43 Done
% 198.00/198.43
% 198.00/198.43
% 198.00/198.43 Intermediate Status:
% 198.00/198.43 Generated: 299249
% 198.00/198.43 Kept: 118341
% 198.00/198.43 Inuse: 2671
% 198.00/198.43 Deleted: 833
% 198.00/198.43 Deletedinuse: 96
% 198.00/198.43
% 198.00/198.43 Resimplifying inuse:
% 198.00/198.43 Done
% 198.00/198.43
% 198.00/198.43 Resimplifying inuse:
% 198.00/198.43 Done
% 198.00/198.43
% 198.00/198.43
% 198.00/198.43 Intermediate Status:
% 198.00/198.43 Generated: 314174
% 198.00/198.43 Kept: 120355
% 198.00/198.43 Inuse: 2707
% 198.00/198.43 Deleted: 833
% 198.00/198.43 Deletedinuse: 96
% 198.00/198.43
% 198.00/198.43 Resimplifying inuse:
% 198.00/198.43 Done
% 198.00/198.43
% 198.00/198.43 Resimplifying clauses:
% 198.00/198.43 Done
% 198.00/198.43
% 198.00/198.43 Resimplifying inuse:
% 198.00/198.43 Done
% 198.00/198.43
% 198.00/198.43
% 198.00/198.43 Intermediate Status:
% 198.00/198.43 Generated: 338950
% 198.00/198.43 Kept: 122356
% 198.00/198.43 Inuse: 2740
% 198.00/198.43 Deleted: 1043
% 198.00/198.43 Deletedinuse: 96
% 198.00/198.43
% 198.00/198.43 Resimplifying inuse:
% 198.00/198.43 Done
% 198.00/198.43
% 198.00/198.43 ResimplifyCputime limit exceeded (core dumped)
%------------------------------------------------------------------------------