%------------------------------------------------------------------------------ % File : EQP---0.9e % Problem : SWX201-1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : tptp2X_and_run_eqp %s % Computer : n014.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 15.12s 15.55s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWX201-1 : TPTP v9.3.0. Released v9.3.0. % 0.12/0.13 % Command : tptp2X_and_run_eqp %s % 0.15/0.34 % Computer : n014.cluster.edu % 0.15/0.34 % Model : x86_64 x86_64 % 0.15/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.34 % Memory : 8042.1875MB % 0.15/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.34 % CPULimit : 300 % 0.15/0.34 % WCLimit : 300 % 0.15/0.34 % DateTime : Tue May 5 11:18:51 EDT 2026 % 0.15/0.34 % CPUTime : % 0.67/1.09 ----- EQP 0.9e, May 2009 ----- % 0.67/1.09 The job began on n014.cluster.edu, Tue May 5 11:18:52 2026 % 0.67/1.09 The command was "./eqp09e". % 0.67/1.09 % 0.67/1.09 set(prolog_style_variables). % 0.67/1.09 set(lrpo). % 0.67/1.09 set(basic_paramod). % 0.67/1.09 set(functional_subsume). % 0.67/1.09 set(ordered_paramod). % 0.67/1.09 set(prime_paramod). % 0.67/1.09 set(para_pairs). % 0.67/1.09 assign(pick_given_ratio,4). % 0.67/1.09 clear(print_kept). % 0.67/1.09 clear(print_new_demod). % 0.67/1.09 clear(print_back_demod). % 0.67/1.09 clear(print_given). % 0.67/1.09 assign(max_mem,64000). % 0.67/1.09 end_of_commands. % 0.67/1.09 % 0.67/1.09 Usable: % 0.67/1.09 end_of_list. % 0.67/1.09 % 0.67/1.09 Sos: % 0.67/1.09 0 (wt=-1) [] aux(A,B,C,pair2(D,E)) = pair2(cons(B,D),E). % 0.67/1.09 0 (wt=-1) [] aux2(A,B,C,D,btrue) = cons(A,merge(B,cons(C,D))). % 0.67/1.09 0 (wt=-1) [] aux2(A,B,C,D,bfalse) = cons(C,merge(cons(A,B),D)). % 0.67/1.09 0 (wt=-1) [] aux3(A,B,C,pair2(D,E)) = merge(msort(D),msort(E)). % 0.67/1.09 0 (wt=-1) [] aux4(A,B,C,btrue) = s(count(A,C)). % 0.67/1.09 0 (wt=-1) [] aux4(A,B,C,bfalse) = count(A,C). % 0.67/1.09 0 (wt=-1) [] splitAtNat(z,A) = pair2(nil,A). % 0.67/1.09 0 (wt=-1) [] splitAtNat(s(A),nil) = pair2(nil,nil). % 0.67/1.09 0 (wt=-1) [] splitAtNat(s(A),cons(B,C)) = aux(A,B,C,splitAtNat(A,C)). % 0.67/1.09 0 (wt=-1) [] leqNat(z,A) = btrue. % 0.67/1.09 0 (wt=-1) [] leqNat(s(A),z) = bfalse. % 0.67/1.09 0 (wt=-1) [] leqNat(s(A),s(B)) = leqNat(A,B). % 0.67/1.09 0 (wt=-1) [] merge(nil,A) = A. % 0.67/1.09 0 (wt=-1) [] merge(cons(A,B),nil) = cons(A,B). % 0.67/1.09 0 (wt=-1) [] merge(cons(A,B),cons(C,D)) = aux2(A,B,C,D,leqNat(A,C)). % 0.67/1.09 0 (wt=-1) [] lengthNat(nil) = z. % 0.67/1.09 0 (wt=-1) [] lengthNat(cons(A,B)) = s(lengthNat(B)). % 0.67/1.09 0 (wt=-1) [] impl(btrue,A) = A. % 0.67/1.09 0 (wt=-1) [] impl(bfalse,A) = btrue. % 0.67/1.09 0 (wt=-1) [] div2(z) = z. % 0.67/1.09 0 (wt=-1) [] div2(s(z)) = z. % 0.67/1.09 0 (wt=-1) [] div2(s(s(A))) = s(div2(A)). % 0.67/1.09 0 (wt=-1) [] msort(nil) = nil. % 0.67/1.09 0 (wt=-1) [] msort(cons(A,nil)) = cons(A,nil). % 0.67/1.09 0 (wt=-1) [] msort(cons(A,cons(B,C))) = aux3(A,B,C,splitAtNat(div2(lengthNat(cons(A,cons(B,C)))),cons(A,cons(B,C)))). % 0.67/1.09 0 (wt=-1) [] count(A,nil) = z. % 0.67/1.09 0 (wt=-1) [] count(A,cons(B,C)) = aux4(A,B,C,eq(B,A)). % 0.67/1.09 0 (wt=-1) [] prop_msort_permutation_wrong1(A,B) = impl(eq2(leqNat(count(B,A),s(s(s(s(s(z)))))),bfalse),eq(count(B,A),count(s(B),msort(A)))). % 0.67/1.09 0 (wt=-1) [] eq2(bfalse,btrue) = bfalse. % 0.67/1.09 0 (wt=-1) [] eq2(btrue,bfalse) = bfalse. % 0.67/1.09 0 (wt=-1) [] eq(s(A),s(B)) = eq(A,B). % 0.67/1.09 0 (wt=-1) [] eq(z,s(A)) = bfalse. % 0.67/1.09 0 (wt=-1) [] eq(s(A),z) = bfalse. % 0.67/1.09 0 (wt=-1) [] eq(A,A) = btrue. % 0.67/1.09 0 (wt=-1) [] eq2(A,A) = btrue. % 0.67/1.09 0 (wt=-1) [] -(eq2(prop_msort_permutation_wrong1(A,B),bfalse) = btrue). % 0.67/1.09 end_of_list. % 0.67/1.09 % 0.67/1.09 Demodulators: % 0.67/1.09 end_of_list. % 0.67/1.09 % 0.67/1.09 Passive: % 0.67/1.09 end_of_list. % 0.67/1.09 % 0.67/1.09 Starting to process input. % 0.67/1.09 % 0.67/1.09 ** KEPT: 1 (wt=13) [] aux(A,B,C,pair2(D,E)) = pair2(cons(B,D),E). % 0.67/1.09 % 0.67/1.09 ** KEPT: 2 (wt=13) [flip(1)] pair2(cons(A,B),C) = aux(D,A,E,pair2(B,C)). % 0.67/1.09 clause forward subsumed: 0 (wt=13) [flip(2)] aux(D,A,E,pair2(B,C)) = pair2(cons(A,B),C). % 0.67/1.09 % 0.67/1.09 ** KEPT: 3 (wt=14) [flip(1)] cons(A,merge(B,cons(C,D))) = aux2(A,B,C,D,btrue). % 0.67/1.09 3 is a new demodulator. % 0.67/1.09 % 0.67/1.09 ** KEPT: 4 (wt=14) [flip(1)] cons(A,merge(cons(B,C),D)) = aux2(B,C,A,D,bfalse). % 0.67/1.09 4 is a new demodulator. % 0.67/1.09 % 0.67/1.09 ** KEPT: 5 (wt=13) [] aux3(A,B,C,pair2(D,E)) = merge(msort(D),msort(E)). % 0.67/1.09 % 0.67/1.09 ** KEPT: 6 (wt=13) [flip(5)] merge(msort(A),msort(B)) = aux3(C,D,E,pair2(A,B)). % 0.67/1.09 clause forward subsumed: 0 (wt=13) [flip(6)] aux3(C,D,E,pair2(A,B)) = merge(msort(A),msort(B)). % 0.67/1.09 % 0.67/1.09 ** KEPT: 7 (wt=10) [] aux4(A,B,C,btrue) = s(count(A,C)). % 0.67/1.09 % 0.67/1.09 ** KEPT: 8 (wt=10) [flip(7)] s(count(A,B)) = aux4(A,C,B,btrue). % 0.67/1.09 clause forward subsumed: 0 (wt=10) [flip(8)] aux4(A,C,B,btrue) = s(count(A,B)). % 0.67/1.09 % 0.67/1.09 ** KEPT: 9 (wt=9) [] aux4(A,B,C,bfalse) = count(A,C). % 0.67/1.09 % 0.67/1.09 ** KEPT: 10 (wt=9) [flip(9)] count(A,B) = aux4(A,C,B,bfalse). % 0.67/1.09 clause forward subsumed: 0 (wt=9) [flip(10)] aux4(A,C,B,bfalse) = count(A,B). % 0.67/1.09 % 0.67/1.09 ** KEPT: 11 (wt=7) [] splitAtNat(z,A) = pair2(nil,A). % 0.67/1.09 11 is a new demodulator. % 0.67/1.09 % 0.67/1.09 ** KEPT: 12 (wt=8) [] splitAtNat(s(A),nil) = pair2(nil,nil). % 0.67/1.09 12 is a new demodulator. % 0.67/1.09 % 0.67/1.09 ** KEPT: 13 (wt=14) [] splitAtNat(s(A),cons(B,C)) = aux(A,B,C,splitAtNat(A,C)). % 0.67/1.09 13 is a new demodulator. % 0.67/1.09 % 0.67/1.09 ** KEPT: 14 (wt=5) [] leqNat(z,A) = btrue. % 0.67/1.09 14 is a new demodulator. % 0.67/1.09 % 0.67/1.09 ** KEPT: 15 (wt=6) [] leqNat(s(A),z) = bfalse. % 0.67/1.09 15 is a new demodulator. % 0.67/1.09 % 0.67/1.09 ** KEPT: 16 (wt=9) [] leqNat(s(A),s(B)) = leqNat(A,B). % 0.67/1.09 16 is a new demodulator. % 0.67/1.09 % 0.67/1.09 ** KEPT: 17 (wt=5) [] merge(nil,A) = A. % 0.67/1.09 17 is a new demodulator. % 0.67/1.09 % 0.67/1.09 ** KEPT: 18 (wt=9) [] merge(cons(A,B),nil) = cons(A,B). % 0.67/1.09 18 is a new demodulator. % 0.67/1.09 % 0.67/1.09 ** KEPT: 19 (wt=16) [] merge(cons(A,B),cons(C,D)) = aux2(A,B,C,D,leqNat(A,C)). % 15.12/15.54 19 is a new demodulator. % 15.12/15.54 % 15.12/15.54 ** KEPT: 20 (wt=4) [] lengthNat(nil) = z. % 15.12/15.54 20 is a new demodulator. % 15.12/15.54 % 15.12/15.54 ** KEPT: 21 (wt=8) [] lengthNat(cons(A,B)) = s(lengthNat(B)). % 15.12/15.54 % 15.12/15.54 ** KEPT: 22 (wt=8) [flip(21)] s(lengthNat(A)) = lengthNat(cons(B,A)). % 15.12/15.54 clause forward subsumed: 0 (wt=8) [flip(22)] lengthNat(cons(B,A)) = s(lengthNat(A)). % 15.12/15.54 % 15.12/15.54 ** KEPT: 23 (wt=5) [] impl(btrue,A) = A. % 15.12/15.54 23 is a new demodulator. % 15.12/15.54 % 15.12/15.54 ** KEPT: 24 (wt=5) [] impl(bfalse,A) = btrue. % 15.12/15.54 24 is a new demodulator. % 15.12/15.54 % 15.12/15.54 ** KEPT: 25 (wt=4) [] div2(z) = z. % 15.12/15.54 25 is a new demodulator. % 15.12/15.54 % 15.12/15.54 ** KEPT: 26 (wt=5) [] div2(s(z)) = z. % 15.12/15.54 26 is a new demodulator. % 15.12/15.54 % 15.12/15.54 ** KEPT: 27 (wt=8) [] div2(s(s(A))) = s(div2(A)). % 15.12/15.54 27 is a new demodulator. % 15.12/15.54 % 15.12/15.54 ** KEPT: 28 (wt=4) [] msort(nil) = nil. % 15.12/15.54 28 is a new demodulator. % 15.12/15.54 % 15.12/15.54 ** KEPT: 29 (wt=8) [] msort(cons(A,nil)) = cons(A,nil). % 15.12/15.54 29 is a new demodulator. % 15.12/15.54 % 15.12/15.54 ** KEPT: 30 (wt=24) [] msort(cons(A,cons(B,C))) = aux3(A,B,C,splitAtNat(div2(lengthNat(cons(A,cons(B,C)))),cons(A,cons(B,C)))). % 15.12/15.54 30 is a new demodulator. % 15.12/15.54 % 15.12/15.54 ** KEPT: 31 (wt=5) [] count(A,nil) = z. % 15.12/15.54 31 is a new demodulator. % 15.12/15.54 % 15.12/15.54 ** KEPT: 32 (wt=13) [] count(A,cons(B,C)) = aux4(A,B,C,eq(B,A)). % 15.12/15.54 % 15.12/15.54 ** KEPT: 33 (wt=13) [flip(32)] aux4(A,B,C,eq(B,A)) = count(A,cons(B,C)). % 15.12/15.54 clause forward subsumed: 0 (wt=13) [flip(33)] count(A,cons(B,C)) = aux4(A,B,C,eq(B,A)). % 15.12/15.54 % 15.12/15.54 ** KEPT: 34 (wt=26) [] prop_msort_permutation_wrong1(A,B) = impl(eq2(leqNat(count(B,A),s(s(s(s(s(z)))))),bfalse),eq(count(B,A),count(s(B),msort(A)))). % 15.12/15.54 % 15.12/15.54 ** KEPT: 35 (wt=26) [flip(34)] impl(eq2(leqNat(count(A,B),s(s(s(s(s(z)))))),bfalse),eq(count(A,B),count(s(A),msort(B)))) = prop_msort_permutation_wrong1(B,A). % 15.12/15.54 clause forward subsumed: 0 (wt=26) [flip(35)] prop_msort_permutation_wrong1(B,A) = impl(eq2(leqNat(count(A,B),s(s(s(s(s(z)))))),bfalse),eq(count(A,B),count(s(A),msort(B)))). % 15.12/15.54 % 15.12/15.54 ** KEPT: 36 (wt=5) [] eq2(bfalse,btrue) = bfalse. % 15.12/15.54 36 is a new demodulator. % 15.12/15.54 % 15.12/15.54 ** KEPT: 37 (wt=5) [] eq2(btrue,bfalse) = bfalse. % 15.12/15.54 37 is a new demodulator. % 15.12/15.54 % 15.12/15.54 ** KEPT: 38 (wt=9) [] eq(s(A),s(B)) = eq(A,B). % 15.12/15.54 38 is a new demodulator. % 15.12/15.54 % 15.12/15.54 ** KEPT: 39 (wt=6) [] eq(z,s(A)) = bfalse. % 15.12/15.54 39 is a new demodulator. % 15.12/15.54 % 15.12/15.54 ** KEPT: 40 (wt=6) [] eq(s(A),z) = bfalse. % 15.12/15.54 40 is a new demodulator. % 15.12/15.54 % 15.12/15.54 ** KEPT: 41 (wt=5) [] eq(A,A) = btrue. % 15.12/15.54 41 is a new demodulator. % 15.12/15.54 % 15.12/15.54 ** KEPT: 42 (wt=5) [] eq2(A,A) = btrue. % 15.12/15.54 42 is a new demodulator. % 15.12/15.54 % 15.12/15.54 ** KEPT: 43 (wt=7) [] -(eq2(prop_msort_permutation_wrong1(A,B),bfalse) = btrue). % 15.12/15.54 % 15.12/15.54 After processing input: % 15.12/15.54 % 15.12/15.54 Usable: % 15.12/15.54 end_of_list. % 15.12/15.54 % 15.12/15.54 Sos: % 15.12/15.54 20 (wt=4) [] lengthNat(nil) = z. % 15.12/15.54 25 (wt=4) [] div2(z) = z. % 15.12/15.54 28 (wt=4) [] msort(nil) = nil. % 15.12/15.54 14 (wt=5) [] leqNat(z,A) = btrue. % 15.12/15.54 17 (wt=5) [] merge(nil,A) = A. % 15.12/15.54 23 (wt=5) [] impl(btrue,A) = A. % 15.12/15.54 24 (wt=5) [] impl(bfalse,A) = btrue. % 15.12/15.54 26 (wt=5) [] div2(s(z)) = z. % 15.12/15.54 31 (wt=5) [] count(A,nil) = z. % 15.12/15.54 36 (wt=5) [] eq2(bfalse,btrue) = bfalse. % 15.12/15.54 37 (wt=5) [] eq2(btrue,bfalse) = bfalse. % 15.12/15.54 41 (wt=5) [] eq(A,A) = btrue. % 15.12/15.54 42 (wt=5) [] eq2(A,A) = btrue. % 15.12/15.54 15 (wt=6) [] leqNat(s(A),z) = bfalse. % 15.12/15.54 39 (wt=6) [] eq(z,s(A)) = bfalse. % 15.12/15.54 40 (wt=6) [] eq(s(A),z) = bfalse. % 15.12/15.54 11 (wt=7) [] splitAtNat(z,A) = pair2(nil,A). % 15.12/15.54 43 (wt=7) [] -(eq2(prop_msort_permutation_wrong1(A,B),bfalse) = btrue). % 15.12/15.54 12 (wt=8) [] splitAtNat(s(A),nil) = pair2(nil,nil). % 15.12/15.54 21 (wt=8) [] lengthNat(cons(A,B)) = s(lengthNat(B)). % 15.12/15.54 22 (wt=8) [flip(21)] s(lengthNat(A)) = lengthNat(cons(B,A)). % 15.12/15.54 27 (wt=8) [] div2(s(s(A))) = s(div2(A)). % 15.12/15.54 29 (wt=8) [] msort(cons(A,nil)) = cons(A,nil). % 15.12/15.54 9 (wt=9) [] aux4(A,B,C,bfalse) = count(A,C). % 15.12/15.54 10 (wt=9) [flip(9)] count(A,B) = aux4(A,C,B,bfalse). % 15.12/15.54 16 (wt=9) [] leqNat(s(A),s(B)) = leqNat(A,B). % 15.12/15.54 18 (wt=9) [] merge(cons(A,B),nil) = cons(A,B). % 15.12/15.54 38 (wt=9) [] eq(s(A),s(B)) = eq(A,B). % 15.12/15.54 7 (wt=10) [] aux4(A,B,C,btrue) = s(count(A,C)). % 15.12/15.54 8 (wt=10) [flip(7)] s(count(A,B)) = aux4(A,C,B,btrue). % 15.12/15.54 1 (wt=13) [] aux(A,B,C,pair2(D,E)) = pair2(cons(B,D),E). % 15.12/15.54 2 (wt=13) [flip(1)] pair2(cons(A,B),C) = aux(D,A,E,pair2(B,C)). % 15.12/15.54 5 (wt=13) [] aux3(A,B,C,pair2(D,E)) = merge(msort(D),msort(E)). % 15.12/15.54 6 (wt=13) [flip(5)] merge(msort(A),msort(B)) = aux3(C,D,E,pair2(A,B)). % 15.12/15.54 32 (wt=13) [] count(A,cons(B,C)) = aux4(A,B,C,eq(B,A)). % 15.12/15.54 33 (wt=13) [flip(32)] aux4(A,B,C,eq(B,A)) = count(A,cons(B,C)). % 15.12/15.54 3 (wt=14) [flip(1)] cons(A,merge(B,cons(C,D))) = aux2(A,B,C,D,btrue). % 15.12/15.54 4 (wt=14) [flip(1)] cons(A,merge(cons(B,C),D)) = aux2(B,C,A,D,bfalse). % 15.12/15.54 13 (wt=14) [] splitAtNat(s(A),cons(B,C)) = aux(A,B,C,splitAtNat(A,C)). % 15.12/15.54 19 (wt=16) [] merge(cons(A,B),cons(C,D)) = aux2(A,B,C,D,leqNat(A,C)). % 15.12/15.54 30 (wt=24) [] msort(cons(A,cons(B,C))) = aux3(A,B,C,splitAtNat(div2(lengthNat(cons(A,cons(B,C)))),cons(A,cons(B,C)))). % 15.12/15.54 34 (wt=26) [] prop_msort_permutation_wrong1(A,B) = impl(eq2(leqNat(count(B,A),s(s(s(s(s(z)))))),bfalse),eq(count(B,A),count(s(B),msort(A)))). % 15.12/15.54 35 (wt=26) [flip(34)] impl(eq2(leqNat(count(A,B),s(s(s(s(s(z)))))),bfalse),eq(count(A,B),count(s(A),msort(B)))) = prop_msort_permutation_wrong1(B,A). % 15.12/15.54 end_of_list. % 15.12/15.54 % 15.12/15.54 Demodulators: % 15.12/15.54 3 (wt=14) [flip(1)] cons(A,merge(B,cons(C,D))) = aux2(A,B,C,D,btrue). % 15.12/15.54 4 (wt=14) [flip(1)] cons(A,merge(cons(B,C),D)) = aux2(B,C,A,D,bfalse). % 15.12/15.54 11 (wt=7) [] splitAtNat(z,A) = pair2(nil,A). % 15.12/15.54 12 (wt=8) [] splitAtNat(s(A),nil) = pair2(nil,nil). % 15.12/15.54 13 (wt=14) [] splitAtNat(s(A),cons(B,C)) = aux(A,B,C,splitAtNat(A,C)). % 15.12/15.54 14 (wt=5) [] leqNat(z,A) = btrue. % 15.12/15.54 15 (wt=6) [] leqNat(s(A),z) = bfalse. % 15.12/15.54 16 (wt=9) [] leqNat(s(A),s(B)) = leqNat(A,B). % 15.12/15.54 17 (wt=5) [] merge(nil,A) = A. % 15.12/15.54 18 (wt=9) [] merge(cons(A,B),nil) = cons(A,B). % 15.12/15.54 19 (wt=16) [] merge(cons(A,B),cons(C,D)) = aux2(A,B,C,D,leqNat(A,C)). % 15.12/15.54 20 (wt=4) [] lengthNat(nil) = z. % 15.12/15.54 23 (wt=5) [] impl(btrue,A) = A. % 15.12/15.54 24 (wt=5) [] impl(bfalse,A) = btrue. % 15.12/15.54 25 (wt=4) [] div2(z) = z. % 15.12/15.54 26 (wt=5) [] div2(s(z)) = z. % 15.12/15.54 27 (wt=8) [] div2(s(s(A))) = s(div2(A)). % 15.12/15.54 28 (wt=4) [] msort(nil) = nil. % 15.12/15.54 29 (wt=8) [] msort(cons(A,nil)) = cons(A,nil). % 15.12/15.54 30 (wt=24) [] msort(cons(A,cons(B,C))) = aux3(A,B,C,splitAtNat(div2(lengthNat(cons(A,cons(B,C)))),cons(A,cons(B,C)))). % 15.12/15.54 31 (wt=5) [] count(A,nil) = z. % 15.12/15.54 36 (wt=5) [] eq2(bfalse,btrue) = bfalse. % 15.12/15.54 37 (wt=5) [] eq2(btrue,bfalse) = bfalse. % 15.12/15.54 38 (wt=9) [] eq(s(A),s(B)) = eq(A,B). % 15.12/15.54 39 (wt=6) [] eq(z,s(A)) = bfalse. % 15.12/15.54 40 (wt=6) [] eq(s(A),z) = bfalse. % 15.12/15.54 41 (wt=5) [] eq(A,A) = btrue. % 15.12/15.54 42 (wt=5) [] eq2(A,A) = btrue. % 15.12/15.54 end_of_list. % 15.12/15.54 % 15.12/15.54 Passive: % 15.12/15.54 end_of_list. % 15.12/15.54 % 15.12/15.54 ------------- memory usage ------------ % 15.12/15.54 Memory dynamically allocated (tp_alloc): 63964. % 15.12/15.54 type (bytes each) gets frees in use avail bytes % 15.12/15.54 sym_ent ( 96) 83 0 83 0 7.8 K % 15.12/15.54 term ( 16) 3013993 2045442 968551 6 18785.7 K % 15.12/15.54 gen_ptr ( 8) 4668088 405994 4262094 0 33297.6 K % 15.12/15.54 context ( 808) 13319809 % 15.12/15.54 % 15.12/15.54 ********** ABNORMAL END ********** % 15.12/15.54 ********** in tp_alloc, max_mem parameter exceeded. % 15.12/15.54 13319807 2 5 5.5 K % 15.12/15.54 trail ( 12) 50919 50919 0 12 0.1 K % 15.12/15.54 bt_node ( 68) 6357334 6357331 3 30 2.2 K % 15.12/15.54 ac_position (285432) 0 0 0 0 0.0 K % 15.12/15.54 ac_match_pos (14044) 0 0 0 0 0.0 K % 15.12/15.54 ac_match_free_vars_pos (4020) % 15.12/15.54 0 0 0 0 0.0 K % 15.12/15.54 discrim ( 12) 549645 34134 515511 0 6041.1 K % 15.12/15.54 flat ( 40) 6394329 6394329 0 90 3.5 K % 15.12/15.54 discrim_pos ( 12) 95970 95970 0 1 0.0 K % 15.12/15.54 fpa_head ( 12) 68712 0 68712 0 805.2 K % 15.12/15.54 fpa_tree ( 28) 95806 95806 0 25 0.7 K % 15.12/15.54 fpa_pos ( 36) 42036 42036 0 1 0.0 K % 15.12/15.54 literal ( 12) 158615 124954 33661 1 394.5 K % 15.12/15.54 clause ( 24) 158615 124954 33661 1 789.0 K % 15.12/15.54 list ( 12) 8434 8378 56 3 0.7 K % 15.12/15.54 list_pos ( 20) 115053 14035 101018 0 1973.0 K % 15.12/15.54 pair_index ( 40) 2 0 2 0 0.1 K % 15.12/15.54 % 15.12/15.54 -------------- statistics ------------- % 15.12/15.54 Clauses input 36 % 15.12/15.54 Usable input 0 % 15.12/15.54 Sos input 36 % 15.12/15.54 Demodulators input 0 % 15.12/15.54 Passive input 0 % 15.12/15.54 % 15.12/15.54 Processed BS (before search) 50 % 15.12/15.54 Forward subsumed BS 7 % 15.12/15.54 Kept BS 43 % 15.12/15.54 New demodulators BS 28 % 15.12/15.54 Back demodulated BS 0 % 15.12/15.54 % 15.12/15.54 Clauses or pairs given 919100 % 15.12/15.54 Clauses generated 91884 % 15.12/15.54 Forward subsumed 58266 % 15.12/15.54 Deleted by weight 0 % 15.12/15.54 Deleted by variable count 0 % 15.12/15.54 Kept 33618 % 15.12/15.54 New demodulators 8347 % 15.12/15.54 Back demodulated 2829 % 15.12/15.54 Ordered paramod prunes 0 % 15.12/15.54 Basic paramod prunes 3501926 % 15.12/15.54 Prime paramod prunes 4 % 15.12/15.54 Semantic prunes 0 % 15.12/15.54 % 15.12/15.54 Rewrite attmepts 1554412 % 15.12/15.54 Rewrites 69553 % 15.12/15.54 % 15.12/15.54 FPA overloads 0 % 15.12/15.54 FPA underloads 0 % 15.12/15.54 % 15.12/15.54 Usable size 0 % 15.12/15.54 Sos size 30832 % 15.12/15.54 Demodulators size 5693 % 15.12/15.54 Passive size 0 % 15.12/15.54 Disabled size 2829 % 15.12/15.54 % 15.12/15.54 Proofs found 0 % 15.12/15.54 % 15.12/15.54 ----------- times (seconds) ----------- Tue May 5 11:19:06 2026 % 15.12/15.54 % 15.12/15.54 user CPU time 11.24 (0 hr, 0 min, 11 sec) % 15.12/15.54 system CPU time 3.21 (0 hr, 0 min, 3 sec) % 15.12/15.54 wall-clock time 14 (0 hr, 0 min, 14 sec) % 15.12/15.54 input time 0.00 % 15.12/15.54 paramodulation time 1.18 % 15.12/15.54 demodulation time 0.22 % 15.12/15.54 orient time 0.19 % 15.12/15.54 weigh time 0.04 % 15.12/15.54 forward subsume time 0.12 % 15.12/15.54 back demod find time 0.13 % 15.12/15.54 conflict time 0.03 % 15.12/15.54 LRPO time 0.09 % 15.12/15.54 store clause time 7.34 % 15.12/15.54 disable clause time 0.71 % 15.12/15.54 prime paramod time 0.08 % 15.12/15.54 semantics time 0.00 % 15.12/15.54 % 15.12/15.55 EQP interrupted %------------------------------------------------------------------------------