%------------------------------------------------------------------------------ % File : EQP---0.9e % Problem : SWX202-1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : tptp2X_and_run_eqp %s % Computer : n028.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.32s 15.75s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWX202-1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.12 % Command : tptp2X_and_run_eqp %s % 0.15/0.33 % Computer : n028.cluster.edu % 0.15/0.33 % Model : x86_64 x86_64 % 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.33 % Memory : 8042.1875MB % 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.33 % CPULimit : 300 % 0.15/0.33 % WCLimit : 300 % 0.15/0.33 % DateTime : Tue May 5 11:22:30 EDT 2026 % 0.15/0.33 % CPUTime : % 0.67/1.09 ----- EQP 0.9e, May 2009 ----- % 0.67/1.09 The job began on n028.cluster.edu, Tue May 5 11:22:31 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_wrong2(A,B) = impl(eq2(leqNat(count(B,A),s(s(s(s(s(z)))))),bfalse),eq(count(s(B),A),count(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_wrong2(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.32/15.74 19 is a new demodulator. % 15.32/15.74 % 15.32/15.74 ** KEPT: 20 (wt=4) [] lengthNat(nil) = z. % 15.32/15.74 20 is a new demodulator. % 15.32/15.74 % 15.32/15.74 ** KEPT: 21 (wt=8) [] lengthNat(cons(A,B)) = s(lengthNat(B)). % 15.32/15.74 % 15.32/15.74 ** KEPT: 22 (wt=8) [flip(21)] s(lengthNat(A)) = lengthNat(cons(B,A)). % 15.32/15.74 clause forward subsumed: 0 (wt=8) [flip(22)] lengthNat(cons(B,A)) = s(lengthNat(A)). % 15.32/15.74 % 15.32/15.74 ** KEPT: 23 (wt=5) [] impl(btrue,A) = A. % 15.32/15.74 23 is a new demodulator. % 15.32/15.74 % 15.32/15.74 ** KEPT: 24 (wt=5) [] impl(bfalse,A) = btrue. % 15.32/15.74 24 is a new demodulator. % 15.32/15.74 % 15.32/15.74 ** KEPT: 25 (wt=4) [] div2(z) = z. % 15.32/15.74 25 is a new demodulator. % 15.32/15.74 % 15.32/15.74 ** KEPT: 26 (wt=5) [] div2(s(z)) = z. % 15.32/15.74 26 is a new demodulator. % 15.32/15.74 % 15.32/15.74 ** KEPT: 27 (wt=8) [] div2(s(s(A))) = s(div2(A)). % 15.32/15.74 27 is a new demodulator. % 15.32/15.74 % 15.32/15.74 ** KEPT: 28 (wt=4) [] msort(nil) = nil. % 15.32/15.74 28 is a new demodulator. % 15.32/15.74 % 15.32/15.74 ** KEPT: 29 (wt=8) [] msort(cons(A,nil)) = cons(A,nil). % 15.32/15.74 29 is a new demodulator. % 15.32/15.74 % 15.32/15.74 ** 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.32/15.74 30 is a new demodulator. % 15.32/15.74 % 15.32/15.74 ** KEPT: 31 (wt=5) [] count(A,nil) = z. % 15.32/15.74 31 is a new demodulator. % 15.32/15.74 % 15.32/15.74 ** KEPT: 32 (wt=13) [] count(A,cons(B,C)) = aux4(A,B,C,eq(B,A)). % 15.32/15.74 % 15.32/15.74 ** KEPT: 33 (wt=13) [flip(32)] aux4(A,B,C,eq(B,A)) = count(A,cons(B,C)). % 15.32/15.74 clause forward subsumed: 0 (wt=13) [flip(33)] count(A,cons(B,C)) = aux4(A,B,C,eq(B,A)). % 15.32/15.74 % 15.32/15.74 ** KEPT: 34 (wt=26) [] prop_msort_permutation_wrong2(A,B) = impl(eq2(leqNat(count(B,A),s(s(s(s(s(z)))))),bfalse),eq(count(s(B),A),count(B,msort(A)))). % 15.32/15.74 % 15.32/15.74 ** KEPT: 35 (wt=26) [flip(34)] impl(eq2(leqNat(count(A,B),s(s(s(s(s(z)))))),bfalse),eq(count(s(A),B),count(A,msort(B)))) = prop_msort_permutation_wrong2(B,A). % 15.32/15.74 clause forward subsumed: 0 (wt=26) [flip(35)] prop_msort_permutation_wrong2(B,A) = impl(eq2(leqNat(count(A,B),s(s(s(s(s(z)))))),bfalse),eq(count(s(A),B),count(A,msort(B)))). % 15.32/15.74 % 15.32/15.74 ** KEPT: 36 (wt=5) [] eq2(bfalse,btrue) = bfalse. % 15.32/15.74 36 is a new demodulator. % 15.32/15.74 % 15.32/15.74 ** KEPT: 37 (wt=5) [] eq2(btrue,bfalse) = bfalse. % 15.32/15.74 37 is a new demodulator. % 15.32/15.74 % 15.32/15.74 ** KEPT: 38 (wt=9) [] eq(s(A),s(B)) = eq(A,B). % 15.32/15.74 38 is a new demodulator. % 15.32/15.74 % 15.32/15.74 ** KEPT: 39 (wt=6) [] eq(z,s(A)) = bfalse. % 15.32/15.74 39 is a new demodulator. % 15.32/15.74 % 15.32/15.74 ** KEPT: 40 (wt=6) [] eq(s(A),z) = bfalse. % 15.32/15.74 40 is a new demodulator. % 15.32/15.74 % 15.32/15.74 ** KEPT: 41 (wt=5) [] eq(A,A) = btrue. % 15.32/15.74 41 is a new demodulator. % 15.32/15.74 % 15.32/15.74 ** KEPT: 42 (wt=5) [] eq2(A,A) = btrue. % 15.32/15.74 42 is a new demodulator. % 15.32/15.74 % 15.32/15.74 ** KEPT: 43 (wt=7) [] -(eq2(prop_msort_permutation_wrong2(A,B),bfalse) = btrue). % 15.32/15.74 % 15.32/15.74 After processing input: % 15.32/15.74 % 15.32/15.74 Usable: % 15.32/15.74 end_of_list. % 15.32/15.74 % 15.32/15.74 Sos: % 15.32/15.74 20 (wt=4) [] lengthNat(nil) = z. % 15.32/15.74 25 (wt=4) [] div2(z) = z. % 15.32/15.74 28 (wt=4) [] msort(nil) = nil. % 15.32/15.74 14 (wt=5) [] leqNat(z,A) = btrue. % 15.32/15.74 17 (wt=5) [] merge(nil,A) = A. % 15.32/15.74 23 (wt=5) [] impl(btrue,A) = A. % 15.32/15.74 24 (wt=5) [] impl(bfalse,A) = btrue. % 15.32/15.74 26 (wt=5) [] div2(s(z)) = z. % 15.32/15.74 31 (wt=5) [] count(A,nil) = z. % 15.32/15.74 36 (wt=5) [] eq2(bfalse,btrue) = bfalse. % 15.32/15.74 37 (wt=5) [] eq2(btrue,bfalse) = bfalse. % 15.32/15.74 41 (wt=5) [] eq(A,A) = btrue. % 15.32/15.74 42 (wt=5) [] eq2(A,A) = btrue. % 15.32/15.74 15 (wt=6) [] leqNat(s(A),z) = bfalse. % 15.32/15.74 39 (wt=6) [] eq(z,s(A)) = bfalse. % 15.32/15.74 40 (wt=6) [] eq(s(A),z) = bfalse. % 15.32/15.74 11 (wt=7) [] splitAtNat(z,A) = pair2(nil,A). % 15.32/15.74 43 (wt=7) [] -(eq2(prop_msort_permutation_wrong2(A,B),bfalse) = btrue). % 15.32/15.74 12 (wt=8) [] splitAtNat(s(A),nil) = pair2(nil,nil). % 15.32/15.74 21 (wt=8) [] lengthNat(cons(A,B)) = s(lengthNat(B)). % 15.32/15.74 22 (wt=8) [flip(21)] s(lengthNat(A)) = lengthNat(cons(B,A)). % 15.32/15.74 27 (wt=8) [] div2(s(s(A))) = s(div2(A)). % 15.32/15.74 29 (wt=8) [] msort(cons(A,nil)) = cons(A,nil). % 15.32/15.74 9 (wt=9) [] aux4(A,B,C,bfalse) = count(A,C). % 15.32/15.74 10 (wt=9) [flip(9)] count(A,B) = aux4(A,C,B,bfalse). % 15.32/15.74 16 (wt=9) [] leqNat(s(A),s(B)) = leqNat(A,B). % 15.32/15.74 18 (wt=9) [] merge(cons(A,B),nil) = cons(A,B). % 15.32/15.74 38 (wt=9) [] eq(s(A),s(B)) = eq(A,B). % 15.32/15.74 7 (wt=10) [] aux4(A,B,C,btrue) = s(count(A,C)). % 15.32/15.74 8 (wt=10) [flip(7)] s(count(A,B)) = aux4(A,C,B,btrue). % 15.32/15.74 1 (wt=13) [] aux(A,B,C,pair2(D,E)) = pair2(cons(B,D),E). % 15.32/15.74 2 (wt=13) [flip(1)] pair2(cons(A,B),C) = aux(D,A,E,pair2(B,C)). % 15.32/15.74 5 (wt=13) [] aux3(A,B,C,pair2(D,E)) = merge(msort(D),msort(E)). % 15.32/15.74 6 (wt=13) [flip(5)] merge(msort(A),msort(B)) = aux3(C,D,E,pair2(A,B)). % 15.32/15.74 32 (wt=13) [] count(A,cons(B,C)) = aux4(A,B,C,eq(B,A)). % 15.32/15.74 33 (wt=13) [flip(32)] aux4(A,B,C,eq(B,A)) = count(A,cons(B,C)). % 15.32/15.74 3 (wt=14) [flip(1)] cons(A,merge(B,cons(C,D))) = aux2(A,B,C,D,btrue). % 15.32/15.74 4 (wt=14) [flip(1)] cons(A,merge(cons(B,C),D)) = aux2(B,C,A,D,bfalse). % 15.32/15.74 13 (wt=14) [] splitAtNat(s(A),cons(B,C)) = aux(A,B,C,splitAtNat(A,C)). % 15.32/15.74 19 (wt=16) [] merge(cons(A,B),cons(C,D)) = aux2(A,B,C,D,leqNat(A,C)). % 15.32/15.74 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.32/15.74 34 (wt=26) [] prop_msort_permutation_wrong2(A,B) = impl(eq2(leqNat(count(B,A),s(s(s(s(s(z)))))),bfalse),eq(count(s(B),A),count(B,msort(A)))). % 15.32/15.74 35 (wt=26) [flip(34)] impl(eq2(leqNat(count(A,B),s(s(s(s(s(z)))))),bfalse),eq(count(s(A),B),count(A,msort(B)))) = prop_msort_permutation_wrong2(B,A). % 15.32/15.74 end_of_list. % 15.32/15.74 % 15.32/15.74 Demodulators: % 15.32/15.74 3 (wt=14) [flip(1)] cons(A,merge(B,cons(C,D))) = aux2(A,B,C,D,btrue). % 15.32/15.74 4 (wt=14) [flip(1)] cons(A,merge(cons(B,C),D)) = aux2(B,C,A,D,bfalse). % 15.32/15.74 11 (wt=7) [] splitAtNat(z,A) = pair2(nil,A). % 15.32/15.74 12 (wt=8) [] splitAtNat(s(A),nil) = pair2(nil,nil). % 15.32/15.74 13 (wt=14) [] splitAtNat(s(A),cons(B,C)) = aux(A,B,C,splitAtNat(A,C)). % 15.32/15.74 14 (wt=5) [] leqNat(z,A) = btrue. % 15.32/15.74 15 (wt=6) [] leqNat(s(A),z) = bfalse. % 15.32/15.74 16 (wt=9) [] leqNat(s(A),s(B)) = leqNat(A,B). % 15.32/15.74 17 (wt=5) [] merge(nil,A) = A. % 15.32/15.74 18 (wt=9) [] merge(cons(A,B),nil) = cons(A,B). % 15.32/15.74 19 (wt=16) [] merge(cons(A,B),cons(C,D)) = aux2(A,B,C,D,leqNat(A,C)). % 15.32/15.74 20 (wt=4) [] lengthNat(nil) = z. % 15.32/15.74 23 (wt=5) [] impl(btrue,A) = A. % 15.32/15.74 24 (wt=5) [] impl(bfalse,A) = btrue. % 15.32/15.74 25 (wt=4) [] div2(z) = z. % 15.32/15.74 26 (wt=5) [] div2(s(z)) = z. % 15.32/15.74 27 (wt=8) [] div2(s(s(A))) = s(div2(A)). % 15.32/15.74 28 (wt=4) [] msort(nil) = nil. % 15.32/15.74 29 (wt=8) [] msort(cons(A,nil)) = cons(A,nil). % 15.32/15.74 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.32/15.74 31 (wt=5) [] count(A,nil) = z. % 15.32/15.74 36 (wt=5) [] eq2(bfalse,btrue) = bfalse. % 15.32/15.74 37 (wt=5) [] eq2(btrue,bfalse) = bfalse. % 15.32/15.74 38 (wt=9) [] eq(s(A),s(B)) = eq(A,B). % 15.32/15.74 39 (wt=6) [] eq(z,s(A)) = bfalse. % 15.32/15.74 40 (wt=6) [] eq(s(A),z) = bfalse. % 15.32/15.74 41 (wt=5) [] eq(A,A) = btrue. % 15.32/15.74 42 (wt=5) [] eq2(A,A) = btrue. % 15.32/15.74 end_of_list. % 15.32/15.74 % 15.32/15.74 Passive: % 15.32/15.74 end_of_list. % 15.32/15.74 % 15.32/15.74 ------------- memory usage ------------ % 15.32/15.74 Memory dynamically allocated (tp_alloc): 63964. % 15.32/15.74 type (bytes each) gets frees in use avail bytes % 15.32/15.74 sym_ent ( 96) 83 0 83 0 7.8 K % 15.32/15.74 term ( 16) 3016692 2047441 969251 4 18799.1 K % 15.32/15.74 gen_ptr ( 8) 4659884 406250 4253634 0 33231.5 K % 15.32/15.74 context ( 808) 13418632 % 15.32/15.74 % 15.32/15.74 ********** ABNORMAL END ********** % 15.32/15.74 ********** in tp_alloc, max_mem parameter exceeded. % 15.32/15.74 13418630 2 5 5.5 K % 15.32/15.74 trail ( 12) 51094 51094 0 12 0.1 K % 15.32/15.74 bt_node ( 68) 6412132 6412129 3 30 2.2 K % 15.32/15.74 ac_position (285432) 0 0 0 0 0.0 K % 15.32/15.74 ac_match_pos (14044) 0 0 0 0 0.0 K % 15.32/15.74 ac_match_free_vars_pos (4020) % 15.32/15.74 0 0 0 0 0.0 K % 15.32/15.74 discrim ( 12) 554134 34209 519925 0 6092.9 K % 15.32/15.74 flat ( 40) 6384528 6384528 0 90 3.5 K % 15.32/15.74 discrim_pos ( 12) 95972 95972 0 1 0.0 K % 15.32/15.74 fpa_head ( 12) 68433 0 68433 0 801.9 K % 15.32/15.74 fpa_tree ( 28) 96252 96252 0 27 0.7 K % 15.32/15.74 fpa_pos ( 36) 42132 42132 0 1 0.0 K % 15.32/15.74 literal ( 12) 158806 125089 33717 0 395.1 K % 15.32/15.74 clause ( 24) 158806 125089 33717 0 790.2 K % 15.32/15.74 list ( 12) 8475 8419 56 3 0.7 K % 15.32/15.74 list_pos ( 20) 115265 14050 101215 0 1976.9 K % 15.32/15.74 pair_index ( 40) 2 0 2 0 0.1 K % 15.32/15.74 % 15.32/15.74 -------------- statistics ------------- % 15.32/15.74 Clauses input 36 % 15.32/15.74 Usable input 0 % 15.32/15.74 Sos input 36 % 15.32/15.74 Demodulators input 0 % 15.32/15.74 Passive input 0 % 15.32/15.74 % 15.32/15.74 Processed BS (before search) 50 % 15.32/15.74 Forward subsumed BS 7 % 15.32/15.74 Kept BS 43 % 15.32/15.74 New demodulators BS 28 % 15.32/15.74 Back demodulated BS 0 % 15.32/15.75 % 15.32/15.75 Clauses or pairs given 928270 % 15.32/15.75 Clauses generated 91963 % 15.32/15.75 Forward subsumed 58290 % 15.32/15.75 Deleted by weight 0 % 15.32/15.75 Deleted by variable count 0 % 15.32/15.75 Kept 33673 % 15.32/15.75 New demodulators 8388 % 15.32/15.75 Back demodulated 2832 % 15.32/15.75 Ordered paramod prunes 0 % 15.32/15.75 Basic paramod prunes 3544716 % 15.32/15.75 Prime paramod prunes 4 % 15.32/15.75 Semantic prunes 0 % 15.32/15.75 % 15.32/15.75 Rewrite attmepts 1551224 % 15.32/15.75 Rewrites 69543 % 15.32/15.75 % 15.32/15.75 FPA overloads 0 % 15.32/15.75 FPA underloads 0 % 15.32/15.75 % 15.32/15.75 Usable size 0 % 15.32/15.75 Sos size 30884 % 15.32/15.75 Demodulators size 5731 % 15.32/15.75 Passive size 0 % 15.32/15.75 Disabled size 2832 % 15.32/15.75 % 15.32/15.75 Proofs found 0 % 15.32/15.75 % 15.32/15.75 ----------- times (seconds) ----------- Tue May 5 11:22:46 2026 % 15.32/15.75 % 15.32/15.75 user CPU time 11.36 (0 hr, 0 min, 11 sec) % 15.32/15.75 system CPU time 3.30 (0 hr, 0 min, 3 sec) % 15.32/15.75 wall-clock time 15 (0 hr, 0 min, 15 sec) % 15.32/15.75 input time 0.00 % 15.32/15.75 paramodulation time 1.30 % 15.32/15.75 demodulation time 0.24 % 15.32/15.75 orient time 0.21 % 15.32/15.75 weigh time 0.05 % 15.32/15.75 forward subsume time 0.10 % 15.32/15.75 back demod find time 0.12 % 15.32/15.75 conflict time 0.02 % 15.32/15.75 LRPO time 0.11 % 15.32/15.75 store clause time 7.20 % 15.32/15.75 disable clause time 0.67 % 15.32/15.75 prime paramod time 0.09 % 15.32/15.75 semantics time 0.00 % 15.32/15.75 % 15.32/15.75 EQP interrupted %------------------------------------------------------------------------------