%------------------------------------------------------------------------------ % File : SPASS+T---2.2.22 % Problem : DAT106_1 : TPTP v8.1.0. Released v6.1.0. % Transfm : none % Format : tptp:raw % Command : spasst-tptp-script %s %d % Computer : n014.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 : Sat Jul 16 01:32:15 EDT 2022 % Result : Theorem 10.94s 6.26s % Output : Refutation 10.94s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : DAT106_1 : TPTP v8.1.0. Released v6.1.0. % 0.03/0.13 % Command : spasst-tptp-script %s %d % 0.12/0.34 % Computer : n014.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 600 % 0.12/0.34 % DateTime : Fri Jul 1 20:47:25 EDT 2022 % 0.12/0.34 % CPUTime : % 0.19/0.47 % Using integer theory % 10.94/6.26 % 10.94/6.26 % 10.94/6.26 % SZS status Theorem for /tmp/SPASST_19263_n014.cluster.edu % 10.94/6.26 % 10.94/6.26 SPASS V 2.2.22 in combination with yices. % 10.94/6.26 SPASS beiseite: Proof found by SPASS. % 10.94/6.26 Problem: /tmp/SPASST_19263_n014.cluster.edu % 10.94/6.26 SPASS derived 58808 clauses, backtracked 0 clauses and kept 4931 clauses. % 10.94/6.26 SPASS backtracked 0 times (0 times due to theory inconsistency). % 10.94/6.26 SPASS allocated 61472 KBytes. % 10.94/6.26 SPASS spent 0:00:05.18 on the problem. % 10.94/6.26 0:00:00.00 for the input. % 10.94/6.26 0:00:00.01 for the FLOTTER CNF translation. % 10.94/6.26 0:00:00.35 for inferences. % 10.94/6.26 0:00:00.00 for the backtracking. % 10.94/6.26 0:00:04.02 for the reduction. % 10.94/6.26 0:00:00.35 for interacting with the SMT procedure. % 10.94/6.26 % 10.94/6.26 % 10.94/6.26 % SZS output start CNFRefutation for /tmp/SPASST_19263_n014.cluster.edu % 10.94/6.26 % 10.94/6.26 % Here is a proof with depth 7, length 32 : % 10.94/6.26 2[0:Inp] || -> list(nil)*. % 10.94/6.26 4[0:Inp] || -> lesseq(0,skf3(U,V))*. % 10.94/6.26 7[0:Inp] || list(U) -> list(cons(V,U))*. % 10.94/6.26 8[0:Inp] || list(U) equal(cons(V,U),nil)** -> . % 10.94/6.26 10[0:Inp] || list(U) -> equal(head(cons(V,U)),V)**. % 10.94/6.26 11[0:Inp] || list(U) equal(U,nil) -> inRange(V,U)*. % 10.94/6.26 13[0:Inp] || list(U) inRange(V,U) -> list(skf2(V,U))* equal(U,nil). % 10.94/6.26 15[0:Inp] || list(U) inRange(V,U) -> equal(U,nil) equal(cons(skf3(V,U),skf2(V,U)),U)**. % 10.94/6.26 16[0:Inp] || equal(U,minus(V,2)) equal(W,minus(V,2))* list(X) inRange(V,X) greater(V,0) list(cons(W,X))* -> inRange(V,cons(U,X))*. % 10.94/6.26 21[0:ThA] || -> equal(plus(plus(U,uminus(V)),V),U)**. % 10.94/6.26 25[0:ThA] || -> equal(plus(U,0),U)**. % 10.94/6.26 28[0:ThA] || -> less(U,plus(U,1))*. % 10.94/6.26 50[0:ArS:16.4] || equal(U,plus(V,-2)) equal(W,plus(V,-2))* list(X) inRange(V,X) less(0,V) list(cons(W,X))* -> inRange(V,cons(U,X))*. % 10.94/6.26 51[0:TOC:50.4] || equal(U,plus(V,-2)) equal(W,plus(V,-2))* list(X) inRange(V,X) list(cons(W,X))* -> lesseq(V,0) inRange(V,cons(U,X))*. % 10.94/6.26 52[0:MRR:51.4,7.1] || list(U) inRange(V,U) equal(W,plus(V,-2))*+ equal(X,plus(V,-2)) -> lesseq(V,0) inRange(V,cons(X,U))*. % 10.94/6.26 89[0:SpR:15.3,10.1] || list(U) inRange(V,U) list(skf2(V,U))* -> equal(U,nil) equal(skf3(V,U),head(U)). % 10.94/6.26 92[0:MRR:89.2,13.2] || list(U) inRange(V,U) -> equal(U,nil) equal(skf3(V,U),head(U))**. % 10.94/6.26 132[0:SpL:21.0,52.2] || list(U) inRange(plus(V,uminus(-2)),U) equal(W,V)* equal(X,plus(plus(V,uminus(-2)),-2)) -> lesseq(plus(V,uminus(-2)),0) inRange(plus(V,uminus(-2)),cons(X,U))*. % 10.94/6.26 136[0:ArS:132.5] || list(U) inRange(plus(V,2),U) equal(W,V)* equal(X,plus(V,0)) -> lesseq(V,-2) inRange(plus(V,2),cons(X,U))*. % 10.94/6.26 137[0:AED:136.2] || list(U) inRange(plus(V,2),U) equal(W,plus(V,0)) -> lesseq(V,-2) inRange(plus(V,2),cons(W,U))*. % 10.94/6.26 138[0:Rew:25.0,137.2] || list(U) inRange(plus(V,2),U) equal(W,V) -> lesseq(V,-2) inRange(plus(V,2),cons(W,U))*. % 10.94/6.26 159[0:SpR:92.3,4.0] || list(U) inRange(V,U)*+ -> equal(U,nil) lesseq(0,head(U))*. % 10.94/6.26 672[0:Res:138.4,159.1] || list(U) inRange(plus(V,2),U)* equal(W,V)* list(cons(W,U)) -> lesseq(V,-2) equal(cons(W,U),nil) lesseq(0,head(cons(W,U)))*. % 10.94/6.26 688[0:Rew:10.1,672.6] || list(U) inRange(plus(V,2),U)* equal(W,V)* list(cons(W,U))* -> lesseq(V,-2) equal(cons(W,U),nil) lesseq(0,W). % 10.94/6.26 689[0:MRR:688.3,688.5,7.1,8.1] || list(U) inRange(plus(V,2),U)*+ equal(W,V)* -> lesseq(V,-2) lesseq(0,W)*. % 10.94/6.26 19250[0:Res:11.2,689.1] || list(U)* equal(U,nil) list(U)* equal(V,W)* -> lesseq(W,-2)* lesseq(0,V)*. % 10.94/6.26 19257[0:Obv:19250.0] || equal(U,nil)+ list(U)* equal(V,W)* -> lesseq(W,-2)* lesseq(0,V)*. % 10.94/6.26 48906[0:EqR:19257.0] || list(nil)* equal(U,V)* -> lesseq(V,-2)* lesseq(0,U)*. % 10.94/6.26 48907[0:MRR:48906.0,2.0] || equal(U,V)*+ -> lesseq(V,-2)* lesseq(0,U)*. % 10.94/6.26 111220[0:EqR:48907.0] || -> lesseq(U,-2)* lesseq(0,U). % 10.94/6.26 111245[0:OCE:111220.0,28.0] || -> lesseq(0,plus(-2,1))*. % 10.94/6.26 111299(e)[0:ArS:111245.0] || -> . % 10.94/6.26 % 10.94/6.26 % SZS output end CNFRefutation for /tmp/SPASST_19263_n014.cluster.edu % 10.94/6.26 % 10.94/6.26 Formulae used in the proof : fof_head_type fof_list_type fof_tail_type fof_cons_type fof_l2 fof_l1 fof_l3 fof_inRange fof_nil_type % 22.59/12.12 % 22.59/12.12 SPASS+T ended %------------------------------------------------------------------------------