%------------------------------------------------------------------------------ % File : SPASS+T---2.2.22 % Problem : DAT078_1 : 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 : Sat Jul 16 01:32:07 EDT 2022 % Result : Theorem 0.82s 1.50s % Output : Refutation 0.82s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : DAT078_1 : TPTP v8.1.0. Released v6.1.0. % 0.07/0.13 % Command : spasst-tptp-script %s %d % 0.13/0.34 % Computer : n021.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 : Fri Jul 1 18:11:29 EDT 2022 % 0.13/0.34 % CPUTime : % 0.20/0.48 % Using integer theory % 0.82/1.50 % 0.82/1.50 % 0.82/1.50 % SZS status Theorem for /tmp/SPASST_834_n021.cluster.edu % 0.82/1.50 % 0.82/1.50 SPASS V 2.2.22 in combination with yices. % 0.82/1.50 SPASS beiseite: Proof found by SPASS. % 0.82/1.50 Problem: /tmp/SPASST_834_n021.cluster.edu % 0.82/1.50 SPASS derived 3272 clauses, backtracked 0 clauses and kept 749 clauses. % 0.82/1.50 SPASS backtracked 0 times (0 times due to theory inconsistency). % 0.82/1.50 SPASS allocated 9814 KBytes. % 0.82/1.50 SPASS spent 0:00:00.43 on the problem. % 0.82/1.50 0:00:00.00 for the input. % 0.82/1.50 0:00:00.01 for the FLOTTER CNF translation. % 0.82/1.50 0:00:00.04 for inferences. % 0.82/1.50 0:00:00.00 for the backtracking. % 0.82/1.50 0:00:00.30 for the reduction. % 0.82/1.50 0:00:00.04 for interacting with the SMT procedure. % 0.82/1.50 % 0.82/1.50 % 0.82/1.50 % SZS output start CNFRefutation for /tmp/SPASST_834_n021.cluster.edu % 0.82/1.50 % 0.82/1.50 % Here is a proof with depth 3, length 25 : % 0.82/1.50 4[0:Inp] || -> array(init(U))*. % 0.82/1.50 11[0:Inp] || -> equal(read(init(U),V),U)**. % 0.82/1.50 21[0:Inp] || greater(U,0) sorted(V,U) array(V) -> distinct(V,U)*. % 0.82/1.50 24[0:Inp] || array(U) lesseq(read(U,skf11(U,V)),read(U,skf10(U,V)))* -> sorted(U,V). % 0.82/1.50 35[0:Inp] || array(U) greater(V,W)* greatereq(W,0) equal(read(U,X),read(U,W))* greatereq(X,0) greater(V,X)* distinct(U,V)* -> equal(X,W). % 0.82/1.50 45[0:ThA] || -> lesseq(U,U)*. % 0.82/1.50 74[0:ArS:21.0] || less(0,U) sorted(V,U) array(V) -> distinct(V,U)*. % 0.82/1.50 75[0:TOC:74.0] || array(U) sorted(U,V) -> distinct(U,V)* lesseq(V,0). % 0.82/1.50 76[0:TOC:24.1] || array(U) -> sorted(U,V) less(read(U,skf10(U,V)),read(U,skf11(U,V)))*. % 0.82/1.50 92[0:ArS:35.5] || array(U) less(V,W)* lesseq(0,V) equal(read(U,X),read(U,V))* lesseq(0,X) less(X,W)* distinct(U,W)* -> equal(X,V). % 0.82/1.50 93[0:TOC:92.4] || array(U) distinct(U,V)* equal(read(U,W),read(U,X))*+ -> equal(W,X) lesseq(V,X)* lesseq(V,W)* less(X,0) less(W,0). % 0.82/1.50 97[0:Res:4.0,75.0] || sorted(init(U),V) -> lesseq(V,0) distinct(init(U),V)*. % 0.82/1.50 144[0:SpR:11.0,76.2] || array(init(U)) -> sorted(init(U),V) less(read(init(U),skf10(init(U),V)),U)*. % 0.82/1.50 150[0:Rew:11.0,144.2] || array(init(U)) -> sorted(init(U),V)* less(U,U)*. % 0.82/1.50 151[0:MRR:150.0,4.0] || -> sorted(init(U),V)* less(U,U)*. % 0.82/1.50 165[0:OCE:151.1,45.0] || -> sorted(init(U),V)*. % 0.82/1.50 166[0:MRR:97.0,165.0] || -> lesseq(U,0) distinct(init(V),U)*. % 0.82/1.50 597[0:SpL:11.0,93.2] || array(init(U)) distinct(init(U),V)* equal(read(init(U),W),U)** -> equal(W,X)* lesseq(V,X)* lesseq(V,W)* less(X,0) less(W,0). % 0.82/1.50 601[0:Rew:11.0,597.2] || array(init(U)) distinct(init(U),V)* equal(U,U) -> equal(W,X)* lesseq(V,X)* lesseq(V,W)* less(X,0) less(W,0). % 0.82/1.50 602[0:Obv:601.2] || array(init(U)) distinct(init(U),V)* -> equal(W,X)* lesseq(V,X)* lesseq(V,W)* less(X,0) less(W,0). % 0.82/1.50 603[0:MRR:602.0,4.0] || distinct(init(U),V)*+ -> equal(W,X)* lesseq(V,X)* lesseq(V,W)* less(X,0) less(W,0). % 0.82/1.50 1440[0:Res:166.1,603.0] || -> lesseq(U,0)* equal(V,W)* lesseq(U,W)* lesseq(U,V)* less(W,0) less(V,0). % 0.82/1.50 1445[0:BLD:1440.0] || -> equal(U,V)* less(V,0)* less(U,0)*. % 0.82/1.50 4841[0:OCE:1445.1,45.0] || -> equal(U,0) less(U,0)*. % 0.82/1.50 4939(e)[0:BLD:4841.0] || -> . % 0.82/1.50 % 0.82/1.50 % SZS output end CNFRefutation for /tmp/SPASST_834_n021.cluster.edu % 0.82/1.50 % 0.82/1.50 Formulae used in the proof : fof_array_type fof_a fof_distinct fof_rev_n1_proper % 0.82/1.55 % 0.82/1.55 SPASS+T ended %------------------------------------------------------------------------------