%------------------------------------------------------------------------------ % File : Otter---3.3 % Problem : SWW095+1 : TPTP v8.1.0. Released v5.2.0. % Transfm : none % Format : tptp:raw % Command : otter-tptp-script %s % Computer : n010.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:22:00 EDT 2022 % Result : Unknown 24.35s 24.52s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.11 % Problem : SWW095+1 : TPTP v8.1.0. Released v5.2.0. % 0.12/0.12 % Command : otter-tptp-script %s % 0.12/0.33 % Computer : n010.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Wed Jul 27 02:50:54 EDT 2022 % 0.12/0.33 % CPUTime : % 3.24/3.39 ----- Otter 3.3f, August 2004 ----- % 3.24/3.39 The process was started by sandbox2 on n010.cluster.edu, % 3.24/3.39 Wed Jul 27 02:50:55 2022 % 3.24/3.39 The command was "./otter". The process ID is 18445. % 3.24/3.39 % 3.24/3.39 set(prolog_style_variables). % 3.24/3.39 set(auto). % 3.24/3.39 dependent: set(auto1). % 3.24/3.39 dependent: set(process_input). % 3.24/3.39 dependent: clear(print_kept). % 3.24/3.39 dependent: clear(print_new_demod). % 3.24/3.39 dependent: clear(print_back_demod). % 3.24/3.39 dependent: clear(print_back_sub). % 3.24/3.39 dependent: set(control_memory). % 3.24/3.39 dependent: assign(max_mem, 12000). % 3.24/3.39 dependent: assign(pick_given_ratio, 4). % 3.24/3.39 dependent: assign(stats_level, 1). % 3.24/3.39 dependent: assign(max_seconds, 10800). % 3.24/3.39 clear(print_given). % 3.24/3.39 % 3.24/3.39 formula_list(usable). % 3.24/3.39 all A (A=A). % 3.24/3.39 all X (-integer(X)|lte_q(X,X)). % 3.24/3.39 all X Y (-(integer(X)&integer(Y))| -(lte_q(X,Y)<e_q(Y,X))|X=Y). % 3.24/3.39 all X Y Z (-(integer(X)&integer(Y)&integer(Z))| -(lte_q(X,Y)<e_q(Y,Z))|lte_q(X,Z)). % 3.24/3.39 all X Y (-(integer(X)&integer(Y))|lte_q(X,Y)|lte_q(Y,X)). % 3.24/3.39 all X Y (-(integer(X)&integer(Y))| (-lte_q(X,Y)|X=Y| -lte_q(Y,X))& (-(X=Y| -lte_q(Y,X))|lte_q(X,Y))). % 3.24/3.39 object(nn). % 3.24/3.39 object(tmp_6_2). % 3.24/3.39 object(prev_2). % 3.24/3.39 all V__ object(node_value(V__)). % 3.24/3.39 all V__ integer(node_key(V__)). % 3.24/3.39 object(null). % 3.24/3.39 all V__ I__ object(array_arrayState(V__,I__)). % 3.24/3.39 object(sortedList_first). % 3.24/3.39 all V__ object(node_next(V__)). % 3.24/3.39 null=node_next(null). % 3.24/3.39 all T1 T2 T3 (-(object(T1)&object(T2)&object(T3))| -v__1(T1,T2,T2)| -v__1(T2,T3,T3)|v__1(T1,T3,T3)). % 3.24/3.39 all T T0 T1_1 T2_1 (-(object(T)&object(T0)&object(T1_1)&object(T2_1))| -v__1(T0,T1_1,T2_1)| -v__1(T1_1,T,T2_1)|v__1(T0,T1_1,T)&v__1(T0,T,T2_1)). % 3.24/3.39 all T_1 T0_1 T1_2 T2_2 (-(object(T_1)&object(T0_1)&object(T1_2)&object(T2_2))| -v__1(T0_1,T1_2,T2_2)| -v__1(T0_1,T_1,T1_2)|v__1(T0_1,T_1,T2_2)&v__1(T_1,T1_2,T2_2)). % 3.24/3.39 all T1_3 T2_3 T3_1 (-(object(T1_3)&object(T2_3)&object(T3_1))| -v__1(T1_3,T2_3,T2_3)| -v__1(T1_3,T3_1,T3_1)|v__1(T1_3,T2_3,T3_1)|v__1(T1_3,T3_1,T2_3)). % 3.24/3.39 all T1_4 T2_4 T3_2 (-(object(T1_4)&object(T2_4)&object(T3_2))| -v__1(T1_4,T2_4,T3_2)|v__1(T1_4,T2_4,T2_4)&v__1(T2_4,T3_2,T3_2)). % 3.24/3.39 all T_2 (-object(T_2)|v__1(T_2,T_2,T_2)). % 3.24/3.39 all T1_5 T2_5 (-(object(T1_5)&object(T2_5))| -v__1(T1_5,T2_5,T1_5)|T1_5=T2_5). % 3.24/3.39 all T1_6 T2_6 (-(object(T1_6)&object(T2_6))|T1_6!=node_next(T1_6)| -v__1(T1_6,T2_6,T2_6)|T1_6=T2_6). % 3.24/3.39 all T_3 (-object(T_3)| (all Fun_flat_foltrans_156 Fun_flat_foltrans_155 (-(object(Fun_flat_foltrans_156)&object(Fun_flat_foltrans_155))|Fun_flat_foltrans_156!=node_next(T_3)|Fun_flat_foltrans_155!=node_next(T_3)|v__1(T_3,Fun_flat_foltrans_156,Fun_flat_foltrans_155)))). % 3.24/3.39 all T1_7 T2_7 (-(object(T1_7)&object(T2_7))| -v__1(T1_7,T2_7,T2_7)|T1_7=T2_7| (all Fun_flat_foltrans_157 (-object(Fun_flat_foltrans_157)|Fun_flat_foltrans_157!=node_next(T1_7)|v__1(T1_7,Fun_flat_foltrans_157,T2_7)))). % 3.24/3.39 prev_2!=null. % 3.24/3.39 exists Fun_flat_foltrans_159 Fun_flat_foltrans_158 (integer(Fun_flat_foltrans_159)&integer(Fun_flat_foltrans_158)<e_q(Fun_flat_foltrans_159,Fun_flat_foltrans_158)&Fun_flat_foltrans_159=node_key(nn)&Fun_flat_foltrans_158=node_key(nn)). % 3.24/3.39 nn!=null. % 3.24/3.39 null=node_next(null). % 3.24/3.39 v__1(nn,nn,nn)|nn=null| -v__1(sortedList_first,nn,nn). % 3.24/3.39 prev_2=null|prev_2!=null&v__1(sortedList_first,prev_2,prev_2). % 3.24/3.39 nn=null|nn!=null&v__1(sortedList_first,nn,nn). % 3.24/3.39 prev_2!=null|nn=sortedList_first. % 3.24/3.39 prev_2=null|nn=node_next(prev_2). % 3.24/3.39 node(prev_2). % 3.24/3.39 object_alloc(prev_2). % 3.24/3.39 node(tmp_6_2). % 3.24/3.39 object_alloc(tmp_6_2). % 3.24/3.39 node(nn). % 3.24/3.39 object_alloc(nn). % 3.24/3.39 all Z_setinc_foltrans_3 (-object(Z_setinc_foltrans_3)| -object_alloc(Z_setinc_foltrans_3)|object_alloc(Z_setinc_foltrans_3)). % 3.24/3.39 object_alloc(nn). % 3.24/3.39 node(nn). % 3.24/3.39 all X Y (-(object(X)&object(Y))| -v__1(sortedList_first,X,X)|X=null| (all Fun_flat_foltrans_160 (-object(Fun_flat_foltrans_160)| -v__1(Fun_flat_foltrans_160,Y,Y)|Fun_flat_foltrans_160!=node_next(X)))|Y=null| (all Fun_flat_foltrans_162 Fun_flat_foltrans_161 (-(integer(Fun_flat_foltrans_162)&integer(Fun_flat_foltrans_161))|Fun_flat_foltrans_162!=node_key(X)|Fun_flat_foltrans_161!=node_key(Y)|lte_q(Fun_flat_foltrans_162,Fun_flat_foltrans_161)))& (all T_e_qof_foltrans_1 (-integer(T_e_qof_foltrans_1)|T_e_qof_foltrans_1!=node_key(X)|T_e_qof_foltrans_1!=node_key(Y)))). % 3.24/3.39 all X_2 N (-(object(X_2)&object(N))|X_2=null|N=null|N!=node_next(X_2)|N!=null&v__1(sortedList_first,N,N)). % 24.35/24.52 sortedList_first=null| (all N_1 (-object(N_1)|sortedList_first!=node_next(N_1))). % 24.35/24.52 nn!=null. % 24.35/24.52 node(sortedList_first). % 24.35/24.52 all X_3 (-object(X_3)|object_alloc(X_3)| (all Y_1 (-object(Y_1)|X_3!=node_value(Y_1)))& (all Y_2 (-object(Y_2)|X_3!=node_next(Y_2)))& (all Z I (-(object(Z)&integer(I))|X_3!=array_arrayState(Z,I)))&sortedList_first!=X_3&null=node_value(X_3)&null=node_next(X_3)& (all J (-integer(J)|null=array_arrayState(X_3,J)))). % 24.35/24.52 all Pto_foltrans_1 (-object(Pto_foltrans_1)| -node(Pto_foltrans_1)| (all T_ms1_foltrans_1 (-object(T_ms1_foltrans_1)|T_ms1_foltrans_1!=node_next(Pto_foltrans_1)|node(T_ms1_foltrans_1)))). % 24.35/24.52 object_alloc(sortedList_first). % 24.35/24.52 object_alloc(null). % 24.35/24.52 all Z_setinc_foltrans_5 (-object(Z_setinc_foltrans_5)| -sortedList(Z_setinc_foltrans_5)| -node(Z_setinc_foltrans_5)|Z_setinc_foltrans_5=null). % 24.35/24.52 all Z_setinc_foltrans_4 (-object(Z_setinc_foltrans_4)|Z_setinc_foltrans_4!=null|sortedList(Z_setinc_foltrans_4)&node(Z_setinc_foltrans_4)). % 24.35/24.52 all Z_setinc_foltrans_7 (-object(Z_setinc_foltrans_7)| -sortedList(Z_setinc_foltrans_7)| -array(Z_setinc_foltrans_7)|Z_setinc_foltrans_7=null). % 24.35/24.52 all Z_setinc_foltrans_6 (-object(Z_setinc_foltrans_6)|Z_setinc_foltrans_6!=null|sortedList(Z_setinc_foltrans_6)&array(Z_setinc_foltrans_6)). % 24.35/24.52 all Z_setinc_foltrans_9 (-object(Z_setinc_foltrans_9)| -node(Z_setinc_foltrans_9)| -array(Z_setinc_foltrans_9)|Z_setinc_foltrans_9=null). % 24.35/24.52 all Z_setinc_foltrans_8 (-object(Z_setinc_foltrans_8)|Z_setinc_foltrans_8!=null|node(Z_setinc_foltrans_8)&array(Z_setinc_foltrans_8)). % 24.35/24.52 all XObj (-object(XObj)|object(XObj)). % 24.35/24.52 null=node_next(null). % 24.35/24.52 null=node_value(null). % 24.35/24.52 -(all Z_setinc_foltrans_2 (-object(Z_setinc_foltrans_2)|Z_setinc_foltrans_2=null| ((-v__1(sortedList_first,Z_setinc_foltrans_2,Z_setinc_foltrans_2)| -v__1(sortedList_first,Z_setinc_foltrans_2,nn)& (-v__1(sortedList_first,Z_setinc_foltrans_2,Z_setinc_foltrans_2)|v__1(sortedList_first,nn,nn)))& (nn=Z_setinc_foltrans_2| -v__1(sortedList_first,nn,Z_setinc_foltrans_2)& (-v__1(sortedList_first,nn,nn)|v__1(sortedList_first,Z_setinc_foltrans_2,Z_setinc_foltrans_2))| -v__1(sortedList_first,Z_setinc_foltrans_2,nn)| -v__1(null,Z_setinc_foltrans_2,nn)& (-v__1(null,Z_setinc_foltrans_2,Z_setinc_foltrans_2)|v__1(null,nn,nn)))& (nn=Z_setinc_foltrans_2| -v__1(sortedList_first,nn,Z_setinc_foltrans_2)& (-v__1(sortedList_first,nn,nn)|v__1(sortedList_first,Z_setinc_foltrans_2,Z_setinc_foltrans_2))| -v__1(null,Z_setinc_foltrans_2,Z_setinc_foltrans_2)| -v__1(null,Z_setinc_foltrans_2,nn)& (-v__1(null,Z_setinc_foltrans_2,Z_setinc_foltrans_2)|v__1(null,nn,nn)))| (-v__1(sortedList_first,Z_setinc_foltrans_2,prev_2)| -v__1(sortedList_first,prev_2,nn)& (-v__1(sortedList_first,prev_2,prev_2)|v__1(sortedList_first,nn,nn)))& (nn=prev_2| -v__1(sortedList_first,nn,prev_2)& (-v__1(sortedList_first,nn,nn)|v__1(sortedList_first,prev_2,prev_2))| -v__1(sortedList_first,Z_setinc_foltrans_2,nn)| -v__1(null,prev_2,nn)& (-v__1(null,prev_2,prev_2)|v__1(null,nn,nn)))& (nn=prev_2| -v__1(sortedList_first,nn,prev_2)& (-v__1(sortedList_first,nn,nn)|v__1(sortedList_first,prev_2,prev_2))| -v__1(null,Z_setinc_foltrans_2,prev_2)| -v__1(null,prev_2,nn)& (-v__1(null,prev_2,prev_2)|v__1(null,nn,nn)))& ((-v__1(sortedList_first,Z_setinc_foltrans_2,Z_setinc_foltrans_2)| -v__1(sortedList_first,Z_setinc_foltrans_2,nn)& (-v__1(sortedList_first,Z_setinc_foltrans_2,Z_setinc_foltrans_2)|v__1(sortedList_first,nn,nn)))& (nn=Z_setinc_foltrans_2| -v__1(sortedList_first,nn,Z_setinc_foltrans_2)& (-v__1(sortedList_first,nn,nn)|v__1(sortedList_first,Z_setinc_foltrans_2,Z_setinc_foltrans_2))| -v__1(sortedList_first,Z_setinc_foltrans_2,nn)| -v__1(null,Z_setinc_foltrans_2,nn)& (-v__1(null,Z_setinc_foltrans_2,Z_setinc_foltrans_2)|v__1(null,nn,nn)))& (nn=Z_setinc_foltrans_2| -v__1(sortedList_first,nn,Z_setinc_foltrans_2)& (-v__1(sortedList_first,nn,nn)|v__1(sortedList_first,Z_setinc_foltrans_2,Z_setinc_foltrans_2))| -v__1(null,Z_setinc_foltrans_2,Z_setinc_foltrans_2)| -v__1(null,Z_setinc_foltrans_2,nn)& (-v__1(null,Z_setinc_foltrans_2,Z_setinc_foltrans_2)|v__1(null,nn,nn)))|v__1(sortedList_first,prev_2,prev_2)& (v__1(sortedList_first,prev_2,nn)|v__1(sortedList_first,prev_2,prev_2)& -v__1(sortedList_first,nn,nn))|nn!=prev_2&v__1(sortedList_first,prev_2,nn)& (v__1(null,prev_2,nn)|v__1(null,prev_2,prev_2)& -v__1(null,nn,nn))& (v__1(sortedList_first,nn,prev_2)|v__1(sortedList_first,nn,nn)& -v__1(sortedList_first,prev_2,prev_2))|nn!=prev_2&v__1(null,prev_2,prev_2)& (v__1(null,prev_2,nn)|v__1(null,prev_2,prev_2)& -v__1(null,nn,nn))& (v__1(sortedList_first,nn,prev_2)|v__1(sortedList_first,nn,nn)& -v__1(sortedList_first,prev_2,prev_2))))& (prev_2=Z_setinc_foltrans_2| (-v__1(sortedList_first,prev_2,Z_setinc_foltrans_2)| -v__1(sortedList_first,Z_setinc_foltrans_2,nn)& (-v__1(sortedList_first,Z_setinc_foltrans_2,Z_setinc_foltrans_2)|v__1(sortedList_first,nn,nn)))& (nn=Z_setinc_foltrans_2| -v__1(sortedList_first,nn,Z_setinc_foltrans_2)& (-v__1(sortedList_first,nn,nn)|v__1(sortedList_first,Z_setinc_foltrans_2,Z_setinc_foltrans_2))| -v__1(sortedList_first,prev_2,nn)| -v__1(null,Z_setinc_foltrans_2,nn)& (-v__1(null,Z_setinc_foltrans_2,Z_setinc_foltrans_2)|v__1(null,nn,nn)))& (nn=Z_setinc_foltrans_2| -v__1(sortedList_first,nn,Z_setinc_foltrans_2)& (-v__1(sortedList_first,nn,nn)|v__1(sortedList_first,Z_setinc_foltrans_2,Z_setinc_foltrans_2))| -v__1(null,prev_2,Z_setinc_foltrans_2)| -v__1(null,Z_setinc_foltrans_2,nn)& (-v__1(null,Z_setinc_foltrans_2,Z_setinc_foltrans_2)|v__1(null,nn,nn)))& ((-v__1(sortedList_first,prev_2,prev_2)| -v__1(sortedList_first,prev_2,nn)& (-v__1(sortedList_first,prev_2,prev_2)|v__1(sortedList_first,nn,nn)))& (nn=prev_2| -v__1(sortedList_first,nn,prev_2)& (-v__1(sortedList_first,nn,nn)|v__1(sortedList_first,prev_2,prev_2))| -v__1(sortedList_first,prev_2,nn)| -v__1(null,prev_2,nn)& (-v__1(null,prev_2,prev_2)|v__1(null,nn,nn)))& (nn=prev_2| -v__1(sortedList_first,nn,prev_2)& (-v__1(sortedList_first,nn,nn)|v__1(sortedList_first,prev_2,prev_2))| -v__1(null,prev_2,prev_2)| -v__1(null,prev_2,nn)& (-v__1(null,prev_2,prev_2)|v__1(null,nn,nn)))|v__1(sortedList_first,Z_setinc_foltrans_2,Z_setinc_foltrans_2)& (v__1(sortedList_first,Z_setinc_foltrans_2,nn)|v__1(sortedList_first,Z_setinc_foltrans_2,Z_setinc_foltrans_2)& -v__1(sortedList_first,nn,nn))|nn!=Z_setinc_foltrans_2&v__1(sortedList_first,Z_setinc_foltrans_2,nn)& (v__1(null,Z_setinc_foltrans_2,nn)|v__1(null,Z_setinc_foltrans_2,Z_setinc_foltrans_2)& -v__1(null,nn,nn))& (v__1(sortedList_first,nn,Z_setinc_foltrans_2)|v__1(sortedList_first,nn,nn)& -v__1(sortedList_first,Z_setinc_foltrans_2,Z_setinc_foltrans_2))|nn!=Z_setinc_foltrans_2&v__1(null,Z_setinc_foltrans_2,Z_setinc_foltrans_2)& (v__1(null,Z_setinc_foltrans_2,nn)|v__1(null,Z_setinc_foltrans_2,Z_setinc_foltrans_2)& -v__1(null,nn,nn))& (v__1(sortedList_first,nn,Z_setinc_foltrans_2)|v__1(sortedList_first,nn,nn)& -v__1(sortedList_first,Z_setinc_foltrans_2,Z_setinc_foltrans_2)))| (-v__1(sortedList_first,Z_setinc_foltrans_2,prev_2)| -v__1(sortedList_first,prev_2,nn)& (-v__1(sortedList_first,prev_2,prev_2)|v__1(sortedList_first,nn,nn)))& (nn=prev_2| -v__1(sortedList_first,nn,prev_2)& (-v__1(sortedList_first,nn,nn)|v__1(sortedList_first,prev_2,prev_2))| -v__1(sortedList_first,Z_setinc_foltrans_2,nn)| -v__1(null,prev_2,nn)& (-v__1(null,prev_2,prev_2)|v__1(null,nn,nn)))& (nn=prev_2| -v__1(sortedList_first,nn,prev_2)& (-v__1(sortedList_first,nn,nn)|v__1(sortedList_first,prev_2,prev_2))| -v__1(null,Z_setinc_foltrans_2,prev_2)| -v__1(null,prev_2,nn)& (-v__1(null,prev_2,prev_2)|v__1(null,nn,nn)))| ((all Fun_flat_foltrans_1 (-object(Fun_flat_foltrans_1)| -v__1(Fun_flat_foltrans_1,Z_setinc_foltrans_2,prev_2)|Fun_flat_foltrans_1!=node_next(nn)))| (all Fun_flat_foltrans_2 (-object(Fun_flat_foltrans_2)| -v__1(Fun_flat_foltrans_2,prev_2,nn)|Fun_flat_foltrans_2!=node_next(nn)))& ((all Fun_flat_foltrans_3 (-object(Fun_flat_foltrans_3)| -v__1(Fun_flat_foltrans_3,prev_2,prev_2)|Fun_flat_foltrans_3!=node_next(nn)))| (all Fun_flat_foltrans_4 (-object(Fun_flat_foltrans_4)|Fun_flat_foltrans_4!=node_next(nn)|v__1(Fun_flat_foltrans_4,nn,nn)))))& (nn=prev_2| (all Fun_flat_foltrans_5 (-object(Fun_flat_foltrans_5)| -v__1(Fun_flat_foltrans_5,nn,prev_2)|Fun_flat_foltrans_5!=node_next(nn)))& ((all Fun_flat_foltrans_6 (-object(Fun_flat_foltrans_6)| -v__1(Fun_flat_foltrans_6,nn,nn)|Fun_flat_foltrans_6!=node_next(nn)))| (all Fun_flat_foltrans_7 (-object(Fun_flat_foltrans_7)|Fun_flat_foltrans_7!=node_next(nn)|v__1(Fun_flat_foltrans_7,prev_2,prev_2))))| (all Fun_flat_foltrans_8 (-object(Fun_flat_foltrans_8)| -v__1(Fun_flat_foltrans_8,Z_setinc_foltrans_2,nn)|Fun_flat_foltrans_8!=node_next(nn)))| -v__1(null,prev_2,nn)& (-v__1(null,prev_2,prev_2)|v__1(null,nn,nn)))& (nn=prev_2| (all Fun_flat_foltrans_9 (-object(Fun_flat_foltrans_9)| -v__1(Fun_flat_foltrans_9,nn,prev_2)|Fun_flat_foltrans_9!=node_next(nn)))& ((all Fun_flat_foltrans_10 (-object(Fun_flat_foltrans_10)| -v__1(Fun_flat_foltrans_10,nn,nn)|Fun_flat_foltrans_10!=node_next(nn)))| (all Fun_flat_foltrans_11 (-object(Fun_flat_foltrans_11)|Fun_flat_foltrans_11!=node_next(nn)|v__1(Fun_flat_foltrans_11,prev_2,prev_2))))| -v__1(null,Z_setinc_foltrans_2,prev_2)| -v__1(null,prev_2,nn)& (-v__1(null,prev_2,prev_2)|v__1(null,nn,nn)))& (((all Fun_flat_foltrans_12 (-object(Fun_flat_foltrans_12)| -v__1(Fun_flat_foltrans_12,Z_setinc_foltrans_2,Z_setinc_foltrans_2)|Fun_flat_foltrans_12!=node_next(nn)))| (all Fun_flat_foltrans_13 (-object(Fun_flat_foltrans_13)| -v__1(Fun_flat_foltrans_13,Z_setinc_foltrans_2,nn)|Fun_flat_foltrans_13!=node_next(nn)))& ((all Fun_flat_foltrans_14 (-object(Fun_flat_foltrans_14)| -v__1(Fun_flat_foltrans_14,Z_setinc_foltrans_2,Z_setinc_foltrans_2)|Fun_flat_foltrans_14!=node_next(nn)))| (all Fun_flat_foltrans_15 (-object(Fun_flat_foltrans_15)|Fun_flat_foltrans_15!=node_next(nn)|v__1(Fun_flat_foltrans_15,nn,nn)))))& (nn=Z_setinc_foltrans_2| (all Fun_flat_foltrans_16 (-object(Fun_flat_foltrans_16)| -v__1(Fun_flat_foltrans_16,nn,Z_setinc_foltrans_2)|Fun_flat_foltrans_16!=node_next(nn)))& ((all Fun_flat_foltrans_17 (-object(Fun_flat_foltrans_17)| -v__1(Fun_flat_foltrans_17,nn,nn)|Fun_flat_foltrans_17!=node_next(nn)))| (all Fun_flat_foltrans_18 (-object(Fun_flat_foltrans_18)|Fun_flat_foltrans_18!=node_next(nn)|v__1(Fun_flat_foltrans_18,Z_setinc_foltrans_2,Z_setinc_foltrans_2))))| (all Fun_flat_foltrans_19 (-object(Fun_flat_foltrans_19)| -v__1(Fun_flat_foltrans_19,Z_setinc_foltrans_2,nn)|Fun_flat_foltrans_19!=node_next(nn)))| -v__1(null,Z_setinc_foltrans_2,nn)& (-v__1(null,Z_setinc_foltrans_2,Z_setinc_foltrans_2)|v__1(null,nn,nn)))& (nn=Z_setinc_foltrans_2| (all Fun_flat_foltrans_20 (-object(Fun_flat_foltrans_20)| -v__1(Fun_flat_foltrans_20,nn,Z_setinc_foltrans_2)|Fun_flat_foltrans_20!=node_next(nn)))& ((all Fun_flat_foltrans_21 (-object(Fun_flat_foltrans_21)| -v__1(Fun_flat_foltrans_21,nn,nn)|Fun_flat_foltrans_21!=node_next(nn)))| (all Fun_flat_foltrans_22 (-object(Fun_flat_foltrans_22)|Fun_flat_foltrans_22!=node_next(nn)|v__1(Fun_flat_foltrans_22,Z_setinc_foltrans_2,Z_setinc_foltrans_2))))| -v__1(null,Z_setinc_foltrans_2,Z_setinc_foltrans_2)| -v__1(null,Z_setinc_foltrans_2,nn)& (-v__1(null,Z_setinc_foltrans_2,Z_setinc_foltrans_2)|v__1(null,nn,nn)))| (all Fun_flat_foltrans_23 (-object(Fun_flat_foltrans_23)|Fun_flat_foltrans_23!=node_next(nn)|v__1(Fun_flat_foltrans_23,prev_2,prev_2)))& ((all Fun_flat_foltrans_24 (-object(Fun_flat_foltrans_24)|Fun_flat_foltrans_24!=node_next(nn)|v__1(Fun_flat_foltrans_24,prev_2,nn)))| (all Fun_flat_foltrans_25 (-object(Fun_flat_foltrans_25)|Fun_flat_foltrans_25!=node_next(nn)|v__1(Fun_flat_foltrans_25,prev_2,prev_2)))& (all Fun_flat_foltrans_26 (-object(Fun_flat_foltrans_26)| -v__1(Fun_flat_foltrans_26,nn,nn)|Fun_flat_foltrans_26!=node_next(nn))))|nn!=prev_2& (all Fun_flat_foltrans_27 (-object(Fun_flat_foltrans_27)|Fun_flat_foltrans_27!=node_next(nn)|v__1(Fun_flat_foltrans_27,prev_2,nn)))& (v__1(null,prev_2,nn)|v__1(null,prev_2,prev_2)& -v__1(null,nn,nn))& ((all Fun_flat_foltrans_28 (-object(Fun_flat_foltrans_28)|Fun_flat_foltrans_28!=node_next(nn)|v__1(Fun_flat_foltrans_28,nn,prev_2)))| (all Fun_flat_foltrans_29 (-object(Fun_flat_foltrans_29)|Fun_flat_foltrans_29!=node_next(nn)|v__1(Fun_flat_foltrans_29,nn,nn)))& (all Fun_flat_foltrans_30 (-object(Fun_flat_foltrans_30)| -v__1(Fun_flat_foltrans_30,prev_2,prev_2)|Fun_flat_foltrans_30!=node_next(nn))))|nn!=prev_2&v__1(null,prev_2,prev_2)& (v__1(null,prev_2,nn)|v__1(null,prev_2,prev_2)& -v__1(null,nn,nn))& ((all Fun_flat_foltrans_31 (-object(Fun_flat_foltrans_31)|Fun_flat_foltrans_31!=node_next(nn)|v__1(Fun_flat_foltrans_31,nn,prev_2)))| (all Fun_flat_foltrans_32 (-object(Fun_flat_foltrans_32)|Fun_flat_foltrans_32!=node_next(nn)|v__1(Fun_flat_foltrans_32,nn,nn)))& (all Fun_flat_foltrans_33 (-object(Fun_flat_foltrans_33)| -v__1(Fun_flat_foltrans_33,prev_2,prev_2)|Fun_flat_foltrans_33!=node_next(nn))))))& (prev_2=Z_setinc_foltrans_2| (-v__1(sortedList_first,prev_2,Z_setinc_foltrans_2)| -v__1(sortedList_first,Z_setinc_foltrans_2,nn)& (-v__1(sortedList_first,Z_setinc_foltrans_2,Z_setinc_foltrans_2)|v__1(sortedList_first,nn,nn)))& (nn=Z_setinc_foltrans_2| -v__1(sortedList_first,nn,Z_setinc_foltrans_2)& (-v__1(sortedList_first,nn,nn)|v__1(sortedList_first,Z_setinc_foltrans_2,Z_setinc_foltrans_2))| -v__1(sortedList_first,prev_2,nn)| -v__1(null,Z_setinc_foltrans_2,nn)& (-v__1(null,Z_setinc_foltrans_2,Z_setinc_foltrans_2)|v__1(null,nn,nn)))& (nn=Z_setinc_foltrans_2| -v__1(sortedList_first,nn,Z_setinc_foltrans_2)& (-v__1(sortedList_first,nn,nn)|v__1(sortedList_first,Z_setinc_foltrans_2,Z_setinc_foltrans_2))| -v__1(null,prev_2,Z_setinc_foltrans_2)| -v__1(null,Z_setinc_foltrans_2,nn)& (-v__1(null,Z_setinc_foltrans_2,Z_setinc_foltrans_2)|v__1(null,nn,nn)))& ((-v__1(sortedList_first,prev_2,prev_2)| -v__1(sortedList_first,prev_2,nn)& (-v__1(sortedList_first,prev_2,prev_2)|v__1(sortedList_first,nn,nn)))& (nn=prev_2| -v__1(sortedList_first,nn,prev_2)& (-v__1(sortedList_first,nn,nn)|v__1(sortedList_first,prev_2,prev_2))| -v__1(sortedList_first,prev_2,nn)| -v__1(null,prev_2,nn)& (-v__1(null,prev_2,prev_2)|v__1(null,nn,nn)))& (nn=prev_2| -v__1(sortedList_first,nn,prev_2)& (-v__1(sortedList_first,nn,nn)|v__1(sortedList_first,prev_2,prev_2))| -v__1(null,prev_2,prev_2)| -v__1(null,prev_2,nn)& (-v__1(null,prev_2,prev_2)|v__1(null,nn,nn)))|v__1(sortedList_first,Z_setinc_foltrans_2,Z_setinc_foltrans_2)& (v__1(sortedList_first,Z_setinc_foltrans_2,nn)|v__1(sortedList_first,Z_setinc_foltrans_2,Z_setinc_foltrans_2)& -v__1(sortedList_first,nn,nn))|nn!=Z_setinc_foltrans_2&v__1(sortedList_first,Z_setinc_foltrans_2,nn)& (v__1(null,Z_setinc_foltrans_2,nn)|v__1(null,Z_setinc_foltrans_2,Z_setinc_foltrans_2)& -v__1(null,nn,nn))& (v__1(sortedList_first,nn,Z_setinc_foltrans_2)|v__1(sortedList_first,nn,nn)& -v__1(sortedList_first,Z_setinc_foltrans_2,Z_setinc_foltrans_2))|nn!=Z_setinc_foltrans_2&v__1(null,Z_setinc_foltrans_2,Z_setinc_foltrans_2)& (v__1(null,Z_setinc_foltrans_2,nn)|v__1(null,Z_setinc_foltrans_2,Z_setinc_foltrans_2)& -v__1(null,nn,nn))& (v__1(sortedList_first,nn,Z_setinc_foltrans_2)|v__1(sortedList_first,nn,nn)& -v__1(sortedList_first,Z_setinc_foltrans_2,Z_setinc_foltrans_2)))| ((all Fun_flat_foltrans_34 (-object(Fun_flat_foltrans_34)| -v__1(Fun_flat_foltrans_34,Z_setinc_foltrans_2,Z_setinc_foltrans_2)|Fun_flat_foltrans_34!=node_next(nn)))| (all Fun_flat_foltrans_35 (-object(Fun_flat_foltrans_35)| -v__1(Fun_flat_foltrans_35,Z_setinc_foltrans_2,nn)|Fun_flat_foltrans_35!=node_next(nn)))& ((all Fun_flat_foltrans_36 (-object(Fun_flat_foltrans_36)| -v__1(Fun_flat_foltrans_36,Z_setinc_foltrans_2,Z_setinc_foltrans_2)|Fun_flat_foltrans_36!=node_next(nn)))| (all Fun_flat_foltrans_37 (-object(Fun_flat_foltrans_37)|Fun_flat_foltrans_37!=node_next(nn)|v__1(Fun_flat_foltrans_37,nn,nn)))))& (nn=Z_setinc_foltrans_2| (all Fun_flat_foltrans_38 (-object(Fun_flat_foltrans_38)| -v__1(Fun_flat_foltrans_38,nn,Z_setinc_foltrans_2)|Fun_flat_foltrans_38!=node_next(nn)))& ((all Fun_flat_foltrans_39 (-object(Fun_flat_foltrans_39)| -v__1(Fun_flat_foltrans_39,nn,nn)|Fun_flat_foltrans_39!=node_next(nn)))| (all Fun_flat_foltrans_40 (-object(Fun_flat_foltrans_40)|Fun_flat_foltrans_40!=node_next(nn)|v__1(Fun_flat_foltrans_40,Z_setinc_foltrans_2,Z_setinc_foltrans_2))))| (all Fun_flat_foltrans_41 (-object(Fun_flat_foltrans_41)| -v__1(Fun_flat_foltrans_41,Z_setinc_foltrans_2,nn)|Fun_flat_foltrans_41!=node_next(nn)))| -v__1(null,Z_setinc_foltrans_2,nn)& (-v__1(null,Z_setinc_foltrans_2,Z_setinc_foltrans_2)|v__1(null,nn,nn)))& (nn=Z_setinc_foltrans_2| (all Fun_flat_foltrans_42 (-object(Fun_flat_foltrans_42)| -v__1(Fun_flat_foltrans_42,nn,Z_setinc_foltrans_2)|Fun_flat_foltrans_42!=node_next(nn)))& ((all Fun_flat_foltrans_43 (-object(Fun_flat_foltrans_43)| -v__1(Fun_flat_foltrans_43,nn,nn)|Fun_flat_foltrans_43!=node_next(nn)))| (all Fun_flat_foltrans_44 (-object(Fun_flat_foltrans_44)|Fun_flat_foltrans_44!=node_next(nn)|v__1(Fun_flat_foltrans_44,Z_setinc_foltrans_2,Z_setinc_foltrans_2))))| -v__1(null,Z_setinc_foltrans_2,Z_setinc_foltrans_2)| -v__1(null,Z_setinc_foltrans_2,nn)& (-v__1(null,Z_setinc_foltrans_2,Z_setinc_foltrans_2)|v__1(null,nn,nn)))| ((all Fun_flat_foltrans_45 (-object(Fun_flat_foltrans_45)| -v__1(Fun_flat_foltrans_45,Z_setinc_foltrans_2,prev_2)|Fun_flat_foltrans_45!=node_next(nn)))| (all Fun_flat_foltrans_46 (-object(Fun_flat_foltrans_46)| -v__1(Fun_flat_foltrans_46,prev_2,nn)|Fun_flat_foltrans_46!=node_next(nn)))& ((all Fun_flat_foltrans_47 (-object(Fun_flat_foltrans_47)| -v__1(Fun_flat_foltrans_47,prev_2,prev_2)|Fun_flat_foltrans_47!=node_next(nn)))| (all Fun_flat_foltrans_48 (-object(Fun_flat_foltrans_48)|Fun_flat_foltrans_48!=node_next(nn)|v__1(Fun_flat_foltrans_48,nn,nn)))))& (nn=prev_2| (all Fun_flat_foltrans_49 (-object(Fun_flat_foltrans_49)| -v__1(Fun_flat_foltrans_49,nn,prev_2)|Fun_flat_foltrans_49!=node_next(nn)))& ((all Fun_flat_foltrans_50 (-object(Fun_flat_foltrans_50)| -v__1(Fun_flat_foltrans_50,nn,nn)|Fun_flat_foltrans_50!=node_next(nn)))| (all Fun_flat_foltrans_51 (-object(Fun_flat_foltrans_51)|Fun_flat_foltrans_51!=node_next(nn)|v__1(Fun_flat_foltrans_51,prev_2,prev_2))))| (all Fun_flat_foltrans_52 (-object(Fun_flat_foltrans_52)| -v__1(Fun_flat_foltrans_52,Z_setinc_foltrans_2,nn)|Fun_flat_foltrans_52!=node_next(nn)))| -v__1(null,prev_2,nn)& (-v__1(null,prev_2,prev_2)|v__1(null,nn,nn)))& (nn=prev_2| (all Fun_flat_foltrans_53 (-object(Fun_flat_foltrans_53)| -v__1(Fun_flat_foltrans_53,nn,prev_2)|Fun_flat_foltrans_53!=node_next(nn)))& ((all Fun_flat_foltrans_54 (-object(Fun_flat_foltrans_54)| -v__1(Fun_flat_foltrans_54,nn,nn)|Fun_flat_foltrans_54!=node_next(nn)))| (all Fun_flat_foltrans_55 (-object(Fun_flat_foltrans_55)|Fun_flat_foltrans_55!=node_next(nn)|v__1(Fun_flat_foltrans_55,prev_2,prev_2))))| -v__1(null,Z_setinc_foltrans_2,prev_2)| -v__1(null,prev_2,nn)& (-v__1(null,prev_2,prev_2)|v__1(null,nn,nn)))& (((all Fun_flat_foltrans_56 (-object(Fun_flat_foltrans_56)| -v__1(Fun_flat_foltrans_56,Z_setinc_foltrans_2,Z_setinc_foltrans_2)|Fun_flat_foltrans_56!=node_next(nn)))| (all Fun_flat_foltrans_57 (-object(Fun_flat_foltrans_57)| -v__1(Fun_flat_foltrans_57,Z_setinc_foltrans_2,nn)|Fun_flat_foltrans_57!=node_next(nn)))& ((all Fun_flat_foltrans_58 (-object(Fun_flat_foltrans_58)| -v__1(Fun_flat_foltrans_58,Z_setinc_foltrans_2,Z_setinc_foltrans_2)|Fun_flat_foltrans_58!=node_next(nn)))| (all Fun_flat_foltrans_59 (-object(Fun_flat_foltrans_59)|Fun_flat_foltrans_59!=node_next(nn)|v__1(Fun_flat_foltrans_59,nn,nn)))))& (nn=Z_setinc_foltrans_2| (all Fun_flat_foltrans_60 (-object(Fun_flat_foltrans_60)| -v__1(Fun_flat_foltrans_60,nn,Z_setinc_foltrans_2)|Fun_flat_foltrans_60!=node_next(nn)))& ((all Fun_flat_foltrans_61 (-object(Fun_flat_foltrans_61)| -v__1(Fun_flat_foltrans_61,nn,nn)|Fun_flat_foltrans_61!=node_next(nn)))| (all Fun_flat_foltrans_62 (-object(Fun_flat_foltrans_62)|Fun_flat_foltrans_62!=node_next(nn)|v__1(Fun_flat_foltrans_62,Z_setinc_foltrans_2,Z_setinc_foltrans_2))))| (all Fun_flat_foltrans_63 (-object(Fun_flat_foltrans_63)| -v__1(Fun_flat_foltrans_63,Z_setinc_foltrans_2,nn)|Fun_flat_foltrans_63!=node_next(nn)))| -v__1(null,Z_setinc_foltrans_2,nn)& (-v__1(null,Z_setinc_foltrans_2,Z_setinc_foltrans_2)|v__1(null,nn,nn)))& (nn=Z_setinc_foltrans_2| (all Fun_flat_foltrans_64 (-object(Fun_flat_foltrans_64)| -v__1(Fun_flat_foltrans_64,nn,Z_setinc_foltrans_2)|Fun_flat_foltrans_64!=node_next(nn)))& ((all Fun_flat_foltrans_65 (-object(Fun_flat_foltrans_65)| -v__1(Fun_flat_foltrans_65,nn,nn)|Fun_flat_foltrans_65!=node_next(nn)))| % 24.35/24.52 Search stopped in tp_alloc by max_mem option. % 24.35/24.52 (all Fun_flat_foltrans_66 (-object(Fun_flat_foltrans_66)|Fun_flat_foltrans_66!=node_next(nn)|v__1(Fun_flat_foltrans_66,Z_setinc_foltrans_2,Z_setinc_foltrans_2))))| -v__1(null,Z_setinc_foltrans_2,Z_setinc_foltrans_2)| -v__1(null,Z_setinc_foltrans_2,nn)& (-v__1(null,Z_setinc_foltrans_2,Z_setinc_foltrans_2)|v__1(null,nn,nn)))| (all Fun_flat_foltrans_67 (-object(Fun_flat_foltrans_67)|Fun_flat_foltrans_67!=node_next(nn)|v__1(Fun_flat_foltrans_67,prev_2,prev_2)))& ((all Fun_flat_foltrans_68 (-object(Fun_flat_foltrans_68)|Fun_flat_foltrans_68!=node_next(nn)|v__1(Fun_flat_foltrans_68,prev_2,nn)))| (all Fun_flat_foltrans_69 (-object(Fun_flat_foltrans_69)|Fun_flat_foltrans_69!=node_next(nn)|v__1(Fun_flat_foltrans_69,prev_2,prev_2)))& (all Fun_flat_foltrans_70 (-object(Fun_flat_foltrans_70)| -v__1(Fun_flat_foltrans_70,nn,nn)|Fun_flat_foltrans_70!=node_next(nn))))|nn!=prev_2& (all Fun_flat_foltrans_71 (-object(Fun_flat_foltrans_71)|Fun_flat_foltrans_71!=node_next(nn)|v__1(Fun_flat_foltrans_71,prev_2,nn)))& (v__1(null,prev_2,nn)|v__1(null,prev_2,prev_2)& -v__1(null,nn,nn))& ((all Fun_flat_foltrans_72 (-object(Fun_flat_foltrans_72)|Fun_flat_foltrans_72!=node_next(nn)|v__1(Fun_flat_foltrans_72,nn,prev_2)))| (all Fun_flat_foltrans_73 (-object(Fun_flat_foltrans_73)|Fun_flat_foltrans_73!=node_next(nn)|v__1(Fun_flat_foltrans_73,nn,nn)))& (all Fun_flat_foltrans_74 (-object(Fun_flat_foltrans_74)| -v__1(Fun_flat_foltrans_74,prev_2,prev_2)|Fun_flat_foltrans_74!=node_next(nn))))|nn!=prev_2&v__1(null,prev_2,prev_2)& (v__1(null,prev_2,nn)|v__1(null,prev_2,prev_2)& -v__1(null,nn,nn))& ((all Fun_flat_foltrans_75 (-object(Fun_flat_foltrans_75)|Fun_flat_foltrans_75!=node_next(nn)|v__1(Fun_flat_foltrans_75,nn,prev_2)))| (all Fun_flat_foltrans_76 (-object(Fun_flat_foltrans_76)|Fun_flat_foltrans_76!=node_next(nn)|v__1(Fun_flat_foltrans_76,nn,nn)))& (all Fun_flat_foltrans_77 (-object(Fun_flat_foltrans_77)| -v__1(Fun_flat_foltrans_77,prev_2,prev_2)|Fun_flat_foltrans_77!=node_next(nn))))))|Z_setinc_foltrans_2!=null&v__1(sortedList_first,Z_setinc_foltrans_2,Z_setinc_foltrans_2)&Z_setinc_foltrans_2!=nn)). % 24.35/24.52 end_of_list. % 24.35/24.52 % 24.35/24.52 Search stopped in tp_alloc by max_mem option. % 24.35/24.52 % 24.35/24.52 ============ end of search ============ % 24.35/24.52 % 24.35/24.52 -------------- statistics ------------- % 24.35/24.52 clauses given 0 % 24.35/24.52 clauses generated 0 % 24.35/24.52 clauses kept 0 % 24.35/24.52 clauses forward subsumed 0 % 24.35/24.52 clauses back subsumed 0 % 24.35/24.52 Kbytes malloced 11718 % 24.35/24.52 % 24.35/24.52 ----------- times (seconds) ----------- % 24.35/24.52 user CPU time 21.15 (0 hr, 0 min, 21 sec) % 24.35/24.52 system CPU time 0.01 (0 hr, 0 min, 0 sec) % 24.35/24.52 wall-clock time 24 (0 hr, 0 min, 24 sec) % 24.35/24.52 % 24.35/24.52 Process 18445 finished Wed Jul 27 02:51:19 2022 % 24.35/24.52 Otter interrupted % 24.35/24.52 PROOF NOT FOUND %------------------------------------------------------------------------------