%------------------------------------------------------------------------------ % File : SOS---2.0 % Problem : LCL658+1.005 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : sos-script %s % Computer : n013.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:39 EDT 2022 % Result : Unknown 207.87s 208.05s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : LCL658+1.005 : TPTP v8.1.0. Released v4.0.0. % 0.07/0.13 % Command : sos-script %s % 0.13/0.34 % Computer : n013.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 15:24:44 EDT 2022 % 0.13/0.34 % CPUTime : % 207.56/207.80 ----- Otter 3.2, August 2001 ----- % 207.56/207.80 The process was started by sandbox2 on n013.cluster.edu, % 207.56/207.80 Mon Jul 4 15:24:44 2022 % 207.56/207.80 The command was "./sos". The process ID is 4308. % 207.56/207.80 % 207.56/207.80 set(prolog_style_variables). % 207.56/207.80 set(auto). % 207.56/207.80 dependent: set(auto1). % 207.56/207.80 dependent: set(process_input). % 207.56/207.80 dependent: clear(print_kept). % 207.56/207.80 dependent: clear(print_new_demod). % 207.56/207.80 dependent: clear(print_back_demod). % 207.56/207.80 dependent: clear(print_back_sub). % 207.56/207.80 dependent: set(control_memory). % 207.56/207.80 dependent: assign(max_mem, 12000). % 207.56/207.80 dependent: assign(pick_given_ratio, 4). % 207.56/207.80 dependent: assign(stats_level, 1). % 207.56/207.80 dependent: assign(pick_semantic_ratio, 3). % 207.56/207.80 dependent: assign(sos_limit, 5000). % 207.56/207.80 dependent: assign(max_weight, 60). % 207.56/207.80 clear(print_given). % 207.56/207.80 % 207.56/207.80 formula_list(usable). % 207.56/207.80 % 207.56/207.80 SCAN INPUT: prop=0, horn=0, equality=0, symmetry=0, max_lits=14. % 207.56/207.80 % 207.56/207.80 This is a non-Horn set without equality. The strategy % 207.56/207.80 will be ordered hyper_res, ur_res, unit deletion, and % 207.56/207.80 factoring, with satellites in sos and nuclei in usable. % 207.56/207.80 % 207.56/207.80 dependent: set(hyper_res). % 207.56/207.80 dependent: set(factor). % 207.56/207.80 dependent: set(unit_deletion). % 207.56/207.80 % 207.56/207.80 ------------> process usable: % 207.56/207.80 185 back subsumes 166. % 207.56/207.80 185 back subsumes 146. % 207.56/207.80 373 back subsumes 354. % 207.56/207.80 373 back subsumes 335. % 207.56/207.80 480 back subsumes 458. % 207.56/207.80 480 back subsumes 436. % 207.56/207.80 770 back subsumes 768. % 207.56/207.80 772 back subsumes 765. % 207.56/207.80 823 back subsumes 821. % 207.56/207.80 825 back subsumes 818. % 207.56/207.80 1080 back subsumes 984. % 207.56/207.80 1080 back subsumes 902. % 207.56/207.80 1108 back subsumes 1010. % 207.56/207.80 1108 back subsumes 924. % 207.56/207.80 1124 back subsumes 1025. % 207.56/207.80 1124 back subsumes 937. % 207.56/207.80 1394 back subsumes 1313. % 207.56/207.80 1394 back subsumes 1235. % 207.56/207.80 1422 back subsumes 1335. % 207.56/207.80 1422 back subsumes 1257. % 207.56/207.80 1438 back subsumes 1348. % 207.56/207.80 1438 back subsumes 1270. % 207.56/207.80 1719 back subsumes 1629. % 207.56/207.80 1719 back subsumes 1549. % 207.56/207.80 1749 back subsumes 1653. % 207.56/207.80 1749 back subsumes 1571. % 207.56/207.80 1766 back subsumes 1667. % 207.56/207.80 1766 back subsumes 1584. % 207.56/207.80 2154 back subsumes 2029. % 207.56/207.80 2154 back subsumes 1914. % 207.56/207.80 2189 back subsumes 2060. % 207.56/207.80 2189 back subsumes 1943. % 207.56/207.80 2210 back subsumes 2078. % 207.56/207.80 2210 back subsumes 1960. % 207.56/207.80 2386 back subsumes 2384. % 207.56/207.80 2388 back subsumes 2381. % 207.56/207.80 2439 back subsumes 2437. % 207.56/207.80 2441 back subsumes 2434. % 207.56/207.80 3131 back subsumes 3026. % 207.56/207.80 3131 back subsumes 2935. % 207.56/207.80 3172 back subsumes 3079. % 207.56/207.80 3172 back subsumes 3067. % 207.56/207.80 3172 back subsumes 3064. % 207.56/207.80 3172 back subsumes 2978. % 207.56/207.80 3172 back subsumes 2968. % 207.56/207.80 3172 back subsumes 2965. % 207.56/207.80 3417 back subsumes 3350. % 207.56/207.80 3417 back subsumes 3279. % 207.56/207.80 3458 back subsumes 3384. % 207.56/207.80 3458 back subsumes 3376. % 207.56/207.80 3458 back subsumes 3373. % 207.56/207.80 3458 back subsumes 3313. % 207.56/207.80 3458 back subsumes 3305. % 207.56/207.80 3458 back subsumes 3302. % 207.56/207.80 3738 back subsumes 3641. % 207.56/207.80 3738 back subsumes 3567. % 207.56/207.80 3791 back subsumes 3691. % 207.56/207.80 3791 back subsumes 3680. % 207.56/207.80 3791 back subsumes 3677. % 207.56/207.80 3791 back subsumes 3601. % 207.56/207.80 3791 back subsumes 3593. % 207.56/207.80 3791 back subsumes 3590. % 207.56/207.80 4288 back subsumes 4103. % 207.56/207.80 4288 back subsumes 3946. % 207.56/207.80 4367 back subsumes 4183. % 207.56/207.80 4367 back subsumes 4166. % 207.56/207.80 4367 back subsumes 4163. % 207.56/207.80 4367 back subsumes 4011. % 207.56/207.80 4367 back subsumes 3997. % 207.56/207.80 4367 back subsumes 3994. % 207.56/207.80 % 207.56/207.80 ------------> process sos: % 207.56/207.80 % 207.56/207.80 ======= end of input processing ======= % 207.87/208.04 % 207.87/208.04 % 207.87/208.04 % 207.87/208.04 Aborting on detection of an error: % 207.87/208.04 % 207.87/208.04 Too many clauses (whew!). % 207.87/208.04 %------------------------------------------------------------------------------