Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
----- Otter 3.0.4, August 1995 ----- The job was started by wos on eagle.mcs.anl.gov, Mon Oct 16 16:55:52 1995 The command was "otter304". %%%%%%%%%%%%%%%%%%%%% Basic options op(400, xfx, [*,+,^,v,/,\,#]). % infix operators op(300,yf,@). % postfix operator clear(print_kept). % Do not enter into the output file clauses as they are retained. clear(print_new_demod). clear(print_back_demod). assign(pick_given_ratio, 4). % Twelve clauses are chosen by weight and one by breadth first, repeatedly. assign(max_mem, 20000). % Limit the memory usage in kilobytes. %%%%%%%%%%%%%%%%%%%%% Standard for equational problems set(knuth_bendix). dependent: set(para_from). % Paramodulate from the chosen clause. dependent: set(para_into). % Paramodulate into the chosen clause. dependent: clear(para_from_right). dependent: clear(para_into_right). dependent: set(para_from_vars). dependent: set(eq_units_both_ways). dependent: set(dynamic_demod_all). dependent: set(dynamic_demod). % Adjoin demodulators during the run. dependent: set(order_eq). % Flip arguments if righthand heavier than lefthand. dependent: set(back_demod). % Apply new demodulators to retained clauses. dependent: set(process_input). % Treat input clauses as if they were generated by applying an inference rule. dependent: set(lrpo). % Activate the LRPO ordering for orienting equalities and deciding dynamic demodulators. set(build_proof_object). dependent: set(order_history). %%%%%%%%%%%%%%%%%%%%% Modifications to strategy assign(max_weight,15). % Disallow clauses with weight strictly greater than value. WARNING: assign(heat,1) already has that value. assign(heat,1). % Used to direct the reasoning and to purge unwanted clauses. weight_list(pick_and_purge). % Followinng are positive steps from temp.wos.qlt0.out1 weight(x^ (y^z)=y^ (x^z),2). weight(x^ (y^x)=y^x,2). weight(x v (y v z)=y v (x v z),2). weight(x v (y v x)=y v x,2). weight((x^ (y v z)) v (x^z)=x^ (y v z),2). weight((x^ ((y^x) v z)) v (y^x)=x^ ((y^x) v z),2). weight((x v (y^z))^ (x v z)=x v (y^z),2). weight(x v (y^z)=x v (z^y),2). weight((x v (y^z))^y=y^ (x v z),2). weight((x^y) v z=z v (y^x),2). weight(x v (y^z)= (z^y) v x,2). weight(x^ ((y^x) v z)=x^ (z v y),2). weight(x v ((y^z) v (y^ (x v z)))=x v (y^z),2). weight((x^y) v (x^ (z v y))=x^ (z v y),2). weight(x v (y^ (x v z))=x v (y^z),2). weight((x^y) v (y^z)=y^ ((x^y) v z),2). end_of_list. %%%%%%%%%%%%%%%%%%%%% Clauses list(usable). 0 [] x=x. end_of_list. list(sos). 0 [] x^x=x. 0 [] x^y=y^x. 0 [] (x^y)^z=x^ (y^z). 0 [] x v x=x. 0 [] x v y=y v x. 0 [] (x v y) v z=x v (y v z). 0 [] (x^ (y v z)) v (x^y)=x^ (y v z). 0 [] (x v (y^z))^ (x v y)=x v (y^z). 0 [] x^ (y v (x^z))=x^ (y v z). 0 [] A^ (B v C)!= (A^B) v (A^C). end_of_list. list(passive). end_of_list. list(hot). 1 [] x^x=x. 2 [] x v x=x. end_of_list.