%------------------------------------------------------------------------------ % File : SOS---2.0 % Problem : LCL640+1.005 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : sos-script %s % Computer : n017.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 : 600s % DateTime : Sun Jul 17 14:31:15 EDT 2022 % Result : Unknown 242.11s 242.30s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : LCL640+1.005 : TPTP v8.1.0. Released v4.0.0. % 0.11/0.13 % Command : sos-script %s % 0.13/0.34 % Computer : n017.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Mon Jul 4 23:17:27 EDT 2022 % 0.13/0.34 % CPUTime : % 241.84/242.03 ----- Otter 3.2, August 2001 ----- % 241.84/242.03 The process was started by sandbox on n017.cluster.edu, % 241.84/242.03 Mon Jul 4 23:17:27 2022 % 241.84/242.03 The command was "./sos". The process ID is 13148. % 241.84/242.03 % 241.84/242.03 set(prolog_style_variables). % 241.84/242.03 set(auto). % 241.84/242.03 dependent: set(auto1). % 241.84/242.03 dependent: set(process_input). % 241.84/242.03 dependent: clear(print_kept). % 241.84/242.03 dependent: clear(print_new_demod). % 241.84/242.03 dependent: clear(print_back_demod). % 241.84/242.03 dependent: clear(print_back_sub). % 241.84/242.03 dependent: set(control_memory). % 241.84/242.03 dependent: assign(max_mem, 12000). % 241.84/242.03 dependent: assign(pick_given_ratio, 4). % 241.84/242.03 dependent: assign(stats_level, 1). % 241.84/242.03 dependent: assign(pick_semantic_ratio, 3). % 241.84/242.03 dependent: assign(sos_limit, 5000). % 241.84/242.03 dependent: assign(max_weight, 60). % 241.84/242.03 clear(print_given). % 241.84/242.03 % 241.84/242.03 formula_list(usable). % 241.84/242.03 % 241.84/242.03 SCAN INPUT: prop=0, horn=0, equality=0, symmetry=0, max_lits=14. % 241.84/242.03 % 241.84/242.03 This is a non-Horn set without equality. The strategy % 241.84/242.03 will be ordered hyper_res, ur_res, unit deletion, and % 241.84/242.03 factoring, with satellites in sos and nuclei in usable. % 241.84/242.03 % 241.84/242.03 dependent: set(hyper_res). % 241.84/242.03 dependent: set(factor). % 241.84/242.03 dependent: set(unit_deletion). % 241.84/242.03 % 241.84/242.03 ------------> process usable: % 241.84/242.03 286 back subsumes 267. % 241.84/242.03 286 back subsumes 247. % 241.84/242.03 474 back subsumes 455. % 241.84/242.03 474 back subsumes 436. % 241.84/242.03 581 back subsumes 559. % 241.84/242.03 581 back subsumes 537. % 241.84/242.03 1155 back subsumes 1128. % 241.84/242.03 1185 back subsumes 1183. % 241.84/242.03 1187 back subsumes 1180. % 241.84/242.03 1279 back subsumes 1252. % 241.84/242.03 1309 back subsumes 1307. % 241.84/242.03 1311 back subsumes 1304. % 241.84/242.03 1566 back subsumes 1470. % 241.84/242.03 1566 back subsumes 1388. % 241.84/242.03 1594 back subsumes 1496. % 241.84/242.03 1594 back subsumes 1410. % 241.84/242.03 1610 back subsumes 1511. % 241.84/242.03 1610 back subsumes 1423. % 241.84/242.03 1880 back subsumes 1799. % 241.84/242.03 1880 back subsumes 1721. % 241.84/242.03 1908 back subsumes 1821. % 241.84/242.03 1908 back subsumes 1743. % 241.84/242.03 1924 back subsumes 1834. % 241.84/242.03 1924 back subsumes 1756. % 241.84/242.03 2205 back subsumes 2115. % 241.84/242.03 2205 back subsumes 2035. % 241.84/242.03 2235 back subsumes 2139. % 241.84/242.03 2235 back subsumes 2057. % 241.84/242.03 2252 back subsumes 2153. % 241.84/242.03 2252 back subsumes 2070. % 241.84/242.03 2640 back subsumes 2515. % 241.84/242.03 2640 back subsumes 2400. % 241.84/242.03 2675 back subsumes 2546. % 241.84/242.03 2675 back subsumes 2429. % 241.84/242.03 2696 back subsumes 2564. % 241.84/242.03 2696 back subsumes 2446. % 241.84/242.03 2872 back subsumes 2870. % 241.84/242.03 2874 back subsumes 2867. % 241.84/242.03 2925 back subsumes 2923. % 241.84/242.03 2927 back subsumes 2920. % 241.84/242.03 3381 back subsumes 3379. % 241.84/242.03 3383 back subsumes 3376. % 241.84/242.03 3398 back subsumes 3396. % 241.84/242.03 3400 back subsumes 3393. % 241.84/242.03 3565 back subsumes 3561. % 241.84/242.03 3611 back subsumes 3600. % 241.84/242.03 3621 back subsumes 3617. % 241.84/242.03 3648 back subsumes 3642. % 241.84/242.03 3656 back subsumes 3626. % 241.84/242.03 3659 back subsumes 3643. % 241.84/242.03 3664 back subsumes 3627. % 241.84/242.03 3693 back subsumes 3689. % 241.84/242.03 3739 back subsumes 3728. % 241.84/242.03 3749 back subsumes 3745. % 241.84/242.03 3776 back subsumes 3770. % 241.84/242.03 3784 back subsumes 3754. % 241.84/242.03 3787 back subsumes 3771. % 241.84/242.03 3792 back subsumes 3755. % 241.84/242.03 4017 back subsumes 3912. % 241.84/242.03 4017 back subsumes 3821. % 241.84/242.03 4058 back subsumes 3965. % 241.84/242.03 4058 back subsumes 3953. % 241.84/242.03 4058 back subsumes 3950. % 241.84/242.03 4058 back subsumes 3864. % 241.84/242.03 4058 back subsumes 3854. % 241.84/242.03 4058 back subsumes 3851. % 241.84/242.03 4303 back subsumes 4236. % 241.84/242.03 4303 back subsumes 4165. % 241.84/242.03 4344 back subsumes 4270. % 241.84/242.03 4344 back subsumes 4262. % 241.84/242.03 4344 back subsumes 4259. % 241.84/242.03 4344 back subsumes 4199. % 241.84/242.03 4344 back subsumes 4191. % 241.84/242.03 4344 back subsumes 4188. % 241.84/242.03 4624 back subsumes 4527. % 241.84/242.03 4624 back subsumes 4453. % 241.84/242.03 4677 back subsumes 4577. % 241.84/242.03 4677 back subsumes 4566. % 241.84/242.03 4677 back subsumes 4563. % 241.84/242.03 4677 back subsumes 4487. % 241.84/242.03 4677 back subsumes 4479. % 241.84/242.03 4677 back subsumes 4476. % 241.84/242.03 5174 back subsumes 4989. % 241.84/242.03 5174 back subsumes 4832. % 241.84/242.03 5253 back subsumes 5069. % 241.84/242.03 5253 back subsumes 5052. % 241.84/242.03 5253 back subsumes 5049. % 241.84/242.03 5253 back subsumes 4897. % 241.84/242.03 5253 back subsumes 4883. % 241.84/242.03 5253 back subsumes 4880. % 241.84/242.03 % 241.84/242.03 ------------> process sos: % 241.84/242.03 % 241.84/242.03 ======= end of input processing ======= % 242.11/242.29 % 242.11/242.29 % 242.11/242.29 % 242.11/242.29 Aborting on detection of an error: % 242.11/242.29 % 242.11/242.29 Too many clauses (whew!). % 242.11/242.29 %------------------------------------------------------------------------------