↑ Up

EQP---0.9e.UNK-Non.f

View TPTP
Problem
Process solution in
SystemOnTSTP
Download .tgz
%------------------------------------------------------------------------------
% File     : EQP---0.9e
% Problem  : SWX203-1 : TPTP v9.3.0. Released v9.3.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : tptp2X_and_run_eqp %s

% Computer : n018.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 : Tue May  5 07:00:09 PM UTC 2026

% Result   : Unknown 11.94s 12.33s
% Output   : None 
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12  % Problem  : SWX203-1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.13  % Command  : tptp2X_and_run_eqp %s
% 0.18/0.34  % Computer : n018.cluster.edu
% 0.18/0.34  % Model    : x86_64 x86_64
% 0.18/0.34  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.34  % Memory   : 8042.1875MB
% 0.18/0.34  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.18/0.34  % CPULimit : 300
% 0.18/0.34  % WCLimit  : 300
% 0.18/0.34  % DateTime : Tue May  5 11:26:16 EDT 2026
% 0.18/0.34  % CPUTime  : 
% 0.72/1.10  ----- EQP 0.9e, May 2009 -----
% 0.72/1.10  The job began on n018.cluster.edu, Tue May  5 11:26:17 2026
% 0.72/1.10  The command was "./eqp09e".
% 0.72/1.10  
% 0.72/1.10  set(prolog_style_variables).
% 0.72/1.10  set(lrpo).
% 0.72/1.10  set(basic_paramod).
% 0.72/1.10  set(functional_subsume).
% 0.72/1.10  set(ordered_paramod).
% 0.72/1.10  set(prime_paramod).
% 0.72/1.10  set(para_pairs).
% 0.72/1.10  assign(pick_given_ratio,4).
% 0.72/1.10  clear(print_kept).
% 0.72/1.10  clear(print_new_demod).
% 0.72/1.10  clear(print_back_demod).
% 0.72/1.10  clear(print_given).
% 0.72/1.10  assign(max_mem,64000).
% 0.72/1.10  end_of_commands.
% 0.72/1.10  
% 0.72/1.10  Usable:
% 0.72/1.10  end_of_list.
% 0.72/1.10  
% 0.72/1.10  Sos:
% 0.72/1.10  0 (wt=-1) [] aux(A,B,btrue) = bfalse.
% 0.72/1.10  0 (wt=-1) [] aux(A,B,bfalse) = unique(B).
% 0.72/1.10  0 (wt=-1) [] orb(btrue,A) = btrue.
% 0.72/1.10  0 (wt=-1) [] orb(bfalse,A) = A.
% 0.72/1.10  0 (wt=-1) [] leqNat(z,A) = btrue.
% 0.72/1.10  0 (wt=-1) [] leqNat(s(A),z) = bfalse.
% 0.72/1.10  0 (wt=-1) [] leqNat(s(A),s(B)) = leqNat(A,B).
% 0.72/1.10  0 (wt=-1) [] lengthNat(nil) = z.
% 0.72/1.10  0 (wt=-1) [] lengthNat(cons(A,B)) = s(lengthNat(B)).
% 0.72/1.10  0 (wt=-1) [] impl(btrue,A) = A.
% 0.72/1.10  0 (wt=-1) [] impl(bfalse,A) = btrue.
% 0.72/1.10  0 (wt=-1) [] elemNat(A,nil) = bfalse.
% 0.72/1.10  0 (wt=-1) [] elemNat(A,cons(B,C)) = orb(eq(A,B),elemNat(A,C)).
% 0.72/1.10  0 (wt=-1) [] unique(nil) = btrue.
% 0.72/1.10  0 (wt=-1) [] unique(cons(A,B)) = aux(A,B,elemNat(A,B)).
% 0.72/1.10  0 (wt=-1) [] append(nil,A) = A.
% 0.72/1.10  0 (wt=-1) [] append(cons(A,B),C) = cons(A,append(B,C)).
% 0.72/1.10  0 (wt=-1) [] rev(nil) = nil.
% 0.72/1.10  0 (wt=-1) [] rev(cons(A,B)) = append(rev(B),cons(A,nil)).
% 0.72/1.10  0 (wt=-1) [] andb(btrue,A) = A.
% 0.72/1.10  0 (wt=-1) [] andb(bfalse,A) = bfalse.
% 0.72/1.10  0 (wt=-1) [] sorted(nil) = btrue.
% 0.72/1.10  0 (wt=-1) [] sorted(cons(A,nil)) = btrue.
% 0.72/1.10  0 (wt=-1) [] sorted(cons(A,cons(B,C))) = andb(leqNat(A,B),sorted(cons(B,C))).
% 0.72/1.10  0 (wt=-1) [] psorted_rev(A) = impl(eq2(sorted(rev(A)),btrue),impl(eq2(unique(A),btrue),eq2(leqNat(lengthNat(A),s(s(s(z)))),btrue))).
% 0.72/1.10  0 (wt=-1) [] eq2(bfalse,btrue) = bfalse.
% 0.72/1.10  0 (wt=-1) [] eq2(btrue,bfalse) = bfalse.
% 0.72/1.10  0 (wt=-1) [] eq(s(A),s(B)) = eq(A,B).
% 0.72/1.10  0 (wt=-1) [] eq(z,s(A)) = bfalse.
% 0.72/1.10  0 (wt=-1) [] eq(s(A),z) = bfalse.
% 0.72/1.10  0 (wt=-1) [] eq(A,A) = btrue.
% 0.72/1.10  0 (wt=-1) [] eq2(A,A) = btrue.
% 0.72/1.10  0 (wt=-1) [] -(eq2(psorted_rev(A),bfalse) = btrue).
% 0.72/1.10  end_of_list.
% 0.72/1.10  
% 0.72/1.10  Demodulators:
% 0.72/1.10  end_of_list.
% 0.72/1.10  
% 0.72/1.10  Passive:
% 0.72/1.10  end_of_list.
% 0.72/1.10  
% 0.72/1.10  Starting to process input.
% 0.72/1.10  
% 0.72/1.10  ** KEPT: 1 (wt=6) [] aux(A,B,btrue) = bfalse.
% 0.72/1.10  1 is a new demodulator.
% 0.72/1.10  
% 0.72/1.10  ** KEPT: 2 (wt=7) [] aux(A,B,bfalse) = unique(B).
% 0.72/1.10  
% 0.72/1.10  ** KEPT: 3 (wt=7) [flip(2)] unique(A) = aux(B,A,bfalse).
% 0.72/1.10  clause forward subsumed: 0 (wt=7) [flip(3)] aux(B,A,bfalse) = unique(A).
% 0.72/1.10  
% 0.72/1.10  ** KEPT: 4 (wt=5) [] orb(btrue,A) = btrue.
% 0.72/1.10  4 is a new demodulator.
% 0.72/1.10  
% 0.72/1.10  ** KEPT: 5 (wt=5) [] orb(bfalse,A) = A.
% 0.72/1.10  5 is a new demodulator.
% 0.72/1.10  
% 0.72/1.10  ** KEPT: 6 (wt=5) [] leqNat(z,A) = btrue.
% 0.72/1.10  6 is a new demodulator.
% 0.72/1.10  
% 0.72/1.10  ** KEPT: 7 (wt=6) [] leqNat(s(A),z) = bfalse.
% 0.72/1.10  7 is a new demodulator.
% 0.72/1.10  
% 0.72/1.10  ** KEPT: 8 (wt=9) [] leqNat(s(A),s(B)) = leqNat(A,B).
% 0.72/1.10  8 is a new demodulator.
% 0.72/1.10  
% 0.72/1.10  ** KEPT: 9 (wt=4) [] lengthNat(nil) = z.
% 0.72/1.10  9 is a new demodulator.
% 0.72/1.10  
% 0.72/1.10  ** KEPT: 10 (wt=8) [] lengthNat(cons(A,B)) = s(lengthNat(B)).
% 0.72/1.10  
% 0.72/1.10  ** KEPT: 11 (wt=8) [flip(10)] s(lengthNat(A)) = lengthNat(cons(B,A)).
% 0.72/1.10  clause forward subsumed: 0 (wt=8) [flip(11)] lengthNat(cons(B,A)) = s(lengthNat(A)).
% 0.72/1.10  
% 0.72/1.10  ** KEPT: 12 (wt=5) [] impl(btrue,A) = A.
% 0.72/1.10  12 is a new demodulator.
% 0.72/1.10  
% 0.72/1.10  ** KEPT: 13 (wt=5) [] impl(bfalse,A) = btrue.
% 0.72/1.10  13 is a new demodulator.
% 0.72/1.10  
% 0.72/1.10  ** KEPT: 14 (wt=5) [] elemNat(A,nil) = bfalse.
% 0.72/1.10  14 is a new demodulator.
% 0.72/1.10  
% 0.72/1.10  ** KEPT: 15 (wt=13) [flip(1)] orb(eq(A,B),elemNat(A,C)) = elemNat(A,cons(B,C)).
% 0.72/1.10  15 is a new demodulator.
% 0.72/1.10  
% 0.72/1.10  ** KEPT: 16 (wt=4) [] unique(nil) = btrue.
% 0.72/1.10  16 is a new demodulator.
% 0.72/1.10  
% 0.72/1.10  ** KEPT: 17 (wt=11) [] unique(cons(A,B)) = aux(A,B,elemNat(A,B)).
% 0.72/1.10  17 is a new demodulator.
% 0.72/1.10  
% 0.72/1.10  ** KEPT: 18 (wt=5) [] append(nil,A) = A.
% 0.72/1.10  18 is a new demodulator.
% 0.72/1.10  
% 0.72/1.10  ** KEPT: 19 (wt=11) [flip(1)] cons(A,append(B,C)) = append(cons(A,B),C).
% 0.72/1.10  19 is a new demodulator.
% 0.72/1.10  
% 0.72/1.10  ** KEPT: 20 (wt=4) [] rev(nil) = nil.
% 0.72/1.10  20 is a new demodulator.
% 0.72/1.10  
% 0.72/1.10  ** KEPT: 21 (wt=11) [] rev(cons(A,B)) = append(rev(B),cons(A,nil)).
% 0.72/1.10  21 is a new demodulator.
% 0.72/1.10  
% 0.72/1.10  ** KEPT: 22 (wt=5) [] andb(btrue,A) = A.
% 0.72/1.10  22 is a new demodulator.
% 0.72/1.10  
% 0.72/1.10  ** KEPT: 23 (wt=5) [] andb(bfalse,A) = bfalse.
% 0.72/1.10  23 is a new demodulator.
% 0.72/1.10  
% 0.72/1.10  ** KEPT: 24 (wt=4) [] sorted(nil) = btrue.
% 0.72/1.10  24 is a new demodulator.
% 0.72/1.10  
% 0.72/1.10  ** KEPT: 25 (wt=6) [] sorted(cons(A,nil)) = btrue.
% 0.72/1.10  25 is a new demodulator.
% 0.72/1.10  
% 0.72/1.10  ** KEPT: 26 (wt=15) [] sorted(cons(A,cons(B,C))) = andb(leqNat(A,B),sorted(cons(B,C))).
% 0.72/1.10  26 is a new demodulator.
% 0.72/1.10  
% 0.72/1.10  ** KEPT: 27 (wt=23) [flip(1)] impl(eq2(sorted(rev(A)),btrue),impl(eq2(unique(A),btrue),eq2(leqNat(lengthNat(A),s(s(s(z)))),btrue))) = psorted_rev(A).
% 11.94/12.32  27 is a new demodulator.
% 11.94/12.32  
% 11.94/12.32  ** KEPT: 28 (wt=5) [] eq2(bfalse,btrue) = bfalse.
% 11.94/12.32  28 is a new demodulator.
% 11.94/12.32  
% 11.94/12.32  ** KEPT: 29 (wt=5) [] eq2(btrue,bfalse) = bfalse.
% 11.94/12.32  29 is a new demodulator.
% 11.94/12.32  
% 11.94/12.32  ** KEPT: 30 (wt=9) [] eq(s(A),s(B)) = eq(A,B).
% 11.94/12.32  30 is a new demodulator.
% 11.94/12.32  
% 11.94/12.32  ** KEPT: 31 (wt=6) [] eq(z,s(A)) = bfalse.
% 11.94/12.32  31 is a new demodulator.
% 11.94/12.32  
% 11.94/12.32  ** KEPT: 32 (wt=6) [] eq(s(A),z) = bfalse.
% 11.94/12.32  32 is a new demodulator.
% 11.94/12.32  
% 11.94/12.32  ** KEPT: 33 (wt=5) [] eq(A,A) = btrue.
% 11.94/12.32  33 is a new demodulator.
% 11.94/12.32  
% 11.94/12.32  ** KEPT: 34 (wt=5) [] eq2(A,A) = btrue.
% 11.94/12.32  34 is a new demodulator.
% 11.94/12.32  
% 11.94/12.32  ** KEPT: 35 (wt=6) [] -(eq2(psorted_rev(A),bfalse) = btrue).
% 11.94/12.32  
% 11.94/12.32  After processing input:
% 11.94/12.32  
% 11.94/12.32  Usable:
% 11.94/12.32  end_of_list.
% 11.94/12.32  
% 11.94/12.32  Sos:
% 11.94/12.32  9 (wt=4) [] lengthNat(nil) = z.
% 11.94/12.32  16 (wt=4) [] unique(nil) = btrue.
% 11.94/12.32  20 (wt=4) [] rev(nil) = nil.
% 11.94/12.32  24 (wt=4) [] sorted(nil) = btrue.
% 11.94/12.32  4 (wt=5) [] orb(btrue,A) = btrue.
% 11.94/12.32  5 (wt=5) [] orb(bfalse,A) = A.
% 11.94/12.32  6 (wt=5) [] leqNat(z,A) = btrue.
% 11.94/12.32  12 (wt=5) [] impl(btrue,A) = A.
% 11.94/12.32  13 (wt=5) [] impl(bfalse,A) = btrue.
% 11.94/12.32  14 (wt=5) [] elemNat(A,nil) = bfalse.
% 11.94/12.32  18 (wt=5) [] append(nil,A) = A.
% 11.94/12.32  22 (wt=5) [] andb(btrue,A) = A.
% 11.94/12.32  23 (wt=5) [] andb(bfalse,A) = bfalse.
% 11.94/12.32  28 (wt=5) [] eq2(bfalse,btrue) = bfalse.
% 11.94/12.32  29 (wt=5) [] eq2(btrue,bfalse) = bfalse.
% 11.94/12.32  33 (wt=5) [] eq(A,A) = btrue.
% 11.94/12.32  34 (wt=5) [] eq2(A,A) = btrue.
% 11.94/12.32  1 (wt=6) [] aux(A,B,btrue) = bfalse.
% 11.94/12.32  7 (wt=6) [] leqNat(s(A),z) = bfalse.
% 11.94/12.32  25 (wt=6) [] sorted(cons(A,nil)) = btrue.
% 11.94/12.32  31 (wt=6) [] eq(z,s(A)) = bfalse.
% 11.94/12.32  32 (wt=6) [] eq(s(A),z) = bfalse.
% 11.94/12.32  35 (wt=6) [] -(eq2(psorted_rev(A),bfalse) = btrue).
% 11.94/12.32  2 (wt=7) [] aux(A,B,bfalse) = unique(B).
% 11.94/12.32  3 (wt=7) [flip(2)] unique(A) = aux(B,A,bfalse).
% 11.94/12.32  10 (wt=8) [] lengthNat(cons(A,B)) = s(lengthNat(B)).
% 11.94/12.32  11 (wt=8) [flip(10)] s(lengthNat(A)) = lengthNat(cons(B,A)).
% 11.94/12.32  8 (wt=9) [] leqNat(s(A),s(B)) = leqNat(A,B).
% 11.94/12.32  30 (wt=9) [] eq(s(A),s(B)) = eq(A,B).
% 11.94/12.32  17 (wt=11) [] unique(cons(A,B)) = aux(A,B,elemNat(A,B)).
% 11.94/12.32  19 (wt=11) [flip(1)] cons(A,append(B,C)) = append(cons(A,B),C).
% 11.94/12.32  21 (wt=11) [] rev(cons(A,B)) = append(rev(B),cons(A,nil)).
% 11.94/12.32  15 (wt=13) [flip(1)] orb(eq(A,B),elemNat(A,C)) = elemNat(A,cons(B,C)).
% 11.94/12.32  26 (wt=15) [] sorted(cons(A,cons(B,C))) = andb(leqNat(A,B),sorted(cons(B,C))).
% 11.94/12.32  27 (wt=23) [flip(1)] impl(eq2(sorted(rev(A)),btrue),impl(eq2(unique(A),btrue),eq2(leqNat(lengthNat(A),s(s(s(z)))),btrue))) = psorted_rev(A).
% 11.94/12.32  end_of_list.
% 11.94/12.32  
% 11.94/12.32  Demodulators:
% 11.94/12.32  1 (wt=6) [] aux(A,B,btrue) = bfalse.
% 11.94/12.32  4 (wt=5) [] orb(btrue,A) = btrue.
% 11.94/12.32  5 (wt=5) [] orb(bfalse,A) = A.
% 11.94/12.32  6 (wt=5) [] leqNat(z,A) = btrue.
% 11.94/12.32  7 (wt=6) [] leqNat(s(A),z) = bfalse.
% 11.94/12.32  8 (wt=9) [] leqNat(s(A),s(B)) = leqNat(A,B).
% 11.94/12.32  9 (wt=4) [] lengthNat(nil) = z.
% 11.94/12.32  12 (wt=5) [] impl(btrue,A) = A.
% 11.94/12.32  13 (wt=5) [] impl(bfalse,A) = btrue.
% 11.94/12.32  14 (wt=5) [] elemNat(A,nil) = bfalse.
% 11.94/12.32  15 (wt=13) [flip(1)] orb(eq(A,B),elemNat(A,C)) = elemNat(A,cons(B,C)).
% 11.94/12.32  16 (wt=4) [] unique(nil) = btrue.
% 11.94/12.32  17 (wt=11) [] unique(cons(A,B)) = aux(A,B,elemNat(A,B)).
% 11.94/12.32  18 (wt=5) [] append(nil,A) = A.
% 11.94/12.32  19 (wt=11) [flip(1)] cons(A,append(B,C)) = append(cons(A,B),C).
% 11.94/12.32  20 (wt=4) [] rev(nil) = nil.
% 11.94/12.32  21 (wt=11) [] rev(cons(A,B)) = append(rev(B),cons(A,nil)).
% 11.94/12.32  22 (wt=5) [] andb(btrue,A) = A.
% 11.94/12.33  23 (wt=5) [] andb(bfalse,A) = bfalse.
% 11.94/12.33  24 (wt=4) [] sorted(nil) = btrue.
% 11.94/12.33  25 (wt=6) [] sorted(cons(A,nil)) = btrue.
% 11.94/12.33  26 (wt=15) [] sorted(cons(A,cons(B,C))) = andb(leqNat(A,B),sorted(cons(B,C))).
% 11.94/12.33  27 (wt=23) [flip(1)] impl(eq2(sorted(rev(A)),btrue),impl(eq2(unique(A),btrue),eq2(leqNat(lengthNat(A),s(s(s(z)))),btrue))) = psorted_rev(A).
% 11.94/12.33  28 (wt=5) [] eq2(bfalse,btrue) = bfalse.
% 11.94/12.33  29 (wt=5) [] eq2(btrue,bfalse) = bfalse.
% 11.94/12.33  30 (wt=9) [] eq(s(A),s(B)) = eq(A,B).
% 11.94/12.33  31 (wt=6) [] eq(z,s(A)) = bfalse.
% 11.94/12.33  32 (wt=6) [] eq(s(A),z) = bfalse.
% 11.94/12.33  33 (wt=5) [] eq(A,A) = btrue.
% 11.94/12.33  34 (wt=5) [] eq2(A,A) = btrue.
% 11.94/12.33  end_of_list.
% 11.94/12.33  
% 11.94/12.33  Passive:
% 11.94/12.33  end_of_list.
% 11.94/12.33  
% 11.94/12.33  ------------- memory usage ------------
% 11.94/12.33  Memory dynamically allocated (tp_alloc): 63964.
% 11.94/12.33    type (bytes each)        gets      frees     in use      avail      bytes
% 11.94/12.33  sym_ent (  96)               75          0         75          0      7.0 K
% 11.94/12.33  term (  16)             5953393    5093127     860266          2  16697.2 K
% 11.94/12.33  gen_ptr (   8)          5568530     666419    4902111          0  38297.7 K
% 11.94/12.33  context ( 808)         15434379   15434377          2         11     10.3 K
% 11.94/12.33  trail (  12)              70676      70676          0         13      0.2 K
% 11.94/12.33  bt_node (  68)          6762767    6762762          5         55      4.0 K
% 11.94/12.33  ac_position (285432)          0          0          0          0      0.0 K
% 11.94/12.33  ac_match_pos (14044)          0          0          0          0      0.0 K
% 11.94/12.33  ac_match_free_vars_pos (4020)
% 11.94/12.33                                0          0          0          0      0.0 K
% 11.94/12.33  discrim (  12)           446501      41160     405341          0   4750.1 K
% 11.94/12.33  flat (  40)            11261784   11261784          0         96      3.8 K
% 11.94/12.33  discrim_pos (  12)       270534     270534          0      
% 11.94/12.33  
% 11.94/12.33  ********** ABNORMAL END **********
% 11.94/12.33  ********** in tp_alloc, max_mem parameter exceeded.
% 11.94/12.33      1      0.0 K
% 11.94/12.33  fpa_head (  12)           25483          0      25483          0    298.6 K
% 11.94/12.33  fpa_tree (  28)           93146      93146          0         41      1.1 K
% 11.94/12.33  fpa_pos (  36)            35833      35833          0          1      0.0 K
% 11.94/12.33  literal (  12)           188351     161499      26852          0    314.7 K
% 11.94/12.33  clause (  24)            188351     161499      26852          0    629.3 K
% 11.94/12.33  list (  12)                9041       8985         56          3      0.7 K
% 11.94/12.33  list_pos (  20)           95673      14262      81411          0   1590.1 K
% 11.94/12.33  pair_index (   40)              2          0          2          0      0.1 K
% 11.94/12.33  
% 11.94/12.33  -------------- statistics -------------
% 11.94/12.33  Clauses input                 33
% 11.94/12.33    Usable input                   0
% 11.94/12.33    Sos input                     33
% 11.94/12.33    Demodulators input             0
% 11.94/12.33    Passive input                  0
% 11.94/12.33  
% 11.94/12.33  Processed BS (before search)  37
% 11.94/12.33  Forward subsumed BS            2
% 11.94/12.33  Kept BS                       35
% 11.94/12.33  New demodulators BS           30
% 11.94/12.33  Back demodulated BS            0
% 11.94/12.33  
% 11.94/12.33  Clauses or pairs given    685635
% 11.94/12.33  Clauses generated         107664
% 11.94/12.33  Forward subsumed           80848
% 11.94/12.33  Deleted by weight              0
% 11.94/12.33  Deleted by variable count      0
% 11.94/12.33  Kept                       26816
% 11.94/12.33  New demodulators            8952
% 11.94/12.33  Back demodulated            3050
% 11.94/12.33  Ordered paramod prunes         0
% 11.94/12.33  Basic paramod prunes     2627995
% 11.94/12.33  Prime paramod prunes          25
% 11.94/12.33  Semantic prunes                0
% 11.94/12.33  
% 11.94/12.33  Rewrite attmepts         2897470
% 11.94/12.33  Rewrites                  230243
% 11.94/12.33  
% 11.94/12.33  FPA overloads                  0
% 11.94/12.33  FPA underloads                 0
% 11.94/12.33  
% 11.94/12.33  Usable size                    0
% 11.94/12.33  Sos size                   23801
% 11.94/12.33  Demodulators size           6958
% 11.94/12.33  Passive size                   0
% 11.94/12.33  Disabled size               3050
% 11.94/12.33  
% 11.94/12.33  Proofs found                   0
% 11.94/12.33  
% 11.94/12.33  ----------- times (seconds) ----------- Tue May  5 11:26:28 2026
% 11.94/12.33  
% 11.94/12.33  user CPU time             8.40   (0 hr, 0 min, 8 sec)
% 11.94/12.33  system CPU time           2.83   (0 hr, 0 min, 2 sec)
% 11.94/12.33  wall-clock time          11      (0 hr, 0 min, 11 sec)
% 11.94/12.33  input time                0.00
% 11.94/12.33  paramodulation time       1.05
% 11.94/12.33  demodulation time         0.36
% 11.94/12.33  orient time               0.21
% 11.94/12.33  weigh time                0.05
% 11.94/12.33  forward subsume time      0.15
% 11.94/12.33  back demod find time      0.18
% 11.94/12.33  conflict time             0.02
% 11.94/12.33  LRPO time                 0.10
% 11.94/12.33  store clause time         4.70
% 11.94/12.33  disable clause time       0.56
% 11.94/12.33  prime paramod time        0.10
% 11.94/12.33  semantics time            0.00
% 11.94/12.33  
% 11.94/12.33  EQP interrupted
%------------------------------------------------------------------------------