%------------------------------------------------------------------------------ % File : Otter---3.3 % Problem : SWV422-1.065 : TPTP v8.1.0. Released v3.5.0. % Transfm : none % Format : tptp:raw % Command : otter-tptp-script %s % Computer : n012.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 Jul 27 13:20:43 EDT 2022 % Result : Unknown 1.95s 2.13s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.11 % Problem : SWV422-1.065 : TPTP v8.1.0. Released v3.5.0. % 0.03/0.12 % Command : otter-tptp-script %s % 0.11/0.33 % Computer : n012.cluster.edu % 0.11/0.33 % Model : x86_64 x86_64 % 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.33 % Memory : 8042.1875MB % 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.33 % CPULimit : 300 % 0.11/0.33 % WCLimit : 300 % 0.11/0.33 % DateTime : Wed Jul 27 06:00:50 EDT 2022 % 0.11/0.33 % CPUTime : % 1.82/2.04 ----- Otter 3.3f, August 2004 ----- % 1.82/2.04 The process was started by sandbox on n012.cluster.edu, % 1.82/2.04 Wed Jul 27 06:00:50 2022 % 1.82/2.04 The command was "./otter". The process ID is 19194. % 1.82/2.04 % 1.82/2.04 set(prolog_style_variables). % 1.82/2.04 set(auto). % 1.82/2.04 dependent: set(auto1). % 1.82/2.04 dependent: set(process_input). % 1.82/2.04 dependent: clear(print_kept). % 1.82/2.04 dependent: clear(print_new_demod). % 1.82/2.04 dependent: clear(print_back_demod). % 1.82/2.04 dependent: clear(print_back_sub). % 1.82/2.04 dependent: set(control_memory). % 1.82/2.04 dependent: assign(max_mem, 12000). % 1.82/2.04 dependent: assign(pick_given_ratio, 4). % 1.82/2.04 dependent: assign(stats_level, 1). % 1.82/2.04 dependent: assign(max_seconds, 10800). % 1.82/2.04 clear(print_given). % 1.82/2.04 % 1.82/2.04 list(usable). % 1.82/2.04 0 [] succ(s0,s1). % 1.82/2.04 0 [] succ(s1,s2). % 1.82/2.04 0 [] succ(s2,s3). % 1.82/2.04 0 [] succ(s3,s4). % 1.82/2.04 0 [] succ(s4,s5). % 1.82/2.04 0 [] succ(s5,s6). % 1.82/2.04 0 [] succ(s6,s7). % 1.82/2.04 0 [] succ(s7,s8). % 1.82/2.04 0 [] succ(s8,s9). % 1.82/2.04 0 [] succ(s9,s10). % 1.82/2.04 0 [] succ(s10,s11). % 1.82/2.04 0 [] succ(s11,s12). % 1.82/2.04 0 [] succ(s12,s13). % 1.82/2.04 0 [] succ(s13,s14). % 1.82/2.04 0 [] succ(s14,s15). % 1.82/2.04 0 [] succ(s15,s16). % 1.82/2.04 0 [] succ(s16,s17). % 1.82/2.04 0 [] succ(s17,s18). % 1.82/2.04 0 [] succ(s18,s19). % 1.82/2.04 0 [] succ(s19,s20). % 1.82/2.04 0 [] succ(s20,s21). % 1.82/2.04 0 [] succ(s21,s22). % 1.82/2.04 0 [] succ(s22,s23). % 1.82/2.04 0 [] succ(s23,s24). % 1.82/2.04 0 [] succ(s24,s25). % 1.82/2.04 0 [] succ(s25,s26). % 1.82/2.04 0 [] succ(s26,s27). % 1.82/2.04 0 [] succ(s27,s28). % 1.82/2.04 0 [] succ(s28,s29). % 1.82/2.04 0 [] succ(s29,s30). % 1.82/2.04 0 [] succ(s30,s31). % 1.82/2.04 0 [] succ(s31,s32). % 1.82/2.04 0 [] succ(s32,s33). % 1.82/2.04 0 [] succ(s33,s34). % 1.82/2.04 0 [] succ(s34,s35). % 1.82/2.04 0 [] succ(s35,s36). % 1.82/2.04 0 [] succ(s36,s37). % 1.82/2.04 0 [] succ(s37,s38). % 1.82/2.04 0 [] succ(s38,s39). % 1.82/2.04 0 [] succ(s39,s40). % 1.82/2.04 0 [] succ(s40,s41). % 1.82/2.04 0 [] succ(s41,s42). % 1.82/2.04 0 [] succ(s42,s43). % 1.82/2.04 0 [] succ(s43,s44). % 1.82/2.04 0 [] succ(s44,s45). % 1.82/2.04 0 [] succ(s45,s46). % 1.82/2.04 0 [] succ(s46,s47). % 1.82/2.04 0 [] succ(s47,s48). % 1.82/2.04 0 [] succ(s48,s49). % 1.82/2.04 0 [] succ(s49,s50). % 1.82/2.04 0 [] succ(s50,s51). % 1.82/2.04 0 [] succ(s51,s52). % 1.82/2.04 0 [] succ(s52,s53). % 1.82/2.04 0 [] succ(s53,s54). % 1.82/2.04 0 [] succ(s54,s55). % 1.82/2.04 0 [] succ(s55,s56). % 1.82/2.04 0 [] succ(s56,s57). % 1.82/2.04 0 [] succ(s57,s58). % 1.82/2.04 0 [] succ(s58,s59). % 1.82/2.04 0 [] succ(s59,s60). % 1.82/2.04 0 [] succ(s60,s61). % 1.82/2.04 0 [] succ(s61,s62). % 1.82/2.04 0 [] succ(s62,s63). % 1.82/2.04 0 [] succ(s63,s64). % 1.82/2.04 0 [] last(s64). % 1.82/2.04 0 [] -succ(X,Y)|trans(X,Y). % 1.82/2.04 0 [] -loop|trans(s64,s0)|trans(s64,s1)|trans(s64,s2)|trans(s64,s3)|trans(s64,s4)|trans(s64,s5)|trans(s64,s6)|trans(s64,s7)|trans(s64,s8)|trans(s64,s9)|trans(s64,s10)|trans(s64,s11)|trans(s64,s12)|trans(s64,s13)|trans(s64,s14)|trans(s64,s15)|trans(s64,s16)|trans(s64,s17)|trans(s64,s18)|trans(s64,s19)|trans(s64,s20)|trans(s64,s21)|trans(s64,s22)|trans(s64,s23)|trans(s64,s24)|trans(s64,s25)|trans(s64,s26)|trans(s64,s27)|trans(s64,s28)|trans(s64,s29)|trans(s64,s30)|trans(s64,s31)|trans(s64,s32)|trans(s64,s33)|trans(s64,s34)|trans(s64,s35)|trans(s64,s36)|trans(s64,s37)|trans(s64,s38)|trans(s64,s39)|trans(s64,s40)|trans(s64,s41)|trans(s64,s42)|trans(s64,s43)|trans(s64,s44)|trans(s64,s45)|trans(s64,s46)|trans(s64,s47)|trans(s64,s48)|trans(s64,s49)|trans(s64,s50)|trans(s64,s51)|trans(s64,s52)|trans(s64,s53)|trans(s64,s54)|trans(s64,s55)|trans(s64,s56)|trans(s64,s57)|trans(s64,s58)|trans(s64,s59)|trans(s64,s60)|trans(s64,s61)|trans(s64,s62)|trans(s64,s63)|trans(s64,s64). % 1.82/2.04 0 [] m_main_v_state1(X,c_n1)|m_main_v_state1(X,c_t1)|m_main_v_state1(X,c_c1). % 1.82/2.04 0 [] -m_main_v_state1(X,c_n1)| -m_main_v_state1(X,c_t1). % 1.82/2.04 0 [] -m_main_v_state1(X,c_n1)| -m_main_v_state1(X,c_c1). % 1.82/2.04 0 [] -m_main_v_state1(X,c_t1)| -m_main_v_state1(X,c_c1). % 1.82/2.04 0 [] m_main_v_state2(X,c_n2)|m_main_v_state2(X,c_t2)|m_main_v_state2(X,c_c2). % 1.82/2.04 0 [] -m_main_v_state2(X,c_n2)| -m_main_v_state2(X,c_t2). % 1.82/2.04 0 [] -m_main_v_state2(X,c_n2)| -m_main_v_state2(X,c_c2). % 1.82/2.04 0 [] -m_main_v_state2(X,c_t2)| -m_main_v_state2(X,c_c2). % 1.82/2.04 0 [] m_main_v_turn(X,c_1)|m_main_v_turn(X,c_2). % 1.82/2.04 0 [] -m_main_v_turn(X,c_1)| -m_main_v_turn(X,c_2). % 1.82/2.04 0 [] m_main_v_state1(s0,c_n1). % 1.82/2.04 0 [] m_main_v_state2(s0,c_n2). % 1.82/2.04 0 [] m_main_v_turn(s0,c_1). % 1.82/2.04 0 [] m_main_v_state1(X,c_n1)| -node1(X). % 1.82/2.04 0 [] m_main_v_state2(X,c_t2)| -node1(X). % 1.82/2.04 0 [] m_main_v_state1(X,c_n1)| -node2(X). % 1.82/2.04 0 [] m_main_v_state2(X,c_n2)| -node2(X). % 1.82/2.04 0 [] m_main_v_state1(X,c_n1)| -node3(X). % 1.82/2.04 0 [] m_main_v_state2(X,c_c2)| -node3(X). % 1.82/2.04 0 [] m_main_v_state1(X,c_t1)| -node4(X). % 1.82/2.04 0 [] m_main_v_state2(X,c_n2)| -node4(X). % 1.82/2.04 0 [] m_main_v_state1(X,c_t1)| -node5(X). % 1.82/2.04 0 [] m_main_v_state2(X,c_t2)| -node5(X). % 1.82/2.04 0 [] m_main_v_turn(X,c_1)| -node5(X). % 1.82/2.04 0 [] m_main_v_state1(Y,V)| -m_main_v_state1(X,V)| -node6(X,Y). % 1.82/2.04 0 [] -m_main_v_state1(Y,V)|m_main_v_state1(X,V)| -node6(X,Y). % 1.82/2.04 0 [] -m_main_v_state1(X,c_n1)| -m_main_v_state2(X,c_t2)|m_main_v_state1(Y,c_t1)| -node7(X,Y). % 1.82/2.04 0 [] node1(X)| -m_main_v_state1(X,c_n1)| -m_main_v_state2(X,c_n2)|m_main_v_state1(Y,c_t1)| -node7(X,Y). % 1.82/2.04 0 [] node1(X)|node2(X)| -m_main_v_state1(X,c_n1)| -m_main_v_state2(X,c_c2)|m_main_v_state1(Y,c_t1)| -node7(X,Y). % 1.82/2.04 0 [] node1(X)|node2(X)|node3(X)| -m_main_v_state1(X,c_t1)| -m_main_v_state2(X,c_n2)|m_main_v_state1(Y,c_c1)| -node7(X,Y). % 1.82/2.04 0 [] node1(X)|node2(X)|node3(X)|node4(X)| -m_main_v_state1(X,c_t1)| -m_main_v_state2(X,c_t2)| -m_main_v_turn(X,c_1)|m_main_v_state1(Y,c_c1)| -node7(X,Y). % 1.82/2.04 0 [] node1(X)|node2(X)|node3(X)|node4(X)|node5(X)| -m_main_v_state1(X,c_c1)|m_main_v_state1(Y,c_n1)| -node7(X,Y). % 1.82/2.04 0 [] node1(X)|node2(X)|node3(X)|node4(X)|node5(X)|m_main_v_state1(X,c_c1)|node6(X,Y)| -node7(X,Y). % 1.82/2.04 0 [] -trans(X,Y)|node7(X,Y). % 1.82/2.04 0 [] m_main_v_state2(X,c_n2)| -node8(X). % 1.82/2.04 0 [] m_main_v_state1(X,c_t1)| -node8(X). % 1.82/2.04 0 [] m_main_v_state2(X,c_n2)| -node9(X). % 1.82/2.04 0 [] m_main_v_state1(X,c_n1)| -node9(X). % 1.82/2.04 0 [] m_main_v_state2(X,c_n2)| -node10(X). % 1.82/2.04 0 [] m_main_v_state1(X,c_c1)| -node10(X). % 1.82/2.04 0 [] m_main_v_state2(X,c_t2)| -node11(X). % 1.82/2.04 0 [] m_main_v_state1(X,c_n1)| -node11(X). % 1.82/2.04 0 [] m_main_v_state2(X,c_t2)| -node12(X). % 1.82/2.04 0 [] m_main_v_state1(X,c_t1)| -node12(X). % 1.82/2.04 0 [] m_main_v_turn(X,c_2)| -node12(X). % 1.82/2.04 0 [] m_main_v_state2(Y,V)| -m_main_v_state2(X,V)| -node13(X,Y). % 1.82/2.04 0 [] -m_main_v_state2(Y,V)|m_main_v_state2(X,V)| -node13(X,Y). % 1.82/2.04 0 [] -m_main_v_state2(X,c_n2)| -m_main_v_state1(X,c_t1)|m_main_v_state2(Y,c_t2)| -node14(X,Y). % 1.82/2.04 0 [] node8(X)| -m_main_v_state2(X,c_n2)| -m_main_v_state1(X,c_n1)|m_main_v_state2(Y,c_t2)| -node14(X,Y). % 1.82/2.04 0 [] node8(X)|node9(X)| -m_main_v_state2(X,c_n2)| -m_main_v_state1(X,c_c1)|m_main_v_state2(Y,c_t2)| -node14(X,Y). % 1.82/2.04 0 [] node8(X)|node9(X)|node10(X)| -m_main_v_state2(X,c_t2)| -m_main_v_state1(X,c_n1)|m_main_v_state2(Y,c_c2)| -node14(X,Y). % 1.82/2.04 0 [] node8(X)|node9(X)|node10(X)|node11(X)| -m_main_v_state2(X,c_t2)| -m_main_v_state1(X,c_t1)| -m_main_v_turn(X,c_2)|m_main_v_state2(Y,c_c2)| -node14(X,Y). % 1.82/2.04 0 [] node8(X)|node9(X)|node10(X)|node11(X)|node12(X)| -m_main_v_state2(X,c_c2)|m_main_v_state2(Y,c_n2)| -node14(X,Y). % 1.82/2.04 0 [] node8(X)|node9(X)|node10(X)|node11(X)|node12(X)|m_main_v_state2(X,c_c2)|node13(X,Y)| -node14(X,Y). % 1.82/2.04 0 [] -trans(X,Y)|node14(X,Y). % 1.82/2.04 0 [] m_main_v_state1(X,c_n1)| -node15(X). % 1.82/2.04 0 [] m_main_v_state2(X,c_t2)| -node15(X). % 1.82/2.04 0 [] m_main_v_state2(X,c_n2)| -node16(X). % 1.82/2.04 0 [] m_main_v_state1(X,c_t1)| -node16(X). % 1.82/2.04 0 [] m_main_v_turn(Y,V)| -m_main_v_turn(X,V)| -node17(X,Y). % 1.82/2.04 0 [] -m_main_v_turn(Y,V)|m_main_v_turn(X,V)| -node17(X,Y). % 1.82/2.04 0 [] -m_main_v_state1(X,c_n1)| -m_main_v_state2(X,c_t2)|m_main_v_turn(Y,c_2)| -node18(X,Y). % 1.82/2.04 0 [] node15(X)| -m_main_v_state2(X,c_n2)| -m_main_v_state1(X,c_t1)|m_main_v_turn(Y,c_1)| -node18(X,Y). % 1.82/2.04 0 [] node15(X)|node16(X)|node17(X,Y)| -node18(X,Y). % 1.82/2.04 0 [] -trans(X,Y)|node18(X,Y). % 1.82/2.04 0 [] -m_main_v_state2(X,c_c2)| -always25(X). % 1.82/2.04 0 [] always25(Y)| -trans(X,Y)| -always25(X). % 1.82/2.04 0 [] loop| -always25(X)| -last(X). % 1.82/2.04 0 [] m_main_v_state2(X,c_t2)| -node26(X). % 1.82/2.04 0 [] always25(X)| -node26(X). % 1.82/2.04 0 [] node26(X)|xuntil28(X)| -until27(X). % 1.82/2.04 0 [] until27(Y)| -succ(X,Y)| -xuntil28(X). % 1.82/2.04 0 [] loop| -last(X)| -xuntil28(X). % 1.82/2.04 0 [] until2p29(Y)| -trans(X,Y)| -last(X)| -xuntil28(X). % 1.82/2.04 0 [] node26(X)|xuntil2p30(X)| -until2p29(X). % 1.82/2.04 0 [] until2p29(Y)| -succ(X,Y)| -xuntil2p30(X). % 1.82/2.04 0 [] -last(X)| -xuntil2p30(X). % 1.82/2.04 0 [] until27(s0). % 1.82/2.04 end_of_list. % 1.82/2.04 % 1.82/2.04 SCAN INPUT: prop=0, horn=0, equality=0, symmetry=0, max_lits=66. % 1.82/2.04 % 1.82/2.04 This is a non-Horn set without equality. The strategy will % 1.82/2.04 be ordered hyper_res, unit deletion, and factoring, with % 1.82/2.04 satellites in sos and with nuclei in usable. % 1.82/2.04 % 1.82/2.04 dependent: set(hyper_res). % 1.82/2.04 dependent: set(factor). % 1.82/2.04 dependent: set(unit_deletion). % 1.82/2.04 % 1.82/2.04 ------------> process usable: % 1.82/2.04 ** KEPT (pick-wt=6): 1 [] -succ(A,B)|trans(A,B). % 1.82/2.04 ** KEPT (pick-wt=196): 2 [] -loop|trans(s64,s0)|trans(s64,s1)|trans(s64,s2)|trans(s64,s3)|trans(s64,s4)|trans(s64,s5)|trans(s64,s6)|trans(s64,s7)|trans(s64,s8)|trans(s64,s9)|trans(s64,s10)|trans(s64,s11)|trans(s64,s12)|trans(s64,s13)|trans(s64,s14)|trans(s64,s15)|trans(s64,s16)|trans(s64,s17)|trans(s64,s18)|trans(s64,s19)|trans(s64,s20)|trans(s64,s21)|trans(s64,s22)|trans(s64,s23)|trans(s64,s24)|trans(s64,s25)|trans(s64,s26)|trans(s64,s27)|trans(s64,s28)|trans(s64,s29)|trans(s64,s30)|trans(s64,s31)|trans(s64,s32)|trans(s64,s33)|trans(s64,s34)|trans(s64,s35)|trans(s64,s36)|trans(s64,s37)|trans(s64,s38)|trans(s64,s39)|trans(s64,s40)|trans(s64,s41)|trans(s64,s42)|trans(s64,s43)|trans(s64,s44)|trans(s64,s45)|trans(s64,s46)|trans(s64,s47)|trans(s64,s48)|trans(s64,s49)|trans(s64,s50)|trans(s64,s51)|trans(s64,s52)|trans(s64,s53)|trans(s64,s54)|trans(s64,s55)|trans(s64,s56)|trans(s64,s57)|trans(s64,s58)|trans(s64,s59)|trans(s64,s60)|trans(s64,s61)|trans(s64,s62)|trans(s64,s63)|trans(s64,s64). % 1.82/2.04 ** KEPT (pick-wt=6): 3 [] -m_main_v_state1(A,c_n1)| -m_main_v_state1(A,c_t1). % 1.82/2.04 ** KEPT (pick-wt=6): 4 [] -m_main_v_state1(A,c_n1)| -m_main_v_state1(A,c_c1). % 1.82/2.04 ** KEPT (pick-wt=6): 5 [] -m_main_v_state1(A,c_t1)| -m_main_v_state1(A,c_c1). % 1.82/2.04 ** KEPT (pick-wt=6): 6 [] -m_main_v_state2(A,c_n2)| -m_main_v_state2(A,c_t2). % 1.82/2.04 ** KEPT (pick-wt=6): 7 [] -m_main_v_state2(A,c_n2)| -m_main_v_state2(A,c_c2). % 1.82/2.04 ** KEPT (pick-wt=6): 8 [] -m_main_v_state2(A,c_t2)| -m_main_v_state2(A,c_c2). % 1.82/2.04 ** KEPT (pick-wt=6): 9 [] -m_main_v_turn(A,c_1)| -m_main_v_turn(A,c_2). % 1.82/2.04 ** KEPT (pick-wt=5): 10 [] m_main_v_state1(A,c_n1)| -node1(A). % 1.82/2.04 ** KEPT (pick-wt=5): 11 [] m_main_v_state2(A,c_t2)| -node1(A). % 1.82/2.04 ** KEPT (pick-wt=5): 12 [] m_main_v_state1(A,c_n1)| -node2(A). % 1.82/2.04 ** KEPT (pick-wt=5): 13 [] m_main_v_state2(A,c_n2)| -node2(A). % 1.82/2.04 ** KEPT (pick-wt=5): 14 [] m_main_v_state1(A,c_n1)| -node3(A). % 1.82/2.04 ** KEPT (pick-wt=5): 15 [] m_main_v_state2(A,c_c2)| -node3(A). % 1.82/2.04 ** KEPT (pick-wt=5): 16 [] m_main_v_state1(A,c_t1)| -node4(A). % 1.82/2.04 ** KEPT (pick-wt=5): 17 [] m_main_v_state2(A,c_n2)| -node4(A). % 1.82/2.04 ** KEPT (pick-wt=5): 18 [] m_main_v_state1(A,c_t1)| -node5(A). % 1.82/2.04 ** KEPT (pick-wt=5): 19 [] m_main_v_state2(A,c_t2)| -node5(A). % 1.82/2.04 ** KEPT (pick-wt=5): 20 [] m_main_v_turn(A,c_1)| -node5(A). % 1.82/2.04 ** KEPT (pick-wt=9): 21 [] m_main_v_state1(A,B)| -m_main_v_state1(C,B)| -node6(C,A). % 1.82/2.04 ** KEPT (pick-wt=9): 22 [] -m_main_v_state1(A,B)|m_main_v_state1(C,B)| -node6(C,A). % 1.82/2.04 ** KEPT (pick-wt=12): 23 [] -m_main_v_state1(A,c_n1)| -m_main_v_state2(A,c_t2)|m_main_v_state1(B,c_t1)| -node7(A,B). % 1.82/2.04 ** KEPT (pick-wt=14): 24 [] node1(A)| -m_main_v_state1(A,c_n1)| -m_main_v_state2(A,c_n2)|m_main_v_state1(B,c_t1)| -node7(A,B). % 1.82/2.04 ** KEPT (pick-wt=16): 25 [] node1(A)|node2(A)| -m_main_v_state1(A,c_n1)| -m_main_v_state2(A,c_c2)|m_main_v_state1(B,c_t1)| -node7(A,B). % 1.82/2.04 ** KEPT (pick-wt=18): 26 [] node1(A)|node2(A)|node3(A)| -m_main_v_state1(A,c_t1)| -m_main_v_state2(A,c_n2)|m_main_v_state1(B,c_c1)| -node7(A,B). % 1.82/2.04 ** KEPT (pick-wt=23): 27 [] node1(A)|node2(A)|node3(A)|node4(A)| -m_main_v_state1(A,c_t1)| -m_main_v_state2(A,c_t2)| -m_main_v_turn(A,c_1)|m_main_v_state1(B,c_c1)| -node7(A,B). % 1.82/2.04 ** KEPT (pick-wt=19): 28 [] node1(A)|node2(A)|node3(A)|node4(A)|node5(A)| -m_main_v_state1(A,c_c1)|m_main_v_state1(B,c_n1)| -node7(A,B). % 1.82/2.04 ** KEPT (pick-wt=19): 29 [] node1(A)|node2(A)|node3(A)|node4(A)|node5(A)|m_main_v_state1(A,c_c1)|node6(A,B)| -node7(A,B). % 1.82/2.04 ** KEPT (pick-wt=6): 30 [] -trans(A,B)|node7(A,B). % 1.82/2.04 ** KEPT (pick-wt=5): 31 [] m_main_v_state2(A,c_n2)| -node8(A). % 1.82/2.04 ** KEPT (pick-wt=5): 32 [] m_main_v_state1(A,c_t1)| -node8(A). % 1.82/2.04 ** KEPT (pick-wt=5): 33 [] m_main_v_state2(A,c_n2)| -node9(A). % 1.82/2.04 ** KEPT (pick-wt=5): 34 [] m_main_v_state1(A,c_n1)| -node9(A). % 1.82/2.04 ** KEPT (pick-wt=5): 35 [] m_main_v_state2(A,c_n2)| -node10(A). % 1.82/2.04 ** KEPT (pick-wt=5): 36 [] m_main_v_state1(A,c_c1)| -node10(A). % 1.82/2.04 ** KEPT (pick-wt=5): 37 [] m_main_v_state2(A,c_t2)| -node11(A). % 1.82/2.04 ** KEPT (pick-wt=5): 38 [] m_main_v_state1(A,c_n1)| -node11(A). % 1.82/2.04 ** KEPT (pick-wt=5): 39 [] m_main_v_state2(A,c_t2)| -node12(A). % 1.82/2.04 ** KEPT (pick-wt=5): 40 [] m_main_v_state1(A,c_t1)| -node12(A). % 1.82/2.04 ** KEPT (pick-wt=5): 41 [] m_main_v_turn(A,c_2)| -node12(A). % 1.82/2.04 ** KEPT (pick-wt=9): 42 [] m_main_v_state2(A,B)| -m_main_v_state2(C,B)| -node13(C,A). % 1.82/2.04 ** KEPT (pick-wt=9): 43 [] -m_main_v_state2(A,B)|m_main_v_state2(C,B)| -node13(C,A). % 1.82/2.04 ** KEPT (pick-wt=12): 44 [] -m_main_v_state2(A,c_n2)| -m_main_v_state1(A,c_t1)|m_main_v_state2(B,c_t2)| -node14(A,B). % 1.82/2.04 ** KEPT (pick-wt=14): 45 [] node8(A)| -m_main_v_state2(A,c_n2)| -m_main_v_state1(A,c_n1)|m_main_v_state2(B,c_t2)| -node14(A,B). % 1.82/2.04 ** KEPT (pick-wt=16): 46 [] node8(A)|node9(A)| -m_main_v_state2(A,c_n2)| -m_main_v_state1(A,c_c1)|m_main_v_state2(B,c_t2)| -node14(A,B). % 1.82/2.04 ** KEPT (pick-wt=18): 47 [] node8(A)|node9(A)|node10(A)| -m_main_v_state2(A,c_t2)| -m_main_v_state1(A,c_n1)|m_main_v_state2(B,c_c2)| -node14(A,B). % 1.82/2.04 ** KEPT (pick-wt=23): 48 [] node8(A)|node9(A)|node10(A)|node11(A)| -m_main_v_state2(A,c_t2)| -m_main_v_state1(A,c_t1)| -m_main_v_turn(A,c_2)|m_main_v_state2(B,c_c2)| -node14(A,B). % 1.82/2.04 ** KEPT (pick-wt=19): 49 [] node8(A)|node9(A)|node10(A)|node11(A)|node12(A)| -m_main_v_state2(A,c_c2)|m_main_v_state2(B,c_n2)| -node14(A,B). % 1.82/2.04 ** KEPT (pick-wt=19): 50 [] node8(A)|node9(A)|node10(A)|node11(A)|node12(A)|m_main_v_state2(A,c_c2)|node13(A,B)| -node14(A,B). % 1.82/2.04 ** KEPT (pick-wt=6): 51 [] -trans(A,B)|node14(A,B). % 1.82/2.04 ** KEPT (pick-wt=5): 52 [] m_main_v_state1(A,c_n1)| -node15(A). % 1.82/2.04 ** KEPT (pick-wt=5): 53 [] m_main_v_state2(A,c_t2)| -node15(A). % 1.82/2.04 ** KEPT (pick-wt=5): 54 [] m_main_v_state2(A,c_n2)| -node16(A). % 1.82/2.04 ** KEPT (pick-wt=5): 55 [] m_main_v_state1(A,c_t1)| -node16(A). % 1.82/2.04 ** KEPT (pick-wt=9): 56 [] m_main_v_turn(A,B)| -m_main_v_turn(C,B)| -node17(C,A). % 1.82/2.04 ** KEPT (pick-wt=9): 57 [] -m_main_v_turn(A,B)|m_main_v_turn(C,B)| -node17(C,A). % 1.82/2.04 ** KEPT (pick-wt=12): 58 [] -m_main_v_state1(A,c_n1)| -m_main_v_state2(A,c_t2)|m_main_v_turn(B,c_2)| -node18(A,B). % 1.82/2.04 ** KEPT (pick-wt=14): 59 [] node15(A)| -m_main_v_state2(A,c_n2)| -m_main_v_state1(A,c_t1)|m_main_v_turn(B,c_1)| -node18(A,B). % 1.82/2.04 ** KEPT (pick-wt=10): 60 [] node15(A)|node16(A)|node17(A,B)| -node18(A,B). % 1.82/2.04 ** KEPT (pick-wt=6): 61 [] -trans(A,B)|node18(A,B). % 1.82/2.04 ** KEPT (pick-wt=5): 62 [] -m_main_v_state2(A,c_c2)| -always25(A). % 1.82/2.04 ** KEPT (pick-wt=7): 63 [] always25(A)| -trans(B,A)| -always25(B). % 1.82/2.04 ** KEPT (pick-wt=5): 64 [] loop| -always25(A)| -last(A). % 1.82/2.04 ** KEPT (pick-wt=5): 65 [] m_main_v_state2(A,c_t2)| -node26(A). % 1.82/2.04 ** KEPT (pick-wt=4): 66 [] always25(A)| -node26(A). % 1.82/2.04 ** KEPT (pick-wt=6): 67 [] node26(A)|xuntil28(A)| -until27(A). % 1.82/2.04 ** KEPT (pick-wt=7): 68 [] until27(A)| -succ(B,A)| -xuntil28(B). % 1.82/2.04 ** KEPT (pick-wt=5): 69 [] loop| -last(A)| -xuntil28(A). % 1.82/2.04 ** KEPT (pick-wt=9): 70 [] until2p29(A)| -trans(B,A)| -last(B)| -xuntil28(B). % 1.82/2.04 ** KEPT (pick-wt=6): 71 [] node26(A)|xuntil2p30(A)| -until2p29(A). % 1.82/2.04 ** KEPT (pick-wt=7): 72 [] until2p29(A)| -succ(B,A)| -xuntil2p30(B). % 1.82/2.04 ** KEPT (pick-wt=4): 73 [] -last(A)| -xuntil2p30(A). % 1.82/2.04 % 1.82/2.04 ------------> process sos: % 1.82/2.04 ** KEPT (pick-wt=3): 74 [] succ(s0,s1). % 1.82/2.04 ** KEPT (pick-wt=3): 75 [] succ(s1,s2). % 1.82/2.04 ** KEPT (pick-wt=3): 76 [] succ(s2,s3). % 1.82/2.04 ** KEPT (pick-wt=3): 77 [] succ(s3,s4). % 1.82/2.04 ** KEPT (pick-wt=3): 78 [] succ(s4,s5). % 1.82/2.04 ** KEPT (pick-wt=3): 79 [] succ(s5,s6). % 1.82/2.04 ** KEPT (pick-wt=3): 80 [] succ(s6,s7). % 1.82/2.04 ** KEPT (pick-wt=3): 81 [] succ(s7,s8). % 1.82/2.04 ** KEPT (pick-wt=3): 82 [] succ(s8,s9). % 1.82/2.04 ** KEPT (pick-wt=3): 83 [] succ(s9,s10). % 1.82/2.04 ** KEPT (pick-wt=3): 84 [] succ(s10,s11). % 1.82/2.04 ** KEPT (pick-wt=3): 85 [] succ(s11,s12). % 1.82/2.04 ** KEPT (pick-wt=3): 86 [] succ(s12,s13). % 1.82/2.04 ** KEPT (pick-wt=3): 87 [] succ(s13,s14). % 1.82/2.04 ** KEPT (pick-wt=3): 88 [] succ(s14,s15). % 1.82/2.04 ** KEPT (pick-wt=3): 89 [] succ(s15,s16). % 1.82/2.04 ** KEPT (pick-wt=3): 90 [] succ(s16,s17). % 1.82/2.04 ** KEPT (pick-wt=3): 91 [] succ(s17,s18). % 1.82/2.04 ** KEPT (pick-wt=3): 92 [] succ(s18,s19). % 1.82/2.04 ** KEPT (pick-wt=3): 93 [] succ(s19,s20). % 1.82/2.04 ** KEPT (pick-wt=3): 94 [] succ(s20,s21). % 1.82/2.04 ** KEPT (pick-wt=3): 95 [] succ(s21,s22). % 1.82/2.04 ** KEPT (pick-wt=3): 96 [] succ(s22,s23). % 1.82/2.04 ** KEPT (pick-wt=3): 97 [] succ(s23,s24). % 1.82/2.04 ** KEPT (pick-wt=3): 98 [] succ(s24,s25). % 1.82/2.04 ** KEPT (pick-wt=3): 99 [] succ(s25,s26). % 1.82/2.04 ** KEPT (pick-wt=3): 100 [] succ(s26,s27). % 1.82/2.04 ** KEPT (pick-wt=3): 101 [] succ(s27,s28). % 1.82/2.04 ** KEPT (pick-wt=3): 102 [] succ(s28,s29). % 1.82/2.04 ** KEPT (pick-wt=3): 103 [] succ(s29,s30). % 1.82/2.04 ** KEPT (pick-wt=3): 104 [] succ(s30,s31). % 1.82/2.04 ** KEPT (pick-wt=3): 105 [] succ(s31,s32). % 1.82/2.04 ** KEPT (pick-wt=3): 106 [] succ(s32,s33). % 1.82/2.04 ** KEPT (pick-wt=3): 107 [] succ(s33,s34). % 1.82/2.04 ** KEPT (pick-wt=3): 108 [] succ(s34,s35). % 1.82/2.04 ** KEPT (pick-wt=3): 109 [] succ(s35,s36). % 1.82/2.04 ** KEPT (pick-wt=3): 110 [] succ(s36,s37). % 1.82/2.04 ** KEPT (pick-wt=3): 111 [] succ(s37,s38). % 1.95/2.12 ** KEPT (pick-wt=3): 112 [] succ(s38,s39). % 1.95/2.12 ** KEPT (pick-wt=3): 113 [] succ(s39,s40). % 1.95/2.12 ** KEPT (pick-wt=3): 114 [] succ(s40,s41). % 1.95/2.12 ** KEPT (pick-wt=3): 115 [] succ(s41,s42). % 1.95/2.12 ** KEPT (pick-wt=3): 116 [] succ(s42,s43). % 1.95/2.12 ** KEPT (pick-wt=3): 117 [] succ(s43,s44). % 1.95/2.12 ** KEPT (pick-wt=3): 118 [] succ(s44,s45). % 1.95/2.12 ** KEPT (pick-wt=3): 119 [] succ(s45,s46). % 1.95/2.12 ** KEPT (pick-wt=3): 120 [] succ(s46,s47). % 1.95/2.12 ** KEPT (pick-wt=3): 121 [] succ(s47,s48). % 1.95/2.12 ** KEPT (pick-wt=3): 122 [] succ(s48,s49). % 1.95/2.12 ** KEPT (pick-wt=3): 123 [] succ(s49,s50). % 1.95/2.12 ** KEPT (pick-wt=3): 124 [] succ(s50,s51). % 1.95/2.12 ** KEPT (pick-wt=3): 125 [] succ(s51,s52). % 1.95/2.12 ** KEPT (pick-wt=3): 126 [] succ(s52,s53). % 1.95/2.12 ** KEPT (pick-wt=3): 127 [] succ(s53,s54). % 1.95/2.12 ** KEPT (pick-wt=3): 128 [] succ(s54,s55). % 1.95/2.12 ** KEPT (pick-wt=3): 129 [] succ(s55,s56). % 1.95/2.12 ** KEPT (pick-wt=3): 130 [] succ(s56,s57). % 1.95/2.12 ** KEPT (pick-wt=3): 131 [] succ(s57,s58). % 1.95/2.12 ** KEPT (pick-wt=3): 132 [] succ(s58,s59). % 1.95/2.12 ** KEPT (pick-wt=3): 133 [] succ(s59,s60). % 1.95/2.12 ** KEPT (pick-wt=3): 134 [] succ(s60,s61). % 1.95/2.12 ** KEPT (pick-wt=3): 135 [] succ(s61,s62). % 1.95/2.12 ** KEPT (pick-wt=3): 136 [] succ(s62,s63). % 1.95/2.12 ** KEPT (pick-wt=3): 137 [] succ(s63,s64). % 1.95/2.12 ** KEPT (pick-wt=2): 138 [] last(s64). % 1.95/2.12 ** KEPT (pick-wt=9): 139 [] m_main_v_state1(A,c_n1)|m_main_v_state1(A,c_t1)|m_main_v_state1(A,c_c1). % 1.95/2.12 ** KEPT (pick-wt=9): 140 [] m_main_v_state2(A,c_n2)|m_main_v_state2(A,c_t2)|m_main_v_state2(A,c_c2). % 1.95/2.12 ** KEPT (pick-wt=6): 141 [] m_main_v_turn(A,c_1)|m_main_v_turn(A,c_2). % 1.95/2.12 ** KEPT (pick-wt=3): 142 [] m_main_v_state1(s0,c_n1). % 1.95/2.12 ** KEPT (pick-wt=3): 143 [] m_main_v_state2(s0,c_n2). % 1.95/2.12 ** KEPT (pick-wt=3): 144 [] m_main_v_turn(s0,c_1). % 1.95/2.12 ** KEPT (pick-wt=2): 145 [] until27(s0). % 1.95/2.12 % 1.95/2.12 ======= end of input processing ======= % 1.95/2.12 % 1.95/2.12 =========== start of search =========== % 1.95/2.12 % 1.95/2.12 % 1.95/2.12 Resetting weight limit to 3. % 1.95/2.12 % 1.95/2.12 % 1.95/2.12 Resetting weight limit to 3. % 1.95/2.12 % 1.95/2.12 sos_size=608 % 1.95/2.12 % 1.95/2.12 Search stopped because sos empty. % 1.95/2.12 % 1.95/2.12 % 1.95/2.12 Search stopped because sos empty. % 1.95/2.12 % 1.95/2.12 ============ end of search ============ % 1.95/2.12 % 1.95/2.12 -------------- statistics ------------- % 1.95/2.12 clauses given 839 % 1.95/2.12 clauses generated 3576 % 1.95/2.12 clauses kept 912 % 1.95/2.12 clauses forward subsumed 46 % 1.95/2.12 clauses back subsumed 0 % 1.95/2.12 Kbytes malloced 5859 % 1.95/2.12 % 1.95/2.12 ----------- times (seconds) ----------- % 1.95/2.12 user CPU time 0.09 (0 hr, 0 min, 0 sec) % 1.95/2.12 system CPU time 0.00 (0 hr, 0 min, 0 sec) % 1.95/2.12 wall-clock time 2 (0 hr, 0 min, 2 sec) % 1.95/2.12 % 1.95/2.12 Process 19194 finished Wed Jul 27 06:00:52 2022 % 1.95/2.12 Otter interrupted % 1.95/2.12 PROOF NOT FOUND %------------------------------------------------------------------------------