%------------------------------------------------------------------------------ % File : Waldmeister---710 % Problem : SWX237-1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : woody %s % Computer : n025.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:08:09 PM UTC 2026 % Result : Timeout 299.47s 300.02s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWX237-1 : TPTP v9.3.0. Released v9.3.0. % 0.12/0.13 % Command : woody %s % 0.17/0.34 % Computer : n025.cluster.edu % 0.17/0.34 % Model : x86_64 x86_64 % 0.17/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/0.34 % Memory : 8042.1875MB % 0.17/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.17/0.34 % CPULimit : 300 % 0.17/0.34 % WCLimit : 300 % 0.17/0.34 % DateTime : Tue May 5 13:14:58 EDT 2026 % 0.17/0.34 % CPUTime : % 0.79/1.19 ******************************************************************************** % 0.79/1.19 * W A L D M E I S T E R \| \ / \|/ * % 0.79/1.19 * |/ | \/ | * % 0.79/1.19 * (C) 1994-2010 A. Buch and Th. Hillenbrand, \ / \ / * % 0.79/1.19 * A. Jaeger and B. Loechner | | * % 0.79/1.19 * <waldmeister@informatik.uni-kl.de> | * % 0.79/1.19 ******************************************************************************** % 0.79/1.19 % 0.79/1.19 % 0.79/1.19 Goals: % 0.79/1.19 ------ % 0.79/1.19 % 0.79/1.19 ( 1) true ?= false % 0.79/1.19 using narrowing to prove btrue ?= eq2(prop_kfind4(x1),bfalse) % 0.79/1.19 % 0.79/1.19 Detected structure: Orkus % 0.79/1.19 ******************************************************************************** % 0.79/1.19 ****************************** COMPLETION - PROOF ****************************** % 0.79/1.19 ******************************************************************************** % 0.79/1.19 % 299.47/300.02 % 299.47/300.02 Problem WALDMEISTER_13422_n025 % 299.47/300.02 CPs.gen 31285927 % 299.47/300.02 CPs.reexp 0 % 299.47/300.02 Select 155450 % 299.47/300.02 R 59545 % 299.47/300.02 E 77 % 299.47/300.02 vsize 55.1M % 299.47/300.02 rss 53.8M % 299.47/300.02 process.time 298.654s % 299.47/300.02 wallclock.time 298.838s % 299.47/300.02 status T % 299.47/300.02 % 299.47/300.02 % 299.47/300.02 TIMEOUT: Got SIGTERM % 299.47/300.03 Terminated %------------------------------------------------------------------------------