%------------------------------------------------------------------------------ % File : SPASS+T---2.2.22 % Problem : SEV422_1 : TPTP v8.1.0. Released v5.0.0. % Transfm : none % Format : tptp:raw % Command : spasst-tptp-script %s %d % Computer : n006.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 : Tue Jul 19 18:16:31 EDT 2022 % Result : Theorem 1.59s 1.48s % Output : Refutation 1.59s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SEV422_1 : TPTP v8.1.0. Released v5.0.0. % 0.07/0.12 % Command : spasst-tptp-script %s %d % 0.12/0.33 % Computer : n006.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 : Tue Jun 28 06:18:53 EDT 2022 % 0.12/0.33 % CPUTime : % 0.19/0.46 % Using integer theory % 1.59/1.48 % 1.59/1.48 % 1.59/1.48 % SZS status Theorem for /tmp/SPASST_8439_n006.cluster.edu % 1.59/1.48 % 1.59/1.48 SPASS V 2.2.22 in combination with yices. % 1.59/1.48 SPASS beiseite: Proof found by SPASS. % 1.59/1.48 Problem: /tmp/SPASST_8439_n006.cluster.edu % 1.59/1.48 SPASS derived 2240 clauses, backtracked 257 clauses and kept 982 clauses. % 1.59/1.48 SPASS backtracked 10 times (0 times due to theory inconsistency). % 1.59/1.48 SPASS allocated 8838 KBytes. % 1.59/1.48 SPASS spent 0:00:00.41 on the problem. % 1.59/1.48 0:00:00.00 for the input. % 1.59/1.48 0:00:00.01 for the FLOTTER CNF translation. % 1.59/1.48 0:00:00.03 for inferences. % 1.59/1.48 0:00:00.01 for the backtracking. % 1.59/1.48 0:00:00.30 for the reduction. % 1.59/1.48 0:00:00.04 for interacting with the SMT procedure. % 1.59/1.48 % 1.59/1.48 % 1.59/1.48 % SZS output start CNFRefutation for /tmp/SPASST_8439_n006.cluster.edu % 1.59/1.48 % 1.59/1.48 % Here is a proof with depth 4, length 28 : % 1.59/1.48 5[0:Inp] || -> element(skc5)*. % 1.59/1.48 6[0:Inp] || -> set(skc4)*. % 1.59/1.48 7[0:Inp] || -> element(skf2(U))*. % 1.59/1.48 9[0:Inp] || member(skc5,skc4)* -> . % 1.59/1.48 11[0:Inp] || element(U) -> set(singleton(U))*. % 1.59/1.48 12[0:Inp] || set(U) -> equal(U,empty_set) member(skf2(U),U)*. % 1.59/1.48 15[0:Inp] || set(U) set(V) -> set(intersection(U,V))*. % 1.59/1.48 18[0:Inp] || equal(cardinality(union(singleton(skc5),skc4)),plus(cardinality(skc4),1))** -> . % 1.59/1.48 21[0:Inp] || element(U) element(V) member(U,singleton(V))* -> equal(U,V). % 1.59/1.48 31[0:Inp] || element(U) set(V) set(W) member(U,intersection(V,W))* -> member(U,V). % 1.59/1.48 32[0:Inp] || element(U) set(V) set(W) member(U,intersection(V,W))* -> member(U,W). % 1.59/1.48 43[0:Inp] || element(U) set(V) equal(intersection(singleton(U),V),empty_set) -> equal(cardinality(union(singleton(U),V)),plus(cardinality(V),1))**. % 1.59/1.48 91(e)[0:Res:6.0,31.0] || element(U) set(V) member(U,intersection(V,skc4))* -> member(U,V). % 1.59/1.48 92[0:Res:6.0,32.0] || element(U) set(V) member(U,intersection(V,skc4))* -> member(U,skc4). % 1.59/1.48 102[0:Res:6.0,15.0] || set(U) -> set(intersection(U,skc4))*. % 1.59/1.48 124[0:Res:5.0,21.0] || element(U) member(U,singleton(skc5))* -> equal(U,skc5). % 1.59/1.48 127[0:Res:5.0,11.0] || -> set(singleton(skc5))*. % 1.59/1.48 1546[0:SpL:43.3,18.0] || element(skc5) set(skc4) equal(intersection(singleton(skc5),skc4),empty_set)** equal(plus(cardinality(skc4),1),plus(cardinality(skc4),1)) -> . % 1.59/1.48 1550[0:Obv:1546.3] || element(skc5) set(skc4) equal(intersection(singleton(skc5),skc4),empty_set)** -> . % 1.59/1.48 1551[0:MRR:1550.0,1550.1,5.0,6.0] || equal(intersection(singleton(skc5),skc4),empty_set)** -> . % 1.59/1.48 2144[0:Res:12.2,92.2] || set(intersection(U,skc4)) element(skf2(intersection(U,skc4))) set(U) -> equal(intersection(U,skc4),empty_set) member(skf2(intersection(U,skc4)),skc4)*. % 1.59/1.48 2151[0:MRR:2144.0,2144.1,102.1,7.0] || set(U) -> equal(intersection(U,skc4),empty_set) member(skf2(intersection(U,skc4)),skc4)*. % 1.59/1.48 2409[0:Res:12.2,91.2] || set(intersection(U,skc4)) element(skf2(intersection(U,skc4))) set(U) -> equal(intersection(U,skc4),empty_set) member(skf2(intersection(U,skc4)),U)*. % 1.59/1.48 2418[0:MRR:2409.0,2409.1,102.1,7.0] || set(U) -> equal(intersection(U,skc4),empty_set) member(skf2(intersection(U,skc4)),U)*. % 1.59/1.48 3533[0:Res:2418.2,124.1] || set(singleton(skc5)) element(skf2(intersection(singleton(skc5),skc4)))* -> equal(intersection(singleton(skc5),skc4),empty_set) equal(skf2(intersection(singleton(skc5),skc4)),skc5). % 1.59/1.48 3548[0:MRR:3533.0,3533.1,3533.2,127.0,7.0,1551.0] || -> equal(skf2(intersection(singleton(skc5),skc4)),skc5)**. % 1.59/1.48 3592[0:SpR:3548.0,2151.2] || set(singleton(skc5)) -> equal(intersection(singleton(skc5),skc4),empty_set)** member(skc5,skc4). % 1.59/1.48 3595(e)[0:MRR:3592.0,3592.1,3592.2,127.0,1551.0,9.0] || -> . % 1.59/1.48 % 1.59/1.48 % SZS output end CNFRefutation for /tmp/SPASST_8439_n006.cluster.edu % 1.59/1.48 % 1.59/1.48 Formulae used in the proof : fof_set_type fof_vc2 fof_subset fof_element_type fof_complement_type fof_singleton_type fof_union_type fof_cardinality_empty_set fof_union fof_intersection fof_cardinality_intersection_2 % 1.67/1.54 % 1.67/1.54 SPASS+T ended %------------------------------------------------------------------------------