%------------------------------------------------------------------------------ % File : EQP---0.9e % Problem : NUM026-10 : TPTP v8.1.0. Released v7.3.0. % Transfm : none % Format : tptp:raw % Command : tptp2X_and_run_eqp %s % Computer : n021.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 : 600s % DateTime : Mon Jul 18 08:50:23 EDT 2022 % Result : Unknown 54.55s 54.98s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.12 % Problem : NUM026-10 : TPTP v8.1.0. Released v7.3.0. % 0.12/0.12 % Command : tptp2X_and_run_eqp %s % 0.12/0.33 % Computer : n021.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Wed Jul 6 21:41:34 EDT 2022 % 0.12/0.34 % CPUTime : % 54.55/54.98 ----- EQP 0.9e, May 2009 ----- % 54.55/54.98 The job began on n021.cluster.edu, Wed Jul 6 21:41:34 2022 % 54.55/54.98 The command was "./eqp09e". % 54.55/54.98 % 54.55/54.98 set(prolog_style_variables). % 54.55/54.98 set(lrpo). % 54.55/54.98 set(basic_paramod). % 54.55/54.98 set(functional_subsume). % 54.55/54.98 set(ordered_paramod). % 54.55/54.98 set(prime_paramod). % 54.55/54.98 set(para_pairs). % 54.55/54.98 assign(pick_given_ratio,4). % 54.55/54.98 clear(print_kept). % 54.55/54.98 clear(print_new_demod). % 54.55/54.98 clear(print_back_demod). % 54.55/54.98 clear(print_given). % 54.55/54.98 assign(max_mem,64000). % 54.55/54.98 end_of_commands. % 54.55/54.98 % 54.55/54.98 Usable: % 54.55/54.98 end_of_list. % 54.55/54.98 % 54.55/54.98 Sos: % 54.55/54.98 0 (wt=-1) [] ifeq2(A,A,B,C) = B. % 54.55/54.98 0 (wt=-1) [] ifeq(A,A,B,C) = B. % 54.55/54.98 0 (wt=-1) [] equalish(add(A,n0),A) = true. % 54.55/54.98 0 (wt=-1) [] equalish(add(A,successor(B)),successor(add(A,B))) = true. % 54.55/54.98 0 (wt=-1) [] equalish(multiply(A,n0),n0) = true. % 54.55/54.98 0 (wt=-1) [] equalish(multiply(A,successor(B)),add(multiply(A,B),A)) = true. % 54.55/54.98 0 (wt=-1) [] ifeq2(equalish(successor(A),successor(B)),true,equalish(A,B),true) = true. % 54.55/54.98 0 (wt=-1) [] ifeq2(equalish(A,B),true,equalish(successor(A),successor(B)),true) = true. % 54.55/54.98 0 (wt=-1) [] ifeq2(less(A,B),true,ifeq2(less(B,C),true,less(A,C),true),true) = true. % 54.55/54.98 0 (wt=-1) [] ifeq2(equalish(add(successor(A),B),C),true,less(B,C),true) = true. % 54.55/54.98 0 (wt=-1) [] ifeq2(less(A,B),true,equalish(add(successor(predecessor_of_1st_minus_2nd(B,A)),A),B),true) = true. % 54.55/54.98 0 (wt=-1) [] equalish(A,A) = true. % 54.55/54.98 0 (wt=-1) [] ifeq2(equalish(A,B),true,equalish(B,A),true) = true. % 54.55/54.98 0 (wt=-1) [] ifeq2(equalish(A,B),true,ifeq2(equalish(C,A),true,equalish(C,B),true),true) = true. % 54.55/54.98 0 (wt=-1) [] less(a,b) = true. % 54.55/54.98 0 (wt=-1) [] ifeq(equalish(successor(A),n0),true,a2,b2) = b2. % 54.55/54.98 0 (wt=-1) [] ifeq(less(A,A),true,a2,b2) = b2. % 54.55/54.98 0 (wt=-1) [] ifeq(equalish(c,n0),true,a2,b2) = b2. % 54.55/54.98 0 (wt=-1) [] ifeq(less(multiply(a,c),multiply(b,c)),true,a2,b2) = b2. % 54.55/54.98 0 (wt=-1) [] -(a2 = b2). % 54.55/54.98 end_of_list. % 54.55/54.98 % 54.55/54.98 Demodulators: % 54.55/54.98 end_of_list. % 54.55/54.98 % 54.55/54.98 Passive: % 54.55/54.98 end_of_list. % 54.55/54.98 % 54.55/54.98 Starting to process input. % 54.55/54.98 % 54.55/54.98 ** KEPT: 1 (wt=7) [] ifeq2(A,A,B,C) = B. % 54.55/54.98 1 is a new demodulator. % 54.55/54.98 % 54.55/54.98 ** KEPT: 2 (wt=7) [] ifeq(A,A,B,C) = B. % 54.55/54.98 2 is a new demodulator. % 54.55/54.98 % 54.55/54.98 ** KEPT: 3 (wt=7) [] equalish(add(A,n0),A) = true. % 54.55/54.98 3 is a new demodulator. % 54.55/54.98 % 54.55/54.98 ** KEPT: 4 (wt=11) [] equalish(add(A,successor(B)),successor(add(A,B))) = true. % 54.55/54.98 4 is a new demodulator. % 54.55/54.98 % 54.55/54.98 ** KEPT: 5 (wt=7) [] equalish(multiply(A,n0),n0) = true. % 54.55/54.98 5 is a new demodulator. % 54.55/54.98 % 54.55/54.98 ** KEPT: 6 (wt=12) [] equalish(multiply(A,successor(B)),add(multiply(A,B),A)) = true. % 54.55/54.98 6 is a new demodulator. % 54.55/54.98 % 54.55/54.98 ** KEPT: 7 (wt=13) [] ifeq2(equalish(successor(A),successor(B)),true,equalish(A,B),true) = true. % 54.55/54.98 7 is a new demodulator. % 54.55/54.98 % 54.55/54.98 ** KEPT: 8 (wt=13) [] ifeq2(equalish(A,B),true,equalish(successor(A),successor(B)),true) = true. % 54.55/54.98 8 is a new demodulator. % 54.55/54.98 % 54.55/54.98 ** KEPT: 9 (wt=17) [] ifeq2(less(A,B),true,ifeq2(less(B,C),true,less(A,C),true),true) = true. % 54.55/54.98 9 is a new demodulator. % 54.55/54.98 % 54.55/54.98 ** KEPT: 10 (wt=14) [] ifeq2(equalish(add(successor(A),B),C),true,less(B,C),true) = true. % 54.55/54.98 10 is a new demodulator. % 54.55/54.98 % 54.55/54.98 ** KEPT: 11 (wt=16) [] ifeq2(less(A,B),true,equalish(add(successor(predecessor_of_1st_minus_2nd(B,A)),A),B),true) = true. % 54.55/54.98 11 is a new demodulator. % 54.55/54.98 % 54.55/54.98 ** KEPT: 12 (wt=5) [] equalish(A,A) = true. % 54.55/54.98 12 is a new demodulator. % 54.55/54.98 % 54.55/54.98 ** KEPT: 13 (wt=11) [] ifeq2(equalish(A,B),true,equalish(B,A),true) = true. % 54.55/54.98 13 is a new demodulator. % 54.55/54.98 % 54.55/54.98 ** KEPT: 14 (wt=17) [] ifeq2(equalish(A,B),true,ifeq2(equalish(C,A),true,equalish(C,B),true),true) = true. % 54.55/54.98 14 is a new demodulator. % 54.55/54.98 % 54.55/54.98 ** KEPT: 15 (wt=5) [] less(a,b) = true. % 54.55/54.98 15 is a new demodulator. % 54.55/54.98 % 54.55/54.98 ** KEPT: 16 (wt=10) [] ifeq(equalish(successor(A),n0),true,a2,b2) = b2. % 54.55/54.98 16 is a new demodulator. % 54.55/54.98 % 54.55/54.98 ** KEPT: 17 (wt=9) [] ifeq(less(A,A),true,a2,b2) = b2. % 54.55/54.98 17 is a new demodulator. % 54.55/54.98 % 54.55/54.98 ** KEPT: 18 (wt=9) [] ifeq(equalish(c,n0),true,a2,b2) = b2. % 54.55/54.98 18 is a new demodulator. % 54.55/54.98 % 54.55/54.98 ** KEPT: 19 (wt=13) [] ifeq(less(multiply(a,c),multiply(b,c)),true,a2,b2) = b2. % 54.55/54.98 19 is a new demodulator. % 54.55/54.98 % 54.55/54.98 ** KEPT: 20 (wt=3) [flip(1)] -(b2 = a2). % 54.55/54.98 % 54.55/54.98 After processing input: % 54.55/54.98 % 54.55/54.98 Usable: % 54.55/54.98 end_of_list. % 54.55/54.98 % 54.55/54.98 Sos: % 54.55/54.98 20 (wt=3) [flip(1)] -(b2 = a2). % 54.55/54.98 12 (wt=5) [] equalish(A,A) = true. % 54.55/54.98 15 (wt=5) [] less(a,b) = true. % 54.55/54.98 1 (wt=7) [] ifeq2(A,A,B,C) = B. % 54.55/54.98 2 (wt=7) [] ifeq(A,A,B,C) = B. % 54.55/54.98 3 (wt=7) [] equalish(add(A,n0),A) = true. % 54.55/54.98 5 (wt=7) [] equalish(multiply(A,n0),n0) = true. % 54.55/54.98 17 (wt=9) [] ifeq(less(A,A),true,a2,b2) = b2. % 54.55/54.98 18 (wt=9) [] ifeq(equalish(c,n0),true,a2,b2) = b2. % 54.55/54.98 16 (wt=10) [] ifeq(equalish(successor(A),n0),true,a2,b2) = b2. % 54.55/54.98 4 (wt=11) [] equalish(add(A,successor(B)),successor(add(A,B))) = true. % 54.55/54.98 13 (wt=11) [] ifeq2(equalish(A,B),true,equalish(B,A),true) = true. % 54.55/54.98 6 (wt=12) [] equalish(multiply(A,successor(B)),add(multiply(A,B),A)) = true. % 54.55/54.98 7 (wt=13) [] ifeq2(equalish(successor(A),successor(B)),true,equalish(A,B),true) = true. % 54.55/54.98 8 (wt=13) [] ifeq2(equalish(A,B),true,equalish(successor(A),successor(B)),true) = true. % 54.55/54.98 19 (wt=13) [] ifeq(less(multiply(a,c),multiply(b,c)),true,a2,b2) = b2. % 54.55/54.98 10 (wt=14) [] ifeq2(equalish(add(successor(A),B),C),true,less(B,C),true) = true. % 54.55/54.98 11 (wt=16) [] ifeq2(less(A,B),true,equalish(add(successor(predecessor_of_1st_minus_2nd(B,A)),A),B),true) = true. % 54.55/54.98 9 (wt=17) [] ifeq2(less(A,B),true,ifeq2(less(B,C),true,less(A,C),true),true) = true. % 54.55/54.98 14 (wt=17) [] ifeq2(equalish(A,B),true,ifeq2(equalish(C,A),true,equalish(C,B),true),true) = true. % 54.55/54.98 end_of_list. % 54.55/54.98 % 54.55/54.98 Demodulators: % 54.55/54.98 1 (wt=7) [] ifeq2(A,A,B,C) = B. % 54.55/54.98 2 (wt=7) [] ifeq(A,A,B,C) = B. % 54.55/54.98 3 (wt=7) [] equalish(add(A,n0),A) = true. % 54.55/54.98 4 (wt=11) [] equalish(add(A,successor(B)),successor(add(A,B))) = true. % 54.55/54.98 5 (wt=7) [] equalish(multiply(A,n0),n0) = true. % 54.55/54.98 6 (wt=12) [] equalish(multiply(A,successor(B)),add(multiply(A,B),A)) = true. % 54.55/54.98 7 (wt=13) [] ifeq2(equalish(successor(A),successor(B)),true,equalish(A,B),true) = true. % 54.55/54.98 8 (wt=13) [] ifeq2(equalish(A,B),true,equalish(successor(A),successor(B)),true) = true. % 54.55/54.98 9 (wt=17) [] ifeq2(less(A,B),true,ifeq2(less(B,C),true,less(A,C),true),true) = true. % 54.55/54.98 10 (wt=14) [] ifeq2(equalish(add(successor(A),B),C),true,less(B,C),true) = true. % 54.55/54.98 11 (wt=16) [] ifeq2(less(A,B),true,equalish(add(successor(predecessor_of_1st_minus_2nd(B,A)),A),B),true) = true. % 54.55/54.98 12 (wt=5) [] equalish(A,A) = true. % 54.55/54.98 13 (wt=11) [] ifeq2(equalish(A,B),true,equalish(B,A),true) = true. % 54.55/54.98 14 (wt=17) [] ifeq2(equalish(A,B),true,ifeq2(equalish(C,A),true,equalish(C,B),true),true) = true. % 54.55/54.98 15 (wt=5) [] less(a,b) = true. % 54.55/54.98 16 (wt=10) [] ifeq(equalish(successor(A),n0),true,a2,b2) = b2. % 54.55/54.98 17 (wt=9) [] ifeq(less(A,A),true,a2,b2) = b2. % 54.55/54.98 18 (wt=9) [] ifeq(equalish(c,n0),true,a2,b2) = b2. % 54.55/54.98 19 (wt=13) [] ifeq(less(multiply(a,c),multiply(b,c)),true,a2,b2) = b2. % 54.55/54.98 end_of_list. % 54.55/54.98 % 54.55/54.98 Passive: % 54.55/54.98 end_of_list. % 54.55/54.98 % 54.55/54.98 ------------- memory usage ------------ % 54.55/54.98 Memory dynamically allocated (tp_alloc): 63964. % 54.55/54.98 type (bytes each) gets frees in use avail bytes % 54.55/54.98 sym_ent ( 96) 69 0 69 0 6.5 K % 54.55/54.98 term ( 16) 9765754 8969417 796337 27 15396.4 K % 54.55/54.98 gen_ptr ( 8) 5984494 1791387 4193107 0 32758.6 K % 54.55/54.98 context ( 808) 296079453 296079450 3 1 3.2 K % 54.55/54.98 trail ( 12) 62424 62424 0 6 0.1 K % 54.55/54.98 bt_node ( 68) 161797536 161797533 3 25 1.9 K % 54.55/54.98 ac_position (285432) 0 0 0 0 0.0 K % 54.55/54.98 ac_match_pos (14044) 0 0 0 0 0.0 K % 54.55/54.98 ac_match_free_vars_pos (4020) % 54.55/54.98 0 0 0 0 0.0 K % 54.55/54.98 discrim ( 12) 694123 169401 524722 0 6149.1 K % 54.55/54.98 flat ( 40) 13118503 13118503 0 36 1.4 K % 54.55/54.98 discrim_pos ( 12) 470998 470998 0 1 0.0 K % 54.55/54.98 fpa_head ( 12) 58829 0 58829 0 689.4 K % 54.55/54.98 fpa_tree ( 28) 475408 475407 1 30 0.8 K % 54.55/54.98 fpa_pos ( 36) 80657 80656 1 0 0.0 K % 54.55/54.98 literal ( 12) 294918 254589 40329 1 472.6 K % 54.55/54.98 clause ( 24) 294918 254589 40329 1 945.2 K % 54.55/54.98 list ( 12) % 54.55/54.98 % 54.55/54.98 ********** ABNORMAL END ********** % 54.55/54.98 ********** in tp_alloc, max_mem parameter exceeded. % 54.55/54.98 40387 40330 57 2 0.7 K % 54.55/54.98 list_pos ( 20) 174609 33205 141404 0 2761.8 K % 54.55/54.98 pair_index ( 40) 2 0 2 0 0.1 K % 54.55/54.98 % 54.55/54.98 -------------- statistics ------------- % 54.55/54.98 Clauses input 20 % 54.55/54.98 Usable input 0 % 54.55/54.98 Sos input 20 % 54.55/54.98 Demodulators input 0 % 54.55/54.98 Passive input 0 % 54.55/54.98 % 54.55/54.98 Processed BS (before search) 20 % 54.55/54.98 Forward subsumed BS 0 % 54.55/54.98 Kept BS 20 % 54.55/54.98 New demodulators BS 19 % 54.55/54.98 Back demodulated BS 0 % 54.55/54.98 % 54.55/54.98 Clauses or pairs given 7593395 % 54.55/54.98 Clauses generated 254570 % 54.55/54.98 Forward subsumed 214261 % 54.55/54.98 Deleted by weight 0 % 54.55/54.98 Deleted by variable count 0 % 54.55/54.98 Kept 40309 % 54.55/54.98 New demodulators 40309 % 54.55/54.98 Back demodulated 6637 % 54.55/54.98 Ordered paramod prunes 0 % 54.55/54.98 Basic paramod prunes 6194217 % 54.55/54.98 Prime paramod prunes 0 % 54.55/54.98 Semantic prunes 0 % 54.55/54.98 % 54.55/54.98 Rewrite attmepts 5104165 % 54.55/54.98 Rewrites 470998 % 54.55/54.98 % 54.55/54.98 FPA overloads 0 % 54.55/54.98 FPA underloads 0 % 54.55/54.98 % 54.55/54.98 Usable size 0 % 54.55/54.98 Sos size 33692 % 54.55/54.98 Demodulators size 33691 % 54.55/54.98 Passive size 0 % 54.55/54.98 Disabled size 6637 % 54.55/54.98 % 54.55/54.98 Proofs found 0 % 54.55/54.98 % 54.55/54.98 ----------- times (seconds) ----------- Wed Jul 6 21:42:28 2022 % 54.55/54.98 % 54.55/54.98 user CPU time 32.07 (0 hr, 0 min, 32 sec) % 54.55/54.98 system CPU time 21.80 (0 hr, 0 min, 21 sec) % 54.55/54.98 wall-clock time 54 (0 hr, 0 min, 54 sec) % 54.55/54.98 input time 0.00 % 54.55/54.98 paramodulation time 10.47 % 54.55/54.98 demodulation time 0.51 % 54.55/54.98 orient time 0.39 % 54.55/54.98 weigh time 0.09 % 54.55/54.98 forward subsume time 0.13 % 54.55/54.98 back demod find time 3.24 % 54.55/54.98 conflict time 0.03 % 54.55/54.98 LRPO time 0.13 % 54.55/54.98 store clause time 7.58 % 54.55/54.98 disable clause time 2.04 % 54.55/54.98 prime paramod time 0.28 % 54.55/54.98 semantics time 0.00 % 54.55/54.98 % 54.55/54.98 EQP interrupted %------------------------------------------------------------------------------