%------------------------------------------------------------------------------ % File : Prover9---1109a % Problem : SWX232-1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : tptp2X_and_run_prover9 %d %s % Computer : n019.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:09 PM UTC 2026 % Result : Timeout 295.62s 295.96s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWX232-1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.12 % Command : tptp2X_and_run_prover9 %d %s % 0.15/0.33 % Computer : n019.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 : Wed Apr 29 02:45:58 EDT 2026 % 0.15/0.33 % CPUTime : % 2.43/2.70 ============================== Prover9 =============================== % 2.43/2.70 Prover9 (32) version 2009-11A, November 2009. % 2.43/2.70 Process 32068 was started by sandbox2 on n019.cluster.edu, % 2.43/2.70 Wed Apr 29 02:45:59 2026 % 2.43/2.70 The command was "/export/starexec/sandbox2/solver/bin/prover9 -t 300 -f /tmp/Prover9_31913_n019.cluster.edu". % 2.43/2.70 ============================== end of head =========================== % 2.43/2.70 % 2.43/2.70 ============================== INPUT ================================= % 2.43/2.70 % 2.43/2.70 % Reading from file /tmp/Prover9_31913_n019.cluster.edu % 2.43/2.70 % 2.43/2.70 set(prolog_style_variables). % 2.43/2.70 set(auto2). % 2.43/2.70 % set(auto2) -> set(auto). % 2.43/2.70 % set(auto) -> set(auto_inference). % 2.43/2.70 % set(auto) -> set(auto_setup). % 2.43/2.70 % set(auto_setup) -> set(predicate_elim). % 2.43/2.70 % set(auto_setup) -> assign(eq_defs, unfold). % 2.43/2.70 % set(auto) -> set(auto_limits). % 2.43/2.70 % set(auto_limits) -> assign(max_weight, "100.000"). % 2.43/2.70 % set(auto_limits) -> assign(sos_limit, 20000). % 2.43/2.70 % set(auto) -> set(auto_denials). % 2.43/2.70 % set(auto) -> set(auto_process). % 2.43/2.70 % set(auto2) -> assign(new_constants, 1). % 2.43/2.70 % set(auto2) -> assign(fold_denial_max, 3). % 2.43/2.70 % set(auto2) -> assign(max_weight, "200.000"). % 2.43/2.70 % set(auto2) -> assign(max_hours, 1). % 2.43/2.70 % assign(max_hours, 1) -> assign(max_seconds, 3600). % 2.43/2.70 % set(auto2) -> assign(max_seconds, 0). % 2.43/2.70 % set(auto2) -> assign(max_minutes, 5). % 2.43/2.70 % assign(max_minutes, 5) -> assign(max_seconds, 300). % 2.43/2.70 % set(auto2) -> set(sort_initial_sos). % 2.43/2.70 % set(auto2) -> assign(sos_limit, -1). % 2.43/2.70 % set(auto2) -> assign(lrs_ticks, 3000). % 2.43/2.70 % set(auto2) -> assign(max_megs, 400). % 2.43/2.70 % set(auto2) -> assign(stats, some). % 2.43/2.70 % set(auto2) -> clear(echo_input). % 2.43/2.70 % set(auto2) -> set(quiet). % 2.43/2.70 % set(auto2) -> clear(print_initial_clauses). % 2.43/2.70 % set(auto2) -> clear(print_given). % 2.43/2.70 assign(lrs_ticks,-1). % 2.43/2.70 assign(sos_limit,10000). % 2.43/2.70 assign(order,kbo). % 2.43/2.70 set(lex_order_vars). % 2.43/2.70 clear(print_given). % 2.43/2.70 % 2.43/2.70 % formulas(sos). % not echoed (71 formulas) % 2.43/2.70 % 2.43/2.70 ============================== end of input ========================== % 2.43/2.70 % 2.43/2.70 % From the command line: assign(max_seconds, 300). % 2.43/2.70 % 2.43/2.70 ============================== PROCESS NON-CLAUSAL FORMULAS ========== % 2.43/2.70 % 2.43/2.70 % Formulas that are not ordinary clauses: % 2.43/2.70 % 2.43/2.70 ============================== end of process non-clausal formulas === % 2.43/2.70 % 2.43/2.70 ============================== PROCESS INITIAL CLAUSES =============== % 2.43/2.70 % 2.43/2.70 ============================== PREDICATE ELIMINATION ================= % 2.43/2.70 % 2.43/2.70 ============================== end predicate elimination ============= % 2.43/2.70 % 2.43/2.70 Auto_denials: % 2.43/2.70 % copying label goal to answer in negative clause % 2.43/2.70 % 2.43/2.70 Term ordering decisions: % 2.43/2.70 Function symbol KB weights: bfalse=1. zero=1. btrue=1. nil2=1. nil=1. two=1. nil3=1. one=1. three=1. add=1. cons2=1. cons=1. pair2=1. eq=1. andb=1. append=1. enumFromToNat=1. lt=1. orb=1. path2=1. tour=1. dodeca2=1. dodeca3=1. dodeca4=1. dodeca5=1. dodeca6=1. elem=1. last=1. maxNat=1. maximum=1. eq2=1. cons3=1. suc=1. dodeca=1. len=1. or2=1. unique=1. dodeca7=1. notb=1. predNat=1. prop_t3=1. path=1. aux=1. aux2=1. aux3=1. % 2.43/2.70 % 2.43/2.70 ============================== end of process initial clauses ======== % 2.43/2.70 % 2.43/2.70 ============================== CLAUSES FOR SEARCH ==================== % 2.43/2.70 % 2.43/2.70 ============================== end of clauses for search ============= % 2.43/2.70 % 2.43/2.70 ============================== SEARCH ================================ % 2.43/2.70 % 2.43/2.70 % Starting search at 0.02 seconds. % 2.43/2.70 % 2.43/2.70 NOTE: Back_subsumption disabled, ratio of kept to back_subsumed is 163 (0.00 of 0.54 sec). % 2.43/2.70 % 2.43/2.70 Low Water (keep): wt=132.000, iters=3379 % 2.43/2.70 % 2.43/2.70 Low Water (keep): wt=114.000, iters=3371 % 2.43/2.70 % 2.43/2.70 Low Water (keep): wt=83.000, iters=3369 % 2.43/2.70 % 2.43/2.70 Low Water (keep): wt=78.000, iters=3354 % 2.43/2.70 % 2.43/2.70 Low Water (keep): wt=73.000, iters=3343 % 2.43/2.70 % 2.43/2.70 Low Water (keep): wt=64.000, iters=3351 % 2.43/2.70 % 2.43/2.70 Low Water (keep): wt=59.000, iters=3334 % 2.43/2.70 % 2.43/2.70 Low Water (keep): wt=58.000, iters=3344 % 2.43/2.70 % 2.43/2.70 Low Water (keep): wt=56.000, iters=3377 % 2.43/2.70 % 2.43/2.70 Low Water (keep): wt=55.000, iters=3350 % 2.43/2.70 % 2.43/2.70 Low Water (keep): wt=52.000, iters=3378 % 2.43/2.70 % 2.43/2.70 Low Water (keep): wt=51.000, iters=3362 % 2.43/2.70 % 2.43/2.70 Low Water (keep): wt=50.000, iters=3336 % 2.43/2.70 % 2.43/2.70 Low Water (keep): wt=49.000, iters=3369 % 2.43/2.70 % 2.43/2.70 Low Water (keep): wt=44.000, iters=3344 % 2.43/2.70 % 2.43/2.70 Low Water (keep): wt=43.000, iters=3497 % 2.43/2.70 % 2.43/2.70 Low Water (keep): wt=42.000, iters=3416 % 2.43/2.70 % 2.43/2.70 Low Water (keep): wt=41.000, iters=3388 % 295.62/295.96 % 295.62/295.96 Low Water (keep): wt=40.000, iters=3424 % 295.62/295.96 % 295.62/295.96 Low Water (keep): wt=39.000, iters=3336 % 295.62/295.96 % 295.62/295.96 Low Water (keep): wt=38.000, iters=3393 % 295.62/295.96 % 295.62/295.96 Low Water (keep): wt=37.000, iters=3333 % 295.62/295.96 % 295.62/295.96 Low Water (keep): wt=36.000, iters=3372 % 295.62/295.96 % 295.62/295.96 Low Water (keep): wt=35.000, iters=3414 % 295.62/295.96 % 295.62/295.96 Low Water (keep): wt=34.000, iters=3361 % 295.62/295.96 % 295.62/295.96 Low Water (keep): wt=33.000, iters=3375 % 295.62/295.96 % 295.62/295.96 Low Water (keep): wt=32.000, iters=3340 % 295.62/295.96 % 295.62/295.96 Low Water (keep): wt=31.000, iters=3359 % 295.62/295.96 % 295.62/295.96 Low Water (keep): wt=30.000, iters=3365 % 295.62/295.96 % 295.62/295.96 Low Water (keep): wt=29.000, iters=3348 % 295.62/295.96 % 295.62/295.96 Low Water (keep): wt=28.000, iters=3376 % 295.62/295.96 % 295.62/295.96 Low Water (keep): wt=27.000, iters=3335 % 295.62/295.96 % 295.62/295.96 Low Water (displace): id=5411, wt=200.000 % 295.62/295.96 % 295.62/295.96 Low Water (displace): id=3983, wt=198.000 % 295.62/295.96 % 295.62/295.96 Low Water (displace): id=3992, wt=193.000 % 295.62/295.96 % 295.62/295.96 Low Water (displace): id=6012, wt=186.000 % 295.62/295.96 % 295.62/295.96 Low Water (displace): id=4028, wt=184.000 % 295.62/295.96 % 295.62/295.96 Low Water (displace): id=3990, wt=180.000 % 295.62/295.96 % 295.62/295.96 Low Water (displace): id=3991, wt=178.000 % 295.62/295.96 % 295.62/295.96 Low Water (displace): id=6009, wt=170.000 % 295.62/295.96 % 295.62/295.96 Low Water (displace): id=3989, wt=167.000 % 295.62/295.96 % 295.62/295.96 Low Water (displace): id=4025, wt=160.000 % 295.62/295.96 % 295.62/295.96 Low Water (displace): id=3988, wt=156.000 % 295.62/295.96 % 295.62/295.96 Low Water (displace): id=6011, wt=152.000 % 295.62/295.96 % 295.62/295.96 Low Water (displace): id=3984, wt=148.000 % 295.62/295.96 % 295.62/295.96 Low Water (displace): id=4037, wt=143.000 % 295.62/295.96 % 295.62/295.96 Low Water (displace): id=6010, wt=137.000 % 295.62/295.96 % 295.62/295.96 Low Water (keep): wt=26.000, iters=3383 % 295.62/295.96 % 295.62/295.96 Low Water (displace): id=4027, wt=136.000 % 295.62/295.96 % 295.62/295.96 Low Water (displace): id=3978, wt=131.000 % 295.62/295.96 % 295.62/295.96 Low Water (displace): id=4035, wt=128.000 % 295.62/295.96 % 295.62/295.96 Low Water (displace): id=4026, wt=123.000 % 295.62/295.96 % 295.62/295.96 Low Water (displace): id=3701, wt=122.000 % 295.62/295.96 % 295.62/295.96 Low Water (displace): id=6004, wt=121.000 % 295.62/295.96 % 295.62/295.96 Low Water (displace): id=6006, wt=120.000 % 295.62/295.96 % 295.62/295.96 Low Water (displace): id=3960, wt=119.000 % 295.62/295.96 % 295.62/295.96 Low Water (displace): id=6005, wt=118.000 % 295.62/295.96 % 295.62/295.96 Low Water (displace): id=3987, wt=117.000 % 295.62/295.96 % 295.62/295.96 Low Water (displace): id=4029, wt=116.000 % 295.62/295.96 % 295.62/295.96 Low Water (displace): id=4021, wt=112.000 % 295.62/295.96 % 295.62/295.96 Low Water (displace): id=6775, wt=109.000 % 295.62/295.96 % 295.62/295.96 Low Water (displace): id=3813, wt=104.000 % 295.62/295.96 % 295.62/295.96 Low Water (displace): id=6744, wt=103.000 % 295.62/295.96 % 295.62/295.96 Low Water (displace): id=6007, wt=102.000 % 295.62/295.96 % 295.62/295.96 Low Water (displace): id=3986, wt=101.000 % 295.62/295.96 % 295.62/295.96 Low Water (displace): id=5409, wt=98.000 % 295.62/295.96 % 295.62/295.96 Low Water (displace): id=3979, wt=89.000 % 295.62/295.96 % 295.62/295.96 Low Water (displace): id=5979, wt=85.000 % 295.62/295.96 % 295.62/295.96 Low Water (displace): id=4024, wt=84.000 % 295.62/295.96 % 295.62/295.96 Low Water (displace): id=3948, wt=83.000 % 295.62/295.96 % 295.62/295.96 Low Water (displace): id=3360, wt=81.000 % 295.62/295.96 % 295.62/295.96 Low Water (displace): id=3985, wt=80.000 % 295.62/295.96 % 295.62/295.96 Low Water (displace): id=3875, wt=79.000 % 295.62/295.96 % 295.62/295.96 Low Water (displace): id=3912, wt=78.000 % 295.62/295.96 % 295.62/295.96 Low Water (displace): id=3972, wt=77.000 % 295.62/295.96 % 295.62/295.96 Low Water (displace): id=5864, wt=76.000 % 295.62/295.96 % 295.62/295.96 Low Water (displace): id=5853, wt=75.000 % 295.62/295.96 % 295.62/295.96 Low Water (displace): id=3959, wt=74.000 % 295.62/295.96 % 295.62/295.96 Low Water (displace): id=3969, wt=73.000 % 295.62/295.96 % 295.62/295.96 Low Water (displace): id=3953, wt=71.000 % 295.62/295.96 % 295.62/295.96 Low Water (displace): id=5977, wt=70.000 % 295.62/295.96 % 295.62/295.96 Low Water (displace): id=5772, wt=69.000 % 295.62/295.96 % 295.62/295.96 Low Water (displace): id=5922, wt=68.000 % 295.62/295.96 % 295.62/295.96 Low Water (displace): id=5380, wt=67.000 % 295.62/295.96 % 295.62/295.96 Low Water (displace): id=7139, wt=66.000 % 295.62/295.96 % 295.62/295.96 Low Water (displace): id=3906, wt=65.000 % 295.62/295.96 % 295.62/295.96 Low Water (displace): id=3941, wt=64.000 % 295.62/295.96 % 295.62/295.96 Low Water (displace): id=5985, wt=63.000 % 295.62/295.96 % 295.62/295.96 Low Water (displace): id=7145, wt=62.000 % 295.62/295.96 % 295.62/295.96 Low Water (displace): id=7130, wt=61.000 % 295.62/295.96 % 295.62/295.96 Low Water (displace): id=5912, wt=60.000 % 295.62/295.96 % 295.62/295.96 Low Water (displace): id=7133, wt=59.000 % 295.62/295.96 % 295.62/295.96 Low Water (keep): wt=25.000, iters=3347 % 295.62/295.96 % 295.62/295.96 Low Water (displace): id=7280, wt=58.000 % 295.62/295.96 % 295.62/295.96 Low Water (displace): id=6486, wt=57.000 % 295.62/295.96 % 295.62/295.96 Low Water (displace): id=7128, wt=56.000 % 295.62/295.96 % 295.62/295.96 Low Water (displace): id=16169, wt=17.000 % 295.62/295.96 % 295.62/295.96 Low Water (displace): id=16437, wt=16.000 % 295.62/295.96 % 295.62/295.96 Low Water (displace): id=16438, wt=15.000 % 295.62/295.96 % 295.62/295.96 Low Water (keep): wt=24.000, iters=3336 % 295.62/295.96 % 295.62/295.96 Low Water (keep): wt=23.000, iters=3334 % 295.62/295.96 % 295.62/295.96 Low Water (keep): wt=22.000, iters=3339 % 295.62/295.96 % 295.62/295.96 Low Water (keep): wt=21.000, iters=3335 % 295.62/295.96 % 295.62/295.96 Low Water (keep): wt=20.000, iters=3338 % 295.62/295.96 % 295.62/295.96 Low Water (keep): wt=19.000, iters=3333 % 295.62/295.96 % 295.62/295.96 Low Water (keep): wt=18.000, iters=3336 % 295.62/295.96 % 295.62/295.96 Low Water (displace): id=40989, wt=14.000 % 295.62/295.96 % 295.62/295.96 Low Water (displace): id=40994, wt=13.000 % 295.62/295.96 % 295.62/295.96 Low Water (displace): id=40999, wt=12.000 % 295.62/295.96 % 295.62/295.96 Low Water (displace): id=41214, wt=11.000 % 295.62/295.96 % 295.62/295.96 Low Water (displace): id=42041, wt=10.000 % 295.62/295.96 % 295.62/295.96 Low Water (displace): id=42148, wt=9.000 % 295.62/295.96 % 295.62/295.96 Low Water (displace): id=43021, wt=8.000 % 295.62/295.96 % 295.62/295.96 Low Water (displace): id=45071, wt=7.000 % 295.62/295.96 % 295.62/295.96 Low Water (keep): wt=17.000, iters=3337 % 295.62/295.96 % 295.62/295.96 LTerminated % 299.76/300.03 Prover9 interrupted %------------------------------------------------------------------------------