%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : TOP014-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.04s 300.60s
% Output : None
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : TOP014-1 : TPTP v8.1.0. Released v1.0.0.
% 0.07/0.13 % Command : bliksem %s
% 0.13/0.34 % Computer : n022.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % DateTime : Sun May 29 08:21:08 EDT 2022
% 0.13/0.35 % CPUTime :
% 0.47/1.13 *** allocated 10000 integers for termspace/termends
% 0.47/1.13 *** allocated 10000 integers for clauses
% 0.47/1.13 *** allocated 10000 integers for justifications
% 0.47/1.13 Bliksem 1.12
% 0.47/1.13
% 0.47/1.13
% 0.47/1.13 Automatic Strategy Selection
% 0.47/1.13
% 0.47/1.13 Clauses:
% 0.47/1.13 [
% 0.47/1.13 [ ~( 'element_of_set'( X, 'union_of_members'( Y ) ) ), 'element_of_set'(
% 0.47/1.13 X, f1( Y, X ) ) ],
% 0.47/1.13 [ ~( 'element_of_set'( X, 'union_of_members'( Y ) ) ),
% 0.47/1.13 'element_of_collection'( f1( Y, X ), Y ) ],
% 0.47/1.13 [ 'element_of_set'( X, 'union_of_members'( Y ) ), ~( 'element_of_set'( X
% 0.47/1.13 , Z ) ), ~( 'element_of_collection'( Z, Y ) ) ],
% 0.47/1.13 [ ~( 'element_of_set'( X, 'intersection_of_members'( Y ) ) ), ~(
% 0.47/1.13 'element_of_collection'( Z, Y ) ), 'element_of_set'( X, Z ) ],
% 0.47/1.13 [ 'element_of_set'( X, 'intersection_of_members'( Y ) ),
% 0.47/1.13 'element_of_collection'( f2( Y, X ), Y ) ],
% 0.47/1.13 [ 'element_of_set'( X, 'intersection_of_members'( Y ) ), ~(
% 0.47/1.13 'element_of_set'( X, f2( Y, X ) ) ) ],
% 0.47/1.13 [ ~( 'topological_space'( X, Y ) ), 'equal_sets'( 'union_of_members'( Y
% 0.47/1.13 ), X ) ],
% 0.47/1.13 [ ~( 'topological_space'( X, Y ) ), 'element_of_collection'( 'empty_set'
% 0.47/1.13 , Y ) ],
% 0.47/1.13 [ ~( 'topological_space'( X, Y ) ), 'element_of_collection'( X, Y ) ]
% 0.47/1.13 ,
% 0.47/1.13 [ ~( 'topological_space'( X, Y ) ), ~( 'element_of_collection'( Z, Y ) )
% 0.47/1.13 , ~( 'element_of_collection'( T, Y ) ), 'element_of_collection'(
% 0.47/1.13 'intersection_of_sets'( Z, T ), Y ) ],
% 0.47/1.13 [ ~( 'topological_space'( X, Y ) ), ~( 'subset_collections'( Z, Y ) ),
% 0.47/1.13 'element_of_collection'( 'union_of_members'( Z ), Y ) ],
% 0.47/1.13 [ 'topological_space'( X, Y ), ~( 'equal_sets'( 'union_of_members'( Y )
% 0.47/1.13 , X ) ), ~( 'element_of_collection'( 'empty_set', Y ) ), ~(
% 0.47/1.13 'element_of_collection'( X, Y ) ), 'element_of_collection'( f3( X, Y ), Y
% 0.47/1.13 ), 'subset_collections'( f5( X, Y ), Y ) ],
% 0.47/1.13 [ 'topological_space'( X, Y ), ~( 'equal_sets'( 'union_of_members'( Y )
% 0.47/1.13 , X ) ), ~( 'element_of_collection'( 'empty_set', Y ) ), ~(
% 0.47/1.13 'element_of_collection'( X, Y ) ), 'element_of_collection'( f3( X, Y ), Y
% 0.47/1.13 ), ~( 'element_of_collection'( 'union_of_members'( f5( X, Y ) ), Y ) ) ]
% 0.47/1.13 ,
% 0.47/1.13 [ 'topological_space'( X, Y ), ~( 'equal_sets'( 'union_of_members'( Y )
% 0.47/1.13 , X ) ), ~( 'element_of_collection'( 'empty_set', Y ) ), ~(
% 0.47/1.13 'element_of_collection'( X, Y ) ), 'element_of_collection'( f4( X, Y ), Y
% 0.47/1.13 ), 'subset_collections'( f5( X, Y ), Y ) ],
% 0.47/1.13 [ 'topological_space'( X, Y ), ~( 'equal_sets'( 'union_of_members'( Y )
% 0.47/1.13 , X ) ), ~( 'element_of_collection'( 'empty_set', Y ) ), ~(
% 0.47/1.13 'element_of_collection'( X, Y ) ), 'element_of_collection'( f4( X, Y ), Y
% 0.47/1.13 ), ~( 'element_of_collection'( 'union_of_members'( f5( X, Y ) ), Y ) ) ]
% 0.47/1.13 ,
% 0.47/1.13 [ 'topological_space'( X, Y ), ~( 'equal_sets'( 'union_of_members'( Y )
% 0.47/1.13 , X ) ), ~( 'element_of_collection'( 'empty_set', Y ) ), ~(
% 0.47/1.13 'element_of_collection'( X, Y ) ), ~( 'element_of_collection'(
% 0.47/1.13 'intersection_of_sets'( f3( X, Y ), f4( X, Y ) ), Y ) ),
% 0.47/1.13 'subset_collections'( f5( X, Y ), Y ) ],
% 0.47/1.13 [ 'topological_space'( X, Y ), ~( 'equal_sets'( 'union_of_members'( Y )
% 0.47/1.13 , X ) ), ~( 'element_of_collection'( 'empty_set', Y ) ), ~(
% 0.47/1.13 'element_of_collection'( X, Y ) ), ~( 'element_of_collection'(
% 0.47/1.13 'intersection_of_sets'( f3( X, Y ), f4( X, Y ) ), Y ) ), ~(
% 0.47/1.13 'element_of_collection'( 'union_of_members'( f5( X, Y ) ), Y ) ) ],
% 0.47/1.13 [ ~( open( X, Y, Z ) ), 'topological_space'( Y, Z ) ],
% 0.47/1.13 [ ~( open( X, Y, Z ) ), 'element_of_collection'( X, Z ) ],
% 0.47/1.13 [ open( X, Y, Z ), ~( 'topological_space'( Y, Z ) ), ~(
% 0.47/1.13 'element_of_collection'( X, Z ) ) ],
% 0.47/1.13 [ ~( closed( X, Y, Z ) ), 'topological_space'( Y, Z ) ],
% 0.47/1.13 [ ~( closed( X, Y, Z ) ), open( 'relative_complement_sets'( X, Y ), Y, Z
% 0.47/1.13 ) ],
% 0.47/1.13 [ closed( X, Y, Z ), ~( 'topological_space'( Y, Z ) ), ~( open(
% 0.47/1.13 'relative_complement_sets'( X, Y ), Y, Z ) ) ],
% 0.47/1.13 [ ~( finer( X, Y, Z ) ), 'topological_space'( Z, X ) ],
% 0.47/1.13 [ ~( finer( X, Y, Z ) ), 'topological_space'( Z, Y ) ],
% 0.47/1.13 [ ~( finer( X, Y, Z ) ), 'subset_collections'( Y, X ) ],
% 0.47/1.13 [ finer( X, Y, Z ), ~( 'topological_space'( Z, X ) ), ~(
% 0.47/1.13 'topological_space'( Z, Y ) ), ~( 'subset_collections'( Y, X ) ) ],
% 0.47/1.13 [ ~( basis( X, Y ) ), 'equal_sets'( 'union_of_members'( Y ), X ) ],
% 0.47/1.13 [ ~( basis( X, Y ) ), ~( 'element_of_set'( Z, X ) ), ~(
% 0.47/1.13 'element_of_collection'( T, Y ) ), ~( 'element_of_collection'( U, Y ) ),
% 0.47/1.13 ~( 'element_of_set'( Z, 'intersection_of_sets'( T, U ) ) ),
% 0.47/1.13 'element_of_set'( Z, f6( X, Y, Z, T, U ) ) ],
% 0.47/1.13 [ ~( basis( X, Y ) ), ~( 'element_of_set'( Z, X ) ), ~(
% 0.47/1.13 'element_of_collection'( T, Y ) ), ~( 'element_of_collection'( U, Y ) ),
% 0.47/1.13 ~( 'element_of_set'( Z, 'intersection_of_sets'( T, U ) ) ),
% 0.47/1.13 'element_of_collection'( f6( X, Y, Z, T, U ), Y ) ],
% 0.47/1.13 [ ~( basis( X, Y ) ), ~( 'element_of_set'( Z, X ) ), ~(
% 0.47/1.13 'element_of_collection'( T, Y ) ), ~( 'element_of_collection'( U, Y ) ),
% 0.47/1.13 ~( 'element_of_set'( Z, 'intersection_of_sets'( T, U ) ) ), 'subset_sets'(
% 0.47/1.13 f6( X, Y, Z, T, U ), 'intersection_of_sets'( T, U ) ) ],
% 0.47/1.13 [ basis( X, Y ), ~( 'equal_sets'( 'union_of_members'( Y ), X ) ),
% 0.47/1.13 'element_of_set'( f7( X, Y ), X ) ],
% 0.47/1.13 [ basis( X, Y ), ~( 'equal_sets'( 'union_of_members'( Y ), X ) ),
% 0.47/1.13 'element_of_collection'( f8( X, Y ), Y ) ],
% 0.47/1.13 [ basis( X, Y ), ~( 'equal_sets'( 'union_of_members'( Y ), X ) ),
% 0.47/1.13 'element_of_collection'( f9( X, Y ), Y ) ],
% 0.47/1.13 [ basis( X, Y ), ~( 'equal_sets'( 'union_of_members'( Y ), X ) ),
% 0.47/1.13 'element_of_set'( f7( X, Y ), 'intersection_of_sets'( f8( X, Y ), f9( X,
% 0.47/1.13 Y ) ) ) ],
% 0.47/1.13 [ basis( X, Y ), ~( 'equal_sets'( 'union_of_members'( Y ), X ) ), ~(
% 0.47/1.13 'element_of_set'( f7( X, Y ), Z ) ), ~( 'element_of_collection'( Z, Y ) )
% 0.47/1.13 , ~( 'subset_sets'( Z, 'intersection_of_sets'( f8( X, Y ), f9( X, Y ) ) )
% 0.47/1.13 ) ],
% 0.47/1.13 [ ~( 'element_of_collection'( X, 'top_of_basis'( Y ) ) ), ~(
% 0.47/1.13 'element_of_set'( Z, X ) ), 'element_of_set'( Z, f10( Y, X, Z ) ) ],
% 0.47/1.13 [ ~( 'element_of_collection'( X, 'top_of_basis'( Y ) ) ), ~(
% 0.47/1.13 'element_of_set'( Z, X ) ), 'element_of_collection'( f10( Y, X, Z ), Y )
% 0.47/1.13 ],
% 0.47/1.13 [ ~( 'element_of_collection'( X, 'top_of_basis'( Y ) ) ), ~(
% 0.47/1.13 'element_of_set'( Z, X ) ), 'subset_sets'( f10( Y, X, Z ), X ) ],
% 0.47/1.13 [ 'element_of_collection'( X, 'top_of_basis'( Y ) ), 'element_of_set'(
% 0.47/1.13 f11( Y, X ), X ) ],
% 0.47/1.13 [ 'element_of_collection'( X, 'top_of_basis'( Y ) ), ~( 'element_of_set'(
% 0.47/1.13 f11( Y, X ), Z ) ), ~( 'element_of_collection'( Z, Y ) ), ~(
% 0.47/1.13 'subset_sets'( Z, X ) ) ],
% 0.47/1.13 [ ~( 'element_of_collection'( X, 'subspace_topology'( Y, Z, T ) ) ),
% 0.47/1.13 'topological_space'( Y, Z ) ],
% 0.47/1.13 [ ~( 'element_of_collection'( X, 'subspace_topology'( Y, Z, T ) ) ),
% 0.47/1.13 'subset_sets'( T, Y ) ],
% 0.47/1.13 [ ~( 'element_of_collection'( X, 'subspace_topology'( Y, Z, T ) ) ),
% 0.47/1.13 'element_of_collection'( f12( Y, Z, T, X ), Z ) ],
% 0.47/1.13 [ ~( 'element_of_collection'( X, 'subspace_topology'( Y, Z, T ) ) ),
% 0.47/1.13 'equal_sets'( X, 'intersection_of_sets'( T, f12( Y, Z, T, X ) ) ) ],
% 0.47/1.13 [ 'element_of_collection'( X, 'subspace_topology'( Y, Z, T ) ), ~(
% 0.47/1.13 'topological_space'( Y, Z ) ), ~( 'subset_sets'( T, Y ) ), ~(
% 0.47/1.13 'element_of_collection'( U, Z ) ), ~( 'equal_sets'( X,
% 0.47/1.13 'intersection_of_sets'( T, U ) ) ) ],
% 0.47/1.13 [ ~( 'element_of_set'( X, interior( Y, Z, T ) ) ), 'topological_space'(
% 0.47/1.13 Z, T ) ],
% 0.47/1.13 [ ~( 'element_of_set'( X, interior( Y, Z, T ) ) ), 'subset_sets'( Y, Z )
% 0.47/1.13 ],
% 0.47/1.13 [ ~( 'element_of_set'( X, interior( Y, Z, T ) ) ), 'element_of_set'( X,
% 0.47/1.13 f13( Y, Z, T, X ) ) ],
% 0.47/1.13 [ ~( 'element_of_set'( X, interior( Y, Z, T ) ) ), 'subset_sets'( f13( Y
% 0.47/1.13 , Z, T, X ), Y ) ],
% 0.47/1.13 [ ~( 'element_of_set'( X, interior( Y, Z, T ) ) ), open( f13( Y, Z, T, X
% 0.47/1.13 ), Z, T ) ],
% 0.47/1.13 [ 'element_of_set'( X, interior( Y, Z, T ) ), ~( 'topological_space'( Z
% 0.47/1.13 , T ) ), ~( 'subset_sets'( Y, Z ) ), ~( 'element_of_set'( X, U ) ), ~(
% 0.47/1.13 'subset_sets'( U, Y ) ), ~( open( U, Z, T ) ) ],
% 0.47/1.13 [ ~( 'element_of_set'( X, closure( Y, Z, T ) ) ), 'topological_space'( Z
% 0.47/1.13 , T ) ],
% 0.47/1.13 [ ~( 'element_of_set'( X, closure( Y, Z, T ) ) ), 'subset_sets'( Y, Z )
% 0.47/1.13 ],
% 0.47/1.13 [ ~( 'element_of_set'( X, closure( Y, Z, T ) ) ), ~( 'subset_sets'( Y, U
% 0.47/1.13 ) ), ~( closed( U, Z, T ) ), 'element_of_set'( X, U ) ],
% 0.47/1.13 [ 'element_of_set'( X, closure( Y, Z, T ) ), ~( 'topological_space'( Z,
% 0.47/1.13 T ) ), ~( 'subset_sets'( Y, Z ) ), 'subset_sets'( Y, f14( Y, Z, T, X ) )
% 0.47/1.13 ],
% 0.47/1.13 [ 'element_of_set'( X, closure( Y, Z, T ) ), ~( 'topological_space'( Z,
% 0.47/1.13 T ) ), ~( 'subset_sets'( Y, Z ) ), closed( f14( Y, Z, T, X ), Z, T ) ]
% 0.47/1.13 ,
% 0.47/1.13 [ 'element_of_set'( X, closure( Y, Z, T ) ), ~( 'topological_space'( Z,
% 0.47/1.13 T ) ), ~( 'subset_sets'( Y, Z ) ), ~( 'element_of_set'( X, f14( Y, Z, T,
% 0.47/1.13 X ) ) ) ],
% 0.47/1.13 [ ~( neighborhood( X, Y, Z, T ) ), 'topological_space'( Z, T ) ],
% 0.47/1.13 [ ~( neighborhood( X, Y, Z, T ) ), open( X, Z, T ) ],
% 0.47/1.13 [ ~( neighborhood( X, Y, Z, T ) ), 'element_of_set'( Y, X ) ],
% 0.47/1.13 [ neighborhood( X, Y, Z, T ), ~( 'topological_space'( Z, T ) ), ~( open(
% 0.47/1.13 X, Z, T ) ), ~( 'element_of_set'( Y, X ) ) ],
% 0.47/1.13 [ ~( 'limit_point'( X, Y, Z, T ) ), 'topological_space'( Z, T ) ],
% 0.47/1.13 [ ~( 'limit_point'( X, Y, Z, T ) ), 'subset_sets'( Y, Z ) ],
% 0.47/1.13 [ ~( 'limit_point'( X, Y, Z, T ) ), ~( neighborhood( U, X, Z, T ) ),
% 0.47/1.13 'element_of_set'( f15( X, Y, Z, T, U ), 'intersection_of_sets'( U, Y ) )
% 0.47/1.13 ],
% 0.47/1.13 [ ~( 'limit_point'( X, Y, Z, T ) ), ~( neighborhood( U, X, Z, T ) ), ~(
% 0.47/1.13 'eq_p'( f15( X, Y, Z, T, U ), X ) ) ],
% 0.47/1.13 [ 'limit_point'( X, Y, Z, T ), ~( 'topological_space'( Z, T ) ), ~(
% 0.47/1.13 'subset_sets'( Y, Z ) ), neighborhood( f16( X, Y, Z, T ), X, Z, T ) ]
% 0.47/1.13 ,
% 0.47/1.13 [ 'limit_point'( X, Y, Z, T ), ~( 'topological_space'( Z, T ) ), ~(
% 0.47/1.13 'subset_sets'( Y, Z ) ), ~( 'element_of_set'( U, 'intersection_of_sets'(
% 0.47/1.13 f16( X, Y, Z, T ), Y ) ) ), 'eq_p'( U, X ) ],
% 0.47/1.13 [ ~( 'element_of_set'( X, boundary( Y, Z, T ) ) ), 'topological_space'(
% 0.47/1.13 Z, T ) ],
% 0.47/1.13 [ ~( 'element_of_set'( X, boundary( Y, Z, T ) ) ), 'element_of_set'( X,
% 0.47/1.13 closure( Y, Z, T ) ) ],
% 0.47/1.13 [ ~( 'element_of_set'( X, boundary( Y, Z, T ) ) ), 'element_of_set'( X,
% 0.47/1.13 closure( 'relative_complement_sets'( Y, Z ), Z, T ) ) ],
% 0.47/1.13 [ 'element_of_set'( X, boundary( Y, Z, T ) ), ~( 'topological_space'( Z
% 0.47/1.13 , T ) ), ~( 'element_of_set'( X, closure( Y, Z, T ) ) ), ~(
% 0.47/1.13 'element_of_set'( X, closure( 'relative_complement_sets'( Y, Z ), Z, T )
% 0.47/1.13 ) ) ],
% 0.47/1.13 [ ~( hausdorff( X, Y ) ), 'topological_space'( X, Y ) ],
% 0.47/1.13 [ ~( hausdorff( X, Y ) ), ~( 'element_of_set'( Z, X ) ), ~(
% 0.47/1.13 'element_of_set'( T, X ) ), 'eq_p'( Z, T ), neighborhood( f17( X, Y, Z, T
% 0.47/1.13 ), Z, X, Y ) ],
% 0.47/1.13 [ ~( hausdorff( X, Y ) ), ~( 'element_of_set'( Z, X ) ), ~(
% 0.47/1.13 'element_of_set'( T, X ) ), 'eq_p'( Z, T ), neighborhood( f18( X, Y, Z, T
% 0.47/1.13 ), T, X, Y ) ],
% 0.47/1.13 [ ~( hausdorff( X, Y ) ), ~( 'element_of_set'( Z, X ) ), ~(
% 0.47/1.13 'element_of_set'( T, X ) ), 'eq_p'( Z, T ), 'disjoint_s'( f17( X, Y, Z, T
% 0.47/1.13 ), f18( X, Y, Z, T ) ) ],
% 0.47/1.13 [ hausdorff( X, Y ), ~( 'topological_space'( X, Y ) ), 'element_of_set'(
% 0.47/1.13 f19( X, Y ), X ) ],
% 0.47/1.13 [ hausdorff( X, Y ), ~( 'topological_space'( X, Y ) ), 'element_of_set'(
% 0.47/1.13 f20( X, Y ), X ) ],
% 0.47/1.13 [ hausdorff( X, Y ), ~( 'topological_space'( X, Y ) ), ~( 'eq_p'( f19( X
% 0.47/1.13 , Y ), f20( X, Y ) ) ) ],
% 0.47/1.13 [ hausdorff( X, Y ), ~( 'topological_space'( X, Y ) ), ~( neighborhood(
% 0.47/1.13 Z, f19( X, Y ), X, Y ) ), ~( neighborhood( T, f20( X, Y ), X, Y ) ), ~(
% 0.47/1.13 'disjoint_s'( Z, T ) ) ],
% 0.47/1.13 [ ~( separation( X, Y, Z, T ) ), 'topological_space'( Z, T ) ],
% 0.47/1.13 [ ~( separation( X, Y, Z, T ) ), ~( 'equal_sets'( X, 'empty_set' ) ) ]
% 0.47/1.13 ,
% 0.47/1.13 [ ~( separation( X, Y, Z, T ) ), ~( 'equal_sets'( Y, 'empty_set' ) ) ]
% 0.47/1.13 ,
% 0.47/1.13 [ ~( separation( X, Y, Z, T ) ), 'element_of_collection'( X, T ) ],
% 0.47/1.13 [ ~( separation( X, Y, Z, T ) ), 'element_of_collection'( Y, T ) ],
% 0.47/1.13 [ ~( separation( X, Y, Z, T ) ), 'equal_sets'( 'union_of_sets'( X, Y ),
% 0.47/1.13 Z ) ],
% 0.47/1.13 [ ~( separation( X, Y, Z, T ) ), 'disjoint_s'( X, Y ) ],
% 0.47/1.13 [ separation( X, Y, Z, T ), ~( 'topological_space'( Z, T ) ),
% 0.47/1.13 'equal_sets'( X, 'empty_set' ), 'equal_sets'( Y, 'empty_set' ), ~(
% 0.47/1.13 'element_of_collection'( X, T ) ), ~( 'element_of_collection'( Y, T ) ),
% 0.47/1.13 ~( 'equal_sets'( 'union_of_sets'( X, Y ), Z ) ), ~( 'disjoint_s'( X, Y )
% 0.47/1.13 ) ],
% 0.47/1.13 [ ~( 'connected_space'( X, Y ) ), 'topological_space'( X, Y ) ],
% 0.47/1.13 [ ~( 'connected_space'( X, Y ) ), ~( separation( Z, T, X, Y ) ) ],
% 0.47/1.13 [ 'connected_space'( X, Y ), ~( 'topological_space'( X, Y ) ),
% 0.47/1.13 separation( f21( X, Y ), f22( X, Y ), X, Y ) ],
% 0.47/1.13 [ ~( 'connected_set'( X, Y, Z ) ), 'topological_space'( Y, Z ) ],
% 0.47/1.13 [ ~( 'connected_set'( X, Y, Z ) ), 'subset_sets'( X, Y ) ],
% 0.47/1.13 [ ~( 'connected_set'( X, Y, Z ) ), 'connected_space'( X,
% 2.96/3.33 'subspace_topology'( Y, Z, X ) ) ],
% 2.96/3.33 [ 'connected_set'( X, Y, Z ), ~( 'topological_space'( Y, Z ) ), ~(
% 2.96/3.33 'subset_sets'( X, Y ) ), ~( 'connected_space'( X, 'subspace_topology'( Y
% 2.96/3.33 , Z, X ) ) ) ],
% 2.96/3.33 [ ~( 'open_covering'( X, Y, Z ) ), 'topological_space'( Y, Z ) ],
% 2.96/3.33 [ ~( 'open_covering'( X, Y, Z ) ), 'subset_collections'( X, Z ) ],
% 2.96/3.33 [ ~( 'open_covering'( X, Y, Z ) ), 'equal_sets'( 'union_of_members'( X )
% 2.96/3.33 , Y ) ],
% 2.96/3.33 [ 'open_covering'( X, Y, Z ), ~( 'topological_space'( Y, Z ) ), ~(
% 2.96/3.33 'subset_collections'( X, Z ) ), ~( 'equal_sets'( 'union_of_members'( X )
% 2.96/3.33 , Y ) ) ],
% 2.96/3.33 [ ~( 'compact_space'( X, Y ) ), 'topological_space'( X, Y ) ],
% 2.96/3.33 [ ~( 'compact_space'( X, Y ) ), ~( 'open_covering'( Z, X, Y ) ), finite(
% 2.96/3.33 f23( X, Y, Z ) ) ],
% 2.96/3.33 [ ~( 'compact_space'( X, Y ) ), ~( 'open_covering'( Z, X, Y ) ),
% 2.96/3.33 'subset_collections'( f23( X, Y, Z ), Z ) ],
% 2.96/3.33 [ ~( 'compact_space'( X, Y ) ), ~( 'open_covering'( Z, X, Y ) ),
% 2.96/3.33 'open_covering'( f23( X, Y, Z ), X, Y ) ],
% 2.96/3.33 [ 'compact_space'( X, Y ), ~( 'topological_space'( X, Y ) ),
% 2.96/3.33 'open_covering'( f24( X, Y ), X, Y ) ],
% 2.96/3.33 [ 'compact_space'( X, Y ), ~( 'topological_space'( X, Y ) ), ~( finite(
% 2.96/3.33 Z ) ), ~( 'subset_collections'( Z, f24( X, Y ) ) ), ~( 'open_covering'( Z
% 2.96/3.33 , X, Y ) ) ],
% 2.96/3.33 [ ~( 'compact_set'( X, Y, Z ) ), 'topological_space'( Y, Z ) ],
% 2.96/3.33 [ ~( 'compact_set'( X, Y, Z ) ), 'subset_sets'( X, Y ) ],
% 2.96/3.33 [ ~( 'compact_set'( X, Y, Z ) ), 'compact_space'( X, 'subspace_topology'(
% 2.96/3.33 Y, Z, X ) ) ],
% 2.96/3.33 [ 'compact_set'( X, Y, Z ), ~( 'topological_space'( Y, Z ) ), ~(
% 2.96/3.33 'subset_sets'( X, Y ) ), ~( 'compact_space'( X, 'subspace_topology'( Y, Z
% 2.96/3.33 , X ) ) ) ],
% 2.96/3.33 [ 'topological_space'( cx, ct ) ],
% 2.96/3.33 [ 'subset_sets'( a, cx ) ],
% 2.96/3.33 [ open( a, cx, ct ), 'equal_sets'( a, interior( a, cx, ct ) ), closed( a
% 2.96/3.33 , cx, ct ), 'equal_sets'( a, closure( a, cx, ct ) ) ],
% 2.96/3.33 [ open( a, cx, ct ), 'equal_sets'( a, interior( a, cx, ct ) ), ~( closed(
% 2.96/3.33 a, cx, ct ) ), ~( 'equal_sets'( a, closure( a, cx, ct ) ) ) ],
% 2.96/3.33 [ ~( open( a, cx, ct ) ), ~( 'equal_sets'( a, interior( a, cx, ct ) ) )
% 2.96/3.33 , closed( a, cx, ct ), 'equal_sets'( a, closure( a, cx, ct ) ) ],
% 2.96/3.33 [ ~( open( a, cx, ct ) ), ~( 'equal_sets'( a, interior( a, cx, ct ) ) )
% 2.96/3.33 , ~( closed( a, cx, ct ) ), ~( 'equal_sets'( a, closure( a, cx, ct ) ) )
% 2.96/3.33 ]
% 2.96/3.33 ] .
% 2.96/3.33
% 2.96/3.33
% 2.96/3.33 percentage equality = 0.000000, percentage horn = 0.773913
% 2.96/3.33 This a non-horn, non-equality problem
% 2.96/3.33
% 2.96/3.33
% 2.96/3.33 Options Used:
% 2.96/3.33
% 2.96/3.33 useres = 1
% 2.96/3.33 useparamod = 0
% 2.96/3.33 useeqrefl = 0
% 2.96/3.33 useeqfact = 0
% 2.96/3.33 usefactor = 1
% 2.96/3.33 usesimpsplitting = 0
% 2.96/3.33 usesimpdemod = 0
% 2.96/3.33 usesimpres = 3
% 2.96/3.33
% 2.96/3.33 resimpinuse = 1000
% 2.96/3.33 resimpclauses = 20000
% 2.96/3.33 substype = standard
% 2.96/3.33 backwardsubs = 1
% 2.96/3.33 selectoldest = 5
% 2.96/3.33
% 2.96/3.33 litorderings [0] = split
% 2.96/3.33 litorderings [1] = liftord
% 2.96/3.33
% 2.96/3.33 termordering = none
% 2.96/3.33
% 2.96/3.33 litapriori = 1
% 2.96/3.33 termapriori = 0
% 2.96/3.33 litaposteriori = 0
% 2.96/3.33 termaposteriori = 0
% 2.96/3.33 demodaposteriori = 0
% 2.96/3.33 ordereqreflfact = 0
% 2.96/3.33
% 2.96/3.33 litselect = none
% 2.96/3.33
% 2.96/3.33 maxweight = 15
% 2.96/3.33 maxdepth = 30000
% 2.96/3.33 maxlength = 115
% 2.96/3.33 maxnrvars = 195
% 2.96/3.33 excuselevel = 1
% 2.96/3.33 increasemaxweight = 1
% 2.96/3.33
% 2.96/3.33 maxselected = 10000000
% 2.96/3.33 maxnrclauses = 10000000
% 2.96/3.33
% 2.96/3.33 showgenerated = 0
% 2.96/3.33 showkept = 0
% 2.96/3.33 showselected = 0
% 2.96/3.33 showdeleted = 0
% 2.96/3.33 showresimp = 1
% 2.96/3.33 showstatus = 2000
% 2.96/3.33
% 2.96/3.33 prologoutput = 1
% 2.96/3.33 nrgoals = 5000000
% 2.96/3.33 totalproof = 1
% 2.96/3.33
% 2.96/3.33 Symbols occurring in the translation:
% 2.96/3.33
% 2.96/3.33 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 2.96/3.33 . [1, 2] (w:1, o:47, a:1, s:1, b:0),
% 2.96/3.33 ! [4, 1] (w:0, o:38, a:1, s:1, b:0),
% 2.96/3.33 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 2.96/3.33 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 2.96/3.33 'union_of_members' [41, 1] (w:1, o:44, a:1, s:1, b:0),
% 2.96/3.33 'element_of_set' [42, 2] (w:1, o:75, a:1, s:1, b:0),
% 2.96/3.33 f1 [43, 2] (w:1, o:79, a:1, s:1, b:0),
% 2.96/3.33 'element_of_collection' [44, 2] (w:1, o:76, a:1, s:1, b:0),
% 2.96/3.33 'intersection_of_members' [46, 1] (w:1, o:45, a:1, s:1, b:0),
% 2.96/3.33 f2 [48, 2] (w:1, o:82, a:1, s:1, b:0),
% 2.96/3.33 'topological_space' [51, 2] (w:1, o:86, a:1, s:1, b:0),
% 2.96/3.33 'equal_sets' [52, 2] (w:1, o:77, a:1, s:1, b:0),
% 2.96/3.33 'empty_set' [Cputime limit exceeded (core dumped)
%------------------------------------------------------------------------------