1		generated(1585669537658,'Tue Mar 31 17:45:37 CEST 2020').
2		project_name('Test').
3		machine_name('TestWD_Prover').
4		disprover_po('axm4/WD',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,a),integer_set(none)),member(none,identifier(none,b),integer_set(none)),member(none,identifier(none,c),integer_set(none)),member(none,identifier(none,s),pow_subset(none,integer_set(none))),member(none,identifier(none,f),pow_subset(none,cartesian_product(none,integer_set(none),integer_set(none)))),member(none,identifier(none,g),pow_subset(none,cartesian_product(none,integer_set(none),integer_set(none)))),member(none,identifier(none,f),total_function(none,natural1_set(none),natural1_set(none))),member(none,identifier(none,a),natural1_set(none)),member(none,identifier(none,b),natural_set(none))]),constants(none,[identifier(none,a),identifier(none,b),identifier(none,c),identifier(none,s),identifier(none,f),identifier(none,g)]),sets(none,[])]),conjunct(none,member(none,identifier(none,a),domain(none,identifier(none,f))),member(none,identifier(none,f),partial_function(none,integer_set(none),integer_set(none)))),[member(none,identifier(none,f),total_function(none,natural1_set(none),natural1_set(none))),member(none,identifier(none,a),natural1_set(none)),member(none,identifier(none,b),natural_set(none))],[member(none,identifier(none,f),total_function(none,natural1_set(none),natural1_set(none))),member(none,identifier(none,a),natural1_set(none)),member(none,identifier(none,b),natural_set(none))],true).
5		disprover_po('axm5/WD',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,a),integer_set(none)),member(none,identifier(none,b),integer_set(none)),member(none,identifier(none,c),integer_set(none)),member(none,identifier(none,s),pow_subset(none,integer_set(none))),member(none,identifier(none,f),pow_subset(none,cartesian_product(none,integer_set(none),integer_set(none)))),member(none,identifier(none,g),pow_subset(none,cartesian_product(none,integer_set(none),integer_set(none)))),member(none,identifier(none,f),total_function(none,natural1_set(none),natural1_set(none))),member(none,identifier(none,a),natural1_set(none)),member(none,identifier(none,b),natural_set(none)),equal(none,function(none,identifier(none,f),[identifier(none,a)]),identifier(none,c)),member(none,identifier(none,a),domain(none,identifier(none,f))),member(none,identifier(none,f),partial_function(none,integer_set(none),integer_set(none)))]),constants(none,[identifier(none,a),identifier(none,b),identifier(none,c),identifier(none,s),identifier(none,f),identifier(none,g)]),sets(none,[])]),conjunct(none,member(none,add(none,identifier(none,b),integer(none,1)),domain(none,identifier(none,f))),member(none,identifier(none,f),partial_function(none,integer_set(none),integer_set(none)))),[member(none,identifier(none,f),total_function(none,natural1_set(none),natural1_set(none))),member(none,identifier(none,a),natural1_set(none)),member(none,identifier(none,b),natural_set(none)),equal(none,function(none,identifier(none,f),[identifier(none,a)]),identifier(none,c)),member(none,identifier(none,a),domain(none,identifier(none,f))),member(none,identifier(none,f),partial_function(none,integer_set(none),integer_set(none)))],[member(none,identifier(none,f),total_function(none,natural1_set(none),natural1_set(none))),member(none,identifier(none,a),natural1_set(none)),member(none,identifier(none,b),natural_set(none)),equal(none,function(none,identifier(none,f),[identifier(none,a)]),identifier(none,c))],unknown).
6		disprover_po('axm6/WD',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,a),integer_set(none)),member(none,identifier(none,b),integer_set(none)),member(none,identifier(none,c),integer_set(none)),member(none,identifier(none,s),pow_subset(none,integer_set(none))),member(none,identifier(none,f),pow_subset(none,cartesian_product(none,integer_set(none),integer_set(none)))),member(none,identifier(none,g),pow_subset(none,cartesian_product(none,integer_set(none),integer_set(none)))),member(none,identifier(none,f),total_function(none,natural1_set(none),natural1_set(none))),member(none,identifier(none,a),natural1_set(none)),member(none,identifier(none,b),natural_set(none)),equal(none,function(none,identifier(none,f),[identifier(none,a)]),identifier(none,c)),member(none,identifier(none,a),domain(none,identifier(none,f))),member(none,identifier(none,f),partial_function(none,integer_set(none),integer_set(none))),equal(none,function(none,identifier(none,f),[add(none,identifier(none,b),integer(none,1))]),identifier(none,c)),member(none,add(none,identifier(none,b),integer(none,1)),domain(none,identifier(none,f)))]),constants(none,[identifier(none,a),identifier(none,b),identifier(none,c),identifier(none,s),identifier(none,f),identifier(none,g)]),sets(none,[])]),conjunct(none,member(none,identifier(none,a),domain(none,identifier(none,f))),conjunct(none,member(none,identifier(none,f),partial_function(none,integer_set(none),integer_set(none))),conjunct(none,not_equal(none,function(none,identifier(none,f),[identifier(none,a)]),integer(none,0)),not_equal(none,identifier(none,a),integer(none,0))))),[member(none,identifier(none,f),total_function(none,natural1_set(none),natural1_set(none))),member(none,identifier(none,a),natural1_set(none)),member(none,identifier(none,b),natural_set(none)),equal(none,function(none,identifier(none,f),[identifier(none,a)]),identifier(none,c)),member(none,identifier(none,a),domain(none,identifier(none,f))),member(none,identifier(none,f),partial_function(none,integer_set(none),integer_set(none))),equal(none,function(none,identifier(none,f),[add(none,identifier(none,b),integer(none,1))]),identifier(none,c)),member(none,add(none,identifier(none,b),integer(none,1)),domain(none,identifier(none,f)))],[member(none,identifier(none,f),total_function(none,natural1_set(none),natural1_set(none))),member(none,identifier(none,a),natural1_set(none)),member(none,identifier(none,b),natural_set(none)),equal(none,function(none,identifier(none,f),[identifier(none,a)]),identifier(none,c)),equal(none,function(none,identifier(none,f),[add(none,identifier(none,b),integer(none,1))]),identifier(none,c))],true).
7		disprover_po('axm7/WD',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,a),integer_set(none)),member(none,identifier(none,b),integer_set(none)),member(none,identifier(none,c),integer_set(none)),member(none,identifier(none,s),pow_subset(none,integer_set(none))),member(none,identifier(none,f),pow_subset(none,cartesian_product(none,integer_set(none),integer_set(none)))),member(none,identifier(none,g),pow_subset(none,cartesian_product(none,integer_set(none),integer_set(none)))),member(none,identifier(none,f),total_function(none,natural1_set(none),natural1_set(none))),member(none,identifier(none,a),natural1_set(none)),member(none,identifier(none,b),natural_set(none)),equal(none,function(none,identifier(none,f),[identifier(none,a)]),identifier(none,c)),member(none,identifier(none,a),domain(none,identifier(none,f))),member(none,identifier(none,f),partial_function(none,integer_set(none),integer_set(none))),equal(none,function(none,identifier(none,f),[add(none,identifier(none,b),integer(none,1))]),identifier(none,c)),member(none,add(none,identifier(none,b),integer(none,1)),domain(none,identifier(none,f))),equal(none,div(none,integer(none,10),function(none,identifier(none,f),[identifier(none,a)])),div(none,integer(none,10),identifier(none,a))),not_equal(none,function(none,identifier(none,f),[identifier(none,a)]),integer(none,0)),not_equal(none,identifier(none,a),integer(none,0))]),constants(none,[identifier(none,a),identifier(none,b),identifier(none,c),identifier(none,s),identifier(none,f),identifier(none,g)]),sets(none,[])]),conjunct(none,member(none,add(none,identifier(none,b),integer(none,1)),domain(none,identifier(none,f))),conjunct(none,member(none,identifier(none,f),partial_function(none,integer_set(none),integer_set(none))),conjunct(none,not_equal(none,function(none,identifier(none,f),[add(none,identifier(none,b),integer(none,1))]),integer(none,0)),not_equal(none,add(none,identifier(none,b),integer(none,1)),integer(none,0))))),[member(none,identifier(none,f),total_function(none,natural1_set(none),natural1_set(none))),member(none,identifier(none,a),natural1_set(none)),member(none,identifier(none,b),natural_set(none)),equal(none,function(none,identifier(none,f),[identifier(none,a)]),identifier(none,c)),member(none,identifier(none,a),domain(none,identifier(none,f))),member(none,identifier(none,f),partial_function(none,integer_set(none),integer_set(none))),equal(none,function(none,identifier(none,f),[add(none,identifier(none,b),integer(none,1))]),identifier(none,c)),member(none,add(none,identifier(none,b),integer(none,1)),domain(none,identifier(none,f))),equal(none,div(none,integer(none,10),function(none,identifier(none,f),[identifier(none,a)])),div(none,integer(none,10),identifier(none,a))),not_equal(none,function(none,identifier(none,f),[identifier(none,a)]),integer(none,0)),not_equal(none,identifier(none,a),integer(none,0))],[member(none,identifier(none,f),total_function(none,natural1_set(none),natural1_set(none))),member(none,identifier(none,a),natural1_set(none)),member(none,identifier(none,b),natural_set(none)),equal(none,function(none,identifier(none,f),[identifier(none,a)]),identifier(none,c)),equal(none,function(none,identifier(none,f),[add(none,identifier(none,b),integer(none,1))]),identifier(none,c)),equal(none,div(none,integer(none,10),function(none,identifier(none,f),[identifier(none,a)])),div(none,integer(none,10),identifier(none,a)))],true).
8		disprover_po('axm8/WD',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,a),integer_set(none)),member(none,identifier(none,b),integer_set(none)),member(none,identifier(none,c),integer_set(none)),member(none,identifier(none,s),pow_subset(none,integer_set(none))),member(none,identifier(none,f),pow_subset(none,cartesian_product(none,integer_set(none),integer_set(none)))),member(none,identifier(none,g),pow_subset(none,cartesian_product(none,integer_set(none),integer_set(none)))),member(none,identifier(none,f),total_function(none,natural1_set(none),natural1_set(none))),member(none,identifier(none,a),natural1_set(none)),member(none,identifier(none,b),natural_set(none)),equal(none,function(none,identifier(none,f),[identifier(none,a)]),identifier(none,c)),member(none,identifier(none,a),domain(none,identifier(none,f))),member(none,identifier(none,f),partial_function(none,integer_set(none),integer_set(none))),equal(none,function(none,identifier(none,f),[add(none,identifier(none,b),integer(none,1))]),identifier(none,c)),member(none,add(none,identifier(none,b),integer(none,1)),domain(none,identifier(none,f))),equal(none,div(none,integer(none,10),function(none,identifier(none,f),[identifier(none,a)])),div(none,integer(none,10),identifier(none,a))),not_equal(none,function(none,identifier(none,f),[identifier(none,a)]),integer(none,0)),not_equal(none,identifier(none,a),integer(none,0)),equal(none,div(none,integer(none,10),function(none,identifier(none,f),[add(none,identifier(none,b),integer(none,1))])),div(none,integer(none,10),add(none,identifier(none,b),integer(none,1)))),not_equal(none,function(none,identifier(none,f),[add(none,identifier(none,b),integer(none,1))]),integer(none,0)),not_equal(none,add(none,identifier(none,b),integer(none,1)),integer(none,0))]),constants(none,[identifier(none,a),identifier(none,b),identifier(none,c),identifier(none,s),identifier(none,f),identifier(none,g)]),sets(none,[])]),conjunct(none,not_equal(none,set_extension(none,[identifier(none,a),identifier(none,b),identifier(none,c)]),typeof(none,empty_set(none),pow_subset(none,integer_set(none)))),exists(none,[identifier(none,b0)],conjunct(none,member(none,identifier(none,b0),integer_set(none)),forall(none,[identifier(none,x)],implication(none,conjunct(none,member(none,identifier(none,x),integer_set(none)),member(none,identifier(none,x),set_extension(none,[identifier(none,a),identifier(none,b),identifier(none,c)]))),greater_equal(none,identifier(none,b0),identifier(none,x))))))),[member(none,identifier(none,f),total_function(none,natural1_set(none),natural1_set(none))),member(none,identifier(none,a),natural1_set(none)),member(none,identifier(none,b),natural_set(none)),equal(none,function(none,identifier(none,f),[identifier(none,a)]),identifier(none,c)),member(none,identifier(none,a),domain(none,identifier(none,f))),member(none,identifier(none,f),partial_function(none,integer_set(none),integer_set(none))),equal(none,function(none,identifier(none,f),[add(none,identifier(none,b),integer(none,1))]),identifier(none,c)),member(none,add(none,identifier(none,b),integer(none,1)),domain(none,identifier(none,f))),equal(none,div(none,integer(none,10),function(none,identifier(none,f),[identifier(none,a)])),div(none,integer(none,10),identifier(none,a))),not_equal(none,function(none,identifier(none,f),[identifier(none,a)]),integer(none,0)),not_equal(none,identifier(none,a),integer(none,0)),equal(none,div(none,integer(none,10),function(none,identifier(none,f),[add(none,identifier(none,b),integer(none,1))])),div(none,integer(none,10),add(none,identifier(none,b),integer(none,1)))),not_equal(none,function(none,identifier(none,f),[add(none,identifier(none,b),integer(none,1))]),integer(none,0)),not_equal(none,add(none,identifier(none,b),integer(none,1)),integer(none,0))],[member(none,identifier(none,f),total_function(none,natural1_set(none),natural1_set(none))),member(none,identifier(none,a),natural1_set(none)),member(none,identifier(none,b),natural_set(none)),equal(none,function(none,identifier(none,f),[identifier(none,a)]),identifier(none,c)),equal(none,function(none,identifier(none,f),[add(none,identifier(none,b),integer(none,1))]),identifier(none,c)),equal(none,div(none,integer(none,10),function(none,identifier(none,f),[identifier(none,a)])),div(none,integer(none,10),identifier(none,a))),equal(none,div(none,integer(none,10),function(none,identifier(none,f),[add(none,identifier(none,b),integer(none,1))])),div(none,integer(none,10),add(none,identifier(none,b),integer(none,1))))],unknown).
9		disprover_po('axm9/WD',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,a),integer_set(none)),member(none,identifier(none,b),integer_set(none)),member(none,identifier(none,c),integer_set(none)),member(none,identifier(none,s),pow_subset(none,integer_set(none))),member(none,identifier(none,f),pow_subset(none,cartesian_product(none,integer_set(none),integer_set(none)))),member(none,identifier(none,g),pow_subset(none,cartesian_product(none,integer_set(none),integer_set(none)))),member(none,identifier(none,f),total_function(none,natural1_set(none),natural1_set(none))),member(none,identifier(none,a),natural1_set(none)),member(none,identifier(none,b),natural_set(none)),equal(none,function(none,identifier(none,f),[identifier(none,a)]),identifier(none,c)),member(none,identifier(none,a),domain(none,identifier(none,f))),member(none,identifier(none,f),partial_function(none,integer_set(none),integer_set(none))),equal(none,function(none,identifier(none,f),[add(none,identifier(none,b),integer(none,1))]),identifier(none,c)),member(none,add(none,identifier(none,b),integer(none,1)),domain(none,identifier(none,f))),equal(none,div(none,integer(none,10),function(none,identifier(none,f),[identifier(none,a)])),div(none,integer(none,10),identifier(none,a))),not_equal(none,function(none,identifier(none,f),[identifier(none,a)]),integer(none,0)),not_equal(none,identifier(none,a),integer(none,0)),equal(none,div(none,integer(none,10),function(none,identifier(none,f),[add(none,identifier(none,b),integer(none,1))])),div(none,integer(none,10),add(none,identifier(none,b),integer(none,1)))),not_equal(none,function(none,identifier(none,f),[add(none,identifier(none,b),integer(none,1))]),integer(none,0)),not_equal(none,add(none,identifier(none,b),integer(none,1)),integer(none,0)),equal(none,max(none,set_extension(none,[identifier(none,a),identifier(none,b),identifier(none,c)])),identifier(none,c)),not_equal(none,set_extension(none,[identifier(none,a),identifier(none,b),identifier(none,c)]),typeof(none,empty_set(none),pow_subset(none,integer_set(none)))),exists(none,[identifier(none,b)],conjunct(none,member(none,identifier(none,b),integer_set(none)),forall(none,[identifier(none,x)],implication(none,conjunct(none,member(none,identifier(none,x),integer_set(none)),member(none,identifier(none,x),set_extension(none,[identifier(none,a),identifier(none,b),identifier(none,c)]))),greater_equal(none,identifier(none,b),identifier(none,x))))))]),constants(none,[identifier(none,a),identifier(none,b),identifier(none,c),identifier(none,s),identifier(none,f),identifier(none,g)]),sets(none,[])]),implication(none,greater(none,identifier(none,c),identifier(none,a)),conjunct(none,not_equal(none,interval(none,identifier(none,a),identifier(none,c)),typeof(none,empty_set(none),pow_subset(none,integer_set(none)))),exists(none,[identifier(none,b)],conjunct(none,member(none,identifier(none,b),integer_set(none)),forall(none,[identifier(none,x)],implication(none,conjunct(none,member(none,identifier(none,x),integer_set(none)),member(none,identifier(none,x),interval(none,identifier(none,a),identifier(none,c)))),greater_equal(none,identifier(none,b),identifier(none,x)))))))),[member(none,identifier(none,f),total_function(none,natural1_set(none),natural1_set(none))),member(none,identifier(none,a),natural1_set(none)),member(none,identifier(none,b),natural_set(none)),equal(none,function(none,identifier(none,f),[identifier(none,a)]),identifier(none,c)),member(none,identifier(none,a),domain(none,identifier(none,f))),member(none,identifier(none,f),partial_function(none,integer_set(none),integer_set(none))),equal(none,function(none,identifier(none,f),[add(none,identifier(none,b),integer(none,1))]),identifier(none,c)),member(none,add(none,identifier(none,b),integer(none,1)),domain(none,identifier(none,f))),equal(none,div(none,integer(none,10),function(none,identifier(none,f),[identifier(none,a)])),div(none,integer(none,10),identifier(none,a))),not_equal(none,function(none,identifier(none,f),[identifier(none,a)]),integer(none,0)),not_equal(none,identifier(none,a),integer(none,0)),equal(none,div(none,integer(none,10),function(none,identifier(none,f),[add(none,identifier(none,b),integer(none,1))])),div(none,integer(none,10),add(none,identifier(none,b),integer(none,1)))),not_equal(none,function(none,identifier(none,f),[add(none,identifier(none,b),integer(none,1))]),integer(none,0)),not_equal(none,add(none,identifier(none,b),integer(none,1)),integer(none,0)),equal(none,max(none,set_extension(none,[identifier(none,a),identifier(none,b),identifier(none,c)])),identifier(none,c)),not_equal(none,set_extension(none,[identifier(none,a),identifier(none,b),identifier(none,c)]),typeof(none,empty_set(none),pow_subset(none,integer_set(none)))),exists(none,[identifier(none,b)],conjunct(none,member(none,identifier(none,b),integer_set(none)),forall(none,[identifier(none,x)],implication(none,conjunct(none,member(none,identifier(none,x),integer_set(none)),member(none,identifier(none,x),set_extension(none,[identifier(none,a),identifier(none,b),identifier(none,c)]))),greater_equal(none,identifier(none,b),identifier(none,x))))))],[member(none,identifier(none,f),total_function(none,natural1_set(none),natural1_set(none))),member(none,identifier(none,a),natural1_set(none)),member(none,identifier(none,b),natural_set(none)),equal(none,function(none,identifier(none,f),[identifier(none,a)]),identifier(none,c)),equal(none,function(none,identifier(none,f),[add(none,identifier(none,b),integer(none,1))]),identifier(none,c)),equal(none,div(none,integer(none,10),function(none,identifier(none,f),[identifier(none,a)])),div(none,integer(none,10),identifier(none,a))),equal(none,div(none,integer(none,10),function(none,identifier(none,f),[add(none,identifier(none,b),integer(none,1))])),div(none,integer(none,10),add(none,identifier(none,b),integer(none,1)))),equal(none,max(none,set_extension(none,[identifier(none,a),identifier(none,b),identifier(none,c)])),identifier(none,c))],unknown).
10		disprover_po('axm11/WD',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,a),integer_set(none)),member(none,identifier(none,b),integer_set(none)),member(none,identifier(none,c),integer_set(none)),member(none,identifier(none,s),pow_subset(none,integer_set(none))),member(none,identifier(none,f),pow_subset(none,cartesian_product(none,integer_set(none),integer_set(none)))),member(none,identifier(none,g),pow_subset(none,cartesian_product(none,integer_set(none),integer_set(none)))),member(none,identifier(none,f),total_function(none,natural1_set(none),natural1_set(none))),member(none,identifier(none,a),natural1_set(none)),member(none,identifier(none,b),natural_set(none)),equal(none,function(none,identifier(none,f),[identifier(none,a)]),identifier(none,c)),member(none,identifier(none,a),domain(none,identifier(none,f))),member(none,identifier(none,f),partial_function(none,integer_set(none),integer_set(none))),equal(none,function(none,identifier(none,f),[add(none,identifier(none,b),integer(none,1))]),identifier(none,c)),member(none,add(none,identifier(none,b),integer(none,1)),domain(none,identifier(none,f))),equal(none,div(none,integer(none,10),function(none,identifier(none,f),[identifier(none,a)])),div(none,integer(none,10),identifier(none,a))),not_equal(none,function(none,identifier(none,f),[identifier(none,a)]),integer(none,0)),not_equal(none,identifier(none,a),integer(none,0)),equal(none,div(none,integer(none,10),function(none,identifier(none,f),[add(none,identifier(none,b),integer(none,1))])),div(none,integer(none,10),add(none,identifier(none,b),integer(none,1)))),not_equal(none,function(none,identifier(none,f),[add(none,identifier(none,b),integer(none,1))]),integer(none,0)),not_equal(none,add(none,identifier(none,b),integer(none,1)),integer(none,0)),equal(none,max(none,set_extension(none,[identifier(none,a),identifier(none,b),identifier(none,c)])),identifier(none,c)),not_equal(none,set_extension(none,[identifier(none,a),identifier(none,b),identifier(none,c)]),typeof(none,empty_set(none),pow_subset(none,integer_set(none)))),exists(none,[identifier(none,b)],conjunct(none,member(none,identifier(none,b),integer_set(none)),forall(none,[identifier(none,x)],implication(none,conjunct(none,member(none,identifier(none,x),integer_set(none)),member(none,identifier(none,x),set_extension(none,[identifier(none,a),identifier(none,b),identifier(none,c)]))),greater_equal(none,identifier(none,b),identifier(none,x)))))),conjunct(none,greater(none,identifier(none,c),identifier(none,a)),equal(none,max(none,interval(none,identifier(none,a),identifier(none,c))),identifier(none,c))),implication(none,greater(none,identifier(none,c),identifier(none,a)),conjunct(none,not_equal(none,interval(none,identifier(none,a),identifier(none,c)),typeof(none,empty_set(none),pow_subset(none,integer_set(none)))),exists(none,[identifier(none,b)],conjunct(none,member(none,identifier(none,b),integer_set(none)),forall(none,[identifier(none,x)],implication(none,conjunct(none,member(none,identifier(none,x),integer_set(none)),member(none,identifier(none,x),interval(none,identifier(none,a),identifier(none,c)))),greater_equal(none,identifier(none,b),identifier(none,x)))))))),member(none,identifier(none,g),total_function(none,interval(none,identifier(none,a),identifier(none,c)),natural1_set(none)))]),constants(none,[identifier(none,a),identifier(none,b),identifier(none,c),identifier(none,s),identifier(none,f),identifier(none,g)]),sets(none,[])]),conjunct(none,member(none,identifier(none,a),domain(none,identifier(none,g))),conjunct(none,member(none,identifier(none,g),partial_function(none,integer_set(none),integer_set(none))),member(none,identifier(none,c),domain(none,identifier(none,g))))),[member(none,identifier(none,f),total_function(none,natural1_set(none),natural1_set(none))),member(none,identifier(none,a),natural1_set(none)),member(none,identifier(none,b),natural_set(none)),equal(none,function(none,identifier(none,f),[identifier(none,a)]),identifier(none,c)),member(none,identifier(none,a),domain(none,identifier(none,f))),member(none,identifier(none,f),partial_function(none,integer_set(none),integer_set(none))),equal(none,function(none,identifier(none,f),[add(none,identifier(none,b),integer(none,1))]),identifier(none,c)),member(none,add(none,identifier(none,b),integer(none,1)),domain(none,identifier(none,f))),equal(none,div(none,integer(none,10),function(none,identifier(none,f),[identifier(none,a)])),div(none,integer(none,10),identifier(none,a))),not_equal(none,function(none,identifier(none,f),[identifier(none,a)]),integer(none,0)),not_equal(none,identifier(none,a),integer(none,0)),equal(none,div(none,integer(none,10),function(none,identifier(none,f),[add(none,identifier(none,b),integer(none,1))])),div(none,integer(none,10),add(none,identifier(none,b),integer(none,1)))),not_equal(none,function(none,identifier(none,f),[add(none,identifier(none,b),integer(none,1))]),integer(none,0)),not_equal(none,add(none,identifier(none,b),integer(none,1)),integer(none,0)),equal(none,max(none,set_extension(none,[identifier(none,a),identifier(none,b),identifier(none,c)])),identifier(none,c)),not_equal(none,set_extension(none,[identifier(none,a),identifier(none,b),identifier(none,c)]),typeof(none,empty_set(none),pow_subset(none,integer_set(none)))),exists(none,[identifier(none,b)],conjunct(none,member(none,identifier(none,b),integer_set(none)),forall(none,[identifier(none,x)],implication(none,conjunct(none,member(none,identifier(none,x),integer_set(none)),member(none,identifier(none,x),set_extension(none,[identifier(none,a),identifier(none,b),identifier(none,c)]))),greater_equal(none,identifier(none,b),identifier(none,x)))))),conjunct(none,greater(none,identifier(none,c),identifier(none,a)),equal(none,max(none,interval(none,identifier(none,a),identifier(none,c))),identifier(none,c))),implication(none,greater(none,identifier(none,c),identifier(none,a)),conjunct(none,not_equal(none,interval(none,identifier(none,a),identifier(none,c)),typeof(none,empty_set(none),pow_subset(none,integer_set(none)))),exists(none,[identifier(none,b)],conjunct(none,member(none,identifier(none,b),integer_set(none)),forall(none,[identifier(none,x)],implication(none,conjunct(none,member(none,identifier(none,x),integer_set(none)),member(none,identifier(none,x),interval(none,identifier(none,a),identifier(none,c)))),greater_equal(none,identifier(none,b),identifier(none,x)))))))),member(none,identifier(none,g),total_function(none,interval(none,identifier(none,a),identifier(none,c)),natural1_set(none)))],[member(none,identifier(none,f),total_function(none,natural1_set(none),natural1_set(none))),member(none,identifier(none,a),natural1_set(none)),member(none,identifier(none,b),natural_set(none)),equal(none,function(none,identifier(none,f),[identifier(none,a)]),identifier(none,c)),equal(none,function(none,identifier(none,f),[add(none,identifier(none,b),integer(none,1))]),identifier(none,c)),equal(none,div(none,integer(none,10),function(none,identifier(none,f),[identifier(none,a)])),div(none,integer(none,10),identifier(none,a))),equal(none,div(none,integer(none,10),function(none,identifier(none,f),[add(none,identifier(none,b),integer(none,1))])),div(none,integer(none,10),add(none,identifier(none,b),integer(none,1)))),equal(none,max(none,set_extension(none,[identifier(none,a),identifier(none,b),identifier(none,c)])),identifier(none,c)),conjunct(none,greater(none,identifier(none,c),identifier(none,a)),equal(none,max(none,interval(none,identifier(none,a),identifier(none,c))),identifier(none,c))),member(none,identifier(none,g),total_function(none,interval(none,identifier(none,a),identifier(none,c)),natural1_set(none)))],true).
11		disprover_po('axm12/WD',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,a),integer_set(none)),member(none,identifier(none,b),integer_set(none)),member(none,identifier(none,c),integer_set(none)),member(none,identifier(none,s),pow_subset(none,integer_set(none))),member(none,identifier(none,f),pow_subset(none,cartesian_product(none,integer_set(none),integer_set(none)))),member(none,identifier(none,g),pow_subset(none,cartesian_product(none,integer_set(none),integer_set(none)))),member(none,identifier(none,f),total_function(none,natural1_set(none),natural1_set(none))),member(none,identifier(none,a),natural1_set(none)),member(none,identifier(none,b),natural_set(none)),equal(none,function(none,identifier(none,f),[identifier(none,a)]),identifier(none,c)),member(none,identifier(none,a),domain(none,identifier(none,f))),member(none,identifier(none,f),partial_function(none,integer_set(none),integer_set(none))),equal(none,function(none,identifier(none,f),[add(none,identifier(none,b),integer(none,1))]),identifier(none,c)),member(none,add(none,identifier(none,b),integer(none,1)),domain(none,identifier(none,f))),equal(none,div(none,integer(none,10),function(none,identifier(none,f),[identifier(none,a)])),div(none,integer(none,10),identifier(none,a))),not_equal(none,function(none,identifier(none,f),[identifier(none,a)]),integer(none,0)),not_equal(none,identifier(none,a),integer(none,0)),equal(none,div(none,integer(none,10),function(none,identifier(none,f),[add(none,identifier(none,b),integer(none,1))])),div(none,integer(none,10),add(none,identifier(none,b),integer(none,1)))),not_equal(none,function(none,identifier(none,f),[add(none,identifier(none,b),integer(none,1))]),integer(none,0)),not_equal(none,add(none,identifier(none,b),integer(none,1)),integer(none,0)),equal(none,max(none,set_extension(none,[identifier(none,a),identifier(none,b),identifier(none,c)])),identifier(none,c)),not_equal(none,set_extension(none,[identifier(none,a),identifier(none,b),identifier(none,c)]),typeof(none,empty_set(none),pow_subset(none,integer_set(none)))),exists(none,[identifier(none,b)],conjunct(none,member(none,identifier(none,b),integer_set(none)),forall(none,[identifier(none,x)],implication(none,conjunct(none,member(none,identifier(none,x),integer_set(none)),member(none,identifier(none,x),set_extension(none,[identifier(none,a),identifier(none,b),identifier(none,c)]))),greater_equal(none,identifier(none,b),identifier(none,x)))))),conjunct(none,greater(none,identifier(none,c),identifier(none,a)),equal(none,max(none,interval(none,identifier(none,a),identifier(none,c))),identifier(none,c))),implication(none,greater(none,identifier(none,c),identifier(none,a)),conjunct(none,not_equal(none,interval(none,identifier(none,a),identifier(none,c)),typeof(none,empty_set(none),pow_subset(none,integer_set(none)))),exists(none,[identifier(none,b)],conjunct(none,member(none,identifier(none,b),integer_set(none)),forall(none,[identifier(none,x)],implication(none,conjunct(none,member(none,identifier(none,x),integer_set(none)),member(none,identifier(none,x),interval(none,identifier(none,a),identifier(none,c)))),greater_equal(none,identifier(none,b),identifier(none,x)))))))),member(none,identifier(none,g),total_function(none,interval(none,identifier(none,a),identifier(none,c)),natural1_set(none))),equal(none,function(none,identifier(none,g),[identifier(none,a)]),function(none,identifier(none,g),[identifier(none,c)])),member(none,identifier(none,a),domain(none,identifier(none,g))),member(none,identifier(none,g),partial_function(none,integer_set(none),integer_set(none))),member(none,identifier(none,c),domain(none,identifier(none,g)))]),constants(none,[identifier(none,a),identifier(none,b),identifier(none,c),identifier(none,s),identifier(none,f),identifier(none,g)]),sets(none,[])]),finite(none,set_extension(none,[identifier(none,a),identifier(none,b),identifier(none,c)])),[member(none,identifier(none,f),total_function(none,natural1_set(none),natural1_set(none))),member(none,identifier(none,a),natural1_set(none)),member(none,identifier(none,b),natural_set(none)),equal(none,function(none,identifier(none,f),[identifier(none,a)]),identifier(none,c)),member(none,identifier(none,a),domain(none,identifier(none,f))),member(none,identifier(none,f),partial_function(none,integer_set(none),integer_set(none))),equal(none,function(none,identifier(none,f),[add(none,identifier(none,b),integer(none,1))]),identifier(none,c)),member(none,add(none,identifier(none,b),integer(none,1)),domain(none,identifier(none,f))),equal(none,div(none,integer(none,10),function(none,identifier(none,f),[identifier(none,a)])),div(none,integer(none,10),identifier(none,a))),not_equal(none,function(none,identifier(none,f),[identifier(none,a)]),integer(none,0)),not_equal(none,identifier(none,a),integer(none,0)),equal(none,div(none,integer(none,10),function(none,identifier(none,f),[add(none,identifier(none,b),integer(none,1))])),div(none,integer(none,10),add(none,identifier(none,b),integer(none,1)))),not_equal(none,function(none,identifier(none,f),[add(none,identifier(none,b),integer(none,1))]),integer(none,0)),not_equal(none,add(none,identifier(none,b),integer(none,1)),integer(none,0)),equal(none,max(none,set_extension(none,[identifier(none,a),identifier(none,b),identifier(none,c)])),identifier(none,c)),not_equal(none,set_extension(none,[identifier(none,a),identifier(none,b),identifier(none,c)]),typeof(none,empty_set(none),pow_subset(none,integer_set(none)))),exists(none,[identifier(none,b)],conjunct(none,member(none,identifier(none,b),integer_set(none)),forall(none,[identifier(none,x)],implication(none,conjunct(none,member(none,identifier(none,x),integer_set(none)),member(none,identifier(none,x),set_extension(none,[identifier(none,a),identifier(none,b),identifier(none,c)]))),greater_equal(none,identifier(none,b),identifier(none,x)))))),conjunct(none,greater(none,identifier(none,c),identifier(none,a)),equal(none,max(none,interval(none,identifier(none,a),identifier(none,c))),identifier(none,c))),implication(none,greater(none,identifier(none,c),identifier(none,a)),conjunct(none,not_equal(none,interval(none,identifier(none,a),identifier(none,c)),typeof(none,empty_set(none),pow_subset(none,integer_set(none)))),exists(none,[identifier(none,b)],conjunct(none,member(none,identifier(none,b),integer_set(none)),forall(none,[identifier(none,x)],implication(none,conjunct(none,member(none,identifier(none,x),integer_set(none)),member(none,identifier(none,x),interval(none,identifier(none,a),identifier(none,c)))),greater_equal(none,identifier(none,b),identifier(none,x)))))))),member(none,identifier(none,g),total_function(none,interval(none,identifier(none,a),identifier(none,c)),natural1_set(none))),equal(none,function(none,identifier(none,g),[identifier(none,a)]),function(none,identifier(none,g),[identifier(none,c)])),member(none,identifier(none,a),domain(none,identifier(none,g))),member(none,identifier(none,g),partial_function(none,integer_set(none),integer_set(none))),member(none,identifier(none,c),domain(none,identifier(none,g)))],[member(none,identifier(none,f),total_function(none,natural1_set(none),natural1_set(none))),member(none,identifier(none,a),natural1_set(none)),member(none,identifier(none,b),natural_set(none)),equal(none,function(none,identifier(none,f),[identifier(none,a)]),identifier(none,c)),equal(none,function(none,identifier(none,f),[add(none,identifier(none,b),integer(none,1))]),identifier(none,c)),equal(none,div(none,integer(none,10),function(none,identifier(none,f),[identifier(none,a)])),div(none,integer(none,10),identifier(none,a))),equal(none,div(none,integer(none,10),function(none,identifier(none,f),[add(none,identifier(none,b),integer(none,1))])),div(none,integer(none,10),add(none,identifier(none,b),integer(none,1)))),equal(none,max(none,set_extension(none,[identifier(none,a),identifier(none,b),identifier(none,c)])),identifier(none,c)),conjunct(none,greater(none,identifier(none,c),identifier(none,a)),equal(none,max(none,interval(none,identifier(none,a),identifier(none,c))),identifier(none,c))),member(none,identifier(none,g),total_function(none,interval(none,identifier(none,a),identifier(none,c)),natural1_set(none))),equal(none,function(none,identifier(none,g),[identifier(none,a)]),function(none,identifier(none,g),[identifier(none,c)]))],true).
12		disprover_po('axm13/WD',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,a),integer_set(none)),member(none,identifier(none,b),integer_set(none)),member(none,identifier(none,c),integer_set(none)),member(none,identifier(none,s),pow_subset(none,integer_set(none))),member(none,identifier(none,f),pow_subset(none,cartesian_product(none,integer_set(none),integer_set(none)))),member(none,identifier(none,g),pow_subset(none,cartesian_product(none,integer_set(none),integer_set(none)))),member(none,identifier(none,f),total_function(none,natural1_set(none),natural1_set(none))),member(none,identifier(none,a),natural1_set(none)),member(none,identifier(none,b),natural_set(none)),equal(none,function(none,identifier(none,f),[identifier(none,a)]),identifier(none,c)),member(none,identifier(none,a),domain(none,identifier(none,f))),member(none,identifier(none,f),partial_function(none,integer_set(none),integer_set(none))),equal(none,function(none,identifier(none,f),[add(none,identifier(none,b),integer(none,1))]),identifier(none,c)),member(none,add(none,identifier(none,b),integer(none,1)),domain(none,identifier(none,f))),equal(none,div(none,integer(none,10),function(none,identifier(none,f),[identifier(none,a)])),div(none,integer(none,10),identifier(none,a))),not_equal(none,function(none,identifier(none,f),[identifier(none,a)]),integer(none,0)),not_equal(none,identifier(none,a),integer(none,0)),equal(none,div(none,integer(none,10),function(none,identifier(none,f),[add(none,identifier(none,b),integer(none,1))])),div(none,integer(none,10),add(none,identifier(none,b),integer(none,1)))),not_equal(none,function(none,identifier(none,f),[add(none,identifier(none,b),integer(none,1))]),integer(none,0)),not_equal(none,add(none,identifier(none,b),integer(none,1)),integer(none,0)),equal(none,max(none,set_extension(none,[identifier(none,a),identifier(none,b),identifier(none,c)])),identifier(none,c)),not_equal(none,set_extension(none,[identifier(none,a),identifier(none,b),identifier(none,c)]),typeof(none,empty_set(none),pow_subset(none,integer_set(none)))),exists(none,[identifier(none,b)],conjunct(none,member(none,identifier(none,b),integer_set(none)),forall(none,[identifier(none,x)],implication(none,conjunct(none,member(none,identifier(none,x),integer_set(none)),member(none,identifier(none,x),set_extension(none,[identifier(none,a),identifier(none,b),identifier(none,c)]))),greater_equal(none,identifier(none,b),identifier(none,x)))))),conjunct(none,greater(none,identifier(none,c),identifier(none,a)),equal(none,max(none,interval(none,identifier(none,a),identifier(none,c))),identifier(none,c))),implication(none,greater(none,identifier(none,c),identifier(none,a)),conjunct(none,not_equal(none,interval(none,identifier(none,a),identifier(none,c)),typeof(none,empty_set(none),pow_subset(none,integer_set(none)))),exists(none,[identifier(none,b)],conjunct(none,member(none,identifier(none,b),integer_set(none)),forall(none,[identifier(none,x)],implication(none,conjunct(none,member(none,identifier(none,x),integer_set(none)),member(none,identifier(none,x),interval(none,identifier(none,a),identifier(none,c)))),greater_equal(none,identifier(none,b),identifier(none,x)))))))),member(none,identifier(none,g),total_function(none,interval(none,identifier(none,a),identifier(none,c)),natural1_set(none))),equal(none,function(none,identifier(none,g),[identifier(none,a)]),function(none,identifier(none,g),[identifier(none,c)])),member(none,identifier(none,a),domain(none,identifier(none,g))),member(none,identifier(none,g),partial_function(none,integer_set(none),integer_set(none))),member(none,identifier(none,c),domain(none,identifier(none,g))),equal(none,card(none,set_extension(none,[identifier(none,a),identifier(none,b),identifier(none,c)])),integer(none,3)),finite(none,set_extension(none,[identifier(none,a),identifier(none,b),identifier(none,c)]))]),constants(none,[identifier(none,a),identifier(none,b),identifier(none,c),identifier(none,s),identifier(none,f),identifier(none,g)]),sets(none,[])]),finite(none,interval(none,identifier(none,a),identifier(none,c))),[member(none,identifier(none,f),total_function(none,natural1_set(none),natural1_set(none))),member(none,identifier(none,a),natural1_set(none)),member(none,identifier(none,b),natural_set(none)),equal(none,function(none,identifier(none,f),[identifier(none,a)]),identifier(none,c)),member(none,identifier(none,a),domain(none,identifier(none,f))),member(none,identifier(none,f),partial_function(none,integer_set(none),integer_set(none))),equal(none,function(none,identifier(none,f),[add(none,identifier(none,b),integer(none,1))]),identifier(none,c)),member(none,add(none,identifier(none,b),integer(none,1)),domain(none,identifier(none,f))),equal(none,div(none,integer(none,10),function(none,identifier(none,f),[identifier(none,a)])),div(none,integer(none,10),identifier(none,a))),not_equal(none,function(none,identifier(none,f),[identifier(none,a)]),integer(none,0)),not_equal(none,identifier(none,a),integer(none,0)),equal(none,div(none,integer(none,10),function(none,identifier(none,f),[add(none,identifier(none,b),integer(none,1))])),div(none,integer(none,10),add(none,identifier(none,b),integer(none,1)))),not_equal(none,function(none,identifier(none,f),[add(none,identifier(none,b),integer(none,1))]),integer(none,0)),not_equal(none,add(none,identifier(none,b),integer(none,1)),integer(none,0)),equal(none,max(none,set_extension(none,[identifier(none,a),identifier(none,b),identifier(none,c)])),identifier(none,c)),not_equal(none,set_extension(none,[identifier(none,a),identifier(none,b),identifier(none,c)]),typeof(none,empty_set(none),pow_subset(none,integer_set(none)))),exists(none,[identifier(none,b)],conjunct(none,member(none,identifier(none,b),integer_set(none)),forall(none,[identifier(none,x)],implication(none,conjunct(none,member(none,identifier(none,x),integer_set(none)),member(none,identifier(none,x),set_extension(none,[identifier(none,a),identifier(none,b),identifier(none,c)]))),greater_equal(none,identifier(none,b),identifier(none,x)))))),conjunct(none,greater(none,identifier(none,c),identifier(none,a)),equal(none,max(none,interval(none,identifier(none,a),identifier(none,c))),identifier(none,c))),implication(none,greater(none,identifier(none,c),identifier(none,a)),conjunct(none,not_equal(none,interval(none,identifier(none,a),identifier(none,c)),typeof(none,empty_set(none),pow_subset(none,integer_set(none)))),exists(none,[identifier(none,b)],conjunct(none,member(none,identifier(none,b),integer_set(none)),forall(none,[identifier(none,x)],implication(none,conjunct(none,member(none,identifier(none,x),integer_set(none)),member(none,identifier(none,x),interval(none,identifier(none,a),identifier(none,c)))),greater_equal(none,identifier(none,b),identifier(none,x)))))))),member(none,identifier(none,g),total_function(none,interval(none,identifier(none,a),identifier(none,c)),natural1_set(none))),equal(none,function(none,identifier(none,g),[identifier(none,a)]),function(none,identifier(none,g),[identifier(none,c)])),member(none,identifier(none,a),domain(none,identifier(none,g))),member(none,identifier(none,g),partial_function(none,integer_set(none),integer_set(none))),member(none,identifier(none,c),domain(none,identifier(none,g))),equal(none,card(none,set_extension(none,[identifier(none,a),identifier(none,b),identifier(none,c)])),integer(none,3)),finite(none,set_extension(none,[identifier(none,a),identifier(none,b),identifier(none,c)]))],[member(none,identifier(none,f),total_function(none,natural1_set(none),natural1_set(none))),member(none,identifier(none,a),natural1_set(none)),member(none,identifier(none,b),natural_set(none)),equal(none,function(none,identifier(none,f),[identifier(none,a)]),identifier(none,c)),equal(none,function(none,identifier(none,f),[add(none,identifier(none,b),integer(none,1))]),identifier(none,c)),equal(none,div(none,integer(none,10),function(none,identifier(none,f),[identifier(none,a)])),div(none,integer(none,10),identifier(none,a))),equal(none,div(none,integer(none,10),function(none,identifier(none,f),[add(none,identifier(none,b),integer(none,1))])),div(none,integer(none,10),add(none,identifier(none,b),integer(none,1)))),equal(none,max(none,set_extension(none,[identifier(none,a),identifier(none,b),identifier(none,c)])),identifier(none,c)),conjunct(none,greater(none,identifier(none,c),identifier(none,a)),equal(none,max(none,interval(none,identifier(none,a),identifier(none,c))),identifier(none,c))),member(none,identifier(none,g),total_function(none,interval(none,identifier(none,a),identifier(none,c)),natural1_set(none))),equal(none,function(none,identifier(none,g),[identifier(none,a)]),function(none,identifier(none,g),[identifier(none,c)])),equal(none,card(none,set_extension(none,[identifier(none,a),identifier(none,b),identifier(none,c)])),integer(none,3))],true).
13		disprover_po('axm15/WD',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,a),integer_set(none)),member(none,identifier(none,b),integer_set(none)),member(none,identifier(none,c),integer_set(none)),member(none,identifier(none,s),pow_subset(none,integer_set(none))),member(none,identifier(none,f),pow_subset(none,cartesian_product(none,integer_set(none),integer_set(none)))),member(none,identifier(none,g),pow_subset(none,cartesian_product(none,integer_set(none),integer_set(none)))),member(none,identifier(none,f),total_function(none,natural1_set(none),natural1_set(none))),member(none,identifier(none,a),natural1_set(none)),member(none,identifier(none,b),natural_set(none)),equal(none,function(none,identifier(none,f),[identifier(none,a)]),identifier(none,c)),member(none,identifier(none,a),domain(none,identifier(none,f))),member(none,identifier(none,f),partial_function(none,integer_set(none),integer_set(none))),equal(none,function(none,identifier(none,f),[add(none,identifier(none,b),integer(none,1))]),identifier(none,c)),member(none,add(none,identifier(none,b),integer(none,1)),domain(none,identifier(none,f))),equal(none,div(none,integer(none,10),function(none,identifier(none,f),[identifier(none,a)])),div(none,integer(none,10),identifier(none,a))),not_equal(none,function(none,identifier(none,f),[identifier(none,a)]),integer(none,0)),not_equal(none,identifier(none,a),integer(none,0)),equal(none,div(none,integer(none,10),function(none,identifier(none,f),[add(none,identifier(none,b),integer(none,1))])),div(none,integer(none,10),add(none,identifier(none,b),integer(none,1)))),not_equal(none,function(none,identifier(none,f),[add(none,identifier(none,b),integer(none,1))]),integer(none,0)),not_equal(none,add(none,identifier(none,b),integer(none,1)),integer(none,0)),equal(none,max(none,set_extension(none,[identifier(none,a),identifier(none,b),identifier(none,c)])),identifier(none,c)),not_equal(none,set_extension(none,[identifier(none,a),identifier(none,b),identifier(none,c)]),typeof(none,empty_set(none),pow_subset(none,integer_set(none)))),exists(none,[identifier(none,b)],conjunct(none,member(none,identifier(none,b),integer_set(none)),forall(none,[identifier(none,x)],implication(none,conjunct(none,member(none,identifier(none,x),integer_set(none)),member(none,identifier(none,x),set_extension(none,[identifier(none,a),identifier(none,b),identifier(none,c)]))),greater_equal(none,identifier(none,b),identifier(none,x)))))),conjunct(none,greater(none,identifier(none,c),identifier(none,a)),equal(none,max(none,interval(none,identifier(none,a),identifier(none,c))),identifier(none,c))),implication(none,greater(none,identifier(none,c),identifier(none,a)),conjunct(none,not_equal(none,interval(none,identifier(none,a),identifier(none,c)),typeof(none,empty_set(none),pow_subset(none,integer_set(none)))),exists(none,[identifier(none,b)],conjunct(none,member(none,identifier(none,b),integer_set(none)),forall(none,[identifier(none,x)],implication(none,conjunct(none,member(none,identifier(none,x),integer_set(none)),member(none,identifier(none,x),interval(none,identifier(none,a),identifier(none,c)))),greater_equal(none,identifier(none,b),identifier(none,x)))))))),member(none,identifier(none,g),total_function(none,interval(none,identifier(none,a),identifier(none,c)),natural1_set(none))),equal(none,function(none,identifier(none,g),[identifier(none,a)]),function(none,identifier(none,g),[identifier(none,c)])),member(none,identifier(none,a),domain(none,identifier(none,g))),member(none,identifier(none,g),partial_function(none,integer_set(none),integer_set(none))),member(none,identifier(none,c),domain(none,identifier(none,g))),equal(none,card(none,set_extension(none,[identifier(none,a),identifier(none,b),identifier(none,c)])),integer(none,3)),finite(none,set_extension(none,[identifier(none,a),identifier(none,b),identifier(none,c)])),greater(none,card(none,interval(none,identifier(none,a),identifier(none,c))),integer(none,1)),finite(none,interval(none,identifier(none,a),identifier(none,c))),subset(none,identifier(none,s),set_extension(none,[identifier(none,a),identifier(none,b),identifier(none,c)]))]),constants(none,[identifier(none,a),identifier(none,b),identifier(none,c),identifier(none,s),identifier(none,f),identifier(none,g)]),sets(none,[])]),finite(none,identifier(none,s)),[member(none,identifier(none,f),total_function(none,natural1_set(none),natural1_set(none))),member(none,identifier(none,a),natural1_set(none)),member(none,identifier(none,b),natural_set(none)),equal(none,function(none,identifier(none,f),[identifier(none,a)]),identifier(none,c)),member(none,identifier(none,a),domain(none,identifier(none,f))),member(none,identifier(none,f),partial_function(none,integer_set(none),integer_set(none))),equal(none,function(none,identifier(none,f),[add(none,identifier(none,b),integer(none,1))]),identifier(none,c)),member(none,add(none,identifier(none,b),integer(none,1)),domain(none,identifier(none,f))),equal(none,div(none,integer(none,10),function(none,identifier(none,f),[identifier(none,a)])),div(none,integer(none,10),identifier(none,a))),not_equal(none,function(none,identifier(none,f),[identifier(none,a)]),integer(none,0)),not_equal(none,identifier(none,a),integer(none,0)),equal(none,div(none,integer(none,10),function(none,identifier(none,f),[add(none,identifier(none,b),integer(none,1))])),div(none,integer(none,10),add(none,identifier(none,b),integer(none,1)))),not_equal(none,function(none,identifier(none,f),[add(none,identifier(none,b),integer(none,1))]),integer(none,0)),not_equal(none,add(none,identifier(none,b),integer(none,1)),integer(none,0)),equal(none,max(none,set_extension(none,[identifier(none,a),identifier(none,b),identifier(none,c)])),identifier(none,c)),not_equal(none,set_extension(none,[identifier(none,a),identifier(none,b),identifier(none,c)]),typeof(none,empty_set(none),pow_subset(none,integer_set(none)))),exists(none,[identifier(none,b)],conjunct(none,member(none,identifier(none,b),integer_set(none)),forall(none,[identifier(none,x)],implication(none,conjunct(none,member(none,identifier(none,x),integer_set(none)),member(none,identifier(none,x),set_extension(none,[identifier(none,a),identifier(none,b),identifier(none,c)]))),greater_equal(none,identifier(none,b),identifier(none,x)))))),conjunct(none,greater(none,identifier(none,c),identifier(none,a)),equal(none,max(none,interval(none,identifier(none,a),identifier(none,c))),identifier(none,c))),implication(none,greater(none,identifier(none,c),identifier(none,a)),conjunct(none,not_equal(none,interval(none,identifier(none,a),identifier(none,c)),typeof(none,empty_set(none),pow_subset(none,integer_set(none)))),exists(none,[identifier(none,b)],conjunct(none,member(none,identifier(none,b),integer_set(none)),forall(none,[identifier(none,x)],implication(none,conjunct(none,member(none,identifier(none,x),integer_set(none)),member(none,identifier(none,x),interval(none,identifier(none,a),identifier(none,c)))),greater_equal(none,identifier(none,b),identifier(none,x)))))))),member(none,identifier(none,g),total_function(none,interval(none,identifier(none,a),identifier(none,c)),natural1_set(none))),equal(none,function(none,identifier(none,g),[identifier(none,a)]),function(none,identifier(none,g),[identifier(none,c)])),member(none,identifier(none,a),domain(none,identifier(none,g))),member(none,identifier(none,g),partial_function(none,integer_set(none),integer_set(none))),member(none,identifier(none,c),domain(none,identifier(none,g))),equal(none,card(none,set_extension(none,[identifier(none,a),identifier(none,b),identifier(none,c)])),integer(none,3)),finite(none,set_extension(none,[identifier(none,a),identifier(none,b),identifier(none,c)])),greater(none,card(none,interval(none,identifier(none,a),identifier(none,c))),integer(none,1)),finite(none,interval(none,identifier(none,a),identifier(none,c))),subset(none,identifier(none,s),set_extension(none,[identifier(none,a),identifier(none,b),identifier(none,c)]))],[member(none,identifier(none,f),total_function(none,natural1_set(none),natural1_set(none))),member(none,identifier(none,a),natural1_set(none)),member(none,identifier(none,b),natural_set(none)),equal(none,function(none,identifier(none,f),[identifier(none,a)]),identifier(none,c)),equal(none,function(none,identifier(none,f),[add(none,identifier(none,b),integer(none,1))]),identifier(none,c)),equal(none,div(none,integer(none,10),function(none,identifier(none,f),[identifier(none,a)])),div(none,integer(none,10),identifier(none,a))),equal(none,div(none,integer(none,10),function(none,identifier(none,f),[add(none,identifier(none,b),integer(none,1))])),div(none,integer(none,10),add(none,identifier(none,b),integer(none,1)))),equal(none,max(none,set_extension(none,[identifier(none,a),identifier(none,b),identifier(none,c)])),identifier(none,c)),conjunct(none,greater(none,identifier(none,c),identifier(none,a)),equal(none,max(none,interval(none,identifier(none,a),identifier(none,c))),identifier(none,c))),member(none,identifier(none,g),total_function(none,interval(none,identifier(none,a),identifier(none,c)),natural1_set(none))),equal(none,function(none,identifier(none,g),[identifier(none,a)]),function(none,identifier(none,g),[identifier(none,c)])),equal(none,card(none,set_extension(none,[identifier(none,a),identifier(none,b),identifier(none,c)])),integer(none,3)),greater(none,card(none,interval(none,identifier(none,a),identifier(none,c))),integer(none,1)),subset(none,identifier(none,s),set_extension(none,[identifier(none,a),identifier(none,b),identifier(none,c)]))],true).
14		disprover_po('axm16/WD',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,a),integer_set(none)),member(none,identifier(none,b),integer_set(none)),member(none,identifier(none,c),integer_set(none)),member(none,identifier(none,s),pow_subset(none,integer_set(none))),member(none,identifier(none,f),pow_subset(none,cartesian_product(none,integer_set(none),integer_set(none)))),member(none,identifier(none,g),pow_subset(none,cartesian_product(none,integer_set(none),integer_set(none)))),member(none,identifier(none,f),total_function(none,natural1_set(none),natural1_set(none))),member(none,identifier(none,a),natural1_set(none)),member(none,identifier(none,b),natural_set(none)),equal(none,function(none,identifier(none,f),[identifier(none,a)]),identifier(none,c)),member(none,identifier(none,a),domain(none,identifier(none,f))),member(none,identifier(none,f),partial_function(none,integer_set(none),integer_set(none))),equal(none,function(none,identifier(none,f),[add(none,identifier(none,b),integer(none,1))]),identifier(none,c)),member(none,add(none,identifier(none,b),integer(none,1)),domain(none,identifier(none,f))),equal(none,div(none,integer(none,10),function(none,identifier(none,f),[identifier(none,a)])),div(none,integer(none,10),identifier(none,a))),not_equal(none,function(none,identifier(none,f),[identifier(none,a)]),integer(none,0)),not_equal(none,identifier(none,a),integer(none,0)),equal(none,div(none,integer(none,10),function(none,identifier(none,f),[add(none,identifier(none,b),integer(none,1))])),div(none,integer(none,10),add(none,identifier(none,b),integer(none,1)))),not_equal(none,function(none,identifier(none,f),[add(none,identifier(none,b),integer(none,1))]),integer(none,0)),not_equal(none,add(none,identifier(none,b),integer(none,1)),integer(none,0)),equal(none,max(none,set_extension(none,[identifier(none,a),identifier(none,b),identifier(none,c)])),identifier(none,c)),not_equal(none,set_extension(none,[identifier(none,a),identifier(none,b),identifier(none,c)]),typeof(none,empty_set(none),pow_subset(none,integer_set(none)))),exists(none,[identifier(none,b)],conjunct(none,member(none,identifier(none,b),integer_set(none)),forall(none,[identifier(none,x)],implication(none,conjunct(none,member(none,identifier(none,x),integer_set(none)),member(none,identifier(none,x),set_extension(none,[identifier(none,a),identifier(none,b),identifier(none,c)]))),greater_equal(none,identifier(none,b),identifier(none,x)))))),conjunct(none,greater(none,identifier(none,c),identifier(none,a)),equal(none,max(none,interval(none,identifier(none,a),identifier(none,c))),identifier(none,c))),implication(none,greater(none,identifier(none,c),identifier(none,a)),conjunct(none,not_equal(none,interval(none,identifier(none,a),identifier(none,c)),typeof(none,empty_set(none),pow_subset(none,integer_set(none)))),exists(none,[identifier(none,b)],conjunct(none,member(none,identifier(none,b),integer_set(none)),forall(none,[identifier(none,x)],implication(none,conjunct(none,member(none,identifier(none,x),integer_set(none)),member(none,identifier(none,x),interval(none,identifier(none,a),identifier(none,c)))),greater_equal(none,identifier(none,b),identifier(none,x)))))))),member(none,identifier(none,g),total_function(none,interval(none,identifier(none,a),identifier(none,c)),natural1_set(none))),equal(none,function(none,identifier(none,g),[identifier(none,a)]),function(none,identifier(none,g),[identifier(none,c)])),member(none,identifier(none,a),domain(none,identifier(none,g))),member(none,identifier(none,g),partial_function(none,integer_set(none),integer_set(none))),member(none,identifier(none,c),domain(none,identifier(none,g))),equal(none,card(none,set_extension(none,[identifier(none,a),identifier(none,b),identifier(none,c)])),integer(none,3)),finite(none,set_extension(none,[identifier(none,a),identifier(none,b),identifier(none,c)])),greater(none,card(none,interval(none,identifier(none,a),identifier(none,c))),integer(none,1)),finite(none,interval(none,identifier(none,a),identifier(none,c))),subset(none,identifier(none,s),set_extension(none,[identifier(none,a),identifier(none,b),identifier(none,c)])),equal(none,card(none,identifier(none,s)),integer(none,3)),finite(none,identifier(none,s))]),constants(none,[identifier(none,a),identifier(none,b),identifier(none,c),identifier(none,s),identifier(none,f),identifier(none,g)]),sets(none,[])]),conjunct(none,not_equal(none,set_extension(none,[identifier(none,a),identifier(none,b),identifier(none,c)]),typeof(none,empty_set(none),pow_subset(none,integer_set(none)))),exists(none,[identifier(none,b0)],conjunct(none,member(none,identifier(none,b0),integer_set(none)),forall(none,[identifier(none,x)],implication(none,conjunct(none,member(none,identifier(none,x),integer_set(none)),member(none,identifier(none,x),set_extension(none,[identifier(none,a),identifier(none,b),identifier(none,c)]))),less_equal(none,identifier(none,b0),identifier(none,x))))))),[member(none,identifier(none,f),total_function(none,natural1_set(none),natural1_set(none))),member(none,identifier(none,a),natural1_set(none)),member(none,identifier(none,b),natural_set(none)),equal(none,function(none,identifier(none,f),[identifier(none,a)]),identifier(none,c)),member(none,identifier(none,a),domain(none,identifier(none,f))),member(none,identifier(none,f),partial_function(none,integer_set(none),integer_set(none))),equal(none,function(none,identifier(none,f),[add(none,identifier(none,b),integer(none,1))]),identifier(none,c)),member(none,add(none,identifier(none,b),integer(none,1)),domain(none,identifier(none,f))),equal(none,div(none,integer(none,10),function(none,identifier(none,f),[identifier(none,a)])),div(none,integer(none,10),identifier(none,a))),not_equal(none,function(none,identifier(none,f),[identifier(none,a)]),integer(none,0)),not_equal(none,identifier(none,a),integer(none,0)),equal(none,div(none,integer(none,10),function(none,identifier(none,f),[add(none,identifier(none,b),integer(none,1))])),div(none,integer(none,10),add(none,identifier(none,b),integer(none,1)))),not_equal(none,function(none,identifier(none,f),[add(none,identifier(none,b),integer(none,1))]),integer(none,0)),not_equal(none,add(none,identifier(none,b),integer(none,1)),integer(none,0)),equal(none,max(none,set_extension(none,[identifier(none,a),identifier(none,b),identifier(none,c)])),identifier(none,c)),not_equal(none,set_extension(none,[identifier(none,a),identifier(none,b),identifier(none,c)]),typeof(none,empty_set(none),pow_subset(none,integer_set(none)))),exists(none,[identifier(none,b)],conjunct(none,member(none,identifier(none,b),integer_set(none)),forall(none,[identifier(none,x)],implication(none,conjunct(none,member(none,identifier(none,x),integer_set(none)),member(none,identifier(none,x),set_extension(none,[identifier(none,a),identifier(none,b),identifier(none,c)]))),greater_equal(none,identifier(none,b),identifier(none,x)))))),conjunct(none,greater(none,identifier(none,c),identifier(none,a)),equal(none,max(none,interval(none,identifier(none,a),identifier(none,c))),identifier(none,c))),implication(none,greater(none,identifier(none,c),identifier(none,a)),conjunct(none,not_equal(none,interval(none,identifier(none,a),identifier(none,c)),typeof(none,empty_set(none),pow_subset(none,integer_set(none)))),exists(none,[identifier(none,b)],conjunct(none,member(none,identifier(none,b),integer_set(none)),forall(none,[identifier(none,x)],implication(none,conjunct(none,member(none,identifier(none,x),integer_set(none)),member(none,identifier(none,x),interval(none,identifier(none,a),identifier(none,c)))),greater_equal(none,identifier(none,b),identifier(none,x)))))))),member(none,identifier(none,g),total_function(none,interval(none,identifier(none,a),identifier(none,c)),natural1_set(none))),equal(none,function(none,identifier(none,g),[identifier(none,a)]),function(none,identifier(none,g),[identifier(none,c)])),member(none,identifier(none,a),domain(none,identifier(none,g))),member(none,identifier(none,g),partial_function(none,integer_set(none),integer_set(none))),member(none,identifier(none,c),domain(none,identifier(none,g))),equal(none,card(none,set_extension(none,[identifier(none,a),identifier(none,b),identifier(none,c)])),integer(none,3)),finite(none,set_extension(none,[identifier(none,a),identifier(none,b),identifier(none,c)])),greater(none,card(none,interval(none,identifier(none,a),identifier(none,c))),integer(none,1)),finite(none,interval(none,identifier(none,a),identifier(none,c))),subset(none,identifier(none,s),set_extension(none,[identifier(none,a),identifier(none,b),identifier(none,c)])),equal(none,card(none,identifier(none,s)),integer(none,3)),finite(none,identifier(none,s))],[member(none,identifier(none,f),total_function(none,natural1_set(none),natural1_set(none))),member(none,identifier(none,a),natural1_set(none)),member(none,identifier(none,b),natural_set(none)),equal(none,function(none,identifier(none,f),[identifier(none,a)]),identifier(none,c)),equal(none,function(none,identifier(none,f),[add(none,identifier(none,b),integer(none,1))]),identifier(none,c)),equal(none,div(none,integer(none,10),function(none,identifier(none,f),[identifier(none,a)])),div(none,integer(none,10),identifier(none,a))),equal(none,div(none,integer(none,10),function(none,identifier(none,f),[add(none,identifier(none,b),integer(none,1))])),div(none,integer(none,10),add(none,identifier(none,b),integer(none,1)))),equal(none,max(none,set_extension(none,[identifier(none,a),identifier(none,b),identifier(none,c)])),identifier(none,c)),conjunct(none,greater(none,identifier(none,c),identifier(none,a)),equal(none,max(none,interval(none,identifier(none,a),identifier(none,c))),identifier(none,c))),member(none,identifier(none,g),total_function(none,interval(none,identifier(none,a),identifier(none,c)),natural1_set(none))),equal(none,function(none,identifier(none,g),[identifier(none,a)]),function(none,identifier(none,g),[identifier(none,c)])),equal(none,card(none,set_extension(none,[identifier(none,a),identifier(none,b),identifier(none,c)])),integer(none,3)),greater(none,card(none,interval(none,identifier(none,a),identifier(none,c))),integer(none,1)),subset(none,identifier(none,s),set_extension(none,[identifier(none,a),identifier(none,b),identifier(none,c)])),equal(none,card(none,identifier(none,s)),integer(none,3))],true).
15