%------------------------------------------------------------------------------ % File : EQP---0.9e % Problem : SWX198-1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : tptp2X_and_run_eqp %s % Computer : n024.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 0.42s 12.60s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.06 % Problem : SWX198-1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.06 % Command : tptp2X_and_run_eqp %s % 0.06/0.24 % Computer : n024.cluster.edu % 0.06/0.24 % Model : x86_64 x86_64 % 0.06/0.24 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.06/0.24 % Memory : 8042.1875MB % 0.06/0.24 % OS : Linux 3.10.0-693.el7.x86_64 % 0.06/0.24 % CPULimit : 300 % 0.06/0.24 % WCLimit : 300 % 0.06/0.24 % DateTime : Tue May 5 06:09:11 EDT 2026 % 0.06/0.25 % CPUTime : % 0.42/0.80 ----- EQP 0.9e, May 2009 ----- % 0.42/0.80 The job began on n024.cluster.edu, Tue May 5 06:09:12 2026 % 0.42/0.80 The command was "./eqp09e". % 0.42/0.80 % 0.42/0.80 set(prolog_style_variables). % 0.42/0.80 set(lrpo). % 0.42/0.80 set(basic_paramod). % 0.42/0.80 set(functional_subsume). % 0.42/0.80 set(ordered_paramod). % 0.42/0.80 set(prime_paramod). % 0.42/0.80 set(para_pairs). % 0.42/0.80 assign(pick_given_ratio,4). % 0.42/0.80 clear(print_kept). % 0.42/0.80 clear(print_new_demod). % 0.42/0.80 clear(print_back_demod). % 0.42/0.80 clear(print_given). % 0.42/0.80 assign(max_mem,64000). % 0.42/0.80 end_of_commands. % 0.42/0.80 % 0.42/0.80 Usable: % 0.42/0.80 end_of_list. % 0.42/0.80 % 0.42/0.80 Sos: % 0.42/0.80 0 (wt=-1) [] ltNat(z,z) = bfalse. % 0.42/0.80 0 (wt=-1) [] ltNat(z,s(A)) = btrue. % 0.42/0.80 0 (wt=-1) [] ltNat(s(A),z) = bfalse. % 0.42/0.80 0 (wt=-1) [] ltNat(s(A),s(B)) = ltNat(A,B). % 0.42/0.80 0 (wt=-1) [] leqNat(z,A) = btrue. % 0.42/0.80 0 (wt=-1) [] leqNat(s(A),z) = bfalse. % 0.42/0.80 0 (wt=-1) [] leqNat(s(A),s(B)) = leqNat(A,B). % 0.42/0.80 0 (wt=-1) [] lengthNat(nil) = z. % 0.42/0.80 0 (wt=-1) [] lengthNat(cons(A,B)) = s(lengthNat(B)). % 0.42/0.80 0 (wt=-1) [] impl(btrue,A) = A. % 0.42/0.80 0 (wt=-1) [] impl(bfalse,A) = btrue. % 0.42/0.80 0 (wt=-1) [] append(nil,A) = A. % 0.42/0.80 0 (wt=-1) [] append(cons(A,B),C) = cons(A,append(B,C)). % 0.42/0.80 0 (wt=-1) [] rev(nil) = nil. % 0.42/0.80 0 (wt=-1) [] rev(cons(A,B)) = append(rev(B),cons(A,nil)). % 0.42/0.80 0 (wt=-1) [] andb(btrue,A) = A. % 0.42/0.80 0 (wt=-1) [] andb(bfalse,A) = bfalse. % 0.42/0.80 0 (wt=-1) [] usorted(nil) = btrue. % 0.42/0.80 0 (wt=-1) [] usorted(cons(A,nil)) = btrue. % 0.42/0.80 0 (wt=-1) [] usorted(cons(A,cons(B,C))) = andb(ltNat(A,B),usorted(cons(B,C))). % 0.42/0.80 0 (wt=-1) [] allsmall(A,nil) = btrue. % 0.42/0.80 0 (wt=-1) [] allsmall(A,cons(B,C)) = andb(ltNat(B,A),allsmall(A,C)). % 0.42/0.80 0 (wt=-1) [] pallsmall(A) = impl(eq2(usorted(rev(A)),btrue),impl(eq2(allsmall(s(z),A),btrue),eq2(leqNat(lengthNat(A),s(s(z))),btrue))). % 0.42/0.80 0 (wt=-1) [] eq2(bfalse,btrue) = bfalse. % 0.42/0.80 0 (wt=-1) [] eq2(btrue,bfalse) = bfalse. % 0.42/0.80 0 (wt=-1) [] eq(s(A),s(B)) = eq(A,B). % 0.42/0.80 0 (wt=-1) [] eq(z,s(A)) = bfalse. % 0.42/0.80 0 (wt=-1) [] eq(s(A),z) = bfalse. % 0.42/0.80 0 (wt=-1) [] eq(A,A) = btrue. % 0.42/0.80 0 (wt=-1) [] eq2(A,A) = btrue. % 0.42/0.80 0 (wt=-1) [] -(eq2(pallsmall(A),bfalse) = btrue). % 0.42/0.80 end_of_list. % 0.42/0.80 % 0.42/0.80 Demodulators: % 0.42/0.80 end_of_list. % 0.42/0.80 % 0.42/0.80 Passive: % 0.42/0.80 end_of_list. % 0.42/0.80 % 0.42/0.80 Starting to process input. % 0.42/0.80 % 0.42/0.80 ** KEPT: 1 (wt=5) [] ltNat(z,z) = bfalse. % 0.42/0.80 1 is a new demodulator. % 0.42/0.80 % 0.42/0.80 ** KEPT: 2 (wt=6) [] ltNat(z,s(A)) = btrue. % 0.42/0.80 2 is a new demodulator. % 0.42/0.80 % 0.42/0.80 ** KEPT: 3 (wt=6) [] ltNat(s(A),z) = bfalse. % 0.42/0.80 3 is a new demodulator. % 0.42/0.80 % 0.42/0.80 ** KEPT: 4 (wt=9) [] ltNat(s(A),s(B)) = ltNat(A,B). % 0.42/0.80 4 is a new demodulator. % 0.42/0.80 % 0.42/0.80 ** KEPT: 5 (wt=5) [] leqNat(z,A) = btrue. % 0.42/0.80 5 is a new demodulator. % 0.42/0.80 % 0.42/0.80 ** KEPT: 6 (wt=6) [] leqNat(s(A),z) = bfalse. % 0.42/0.80 6 is a new demodulator. % 0.42/0.80 % 0.42/0.80 ** KEPT: 7 (wt=9) [] leqNat(s(A),s(B)) = leqNat(A,B). % 0.42/0.80 7 is a new demodulator. % 0.42/0.80 % 0.42/0.80 ** KEPT: 8 (wt=4) [] lengthNat(nil) = z. % 0.42/0.80 8 is a new demodulator. % 0.42/0.80 % 0.42/0.80 ** KEPT: 9 (wt=8) [] lengthNat(cons(A,B)) = s(lengthNat(B)). % 0.42/0.80 % 0.42/0.80 ** KEPT: 10 (wt=8) [flip(9)] s(lengthNat(A)) = lengthNat(cons(B,A)). % 0.42/0.80 clause forward subsumed: 0 (wt=8) [flip(10)] lengthNat(cons(B,A)) = s(lengthNat(A)). % 0.42/0.80 % 0.42/0.80 ** KEPT: 11 (wt=5) [] impl(btrue,A) = A. % 0.42/0.80 11 is a new demodulator. % 0.42/0.80 % 0.42/0.80 ** KEPT: 12 (wt=5) [] impl(bfalse,A) = btrue. % 0.42/0.80 12 is a new demodulator. % 0.42/0.80 % 0.42/0.80 ** KEPT: 13 (wt=5) [] append(nil,A) = A. % 0.42/0.80 13 is a new demodulator. % 0.42/0.80 % 0.42/0.80 ** KEPT: 14 (wt=11) [flip(1)] cons(A,append(B,C)) = append(cons(A,B),C). % 0.42/0.80 14 is a new demodulator. % 0.42/0.80 % 0.42/0.80 ** KEPT: 15 (wt=4) [] rev(nil) = nil. % 0.42/0.80 15 is a new demodulator. % 0.42/0.80 % 0.42/0.80 ** KEPT: 16 (wt=11) [] rev(cons(A,B)) = append(rev(B),cons(A,nil)). % 0.42/0.80 16 is a new demodulator. % 0.42/0.80 % 0.42/0.80 ** KEPT: 17 (wt=5) [] andb(btrue,A) = A. % 0.42/0.80 17 is a new demodulator. % 0.42/0.80 % 0.42/0.80 ** KEPT: 18 (wt=5) [] andb(bfalse,A) = bfalse. % 0.42/0.80 18 is a new demodulator. % 0.42/0.80 % 0.42/0.80 ** KEPT: 19 (wt=4) [] usorted(nil) = btrue. % 0.42/0.80 19 is a new demodulator. % 0.42/0.80 % 0.42/0.80 ** KEPT: 20 (wt=6) [] usorted(cons(A,nil)) = btrue. % 0.42/0.80 20 is a new demodulator. % 0.42/0.80 % 0.42/0.80 ** KEPT: 21 (wt=15) [] usorted(cons(A,cons(B,C))) = andb(ltNat(A,B),usorted(cons(B,C))). % 0.42/0.80 21 is a new demodulator. % 0.42/0.80 % 0.42/0.80 ** KEPT: 22 (wt=5) [] allsmall(A,nil) = btrue. % 0.42/0.80 22 is a new demodulator. % 0.42/0.80 % 0.42/0.80 ** KEPT: 23 (wt=13) [] allsmall(A,cons(B,C)) = andb(ltNat(B,A),allsmall(A,C)). % 0.42/0.80 % 0.42/0.80 ** KEPT: 24 (wt=13) [flip(23)] andb(ltNat(A,B),allsmall(B,C)) = allsmall(B,cons(A,C)). % 0.42/0.80 clause forward subsumed: 0 (wt=13) [flip(24)] allsmall(B,cons(A,C)) = andb(ltNat(A,B),allsmall(B,C)). % 0.42/0.80 % 0.42/0.80 ** KEPT: 25 (wt=24) [flip(1)] impl(eq2(usorted(rev(A)),btrue),impl(eq2(allsmall(s(z),A),btrue),eq2(leqNat(lengthNat(A),s(s(z))),btrue))) = pallsmall(A). % 0.42/0.80 25 is a new demodulator. % 0.42/0.80 % 0.42/0.80 ** KEPT: 26 (wt=5) [] eq2(bfalse,btrue) = bfalse. % 12.11/12.59 26 is a new demodulator. % 12.11/12.59 % 12.11/12.59 ** KEPT: 27 (wt=5) [] eq2(btrue,bfalse) = bfalse. % 12.11/12.59 27 is a new demodulator. % 12.11/12.59 % 12.11/12.59 ** KEPT: 28 (wt=9) [] eq(s(A),s(B)) = eq(A,B). % 12.11/12.59 28 is a new demodulator. % 12.11/12.59 % 12.11/12.59 ** KEPT: 29 (wt=6) [] eq(z,s(A)) = bfalse. % 12.11/12.59 29 is a new demodulator. % 12.11/12.59 % 12.11/12.59 ** KEPT: 30 (wt=6) [] eq(s(A),z) = bfalse. % 12.11/12.59 30 is a new demodulator. % 12.11/12.59 % 12.11/12.59 ** KEPT: 31 (wt=5) [] eq(A,A) = btrue. % 12.11/12.59 31 is a new demodulator. % 12.11/12.59 % 12.11/12.59 ** KEPT: 32 (wt=5) [] eq2(A,A) = btrue. % 12.11/12.59 32 is a new demodulator. % 12.11/12.59 % 12.11/12.59 ** KEPT: 33 (wt=6) [] -(eq2(pallsmall(A),bfalse) = btrue). % 12.11/12.59 % 12.11/12.59 After processing input: % 12.11/12.59 % 12.11/12.59 Usable: % 12.11/12.59 end_of_list. % 12.11/12.59 % 12.11/12.59 Sos: % 12.11/12.59 8 (wt=4) [] lengthNat(nil) = z. % 12.11/12.59 15 (wt=4) [] rev(nil) = nil. % 12.11/12.59 19 (wt=4) [] usorted(nil) = btrue. % 12.11/12.59 1 (wt=5) [] ltNat(z,z) = bfalse. % 12.11/12.59 5 (wt=5) [] leqNat(z,A) = btrue. % 12.11/12.59 11 (wt=5) [] impl(btrue,A) = A. % 12.11/12.59 12 (wt=5) [] impl(bfalse,A) = btrue. % 12.11/12.59 13 (wt=5) [] append(nil,A) = A. % 12.11/12.59 17 (wt=5) [] andb(btrue,A) = A. % 12.11/12.59 18 (wt=5) [] andb(bfalse,A) = bfalse. % 12.11/12.59 22 (wt=5) [] allsmall(A,nil) = btrue. % 12.11/12.59 26 (wt=5) [] eq2(bfalse,btrue) = bfalse. % 12.11/12.59 27 (wt=5) [] eq2(btrue,bfalse) = bfalse. % 12.11/12.59 31 (wt=5) [] eq(A,A) = btrue. % 12.11/12.59 32 (wt=5) [] eq2(A,A) = btrue. % 12.11/12.59 2 (wt=6) [] ltNat(z,s(A)) = btrue. % 12.11/12.59 3 (wt=6) [] ltNat(s(A),z) = bfalse. % 12.11/12.59 6 (wt=6) [] leqNat(s(A),z) = bfalse. % 12.11/12.59 20 (wt=6) [] usorted(cons(A,nil)) = btrue. % 12.11/12.59 29 (wt=6) [] eq(z,s(A)) = bfalse. % 12.11/12.59 30 (wt=6) [] eq(s(A),z) = bfalse. % 12.11/12.59 33 (wt=6) [] -(eq2(pallsmall(A),bfalse) = btrue). % 12.11/12.59 9 (wt=8) [] lengthNat(cons(A,B)) = s(lengthNat(B)). % 12.11/12.59 10 (wt=8) [flip(9)] s(lengthNat(A)) = lengthNat(cons(B,A)). % 12.11/12.59 4 (wt=9) [] ltNat(s(A),s(B)) = ltNat(A,B). % 12.11/12.59 7 (wt=9) [] leqNat(s(A),s(B)) = leqNat(A,B). % 12.11/12.59 28 (wt=9) [] eq(s(A),s(B)) = eq(A,B). % 12.11/12.59 14 (wt=11) [flip(1)] cons(A,append(B,C)) = append(cons(A,B),C). % 12.11/12.59 16 (wt=11) [] rev(cons(A,B)) = append(rev(B),cons(A,nil)). % 12.11/12.59 23 (wt=13) [] allsmall(A,cons(B,C)) = andb(ltNat(B,A),allsmall(A,C)). % 12.11/12.59 24 (wt=13) [flip(23)] andb(ltNat(A,B),allsmall(B,C)) = allsmall(B,cons(A,C)). % 12.11/12.59 21 (wt=15) [] usorted(cons(A,cons(B,C))) = andb(ltNat(A,B),usorted(cons(B,C))). % 12.11/12.59 25 (wt=24) [flip(1)] impl(eq2(usorted(rev(A)),btrue),impl(eq2(allsmall(s(z),A),btrue),eq2(leqNat(lengthNat(A),s(s(z))),btrue))) = pallsmall(A). % 12.11/12.59 end_of_list. % 12.11/12.59 % 12.11/12.59 Demodulators: % 12.11/12.59 1 (wt=5) [] ltNat(z,z) = bfalse. % 12.11/12.59 2 (wt=6) [] ltNat(z,s(A)) = btrue. % 12.11/12.59 3 (wt=6) [] ltNat(s(A),z) = bfalse. % 12.11/12.59 4 (wt=9) [] ltNat(s(A),s(B)) = ltNat(A,B). % 12.11/12.59 5 (wt=5) [] leqNat(z,A) = btrue. % 12.11/12.59 6 (wt=6) [] leqNat(s(A),z) = bfalse. % 12.11/12.59 7 (wt=9) [] leqNat(s(A),s(B)) = leqNat(A,B). % 12.11/12.59 8 (wt=4) [] lengthNat(nil) = z. % 12.11/12.59 11 (wt=5) [] impl(btrue,A) = A. % 12.11/12.59 12 (wt=5) [] impl(bfalse,A) = btrue. % 12.11/12.59 13 (wt=5) [] append(nil,A) = A. % 12.11/12.59 14 (wt=11) [flip(1)] cons(A,append(B,C)) = append(cons(A,B),C). % 12.11/12.59 15 (wt=4) [] rev(nil) = nil. % 12.11/12.59 16 (wt=11) [] rev(cons(A,B)) = append(rev(B),cons(A,nil)). % 12.11/12.59 17 (wt=5) [] andb(btrue,A) = A. % 12.11/12.59 18 (wt=5) [] andb(bfalse,A) = bfalse. % 12.11/12.59 19 (wt=4) [] usorted(nil) = btrue. % 12.11/12.59 20 (wt=6) [] usorted(cons(A,nil)) = btrue. % 12.11/12.59 21 (wt=15) [] usorted(cons(A,cons(B,C))) = andb(ltNat(A,B),usorted(cons(B,C))). % 12.11/12.59 22 (wt=5) [] allsmall(A,nil) = btrue. % 12.11/12.59 25 (wt=24) [flip(1)] impl(eq2(usorted(rev(A)),btrue),impl(eq2(allsmall(s(z),A),btrue),eq2(leqNat(lengthNat(A),s(s(z))),btrue))) = pallsmall(A). % 12.11/12.59 26 (wt=5) [] eq2(bfalse,btrue) = bfalse. % 12.11/12.59 27 (wt=5) [] eq2(btrue,bfalse) = bfalse. % 12.11/12.59 28 (wt=9) [] eq(s(A),s(B)) = eq(A,B). % 12.11/12.59 29 (wt=6) [] eq(z,s(A)) = bfalse. % 12.11/12.59 30 (wt=6) [] eq(s(A),z) = bfalse. % 12.11/12.59 31 (wt=5) [] eq(A,A) = btrue. % 12.11/12.59 32 (wt=5) [] eq2(A,A) = btrue. % 12.11/12.59 end_of_list. % 12.11/12.59 % 12.11/12.59 Passive: % 12.11/12.59 end_of_list. % 12.11/12.59 % 12.11/12.59 ------------- memory usage ------------ % 12.11/12.59 Memory dynamically allocated (tp_alloc): 63964. % 12.11/12.59 type (bytes each) gets frees in use avail bytes % 12.11/12.59 sym_ent ( 96) 74 0 74 0 6.9 K % 12.11/12.59 term ( 16) 5017785 4121637 896148 1 17400.8 K % 12.11/12.59 gen_ptr ( 8) 5364644 545248 4819396 0 37651.5 K % 12.11/12.59 context ( 808) 16721855 16721853 2 9 8.7 K % 12.11/12.59 trail ( 12) 31805 31805 0 10 0.1 K % 12.11/12.59 bt_node ( 68) 7663795 7663791 4 40 2.9 K % 12.11/12.59 ac_position (285432) 0 0 0 0 0.0 K % 12.11/12.59 ac_match_pos (14044) 0 0 0 0 0.0 K % 0.42/12.60 ac_match_free_vars_pos (4020) % 0.42/12.60 0 0 0 0 0.0 K % 0.42/12.60 discrim ( 12) 462657 16460 446197 0 5228.9 K % 0.42/12.60 flat ( 40) 10218754 10218754 0 94 3.7 K % 0.42/12.60 discrim_pos ( 12) 235598 235598 0 1 0.0 K % 0.42/12.60 fpa_head ( 12) 21649 0 21649 0 253.7 K % 0.42/12.60 fpa_tree ( 28) 56490 56490 0 37 1.0 % 0.42/12.60 % 0.42/12.60 ********** ABNORMAL END ********** % 0.42/12.60 ********** in tp_alloc, max_mem parameter exceeded. % 0.42/12.60 K % 0.42/12.60 fpa_pos ( 36) 30858 30858 0 1 0.0 K % 0.42/12.60 literal ( 12) 186018 159866 26152 1 306.5 K % 0.42/12.60 clause ( 24) 186018 159866 26152 1 613.0 K % 0.42/12.60 list ( 12) 4765 4709 56 3 0.7 K % 0.42/12.60 list_pos ( 20) 86179 6731 79448 0 1551.7 K % 0.42/12.60 pair_index ( 40) 2 0 2 0 0.1 K % 0.42/12.60 % 0.42/12.60 -------------- statistics ------------- % 0.42/12.60 Clauses input 31 % 0.42/12.60 Usable input 0 % 0.42/12.60 Sos input 31 % 0.42/12.60 Demodulators input 0 % 0.42/12.60 Passive input 0 % 0.42/12.60 % 0.42/12.60 Processed BS (before search) 35 % 0.42/12.60 Forward subsumed BS 2 % 0.42/12.60 Kept BS 33 % 0.42/12.60 New demodulators BS 28 % 0.42/12.60 Back demodulated BS 0 % 0.42/12.60 % 0.42/12.60 Clauses or pairs given 811370 % 0.42/12.60 Clauses generated 104818 % 0.42/12.60 Forward subsumed 78699 % 0.42/12.60 Deleted by weight 0 % 0.42/12.60 Deleted by variable count 0 % 0.42/12.60 Kept 26119 % 0.42/12.60 New demodulators 4678 % 0.42/12.60 Back demodulated 1489 % 0.42/12.60 Ordered paramod prunes 0 % 0.42/12.60 Basic paramod prunes 3330327 % 0.42/12.60 Prime paramod prunes 1 % 0.42/12.60 Semantic prunes 0 % 0.42/12.60 % 0.42/12.60 Rewrite attmepts 2611505 % 0.42/12.60 Rewrites 191352 % 0.42/12.60 % 0.42/12.60 FPA overloads 0 % 0.42/12.60 FPA underloads 0 % 0.42/12.60 % 0.42/12.60 Usable size 0 % 0.42/12.60 Sos size 24663 % 0.42/12.60 Demodulators size 3970 % 0.42/12.60 Passive size 0 % 0.42/12.60 Disabled size 1489 % 0.42/12.60 % 0.42/12.60 Proofs found 0 % 0.42/12.60 % 0.42/12.60 ----------- times (seconds) ----------- Tue May 5 06:09:24 2026 % 0.42/12.60 % 0.42/12.60 user CPU time 8.30 (0 hr, 0 min, 8 sec) % 0.42/12.60 system CPU time 3.50 (0 hr, 0 min, 3 sec) % 0.42/12.60 wall-clock time 12 (0 hr, 0 min, 12 sec) % 0.42/12.60 input time 0.00 % 0.42/12.60 paramodulation time 1.31 % 0.42/12.60 demodulation time 0.34 % 0.42/12.60 orient time 0.26 % 0.42/12.60 weigh time 0.05 % 0.42/12.60 forward subsume time 0.12 % 0.42/12.60 back demod find time 0.15 % 0.42/12.60 conflict time 0.03 % 0.42/12.60 LRPO time 0.13 % 0.42/12.60 store clause time 4.45 % 0.42/12.60 disable clause time 0.26 % 0.42/12.60 prime paramod time 0.09 % 0.42/12.60 semantics time 0.00 % 0.42/12.60 % 0.42/12.60 EQP interrupted %------------------------------------------------------------------------------