%------------------------------------------------------------------------------ % File : SPASS+T---2.2.22 % Problem : SWW626_2 : TPTP v8.1.0. Released v6.1.0. % Transfm : none % Format : tptp:raw % Command : spasst-tptp-script %s %d % Computer : n021.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 : Thu Jul 21 01:30:34 EDT 2022 % Result : Theorem 1.44s 1.74s % Output : Refutation 1.44s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SWW626_2 : TPTP v8.1.0. Released v6.1.0. % 0.03/0.12 % Command : spasst-tptp-script %s %d % 0.12/0.33 % Computer : n021.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 : 600 % 0.12/0.33 % DateTime : Sat Jun 4 19:45:18 EDT 2022 % 0.12/0.33 % CPUTime : % 0.19/0.46 % Using integer theory % 1.44/1.74 % 1.44/1.74 % 1.44/1.74 % SZS status Theorem for /tmp/SPASST_30104_n021.cluster.edu % 1.44/1.74 % 1.44/1.74 SPASS V 2.2.22 in combination with yices. % 1.44/1.74 SPASS beiseite: Proof found by SMT. % 1.44/1.74 Problem: /tmp/SPASST_30104_n021.cluster.edu % 1.44/1.74 SPASS derived 509 clauses, backtracked 0 clauses and kept 600 clauses. % 1.44/1.74 SPASS backtracked 1 times (1 times due to theory inconsistency). % 1.44/1.74 SPASS allocated 7515 KBytes. % 1.44/1.74 SPASS spent 0:00:00.14 on the problem. % 1.44/1.74 0:00:00.00 for the input. % 1.44/1.74 0:00:00.03 for the FLOTTER CNF translation. % 1.44/1.74 0:00:00.00 for inferences. % 1.44/1.74 0:00:00.00 for the backtracking. % 1.44/1.74 0:00:00.04 for the reduction. % 1.44/1.74 0:00:00.01 for interacting with the SMT procedure. % 1.44/1.74 % 1.44/1.74 % 1.44/1.74 % SZS output start CNFRefutation for /tmp/SPASST_30104_n021.cluster.edu % 1.44/1.74 % 1.44/1.74 % Here is a proof with depth 0, length 20 : % 1.44/1.74 7[0:Inp] || -> ty(elt1)*. % 1.44/1.74 21[0:Inp] || -> list_elt(skc17)*. % 1.44/1.74 22[0:Inp] || -> list_elt(skc16)*. % 1.44/1.74 23[0:Inp] || -> list_elt(skc15)*. % 1.44/1.74 24[0:Inp] || -> list_elt(skc14)*. % 1.44/1.74 27[0:Inp] || -> list_elt(skc12)*. % 1.44/1.74 57(e)[0:Inp] || list_elt(U) -> uni(t2tb(U))*. % 1.44/1.74 58(e)[0:Inp] || ty(U) -> uni(nil(U))*. % 1.44/1.74 71(e)[0:Inp] || uni(U) -> equal(t2tb(tb2t(U)),U)**. % 1.44/1.74 86(e)[0:Inp] || permut(elt1,t2tb(skc17),prefix(elt1,skc13,t2tb(skc12)))* -> . % 1.44/1.74 91(e)[0:Inp] || ty(U) uni(V) -> uni(prefix(U,W,V))*. % 1.44/1.74 92[0:Inp] || -> permut(elt1,t2tb(skc15),prefix(elt1,div_f(skc13,2),t2tb(skc12)))*. % 1.44/1.74 113(e)[0:Inp] || ty(U) uni(V) -> equal(infix_plpl(U,nil(U),V),V)**. % 1.44/1.74 114[0:Inp] || -> permut(elt1,t2tb(skc16),prefix(elt1,minus(skc13,div_f(skc13,2)),t2tb(skc14)))*. % 1.44/1.74 117(e)[0:Inp] || ty(U) uni(V) uni(W) -> uni(infix_plpl(U,V,W))*. % 1.44/1.74 120[0:Inp] || -> permut(elt1,t2tb(skc17),infix_plpl(elt1,infix_plpl(elt1,nil(elt1),t2tb(skc15)),t2tb(skc16)))*. % 1.44/1.74 172[0:Inp] || -> equal(tb2t(infix_plpl(elt1,prefix(elt1,div_f(skc13,2),t2tb(skc12)),prefix(elt1,minus(skc13,div_f(skc13,2)),t2tb(skc14)))),tb2t(prefix(elt1,skc13,t2tb(skc12))))**. % 1.44/1.74 176(e)[0:Inp] || ty(U) uni(V) uni(W) uni(X) permut(U,V,W)* permut(U,W,X)* -> permut(U,V,X)*. % 1.44/1.74 209(e)[0:Inp] || ty(U) uni(V) uni(W) uni(X) uni(Y) permut(U,V,X) permut(U,W,Y) -> permut(U,infix_plpl(U,V,W),infix_plpl(U,X,Y))*. % 1.44/1.74 1013(e)[0:ThR:209,176,172,120,117,114,113,92,91,86,71,58,57,27,24,23,22,21,7] || -> . % 1.44/1.74 % 1.44/1.74 % SZS output end CNFRefutation for /tmp/SPASST_30104_n021.cluster.edu % 1.44/1.74 % 1.44/1.74 Formulae used in the proof : fof_list_elt fof_uni fof_wP_parameter_rev_sort fof_tb2t fof_t2tb fof_bridgeL1 fof_cons_proj_1 fof_cons_proj_1_sort fof_prefix fof_append_l_nil fof_infix_plpl_def fof_rev_append fof_div_mult fof_permut_def fof_mem_def % 1.44/1.74 % 1.44/1.74 SPASS+T ended %------------------------------------------------------------------------------