%------------------------------------------------------------------------------ % File : Prover9---1109a % Problem : SWX208+1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : tptp2X_and_run_prover9 %d %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 : Wed Apr 29 02:38:05 PM UTC 2026 % Result : Timeout 299.79s 300.03s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWX208+1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.12 % Command : tptp2X_and_run_prover9 %d %s % 0.16/0.33 % Computer : n014.cluster.edu % 0.16/0.33 % Model : x86_64 x86_64 % 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.33 % Memory : 8042.1875MB % 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.33 % CPULimit : 300 % 0.16/0.33 % WCLimit : 300 % 0.16/0.33 % DateTime : Wed Apr 29 01:02:05 EDT 2026 % 0.16/0.33 % CPUTime : % 0.80/1.08 ============================== Prover9 =============================== % 0.80/1.08 Prover9 (32) version 2009-11A, November 2009. % 0.80/1.08 Process 26521 was started by sandbox on n014.cluster.edu, % 0.80/1.08 Wed Apr 29 01:02:06 2026 % 0.80/1.08 The command was "/export/starexec/sandbox/solver/bin/prover9 -t 300 -f /tmp/Prover9_26368_n014.cluster.edu". % 0.80/1.08 ============================== end of head =========================== % 0.80/1.08 % 0.80/1.08 ============================== INPUT ================================= % 0.80/1.08 % 0.80/1.08 % Reading from file /tmp/Prover9_26368_n014.cluster.edu % 0.80/1.08 % 0.80/1.08 set(prolog_style_variables). % 0.80/1.08 set(auto2). % 0.80/1.08 % set(auto2) -> set(auto). % 0.80/1.08 % set(auto) -> set(auto_inference). % 0.80/1.08 % set(auto) -> set(auto_setup). % 0.80/1.08 % set(auto_setup) -> set(predicate_elim). % 0.80/1.08 % set(auto_setup) -> assign(eq_defs, unfold). % 0.80/1.08 % set(auto) -> set(auto_limits). % 0.80/1.08 % set(auto_limits) -> assign(max_weight, "100.000"). % 0.80/1.08 % set(auto_limits) -> assign(sos_limit, 20000). % 0.80/1.08 % set(auto) -> set(auto_denials). % 0.80/1.08 % set(auto) -> set(auto_process). % 0.80/1.08 % set(auto2) -> assign(new_constants, 1). % 0.80/1.08 % set(auto2) -> assign(fold_denial_max, 3). % 0.80/1.08 % set(auto2) -> assign(max_weight, "200.000"). % 0.80/1.08 % set(auto2) -> assign(max_hours, 1). % 0.80/1.08 % assign(max_hours, 1) -> assign(max_seconds, 3600). % 0.80/1.08 % set(auto2) -> assign(max_seconds, 0). % 0.80/1.08 % set(auto2) -> assign(max_minutes, 5). % 0.80/1.08 % assign(max_minutes, 5) -> assign(max_seconds, 300). % 0.80/1.08 % set(auto2) -> set(sort_initial_sos). % 0.80/1.08 % set(auto2) -> assign(sos_limit, -1). % 0.80/1.08 % set(auto2) -> assign(lrs_ticks, 3000). % 0.80/1.08 % set(auto2) -> assign(max_megs, 400). % 0.80/1.08 % set(auto2) -> assign(stats, some). % 0.80/1.08 % set(auto2) -> clear(echo_input). % 0.80/1.08 % set(auto2) -> set(quiet). % 0.80/1.08 % set(auto2) -> clear(print_initial_clauses). % 0.80/1.08 % set(auto2) -> clear(print_given). % 0.80/1.08 assign(lrs_ticks,-1). % 0.80/1.08 assign(sos_limit,10000). % 0.80/1.08 assign(order,kbo). % 0.80/1.08 set(lex_order_vars). % 0.80/1.08 clear(print_given). % 0.80/1.08 % 0.80/1.08 % formulas(sos). % not echoed (156 formulas) % 0.80/1.08 % 0.80/1.08 ============================== end of input ========================== % 0.80/1.08 % 0.80/1.08 % From the command line: assign(max_seconds, 300). % 0.80/1.08 % 0.80/1.08 ============================== PROCESS NON-CLAUSAL FORMULAS ========== % 0.80/1.08 % 0.80/1.08 % Formulas that are not ordinary clauses: % 0.80/1.08 1 (all X all X2 proj1pair(pair2(X,X2)) = X) # label(axiom_001) # label(axiom) # label(non_clause). [assumption]. % 0.80/1.08 2 (all X all X2 proj2pair(pair2(X,X2)) = X2) # label(axiom_002) # label(axiom) # label(non_clause). [assumption]. % 0.80/1.08 3 (all X all X2 head(cons(X,X2)) = X) # label(axiom_003) # label(axiom) # label(non_clause). [assumption]. % 0.80/1.08 4 (all X all X2 tail(cons(X,X2)) = X2) # label(axiom_004) # label(axiom) # label(non_clause). [assumption]. % 0.80/1.08 5 (all X all X2 nil != cons(X,X2)) # label(axiom_005) # label(axiom) # label(non_clause). [assumption]. % 0.80/1.08 6 (all X proj1S(s(X)) = X) # label(axiom_006) # label(axiom) # label(non_clause). [assumption]. % 0.80/1.08 7 (all X z != s(X)) # label(axiom_007) # label(axiom) # label(non_clause). [assumption]. % 0.80/1.08 8 (all X all X2 proj1Add(add(X,X2)) = X) # label(axiom_008) # label(axiom) # label(non_clause). [assumption]. % 0.80/1.08 9 (all X all X2 proj2Add(add(X,X2)) = X2) # label(axiom_009) # label(axiom) # label(non_clause). [assumption]. % 0.80/1.08 10 (all X all X2 proj1Mul(mul(X,X2)) = X) # label(axiom_010) # label(axiom) # label(non_clause). [assumption]. % 0.80/1.08 11 (all X all X2 proj2Mul(mul(X,X2)) = X2) # label(axiom_011) # label(axiom) # label(non_clause). [assumption]. % 0.80/1.08 12 (all X proj1Num(num(X)) = X) # label(axiom_012) # label(axiom) # label(non_clause). [assumption]. % 0.80/1.08 13 (all X all X2 x != add(X,X2)) # label(axiom_013) # label(axiom) # label(non_clause). [assumption]. % 0.80/1.08 14 (all X all X2 x != mul(X,X2)) # label(axiom_014) # label(axiom) # label(non_clause). [assumption]. % 0.80/1.08 15 (all X x != num(X)) # label(axiom_015) # label(axiom) # label(non_clause). [assumption]. % 0.80/1.08 16 (all X all X2 all X3 all X4 add(X,X2) != mul(X3,X4)) # label(axiom_016) # label(axiom) # label(non_clause). [assumption]. % 0.80/1.08 17 (all X all X2 all X3 add(X,X2) != num(X3)) # label(axiom_017) # label(axiom) # label(non_clause). [assumption]. % 0.80/1.08 18 (all X all X2 all X3 mul(X,X2) != num(X3)) # label(axiom_018) # label(axiom) # label(non_clause). [assumption]. % 0.80/1.08 19 (all X proj1Left(left(X)) = X) # label(axiom_019) # label(axiom) # label(non_clause). [assumption]. % 2.07/2.33 20 (all X proj1Right(right(X)) = X) # label(axiom_020) # label(axiom) # label(non_clause). [assumption]. % 2.07/2.33 21 (all X all X2 left(X) != right(X2)) # label(axiom_021) # label(axiom) # label(non_clause). [assumption]. % 2.07/2.33 22 (all Y append(nil,Y) = Y) # label(axiom_127) # label(axiom) # label(non_clause). [assumption]. % 2.07/2.33 23 (all Y all Z all Xs append(cons(Z,Xs),Y) = cons(Z,append(Xs,Y))) # label(axiom_128) # label(axiom) # label(non_clause). [assumption]. % 2.07/2.33 24 (all Z x2(z,s(Z)) = z) # label(axiom_130) # label(axiom) # label(non_clause). [assumption]. % 2.07/2.33 25 (all N x2(s(N),z) = s(N)) # label(axiom_131) # label(axiom) # label(non_clause). [assumption]. % 2.07/2.33 26 (all N all M x2(s(N),s(M)) = x2(N,M)) # label(axiom_132) # label(axiom) # label(non_clause). [assumption]. % 2.07/2.33 27 (all X9 min10(s(s(s(s(s(s(s(s(s(s(X9))))))))))) = right(x2(s(s(s(s(s(s(s(s(s(s(X9)))))))))),s(s(s(s(s(s(s(s(s(s(z))))))))))))) # label(axiom_143) # label(axiom) # label(non_clause). [assumption]. % 2.07/2.33 28 (all X all D (min10(X) = left(D) -> mod10(X) = pair2(D,z))) # label(axiom_144) # label(axiom) # label(non_clause). [assumption]. % 2.07/2.33 29 (all X all N all D1 all N2 (min10(X) = right(N) -> (mod10(N) = pair2(D1,N2) -> mod10(X) = pair2(D1,s(N2))))) # label(axiom_145) # label(axiom) # label(non_clause). [assumption]. % 2.07/2.33 30 (all X showNumnum(X,z) = X) # label(axiom_146) # label(axiom) # label(non_clause). [assumption]. % 2.07/2.33 31 (all X all Z all A1 all N (mod10(s(Z)) = pair2(A1,N) -> showNumnum(X,s(Z)) = showNumnum(cons(A1,X),N))) # label(axiom_147) # label(axiom) # label(non_clause). [assumption]. % 2.07/2.33 32 (all Y showNum(s(Y)) = showNumnum(nil,s(Y))) # label(axiom_149) # label(axiom) # label(non_clause). [assumption]. % 2.07/2.33 33 (all B all C show(add(B,C)) = append(show(B),append(cons(pLUS,nil),show(C)))) # label(axiom_151) # label(axiom) # label(non_clause). [assumption]. % 2.07/2.33 34 (all A3 all B2 show(mul(A3,B2)) = append(showF(A3),append(cons(mULT,nil),showF(B2)))) # label(axiom_152) # label(axiom) # label(non_clause). [assumption]. % 2.07/2.33 35 (all N show(num(N)) = showNum(N)) # label(axiom_153) # label(axiom) # label(non_clause). [assumption]. % 2.07/2.33 36 (all X (X != add(proj1Add(X),proj2Add(X)) -> showF(X) = show(X))) # label(axiom_154) # label(axiom) # label(non_clause). [assumption]. % 2.07/2.33 37 (all Y all Z showF(add(Y,Z)) = cons(pAR1,append(show(add(Y,Z)),cons(pAR2,nil)))) # label(axiom_155) # label(axiom) # label(non_clause). [assumption]. % 2.07/2.33 38 -(exists E show(E) = cons(pAR1,cons(pAR1,cons(cHARX,cons(pLUS,cons(dIG5,cons(pAR2,cons(pLUS,cons(dIG7,cons(pAR2,cons(mULT,cons(cHARX,nil)))))))))))) # label(goal_156) # label(negated_conjecture) # label(non_clause). [assumption]. % 2.07/2.33 % 2.07/2.33 ============================== end of process non-clausal formulas === % 2.07/2.33 % 2.07/2.33 ============================== PROCESS INITIAL CLAUSES =============== % 2.07/2.33 % 2.07/2.33 ============================== PREDICATE ELIMINATION ================= % 2.07/2.33 % 2.07/2.33 ============================== end predicate elimination ============= % 2.07/2.33 % 2.07/2.33 Auto_denials: (non-Horn, no changes). % 2.07/2.33 % 2.07/2.33 Term ordering decisions: % 2.07/2.33 Function symbol KB weights: z=1. nil=1. dIG0=1. cHARX=1. dIG1=1. dIG2=1. dIG3=1. dIG4=1. dIG5=1. dIG6=1. dIG7=1. dIG8=1. dIG9=1. mULT=1. pAR1=1. pAR2=1. pLUS=1. x=1. cons=1. append=1. add=1. pair2=1. x2=1. showNumnum=1. mul=1. s=1. min10=1. left=1. show=1. mod10=1. showF=1. right=1. showNum=1. num=1. proj1Add=1. proj2Add=1. head=1. proj1Left=1. proj1Mul=1. proj1Num=1. proj1Right=1. proj1S=1. proj1pair=1. proj2Mul=1. proj2pair=1. tail=1. % 2.07/2.33 % 2.07/2.33 ============================== end of process initial clauses ======== % 2.07/2.33 % 2.07/2.33 ============================== CLAUSES FOR SEARCH ==================== % 2.07/2.33 % 2.07/2.33 ============================== end of clauses for search ============= % 2.07/2.33 % 2.07/2.33 ============================== SEARCH ================================ % 2.07/2.33 % 2.07/2.33 % Starting search at 0.03 seconds. % 2.07/2.33 % 2.07/2.33 NOTE: Back_subsumption disabled, ratio of kept to back_subsumed is 63 (0.00 of 0.19 sec). % 2.07/2.33 % 2.07/2.33 Low Water (keep): wt=50.000, iters=3404 % 2.07/2.33 % 2.07/2.33 Low Water (keep): wt=49.000, iters=3337 % 2.07/2.33 % 2.07/2.33 Low Water (keep): wt=48.000, iters=3371 % 2.07/2.33 % 2.07/2.33 Low Water (keep): wt=44.000, iters=3358 % 2.07/2.33 % 2.07/2.33 Low Water (keep): wTerminated % 299.79/300.03 Prover9 interrupted %------------------------------------------------------------------------------