%------------------------------------------------------------------------------ % File : Otter---3.3 % Problem : KLE044+2 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : otter-tptp-script %s % Computer : n011.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 : 300s % DateTime : Wed Jul 27 13:00:36 EDT 2022 % Result : Timeout 299.87s 300.02s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.11 % Problem : KLE044+2 : TPTP v8.1.0. Released v4.0.0. % 0.03/0.12 % Command : otter-tptp-script %s % 0.13/0.33 % Computer : n011.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 300 % 0.13/0.33 % DateTime : Wed Jul 27 06:29:55 EDT 2022 % 0.13/0.33 % CPUTime : % 1.95/2.13 ----- Otter 3.3f, August 2004 ----- % 1.95/2.13 The process was started by sandbox2 on n011.cluster.edu, % 1.95/2.13 Wed Jul 27 06:29:55 2022 % 1.95/2.13 The command was "./otter". The process ID is 23068. % 1.95/2.13 % 1.95/2.13 set(prolog_style_variables). % 1.95/2.13 set(auto). % 1.95/2.13 dependent: set(auto1). % 1.95/2.13 dependent: set(process_input). % 1.95/2.13 dependent: clear(print_kept). % 1.95/2.13 dependent: clear(print_new_demod). % 1.95/2.13 dependent: clear(print_back_demod). % 1.95/2.13 dependent: clear(print_back_sub). % 1.95/2.13 dependent: set(control_memory). % 1.95/2.13 dependent: assign(max_mem, 12000). % 1.95/2.13 dependent: assign(pick_given_ratio, 4). % 1.95/2.13 dependent: assign(stats_level, 1). % 1.95/2.13 dependent: assign(max_seconds, 10800). % 1.95/2.13 clear(print_given). % 1.95/2.13 % 1.95/2.13 formula_list(usable). % 1.95/2.13 all A (A=A). % 1.95/2.13 all A B (addition(A,B)=addition(B,A)). % 1.95/2.13 all C B A (addition(A,addition(B,C))=addition(addition(A,B),C)). % 1.95/2.13 all A (addition(A,zero)=A). % 1.95/2.13 all A (addition(A,A)=A). % 1.95/2.13 all A B C (multiplication(A,multiplication(B,C))=multiplication(multiplication(A,B),C)). % 1.95/2.13 all A (multiplication(A,one)=A). % 1.95/2.13 all A (multiplication(one,A)=A). % 1.95/2.13 all A B C (multiplication(A,addition(B,C))=addition(multiplication(A,B),multiplication(A,C))). % 1.95/2.13 all A B C (multiplication(addition(A,B),C)=addition(multiplication(A,C),multiplication(B,C))). % 1.95/2.13 all A (multiplication(A,zero)=zero). % 1.95/2.13 all A (multiplication(zero,A)=zero). % 1.95/2.13 all A B (le_q(A,B)<->addition(A,B)=B). % 1.95/2.13 all A le_q(addition(one,multiplication(A,star(A))),star(A)). % 1.95/2.13 all A le_q(addition(one,multiplication(star(A),A)),star(A)). % 1.95/2.13 all A B C (le_q(addition(multiplication(A,B),C),B)->le_q(multiplication(star(A),C),B)). % 1.95/2.13 all A B C (le_q(addition(multiplication(A,B),C),A)->le_q(multiplication(C,star(B)),A)). % 1.95/2.13 -(all X0 (le_q(star(addition(one,X0)),star(X0))&le_q(star(X0),star(addition(one,X0))))). % 1.95/2.13 end_of_list. % 1.95/2.13 % 1.95/2.13 -------> usable clausifies to: % 1.95/2.13 % 1.95/2.13 list(usable). % 1.95/2.13 0 [] A=A. % 1.95/2.13 0 [] addition(A,B)=addition(B,A). % 1.95/2.13 0 [] addition(A,addition(B,C))=addition(addition(A,B),C). % 1.95/2.13 0 [] addition(A,zero)=A. % 1.95/2.13 0 [] addition(A,A)=A. % 1.95/2.13 0 [] multiplication(A,multiplication(B,C))=multiplication(multiplication(A,B),C). % 1.95/2.13 0 [] multiplication(A,one)=A. % 1.95/2.13 0 [] multiplication(one,A)=A. % 1.95/2.13 0 [] multiplication(A,addition(B,C))=addition(multiplication(A,B),multiplication(A,C)). % 1.95/2.13 0 [] multiplication(addition(A,B),C)=addition(multiplication(A,C),multiplication(B,C)). % 1.95/2.13 0 [] multiplication(A,zero)=zero. % 1.95/2.13 0 [] multiplication(zero,A)=zero. % 1.95/2.13 0 [] -le_q(A,B)|addition(A,B)=B. % 1.95/2.13 0 [] le_q(A,B)|addition(A,B)!=B. % 1.95/2.13 0 [] le_q(addition(one,multiplication(A,star(A))),star(A)). % 1.95/2.13 0 [] le_q(addition(one,multiplication(star(A),A)),star(A)). % 1.95/2.13 0 [] -le_q(addition(multiplication(A,B),C),B)|le_q(multiplication(star(A),C),B). % 1.95/2.13 0 [] -le_q(addition(multiplication(A,B),C),A)|le_q(multiplication(C,star(B)),A). % 1.95/2.13 0 [] -le_q(star(addition(one,$c1)),star($c1))| -le_q(star($c1),star(addition(one,$c1))). % 1.95/2.13 end_of_list. % 1.95/2.13 % 1.95/2.13 SCAN INPUT: prop=0, horn=1, equality=1, symmetry=0, max_lits=2. % 1.95/2.13 % 1.95/2.13 This is a Horn set with equality. The strategy will be % 1.95/2.13 Knuth-Bendix and hyper_res, with positive clauses in % 1.95/2.13 sos and nonpositive clauses in usable. % 1.95/2.13 % 1.95/2.13 dependent: set(knuth_bendix). % 1.95/2.13 dependent: set(anl_eq). % 1.95/2.13 dependent: set(para_from). % 1.95/2.13 dependent: set(para_into). % 1.95/2.13 dependent: clear(para_from_right). % 1.95/2.13 dependent: clear(para_into_right). % 1.95/2.13 dependent: set(para_from_vars). % 1.95/2.13 dependent: set(eq_units_both_ways). % 1.95/2.13 dependent: set(dynamic_demod_all). % 1.95/2.13 dependent: set(dynamic_demod). % 1.95/2.13 dependent: set(order_eq). % 1.95/2.13 dependent: set(back_demod). % 1.95/2.13 dependent: set(lrpo). % 1.95/2.13 dependent: set(hyper_res). % 1.95/2.13 dependent: clear(order_hyper). % 1.95/2.13 % 1.95/2.13 ------------> process usable: % 1.95/2.13 ** KEPT (pick-wt=8): 1 [] -le_q(A,B)|addition(A,B)=B. % 1.95/2.13 ** KEPT (pick-wt=8): 2 [] le_q(A,B)|addition(A,B)!=B. % 1.95/2.13 ** KEPT (pick-wt=13): 3 [] -le_q(addition(multiplication(A,B),C),B)|le_q(multiplication(star(A),C),B). % 1.95/2.13 ** KEPT (pick-wt=13): 4 [] -le_q(addition(multiplication(A,B),C),A)|le_q(multiplication(C,star(B)),A). % 1.95/2.13 ** KEPT (pick-wt=14): 5 [] -le_q(star(addition(one,$c1)),star($c1))| -le_q(star($c1),star(addition(one,$c1))). % 1.95/2.13 % 1.95/2.13 ------------> process sos: % 1.95/2.13 ** KEPT (pick-wt=3): 6 [] A=A. % 1.95/2.13 ** KEPT (pick-wt=7): 7 [] addition(A,B)=addition(B,A). % 1.95/2.13 ** KEPT (pick-wt=11): 9 [copy,8,flip.1] addition(addition(A,B),C)=addition(A,addition(B,C)). % 1.95/2.13 ---> New Alarm clock % 299.87/300.02 Otter interrupted % 299.87/300.02 PROOF NOT FOUND %------------------------------------------------------------------------------