1		generated(1767432892709,'Sat Jan 03 10:34:52 CET 2026').
2		project_name('Test').
3		machine_name('TestSequentProverRules').
4		disprover_po('thm1-DERIV_TYPE_SETMINUS_BINTER/THM',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,a),integer_set(none)),member(none,identifier(none,b),bool_set(none)),member(none,identifier(none,c),identifier(none,'D')),member(none,identifier(none,d),identifier(none,'D')),member(none,identifier(none,e1),identifier(none,'E')),member(none,identifier(none,e2),identifier(none,'E')),member(none,identifier(none,a),integer_set(none)),member(none,identifier(none,b),bool_set(none)),member(none,identifier(none,c),identifier(none,'D')),member(none,identifier(none,d),identifier(none,'D')),partition(none,identifier(none,'E'),[set_extension(none,[identifier(none,e1)]),set_extension(none,[identifier(none,e2)])])]),constants(none,[identifier(none,a),identifier(none,b),identifier(none,c),identifier(none,d),identifier(none,e1),identifier(none,e2)]),sets(none,[deferred_set(none,'D'),deferred_set(none,'E')])]),equal(none,set_subtraction(none,identifier(none,'D'),intersection(none,set_extension(none,[identifier(none,c)]),set_extension(none,[identifier(none,d)]))),union(none,set_subtraction(none,identifier(none,'D'),set_extension(none,[identifier(none,c)])),set_subtraction(none,identifier(none,'D'),set_extension(none,[identifier(none,d)])))),[member(none,identifier(none,a),integer_set(none)),member(none,identifier(none,b),bool_set(none)),member(none,identifier(none,c),identifier(none,'D')),member(none,identifier(none,d),identifier(none,'D')),partition(none,identifier(none,'E'),[set_extension(none,[identifier(none,e1)]),set_extension(none,[identifier(none,e2)])])],[member(none,identifier(none,a),integer_set(none)),member(none,identifier(none,b),bool_set(none)),member(none,identifier(none,c),identifier(none,'D')),member(none,identifier(none,d),identifier(none,'D')),partition(none,identifier(none,'E'),[set_extension(none,[identifier(none,e1)]),set_extension(none,[identifier(none,e2)])])],true).
5		disprover_po('thm2-DERIV_TYPE_SETMINUS_BUNION/THM',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,a),integer_set(none)),member(none,identifier(none,b),bool_set(none)),member(none,identifier(none,c),identifier(none,'D')),member(none,identifier(none,d),identifier(none,'D')),member(none,identifier(none,e1),identifier(none,'E')),member(none,identifier(none,e2),identifier(none,'E')),member(none,identifier(none,a),integer_set(none)),member(none,identifier(none,b),bool_set(none)),member(none,identifier(none,c),identifier(none,'D')),member(none,identifier(none,d),identifier(none,'D')),partition(none,identifier(none,'E'),[set_extension(none,[identifier(none,e1)]),set_extension(none,[identifier(none,e2)])]),equal(none,set_subtraction(none,identifier(none,'D'),intersection(none,set_extension(none,[identifier(none,c)]),set_extension(none,[identifier(none,d)]))),union(none,set_subtraction(none,identifier(none,'D'),set_extension(none,[identifier(none,c)])),set_subtraction(none,identifier(none,'D'),set_extension(none,[identifier(none,d)]))))]),constants(none,[identifier(none,a),identifier(none,b),identifier(none,c),identifier(none,d),identifier(none,e1),identifier(none,e2)]),sets(none,[deferred_set(none,'D'),deferred_set(none,'E')])]),equal(none,set_subtraction(none,identifier(none,'D'),union(none,set_extension(none,[identifier(none,c)]),set_extension(none,[identifier(none,d)]))),intersection(none,set_subtraction(none,identifier(none,'D'),set_extension(none,[identifier(none,c)])),set_subtraction(none,identifier(none,'D'),set_extension(none,[identifier(none,d)])))),[member(none,identifier(none,a),integer_set(none)),member(none,identifier(none,b),bool_set(none)),member(none,identifier(none,c),identifier(none,'D')),member(none,identifier(none,d),identifier(none,'D')),partition(none,identifier(none,'E'),[set_extension(none,[identifier(none,e1)]),set_extension(none,[identifier(none,e2)])]),equal(none,set_subtraction(none,identifier(none,'D'),intersection(none,set_extension(none,[identifier(none,c)]),set_extension(none,[identifier(none,d)]))),union(none,set_subtraction(none,identifier(none,'D'),set_extension(none,[identifier(none,c)])),set_subtraction(none,identifier(none,'D'),set_extension(none,[identifier(none,d)]))))],[member(none,identifier(none,a),integer_set(none)),member(none,identifier(none,b),bool_set(none)),member(none,identifier(none,c),identifier(none,'D')),member(none,identifier(none,d),identifier(none,'D')),partition(none,identifier(none,'E'),[set_extension(none,[identifier(none,e1)]),set_extension(none,[identifier(none,e2)])]),equal(none,set_subtraction(none,identifier(none,'D'),intersection(none,set_extension(none,[identifier(none,c)]),set_extension(none,[identifier(none,d)]))),union(none,set_subtraction(none,identifier(none,'D'),set_extension(none,[identifier(none,c)])),set_subtraction(none,identifier(none,'D'),set_extension(none,[identifier(none,d)]))))],true).
6		disprover_po('thm3-DERIV_TYPE_SETMINUS_BINTER/THM',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,a),integer_set(none)),member(none,identifier(none,b),bool_set(none)),member(none,identifier(none,c),identifier(none,'D')),member(none,identifier(none,d),identifier(none,'D')),member(none,identifier(none,e1),identifier(none,'E')),member(none,identifier(none,e2),identifier(none,'E')),member(none,identifier(none,a),integer_set(none)),member(none,identifier(none,b),bool_set(none)),member(none,identifier(none,c),identifier(none,'D')),member(none,identifier(none,d),identifier(none,'D')),partition(none,identifier(none,'E'),[set_extension(none,[identifier(none,e1)]),set_extension(none,[identifier(none,e2)])]),equal(none,set_subtraction(none,identifier(none,'D'),intersection(none,set_extension(none,[identifier(none,c)]),set_extension(none,[identifier(none,d)]))),union(none,set_subtraction(none,identifier(none,'D'),set_extension(none,[identifier(none,c)])),set_subtraction(none,identifier(none,'D'),set_extension(none,[identifier(none,d)])))),equal(none,set_subtraction(none,identifier(none,'D'),union(none,set_extension(none,[identifier(none,c)]),set_extension(none,[identifier(none,d)]))),intersection(none,set_subtraction(none,identifier(none,'D'),set_extension(none,[identifier(none,c)])),set_subtraction(none,identifier(none,'D'),set_extension(none,[identifier(none,d)]))))]),constants(none,[identifier(none,a),identifier(none,b),identifier(none,c),identifier(none,d),identifier(none,e1),identifier(none,e2)]),sets(none,[deferred_set(none,'D'),deferred_set(none,'E')])]),equal(none,set_subtraction(none,identifier(none,'E'),union(none,set_extension(none,[identifier(none,e1)]),set_extension(none,[identifier(none,e2)]))),intersection(none,set_subtraction(none,identifier(none,'E'),set_extension(none,[identifier(none,e1)])),set_subtraction(none,identifier(none,'E'),set_extension(none,[identifier(none,e2)])))),[member(none,identifier(none,a),integer_set(none)),member(none,identifier(none,b),bool_set(none)),member(none,identifier(none,c),identifier(none,'D')),member(none,identifier(none,d),identifier(none,'D')),partition(none,identifier(none,'E'),[set_extension(none,[identifier(none,e1)]),set_extension(none,[identifier(none,e2)])]),equal(none,set_subtraction(none,identifier(none,'D'),intersection(none,set_extension(none,[identifier(none,c)]),set_extension(none,[identifier(none,d)]))),union(none,set_subtraction(none,identifier(none,'D'),set_extension(none,[identifier(none,c)])),set_subtraction(none,identifier(none,'D'),set_extension(none,[identifier(none,d)])))),equal(none,set_subtraction(none,identifier(none,'D'),union(none,set_extension(none,[identifier(none,c)]),set_extension(none,[identifier(none,d)]))),intersection(none,set_subtraction(none,identifier(none,'D'),set_extension(none,[identifier(none,c)])),set_subtraction(none,identifier(none,'D'),set_extension(none,[identifier(none,d)]))))],[member(none,identifier(none,a),integer_set(none)),member(none,identifier(none,b),bool_set(none)),member(none,identifier(none,c),identifier(none,'D')),member(none,identifier(none,d),identifier(none,'D')),partition(none,identifier(none,'E'),[set_extension(none,[identifier(none,e1)]),set_extension(none,[identifier(none,e2)])]),equal(none,set_subtraction(none,identifier(none,'D'),intersection(none,set_extension(none,[identifier(none,c)]),set_extension(none,[identifier(none,d)]))),union(none,set_subtraction(none,identifier(none,'D'),set_extension(none,[identifier(none,c)])),set_subtraction(none,identifier(none,'D'),set_extension(none,[identifier(none,d)])))),equal(none,set_subtraction(none,identifier(none,'D'),union(none,set_extension(none,[identifier(none,c)]),set_extension(none,[identifier(none,d)]))),intersection(none,set_subtraction(none,identifier(none,'D'),set_extension(none,[identifier(none,c)])),set_subtraction(none,identifier(none,'D'),set_extension(none,[identifier(none,d)]))))],true).
7