%------------------------------------------------------------------------------ % File : SPASS+T---2.2.22 % Problem : SWX000_1 : TPTP v9.1.0. Released v9.1.0. % Transfm : none % Format : tptp:raw % Command : spasst-tptp-script %s %d % Computer : n015.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 : Sun Apr 6 10:09:26 AM UTC 2025 % Result : Theorem 0.78s 1.15s % Output : Refutation 0.78s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.12 % Problem : SWX000_1 : TPTP v9.1.0. Released v9.1.0. % 0.12/0.13 % Command : spasst-tptp-script %s %d % 0.12/0.34 % Computer : n015.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 : 300 % 0.12/0.34 % DateTime : Sun Apr 6 03:04:50 EDT 2025 % 0.12/0.34 % CPUTime : % 0.19/0.48 % Using integer theory % 0.78/1.15 % 0.78/1.15 % 0.78/1.15 % SZS status Theorem for /tmp/SPASST_12381_n015.cluster.edu % 0.78/1.15 % 0.78/1.15 SPASS V 2.2.22 in combination with yices. % 0.78/1.15 SPASS beiseite: Proof found by SPASS. % 0.78/1.15 Problem: /tmp/SPASST_12381_n015.cluster.edu % 0.78/1.15 SPASS derived 930 clauses, backtracked 22 clauses and kept 439 clauses. % 0.78/1.15 SPASS backtracked 3 times (0 times due to theory inconsistency). % 0.78/1.15 SPASS allocated 6981 KBytes. % 0.78/1.15 SPASS spent 0:00:00.06 on the problem. % 0.78/1.15 0:00:00.00 for the input. % 0.78/1.15 0:00:00.00 for the FLOTTER CNF translation. % 0.78/1.15 0:00:00.00 for inferences. % 0.78/1.15 0:00:00.00 for the backtracking. % 0.78/1.15 0:00:00.03 for the reduction. % 0.78/1.15 0:00:00.01 for interacting with the SMT procedure. % 0.78/1.15 % 0.78/1.15 % 0.78/1.15 % SZS output start CNFRefutation for /tmp/SPASST_12381_n015.cluster.edu % 0.78/1.15 % 0.78/1.15 % Here is a proof with depth 6, length 61 : % 0.78/1.15 5[0:Inp] || -> general(skc3)*. % 0.78/1.15 7[0:Inp] || -> general(f__integer__(U))*. % 0.78/1.15 9[0:Inp] || hp(U) -> SkP0(U)*. % 0.78/1.15 11[0:Inp] || SkP0(skc3) tp(skc3)* -> . % 0.78/1.15 12[0:Inp] || -> SkP0(U)* equal(U,f__integer__(4))*. % 0.78/1.15 14[0:Inp] || SkP0(skc3)* -> equal(f__integer__(4),skc3). % 0.78/1.15 15[0:Inp] || general(U) hp(U) -> tp(U)*. % 0.78/1.16 18[0:Inp] || lesseq(U,V) -> p__less_equal__(f__integer__(U),f__integer__(V))*. % 0.78/1.16 19[0:Inp] || equal(f__integer__(U),f__integer__(V))* -> equal(U,V). % 0.78/1.16 21[0:Inp] || general(U) equal(U,f__integer__(V))*+ -> p__is_integer__(U)*. % 0.78/1.16 23[0:Inp] || general(U) p__is_integer__(U) -> equal(f__integer__(skf2(U)),U)**. % 0.78/1.16 35[0:Inp] || general(U) general(V) p__less_equal__(V,U)* -> equal(U,V) p__greater__(U,V). % 0.78/1.16 36[0:Inp] || general(U) general(V) p__less_equal__(U,V)* -> equal(U,V) p__less__(U,V). % 0.78/1.16 40[0:Inp] || general(U) p__less__(U,f__integer__(5))* general(f__integer__(5)) p__greater__(U,f__integer__(3)) general(f__integer__(3)) equal(V,U)* general(V) -> hp(V)*. % 0.78/1.16 51[0:ThA] || -> less(U,plus(U,1))*. % 0.78/1.16 52[0:ThA] || -> less(plus(U,-1),U)*. % 0.78/1.16 72[0:MRR:14.0,12.0] || -> equal(f__integer__(4),skc3)**. % 0.78/1.16 74[0:TOC:18.0] || -> less(U,V) p__less_equal__(f__integer__(V),f__integer__(U))*. % 0.78/1.16 76(e)[0:MRR:40.2,40.4,7.0,7.0] || general(U) general(V) equal(U,V)* p__greater__(V,f__integer__(3)) p__less__(V,f__integer__(5))* -> hp(U)*. % 0.78/1.16 93[0:Res:5.0,23.1] || p__is_integer__(skc3) -> equal(f__integer__(skf2(skc3)),skc3)**. % 0.78/1.16 95[0:Res:5.0,15.1] || hp(skc3) -> tp(skc3)*. % 0.78/1.16 110[0:Res:72.0,76.3] || general(skc3) p__less__(skc3,f__integer__(5))* p__greater__(skc3,f__integer__(3)) general(f__integer__(4)) -> hp(f__integer__(4)). % 0.78/1.16 122[0:Res:72.0,21.0] || general(skc3) -> p__is_integer__(skc3)*. % 0.78/1.16 123[0:MRR:122.0,5.0] || -> p__is_integer__(skc3)*. % 0.78/1.16 124[0:MRR:93.0,123.0] || -> equal(f__integer__(skf2(skc3)),skc3)**. % 0.78/1.16 138[0:Rew:72.0,110.4,72.0,110.3] || general(skc3) p__less__(skc3,f__integer__(5))* p__greater__(skc3,f__integer__(3)) general(skc3) -> hp(skc3). % 0.78/1.16 139[0:Obv:138.0] || p__less__(skc3,f__integer__(5))* p__greater__(skc3,f__integer__(3)) general(skc3) -> hp(skc3). % 0.78/1.16 140[0:MRR:139.2,5.0] || p__greater__(skc3,f__integer__(3)) p__less__(skc3,f__integer__(5))* -> hp(skc3). % 0.78/1.16 189[0:Res:95.1,11.1] || hp(skc3) SkP0(skc3)* -> . % 0.78/1.16 190[0:MRR:189.1,9.1] || hp(skc3)* -> . % 0.78/1.16 191[0:MRR:140.2,190.0] || p__greater__(skc3,f__integer__(3)) p__less__(skc3,f__integer__(5))* -> . % 0.78/1.16 207[0:SpR:124.0,74.1] || -> less(skf2(skc3),U)* p__less_equal__(f__integer__(U),skc3). % 0.78/1.16 209[0:SpR:124.0,74.1] || -> less(U,skf2(skc3))* p__less_equal__(skc3,f__integer__(U)). % 0.78/1.16 244[0:OCE:207.0,52.0] || -> p__less_equal__(f__integer__(plus(skf2(skc3),-1)),skc3)*. % 0.78/1.16 256[0:OCE:209.0,51.0] || -> p__less_equal__(skc3,f__integer__(plus(skf2(skc3),1)))*. % 0.78/1.16 268[0:SpL:72.0,19.0] || equal(f__integer__(U),skc3)** -> equal(4,U). % 0.78/1.16 305[0:SpL:124.0,268.0] || equal(skc3,skc3) -> equal(skf2(skc3),4)**. % 0.78/1.16 308[0:Obv:305.0] || -> equal(skf2(skc3),4)**. % 0.78/1.16 311[0:Rew:308.0,244.0] || -> p__less_equal__(f__integer__(plus(4,-1)),skc3)*. % 0.78/1.16 313[0:Rew:308.0,256.0] || -> p__less_equal__(skc3,f__integer__(plus(4,1)))*. % 0.78/1.16 318[0:ArS:311.0] || -> p__less_equal__(f__integer__(3),skc3)*. % 0.78/1.16 319[0:ArS:313.0] || -> p__less_equal__(skc3,f__integer__(5))*. % 0.78/1.16 1202[0:Res:319.0,35.2] || general(f__integer__(5)) general(skc3) -> equal(f__integer__(5),skc3) p__greater__(f__integer__(5),skc3)*. % 0.78/1.16 1207[0:Res:318.0,35.2] || general(skc3) general(f__integer__(3)) -> equal(f__integer__(3),skc3) p__greater__(skc3,f__integer__(3))*. % 0.78/1.16 1211(e)[0:MRR:1202.0,1202.1,7.0,5.0] || -> equal(f__integer__(5),skc3) p__greater__(f__integer__(5),skc3)*. % 0.78/1.16 1212(e)[0:MRR:1207.0,1207.1,5.0,7.0] || -> equal(f__integer__(3),skc3) p__greater__(skc3,f__integer__(3))*. % 0.78/1.16 1222[1:Spt:1211.0] || -> equal(f__integer__(5),skc3)**. % 0.78/1.16 1251[1:SpL:1222.0,268.0] || equal(skc3,skc3)* -> equal(5,4). % 0.78/1.16 1269[1:ArS:1251.1] || equal(skc3,skc3)* -> . % 0.78/1.16 1270(e)[1:Obv:1269.0] || -> . % 0.78/1.16 1275[1:Spt:1270.0,1211.0,1222.0] || equal(f__integer__(5),skc3)** -> . % 0.78/1.16 1276[1:Spt:1270.0,1211.1] || -> p__greater__(f__integer__(5),skc3)*. % 0.78/1.16 1282[2:Spt:1212.0] || -> equal(f__integer__(3),skc3)**. % 0.78/1.16 1310[2:SpL:1282.0,268.0] || equal(skc3,skc3)* -> equal(4,3). % 0.78/1.16 1327[2:ArS:1310.1] || equal(skc3,skc3)* -> . % 0.78/1.16 1328(e)[2:Obv:1327.0] || -> . % 0.78/1.16 1333[2:Spt:1328.0,1212.0,1282.0] || equal(f__integer__(3),skc3)** -> . % 0.78/1.16 1334[2:Spt:1328.0,1212.1] || -> p__greater__(skc3,f__integer__(3))*. % 0.78/1.16 1335[2:MRR:191.0,1334.0] || p__less__(skc3,f__integer__(5))* -> . % 0.78/1.16 1412[0:Res:319.0,36.2] || general(skc3) general(f__integer__(5)) -> equal(f__integer__(5),skc3) p__less__(skc3,f__integer__(5))*. % 0.78/1.16 1420(e)[2:MRR:1412.0,1412.1,1412.2,1412.3,5.0,7.0,1275.0,1335.0] || -> . % 0.78/1.16 % 0.78/1.16 % SZS output end CNFRefutation for /tmp/SPASST_12381_n015.cluster.edu % 0.78/1.16 % 0.78/1.16 Formulae used in the proof : fof_general_type fof_p__is_symbolic__def_ax fof_symbol_type fof_minimal_element_ax fof_f__symbolic___decl fof_formula_2_right_0 fof_maximal_element_ax fof_numeral_ordering_ax fof_f__integer__def_ax fof_f__symbolic__def_ax fof_p__greater__def_ax fof_formula_1_left_0 % 0.84/1.18 % 0.84/1.18 SPASS+T ended %------------------------------------------------------------------------------